theorem PSet.ofNat_mem_ofNat_of_lt (m n : ℕ) : n < m → ofNat n ∈ ofNat m

A preliminary lemma about PSet: their natural numbers are ordered by membership.

theorem PSet.mem_ofNat_iff (n m : ℕ) : ofNat n ∈ ofNat m ↔ n < m

theorem PSet.eq_of_ofNat_equiv_ofNat (n m : ℕ) : (ofNat n).Equiv (ofNat m) → n = m

Another preliminary lemma: Natural numbers in PSet can only be equivalent if they are equal.

noncomputable def ZFSet.nat_equiv : ℕ ≃ ↥omega

Using the above lemmas, we can create a bijection between ZFSet.omega and the natural numbers.

Equations

• ZFSet.nat_equiv = Equiv.ofBijective (fun (n : ℕ) => ⟨ZFSet.mk (PSet.ofNat n), ⋯⟩) ZFSet.nat_equiv._proof_2

@[implicit_reducible]

noncomputable instance ZFSet.inst_SetTheory : Chapter3.SetTheory

Show that ZFSet obeys the Chapter3.SetTheory axioms. Most of these axioms were essentially already established in Mathlib and are relatively routine to transfer over; the equivalence of ZF.omega and Nat being the trickiest one in content (and the power set axiom also requiring some technical manipulation).

Equations

• One or more equations did not get rendered due to their size.