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	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	symgtrf.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	symgtrf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	symggen.k	⊢ 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
Assertion	symggen2	⊢ ( 𝐷 ∈ Fin → ( 𝐾 ‘ 𝑇 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		symgtrf.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
2		symgtrf.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
3		symgtrf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		symggen.k	⊢ 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) )
5	1 2 3 4	symggen	⊢ ( 𝐷 ∈ Fin → ( 𝐾 ‘ 𝑇 ) = { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
6		difss	⊢ ( 𝑥 ∖ I ) ⊆ 𝑥
7		dmss	⊢ ( ( 𝑥 ∖ I ) ⊆ 𝑥 → dom ( 𝑥 ∖ I ) ⊆ dom 𝑥 )
8	6 7	ax-mp	⊢ dom ( 𝑥 ∖ I ) ⊆ dom 𝑥
9	2 3	symgbasf1o	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 : 𝐷 –1-1-onto→ 𝐷 )
10		f1odm	⊢ ( 𝑥 : 𝐷 –1-1-onto→ 𝐷 → dom 𝑥 = 𝐷 )
11	9 10	syl	⊢ ( 𝑥 ∈ 𝐵 → dom 𝑥 = 𝐷 )
12	8 11	sseqtrid	⊢ ( 𝑥 ∈ 𝐵 → dom ( 𝑥 ∖ I ) ⊆ 𝐷 )
13		ssfi	⊢ ( ( 𝐷 ∈ Fin ∧ dom ( 𝑥 ∖ I ) ⊆ 𝐷 ) → dom ( 𝑥 ∖ I ) ∈ Fin )
14	12 13	sylan2	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑥 ∈ 𝐵 ) → dom ( 𝑥 ∖ I ) ∈ Fin )
15	14	ralrimiva	⊢ ( 𝐷 ∈ Fin → ∀ 𝑥 ∈ 𝐵 dom ( 𝑥 ∖ I ) ∈ Fin )
16		rabid2	⊢ ( 𝐵 = { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } ↔ ∀ 𝑥 ∈ 𝐵 dom ( 𝑥 ∖ I ) ∈ Fin )
17	15 16	sylibr	⊢ ( 𝐷 ∈ Fin → 𝐵 = { 𝑥 ∈ 𝐵 ∣ dom ( 𝑥 ∖ I ) ∈ Fin } )
18	5 17	eqtr4d	⊢ ( 𝐷 ∈ Fin → ( 𝐾 ‘ 𝑇 ) = 𝐵 )