Step | Hyp | Ref
| Expression |
1 | | stoweidlem46.3 |
. . . . . . . 8
⊢
Ⅎ𝑞𝜑 |
2 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑞 𝑠 ∈ (𝑇 ∖ 𝑈) |
3 | 1, 2 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑞(𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) |
4 | | stoweidlem46.4 |
. . . . . . . 8
⊢
Ⅎ𝑡𝜑 |
5 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑇 |
6 | | stoweidlem46.1 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑈 |
7 | 5, 6 | nfdif 4060 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑇 ∖ 𝑈) |
8 | 7 | nfel2 2925 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑠 ∈ (𝑇 ∖ 𝑈) |
9 | 4, 8 | nfan 1902 |
. . . . . . 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 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝐽 ∈ Comp) |
16 | | stoweidlem46.10 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
17 | 16 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
18 | | stoweidlem46.11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
19 | 18 | 3adant1r 1176 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
20 | | stoweidlem46.12 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
21 | 20 | 3adant1r 1176 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
22 | | stoweidlem46.13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
23 | 22 | adantlr 712 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
24 | | stoweidlem46.14 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
25 | 24 | adantlr 712 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡)) |
26 | | stoweidlem46.15 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
27 | 26 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝑈 ∈ 𝐽) |
28 | | stoweidlem46.16 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
29 | 28 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝑍 ∈ 𝑈) |
30 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝑠 ∈ (𝑇 ∖ 𝑈)) |
31 | 3, 9, 10, 11, 12, 13, 15, 17, 19, 21, 23, 25, 27, 29, 30 | stoweidlem43 43584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → ∃ℎ(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑠))) |
32 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑔(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑠)) |
33 | 10 | nfel2 2925 |
. . . . . . . 8
⊢
Ⅎℎ 𝑔 ∈ 𝑄 |
34 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎℎ0 < (𝑔‘𝑠) |
35 | 33, 34 | nfan 1902 |
. . . . . . 7
⊢
Ⅎℎ(𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠)) |
36 | | eleq1 2826 |
. . . . . . . 8
⊢ (ℎ = 𝑔 → (ℎ ∈ 𝑄 ↔ 𝑔 ∈ 𝑄)) |
37 | | fveq1 6773 |
. . . . . . . . 9
⊢ (ℎ = 𝑔 → (ℎ‘𝑠) = (𝑔‘𝑠)) |
38 | 37 | breq2d 5086 |
. . . . . . . 8
⊢ (ℎ = 𝑔 → (0 < (ℎ‘𝑠) ↔ 0 < (𝑔‘𝑠))) |
39 | 36, 38 | anbi12d 631 |
. . . . . . 7
⊢ (ℎ = 𝑔 → ((ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑠)) ↔ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠)))) |
40 | 32, 35, 39 | cbvexv1 2339 |
. . . . . 6
⊢
(∃ℎ(ℎ ∈ 𝑄 ∧ 0 < (ℎ‘𝑠)) ↔ ∃𝑔(𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) |
41 | 31, 40 | sylib 217 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → ∃𝑔(𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) |
42 | | stoweidlem46.17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ V) |
43 | | rabexg 5255 |
. . . . . . . 8
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V) |
44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V) |
45 | 44 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V) |
46 | | eldifi 4061 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝑇 ∖ 𝑈) → 𝑠 ∈ 𝑇) |
47 | 46 | ad2antlr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 𝑠 ∈ 𝑇) |
48 | | simprr 770 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 0 < (𝑔‘𝑠)) |
49 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → (𝑔‘𝑡) = (𝑔‘𝑠)) |
50 | 49 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → (0 < (𝑔‘𝑡) ↔ 0 < (𝑔‘𝑠))) |
51 | 50 | elrab 3624 |
. . . . . . 7
⊢ (𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ↔ (𝑠 ∈ 𝑇 ∧ 0 < (𝑔‘𝑠))) |
52 | 47, 48, 51 | sylanbrc 583 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)}) |
53 | | simpll 764 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 𝜑) |
54 | 16 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
55 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝑔 ∈ 𝑄) |
56 | 55, 12 | eleqtrdi 2849 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝑔 ∈ {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))}) |
57 | | fveq1 6773 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝑔 → (ℎ‘𝑍) = (𝑔‘𝑍)) |
58 | 57 | eqeq1d 2740 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝑔 → ((ℎ‘𝑍) = 0 ↔ (𝑔‘𝑍) = 0)) |
59 | | fveq1 6773 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = 𝑔 → (ℎ‘𝑡) = (𝑔‘𝑡)) |
60 | 59 | breq2d 5086 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = 𝑔 → (0 ≤ (ℎ‘𝑡) ↔ 0 ≤ (𝑔‘𝑡))) |
61 | 59 | breq1d 5084 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = 𝑔 → ((ℎ‘𝑡) ≤ 1 ↔ (𝑔‘𝑡) ≤ 1)) |
62 | 60, 61 | anbi12d 631 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝑔 → ((0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1))) |
63 | 62 | ralbidv 3112 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝑔 → (∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1))) |
64 | 58, 63 | anbi12d 631 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝑔 → (((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1)) ↔ ((𝑔‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1)))) |
65 | 64 | elrab 3624 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} ↔ (𝑔 ∈ 𝐴 ∧ ((𝑔‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1)))) |
66 | 56, 65 | sylib 217 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → (𝑔 ∈ 𝐴 ∧ ((𝑔‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑔‘𝑡) ∧ (𝑔‘𝑡) ≤ 1)))) |
67 | 66 | simpld 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝑔 ∈ 𝐴) |
68 | 54, 67 | sseldd 3922 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → 𝑔 ∈ (𝐽 Cn 𝐾)) |
69 | 68 | ad2ant2r 744 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → 𝑔 ∈ (𝐽 Cn 𝐾)) |
70 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑡0 |
71 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑔 |
72 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡 𝑔 ∈ (𝐽 Cn 𝐾) |
73 | 4, 72 | nfan 1902 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝜑 ∧ 𝑔 ∈ (𝐽 Cn 𝐾)) |
74 | | eqid 2738 |
. . . . . . . . . 10
⊢ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} |
75 | | 0xr 11022 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
76 | 75 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn 𝐾)) → 0 ∈
ℝ*) |
77 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn 𝐾)) → 𝑔 ∈ (𝐽 Cn 𝐾)) |
78 | 70, 71, 73, 11, 13, 74, 76, 77 | rfcnpre1 42562 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn 𝐾)) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝐽) |
79 | 53, 69, 78 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝐽) |
80 | | eqidd 2739 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)}) |
81 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎℎ{𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} |
82 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎℎ𝑔 |
83 | 59 | breq2d 5086 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑔 → (0 < (ℎ‘𝑡) ↔ 0 < (𝑔‘𝑡))) |
84 | 83 | rabbidv 3414 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑔 → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)}) |
85 | 84 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑔 → ({𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)})) |
86 | 81, 82, 10, 85 | rspcegf 42566 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ 𝑄 ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)}) → ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
87 | 55, 80, 86 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝑄) → ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
88 | 87 | ad2ant2r 744 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}) |
89 | | eqeq1 2742 |
. . . . . . . . . 10
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
90 | 89 | rexbidv 3226 |
. . . . . . . . 9
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → (∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ ∃ℎ ∈ 𝑄 {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)})) |
91 | 90 | elrab 3624 |
. . . . . . . 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 2850 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊) |
95 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑤{𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} |
96 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} |
97 | | nfrab1 3317 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤{𝑤 ∈ 𝐽 ∣ ∃ℎ ∈ 𝑄 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} |
98 | 93, 97 | nfcxfr 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑤𝑊 |
99 | 98 | nfel2 2925 |
. . . . . . . . 9
⊢
Ⅎ𝑤{𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊 |
100 | 96, 99 | nfan 1902 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊) |
101 | | eleq2 2827 |
. . . . . . . . 9
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → (𝑠 ∈ 𝑤 ↔ 𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)})) |
102 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → (𝑤 ∈ 𝑊 ↔ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊)) |
103 | 101, 102 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} → ((𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊) ↔ (𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊))) |
104 | 95, 100, 103 | spcegf 3531 |
. . . . . . 7
⊢ ({𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V → ((𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊))) |
105 | 104 | imp 407 |
. . . . . 6
⊢ (({𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ V ∧ (𝑠 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∧ {𝑡 ∈ 𝑇 ∣ 0 < (𝑔‘𝑡)} ∈ 𝑊)) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊)) |
106 | 45, 52, 94, 105 | syl12anc 834 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑔 ∈ 𝑄 ∧ 0 < (𝑔‘𝑠))) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊)) |
107 | 41, 106 | exlimddv 1938 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊)) |
108 | | nfcv 2907 |
. . . . 5
⊢
Ⅎ𝑤𝑠 |
109 | 108, 98 | elunif 42559 |
. . . 4
⊢ (𝑠 ∈ ∪ 𝑊
↔ ∃𝑤(𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊)) |
110 | 107, 109 | sylibr 233 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (𝑇 ∖ 𝑈)) → 𝑠 ∈ ∪ 𝑊) |
111 | 110 | ex 413 |
. 2
⊢ (𝜑 → (𝑠 ∈ (𝑇 ∖ 𝑈) → 𝑠 ∈ ∪ 𝑊)) |
112 | 111 | ssrdv 3927 |
1
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑊) |