Metamath Proof Explorer

Definition df-smblfn

Description: Define a real-valued measurable function w.r.t. a given sigma-algebra. See Definition 121C of Fremlin1 p. 36 and Definition 135E (b) of Fremlin1 p. 80 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Assertion df-smblfn ⊢ SMblFn = s ∈ SAlg ⟼ f ∈ ℝ ↑ 𝑝𝑚 ⋃ s | ∀ a ∈ ℝ f -1 −∞ a ∈ s ↾ 𝑡 dom ⁡ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 csmblfn class SMblFn
1 vs setvar s
2 csalg class SAlg
3 vf setvar f
4 cr class ℝ
5 cpm class ↑ 𝑝𝑚
6 1 cv setvar s
7 6 cuni class ⋃ s
8 4 7 5 co class ℝ ↑ 𝑝𝑚 ⋃ s
9 va setvar a
10 3 cv setvar f
11 10 ccnv class f -1
12 cmnf class −∞
13 cioo class .
14 9 cv setvar a
15 12 14 13 co class −∞ a
16 11 15 cima class f -1 −∞ a
17 crest class ↾ 𝑡
18 10 cdm class dom ⁡ f
19 6 18 17 co class s ↾ 𝑡 dom ⁡ f
20 16 19 wcel wff f -1 −∞ a ∈ s ↾ 𝑡 dom ⁡ f
21 20 9 4 wral wff ∀ a ∈ ℝ f -1 −∞ a ∈ s ↾ 𝑡 dom ⁡ f
22 21 3 8 crab class f ∈ ℝ ↑ 𝑝𝑚 ⋃ s | ∀ a ∈ ℝ f -1 −∞ a ∈ s ↾ 𝑡 dom ⁡ f
23 1 2 22 cmpt class s ∈ SAlg ⟼ f ∈ ℝ ↑ 𝑝𝑚 ⋃ s | ∀ a ∈ ℝ f -1 −∞ a ∈ s ↾ 𝑡 dom ⁡ f
24 0 23 wceq wff SMblFn = s ∈ SAlg ⟼ f ∈ ℝ ↑ 𝑝𝑚 ⋃ s | ∀ a ∈ ℝ f -1 −∞ a ∈ s ↾ 𝑡 dom ⁡ f