Metamath Proof Explorer

Theorem issmfgtlem

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-open 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 (iii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfgtlem.x ⊢ Ⅎ 𝑥 𝜑
issmfgtlem.a ⊢ Ⅎ 𝑎 𝜑
issmfgtlem.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
issmfgtlem.d ⊢ 𝐷 = dom 𝐹
issmfgtlem.i ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
issmfgtlem.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
issmfgtlem.p ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
Assertion issmfgtlem ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 issmfgtlem.x ⊢ Ⅎ 𝑥 𝜑
2 issmfgtlem.a ⊢ Ⅎ 𝑎 𝜑
3 issmfgtlem.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4 issmfgtlem.d ⊢ 𝐷 = dom 𝐹
5 issmfgtlem.i ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
6 issmfgtlem.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
7 issmfgtlem.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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
30 29 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
31 30 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
32 8 rabeqdv ⊢ ( 𝜑 → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } )
34 7 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
35 33 34 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
36 35 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
38 13 15 23 24 31 36 37 salpreimagtlt ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
39 11 38 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
40 39 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
41 5 6 40 3jca ⊢ ( 𝜑 → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
42 3 4 issmf ⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
43 41 42 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )