| Step | Hyp | Ref
| Expression |
| 1 | | stoweidlem57.2 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑈 |
| 2 | | stoweidlem57.3 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝜑 |
| 3 | | stoweidlem57.1 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝐷 |
| 4 | 3 | nfcri 2897 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡 𝑠 ∈ 𝐷 |
| 5 | 2, 4 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝜑 ∧ 𝑠 ∈ 𝐷) |
| 6 | | stoweidlem57.6 |
. . . . . . . . . 10
⊢ 𝐾 = (topGen‘ran
(,)) |
| 7 | | stoweidlem57.10 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ Comp) |
| 8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝐽 ∈ Comp) |
| 9 | | stoweidlem57.7 |
. . . . . . . . . 10
⊢ 𝑇 = ∪
𝐽 |
| 10 | | stoweidlem57.8 |
. . . . . . . . . 10
⊢ 𝐶 = (𝐽 Cn 𝐾) |
| 11 | | stoweidlem57.11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| 12 | 11 | adantr 480 |
. . . . . . . . . 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 23403 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
| 24 | 9 | iscld 23035 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ Top → (𝐵 ∈ (Clsd‘𝐽) ↔ (𝐵 ⊆ 𝑇 ∧ (𝑇 ∖ 𝐵) ∈ 𝐽))) |
| 25 | 7, 23, 24 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ∈ (Clsd‘𝐽) ↔ (𝐵 ⊆ 𝑇 ∧ (𝑇 ∖ 𝐵) ∈ 𝐽))) |
| 26 | 22, 25 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 ⊆ 𝑇 ∧ (𝑇 ∖ 𝐵) ∈ 𝐽)) |
| 27 | 26 | simprd 495 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑇 ∖ 𝐵) ∈ 𝐽) |
| 28 | 21, 27 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
| 29 | 28 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑈 ∈ 𝐽) |
| 30 | | stoweidlem57.17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ (Clsd‘𝐽)) |
| 31 | 9 | cldss 23037 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (Clsd‘𝐽) → 𝐷 ⊆ 𝑇) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ⊆ 𝑇) |
| 33 | 32 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ 𝑇) |
| 34 | | stoweidlem57.18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅) |
| 35 | | disjr 4451 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∩ 𝐷) = ∅ ↔ ∀𝑠 ∈ 𝐷 ¬ 𝑠 ∈ 𝐵) |
| 36 | 34, 35 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑠 ∈ 𝐷 ¬ 𝑠 ∈ 𝐵) |
| 37 | 36 | r19.21bi 3251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → ¬ 𝑠 ∈ 𝐵) |
| 38 | 33, 37 | eldifd 3962 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ (𝑇 ∖ 𝐵)) |
| 39 | 38, 21 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ 𝑈) |
| 40 | 1, 5, 6, 8, 9, 10,
12, 14, 16, 18, 20, 29, 39 | stoweidlem56 46071 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → ∃𝑤 ∈ 𝐽 ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) |
| 41 | | simpl 482 |
. . . . . . . . . . 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 | reqabi 3460 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑉 ↔ (𝑤 ∈ 𝐽 ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) |
| 46 | 41, 43, 45 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) → 𝑤 ∈ 𝑉) |
| 47 | 41, 42, 46 | jca32 515 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝐽 ∧ ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)))) → (𝑤 ∈ 𝐽 ∧ (𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉))) |
| 48 | 47 | reximi2 3079 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
𝐽 ((𝑠 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))) → ∃𝑤 ∈ 𝐽 (𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉)) |
| 49 | | rexex 3076 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
𝐽 (𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉)) |
| 50 | 40, 48, 49 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉)) |
| 51 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝑠 |
| 52 | | nfrab1 3457 |
. . . . . . . . . 10
⊢
Ⅎ𝑤{𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
| 53 | 44, 52 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝑉 |
| 54 | 51, 53 | elunif 45021 |
. . . . . . . 8
⊢ (𝑠 ∈ ∪ 𝑉
↔ ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑉)) |
| 55 | 50, 54 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐷) → 𝑠 ∈ ∪ 𝑉) |
| 56 | 55 | ex 412 |
. . . . . 6
⊢ (𝜑 → (𝑠 ∈ 𝐷 → 𝑠 ∈ ∪ 𝑉)) |
| 57 | 56 | ssrdv 3989 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑉) |
| 58 | | cmpcld 23410 |
. . . . . . . 8
⊢ ((𝐽 ∈ Comp ∧ 𝐷 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐷) ∈ Comp) |
| 59 | 7, 30, 58 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐽 ↾t 𝐷) ∈ Comp) |
| 60 | 7, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Top) |
| 61 | 9 | cmpsub 23408 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐷 ⊆ 𝑇) → ((𝐽 ↾t 𝐷) ∈ Comp ↔ ∀𝑘 ∈ 𝒫 𝐽(𝐷 ⊆ ∪ 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢))) |
| 62 | 60, 32, 61 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝐽 ↾t 𝐷) ∈ Comp ↔ ∀𝑘 ∈ 𝒫 𝐽(𝐷 ⊆ ∪ 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢))) |
| 63 | 59, 62 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ 𝒫 𝐽(𝐷 ⊆ ∪ 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢)) |
| 64 | | ssrab2 4080 |
. . . . . . . 8
⊢ {𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} ⊆ 𝐽 |
| 65 | 44, 64 | eqsstri 4030 |
. . . . . . 7
⊢ 𝑉 ⊆ 𝐽 |
| 66 | 44, 7 | rabexd 5340 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ V) |
| 67 | | elpwg 4603 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 ⊆ 𝐽)) |
| 68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑉 ∈ 𝒫 𝐽 ↔ 𝑉 ⊆ 𝐽)) |
| 69 | 65, 68 | mpbiri 258 |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ 𝒫 𝐽) |
| 70 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝑘 = 𝑉 → ∪ 𝑘 = ∪
𝑉) |
| 71 | 70 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑘 = 𝑉 → (𝐷 ⊆ ∪ 𝑘 ↔ 𝐷 ⊆ ∪ 𝑉)) |
| 72 | | pweq 4614 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑉 → 𝒫 𝑘 = 𝒫 𝑉) |
| 73 | 72 | ineq1d 4219 |
. . . . . . . . 9
⊢ (𝑘 = 𝑉 → (𝒫 𝑘 ∩ Fin) = (𝒫 𝑉 ∩ Fin)) |
| 74 | 73 | rexeqdv 3327 |
. . . . . . . 8
⊢ (𝑘 = 𝑉 → (∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢 ↔ ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢)) |
| 75 | 71, 74 | imbi12d 344 |
. . . . . . 7
⊢ (𝑘 = 𝑉 → ((𝐷 ⊆ ∪ 𝑘 → ∃𝑢 ∈ (𝒫 𝑘 ∩ Fin)𝐷 ⊆ ∪ 𝑢) ↔ (𝐷 ⊆ ∪ 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢))) |
| 76 | 75 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑘 ∈
𝒫 𝐽(𝐷 ⊆ ∪ 𝑘
→ ∃𝑢 ∈
(𝒫 𝑘 ∩
Fin)𝐷 ⊆ ∪ 𝑢)
∧ 𝑉 ∈ 𝒫
𝐽) → (𝐷 ⊆ ∪ 𝑉
→ ∃𝑢 ∈
(𝒫 𝑉 ∩
Fin)𝐷 ⊆ ∪ 𝑢)) |
| 77 | 63, 69, 76 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐷 ⊆ ∪ 𝑉 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢)) |
| 78 | 57, 77 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢) |
| 79 | | elinel1 4201 |
. . . . . . . . 9
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → 𝑢 ∈ 𝒫 𝑉) |
| 80 | | elpwi 4607 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ 𝒫 𝑉 → 𝑢 ⊆ 𝑉) |
| 81 | 80 | ssdifssd 4147 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝒫 𝑉 → (𝑢 ∖ {∅}) ⊆ 𝑉) |
| 82 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
| 83 | | difexg 5329 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ V → (𝑢 ∖ {∅}) ∈
V) |
| 84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑢 ∖ {∅}) ∈
V |
| 85 | 84 | elpw 4604 |
. . . . . . . . . 10
⊢ ((𝑢 ∖ {∅}) ∈
𝒫 𝑉 ↔ (𝑢 ∖ {∅}) ⊆
𝑉) |
| 86 | 81, 85 | sylibr 234 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝒫 𝑉 → (𝑢 ∖ {∅}) ∈ 𝒫 𝑉) |
| 87 | 79, 86 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈
𝒫 𝑉) |
| 88 | | elinel2 4202 |
. . . . . . . . 9
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → 𝑢 ∈ Fin) |
| 89 | | diffi 9215 |
. . . . . . . . 9
⊢ (𝑢 ∈ Fin → (𝑢 ∖ {∅}) ∈
Fin) |
| 90 | 88, 89 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈
Fin) |
| 91 | 87, 90 | elind 4200 |
. . . . . . 7
⊢ (𝑢 ∈ (𝒫 𝑉 ∩ Fin) → (𝑢 ∖ {∅}) ∈
(𝒫 𝑉 ∩
Fin)) |
| 92 | 91 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 ⊆ ∪ 𝑢) → (𝑢 ∖ {∅}) ∈ (𝒫 𝑉 ∩ Fin)) |
| 93 | | unidif0 5360 |
. . . . . . . . 9
⊢ ∪ (𝑢
∖ {∅}) = ∪ 𝑢 |
| 94 | 93 | sseq2i 4013 |
. . . . . . . 8
⊢ (𝐷 ⊆ ∪ (𝑢
∖ {∅}) ↔ 𝐷
⊆ ∪ 𝑢) |
| 95 | 94 | biimpri 228 |
. . . . . . 7
⊢ (𝐷 ⊆ ∪ 𝑢
→ 𝐷 ⊆ ∪ (𝑢
∖ {∅})) |
| 96 | 95 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 ⊆ ∪ 𝑢) → 𝐷 ⊆ ∪ (𝑢 ∖
{∅})) |
| 97 | | eldifsni 4790 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝑢 ∖ {∅}) → 𝑤 ≠ ∅) |
| 98 | 97 | rgen 3063 |
. . . . . . 7
⊢
∀𝑤 ∈
(𝑢 ∖ {∅})𝑤 ≠ ∅ |
| 99 | 98 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 ⊆ ∪ 𝑢) → ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅) |
| 100 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝑟 = (𝑢 ∖ {∅}) → ∪ 𝑟 =
∪ (𝑢 ∖ {∅})) |
| 101 | 100 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑟 = (𝑢 ∖ {∅}) → (𝐷 ⊆ ∪ 𝑟 ↔ 𝐷 ⊆ ∪ (𝑢 ∖
{∅}))) |
| 102 | | raleq 3323 |
. . . . . . . 8
⊢ (𝑟 = (𝑢 ∖ {∅}) → (∀𝑤 ∈ 𝑟 𝑤 ≠ ∅ ↔ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)) |
| 103 | 101, 102 | anbi12d 632 |
. . . . . . 7
⊢ (𝑟 = (𝑢 ∖ {∅}) → ((𝐷 ⊆ ∪ 𝑟
∧ ∀𝑤 ∈
𝑟 𝑤 ≠ ∅) ↔ (𝐷 ⊆ ∪ (𝑢 ∖ {∅}) ∧
∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠
∅))) |
| 104 | 103 | rspcev 3622 |
. . . . . 6
⊢ (((𝑢 ∖ {∅}) ∈
(𝒫 𝑉 ∩ Fin)
∧ (𝐷 ⊆ ∪ (𝑢
∖ {∅}) ∧ ∀𝑤 ∈ (𝑢 ∖ {∅})𝑤 ≠ ∅)) → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
| 105 | 92, 96, 99, 104 | syl12anc 837 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (𝒫 𝑉 ∩ Fin) ∧ 𝐷 ⊆ ∪ 𝑢) → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
| 106 | 105 | rexlimdv3a 3159 |
. . . 4
⊢ (𝜑 → (∃𝑢 ∈ (𝒫 𝑉 ∩ Fin)𝐷 ⊆ ∪ 𝑢 → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅))) |
| 107 | 78, 106 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
| 108 | | nfv 1914 |
. . . . . 6
⊢
Ⅎℎ𝜑 |
| 109 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎℎℝ+ |
| 110 | | nfre1 3285 |
. . . . . . . . . . . 12
⊢
Ⅎℎ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
| 111 | 109, 110 | nfralw 3311 |
. . . . . . . . . . 11
⊢
Ⅎℎ∀𝑒 ∈ ℝ+
∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
| 112 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎℎ𝐽 |
| 113 | 111, 112 | nfrabw 3475 |
. . . . . . . . . 10
⊢
Ⅎℎ{𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
| 114 | 44, 113 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎℎ𝑉 |
| 115 | 114 | nfpw 4619 |
. . . . . . . 8
⊢
Ⅎℎ𝒫 𝑉 |
| 116 | | nfcv 2905 |
. . . . . . . 8
⊢
ℲℎFin |
| 117 | 115, 116 | nfin 4224 |
. . . . . . 7
⊢
Ⅎℎ(𝒫 𝑉 ∩ Fin) |
| 118 | 117 | nfcri 2897 |
. . . . . 6
⊢
Ⅎℎ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) |
| 119 | | nfv 1914 |
. . . . . 6
⊢
Ⅎℎ(𝐷 ⊆ ∪ 𝑟
∧ ∀𝑤 ∈
𝑟 𝑤 ≠ ∅) |
| 120 | 108, 118,
119 | nf3an 1901 |
. . . . 5
⊢
Ⅎℎ(𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
| 121 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡ℝ+ |
| 122 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡𝐴 |
| 123 | | nfra1 3284 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) |
| 124 | | nfra1 3284 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 |
| 125 | | nfra1 3284 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡) |
| 126 | 123, 124,
125 | nf3an 1901 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
| 127 | 122, 126 | nfrexw 3313 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
| 128 | 121, 127 | nfralw 3311 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡)) |
| 129 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝐽 |
| 130 | 128, 129 | nfrabw 3475 |
. . . . . . . . . 10
⊢
Ⅎ𝑡{𝑤 ∈ 𝐽 ∣ ∀𝑒 ∈ ℝ+ ∃ℎ ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑤 (ℎ‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (ℎ‘𝑡))} |
| 131 | 44, 130 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝑉 |
| 132 | 131 | nfpw 4619 |
. . . . . . . 8
⊢
Ⅎ𝑡𝒫 𝑉 |
| 133 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑡Fin |
| 134 | 132, 133 | nfin 4224 |
. . . . . . 7
⊢
Ⅎ𝑡(𝒫 𝑉 ∩ Fin) |
| 135 | 134 | nfcri 2897 |
. . . . . 6
⊢
Ⅎ𝑡 𝑟 ∈ (𝒫 𝑉 ∩ Fin) |
| 136 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑡∪ 𝑟 |
| 137 | 3, 136 | nfss 3976 |
. . . . . . 7
⊢
Ⅎ𝑡 𝐷 ⊆ ∪ 𝑟 |
| 138 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑡∀𝑤 ∈ 𝑟 𝑤 ≠ ∅ |
| 139 | 137, 138 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑡(𝐷 ⊆ ∪ 𝑟
∧ ∀𝑤 ∈
𝑟 𝑤 ≠ ∅) |
| 140 | 2, 135, 139 | nf3an 1901 |
. . . . 5
⊢
Ⅎ𝑡(𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) |
| 141 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑤𝜑 |
| 142 | 53 | nfpw 4619 |
. . . . . . . 8
⊢
Ⅎ𝑤𝒫 𝑉 |
| 143 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑤Fin |
| 144 | 142, 143 | nfin 4224 |
. . . . . . 7
⊢
Ⅎ𝑤(𝒫 𝑉 ∩ Fin) |
| 145 | 144 | nfcri 2897 |
. . . . . 6
⊢
Ⅎ𝑤 𝑟 ∈ (𝒫 𝑉 ∩ Fin) |
| 146 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑤 𝐷 ⊆ ∪ 𝑟 |
| 147 | | nfra1 3284 |
. . . . . . 7
⊢
Ⅎ𝑤∀𝑤 ∈ 𝑟 𝑤 ≠ ∅ |
| 148 | 146, 147 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑤(𝐷 ⊆ ∪ 𝑟
∧ ∀𝑤 ∈
𝑟 𝑤 ≠ ∅) |
| 149 | 141, 145,
148 | nf3an 1901 |
. . . . 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 494 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ 𝑇) |
| 158 | 157 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝐵 ⊆ 𝑇) |
| 159 | 66 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝑉 ∈ V) |
| 160 | | retop 24782 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
| 161 | 6, 160 | eqeltri 2837 |
. . . . . . . 8
⊢ 𝐾 ∈ Top |
| 162 | | cnfex 45033 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V) |
| 163 | 60, 161, 162 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝐽 Cn 𝐾) ∈ V) |
| 164 | 11, 10 | sseqtrdi 4024 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
| 165 | 163, 164 | ssexd 5324 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
| 166 | 165 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → 𝐴 ∈ V) |
| 167 | 120, 140,
149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166 | stoweidlem39 46054 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 𝑉 ∩ Fin) ∧ (𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅)) → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
| 168 | 167 | rexlimdv3a 3159 |
. . 3
⊢ (𝜑 → (∃𝑟 ∈ (𝒫 𝑉 ∩ Fin)(𝐷 ⊆ ∪ 𝑟 ∧ ∀𝑤 ∈ 𝑟 𝑤 ≠ ∅) → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))))) |
| 169 | 107, 168 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
| 170 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑖(𝜑 ∧ 𝑚 ∈ ℕ) |
| 171 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑖 𝑣:(1...𝑚)⟶𝑉 |
| 172 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑖 𝐷 ⊆ ∪ ran 𝑣 |
| 173 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑖 𝑦:(1...𝑚)⟶𝑌 |
| 174 | | nfra1 3284 |
. . . . . . . . . 10
⊢
Ⅎ𝑖∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)) |
| 175 | 173, 174 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
| 176 | 175 | nfex 2324 |
. . . . . . . 8
⊢
Ⅎ𝑖∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
| 177 | 171, 172,
176 | nf3an 1901 |
. . . . . . 7
⊢
Ⅎ𝑖(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
| 178 | 170, 177 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑖((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
| 179 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑚 ∈ ℕ |
| 180 | 2, 179 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ 𝑚 ∈ ℕ) |
| 181 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝑣 |
| 182 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑡(1...𝑚) |
| 183 | 181, 182,
131 | nff 6732 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑣:(1...𝑚)⟶𝑉 |
| 184 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑡∪ ran 𝑣 |
| 185 | 3, 184 | nfss 3976 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝐷 ⊆ ∪ ran 𝑣 |
| 186 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑦 |
| 187 | 123, 122 | nfrabw 3475 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
| 188 | 150, 187 | nfcxfr 2903 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡𝑌 |
| 189 | 186, 182,
188 | nff 6732 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑦:(1...𝑚)⟶𝑌 |
| 190 | | nfra1 3284 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) |
| 191 | | nfra1 3284 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡) |
| 192 | 190, 191 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)) |
| 193 | 182, 192 | nfralw 3311 |
. . . . . . . . . 10
⊢
Ⅎ𝑡∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)) |
| 194 | 189, 193 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
| 195 | 194 | nfex 2324 |
. . . . . . . 8
⊢
Ⅎ𝑡∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
| 196 | 183, 185,
195 | nf3an 1901 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
| 197 | 180, 196 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑡((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
| 198 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑦(𝜑 ∧ 𝑚 ∈ ℕ) |
| 199 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑣:(1...𝑚)⟶𝑉 |
| 200 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝐷 ⊆ ∪ ran 𝑣 |
| 201 | | nfe1 2150 |
. . . . . . . 8
⊢
Ⅎ𝑦∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
| 202 | 199, 200,
201 | nf3an 1901 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
| 203 | 198, 202 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑦((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
| 204 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑤(𝜑 ∧ 𝑚 ∈ ℕ) |
| 205 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝑣 |
| 206 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑤(1...𝑚) |
| 207 | 205, 206,
53 | nff 6732 |
. . . . . . . 8
⊢
Ⅎ𝑤 𝑣:(1...𝑚)⟶𝑉 |
| 208 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑤 𝐷 ⊆ ∪ ran 𝑣 |
| 209 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑤∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) |
| 210 | 207, 208,
209 | nf3an 1901 |
. . . . . . 7
⊢
Ⅎ𝑤(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
| 211 | 204, 210 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑤((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) |
| 212 | | eqid 2737 |
. . . . . 6
⊢ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} |
| 213 | | eqid 2737 |
. . . . . 6
⊢ (𝑓 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}, 𝑔 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) = (𝑓 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}, 𝑔 ∈ {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡)))) |
| 214 | | eqid 2737 |
. . . . . 6
⊢ (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦‘𝑖)‘𝑡))) |
| 215 | | eqid 2737 |
. . . . . 6
⊢ (𝑡 ∈ 𝑇 ↦ (seq1( · , ((𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦‘𝑖)‘𝑡)))‘𝑡))‘𝑚)) = (𝑡 ∈ 𝑇 ↦ (seq1( · , ((𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑚) ↦ ((𝑦‘𝑖)‘𝑡)))‘𝑡))‘𝑚)) |
| 216 | | simp1ll 1237 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → 𝜑) |
| 217 | 216, 15 | syld3an1 1412 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 218 | 11 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ 𝐶) |
| 219 | 6, 9, 10, 218 | fcnre 45030 |
. . . . . . 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 23037 |
. . . . . . . 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 6718 |
. . . . . . . . . . . 12
⊢ (𝑌 = {ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} → (𝑦:(1...𝑚)⟶𝑌 ↔ 𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)})) |
| 229 | 150, 228 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑦:(1...𝑚)⟶𝑌 ↔ 𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}) |
| 230 | 229 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑦:(1...𝑚)⟶𝑌 → 𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)}) |
| 231 | 230 | anim1i 615 |
. . . . . . . . 9
⊢ ((𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))) → (𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
| 232 | 231 | eximi 1835 |
. . . . . . . 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 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → ∃𝑦(𝑦:(1...𝑚)⟶{ℎ ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)} ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) |
| 235 | 7 | uniexd 7762 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝐽
∈ V) |
| 236 | 9, 235 | eqeltrid 2845 |
. . . . . . 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 46069 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡))))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡))) |
| 242 | 241 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))) |
| 243 | 242 | exlimdv 1933 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))) |
| 244 | 243 | rexlimdva 3155 |
. 2
⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑉 ∧ 𝐷 ⊆ ∪ ran
𝑣 ∧ ∃𝑦(𝑦:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣‘𝑖)((𝑦‘𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ 𝐵 (1 − (𝐸 / 𝑚)) < ((𝑦‘𝑖)‘𝑡)))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡)))) |
| 245 | 169, 244 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝐷 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ 𝐵 (1 − 𝐸) < (𝑥‘𝑡))) |