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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 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 𝐷 ) ) ) )