mmdefinitions - Intuitionistic Logic Explorer

List of Syntax, Axioms (ax-) and Definitions (df-)

Ref	Expression (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 619	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 620	|- ( -. ph -> ( ph -> ps ) )
wo 715	wff ( ph \/ ps )
ax-io 716	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 837	wff STAB ph
df-stab 838	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 841	wff DECID ph
df-dc 842	|- (DECID ph <-> ( ph \/ -. ph ) )
wif 985	wff if- ( ph , ps , ch )
df-ifp 986	|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
w3o 1003	wff ( ph \/ ps \/ ch )
w3a 1004	wff ( ph /\ ps /\ ch )
df-3or 1005	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 1006	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1395	wff A. x ph
cv 1396	class x
wceq 1397	wff A = B
wtru 1398	wff T.
df-tru 1400	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1402	wff F.
df-fal 1403	|- ( F. <-> -. T. )
wxo 1419	wff ( ph \/_ ps )
df-xor 1420	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1495	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1496	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1497	|- ph   =>    |- A. x ph
wnf 1508	wff F/ x ph
df-nf 1509	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1540	wff E. x ph
ax-ie1 1541	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1542	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1552	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1553	|- ( A. x x = y -> A. y y = x )
ax-11 1554	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1555	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1557	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1558	|- ( A. x ph -> ph )
ax-17 1574	|- ( ph -> A. x ph )
ax-i9 1578	|- E. x x = y
ax-ial 1582	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1583	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1764	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1810	wff [ y / x ] ph
df-sb 1811	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1862	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1871	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2079	wff E! x ph
wmo 2080	wff E* x ph
df-eu 2082	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2083	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2202	wff A e. B
ax-13 2204	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2205	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2213	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2217	class { x | ph }
df-clab 2218	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2224	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2227	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2361	wff F/_ x A
df-nfc 2363	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2402	wff A =/= B
df-ne 2403	|- ( A =/= B <-> -. A = B )
wnel 2497	wff A e/ B
df-nel 2498	|- ( A e/ B <-> -. A e. B )
wral 2510	wff A. x e. A ph
wrex 2511	wff E. x e. A ph
wreu 2512	wff E! x e. A ph
wrmo 2513	wff E* x e. A ph
crab 2514	class { x e. A | ph }
df-ral 2515	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2516	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2517	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2518	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2519	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2802	class _V
df-v 2804	|- _V = { x | x = x }
wcdeq 3014	wff CondEq ( x = y -> ph )
df-cdeq 3015	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 3031	wff [. A / x ]. ph
df-sbc 3032	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3127	class [_ A / x ]_ B
df-csb 3128	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3197	class ( A \ B )
cun 3198	class ( A u. B )
cin 3199	class ( A i^i B )
wss 3200	wff A C_ B
df-dif 3202	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3204	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3206	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3213	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3494	class (/)
df-nul 3495	|- (/) = ( _V \ _V )
cif 3605	class if ( ph , A , B )
df-if 3606	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3652	class ~P A
df-pw 3654	|- ~P A = { x | x C_ A }
csn 3669	class { A }
cpr 3670	class { A , B }
ctp 3671	class { A , B , C }
cop 3672	class <. A , B >.
cotp 3673	class <. A , B , C >.
df-sn 3675	|- { A } = { x | x = A }
df-pr 3676	|- { A , B } = ( { A } u. { B } )
df-tp 3677	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3678	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3679	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3893	class U. A
df-uni 3894	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3928	class |^| A
df-int 3929	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3970	class U_ x e. A B
ciin 3971	class |^|_ x e. A B
df-iun 3972	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3973	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4064	wff Disj x e. A B
df-disj 4065	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4088	wff A R B
df-br 4089	|- ( A R B <-> <. A , B >. e. R )
copab 4149	class { <. x , y >. | ph }
cmpt 4150	class ( x e. A |-> B )
df-opab 4151	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4152	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4187	wff Tr A
df-tr 4188	|- ( Tr A <-> U. A C_ A )
ax-coll 4204	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4207	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4215	|- E. x A. y -. y e. x
ax-pow 4264	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4284	wff EXMID
df-exmid 4285	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4299	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4384	class _E
cid 4385	class _I
df-eprel 4386	|- _E = { <. x , y >. | x e. y }
df-id 4390	|- _I = { <. x , y >. | x = y }
wpo 4391	wff R Po A
wor 4392	wff R Or A
df-po 4393	|- ( 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 4394	|- ( 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 4424	wff FrFor R A S
wfr 4425	wff R Fr A
wse 4426	wff R Se A
wwe 4427	wff R We A
df-frfor 4428	|- (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 4429	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4430	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4431	|- ( 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 4459	wff Ord A
con0 4460	class On
wlim 4461	wff Lim A
csuc 4462	class suc A
df-iord 4463	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4465	|- On = { x | Ord x }
df-ilim 4466	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4468	|- suc A = ( A u. { A } )
ax-un 4530	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4635	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4686	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4688	class om
df-iom 4689	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4723	class ( A X. B )
ccnv 4724	class `' A
cdm 4725	class dom A
crn 4726	class ran A
cres 4727	class ( A |` B )
cima 4728	class ( A " B )
ccom 4729	class ( A o. B )
wrel 4730	wff Rel A
df-xp 4731	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4732	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4733	|- `' A = { <. x , y >. | y A x }
df-co 4734	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4735	|- dom A = { x | E. y x A y }
df-rn 4736	|- ran A = dom `' A
df-res 4737	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4738	|- ( A " B ) = ran ( A |` B )
cio 5284	class ( iota x ph )
df-iota 5286	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5320	wff Fun A
wfn 5321	wff A Fn B
wf 5322	wff F : A --> B
wf1 5323	wff F : A -1-1-> B
wfo 5324	wff F : A -onto-> B
wf1o 5325	wff F : A -1-1-onto-> B
cfv 5326	class ( F ` A )
wiso 5327	wff H Isom R , S ( A , B )
df-fun 5328	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5329	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5330	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5331	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5332	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5333	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5334	|- ( F ` A ) = ( iota x A F x )
df-isom 5335	|- ( 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 5969	class ( iota_ x e. A ph )
df-riota 5970	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6017	class ( A F B )
coprab 6018	class { <. <. x , y >. , z >. | ph }
cmpo 6019	class ( x e. A , y e. B |-> C )
df-ov 6020	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6021	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6022	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6232	class oF R
cofr 6233	class oR R
df-of 6234	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6235	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6300	class 1st
c2nd 6301	class 2nd
df-1st 6302	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6303	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6409	class tpos F
df-tpos 6410	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6450	wff Smo A
df-smo 6451	|- ( 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 6469	class recs ( F )
df-recs 6470	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6534	class rec ( F , I )
df-irdg 6535	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6555	class frec ( F , I )
df-frec 6556	|- 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 6574	class 1o
c2o 6575	class 2o
c3o 6576	class 3o
c4o 6577	class 4o
coa 6578	class +o
comu 6579	class .o
coei 6580	class ↑o
df-1o 6581	|- 1o = suc (/)
df-2o 6582	|- 2o = suc 1o
df-3o 6583	|- 3o = suc 2o
df-4o 6584	|- 4o = suc 3o
df-oadd 6585	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6586	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6587	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6698	wff R Er A
cec 6699	class [ A ] R
cqs 6700	class ( A /. R )
df-er 6701	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6703	|- [ A ] R = ( R " { A } )
df-qs 6707	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6816	class ^m
cpm 6817	class ^pm
df-map 6818	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6819	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6866	class X_ x e. A B
df-ixp 6867	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6906	class ~~
cdom 6907	class ~<_
cfn 6908	class Fin
df-en 6909	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6910	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6911	|- Fin = { x | E. y e. om x ~~ y }
cfi 7166	class fi
df-fi 7167	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7180	class sup ( A , B , R )
cinf 7181	class inf ( A , B , R )
df-sup 7182	|- 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 7183	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7235	class ( A ⊔ B )
df-dju 7236	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7243	class inl
cinr 7244	class inr
df-inl 7245	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7246	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7281	class case ( R , S )
df-case 7282	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7300	class ( R ⊔d S )
df-djud 7301	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7317	class ℕ∞
df-nninf 7318	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7332	class Omni
df-omni 7333	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7349	class Markov
df-markov 7350	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7361	class WOmni
df-womni 7362	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7380	class card
wacn 7381	class AC A
df-card 7382	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7383	|- AC A = { x | ( A e. _V /\ A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
wac 7419	wff CHOICE
df-ac 7420	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7465	wff R Ap A
df-pap 7466	|- ( 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 7467	wff R TAp A
df-tap 7468	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7480	wff CCHOICE
df-cc 7481	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7491	class N.
cpli 7492	class +N
cmi 7493	class .N
clti 7494	class <N
cplpq 7495	class +pQ
cmpq 7496	class .pQ
cltpq 7497	class <pQ
ceq 7498	class ~Q
cnq 7499	class Q.
c1q 7500	class 1Q
cplq 7501	class +Q
cmq 7502	class .Q
crq 7503	class *Q
cltq 7504	class <Q
ceq0 7505	class ~Q0
cnq0 7506	class Q0
c0q0 7507	class 0Q0
cplq0 7508	class +Q0
cmq0 7509	class ·Q0
cnp 7510	class P.
c1p 7511	class 1P
cpp 7512	class +P.
cmp 7513	class .P.
cltp 7514	class <P
cer 7515	class ~R
cnr 7516	class R.
c0r 7517	class 0R
c1r 7518	class 1R
cm1r 7519	class -1R
cplr 7520	class +R
cmr 7521	class .R
cltr 7522	class <R
df-ni 7523	|- N. = ( om \ { (/) } )
df-pli 7524	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7525	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7526	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7563	|- +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 7564	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7565	|- <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 7566	|- ~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 7567	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7568	|- +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 7569	|- .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 7570	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7571	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7572	|- <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 7643	|- ~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 7644	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7645	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7646	|- +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 7647	|- ·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 7685	|- 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 7686	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7687	|- +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 7688	|- .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 7689	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7945	|- ~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 7946	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7947	|- +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 7948	|- .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 7949	|- <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 7950	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7951	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7952	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8029	class CC
cr 8030	class RR
cc0 8031	class 0
c1 8032	class 1
ci 8033	class _i
caddc 8034	class +
cltrr 8035	class <RR
cmul 8036	class x.
df-c 8037	|- CC = ( R. X. R. )
df-0 8038	|- 0 = <. 0R , 0R >.
df-1 8039	|- 1 = <. 1R , 0R >.
df-i 8040	|- _i = <. 0R , 1R >.
df-r 8041	|- RR = ( R. X. { 0R } )
df-add 8042	|- + = { <. <. 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 8043	|- 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 8044	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8122	|- CC e. _V
ax-resscn 8123	|- RR C_ CC
ax-1cn 8124	|- 1 e. CC
ax-1re 8125	|- 1 e. RR
ax-icn 8126	|- _i e. CC
ax-addcl 8127	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8128	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8129	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8130	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8131	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8132	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8133	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8134	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8135	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8136	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8137	|- 0 <RR 1
ax-1rid 8138	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8139	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8140	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8141	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8142	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8143	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8144	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8145	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8146	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8147	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8148	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8149	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8150	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8151	|- 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 8152	|- ( ( ( 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 8153	|- + : ( CC X. CC ) --> CC
ax-mulf 8154	|- x. : ( CC X. CC ) --> CC
cpnf 8210	class +oo
cmnf 8211	class -oo
cxr 8212	class RR*
clt 8213	class <
cle 8214	class <_
df-pnf 8215	|- +oo = ~P U. CC
df-mnf 8216	|- -oo = ~P +oo
df-xr 8217	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8218	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8219	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8349	class -
cneg 8350	class -u A
df-sub 8351	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8352	|- -u A = ( 0 - A )
creap 8753	class #ℝ
df-reap 8754	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8760	class #
df-ap 8761	|- # = { <. 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 8851	class /
df-div 8852	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9142	class NN
df-inn 9143	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9193	class 2
c3 9194	class 3
c4 9195	class 4
c5 9196	class 5
c6 9197	class 6
c7 9198	class 7
c8 9199	class 8
c9 9200	class 9
df-2 9201	|- 2 = ( 1 + 1 )
df-3 9202	|- 3 = ( 2 + 1 )
df-4 9203	|- 4 = ( 3 + 1 )
df-5 9204	|- 5 = ( 4 + 1 )
df-6 9205	|- 6 = ( 5 + 1 )
df-7 9206	|- 7 = ( 6 + 1 )
df-8 9207	|- 8 = ( 7 + 1 )
df-9 9208	|- 9 = ( 8 + 1 )
cn0 9401	class NN0
df-n0 9402	|- NN0 = ( NN u. { 0 } )
cxnn0 9464	class NN0*
df-xnn0 9465	|- NN0* = ( NN0 u. { +oo } )
cz 9478	class ZZ
df-z 9479	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9610	class ; A B
df-dec 9611	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9754	class ZZ>=
df-uz 9755	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9852	class QQ
df-q 9853	|- QQ = ( / " ( ZZ X. NN ) )
crp 9887	class RR+
df-rp 9888	|- RR+ = { x e. RR | 0 < x }
cxne 10003	class -e A
cxad 10004	class +e
cxmu 10005	class xe
df-xneg 10006	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10007	|- +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 10008	|- 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 10122	class (,)
cioc 10123	class (,]
cico 10124	class [,)
cicc 10125	class [,]
df-ioo 10126	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10127	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10128	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10129	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10242	class ...
df-fz 10243	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10376	class ..^
df-fzo 10377	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10527	class |_
cceil 10528	class ⌈
df-fl 10529	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10530	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10583	class mod
df-mod 10584	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10708	class seq M ( .+ , F )
df-seqfrec 10709	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10799	class ^
df-exp 10800	|- ^ = ( 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 10986	class !
df-fac 10987	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11008	class _C
df-bc 11009	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11036	class ♯
df-ihash 11037	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11112	class Word S
df-word 11113	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11157	class lastS
df-lsw 11158	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11166	class ++
df-concat 11167	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11191	class <" A ">
df-s1 11192	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11225	class substr
df-substr 11226	|- substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )
cpfx 11252	class prefix
df-pfx 11253	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11329	class <" A B ">
cs3 11330	class <" A B C ">
cs4 11331	class <" A B C D ">
cs5 11332	class <" A B C D E ">
cs6 11333	class <" A B C D E F ">
cs7 11334	class <" A B C D E F G ">
cs8 11335	class <" A B C D E F G H ">
df-s2 11336	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11337	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11338	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11339	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11340	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11341	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11342	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11374	class shift
df-shft 11375	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11399	class *
cre 11400	class Re
cim 11401	class Im
df-cj 11402	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11403	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11404	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11556	class sqr
cabs 11557	class abs
df-rsqrt 11558	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11559	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11838	class ~~>
df-clim 11839	|- ~~> = { <. 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 11913	class sum_ k e. A B
df-sumdc 11914	|- 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 12110	class prod_ k e. A B
df-proddc 12111	|- 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 12202	class exp
ceu 12203	class _e
csin 12204	class sin
ccos 12205	class cos
ctan 12206	class tan
cpi 12207	class pi
df-ef 12208	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12209	|- _e = ( exp ` 1 )
df-sin 12210	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12211	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12212	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12213	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12335	class tau
df-tau 12336	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12347	class ||
df-dvds 12348	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12500	class bits
df-bits 12501	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12523	class gcd
df-gcd 12524	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12631	class lcm
df-lcm 12632	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12678	class Prime
df-prm 12679	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12752	class numer
cdenom 12753	class denom
df-numer 12754	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12755	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12779	class odZ
cphi 12780	class phi
df-odz 12781	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12782	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12856	class pCnt
df-pc 12857	|- 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 12941	class ZZ[_i]
df-gz 12942	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13077	class Struct
cnx 13078	class ndx
csts 13079	class sSet
cslot 13080	class Slot A
cbs 13081	class Base
cress 13082	class ↾s
df-struct 13083	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13084	|- ndx = ( _I |` NN )
df-slot 13085	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13087	|- Base = Slot 1
df-sets 13088	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13089	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13159	class +g
cmulr 13160	class .r
cstv 13161	class *r
csca 13162	class Scalar
cvsca 13163	class .s
cip 13164	class .i
cts 13165	class TopSet
cple 13166	class le
coc 13167	class oc
cds 13168	class dist
cunif 13169	class UnifSet
chom 13170	class Hom
cco 13171	class comp
df-plusg 13172	|- +g = Slot 2
df-mulr 13173	|- .r = Slot 3
df-starv 13174	|- *r = Slot 4
df-sca 13175	|- Scalar = Slot 5
df-vsca 13176	|- .s = Slot 6
df-ip 13177	|- .i = Slot 8
df-tset 13178	|- TopSet = Slot 9
df-ple 13179	|- le = Slot ; 1 0
df-ocomp 13180	|- oc = Slot ; 1 1
df-ds 13181	|- dist = Slot ; 1 2
df-unif 13182	|- UnifSet = Slot ; 1 3
df-hom 13183	|- Hom = Slot ; 1 4
df-cco 13184	|- comp = Slot ; 1 5
crest 13321	class ↾t
ctopn 13322	class TopOpen
df-rest 13323	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13324	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13336	class topGen
cpt 13337	class Xt_
c0g 13338	class 0g
cgsu 13339	class gsumg
df-0g 13340	|- 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-igsum 13341	|- gsumg = ( w e. _V , f e. _V |-> ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) ) )
df-topgen 13342	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13343	|- 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 13347	class X_s
cpws 13348	class ^s
df-prds 13349	|- 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. ( ( 2nd ` a ) h c ) , 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 13372	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13381	class "s
cqus 13382	class /.s
cxps 13383	class X.s
df-iimas 13384	|- "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 13385	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13386	|- 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 13435	class +f
cmgm 13436	class Mgm
df-plusf 13437	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13438	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13483	class Smgrp
df-sgrp 13484	|- 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 13498	class Mnd
df-mnd 13499	|- 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 13539	class MndHom
csubmnd 13540	class SubMnd
df-mhm 13541	|- 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 13542	|- 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 13582	class Grp
cminusg 13583	class invg
csg 13584	class -g
df-grp 13585	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13586	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13587	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13705	class .g
df-mulg 13706	|- .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 13753	class SubGrp
cnsg 13754	class NrmSGrp
cqg 13755	class ~QG
df-subg 13756	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13757	|- 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 13758	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13826	class GrpHom
df-ghm 13827	|- GrpHom = ( s e. Grp , t e. Grp |-> { g | [. ( Base ` s ) / w ]. ( g : w --> ( Base ` t ) /\ A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) ) ) } )
ccmn 13870	class CMnd
cabl 13871	class Abel
df-cmn 13872	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13873	|- Abel = ( Grp i^i CMnd )
cmgp 13932	class mulGrp
df-mgp 13933	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 13944	class Rng
df-rng 13945	|- Rng = { f e. Abel | ( (mulGrp ` f ) e. Smgrp /\ [. ( Base ` f ) / b ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
cur 13971	class 1r
df-ur 13972	|- 1r = ( 0g o. mulGrp )
csrg 13975	class SRing
df-srg 13976	|- 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 14008	class Ring
ccrg 14009	class CRing
df-ring 14010	|- 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 14011	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14079	class oppr
df-oppr 14080	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14098	class ||r
cui 14099	class Unit
cir 14100	class Irred
df-dvdsr 14101	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14102	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14103	|- 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 14133	class invr
df-invr 14134	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14144	class /r
df-dvr 14145	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14163	class RingHom
crs 14164	class RingIso
df-rhm 14165	|- 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-rim 14166	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14192	class NzRing
df-nzr 14193	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14203	class LRing
df-lring 14204	|- 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 ) ) ) }
csubrng 14210	class SubRng
df-subrng 14211	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14230	class SubRing
crgspn 14231	class RingSpan
df-subrg 14232	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14233	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14268	class RLReg
cdomn 14269	class Domn
cidom 14270	class IDomn
df-rlreg 14271	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14272	|- Domn = { r e. NzRing | [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) }
df-idom 14273	|- IDomn = ( CRing i^i Domn )
capr 14293	class #r
df-apr 14294	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 14300	class LMod
cscaf 14301	class .sf
df-lmod 14302	|- 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 14303	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14365	class LSubSp
df-lssm 14366	|- 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 14399	class LSpan
df-lsp 14400	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14446	class subringAlg
crglmod 14447	class ringLMod
df-sra 14448	|- subringAlg = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) )
df-rgmod 14449	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14480	class LIdeal
crsp 14481	class RSpan
df-lidl 14482	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14483	|- RSpan = ( LSpan o. ringLMod )
c2idl 14512	class 2Ideal
df-2idl 14513	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14548	class PsMet
cxmet 14549	class *Met
cmet 14550	class Met
cbl 14551	class ball
cfbas 14552	class fBas
cfg 14553	class filGen
cmopn 14554	class MetOpen
cmetu 14555	class metUnif
df-psmet 14556	|- 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 14557	|- *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 14558	|- 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 14559	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14560	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14561	|- 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 14562	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14563	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14569	class ℂfld
df-cnfld 14570	|- ℂfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } ) )
czring 14603	class ℤring
df-zring 14604	|- ℤring = (ℂfld ↾s ZZ )
czrh 14624	class ZRHom
czlm 14625	class ZMod
czn 14626	class ℤ/nℤ
df-zrh 14627	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14628	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14629	|- ℤ/nℤ = ( n e. NN0 |-> [_ℤring / z ]_ [_ ( z /.s ( z ~QG ( (RSpan ` z ) ` { n } ) ) ) / s ]_ ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. ) )
cmps 14674	class mPwSer
cmpl 14675	class mPoly
df-psr 14676	|- mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
df-mplcoe 14677	|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )
ctop 14720	class Top
df-top 14721	|- 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 14733	class TopOn
df-topon 14734	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14753	class TopSp
df-topsp 14754	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14765	class TopBases
df-bases 14766	|- 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 14815	class Clsd
cnt 14816	class int
ccl 14817	class cls
df-cld 14818	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14819	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14820	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14861	class nei
df-nei 14862	|- 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 14908	class Cn
ccnp 14909	class CnP
clm 14910	class ~~> t
df-cn 14911	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 14912	|- 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 14913	|- ~~> 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 14975	class tX
df-tx 14976	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15023	class Homeo
df-hmeo 15024	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15059	class *MetSp
cms 15060	class MetSp
ctms 15061	class toMetSp
df-xms 15062	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15063	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15064	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15293	class -cn->
df-cncf 15294	|- -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 15377	class lim CC
cdv 15378	class _D
df-limced 15379	|- 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 15380	|- _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 ) ) )
cply 15451	class Poly
cidp 15452	class Xp
df-ply 15453	|- Poly = ( x e. ~P CC |-> { f | E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
df-idp 15454	|- Xp = ( _I |` CC )
clog 15579	class log
ccxp 15580	class ^c
df-relog 15581	|- log = `' ( exp |` RR )
df-rpcxp 15582	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15666	class logb
df-logb 15667	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15704	class sigma
df-sgm 15705	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15725	class /L
df-lgs 15726	|- /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 ) ) ) ) )
cedgf 15854	class .ef
df-edgf 15855	|- .ef = Slot ; 1 8
cvtx 15862	class Vtx
ciedg 15863	class iEdg
df-vtx 15864	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 15865	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 15907	class Edg
df-edg 15908	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 15917	class UHGraph
cushgr 15918	class USHGraph
df-uhgrm 15919	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 15920	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 15941	class UPGraph
cumgr 15942	class UMGraph
df-upgren 15943	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 15944	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16003	class USPGraph
cusgr 16004	class USGraph
df-uspgren 16005	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16006	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16103	class SubGraph
df-subgr 16104	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16136	class VtxDeg
df-vtxdg 16137	|- VtxDeg = ( g e. _V |-> [_ (Vtx ` g ) / v ]_ [_ (iEdg ` g ) / e ]_ ( u e. v |-> ( (♯ ` { x e. dom e | u e. ( e ` x ) } ) +e (♯ ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )
cwlks 16167	class Walks
df-wlks 16168	|- Walks = ( g e. _V |-> { <. f , p >. | ( f e. Word dom (iEdg ` g ) /\ p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g ) /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) ) ) } )
ctrls 16230	class Trails
df-trls 16231	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16241	class ClWWalks
df-clwwlk 16242	|- ClWWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )
cclwwlkn 16253	class ClWWalksN
df-clwwlkn 16254	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16276	class ClWWalksNOn
df-clwwlknon 16277	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16292	class EulerPaths
df-eupth 16293	|- EulerPaths = ( g e. _V |-> { <. f , p >. | ( f (Trails ` g ) p /\ f : ( 0..^ (♯ ` f ) ) -onto-> dom (iEdg ` g ) ) } )
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 16389	wff A DECIDin B
df-dcin 16390	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16407	wff BOUNDED ph
ax-bd0 16408	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16409	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16410	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16411	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16412	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16413	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16414	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16415	|- BOUNDED x = y
ax-bdel 16416	|- BOUNDED x e. y
ax-bdsb 16417	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16435	wff BOUNDED A
df-bdc 16436	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16479	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16519	|- BOUNDED ph   =>    |- DECID ph
wind 16521	wff Ind A
df-bj-ind 16522	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16536	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16563	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16571	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16577	|- 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 16582	|- 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 16584	|- ( ( ( 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 ) ) )
cgfsu 16678	class gfsumgf
df-gfsum 16679	|- gfsumgf = ( w e. CMnd , f e. _V |-> ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gsumg ( f o. g ) ) ) ) ) )
walsi 16687	wff A.! x ( ph -> ps )
walsc 16688	wff A.! x e. A ph
df-alsi 16689	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 16690	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )