Metamath Proof Explorer

Theorem mbfres2

Description: Measurability of a piecewise function: if F is measurable on subsets B and C of its domain, and these pieces make up all of A , then F is measurable on the whole domain. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses mbfres2.1 ⊢ φ → F : A ⟶ ℝ
mbfres2.2 ⊢ φ → F ↾ B ∈ MblFn
mbfres2.3 ⊢ φ → F ↾ C ∈ MblFn
mbfres2.4 ⊢ φ → B ∪ C = A
Assertion mbfres2 ⊢ φ → F ∈ MblFn

Proof

Step Hyp Ref Expression
1 mbfres2.1 ⊢ φ → F : A ⟶ ℝ
2 mbfres2.2 ⊢ φ → F ↾ B ∈ MblFn
3 mbfres2.3 ⊢ φ → F ↾ C ∈ MblFn
4 mbfres2.4 ⊢ φ → B ∪ C = A
5 4 reseq2d ⊢ φ → F ↾ B ∪ C = F ↾ A
6 ffn ⊢ F : A ⟶ ℝ → F Fn A
7 fnresdm ⊢ F Fn A → F ↾ A = F
8 1 6 7 3syl ⊢ φ → F ↾ A = F
9 5 8 eqtr2d ⊢ φ → F = F ↾ B ∪ C
10 9 adantr ⊢ φ ∧ x ∈ ran ⁡ . → F = F ↾ B ∪ C
11 resundi ⊢ F ↾ B ∪ C = F ↾ B ∪ F ↾ C
12 10 11 eqtrdi ⊢ φ ∧ x ∈ ran ⁡ . → F = F ↾ B ∪ F ↾ C
13 12 cnveqd ⊢ φ ∧ x ∈ ran ⁡ . → F -1 = F ↾ B ∪ F ↾ C -1
14 cnvun ⊢ F ↾ B ∪ F ↾ C -1 = F ↾ B -1 ∪ F ↾ C -1
15 13 14 eqtrdi ⊢ φ ∧ x ∈ ran ⁡ . → F -1 = F ↾ B -1 ∪ F ↾ C -1
16 15 imaeq1d ⊢ φ ∧ x ∈ ran ⁡ . → F -1 x = F ↾ B -1 ∪ F ↾ C -1 x
17 imaundir ⊢ F ↾ B -1 ∪ F ↾ C -1 x = F ↾ B -1 x ∪ F ↾ C -1 x
18 16 17 eqtrdi ⊢ φ ∧ x ∈ ran ⁡ . → F -1 x = F ↾ B -1 x ∪ F ↾ C -1 x
19 ssun1 ⊢ B ⊆ B ∪ C
20 19 4 sseqtrid ⊢ φ → B ⊆ A
21 1 20 fssresd ⊢ φ → F ↾ B : B ⟶ ℝ
22 ismbf ⊢ F ↾ B : B ⟶ ℝ → F ↾ B ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F ↾ B -1 x ∈ dom ⁡ vol
23 21 22 syl ⊢ φ → F ↾ B ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F ↾ B -1 x ∈ dom ⁡ vol
24 2 23 mpbid ⊢ φ → ∀ x ∈ ran ⁡ . F ↾ B -1 x ∈ dom ⁡ vol
25 24 r19.21bi ⊢ φ ∧ x ∈ ran ⁡ . → F ↾ B -1 x ∈ dom ⁡ vol
26 ssun2 ⊢ C ⊆ B ∪ C
27 26 4 sseqtrid ⊢ φ → C ⊆ A
28 1 27 fssresd ⊢ φ → F ↾ C : C ⟶ ℝ
29 ismbf ⊢ F ↾ C : C ⟶ ℝ → F ↾ C ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F ↾ C -1 x ∈ dom ⁡ vol
30 28 29 syl ⊢ φ → F ↾ C ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F ↾ C -1 x ∈ dom ⁡ vol
31 3 30 mpbid ⊢ φ → ∀ x ∈ ran ⁡ . F ↾ C -1 x ∈ dom ⁡ vol
32 31 r19.21bi ⊢ φ ∧ x ∈ ran ⁡ . → F ↾ C -1 x ∈ dom ⁡ vol
33 unmbl ⊢ F ↾ B -1 x ∈ dom ⁡ vol ∧ F ↾ C -1 x ∈ dom ⁡ vol → F ↾ B -1 x ∪ F ↾ C -1 x ∈ dom ⁡ vol
34 25 32 33 syl2anc ⊢ φ ∧ x ∈ ran ⁡ . → F ↾ B -1 x ∪ F ↾ C -1 x ∈ dom ⁡ vol
35 18 34 eqeltrd ⊢ φ ∧ x ∈ ran ⁡ . → F -1 x ∈ dom ⁡ vol
36 35 ralrimiva ⊢ φ → ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
37 ismbf ⊢ F : A ⟶ ℝ → F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
38 1 37 syl ⊢ φ → F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
39 36 38 mpbird ⊢ φ → F ∈ MblFn