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 623	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 624	|- ( -. ph -> ( ph -> ps ) )
wo 720	wff ( ph \/ ps )
ax-io 721	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 842	wff STAB ph
df-stab 843	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 846	wff DECID ph
df-dc 847	|- (DECID ph <-> ( ph \/ -. ph ) )
wif 990	wff if- ( ph , ps , ch )
df-ifp 991	|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
w3o 1008	wff ( ph \/ ps \/ ch )
w3a 1009	wff ( ph /\ ps /\ ch )
df-3or 1010	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 1011	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1400	wff A. x ph
cv 1401	class x
wceq 1402	wff A = B
wtru 1403	wff T.
df-tru 1405	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1407	wff F.
df-fal 1408	|- ( F. <-> -. T. )
wxo 1424	wff ( ph \/_ ps )
df-xor 1425	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1500	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1501	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1502	|- ph   =>    |- A. x ph
wnf 1513	wff F/ x ph
df-nf 1514	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1545	wff E. x ph
ax-ie1 1546	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1547	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1557	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1558	|- ( A. x x = y -> A. y y = x )
ax-11 1559	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1560	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1562	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1563	|- ( A. x ph -> ph )
ax-17 1579	|- ( ph -> A. x ph )
ax-i9 1583	|- E. x x = y
ax-ial 1587	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1588	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1768	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1815	wff [ y / x ] ph
df-sb 1816	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1867	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1876	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2086	wff E! x ph
wmo 2087	wff E* x ph
df-eu 2089	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2090	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2209	wff A e. B
ax-13 2211	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2212	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2220	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2224	class { x | ph }
df-clab 2225	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2231	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2234	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2379	wff F/_ x A
df-nfc 2381	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2420	wff A =/= B
df-ne 2421	|- ( A =/= B <-> -. A = B )
wnel 2515	wff A e/ B
df-nel 2516	|- ( A e/ B <-> -. A e. B )
wral 2528	wff A. x e. A ph
wrex 2529	wff E. x e. A ph
wreu 2530	wff E! x e. A ph
wrmo 2531	wff E* x e. A ph
crab 2532	class { x e. A | ph }
df-ral 2533	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2534	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2535	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2536	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2537	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2821	class _V
df-v 2823	|- _V = { x | x = x }
wcdeq 3034	wff CondEq ( x = y -> ph )
df-cdeq 3035	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 3051	wff [. A / x ]. ph
df-sbc 3052	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3147	class [_ A / x ]_ B
df-csb 3148	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3217	class ( A \ B )
cun 3218	class ( A u. B )
cin 3219	class ( A i^i B )
wss 3220	wff A C_ B
df-dif 3222	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3224	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3226	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3233	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3520	class (/)
df-nul 3521	|- (/) = ( _V \ _V )
cif 3638	class if ( ph , A , B )
df-if 3639	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3688	class ~P A
df-pw 3690	|- ~P A = { x | x C_ A }
csn 3708	class { A }
cpr 3709	class { A , B }
ctp 3710	class { A , B , C }
cop 3711	class <. A , B >.
cotp 3712	class <. A , B , C >.
df-sn 3714	|- { A } = { x | x = A }
df-pr 3715	|- { A , B } = ( { A } u. { B } )
df-tp 3716	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3717	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3718	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3933	class U. A
df-uni 3934	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3968	class |^| A
df-int 3969	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 4010	class U_ x e. A B
ciin 4011	class |^|_ x e. A B
df-iun 4012	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 4013	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4104	wff Disj x e. A B
df-disj 4105	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4128	wff A R B
df-br 4129	|- ( A R B <-> <. A , B >. e. R )
copab 4189	class { <. x , y >. | ph }
cmpt 4190	class ( x e. A |-> B )
df-opab 4191	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4192	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4227	wff Tr A
df-tr 4228	|- ( Tr A <-> U. A C_ A )
ax-coll 4244	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4247	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4257	|- E. x A. y -. y e. x
ax-pow 4309	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4329	wff EXMID
df-exmid 4330	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4344	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4430	class _E
cid 4431	class _I
df-eprel 4432	|- _E = { <. x , y >. | x e. y }
df-id 4436	|- _I = { <. x , y >. | x = y }
wpo 4437	wff R Po A
wor 4438	wff R Or A
df-po 4439	|- ( 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 4440	|- ( 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 4470	wff FrFor R A S
wfr 4471	wff R Fr A
wse 4472	wff R Se A
wwe 4473	wff R We A
df-frfor 4474	|- (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 4475	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4476	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4477	|- ( 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 4505	wff Ord A
con0 4506	class On
wlim 4507	wff Lim A
csuc 4508	class suc A
df-iord 4509	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4511	|- On = { x | Ord x }
df-ilim 4512	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4514	|- suc A = ( A u. { A } )
ax-un 4576	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4682	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4733	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4735	class om
df-iom 4736	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4770	class ( A X. B )
ccnv 4771	class `' A
cdm 4772	class dom A
crn 4773	class ran A
cres 4774	class ( A |` B )
cima 4775	class ( A " B )
ccom 4776	class ( A o. B )
wrel 4777	wff Rel A
df-xp 4778	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4779	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4780	|- `' A = { <. x , y >. | y A x }
df-co 4781	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4782	|- dom A = { x | E. y x A y }
df-rn 4783	|- ran A = dom `' A
df-res 4784	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4785	|- ( A " B ) = ran ( A |` B )
cio 5333	class ( iota x ph )
df-iota 5335	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5369	wff Fun A
wfn 5370	wff A Fn B
wf 5371	wff F : A --> B
wf1 5372	wff F : A -1-1-> B
wfo 5373	wff F : A -onto-> B
wf1o 5374	wff F : A -1-1-onto-> B
cfv 5375	class ( F ` A )
wiso 5376	wff H Isom R , S ( A , B )
df-fun 5377	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5378	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5379	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5380	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5381	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5382	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5383	|- ( F ` A ) = ( iota x A F x )
df-isom 5384	|- ( 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 6030	class ( iota_ x e. A ph )
df-riota 6031	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6078	class ( A F B )
coprab 6079	class { <. <. x , y >. , z >. | ph }
cmpo 6080	class ( x e. A , y e. B |-> C )
df-ov 6081	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6082	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6083	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6293	class oF R
cofr 6294	class oR R
df-of 6295	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6296	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6365	class 1st
c2nd 6366	class 2nd
df-1st 6367	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6368	|- 2nd = ( x e. _V |-> U. ran { x } )
csupp 6468	class supp
df-supp 6469	|- supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
ctpos 6508	class tpos F
df-tpos 6509	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6549	wff Smo A
df-smo 6550	|- ( 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 6568	class recs ( F )
df-recs 6569	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6633	class rec ( F , I )
df-irdg 6634	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6654	class frec ( F , I )
df-frec 6655	|- 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 6673	class 1o
c2o 6674	class 2o
c3o 6675	class 3o
c4o 6676	class 4o
coa 6677	class +o
comu 6678	class .o
coei 6679	class ↑o
df-1o 6680	|- 1o = suc (/)
df-2o 6681	|- 2o = suc 1o
df-3o 6682	|- 3o = suc 2o
df-4o 6683	|- 4o = suc 3o
df-oadd 6684	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6685	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6686	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6797	wff R Er A
cec 6798	class [ A ] R
cqs 6799	class ( A /. R )
df-er 6800	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6802	|- [ A ] R = ( R " { A } )
df-qs 6806	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6915	class ^m
cpm 6916	class ^pm
df-map 6917	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6918	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6973	class X_ x e. A B
df-ixp 6974	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 7013	class ~~
cdom 7014	class ~<_
cfn 7015	class Fin
df-en 7016	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 7017	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 7018	|- Fin = { x | E. y e. om x ~~ y }
cfsupp 7278	class finSupp
df-fsupp 7279	|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
cfi 7295	class fi
df-fi 7296	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7315	class sup ( A , B , R )
cinf 7316	class inf ( A , B , R )
df-sup 7317	|- 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 7318	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7370	class ( A ⊔ B )
df-dju 7371	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7378	class inl
cinr 7379	class inr
df-inl 7380	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7381	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7416	class case ( R , S )
df-case 7417	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7435	class ( R ⊔d S )
df-djud 7436	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7452	class ℕ∞
df-nninf 7453	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7467	class Omni
df-omni 7468	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7484	class Markov
df-markov 7485	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7496	class WOmni
df-womni 7497	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7515	class card
wacn 7516	class AC A
df-card 7517	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7518	|- 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 7554	wff CHOICE
df-ac 7555	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7600	wff R Ap A
df-pap 7601	|- ( 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 7607	wff R TAp A
df-tap 7608	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7621	wff CCHOICE
df-cc 7622	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7632	class N.
cpli 7633	class +N
cmi 7634	class .N
clti 7635	class <N
cplpq 7636	class +pQ
cmpq 7637	class .pQ
cltpq 7638	class <pQ
ceq 7639	class ~Q
cnq 7640	class Q.
c1q 7641	class 1Q
cplq 7642	class +Q
cmq 7643	class .Q
crq 7644	class *Q
cltq 7645	class <Q
ceq0 7646	class ~Q0
cnq0 7647	class Q0
c0q0 7648	class 0Q0
cplq0 7649	class +Q0
cmq0 7650	class ·Q0
cnp 7651	class P.
c1p 7652	class 1P
cpp 7653	class +P.
cmp 7654	class .P.
cltp 7655	class <P
cer 7656	class ~R
cnr 7657	class R.
c0r 7658	class 0R
c1r 7659	class 1R
cm1r 7660	class -1R
cplr 7661	class +R
cmr 7662	class .R
cltr 7663	class <R
df-ni 7664	|- N. = ( om \ { (/) } )
df-pli 7665	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7666	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7667	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7704	|- +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 7705	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7706	|- <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 7707	|- ~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 7708	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7709	|- +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 7710	|- .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 7711	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7712	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7713	|- <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 7784	|- ~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 7785	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7786	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7787	|- +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 7788	|- ·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 7826	|- 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 7827	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7828	|- +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 7829	|- .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 7830	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 8086	|- ~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 8087	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 8088	|- +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 8089	|- .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 8090	|- <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 8091	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 8092	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 8093	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8170	class CC
cr 8171	class RR
cc0 8172	class 0
c1 8173	class 1
ci 8174	class _i
caddc 8175	class +
cltrr 8176	class <RR
cmul 8177	class x.
df-c 8178	|- CC = ( R. X. R. )
df-0 8179	|- 0 = <. 0R , 0R >.
df-1 8180	|- 1 = <. 1R , 0R >.
df-i 8181	|- _i = <. 0R , 1R >.
df-r 8182	|- RR = ( R. X. { 0R } )
df-add 8183	|- + = { <. <. 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 8184	|- 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 8185	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8263	|- CC e. _V
ax-resscn 8264	|- RR C_ CC
ax-1cn 8265	|- 1 e. CC
ax-1re 8266	|- 1 e. RR
ax-icn 8267	|- _i e. CC
ax-addcl 8268	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8269	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8270	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8271	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8272	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8273	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8274	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8275	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8276	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8277	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8278	|- 0 <RR 1
ax-1rid 8279	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8280	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8281	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8282	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8283	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8284	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8285	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8286	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8287	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8288	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8289	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8290	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8291	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8292	|- 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 8293	|- ( ( ( 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 8294	|- + : ( CC X. CC ) --> CC
ax-mulf 8295	|- x. : ( CC X. CC ) --> CC
cpnf 8350	class +oo
cmnf 8351	class -oo
cxr 8352	class RR*
clt 8353	class <
cle 8354	class <_
df-pnf 8355	|- +oo = ~P U. CC
df-mnf 8356	|- -oo = ~P +oo
df-xr 8357	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8358	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8359	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8490	class -
cneg 8491	class -u A
df-sub 8492	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8493	|- -u A = ( 0 - A )
creap 8895	class #ℝ
df-reap 8896	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8902	class #
df-ap 8903	|- # = { <. 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 8995	class /
df-div 8996	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9286	class NN
df-inn 9287	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9337	class 2
c3 9338	class 3
c4 9339	class 4
c5 9340	class 5
c6 9341	class 6
c7 9342	class 7
c8 9343	class 8
c9 9344	class 9
df-2 9345	|- 2 = ( 1 + 1 )
df-3 9346	|- 3 = ( 2 + 1 )
df-4 9347	|- 4 = ( 3 + 1 )
df-5 9348	|- 5 = ( 4 + 1 )
df-6 9349	|- 6 = ( 5 + 1 )
df-7 9350	|- 7 = ( 6 + 1 )
df-8 9351	|- 8 = ( 7 + 1 )
df-9 9352	|- 9 = ( 8 + 1 )
cn0 9545	class NN0
df-n0 9546	|- NN0 = ( NN u. { 0 } )
cxnn0 9612	class NN0*
df-xnn0 9613	|- NN0* = ( NN0 u. { +oo } )
cz 9626	class ZZ
df-z 9627	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9759	class ; A B
df-dec 9760	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9903	class ZZ>=
df-uz 9904	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 10001	class QQ
df-q 10002	|- QQ = ( / " ( ZZ X. NN ) )
crp 10036	class RR+
df-rp 10037	|- RR+ = { x e. RR | 0 < x }
cxne 10153	class -e A
cxad 10154	class +e
cxmu 10155	class xe
df-xneg 10156	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10157	|- +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 10158	|- 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 10272	class (,)
cioc 10273	class (,]
cico 10274	class [,)
cicc 10275	class [,]
df-ioo 10276	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10277	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10278	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10279	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10393	class ...
df-fz 10394	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10530	class ..^
df-fzo 10531	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10684	class |_
cceil 10685	class ⌈
df-fl 10686	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10687	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10740	class mod
df-mod 10741	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10865	class seq M ( .+ , F )
df-seqfrec 10866	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10956	class ^
df-exp 10957	|- ^ = ( 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 11144	class !
df-fac 11145	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11166	class _C
df-bc 11167	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11195	class ♯
df-ihash 11196	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11285	class Word S
df-word 11286	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11330	class lastS
df-lsw 11331	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11339	class ++
df-concat 11340	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11364	class <" A ">
df-s1 11365	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11398	class substr
df-substr 11399	|- 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 11425	class prefix
df-pfx 11426	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11502	class <" A B ">
cs3 11503	class <" A B C ">
cs4 11504	class <" A B C D ">
cs5 11505	class <" A B C D E ">
cs6 11506	class <" A B C D E F ">
cs7 11507	class <" A B C D E F G ">
cs8 11508	class <" A B C D E F G H ">
df-s2 11509	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11510	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11511	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11512	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11513	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11514	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11515	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11560	class shift
df-shft 11561	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11585	class *
cre 11586	class Re
cim 11587	class Im
df-cj 11588	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11589	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11590	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11743	class sqr
cabs 11744	class abs
df-rsqrt 11745	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11746	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 12025	class ~~>
df-clim 12026	|- ~~> = { <. 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 12100	class sum_ k e. A B
df-sumdc 12101	|- 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 12298	class prod_ k e. A B
df-proddc 12299	|- 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 12390	class exp
ceu 12391	class _e
csin 12392	class sin
ccos 12393	class cos
ctan 12394	class tan
cpi 12395	class pi
df-ef 12396	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12397	|- _e = ( exp ` 1 )
df-sin 12398	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12399	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12400	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12401	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12523	class tau
df-tau 12524	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12535	class ||
df-dvds 12536	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12688	class bits
df-bits 12689	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12711	class gcd
df-gcd 12712	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12819	class lcm
df-lcm 12820	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12866	class Prime
df-prm 12867	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12940	class numer
cdenom 12941	class denom
df-numer 12942	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12943	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12967	class odZ
cphi 12968	class phi
df-odz 12969	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12970	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 13044	class pCnt
df-pc 13045	|- 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 13129	class ZZ[_i]
df-gz 13130	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13329	class Struct
cnx 13330	class ndx
csts 13331	class sSet
cslot 13332	class Slot A
cbs 13333	class Base
cress 13334	class ↾s
df-struct 13335	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13336	|- ndx = ( _I |` NN )
df-slot 13337	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13339	|- Base = Slot 1
df-sets 13340	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13341	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13411	class +g
cmulr 13412	class .r
cstv 13413	class *r
csca 13414	class Scalar
cvsca 13415	class .s
cip 13416	class .i
cts 13417	class TopSet
cple 13418	class le
coc 13419	class oc
cds 13420	class dist
cunif 13421	class UnifSet
chom 13422	class Hom
cco 13423	class comp
df-plusg 13424	|- +g = Slot 2
df-mulr 13425	|- .r = Slot 3
df-starv 13426	|- *r = Slot 4
df-sca 13427	|- Scalar = Slot 5
df-vsca 13428	|- .s = Slot 6
df-ip 13429	|- .i = Slot 8
df-tset 13430	|- TopSet = Slot 9
df-ple 13431	|- le = Slot ; 1 0
df-ocomp 13432	|- oc = Slot ; 1 1
df-ds 13433	|- dist = Slot ; 1 2
df-unif 13434	|- UnifSet = Slot ; 1 3
df-hom 13435	|- Hom = Slot ; 1 4
df-cco 13436	|- comp = Slot ; 1 5
crest 13573	class ↾t
ctopn 13574	class TopOpen
df-rest 13575	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13576	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13588	class topGen
cpt 13589	class Xt_
c0g 13590	class 0g
cgzsu 13591	class gzsumgz
df-0g 13592	|- 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-gzsum 13593	|- gzsumgz = ( 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 13594	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13595	|- 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 ) ) } ) )
cimas 13602	class "s
cqus 13603	class /.s
df-iimas 13604	|- "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 13605	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
cplusf 13653	class +f
cmgm 13654	class Mgm
df-plusf 13655	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13656	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13696	class Smgrp
df-sgrp 13697	|- 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 13709	class Mnd
df-mnd 13710	|- 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 13744	class MndHom
csubmnd 13745	class SubMnd
df-mhm 13746	|- 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 13747	|- 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 13785	class Grp
cminusg 13786	class invg
csg 13787	class -g
df-grp 13788	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13789	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13790	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13902	class .g
df-mulg 13903	|- .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 13950	class SubGrp
cnsg 13951	class NrmSGrp
cqg 13952	class ~QG
df-subg 13953	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13954	|- 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 13955	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 14023	class GrpHom
df-ghm 14024	|- 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 14067	class CMnd
cabl 14068	class Abel
df-cmn 14069	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 14070	|- Abel = ( Grp i^i CMnd )
cgsu 14130	class gsumg
df-gsumfi 14131	|- gsumg = ( 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 gzsumgz ( f o. g ) ) ) ) ) )
cprds 14149	class X_s
df-prds 14150	|- 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 ) ) ) ) ) >. } ) ) )
cxps 14179	class X.s
df-xps 14180	|- 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 >. } ) ) )
cpws 14182	class ^s
df-pws 14183	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cmgp 14197	class mulGrp
df-mgp 14198	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 14209	class Rng
df-rng 14210	|- 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 14240	class 1r
df-ur 14241	|- 1r = ( 0g o. mulGrp )
csrg 14244	class SRing
df-srg 14245	|- 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 14277	class Ring
ccrg 14278	class CRing
df-ring 14279	|- 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 14280	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14348	class oppr
df-oppr 14349	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14368	class ||r
cui 14369	class Unit
cir 14370	class Irred
df-dvdsr 14371	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14372	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14373	|- 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 14403	class invr
df-invr 14404	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14414	class /r
df-dvr 14415	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14433	class RingHom
crs 14434	class RingIso
df-rhm 14435	|- 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 14436	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14462	class NzRing
df-nzr 14463	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14473	class LRing
df-lring 14474	|- 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 14481	class SubRng
df-subrng 14482	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14501	class SubRing
crgspn 14502	class RingSpan
df-subrg 14503	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14504	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14539	class RLReg
cdomn 14540	class Domn
cidom 14541	class IDomn
df-rlreg 14542	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14543	|- 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 14544	|- IDomn = ( CRing i^i Domn )
capr 14565	class #r
df-apr 14566	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
cdr 14578	class DivRing
cfield 14579	class Field
df-drngap 14580	|- DivRing = { r e. Ring | (#r ` r ) TAp ( Base ` r ) }
df-field 14581	|- Field = ( DivRing i^i CRing )
clmod 14599	class LMod
cscaf 14600	class .sf
df-lmod 14601	|- 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 14602	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14664	class LSubSp
df-lssm 14665	|- 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 14698	class LSpan
df-lsp 14699	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14745	class subringAlg
crglmod 14746	class ringLMod
df-sra 14747	|- 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 14748	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14779	class LIdeal
crsp 14780	class RSpan
df-lidl 14781	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14782	|- RSpan = ( LSpan o. ringLMod )
c2idl 14811	class 2Ideal
df-2idl 14812	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14847	class PsMet
cxmet 14848	class *Met
cmet 14849	class Met
cbl 14850	class ball
cfbas 14851	class fBas
cfg 14852	class filGen
cmopn 14853	class MetOpen
cmetu 14854	class metUnif
df-psmet 14855	|- 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 14856	|- *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 14857	|- 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 14858	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14859	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14860	|- 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 14861	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14862	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14868	class ℂfld
df-cnfld 14869	|- ℂ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 14900	class ℤring
df-zring 14901	|- ℤring = (ℂfld ↾s ZZ )
czrh 14921	class ZRHom
czlm 14922	class ZMod
czn 14923	class ℤ/nℤ
df-zrh 14924	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14925	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14926	|- ℤ/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 14971	class mPwSer
cmpl 14972	class mPoly
df-psr 14973	|- 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 14974	|- 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 15024	class Top
df-top 15025	|- 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 15037	class TopOn
df-topon 15038	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 15057	class TopSp
df-topsp 15058	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 15069	class TopBases
df-bases 15070	|- 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 15119	class Clsd
cnt 15120	class int
ccl 15121	class cls
df-cld 15122	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 15123	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 15124	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 15165	class nei
df-nei 15166	|- 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 15212	class Cn
ccnp 15213	class CnP
clm 15214	class ~~> t
df-cn 15215	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 15216	|- 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 15217	|- ~~> 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 15279	class tX
df-tx 15280	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15327	class Homeo
df-hmeo 15328	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15363	class *MetSp
cms 15364	class MetSp
ctms 15365	class toMetSp
df-xms 15366	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15367	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15368	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15597	class -cn->
df-cncf 15598	|- -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 15681	class lim CC
cdv 15682	class _D
df-limced 15683	|- 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 15684	|- _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 15755	class Poly
cidp 15756	class Xp
df-ply 15757	|- 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 15758	|- Xp = ( _I |` CC )
clog 15883	class log
ccxp 15884	class ^c
df-relog 15885	|- log = `' ( exp |` RR )
df-rpcxp 15886	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15971	class logb
df-logb 15972	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 16012	class sigma
df-sgm 16013	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 16033	class /L
df-lgs 16034	|- /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 16162	class .ef
df-edgf 16163	|- .ef = Slot ; 1 8
cvtx 16170	class Vtx
ciedg 16171	class iEdg
df-vtx 16172	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 16173	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 16215	class Edg
df-edg 16216	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 16225	class UHGraph
cushgr 16226	class USHGraph
df-uhgrm 16227	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 16228	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 16249	class UPGraph
cumgr 16250	class UMGraph
df-upgren 16251	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 16252	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16311	class USPGraph
cusgr 16312	class USGraph
df-uspgren 16313	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16314	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16411	class SubGraph
df-subgr 16412	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16444	class VtxDeg
df-vtxdg 16445	|- 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 16475	class Walks
df-wlks 16476	|- 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 16538	class Trails
df-trls 16539	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16549	class ClWWalks
df-clwwlk 16550	|- 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 16561	class ClWWalksN
df-clwwlkn 16562	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16584	class ClWWalksNOn
df-clwwlknon 16585	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16600	class EulerPaths
df-eupth 16601	|- 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 16738	wff A DECIDin B
df-dcin 16739	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16755	wff BOUNDED ph
ax-bd0 16756	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16757	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16758	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16759	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16760	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16761	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16762	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16763	|- BOUNDED x = y
ax-bdel 16764	|- BOUNDED x e. y
ax-bdsb 16765	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16783	wff BOUNDED A
df-bdc 16784	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16827	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16867	|- BOUNDED ph   =>    |- DECID ph
wind 16869	wff Ind A
df-bj-ind 16870	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16884	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16911	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16919	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16925	|- 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 16930	|- 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 16932	|- ( ( ( 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 ) ) )
wals 17034	wff A.E. x ( ph -> ps )
wrals 17035	wff A.E. x e. A ( ph -> ps )
df-als 17036	|- ( A.E. x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-rals 17037	|- ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )