This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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