lmmbr

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 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	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))$

Proof

Step	Hyp	Ref	Expression
1		lmmbr.2	$⊢ J = MetOpen (D)$
2		lmmbr.3	$⊢ φ \to D \in ∞Met (X)$
3	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
4	2 3	syl	$⊢ φ \to J \in TopOn (X)$
5	4	lmbr	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)))$
6		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
7	1	blopn	$⊢ (D \in ∞Met (X) \land P \in X \land x \in ℝ^{*}) \to P ball (D) x \in J$
8	6 7	syl3an3	$⊢ (D \in ∞Met (X) \land P \in X \land x \in ℝ^{+}) \to P ball (D) x \in J$
9		blcntr	$⊢ (D \in ∞Met (X) \land P \in X \land x \in ℝ^{+}) \to P \in (P ball (D) x)$
10		eleq2	$⊢ u = P ball (D) x \to (P \in u \leftrightarrow P \in (P ball (D) x))$
11		feq3	$⊢ u = P ball (D) x \to (({F ↾}_{y}) : y ⟶ u \leftrightarrow ({F ↾}_{y}) : y ⟶ P ball (D) x)$
12	11	rexbidv	$⊢ u = P ball (D) x \to (\exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u \leftrightarrow \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
13	10 12	imbi12d	$⊢ u = P ball (D) x \to ((P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u) \leftrightarrow (P \in (P ball (D) x) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x))$
14	13	rspcva	$⊢ (P ball (D) x \in J \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)) \to (P \in (P ball (D) x) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
15	14	impancom	$⊢ (P ball (D) x \in J \land P \in (P ball (D) x)) \to (\forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
16	8 9 15	syl2anc	$⊢ (D \in ∞Met (X) \land P \in X \land x \in ℝ^{+}) \to (\forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
17	16	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land x \in ℝ^{+}) \to (\forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
18	17	adantlrl	$⊢ ((D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \land x \in ℝ^{+}) \to (\forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
19	18	impancom	$⊢ ((D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)) \to (x \in ℝ^{+} \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
20	19	ralrimiv	$⊢ ((D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)) \to \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x$
21	1	mopni2	$⊢ (D \in ∞Met (X) \land u \in J \land P \in u) \to \exists x \in ℝ^{+} P ball (D) x \subseteq u$
22		r19.29	$⊢ (\forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \land \exists x \in ℝ^{+} P ball (D) x \subseteq u) \to \exists x \in ℝ^{+} (\exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \land P ball (D) x \subseteq u)$
23		fss	$⊢ (({F ↾}_{y}) : y ⟶ P ball (D) x \land P ball (D) x \subseteq u) \to ({F ↾}_{y}) : y ⟶ u$
24	23	expcom	$⊢ P ball (D) x \subseteq u \to (({F ↾}_{y}) : y ⟶ P ball (D) x \to ({F ↾}_{y}) : y ⟶ u)$
25	24	reximdv	$⊢ P ball (D) x \subseteq u \to (\exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)$
26	25	impcom	$⊢ (\exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \land P ball (D) x \subseteq u) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u$
27	26	rexlimivw	$⊢ \exists x \in ℝ^{+} (\exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \land P ball (D) x \subseteq u) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u$
28	22 27	syl	$⊢ (\forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \land \exists x \in ℝ^{+} P ball (D) x \subseteq u) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u$
29	21 28	sylan2	$⊢ (\forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \land (D \in ∞Met (X) \land u \in J \land P \in u)) \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u$
30	29	3exp2	$⊢ \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x \to (D \in ∞Met (X) \to (u \in J \to (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)))$
31	30	impcom	$⊢ (D \in ∞Met (X) \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x) \to (u \in J \to (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u))$
32	31	adantlr	$⊢ ((D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x) \to (u \in J \to (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u))$
33	32	ralrimiv	$⊢ ((D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x) \to \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)$
34	20 33	impbida	$⊢ (D \in ∞Met (X) \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to (\forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u) \leftrightarrow \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x)$
35	34	pm5.32da	$⊢ D \in ∞Met (X) \to (((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x))$
36		df-3an	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u))$
37		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)$
38	35 36 37	3bitr4g	$⊢ D \in ∞Met (X) \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x))$
39	2 38	syl	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ P ball (D) x))$
40	5 39	bitrd	$⊢ φ \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))$

Metamath Proof Explorer

Theorem lmmbr

Proof