Metamath Proof Explorer

Theorem smfpimne2

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value is in the subspace sigma-algebra induced by its domain. Notice that A is not assumed to be an extended real. (Contributed by Glauco Siliprandi, 5-Jan-2025)

Ref Expression
Hypotheses smfpimne2.p 
|- F/ x ph
smfpimne2.x 
|- F/_ x F
smfpimne2.s 
|- ( ph -> S e. SAlg )
smfpimne2.f 
|- ( ph -> F e. ( SMblFn ` S ) )
smfpimne2.d 
|- D = dom F
Assertion smfpimne2 
|- ( ph -> { x e. D | ( F ` x ) =/= A } e. ( S |`t D ) )

Proof

Step Hyp Ref Expression
1 smfpimne2.p 
 |-  F/ x ph
2 smfpimne2.x 
 |-  F/_ x F
3 smfpimne2.s 
 |-  ( ph -> S e. SAlg )
4 smfpimne2.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
5 smfpimne2.d 
 |-  D = dom F
6 nfv 
 |-  F/ x A e. RR*
7 1 6 nfan 
 |-  F/ x ( ph /\ A e. RR* )
8 3 adantr 
 |-  ( ( ph /\ A e. RR* ) -> S e. SAlg )
9 4 adantr 
 |-  ( ( ph /\ A e. RR* ) -> F e. ( SMblFn ` S ) )
10 simpr 
 |-  ( ( ph /\ A e. RR* ) -> A e. RR* )
11 7 2 8 9 5 10 smfpimne 
 |-  ( ( ph /\ A e. RR* ) -> { x e. D | ( F ` x ) =/= A } e. ( S |`t D ) )
12 2 nfdm 
 |-  F/_ x dom F
13 5 12 nfcxfr 
 |-  F/_ x D
14 13 ssrab2f 
 |-  { x e. D | ( F ` x ) =/= A } C_ D
15 14 a1i 
 |-  ( ( ph /\ -. A e. RR* ) -> { x e. D | ( F ` x ) =/= A } C_ D )
16 nfv 
 |-  F/ x -. A e. RR*
17 1 16 nfan 
 |-  F/ x ( ph /\ -. A e. RR* )
18 ssidd 
 |-  ( ( ph /\ -. A e. RR* ) -> D C_ D )
19 nne 
 |-  ( -. ( F ` x ) =/= A <-> ( F ` x ) = A )
20 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ ( F ` x ) = A ) -> ( F ` x ) = A )
21 3 4 5 smff 
 |-  ( ph -> F : D --> RR )
22 21 ffvelcdmda 
 |-  ( ( ph /\ x e. D ) -> ( F ` x ) e. RR )
23 22 rexrd 
 |-  ( ( ph /\ x e. D ) -> ( F ` x ) e. RR* )
24 23 adantr 
 |-  ( ( ( ph /\ x e. D ) /\ ( F ` x ) = A ) -> ( F ` x ) e. RR* )
25 20 24 eqeltrrd 
 |-  ( ( ( ph /\ x e. D ) /\ ( F ` x ) = A ) -> A e. RR* )
26 19 25 sylan2b 
 |-  ( ( ( ph /\ x e. D ) /\ -. ( F ` x ) =/= A ) -> A e. RR* )
27 26 adantllr 
 |-  ( ( ( ( ph /\ -. A e. RR* ) /\ x e. D ) /\ -. ( F ` x ) =/= A ) -> A e. RR* )
28 simpllr 
 |-  ( ( ( ( ph /\ -. A e. RR* ) /\ x e. D ) /\ -. ( F ` x ) =/= A ) -> -. A e. RR* )
29 27 28 condan 
 |-  ( ( ( ph /\ -. A e. RR* ) /\ x e. D ) -> ( F ` x ) =/= A )
30 13 13 17 18 29 ssrabdf 
 |-  ( ( ph /\ -. A e. RR* ) -> D C_ { x e. D | ( F ` x ) =/= A } )
31 15 30 eqssd 
 |-  ( ( ph /\ -. A e. RR* ) -> { x e. D | ( F ` x ) =/= A } = D )
32 3 4 5 smfdmss 
 |-  ( ph -> D C_ U. S )
33 3 32 subsaluni 
 |-  ( ph -> D e. ( S |`t D ) )
34 33 adantr 
 |-  ( ( ph /\ -. A e. RR* ) -> D e. ( S |`t D ) )
35 31 34 eqeltrd 
 |-  ( ( ph /\ -. A e. RR* ) -> { x e. D | ( F ` x ) =/= A } e. ( S |`t D ) )
36 11 35 pm2.61dan 
 |-  ( ph -> { x e. D | ( F ` x ) =/= A } e. ( S |`t D ) )