Metamath Proof Explorer

Theorem lmmbr3

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

		Ref	Expression
	Hypotheses	lmmbr.2	$⊢ J = MetOpen (D)$
		lmmbr.3	$⊢ φ \to D \in ∞Met (X)$
		lmmbr3.5	$⊢ Z = ℤ_{\geq M}$
		lmmbr3.6	$⊢ φ \to M \in ℤ$
	Assertion	lmmbr3	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in Z \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		lmmbr3.5	$⊢ Z = ℤ_{\geq M}$
4		lmmbr3.6	$⊢ φ \to M \in ℤ$
5	1 2	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)))$
6	3	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < 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))$
7	4 6	syl	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < 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))$
8	7	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < 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))$
9	8	3anbi3d	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in Z \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)))$
10	5 9	bitr4d	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$