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 ⊢A∈Fin∧∀k∈AB∈dom⁡vol→⋃k∈AB∈dom⁡vol

Proof

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