lmbr2

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Hypotheses	lmbr.2	$⊢ φ \to J \in TopOn (X)$
	lmbr2.4	$⊢ Z = ℤ_{\geq M}$
	lmbr2.5	$⊢ φ \to M \in ℤ$
Assertion	lmbr2	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$

Proof

Step	Hyp	Ref	Expression
1		lmbr.2	$⊢ φ \to J \in TopOn (X)$
2		lmbr2.4	$⊢ Z = ℤ_{\geq M}$
3		lmbr2.5	$⊢ φ \to M \in ℤ$
4	1	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 z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u)))$
5		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
6		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
7		reseq2	$⊢ z = ℤ_{\geq j} \to {F ↾}_{z} = {F ↾}_{ℤ_{\geq j}}$
8		id	$⊢ z = ℤ_{\geq j} \to z = ℤ_{\geq j}$
9	7 8	feq12d	$⊢ z = ℤ_{\geq j} \to (({F ↾}_{z}) : z ⟶ u \leftrightarrow ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ u)$
10	9	rexrn	$⊢ ℤ_{\geq} Fn ℤ \to (\exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u \leftrightarrow \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ u)$
11	5 6 10	mp2b	$⊢ \exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u \leftrightarrow \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ u$
12		pmfun	$⊢ F \in (X ↑_{𝑝𝑚} ℂ) \to Fun F$
13	12	ad2antrl	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to Fun F$
14		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ u \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
15	13 14	syl	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ u \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
16	15	rexbidv	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to (\exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ u \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
17	3	adantr	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to M \in ℤ$
18	2	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
19	17 18	syl	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
20	16 19	bitr4d	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to (\exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ u \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
21	11 20	syl5bb	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to (\exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
22	21	imbi2d	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to ((P \in u \to \exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u) \leftrightarrow (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
23	22	ralbidv	$⊢ (φ \land (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X)) \to (\forall u \in J (P \in u \to \exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u) \leftrightarrow \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
24	23	pm5.32da	$⊢ φ \to (((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall u \in J (P \in u \to \exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u)) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
25		df-3an	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u)) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall u \in J (P \in u \to \exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u))$
26		df-3an	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))) \leftrightarrow ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X) \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
27	24 25 26	3bitr4g	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists z \in ran ℤ_{\geq} ({F ↾}_{z}) : z ⟶ u)) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
28	4 27	bitrd	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$

Metamath Proof Explorer

Theorem lmbr2

Proof