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

Metamath Proof Explorer

Theorem nsmndex1

Description: The base set B of the constructed monoid S is not a submonoid of the monoid M of endofunctions on set NN0 , although M e. Mnd and S e. Mnd and B C_ ( BaseM ) hold. (Contributed by AV, 17-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 nsmndex1 
|- B e/ ( SubMnd ` M )

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 6 smndex1n0mnd 
 |-  ( 0g ` M ) e/ B
8 7 neli 
 |-  -. ( 0g ` M ) e. B
9 8 intnan 
 |-  -. ( B C_ ( Base ` M ) /\ ( 0g ` M ) e. B )
10 9 intnan 
 |-  -. ( ( M e. Mnd /\ ( M |`s B ) e. Mnd ) /\ ( B C_ ( Base ` M ) /\ ( 0g ` M ) e. B ) )
11 eqid 
 |-  ( Base ` M ) = ( Base ` M )
12 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
13 11 12 issubmndb 
 |-  ( B e. ( SubMnd ` M ) <-> ( ( M e. Mnd /\ ( M |`s B ) e. Mnd ) /\ ( B C_ ( Base ` M ) /\ ( 0g ` M ) e. B ) ) )
14 10 13 mtbir 
 |-  -. B e. ( SubMnd ` M )
15 14 nelir 
 |-  B e/ ( SubMnd ` M )