smndex1ibas

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

Step	Hyp	Ref	Expression
1		smndex1ibas.m	$⊢ M = EndoFMnd (ℕ_{0})$
2		smndex1ibas.n	$⊢ N \in ℕ$
3		smndex1ibas.i	$⊢ I = (x \in ℕ_{0} ⟼ x \mod N)$
4		eqid	$⊢ (x \in ℕ_{0} ⟼ x \mod N) = (x \in ℕ_{0} ⟼ x \mod N)$
5		nn0z	$⊢ x \in ℕ_{0} \to x \in ℤ$
6	2	a1i	$⊢ x \in ℕ_{0} \to N \in ℕ$
7	5 6	zmodcld	$⊢ x \in ℕ_{0} \to x \mod N \in ℕ_{0}$
8	4 7	fmpti	$⊢ (x \in ℕ_{0} ⟼ x \mod N) : ℕ_{0} ⟶ ℕ_{0}$
9		nn0ex	$⊢ ℕ_{0} \in V$
10	9 9	elmap	$⊢ (x \in ℕ_{0} ⟼ x \mod N) \in ({ℕ_{0}}^{ℕ_{0}}) \leftrightarrow (x \in ℕ_{0} ⟼ x \mod N) : ℕ_{0} ⟶ ℕ_{0}$
11	8 10	mpbir	$⊢ (x \in ℕ_{0} ⟼ x \mod N) \in ({ℕ_{0}}^{ℕ_{0}})$
12		eqid	$⊢ {Base}_{M} = {Base}_{M}$
13	1 12	efmndbas	$⊢ {Base}_{M} = {ℕ_{0}}^{ℕ_{0}}$
14	11 3 13	3eltr4i	$⊢ I \in {Base}_{M}$

Metamath Proof Explorer