# Metamath Proof Explorer

## Theorem smfpimgtxrmpt

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 smfpimgtxrmpt.x
`|- F/ x ph`
smfpimgtxrmpt.s
`|- ( ph -> S e. SAlg )`
smfpimgtxrmpt.b
`|- ( ( ph /\ x e. A ) -> B e. V )`
smfpimgtxrmpt.f
`|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )`
smfpimgtxrmpt.l
`|- ( ph -> L e. RR* )`
Assertion smfpimgtxrmpt
`|- ( ph -> { x e. A | L < B } e. ( S |`t A ) )`

### Proof

Step Hyp Ref Expression
1 smfpimgtxrmpt.x
` |-  F/ x ph`
2 smfpimgtxrmpt.s
` |-  ( ph -> S e. SAlg )`
3 smfpimgtxrmpt.b
` |-  ( ( ph /\ x e. A ) -> B e. V )`
4 smfpimgtxrmpt.f
` |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )`
5 smfpimgtxrmpt.l
` |-  ( ph -> L e. RR* )`
6 nfmpt1
` |-  F/_ x ( x e. A |-> B )`
7 6 nfdm
` |-  F/_ x dom ( x e. A |-> B )`
8 nfcv
` |-  F/_ y dom ( x e. A |-> B )`
9 nfv
` |-  F/ y L < ( ( x e. A |-> B ) ` x )`
10 nfcv
` |-  F/_ x L`
11 nfcv
` |-  F/_ x <`
12 nfcv
` |-  F/_ x y`
13 6 12 nffv
` |-  F/_ x ( ( x e. A |-> B ) ` y )`
14 10 11 13 nfbr
` |-  F/ x L < ( ( x e. A |-> B ) ` y )`
15 fveq2
` |-  ( x = y -> ( ( x e. A |-> B ) ` x ) = ( ( x e. A |-> B ) ` y ) )`
16 15 breq2d
` |-  ( x = y -> ( L < ( ( x e. A |-> B ) ` x ) <-> L < ( ( x e. A |-> B ) ` y ) ) )`
17 7 8 9 14 16 cbvrabw
` |-  { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } = { y e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` y ) }`
18 17 a1i
` |-  ( ph -> { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } = { y e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` y ) } )`
19 nfcv
` |-  F/_ y ( x e. A |-> B )`
20 eqid
` |-  dom ( x e. A |-> B ) = dom ( x e. A |-> B )`
21 19 2 4 20 5 smfpimgtxr
` |-  ( ph -> { y e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` y ) } e. ( S |`t dom ( x e. A |-> B ) ) )`
22 18 21 eqeltrd
` |-  ( ph -> { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } e. ( S |`t dom ( x e. A |-> B ) ) )`
23 eqid
` |-  ( x e. A |-> B ) = ( x e. A |-> B )`
24 1 23 3 dmmptdf
` |-  ( ph -> dom ( x e. A |-> B ) = A )`
25 nfcv
` |-  F/_ x A`
26 7 25 rabeqf
` |-  ( dom ( x e. A |-> B ) = A -> { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } = { x e. A | L < ( ( x e. A |-> B ) ` x ) } )`
27 24 26 syl
` |-  ( ph -> { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } = { x e. A | L < ( ( x e. A |-> B ) ` x ) } )`
28 23 a1i
` |-  ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )`
29 28 3 fvmpt2d
` |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )`
30 29 breq2d
` |-  ( ( ph /\ x e. A ) -> ( L < ( ( x e. A |-> B ) ` x ) <-> L < B ) )`
31 1 30 rabbida
` |-  ( ph -> { x e. A | L < ( ( x e. A |-> B ) ` x ) } = { x e. A | L < B } )`
32 eqidd
` |-  ( ph -> { x e. A | L < B } = { x e. A | L < B } )`
33 27 31 32 3eqtrrd
` |-  ( ph -> { x e. A | L < B } = { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } )`
34 24 eqcomd
` |-  ( ph -> A = dom ( x e. A |-> B ) )`
35 34 oveq2d
` |-  ( ph -> ( S |`t A ) = ( S |`t dom ( x e. A |-> B ) ) )`
36 33 35 eleq12d
` |-  ( ph -> ( { x e. A | L < B } e. ( S |`t A ) <-> { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } e. ( S |`t dom ( x e. A |-> B ) ) ) )`
37 22 36 mpbird
` |-  ( ph -> { x e. A | L < B } e. ( S |`t A ) )`