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 ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ◡ 𝐹 “ ( 𝐵 [,] 𝐶 ) ) ∈ dom vol )

Proof

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