Definition df-smblfn 40910

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 = ( s e. SAlg |-> { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s ↾t dom f ) } )

Distinct variable group:   f, s, a

Detailed syntax breakdown of Definition df-smblfn

Step	Hyp	Ref	Expression
1		csmblfn 40909	. 2 class SMblFn
2		vs	. . 3 setvar s
3		csalg 40528	. . 3 class SAlg
4		vf	. . . . . . . . 9 setvar f
5	4	cv 1482	. . . . . . . 8 class f
6	5	ccnv 5113	. . . . . . 7 class `' f
7		cmnf 10072	. . . . . . . 8 class -oo
8		va	. . . . . . . . 9 setvar a
9	8	cv 1482	. . . . . . . 8 class a
10		cioo 12175	. . . . . . . 8 class (,)
11	7, 9, 10	co 6650	. . . . . . 7 class ( -oo (,) a )
12	6, 11	cima 5117	. . . . . 6 class ( `' f " ( -oo (,) a ) )
13	2	cv 1482	. . . . . . 7 class s
14	5	cdm 5114	. . . . . . 7 class dom f
15		crest 16081	. . . . . . 7 class ↾t
16	13, 14, 15	co 6650	. . . . . 6 class ( s ↾t dom f )
17	12, 16	wcel 1990	. . . . 5 wff ( `' f " ( -oo (,) a ) ) e. ( s ↾t dom f )
18		cr 9935	. . . . 5 class RR
19	17, 8, 18	wral 2912	. . . 4 wff A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s ↾t dom f )
20	13	cuni 4436	. . . . 5 class U. s
21		cpm 7858	. . . . 5 class ^pm
22	18, 20, 21	co 6650	. . . 4 class ( RR ^pm U. s )
23	19, 4, 22	crab 2916	. . 3 class { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s ↾t dom f ) }
24	2, 3, 23	cmpt 4729	. 2 class ( s e. SAlg |-> { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s ↾t dom f ) } )
25	1, 24	wceq 1483	1 wff SMblFn = ( s e. SAlg |-> { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s ↾t dom f ) } )

This definition is referenced by:  issmflem  40936