Metamath Proof Explorer

Theorem symggen2

Description: A finite permutation group is generated by the transpositions, see also Theorem 3.4 in Rotman p. 31. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses symgtrf.t ⊢ T = ran ⁡ pmTrsp ⁡ D
symgtrf.g ⊢ G = SymGrp ⁡ D
symgtrf.b ⊢ B = Base G
symggen.k ⊢ K = mrCls ⁡ SubMnd ⁡ G
Assertion symggen2 ⊢ D ∈ Fin → K ⁡ T = B

Proof

Step Hyp Ref Expression
1 symgtrf.t ⊢ T = ran ⁡ pmTrsp ⁡ D
2 symgtrf.g ⊢ G = SymGrp ⁡ D
3 symgtrf.b ⊢ B = Base G
4 symggen.k ⊢ K = mrCls ⁡ SubMnd ⁡ G
5 1 2 3 4 symggen ⊢ D ∈ Fin → K ⁡ T = x ∈ B | dom ⁡ x ∖ I ∈ Fin
6 difss ⊢ x ∖ I ⊆ x
7 dmss ⊢ x ∖ I ⊆ x → dom ⁡ x ∖ I ⊆ dom ⁡ x
8 6 7 ax-mp ⊢ dom ⁡ x ∖ I ⊆ dom ⁡ x
9 2 3 symgbasf1o ⊢ x ∈ B → x : D ⟶ 1-1 onto D
10 f1odm ⊢ x : D ⟶ 1-1 onto D → dom ⁡ x = D
11 9 10 syl ⊢ x ∈ B → dom ⁡ x = D
12 8 11 sseqtrid ⊢ x ∈ B → dom ⁡ x ∖ I ⊆ D
13 ssfi ⊢ D ∈ Fin ∧ dom ⁡ x ∖ I ⊆ D → dom ⁡ x ∖ I ∈ Fin
14 12 13 sylan2 ⊢ D ∈ Fin ∧ x ∈ B → dom ⁡ x ∖ I ∈ Fin
15 14 ralrimiva ⊢ D ∈ Fin → ∀ x ∈ B dom ⁡ x ∖ I ∈ Fin
16 rabid2 ⊢ B = x ∈ B | dom ⁡ x ∖ I ∈ Fin ↔ ∀ x ∈ B dom ⁡ x ∖ I ∈ Fin
17 15 16 sylibr ⊢ D ∈ Fin → B = x ∈ B | dom ⁡ x ∖ I ∈ Fin
18 5 17 eqtr4d ⊢ D ∈ Fin → K ⁡ T = B