Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  i1fima Structured version   Visualization version   GIF version

Theorem i1fima 23665
 Description: Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.)
Assertion
Ref Expression
i1fima (𝐹 ∈ dom ∫1 → (𝐹𝐴) ∈ dom vol)

Proof of Theorem i1fima
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 i1ff 23663 . . 3 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
2 ffun 6187 . . 3 (𝐹:ℝ⟶ℝ → Fun 𝐹)
3 inpreima 6487 . . . 4 (Fun 𝐹 → (𝐹 “ (𝐴 ∩ ran 𝐹)) = ((𝐹𝐴) ∩ (𝐹 “ ran 𝐹)))
4 iunid 4710 . . . . . 6 𝑦 ∈ (𝐴 ∩ ran 𝐹){𝑦} = (𝐴 ∩ ran 𝐹)
54imaeq2i 5604 . . . . 5 (𝐹 𝑦 ∈ (𝐴 ∩ ran 𝐹){𝑦}) = (𝐹 “ (𝐴 ∩ ran 𝐹))
6 imaiun 6649 . . . . 5 (𝐹 𝑦 ∈ (𝐴 ∩ ran 𝐹){𝑦}) = 𝑦 ∈ (𝐴 ∩ ran 𝐹)(𝐹 “ {𝑦})
75, 6eqtr3i 2795 . . . 4 (𝐹 “ (𝐴 ∩ ran 𝐹)) = 𝑦 ∈ (𝐴 ∩ ran 𝐹)(𝐹 “ {𝑦})
8 cnvimass 5625 . . . . . 6 (𝐹𝐴) ⊆ dom 𝐹
9 cnvimarndm 5626 . . . . . 6 (𝐹 “ ran 𝐹) = dom 𝐹
108, 9sseqtr4i 3787 . . . . 5 (𝐹𝐴) ⊆ (𝐹 “ ran 𝐹)
11 df-ss 3737 . . . . 5 ((𝐹𝐴) ⊆ (𝐹 “ ran 𝐹) ↔ ((𝐹𝐴) ∩ (𝐹 “ ran 𝐹)) = (𝐹𝐴))
1210, 11mpbi 220 . . . 4 ((𝐹𝐴) ∩ (𝐹 “ ran 𝐹)) = (𝐹𝐴)
133, 7, 123eqtr3g 2828 . . 3 (Fun 𝐹 𝑦 ∈ (𝐴 ∩ ran 𝐹)(𝐹 “ {𝑦}) = (𝐹𝐴))
141, 2, 133syl 18 . 2 (𝐹 ∈ dom ∫1 𝑦 ∈ (𝐴 ∩ ran 𝐹)(𝐹 “ {𝑦}) = (𝐹𝐴))
15 i1frn 23664 . . . 4 (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
16 inss2 3982 . . . 4 (𝐴 ∩ ran 𝐹) ⊆ ran 𝐹
17 ssfi 8340 . . . 4 ((ran 𝐹 ∈ Fin ∧ (𝐴 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝐴 ∩ ran 𝐹) ∈ Fin)
1815, 16, 17sylancl 574 . . 3 (𝐹 ∈ dom ∫1 → (𝐴 ∩ ran 𝐹) ∈ Fin)
19 i1fmbf 23662 . . . . . 6 (𝐹 ∈ dom ∫1𝐹 ∈ MblFn)
2019adantr 466 . . . . 5 ((𝐹 ∈ dom ∫1𝑦 ∈ (𝐴 ∩ ran 𝐹)) → 𝐹 ∈ MblFn)
211adantr 466 . . . . 5 ((𝐹 ∈ dom ∫1𝑦 ∈ (𝐴 ∩ ran 𝐹)) → 𝐹:ℝ⟶ℝ)
221frnd 6191 . . . . . . 7 (𝐹 ∈ dom ∫1 → ran 𝐹 ⊆ ℝ)
2316, 22syl5ss 3763 . . . . . 6 (𝐹 ∈ dom ∫1 → (𝐴 ∩ ran 𝐹) ⊆ ℝ)
2423sselda 3752 . . . . 5 ((𝐹 ∈ dom ∫1𝑦 ∈ (𝐴 ∩ ran 𝐹)) → 𝑦 ∈ ℝ)
25 mbfimasn 23620 . . . . 5 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ 𝑦 ∈ ℝ) → (𝐹 “ {𝑦}) ∈ dom vol)
2620, 21, 24, 25syl3anc 1476 . . . 4 ((𝐹 ∈ dom ∫1𝑦 ∈ (𝐴 ∩ ran 𝐹)) → (𝐹 “ {𝑦}) ∈ dom vol)
2726ralrimiva 3115 . . 3 (𝐹 ∈ dom ∫1 → ∀𝑦 ∈ (𝐴 ∩ ran 𝐹)(𝐹 “ {𝑦}) ∈ dom vol)
28 finiunmbl 23532 . . 3 (((𝐴 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∩ ran 𝐹)(𝐹 “ {𝑦}) ∈ dom vol) → 𝑦 ∈ (𝐴 ∩ ran 𝐹)(𝐹 “ {𝑦}) ∈ dom vol)
2918, 27, 28syl2anc 573 . 2 (𝐹 ∈ dom ∫1 𝑦 ∈ (𝐴 ∩ ran 𝐹)(𝐹 “ {𝑦}) ∈ dom vol)
3014, 29eqeltrrd 2851 1 (𝐹 ∈ dom ∫1 → (𝐹𝐴) ∈ dom vol)