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

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 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → 𝐵 = { { ⟨ 𝐼 , 𝐼 ⟩ } } )