Metamath Proof Explorer


Theorem issmfgtd

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

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

Proof

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