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 2212 |-  ( A. x ph  ->  ph )
ax-5o 2213 |-  ( A. x ( A. x ph  ->  ps )  ->  ( A. x ph  ->  A. x ps )
)
ax-6o 2214 |-  ( -.  A. x  -.  A. x ph  ->  ph )
ax-9o 2215 |-  ( A. x ( x  =  y  ->  A. x ph )  ->  ph )
ax-10o 2216 |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph ) )
ax-10 2217 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11o 2218 |-  ( -.  A. x  x  =  y  ->  ( x  =  y  -> 
( ph  ->  A. x
( x  =  y  ->  ph ) ) ) )
ax-12o 2219 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  =  y  ->  A. z  x  =  y ) ) )
ax-15 2220 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  e.  y  ->  A. z  x  e.  y ) ) )
ax-16 2221 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
weu 2281 wff 
E! x ph
wmo 2282 wff 
E* x ph
df-eu 2285 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
df-mo 2286 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
ax-7d 2372 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-8d 2373 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-9d1 2374 |- 
-.  A. x  -.  x  =  x
ax-9d2 2375 |- 
-.  A. x  -.  x  =  y
ax-10d 2376 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11d 2377 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-ext 2417 |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
cab 2422 class  { x  |  ph }
df-clab 2423 |-  ( x  e.  {
y  |  ph }  <->  [ x  /  y ]
ph )
df-cleq 2429 |-  ( A. x ( x  e.  y  <->  x  e.  z )  ->  y  =  z )   =>    |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
df-clel 2432 |-  ( A  e.  B  <->  E. x ( x  =  A  /\  x  e.  B ) )
wnfc 2559 wff  F/_ x A
df-nfc 2561 |-  ( F/_ x A  <->  A. y F/ x  y  e.  A )
wne 2599 wff 
A  =/=  B
wnel 2600 wff 
A  e/  B
df-ne 2601 |-  ( A  =/=  B  <->  -.  A  =  B )
df-nel 2602 |-  ( A  e/  B  <->  -.  A  e.  B )
wral 2705 wff  A. x  e.  A  ph
wrex 2706 wff 
E. x  e.  A  ph
wreu 2707 wff 
E! x  e.  A  ph
wrmo 2708 wff 
E* x  e.  A ph
crab 2709 class  { x  e.  A  |  ph }
df-ral 2710 |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
df-rex 2711 |-  ( E. x  e.  A  ph  <->  E. x
( x  e.  A  /\  ph ) )
df-reu 2712 |-  ( E! x  e.  A  ph  <->  E! x
( x  e.  A  /\  ph ) )
df-rmo 2713 |-  ( E* x  e.  A ph  <->  E* x
( x  e.  A  /\  ph ) )
df-rab 2714 |- 
{ x  e.  A  |  ph }  =  {
x  |  ( x  e.  A  /\  ph ) }
cvv 2956 class  _V
df-v 2958 |-  _V  =  { x  |  x  =  x }
wcdeq 3144 wff CondEq ( x  =  y  ->  ph )
df-cdeq 3145 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 3161 wff  [. A  /  x ]. ph
df-sbc 3162 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 3251 class  [_ A  /  x ]_ B
df-csb 3252 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 3317 class  ( A  \  B )
cun 3318 class  ( A  u.  B )
cin 3319 class  ( A  i^i  B )
wss 3320 wff 
A  C_  B
wpss 3321 wff 
A  C.  B
df-dif 3323 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 3325 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 3327 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 3334 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
df-pss 3336 |-  ( A  C.  B  <->  ( A  C_  B  /\  A  =/=  B ) )
c0 3628 class  (/)
df-nul 3629 |-  (/)  =  ( _V  \  _V )
cif 3739 class  if ( ph ,  A ,  B )
df-if 3740 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3799 class  ~P A
df-pw 3801 |-  ~P A  =  {
x  |  x  C_  A }
csn 3814 class  { A }
cpr 3815 class  { A ,  B }
ctp 3816 class  { A ,  B ,  C }
cop 3817 class  <. A ,  B >.
cotp 3818 class  <. A ,  B ,  C >.
df-sn 3820 |-  { A }  =  {
x  |  x  =  A }
df-pr 3821 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3822 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3823 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3824 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 4015 class  U. A
df-uni 4016 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 4050 class  |^| A
df-int 4051 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 4093 class  U_ x  e.  A  B
ciin 4094 class  |^|_
x  e.  A  B
df-iun 4095 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 4096 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 4182 wff Disj  x  e.  A B
df-disj 4183 |-  (Disj  x  e.  A B 
<-> 
A. y E* x  e.  A y  e.  B
)
wbr 4212 wff 
A R B
df-br 4213 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 4265 class  {
<. x ,  y >.  |  ph }
cmpt 4266 class  ( x  e.  A  |->  B )
df-opab 4267 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 4268 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 4302 wff 
Tr  A
df-tr 4303 |-  ( Tr  A  <->  U. A  C_  A )
ax-rep 4320 |-  ( 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 4330 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 4338 |- 
E. x A. y  -.  y  e.  x
ax-pow 4377 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
ax-pr 4403 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4492 class  _E
cid 4493 class  _I
df-eprel 4494 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4498 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4501 wff 
R  Po  A
wor 4502 wff 
R  Or  A
df-po 4503 |-  ( 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 4504 |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) ) )
wfr 4538 wff 
R  Fr  A
wse 4539 wff 
R Se  A
wwe 4540 wff 
R  We  A
df-fr 4541 |-  ( R  Fr  A  <->  A. x ( ( x 
C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
df-se 4542 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-we 4543 |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A )
)
word 4580 wff 
Ord  A
con0 4581 class  On
wlim 4582 wff 
Lim  A
csuc 4583 class  suc 
A
df-ord 4584 |-  ( Ord  A  <->  ( Tr  A  /\  _E  We  A
) )
df-on 4585 |-  On  =  { x  |  Ord  x }
df-lim 4586 |-  ( Lim  A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
df-suc 4587 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4701 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
com 4845 class  om
df-om 4846 |-  om  =  { x  e.  On  |  A. y
( Lim  y  ->  x  e.  y ) }
cxp 4876 class  ( A  X.  B )
ccnv 4877 class  `' A
cdm 4878 class  dom 
A
crn 4879 class  ran 
A
cres 4880 class  ( A  |`  B )
cima 4881 class  ( A " B )
ccom 4882 class  ( A  o.  B )
wrel 4883 wff 
Rel  A
df-xp 4884 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4885 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4886 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4887 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4888 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4889 |-  ran  A  =  dom  `' A
df-res 4890 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4891 |-  ( A " B
)  =  ran  ( A  |`  B )
cio 5416 class  ( iota x ph )
df-iota 5418 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
wfun 5448 wff 
Fun  A
wfn 5449 wff 
A  Fn  B
wf 5450 wff 
F : A --> B
wf1 5451 wff 
F : A -1-1-> B
wfo 5452 wff 
F : A -onto-> B
wf1o 5453 wff 
F : A -1-1-onto-> B
cfv 5454 class  ( F `  A )
wiso 5455 wff 
H  Isom  R ,  S  ( A ,  B )
df-fun 5456 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 5457 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 5458 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 5459 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 5460 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 5461 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 5462 |-  ( F `  A )  =  ( iota x A F x )
df-isom 5463 |-  ( 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 6081 class  ( A F B )
coprab 6082 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpt2 6083 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 6084 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 6085 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpt2 6086 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 6303 class  o F R
cofr 6304 class  o R R
df-of 6305 |-  o F R  =  ( f  e.  _V , 
g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 6306 |-  o R R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 6347 class  1st
c2nd 6348 class  2nd
df-1st 6349 |- 
1st  =  ( x  e.  _V  |->  U. dom  { x } )
df-2nd 6350 |- 
2nd  =  ( x  e.  _V  |->  U. ran  { x } )
ctpos 6478 class tpos  F
df-tpos 6479 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
ccur 6517 class curry  A
cunc 6518 class uncurry  A
df-cur 6519 |- curry  F  =  ( x  e.  dom  dom  F  |->  {
<. y ,  z >.  |  <. x ,  y
>. F z } )
df-unc 6520 |- uncurry  F  =  { <. <. x ,  y >. ,  z
>.  |  y ( F `  x )
z }
crpss 6521 class [ C.]
df-rpss 6522 |- [
C.]  =  { <. x ,  y >.  |  x 
C.  y }
cund 6541 class  Undef
crio 6542 class  (
iota_ x  e.  A ph )
df-undef 6543 |- 
Undef  =  ( s  e.  _V  |->  ~P U. s )
df-riota 6549 |-  ( iota_ x  e.  A ph )  =  if ( E! x  e.  A  ph ,  ( iota x
( x  e.  A  /\  ph ) ) ,  ( Undef `  { x  |  x  e.  A } ) )
wsmo 6607 wff 
Smo  A
df-smo 6608 |-  ( 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 6632 class recs ( F )
df-recs 6633 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 6667 class  rec ( F ,  I
)
df-rdg 6668 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  if ( g  =  (/) ,  I ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) ) )
cseqom 6704 class seq𝜔 ( F ,  I )
df-seqom 6705 |- seq𝜔 ( F ,  I )  =  ( rec (
( i  e.  om ,  v  e.  _V  |->  <. suc  i ,  ( i F v )
>. ) ,  <. (/) ,  (  _I  `  I )
>. ) " om )
c1o 6717 class  1o
c2o 6718 class  2o
c3o 6719 class  3o
c4o 6720 class  4o
coa 6721 class  +o
comu 6722 class  .o
coe 6723 class  ^o
df-1o 6724 |-  1o  =  suc  (/)
df-2o 6725 |-  2o  =  suc  1o
df-3o 6726 |-  3o  =  suc  2o
df-4o 6727 |-  4o  =  suc  3o
df-oadd 6728 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6729 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexp 6730 |- 
^o  =  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
wer 6902 wff 
R  Er  A
cec 6903 class  [ A ] R
cqs 6904 class  ( A /. R )
df-er 6905 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6907 |-  [ A ] R  =  ( R " { A } )
df-qs 6911 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cmap 7018 class  ^m
cpm 7019 class  ^pm
df-map 7020 |- 
^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
df-pm 7021 |-  ^pm  =  ( x  e. 
_V ,  y  e. 
_V  |->  { f  e. 
~P ( y  X.  x )  |  Fun  f } )
cixp 7063 class  X_ x  e.  A  B
df-ixp 7064 |-  X_ x  e.  A  B  =  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
cen 7106 class  ~~
cdom 7107 class  ~<_
csdm 7108 class  ~<
cfn 7109 class  Fin
df-en 7110 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 7111 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-sdom 7112 |- 
~<  =  (  ~<_  \  ~~  )
df-fin 7113 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
cfi 7415 class  fi
df-fi 7416 |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
csup 7445 class  sup ( A ,  B ,  R )
df-sup 7446 |- 
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 7478 class OrdIso ( R ,  A )
df-oi 7479 |- 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 7524 class har
cwdom 7525 class  ~<_*
df-har 7526 |- har 
=  ( x  e. 
_V  |->  { y  e.  On  |  y  ~<_  x } )
df-wdom 7527 |-  ~<_*  =  { <. x ,  y
>.  |  ( x  =  (/)  \/  E. z 
z : y -onto-> x ) }
ax-reg 7560 |-  ( E. y  y  e.  x  ->  E. y
( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x )
) )
ax-inf 7593 |- 
E. y ( x  e.  y  /\  A. z ( z  e.  y  ->  E. w
( z  e.  w  /\  w  e.  y
) ) )
ax-inf2 7596 |- 
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 7616 class CNF
df-cnf 7617 |- 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 7675 class  TC
df-tc 7676 |-  TC  =  ( x  e.  _V  |->  |^| { y  |  ( x  C_  y  /\  Tr  y ) } )
cr1 7688 class  R1
crnk 7689 class  rank
df-r1 7690 |-  R1  =  rec (
( x  e.  _V  |->  ~P x ) ,  (/) )
df-rank 7691 |- 
rank  =  ( x  e.  _V  |->  |^| { y  e.  On  |  x  e.  ( R1 `  suc  y ) } )
ccrd 7822 class  card
cale 7823 class  aleph
ccf 7824 class  cf
wacn 7825 class AC  A
df-card 7826 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
df-aleph 7827 |-  aleph  =  rec (har ,  om )
df-cf 7828 |-  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 7829 |- 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 7996 wff CHOICE
df-ac 7997 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x ) )
ccda 8047 class  +c
df-cda 8048 |- 
+c  =  ( x  e.  _V ,  y  e.  _V  |->  ( ( x  X.  { (/) } )  u.  ( y  X.  { 1o }
) ) )
cfin1a 8158 class FinIa
cfin2 8159 class FinII
cfin4 8160 class FinIV
cfin3 8161 class FinIII
cfin5 8162 class FinV
cfin6 8163 class FinVI
cfin7 8164 class FinVII
df-fin1a 8165 |- FinIa  =  { x  |  A. y  e.  ~P  x
( y  e.  Fin  \/  ( x  \  y
)  e.  Fin ) }
df-fin2 8166 |- FinII  =  { x  |  A. y  e.  ~P  ~P x
( ( y  =/=  (/)  /\ [ C.]  Or  y
)  ->  U. y  e.  y ) }
df-fin4 8167 |- FinIV  =  { x  |  -.  E. y ( y  C.  x  /\  y  ~~  x
) }
df-fin3 8168 |- FinIII  =  { x  |  ~P x  e. FinIV }
df-fin5 8169 |- FinV  =  { x  |  ( x  =  (/)  \/  x  ~<  ( x  +c  x
) ) }
df-fin6 8170 |- FinVI  =  { x  |  ( x  ~<  2o  \/  x  ~<  ( x  X.  x ) ) }
df-fin7 8171 |- FinVII  =  { x  |  -.  E. y  e.  ( On 
\  om ) x 
~~  y }
ax-cc 8315 |-  ( x  ~~  om  ->  E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
ax-dc 8326 |-  ( ( 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 8339 |-  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 8343 |- 
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 8495 class GCH
df-gch 8496 |- GCH 
=  ( Fin  u.  { x  |  A. y  -.  ( x  ~<  y  /\  y  ~<  ~P x
) } )
cwina 8557 class  Inacc W
cina 8558 class  Inacc
df-wina 8559 |- 
Inacc W  =  {
x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z
) }
df-ina 8560 |- 
Inacc  =  { x  |  ( x  =/=  (/)  /\  ( cf `  x
)  =  x  /\  A. y  e.  x  ~P y  ~<  x ) }
cwun 8575 class WUni
cwunm 8576 class wUniCl
df-wun 8577 |- 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 8578 |- wUniCl  =  ( x  e. 
_V  |->  |^| { u  e. WUni  |  x  C_  u }
)
ctsk 8623 class  Tarski
df-tsk 8624 |- 
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 8665 class  Univ
df-gru 8666 |- 
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 8698 |- 
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 8712 class  tarskiMap
df-tskm 8713 |-  tarskiMap 
=  ( x  e. 
_V  |->  |^| { y  e. 
Tarski  |  x  e.  y } )
cnpi 8719 class  N.
cpli 8720 class  +N
cmi 8721 class  .N
clti 8722 class  <N
cplpq 8723 class  +pQ
cmpq 8724 class  .pQ
cltpq 8725 class  <pQ
ceq 8726 class  ~Q
cnq 8727 class  Q.
c1q 8728 class  1Q
cerq 8729 class  /Q
cplq 8730 class  +Q
cmq 8731 class  .Q
crq 8732 class  *Q
cltq 8733 class  <Q
cnp 8734 class  P.
c1p 8735 class  1P
cpp 8736 class  +P.
cmp 8737 class  .P.
cltp 8738 class  <P
cplpr 8739 class  +pR
cmpr 8740 class  .pR
cer 8741 class  ~R
cnr 8742 class  R.
c0r 8743 class  0R
c1r 8744 class  1R
cm1r 8745 class  -1R
cplr 8746 class  +R
cmr 8747 class  .R
cltr 8748 class  <R
df-ni 8749 |-  N.  =  ( om  \  { (/) } )
df-pli 8750 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 8751 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 8752 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 8785 |- 
+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 8786 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 8787 |- 
<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 8788 |- 
~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 8789 |-  Q.  =  { x  e.  ( N.  X.  N. )  |  A. y  e.  ( N.  X.  N. ) ( x  ~Q  y  ->  -.  ( 2nd `  y )  <N  ( 2nd `  x ) ) }
df-erq 8790 |- 
/Q  =  (  ~Q  i^i  ( ( N.  X.  N. )  X.  Q. )
)
df-plq 8791 |- 
+Q  =  ( ( /Q  o.  +pQ  )  |`  ( Q.  X.  Q. ) )
df-mq 8792 |-  .Q  =  ( ( /Q  o.  .pQ  )  |`  ( Q.  X.  Q. ) )
df-1nq 8793 |-  1Q  =  <. 1o ,  1o >.
df-rq 8794 |-  *Q  =  ( `'  .Q  " { 1Q } )
df-ltnq 8795 |- 
<Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
df-np 8858 |-  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 8859 |-  1P  =  { x  |  x  <Q  1Q }
df-plp 8860 |- 
+P.  =  ( x  e.  P. ,  y  e.  P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  +Q  u ) } )
df-mp 8861 |-  .P.  =  ( x  e. 
P. ,  y  e. 
P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  .Q  u ) } )
df-ltp 8862 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  x  C.  y ) }
df-plpr 8932 |- 
+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 8933 |- 
.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 8934 |- 
~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 8935 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 8936 |- 
+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 8937 |-  .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 8938 |- 
<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 8939 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 8940 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 8941 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 8988 class  CC
cr 8989 class  RR
cc0 8990 class  0
c1 8991 class  1
ci 8992 class  _i
caddc 8993 class  +
cltrr 8994 class  <RR
cmul 8995 class  x.
df-c 8996 |-  CC  =  ( R.  X.  R. )
df-0 8997 |-  0  =  <. 0R ,  0R >.
df-1 8998 |-  1  =  <. 1R ,  0R >.
df-i 8999 |-  _i  =  <. 0R ,  1R >.
df-r 9000 |-  RR  =  ( R.  X.  { 0R } )
df-add 9001 |-  +  =  { <. <.
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 9002 |-  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 9003 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 9046 |-  CC  e.  _V
ax-resscn 9047 |-  RR  C_  CC
ax-1cn 9048 |-  1  e.  CC
ax-icn 9049 |-  _i  e.  CC
ax-addcl 9050 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 9051 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 9052 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 9053 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-mulcom 9054 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 9055 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 9056 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 9057 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 9058 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-1ne0 9059 |-  1  =/=  0
ax-1rid 9060 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-rnegex 9061 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-rrecex 9062 |-  ( ( A  e.  RR  /\  A  =/=  0 )  ->  E. x  e.  RR  ( A  x.  x )  =  1 )
ax-cnre 9063 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-lttri 9064 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <RR  B  <->  -.  ( A  =  B  \/  B  <RR  A ) ) )
ax-pre-lttrn 9065 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-ltadd 9066 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 9067 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-sup 9068 |-  ( ( 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 9069 |-  +  : ( CC 
X.  CC ) --> CC
ax-mulf 9070 |-  x.  : ( CC 
X.  CC ) --> CC
cpnf 9117 class  +oo
cmnf 9118 class  -oo
cxr 9119 class  RR*
clt 9120 class  <
cle 9121 class  <_
df-pnf 9122 |- 
+oo  =  ~P U. CC
df-mnf 9123 |- 
-oo  =  ~P  +oo
df-xr 9124 |-  RR*  =  ( RR  u.  { 
+oo ,  -oo } )
df-ltxr 9125 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { 
-oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) ) )
df-le 9126 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 9291 class  -
cneg 9292 class  -u A
df-sub 9293 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC ( y  +  z )  =  x ) )
df-neg 9294 |-  -u A  =  (
0  -  A )
cdiv 9677 class  /
df-div 9678 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC ( y  x.  z
)  =  x ) )
cn 10000 class  NN
df-nn 10001 |-  NN  =  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )
c2 10049 class  2
c3 10050 class  3
c4 10051 class  4
c5 10052 class  5
c6 10053 class  6
c7 10054 class  7
c8 10055 class  8
c9 10056 class  9
c10 10057 class  10
df-2 10058 |-  2  =  ( 1  +  1 )
df-3 10059 |-  3  =  ( 2  +  1 )
df-4 10060 |-  4  =  ( 3  +  1 )
df-5 10061 |-  5  =  ( 4  +  1 )
df-6 10062 |-  6  =  ( 5  +  1 )
df-7 10063 |-  7  =  ( 6  +  1 )
df-8 10064 |-  8  =  ( 7  +  1 )
df-9 10065 |-  9  =  ( 8  +  1 )
df-10 10066 |-  10  =  ( 9  +  1 )
cn0 10221 class  NN0
df-n0 10222 |-  NN0  =  ( NN  u.  { 0 } )
cz 10282 class  ZZ
df-z 10283 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 10382 class ; A B
df-dec 10383 |- ; A B  =  ( ( 10  x.  A )  +  B )
cuz 10488 class  ZZ>=
df-uz 10489 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 10574 class  QQ
df-q 10575 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 10612 class  RR+
df-rp 10613 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 10707 class  - e A
cxad 10708 class  + e
cxmu 10709 class  x e
df-xneg 10710 |-  - e A  =  if ( A  =  +oo , 
-oo ,  if ( A  =  -oo ,  +oo , 
-u A ) )
df-xadd 10711 |-  + 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 10712 |-  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 10916 class  (,)
cioc 10917 class  (,]
cico 10918 class  [,)
cicc 10919 class  [,]
df-ioo 10920 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 10921 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 10922 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 10923 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 11043 class  ...
df-fz 11044 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 11135 class ..^
df-fzo 11136 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 11201 class  |_
df-fl 11202 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
cmo 11250 class  mod
df-mod 11251 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 11323 class  seq 
M (  .+  ,  F )
df-seq 11324 |- 
seq  M (  .+  ,  F )  =  ( rec ( ( x  e.  _V ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. ) " om )
cexp 11382 class  ^
df-exp 11383 |- 
^  =  ( 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 11566 class  !
df-fac 11567 |-  !  =  ( {
<. 0 ,  1
>. }  u.  seq  1
(  x.  ,  _I  ) )
cbc 11593 class  _C
df-bc 11594 |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n
)  /  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) ) ) ,  0 ) )
chash 11618 class  #
df-hash 11619 |-  #  =  ( (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om )  o.  card )  u.  ( ( _V  \  Fin )  X. 
{  +oo } ) )
cword 11717 class Word  S
cconcat 11718 class concat
cs1 11719 class  <" A ">
csubstr 11720 class substr
csplice 11721 class splice
creverse 11722 class reverse
df-word 11723 |- Word  S  =  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
df-concat 11724 |- concat  =  ( s  e. 
_V ,  t  e. 
_V  |->  ( x  e.  ( 0..^ ( (
# `  s )  +  ( # `  t
) ) )  |->  if ( x  e.  ( 0..^ ( # `  s
) ) ,  ( s `  x ) ,  ( t `  ( x  -  ( # `
 s ) ) ) ) ) )
df-s1 11725 |-  <" A ">  =  { <. 0 ,  (  _I  `  A )
>. }
df-substr 11726 |- 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 11727 |- 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 11728 |- reverse  =  ( s  e. 
_V  |->  ( x  e.  ( 0..^ ( # `  s ) )  |->  ( s `  ( ( ( # `  s
)  -  1 )  -  x ) ) ) )
cs2 11805 class  <" A B ">
cs3 11806 class  <" A B C ">
cs4 11807 class  <" A B C D ">
cs5 11808 class  <" A B C D E ">
cs6 11809 class  <" A B C D E F ">
cs7 11810 class  <" A B C D E F G ">
cs8 11811 class  <" A B C D E F G H ">
df-s2 11812 |-  <" A B ">  =  ( <" A "> concat  <" B "> )
df-s3 11813 |-  <" A B C ">  =  (
<" A B "> concat 
<" C "> )
df-s4 11814 |-  <" A B C D ">  =  ( <" A B C "> concat  <" D "> )
df-s5 11815 |-  <" A B C D E ">  =  ( <" A B C D "> concat  <" E "> )
df-s6 11816 |-  <" A B C D E F ">  =  ( <" A B C D E "> concat 
<" F "> )
df-s7 11817 |-  <" A B C D E F G ">  =  (
<" A B C D E F "> concat 
<" G "> )
df-s8 11818 |-  <" A B C D E F G H ">  =  ( <" A B C D E F G "> concat  <" H "> )
cshi 11881 class  shift
df-shft 11882 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 11901 class  *
cre 11902 class  Re
cim 11903 class  Im
df-cj 11904 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 11905 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 11906 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqr 12038 class  sqr
cabs 12039 class  abs
df-sqr 12040 |- 
sqr  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
df-abs 12041 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
clsp 12264 class  limsup
df-limsup 12265 |- 
limsup  =  ( x  e. 
_V  |->  sup ( ran  (
k  e.  RR  |->  sup ( ( ( x
" ( k [,) 
+oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  ) )
cli 12278 class  ~~>
crli 12279 class  ~~> r
co1 12280 class  O ( 1 )
clo1 12281 class  <_
O ( 1 )
df-clim 12282 |-  ~~>  =  { <. 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 12283 |-  ~~> 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 12284 |-  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 12285 |- 
<_ 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 12479 class  sum_ k  e.  A  B
df-sum 12480 |- 
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 12664 class  exp
ceu 12665 class  _e
csin 12666 class  sin
ccos 12667 class  cos
ctan 12668 class  tan
cpi 12669 class  pi
df-ef 12670 |-  exp  =  ( x  e.  CC  |->  sum_ k  e.  NN0  ( ( x ^
k )  /  ( ! `  k )
) )
df-e 12671 |-  _e  =  ( exp `  1 )
df-sin 12672 |- 
sin  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  -  ( exp `  ( -u _i  x.  x ) ) )  /  ( 2  x.  _i ) ) )
df-cos 12673 |- 
cos  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  +  ( exp `  ( -u _i  x.  x ) ) )  /  2 ) )
df-tan 12674 |- 
tan  =  ( x  e.  ( `' cos " ( CC  \  {
0 } ) ) 
|->  ( ( sin `  x
)  /  ( cos `  x ) ) )
df-pi 12675 |-  pi  =  sup (
( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  `'  <  )
cdivides 12852 class  ||
df-dvds 12853 |- 
||  =  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
cbits 12931 class bits
csad 12932 class sadd
csmu 12933 class smul
df-bits 12934 |- bits 
=  ( n  e.  ZZ  |->  { m  e. 
NN0  |  -.  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) ) } )
df-sad 12963 |- 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 12988 |- 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 13006 class  gcd
df-gcd 13007 |- 
gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
cprime 13079 class  Prime
df-prm 13080 |- 
Prime  =  { p  e.  NN  |  { n  e.  NN  |  n  ||  p }  ~~  2o }
cnumer 13125 class numer
cdenom 13126 class denom
df-numer 13127 |- numer  =  ( y  e.  QQ  |->  ( 1st `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
df-denom 13128 |- denom  =  ( y  e.  QQ  |->  ( 2nd `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
codz 13152 class  od
Z
cphi 13153 class  phi
df-odz 13154 |-  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 13155 |- 
phi  =  ( n  e.  NN  |->  ( # `  { x  e.  ( 1 ... n )  |  ( x  gcd  n )  =  1 } ) )
cpc 13210 class  pCnt
df-pc 13211 |-  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 13297 class  ZZ [ _i ]
df-gz 13298 |-  ZZ [ _i ]  =  { x  e.  CC  |  ( ( Re
`  x )  e.  ZZ  /\  ( Im
`  x )  e.  ZZ ) }
cvdwa 13333 class AP
cvdwm 13334 class MonoAP
cvdwp 13335 class PolyAP
df-vdwap 13336 |- AP 
=  ( k  e. 
NN0  |->  ( a  e.  NN ,  d  e.  NN  |->  ran  ( m  e.  ( 0 ... (
k  -  1 ) )  |->  ( a  +  ( m  x.  d
) ) ) ) )
df-vdwmc 13337 |- MonoAP  =  { <. k ,  f
>.  |  E. c
( ran  (AP `  k
)  i^i  ~P ( `' f " {
c } ) )  =/=  (/) }
df-vdwpc 13338 |- 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 13367 class Ramsey
df-ram 13369 |- 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 13465 class Struct
cnx 13466 class  ndx
csts 13467 class sSet
cslot 13468 class Slot  A
cbs 13469 class  Base
cress 13470 classs
df-struct 13471 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( f 
\  { (/) } )  /\  dom  f  C_  ( ... `  x ) ) }
df-ndx 13472 |- 
ndx  =  (  _I  |`  NN )
df-slot 13473 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
df-base 13474 |- 
Base  = Slot  1
df-sets 13475 |- sSet 
=  ( s  e. 
_V ,  e  e. 
_V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u.  { e } ) )
df-ress 13476 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  if ( ( Base `  w
)  C_  x ,  w ,  ( w sSet  <.
( Base `  ndx ) ,  ( x  i^i  ( Base `  w ) )
>. ) ) )
cplusg 13529 class  +g
cmulr 13530 class  .r
cstv 13531 class  * r
csca 13532 class Scalar
cvsca 13533 class  .s
cip 13534 class  .i
cts 13535 class TopSet
cple 13536 class  le
coc 13537 class  oc
cds 13538 class  dist
cunif 13539 class  UnifSet
chom 13540 class  Hom
cco 13541 class comp
df-plusg 13542 |- 
+g  = Slot  2
df-mulr 13543 |- 
.r  = Slot  3
df-starv 13544 |-  * r  = Slot  4
df-sca 13545 |- Scalar  = Slot  5
df-vsca 13546 |-  .s  = Slot  6
df-ip 13547 |-  .i  = Slot  8
df-tset 13548 |- TopSet  = Slot  9
df-ple 13549 |- 
le  = Slot  10
df-ocomp 13550 |-  oc  = Slot ; 1 1
df-ds 13551 |-  dist 
= Slot ; 1 2
df-unif 13552 |- 
UnifSet  = Slot ; 1 3
df-hom 13553 |- 
Hom  = Slot ; 1 4
df-cco 13554 |- comp 
= Slot ; 1 5
crest 13648 classt
ctopn 13649 class  TopOpen
df-rest 13650 |-t  =  ( j  e.  _V ,  x  e.  _V  |->  ran  ( y  e.  j 
|->  ( y  i^i  x
) ) )
df-topn 13651 |-  TopOpen  =  ( w  e. 
_V  |->  ( (TopSet `  w )t  ( Base `  w
) ) )
ctg 13665 class  topGen
cpt 13666 class  Xt_
df-topgen 13667 |- 
topGen  =  ( x  e. 
_V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
df-pt 13668 |-  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 13669 class  X_s
cpws 13670 class  ^s
df-prds 13671 |-  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 13673 |- 
^s  =  ( r  e. 
_V ,  i  e. 
_V  |->  ( (Scalar `  r ) X_s ( i  X.  {
r } ) ) )
cordt 13721 class ordTop
cxrs 13722 class  RR* s
c0g 13723 class  0g
cgsu 13724 class  gsumg
df-ordt 13725 |- 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 13726 |- 
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 13727 |-  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 13728 |- 
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 13729 class qTop
cimas 13730 class  "s
cqus 13731 class  /.s
cxps 13732 class  X.s
df-qtop 13733 |- qTop 
=  ( j  e. 
_V ,  f  e. 
_V  |->  { s  e. 
~P ( f " U. j )  |  ( ( `' f "
s )  i^i  U. j )  e.  j } )
df-imas 13734 |-  "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 13735 |- 
/.s 
=  ( r  e. 
_V ,  e  e. 
_V  |->  ( ( x  e.  ( Base `  r
)  |->  [ x ]
e )  "s  r )
)
df-xps 13736 |- 
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 13807 class Moore
cmrc 13808 class mrCls
cmri 13809 class mrInd
cacs 13810 class ACS
df-mre 13811 |- Moore  =  ( x  e. 
_V  |->  { c  e. 
~P ~P x  |  ( x  e.  c  /\  A. s  e. 
~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
df-mrc 13812 |- mrCls  =  ( c  e. 
U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^|
{ s  e.  c  |  x  C_  s } ) )
df-mri 13813 |- mrInd  =  ( c  e. 
U. ran Moore  |->  { s  e.  ~P U. c  | 
A. x  e.  s  -.  x  e.  ( (mrCls `  c ) `  ( s  \  {
x } ) ) } )
df-acs 13814 |- 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 13889 class  Cat
ccid 13890 class  Id
chomf 13891 class  Homf
ccomf 13892 class compf
df-cat 13893 |- 
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 13894 |-  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 13895 |- 
Homf 
=  ( c  e. 
_V  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( x (  Hom  `  c )
y ) ) )
df-comf 13896 |- 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 13937 class oppCat
df-oppc 13938 |- 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 13954 class Mono
cepi 13955 class Epi
df-mon 13956 |- 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 13957 |- Epi 
=  ( c  e. 
Cat  |-> tpos  (Mono `  (oppCat `  c
) ) )
csect 13970 class Sect
cinv 13971 class Inv
ciso 13972 class  Iso
df-sect 13973 |- 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 13974 |- Inv 
=  ( c  e. 
Cat  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( ( x (Sect `  c )
y )  i^i  `' ( y (Sect `  c ) x ) ) ) )
df-iso 13975 |- 
Iso  =  ( c  e.  Cat  |->  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) ) )
cssc 14007 class  C_cat
cresc 14008 class  |`cat
csubc 14009 class Subcat
df-ssc 14010 |-  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 14011 |-  |`cat 
=  ( c  e. 
_V ,  h  e. 
_V  |->  ( ( cs  dom 
dom  h ) sSet  <. (  Hom  `  ndx ) ,  h >. ) )
df-subc 14012 |- 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 14051 class  Func
cidfu 14052 class idfunc
ccofu 14053 class  o.func
cresf 14054 class  |`f
df-func 14055 |- 
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 14056 |- idfunc  =  ( t  e.  Cat  |->  [_ ( Base `  t
)  /  b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
df-cofu 14057 |-  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 14058 |-  |`f  =  ( f  e. 
_V ,  h  e. 
_V  |->  <. ( ( 1st `  f )  |`  dom  dom  h ) ,  ( x  e.  dom  h  |->  ( ( ( 2nd `  f ) `  x
)  |`  ( h `  x ) ) )
>. )
cful 14099 class Full
cfth 14100 class Faith
df-full 14101 |- 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 14102 |- 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 14138 class Nat
cfuc 14139 class FuncCat
df-nat 14140 |- 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 14141 |- 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 14175 class domA
ccoda 14176 class coda
carw 14177 class Nat
choma 14178 class Homa
df-doma 14179 |- domA  =  ( 1st  o.  1st )
df-coda 14180 |- coda  =  ( 2nd  o.  1st )
df-homa 14181 |- Homa  =  ( c  e.  Cat  |->  ( x  e.  (
( Base `  c )  X.  ( Base `  c
) )  |->  ( { x }  X.  (
(  Hom  `  c ) `
 x ) ) ) )
df-arw 14182 |- Nat 
=  ( c  e. 
Cat  |->  U. ran  (Homa `  c
) )
cida 14208 class Ida
ccoa 14209 class compa
df-ida 14210 |- Ida  =  ( c  e.  Cat  |->  ( x  e.  ( Base `  c )  |->  <.
x ,  x ,  ( ( Id `  c ) `  x
) >. ) )
df-coa 14211 |- 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 14230 class  SetCat
df-setc 14231 |- 
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 14249 class CatCat
df-catc 14250 |- 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 14265 class  X.c
c1stf 14266 class  1stF
c2ndf 14267 class  2ndF
cprf 14268 class ⟨,⟩F
df-xpc 14269 |- 
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 14270 |- 
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 14271 |- 
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 14272 |- ⟨,⟩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 14306 class evalF
ccurf 14307 class curryF
cuncf 14308 class uncurryF
cdiag 14309 class Δfunc
df-evlf 14310 |- 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 14311 |- 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 14312 |- 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 14313 |- Δfunc  =  ( c  e.  Cat ,  d  e.  Cat  |->  (
<. c ,  d >. curryF  ( c  1stF  d ) ) )
chof 14345 class HomF
cyon 14346 class Yon
df-hof 14347 |- 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 14348 |- Yon 
=  ( c  e. 
Cat  |->  ( <. c ,  (oppCat `  c ) >. curryF  (HomF `  (oppCat `  c ) ) ) )
cpreset 14383 class  Preset
cdrs 14384 class Dirset
df-preset 14385 |- 
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 14386 |- Dirset  =  { f  e.  Preset  | 
[. ( Base `  f
)  /  b ]. [. ( le `  f
)  /  r ]. ( b  =/=  (/)  /\  A. x  e.  b  A. y  e.