Metamath Proof Explorer


Theorem smfpreimalt

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 smfpreimalt.s ( 𝜑𝑆 ∈ SAlg )
smfpreimalt.f ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
smfpreimalt.d 𝐷 = dom 𝐹
smfpreimalt.a ( 𝜑𝐴 ∈ ℝ )
Assertion smfpreimalt ( 𝜑 → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝐴 } ∈ ( 𝑆t 𝐷 ) )

Proof

Step Hyp Ref Expression
1 smfpreimalt.s ( 𝜑𝑆 ∈ SAlg )
2 smfpreimalt.f ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3 smfpreimalt.d 𝐷 = dom 𝐹
4 smfpreimalt.a ( 𝜑𝐴 ∈ ℝ )
5 1 3 issmf ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝑆t 𝐷 ) ) ) )
6 2 5 mpbid ( 𝜑 → ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝑆t 𝐷 ) ) )
7 6 simp3d ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝑆t 𝐷 ) )
8 breq2 ( 𝑎 = 𝐴 → ( ( 𝐹𝑥 ) < 𝑎 ↔ ( 𝐹𝑥 ) < 𝐴 ) )
9 8 rabbidv ( 𝑎 = 𝐴 → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑎 } = { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝐴 } )
10 9 eleq1d ( 𝑎 = 𝐴 → ( { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝑆t 𝐷 ) ↔ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝐴 } ∈ ( 𝑆t 𝐷 ) ) )
11 10 rspcva ( ( 𝐴 ∈ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝑆t 𝐷 ) ) → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝐴 } ∈ ( 𝑆t 𝐷 ) )
12 4 7 11 syl2anc ( 𝜑 → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝐴 } ∈ ( 𝑆t 𝐷 ) )