HomeHome Metamath Proof Explorer This is the GIF version.
Change to Unicode version
 
List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 2wff -. ph
wi 3wff (ph -> ps)
ax-1 4|- (ph -> (ps -> ph))
ax-2 5|- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))
ax-3 6|- ((-. ph -> -. ps) -> (ps -> ph))
ax-mp 7|- ph   &   |- (ph -> ps)   =>   |- ps
wb 144wff (ph <-> ps)
df-bi 145|- -. (((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph <-> ps)))
wo 220wff (ph \/ ps)
wa 221wff (ph /\ ps)
df-or 222|- ((ph \/ ps) <-> (-. ph -> ps))
df-an 223|- ((ph /\ ps) <-> -. (ph -> -. ps))
w3o 780wff (ph \/ ps \/ ch)
w3a 781wff (ph /\ ps /\ ch)
df-3or 782|- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
df-3an 783|- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
wnand 959wff (ph -/\ ps)
df-nand 960|- ((ph -/\ ps) <-> -. (ph /\ ps))
wal 990wff A.xph
cv 991class x
wceq 992wff A = B
wcel 994wff A e. B
ax-5 996|- (A.x(ph -> ps) -> (A.xph -> A.xps))
ax-6 997|- (-. A.xph -> A.x -. A.xph)
ax-7 998|- (A.xA.yph -> A.yA.xph)
ax-gen 999|- ph   =>   |- A.xph
ax-8 1000|- (x = y -> (x = z -> y = z))
ax-9 1001|- -. A.x -. x = y
ax-10 1002|- (A.x x = y -> A.y y = x)
ax-11 1003|- (x = y -> (A.yph -> A.x(x = y -> ph)))
ax-12 1004|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
ax-13 1005|- (x = y -> (x e. z -> y e. z))
ax-14 1006|- (x = y -> (z e. x -> z e. y))
ax-17 1007|- (ph -> A.xph)
ax-4 1009|- (A.xph -> ph)
ax-5o 1011|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
ax-6o 1014|- (-. A.x -. A.xph -> ph)
wex 1016wff E.xph
df-ex 1017|- (E.xph <-> -. A.x -. ph)
ax-9o 1159|- (A.x(x = y -> A.xph) -> ph)
ax-10o 1177|- (A.x x = y -> (A.xph -> A.yph))
wsbc 1207wff [A / x]ph
df-sb 1209|- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
ax-16 1247|- (A.x x = y -> (ph -> A.xph))
ax-11o 1255|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
ax-15 1399|- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
weu 1419wff E!xph
wmo 1420wff E*xph
df-eu 1421|- (E!xph <-> E.yA.x(ph <-> x = y))
df-mo 1422|- (E*xph <-> (E.xph -> E!xph))
ax-ext 1500|- (A.z(z e. x <-> z e. y) -> x = y)
cab 1505class {x | ph}
df-clab 1506|- (x e. {y | ph} <-> [x / y]ph)
df-cleq 1511|- (A.x(x e. y <-> x e. z) -> y = z)   =>   |- (A = B <-> A.x(x e. A <-> x e. B))
df-clel 1514|- (A e. B <-> E.x(x = A /\ x e. B))
wne 1628wff A =/= B
wnel 1629wff A e/ B
df-ne 1630|- (A =/= B <-> -. A = B)
df-nel 1631|- (A e/ B <-> -. A e. B)
wral 1691wff A.x e. A ph
wrex 1692wff E.x e. A ph
wreu 1693wff E!x e. A ph
crab 1694class {x e. A | ph}
df-ral 1695|- (A.x e. A ph <-> A.x(x e. A -> ph))
df-rex 1696|- (E.x e. A ph <-> E.x(x e. A /\ ph))
df-reu 1697|- (E!x e. A ph <-> E!x(x e. A /\ ph))
df-rab 1698|- {x e. A | ph} = {x | (x e. A /\ ph)}
cvv 1857class V
df-v 1858|- V = {x | x = x}
df-sbc 1987|- ([A / x]ph <-> A e. {x | ph})
csb 2051class [_A / x]_B
df-csb 2052|- [_A / x]_B = {y | [A / x]y e. B}
cdif 2096class (A \ B)
cun 2097class (A u. B)
cin 2098class (A i^i B)
wss 2099wff A (_ B
wpss 2100wff A (. B
df-dif 2101|- (A \ B) = {x | (x e. A /\ -. x e. B)}
df-un 2102|- (A u. B) = {x | (x e. A \/ x e. B)}
df-in 2103|- (A i^i B) = {x | (x e. A /\ x e. B)}
df-ss 2105|- (A (_ B <-> (A i^i B) = A)
df-pss 2107|- (A (. B <-> (A (_ B /\ A =/= B))
c0 2332class (/)
df-nul 2333|- (/) = (V \ V)
cif 2415class if(ph, A, B)
df-if 2416|- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
cpw 2458class P~A
df-pw 2459|- P~A = {x | x (_ A}
csn 2467class {A}
cpr 2468class {A, B}
cop 2469class <.A, B>.
df-sn 2470|- {A} = {x | x = A}
df-pr 2471|- {A, B} = ({A} u. {B})
ctp 2472class {A, B, C}
df-tp 2473|- {A, B, C} = ({A, B} u. {C})
df-op 2474|- <.A, B>. = {{A}, {A, B}}
cuni 2569class U.A
df-uni 2570|- U.A = {x | E.y(x e. y /\ y e. A)}
cint 2600class |^|A
df-int 2601|- |^|A = {x | A.y(y e. A -> x e. y)}
ciun 2633class U_x e. A B
ciin 2634class |^|_x e. A B
df-iun 2635|- U_x e. A B = {y | E.x e. A y e. B}
df-iin 2636|- |^|_x e. A B = {y | A.x e. A y e. B}
wbr 2692wff ARB
df-br 2693|- (ARB <-> <.A, B>. e. R)
copab 2740class {<.x, y>. | ph}
df-opab 2741|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}
wtr 2754wff Tr A
df-tr 2755|- (Tr A <-> U.A (_ A)
ax-rep 2767|- (A.wE.yA.z(A.yph -> z = y) -> E.yA.z(z e. y <-> E.w(w e. x /\ A.yph)))
ax-sep 2777|- E.yA.x(x e. y <-> (x e. z /\ ph))
ax-nul 2784|- E.xA.y -. y e. x
ax-pow 2818|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
ax-pr 2855|- E.zA.w((w = x \/ w = y) -> w e. z)
cep 2908class E
cid 2909class I
df-eprel 2910|- E = {<.x, y>. | x e. y}
df-id 2913|- I = {<.x, y>. | x = y}
wpo 2916wff R Po A
wor 2917wff R Or A
df-po 2918|- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
df-so 2929|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
wfr 2945wff R Fr A
wwe 2946wff R We A
df-fr 2947|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))
df-we 2962|- (R We A <-> (R Fr A /\ R Or A))
word 2974wff Ord A
con0 2975class On
wlim 2976wff Lim A
csuc 2977class suc A
df-ord 2978|- (Ord A <-> (Tr A /\ E We A))
df-on 2979|- On = {x | Ord x}
df-lim 2980|- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
df-suc 2981|- suc A = (A u. {A})
ax-un 3089|- E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)
com 3218class om
df-om 3219|- om = {x | (Ord x /\ A.y(Lim y -> x e. y))}
cxp 3249class (A X. B)
ccnv 3250class `'A
cdm 3251class dom A
crn 3252class ran A
cres 3253class (A |` B)
cima 3254class (A"B)
ccom 3255class (A o. B)
wrel 3256wff Rel A
wfun 3257wff Fun A
wfn 3258wff A Fn B
wf 3259wff F:A-->B
wf1 3260wff F:A-1-1->B
wfo 3261wff F:A-onto->B
wf1o 3262wff F:A-1-1-onto->B
cfv 3263class (F` A)
wiso 3264wff H Isom R, S (A, B)
df-xp 3265|- (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}
df-rel 3266|- (Rel A <-> A (_ (V X. V))
df-cnv 3267|- `'A = {<.x, y>. | yAx}
df-co 3268|- (A o. B) = {<.x, y>. | E.z(xBz /\ zAy)}
df-dm 3269|- dom A = {x | E.y xAy}
df-rn 3270|- ran A = dom `' A
df-res 3271|- (A |` B) = (A i^i (B X. V))
df-ima 3272|- (A"B) = ran ( A |` B)
df-fun 3273|- (Fun A <-> (Rel A /\ (A o. `'A) (_ I))
df-fn 3274|- (A Fn B <-> (Fun A /\ dom A = B))
df-f 3275|- (F:A-->B <-> (F Fn A /\ ran F (_ B))
df-f1 3276|- (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))
df-fo 3277|- (F:A-onto->B <-> (F Fn A /\ ran F = B))
df-f1o 3278|- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
df-fv 3279|- (F` A) = U.{x | (F"{A}) = {x}}
df-iso 3280|- (H Isom R, S (A, B) <-> (H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))
co 4021class (AFB)
copab2 4022class {<.<.x, y>., z>. | ph}
df-opr 4023|- (AFB) = (F` <.A, B>.)
df-oprab 4024|- {<.<.x, y>., z>. | ph} = {w | E.xE.yE.z(w = <.<.x, y>., z>. /\ ph)}
cmpt 4132class (x e. A |-> B)
cmpt2 4133class (x e. A, y e. B |-> C)
df-mpt 4134|- (x e. A |-> B) = {<.x, y>. | (x e. A /\ y = B)}
df-mpt2 4135|- (x e. A, y e. B |-> C) = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}
c1st 4138class 1st
c2nd 4139class 2nd
df-1st 4140|- 1st = {<.x, y>. | y = U.dom { x}}
df-2nd 4141|- 2nd = {<.x, y>. | y = U.ran { x}}
crdg 4232class rec(A, B)
df-rdg 4233|- rec(F, A) = U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y)))}
c1o 4264class 1o
c2o 4265class 2o
coa 4266class +o
comu 4267class .o
coe 4268class ^o
df-1o 4269|- 1o = suc (/)
df-2o 4270|- 2o = suc 1o
df-oadd 4271|- +o = {<.<.x, y>., z>. | ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = suc w}, x)` y))}
df-omul 4272|- .o = {<.<.x, y>., z>. | ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = (w +o x)}, (/))` y))}
df-oexp 4273|- ^o = {<.<.x, y>., z>. | ((x e. On /\ y e. On) /\ z = if(x = (/), (1o \ y), (rec({<.w, v>. | v = (w .o x)}, 1o)` y)))}
wer 4398wff Er R
cec 4399class [A]R
cqs 4400class (A/.R)
df-er 4401|- (Er R <-> (`'R u. (R o. R)) (_ R)
df-ec 4403|- [A]R = (R"{A})
df-qs 4406|- (A/.R) = {y | E.x e. A y = [x]R}
cm 4463class ^m
cpm 4464class ^pm
df-map 4465|- ^m = {<.<.x, y>., z>. | z = {f | f:y-->x}}
df-pm 4466|- ^pm = {<.<.x, y>., z>. | z = {f | (Fun f /\ f (_ (y X. x))}}
cixp 4488class X_x e. A B
df-ixp 4489|- X_x e. A B = {f | (f Fn A /\ A.x e. A (f` x) e. B)}
cen 4505class ~~
cdom 4506class ~<_
csdm 4507class ~<
cfn 4508class Fin
df-en 4509|- ~~ = {<.x, y>. | E.f f:x-1-1-onto->y}
df-dom 4510|- ~<_ = {<.x, y>. | E.f f:x-1-1->y}
df-sdom 4511|- ~< = ( ~<_ \ ~~ )
df-fin 4512|- Fin = {x | E.y e. om x ~~ y}
csup 4716class sup(A, B, R)
df-sup 4717|- sup(B, A, R) = U.{x e. A | (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))}
ax-reg 4736|- (E.y y e. x -> E.y(y e. x /\ A.z(z e. y -> -. z e. x)))
ax-inf 4767|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))
ax-inf2 4770|- E.x(E.y(y e. x /\ A.z -. z e. y) /\ A.y(y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))))
cr1 4787class R1
crnk 4788class rank
df-r1 4789|- R1 = rec({<.x, y>. | y = P~x}, (/))
df-rank 4790|- rank = {<.x, y>. | y = |^|{z e. On | x e. (R1` suc z)}}
ax-ac 4890|- E.yA.zA.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v))
ccrd 4959class card
cale 4960class aleph
ccf 4961class cf
df-card 4962|- card = {<.x, y>. | y = |^|{z e. On | z ~~ x}}
df-aleph 4963|- aleph = rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)
df-cf 4964|- cf = {<.x, y>. | (x e. On /\ y = |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))})}
ccda 5067class +c
df-cda 5068|- +c = {<.<.x, y>., z>. | z = ((x X. {(/)}) u. (y X. {1o}))}
cnpi 5126class N.
cpli 5127class +N
cmi 5128class .N
clti 5129class <N
cplpq 5130class +pQ
cmpq 5131class .pQ
ceq 5132class ~Q
cnq 5133class Q.
c1q 5134class 1Q
cplq 5135class +Q
cmq 5136class .Q
crq 5137class *Q
cltq 5138class <Q
cnp 5139class P.
c1p 5140class 1P
cpp 5141class +P.
cmp 5142class .P.
cltp 5143class <P
cplpr 5144class +pR
cmpr 5145class .pR
cer 5146class ~R
cnr 5147class R.
c0r 5148class 0R
c1r 5149class 1R
cm1r 5150class -1R
cplr 5151class +R
cmr 5152class .R
cltr 5153class <R
df-ni 5154|- N. = (om \ {(/)})
df-pli 5155|- +N = ( +o |` (N. X. N.))
df-mi 5156|- .N = ( .o |` (N. X. N.))
df-lti 5157|- <N = (E i^i (N. X. N.))
df-plpq 5189|- +pQ = {<.<.x, y>., z>. | ((x e. (N. X. N.) /\ y e. (N. X. N.)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.))}
df-mpq 5190|- .pQ = {<.<.x, y>., z>. | ((x e. (N. X. N.) /\ y e. (N. X. N.)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w .N u), (v .N f)>.))}
df-enq 5191|- ~Q = {<.x, y>. | ((x e. (N. X. N.) /\ y e. (N. X. N.)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z .N u) = (w .N v)))}
df-nq 5192|- Q. = ((N. X. N.)/. ~Q )
df-plq 5193|- +Q = {<.<.x, y>., z>. | ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. +pQ <.u, f>.)] ~Q ))}
df-mq 5194|- .Q = {<.<.x, y>., z>. | ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q ))}
df-rq 5195|- *Q = {<.x, y>. | (x e. Q. /\ (x .Q y) = 1Q)}
df-ltq 5196|- <Q = {<.x, y>. | ((x e. Q. /\ y e. Q.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~Q /\ y = [<.v, u>.] ~Q ) /\ (z .N u) <N (w .N v)))}
df-1q 5197|- 1Q = [<.1o, 1o>.] ~Q
df-np 5240|- P. = {x | (((/) (. x /\ x (. Q.) /\ A.y e. x (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z))}
df-1p 5241|- 1P = {x | x <Q 1Q}
df-plp 5242|- +P. = {<.<.x, y>., z>. | ((x e. P. /\ y e. P.) /\ z = {w | E.v e. x E.u e. y w = (v +Q u)})}
df-mp 5243|- .P. = {<.<.x, y>., z>. | ((x e. P. /\ y e. P.) /\ z = {w | E.v e. x E.u e. y w = (v .Q u)})}
df-ltp 5244|- <P = {<.x, y>. | ((x e. P. /\ y e. P.) /\ x (. y)}
df-plpr 5318|- +pR = {<.<.x, y>., z>. | ((x e. (P. X. P.) /\ y e. (P. X. P.)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +P. u), (v +P. f)>.))}
df-mpr 5319|- .pR = {<.<.x, y>., z>. | ((x e. (P. X. P.) /\ y e. (P. X. P.)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .P. u) +P. (v .P. f)), ((w .P. f) +P. (v .P. u))>.))}
df-enr 5320|- ~R = {<.x, y>. | ((x e. (P. X. P.) /\ y e. (P. X. P.)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (z +P. u) = (w +P. v)))}
df-nr 5321|- R. = ((P. X. P.)/. ~R )
df-plr 5322|- +R = {<.<.x, y>., z>. | ((x e. R. /\ y e. R.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. +pR <.u, f>.)] ~R ))}
df-mr 5323|- .R = {<.<.x, y>., z>. | ((x e. R. /\ y e. R.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R ))}
df-ltr 5324|- <R = {<.x, y>. | ((x e. R. /\ y e. R.) /\ E.zE.wE.vE.u((x = [<.z, w>.] ~R /\ y = [<.v, u>.] ~R ) /\ (z +P. u) <P (w +P. v)))}
df-0r 5325|- 0R = [<.1P, 1P>.] ~R
df-1r 5326|- 1R = [<.(1P +P. 1P), 1P>.] ~R
df-m1r 5327|- -1R = [<.1P, (1P +P. 1P)>.] ~R
cc 5386class CC
cr 5387class RR
cc0 5388class 0
c1 5389class 1
ci 5390class i
caddc 5391class +
cltrr 5392class <R
cmul 5393class x.
df-c 5394|- CC = (R. X. R.)
df-0 5395|- 0 = <.0R, 0R>.
df-1 5396|- 1 = <.1R, 0R>.
df-i 5397|- i = <.0R, 1R>.
df-r 5398|- RR = (R. X. {0R})
df-plus 5399|- + = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.))}
df-mul 5400|- x. = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.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 5401|- <R = {<.x, y>. | ((x e. RR /\ y e. RR) /\ E.zE.w((x = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w))}
cmin 5446class -
cneg 5447class -uA
cdiv 5448class /
cle 5449class <_
cn 5450class NN
cn0 5451class NN0
cz 5452class ZZ
cq 5453class QQ
crp 5454class RR+
df-sub 5510|- - = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ z = U.{w e. CC | (y + w) = x})}
df-neg 5512|- -uA = (0 - A)
cpnf 5637class +oo
cmnf 5638class -oo
cxr 5639class RR*
clt 5640class <
df-pnf 5641|- +oo = P~U.CC
df-mnf 5642|- -oo = P~ +oo
df-xr 5643|- RR* = (RR u. { +oo, -oo})
df-ltxr 5644|- < = ((( <R i^i (RR X. RR)) u. {<. -oo, +oo>.}) u. ((RR X. { +oo}) u. ({ -oo} X. RR)))
df-le 5645|- <_ = ((RR* X. RR*) \ `' < )
df-div 5855|- / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = U.{w e. CC | (y x. w) = x})}
df-n 6070|- NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
c2 6107class 2
c3 6108class 3
c4 6109class 4
c5 6110class 5
c6 6111class 6
c7 6112class 7
c8 6113class 8
c9 6114class 9
c10 6115class 10
df-2 6116|- 2 = (1 + 1)
df-3 6117|- 3 = (2 + 1)
df-4 6118|- 4 = (3 + 1)
df-5 6119|- 5 = (4 + 1)
df-6 6120|- 6 = (5 + 1)
df-7 6121|- 7 = (6 + 1)
df-8 6122|- 8 = (7 + 1)
df-9 6123|- 9 = (8 + 1)
df-10 6124|- 10 = (9 + 1)
df-rp 6191|- RR+ = {x e. RR | 0 < x}
df-n0 6268|- NN0 = (NN u. {0})
df-z 6304|- ZZ = {n e. RR | (n = 0 \/ n e. NN \/ -un e. NN)}
df-q 6395|- QQ = {x | E.m e. ZZ E.n e. NN x = (m / n)}
cfl 6421class |_
df-fl 6422|- |_ = {<.x, y>. | (x e. RR /\ y = U.{z e. ZZ | (z <_ x /\ x < (z + 1))})}
cmo 6458class mod
df-mod 6459|- mod = {<.<.x, y>., z>. | ((x e. RR /\ y e. RR+) /\ z = (x - (y x. (|_` (x / y)))))}
cioo 6483class (,)
cioc 6484class (,]
cico 6485class [,)
cicc 6486class [,]
df-ioo 6487|- (,) = {<.<.x, y>., z>. | ((x e. RR* /\ y e. RR*) /\ z = {w e. RR* | (x < w /\ w < y)})}
df-ioc 6488|- (,] = {<.<.x, y>., z>. | ((x e. RR* /\ y e. RR*) /\ z = {w e. RR* | (x < w /\ w <_ y)})}
df-ico 6489|- [,) = {<.<.x, y>., z>. | ((x e. RR* /\ y e. RR*) /\ z = {w e. RR* | (x <_ w /\ w < y)})}
df-icc 6490|- [,] = {<.<.x, y>., z>. | ((x e. RR* /\ y e. RR*) /\ z = {w e. RR* | (x <_ w /\ w <_ y)})}
cuz 6544class ZZ>=
df-uz 6545|- ZZ>= = {<.j, y>. | (j e. ZZ /\ y = {k e. ZZ | j <_ k})}
cfz 6595class ...
df-fz 6596|- ... = {<.<.m, n>., z>. | ((m e. ZZ /\ n e. ZZ) /\ z = {k e. ZZ | (m <_ k /\ k <_ n)})}
cseq1 6672class seq1
df-seq1 6673|- seq1 = {<.<.f, g>., h>. | h = {<.x, y>. | (x e. NN /\ y = (2nd` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om))` x)))}}
cshi 6705class shift
df-shft 6706|- shift = {<.<.f, x>., g>. | g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}}
clsp 6722class limsup
df-limsup 6723|- limsup = {<.x, y>. | y = sup({z | E.k e. ZZ z = sup(((x"(ZZ>=` k)) i^i RR*), RR*, < )}, RR*, `' < )}
cseqz 6726class seq
cseq0 6727class seq0
df-seqz 6728|- seq = {<.<.x, g>., h>. | h = ((((2nd` x) seq1 (g shift (1 - (1st` x)))) shift ((1st` x) - 1)) |` {k e. ZZ | (1st` x) <_ k})}
df-seq0 6729|- seq0 = {<.<.f, g>., h>. | h = (((f seq1 (g shift 1)) shift -u1) |` NN0)}
cexp 6763class ^
df-exp 6764|- ^ = {<.<.x, y>., z>. | ((x e. CC /\ y e. NN0) /\ z = if(y = 0, 1, (( x. seq1 (NN X. {x}))` y)))}
csqr 6870class sqr
df-sqr 6871|- sqr = {<.x, y>. | ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))}
cre 6948class Re
cim 6949class Im
ccj 6950class *
cabs 6951class abs
df-re 6952|- Re = {<.x, y>. | (x e. CC /\ y = U.{z e. RR | E.w e. RR x = (z + (i x. w))})}
df-im 6953|- Im = {<.x, y>. | (x e. CC /\ y = U.{w e. RR | E.z e. RR x = (z + (i x. w))})}
df-cj 6954|- * = {<.x, y>. | (x e. CC /\ y = ((Re` x) - (i x. (Im` x))))}
df-abs 6955|- abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}
cfa 7134class !
df-fac 7135|- ! = ({<.0, 1>.} u. ( x. seq1 (I |` NN)))
cbc 7159class C.
df-bc 7160|- C. = {<.<.n, k>., m>. | ((n e. NN0 /\ k e. ZZ) /\ m = if((0 <_ k /\ k <_ n), ((!` n) / ((!` (n - k)) x. (!` k))), 0))}
cli 7177class ~~>
df-clim 7178|- ~~> = {<.f, y>. | (y e. CC /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. CC /\ (abs` ((f` k) - y)) < x))))}
csu 7182class sum_k e. A B
df-sum 7183|- sum_k e. A B = ({x | E.mE.n e. (ZZ>=` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n))} u. U.{x | E.m e. ZZ (A = (ZZ>=` m) /\ (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x)})
ccncf 7467class -cn->
df-cncf 7468|- -cn-> = {<.<.a, b>., s>. | ((a (_ CC /\ b (_ CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})}
ce 7498class exp
ceu 7499class e
csin 7500class sin
ccos 7501class cos
cpi 7502class pi
df-ef 7503|- exp = {<.x, y>. | (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))}
df-e 7504|- e = (exp` 1)
df-sin 7505|- sin = {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i)))}
df-cos 7506|- cos = {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) + (exp` (-ui x. x))) / 2))}
df-pi 7507|- pi = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )
ctop 7800class Top
ctps 7801class TopSp
ctb 7802class Bases
ctg 7803class topGen
df-top 7804|- Top = {x | (A.y(y (_ x -> U.y e. x) /\ A.y e. x A.z e. x (y i^i z) e. x)}
df-topsp 7805|- TopSp = {<.x, y>. | (y e. Top /\ x = U.y)}
df-bases 7806|- Bases = {x | A.y e. x A.z e. x (y i^i z) (_ U.(x i^i P~(y i^i z))}
df-topgen 7807|- topGen = {<.x, y>. | (x e. Bases /\ y = {z | z (_ U.(x i^i P~z)})}
ccld 7870class Clsd
cnt 7871class int
ccl 7872class cls
df-cld 7873|- Clsd = {<.z, w>. | (z e. Top /\ w = {x | (x (_ U.z /\ (U.z \ x) e. z)})}
df-ntr 7874|- int = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = U.{v e. z | v (_ x})})}
df-cls 7875|- cls = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})})}
cnei 7922class nei
df-nei 7923|- nei = {<.j, y>. | (j e. Top /\ y = {<.z, v>. | (z (_ U.j /\ v = {w | (w (_ U.j /\ E.g e. j (z (_ g /\ g (_ w))})})}
clp 7950class limPt
df-lp 7951|- limPt = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})})}
ccn 7962class Cn
ccnp 7963class CnP
df-cn 7964|- Cn = {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {f e. (U.k ^m U.j) | A.y e. k (`'f"y) e. j})}
df-cnp 7965|- CnP = {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {<.x, y>. | (x e. U.j /\ y = {f e. (U.k ^m U.j) | A.w e. k ((f` x) e. w -> E.v e. j (x e. v /\ (f"v) (_ w))})})}
cha 7991class Haus
df-haus 7992|- Haus = {j e. Top | A.x e. U.jA.y e. U.j(x =/= y -> E.n e. j E.m e. j (x e. n /\ y e. m /\ (n i^i m) = (/)))}
cme 7999class Met
cmt 8000class MetSp
cbl 8001class ball
copn 8002class Open
df-met 8003|- Met = {x | E.y(x:(y X. y)-->RR /\ A.z e. y A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw))))}
df-ms 8004|- MetSp = {<.x, y>. | (y e. Met /\ x = dom dom y)}
df-bl 8005|- ball = {<.x, y>. | (x e. Met /\ y = {<.<.z, w>., v>. | ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))})}
df-opn 8006|- Open = {<.x, y>. | (x e. Met /\ y = {z | (z (_ dom dom x /\ A.w e. z E.v e. ran ( ball ` x)(w e. v /\ v (_ z))})}
clm 8130class ~~>m
cca 8131class Cau
cms 8132class CMet
df-lm 8133|- ~~>m = {<.z, w>. | (z e. Met /\ w = {<.f, y>. | (f (_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))})}
df-cau 8134|- Cau = {<.z, w>. | (z e. Met /\ w = {f | (f (_ (CC X. dom dom z) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ A.m e. ZZ ((j <_ k /\ j <_ m) -> ((f` k) e. dom dom z /\ (f` m) e. dom dom z /\ ((f` k)D(f` m)) < x))))})}
df-cmet 8135|- CMet = {x e. Met | A.f e. (Cau` x)E.y e. dom dom x f(~~>m` x)y}
cgr 8244class Grp
cgi 8245class Id
cgn 8246class inv
cgs 8247class /g
cgx 8248class ^g
df-grp 8249|- Grp = {g | E.t(g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u))}
df-gid 8250|- Id = {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}
df-ginv 8251|- inv = {<.g, f>. | (g e. Grp /\ f = {<.x, y>. | (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})})}
df-gdiv 8252|- /g = {<.g, f>. | (g e. Grp /\ f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))