Let x0 of type ο be given.
Apply H1 with
symgroup_fixing 3 1.
Let x1 of type ο be given.
Apply H2 with
symgroup 3.
Apply and3I with
Group (symgroup 3),
subgroup (symgroup_fixing 3 1) (symgroup 3),
not (normal_subgroup (symgroup_fixing 3 1) (symgroup 3)) leaving 3 subgoals.
The subproof is completed by applying L3.
Apply subgroup_symgroup_fixing with
3,
1.
The subproof is completed by applying L0.
Apply H5 with
False.
Apply unknownprop_a38119175a5c7a068cd247f906b2f1feb5daeb7691af95918cb490283a35a18e with
{x2 ∈ setexp 3 3|and (bij 3 3 (λ x3 . ap x2 x3)) (∀ x3 . x3 ∈ 1 ⟶ ap x2 x3 = x3)},
{x2 ∈ setexp 3 3|bij 3 3 (λ x3 . ap x2 x3)},
λ x2 x3 . lam 3 (λ x4 . ap x3 (ap x2 x4)),
λ x2 x3 . lam 3 (λ x4 . ap x3 (ap x2 x4)),
λ x2 x3 : ο . x3 ⟶ False leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Assume H7:
∀ x2 . ... ⟶ {(λ x4 x5 . lam 3 (λ x6 . ap x5 (ap x4 x6))) x2 ((λ x4 x5 . lam 3 (λ x6 . ap x5 (ap x4 x6))) ... ...)|x3 ∈ {x3 ∈ setexp 3 3|and (bij 3 3 (λ x4 . ap x3 x4)) (∀ x4 . x4 ∈ 1 ⟶ ap x3 x4 = x4)}} ⊆ ....