symg1bas

Description: The symmetric group on a singleton is the symmetric group S_1 consisting of the identity only. (Contributed by AV, 9-Dec-2018)

	Ref	Expression
Hypotheses	symg1bas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symg1bas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
	symg1bas.0	⊢ 𝐴 = { 𝐼 }
Assertion	symg1bas	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ } } )

Proof

Step	Hyp	Ref	Expression
1		symg1bas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symg1bas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		symg1bas.0	⊢ 𝐴 = { 𝐼 }
4	1 2	symgbas	⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
5		eqidd	⊢ ( 𝐴 = { 𝐼 } → 𝑝 = 𝑝 )
6		id	⊢ ( 𝐴 = { 𝐼 } → 𝐴 = { 𝐼 } )
7	5 6 6	f1oeq123d	⊢ ( 𝐴 = { 𝐼 } → ( 𝑝 : 𝐴 –1-1-onto→ 𝐴 ↔ 𝑝 : { 𝐼 } –1-1-onto→ { 𝐼 } ) )
8	3 7	ax-mp	⊢ ( 𝑝 : 𝐴 –1-1-onto→ 𝐴 ↔ 𝑝 : { 𝐼 } –1-1-onto→ { 𝐼 } )
9		f1of	⊢ ( 𝑝 : { 𝐼 } –1-1-onto→ { 𝐼 } → 𝑝 : { 𝐼 } ⟶ { 𝐼 } )
10		fsng	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) → ( 𝑝 : { 𝐼 } ⟶ { 𝐼 } ↔ 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
11	10	anidms	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑝 : { 𝐼 } ⟶ { 𝐼 } ↔ 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
12	9 11	imbitrid	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑝 : { 𝐼 } –1-1-onto→ { 𝐼 } → 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
13		f1osng	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉 ) → { ⟨ 𝐼 , 𝐼 ⟩ } : { 𝐼 } –1-1-onto→ { 𝐼 } )
14	13	anidms	⊢ ( 𝐼 ∈ 𝑉 → { ⟨ 𝐼 , 𝐼 ⟩ } : { 𝐼 } –1-1-onto→ { 𝐼 } )
15		f1oeq1	⊢ ( 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } → ( 𝑝 : { 𝐼 } –1-1-onto→ { 𝐼 } ↔ { ⟨ 𝐼 , 𝐼 ⟩ } : { 𝐼 } –1-1-onto→ { 𝐼 } ) )
16	14 15	syl5ibrcom	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } → 𝑝 : { 𝐼 } –1-1-onto→ { 𝐼 } ) )
17	12 16	impbid	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑝 : { 𝐼 } –1-1-onto→ { 𝐼 } ↔ 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
18	8 17	bitrid	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑝 : 𝐴 –1-1-onto→ 𝐴 ↔ 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
19		vex	⊢ 𝑝 ∈ V
20		f1oeq1	⊢ ( 𝑓 = 𝑝 → ( 𝑓 : 𝐴 –1-1-onto→ 𝐴 ↔ 𝑝 : 𝐴 –1-1-onto→ 𝐴 ) )
21	19 20	elab	⊢ ( 𝑝 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ↔ 𝑝 : 𝐴 –1-1-onto→ 𝐴 )
22		velsn	⊢ ( 𝑝 ∈ { { ⟨ 𝐼 , 𝐼 ⟩ } } ↔ 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } )
23	18 21 22	3bitr4g	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑝 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ↔ 𝑝 ∈ { { ⟨ 𝐼 , 𝐼 ⟩ } } ) )
24	23	eqrdv	⊢ ( 𝐼 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } = { { ⟨ 𝐼 , 𝐼 ⟩ } } )
25	4 24	eqtrid	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ } } )

Metamath Proof Explorer

Theorem symg1bas

Proof