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=TopOpen⁡ℂfld
mbfimaopn2.2 ⊢K=J↾𝑡B
Assertion mbfimaopn2 ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧C∈K→F-1C∈dom⁡vol

Proof

Step Hyp Ref Expression
1 mbfimaopn.1 ⊢J=TopOpen⁡ℂfld
2 mbfimaopn2.2 ⊢K=J↾𝑡B
3 2 eleq2i ⊢C∈K↔C∈J↾𝑡B
4 1 cnfldtop ⊢J∈Top
5 simp3 ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ→B⊆ℂ
6 cnex ⊢ℂ∈V
7 ssexg ⊢B⊆ℂ∧ℂ∈V→B∈V
8 5 6 7 sylancl ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ→B∈V
9 elrest ⊢J∈Top∧B∈V→C∈J↾𝑡B↔∃u∈JC=u∩B
10 4 8 9 sylancr ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ→C∈J↾𝑡B↔∃u∈JC=u∩B
11 3 10 bitrid ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ→C∈K↔∃u∈JC=u∩B
12 simpl2 ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→F:A⟶B
13 ffun ⊢F:A⟶B→Fun⁡F
14 inpreima ⊢Fun⁡F→F-1u∩B=F-1u∩F-1B
15 12 13 14 3syl ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→F-1u∩B=F-1u∩F-1B
16 1 mbfimaopn ⊢F∈MblFn∧u∈J→F-1u∈dom⁡vol
17 16 3ad2antl1 ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→F-1u∈dom⁡vol
18 fimacnv ⊢F:A⟶B→F-1B=A
19 fdm ⊢F:A⟶B→dom⁡F=A
20 18 19 eqtr4d ⊢F:A⟶B→F-1B=dom⁡F
21 12 20 syl ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→F-1B=dom⁡F
22 simpl1 ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→F∈MblFn
23 mbfdm ⊢F∈MblFn→dom⁡F∈dom⁡vol
24 22 23 syl ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→dom⁡F∈dom⁡vol
25 21 24 eqeltrd ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→F-1B∈dom⁡vol
26 inmbl ⊢F-1u∈dom⁡vol∧F-1B∈dom⁡vol→F-1u∩F-1B∈dom⁡vol
27 17 25 26 syl2anc ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→F-1u∩F-1B∈dom⁡vol
28 15 27 eqeltrd ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→F-1u∩B∈dom⁡vol
29 imaeq2 ⊢C=u∩B→F-1C=F-1u∩B
30 29 eleq1d ⊢C=u∩B→F-1C∈dom⁡vol↔F-1u∩B∈dom⁡vol
31 28 30 syl5ibrcom ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧u∈J→C=u∩B→F-1C∈dom⁡vol
32 31 rexlimdva ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ→∃u∈JC=u∩B→F-1C∈dom⁡vol
33 11 32 sylbid ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ→C∈K→F-1C∈dom⁡vol
34 33 imp ⊢F∈MblFn∧F:A⟶B∧B⊆ℂ∧C∈K→F-1C∈dom⁡vol