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 104 wff  ( ph  /\  ps )
wb 105 wff  ( ph  <->  ps )
ax-ia1 106 |-  ( ( ph  /\  ps )  ->  ph )
ax-ia2 107 |-  ( ( ph  /\  ps )  ->  ps )
ax-ia3 108 |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
df-bi 117 |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )  /\  (
( ( ph  ->  ps )  /\  ( ps 
->  ph ) )  -> 
( ph  <->  ps ) ) )
ax-in1 614 |-  ( ( ph  ->  -. 
ph )  ->  -.  ph )
ax-in2 615 |-  ( -.  ph  ->  (
ph  ->  ps ) )
wo 708 wff  ( ph  \/  ps )
ax-io 709 |-  ( ( ( ph  \/  ch )  ->  ps ) 
<->  ( ( ph  ->  ps )  /\  ( ch 
->  ps ) ) )
wstab 830 wff STAB  ph
df-stab 831 |-  (STAB 
ph 
<->  ( -.  -.  ph  ->  ph ) )
wdc 834 wff DECID  ph
df-dc 835 |-  (DECID 
ph 
<->  ( ph  \/  -.  ph ) )
w3o 977 wff  ( ph  \/  ps  \/  ch )
w3a 978 wff  ( ph  /\  ps  /\ 
ch )
df-3or 979 |-  ( ( ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/ 
ch ) )
df-3an 980 |-  ( ( ph  /\  ps  /\  ch )  <->  ( ( ph  /\  ps )  /\  ch ) )
wal 1351 wff  A. x ph
cv 1352 class  x
wceq 1353 wff 
A  =  B
wtru 1354 wff T.
df-tru 1356 |-  ( T.  <->  ( A. x  x  =  x  ->  A. x  x  =  x ) )
wfal 1358 wff F.
df-fal 1359 |-  ( F.  <->  -. T.  )
wxo 1375 wff  ( ph  \/_  ps )
df-xor 1376 |-  ( ( ph  \/_  ps ) 
<->  ( ( ph  \/  ps )  /\  -.  ( ph  /\  ps ) ) )
ax-5 1447 |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
ax-7 1448 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-gen 1449 |- 
ph   =>    |- 
A. x ph
wnf 1460 wff 
F/ x ph
df-nf 1461 |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
wex 1492 wff 
E. x ph
ax-ie1 1493 |-  ( E. x ph  ->  A. x E. x ph )
ax-ie2 1494 |-  ( A. x ( ps  ->  A. x ps )  ->  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) ) )
ax-8 1504 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-10 1505 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11 1506 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-i12 1507 |-  ( A. z  z  =  x  \/  ( A. z  z  =  y  \/  A. z
( x  =  y  ->  A. z  x  =  y ) ) )
ax-bndl 1509 |-  ( A. z  z  =  x  \/  ( A. z  z  =  y  \/  A. x A. z ( x  =  y  ->  A. z  x  =  y )
) )
ax-4 1510 |-  ( A. x ph  ->  ph )
ax-17 1526 |-  ( ph  ->  A. x ph )
ax-i9 1530 |-  E. x  x  =  y
ax-ial 1534 |-  ( A. x ph  ->  A. x A. x ph )
ax-i5r 1535 |-  ( ( A. x ph  ->  A. x ps )  ->  A. x ( A. x ph  ->  ps )
)
ax-10o 1716 |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph ) )
wsb 1762 wff 
[ y  /  x ] ph
df-sb 1763 |-  ( [ y  /  x ] ph  <->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph ) ) )
ax-16 1814 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
ax-11o 1823 |-  ( -.  A. x  x  =  y  ->  ( x  =  y  -> 
( ph  ->  A. x
( x  =  y  ->  ph ) ) ) )
weu 2026 wff 
E! x ph
wmo 2027 wff 
E* x ph
df-eu 2029 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
df-mo 2030 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
wcel 2148 wff 
A  e.  B
ax-13 2150 |-  ( x  =  y  ->  ( x  e.  z  ->  y  e.  z ) )
ax-14 2151 |-  ( x  =  y  ->  ( z  e.  x  ->  z  e.  y ) )
ax-ext 2159 |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
cab 2163 class  { x  |  ph }
df-clab 2164 |-  ( x  e.  {
y  |  ph }  <->  [ x  /  y ]
ph )
df-cleq 2170 |-  ( A. x ( x  e.  y  <->  x  e.  z )  ->  y  =  z )   =>    |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
df-clel 2173 |-  ( A  e.  B  <->  E. x ( x  =  A  /\  x  e.  B ) )
wnfc 2306 wff  F/_ x A
df-nfc 2308 |-  ( F/_ x A  <->  A. y F/ x  y  e.  A )
wne 2347 wff 
A  =/=  B
df-ne 2348 |-  ( A  =/=  B  <->  -.  A  =  B )
wnel 2442 wff 
A  e/  B
df-nel 2443 |-  ( A  e/  B  <->  -.  A  e.  B )
wral 2455 wff  A. x  e.  A  ph
wrex 2456 wff 
E. x  e.  A  ph
wreu 2457 wff 
E! x  e.  A  ph
wrmo 2458 wff 
E* x  e.  A  ph
crab 2459 class  { x  e.  A  |  ph }
df-ral 2460 |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
df-rex 2461 |-  ( E. x  e.  A  ph  <->  E. x
( x  e.  A  /\  ph ) )
df-reu 2462 |-  ( E! x  e.  A  ph  <->  E! x
( x  e.  A  /\  ph ) )
df-rmo 2463 |-  ( E* x  e.  A  ph  <->  E* x
( x  e.  A  /\  ph ) )
df-rab 2464 |- 
{ x  e.  A  |  ph }  =  {
x  |  ( x  e.  A  /\  ph ) }
cvv 2738 class  _V
df-v 2740 |-  _V  =  { x  |  x  =  x }
wcdeq 2946 wff CondEq ( x  =  y  ->  ph )
df-cdeq 2947 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 2963 wff  [. A  /  x ]. ph
df-sbc 2964 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 3058 class  [_ A  /  x ]_ B
df-csb 3059 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 3127 class  ( A  \  B )
cun 3128 class  ( A  u.  B )
cin 3129 class  ( A  i^i  B )
wss 3130 wff 
A  C_  B
df-dif 3132 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 3134 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 3136 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 3143 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
c0 3423 class  (/)
df-nul 3424 |-  (/)  =  ( _V  \  _V )
cif 3535 class  if ( ph ,  A ,  B )
df-if 3536 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3576 class  ~P A
df-pw 3578 |-  ~P A  =  {
x  |  x  C_  A }
csn 3593 class  { A }
cpr 3594 class  { A ,  B }
ctp 3595 class  { A ,  B ,  C }
cop 3596 class  <. A ,  B >.
cotp 3597 class  <. A ,  B ,  C >.
df-sn 3599 |-  { A }  =  {
x  |  x  =  A }
df-pr 3600 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3601 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3602 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3603 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 3810 class  U. A
df-uni 3811 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 3845 class  |^| A
df-int 3846 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 3887 class  U_ x  e.  A  B
ciin 3888 class  |^|_
x  e.  A  B
df-iun 3889 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 3890 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 3981 wff Disj  x  e.  A  B
df-disj 3982 |-  (Disj  x  e.  A  B 
<-> 
A. y E* x  e.  A  y  e.  B )
wbr 4004 wff 
A R B
df-br 4005 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 4064 class  {
<. x ,  y >.  |  ph }
cmpt 4065 class  ( x  e.  A  |->  B )
df-opab 4066 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 4067 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 4102 wff 
Tr  A
df-tr 4103 |-  ( Tr  A  <->  U. A  C_  A )
ax-coll 4119 |-  F/ b ph   =>    |-  ( A. x  e.  a  E. y ph  ->  E. b A. x  e.  a  E. y  e.  b  ph )
ax-sep 4122 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 4130 |- 
E. x A. y  -.  y  e.  x
ax-pow 4175 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
wem 4195 wff EXMID
df-exmid 4196 |-  (EXMID  <->  A. x ( x  C_  {
(/) }  -> DECID  (/)  e.  x ) )
ax-pr 4210 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4288 class  _E
cid 4289 class  _I
df-eprel 4290 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4294 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4295 wff 
R  Po  A
wor 4296 wff 
R  Or  A
df-po 4297 |-  ( 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 4298 |-  ( 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 4328 wff FrFor  R A S
wfr 4329 wff 
R  Fr  A
wse 4330 wff 
R Se  A
wwe 4331 wff 
R  We  A
df-frfor 4332 |-  (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 4333 |-  ( R  Fr  A  <->  A. sFrFor  R A s )
df-se 4334 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-wetr 4335 |-  ( 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 4363 wff 
Ord  A
con0 4364 class  On
wlim 4365 wff 
Lim  A
csuc 4366 class  suc 
A
df-iord 4367 |-  ( Ord  A  <->  ( Tr  A  /\  A. x  e.  A  Tr  x ) )
df-on 4369 |-  On  =  { x  |  Ord  x }
df-ilim 4370 |-  ( Lim  A  <->  ( Ord  A  /\  (/)  e.  A  /\  A  =  U. A ) )
df-suc 4372 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4434 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
ax-setind 4537 |-  ( A. a ( A. y  e.  a  [ y  /  a ] ph  ->  ph )  ->  A. a ph )
ax-iinf 4588 |- 
E. x ( (/)  e.  x  /\  A. y
( y  e.  x  ->  suc  y  e.  x
) )
com 4590 class  om
df-iom 4591 |- 
om  =  |^| { x  |  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
) }
cxp 4625 class  ( A  X.  B )
ccnv 4626 class  `' A
cdm 4627 class  dom 
A
crn 4628 class  ran 
A
cres 4629 class  ( A  |`  B )
cima 4630 class  ( A " B )
ccom 4631 class  ( A  o.  B )
wrel 4632 wff 
Rel  A
df-xp 4633 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4634 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4635 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4636 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4637 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4638 |-  ran  A  =  dom  `' A
df-res 4639 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4640 |-  ( A " B
)  =  ran  ( A  |`  B )
cio 5177 class  ( iota x ph )
df-iota 5179 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
wfun 5211 wff 
Fun  A
wfn 5212 wff 
A  Fn  B
wf 5213 wff 
F : A --> B
wf1 5214 wff 
F : A -1-1-> B
wfo 5215 wff 
F : A -onto-> B
wf1o 5216 wff 
F : A -1-1-onto-> B
cfv 5217 class  ( F `  A )
wiso 5218 wff 
H  Isom  R ,  S  ( A ,  B )
df-fun 5219 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 5220 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 5221 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 5222 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 5223 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 5224 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 5225 |-  ( F `  A )  =  ( iota x A F x )
df-isom 5226 |-  ( 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 5830 class  (
iota_ x  e.  A  ph )
df-riota 5831 |-  ( iota_ x  e.  A  ph )  =  ( iota
x ( x  e.  A  /\  ph )
)
co 5875 class  ( A F B )
coprab 5876 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpo 5877 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 5878 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 5879 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpo 5880 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 6081 class  oF R
cofr 6082 class  oR R
df-of 6083 |-  oF R  =  ( f  e.  _V ,  g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 6084 |-  oR R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 6139 class  1st
c2nd 6140 class  2nd
df-1st 6141 |- 
1st  =  ( x  e.  _V  |->  U. dom  { x } )
df-2nd 6142 |- 
2nd  =  ( x  e.  _V  |->  U. ran  { x } )
ctpos 6245 class tpos  F
df-tpos 6246 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
wsmo 6286 wff 
Smo  A
df-smo 6287 |-  ( 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 6305 class recs ( F )
df-recs 6306 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 6370 class  rec ( F ,  I
)
df-irdg 6371 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  ( I  u.  U_ x  e.  dom  g ( F `
 ( g `  x ) ) ) ) )
cfrec 6391 class frec ( F ,  I )
df-frec 6392 |- 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 6410 class  1o
c2o 6411 class  2o
c3o 6412 class  3o
c4o 6413 class  4o
coa 6414 class  +o
comu 6415 class  .o
coei 6416 classo
df-1o 6417 |-  1o  =  suc  (/)
df-2o 6418 |-  2o  =  suc  1o
df-3o 6419 |-  3o  =  suc  2o
df-4o 6420 |-  4o  =  suc  3o
df-oadd 6421 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6422 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexpi 6423 |-o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e.  _V  |->  ( z  .o  x ) ) ,  1o ) `  y ) )
wer 6532 wff 
R  Er  A
cec 6533 class  [ A ] R
cqs 6534 class  ( A /. R )
df-er 6535 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6537 |-  [ A ] R  =  ( R " { A } )
df-qs 6541 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cmap 6648 class  ^m
cpm 6649 class  ^pm
df-map 6650 |- 
^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
df-pm 6651 |-  ^pm  =  ( x  e. 
_V ,  y  e. 
_V  |->  { f  e. 
~P ( y  X.  x )  |  Fun  f } )
cixp 6698 class  X_ x  e.  A  B
df-ixp 6699 |-  X_ x  e.  A  B  =  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
cen 6738 class  ~~
cdom 6739 class  ~<_
cfn 6740 class  Fin
df-en 6741 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 6742 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-fin 6743 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
cfi 6967 class  fi
df-fi 6968 |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
csup 6981 class  sup ( A ,  B ,  R )
cinf 6982 class inf ( A ,  B ,  R )
df-sup 6983 |- 
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 6984 |- inf ( A ,  B ,  R )  =  sup ( A ,  B ,  `' R )
cdju 7036 class  ( A B )
df-dju 7037 |-  ( A B )  =  ( ( {
(/) }  X.  A
)  u.  ( { 1o }  X.  B
) )
cinl 7044 class inl
cinr 7045 class inr
df-inl 7046 |- inl 
=  ( x  e. 
_V  |->  <. (/) ,  x >. )
df-inr 7047 |- inr 
=  ( x  e. 
_V  |->  <. 1o ,  x >. )
cdjucase 7082 class case ( R ,  S )
df-case 7083 |- case
( R ,  S
)  =  ( ( R  o.  `'inl )  u.  ( S  o.  `'inr ) )
cdjud 7101 class  ( R ⊔d  S )
df-djud 7102 |-  ( R ⊔d  S )  =  ( ( R  o.  `' (inl  |`  dom  R
) )  u.  ( S  o.  `' (inr  |` 
dom  S ) ) )
xnninf 7118 class
df-nninf 7119 |-  =  { f  e.  ( 2o  ^m  om )  |  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i ) }
comni 7132 class Omni
df-omni 7133 |- Omni 
=  { y  | 
A. f ( f : y --> 2o  ->  ( E. x  e.  y  ( f `  x
)  =  (/)  \/  A. x  e.  y  (
f `  x )  =  1o ) ) }
cmarkov 7149 class Markov
df-markov 7150 |- Markov  =  { y  |  A. f ( f : y --> 2o  ->  ( -.  A. x  e.  y  ( f `  x
)  =  1o  ->  E. x  e.  y  ( f `  x )  =  (/) ) ) }
cwomni 7161 class WOmni
df-womni 7162 |- WOmni  =  { y  |  A. f ( f : y --> 2o  -> DECID  A. x  e.  y  ( f `  x
)  =  1o ) }
ccrd 7178 class  card
df-card 7179 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
wac 7204 wff CHOICE
df-ac 7205 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x ) )
wap 7246 wff 
R Ap  A
df-pap 7247 |-  ( R Ap  A  <->  ( ( R  C_  ( A  X.  A )  /\  A. x  e.  A  -.  x R x )  /\  ( A. x  e.  A  A. y  e.  A  ( x R y  ->  y R x )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R y  ->  (
x R z  \/  y R z ) ) ) ) )
wtap 7248 wff 
R TAp  A
df-tap 7249 |-  ( R TAp  A  <->  ( R Ap  A  /\  A. x  e.  A  A. y  e.  A  ( -.  x R y  ->  x  =  y ) ) )
wacc 7261 wff CCHOICE
df-cc 7262 |-  (CCHOICE  <->  A. x ( dom  x  ~~  om  ->  E. f
( f  C_  x  /\  f  Fn  dom  x ) ) )
cnpi 7271 class  N.
cpli 7272 class  +N
cmi 7273 class  .N
clti 7274 class  <N
cplpq 7275 class  +pQ
cmpq 7276 class  .pQ
cltpq 7277 class  <pQ
ceq 7278 class  ~Q
cnq 7279 class  Q.
c1q 7280 class  1Q
cplq 7281 class  +Q
cmq 7282 class  .Q
crq 7283 class  *Q
cltq 7284 class  <Q
ceq0 7285 class ~Q0
cnq0 7286 class Q0
c0q0 7287 class 0Q0
cplq0 7288 class +Q0
cmq0 7289 class ·Q0
cnp 7290 class  P.
c1p 7291 class  1P
cpp 7292 class  +P.
cmp 7293 class  .P.
cltp 7294 class  <P
cer 7295 class  ~R
cnr 7296 class  R.
c0r 7297 class  0R
c1r 7298 class  1R
cm1r 7299 class  -1R
cplr 7300 class  +R
cmr 7301 class  .R
cltr 7302 class  <R
df-ni 7303 |-  N.  =  ( om  \  { (/) } )
df-pli 7304 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 7305 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 7306 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 7343 |- 
+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 7344 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 7345 |- 
<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 7346 |- 
~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 7347 |- 
Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
df-plqqs 7348 |- 
+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 7349 |- 
.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 7350 |-  1Q  =  [ <. 1o ,  1o >. ]  ~Q
df-rq 7351 |-  *Q  =  { <. x ,  y >.  |  ( x  e.  Q.  /\  y  e.  Q.  /\  (
x  .Q  y )  =  1Q ) }
df-ltnqqs 7352 |- 
<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 7423 |- ~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 7424 |- Q0  =  ( ( om  X.  N. ) /. ~Q0  )
df-0nq0 7425 |- 0Q0  =  [ <. (/) ,  1o >. ] ~Q0
df-plq0 7426 |- +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 7427 |- ·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 7465 |- 
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 7466 |-  1P  =  <. { l  |  l  <Q  1Q } ,  { u  |  1Q  <Q  u } >.
df-iplp 7467 |- 
+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 7468 |- 
.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 7469 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }
df-enr 7725 |- 
~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 7726 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 7727 |- 
+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 7728 |-  .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 7729 |- 
<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 7730 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 7731 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 7732 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 7809 class  CC
cr 7810 class  RR
cc0 7811 class  0
c1 7812 class  1
ci 7813 class  _i
caddc 7814 class  +
cltrr 7815 class  <RR
cmul 7816 class  x.
df-c 7817 |-  CC  =  ( R.  X.  R. )
df-0 7818 |-  0  =  <. 0R ,  0R >.
df-1 7819 |-  1  =  <. 1R ,  0R >.
df-i 7820 |-  _i  =  <. 0R ,  1R >.
df-r 7821 |-  RR  =  ( R.  X.  { 0R } )
df-add 7822 |-  +  =  { <. <.
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 7823 |-  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 7824 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 7902 |-  CC  e.  _V
ax-resscn 7903 |-  RR  C_  CC
ax-1cn 7904 |-  1  e.  CC
ax-1re 7905 |-  1  e.  RR
ax-icn 7906 |-  _i  e.  CC
ax-addcl 7907 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 7908 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 7909 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 7910 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-addcom 7911 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  =  ( B  +  A ) )
ax-mulcom 7912 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 7913 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 7914 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 7915 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 7916 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-0lt1 7917 |-  0  <RR  1
ax-1rid 7918 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-0id 7919 |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
ax-rnegex 7920 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-precex 7921 |-  ( ( A  e.  RR  /\  0  <RR  A )  ->  E. x  e.  RR  ( 0  <RR  x  /\  ( A  x.  x )  =  1 ) )
ax-cnre 7922 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-ltirr 7923 |-  ( A  e.  RR  ->  -.  A  <RR  A )
ax-pre-ltwlin 7924 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( A  <RR  C  \/  C  <RR  B ) ) )
ax-pre-lttrn 7925 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-apti 7926 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  -.  ( A  <RR  B  \/  B  <RR  A ) )  ->  A  =  B )
ax-pre-ltadd 7927 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 7928 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-mulext 7929 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  x.  C
)  <RR  ( B  x.  C )  ->  ( A  <RR  B  \/  B  <RR  A ) ) )
ax-arch 7930 |-  ( A  e.  RR  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  (
y  +  1 )  e.  x ) } A  <RR  n )
ax-caucvg 7931 |-  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 7932 |-  ( ( ( 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 7933 |-  +  : ( CC 
X.  CC ) --> CC
ax-mulf 7934 |-  x.  : ( CC 
X.  CC ) --> CC
cpnf 7989 class +oo
cmnf 7990 class -oo
cxr 7991 class  RR*
clt 7992 class  <
cle 7993 class  <_
df-pnf 7994 |- +oo  =  ~P U. CC
df-mnf 7995 |- -oo  =  ~P +oo
df-xr 7996 |-  RR*  =  ( RR  u.  { +oo , -oo }
)
df-ltxr 7997 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { -oo } )  X. 
{ +oo } )  u.  ( { -oo }  X.  RR ) ) )
df-le 7998 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 8128 class  -
cneg 8129 class  -u A
df-sub 8130 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC  ( y  +  z )  =  x ) )
df-neg 8131 |-  -u A  =  (
0  -  A )
creap 8531 class #
df-reap 8532 |- #  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  ( x  <  y  \/  y  <  x ) ) }
cap 8538 class #
df-ap 8539 |- #  =  { <. 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 8629 class  /
df-div 8630 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC  ( y  x.  z
)  =  x ) )
cn 8919 class  NN
df-inn 8920 |-  NN  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
c2 8970 class  2
c3 8971 class  3
c4 8972 class  4
c5 8973 class  5
c6 8974 class  6
c7 8975 class  7
c8 8976 class  8
c9 8977 class  9
df-2 8978 |-  2  =  ( 1  +  1 )
df-3 8979 |-  3  =  ( 2  +  1 )
df-4 8980 |-  4  =  ( 3  +  1 )
df-5 8981 |-  5  =  ( 4  +  1 )
df-6 8982 |-  6  =  ( 5  +  1 )
df-7 8983 |-  7  =  ( 6  +  1 )
df-8 8984 |-  8  =  ( 7  +  1 )
df-9 8985 |-  9  =  ( 8  +  1 )
cn0 9176 class  NN0
df-n0 9177 |-  NN0  =  ( NN  u.  { 0 } )
cxnn0 9239 class NN0*
df-xnn0 9240 |- NN0* 
=  ( NN0  u.  { +oo } )
cz 9253 class  ZZ
df-z 9254 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 9384 class ; A B
df-dec 9385 |- ; A B  =  ( ( ( 9  +  1 )  x.  A )  +  B )
cuz 9528 class  ZZ>=
df-uz 9529 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 9619 class  QQ
df-q 9620 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 9653 class  RR+
df-rp 9654 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 9769 class  -e A
cxad 9770 class  +e
cxmu 9771 class  xe
df-xneg 9772 |-  -e A  =  if ( A  = +oo , -oo ,  if ( A  = -oo , +oo ,  -u A
) )
df-xadd 9773 |-  +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 9774 |-  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 9888 class  (,)
cioc 9889 class  (,]
cico 9890 class  [,)
cicc 9891 class  [,]
df-ioo 9892 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 9893 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 9894 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 9895 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 10008 class  ...
df-fz 10009 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 10142 class ..^
df-fzo 10143 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 10268 class  |_
cceil 10269 class
df-fl 10270 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ  ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
df-ceil 10271 |- =  ( x  e.  RR  |->  -u ( |_ `  -u x ) )
cmo 10322 class  mod
df-mod 10323 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 10445 class  seq M (  .+  ,  F )
df-seqfrec 10446 |- 
seq M (  .+  ,  F )  =  ran frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. )
cexp 10519 class  ^
df-exp 10520 |- 
^  =  ( 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 10705 class  !
df-fac 10706 |-  !  =  ( {
<. 0 ,  1
>. }  u.  seq 1
(  x.  ,  _I  ) )
cbc 10727 class  _C
df-bc 10728 |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n
)  /  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) ) ) ,  0 ) )
chash 10755 class
df-ihash 10756 |- =  ( (frec ( ( x  e.  ZZ  |->  ( x  +  1
) ) ,  0 )  u.  { <. om , +oo >. } )  o.  ( x  e. 
_V  |->  U. { y  e.  ( om  u.  { om } )  |  y  ~<_  x } ) )
cshi 10823 class  shift
df-shft 10824 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 10848 class  *
cre 10849 class  Re
cim 10850 class  Im
df-cj 10851 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC  ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 10852 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 10853 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqrt 11005 class  sqr
cabs 11006 class  abs
df-rsqrt 11007 |- 
sqr  =  ( x  e.  RR  |->  ( iota_ y  e.  RR  ( ( y ^ 2 )  =  x  /\  0  <_  y ) ) )
df-abs 11008 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
cli 11286 class  ~~>
df-clim 11287 |-  ~~>  =  { <. 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 11361 class  sum_ k  e.  A  B
df-sumdc 11362 |- 
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
) ) ) )
cprod 11558 class  prod_
k  e.  A  B
df-proddc 11559 |- 
prod_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( ( A 
C_  ( ZZ>= `  m
)  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A )  /\  ( E. n  e.  ( ZZ>=
`  m ) E. y ( y #  0  /\  seq n (  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  y )  /\  seq m (  x.  ,  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  1 ) ) )  ~~>  x ) )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  x.  , 
( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  1 ) ) ) `  m
) ) ) )
ce 11650 class  exp
ceu 11651 class  _e
csin 11652 class  sin
ccos 11653 class  cos
ctan 11654 class  tan
cpi 11655 class  pi
df-ef 11656 |-  exp  =  ( x  e.  CC  |->  sum_ k  e.  NN0  ( ( x ^
k )  /  ( ! `  k )
) )
df-e 11657 |-  _e  =  ( exp `  1 )
df-sin 11658 |- 
sin  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  -  ( exp `  ( -u _i  x.  x ) ) )  /  ( 2  x.  _i ) ) )
df-cos 11659 |- 
cos  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  +  ( exp `  ( -u _i  x.  x ) ) )  /  2 ) )
df-tan 11660 |- 
tan  =  ( x  e.  ( `' cos " ( CC  \  {
0 } ) ) 
|->  ( ( sin `  x
)  /  ( cos `  x ) ) )
df-pi 11661 |-  pi  = inf ( ( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  <  )
ctau 11782 class  tau
df-tau 11783 |- 
tau  = inf ( ( RR+  i^i  ( `' cos " { 1 } ) ) ,  RR ,  <  )
cdvds 11794 class  ||
df-dvds 11795 |- 
||  =  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
cgcd 11943 class  gcd
df-gcd 11944 |- 
gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
clcm 12060 class lcm
df-lcm 12061 |- lcm 
=  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 , inf ( { n  e.  NN  |  ( x  ||  n  /\  y  ||  n
) } ,  RR ,  <  ) ) )
cprime 12107 class  Prime
df-prm 12108 |- 
Prime  =  { p  e.  NN  |  { n  e.  NN  |  n  ||  p }  ~~  2o }
cnumer 12181 class numer
cdenom 12182 class denom
df-numer 12183 |- numer  =  ( y  e.  QQ  |->  ( 1st `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
df-denom 12184 |- denom  =  ( y  e.  QQ  |->  ( 2nd `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
codz 12208 class  odZ
cphi 12209 class  phi
df-odz 12210 |-  odZ  =  ( n  e.  NN  |->  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |-> inf ( { m  e.  NN  |  n  ||  ( ( x ^ m )  - 
1 ) } ,  RR ,  <  ) ) )
df-phi 12211 |- 
phi  =  ( n  e.  NN  |->  ( `  {
x  e.  ( 1 ... n )  |  ( x  gcd  n
)  =  1 } ) )
cpc 12284 class  pCnt
df-pc 12285 |-  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 12367 class  ZZ[_i]
df-gz 12368 |-  ZZ[_i]  =  { x  e.  CC  |  ( ( Re
`  x )  e.  ZZ  /\  ( Im
`  x )  e.  ZZ ) }
cstr 12458 class Struct
cnx 12459 class  ndx
csts 12460 class sSet
cslot 12461 class Slot  A
cbs 12462 class  Base
cress 12463 classs
df-struct 12464 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( f 
\  { (/) } )  /\  dom  f  C_  ( ... `  x ) ) }
df-ndx 12465 |- 
ndx  =  (  _I  |`  NN )
df-slot 12466 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
df-base 12468 |- 
Base  = Slot  1
df-sets 12469 |- sSet 
=  ( s  e. 
_V ,  e  e. 
_V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u.  { e } ) )
df-iress 12470 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  ( w sSet  <. ( Base `  ndx ) ,  ( x  i^i  ( Base `  w ) ) >.
) )
cplusg 12536 class  +g
cmulr 12537 class  .r
cstv 12538 class  *r
csca 12539 class Scalar
cvsca 12540 class  .s
cip 12541 class  .i
cts 12542 class TopSet
cple 12543 class  le
coc 12544 class  oc
cds 12545 class  dist
cunif 12546 class  UnifSet
chom 12547 class  Hom
cco 12548 class comp
df-plusg 12549 |- 
+g  = Slot  2
df-mulr 12550 |- 
.r  = Slot  3
df-starv 12551 |-  *r  = Slot  4
df-sca 12552 |- Scalar  = Slot  5
df-vsca 12553 |-  .s  = Slot  6
df-ip 12554 |-  .i  = Slot  8
df-tset 12555 |- TopSet  = Slot  9
df-ple 12556 |- 
le  = Slot ; 1 0
df-ocomp 12557 |-  oc  = Slot ; 1 1
df-ds 12558 |-  dist 
= Slot ; 1 2
df-unif 12559 |- 
UnifSet  = Slot ; 1 3
df-hom 12560 |- 
Hom  = Slot ; 1 4
df-cco 12561 |- comp 
= Slot ; 1 5
crest 12688 classt
ctopn 12689 class  TopOpen
df-rest 12690 |-t  =  ( j  e.  _V ,  x  e.  _V  |->  ran  ( y  e.  j 
|->  ( y  i^i  x
) ) )
df-topn 12691 |-  TopOpen  =  ( w  e. 
_V  |->  ( (TopSet `  w )t  ( Base `  w
) ) )
ctg 12703 class  topGen
cpt 12704 class  Xt_
c0g 12705 class  0g
cgsu 12706 class  gsumg
df-0g 12707 |-  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 12708 |- 
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 12709 |- 
topGen  =  ( x  e. 
_V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
df-pt 12710 |-  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 12714 class  X_s
cpws 12715 class  ^s
df-prds 12716 |-  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 12719 |- 
^s  =  ( r  e. 
_V ,  i  e. 
_V  |->  ( (Scalar `  r ) X_s ( i  X.  {
r } ) ) )
cimas 12720 class  "s
cqus 12721 class  /.s
cxps 12722 class  X.s
df-iimas 12723 |-  "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 ) ) >. } >. } )
df-qus 12724 |- 
/.s 
=  ( r  e. 
_V ,  e  e. 
_V  |->  ( ( x  e.  ( Base `  r
)  |->  [ x ]
e )  "s  r )
)
df-xps 12725 |- 
X.s 
=  ( r  e. 
_V ,  s  e. 
_V  |->  ( `' ( x  e.  ( Base `  r ) ,  y  e.  ( Base `  s
)  |->  { <. (/) ,  x >. ,  <. 1o ,  y
>. } )  "s  ( (Scalar `  r ) X_s { <. (/) ,  r >. ,  <. 1o ,  s
>. } ) ) )
cplusf 12772 class  +f
cmgm 12773 class Mgm
df-plusf 12774 |-  +f  =  ( g  e.  _V  |->  ( x  e.  ( Base `  g ) ,  y  e.  ( Base `  g
)  |->  ( x ( +g  `  g ) y ) ) )
df-mgm 12775 |- Mgm 
=  { g  | 
[. ( Base `  g
)  /  b ]. [. ( +g  `  g
)  /  o ]. A. x  e.  b  A. y  e.  b 
( x o y )  e.  b }
csgrp 12807 class Smgrp
df-sgrp 12808 |- Smgrp  =  { g  e. Mgm  |  [. ( Base `  g
)  /  b ]. [. ( +g  `  g
)  /  o ]. A. x  e.  b  A. y  e.  b  A. z  e.  b 
( ( x o y ) o z )  =  ( x o ( y o z ) ) }
cmnd 12817 class  Mnd
df-mnd 12818 |- 
Mnd  =  { g  e. Smgrp  |  [. ( Base `  g )  /  b ]. [. ( +g  `  g
)  /  p ]. E. e  e.  b  A. x  e.  b 
( ( e p x )  =  x  /\  ( x p e )  =  x ) }
cmhm 12849 class MndHom
csubmnd 12850 class SubMnd
df-mhm 12851 |- MndHom  =  ( s  e. 
Mnd ,  t  e.  Mnd  |->  { f  e.  ( ( Base `  t
)  ^m  ( Base `  s ) )  |  ( A. x  e.  ( Base `  s
) A. y  e.  ( Base `  s
) ( f `  ( x ( +g  `  s ) y ) )  =  ( ( f `  x ) ( +g  `  t
) ( f `  y ) )  /\  ( f `  ( 0g `  s ) )  =  ( 0g `  t ) ) } )
df-submnd 12852 |- SubMnd  =  ( s  e. 
Mnd  |->  { t  e. 
~P ( Base `  s
)  |  ( ( 0g `  s )  e.  t  /\  A. x  e.  t  A. y  e.  t  (
x ( +g  `  s
) y )  e.  t ) } )
cgrp 12877 class  Grp
cminusg 12878 class  invg
csg 12879 class  -g
df-grp 12880 |- 
Grp  =  { g  e.  Mnd  |  A. a  e.  ( Base `  g ) E. m  e.  ( Base `  g
) ( m ( +g  `  g ) a )  =  ( 0g `  g ) }
df-minusg 12881 |- 
invg  =  ( g  e.  _V  |->  ( x  e.  ( Base `  g )  |->  ( iota_ w  e.  ( Base `  g
) ( w ( +g  `  g ) x )  =  ( 0g `  g ) ) ) )
df-sbg 12882 |- 
-g  =  ( g  e.  _V  |->  ( x  e.  ( Base `  g
) ,  y  e.  ( Base `  g
)  |->  ( x ( +g  `  g ) ( ( invg `  g ) `  y
) ) ) )
cmg 12983 class .g
df-mulg 12984 |- .g  =  ( g  e.  _V  |->  ( n  e.  ZZ ,  x  e.  ( Base `  g )  |->  if ( n  =  0 ,  ( 0g `  g ) ,  [_  seq 1 ( ( +g  `  g ) ,  ( NN  X.  { x } ) )  / 
s ]_ if ( 0  <  n ,  ( s `  n ) ,  ( ( invg `  g ) `
 ( s `  -u n ) ) ) ) ) )
csubg 13027 class SubGrp
cnsg 13028 class NrmSGrp
cqg 13029 class ~QG
df-subg 13030 |- SubGrp  =  ( w  e. 
Grp  |->  { s  e. 
~P ( Base `  w
)  |  ( ws  s )  e.  Grp }
)
df-nsg 13031 |- NrmSGrp  =  ( w  e. 
Grp  |->  { s  e.  (SubGrp `  w )  |  [. ( Base `  w
)  /  b ]. [. ( +g  `  w
)  /  p ]. A. x  e.  b  A. y  e.  b 
( ( x p y )  e.  s  <-> 
( y p x )  e.  s ) } )
df-eqg 13032 |- ~QG  =  ( r  e.  _V ,  i  e.  _V  |->  { <. x ,  y
>.  |  ( {
x ,  y } 
C_  ( Base `  r
)  /\  ( (
( invg `  r ) `  x
) ( +g  `  r
) y )  e.  i ) } )
ccmn 13088 class CMnd
cabl 13089 class  Abel
df-cmn 13090 |- CMnd 
=  { g  e. 
Mnd  |  A. a  e.  ( Base `  g
) A. b  e.  ( Base `  g
) ( a ( +g  `  g ) b )  =  ( b ( +g  `  g
) a ) }
df-abl 13091 |- 
Abel  =  ( Grp  i^i CMnd
)
cmgp 13130 class mulGrp
df-mgp 13131 |- mulGrp  =  ( w  e. 
_V  |->  ( w sSet  <. ( +g  `  ndx ) ,  ( .r `  w ) >. )
)
cur 13142 class  1r
df-ur 13143 |-  1r  =  ( 0g  o. mulGrp )
csrg 13146 class SRing
df-srg 13147 |- SRing  =  { f  e. CMnd  | 
( (mulGrp `  f
)  e.  Mnd  /\  [. ( Base `  f
)  /  r ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. [. ( 0g `  f
)  /  n ]. A. x  e.  r 
( A. y  e.  r  A. z  e.  r  ( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) )  /\  (
( n t x )  =  n  /\  ( x t n )  =  n ) ) ) }
crg 13179 class  Ring
ccrg 13180 class  CRing
df-ring 13181 |- 
Ring  =  { f  e.  Grp  |  ( (mulGrp `  f )  e.  Mnd  /\ 
[. ( Base `  f
)  /  r ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. A. x  e.  r  A. y  e.  r  A. z  e.  r 
( ( x t ( y p z ) )  =  ( ( x t y ) p ( x t z ) )  /\  ( ( x p y ) t z )  =  ( ( x t z ) p ( y t z ) ) ) ) }
df-cring 13182 |- 
CRing  =  { f  e.  Ring  |  (mulGrp `  f )  e. CMnd }
coppr 13239 class oppr
df-oppr 13240 |- oppr  =  ( f  e.  _V  |->  ( f sSet  <. ( .r
`  ndx ) , tpos  ( .r `  f ) >.
) )
cdsr 13255 class  ||r
cui 13256 class Unit
cir 13257 class Irred
df-dvdsr 13258 |- 
||r 
=  ( w  e. 
_V  |->  { <. x ,  y >.  |  ( x  e.  ( Base `  w )  /\  E. z  e.  ( Base `  w ) ( z ( .r `  w
) x )  =  y ) } )
df-unit 13259 |- Unit 
=  ( w  e. 
_V  |->  ( `' ( ( ||r `
 w )  i^i  ( ||r `
 (oppr
`  w ) ) ) " { ( 1r `  w ) } ) )
df-irred 13260 |- Irred  =  ( w  e. 
_V  |->  [_ ( ( Base `  w )  \  (Unit `  w ) )  / 
b ]_ { z  e.  b  |  A. x  e.  b  A. y  e.  b  ( x
( .r `  w
) y )  =/=  z } )
cinvr 13289 class  invr
df-invr 13290 |- 
invr  =  ( r  e.  _V  |->  ( invg `  ( (mulGrp `  r
)s  (Unit `  r )
) ) )
cdvr 13300 class /r
df-dvr 13301 |- /r  =  ( r  e.  _V  |->  ( x  e.  ( Base `  r ) ,  y  e.  (Unit `  r )  |->  ( x ( .r `  r
) ( ( invr `  r ) `  y
) ) ) )
crh 13319 class RingHom
crs 13320 class RingIso
df-rnghom 13321 |- RingHom  =  ( r  e. 
Ring ,  s  e.  Ring  |-> 
[_ ( Base `  r
)  /  v ]_ [_ ( Base `  s
)  /  w ]_ { f  e.  ( w  ^m  v )  |  ( ( f `
 ( 1r `  r ) )  =  ( 1r `  s
)  /\  A. x  e.  v  A. y  e.  v  ( (
f `  ( x
( +g  `  r ) y ) )  =  ( ( f `  x ) ( +g  `  s ) ( f `
 y ) )  /\  ( f `  ( x ( .r
`  r ) y ) )  =  ( ( f `  x
) ( .r `  s ) ( f `
 y ) ) ) ) } )
df-rngiso 13322 |- RingIso  =  ( r  e. 
_V ,  s  e. 
_V  |->  { f  e.  ( r RingHom  s )  |  `' f  e.  ( s RingHom  r ) } )
cnzr 13323 class NzRing
df-nzr 13324 |- NzRing  =  { r  e.  Ring  |  ( 1r `  r
)  =/=  ( 0g
`  r ) }
clring 13331 class LRing
df-lring 13332 |- LRing  =  { r  e. NzRing  |  A. x  e.  ( Base `  r ) A. y  e.  ( Base `  r
) ( ( x ( +g  `  r
) y )  =  ( 1r `  r
)  ->  ( x  e.  (Unit `  r )  \/  y  e.  (Unit `  r ) ) ) }
csubrg 13338 class SubRing
crgspn 13339 class RingSpan
df-subrg 13340 |- SubRing  =  ( w  e. 
Ring  |->  { s  e. 
~P ( Base `  w
)  |  ( ( ws  s )  e.  Ring  /\  ( 1r `  w
)  e.  s ) } )
df-rgspn 13341 |- RingSpan  =  ( w  e. 
_V  |->  ( s  e. 
~P ( Base `  w
)  |->  |^| { t  e.  (SubRing `  w )  |  s  C_  t } ) )
capr 13370 class #r
df-apr 13371 |- #r  =  ( w  e.  _V  |->  { <. x ,  y
>.  |  ( (
x  e.  ( Base `  w )  /\  y  e.  ( Base `  w
) )  /\  (
x ( -g `  w
) y )  e.  (Unit `  w )
) } )
clmod 13377 class  LMod
cscaf 13378 class  .sf
df-lmod 13379 |- 
LMod  =  { g  e.  Grp  |  [. ( Base `  g )  / 
v ]. [. ( +g  `  g )  /  a ]. [. (Scalar `  g
)  /  f ]. [. ( .s `  g
)  /  s ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) ) }
df-scaf 13380 |-  .sf  =  ( g  e.  _V  |->  ( x  e.  ( Base `  (Scalar `  g )
) ,  y  e.  ( Base `  g
)  |->  ( x ( .s `  g ) y ) ) )
cpsmet 13442 class PsMet
cxmet 13443 class  *Met
cmet 13444 class  Met
cbl 13445 class  ball
cfbas 13446 class  fBas
cfg 13447 class  filGen
cmopn 13448 class  MetOpen
cmetu 13449 class metUnif
df-psmet 13450 |- 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 13451 |- 
*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 13452 |- 
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 13453 |-  ball 
=  ( d  e. 
_V  |->  ( x  e. 
dom  dom  d ,  z  e.  RR*  |->  { y  e.  dom  dom  d  |  ( x d y )  <  z } ) )
df-mopn 13454 |-  MetOpen  =  ( d  e. 
U. ran  *Met  |->  ( topGen `  ran  ( ball `  d ) ) )
df-fbas 13455 |- 
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 13456 |-  filGen  =  ( w  e. 
_V ,  x  e.  ( fBas `  w
)  |->  { y  e. 
~P w  |  ( x  i^i  ~P y
)  =/=  (/) } )
df-metu 13457 |- metUnif  =  ( d  e. 
U. ran PsMet  |->  ( ( dom  dom  d  X.  dom  dom  d ) filGen ran  (
a  e.  RR+  |->  ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 13458 classfld
df-icnfld 13459 |-fld  =  ( { <. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( *r `  ndx ) ,  * >. } )
czring 13483 classring
df-zring 13484 |-ring  =  (flds  ZZ )
ctop 13500 class  Top
df-top 13501 |- 
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 13513 class TopOn
df-topon 13514 |- TopOn  =  ( b  e. 
_V  |->  { j  e. 
Top  |  b  =  U. j } )
ctps 13533 class  TopSp
df-topsp 13534 |- 
TopSp  =  { f  |  ( TopOpen `  f
)  e.  (TopOn `  ( Base `  f )
) }
ctb 13545 class  TopBases
df-bases 13546 |-  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 13595 class  Clsd
cnt 13596 class  int
ccl 13597 class  cls
df-cld 13598 |- 
Clsd  =  ( j  e.  Top  |->  { x  e. 
~P U. j  |  ( U. j  \  x
)  e.  j } )
df-ntr 13599 |- 
int  =  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) ) )
df-cls 13600 |- 
cls  =  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
|^| { y  e.  (
Clsd `  j )  |  x  C_  y } ) )
cnei 13641 class  nei
df-nei 13642 |- 
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 13688 class  Cn
ccnp 13689 class  CnP
clm 13690 class  ~~> t
df-cn 13691 |-  Cn  =  ( j  e.  Top ,  k  e. 
Top  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  ( `' f " y
)  e.  j } )
df-cnp 13692 |- 
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 13693 |-  ~~> 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 13755 class  tX
df-tx 13756 |-  tX  =  ( r  e. 
_V ,  s  e. 
_V  |->  ( topGen `  ran  ( x  e.  r ,  y  e.  s  |->  ( x  X.  y
) ) ) )
chmeo 13803 class  Homeo
df-hmeo 13804 |- 
Homeo  =  ( j  e.  Top ,  k  e. 
Top  |->  { f  e.  ( j  Cn  k
)  |  `' f  e.  ( k  Cn  j ) } )
cxms 13839 class  *MetSp
cms 13840 class  MetSp
ctms 13841 class toMetSp
df-xms 13842 |- 
*MetSp  =  { f  e.  TopSp  |  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) ) }
df-ms 13843 |-  MetSp  =  { f  e.  *MetSp  |  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) )  e.  ( Met `  ( Base `  f ) ) }
df-tms 13844 |- toMetSp  =  ( d  e. 
U. ran  *Met  |->  ( { <. ( Base `  ndx ) ,  dom  dom  d >. ,  <. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
ccncf 14060 class  -cn->
df-cncf 14061 |- 
-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 14126 class lim CC
cdv 14127 class  _D
df-limced 14128 |- 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 14129 |- 
_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
) ) )
clog 14280 class  log
ccxp 14281 class  ^c
df-relog 14282 |- 
log  =  `' ( exp  |`  RR )
df-rpcxp 14283 |- 
^c  =  ( x  e.  RR+ ,  y  e.  CC  |->  ( exp `  ( y  x.  ( log `  x ) ) ) )
clogb 14364 class logb
df-logb 14365 |- logb  =  ( x  e.  ( CC  \  { 0 ,  1 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( ( log `  y )  /  ( log `  x
) ) )
clgs 14401 class  /L
df-lgs 14402 |- 
/L  =  ( a  e.  ZZ ,  n  e.  ZZ  |->  if ( n  =  0 ,  if ( ( a ^ 2 )  =  1 ,  1 ,  0 ) ,  ( if ( ( n  <  0  /\  a  <  0 ) ,  -u
1 ,  1 )  x.  (  seq 1
(  x.  ,  ( m  e.  NN  |->  if ( m  e.  Prime ,  ( if ( m  =  2 ,  if ( 2  ||  a ,  0 ,  if ( ( a  mod  8 )  e.  {
1 ,  7 } ,  1 ,  -u
1 ) ) ,  ( ( ( ( a ^ ( ( m  -  1 )  /  2 ) )  +  1 )  mod  m )  -  1 ) ) ^ (
m  pCnt  n )
) ,  1 ) ) ) `  ( abs `  n ) ) ) ) )
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 14548 wff 
A DECIDin  B
df-dcin 14549 |-  ( A DECIDin  B 
<-> 
A. x  e.  B DECID  x  e.  A )
wbd 14567 wff BOUNDED  ph
ax-bd0 14568 |-  ( ph  <->  ps )   =>    |-  (BOUNDED  ph  -> BOUNDED  ps )
ax-bdim 14569 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  ->  ps )
ax-bdan 14570 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  /\  ps )
ax-bdor 14571 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  \/  ps )
ax-bdn 14572 |- BOUNDED  ph   =>    |- BOUNDED  -.  ph
ax-bdal 14573 |- BOUNDED  ph   =>    |- BOUNDED  A. x  e.  y 
ph
ax-bdex 14574 |- BOUNDED  ph   =>    |- BOUNDED  E. x  e.  y 
ph
ax-bdeq 14575 |- BOUNDED  x  =  y
ax-bdel 14576 |- BOUNDED  x  e.  y
ax-bdsb 14577 |- BOUNDED  ph   =>    |- BOUNDED  [ y  /  x ] ph
wbdc 14595 wff BOUNDED  A
df-bdc 14596 |-  (BOUNDED  A 
<-> 
A. xBOUNDED  x  e.  A )
ax-bdsep 14639 |- BOUNDED  ph   =>    |-  A. a E. b A. x
( x  e.  b  <-> 
( x  e.  a  /\  ph ) )
ax-bj-d0cl 14679 |- BOUNDED  ph   =>    |- DECID  ph
wind 14681 wff Ind  A
df-bj-ind 14682 |-  (Ind  A  <->  ( (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A ) )
ax-infvn 14696 |- 
E. x (Ind  x  /\  A. y (Ind  y  ->  x  C_  y
) )
ax-bdsetind 14723 |- BOUNDED  ph   =>    |-  ( A. a ( A. y  e.  a  [ y  /  a ] ph  ->  ph )  ->  A. a ph )
ax-inf2 14731 |- 
E. a A. x
( x  e.  a  <-> 
( x  =  (/)  \/ 
E. y  e.  a  x  =  suc  y
) )
ax-strcoll 14737 |- 
A. a ( A. x  e.  a  E. y ph  ->  E. b
( A. x  e.  a  E. y  e.  b  ph  /\  A. y  e.  b  E. x  e.  a  ph ) )
ax-sscoll 14742 |- 
A. a A. b E. c A. z ( A. x  e.  a  E. y  e.  b 
ph  ->  E. d  e.  c  ( A. x  e.  a  E. y  e.  d  ph  /\  A. y  e.  d  E. x  e.  a  ph ) )
ax-ddkcomp 14744 |-  ( ( ( 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 14826 wff  A.! x ( ph  ->  ps )
walsc 14827 wff  A.! x  e.  A ph
df-alsi 14828 |-  ( A.! x (
ph  ->  ps )  <->  ( A. x ( ph  ->  ps )  /\  E. x ph ) )
df-alsc 14829 |-  ( A.! x  e.  A ph  <->  ( A. x  e.  A  ph  /\  E. x  x  e.  A
) )
  Copyright terms: Public domain W3C validator