This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 nfrexw ⊢ Ⅎ 𝑛 ∃ 𝑘 ∈ ℕ 𝑥 ∈ ⦋ ( ◡ 𝑓 ‘ 𝑘 ) / 𝑛 ⦌ 𝐵
16 f1of ⊢ ( 𝑓 : 𝐴 –1-1-onto→ ℕ → 𝑓 : 𝐴 ⟶ ℕ )
17 16 ffvelcdmda ⊢ ( ( 𝑓 : 𝐴 –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 )