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-1BC∈dom⁡vol

Proof

Step Hyp Ref Expression
1 iccssre ⊢B∈ℝ∧C∈ℝ→BC⊆ℝ
2 1 adantl ⊢F∈MblFn∧F:A⟶ℝ∧B∈ℝ∧C∈ℝ→BC⊆ℝ
3 dfss4 ⊢BC⊆ℝ↔ℝ∖ℝ∖BC=BC
4 2 3 sylib ⊢F∈MblFn∧F:A⟶ℝ∧B∈ℝ∧C∈ℝ→ℝ∖ℝ∖BC=BC
5 difreicc ⊢B∈ℝ∧C∈ℝ→ℝ∖BC=−∞B∪C+∞
6 5 adantl ⊢F∈MblFn∧F:A⟶ℝ∧B∈ℝ∧C∈ℝ→ℝ∖BC=−∞B∪C+∞
7 6 difeq2d ⊢F∈MblFn∧F:A⟶ℝ∧B∈ℝ∧C∈ℝ→ℝ∖ℝ∖BC=ℝ∖−∞B∪C+∞
8 4 7 eqtr3d ⊢F∈MblFn∧F:A⟶ℝ∧B∈ℝ∧C∈ℝ→BC=ℝ∖−∞B∪C+∞
9 8 imaeq2d ⊢F∈MblFn∧F:A⟶ℝ∧B∈ℝ∧C∈ℝ→F-1BC=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-1BC=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-1C+∞
26 mbfima ⊢F∈MblFn∧F:A⟶ℝ→F-1−∞B∈dom⁡vol
27 mbfima ⊢F∈MblFn∧F:A⟶ℝ→F-1C+∞∈dom⁡vol
28 unmbl ⊢F-1−∞B∈dom⁡vol∧F-1C+∞∈dom⁡vol→F-1−∞B∪F-1C+∞∈dom⁡vol
29 26 27 28 syl2anc ⊢F∈MblFn∧F:A⟶ℝ→F-1−∞B∪F-1C+∞∈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-1BC∈dom⁡vol