Step | Hyp | Ref
| Expression |
1 | | caubl.5 |
. . 3
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ (2nd
‘(𝐹‘𝑛)) < 𝑟) |
2 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑛 → (𝐹‘𝑟) = (𝐹‘𝑛)) |
3 | 2 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑛 → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘𝑛))) |
4 | 3 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑛 → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
5 | 4 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑛 → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
6 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑘 → (𝐹‘𝑟) = (𝐹‘𝑘)) |
7 | 6 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑘 → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘𝑘))) |
8 | 7 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑘 → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
9 | 8 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑘 → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
10 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = (𝑘 + 1) → (𝐹‘𝑟) = (𝐹‘(𝑘 + 1))) |
11 | 10 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑟 = (𝑘 + 1) → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘(𝑘 + 1)))) |
12 | 11 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑟 = (𝑘 + 1) → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
13 | 12 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑘 + 1) → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
14 | | ssid 3587 |
. . . . . . . . . . . 12
⊢
((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) |
15 | 14 | 2a1i 12 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
16 | | caubl.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) |
17 | | eluznn 11634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
18 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1))) |
20 | 19 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) = ((ball‘𝐷)‘(𝐹‘(𝑘 + 1)))) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
22 | 21 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((ball‘𝐷)‘(𝐹‘𝑘))) |
23 | 20, 22 | sseq12d 3597 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘)))) |
24 | 23 | rspccva 3281 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘))) |
25 | 16, 17, 24 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑛))) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘))) |
26 | 25 | anassrs 678 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘))) |
27 | | sstr2 3575 |
. . . . . . . . . . . . . 14
⊢
(((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
29 | 28 | expcom 450 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → ((𝜑 ∧ 𝑛 ∈ ℕ) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
30 | 29 | a2d 29 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
31 | 5, 9, 13, 9, 15, 30 | uzind4 11622 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
32 | 31 | com12 32 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (ℤ≥‘𝑛) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
33 | 32 | ad2ant2r 779 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
34 | | relxp 5150 |
. . . . . . . . . . . . . . . 16
⊢ Rel
(𝑋 ×
ℝ+) |
35 | | caubl.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 ×
ℝ+)) |
36 | 35 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐹:ℕ⟶(𝑋 ×
ℝ+)) |
37 | | simplrl 796 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℕ) |
38 | 36, 37 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑛) ∈ (𝑋 ×
ℝ+)) |
39 | | 1st2nd 7105 |
. . . . . . . . . . . . . . . 16
⊢ ((Rel
(𝑋 ×
ℝ+) ∧ (𝐹‘𝑛) ∈ (𝑋 × ℝ+)) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
40 | 34, 38, 39 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
41 | 40 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((ball‘𝐷)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉)) |
42 | | df-ov 6552 |
. . . . . . . . . . . . . 14
⊢
((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) = ((ball‘𝐷)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
43 | 41, 42 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛)))) |
44 | | caubl.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
45 | 44 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐷 ∈ (∞Met‘𝑋)) |
46 | | xp1st 7089 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑛) ∈ (𝑋 × ℝ+) →
(1st ‘(𝐹‘𝑛)) ∈ 𝑋) |
47 | 38, 46 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st
‘(𝐹‘𝑛)) ∈ 𝑋) |
48 | | xp2nd 7090 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) ∈ (𝑋 × ℝ+) →
(2nd ‘(𝐹‘𝑛)) ∈
ℝ+) |
49 | 38, 48 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ+) |
50 | 49 | rpxrd 11749 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ*) |
51 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℝ+) |
52 | 51 | rpxrd 11749 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℝ*) |
53 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑛)) < 𝑟) |
54 | | rpre 11715 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(𝐹‘𝑛)) ∈ ℝ+ →
(2nd ‘(𝐹‘𝑛)) ∈ ℝ) |
55 | | rpre 11715 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
56 | | ltle 10005 |
. . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((2nd
‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟)) |
57 | 54, 55, 56 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢
(((2nd ‘(𝐹‘𝑛)) ∈ ℝ+ ∧ 𝑟 ∈ ℝ+)
→ ((2nd ‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟)) |
58 | 49, 51, 57 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((2nd
‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟)) |
59 | 53, 58 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑛)) ≤ 𝑟) |
60 | | ssbl 22038 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (1st
‘(𝐹‘𝑛)) ∈ 𝑋) ∧ ((2nd ‘(𝐹‘𝑛)) ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
∧ (2nd ‘(𝐹‘𝑛)) ≤ 𝑟) → ((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)) |
61 | 45, 47, 50, 52, 59, 60 | syl221anc 1329 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((1st
‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)) |
62 | 43, 61 | eqsstrd 3602 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)) |
63 | | sstr2 3575 |
. . . . . . . . . . . 12
⊢
(((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))) |
64 | 62, 63 | syl5com 31 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))) |
65 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → 𝑛 ∈ ℕ) |
66 | 65, 17 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
67 | 36, 66 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ∈ (𝑋 ×
ℝ+)) |
68 | | xp1st 7089 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘) ∈ (𝑋 × ℝ+) →
(1st ‘(𝐹‘𝑘)) ∈ 𝑋) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st
‘(𝐹‘𝑘)) ∈ 𝑋) |
70 | | xp2nd 7090 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘) ∈ (𝑋 × ℝ+) →
(2nd ‘(𝐹‘𝑘)) ∈
ℝ+) |
71 | 67, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ+) |
72 | | blcntr 22028 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st
‘(𝐹‘𝑘)) ∈ 𝑋 ∧ (2nd ‘(𝐹‘𝑘)) ∈ ℝ+) →
(1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘)))) |
73 | 45, 69, 71, 72 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st
‘(𝐹‘𝑘)) ∈ ((1st
‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘)))) |
74 | | 1st2nd 7105 |
. . . . . . . . . . . . . . 15
⊢ ((Rel
(𝑋 ×
ℝ+) ∧ (𝐹‘𝑘) ∈ (𝑋 × ℝ+)) → (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
75 | 34, 67, 74 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
76 | 75 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) = ((ball‘𝐷)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉)) |
77 | | df-ov 6552 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘))) = ((ball‘𝐷)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
78 | 76, 77 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) = ((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘)))) |
79 | 73, 78 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st
‘(𝐹‘𝑘)) ∈ ((ball‘𝐷)‘(𝐹‘𝑘))) |
80 | | ssel 3562 |
. . . . . . . . . . 11
⊢
(((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) → ((1st ‘(𝐹‘𝑘)) ∈ ((ball‘𝐷)‘(𝐹‘𝑘)) → (1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))) |
81 | 64, 79, 80 | syl6ci 69 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → (1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))) |
82 | | elbl2 22005 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧
((1st ‘(𝐹‘𝑛)) ∈ 𝑋 ∧ (1st ‘(𝐹‘𝑘)) ∈ 𝑋)) → ((1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) ↔ ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
83 | 45, 52, 47, 69, 82 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((1st
‘(𝐹‘𝑘)) ∈ ((1st
‘(𝐹‘𝑛))(ball‘𝐷)𝑟) ↔ ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
84 | 81, 83 | sylibd 228 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
85 | 84 | ex 449 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))) |
86 | 33, 85 | mpdd 42 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → ((1st
‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
87 | 86 | ralrimiv 2948 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟) |
88 | 87 | expr 641 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) →
((2nd ‘(𝐹‘𝑛)) < 𝑟 → ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
89 | 88 | reximdva 3000 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑛 ∈ ℕ
(2nd ‘(𝐹‘𝑛)) < 𝑟 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
90 | 89 | ralimdva 2945 |
. . 3
⊢ (𝜑 → (∀𝑟 ∈ ℝ+
∃𝑛 ∈ ℕ
(2nd ‘(𝐹‘𝑛)) < 𝑟 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
91 | 1, 90 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟) |
92 | | nnuz 11599 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
93 | | 1zzd 11285 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
94 | | fvco3 6185 |
. . . 4
⊢ ((𝐹:ℕ⟶(𝑋 × ℝ+)
∧ 𝑘 ∈ ℕ)
→ ((1st ∘ 𝐹)‘𝑘) = (1st ‘(𝐹‘𝑘))) |
95 | 35, 94 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1st
∘ 𝐹)‘𝑘) = (1st
‘(𝐹‘𝑘))) |
96 | | fvco3 6185 |
. . . 4
⊢ ((𝐹:ℕ⟶(𝑋 × ℝ+)
∧ 𝑛 ∈ ℕ)
→ ((1st ∘ 𝐹)‘𝑛) = (1st ‘(𝐹‘𝑛))) |
97 | 35, 96 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
∘ 𝐹)‘𝑛) = (1st
‘(𝐹‘𝑛))) |
98 | | 1stcof 7087 |
. . . 4
⊢ (𝐹:ℕ⟶(𝑋 × ℝ+)
→ (1st ∘ 𝐹):ℕ⟶𝑋) |
99 | 35, 98 | syl 17 |
. . 3
⊢ (𝜑 → (1st ∘
𝐹):ℕ⟶𝑋) |
100 | 92, 44, 93, 95, 97, 99 | iscauf 22886 |
. 2
⊢ (𝜑 → ((1st ∘
𝐹) ∈ (Cau‘𝐷) ↔ ∀𝑟 ∈ ℝ+
∃𝑛 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
101 | 91, 100 | mpbird 246 |
1
⊢ (𝜑 → (1st ∘
𝐹) ∈ (Cau‘𝐷)) |