| Step | Hyp | Ref
| Expression |
| 1 | | stoweidlem46.3 |
. . . . . . . 8
⊢
Ⅎ𝑞𝜑 |
| 2 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑞 𝑠 ∈ (𝑇 ∖ 𝑈) |
| 3 | 1, 2 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑞(𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) |
| 4 | | stoweidlem46.4 |
. . . . . . . 8
⊢
Ⅎ𝑡𝜑 |
| 5 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑇 |
| 6 | | stoweidlem46.1 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑈 |
| 7 | 5, 6 | nfdif 4129 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑇 ∖ 𝑈) |
| 8 | 7 | nfel2 2924 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑠 ∈ (𝑇 ∖ 𝑈) |
| 9 | 4, 8 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) |
| 10 | | stoweidlem46.2 |
. . . . . . 7
⊢
Ⅎℎ𝑄 |
| 11 | | stoweidlem46.5 |
. . . . . . 7
⊢ 𝐾 = (topGen‘ran
(,)) |
| 12 | | stoweidlem46.6 |
. . . . . . 7
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
| 13 | | stoweidlem46.8 |
. . . . . . 7
⊢ 𝑇 = ∪
𝐽 |
| 14 | | stoweidlem46.9 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Comp) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝐽 ∈ Comp) |
| 16 | | stoweidlem46.10 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
| 17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
| 18 | | stoweidlem46.11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 19 | 18 | 3adant1r 1178 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 20 | | stoweidlem46.12 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 21 | 20 | 3adant1r 1178 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 22 | | stoweidlem46.13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
| 23 | 22 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
| 24 | | stoweidlem46.14 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
| 25 | 24 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
| 26 | | stoweidlem46.15 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝑈 ∈ 𝐽) |
| 28 | | stoweidlem46.16 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
| 29 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝑍 ∈ 𝑈) |
| 30 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝑠 ∈ (𝑇 ∖ 𝑈)) |
| 31 | 3, 9, 10, 11, 12, 13, 15, 17, 19, 21, 23, 25, 27, 29, 30 | stoweidlem43 46058 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → ∃ℎ(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑠))) |
| 32 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑔(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑠)) |
| 33 | 10 | nfel2 2924 |
. . . . . . . 8
⊢
Ⅎℎ 𝑔 ∈ 𝑄 |
| 34 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎℎ0 < (𝑔‘𝑠) |
| 35 | 33, 34 | nfan 1899 |
. . . . . . 7
⊢
Ⅎℎ(𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠)) |
| 36 | | eleq1 2829 |
. . . . . . . 8
⊢ (ℎ = 𝑔 → (ℎ ∈ 𝑄 ↔ 𝑔 ∈ 𝑄)) |
| 37 | | fveq1 6905 |
. . . . . . . . 9
⊢ (ℎ = 𝑔 → (ℎ‘𝑠) = (𝑔‘𝑠)) |
| 38 | 37 | breq2d 5155 |
. . . . . . . 8
⊢ (ℎ = 𝑔 → (0 < (ℎ‘𝑠) ↔ 0 < (𝑔‘𝑠))) |
| 39 | 36, 38 | anbi12d 632 |
. . . . . . 7
⊢ (ℎ = 𝑔 → ((ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑠)) ↔ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠)))) |
| 40 | 32, 35, 39 | cbvexv1 2344 |
. . . . . 6
⊢
(∃ℎ(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑠)) ↔ ∃𝑔(𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) |
| 41 | 31, 40 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → ∃𝑔(𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) |
| 42 | | stoweidlem46.17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ V) |
| 43 | | rabexg 5337 |
. . . . . . . 8
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V) |
| 44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V) |
| 45 | 44 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V) |
| 46 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝑇 ∖ 𝑈) → 𝑠 ∈ 𝑇) |
| 47 | 46 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 𝑠 ∈ 𝑇) |
| 48 | | simprr 773 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 0 < (𝑔‘𝑠)) |
| 49 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → (𝑔‘𝑡) = (𝑔‘𝑠)) |
| 50 | 49 | breq2d 5155 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → (0 < (𝑔‘𝑡) ↔ 0 < (𝑔‘𝑠))) |
| 51 | 50 | elrab 3692 |
. . . . . . 7
⊢ (𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ↔ (𝑠 ∈ 𝑇 ∧ 0 < (𝑔‘𝑠))) |
| 52 | 47, 48, 51 | sylanbrc 583 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)}) |
| 53 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 𝜑) |
| 54 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
| 55 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝑔 ∈ 𝑄) |
| 56 | 55, 12 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝑔 ∈ {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}) |
| 57 | | fveq1 6905 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝑔 → (ℎ‘𝑍) = (𝑔‘𝑍)) |
| 58 | 57 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝑔 → ((ℎ‘𝑍) = 0 ↔ (𝑔‘𝑍) = 0)) |
| 59 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = 𝑔 → (ℎ‘𝑡) = (𝑔‘𝑡)) |
| 60 | 59 | breq2d 5155 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = 𝑔 → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (𝑔‘𝑡))) |
| 61 | 59 | breq1d 5153 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = 𝑔 → ((ℎ‘𝑡) ≤ 1 ↔ (𝑔‘𝑡) ≤ 1)) |
| 62 | 60, 61 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝑔 → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1))) |
| 63 | 62 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝑔 → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1))) |
| 64 | 58, 63 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝑔 → (((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)) ↔ ((𝑔‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1)))) |
| 65 | 64 | elrab 3692 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} ↔ (𝑔 ∈ 𝐴 ∧ ((𝑔‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1)))) |
| 66 | 56, 65 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → (𝑔 ∈ 𝐴 ∧ ((𝑔‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1)))) |
| 67 | 66 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝑔 ∈ 𝐴) |
| 68 | 54, 67 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝑔 ∈ (𝐽 Cn 𝐾)) |
| 69 | 68 | ad2ant2r 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 𝑔 ∈ (𝐽 Cn 𝐾)) |
| 70 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑡0 |
| 71 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑔 |
| 72 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡 𝑔 ∈ (𝐽 Cn 𝐾) |
| 73 | 4, 72 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝜑 ∧ 𝑔 ∈ (𝐽 Cn 𝐾)) |
| 74 | | eqid 2737 |
. . . . . . . . . 10
⊢ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} |
| 75 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 76 | 75 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn 𝐾)) → 0 ∈
ℝ*) |
| 77 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn 𝐾)) → 𝑔 ∈ (𝐽 Cn 𝐾)) |
| 78 | 70, 71, 73, 11, 13, 74, 76, 77 | rfcnpre1 45024 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn 𝐾)) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝐽) |
| 79 | 53, 69, 78 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝐽) |
| 80 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)}) |
| 81 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎℎ{𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} |
| 82 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎℎ𝑔 |
| 83 | 59 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑔 → (0 < (ℎ‘𝑡) ↔ 0 < (𝑔‘𝑡))) |
| 84 | 83 | rabbidv 3444 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑔 → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)}) |
| 85 | 84 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑔 → ({𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)})) |
| 86 | 81, 82, 10, 85 | rspcegf 45028 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ 𝑄 ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)}) → ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
| 87 | 55, 80, 86 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
| 88 | 87 | ad2ant2r 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
| 89 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 90 | 89 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → (∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 91 | 90 | elrab 3692 |
. . . . . . . 8
⊢ ({𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ({𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝐽 ∧ ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
| 92 | 79, 88, 91 | sylanbrc 583 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
| 93 | | stoweidlem46.7 |
. . . . . . 7
⊢ 𝑊 = {𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
| 94 | 92, 93 | eleqtrrdi 2852 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊) |
| 95 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑤{𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} |
| 96 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} |
| 97 | | nfrab1 3457 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤{𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
| 98 | 93, 97 | nfcxfr 2903 |
. . . . . . . . . 10
⊢
Ⅎ𝑤𝑊 |
| 99 | 98 | nfel2 2924 |
. . . . . . . . 9
⊢
Ⅎ𝑤{𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊 |
| 100 | 96, 99 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊) |
| 101 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → (𝑠 ∈ 𝑤 ↔ 𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)})) |
| 102 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → (𝑤 ∈ 𝑊 ↔ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊)) |
| 103 | 101, 102 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → ((𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊) ↔ (𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊))) |
| 104 | 95, 100, 103 | spcegf 3592 |
. . . . . . 7
⊢ ({𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V → ((𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊))) |
| 105 | 104 | imp 406 |
. . . . . 6
⊢ (({𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V ∧ (𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊)) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊)) |
| 106 | 45, 52, 94, 105 | syl12anc 837 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊)) |
| 107 | 41, 106 | exlimddv 1935 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊)) |
| 108 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑤𝑠 |
| 109 | 108, 98 | elunif 45021 |
. . . 4
⊢ (𝑠 ∈ ∪ 𝑊
↔ ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊)) |
| 110 | 107, 109 | sylibr 234 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝑠 ∈ ∪ 𝑊) |
| 111 | 110 | ex 412 |
. 2
⊢ (𝜑 → (𝑠 ∈ (𝑇 ∖ 𝑈) → 𝑠 ∈ ∪ 𝑊)) |
| 112 | 111 | ssrdv 3989 |
1
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) |