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

Detailed syntax breakdown

Step Hyp Ref Expression
0 csmblfn 
 |-  SMblFn
1 vs 
 |-  s
2 csalg 
 |-  SAlg
3 vf 
 |-  f
4 cr 
 |-  RR
5 cpm 
 |-  ^pm
6 1 cv 
 |-  s
7 6 cuni 
 |-  U. s
8 4 7 5 co 
 |-  ( RR ^pm U. s )
9 va 
 |-  a
10 3 cv 
 |-  f
11 10 ccnv 
 |-  `' f
12 cmnf 
 |-  -oo
13 cioo 
 |-  (,)
14 9 cv 
 |-  a
15 12 14 13 co 
 |-  ( -oo (,) a )
16 11 15 cima 
 |-  ( `' f " ( -oo (,) a ) )
17 crest 
 |-  |`t
18 10 cdm 
 |-  dom f
19 6 18 17 co 
 |-  ( s |`t dom f )
20 16 19 wcel 
 |-  ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f )
21 20 9 4 wral 
 |-  A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f )
22 21 3 8 crab 
 |-  { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) }
23 1 2 22 cmpt 
 |-  ( s e. SAlg |-> { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) } )
24 0 23 wceq 
 |-  SMblFn = ( s e. SAlg |-> { f e. ( RR ^pm U. s ) | A. a e. RR ( `' f " ( -oo (,) a ) ) e. ( s |`t dom f ) } )