Metamath Proof Explorer


Theorem iunmbl2

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

Ref Expression
Assertion iunmbl2 ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → 𝑛𝐴 𝐵 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 brdom2 ( 𝐴 ≼ ℕ ↔ ( 𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ ) )
2 nnenom ℕ ≈ ω
3 sdomentr ( ( 𝐴 ≺ ℕ ∧ ℕ ≈ ω ) → 𝐴 ≺ ω )
4 2 3 mpan2 ( 𝐴 ≺ ℕ → 𝐴 ≺ ω )
5 isfinite ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω )
6 finiunmbl ( ( 𝐴 ∈ Fin ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → 𝑛𝐴 𝐵 ∈ dom vol )
7 6 ex ( 𝐴 ∈ Fin → ( ∀ 𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol ) )
8 5 7 sylbir ( 𝐴 ≺ ω → ( ∀ 𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol ) )
9 4 8 syl ( 𝐴 ≺ ℕ → ( ∀ 𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol ) )
10 bren ( 𝐴 ≈ ℕ ↔ ∃ 𝑓 𝑓 : 𝐴1-1-onto→ ℕ )
11 nfv 𝑛 𝑓 : 𝐴1-1-onto→ ℕ
12 nfcv 𝑛
13 nfcsb1v 𝑛 ( 𝑓𝑘 ) / 𝑛 𝐵
14 13 nfcri 𝑛 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵
15 12 14 nfrex 𝑛𝑘 ∈ ℕ 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵
16 f1of ( 𝑓 : 𝐴1-1-onto→ ℕ → 𝑓 : 𝐴 ⟶ ℕ )
17 16 ffvelrnda ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴 ) → ( 𝑓𝑛 ) ∈ ℕ )
18 17 3adant3 ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴𝑥𝐵 ) → ( 𝑓𝑛 ) ∈ ℕ )
19 simp3 ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴𝑥𝐵 ) → 𝑥𝐵 )
20 f1ocnvfv1 ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴 ) → ( 𝑓 ‘ ( 𝑓𝑛 ) ) = 𝑛 )
21 20 3adant3 ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴𝑥𝐵 ) → ( 𝑓 ‘ ( 𝑓𝑛 ) ) = 𝑛 )
22 21 eqcomd ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴𝑥𝐵 ) → 𝑛 = ( 𝑓 ‘ ( 𝑓𝑛 ) ) )
23 csbeq1a ( 𝑛 = ( 𝑓 ‘ ( 𝑓𝑛 ) ) → 𝐵 = ( 𝑓 ‘ ( 𝑓𝑛 ) ) / 𝑛 𝐵 )
24 22 23 syl ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴𝑥𝐵 ) → 𝐵 = ( 𝑓 ‘ ( 𝑓𝑛 ) ) / 𝑛 𝐵 )
25 19 24 eleqtrd ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴𝑥𝐵 ) → 𝑥 ( 𝑓 ‘ ( 𝑓𝑛 ) ) / 𝑛 𝐵 )
26 fveq2 ( 𝑘 = ( 𝑓𝑛 ) → ( 𝑓𝑘 ) = ( 𝑓 ‘ ( 𝑓𝑛 ) ) )
27 26 csbeq1d ( 𝑘 = ( 𝑓𝑛 ) → ( 𝑓𝑘 ) / 𝑛 𝐵 = ( 𝑓 ‘ ( 𝑓𝑛 ) ) / 𝑛 𝐵 )
28 27 eleq2d ( 𝑘 = ( 𝑓𝑛 ) → ( 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵𝑥 ( 𝑓 ‘ ( 𝑓𝑛 ) ) / 𝑛 𝐵 ) )
29 28 rspcev ( ( ( 𝑓𝑛 ) ∈ ℕ ∧ 𝑥 ( 𝑓 ‘ ( 𝑓𝑛 ) ) / 𝑛 𝐵 ) → ∃ 𝑘 ∈ ℕ 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 )
30 18 25 29 syl2anc ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑛𝐴𝑥𝐵 ) → ∃ 𝑘 ∈ ℕ 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 )
31 30 3exp ( 𝑓 : 𝐴1-1-onto→ ℕ → ( 𝑛𝐴 → ( 𝑥𝐵 → ∃ 𝑘 ∈ ℕ 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 ) ) )
32 11 15 31 rexlimd ( 𝑓 : 𝐴1-1-onto→ ℕ → ( ∃ 𝑛𝐴 𝑥𝐵 → ∃ 𝑘 ∈ ℕ 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 ) )
33 f1ocnvdm ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑓𝑘 ) ∈ 𝐴 )
34 csbeq1a ( 𝑛 = ( 𝑓𝑘 ) → 𝐵 = ( 𝑓𝑘 ) / 𝑛 𝐵 )
35 34 eleq2d ( 𝑛 = ( 𝑓𝑘 ) → ( 𝑥𝐵𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 ) )
36 14 35 rspce ( ( ( 𝑓𝑘 ) ∈ 𝐴𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 ) → ∃ 𝑛𝐴 𝑥𝐵 )
37 36 ex ( ( 𝑓𝑘 ) ∈ 𝐴 → ( 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 → ∃ 𝑛𝐴 𝑥𝐵 ) )
38 33 37 syl ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 → ∃ 𝑛𝐴 𝑥𝐵 ) )
39 38 rexlimdva ( 𝑓 : 𝐴1-1-onto→ ℕ → ( ∃ 𝑘 ∈ ℕ 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 → ∃ 𝑛𝐴 𝑥𝐵 ) )
40 32 39 impbid ( 𝑓 : 𝐴1-1-onto→ ℕ → ( ∃ 𝑛𝐴 𝑥𝐵 ↔ ∃ 𝑘 ∈ ℕ 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 ) )
41 eliun ( 𝑥 𝑛𝐴 𝐵 ↔ ∃ 𝑛𝐴 𝑥𝐵 )
42 eliun ( 𝑥 𝑘 ∈ ℕ ( 𝑓𝑘 ) / 𝑛 𝐵 ↔ ∃ 𝑘 ∈ ℕ 𝑥 ( 𝑓𝑘 ) / 𝑛 𝐵 )
43 40 41 42 3bitr4g ( 𝑓 : 𝐴1-1-onto→ ℕ → ( 𝑥 𝑛𝐴 𝐵𝑥 𝑘 ∈ ℕ ( 𝑓𝑘 ) / 𝑛 𝐵 ) )
44 43 eqrdv ( 𝑓 : 𝐴1-1-onto→ ℕ → 𝑛𝐴 𝐵 = 𝑘 ∈ ℕ ( 𝑓𝑘 ) / 𝑛 𝐵 )
45 44 adantr ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → 𝑛𝐴 𝐵 = 𝑘 ∈ ℕ ( 𝑓𝑘 ) / 𝑛 𝐵 )
46 rspcsbela ( ( ( 𝑓𝑘 ) ∈ 𝐴 ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → ( 𝑓𝑘 ) / 𝑛 𝐵 ∈ dom vol )
47 33 46 sylan ( ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ 𝑘 ∈ ℕ ) ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → ( 𝑓𝑘 ) / 𝑛 𝐵 ∈ dom vol )
48 47 an32s ( ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓𝑘 ) / 𝑛 𝐵 ∈ dom vol )
49 48 ralrimiva ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → ∀ 𝑘 ∈ ℕ ( 𝑓𝑘 ) / 𝑛 𝐵 ∈ dom vol )
50 iunmbl ( ∀ 𝑘 ∈ ℕ ( 𝑓𝑘 ) / 𝑛 𝐵 ∈ dom vol → 𝑘 ∈ ℕ ( 𝑓𝑘 ) / 𝑛 𝐵 ∈ dom vol )
51 49 50 syl ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → 𝑘 ∈ ℕ ( 𝑓𝑘 ) / 𝑛 𝐵 ∈ dom vol )
52 45 51 eqeltrd ( ( 𝑓 : 𝐴1-1-onto→ ℕ ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → 𝑛𝐴 𝐵 ∈ dom vol )
53 52 ex ( 𝑓 : 𝐴1-1-onto→ ℕ → ( ∀ 𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol ) )
54 53 exlimiv ( ∃ 𝑓 𝑓 : 𝐴1-1-onto→ ℕ → ( ∀ 𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol ) )
55 10 54 sylbi ( 𝐴 ≈ ℕ → ( ∀ 𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol ) )
56 9 55 jaoi ( ( 𝐴 ≺ ℕ ∨ 𝐴 ≈ ℕ ) → ( ∀ 𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol ) )
57 1 56 sylbi ( 𝐴 ≼ ℕ → ( ∀ 𝑛𝐴 𝐵 ∈ dom vol → 𝑛𝐴 𝐵 ∈ dom vol ) )
58 57 imp ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑛𝐴 𝐵 ∈ dom vol ) → 𝑛𝐴 𝐵 ∈ dom vol )