efmndtset

Description: The topology of the monoid of endofunctions on A . This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just endofunctions - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by AV, 25-Jan-2024)

		Ref	Expression
	Hypothesis	efmndtset.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
	Assertion	efmndtset	⊢ ( 𝐴 ∈ 𝑉 → ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		efmndtset.g	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2		fvex	⊢ ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ V
3		eqid	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝐴 ↑_m 𝐴 ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 𝐴 ↑_m 𝐴 ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ }
4	3	topgrptset	⊢ ( ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ V → ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴 ↑_m 𝐴 ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
5	2 4	ax-mp	⊢ ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴 ↑_m 𝐴 ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } )
6		eqid	⊢ ( 𝐴 ↑_m 𝐴 ) = ( 𝐴 ↑_m 𝐴 )
7		eqid	⊢ ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) )
8		eqid	⊢ ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
9	1 6 7 8	efmnd	⊢ ( 𝐴 ∈ 𝑉 → 𝐺 = { ⟨ ( Base ‘ ndx ) , ( 𝐴 ↑_m 𝐴 ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } )
10	9	fveq2d	⊢ ( 𝐴 ∈ 𝑉 → ( TopSet ‘ 𝐺 ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴 ↑_m 𝐴 ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
11	5 10	eqtr4id	⊢ ( 𝐴 ∈ 𝑉 → ( ∏_t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem efmndtset

Proof