Metamath Proof Explorer

Theorem smfpimltxrmptf

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

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

Proof

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