Definition df-cau 7923

Description: Define a function on metric spaces whose value is the set of Cauchy sequences of the space.

Assertion

Ref	Expression
df-cau	|- Cau = {<.z, w>. | (z e. Met /\ w = {f | (f (_ (CC X. dom dom z) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))))})}

Distinct variable group:   j,k,m,x,f,z,w

Detailed syntax breakdown of Definition df-cau

Step	Hyp	Ref	Expression
1		cca 7920	. 2 class Cau
2		vz	. . . . . 6 set z
3	2	cv 955	. . . . 5 class z
4		cme 7789	. . . . 5 class Met
5	3, 4	wcel 958	. . . 4 wff z e. Met
6		vw	. . . . . 6 set w
7	6	cv 955	. . . . 5 class w
8		vf	. . . . . . . . 9 set f
9	8	cv 955	. . . . . . . 8 class f
10		cc 5232	. . . . . . . . 9 class CC
11	3	cdm 3170	. . . . . . . . . 10 class dom z
12	11	cdm 3170	. . . . . . . . 9 class dom dom z
13	10, 12	cxp 3168	. . . . . . . 8 class (CC X. dom dom z)
14	9, 13	wss 2047	. . . . . . 7 wff f (_ (CC X. dom dom z)
15		cc0 5234	. . . . . . . . . 10 class 0
16		vx	. . . . . . . . . . 11 set x
17	16	cv 955	. . . . . . . . . 10 class x
18		clt 5486	. . . . . . . . . 10 class <
19	15, 17, 18	wbr 2619	. . . . . . . . 9 wff 0 < x
20		vj	. . . . . . . . . . . . . . . 16 set j
21	20	cv 955	. . . . . . . . . . . . . . 15 class j
22		vk	. . . . . . . . . . . . . . . 16 set k
23	22	cv 955	. . . . . . . . . . . . . . 15 class k
24		cle 5295	. . . . . . . . . . . . . . 15 class <_
25	21, 23, 24	wbr 2619	. . . . . . . . . . . . . 14 wff j <_ k
26		vm	. . . . . . . . . . . . . . . 16 set m
27	26	cv 955	. . . . . . . . . . . . . . 15 class m
28	21, 27, 24	wbr 2619	. . . . . . . . . . . . . 14 wff j <_ m
29	25, 28	wa 223	. . . . . . . . . . . . 13 wff (j <_ k /\ j <_ m)
30	23, 9	cfv 3182	. . . . . . . . . . . . . . 15 class (f` k)
31	30, 12	wcel 958	. . . . . . . . . . . . . 14 wff (f` k) e. dom dom z
32	27, 9	cfv 3182	. . . . . . . . . . . . . . 15 class (f` m)
33	32, 12	wcel 958	. . . . . . . . . . . . . 14 wff (f` m) e. dom dom z
34		cD	. . . . . . . . . . . . . . . 16 class D
35	30, 32, 34	co 3963	. . . . . . . . . . . . . . 15 class ((f` k)D(f` m))
36	35, 17, 18	wbr 2619	. . . . . . . . . . . . . 14 wff ((f` k)D(f` m)) < x
37	31, 33, 36	w3a 775	. . . . . . . . . . . . 13 wff ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x)
38	29, 37	wi 3	. . . . . . . . . . . 12 wff ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))
39		cz 5298	. . . . . . . . . . . 12 class ZZ
40	38, 26, 39	wral 1645	. . . . . . . . . . 11 wff A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))
41	40, 22, 39	wral 1645	. . . . . . . . . 10 wff A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))
42	41, 20, 39	wrex 1646	. . . . . . . . 9 wff E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))
43	19, 42	wi 3	. . . . . . . 8 wff (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x)))
44		cr 5233	. . . . . . . 8 class RR
45	43, 16, 44	wral 1645	. . . . . . 7 wff A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x)))
46	14, 45	wa 223	. . . . . 6 wff (f (_ (CC X. dom dom z) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))))
47	46, 8	cab 1463	. . . . 5 class {f | (f (_ (CC X. dom dom z) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))))}
48	7, 47	wceq 956	. . . 4 wff w = {f | (f (_ (CC X. dom dom z) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))))}
49	5, 48	wa 223	. . 3 wff (z e. Met /\ w = {f | (f (_ (CC X. dom dom z) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))))})
50	49, 2, 6	copab 2666	. 2 class {<.z, w>. | (z e. Met /\ w = {f | (f (_ (CC X. dom dom z) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))))})}
51	1, 50	wceq 956	1 wff Cau = {<.z, w>. | (z e. Met /\ w = {f | (f (_ (CC X. dom dom z) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))))})}

This definition is referenced by:  caufval 7926

Copyright terms: Public domain