Proofgold Proposition

∀ x0 x1 . x1 ⊆ x0 ⟶ explicit_subgroup {x2 ∈ setexp x0 x0|bij x0 x0 (ap x2)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4))) {x2 ∈ setexp x0 x0|and (bij x0 x0 (ap x2)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)}

type
prop

theory
HotG

name
explicit_subgroup_symgroup_fixing

proof
PUMaE..

Megalodon
explicit_subgroup_symgroup_fixing

proofgold address
TMQPa..^{explicit_subgroup_symgroup_fixing}

creator
4924 Pr6Pc../ede8a..

owner
4924 Pr6Pc../ede8a..

term root
bbace..