Claim L1:
∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ 127dd.. x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ 127dd.. x2 x3 ⟶ ∀ x4 x5 . MagmaHom (pack_b x0 x1) (pack_b x2 x3) x4 ⟶ MagmaHom (pack_b x0 x1) (pack_b x2 x3) x5 ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ {x8 ∈ x0|ap x4 x8 = ap x5 x8} ⟶ ∀ x8 . x8 ∈ {x9 ∈ x0|ap x4 x9 = ap x5 x9} ⟶ x1 x7 x8 = x6 x7 x8) ⟶ 127dd.. {x7 ∈ x0|ap x4 x7 = ap x5 x7} x6Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Assume H1: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Assume H3: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι → ι → ι be given.
Assume H7:
∀ x7 . x7 ∈ {x8 ∈ x0|ap x4 x8 = ap x5 x8} ⟶ ∀ x8 . x8 ∈ {x9 ∈ x0|ap x4 x9 = ap x5 x9} ⟶ x1 x7 x8 = x6 x7 x8.
Apply H2 with
127dd.. {x7 ∈ x0|ap x4 x7 = ap x5 x7} x6.
Apply H4 with
127dd.. {x7 ∈ x0|ap x4 x7 = ap x5 x7} x6.
Apply andI with
explicit_Group {x7 ∈ x0|ap x4 x7 = ap x5 x7} x6,
explicit_abelian {x7 ∈ x0|ap x4 x7 = ap x5 x7} x6 leaving 2 subgoals.
Apply unknownprop_25b39f95acc38e90496ee4808ab1a128bdb11a29e9c4569e1287049e660c9b38 with
x0,
x1,
x2,
x3,
x4,
x5,
x6 leaving 7 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H8.
The subproof is completed by applying H3.
The subproof is completed by applying H10.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Let x7 of type ι be given.
Assume H12:
x7 ∈ {x8 ∈ x0|ap x4 x8 = ap x5 x8}.
Let x8 of type ι be given.
Assume H13:
x8 ∈ {x9 ∈ x0|ap x4 x9 = ap ... ...}.
Apply unknownprop_cffd5c2c6377c7c9139709f837f7b00ba99be51fbf6add4c20b3723106916eaa with
127dd.. leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.