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

Metamath Proof Explorer

Theorem 0symgefmndeq

Description: The symmetric group on the empty set is identical with the monoid of endofunctions on the empty set. (Contributed by AV, 30-Mar-2024)

Ref Expression
Assertion 0symgefmndeq ( EndoFMnd ‘ ∅ ) = ( SymGrp ‘ ∅ )

Proof

Step Hyp Ref Expression
1 ssid ⊢ { ∅ } ⊆ { ∅ }
2 fvex ⊢ ( EndoFMnd ‘ ∅ ) ∈ V
3 p0ex ⊢ { ∅ } ∈ V
4 eqid ⊢ ( SymGrp ‘ ∅ ) = ( SymGrp ‘ ∅ )
5 symgbas0 ⊢ ( Base ‘ ( SymGrp ‘ ∅ ) ) = { ∅ }
6 5 eqcomi ⊢ { ∅ } = ( Base ‘ ( SymGrp ‘ ∅ ) )
7 eqid ⊢ ( EndoFMnd ‘ ∅ ) = ( EndoFMnd ‘ ∅ )
8 4 6 7 symgressbas ⊢ ( SymGrp ‘ ∅ ) = ( ( EndoFMnd ‘ ∅ ) ↾s { ∅ } )
9 efmndbas0 ⊢ ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = { ∅ }
10 9 eqcomi ⊢ { ∅ } = ( Base ‘ ( EndoFMnd ‘ ∅ ) )
11 8 10 ressid2 ⊢ ( ( { ∅ } ⊆ { ∅ } ∧ ( EndoFMnd ‘ ∅ ) ∈ V ∧ { ∅ } ∈ V ) → ( SymGrp ‘ ∅ ) = ( EndoFMnd ‘ ∅ ) )
12 1 2 3 11 mp3an ⊢ ( SymGrp ‘ ∅ ) = ( EndoFMnd ‘ ∅ )
13 12 eqcomi ⊢ ( EndoFMnd ‘ ∅ ) = ( SymGrp ‘ ∅ )