Metamath Proof Explorer

Theorem issmfle

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 right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of F is required to be b subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (ii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfle.s 
|- ( ph -> S e. SAlg )
issmfle.d 
|- D = dom F
Assertion issmfle 
|- ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) ) ) )

Proof

Step Hyp Ref Expression
1 issmfle.s 
 |-  ( ph -> S e. SAlg )
2 issmfle.d 
 |-  D = dom F
3 1 adantr 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> S e. SAlg )
4 simpr 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> F e. ( SMblFn ` S ) )
5 3 4 2 smfdmss 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> D C_ U. S )
6 3 4 2 smff 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> F : D --> RR )
7 nfv 
 |-  F/ b ph
8 nfv 
 |-  F/ b F e. ( SMblFn ` S )
9 7 8 nfan 
 |-  F/ b ( ph /\ F e. ( SMblFn ` S ) )
10 nfv 
 |-  F/ y ph
11 nfv 
 |-  F/ y F e. ( SMblFn ` S )
12 10 11 nfan 
 |-  F/ y ( ph /\ F e. ( SMblFn ` S ) )
13 nfv 
 |-  F/ y b e. RR
14 12 13 nfan 
 |-  F/ y ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR )
15 nfv 
 |-  F/ c ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR )
16 1 uniexd 
 |-  ( ph -> U. S e. _V )
17 16 adantr 
 |-  ( ( ph /\ D C_ U. S ) -> U. S e. _V )
18 simpr 
 |-  ( ( ph /\ D C_ U. S ) -> D C_ U. S )
19 17 18 ssexd 
 |-  ( ( ph /\ D C_ U. S ) -> D e. _V )
20 5 19 syldan 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> D e. _V )
21 eqid 
 |-  ( S |`t D ) = ( S |`t D )
22 3 20 21 subsalsal 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( S |`t D ) e. SAlg )
23 22 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> ( S |`t D ) e. SAlg )
24 6 frexr 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> F : D --> RR* )
25 24 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> F : D --> RR* )
26 25 ffvelrnda 
 |-  ( ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) /\ y e. D ) -> ( F ` y ) e. RR* )
27 3 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ c e. RR ) -> S e. SAlg )
28 4 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ c e. RR ) -> F e. ( SMblFn ` S ) )
29 simpr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ c e. RR ) -> c e. RR )
30 27 28 2 29 smfpreimalt 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ c e. RR ) -> { y e. D | ( F ` y ) < c } e. ( S |`t D ) )
31 30 adantlr 
 |-  ( ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) /\ c e. RR ) -> { y e. D | ( F ` y ) < c } e. ( S |`t D ) )
32 simpr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> b e. RR )
33 14 15 23 26 31 32 salpreimaltle 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) )
34 33 ex 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( b e. RR -> { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) )
35 9 34 ralrimi 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) )
36 5 6 35 3jca 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) )
37 36 ex 
 |-  ( ph -> ( F e. ( SMblFn ` S ) -> ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) ) )
38 nfv 
 |-  F/ y D C_ U. S
39 nfv 
 |-  F/ y F : D --> RR
40 nfcv 
 |-  F/_ y RR
41 nfrab1 
 |-  F/_ y { y e. D | ( F ` y ) <_ b }
42 nfcv 
 |-  F/_ y ( S |`t D )
43 41 42 nfel 
 |-  F/ y { y e. D | ( F ` y ) <_ b } e. ( S |`t D )
44 40 43 nfralw 
 |-  F/ y A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D )
45 38 39 44 nf3an 
 |-  F/ y ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) )
46 10 45 nfan 
 |-  F/ y ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) )
47 nfv 
 |-  F/ b D C_ U. S
48 nfv 
 |-  F/ b F : D --> RR
49 nfra1 
 |-  F/ b A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D )
50 47 48 49 nf3an 
 |-  F/ b ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) )
51 7 50 nfan 
 |-  F/ b ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) )
52 1 adantr 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) ) -> S e. SAlg )
53 simpr1 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) ) -> D C_ U. S )
54 simpr2 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) ) -> F : D --> RR )
55 rspa 
 |-  ( ( A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) /\ b e. RR ) -> { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) )
56 55 3ad2antl3 
 |-  ( ( ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) /\ b e. RR ) -> { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) )
57 56 adantll 
 |-  ( ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) ) /\ b e. RR ) -> { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) )
58 46 51 52 2 53 54 57 issmflelem 
 |-  ( ( ph /\ ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) ) -> F e. ( SMblFn ` S ) )
59 58 ex 
 |-  ( ph -> ( ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) -> F e. ( SMblFn ` S ) ) )
60 37 59 impbid 
 |-  ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) ) )
61 breq2 
 |-  ( b = a -> ( ( F ` y ) <_ b <-> ( F ` y ) <_ a ) )
62 61 rabbidv 
 |-  ( b = a -> { y e. D | ( F ` y ) <_ b } = { y e. D | ( F ` y ) <_ a } )
63 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
64 63 breq1d 
 |-  ( y = x -> ( ( F ` y ) <_ a <-> ( F ` x ) <_ a ) )
65 64 cbvrabv 
 |-  { y e. D | ( F ` y ) <_ a } = { x e. D | ( F ` x ) <_ a }
66 65 a1i 
 |-  ( b = a -> { y e. D | ( F ` y ) <_ a } = { x e. D | ( F ` x ) <_ a } )
67 62 66 eqtrd 
 |-  ( b = a -> { y e. D | ( F ` y ) <_ b } = { x e. D | ( F ` x ) <_ a } )
68 67 eleq1d 
 |-  ( b = a -> ( { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) <-> { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) ) )
69 68 cbvralvw 
 |-  ( A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) <-> A. a e. RR { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) )
70 69 3anbi3i 
 |-  ( ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) ) )
71 70 a1i 
 |-  ( ph -> ( ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | ( F ` y ) <_ b } e. ( S |`t D ) ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) ) ) )
72 60 71 bitrd 
 |-  ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) <_ a } e. ( S |`t D ) ) ) )