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 1 2 5 smff 
 |-  ( ph -> F : dom F --> RR )
9 4 a1i 
 |-  ( ph -> ( B i^i dom F ) C_ dom F )
10 fssres 
 |-  ( ( F : dom F --> RR /\ ( B i^i dom F ) C_ dom F ) -> ( F |` ( B i^i dom F ) ) : ( B i^i dom F ) --> RR )
11 8 9 10 syl2anc 
 |-  ( ph -> ( F |` ( B i^i dom F ) ) : ( B i^i dom F ) --> RR )
12 8 freld 
 |-  ( ph -> Rel F )
13 resindm 
 |-  ( Rel F -> ( F |` ( B i^i dom F ) ) = ( F |` B ) )
14 12 13 syl 
 |-  ( ph -> ( F |` ( B i^i dom F ) ) = ( F |` B ) )
15 14 eqcomd 
 |-  ( ph -> ( F |` B ) = ( F |` ( B i^i dom F ) ) )
16 dmres 
 |-  dom ( F |` B ) = ( B i^i dom F )
17 16 a1i 
 |-  ( ph -> dom ( F |` B ) = ( B i^i dom F ) )
18 15 17 feq12d 
 |-  ( ph -> ( ( F |` B ) : dom ( F |` B ) --> RR <-> ( F |` ( B i^i dom F ) ) : ( B i^i dom F ) --> RR ) )
19 11 18 mpbird 
 |-  ( ph -> ( F |` B ) : dom ( F |` B ) --> RR )
20 17 feq2d 
 |-  ( ph -> ( ( F |` B ) : dom ( F |` B ) --> RR <-> ( F |` B ) : ( B i^i dom F ) --> RR ) )
21 19 20 mpbid 
 |-  ( ph -> ( F |` B ) : ( B i^i dom F ) --> RR )
22 1 adantr 
 |-  ( ( ph /\ a e. RR ) -> S e. SAlg )
23 2 adantr 
 |-  ( ( ph /\ a e. RR ) -> F e. ( SMblFn ` S ) )
24 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
25 22 23 5 24 smfpreimalt 
 |-  ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) )
26 2 dmexd 
 |-  ( ph -> dom F e. _V )
27 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 ) ) )
28 1 26 27 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 ) ) )
29 28 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 ) ) )
30 25 29 mpbid 
 |-  ( ( ph /\ a e. RR ) -> E. w e. S { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) )
31 elinel1 
 |-  ( x e. ( B i^i dom F ) -> x e. B )
32 31 fvresd 
 |-  ( x e. ( B i^i dom F ) -> ( ( F |` B ) ` x ) = ( F ` x ) )
33 32 breq1d 
 |-  ( x e. ( B i^i dom F ) -> ( ( ( F |` B ) ` x ) < a <-> ( F ` x ) < a ) )
34 33 rabbiia 
 |-  { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } = { x e. ( B i^i dom F ) | ( F ` x ) < a }
35 34 a1i 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } = { x e. ( B i^i dom F ) | ( F ` x ) < a } )
36 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 } )
37 4 36 ax-mp 
 |-  { x e. ( B i^i dom F ) | ( F ` x ) < a } C_ { x e. dom F | ( F ` x ) < a }
38 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 ) )
39 inss1 
 |-  ( w i^i dom F ) C_ w
40 39 a1i 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> ( w i^i dom F ) C_ w )
41 38 40 eqsstrd 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> { x e. dom F | ( F ` x ) < a } C_ w )
42 37 41 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 )
43 ssrab2 
 |-  { x e. ( B i^i dom F ) | ( F ` x ) < a } C_ ( B i^i dom F )
44 43 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 ) )
45 42 44 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 ) ) )
46 nfrab1 
 |-  F/_ x { x e. dom F | ( F ` x ) < a }
47 nfcv 
 |-  F/_ x ( w i^i dom F )
48 46 47 nfeq 
 |-  F/ x { x e. dom F | ( F ` x ) < a } = ( w i^i dom F )
49 elinel2 
 |-  ( x e. ( w i^i ( B i^i dom F ) ) -> x e. ( B i^i dom F ) )
50 49 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 ) )
51 elinel1 
 |-  ( x e. ( w i^i ( B i^i dom F ) ) -> x e. w )
52 4 sseli 
 |-  ( x e. ( B i^i dom F ) -> x e. dom F )
53 49 52 syl 
 |-  ( x e. ( w i^i ( B i^i dom F ) ) -> x e. dom F )
54 51 53 elind 
 |-  ( x e. ( w i^i ( B i^i dom F ) ) -> x e. ( w i^i dom F ) )
55 54 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 ) )
56 38 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 } )
57 56 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 } )
58 55 57 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 } )
59 rabid 
 |-  ( x e. { x e. dom F | ( F ` x ) < a } <-> ( x e. dom F /\ ( F ` x ) < a ) )
60 59 biimpi 
 |-  ( x e. { x e. dom F | ( F ` x ) < a } -> ( x e. dom F /\ ( F ` x ) < a ) )
61 60 simprd 
 |-  ( x e. { x e. dom F | ( F ` x ) < a } -> ( F ` x ) < a )
62 58 61 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 )
63 50 62 jca 
 |-  ( ( { 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 ) /\ ( F ` x ) < a ) )
64 rabid 
 |-  ( x e. { x e. ( B i^i dom F ) | ( F ` x ) < a } <-> ( x e. ( B i^i dom F ) /\ ( F ` x ) < a ) )
65 63 64 sylibr 
 |-  ( ( { 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 } )
66 65 ex 
 |-  ( { 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 } ) )
67 48 66 ralrimi 
 |-  ( { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) -> A. x e. ( w i^i ( B i^i dom F ) ) x e. { x e. ( B i^i dom F ) | ( F ` x ) < a } )
68 nfcv 
 |-  F/_ x ( w i^i ( B i^i dom F ) )
69 nfrab1 
 |-  F/_ x { x e. ( B i^i dom F ) | ( F ` x ) < a }
70 68 69 dfss3f 
 |-  ( ( w i^i ( B i^i dom F ) ) C_ { x e. ( B i^i dom F ) | ( F ` x ) < a } <-> A. x e. ( w i^i ( B i^i dom F ) ) x e. { x e. ( B i^i dom F ) | ( F ` x ) < a } )
71 67 70 sylibr 
 |-  ( { 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 } )
72 38 38 38 71 4syl 
 |-  ( { 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 } )
73 45 72 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 ) ) )
74 35 73 eqtrd 
 |-  ( { 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 ) ) )
75 74 adantl 
 |-  ( ( ( ph /\ a e. RR ) /\ { 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 ) ) )
76 75 3adant2 
 |-  ( ( ( 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 ) ) )
77 22 3ad2ant1 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> S e. SAlg )
78 simp1l 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> ph )
79 26 9 ssexd 
 |-  ( ph -> ( B i^i dom F ) e. _V )
80 78 79 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 )
81 simp2 
 |-  ( ( ( ph /\ a e. RR ) /\ w e. S /\ { x e. dom F | ( F ` x ) < a } = ( w i^i dom F ) ) -> w e. S )
82 eqid 
 |-  ( w i^i ( B i^i dom F ) ) = ( w i^i ( B i^i dom F ) )
83 77 80 81 82 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 ) ) )
84 76 83 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 ) ) )
85 84 3exp 
 |-  ( ( 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 ) ) ) ) )
86 85 rexlimdv 
 |-  ( ( 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 ) ) ) )
87 30 86 mpd 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( B i^i dom F ) | ( ( F |` B ) ` x ) < a } e. ( S |`t ( B i^i dom F ) ) )
88 3 1 7 21 87 issmfd 
 |-  ( ph -> ( F |` B ) e. ( SMblFn ` S ) )