Let A, B and f be given.
Assume Hinj: inj A B f.
We will prove inj (𝒫 A) (𝒫 B) (λS : set ⇒ {f x|x ∈ S}).
Apply (injI (𝒫 A) (𝒫 B) (λS : set ⇒ {f x|x ∈ S})) to the current goal.
Let S be given.
Assume HS: S ∈ 𝒫 A.
We will prove {f x|x ∈ S} ∈ 𝒫 B.
Apply PowerI to the current goal.
We will prove {f x|x ∈ S} ⊆ B.
Let y be given.
Assume Hy: y ∈ {f x|x ∈ S}.
We will prove y ∈ B.
We prove the intermediate claim Himg: ∀x ∈ A, f x ∈ B.
An exact proof term for the current goal is (andEL (∀x ∈ A, f x ∈ B) (∀x z ∈ A, f x = f z → x = z) Hinj).
We prove the intermediate claim HSsubA: S ⊆ A.
An exact proof term for the current goal is (PowerE A S HS).
Apply (ReplE_impred S f y Hy (y ∈ B)) to the current goal.
Let x be given.
Assume HxS: x ∈ S.
Assume Hyeq: y = f x.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (HSsubA x HxS).
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is (Himg x HxA).
Let S1 be given.
Assume HS1: S1 ∈ 𝒫 A.
Let S2 be given.
Assume HS2: S2 ∈ 𝒫 A.
Assume Heq: {f x|x ∈ S1} = {f x|x ∈ S2}.
We will prove S1 = S2.
Apply set_ext to the current goal.
Let x be given.
Assume Hx1: x ∈ S1.
We will prove x ∈ S2.
We prove the intermediate claim HS1subA: S1 ⊆ A.
An exact proof term for the current goal is (PowerE A S1 HS1).
We prove the intermediate claim HS2subA: S2 ⊆ A.
An exact proof term for the current goal is (PowerE A S2 HS2).
We prove the intermediate claim Hinj0: ∀u v ∈ A, f u = f v → u = v.
An exact proof term for the current goal is (andER (∀x ∈ A, f x ∈ B) (∀x z ∈ A, f x = f z → x = z) Hinj).
We prove the intermediate claim Hfx1: f x ∈ {f y|y ∈ S1}.
An exact proof term for the current goal is (ReplI S1 f x Hx1).
We prove the intermediate claim Hfx2: f x ∈ {f y|y ∈ S2}.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hfx1.
Apply (ReplE_impred S2 f (f x) Hfx2 (x ∈ S2)) to the current goal.
Let y be given.
Assume HyS2: y ∈ S2.
Assume Hfxy: f x = f y.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (HS1subA x Hx1).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (HS2subA y HyS2).
We prove the intermediate claim Hxy: x = y.
An exact proof term for the current goal is (Hinj0 x HxA y HyA Hfxy).
rewrite the current goal using Hxy (from left to right).
An exact proof term for the current goal is HyS2.
Let x be given.
Assume Hx2: x ∈ S2.
We will prove x ∈ S1.
We prove the intermediate claim HS1subA: S1 ⊆ A.
An exact proof term for the current goal is (PowerE A S1 HS1).
We prove the intermediate claim HS2subA: S2 ⊆ A.
An exact proof term for the current goal is (PowerE A S2 HS2).
We prove the intermediate claim Hinj0: ∀u v ∈ A, f u = f v → u = v.
An exact proof term for the current goal is (andER (∀x ∈ A, f x ∈ B) (∀x z ∈ A, f x = f z → x = z) Hinj).
We prove the intermediate claim Hfx2: f x ∈ {f y|y ∈ S2}.
An exact proof term for the current goal is (ReplI S2 f x Hx2).
We prove the intermediate claim Hfx1: f x ∈ {f y|y ∈ S1}.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hfx2.
Apply (ReplE_impred S1 f (f x) Hfx1 (x ∈ S1)) to the current goal.
Let y be given.
Assume HyS1: y ∈ S1.
Assume Hfxy: f x = f y.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (HS2subA x Hx2).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (HS1subA y HyS1).
We prove the intermediate claim Hxy: x = y.
An exact proof term for the current goal is (Hinj0 x HxA y HyA Hfxy).
rewrite the current goal using Hxy (from left to right).
An exact proof term for the current goal is HyS1.
∎