Metamath Proof Explorer


Theorem efmndbasabf

Description: The base set of the monoid of endofunctions on class A is the set of functions from A into itself. (Contributed by AV, 29-Mar-2024)

Ref Expression
Hypotheses efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
Assertion efmndbasabf 𝐵 = { 𝑓𝑓 : 𝐴𝐴 }

Proof

Step Hyp Ref Expression
1 efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
3 1 2 efmndbas 𝐵 = ( 𝐴m 𝐴 )
4 mapvalg ( ( 𝐴 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐴m 𝐴 ) = { 𝑓𝑓 : 𝐴𝐴 } )
5 4 anidms ( 𝐴 ∈ V → ( 𝐴m 𝐴 ) = { 𝑓𝑓 : 𝐴𝐴 } )
6 3 5 eqtrid ( 𝐴 ∈ V → 𝐵 = { 𝑓𝑓 : 𝐴𝐴 } )
7 base0 ∅ = ( Base ‘ ∅ )
8 7 eqcomi ( Base ‘ ∅ ) = ∅
9 fvprc ( ¬ 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = ∅ )
10 1 9 eqtrid ( ¬ 𝐴 ∈ V → 𝐺 = ∅ )
11 10 fveq2d ( ¬ 𝐴 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) )
12 2 11 eqtrid ( ¬ 𝐴 ∈ V → 𝐵 = ( Base ‘ ∅ ) )
13 mapprc ( ¬ 𝐴 ∈ V → { 𝑓𝑓 : 𝐴𝐴 } = ∅ )
14 8 12 13 3eqtr4a ( ¬ 𝐴 ∈ V → 𝐵 = { 𝑓𝑓 : 𝐴𝐴 } )
15 6 14 pm2.61i 𝐵 = { 𝑓𝑓 : 𝐴𝐴 }