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	|- M = ( EndoFMnd ` NN0 )
	smndex1ibas.n	|- N e. NN
	smndex1ibas.i	|- I = ( x e. NN0 |-> ( x mod N ) )
	smndex1ibas.g	|- G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
	smndex1mgm.b	|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
	smndex1mgm.s	|- S = ( M |`s B )
Assertion	smndex1bas	|- ( Base ` S ) = B

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	|- M = ( EndoFMnd ` NN0 )
2		smndex1ibas.n	|- N e. NN
3		smndex1ibas.i	|- I = ( x e. NN0 |-> ( x mod N ) )
4		smndex1ibas.g	|- G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
5		smndex1mgm.b	|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
6		smndex1mgm.s	|- S = ( M |`s B )
7	1 2 3 4 5	smndex1basss	|- B C_ ( Base ` M )
8		dfss	|- ( B C_ ( Base ` M ) <-> B = ( B i^i ( Base ` M ) ) )
9	7 8	mpbi	|- B = ( B i^i ( Base ` M ) )
10		snex	|- { I } e. _V
11		ovex	|- ( 0 ..^ N ) e. _V
12		snex	|- { ( G ` n ) } e. _V
13	11 12	iunex	|- U_ n e. ( 0 ..^ N ) { ( G ` n ) } e. _V
14	10 13	unex	|- ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) e. _V
15	5 14	eqeltri	|- B e. _V
16		eqid	|- ( Base ` M ) = ( Base ` M )
17	6 16	ressbas	|- ( B e. _V -> ( B i^i ( Base ` M ) ) = ( Base ` S ) )
18	15 17	ax-mp	|- ( B i^i ( Base ` M ) ) = ( Base ` S )
19	9 18	eqtr2i	|- ( Base ` S ) = B