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

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 ) , 𝐽 ⟩ } )