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 ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex1ibas.n ⊢ 𝑁 ∈ ℕ
smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
Assertion smndex1ibas 𝐼 ∈ ( Base ‘ 𝑀 )

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex1ibas.n ⊢ 𝑁 ∈ ℕ
3 smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4 eqid ⊢ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
5 nn0z ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
6 2 a1i ⊢ ( 𝑥 ∈ ℕ0 → 𝑁 ∈ ℕ )
7 5 6 zmodcld ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 mod 𝑁 ) ∈ ℕ0 )
8 4 7 fmpti ⊢ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) : ℕ0 ⟶ ℕ0
9 nn0ex ⊢ ℕ0 ∈ V
10 9 9 elmap ⊢ ( ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) ∈ ( ℕ0 ↑m ℕ0 ) ↔ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) : ℕ0 ⟶ ℕ0 )
11 8 10 mpbir ⊢ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) ∈ ( ℕ0 ↑m ℕ0 )
12 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
13 1 12 efmndbas ⊢ ( Base ‘ 𝑀 ) = ( ℕ0 ↑m ℕ0 )
14 11 3 13 3eltr4i ⊢ 𝐼 ∈ ( Base ‘ 𝑀 )