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	biimpi	$$⊢x\in \bigcup _{n\in Z}A\to \exists m\in Zx\in ⦋m/n⦌A$$
10	9	adantl	$$⊢\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$$
11		nfra1	$$⊢Ⅎm\forall m\in Z\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B$$
12		nfv	$$⊢Ⅎmx\in \bigcup _{n\in Z}B$$
13		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$$
14		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$$
15	14	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$$
16		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$$
17		id	$$⊢\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B$$
18		fzssuz	$$⊢\left(N\dots m\right)\subseteq {\mathbb{Z}}_{\ge N}$$
19	1	eqcomi	$$⊢{\mathbb{Z}}_{\ge N}=Z$$
20	18 19	sseqtri	$$⊢\left(N\dots m\right)\subseteq Z$$
21		iunss1	$$⊢\left(N\dots m\right)\subseteq Z\to \bigcup _{n=N}^{m}B\subseteq \bigcup _{n\in Z}B$$
22	20 21	mp1i	$$⊢\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n=N}^{m}B\subseteq \bigcup _{n\in Z}B$$
23	17 22	eqsstrd	$$⊢\bigcup _{n=N}^{m}A=\bigcup _{n=N}^{m}B\to \bigcup _{n=N}^{m}A\subseteq \bigcup _{n\in Z}B$$
24	23	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$$
25	1	eleq2i	$$⊢m\in Z\leftrightarrow m\in {\mathbb{Z}}_{\ge N}$$
26	25	biimpi	$$⊢m\in Z\to m\in {\mathbb{Z}}_{\ge N}$$
27		eluzel2	$$⊢m\in {\mathbb{Z}}_{\ge N}\to N\in \mathbb{Z}$$
28	26 27	syl	$$⊢m\in Z\to N\in \mathbb{Z}$$
29		eluzelz	$$⊢m\in {\mathbb{Z}}_{\ge N}\to m\in \mathbb{Z}$$
30	26 29	syl	$$⊢m\in Z\to m\in \mathbb{Z}$$
31		eluzle	$$⊢m\in {\mathbb{Z}}_{\ge N}\to N\le m$$
32	26 31	syl	$$⊢m\in Z\to N\le m$$
33	30	zred	$$⊢m\in Z\to m\in ℝ$$
34		leid	$$⊢m\in ℝ\to m\le m$$
35	33 34	syl	$$⊢m\in Z\to m\le m$$
36	28 30 30 32 35	elfzd	$$⊢m\in Z\to m\in \left(N\dots m\right)$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}nx$$
38	37 3	nfel	$$⊢Ⅎnx\in ⦋m/n⦌A$$
39	4	eleq2d	$$⊢n=m\to \left(x\in A\leftrightarrow x\in ⦋m/n⦌A\right)$$
40	38 39	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$$
41	36 40	sylan	$$⊢\left(m\in Z\wedge x\in ⦋m/n⦌A\right)\to \exists n\in \left(N\dots m\right)x\in A$$
42		eliun	$$⊢x\in \bigcup _{n=N}^{m}A\leftrightarrow \exists n\in \left(N\dots m\right)x\in A$$
43	41 42	sylibr	$$⊢\left(m\in Z\wedge x\in ⦋m/n⦌A\right)\to x\in \bigcup _{n=N}^{m}A$$
44	43	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$$
45	24 44	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$$
46	13 15 16 45	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$$
47	46	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)$$
48	11 12 47	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)$$
49	48	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)$$
50	10 49	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$$
51	50	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$$
52		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$$
53	51 52	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$$