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 ⊢ φ → J ∈ TopOn ⁡ X
Assertion lmbr3v ⊢ φ → F ⇝t ⁡ J P ↔ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ u ∈ J P ∈ u → ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u

Proof

Step Hyp Ref Expression
1 lmbr3v.1 ⊢ φ → J ∈ TopOn ⁡ X
2 eqid ⊢ ℤ ≥ 0 = ℤ ≥ 0
3 0zd ⊢ φ → 0 ∈ ℤ
4 1 2 3 lmbr2 ⊢ φ → F ⇝t ⁡ J P ↔ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ u ∈ J P ∈ u → ∃ j ∈ ℤ ≥ 0 ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u
5 0z ⊢ 0 ∈ ℤ
6 2 rexuz3 ⊢ 0 ∈ ℤ → ∃ j ∈ ℤ ≥ 0 ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u
7 5 6 ax-mp ⊢ ∃ j ∈ ℤ ≥ 0 ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u
8 7 imbi2i ⊢ P ∈ u → ∃ j ∈ ℤ ≥ 0 ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u ↔ P ∈ u → ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u
9 8 ralbii ⊢ ∀ u ∈ J P ∈ u → ∃ j ∈ ℤ ≥ 0 ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u ↔ ∀ u ∈ J P ∈ u → ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u
10 9 3anbi3i ⊢ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ u ∈ J P ∈ u → ∃ j ∈ ℤ ≥ 0 ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u ↔ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ u ∈ J P ∈ u → ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u
11 4 10 bitrdi ⊢ φ → F ⇝t ⁡ J P ↔ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ u ∈ J P ∈ u → ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ u