Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ⊆ x0.
Let x2 of type ι be given.
Assume H5:
x2 ∈ {x3 ∈ setexp x0 x0|and (bij x0 x0 (λ x4 . ap x3 x4)) (∀ x4 . x4 ∈ x1 ⟶ ap x3 x4 = x4)}.
Apply explicit_Group_symgroup_inv_eq with
x0,
x2,
λ x3 x4 . ... leaving 2 subgoals.
Claim L6:
∀ x2 . x2 ∈ {x3 ∈ setexp x0 x0|and (bij x0 x0 (λ x4 . ap x3 x4)) (∀ x4 . x4 ∈ x1 ⟶ ap x3 x4 = x4)} ⟶ ∀ x3 . x3 ∈ {x4 ∈ setexp x0 x0|and (bij x0 x0 (λ x5 . ap x4 x5)) (∀ x5 . x5 ∈ x1 ⟶ ap x4 x5 = x5)} ⟶ lam x0 (λ x4 . ap x3 (ap x2 x4)) ∈ {x4 ∈ setexp x0 x0|and (bij x0 x0 (λ x5 . ap x4 x5)) (∀ x5 . x5 ∈ x1 ⟶ ap x4 x5 = x5)}Apply unknownprop_84ca4ed305d5b4e27ce2e93e41baee1fcbe8346e3121687514bb4244ad3fd62a with
x0,
x1.
The subproof is completed by applying H0.
Apply GroupI with
{x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)},
λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)).
The subproof is completed by applying explicit_Group_symgroup with x0.
Apply explicit_subgroup_test with
{x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)},
λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)),
{x2 ∈ setexp x0 x0|and (bij x0 x0 (λ x3 . ap x2 x3)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)} leaving 5 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L1.
The subproof is completed by applying L3.
The subproof is completed by applying L5.
The subproof is completed by applying L6.