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) (Revised by Glauco Siliprandi, 15-Dec-2024)

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 1 nfdm 
 |-  F/_ x dom F
9 4 8 nfcxfr 
 |-  F/_ x D
10 2 3 4 smff 
 |-  ( ph -> F : D --> RR )
11 1 9 10 pimltpnf2f 
 |-  ( ph -> { x e. D | ( F ` x ) < +oo } = D )
12 7 11 sylan9eqr 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | ( F ` x ) < A } = D )
13 2 3 4 smfdmss 
 |-  ( ph -> D C_ U. S )
14 2 13 subsaluni 
 |-  ( ph -> D e. ( S |`t D ) )
15 14 adantr 
 |-  ( ( ph /\ A = +oo ) -> D e. ( S |`t D ) )
16 12 15 eqeltrd 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
17 breq2 
 |-  ( A = -oo -> ( ( F ` x ) < A <-> ( F ` x ) < -oo ) )
18 17 rabbidv 
 |-  ( A = -oo -> { x e. D | ( F ` x ) < A } = { x e. D | ( F ` x ) < -oo } )
19 18 adantl 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | ( F ` x ) < A } = { x e. D | ( F ` x ) < -oo } )
20 10 adantr 
 |-  ( ( ph /\ A = -oo ) -> F : D --> RR )
21 1 9 20 pimltmnf2f 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | ( F ` x ) < -oo } = (/) )
22 19 21 eqtrd 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | ( F ` x ) < A } = (/) )
23 3 dmexd 
 |-  ( ph -> dom F e. _V )
24 4 23 eqeltrid 
 |-  ( ph -> D e. _V )
25 eqid 
 |-  ( S |`t D ) = ( S |`t D )
26 2 24 25 subsalsal 
 |-  ( ph -> ( S |`t D ) e. SAlg )
27 26 0sald 
 |-  ( ph -> (/) e. ( S |`t D ) )
28 27 adantr 
 |-  ( ( ph /\ A = -oo ) -> (/) e. ( S |`t D ) )
29 22 28 eqeltrd 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
30 29 adantlr 
 |-  ( ( ( ph /\ A =/= +oo ) /\ A = -oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
31 simpll 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> ph )
32 31 5 syl 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> A e. RR* )
33 neqne 
 |-  ( -. A = -oo -> A =/= -oo )
34 33 adantl 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> A =/= -oo )
35 simplr 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> A =/= +oo )
36 32 34 35 xrred 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> A e. RR )
37 2 adantr 
 |-  ( ( ph /\ A e. RR ) -> S e. SAlg )
38 3 adantr 
 |-  ( ( ph /\ A e. RR ) -> F e. ( SMblFn ` S ) )
39 simpr 
 |-  ( ( ph /\ A e. RR ) -> A e. RR )
40 1 37 38 4 39 smfpreimaltf 
 |-  ( ( ph /\ A e. RR ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
41 31 36 40 syl2anc 
 |-  ( ( ( ph /\ A =/= +oo ) /\ -. A = -oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
42 30 41 pm2.61dan 
 |-  ( ( ph /\ A =/= +oo ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
43 16 42 pm2.61dane 
 |-  ( ph -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )