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	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	smndex1bas	$$⊢{\mathrm{Base}}_S=B$$

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	smndex1basss	$$⊢B\subseteq {\mathrm{Base}}_M$$
8		dfss	$$⊢B\subseteq {\mathrm{Base}}_M\leftrightarrow B=B\cap {\mathrm{Base}}_M$$
9	7 8	mpbi	$$⊢B=B\cap {\mathrm{Base}}_M$$
10		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
11		ovex	$$⊢\left(0..^N\right)\in \mathrm{V}$$
12		snex	$$⊢\left\{G\left(n\right)\right\}\in \mathrm{V}$$
13	11 12	iunex	$$⊢\bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\in \mathrm{V}$$
14	10 13	unex	$$⊢\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\in \mathrm{V}$$
15	5 14	eqeltri	$$⊢B\in \mathrm{V}$$
16		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
17	6 16	ressbas	$$⊢B\in \mathrm{V}\to B\cap {\mathrm{Base}}_M={\mathrm{Base}}_S$$
18	15 17	ax-mp	$$⊢B\cap {\mathrm{Base}}_M={\mathrm{Base}}_S$$
19	9 18	eqtr2i	$$⊢{\mathrm{Base}}_S=B$$