Metamath Proof Explorer

Theorem smfpreimaltf

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpreimaltf.x ⊢ Ⅎ _ x F
smfpreimaltf.s ⊢ φ → S ∈ SAlg
smfpreimaltf.f ⊢ φ → F ∈ SMblFn ⁡ S
smfpreimaltf.d ⊢ D = dom ⁡ F
smfpreimaltf.a ⊢ φ → A ∈ ℝ
Assertion smfpreimaltf ⊢ φ → x ∈ D | F ⁡ x < A ∈ S ↾ 𝑡 D

Proof

Step Hyp Ref Expression
1 smfpreimaltf.x ⊢ Ⅎ _ x F
2 smfpreimaltf.s ⊢ φ → S ∈ SAlg
3 smfpreimaltf.f ⊢ φ → F ∈ SMblFn ⁡ S
4 smfpreimaltf.d ⊢ D = dom ⁡ F
5 smfpreimaltf.a ⊢ φ → A ∈ ℝ
6 1 2 4 issmff ⊢ φ → F ∈ SMblFn ⁡ S ↔ D ⊆ ⋃ S ∧ F : D ⟶ ℝ ∧ ∀ a ∈ ℝ x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D
7 3 6 mpbid ⊢ φ → D ⊆ ⋃ S ∧ F : D ⟶ ℝ ∧ ∀ a ∈ ℝ x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D
8 7 simp3d ⊢ φ → ∀ a ∈ ℝ x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D
9 breq2 ⊢ a = A → F ⁡ x < a ↔ F ⁡ x < A
10 9 rabbidv ⊢ a = A → x ∈ D | F ⁡ x < a = x ∈ D | F ⁡ x < A
11 10 eleq1d ⊢ a = A → x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D ↔ x ∈ D | F ⁡ x < A ∈ S ↾ 𝑡 D
12 11 rspcva ⊢ A ∈ ℝ ∧ ∀ a ∈ ℝ x ∈ D | F ⁡ x < a ∈ S ↾ 𝑡 D → x ∈ D | F ⁡ x < A ∈ S ↾ 𝑡 D
13 5 8 12 syl2anc ⊢ φ → x ∈ D | F ⁡ x < A ∈ S ↾ 𝑡 D