Metamath Proof Explorer


Theorem lmbr3v

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypothesis lmbr3v.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
Assertion lmbr3v ( 𝜑 → ( 𝐹 ( ⇝𝑡𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lmbr3v.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 eqid ( ℤ ‘ 0 ) = ( ℤ ‘ 0 )
3 0zd ( 𝜑 → 0 ∈ ℤ )
4 1 2 3 lmbr2 ( 𝜑 → ( 𝐹 ( ⇝𝑡𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ( ℤ ‘ 0 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) )
5 0z 0 ∈ ℤ
6 2 rexuz3 ( 0 ∈ ℤ → ( ∃ 𝑗 ∈ ( ℤ ‘ 0 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
7 5 6 ax-mp ( ∃ 𝑗 ∈ ( ℤ ‘ 0 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) )
8 7 imbi2i ( ( 𝑃𝑢 → ∃ 𝑗 ∈ ( ℤ ‘ 0 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ↔ ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
9 8 ralbii ( ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ( ℤ ‘ 0 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ↔ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) )
10 9 3anbi3i ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ( ℤ ‘ 0 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) )
11 4 10 bitrdi ( 𝜑 → ( 𝐹 ( ⇝𝑡𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑢𝐽 ( 𝑃𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑢 ) ) ) ) )