Theorem reprfz1

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

	Ref	Expression
Hypotheses	reprfz1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	reprfz1.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
Assertion	reprfz1	$$⊢\phi \to \mathbb{N}\mathrm{repr}\left(S\right)N=\left(1\dots N\right)\mathrm{repr}\left(S\right)N$$

Proof

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