Metamath Proof Explorer


Theorem issmfled

Description: A sufficient condition for " F being a real-valued measurable function w.r.t. to the sigma-algebra S ". (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfled.a 𝑎 𝜑
issmfled.s ( 𝜑𝑆 ∈ SAlg )
issmfled.d ( 𝜑𝐷 𝑆 )
issmfled.f ( 𝜑𝐹 : 𝐷 ⟶ ℝ )
issmfled.6 ( ( 𝜑𝑎 ∈ ℝ ) → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t 𝐷 ) )
Assertion issmfled ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 issmfled.a 𝑎 𝜑
2 issmfled.s ( 𝜑𝑆 ∈ SAlg )
3 issmfled.d ( 𝜑𝐷 𝑆 )
4 issmfled.f ( 𝜑𝐹 : 𝐷 ⟶ ℝ )
5 issmfled.6 ( ( 𝜑𝑎 ∈ ℝ ) → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t 𝐷 ) )
6 4 fdmd ( 𝜑 → dom 𝐹 = 𝐷 )
7 6 3 eqsstrd ( 𝜑 → dom 𝐹 𝑆 )
8 4 ffdmd ( 𝜑𝐹 : dom 𝐹 ⟶ ℝ )
9 6 rabeqdv ( 𝜑 → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } = { 𝑥𝐷 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } )
10 6 oveq2d ( 𝜑 → ( 𝑆t dom 𝐹 ) = ( 𝑆t 𝐷 ) )
11 9 10 eleq12d ( 𝜑 → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t dom 𝐹 ) ↔ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t 𝐷 ) ) )
12 11 adantr ( ( 𝜑𝑎 ∈ ℝ ) → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t dom 𝐹 ) ↔ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t 𝐷 ) ) )
13 5 12 mpbird ( ( 𝜑𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t dom 𝐹 ) )
14 13 ex ( 𝜑 → ( 𝑎 ∈ ℝ → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t dom 𝐹 ) ) )
15 1 14 ralrimi ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t dom 𝐹 ) )
16 7 8 15 3jca ( 𝜑 → ( dom 𝐹 𝑆𝐹 : dom 𝐹 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t dom 𝐹 ) ) )
17 eqid dom 𝐹 = dom 𝐹
18 2 17 issmfle ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( dom 𝐹 𝑆𝐹 : dom 𝐹 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹𝑥 ) ≤ 𝑎 } ∈ ( 𝑆t dom 𝐹 ) ) ) )
19 16 18 mpbird ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )