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)

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 7 adantl 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | A < ( F ` x ) } = { x e. D | -oo < ( F ` x ) } )
9 1 nfdm 
 |-  F/_ x dom F
10 4 9 nfcxfr 
 |-  F/_ x D
11 nfcv 
 |-  F/_ y D
12 nfv 
 |-  F/ y -oo < ( F ` x )
13 nfcv 
 |-  F/_ x -oo
14 nfcv 
 |-  F/_ x <
15 nfcv 
 |-  F/_ x y
16 1 15 nffv 
 |-  F/_ x ( F ` y )
17 13 14 16 nfbr 
 |-  F/ x -oo < ( F ` y )
18 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
19 18 breq2d 
 |-  ( x = y -> ( -oo < ( F ` x ) <-> -oo < ( F ` y ) ) )
20 10 11 12 17 19 cbvrabw 
 |-  { x e. D | -oo < ( F ` x ) } = { y e. D | -oo < ( F ` y ) }
21 20 a1i 
 |-  ( ph -> { x e. D | -oo < ( F ` x ) } = { y e. D | -oo < ( F ` y ) } )
22 nfv 
 |-  F/ y ph
23 2 3 4 smff 
 |-  ( ph -> F : D --> RR )
24 23 adantr 
 |-  ( ( ph /\ y e. D ) -> F : D --> RR )
25 simpr 
 |-  ( ( ph /\ y e. D ) -> y e. D )
26 24 25 ffvelrnd 
 |-  ( ( ph /\ y e. D ) -> ( F ` y ) e. RR )
27 22 26 pimgtmnf 
 |-  ( ph -> { y e. D | -oo < ( F ` y ) } = D )
28 eqidd 
 |-  ( ph -> D = D )
29 21 27 28 3eqtrd 
 |-  ( ph -> { x e. D | -oo < ( F ` x ) } = D )
30 29 adantr 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | -oo < ( F ` x ) } = D )
31 8 30 eqtrd 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | A < ( F ` x ) } = D )
32 2 3 4 smfdmss 
 |-  ( ph -> D C_ U. S )
33 2 32 restuni4 
 |-  ( ph -> U. ( S |`t D ) = D )
34 33 eqcomd 
 |-  ( ph -> D = U. ( S |`t D ) )
35 3 dmexd 
 |-  ( ph -> dom F e. _V )
36 4 35 eqeltrid 
 |-  ( ph -> D e. _V )
37 eqid 
 |-  ( S |`t D ) = ( S |`t D )
38 2 36 37 subsalsal 
 |-  ( ph -> ( S |`t D ) e. SAlg )
39 38 salunid 
 |-  ( ph -> U. ( S |`t D ) e. ( S |`t D ) )
40 34 39 eqeltrd 
 |-  ( ph -> D e. ( S |`t D ) )
41 40 adantr 
 |-  ( ( ph /\ A = -oo ) -> D e. ( S |`t D ) )
42 31 41 eqeltrd 
 |-  ( ( ph /\ A = -oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
43 neqne 
 |-  ( -. A = -oo -> A =/= -oo )
44 43 adantl 
 |-  ( ( ph /\ -. A = -oo ) -> A =/= -oo )
45 breq1 
 |-  ( A = +oo -> ( A < ( F ` x ) <-> +oo < ( F ` x ) ) )
46 45 rabbidv 
 |-  ( A = +oo -> { x e. D | A < ( F ` x ) } = { x e. D | +oo < ( F ` x ) } )
47 46 adantl 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | A < ( F ` x ) } = { x e. D | +oo < ( F ` x ) } )
48 1 23 pimgtpnf2 
 |-  ( ph -> { x e. D | +oo < ( F ` x ) } = (/) )
49 48 adantr 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | +oo < ( F ` x ) } = (/) )
50 47 49 eqtrd 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | A < ( F ` x ) } = (/) )
51 38 0sald 
 |-  ( ph -> (/) e. ( S |`t D ) )
52 51 adantr 
 |-  ( ( ph /\ A = +oo ) -> (/) e. ( S |`t D ) )
53 50 52 eqeltrd 
 |-  ( ( ph /\ A = +oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
54 53 adantlr 
 |-  ( ( ( ph /\ A =/= -oo ) /\ A = +oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
55 simpll 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> ph )
56 55 5 syl 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A e. RR* )
57 simplr 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A =/= -oo )
58 neqne 
 |-  ( -. A = +oo -> A =/= +oo )
59 58 adantl 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A =/= +oo )
60 56 57 59 xrred 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A e. RR )
61 2 adantr 
 |-  ( ( ph /\ A e. RR ) -> S e. SAlg )
62 3 adantr 
 |-  ( ( ph /\ A e. RR ) -> F e. ( SMblFn ` S ) )
63 simpr 
 |-  ( ( ph /\ A e. RR ) -> A e. RR )
64 1 61 62 4 63 smfpreimagtf 
 |-  ( ( ph /\ A e. RR ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
65 55 60 64 syl2anc 
 |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
66 54 65 pm2.61dan 
 |-  ( ( ph /\ A =/= -oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
67 44 66 syldan 
 |-  ( ( ph /\ -. A = -oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
68 42 67 pm2.61dan 
 |-  ( ph -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )