MPE Home Metamath Proof Explorer This is the GIF version.
Change to Unicode version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 5 wff 
-.  ph
wi 6 wff  ( ph  ->  ps )
ax-1 7 |-  ( ph  ->  ( ps  ->  ph ) )
ax-2 8 |-  ( ( ph  ->  ( ps  ->  ch )
)  ->  ( ( ph  ->  ps )  -> 
( ph  ->  ch )
) )
ax-3 9 |-  ( ( -.  ph  ->  -.  ps )  -> 
( ps  ->  ph )
)
ax-mp 10 |- 
ph   &    |-  ( ph  ->  ps )   =>    |- 
ps
wb 178 wff  ( ph  <->  ps )
df-bi 179 |- 
-.  ( ( (
ph 
<->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ph  <->  ps ) ) )
wo 359 wff  ( ph  \/  ps )
wa 360 wff  ( ph  /\  ps )
df-or 361 |-  ( ( ph  \/  ps )  <->  ( -.  ph  ->  ps ) )
df-an 362 |-  ( ( ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
w3o 938 wff  ( ph  \/  ps  \/  ch )
w3a 939 wff  ( ph  /\  ps  /\ 
ch )
df-3or 940 |-  ( ( ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/ 
ch ) )
df-3an 941 |-  ( ( ph  /\  ps  /\  ch )  <->  ( ( ph  /\  ps )  /\  ch ) )
wnan 1292 wff  ( ph  -/\  ps )
df-nan 1293 |-  ( ( ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
wxo 1300 wff  ( ph \/_ ps )
df-xor 1301 |-  ( ( ph \/_ ps )  <->  -.  ( ph  <->  ps ) )
wtru 1312 wff 
T.
wfal 1313 wff 
F.
df-tru 1315 |-  (  T.  <->  ( ph  <->  ph ) )
df-fal 1316 |-  (  F.  <->  -.  T.  )
whad 1374 wff hadd
( ph ,  ps ,  ch )
wcad 1375 wff cadd
( ph ,  ps ,  ch )
df-had 1376 |-  (hadd ( ph ,  ps ,  ch )  <->  ( ( ph \/_ ps ) \/_ ch ) )
df-cad 1377 |-  (cadd ( ph ,  ps ,  ch )  <->  ( ( ph  /\  ps )  \/  ( ch  /\  ( ph \/_ ps ) ) ) )
ax-meredith 1401 |-  ( ( ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -.  th ) )  ->  ch )  ->  ta )  ->  ( ( ta  ->  ph )  -> 
( th  ->  ph )
) )
wal 1532 wff  A. x ph
ax-5 1533 |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
ax-6 1534 |-  ( -.  A. x ph  ->  A. x  -.  A. x ph )
ax-7 1535 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-gen 1536 |- 
ph   =>    |- 
A. x ph
wex 1537 wff 
E. x ph
df-ex 1538 |-  ( E. x ph  <->  -.  A. x  -.  ph )
wnf 1539 wff 
F/ x ph
df-nf 1540 |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
cv 1618 class  x
wceq 1619 wff 
A  =  B
wcel 1621 wff 
A  e.  B
ax-8 1623 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-11 1624 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-13 1625 |-  ( x  =  y  ->  ( x  e.  z  ->  y  e.  z ) )
ax-14 1626 |-  ( x  =  y  ->  ( z  e.  x  ->  z  e.  y ) )
ax-17 1628 |-  ( ph  ->  A. x ph )
ax-9v 1632 |-  -.  A. x  -.  x  =  y
ax-12 1633 |-  ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
)
ax-12o 1664 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  =  y  ->  A. z  x  =  y ) ) )
ax-10 1678 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-9 1684 |-  -.  A. x  -.  x  =  y
ax-4 1692 |-  ( A. x ph  ->  ph )
ax-5o 1694 |-  ( A. x ( A. x ph  ->  ps )  ->  ( A. x ph  ->  A. x ps )
)
ax-6o 1697 |-  ( -.  A. x  -.  A. x ph  ->  ph )
ax-9o 1815 |-  ( A. x ( x  =  y  ->  A. x ph )  ->  ph )
ax-10o 1835 |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph ) )
wsb 1882 wff 
[ y  /  x ] ph
df-sb 1883 |-  ( [ y  /  x ] ph  <->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph ) ) )
ax-16 1926 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
ax-11o 1940 |-  ( -.  A. x  x  =  y  ->  ( x  =  y  -> 
( ph  ->  A. x
( x  =  y  ->  ph ) ) ) )
ax-15 2102 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  e.  y  ->  A. z  x  e.  y ) ) )
weu 2114 wff 
E! x ph
wmo 2115 wff 
E* x ph
df-eu 2118 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
df-mo 2119 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
ax-7d 2204 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-8d 2205 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-9d1 2206 |- 
-.  A. x  -.  x  =  x
ax-9d2 2207 |- 
-.  A. x  -.  x  =  y
ax-10d 2208 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11d 2209 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-ext 2234 |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
cab 2239 class  { x  |  ph }
df-clab 2240 |-  ( x  e.  {
y  |  ph }  <->  [ x  /  y ]
ph )
df-cleq 2246 |-  ( A. x ( x  e.  y  <->  x  e.  z )  ->  y  =  z )   =>    |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
df-clel 2249 |-  ( A  e.  B  <->  E. x ( x  =  A  /\  x  e.  B ) )
wnfc 2372 wff  F/_ x A
df-nfc 2374 |-  ( F/_ x A  <->  A. y F/ x  y  e.  A )
wne 2412 wff 
A  =/=  B
wnel 2413 wff 
A  e/  B
df-ne 2414 |-  ( A  =/=  B  <->  -.  A  =  B )
df-nel 2415 |-  ( A  e/  B  <->  -.  A  e.  B )
wral 2509 wff  A. x  e.  A  ph
wrex 2510 wff 
E. x  e.  A  ph
wreu 2511 wff 
E! x  e.  A  ph
crab 2512 class  { x  e.  A  |  ph }
df-ral 2513 |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
df-rex 2514 |-  ( E. x  e.  A  ph  <->  E. x
( x  e.  A  /\  ph ) )
df-reu 2515 |-  ( E! x  e.  A  ph  <->  E! x
( x  e.  A  /\  ph ) )
df-rab 2516 |- 
{ x  e.  A  |  ph }  =  {
x  |  ( x  e.  A  /\  ph ) }
cvv 2727 class  _V
df-v 2729 |-  _V  =  { x  |  x  =  x }
wcdeq 2904 wff CondEq ( x  =  y  ->  ph )
df-cdeq 2905 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 2921 wff  [. A  /  x ]. ph
df-sbc 2922 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 3009 class  [_ A  /  x ]_ B
df-csb 3010 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 3075 class  ( A  \  B )
cun 3076 class  ( A  u.  B )
cin 3077 class  ( A  i^i  B )
wss 3078 wff 
A  C_  B
wpss 3079 wff 
A  C.  B
df-dif 3081 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 3083 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 3085 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 3089 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
df-pss 3091 |-  ( A  C.  B  <->  ( A  C_  B  /\  A  =/=  B ) )
c0 3362 class  (/)
df-nul 3363 |-  (/)  =  ( _V  \  _V )
cif 3470 class  if ( ph ,  A ,  B )
df-if 3471 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3530 class  ~P A
df-pw 3532 |-  ~P A  =  {
x  |  x  C_  A }
csn 3544 class  { A }
cpr 3545 class  { A ,  B }
ctp 3546 class  { A ,  B ,  C }
cop 3547 class  <. A ,  B >.
cotp 3548 class  <. A ,  B ,  C >.
df-sn 3550 |-  { A }  =  {
x  |  x  =  A }
df-pr 3551 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3552 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3553 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3554 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 3727 class  U. A
df-uni 3728 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 3760 class  |^| A
df-int 3761 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 3803 class  U_ x  e.  A  B
ciin 3804 class  |^|_
x  e.  A  B
df-iun 3805 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 3806 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 3891 wff Disj  x  e.  A B
df-disj 3892 |-  (Disj  x  e.  A B 
<-> 
A. y E* x
( x  e.  A  /\  y  e.  B
) )
wbr 3920 wff 
A R B
df-br 3921 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 3973 class  {
<. x ,  y >.  |  ph }
cmpt 3974 class  ( x  e.  A  |->  B )
df-opab 3975 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 3976 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 4010 wff 
Tr  A
df-tr 4011 |-  ( Tr  A  <->  U. A  C_  A )
ax-rep 4028 |-  ( A. w E. y A. z ( A. y ph  ->  z  =  y )  ->  E. y A. z ( z  e.  y  <->  E. w ( w  e.  x  /\  A. y ph ) ) )
ax-sep 4038 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 4046 |- 
E. x A. y  -.  y  e.  x
ax-pow 4082 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
ax-pr 4108 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4196 class  _E
cid 4197 class  _I
df-eprel 4198 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4202 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4205 wff 
R  Po  A
wor 4206 wff 
R  Or  A
df-po 4207 |-  ( R  Po  A  <->  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) ) )
df-so 4208 |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) ) )
wfr 4242 wff 
R  Fr  A
wse 4243 wff 
R Se  A
wwe 4244 wff 
R  We  A
df-fr 4245 |-  ( R  Fr  A  <->  A. x ( ( x 
C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
df-se 4246 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-we 4247 |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A )
)
word 4284 wff 
Ord  A
con0 4285 class  On
wlim 4286 wff 
Lim  A
csuc 4287 class  suc 
A
df-ord 4288 |-  ( Ord  A  <->  ( Tr  A  /\  _E  We  A
) )
df-on 4289 |-  On  =  { x  |  Ord  x }
df-lim 4290 |-  ( Lim  A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
df-suc 4291 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4403 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
com 4547 class  om
df-om 4548 |-  om  =  { x  e.  On  |  A. y
( Lim  y  ->  x  e.  y ) }
cxp 4578 class  ( A  X.  B )
ccnv 4579 class  `' A
cdm 4580 class  dom 
A
crn 4581 class  ran 
A
cres 4582 class  ( A  |`  B )
cima 4583 class  ( A " B )
ccom 4584 class  ( A  o.  B )
wrel 4585 wff 
Rel  A
wfun 4586 wff 
Fun  A
wfn 4587 wff 
A  Fn  B
wf 4588 wff 
F : A --> B
wf1 4589 wff 
F : A -1-1-> B
wfo 4590 wff 
F : A -onto-> B
wf1o 4591 wff 
F : A -1-1-onto-> B
cfv 4592 class  ( F `  A )
wiso 4593 wff 
H  Isom  R ,  S  ( A ,  B )
df-xp 4594 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4595 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4596 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4597 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4598 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4599 |-  ran  A  =  dom  `'  A
df-res 4600 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4601 |-  ( A " B
)  =  ran  (  A  |`  B )
df-fun 4602 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 4603 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 4604 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 4605 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 4606 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 4607 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 4608 |-  ( F `  A )  =  U. { x  |  ( F " { A } )  =  { x } }
df-isom 4609 |-  ( H  Isom  R ,  S  ( A ,  B )  <->  ( H : A -1-1-onto-> B  /\  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) ) ) )
co 5710 class  ( A F B )
copab2 5711 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpt2 5712 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 5713 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 5714 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpt2 5715 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 5928 class  o F R
cofr 5929 class  o R R
df-of 5930 |-  o F R  =  ( f  e.  _V , 
g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 5931 |-  o R R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 5972 class  1st
c2nd 5973 class  2nd
df-1st 5974 |- 
1st  =  ( x  e.  _V  |->  U. dom  {  x } )
df-2nd 5975 |- 
2nd  =  ( x  e.  _V  |->  U. ran  {  x } )
ctpos 6085 class tpos  F
df-tpos 6086 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
ccur 6124 class curry  A
cunc 6125 class uncurry  A
df-cur 6126 |- curry  F  =  ( x  e.  dom  dom  F  |->  {
<. y ,  z >.  |  <. x ,  y
>. F z } )
df-unc 6127 |- uncurry  F  =  { <. <. x ,  y >. ,  z
>.  |  y ( F `  x )
z }
crpss 6128 class [ C.]
df-rpss 6129 |- [
C.]  =  { <. x ,  y >.  |  x 
C.  y }
cio 6141 class  ( iota x ph )
df-iota 6143 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
cund 6180 class  Undef
crio 6181 class  (
iota_ x  e.  A ph )
df-undef 6182 |- 
Undef  =  ( s  e.  _V  |->  ~P U. s )
df-riota 6190 |-  ( iota_ x  e.  A ph )  =  if ( E! x  e.  A  ph ,  ( iota x
( x  e.  A  /\  ph ) ) ,  ( Undef `  { x  |  x  e.  A } ) )
wsmo 6248 wff 
Smo  A
df-smo 6249 |-  ( Smo  A  <->  ( A : dom  A --> On  /\  Ord  dom  A  /\  A. x  e.  dom  A A. y  e.  dom  A ( x  e.  y  -> 
( A `  x
)  e.  ( A `
 y ) ) ) )
crecs 6273 class recs ( F )
df-recs 6274 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 6308 class  rec ( F ,  I
)
df-rdg 6309 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  if ( g  =  (/) ,  I ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) ) )
cseqom 6345 class seq𝜔 ( F ,  I )
df-seqom 6346 |- seq𝜔 ( F ,  I )  =  ( rec (
( i  e.  om ,  v  e.  _V  |->  <. suc  i ,  ( i F v )
>. ) ,  <. (/) ,  (  _I  `  I )
>. ) " om )
c1o 6358 class  1o
c2o 6359 class  2o
c3o 6360 class  3o
c4o 6361 class  4o
coa 6362 class  +o
comu 6363 class  .o
coe 6364 class  ^o
df-1o 6365 |-  1o  =  suc  (/)
df-2o 6366 |-  2o  =  suc  1o
df-3o 6367 |-  3o  =  suc  2o
df-4o 6368 |-  4o  =  suc  3o
df-oadd 6369 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6370 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexp 6371 |- 
^o  =  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
wer 6543 wff 
R  Er  A
cec 6544 class  [ A ] R
cqs 6545 class  ( A /. R )
df-er 6546 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6548 |-  [ A ] R  =  ( R " { A } )
df-qs 6552 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cmap 6658 class  ^m
cpm 6659 class  ^pm
df-map 6660 |- 
^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
df-pm 6661 |-  ^pm  =  ( x  e. 
_V ,  y  e. 
_V  |->  { f  e. 
~P ( y  X.  x )  |  Fun  f } )
cixp 6703 class  X_ x  e.  A  B
df-ixp 6704 |-  X_ x  e.  A  B  =  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
cen 6746 class  ~~
cdom 6747 class  ~<_
csdm 6748 class  ~<
cfn 6749 class  Fin
df-en 6750 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 6751 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-sdom 6752 |- 
~<  =  (  ~<_  \  ~~  )
df-fin 6753 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
cfi 7048 class  fi
df-fi 7049 |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
csup 7077 class  sup ( A ,  B ,  R )
df-sup 7078 |- 
sup ( A ,  B ,  R )  =  U. { x  e.  B  |  ( A. y  e.  A  -.  x R y  /\  A. y  e.  B  (
y R x  ->  E. z  e.  A  y R z ) ) }
coi 7108 class OrdIso ( R ,  A )
df-oi 7109 |- OrdIso ( R ,  A )  =  if ( ( R  We  A  /\  R Se  A ) ,  (recs ( ( h  e. 
_V  |->  ( iota_ v  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )  |`  { x  e.  On  |  E. t  e.  A  A. z  e.  (recs ( ( h  e. 
_V  |->  ( iota_ v  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w } A. u  e. 
{ w  e.  A  |  A. j  e.  ran  h  j R w }  -.  u R v ) ) )
" x ) z R t } ) ,  (/) )
char 7154 class har
cwdom 7155 class  ~<_*
df-har 7156 |- har 
=  ( x  e. 
_V  |->  { y  e.  On  |  y  ~<_  x } )
df-wdom 7157 |-  ~<_*  =  { <. x ,  y
>.  |  ( x  =  (/)  \/  E. z 
z : y -onto-> x ) }
ax-reg 7190 |-  ( E. y  y  e.  x  ->  E. y
( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x )
) )
ax-inf 7223 |- 
E. y ( x  e.  y  /\  A. z ( z  e.  y  ->  E. w
( z  e.  w  /\  w  e.  y
) ) )
ax-inf2 7226 |- 
E. x ( E. y ( y  e.  x  /\  A. z  -.  z  e.  y
)  /\  A. y
( y  e.  x  ->  E. z ( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) ) ) )
ccnf 7246 class CNF
df-cnf 7247 |- CNF 
=  ( x  e.  On ,  y  e.  On  |->  ( f  e. 
{ g  e.  ( x  ^m  y )  |  ( `' g
" ( _V  \  1o ) )  e.  Fin } 
|->  [_OrdIso (  _E  , 
( `' f "
( _V  \  1o ) ) )  /  h ]_ (seq𝜔 ( ( k  e. 
_V ,  z  e. 
_V  |->  ( ( ( x  ^o  ( h `
 k ) )  .o  ( f `  ( h `  k
) ) )  +o  z ) ) ,  (/) ) `  dom  h
) ) )
ctc 7305 class  TC
df-tc 7306 |-  TC  =  ( x  e.  _V  |->  |^| { y  |  ( x  C_  y  /\  Tr  y ) } )
cr1 7318 class  R1
crnk 7319 class  rank
df-r1 7320 |-  R1  =  rec (
( x  e.  _V  |->  ~P x ) ,  (/) )
df-rank 7321 |- 
rank  =  ( x  e.  _V  |->  |^| { y  e.  On  |  x  e.  ( R1 `  suc  y ) } )
ccrd 7452 class  card
cale 7453 class  aleph
ccf 7454 class  cf
wacn 7455 class AC  A
df-card 7456 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
df-aleph 7457 |-  aleph  =  rec (har ,  om )
df-cf 7458 |-  cf  =  ( x  e.  On  |->  |^| { y  |  E. z ( y  =  ( card `  z
)  /\  ( z  C_  x  /\  A. v  e.  x  E. u  e.  z  v  C_  u ) ) } )
df-acn 7459 |- AC  A  =  { x  |  ( A  e. 
_V  /\  A. f  e.  ( ( ~P x  \  { (/) } )  ^m  A ) E. g A. y  e.  A  ( g `  y
)  e.  ( f `
 y ) ) }
wac 7626 wff CHOICE
df-ac 7627 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x ) )
ccda 7677 class  +c
df-cda 7678 |- 
+c  =  ( x  e.  _V ,  y  e.  _V  |->  ( ( x  X.  { (/) } )  u.  ( y  X.  { 1o }
) ) )
cfin1a 7788 class FinIa
cfin2 7789 class FinII
cfin4 7790 class FinIV
cfin3 7791 class FinIII
cfin5 7792 class FinV
cfin6 7793 class FinVI
cfin7 7794 class FinVII
df-fin1a 7795 |- FinIa  =  { x  |  A. y  e.  ~P  x
( y  e.  Fin  \/  ( x  \  y
)  e.  Fin ) }
df-fin2 7796 |- FinII  =  { x  |  A. y  e.  ~P  ~P x
( ( y  =/=  (/)  /\ [ C.]  Or  y
)  ->  U. y  e.  y ) }
df-fin4 7797 |- FinIV  =  { x  |  -.  E. y ( y  C.  x  /\  y  ~~  x
) }
df-fin3 7798 |- FinIII  =  { x  |  ~P x  e. FinIV }
df-fin5 7799 |- FinV  =  { x  |  ( x  =  (/)  \/  x  ~<  ( x  +c  x
) ) }
df-fin6 7800 |- FinVI  =  { x  |  ( x  ~<  2o  \/  x  ~<  ( x  X.  x ) ) }
df-fin7 7801 |- FinVII  =  { x  |  -.  E. y  e.  ( On 
\  om ) x 
~~  y }
ax-cc 7945 |-  ( x  ~~  om  ->  E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
ax-dc 7956 |-  ( ( E. y E. z  y x
z  /\  ran  x  C_  dom  x )  ->  E. f A. n  e.  om  ( f `  n
) x ( f `
 suc  n )
)
ax-ac 7969 |-  E. y A. z A. w ( ( z  e.  w  /\  w  e.  x )  ->  E. v A. u ( E. t
( ( u  e.  w  /\  w  e.  t )  /\  (
u  e.  t  /\  t  e.  y )
)  <->  u  =  v
) )
ax-ac2 7973 |- 
E. y A. z E. v A. u ( ( y  e.  x  /\  ( z  e.  y  ->  ( ( v  e.  x  /\  -.  y  =  v )  /\  z  e.  v
) ) )  \/  ( -.  y  e.  x  /\  ( z  e.  x  ->  (
( v  e.  z  /\  v  e.  y )  /\  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v ) ) ) ) )
cgch 8122 class GCH
df-gch 8123 |- GCH 
=  ( Fin  u.  { x  |  A. y  -.  ( x  ~<  y  /\  y  ~<  ~P x
) } )
cwina 8184 class  Inacc W
cina 8185 class  Inacc
df-wina 8186 |- 
Inacc W  =  {
x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z
) }
df-ina 8187 |- 
Inacc  =  { x  |  ( x  =/=  (/)  /\  ( cf `  x
)  =  x  /\  A. y  e.  x  ~P y  ~<  x ) }
cwun 8202 class WUni
cwunm 8203 class wUniCl
df-wun 8204 |- WUni 
=  { u  |  ( Tr  u  /\  u  =/=  (/)  /\  A. x  e.  u  ( U. x  e.  u  /\  ~P x  e.  u  /\  A. y  e.  u  { x ,  y }  e.  u ) ) }
df-wunc 8205 |- wUniCl  =  ( x  e. 
_V  |->  |^| { u  e. WUni  |  x  C_  u }
)
ctsk 8250 class  Tarski
df-tsk 8251 |- 
Tarski  =  { y  |  ( A. z  e.  y  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )  /\  A. z  e.  ~P  y
( z  ~~  y  \/  z  e.  y
) ) }
cgru 8292 class  Univ
df-gru 8293 |- 
Univ  =  { u  |  ( Tr  u  /\  A. x  e.  u  ( ~P x  e.  u  /\  A. y  e.  u  { x ,  y }  e.  u  /\  A. y  e.  ( u  ^m  x ) U. ran  y  e.  u
) ) }
ax-groth 8325 |- 
E. y ( x  e.  y  /\  A. z  e.  y  ( A. w ( w  C_  z  ->  w  e.  y )  /\  E. w  e.  y  A. v
( v  C_  z  ->  v  e.  w ) )  /\  A. z
( z  C_  y  ->  ( z  ~~  y  \/  z  e.  y
) ) )
ctskm 8339 class  tarskiMap
df-tskm 8340 |-  tarskiMap 
=  ( x  e. 
_V  |->  |^| { y  e. 
Tarski  |  x  e.  y } )
cnpi 8346 class  N.
cpli 8347 class  +N
cmi 8348 class  .N
clti 8349 class  <N
cplpq 8350 class  +pQ
cmpq 8351 class  .pQ
cltpq 8352 class  <pQ
ceq 8353 class  ~Q
cnq 8354 class  Q.
c1q 8355 class  1Q
cerq 8356 class  /Q
cplq 8357 class  +Q
cmq 8358 class  .Q
crq 8359 class  *Q
cltq 8360 class  <Q
cnp 8361 class  P.
c1p 8362 class  1P
cpp 8363 class  +P.
cmp 8364 class  .P.
cltp 8365 class  <P
cplpr 8366 class  +pR
cmpr 8367 class  .pR
cer 8368 class  ~R
cnr 8369 class  R.
c0r 8370 class  0R
c1r 8371 class  1R
cm1r 8372 class  -1R
cplr 8373 class  +R
cmr 8374 class  .R
cltr 8375 class  <R
df-ni 8376 |-  N.  =  ( om  \  { (/) } )
df-pli 8377 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 8378 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 8379 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 8412 |- 
+pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( ( 1st `  x )  .N  ( 2nd `  y
) )  +N  (
( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-mpq 8413 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 8414 |- 
<pQ  =  { <. x ,  y >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( ( 1st `  x )  .N  ( 2nd `  y ) ) 
<N  ( ( 1st `  y
)  .N  ( 2nd `  x ) ) ) }
df-enq 8415 |- 
~Q  =  { <. x ,  y >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u
)  =  ( w  .N  v ) ) ) }
df-nq 8416 |-  Q.  =  { x  e.  ( N.  X.  N. )  |  A. y  e.  ( N.  X.  N. ) ( x  ~Q  y  ->  -.  ( 2nd `  y )  <N  ( 2nd `  x ) ) }
df-erq 8417 |- 
/Q  =  (  ~Q  i^i  ( ( N.  X.  N. )  X.  Q. )
)
df-plq 8418 |- 
+Q  =  ( ( /Q  o.  +pQ  )  |`  ( Q.  X.  Q. ) )
df-mq 8419 |-  .Q  =  ( ( /Q  o.  .pQ  )  |`  ( Q.  X.  Q. ) )
df-1nq 8420 |-  1Q  =  <. 1o ,  1o >.
df-rq 8421 |-  *Q  =  ( `'  .Q  " { 1Q } )
df-ltnq 8422 |- 
<Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
df-np 8485 |-  P.  =  { x  |  ( ( (/)  C.  x  /\  x  C.  Q. )  /\  A. y  e.  x  ( A. z ( z  <Q 
y  ->  z  e.  x )  /\  E. z  e.  x  y  <Q  z ) ) }
df-1p 8486 |-  1P  =  { x  |  x  <Q  1Q }
df-plp 8487 |- 
+P.  =  ( x  e.  P. ,  y  e.  P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  +Q  u ) } )
df-mp 8488 |-  .P.  =  ( x  e. 
P. ,  y  e. 
P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  .Q  u ) } )
df-ltp 8489 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  x  C.  y ) }
df-plpr 8559 |- 
+pR  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  ( P.  X.  P. )  /\  y  e.  ( P.  X.  P. ) )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( w  +P.  u ) ,  ( v  +P.  f ) >. )
) }
df-mpr 8560 |- 
.pR  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  ( P.  X.  P. )  /\  y  e.  ( P.  X.  P. ) )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. ) ) }
df-enr 8561 |- 
~R  =  { <. x ,  y >.  |  ( ( x  e.  ( P.  X.  P. )  /\  y  e.  ( P.  X.  P. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  +P.  u
)  =  ( w  +P.  v ) ) ) }
df-nr 8562 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 8563 |- 
+R  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  R.  /\  y  e.  R. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ]  ~R  /\  y  =  [ <. u ,  f
>. ]  ~R  )  /\  z  =  [ ( <. w ,  v >.  +pR  <. u ,  f
>. ) ]  ~R  )
) }
df-mr 8564 |-  .R  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  R.  /\  y  e.  R. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ]  ~R  /\  y  =  [ <. u ,  f
>. ]  ~R  )  /\  z  =  [ ( <. w ,  v >.  .pR  <. u ,  f
>. ) ]  ~R  )
) }
df-ltr 8565 |- 
<R  =  { <. x ,  y >.  |  ( ( x  e.  R.  /\  y  e.  R. )  /\  E. z E. w E. v E. u ( ( x  =  [ <. z ,  w >. ]  ~R  /\  y  =  [ <. v ,  u >. ]  ~R  )  /\  ( z  +P.  u
)  <P  ( w  +P.  v ) ) ) }
df-0r 8566 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 8567 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 8568 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 8615 class  CC
cr 8616 class  RR
cc0 8617 class  0
c1 8618 class  1
ci 8619 class  _i
caddc 8620 class  +
cltrr 8621 class  <RR
cmul 8622 class  x.
df-c 8623 |-  CC  =  ( R.  X.  R. )
df-0 8624 |-  0  =  <. 0R ,  0R >.
df-1 8625 |-  1  =  <. 1R ,  0R >.
df-i 8626 |-  _i  =  <. 0R ,  1R >.
df-r 8627 |-  RR  =  ( R.  X.  { 0R } )
df-plus 8628 |-  +  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  CC  /\  y  e.  CC )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( w  +R  u ) ,  ( v  +R  f ) >. )
) }
df-mul 8629 |-  x.  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  CC  /\  y  e.  CC )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .R  u
)  +R  ( -1R 
.R  ( v  .R  f ) ) ) ,  ( ( v  .R  u )  +R  ( w  .R  f
) ) >. )
) }
df-lt 8630 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 8673 |-  CC  e.  _V
ax-resscn 8674 |-  RR  C_  CC
ax-1cn 8675 |-  1  e.  CC
ax-icn 8676 |-  _i  e.  CC
ax-addcl 8677 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 8678 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 8679 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 8680 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-mulcom 8681 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 8682 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 8683 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 8684 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 8685 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-1ne0 8686 |-  1  =/=  0
ax-1rid 8687 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-rnegex 8688 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-rrecex 8689 |-  ( ( A  e.  RR  /\  A  =/=  0 )  ->  E. x  e.  RR  ( A  x.  x )  =  1 )
ax-cnre 8690 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-lttri 8691 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <RR  B  <->  -.  ( A  =  B  \/  B  <RR  A ) ) )
ax-pre-lttrn 8692 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-ltadd 8693 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 8694 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-sup 8695 |-  ( ( A  C_  RR  /\  A  =/=  (/)  /\  E. x  e.  RR  A. y  e.  A  y  <RR  x )  ->  E. x  e.  RR  ( A. y  e.  A  -.  x  <RR  y  /\  A. y  e.  RR  ( y  <RR  x  ->  E. z  e.  A  y  <RR  z ) ) )
ax-addf 8696 |-  +  : ( CC 
X.  CC ) --> CC
ax-mulf 8697 |-  x.  : ( CC 
X.  CC ) --> CC
cpnf 8744 class  +oo
cmnf 8745 class  -oo
cxr 8746 class  RR*
clt 8747 class  <
cle 8748 class  <_
df-pnf 8749 |- 
+oo  =  ~P U. CC
df-mnf 8750 |- 
-oo  =  ~P  +oo
df-xr 8751 |-  RR*  =  ( RR  u.  { 
+oo ,  -oo } )
df-ltxr 8752 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { 
-oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) ) )
df-le 8753 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 8917 class  -
cneg 8918 class  -u A
df-sub 8919 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC ( y  +  z )  =  x ) )
df-neg 8920 |-  -u A  =  (
0  -  A )
cdiv 9303 class  /
df-div 9304 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC ( y  x.  z
)  =  x ) )
cn 9626 class  NN
df-n 9627 |-  NN  =  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )
c2 9675 class  2
c3 9676 class  3
c4 9677 class  4
c5 9678 class  5
c6 9679 class  6
c7 9680 class  7
c8 9681 class  8
c9 9682 class  9
c10 9683 class  10
df-2 9684 |-  2  =  ( 1  +  1 )
df-3 9685 |-  3  =  ( 2  +  1 )
df-4 9686 |-  4  =  ( 3  +  1 )
df-5 9687 |-  5  =  ( 4  +  1 )
df-6 9688 |-  6  =  ( 5  +  1 )
df-7 9689 |-  7  =  ( 6  +  1 )
df-8 9690 |-  8  =  ( 7  +  1 )
df-9 9691 |-  9  =  ( 8  +  1 )
df-10 9692 |-  10  =  ( 9  +  1 )
cn0 9844 class  NN0
df-n0 9845 |-  NN0  =  ( NN  u.  { 0 } )
cz 9903 class  ZZ
df-z 9904 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 10003 class ; A B
df-dec 10004 |- ; A B  =  ( ( 10  x.  A )  +  B )
cuz 10109 class  ZZ>=
df-uz 10110 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 10195 class  QQ
df-q 10196 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 10233 class  RR+
df-rp 10234 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 10328 class  - e A
cxad 10329 class  + e
cxmu 10330 class  x e
df-xneg 10331 |-  - e A  =  if ( A  =  +oo , 
-oo ,  if ( A  =  -oo ,  +oo , 
-u A ) )
df-xadd 10332 |-  + e  =  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  =  +oo ,  if ( y  =  -oo ,  0 ,  +oo ) ,  if ( x  = 
-oo ,  if (
y  =  +oo , 
0 ,  -oo ) ,  if ( y  = 
+oo ,  +oo ,  if ( y  =  -oo , 
-oo ,  ( x  +  y ) ) ) ) ) )
df-xmul 10333 |-  x e  =  ( x  e.  RR* ,  y  e.  RR*  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 ,  if ( ( ( ( 0  <  y  /\  x  =  +oo )  \/  ( y  <  0  /\  x  = 
-oo ) )  \/  ( ( 0  < 
x  /\  y  =  +oo )  \/  (
x  <  0  /\  y  =  -oo ) ) ) ,  +oo ,  if ( ( ( ( 0  <  y  /\  x  =  -oo )  \/  ( y  <  0  /\  x  =  +oo ) )  \/  (
( 0  <  x  /\  y  =  -oo )  \/  ( x  <  0  /\  y  = 
+oo ) ) ) ,  -oo ,  ( x  x.  y ) ) ) ) )
cioo 10534 class  (,)
cioc 10535 class  (,]
cico 10536 class  [,)
cicc 10537 class  [,]
df-ioo 10538 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 10539 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 10540 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 10541 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 10660 class  ...
df-fz 10661 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 10748 class ..^
df-fzo 10749 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 10802 class  |_
df-fl 10803 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
cmo 10851 class  mod
df-mod 10852 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 10924 class  seq 
M (  .+  ,  F )
df-seq 10925 |- 
seq  M (  .+  ,  F )  =  ( rec ( ( x  e.  _V ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. ) " om )
cexp 10982 class  ^
df-exp 10983 |- 
^  =  ( x  e.  CC ,  y  e.  ZZ  |->  if ( y  =  0 ,  1 ,  if ( 0  <  y ,  (  seq  1 (  x.  ,  ( NN 
X.  { x }
) ) `  y
) ,  ( 1  /  (  seq  1
(  x.  ,  ( NN  X.  { x } ) ) `  -u y ) ) ) ) )
cfa 11166 class  !
df-fac 11167 |-  !  =  ( {
<. 0 ,  1
>. }  u.  seq  1
(  x.  ,  _I  ) )
cbc 11193 class  _C
df-bc 11194 |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n
)  /  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) ) ) ,  0 ) )
chash 11215 class  #
df-hash 11216 |-  #  =  ( (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om )  o.  card )  u.  ( ( _V  \  Fin )  X. 
{  +oo } ) )
cword 11280 class Word  S
cconcat 11281 class concat
cs1 11282 class  <" A ">
csubstr 11283 class substr
csplice 11284 class splice
creverse 11285 class reverse
df-word 11286 |- Word  S  =  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
df-concat 11287 |- concat  =  ( s  e. 
_V ,  t  e. 
_V  |->  ( x  e.  ( 0..^ ( (
# `  s )  +  ( # `  t
) ) )  |->  if ( x  e.  ( 0..^ ( # `  s
) ) ,  ( s `  x ) ,  ( t `  ( x  -  ( # `
 s ) ) ) ) ) )
df-s1 11288 |-  <" A ">  =  { <. 0 ,  (  _I  `  A )
>. }
df-substr 11289 |- substr  =  ( s  e. 
_V ,  b  e.  ( ZZ  X.  ZZ )  |->  if ( ( ( 1st `  b
)..^ ( 2nd `  b
) )  C_  dom  s ,  ( x  e.  ( 0..^ ( ( 2nd `  b )  -  ( 1st `  b
) ) )  |->  ( s `  ( x  +  ( 1st `  b
) ) ) ) ,  (/) ) )
df-splice 11290 |- splice  =  ( s  e. 
_V ,  b  e. 
_V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) ) >.
) concat  ( 2nd `  b
) ) concat  ( s substr  <.
( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
df-reverse 11291 |- reverse  =  ( s  e. 
_V  |->  ( x  e.  ( 0..^ ( # `  s ) )  |->  ( s `  ( ( ( # `  s
)  -  1 )  -  x ) ) ) )
cs2 11368 class  <" A B ">
cs3 11369 class  <" A B C ">
cs4 11370 class  <" A B C D ">
cs5 11371 class  <" A B C D E ">
cs6 11372 class  <" A B C D E F ">
cs7 11373 class  <" A B C D E F G ">
cs8 11374 class  <" A B C D E F G H ">
df-s2 11375 |-  <" A B ">  =  ( <" A "> concat  <" B "> )
df-s3 11376 |-  <" A B C ">  =  (
<" A B "> concat 
<" C "> )
df-s4 11377 |-  <" A B C D ">  =  ( <" A B C "> concat  <" D "> )
df-s5 11378 |-  <" A B C D E ">  =  ( <" A B C D "> concat  <" E "> )
df-s6 11379 |-  <" A B C D E F ">  =  ( <" A B C D E "> concat 
<" F "> )
df-s7 11380 |-  <" A B C D E F G ">  =  (
<" A B C D E F "> concat 
<" G "> )
df-s8 11381 |-  <" A B C D E F G H ">  =  ( <" A B C D E F G "> concat  <" H "> )
cshi 11438 class  shift
df-shft 11439 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 11458 class  *
cre 11459 class  Re
cim 11460 class  Im
df-cj 11461 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 11462 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 11463 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqr 11595 class  sqr
cabs 11596 class  abs
df-sqr 11597 |- 
sqr  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
df-abs 11598 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
clsp 11821 class  limsup
df-limsup 11822 |- 
limsup  =  ( x  e. 
_V  |->  sup ( ran  ( 
k  e.  RR  |->  sup ( ( ( x
" ( k [,) 
+oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  ) )
cli 11835 class  ~~>
crli 11836 class  ~~> r
co1 11837 class  O ( 1 )
clo1 11838 class  <_
O ( 1 )
df-clim 11839 |-  ~~>  =  { <. f ,  y
>.  |  ( y  e.  CC  /\  A. x  e.  RR+  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j )
( ( f `  k )  e.  CC  /\  ( abs `  (
( f `  k
)  -  y ) )  <  x ) ) }
df-rlim 11840 |-  ~~> r  =  { <. f ,  x >.  |  (
( f  e.  ( CC  ^pm  RR )  /\  x  e.  CC )  /\  A. y  e.  RR+  E. z  e.  RR  A. w  e.  dom  f
( z  <_  w  ->  ( abs `  (
( f `  w
)  -  x ) )  <  y ) ) }
df-o1 11841 |-  O ( 1 )  =  { f  e.  ( CC  ^pm  RR )  |  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,)  +oo ) ) ( abs `  ( f `  y
) )  <_  m }
df-lo1 11842 |- 
<_ O ( 1 )  =  { f  e.  ( RR  ^pm  RR )  |  E. x  e.  RR  E. m  e.  RR  A. y  e.  ( dom  f  i^i  ( x [,)  +oo ) ) ( f `
 y )  <_  m }
csu 12035 class  sum_ k  e.  A  B
df-sum 12036 |- 
sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq  m (  +  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) ) )  ~~>  x )  \/ 
E. m  e.  NN  E. f ( f : ( 1 ... m
)
-1-1-onto-> A  /\  x  =  (  seq  1 (  +  ,  ( n  e.  NN  |->  [_ ( f `  n )  /  k ]_ B ) ) `  m ) ) ) )
ce 12217 class  exp
ceu 12218 class  _e
csin 12219 class  sin
ccos 12220 class  cos
ctan 12221 class  tan
cpi 12222 class  pi
df-ef 12223 |-  exp  =  ( x  e.  CC  |->  sum_ k  e.  NN0  ( ( x ^
k )  /  ( ! `  k )
) )
df-e 12224 |-  _e  =  ( exp `  1 )
df-sin 12225 |- 
sin  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  -  ( exp `  ( -u _i  x.  x ) ) )  /  ( 2  x.  _i ) ) )
df-cos 12226 |- 
cos  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  +  ( exp `  ( -u _i  x.  x ) ) )  /  2 ) )
df-tan 12227 |- 
tan  =  ( x  e.  ( `' cos " ( CC  \  {
0 } ) ) 
|->  ( ( sin `  x
)  /  ( cos `  x ) ) )
df-pi 12228 |-  pi  =  sup (
( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  `'  <  )
cdivides 12405 class  ||
df-divides 12406 |- 
||  =  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
cbits 12484 class bits
csad 12485 class sadd
csmu 12486 class smul
df-bits 12487 |- bits 
=  ( n  e.  ZZ  |->  { m  e. 
NN0  |  -.  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) ) } )
df-sad 12516 |- sadd 
=  ( x  e. 
~P NN0 ,  y  e. 
~P NN0  |->  { k  e.  NN0  | hadd (
k  e.  x ,  k  e.  y ,  (/)  e.  (  seq  0
( ( c  e.  2o ,  m  e. 
NN0  |->  if (cadd ( m  e.  x ,  m  e.  y ,  (/)  e.  c ) ,  1o ,  (/) ) ) ,  ( n  e. 
NN0  |->  if ( n  =  0 ,  (/) ,  ( n  -  1 ) ) ) ) `
 k ) ) } )
df-smu 12541 |- smul 
=  ( x  e. 
~P NN0 ,  y  e. 
~P NN0  |->  { k  e.  NN0  |  k  e.  (  seq  0
( ( p  e. 
~P NN0 ,  m  e. 
NN0  |->  ( p sadd  {
n  e.  NN0  | 
( m  e.  x  /\  ( n  -  m
)  e.  y ) } ) ) ,  ( n  e.  NN0  |->  if ( n  =  0 ,  (/) ,  ( n  -  1 ) ) ) ) `  (
k  +  1 ) ) } )
cgcd 12559 class  gcd
df-gcd 12560 |- 
gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
cprime 12632 class  Prime
df-prime 12633 |- 
Prime  =  { p  e.  NN  |  { n  e.  NN  |  n  ||  p }  ~~  2o }
cnumer 12678 class numer
cdenom 12679 class denom
df-numer 12680 |- numer  =  ( y  e.  QQ  |->  ( 1st `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
df-denom 12681 |- denom  =  ( y  e.  QQ  |->  ( 2nd `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
codz 12705 class  od
Z
cphi 12706 class  phi
df-odz 12707 |-  od Z  =  ( n  e.  NN  |->  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |->  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  ) ) )
df-phi 12708 |- 
phi  =  ( n  e.  NN  |->  ( # `  { x  e.  ( 1 ... n )  |  ( x  gcd  n )  =  1 } ) )
cpc 12763 class  pCnt
df-pc 12764 |-  pCnt 
=  ( p  e. 
Prime ,  r  e.  QQ  |->  if ( r  =  0 ,  +oo ,  ( iota z E. x  e.  ZZ  E. y  e.  NN  (
r  =  ( x  /  y )  /\  z  =  ( sup ( { n  e.  NN0  |  ( p ^ n
)  ||  x } ,  RR ,  <  )  -  sup ( { n  e.  NN0  |  ( p ^ n )  ||  y } ,  RR ,  <  ) ) ) ) ) )
cgz 12850 class  ZZ [ _i ]
df-gz 12851 |-  ZZ [ _i ]  =  { x  e.  CC  |  ( ( Re
`  x )  e.  ZZ  /\  ( Im
`  x )  e.  ZZ ) }
cvdwa 12886 class AP
cvdwm 12887 class MonoAP
cvdwp 12888 class PolyAP
df-vdwap 12889 |- AP 
=  ( k  e. 
NN0  |->  ( a  e.  NN ,  d  e.  NN  |->  ran  (  m  e.  ( 0 ... (
k  -  1 ) )  |->  ( a  +  ( m  x.  d
) ) ) ) )
df-vdwmc 12890 |- MonoAP  =  { <. k ,  f
>.  |  E. c
( ran  (AP `  k
)  i^i  ~P ( `' f " {
c } ) )  =/=  (/) }
df-vdwpc 12891 |- PolyAP  =  { <. <. m ,  k
>. ,  f >.  |  E. a  e.  NN  E. d  e.  ( NN 
^m  ( 1 ... m ) ) ( A. i  e.  ( 1 ... m ) ( ( a  +  ( d `  i
) ) (AP `  k ) ( d `
 i ) ) 
C_  ( `' f
" { ( f `
 ( a  +  ( d `  i
) ) ) } )  /\  ( # `  ran  (  i  e.  ( 1 ... m
)  |->  ( f `  ( a  +  ( d `  i ) ) ) ) )  =  m ) }
cram 12920 class Ramsey
df-ram 12922 |- Ramsey  =  ( m  e. 
NN0 ,  r  e.  _V  |->  sup ( { n  e.  NN0  |  A. s
( n  <_  ( # `
 s )  ->  A. f  e.  ( dom  r  ^m  { y  e.  ~P s  |  ( # `  y
)  =  m }
) E. c  e. 
dom  r E. x  e.  ~P  s ( ( r `  c )  <_  ( # `  x
)  /\  A. y  e.  ~P  x ( (
# `  y )  =  m  ->  ( f `
 y )  =  c ) ) ) } ,  RR* ,  `'  <  ) )
cstr 13018 class Struct
cnx 13019 class  ndx
csts 13020 class sSet
cslot 13021 class Slot  A
cbs 13022 class  Base
cress 13023 classs
df-struct 13024 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( f 
\  { (/) } )  /\  dom  f  C_  ( ... `  x ) ) }
df-ndx 13025 |- 
ndx  =  (  _I  |`  NN )
df-slot 13026 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
df-base 13027 |- 
Base  = Slot  1
df-sets 13028 |- sSet 
=  ( s  e. 
_V ,  e  e. 
_V  |->  ( ( s  |`  ( _V  \  dom  {  e } ) )  u.  { e } ) )
df-ress 13029 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  if ( ( Base `  w
)  C_  x ,  w ,  ( w sSet  <.
( Base `  ndx ) ,  ( x  i^i  ( Base `  w ) )
>. ) ) )
cplusg 13082 class  +g
cmulr 13083 class  .r
cstv 13084 class  * r
csca 13085 class Scalar
cvsca 13086 class  .s
cip 13087 class  .i
cts 13088 class TopSet
cple 13089 class  le
coc 13090 class  oc
cds 13091 class  dist
cunif 13092 class  Unif
chom 13093 class  Hom
cco 13094 class comp
df-plusg 13095 |- 
+g  = Slot  2
df-mulr 13096 |- 
.r  = Slot  3
df-starv 13097 |-  * r  = Slot  4
df-sca 13098 |- Scalar  = Slot  5
df-vsca 13099 |-  .s  = Slot  6
df-ip 13100 |-  .i  = Slot  8
df-tset 13101 |- TopSet  = Slot  9
df-ple 13102 |- 
le  = Slot  10
df-ocomp 13103 |-  oc  = Slot ; 1 1
df-ds 13104 |-  dist 
= Slot ; 1 2
df-unif 13105 |- 
Unif  = Slot ; 1 3
df-hom 13106 |- 
Hom  = Slot ; 1 4
df-cco 13107 |- comp 
= Slot ; 1 5
crest 13199 classt
ctopn 13200 class  TopOpen
df-rest 13201 |-t  =  ( j  e.  _V ,  x  e.  _V  |->  ran  (  y  e.  j  |->  ( y  i^i  x ) ) )
df-topn 13202 |-  TopOpen  =  ( w  e. 
_V  |->  ( (TopSet `  w )t  ( Base `  w
) ) )
ctg 13216 class  topGen
cpt 13217 class  Xt_
df-topgen 13218 |- 
topGen  =  ( x  e. 
_V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
df-pt 13219 |-  Xt_  =  ( f  e. 
_V  |->  ( topGen `  {
x  |  E. g
( ( g  Fn 
dom  f  /\  A. y  e.  dom  f ( g `  y )  e.  ( f `  y )  /\  E. z  e.  Fin  A. y  e.  ( dom  f  \ 
z ) ( g `
 y )  = 
U. ( f `  y ) )  /\  x  =  X_ y  e. 
dom  f ( g `
 y ) ) } ) )
cprds 13220 class  X_s
cpws 13221 class  ^s
df-prds 13222 |-  X_s  =  ( s  e. 
_V ,  r  e. 
_V  |->  [_ X_ x  e.  dom  r ( Base `  (
r `  x )
)  /  v ]_ [_ ( f  e.  v ,  g  e.  v 
|->  X_ x  e.  dom  r ( ( f `
 x ) (  Hom  `  ( r `  x ) ) ( g `  x ) ) )  /  h ]_ ( ( { <. (
Base `  ndx ) ,  v >. ,  <. ( +g  `  ndx ) ,  ( f  e.  v ,  g  e.  v 
|->  ( x  e.  dom  r  |->  ( ( f `
 x ) ( +g  `  ( r `
 x ) ) ( g `  x
) ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( f  e.  v ,  g  e.  v  |->  ( x  e.  dom  r  |->  ( ( f `  x ) ( .r
`  ( r `  x ) ) ( g `  x ) ) ) ) >. }  u.  { <. (Scalar ` 
ndx ) ,  s
>. ,  <. ( .s
`  ndx ) ,  ( f  e.  ( Base `  s ) ,  g  e.  v  |->  ( x  e.  dom  r  |->  ( f ( .s `  ( r `  x
) ) ( g `
 x ) ) ) ) >. } )  u.  ( { <. (TopSet `  ndx ) ,  (
Xt_ `  ( TopOpen  o.  r
) ) >. ,  <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  v  /\  A. x  e.  dom  r ( f `  x ) ( le `  (
r `  x )
) ( g `  x ) ) }
>. ,  <. ( dist `  ndx ) ,  ( f  e.  v ,  g  e.  v  |->  sup ( ( ran  (  x  e.  dom  r  |->  ( ( f `  x
) ( dist `  (
r `  x )
) ( g `  x ) ) )  u.  { 0 } ) ,  RR* ,  <  ) ) >. }  u.  { <. (  Hom  `  ndx ) ,  h >. , 
<. (comp `  ndx ) ,  ( a  e.  ( v  X.  v ) ,  c  e.  v 
|->  ( d  e.  ( c h ( 2nd `  a ) ) ,  e  e.  ( h `
 a )  |->  ( x  e.  dom  r  |->  ( ( d `  x ) ( <.
( ( 1st `  a
) `  x ) ,  ( ( 2nd `  a ) `  x
) >. (comp `  (
r `  x )
) ( c `  x ) ) ( e `  x ) ) ) ) )
>. } ) ) )
df-pws 13224 |- 
^s  =  ( r  e. 
_V ,  i  e. 
_V  |->  ( (Scalar `  r ) X_s ( i  X.  {
r } ) ) )
cordt 13272 class ordTop
cxrs 13273 class  RR* s
c0g 13274 class  0g
cgsu 13275 class  gsumg
df-ordt 13276 |- ordTop  =  ( r  e. 
_V  |->  ( topGen `  ( fi `  ( { dom  r }  u.  ran  ( ( x  e. 
dom  r  |->  { y  e.  dom  r  |  -.  y r x } )  u.  (
x  e.  dom  r  |->  { y  e.  dom  r  |  -.  x
r y } ) ) ) ) ) )
df-xrs 13277 |- 
RR* s  =  ( { <. ( Base `  ndx ) ,  RR* >. ,  <. ( +g  `  ndx ) ,  + e >. ,  <. ( .r `  ndx ) ,  x e >. }  u.  {
<. (TopSet `  ndx ) ,  (ordTop `  <_  ) >. ,  <. ( le `  ndx ) ,  <_  >. ,  <. (
dist `  ndx ) ,  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  <_  y , 
( y + e  - e x ) ,  ( x + e  - e y ) ) ) >. } )
df-0g 13278 |-  0g  =  ( g  e.  _V  |->  ( iota e
( e  e.  (
Base `  g )  /\  A. x  e.  (
Base `  g )
( ( e ( +g  `  g ) x )  =  x  /\  ( x ( +g  `  g ) e )  =  x ) ) ) )
df-gsum 13279 |- 
gsumg  =  ( w  e. 
_V ,  f  e. 
_V  |->  [_ { x  e.  ( Base `  w
)  |  A. y  e.  ( Base `  w
) ( ( x ( +g  `  w
) y )  =  y  /\  ( y ( +g  `  w
) x )  =  y ) }  / 
o ]_ if ( ran  f  C_  o , 
( 0g `  w
) ,  if ( dom  f  e.  ran  ...
,  ( iota x E. m E. n  e.  ( ZZ>= `  m )
( dom  f  =  ( m ... n
)  /\  x  =  (  seq  m ( ( +g  `  w ) ,  f ) `  n ) ) ) ,  ( iota x E. g [. ( `' f " ( _V 
\  o ) )  /  y ]. (
g : ( 1 ... ( # `  y
) ) -1-1-onto-> y  /\  x  =  (  seq  1
( ( +g  `  w
) ,  ( f  o.  g ) ) `
 ( # `  y
) ) ) ) ) ) )
cqtop 13280 class qTop
cimas 13281 class  "s
cqus 13282 class  /.s
cxps 13283 class  X.s
df-qtop 13284 |- qTop 
=  ( j  e. 
_V ,  f  e. 
_V  |->  { s  e. 
~P ( f " U. j )  |  ( ( `' f "
s )  i^i  U. j )  e.  j } )
df-imas 13285 |-  "s  =  ( f  e. 
_V ,  r  e. 
_V  |->  [_ ( Base `  r
)  /  v ]_ ( ( { <. (
Base `  ndx ) ,  ran  f >. ,  <. ( +g  `  ndx ) ,  U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( +g  `  r ) q ) ) >. } >. ,  <. ( .r `  ndx ) ,  U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >. }  u.  { <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >. ,  <. ( .s `  ndx ) ,  U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >. } )  u. 
{ <. (TopSet `  ndx ) ,  ( ( TopOpen
`  r ) qTop  f
) >. ,  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r
) )  o.  `' f ) >. ,  <. (
dist `  ndx ) ,  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  (  g  e.  { h  e.  ( ( v  X.  v )  ^m  ( 1 ... n ) )  |  ( ( f `  ( 1st `  ( h `
 1 ) ) )  =  x  /\  ( f `  ( 2nd `  ( h `  n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) ) >. } ) )
df-divs 13286 |- 
/.s 
=  ( r  e. 
_V ,  e  e. 
_V  |->  ( ( x  e.  ( Base `  r
)  |->  [ x ]
e )  "s  r )
)
df-xps 13287 |- 
X.s 
=  ( r  e. 
_V ,  s  e. 
_V  |->  ( `' ( x  e.  ( Base `  r ) ,  y  e.  ( Base `  s
)  |->  `' ( { x }  +c  {
y } ) ) 
"s  ( (Scalar `  r
) X_s `' ( { r }  +c  { s } ) ) ) )
cmre 13358 class Moore
cmrc 13359 class mrCls
cacs 13360 class ACS
df-mre 13361 |- Moore  =  ( x  e. 
_V  |->  { c  e. 
~P ~P x  |  ( x  e.  c  /\  A. s  e. 
~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
df-mrc 13362 |- mrCls  =  ( c  e. 
U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^|
{ s  e.  c  |  x  C_  s } ) )
df-acs 13363 |- ACS 
=  ( x  e. 
_V  |->  { c  e.  (Moore `  x )  |  E. f ( f : ~P x --> ~P x  /\  A. s  e.  ~P  x ( s  e.  c  <->  U. ( f "
( ~P s  i^i 
Fin ) )  C_  s ) ) } )
ccat 13410 class  Cat
ccid 13411 class  Id
chomf 13412 class  Homf
ccomf 13413 class compf
df-cat 13414 |- 
Cat  =  { c  |  [. ( Base `  c )  /  b ]. [. (  Hom  `  c
)  /  h ]. [. (comp `  c )  /  o ]. A. x  e.  b  ( E. g  e.  (
x h x ) A. y  e.  b  ( A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f  /\  A. f  e.  ( x h y ) ( f ( <. x ,  x >. o y ) g )  =  f )  /\  A. y  e.  b  A. z  e.  b  A. f  e.  ( x h y ) A. g  e.  ( y h z ) ( ( g ( <. x ,  y
>. o z ) f )  e.  ( x h z )  /\  A. w  e.  b  A. k  e.  ( z
h w ) ( ( k ( <.
y ,  z >.
o w ) g ) ( <. x ,  y >. o
w ) f )  =  ( k (
<. x ,  z >.
o w ) ( g ( <. x ,  y >. o
z ) f ) ) ) ) }
df-cid 13415 |-  Id  =  ( c  e.  Cat  |->  [_ ( Base `  c )  / 
b ]_ [_ (  Hom  `  c )  /  h ]_ [_ (comp `  c
)  /  o ]_ ( x  e.  b  |->  ( iota_ g  e.  ( x h x ) A. y  e.  b  ( A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f  /\  A. f  e.  ( x h y ) ( f ( <. x ,  x >. o y ) g )  =  f ) ) ) )
df-homf 13416 |- 
Homf 
=  ( c  e. 
_V  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( x (  Hom  `  c )
y ) ) )
df-comf 13417 |- compf  =  ( c  e.  _V  |->  ( x  e.  (
( Base `  c )  X.  ( Base `  c
) ) ,  y  e.  ( Base `  c
)  |->  ( g  e.  ( ( 2nd `  x
) (  Hom  `  c
) y ) ,  f  e.  ( (  Hom  `  c ) `  x )  |->  ( g ( x (comp `  c ) y ) f ) ) ) )
coppc 13458 class oppCat
df-oppc 13459 |- oppCat  =  ( f  e. 
_V  |->  ( ( f sSet  <. (  Hom  `  ndx ) , tpos  (  Hom  `  f
) >. ) sSet  <. (comp ` 
ndx ) ,  ( u  e.  ( (
Base `  f )  X.  ( Base `  f
) ) ,  z  e.  ( Base `  f
)  |-> tpos  ( <. z ,  ( 2nd `  u )
>. (comp `  f )
( 1st `  u
) ) ) >.
) )
cmon 13475 class Mono
cepi 13476 class Epi
df-mon 13477 |- Mono 
=  ( c  e. 
Cat  |->  [_ ( Base `  c
)  /  b ]_ [_ (  Hom  `  c
)  /  h ]_ ( x  e.  b ,  y  e.  b  |->  { f  e.  ( x h y )  |  A. z  e.  b  Fun  `' ( g  e.  ( z h x )  |->  ( f ( <. z ,  x >. (comp `  c
) y ) g ) ) } ) )
df-epi 13478 |- Epi 
=  ( c  e. 
Cat  |-> tpos  (Mono `  (oppCat `  c
) ) )
csect 13491 class Sect
cinv 13492 class Inv
ciso 13493 class  Iso
df-sect 13494 |- Sect 
=  ( c  e. 
Cat  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  { <. f ,  g >.  |  [. (  Hom  `  c )  /  h ]. ( ( f  e.  ( x h y )  /\  g  e.  ( y
h x ) )  /\  ( g (
<. x ,  y >.
(comp `  c )
x ) f )  =  ( ( Id
`  c ) `  x ) ) } ) )
df-inv 13495 |- Inv 
=  ( c  e. 
Cat  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( ( x (Sect `  c )
y )  i^i  `' ( y (Sect `  c ) x ) ) ) )
df-iso 13496 |- 
Iso  =  ( c  e.  Cat  |->  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) ) )
cssc 13528 class  C_cat
cresc 13529 class  |`cat
csubc 13530 class Subcat
df-ssc 13531 |-  C_cat 
=  { <. h ,  j >.  |  E. t ( j  Fn  ( t  X.  t
)  /\  E. s  e.  ~P  t h  e.  X_ x  e.  (
s  X.  s ) ~P ( j `  x ) ) }
df-resc 13532 |-  |`cat 
=  ( c  e. 
_V ,  h  e. 
_V  |->  ( ( cs  dom 
dom  h ) sSet  <. (  Hom  `  ndx ) ,  h >. ) )
df-subc 13533 |- Subcat  =  ( c  e. 
Cat  |->  { h  |  ( h  C_cat  (  Homf  `  c )  /\  [. dom  dom  h  /  s ]. A. x  e.  s 
( ( ( Id
`  c ) `  x )  e.  ( x h x )  /\  A. y  e.  s  A. z  e.  s  A. f  e.  ( x h y ) A. g  e.  ( y h z ) ( g (
<. x ,  y >.
(comp `  c )
z ) f )  e.  ( x h z ) ) ) } )
cfunc 13572 class  Func
cidfu 13573 class idfunc
ccofu 13574 class  o.func
cresf 13575 class  |`f
df-func 13576 |- 
Func  =  ( t  e.  Cat ,  u  e. 
Cat  |->  { <. f ,  g >.  |  [. ( Base `  t )  /  b ]. (
f : b --> (
Base `  u )  /\  g  e.  X_ z  e.  ( b  X.  b
) ( ( ( f `  ( 1st `  z ) ) (  Hom  `  u )
( f `  ( 2nd `  z ) ) )  ^m  ( (  Hom  `  t ) `  z ) )  /\  A. x  e.  b  ( ( ( x g x ) `  (
( Id `  t
) `  x )
)  =  ( ( Id `  u ) `
 ( f `  x ) )  /\  A. y  e.  b  A. z  e.  b  A. m  e.  ( x
(  Hom  `  t ) y ) A. n  e.  ( y (  Hom  `  t ) z ) ( ( x g z ) `  (
n ( <. x ,  y >. (comp `  t ) z ) m ) )  =  ( ( ( y g z ) `  n ) ( <.
( f `  x
) ,  ( f `
 y ) >.
(comp `  u )
( f `  z
) ) ( ( x g y ) `
 m ) ) ) ) } )
df-idfu 13577 |- idfunc  =  ( t  e.  Cat  |->  [_ ( Base `  t
)  /  b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
df-cofu 13578 |-  o.func  =  ( g  e. 
_V ,  f  e. 
_V  |->  <. ( ( 1st `  g )  o.  ( 1st `  f ) ) ,  ( x  e. 
dom  dom  ( 2nd `  f
) ,  y  e. 
dom  dom  ( 2nd `  f
)  |->  ( ( ( ( 1st `  f
) `  x )
( 2nd `  g
) ( ( 1st `  f ) `  y
) )  o.  (
x ( 2nd `  f
) y ) ) ) >. )
df-resf 13579 |-  |`f  =  ( f  e. 
_V ,  h  e. 
_V  |->  <. ( ( 1st `  f )  |`  dom  dom  h ) ,  ( x  e.  dom  h  |->  ( ( ( 2nd `  f ) `  x
)  |`  ( h `  x ) ) )
>. )
cful 13620 class Full
cfth 13621 class Faith
df-full 13622 |- Full 
=  ( c  e. 
Cat ,  d  e.  Cat  |->  { <. f ,  g >.  |  ( f ( c  Func  d ) g  /\  A. x  e.  ( Base `  c ) A. y  e.  ( Base `  c
) ran  (  x
g y )  =  ( ( f `  x ) (  Hom  `  d ) ( f `
 y ) ) ) } )
df-fth 13623 |- Faith  =  ( c  e. 
Cat ,  d  e.  Cat  |->  { <. f ,  g >.  |  ( f ( c  Func  d ) g  /\  A. x  e.  ( Base `  c ) A. y  e.  ( Base `  c
) Fun  `' (
x g y ) ) } )
cnat 13659 class Nat
cfuc 13660 class FuncCat
df-nat 13661 |- Nat 
=  ( t  e. 
Cat ,  u  e.  Cat  |->  ( f  e.  ( t  Func  u
) ,  g  e.  ( t  Func  u
)  |->  [_ ( 1st `  f
)  /  r ]_ [_ ( 1st `  g
)  /  s ]_ { a  e.  X_ x  e.  ( Base `  t ) ( ( r `  x ) (  Hom  `  u
) ( s `  x ) )  | 
A. x  e.  (
Base `  t ) A. y  e.  ( Base `  t ) A. h  e.  ( x
(  Hom  `  t ) y ) ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) ) } ) )
df-fuc 13662 |- FuncCat  =  ( t  e. 
Cat ,  u  e.  Cat  |->  { <. ( Base `  ndx ) ,  ( t  Func  u
) >. ,  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
cdoma 13696 class domA
ccoda 13697 class coda
carw 13698 class Nat
choma 13699 class Homa
df-doma 13700 |- domA  =  ( 1st  o.  1st )
df-coda 13701 |- coda  =  ( 2nd  o.  1st )
df-homa 13702 |- Homa  =  ( c  e.  Cat  |->  ( x  e.  (
( Base `  c )  X.  ( Base `  c
) )  |->  ( { x }  X.  (
(  Hom  `  c ) `
 x ) ) ) )
df-arw 13703 |- Nat 
=  ( c  e. 
Cat  |->  U. ran  (Homa `  c
) )
cida 13729 class Ida
ccoa 13730 class compa
df-ida 13731 |- Ida  =  ( c  e.  Cat  |->  ( x  e.  ( Base `  c )  |->  <.
x ,  x ,  ( ( Id `  c ) `  x
) >. ) )
df-coa 13732 |- compa  =  ( c  e.  Cat  |->  ( g  e.  (Nat
`  c ) ,  f  e.  { h  e.  (Nat `  c )  |  (coda
`  h )  =  (domA `  g ) }  |->  <.
(domA `  f ) ,  (coda `  g ) ,  ( ( 2nd `  g
) ( <. (domA `  f ) ,  (domA `  g ) >. (comp `  c ) (coda `  g
) ) ( 2nd `  f ) ) >.
) )
csetc 13751 class  SetCat
df-setc 13752 |- 
SetCat  =  ( u  e. 
_V  |->  { <. ( Base `  ndx ) ,  u >. ,  <. (  Hom  `  ndx ) ,  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x
) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( u  X.  u ) ,  z  e.  u  |->  ( g  e.  ( z  ^m  ( 2nd `  v
) ) ,  f  e.  ( ( 2nd `  v )  ^m  ( 1st `  v ) ) 
|->  ( g  o.  f
) ) ) >. } )
ccatc 13770 class CatCat
df-catc 13771 |- CatCat  =  ( u  e. 
_V  |->  [_ ( u  i^i 
Cat )  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. (  Hom  `  ndx ) ,  ( x  e.  b ,  y  e.  b  |->  ( x  Func  y ) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( b  X.  b ) ,  z  e.  b  |->  ( g  e.  ( ( 2nd `  v ) 
Func  z ) ,  f  e.  (  Func  `  v )  |->  ( g  o.func  f ) ) )
>. } )
cxpc 13786 class  X.c
c1stf 13787 class  1stF
c2ndf 13788 class  2ndF
cprf 13789 class ⟨,⟩F
df-xpc 13790 |- 
X.c 
=  ( r  e. 
_V ,  s  e. 
_V  |->  [_ ( ( Base `  r )  X.  ( Base `  s ) )  /  b ]_ [_ (
u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u
) (  Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) (  Hom  `  s
) ( 2nd `  v
) ) ) )  /  h ]_ { <. ( Base `  ndx ) ,  b >. , 
<. (  Hom  `  ndx ) ,  h >. , 
<. (comp `  ndx ) ,  ( x  e.  ( b  X.  b ) ,  y  e.  b 
|->  ( g  e.  ( ( 2nd `  x
) h y ) ,  f  e.  ( h `  x ) 
|->  <. ( ( 1st `  g ) ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) ) >. } )
df-1stf 13791 |- 
1stF 
=  ( r  e. 
Cat ,  s  e.  Cat  |->  [_ ( ( Base `  r )  X.  ( Base `  s ) )  /  b ]_ <. ( 1st  |`  b ) ,  ( x  e.  b ,  y  e.  b  |->  ( 1st  |`  (
x (  Hom  `  (
r  X.c  s ) ) y ) ) ) >.
)
df-2ndf 13792 |- 
2ndF 
=  ( r  e. 
Cat ,  s  e.  Cat  |->  [_ ( ( Base `  r )  X.  ( Base `  s ) )  /  b ]_ <. ( 2nd  |`  b ) ,  ( x  e.  b ,  y  e.  b  |->  ( 2nd  |`  (
x (  Hom  `  (
r  X.c  s ) ) y ) ) ) >.
)
df-prf 13793 |- ⟨,⟩F  =  ( f  e.  _V , 
g  e.  _V  |->  [_ dom  ( 1st `  f
)  /  b ]_ <. ( x  e.  b 
|->  <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
) ,  ( x  e.  b ,  y  e.  b  |->  ( h  e.  dom  (  x ( 2nd `  f
) y )  |->  <.
( ( x ( 2nd `  f ) y ) `  h
) ,  ( ( x ( 2nd `  g
) y ) `  h ) >. )
) >. )
cevlf 13827 class evalF
ccurf 13828 class curryF
cuncf 13829 class uncurryF
cdiag 13830 class Δfunc
df-evlf 13831 |- evalF  =  ( c  e.  Cat ,  d  e.  Cat  |->  <.
( f  e.  ( c  Func  d ) ,  x  e.  ( Base `  c )  |->  ( ( 1st `  f
) `  x )
) ,  ( x  e.  ( ( c 
Func  d )  X.  ( Base `  c
) ) ,  y  e.  ( ( c 
Func  d )  X.  ( Base `  c
) )  |->  [_ ( 1st `  x )  /  m ]_ [_ ( 1st `  y )  /  n ]_ ( a  e.  ( m ( c Nat  d
) n ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  c
) ( 2nd `  y
) )  |->  ( ( a `  ( 2nd `  y ) ) (
<. ( ( 1st `  m
) `  ( 2nd `  x ) ) ,  ( ( 1st `  m
) `  ( 2nd `  y ) ) >.
(comp `  d )
( ( 1st `  n
) `  ( 2nd `  y ) ) ) ( ( ( 2nd `  x ) ( 2nd `  m ) ( 2nd `  y ) ) `  g ) ) ) ) >. )
df-curf 13832 |- curryF  =  ( e  e.  _V ,  f  e.  _V  |->  [_ ( 1st `  e
)  /  c ]_ [_ ( 2nd `  e
)  /  d ]_ <. ( x  e.  (
Base `  c )  |-> 
<. ( y  e.  (
Base `  d )  |->  ( x ( 1st `  f ) y ) ) ,  ( y  e.  ( Base `  d
) ,  z  e.  ( Base `  d
)  |->  ( g  e.  ( y (  Hom  `  d ) z ) 
|->  ( ( ( Id
`  c ) `  x ) ( <.
x ,  y >.
( 2nd `  f
) <. x ,  z
>. ) g ) ) ) >. ) ,  ( x  e.  ( Base `  c ) ,  y  e.  ( Base `  c
)  |->  ( g  e.  ( x (  Hom  `  c ) y ) 
|->  ( z  e.  (
Base `  d )  |->  ( g ( <.
x ,  z >.
( 2nd `  f
) <. y ,  z
>. ) ( ( Id
`  d ) `  z ) ) ) ) ) >. )
df-uncf 13833 |- uncurryF  =  ( c  e.  _V ,  f  e.  _V  |->  ( ( ( c `
 1 ) evalF  ( c `
 2 ) )  o.func  ( ( f  o.func  ( ( c `  0
)  1stF  ( c `  1
) ) ) ⟨,⟩F  ( ( c ` 
0 )  2ndF  ( c `  1 ) ) ) ) )
df-diag 13834 |- Δfunc  =  ( c  e.  Cat ,  d  e.  Cat  |->  (
<. c ,  d >. curryF  ( c  1stF  d ) ) )
chof 13866 class HomF
cyon 13867 class Yon
df-hof 13868 |- HomF  =  ( c  e.  Cat  |->  <. (  Homf 
`  c ) , 
[_ ( Base `  c
)  /  b ]_ ( x  e.  (
b  X.  b ) ,  y  e.  ( b  X.  b ) 
|->  ( f  e.  ( ( 1st `  y
) (  Hom  `  c
) ( 1st `  x
) ) ,  g  e.  ( ( 2nd `  x ) (  Hom  `  c ) ( 2nd `  y ) )  |->  ( h  e.  ( (  Hom  `  c ) `  x )  |->  ( ( g ( x (comp `  c ) ( 2nd `  y ) ) h ) ( <. ( 1st `  y ) ,  ( 1st `  x
) >. (comp `  c
) ( 2nd `  y
) ) f ) ) ) ) >.
)
df-yon 13869 |- Yon 
=  ( c  e. 
Cat  |->  ( <. c ,  (oppCat `  c ) >. curryF  (HomF `  (oppCat `  c ) ) ) )
cpreset 13904 class  Preset
cdrs 13905 class Dirset
df-preset 13906 |- 
Preset  =  { f  | 
[. ( Base `  f
)  /  b ]. [. ( le `  f
)  /  r ]. A. x  e.  b  A. y  e.  b  A. z  e.  b 
( x r x  /\  ( ( x r y  /\  y
r z )  ->  x r z ) ) }
df-drs 13907 |- Dirset  =  { f