Step | Hyp | Ref
| Expression |
1 | | caubl.5 |
. . 3
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ (2nd
‘(𝐹‘𝑛)) < 𝑟) |
2 | | 2fveq3 6776 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑛 → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘𝑛))) |
3 | 2 | sseq1d 3957 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑛 → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
4 | 3 | imbi2d 341 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑛 → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
5 | | 2fveq3 6776 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑘 → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘𝑘))) |
6 | 5 | sseq1d 3957 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑘 → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
7 | 6 | imbi2d 341 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑘 → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
8 | | 2fveq3 6776 |
. . . . . . . . . . . . 13
⊢ (𝑟 = (𝑘 + 1) → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘(𝑘 + 1)))) |
9 | 8 | sseq1d 3957 |
. . . . . . . . . . . 12
⊢ (𝑟 = (𝑘 + 1) → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
10 | 9 | imbi2d 341 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑘 + 1) → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
11 | | ssid 3948 |
. . . . . . . . . . . 12
⊢
((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) |
12 | 11 | 2a1i 12 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
13 | | caubl.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) |
14 | | eluznn 12669 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
15 | | fvoveq1 7295 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1))) |
16 | 15 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) = ((ball‘𝐷)‘(𝐹‘(𝑘 + 1)))) |
17 | | 2fveq3 6776 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((ball‘𝐷)‘(𝐹‘𝑘))) |
18 | 16, 17 | sseq12d 3959 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘)))) |
19 | 18 | rspccva 3560 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘))) |
20 | 13, 14, 19 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑛))) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘))) |
21 | 20 | anassrs 468 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘))) |
22 | | sstr2 3933 |
. . . . . . . . . . . . . 14
⊢
(((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
24 | 23 | expcom 414 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → ((𝜑 ∧ 𝑛 ∈ ℕ) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
25 | 24 | a2d 29 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))) |
26 | 4, 7, 10, 7, 12, 25 | uzind4 12657 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
27 | 26 | com12 32 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (ℤ≥‘𝑛) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
28 | 27 | ad2ant2r 744 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))) |
29 | | relxp 5608 |
. . . . . . . . . . . . . . . 16
⊢ Rel
(𝑋 ×
ℝ+) |
30 | | caubl.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 ×
ℝ+)) |
31 | 30 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐹:ℕ⟶(𝑋 ×
ℝ+)) |
32 | | simplrl 774 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℕ) |
33 | 31, 32 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑛) ∈ (𝑋 ×
ℝ+)) |
34 | | 1st2nd 7874 |
. . . . . . . . . . . . . . . 16
⊢ ((Rel
(𝑋 ×
ℝ+) ∧ (𝐹‘𝑛) ∈ (𝑋 × ℝ+)) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
35 | 29, 33, 34 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑛) = 〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
36 | 35 | fveq2d 6775 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((ball‘𝐷)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉)) |
37 | | df-ov 7275 |
. . . . . . . . . . . . . 14
⊢
((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) = ((ball‘𝐷)‘〈(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))〉) |
38 | 36, 37 | eqtr4di 2798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛)))) |
39 | | caubl.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
40 | 39 | ad3antrrr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐷 ∈ (∞Met‘𝑋)) |
41 | | xp1st 7857 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑛) ∈ (𝑋 × ℝ+) →
(1st ‘(𝐹‘𝑛)) ∈ 𝑋) |
42 | 33, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st
‘(𝐹‘𝑛)) ∈ 𝑋) |
43 | | xp2nd 7858 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) ∈ (𝑋 × ℝ+) →
(2nd ‘(𝐹‘𝑛)) ∈
ℝ+) |
44 | 33, 43 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ+) |
45 | 44 | rpxrd 12784 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ*) |
46 | | simpllr 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℝ+) |
47 | 46 | rpxrd 12784 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℝ*) |
48 | | simplrr 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑛)) < 𝑟) |
49 | | rpre 12749 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(𝐹‘𝑛)) ∈ ℝ+ →
(2nd ‘(𝐹‘𝑛)) ∈ ℝ) |
50 | | rpre 12749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
51 | | ltle 11074 |
. . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((2nd
‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟)) |
52 | 49, 50, 51 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢
(((2nd ‘(𝐹‘𝑛)) ∈ ℝ+ ∧ 𝑟 ∈ ℝ+)
→ ((2nd ‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟)) |
53 | 44, 46, 52 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((2nd
‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟)) |
54 | 48, 53 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑛)) ≤ 𝑟) |
55 | | ssbl 23587 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (1st
‘(𝐹‘𝑛)) ∈ 𝑋) ∧ ((2nd ‘(𝐹‘𝑛)) ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
∧ (2nd ‘(𝐹‘𝑛)) ≤ 𝑟) → ((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)) |
56 | 40, 42, 45, 47, 54, 55 | syl221anc 1380 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((1st
‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)) |
57 | 38, 56 | eqsstrd 3964 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)) |
58 | | sstr2 3933 |
. . . . . . . . . . . 12
⊢
(((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))) |
59 | 57, 58 | syl5com 31 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))) |
60 | | simprl 768 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → 𝑛 ∈ ℕ) |
61 | 60, 14 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
62 | 31, 61 | ffvelrnd 6959 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ∈ (𝑋 ×
ℝ+)) |
63 | | xp1st 7857 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘) ∈ (𝑋 × ℝ+) →
(1st ‘(𝐹‘𝑘)) ∈ 𝑋) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st
‘(𝐹‘𝑘)) ∈ 𝑋) |
65 | | xp2nd 7858 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘) ∈ (𝑋 × ℝ+) →
(2nd ‘(𝐹‘𝑘)) ∈
ℝ+) |
66 | 62, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd
‘(𝐹‘𝑘)) ∈
ℝ+) |
67 | | blcntr 23577 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st
‘(𝐹‘𝑘)) ∈ 𝑋 ∧ (2nd ‘(𝐹‘𝑘)) ∈ ℝ+) →
(1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘)))) |
68 | 40, 64, 66, 67 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st
‘(𝐹‘𝑘)) ∈ ((1st
‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘)))) |
69 | | 1st2nd 7874 |
. . . . . . . . . . . . . . 15
⊢ ((Rel
(𝑋 ×
ℝ+) ∧ (𝐹‘𝑘) ∈ (𝑋 × ℝ+)) → (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
70 | 29, 62, 69 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) = 〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
71 | 70 | fveq2d 6775 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) = ((ball‘𝐷)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉)) |
72 | | df-ov 7275 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘))) = ((ball‘𝐷)‘〈(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))〉) |
73 | 71, 72 | eqtr4di 2798 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) = ((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘)))) |
74 | 68, 73 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st
‘(𝐹‘𝑘)) ∈ ((ball‘𝐷)‘(𝐹‘𝑘))) |
75 | | ssel 3919 |
. . . . . . . . . . 11
⊢
(((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) → ((1st ‘(𝐹‘𝑘)) ∈ ((ball‘𝐷)‘(𝐹‘𝑘)) → (1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))) |
76 | 59, 74, 75 | syl6ci 71 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → (1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))) |
77 | | elbl2 23554 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧
((1st ‘(𝐹‘𝑛)) ∈ 𝑋 ∧ (1st ‘(𝐹‘𝑘)) ∈ 𝑋)) → ((1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) ↔ ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
78 | 40, 47, 42, 64, 77 | syl22anc 836 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((1st
‘(𝐹‘𝑘)) ∈ ((1st
‘(𝐹‘𝑛))(ball‘𝐷)𝑟) ↔ ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
79 | 76, 78 | sylibd 238 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
80 | 79 | ex 413 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))) |
81 | 28, 80 | mpdd 43 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → ((1st
‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
82 | 81 | ralrimiv 3109 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧
(2nd ‘(𝐹‘𝑛)) < 𝑟)) → ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟) |
83 | 82 | expr 457 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) →
((2nd ‘(𝐹‘𝑛)) < 𝑟 → ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
84 | 83 | reximdva 3205 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑛 ∈ ℕ
(2nd ‘(𝐹‘𝑛)) < 𝑟 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
85 | 84 | ralimdva 3105 |
. . 3
⊢ (𝜑 → (∀𝑟 ∈ ℝ+
∃𝑛 ∈ ℕ
(2nd ‘(𝐹‘𝑛)) < 𝑟 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
86 | 1, 85 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟) |
87 | | nnuz 12632 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
88 | | 1zzd 12362 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
89 | | fvco3 6864 |
. . . 4
⊢ ((𝐹:ℕ⟶(𝑋 × ℝ+)
∧ 𝑘 ∈ ℕ)
→ ((1st ∘ 𝐹)‘𝑘) = (1st ‘(𝐹‘𝑘))) |
90 | 30, 89 | sylan 580 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1st
∘ 𝐹)‘𝑘) = (1st
‘(𝐹‘𝑘))) |
91 | | fvco3 6864 |
. . . 4
⊢ ((𝐹:ℕ⟶(𝑋 × ℝ+)
∧ 𝑛 ∈ ℕ)
→ ((1st ∘ 𝐹)‘𝑛) = (1st ‘(𝐹‘𝑛))) |
92 | 30, 91 | sylan 580 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
∘ 𝐹)‘𝑛) = (1st
‘(𝐹‘𝑛))) |
93 | | 1stcof 7855 |
. . . 4
⊢ (𝐹:ℕ⟶(𝑋 × ℝ+)
→ (1st ∘ 𝐹):ℕ⟶𝑋) |
94 | 30, 93 | syl 17 |
. . 3
⊢ (𝜑 → (1st ∘
𝐹):ℕ⟶𝑋) |
95 | 87, 39, 88, 90, 92, 94 | iscauf 24455 |
. 2
⊢ (𝜑 → ((1st ∘
𝐹) ∈ (Cau‘𝐷) ↔ ∀𝑟 ∈ ℝ+
∃𝑛 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)) |
96 | 86, 95 | mpbird 256 |
1
⊢ (𝜑 → (1st ∘
𝐹) ∈ (Cau‘𝐷)) |