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	syl5eq	⊢ ( 𝐴 ∈ 𝑉 → 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )