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.
Let x5 of type ι → ι be given.
Apply bijE with
x2,
x3,
x5,
(∃ x6 . and (x6 ⊆ x2) (and (equip x0 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x4 (x5 x7) (x5 x8)))) ⟶ ∃ x6 . and (x6 ⊆ x3) (and (equip x1 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x4 x7 x8)) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: ∀ x6 . x6 ∈ x2 ⟶ x5 x6 ∈ x3.
Assume H3: ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ x5 x6 = x5 x7 ⟶ x6 = x7.
Assume H4:
∀ x6 . x6 ∈ x3 ⟶ ∃ x7 . and (x7 ∈ x2) (x5 x7 = x6).
Assume H5:
∃ x6 . and (x6 ⊆ x2) (and (equip x0 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x4 (x5 x7) (x5 x8))).
Apply H5 with
∃ x6 . and (x6 ⊆ x3) (and (equip x1 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x4 x7 x8)).
Let x6 of type ι be given.
Assume H6:
(λ x7 . and (x7 ⊆ x2) (and (equip x0 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x4 (x5 x8) (x5 x9)))) x6.
Apply H6 with
∃ x7 . and (x7 ⊆ x3) (and (equip x1 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x4 x8 x9)).
Assume H7: x6 ⊆ x2.
Assume H8:
and (equip x0 x6) (∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ (x7 = x8 ⟶ ∀ x9 : ο . x9) ⟶ x4 (x5 x7) (x5 x8)).
Apply H8 with
∃ x7 . and (x7 ⊆ x3) (and (equip x1 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x4 x8 x9)).
Assume H10: ∀ x7 . ... ⟶ ∀ x8 . ... ⟶ ... ⟶ x4 (x5 x7) (x5 x8).