Theorem smndex1basss

Description: The modulo function I and the constant functions ( GK ) are endofunctions on NN0 . (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\}$$
Assertion	smndex1basss	$$⊢B\subseteq {\mathrm{Base}}_M$$

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	5	eleq2i	$$⊢b\in B\leftrightarrow b\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)$$
7		fveq2	$$⊢n=k\to G\left(n\right)=G\left(k\right)$$
8	7	sneqd	$$⊢n=k\to \left\{G\left(n\right)\right\}=\left\{G\left(k\right)\right\}$$
9	8	cbviunv	$$⊢\bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}=\bigcup _{k\in \left(0..^N\right)}\left\{G\left(k\right)\right\}$$
10	9	uneq2i	$$⊢\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}=\left\{I\right\}\cup \bigcup _{k\in \left(0..^N\right)}\left\{G\left(k\right)\right\}$$
11	10	eleq2i	$$⊢b\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)\leftrightarrow b\in \left(\left\{I\right\}\cup \bigcup _{k\in \left(0..^N\right)}\left\{G\left(k\right)\right\}\right)$$
12	6 11	bitri	$$⊢b\in B\leftrightarrow b\in \left(\left\{I\right\}\cup \bigcup _{k\in \left(0..^N\right)}\left\{G\left(k\right)\right\}\right)$$
13		elun	$$⊢b\in \left(\left\{I\right\}\cup \bigcup _{k\in \left(0..^N\right)}\left\{G\left(k\right)\right\}\right)\leftrightarrow \left(b\in \left\{I\right\}\vee b\in \bigcup _{k\in \left(0..^N\right)}\left\{G\left(k\right)\right\}\right)$$
14		velsn	$$⊢b\in \left\{I\right\}\leftrightarrow b=I$$
15		eliun	$$⊢b\in \bigcup _{k\in \left(0..^N\right)}\left\{G\left(k\right)\right\}\leftrightarrow \exists k\in \left(0..^N\right)b\in \left\{G\left(k\right)\right\}$$
16	14 15	orbi12i	$$⊢\left(b\in \left\{I\right\}\vee b\in \bigcup _{k\in \left(0..^N\right)}\left\{G\left(k\right)\right\}\right)\leftrightarrow \left(b=I\vee \exists k\in \left(0..^N\right)b\in \left\{G\left(k\right)\right\}\right)$$
17	12 13 16	3bitri	$$⊢b\in B\leftrightarrow \left(b=I\vee \exists k\in \left(0..^N\right)b\in \left\{G\left(k\right)\right\}\right)$$
18	1 2 3	smndex1ibas	$$⊢I\in {\mathrm{Base}}_M$$
19		eleq1	$$⊢b=I\to \left(b\in {\mathrm{Base}}_M\leftrightarrow I\in {\mathrm{Base}}_M\right)$$
20	18 19	mpbiri	$$⊢b=I\to b\in {\mathrm{Base}}_M$$
21	1 2 3 4	smndex1gbas	$$⊢k\in \left(0..^N\right)\to G\left(k\right)\in {\mathrm{Base}}_M$$
22	21	adantr	$$⊢\left(k\in \left(0..^N\right)\wedge b\in \left\{G\left(k\right)\right\}\right)\to G\left(k\right)\in {\mathrm{Base}}_M$$
23		elsni	$$⊢b\in \left\{G\left(k\right)\right\}\to b=G\left(k\right)$$
24	23	eleq1d	$$⊢b\in \left\{G\left(k\right)\right\}\to \left(b\in {\mathrm{Base}}_M\leftrightarrow G\left(k\right)\in {\mathrm{Base}}_M\right)$$
25	24	adantl	$$⊢\left(k\in \left(0..^N\right)\wedge b\in \left\{G\left(k\right)\right\}\right)\to \left(b\in {\mathrm{Base}}_M\leftrightarrow G\left(k\right)\in {\mathrm{Base}}_M\right)$$
26	22 25	mpbird	$$⊢\left(k\in \left(0..^N\right)\wedge b\in \left\{G\left(k\right)\right\}\right)\to b\in {\mathrm{Base}}_M$$
27	26	rexlimiva	$$⊢\exists k\in \left(0..^N\right)b\in \left\{G\left(k\right)\right\}\to b\in {\mathrm{Base}}_M$$
28	20 27	jaoi	$$⊢\left(b=I\vee \exists k\in \left(0..^N\right)b\in \left\{G\left(k\right)\right\}\right)\to b\in {\mathrm{Base}}_M$$
29	17 28	sylbi	$$⊢b\in B\to b\in {\mathrm{Base}}_M$$
30	29	ssriv	$$⊢B\subseteq {\mathrm{Base}}_M$$