Let U be given.
Assume C: ZF_closed U.
Let x be given.
Assume Hx: x ∈ U.
Let y be given.
Assume Hy: y ∈ U.
We will prove {x,y} ∈ U.
We prove the intermediate claim L1: {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)} = {x,y}.
Apply set_ext to the current goal.
We will prove {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)} ⊆ {x,y}.
Let z be given.
Assume Hz: z ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.
We will prove z ∈ {x,y}.
Apply (ReplE_impred (𝒫 (𝒫 x)) (λX ⇒ if x ∈ X then x else y) z Hz) to the current goal.
Let X be given.
Assume _.
We will prove z = (if x ∈ X then x else y) → z ∈ {x,y}.
Apply (xm (x ∈ X)) to the current goal.
Assume H2: x ∈ X.
rewrite the current goal using (If_i_1 (x ∈ X) x y H2) (from left to right).
We will prove (z = x → z ∈ {x,y}).
Assume H3: z = x.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is (UPairI1 x y).
Assume H2: x ∉ X.
rewrite the current goal using (If_i_0 (x ∈ X) x y H2) (from left to right).
We will prove (z = y → z ∈ {x,y}).
Assume H3: z = y.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is (UPairI2 x y).
We will prove {x,y} ⊆ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.
Let z be given.
Assume Hz: z ∈ {x,y}.
We will prove z ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.
We prove the intermediate claim L1a: (if x ∈ (𝒫 x) then x else y) ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.
Apply (ReplI (𝒫 (𝒫 x)) (λX ⇒ if x ∈ X then x else y) (𝒫 x)) to the current goal.
We will prove 𝒫 x ∈ 𝒫 (𝒫 x).
An exact proof term for the current goal is (Self_In_Power (𝒫 x)).
We prove the intermediate claim L1b: (if x ∈ Empty then x else y) ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.
Apply (ReplI (𝒫 (𝒫 x)) (λX ⇒ if x ∈ X then x else y) Empty) to the current goal.
We will prove Empty ∈ 𝒫 (𝒫 x).
An exact proof term for the current goal is (Empty_In_Power (𝒫 x)).
Apply (UPairE z x y Hz) to the current goal.
Assume H1: z = x.
rewrite the current goal using H1 (from left to right).
We will prove x ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.
rewrite the current goal using (If_i_1 (x ∈ (𝒫 x)) x y (Self_In_Power x)) (from right to left) at position 1.
An exact proof term for the current goal is L1a.
Assume H1: z = y.
rewrite the current goal using H1 (from left to right).
We will prove y ∈ {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)}.
rewrite the current goal using (If_i_0 (x ∈ Empty) x y (EmptyE x)) (from right to left) at position 1.
An exact proof term for the current goal is L1b.
We will prove {x,y} ∈ U.
rewrite the current goal using L1 (from right to left).
We will prove {if x ∈ X then x else y|X ∈ 𝒫 (𝒫 x)} ∈ U.
We prove the intermediate claim L2: 𝒫 (𝒫 x) ∈ U.
An exact proof term for the current goal is (ZF_Power_closed U C (𝒫 x) (ZF_Power_closed U C x Hx)).
We prove the intermediate claim L3: ∀X ∈ 𝒫 (𝒫 x), (if x ∈ X then x else y) ∈ U.
Let X be given.
Assume _.
We will prove (if x ∈ X then x else y) ∈ U.
Apply (xm (x ∈ X)) to the current goal.
Assume H1: x ∈ X.
rewrite the current goal using (If_i_1 (x ∈ X) x y H1) (from left to right).
We will prove x ∈ U.
An exact proof term for the current goal is Hx.
Assume H1: x ∉ X.
rewrite the current goal using (If_i_0 (x ∈ X) x y H1) (from left to right).
We will prove y ∈ U.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is (ZF_Repl_closed U C (𝒫 (𝒫 x)) L2 (λX ⇒ if x ∈ X then x else y) L3).
∎