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	$⊢ φ \to J \in TopOn (X)$
	Assertion	lmbr3v	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$

Proof

Step	Hyp	Ref	Expression
1		lmbr3v.1	$⊢ φ \to J \in TopOn (X)$
2		eqid	$⊢ ℤ_{\geq 0} = ℤ_{\geq 0}$
3		0zd	$⊢ φ \to 0 \in ℤ$
4	1 2 3	lmbr2	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ_{\geq 0} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
5		0z	$⊢ 0 \in ℤ$
6	2	rexuz3	$⊢ 0 \in ℤ \to (\exists j \in ℤ_{\geq 0} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
7	5 6	ax-mp	$⊢ \exists j \in ℤ_{\geq 0} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
8	7	imbi2i	$⊢ (P \in u \to \exists j \in ℤ_{\geq 0} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \leftrightarrow (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
9	8	ralbii	$⊢ \forall u \in J (P \in u \to \exists j \in ℤ_{\geq 0} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \leftrightarrow \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
10	9	3anbi3i	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ_{\geq 0} \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
11	4 10	bitrdi	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$