omega_ne_empty
plain-language theorem explainer
The von Neumann ordinal ω is not the empty set in the pinned ZF universe ZFSet.{0}. Anyone wiring a FormalSystem witness that claims an infinite carrier cites this to guarantee the infinity axiom is realized by a genuinely nonempty infinite set. The proof is a short membership contradiction: 0 ∈ ω, so if ω = ∅ then ∅ ∈ ∅, which is impossible.
Claim. In the ZF universe at universe level $0$, the von Neumann infinite set $\omega$ is unequal to the empty set: $\omega \neq \emptyset$.
background
This module builds a Type-0 parse of ZF set theory as a FormalSystem for the Primitive Recognition Calculus. The carrier is pinned by the abbreviation ZF := ZFSet.{0}, so the FormalSystem interface (which lives in Type) can talk about genuine ZF sets without climbing universes.
Mathlib supplies ZFSet.omega as the least inductive set (von Neumann naturals) and the standard facts ZFSet.omega_zero (∅ ∈ ω) and ZFSet.notMem_empty (nothing is a member of ∅). Sibling lemmas already separate ∅ from {∅}; this lemma separates ∅ from the infinite set itself.
Local goal: show the ZF carrier is not a finite toy. Distinguishing ω from ∅ is the minimal certificate that the infinity axiom is modeled by a set that is actually infinite and nonempty.
proof idea
Assume for contradiction that ω = ∅. From ZFSet.omega_zero one has ∅ ∈ ω. Rewrite the membership along the assumed equality to obtain ∅ ∈ ∅. Discharge with ZFSet.notMem_empty applied to ∅. Pure membership contradiction; no induction or recursive construction.
why it matters
In the PRC/ZFC parse stack, a FormalSystem must exhibit genuine distinctions, not a collapsed carrier. This theorem is the infinity half of that check: the carrier contains an infinite set distinct from empty, so the infinity axiom is not vacuously named. It sits beside empty_ne_singleton and empty_distinct_singleton_extensionally (von Neumann 0 ≠ 1) and feeds the later zfWitness / zfSystem_expressive development that embeds a token dichotomy into ZF.
No downstream used_by edges are recorded yet; the lemma is infrastructure for the expressive FormalSystem witness rather than a physics forcing step (T5–T8). It closes the obvious referee objection that "ω" might have been an alias for ∅ in a degenerate model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.