Theorem snsymgefmndeq

Description: The symmetric group on a singleton A is identical with the monoid of endofunctions on A . (Contributed by AV, 31-Mar-2024)

	Ref	Expression
Assertion	snsymgefmndeq	⊢ ( 𝐴 = { 𝑋 } → ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ssidd	⊢ ( 𝑋 ∈ V → { { ⟨ 𝑋 , 𝑋 ⟩ } } ⊆ { { ⟨ 𝑋 , 𝑋 ⟩ } } )
2		eqid	⊢ ( EndoFMnd ‘ { 𝑋 } ) = ( EndoFMnd ‘ { 𝑋 } )
3		eqid	⊢ ( Base ‘ ( EndoFMnd ‘ { 𝑋 } ) ) = ( Base ‘ ( EndoFMnd ‘ { 𝑋 } ) )
4		eqid	⊢ { 𝑋 } = { 𝑋 }
5	2 3 4	efmnd1bas	⊢ ( 𝑋 ∈ V → ( Base ‘ ( EndoFMnd ‘ { 𝑋 } ) ) = { { ⟨ 𝑋 , 𝑋 ⟩ } } )
6		eqid	⊢ ( SymGrp ‘ { 𝑋 } ) = ( SymGrp ‘ { 𝑋 } )
7		eqid	⊢ ( Base ‘ ( SymGrp ‘ { 𝑋 } ) ) = ( Base ‘ ( SymGrp ‘ { 𝑋 } ) )
8	6 7 4	symg1bas	⊢ ( 𝑋 ∈ V → ( Base ‘ ( SymGrp ‘ { 𝑋 } ) ) = { { ⟨ 𝑋 , 𝑋 ⟩ } } )
9	1 5 8	3sstr4d	⊢ ( 𝑋 ∈ V → ( Base ‘ ( EndoFMnd ‘ { 𝑋 } ) ) ⊆ ( Base ‘ ( SymGrp ‘ { 𝑋 } ) ) )
10		fvexd	⊢ ( 𝑋 ∈ V → ( EndoFMnd ‘ { 𝑋 } ) ∈ V )
11		fvexd	⊢ ( 𝑋 ∈ V → ( Base ‘ ( SymGrp ‘ { 𝑋 } ) ) ∈ V )
12	6 7 2	symgressbas	⊢ ( SymGrp ‘ { 𝑋 } ) = ( ( EndoFMnd ‘ { 𝑋 } ) ↾s ( Base ‘ ( SymGrp ‘ { 𝑋 } ) ) )
13	12 3	ressid2	⊢ ( ( ( Base ‘ ( EndoFMnd ‘ { 𝑋 } ) ) ⊆ ( Base ‘ ( SymGrp ‘ { 𝑋 } ) ) ∧ ( EndoFMnd ‘ { 𝑋 } ) ∈ V ∧ ( Base ‘ ( SymGrp ‘ { 𝑋 } ) ) ∈ V ) → ( SymGrp ‘ { 𝑋 } ) = ( EndoFMnd ‘ { 𝑋 } ) )
14	9 10 11 13	syl3anc	⊢ ( 𝑋 ∈ V → ( SymGrp ‘ { 𝑋 } ) = ( EndoFMnd ‘ { 𝑋 } ) )
15	14	eqcomd	⊢ ( 𝑋 ∈ V → ( EndoFMnd ‘ { 𝑋 } ) = ( SymGrp ‘ { 𝑋 } ) )
16		fveq2	⊢ ( 𝐴 = { 𝑋 } → ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ { 𝑋 } ) )
17		fveq2	⊢ ( 𝐴 = { 𝑋 } → ( SymGrp ‘ 𝐴 ) = ( SymGrp ‘ { 𝑋 } ) )
18	16 17	eqeq12d	⊢ ( 𝐴 = { 𝑋 } → ( ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) ↔ ( EndoFMnd ‘ { 𝑋 } ) = ( SymGrp ‘ { 𝑋 } ) ) )
19	15 18	syl5ibrcom	⊢ ( 𝑋 ∈ V → ( 𝐴 = { 𝑋 } → ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) ) )
20		snprc	⊢ ( ¬ 𝑋 ∈ V ↔ { 𝑋 } = ∅ )
21	20	biimpi	⊢ ( ¬ 𝑋 ∈ V → { 𝑋 } = ∅ )
22	21	eqeq2d	⊢ ( ¬ 𝑋 ∈ V → ( 𝐴 = { 𝑋 } ↔ 𝐴 = ∅ ) )
23		0symgefmndeq	⊢ ( EndoFMnd ‘ ∅ ) = ( SymGrp ‘ ∅ )
24		fveq2	⊢ ( 𝐴 = ∅ → ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ ∅ ) )
25		fveq2	⊢ ( 𝐴 = ∅ → ( SymGrp ‘ 𝐴 ) = ( SymGrp ‘ ∅ ) )
26	23 24 25	3eqtr4a	⊢ ( 𝐴 = ∅ → ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) )
27	22 26	syl6bi	⊢ ( ¬ 𝑋 ∈ V → ( 𝐴 = { 𝑋 } → ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) ) )
28	19 27	pm2.61i	⊢ ( 𝐴 = { 𝑋 } → ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) )