x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ ↑(map (fun y => Classical.epsilon fun z => z ∈ y) x) ′ ↑y ∈ ↑y
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ ↑(choice x) ′ ↑y ∈ ↑y
delta choice
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ (Classical.epsilon fun z => z ∈ y) ∈ y
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ ↑(map (fun y => Classical.epsilon fun z => z ∈ y) x) ′ ↑y ∈ ↑y
rw [@map_fval _ (Classical.AllDefinable _) x y yx, Class.coe_mem, Class.coe_apply]
no goals
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ (Classical.epsilon fun z => z ∈ y) ∈ y
exact choice_mem_aux x h y yx