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
x y✝ z✝ : ZFSet
h : IsTransitive x
y : ZFSet
hy : y ∈ ⋃₀ x
z : ZFSet
hz : z ∈ y
⊢ z ∈ ⋃₀ x
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
no goals
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
exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)