reprfz1

Step	Hyp	Ref	Expression
1		reprfz1.n	$⊢ φ \to N \in ℕ_{0}$
2		reprfz1.s	$⊢ φ \to S \in ℕ_{0}$
3		ssidd	$⊢ φ \to ℕ \subseteq ℕ$
4	1 2 3	reprinfz1	$⊢ φ \to ℕ repr (S) N = (ℕ \cap (1 \dots N)) repr (S) N$
5		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
6		dfss	$⊢ (1 \dots N) \subseteq ℕ \leftrightarrow (1 \dots N) = (1 \dots N) \cap ℕ$
7	5 6	mpbi	$⊢ (1 \dots N) = (1 \dots N) \cap ℕ$
8		incom	$⊢ (1 \dots N) \cap ℕ = ℕ \cap (1 \dots N)$
9	7 8	eqtri	$⊢ (1 \dots N) = ℕ \cap (1 \dots N)$
10	9	oveq1i	$⊢ (1 \dots N) repr (S) N = (ℕ \cap (1 \dots N)) repr (S) N$
11	4 10	eqtr4di	$⊢ φ \to ℕ repr (S) N = (1 \dots N) repr (S) N$

Metamath Proof Explorer