caucfil

Description: A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	caucfil.1	$⊢ Z = ℤ_{\geq M}$
	caucfil.2	$⊢ L = (X FilMap F) (ℤ_{\geq} [Z])$
Assertion	caucfil	$⊢ (D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \to (F \in Cau (D) \leftrightarrow L \in CauFil (D))$

Proof

Step	Hyp	Ref	Expression
1		caucfil.1	$⊢ Z = ℤ_{\geq M}$
2		caucfil.2	$⊢ L = (X FilMap F) (ℤ_{\geq} [Z])$
3		df-3an	$⊢ (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x)$
4	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
5	4	adantll	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
6		simpll3	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to F : Z ⟶ X$
7	6	fdmd	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to dom F = Z$
8	5 7	eleqtrrd	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in dom F$
9	6 5	ffvelcdmd	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in X$
10	8 9	jca	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to (k \in dom F \land F (k) \in X)$
11	10	biantrurd	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to (\forall m \in ℤ_{\geq k} F (k) D F (m) < x \leftrightarrow ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x))$
12		uzss	$⊢ k \in ℤ_{\geq j} \to ℤ_{\geq k} \subseteq ℤ_{\geq j}$
13	12	adantl	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to ℤ_{\geq k} \subseteq ℤ_{\geq j}$
14	13	sseld	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to (m \in ℤ_{\geq k} \to m \in ℤ_{\geq j})$
15	14	pm4.71rd	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to (m \in ℤ_{\geq k} \leftrightarrow (m \in ℤ_{\geq j} \land m \in ℤ_{\geq k}))$
16	15	imbi1d	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to ((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \leftrightarrow ((m \in ℤ_{\geq j} \land m \in ℤ_{\geq k}) \to F (k) D F (m) < x))$
17		impexp	$⊢ ((m \in ℤ_{\geq j} \land m \in ℤ_{\geq k}) \to F (k) D F (m) < x) \leftrightarrow (m \in ℤ_{\geq j} \to (m \in ℤ_{\geq k} \to F (k) D F (m) < x))$
18	16 17	bitrdi	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to ((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \leftrightarrow (m \in ℤ_{\geq j} \to (m \in ℤ_{\geq k} \to F (k) D F (m) < x)))$
19	18	ralbidv2	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to (\forall m \in ℤ_{\geq k} F (k) D F (m) < x \leftrightarrow \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x))$
20	11 19	bitr3d	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to (((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x))$
21	3 20	bitrid	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land k \in ℤ_{\geq j}) \to ((k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x))$
22	21	ralbidva	$⊢ ((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x))$
23		r19.26-2	$⊢ \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} ((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land (k \in ℤ_{\geq m} \to F (m) D F (k) < x)) \leftrightarrow (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (k \in ℤ_{\geq m} \to F (m) D F (k) < x))$
24		eleq1w	$⊢ u = k \to (u \in ℤ_{\geq m} \leftrightarrow k \in ℤ_{\geq m})$
25		fveq2	$⊢ u = k \to F (u) = F (k)$
26	25	oveq2d	$⊢ u = k \to F (m) D F (u) = F (m) D F (k)$
27	26	breq1d	$⊢ u = k \to (F (m) D F (u) < x \leftrightarrow F (m) D F (k) < x)$
28	24 27	imbi12d	$⊢ u = k \to ((u \in ℤ_{\geq m} \to F (m) D F (u) < x) \leftrightarrow (k \in ℤ_{\geq m} \to F (m) D F (k) < x))$
29	28	cbvralvw	$⊢ \forall u \in ℤ_{\geq j} (u \in ℤ_{\geq m} \to F (m) D F (u) < x) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in ℤ_{\geq m} \to F (m) D F (k) < x)$
30	29	ralbii	$⊢ \forall m \in ℤ_{\geq j} \forall u \in ℤ_{\geq j} (u \in ℤ_{\geq m} \to F (m) D F (u) < x) \leftrightarrow \forall m \in ℤ_{\geq j} \forall k \in ℤ_{\geq j} (k \in ℤ_{\geq m} \to F (m) D F (k) < x)$
31		fveq2	$⊢ m = k \to ℤ_{\geq m} = ℤ_{\geq k}$
32	31	eleq2d	$⊢ m = k \to (u \in ℤ_{\geq m} \leftrightarrow u \in ℤ_{\geq k})$
33		fveq2	$⊢ m = k \to F (m) = F (k)$
34	33	oveq1d	$⊢ m = k \to F (m) D F (u) = F (k) D F (u)$
35	34	breq1d	$⊢ m = k \to (F (m) D F (u) < x \leftrightarrow F (k) D F (u) < x)$
36	32 35	imbi12d	$⊢ m = k \to ((u \in ℤ_{\geq m} \to F (m) D F (u) < x) \leftrightarrow (u \in ℤ_{\geq k} \to F (k) D F (u) < x))$
37		eleq1w	$⊢ u = m \to (u \in ℤ_{\geq k} \leftrightarrow m \in ℤ_{\geq k})$
38		fveq2	$⊢ u = m \to F (u) = F (m)$
39	38	oveq2d	$⊢ u = m \to F (k) D F (u) = F (k) D F (m)$
40	39	breq1d	$⊢ u = m \to (F (k) D F (u) < x \leftrightarrow F (k) D F (m) < x)$
41	37 40	imbi12d	$⊢ u = m \to ((u \in ℤ_{\geq k} \to F (k) D F (u) < x) \leftrightarrow (m \in ℤ_{\geq k} \to F (k) D F (m) < x))$
42	36 41	cbvral2vw	$⊢ \forall m \in ℤ_{\geq j} \forall u \in ℤ_{\geq j} (u \in ℤ_{\geq m} \to F (m) D F (u) < x) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x)$
43		ralcom	$⊢ \forall m \in ℤ_{\geq j} \forall k \in ℤ_{\geq j} (k \in ℤ_{\geq m} \to F (m) D F (k) < x) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (k \in ℤ_{\geq m} \to F (m) D F (k) < x)$
44	30 42 43	3bitr3i	$⊢ \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (k \in ℤ_{\geq m} \to F (m) D F (k) < x)$
45	44	anbi2i	$⊢ (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x)) \leftrightarrow (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (k \in ℤ_{\geq m} \to F (m) D F (k) < x))$
46		anidm	$⊢ (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x)) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x)$
47	23 45 46	3bitr2i	$⊢ \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} ((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land (k \in ℤ_{\geq m} \to F (m) D F (k) < x)) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x)$
48		simpll1	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to D \in ∞Met (X)$
49		simpll3	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to F : Z ⟶ X$
50	1	uztrn2	$⊢ (j \in Z \land m \in ℤ_{\geq j}) \to m \in Z$
51	50	ad2ant2l	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to m \in Z$
52	49 51	ffvelcdmd	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to F (m) \in X$
53	9	adantrr	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to F (k) \in X$
54		xmetsym	$⊢ (D \in ∞Met (X) \land F (m) \in X \land F (k) \in X) \to F (m) D F (k) = F (k) D F (m)$
55	48 52 53 54	syl3anc	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to F (m) D F (k) = F (k) D F (m)$
56	55	breq1d	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to (F (m) D F (k) < x \leftrightarrow F (k) D F (m) < x)$
57	56	imbi2d	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to ((k \in ℤ_{\geq m} \to F (m) D F (k) < x) \leftrightarrow (k \in ℤ_{\geq m} \to F (k) D F (m) < x))$
58	57	anbi2d	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to (((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land (k \in ℤ_{\geq m} \to F (m) D F (k) < x)) \leftrightarrow ((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land (k \in ℤ_{\geq m} \to F (k) D F (m) < x)))$
59		jaob	$⊢ ((m \in ℤ_{\geq k} \lor k \in ℤ_{\geq m}) \to F (k) D F (m) < x) \leftrightarrow ((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land (k \in ℤ_{\geq m} \to F (k) D F (m) < x))$
60		eluzelz	$⊢ k \in ℤ_{\geq j} \to k \in ℤ$
61		eluzelz	$⊢ m \in ℤ_{\geq j} \to m \in ℤ$
62		uztric	$⊢ (k \in ℤ \land m \in ℤ) \to (m \in ℤ_{\geq k} \lor k \in ℤ_{\geq m})$
63	60 61 62	syl2an	$⊢ (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j}) \to (m \in ℤ_{\geq k} \lor k \in ℤ_{\geq m})$
64	63	adantl	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to (m \in ℤ_{\geq k} \lor k \in ℤ_{\geq m})$
65		pm5.5	$⊢ (m \in ℤ_{\geq k} \lor k \in ℤ_{\geq m}) \to (((m \in ℤ_{\geq k} \lor k \in ℤ_{\geq m}) \to F (k) D F (m) < x) \leftrightarrow F (k) D F (m) < x)$
66	64 65	syl	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to (((m \in ℤ_{\geq k} \lor k \in ℤ_{\geq m}) \to F (k) D F (m) < x) \leftrightarrow F (k) D F (m) < x)$
67	59 66	bitr3id	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to (((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land (k \in ℤ_{\geq m} \to F (k) D F (m) < x)) \leftrightarrow F (k) D F (m) < x)$
68	58 67	bitrd	$⊢ (((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \land (k \in ℤ_{\geq j} \land m \in ℤ_{\geq j})) \to (((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land (k \in ℤ_{\geq m} \to F (m) D F (k) < x)) \leftrightarrow F (k) D F (m) < x)$
69	68	2ralbidva	$⊢ ((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} ((m \in ℤ_{\geq k} \to F (k) D F (m) < x) \land (k \in ℤ_{\geq m} \to F (m) D F (k) < x)) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} F (k) D F (m) < x)$
70	47 69	bitr3id	$⊢ ((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} (m \in ℤ_{\geq k} \to F (k) D F (m) < x) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} F (k) D F (m) < x)$
71	22 70	bitrd	$⊢ ((D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} F (k) D F (m) < x)$
72	71	rexbidva	$⊢ (D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} F (k) D F (m) < x)$
73		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
74		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
75	73 74	ax-mp	$⊢ ℤ_{\geq} Fn ℤ$
76		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
77	1 76	eqsstri	$⊢ Z \subseteq ℤ$
78		raleq	$⊢ u = ℤ_{\geq j} \to (\forall m \in u F (k) D F (m) < x \leftrightarrow \forall m \in ℤ_{\geq j} F (k) D F (m) < x)$
79	78	raleqbi1dv	$⊢ u = ℤ_{\geq j} \to (\forall k \in u \forall m \in u F (k) D F (m) < x \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} F (k) D F (m) < x)$
80	79	rexima	$⊢ (ℤ_{\geq} Fn ℤ \land Z \subseteq ℤ) \to (\exists u \in ℤ_{\geq} [Z] \forall k \in u \forall m \in u F (k) D F (m) < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} F (k) D F (m) < x)$
81	75 77 80	mp2an	$⊢ \exists u \in ℤ_{\geq} [Z] \forall k \in u \forall m \in u F (k) D F (m) < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq j} F (k) D F (m) < x$
82	72 81	bitr4di	$⊢ (D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow \exists u \in ℤ_{\geq} [Z] \forall k \in u \forall m \in u F (k) D F (m) < x)$
83	82	ralbidv	$⊢ (D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow \forall x \in ℝ^{+} \exists u \in ℤ_{\geq} [Z] \forall k \in u \forall m \in u F (k) D F (m) < x)$
84		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
85	84	adantr	$⊢ (D \in ∞Met (X) \land M \in ℤ) \to X \in dom ∞Met$
86		cnex	$⊢ ℂ \in V$
87	85 86	jctir	$⊢ (D \in ∞Met (X) \land M \in ℤ) \to (X \in dom ∞Met \land ℂ \in V)$
88		zsscn	$⊢ ℤ \subseteq ℂ$
89	77 88	sstri	$⊢ Z \subseteq ℂ$
90	89	jctr	$⊢ F : Z ⟶ X \to (F : Z ⟶ X \land Z \subseteq ℂ)$
91		elpm2r	$⊢ ((X \in dom ∞Met \land ℂ \in V) \land (F : Z ⟶ X \land Z \subseteq ℂ)) \to F \in (X ↑_{𝑝𝑚} ℂ)$
92	87 90 91	syl2an	$⊢ ((D \in ∞Met (X) \land M \in ℤ) \land F : Z ⟶ X) \to F \in (X ↑_{𝑝𝑚} ℂ)$
93		simpl	$⊢ (D \in ∞Met (X) \land M \in ℤ) \to D \in ∞Met (X)$
94		simpr	$⊢ (D \in ∞Met (X) \land M \in ℤ) \to M \in ℤ$
95	1 93 94	iscau3	$⊢ (D \in ∞Met (X) \land M \in ℤ) \to (F \in Cau (D) \leftrightarrow (F \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 \forall m \in ℤ_{\geq k} F (k) D F (m) < x)))$
96	95	baibd	$⊢ ((D \in ∞Met (X) \land M \in ℤ) \land F \in (X ↑_{𝑝𝑚} ℂ)) \to (F \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x))$
97	92 96	syldan	$⊢ ((D \in ∞Met (X) \land M \in ℤ) \land F : Z ⟶ X) \to (F \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x))$
98	97	3impa	$⊢ (D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \to (F \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x))$
99	2	eleq1i	$⊢ L \in CauFil (D) \leftrightarrow (X FilMap F) (ℤ_{\geq} [Z]) \in CauFil (D)$
100	1	uzfbas	$⊢ M \in ℤ \to ℤ_{\geq} [Z] \in fBas (Z)$
101		fmcfil	$⊢ (D \in ∞Met (X) \land ℤ_{\geq} [Z] \in fBas (Z) \land F : Z ⟶ X) \to ((X FilMap F) (ℤ_{\geq} [Z]) \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists u \in ℤ_{\geq} [Z] \forall k \in u \forall m \in u F (k) D F (m) < x)$
102	100 101	syl3an2	$⊢ (D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \to ((X FilMap F) (ℤ_{\geq} [Z]) \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists u \in ℤ_{\geq} [Z] \forall k \in u \forall m \in u F (k) D F (m) < x)$
103	99 102	bitrid	$⊢ (D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \to (L \in CauFil (D) \leftrightarrow \forall x \in ℝ^{+} \exists u \in ℤ_{\geq} [Z] \forall k \in u \forall m \in u F (k) D F (m) < x)$
104	83 98 103	3bitr4d	$⊢ (D \in ∞Met (X) \land M \in ℤ \land F : Z ⟶ X) \to (F \in Cau (D) \leftrightarrow L \in CauFil (D))$

Metamath Proof Explorer

Theorem caucfil

Proof