Metamath Proof Explorer


Theorem efmnd

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

Ref Expression
Hypotheses efmnd.1 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmnd.2 𝐵 = ( 𝐴m 𝐴 )
efmnd.3 + = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓𝑔 ) )
efmnd.4 𝐽 = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
Assertion efmnd ( 𝐴𝑉𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )

Proof

Step Hyp Ref Expression
1 efmnd.1 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmnd.2 𝐵 = ( 𝐴m 𝐴 )
3 efmnd.3 + = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓𝑔 ) )
4 efmnd.4 𝐽 = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
5 elex ( 𝐴𝑉𝐴 ∈ V )
6 ovexd ( 𝑎 = 𝐴 → ( 𝑎m 𝑎 ) ∈ V )
7 id ( 𝑏 = ( 𝑎m 𝑎 ) → 𝑏 = ( 𝑎m 𝑎 ) )
8 id ( 𝑎 = 𝐴𝑎 = 𝐴 )
9 8 8 oveq12d ( 𝑎 = 𝐴 → ( 𝑎m 𝑎 ) = ( 𝐴m 𝐴 ) )
10 9 2 eqtr4di ( 𝑎 = 𝐴 → ( 𝑎m 𝑎 ) = 𝐵 )
11 7 10 sylan9eqr ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → 𝑏 = 𝐵 )
12 11 opeq2d ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
13 eqidd ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ( 𝑓𝑔 ) = ( 𝑓𝑔 ) )
14 11 11 13 mpoeq123dv ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑓𝑔 ) ) )
15 14 3 eqtr4di ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) = + )
16 15 opeq2d ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , + ⟩ )
17 simpl ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → 𝑎 = 𝐴 )
18 pweq ( 𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴 )
19 18 sneqd ( 𝑎 = 𝐴 → { 𝒫 𝑎 } = { 𝒫 𝐴 } )
20 19 adantr ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → { 𝒫 𝑎 } = { 𝒫 𝐴 } )
21 17 20 xpeq12d ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ( 𝑎 × { 𝒫 𝑎 } ) = ( 𝐴 × { 𝒫 𝐴 } ) )
22 21 fveq2d ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) )
23 22 4 eqtr4di ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) = 𝐽 )
24 23 opeq2d ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) ⟩ = ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ )
25 12 16 24 tpeq123d ( ( 𝑎 = 𝐴𝑏 = ( 𝑎m 𝑎 ) ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
26 6 25 csbied ( 𝑎 = 𝐴 ( 𝑎m 𝑎 ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
27 df-efmnd EndoFMnd = ( 𝑎 ∈ V ↦ ( 𝑎m 𝑎 ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑎 × { 𝒫 𝑎 } ) ) ⟩ } )
28 tpex { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∈ V
29 26 27 28 fvmpt ( 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
30 5 29 syl ( 𝐴𝑉 → ( EndoFMnd ‘ 𝐴 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
31 1 30 eqtrid ( 𝐴𝑉𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )