Metamath Proof Explorer


Theorem issmfge

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 b 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 issmfge.s ( 𝜑𝑆 ∈ SAlg )
issmfge.d 𝐷 = dom 𝐹
Assertion issmfge ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 issmfge.s ( 𝜑𝑆 ∈ SAlg )
2 issmfge.d 𝐷 = dom 𝐹
3 1 adantr ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝑆 ∈ SAlg )
4 simpr ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
5 3 4 2 smfdmss ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐷 𝑆 )
6 3 4 2 smff ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 : 𝐷 ⟶ ℝ )
7 nfv 𝑦 𝜑
8 nfv 𝑦 𝐹 ∈ ( SMblFn ‘ 𝑆 )
9 7 8 nfan 𝑦 ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
10 nfv 𝑦 𝑏 ∈ ℝ
11 9 10 nfan 𝑦 ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ )
12 nfv 𝑐 ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ )
13 1 uniexd ( 𝜑 𝑆 ∈ V )
14 13 adantr ( ( 𝜑𝐷 𝑆 ) → 𝑆 ∈ V )
15 simpr ( ( 𝜑𝐷 𝑆 ) → 𝐷 𝑆 )
16 14 15 ssexd ( ( 𝜑𝐷 𝑆 ) → 𝐷 ∈ V )
17 5 16 syldan ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐷 ∈ V )
18 eqid ( 𝑆t 𝐷 ) = ( 𝑆t 𝐷 )
19 3 17 18 subsalsal ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝑆t 𝐷 ) ∈ SAlg )
20 19 adantr ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → ( 𝑆t 𝐷 ) ∈ SAlg )
21 6 ffvelrnda ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑦𝐷 ) → ( 𝐹𝑦 ) ∈ ℝ )
22 21 rexrd ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑦𝐷 ) → ( 𝐹𝑦 ) ∈ ℝ* )
23 22 adantlr ( ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) ∧ 𝑦𝐷 ) → ( 𝐹𝑦 ) ∈ ℝ* )
24 3 adantr ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → 𝑆 ∈ SAlg )
25 4 adantr ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
26 simpr ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → 𝑐 ∈ ℝ )
27 24 25 2 26 smfpreimagt ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → { 𝑦𝐷𝑐 < ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) )
28 27 adantlr ( ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) ∧ 𝑐 ∈ ℝ ) → { 𝑦𝐷𝑐 < ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) )
29 simpr ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
30 11 12 20 23 28 29 salpreimagtge ( ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) )
31 30 ralrimiva ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) )
32 5 6 31 3jca ( ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) )
33 32 ex ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) → ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ) )
34 nfv 𝑦 𝐷 𝑆
35 nfv 𝑦 𝐹 : 𝐷 ⟶ ℝ
36 nfcv 𝑦
37 nfrab1 𝑦 { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) }
38 nfcv 𝑦 ( 𝑆t 𝐷 )
39 37 38 nfel 𝑦 { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 )
40 36 39 nfralw 𝑦𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 )
41 34 35 40 nf3an 𝑦 ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) )
42 7 41 nfan 𝑦 ( 𝜑 ∧ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) )
43 nfv 𝑏 𝜑
44 nfv 𝑏 𝐷 𝑆
45 nfv 𝑏 𝐹 : 𝐷 ⟶ ℝ
46 nfra1 𝑏𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 )
47 44 45 46 nf3an 𝑏 ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) )
48 43 47 nfan 𝑏 ( 𝜑 ∧ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) )
49 1 adantr ( ( 𝜑 ∧ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ) → 𝑆 ∈ SAlg )
50 simpr1 ( ( 𝜑 ∧ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ) → 𝐷 𝑆 )
51 simpr2 ( ( 𝜑 ∧ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ) → 𝐹 : 𝐷 ⟶ ℝ )
52 simpr3 ( ( 𝜑 ∧ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ) → ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) )
53 42 48 49 2 50 51 52 issmfgelem ( ( 𝜑 ∧ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
54 53 ex ( 𝜑 → ( ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) )
55 33 54 impbid ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ) )
56 breq1 ( 𝑏 = 𝑎 → ( 𝑏 ≤ ( 𝐹𝑦 ) ↔ 𝑎 ≤ ( 𝐹𝑦 ) ) )
57 56 rabbidv ( 𝑏 = 𝑎 → { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } = { 𝑦𝐷𝑎 ≤ ( 𝐹𝑦 ) } )
58 fveq2 ( 𝑦 = 𝑥 → ( 𝐹𝑦 ) = ( 𝐹𝑥 ) )
59 58 breq2d ( 𝑦 = 𝑥 → ( 𝑎 ≤ ( 𝐹𝑦 ) ↔ 𝑎 ≤ ( 𝐹𝑥 ) ) )
60 59 cbvrabv { 𝑦𝐷𝑎 ≤ ( 𝐹𝑦 ) } = { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) }
61 60 a1i ( 𝑏 = 𝑎 → { 𝑦𝐷𝑎 ≤ ( 𝐹𝑦 ) } = { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } )
62 57 61 eqtrd ( 𝑏 = 𝑎 → { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } = { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } )
63 62 eleq1d ( 𝑏 = 𝑎 → ( { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ↔ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ) )
64 63 cbvralvw ( ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ↔ ∀ 𝑎 ∈ ℝ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) )
65 64 3anbi3i ( ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ↔ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ) )
66 65 a1i ( 𝜑 → ( ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦𝐷𝑏 ≤ ( 𝐹𝑦 ) } ∈ ( 𝑆t 𝐷 ) ) ↔ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ) ) )
67 55 66 bitrd ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷𝑎 ≤ ( 𝐹𝑥 ) } ∈ ( 𝑆t 𝐷 ) ) ) )