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 ‘ ∅ )