Metamath Proof Explorer

Theorem sibfima

Description: Any preimage of a singleton by a simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018)

Ref Expression
Hypotheses sitgval.b ⊢ B = Base W
sitgval.j ⊢ J = TopOpen ⁡ W
sitgval.s ⊢ S = 𝛔 ⁡ J
sitgval.0 ⊢ 0 ˙ = 0 W
sitgval.x ⊢ · ˙ = ⋅ W
sitgval.h ⊢ H = ℝHom ⁡ Scalar ⁡ W
sitgval.1 ⊢ φ → W ∈ V
sitgval.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
sibfmbl.1 ⊢ φ → F ∈ ℑ M W
Assertion sibfima ⊢ φ ∧ A ∈ ran ⁡ F ∖ 0 ˙ → M ⁡ F -1 A ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 sitgval.b ⊢ B = Base W
2 sitgval.j ⊢ J = TopOpen ⁡ W
3 sitgval.s ⊢ S = 𝛔 ⁡ J
4 sitgval.0 ⊢ 0 ˙ = 0 W
5 sitgval.x ⊢ · ˙ = ⋅ W
6 sitgval.h ⊢ H = ℝHom ⁡ Scalar ⁡ W
7 sitgval.1 ⊢ φ → W ∈ V
8 sitgval.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
9 sibfmbl.1 ⊢ φ → F ∈ ℑ M W
10 1 2 3 4 5 6 7 8 issibf ⊢ φ → F ∈ ℑ M W ↔ F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
11 9 10 mpbid ⊢ φ → F ∈ dom ⁡ M MblFn μ S ∧ ran ⁡ F ∈ Fin ∧ ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
12 11 simp3d ⊢ φ → ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞
13 sneq ⊢ x = A → x = A
14 13 imaeq2d ⊢ x = A → F -1 x = F -1 A
15 14 fveq2d ⊢ x = A → M ⁡ F -1 x = M ⁡ F -1 A
16 15 eleq1d ⊢ x = A → M ⁡ F -1 x ∈ 0 +∞ ↔ M ⁡ F -1 A ∈ 0 +∞
17 16 rspcv ⊢ A ∈ ran ⁡ F ∖ 0 ˙ → ∀ x ∈ ran ⁡ F ∖ 0 ˙ M ⁡ F -1 x ∈ 0 +∞ → M ⁡ F -1 A ∈ 0 +∞
18 12 17 mpan9 ⊢ φ ∧ A ∈ ran ⁡ F ∖ 0 ˙ → M ⁡ F -1 A ∈ 0 +∞