Step | Hyp | Ref
| Expression |
1 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑠𝐹 |
2 | | rfcnnnub.1 |
. . . . . . . 8
⊢
Ⅎ𝑡𝐹 |
3 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑠𝑇 |
4 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑡𝑇 |
5 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑠𝜑 |
6 | | rfcnnnub.2 |
. . . . . . . 8
⊢
Ⅎ𝑡𝜑 |
7 | | rfcnnnub.5 |
. . . . . . . 8
⊢ 𝑇 = ∪
𝐽 |
8 | | rfcnnnub.3 |
. . . . . . . 8
⊢ 𝐾 = (topGen‘ran
(,)) |
9 | | rfcnnnub.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Comp) |
10 | | rfcnnnub.8 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝐶) |
11 | | rfcnnnub.7 |
. . . . . . . . 9
⊢ 𝐶 = (𝐽 Cn 𝐾) |
12 | 10, 11 | eleqtrdi 2849 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
13 | | rfcnnnub.6 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ≠ ∅) |
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 12,
13 | evthf 42551 |
. . . . . . 7
⊢ (𝜑 → ∃𝑠 ∈ 𝑇 ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) |
15 | | df-rex 3070 |
. . . . . . 7
⊢
(∃𝑠 ∈
𝑇 ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ↔ ∃𝑠(𝑠 ∈ 𝑇 ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠))) |
16 | 14, 15 | sylib 217 |
. . . . . 6
⊢ (𝜑 → ∃𝑠(𝑠 ∈ 𝑇 ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠))) |
17 | 8, 7, 11, 10 | fcnre 42549 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
18 | 17 | ffvelrnda 6953 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → (𝐹‘𝑠) ∈ ℝ) |
19 | 18 | ex 413 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ 𝑇 → (𝐹‘𝑠) ∈ ℝ)) |
20 | 19 | anim1d 611 |
. . . . . . 7
⊢ (𝜑 → ((𝑠 ∈ 𝑇 ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) → ((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)))) |
21 | 20 | eximdv 1920 |
. . . . . 6
⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝑇 ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) → ∃𝑠((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)))) |
22 | 16, 21 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑠((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠))) |
23 | 17 | ffvelrnda 6953 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) |
24 | 23 | ex 413 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ 𝑇 → (𝐹‘𝑡) ∈ ℝ)) |
25 | 6, 24 | ralrimi 3140 |
. . . . 5
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) |
26 | | 19.41v 1953 |
. . . . 5
⊢
(∃𝑠(((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ↔ (∃𝑠((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ)) |
27 | 22, 25, 26 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → ∃𝑠(((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ)) |
28 | | df-3an 1088 |
. . . . 5
⊢ (((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ↔ (((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ)) |
29 | 28 | exbii 1850 |
. . . 4
⊢
(∃𝑠((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ↔ ∃𝑠(((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ)) |
30 | 27, 29 | sylibr 233 |
. . 3
⊢ (𝜑 → ∃𝑠((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ)) |
31 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑡𝑠 |
32 | 2, 31 | nffv 6776 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝐹‘𝑠) |
33 | 32 | nfel1 2923 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝐹‘𝑠) ∈ ℝ |
34 | | nfra1 3143 |
. . . . . . . 8
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) |
35 | | nfra1 3143 |
. . . . . . . 8
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ |
36 | 33, 34, 35 | nf3an 1904 |
. . . . . . 7
⊢
Ⅎ𝑡((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) |
37 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑛 ∈ ℕ |
38 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑡
< |
39 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝑛 |
40 | 32, 38, 39 | nfbr 5120 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝐹‘𝑠) < 𝑛 |
41 | 37, 40 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛) |
42 | 36, 41 | nfan 1902 |
. . . . . 6
⊢
Ⅎ𝑡(((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) |
43 | | simpll3 1213 |
. . . . . . . . 9
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) |
44 | | simpr 485 |
. . . . . . . . 9
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
45 | | rsp 3130 |
. . . . . . . . 9
⊢
(∀𝑡 ∈
𝑇 (𝐹‘𝑡) ∈ ℝ → (𝑡 ∈ 𝑇 → (𝐹‘𝑡) ∈ ℝ)) |
46 | 43, 44, 45 | sylc 65 |
. . . . . . . 8
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) |
47 | | simpll1 1211 |
. . . . . . . 8
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑠) ∈ ℝ) |
48 | | simplrl 774 |
. . . . . . . . 9
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → 𝑛 ∈ ℕ) |
49 | 48 | nnred 11998 |
. . . . . . . 8
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → 𝑛 ∈ ℝ) |
50 | | simpl2 1191 |
. . . . . . . . 9
⊢ ((((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) → ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠)) |
51 | 50 | r19.21bi 3133 |
. . . . . . . 8
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ≤ (𝐹‘𝑠)) |
52 | | simplrr 775 |
. . . . . . . 8
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑠) < 𝑛) |
53 | 46, 47, 49, 51, 52 | lelttrd 11143 |
. . . . . . 7
⊢
(((((𝐹‘𝑠) ∈ ℝ ∧
∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) < 𝑛) |
54 | 53 | ex 413 |
. . . . . 6
⊢ ((((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) → (𝑡 ∈ 𝑇 → (𝐹‘𝑡) < 𝑛)) |
55 | 42, 54 | ralrimi 3140 |
. . . . 5
⊢ ((((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑠) < 𝑛)) → ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛) |
56 | | arch 12240 |
. . . . . 6
⊢ ((𝐹‘𝑠) ∈ ℝ → ∃𝑛 ∈ ℕ (𝐹‘𝑠) < 𝑛) |
57 | 56 | 3ad2ant1 1132 |
. . . . 5
⊢ (((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) → ∃𝑛 ∈ ℕ (𝐹‘𝑠) < 𝑛) |
58 | 55, 57 | reximddv 3202 |
. . . 4
⊢ (((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) → ∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛) |
59 | 58 | eximi 1837 |
. . 3
⊢
(∃𝑠((𝐹‘𝑠) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ (𝐹‘𝑠) ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ∈ ℝ) → ∃𝑠∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛) |
60 | 30, 59 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑠∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛) |
61 | | 19.9v 1987 |
. 2
⊢
(∃𝑠∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛 ↔ ∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛) |
62 | 60, 61 | sylib 217 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛) |