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 syl5eq ( ∀ 𝑘 ∈ ℕ 𝑘 / 𝑛 𝐴 ∈ 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 )