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	No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
	smndex1ibas.n	$$⊢N\in \mathbb{N}$$
	smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
	smndex1ibas.g	$$⊢G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
	smndex1mgm.b	$$⊢B=\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}$$
	smndex1mgm.s	$$⊢S=M{\upharpoonright }_{𝑠}B$$
Assertion	nsmndex1	$$⊢B\notin \mathrm{SubMnd}\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	Could not format M = ( EndoFMnd ` NN0 ) : No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
2		smndex1ibas.n	$$⊢N\in \mathbb{N}$$
3		smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
4		smndex1ibas.g	$$⊢G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
5		smndex1mgm.b	$$⊢B=\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}$$
6		smndex1mgm.s	$$⊢S=M{\upharpoonright }_{𝑠}B$$
7	1 2 3 4 5 6	smndex1n0mnd	$$⊢0_M\notin B$$
8	7	neli	$$⊢\neg 0_M\in B$$
9	8	intnan	$$⊢\neg \left(B\subseteq {\mathrm{Base}}_M\wedge 0_M\in B\right)$$
10	9	intnan	$$⊢\neg \left(\left(M\in \mathrm{Mnd}\wedge M{\upharpoonright }_{𝑠}B\in \mathrm{Mnd}\right)\wedge \left(B\subseteq {\mathrm{Base}}_M\wedge 0_M\in B\right)\right)$$
11		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
12		eqid	$$⊢0_M=0_M$$
13	11 12	issubmndb	$$⊢B\in \mathrm{SubMnd}\left(M\right)\leftrightarrow \left(\left(M\in \mathrm{Mnd}\wedge M{\upharpoonright }_{𝑠}B\in \mathrm{Mnd}\right)\wedge \left(B\subseteq {\mathrm{Base}}_M\wedge 0_M\in B\right)\right)$$
14	10 13	mtbir	$$⊢\neg B\in \mathrm{SubMnd}\left(M\right)$$
15	14	nelir	$$⊢B\notin \mathrm{SubMnd}\left(M\right)$$