Metamath Proof Explorer


Theorem xrge0tsms

Description: Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015) (Proof shortened by AV, 26-Jul-2019)

Ref Expression
Hypotheses xrge0tsms.g G = 𝑠 * 𝑠 0 +∞
xrge0tsms.a φ A V
xrge0tsms.f φ F : A 0 +∞
xrge0tsms.s S = sup ran s 𝒫 A Fin G F s * <
Assertion xrge0tsms φ G tsums F = S

Proof

Step Hyp Ref Expression
1 xrge0tsms.g G = 𝑠 * 𝑠 0 +∞
2 xrge0tsms.a φ A V
3 xrge0tsms.f φ F : A 0 +∞
4 xrge0tsms.s S = sup ran s 𝒫 A Fin G F s * <
5 iccssxr 0 +∞ *
6 xrsbas * = Base 𝑠 *
7 1 6 ressbas2 0 +∞ * 0 +∞ = Base G
8 5 7 ax-mp 0 +∞ = Base G
9 eqid 𝑠 * 𝑠 * −∞ = 𝑠 * 𝑠 * −∞
10 9 xrge0subm 0 +∞ SubMnd 𝑠 * 𝑠 * −∞
11 xrex * V
12 11 difexi * −∞ V
13 simpl x * 0 x x *
14 ge0nemnf x * 0 x x −∞
15 13 14 jca x * 0 x x * x −∞
16 elxrge0 x 0 +∞ x * 0 x
17 eldifsn x * −∞ x * x −∞
18 15 16 17 3imtr4i x 0 +∞ x * −∞
19 18 ssriv 0 +∞ * −∞
20 ressabs * −∞ V 0 +∞ * −∞ 𝑠 * 𝑠 * −∞ 𝑠 0 +∞ = 𝑠 * 𝑠 0 +∞
21 12 19 20 mp2an 𝑠 * 𝑠 * −∞ 𝑠 0 +∞ = 𝑠 * 𝑠 0 +∞
22 1 21 eqtr4i G = 𝑠 * 𝑠 * −∞ 𝑠 0 +∞
23 9 xrs10 0 = 0 𝑠 * 𝑠 * −∞
24 22 23 subm0 0 +∞ SubMnd 𝑠 * 𝑠 * −∞ 0 = 0 G
25 10 24 ax-mp 0 = 0 G
26 xrge0cmn 𝑠 * 𝑠 0 +∞ CMnd
27 1 26 eqeltri G CMnd
28 27 a1i φ s 𝒫 A Fin G CMnd
29 elinel2 s 𝒫 A Fin s Fin
30 29 adantl φ s 𝒫 A Fin s Fin
31 elfpw s 𝒫 A Fin s A s Fin
32 31 simplbi s 𝒫 A Fin s A
33 fssres F : A 0 +∞ s A F s : s 0 +∞
34 3 32 33 syl2an φ s 𝒫 A Fin F s : s 0 +∞
35 c0ex 0 V
36 35 a1i φ s 𝒫 A Fin 0 V
37 34 30 36 fdmfifsupp φ s 𝒫 A Fin finSupp 0 F s
38 8 25 28 30 34 37 gsumcl φ s 𝒫 A Fin G F s 0 +∞
39 5 38 sselid φ s 𝒫 A Fin G F s *
40 39 fmpttd φ s 𝒫 A Fin G F s : 𝒫 A Fin *
41 40 frnd φ ran s 𝒫 A Fin G F s *
42 supxrcl ran s 𝒫 A Fin G F s * sup ran s 𝒫 A Fin G F s * < *
43 41 42 syl φ sup ran s 𝒫 A Fin G F s * < *
44 4 43 eqeltrid φ S *
45 0ss A
46 0fin Fin
47 elfpw 𝒫 A Fin A Fin
48 45 46 47 mpbir2an 𝒫 A Fin
49 0cn 0
50 eqid s 𝒫 A Fin G F s = s 𝒫 A Fin G F s
51 reseq2 s = F s = F
52 res0 F =
53 51 52 eqtrdi s = F s =
54 53 oveq2d s = G F s = G
55 25 gsum0 G = 0
56 54 55 eqtrdi s = G F s = 0
57 50 56 elrnmpt1s 𝒫 A Fin 0 0 ran s 𝒫 A Fin G F s
58 48 49 57 mp2an 0 ran s 𝒫 A Fin G F s
59 supxrub ran s 𝒫 A Fin G F s * 0 ran s 𝒫 A Fin G F s 0 sup ran s 𝒫 A Fin G F s * <
60 41 58 59 sylancl φ 0 sup ran s 𝒫 A Fin G F s * <
61 60 4 breqtrrdi φ 0 S
62 elxrge0 S 0 +∞ S * 0 S
63 44 61 62 sylanbrc φ S 0 +∞
64 letop ordTop Top
65 ovex 0 +∞ V
66 elrest ordTop Top 0 +∞ V u ordTop 𝑡 0 +∞ v ordTop u = v 0 +∞
67 64 65 66 mp2an u ordTop 𝑡 0 +∞ v ordTop u = v 0 +∞
68 elinel1 S v 0 +∞ S v
69 reex V
70 simplrl φ v ordTop S v S v ordTop
71 elrestr ordTop Top V v ordTop v ordTop 𝑡
72 64 69 70 71 mp3an12i φ v ordTop S v S v ordTop 𝑡
73 eqid ordTop 𝑡 = ordTop 𝑡
74 73 xrtgioo topGen ran . = ordTop 𝑡
75 72 74 eleqtrrdi φ v ordTop S v S v topGen ran .
76 simplrr φ v ordTop S v S S v
77 simpr φ v ordTop S v S S
78 76 77 elind φ v ordTop S v S S v
79 tg2 v topGen ran . S v u ran . S u u v
80 75 78 79 syl2anc φ v ordTop S v S u ran . S u u v
81 ioof . : * × * 𝒫
82 ffn . : * × * 𝒫 . Fn * × *
83 ovelrn . Fn * × * u ran . r * w * u = r w
84 81 82 83 mp2b u ran . r * w * u = r w
85 simprrr φ v ordTop S v S r * w * S r w r w v r w v
86 85 adantr φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r w v
87 inss1 v v
88 86 87 sstrdi φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r w v
89 27 a1i φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G CMnd
90 simprrl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y y 𝒫 A Fin
91 elinel2 y 𝒫 A Fin y Fin
92 90 91 syl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y y Fin
93 simp-4l φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y φ
94 93 3 syl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y F : A 0 +∞
95 elfpw y 𝒫 A Fin y A y Fin
96 95 simplbi y 𝒫 A Fin y A
97 90 96 syl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y y A
98 94 97 fssresd φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y F y : y 0 +∞
99 35 a1i φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y 0 V
100 98 92 99 fdmfifsupp φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y finSupp 0 F y
101 8 25 89 92 98 100 gsumcl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y 0 +∞
102 5 101 sselid φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y *
103 simprll φ v ordTop S v S r * w * S r w r w v r *
104 103 adantr φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r *
105 simprrr φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y z y
106 92 105 ssfid φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y z Fin
107 105 97 sstrd φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y z A
108 94 107 fssresd φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y F z : z 0 +∞
109 108 106 99 fdmfifsupp φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y finSupp 0 F z
110 8 25 89 106 108 109 gsumcl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F z 0 +∞
111 5 110 sselid φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F z *
112 simprlr φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r < G F z
113 93 2 syl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y A V
114 1 113 94 90 105 xrge0gsumle φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F z G F y
115 104 111 102 112 114 xrltletrd φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r < G F y
116 93 44 syl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y S *
117 simprlr φ v ordTop S v S r * w * S r w r w v w *
118 117 adantr φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y w *
119 93 41 syl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y ran s 𝒫 A Fin G F s *
120 ovex G F y V
121 reseq2 s = y F s = F y
122 121 oveq2d s = y G F s = G F y
123 50 122 elrnmpt1s y 𝒫 A Fin G F y V G F y ran s 𝒫 A Fin G F s
124 90 120 123 sylancl φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y ran s 𝒫 A Fin G F s
125 supxrub ran s 𝒫 A Fin G F s * G F y ran s 𝒫 A Fin G F s G F y sup ran s 𝒫 A Fin G F s * <
126 119 124 125 syl2anc φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y sup ran s 𝒫 A Fin G F s * <
127 126 4 breqtrrdi φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y S
128 simprrl φ v ordTop S v S r * w * S r w r w v S r w
129 eliooord S r w r < S S < w
130 128 129 syl φ v ordTop S v S r * w * S r w r w v r < S S < w
131 130 simprd φ v ordTop S v S r * w * S r w r w v S < w
132 131 adantr φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y S < w
133 102 116 118 127 132 xrlelttrd φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y < w
134 elioo1 r * w * G F y r w G F y * r < G F y G F y < w
135 104 118 134 syl2anc φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y r w G F y * r < G F y G F y < w
136 102 115 133 135 mpbir3and φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y r w
137 88 136 sseldd φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v
138 137 101 elind φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v 0 +∞
139 138 anassrs φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v 0 +∞
140 139 expr φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v 0 +∞
141 140 ralrimiva φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v 0 +∞
142 130 simpld φ v ordTop S v S r * w * S r w r w v r < S
143 142 4 breqtrdi φ v ordTop S v S r * w * S r w r w v r < sup ran s 𝒫 A Fin G F s * <
144 41 ad3antrrr φ v ordTop S v S r * w * S r w r w v ran s 𝒫 A Fin G F s *
145 supxrlub ran s 𝒫 A Fin G F s * r * r < sup ran s 𝒫 A Fin G F s * < w ran s 𝒫 A Fin G F s r < w
146 144 103 145 syl2anc φ v ordTop S v S r * w * S r w r w v r < sup ran s 𝒫 A Fin G F s * < w ran s 𝒫 A Fin G F s r < w
147 143 146 mpbid φ v ordTop S v S r * w * S r w r w v w ran s 𝒫 A Fin G F s r < w
148 ovex G F z V
149 148 rgenw z 𝒫 A Fin G F z V
150 reseq2 s = z F s = F z
151 150 oveq2d s = z G F s = G F z
152 151 cbvmptv s 𝒫 A Fin G F s = z 𝒫 A Fin G F z
153 breq2 w = G F z r < w r < G F z
154 152 153 rexrnmptw z 𝒫 A Fin G F z V w ran s 𝒫 A Fin G F s r < w z 𝒫 A Fin r < G F z
155 149 154 ax-mp w ran s 𝒫 A Fin G F s r < w z 𝒫 A Fin r < G F z
156 147 155 sylib φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin r < G F z
157 141 156 reximddv φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
158 157 expr φ v ordTop S v S r * w * S r w r w v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
159 eleq2 u = r w S u S r w
160 sseq1 u = r w u v r w v
161 159 160 anbi12d u = r w S u u v S r w r w v
162 161 imbi1d u = r w S u u v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞ S r w r w v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
163 158 162 syl5ibrcom φ v ordTop S v S r * w * u = r w S u u v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
164 163 rexlimdvva φ v ordTop S v S r * w * u = r w S u u v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
165 84 164 syl5bi φ v ordTop S v S u ran . S u u v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
166 165 rexlimdv φ v ordTop S v S u ran . S u u v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
167 80 166 mpd φ v ordTop S v S z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
168 simplrl φ v ordTop S v S = +∞ v ordTop
169 simpr φ v ordTop S v S = +∞ S = +∞
170 simplrr φ v ordTop S v S = +∞ S v
171 169 170 eqeltrrd φ v ordTop S v S = +∞ +∞ v
172 pnfnei v ordTop +∞ v r r +∞ v
173 168 171 172 syl2anc φ v ordTop S v S = +∞ r r +∞ v
174 simprr φ v ordTop S v S = +∞ r r +∞ v r +∞ v
175 174 ad2antrr φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r +∞ v
176 27 a1i φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G CMnd
177 91 ad2antrl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y y Fin
178 simp-5l φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y φ
179 178 3 syl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y F : A 0 +∞
180 96 ad2antrl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y y A
181 179 180 fssresd φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y F y : y 0 +∞
182 35 a1i φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y 0 V
183 181 177 182 fdmfifsupp φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y finSupp 0 F y
184 8 25 176 177 181 183 gsumcl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y 0 +∞
185 5 184 sselid φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y *
186 rexr r r *
187 186 ad2antrl φ v ordTop S v S = +∞ r r +∞ v r *
188 187 ad2antrr φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r *
189 simprr φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y z y
190 177 189 ssfid φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y z Fin
191 189 180 sstrd φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y z A
192 179 191 fssresd φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y F z : z 0 +∞
193 192 190 182 fdmfifsupp φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y finSupp 0 F z
194 8 25 176 190 192 193 gsumcl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F z 0 +∞
195 5 194 sselid φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F z *
196 simplrr φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r < G F z
197 178 2 syl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y A V
198 simprl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y y 𝒫 A Fin
199 1 197 179 198 189 xrge0gsumle φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F z G F y
200 188 195 185 196 199 xrltletrd φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y r < G F y
201 pnfge G F y * G F y +∞
202 185 201 syl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y +∞
203 pnfxr +∞ *
204 elioc1 r * +∞ * G F y r +∞ G F y * r < G F y G F y +∞
205 188 203 204 sylancl φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y r +∞ G F y * r < G F y G F y +∞
206 185 200 202 205 mpbir3and φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y r +∞
207 175 206 sseldd φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v
208 207 184 elind φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v 0 +∞
209 208 expr φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v 0 +∞
210 209 ralrimiva φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z y 𝒫 A Fin z y G F y v 0 +∞
211 ltpnf r r < +∞
212 211 ad2antrl φ v ordTop S v S = +∞ r r +∞ v r < +∞
213 simplr φ v ordTop S v S = +∞ r r +∞ v S = +∞
214 212 213 breqtrrd φ v ordTop S v S = +∞ r r +∞ v r < S
215 214 4 breqtrdi φ v ordTop S v S = +∞ r r +∞ v r < sup ran s 𝒫 A Fin G F s * <
216 41 ad3antrrr φ v ordTop S v S = +∞ r r +∞ v ran s 𝒫 A Fin G F s *
217 216 187 145 syl2anc φ v ordTop S v S = +∞ r r +∞ v r < sup ran s 𝒫 A Fin G F s * < w ran s 𝒫 A Fin G F s r < w
218 215 217 mpbid φ v ordTop S v S = +∞ r r +∞ v w ran s 𝒫 A Fin G F s r < w
219 218 155 sylib φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin r < G F z
220 210 219 reximddv φ v ordTop S v S = +∞ r r +∞ v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
221 173 220 rexlimddv φ v ordTop S v S = +∞ z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
222 ge0nemnf S * 0 S S −∞
223 44 61 222 syl2anc φ S −∞
224 44 223 jca φ S * S −∞
225 224 adantr φ v ordTop S v S * S −∞
226 xrnemnf S * S −∞ S S = +∞
227 225 226 sylib φ v ordTop S v S S = +∞
228 167 221 227 mpjaodan φ v ordTop S v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
229 228 expr φ v ordTop S v z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
230 68 229 syl5 φ v ordTop S v 0 +∞ z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
231 eleq2 u = v 0 +∞ S u S v 0 +∞
232 eleq2 u = v 0 +∞ G F y u G F y v 0 +∞
233 232 imbi2d u = v 0 +∞ z y G F y u z y G F y v 0 +∞
234 233 rexralbidv u = v 0 +∞ z 𝒫 A Fin y 𝒫 A Fin z y G F y u z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
235 231 234 imbi12d u = v 0 +∞ S u z 𝒫 A Fin y 𝒫 A Fin z y G F y u S v 0 +∞ z 𝒫 A Fin y 𝒫 A Fin z y G F y v 0 +∞
236 230 235 syl5ibrcom φ v ordTop u = v 0 +∞ S u z 𝒫 A Fin y 𝒫 A Fin z y G F y u
237 236 rexlimdva φ v ordTop u = v 0 +∞ S u z 𝒫 A Fin y 𝒫 A Fin z y G F y u
238 67 237 syl5bi φ u ordTop 𝑡 0 +∞ S u z 𝒫 A Fin y 𝒫 A Fin z y G F y u
239 238 ralrimiv φ u ordTop 𝑡 0 +∞ S u z 𝒫 A Fin y 𝒫 A Fin z y G F y u
240 xrstset ordTop = TopSet 𝑠 *
241 1 240 resstset 0 +∞ V ordTop = TopSet G
242 65 241 ax-mp ordTop = TopSet G
243 8 242 topnval ordTop 𝑡 0 +∞ = TopOpen G
244 eqid 𝒫 A Fin = 𝒫 A Fin
245 27 a1i φ G CMnd
246 xrstps 𝑠 * TopSp
247 resstps 𝑠 * TopSp 0 +∞ V 𝑠 * 𝑠 0 +∞ TopSp
248 246 65 247 mp2an 𝑠 * 𝑠 0 +∞ TopSp
249 1 248 eqeltri G TopSp
250 249 a1i φ G TopSp
251 8 243 244 245 250 2 3 eltsms φ S G tsums F S 0 +∞ u ordTop 𝑡 0 +∞ S u z 𝒫 A Fin y 𝒫 A Fin z y G F y u
252 63 239 251 mpbir2and φ S G tsums F
253 letsr TosetRel
254 ordthaus TosetRel ordTop Haus
255 253 254 mp1i φ ordTop Haus
256 resthaus ordTop Haus 0 +∞ V ordTop 𝑡 0 +∞ Haus
257 255 65 256 sylancl φ ordTop 𝑡 0 +∞ Haus
258 8 245 250 2 3 243 257 haustsms2 φ S G tsums F G tsums F = S
259 252 258 mpd φ G tsums F = S