Metamath Proof Explorer

Theorem iunmbl

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

Ref Expression
Assertion iunmbl ⊢ ∀ n ∈ ℕ A ∈ dom ⁡ vol → ⋃ n ∈ ℕ A ∈ dom ⁡ vol

Proof

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