Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem57 Structured version   Visualization version   GIF version

Theorem stoweidlem57 42210
 Description: There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem57.1 𝑡𝐷
stoweidlem57.2 𝑡𝑈
stoweidlem57.3 𝑡𝜑
stoweidlem57.4 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
stoweidlem57.5 𝑉 = {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
stoweidlem57.6 𝐾 = (topGen‘ran (,))
stoweidlem57.7 𝑇 = 𝐽
stoweidlem57.8 𝐶 = (𝐽 Cn 𝐾)
stoweidlem57.9 𝑈 = (𝑇𝐵)
stoweidlem57.10 (𝜑𝐽 ∈ Comp)
stoweidlem57.11 (𝜑𝐴𝐶)
stoweidlem57.12 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
stoweidlem57.13 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem57.14 ((𝜑𝑎 ∈ ℝ) → (𝑡𝑇𝑎) ∈ 𝐴)
stoweidlem57.15 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
stoweidlem57.16 (𝜑𝐵 ∈ (Clsd‘𝐽))
stoweidlem57.17 (𝜑𝐷 ∈ (Clsd‘𝐽))
stoweidlem57.18 (𝜑 → (𝐵𝐷) = ∅)
stoweidlem57.19 (𝜑𝐷 ≠ ∅)
stoweidlem57.20 (𝜑𝐸 ∈ ℝ+)
stoweidlem57.21 (𝜑𝐸 < (1 / 3))
Assertion
Ref Expression
stoweidlem57 (𝜑 → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡)))
Distinct variable groups:   𝑒,𝑎,𝑓,𝑡   𝑞,𝑎,𝑟,𝑓,𝑡,𝐴   𝐴,𝑒,𝑓,𝑡   𝐷,𝑎,𝑒,𝑓   𝑇,𝑎,𝑒,𝑓,𝑡   𝑈,𝑎,𝑒,𝑓   𝜑,𝑎,𝑒,𝑓   𝑒,𝑔,,𝑓,𝑡,𝐴   𝑤,𝑒,,𝑡,𝐴   𝑒,𝐸,𝑓,𝑔,,𝑡   𝑔,𝑟,,𝐴   𝑥,𝑓,𝑔,,𝑡,𝐴   𝐵,𝑓,𝑔,𝑟   𝑓,𝑉,𝑔,𝑟   𝑓,𝑌,𝑔,𝑟   𝑔,𝑞,𝐷   𝐷,,𝑟   𝑔,𝐽,,𝑡   𝑇,𝑔,,𝑟   𝑈,𝑔,,𝑟   𝜑,𝑔,,𝑟   𝑤,𝑟,𝐸   𝐴,𝑞   𝐷,𝑞   𝑇,𝑞   𝑈,𝑞   𝜑,𝑞   𝑤,𝐷   𝑤,𝐵   𝑡,𝐾   𝜑,𝑤   𝑤,𝐽   𝑤,𝑇   𝑤,𝑈   𝑤,𝑌   𝑥,𝐵   𝑥,𝐷   𝑥,𝐸   𝑥,𝑇
Allowed substitution hints:   𝜑(𝑥,𝑡)   𝐵(𝑡,𝑒,,𝑞,𝑎)   𝐶(𝑥,𝑤,𝑡,𝑒,𝑓,𝑔,,𝑟,𝑞,𝑎)   𝐷(𝑡)   𝑈(𝑥,𝑡)   𝐸(𝑞,𝑎)   𝐽(𝑥,𝑒,𝑓,𝑟,𝑞,𝑎)   𝐾(𝑥,𝑤,𝑒,𝑓,𝑔,,𝑟,𝑞,𝑎)   𝑉(𝑥,𝑤,𝑡,𝑒,,𝑞,𝑎)   𝑌(𝑥,𝑡,𝑒,,𝑞,𝑎)

Proof of Theorem stoweidlem57
Dummy variables 𝑠 𝑚 𝑖 𝑣 𝑦 𝑢 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem57.2 . . . . . . . . . 10 𝑡𝑈
2 stoweidlem57.3 . . . . . . . . . . 11 𝑡𝜑
3 stoweidlem57.1 . . . . . . . . . . . 12 𝑡𝐷
43nfcri 2975 . . . . . . . . . . 11 𝑡 𝑠𝐷
52, 4nfan 1893 . . . . . . . . . 10 𝑡(𝜑𝑠𝐷)
6 stoweidlem57.6 . . . . . . . . . 10 𝐾 = (topGen‘ran (,))
7 stoweidlem57.10 . . . . . . . . . . 11 (𝜑𝐽 ∈ Comp)
87adantr 481 . . . . . . . . . 10 ((𝜑𝑠𝐷) → 𝐽 ∈ Comp)
9 stoweidlem57.7 . . . . . . . . . 10 𝑇 = 𝐽
10 stoweidlem57.8 . . . . . . . . . 10 𝐶 = (𝐽 Cn 𝐾)
11 stoweidlem57.11 . . . . . . . . . . 11 (𝜑𝐴𝐶)
1211adantr 481 . . . . . . . . . 10 ((𝜑𝑠𝐷) → 𝐴𝐶)
13 stoweidlem57.12 . . . . . . . . . . 11 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
14133adant1r 1171 . . . . . . . . . 10 (((𝜑𝑠𝐷) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
15 stoweidlem57.13 . . . . . . . . . . 11 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
16153adant1r 1171 . . . . . . . . . 10 (((𝜑𝑠𝐷) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
17 stoweidlem57.14 . . . . . . . . . . 11 ((𝜑𝑎 ∈ ℝ) → (𝑡𝑇𝑎) ∈ 𝐴)
1817adantlr 711 . . . . . . . . . 10 (((𝜑𝑠𝐷) ∧ 𝑎 ∈ ℝ) → (𝑡𝑇𝑎) ∈ 𝐴)
19 stoweidlem57.15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
2019adantlr 711 . . . . . . . . . 10 (((𝜑𝑠𝐷) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
21 stoweidlem57.9 . . . . . . . . . . . 12 𝑈 = (𝑇𝐵)
22 stoweidlem57.16 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (Clsd‘𝐽))
23 cmptop 21921 . . . . . . . . . . . . . . 15 (𝐽 ∈ Comp → 𝐽 ∈ Top)
249iscld 21553 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top → (𝐵 ∈ (Clsd‘𝐽) ↔ (𝐵𝑇 ∧ (𝑇𝐵) ∈ 𝐽)))
257, 23, 243syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 ∈ (Clsd‘𝐽) ↔ (𝐵𝑇 ∧ (𝑇𝐵) ∈ 𝐽)))
2622, 25mpbid 233 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝑇 ∧ (𝑇𝐵) ∈ 𝐽))
2726simprd 496 . . . . . . . . . . . 12 (𝜑 → (𝑇𝐵) ∈ 𝐽)
2821, 27eqeltrid 2921 . . . . . . . . . . 11 (𝜑𝑈𝐽)
2928adantr 481 . . . . . . . . . 10 ((𝜑𝑠𝐷) → 𝑈𝐽)
30 stoweidlem57.17 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ (Clsd‘𝐽))
319cldss 21555 . . . . . . . . . . . . . 14 (𝐷 ∈ (Clsd‘𝐽) → 𝐷𝑇)
3230, 31syl 17 . . . . . . . . . . . . 13 (𝜑𝐷𝑇)
3332sselda 3970 . . . . . . . . . . . 12 ((𝜑𝑠𝐷) → 𝑠𝑇)
34 stoweidlem57.18 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐷) = ∅)
35 disjr 4402 . . . . . . . . . . . . . 14 ((𝐵𝐷) = ∅ ↔ ∀𝑠𝐷 ¬ 𝑠𝐵)
3634, 35sylib 219 . . . . . . . . . . . . 13 (𝜑 → ∀𝑠𝐷 ¬ 𝑠𝐵)
3736r19.21bi 3212 . . . . . . . . . . . 12 ((𝜑𝑠𝐷) → ¬ 𝑠𝐵)
3833, 37eldifd 3950 . . . . . . . . . . 11 ((𝜑𝑠𝐷) → 𝑠 ∈ (𝑇𝐵))
3938, 21syl6eleqr 2928 . . . . . . . . . 10 ((𝜑𝑠𝐷) → 𝑠𝑈)
401, 5, 6, 8, 9, 10, 12, 14, 16, 18, 20, 29, 39stoweidlem56 42209 . . . . . . . . 9 ((𝜑𝑠𝐷) → ∃𝑤𝐽 ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))))
41 simpl 483 . . . . . . . . . . 11 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → 𝑤𝐽)
42 simprll 775 . . . . . . . . . . 11 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → 𝑠𝑤)
43 simprr 769 . . . . . . . . . . . 12 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))
44 stoweidlem57.5 . . . . . . . . . . . . 13 𝑉 = {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
4544rabeq2i 3492 . . . . . . . . . . . 12 (𝑤𝑉 ↔ (𝑤𝐽 ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))))
4641, 43, 45sylanbrc 583 . . . . . . . . . . 11 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → 𝑤𝑉)
4741, 42, 46jca32 516 . . . . . . . . . 10 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → (𝑤𝐽 ∧ (𝑠𝑤𝑤𝑉)))
4847reximi2 3248 . . . . . . . . 9 (∃𝑤𝐽 ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))) → ∃𝑤𝐽 (𝑠𝑤𝑤𝑉))
49 rexex 3244 . . . . . . . . 9 (∃𝑤𝐽 (𝑠𝑤𝑤𝑉) → ∃𝑤(𝑠𝑤𝑤𝑉))
5040, 48, 493syl 18 . . . . . . . 8 ((𝜑𝑠𝐷) → ∃𝑤(𝑠𝑤𝑤𝑉))
51 nfcv 2981 . . . . . . . . 9 𝑤𝑠
52 nfrab1 3389 . . . . . . . . . 10 𝑤{𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
5344, 52nfcxfr 2979 . . . . . . . . 9 𝑤𝑉
5451, 53elunif 41140 . . . . . . . 8 (𝑠 𝑉 ↔ ∃𝑤(𝑠𝑤𝑤𝑉))
5550, 54sylibr 235 . . . . . . 7 ((𝜑𝑠𝐷) → 𝑠 𝑉)
5655ex 413 . . . . . 6 (𝜑 → (𝑠𝐷𝑠 𝑉))
5756ssrdv 3976 . . . . 5 (𝜑𝐷 𝑉)
58 cmpcld 21928 . . . . . . . 8 ((𝐽 ∈ Comp ∧ 𝐷 ∈ (Clsd‘𝐽)) → (𝐽t 𝐷) ∈ Comp)
597, 30, 58syl2anc 584 . . . . . . 7 (𝜑 → (𝐽t 𝐷) ∈ Comp)
607, 23syl 17 . . . . . . . 8 (𝜑𝐽 ∈ Top)
619cmpsub 21926 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐷𝑇) → ((𝐽t 𝐷) ∈ Comp ↔ ∀𝑘 ∈ 𝒫 𝐽(𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢)))
6260, 32, 61syl2anc 584 . . . . . . 7 (𝜑 → ((𝐽t 𝐷) ∈ Comp ↔ ∀𝑘 ∈ 𝒫 𝐽(𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢)))
6359, 62mpbid 233 . . . . . 6 (𝜑 → ∀𝑘 ∈ 𝒫 𝐽(𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢))
64 ssrab2 4059 . . . . . . . 8 {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))} ⊆ 𝐽
6544, 64eqsstri 4004 . . . . . . 7 𝑉𝐽
6644, 7rabexd 5232 . . . . . . . 8 (𝜑𝑉 ∈ V)
67 elpwg 4547 . . . . . . . 8 (𝑉 ∈ V → (𝑉 ∈ 𝒫 𝐽𝑉𝐽))
6866, 67syl 17 . . . . . . 7 (𝜑 → (𝑉 ∈ 𝒫 𝐽𝑉𝐽))
6965, 68mpbiri 259 . . . . . 6 (𝜑𝑉 ∈ 𝒫 𝐽)
70 unieq 4844 . . . . . . . . 9 (𝑘 = 𝑉 𝑘 = 𝑉)
7170sseq2d 4002 . . . . . . . 8 (𝑘 = 𝑉 → (𝐷 𝑘𝐷 𝑉))
72 pweq 4544 . . . . . . . . . 10 (𝑘 = 𝑉 → 𝒫 𝑘 = 𝒫 𝑉)
7372ineq1d 4191 . . . . . . . . 9 (𝑘 = 𝑉 → (𝒫 𝑘 ∩ Fin) = (𝒫 𝑉 ∩ Fin))
7473rexeqdv 3421 . . . . . . . 8 (𝑘 = 𝑉 → (∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢 ↔ ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢))
7571, 74imbi12d 346 . . . . . . 7 (𝑘 = 𝑉 → ((𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢) ↔ (𝐷 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢)))
7675rspccva 3625 . . . . . 6 ((∀𝑘 ∈ 𝒫 𝐽(𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢) ∧ 𝑉 ∈ 𝒫 𝐽) → (𝐷 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢))
7763, 69, 76syl2anc 584 . . . . 5 (𝜑 → (𝐷 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢))
7857, 77mpd 15 . . . 4 (𝜑 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢)
79 elinel1 4175 . . . . . . . . 9 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → 𝑢 ∈ 𝒫 𝑉)
80 elpwi 4553 . . . . . . . . . . 11 (𝑢 ∈ 𝒫 𝑉𝑢𝑉)
8180ssdifssd 4122 . . . . . . . . . 10 (𝑢 ∈ 𝒫 𝑉 → (𝑢 ∖ {∅}) ⊆ 𝑉)
82 vex 3502 . . . . . . . . . . . 12 𝑢 ∈ V
83 difexg 5227 . . . . . . . . . . . 12 (𝑢 ∈ V → (𝑢 ∖ {∅}) ∈ V)
8482, 83ax-mp 5 . . . . . . . . . . 11 (𝑢 ∖ {∅}) ∈ V
8584elpw 4548 . . . . . . . . . 10 ((𝑢 ∖ {∅}) ∈ 𝒫 𝑉 ↔ (𝑢 ∖ {∅}) ⊆ 𝑉)
8681, 85sylibr 235 . . . . . . . . 9 (𝑢 ∈ 𝒫 𝑉 → (𝑢 ∖ {∅}) ∈ 𝒫 𝑉)
8779, 86syl 17 . . . . . . . 8 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈ 𝒫 𝑉)
88 elinel2 4176 . . . . . . . . 9 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → 𝑢 ∈ Fin)
89 diffi 8742 . . . . . . . . 9 (𝑢 ∈ Fin → (𝑢 ∖ {∅}) ∈ Fin)
9088, 89syl 17 . . . . . . . 8 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈ Fin)
9187, 90elind 4174 . . . . . . 7 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈ (𝒫 𝑉 ∩ Fin))
92913ad2ant2 1128 . . . . . 6 ((𝜑𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 𝑢) → (𝑢 ∖ {∅}) ∈ (𝒫 𝑉 ∩ Fin))
93 unidif0 5256 . . . . . . . . 9 (𝑢 ∖ {∅}) = 𝑢
9493sseq2i 3999 . . . . . . . 8 (𝐷 (𝑢 ∖ {∅}) ↔ 𝐷 𝑢)
9594biimpri 229 . . . . . . 7 (𝐷 𝑢𝐷 (𝑢 ∖ {∅}))
96953ad2ant3 1129 . . . . . 6 ((𝜑𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 𝑢) → 𝐷 (𝑢 ∖ {∅}))
97 eldifsni 4720 . . . . . . . 8 (𝑤 ∈ (𝑢 ∖ {∅}) → 𝑤 ≠ ∅)
9897rgen 3152 . . . . . . 7 𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅
9998a1i 11 . . . . . 6 ((𝜑𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 𝑢) → ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)
100 unieq 4844 . . . . . . . . 9 (𝑟 = (𝑢 ∖ {∅}) → 𝑟 = (𝑢 ∖ {∅}))
101100sseq2d 4002 . . . . . . . 8 (𝑟 = (𝑢 ∖ {∅}) → (𝐷 𝑟𝐷 (𝑢 ∖ {∅})))
102 raleq 3410 . . . . . . . 8 (𝑟 = (𝑢 ∖ {∅}) → (∀𝑤𝑟 𝑤 ≠ ∅ ↔ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅))
103101, 102anbi12d 630 . . . . . . 7 (𝑟 = (𝑢 ∖ {∅}) → ((𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅) ↔ (𝐷 (𝑢 ∖ {∅}) ∧ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)))
104103rspcev 3626 . . . . . 6 (((𝑢 ∖ {∅}) ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 (𝑢 ∖ {∅}) ∧ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)) → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
10592, 96, 99, 104syl12anc 834 . . . . 5 ((𝜑𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 𝑢) → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
106105rexlimdv3a 3290 . . . 4 (𝜑 → (∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢 → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)))
10778, 106mpd 15 . . 3 (𝜑 → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
108 nfv 1908 . . . . . 6 𝜑
109 nfcv 2981 . . . . . . . . . . . 12 +
110 nfre1 3310 . . . . . . . . . . . 12 𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
111109, 110nfral 3230 . . . . . . . . . . 11 𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
112 nfcv 2981 . . . . . . . . . . 11 𝐽
113111, 112nfrab 3391 . . . . . . . . . 10 {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
11444, 113nfcxfr 2979 . . . . . . . . 9 𝑉
115114nfpw 4557 . . . . . . . 8 𝒫 𝑉
116 nfcv 2981 . . . . . . . 8 Fin
117115, 116nfin 4196 . . . . . . 7 (𝒫 𝑉 ∩ Fin)
118117nfcri 2975 . . . . . 6 𝑟 ∈ (𝒫 𝑉 ∩ Fin)
119 nfv 1908 . . . . . 6 (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)
120108, 118, 119nf3an 1895 . . . . 5 (𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
121 nfcv 2981 . . . . . . . . . . . 12 𝑡+
122 nfcv 2981 . . . . . . . . . . . . 13 𝑡𝐴
123 nfra1 3223 . . . . . . . . . . . . . 14 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
124 nfra1 3223 . . . . . . . . . . . . . 14 𝑡𝑡𝑤 (𝑡) < 𝑒
125 nfra1 3223 . . . . . . . . . . . . . 14 𝑡𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)
126123, 124, 125nf3an 1895 . . . . . . . . . . . . 13 𝑡(∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
127122, 126nfrex 3313 . . . . . . . . . . . 12 𝑡𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
128121, 127nfral 3230 . . . . . . . . . . 11 𝑡𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
129 nfcv 2981 . . . . . . . . . . 11 𝑡𝐽
130128, 129nfrab 3391 . . . . . . . . . 10 𝑡{𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
13144, 130nfcxfr 2979 . . . . . . . . 9 𝑡𝑉
132131nfpw 4557 . . . . . . . 8 𝑡𝒫 𝑉
133 nfcv 2981 . . . . . . . 8 𝑡Fin
134132, 133nfin 4196 . . . . . . 7 𝑡(𝒫 𝑉 ∩ Fin)
135134nfcri 2975 . . . . . 6 𝑡 𝑟 ∈ (𝒫 𝑉 ∩ Fin)
136 nfcv 2981 . . . . . . . 8 𝑡 𝑟
1373, 136nfss 3963 . . . . . . 7 𝑡 𝐷 𝑟
138 nfv 1908 . . . . . . 7 𝑡𝑤𝑟 𝑤 ≠ ∅
139137, 138nfan 1893 . . . . . 6 𝑡(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)
1402, 135, 139nf3an 1895 . . . . 5 𝑡(𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
141 nfv 1908 . . . . . 6 𝑤𝜑
14253nfpw 4557 . . . . . . . 8 𝑤𝒫 𝑉
143 nfcv 2981 . . . . . . . 8 𝑤Fin
144142, 143nfin 4196 . . . . . . 7 𝑤(𝒫 𝑉 ∩ Fin)
145144nfcri 2975 . . . . . 6 𝑤 𝑟 ∈ (𝒫 𝑉 ∩ Fin)
146 nfv 1908 . . . . . . 7 𝑤 𝐷 𝑟
147 nfra1 3223 . . . . . . 7 𝑤𝑤𝑟 𝑤 ≠ ∅
148146, 147nfan 1893 . . . . . 6 𝑤(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)
149141, 145, 148nf3an 1895 . . . . 5 𝑤(𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
150 stoweidlem57.4 . . . . 5 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
151 simp2 1131 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝑟 ∈ (𝒫 𝑉 ∩ Fin))
152 simp3l 1195 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐷 𝑟)
153 stoweidlem57.19 . . . . . 6 (𝜑𝐷 ≠ ∅)
1541533ad2ant1 1127 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐷 ≠ ∅)
155 stoweidlem57.20 . . . . . 6 (𝜑𝐸 ∈ ℝ+)
1561553ad2ant1 1127 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐸 ∈ ℝ+)
15726simpld 495 . . . . . 6 (𝜑𝐵𝑇)
1581573ad2ant1 1127 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐵𝑇)
159663ad2ant1 1127 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝑉 ∈ V)
160 retop 23287 . . . . . . . . 9 (topGen‘ran (,)) ∈ Top
1616, 160eqeltri 2913 . . . . . . . 8 𝐾 ∈ Top
162 cnfex 41152 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V)
16360, 161, 162sylancl 586 . . . . . . 7 (𝜑 → (𝐽 Cn 𝐾) ∈ V)
16411, 10syl6sseq 4020 . . . . . . 7 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
165163, 164ssexd 5224 . . . . . 6 (𝜑𝐴 ∈ V)
1661653ad2ant1 1127 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐴 ∈ V)
167120, 140, 149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166stoweidlem39 42192 . . . 4 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
168167rexlimdv3a 3290 . . 3 (𝜑 → (∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅) → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))))
169107, 168mpd 15 . 2 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
170 nfv 1908 . . . . . . 7 𝑖(𝜑𝑚 ∈ ℕ)
171 nfv 1908 . . . . . . . 8 𝑖 𝑣:(1...𝑚)⟶𝑉
172 nfv 1908 . . . . . . . 8 𝑖 𝐷 ran 𝑣
173 nfv 1908 . . . . . . . . . 10 𝑖 𝑦:(1...𝑚)⟶𝑌
174 nfra1 3223 . . . . . . . . . 10 𝑖𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))
175173, 174nfan 1893 . . . . . . . . 9 𝑖(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
176175nfex 2337 . . . . . . . 8 𝑖𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
177171, 172, 176nf3an 1895 . . . . . . 7 𝑖(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
178170, 177nfan 1893 . . . . . 6 𝑖((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
179 nfv 1908 . . . . . . . 8 𝑡 𝑚 ∈ ℕ
1802, 179nfan 1893 . . . . . . 7 𝑡(𝜑𝑚 ∈ ℕ)
181 nfcv 2981 . . . . . . . . 9 𝑡𝑣
182 nfcv 2981 . . . . . . . . 9 𝑡(1...𝑚)
183181, 182, 131nff 6506 . . . . . . . 8 𝑡 𝑣:(1...𝑚)⟶𝑉
184 nfcv 2981 . . . . . . . . 9 𝑡 ran 𝑣
1853, 184nfss 3963 . . . . . . . 8 𝑡 𝐷 ran 𝑣
186 nfcv 2981 . . . . . . . . . . 11 𝑡𝑦
187123, 122nfrab 3391 . . . . . . . . . . . 12 𝑡{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
188150, 187nfcxfr 2979 . . . . . . . . . . 11 𝑡𝑌
189186, 182, 188nff 6506 . . . . . . . . . 10 𝑡 𝑦:(1...𝑚)⟶𝑌
190 nfra1 3223 . . . . . . . . . . . 12 𝑡𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚)
191 nfra1 3223 . . . . . . . . . . . 12 𝑡𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)
192190, 191nfan 1893 . . . . . . . . . . 11 𝑡(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))
193182, 192nfral 3230 . . . . . . . . . 10 𝑡𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))
194189, 193nfan 1893 . . . . . . . . 9 𝑡(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
195194nfex 2337 . . . . . . . 8 𝑡𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
196183, 185, 195nf3an 1895 . . . . . . 7 𝑡(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
197180, 196nfan 1893 . . . . . 6 𝑡((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
198 nfv 1908 . . . . . . 7 𝑦(𝜑𝑚 ∈ ℕ)
199 nfv 1908 . . . . . . . 8 𝑦 𝑣:(1...𝑚)⟶𝑉
200 nfv 1908 . . . . . . . 8 𝑦 𝐷 ran 𝑣
201 nfe1 2147 . . . . . . . 8 𝑦𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
202199, 200, 201nf3an 1895 . . . . . . 7 𝑦(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
203198, 202nfan 1893 . . . . . 6 𝑦((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
204 nfv 1908 . . . . . . 7 𝑤(𝜑𝑚 ∈ ℕ)
205 nfcv 2981 . . . . . . . . 9 𝑤𝑣
206 nfcv 2981 . . . . . . . . 9 𝑤(1...𝑚)
207205, 206, 53nff 6506 . . . . . . . 8 𝑤 𝑣:(1...𝑚)⟶𝑉
208 nfv 1908 . . . . . . . 8 𝑤 𝐷 ran 𝑣
209 nfv 1908 . . . . . . . 8 𝑤𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
210207, 208, 209nf3an 1895 . . . . . . 7 𝑤(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
211204, 210nfan 1893 . . . . . 6 𝑤((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
212 eqid 2825 . . . . . 6 {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
213 eqid 2825 . . . . . 6 (𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}, 𝑔 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡)))) = (𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}, 𝑔 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
214 eqid 2825 . . . . . 6 (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦𝑖)‘𝑡))) = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦𝑖)‘𝑡)))
215 eqid 2825 . . . . . 6 (𝑡𝑇 ↦ (seq1( · , ((𝑡𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦𝑖)‘𝑡)))‘𝑡))‘𝑚)) = (𝑡𝑇 ↦ (seq1( · , ((𝑡𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦𝑖)‘𝑡)))‘𝑡))‘𝑚))
216 simp1ll 1230 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) ∧ 𝑓𝐴𝑔𝐴) → 𝜑)
217216, 15syld3an1 1404 . . . . . 6 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
21811sselda 3970 . . . . . . . 8 ((𝜑𝑓𝐴) → 𝑓𝐶)
2196, 9, 10, 218fcnre 41149 . . . . . . 7 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
220219ad4ant14 748 . . . . . 6 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) ∧ 𝑓𝐴) → 𝑓:𝑇⟶ℝ)
221 simplr 765 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝑚 ∈ ℕ)
222 simpr1 1188 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝑣:(1...𝑚)⟶𝑉)
2239cldss 21555 . . . . . . . 8 (𝐵 ∈ (Clsd‘𝐽) → 𝐵𝑇)
22422, 223syl 17 . . . . . . 7 (𝜑𝐵𝑇)
225224ad2antrr 722 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐵𝑇)
226 simpr2 1189 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐷 ran 𝑣)
22732ad2antrr 722 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐷𝑇)
228 feq3 6493 . . . . . . . . . . . 12 (𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} → (𝑦:(1...𝑚)⟶𝑌𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}))
229150, 228ax-mp 5 . . . . . . . . . . 11 (𝑦:(1...𝑚)⟶𝑌𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)})
230229biimpi 217 . . . . . . . . . 10 (𝑦:(1...𝑚)⟶𝑌𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)})
231230anim1i 614 . . . . . . . . 9 ((𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))) → (𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
232231eximi 1828 . . . . . . . 8 (∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))) → ∃𝑦(𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
2332323ad2ant3 1129 . . . . . . 7 ((𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))) → ∃𝑦(𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
234233adantl 482 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → ∃𝑦(𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
235 uniexg 7460 . . . . . . . . 9 (𝐽 ∈ Comp → 𝐽 ∈ V)
2367, 235syl 17 . . . . . . . 8 (𝜑 𝐽 ∈ V)
2379, 236eqeltrid 2921 . . . . . . 7 (𝜑𝑇 ∈ V)
238237ad2antrr 722 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝑇 ∈ V)
239155ad2antrr 722 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐸 ∈ ℝ+)
240 stoweidlem57.21 . . . . . . 7 (𝜑𝐸 < (1 / 3))
241240ad2antrr 722 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐸 < (1 / 3))
242178, 197, 203, 211, 9, 212, 213, 214, 215, 44, 217, 220, 221, 222, 225, 226, 227, 234, 238, 239, 241stoweidlem54 42207 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡)))
243242ex 413 . . . 4 ((𝜑𝑚 ∈ ℕ) → ((𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡))))
244243exlimdv 1927 . . 3 ((𝜑𝑚 ∈ ℕ) → (∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡))))
245244rexlimdva 3288 . 2 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡))))
246169, 245mpd 15 1 (𝜑 → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1081   = wceq 1530  ∃wex 1773  Ⅎwnf 1777   ∈ wcel 2107  Ⅎwnfc 2965   ≠ wne 3020  ∀wral 3142  ∃wrex 3143  {crab 3146  Vcvv 3499   ∖ cdif 3936   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  𝒫 cpw 4541  {csn 4563  ∪ cuni 4836   class class class wbr 5062   ↦ cmpt 5142  ran crn 5554  ⟶wf 6347  ‘cfv 6351  (class class class)co 7151   ∈ cmpo 7153  Fincfn 8501  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  ℕcn 11630  3c3 11685  ℝ+crp 12382  (,)cioo 12731  ...cfz 12885  seqcseq 13362   ↾t crest 16686  topGenctg 16703  Topctop 21419  Clsdccld 21542   Cn ccn 21750  Compccmp 21912 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-mulf 10609 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7402  df-om 7572  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-map 8401  df-pm 8402  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ioo 12735  df-ico 12737  df-icc 12738  df-fz 12886  df-fzo 13027  df-fl 13155  df-seq 13363  df-exp 13423  df-hash 13684  df-cj 14451  df-re 14452  df-im 14453  df-sqrt 14587  df-abs 14588  df-clim 14838  df-rlim 14839  df-sum 15036  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-submnd 17947  df-mulg 18157  df-cntz 18379  df-cmn 18830  df-psmet 20455  df-xmet 20456  df-met 20457  df-bl 20458  df-mopn 20459  df-cnfld 20464  df-top 21420  df-topon 21437  df-topsp 21459  df-bases 21472  df-cld 21545  df-cn 21753  df-cnp 21754  df-cmp 21913  df-tx 22088  df-hmeo 22281  df-xms 22847  df-ms 22848  df-tms 22849 This theorem is referenced by:  stoweidlem58  42211
 Copyright terms: Public domain W3C validator