Metamath Proof Explorer


Theorem xlimbr

Description: Express the binary relation "sequence F converges to point P " w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses xlimbr.k 𝑘 𝐹
xlimbr.m ( 𝜑𝑀 ∈ ℤ )
xlimbr.z 𝑍 = ( ℤ𝑀 )
xlimbr.f ( 𝜑𝐹 : 𝑍 ⟶ ℝ* )
xlimbr.j 𝐽 = ( ordTop ‘ ≤ )
Assertion xlimbr ( 𝜑 → ( 𝐹 ~~>* 𝑃 ↔ ( 𝑃 ∈ ℝ* ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 xlimbr.k 𝑘 𝐹
2 xlimbr.m ( 𝜑𝑀 ∈ ℤ )
3 xlimbr.z 𝑍 = ( ℤ𝑀 )
4 xlimbr.f ( 𝜑𝐹 : 𝑍 ⟶ ℝ* )
5 xlimbr.j 𝐽 = ( ordTop ‘ ≤ )
6 df-xlim ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )
7 6 breqi ( 𝐹 ~~>* 𝑃𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝑃 )
8 7 a1i ( 𝜑 → ( 𝐹 ~~>* 𝑃𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝑃 ) )
9 letopon ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
10 9 a1i ( 𝜑 → ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) )
11 1 10 lmbr3 ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝑃 ↔ ( 𝐹 ∈ ( ℝ*pm ℂ ) ∧ 𝑃 ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) )
12 simpr2 ( ( 𝜑 ∧ ( 𝐹 ∈ ( ℝ*pm ℂ ) ∧ 𝑃 ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) → 𝑃 ∈ ℝ* )
13 5 eqcomi ( ordTop ‘ ≤ ) = 𝐽
14 13 raleqi ( ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ↔ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
15 3 rexuz3 ( 𝑀 ∈ ℤ → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
16 15 bicomd ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
17 16 imbi2d ( 𝑀 ∈ ℤ → ( ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ↔ ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
18 17 biimpd ( 𝑀 ∈ ℤ → ( ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) → ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
19 18 ralimdv ( 𝑀 ∈ ℤ → ( ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
20 2 19 syl ( 𝜑 → ( ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
21 20 imp ( ( 𝜑 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
22 14 21 sylan2b ( ( 𝜑 ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
23 22 3ad2antr3 ( ( 𝜑 ∧ ( 𝐹 ∈ ( ℝ*pm ℂ ) ∧ 𝑃 ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
24 12 23 jca ( ( 𝜑 ∧ ( 𝐹 ∈ ( ℝ*pm ℂ ) ∧ 𝑃 ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) → ( 𝑃 ∈ ℝ* ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
25 cnex ℂ ∈ V
26 25 a1i ( 𝜑 → ℂ ∈ V )
27 10 elfvexd ( 𝜑 → ℝ* ∈ V )
28 3 uzsscn2 𝑍 ⊆ ℂ
29 28 a1i ( 𝜑𝑍 ⊆ ℂ )
30 26 27 29 4 fpmd ( 𝜑𝐹 ∈ ( ℝ*pm ℂ ) )
31 30 adantr ( ( 𝜑 ∧ ( 𝑃 ∈ ℝ* ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) → 𝐹 ∈ ( ℝ*pm ℂ ) )
32 simprl ( ( 𝜑 ∧ ( 𝑃 ∈ ℝ* ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) → 𝑃 ∈ ℝ* )
33 17 biimprd ( 𝑀 ∈ ℤ → ( ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) → ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
34 33 ralimdv ( 𝑀 ∈ ℤ → ( ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
35 2 34 syl ( 𝜑 → ( ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
36 35 imp ( ( 𝜑 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) → ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
37 5 raleqi ( ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
38 36 37 sylib ( ( 𝜑 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) → ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
39 38 adantrl ( ( 𝜑 ∧ ( 𝑃 ∈ ℝ* ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) → ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
40 31 32 39 3jca ( ( 𝜑 ∧ ( 𝑃 ∈ ℝ* ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) → ( 𝐹 ∈ ( ℝ*pm ℂ ) ∧ 𝑃 ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
41 24 40 impbida ( 𝜑 → ( ( 𝐹 ∈ ( ℝ*pm ℂ ) ∧ 𝑃 ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ↔ ( 𝑃 ∈ ℝ* ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) )
42 8 11 41 3bitrd ( 𝜑 → ( 𝐹 ~~>* 𝑃 ↔ ( 𝑃 ∈ ℝ* ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) )