iundisjf

Description: Rewrite a countable union as a disjoint union. Cf. iundisj . (Contributed by Thierry Arnoux, 31-Dec-2016)

	Ref	Expression
Hypotheses	iundisjf.1	$⊢ \underline{Ⅎ} k A$
	iundisjf.2	$⊢ \underline{Ⅎ} n B$
	iundisjf.3	$⊢ n = k \to A = B$
Assertion	iundisjf	$⊢ ⋃_{n \in ℕ} A = ⋃_{n \in ℕ} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Proof

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

Metamath Proof Explorer

Theorem iundisjf

Proof