Theorem smndex1bas

Description: The base set of the monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) . (Contributed by AV, 12-Feb-2024)

	Ref	Expression
Hypotheses	smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex1ibas.n	⊢ 𝑁 ∈ ℕ
	smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
	smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
	smndex1mgm.b	⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
	smndex1mgm.s	⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
Assertion	smndex1bas	⊢ ( Base ‘ 𝑆 ) = 𝐵

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex1ibas.n	⊢ 𝑁 ∈ ℕ
3		smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4		smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5		smndex1mgm.b	⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
6		smndex1mgm.s	⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
7	1 2 3 4 5	smndex1basss	⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
8		dfss	⊢ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) ↔ 𝐵 = ( 𝐵 ∩ ( Base ‘ 𝑀 ) ) )
9	7 8	mpbi	⊢ 𝐵 = ( 𝐵 ∩ ( Base ‘ 𝑀 ) )
10		snex	⊢ { 𝐼 } ∈ V
11		ovex	⊢ ( 0 ..^ 𝑁 ) ∈ V
12		snex	⊢ { ( 𝐺 ‘ 𝑛 ) } ∈ V
13	11 12	iunex	⊢ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ∈ V
14	10 13	unex	⊢ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ∈ V
15	5 14	eqeltri	⊢ 𝐵 ∈ V
16		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
17	6 16	ressbas	⊢ ( 𝐵 ∈ V → ( 𝐵 ∩ ( Base ‘ 𝑀 ) ) = ( Base ‘ 𝑆 ) )
18	15 17	ax-mp	⊢ ( 𝐵 ∩ ( Base ‘ 𝑀 ) ) = ( Base ‘ 𝑆 )
19	9 18	eqtr2i	⊢ ( Base ‘ 𝑆 ) = 𝐵