[GOAL]
x : PSet
y : PSet
inst✝¹ : IsEmpty (Type x)
inst✝ : IsEmpty (Type y)
⊢ (∀ (i : Type x), ∃ j, Equiv (Func x i) (Func y j)) ∧ ∀ (j : Type y), ∃ i, Equiv (Func x i) (Func y j)
[PROOFSTEP]
simp
[GOAL]
x y z : PSet
hxy : x ⊆ y
hyz : y ⊆ z
a : Type x
⊢ ∃ b, Equiv (Func x a) (Func z b)
[PROOFSTEP]
cases' hxy a with b hb
[GOAL]
case intro
x y z : PSet
hxy : x ⊆ y
hyz : y ⊆ z
a : Type x
b : Type y
hb : Equiv (Func x a) (Func y b)
⊢ ∃ b, Equiv (Func x a) (Func z b)
[PROOFSTEP]
cases' hyz b with c hc
[GOAL]
case intro.intro
x y z : PSet
hxy : x ⊆ y
hyz : y ⊆ z
a : Type x
b : Type y
hb : Equiv (Func x a) (Func y b)
c : Type z
hc : Equiv (Func y b) (Func z c)
⊢ ∃ b, Equiv (Func x a) (Func z b)
[PROOFSTEP]
exact ⟨c, hb.trans hc⟩
[GOAL]
x : PSet
i : Type x
⊢ Func x i ∈ x
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ : Type u_1
A✝ : α✝ → PSet
i : Type (mk α✝ A✝)
⊢ Func (mk α✝ A✝) i ∈ mk α✝ A✝
[PROOFSTEP]
apply Mem.mk
[GOAL]
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
⊢ ∀ (y : PSet), y ∈ mk β B → Acc (fun x x_1 => x ∈ x_1) y
[PROOFSTEP]
rintro ⟨γ, C⟩ ⟨b, hc⟩
[GOAL]
case mk.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
[PROOFSTEP]
cases' H.exists_right b with a ha
[GOAL]
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
[PROOFSTEP]
have H := ha.trans hc.symm
[GOAL]
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H✝ : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
H : Equiv (Func (mk α A) a) (mk γ C)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
[PROOFSTEP]
rw [mk_func] at H 
[GOAL]
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H✝ : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
H : Equiv (A a) (mk γ C)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
[PROOFSTEP]
exact mem_wf_aux H
[GOAL]
⊢ toSet ∅ = ∅
[PROOFSTEP]
simp [toSet]
[GOAL]
⊢ ¬PSet.Nonempty ∅
[PROOFSTEP]
simp [PSet.Nonempty]
[GOAL]
α : Type u
A : α → PSet
y : PSet
x✝ : y ∈ ⋃₀ mk α A
a : Type (mk α A)
c : Type (Func (mk α A) a)
e : Equiv y (Func (A a) c)
this : Func (A a) c ∈ mk (Type (A a)) (Func (A a))
⊢ Func (A a) c ∈ A (?m.26421 α A y x✝ a c e this)
[PROOFSTEP]
rwa [eta] at this 
[GOAL]
α : Type u
A : α → PSet
y : PSet
x✝ : ∃ z, z ∈ mk α A ∧ y ∈ z
β : Type u
B : β → PSet
a : Type (mk α A)
e : Equiv (mk β B) (A a)
b : Type (mk β B)
yb : Equiv y (Func (mk β B) b)
⊢ y ∈ ⋃₀ mk α A
[PROOFSTEP]
rw [← eta (A a)] at e 
[GOAL]
α : Type u
A : α → PSet
y : PSet
x✝ : ∃ z, z ∈ mk α A ∧ y ∈ z
β : Type u
B : β → PSet
a : Type (mk α A)
e : Equiv (mk β B) (mk (Type (A a)) (Func (A a)))
b : Type (mk β B)
yb : Equiv y (Func (mk β B) b)
⊢ y ∈ ⋃₀ mk α A
[PROOFSTEP]
exact
  let ⟨βt, _⟩ := e
  let ⟨c, bc⟩ := βt b
  ⟨⟨a, c⟩, yb.trans bc⟩
[GOAL]
x : PSet
⊢ toSet (⋃₀ x) = ⋃₀ (toSet '' toSet x)
[PROOFSTEP]
ext
[GOAL]
case h
x x✝ : PSet
⊢ x✝ ∈ toSet (⋃₀ x) ↔ x✝ ∈ ⋃₀ (toSet '' toSet x)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
F : Arity ZFSet (n + 1)
⊢ Definable (n + 1) F
[PROOFSTEP]
have I := fun x => allDefinable (F x)
[GOAL]
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
⊢ Definable (n + 1) F
[PROOFSTEP]
refine' @Definable.EqMk (n + 1) ⟨fun x : PSet => (@Definable.Resp _ _ (I ⟦x⟧)).1, _⟩ _ _
[GOAL]
case refine'_1
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
⊢ Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
    ↑(Definable.Resp (F (Quotient.mk setoid x)))
[PROOFSTEP]
dsimp [Arity.Equiv]
[GOAL]
case refine'_1
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
⊢ ∀ (x y : PSet),
    PSet.Equiv x y →
      Arity.Equiv ↑(Definable.Resp (F (Quotient.mk setoid x))) ↑(Definable.Resp (F (Quotient.mk setoid y)))
[PROOFSTEP]
intro x y h
[GOAL]
case refine'_1
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
x y : PSet
h : PSet.Equiv x y
⊢ Arity.Equiv ↑(Definable.Resp (F (Quotient.mk setoid x))) ↑(Definable.Resp (F (Quotient.mk setoid y)))
[PROOFSTEP]
rw [@Quotient.sound PSet _ _ _ h]
[GOAL]
case refine'_1
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
x y : PSet
h : PSet.Equiv x y
⊢ Arity.Equiv ↑(Definable.Resp (F (Quotient.mk setoid y))) ↑(Definable.Resp (F (Quotient.mk setoid y)))
[PROOFSTEP]
exact (Definable.Resp (F ⟦y⟧)).2
[GOAL]
case refine'_2
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
⊢ Resp.eval (n + 1)
      { val := fun x => ↑(Definable.Resp (F (Quotient.mk setoid x))),
        property :=
          (_ :
            Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
              ↑(Definable.Resp (F (Quotient.mk setoid x)))) } =
    F
[PROOFSTEP]
refine' funext fun q => Quotient.inductionOn q fun x => _
[GOAL]
case refine'_2
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
q : ZFSet
x : PSet
⊢ Resp.eval (n + 1)
      { val := fun x => ↑(Definable.Resp (F (Quotient.mk setoid x))),
        property :=
          (_ :
            Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
              ↑(Definable.Resp (F (Quotient.mk setoid x)))) }
      (Quotient.mk setoid x) =
    F (Quotient.mk setoid x)
[PROOFSTEP]
simp_rw [Resp.eval_val, Resp.f]
[GOAL]
case refine'_2
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
q : ZFSet
x : PSet
⊢ Resp.eval n
      { val := ↑(Definable.Resp (F (Quotient.mk setoid x))),
        property :=
          (_ :
            Arity.Equiv
              (↑{ val := fun x => ↑(Definable.Resp (F (Quotient.mk setoid x))),
                    property :=
                      (_ :
                        Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
                          ↑(Definable.Resp (F (Quotient.mk setoid x)))) }
                x)
              (↑{ val := fun x => ↑(Definable.Resp (F (Quotient.mk setoid x))),
                    property :=
                      (_ :
                        Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
                          ↑(Definable.Resp (F (Quotient.mk setoid x)))) }
                x)) } =
    F (Quotient.mk setoid x)
[PROOFSTEP]
exact @Definable.eq _ (F ⟦x⟧) (I ⟦x⟧)
[GOAL]
x : ZFSet
a : PSet
⊢ Small.{u, u + 1} ↑(toSet (Quotient.mk setoid a))
[PROOFSTEP]
let f : a.Type → (mk a).toSet := fun i => ⟨mk <| a.Func i, func_mem a i⟩
[GOAL]
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
⊢ Small.{u, u + 1} ↑(toSet (Quotient.mk setoid a))
[PROOFSTEP]
suffices Function.Surjective f by exact small_of_surjective this
[GOAL]
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
this : Function.Surjective f
⊢ Small.{u, u + 1} ↑(toSet (Quotient.mk setoid a))
[PROOFSTEP]
exact small_of_surjective this
[GOAL]
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
⊢ Function.Surjective f
[PROOFSTEP]
rintro ⟨y, hb⟩
[GOAL]
case mk
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
y : ZFSet
hb : y ∈ toSet (mk a)
⊢ ∃ a_1, f a_1 = { val := y, property := hb }
[PROOFSTEP]
induction y using Quotient.inductionOn
[GOAL]
case mk.h
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
a✝ : PSet
hb : Quotient.mk setoid a✝ ∈ toSet (mk a)
⊢ ∃ a_1, f a_1 = { val := Quotient.mk setoid a✝, property := hb }
[PROOFSTEP]
cases' hb with i h
[GOAL]
case mk.h.intro
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
a✝ : PSet
i : Type a
h : PSet.Equiv a✝ (Func a i)
⊢ ∃ a_1, f a_1 = { val := Quotient.mk setoid a✝, property := (_ : ∃ b, PSet.Equiv a✝ (Func a b)) }
[PROOFSTEP]
exact ⟨i, Subtype.coe_injective (Quotient.sound h.symm)⟩
[GOAL]
x y : ZFSet
⊢ toSet x ⊆ toSet y ↔ x ⊆ y
[PROOFSTEP]
simp [subset_def, Set.subset_def]
[GOAL]
x y : ZFSet
h : x = y
⊢ ∀ (z : ZFSet), z ∈ x ↔ z ∈ y
[PROOFSTEP]
simp [h]
[GOAL]
⊢ toSet ∅ = ∅
[PROOFSTEP]
simp [toSet]
[GOAL]
⊢ ¬ZFSet.Nonempty ∅
[PROOFSTEP]
simp [ZFSet.Nonempty]
[GOAL]
x : PSet
⊢ ZFSet.Nonempty (mk x) ↔ PSet.Nonempty x
[PROOFSTEP]
refine' ⟨_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩
[GOAL]
x : PSet
⊢ ZFSet.Nonempty (mk x) → PSet.Nonempty x
[PROOFSTEP]
rintro ⟨a, h⟩
[GOAL]
case intro
x : PSet
a : ZFSet
h : a ∈ toSet (mk x)
⊢ PSet.Nonempty x
[PROOFSTEP]
induction a using Quotient.inductionOn
[GOAL]
case intro.h
x a✝ : PSet
h : Quotient.mk setoid a✝ ∈ toSet (mk x)
⊢ PSet.Nonempty x
[PROOFSTEP]
exact ⟨_, h⟩
[GOAL]
x : ZFSet
⊢ x = ∅ ↔ ∀ (y : ZFSet), ¬y ∈ x
[PROOFSTEP]
rw [ext_iff]
[GOAL]
x : ZFSet
⊢ (∀ (z : ZFSet), z ∈ x ↔ z ∈ ∅) ↔ ∀ (y : ZFSet), ¬y ∈ x
[PROOFSTEP]
simp
[GOAL]
u : ZFSet
⊢ u = ∅ ∨ ZFSet.Nonempty u
[PROOFSTEP]
rw [eq_empty, ← not_exists]
[GOAL]
u : ZFSet
⊢ (¬∃ x, x ∈ u) ∨ ZFSet.Nonempty u
[PROOFSTEP]
apply em'
[GOAL]
x y : ZFSet
⊢ toSet (insert x y) = insert x (toSet y)
[PROOFSTEP]
ext
[GOAL]
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (insert x y) ↔ x✝ ∈ insert x (toSet y)
[PROOFSTEP]
simp
[GOAL]
x : ZFSet
⊢ toSet {x} = {x}
[PROOFSTEP]
ext
[GOAL]
case h
x x✝ : ZFSet
⊢ x✝ ∈ toSet {x} ↔ x✝ ∈ {x}
[PROOFSTEP]
simp
[GOAL]
x y z : ZFSet
⊢ x ∈ {y, z} ↔ x = y ∨ x = z
[PROOFSTEP]
simp
[GOAL]
n✝ : ZFSet
x : PSet
x✝ : Quotient.mk setoid x ∈ omega
n : ℕ
h : PSet.Equiv x (Func PSet.omega { down := n })
⊢ insert (mk x) (mk x) = insert (mk (ofNat n)) (mk (ofNat n))
[PROOFSTEP]
rw [ZFSet.sound h]
[GOAL]
n✝ : ZFSet
x : PSet
x✝ : Quotient.mk setoid x ∈ omega
n : ℕ
h : PSet.Equiv x (Func PSet.omega { down := n })
⊢ insert (mk (Func PSet.omega { down := n })) (mk (Func PSet.omega { down := n })) =
    insert (mk (ofNat n)) (mk (ofNat n))
[PROOFSTEP]
rfl
[GOAL]
p : ZFSet → Prop
x✝³ x✝² : PSet
α : Type ?u.55373
A : α → PSet
β : Type ?u.55373
B : β → PSet
x✝¹ : PSet.Equiv (PSet.mk α A) (PSet.mk β B)
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
βα : ∀ (b : β), ∃ a, PSet.Equiv (A a) (B b)
x✝ : { a // (fun y => p (mk y)) (Func (PSet.mk α A) a) }
a : Type (PSet.mk α A)
pa : (fun y => p (mk y)) (Func (PSet.mk α A) a)
b : β
hb : PSet.Equiv (A a) (B b)
⊢ (fun y => p (mk y)) (Func (PSet.mk β B) b)
[PROOFSTEP]
simpa only [mk_func, ← ZFSet.sound hb]
[GOAL]
p : ZFSet → Prop
x✝³ x✝² : PSet
α : Type ?u.55373
A : α → PSet
β : Type ?u.55373
B : β → PSet
x✝¹ : PSet.Equiv (PSet.mk α A) (PSet.mk β B)
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
βα : ∀ (b : β), ∃ a, PSet.Equiv (A a) (B b)
x✝ : { a // (fun y => p (mk y)) (Func (PSet.mk β B) a) }
b : Type (PSet.mk β B)
pb : (fun y => p (mk y)) (Func (PSet.mk β B) b)
a : α
ha : PSet.Equiv (A a) (B b)
⊢ (fun y => p (mk y)) (Func (PSet.mk α A) a)
[PROOFSTEP]
simpa only [mk_func, ZFSet.sound ha]
[GOAL]
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ ZFSet.sep p (Quotient.mk setoid (PSet.mk α A))
a : Type (PSet.mk α A)
pa : (fun y => p (mk y)) (Func (PSet.mk α A) a)
h :
  PSet.Equiv y
    (Func
      ↑(Resp.f
          { val := PSet.sep fun y => p (mk y),
            property :=
              (_ :
                ∀ (x x_1 : PSet),
                  PSet.Equiv x x_1 → Arity.Equiv (PSet.sep (fun y => p (mk y)) x) (PSet.sep (fun y => p (mk y)) x_1)) }
          (PSet.mk α A))
      { val := a, property := pa })
⊢ p (Quotient.mk setoid y)
[PROOFSTEP]
rwa [@Quotient.sound PSet _ _ _ h]
[GOAL]
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ Quotient.mk setoid (PSet.mk α A) ∧ p (Quotient.mk setoid y)
a : Type (PSet.mk α A)
h : PSet.Equiv y (Func (PSet.mk α A) a)
pa : p (Quotient.mk setoid y)
⊢ (fun y => p (mk y)) (Func (PSet.mk α A) a)
[PROOFSTEP]
rw [mk_func] at h 
[GOAL]
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ Quotient.mk setoid (PSet.mk α A) ∧ p (Quotient.mk setoid y)
a : Type (PSet.mk α A)
h : PSet.Equiv y (A a)
pa : p (Quotient.mk setoid y)
⊢ p (mk (Func (PSet.mk α A) a))
[PROOFSTEP]
rwa [mk_func, ← ZFSet.sound h]
[GOAL]
a : ZFSet
p : ZFSet → Prop
⊢ toSet (ZFSet.sep p a) = {x | x ∈ toSet a ∧ p x}
[PROOFSTEP]
ext
[GOAL]
case h
a : ZFSet
p : ZFSet → Prop
x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep p a) ↔ x✝ ∈ {x | x ∈ toSet a ∧ p x}
[PROOFSTEP]
simp
[GOAL]
x y : ZFSet
x✝¹ x✝ : PSet
α : Type u
A : α → PSet
β : Type u
B : β → PSet
⊢ PSet.mk β B ∈ PSet.powerset (PSet.mk α A) ↔ Quotient.mk setoid (PSet.mk β B) ⊆ Quotient.mk setoid (PSet.mk α A)
[PROOFSTEP]
simp [mem_powerset, subset_iff]
[GOAL]
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
let ⟨b, hb⟩ := αβ a
[GOAL]
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
hb : PSet.Equiv (A a) (B b)
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
induction' ea : A a with γ Γ
[GOAL]
case mk
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
hb : PSet.Equiv (A a) (B b)
x✝ : PSet
ea✝ : A a = x✝
γ : Type u
Γ : γ → PSet
A_ih✝ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
induction' eb : B b with δ Δ
[GOAL]
case mk.mk
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
hb : PSet.Equiv (A a) (B b)
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
rw [ea, eb] at hb 
[GOAL]
case mk.mk
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
hb : PSet.Equiv (PSet.mk γ Γ) (PSet.mk δ Δ)
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
cases' hb with γδ δγ
[GOAL]
case mk.mk.intro
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
let c : (A a).Type := c
[GOAL]
case mk.mk.intro
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
let ⟨d, hd⟩ := γδ (by rwa [ea] at c )
[GOAL]
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
⊢ γ
[PROOFSTEP]
rwa [ea] at c 
[GOAL]
case mk.mk.intro
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
d : δ
hd : PSet.Equiv (Γ (Eq.mp (_ : Type (A a) = Type (PSet.mk γ Γ)) c)) (Δ d)
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
use⟨b, Eq.ndrec d (Eq.symm eb)⟩
[GOAL]
case h
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
d : δ
hd : PSet.Equiv (Γ (Eq.mp (_ : Type (A a) = Type (PSet.mk γ Γ)) c)) (Δ d)
⊢ PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ })
    (Func (⋃₀ PSet.mk β B) { fst := b, snd := (_ : PSet.mk δ Δ = Func (PSet.mk β B) b) ▸ d })
[PROOFSTEP]
change PSet.Equiv ((A a).Func c) ((B b).Func (Eq.ndrec d eb.symm))
[GOAL]
case h
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
d : δ
hd : PSet.Equiv (Γ (Eq.mp (_ : Type (A a) = Type (PSet.mk γ Γ)) c)) (Δ d)
⊢ PSet.Equiv (Func (A a) c) (Func (B b) ((_ : PSet.mk δ Δ = B b) ▸ d))
[PROOFSTEP]
match A a, B b, ea, eb, c, d, hd with
| _, _, rfl, rfl, _, _, hd => exact hd
[GOAL]
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝³ : PSet
ea✝ : A a = x✝³
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝² : PSet
eb✝ : B b = x✝²
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
d : δ
hd✝ : PSet.Equiv (Γ (Eq.mp (_ : Type (A a) = Type (PSet.mk γ Γ)) c)) (Δ d)
x✝¹ : Type (PSet.mk γ Γ)
x✝ : δ
hd : PSet.Equiv (Γ (Eq.mp (_ : Type (PSet.mk γ Γ) = Type (PSet.mk γ Γ)) x✝¹)) (Δ x✝)
⊢ PSet.Equiv (Func (PSet.mk γ Γ) x✝¹) (Func (PSet.mk δ Δ) ((_ : PSet.mk δ Δ = PSet.mk δ Δ) ▸ x✝))
[PROOFSTEP]
exact hd
[GOAL]
x : ZFSet
⊢ ZFSet
[PROOFSTEP]
classical exact if h : x.Nonempty then ZFSet.sep (fun y => ∀ z ∈ x, y ∈ z) h.some else ∅
[GOAL]
x : ZFSet
⊢ ZFSet
[PROOFSTEP]
exact if h : x.Nonempty then ZFSet.sep (fun y => ∀ z ∈ x, y ∈ z) h.some else ∅
[GOAL]
x y : ZFSet
h : ZFSet.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ (z : ZFSet), z ∈ x → y ∈ z
[PROOFSTEP]
rw [sInter, dif_pos h]
[GOAL]
x y : ZFSet
h : ZFSet.Nonempty x
⊢ y ∈ ZFSet.sep (fun y => ∀ (z : ZFSet), z ∈ x → y ∈ z) (Set.Nonempty.some h) ↔ ∀ (z : ZFSet), z ∈ x → y ∈ z
[PROOFSTEP]
simp only [mem_toSet, mem_sep, and_iff_right_iff_imp]
[GOAL]
x y : ZFSet
h : ZFSet.Nonempty x
⊢ (∀ (z : ZFSet), z ∈ x → y ∈ z) → y ∈ Set.Nonempty.some h
[PROOFSTEP]
exact fun H => H _ h.some_mem
[GOAL]
⊢ ⋃₀ ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
z✝ : ZFSet
⊢ z✝ ∈ ⋃₀ ∅ ↔ z✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
⊢ ¬ZFSet.Nonempty ∅
[PROOFSTEP]
simp
[GOAL]
x y z : ZFSet
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z
[PROOFSTEP]
rcases eq_empty_or_nonempty x with (rfl | hx)
[GOAL]
case inl
y z : ZFSet
hy : y ∈ ⋂₀ ∅
hz : z ∈ ∅
⊢ y ∈ z
[PROOFSTEP]
exact (not_mem_empty z hz).elim
[GOAL]
case inr
x y z : ZFSet
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : ZFSet.Nonempty x
⊢ y ∈ z
[PROOFSTEP]
exact (mem_sInter hx).1 hy z hz
[GOAL]
x y : ZFSet
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x
[PROOFSTEP]
simp_rw [mem_sUnion, mem_singleton, exists_eq_left]
[GOAL]
x y : ZFSet
⊢ y ∈ ⋂₀ {x} ↔ y ∈ x
[PROOFSTEP]
simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]
[GOAL]
x : ZFSet
⊢ toSet (⋃₀ x) = ⋃₀ (toSet '' toSet x)
[PROOFSTEP]
ext
[GOAL]
case h
x x✝ : ZFSet
⊢ x✝ ∈ toSet (⋃₀ x) ↔ x✝ ∈ ⋃₀ (toSet '' toSet x)
[PROOFSTEP]
simp
[GOAL]
x : ZFSet
h : ZFSet.Nonempty x
⊢ toSet (⋂₀ x) = ⋂₀ (toSet '' toSet x)
[PROOFSTEP]
ext
[GOAL]
case h
x : ZFSet
h : ZFSet.Nonempty x
x✝ : ZFSet
⊢ x✝ ∈ toSet (⋂₀ x) ↔ x✝ ∈ ⋂₀ (toSet '' toSet x)
[PROOFSTEP]
simp [mem_sInter h]
[GOAL]
x y : ZFSet
H : {x} = {y}
⊢ x = y
[PROOFSTEP]
let this := congr_arg sUnion H
[GOAL]
x y : ZFSet
H : {x} = {y}
this : ⋃₀ {x} = ⋃₀ {y} := congr_arg sUnion H
⊢ x = y
[PROOFSTEP]
rwa [sUnion_singleton, sUnion_singleton] at this 
[GOAL]
x y : ZFSet
⊢ toSet (x ∪ y) = toSet x ∪ toSet y
[PROOFSTEP]
change (⋃₀ { x, y }).toSet = _
[GOAL]
x y : ZFSet
⊢ toSet (⋃₀ {x, y}) = toSet x ∪ toSet y
[PROOFSTEP]
simp
[GOAL]
x y : ZFSet
⊢ toSet (x ∩ y) = toSet x ∩ toSet y
[PROOFSTEP]
change (ZFSet.sep (fun z => z ∈ y) x).toSet = _
[GOAL]
x y : ZFSet
⊢ toSet (ZFSet.sep (fun z => z ∈ y) x) = toSet x ∩ toSet y
[PROOFSTEP]
ext
[GOAL]
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep (fun z => z ∈ y) x) ↔ x✝ ∈ toSet x ∩ toSet y
[PROOFSTEP]
simp
[GOAL]
x y : ZFSet
⊢ toSet (x \ y) = toSet x \ toSet y
[PROOFSTEP]
change (ZFSet.sep (fun z => z ∉ y) x).toSet = _
[GOAL]
x y : ZFSet
⊢ toSet (ZFSet.sep (fun z => ¬z ∈ y) x) = toSet x \ toSet y
[PROOFSTEP]
ext
[GOAL]
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep (fun z => ¬z ∈ y) x) ↔ x✝ ∈ toSet x \ toSet y
[PROOFSTEP]
simp
[GOAL]
x y z : ZFSet
⊢ z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y
[PROOFSTEP]
rw [← mem_toSet]
[GOAL]
x y z : ZFSet
⊢ z ∈ toSet (x ∪ y) ↔ z ∈ x ∨ z ∈ y
[PROOFSTEP]
simp
[GOAL]
f : ZFSet → ZFSet
H : Definable 1 f
x : ZFSet
⊢ toSet (image f x) = f '' toSet x
[PROOFSTEP]
ext
[GOAL]
case h
f : ZFSet → ZFSet
H : Definable 1 f
x x✝ : ZFSet
⊢ x✝ ∈ toSet (image f x) ↔ x✝ ∈ f '' toSet x
[PROOFSTEP]
simp
[GOAL]
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ range f ↔ Quotient.mk setoid y ∈ Set.range f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ range f → Quotient.mk setoid y ∈ Set.range f
[PROOFSTEP]
rintro ⟨z, hz⟩
[GOAL]
case mp.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : Type (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down))
hz : PSet.Equiv y (Func (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down)) z)
⊢ Quotient.mk setoid y ∈ Set.range f
[PROOFSTEP]
exact ⟨z.down, Quotient.eq_mk_iff_out.2 hz.symm⟩
[GOAL]
case mpr
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ Set.range f → Quotient.mk setoid y ∈ range f
[PROOFSTEP]
rintro ⟨z, hz⟩
[GOAL]
case mpr.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : α
hz : f z = Quotient.mk setoid y
⊢ Quotient.mk setoid y ∈ range f
[PROOFSTEP]
use ULift.up z
[GOAL]
case h
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : α
hz : f z = Quotient.mk setoid y
⊢ PSet.Equiv y (Func (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down)) { down := z })
[PROOFSTEP]
simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)
[GOAL]
α : Type u
f : α → ZFSet
⊢ toSet (range f) = Set.range f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
f : α → ZFSet
x✝ : ZFSet
⊢ x✝ ∈ toSet (range f) ↔ x✝ ∈ Set.range f
[PROOFSTEP]
simp
[GOAL]
x y : ZFSet
⊢ toSet (pair x y) = {{x}, {x, y}}
[PROOFSTEP]
simp [pair]
[GOAL]
p : ZFSet → ZFSet → Prop
x y z : ZFSet
⊢ z ∈ pairSep p x y ↔ ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b ∧ p a b
[PROOFSTEP]
refine' mem_sep.trans ⟨And.right, fun e => ⟨_, e⟩⟩
[GOAL]
p : ZFSet → ZFSet → Prop
x y z : ZFSet
e : ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b ∧ p a b
⊢ z ∈ powerset (powerset (x ∪ y))
[PROOFSTEP]
rcases e with ⟨a, ax, b, bY, rfl, pab⟩
[GOAL]
case intro.intro.intro.intro.intro
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
⊢ pair a b ∈ powerset (powerset (x ∪ y))
[PROOFSTEP]
simp only [mem_powerset, subset_def, mem_union, pair, mem_pair]
[GOAL]
case intro.intro.intro.intro.intro
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
⊢ ∀ ⦃z : ZFSet⦄, z = {a} ∨ z = {a, b} → ∀ ⦃z_1 : ZFSet⦄, z_1 ∈ z → z_1 ∈ x ∨ z_1 ∈ y
[PROOFSTEP]
rintro u (rfl | rfl) v
[GOAL]
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v ∈ {a} → v ∈ x ∨ v ∈ y
[PROOFSTEP]
simp only [mem_singleton, mem_pair]
[GOAL]
case intro.intro.intro.intro.intro.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v ∈ {a, b} → v ∈ x ∨ v ∈ y
[PROOFSTEP]
simp only [mem_singleton, mem_pair]
[GOAL]
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a → v ∈ x ∨ v ∈ y
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y b : ZFSet
bY : b ∈ y
v : ZFSet
ax : v ∈ x
pab : p v b
⊢ v ∈ x ∨ v ∈ y
[PROOFSTEP]
exact Or.inl ax
[GOAL]
case intro.intro.intro.intro.intro.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a ∨ v = b → v ∈ x ∨ v ∈ y
[PROOFSTEP]
rintro (rfl | rfl) <;> [left; right]
[GOAL]
case intro.intro.intro.intro.intro.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a ∨ v = b → v ∈ x ∨ v ∈ y
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case intro.intro.intro.intro.intro.inr.inl
p : ZFSet → ZFSet → Prop
x y b : ZFSet
bY : b ∈ y
v : ZFSet
ax : v ∈ x
pab : p v b
⊢ v ∈ x ∨ v ∈ y
[PROOFSTEP]
left
[GOAL]
case intro.intro.intro.intro.intro.inr.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
v : ZFSet
bY : v ∈ y
pab : p a v
⊢ v ∈ x ∨ v ∈ y
[PROOFSTEP]
right
[GOAL]
case intro.intro.intro.intro.intro.inr.inl.h
p : ZFSet → ZFSet → Prop
x y b : ZFSet
bY : b ∈ y
v : ZFSet
ax : v ∈ x
pab : p v b
⊢ v ∈ x
[PROOFSTEP]
assumption
[GOAL]
case intro.intro.intro.intro.intro.inr.inr.h
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
v : ZFSet
bY : v ∈ y
pab : p a v
⊢ v ∈ y
[PROOFSTEP]
assumption
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
⊢ x = x' ∧ y = y'
[PROOFSTEP]
have ae := ext_iff.1 H
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z ∈ pair x y ↔ z ∈ pair x' y'
⊢ x = x' ∧ y = y'
[PROOFSTEP]
simp only [pair, mem_pair] at ae 
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ y = y'
[PROOFSTEP]
obtain rfl : x = x' := by
  cases' (ae { x }).1 (by simp) with h h
  · exact singleton_injective h
  · have m : x' ∈ ({ x } : ZFSet) := by simp [h]
    rw [mem_singleton.mp m]
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x'
[PROOFSTEP]
cases' (ae { x }).1 (by simp) with h h
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ {x} = {x} ∨ {x} = {x, y}
[PROOFSTEP]
simp
[GOAL]
case inl
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x'}
⊢ x = x'
[PROOFSTEP]
exact singleton_injective h
[GOAL]
case inr
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
⊢ x = x'
[PROOFSTEP]
have m : x' ∈ ({ x } : ZFSet) := by simp [h]
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
⊢ x' ∈ {x}
[PROOFSTEP]
simp [h]
[GOAL]
case inr
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
m : x' ∈ {x}
⊢ x = x'
[PROOFSTEP]
rw [mem_singleton.mp m]
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ x = x ∧ y = y'
[PROOFSTEP]
have he : x = y → y = y' := by
  rintro rfl
  cases' (ae { x, y' }).2 (by simp only [eq_self_iff_true, or_true_iff]) with xy'x xy'xx
  · rw [eq_comm, ← mem_singleton, ← xy'x, mem_pair]
    exact Or.inr rfl
  · simpa [eq_comm] using (ext_iff.1 xy'xx y').1 (by simp)
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ x = y → y = y'
[PROOFSTEP]
rintro rfl
[GOAL]
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
⊢ x = y'
[PROOFSTEP]
cases' (ae { x, y' }).2 (by simp only [eq_self_iff_true, or_true_iff]) with xy'x xy'xx
[GOAL]
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
⊢ {x, y'} = {x} ∨ {x, y'} = {x, y'}
[PROOFSTEP]
simp only [eq_self_iff_true, or_true_iff]
[GOAL]
case inl
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'x : {x, y'} = {x}
⊢ x = y'
[PROOFSTEP]
rw [eq_comm, ← mem_singleton, ← xy'x, mem_pair]
[GOAL]
case inl
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'x : {x, y'} = {x}
⊢ y' = x ∨ y' = y'
[PROOFSTEP]
exact Or.inr rfl
[GOAL]
case inr
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'xx : {x, y'} = {x, x}
⊢ x = y'
[PROOFSTEP]
simpa [eq_comm] using (ext_iff.1 xy'xx y').1 (by simp)
[GOAL]
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'xx : {x, y'} = {x, x}
⊢ y' ∈ {x, y'}
[PROOFSTEP]
simp
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
⊢ x = x ∧ y = y'
[PROOFSTEP]
obtain xyx | xyy' := (ae { x, y }).1 (by simp)
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
⊢ {x, y} = {x} ∨ {x, y} = {x, y}
[PROOFSTEP]
simp
[GOAL]
case inl
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyx : {x, y} = {x}
⊢ x = x ∧ y = y'
[PROOFSTEP]
obtain rfl := mem_singleton.mp ((ext_iff.1 xyx y).1 <| by simp)
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyx : {x, y} = {x}
⊢ y ∈ {x, y}
[PROOFSTEP]
simp
[GOAL]
case inl
y y' : ZFSet
H : pair y y = pair y y'
ae : ∀ (z : ZFSet), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
he : y = y → y = y'
xyx : {y, y} = {y}
⊢ y = y ∧ y = y'
[PROOFSTEP]
simp [he rfl]
[GOAL]
case inr
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
⊢ x = x ∧ y = y'
[PROOFSTEP]
obtain rfl | yy' := mem_pair.mp ((ext_iff.1 xyy' y).1 <| by simp)
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
⊢ y ∈ {x, y}
[PROOFSTEP]
simp
[GOAL]
case inr.inl
y y' : ZFSet
H : pair y y = pair y y'
ae : ∀ (z : ZFSet), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
he : y = y → y = y'
xyy' : {y, y} = {y, y'}
⊢ y = y ∧ y = y'
[PROOFSTEP]
simp [he rfl]
[GOAL]
case inr.inr
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
yy' : y = y'
⊢ x = x ∧ y = y'
[PROOFSTEP]
simp [yy']
[GOAL]
x y z : ZFSet
⊢ z ∈ prod x y ↔ ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b
[PROOFSTEP]
simp [prod]
[GOAL]
x y a b : ZFSet
⊢ pair a b ∈ prod x y ↔ a ∈ x ∧ b ∈ y
[PROOFSTEP]
simp
[GOAL]
x y f : ZFSet
⊢ f ∈ funs x y ↔ IsFunc x y f
[PROOFSTEP]
simp [funs, IsFunc]
[GOAL]
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
⊢ y = f z
[PROOFSTEP]
let ⟨w, _, we⟩ := mem_image.1 yx
[GOAL]
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
w : ZFSet
left✝ : w ∈ x
we : pair w (f w) = pair z y
⊢ y = f z
[PROOFSTEP]
let ⟨wz, fy⟩ := pair_injective we
[GOAL]
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
w : ZFSet
left✝ : w ∈ x
we : pair w (f w) = pair z y
wz : w = z
fy : f w = y
⊢ y = f z
[PROOFSTEP]
rw [← fy, wz]
[GOAL]
p : ZFSet → Prop
x y : ZFSet
⊢ Hereditarily p x ↔ p x ∧ ∀ (y : ZFSet), y ∈ x → Hereditarily p y
[PROOFSTEP]
rw [← Hereditarily]
[GOAL]
p : ZFSet → Prop
x y : ZFSet
⊢ Hereditarily p x → p ∅
[PROOFSTEP]
apply @ZFSet.inductionOn _ x
[GOAL]
p : ZFSet → Prop
x y : ZFSet
⊢ ∀ (x : ZFSet), (∀ (y : ZFSet), y ∈ x → Hereditarily p y → p ∅) → Hereditarily p x → p ∅
[PROOFSTEP]
intro y IH h
[GOAL]
p : ZFSet → Prop
x y✝ y : ZFSet
IH : ∀ (y_1 : ZFSet), y_1 ∈ y → Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅
[PROOFSTEP]
rcases ZFSet.eq_empty_or_nonempty y with (rfl | ⟨a, ha⟩)
[GOAL]
case inl
p : ZFSet → Prop
x y : ZFSet
IH : ∀ (y : ZFSet), y ∈ ∅ → Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅
[PROOFSTEP]
exact h.self
[GOAL]
case inr.intro
p : ZFSet → Prop
x y✝ y : ZFSet
IH : ∀ (y_1 : ZFSet), y_1 ∈ y → Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet
ha : a ∈ toSet y
⊢ p ∅
[PROOFSTEP]
exact IH a ha (h.mem ha)
[GOAL]
⊢ ∀ (a : Class), Acc (fun x x_1 => x ∈ x_1) a
[PROOFSTEP]
have H : ∀ x : ZFSet.{u}, @Acc Class.{u} (· ∈ ·) ↑x :=
  by
  refine' fun a => ZFSet.inductionOn a fun x IH => ⟨_, _⟩
  rintro A ⟨z, rfl, hz⟩
  exact IH z hz
[GOAL]
⊢ ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
[PROOFSTEP]
refine' fun a => ZFSet.inductionOn a fun x IH => ⟨_, _⟩
[GOAL]
a x : ZFSet
IH : ∀ (y : ZFSet), y ∈ x → Acc (fun x x_1 => x ∈ x_1) ↑y
⊢ ∀ (y : Class), y ∈ ↑x → Acc (fun x x_1 => x ∈ x_1) y
[PROOFSTEP]
rintro A ⟨z, rfl, hz⟩
[GOAL]
case intro.intro
a x : ZFSet
IH : ∀ (y : ZFSet), y ∈ x → Acc (fun x x_1 => x ∈ x_1) ↑y
z : ZFSet
hz : ↑x z
⊢ Acc (fun x x_1 => x ∈ x_1) ↑z
[PROOFSTEP]
exact IH z hz
[GOAL]
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
⊢ ∀ (a : Class), Acc (fun x x_1 => x ∈ x_1) a
[PROOFSTEP]
refine' fun A => ⟨A, _⟩
[GOAL]
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
A : Class
⊢ ∀ (y : Class), y ∈ A → Acc (fun x x_1 => x ∈ x_1) y
[PROOFSTEP]
rintro B ⟨x, rfl, _⟩
[GOAL]
case intro.intro
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
A : Class
x : ZFSet
right✝ : A x
⊢ Acc (fun x x_1 => x ∈ x_1) ↑x
[PROOFSTEP]
exact H x
[GOAL]
⊢ congToClass ∅ = ∅
[PROOFSTEP]
ext z
[GOAL]
case a
z : ZFSet
⊢ congToClass ∅ z ↔ ∅ z
[PROOFSTEP]
simp only [congToClass, not_empty_hom, iff_false_iff]
[GOAL]
case a
z : ZFSet
⊢ ¬setOf (fun y => ↑y ∈ ∅) z
[PROOFSTEP]
exact Set.not_mem_empty z
[GOAL]
⊢ classToCong ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case h
x✝ : Class
⊢ x✝ ∈ classToCong ∅ ↔ x✝ ∈ ∅
[PROOFSTEP]
simp [classToCong]
[GOAL]
x y : ZFSet
h : ↑x = ↑y
z : ZFSet
⊢ z ∈ x ↔ z ∈ y
[PROOFSTEP]
change (x : Class.{u}) z ↔ (y : Class.{u}) z
[GOAL]
x y : ZFSet
h : ↑x = ↑y
z : ZFSet
⊢ ↑x z ↔ ↑y z
[PROOFSTEP]
rw [h]
[GOAL]
A : Class
x : ZFSet
x✝ : ToSet A ↑x
y : ZFSet
yx : ↑y = ↑x
py : A y
⊢ A x
[PROOFSTEP]
rwa [ofSet.inj yx] at py 
[GOAL]
x : Class
y : ZFSet
⊢ (⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z
[PROOFSTEP]
constructor
[GOAL]
case mp
x : Class
y : ZFSet
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z
[PROOFSTEP]
rintro ⟨-, ⟨z, rfl, hxz⟩, hyz⟩
[GOAL]
case mp.intro.intro.intro.intro
x : Class
y z : ZFSet
hxz : x z
hyz : y ∈ ↑z
⊢ ∃ z, x z ∧ y ∈ z
[PROOFSTEP]
exact ⟨z, hxz, hyz⟩
[GOAL]
case mpr
x : Class
y : ZFSet
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y
[PROOFSTEP]
exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩
[GOAL]
x y : ZFSet
⊢ (∃ z, ↑x z ∧ y ∈ z) ↔ ∃ z, z ∈ x ∧ y ∈ z
[PROOFSTEP]
rfl
[GOAL]
x y : Class
⊢ y ∈ ⋃₀ x ↔ ∃ z, z ∈ x ∧ y ∈ z
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : Class
⊢ y ∈ ⋃₀ x → ∃ z, z ∈ x ∧ y ∈ z
[PROOFSTEP]
rintro ⟨w, rfl, z, hzx, hwz⟩
[GOAL]
case mp.intro.intro.intro.intro
x : Class
w : ZFSet
z : Set ZFSet
hzx : z ∈ classToCong x
hwz : w ∈ z
⊢ ∃ z, z ∈ x ∧ ↑w ∈ z
[PROOFSTEP]
exact ⟨z, hzx, coe_mem.2 hwz⟩
[GOAL]
case mpr
x y : Class
⊢ (∃ z, z ∈ x ∧ y ∈ z) → y ∈ ⋃₀ x
[PROOFSTEP]
rintro ⟨w, hwx, z, rfl, hwz⟩
[GOAL]
case mpr.intro.intro.intro.intro
x w : Class
hwx : w ∈ x
z : ZFSet
hwz : w z
⊢ ↑z ∈ ⋃₀ x
[PROOFSTEP]
exact ⟨z, rfl, w, hwx, hwz⟩
[GOAL]
x : Class
y : ZFSet
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet), x z → y ∈ z
[PROOFSTEP]
refine' ⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, _⟩
[GOAL]
x : Class
y : ZFSet
⊢ (∀ (z : ZFSet), x z → y ∈ z) → (⋂₀ x) y
[PROOFSTEP]
rintro H - ⟨z, rfl, hxz⟩
[GOAL]
case intro.intro
x : Class
y : ZFSet
H : ∀ (z : ZFSet), x z → y ∈ z
z : ZFSet
hxz : x z
⊢ y ∈ ↑z
[PROOFSTEP]
exact H _ hxz
[GOAL]
x y z : Class
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z
[PROOFSTEP]
obtain ⟨w, rfl, hw⟩ := hy
[GOAL]
case intro.intro
x z : Class
hz : z ∈ x
w : ZFSet
hw : (⋂₀ x) w
⊢ ↑w ∈ z
[PROOFSTEP]
exact coe_mem.2 (hw z hz)
[GOAL]
x y : Class
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ (z : Class), z ∈ x → y ∈ z
[PROOFSTEP]
refine' ⟨fun hy z => mem_of_mem_sInter hy, fun H => _⟩
[GOAL]
x y : Class
h : Set.Nonempty x
H : ∀ (z : Class), z ∈ x → y ∈ z
⊢ y ∈ ⋂₀ x
[PROOFSTEP]
simp_rw [mem_def, sInter_apply]
[GOAL]
x y : Class
h : Set.Nonempty x
H : ∀ (z : Class), z ∈ x → y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
[PROOFSTEP]
obtain ⟨z, hz⟩ := h
[GOAL]
case intro
x y : Class
H : ∀ (z : Class), z ∈ x → y ∈ z
z : ZFSet
hz : z ∈ x
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
[PROOFSTEP]
obtain ⟨y, rfl, _⟩ := H z (coe_mem.2 hz)
[GOAL]
case intro.intro.intro
x : Class
z : ZFSet
hz : z ∈ x
y : ZFSet
right✝ : ↑z y
H : ∀ (z : Class), z ∈ x → ↑y ∈ z
⊢ ∃ x_1, ↑x_1 = ↑y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
[PROOFSTEP]
refine' ⟨y, rfl, fun w hxw => _⟩
[GOAL]
case intro.intro.intro
x : Class
z : ZFSet
hz : z ∈ x
y : ZFSet
right✝ : ↑z y
H : ∀ (z : Class), z ∈ x → ↑y ∈ z
w : ZFSet
hxw : x w
⊢ y ∈ w
[PROOFSTEP]
simpa only [coe_mem, coe_apply] using H w (coe_mem.2 hxw)
[GOAL]
⊢ ⋃₀ ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
z✝ : ZFSet
⊢ (⋃₀ ∅) z✝ ↔ ∅ z✝
[PROOFSTEP]
simp
[GOAL]
⊢ ⋂₀ ∅ = univ
[PROOFSTEP]
rw [sInter, classToCong_empty, Set.sInter_empty, univ]
[GOAL]
A : Class
hA : powerset A ⊆ A
⊢ ∀ (x : ZFSet), A x
[PROOFSTEP]
by_contra' hnA
[GOAL]
A : Class
hA : powerset A ⊆ A
hnA : ∃ x, ¬A x
⊢ False
[PROOFSTEP]
exact
  WellFounded.min_mem ZFSet.mem_wf _ hnA
    (hA fun x hx => Classical.not_not.1 fun hB => WellFounded.not_lt_min ZFSet.mem_wf _ hnA hB <| coe_apply.1 hx)
[GOAL]
A : Class
x : ZFSet
H : ∀ (y : ZFSet), A y ↔ y = x
y : ZFSet
x✝ : iota A y
x' : ZFSet
h : setOf (fun x => ∀ (y : ZFSet), A y ↔ y = x) x'
yx' : y ∈ ↑x'
⊢ ↑x y
[PROOFSTEP]
rwa [← (H x').1 <| (h x').2 rfl]
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
⊢ Class.ToSet (fun x_1 => ↑(map f x) (pair x_1 z)) ↑y ↔ z = f y
[PROOFSTEP]
rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
⊢ (∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z) ↔ z = f y
[PROOFSTEP]
exact
  ⟨fun ⟨w, _, pr⟩ => by
    let ⟨wy, fw⟩ := ZFSet.pair_injective pr
    rw [← fw, wy], fun e => by
    subst e
    exact ⟨_, h, rfl⟩⟩
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
x✝ : ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
w : ZFSet
left✝ : w ∈ x
pr : pair w (f w) = pair y z
⊢ z = f y
[PROOFSTEP]
let ⟨wy, fw⟩ := ZFSet.pair_injective pr
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
x✝ : ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
w : ZFSet
left✝ : w ∈ x
pr : pair w (f w) = pair y z
wy : w = y
fw : f w = z
⊢ z = f y
[PROOFSTEP]
rw [← fw, wy]
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
e : z = f y
⊢ ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
[PROOFSTEP]
subst e
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
⊢ ∃ z, z ∈ x ∧ pair z (f z) = pair y (f y)
[PROOFSTEP]
exact ⟨_, h, rfl⟩
[GOAL]
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
n : ¬∃ y_1, y_1 ∈ y
⊢ ∅ ∈ x
[PROOFSTEP]
rwa [← (eq_empty y).2 fun z zx => n ⟨z, zx⟩]
[GOAL]
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ ↑(choice x) ′ ↑y ∈ ↑y
[PROOFSTEP]
delta choice
[GOAL]
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ ↑(map (fun y => Classical.epsilon fun z => z ∈ y) x) ′ ↑y ∈ ↑y
[PROOFSTEP]
rw [@map_fval _ (Classical.allDefinable _) x y yx, Class.coe_mem, Class.coe_apply]
[GOAL]
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ (Classical.epsilon fun z => z ∈ y) ∈ y
[PROOFSTEP]
exact choice_mem_aux x h y yx
