Step | Hyp | Ref
| Expression |
1 | | stoweidlem29.4 |
. . . . . 6
⊢ 𝐾 = (topGen‘ran
(,)) |
2 | | stoweidlem29.3 |
. . . . . 6
⊢ 𝑇 = ∪
𝐽 |
3 | | eqid 2737 |
. . . . . 6
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾) |
4 | | stoweidlem29.6 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
5 | 1, 2, 3, 4 | fcnre 42241 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
6 | | df-f 6384 |
. . . . 5
⊢ (𝐹:𝑇⟶ℝ ↔ (𝐹 Fn 𝑇 ∧ ran 𝐹 ⊆ ℝ)) |
7 | 5, 6 | sylib 221 |
. . . 4
⊢ (𝜑 → (𝐹 Fn 𝑇 ∧ ran 𝐹 ⊆ ℝ)) |
8 | 7 | simprd 499 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
9 | 7 | simpld 498 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑇) |
10 | | fnfun 6479 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑇 → Fun 𝐹) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
12 | 11 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → Fun 𝐹) |
13 | 5 | fdmd 6556 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝑇) |
14 | 13 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 = dom 𝐹) |
15 | 14 | eleq2d 2823 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ 𝑇 ↔ 𝑠 ∈ dom 𝐹)) |
16 | 15 | biimpa 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝑠 ∈ dom 𝐹) |
17 | | fvelrn 6897 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑠 ∈ dom 𝐹) → (𝐹‘𝑠) ∈ ran 𝐹) |
18 | 12, 16, 17 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (𝐹‘𝑠) ∈ ran 𝐹) |
19 | | stoweidlem29.1 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝐹 |
20 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑠 |
21 | 19, 20 | nffv 6727 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝐹‘𝑠) |
22 | 21 | nfeq2 2921 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑥 = (𝐹‘𝑠) |
23 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑠) → (𝑥 ≤ (𝐹‘𝑡) ↔ (𝐹‘𝑠) ≤ (𝐹‘𝑡))) |
24 | 22, 23 | ralbid 3154 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑠) → (∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡) ↔ ∀𝑡 ∈ 𝑇 (𝐹‘𝑠) ≤ (𝐹‘𝑡))) |
25 | 24 | rspcev 3537 |
. . . . . 6
⊢ (((𝐹‘𝑠) ∈ ran 𝐹 ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑠) ≤ (𝐹‘𝑡)) → ∃𝑥 ∈ ran 𝐹∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
26 | 18, 25 | sylan 583 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑠) ≤ (𝐹‘𝑡)) → ∃𝑥 ∈ ran 𝐹∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
27 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑠𝐹 |
28 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑠𝑇 |
29 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑡𝑇 |
30 | | stoweidlem29.5 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Comp) |
31 | | stoweidlem29.7 |
. . . . . 6
⊢ (𝜑 → 𝑇 ≠ ∅) |
32 | 27, 19, 28, 29, 2, 1, 30, 4, 31 | evth2f 42231 |
. . . . 5
⊢ (𝜑 → ∃𝑠 ∈ 𝑇 ∀𝑡 ∈ 𝑇 (𝐹‘𝑠) ≤ (𝐹‘𝑡)) |
33 | 26, 32 | r19.29a 3208 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ ran 𝐹∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
34 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑦(𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
35 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
36 | 9 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → 𝐹 Fn 𝑇) |
37 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑦 |
38 | 29, 37, 19 | fvelrnbf 42234 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝑇 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑡 ∈ 𝑇 (𝐹‘𝑡) = 𝑦)) |
39 | 36, 38 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑡 ∈ 𝑇 (𝐹‘𝑡) = 𝑦)) |
40 | 35, 39 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑡 ∈ 𝑇 (𝐹‘𝑡) = 𝑦) |
41 | | stoweidlem29.2 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝜑 |
42 | | nfra1 3140 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡) |
43 | 41, 42 | nfan 1907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
44 | 19 | nfrn 5821 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡ran
𝐹 |
45 | 44 | nfcri 2891 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡 𝑦 ∈ ran 𝐹 |
46 | 43, 45 | nfan 1907 |
. . . . . . . . . 10
⊢
Ⅎ𝑡((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) |
47 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑥 ≤ 𝑦 |
48 | | rspa 3128 |
. . . . . . . . . . . . 13
⊢
((∀𝑡 ∈
𝑇 𝑥 ≤ (𝐹‘𝑡) ∧ 𝑡 ∈ 𝑇) → 𝑥 ≤ (𝐹‘𝑡)) |
49 | | breq2 5057 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑡) = 𝑦 → (𝑥 ≤ (𝐹‘𝑡) ↔ 𝑥 ≤ 𝑦)) |
50 | 48, 49 | syl5ibcom 248 |
. . . . . . . . . . . 12
⊢
((∀𝑡 ∈
𝑇 𝑥 ≤ (𝐹‘𝑡) ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) = 𝑦 → 𝑥 ≤ 𝑦)) |
51 | 50 | ex 416 |
. . . . . . . . . . 11
⊢
(∀𝑡 ∈
𝑇 𝑥 ≤ (𝐹‘𝑡) → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡) = 𝑦 → 𝑥 ≤ 𝑦))) |
52 | 51 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡) = 𝑦 → 𝑥 ≤ 𝑦))) |
53 | 46, 47, 52 | rexlimd 3236 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → (∃𝑡 ∈ 𝑇 (𝐹‘𝑡) = 𝑦 → 𝑥 ≤ 𝑦)) |
54 | 40, 53 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → 𝑥 ≤ 𝑦) |
55 | 54 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) → (𝑦 ∈ ran 𝐹 → 𝑥 ≤ 𝑦)) |
56 | 34, 55 | ralrimi 3137 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) → ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) |
57 | 56 | ex 416 |
. . . . 5
⊢ (𝜑 → (∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡) → ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦)) |
58 | 57 | reximdv 3192 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ ran 𝐹∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡) → ∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦)) |
59 | 33, 58 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) |
60 | | lbinfcl 11786 |
. . 3
⊢ ((ran
𝐹 ⊆ ℝ ∧
∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) → inf(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
61 | 8, 59, 60 | syl2anc 587 |
. 2
⊢ (𝜑 → inf(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
62 | 8, 61 | sseldd 3902 |
. 2
⊢ (𝜑 → inf(ran 𝐹, ℝ, < ) ∈
ℝ) |
63 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ran 𝐹 ⊆ ℝ) |
64 | 59 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) |
65 | | dffn3 6558 |
. . . . . . 7
⊢ (𝐹 Fn 𝑇 ↔ 𝐹:𝑇⟶ran 𝐹) |
66 | 9, 65 | sylib 221 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑇⟶ran 𝐹) |
67 | 66 | ffvelrnda 6904 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ran 𝐹) |
68 | | lbinfle 11787 |
. . . . 5
⊢ ((ran
𝐹 ⊆ ℝ ∧
∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ∧ (𝐹‘𝑡) ∈ ran 𝐹) → inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡)) |
69 | 63, 64, 67, 68 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡)) |
70 | 69 | ex 416 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 → inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡))) |
71 | 41, 70 | ralrimi 3137 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡)) |
72 | 61, 62, 71 | 3jca 1130 |
1
⊢ (𝜑 → (inf(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ∧ inf(ran 𝐹, ℝ, < ) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡))) |