[GOAL]
x y z✝ : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z : ZFSet
hz : z ∈ x ∩ y
w : ZFSet
hw : w ∈ z
⊢ w ∈ x ∩ y
[PROOFSTEP]
rw [mem_inter] at hz ⊢
[GOAL]
x y z✝ : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z : ZFSet
hz : z ∈ x ∧ z ∈ y
w : ZFSet
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y
[PROOFSTEP]
exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩
[GOAL]
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
⊢ z ∈ ⋃₀ x
[PROOFSTEP]
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
[GOAL]
case intro.intro
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
w : ZFSet
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x
[PROOFSTEP]
exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)
[GOAL]
x y✝ z✝ : ZFSet
H : ∀ (y : ZFSet), y ∈ x → IsTransitive y
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
⊢ z ∈ ⋃₀ x
[PROOFSTEP]
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
[GOAL]
case intro.intro
x y✝ z✝ : ZFSet
H : ∀ (y : ZFSet), y ∈ x → IsTransitive y
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
w : ZFSet
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x
[PROOFSTEP]
exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ IsTransitive (x ∪ y)
[PROOFSTEP]
rw [← sUnion_pair]
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ IsTransitive (⋃₀ {x, y})
[PROOFSTEP]
apply IsTransitive.sUnion' fun z => _
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ ∀ (z : ZFSet), z ∈ {x, y} → IsTransitive z
[PROOFSTEP]
intro
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z✝ : ZFSet
⊢ z✝ ∈ {x, y} → IsTransitive z✝
[PROOFSTEP]
rw [mem_pair]
[GOAL]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z✝ : ZFSet
⊢ z✝ = x ∨ z✝ = y → IsTransitive z✝
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
y z : ZFSet
hy : IsTransitive y
z✝ : ZFSet
hx : IsTransitive z✝
⊢ IsTransitive z✝
case inr x z : ZFSet hx : IsTransitive x z✝ : ZFSet hy : IsTransitive z✝ ⊢ IsTransitive z✝
[PROOFSTEP]
assumption'
[GOAL]
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ powerset x
z : ZFSet
hz : z ∈ y
⊢ z ∈ powerset x
[PROOFSTEP]
rw [mem_powerset] at hy ⊢
[GOAL]
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ⊆ x
z : ZFSet
hz : z ∈ y
⊢ z ⊆ x
[PROOFSTEP]
exact h.subset_of_mem (hy hz)
[GOAL]
x y✝ z : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
⊢ y ∈ x
[PROOFSTEP]
rcases mem_sUnion.1 hy with ⟨z, hz, hz'⟩
[GOAL]
case intro.intro
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ x
hz' : y ∈ z
⊢ y ∈ x
[PROOFSTEP]
exact h.mem_trans hz' hz
