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 )