Metamath Proof Explorer

Theorem mbfimaicc

Description: The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion mbfimaicc ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → F -1 B C ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 iccssre ⊢ B ∈ ℝ ∧ C ∈ ℝ → B C ⊆ ℝ
2 1 adantl ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B C ⊆ ℝ
3 dfss4 ⊢ B C ⊆ ℝ ↔ ℝ ∖ ℝ ∖ B C = B C
4 2 3 sylib ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ℝ ∖ ℝ ∖ B C = B C
5 difreicc ⊢ B ∈ ℝ ∧ C ∈ ℝ → ℝ ∖ B C = −∞ B ∪ C +∞
6 5 adantl ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ℝ ∖ B C = −∞ B ∪ C +∞
7 6 difeq2d ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → ℝ ∖ ℝ ∖ B C = ℝ ∖ −∞ B ∪ C +∞
8 4 7 eqtr3d ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B C = ℝ ∖ −∞ B ∪ C +∞
9 8 imaeq2d ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → F -1 B C = F -1 ℝ ∖ −∞ B ∪ C +∞
10 ffun ⊢ F : A ⟶ ℝ → Fun ⁡ F
11 funcnvcnv ⊢ Fun ⁡ F → Fun ⁡ F -1 -1
12 10 11 syl ⊢ F : A ⟶ ℝ → Fun ⁡ F -1 -1
13 12 ad2antlr ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → Fun ⁡ F -1 -1
14 imadif ⊢ Fun ⁡ F -1 -1 → F -1 ℝ ∖ −∞ B ∪ C +∞ = F -1 ℝ ∖ F -1 −∞ B ∪ C +∞
15 13 14 syl ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → F -1 ℝ ∖ −∞ B ∪ C +∞ = F -1 ℝ ∖ F -1 −∞ B ∪ C +∞
16 9 15 eqtrd ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → F -1 B C = F -1 ℝ ∖ F -1 −∞ B ∪ C +∞
17 fimacnv ⊢ F : A ⟶ ℝ → F -1 ℝ = A
18 17 adantl ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → F -1 ℝ = A
19 mbfdm ⊢ F ∈ MblFn → dom ⁡ F ∈ dom ⁡ vol
20 fdm ⊢ F : A ⟶ ℝ → dom ⁡ F = A
21 20 eleq1d ⊢ F : A ⟶ ℝ → dom ⁡ F ∈ dom ⁡ vol ↔ A ∈ dom ⁡ vol
22 21 biimpac ⊢ dom ⁡ F ∈ dom ⁡ vol ∧ F : A ⟶ ℝ → A ∈ dom ⁡ vol
23 19 22 sylan ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → A ∈ dom ⁡ vol
24 18 23 eqeltrd ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → F -1 ℝ ∈ dom ⁡ vol
25 imaundi ⊢ F -1 −∞ B ∪ C +∞ = F -1 −∞ B ∪ F -1 C +∞
26 mbfima ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → F -1 −∞ B ∈ dom ⁡ vol
27 mbfima ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → F -1 C +∞ ∈ dom ⁡ vol
28 unmbl ⊢ F -1 −∞ B ∈ dom ⁡ vol ∧ F -1 C +∞ ∈ dom ⁡ vol → F -1 −∞ B ∪ F -1 C +∞ ∈ dom ⁡ vol
29 26 27 28 syl2anc ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → F -1 −∞ B ∪ F -1 C +∞ ∈ dom ⁡ vol
30 25 29 eqeltrid ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → F -1 −∞ B ∪ C +∞ ∈ dom ⁡ vol
31 difmbl ⊢ F -1 ℝ ∈ dom ⁡ vol ∧ F -1 −∞ B ∪ C +∞ ∈ dom ⁡ vol → F -1 ℝ ∖ F -1 −∞ B ∪ C +∞ ∈ dom ⁡ vol
32 24 30 31 syl2anc ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ → F -1 ℝ ∖ F -1 −∞ B ∪ C +∞ ∈ dom ⁡ vol
33 32 adantr ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → F -1 ℝ ∖ F -1 −∞ B ∪ C +∞ ∈ dom ⁡ vol
34 16 33 eqeltrd ⊢ F ∈ MblFn ∧ F : A ⟶ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → F -1 B C ∈ dom ⁡ vol