# Metamath Proof Explorer

## Theorem ismbf2d

Description: Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses ismbf2d.1 ${⊢}{\phi }\to {F}:{A}⟶ℝ$
ismbf2d.2 ${⊢}{\phi }\to {A}\in \mathrm{dom}vol$
ismbf2d.3 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
ismbf2d.4 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
Assertion ismbf2d ${⊢}{\phi }\to {F}\in MblFn$

### Proof

Step Hyp Ref Expression
1 ismbf2d.1 ${⊢}{\phi }\to {F}:{A}⟶ℝ$
2 ismbf2d.2 ${⊢}{\phi }\to {A}\in \mathrm{dom}vol$
3 ismbf2d.3 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
4 ismbf2d.4 ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
5 elxr ${⊢}{x}\in {ℝ}^{*}↔\left({x}\in ℝ\vee {x}=\mathrm{+\infty }\vee {x}=\mathrm{-\infty }\right)$
6 oveq1 ${⊢}{x}=\mathrm{+\infty }\to \left({x},\mathrm{+\infty }\right)=\left(\mathrm{+\infty },\mathrm{+\infty }\right)$
7 iooid ${⊢}\left(\mathrm{+\infty },\mathrm{+\infty }\right)=\varnothing$
8 6 7 syl6eq ${⊢}{x}=\mathrm{+\infty }\to \left({x},\mathrm{+\infty }\right)=\varnothing$
9 8 imaeq2d ${⊢}{x}=\mathrm{+\infty }\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]={{F}}^{-1}\left[\varnothing \right]$
10 ima0 ${⊢}{{F}}^{-1}\left[\varnothing \right]=\varnothing$
11 0mbl ${⊢}\varnothing \in \mathrm{dom}vol$
12 10 11 eqeltri ${⊢}{{F}}^{-1}\left[\varnothing \right]\in \mathrm{dom}vol$
13 9 12 eqeltrdi ${⊢}{x}=\mathrm{+\infty }\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
14 13 adantl ${⊢}\left({\phi }\wedge {x}=\mathrm{+\infty }\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
15 fimacnv ${⊢}{F}:{A}⟶ℝ\to {{F}}^{-1}\left[ℝ\right]={A}$
16 1 15 syl ${⊢}{\phi }\to {{F}}^{-1}\left[ℝ\right]={A}$
17 16 2 eqeltrd ${⊢}{\phi }\to {{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol$
18 oveq1 ${⊢}{x}=\mathrm{-\infty }\to \left({x},\mathrm{+\infty }\right)=\left(\mathrm{-\infty },\mathrm{+\infty }\right)$
19 ioomax ${⊢}\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$
20 18 19 syl6eq ${⊢}{x}=\mathrm{-\infty }\to \left({x},\mathrm{+\infty }\right)=ℝ$
21 20 imaeq2d ${⊢}{x}=\mathrm{-\infty }\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]={{F}}^{-1}\left[ℝ\right]$
22 21 eleq1d ${⊢}{x}=\mathrm{-\infty }\to \left({{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol↔{{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol\right)$
23 17 22 syl5ibrcom ${⊢}{\phi }\to \left({x}=\mathrm{-\infty }\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol\right)$
24 23 imp ${⊢}\left({\phi }\wedge {x}=\mathrm{-\infty }\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
25 3 14 24 3jaodan ${⊢}\left({\phi }\wedge \left({x}\in ℝ\vee {x}=\mathrm{+\infty }\vee {x}=\mathrm{-\infty }\right)\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
26 5 25 sylan2b ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
27 oveq2 ${⊢}{x}=\mathrm{+\infty }\to \left(\mathrm{-\infty },{x}\right)=\left(\mathrm{-\infty },\mathrm{+\infty }\right)$
28 27 19 syl6eq ${⊢}{x}=\mathrm{+\infty }\to \left(\mathrm{-\infty },{x}\right)=ℝ$
29 28 imaeq2d ${⊢}{x}=\mathrm{+\infty }\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]={{F}}^{-1}\left[ℝ\right]$
30 29 eleq1d ${⊢}{x}=\mathrm{+\infty }\to \left({{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol↔{{F}}^{-1}\left[ℝ\right]\in \mathrm{dom}vol\right)$
31 17 30 syl5ibrcom ${⊢}{\phi }\to \left({x}=\mathrm{+\infty }\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol\right)$
32 31 imp ${⊢}\left({\phi }\wedge {x}=\mathrm{+\infty }\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
33 oveq2 ${⊢}{x}=\mathrm{-\infty }\to \left(\mathrm{-\infty },{x}\right)=\left(\mathrm{-\infty },\mathrm{-\infty }\right)$
34 iooid ${⊢}\left(\mathrm{-\infty },\mathrm{-\infty }\right)=\varnothing$
35 33 34 syl6eq ${⊢}{x}=\mathrm{-\infty }\to \left(\mathrm{-\infty },{x}\right)=\varnothing$
36 35 imaeq2d ${⊢}{x}=\mathrm{-\infty }\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]={{F}}^{-1}\left[\varnothing \right]$
37 36 12 eqeltrdi ${⊢}{x}=\mathrm{-\infty }\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
38 37 adantl ${⊢}\left({\phi }\wedge {x}=\mathrm{-\infty }\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
39 4 32 38 3jaodan ${⊢}\left({\phi }\wedge \left({x}\in ℝ\vee {x}=\mathrm{+\infty }\vee {x}=\mathrm{-\infty }\right)\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
40 5 39 sylan2b ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
41 1 26 40 ismbfd ${⊢}{\phi }\to {F}\in MblFn$