Apply Inj0_pair_0_eq with λ x0 x1 : ι → ι . ∀ x2 x3 . x0 x3 ∈ x2 ⟶ x3 ∈ proj0 x2.

Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: Inj0 x1 ∈ x0.

Apply Unj_Inj0_eq with x1, λ x2 x3 . x2 ∈ {Unj x4|x4 ∈ x0,∃ x5 . Inj0 x5 = x4}.

Apply ReplSepI with x0, λ x2 . ∃ x3 . Inj0 x3 = x2, Unj, Inj0 x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x2 of type ο be given.

Assume H1: ∀ x3 . Inj0 x3 = Inj0 x1 ⟶ x2.

Apply H1 with x1.

Let x3 of type ι → ι → ο be given.

Assume H2: x3 (Inj0 x1) (Inj0 x1).

The subproof is completed by applying H2.

■

Proofgold Proof