Metamath Proof Explorer

Theorem smfpreimale

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded below is in the subspace sigma-algebra induced by its domain. See Proposition 121B (ii) of Fremlin1 p. 35 (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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