Theorem iuneqfzuz

Description: If two unions indexed by upper integers are equal if they agree on any partial indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	iuneqfzuz.z	$$⊢Z={\mathbb{Z}}_{\ge N}$$
Assertion	iuneqfzuz	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n\in Z}A=\bigcup _{n\in Z}B$$

Proof

Step	Hyp	Ref	Expression
1		iuneqfzuz.z	$$⊢Z={\mathbb{Z}}_{\ge N}$$
2	1	iuneqfzuzlem	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n\in Z}A\subseteq \bigcup _{n\in Z}B$$
3		eqcom	$$⊢\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\leftrightarrow \bigcup _{n=N}^{m}B=\bigcup _{n=N}^{m}A$$
4	3	ralbii	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\leftrightarrow \forall m\in Z\bigcup _{n=N}^{m}B=\bigcup _{n=N}^{m}A$$
5	4	biimpi	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \forall m\in Z\bigcup _{n=N}^{m}B=\bigcup _{n=N}^{m}A$$
6	1	iuneqfzuzlem	$$⊢\forall m\in Z\bigcup _{n=N}^{m}B=\bigcup _{n=N}^{m}A\to \bigcup _{n\in Z}B\subseteq \bigcup _{n\in Z}A$$
7	5 6	syl	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n\in Z}B\subseteq \bigcup _{n\in Z}A$$
8	2 7	eqssd	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n\in Z}A=\bigcup _{n\in Z}B$$