lmmbr2

Description: Express the binary relation "sequence F converges to point P " in a metric space. Definition 1.4-1 of Kreyszig p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmmbr.2	$⊢ J = MetOpen (D)$
	lmmbr.3	$⊢ φ \to D \in ∞Met (X)$
Assertion	lmmbr2	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$

Proof

Step	Hyp	Ref	Expression
1		lmmbr.2	$⊢ J = MetOpen (D)$
2		lmmbr.3	$⊢ φ \to D \in ∞Met (X)$
3	1 2	lmmbr	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x))$
4		df-3an	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
5		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
6		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
7		reseq2	$⊢ y = ℤ_{\geq j} \to {F ↾}_{y} = {F ↾}_{ℤ_{\geq j}}$
8		id	$⊢ y = ℤ_{\geq j} \to y = ℤ_{\geq j}$
9	7 8	feq12d	$⊢ y = ℤ_{\geq j} \to (({F ↾}_{y}) : y ⟶ P ball (D) x \leftrightarrow ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ P ball (D) x)$
10	9	rexrn	$⊢ ℤ_{\geq} Fn ℤ \to (\exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \leftrightarrow \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ P ball (D) x)$
11	5 6 10	mp2b	$⊢ \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \leftrightarrow \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ P ball (D) x$
12		simp2l	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to F \in (X ↑_{𝑝𝑚} ℂ)$
13		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
14	13	3ad2ant1	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to X \in dom ∞Met$
15		cnex	$⊢ ℂ \in V$
16		elpmg	$⊢ (X \in dom ∞Met \land ℂ \in V) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
17	14 15 16	sylancl	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
18	12 17	mpbid	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to (Fun F \land F \subseteq ℂ \times X)$
19	18	simpld	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to Fun F$
20		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ P ball (D) x \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (P ball (D) x)))$
21	19 20	syl	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ P ball (D) x \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (P ball (D) x)))$
22		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
23		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land x \in ℝ^{*}) \to (F (k) \in (P ball (D) x) \leftrightarrow (F (k) \in X \land P D F (k) < x))$
24	22 23	syl3an3	$⊢ (D \in ∞Met (X) \land P \in X \land x \in ℝ^{+}) \to (F (k) \in (P ball (D) x) \leftrightarrow (F (k) \in X \land P D F (k) < x))$
25		xmetsym	$⊢ (D \in ∞Met (X) \land P \in X \land F (k) \in X) \to P D F (k) = F (k) D P$
26	25	breq1d	$⊢ (D \in ∞Met (X) \land P \in X \land F (k) \in X) \to (P D F (k) < x \leftrightarrow F (k) D P < x)$
27	26	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land F (k) \in X) \to (P D F (k) < x \leftrightarrow F (k) D P < x)$
28	27	pm5.32da	$⊢ (D \in ∞Met (X) \land P \in X) \to ((F (k) \in X \land P D F (k) < x) \leftrightarrow (F (k) \in X \land F (k) D P < x))$
29	28	3adant3	$⊢ (D \in ∞Met (X) \land P \in X \land x \in ℝ^{+}) \to ((F (k) \in X \land P D F (k) < x) \leftrightarrow (F (k) \in X \land F (k) D P < x))$
30	24 29	bitrd	$⊢ (D \in ∞Met (X) \land P \in X \land x \in ℝ^{+}) \to (F (k) \in (P ball (D) x) \leftrightarrow (F (k) \in X \land F (k) D P < x))$
31	30	3adant2l	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to (F (k) \in (P ball (D) x) \leftrightarrow (F (k) \in X \land F (k) D P < x))$
32	31	anbi2d	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to ((k \in dom F \land F (k) \in (P ball (D) x)) \leftrightarrow (k \in dom F \land (F (k) \in X \land F (k) D P < x)))$
33		3anass	$⊢ (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))$
34	32 33	bitr4di	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to ((k \in dom F \land F (k) \in (P ball (D) x)) \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D P < x))$
35	34	ralbidv	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (P ball (D) x)) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
36	21 35	bitrd	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ P ball (D) x \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
37	36	rexbidv	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to (\exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ P ball (D) x \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
38	11 37	syl5bb	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land x \in ℝ^{+}) \to (\exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
39	38	3expa	$⊢ ((D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \land x \in ℝ^{+}) \to (\exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
40	39	ralbidva	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to (\forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
41	40	pm5.32da	$⊢ D \in ∞Met (X) \to (((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$
42	2 41	syl	$⊢ φ \to (((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$
43	4 42	syl5bb	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$
44		df-3an	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in ℤ \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 ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
45	43 44	bitr4di	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$
46	3 45	bitrd	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$

Metamath Proof Explorer

Theorem lmmbr2

Proof