Proof of Theorem xlimbr
Step | Hyp | Ref
| Expression |
1 | | df-xlim 43360 |
. . . 4
⊢ ~~>* =
(⇝𝑡‘(ordTop‘ ≤ )) |
2 | 1 | breqi 5080 |
. . 3
⊢ (𝐹~~>*𝑃 ↔ 𝐹(⇝𝑡‘(ordTop‘
≤ ))𝑃) |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹~~>*𝑃 ↔ 𝐹(⇝𝑡‘(ordTop‘
≤ ))𝑃)) |
4 | | xlimbr.k |
. . 3
⊢
Ⅎ𝑘𝐹 |
5 | | letopon 22356 |
. . . 4
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → (ordTop‘ ≤ )
∈ (TopOn‘ℝ*)) |
7 | 4, 6 | lmbr3 43288 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑡‘(ordTop‘
≤ ))𝑃 ↔ (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |
8 | | simpr2 1194 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → 𝑃 ∈
ℝ*) |
9 | | xlimbr.j |
. . . . . . . 8
⊢ 𝐽 = (ordTop‘ ≤
) |
10 | 9 | eqcomi 2747 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) = 𝐽 |
11 | 10 | raleqi 3346 |
. . . . . 6
⊢
(∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) ↔ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
12 | | xlimbr.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | | xlimbr.z |
. . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ≥‘𝑀) |
14 | 13 | rexuz3 15060 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
15 | 14 | bicomd 222 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
16 | 15 | imbi2d 341 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
17 | 16 | biimpd 228 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
18 | 17 | ralimdv 3109 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
(∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
19 | 12, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
20 | 19 | imp 407 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
21 | 11, 20 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
22 | 21 | 3ad2antr3 1189 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
23 | 8, 22 | jca 512 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
24 | | cnex 10952 |
. . . . . . 7
⊢ ℂ
∈ V |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ ∈
V) |
26 | 6 | elfvexd 6808 |
. . . . . 6
⊢ (𝜑 → ℝ* ∈
V) |
27 | 13 | uzsscn2 43018 |
. . . . . . 7
⊢ 𝑍 ⊆
ℂ |
28 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑍 ⊆ ℂ) |
29 | | xlimbr.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
30 | 25, 26, 28, 29 | fpmd 42811 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (ℝ*
↑pm ℂ)) |
31 | 30 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → 𝐹 ∈ (ℝ*
↑pm ℂ)) |
32 | | simprl 768 |
. . . 4
⊢ ((𝜑 ∧ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → 𝑃 ∈
ℝ*) |
33 | 16 | biimprd 247 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
34 | 33 | ralimdv 3109 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
(∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
35 | 12, 34 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
36 | 35 | imp 407 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
37 | 9 | raleqi 3346 |
. . . . . 6
⊢
(∀𝑢 ∈
𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) ↔ ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
38 | 36, 37 | sylib 217 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) → ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
39 | 38 | adantrl 713 |
. . . 4
⊢ ((𝜑 ∧ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
40 | 31, 32, 39 | 3jca 1127 |
. . 3
⊢ ((𝜑 ∧ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
41 | 23, 40 | impbida 798 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) ↔ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |
42 | 3, 7, 41 | 3bitrd 305 |
1
⊢ (𝜑 → (𝐹~~>*𝑃 ↔ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |