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

Proof

Step Hyp Ref Expression
1 smfpreimale.s ( 𝜑𝑆 ∈ SAlg )
2 smfpreimale.f ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3 smfpreimale.d 𝐷 = dom 𝐹
4 smfpreimale.a ( 𝜑𝐴 ∈ ℝ )
5 1 3 issmfle ( 𝜑 → ( 𝐹 ∈ ( 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 𝐷 ) )