Metamath Proof Explorer

Theorem smfpimltmpt

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

Proof

Step Hyp Ref Expression
1 smfpimltmpt.x 
 |-  F/ x ph
2 smfpimltmpt.s 
 |-  ( ph -> S e. SAlg )
3 smfpimltmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 smfpimltmpt.f 
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
5 smfpimltmpt.r 
 |-  ( ph -> R 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 smfpreimaltf 
 |-  ( ph -> { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } 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 ) | ( ( x e. A |-> B ) ` x ) < R } = { x e. A | ( ( x e. A |-> B ) ` x ) < R } )
14 10 13 syl 
 |-  ( ph -> { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } = { x e. A | ( ( x e. A |-> B ) ` x ) < R } )
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 breq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) < R <-> B < R ) )
18 1 17 rabbida 
 |-  ( ph -> { x e. A | ( ( x e. A |-> B ) ` x ) < R } = { x e. A | B < R } )
19 eqidd 
 |-  ( ph -> { x e. A | B < R } = { x e. A | B < R } )
20 14 18 19 3eqtrrd 
 |-  ( ph -> { x e. A | B < R } = { x e. dom ( x e. A |-> B ) | ( ( x e. A |-> B ) ` x ) < R } )
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 | 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 ) ) ) )
24 8 23 mpbird 
 |-  ( ph -> { x e. A | B < R } e. ( S |`t A ) )