Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι → ι be given.
Let x4 of type ι → ι be given.
Apply H0 with
bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5)).
Assume H1:
and (∀ x5 . x5 ∈ x0 ⟶ x3 x5 ∈ x1) (∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x3 x5 = x3 x6 ⟶ x5 = x6).
Assume H2:
∀ x5 . x5 ∈ x1 ⟶ ∃ x6 . and (x6 ∈ x0) (x3 x6 = x5).
Apply H1 with
bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5)).
Assume H3: ∀ x5 . x5 ∈ x0 ⟶ x3 x5 ∈ x1.
Assume H4: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x3 x5 = x3 x6 ⟶ x5 = x6.
Apply H5 with
bij x0 x2 (λ x5 . x4 (x3 x5)).
Assume H6:
and (∀ x5 . x5 ∈ x1 ⟶ x4 x5 ∈ x2) (∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6).
Assume H7:
∀ x5 . x5 ∈ x2 ⟶ ∃ x6 . and (x6 ∈ x1) (x4 x6 = x5).
Apply H6 with
bij x0 x2 (λ x5 . x4 (x3 x5)).
Assume H8: ∀ x5 . x5 ∈ x1 ⟶ x4 x5 ∈ x2.
Assume H9: ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Apply and3I with
∀ x5 . x5 ∈ x0 ⟶ x4 (x3 x5) ∈ x2,
∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 (x3 x5) = x4 (x3 x6) ⟶ x5 = x6,
∀ x5 . x5 ∈ x2 ⟶ ∃ x6 . and (x6 ∈ x0) (x4 (x3 x6) = x5) leaving 3 subgoals.
Let x5 of type ι be given.
Assume H10: x5 ∈ x0.
Apply H8 with
x3 x5.
Apply H3 with
x5.
The subproof is completed by applying H10.
Let x5 of type ι be given.
Assume H10: x5 ∈ x0.
Let x6 of type ι be given.
Assume H11: x6 ∈ x0.
Assume H12: x4 (x3 x5) = x4 (x3 x6).
Apply H4 with
x5,
x6 leaving 3 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Apply H9 with
x3 x5,
x3 x6 leaving 3 subgoals.
Apply H3 with
x5.
The subproof is completed by applying H10.
Apply H3 with
x6.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
Let x5 of type ι be given.
Assume H10: x5 ∈ x2.
Apply H7 with
x5,
∃ x6 . and (x6 ∈ x0) (x4 (x3 x6) = x5) leaving 2 subgoals.
The subproof is completed by applying H10.
Let x6 of type ι be given.
Assume H11:
(λ x7 . and (x7 ∈ x1) (x4 ... = ...)) ....