ILE Home Intuitionistic Logic 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-mp 5 |- 
ph   &    |-  ( ph  ->  ps )   =>    |- 
ps
ax-1 6 |-  ( ph  ->  ( ps  ->  ph ) )
ax-2 7 |-  ( ( ph  ->  ( ps  ->  ch )
)  ->  ( ( ph  ->  ps )  -> 
( ph  ->  ch )
) )
wa 103 wff  ( ph  /\  ps )
wb 104 wff  ( ph  <->  ps )
ax-ia1 105 |-  ( ( ph  /\  ps )  ->  ph )
ax-ia2 106 |-  ( ( ph  /\  ps )  ->  ps )
ax-ia3 107 |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
df-bi 116 |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )  /\  (
( ( ph  ->  ps )  /\  ( ps 
->  ph ) )  -> 
( ph  <->  ps ) ) )
ax-in1 588 |-  ( ( ph  ->  -. 
ph )  ->  -.  ph )
ax-in2 589 |-  ( -.  ph  ->  (
ph  ->  ps ) )
wo 682 wff  ( ph  \/  ps )
ax-io 683 |-  ( ( ( ph  \/  ch )  ->  ps ) 
<->  ( ( ph  ->  ps )  /\  ( ch 
->  ps ) ) )
wstab 800 wff STAB  ph
df-stab 801 |-  (STAB 
ph 
<->  ( -.  -.  ph  ->  ph ) )
wdc 804 wff DECID  ph
df-dc 805 |-  (DECID 
ph 
<->  ( ph  \/  -.  ph ) )
w3o 946 wff  ( ph  \/  ps  \/  ch )
w3a 947 wff  ( ph  /\  ps  /\ 
ch )
df-3or 948 |-  ( ( ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/ 
ch ) )
df-3an 949 |-  ( ( ph  /\  ps  /\  ch )  <->  ( ( ph  /\  ps )  /\  ch ) )
wal 1314 wff  A. x ph
cv 1315 class  x
wceq 1316 wff 
A  =  B
wtru 1317 wff T.
df-tru 1319 |-  ( T.  <->  ( A. x  x  =  x  ->  A. x  x  =  x ) )
wfal 1321 wff F.
df-fal 1322 |-  ( F.  <->  -. T.  )
wxo 1338 wff  ( ph  \/_  ps )
df-xor 1339 |-  ( ( ph  \/_  ps ) 
<->  ( ( ph  \/  ps )  /\  -.  ( ph  /\  ps ) ) )
ax-5 1408 |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
ax-7 1409 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-gen 1410 |- 
ph   =>    |- 
A. x ph
wnf 1421 wff 
F/ x ph
df-nf 1422 |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
wex 1453 wff 
E. x ph
ax-ie1 1454 |-  ( E. x ph  ->  A. x E. x ph )
ax-ie2 1455 |-  ( A. x ( ps  ->  A. x ps )  ->  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) ) )
wcel 1465 wff 
A  e.  B
ax-8 1467 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-10 1468 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11 1469 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-i12 1470 |-  ( A. z  z  =  x  \/  ( A. z  z  =  y  \/  A. z
( x  =  y  ->  A. z  x  =  y ) ) )
ax-bndl 1471 |-  ( A. z  z  =  x  \/  ( A. z  z  =  y  \/  A. x A. z ( x  =  y  ->  A. z  x  =  y )
) )
ax-4 1472 |-  ( A. x ph  ->  ph )
ax-13 1476 |-  ( x  =  y  ->  ( x  e.  z  ->  y  e.  z ) )
ax-14 1477 |-  ( x  =  y  ->  ( z  e.  x  ->  z  e.  y ) )
ax-17 1491 |-  ( ph  ->  A. x ph )
ax-i9 1495 |-  E. x  x  =  y
ax-ial 1499 |-  ( A. x ph  ->  A. x A. x ph )
ax-i5r 1500 |-  ( ( A. x ph  ->  A. x ps )  ->  A. x ( A. x ph  ->  ps )
)
ax-10o 1679 |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph ) )
wsb 1720 wff 
[ y  /  x ] ph
df-sb 1721 |-  ( [ y  /  x ] ph  <->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph ) ) )
ax-16 1770 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
ax-11o 1779 |-  ( -.  A. x  x  =  y  ->  ( x  =  y  -> 
( ph  ->  A. x
( x  =  y  ->  ph ) ) ) )
weu 1977 wff 
E! x ph
wmo 1978 wff 
E* x ph
df-eu 1980 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
df-mo 1981 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
ax-ext 2099 |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
cab 2103 class  { x  |  ph }
df-clab 2104 |-  ( x  e.  {
y  |  ph }  <->  [ x  /  y ]
ph )
df-cleq 2110 |-  ( A. x ( x  e.  y  <->  x  e.  z )  ->  y  =  z )   =>    |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
df-clel 2113 |-  ( A  e.  B  <->  E. x ( x  =  A  /\  x  e.  B ) )
wnfc 2245 wff  F/_ x A
df-nfc 2247 |-  ( F/_ x A  <->  A. y F/ x  y  e.  A )
wne 2285 wff 
A  =/=  B
df-ne 2286 |-  ( A  =/=  B  <->  -.  A  =  B )
wnel 2380 wff 
A  e/  B
df-nel 2381 |-  ( A  e/  B  <->  -.  A  e.  B )
wral 2393 wff  A. x  e.  A  ph
wrex 2394 wff 
E. x  e.  A  ph
wreu 2395 wff 
E! x  e.  A  ph
wrmo 2396 wff 
E* x  e.  A  ph
crab 2397 class  { x  e.  A  |  ph }
df-ral 2398 |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
df-rex 2399 |-  ( E. x  e.  A  ph  <->  E. x
( x  e.  A  /\  ph ) )
df-reu 2400 |-  ( E! x  e.  A  ph  <->  E! x
( x  e.  A  /\  ph ) )
df-rmo 2401 |-  ( E* x  e.  A  ph  <->  E* x
( x  e.  A  /\  ph ) )
df-rab 2402 |- 
{ x  e.  A  |  ph }  =  {
x  |  ( x  e.  A  /\  ph ) }
cvv 2660 class  _V
df-v 2662 |-  _V  =  { x  |  x  =  x }
wcdeq 2865 wff CondEq ( x  =  y  ->  ph )
df-cdeq 2866 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 2882 wff  [. A  /  x ]. ph
df-sbc 2883 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 2975 class  [_ A  /  x ]_ B
df-csb 2976 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 3038 class  ( A  \  B )
cun 3039 class  ( A  u.  B )
cin 3040 class  ( A  i^i  B )
wss 3041 wff 
A  C_  B
df-dif 3043 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 3045 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 3047 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 3054 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
c0 3333 class  (/)
df-nul 3334 |-  (/)  =  ( _V  \  _V )
cif 3444 class  if ( ph ,  A ,  B )
df-if 3445 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3480 class  ~P A
df-pw 3482 |-  ~P A  =  {
x  |  x  C_  A }
csn 3497 class  { A }
cpr 3498 class  { A ,  B }
ctp 3499 class  { A ,  B ,  C }
cop 3500 class  <. A ,  B >.
cotp 3501 class  <. A ,  B ,  C >.
df-sn 3503 |-  { A }  =  {
x  |  x  =  A }
df-pr 3504 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3505 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3506 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3507 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 3706 class  U. A
df-uni 3707 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 3741 class  |^| A
df-int 3742 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 3783 class  U_ x  e.  A  B
ciin 3784 class  |^|_
x  e.  A  B
df-iun 3785 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 3786 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 3876 wff Disj  x  e.  A  B
df-disj 3877 |-  (Disj  x  e.  A  B 
<-> 
A. y E* x  e.  A  y  e.  B )
wbr 3899 wff 
A R B
df-br 3900 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 3958 class  {
<. x ,  y >.  |  ph }
cmpt 3959 class  ( x  e.  A  |->  B )
df-opab 3960 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 3961 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 3996 wff 
Tr  A
df-tr 3997 |-  ( Tr  A  <->  U. A  C_  A )
ax-coll 4013 |-  F/ b ph   =>    |-  ( A. x  e.  a  E. y ph  ->  E. b A. x  e.  a  E. y  e.  b  ph )
ax-sep 4016 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 4024 |- 
E. x A. y  -.  y  e.  x
ax-pow 4068 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
wem 4088 wff EXMID
df-exmid 4089 |-  (EXMID  <->  A. x ( x  C_  {
(/) }  -> DECID  (/)  e.  x ) )
ax-pr 4101 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4179 class  _E
cid 4180 class  _I
df-eprel 4181 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4185 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4186 wff 
R  Po  A
wor 4187 wff 
R  Or  A
df-po 4188 |-  ( 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-iso 4189 |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  (
x R y  -> 
( x R z  \/  z R y ) ) ) )
wfrfor 4219 wff FrFor  R A S
wfr 4220 wff 
R  Fr  A
wse 4221 wff 
R Se  A
wwe 4222 wff 
R  We  A
df-frfor 4223 |-  (FrFor  R A S  <-> 
( A. x  e.  A  ( A. y  e.  A  ( y R x  ->  y  e.  S )  ->  x  e.  S )  ->  A  C_  S ) )
df-frind 4224 |-  ( R  Fr  A  <->  A. sFrFor  R A s )
df-se 4225 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-wetr 4226 |-  ( R  We  A  <->  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  (
( x R y  /\  y R z )  ->  x R
z ) ) )
word 4254 wff 
Ord  A
con0 4255 class  On
wlim 4256 wff 
Lim  A
csuc 4257 class  suc 
A
df-iord 4258 |-  ( Ord  A  <->  ( Tr  A  /\  A. x  e.  A  Tr  x ) )
df-on 4260 |-  On  =  { x  |  Ord  x }
df-ilim 4261 |-  ( Lim  A  <->  ( Ord  A  /\  (/)  e.  A  /\  A  =  U. A ) )
df-suc 4263 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4325 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
ax-setind 4422 |-  ( A. a ( A. y  e.  a  [ y  /  a ] ph  ->  ph )  ->  A. a ph )
ax-iinf 4472 |- 
E. x ( (/)  e.  x  /\  A. y
( y  e.  x  ->  suc  y  e.  x
) )
com 4474 class  om
df-iom 4475 |- 
om  =  |^| { x  |  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
) }
cxp 4507 class  ( A  X.  B )
ccnv 4508 class  `' A
cdm 4509 class  dom 
A
crn 4510 class  ran 
A
cres 4511 class  ( A  |`  B )
cima 4512 class  ( A " B )
ccom 4513 class  ( A  o.  B )
wrel 4514 wff 
Rel  A
df-xp 4515 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4516 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4517 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4518 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4519 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4520 |-  ran  A  =  dom  `' A
df-res 4521 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4522 |-  ( A " B
)  =  ran  ( A  |`  B )
cio 5056 class  ( iota x ph )
df-iota 5058 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
wfun 5087 wff 
Fun  A
wfn 5088 wff 
A  Fn  B
wf 5089 wff 
F : A --> B
wf1 5090 wff 
F : A -1-1-> B
wfo 5091 wff 
F : A -onto-> B
wf1o 5092 wff 
F : A -1-1-onto-> B
cfv 5093 class  ( F `  A )
wiso 5094 wff 
H  Isom  R ,  S  ( A ,  B )
df-fun 5095 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 5096 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 5097 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 5098 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 5099 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 5100 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 5101 |-  ( F `  A )  =  ( iota x A F x )
df-isom 5102 |-  ( 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 ) ) ) )
crio 5697 class  (
iota_ x  e.  A  ph )
df-riota 5698 |-  ( iota_ x  e.  A  ph )  =  ( iota
x ( x  e.  A  /\  ph )
)
co 5742 class  ( A F B )
coprab 5743 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpo 5744 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 5745 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 5746 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpo 5747 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 5948 class  oF R
cofr 5949 class  oR R
df-of 5950 |-  oF R  =  ( f  e.  _V ,  g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 5951 |-  oR R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 6004 class  1st
c2nd 6005 class  2nd
df-1st 6006 |- 
1st  =  ( x  e.  _V  |->  U. dom  { x } )
df-2nd 6007 |- 
2nd  =  ( x  e.  _V  |->  U. ran  { x } )
ctpos 6109 class tpos  F
df-tpos 6110 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
wsmo 6150 wff 
Smo  A
df-smo 6151 |-  ( 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 6169 class recs ( F )
df-recs 6170 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 6234 class  rec ( F ,  I
)
df-irdg 6235 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  ( I  u.  U_ x  e.  dom  g ( F `
 ( g `  x ) ) ) ) )
cfrec 6255 class frec ( F ,  I )
df-frec 6256 |- frec
( F ,  I
)  =  (recs ( ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `
 m ) ) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) ) } ) )  |`  om )
c1o 6274 class  1o
c2o 6275 class  2o
c3o 6276 class  3o
c4o 6277 class  4o
coa 6278 class  +o
comu 6279 class  .o
coei 6280 classo
df-1o 6281 |-  1o  =  suc  (/)
df-2o 6282 |-  2o  =  suc  1o
df-3o 6283 |-  3o  =  suc  2o
df-4o 6284 |-  4o  =  suc  3o
df-oadd 6285 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6286 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexpi 6287 |-o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e.  _V  |->  ( z  .o  x ) ) ,  1o ) `  y ) )
wer 6394 wff 
R  Er  A
cec 6395 class  [ A ] R
cqs 6396 class  ( A /. R )
df-er 6397 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6399 |-  [ A ] R  =  ( R " { A } )
df-qs 6403 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cmap 6510 class  ^m
cpm 6511 class  ^pm
df-map 6512 |- 
^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
df-pm 6513 |-  ^pm  =  ( x  e. 
_V ,  y  e. 
_V  |->  { f  e. 
~P ( y  X.  x )  |  Fun  f } )
cixp 6560 class  X_ x  e.  A  B
df-ixp 6561 |-  X_ x  e.  A  B  =  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
cen 6600 class  ~~
cdom 6601 class  ~<_
cfn 6602 class  Fin
df-en 6603 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 6604 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-fin 6605 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
cfi 6824 class  fi
df-fi 6825 |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
csup 6837 class  sup ( A ,  B ,  R )
cinf 6838 class inf ( A ,  B ,  R )
df-sup 6839 |- 
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 ) ) }
df-inf 6840 |- inf ( A ,  B ,  R )  =  sup ( A ,  B ,  `' R )
cdju 6890 class  ( A B )
df-dju 6891 |-  ( A B )  =  ( ( {
(/) }  X.  A
)  u.  ( { 1o }  X.  B
) )
cinl 6898 class inl
cinr 6899 class inr
df-inl 6900 |- inl 
=  ( x  e. 
_V  |->  <. (/) ,  x >. )
df-inr 6901 |- inr 
=  ( x  e. 
_V  |->  <. 1o ,  x >. )
cdjucase 6936 class case ( R ,  S )
df-case 6937 |- case
( R ,  S
)  =  ( ( R  o.  `'inl )  u.  ( S  o.  `'inr ) )
cdjud 6955 class  ( R ⊔d  S )
df-djud 6956 |-  ( R ⊔d  S )  =  ( ( R  o.  `' (inl  |`  dom  R
) )  u.  ( S  o.  `' (inr  |` 
dom  S ) ) )
comni 6972 class Omni
xnninf 6973 class
df-omni 6974 |- Omni 
=  { y  | 
A. f ( f : y --> 2o  ->  ( E. x  e.  y  ( f `  x
)  =  (/)  \/  A. x  e.  y  (
f `  x )  =  1o ) ) }
df-nninf 6975 |-  =  { f  e.  ( 2o  ^m  om )  |  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i ) }
cmarkov 6993 class Markov
df-markov 6994 |- Markov  =  { y  |  A. f ( f : y --> 2o  ->  ( -.  A. x  e.  y  ( f `  x
)  =  1o  ->  E. x  e.  y  ( f `  x )  =  (/) ) ) }
ccrd 7003 class  card
df-card 7004 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
wac 7029 wff CHOICE
df-ac 7030 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x ) )
wacc 7045 wff CCHOICE
df-cc 7046 |-  (CCHOICE  <->  A. x ( dom  x  ~~  om  ->  E. f
( f  C_  x  /\  f  Fn  dom  x ) ) )
cnpi 7048 class  N.
cpli 7049 class  +N
cmi 7050 class  .N
clti 7051 class  <N
cplpq 7052 class  +pQ
cmpq 7053 class  .pQ
cltpq 7054 class  <pQ
ceq 7055 class  ~Q
cnq 7056 class  Q.
c1q 7057 class  1Q
cplq 7058 class  +Q
cmq 7059 class  .Q
crq 7060 class  *Q
cltq 7061 class  <Q
ceq0 7062 class ~Q0
cnq0 7063 class Q0
c0q0 7064 class 0Q0
cplq0 7065 class +Q0
cmq0 7066 class ·Q0
cnp 7067 class  P.
c1p 7068 class  1P
cpp 7069 class  +P.
cmp 7070 class  .P.
cltp 7071 class  <P
cer 7072 class  ~R
cnr 7073 class  R.
c0r 7074 class  0R
c1r 7075 class  1R
cm1r 7076 class  -1R
cplr 7077 class  +R
cmr 7078 class  .R
cltr 7079 class  <R
df-ni 7080 |-  N.  =  ( om  \  { (/) } )
df-pli 7081 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 7082 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 7083 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 7120 |- 
+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 7121 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 7122 |- 
<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 7123 |- 
~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-nqqs 7124 |- 
Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
df-plqqs 7125 |- 
+Q  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  Q.  /\  y  e.  Q. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ]  ~Q  /\  y  =  [ <. u ,  f
>. ]  ~Q  )  /\  z  =  [ ( <. w ,  v >.  +pQ  <. u ,  f
>. ) ]  ~Q  )
) }
df-mqqs 7126 |- 
.Q  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  Q.  /\  y  e.  Q. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ]  ~Q  /\  y  =  [ <. u ,  f
>. ]  ~Q  )  /\  z  =  [ ( <. w ,  v >.  .pQ  <. u ,  f
>. ) ]  ~Q  )
) }
df-1nqqs 7127 |-  1Q  =  [ <. 1o ,  1o >. ]  ~Q
df-rq 7128 |-  *Q  =  { <. x ,  y >.  |  ( x  e.  Q.  /\  y  e.  Q.  /\  (
x  .Q  y )  =  1Q ) }
df-ltnqqs 7129 |- 
<Q  =  { <. x ,  y >.  |  ( ( x  e.  Q.  /\  y  e.  Q. )  /\  E. z E. w E. v E. u ( ( x  =  [ <. z ,  w >. ]  ~Q  /\  y  =  [ <. v ,  u >. ]  ~Q  )  /\  ( z  .N  u
)  <N  ( w  .N  v ) ) ) }
df-enq0 7200 |- ~Q0  =  { <. x ,  y
>.  |  ( (
x  e.  ( om 
X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) ) }
df-nq0 7201 |- Q0  =  ( ( om  X.  N. ) /. ~Q0  )
df-0nq0 7202 |- 0Q0  =  [ <. (/) ,  1o >. ] ~Q0
df-plq0 7203 |- +Q0  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e. Q0  /\  y  e. Q0 )  /\  E. w E. v E. u E. f
( ( x  =  [ <. w ,  v
>. ] ~Q0  /\  y  =  [ <. u ,  f >. ] ~Q0  )  /\  z  =  [ <. ( ( w  .o  f )  +o  (
v  .o  u ) ) ,  ( v  .o  f ) >. ] ~Q0  ) ) }
df-mq0 7204 |- ·Q0  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e. Q0  /\  y  e. Q0 )  /\  E. w E. v E. u E. f
( ( x  =  [ <. w ,  v
>. ] ~Q0  /\  y  =  [ <. u ,  f >. ] ~Q0  )  /\  z  =  [ <. ( w  .o  u
) ,  ( v  .o  f ) >. ] ~Q0  ) ) }
df-inp 7242 |- 
P.  =  { <. l ,  u >.  |  ( ( ( l  C_  Q.  /\  u  C_  Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e. 
Q.  r  e.  u
) )  /\  (
( A. q  e. 
Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )  /\  A. r  e.  Q.  (
r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) ) )  /\  A. q  e. 
Q.  -.  ( q  e.  l  /\  q  e.  u )  /\  A. q  e.  Q.  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) ) ) ) }
df-i1p 7243 |-  1P  =  <. { l  |  l  <Q  1Q } ,  { u  |  1Q  <Q  u } >.
df-iplp 7244 |- 
+P.  =  ( x  e.  P. ,  y  e.  P.  |->  <. { q  e.  Q.  |  E. r  e.  Q.  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) ) } ,  {
q  e.  Q.  |  E. r  e.  Q.  E. s  e.  Q.  (
r  e.  ( 2nd `  x )  /\  s  e.  ( 2nd `  y
)  /\  q  =  ( r  +Q  s
) ) } >. )
df-imp 7245 |- 
.P.  =  ( x  e.  P. ,  y  e.  P.  |->  <. { q  e.  Q.  |  E. r  e.  Q.  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) ) } ,  {
q  e.  Q.  |  E. r  e.  Q.  E. s  e.  Q.  (
r  e.  ( 2nd `  x )  /\  s  e.  ( 2nd `  y
)  /\  q  =  ( r  .Q  s
) ) } >. )
df-iltp 7246 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }
df-enr 7502 |- 
~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 7503 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 7504 |- 
+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  +P.  u ) ,  ( v  +P.  f ) >. ]  ~R  ) ) }
df-mr 7505 |-  .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  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. ]  ~R  )
) }
df-ltr 7506 |- 
<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 7507 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 7508 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 7509 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 7586 class  CC
cr 7587 class  RR
cc0 7588 class  0
c1 7589 class  1
ci 7590 class  _i
caddc 7591 class  +
cltrr 7592 class  <RR
cmul 7593 class  x.
df-c 7594 |-  CC  =  ( R.  X.  R. )
df-0 7595 |-  0  =  <. 0R ,  0R >.
df-1 7596 |-  1  =  <. 1R ,  0R >.
df-i 7597 |-  _i  =  <. 0R ,  1R >.
df-r 7598 |-  RR  =  ( R.  X.  { 0R } )
df-add 7599 |-  +  =  { <. <.
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 7600 |-  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 7601 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 7679 |-  CC  e.  _V
ax-resscn 7680 |-  RR  C_  CC
ax-1cn 7681 |-  1  e.  CC
ax-1re 7682 |-  1  e.  RR
ax-icn 7683 |-  _i  e.  CC
ax-addcl 7684 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 7685 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 7686 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 7687 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-addcom 7688 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  =  ( B  +  A ) )
ax-mulcom 7689 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 7690 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 7691 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 7692 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 7693 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-0lt1 7694 |-  0  <RR  1
ax-1rid 7695 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-0id 7696 |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
ax-rnegex 7697 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-precex 7698 |-  ( ( A  e.  RR  /\  0  <RR  A )  ->  E. x  e.  RR  ( 0  <RR  x  /\  ( A  x.  x )  =  1 ) )
ax-cnre 7699 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-ltirr 7700 |-  ( A  e.  RR  ->  -.  A  <RR  A )
ax-pre-ltwlin 7701 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( A  <RR  C  \/  C  <RR  B ) ) )
ax-pre-lttrn 7702 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-apti 7703 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  -.  ( A  <RR  B  \/  B  <RR  A ) )  ->  A  =  B )
ax-pre-ltadd 7704 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 7705 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-mulext 7706 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  x.  C
)  <RR  ( B  x.  C )  ->  ( A  <RR  B  \/  B  <RR  A ) ) )
ax-arch 7707 |-  ( A  e.  RR  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  (
y  +  1 )  e.  x ) } A  <RR  n )
ax-caucvg 7708 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }   &    |-  ( ph  ->  F : N --> RR )   &    |-  ( ph  ->  A. n  e.  N  A. k  e.  N  (
n  <RR  k  ->  (
( F `  n
)  <RR  ( ( F `
 k )  +  ( iota_ r  e.  RR  ( n  x.  r
)  =  1 ) )  /\  ( F `
 k )  <RR  ( ( F `  n
)  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) ) ) ) )   =>    |-  ( ph  ->  E. y  e.  RR  A. x  e.  RR  (
0  <RR  x  ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  ->  ( ( F `  k )  <RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) ) ) ) )
ax-pre-suploc 7709 |-  ( ( ( A 
C_  RR  /\  E. x  x  e.  A )  /\  ( E. x  e.  RR  A. y  e.  A  y  <RR  x  /\  A. x  e.  RR  A. y  e.  RR  (
x  <RR  y  ->  ( E. z  e.  A  x  <RR  z  \/  A. z  e.  A  z  <RR  y ) ) ) )  ->  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 7710 |-  +  : ( CC 
X.  CC ) --> CC
ax-mulf 7711 |-  x.  : ( CC 
X.  CC ) --> CC
cpnf 7765 class +oo
cmnf 7766 class -oo
cxr 7767 class  RR*
clt 7768 class  <
cle 7769 class  <_
df-pnf 7770 |- +oo  =  ~P U. CC
df-mnf 7771 |- -oo  =  ~P +oo
df-xr 7772 |-  RR*  =  ( RR  u.  { +oo , -oo }
)
df-ltxr 7773 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { -oo } )  X. 
{ +oo } )  u.  ( { -oo }  X.  RR ) ) )
df-le 7774 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 7901 class  -
cneg 7902 class  -u A
df-sub 7903 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC  ( y  +  z )  =  x ) )
df-neg 7904 |-  -u A  =  (
0  -  A )
creap 8304 class #
df-reap 8305 |- #  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  ( x  <  y  \/  y  <  x ) ) }
cap 8311 class #
df-ap 8312 |- #  =  { <. x ,  y
>.  |  E. r  e.  RR  E. s  e.  RR  E. t  e.  RR  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) ) }
cdiv 8400 class  /
df-div 8401 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC  ( y  x.  z
)  =  x ) )
cn 8688 class  NN
df-inn 8689 |-  NN  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
c2 8739 class  2
c3 8740 class  3
c4 8741 class  4
c5 8742 class  5
c6 8743 class  6
c7 8744 class  7
c8 8745 class  8
c9 8746 class  9
df-2 8747 |-  2  =  ( 1  +  1 )
df-3 8748 |-  3  =  ( 2  +  1 )
df-4 8749 |-  4  =  ( 3  +  1 )
df-5 8750 |-  5  =  ( 4  +  1 )
df-6 8751 |-  6  =  ( 5  +  1 )
df-7 8752 |-  7  =  ( 6  +  1 )
df-8 8753 |-  8  =  ( 7  +  1 )
df-9 8754 |-  9  =  ( 8  +  1 )
cn0 8945 class  NN0
df-n0 8946 |-  NN0  =  ( NN  u.  { 0 } )
cxnn0 9008 class NN0*
df-xnn0 9009 |- NN0* 
=  ( NN0  u.  { +oo } )
cz 9022 class  ZZ
df-z 9023 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 9150 class ; A B
df-dec 9151 |- ; A B  =  ( ( ( 9  +  1 )  x.  A )  +  B )
cuz 9294 class  ZZ>=
df-uz 9295 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 9379 class  QQ
df-q 9380 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 9409 class  RR+
df-rp 9410 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 9524 class  -e A
cxad 9525 class  +e
cxmu 9526 class  xe
df-xneg 9527 |-  -e A  =  if ( A  = +oo , -oo ,  if ( A  = -oo , +oo ,  -u A
) )
df-xadd 9528 |-  +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 9529 |-  xe  =  ( 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 9639 class  (,)
cioc 9640 class  (,]
cico 9641 class  [,)
cicc 9642 class  [,]
df-ioo 9643 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 9644 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 9645 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 9646 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 9758 class  ...
df-fz 9759 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 9887 class ..^
df-fzo 9888 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 10009 class  |_
cceil 10010 class
df-fl 10011 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ  ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
df-ceil 10012 |- =  ( x  e.  RR  |->  -u ( |_ `  -u x ) )
cmo 10063 class  mod
df-mod 10064 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 10186 class  seq M (  .+  ,  F )
df-seqfrec 10187 |- 
seq M (  .+  ,  F )  =  ran frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. )
cexp 10260 class  ^
df-exp 10261 |- 
^  =  ( 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 10439 class  !
df-fac 10440 |-  !  =  ( {
<. 0 ,  1
>. }  u.  seq 1
(  x.  ,  _I  ) )
cbc 10461 class  _C
df-bc 10462 |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n
)  /  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) ) ) ,  0 ) )
chash 10489 class
df-ihash 10490 |- =  ( (frec ( ( x  e.  ZZ  |->  ( x  +  1
) ) ,  0 )  u.  { <. om , +oo >. } )  o.  ( x  e. 
_V  |->  U. { y  e.  ( om  u.  { om } )  |  y  ~<_  x } ) )
cshi 10554 class  shift
df-shft 10555 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 10579 class  *
cre 10580 class  Re
cim 10581 class  Im
df-cj 10582 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC  ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 10583 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 10584 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqrt 10736 class  sqr
cabs 10737 class  abs
df-rsqrt 10738 |- 
sqr  =  ( x  e.  RR  |->  ( iota_ y  e.  RR  ( ( y ^ 2 )  =  x  /\  0  <_  y ) ) )
df-abs 10739 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
cli 11015 class  ~~>
df-clim 11016 |-  ~~>  =  { <. 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 ) ) }
csu 11090 class  sum_ k  e.  A  B
df-sumdc 11091 |- 
sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  (
ZZ>= `  m )DECID  j  e.  A  /\  seq m
(  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  0 ) ) ) `  m
) ) ) )
ce 11275 class  exp
ceu 11276 class  _e
csin 11277 class  sin
ccos 11278 class  cos
ctan 11279 class  tan
cpi 11280 class  pi
df-ef 11281 |-  exp  =  ( x  e.  CC  |->  sum_ k  e.  NN0  ( ( x ^
k )  /  ( ! `  k )
) )
df-e 11282 |-  _e  =  ( exp `  1 )
df-sin 11283 |- 
sin  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  -  ( exp `  ( -u _i  x.  x ) ) )  /  ( 2  x.  _i ) ) )
df-cos 11284 |- 
cos  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  +  ( exp `  ( -u _i  x.  x ) ) )  /  2 ) )
df-tan 11285 |- 
tan  =  ( x  e.  ( `' cos " ( CC  \  {
0 } ) ) 
|->  ( ( sin `  x
)  /  ( cos `  x ) ) )
df-pi 11286 |-  pi  = inf ( ( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  <  )
ctau 11408 class  tau
df-tau 11409 |- 
tau  = inf ( ( RR+  i^i  ( `' cos " { 1 } ) ) ,  RR ,  <  )
cdvds 11420 class  ||
df-dvds 11421 |- 
||  =  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
cgcd 11562 class  gcd
df-gcd 11563 |- 
gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
clcm 11668 class lcm
df-lcm 11669 |- lcm 
=  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 , inf ( { n  e.  NN  |  ( x  ||  n  /\  y  ||  n
) } ,  RR ,  <  ) ) )
cprime 11715 class  Prime
df-prm 11716 |- 
Prime  =  { p  e.  NN  |  { n  e.  NN  |  n  ||  p }  ~~  2o }
cnumer 11786 class numer
cdenom 11787 class denom
df-numer 11788 |- numer  =  ( y  e.  QQ  |->  ( 1st `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
df-denom 11789 |- denom  =  ( y  e.  QQ  |->  ( 2nd `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
cphi 11813 class  phi
df-phi 11814 |- 
phi  =  ( n  e.  NN  |->  ( `  {
x  e.  ( 1 ... n )  |  ( x  gcd  n
)  =  1 } ) )
cstr 11882 class Struct
cnx 11883 class  ndx
csts 11884 class sSet
cslot 11885 class Slot  A
cbs 11886 class  Base
cress 11887 classs
df-struct 11888 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( f 
\  { (/) } )  /\  dom  f  C_  ( ... `  x ) ) }
df-ndx 11889 |- 
ndx  =  (  _I  |`  NN )
df-slot 11890 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
df-base 11892 |- 
Base  = Slot  1
df-sets 11893 |- sSet 
=  ( s  e. 
_V ,  e  e. 
_V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u.  { e } ) )
df-ress 11894 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  if ( ( Base `  w
)  C_  x ,  w ,  ( w sSet  <.
( Base `  ndx ) ,  ( x  i^i  ( Base `  w ) )
>. ) ) )
cplusg 11948 class  +g
cmulr 11949 class  .r
cstv 11950 class  *r
csca 11951 class Scalar
cvsca 11952 class  .s
cip 11953 class  .i
cts 11954 class TopSet
cple 11955 class  le
coc 11956 class  oc
cds 11957 class  dist
cunif 11958 class  UnifSet
chom 11959 class  Hom
cco 11960 class comp
df-plusg 11961 |- 
+g  = Slot  2
df-mulr 11962 |- 
.r  = Slot  3
df-starv 11963 |-  *r  = Slot  4
df-sca 11964 |- Scalar  = Slot  5
df-vsca 11965 |-  .s  = Slot  6
df-ip 11966 |-  .i  = Slot  8
df-tset 11967 |- TopSet  = Slot  9
df-ple 11968 |- 
le  = Slot ; 1 0
df-ocomp 11969 |-  oc  = Slot ; 1 1
df-ds 11970 |-  dist 
= Slot ; 1 2
df-unif 11971 |- 
UnifSet  = Slot ; 1 3
df-hom 11972 |- 
Hom  = Slot ; 1 4
df-cco 11973 |- comp 
= Slot ; 1 5
crest 12047 classt
ctopn 12048 class  TopOpen
df-rest 12049 |-t  =  ( j  e.  _V ,  x  e.  _V  |->  ran  ( y  e.  j 
|->  ( y  i^i  x
) ) )
df-topn 12050 |-  TopOpen  =  ( w  e. 
_V  |->  ( (TopSet `  w )t  ( Base `  w
) ) )
ctg 12062 class  topGen
cpt 12063 class  Xt_
c0g 12064 class  0g
cgsu 12065 class  gsumg
df-0g 12066 |-  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 12067 |- 
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
) ) ) ) ) ) )
df-topgen 12068 |- 
topGen  =  ( x  e. 
_V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
df-pt 12069 |-  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 12070 class  X_s
cpws 12071 class  ^s
df-prds 12072 |-  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 ) ) ) ) >. ,  <. ( .i `  ndx ) ,  ( f  e.  v ,  g  e.  v  |->  ( s  gsumg  ( x  e.  dom  r  |->  ( ( f `  x
) ( .i `  ( 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 12074 |- 
^s  =  ( r  e. 
_V ,  i  e. 
_V  |->  ( (Scalar `  r ) X_s ( i  X.  {
r } ) ) )
cpsmet 12075 class PsMet
cxmet 12076 class  *Met
cmet 12077 class  Met
cbl 12078 class  ball
cfbas 12079 class  fBas
cfg 12080 class  filGen
cmopn 12081 class  MetOpen
cmetu 12082 class metUnif
df-psmet 12083 |- PsMet  =  ( x  e. 
_V  |->  { d  e.  ( RR*  ^m  (
x  X.  x ) )  |  A. y  e.  x  ( (
y d y )  =  0  /\  A. z  e.  x  A. w  e.  x  (
y d z )  <_  ( ( w d y ) +e ( w d z ) ) ) } )
df-xmet 12084 |- 
*Met  =  ( x  e.  _V  |->  { d  e.  ( RR*  ^m  ( x  X.  x
) )  |  A. y  e.  x  A. z  e.  x  (
( ( y d z )  =  0  <-> 
y  =  z )  /\  A. w  e.  x  ( y d z )  <_  (
( w d y ) +e ( w d z ) ) ) } )
df-met 12085 |- 
Met  =  ( x  e.  _V  |->  { d  e.  ( RR  ^m  ( x  X.  x
) )  |  A. y  e.  x  A. z  e.  x  (
( ( y d z )  =  0  <-> 
y  =  z )  /\  A. w  e.  x  ( y d z )  <_  (
( w d y )  +  ( w d z ) ) ) } )
df-bl 12086 |-  ball 
=  ( d  e. 
_V  |->  ( x  e. 
dom  dom  d ,  z  e.  RR*  |->  { y  e.  dom  dom  d  |  ( x d y )  <  z } ) )
df-mopn 12087 |-  MetOpen  =  ( d  e. 
U. ran  *Met  |->  ( topGen `  ran  ( ball `  d ) ) )
df-fbas 12088 |- 
fBas  =  ( w  e.  _V  |->  { x  e. 
~P ~P w  |  ( x  =/=  (/)  /\  (/)  e/  x  /\  A. y  e.  x  A. z  e.  x  ( x  i^i  ~P (
y  i^i  z )
)  =/=  (/) ) } )
df-fg 12089 |-  filGen  =  ( w  e. 
_V ,  x  e.  ( fBas `  w
)  |->  { y  e. 
~P w  |  ( x  i^i  ~P y
)  =/=  (/) } )
df-metu 12090 |- metUnif  =  ( d  e. 
U. ran PsMet  |->  ( ( dom  dom  d  X.  dom  dom  d ) filGen ran  (
a  e.  RR+  |->  ( `' d " ( 0 [,) a ) ) ) ) )
ctop 12091 class  Top
df-top 12092 |- 
Top  =  { x  |  ( A. y  e.  ~P  x U. y  e.  x  /\  A. y  e.  x  A. z  e.  x  ( y  i^i  z )  e.  x
) }
ctopon 12104 class TopOn
df-topon 12105 |- TopOn  =  ( b  e. 
_V  |->  { j  e. 
Top  |  b  =  U. j } )
ctps 12124 class  TopSp
df-topsp 12125 |- 
TopSp  =  { f  |  ( TopOpen `  f
)  e.  (TopOn `  ( Base `  f )
) }
ctb 12136 class  TopBases
df-bases 12137 |-  TopBases  =  { x  | 
A. y  e.  x  A. z  e.  x  ( y  i^i  z
)  C_  U. (
x  i^i  ~P (
y  i^i  z )
) }
ccld 12188 class  Clsd
cnt 12189 class  int
ccl 12190 class  cls
df-cld 12191 |- 
Clsd  =  ( j  e.  Top  |->  { x  e. 
~P U. j  |  ( U. j  \  x
)  e.  j } )
df-ntr 12192 |- 
int  =  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) ) )
df-cls 12193 |- 
cls  =  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
|^| { y  e.  (
Clsd `  j )  |  x  C_  y } ) )
cnei 12234 class  nei
df-nei 12235 |- 
nei  =  ( j  e.  Top  |->  ( x  e.  ~P U. j  |->  { y  e.  ~P U. j  |  E. g  e.  j  ( x  C_  g  /\  g  C_  y ) } ) )
ccn 12281 class  Cn
ccnp 12282 class  CnP
clm 12283 class  ~~> t
df-cn 12284 |-  Cn  =  ( j  e.  Top ,  k  e. 
Top  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  ( `' f " y
)  e.  j } )
df-cnp 12285 |- 
CnP  =  ( j  e.  Top ,  k  e.  Top  |->  ( x  e.  U. j  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  ( ( f `
 x )  e.  y  ->  E. g  e.  j  ( x  e.  g  /\  (
f " g ) 
C_  y ) ) } ) )
df-lm 12286 |-  ~~> t  =  ( j  e. 
Top  |->  { <. f ,  x >.  |  (
f  e.  ( U. j  ^pm  CC )  /\  x  e.  U. j  /\  A. u  e.  j  ( x  e.  u  ->  E. y  e.  ran  ZZ>= ( f  |`  y
) : y --> u ) ) } )
ctx 12348 class  tX
df-tx 12349 |-  tX  =  ( r  e. 
_V ,  s  e. 
_V  |->  ( topGen `  ran  ( x  e.  r ,  y  e.  s  |->  ( x  X.  y
) ) ) )
chmeo 12396 class  Homeo
df-hmeo 12397 |- 
Homeo  =  ( j  e.  Top ,  k  e. 
Top  |->  { f  e.  ( j  Cn  k
)  |  `' f  e.  ( k  Cn  j ) } )
cxms 12432 class  *MetSp
cms 12433 class  MetSp
ctms 12434 class toMetSp
df-xms 12435 |- 
*MetSp  =  { f  e.  TopSp  |  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) ) }
df-ms 12436 |-  MetSp  =  { f  e.  *MetSp  |  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) )  e.  ( Met `  ( Base `  f ) ) }
df-tms 12437 |- toMetSp  =  ( d  e. 
U. ran  *Met  |->  ( { <. ( Base `  ndx ) ,  dom  dom  d >. ,  <. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
ccncf 12653 class  -cn->
df-cncf 12654 |- 
-cn->  =  ( a  e. 
~P CC ,  b  e.  ~P CC  |->  { f  e.  ( b  ^m  a )  | 
A. x  e.  a 
A. e  e.  RR+  E. d  e.  RR+  A. y  e.  a  ( ( abs `  ( x  -  y ) )  < 
d  ->  ( abs `  ( ( f `  x )  -  (
f `  y )
) )  <  e
) } )
climc 12719 class lim CC
cdv 12720 class  _D
df-limced 12721 |- lim
CC  =  ( f  e.  ( CC  ^pm  CC ) ,  x  e.  CC  |->  { y  e.  CC  |  ( ( f : dom  f --> CC  /\  dom  f  C_  CC )  /\  (
x  e.  CC  /\  A. e  e.  RR+  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e ) ) ) } )
df-dvap 12722 |- 
_D  =  ( s  e.  ~P CC , 
f  e.  ( CC 
^pm  s )  |->  U_ x  e.  ( ( int `  ( ( MetOpen `  ( abs  o.  -  )
)t  s ) ) `  dom  f ) ( { x }  X.  (
( z  e.  {
w  e.  dom  f  |  w #  x }  |->  ( ( ( f `
 z )  -  ( f `  x
) )  /  (
z  -  x ) ) ) lim CC  x
) ) )
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 12927 wff 
A DECIDin  B
df-dcin 12928 |-  ( A DECIDin  B 
<-> 
A. x  e.  B DECID  x  e.  A )
wbd 12937 wff BOUNDED  ph
ax-bd0 12938 |-  ( ph  <->  ps )   =>    |-  (BOUNDED  ph  -> BOUNDED  ps )
ax-bdim 12939 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  ->  ps )
ax-bdan 12940 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  /\  ps )
ax-bdor 12941 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  \/  ps )
ax-bdn 12942 |- BOUNDED  ph   =>    |- BOUNDED  -.  ph
ax-bdal 12943 |- BOUNDED  ph   =>    |- BOUNDED  A. x  e.  y 
ph
ax-bdex 12944 |- BOUNDED  ph   =>    |- BOUNDED  E. x  e.  y 
ph
ax-bdeq 12945 |- BOUNDED  x  =  y
ax-bdel 12946 |- BOUNDED  x  e.  y
ax-bdsb 12947 |- BOUNDED  ph   =>    |- BOUNDED  [ y  /  x ] ph
wbdc 12965 wff BOUNDED  A
df-bdc 12966 |-  (BOUNDED  A 
<-> 
A. xBOUNDED  x  e.  A )
ax-bdsep 13009 |- BOUNDED  ph   =>    |-  A. a E. b A. x
( x  e.  b  <-> 
( x  e.  a  /\  ph ) )
ax-bj-d0cl 13049 |- BOUNDED  ph   =>    |- DECID  ph
wind 13051 wff Ind  A
df-bj-ind 13052 |-  (Ind  A  <->  ( (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A ) )
ax-infvn 13066 |- 
E. x (Ind  x  /\  A. y (Ind  y  ->  x  C_  y
) )
ax-bdsetind 13093 |- BOUNDED  ph   =>    |-  ( A. a ( A. y  e.  a  [ y  /  a ] ph  ->  ph )  ->  A. a ph )
ax-inf2 13101 |- 
E. a A. x
( x  e.  a  <-> 
( x  =  (/)  \/ 
E. y  e.  a  x  =  suc  y
) )
ax-strcoll 13107 |- 
A. a ( A. x  e.  a  E. y ph  ->  E. b A. y ( y  e.  b  <->  E. x  e.  a 
ph ) )
ax-sscoll 13112 |- 
A. a A. b E. c A. z ( A. x  e.  a  E. y  e.  b 
ph  ->  E. d  e.  c 
A. y ( y  e.  d  <->  E. x  e.  a  ph ) )
ax-ddkcomp 13114 |-  ( ( ( A 
C_  RR  /\  E. x  x  e.  A )  /\  E. x  e.  RR  A. y  e.  A  y  <  x  /\  A. x  e.  RR  A. y  e.  RR  ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )  ->  E. x  e.  RR  ( A. y  e.  A  y  <_  x  /\  (
( B  e.  R  /\  A. y  e.  A  y  <_  B )  ->  x  <_  B ) ) )
walsi 13169 wff  A.! x ( ph  ->  ps )
walsc 13170 wff  A.! x  e.  A ph
df-alsi 13171 |-  ( A.! x (
ph  ->  ps )  <->  ( A. x ( ph  ->  ps )  /\  E. x ph ) )
df-alsc 13172 |-  ( A.! x  e.  A ph  <->  ( A. x  e.  A  ph  /\  E. x  x  e.  A
) )
  Copyright terms: Public domain W3C validator