lmbr

Description: Express the binary relation "sequence F converges to point P " in a topological 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 Mario Carneiro, 14-Nov-2013)

		Ref	Expression
	Hypothesis	lmbr.2	$⊢ φ \to J \in TopOn (X)$
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		lmbr.2	$⊢ φ \to J \in TopOn (X)$
2		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))\}$
3	1 2	syl	$⊢ φ \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))\}$
4	3	breqd	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow F \{⟨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))\} P)$
5		reseq1	$⊢ f = F \to {f ↾}_{y} = {F ↾}_{y}$
6	5	feq1d	$⊢ f = F \to (({f ↾}_{y}) : y ⟶ u \leftrightarrow ({F ↾}_{y}) : y ⟶ u)$
7	6	rexbidv	$⊢ f = F \to (\exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u \leftrightarrow \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)$
8	7	imbi2d	$⊢ f = F \to ((x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u) \leftrightarrow (x \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u))$
9	8	ralbidv	$⊢ f = F \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))$
10		eleq1	$⊢ x = P \to (x \in u \leftrightarrow P \in u)$
11	10	imbi1d	$⊢ x = P \to ((x \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u) \leftrightarrow (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u))$
12	11	ralbidv	$⊢ x = P \to (\forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u) \leftrightarrow \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u))$
13	9 12	sylan9bb	$⊢ (f = F \land x = P) \to (\forall u \in J (x \in u \to \exists y \in ran ℤ_{\geq} ({f ↾}_{y}) : y ⟶ u) \leftrightarrow \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u))$
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	13 15	brab2a	$⊢ F \{⟨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))\} 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))$
17		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))$
18	16 17	bitr4i	$⊢ F \{⟨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))\} 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))$
19	4 18	bitrdi	$⊢ φ \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)))$

Metamath Proof Explorer

Theorem lmbr

Proof