Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: x1 ⊆ x0.

Apply explicit_subgroup_symgroup_fixing with x0, x1, Group (pack_b {x2 ∈ setexp x0 x0|and (bij x0 x0 (λ x3 . ap x2 x3)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)))) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: Group (pack_b {x2 ∈ setexp x0 x0|and (bij x0 x0 (ap x2)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)))).

Assume H2: {x2 ∈ setexp x0 x0|and (bij x0 x0 (ap x2)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)} ⊆ {x2 ∈ setexp x0 x0|bij x0 x0 (ap x2)}.

The subproof is completed by applying H1.

■

Proofgold Proof