# Metamath Proof Explorer

## Theorem smfpimioompt

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpimioompt.x
`|- F/ x ph`
smfpimioompt.s
`|- ( ph -> S e. SAlg )`
smfpimioompt.a
`|- ( ph -> A e. V )`
smfpimioompt.b
`|- ( ( ph /\ x e. A ) -> B e. W )`
smfpimioompt.m
`|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )`
smfpimioompt.l
`|- ( ph -> L e. RR* )`
smfpimioompt.r
`|- ( ph -> R e. RR* )`
Assertion smfpimioompt
`|- ( ph -> { x e. A | B e. ( L (,) R ) } e. ( S |`t A ) )`

### Proof

Step Hyp Ref Expression
1 smfpimioompt.x
` |-  F/ x ph`
2 smfpimioompt.s
` |-  ( ph -> S e. SAlg )`
3 smfpimioompt.a
` |-  ( ph -> A e. V )`
4 smfpimioompt.b
` |-  ( ( ph /\ x e. A ) -> B e. W )`
5 smfpimioompt.m
` |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )`
6 smfpimioompt.l
` |-  ( ph -> L e. RR* )`
7 smfpimioompt.r
` |-  ( ph -> R e. RR* )`
8 eqid
` |-  dom ( x e. A |-> B ) = dom ( x e. A |-> B )`
9 2 5 8 smff
` |-  ( ph -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> RR )`
10 eqid
` |-  ( x e. A |-> B ) = ( x e. A |-> B )`
11 1 10 4 dmmptdf
` |-  ( ph -> dom ( x e. A |-> B ) = A )`
12 11 feq2d
` |-  ( ph -> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> RR <-> ( x e. A |-> B ) : A --> RR ) )`
13 9 12 mpbid
` |-  ( ph -> ( x e. A |-> B ) : A --> RR )`
14 13 fvmptelrn
` |-  ( ( ph /\ x e. A ) -> B e. RR )`
15 14 rexrd
` |-  ( ( ph /\ x e. A ) -> B e. RR* )`
16 1 6 7 15 pimiooltgt
` |-  ( ph -> { x e. A | B e. ( L (,) R ) } = ( { x e. A | B < R } i^i { x e. A | L < B } ) )`
17 eqid
` |-  ( S |`t A ) = ( S |`t A )`
18 2 3 17 subsalsal
` |-  ( ph -> ( S |`t A ) e. SAlg )`
19 1 2 4 5 7 smfpimltxrmpt
` |-  ( ph -> { x e. A | B < R } e. ( S |`t A ) )`
20 1 2 4 5 6 smfpimgtxrmpt
` |-  ( ph -> { x e. A | L < B } e. ( S |`t A ) )`
21 18 19 20 salincld
` |-  ( ph -> ( { x e. A | B < R } i^i { x e. A | L < B } ) e. ( S |`t A ) )`
22 16 21 eqeltrd
` |-  ( ph -> { x e. A | B e. ( L (,) R ) } e. ( S |`t A ) )`