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 ⊢ Ⅎ x φ
issmfgelem.a ⊢ Ⅎ a φ
issmfgelem.s ⊢ φ → S ∈ SAlg
issmfgelem.d ⊢ D = dom ⁡ F
issmfgelem.i ⊢ φ → D ⊆ ⋃ S
issmfgelem.f ⊢ φ → F : D ⟶ ℝ
issmfgelem.p ⊢ φ → ∀ a ∈ ℝ x ∈ D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
Assertion issmfgelem ⊢ φ → F ∈ SMblFn ⁡ S

Proof

Step Hyp Ref Expression
1 issmfgelem.x ⊢ Ⅎ x φ
2 issmfgelem.a ⊢ Ⅎ a φ
3 issmfgelem.s ⊢ φ → S ∈ SAlg
4 issmfgelem.d ⊢ D = dom ⁡ F
5 issmfgelem.i ⊢ φ → D ⊆ ⋃ S
6 issmfgelem.f ⊢ φ → F : D ⟶ ℝ
7 issmfgelem.p ⊢ φ → ∀ a ∈ ℝ x ∈ D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
8 3 5 restuni4 ⊢ φ → ⋃ S ↾ 𝑡 D = D
9 8 eqcomd ⊢ φ → D = ⋃ S ↾ 𝑡 D
10 9 rabeqdv ⊢ φ → x ∈ D | F ⁡ x < b = x ∈ ⋃ S ↾ 𝑡 D | F ⁡ x < b
11 10 adantr ⊢ φ ∧ b ∈ ℝ → x ∈ D | F ⁡ x < b = x ∈ ⋃ S ↾ 𝑡 D | F ⁡ x < b
12 nfv ⊢ Ⅎ x b ∈ ℝ
13 1 12 nfan ⊢ Ⅎ x φ ∧ b ∈ ℝ
14 nfv ⊢ Ⅎ a b ∈ ℝ
15 2 14 nfan ⊢ Ⅎ a φ ∧ b ∈ ℝ
16 3 uniexd ⊢ φ → ⋃ S ∈ V
17 16 adantr ⊢ φ ∧ D ⊆ ⋃ S → ⋃ S ∈ V
18 simpr ⊢ φ ∧ D ⊆ ⋃ S → D ⊆ ⋃ S
19 17 18 ssexd ⊢ φ ∧ D ⊆ ⋃ S → D ∈ V
20 5 19 mpdan ⊢ φ → D ∈ V
21 eqid ⊢ S ↾ 𝑡 D = S ↾ 𝑡 D
22 3 20 21 subsalsal ⊢ φ → S ↾ 𝑡 D ∈ SAlg
23 22 adantr ⊢ φ ∧ b ∈ ℝ → S ↾ 𝑡 D ∈ SAlg
24 eqid ⊢ ⋃ S ↾ 𝑡 D = ⋃ S ↾ 𝑡 D
25 6 adantr ⊢ φ ∧ x ∈ ⋃ S ↾ 𝑡 D → F : D ⟶ ℝ
26 simpr ⊢ φ ∧ x ∈ ⋃ S ↾ 𝑡 D → x ∈ ⋃ S ↾ 𝑡 D
27 8 adantr ⊢ φ ∧ x ∈ ⋃ S ↾ 𝑡 D → ⋃ S ↾ 𝑡 D = D
28 26 27 eleqtrd ⊢ φ ∧ x ∈ ⋃ S ↾ 𝑡 D → x ∈ D
29 25 28 ffvelrnd ⊢ φ ∧ x ∈ ⋃ S ↾ 𝑡 D → F ⁡ x ∈ ℝ
30 29 rexrd ⊢ φ ∧ x ∈ ⋃ S ↾ 𝑡 D → F ⁡ x ∈ ℝ *
31 30 adantlr ⊢ φ ∧ b ∈ ℝ ∧ x ∈ ⋃ S ↾ 𝑡 D → F ⁡ x ∈ ℝ *
32 9 rabeqdv ⊢ φ → x ∈ D | a ≤ F ⁡ x = x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x
33 32 eleq1d ⊢ φ → x ∈ D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D ↔ x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
34 2 33 ralbid ⊢ φ → ∀ a ∈ ℝ x ∈ D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D ↔ ∀ a ∈ ℝ x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
35 7 34 mpbid ⊢ φ → ∀ a ∈ ℝ x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
36 35 adantr ⊢ φ ∧ a ∈ ℝ → ∀ a ∈ ℝ x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
37 simpr ⊢ φ ∧ a ∈ ℝ → a ∈ ℝ
38 rspa ⊢ ∀ a ∈ ℝ x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D ∧ a ∈ ℝ → x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
39 36 37 38 syl2anc ⊢ φ ∧ a ∈ ℝ → x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
40 39 adantlr ⊢ φ ∧ b ∈ ℝ ∧ a ∈ ℝ → x ∈ ⋃ S ↾ 𝑡 D | a ≤ F ⁡ x ∈ S ↾ 𝑡 D
41 simpr ⊢ φ ∧ b ∈ ℝ → b ∈ ℝ
42 13 15 23 24 31 40 41 salpreimagelt ⊢ φ ∧ b ∈ ℝ → x ∈ ⋃ S ↾ 𝑡 D | F ⁡ x < b ∈ S ↾ 𝑡 D
43 11 42 eqeltrd ⊢ φ ∧ b ∈ ℝ → x ∈ D | F ⁡ x < b ∈ S ↾ 𝑡 D
44 43 ralrimiva ⊢ φ → ∀ b ∈ ℝ x ∈ D | F ⁡ x < b ∈ S ↾ 𝑡 D
45 5 6 44 3jca ⊢ φ → D ⊆ ⋃ S ∧ F : D ⟶ ℝ ∧ ∀ b ∈ ℝ x ∈ D | F ⁡ x < b ∈ S ↾ 𝑡 D
46 3 4 issmf ⊢ φ → F ∈ SMblFn ⁡ S ↔ D ⊆ ⋃ S ∧ F : D ⟶ ℝ ∧ ∀ b ∈ ℝ x ∈ D | F ⁡ x < b ∈ S ↾ 𝑡 D
47 45 46 mpbird ⊢ φ → F ∈ SMblFn ⁡ S