# Metamath Proof Explorer

## Theorem mbfimaopn2

Description: The preimage of any set open in the subspace topology of the range of the function is measurable. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses mbfimaopn.1 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
mbfimaopn2.2 ${⊢}{K}={J}{↾}_{𝑡}{B}$
Assertion mbfimaopn2 ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {C}\in {K}\right)\to {{F}}^{-1}\left[{C}\right]\in \mathrm{dom}vol$

### Proof

Step Hyp Ref Expression
1 mbfimaopn.1 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 mbfimaopn2.2 ${⊢}{K}={J}{↾}_{𝑡}{B}$
3 2 eleq2i ${⊢}{C}\in {K}↔{C}\in \left({J}{↾}_{𝑡}{B}\right)$
4 1 cnfldtop ${⊢}{J}\in \mathrm{Top}$
5 simp3 ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\to {B}\subseteq ℂ$
6 cnex ${⊢}ℂ\in \mathrm{V}$
7 ssexg ${⊢}\left({B}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to {B}\in \mathrm{V}$
8 5 6 7 sylancl ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\to {B}\in \mathrm{V}$
9 elrest ${⊢}\left({J}\in \mathrm{Top}\wedge {B}\in \mathrm{V}\right)\to \left({C}\in \left({J}{↾}_{𝑡}{B}\right)↔\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{C}={u}\cap {B}\right)$
10 4 8 9 sylancr ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\to \left({C}\in \left({J}{↾}_{𝑡}{B}\right)↔\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{C}={u}\cap {B}\right)$
11 3 10 syl5bb ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\to \left({C}\in {K}↔\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{C}={u}\cap {B}\right)$
12 simpl2 ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to {F}:{A}⟶{B}$
13 ffun ${⊢}{F}:{A}⟶{B}\to \mathrm{Fun}{F}$
14 inpreima ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[{u}\cap {B}\right]={{F}}^{-1}\left[{u}\right]\cap {{F}}^{-1}\left[{B}\right]$
15 12 13 14 3syl ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to {{F}}^{-1}\left[{u}\cap {B}\right]={{F}}^{-1}\left[{u}\right]\cap {{F}}^{-1}\left[{B}\right]$
16 1 mbfimaopn ${⊢}\left({F}\in MblFn\wedge {u}\in {J}\right)\to {{F}}^{-1}\left[{u}\right]\in \mathrm{dom}vol$
17 16 3ad2antl1 ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to {{F}}^{-1}\left[{u}\right]\in \mathrm{dom}vol$
18 fimacnv ${⊢}{F}:{A}⟶{B}\to {{F}}^{-1}\left[{B}\right]={A}$
19 fdm ${⊢}{F}:{A}⟶{B}\to \mathrm{dom}{F}={A}$
20 18 19 eqtr4d ${⊢}{F}:{A}⟶{B}\to {{F}}^{-1}\left[{B}\right]=\mathrm{dom}{F}$
21 12 20 syl ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to {{F}}^{-1}\left[{B}\right]=\mathrm{dom}{F}$
22 simpl1 ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to {F}\in MblFn$
23 mbfdm ${⊢}{F}\in MblFn\to \mathrm{dom}{F}\in \mathrm{dom}vol$
24 22 23 syl ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to \mathrm{dom}{F}\in \mathrm{dom}vol$
25 21 24 eqeltrd ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to {{F}}^{-1}\left[{B}\right]\in \mathrm{dom}vol$
26 inmbl ${⊢}\left({{F}}^{-1}\left[{u}\right]\in \mathrm{dom}vol\wedge {{F}}^{-1}\left[{B}\right]\in \mathrm{dom}vol\right)\to {{F}}^{-1}\left[{u}\right]\cap {{F}}^{-1}\left[{B}\right]\in \mathrm{dom}vol$
27 17 25 26 syl2anc ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to {{F}}^{-1}\left[{u}\right]\cap {{F}}^{-1}\left[{B}\right]\in \mathrm{dom}vol$
28 15 27 eqeltrd ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to {{F}}^{-1}\left[{u}\cap {B}\right]\in \mathrm{dom}vol$
29 imaeq2 ${⊢}{C}={u}\cap {B}\to {{F}}^{-1}\left[{C}\right]={{F}}^{-1}\left[{u}\cap {B}\right]$
30 29 eleq1d ${⊢}{C}={u}\cap {B}\to \left({{F}}^{-1}\left[{C}\right]\in \mathrm{dom}vol↔{{F}}^{-1}\left[{u}\cap {B}\right]\in \mathrm{dom}vol\right)$
31 28 30 syl5ibrcom ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {u}\in {J}\right)\to \left({C}={u}\cap {B}\to {{F}}^{-1}\left[{C}\right]\in \mathrm{dom}vol\right)$
32 31 rexlimdva ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\to \left(\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{C}={u}\cap {B}\to {{F}}^{-1}\left[{C}\right]\in \mathrm{dom}vol\right)$
33 11 32 sylbid ${⊢}\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\to \left({C}\in {K}\to {{F}}^{-1}\left[{C}\right]\in \mathrm{dom}vol\right)$
34 33 imp ${⊢}\left(\left({F}\in MblFn\wedge {F}:{A}⟶{B}\wedge {B}\subseteq ℂ\right)\wedge {C}\in {K}\right)\to {{F}}^{-1}\left[{C}\right]\in \mathrm{dom}vol$