iundisj

Description: Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014)

		Ref	Expression
	Hypothesis	iundisj.1	$⊢ n = k \to A = B$
	Assertion	iundisj	$⊢ ⋃_{n \in ℕ} A = ⋃_{n \in ℕ} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Proof

Step	Hyp	Ref	Expression
1		iundisj.1	$⊢ n = k \to A = B$
2		ssrab2	$⊢ \{n \in ℕ \| x \in A\} \subseteq ℕ$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4	2 3	sseqtri	$⊢ \{n \in ℕ \| x \in A\} \subseteq ℤ_{\geq 1}$
5		rabn0	$⊢ \{n \in ℕ \| x \in A\} \neq \emptyset \leftrightarrow \exists n \in ℕ x \in A$
6	5	biimpri	$⊢ \exists n \in ℕ x \in A \to \{n \in ℕ \| x \in A\} \neq \emptyset$
7		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\}$
8	4 6 7	sylancr	$⊢ \exists n \in ℕ x \in A \to inf (\{n \in ℕ \| x \in A\} ℝ <) \in \{n \in ℕ \| x \in A\}$
9		nfrab1	$⊢ \underline{Ⅎ} n \{n \in ℕ \| x \in A\}$
10		nfcv	$⊢ \underline{Ⅎ} n ℝ$
11		nfcv	$⊢ \underline{Ⅎ} n <$
12	9 10 11	nfinf	$⊢ \underline{Ⅎ} n inf (\{n \in ℕ \| x \in A\} ℝ <)$
13		nfcv	$⊢ \underline{Ⅎ} n ℕ$
14	12	nfcsb1	$⊢ \underline{Ⅎ} n ⦋ inf (\{n \in ℕ \| x \in A\} ℝ <) / n ⦌ A$
15	14	nfcri	$⊢ Ⅎ n x \in ⦋ inf (\{n \in ℕ \| x \in A\} ℝ <) / n ⦌ A$
16		csbeq1a	$⊢ n = inf (\{n \in ℕ \| x \in A\} ℝ <) \to A = ⦋ inf (\{n \in ℕ \| x \in A\} ℝ <) / n ⦌ A$
17	16	eleq2d	$⊢ n = inf (\{n \in ℕ \| x \in A\} ℝ <) \to (x \in A \leftrightarrow x \in ⦋ inf (\{n \in ℕ \| x \in A\} ℝ <) / n ⦌ A)$
18	12 13 15 17	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)$
19	8 18	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)$
20	19	simpld	$⊢ \exists n \in ℕ x \in A \to inf (\{n \in ℕ \| x \in A\} ℝ <) \in ℕ$
21	19	simprd	$⊢ \exists n \in ℕ x \in A \to x \in ⦋ inf (\{n \in ℕ \| x \in A\} ℝ <) / n ⦌ A$
22	20	nnred	$⊢ \exists n \in ℕ x \in A \to inf (\{n \in ℕ \| x \in A\} ℝ <) \in ℝ$
23	22	ltnrd	$⊢ \exists n \in ℕ x \in A \to \neg inf (\{n \in ℕ \| x \in A\} ℝ <) < inf (\{n \in ℕ \| x \in A\} ℝ <)$
24		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$
25	22	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 ℝ$
26		elfzouz	$⊢ k \in (1 ..^inf (\{n \in ℕ \| x \in A\} ℝ <)) \to k \in ℤ_{\geq 1}$
27	26 3	eleqtrrdi	$⊢ k \in (1 ..^inf (\{n \in ℕ \| x \in A\} ℝ <)) \to k \in ℕ$
28	27	ad2antlr	$⊢ ((\exists n \in ℕ x \in A \land k \in (1 ..^inf (\{n \in ℕ \| x \in A\} ℝ <))) \land x \in B) \to k \in ℕ$
29	28	nnred	$⊢ ((\exists n \in ℕ x \in A \land k \in (1 ..^inf (\{n \in ℕ \| x \in A\} ℝ <))) \land x \in B) \to k \in ℝ$
30	1	eleq2d	$⊢ n = k \to (x \in A \leftrightarrow x \in B)$
31		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$
32	30 28 31	elrabd	$⊢ ((\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\}$
33		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$
34	4 32 33	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$
35		elfzolt2	$⊢ k \in (1 ..^inf (\{n \in ℕ \| x \in A\} ℝ <)) \to k < inf (\{n \in ℕ \| x \in A\} ℝ <)$
36	35	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\} ℝ <)$
37	25 29 25 34 36	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\} ℝ <)$
38	37	rexlimdva2	$⊢ \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\} ℝ <))$
39	24 38	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\} ℝ <))$
40	23 39	mtod	$⊢ \exists n \in ℕ x \in A \to \neg x \in ⋃_{k \in (1 ..^inf (\{n \in ℕ \| x \in A\} ℝ <))} B$
41	21 40	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)$
42		csbeq1	$⊢ m = inf (\{n \in ℕ \| x \in A\} ℝ <) \to ⦋ m / n ⦌ A = ⦋ inf (\{n \in ℕ \| x \in A\} ℝ <) / n ⦌ A$
43		oveq2	$⊢ m = inf (\{n \in ℕ \| x \in A\} ℝ <) \to (1 ..^m) = (1 ..^inf (\{n \in ℕ \| x \in A\} ℝ <))$
44	43	iuneq1d	$⊢ m = inf (\{n \in ℕ \| x \in A\} ℝ <) \to ⋃_{k \in (1 ..^m)} B = ⋃_{k \in (1 ..^inf (\{n \in ℕ \| x \in A\} ℝ <))} B$
45	42 44	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$
46	45	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))$
47	46	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)$
48	20 41 47	syl2anc	$⊢ \exists n \in ℕ x \in A \to \exists m \in ℕ x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B)$
49		nfv	$⊢ Ⅎ m x \in (A ∖ ⋃_{k \in (1 ..^n)} B)$
50		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ m / n ⦌ A$
51		nfcv	$⊢ \underline{Ⅎ} n ⋃_{k \in (1 ..^m)} B$
52	50 51	nfdif	$⊢ \underline{Ⅎ} n (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B)$
53	52	nfcri	$⊢ Ⅎ n x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B)$
54		csbeq1a	$⊢ n = m \to A = ⦋ m / n ⦌ A$
55		oveq2	$⊢ n = m \to (1 ..^n) = (1 ..^m)$
56	55	iuneq1d	$⊢ n = m \to ⋃_{k \in (1 ..^n)} B = ⋃_{k \in (1 ..^m)} B$
57	54 56	difeq12d	$⊢ n = m \to A ∖ ⋃_{k \in (1 ..^n)} B = ⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B$
58	57	eleq2d	$⊢ n = m \to (x \in (A ∖ ⋃_{k \in (1 ..^n)} B) \leftrightarrow x \in (⦋ m / n ⦌ A ∖ ⋃_{k \in (1 ..^m)} B))$
59	49 53 58	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)$
60	48 59	sylibr	$⊢ \exists n \in ℕ x \in A \to \exists n \in ℕ x \in (A ∖ ⋃_{k \in (1 ..^n)} B)$
61		eldifi	$⊢ x \in (A ∖ ⋃_{k \in (1 ..^n)} B) \to x \in A$
62	61	reximi	$⊢ \exists n \in ℕ x \in (A ∖ ⋃_{k \in (1 ..^n)} B) \to \exists n \in ℕ x \in A$
63	60 62	impbii	$⊢ \exists n \in ℕ x \in A \leftrightarrow \exists n \in ℕ x \in (A ∖ ⋃_{k \in (1 ..^n)} B)$
64		eliun	$⊢ x \in ⋃_{n \in ℕ} A \leftrightarrow \exists n \in ℕ x \in A$
65		eliun	$⊢ x \in ⋃_{n \in ℕ} (A ∖ ⋃_{k \in (1 ..^n)} B) \leftrightarrow \exists n \in ℕ x \in (A ∖ ⋃_{k \in (1 ..^n)} B)$
66	63 64 65	3bitr4i	$⊢ x \in ⋃_{n \in ℕ} A \leftrightarrow x \in ⋃_{n \in ℕ} (A ∖ ⋃_{k \in (1 ..^n)} B)$
67	66	eqriv	$⊢ ⋃_{n \in ℕ} A = ⋃_{n \in ℕ} (A ∖ ⋃_{k \in (1 ..^n)} B)$

Metamath Proof Explorer

Theorem iundisj

Proof