Metamath Proof Explorer

Theorem smfresal

Description: Given a sigma-measurable function, the subsets of RR whose preimage is in the sigma-algebra induced by the function's domain, form a sigma-algebra. First part of the proof of Proposition 121E (f) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfresal.s 
|- ( ph -> S e. SAlg )
smfresal.f 
|- ( ph -> F e. ( SMblFn ` S ) )
smfresal.d 
|- D = dom F
smfresal.t 
|- T = { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
Assertion smfresal 
|- ( ph -> T e. SAlg )

Proof

Step Hyp Ref Expression
1 smfresal.s 
 |-  ( ph -> S e. SAlg )
2 smfresal.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 smfresal.d 
 |-  D = dom F
4 smfresal.t 
 |-  T = { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
5 reex 
 |-  RR e. _V
6 5 pwex 
 |-  ~P RR e. _V
7 4 6 rabex2 
 |-  T e. _V
8 7 a1i 
 |-  ( ph -> T e. _V )
9 0elpw 
 |-  (/) e. ~P RR
10 9 a1i 
 |-  ( ph -> (/) e. ~P RR )
11 ima0 
 |-  ( `' F " (/) ) = (/)
12 11 a1i 
 |-  ( ph -> ( `' F " (/) ) = (/) )
13 1 uniexd 
 |-  ( ph -> U. S e. _V )
14 1 2 3 smfdmss 
 |-  ( ph -> D C_ U. S )
15 13 14 ssexd 
 |-  ( ph -> D e. _V )
16 eqid 
 |-  ( S |`t D ) = ( S |`t D )
17 1 15 16 subsalsal 
 |-  ( ph -> ( S |`t D ) e. SAlg )
18 17 0sald 
 |-  ( ph -> (/) e. ( S |`t D ) )
19 12 18 eqeltrd 
 |-  ( ph -> ( `' F " (/) ) e. ( S |`t D ) )
20 10 19 jca 
 |-  ( ph -> ( (/) e. ~P RR /\ ( `' F " (/) ) e. ( S |`t D ) ) )
21 imaeq2 
 |-  ( e = (/) -> ( `' F " e ) = ( `' F " (/) ) )
22 21 eleq1d 
 |-  ( e = (/) -> ( ( `' F " e ) e. ( S |`t D ) <-> ( `' F " (/) ) e. ( S |`t D ) ) )
23 22 4 elrab2 
 |-  ( (/) e. T <-> ( (/) e. ~P RR /\ ( `' F " (/) ) e. ( S |`t D ) ) )
24 20 23 sylibr 
 |-  ( ph -> (/) e. T )
25 eqid 
 |-  U. T = U. T
26 nfv 
 |-  F/ y ph
27 nfcv 
 |-  F/_ e y
28 nfrab1 
 |-  F/_ e { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
29 4 28 nfcxfr 
 |-  F/_ e T
30 27 29 eluni2f 
 |-  ( y e. U. T <-> E. e e. T y e. e )
31 30 bilani 
 |-  ( ( ph /\ y e. U. T ) -> E. e e. T y e. e )
32 nfv 
 |-  F/ e ph
33 29 nfuni 
 |-  F/_ e U. T
34 27 33 nfel 
 |-  F/ e y e. U. T
35 32 34 nfan 
 |-  F/ e ( ph /\ y e. U. T )
36 27 nfel1 
 |-  F/ e y e. RR
37 4 eleq2i 
 |-  ( e e. T <-> e e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } )
38 37 biimpi 
 |-  ( e e. T -> e e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } )
39 rabidim1 
 |-  ( e e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } -> e e. ~P RR )
40 38 39 syl 
 |-  ( e e. T -> e e. ~P RR )
41 elpwi 
 |-  ( e e. ~P RR -> e C_ RR )
42 40 41 syl 
 |-  ( e e. T -> e C_ RR )
43 42 adantr 
 |-  ( ( e e. T /\ y e. e ) -> e C_ RR )
44 simpr 
 |-  ( ( e e. T /\ y e. e ) -> y e. e )
45 43 44 sseldd 
 |-  ( ( e e. T /\ y e. e ) -> y e. RR )
46 45 ex 
 |-  ( e e. T -> ( y e. e -> y e. RR ) )
47 46 a1i 
 |-  ( ( ph /\ y e. U. T ) -> ( e e. T -> ( y e. e -> y e. RR ) ) )
48 35 36 47 rexlimd 
 |-  ( ( ph /\ y e. U. T ) -> ( E. e e. T y e. e -> y e. RR ) )
49 31 48 mpd 
 |-  ( ( ph /\ y e. U. T ) -> y e. RR )
50 49 ex 
 |-  ( ph -> ( y e. U. T -> y e. RR ) )
51 ovexd 
 |-  ( ph -> ( ( y - 1 ) (,) ( y + 1 ) ) e. _V )
52 ioossre 
 |-  ( ( y - 1 ) (,) ( y + 1 ) ) C_ RR
53 52 a1i 
 |-  ( ph -> ( ( y - 1 ) (,) ( y + 1 ) ) C_ RR )
54 51 53 elpwd 
 |-  ( ph -> ( ( y - 1 ) (,) ( y + 1 ) ) e. ~P RR )
55 54 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( ( y - 1 ) (,) ( y + 1 ) ) e. ~P RR )
56 1 2 3 smff 
 |-  ( ph -> F : D --> RR )
57 56 ffnd 
 |-  ( ph -> F Fn D )
58 fncnvima2 
 |-  ( F Fn D -> ( `' F " ( ( y - 1 ) (,) ( y + 1 ) ) ) = { x e. D | ( F ` x ) e. ( ( y - 1 ) (,) ( y + 1 ) ) } )
59 57 58 syl 
 |-  ( ph -> ( `' F " ( ( y - 1 ) (,) ( y + 1 ) ) ) = { x e. D | ( F ` x ) e. ( ( y - 1 ) (,) ( y + 1 ) ) } )
60 59 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( `' F " ( ( y - 1 ) (,) ( y + 1 ) ) ) = { x e. D | ( F ` x ) e. ( ( y - 1 ) (,) ( y + 1 ) ) } )
61 nfv 
 |-  F/ x ( ph /\ y e. RR )
62 1 adantr 
 |-  ( ( ph /\ y e. RR ) -> S e. SAlg )
63 15 adantr 
 |-  ( ( ph /\ y e. RR ) -> D e. _V )
64 56 adantr 
 |-  ( ( ph /\ x e. D ) -> F : D --> RR )
65 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
66 64 65 ffvelcdmd 
 |-  ( ( ph /\ x e. D ) -> ( F ` x ) e. RR )
67 66 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. D ) -> ( F ` x ) e. RR )
68 56 feqmptd 
 |-  ( ph -> F = ( x e. D |-> ( F ` x ) ) )
69 68 eqcomd 
 |-  ( ph -> ( x e. D |-> ( F ` x ) ) = F )
70 69 2 eqeltrd 
 |-  ( ph -> ( x e. D |-> ( F ` x ) ) e. ( SMblFn ` S ) )
71 70 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( x e. D |-> ( F ` x ) ) e. ( SMblFn ` S ) )
72 peano2rem 
 |-  ( y e. RR -> ( y - 1 ) e. RR )
73 72 rexrd 
 |-  ( y e. RR -> ( y - 1 ) e. RR* )
74 73 adantl 
 |-  ( ( ph /\ y e. RR ) -> ( y - 1 ) e. RR* )
75 peano2re 
 |-  ( y e. RR -> ( y + 1 ) e. RR )
76 75 rexrd 
 |-  ( y e. RR -> ( y + 1 ) e. RR* )
77 76 adantl 
 |-  ( ( ph /\ y e. RR ) -> ( y + 1 ) e. RR* )
78 61 62 63 67 71 74 77 smfpimioompt 
 |-  ( ( ph /\ y e. RR ) -> { x e. D | ( F ` x ) e. ( ( y - 1 ) (,) ( y + 1 ) ) } e. ( S |`t D ) )
79 60 78 eqeltrd 
 |-  ( ( ph /\ y e. RR ) -> ( `' F " ( ( y - 1 ) (,) ( y + 1 ) ) ) e. ( S |`t D ) )
80 55 79 jca 
 |-  ( ( ph /\ y e. RR ) -> ( ( ( y - 1 ) (,) ( y + 1 ) ) e. ~P RR /\ ( `' F " ( ( y - 1 ) (,) ( y + 1 ) ) ) e. ( S |`t D ) ) )
81 imaeq2 
 |-  ( e = ( ( y - 1 ) (,) ( y + 1 ) ) -> ( `' F " e ) = ( `' F " ( ( y - 1 ) (,) ( y + 1 ) ) ) )
82 81 eleq1d 
 |-  ( e = ( ( y - 1 ) (,) ( y + 1 ) ) -> ( ( `' F " e ) e. ( S |`t D ) <-> ( `' F " ( ( y - 1 ) (,) ( y + 1 ) ) ) e. ( S |`t D ) ) )
83 82 4 elrab2 
 |-  ( ( ( y - 1 ) (,) ( y + 1 ) ) e. T <-> ( ( ( y - 1 ) (,) ( y + 1 ) ) e. ~P RR /\ ( `' F " ( ( y - 1 ) (,) ( y + 1 ) ) ) e. ( S |`t D ) ) )
84 80 83 sylibr 
 |-  ( ( ph /\ y e. RR ) -> ( ( y - 1 ) (,) ( y + 1 ) ) e. T )
85 id 
 |-  ( y e. RR -> y e. RR )
86 ltm1 
 |-  ( y e. RR -> ( y - 1 ) < y )
87 ltp1 
 |-  ( y e. RR -> y < ( y + 1 ) )
88 73 76 85 86 87 eliood 
 |-  ( y e. RR -> y e. ( ( y - 1 ) (,) ( y + 1 ) ) )
89 88 adantl 
 |-  ( ( ph /\ y e. RR ) -> y e. ( ( y - 1 ) (,) ( y + 1 ) ) )
90 nfv 
 |-  F/ e y e. ( ( y - 1 ) (,) ( y + 1 ) )
91 nfcv 
 |-  F/_ e ( ( y - 1 ) (,) ( y + 1 ) )
92 eleq2 
 |-  ( e = ( ( y - 1 ) (,) ( y + 1 ) ) -> ( y e. e <-> y e. ( ( y - 1 ) (,) ( y + 1 ) ) ) )
93 90 91 29 92 rspcef 
 |-  ( ( ( ( y - 1 ) (,) ( y + 1 ) ) e. T /\ y e. ( ( y - 1 ) (,) ( y + 1 ) ) ) -> E. e e. T y e. e )
94 84 89 93 syl2anc 
 |-  ( ( ph /\ y e. RR ) -> E. e e. T y e. e )
95 94 30 sylibr 
 |-  ( ( ph /\ y e. RR ) -> y e. U. T )
96 95 ex 
 |-  ( ph -> ( y e. RR -> y e. U. T ) )
97 50 96 impbid 
 |-  ( ph -> ( y e. U. T <-> y e. RR ) )
98 26 97 alrimi 
 |-  ( ph -> A. y ( y e. U. T <-> y e. RR ) )
99 dfcleq 
 |-  ( U. T = RR <-> A. y ( y e. U. T <-> y e. RR ) )
100 98 99 sylibr 
 |-  ( ph -> U. T = RR )
101 100 difeq1d 
 |-  ( ph -> ( U. T \ x ) = ( RR \ x ) )
102 101 adantr 
 |-  ( ( ph /\ x e. T ) -> ( U. T \ x ) = ( RR \ x ) )
103 difss 
 |-  ( RR \ x ) C_ RR
104 5 103 ssexi 
 |-  ( RR \ x ) e. _V
105 elpwg 
 |-  ( ( RR \ x ) e. _V -> ( ( RR \ x ) e. ~P RR <-> ( RR \ x ) C_ RR ) )
106 104 105 ax-mp 
 |-  ( ( RR \ x ) e. ~P RR <-> ( RR \ x ) C_ RR )
107 103 106 mpbir 
 |-  ( RR \ x ) e. ~P RR
108 107 a1i 
 |-  ( ( ph /\ x e. T ) -> ( RR \ x ) e. ~P RR )
109 56 ffund 
 |-  ( ph -> Fun F )
110 difpreima 
 |-  ( Fun F -> ( `' F " ( RR \ x ) ) = ( ( `' F " RR ) \ ( `' F " x ) ) )
111 109 110 syl 
 |-  ( ph -> ( `' F " ( RR \ x ) ) = ( ( `' F " RR ) \ ( `' F " x ) ) )
112 fimacnv 
 |-  ( F : D --> RR -> ( `' F " RR ) = D )
113 56 112 syl 
 |-  ( ph -> ( `' F " RR ) = D )
114 1 14 restuni4 
 |-  ( ph -> U. ( S |`t D ) = D )
115 113 114 eqtr4d 
 |-  ( ph -> ( `' F " RR ) = U. ( S |`t D ) )
116 115 difeq1d 
 |-  ( ph -> ( ( `' F " RR ) \ ( `' F " x ) ) = ( U. ( S |`t D ) \ ( `' F " x ) ) )
117 111 116 eqtrd 
 |-  ( ph -> ( `' F " ( RR \ x ) ) = ( U. ( S |`t D ) \ ( `' F " x ) ) )
118 117 adantr 
 |-  ( ( ph /\ x e. T ) -> ( `' F " ( RR \ x ) ) = ( U. ( S |`t D ) \ ( `' F " x ) ) )
119 17 adantr 
 |-  ( ( ph /\ x e. T ) -> ( S |`t D ) e. SAlg )
120 imaeq2 
 |-  ( e = x -> ( `' F " e ) = ( `' F " x ) )
121 120 eleq1d 
 |-  ( e = x -> ( ( `' F " e ) e. ( S |`t D ) <-> ( `' F " x ) e. ( S |`t D ) ) )
122 121 4 elrab2 
 |-  ( x e. T <-> ( x e. ~P RR /\ ( `' F " x ) e. ( S |`t D ) ) )
123 122 biimpi 
 |-  ( x e. T -> ( x e. ~P RR /\ ( `' F " x ) e. ( S |`t D ) ) )
124 123 simprd 
 |-  ( x e. T -> ( `' F " x ) e. ( S |`t D ) )
125 124 adantl 
 |-  ( ( ph /\ x e. T ) -> ( `' F " x ) e. ( S |`t D ) )
126 119 125 saldifcld 
 |-  ( ( ph /\ x e. T ) -> ( U. ( S |`t D ) \ ( `' F " x ) ) e. ( S |`t D ) )
127 118 126 eqeltrd 
 |-  ( ( ph /\ x e. T ) -> ( `' F " ( RR \ x ) ) e. ( S |`t D ) )
128 108 127 jca 
 |-  ( ( ph /\ x e. T ) -> ( ( RR \ x ) e. ~P RR /\ ( `' F " ( RR \ x ) ) e. ( S |`t D ) ) )
129 imaeq2 
 |-  ( e = ( RR \ x ) -> ( `' F " e ) = ( `' F " ( RR \ x ) ) )
130 129 eleq1d 
 |-  ( e = ( RR \ x ) -> ( ( `' F " e ) e. ( S |`t D ) <-> ( `' F " ( RR \ x ) ) e. ( S |`t D ) ) )
131 130 4 elrab2 
 |-  ( ( RR \ x ) e. T <-> ( ( RR \ x ) e. ~P RR /\ ( `' F " ( RR \ x ) ) e. ( S |`t D ) ) )
132 128 131 sylibr 
 |-  ( ( ph /\ x e. T ) -> ( RR \ x ) e. T )
133 102 132 eqeltrd 
 |-  ( ( ph /\ x e. T ) -> ( U. T \ x ) e. T )
134 nnex 
 |-  NN e. _V
135 fvex 
 |-  ( g ` n ) e. _V
136 134 135 iunex 
 |-  U_ n e. NN ( g ` n ) e. _V
137 136 a1i 
 |-  ( g : NN --> T -> U_ n e. NN ( g ` n ) e. _V )
138 ffvelcdm 
 |-  ( ( g : NN --> T /\ n e. NN ) -> ( g ` n ) e. T )
139 4 eleq2i 
 |-  ( ( g ` n ) e. T <-> ( g ` n ) e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } )
140 139 biimpi 
 |-  ( ( g ` n ) e. T -> ( g ` n ) e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } )
141 elrabi 
 |-  ( ( g ` n ) e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } -> ( g ` n ) e. ~P RR )
142 elpwi 
 |-  ( ( g ` n ) e. ~P RR -> ( g ` n ) C_ RR )
143 138 140 141 142 4syl 
 |-  ( ( g : NN --> T /\ n e. NN ) -> ( g ` n ) C_ RR )
144 143 iunssd 
 |-  ( g : NN --> T -> U_ n e. NN ( g ` n ) C_ RR )
145 137 144 elpwd 
 |-  ( g : NN --> T -> U_ n e. NN ( g ` n ) e. ~P RR )
146 145 adantl 
 |-  ( ( ph /\ g : NN --> T ) -> U_ n e. NN ( g ` n ) e. ~P RR )
147 imaiun 
 |-  ( `' F " U_ n e. NN ( g ` n ) ) = U_ n e. NN ( `' F " ( g ` n ) )
148 147 a1i 
 |-  ( ( ph /\ g : NN --> T ) -> ( `' F " U_ n e. NN ( g ` n ) ) = U_ n e. NN ( `' F " ( g ` n ) ) )
149 17 adantr 
 |-  ( ( ph /\ g : NN --> T ) -> ( S |`t D ) e. SAlg )
150 nnct 
 |-  NN ~<_ _om
151 150 a1i 
 |-  ( ( ph /\ g : NN --> T ) -> NN ~<_ _om )
152 imaeq2 
 |-  ( e = ( g ` n ) -> ( `' F " e ) = ( `' F " ( g ` n ) ) )
153 152 eleq1d 
 |-  ( e = ( g ` n ) -> ( ( `' F " e ) e. ( S |`t D ) <-> ( `' F " ( g ` n ) ) e. ( S |`t D ) ) )
154 153 4 elrab2 
 |-  ( ( g ` n ) e. T <-> ( ( g ` n ) e. ~P RR /\ ( `' F " ( g ` n ) ) e. ( S |`t D ) ) )
155 154 biimpi 
 |-  ( ( g ` n ) e. T -> ( ( g ` n ) e. ~P RR /\ ( `' F " ( g ` n ) ) e. ( S |`t D ) ) )
156 155 simprd 
 |-  ( ( g ` n ) e. T -> ( `' F " ( g ` n ) ) e. ( S |`t D ) )
157 138 156 syl 
 |-  ( ( g : NN --> T /\ n e. NN ) -> ( `' F " ( g ` n ) ) e. ( S |`t D ) )
158 157 adantll 
 |-  ( ( ( ph /\ g : NN --> T ) /\ n e. NN ) -> ( `' F " ( g ` n ) ) e. ( S |`t D ) )
159 149 151 158 saliuncl 
 |-  ( ( ph /\ g : NN --> T ) -> U_ n e. NN ( `' F " ( g ` n ) ) e. ( S |`t D ) )
160 148 159 eqeltrd 
 |-  ( ( ph /\ g : NN --> T ) -> ( `' F " U_ n e. NN ( g ` n ) ) e. ( S |`t D ) )
161 146 160 jca 
 |-  ( ( ph /\ g : NN --> T ) -> ( U_ n e. NN ( g ` n ) e. ~P RR /\ ( `' F " U_ n e. NN ( g ` n ) ) e. ( S |`t D ) ) )
162 imaeq2 
 |-  ( e = U_ n e. NN ( g ` n ) -> ( `' F " e ) = ( `' F " U_ n e. NN ( g ` n ) ) )
163 162 eleq1d 
 |-  ( e = U_ n e. NN ( g ` n ) -> ( ( `' F " e ) e. ( S |`t D ) <-> ( `' F " U_ n e. NN ( g ` n ) ) e. ( S |`t D ) ) )
164 163 4 elrab2 
 |-  ( U_ n e. NN ( g ` n ) e. T <-> ( U_ n e. NN ( g ` n ) e. ~P RR /\ ( `' F " U_ n e. NN ( g ` n ) ) e. ( S |`t D ) ) )
165 161 164 sylibr 
 |-  ( ( ph /\ g : NN --> T ) -> U_ n e. NN ( g ` n ) e. T )
166 8 24 25 133 165 issalnnd 
 |-  ( ph -> T e. SAlg )