Let A and f be given.
Assume H.
Apply H to the current goal.
Assume H1: ∀u ∈ A, f u ∈ 𝒫 A.
Assume H2: ∀w ∈ 𝒫 A, ∃u ∈ A, f u = w.
Set D to be the term {x ∈ A|x ∉ f x}.
We prove the intermediate claim L1: D ∈ 𝒫 A.
An exact proof term for the current goal is Sep_In_Power A (λx ⇒ x ∉ f x).
Apply H2 D L1 to the current goal.
Let d be given.
Assume H.
Apply H to the current goal.
Assume Hd: d ∈ A.
Assume HfdD: f d = D.
We prove the intermediate claim L2: d ∉ D.
Assume H3: d ∈ D.
Apply SepE2 A (λx ⇒ x ∉ f x) d H3 to the current goal.
We will prove d ∈ f d.
rewrite the current goal using HfdD (from left to right).
We will prove d ∈ D.
An exact proof term for the current goal is H3.
Apply L2 to the current goal.
We will prove d ∈ D.
Apply SepI to the current goal.
We will prove d ∈ A.
An exact proof term for the current goal is Hd.
We will prove d ∉ f d.
rewrite the current goal using HfdD (from left to right).
An exact proof term for the current goal is L2.
∎