f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
⊢ (∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z) ↔ z = f y
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
⊢ Class.ToSet (fun x_1 => ↑(map f x) (pair x_1 z)) ↑y ↔ z = f y
rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]
no goals
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
⊢ (∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z) ↔ z = f y
exact
  ⟨fun ⟨w, _, pr⟩ => by
    let ⟨wy, fw⟩ := ZFSet.pair_injective pr
    rw [← fw, wy], fun e => by
    subst e
    exact ⟨_, h, rfl⟩⟩
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
x✝ : ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
w : ZFSet
left✝ : w ∈ x
pr : pair w (f w) = pair y z
wy : w = y
fw : f w = z
⊢ z = f y
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
x✝ : ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
w : ZFSet
left✝ : w ∈ x
pr : pair w (f w) = pair y z
⊢ z = f y
let ⟨wy, fw⟩ := ZFSet.pair_injective pr
no goals
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
x✝ : ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
w : ZFSet
left✝ : w ∈ x
pr : pair w (f w) = pair y z
wy : w = y
fw : f w = z
⊢ z = f y
rw [← fw, wy]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
⊢ ∃ z, z ∈ x ∧ pair z (f z) = pair y (f y)
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
e : z = f y
⊢ ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
subst e
no goals
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
⊢ ∃ z, z ∈ x ∧ pair z (f z) = pair y (f y)
exact ⟨_, h, rfl⟩