Metamath Proof Explorer


Theorem idressubmefmnd

Description: The singleton containing only the identity function restricted to a set is a submonoid of the monoid of endofunctions on this set. (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypothesis idressubmefmnd.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
Assertion idressubmefmnd ( 𝐴𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 idressubmefmnd.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 1 efmndid ( 𝐴𝑉 → ( I ↾ 𝐴 ) = ( 0g𝐺 ) )
3 2 sneqd ( 𝐴𝑉 → { ( I ↾ 𝐴 ) } = { ( 0g𝐺 ) } )
4 1 efmndmnd ( 𝐴𝑉𝐺 ∈ Mnd )
5 eqid ( 0g𝐺 ) = ( 0g𝐺 )
6 5 0subm ( 𝐺 ∈ Mnd → { ( 0g𝐺 ) } ∈ ( SubMnd ‘ 𝐺 ) )
7 4 6 syl ( 𝐴𝑉 → { ( 0g𝐺 ) } ∈ ( SubMnd ‘ 𝐺 ) )
8 3 7 eqeltrd ( 𝐴𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubMnd ‘ 𝐺 ) )