Metamath Proof Explorer

Theorem issmff

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

Ref Expression
Hypotheses issmff.x 
|- F/_ x F
issmff.s 
|- ( ph -> S e. SAlg )
issmff.d 
|- D = dom F
Assertion issmff 
|- ( 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 issmff.x 
 |-  F/_ x F
2 issmff.s 
 |-  ( ph -> S e. SAlg )
3 issmff.d 
 |-  D = dom F
4 2 3 issmf 
 |-  ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { y e. D | ( F ` y ) < a } e. ( S |`t D ) ) ) )
5 nfcv 
 |-  F/_ y D
6 1 nfdm 
 |-  F/_ x dom F
7 3 6 nfcxfr 
 |-  F/_ x D
8 nfcv 
 |-  F/_ x y
9 1 8 nffv 
 |-  F/_ x ( F ` y )
10 nfcv 
 |-  F/_ x <
11 nfcv 
 |-  F/_ x a
12 9 10 11 nfbr 
 |-  F/ x ( F ` y ) < a
13 nfv 
 |-  F/ y ( F ` x ) < a
14 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
15 14 breq1d 
 |-  ( y = x -> ( ( F ` y ) < a <-> ( F ` x ) < a ) )
16 5 7 12 13 15 cbvrabw 
 |-  { y e. D | ( F ` y ) < a } = { x e. D | ( F ` x ) < a }
17 16 eleq1i 
 |-  ( { y e. D | ( F ` y ) < a } e. ( S |`t D ) <-> { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
18 17 ralbii 
 |-  ( A. a e. RR { y e. D | ( F ` y ) < a } e. ( S |`t D ) <-> A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
19 18 3anbi3i 
 |-  ( ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { y e. D | ( F ` y ) < a } 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 ) ) )
20 19 a1i 
 |-  ( ph -> ( ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { y e. D | ( F ` y ) < a } 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 ) ) ) )
21 4 20 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 ) ) ) )