x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ IsTransitive (⋃₀ {x, y})
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ IsTransitive (x ∪ y)
rw [← sUnion_pair]
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ ∀ (z : ZFSet), z ∈ {x, y} → IsTransitive z
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ IsTransitive (⋃₀ {x, y})
apply IsTransitive.sUnion' fun z => _
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z✝ : ZFSet
⊢ z✝ ∈ {x, y} → IsTransitive z✝
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
⊢ ∀ (z : ZFSet), z ∈ {x, y} → IsTransitive z
intro
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z✝ : ZFSet
⊢ z✝ = x ∨ z✝ = y → IsTransitive z✝
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z✝ : ZFSet
⊢ z✝ ∈ {x, y} → IsTransitive z✝
rw [mem_pair]
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✝
x y z : ZFSet
hx : IsTransitive x
hy : IsTransitive y
z✝ : ZFSet
⊢ z✝ = x ∨ z✝ = y → IsTransitive z✝
rintro (rfl | rfl)
no goals
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✝
assumption'