This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmmbr3

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 ⊢ J = MetOpen ⁡ D
lmmbr.3 ⊢ φ → D ∈ ∞Met ⁡ X
lmmbr3.5 ⊢ Z = ℤ ≥ M
lmmbr3.6 ⊢ φ → M ∈ ℤ
Assertion lmmbr3 ⊢ φ → F ⇝t ⁡ J P ↔ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x

Proof

Step Hyp Ref Expression
1 lmmbr.2 ⊢ J = MetOpen ⁡ D
2 lmmbr.3 ⊢ φ → D ∈ ∞Met ⁡ X
3 lmmbr3.5 ⊢ Z = ℤ ≥ M
4 lmmbr3.6 ⊢ φ → M ∈ ℤ
5 1 2 lmmbr2 ⊢ φ → F ⇝t ⁡ J P ↔ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x
6 3 rexuz3 ⊢ M ∈ ℤ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x
7 4 6 syl ⊢ φ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x
8 7 ralbidv ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x ↔ ∀ x ∈ ℝ + ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x
9 8 3anbi3d ⊢ φ → F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x ↔ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x
10 5 9 bitr4d ⊢ φ → F ⇝t ⁡ J P ↔ F ∈ X ↑ 𝑝𝑚 ℂ ∧ P ∈ X ∧ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j k ∈ dom ⁡ F ∧ F ⁡ k ∈ X ∧ F ⁡ k D P < x