See https://leanprover.zulipchat.com/#narrow/channel/514017-Analysis-I/topic/.E2.9C.94.20Is.20Exercise.203.2E4.2E6.20.28ii.29.20missing.3F/near/531046257

powerset.lean

import Analysis.Section_3_4

namespace Chapter3

variable [SetTheory]

open SetTheory
open SetTheory.Set

---

def pair_set (x y : Object) : Set := {(({x}: Set): Object), (({x, y}: Set): Object)}
def pair (x y : Object) : Object := pair_set x y

lemma pair_aux1 : ∀ {x}, ({x, x}: Set) = {x} := by
  intro x
  apply ext
  aesop

lemma pair_aux2 : ∀ {x y}, ({x}: Set) = {y} → x = y := by
  intro x y h
  rw [ext_iff] at h
  aesop

lemma pair_aux3 : ∀ {x y z}, ({x}: Set) = {y, z} → x = y ∧ x = z := by
  intro x y z h
  rw [ext_iff] at h
  have : x ∈ ({y, z}: Set) := by specialize h x; aesop
  have : y ∈ ({x}: Set) := by specialize h y; aesop
  have : z ∈ ({x}: Set) := by specialize h z; aesop
  aesop

lemma pair_aux4 : ∀ {x y z w}, ({x, y}: Set) = {z, w} → (x = z ∧ y = w) ∨ (x = w ∧ y = z) := by
  intro x y z w h
  rw [ext_iff] at h
  simp only [mem_pair] at h
  have h1 : x = z ∨ x = w := by apply (h x).mp; left; rfl
  have h2 : y = z ∨ y = w := by apply (h y).mp; right; rfl
  have := h w
  have := h z
  grind

lemma pair_aux5 : ∀ {x y z w}, (x ≠ y) →
    ({(({x}: Set): Object), (({x, y}: Set): Object)}: Set) = ({(({z}: Set): Object), (({z, w}: Set): Object)}: Set) →
    ({x}: Set) = {z} ∧ ({x, y}: Set) = {z, w} := by
  intro x y z w _ h
  apply pair_aux4 at h
  have : ({x, y}: Set) ≠ {z} := by
    intro h
    rw [ext_iff] at h
    have : x ∈ ({z}: Set) := by specialize h x; aesop
    aesop
  aesop

lemma pair_injective : ∀ {x1 y1 x2 y2}, pair x1 y1 = pair x2 y2 → x1 = x2 ∧ y1 = y2 := by
  intro x1 y1 x2 y2 h
  unfold pair at h
  constructor
  · contrapose! h
    intro hs
    simp only [EmbeddingLike.apply_eq_iff_eq] at hs
    unfold pair_set at hs
    rw [ext_iff] at hs
    specialize hs ({x1}: Set)
    simp only [ne_eq, mem_pair, EmbeddingLike.apply_eq_iff_eq, true_or, true_iff] at hs
    rcases hs with (hx | hx)
    · rw [ext_iff] at hx
      simp_all
    rw [ext_iff] at hx
    specialize hx x2
    simp_all
  contrapose! h
  intro hs
  simp only [EmbeddingLike.apply_eq_iff_eq] at hs
  unfold pair_set at hs
  by_cases h1 : x1 = y1
  · subst h1
    simp only [pair_aux1] at hs
    have ⟨h2, h3⟩ := pair_aux3 hs
    simp only [EmbeddingLike.apply_eq_iff_eq] at h2 h3
    apply pair_aux2 at h2
    apply pair_aux3 at h3
    aesop
  apply pair_aux5 at hs
  obtain ⟨h2, h3⟩ := hs
  apply pair_aux2 at h2
  apply pair_aux4 at h3
  simp_all only [ne_eq, and_false, false_or, not_true_eq_false]
  exact h1

---

@[ext]
structure Graph (X Y : Set) where
  pairs : Set
  relation : ∀ p ∈ pairs, ∃ (x: X) (y: Y), p = pair x y
  defined : ∀ x : X, ∃ y : Y, pair x y ∈ pairs
  functional : ∀ {x : X} {y1 y2 : Y}, pair x y1 ∈ pairs → pair x y2 ∈ pairs → y1 = y2

lemma graph_eq (g1 g2 : Graph X Y) : g1.pairs = g2.pairs → g1 = g2 := by
  intro h
  ext
  exact h

noncomputable def Graph.value_at (g : Graph X Y) (x : X) : Y :=
  (g.defined x).choose

lemma Graph.value_at_spec (g : Graph X Y) (x : X) : pair x (g.value_at x) ∈ g.pairs :=
  (g.defined x).choose_spec

noncomputable def Graph.toFun (g : Graph X Y) : X → Y := fun x ↦
  g.value_at x

---

lemma pair_in_powerset {X Y : Set} (x : X) (y : Y) : pair x y ∈ (X ∪ Y).powerset.powerset := by
  rw [mem_powerset]
  use pair_set x y
  constructor
  · unfold pair
    rfl
  rw [subset_def]
  intro a ha
  unfold pair_set at ha
  rw [mem_pair] at ha
  simp only [mem_powerset, subset_def]
  rcases ha with (ha | ha)
  · use {x.val}, ha
    simp [x.prop, y.prop]
  use {x.val, y.val}, ha
  simp [x.prop, y.prop]

def AllPairs (X Y : Set) : Set :=
  (X ∪ Y).powerset.powerset.specify (fun p ↦ ∃ x ∈ X, ∃ y ∈ Y, p.val = pair x y)

theorem pair_in_AllPairs {X Y : Set} (x : X) (y : Y) : (pair x y : Object) ∈ AllPairs X Y := by
  unfold AllPairs
  rw [specification_axiom'']
  simp only [exists_prop]
  constructor
  · apply pair_in_powerset
  use x, x.prop, y, y.prop

---

noncomputable def funGraph {X Y : Set} (f : X → Y) : Graph X Y where
  pairs := (AllPairs X Y).specify (fun p ↦ ∃ x : X, p = pair x (f x))
  relation := by
    intro p hp
    rw [specification_axiom''] at hp
    obtain ⟨_, ⟨x, _⟩⟩ := hp
    use x, (f x)
  defined := by
    intro x
    use (f x)
    rw [specification_axiom'']
    constructor
    · use x
    apply pair_in_AllPairs
  functional := by
    intro x y1 y2 hy1 hy2
    rw [specification_axiom''] at hy1
    rw [specification_axiom''] at hy2
    obtain ⟨hp1, ⟨x1, h1⟩⟩ := hy1
    obtain ⟨hp2, ⟨x2, h2⟩⟩ := hy2
    apply pair_injective at h1
    apply pair_injective at h2
    aesop

theorem funGraph_eval (X Y : Set) (f : X → Y) (x : X) : (funGraph f).value_at x = f x := by
  set G := funGraph f
  apply G.functional
  · apply G.value_at_spec
  simp only [G, funGraph]
  rw [specification_axiom'']
  constructor
  · use x
  apply pair_in_AllPairs

theorem funGraph_toFun {X Y : Set} (f: X → Y) : f = (funGraph f).toFun := by
  ext x
  simp [Graph.toFun, funGraph_eval]

---

noncomputable def AllGraphs (X Y: Set) : Set :=
  (AllPairs X Y).powerset.specify (fun G ↦ ∃ g : Graph X Y, g.pairs = G.val)

lemma AllGraphs_spec {X Y : Set} : ∀ G, G ∈ (AllGraphs X Y) ↔ ∃ (g: Graph X Y), g.pairs = G := by
  intro G
  unfold AllGraphs
  simp only [specification_axiom'', exists_prop, and_iff_right_iff_imp,
    forall_exists_index, mem_powerset, subset_def]
  intro g hg
  use g.pairs, hg.symm
  intro p hp
  obtain ⟨x, ⟨y, rfl⟩⟩ := g.relation p hp
  apply pair_in_AllPairs

noncomputable def asGraph {X Y : Set} (G : AllGraphs X Y) : Graph X Y :=
  ((AllGraphs_spec G.val).mp G.prop).choose

noncomputable def asGraph_spec {X Y : Set} (G : AllGraphs X Y) : (asGraph G).pairs = G.val :=
  ((AllGraphs_spec G.val).mp G.prop).choose_spec

lemma asGraph_funGraph_pairs_toFun {X Y : Set} (f : X → Y) (G: AllGraphs X Y) (h : G.val = (funGraph f).pairs) :
    f = (asGraph G).toFun := by
  have hg := asGraph_spec G
  simp_all only [EmbeddingLike.apply_eq_iff_eq]
  apply graph_eq at hg
  rw [hg]
  apply funGraph_toFun

---

noncomputable def AllFuns (X Y: Set) : Set :=
  (AllGraphs X Y).replace (P := fun G F ↦ F = (asGraph G).toFun) (by simp)

lemma AllFuns_spec (X Y : Set) : ∀ F, F ∈ (AllFuns X Y) ↔ ∃ (f: X → Y), f = F := by
  intro F
  unfold AllFuns
  simp only [Set.replacement_axiom, Subtype.exists]
  constructor
  · rintro ⟨G, ⟨hG, rfl⟩⟩
    use (asGraph ⟨G, hG⟩).toFun
  rintro ⟨f, rfl⟩
  use (funGraph f).pairs
  use (AllGraphs_spec _).mpr (by tauto)
  congr
  apply asGraph_funGraph_pairs_toFun
  rfl

open Classical in
theorem SetTheory.Set.powerset_axiom' {X Y:Set} : ∃ Z:Set,
  ∀ F:Object, F ∈ Z ↔ ∃ f: Y → X, f = F := by
  use AllFuns Y X
  intro F
  constructor
  · intro hF
    apply (AllFuns_spec _ _ _).mp hF
  rintro ⟨f, rfl⟩
  apply (AllFuns_spec _ _ _).mpr
  use f