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 ) } )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) } )`
` |-  ( ( 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 ) } = (/) )`
` |-  ( ( 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 ) )`
` |-  ( ( ph /\ A = +oo ) -> (/) e. ( S |`t D ) )`
53 50 52 eqeltrd
` |-  ( ( ph /\ A = +oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A =/= +oo )`
60 56 57 59 xrred
` |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> A e. RR )`
` |-  ( ( ph /\ A e. RR ) -> S e. SAlg )`
` |-  ( ( ph /\ A e. RR ) -> F e. ( SMblFn ` S ) )`
` |-  ( ( ph /\ A e. RR ) -> A e. RR )`
` |-  ( ( ph /\ A e. RR ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )`
` |-  ( ( ( ph /\ A =/= -oo ) /\ -. A = +oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )`
` |-  ( ( ph /\ A =/= -oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )`
` |-  ( ( ph /\ -. A = -oo ) -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )`
` |-  ( ph -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )`