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 2739 class  _V
df-v 2741 |-  _V  =  { x  |  x  =  x }
wcdeq 2947 wff CondEq ( x  =  y  ->  ph )
df-cdeq 2948 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 2964 wff  [. A  /  x ]. ph
df-sbc 2965 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 3059 class  [_ A  /  x ]_ B
df-csb 3060 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 3128 class  ( A  \  B )
cun 3129 class  ( A  u.  B )
cin 3130 class  ( A  i^i  B )
wss 3131 wff 
A  C_  B
df-dif 3133 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 3135 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 3137 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 3144 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
c0 3424 class  (/)
df-nul 3425 |-  (/)  =  ( _V  \  _V )
cif 3536 class  if ( ph ,  A ,  B )
df-if 3537 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3577 class  ~P A
df-pw 3579 |-  ~P A  =  {
x  |  x  C_  A }
csn 3594 class  { A }
cpr 3595 class  { A ,  B }
ctp 3596 class  { A ,  B ,  C }
cop 3597 class  <. A ,  B >.
cotp 3598 class  <. A ,  B ,  C >.
df-sn 3600 |-  { A }  =  {
x  |  x  =  A }
df-pr 3601 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3602 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3603 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3604 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 3811 class  U. A
df-uni 3812 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 3846 class  |^| A
df-int 3847 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 3888 class  U_ x  e.  A  B
ciin 3889 class  |^|_
x  e.  A  B
df-iun 3890 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 3891 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 3982 wff Disj  x  e.  A  B
df-disj 3983 |-  (Disj  x  e.  A  B 
<-> 
A. y E* x  e.  A  y  e.  B )
wbr 4005 wff 
A R B
df-br 4006 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 4065 class  {
<. x ,  y >.  |  ph }
cmpt 4066 class  ( x  e.  A  |->  B )
df-opab 4067 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 4068 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 4103 wff 
Tr  A
df-tr 4104 |-  ( Tr  A  <->  U. A  C_  A )
ax-coll 4120 |-  F/ b ph   =>    |-  ( A. x  e.  a  E. y ph  ->  E. b A. x  e.  a  E. y  e.  b  ph )
ax-sep 4123 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 4131 |- 
E. x A. y  -.  y  e.  x
ax-pow 4176 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
wem 4196 wff EXMID
df-exmid 4197 |-  (EXMID  <->  A. x ( x  C_  {
(/) }  -> DECID  (/)  e.  x ) )
ax-pr 4211 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4289 class  _E
cid 4290 class  _I
df-eprel 4291 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4295 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4296 wff 
R  Po  A
wor 4297 wff 
R  Or  A
df-po 4298 |-  ( 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 4299 |-  ( 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 4329 wff FrFor  R A S
wfr 4330 wff 
R  Fr  A
wse 4331 wff 
R Se  A
wwe 4332 wff 
R  We  A
df-frfor 4333 |-  (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 4334 |-  ( R  Fr  A  <->  A. sFrFor  R A s )
df-se 4335 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-wetr 4336 |-  ( 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 4364 wff 
Ord  A
con0 4365 class  On
wlim 4366 wff 
Lim  A
csuc 4367 class  suc 
A
df-iord 4368 |-  ( Ord  A  <->  ( Tr  A  /\  A. x  e.  A  Tr  x ) )
df-on 4370 |-  On  =  { x  |  Ord  x }
df-ilim 4371 |-  ( Lim  A  <->  ( Ord  A  /\  (/)  e.  A  /\  A  =  U. A ) )
df-suc 4373 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4435 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
ax-setind 4538 |-  ( A. a ( A. y  e.  a  [ y  /  a ] ph  ->  ph )  ->  A. a ph )
ax-iinf 4589 |- 
E. x ( (/)  e.  x  /\  A. y
( y  e.  x  ->  suc  y  e.  x
) )
com 4591 class  om
df-iom 4592 |- 
om  =  |^| { x  |  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
) }
cxp 4626 class  ( A  X.  B )
ccnv 4627 class  `' A
cdm 4628 class  dom 
A
crn 4629 class  ran 
A
cres 4630 class  ( A  |`  B )
cima 4631 class  ( A " B )
ccom 4632 class  ( A  o.  B )
wrel 4633 wff 
Rel  A
df-xp 4634 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4635 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4636 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4637 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4638 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4639 |-  ran  A  =  dom  `' A
df-res 4640 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4641 |-  ( A " B
)  =  ran  ( A  |`  B )
cio 5178 class  ( iota x ph )
df-iota 5180 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
wfun 5212 wff 
Fun  A
wfn 5213 wff 
A  Fn  B
wf 5214 wff 
F : A --> B
wf1 5215 wff 
F : A -1-1-> B
wfo 5216 wff 
F : A -onto-> B
wf1o 5217 wff 
F : A -1-1-onto-> B
cfv 5218 class  ( F `  A )
wiso 5219 wff 
H  Isom  R ,  S  ( A ,  B )
df-fun 5220 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 5221 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 5222 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 5223 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 5224 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 5225 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 5226 |-  ( F `  A )  =  ( iota x A F x )
df-isom 5227 |-  ( 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 5832 class  (
iota_ x  e.  A  ph )
df-riota 5833 |-  ( iota_ x  e.  A  ph )  =  ( iota
x ( x  e.  A  /\  ph )
)
co 5877 class  ( A F B )
coprab 5878 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpo 5879 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 5880 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 5881 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpo 5882 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 6083 class  oF R
cofr 6084 class  oR R
df-of 6085 |-  oF R  =  ( f  e.  _V ,  g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 6086 |-  oR R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 6141 class  1st
c2nd 6142 class  2nd
df-1st 6143 |- 
1st  =  ( x  e.  _V  |->  U. dom  { x } )
df-2nd 6144 |- 
2nd  =  ( x  e.  _V  |->  U. ran  { x } )
ctpos 6247 class tpos  F
df-tpos 6248 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
wsmo 6288 wff 
Smo  A
df-smo 6289 |-  ( 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 6307 class recs ( F )
df-recs 6308 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 6372 class  rec ( F ,  I
)
df-irdg 6373 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  ( I  u.  U_ x  e.  dom  g ( F `
 ( g `  x ) ) ) ) )
cfrec 6393 class frec ( F ,  I )
df-frec 6394 |- 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 6412 class  1o
c2o 6413 class  2o
c3o 6414 class  3o
c4o 6415 class  4o
coa 6416 class  +o
comu 6417 class  .o
coei 6418 classo
df-1o 6419 |-  1o  =  suc  (/)
df-2o 6420 |-  2o  =  suc  1o
df-3o 6421 |-  3o  =  suc  2o
df-4o 6422 |-  4o  =  suc  3o
df-oadd 6423 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6424 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexpi 6425 |-o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e.  _V  |->  ( z  .o  x ) ) ,  1o ) `  y ) )
wer 6534 wff 
R  Er  A
cec 6535 class  [ A ] R
cqs 6536 class  ( A /. R )
df-er 6537 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6539 |-  [ A ] R  =  ( R " { A } )
df-qs 6543 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cmap 6650 class  ^m
cpm 6651 class  ^pm
df-map 6652 |- 
^m  =  ( x  e.  _V ,  y  e.  _V  |->  { f  |  f : y --> x } )
df-pm 6653 |-  ^pm  =  ( x  e. 
_V ,  y  e. 
_V  |->  { f  e. 
~P ( y  X.  x )  |  Fun  f } )
cixp 6700 class  X_ x  e.  A  B
df-ixp 6701 |-  X_ x  e.  A  B  =  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
cen 6740 class  ~~
cdom 6741 class  ~<_
cfn 6742 class  Fin
df-en 6743 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 6744 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-fin 6745 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
cfi 6969 class  fi
df-fi 6970 |-  fi  =  ( x  e.  _V  |->  { z  |  E. y  e.  ( ~P x  i^i  Fin ) z  =  |^| y } )
csup 6983 class  sup ( A ,  B ,  R )
cinf 6984 class inf ( A ,  B ,  R )
df-sup 6985 |- 
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 6986 |- inf ( A ,  B ,  R )  =  sup ( A ,  B ,  `' R )
cdju 7038 class  ( A B )
df-dju 7039 |-  ( A B )  =  ( ( {
(/) }  X.  A
)  u.  ( { 1o }  X.  B
) )
cinl 7046 class inl
cinr 7047 class inr
df-inl 7048 |- inl 
=  ( x  e. 
_V  |->  <. (/) ,  x >. )
df-inr 7049 |- inr 
=  ( x  e. 
_V  |->  <. 1o ,  x >. )
cdjucase 7084 class case ( R ,  S )
df-case 7085 |- case
( R ,  S
)  =  ( ( R  o.  `'inl )  u.  ( S  o.  `'inr ) )
cdjud 7103 class  ( R ⊔d  S )
df-djud 7104 |-  ( R ⊔d  S )  =  ( ( R  o.  `' (inl  |`  dom  R
) )  u.  ( S  o.  `' (inr  |` 
dom  S ) ) )
xnninf 7120 class
df-nninf 7121 |-  =  { f  e.  ( 2o  ^m  om )  |  A. i  e.  om  ( f `  suc  i )  C_  (
f `  i ) }
comni 7134 class Omni
df-omni 7135 |- Omni 
=  { y  | 
A. f ( f : y --> 2o  ->  ( E. x  e.  y  ( f `  x
)  =  (/)  \/  A. x  e.  y  (
f `  x )  =  1o ) ) }
cmarkov 7151 class Markov
df-markov 7152 |- Markov  =  { y  |  A. f ( f : y --> 2o  ->  ( -.  A. x  e.  y  ( f `  x
)  =  1o  ->  E. x  e.  y  ( f `  x )  =  (/) ) ) }
cwomni 7163 class WOmni
df-womni 7164 |- WOmni  =  { y  |  A. f ( f : y --> 2o  -> DECID  A. x  e.  y  ( f `  x
)  =  1o ) }
ccrd 7180 class  card
df-card 7181 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
wac 7206 wff CHOICE
df-ac 7207 |-  (CHOICE  <->  A. x E. f ( f  C_  x  /\  f  Fn  dom  x ) )
wap 7248 wff 
R Ap  A
df-pap 7249 |-  ( 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 7250 wff 
R TAp  A
df-tap 7251 |-  ( R TAp  A  <->  ( R Ap  A  /\  A. x  e.  A  A. y  e.  A  ( -.  x R y  ->  x  =  y ) ) )
wacc 7263 wff CCHOICE
df-cc 7264 |-  (CCHOICE  <->  A. x ( dom  x  ~~  om  ->  E. f
( f  C_  x  /\  f  Fn  dom  x ) ) )
cnpi 7273 class  N.
cpli 7274 class  +N
cmi 7275 class  .N
clti 7276 class  <N
cplpq 7277 class  +pQ
cmpq 7278 class  .pQ
cltpq 7279 class  <pQ
ceq 7280 class  ~Q
cnq 7281 class  Q.
c1q 7282 class  1Q
cplq 7283 class  +Q
cmq 7284 class  .Q
crq 7285 class  *Q
cltq 7286 class  <Q
ceq0 7287 class ~Q0
cnq0 7288 class Q0
c0q0 7289 class 0Q0
cplq0 7290 class +Q0
cmq0 7291 class ·Q0
cnp 7292 class  P.
c1p 7293 class  1P
cpp 7294 class  +P.
cmp 7295 class  .P.
cltp 7296 class  <P
cer 7297 class  ~R
cnr 7298 class  R.
c0r 7299 class  0R
c1r 7300 class  1R
cm1r 7301 class  -1R
cplr 7302 class  +R
cmr 7303 class  .R
cltr 7304 class  <R
df-ni 7305 |-  N.  =  ( om  \  { (/) } )
df-pli 7306 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 7307 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 7308 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 7345 |- 
+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 7346 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 7347 |- 
<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 7348 |- 
~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 7349 |- 
Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
df-plqqs 7350 |- 
+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 7351 |- 
.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 7352 |-  1Q  =  [ <. 1o ,  1o >. ]  ~Q
df-rq 7353 |-  *Q  =  { <. x ,  y >.  |  ( x  e.  Q.  /\  y  e.  Q.  /\  (
x  .Q  y )  =  1Q ) }
df-ltnqqs 7354 |- 
<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 7425 |- ~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 7426 |- Q0  =  ( ( om  X.  N. ) /. ~Q0  )
df-0nq0 7427 |- 0Q0  =  [ <. (/) ,  1o >. ] ~Q0
df-plq0 7428 |- +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 7429 |- ·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 7467 |- 
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 7468 |-  1P  =  <. { l  |  l  <Q  1Q } ,  { u  |  1Q  <Q  u } >.
df-iplp 7469 |- 
+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 7470 |- 
.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 7471 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }
df-enr 7727 |- 
~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 7728 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 7729 |- 
+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 7730 |-  .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 7731 |- 
<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 7732 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 7733 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 7734 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 7811 class  CC
cr 7812 class  RR
cc0 7813 class  0
c1 7814 class  1
ci 7815 class  _i
caddc 7816 class  +
cltrr 7817 class  <RR
cmul 7818 class  x.
df-c 7819 |-  CC  =  ( R.  X.  R. )
df-0 7820 |-  0  =  <. 0R ,  0R >.
df-1 7821 |-  1  =  <. 1R ,  0R >.
df-i 7822 |-  _i  =  <. 0R ,  1R >.
df-r 7823 |-  RR  =  ( R.  X.  { 0R } )
df-add 7824 |-  +  =  { <. <.
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 7825 |-  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 7826 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 7904 |-  CC  e.  _V
ax-resscn 7905 |-  RR  C_  CC
ax-1cn 7906 |-  1  e.  CC
ax-1re 7907 |-  1  e.  RR
ax-icn 7908 |-  _i  e.  CC
ax-addcl 7909 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 7910 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 7911 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 7912 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-addcom 7913 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  =  ( B  +  A ) )
ax-mulcom 7914 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 7915 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 7916 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 7917 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 7918 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-0lt1 7919 |-  0  <RR  1
ax-1rid 7920 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-0id 7921 |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
ax-rnegex 7922 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-precex 7923 |-  ( ( A  e.  RR  /\  0  <RR  A )  ->  E. x  e.  RR  ( 0  <RR  x  /\  ( A  x.  x )  =  1 ) )
ax-cnre 7924 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-ltirr 7925 |-  ( A  e.  RR  ->  -.  A  <RR  A )
ax-pre-ltwlin 7926 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( A  <RR  C  \/  C  <RR  B ) ) )
ax-pre-lttrn 7927 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-apti 7928 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  -.  ( A  <RR  B  \/  B  <RR  A ) )  ->  A  =  B )
ax-pre-ltadd 7929 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 7930 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-mulext 7931 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  x.  C
)  <RR  ( B  x.  C )  ->  ( A  <RR  B  \/  B  <RR  A ) ) )
ax-arch 7932 |-  ( A  e.  RR  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  (
y  +  1 )  e.  x ) } A  <RR  n )
ax-caucvg 7933 |-  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 7934 |-  ( ( ( 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 7935 |-  +  : ( CC 
X.  CC ) --> CC
ax-mulf 7936 |-  x.  : ( CC 
X.  CC ) --> CC
cpnf 7991 class +oo
cmnf 7992 class -oo
cxr 7993 class  RR*
clt 7994 class  <
cle 7995 class  <_
df-pnf 7996 |- +oo  =  ~P U. CC
df-mnf 7997 |- -oo  =  ~P +oo
df-xr 7998 |-  RR*  =  ( RR  u.  { +oo , -oo }
)
df-ltxr 7999 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { -oo } )  X. 
{ +oo } )  u.  ( { -oo }  X.  RR ) ) )
df-le 8000 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 8130 class  -
cneg 8131 class  -u A
df-sub 8132 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC  ( y  +  z )  =  x ) )
df-neg 8133 |-  -u A  =  (
0  -  A )
creap 8533 class #
df-reap 8534 |- #  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  ( x  <  y  \/  y  <  x ) ) }
cap 8540 class #
df-ap 8541 |- #  =  { <. 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 8631 class  /
df-div 8632 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC  ( y  x.  z
)  =  x ) )
cn 8921 class  NN
df-inn 8922 |-  NN  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
c2 8972 class  2
c3 8973 class  3
c4 8974 class  4
c5 8975 class  5
c6 8976 class  6
c7 8977 class  7
c8 8978 class  8
c9 8979 class  9
df-2 8980 |-  2  =  ( 1  +  1 )
df-3 8981 |-  3  =  ( 2  +  1 )
df-4 8982 |-  4  =  ( 3  +  1 )
df-5 8983 |-  5  =  ( 4  +  1 )
df-6 8984 |-  6  =  ( 5  +  1 )
df-7 8985 |-  7  =  ( 6  +  1 )
df-8 8986 |-  8  =  ( 7  +  1 )
df-9 8987 |-  9  =  ( 8  +  1 )
cn0 9178 class  NN0
df-n0 9179 |-  NN0  =  ( NN  u.  { 0 } )
cxnn0 9241 class NN0*
df-xnn0 9242 |- NN0* 
=  ( NN0  u.  { +oo } )
cz 9255 class  ZZ
df-z 9256 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 9386 class ; A B
df-dec 9387 |- ; A B  =  ( ( ( 9  +  1 )  x.  A )  +  B )
cuz 9530 class  ZZ>=
df-uz 9531 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 9621 class  QQ
df-q 9622 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 9655 class  RR+
df-rp 9656 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 9771 class  -e A
cxad 9772 class  +e
cxmu 9773 class  xe
df-xneg 9774 |-  -e A  =  if ( A  = +oo , -oo ,  if ( A  = -oo , +oo ,  -u A
) )
df-xadd 9775 |-  +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 9776 |-  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 9890 class  (,)
cioc 9891 class  (,]
cico 9892 class  [,)
cicc 9893 class  [,]
df-ioo 9894 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 9895 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 9896 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 9897 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 10010 class  ...
df-fz 10011 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 10144 class ..^
df-fzo 10145 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 10270 class  |_
cceil 10271 class
df-fl 10272 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ  ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
df-ceil 10273 |- =  ( x  e.  RR  |->  -u ( |_ `  -u x ) )
cmo 10324 class  mod
df-mod 10325 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 10447 class  seq M (  .+  ,  F )
df-seqfrec 10448 |- 
seq M (  .+  ,  F )  =  ran frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. )
cexp 10521 class  ^
df-exp 10522 |- 
^  =  ( 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 10707 class  !
df-fac 10708 |-  !  =  ( {
<. 0 ,  1
>. }  u.  seq 1
(  x.  ,  _I  ) )
cbc 10729 class  _C
df-bc 10730 |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n
)  /  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) ) ) ,  0 ) )
chash 10757 class
df-ihash 10758 |- =  ( (frec ( ( x  e.  ZZ  |->  ( x  +  1
) ) ,  0 )  u.  { <. om , +oo >. } )  o.  ( x  e. 
_V  |->  U. { y  e.  ( om  u.  { om } )  |  y  ~<_  x } ) )
cshi 10825 class  shift
df-shft 10826 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 10850 class  *
cre 10851 class  Re
cim 10852 class  Im
df-cj 10853 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC  ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 10854 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 10855 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqrt 11007 class  sqr
cabs 11008 class  abs
df-rsqrt 11009 |- 
sqr  =  ( x  e.  RR  |->  ( iota_ y  e.  RR  ( ( y ^ 2 )  =  x  /\  0  <_  y ) ) )
df-abs 11010 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
cli 11288 class  ~~>
df-clim 11289 |-  ~~>  =  { <. 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 11363 class  sum_ k  e.  A  B
df-sumdc 11364 |- 
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 11560 class  prod_
k  e.  A  B
df-proddc 11561 |- 
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 11652 class  exp
ceu 11653 class  _e
csin 11654 class  sin
ccos 11655 class  cos
ctan 11656 class  tan
cpi 11657 class  pi
df-ef 11658 |-  exp  =  ( x  e.  CC  |->  sum_ k  e.  NN0  ( ( x ^
k )  /  ( ! `  k )
) )
df-e 11659 |-  _e  =  ( exp `  1 )
df-sin 11660 |- 
sin  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  -  ( exp `  ( -u _i  x.  x ) ) )  /  ( 2  x.  _i ) ) )
df-cos 11661 |- 
cos  =  ( x  e.  CC  |->  ( ( ( exp `  (
_i  x.  x )
)  +  ( exp `  ( -u _i  x.  x ) ) )  /  2 ) )
df-tan 11662 |- 
tan  =  ( x  e.  ( `' cos " ( CC  \  {
0 } ) ) 
|->  ( ( sin `  x
)  /  ( cos `  x ) ) )
df-pi 11663 |-  pi  = inf ( ( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  <  )
ctau 11784 class  tau
df-tau 11785 |- 
tau  = inf ( ( RR+  i^i  ( `' cos " { 1 } ) ) ,  RR ,  <  )
cdvds 11796 class  ||
df-dvds 11797 |- 
||  =  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
cgcd 11945 class  gcd
df-gcd 11946 |- 
gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
clcm 12062 class lcm
df-lcm 12063 |- lcm 
=  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 , inf ( { n  e.  NN  |  ( x  ||  n  /\  y  ||  n
) } ,  RR ,  <  ) ) )
cprime 12109 class  Prime
df-prm 12110 |- 
Prime  =  { p  e.  NN  |  { n  e.  NN  |  n  ||  p }  ~~  2o }
cnumer 12183 class numer
cdenom 12184 class denom
df-numer 12185 |- numer  =  ( y  e.  QQ  |->  ( 1st `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
df-denom 12186 |- denom  =  ( y  e.  QQ  |->  ( 2nd `  ( iota_ x  e.  ( ZZ 
X.  NN ) ( ( ( 1st `  x
)  gcd  ( 2nd `  x ) )  =  1  /\  y  =  ( ( 1st `  x
)  /  ( 2nd `  x ) ) ) ) ) )
codz 12210 class  odZ
cphi 12211 class  phi
df-odz 12212 |-  odZ  =  ( n  e.  NN  |->  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |-> inf ( { m  e.  NN  |  n  ||  ( ( x ^ m )  - 
1 ) } ,  RR ,  <  ) ) )
df-phi 12213 |- 
phi  =  ( n  e.  NN  |->  ( `  {
x  e.  ( 1 ... n )  |  ( x  gcd  n
)  =  1 } ) )
cpc 12286 class  pCnt
df-pc 12287 |-  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 12369 class  ZZ[_i]
df-gz 12370 |-  ZZ[_i]  =  { x  e.  CC  |  ( ( Re
`  x )  e.  ZZ  /\  ( Im
`  x )  e.  ZZ ) }
cstr 12460 class Struct
cnx 12461 class  ndx
csts 12462 class sSet
cslot 12463 class Slot  A
cbs 12464 class  Base
cress 12465 classs
df-struct 12466 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( f 
\  { (/) } )  /\  dom  f  C_  ( ... `  x ) ) }
df-ndx 12467 |- 
ndx  =  (  _I  |`  NN )
df-slot 12468 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
df-base 12470 |- 
Base  = Slot  1
df-sets 12471 |- sSet 
=  ( s  e. 
_V ,  e  e. 
_V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u.  { e } ) )
df-iress 12472 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  ( w sSet  <. ( Base `  ndx ) ,  ( x  i^i  ( Base `  w ) ) >.
) )
cplusg 12538 class  +g
cmulr 12539 class  .r
cstv 12540 class  *r
csca 12541 class Scalar
cvsca 12542 class  .s
cip 12543 class  .i
cts 12544 class TopSet
cple 12545 class  le
coc 12546 class  oc
cds 12547 class  dist
cunif 12548 class  UnifSet
chom 12549 class  Hom
cco 12550 class comp
df-plusg 12551 |- 
+g  = Slot  2
df-mulr 12552 |- 
.r  = Slot  3
df-starv 12553 |-  *r  = Slot  4
df-sca 12554 |- Scalar  = Slot  5
df-vsca 12555 |-  .s  = Slot  6
df-ip 12556 |-  .i  = Slot  8
df-tset 12557 |- TopSet  = Slot  9
df-ple 12558 |- 
le  = Slot ; 1 0
df-ocomp 12559 |-  oc  = Slot ; 1 1
df-ds 12560 |-  dist 
= Slot ; 1 2
df-unif 12561 |- 
UnifSet  = Slot ; 1 3
df-hom 12562 |- 
Hom  = Slot ; 1 4
df-cco 12563 |- comp 
= Slot ; 1 5
crest 12693 classt
ctopn 12694 class  TopOpen
df-rest 12695 |-t  =  ( j  e.  _V ,  x  e.  _V  |->  ran  ( y  e.  j 
|->  ( y  i^i  x
) ) )
df-topn 12696 |-  TopOpen  =  ( w  e. 
_V  |->  ( (TopSet `  w )t  ( Base `  w
) ) )
ctg 12708 class  topGen
cpt 12709 class  Xt_
c0g 12710 class  0g
cgsu 12711 class  gsumg
df-0g 12712 |-  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 12713 |- 
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 12714 |- 
topGen  =  ( x  e. 
_V  |->  { y  |  y  C_  U. (
x  i^i  ~P y
) } )
df-pt 12715 |-  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 12719 class  X_s
cpws 12720 class  ^s
df-prds 12721 |-  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 12724 |- 
^s  =  ( r  e. 
_V ,  i  e. 
_V  |->  ( (Scalar `  r ) X_s ( i  X.  {
r } ) ) )
cimas 12725 class  "s
cqus 12726 class  /.s
cxps 12727 class  X.s
df-iimas 12728 |-  "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 12729 |- 
/.s 
=  ( r  e. 
_V ,  e  e. 
_V  |->  ( ( x  e.  ( Base `  r
)  |->  [ x ]
e )  "s  r )
)
df-xps 12730 |- 
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 12777 class  +f
cmgm 12778 class Mgm
df-plusf 12779 |-  +f  =  ( g  e.  _V  |->  ( x  e.  ( Base `  g ) ,  y  e.  ( Base `  g
)  |->  ( x ( +g  `  g ) y ) ) )
df-mgm 12780 |- Mgm 
=  { g  | 
[. ( Base `  g
)  /  b ]. [. ( +g  `  g
)  /  o ]. A. x  e.  b  A. y  e.  b 
( x o y )  e.  b }
csgrp 12812 class Smgrp
df-sgrp 12813 |- 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 12822 class  Mnd
df-mnd 12823 |- 
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 12854 class MndHom
csubmnd 12855 class SubMnd
df-mhm 12856 |- 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 12857 |- 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 12882 class  Grp
cminusg 12883 class  invg
csg 12884 class  -g
df-grp 12885 |- 
Grp  =  { g  e.  Mnd  |  A. a  e.  ( Base `  g ) E. m  e.  ( Base `  g
) ( m ( +g  `  g ) a )  =  ( 0g `  g ) }
df-minusg 12886 |- 
invg  =  ( g  e.  _V  |->  ( x  e.  ( Base `  g )  |->  ( iota_ w  e.  ( Base `  g
) ( w ( +g  `  g ) x )  =  ( 0g `  g ) ) ) )
df-sbg 12887 |- 
-g  =  ( g  e.  _V  |->  ( x  e.  ( Base `  g
) ,  y  e.  ( Base `  g
)  |->  ( x ( +g  `  g ) ( ( invg `  g ) `  y
) ) ) )
cmg 12988 class .g
df-mulg 12989 |- .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 13032 class SubGrp
cnsg 13033 class NrmSGrp
cqg 13034 class ~QG
df-subg 13035 |- SubGrp  =  ( w  e. 
Grp  |->  { s  e. 
~P ( Base `  w
)  |  ( ws  s )  e.  Grp }
)
df-nsg 13036 |- 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 13037 |- ~QG  =  ( r  e.  _V ,  i  e.  _V  |->  { <. x ,  y
>.  |  ( {
x ,  y } 
C_  ( Base `  r
)  /\  ( (
( invg `  r ) `  x
) ( +g  `  r
) y )  e.  i ) } )
ccmn 13093 class CMnd
cabl 13094 class  Abel
df-cmn 13095 |- CMnd 
=  { g  e. 
Mnd  |  A. a  e.  ( Base `  g
) A. b  e.  ( Base `  g
) ( a ( +g  `  g ) b )  =  ( b ( +g  `  g
) a ) }
df-abl 13096 |- 
Abel  =  ( Grp  i^i CMnd
)
cmgp 13135 class mulGrp
df-mgp 13136 |- mulGrp  =  ( w  e. 
_V  |->  ( w sSet  <. ( +g  `  ndx ) ,  ( .r `  w ) >. )
)
cur 13147 class  1r
df-ur 13148 |-  1r  =  ( 0g  o. mulGrp )
csrg 13151 class SRing
df-srg 13152 |- 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 13184 class  Ring
ccrg 13185 class  CRing
df-ring 13186 |- 
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 13187 |- 
CRing  =  { f  e.  Ring  |  (mulGrp `  f )  e. CMnd }
coppr 13244 class oppr
df-oppr 13245 |- oppr  =  ( f  e.  _V  |->  ( f sSet  <. ( .r
`  ndx ) , tpos  ( .r `  f ) >.
) )
cdsr 13260 class  ||r
cui 13261 class Unit
cir 13262 class Irred
df-dvdsr 13263 |- 
||r 
=  ( w  e. 
_V  |->  { <. x ,  y >.  |  ( x  e.  ( Base `  w )  /\  E. z  e.  ( Base `  w ) ( z ( .r `  w
) x )  =  y ) } )
df-unit 13264 |- Unit 
=  ( w  e. 
_V  |->  ( `' ( ( ||r `
 w )  i^i  ( ||r `
 (oppr
`  w ) ) ) " { ( 1r `  w ) } ) )
df-irred 13265 |- 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 13294 class  invr
df-invr 13295 |- 
invr  =  ( r  e.  _V  |->  ( invg `  ( (mulGrp `  r
)s  (Unit `  r )
) ) )
cdvr 13305 class /r
df-dvr 13306 |- /r  =  ( r  e.  _V  |->  ( x  e.  ( Base `  r ) ,  y  e.  (Unit `  r )  |->  ( x ( .r `  r
) ( ( invr `  r ) `  y
) ) ) )
crh 13324 class RingHom
crs 13325 class RingIso
df-rnghom 13326 |- 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 13327 |- RingIso  =  ( r  e. 
_V ,  s  e. 
_V  |->  { f  e.  ( r RingHom  s )  |  `' f  e.  ( s RingHom  r ) } )
cnzr 13328 class NzRing
df-nzr 13329 |- NzRing  =  { r  e.  Ring  |  ( 1r `  r
)  =/=  ( 0g
`  r ) }
clring 13336 class LRing
df-lring 13337 |- 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 13343 class SubRing
crgspn 13344 class RingSpan
df-subrg 13345 |- SubRing  =  ( w  e. 
Ring  |->  { s  e. 
~P ( Base `  w
)  |  ( ( ws  s )  e.  Ring  /\  ( 1r `  w
)  e.  s ) } )
df-rgspn 13346 |- RingSpan  =  ( w  e. 
_V  |->  ( s  e. 
~P ( Base `  w
)  |->  |^| { t  e.  (SubRing `  w )  |  s  C_  t } ) )
capr 13375 class #r
df-apr 13376 |- #r  =  ( w  e.  _V  |->  { <. x ,  y
>.  |  ( (
x  e.  ( Base `  w )  /\  y  e.  ( Base `  w
) )  /\  (
x ( -g `  w
) y )  e.  (Unit `  w )
) } )
clmod 13382 class  LMod
cscaf 13383 class  .sf
df-lmod 13384 |- 
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 13385 |-  .sf  =  ( g  e.  _V  |->  ( x  e.  ( Base `  (Scalar `  g )
) ,  y  e.  ( Base `  g
)  |->  ( x ( .s `  g ) y ) ) )
clss 13447 class  LSubSp
df-lssm 13448 |- 
LSubSp  =  ( w  e. 
_V  |->  { s  e. 
~P ( Base `  w
)  |  ( E. j  j  e.  s  /\  A. x  e.  ( Base `  (Scalar `  w ) ) A. a  e.  s  A. b  e.  s  (
( x ( .s
`  w ) a ) ( +g  `  w
) b )  e.  s ) } )
clspn 13478 class  LSpan
df-lsp 13479 |- 
LSpan  =  ( w  e.  _V  |->  ( s  e. 
~P ( Base `  w
)  |->  |^| { t  e.  ( LSubSp `  w )  |  s  C_  t } ) )
cpsmet 13524 class PsMet
cxmet 13525 class  *Met
cmet 13526 class  Met
cbl 13527 class  ball
cfbas 13528 class  fBas
cfg 13529 class  filGen
cmopn 13530 class  MetOpen
cmetu 13531 class metUnif
df-psmet 13532 |- 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 13533 |- 
*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 13534 |- 
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 13535 |-  ball 
=  ( d  e. 
_V  |->  ( x  e. 
dom  dom  d ,  z  e.  RR*  |->  { y  e.  dom  dom  d  |  ( x d y )  <  z } ) )
df-mopn 13536 |-  MetOpen  =  ( d  e. 
U. ran  *Met  |->  ( topGen `  ran  ( ball `  d ) ) )
df-fbas 13537 |- 
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 13538 |-  filGen  =  ( w  e. 
_V ,  x  e.  ( fBas `  w
)  |->  { y  e. 
~P w  |  ( x  i^i  ~P y
)  =/=  (/) } )
df-metu 13539 |- metUnif  =  ( d  e. 
U. ran PsMet  |->  ( ( dom  dom  d  X.  dom  dom  d ) filGen ran  (
a  e.  RR+  |->  ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 13540 classfld
df-icnfld 13541 |-fld  =  ( { <. ( Base `  ndx ) ,  CC >. ,  <. ( +g  `  ndx ) ,  +  >. ,  <. ( .r `  ndx ) ,  x.  >. }  u.  {
<. ( *r `  ndx ) ,  * >. } )
czring 13565 classring
df-zring 13566 |-ring  =  (flds  ZZ )
ctop 13582 class  Top
df-top 13583 |- 
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 13595 class TopOn
df-topon 13596 |- TopOn  =  ( b  e. 
_V  |->  { j  e. 
Top  |  b  =  U. j } )
ctps 13615 class  TopSp
df-topsp 13616 |- 
TopSp  =  { f  |  ( TopOpen `  f
)  e.  (TopOn `  ( Base `  f )
) }
ctb 13627 class  TopBases
df-bases 13628 |-  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 13677 class  Clsd
cnt 13678 class  int
ccl 13679 class  cls
df-cld 13680 |- 
Clsd  =  ( j  e.  Top  |->  { x  e. 
~P U. j  |  ( U. j  \  x
)  e.  j } )
df-ntr 13681 |- 
int  =  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
U. ( j  i^i 
~P x ) ) )
df-cls 13682 |- 
cls  =  ( j  e.  Top  |->  ( x  e.  ~P U. j  |-> 
|^| { y  e.  (
Clsd `  j )  |  x  C_  y } ) )
cnei 13723 class  nei
df-nei 13724 |- 
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 13770 class  Cn
ccnp 13771 class  CnP
clm 13772 class  ~~> t
df-cn 13773 |-  Cn  =  ( j  e.  Top ,  k  e. 
Top  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  ( `' f " y
)  e.  j } )
df-cnp 13774 |- 
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 13775 |-  ~~> 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 13837 class  tX
df-tx 13838 |-  tX  =  ( r  e. 
_V ,  s  e. 
_V  |->  ( topGen `  ran  ( x  e.  r ,  y  e.  s  |->  ( x  X.  y
) ) ) )
chmeo 13885 class  Homeo
df-hmeo 13886 |- 
Homeo  =  ( j  e.  Top ,  k  e. 
Top  |->  { f  e.  ( j  Cn  k
)  |  `' f  e.  ( k  Cn  j ) } )
cxms 13921 class  *MetSp
cms 13922 class  MetSp
ctms 13923 class toMetSp
df-xms 13924 |- 
*MetSp  =  { f  e.  TopSp  |  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) ) }
df-ms 13925 |-  MetSp  =  { f  e.  *MetSp  |  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) )  e.  ( Met `  ( Base `  f ) ) }
df-tms 13926 |- toMetSp  =  ( d  e. 
U. ran  *Met  |->  ( { <. ( Base `  ndx ) ,  dom  dom  d >. ,  <. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
ccncf 14142 class  -cn->
df-cncf 14143 |- 
-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 14208 class lim CC
cdv 14209 class  _D
df-limced 14210 |- 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 14211 |- 
_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 14362 class  log
ccxp 14363 class  ^c
df-relog 14364 |- 
log  =  `' ( exp  |`  RR )
df-rpcxp 14365 |- 
^c  =  ( x  e.  RR+ ,  y  e.  CC  |->  ( exp `  ( y  x.  ( log `  x ) ) ) )
clogb 14446 class logb
df-logb 14447 |- logb  =  ( x  e.  ( CC  \  { 0 ,  1 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( ( log `  y )  /  ( log `  x
) ) )
clgs 14483 class  /L
df-lgs 14484 |- 
/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 14630 wff 
A DECIDin  B
df-dcin 14631 |-  ( A DECIDin  B 
<-> 
A. x  e.  B DECID  x  e.  A )
wbd 14649 wff BOUNDED  ph
ax-bd0 14650 |-  ( ph  <->  ps )   =>    |-  (BOUNDED  ph  -> BOUNDED  ps )
ax-bdim 14651 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  ->  ps )
ax-bdan 14652 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  /\  ps )
ax-bdor 14653 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  \/  ps )
ax-bdn 14654 |- BOUNDED  ph   =>    |- BOUNDED  -.  ph
ax-bdal 14655 |- BOUNDED  ph   =>    |- BOUNDED  A. x  e.  y 
ph
ax-bdex 14656 |- BOUNDED  ph   =>    |- BOUNDED  E. x  e.  y 
ph
ax-bdeq 14657 |- BOUNDED  x  =  y
ax-bdel 14658 |- BOUNDED  x  e.  y
ax-bdsb 14659 |- BOUNDED  ph   =>    |- BOUNDED  [ y  /  x ] ph
wbdc 14677 wff BOUNDED  A
df-bdc 14678 |-  (BOUNDED  A 
<-> 
A. xBOUNDED  x  e.  A )
ax-bdsep 14721 |- BOUNDED  ph   =>    |-  A. a E. b A. x
( x  e.  b  <-> 
( x  e.  a  /\  ph ) )
ax-bj-d0cl 14761 |- BOUNDED  ph   =>    |- DECID  ph
wind 14763 wff Ind  A
df-bj-ind 14764 |-  (Ind  A  <->  ( (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A ) )
ax-infvn 14778 |- 
E. x (Ind  x  /\  A. y (Ind  y  ->  x  C_  y
) )
ax-bdsetind 14805 |- BOUNDED  ph   =>    |-  ( A. a ( A. y  e.  a  [ y  /  a ] ph  ->  ph )  ->  A. a ph )
ax-inf2 14813 |- 
E. a A. x
( x  e.  a  <-> 
( x  =  (/)  \/ 
E. y  e.  a  x  =  suc  y
) )
ax-strcoll 14819 |- 
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 14824 |- 
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 14826 |-  ( ( ( 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 14909 wff  A.! x ( ph  ->  ps )
walsc 14910 wff  A.! x  e.  A ph
df-alsi 14911 |-  ( A.! x (
ph  ->  ps )  <->  ( A. x ( ph  ->  ps )  /\  E. x ph ) )
df-alsc 14912 |-  ( A.! x  e.  A ph  <->  ( A. x  e.  A  ph  /\  E. x  x  e.  A
) )
  Copyright terms: Public domain W3C validator