Metamath Proof Explorer

Theorem finiunmbl

Description: A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Assertion finiunmbl ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol ) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 raleq ⊢ ( 𝑦 = ∅ → ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ↔ ∀ 𝑘 ∈ ∅ 𝐵 ∈ dom vol ) )
2 iuneq1 ⊢ ( 𝑦 = ∅ → ∪ 𝑘 ∈ 𝑦 𝐵 = ∪ 𝑘 ∈ ∅ 𝐵 )
3 2 eleq1d ⊢ ( 𝑦 = ∅ → ( ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ↔ ∪ 𝑘 ∈ ∅ 𝐵 ∈ dom vol ) )
4 1 3 imbi12d ⊢ ( 𝑦 = ∅ → ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) ↔ ( ∀ 𝑘 ∈ ∅ 𝐵 ∈ dom vol → ∪ 𝑘 ∈ ∅ 𝐵 ∈ dom vol ) ) )
5 raleq ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ↔ ∀ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ) )
6 iuneq1 ⊢ ( 𝑦 = 𝑥 → ∪ 𝑘 ∈ 𝑦 𝐵 = ∪ 𝑘 ∈ 𝑥 𝐵 )
7 6 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ↔ ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ) )
8 5 7 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) ↔ ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ) ) )
9 raleq ⊢ ( 𝑦 = ( 𝑥 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ↔ ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) )
10 iuneq1 ⊢ ( 𝑦 = ( 𝑥 ∪ { 𝑧 } ) → ∪ 𝑘 ∈ 𝑦 𝐵 = ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 )
11 10 eleq1d ⊢ ( 𝑦 = ( 𝑥 ∪ { 𝑧 } ) → ( ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ↔ ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) )
12 9 11 imbi12d ⊢ ( 𝑦 = ( 𝑥 ∪ { 𝑧 } ) → ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) ↔ ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) ) )
13 raleq ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ↔ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol ) )
14 iuneq1 ⊢ ( 𝑦 = 𝐴 → ∪ 𝑘 ∈ 𝑦 𝐵 = ∪ 𝑘 ∈ 𝐴 𝐵 )
15 14 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ↔ ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol ) )
16 13 15 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ∀ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑦 𝐵 ∈ dom vol ) ↔ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol ) ) )
17 0iun ⊢ ∪ 𝑘 ∈ ∅ 𝐵 = ∅
18 0mbl ⊢ ∅ ∈ dom vol
19 17 18 eqeltri ⊢ ∪ 𝑘 ∈ ∅ 𝐵 ∈ dom vol
20 19 a1i ⊢ ( ∀ 𝑘 ∈ ∅ 𝐵 ∈ dom vol → ∪ 𝑘 ∈ ∅ 𝐵 ∈ dom vol )
21 ssun1 ⊢ 𝑥 ⊆ ( 𝑥 ∪ { 𝑧 } )
22 ssralv ⊢ ( 𝑥 ⊆ ( 𝑥 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∀ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ) )
23 21 22 ax-mp ⊢ ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∀ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol )
24 23 imim1i ⊢ ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ) → ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ) )
25 ssun2 ⊢ { 𝑧 } ⊆ ( 𝑥 ∪ { 𝑧 } )
26 ssralv ⊢ ( { 𝑧 } ⊆ ( 𝑥 ∪ { 𝑧 } ) → ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol ) )
27 25 26 ax-mp ⊢ ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol )
28 iunxun ⊢ ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 = ( ∪ 𝑘 ∈ 𝑥 𝐵 ∪ ∪ 𝑘 ∈ { 𝑧 } 𝐵 )
29 vex ⊢ 𝑧 ∈ V
30 csbeq1 ⊢ ( 𝑥 = 𝑧 → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
31 30 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ dom vol ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol ) )
32 29 31 ralsn ⊢ ( ∀ 𝑥 ∈ { 𝑧 } ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ dom vol ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol )
33 nfv ⊢ Ⅎ 𝑥 𝐵 ∈ dom vol
34 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐵
35 34 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ dom vol
36 csbeq1a ⊢ ( 𝑘 = 𝑥 → 𝐵 = ⦋ 𝑥 / 𝑘 ⦌ 𝐵 )
37 36 eleq1d ⊢ ( 𝑘 = 𝑥 → ( 𝐵 ∈ dom vol ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ dom vol ) )
38 33 35 37 cbvralw ⊢ ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol ↔ ∀ 𝑥 ∈ { 𝑧 } ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ dom vol )
39 nfcv ⊢ Ⅎ 𝑥 𝐵
40 39 34 36 cbviun ⊢ ∪ 𝑘 ∈ { 𝑧 } 𝐵 = ∪ 𝑥 ∈ { 𝑧 } ⦋ 𝑥 / 𝑘 ⦌ 𝐵
41 29 30 iunxsn ⊢ ∪ 𝑥 ∈ { 𝑧 } ⦋ 𝑥 / 𝑘 ⦌ 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵
42 40 41 eqtri ⊢ ∪ 𝑘 ∈ { 𝑧 } 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵
43 42 eleq1i ⊢ ( ∪ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ dom vol )
44 32 38 43 3bitr4i ⊢ ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol ↔ ∪ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol )
45 unmbl ⊢ ( ( ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ∧ ∪ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol ) → ( ∪ 𝑘 ∈ 𝑥 𝐵 ∪ ∪ 𝑘 ∈ { 𝑧 } 𝐵 ) ∈ dom vol )
46 44 45 sylan2b ⊢ ( ( ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol ) → ( ∪ 𝑘 ∈ 𝑥 𝐵 ∪ ∪ 𝑘 ∈ { 𝑧 } 𝐵 ) ∈ dom vol )
47 28 46 eqeltrid ⊢ ( ( ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ∧ ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol ) → ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol )
48 47 expcom ⊢ ( ∀ 𝑘 ∈ { 𝑧 } 𝐵 ∈ dom vol → ( ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol → ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) )
49 27 48 syl ⊢ ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ( ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol → ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) )
50 24 49 sylcom ⊢ ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ) → ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) )
51 50 a1i ⊢ ( 𝑥 ∈ Fin → ( ( ∀ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝑥 𝐵 ∈ dom vol ) → ( ∀ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol → ∪ 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) 𝐵 ∈ dom vol ) ) )
52 4 8 12 16 20 51 findcard2 ⊢ ( 𝐴 ∈ Fin → ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol ) )
53 52 imp ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol ) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol )