Metamath Proof Explorer

Theorem smfpimltxr

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 smfpimltxr.x 
 |-  F/_ x F
2 smfpimltxr.s 
 |-  ( ph -> S e. SAlg )
3 smfpimltxr.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
4 smfpimltxr.d 
 |-  D = dom F
5 smfpimltxr.a 
 |-  ( ph -> A e. RR* )
6 breq2 
 |-  ( A = +oo -> ( ( F ` x ) < A <-> ( F ` x ) < +oo ) )
7 6 rabbidv 
 |-  ( A = +oo -> { x e. D | ( F ` x ) < A } = { x e. D | ( F ` x ) < +oo } )
8 7 adantl 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | ( F ` x ) < A } = { x e. D | ( F ` x ) < +oo } )
9 1 2 4 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 ) ) ) )
10 3 9 mpbid 
 |-  ( ph -> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
11 10 simp2d 
 |-  ( ph -> F : D --> RR )
12 1 11 pimltpnf2 
 |-  ( ph -> { x e. D | ( F ` x ) < +oo } = D )
13 12 adantr 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | ( F ` x ) < +oo } = D )
14 eqidd 
 |-  ( ( ph /\ A = +oo ) -> D = D )
15 8 13 14 3eqtrd 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | ( F ` x ) < A } = D )
16 10 simp1d 
 |-  ( ph -> D C_ U. S )
17 2 16 restuni4 
 |-  ( ph -> U. ( S |`t D ) = D )
18 17 eqcomd 
 |-  ( ph -> D = U. ( S |`t D ) )
19 3 dmexd 
 |-  ( ph -> dom F e. _V )
20 4 19 eqeltrid 
 |-  ( ph -> D e. _V )
21 eqid 
 |-  ( S |`t D ) = ( S |`t D )
22 2 20 21 subsalsal 
 |-  ( ph -> ( S |`t D ) e. SAlg )
23 22 salunid 
 |-  ( ph -> U. ( S |`t D ) e. ( S |`t D ) )
24 18 23 eqeltrd 
 |-  ( ph -> D e. ( S |`t D ) )
25 24 adantr 
 |-  ( ( ph /\ A = +oo ) -> D e. ( S |`t D ) )
26 15 25 eqeltrd 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
27 neqne 
 |-  ( -. A = +oo -> A =/= +oo )
28 27 adantl 
 |-  ( ( ph /\ -. A = +oo ) -> A =/= +oo )
29 breq2 
 |-  ( A = -oo -> ( ( F ` x ) < A <-> ( F ` x ) < -oo ) )
30 29 rabbidv 
 |-  ( A = -oo -> { x e. D | ( F ` x ) < A } = { x e. D | ( F ` x ) < -oo } )
31 30 adantl 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | ( F ` x ) < A } = { x e. D | ( F ` x ) < -oo } )
32 11 adantr 
 |-  ( ( ph /\ A = -oo ) -> F : D --> RR )
33 1 32 pimltmnf2 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | ( F ` x ) < -oo } = (/) )
34 31 33 eqtrd 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | ( F ` x ) < A } = (/) )
35 22 0sald 
 |-  ( ph -> (/) e. ( S |`t D ) )
36 35 adantr 
 |-  ( ( ph /\ A = -oo ) -> (/) e. ( S |`t D ) )
37 34 36 eqeltrd 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
38 37 adantlr 
 |-  ( ( ( ph /\ A =/= +oo ) /\ A = -oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
39 simpll 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> ph )
40 39 5 syl 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> A e. RR* )
41 neqne 
 |-  ( -. A = -oo -> A =/= -oo )
42 41 adantl 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> A =/= -oo )
43 simplr 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> A =/= +oo )
44 40 42 43 xrred 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> A e. RR )
45 2 adantr 
 |-  ( ( ph /\ A e. RR ) -> S e. SAlg )
46 3 adantr 
 |-  ( ( ph /\ A e. RR ) -> F e. ( SMblFn ` S ) )
47 simpr 
 |-  ( ( ph /\ A e. RR ) -> A e. RR )
48 1 45 46 4 47 smfpreimaltf 
 |-  ( ( ph /\ A e. RR ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
49 39 44 48 syl2anc 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
50 38 49 pm2.61dan 
 |-  ( ( ph /\ A =/= +oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
51 28 50 syldan 
 |-  ( ( ph /\ -. A = +oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
52 26 51 pm2.61dan 
 |-  ( ph -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )