Metamath Proof Explorer


Theorem issmfgelem

Description: The predicate " F is a real-valued measurable function w.r.t. to the sigma-algebra S ". A function is measurable iff the preimages of all left-closed intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of F is required to be a subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (iv) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfgelem.x 𝑥 𝜑
issmfgelem.a 𝑎 𝜑
issmfgelem.s ( 𝜑𝑆 ∈ SAlg )
issmfgelem.d 𝐷 = dom 𝐹
issmfgelem.i ( 𝜑𝐷 𝑆 )
issmfgelem.f ( 𝜑𝐹 : 𝐷 ⟶ ℝ )
issmfgelem.p ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
Assertion issmfgelem ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 issmfgelem.x 𝑥 𝜑
2 issmfgelem.a 𝑎 𝜑
3 issmfgelem.s ( 𝜑𝑆 ∈ SAlg )
4 issmfgelem.d 𝐷 = dom 𝐹
5 issmfgelem.i ( 𝜑𝐷 𝑆 )
6 issmfgelem.f ( 𝜑𝐹 : 𝐷 ⟶ ℝ )
7 issmfgelem.p ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
8 3 5 restuni4 ( 𝜑 ( 𝑆t 𝐷 ) = 𝐷 )
9 8 eqcomd ( 𝜑𝐷 = ( 𝑆t 𝐷 ) )
10 9 rabeqdv ( 𝜑 → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑏 } = { 𝑥 ( 𝑆t 𝐷 ) ∣ ( 𝐹𝑥 ) < 𝑏 } )
11 10 adantr ( ( 𝜑𝑏 ∈ ℝ ) → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑏 } = { 𝑥 ( 𝑆t 𝐷 ) ∣ ( 𝐹𝑥 ) < 𝑏 } )
12 nfv 𝑥 𝑏 ∈ ℝ
13 1 12 nfan 𝑥 ( 𝜑𝑏 ∈ ℝ )
14 nfv 𝑎 𝑏 ∈ ℝ
15 2 14 nfan 𝑎 ( 𝜑𝑏 ∈ ℝ )
16 3 uniexd ( 𝜑 𝑆 ∈ V )
17 16 adantr ( ( 𝜑𝐷 𝑆 ) → 𝑆 ∈ V )
18 simpr ( ( 𝜑𝐷 𝑆 ) → 𝐷 𝑆 )
19 17 18 ssexd ( ( 𝜑𝐷 𝑆 ) → 𝐷 ∈ V )
20 5 19 mpdan ( 𝜑𝐷 ∈ V )
21 eqid ( 𝑆t 𝐷 ) = ( 𝑆t 𝐷 )
22 3 20 21 subsalsal ( 𝜑 → ( 𝑆t 𝐷 ) ∈ SAlg )
23 22 adantr ( ( 𝜑𝑏 ∈ ℝ ) → ( 𝑆t 𝐷 ) ∈ SAlg )
24 eqid ( 𝑆t 𝐷 ) = ( 𝑆t 𝐷 )
25 6 adantr ( ( 𝜑𝑥 ( 𝑆t 𝐷 ) ) → 𝐹 : 𝐷 ⟶ ℝ )
26 simpr ( ( 𝜑𝑥 ( 𝑆t 𝐷 ) ) → 𝑥 ( 𝑆t 𝐷 ) )
27 8 adantr ( ( 𝜑𝑥 ( 𝑆t 𝐷 ) ) → ( 𝑆t 𝐷 ) = 𝐷 )
28 26 27 eleqtrd ( ( 𝜑𝑥 ( 𝑆t 𝐷 ) ) → 𝑥𝐷 )
29 25 28 ffvelrnd ( ( 𝜑𝑥 ( 𝑆t 𝐷 ) ) → ( 𝐹𝑥 ) ∈ ℝ )
30 29 rexrd ( ( 𝜑𝑥 ( 𝑆t 𝐷 ) ) → ( 𝐹𝑥 ) ∈ ℝ* )
31 30 adantlr ( ( ( 𝜑𝑏 ∈ ℝ ) ∧ 𝑥 ( 𝑆t 𝐷 ) ) → ( 𝐹𝑥 ) ∈ ℝ* )
32 9 rabeqdv ( 𝜑 → { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } = { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } )
33 32 eleq1d ( 𝜑 → ( { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ↔ { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ) )
34 2 33 ralbid ( 𝜑 → ( ∀ 𝑎 ∈ ℝ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ↔ ∀ 𝑎 ∈ ℝ { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ) )
35 7 34 mpbid ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
36 35 adantr ( ( 𝜑𝑎 ∈ ℝ ) → ∀ 𝑎 ∈ ℝ { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
37 simpr ( ( 𝜑𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
38 rspa ( ( ∀ 𝑎 ∈ ℝ { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ∧ 𝑎 ∈ ℝ ) → { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
39 36 37 38 syl2anc ( ( 𝜑𝑎 ∈ ℝ ) → { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
40 39 adantlr ( ( ( 𝜑𝑏 ∈ ℝ ) ∧ 𝑎 ∈ ℝ ) → { 𝑥 ( 𝑆t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
41 simpr ( ( 𝜑𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
42 13 15 23 24 31 40 41 salpreimagelt ( ( 𝜑𝑏 ∈ ℝ ) → { 𝑥 ( 𝑆t 𝐷 ) ∣ ( 𝐹𝑥 ) < 𝑏 } ∈ ( 𝑆t 𝐷 ) )
43 11 42 eqeltrd ( ( 𝜑𝑏 ∈ ℝ ) → { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑏 } ∈ ( 𝑆t 𝐷 ) )
44 43 ralrimiva ( 𝜑 → ∀ 𝑏 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑏 } ∈ ( 𝑆t 𝐷 ) )
45 5 6 44 3jca ( 𝜑 → ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑏 } ∈ ( 𝑆t 𝐷 ) ) )
46 3 4 issmf ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑏 } ∈ ( 𝑆t 𝐷 ) ) ) )
47 45 46 mpbird ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )