lmfval

Description: The relation "sequence f converges to point y " in a metric space. (Contributed by NM, 7-Sep-2006) (Revised by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	lmfval	$⊢ J \in TopOn (X) \to \underset{t}{⇝} (J) = \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$

Proof

Step	Hyp	Ref	Expression
1		df-lm	$⊢ \underset{t}{⇝} = (j \in Top ⟼ \{⟨f, x⟩ \| (f \in (⋃ j ↑_{𝑝𝑚} ℂ) \land x \in ⋃ j \land \forall u \in j (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\})$
2		simpr	$⊢ (J \in TopOn (X) \land j = J) \to j = J$
3	2	unieqd	$⊢ (J \in TopOn (X) \land j = J) \to ⋃ j = ⋃ J$
4		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
5	4	adantr	$⊢ (J \in TopOn (X) \land j = J) \to X = ⋃ J$
6	3 5	eqtr4d	$⊢ (J \in TopOn (X) \land j = J) \to ⋃ j = X$
7	6	oveq1d	$⊢ (J \in TopOn (X) \land j = J) \to ⋃ j ↑_{𝑝𝑚} ℂ = X ↑_{𝑝𝑚} ℂ$
8	7	eleq2d	$⊢ (J \in TopOn (X) \land j = J) \to (f \in (⋃ j ↑_{𝑝𝑚} ℂ) \leftrightarrow f \in (X ↑_{𝑝𝑚} ℂ))$
9	6	eleq2d	$⊢ (J \in TopOn (X) \land j = J) \to (x \in ⋃ j \leftrightarrow x \in X)$
10	2	raleqdv	$⊢ (J \in TopOn (X) \land j = J) \to (\forall u \in j (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u) \leftrightarrow \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))$
11	8 9 10	3anbi123d	$⊢ (J \in TopOn (X) \land j = J) \to ((f \in (⋃ j ↑_{𝑝𝑚} ℂ) \land x \in ⋃ j \land \forall u \in j (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u)) \leftrightarrow (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u)))$
12	11	opabbidv	$⊢ (J \in TopOn (X) \land j = J) \to \{⟨f, x⟩ \| (f \in (⋃ j ↑_{𝑝𝑚} ℂ) \land x \in ⋃ j \land \forall u \in j (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} = \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$
13		topontop	$⊢ J \in TopOn (X) \to J \in Top$
14		df-3an	$⊢ (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u)) \leftrightarrow ((f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X) \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))$
15	14	opabbii	$⊢ \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} = \{⟨f, x⟩ \| ((f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X) \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$
16		opabssxp	$⊢ \{⟨f, x⟩ \| ((f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X) \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} \subseteq (X ↑_{𝑝𝑚} ℂ) \times X$
17	15 16	eqsstri	$⊢ \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} \subseteq (X ↑_{𝑝𝑚} ℂ) \times X$
18		ovex	$⊢ X ↑_{𝑝𝑚} ℂ \in V$
19		toponmax	$⊢ J \in TopOn (X) \to X \in J$
20		xpexg	$⊢ (X ↑_{𝑝𝑚} ℂ \in V \land X \in J) \to (X ↑_{𝑝𝑚} ℂ) \times X \in V$
21	18 19 20	sylancr	$⊢ J \in TopOn (X) \to (X ↑_{𝑝𝑚} ℂ) \times X \in V$
22		ssexg	$⊢ (\{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} \subseteq (X ↑_{𝑝𝑚} ℂ) \times X \land (X ↑_{𝑝𝑚} ℂ) \times X \in V) \to \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} \in V$
23	17 21 22	sylancr	$⊢ J \in TopOn (X) \to \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\} \in V$
24	1 12 13 23	fvmptd2	$⊢ J \in TopOn (X) \to \underset{t}{⇝} (J) = \{⟨f, x⟩ \| (f \in (X ↑_{𝑝𝑚} ℂ) \land x \in X \land \forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u))\}$

Metamath Proof Explorer

Theorem lmfval

Proof