Step | Hyp | Ref
| Expression |
1 | | stoweidlem57.2 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑈 |
2 | | stoweidlem57.3 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝜑 |
3 | | stoweidlem57.1 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝐷 |
4 | 3 | nfcri 2886 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡 𝑠 ∈ 𝐷 |
5 | 2, 4 | nfan 1906 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝜑 ∧ 𝑠 ∈ 𝐷) |
6 | | stoweidlem57.6 |
. . . . . . . . . 10
⊢ 𝐾 = (topGen‘ran
(,)) |
7 | | stoweidlem57.10 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ Comp) |
8 | 7 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝐽 ∈ Comp) |
9 | | stoweidlem57.7 |
. . . . . . . . . 10
⊢ 𝑇 = ∪
𝐽 |
10 | | stoweidlem57.8 |
. . . . . . . . . 10
⊢ 𝐶 = (𝐽 Cn 𝐾) |
11 | | stoweidlem57.11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
12 | 11 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝐴 ⊆ 𝐶) |
13 | | stoweidlem57.12 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
14 | 13 | 3adant1r 1178 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐷) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
15 | | stoweidlem57.13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
16 | 15 | 3adant1r 1178 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐷) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
17 | | stoweidlem57.14 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴) |
18 | 17 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐷) ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴) |
19 | | stoweidlem57.15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
20 | 19 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐷) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
21 | | stoweidlem57.9 |
. . . . . . . . . . . 12
⊢ 𝑈 = (𝑇 ∖ 𝐵) |
22 | | stoweidlem57.16 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽)) |
23 | | cmptop 22146 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
24 | 9 | iscld 21778 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ Top → (𝐵 ∈ (Clsd‘𝐽) ↔ (𝐵 ⊆ 𝑇 ∧ (𝑇 ∖ 𝐵) ∈ 𝐽))) |
25 | 7, 23, 24 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ∈ (Clsd‘𝐽) ↔ (𝐵 ⊆ 𝑇 ∧ (𝑇 ∖ 𝐵) ∈ 𝐽))) |
26 | 22, 25 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 ⊆ 𝑇 ∧ (𝑇 ∖ 𝐵) ∈ 𝐽)) |
27 | 26 | simprd 499 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑇 ∖ 𝐵) ∈ 𝐽) |
28 | 21, 27 | eqeltrid 2837 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
29 | 28 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑈 ∈ 𝐽) |
30 | | stoweidlem57.17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ (Clsd‘𝐽)) |
31 | 9 | cldss 21780 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (Clsd‘𝐽) → 𝐷 ⊆ 𝑇) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ⊆ 𝑇) |
33 | 32 | sselda 3877 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ 𝑇) |
34 | | stoweidlem57.18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅) |
35 | | disjr 4339 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∩ 𝐷) = ∅ ↔ ∀𝑠 ∈ 𝐷 ¬ 𝑠 ∈ 𝐵) |
36 | 34, 35 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑠 ∈ 𝐷 ¬ 𝑠 ∈ 𝐵) |
37 | 36 | r19.21bi 3121 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → ¬ 𝑠 ∈ 𝐵) |
38 | 33, 37 | eldifd 3854 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ (𝑇 ∖ 𝐵)) |
39 | 38, 21 | eleqtrrdi 2844 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ 𝑈) |
40 | 1, 5, 6, 8, 9, 10,
12, 14, 16, 18, 20, 29, 39 | stoweidlem56 43159 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → ∃𝑤 ∈ 𝐽 ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) |
41 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) → 𝑤 ∈ 𝐽) |
42 | | simprll 779 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) → 𝑠 ∈ 𝑤) |
43 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) → ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))) |
44 | | stoweidlem57.5 |
. . . . . . . . . . . . 13
⊢ 𝑉 = {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
45 | 44 | rabeq2i 3389 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑉 ↔ (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) |
46 | 41, 43, 45 | sylanbrc 586 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) → 𝑤 ∈ 𝑉) |
47 | 41, 42, 46 | jca32 519 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) → (𝑤 ∈ 𝐽 ∧ (𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉))) |
48 | 47 | reximi2 3158 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
𝐽 ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))) → ∃𝑤 ∈ 𝐽 (𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉)) |
49 | | rexex 3153 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
𝐽 (𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉)) |
50 | 40, 48, 49 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉)) |
51 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝑠 |
52 | | nfrab1 3287 |
. . . . . . . . . 10
⊢
Ⅎ𝑤{𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
53 | 44, 52 | nfcxfr 2897 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝑉 |
54 | 51, 53 | elunif 42117 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ 𝑉
↔ ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉)) |
55 | 50, 54 | sylibr 237 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ ∪ 𝑉) |
56 | 55 | ex 416 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ 𝐷 → 𝑠 ∈ ∪ 𝑉)) |
57 | 56 | ssrdv 3883 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑉) |
58 | | cmpcld 22153 |
. . . . . . . 8
⊢ ((𝐽 ∈ Comp ∧ 𝐷 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐷) ∈ Comp) |
59 | 7, 30, 58 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐽 ↾t 𝐷) ∈ Comp) |
60 | 7, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Top) |
61 | 9 | cmpsub 22151 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐷 ⊆ 𝑇) → ((𝐽 ↾t 𝐷) ∈ Comp ↔ ∀𝑘 ∈ 𝒫 𝐽(𝐷 ⊆ ∪ 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢))) |
62 | 60, 32, 61 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ((𝐽 ↾t 𝐷) ∈ Comp ↔ ∀𝑘 ∈ 𝒫 𝐽(𝐷 ⊆ ∪ 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢))) |
63 | 59, 62 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ 𝒫 𝐽(𝐷 ⊆ ∪ 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢)) |
64 | | ssrab2 3969 |
. . . . . . . 8
⊢ {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} ⊆ 𝐽 |
65 | 44, 64 | eqsstri 3911 |
. . . . . . 7
⊢ 𝑉 ⊆ 𝐽 |
66 | 44, 7 | rabexd 5201 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ V) |
67 | | elpwg 4491 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 ⊆ 𝐽)) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 ⊆ 𝐽)) |
69 | 65, 68 | mpbiri 261 |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ 𝒫 𝐽) |
70 | | unieq 4807 |
. . . . . . . . 9
⊢ (𝑘 = 𝑉 → ∪ 𝑘 = ∪
𝑉) |
71 | 70 | sseq2d 3909 |
. . . . . . . 8
⊢ (𝑘 = 𝑉 → (𝐷 ⊆ ∪ 𝑘 ↔ 𝐷 ⊆ ∪ 𝑉)) |
72 | | pweq 4504 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑉 → 𝒫 𝑘 = 𝒫 𝑉) |
73 | 72 | ineq1d 4102 |
. . . . . . . . 9
⊢ (𝑘 = 𝑉 → (𝒫 𝑘 ∩ Fin) = (𝒫 𝑉 ∩ Fin)) |
74 | 73 | rexeqdv 3317 |
. . . . . . . 8
⊢ (𝑘 = 𝑉 → (∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢 ↔ ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢)) |
75 | 71, 74 | imbi12d 348 |
. . . . . . 7
⊢ (𝑘 = 𝑉 → ((𝐷 ⊆ ∪ 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢) ↔ (𝐷 ⊆ ∪ 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢))) |
76 | 75 | rspccva 3525 |
. . . . . 6
⊢
((∀𝑘 ∈
𝒫 𝐽(𝐷 ⊆ ∪ 𝑘
→ ∃𝑢 ∈
(𝒫 𝑘 ∩
Fin)𝐷 ⊆ ∪ 𝑢)
∧ 𝑉 ∈ 𝒫
𝐽) → (𝐷 ⊆ ∪ 𝑉
→ ∃𝑢 ∈
(𝒫 𝑉 ∩
Fin)𝐷 ⊆ ∪ 𝑢)) |
77 | 63, 69, 76 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐷 ⊆ ∪ 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢)) |
78 | 57, 77 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢) |
79 | | elinel1 4085 |
. . . . . . . . 9
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → 𝑢 ∈ 𝒫 𝑉) |
80 | | elpwi 4497 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ 𝒫 𝑉 → 𝑢 ⊆ 𝑉) |
81 | 80 | ssdifssd 4033 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝒫 𝑉 → (𝑢 ∖ {∅}) ⊆ 𝑉) |
82 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
83 | | difexg 5195 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ V → (𝑢 ∖ {∅}) ∈
V) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑢 ∖ {∅}) ∈
V |
85 | 84 | elpw 4492 |
. . . . . . . . . 10
⊢ ((𝑢 ∖ {∅}) ∈
𝒫 𝑉 ↔ (𝑢 ∖ {∅}) ⊆
𝑉) |
86 | 81, 85 | sylibr 237 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝒫 𝑉 → (𝑢 ∖ {∅}) ∈ 𝒫 𝑉) |
87 | 79, 86 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈
𝒫 𝑉) |
88 | | elinel2 4086 |
. . . . . . . . 9
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → 𝑢 ∈ Fin) |
89 | | diffi 8827 |
. . . . . . . . 9
⊢ (𝑢 ∈ Fin → (𝑢 ∖ {∅}) ∈
Fin) |
90 | 88, 89 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈
Fin) |
91 | 87, 90 | elind 4084 |
. . . . . . 7
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈
(𝒫 𝑉 ∩
Fin)) |
92 | 91 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 ⊆ ∪ 𝑢) → (𝑢 ∖ {∅}) ∈ (𝒫 𝑉 ∩ Fin)) |
93 | | unidif0 5226 |
. . . . . . . . 9
⊢ ∪ (𝑢
∖ {∅}) = ∪ 𝑢 |
94 | 93 | sseq2i 3906 |
. . . . . . . 8
⊢ (𝐷 ⊆ ∪ (𝑢
∖ {∅}) ↔ 𝐷
⊆ ∪ 𝑢) |
95 | 94 | biimpri 231 |
. . . . . . 7
⊢ (𝐷 ⊆ ∪ 𝑢
→ 𝐷 ⊆ ∪ (𝑢
∖ {∅})) |
96 | 95 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 ⊆ ∪ 𝑢) → 𝐷 ⊆ ∪ (𝑢 ∖
{∅})) |
97 | | eldifsni 4678 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝑢 ∖ {∅}) → 𝑤 ≠ ∅) |
98 | 97 | rgen 3063 |
. . . . . . 7
⊢
∀𝑤 ∈
(𝑢 ∖ {∅})𝑤 ≠ ∅ |
99 | 98 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 ⊆ ∪ 𝑢) → ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅) |
100 | | unieq 4807 |
. . . . . . . . 9
⊢ (𝑟 = (𝑢 ∖ {∅}) → ∪ 𝑟 =
∪ (𝑢 ∖ {∅})) |
101 | 100 | sseq2d 3909 |
. . . . . . . 8
⊢ (𝑟 = (𝑢 ∖ {∅}) → (𝐷 ⊆ ∪ 𝑟 ↔ 𝐷 ⊆ ∪ (𝑢 ∖
{∅}))) |
102 | | raleq 3310 |
. . . . . . . 8
⊢ (𝑟 = (𝑢 ∖ {∅}) → (∀𝑤 ∈ 𝑟 𝑤 ≠ ∅ ↔ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)) |
103 | 101, 102 | anbi12d 634 |
. . . . . . 7
⊢ (𝑟 = (𝑢 ∖ {∅}) → ((𝐷 ⊆ ∪ 𝑟
∧ ∀𝑤 ∈
𝑟 𝑤 ≠ ∅) ↔ (𝐷 ⊆ ∪ (𝑢 ∖ {∅}) ∧
∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠
∅))) |
104 | 103 | rspcev 3526 |
. . . . . 6
⊢ (((𝑢 ∖ {∅}) ∈
(𝒫 𝑉 ∩ Fin)
∧ (𝐷 ⊆ ∪ (𝑢
∖ {∅}) ∧ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)) → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
105 | 92, 96, 99, 104 | syl12anc 836 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 ⊆ ∪ 𝑢) → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
106 | 105 | rexlimdv3a 3196 |
. . . 4
⊢ (𝜑 → (∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢 → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅))) |
107 | 78, 106 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
108 | | nfv 1921 |
. . . . . 6
⊢
Ⅎℎ𝜑 |
109 | | nfcv 2899 |
. . . . . . . . . . . 12
⊢
Ⅎℎℝ+ |
110 | | nfre1 3216 |
. . . . . . . . . . . 12
⊢
Ⅎℎ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
111 | 109, 110 | nfralw 3138 |
. . . . . . . . . . 11
⊢
Ⅎℎ∀𝑒 ∈ ℝ+
∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
112 | | nfcv 2899 |
. . . . . . . . . . 11
⊢
Ⅎℎ𝐽 |
113 | 111, 112 | nfrabw 3288 |
. . . . . . . . . 10
⊢
Ⅎℎ{𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
114 | 44, 113 | nfcxfr 2897 |
. . . . . . . . 9
⊢
Ⅎℎ𝑉 |
115 | 114 | nfpw 4509 |
. . . . . . . 8
⊢
Ⅎℎ𝒫 𝑉 |
116 | | nfcv 2899 |
. . . . . . . 8
⊢
ℲℎFin |
117 | 115, 116 | nfin 4107 |
. . . . . . 7
⊢
Ⅎℎ(𝒫 𝑉 ∩ Fin) |
118 | 117 | nfcri 2886 |
. . . . . 6
⊢
Ⅎℎ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) |
119 | | nfv 1921 |
. . . . . 6
⊢
Ⅎℎ(𝐷 ⊆ ∪ 𝑟
∧ ∀𝑤 ∈
𝑟 𝑤 ≠ ∅) |
120 | 108, 118,
119 | nf3an 1908 |
. . . . 5
⊢
Ⅎℎ(𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
121 | | nfcv 2899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡ℝ+ |
122 | | nfcv 2899 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡𝐴 |
123 | | nfra1 3131 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
124 | | nfra1 3131 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 |
125 | | nfra1 3131 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡) |
126 | 123, 124,
125 | nf3an 1908 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
127 | 122, 126 | nfrex 3219 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
128 | 121, 127 | nfralw 3138 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
129 | | nfcv 2899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝐽 |
130 | 128, 129 | nfrabw 3288 |
. . . . . . . . . 10
⊢
Ⅎ𝑡{𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
131 | 44, 130 | nfcxfr 2897 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝑉 |
132 | 131 | nfpw 4509 |
. . . . . . . 8
⊢
Ⅎ𝑡𝒫 𝑉 |
133 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑡Fin |
134 | 132, 133 | nfin 4107 |
. . . . . . 7
⊢
Ⅎ𝑡(𝒫 𝑉 ∩ Fin) |
135 | 134 | nfcri 2886 |
. . . . . 6
⊢
Ⅎ𝑡 𝑟 ∈ (𝒫 𝑉 ∩ Fin) |
136 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑡∪ 𝑟 |
137 | 3, 136 | nfss 3869 |
. . . . . . 7
⊢
Ⅎ𝑡 𝐷 ⊆ ∪ 𝑟 |
138 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑡∀𝑤 ∈ 𝑟 𝑤 ≠ ∅ |
139 | 137, 138 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑡(𝐷 ⊆ ∪ 𝑟
∧ ∀𝑤 ∈
𝑟 𝑤 ≠ ∅) |
140 | 2, 135, 139 | nf3an 1908 |
. . . . 5
⊢
Ⅎ𝑡(𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
141 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑤𝜑 |
142 | 53 | nfpw 4509 |
. . . . . . . 8
⊢
Ⅎ𝑤𝒫 𝑉 |
143 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑤Fin |
144 | 142, 143 | nfin 4107 |
. . . . . . 7
⊢
Ⅎ𝑤(𝒫 𝑉 ∩ Fin) |
145 | 144 | nfcri 2886 |
. . . . . 6
⊢
Ⅎ𝑤 𝑟 ∈ (𝒫 𝑉 ∩ Fin) |
146 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑤 𝐷 ⊆ ∪ 𝑟 |
147 | | nfra1 3131 |
. . . . . . 7
⊢
Ⅎ𝑤∀𝑤 ∈ 𝑟 𝑤 ≠ ∅ |
148 | 146, 147 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑤(𝐷 ⊆ ∪ 𝑟
∧ ∀𝑤 ∈
𝑟 𝑤 ≠ ∅) |
149 | 141, 145,
148 | nf3an 1908 |
. . . . 5
⊢
Ⅎ𝑤(𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
150 | | stoweidlem57.4 |
. . . . 5
⊢ 𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
151 | | simp2 1138 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝑟 ∈ (𝒫 𝑉 ∩ Fin)) |
152 | | simp3l 1202 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝐷 ⊆ ∪ 𝑟) |
153 | | stoweidlem57.19 |
. . . . . 6
⊢ (𝜑 → 𝐷 ≠ ∅) |
154 | 153 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝐷 ≠ ∅) |
155 | | stoweidlem57.20 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
156 | 155 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝐸 ∈
ℝ+) |
157 | 26 | simpld 498 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ 𝑇) |
158 | 157 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝐵 ⊆ 𝑇) |
159 | 66 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝑉 ∈ V) |
160 | | retop 23514 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
161 | 6, 160 | eqeltri 2829 |
. . . . . . . 8
⊢ 𝐾 ∈ Top |
162 | | cnfex 42129 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V) |
163 | 60, 161, 162 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → (𝐽 Cn 𝐾) ∈ V) |
164 | 11, 10 | sseqtrdi 3927 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
165 | 163, 164 | ssexd 5192 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
166 | 165 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝐴 ∈ V) |
167 | 120, 140,
149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166 | stoweidlem39 43142 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
168 | 167 | rexlimdv3a 3196 |
. . 3
⊢ (𝜑 → (∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅) → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))))) |
169 | 107, 168 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
170 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑖(𝜑 ∧ 𝑚 ∈ ℕ) |
171 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑖 𝑣:(1...𝑚)⟶𝑉 |
172 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑖 𝐷 ⊆ ∪ ran 𝑣 |
173 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑖 𝑦:(1...𝑚)⟶𝑌 |
174 | | nfra1 3131 |
. . . . . . . . . 10
⊢
Ⅎ𝑖∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)) |
175 | 173, 174 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
176 | 175 | nfex 2326 |
. . . . . . . 8
⊢
Ⅎ𝑖∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
177 | 171, 172,
176 | nf3an 1908 |
. . . . . . 7
⊢
Ⅎ𝑖(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
178 | 170, 177 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑖((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
179 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑚 ∈ ℕ |
180 | 2, 179 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ 𝑚 ∈ ℕ) |
181 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝑣 |
182 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑡(1...𝑚) |
183 | 181, 182,
131 | nff 6500 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑣:(1...𝑚)⟶𝑉 |
184 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑡∪ ran 𝑣 |
185 | 3, 184 | nfss 3869 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝐷 ⊆ ∪ ran 𝑣 |
186 | | nfcv 2899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑦 |
187 | 123, 122 | nfrabw 3288 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
188 | 150, 187 | nfcxfr 2897 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑌 |
189 | 186, 182,
188 | nff 6500 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑦:(1...𝑚)⟶𝑌 |
190 | | nfra1 3131 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) |
191 | | nfra1 3131 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡) |
192 | 190, 191 | nfan 1906 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)) |
193 | 182, 192 | nfralw 3138 |
. . . . . . . . . 10
⊢
Ⅎ𝑡∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)) |
194 | 189, 193 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
195 | 194 | nfex 2326 |
. . . . . . . 8
⊢
Ⅎ𝑡∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
196 | 183, 185,
195 | nf3an 1908 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
197 | 180, 196 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑡((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
198 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑦(𝜑 ∧ 𝑚 ∈ ℕ) |
199 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑣:(1...𝑚)⟶𝑉 |
200 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝐷 ⊆ ∪ ran 𝑣 |
201 | | nfe1 2155 |
. . . . . . . 8
⊢
Ⅎ𝑦∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
202 | 199, 200,
201 | nf3an 1908 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
203 | 198, 202 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑦((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
204 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑤(𝜑 ∧ 𝑚 ∈ ℕ) |
205 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝑣 |
206 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑤(1...𝑚) |
207 | 205, 206,
53 | nff 6500 |
. . . . . . . 8
⊢
Ⅎ𝑤 𝑣:(1...𝑚)⟶𝑉 |
208 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑤 𝐷 ⊆ ∪ ran 𝑣 |
209 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑤∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
210 | 207, 208,
209 | nf3an 1908 |
. . . . . . 7
⊢
Ⅎ𝑤(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
211 | 204, 210 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑤((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
212 | | eqid 2738 |
. . . . . 6
⊢ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
213 | | eqid 2738 |
. . . . . 6
⊢ (𝑓 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}, 𝑔 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) = (𝑓 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}, 𝑔 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
214 | | eqid 2738 |
. . . . . 6
⊢ (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦‘𝑖)‘𝑡))) |
215 | | eqid 2738 |
. . . . . 6
⊢ (𝑡 ∈ 𝑇 ↦ (seq1( · , ((𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦‘𝑖)‘𝑡)))‘𝑡))‘𝑚)) = (𝑡 ∈ 𝑇 ↦ (seq1( · , ((𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦‘𝑖)‘𝑡)))‘𝑡))‘𝑚)) |
216 | | simp1ll 1237 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → 𝜑) |
217 | 216, 15 | syld3an1 1411 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
218 | 11 | sselda 3877 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ 𝐶) |
219 | 6, 9, 10, 218 | fcnre 42126 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
220 | 219 | ad4ant14 752 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
221 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → 𝑚 ∈ ℕ) |
222 | | simpr1 1195 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → 𝑣:(1...𝑚)⟶𝑉) |
223 | 9 | cldss 21780 |
. . . . . . . 8
⊢ (𝐵 ∈ (Clsd‘𝐽) → 𝐵 ⊆ 𝑇) |
224 | 22, 223 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝑇) |
225 | 224 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → 𝐵 ⊆ 𝑇) |
226 | | simpr2 1196 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → 𝐷 ⊆ ∪ ran
𝑣) |
227 | 32 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → 𝐷 ⊆ 𝑇) |
228 | | feq3 6487 |
. . . . . . . . . . . 12
⊢ (𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} → (𝑦:(1...𝑚)⟶𝑌 ↔ 𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)})) |
229 | 150, 228 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑦:(1...𝑚)⟶𝑌 ↔ 𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}) |
230 | 229 | biimpi 219 |
. . . . . . . . . 10
⊢ (𝑦:(1...𝑚)⟶𝑌 → 𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}) |
231 | 230 | anim1i 618 |
. . . . . . . . 9
⊢ ((𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) → (𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
232 | 231 | eximi 1841 |
. . . . . . . 8
⊢
(∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) → ∃𝑦(𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
233 | 232 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) → ∃𝑦(𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
234 | 233 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → ∃𝑦(𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
235 | 7 | uniexd 7486 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝐽
∈ V) |
236 | 9, 235 | eqeltrid 2837 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ V) |
237 | 236 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → 𝑇 ∈ V) |
238 | 155 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → 𝐸 ∈
ℝ+) |
239 | | stoweidlem57.21 |
. . . . . . 7
⊢ (𝜑 → 𝐸 < (1 / 3)) |
240 | 239 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → 𝐸 < (1 / 3)) |
241 | 178, 197,
203, 211, 9, 212, 213, 214, 215, 44, 217, 220, 221, 222, 225, 226, 227, 234, 237, 238, 240 | stoweidlem54 43157 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡))) |
242 | 241 | ex 416 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))) |
243 | 242 | exlimdv 1940 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))) |
244 | 243 | rexlimdva 3194 |
. 2
⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))) |
245 | 169, 244 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡))) |