Theorem reprfi2

Description: Corollary of reprinfz1 . (Contributed by Thierry Arnoux, 15-Dec-2021)

	Ref	Expression
Hypotheses	reprinfz1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	reprinfz1.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	reprinfz1.a	$$⊢\phi \to A\subseteq \mathbb{N}$$
Assertion	reprfi2	$$⊢\phi \to A\mathrm{repr}\left(S\right)N\in \mathrm{Fin}$$

Proof

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