Metamath Proof Explorer


Theorem i1fima

Description: Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion i1fima ( 𝐹 ∈ dom ∫1 → ( 𝐹𝐴 ) ∈ dom vol )

Proof

Step Hyp Ref Expression
1 i1ff ( 𝐹 ∈ dom ∫1𝐹 : ℝ ⟶ ℝ )
2 ffun ( 𝐹 : ℝ ⟶ ℝ → Fun 𝐹 )
3 inpreima ( Fun 𝐹 → ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) )
4 iunid 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) { 𝑦 } = ( 𝐴 ∩ ran 𝐹 )
5 4 imaeq2i ( 𝐹 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) { 𝑦 } ) = ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) )
6 imaiun ( 𝐹 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) { 𝑦 } ) = 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ( 𝐹 “ { 𝑦 } )
7 5 6 eqtr3i ( 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ( 𝐹 “ { 𝑦 } )
8 cnvimass ( 𝐹𝐴 ) ⊆ dom 𝐹
9 cnvimarndm ( 𝐹 “ ran 𝐹 ) = dom 𝐹
10 8 9 sseqtrri ( 𝐹𝐴 ) ⊆ ( 𝐹 “ ran 𝐹 )
11 df-ss ( ( 𝐹𝐴 ) ⊆ ( 𝐹 “ ran 𝐹 ) ↔ ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) = ( 𝐹𝐴 ) )
12 10 11 mpbi ( ( 𝐹𝐴 ) ∩ ( 𝐹 “ ran 𝐹 ) ) = ( 𝐹𝐴 )
13 3 7 12 3eqtr3g ( Fun 𝐹 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ( 𝐹 “ { 𝑦 } ) = ( 𝐹𝐴 ) )
14 1 2 13 3syl ( 𝐹 ∈ dom ∫1 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ( 𝐹 “ { 𝑦 } ) = ( 𝐹𝐴 ) )
15 i1frn ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
16 inss2 ( 𝐴 ∩ ran 𝐹 ) ⊆ ran 𝐹
17 ssfi ( ( ran 𝐹 ∈ Fin ∧ ( 𝐴 ∩ ran 𝐹 ) ⊆ ran 𝐹 ) → ( 𝐴 ∩ ran 𝐹 ) ∈ Fin )
18 15 16 17 sylancl ( 𝐹 ∈ dom ∫1 → ( 𝐴 ∩ ran 𝐹 ) ∈ Fin )
19 i1fmbf ( 𝐹 ∈ dom ∫1𝐹 ∈ MblFn )
20 19 adantr ( ( 𝐹 ∈ dom ∫1𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ) → 𝐹 ∈ MblFn )
21 1 adantr ( ( 𝐹 ∈ dom ∫1𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ) → 𝐹 : ℝ ⟶ ℝ )
22 1 frnd ( 𝐹 ∈ dom ∫1 → ran 𝐹 ⊆ ℝ )
23 16 22 sstrid ( 𝐹 ∈ dom ∫1 → ( 𝐴 ∩ ran 𝐹 ) ⊆ ℝ )
24 23 sselda ( ( 𝐹 ∈ dom ∫1𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ) → 𝑦 ∈ ℝ )
25 mbfimasn ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐹 “ { 𝑦 } ) ∈ dom vol )
26 20 21 24 25 syl3anc ( ( 𝐹 ∈ dom ∫1𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ) → ( 𝐹 “ { 𝑦 } ) ∈ dom vol )
27 26 ralrimiva ( 𝐹 ∈ dom ∫1 → ∀ 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ( 𝐹 “ { 𝑦 } ) ∈ dom vol )
28 finiunmbl ( ( ( 𝐴 ∩ ran 𝐹 ) ∈ Fin ∧ ∀ 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ( 𝐹 “ { 𝑦 } ) ∈ dom vol ) → 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ( 𝐹 “ { 𝑦 } ) ∈ dom vol )
29 18 27 28 syl2anc ( 𝐹 ∈ dom ∫1 𝑦 ∈ ( 𝐴 ∩ ran 𝐹 ) ( 𝐹 “ { 𝑦 } ) ∈ dom vol )
30 14 29 eqeltrrd ( 𝐹 ∈ dom ∫1 → ( 𝐹𝐴 ) ∈ dom vol )