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