Metamath Proof Explorer

Theorem smfpimgtmpt

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 smfpimgtmpt.x 
|- F/ x ph
smfpimgtmpt.s 
|- ( ph -> S e. SAlg )
smfpimgtmpt.b 
|- ( ( ph /\ x e. A ) -> B e. V )
smfpimgtmpt.f 
|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfpimgtmpt.l 
|- ( ph -> L e. RR )
Assertion smfpimgtmpt 
|- ( ph -> { x e. A | L < B } e. ( S |`t A ) )

Proof

Step Hyp Ref Expression
1 smfpimgtmpt.x 
 |-  F/ x ph
2 smfpimgtmpt.s 
 |-  ( ph -> S e. SAlg )
3 smfpimgtmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 smfpimgtmpt.f 
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
5 smfpimgtmpt.l 
 |-  ( ph -> L e. RR )
6 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
7 eqid 
 |-  dom ( x e. A |-> B ) = dom ( x e. A |-> B )
8 6 2 4 7 5 smfpreimagtf 
 |-  ( ph -> { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } e. ( S |`t dom ( x e. A |-> B ) ) )
9 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
10 1 9 3 dmmptdf 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
11 6 nfdm 
 |-  F/_ x dom ( x e. A |-> B )
12 nfcv 
 |-  F/_ x A
13 11 12 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 ) } )
14 10 13 syl 
 |-  ( ph -> { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } = { x e. A | L < ( ( x e. A |-> B ) ` x ) } )
15 9 a1i 
 |-  ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
16 15 3 fvmpt2d 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
17 16 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( L < ( ( x e. A |-> B ) ` x ) <-> L < B ) )
18 1 17 rabbida 
 |-  ( ph -> { x e. A | L < ( ( x e. A |-> B ) ` x ) } = { x e. A | L < B } )
19 eqidd 
 |-  ( ph -> { x e. A | L < B } = { x e. A | L < B } )
20 14 18 19 3eqtrrd 
 |-  ( ph -> { x e. A | L < B } = { x e. dom ( x e. A |-> B ) | L < ( ( x e. A |-> B ) ` x ) } )
21 10 eqcomd 
 |-  ( ph -> A = dom ( x e. A |-> B ) )
22 21 oveq2d 
 |-  ( ph -> ( S |`t A ) = ( S |`t dom ( x e. A |-> B ) ) )
23 20 22 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 ) ) ) )
24 8 23 mpbird 
 |-  ( ph -> { x e. A | L < B } e. ( S |`t A ) )