lmbr3

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
Hypotheses	lmbr3.1	$⊢ \underline{Ⅎ} k F$
	lmbr3.2	$⊢ φ \to J \in TopOn (X)$
Assertion	lmbr3	$⊢ φ \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		lmbr3.1	$⊢ \underline{Ⅎ} k F$
2		lmbr3.2	$⊢ φ \to J \in TopOn (X)$
3	2	lmbr3v	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall v \in J (P \in v \to \exists i \in ℤ \forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in v))))$
4		eleq2w	$⊢ v = u \to (P \in v \leftrightarrow P \in u)$
5		eleq2w	$⊢ v = u \to (F (l) \in v \leftrightarrow F (l) \in u)$
6	5	anbi2d	$⊢ v = u \to ((l \in dom F \land F (l) \in v) \leftrightarrow (l \in dom F \land F (l) \in u))$
7	6	rexralbidv	$⊢ v = u \to (\exists i \in ℤ \forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in v) \leftrightarrow \exists i \in ℤ \forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in u))$
8		fveq2	$⊢ i = j \to ℤ_{\geq i} = ℤ_{\geq j}$
9	8	raleqdv	$⊢ i = j \to (\forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in u) \leftrightarrow \forall l \in ℤ_{\geq j} (l \in dom F \land F (l) \in u))$
10		nfcv	$⊢ \underline{Ⅎ} k l$
11	1	nfdm	$⊢ \underline{Ⅎ} k dom F$
12	10 11	nfel	$⊢ Ⅎ k l \in dom F$
13	1 10	nffv	$⊢ \underline{Ⅎ} k F (l)$
14		nfcv	$⊢ \underline{Ⅎ} k u$
15	13 14	nfel	$⊢ Ⅎ k F (l) \in u$
16	12 15	nfan	$⊢ Ⅎ k (l \in dom F \land F (l) \in u)$
17		nfv	$⊢ Ⅎ l (k \in dom F \land F (k) \in u)$
18		eleq1w	$⊢ l = k \to (l \in dom F \leftrightarrow k \in dom F)$
19		fveq2	$⊢ l = k \to F (l) = F (k)$
20	19	eleq1d	$⊢ l = k \to (F (l) \in u \leftrightarrow F (k) \in u)$
21	18 20	anbi12d	$⊢ l = k \to ((l \in dom F \land F (l) \in u) \leftrightarrow (k \in dom F \land F (k) \in u))$
22	16 17 21	cbvralw	$⊢ \forall l \in ℤ_{\geq j} (l \in dom F \land F (l) \in u) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
23	9 22	bitrdi	$⊢ i = j \to (\forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in u) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
24	23	cbvrexvw	$⊢ \exists i \in ℤ \forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
25	7 24	bitrdi	$⊢ v = u \to (\exists i \in ℤ \forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in v) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
26	4 25	imbi12d	$⊢ v = u \to ((P \in v \to \exists i \in ℤ \forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in v)) \leftrightarrow (P \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
27	26	cbvralvw	$⊢ \forall v \in J (P \in v \to \exists i \in ℤ \forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in v)) \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))$
28	27	3anbi3i	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall v \in J (P \in v \to \exists i \in ℤ \forall l \in ℤ_{\geq i} (l \in dom F \land F (l) \in v))) \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)))$
29	3 28	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))))$

Metamath Proof Explorer

Theorem lmbr3

Proof