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 )