Metamath Proof Explorer


Theorem efmndbas

Description: The base set of the monoid of endofunctions on class A . (Contributed by AV, 25-Jan-2024)

Ref Expression
Hypotheses efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
Assertion efmndbas 𝐵 = ( 𝐴m 𝐴 )

Proof

Step Hyp Ref Expression
1 efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
3 ovex ( 𝐴m 𝐴 ) ∈ V
4 eqid { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ }
5 4 topgrpbas ( ( 𝐴m 𝐴 ) ∈ V → ( 𝐴m 𝐴 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
6 3 5 mp1i ( 𝐴 ∈ V → ( 𝐴m 𝐴 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
7 eqid ( 𝐴m 𝐴 ) = ( 𝐴m 𝐴 )
8 eqid ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) = ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) )
9 eqid ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
10 1 7 8 9 efmnd ( 𝐴 ∈ V → 𝐺 = { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } )
11 10 fveq2d ( 𝐴 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
12 6 11 eqtr4d ( 𝐴 ∈ V → ( 𝐴m 𝐴 ) = ( Base ‘ 𝐺 ) )
13 base0 ∅ = ( Base ‘ ∅ )
14 reldmmap Rel dom ↑m
15 14 ovprc1 ( ¬ 𝐴 ∈ V → ( 𝐴m 𝐴 ) = ∅ )
16 fvprc ( ¬ 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = ∅ )
17 1 16 eqtrid ( ¬ 𝐴 ∈ V → 𝐺 = ∅ )
18 17 fveq2d ( ¬ 𝐴 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) )
19 13 15 18 3eqtr4a ( ¬ 𝐴 ∈ V → ( 𝐴m 𝐴 ) = ( Base ‘ 𝐺 ) )
20 12 19 pm2.61i ( 𝐴m 𝐴 ) = ( Base ‘ 𝐺 )
21 2 20 eqtr4i 𝐵 = ( 𝐴m 𝐴 )