case inl
y z : ZFSet
hy : y ∈ ⋂₀ ∅
hz : z ∈ ∅
⊢ y ∈ z

case inr
x y z : ZFSet
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : ZFSet.Nonempty x
⊢ y ∈ z
x y z : ZFSet
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z
rcases eq_empty_or_nonempty x with (rfl | hx)
no goals
case inl
y z : ZFSet
hy : y ∈ ⋂₀ ∅
hz : z ∈ ∅
⊢ y ∈ z
exact (not_mem_empty z hz).elim
no goals
case inr
x y z : ZFSet
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : ZFSet.Nonempty x
⊢ y ∈ z
exact (mem_sInter hx).1 hy z hz