Theorem smndex1ibas

Description: The modulo function I is an endofunction 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)$$
Assertion	smndex1ibas	$$⊢I\in {\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		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
5		nn0z	$$⊢x\in {\mathbb{N}}_0\to x\in \mathbb{Z}$$
6	2	a1i	$$⊢x\in {\mathbb{N}}_0\to N\in \mathbb{N}$$
7	5 6	zmodcld	$$⊢x\in {\mathbb{N}}_0\to x\mathrm{mod}N\in {\mathbb{N}}_0$$
8	4 7	fmpti	$$⊢\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
9		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
10	9 9	elmap	$$⊢\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)\in \left({{\mathbb{N}}_0}^{{\mathbb{N}}_0}\right)\leftrightarrow \left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
11	8 10	mpbir	$$⊢\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)\in \left({{\mathbb{N}}_0}^{{\mathbb{N}}_0}\right)$$
12		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
13	1 12	efmndbas	$$⊢{\mathrm{Base}}_M={{\mathbb{N}}_0}^{{\mathbb{N}}_0}$$
14	11 3 13	3eltr4i	$$⊢I\in {\mathrm{Base}}_M$$