This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( ¬ 𝑋 ∈ V → ( 𝐴 = { 𝑋 } → ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) ) )
28 19 27 pm2.61i ⊢ ( 𝐴 = { 𝑋 } → ( EndoFMnd ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 ) )