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

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 5 wff 
-.  ph
wi 6 wff  ( ph  ->  ps )
ax-1 7 |-  ( ph  ->  ( ps  ->  ph ) )
ax-2 8 |-  ( ( ph  ->  ( ps  ->  ch )
)  ->  ( ( ph  ->  ps )  -> 
( ph  ->  ch )
) )
ax-3 9 |-  ( ( -.  ph  ->  -.  ps )  -> 
( ps  ->  ph )
)
ax-mp 10 |- 
ph   &    |-  ( ph  ->  ps )   =>    |- 
ps
wb 178 wff  ( ph  <->  ps )
df-bi 179 |- 
-.  ( ( (
ph 
<->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ph  <->  ps ) ) )
wo 359 wff  ( ph  \/  ps )
wa 360 wff  ( ph  /\  ps )
df-or 361 |-  ( ( ph  \/  ps )  <->  ( -.  ph  ->  ps ) )
df-an 362 |-  ( ( ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
w3o 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 1289 wff  ( ph  -/\  ps )
df-nan 1290 |-  ( ( ph  -/\  ps )  <->  -.  ( ph  /\  ps ) )
wxo 1297 wff  ( ph \/_ ps )
df-xor 1298 |-  ( ( ph \/_ ps )  <->  -.  ( ph  <->  ps ) )
wtru 1309 wff 
T.
wfal 1310 wff 
F.
df-tru 1312 |-  (  T.  <->  ( ph  <->  ph ) )
df-fal 1313 |-  (  F.  <->  -.  T.  )
whad 1370 wff hadd
( ph ,  ps ,  ch )
wcad 1371 wff cadd
( ph ,  ps ,  ch )
df-had 1372 |-  (hadd ( ph ,  ps ,  ch )  <->  ( ( ph \/_ ps ) \/_ ch ) )
df-cad 1373 |-  (cadd ( ph ,  ps ,  ch )  <->  ( ( ph  /\  ps )  \/  ( ch  /\  ( ph \/_ ps ) ) ) )
ax-meredith 1398 |-  ( ( ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -.  th ) )  ->  ch )  ->  ta )  ->  ( ( ta  ->  ph )  -> 
( th  ->  ph )
) )
wal 1529 wff  A. x ph
wex 1530 wff 
E. x ph
df-ex 1531 |-  ( E. x ph  <->  -.  A. x  -.  ph )
wnf 1533 wff 
F/ x ph
df-nf 1534 |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
ax-gen 1535 |- 
ph   =>    |- 
A. x ph
ax-5 1546 |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
ax-17 1605 |-  ( ph  ->  A. x ph )
cv 1624 class  x
wceq 1625 wff 
A  =  B
wsb 1632 wff 
[ y  /  x ] ph
df-sb 1633 |-  ( [ y  /  x ] ph  <->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph ) ) )
ax-9 1638 |-  -.  A. x  -.  x  =  y
ax-8 1646 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
wcel 1687 wff 
A  e.  B
ax-13 1689 |-  ( x  =  y  ->  ( x  e.  z  ->  y  e.  z ) )
ax-14 1691 |-  ( x  =  y  ->  ( z  e.  x  ->  z  e.  y ) )
ax-6 1706 |-  ( -.  A. x ph  ->  A. x  -.  A. x ph )
ax-7 1711 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-11 1718 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-12 1870 |-  ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
)
ax-4 2079 |-  ( A. x ph  ->  ph )
ax-5o 2080 |-  ( A. x ( A. x ph  ->  ps )  ->  ( A. x ph  ->  A. x ps )
)
ax-6o 2081 |-  ( -.  A. x  -.  A. x ph  ->  ph )
ax-9o 2082 |-  ( A. x ( x  =  y  ->  A. x ph )  ->  ph )
ax-10o 2083 |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph ) )
ax-10 2084 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11o 2085 |-  ( -.  A. x  x  =  y  ->  ( x  =  y  -> 
( ph  ->  A. x
( x  =  y  ->  ph ) ) ) )
ax-12o 2086 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  =  y  ->  A. z  x  =  y ) ) )
ax-15 2087 |-  ( -.  A. z 
z  =  x  -> 
( -.  A. z 
z  =  y  -> 
( x  e.  y  ->  A. z  x  e.  y ) ) )
ax-16 2088 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
weu 2146 wff 
E! x ph
wmo 2147 wff 
E* x ph
df-eu 2150 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
df-mo 2151 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
ax-7d 2237 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-8d 2238 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-9d1 2239 |- 
-.  A. x  -.  x  =  x
ax-9d2 2240 |- 
-.  A. x  -.  x  =  y
ax-10d 2241 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11d 2242 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-ext 2267 |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
cab 2272 class  { x  |  ph }
df-clab 2273 |-  ( x  e.  {
y  |  ph }  <->  [ x  /  y ]
ph )
df-cleq 2279 |-  ( A. x ( x  e.  y  <->  x  e.  z )  ->  y  =  z )   =>    |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
df-clel 2282 |-  ( A  e.  B  <->  E. x ( x  =  A  /\  x  e.  B ) )
wnfc 2409 wff  F/_ x A
df-nfc 2411 |-  ( F/_ x A  <->  A. y F/ x  y  e.  A )
wne 2449 wff 
A  =/=  B
wnel 2450 wff 
A  e/  B
df-ne 2451 |-  ( A  =/=  B  <->  -.  A  =  B )
df-nel 2452 |-  ( A  e/  B  <->  -.  A  e.  B )
wral 2546 wff  A. x  e.  A  ph
wrex 2547 wff 
E. x  e.  A  ph
wreu 2548 wff 
E! x  e.  A  ph
wrmo 2549 wff 
E* x  e.  A ph
crab 2550 class  { x  e.  A  |  ph }
df-ral 2551 |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
df-rex 2552 |-  ( E. x  e.  A  ph  <->  E. x
( x  e.  A  /\  ph ) )
df-reu 2553 |-  ( E! x  e.  A  ph  <->  E! x
( x  e.  A  /\  ph ) )
df-rmo 2554 |-  ( E* x  e.  A ph  <->  E* x
( x  e.  A  /\  ph ) )
df-rab 2555 |- 
{ x  e.  A  |  ph }  =  {
x  |  ( x  e.  A  /\  ph ) }
cvv 2791 class  _V
df-v 2793 |-  _V  =  { x  |  x  =  x }
wcdeq 2977 wff CondEq ( x  =  y  ->  ph )
df-cdeq 2978 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 2994 wff  [. A  /  x ]. ph
df-sbc 2995 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 3084 class  [_ A  /  x ]_ B
df-csb 3085 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 3152 class  ( A  \  B )
cun 3153 class  ( A  u.  B )
cin 3154 class  ( A  i^i  B )
wss 3155 wff 
A  C_  B
wpss 3156 wff 
A  C.  B
df-dif 3158 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 3160 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 3162 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 3169 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
df-pss 3171 |-  ( A  C.  B  <->  ( A  C_  B  /\  A  =/=  B ) )
c0 3458 class  (/)
df-nul 3459 |-  (/)  =  ( _V  \  _V )
cif 3568 class  if ( ph ,  A ,  B )
df-if 3569 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3628 class  ~P A
df-pw 3630 |-  ~P A  =  {
x  |  x  C_  A }
csn 3643 class  { A }
cpr 3644 class  { A ,  B }
ctp 3645 class  { A ,  B ,  C }
cop 3646 class  <. A ,  B >.
cotp 3647 class  <. A ,  B ,  C >.
df-sn 3649 |-  { A }  =  {
x  |  x  =  A }
df-pr 3650 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3651 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3652 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3653 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 3830 class  U. A
df-uni 3831 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 3865 class  |^| A
df-int 3866 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 3908 class  U_ x  e.  A  B
ciin 3909 class  |^|_
x  e.  A  B
df-iun 3910 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 3911 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 3996 wff Disj  x  e.  A B
df-disj 3997 |-  (Disj  x  e.  A B 
<-> 
A. y E* x  e.  A y  e.  B
)
wbr 4026 wff 
A R B
df-br 4027 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 4079 class  {
<. x ,  y >.  |  ph }
cmpt 4080 class  ( x  e.  A  |->  B )
df-opab 4081 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 4082 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 4116 wff 
Tr  A
df-tr 4117 |-  ( Tr  A  <->  U. A  C_  A )
ax-rep 4134 |-  ( 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 4144 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 4152 |- 
E. x A. y  -.  y  e.  x
ax-pow 4189 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
ax-pr 4215 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4304 class  _E
cid 4305 class  _I
df-eprel 4306 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4310 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4313 wff 
R  Po  A
wor 4314 wff 
R  Or  A
df-po 4315 |-  ( 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 4316 |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) ) )
wfr 4350 wff 
R  Fr  A
wse 4351 wff 
R Se  A
wwe 4352 wff 
R  We  A
df-fr 4353 |-  ( R  Fr  A  <->  A. x ( ( x 
C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
df-se 4354 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-we 4355 |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A )
)
word 4392 wff 
Ord  A
con0 4393 class  On
wlim 4394 wff 
Lim  A
csuc 4395 class  suc 
A
df-ord 4396 |-  ( Ord  A  <->  ( Tr  A  /\  _E  We  A
) )
df-on 4397 |-  On  =  { x  |  Ord  x }
df-lim 4398 |-  ( Lim  A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
df-suc 4399 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4513 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
com 4657 class  om
df-om 4658 |-  om  =  { x  e.  On  |  A. y
( Lim  y  ->  x  e.  y ) }
cxp 4688 class  ( A  X.  B )
ccnv 4689 class  `' A
cdm 4690 class  dom 
A
crn 4691 class  ran 
A
cres 4692 class  ( A  |`  B )
cima 4693 class  ( A " B )
ccom 4694 class  ( A  o.  B )
wrel 4695 wff 
Rel  A
df-xp 4696 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4697 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4698 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4699 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4700 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4701 |-  ran  A  =  dom  `'  A
df-res 4702 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4703 |-  ( A " B
)  =  ran  (  A  |`  B )
wfun 5217 wff 
Fun  A
wfn 5218 wff 
A  Fn  B
wf 5219 wff 
F : A --> B
wf1 5220 wff 
F : A -1-1-> B
wfo 5221 wff 
F : A -onto-> B
wf1o 5222 wff 
F : A -1-1-onto-> B
cfv 5223 class  ( F `  A )
wiso 5224 wff 
H  Isom  R ,  S  ( A ,  B )
df-fun 5225 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 5226 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 5227 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 5228 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 5229 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 5230 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 5231 |-  ( F `  A )  =  U. { x  |  ( F " { A } )  =  { x } }
df-isom 5232 |-  ( 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 5821 class  ( A F B )
coprab 5822 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpt2 5823 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 5824 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 5825 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpt2 5826 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 6039 class  o F R
cofr 6040 class  o R R
df-of 6041 |-  o F R  =  ( f  e.  _V , 
g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 6042 |-  o R R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 6083 class  1st
c2nd 6084 class  2nd
df-1st 6085 |- 
1st  =  ( x  e.  _V  |->  U. dom  {  x } )
df-2nd 6086 |- 
2nd  =  ( x  e.  _V  |->  U. ran  {  x } )
ctpos 6196 class tpos  F
df-tpos 6197 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
ccur 6235 class curry  A
cunc 6236 class uncurry  A
df-cur 6237 |- curry  F  =  ( x  e.  dom  dom  F  |->  {
<. y ,  z >.  |  <. x ,  y
>. F z } )
df-unc 6238 |- uncurry  F  =  { <. <. x ,  y >. ,  z
>.  |  y ( F `  x )
z }
crpss 6239 class [ C.]
df-rpss 6240 |- [
C.]  =  { <. x ,  y >.  |  x 
C.  y }
cio 6252 class  ( iota x ph )
df-iota 6254 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
cund 6291 class  Undef
crio 6292 class  (
iota_ x  e.  A ph )
df-undef 6293 |- 
Undef  =  ( s  e.  _V  |->  ~P U. s )
df-riota 6301 |-  ( iota_ x  e.  A ph )  =  if ( E! x  e.  A  ph ,  ( iota x
( x  e.  A  /\  ph ) ) ,  ( Undef `  { x  |  x  e.  A } ) )
wsmo 6359 wff 
Smo  A
df-smo 6360 |-  ( 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 6384 class recs ( F )
df-recs 6385 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 6419 class  rec ( F ,  I
)
df-rdg 6420 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  if ( g  =  (/) ,  I ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) ) )
cseqom 6456 class seq𝜔 ( F ,  I )
df-seqom 6457 |- seq𝜔 ( F ,  I )  =  ( rec (
( i  e.  om ,  v  e.  _V  |->  <. suc  i ,  ( i F v )
>. ) ,  <. (/) ,  (  _I  `  I )
>. ) " om )
c1o 6469 class  1o
c2o 6470 class  2o
c3o 6471 class  3o
c4o 6472 class  4o
coa 6473 class  +o
comu 6474 class  .o
coe 6475 class  ^o
df-1o 6476 |-  1o  =  suc  (/)
df-2o 6477 |-  2o  =  suc  1o
df-3o 6478 |-  3o  =  suc  2o
df-4o 6479 |-  4o  =  suc  3o
df-oadd 6480 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6481 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexp 6482 |- 
^o  =  ( x  e.  On ,  y  e.  On  |->  if ( x  =  (/) ,  ( 1o  \  y ) ,  ( rec (
( z  e.  _V  |->  ( z  .o  x
) ) ,  1o ) `  y )
) )
wer 6654 wff 
R  Er  A
cec 6655 class  [ A ] R
cqs 6656 class  ( A /. R )
df-er 6657 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6659 |-  [ A ] R  =  ( R " { A } )
df-qs 6663 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cmap 6769 class  ^m
cpm 6770 class  ^pm
df-map 6771 |- 
^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
df-pm 6772 |-  ^pm  =  ( x  e. 
_V ,  y  e. 
_V  |->  { f  e. 
~P ( y  X.  x )  |  Fun  f } )
cixp 6814 class  X_ x  e.  A  B
df-ixp 6815 |-  X_ x  e.  A  B  =  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
cen 6857 class  ~~
cdom 6858 class  ~<_
csdm 6859 class  ~<
cfn 6860 class  Fin
df-en 6861 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 6862 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-sdom 6863 |- 
~<  =  (  ~<_  \  ~~  )
df-fin 6864 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
cfi 7161 class  fi
df-fi 7162 |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
csup 7190 class  sup ( A ,  B ,  R )
df-sup 7191 |- 
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 7221 class OrdIso ( R ,  A )
df-oi 7222 |- 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 7267 class har
cwdom 7268 class  ~<_*
df-har 7269 |- har 
=  ( x  e. 
_V  |->  { y  e.  On  |  y  ~<_  x } )
df-wdom 7270 |-  ~<_*  =  { <. x ,  y
>.  |  ( x  =  (/)  \/  E. z 
z : y -onto-> x ) }
ax-reg 7303 |-  ( E. y  y  e.  x  ->  E. y
( y  e.  x  /\  A. z ( z  e.  y  ->  -.  z  e.  x )
) )
ax-inf 7336 |- 
E. y ( x  e.  y  /\  A. z ( z  e.  y  ->  E. w
( z  e.  w  /\  w  e.  y
) ) )
ax-inf2 7339 |- 
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 7359 class CNF
df-cnf 7360 |- 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 7418 class  TC
df-tc 7419 |-  TC  =  ( x  e.  _V  |->  |^| { y  |  ( x  C_  y  /\  Tr  y ) } )
cr1 7431 class  R1
crnk 7432 class  rank
df-r1 7433 |-  R1  =  rec (
( x  e.  _V  |->  ~P x ) ,  (/) )
df-rank 7434 |- 
rank  =  ( x  e.  _V  |->  |^| { y  e.  On  |  x  e.  ( R1 `  suc  y ) } )
ccrd 7565 class  card
cale 7566 class  aleph
ccf 7567 class  cf
wacn 7568 class AC  A
df-card 7569 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
df-aleph 7570 |-  aleph  =  rec (har ,  om )
df-cf 7571 |-  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 7572 |- 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 7739 wff CHOICE
df-ac 7740 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x ) )
ccda 7790 class  +c
df-cda 7791 |- 
+c  =  ( x  e.  _V ,  y  e.  _V  |->  ( ( x  X.  { (/) } )  u.  ( y  X.  { 1o }
) ) )
cfin1a 7901 class FinIa
cfin2 7902 class FinII
cfin4 7903 class FinIV
cfin3 7904 class FinIII
cfin5 7905 class FinV
cfin6 7906 class FinVI
cfin7 7907 class FinVII
df-fin1a 7908 |- FinIa  =  { x  |  A. y  e.  ~P  x
( y  e.  Fin  \/  ( x  \  y
)  e.  Fin ) }
df-fin2 7909 |- FinII  =  { x  |  A. y  e.  ~P  ~P x
( ( y  =/=  (/)  /\ [ C.]  Or  y
)  ->  U. y  e.  y ) }
df-fin4 7910 |- FinIV  =  { x  |  -.  E. y ( y  C.  x  /\  y  ~~  x
) }
df-fin3 7911 |- FinIII  =  { x  |  ~P x  e. FinIV }
df-fin5 7912 |- FinV  =  { x  |  ( x  =  (/)  \/  x  ~<  ( x  +c  x
) ) }
df-fin6 7913 |- FinVI  =  { x  |  ( x  ~<  2o  \/  x  ~<  ( x  X.  x ) ) }
df-fin7 7914 |- FinVII  =  { x  |  -.  E. y  e.  ( On 
\  om ) x 
~~  y }
ax-cc 8058 |-  ( x  ~~  om  ->  E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
ax-dc 8069 |-  ( ( 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 8082 |-  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 8086 |- 
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 8239 class GCH
df-gch 8240 |- GCH 
=  ( Fin  u.  { x  |  A. y  -.  ( x  ~<  y  /\  y  ~<  ~P x
) } )
cwina 8301 class  Inacc W
cina 8302 class  Inacc
df-wina 8303 |- 
Inacc W  =  {
x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z
) }
df-ina 8304 |- 
Inacc  =  { x  |  ( x  =/=  (/)  /\  ( cf `  x
)  =  x  /\  A. y  e.  x  ~P y  ~<  x ) }
cwun 8319 class WUni
cwunm 8320 class wUniCl
df-wun 8321 |- 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 8322 |- wUniCl  =  ( x  e. 
_V  |->  |^| { u  e. WUni  |  x  C_  u }
)
ctsk 8367 class  Tarski
df-tsk 8368 |- 
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 8409 class  Univ
df-gru 8410 |- 
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 8442 |- 
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 8456 class  tarskiMap
df-tskm 8457 |-  tarskiMap 
=  ( x  e. 
_V  |->  |^| { y  e. 
Tarski  |  x  e.  y } )
cnpi 8463 class  N.
cpli 8464 class  +N
cmi 8465 class  .N
clti 8466 class  <N
cplpq 8467 class  +pQ
cmpq 8468 class  .pQ
cltpq 8469 class  <pQ
ceq 8470 class  ~Q
cnq 8471 class  Q.
c1q 8472 class  1Q
cerq 8473 class  /Q
cplq 8474 class  +Q
cmq 8475 class  .Q
crq 8476 class  *Q
cltq 8477 class  <Q
cnp 8478 class  P.
c1p 8479 class  1P
cpp 8480 class  +P.
cmp 8481 class  .P.
cltp 8482 class  <P
cplpr 8483 class  +pR
cmpr 8484 class  .pR
cer 8485 class  ~R
cnr 8486 class  R.
c0r 8487 class  0R
c1r 8488 class  1R
cm1r 8489 class  -1R
cplr 8490 class  +R
cmr 8491 class  .R
cltr 8492 class  <R
df-ni 8493 |-  N.  =  ( om  \  { (/) } )
df-pli 8494 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 8495 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 8496 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 8529 |- 
+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 8530 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 8531 |- 
<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 8532 |- 
~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 8533 |-  Q.  =  { x  e.  ( N.  X.  N. )  |  A. y  e.  ( N.  X.  N. ) ( x  ~Q  y  ->  -.  ( 2nd `  y )  <N  ( 2nd `  x ) ) }
df-erq 8534 |- 
/Q  =  (  ~Q  i^i  ( ( N.  X.  N. )  X.  Q. )
)
df-plq 8535 |- 
+Q  =  ( ( /Q  o.  +pQ  )  |`  ( Q.  X.  Q. ) )
df-mq 8536 |-  .Q  =  ( ( /Q  o.  .pQ  )  |`  ( Q.  X.  Q. ) )
df-1nq 8537 |-  1Q  =  <. 1o ,  1o >.
df-rq 8538 |-  *Q  =  ( `'  .Q  " { 1Q } )
df-ltnq 8539 |- 
<Q  =  (  <pQ  i^i  ( Q.  X.  Q. ) )
df-np 8602 |-  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 8603 |-  1P  =  { x  |  x  <Q  1Q }
df-plp 8604 |- 
+P.  =  ( x  e.  P. ,  y  e.  P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  +Q  u ) } )
df-mp 8605 |-  .P.  =  ( x  e. 
P. ,  y  e. 
P.  |->  { w  |  E. v  e.  x  E. u  e.  y  w  =  ( v  .Q  u ) } )
df-ltp 8606 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  x  C.  y ) }
df-plpr 8676 |- 
+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 8677 |- 
.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 8678 |- 
~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 8679 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 8680 |- 
+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 8681 |-  .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 8682 |- 
<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 8683 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 8684 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 8685 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 8732 class  CC
cr 8733 class  RR
cc0 8734 class  0
c1 8735 class  1
ci 8736 class  _i
caddc 8737 class  +
cltrr 8738 class  <RR
cmul 8739 class  x.
df-c 8740 |-  CC  =  ( R.  X.  R. )
df-0 8741 |-  0  =  <. 0R ,  0R >.
df-1 8742 |-  1  =  <. 1R ,  0R >.
df-i 8743 |-  _i  =  <. 0R ,  1R >.
df-r 8744 |-  RR  =  ( R.  X.  { 0R } )
df-add 8745 |-  +  =  { <. <.
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 8746 |-  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 8747 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 8790 |-  CC  e.  _V
ax-resscn 8791 |-  RR  C_  CC
ax-1cn 8792 |-  1  e.  CC
ax-icn 8793 |-  _i  e.  CC
ax-addcl 8794 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 8795 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 8796 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 8797 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-mulcom 8798 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 8799 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 8800 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 8801 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 8802 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-1ne0 8803 |-  1  =/=  0
ax-1rid 8804 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-rnegex 8805 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-rrecex 8806 |-  ( ( A  e.  RR  /\  A  =/=  0 )  ->  E. x  e.  RR  ( A  x.  x )  =  1 )
ax-cnre 8807 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-lttri 8808 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <RR  B  <->  -.  ( A  =  B  \/  B  <RR  A ) ) )
ax-pre-lttrn 8809 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-ltadd 8810 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 8811 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-sup 8812 |-  ( ( 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 8813 |-  +  : ( CC 
X.  CC ) --> CC
ax-mulf 8814 |-  x.  : ( CC 
X.  CC ) --> CC
cpnf 8861 class  +oo
cmnf 8862 class  -oo
cxr 8863 class  RR*
clt 8864 class  <
cle 8865 class  <_
df-pnf 8866 |- 
+oo  =  ~P U. CC
df-mnf 8867 |- 
-oo  =  ~P  +oo
df-xr 8868 |-  RR*  =  ( RR  u.  { 
+oo ,  -oo } )
df-ltxr 8869 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { 
-oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) ) )
df-le 8870 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 9034 class  -
cneg 9035 class  -u A
df-sub 9036 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC ( y  +  z )  =  x ) )
df-neg 9037 |-  -u A  =  (
0  -  A )
cdiv 9420 class  /
df-div 9421 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC ( y  x.  z
)  =  x ) )
cn 9743 class  NN
df-nn 9744 |-  NN  =  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )
c2 9792 class  2
c3 9793 class  3
c4 9794 class  4
c5 9795 class  5
c6 9796 class  6
c7 9797 class  7
c8 9798 class  8
c9 9799 class  9
c10 9800 class  10
df-2 9801 |-  2  =  ( 1  +  1 )
df-3 9802 |-  3  =  ( 2  +  1 )
df-4 9803 |-  4  =  ( 3  +  1 )
df-5 9804 |-  5  =  ( 4  +  1 )
df-6 9805 |-  6  =  ( 5  +  1 )
df-7 9806 |-  7  =  ( 6  +  1 )
df-8 9807 |-  8  =  ( 7  +  1 )
df-9 9808 |-  9  =  ( 8  +  1 )
df-10 9809 |-  10  =  ( 9  +  1 )
cn0 9962 class  NN0
df-n0 9963 |-  NN0  =  ( NN  u.  { 0 } )
cz 10021 class  ZZ
df-z 10022 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 10121 class ; A B
df-dec 10122 |- ; A B  =  ( ( 10  x.  A )  +  B )
cuz 10227 class  ZZ>=
df-uz 10228 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 10313 class  QQ
df-q 10314 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 10351 class  RR+
df-rp 10352 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 10446 class  - e A
cxad 10447 class  + e
cxmu 10448 class  x e
df-xneg 10449 |-  - e A  =  if ( A  =  +oo , 
-oo ,  if ( A  =  -oo ,  +oo , 
-u A ) )
df-xadd 10450 |-  + 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 10451 |-  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 10652 class  (,)
cioc 10653 class  (,]
cico 10654 class  [,)
cicc 10655 class  [,]
df-ioo 10656 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 10657 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 10658 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 10659 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 10778 class  ...
df-fz 10779 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 10866 class ..^
df-fzo 10867 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 10920 class  |_
df-fl 10921 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
cmo 10969 class  mod
df-mod 10970 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 11042 class  seq 
M (  .+  ,  F )
df-seq 11043 |- 
seq  M (  .+  ,  F )  =  ( rec ( ( x  e.  _V ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. ) " om )
cexp 11100 class  ^
df-exp 11101 |- 
^  =  ( 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 11284 class  !
df-fac 11285 |-  !  =  ( {
<. 0 ,  1
>. }  u.  seq  1
(  x.  ,  _I  ) )
cbc 11311 class  _C
df-bc 11312 |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n
)  /  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) ) ) ,  0 ) )
chash 11333 class  #
df-hash 11334 |-  #  =  ( (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om )  o.  card )  u.  ( ( _V  \  Fin )  X. 
{  +oo } ) )
cword 11399 class Word  S
cconcat 11400 class concat
cs1 11401 class  <" A ">
csubstr 11402 class substr
csplice 11403 class splice
creverse 11404 class reverse
df-word 11405 |- Word  S  =  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
df-concat 11406 |- concat  =  ( s  e. 
_V ,  t  e. 
_V  |->  ( x  e.  ( 0..^ ( (
# `  s )  +  ( # `  t
) ) )  |->  if ( x  e.  ( 0..^ ( # `  s
) ) ,  ( s `  x ) ,  ( t `  ( x  -  ( # `
 s ) ) ) ) ) )
df-s1 11407 |-  <" A ">  =  { <. 0 ,  (  _I  `  A )
>. }
df-substr 11408 |- 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 11409 |- 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 11410 |- reverse  =  ( s  e. 
_V  |->  ( x  e.  ( 0..^ ( # `  s ) )  |->  ( s `  ( ( ( # `  s
)  -  1 )  -  x ) ) ) )
cs2 11487 class  <" A B ">
cs3 11488 class  <" A B C ">
cs4 11489 class  <" A B C D ">
cs5 11490 class  <" A B C D E ">
cs6 11491 class  <" A B C D E F ">
cs7 11492 class  <" A B C D E F G ">
cs8 11493 class  <" A B C D E F G H ">
df-s2 11494 |-  <" A B ">  =  ( <" A "> concat  <" B "> )
df-s3 11495 |-  <" A B C ">  =  (
<" A B "> concat 
<" C "> )
df-s4 11496 |-  <" A B C D ">  =  ( <" A B C "> concat  <" D "> )
df-s5 11497 |-  <" A B C D E ">  =  ( <" A B C D "> concat  <" E "> )
df-s6 11498 |-  <" A B C D E F ">  =  ( <" A B C D E "> concat 
<" F "> )
df-s7 11499 |-  <" A B C D E F G ">  =  (
<" A B C D E F "> concat 
<" G "> )
df-s8 11500 |-  <" A B C D E F G H ">  =  ( <" A B C D E F G "> concat  <" H "> )
cshi 11557 class  shift
df-shft 11558 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 11577 class  *
cre 11578 class  Re
cim 11579 class  Im
df-cj 11580 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 11581 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 11582 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqr 11714 class  sqr
cabs 11715 class  abs
df-sqr 11716 |- 
sqr  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
df-abs 11717 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
clsp 11940 class  limsup
df-limsup 11941 |- 
limsup  =  ( x  e. 
_V  |->  sup ( ran  ( 
k  e.  RR  |->  sup ( ( ( x
" ( k [,) 
+oo ) )  i^i  RR* ) ,  RR* ,  <  ) ) ,  RR* ,  `'  <  ) )
cli 11954 class  ~~>
crli 11955 class  ~~> r
co1 11956 class  O ( 1 )
clo1 11957 class  <_
O ( 1 )
df-clim 11958 |-  ~~>  =  { <. 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 11959 |-  ~~> 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 11960 |-  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 11961 |- 
<_ 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 12154 class  sum_ k  e.  A  B
df-sum 12155 |- 
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 12339 class  exp
ceu 12340 class  _e
csin 12341 class  sin
ccos 12342 class  cos
ctan 12343 class  tan
cpi 12344 class  pi
df-ef 12345 |-  exp  =  ( x  e.  CC  |->  sum_ k  e.  NN0  ( ( x ^
k )  /  ( ! `  k )
) )
df-e 12346 |-  _e  =  ( exp `  1 )
df-sin 12347 |- 
sin  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  -  ( exp `  ( -u _i  x.  x ) ) )  /  ( 2  x.  _i ) ) )
df-cos 12348 |- 
cos  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  +  ( exp `  ( -u _i  x.  x ) ) )  /  2 ) )
df-tan 12349 |- 
tan  =  ( x  e.  ( `' cos " ( CC  \  {
0 } ) ) 
|->  ( ( sin `  x
)  /  ( cos `  x ) ) )
df-pi 12350 |-  pi  =  sup (
( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  `'  <  )
cdivides 12527 class  ||
df-dvds 12528 |- 
||  =  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
cbits 12606 class bits
csad 12607 class sadd
csmu 12608 class smul
df-bits 12609 |- bits 
=  ( n  e.  ZZ  |->  { m  e. 
NN0  |  -.  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) ) } )
df-sad 12638 |- 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 12663 |- 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 12681 class  gcd
df-gcd 12682 |- 
gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
cprime 12754 class  Prime
df-prm 12755 |- 
Prime  =  { p  e.  NN  |  { n  e.  NN  |  n  ||  p }  ~~  2o }
cnumer 12800 class numer
cdenom 12801 class denom
df-numer 12802 |- numer  =  ( y  e.  QQ  |->  ( 1st `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
df-denom 12803 |- denom  =  ( y  e.  QQ  |->  ( 2nd `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
codz 12827 class  od
Z
cphi 12828 class  phi
df-odz 12829 |-  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 12830 |- 
phi  =  ( n  e.  NN  |->  ( # `  { x  e.  ( 1 ... n )  |  ( x  gcd  n )  =  1 } ) )
cpc 12885 class  pCnt
df-pc 12886 |-  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 12972 class  ZZ [ _i ]
df-gz 12973 |-  ZZ [ _i ]  =  { x  e.  CC  |  ( ( Re
`  x )  e.  ZZ  /\  ( Im
`  x )  e.  ZZ ) }
cvdwa 13008 class AP
cvdwm 13009 class MonoAP
cvdwp 13010 class PolyAP
df-vdwap 13011 |- AP 
=  ( k  e. 
NN0  |->  ( a  e.  NN ,  d  e.  NN  |->  ran  (  m  e.  ( 0 ... (
k  -  1 ) )  |->  ( a  +  ( m  x.  d
) ) ) ) )
df-vdwmc 13012 |- MonoAP  =  { <. k ,  f
>.  |  E. c
( ran  (AP `  k
)  i^i  ~P ( `' f " {
c } ) )  =/=  (/) }
df-vdwpc 13013 |- 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 13042 class Ramsey
df-ram 13044 |- 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 13140 class Struct
cnx 13141 class  ndx
csts 13142 class sSet
cslot 13143 class Slot  A
cbs 13144 class  Base
cress 13145 classs
df-struct 13146 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( f 
\  { (/) } )  /\  dom  f  C_  ( ... `  x ) ) }
df-ndx 13147 |- 
ndx  =  (  _I  |`  NN )
df-slot 13148 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
df-base 13149 |- 
Base  = Slot  1
df-sets 13150 |- sSet 
=  ( s  e. 
_V ,  e  e. 
_V  |->  ( ( s  |`  ( _V  \  dom  {  e } ) )  u.  { e } ) )
df-ress 13151 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  if ( ( Base `  w
)  C_  x ,  w ,  ( w sSet  <.
( Base `  ndx ) ,  ( x  i^i  ( Base `  w ) )
>. ) ) )
cplusg 13204 class  +g
cmulr 13205 class  .r
cstv 13206 class  * r
csca 13207 class Scalar
cvsca 13208 class  .s
cip 13209 class  .i
cts 13210 class TopSet
cple 13211 class  le
coc 13212 class  oc
cds 13213 class  dist
cunif 13214 class  Unif
chom 13215 class  Hom
cco 13216 class comp
df-plusg 13217 |- 
+g  = Slot  2
df-mulr 13218 |- 
.r  = Slot  3
df-starv 13219 |-  * r  = Slot  4
df-sca 13220 |- Scalar  = Slot  5
df-vsca 13221 |-  .s  = Slot  6
df-ip 13222 |-  .i  = Slot  8
df-tset 13223 |- TopSet  = Slot  9
df-ple 13224 |- 
le  = Slot  10
df-ocomp 13225 |-  oc  = Slot ; 1 1
df-ds 13226 |-  dist 
= Slot ; 1 2
df-unif 13227 |- 
Unif  = Slot ; 1 3
df-hom 13228 |- 
Hom  = Slot ; 1 4
df-cco 13229 |- comp 
= Slot ; 1 5
crest 13321 classt
ctopn 13322 class  TopOpen
df-rest 13323 |-t  =  ( j  e.  _V ,  x  e.  _V  |->  ran  (  y  e.  j  |->  ( y  i^i  x ) ) )
df-topn 13324 |-  TopOpen  =  ( w  e. 
_V  |->  ( (TopSet `  w )t  ( Base `  w
) ) )
ctg 13338 class  topGen
cpt 13339 class  Xt_
df-topgen 13340 |- 
topGen  =  ( x  e. 
_V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
df-pt 13341 |-  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 13342 class  X_s
cpws 13343 class  ^s
df-prds 13344 |-  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 13346 |- 
^s  =  ( r  e. 
_V ,  i  e. 
_V  |->  ( (Scalar `  r ) X_s ( i  X.  {
r } ) ) )
cordt 13394 class ordTop
cxrs 13395 class  RR* s
c0g 13396 class  0g
cgsu 13397 class  gsumg
df-ordt 13398 |- 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 13399 |- 
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 13400 |-  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 13401 |- 
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 13402 class qTop
cimas 13403 class  "s
cqus 13404 class  /.s
cxps 13405 class  X.s
df-qtop 13406 |- qTop 
=  ( j  e. 
_V ,  f  e. 
_V  |->  { s  e. 
~P ( f " U. j )  |  ( ( `' f "
s )  i^i  U. j )  e.  j } )
df-imas 13407 |-  "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 13408 |- 
/.s 
=  ( r  e. 
_V ,  e  e. 
_V  |->  ( ( x  e.  ( Base `  r
)  |->  [ x ]
e )  "s  r )
)
df-xps 13409 |- 
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 13480 class Moore
cmrc 13481 class mrCls
cmri 13482 class mrInd
cacs 13483 class ACS
df-mre 13484 |- Moore  =  ( x  e. 
_V  |->  { c  e. 
~P ~P x  |  ( x  e.  c  /\  A. s  e. 
~P  c ( s  =/=  (/)  ->  |^| s  e.  c ) ) } )
df-mrc 13485 |- mrCls  =  ( c  e. 
U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^|
{ s  e.  c  |  x  C_  s } ) )
df-mri 13486 |- mrInd  =  ( c  e. 
U. ran Moore  |->  { s  e.  ~P U. c  | 
A. x  e.  s  -.  x  e.  ( (mrCls `  c ) `  ( s  \  {
x } ) ) } )
df-acs 13487 |- 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 13562 class  Cat
ccid 13563 class  Id
chomf 13564 class  Homf
ccomf 13565 class compf
df-cat 13566 |- 
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 13567 |-  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 13568 |- 
Homf 
=  ( c  e. 
_V  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( x (  Hom  `  c )
y ) ) )
df-comf 13569 |- 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 13610 class oppCat
df-oppc 13611 |- 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 13627 class Mono
cepi 13628 class Epi
df-mon 13629 |- 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 13630 |- Epi 
=  ( c  e. 
Cat  |-> tpos  (Mono `  (oppCat `  c
) ) )
csect 13643 class Sect
cinv 13644 class Inv
ciso 13645 class  Iso
df-sect 13646 |- 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 13647 |- Inv 
=  ( c  e. 
Cat  |->  ( x  e.  ( Base `  c
) ,  y  e.  ( Base `  c
)  |->  ( ( x (Sect `  c )
y )  i^i  `' ( y (Sect `  c ) x ) ) ) )
df-iso 13648 |- 
Iso  =  ( c  e.  Cat  |->  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) ) )
cssc 13680 class  C_cat
cresc 13681 class  |`cat
csubc 13682 class Subcat
df-ssc 13683 |-  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 13684 |-  |`cat 
=  ( c  e. 
_V ,  h  e. 
_V  |->  ( ( cs  dom 
dom  h ) sSet  <. (  Hom  `  ndx ) ,  h >. ) )
df-subc 13685 |- 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 13724 class  Func
cidfu 13725 class idfunc
ccofu 13726 class  o.func
cresf 13727 class  |`f
df-func 13728 |- 
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 13729 |- idfunc  =  ( t  e.  Cat  |->  [_ ( Base `  t
)  /  b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
df-cofu 13730 |-  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 13731 |-  |`f  =  ( f  e. 
_V ,  h  e. 
_V  |->  <. ( ( 1st `  f )  |`  dom  dom  h ) ,  ( x  e.  dom  h  |->  ( ( ( 2nd `  f ) `  x
)  |`  ( h `  x ) ) )
>. )
cful 13772 class Full
cfth 13773 class Faith
df-full 13774 |- 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 13775 |- 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 13811 class Nat
cfuc 13812 class FuncCat
df-nat 13813 |- 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 13814 |- 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 13848 class domA
ccoda 13849 class coda
carw 13850 class Nat
choma 13851 class Homa
df-doma 13852 |- domA  =  ( 1st  o.  1st )
df-coda 13853 |- coda  =  ( 2nd  o.  1st )
df-homa 13854 |- Homa  =  ( c  e.  Cat  |->  ( x  e.  (
( Base `  c )  X.  ( Base `  c
) )  |->  ( { x }  X.  (
(  Hom  `  c ) `
 x ) ) ) )
df-arw 13855 |- Nat 
=  ( c  e. 
Cat  |->  U. ran  (Homa `  c
) )
cida 13881 class Ida
ccoa 13882 class compa
df-ida 13883 |- Ida  =  ( c  e.  Cat  |->  ( x  e.  ( Base `  c )  |->  <.
x ,  x ,  ( ( Id `  c ) `  x
) >. ) )
df-coa 13884 |- 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 13903 class  SetCat
df-setc 13904 |- 
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 13922 class CatCat
df-catc 13923 |- 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 13938 class  X.c
c1stf 13939 class  1stF
c2ndf 13940 class  2ndF
cprf 13941 class ⟨,⟩F
df-xpc 13942 |- 
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 13943 |- 
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 13944 |- 
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 13945 |- ⟨,⟩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 13979 class evalF
ccurf 13980 class curryF
cuncf 13981 class uncurryF
cdiag 13982 class Δfunc
df-evlf 13983 |- 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 13984 |- 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 13985 |- 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 13986 |- Δfunc  =  ( c  e.  Cat ,  d  e.  Cat  |->  (
<. c ,  d >. curryF  ( c  1stF  d ) ) )
chof 14018 class HomF
cyon 14019 class Yon
df-hof 14020 |- 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 14021 |- Yon 
=  ( c  e. 
Cat  |->  ( <. c ,  (oppCat `  c ) >. curryF  (HomF `  (oppCat `  c ) ) ) )
cpreset 14056 class  Preset
cdrs 14057 class Dirset
df-preset 14058 |- 
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 ) )