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 ⊢ℲkA∈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 ⊢Ⅎ_kA
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 eqtrid ⊢∀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 ⊢ℲmA∈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 ⊢Disji∈ℕ⦋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 53 difexd ⊢∀n∈ℕA∈dom⁡vol∧i∈ℕ→⦋i/n⦌A∖⋃m∈1..^i⦋m/n⦌A∈V
55 18 46 47 54 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
56 55 disjeq2dv ⊢∀n∈ℕA∈dom⁡vol→Disji∈ℕk∈ℕ⟼⦋k/n⦌A∖⋃m∈1..^k⦋m/n⦌A⁡i↔Disji∈ℕ⦋i/n⦌A∖⋃m∈1..^i⦋m/n⦌A
57 42 56 mpbiri ⊢∀n∈ℕA∈dom⁡vol→Disji∈ℕk∈ℕ⟼⦋k/n⦌A∖⋃m∈1..^k⦋m/n⦌A⁡i
58 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
59 40 57 58 voliunlem2 ⊢∀n∈ℕA∈dom⁡vol→⋃ran⁡k∈ℕ⟼⦋k/n⦌A∖⋃m∈1..^k⦋m/n⦌A∈dom⁡vol
60 21 59 eqeltrd ⊢∀n∈ℕA∈dom⁡vol→⋃n∈ℕA∈dom⁡vol