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

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 ⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐴 }