Analysis I, Chapter 3 epilogue: Connections with ZFSet

In this epilogue we show that the ZFSet.{u} : Type (u + 1)ZFSet type in Mathlib (derived as a quotient from the PSet.{u} : Type (u + 1)PSet type) can be used to create models of the `SetTheory' class studied in this chapter, so long as we work in a universe of level at least 1. The constructions here are due to Edward van de Meent; see https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Can.20this.20proof.20related.20to.20Set.20replacement.20be.20shorter.3F/near/527305173

universe u lemma PSet.mem_ofNat_iff (n m : ℕ) : ofNat n ∈ ofNat m ↔ n < m := byn:ℕm:ℕ⊢ ofNat n ∈ ofNat m ↔ n < m refine ⟨ ?_, ofNat_mem_ofNat_of_lt m n ⟩n:ℕm:ℕ⊢ ofNat n ∈ ofNat m → n < m contrapose!n:ℕm:ℕ⊢ m ≤ n → ofNat n ∉ ofNat m; rw [le_iff_lt_or_eq]n:ℕm:ℕ⊢ m < n ∨ m = n → ofNat n ∉ ofNat m; rintro (h|rfl)inln:ℕm:ℕh:m < n⊢ ofNat n ∉ ofNat minrm:ℕ⊢ ofNat m ∉ ofNat m ·inln:ℕm:ℕh:m < n⊢ ofNat n ∉ ofNat m exact mem_asymm (ofNat_mem_ofNat_of_lt _ _ h)All goals completed! 🐙 apply mem_irreflAll goals completed! 🐙 open PSet in /-- Using the above lemmas, we can create a bijection between `ZFSet.omega` and the natural numbers. -/ noncomputable def ZFSet.nat_equiv : ℕ ≃ omega.{u} := Equiv.ofBijective (fun n => ⟨mk (ofNat.{u} n),mk_mem_iff.mpr (Mem.mk _ (ULift.up n))⟩) (by⊢ Function.Bijective fun n => ⟨mk (ofNat n), ⋯⟩ constructorleft⊢ Function.Injective fun n => ⟨mk (ofNat n), ⋯⟩right⊢ Function.Surjective fun n => ⟨mk (ofNat n), ⋯⟩ ·left⊢ Function.Injective fun n => ⟨mk (ofNat n), ⋯⟩ intro _ _lefta₁✝:ℕa₂✝:ℕ⊢ (fun n => ⟨mk (ofNat n), ⋯⟩) a₁✝ = (fun n => ⟨mk (ofNat n), ⋯⟩) a₂✝ → a₁✝ = a₂✝; simp [eq]lefta₁✝:ℕa₂✝:ℕ⊢ (ofNat a₁✝).Equiv (ofNat a₂✝) → a₁✝ = a₂✝; apply eq_of_ofNat_equiv_ofNatAll goals completed! 🐙 ·right⊢ Function.Surjective fun n => ⟨mk (ofNat n), ⋯⟩ intro ⟨x,hx⟩rightx:ZFSet.{u}hx:x ∈ omega⊢ ∃ a, (fun n => ⟨mk (ofNat n), ⋯⟩) a = ⟨x, hx⟩; rw [←mk_out x, omega, mk_mem_iff] at hxrightx:ZFSet.{u}hx✝:x ∈ omegahx:Quotient.out x ∈ PSet.omega⊢ ∃ a, (fun n => ⟨mk (ofNat n), ⋯⟩) a = ⟨x, hx✝⟩; obtain ⟨n,hn⟩ := hxright.introx:ZFSet.{u}hx:x ∈ omegan:PSet.omega.Typehn:(Quotient.out x).Equiv (PSet.omega.Func n)⊢ ∃ a, (fun n => ⟨mk (ofNat n), ⋯⟩) a = ⟨x, hx⟩ simp [mk_func, PSet.omega] at *right.introx:ZFSet.{u}hx:x ∈ omegan:PSet.omega.Typehn:(Quotient.out x).Equiv (ofNat n.down)⊢ ∃ a, mk (ofNat a) = x; use n.downhx:ZFSet.{u}hx:x ∈ omegan:PSet.omega.Typehn:(Quotient.out x).Equiv (ofNat n.down)⊢ mk (ofNat n.down) = x; rw [←mk_out x, eq]hx:ZFSet.{u}hx:x ∈ omegan:PSet.omega.Typehn:(Quotient.out x).Equiv (ofNat n.down)⊢ (ofNat n.down).Equiv (Quotient.out x); exact hn.symmAll goals completed! 🐙 )open Classical in /-- 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). -/ noncomputable instance ZFSet.inst_SetTheory : Chapter3.SetTheory.{u + 1,u + 1} where Set := ZFSet Object := ZFSet set_to_object := { toFun ⦃a₁⦄ := a₁, inj' _ _ h := h} mem o s := o ∈ s extensionality _ _ := ext emptyset := ∅ emptyset_mem := notMem_empty singleton x := {x} singleton_axiom _ _ := mem_singleton union_pair x y := x ∪ y union_pair_axiom _ _ _ := mem_union specify A P := ZFSet.sep (fun s ↦ (h : s ∈ A) → P ⟨s,h⟩) A specification_axiom := by⊢ ∀ (A : ZFSet.{u}) (P : { x // x ∈ A } → Prop), (∀ x ∈ ZFSet.sep (fun s => ∀ (h : s ∈ A), P ⟨s, h⟩) A, x ∈ A) ∧ ∀ (x : { x // x ∈ A }), ↑x ∈ ZFSet.sep (fun s => ∀ (h : s ∈ A), P ⟨s, h⟩) A ↔ P x simp +contextualAll goals completed! 🐙 replace A P hp := @(A.sep (fun s ↦ (hs : s ∈ A) → ∃ z, P ⟨s,hs⟩ z)).image (fun s ↦ if h : ∃ (hs : s ∈ A), ∃ z, P ⟨s,hs⟩ z then h.choose_spec.choose else ∅) (allZFSetDefinable _) replacement_axiom A P hp s := byA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}⊢ s ∈ image (fun s => if h : ∃ (hs : s ∈ A), ∃ z, P ⟨s, hs⟩ z then ⋯.choose else ∅) (ZFSet.sep (fun s => ∀ (hs : s ∈ A), ∃ z, P ⟨s, hs⟩ z) A) ↔ ∃ x, P x s simpA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}⊢ (∃ z, (z ∈ A ∧ ∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1) ∧ (if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) = s) ↔ ∃ a, ∃ (b : a ∈ A), P ⟨a, b⟩ s; constructormpA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}⊢ (∃ z, (z ∈ A ∧ ∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1) ∧ (if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) = s) → ∃ a, ∃ (b : a ∈ A), P ⟨a, b⟩ smprA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}⊢ (∃ a, ∃ (b : a ∈ A), P ⟨a, b⟩ s) → ∃ z, (z ∈ A ∧ ∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1) ∧ (if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) = s ·mpA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}⊢ (∃ z, (z ∈ A ∧ ∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1) ∧ (if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) = s) → ∃ a, ∃ (b : a ∈ A), P ⟨a, b⟩ s intro ⟨z, ⟨hzA, hz⟩, hz'⟩mpA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}z:ZFSet.{u}hzA:z ∈ Ahz:∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1hz':(if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) = s⊢ ∃ a, ∃ (b : a ∈ A), P ⟨a, b⟩ s; use z, hzAhA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}z:ZFSet.{u}hzA:z ∈ Ahz:∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1hz':(if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) = s⊢ P ⟨z, hzA⟩ s; simp [hzA, hz hzA] at hz'hA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}z:ZFSet.{u}hzA:z ∈ Ahz:∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1hz':⋯.choose = s⊢ P ⟨z, hzA⟩ s simp [←hz', Exists.choose_spec]All goals completed! 🐙 ·mprA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}⊢ (∃ a, ∃ (b : a ∈ A), P ⟨a, b⟩ s) → ∃ z, (z ∈ A ∧ ∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1) ∧ (if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) = s intro ⟨z, hzA, hz'⟩mprA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}z:ZFSet.{u}hzA:z ∈ Ahz':P ⟨z, hzA⟩ s⊢ ∃ z, (z ∈ A ∧ ∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1) ∧ (if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) = s; use z, ⟨hzA, byA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}z:ZFSet.{u}hzA:z ∈ Ahz':P ⟨z, hzA⟩ s⊢ ∀ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 aesopAll goals completed! 🐙⟩ apply hp ⟨_, hzA⟩right.aA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}z:ZFSet.{u}hzA:z ∈ Ahz':P ⟨z, hzA⟩ s⊢ P ⟨z, hzA⟩ (if h : ∃ (hs : z ∈ A), ∃ z_1, P ⟨z, hs⟩ z_1 then ⋯.choose else ∅) ∧ P ⟨z, hzA⟩ s; rw [dif_pos ⟨hzA, ⟨_, hz'⟩⟩]right.aA:ZFSet.{u}P:{ x // x ∈ A } → ZFSet.{u} → Prophp:∀ (x : { x // x ∈ A }) (y y' : ZFSet.{u}), P x y ∧ P x y' → y = y's:ZFSet.{u}z:ZFSet.{u}hzA:z ∈ Ahz':P ⟨z, hzA⟩ s⊢ P ⟨z, hzA⟩ ⋯.choose ∧ P ⟨z, hzA⟩ s; use Exists.choose_spec _All goals completed! 🐙 nat := omega nat_equiv := nat_equiv regularity_axiom A := byA:ZFSet.{u}⊢ (∃ x, x ∈ A) → ∃ x ∈ A, ∀ (S : ZFSet.{u}), x = { toFun := fun ⦃a₁⦄ => a₁, inj' := ⋯ } S → ¬∃ y ∈ A, y ∈ S simpA:ZFSet.{u}⊢ ∀ x ∈ A, ∃ x ∈ A, ∀ x_1 ∈ A, x_1 ∉ x; intro x hxA:ZFSet.{u}x:ZFSet.{u}hx:x ∈ A⊢ ∃ x ∈ A, ∀ x_1 ∈ A, x_1 ∉ x; have ⟨y,hy,_⟩ := regularity A (byA:ZFSet.{u}x:ZFSet.{u}hx:x ∈ A⊢ A ≠ ∅ aesopAll goals completed! 🐙) use y, hyrightA:ZFSet.{u}x:ZFSet.{u}hx:x ∈ Ay:ZFSet.{u}hy:y ∈ Aright✝:A ∩ y = ∅⊢ ∀ x ∈ A, x ∉ y; intro z _ _rightA:ZFSet.{u}x:ZFSet.{u}hx:x ∈ Ay:ZFSet.{u}hy:y ∈ Aright✝:A ∩ y = ∅z:ZFSet.{u}a✝¹:z ∈ Aa✝:z ∈ y⊢ False; have : z ∈ A ∩ y := byA:ZFSet.{u}⊢ (∃ x, x ∈ A) → ∃ x ∈ A, ∀ (S : ZFSet.{u}), x = { toFun := fun ⦃a₁⦄ => a₁, inj' := ⋯ } S → ¬∃ y ∈ A, y ∈ S simpA:ZFSet.{u}x:ZFSet.{u}hx:x ∈ Ay:ZFSet.{u}hy:y ∈ Aright✝:A ∩ y = ∅z:ZFSet.{u}a✝¹:z ∈ Aa✝:z ∈ y⊢ z ∈ A ∧ z ∈ y; tautoAll goals completed! 🐙 aesopAll goals completed! 🐙 pow X Y := funs Y X function_to_object X Y := { toFun f := @map (fun s ↦ if h : s ∈ X then f ⟨s,h⟩ else ∅) (allZFSetDefinable _) X inj' x _ h := byX:ZFSet.{u}Y:ZFSet.{u}x:{ x // x ∈ X } → { x // x ∈ Y }x✝:{ x // x ∈ X } → { x // x ∈ Y }h:(fun f => map (fun s => if h : s ∈ X then ↑(f ⟨s, h⟩) else ∅) X) x = (fun f => map (fun s => if h : s ∈ X then ↑(f ⟨s, h⟩) else ∅) X) x✝⊢ x = x✝ ext ⟨s, hs⟩h.mk.a.aX:ZFSet.{u}Y:ZFSet.{u}x:{ x // x ∈ X } → { x // x ∈ Y }x✝:{ x // x ∈ X } → { x // x ∈ Y }h:(fun f => map (fun s => if h : s ∈ X then ↑(f ⟨s, h⟩) else ∅) X) x = (fun f => map (fun s => if h : s ∈ X then ↑(f ⟨s, h⟩) else ∅) X) x✝s:ZFSet.{u}hs:s ∈ Xz✝:ZFSet.{u}⊢ z✝ ∈ ↑(x ⟨s, hs⟩) ↔ z✝ ∈ ↑(x✝ ⟨s, hs⟩); simp_rw [ZFSet.ext_iff, mem_map] at hh.mk.a.aX:ZFSet.{u}Y:ZFSet.{u}x:{ x // x ∈ X } → { x // x ∈ Y }x✝:{ x // x ∈ X } → { x // x ∈ Y }s:ZFSet.{u}hs:s ∈ Xz✝:ZFSet.{u}h:∀ (z : ZFSet.{u}), (∃ z_1 ∈ X, z_1.pair (if h : z_1 ∈ X then ↑(x ⟨z_1, h⟩) else ∅) = z) ↔ ∃ z_1 ∈ X, z_1.pair (if h : z_1 ∈ X then ↑(x✝ ⟨z_1, h⟩) else ∅) = z⊢ z✝ ∈ ↑(x ⟨s, hs⟩) ↔ z✝ ∈ ↑(x✝ ⟨s, hs⟩) specialize h (s.pair (x ⟨_,hs⟩))h.mk.a.aX:ZFSet.{u}Y:ZFSet.{u}x:{ x // x ∈ X } → { x // x ∈ Y }x✝:{ x // x ∈ X } → { x // x ∈ Y }s:ZFSet.{u}hs:s ∈ Xz✝:ZFSet.{u}h:(∃ z ∈ X, z.pair (if h : z ∈ X then ↑(x ⟨z, h⟩) else ∅) = s.pair ↑(x ⟨s, hs⟩)) ↔ ∃ z ∈ X, z.pair (if h : z ∈ X then ↑(x✝ ⟨z, h⟩) else ∅) = s.pair ↑(x ⟨s, hs⟩)⊢ z✝ ∈ ↑(x ⟨s, hs⟩) ↔ z✝ ∈ ↑(x✝ ⟨s, hs⟩); aesopAll goals completed! 🐙} powerset_axiom X Y F := byX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}⊢ F ∈ Y.funs X ↔ ∃ f, { toFun := fun f => map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y, inj' := ⋯ } f = F simp [IsFunc]X:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}⊢ (F ⊆ Y.prod X ∧ ∀ z ∈ Y, ∃! w, z.pair w ∈ F) ↔ ∃ f, map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y = F; constructormpX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}⊢ (F ⊆ Y.prod X ∧ ∀ z ∈ Y, ∃! w, z.pair w ∈ F) → ∃ f, map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y = FmprX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}⊢ (∃ f, map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y = F) → F ⊆ Y.prod X ∧ ∀ z ∈ Y, ∃! w, z.pair w ∈ F ·mpX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}⊢ (F ⊆ Y.prod X ∧ ∀ z ∈ Y, ∃! w, z.pair w ∈ F) → ∃ f, map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y = F intro ⟨hsub,huniq⟩mpX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ F⊢ ∃ f, map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y = F use (fun x ↦ ⟨(huniq _ x.property).choose,(pair_mem_prod.mp (hsub (huniq _ x.property).choose_spec)).2⟩)hX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ F⊢ map (fun s => if h : s ∈ Y then ↑((fun x => ⟨⋯.choose, ⋯⟩) ⟨s, h⟩) else ∅) Y = F exth.aX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}⊢ z✝ ∈ map (fun s => if h : s ∈ Y then ↑⟨⋯.choose, ⋯⟩ else ∅) Y ↔ z✝ ∈ F; simph.aX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}⊢ (∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = z✝) ↔ z✝ ∈ F; constructorh.a.mpX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}⊢ (∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = z✝) → z✝ ∈ Fh.a.mprX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}⊢ z✝ ∈ F → ∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = z✝ ·h.a.mpX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}⊢ (∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = z✝) → z✝ ∈ F rintro ⟨y,hy,rfl⟩h.a.mp.intro.introX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fy:ZFSet.{u}hy:y ∈ Y⊢ y.pair (if h : y ∈ Y then ⋯.choose else ∅) ∈ F; simp_all [(huniq _ hy).choose_spec]All goals completed! 🐙 ·h.a.mprX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}⊢ z✝ ∈ F → ∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = z✝ intro hfh.a.mprX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}hsub:F ⊆ Y.prod Xhuniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}hf:z✝ ∈ F⊢ ∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = z✝; specialize hsub hfh.a.mprX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}huniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}hf:z✝ ∈ Fhsub:z✝ ∈ Y.prod X⊢ ∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = z✝; rw [mem_prod] at hsubh.a.mprX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}huniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fz✝:ZFSet.{u}hf:z✝ ∈ Fhsub:∃ a ∈ Y, ∃ b ∈ X, z✝ = a.pair b⊢ ∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = z✝; obtain ⟨y,hy,x,_,rfl⟩ := hsubh.a.mpr.intro.intro.intro.introX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}huniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fy:ZFSet.{u}hy:y ∈ Yx:ZFSet.{u}left✝:x ∈ Xhf:y.pair x ∈ F⊢ ∃ z ∈ Y, z.pair (if h : z ∈ Y then ⋯.choose else ∅) = y.pair x use y,hyrightX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}huniq:∀ z ∈ Y, ∃! w, z.pair w ∈ Fy:ZFSet.{u}hy:y ∈ Yx:ZFSet.{u}left✝:x ∈ Xhf:y.pair x ∈ F⊢ y.pair (if h : y ∈ Y then ⋯.choose else ∅) = y.pair x; simp_all [←(huniq _ hy).choose_eq hf]All goals completed! 🐙 ·mprX:ZFSet.{u}Y:ZFSet.{u}F:ZFSet.{u}⊢ (∃ f, map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y = F) → F ⊆ Y.prod X ∧ ∀ z ∈ Y, ∃! w, z.pair w ∈ F rintro ⟨f,rfl⟩mpr.introX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }⊢ map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y ⊆ Y.prod X ∧ ∀ z ∈ Y, ∃! w, z.pair w ∈ map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y; simpmpr.introX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }⊢ map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y ⊆ Y.prod X ∧ ∀ z ∈ Y, ∃! w, z ∈ Y ∧ (if h : z ∈ Y then ↑(f ⟨z, h⟩) else ∅) = w; constructormpr.intro.leftX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }⊢ map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y ⊆ Y.prod Xmpr.intro.rightX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }⊢ ∀ z ∈ Y, ∃! w, z ∈ Y ∧ (if h : z ∈ Y then ↑(f ⟨z, h⟩) else ∅) = w <;>mpr.intro.leftX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }⊢ map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y ⊆ Y.prod Xmpr.intro.rightX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }⊢ ∀ z ∈ Y, ∃! w, z ∈ Y ∧ (if h : z ∈ Y then ↑(f ⟨z, h⟩) else ∅) = w intro _ _mpr.intro.rightX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }z✝:ZFSet.{u}a✝:z✝ ∈ Y⊢ ∃! w, z✝ ∈ Y ∧ (if h : z✝ ∈ Y then ↑(f ⟨z✝, h⟩) else ∅) = w <;>mpr.intro.leftX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }z✝:ZFSet.{u}a✝:z✝ ∈ map (fun s => if h : s ∈ Y then ↑(f ⟨s, h⟩) else ∅) Y⊢ z✝ ∈ Y.prod Xmpr.intro.rightX:ZFSet.{u}Y:ZFSet.{u}f:{ x // x ∈ Y } → { x // x ∈ X }z✝:ZFSet.{u}a✝:z✝ ∈ Y⊢ ∃! w, z✝ ∈ Y ∧ (if h : z✝ ∈ Y then ↑(f ⟨z✝, h⟩) else ∅) = w aesopAll goals completed! 🐙 union := sUnion union_axiom _ _ := byx✝¹:ZFSet.{u}x✝:ZFSet.{u}⊢ x✝ ∈ ⋃₀ x✝¹ ↔ ∃ S, x✝ ∈ S ∧ { toFun := fun ⦃a₁⦄ => a₁, inj' := ⋯ } S ∈ x✝¹ simp [And.comm]All goals completed! 🐙