Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cplmet Unicode version

Definition df-cplmet 23967
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  o F ( 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
StepHypRef Expression
1 ccpms 23959 . 2  class cplMetSp
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
4 vr . . . 4  set  r
52cv 1622 . . . . . 6  class  w
6 cn 9746 . . . . . 6  class  NN
7 cpws 13347 . . . . . 6  class  ^s
85, 6, 7co 5858 . . . . 5  class  ( w  ^s  NN )
9 cds 13217 . . . . . . 7  class  dist
105, 9cfv 5255 . . . . . 6  class  ( dist `  w )
11 cca 18679 . . . . . 6  class  Cau
1210, 11cfv 5255 . . . . 5  class  ( Cau `  ( dist `  w
) )
13 cress 13149 . . . . 5  classs
148, 12, 13co 5858 . . . 4  class  ( ( w  ^s  NN )s  ( Cau `  ( dist `  w ) ) )
15 vv . . . . 5  set  v
164cv 1622 . . . . . 6  class  r
17 cbs 13148 . . . . . 6  class  Base
1816, 17cfv 5255 . . . . 5  class  ( Base `  r )
19 ve . . . . . 6  set  e
20 vf . . . . . . . . . . 11  set  f
2120cv 1622 . . . . . . . . . 10  class  f
22 vg . . . . . . . . . . 11  set  g
2322cv 1622 . . . . . . . . . 10  class  g
2421, 23cpr 3641 . . . . . . . . 9  class  { f ,  g }
2515cv 1622 . . . . . . . . 9  class  v
2624, 25wss 3152 . . . . . . . 8  wff  { f ,  g }  C_  v
27 vj . . . . . . . . . . . . 13  set  j
2827cv 1622 . . . . . . . . . . . 12  class  j
29 cuz 10230 . . . . . . . . . . . 12  class  ZZ>=
3028, 29cfv 5255 . . . . . . . . . . 11  class  ( ZZ>= `  j )
3128, 23cfv 5255 . . . . . . . . . . . 12  class  ( g `
 j )
32 vx . . . . . . . . . . . . 13  set  x
3332cv 1622 . . . . . . . . . . . 12  class  x
34 cbl 16371 . . . . . . . . . . . . 13  class  ball
3510, 34cfv 5255 . . . . . . . . . . . 12  class  ( ball `  ( dist `  w
) )
3631, 33, 35co 5858 . . . . . . . . . . 11  class  ( ( g `  j ) ( ball `  ( dist `  w ) ) x )
3721, 30cres 4691 . . . . . . . . . . 11  class  ( f  |`  ( ZZ>= `  j )
)
3830, 36, 37wf 5251 . . . . . . . . . 10  wff  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( g `  j ) ( ball `  ( dist `  w ) ) x )
39 cz 10024 . . . . . . . . . 10  class  ZZ
4038, 27, 39wrex 2544 . . . . . . . . 9  wff  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( g `  j ) ( ball `  ( dist `  w ) ) x )
41 crp 10354 . . . . . . . . 9  class  RR+
4240, 32, 41wral 2543 . . . . . . . 8  wff  A. x  e.  RR+  E. j  e.  ZZ  ( f  |`  ( ZZ>= `  j )
) : ( ZZ>= `  j ) --> ( ( g `  j ) ( ball `  ( dist `  w ) ) x )
4326, 42wa 358 . . . . . . 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 ) )
4443, 20, 22copab 4076 . . . . . 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 ) ) }
4519cv 1622 . . . . . . . 8  class  e
46 cqus 13408 . . . . . . . 8  class  /.s
4716, 45, 46co 5858 . . . . . . 7  class  ( r 
/.s  e )
48 cnx 13145 . . . . . . . . . 10  class  ndx
4948, 9cfv 5255 . . . . . . . . 9  class  ( dist `  ndx )
50 vp . . . . . . . . . . . . . . . . 17  set  p
5150cv 1622 . . . . . . . . . . . . . . . 16  class  p
5251, 45cec 6658 . . . . . . . . . . . . . . 15  class  [ p ] e
5333, 52wceq 1623 . . . . . . . . . . . . . 14  wff  x  =  [ p ] e
54 vy . . . . . . . . . . . . . . . 16  set  y
5554cv 1622 . . . . . . . . . . . . . . 15  class  y
56 vq . . . . . . . . . . . . . . . . 17  set  q
5756cv 1622 . . . . . . . . . . . . . . . 16  class  q
5857, 45cec 6658 . . . . . . . . . . . . . . 15  class  [ q ] e
5955, 58wceq 1623 . . . . . . . . . . . . . 14  wff  y  =  [ q ] e
6053, 59wa 358 . . . . . . . . . . . . 13  wff  ( x  =  [ p ]
e  /\  y  =  [ q ] e )
6116, 9cfv 5255 . . . . . . . . . . . . . . . 16  class  ( dist `  r )
6261cof 6076 . . . . . . . . . . . . . . 15  class  o F ( dist `  r
)
6351, 57, 62co 5858 . . . . . . . . . . . . . 14  class  ( p  o F ( dist `  r ) q )
64 vz . . . . . . . . . . . . . . 15  set  z
6564cv 1622 . . . . . . . . . . . . . 14  class  z
66 cli 11958 . . . . . . . . . . . . . 14  class  ~~>
6763, 65, 66wbr 4023 . . . . . . . . . . . . 13  wff  ( p  o F ( dist `  r ) q )  ~~>  z
6860, 67wa 358 . . . . . . . . . . . 12  wff  ( ( x  =  [ p ] e  /\  y  =  [ q ] e )  /\  ( p  o F ( dist `  r ) q )  ~~>  z )
6968, 56, 25wrex 2544 . . . . . . . . . . 11  wff  E. q  e.  v  ( (
x  =  [ p ] e  /\  y  =  [ q ] e )  /\  ( p  o F ( dist `  r ) q )  ~~>  z )
7069, 50, 25wrex 2544 . . . . . . . . . 10  wff  E. p  e.  v  E. q  e.  v  ( (
x  =  [ p ] e  /\  y  =  [ q ] e )  /\  ( p  o F ( dist `  r ) q )  ~~>  z )
7170, 32, 54, 64coprab 5859 . . . . . . . . 9  class  { <. <.
x ,  y >. ,  z >.  |  E. p  e.  v  E. q  e.  v  (
( x  =  [
p ] e  /\  y  =  [ q ] e )  /\  ( p  o F
( dist `  r )
q )  ~~>  z ) }
7249, 71cop 3643 . . . . . . . 8  class  <. ( dist `  ndx ) ,  { <. <. x ,  y
>. ,  z >.  |  E. p  e.  v  E. q  e.  v  ( ( x  =  [ p ] e  /\  y  =  [
q ] e )  /\  ( p  o F ( dist `  r
) q )  ~~>  z ) } >.
7372csn 3640 . . . . . . 7  class  { <. (
dist `  ndx ) ,  { <. <. x ,  y
>. ,  z >.  |  E. p  e.  v  E. q  e.  v  ( ( x  =  [ p ] e  /\  y  =  [
q ] e )  /\  ( p  o F ( dist `  r
) q )  ~~>  z ) } >. }
74 csts 13146 . . . . . . 7  class sSet
7547, 73, 74co 5858 . . . . . 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  o F ( dist `  r
) q )  ~~>  z ) } >. } )
7619, 44, 75csb 3081 . . . . 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  o F ( dist `  r
) q )  ~~>  z ) } >. } )
7715, 18, 76csb 3081 . . . 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  o F ( dist `  r ) q )  ~~>  z ) } >. } )
784, 14, 77csb 3081 . . 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  o F ( dist `  r ) q )  ~~>  z ) } >. } )
792, 3, 78cmpt 4077 . 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  o F ( dist `  r ) q )  ~~>  z ) } >. } ) )
801, 79wceq 1623 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  o F ( dist `  r ) q )  ~~>  z ) } >. } ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator