Theorem smndex1ibas

Description: The modulo function I is an endofunction on NN0 . (Contributed by AV, 12-Feb-2024)

	Ref	Expression
Hypotheses	smndex1ibas.m	|- M = ( EndoFMnd ` NN0 )
	smndex1ibas.n	|- N e. NN
	smndex1ibas.i	|- I = ( x e. NN0 |-> ( x mod N ) )
Assertion	smndex1ibas	|- I e. ( Base ` 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		eqid	|- ( x e. NN0 |-> ( x mod N ) ) = ( x e. NN0 |-> ( x mod N ) )
5		nn0z	|- ( x e. NN0 -> x e. ZZ )
6	2	a1i	|- ( x e. NN0 -> N e. NN )
7	5 6	zmodcld	|- ( x e. NN0 -> ( x mod N ) e. NN0 )
8	4 7	fmpti	|- ( x e. NN0 |-> ( x mod N ) ) : NN0 --> NN0
9		nn0ex	|- NN0 e. _V
10	9 9	elmap	|- ( ( x e. NN0 |-> ( x mod N ) ) e. ( NN0 ^m NN0 ) <-> ( x e. NN0 |-> ( x mod N ) ) : NN0 --> NN0 )
11	8 10	mpbir	|- ( x e. NN0 |-> ( x mod N ) ) e. ( NN0 ^m NN0 )
12		eqid	|- ( Base ` M ) = ( Base ` M )
13	1 12	efmndbas	|- ( Base ` M ) = ( NN0 ^m NN0 )
14	11 3 13	3eltr4i	|- I e. ( Base ` M )