Theorem uzinico3

Description: An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	uzinico3.1	$$⊢\phi \to M\in \mathbb{Z}$$
	uzinico3.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	uzinico3	$$⊢\phi \to Z=Z\cap \left[M,\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		uzinico3.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		uzinico3.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3	1	uzidd	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
4	3	uzinico2	$$⊢\phi \to {\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}\cap \left[M,\mathrm{+\infty }\right)$$
5	2	a1i	$$⊢\phi \to Z={\mathbb{Z}}_{\ge M}$$
6	5	ineq1d	$$⊢\phi \to Z\cap \left[M,\mathrm{+\infty }\right)={\mathbb{Z}}_{\ge M}\cap \left[M,\mathrm{+\infty }\right)$$
7	5 6	eqeq12d	$$⊢\phi \to \left(Z=Z\cap \left[M,\mathrm{+\infty }\right)\leftrightarrow {\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}\cap \left[M,\mathrm{+\infty }\right)\right)$$
8	4 7	mpbird	$$⊢\phi \to Z=Z\cap \left[M,\mathrm{+\infty }\right)$$