lmmbrf

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 lmmbr2 presupposes that F is a function. (Contributed by NM, 20-Jul-2007) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmmbr.2	$⊢ J = MetOpen (D)$
	lmmbr.3	$⊢ φ \to D \in ∞Met (X)$
	lmmbr3.5	$⊢ Z = ℤ_{\geq M}$
	lmmbr3.6	$⊢ φ \to M \in ℤ$
	lmmbrf.7	$⊢ (φ \land k \in Z) \to F (k) = A$
	lmmbrf.8	$⊢ φ \to F : Z ⟶ X$
Assertion	lmmbrf	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} A D P < x))$

Proof

Step	Hyp	Ref	Expression
1		lmmbr.2	$⊢ J = MetOpen (D)$
2		lmmbr.3	$⊢ φ \to D \in ∞Met (X)$
3		lmmbr3.5	$⊢ Z = ℤ_{\geq M}$
4		lmmbr3.6	$⊢ φ \to M \in ℤ$
5		lmmbrf.7	$⊢ (φ \land k \in Z) \to F (k) = A$
6		lmmbrf.8	$⊢ φ \to F : Z ⟶ X$
7		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
8		cnex	$⊢ ℂ \in V$
9	7 8	jctir	$⊢ D \in ∞Met (X) \to (X \in dom ∞Met \land ℂ \in V)$
10		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
11		zsscn	$⊢ ℤ \subseteq ℂ$
12	10 11	sstri	$⊢ ℤ_{\geq M} \subseteq ℂ$
13	3 12	eqsstri	$⊢ Z \subseteq ℂ$
14	13	jctr	$⊢ F : Z ⟶ X \to (F : Z ⟶ X \land Z \subseteq ℂ)$
15		elpm2r	$⊢ ((X \in dom ∞Met \land ℂ \in V) \land (F : Z ⟶ X \land Z \subseteq ℂ)) \to F \in (X ↑_{𝑝𝑚} ℂ)$
16	9 14 15	syl2an	$⊢ (D \in ∞Met (X) \land F : Z ⟶ X) \to F \in (X ↑_{𝑝𝑚} ℂ)$
17	2 6 16	syl2anc	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
18	17	biantrurd	$⊢ φ \to ((P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land (P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))))$
19	3	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
20	19	adantll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
21	5	oveq1d	$⊢ (φ \land k \in Z) \to F (k) D P = A D P$
22	21	breq1d	$⊢ (φ \land k \in Z) \to (F (k) D P < x \leftrightarrow A D P < x)$
23	22	adantrl	$⊢ (φ \land (j \in Z \land k \in Z)) \to (F (k) D P < x \leftrightarrow A D P < x)$
24	6	fdmd	$⊢ φ \to dom F = Z$
25	24	eleq2d	$⊢ φ \to (k \in dom F \leftrightarrow k \in Z)$
26	25	biimpar	$⊢ (φ \land k \in Z) \to k \in dom F$
27	6	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in X$
28	26 27	jca	$⊢ (φ \land k \in Z) \to (k \in dom F \land F (k) \in X)$
29	28	biantrurd	$⊢ (φ \land k \in Z) \to (F (k) D P < x \leftrightarrow ((k \in dom F \land F (k) \in X) \land F (k) D P < x))$
30		df-3an	$⊢ (k \in dom F \land F (k) \in X \land F (k) D P < x) \leftrightarrow ((k \in dom F \land F (k) \in X) \land F (k) D P < x)$
31	29 30	bitr4di	$⊢ (φ \land k \in Z) \to (F (k) D P < x \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D P < x))$
32	31	adantrl	$⊢ (φ \land (j \in Z \land k \in Z)) \to (F (k) D P < x \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D P < x))$
33	23 32	bitr3d	$⊢ (φ \land (j \in Z \land k \in Z)) \to (A D P < x \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D P < x))$
34	33	anassrs	$⊢ ((φ \land j \in Z) \land k \in Z) \to (A D P < x \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D P < x))$
35	20 34	syldan	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (A D P < x \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D P < x))$
36	35	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} A D P < x \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
37	36	rexbidva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} A D P < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
38	37	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} A D P < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
39	38	anbi2d	$⊢ φ \to ((P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} A D P < x) \leftrightarrow (P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$
40	1 2 3 4	lmmbr3	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$
41		3anass	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land (P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$
42	40 41	bitrdi	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land (P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))))$
43	18 39 42	3bitr4rd	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} A D P < x))$

Metamath Proof Explorer

Theorem lmmbrf

Proof