Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι be given.
Assume H1: x2 ⊆ x0.
Assume H4: ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ x1 x3 x4 ∈ x2.
Apply L5 with
explicit_subgroup x0 x1 x2.
Assume H6:
and (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 ∈ x0) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5).
Assume H7:
∃ x3 . and (x3 ∈ x0) (and (∀ x4 . x4 ∈ x0 ⟶ and (x1 x3 x4 = x4) (x1 x4 x3 = x4)) (∀ x4 . x4 ∈ x0 ⟶ ∃ x5 . and (x5 ∈ x0) (and (x1 x4 x5 = x3) (x1 x5 x4 = x3)))).
Apply H6 with
explicit_subgroup x0 x1 x2.
Assume H8: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 ∈ x0.
Assume H9: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5.
Apply andI with
Group (pack_b x2 x1),
x2 ⊆ x0 leaving 2 subgoals.
Apply GroupI with
x2,
x1.
Apply and3I with
∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ x1 x3 x4 ∈ x2,
∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5,
∃ x3 . and (x3 ∈ x2) (and (∀ x4 . x4 ∈ x2 ⟶ and (x1 x3 x4 = x4) (x1 x4 x3 = x4)) (∀ x4 . x4 ∈ x2 ⟶ ∃ x5 . and (x5 ∈ x2) (and (x1 x4 x5 = x3) (x1 x5 x4 = x3)))) leaving 3 subgoals.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Assume H10: x3 ∈ x2.
Let x4 of type ι be given.
Assume H11: x4 ∈ x2.
Let x5 of type ι be given.
Assume H12: x5 ∈ x2.
Apply H9 with
x3,
x4,
x5 leaving 3 subgoals.
Apply H1 with
x3.
The subproof is completed by applying H10.
Apply H1 with
x4.
The subproof is completed by applying H11.
Apply H1 with
x5.
The subproof is completed by applying H12.
Let x3 of type ο be given.
Assume H10:
∀ x4 . and (x4 ∈ ...) ... ⟶ x3.