iundisjfi

Description: Rewrite a countable union as a disjoint union, finite version. Cf. iundisj . (Contributed by Thierry Arnoux, 15-Feb-2017)

	Ref	Expression
Hypotheses	iundisj3.0	$⊢ \underline{Ⅎ} n B$
	iundisj3.1	$⊢ n = k \to A = B$
Assertion	iundisjfi	$⊢ ⋃_{n \in (1 ..^N)} A = ⋃_{n \in (1 ..^N)} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Proof

Step	Hyp	Ref	Expression
1		iundisj3.0	$⊢ \underline{Ⅎ} n B$
2		iundisj3.1	$⊢ n = k \to A = B$
3		ssrab2	$⊢ \{n \in (1 ..^N) \| x \in A\} \subseteq (1 ..^N)$
4		fzossnn	$⊢ (1 ..^N) \subseteq ℕ$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6	4 5	sseqtri	$⊢ (1 ..^N) \subseteq ℤ_{\geq 1}$
7	3 6	sstri	$⊢ \{n \in (1 ..^N) \| x \in A\} \subseteq ℤ_{\geq 1}$
8		rabn0	$⊢ \{n \in (1 ..^N) \| x \in A\} \neq \emptyset \leftrightarrow \exists n \in (1 ..^N) x \in A$
9	8	biimpri	$⊢ \exists n \in (1 ..^N) x \in A \to \{n \in (1 ..^N) \| x \in A\} \neq \emptyset$
10		infssuzcl	$⊢ (\{n \in (1 ..^N) \| x \in A\} \subseteq ℤ_{\geq 1} \land \{n \in (1 ..^N) \| x \in A\} \neq \emptyset) \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in \{n \in (1 ..^N) \| x \in A\}$
11	7 9 10	sylancr	$⊢ \exists n \in (1 ..^N) x \in A \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in \{n \in (1 ..^N) \| x \in A\}$
12	3 11	sselid	$⊢ \exists n \in (1 ..^N) x \in A \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in (1 ..^N)$
13		nfrab1	$⊢ \underline{Ⅎ} n \{n \in (1 ..^N) \| x \in A\}$
14		nfcv	$⊢ \underline{Ⅎ} n ℝ$
15		nfcv	$⊢ \underline{Ⅎ} n <$
16	13 14 15	nfinf	$⊢ \underline{Ⅎ} n inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)$
17		nfcv	$⊢ \underline{Ⅎ} n (1 ..^N)$
18	16	nfcsb1	$⊢ \underline{Ⅎ} n ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A$
19	18	nfcri	$⊢ Ⅎ n x \in ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A$
20		csbeq1a	$⊢ n = inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \to A = ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A$
21	20	eleq2d	$⊢ n = inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \to (x \in A \leftrightarrow x \in ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A)$
22	16 17 19 21	elrabf	$⊢ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in \{n \in (1 ..^N) \| x \in A\} \leftrightarrow (inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in (1 ..^N) \land x \in ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A)$
23	11 22	sylib	$⊢ \exists n \in (1 ..^N) x \in A \to (inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in (1 ..^N) \land x \in ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A)$
24	23	simprd	$⊢ \exists n \in (1 ..^N) x \in A \to x \in ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A$
25	3 4	sstri	$⊢ \{n \in (1 ..^N) \| x \in A\} \subseteq ℕ$
26		nnssre	$⊢ ℕ \subseteq ℝ$
27	25 26	sstri	$⊢ \{n \in (1 ..^N) \| x \in A\} \subseteq ℝ$
28	27 11	sselid	$⊢ \exists n \in (1 ..^N) x \in A \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in ℝ$
29	28	ltnrd	$⊢ \exists n \in (1 ..^N) x \in A \to \neg inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) < inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)$
30		eliun	$⊢ x \in ⋃_{k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))} B \leftrightarrow \exists k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)) x \in B$
31	28	ad2antrr	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in ℝ$
32		elfzouz2	$⊢ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in (1 ..^N) \to N \in ℤ_{\geq inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)}$
33		fzoss2	$⊢ N \in ℤ_{\geq inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)} \to (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)) \subseteq (1 ..^N)$
34	12 32 33	3syl	$⊢ \exists n \in (1 ..^N) x \in A \to (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)) \subseteq (1 ..^N)$
35	34	sselda	$⊢ (\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \to k \in (1 ..^N)$
36	35	adantr	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to k \in (1 ..^N)$
37	4 36	sselid	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to k \in ℕ$
38	37	nnred	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to k \in ℝ$
39		simpr	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to x \in B$
40		nfcv	$⊢ \underline{Ⅎ} n k$
41	1	nfcri	$⊢ Ⅎ n x \in B$
42	2	eleq2d	$⊢ n = k \to (x \in A \leftrightarrow x \in B)$
43	40 17 41 42	elrabf	$⊢ k \in \{n \in (1 ..^N) \| x \in A\} \leftrightarrow (k \in (1 ..^N) \land x \in B)$
44	36 39 43	sylanbrc	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to k \in \{n \in (1 ..^N) \| x \in A\}$
45		infssuzle	$⊢ (\{n \in (1 ..^N) \| x \in A\} \subseteq ℤ_{\geq 1} \land k \in \{n \in (1 ..^N) \| x \in A\}) \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \leq k$
46	7 44 45	sylancr	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \leq k$
47		elfzolt2	$⊢ k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)) \to k < inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)$
48	47	ad2antlr	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to k < inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)$
49	31 38 31 46 48	lelttrd	$⊢ ((\exists n \in (1 ..^N) x \in A \land k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))) \land x \in B) \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) < inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)$
50	49	rexlimdva2	$⊢ \exists n \in (1 ..^N) x \in A \to (\exists k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <)) x \in B \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) < inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))$
51	30 50	biimtrid	$⊢ \exists n \in (1 ..^N) x \in A \to (x \in ⋃_{k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))} B \to inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) < inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))$
52	29 51	mtod	$⊢ \exists n \in (1 ..^N) x \in A \to \neg x \in ⋃_{k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))} B$
53	24 52	eldifd	$⊢ \exists n \in (1 ..^N) x \in A \to x \in (⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A ∖ ⋃_{k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))} B)$
54		csbeq1	$⊢ m = inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \to ⦋ m / n ⦌ A = ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A$
55		oveq2	$⊢ m = inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \to (1 ..^m) = (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))$
56	55	iuneq1d	$⊢ m = inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \to ⋃_{k \in (1 ..^m)} B = ⋃_{k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))} B$
57	54 56	difeq12d	$⊢ m = inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \to ⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B = ⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A ∖ ⋃_{k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))} B$
58	57	eleq2d	$⊢ m = inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \to (x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B) \leftrightarrow x \in (⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A ∖ ⋃_{k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))} B))$
59	58	rspcev	$⊢ (inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) \in (1 ..^N) \land x \in (⦋ inf (\{n \in (1 ..^N) \| x \in A\} ℝ <) / n ⦌ A ∖ ⋃_{k \in (1 ..^inf (\{n \in (1 ..^N) \| x \in A\} ℝ <))} B)) \to \exists m \in (1 ..^N) x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B)$
60	12 53 59	syl2anc	$⊢ \exists n \in (1 ..^N) x \in A \to \exists m \in (1 ..^N) x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B)$
61		nfv	$⊢ Ⅎ m x \in (A ∖ ⋃_{k \in (1 ..^n)} B)$
62		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ m / n ⦌ A$
63		nfcv	$⊢ \underline{Ⅎ} n (1 ..^m)$
64	63 1	nfiun	$⊢ \underline{Ⅎ} n ⋃_{k \in (1 ..^m)} B$
65	62 64	nfdif	$⊢ \underline{Ⅎ} n (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B)$
66	65	nfcri	$⊢ Ⅎ n x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B)$
67		csbeq1a	$⊢ n = m \to A = ⦋ m / n ⦌ A$
68		oveq2	$⊢ n = m \to (1 ..^n) = (1 ..^m)$
69	68	iuneq1d	$⊢ n = m \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^m)} B$
70	67 69	difeq12d	$⊢ n = m \to A ∖ ⋃_{k \in (1 ..^n)} B = ⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B$
71	70	eleq2d	$⊢ n = m \to (x \in (A ∖ ⋃_{k \in (1 ..^n)} B) \leftrightarrow x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B))$
72	61 66 71	cbvrexw	$⊢ \exists n \in (1 ..^N) x \in (A ∖ ⋃_{k \in (1 ..^n)} B) \leftrightarrow \exists m \in (1 ..^N) x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B)$
73	60 72	sylibr	$⊢ \exists n \in (1 ..^N) x \in A \to \exists n \in (1 ..^N) x \in (A ∖ ⋃_{k \in (1 ..^n)} B)$
74		eldifi	$⊢ x \in (A ∖ ⋃_{k \in (1 ..^n)} B) \to x \in A$
75	74	reximi	$⊢ \exists n \in (1 ..^N) x \in (A ∖ ⋃_{k \in (1 ..^n)} B) \to \exists n \in (1 ..^N) x \in A$
76	73 75	impbii	$⊢ \exists n \in (1 ..^N) x \in A \leftrightarrow \exists n \in (1 ..^N) x \in (A ∖ ⋃_{k \in (1 ..^n)} B)$
77		eliun	$⊢ x \in ⋃_{n \in (1 ..^N)} A \leftrightarrow \exists n \in (1 ..^N) x \in A$
78		eliun	$⊢ x \in ⋃_{n \in (1 ..^N)} (A ∖ ⋃_{k \in (1 ..^n)} B) \leftrightarrow \exists n \in (1 ..^N) x \in (A ∖ ⋃_{k \in (1 ..^n)} B)$
79	76 77 78	3bitr4i	$⊢ x \in ⋃_{n \in (1 ..^N)} A \leftrightarrow x \in ⋃_{n \in (1 ..^N)} (A ∖ ⋃_{k \in (1 ..^n)} B)$
80	79	eqriv	$⊢ ⋃_{n \in (1 ..^N)} A = ⋃_{n \in (1 ..^N)} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Metamath Proof Explorer

Theorem iundisjfi

Proof