Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ι be given.

Assume H0: bij x0 x1 x2.

Apply H0 with surj x0 x1 x2.

Assume H1: and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4).

Apply H1 with (∀ x3 . prim1 x3 x1 ⟶ ∃ x4 . and (prim1 x4 x0) (x2 x4 = x3)) ⟶ surj x0 x1 x2.

Assume H2: ∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1.

Assume H3: ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.

Assume H4: ∀ x3 . prim1 x3 x1 ⟶ ∃ x4 . and (prim1 x4 x0) (x2 x4 = x3).

Apply andI with ∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1, ∀ x3 . prim1 x3 x1 ⟶ ∃ x4 . and (prim1 x4 x0) (x2 x4 = x3) leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H4.

■

Proofgold Proof