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

Theorem stoweidlem57 38950
 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 2745 . . . . . . . . . . 11 𝑡 𝑠𝐷
52, 4nfan 1816 . . . . . . . . . 10 𝑡(𝜑𝑠𝐷)
6 stoweidlem57.6 . . . . . . . . . 10 𝐾 = (topGen‘ran (,))
7 stoweidlem57.10 . . . . . . . . . . 11 (𝜑𝐽 ∈ Comp)
87adantr 480 . . . . . . . . . 10 ((𝜑𝑠𝐷) → 𝐽 ∈ Comp)
9 stoweidlem57.7 . . . . . . . . . 10 𝑇 = 𝐽
10 stoweidlem57.8 . . . . . . . . . 10 𝐶 = (𝐽 Cn 𝐾)
11 stoweidlem57.11 . . . . . . . . . . 11 (𝜑𝐴𝐶)
1211adantr 480 . . . . . . . . . 10 ((𝜑𝑠𝐷) → 𝐴𝐶)
13 stoweidlem57.12 . . . . . . . . . . 11 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
14133adant1r 1311 . . . . . . . . . 10 (((𝜑𝑠𝐷) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
15 stoweidlem57.13 . . . . . . . . . . 11 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
16153adant1r 1311 . . . . . . . . . 10 (((𝜑𝑠𝐷) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
17 stoweidlem57.14 . . . . . . . . . . 11 ((𝜑𝑎 ∈ ℝ) → (𝑡𝑇𝑎) ∈ 𝐴)
1817adantlr 747 . . . . . . . . . 10 (((𝜑𝑠𝐷) ∧ 𝑎 ∈ ℝ) → (𝑡𝑇𝑎) ∈ 𝐴)
19 stoweidlem57.15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
2019adantlr 747 . . . . . . . . . 10 (((𝜑𝑠𝐷) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
21 stoweidlem57.9 . . . . . . . . . . . 12 𝑈 = (𝑇𝐵)
22 stoweidlem57.16 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (Clsd‘𝐽))
23 cmptop 21008 . . . . . . . . . . . . . . 15 (𝐽 ∈ Comp → 𝐽 ∈ Top)
249iscld 20641 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top → (𝐵 ∈ (Clsd‘𝐽) ↔ (𝐵𝑇 ∧ (𝑇𝐵) ∈ 𝐽)))
257, 23, 243syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 ∈ (Clsd‘𝐽) ↔ (𝐵𝑇 ∧ (𝑇𝐵) ∈ 𝐽)))
2622, 25mpbid 221 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝑇 ∧ (𝑇𝐵) ∈ 𝐽))
2726simprd 478 . . . . . . . . . . . 12 (𝜑 → (𝑇𝐵) ∈ 𝐽)
2821, 27syl5eqel 2692 . . . . . . . . . . 11 (𝜑𝑈𝐽)
2928adantr 480 . . . . . . . . . 10 ((𝜑𝑠𝐷) → 𝑈𝐽)
30 stoweidlem57.17 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ (Clsd‘𝐽))
319cldss 20643 . . . . . . . . . . . . . 14 (𝐷 ∈ (Clsd‘𝐽) → 𝐷𝑇)
3230, 31syl 17 . . . . . . . . . . . . 13 (𝜑𝐷𝑇)
3332sselda 3568 . . . . . . . . . . . 12 ((𝜑𝑠𝐷) → 𝑠𝑇)
34 stoweidlem57.18 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐷) = ∅)
35 disjr 3970 . . . . . . . . . . . . . 14 ((𝐵𝐷) = ∅ ↔ ∀𝑠𝐷 ¬ 𝑠𝐵)
3634, 35sylib 207 . . . . . . . . . . . . 13 (𝜑 → ∀𝑠𝐷 ¬ 𝑠𝐵)
3736r19.21bi 2916 . . . . . . . . . . . 12 ((𝜑𝑠𝐷) → ¬ 𝑠𝐵)
3833, 37eldifd 3551 . . . . . . . . . . 11 ((𝜑𝑠𝐷) → 𝑠 ∈ (𝑇𝐵))
3938, 21syl6eleqr 2699 . . . . . . . . . 10 ((𝜑𝑠𝐷) → 𝑠𝑈)
401, 5, 6, 8, 9, 10, 12, 14, 16, 18, 20, 29, 39stoweidlem56 38949 . . . . . . . . 9 ((𝜑𝑠𝐷) → ∃𝑤𝐽 ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))))
41 simpl 472 . . . . . . . . . . 11 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → 𝑤𝐽)
42 simprll 798 . . . . . . . . . . 11 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → 𝑠𝑤)
43 simprr 792 . . . . . . . . . . . 12 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))
44 stoweidlem57.5 . . . . . . . . . . . . 13 𝑉 = {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
4544rabeq2i 3170 . . . . . . . . . . . 12 (𝑤𝑉 ↔ (𝑤𝐽 ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))))
4641, 43, 45sylanbrc 695 . . . . . . . . . . 11 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → 𝑤𝑉)
4741, 42, 46jca32 556 . . . . . . . . . 10 ((𝑤𝐽 ∧ ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)))) → (𝑤𝐽 ∧ (𝑠𝑤𝑤𝑉)))
4847reximi2 2993 . . . . . . . . 9 (∃𝑤𝐽 ((𝑠𝑤𝑤𝑈) ∧ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))) → ∃𝑤𝐽 (𝑠𝑤𝑤𝑉))
49 rexex 2985 . . . . . . . . 9 (∃𝑤𝐽 (𝑠𝑤𝑤𝑉) → ∃𝑤(𝑠𝑤𝑤𝑉))
5040, 48, 493syl 18 . . . . . . . 8 ((𝜑𝑠𝐷) → ∃𝑤(𝑠𝑤𝑤𝑉))
51 nfcv 2751 . . . . . . . . 9 𝑤𝑠
52 nfrab1 3099 . . . . . . . . . 10 𝑤{𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
5344, 52nfcxfr 2749 . . . . . . . . 9 𝑤𝑉
5451, 53elunif 38198 . . . . . . . 8 (𝑠 𝑉 ↔ ∃𝑤(𝑠𝑤𝑤𝑉))
5550, 54sylibr 223 . . . . . . 7 ((𝜑𝑠𝐷) → 𝑠 𝑉)
5655ex 449 . . . . . 6 (𝜑 → (𝑠𝐷𝑠 𝑉))
5756ssrdv 3574 . . . . 5 (𝜑𝐷 𝑉)
58 cmpcld 21015 . . . . . . . 8 ((𝐽 ∈ Comp ∧ 𝐷 ∈ (Clsd‘𝐽)) → (𝐽t 𝐷) ∈ Comp)
597, 30, 58syl2anc 691 . . . . . . 7 (𝜑 → (𝐽t 𝐷) ∈ Comp)
607, 23syl 17 . . . . . . . 8 (𝜑𝐽 ∈ Top)
619cmpsub 21013 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐷𝑇) → ((𝐽t 𝐷) ∈ Comp ↔ ∀𝑘 ∈ 𝒫 𝐽(𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢)))
6260, 32, 61syl2anc 691 . . . . . . 7 (𝜑 → ((𝐽t 𝐷) ∈ Comp ↔ ∀𝑘 ∈ 𝒫 𝐽(𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢)))
6359, 62mpbid 221 . . . . . 6 (𝜑 → ∀𝑘 ∈ 𝒫 𝐽(𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢))
64 ssrab2 3650 . . . . . . . 8 {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))} ⊆ 𝐽
6544, 64eqsstri 3598 . . . . . . 7 𝑉𝐽
6644, 7rabexd 4741 . . . . . . . 8 (𝜑𝑉 ∈ V)
67 elpwg 4116 . . . . . . . 8 (𝑉 ∈ V → (𝑉 ∈ 𝒫 𝐽𝑉𝐽))
6866, 67syl 17 . . . . . . 7 (𝜑 → (𝑉 ∈ 𝒫 𝐽𝑉𝐽))
6965, 68mpbiri 247 . . . . . 6 (𝜑𝑉 ∈ 𝒫 𝐽)
70 unieq 4380 . . . . . . . . 9 (𝑘 = 𝑉 𝑘 = 𝑉)
7170sseq2d 3596 . . . . . . . 8 (𝑘 = 𝑉 → (𝐷 𝑘𝐷 𝑉))
72 pweq 4111 . . . . . . . . . 10 (𝑘 = 𝑉 → 𝒫 𝑘 = 𝒫 𝑉)
7372ineq1d 3775 . . . . . . . . 9 (𝑘 = 𝑉 → (𝒫 𝑘 ∩ Fin) = (𝒫 𝑉 ∩ Fin))
7473rexeqdv 3122 . . . . . . . 8 (𝑘 = 𝑉 → (∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢 ↔ ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢))
7571, 74imbi12d 333 . . . . . . 7 (𝑘 = 𝑉 → ((𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢) ↔ (𝐷 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢)))
7675rspccva 3281 . . . . . 6 ((∀𝑘 ∈ 𝒫 𝐽(𝐷 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 𝑢) ∧ 𝑉 ∈ 𝒫 𝐽) → (𝐷 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢))
7763, 69, 76syl2anc 691 . . . . 5 (𝜑 → (𝐷 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢))
7857, 77mpd 15 . . . 4 (𝜑 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢)
79 elinel1 3761 . . . . . . . . 9 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → 𝑢 ∈ 𝒫 𝑉)
80 elpwi 4117 . . . . . . . . . . 11 (𝑢 ∈ 𝒫 𝑉𝑢𝑉)
8180ssdifssd 3710 . . . . . . . . . 10 (𝑢 ∈ 𝒫 𝑉 → (𝑢 ∖ {∅}) ⊆ 𝑉)
82 vex 3176 . . . . . . . . . . . 12 𝑢 ∈ V
83 difexg 4735 . . . . . . . . . . . 12 (𝑢 ∈ V → (𝑢 ∖ {∅}) ∈ V)
8482, 83ax-mp 5 . . . . . . . . . . 11 (𝑢 ∖ {∅}) ∈ V
8584elpw 4114 . . . . . . . . . 10 ((𝑢 ∖ {∅}) ∈ 𝒫 𝑉 ↔ (𝑢 ∖ {∅}) ⊆ 𝑉)
8681, 85sylibr 223 . . . . . . . . 9 (𝑢 ∈ 𝒫 𝑉 → (𝑢 ∖ {∅}) ∈ 𝒫 𝑉)
8779, 86syl 17 . . . . . . . 8 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈ 𝒫 𝑉)
88 elinel2 3762 . . . . . . . . 9 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → 𝑢 ∈ Fin)
89 diffi 8077 . . . . . . . . 9 (𝑢 ∈ Fin → (𝑢 ∖ {∅}) ∈ Fin)
9088, 89syl 17 . . . . . . . 8 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈ Fin)
9187, 90elind 3760 . . . . . . 7 (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈ (𝒫 𝑉 ∩ Fin))
92913ad2ant2 1076 . . . . . 6 ((𝜑𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 𝑢) → (𝑢 ∖ {∅}) ∈ (𝒫 𝑉 ∩ Fin))
93 unidif0 4764 . . . . . . . . 9 (𝑢 ∖ {∅}) = 𝑢
9493sseq2i 3593 . . . . . . . 8 (𝐷 (𝑢 ∖ {∅}) ↔ 𝐷 𝑢)
9594biimpri 217 . . . . . . 7 (𝐷 𝑢𝐷 (𝑢 ∖ {∅}))
96953ad2ant3 1077 . . . . . 6 ((𝜑𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 𝑢) → 𝐷 (𝑢 ∖ {∅}))
97 eldifsni 4261 . . . . . . . 8 (𝑤 ∈ (𝑢 ∖ {∅}) → 𝑤 ≠ ∅)
9897rgen 2906 . . . . . . 7 𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅
9998a1i 11 . . . . . 6 ((𝜑𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 𝑢) → ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)
100 unieq 4380 . . . . . . . . 9 (𝑟 = (𝑢 ∖ {∅}) → 𝑟 = (𝑢 ∖ {∅}))
101100sseq2d 3596 . . . . . . . 8 (𝑟 = (𝑢 ∖ {∅}) → (𝐷 𝑟𝐷 (𝑢 ∖ {∅})))
102 raleq 3115 . . . . . . . 8 (𝑟 = (𝑢 ∖ {∅}) → (∀𝑤𝑟 𝑤 ≠ ∅ ↔ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅))
103101, 102anbi12d 743 . . . . . . 7 (𝑟 = (𝑢 ∖ {∅}) → ((𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅) ↔ (𝐷 (𝑢 ∖ {∅}) ∧ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)))
104103rspcev 3282 . . . . . 6 (((𝑢 ∖ {∅}) ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 (𝑢 ∖ {∅}) ∧ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)) → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
10592, 96, 99, 104syl12anc 1316 . . . . 5 ((𝜑𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 𝑢) → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
106105rexlimdv3a 3015 . . . 4 (𝜑 → (∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 𝑢 → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)))
10778, 106mpd 15 . . 3 (𝜑 → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
108 nfv 1830 . . . . . 6 𝜑
109 nfcv 2751 . . . . . . . . . . . 12 +
110 nfre1 2988 . . . . . . . . . . . 12 𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
111109, 110nfral 2929 . . . . . . . . . . 11 𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
112 nfcv 2751 . . . . . . . . . . 11 𝐽
113111, 112nfrab 3100 . . . . . . . . . 10 {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
11444, 113nfcxfr 2749 . . . . . . . . 9 𝑉
115114nfpw 4120 . . . . . . . 8 𝒫 𝑉
116 nfcv 2751 . . . . . . . 8 Fin
117115, 116nfin 3782 . . . . . . 7 (𝒫 𝑉 ∩ Fin)
118117nfcri 2745 . . . . . 6 𝑟 ∈ (𝒫 𝑉 ∩ Fin)
119 nfv 1830 . . . . . 6 (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)
120108, 118, 119nf3an 1819 . . . . 5 (𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
121 nfcv 2751 . . . . . . . . . . . 12 𝑡+
122 nfcv 2751 . . . . . . . . . . . . 13 𝑡𝐴
123 nfra1 2925 . . . . . . . . . . . . . 14 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
124 nfra1 2925 . . . . . . . . . . . . . 14 𝑡𝑡𝑤 (𝑡) < 𝑒
125 nfra1 2925 . . . . . . . . . . . . . 14 𝑡𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡)
126123, 124, 125nf3an 1819 . . . . . . . . . . . . 13 𝑡(∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
127122, 126nfrex 2990 . . . . . . . . . . . 12 𝑡𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
128121, 127nfral 2929 . . . . . . . . . . 11 𝑡𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))
129 nfcv 2751 . . . . . . . . . . 11 𝑡𝐽
130128, 129nfrab 3100 . . . . . . . . . 10 𝑡{𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
13144, 130nfcxfr 2749 . . . . . . . . 9 𝑡𝑉
132131nfpw 4120 . . . . . . . 8 𝑡𝒫 𝑉
133 nfcv 2751 . . . . . . . 8 𝑡Fin
134132, 133nfin 3782 . . . . . . 7 𝑡(𝒫 𝑉 ∩ Fin)
135134nfcri 2745 . . . . . 6 𝑡 𝑟 ∈ (𝒫 𝑉 ∩ Fin)
136 nfcv 2751 . . . . . . . 8 𝑡 𝑟
1373, 136nfss 3561 . . . . . . 7 𝑡 𝐷 𝑟
138 nfv 1830 . . . . . . 7 𝑡𝑤𝑟 𝑤 ≠ ∅
139137, 138nfan 1816 . . . . . 6 𝑡(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)
1402, 135, 139nf3an 1819 . . . . 5 𝑡(𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
141 nfv 1830 . . . . . 6 𝑤𝜑
14253nfpw 4120 . . . . . . . 8 𝑤𝒫 𝑉
143 nfcv 2751 . . . . . . . 8 𝑤Fin
144142, 143nfin 3782 . . . . . . 7 𝑤(𝒫 𝑉 ∩ Fin)
145144nfcri 2745 . . . . . 6 𝑤 𝑟 ∈ (𝒫 𝑉 ∩ Fin)
146 nfv 1830 . . . . . . 7 𝑤 𝐷 𝑟
147 nfra1 2925 . . . . . . 7 𝑤𝑤𝑟 𝑤 ≠ ∅
148146, 147nfan 1816 . . . . . 6 𝑤(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)
149141, 145, 148nf3an 1819 . . . . 5 𝑤(𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅))
150 stoweidlem57.4 . . . . 5 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
151 simp2 1055 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝑟 ∈ (𝒫 𝑉 ∩ Fin))
152 simp3l 1082 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐷 𝑟)
153 stoweidlem57.19 . . . . . 6 (𝜑𝐷 ≠ ∅)
1541533ad2ant1 1075 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐷 ≠ ∅)
155 stoweidlem57.20 . . . . . 6 (𝜑𝐸 ∈ ℝ+)
1561553ad2ant1 1075 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐸 ∈ ℝ+)
15726simpld 474 . . . . . 6 (𝜑𝐵𝑇)
1581573ad2ant1 1075 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐵𝑇)
159663ad2ant1 1075 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝑉 ∈ V)
160 retop 22375 . . . . . . . . 9 (topGen‘ran (,)) ∈ Top
1616, 160eqeltri 2684 . . . . . . . 8 𝐾 ∈ Top
162 cnfex 38210 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V)
16360, 161, 162sylancl 693 . . . . . . 7 (𝜑 → (𝐽 Cn 𝐾) ∈ V)
16411, 10syl6sseq 3614 . . . . . . 7 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
165163, 164ssexd 4733 . . . . . 6 (𝜑𝐴 ∈ V)
1661653ad2ant1 1075 . . . . 5 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → 𝐴 ∈ V)
167120, 140, 149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166stoweidlem39 38932 . . . 4 ((𝜑𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅)) → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
168167rexlimdv3a 3015 . . 3 (𝜑 → (∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 𝑟 ∧ ∀𝑤𝑟 𝑤 ≠ ∅) → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))))
169107, 168mpd 15 . 2 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
170 nfv 1830 . . . . . . 7 𝑖(𝜑𝑚 ∈ ℕ)
171 nfv 1830 . . . . . . . 8 𝑖 𝑣:(1...𝑚)⟶𝑉
172 nfv 1830 . . . . . . . 8 𝑖 𝐷 ran 𝑣
173 nfv 1830 . . . . . . . . . 10 𝑖 𝑦:(1...𝑚)⟶𝑌
174 nfra1 2925 . . . . . . . . . 10 𝑖𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))
175173, 174nfan 1816 . . . . . . . . 9 𝑖(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
176175nfex 2140 . . . . . . . 8 𝑖𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
177171, 172, 176nf3an 1819 . . . . . . 7 𝑖(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
178170, 177nfan 1816 . . . . . 6 𝑖((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
179 nfv 1830 . . . . . . . 8 𝑡 𝑚 ∈ ℕ
1802, 179nfan 1816 . . . . . . 7 𝑡(𝜑𝑚 ∈ ℕ)
181 nfcv 2751 . . . . . . . . 9 𝑡𝑣
182 nfcv 2751 . . . . . . . . 9 𝑡(1...𝑚)
183181, 182, 131nff 5954 . . . . . . . 8 𝑡 𝑣:(1...𝑚)⟶𝑉
184 nfcv 2751 . . . . . . . . 9 𝑡 ran 𝑣
1853, 184nfss 3561 . . . . . . . 8 𝑡 𝐷 ran 𝑣
186 nfcv 2751 . . . . . . . . . . 11 𝑡𝑦
187123, 122nfrab 3100 . . . . . . . . . . . 12 𝑡{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
188150, 187nfcxfr 2749 . . . . . . . . . . 11 𝑡𝑌
189186, 182, 188nff 5954 . . . . . . . . . 10 𝑡 𝑦:(1...𝑚)⟶𝑌
190 nfra1 2925 . . . . . . . . . . . 12 𝑡𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚)
191 nfra1 2925 . . . . . . . . . . . 12 𝑡𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)
192190, 191nfan 1816 . . . . . . . . . . 11 𝑡(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))
193182, 192nfral 2929 . . . . . . . . . 10 𝑡𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))
194189, 193nfan 1816 . . . . . . . . 9 𝑡(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
195194nfex 2140 . . . . . . . 8 𝑡𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
196183, 185, 195nf3an 1819 . . . . . . 7 𝑡(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
197180, 196nfan 1816 . . . . . 6 𝑡((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
198 nfv 1830 . . . . . . 7 𝑦(𝜑𝑚 ∈ ℕ)
199 nfv 1830 . . . . . . . 8 𝑦 𝑣:(1...𝑚)⟶𝑉
200 nfv 1830 . . . . . . . 8 𝑦 𝐷 ran 𝑣
201 nfe1 2014 . . . . . . . 8 𝑦𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
202199, 200, 201nf3an 1819 . . . . . . 7 𝑦(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
203198, 202nfan 1816 . . . . . 6 𝑦((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
204 nfv 1830 . . . . . . 7 𝑤(𝜑𝑚 ∈ ℕ)
205 nfcv 2751 . . . . . . . . 9 𝑤𝑣
206 nfcv 2751 . . . . . . . . 9 𝑤(1...𝑚)
207205, 206, 53nff 5954 . . . . . . . 8 𝑤 𝑣:(1...𝑚)⟶𝑉
208 nfv 1830 . . . . . . . 8 𝑤 𝐷 ran 𝑣
209 nfv 1830 . . . . . . . 8 𝑤𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))
210207, 208, 209nf3an 1819 . . . . . . 7 𝑤(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
211204, 210nfan 1816 . . . . . 6 𝑤((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))))
212 eqid 2610 . . . . . 6 {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
213 eqid 2610 . . . . . 6 (𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}, 𝑔 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡)))) = (𝑓 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}, 𝑔 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
214 eqid 2610 . . . . . 6 (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦𝑖)‘𝑡))) = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦𝑖)‘𝑡)))
215 eqid 2610 . . . . . 6 (𝑡𝑇 ↦ (seq1( · , ((𝑡𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦𝑖)‘𝑡)))‘𝑡))‘𝑚)) = (𝑡𝑇 ↦ (seq1( · , ((𝑡𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦𝑖)‘𝑡)))‘𝑡))‘𝑚))
216 simp1ll 1117 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) ∧ 𝑓𝐴𝑔𝐴) → 𝜑)
217216, 15syld3an1 1364 . . . . . 6 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
21811sselda 3568 . . . . . . . 8 ((𝜑𝑓𝐴) → 𝑓𝐶)
2196, 9, 10, 218fcnre 38207 . . . . . . 7 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
220219ad4ant14 1285 . . . . . 6 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) ∧ 𝑓𝐴) → 𝑓:𝑇⟶ℝ)
221 simplr 788 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝑚 ∈ ℕ)
222 simpr1 1060 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝑣:(1...𝑚)⟶𝑉)
2239cldss 20643 . . . . . . . 8 (𝐵 ∈ (Clsd‘𝐽) → 𝐵𝑇)
22422, 223syl 17 . . . . . . 7 (𝜑𝐵𝑇)
225224ad2antrr 758 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐵𝑇)
226 simpr2 1061 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐷 ran 𝑣)
22732ad2antrr 758 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐷𝑇)
228 feq3 5941 . . . . . . . . . . . 12 (𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} → (𝑦:(1...𝑚)⟶𝑌𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}))
229150, 228ax-mp 5 . . . . . . . . . . 11 (𝑦:(1...𝑚)⟶𝑌𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)})
230229biimpi 205 . . . . . . . . . 10 (𝑦:(1...𝑚)⟶𝑌𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)})
231230anim1i 590 . . . . . . . . 9 ((𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))) → (𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
232231eximi 1752 . . . . . . . 8 (∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))) → ∃𝑦(𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
2332323ad2ant3 1077 . . . . . . 7 ((𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))) → ∃𝑦(𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
234233adantl 481 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → ∃𝑦(𝑦:(1...𝑚)⟶{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))
235 uniexg 6853 . . . . . . . . 9 (𝐽 ∈ Comp → 𝐽 ∈ V)
2367, 235syl 17 . . . . . . . 8 (𝜑 𝐽 ∈ V)
2379, 236syl5eqel 2692 . . . . . . 7 (𝜑𝑇 ∈ V)
238237ad2antrr 758 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝑇 ∈ V)
239155ad2antrr 758 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → 𝐸 ∈ ℝ+)
240 stoweidlem57.21 . . . . . . 7 (𝜑𝐸 < (1 / 3))
241240ad2antrr 758 . . . . . 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 38947 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡))))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡)))
243242ex 449 . . . 4 ((𝜑𝑚 ∈ ℕ) → ((𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡))))
244243exlimdv 1848 . . 3 ((𝜑𝑚 ∈ ℕ) → (∃𝑣(𝑣:(1...𝑚)⟶𝑉𝐷 ran 𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑦𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦𝑖)‘𝑡)))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡))))
245244rexlimdva 3013 . 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 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643  ran crn 5039  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  Fincfn 7841  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  3c3 10948  ℝ+crp 11708  (,)cioo 12046  ...cfz 12197  seqcseq 12663   ↾t crest 15904  topGenctg 15921  Topctop 20517  Clsdccld 20630   Cn ccn 20838  Compccmp 20999 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-cn 20841  df-cnp 20842  df-cmp 21000  df-tx 21175  df-hmeo 21368  df-xms 21935  df-ms 21936  df-tms 21937 This theorem is referenced by:  stoweidlem58  38951
 Copyright terms: Public domain W3C validator