| Step | Hyp | Ref
| Expression |
| 1 | | stoweidlem50.1 |
. . 3
⊢
Ⅎ𝑡𝑈 |
| 2 | | stoweidlem50.4 |
. . . 4
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
| 3 | | nfrab1 3457 |
. . . 4
⊢
Ⅎℎ{ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
| 4 | 2, 3 | nfcxfr 2903 |
. . 3
⊢
Ⅎℎ𝑄 |
| 5 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑞𝜑 |
| 6 | | stoweidlem50.2 |
. . 3
⊢
Ⅎ𝑡𝜑 |
| 7 | | stoweidlem50.3 |
. . 3
⊢ 𝐾 = (topGen‘ran
(,)) |
| 8 | | stoweidlem50.5 |
. . 3
⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
| 9 | | stoweidlem50.6 |
. . 3
⊢ 𝑇 = ∪
𝐽 |
| 10 | | stoweidlem50.8 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Comp) |
| 11 | | stoweidlem50.9 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| 12 | | stoweidlem50.7 |
. . . 4
⊢ 𝐶 = (𝐽 Cn 𝐾) |
| 13 | 11, 12 | sseqtrdi 4024 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
| 14 | | stoweidlem50.10 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 15 | | stoweidlem50.11 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 16 | | stoweidlem50.12 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
| 17 | | stoweidlem50.13 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
| 18 | | stoweidlem50.14 |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
| 19 | | stoweidlem50.15 |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
| 20 | 10 | uniexd 7762 |
. . . 4
⊢ (𝜑 → ∪ 𝐽
∈ V) |
| 21 | 9, 20 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑇 ∈ V) |
| 22 | 1, 4, 5, 6, 7, 2, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 21 | stoweidlem46 46061 |
. 2
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) |
| 23 | | dfin4 4278 |
. . . . . . . . . . 11
⊢ (𝑇 ∩ 𝑈) = (𝑇 ∖ (𝑇 ∖ 𝑈)) |
| 24 | | elssuni 4937 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ 𝐽 → 𝑈 ⊆ ∪ 𝐽) |
| 25 | 18, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ⊆ ∪ 𝐽) |
| 26 | 25, 9 | sseqtrrdi 4025 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ⊆ 𝑇) |
| 27 | | sseqin2 4223 |
. . . . . . . . . . . 12
⊢ (𝑈 ⊆ 𝑇 ↔ (𝑇 ∩ 𝑈) = 𝑈) |
| 28 | 26, 27 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ∩ 𝑈) = 𝑈) |
| 29 | 23, 28 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 ∖ (𝑇 ∖ 𝑈)) = 𝑈) |
| 30 | 29, 18 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∖ (𝑇 ∖ 𝑈)) ∈ 𝐽) |
| 31 | | cmptop 23403 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
| 32 | 10, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ Top) |
| 33 | | difssd 4137 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ 𝑇) |
| 34 | 9 | iscld2 23036 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ (𝑇 ∖ 𝑈) ⊆ 𝑇) → ((𝑇 ∖ 𝑈) ∈ (Clsd‘𝐽) ↔ (𝑇 ∖ (𝑇 ∖ 𝑈)) ∈ 𝐽)) |
| 35 | 32, 33, 34 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 ∖ 𝑈) ∈ (Clsd‘𝐽) ↔ (𝑇 ∖ (𝑇 ∖ 𝑈)) ∈ 𝐽)) |
| 36 | 30, 35 | mpbird 257 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∖ 𝑈) ∈ (Clsd‘𝐽)) |
| 37 | | cmpcld 23410 |
. . . . . . . 8
⊢ ((𝐽 ∈ Comp ∧ (𝑇 ∖ 𝑈) ∈ (Clsd‘𝐽)) → (𝐽 ↾t (𝑇 ∖ 𝑈)) ∈ Comp) |
| 38 | 10, 36, 37 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐽 ↾t (𝑇 ∖ 𝑈)) ∈ Comp) |
| 39 | 9 | cmpsub 23408 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝑇 ∖ 𝑈) ⊆ 𝑇) → ((𝐽 ↾t (𝑇 ∖ 𝑈)) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽((𝑇 ∖ 𝑈) ⊆ ∪ 𝑐 → ∃𝑢 ∈ (𝒫 𝑐 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢))) |
| 40 | 32, 33, 39 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝐽 ↾t (𝑇 ∖ 𝑈)) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽((𝑇 ∖ 𝑈) ⊆ ∪ 𝑐 → ∃𝑢 ∈ (𝒫 𝑐 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢))) |
| 41 | 38, 40 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ∀𝑐 ∈ 𝒫 𝐽((𝑇 ∖ 𝑈) ⊆ ∪ 𝑐 → ∃𝑢 ∈ (𝒫 𝑐 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |
| 42 | | ssrab2 4080 |
. . . . . . . 8
⊢ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ⊆ 𝐽 |
| 43 | 8, 42 | eqsstri 4030 |
. . . . . . 7
⊢ 𝑊 ⊆ 𝐽 |
| 44 | 8, 10 | rabexd 5340 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ V) |
| 45 | | elpwg 4603 |
. . . . . . . 8
⊢ (𝑊 ∈ V → (𝑊 ∈ 𝒫 𝐽 ↔ 𝑊 ⊆ 𝐽)) |
| 46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑊 ∈ 𝒫 𝐽 ↔ 𝑊 ⊆ 𝐽)) |
| 47 | 43, 46 | mpbiri 258 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝒫 𝐽) |
| 48 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝑐 = 𝑊 → ∪ 𝑐 = ∪
𝑊) |
| 49 | 48 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑐 = 𝑊 → ((𝑇 ∖ 𝑈) ⊆ ∪ 𝑐 ↔ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊)) |
| 50 | | pweq 4614 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑊 → 𝒫 𝑐 = 𝒫 𝑊) |
| 51 | 50 | ineq1d 4219 |
. . . . . . . . 9
⊢ (𝑐 = 𝑊 → (𝒫 𝑐 ∩ Fin) = (𝒫 𝑊 ∩ Fin)) |
| 52 | 51 | rexeqdv 3327 |
. . . . . . . 8
⊢ (𝑐 = 𝑊 → (∃𝑢 ∈ (𝒫 𝑐 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢 ↔ ∃𝑢 ∈ (𝒫 𝑊 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |
| 53 | 49, 52 | imbi12d 344 |
. . . . . . 7
⊢ (𝑐 = 𝑊 → (((𝑇 ∖ 𝑈) ⊆ ∪ 𝑐 → ∃𝑢 ∈ (𝒫 𝑐 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢) ↔ ((𝑇 ∖ 𝑈) ⊆ ∪ 𝑊 → ∃𝑢 ∈ (𝒫 𝑊 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢))) |
| 54 | 53 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑐 ∈
𝒫 𝐽((𝑇 ∖ 𝑈) ⊆ ∪ 𝑐 → ∃𝑢 ∈ (𝒫 𝑐 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢) ∧ 𝑊 ∈ 𝒫 𝐽) → ((𝑇 ∖ 𝑈) ⊆ ∪ 𝑊 → ∃𝑢 ∈ (𝒫 𝑊 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |
| 55 | 41, 47, 54 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝑇 ∖ 𝑈) ⊆ ∪ 𝑊 → ∃𝑢 ∈ (𝒫 𝑊 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |
| 56 | 55 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) → ∃𝑢 ∈ (𝒫 𝑊 ∩ Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢) |
| 57 | | df-rex 3071 |
. . . 4
⊢
(∃𝑢 ∈
(𝒫 𝑊 ∩
Fin)(𝑇 ∖ 𝑈) ⊆ ∪ 𝑢
↔ ∃𝑢(𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |
| 58 | 56, 57 | sylib 218 |
. . 3
⊢ ((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) → ∃𝑢(𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |
| 59 | | elinel2 4202 |
. . . . . . 7
⊢ (𝑢 ∈ (𝒫 𝑊 ∩ Fin) → 𝑢 ∈ Fin) |
| 60 | 59 | ad2antrl 728 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) ∧ (𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) → 𝑢 ∈ Fin) |
| 61 | | elinel1 4201 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝒫 𝑊 ∩ Fin) → 𝑢 ∈ 𝒫 𝑊) |
| 62 | 61 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) ∧ (𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) → 𝑢 ∈ 𝒫 𝑊) |
| 63 | 62 | elpwid 4609 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) ∧ (𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) → 𝑢 ⊆ 𝑊) |
| 64 | | simprr 773 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) ∧ (𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢) |
| 65 | 60, 63, 64 | 3jca 1129 |
. . . . 5
⊢ (((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) ∧ (𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) → (𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |
| 66 | 65 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) → ((𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢) → (𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢))) |
| 67 | 66 | eximdv 1917 |
. . 3
⊢ ((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) → (∃𝑢(𝑢 ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢) → ∃𝑢(𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢))) |
| 68 | 58, 67 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) → ∃𝑢(𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |
| 69 | 22, 68 | mpdan 687 |
1
⊢ (𝜑 → ∃𝑢(𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ (𝑇 ∖ 𝑈) ⊆ ∪ 𝑢)) |