Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι → ι be given.
Apply H3 with
bij x1 x2 x3.
Assume H4: ∀ x4 . x4 ∈ x1 ⟶ x3 x4 ∈ x2.
Assume H5: ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Apply equip_sym with
x1,
x0,
bij x1 x2 x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι → ι be given.
Apply bijE with
x0,
x1,
x4,
bij x1 x2 x3 leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: ∀ x5 . x5 ∈ x0 ⟶ x4 x5 ∈ x1.
Assume H8: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Assume H9:
∀ x5 . x5 ∈ x1 ⟶ ∃ x6 . and (x6 ∈ x0) (x4 x6 = x5).
Apply H2 with
bij x1 x2 x3.
Let x5 of type ι → ι be given.
Assume H10:
bij x2 x0 x5.
Apply bijE with
x2,
x0,
x5,
bij x1 x2 x3 leaving 2 subgoals.
The subproof is completed by applying H10.
Assume H11: ∀ x6 . x6 ∈ x2 ⟶ x5 x6 ∈ x0.
Assume H12: ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ x5 x6 = x5 x7 ⟶ x6 = x7.
Assume H13:
∀ x6 . x6 ∈ x0 ⟶ ∃ x7 . and (x7 ∈ x2) (x5 x7 = x6).
Apply L15 with
bij x1 x2 x3.
Assume H16:
and (∀ x6 . x6 ∈ x0 ⟶ (λ x7 . x5 (x3 (x4 x7))) x6 ∈ x0) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ (λ x8 . x5 (x3 (x4 x8))) x6 = (λ x8 . x5 (x3 (x4 x8))) x7 ⟶ x6 = x7).
Assume H17:
∀ x6 . x6 ∈ x0 ⟶ ∃ x7 . and (x7 ∈ x0) ((λ x8 . x5 (x3 (x4 x8))) x7 = x6).
Apply bijI with
x1,
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Let x6 of type ι be given.
Assume H18: x6 ∈ x2.
Apply H17 with
x5 x6,
∃ x7 . and (x7 ∈ x1) (x3 x7 = x6) leaving 2 subgoals.
The subproof is completed by applying L19.
Let x7 of type ι be given.
Assume H20:
(λ x8 . and (x8 ∈ x0) (x5 (x3 (x4 x8)) = x5 x6)) x7.
Apply H20 with
∃ x8 . and (x8 ∈ x1) (x3 x8 = x6).
Assume H21: x7 ∈ x0.
Assume H22: x5 (x3 (x4 x7)) = x5 x6.
Let x8 of type ο be given.
Assume H23:
∀ x9 . and (x9 ∈ x1) (... = ...) ⟶ x8.