lmbrf

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. This version of lmbr2 presupposes that F is a function. (Contributed by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Hypotheses	lmbr.2	$⊢ φ \to J \in TopOn (X)$
	lmbr2.4	$⊢ Z = ℤ_{\geq M}$
	lmbr2.5	$⊢ φ \to M \in ℤ$
	lmbrf.6	$⊢ φ \to F : Z ⟶ X$
	lmbrf.7	$⊢ (φ \land k \in Z) \to F (k) = A$
Assertion	lmbrf	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} A \in u)))$

Proof

Step	Hyp	Ref	Expression
1		lmbr.2	$⊢ φ \to J \in TopOn (X)$
2		lmbr2.4	$⊢ Z = ℤ_{\geq M}$
3		lmbr2.5	$⊢ φ \to M \in ℤ$
4		lmbrf.6	$⊢ φ \to F : Z ⟶ X$
5		lmbrf.7	$⊢ (φ \land k \in Z) \to F (k) = A$
6	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 Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
7		3anass	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in Z \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 Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
8	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
9	5	eleq1d	$⊢ (φ \land k \in Z) \to (F (k) \in u \leftrightarrow A \in u)$
10	4	fdmd	$⊢ φ \to dom F = Z$
11	10	eleq2d	$⊢ φ \to (k \in dom F \leftrightarrow k \in Z)$
12	11	biimpar	$⊢ (φ \land k \in Z) \to k \in dom F$
13	12	biantrurd	$⊢ (φ \land k \in Z) \to (F (k) \in u \leftrightarrow (k \in dom F \land F (k) \in u))$
14	9 13	bitr3d	$⊢ (φ \land k \in Z) \to (A \in u \leftrightarrow (k \in dom F \land F (k) \in u))$
15	8 14	sylan2	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to (A \in u \leftrightarrow (k \in dom F \land F (k) \in u))$
16	15	anassrs	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (A \in u \leftrightarrow (k \in dom F \land F (k) \in u))$
17	16	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} A \in u \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
18	17	rexbidva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} A \in u \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
19	18	imbi2d	$⊢ φ \to ((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} A \in u) \leftrightarrow (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
20	19	ralbidv	$⊢ φ \to (\forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} A \in u) \leftrightarrow \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
21	20	anbi2d	$⊢ φ \to ((P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} A \in u)) \leftrightarrow (P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
22		toponmax	$⊢ J \in TopOn (X) \to X \in J$
23	1 22	syl	$⊢ φ \to X \in J$
24		cnex	$⊢ ℂ \in V$
25	23 24	jctir	$⊢ φ \to (X \in J \land ℂ \in V)$
26		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
27		zsscn	$⊢ ℤ \subseteq ℂ$
28	26 27	sstri	$⊢ ℤ_{\geq M} \subseteq ℂ$
29	2 28	eqsstri	$⊢ Z \subseteq ℂ$
30	4 29	jctir	$⊢ φ \to (F : Z ⟶ X \land Z \subseteq ℂ)$
31		elpm2r	$⊢ ((X \in J \land ℂ \in V) \land (F : Z ⟶ X \land Z \subseteq ℂ)) \to F \in (X ↑_{𝑝𝑚} ℂ)$
32	25 30 31	syl2anc	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
33	32	biantrurd	$⊢ φ \to ((P \in X \land \forall u \in J (P \in u \to \exists j \in Z \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 Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))))$
34	21 33	bitr2d	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land (P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))) \leftrightarrow (P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} A \in u)))$
35	7 34	syl5bb	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))) \leftrightarrow (P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} A \in u)))$
36	6 35	bitrd	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} A \in u)))$

Metamath Proof Explorer

Theorem lmbrf

Proof