Let A and f be given.
Assume H.
Apply H to the current goal.
Assume H1: ∀X ∈ 𝒫 A, f X ∈ A.
Assume H2: ∀X Y ∈ 𝒫 A, f X = f Y → X = Y.
Set D to be the term {f X|X ∈ 𝒫 A, f X ∉ X}.
We prove the intermediate claim L1: D ∈ 𝒫 A.
Apply PowerI to the current goal.
Let n be given.
Assume H3: n ∈ D.
Apply ReplSepE_impred (𝒫 A) (λX ⇒ f X ∉ X) f n H3 to the current goal.
Let X be given.
Assume HX: X ∈ 𝒫 A.
Assume H4: f X ∉ X.
Assume H5: n = f X.
We will prove n ∈ A.
rewrite the current goal using H5 (from left to right).
Apply H1 to the current goal.
An exact proof term for the current goal is HX.
We prove the intermediate claim L2: f D ∉ D.
Assume H3: f D ∈ D.
Apply ReplSepE_impred (𝒫 A) (λX ⇒ f X ∉ X) f (f D) H3 to the current goal.
Let X be given.
Assume HX: X ∈ 𝒫 A.
Assume H4: f X ∉ X.
Assume H5: f D = f X.
We prove the intermediate claim L2a: D = X.
An exact proof term for the current goal is H2 D L1 X HX H5.
Apply H4 to the current goal.
rewrite the current goal using L2a (from right to left).
An exact proof term for the current goal is H3.
Apply L2 to the current goal.
We will prove f D ∈ D.
Apply ReplSepI to the current goal.
We will prove D ∈ 𝒫 A.
An exact proof term for the current goal is L1.
We will prove f D ∉ D.
An exact proof term for the current goal is L2.
∎