Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply subgroup_E with
x0,
x1,
λ x3 x4 . subgroup x4 x2 ⟶ subgroup x3 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ι → ι be given.
Assume H1: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ∈ x4.
Assume H3: x3 ⊆ x4.
Apply subgroup_E with
pack_b x4 x5,
x2,
λ x6 x7 . pack_b x4 x5 = x6 ⟶ subgroup (pack_b x3 x5) x7 leaving 2 subgoals.
The subproof is completed by applying H4.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι → ι → ι be given.
Assume H5: ∀ x9 . x9 ∈ x7 ⟶ ∀ x10 . x10 ∈ x7 ⟶ x8 x9 x10 ∈ x7.
Assume H7: x6 ⊆ x7.
Apply pack_b_inj with
x4,
x6,
x5,
x8,
subgroup (pack_b x3 x5) (pack_b x7 x8) leaving 2 subgoals.
The subproof is completed by applying H8.
Assume H9: x4 = x6.
Assume H10: ∀ x9 . x9 ∈ x4 ⟶ ∀ x10 . x10 ∈ x4 ⟶ x5 x9 x10 = x8 x9 x10.
Claim L11: ∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ x5 x9 x10 ∈ x3
Apply GroupE with
x3,
x5,
∀ x9 . x9 ∈ x3 ⟶ ∀ x10 . x10 ∈ x3 ⟶ x5 x9 x10 ∈ x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H11:
and (∀ x9 . ... ⟶ ∀ x10 . ... ⟶ ... ∈ ...) ....
Apply pack_b_ext with
x3,
x5,
x8.
Let x9 of type ι be given.
Assume H12: x9 ∈ x3.
Let x10 of type ι be given.
Assume H13: x10 ∈ x3.
Apply H10 with
x9,
x10 leaving 2 subgoals.
Apply H3 with
x9.
The subproof is completed by applying H12.
Apply H3 with
x10.
The subproof is completed by applying H13.
Apply and3I with
struct_b (pack_b x7 x8),
struct_b (pack_b x3 x5),
unpack_b_o (pack_b x7 x8) (λ x9 . λ x10 : ι → ι → ι . unpack_b_o (pack_b x3 x5) (λ x11 . λ x12 : ι → ι → ι . and (and (pack_b x3 x5 = pack_b x11 x10) (Group (pack_b x11 x10))) (x11 ⊆ x9))) leaving 3 subgoals.
Apply pack_struct_b_I with
x7,
x8.
The subproof is completed by applying H5.
Apply pack_struct_b_I with
x3,
x5.
The subproof is completed by applying L11.
Apply unknownprop_673480a732b2360ba263db6ccd7aafefdf5ff6442062595c967c01560edd61e8 with
x3,
x7,
x5,
x8,
λ x9 x10 : ο . x10.
Apply and3I with
pack_b x3 x5 = pack_b x3 x8,
Group (pack_b x3 x8),
x3 ⊆ x7 leaving 3 subgoals.
The subproof is completed by applying L12.
Apply L12 with
λ x9 x10 . Group x9.
The subproof is completed by applying H2.
Let x9 of type ι be given.
Assume H13: x9 ∈ x3.
Apply H7 with
x9.
Apply H9 with
λ x10 x11 . x9 ∈ x10.
Apply H3 with
x9.
The subproof is completed by applying H13.
Apply L5.
Let x6 of type ι → ι → ο be given.
The subproof is completed by applying H6.