Definition df-smblfn 43335

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.)

Assertion

Ref	Expression
df-smblfn	⊢ SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})

Distinct variable group:   𝑓,𝑠,𝑎

Detailed syntax breakdown of Definition df-smblfn

Step	Hyp	Ref	Expression
1		csmblfn 43334	. 2 class SMblFn
2		vs	. . 3 setvar 𝑠
3		csalg 42950	. . 3 class SAlg
4		vf	. . . . . . . . 9 setvar 𝑓
5	4	cv 1537	. . . . . . . 8 class 𝑓
6	5	ccnv 5518	. . . . . . 7 class ◡𝑓
7		cmnf 10662	. . . . . . . 8 class -∞
8		va	. . . . . . . . 9 setvar 𝑎
9	8	cv 1537	. . . . . . . 8 class 𝑎
10		cioo 12726	. . . . . . . 8 class (,)
11	7, 9, 10	co 7135	. . . . . . 7 class (-∞(,)𝑎)
12	6, 11	cima 5522	. . . . . 6 class (◡𝑓 “ (-∞(,)𝑎))
13	2	cv 1537	. . . . . . 7 class 𝑠
14	5	cdm 5519	. . . . . . 7 class dom 𝑓
15		crest 16686	. . . . . . 7 class ↾t
16	13, 14, 15	co 7135	. . . . . 6 class (𝑠 ↾t dom 𝑓)
17	12, 16	wcel 2111	. . . . 5 wff (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)
18		cr 10525	. . . . 5 class ℝ
19	17, 8, 18	wral 3106	. . . 4 wff ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)
20	13	cuni 4800	. . . . 5 class ∪ 𝑠
21		cpm 8390	. . . . 5 class ↑pm
22	18, 20, 21	co 7135	. . . 4 class (ℝ ↑pm ∪ 𝑠)
23	19, 4, 22	crab 3110	. . 3 class {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}
24	2, 3, 23	cmpt 5110	. 2 class (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})
25	1, 24	wceq 1538	1 wff SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)})

This definition is referenced by:  issmflem  43361