x y : Class
h : Set.Nonempty x
H : ∀ (z : Class), z ∈ x → y ∈ z
⊢ y ∈ ⋂₀ x
x y : Class
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ (z : Class), z ∈ x → y ∈ z
refine' ⟨fun hy z => mem_of_mem_sInter hy, fun H => _⟩
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
x y : Class
h : Set.Nonempty x
H : ∀ (z : Class), z ∈ x → y ∈ z
⊢ y ∈ ⋂₀ x
simp_rw [mem_def, sInter_apply]
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
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
obtain ⟨z, hz⟩ := h
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
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
obtain ⟨y, rfl, _⟩ := H z (coe_mem.2 hz)
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
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
refine' ⟨y, rfl, fun w hxw => _⟩
no goals
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
simpa only [coe_mem, coe_apply] using H w (coe_mem.2 hxw)