Step | Hyp | Ref
| Expression |
1 | | stoweidlem29.4 |
. . . . . 6
⊢ 𝐾 = (topGen‘ran
(,)) |
2 | | stoweidlem29.3 |
. . . . . 6
⊢ 𝑇 = ∪
𝐽 |
3 | | eqid 2610 |
. . . . . 6
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾) |
4 | | stoweidlem29.6 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
5 | 1, 2, 3, 4 | fcnre 38207 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
6 | | df-f 5808 |
. . . . 5
⊢ (𝐹:𝑇⟶ℝ ↔ (𝐹 Fn 𝑇 ∧ ran 𝐹 ⊆ ℝ)) |
7 | 5, 6 | sylib 207 |
. . . 4
⊢ (𝜑 → (𝐹 Fn 𝑇 ∧ ran 𝐹 ⊆ ℝ)) |
8 | 7 | simprd 478 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
9 | 7 | simpld 474 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑇) |
10 | | fnfun 5902 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑇 → Fun 𝐹) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → Fun 𝐹) |
13 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐹:𝑇⟶ℝ → dom 𝐹 = 𝑇) |
14 | 5, 13 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝑇) |
15 | 14 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 = dom 𝐹) |
16 | 15 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ 𝑇 ↔ 𝑠 ∈ dom 𝐹)) |
17 | 16 | biimpa 500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝑠 ∈ dom 𝐹) |
18 | | fvelrn 6260 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑠 ∈ dom 𝐹) → (𝐹‘𝑠) ∈ ran 𝐹) |
19 | 12, 17, 18 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (𝐹‘𝑠) ∈ ran 𝐹) |
20 | | stoweidlem29.1 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝐹 |
21 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑠 |
22 | 20, 21 | nffv 6110 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝐹‘𝑠) |
23 | 22 | nfeq2 2766 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑥 = (𝐹‘𝑠) |
24 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑠) → (𝑥 ≤ (𝐹‘𝑡) ↔ (𝐹‘𝑠) ≤ (𝐹‘𝑡))) |
25 | 23, 24 | ralbid 2966 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑠) → (∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡) ↔ ∀𝑡 ∈ 𝑇 (𝐹‘𝑠) ≤ (𝐹‘𝑡))) |
26 | 25 | rspcev 3282 |
. . . . . 6
⊢ (((𝐹‘𝑠) ∈ ran 𝐹 ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑠) ≤ (𝐹‘𝑡)) → ∃𝑥 ∈ ran 𝐹∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
27 | 19, 26 | sylan 487 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑇) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑠) ≤ (𝐹‘𝑡)) → ∃𝑥 ∈ ran 𝐹∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
28 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑠𝐹 |
29 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑠𝑇 |
30 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑡𝑇 |
31 | | stoweidlem29.5 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Comp) |
32 | | stoweidlem29.7 |
. . . . . 6
⊢ (𝜑 → 𝑇 ≠ ∅) |
33 | 28, 20, 29, 30, 2, 1, 31, 4, 32 | evth2f 38197 |
. . . . 5
⊢ (𝜑 → ∃𝑠 ∈ 𝑇 ∀𝑡 ∈ 𝑇 (𝐹‘𝑠) ≤ (𝐹‘𝑡)) |
34 | 27, 33 | r19.29a 3060 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ ran 𝐹∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
35 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑦(𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
36 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
37 | 9 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → 𝐹 Fn 𝑇) |
38 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑦 |
39 | 30, 38, 20 | fvelrnbf 38200 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝑇 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑡 ∈ 𝑇 (𝐹‘𝑡) = 𝑦)) |
40 | 37, 39 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑡 ∈ 𝑇 (𝐹‘𝑡) = 𝑦)) |
41 | 36, 40 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑡 ∈ 𝑇 (𝐹‘𝑡) = 𝑦) |
42 | | stoweidlem29.2 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝜑 |
43 | | nfra1 2925 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡) |
44 | 42, 43 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) |
45 | 20 | nfrn 5289 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡ran
𝐹 |
46 | 45 | nfcri 2745 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡 𝑦 ∈ ran 𝐹 |
47 | 44, 46 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑡((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) |
48 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑥 ≤ 𝑦 |
49 | | rspa 2914 |
. . . . . . . . . . . . 13
⊢
((∀𝑡 ∈
𝑇 𝑥 ≤ (𝐹‘𝑡) ∧ 𝑡 ∈ 𝑇) → 𝑥 ≤ (𝐹‘𝑡)) |
50 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑡) = 𝑦 → (𝑥 ≤ (𝐹‘𝑡) ↔ 𝑥 ≤ 𝑦)) |
51 | 49, 50 | syl5ibcom 234 |
. . . . . . . . . . . 12
⊢
((∀𝑡 ∈
𝑇 𝑥 ≤ (𝐹‘𝑡) ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) = 𝑦 → 𝑥 ≤ 𝑦)) |
52 | 51 | ex 449 |
. . . . . . . . . . 11
⊢
(∀𝑡 ∈
𝑇 𝑥 ≤ (𝐹‘𝑡) → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡) = 𝑦 → 𝑥 ≤ 𝑦))) |
53 | 52 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → (𝑡 ∈ 𝑇 → ((𝐹‘𝑡) = 𝑦 → 𝑥 ≤ 𝑦))) |
54 | 47, 48, 53 | rexlimd 3008 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → (∃𝑡 ∈ 𝑇 (𝐹‘𝑡) = 𝑦 → 𝑥 ≤ 𝑦)) |
55 | 41, 54 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) ∧ 𝑦 ∈ ran 𝐹) → 𝑥 ≤ 𝑦) |
56 | 55 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) → (𝑦 ∈ ran 𝐹 → 𝑥 ≤ 𝑦)) |
57 | 35, 56 | ralrimi 2940 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡)) → ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) |
58 | 57 | ex 449 |
. . . . 5
⊢ (𝜑 → (∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡) → ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦)) |
59 | 58 | reximdv 2999 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ ran 𝐹∀𝑡 ∈ 𝑇 𝑥 ≤ (𝐹‘𝑡) → ∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦)) |
60 | 34, 59 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) |
61 | | lbinfcl 10856 |
. . 3
⊢ ((ran
𝐹 ⊆ ℝ ∧
∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) → inf(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
62 | 8, 60, 61 | syl2anc 691 |
. 2
⊢ (𝜑 → inf(ran 𝐹, ℝ, < ) ∈ ran 𝐹) |
63 | 8, 62 | sseldd 3569 |
. 2
⊢ (𝜑 → inf(ran 𝐹, ℝ, < ) ∈
ℝ) |
64 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ran 𝐹 ⊆ ℝ) |
65 | 60 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) |
66 | | dffn3 5967 |
. . . . . . 7
⊢ (𝐹 Fn 𝑇 ↔ 𝐹:𝑇⟶ran 𝐹) |
67 | 9, 66 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑇⟶ran 𝐹) |
68 | 67 | fnvinran 38196 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ran 𝐹) |
69 | | lbinfle 10857 |
. . . . 5
⊢ ((ran
𝐹 ⊆ ℝ ∧
∃𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ∧ (𝐹‘𝑡) ∈ ran 𝐹) → inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡)) |
70 | 64, 65, 68, 69 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡)) |
71 | 70 | ex 449 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 → inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡))) |
72 | 42, 71 | ralrimi 2940 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡)) |
73 | 62, 63, 72 | 3jca 1235 |
1
⊢ (𝜑 → (inf(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ∧ inf(ran 𝐹, ℝ, < ) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑡))) |