Metamath Proof Explorer

Theorem sssmf

Description: The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses sssmf.s 
|- ( ph -> S e. SAlg )
sssmf.f 
|- ( ph -> F e. ( SMblFn ` S ) )
Assertion sssmf 
|- ( ph -> ( F |` B ) e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 sssmf.s 
 |-  ( ph -> S e. SAlg )
2 sssmf.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 nfv 
 |-  F/ a ph
4 inss2 
 |-  ( B i^i dom F ) C_ dom F
5 eqid 
 |-  dom F = dom F
6 1 2 5 smfdmss 
 |-  ( ph -> dom F C_ U. S )
7 4 6 sstrid 
 |-  ( ph -> ( B i^i dom F ) C_ U. S )
8 resindm 
 |-  ( F |` ( B i^i dom F ) ) = ( F |` B )
9 8 a1i 
 |-  ( ph -> ( F |` ( B i^i dom F ) ) = ( F |` B ) )
10 1 2 5 smff 
 |-  ( ph -> F : dom F --> RR )
11 4 a1i 
 |-  ( ph -> ( B i^i dom F ) C_ dom F )
12 10 11 fssresd 
 |-  ( ph -> ( F |` ( B i^i dom F ) ) : ( B i^i dom F ) --> RR )
13 9 12 feq1dd 
 |-  ( ph -> ( F |` B ) : ( B i^i dom F ) --> RR )
14 1 adantr 
 |-  ( ( ph /\ a e. RR ) -> S e. SAlg )
15 2 adantr 
 |-  ( ( ph /\ a e. RR ) -> F e. ( SMblFn ` S ) )
16 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
17 14 15 5 16 smfpreimalt 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) )
18 2 dmexd 
 |-  ( ph -> dom F e. _V )
19 elrest 
 |-  ( ( S e. SAlg /\ dom F e. _V ) -> ( { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) <-> E. w e. S { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) )
20 1 18 19 syl2anc 
 |-  ( ph -> ( { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) <-> E. w e. S { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) )
21 20 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) <-> E. w e. S { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) )
22 17 21 mpbid 
 |-  ( ( ph /\ a e. RR ) -> E. w e. S { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) )
23 elinel1 
 |-  ( x e. ( B i^i dom F ) -> x e. B )
24 23 fvresd 
 |-  ( x e. ( B i^i dom F ) -> ( ( F |` B ) ` x ) = ( F ` x ) )
25 24 breq1d 
 |-  ( x e. ( B i^i dom F ) -> ( ( ( F |` B ) ` x ) < a <-> ( F ` x ) < a ) )
26 25 rabbiia 
 |-  { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } = { x e. ( B i^i dom F ) | ( F ` x ) < a }
27 rabss2 
 |-  ( ( B i^i dom F ) C_ dom F -> { x e. ( B i^i dom F ) | ( F ` x ) < a } C_ { x e. dom F | ( F ` x ) < a } )
28 4 27 ax-mp 
 |-  { x e. ( B i^i dom F ) | ( F ` x ) < a } C_ { x e. dom F | ( F ` x ) < a }
29 id 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) )
30 inss1 
 |-  ( w i^i dom F ) C_ w
31 29 30 eqsstrdi 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. dom F | ( F ` x ) < a } C_ w )
32 28 31 sstrid 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. ( B i^i dom F ) | ( F ` x ) < a } C_ w )
33 ssrab2 
 |-  { x e. ( B i^i dom F ) | ( F ` x ) < a } C_ ( B i^i dom F )
34 33 a1i 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. ( B i^i dom F ) | ( F ` x ) < a } C_ ( B i^i dom F ) )
35 32 34 ssind 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. ( B i^i dom F ) | ( F ` x ) < a } C_ ( w i^i ( B i^i dom F ) ) )
36 nfrab1 
 |-  F/_ x { x e. dom F | ( F ` x ) < a }
37 36 nfeq1 
 |-  F/ x { x e. dom F | ( F ` x ) < a } = ( w i^i dom F )
38 nfcv 
 |-  F/_ x ( w i^i ( B i^i dom F ) )
39 nfrab1 
 |-  F/_ x { x e. ( B i^i dom F ) | ( F ` x ) < a }
40 elinel2 
 |-  ( x e. ( w i^i ( B i^i dom F ) ) -> x e. ( B i^i dom F ) )
41 40 adantl 
 |-  ( ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) /\ x e. ( w i^i ( B i^i dom F ) ) ) -> x e. ( B i^i dom F ) )
42 elinel1 
 |-  ( x e. ( w i^i ( B i^i dom F ) ) -> x e. w )
43 40 elin2d 
 |-  ( x e. ( w i^i ( B i^i dom F ) ) -> x e. dom F )
44 42 43 elind 
 |-  ( x e. ( w i^i ( B i^i dom F ) ) -> x e. ( w i^i dom F ) )
45 44 adantl 
 |-  ( ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) /\ x e. ( w i^i ( B i^i dom F ) ) ) -> x e. ( w i^i dom F ) )
46 29 eqcomd 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> ( w i^i dom F ) = { x e. dom F | ( F ` x ) < a } )
47 46 adantr 
 |-  ( ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) /\ x e. ( w i^i ( B i^i dom F ) ) ) -> ( w i^i dom F ) = { x e. dom F | ( F ` x ) < a } )
48 45 47 eleqtrd 
 |-  ( ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) /\ x e. ( w i^i ( B i^i dom F ) ) ) -> x e. { x e. dom F | ( F ` x ) < a } )
49 rabidim2 
 |-  ( x e. { x e. dom F | ( F ` x ) < a } -> ( F ` x ) < a )
50 48 49 syl 
 |-  ( ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) /\ x e. ( w i^i ( B i^i dom F ) ) ) -> ( F ` x ) < a )
51 41 50 rabidd 
 |-  ( ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) /\ x e. ( w i^i ( B i^i dom F ) ) ) -> x e. { x e. ( B i^i dom F ) | ( F ` x ) < a } )
52 37 38 39 51 ssdf2 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> ( w i^i ( B i^i dom F ) ) C_ { x e. ( B i^i dom F ) | ( F ` x ) < a } )
53 35 52 eqssd 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. ( B i^i dom F ) | ( F ` x ) < a } = ( w i^i ( B i^i dom F ) ) )
54 26 53 eqtrid 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } = ( w i^i ( B i^i dom F ) ) )
55 54 3ad2ant3 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } = ( w i^i ( B i^i dom F ) ) )
56 14 3ad2ant1 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> S e. SAlg )
57 simp1l 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> ph )
58 18 11 ssexd 
 |-  ( ph -> ( B i^i dom F ) e. _V )
59 57 58 syl 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> ( B i^i dom F ) e. _V )
60 simp2 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> w e. S )
61 eqid 
 |-  ( w i^i ( B i^i dom F ) ) = ( w i^i ( B i^i dom F ) )
62 56 59 60 61 elrestd 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> ( w i^i ( B i^i dom F ) ) e. ( S |`t ( B i^i dom F ) ) )
63 55 62 eqeltrd 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } e. ( S |`t ( B i^i dom F ) ) )
64 63 rexlimdv3a 
 |-  ( ( ph /\ a e. RR ) -> ( E. w e. S { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } e. ( S |`t ( B i^i dom F ) ) ) )
65 22 64 mpd 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } e. ( S |`t ( B i^i dom F ) ) )
66 3 1 7 13 65 issmfd 
 |-  ( ph -> ( F |` B ) e. ( SMblFn ` S ) )