Metamath Proof Explorer

Theorem smfpimgtxr

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above 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 smfpimgtxr.x 
|- F/_ x F
smfpimgtxr.s 
|- ( ph -> S e. SAlg )
smfpimgtxr.f 
|- ( ph -> F e. ( SMblFn ` S ) )
smfpimgtxr.d 
|- D = dom F
smfpimgtxr.a 
|- ( ph -> A e. RR* )
Assertion smfpimgtxr 
|- ( ph -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )

Proof

Step Hyp Ref Expression
1 smfpimgtxr.x 
 |-  F/_ x F
2 smfpimgtxr.s 
 |-  ( ph -> S e. SAlg )
3 smfpimgtxr.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
4 smfpimgtxr.d 
 |-  D = dom F
5 smfpimgtxr.a 
 |-  ( ph -> A e. RR* )
6 breq1 
 |-  ( A = -oo -> ( A < ( F ` x ) <-> -oo < ( F ` x ) ) )
7 6 rabbidv 
 |-  ( A = -oo -> { x e. D | A < ( F ` x ) } = { x e. D | -oo < ( F ` x ) } )
8 1 nfdm 
 |-  F/_ x dom F
9 4 8 nfcxfr 
 |-  F/_ x D
10 nfcv 
 |-  F/_ y D
11 nfv 
 |-  F/ y -oo < ( F ` x )
12 nfcv 
 |-  F/_ x -oo
13 nfcv 
 |-  F/_ x <
14 nfcv 
 |-  F/_ x y
15 1 14 nffv 
 |-  F/_ x ( F ` y )
16 12 13 15 nfbr 
 |-  F/ x -oo < ( F ` y )
17 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
18 17 breq2d 
 |-  ( x = y -> ( -oo < ( F ` x ) <-> -oo < ( F ` y ) ) )
19 9 10 11 16 18 cbvrabw 
 |-  { x e. D | -oo < ( F ` x ) } = { y e. D | -oo < ( F ` y ) }
20 nfv 
 |-  F/ y ph
21 2 3 4 smff 
 |-  ( ph -> F : D --> RR )
22 21 ffvelcdmda 
 |-  ( ( ph /\ y e. D ) -> ( F ` y ) e. RR )
23 20 22 pimgtmnf 
 |-  ( ph -> { y e. D | -oo < ( F ` y ) } = D )
24 19 23 eqtrid 
 |-  ( ph -> { x e. D | -oo < ( F ` x ) } = D )
25 7 24 sylan9eqr 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | A < ( F ` x ) } = D )
26 2 3 4 smfdmss 
 |-  ( ph -> D C_ U. S )
27 2 26 subsaluni 
 |-  ( ph -> D e. ( S |`t D ) )
28 27 adantr 
 |-  ( ( ph /\ A = -oo ) -> D e. ( S |`t D ) )
29 25 28 eqeltrd 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
30 breq1 
 |-  ( A = +oo -> ( A < ( F ` x ) <-> +oo < ( F ` x ) ) )
31 30 rabbidv 
 |-  ( A = +oo -> { x e. D | A < ( F ` x ) } = { x e. D | +oo < ( F ` x ) } )
32 1 9 21 pimgtpnf2f 
 |-  ( ph -> { x e. D | +oo < ( F ` x ) } = (/) )
33 31 32 sylan9eqr 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | A < ( F ` x ) } = (/) )
34 3 dmexd 
 |-  ( ph -> dom F e. _V )
35 4 34 eqeltrid 
 |-  ( ph -> D e. _V )
36 eqid 
 |-  ( S |`t D ) = ( S |`t D )
37 2 35 36 subsalsal 
 |-  ( ph -> ( S |`t D ) e. SAlg )
38 37 0sald 
 |-  ( ph -> (/) e. ( S |`t D ) )
39 38 adantr 
 |-  ( ( ph /\ A = +oo ) -> (/) e. ( S |`t D ) )
40 33 39 eqeltrd 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
41 40 adantlr 
 |-  ( ( ( ph /\ A =/= -oo ) /\ A = +oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
42 simpll 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> ph )
43 42 5 syl 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A e. RR* )
44 simplr 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A =/= -oo )
45 neqne 
 |-  ( -. A = +oo -> A =/= +oo )
46 45 adantl 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A =/= +oo )
47 43 44 46 xrred 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A e. RR )
48 2 adantr 
 |-  ( ( ph /\ A e. RR ) -> S e. SAlg )
49 3 adantr 
 |-  ( ( ph /\ A e. RR ) -> F e. ( SMblFn ` S ) )
50 simpr 
 |-  ( ( ph /\ A e. RR ) -> A e. RR )
51 1 48 49 4 50 smfpreimagtf 
 |-  ( ( ph /\ A e. RR ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
52 42 47 51 syl2anc 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
53 41 52 pm2.61dan 
 |-  ( ( ph /\ A =/= -oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
54 29 53 pm2.61dane 
 |-  ( ph -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )