iscau2

Description: Express the property " F is a Cauchy sequence of metric D " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

		Ref	Expression
	Assertion	iscau2	$⊢ D \in ∞Met (X) \to (F \in Cau (D) \leftrightarrow (F \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 F (j) < x)))$

Proof

Step	Hyp	Ref	Expression
1		iscau	$⊢ D \in ∞Met (X) \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ F (j) ball (D) x))$
2		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
3		cnex	$⊢ ℂ \in V$
4		elpmg	$⊢ (X \in dom ∞Met \land ℂ \in V) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
5	2 3 4	sylancl	$⊢ D \in ∞Met (X) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
6	5	simprbda	$⊢ (D \in ∞Met (X) \land F \in (X ↑_{𝑝𝑚} ℂ)) \to Fun F$
7		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ F (j) ball (D) x \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)))$
8	6 7	syl	$⊢ (D \in ∞Met (X) \land F \in (X ↑_{𝑝𝑚} ℂ)) \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ F (j) ball (D) x \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)))$
9	8	rexbidv	$⊢ (D \in ∞Met (X) \land F \in (X ↑_{𝑝𝑚} ℂ)) \to (\exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ F (j) ball (D) x \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)))$
10	9	adantr	$⊢ ((D \in ∞Met (X) \land F \in (X ↑_{𝑝𝑚} ℂ)) \land x \in ℝ^{+}) \to (\exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ F (j) ball (D) x \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)))$
11		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
12	11	adantl	$⊢ ((D \in ∞Met (X) \land x \in ℝ^{+}) \land j \in ℤ) \to j \in ℤ_{\geq j}$
13		eleq1w	$⊢ k = j \to (k \in dom F \leftrightarrow j \in dom F)$
14		fveq2	$⊢ k = j \to F (k) = F (j)$
15	14	eleq1d	$⊢ k = j \to (F (k) \in (F (j) ball (D) x) \leftrightarrow F (j) \in (F (j) ball (D) x))$
16	13 15	anbi12d	$⊢ k = j \to ((k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow (j \in dom F \land F (j) \in (F (j) ball (D) x)))$
17	16	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \to (j \in dom F \land F (j) \in (F (j) ball (D) x)))$
18	12 17	syl	$⊢ ((D \in ∞Met (X) \land x \in ℝ^{+}) \land j \in ℤ) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \to (j \in dom F \land F (j) \in (F (j) ball (D) x)))$
19		n0i	$⊢ F (j) \in (F (j) ball (D) x) \to \neg F (j) ball (D) x = \emptyset$
20		blf	$⊢ D \in ∞Met (X) \to ball (D) : X \times ℝ^{*} ⟶ 𝒫 X$
21	20	fdmd	$⊢ D \in ∞Met (X) \to dom ball (D) = X \times ℝ^{*}$
22		ndmovg	$⊢ (dom ball (D) = X \times ℝ^{} \land \neg (F (j) \in X \land x \in ℝ^{})) \to F (j) ball (D) x = \emptyset$
23	22	ex	$⊢ dom ball (D) = X \times ℝ^{} \to (\neg (F (j) \in X \land x \in ℝ^{}) \to F (j) ball (D) x = \emptyset)$
24	21 23	syl	$⊢ D \in ∞Met (X) \to (\neg (F (j) \in X \land x \in ℝ^{*}) \to F (j) ball (D) x = \emptyset)$
25	24	con1d	$⊢ D \in ∞Met (X) \to (\neg F (j) ball (D) x = \emptyset \to (F (j) \in X \land x \in ℝ^{*}))$
26		simpl	$⊢ (F (j) \in X \land x \in ℝ^{*}) \to F (j) \in X$
27	19 25 26	syl56	$⊢ D \in ∞Met (X) \to (F (j) \in (F (j) ball (D) x) \to F (j) \in X)$
28	27	adantld	$⊢ D \in ∞Met (X) \to ((j \in dom F \land F (j) \in (F (j) ball (D) x)) \to F (j) \in X)$
29	28	ad2antrr	$⊢ ((D \in ∞Met (X) \land x \in ℝ^{+}) \land j \in ℤ) \to ((j \in dom F \land F (j) \in (F (j) ball (D) x)) \to F (j) \in X)$
30	18 29	syld	$⊢ ((D \in ∞Met (X) \land x \in ℝ^{+}) \land j \in ℤ) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \to F (j) \in X)$
31	14	eleq1d	$⊢ k = j \to (F (k) \in X \leftrightarrow F (j) \in X)$
32	14	oveq1d	$⊢ k = j \to F (k) D F (j) = F (j) D F (j)$
33	32	breq1d	$⊢ k = j \to (F (k) D F (j) < x \leftrightarrow F (j) D F (j) < x)$
34	13 31 33	3anbi123d	$⊢ k = j \to ((k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow (j \in dom F \land F (j) \in X \land F (j) D F (j) < x))$
35	34	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to (j \in dom F \land F (j) \in X \land F (j) D F (j) < x))$
36	12 35	syl	$⊢ ((D \in ∞Met (X) \land x \in ℝ^{+}) \land j \in ℤ) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to (j \in dom F \land F (j) \in X \land F (j) D F (j) < x))$
37		simp2	$⊢ (j \in dom F \land F (j) \in X \land F (j) D F (j) < x) \to F (j) \in X$
38	36 37	syl6	$⊢ ((D \in ∞Met (X) \land x \in ℝ^{+}) \land j \in ℤ) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to F (j) \in X)$
39		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
40		elbl	$⊢ (D \in ∞Met (X) \land F (j) \in X \land x \in ℝ^{*}) \to (F (k) \in (F (j) ball (D) x) \leftrightarrow (F (k) \in X \land F (j) D F (k) < x))$
41	39 40	syl3an3	$⊢ (D \in ∞Met (X) \land F (j) \in X \land x \in ℝ^{+}) \to (F (k) \in (F (j) ball (D) x) \leftrightarrow (F (k) \in X \land F (j) D F (k) < x))$
42		xmetsym	$⊢ (D \in ∞Met (X) \land F (j) \in X \land F (k) \in X) \to F (j) D F (k) = F (k) D F (j)$
43	42	3expa	$⊢ ((D \in ∞Met (X) \land F (j) \in X) \land F (k) \in X) \to F (j) D F (k) = F (k) D F (j)$
44	43	3adantl3	$⊢ ((D \in ∞Met (X) \land F (j) \in X \land x \in ℝ^{+}) \land F (k) \in X) \to F (j) D F (k) = F (k) D F (j)$
45	44	breq1d	$⊢ ((D \in ∞Met (X) \land F (j) \in X \land x \in ℝ^{+}) \land F (k) \in X) \to (F (j) D F (k) < x \leftrightarrow F (k) D F (j) < x)$
46	45	pm5.32da	$⊢ (D \in ∞Met (X) \land F (j) \in X \land x \in ℝ^{+}) \to ((F (k) \in X \land F (j) D F (k) < x) \leftrightarrow (F (k) \in X \land F (k) D F (j) < x))$
47	41 46	bitrd	$⊢ (D \in ∞Met (X) \land F (j) \in X \land x \in ℝ^{+}) \to (F (k) \in (F (j) ball (D) x) \leftrightarrow (F (k) \in X \land F (k) D F (j) < x))$
48	47	3com23	$⊢ (D \in ∞Met (X) \land x \in ℝ^{+} \land F (j) \in X) \to (F (k) \in (F (j) ball (D) x) \leftrightarrow (F (k) \in X \land F (k) D F (j) < x))$
49	48	anbi2d	$⊢ (D \in ∞Met (X) \land x \in ℝ^{+} \land F (j) \in X) \to ((k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow (k \in dom F \land (F (k) \in X \land F (k) D F (j) < x)))$
50		3anass	$⊢ (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow (k \in dom F \land (F (k) \in X \land F (k) D F (j) < x))$
51	49 50	bitr4di	$⊢ (D \in ∞Met (X) \land x \in ℝ^{+} \land F (j) \in X) \to ((k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
52	51	ralbidv	$⊢ (D \in ∞Met (X) \land x \in ℝ^{+} \land F (j) \in X) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
53	52	3expia	$⊢ (D \in ∞Met (X) \land x \in ℝ^{+}) \to (F (j) \in X \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
54	53	adantr	$⊢ ((D \in ∞Met (X) \land x \in ℝ^{+}) \land j \in ℤ) \to (F (j) \in X \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
55	30 38 54	pm5.21ndd	$⊢ ((D \in ∞Met (X) \land x \in ℝ^{+}) \land j \in ℤ) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
56	55	rexbidva	$⊢ (D \in ∞Met (X) \land x \in ℝ^{+}) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
57	56	adantlr	$⊢ ((D \in ∞Met (X) \land F \in (X ↑_{𝑝𝑚} ℂ)) \land x \in ℝ^{+}) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (F (j) ball (D) x)) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
58	10 57	bitrd	$⊢ ((D \in ∞Met (X) \land F \in (X ↑_{𝑝𝑚} ℂ)) \land x \in ℝ^{+}) \to (\exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ F (j) ball (D) x \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
59	58	ralbidva	$⊢ (D \in ∞Met (X) \land F \in (X ↑_{𝑝𝑚} ℂ)) \to (\forall x \in ℝ^{+} \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ F (j) ball (D) 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 F (j) < x))$
60	59	pm5.32da	$⊢ D \in ∞Met (X) \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in ℤ ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ F (j) ball (D) x) \leftrightarrow (F \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 F (j) < x)))$
61	1 60	bitrd	$⊢ D \in ∞Met (X) \to (F \in Cau (D) \leftrightarrow (F \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 F (j) < x)))$

Metamath Proof Explorer

Theorem iscau2

Proof