iunmbl

Description: The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014)

		Ref	Expression
	Assertion	iunmbl	$⊢ \forall n \in ℕ A \in dom vol \to ⋃_{n \in ℕ} A \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ k A \in dom vol$
2		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ k / n ⦌ A$
3	2	nfel1	$⊢ Ⅎ n ⦋ k / n ⦌ A \in dom vol$
4		csbeq1a	$⊢ n = k \to A = ⦋ k / n ⦌ A$
5	4	eleq1d	$⊢ n = k \to (A \in dom vol \leftrightarrow ⦋ k / n ⦌ A \in dom vol)$
6	1 3 5	cbvralw	$⊢ \forall n \in ℕ A \in dom vol \leftrightarrow \forall k \in ℕ ⦋ k / n ⦌ A \in dom vol$
7		nfcv	$⊢ \underline{Ⅎ} k A$
8	7 2 4	cbviun	$⊢ ⋃_{n \in ℕ} A = ⋃_{k \in ℕ} ⦋ k / n ⦌ A$
9		csbeq1	$⊢ k = m \to ⦋ k / n ⦌ A = ⦋ m / n ⦌ A$
10	9	iundisj	$⊢ ⋃_{k \in ℕ} ⦋ k / n ⦌ A = ⋃_{k \in ℕ} (⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A)$
11	8 10	eqtri	$⊢ ⋃_{n \in ℕ} A = ⋃_{k \in ℕ} (⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A)$
12		difexg	$⊢ ⦋ k / n ⦌ A \in dom vol \to ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A \in V$
13	12	ralimi	$⊢ \forall k \in ℕ ⦋ k / n ⦌ A \in dom vol \to \forall k \in ℕ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A \in V$
14		dfiun2g	$⊢ \forall k \in ℕ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A \in V \to ⋃_{k \in ℕ} (⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) = ⋃ \{y \| \exists k \in ℕ y = ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A\}$
15	13 14	syl	$⊢ \forall k \in ℕ ⦋ k / n ⦌ A \in dom vol \to ⋃_{k \in ℕ} (⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) = ⋃ \{y \| \exists k \in ℕ y = ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A\}$
16	11 15	eqtrid	$⊢ \forall k \in ℕ ⦋ k / n ⦌ A \in dom vol \to ⋃_{n \in ℕ} A = ⋃ \{y \| \exists k \in ℕ y = ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A\}$
17	6 16	sylbi	$⊢ \forall n \in ℕ A \in dom vol \to ⋃_{n \in ℕ} A = ⋃ \{y \| \exists k \in ℕ y = ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A\}$
18		eqid	$⊢ (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) = (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A)$
19	18	rnmpt	$⊢ ran (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) = \{y \| \exists k \in ℕ y = ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A\}$
20	19	unieqi	$⊢ ⋃ ran (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) = ⋃ \{y \| \exists k \in ℕ y = ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A\}$
21	17 20	eqtr4di	$⊢ \forall n \in ℕ A \in dom vol \to ⋃_{n \in ℕ} A = ⋃ ran (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A)$
22	3 5	rspc	$⊢ k \in ℕ \to (\forall n \in ℕ A \in dom vol \to ⦋ k / n ⦌ A \in dom vol)$
23	22	impcom	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⦋ k / n ⦌ A \in dom vol$
24		fzofi	$⊢ (1 ..^k) \in Fin$
25		nfv	$⊢ Ⅎ m A \in dom vol$
26		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ m / n ⦌ A$
27	26	nfel1	$⊢ Ⅎ n ⦋ m / n ⦌ A \in dom vol$
28		csbeq1a	$⊢ n = m \to A = ⦋ m / n ⦌ A$
29	28	eleq1d	$⊢ n = m \to (A \in dom vol \leftrightarrow ⦋ m / n ⦌ A \in dom vol)$
30	25 27 29	cbvralw	$⊢ \forall n \in ℕ A \in dom vol \leftrightarrow \forall m \in ℕ ⦋ m / n ⦌ A \in dom vol$
31		fzossnn	$⊢ (1 ..^k) \subseteq ℕ$
32		ssralv	$⊢ (1 ..^k) \subseteq ℕ \to (\forall m \in ℕ ⦋ m / n ⦌ A \in dom vol \to \forall m \in (1 ..^k) ⦋ m / n ⦌ A \in dom vol)$
33	31 32	ax-mp	$⊢ \forall m \in ℕ ⦋ m / n ⦌ A \in dom vol \to \forall m \in (1 ..^k) ⦋ m / n ⦌ A \in dom vol$
34	30 33	sylbi	$⊢ \forall n \in ℕ A \in dom vol \to \forall m \in (1 ..^k) ⦋ m / n ⦌ A \in dom vol$
35	34	adantr	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to \forall m \in (1 ..^k) ⦋ m / n ⦌ A \in dom vol$
36		finiunmbl	$⊢ ((1 ..^k) \in Fin \land \forall m \in (1 ..^k) ⦋ m / n ⦌ A \in dom vol) \to ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A \in dom vol$
37	24 35 36	sylancr	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A \in dom vol$
38		difmbl	$⊢ (⦋ k / n ⦌ A \in dom vol \land ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A \in dom vol) \to ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A \in dom vol$
39	23 37 38	syl2anc	$⊢ (\forall n \in ℕ A \in dom vol \land k \in ℕ) \to ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A \in dom vol$
40	39	fmpttd	$⊢ \forall n \in ℕ A \in dom vol \to (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) : ℕ ⟶ dom vol$
41		csbeq1	$⊢ i = m \to ⦋ i / n ⦌ A = ⦋ m / n ⦌ A$
42	41	iundisj2	$⊢ \underset{i \in ℕ}{Disj} (⦋ i / n ⦌ A ∖ ⋃_{m \in (1 ..^i)} ⦋ m / n ⦌ A)$
43		csbeq1	$⊢ k = i \to ⦋ k / n ⦌ A = ⦋ i / n ⦌ A$
44		oveq2	$⊢ k = i \to (1 ..^k) = (1 ..^i)$
45	44	iuneq1d	$⊢ k = i \to ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A = ⋃_{m \in (1 ..^i)} ⦋ m / n ⦌ A$
46	43 45	difeq12d	$⊢ k = i \to ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A = ⦋ i / n ⦌ A ∖ ⋃_{m \in (1 ..^i)} ⦋ m / n ⦌ A$
47		simpr	$⊢ (\forall n \in ℕ A \in dom vol \land i \in ℕ) \to i \in ℕ$
48		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ i / n ⦌ A$
49	48	nfel1	$⊢ Ⅎ n ⦋ i / n ⦌ A \in dom vol$
50		csbeq1a	$⊢ n = i \to A = ⦋ i / n ⦌ A$
51	50	eleq1d	$⊢ n = i \to (A \in dom vol \leftrightarrow ⦋ i / n ⦌ A \in dom vol)$
52	49 51	rspc	$⊢ i \in ℕ \to (\forall n \in ℕ A \in dom vol \to ⦋ i / n ⦌ A \in dom vol)$
53	52	impcom	$⊢ (\forall n \in ℕ A \in dom vol \land i \in ℕ) \to ⦋ i / n ⦌ A \in dom vol$
54	53	difexd	$⊢ (\forall n \in ℕ A \in dom vol \land i \in ℕ) \to ⦋ i / n ⦌ A ∖ ⋃_{m \in (1 ..^i)} ⦋ m / n ⦌ A \in V$
55	18 46 47 54	fvmptd3	$⊢ (\forall n \in ℕ A \in dom vol \land i \in ℕ) \to (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) (i) = ⦋ i / n ⦌ A ∖ ⋃_{m \in (1 ..^i)} ⦋ m / n ⦌ A$
56	55	disjeq2dv	$⊢ \forall n \in ℕ A \in dom vol \to (\underset{i \in ℕ}{Disj} (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) (i) \leftrightarrow \underset{i \in ℕ}{Disj} (⦋ i / n ⦌ A ∖ ⋃_{m \in (1 ..^i)} ⦋ m / n ⦌ A))$
57	42 56	mpbiri	$⊢ \forall n \in ℕ A \in dom vol \to \underset{i \in ℕ}{Disj} (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) (i)$
58		eqid	$⊢ (y \in ℕ ⟼ {vol}^{} (x \cap (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) (y))) = (y \in ℕ ⟼ {vol}^{} (x \cap (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) (y)))$
59	40 57 58	voliunlem2	$⊢ \forall n \in ℕ A \in dom vol \to ⋃ ran (k \in ℕ ⟼ ⦋ k / n ⦌ A ∖ ⋃_{m \in (1 ..^k)} ⦋ m / n ⦌ A) \in dom vol$
60	21 59	eqeltrd	$⊢ \forall n \in ℕ A \in dom vol \to ⋃_{n \in ℕ} A \in dom vol$

Metamath Proof Explorer

Theorem iunmbl

Proof