Metamath Proof Explorer

Theorem issmfge

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 left-closed intervals unbounded above 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 (iv) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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