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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
mbfimaopn2.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝐵 )
Assertion mbfimaopn2 ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝐶 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝐶 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 mbfimaopn.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 mbfimaopn2.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝐵 )
3 2 eleq2i ⊢ ( 𝐶 ∈ 𝐾 ↔ 𝐶 ∈ ( 𝐽 ↾t 𝐵 ) )
4 1 cnfldtop ⊢ 𝐽 ∈ Top
5 simp3 ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) → 𝐵 ⊆ ℂ )
6 cnex ⊢ ℂ ∈ V
7 ssexg ⊢ ( ( 𝐵 ⊆ ℂ ∧ ℂ ∈ V ) → 𝐵 ∈ V )
8 5 6 7 sylancl ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) → 𝐵 ∈ V )
9 elrest ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ∈ V ) → ( 𝐶 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ∃ 𝑢 ∈ 𝐽 𝐶 = ( 𝑢 ∩ 𝐵 ) ) )
10 4 8 9 sylancr ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) → ( 𝐶 ∈ ( 𝐽 ↾t 𝐵 ) ↔ ∃ 𝑢 ∈ 𝐽 𝐶 = ( 𝑢 ∩ 𝐵 ) ) )
11 3 10 bitrid ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) → ( 𝐶 ∈ 𝐾 ↔ ∃ 𝑢 ∈ 𝐽 𝐶 = ( 𝑢 ∩ 𝐵 ) ) )
12 simpl2 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
13 ffun ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
14 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) )
15 12 13 14 3syl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) )
16 1 mbfimaopn ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝑢 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝑢 ) ∈ dom vol )
17 16 3ad2antl1 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝑢 ) ∈ dom vol )
18 fimacnv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐹 “ 𝐵 ) = 𝐴 )
19 fdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
20 18 19 eqtr4d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐹 “ 𝐵 ) = dom 𝐹 )
21 12 20 syl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝐵 ) = dom 𝐹 )
22 simpl1 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → 𝐹 ∈ MblFn )
23 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
24 22 23 syl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → dom 𝐹 ∈ dom vol )
25 21 24 eqeltrd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝐵 ) ∈ dom vol )
26 inmbl ⊢ ( ( ( ◡ 𝐹 “ 𝑢 ) ∈ dom vol ∧ ( ◡ 𝐹 “ 𝐵 ) ∈ dom vol ) → ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) ∈ dom vol )
27 17 25 26 syl2anc ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → ( ( ◡ 𝐹 “ 𝑢 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) ∈ dom vol )
28 15 27 eqeltrd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝑢 ∩ 𝐵 ) ) ∈ dom vol )
29 imaeq2 ⊢ ( 𝐶 = ( 𝑢 ∩ 𝐵 ) → ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ ( 𝑢 ∩ 𝐵 ) ) )
30 29 eleq1d ⊢ ( 𝐶 = ( 𝑢 ∩ 𝐵 ) → ( ( ◡ 𝐹 “ 𝐶 ) ∈ dom vol ↔ ( ◡ 𝐹 “ ( 𝑢 ∩ 𝐵 ) ) ∈ dom vol ) )
31 28 30 syl5ibrcom ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝑢 ∈ 𝐽 ) → ( 𝐶 = ( 𝑢 ∩ 𝐵 ) → ( ◡ 𝐹 “ 𝐶 ) ∈ dom vol ) )
32 31 rexlimdva ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) → ( ∃ 𝑢 ∈ 𝐽 𝐶 = ( 𝑢 ∩ 𝐵 ) → ( ◡ 𝐹 “ 𝐶 ) ∈ dom vol ) )
33 11 32 sylbid ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) → ( 𝐶 ∈ 𝐾 → ( ◡ 𝐹 “ 𝐶 ) ∈ dom vol ) )
34 33 imp ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ 𝐶 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝐶 ) ∈ dom vol )