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

Metamath Proof Explorer

Theorem efmndbas0

Description: The base set of the monoid of endofunctions on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Jan-2024) (Proof shortened by AV, 31-Mar-2024)

		Ref	Expression
	Assertion	efmndbas0	⊢ ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = { ∅ }

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( EndoFMnd ‘ ∅ ) = ( EndoFMnd ‘ ∅ )
2		eqid	⊢ ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = ( Base ‘ ( EndoFMnd ‘ ∅ ) )
3	1 2	efmndbas	⊢ ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = ( ∅ ↑_m ∅ )
4		0map0sn0	⊢ ( ∅ ↑_m ∅ ) = { ∅ }
5	3 4	eqtri	⊢ ( Base ‘ ( EndoFMnd ‘ ∅ ) ) = { ∅ }