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