This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )