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 ∈ A B ∈ dom ⁡ vol → ⋃ k ∈ A B ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 raleq ⊢ y = ∅ → ∀ k ∈ y B ∈ dom ⁡ vol ↔ ∀ k ∈ ∅ B ∈ dom ⁡ vol
2 iuneq1 ⊢ y = ∅ → ⋃ k ∈ y B = ⋃ k ∈ ∅ B
3 2 eleq1d ⊢ y = ∅ → ⋃ k ∈ y B ∈ dom ⁡ vol ↔ ⋃ k ∈ ∅ B ∈ dom ⁡ vol
4 1 3 imbi12d ⊢ y = ∅ → ∀ k ∈ y B ∈ dom ⁡ vol → ⋃ k ∈ y B ∈ dom ⁡ vol ↔ ∀ k ∈ ∅ B ∈ dom ⁡ vol → ⋃ k ∈ ∅ B ∈ dom ⁡ vol
5 raleq ⊢ y = x → ∀ k ∈ y B ∈ dom ⁡ vol ↔ ∀ k ∈ x B ∈ dom ⁡ vol
6 iuneq1 ⊢ y = x → ⋃ k ∈ y B = ⋃ k ∈ x B
7 6 eleq1d ⊢ y = x → ⋃ k ∈ y B ∈ dom ⁡ vol ↔ ⋃ k ∈ x B ∈ dom ⁡ vol
8 5 7 imbi12d ⊢ y = x → ∀ k ∈ y B ∈ dom ⁡ vol → ⋃ k ∈ y B ∈ dom ⁡ vol ↔ ∀ k ∈ x B ∈ dom ⁡ vol → ⋃ k ∈ x B ∈ dom ⁡ vol
9 raleq ⊢ y = x ∪ z → ∀ k ∈ y B ∈ dom ⁡ vol ↔ ∀ k ∈ x ∪ z B ∈ dom ⁡ vol
10 iuneq1 ⊢ y = x ∪ z → ⋃ k ∈ y B = ⋃ k ∈ x ∪ z B
11 10 eleq1d ⊢ y = x ∪ z → ⋃ k ∈ y B ∈ dom ⁡ vol ↔ ⋃ k ∈ x ∪ z B ∈ dom ⁡ vol
12 9 11 imbi12d ⊢ y = x ∪ z → ∀ k ∈ y B ∈ dom ⁡ vol → ⋃ k ∈ y B ∈ dom ⁡ vol ↔ ∀ k ∈ x ∪ z B ∈ dom ⁡ vol → ⋃ k ∈ x ∪ z B ∈ dom ⁡ vol
13 raleq ⊢ y = A → ∀ k ∈ y B ∈ dom ⁡ vol ↔ ∀ k ∈ A B ∈ dom ⁡ vol
14 iuneq1 ⊢ y = A → ⋃ k ∈ y B = ⋃ k ∈ A B
15 14 eleq1d ⊢ y = A → ⋃ k ∈ y B ∈ dom ⁡ vol ↔ ⋃ k ∈ A B ∈ dom ⁡ vol
16 13 15 imbi12d ⊢ y = A → ∀ k ∈ y B ∈ dom ⁡ vol → ⋃ k ∈ y B ∈ dom ⁡ vol ↔ ∀ k ∈ A B ∈ dom ⁡ vol → ⋃ k ∈ A B ∈ 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 ∪ z B ∈ dom ⁡ vol → ∀ k ∈ x B ∈ dom ⁡ vol
23 21 22 ax-mp ⊢ ∀ k ∈ x ∪ z B ∈ dom ⁡ vol → ∀ k ∈ x B ∈ dom ⁡ vol
24 23 imim1i ⊢ ∀ k ∈ x B ∈ dom ⁡ vol → ⋃ k ∈ x B ∈ dom ⁡ vol → ∀ k ∈ x ∪ z B ∈ dom ⁡ vol → ⋃ k ∈ x B ∈ dom ⁡ vol
25 ssun2 ⊢ z ⊆ x ∪ z
26 ssralv ⊢ z ⊆ x ∪ z → ∀ k ∈ x ∪ z B ∈ dom ⁡ vol → ∀ k ∈ z B ∈ dom ⁡ vol
27 25 26 ax-mp ⊢ ∀ k ∈ x ∪ z B ∈ dom ⁡ vol → ∀ k ∈ z B ∈ dom ⁡ vol
28 iunxun ⊢ ⋃ k ∈ x ∪ z B = ⋃ k ∈ x B ∪ ⋃ k ∈ z B
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 ⊢ Ⅎ x B ∈ 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 ∈ z B ∈ dom ⁡ vol ↔ ∀ x ∈ z ⦋ x / k⦌ B ∈ dom ⁡ vol
39 nfcv ⊢ Ⅎ _ x B
40 39 34 36 cbviun ⊢ ⋃ k ∈ z B = ⋃ x ∈ z ⦋ x / k⦌ B
41 29 30 iunxsn ⊢ ⋃ x ∈ z ⦋ x / k⦌ B = ⦋ z / k⦌ B
42 40 41 eqtri ⊢ ⋃ k ∈ z B = ⦋ z / k⦌ B
43 42 eleq1i ⊢ ⋃ k ∈ z B ∈ dom ⁡ vol ↔ ⦋ z / k⦌ B ∈ dom ⁡ vol
44 32 38 43 3bitr4i ⊢ ∀ k ∈ z B ∈ dom ⁡ vol ↔ ⋃ k ∈ z B ∈ dom ⁡ vol
45 unmbl ⊢ ⋃ k ∈ x B ∈ dom ⁡ vol ∧ ⋃ k ∈ z B ∈ dom ⁡ vol → ⋃ k ∈ x B ∪ ⋃ k ∈ z B ∈ dom ⁡ vol
46 44 45 sylan2b ⊢ ⋃ k ∈ x B ∈ dom ⁡ vol ∧ ∀ k ∈ z B ∈ dom ⁡ vol → ⋃ k ∈ x B ∪ ⋃ k ∈ z B ∈ dom ⁡ vol
47 28 46 eqeltrid ⊢ ⋃ k ∈ x B ∈ dom ⁡ vol ∧ ∀ k ∈ z B ∈ dom ⁡ vol → ⋃ k ∈ x ∪ z B ∈ dom ⁡ vol
48 47 expcom ⊢ ∀ k ∈ z B ∈ dom ⁡ vol → ⋃ k ∈ x B ∈ dom ⁡ vol → ⋃ k ∈ x ∪ z B ∈ dom ⁡ vol
49 27 48 syl ⊢ ∀ k ∈ x ∪ z B ∈ dom ⁡ vol → ⋃ k ∈ x B ∈ dom ⁡ vol → ⋃ k ∈ x ∪ z B ∈ dom ⁡ vol
50 24 49 sylcom ⊢ ∀ k ∈ x B ∈ dom ⁡ vol → ⋃ k ∈ x B ∈ dom ⁡ vol → ∀ k ∈ x ∪ z B ∈ dom ⁡ vol → ⋃ k ∈ x ∪ z B ∈ dom ⁡ vol
51 50 a1i ⊢ x ∈ Fin → ∀ k ∈ x B ∈ dom ⁡ vol → ⋃ k ∈ x B ∈ dom ⁡ vol → ∀ k ∈ x ∪ z B ∈ dom ⁡ vol → ⋃ k ∈ x ∪ z B ∈ dom ⁡ vol
52 4 8 12 16 20 51 findcard2 ⊢ A ∈ Fin → ∀ k ∈ A B ∈ dom ⁡ vol → ⋃ k ∈ A B ∈ dom ⁡ vol
53 52 imp ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ dom ⁡ vol → ⋃ k ∈ A B ∈ dom ⁡ vol