# Metamath Proof Explorer

## Theorem ismbfd

Description: Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d . (Contributed by Mario Carneiro, 18-Jun-2014)

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

### Proof

Step Hyp Ref Expression
1 ismbfd.1 ${⊢}{\phi }\to {F}:{A}⟶ℝ$
2 ismbfd.2 ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
3 ismbfd.3 ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
4 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
5 ffn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
6 ovelrn ${⊢}\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\to \left({z}\in \mathrm{ran}\left(.\right)↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{z}=\left({x},{y}\right)\right)$
7 4 5 6 mp2b ${⊢}{z}\in \mathrm{ran}\left(.\right)↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{z}=\left({x},{y}\right)$
8 simprl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {x}\in {ℝ}^{*}$
9 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
10 9 a1i ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
11 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
12 11 a1i ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
13 simprr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {y}\in {ℝ}^{*}$
14 iooin ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to \left({x},\mathrm{+\infty }\right)\cap \left(\mathrm{-\infty },{y}\right)=\left(if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right),if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\right)$
15 8 10 12 13 14 syl22anc ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to \left({x},\mathrm{+\infty }\right)\cap \left(\mathrm{-\infty },{y}\right)=\left(if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right),if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\right)$
16 ifcl ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\right)\to if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\in {ℝ}^{*}$
17 11 8 16 sylancr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\in {ℝ}^{*}$
18 mnfle ${⊢}{x}\in {ℝ}^{*}\to \mathrm{-\infty }\le {x}$
19 xrleid ${⊢}{x}\in {ℝ}^{*}\to {x}\le {x}$
20 breq1 ${⊢}\mathrm{-\infty }=if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\to \left(\mathrm{-\infty }\le {x}↔if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\le {x}\right)$
21 breq1 ${⊢}{x}=if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\to \left({x}\le {x}↔if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\le {x}\right)$
22 20 21 ifboth ${⊢}\left(\mathrm{-\infty }\le {x}\wedge {x}\le {x}\right)\to if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\le {x}$
23 18 19 22 syl2anc ${⊢}{x}\in {ℝ}^{*}\to if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\le {x}$
24 23 ad2antrl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)\le {x}$
25 xrmax1 ${⊢}\left({x}\in {ℝ}^{*}\wedge \mathrm{-\infty }\in {ℝ}^{*}\right)\to {x}\le if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)$
26 8 11 25 sylancl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {x}\le if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)$
27 17 8 24 26 xrletrid ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right)={x}$
28 ifcl ${⊢}\left(\mathrm{+\infty }\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\in {ℝ}^{*}$
29 9 13 28 sylancr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\in {ℝ}^{*}$
30 xrmin2 ${⊢}\left(\mathrm{+\infty }\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\le {y}$
31 9 13 30 sylancr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\le {y}$
32 pnfge ${⊢}{y}\in {ℝ}^{*}\to {y}\le \mathrm{+\infty }$
33 xrleid ${⊢}{y}\in {ℝ}^{*}\to {y}\le {y}$
34 breq2 ${⊢}\mathrm{+\infty }=if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\to \left({y}\le \mathrm{+\infty }↔{y}\le if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\right)$
35 breq2 ${⊢}{y}=if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\to \left({y}\le {y}↔{y}\le if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\right)$
36 34 35 ifboth ${⊢}\left({y}\le \mathrm{+\infty }\wedge {y}\le {y}\right)\to {y}\le if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)$
37 32 33 36 syl2anc ${⊢}{y}\in {ℝ}^{*}\to {y}\le if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)$
38 37 ad2antll ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {y}\le if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)$
39 29 13 31 38 xrletrid ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)={y}$
40 27 39 oveq12d ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to \left(if\left({x}\le \mathrm{-\infty },\mathrm{-\infty },{x}\right),if\left(\mathrm{+\infty }\le {y},\mathrm{+\infty },{y}\right)\right)=\left({x},{y}\right)$
41 15 40 eqtrd ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to \left({x},\mathrm{+\infty }\right)\cap \left(\mathrm{-\infty },{y}\right)=\left({x},{y}\right)$
42 41 imaeq2d ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\cap \left(\mathrm{-\infty },{y}\right)\right]={{F}}^{-1}\left[\left({x},{y}\right)\right]$
43 1 adantr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {F}:{A}⟶ℝ$
44 43 ffund ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to \mathrm{Fun}{F}$
45 inpreima ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\cap \left(\mathrm{-\infty },{y}\right)\right]={{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\cap {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]$
46 44 45 syl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\cap \left(\mathrm{-\infty },{y}\right)\right]={{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\cap {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]$
47 42 46 eqtr3d ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left({x},{y}\right)\right]={{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\cap {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]$
48 2 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$
49 3 ralrimiva ${⊢}{\phi }\to \forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol$
50 oveq2 ${⊢}{x}={y}\to \left(\mathrm{-\infty },{x}\right)=\left(\mathrm{-\infty },{y}\right)$
51 50 imaeq2d ${⊢}{x}={y}\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]={{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]$
52 51 eleq1d ${⊢}{x}={y}\to \left({{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol↔{{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]\in \mathrm{dom}vol\right)$
53 52 rspccva ${⊢}\left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[\left(\mathrm{-\infty },{x}\right)\right]\in \mathrm{dom}vol\wedge {y}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]\in \mathrm{dom}vol$
54 49 53 sylan ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{*}\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]\in \mathrm{dom}vol$
55 54 adantrl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]\in \mathrm{dom}vol$
56 inmbl ${⊢}\left({{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol\wedge {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]\in \mathrm{dom}vol\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\cap {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]\in \mathrm{dom}vol$
57 48 55 56 syl2anc ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left({x},\mathrm{+\infty }\right)\right]\cap {{F}}^{-1}\left[\left(\mathrm{-\infty },{y}\right)\right]\in \mathrm{dom}vol$
58 47 57 eqeltrd ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to {{F}}^{-1}\left[\left({x},{y}\right)\right]\in \mathrm{dom}vol$
59 imaeq2 ${⊢}{z}=\left({x},{y}\right)\to {{F}}^{-1}\left[{z}\right]={{F}}^{-1}\left[\left({x},{y}\right)\right]$
60 59 eleq1d ${⊢}{z}=\left({x},{y}\right)\to \left({{F}}^{-1}\left[{z}\right]\in \mathrm{dom}vol↔{{F}}^{-1}\left[\left({x},{y}\right)\right]\in \mathrm{dom}vol\right)$
61 58 60 syl5ibrcom ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\right)\to \left({z}=\left({x},{y}\right)\to {{F}}^{-1}\left[{z}\right]\in \mathrm{dom}vol\right)$
62 61 rexlimdvva ${⊢}{\phi }\to \left(\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{z}=\left({x},{y}\right)\to {{F}}^{-1}\left[{z}\right]\in \mathrm{dom}vol\right)$
63 7 62 syl5bi ${⊢}{\phi }\to \left({z}\in \mathrm{ran}\left(.\right)\to {{F}}^{-1}\left[{z}\right]\in \mathrm{dom}vol\right)$
64 63 ralrimiv ${⊢}{\phi }\to \forall {z}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{dom}vol$
65 ismbf ${⊢}{F}:{A}⟶ℝ\to \left({F}\in MblFn↔\forall {z}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{dom}vol\right)$
66 1 65 syl ${⊢}{\phi }\to \left({F}\in MblFn↔\forall {z}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in \mathrm{dom}vol\right)$
67 64 66 mpbird ${⊢}{\phi }\to {F}\in MblFn$