iscmet3

Description: The property " D is a complete metric" expressed in terms of functions on NN (or any other upper integer set). Thus, we only have to look at functions on NN , and not all possible Cauchy filters, to determine completeness. (The proof uses countable choice.) (Contributed by NM, 18-Dec-2006) (Revised by Mario Carneiro, 5-May-2014)

	Ref	Expression
Hypotheses	iscmet3.1	$⊢ Z = ℤ_{\geq M}$
	iscmet3.2	$⊢ J = MetOpen (D)$
	iscmet3.3	$⊢ φ \to M \in ℤ$
	iscmet3.4	$⊢ φ \to D \in Met (X)$
Assertion	iscmet3	$⊢ φ \to (D \in CMet (X) \leftrightarrow \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J)))$

Proof

Step	Hyp	Ref	Expression
1		iscmet3.1	$⊢ Z = ℤ_{\geq M}$
2		iscmet3.2	$⊢ J = MetOpen (D)$
3		iscmet3.3	$⊢ φ \to M \in ℤ$
4		iscmet3.4	$⊢ φ \to D \in Met (X)$
5	2	cmetcau	$⊢ (D \in CMet (X) \land f \in Cau (D)) \to f \in dom \underset{t}{⇝} (J)$
6	5	a1d	$⊢ (D \in CMet (X) \land f \in Cau (D)) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))$
7	6	ralrimiva	$⊢ D \in CMet (X) \to \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))$
8	4	adantr	$⊢ (φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \to D \in Met (X)$
9		simpr	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land g \in CauFil (D)) \to g \in CauFil (D)$
10		1rp	$⊢ 1 \in ℝ^{+}$
11		rphalfcl	$⊢ 1 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
12	10 11	ax-mp	$⊢ \frac{1}{2} \in ℝ^{+}$
13		rpexpcl	$⊢ (\frac{1}{2} \in ℝ^{+} \land k \in ℤ) \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
14	12 13	mpan	$⊢ k \in ℤ \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
15		cfili	$⊢ (g \in CauFil (D) \land {(\frac{1}{2})}^{k} \in ℝ^{+}) \to \exists t \in g \forall u \in t \forall v \in t u D v < {(\frac{1}{2})}^{k}$
16	9 14 15	syl2an	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land g \in CauFil (D)) \land k \in ℤ) \to \exists t \in g \forall u \in t \forall v \in t u D v < {(\frac{1}{2})}^{k}$
17	16	ralrimiva	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land g \in CauFil (D)) \to \forall k \in ℤ \exists t \in g \forall u \in t \forall v \in t u D v < {(\frac{1}{2})}^{k}$
18		vex	$⊢ g \in V$
19		znnen	$⊢ ℤ \approx ℕ$
20		nnenom	$⊢ ℕ \approx ω$
21	19 20	entri	$⊢ ℤ \approx ω$
22		raleq	$⊢ t = s (k) \to (\forall v \in t u D v < {(\frac{1}{2})}^{k} \leftrightarrow \forall v \in s (k) u D v < {(\frac{1}{2})}^{k})$
23	22	raleqbi1dv	$⊢ t = s (k) \to (\forall u \in t \forall v \in t u D v < {(\frac{1}{2})}^{k} \leftrightarrow \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k})$
24	18 21 23	axcc4	$⊢ \forall k \in ℤ \exists t \in g \forall u \in t \forall v \in t u D v < {(\frac{1}{2})}^{k} \to \exists s (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k})$
25	17 24	syl	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land g \in CauFil (D)) \to \exists s (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k})$
26	3	ad2antrr	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to M \in ℤ$
27	1	uzenom	$⊢ M \in ℤ \to Z \approx ω$
28		endom	$⊢ Z \approx ω \to Z ≼ ω$
29	26 27 28	3syl	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to Z ≼ ω$
30		dfin5	$⊢ I (X) \cap ⋂_{n = M}^{k} s (n) = \{x \in I (X) \| x \in ⋂_{n = M}^{k} s (n)\}$
31		fzn0	$⊢ (M \dots k) \neq \emptyset \leftrightarrow k \in ℤ_{\geq M}$
32	31	biimpri	$⊢ k \in ℤ_{\geq M} \to (M \dots k) \neq \emptyset$
33	32 1	eleq2s	$⊢ k \in Z \to (M \dots k) \neq \emptyset$
34		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
35	4 34	syl	$⊢ φ \to D \in ∞Met (X)$
36	35	adantr	$⊢ (φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \to D \in ∞Met (X)$
37		simpl	$⊢ (g \in CauFil (D) \land s : ℤ ⟶ g) \to g \in CauFil (D)$
38		cfilfil	$⊢ (D \in ∞Met (X) \land g \in CauFil (D)) \to g \in Fil (X)$
39	36 37 38	syl2an	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \to g \in Fil (X)$
40		simprr	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \to s : ℤ ⟶ g$
41		elfzelz	$⊢ n \in (M \dots k) \to n \in ℤ$
42		ffvelcdm	$⊢ (s : ℤ ⟶ g \land n \in ℤ) \to s (n) \in g$
43	40 41 42	syl2an	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land n \in (M \dots k)) \to s (n) \in g$
44		filelss	$⊢ (g \in Fil (X) \land s (n) \in g) \to s (n) \subseteq X$
45	39 43 44	syl2an2r	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land n \in (M \dots k)) \to s (n) \subseteq X$
46	45	ralrimiva	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \to \forall n \in (M \dots k) s (n) \subseteq X$
47		r19.2z	$⊢ ((M \dots k) \neq \emptyset \land \forall n \in (M \dots k) s (n) \subseteq X) \to \exists n \in (M \dots k) s (n) \subseteq X$
48	33 46 47	syl2anr	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to \exists n \in (M \dots k) s (n) \subseteq X$
49		iinss	$⊢ \exists n \in (M \dots k) s (n) \subseteq X \to ⋂_{n = M}^{k} s (n) \subseteq X$
50	48 49	syl	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to ⋂_{n = M}^{k} s (n) \subseteq X$
51	8	ad2antrr	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to D \in Met (X)$
52		elfvdm	$⊢ D \in Met (X) \to X \in dom Met$
53		fvi	$⊢ X \in dom Met \to I (X) = X$
54	51 52 53	3syl	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to I (X) = X$
55	50 54	sseqtrrd	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to ⋂_{n = M}^{k} s (n) \subseteq I (X)$
56		sseqin2	$⊢ ⋂_{n = M}^{k} s (n) \subseteq I (X) \leftrightarrow I (X) \cap ⋂_{n = M}^{k} s (n) = ⋂_{n = M}^{k} s (n)$
57	55 56	sylib	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to I (X) \cap ⋂_{n = M}^{k} s (n) = ⋂_{n = M}^{k} s (n)$
58	30 57	eqtr3id	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to \{x \in I (X) \| x \in ⋂_{n = M}^{k} s (n)\} = ⋂_{n = M}^{k} s (n)$
59	39	adantr	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to g \in Fil (X)$
60	43	ralrimiva	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \to \forall n \in (M \dots k) s (n) \in g$
61	60	adantr	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to \forall n \in (M \dots k) s (n) \in g$
62	33	adantl	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to (M \dots k) \neq \emptyset$
63		fzfid	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to (M \dots k) \in Fin$
64		iinfi	$⊢ (g \in Fil (X) \land (\forall n \in (M \dots k) s (n) \in g \land (M \dots k) \neq \emptyset \land (M \dots k) \in Fin)) \to ⋂_{n = M}^{k} s (n) \in fi (g)$
65	59 61 62 63 64	syl13anc	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to ⋂_{n = M}^{k} s (n) \in fi (g)$
66		filfi	$⊢ g \in Fil (X) \to fi (g) = g$
67	59 66	syl	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to fi (g) = g$
68	65 67	eleqtrd	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to ⋂_{n = M}^{k} s (n) \in g$
69		fileln0	$⊢ (g \in Fil (X) \land ⋂_{n = M}^{k} s (n) \in g) \to ⋂_{n = M}^{k} s (n) \neq \emptyset$
70	39 68 69	syl2an2r	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to ⋂_{n = M}^{k} s (n) \neq \emptyset$
71	58 70	eqnetrd	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to \{x \in I (X) \| x \in ⋂_{n = M}^{k} s (n)\} \neq \emptyset$
72		rabn0	$⊢ \{x \in I (X) \| x \in ⋂_{n = M}^{k} s (n)\} \neq \emptyset \leftrightarrow \exists x \in I (X) x \in ⋂_{n = M}^{k} s (n)$
73	71 72	sylib	$⊢ (((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \land k \in Z) \to \exists x \in I (X) x \in ⋂_{n = M}^{k} s (n)$
74	73	ralrimiva	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land s : ℤ ⟶ g)) \to \forall k \in Z \exists x \in I (X) x \in ⋂_{n = M}^{k} s (n)$
75	74	adantrrr	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to \forall k \in Z \exists x \in I (X) x \in ⋂_{n = M}^{k} s (n)$
76		fvex	$⊢ I (X) \in V$
77		eleq1	$⊢ x = f (k) \to (x \in ⋂_{n = M}^{k} s (n) \leftrightarrow f (k) \in ⋂_{n = M}^{k} s (n))$
78		fvex	$⊢ f (k) \in V$
79		eliin	$⊢ f (k) \in V \to (f (k) \in ⋂_{n = M}^{k} s (n) \leftrightarrow \forall n \in (M \dots k) f (k) \in s (n))$
80	78 79	ax-mp	$⊢ f (k) \in ⋂_{n = M}^{k} s (n) \leftrightarrow \forall n \in (M \dots k) f (k) \in s (n)$
81	77 80	bitrdi	$⊢ x = f (k) \to (x \in ⋂_{n = M}^{k} s (n) \leftrightarrow \forall n \in (M \dots k) f (k) \in s (n))$
82	76 81	axcc4dom	$⊢ (Z ≼ ω \land \forall k \in Z \exists x \in I (X) x \in ⋂_{n = M}^{k} s (n)) \to \exists f (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n))$
83	29 75 82	syl2anc	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to \exists f (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n))$
84		df-ral	$⊢ \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J)) \leftrightarrow \forall f (f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J)))$
85		19.29	$⊢ (\forall f (f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land \exists f (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n))) \to \exists f ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))$
86	84 85	sylanb	$⊢ (\forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J)) \land \exists f (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n))) \to \exists f ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))$
87	3	ad2antrr	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to M \in ℤ$
88	4	ad2antrr	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to D \in Met (X)$
89		simprrl	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to f : Z ⟶ I (X)$
90		feq3	$⊢ I (X) = X \to (f : Z ⟶ I (X) \leftrightarrow f : Z ⟶ X)$
91	88 52 53 90	4syl	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to (f : Z ⟶ I (X) \leftrightarrow f : Z ⟶ X)$
92	89 91	mpbid	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to f : Z ⟶ X$
93		simplrr	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k})$
94	93	simprd	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}$
95		fveq2	$⊢ k = i \to s (k) = s (i)$
96		oveq2	$⊢ k = i \to {(\frac{1}{2})}^{k} = {(\frac{1}{2})}^{i}$
97	96	breq2d	$⊢ k = i \to (u D v < {(\frac{1}{2})}^{k} \leftrightarrow u D v < {(\frac{1}{2})}^{i})$
98	95 97	raleqbidv	$⊢ k = i \to (\forall v \in s (k) u D v < {(\frac{1}{2})}^{k} \leftrightarrow \forall v \in s (i) u D v < {(\frac{1}{2})}^{i})$
99	95 98	raleqbidv	$⊢ k = i \to (\forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k} \leftrightarrow \forall u \in s (i) \forall v \in s (i) u D v < {(\frac{1}{2})}^{i})$
100	99	cbvralvw	$⊢ \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k} \leftrightarrow \forall i \in ℤ \forall u \in s (i) \forall v \in s (i) u D v < {(\frac{1}{2})}^{i}$
101	94 100	sylib	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to \forall i \in ℤ \forall u \in s (i) \forall v \in s (i) u D v < {(\frac{1}{2})}^{i}$
102		simprrr	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)$
103		fveq2	$⊢ n = j \to s (n) = s (j)$
104	103	eleq2d	$⊢ n = j \to (f (k) \in s (n) \leftrightarrow f (k) \in s (j))$
105	104	cbvralvw	$⊢ \forall n \in (M \dots k) f (k) \in s (n) \leftrightarrow \forall j \in (M \dots k) f (k) \in s (j)$
106		oveq2	$⊢ k = i \to (M \dots k) = (M \dots i)$
107		fveq2	$⊢ k = i \to f (k) = f (i)$
108	107	eleq1d	$⊢ k = i \to (f (k) \in s (j) \leftrightarrow f (i) \in s (j))$
109	106 108	raleqbidv	$⊢ k = i \to (\forall j \in (M \dots k) f (k) \in s (j) \leftrightarrow \forall j \in (M \dots i) f (i) \in s (j))$
110	105 109	bitrid	$⊢ k = i \to (\forall n \in (M \dots k) f (k) \in s (n) \leftrightarrow \forall j \in (M \dots i) f (i) \in s (j))$
111	110	cbvralvw	$⊢ \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n) \leftrightarrow \forall i \in Z \forall j \in (M \dots i) f (i) \in s (j)$
112	102 111	sylib	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to \forall i \in Z \forall j \in (M \dots i) f (i) \in s (j)$
113	88 34	syl	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to D \in ∞Met (X)$
114		simplrl	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to g \in CauFil (D)$
115	113 114 38	syl2anc	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to g \in Fil (X)$
116	93	simpld	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to s : ℤ ⟶ g$
117	1 2 87 88 92 101 112	iscmet3lem1	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to f \in Cau (D)$
118		simprl	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to (f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J)))$
119	117 92 118	mp2d	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to f \in dom \underset{t}{⇝} (J)$
120	1 2 87 88 92 101 112 115 116 119	iscmet3lem2	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)))) \to J fLim g \neq \emptyset$
121	120	ex	$⊢ (φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to (((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n))) \to J fLim g \neq \emptyset)$
122	121	exlimdv	$⊢ (φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to (\exists f ((f \in Cau (D) \to (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n))) \to J fLim g \neq \emptyset)$
123	86 122	syl5	$⊢ (φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to ((\forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J)) \land \exists f (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n))) \to J fLim g \neq \emptyset)$
124	123	expdimp	$⊢ ((φ \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \to (\exists f (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)) \to J fLim g \neq \emptyset)$
125	124	an32s	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to (\exists f (f : Z ⟶ I (X) \land \forall k \in Z \forall n \in (M \dots k) f (k) \in s (n)) \to J fLim g \neq \emptyset)$
126	83 125	mpd	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land (g \in CauFil (D) \land (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}))) \to J fLim g \neq \emptyset$
127	126	expr	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land g \in CauFil (D)) \to ((s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}) \to J fLim g \neq \emptyset)$
128	127	exlimdv	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land g \in CauFil (D)) \to (\exists s (s : ℤ ⟶ g \land \forall k \in ℤ \forall u \in s (k) \forall v \in s (k) u D v < {(\frac{1}{2})}^{k}) \to J fLim g \neq \emptyset)$
129	25 128	mpd	$⊢ ((φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \land g \in CauFil (D)) \to J fLim g \neq \emptyset$
130	129	ralrimiva	$⊢ (φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \to \forall g \in CauFil (D) J fLim g \neq \emptyset$
131	2	iscmet	$⊢ D \in CMet (X) \leftrightarrow (D \in Met (X) \land \forall g \in CauFil (D) J fLim g \neq \emptyset)$
132	8 130 131	sylanbrc	$⊢ (φ \land \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J))) \to D \in CMet (X)$
133	132	ex	$⊢ φ \to (\forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J)) \to D \in CMet (X))$
134	7 133	impbid2	$⊢ φ \to (D \in CMet (X) \leftrightarrow \forall f \in Cau (D) (f : Z ⟶ X \to f \in dom \underset{t}{⇝} (J)))$

Metamath Proof Explorer

Theorem iscmet3

Proof