empty_distinct_singleton_extensionally
plain-language theorem explainer
In the ZF universe, the empty set and its singleton are extensionally distinct: there exists a witness (namely ∅ itself) that belongs to one but not the other. Anyone building the FormalSystem expressivity check for full ZFC cites this. The proof is a three-line term argument: take ∅ as witness and discharge the biconditional via the standard membership lemmas.
Claim. There exists a set $z$ in the ZF universe such that it is not the case that $z \in \emptyset$ if and only if $z \in \{\emptyset\}$. Equivalently, $\emptyset$ and $\{\emptyset\}$ differ extensionally by the member $\emptyset$.
background
The module parses full ZFC as a FormalSystem for the Primitive Recognition Calculus, contrasting it with hereditarily finite (HF) set theory. Here ZF is the Mathlib ZFSet universe pinned at level 0, so the FormalSystem interface stays in Type 0.
Extensional equality of sets is membership agreement: $A = B$ iff $\forall z., z\in A \leftrightarrow z\in B$. The empty set $\emptyset$ has no members; the singleton ${\emptyset}$ has exactly one. Their difference is the classical von Neumann $0$ versus $1$. The sibling fact that $\emptyset \neq {\emptyset}$ is the non-extensional surface form; this theorem packages the same gap as an existential witness suitable for the Expressive predicate on formal systems.
Upstream, the module imports Mathlib ZFC basics (membership, singleton, empty-set lemmas) and the PRC distinction dichotomy that frames when a system can separate endpoints.
proof idea
Term-mode proof. Instantiate the existential with witness $z = \emptyset$. Assume for contradiction the biconditional $\emptyset \in \emptyset \leftrightarrow \emptyset \in {\emptyset}$. The right-to-left direction plus ZFSet.mem_singleton (with rfl) yields $\emptyset \in \emptyset$. That contradicts ZFSet.notMem_empty. No induction or choice; pure membership algebra.
why it matters
Feeds directly into zfSystem_expressive, whose doc-comment states: "zfSystem distinguishes its endpoints: the genuine ∅ and {∅} differ extensionally." That theorem is a one-line wrapper around this result, discharging the Expressive clause of the FormalSystem interface for full ZFC.
In the PRC stack this is the set-theoretic counterpart of a genuine distinction: HF could not model infinity or the successor chain past finite ranks, while ZFC supplies $\omega$ and the empty/singleton split as the base of the von Neumann hierarchy. The next sibling, infinity_modeled, records that $\omega$ contains $\emptyset$ and is closed under $x \mapsto x \cup {x}$. Together they show the ZFC parse is expressive enough to embed the $\delta$-core of recognition distinctions, closing the gap HF left open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.