Theorem iuneqfzuzlem

Description: Lemma for iuneqfzuz : here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	iuneqfzuzlem.z	$$⊢Z={\mathbb{Z}}_{\ge N}$$
Assertion	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$$

Proof

Step	Hyp	Ref	Expression
1		iuneqfzuzlem.z	$$⊢Z={\mathbb{Z}}_{\ge N}$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}mA$$
3		nfcsb1v	$$⊢\underset{\_}{Ⅎ}n⦋m/n⦌A$$
4		csbeq1a	$$⊢n=m\to A=⦋m/n⦌A$$
5	2 3 4	cbviun	$$⊢\bigcup _{n\in Z}A=\bigcup _{m\in Z}⦋m/n⦌A$$
6	5	eleq2i	$$⊢x\in \bigcup _{n\in Z}A\leftrightarrow x\in \bigcup _{m\in Z}⦋m/n⦌A$$
7		eliun	$$⊢x\in \bigcup _{m\in Z}⦋m/n⦌A\leftrightarrow \exists m\in Zx\in ⦋m/n⦌A$$
8	6 7	bitri	$$⊢x\in \bigcup _{n\in Z}A\leftrightarrow \exists m\in Zx\in ⦋m/n⦌A$$
9	8	bilani	$$⊢\left(\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge x\in \bigcup _{n\in Z}A\right)\to \exists m\in Zx\in ⦋m/n⦌A$$
10		nfra1	$$⊢Ⅎm\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B$$
11		nfv	$$⊢Ⅎmx\in \bigcup _{n\in Z}B$$
12		simp2	$$⊢\left(\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge m\in Z\wedge x\in ⦋m/n⦌A\right)\to m\in Z$$
13		rspa	$$⊢\left(\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge m\in Z\right)\to \bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B$$
14	13	3adant3	$$⊢\left(\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge m\in Z\wedge x\in ⦋m/n⦌A\right)\to \bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B$$
15		simp3	$$⊢\left(\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge m\in Z\wedge x\in ⦋m/n⦌A\right)\to x\in ⦋m/n⦌A$$
16		id	$$⊢\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B$$
17		fzssuz	$$⊢\left(N\dots m\right)\subseteq {\mathbb{Z}}_{\ge N}$$
18	1	eqcomi	$$⊢{\mathbb{Z}}_{\ge N}=Z$$
19	17 18	sseqtri	$$⊢\left(N\dots m\right)\subseteq Z$$
20		iunss1	$$⊢\left(N\dots m\right)\subseteq Z\to \bigcup _{n=N}^{m}B\subseteq \bigcup _{n\in Z}B$$
21	19 20	mp1i	$$⊢\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n=N}^{m}B\subseteq \bigcup _{n\in Z}B$$
22	16 21	eqsstrd	$$⊢\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n=N}^{m}A\subseteq \bigcup _{n\in Z}B$$
23	22	3ad2ant2	$$⊢\left(m\in Z\wedge \bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge x\in ⦋m/n⦌A\right)\to \bigcup _{n=N}^{m}A\subseteq \bigcup _{n\in Z}B$$
24	1	eleq2i	$$⊢m\in Z\leftrightarrow m\in {\mathbb{Z}}_{\ge N}$$
25	24	biimpi	$$⊢m\in Z\to m\in {\mathbb{Z}}_{\ge N}$$
26		eluzel2	$$⊢m\in {\mathbb{Z}}_{\ge N}\to N\in \mathbb{Z}$$
27	25 26	syl	$$⊢m\in Z\to N\in \mathbb{Z}$$
28		eluzelz	$$⊢m\in {\mathbb{Z}}_{\ge N}\to m\in \mathbb{Z}$$
29	25 28	syl	$$⊢m\in Z\to m\in \mathbb{Z}$$
30		eluzle	$$⊢m\in {\mathbb{Z}}_{\ge N}\to N\le m$$
31	25 30	syl	$$⊢m\in Z\to N\le m$$
32	29	zred	$$⊢m\in Z\to m\in ℝ$$
33		leid	$$⊢m\in ℝ\to m\le m$$
34	32 33	syl	$$⊢m\in Z\to m\le m$$
35	27 29 29 31 34	elfzd	$$⊢m\in Z\to m\in \left(N\dots m\right)$$
36		nfcv	$$⊢\underset{\_}{Ⅎ}nx$$
37	36 3	nfel	$$⊢Ⅎnx\in ⦋m/n⦌A$$
38	4	eleq2d	$$⊢n=m\to \left(x\in A\leftrightarrow x\in ⦋m/n⦌A\right)$$
39	37 38	rspce	$$⊢\left(m\in \left(N\dots m\right)\wedge x\in ⦋m/n⦌A\right)\to \exists n\in \left(N\dots m\right)x\in A$$
40	35 39	sylan	$$⊢\left(m\in Z\wedge x\in ⦋m/n⦌A\right)\to \exists n\in \left(N\dots m\right)x\in A$$
41		eliun	$$⊢x\in \bigcup _{n=N}^{m}A\leftrightarrow \exists n\in \left(N\dots m\right)x\in A$$
42	40 41	sylibr	$$⊢\left(m\in Z\wedge x\in ⦋m/n⦌A\right)\to x\in \bigcup _{n=N}^{m}A$$
43	42	3adant2	$$⊢\left(m\in Z\wedge \bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge x\in ⦋m/n⦌A\right)\to x\in \bigcup _{n=N}^{m}A$$
44	23 43	sseldd	$$⊢\left(m\in Z\wedge \bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge x\in ⦋m/n⦌A\right)\to x\in \bigcup _{n\in Z}B$$
45	12 14 15 44	syl3anc	$$⊢\left(\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge m\in Z\wedge x\in ⦋m/n⦌A\right)\to x\in \bigcup _{n\in Z}B$$
46	45	3exp	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \left(m\in Z\to \left(x\in ⦋m/n⦌A\to x\in \bigcup _{n\in Z}B\right)\right)$$
47	10 11 46	rexlimd	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \left(\exists m\in Zx\in ⦋m/n⦌A\to x\in \bigcup _{n\in Z}B\right)$$
48	47	adantr	$$⊢\left(\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge x\in \bigcup _{n\in Z}A\right)\to \left(\exists m\in Zx\in ⦋m/n⦌A\to x\in \bigcup _{n\in Z}B\right)$$
49	9 48	mpd	$$⊢\left(\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\wedge x\in \bigcup _{n\in Z}A\right)\to x\in \bigcup _{n\in Z}B$$
50	49	ralrimiva	$$⊢\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \forall x\in \bigcup _{n\in Z}Ax\in \bigcup _{n\in Z}B$$
51		dfss3	$$⊢\bigcup _{n\in Z}A\subseteq \bigcup _{n\in Z}B\leftrightarrow \forall x\in \bigcup _{n\in Z}Ax\in \bigcup _{n\in Z}B$$
52	50 51	sylibr	$$⊢\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$$