Metamath Proof Explorer

Theorem issmflelem

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 right-closed intervals unbounded below 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 (ii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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