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 ) )