reprfi2

Step	Hyp	Ref	Expression
1		reprinfz1.n	$⊢ φ \to N \in ℕ_{0}$
2		reprinfz1.s	$⊢ φ \to S \in ℕ_{0}$
3		reprinfz1.a	$⊢ φ \to A \subseteq ℕ$
4	1 2 3	reprinfz1	$⊢ φ \to A repr (S) N = (A \cap (1 \dots N)) repr (S) N$
5		inss2	$⊢ A \cap (1 \dots N) \subseteq (1 \dots N)$
6		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
7	5 6	sstri	$⊢ A \cap (1 \dots N) \subseteq ℕ$
8	7	a1i	$⊢ φ \to A \cap (1 \dots N) \subseteq ℕ$
9	1	nn0zd	$⊢ φ \to N \in ℤ$
10		fzfi	$⊢ (1 \dots N) \in Fin$
11	10	a1i	$⊢ φ \to (1 \dots N) \in Fin$
12	5	a1i	$⊢ φ \to A \cap (1 \dots N) \subseteq (1 \dots N)$
13	11 12	ssfid	$⊢ φ \to A \cap (1 \dots N) \in Fin$
14	8 9 2 13	reprfi	$⊢ φ \to (A \cap (1 \dots N)) repr (S) N \in Fin$
15	4 14	eqeltrd	$⊢ φ \to A repr (S) N \in Fin$

Metamath Proof Explorer