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 ‘ 𝑀 ) |