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 ( ∀ 𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol )

Proof

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