Metamath Proof Explorer

Theorem smfpreimage

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

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

Proof

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