Definition df-cplmet 31531

Description: A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

Ref

Expression

df-cplmet

|- cplMetSp = ( w e. _V |-> [_ ( ( w ^s NN ) ↾s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } ) )

Distinct variable group:   e, f, g, j, p, q, r, v, w, x, y, z

Detailed syntax breakdown of Definition df-cplmet

Step	Hyp	Ref	Expression
1		ccpms 31523	. 2 class cplMetSp
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vr	. . . 4 setvar r
5	2	cv 1482	. . . . . 6 class w
6		cn 11020	. . . . . 6 class NN
7		cpws 16107	. . . . . 6 class ^s
8	5, 6, 7	co 6650	. . . . 5 class ( w ^s NN )
9		cds 15950	. . . . . . 7 class dist
10	5, 9	cfv 5888	. . . . . 6 class ( dist ` w )
11		cca 23051	. . . . . 6 class Cau
12	10, 11	cfv 5888	. . . . 5 class ( Cau ` ( dist ` w ) )
13		cress 15858	. . . . 5 class ↾s
14	8, 12, 13	co 6650	. . . 4 class ( ( w ^s NN ) ↾s ( Cau ` ( dist ` w ) ) )
15		vv	. . . . 5 setvar v
16	4	cv 1482	. . . . . 6 class r
17		cbs 15857	. . . . . 6 class Base
18	16, 17	cfv 5888	. . . . 5 class ( Base ` r )
19		ve	. . . . . 6 setvar e
20		vf	. . . . . . . . . . 11 setvar f
21	20	cv 1482	. . . . . . . . . 10 class f
22		vg	. . . . . . . . . . 11 setvar g
23	22	cv 1482	. . . . . . . . . 10 class g
24	21, 23	cpr 4179	. . . . . . . . 9 class { f , g }
25	15	cv 1482	. . . . . . . . 9 class v
26	24, 25	wss 3574	. . . . . . . 8 wff { f , g } C_ v
27		vj	. . . . . . . . . . . . 13 setvar j
28	27	cv 1482	. . . . . . . . . . . 12 class j
29		cuz 11687	. . . . . . . . . . . 12 class ZZ>=
30	28, 29	cfv 5888	. . . . . . . . . . 11 class ( ZZ>= ` j )
31	28, 23	cfv 5888	. . . . . . . . . . . 12 class ( g ` j )
32		vx	. . . . . . . . . . . . 13 setvar x
33	32	cv 1482	. . . . . . . . . . . 12 class x
34		cbl 19733	. . . . . . . . . . . . 13 class ball
35	10, 34	cfv 5888	. . . . . . . . . . . 12 class ( ball ` ( dist ` w ) )
36	31, 33, 35	co 6650	. . . . . . . . . . 11 class ( ( g ` j ) ( ball ` ( dist ` w ) ) x )
37	21, 30	cres 5116	. . . . . . . . . . 11 class ( f |` ( ZZ>= ` j ) )
38	30, 36, 37	wf 5884	. . . . . . . . . 10 wff ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x )
39		cz 11377	. . . . . . . . . 10 class ZZ
40	38, 27, 39	wrex 2913	. . . . . . . . 9 wff E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x )
41		crp 11832	. . . . . . . . 9 class RR+
42	40, 32, 41	wral 2912	. . . . . . . 8 wff A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x )
43	26, 42	wa 384	. . . . . . 7 wff ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) )
44	43, 20, 22	copab 4712	. . . . . 6 class { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) }
45	19	cv 1482	. . . . . . . 8 class e
46		cqus 16165	. . . . . . . 8 class /.s
47	16, 45, 46	co 6650	. . . . . . 7 class ( r /.s e )
48		cnx 15854	. . . . . . . . . 10 class ndx
49	48, 9	cfv 5888	. . . . . . . . 9 class ( dist ` ndx )
50		vp	. . . . . . . . . . . . . . . . 17 setvar p
51	50	cv 1482	. . . . . . . . . . . . . . . 16 class p
52	51, 45	cec 7740	. . . . . . . . . . . . . . 15 class [ p ] e
53	33, 52	wceq 1483	. . . . . . . . . . . . . 14 wff x = [ p ] e
54		vy	. . . . . . . . . . . . . . . 16 setvar y
55	54	cv 1482	. . . . . . . . . . . . . . 15 class y
56		vq	. . . . . . . . . . . . . . . . 17 setvar q
57	56	cv 1482	. . . . . . . . . . . . . . . 16 class q
58	57, 45	cec 7740	. . . . . . . . . . . . . . 15 class [ q ] e
59	55, 58	wceq 1483	. . . . . . . . . . . . . 14 wff y = [ q ] e
60	53, 59	wa 384	. . . . . . . . . . . . 13 wff ( x = [ p ] e /\ y = [ q ] e )
61	16, 9	cfv 5888	. . . . . . . . . . . . . . . 16 class ( dist ` r )
62	61	cof 6895	. . . . . . . . . . . . . . 15 class oF ( dist ` r )
63	51, 57, 62	co 6650	. . . . . . . . . . . . . 14 class ( p oF ( dist ` r ) q )
64		vz	. . . . . . . . . . . . . . 15 setvar z
65	64	cv 1482	. . . . . . . . . . . . . 14 class z
66		cli 14215	. . . . . . . . . . . . . 14 class ~~>
67	63, 65, 66	wbr 4653	. . . . . . . . . . . . 13 wff ( p oF ( dist ` r ) q ) ~~> z
68	60, 67	wa 384	. . . . . . . . . . . 12 wff ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z )
69	68, 56, 25	wrex 2913	. . . . . . . . . . 11 wff E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z )
70	69, 50, 25	wrex 2913	. . . . . . . . . 10 wff E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z )
71	70, 32, 54, 64	coprab 6651	. . . . . . . . 9 class { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) }
72	49, 71	cop 4183	. . . . . . . 8 class <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >.
73	72	csn 4177	. . . . . . 7 class { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. }
74		csts 15855	. . . . . . 7 class sSet
75	47, 73, 74	co 6650	. . . . . 6 class ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } )
76	19, 44, 75	csb 3533	. . . . 5 class [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } )
77	15, 18, 76	csb 3533	. . . 4 class [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } )
78	4, 14, 77	csb 3533	. . 3 class [_ ( ( w ^s NN ) ↾s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } )
79	2, 3, 78	cmpt 4729	. 2 class ( w e. _V |-> [_ ( ( w ^s NN ) ↾s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } ) )
80	1, 79	wceq 1483	1 wff cplMetSp = ( w e. _V |-> [_ ( ( w ^s NN ) ↾s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /.s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } ) )

This definition is referenced by: (None)