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