Proof of Theorem xlimbr
| Step | Hyp | Ref
| Expression |
| 1 | | df-xlim 45834 |
. . . 4
⊢ ~~>* =
(⇝𝑡‘(ordTop‘ ≤ )) |
| 2 | 1 | breqi 5149 |
. . 3
⊢ (𝐹~~>*𝑃 ↔ 𝐹(⇝𝑡‘(ordTop‘
≤ ))𝑃) |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹~~>*𝑃 ↔ 𝐹(⇝𝑡‘(ordTop‘
≤ ))𝑃)) |
| 4 | | xlimbr.k |
. . 3
⊢
Ⅎ𝑘𝐹 |
| 5 | | letopon 23213 |
. . . 4
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
| 6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → (ordTop‘ ≤ )
∈ (TopOn‘ℝ*)) |
| 7 | 4, 6 | lmbr3 45762 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑡‘(ordTop‘
≤ ))𝑃 ↔ (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |
| 8 | | simpr2 1196 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → 𝑃 ∈
ℝ*) |
| 9 | | xlimbr.j |
. . . . . . . 8
⊢ 𝐽 = (ordTop‘ ≤
) |
| 10 | 9 | eqcomi 2746 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) = 𝐽 |
| 11 | 10 | raleqi 3324 |
. . . . . 6
⊢
(∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) ↔ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 12 | | xlimbr.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 13 | | xlimbr.z |
. . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 14 | 13 | rexuz3 15387 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 15 | 14 | bicomd 223 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 16 | 15 | imbi2d 340 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) ↔ (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 17 | 16 | biimpd 229 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 18 | 17 | ralimdv 3169 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
(∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 19 | 12, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 20 | 19 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 21 | 11, 20 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 22 | 21 | 3ad2antr3 1191 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 23 | 8, 22 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 24 | | cnex 11236 |
. . . . . . 7
⊢ ℂ
∈ V |
| 25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ ∈
V) |
| 26 | 6 | elfvexd 6945 |
. . . . . 6
⊢ (𝜑 → ℝ* ∈
V) |
| 27 | 13 | uzsscn2 45488 |
. . . . . . 7
⊢ 𝑍 ⊆
ℂ |
| 28 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑍 ⊆ ℂ) |
| 29 | | xlimbr.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
| 30 | 25, 26, 28, 29 | fpmd 45270 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (ℝ*
↑pm ℂ)) |
| 31 | 30 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → 𝐹 ∈ (ℝ*
↑pm ℂ)) |
| 32 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → 𝑃 ∈
ℝ*) |
| 33 | 16 | biimprd 248 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → ((𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 34 | 33 | ralimdv 3169 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
(∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 35 | 12, 34 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 36 | 35 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 37 | 9 | raleqi 3324 |
. . . . . 6
⊢
(∀𝑢 ∈
𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) ↔ ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 38 | 36, 37 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) → ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 39 | 38 | adantrl 716 |
. . . 4
⊢ ((𝜑 ∧ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → ∀𝑢 ∈ (ordTop‘ ≤ )(𝑃 ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 40 | 31, 32, 39 | 3jca 1129 |
. . 3
⊢ ((𝜑 ∧ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) → (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 41 | 23, 40 | impbida 801 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (ℝ*
↑pm ℂ) ∧ 𝑃 ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(𝑃
∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) ↔ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |
| 42 | 3, 7, 41 | 3bitrd 305 |
1
⊢ (𝜑 → (𝐹~~>*𝑃 ↔ (𝑃 ∈ ℝ* ∧
∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |