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 3 wff 
-.  ph
wi 4 wff  ( ph  ->  ps )
ax-1 5 |-  ( ph  ->  ( ps  ->  ph ) )
ax-2 6 |-  ( ( ph  ->  ( ps  ->  ch )
)  ->  ( ( ph  ->  ps )  -> 
( ph  ->  ch )
) )
ax-3 7 |-  ( ( -.  ph  ->  -.  ps )  -> 
( ps  ->  ph )
)
ax-mp 8 |- 
ph   &    |-  ( ph  ->  ps )   =>    |- 
ps
wb 177 wff  ( ph  <->  ps )
df-bi 178 |- 
-.  ( ( (
ph 
<->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ph  <->  ps ) ) )
wo 358 wff  ( ph  \/  ps )
wa 359 wff  ( ph  /\  ps )
df-or 360 |-  ( ( ph  \/  ps )  <->  ( -.  ph  ->  ps ) )
df-an 361 |-  ( ( ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
w3o 935 wff  ( ph  \/  ps  \/  ch )
w3a 936 wff  ( ph  /\  ps  /\ 
ch )
df-3or 937 |-  ( ( ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/ 
ch ) )
df-3an 938 |-  ( ( ph  /\  ps  /\  ch )  <->  ( ( ph  /\  ps )  /\  ch ) )
wnan 1296 wff  ( ph  -/\  ps )
df-nan 1297 |-  ( ( ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
wxo 1313 wff  ( ph  \/_  ps )
df-xor 1314 |-  ( ( ph  \/_  ps ) 
<->  -.  ( ph  <->  ps )
)
wtru 1325 wff 
T.
wfal 1326 wff 
F.
df-tru 1328 |-  (  T.  <->  ( ph  <->  ph ) )
df-fal 1329 |-  (  F.  <->  -.  T.  )
whad 1387 wff hadd
( ph ,  ps ,  ch )
wcad 1388 wff cadd
( ph ,  ps ,  ch )
df-had 1389 |-  (hadd ( ph ,  ps ,  ch )  <->  ( ( ph  \/_  ps )  \/_  ch ) )
df-cad 1390 |-  (cadd ( ph ,  ps ,  ch )  <->  ( ( ph  /\  ps )  \/  ( ch  /\  ( ph  \/_  ps ) ) ) )
ax-meredith 1415 |-  ( ( ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -.  th ) )  ->  ch )  ->  ta )  ->  ( ( ta  ->  ph )  -> 
( th  ->  ph )
) )
wal 1549 wff  A. x ph
wex 1550 wff 
E. x ph
df-ex 1551 |-  ( E. x ph  <->  -.  A. x  -.  ph )
wnf 1553 wff 
F/ x ph
df-nf 1554 |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
ax-gen 1555 |- 
ph   =>    |- 
A. x ph
ax-5 1566 |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
ax-17 1626 |-  ( ph  ->  A. x ph )
cv 1651 class  x
wceq 1652 wff 
A  =  B
wsb 1658 wff 
[ y  /  x ] ph
df-sb 1659 |-  ( [ y  /  x ] ph  <->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph ) ) )
ax-9 1666 |-  -.  A. x  -.  x  =  y
ax-8 1687 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
wcel 1725 wff 
A  e.  B
ax-13 1727 |-  ( x  =  y  ->  ( x  e.  z  ->  y  e.  z ) )
ax-14 1729 |-  ( x  =  y  ->  ( z  e.  x  ->  z  e.  y ) )
ax-6 1744 |-  ( -.  A. x ph  ->  A. x  -.  A. x ph )
ax-7 1749 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-11 1761 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-12 1950 |-  ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
)
ax-4 2211 |-  ( A. x ph  ->  ph )
ax-5o 2212 |-  ( A. x ( A. x ph  ->  ps )  ->  ( A. x ph  ->  A. x ps )
)
ax-6o 2213 |-  ( -.  A. x  -.  A. x ph  ->  ph )
ax-9o 2214 |-  ( A. x ( x  =  y  ->  A. x ph )  ->  ph )
ax-10o 2215 |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph ) )
ax-10 2216 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11o 2217 |-  ( -.  A. x  x  =  y  ->  ( x  =  y  -> 
( ph  ->  A. x
( x  =  y  ->  ph ) ) ) )
ax-12o 2218 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  =  y  ->  A. z  x  =  y ) ) )
ax-15 2219 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  e.  y  ->  A. z  x  e.  y ) ) )
ax-16 2220 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
weu 2280 wff 
E! x ph
wmo 2281 wff 
E* x ph
df-eu 2284 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
df-mo 2285 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
ax-7d 2371 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-8d 2372 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-9d1 2373 |- 
-.  A. x  -.  x  =  x
ax-9d2 2374 |- 
-.  A. x  -.  x  =  y
ax-10d 2375 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11d 2376 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-ext 2416 |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
cab 2421 class  { x  |  ph }
df-clab 2422 |-  ( x  e.  {
y  |  ph }  <->  [ x  /  y ]
ph )
df-cleq 2428 |-  ( A. x ( x  e.  y  <->  x  e.  z )  ->  y  =  z )   =>    |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
df-clel 2431 |-  ( A  e.  B  <->  E. x ( x  =  A  /\  x  e.  B ) )
wnfc 2558 wff  F/_ x A
df-nfc 2560 |-  ( F/_ x A  <->  A. y F/ x  y  e.  A )
wne 2598 wff 
A  =/=  B
wnel 2599 wff 
A  e/  B
df-ne 2600 |-  ( A  =/=  B  <->  -.  A  =  B )
df-nel 2601 |-  ( A  e/  B  <->  -.  A  e.  B )
wral 2697 wff  A. x  e.  A  ph
wrex 2698 wff 
E. x  e.  A  ph
wreu 2699 wff 
E! x  e.  A  ph
wrmo 2700 wff 
E* x  e.  A ph
crab 2701 class  { x  e.  A  |  ph }
df-ral 2702 |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
df-rex 2703 |-  ( E. x  e.  A  ph  <->  E. x
( x  e.  A  /\  ph ) )
df-reu 2704 |-  ( E! x  e.  A  ph  <->  E! x
( x  e.  A  /\  ph ) )
df-rmo 2705 |-  ( E* x  e.  A ph  <->  E* x
( x  e.  A  /\  ph ) )
df-rab 2706 |- 
{ x  e.  A  |  ph }  =  {
x  |  ( x  e.  A  /\  ph ) }
cvv 2948 class  _V
df-v 2950 |-  _V  =  { x  |  x  =  x }
wcdeq 3136 wff CondEq ( x  =  y  ->  ph )
df-cdeq 3137 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 3153 wff  [. A  /  x ]. ph
df-sbc 3154 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 3243 class  [_ A  /  x ]_ B
df-csb 3244 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 3309 class  ( A  \  B )
cun 3310 class  ( A  u.  B )
cin 3311 class  ( A  i^i  B )
wss 3312 wff 
A  C_  B
wpss 3313 wff 
A  C.  B
df-dif 3315 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 3317 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 3319 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 3326 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
df-pss 3328 |-  ( A  C.  B  <->  ( A  C_  B  /\  A  =/=  B ) )
c0 3620 class  (/)
df-nul 3621 |-  (/)  =  ( _V  \  _V )
cif 3731 class  if ( ph ,  A ,  B )
df-if 3732 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3791 class  ~P A
df-pw 3793 |-  ~P A  =  {
x  |  x  C_  A }
csn 3806 class  { A }
cpr 3807 class  { A ,  B }
ctp 3808 class  { A ,  B ,  C }
cop 3809 class  <. A ,  B >.
cotp 3810 class  <. A ,  B ,  C >.
df-sn 3812 |-  { A }  =  {
x  |  x  =  A }
df-pr 3813 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3814 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3815 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3816 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 4007 class  U. A
df-uni 4008 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 4042 class  |^| A
df-int 4043 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 4085 class  U_ x  e.  A  B
ciin 4086 class  |^|_
x  e.  A  B
df-iun 4087 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 4088 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 4174 wff Disj  x  e.  A B
df-disj 4175 |-  (Disj  x  e.  A B 
<-> 
A. y E* x  e.  A y  e.  B
)
wbr 4204 wff 
A R B
df-br 4205 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 4257 class  {
<. x ,  y >.  |  ph }
cmpt 4258 class  ( x  e.  A  |->  B )
df-opab 4259 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 4260 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 4294 wff 
Tr  A
df-tr 4295 |-  ( Tr  A  <->  U. A  C_  A )
ax-rep 4312 |-  ( 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 4322 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 4330 |- 
E. x A. y  -.  y  e.  x
ax-pow 4369 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
ax-pr 4395 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4484 class  _E
cid 4485 class  _I
df-eprel 4486 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4490 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4493 wff 
R  Po  A
wor 4494 wff 
R  Or  A
df-po 4495 |-  ( 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 4496 |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) ) )
wfr 4530 wff 
R  Fr  A
wse 4531 wff 
R Se  A
wwe 4532 wff 
R  We  A
df-fr 4533 |-  ( R  Fr  A  <->  A. x ( ( x 
C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
df-se 4534 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-we 4535 |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A )
)
word 4572 wff 
Ord  A
con0 4573 class  On
wlim 4574 wff 
Lim  A
csuc 4575 class  suc 
A
df-ord 4576 |-  ( Ord  A  <->  ( Tr  A  /\  _E  We  A
) )
df-on 4577 |-  On  =  { x  |  Ord  x }
df-lim 4578 |-  ( Lim  A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
df-suc 4579 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4692 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
com 4836 class  om
df-om 4837 |-  om  =  { x  e.  On  |  A. y
( Lim  y  ->  x  e.  y ) }
cxp 4867 class  ( A  X.  B )
ccnv 4868 class  `' A
cdm 4869 class  dom 
A
crn 4870 class  ran 
A
cres 4871 class  ( A  |`  B )
cima 4872 class  ( A " B )
ccom 4873 class  ( A  o.  B )
wrel 4874 wff 
Rel  A
df-xp 4875 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4876 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4877 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4878 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4879 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4880 |-  ran  A  =  dom  `' A
df-res 4881 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4882 |-  ( A " B
)  =  ran  ( A  |`  B )
cio 5407 class  ( iota x ph )
df-iota 5409 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
wfun 5439 wff 
Fun  A
wfn 5440 wff 
A  Fn  B
wf 5441 wff 
F : A --> B
wf1 5442 wff 
F : A -1-1-> B
wfo 5443 wff 
F : A -onto-> B
wf1o 5444 wff 
F : A -1-1-onto-> B
cfv 5445 class  ( F `  A )
wiso 5446 wff 
H  Isom  R ,  S  ( A ,  B )
df-fun 5447 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 5448 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 5449 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 5450 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 5451 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 5452 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 5453 |-  ( F `  A )  =  ( iota x A F x )
df-isom 5454 |-  ( 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 6072 class  ( A F B )
coprab 6073 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpt2 6074 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 6075 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 6076 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpt2 6077 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 6294 class  o F R
cofr 6295 class  o R R
df-of 6296 |-  o F R  =  ( f  e.  _V , 
g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 6297 |-  o R R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 6338 class  1st
c2nd 6339 class  2nd
df-1st 6340 |- 
1st  =  ( x  e.  _V  |->  U. dom  { x } )
df-2nd 6341 |- 
2nd  =  ( x  e.  _V  |->  U. ran  { x } )
ctpos 6469 class tpos  F
df-tpos 6470 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
ccur 6508 class curry  A
cunc 6509 class uncurry  A
df-cur 6510 |- curry  F  =  ( x  e.  dom  dom  F  |->  {
<. y ,  z >.  |  <. x ,  y
>. F z } )
df-unc 6511 |- uncurry  F  =  { <. <. x ,  y >. ,  z
>.  |  y ( F `  x )
z }
crpss 6512 class [ C.]
df-rpss 6513 |- [
C.]  =  { <. x ,  y >.  |  x 
C.  y }
cund 6532 class  Undef
crio 6533 class  (
iota_ x  e.  A ph )
df-undef 6534 |- 
Undef  =  ( s  e.  _V  |->  ~P U. s )
df-riota 6540 |-  ( iota_ x  e.  A ph )  =  if ( E! x  e.  A  ph ,  ( iota x
( x  e.  A  /\  ph ) ) ,  ( Undef `  { x  |  x  e.  A } ) )
wsmo 6598 wff 
Smo  A
df-smo 6599 |-  ( 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 6623 class recs ( F )
df-recs 6624 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 6658 class  rec ( F ,  I
)
df-rdg 6659 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  if ( g  =  (/) ,  I ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) ) )
cseqom 6695 class seq𝜔 ( F ,  I )
df-seqom 6696 |- seq𝜔 ( F ,  I )  =  ( rec (
( i  e.  om ,  v  e.  _V  |->  <. suc  i ,  ( i F v )
>. ) ,  <. (/) ,  (  _I  `  I )
>. ) " om )
c1o 6708 class  1o
c2o 6709 class  2o
c3o 6710 class  3o
c4o 6711 class  4o
coa 6712 class  +o
comu 6713 class  .o
coe 6714 class  ^o
df-1o 6715 |-  1o  =  suc  (/)
df-2o 6716 |-  2o  =  suc  1o
df-3o 6717 |-  3o  =  suc  2o
df-4o 6718 |-  4o  =  suc  3o
df-oadd 6719 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6720 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexp 6721 |- 
^o  =  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
wer 6893 wff 
R  Er  A
cec 6894 class  [ A ] R
cqs 6895 class  ( A /. R )
df-er 6896 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6898 |-  [ A ] R  =  ( R " { A } )
df-qs 6902 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cmap 7009 class  ^m
cpm 7010 class  ^pm
df-map 7011 |- 
^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
df-pm 7012 |-  ^pm  =  ( x  e. 
_V ,  y  e. 
_V  |->  { f  e. 
~P ( y  X.  x )  |  Fun  f } )
cixp 7054 class  X_ x  e.  A  B
df-ixp 7055 |-  X_ x  e.  A  B  =  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
cen 7097 class  ~~
cdom 7098 class  ~<_
csdm 7099 class  ~<
cfn 7100 class  Fin
df-en 7101 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 7102 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-sdom 7103 |- 
~<  =  (  ~<_  \  ~~  )
df-fin 7104 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
cfi 7406 class  fi
df-fi 7407 |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
csup 7436 class  sup ( A ,  B ,  R )
df-sup 7437 |- 
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 7467 class OrdIso ( R ,  A )
df-oi 7468 |- 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 7513 class har
cwdom 7514 class  ~<_*
df-har 7515 |- har 
=  ( x  e. 
_V  |->  { y  e.  On  |  y  ~<_  x } )
df-wdom 7516 |-  ~<_*  =  { <. x ,  y
>.  |  ( x  =  (/)  \/  E. z 
z : y -onto-> x ) }
ax-reg 7549 |-  ( E. y  y  e.  x  ->  E. y
( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x )
) )
ax-inf 7582 |- 
E. y ( x  e.  y  /\  A. z ( z  e.  y  ->  E. w
( z  e.  w  /\  w  e.  y
) ) )
ax-inf2 7585 |- 
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 7605 class CNF
df-cnf 7606 |- 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 7664 class  TC
df-tc 7665 |-  TC  =  ( x  e.  _V  |->  |^| { y  |  ( x  C_  y  /\  Tr  y ) } )
cr1 7677 class  R1
crnk 7678 class  rank
df-r1 7679 |-  R1  =  rec (
( x  e.  _V  |->  ~P x ) ,  (/) )
df-rank 7680 |- 
rank  =  ( x  e.  _V  |->  |^| { y  e.  On  |  x  e.  ( R1 `  suc  y ) } )
ccrd 7811 class  card
cale 7812 class  aleph
ccf 7813 class  cf
wacn 7814 class AC  A
df-card 7815 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
df-aleph 7816 |-  aleph  =  rec (har ,  om )
df-cf 7817 |-  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 7818 |- 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 7985 wff CHOICE
df-ac 7986 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x ) )
ccda 8036 class  +c
df-cda 8037 |- 
+c  =  ( x  e.  _V ,  y  e.  _V  |->  ( ( x  X.  { (/) } )  u.  ( y  X.  { 1o }
) ) )
cfin1a 8147 class FinIa
cfin2 8148 class FinII
cfin4 8149 class FinIV
cfin3 8150 class FinIII
cfin5 8151 class FinV
cfin6 8152 class FinVI
cfin7 8153 class FinVII
df-fin1a 8154 |- FinIa  =  { x  |  A. y  e.  ~P  x
( y  e.  Fin  \/  ( x  \  y
)  e.  Fin ) }
df-fin2 8155 |- FinII  =  { x  |  A. y  e.  ~P  ~P x
( ( y  =/=  (/)  /\ [ C.]  Or  y
)  ->  U. y  e.  y ) }
df-fin4 8156 |- FinIV  =  { x  |  -.  E. y ( y  C.  x  /\  y  ~~  x
) }
df-fin3 8157 |- FinIII  =  { x  |  ~P x  e. FinIV }
df-fin5 8158 |- FinV  =  { x  |  ( x  =  (/)  \/  x  ~<  ( x  +c  x
) ) }
df-fin6 8159 |- FinVI  =  { x  |  ( x  ~<  2o  \/  x  ~<  ( x  X.  x ) ) }
df-fin7 8160 |- FinVII  =  { x  |  -.  E. y  e.  ( On 
\  om ) x 
~~  y }
ax-cc 8304 |-  ( x  ~~  om  ->  E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
ax-dc 8315 |-  ( ( 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 8328 |-  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 8332 |- 
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 8484 class GCH
df-gch 8485 |- GCH 
=  ( Fin  u.  { x  |  A. y  -.  ( x  ~<  y  /\  y  ~<  ~P x
) } )
cwina 8546 class  Inacc W
cina 8547 class  Inacc
df-wina 8548 |- 
Inacc W  =  {
x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z
) }
df-ina 8549 |- 
Inacc  =  { x  |  ( x  =/=  (/)  /\  ( cf `  x
)  =  x  /\  A. y  e.  x  ~P y  ~<  x ) }
cwun 8564 class WUni
cwunm 8565 class wUniCl
df-wun 8566 |- 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 8567 |- wUniCl  =  ( x  e. 
_V  |->  |^| { u  e. WUni  |  x  C_  u }
)
ctsk 8612 class  Tarski
df-tsk 8613 |- 
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 8654 class  Univ
df-gru 8655 |- 
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 8687 |- 
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 8701 class  tarskiMap
df-tskm 8702 |-  tarskiMap 
=  ( x  e. 
_V  |->  |^| { y  e. 
Tarski  |  x  e.  y } )
cnpi 8708 class  N.
cpli 8709 class  +N
cmi 8710 class  .N
clti 8711 class  <N
cplpq 8712 class  +pQ
cmpq 8713 class  .pQ
cltpq 8714 class  <pQ
ceq 8715 class  ~Q
cnq 8716 class  Q.
c1q 8717 class  1Q
cerq 8718 class  /Q
cplq 8719 class  +Q
cmq 8720 class  .Q
crq 8721 class  *Q
cltq 8722 class  <Q
cnp 8723 class  P.
c1p 8724 class  1P
cpp 8725 class  +P.
cmp 8726 class  .P.
cltp 8727 class  <P
cplpr 8728 class  +pR
cmpr 8729 class  .pR
cer 8730 class  ~R
cnr 8731 class  R.
c0r 8732 class  0R
c1r 8733 class  1R
cm1r 8734 class  -1R
cplr 8735 class  +R
cmr 8736 class  .R
cltr 8737 class  <R
df-ni 8738 |-  N.  =  ( om  \  { (/) } )
df-pli 8739 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 8740 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 8741 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 8774 |- 
+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 8775 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 8776 |- 
<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 8777 |- 
~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 8778 |-  Q.  =  { x  e.  ( N.  X.  N. )  |  A. y  e.  ( N.  X.  N. ) ( x  ~Q  y  ->  -.  ( 2nd `  y )  <N  ( 2nd `  x ) ) }
df-erq 8779 |- 
/Q  =  (  ~Q  i^i  ( ( N.  X.  N. )  X.  Q. )
)
df-plq 8780 |- 
+Q  =  ( ( /Q  o.  +pQ  )  |`  ( Q.  X.  Q. ) )
df-mq 8781 |-  .Q  =  ( ( /Q  o.  .pQ  )  |`  ( Q.  X.  Q. ) )
df-1nq 8782 |-  1Q  =  <. 1o ,  1o >.
df-rq 8783 |-  *Q  =  ( `'  .Q  " { 1Q } )
df-ltnq 8784 |- 
<Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
df-np 8847 |-  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 8848 |-  1P  =  { x  |  x  <Q  1Q }
df-plp 8849 |- 
+P.  =  ( x  e.  P. ,  y  e.  P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  +Q  u ) } )
df-mp 8850 |-  .P.  =  ( x  e. 
P. ,  y  e. 
P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  .Q  u ) } )
df-ltp 8851 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  x  C.  y ) }
df-plpr 8921 |- 
+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 8922 |- 
.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 8923 |- 
~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 8924 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 8925 |- 
+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 8926 |-  .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 8927 |- 
<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 8928 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 8929 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 8930 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 8977 class  CC
cr 8978 class  RR
cc0 8979 class  0
c1 8980 class  1
ci 8981 class  _i
caddc 8982 class  +
cltrr 8983 class  <RR
cmul 8984 class  x.
df-c 8985 |-  CC  =  ( R.  X.  R. )
df-0 8986 |-  0  =  <. 0R ,  0R >.
df-1 8987 |-  1  =  <. 1R ,  0R >.
df-i 8988 |-  _i  =  <. 0R ,  1R >.
df-r 8989 |-  RR  =  ( R.  X.  { 0R } )
df-add 8990 |-  +  =  { <. <.
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 8991 |-  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 8992 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 9035 |-  CC  e.  _V
ax-resscn 9036 |-  RR  C_  CC
ax-1cn 9037 |-  1  e.  CC
ax-icn 9038 |-  _i  e.  CC
ax-addcl 9039 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 9040 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 9041 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 9042 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-mulcom 9043 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 9044 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 9045 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 9046 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 9047 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-1ne0 9048 |-  1  =/=  0
ax-1rid 9049 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-rnegex 9050 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-rrecex 9051 |-  ( ( A  e.  RR  /\  A  =/=  0 )  ->  E. x  e.  RR  ( A  x.  x )  =  1 )
ax-cnre 9052 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-lttri 9053 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <RR  B  <->  -.  ( A  =  B  \/  B  <RR  A ) ) )
ax-pre-lttrn 9054 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-ltadd 9055 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 9056 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-sup 9057 |-  ( ( 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 9058 |-  +  : ( CC 
X.  CC ) --> CC
ax-mulf 9059 |-  x.  : ( CC 
X.  CC ) --> CC
cpnf 9106 class  +oo
cmnf 9107 class  -oo
cxr 9108 class  RR*
clt 9109 class  <
cle 9110 class  <_
df-pnf 9111 |- 
+oo  =  ~P U. CC
df-mnf 9112 |- 
-oo  =  ~P  +oo
df-xr 9113 |-  RR*  =  ( RR  u.  { 
+oo ,  -oo } )
df-ltxr 9114 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { 
-oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) ) )
df-le 9115 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 9280 class  -
cneg 9281 class  -u A
df-sub 9282 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC ( y  +  z )  =  x ) )
df-neg 9283 |-  -u A  =  (
0  -  A )
cdiv 9666 class  /
df-div 9667 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC ( y  x.  z
)  =  x ) )
cn 9989 class  NN
df-nn 9990 |-  NN  =  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )
c2 10038 class  2
c3 10039 class  3
c4 10040 class  4
c5 10041 class  5
c6 10042 class  6
c7 10043 class  7
c8 10044 class  8
c9 10045 class  9
c10 10046 class  10
df-2 10047 |-  2  =  ( 1  +  1 )
df-3 10048 |-  3  =  ( 2  +  1 )
df-4 10049 |-  4  =  ( 3  +  1 )
df-5 10050 |-  5  =  ( 4  +  1 )
df-6 10051 |-  6  =  ( 5  +  1 )
df-7 10052 |-  7  =  ( 6  +  1 )
df-8 10053 |-  8  =  ( 7  +  1 )
df-9 10054 |-  9  =  ( 8  +  1 )
df-10 10055 |-  10  =  ( 9  +  1 )
cn0 10210 class  NN0
df-n0 10211 |-  NN0  =  ( NN  u.  { 0 } )
cz 10271 class  ZZ
df-z 10272 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 10371 class ; A B
df-dec 10372 |- ; A B  =  ( ( 10  x.  A )  +  B )
cuz 10477 class  ZZ>=
df-uz 10478 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 10563 class  QQ
df-q 10564 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 10601 class  RR+
df-rp 10602 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 10696 class  - e A
cxad 10697 class  + e
cxmu 10698 class  x e
df-xneg 10699 |-  - e A  =  if ( A  =  +oo , 
-oo ,  if ( A  =  -oo ,  +oo , 
-u A ) )
df-xadd 10700 |-  + 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 10701 |-  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 10905 class  (,)
cioc 10906 class  (,]
cico 10907 class  [,)
cicc 10908 class  [,]
df-ioo 10909 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 10910 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 10911 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 10912 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 11032 class  ...
df-fz 11033 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 11123 class ..^
df-fzo 11124 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 11189 class  |_
df-fl 11190 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
cmo 11238 class  mod
df-mod 11239 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 11311 class  seq 
M (  .+  ,  F )
df-seq 11312 |- 
seq  M (  .+  ,  F )  =  ( rec ( ( x  e.  _V ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. ) " om )
cexp 11370 class  ^
df-exp 11371 |- 
^  =  ( 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 11554 class  !
df-fac 11555 |-  !  =  ( {
<. 0 ,  1
>. }  u.  seq  1
(  x.  ,  _I  ) )
cbc 11581 class  _C
df-bc 11582 |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n
)  /  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) ) ) ,  0 ) )
chash 11606 class  #
df-hash 11607 |-  #  =  ( (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om )  o.  card )  u.  ( ( _V  \  Fin )  X. 
{  +oo } ) )
cword 11705 class Word  S
cconcat 11706 class concat
cs1 11707 class  <" A ">
csubstr 11708 class substr
csplice 11709 class splice
creverse 11710 class reverse
df-word 11711 |- Word  S  =  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
df-concat 11712 |- concat  =  ( s  e. 
_V ,  t  e. 
_V  |->  ( x  e.  ( 0..^ ( (
# `  s )  +  ( # `  t
) ) )  |->  if ( x  e.  ( 0..^ ( # `  s
) ) ,  ( s `  x ) ,  ( t `  ( x  -  ( # `
 s ) ) ) ) ) )
df-s1 11713 |-  <" A ">  =  { <. 0 ,  (  _I  `  A )
>. }
df-substr 11714 |- 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 11715 |- 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 11716 |- reverse  =  ( s  e. 
_V  |->  ( x  e.  ( 0..^ ( # `  s ) )  |->  ( s `  ( ( ( # `  s
)  -  1 )  -  x ) ) ) )
cs2 11793 class  <" A B ">
cs3 11794 class  <" A B C ">
cs4 11795 class  <" A B C D ">
cs5 11796 class  <" A B C D E ">
cs6 11797 class  <" A B C D E F ">
cs7 11798 class  <" A B C D E F G ">
cs8 11799 class  <" A B C D E F G H ">
df-s2 11800 |-  <" A B ">  =  ( <" A "> concat  <" B "> )
df-s3 11801 |-  <" A B C ">  =  (
<" A B "> concat 
<" C "> )
df-s4 11802 |-  <" A B C D ">  =  ( <" A B C "> concat  <" D "> )
df-s5 11803 |-  <" A B C D E ">  =  ( <" A B C D "> concat  <" E "> )
df-s6 11804 |-  <" A B C D E F ">  =  ( <" A B C D E "> concat 
<" F "> )
df-s7 11805 |-  <" A B C D E F G ">  =  (
<" A B C D E F "> concat 
<" G "> )
df-s8 11806 |-  <" A B C D E F G H ">  =  ( <" A B C D E F G "> concat  <" H "> )
cshi 11869 class  shift
df-shft 11870 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 11889 class  *
cre 11890 class  Re
cim 11891 class  Im
df-cj 11892 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 11893 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 11894 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqr 12026 class  sqr
cabs 12027 class  abs
df-sqr 12028 |- 
sqr  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
df-abs 12029 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
clsp 12252 class  limsup
df-limsup 12253 |- 
limsup  =  ( x  e. 
_V  |->  sup ( ran  (
k  e.  RR  |->  sup ( ( ( x
" ( k [,) 
+oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  ) )
cli 12266 class  ~~>
crli 12267 class  ~~> r
co1 12268 class  O ( 1 )
clo1 12269 class  <_
O ( 1 )
df-clim 12270 |-  ~~>  =  { <. 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 12271 |-  ~~> 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 12272 |-  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 12273 |- 
<_ 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 12467 class  sum_ k  e.  A  B
df-sum 12468 |- 
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 12652 class  exp
ceu 12653 class  _e
csin 12654 class  sin
ccos 12655 class  cos
ctan 12656 class  tan
cpi 12657 class  pi
df-ef 12658 |-  exp  =  ( x  e.  CC  |->  sum_ k  e.  NN0  ( ( x ^
k )  /  ( ! `  k )
) )
df-e 12659 |-  _e  =  ( exp `  1 )
df-sin 12660 |- 
sin  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  -  ( exp `  ( -u _i  x.  x ) ) )  /  ( 2  x.  _i ) ) )
df-cos 12661 |- 
cos  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  +  ( exp `  ( -u _i  x.  x ) ) )  /  2 ) )
df-tan 12662 |- 
tan  =  ( x  e.  ( `' cos " ( CC  \  {
0 } ) ) 
|->  ( ( sin `  x
)  /  ( cos `  x ) ) )
df-pi 12663 |-  pi  =  sup (
( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  `'  <  )
cdivides 12840 class  ||
df-dvds 12841 |- 
||  =  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
cbits 12919 class bits
csad 12920 class sadd
csmu 12921 class smul
df-bits 12922 |- bits 
=  ( n  e.  ZZ  |->  { m  e. 
NN0  |  -.  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) ) } )
df-sad 12951 |- 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 12976 |- 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 12994 class  gcd
df-gcd 12995 |- 
gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
cprime 13067 class  Prime
df-prm 13068 |- 
Prime  =  { p  e.  NN  |  { n  e.  NN  |  n  ||  p }  ~~  2o }
cnumer 13113 class numer
cdenom 13114 class denom
df-numer 13115 |- numer  =  ( y  e.  QQ  |->  ( 1st `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
df-denom 13116 |- denom  =  ( y  e.  QQ  |->  ( 2nd `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
codz 13140 class  od
Z
cphi 13141 class  phi
df-odz 13142 |-  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 13143 |- 
phi  =  ( n  e.  NN  |->  ( # `  { x  e.  ( 1 ... n )  |  ( x  gcd  n )  =  1 } ) )
cpc 13198 class  pCnt
df-pc 13199 |-  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 13285 class  ZZ [ _i ]
df-gz 13286 |-  ZZ [ _i ]  =  { x  e.  CC  |  ( ( Re
`  x )  e.  ZZ  /\  ( Im
`  x )  e.  ZZ ) }
cvdwa 13321 class AP
cvdwm 13322 class MonoAP
cvdwp 13323 class PolyAP
df-vdwap 13324 |- AP 
=  ( k  e. 
NN0  |->  ( a  e.  NN ,  d  e.  NN  |->  ran  ( m  e.  ( 0 ... (
k  -  1 ) )  |->  ( a  +  ( m  x.  d
) ) ) ) )
df-vdwmc 13325 |- MonoAP  =  { <. k ,  f
>.  |  E. c
( ran  (AP `  k
)  i^i  ~P ( `' f " {
c } ) )  =/=  (/) }
df-vdwpc 13326 |- 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 13355 class Ramsey
df-ram 13357 |- 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 13453 class Struct
cnx 13454 class  ndx
csts 13455 class sSet
cslot 13456 class Slot  A
cbs 13457 class  Base
cress 13458 classs
df-struct 13459 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( f 
\  { (/) } )  /\  dom  f  C_  ( ... `  x ) ) }
df-ndx 13460 |- 
ndx  =  (  _I  |`  NN )
df-slot 13461 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
df-base 13462 |- 
Base  = Slot  1
df-sets 13463 |- sSet 
=  ( s  e. 
_V ,  e  e. 
_V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u.  { e } ) )
df-ress 13464 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  if ( ( Base `  w
)  C_  x ,  w ,  ( w sSet  <.
( Base `  ndx ) ,  ( x  i^i  ( Base `  w ) )
>. ) ) )
cplusg 13517 class  +g
cmulr 13518 class  .r
cstv 13519 class  * r
csca 13520 class Scalar
cvsca 13521 class  .s
cip 13522 class  .i
cts 13523 class TopSet
cple 13524 class  le
coc 13525 class  oc
cds 13526 class  dist
cunif 13527 class  UnifSet
chom 13528 class  Hom
cco 13529 class comp
df-plusg 13530 |- 
+g  = Slot  2
df-mulr 13531 |- 
.r  = Slot  3
df-starv 13532 |-  * r  = Slot  4
df-sca 13533 |- Scalar  = Slot  5
df-vsca 13534 |-  .s  = Slot  6
df-ip 13535 |-  .i  = Slot  8
df-tset 13536 |- TopSet  = Slot  9
df-ple 13537 |- 
le  = Slot  10
df-ocomp 13538 |-  oc  = Slot ; 1 1
df-ds 13539 |-  dist 
= Slot ; 1 2
df-unif 13540 |- 
UnifSet  = Slot ; 1 3
df-hom 13541 |- 
Hom  = Slot ; 1 4
df-cco 13542 |- comp 
= Slot ; 1 5
crest 13636 classt
ctopn 13637 class  TopOpen
df-rest 13638 |-t  =  ( j  e.  _V ,  x  e.  _V  |->  ran  ( y  e.  j 
|->  ( y  i^i  x
) ) )
df-topn 13639 |-  TopOpen  =  ( w  e. 
_V  |->  ( (TopSet `  w )t  ( Base `  w
) ) )
ctg 13653 class  topGen
cpt 13654 class  Xt_
df-topgen 13655 |- 
topGen  =  ( x  e. 
_V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
df-pt 13656 |-  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 13657 class  X_s
cpws 13658 class  ^s
df-prds 13659 |-  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 13661 |- 
^s  =  ( r  e. 
_V ,  i  e. 
_V  |->  ( (Scalar `  r ) X_s ( i  X.  {
r } ) ) )
cordt 13709 class ordTop
cxrs 13710 class  RR* s
c0g 13711 class  0g
cgsu 13712 class  gsumg
df-ordt 13713 |- 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 13714 |- 
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 13715 |-  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 13716 |- 
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 13717 class qTop
cimas 13718 class  "s
cqus 13719 class  /.s
cxps 13720 class  X.s
df-qtop 13721 |- qTop 
=  ( j  e. 
_V ,  f  e. 
_V  |->  { s  e. 
~P ( f " U. j )  |  ( ( `' f "
s )  i^i  U. j )  e.  j } )
df-imas 13722 |-  "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 13723 |- 
/.s 
=  ( r  e. 
_V ,  e  e. 
_V  |->  ( ( x  e.  ( Base `  r
)  |->  [ x ]
e )  "s  r )
)
df-xps 13724 |- 
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 13795 class Moore
cmrc 13796 class mrCls
cmri 13797 class mrInd
cacs 13798 class ACS
df-mre 13799 |- Moore  =  ( x  e. 
_V  |->  { c  e. 
~P ~P x  |  ( x  e.  c  /\  A. s  e. 
~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
df-mrc 13800 |- mrCls  =  ( c  e. 
U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^|
{ s  e.  c  |  x  C_  s } ) )
df-mri 13801 |- mrInd  =  ( c  e. 
U. ran Moore  |->  { s  e.  ~P U. c  | 
A. x  e.  s  -.  x  e.  ( (mrCls `  c ) `  ( s  \  {
x } ) ) } )
df-acs 13802 |- 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 13877 class  Cat
ccid 13878 class  Id
chomf 13879 class  Homf
ccomf 13880 class compf
df-cat 13881 |- 
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 13882 |-  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 13883 |- 
Homf 
=  ( c  e. 
_V  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( x (  Hom  `  c )
y ) ) )
df-comf 13884 |- 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 13925 class oppCat
df-oppc 13926 |- 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 13942 class Mono
cepi 13943 class Epi
df-mon 13944 |- 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 13945 |- Epi 
=  ( c  e. 
Cat  |-> tpos  (Mono `  (oppCat `  c
) ) )
csect 13958 class Sect
cinv 13959 class Inv
ciso 13960 class  Iso
df-sect 13961 |- 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 13962 |- Inv 
=  ( c  e. 
Cat  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( ( x (Sect `  c )
y )  i^i  `' ( y (Sect `  c ) x ) ) ) )
df-iso 13963 |- 
Iso  =  ( c  e.  Cat  |->  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) ) )
cssc 13995 class  C_cat
cresc 13996 class  |`cat
csubc 13997 class Subcat
df-ssc 13998 |-  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 13999 |-  |`cat 
=  ( c  e. 
_V ,  h  e. 
_V  |->  ( ( cs  dom 
dom  h ) sSet  <. (  Hom  `  ndx ) ,  h >. ) )
df-subc 14000 |- 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 14039 class  Func
cidfu 14040 class idfunc
ccofu 14041 class  o.func
cresf 14042 class  |`f
df-func 14043 |- 
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 14044 |- idfunc  =  ( t  e.  Cat  |->  [_ ( Base `  t
)  /  b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
df-cofu 14045 |-  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 14046 |-  |`f  =  ( f  e. 
_V ,  h  e. 
_V  |->  <. ( ( 1st `  f )  |`  dom  dom  h ) ,  ( x  e.  dom  h  |->  ( ( ( 2nd `  f ) `  x
)  |`  ( h `  x ) ) )
>. )
cful 14087 class Full
cfth 14088 class Faith
df-full 14089 |- 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 14090 |- 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 14126 class Nat
cfuc 14127 class FuncCat
df-nat 14128 |- 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 14129 |- 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 14163 class domA
ccoda 14164 class coda
carw 14165 class Nat
choma 14166 class Homa
df-doma 14167 |- domA  =  ( 1st  o.  1st )
df-coda 14168 |- coda  =  ( 2nd  o.  1st )
df-homa 14169 |- Homa  =  ( c  e.  Cat  |->  ( x  e.  (
( Base `  c )  X.  ( Base `  c
) )  |->  ( { x }  X.  (
(  Hom  `  c ) `
 x ) ) ) )
df-arw 14170 |- Nat 
=  ( c  e. 
Cat  |->  U. ran  (Homa `  c
) )
cida 14196 class Ida
ccoa 14197 class compa
df-ida 14198 |- Ida  =  ( c  e.  Cat  |->  ( x  e.  ( Base `  c )  |->  <.
x ,  x ,  ( ( Id `  c ) `  x
) >. ) )
df-coa 14199 |- 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 14218 class  SetCat
df-setc 14219 |- 
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 14237 class CatCat
df-catc 14238 |- 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 14253 class  X.c
c1stf 14254 class  1stF
c2ndf 14255 class  2ndF
cprf 14256 class ⟨,⟩F
df-xpc 14257 |- 
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 14258 |- 
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 14259 |- 
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 14260 |- ⟨,⟩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 14294 class evalF
ccurf 14295 class curryF
cuncf 14296 class uncurryF
cdiag 14297 class Δfunc
df-evlf 14298 |- 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 14299 |- 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 14300 |- 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 14301 |- Δfunc  =  ( c  e.  Cat ,  d  e.  Cat  |->  (
<. c ,  d >. curryF  ( c  1stF  d ) ) )
chof 14333 class HomF
cyon 14334 class Yon
df-hof 14335 |- 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 14336 |- Yon 
=  ( c  e. 
Cat  |->  ( <. c ,  (oppCat `  c ) >. curryF  (HomF `  (oppCat `  c ) ) ) )
cpreset 14371 class  Preset
cdrs 14372 class Dirset
df-preset 14373 |- 
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 14374 |- Dirset  =  { f  e.  Preset  | 
[. ( Base `  f
)  /  b ]. [. ( le `  f
)  /  r ]. ( b  =/=  (/)  /\  A. x  e.  b  A. y  e.