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 176 wff  ( ph  <->  ps )
df-bi 177 |- 
-.  ( ( (
ph 
<->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ph  <->  ps ) ) )
wo 357 wff  ( ph  \/  ps )
wa 358 wff  ( ph  /\  ps )
df-or 359 |-  ( ( ph  \/  ps )  <->  ( -.  ph  ->  ps ) )
df-an 360 |-  ( ( ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
w3o 933 wff  ( ph  \/  ps  \/  ch )
w3a 934 wff  ( ph  /\  ps  /\ 
ch )
df-3or 935 |-  ( ( ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/ 
ch ) )
df-3an 936 |-  ( ( ph  /\  ps  /\  ch )  <->  ( ( ph  /\  ps )  /\  ch ) )
wnan 1287 wff  ( ph  -/\  ps )
df-nan 1288 |-  ( ( ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
wxo 1295 wff  ( ph  \/_  ps )
df-xor 1296 |-  ( ( ph  \/_  ps ) 
<->  -.  ( ph  <->  ps )
)
wtru 1307 wff 
T.
wfal 1308 wff 
F.
df-tru 1310 |-  (  T.  <->  ( ph  <->  ph ) )
df-fal 1311 |-  (  F.  <->  -.  T.  )
whad 1368 wff hadd
( ph ,  ps ,  ch )
wcad 1369 wff cadd
( ph ,  ps ,  ch )
df-had 1370 |-  (hadd ( ph ,  ps ,  ch )  <->  ( ( ph  \/_  ps )  \/_  ch ) )
df-cad 1371 |-  (cadd ( ph ,  ps ,  ch )  <->  ( ( ph  /\  ps )  \/  ( ch  /\  ( ph  \/_  ps ) ) ) )
ax-meredith 1396 |-  ( ( ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -.  th ) )  ->  ch )  ->  ta )  ->  ( ( ta  ->  ph )  -> 
( th  ->  ph )
) )
wal 1530 wff  A. x ph
wex 1531 wff 
E. x ph
df-ex 1532 |-  ( E. x ph  <->  -.  A. x  -.  ph )
wnf 1534 wff 
F/ x ph
df-nf 1535 |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
ax-gen 1536 |- 
ph   =>    |- 
A. x ph
ax-5 1547 |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
ax-17 1606 |-  ( ph  ->  A. x ph )
cv 1631 class  x
wceq 1632 wff 
A  =  B
wsb 1638 wff 
[ y  /  x ] ph
df-sb 1639 |-  ( [ y  /  x ] ph  <->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph ) ) )
ax-9 1644 |-  -.  A. x  -.  x  =  y
ax-8 1661 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
wcel 1696 wff 
A  e.  B
ax-13 1698 |-  ( x  =  y  ->  ( x  e.  z  ->  y  e.  z ) )
ax-14 1700 |-  ( x  =  y  ->  ( z  e.  x  ->  z  e.  y ) )
ax-6 1715 |-  ( -.  A. x ph  ->  A. x  -.  A. x ph )
ax-7 1720 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-11 1727 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-12 1878 |-  ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
)
ax-4 2087 |-  ( A. x ph  ->  ph )
ax-5o 2088 |-  ( A. x ( A. x ph  ->  ps )  ->  ( A. x ph  ->  A. x ps )
)
ax-6o 2089 |-  ( -.  A. x  -.  A. x ph  ->  ph )
ax-9o 2090 |-  ( A. x ( x  =  y  ->  A. x ph )  ->  ph )
ax-10o 2091 |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph ) )
ax-10 2092 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11o 2093 |-  ( -.  A. x  x  =  y  ->  ( x  =  y  -> 
( ph  ->  A. x
( x  =  y  ->  ph ) ) ) )
ax-12o 2094 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  =  y  ->  A. z  x  =  y ) ) )
ax-15 2095 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  e.  y  ->  A. z  x  e.  y ) ) )
ax-16 2096 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
weu 2156 wff 
E! x ph
wmo 2157 wff 
E* x ph
df-eu 2160 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
df-mo 2161 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
ax-7d 2247 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-8d 2248 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-9d1 2249 |- 
-.  A. x  -.  x  =  x
ax-9d2 2250 |- 
-.  A. x  -.  x  =  y
ax-10d 2251 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11d 2252 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-ext 2277 |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
cab 2282 class  { x  |  ph }
df-clab 2283 |-  ( x  e.  {
y  |  ph }  <->  [ x  /  y ]
ph )
df-cleq 2289 |-  ( A. x ( x  e.  y  <->  x  e.  z )  ->  y  =  z )   =>    |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
df-clel 2292 |-  ( A  e.  B  <->  E. x ( x  =  A  /\  x  e.  B ) )
wnfc 2419 wff  F/_ x A
df-nfc 2421 |-  ( F/_ x A  <->  A. y F/ x  y  e.  A )
wne 2459 wff 
A  =/=  B
wnel 2460 wff 
A  e/  B
df-ne 2461 |-  ( A  =/=  B  <->  -.  A  =  B )
df-nel 2462 |-  ( A  e/  B  <->  -.  A  e.  B )
wral 2556 wff  A. x  e.  A  ph
wrex 2557 wff 
E. x  e.  A  ph
wreu 2558 wff 
E! x  e.  A  ph
wrmo 2559 wff 
E* x  e.  A ph
crab 2560 class  { x  e.  A  |  ph }
df-ral 2561 |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
df-rex 2562 |-  ( E. x  e.  A  ph  <->  E. x
( x  e.  A  /\  ph ) )
df-reu 2563 |-  ( E! x  e.  A  ph  <->  E! x
( x  e.  A  /\  ph ) )
df-rmo 2564 |-  ( E* x  e.  A ph  <->  E* x
( x  e.  A  /\  ph ) )
df-rab 2565 |- 
{ x  e.  A  |  ph }  =  {
x  |  ( x  e.  A  /\  ph ) }
cvv 2801 class  _V
df-v 2803 |-  _V  =  { x  |  x  =  x }
wcdeq 2987 wff CondEq ( x  =  y  ->  ph )
df-cdeq 2988 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 3004 wff  [. A  /  x ]. ph
df-sbc 3005 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 3094 class  [_ A  /  x ]_ B
df-csb 3095 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 3162 class  ( A  \  B )
cun 3163 class  ( A  u.  B )
cin 3164 class  ( A  i^i  B )
wss 3165 wff 
A  C_  B
wpss 3166 wff 
A  C.  B
df-dif 3168 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 3170 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 3172 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 3179 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
df-pss 3181 |-  ( A  C.  B  <->  ( A  C_  B  /\  A  =/=  B ) )
c0 3468 class  (/)
df-nul 3469 |-  (/)  =  ( _V  \  _V )
cif 3578 class  if ( ph ,  A ,  B )
df-if 3579 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3638 class  ~P A
df-pw 3640 |-  ~P A  =  {
x  |  x  C_  A }
csn 3653 class  { A }
cpr 3654 class  { A ,  B }
ctp 3655 class  { A ,  B ,  C }
cop 3656 class  <. A ,  B >.
cotp 3657 class  <. A ,  B ,  C >.
df-sn 3659 |-  { A }  =  {
x  |  x  =  A }
df-pr 3660 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3661 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3662 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3663 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 3843 class  U. A
df-uni 3844 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 3878 class  |^| A
df-int 3879 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 3921 class  U_ x  e.  A  B
ciin 3922 class  |^|_
x  e.  A  B
df-iun 3923 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 3924 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 4009 wff Disj  x  e.  A B
df-disj 4010 |-  (Disj  x  e.  A B 
<-> 
A. y E* x  e.  A y  e.  B
)
wbr 4039 wff 
A R B
df-br 4040 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 4092 class  {
<. x ,  y >.  |  ph }
cmpt 4093 class  ( x  e.  A  |->  B )
df-opab 4094 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 4095 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 4129 wff 
Tr  A
df-tr 4130 |-  ( Tr  A  <->  U. A  C_  A )
ax-rep 4147 |-  ( 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 4157 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 4165 |- 
E. x A. y  -.  y  e.  x
ax-pow 4204 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
ax-pr 4230 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4319 class  _E
cid 4320 class  _I
df-eprel 4321 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4325 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4328 wff 
R  Po  A
wor 4329 wff 
R  Or  A
df-po 4330 |-  ( 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 4331 |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) ) )
wfr 4365 wff 
R  Fr  A
wse 4366 wff 
R Se  A
wwe 4367 wff 
R  We  A
df-fr 4368 |-  ( R  Fr  A  <->  A. x ( ( x 
C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
df-se 4369 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-we 4370 |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A )
)
word 4407 wff 
Ord  A
con0 4408 class  On
wlim 4409 wff 
Lim  A
csuc 4410 class  suc 
A
df-ord 4411 |-  ( Ord  A  <->  ( Tr  A  /\  _E  We  A
) )
df-on 4412 |-  On  =  { x  |  Ord  x }
df-lim 4413 |-  ( Lim  A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
df-suc 4414 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4528 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
com 4672 class  om
df-om 4673 |-  om  =  { x  e.  On  |  A. y
( Lim  y  ->  x  e.  y ) }
cxp 4703 class  ( A  X.  B )
ccnv 4704 class  `' A
cdm 4705 class  dom 
A
crn 4706 class  ran 
A
cres 4707 class  ( A  |`  B )
cima 4708 class  ( A " B )
ccom 4709 class  ( A  o.  B )
wrel 4710 wff 
Rel  A
df-xp 4711 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4712 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4713 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4714 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4715 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4716 |-  ran  A  =  dom  `' A
df-res 4717 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4718 |-  ( A " B
)  =  ran  ( A  |`  B )
cio 5233 class  ( iota x ph )
df-iota 5235 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
wfun 5265 wff 
Fun  A
wfn 5266 wff 
A  Fn  B
wf 5267 wff 
F : A --> B
wf1 5268 wff 
F : A -1-1-> B
wfo 5269 wff 
F : A -onto-> B
wf1o 5270 wff 
F : A -1-1-onto-> B
cfv 5271 class  ( F `  A )
wiso 5272 wff 
H  Isom  R ,  S  ( A ,  B )
df-fun 5273 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 5274 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 5275 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 5276 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 5277 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 5278 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 5279 |-  ( F `  A )  =  ( iota x A F x )
df-isom 5280 |-  ( 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 5874 class  ( A F B )
coprab 5875 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpt2 5876 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 5877 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 5878 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpt2 5879 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 6092 class  o F R
cofr 6093 class  o R R
df-of 6094 |-  o F R  =  ( f  e.  _V , 
g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 6095 |-  o R R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 6136 class  1st
c2nd 6137 class  2nd
df-1st 6138 |- 
1st  =  ( x  e.  _V  |->  U. dom  { x } )
df-2nd 6139 |- 
2nd  =  ( x  e.  _V  |->  U. ran  { x } )
ctpos 6249 class tpos  F
df-tpos 6250 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
ccur 6288 class curry  A
cunc 6289 class uncurry  A
df-cur 6290 |- curry  F  =  ( x  e.  dom  dom  F  |->  {
<. y ,  z >.  |  <. x ,  y
>. F z } )
df-unc 6291 |- uncurry  F  =  { <. <. x ,  y >. ,  z
>.  |  y ( F `  x )
z }
crpss 6292 class [ C.]
df-rpss 6293 |- [
C.]  =  { <. x ,  y >.  |  x 
C.  y }
cund 6312 class  Undef
crio 6313 class  (
iota_ x  e.  A ph )
df-undef 6314 |- 
Undef  =  ( s  e.  _V  |->  ~P U. s )
df-riota 6320 |-  ( iota_ x  e.  A ph )  =  if ( E! x  e.  A  ph ,  ( iota x
( x  e.  A  /\  ph ) ) ,  ( Undef `  { x  |  x  e.  A } ) )
wsmo 6378 wff 
Smo  A
df-smo 6379 |-  ( 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 6403 class recs ( F )
df-recs 6404 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 6438 class  rec ( F ,  I
)
df-rdg 6439 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  if ( g  =  (/) ,  I ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) ) )
cseqom 6475 class seq𝜔 ( F ,  I )
df-seqom 6476 |- seq𝜔 ( F ,  I )  =  ( rec (
( i  e.  om ,  v  e.  _V  |->  <. suc  i ,  ( i F v )
>. ) ,  <. (/) ,  (  _I  `  I )
>. ) " om )
c1o 6488 class  1o
c2o 6489 class  2o
c3o 6490 class  3o
c4o 6491 class  4o
coa 6492 class  +o
comu 6493 class  .o
coe 6494 class  ^o
df-1o 6495 |-  1o  =  suc  (/)
df-2o 6496 |-  2o  =  suc  1o
df-3o 6497 |-  3o  =  suc  2o
df-4o 6498 |-  4o  =  suc  3o
df-oadd 6499 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6500 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexp 6501 |- 
^o  =  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
wer 6673 wff 
R  Er  A
cec 6674 class  [ A ] R
cqs 6675 class  ( A /. R )
df-er 6676 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6678 |-  [ A ] R  =  ( R " { A } )
df-qs 6682 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cmap 6788 class  ^m
cpm 6789 class  ^pm
df-map 6790 |- 
^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
df-pm 6791 |-  ^pm  =  ( x  e. 
_V ,  y  e. 
_V  |->  { f  e. 
~P ( y  X.  x )  |  Fun  f } )
cixp 6833 class  X_ x  e.  A  B
df-ixp 6834 |-  X_ x  e.  A  B  =  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
cen 6876 class  ~~
cdom 6877 class  ~<_
csdm 6878 class  ~<
cfn 6879 class  Fin
df-en 6880 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 6881 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-sdom 6882 |- 
~<  =  (  ~<_  \  ~~  )
df-fin 6883 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
cfi 7180 class  fi
df-fi 7181 |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
csup 7209 class  sup ( A ,  B ,  R )
df-sup 7210 |- 
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 7240 class OrdIso ( R ,  A )
df-oi 7241 |- 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 7286 class har
cwdom 7287 class  ~<_*
df-har 7288 |- har 
=  ( x  e. 
_V  |->  { y  e.  On  |  y  ~<_  x } )
df-wdom 7289 |-  ~<_*  =  { <. x ,  y
>.  |  ( x  =  (/)  \/  E. z 
z : y -onto-> x ) }
ax-reg 7322 |-  ( E. y  y  e.  x  ->  E. y
( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x )
) )
ax-inf 7355 |- 
E. y ( x  e.  y  /\  A. z ( z  e.  y  ->  E. w
( z  e.  w  /\  w  e.  y
) ) )
ax-inf2 7358 |- 
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 7378 class CNF
df-cnf 7379 |- 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 7437 class  TC
df-tc 7438 |-  TC  =  ( x  e.  _V  |->  |^| { y  |  ( x  C_  y  /\  Tr  y ) } )
cr1 7450 class  R1
crnk 7451 class  rank
df-r1 7452 |-  R1  =  rec (
( x  e.  _V  |->  ~P x ) ,  (/) )
df-rank 7453 |- 
rank  =  ( x  e.  _V  |->  |^| { y  e.  On  |  x  e.  ( R1 `  suc  y ) } )
ccrd 7584 class  card
cale 7585 class  aleph
ccf 7586 class  cf
wacn 7587 class AC  A
df-card 7588 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
df-aleph 7589 |-  aleph  =  rec (har ,  om )
df-cf 7590 |-  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 7591 |- 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 7758 wff CHOICE
df-ac 7759 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x ) )
ccda 7809 class  +c
df-cda 7810 |- 
+c  =  ( x  e.  _V ,  y  e.  _V  |->  ( ( x  X.  { (/) } )  u.  ( y  X.  { 1o }
) ) )
cfin1a 7920 class FinIa
cfin2 7921 class FinII
cfin4 7922 class FinIV
cfin3 7923 class FinIII
cfin5 7924 class FinV
cfin6 7925 class FinVI
cfin7 7926 class FinVII
df-fin1a 7927 |- FinIa  =  { x  |  A. y  e.  ~P  x
( y  e.  Fin  \/  ( x  \  y
)  e.  Fin ) }
df-fin2 7928 |- FinII  =  { x  |  A. y  e.  ~P  ~P x
( ( y  =/=  (/)  /\ [ C.]  Or  y
)  ->  U. y  e.  y ) }
df-fin4 7929 |- FinIV  =  { x  |  -.  E. y ( y  C.  x  /\  y  ~~  x
) }
df-fin3 7930 |- FinIII  =  { x  |  ~P x  e. FinIV }
df-fin5 7931 |- FinV  =  { x  |  ( x  =  (/)  \/  x  ~<  ( x  +c  x
) ) }
df-fin6 7932 |- FinVI  =  { x  |  ( x  ~<  2o  \/  x  ~<  ( x  X.  x ) ) }
df-fin7 7933 |- FinVII  =  { x  |  -.  E. y  e.  ( On 
\  om ) x 
~~  y }
ax-cc 8077 |-  ( x  ~~  om  ->  E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
ax-dc 8088 |-  ( ( 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 8101 |-  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 8105 |- 
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 8258 class GCH
df-gch 8259 |- GCH 
=  ( Fin  u.  { x  |  A. y  -.  ( x  ~<  y  /\  y  ~<  ~P x
) } )
cwina 8320 class  Inacc W
cina 8321 class  Inacc
df-wina 8322 |- 
Inacc W  =  {
x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z
) }
df-ina 8323 |- 
Inacc  =  { x  |  ( x  =/=  (/)  /\  ( cf `  x
)  =  x  /\  A. y  e.  x  ~P y  ~<  x ) }
cwun 8338 class WUni
cwunm 8339 class wUniCl
df-wun 8340 |- 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 8341 |- wUniCl  =  ( x  e. 
_V  |->  |^| { u  e. WUni  |  x  C_  u }
)
ctsk 8386 class  Tarski
df-tsk 8387 |- 
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 8428 class  Univ
df-gru 8429 |- 
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 8461 |- 
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 8475 class  tarskiMap
df-tskm 8476 |-  tarskiMap 
=  ( x  e. 
_V  |->  |^| { y  e. 
Tarski  |  x  e.  y } )
cnpi 8482 class  N.
cpli 8483 class  +N
cmi 8484 class  .N
clti 8485 class  <N
cplpq 8486 class  +pQ
cmpq 8487 class  .pQ
cltpq 8488 class  <pQ
ceq 8489 class  ~Q
cnq 8490 class  Q.
c1q 8491 class  1Q
cerq 8492 class  /Q
cplq 8493 class  +Q
cmq 8494 class  .Q
crq 8495 class  *Q
cltq 8496 class  <Q
cnp 8497 class  P.
c1p 8498 class  1P
cpp 8499 class  +P.
cmp 8500 class  .P.
cltp 8501 class  <P
cplpr 8502 class  +pR
cmpr 8503 class  .pR
cer 8504 class  ~R
cnr 8505 class  R.
c0r 8506 class  0R
c1r 8507 class  1R
cm1r 8508 class  -1R
cplr 8509 class  +R
cmr 8510 class  .R
cltr 8511 class  <R
df-ni 8512 |-  N.  =  ( om  \  { (/) } )
df-pli 8513 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 8514 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 8515 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 8548 |- 
+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 8549 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 8550 |- 
<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 8551 |- 
~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 8552 |-  Q.  =  { x  e.  ( N.  X.  N. )  |  A. y  e.  ( N.  X.  N. ) ( x  ~Q  y  ->  -.  ( 2nd `  y )  <N  ( 2nd `  x ) ) }
df-erq 8553 |- 
/Q  =  (  ~Q  i^i  ( ( N.  X.  N. )  X.  Q. )
)
df-plq 8554 |- 
+Q  =  ( ( /Q  o.  +pQ  )  |`  ( Q.  X.  Q. ) )
df-mq 8555 |-  .Q  =  ( ( /Q  o.  .pQ  )  |`  ( Q.  X.  Q. ) )
df-1nq 8556 |-  1Q  =  <. 1o ,  1o >.
df-rq 8557 |-  *Q  =  ( `'  .Q  " { 1Q } )
df-ltnq 8558 |- 
<Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
df-np 8621 |-  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 8622 |-  1P  =  { x  |  x  <Q  1Q }
df-plp 8623 |- 
+P.  =  ( x  e.  P. ,  y  e.  P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  +Q  u ) } )
df-mp 8624 |-  .P.  =  ( x  e. 
P. ,  y  e. 
P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  .Q  u ) } )
df-ltp 8625 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  x  C.  y ) }
df-plpr 8695 |- 
+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 8696 |- 
.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 8697 |- 
~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 8698 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 8699 |- 
+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 8700 |-  .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 8701 |- 
<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 8702 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 8703 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 8704 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 8751 class  CC
cr 8752 class  RR
cc0 8753 class  0
c1 8754 class  1
ci 8755 class  _i
caddc 8756 class  +
cltrr 8757 class  <RR
cmul 8758 class  x.
df-c 8759 |-  CC  =  ( R.  X.  R. )
df-0 8760 |-  0  =  <. 0R ,  0R >.
df-1 8761 |-  1  =  <. 1R ,  0R >.
df-i 8762 |-  _i  =  <. 0R ,  1R >.
df-r 8763 |-  RR  =  ( R.  X.  { 0R } )
df-add 8764 |-  +  =  { <. <.
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 8765 |-  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 8766 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 8809 |-  CC  e.  _V
ax-resscn 8810 |-  RR  C_  CC
ax-1cn 8811 |-  1  e.  CC
ax-icn 8812 |-  _i  e.  CC
ax-addcl 8813 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 8814 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 8815 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 8816 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-mulcom 8817 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 8818 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 8819 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 8820 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 8821 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-1ne0 8822 |-  1  =/=  0
ax-1rid 8823 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-rnegex 8824 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-rrecex 8825 |-  ( ( A  e.  RR  /\  A  =/=  0 )  ->  E. x  e.  RR  ( A  x.  x )  =  1 )
ax-cnre 8826 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-lttri 8827 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <RR  B  <->  -.  ( A  =  B  \/  B  <RR  A ) ) )
ax-pre-lttrn 8828 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-ltadd 8829 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 8830 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-sup 8831 |-  ( ( 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 8832 |-  +  : ( CC 
X.  CC ) --> CC
ax-mulf 8833 |-  x.  : ( CC 
X.  CC ) --> CC
cpnf 8880 class  +oo
cmnf 8881 class  -oo
cxr 8882 class  RR*
clt 8883 class  <
cle 8884 class  <_
df-pnf 8885 |- 
+oo  =  ~P U. CC
df-mnf 8886 |- 
-oo  =  ~P  +oo
df-xr 8887 |-  RR*  =  ( RR  u.  { 
+oo ,  -oo } )
df-ltxr 8888 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { 
-oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) ) )
df-le 8889 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 9053 class  -
cneg 9054 class  -u A
df-sub 9055 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC ( y  +  z )  =  x ) )
df-neg 9056 |-  -u A  =  (
0  -  A )
cdiv 9439 class  /
df-div 9440 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC ( y  x.  z
)  =  x ) )
cn 9762 class  NN
df-nn 9763 |-  NN  =  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )
c2 9811 class  2
c3 9812 class  3
c4 9813 class  4
c5 9814 class  5
c6 9815 class  6
c7 9816 class  7
c8 9817 class  8
c9 9818 class  9
c10 9819 class  10
df-2 9820 |-  2  =  ( 1  +  1 )
df-3 9821 |-  3  =  ( 2  +  1 )
df-4 9822 |-  4  =  ( 3  +  1 )
df-5 9823 |-  5  =  ( 4  +  1 )
df-6 9824 |-  6  =  ( 5  +  1 )
df-7 9825 |-  7  =  ( 6  +  1 )
df-8 9826 |-  8  =  ( 7  +  1 )
df-9 9827 |-  9  =  ( 8  +  1 )
df-10 9828 |-  10  =  ( 9  +  1 )
cn0 9981 class  NN0
df-n0 9982 |-  NN0  =  ( NN  u.  { 0 } )
cz 10040 class  ZZ
df-z 10041 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 10140 class ; A B
df-dec 10141 |- ; A B  =  ( ( 10  x.  A )  +  B )
cuz 10246 class  ZZ>=
df-uz 10247 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 10332 class  QQ
df-q 10333 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 10370 class  RR+
df-rp 10371 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 10465 class  - e A
cxad 10466 class  + e
cxmu 10467 class  x e
df-xneg 10468 |-  - e A  =  if ( A  =  +oo , 
-oo ,  if ( A  =  -oo ,  +oo , 
-u A ) )
df-xadd 10469 |-  + 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 10470 |-  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 10672 class  (,)
cioc 10673 class  (,]
cico 10674 class  [,)
cicc 10675 class  [,]
df-ioo 10676 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 10677 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 10678 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 10679 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 10798 class  ...
df-fz 10799 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 10886 class ..^
df-fzo 10887 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 10940 class  |_
df-fl 10941 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
cmo 10989 class  mod
df-mod 10990 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 11062 class  seq 
M (  .+  ,  F )
df-seq 11063 |- 
seq  M (  .+  ,  F )  =  ( rec ( ( x  e.  _V ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. ) " om )
cexp 11120 class  ^
df-exp 11121 |- 
^  =  ( 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 11304 class  !
df-fac 11305 |-  !  =  ( {
<. 0 ,  1
>. }  u.  seq  1
(  x.  ,  _I  ) )
cbc 11331 class  _C
df-bc 11332 |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n
)  /  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) ) ) ,  0 ) )
chash 11353 class  #
df-hash 11354 |-  #  =  ( (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om )  o.  card )  u.  ( ( _V  \  Fin )  X. 
{  +oo } ) )
cword 11419 class Word  S
cconcat 11420 class concat
cs1 11421 class  <" A ">
csubstr 11422 class substr
csplice 11423 class splice
creverse 11424 class reverse
df-word 11425 |- Word  S  =  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
df-concat 11426 |- concat  =  ( s  e. 
_V ,  t  e. 
_V  |->  ( x  e.  ( 0..^ ( (
# `  s )  +  ( # `  t
) ) )  |->  if ( x  e.  ( 0..^ ( # `  s
) ) ,  ( s `  x ) ,  ( t `  ( x  -  ( # `
 s ) ) ) ) ) )
df-s1 11427 |-  <" A ">  =  { <. 0 ,  (  _I  `  A )
>. }
df-substr 11428 |- 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 11429 |- 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 11430 |- reverse  =  ( s  e. 
_V  |->  ( x  e.  ( 0..^ ( # `  s ) )  |->  ( s `  ( ( ( # `  s
)  -  1 )  -  x ) ) ) )
cs2 11507 class  <" A B ">
cs3 11508 class  <" A B C ">
cs4 11509 class  <" A B C D ">
cs5 11510 class  <" A B C D E ">
cs6 11511 class  <" A B C D E F ">
cs7 11512 class  <" A B C D E F G ">
cs8 11513 class  <" A B C D E F G H ">
df-s2 11514 |-  <" A B ">  =  ( <" A "> concat  <" B "> )
df-s3 11515 |-  <" A B C ">  =  (
<" A B "> concat 
<" C "> )
df-s4 11516 |-  <" A B C D ">  =  ( <" A B C "> concat  <" D "> )
df-s5 11517 |-  <" A B C D E ">  =  ( <" A B C D "> concat  <" E "> )
df-s6 11518 |-  <" A B C D E F ">  =  ( <" A B C D E "> concat 
<" F "> )
df-s7 11519 |-  <" A B C D E F G ">  =  (
<" A B C D E F "> concat 
<" G "> )
df-s8 11520 |-  <" A B C D E F G H ">  =  ( <" A B C D E F G "> concat  <" H "> )
cshi 11577 class  shift
df-shft 11578 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 11597 class  *
cre 11598 class  Re
cim 11599 class  Im
df-cj 11600 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 11601 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 11602 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqr 11734 class  sqr
cabs 11735 class  abs
df-sqr 11736 |- 
sqr  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
df-abs 11737 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
clsp 11960 class  limsup
df-limsup 11961 |- 
limsup  =  ( x  e. 
_V  |->  sup ( ran  (
k  e.  RR  |->  sup ( ( ( x
" ( k [,) 
+oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  ) )
cli 11974 class  ~~>
crli 11975 class  ~~> r
co1 11976 class  O ( 1 )
clo1 11977 class  <_
O ( 1 )
df-clim 11978 |-  ~~>  =  { <. 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 11979 |-  ~~> 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 11980 |-  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 11981 |- 
<_ 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 12174 class  sum_ k  e.  A  B
df-sum 12175 |- 
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 12359 class  exp
ceu 12360 class  _e
csin 12361 class  sin
ccos 12362 class  cos
ctan 12363 class  tan
cpi 12364 class  pi
df-ef 12365 |-  exp  =  ( x  e.  CC  |->  sum_ k  e.  NN0  ( ( x ^
k )  /  ( ! `  k )
) )
df-e 12366 |-  _e  =  ( exp `  1 )
df-sin 12367 |- 
sin  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  -  ( exp `  ( -u _i  x.  x ) ) )  /  ( 2  x.  _i ) ) )
df-cos 12368 |- 
cos  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  +  ( exp `  ( -u _i  x.  x ) ) )  /  2 ) )
df-tan 12369 |- 
tan  =  ( x  e.  ( `' cos " ( CC  \  {
0 } ) ) 
|->  ( ( sin `  x
)  /  ( cos `  x ) ) )
df-pi 12370 |-  pi  =  sup (
( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  `'  <  )
cdivides 12547 class  ||
df-dvds 12548 |- 
||  =  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
cbits 12626 class bits
csad 12627 class sadd
csmu 12628 class smul
df-bits 12629 |- bits 
=  ( n  e.  ZZ  |->  { m  e. 
NN0  |  -.  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) ) } )
df-sad 12658 |- 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 12683 |- 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 12701 class  gcd
df-gcd 12702 |- 
gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
cprime 12774 class  Prime
df-prm 12775 |- 
Prime  =  { p  e.  NN  |  { n  e.  NN  |  n  ||  p }  ~~  2o }
cnumer 12820 class numer
cdenom 12821 class denom
df-numer 12822 |- numer  =  ( y  e.  QQ  |->  ( 1st `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
df-denom 12823 |- denom  =  ( y  e.  QQ  |->  ( 2nd `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
codz 12847 class  od
Z
cphi 12848 class  phi
df-odz 12849 |-  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 12850 |- 
phi  =  ( n  e.  NN  |->  ( # `  { x  e.  ( 1 ... n )  |  ( x  gcd  n )  =  1 } ) )
cpc 12905 class  pCnt
df-pc 12906 |-  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 12992 class  ZZ [ _i ]
df-gz 12993 |-  ZZ [ _i ]  =  { x  e.  CC  |  ( ( Re
`  x )  e.  ZZ  /\  ( Im
`  x )  e.  ZZ ) }
cvdwa 13028 class AP
cvdwm 13029 class MonoAP
cvdwp 13030 class PolyAP
df-vdwap 13031 |- AP 
=  ( k  e. 
NN0  |->  ( a  e.  NN ,  d  e.  NN  |->  ran  ( m  e.  ( 0 ... (
k  -  1 ) )  |->  ( a  +  ( m  x.  d
) ) ) ) )
df-vdwmc 13032 |- MonoAP  =  { <. k ,  f
>.  |  E. c
( ran  (AP `  k
)  i^i  ~P ( `' f " {
c } ) )  =/=  (/) }
df-vdwpc 13033 |- 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 13062 class Ramsey
df-ram 13064 |- 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 13160 class Struct
cnx 13161 class  ndx
csts 13162 class sSet
cslot 13163 class Slot  A
cbs 13164 class  Base
cress 13165 classs
df-struct 13166 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( f 
\  { (/) } )  /\  dom  f  C_  ( ... `  x ) ) }
df-ndx 13167 |- 
ndx  =  (  _I  |`  NN )
df-slot 13168 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
df-base 13169 |- 
Base  = Slot  1
df-sets 13170 |- sSet 
=  ( s  e. 
_V ,  e  e. 
_V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u.  { e } ) )
df-ress 13171 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  if ( ( Base `  w
)  C_  x ,  w ,  ( w sSet  <.
( Base `  ndx ) ,  ( x  i^i  ( Base `  w ) )
>. ) ) )
cplusg 13224 class  +g
cmulr 13225 class  .r
cstv 13226 class  * r
csca 13227 class Scalar
cvsca 13228 class  .s
cip 13229 class  .i
cts 13230 class TopSet
cple 13231 class  le
coc 13232 class  oc
cds 13233 class  dist
cunif 13234 class  Unif
chom 13235 class  Hom
cco 13236 class comp
df-plusg 13237 |- 
+g  = Slot  2
df-mulr 13238 |- 
.r  = Slot  3
df-starv 13239 |-  * r  = Slot  4
df-sca 13240 |- Scalar  = Slot  5
df-vsca 13241 |-  .s  = Slot  6
df-ip 13242 |-  .i  = Slot  8
df-tset 13243 |- TopSet  = Slot  9
df-ple 13244 |- 
le  = Slot  10
df-ocomp 13245 |-  oc  = Slot ; 1 1
df-ds 13246 |-  dist 
= Slot ; 1 2
df-unif 13247 |- 
Unif  = Slot ; 1 3
df-hom 13248 |- 
Hom  = Slot ; 1 4
df-cco 13249 |- comp 
= Slot ; 1 5
crest 13341 classt
ctopn 13342 class  TopOpen
df-rest 13343 |-t  =  ( j  e.  _V ,  x  e.  _V  |->  ran  ( y  e.  j 
|->  ( y  i^i  x
) ) )
df-topn 13344 |-  TopOpen  =  ( w  e. 
_V  |->  ( (TopSet `  w )t  ( Base `  w
) ) )
ctg 13358 class  topGen
cpt 13359 class  Xt_
df-topgen 13360 |- 
topGen  =  ( x  e. 
_V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
df-pt 13361 |-  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 13362 class  X_s
cpws 13363 class  ^s
df-prds 13364 |-  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 13366 |- 
^s  =  ( r  e. 
_V ,  i  e. 
_V  |->  ( (Scalar `  r ) X_s ( i  X.  {
r } ) ) )
cordt 13414 class ordTop
cxrs 13415 class  RR* s
c0g 13416 class  0g
cgsu 13417 class  gsumg
df-ordt 13418 |- 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 13419 |- 
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 13420 |-  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 13421 |- 
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 13422 class qTop
cimas 13423 class  "s
cqus 13424 class  /.s
cxps 13425 class  X.s
df-qtop 13426 |- qTop 
=  ( j  e. 
_V ,  f  e. 
_V  |->  { s  e. 
~P ( f " U. j )  |  ( ( `' f "
s )  i^i  U. j )  e.  j } )
df-imas 13427 |-  "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 13428 |- 
/.s 
=  ( r  e. 
_V ,  e  e. 
_V  |->  ( ( x  e.  ( Base `  r
)  |->  [ x ]
e )  "s  r )
)
df-xps 13429 |- 
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 13500 class Moore
cmrc 13501 class mrCls
cmri 13502 class mrInd
cacs 13503 class ACS
df-mre 13504 |- Moore  =  ( x  e. 
_V  |->  { c  e. 
~P ~P x  |  ( x  e.  c  /\  A. s  e. 
~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
df-mrc 13505 |- mrCls  =  ( c  e. 
U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^|
{ s  e.  c  |  x  C_  s } ) )
df-mri 13506 |- mrInd  =  ( c  e. 
U. ran Moore  |->  { s  e.  ~P U. c  | 
A. x  e.  s  -.  x  e.  ( (mrCls `  c ) `  ( s  \  {
x } ) ) } )
df-acs 13507 |- 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 13582 class  Cat
ccid 13583 class  Id
chomf 13584 class  Homf
ccomf 13585 class compf
df-cat 13586 |- 
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 13587 |-  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 13588 |- 
Homf 
=  ( c  e. 
_V  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( x (  Hom  `  c )
y ) ) )
df-comf 13589 |- 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 13630 class oppCat
df-oppc 13631 |- 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 13647 class Mono
cepi 13648 class Epi
df-mon 13649 |- 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 13650 |- Epi 
=  ( c  e. 
Cat  |-> tpos  (Mono `  (oppCat `  c
) ) )
csect 13663 class Sect
cinv 13664 class Inv
ciso 13665 class  Iso
df-sect 13666 |- 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 13667 |- Inv 
=  ( c  e. 
Cat  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( ( x (Sect `  c )
y )  i^i  `' ( y (Sect `  c ) x ) ) ) )
df-iso 13668 |- 
Iso  =  ( c  e.  Cat  |->  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) ) )
cssc 13700 class  C_cat
cresc 13701 class  |`cat
csubc 13702 class Subcat
df-ssc 13703 |-  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 13704 |-  |`cat 
=  ( c  e. 
_V ,  h  e. 
_V  |->  ( ( cs  dom 
dom  h ) sSet  <. (  Hom  `  ndx ) ,  h >. ) )
df-subc 13705 |- 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 13744 class  Func
cidfu 13745 class idfunc
ccofu 13746 class  o.func
cresf 13747 class  |`f
df-func 13748 |- 
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 13749 |- idfunc  =  ( t  e.  Cat  |->  [_ ( Base `  t
)  /  b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
df-cofu 13750 |-  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 13751 |-  |`f  =  ( f  e. 
_V ,  h  e. 
_V  |->  <. ( ( 1st `  f )  |`  dom  dom  h ) ,  ( x  e.  dom  h  |->  ( ( ( 2nd `  f ) `  x
)  |`  ( h `  x ) ) )
>. )
cful 13792 class Full
cfth 13793 class Faith
df-full 13794 |- 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 13795 |- 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 13831 class Nat
cfuc 13832 class FuncCat
df-nat 13833 |- 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 13834 |- 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 13868 class domA
ccoda 13869 class coda
carw 13870 class Nat
choma 13871 class Homa
df-doma 13872 |- domA  =  ( 1st  o.  1st )
df-coda 13873 |- coda  =  ( 2nd  o.  1st )
df-homa 13874 |- Homa  =  ( c  e.  Cat  |->  ( x  e.  (
( Base `  c )  X.  ( Base `  c
) )  |->  ( { x }  X.  (
(  Hom  `  c ) `
 x ) ) ) )
df-arw 13875 |- Nat 
=  ( c  e. 
Cat  |->  U. ran  (Homa `  c
) )
cida 13901 class Ida
ccoa 13902 class compa
df-ida 13903 |- Ida  =  ( c  e.  Cat  |->  ( x  e.  ( Base `  c )  |->  <.
x ,  x ,  ( ( Id `  c ) `  x
) >. ) )
df-coa 13904 |- 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 13923 class  SetCat
df-setc 13924 |- 
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 13942 class CatCat
df-catc 13943 |- 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 13958 class  X.c
c1stf 13959 class  1stF
c2ndf 13960 class  2ndF
cprf 13961 class ⟨,⟩F
df-xpc 13962 |- 
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 13963 |- 
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 13964 |- 
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 13965 |- ⟨,⟩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 13999 class evalF
ccurf 14000 class curryF
cuncf 14001 class uncurryF
cdiag 14002 class Δfunc
df-evlf 14003 |- 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 14004 |- 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 14005 |- 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 14006 |- Δfunc  =  ( c  e.  Cat ,  d  e.  Cat  |->  (
<. c ,  d >. curryF  ( c  1stF  d ) ) )
chof 14038 class HomF
cyon 14039 class Yon
df-hof 14040 |- 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 14041 |- Yon 
=  ( c  e. 
Cat  |->  ( <. c ,  (oppCat `  c ) >. curryF  (HomF `  (oppCat `  c ) ) ) )
cpreset 14076 class  Preset
cdrs 14077 class Dirset
df-preset 14078 |- 
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 14079 |- Dirset  =  { f  e.