Metamath Proof Explorer

Theorem issmfgt

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-open 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 (iii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfgt.s 
|- ( ph -> S e. SAlg )
issmfgt.d 
|- D = dom F
Assertion issmfgt 
|- ( 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 issmfgt.s 
 |-  ( ph -> S e. SAlg )
2 issmfgt.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 3 5 restuni4 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> U. ( S |`t D ) = D )
11 10 eqcomd 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> D = U. ( S |`t D ) )
12 11 rabeqdv 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> { y e. D | b < ( F ` y ) } = { y e. U. ( S |`t D ) | b < ( F ` y ) } )
13 12 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> { y e. D | b < ( F ` y ) } = { y e. U. ( S |`t D ) | b < ( F ` y ) } )
14 nfv 
 |-  F/ y ph
15 nfv 
 |-  F/ y F e. ( SMblFn ` S )
16 14 15 nfan 
 |-  F/ y ( ph /\ F e. ( SMblFn ` S ) )
17 nfv 
 |-  F/ y b e. RR
18 16 17 nfan 
 |-  F/ y ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR )
19 nfv 
 |-  F/ c ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR )
20 1 uniexd 
 |-  ( ph -> U. S e. _V )
21 20 adantr 
 |-  ( ( ph /\ D C_ U. S ) -> U. S e. _V )
22 simpr 
 |-  ( ( ph /\ D C_ U. S ) -> D C_ U. S )
23 21 22 ssexd 
 |-  ( ( ph /\ D C_ U. S ) -> D e. _V )
24 5 23 syldan 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> D e. _V )
25 eqid 
 |-  ( S |`t D ) = ( S |`t D )
26 3 24 25 subsalsal 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( S |`t D ) e. SAlg )
27 26 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> ( S |`t D ) e. SAlg )
28 eqid 
 |-  U. ( S |`t D ) = U. ( S |`t D )
29 6 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ y e. U. ( S |`t D ) ) -> F : D --> RR )
30 simpr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ y e. U. ( S |`t D ) ) -> y e. U. ( S |`t D ) )
31 10 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ y e. U. ( S |`t D ) ) -> U. ( S |`t D ) = D )
32 30 31 eleqtrd 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ y e. U. ( S |`t D ) ) -> y e. D )
33 29 32 ffvelrnd 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ y e. U. ( S |`t D ) ) -> ( F ` y ) e. RR )
34 33 rexrd 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ y e. U. ( S |`t D ) ) -> ( F ` y ) e. RR* )
35 34 adantlr 
 |-  ( ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) /\ y e. U. ( S |`t D ) ) -> ( F ` y ) e. RR* )
36 3 2 issmfle 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. c e. RR { y e. D | ( F ` y ) <_ c } e. ( S |`t D ) ) ) )
37 4 36 mpbid 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( D C_ U. S /\ F : D --> RR /\ A. c e. RR { y e. D | ( F ` y ) <_ c } e. ( S |`t D ) ) )
38 37 simp3d 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> A. c e. RR { y e. D | ( F ` y ) <_ c } e. ( S |`t D ) )
39 10 rabeqdv 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> { y e. U. ( S |`t D ) | ( F ` y ) <_ c } = { y e. D | ( F ` y ) <_ c } )
40 39 eleq1d 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( { y e. U. ( S |`t D ) | ( F ` y ) <_ c } e. ( S |`t D ) <-> { y e. D | ( F ` y ) <_ c } e. ( S |`t D ) ) )
41 40 ralbidv 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( A. c e. RR { y e. U. ( S |`t D ) | ( F ` y ) <_ c } e. ( S |`t D ) <-> A. c e. RR { y e. D | ( F ` y ) <_ c } e. ( S |`t D ) ) )
42 38 41 mpbird 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> A. c e. RR { y e. U. ( S |`t D ) | ( F ` y ) <_ c } e. ( S |`t D ) )
43 42 adantr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ c e. RR ) -> A. c e. RR { y e. U. ( S |`t D ) | ( F ` y ) <_ c } e. ( S |`t D ) )
44 simpr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ c e. RR ) -> c e. RR )
45 rspa 
 |-  ( ( A. c e. RR { y e. U. ( S |`t D ) | ( F ` y ) <_ c } e. ( S |`t D ) /\ c e. RR ) -> { y e. U. ( S |`t D ) | ( F ` y ) <_ c } e. ( S |`t D ) )
46 43 44 45 syl2anc 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ c e. RR ) -> { y e. U. ( S |`t D ) | ( F ` y ) <_ c } e. ( S |`t D ) )
47 46 adantlr 
 |-  ( ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) /\ c e. RR ) -> { y e. U. ( S |`t D ) | ( F ` y ) <_ c } e. ( S |`t D ) )
48 simpr 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> b e. RR )
49 18 19 27 28 35 47 48 salpreimalegt 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> { y e. U. ( S |`t D ) | b < ( F ` y ) } e. ( S |`t D ) )
50 13 49 eqeltrd 
 |-  ( ( ( ph /\ F e. ( SMblFn ` S ) ) /\ b e. RR ) -> { y e. D | b < ( F ` y ) } e. ( S |`t D ) )
51 50 ex 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> ( b e. RR -> { y e. D | b < ( F ` y ) } e. ( S |`t D ) ) )
52 9 51 ralrimi 
 |-  ( ( ph /\ F e. ( SMblFn ` S ) ) -> A. b e. RR { y e. D | b < ( F ` y ) } e. ( S |`t D ) )
53 5 6 52 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 ) ) )
54 53 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 ) ) ) )
55 nfv 
 |-  F/ y D C_ U. S
56 nfv 
 |-  F/ y F : D --> RR
57 nfcv 
 |-  F/_ y RR
58 nfrab1 
 |-  F/_ y { y e. D | b < ( F ` y ) }
59 nfcv 
 |-  F/_ y ( S |`t D )
60 58 59 nfel 
 |-  F/ y { y e. D | b < ( F ` y ) } e. ( S |`t D )
61 57 60 nfralw 
 |-  F/ y A. b e. RR { y e. D | b < ( F ` y ) } e. ( S |`t D )
62 55 56 61 nf3an 
 |-  F/ y ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | b < ( F ` y ) } e. ( S |`t D ) )
63 14 62 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 ) ) )
64 nfv 
 |-  F/ b D C_ U. S
65 nfv 
 |-  F/ b F : D --> RR
66 nfra1 
 |-  F/ b A. b e. RR { y e. D | b < ( F ` y ) } e. ( S |`t D )
67 64 65 66 nf3an 
 |-  F/ b ( D C_ U. S /\ F : D --> RR /\ A. b e. RR { y e. D | b < ( F ` y ) } e. ( S |`t D ) )
68 7 67 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 ) ) )
69 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 )
70 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 )
71 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 )
72 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 ) )
73 63 68 69 2 70 71 72 issmfgtlem 
 |-  ( ( 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 ) )
74 73 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 ) ) )
75 54 74 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 ) ) ) )
76 breq1 
 |-  ( b = a -> ( b < ( F ` y ) <-> a < ( F ` y ) ) )
77 76 rabbidv 
 |-  ( b = a -> { y e. D | b < ( F ` y ) } = { y e. D | a < ( F ` y ) } )
78 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
79 78 breq2d 
 |-  ( y = x -> ( a < ( F ` y ) <-> a < ( F ` x ) ) )
80 79 cbvrabv 
 |-  { y e. D | a < ( F ` y ) } = { x e. D | a < ( F ` x ) }
81 80 a1i 
 |-  ( b = a -> { y e. D | a < ( F ` y ) } = { x e. D | a < ( F ` x ) } )
82 77 81 eqtrd 
 |-  ( b = a -> { y e. D | b < ( F ` y ) } = { x e. D | a < ( F ` x ) } )
83 82 eleq1d 
 |-  ( b = a -> ( { y e. D | b < ( F ` y ) } e. ( S |`t D ) <-> { x e. D | a < ( F ` x ) } e. ( S |`t D ) ) )
84 83 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 ) )
85 84 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 ) ) )
86 85 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 ) ) ) )
87 75 86 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 ) ) ) )