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 𝐴 )

Metamath Proof Explorer

Theorem efmndbas

Proof