Metamath Proof Explorer

Theorem smfpimltxrmpt

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

Ref Expression
Hypotheses smfpimltxrmpt.x 
|- F/ x ph
smfpimltxrmpt.s 
|- ( ph -> S e. SAlg )
smfpimltxrmpt.b 
|- ( ( ph /\ x e. A ) -> B e. V )
smfpimltxrmpt.f 
|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfpimltxrmpt.r 
|- ( ph -> R e. RR* )
Assertion smfpimltxrmpt 
|- ( ph -> { x e. A | B < R } e. ( S |`t A ) )

Proof

Step Hyp Ref Expression
1 smfpimltxrmpt.x 
 |-  F/ x ph
2 smfpimltxrmpt.s 
 |-  ( ph -> S e. SAlg )
3 smfpimltxrmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 smfpimltxrmpt.f 
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
5 smfpimltxrmpt.r 
 |-  ( ph -> R 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 ( ( x e. A |-> B ) ` x ) < R
10 nfcv 
 |-  F/_ x y
11 6 10 nffv 
 |-  F/_ x ( ( x e. A |-> B ) ` y )
12 nfcv 
 |-  F/_ x <
13 nfcv 
 |-  F/_ x R
14 11 12 13 nfbr 
 |-  F/ x ( ( x e. A |-> B ) ` y ) < R
15 fveq2 
 |-  ( x = y -> ( ( x e. A |-> B ) ` x ) = ( ( x e. A |-> B ) ` y ) )
16 15 breq1d 
 |-  ( x = y -> ( ( ( x e. A |-> B ) ` x ) < R <-> ( ( x e. A |-> B ) ` y ) < R ) )
17 7 8 9 14 16 cbvrabw 
 |-  { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } = { y e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` y ) < R }
18 17 a1i 
 |-  ( ph -> { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } = { y e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` y ) < R } )
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 smfpimltxr 
 |-  ( ph -> { y e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` y ) < R } e. ( S |`t dom ( x e. A |-> B ) ) )
22 18 21 eqeltrd 
 |-  ( ph -> { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } 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 ) | ( ( x e. A |-> B ) ` x ) < R } = { x e. A | ( ( x e. A |-> B ) ` x ) < R } )
27 24 26 syl 
 |-  ( ph -> { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } = { x e. A | ( ( x e. A |-> B ) ` x ) < R } )
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 breq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) < R <-> B < R ) )
31 1 30 rabbida 
 |-  ( ph -> { x e. A | ( ( x e. A |-> B ) ` x ) < R } = { x e. A | B < R } )
32 eqidd 
 |-  ( ph -> { x e. A | B < R } = { x e. A | B < R } )
33 27 31 32 3eqtrrd 
 |-  ( ph -> { x e. A | B < R } = { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } )
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 | B < R } e. ( S |`t A ) <-> { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } e. ( S |`t dom ( x e. A |-> B ) ) ) )
37 22 36 mpbird 
 |-  ( ph -> { x e. A | B < R } e. ( S |`t A ) )