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 = ℤ_{\geq N}$
	Assertion	iuneqfzuzlem	$⊢ \forall m \in Z ⋃_{n = N}^{m} A = ⋃_{n = N}^{m} B \to ⋃_{n \in Z} A \subseteq ⋃_{n \in Z} B$

Proof

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

Metamath Proof Explorer

Theorem iuneqfzuzlem

Proof