Metamath Proof Explorer


Theorem efmnd1bas

Description: The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024)

Ref Expression
Hypotheses efmnd1bas.1 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmnd1bas.2 𝐵 = ( Base ‘ 𝐺 )
efmnd1bas.0 𝐴 = { 𝐼 }
Assertion efmnd1bas ( 𝐼𝑉𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ } } )

Proof

Step Hyp Ref Expression
1 efmnd1bas.1 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmnd1bas.2 𝐵 = ( Base ‘ 𝐺 )
3 efmnd1bas.0 𝐴 = { 𝐼 }
4 3 fveq2i ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ { 𝐼 } )
5 1 4 eqtri 𝐺 = ( EndoFMnd ‘ { 𝐼 } )
6 5 2 efmndbas 𝐵 = ( { 𝐼 } ↑m { 𝐼 } )
7 fsng ( ( 𝐼𝑉𝐼𝑉 ) → ( 𝑝 : { 𝐼 } ⟶ { 𝐼 } ↔ 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
8 7 anidms ( 𝐼𝑉 → ( 𝑝 : { 𝐼 } ⟶ { 𝐼 } ↔ 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
9 snex { 𝐼 } ∈ V
10 9 9 elmap ( 𝑝 ∈ ( { 𝐼 } ↑m { 𝐼 } ) ↔ 𝑝 : { 𝐼 } ⟶ { 𝐼 } )
11 velsn ( 𝑝 ∈ { { ⟨ 𝐼 , 𝐼 ⟩ } } ↔ 𝑝 = { ⟨ 𝐼 , 𝐼 ⟩ } )
12 8 10 11 3bitr4g ( 𝐼𝑉 → ( 𝑝 ∈ ( { 𝐼 } ↑m { 𝐼 } ) ↔ 𝑝 ∈ { { ⟨ 𝐼 , 𝐼 ⟩ } } ) )
13 12 eqrdv ( 𝐼𝑉 → ( { 𝐼 } ↑m { 𝐼 } ) = { { ⟨ 𝐼 , 𝐼 ⟩ } } )
14 6 13 syl5eq ( 𝐼𝑉𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ } } )