empty_ne_singleton
plain-language theorem explainer
The empty set and its singleton are unequal in Mathlib's ZF universe: ∅ ∈ {∅} while ∅ ∉ ∅, so they are the von Neumann 0 and 1. Anyone building a faithful ZFC parse of the primitive recognition calculus cites this as the first concrete distinction. The proof is a short membership contradiction via singleton introduction and empty non-membership.
Claim. In the fixed-universe ZF set model, $\emptyset \neq \{\emptyset\}$. Equivalently, the von Neumann numerals $0$ and $1$ are distinct sets, since $\emptyset \in \{\emptyset\}$ but $\emptyset \notin \emptyset$.
background
This module pins Mathlib's ZFSet at universe level 0 as the working ZF universe, so the FormalSystem interface (Type-0) can host a full ZFC parse of the primitive recognition calculus (PRC). The local goal is to exhibit ZFC as a concrete formal system that realizes the δ-core: extensional equality, a genuine first distinction, infinity, and an embedding of the recognition distinction structure.
The two sets in play are the empty set and the singleton of the empty set. In von Neumann arithmetic they are 0 and 1. Distinction here is purely extensional: they differ by the member ∅. Upstream, the module imports Mathlib ZFC basics and the PRC distinction dichotomy; the sibling abbreviation ZF simply names ZFSet at level 0.
Downstream packaging treats this inequality as one of the five conjuncts that certify a faithful ZFC parse of δ.
proof idea
Assume for contradiction that ∅ = {∅}. From the singleton membership rule, ∅ ∈ {∅}. Transport that membership along the assumed equality to obtain ∅ ∈ ∅. The empty-set non-membership axiom then yields an immediate contradiction. The argument is pure ZFSet library facts: mem_singleton and notMem_empty, with a single rewrite.
why it matters
In the Recognition Science foundation stack, the first act of recognition is a bare distinction. This lemma supplies that distinction inside full ZFC: ∅ versus {∅} as von Neumann 0 and 1, differing by a genuine membership. It is consumed by zfWitness_injective, which maps Boolean tokens to these two sets and needs injectivity (the unequal case is discharged by absurdity against this theorem). It is also a direct conjunct of full_zfc_realizes_delta, the packaged claim that Mathlib ZFSet satisfies extensionality, has ∅ ≠ {∅}, discriminates by extensional difference, models infinity, and realizes the δ core via a PRC embedding. Without this elementary inequality the ZFC parse cannot certify that the recognition dichotomy is realized by actual sets rather than by a syntactic label.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.