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 -1 C ∈ 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 ∈ J C = u ∩ B
10 4 8 9 sylancr ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ → C ∈ J ↾ 𝑡 B ↔ ∃ u ∈ J C = u ∩ B
11 3 10 syl5bb ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ → C ∈ K ↔ ∃ u ∈ J C = 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 -1 u ∩ B = F -1 u ∩ F -1 B
15 12 13 14 3syl ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ ∧ u ∈ J → F -1 u ∩ B = F -1 u ∩ F -1 B
16 1 mbfimaopn ⊢ F ∈ MblFn ∧ u ∈ J → F -1 u ∈ dom ⁡ vol
17 16 3ad2antl1 ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ ∧ u ∈ J → F -1 u ∈ dom ⁡ vol
18 fimacnv ⊢ F : A ⟶ B → F -1 B = A
19 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
20 18 19 eqtr4d ⊢ F : A ⟶ B → F -1 B = dom ⁡ F
21 12 20 syl ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ ∧ u ∈ J → F -1 B = 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 -1 B ∈ dom ⁡ vol
26 inmbl ⊢ F -1 u ∈ dom ⁡ vol ∧ F -1 B ∈ dom ⁡ vol → F -1 u ∩ F -1 B ∈ dom ⁡ vol
27 17 25 26 syl2anc ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ ∧ u ∈ J → F -1 u ∩ F -1 B ∈ dom ⁡ vol
28 15 27 eqeltrd ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ ∧ u ∈ J → F -1 u ∩ B ∈ dom ⁡ vol
29 imaeq2 ⊢ C = u ∩ B → F -1 C = F -1 u ∩ B
30 29 eleq1d ⊢ C = u ∩ B → F -1 C ∈ dom ⁡ vol ↔ F -1 u ∩ B ∈ dom ⁡ vol
31 28 30 syl5ibrcom ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ ∧ u ∈ J → C = u ∩ B → F -1 C ∈ dom ⁡ vol
32 31 rexlimdva ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ → ∃ u ∈ J C = u ∩ B → F -1 C ∈ dom ⁡ vol
33 11 32 sylbid ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ → C ∈ K → F -1 C ∈ dom ⁡ vol
34 33 imp ⊢ F ∈ MblFn ∧ F : A ⟶ B ∧ B ⊆ ℂ ∧ C ∈ K → F -1 C ∈ dom ⁡ vol