Metamath Proof Explorer

Theorem smfpimgtxrmptf

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, 20-Dec-2024)

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

Proof

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