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 3709	class { A }
cpr 3710	class { A , B }
ctp 3711	class { A , B , C }
cop 3712	class <. A , B >.
cotp 3713	class <. A , B , C >.
df-sn 3715	|- { A } = { x | x = A }
df-pr 3716	|- { A , B } = ( { A } u. { B } )
df-tp 3717	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3718	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3719	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3935	class U. A
df-uni 3936	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3970	class |^| A
df-int 3971	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 4012	class U_ x e. A B
ciin 4013	class |^|_ x e. A B
df-iun 4014	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 4015	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4106	wff Disj x e. A B
df-disj 4107	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4130	wff A R B
df-br 4131	|- ( A R B <-> <. A , B >. e. R )
copab 4191	class { <. x , y >. | ph }
cmpt 4192	class ( x e. A |-> B )
df-opab 4193	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4194	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4229	wff Tr A
df-tr 4230	|- ( Tr A <-> U. A C_ A )
ax-coll 4246	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4249	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4259	|- E. x A. y -. y e. x
ax-pow 4311	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4331	wff EXMID
df-exmid 4332	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4346	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4432	class _E
cid 4433	class _I
df-eprel 4434	|- _E = { <. x , y >. | x e. y }
df-id 4438	|- _I = { <. x , y >. | x = y }
wpo 4439	wff R Po A
wor 4440	wff R Or A
df-po 4441	|- ( 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 4442	|- ( 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 4472	wff FrFor R A S
wfr 4473	wff R Fr A
wse 4474	wff R Se A
wwe 4475	wff R We A
df-frfor 4476	|- (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 4477	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4478	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4479	|- ( 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 4507	wff Ord A
con0 4508	class On
wlim 4509	wff Lim A
csuc 4510	class suc A
df-iord 4511	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4513	|- On = { x | Ord x }
df-ilim 4514	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4516	|- suc A = ( A u. { A } )
ax-un 4578	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4684	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4735	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4737	class om
df-iom 4738	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4772	class ( A X. B )
ccnv 4773	class `' A
cdm 4774	class dom A
crn 4775	class ran A
cres 4776	class ( A |` B )
cima 4777	class ( A " B )
ccom 4778	class ( A o. B )
wrel 4779	wff Rel A
df-xp 4780	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4781	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4782	|- `' A = { <. x , y >. | y A x }
df-co 4783	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4784	|- dom A = { x | E. y x A y }
df-rn 4785	|- ran A = dom `' A
df-res 4786	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4787	|- ( A " B ) = ran ( A |` B )
cio 5335	class ( iota x ph )
df-iota 5337	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5371	wff Fun A
wfn 5372	wff A Fn B
wf 5373	wff F : A --> B
wf1 5374	wff F : A -1-1-> B
wfo 5375	wff F : A -onto-> B
wf1o 5376	wff F : A -1-1-onto-> B
cfv 5377	class ( F ` A )
wiso 5378	wff H Isom R , S ( A , B )
df-fun 5379	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5380	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5381	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5382	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5383	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5384	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5385	|- ( F ` A ) = ( iota x A F x )
df-isom 5386	|- ( 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 6037	class ( iota_ x e. A ph )
df-riota 6038	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6085	class ( A F B )
coprab 6086	class { <. <. x , y >. , z >. | ph }
cmpo 6087	class ( x e. A , y e. B |-> C )
df-ov 6088	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6089	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6090	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6300	class oF R
cofr 6301	class oR R
df-of 6302	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6303	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6372	class 1st
c2nd 6373	class 2nd
df-1st 6374	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6375	|- 2nd = ( x e. _V |-> U. ran { x } )
csupp 6475	class supp
df-supp 6476	|- supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
ctpos 6515	class tpos F
df-tpos 6516	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6556	wff Smo A
df-smo 6557	|- ( 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 6575	class recs ( F )
df-recs 6576	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6640	class rec ( F , I )
df-irdg 6641	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6661	class frec ( F , I )
df-frec 6662	|- 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 6680	class 1o
c2o 6681	class 2o
c3o 6682	class 3o
c4o 6683	class 4o
coa 6684	class +o
comu 6685	class .o
coei 6686	class ↑o
df-1o 6687	|- 1o = suc (/)
df-2o 6688	|- 2o = suc 1o
df-3o 6689	|- 3o = suc 2o
df-4o 6690	|- 4o = suc 3o
df-oadd 6691	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6692	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6693	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6804	wff R Er A
cec 6805	class [ A ] R
cqs 6806	class ( A /. R )
df-er 6807	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6809	|- [ A ] R = ( R " { A } )
df-qs 6813	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6922	class ^m
cpm 6923	class ^pm
df-map 6924	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6925	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6980	class X_ x e. A B
df-ixp 6981	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 7020	class ~~
cdom 7021	class ~<_
cfn 7022	class Fin
df-en 7023	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 7024	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 7025	|- Fin = { x | E. y e. om x ~~ y }
cfsupp 7285	class finSupp
df-fsupp 7286	|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
cfi 7302	class fi
df-fi 7303	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7323	class sup ( A , B , R )
cinf 7324	class inf ( A , B , R )
df-sup 7325	|- 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 7326	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7378	class ( A ⊔ B )
df-dju 7379	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7386	class inl
cinr 7387	class inr
df-inl 7388	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7389	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7424	class case ( R , S )
df-case 7425	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7443	class ( R ⊔d S )
df-djud 7444	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7460	class ℕ∞
df-nninf 7461	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7475	class Omni
df-omni 7476	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7492	class Markov
df-markov 7493	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7504	class WOmni
df-womni 7505	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7523	class card
wacn 7524	class AC A
df-card 7525	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7526	|- 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 7562	wff CHOICE
df-ac 7563	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7608	wff R Ap A
df-pap 7609	|- ( 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 7615	wff R TAp A
df-tap 7616	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7629	wff CCHOICE
df-cc 7630	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7640	class N.
cpli 7641	class +N
cmi 7642	class .N
clti 7643	class <N
cplpq 7644	class +pQ
cmpq 7645	class .pQ
cltpq 7646	class <pQ
ceq 7647	class ~Q
cnq 7648	class Q.
c1q 7649	class 1Q
cplq 7650	class +Q
cmq 7651	class .Q
crq 7652	class *Q
cltq 7653	class <Q
ceq0 7654	class ~Q0
cnq0 7655	class Q0
c0q0 7656	class 0Q0
cplq0 7657	class +Q0
cmq0 7658	class ·Q0
cnp 7659	class P.
c1p 7660	class 1P
cpp 7661	class +P.
cmp 7662	class .P.
cltp 7663	class <P
cer 7664	class ~R
cnr 7665	class R.
c0r 7666	class 0R
c1r 7667	class 1R
cm1r 7668	class -1R
cplr 7669	class +R
cmr 7670	class .R
cltr 7671	class <R
df-ni 7672	|- N. = ( om \ { (/) } )
df-pli 7673	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7674	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7675	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7712	|- +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 7713	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7714	|- <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 7715	|- ~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 7716	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7717	|- +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 7718	|- .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 7719	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7720	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7721	|- <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 7792	|- ~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 7793	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7794	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7795	|- +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 7796	|- ·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 7834	|- 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 7835	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7836	|- +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 7837	|- .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 7838	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 8094	|- ~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 8095	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 8096	|- +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 8097	|- .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 8098	|- <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 8099	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 8100	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 8101	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8178	class CC
cr 8179	class RR
cc0 8180	class 0
c1 8181	class 1
ci 8182	class _i
caddc 8183	class +
cltrr 8184	class <RR
cmul 8185	class x.
df-c 8186	|- CC = ( R. X. R. )
df-0 8187	|- 0 = <. 0R , 0R >.
df-1 8188	|- 1 = <. 1R , 0R >.
df-i 8189	|- _i = <. 0R , 1R >.
df-r 8190	|- RR = ( R. X. { 0R } )
df-add 8191	|- + = { <. <. 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 8192	|- 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 8193	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8271	|- CC e. _V
ax-resscn 8272	|- RR C_ CC
ax-1cn 8273	|- 1 e. CC
ax-1re 8274	|- 1 e. RR
ax-icn 8275	|- _i e. CC
ax-addcl 8276	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8277	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8278	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8279	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8280	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8281	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8282	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8283	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8284	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8285	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8286	|- 0 <RR 1
ax-1rid 8287	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8288	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8289	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8290	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8291	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8292	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8293	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8294	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8295	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8296	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8297	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8298	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8299	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8300	|- 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 8301	|- ( ( ( 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 8302	|- + : ( CC X. CC ) --> CC
ax-mulf 8303	|- x. : ( CC X. CC ) --> CC
cpnf 8358	class +oo
cmnf 8359	class -oo
cxr 8360	class RR*
clt 8361	class <
cle 8362	class <_
df-pnf 8363	|- +oo = ~P U. CC
df-mnf 8364	|- -oo = ~P +oo
df-xr 8365	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8366	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8367	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8499	class -
cneg 8500	class -u A
df-sub 8501	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8502	|- -u A = ( 0 - A )
creap 8905	class #ℝ
df-reap 8906	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8912	class #
df-ap 8913	|- # = { <. 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 9005	class /
df-div 9006	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cind 9296	class 𝟭
df-ind 9297	|- 𝟭 = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )
cn 9307	class NN
df-inn 9308	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9358	class 2
c3 9359	class 3
c4 9360	class 4
c5 9361	class 5
c6 9362	class 6
c7 9363	class 7
c8 9364	class 8
c9 9365	class 9
df-2 9366	|- 2 = ( 1 + 1 )
df-3 9367	|- 3 = ( 2 + 1 )
df-4 9368	|- 4 = ( 3 + 1 )
df-5 9369	|- 5 = ( 4 + 1 )
df-6 9370	|- 6 = ( 5 + 1 )
df-7 9371	|- 7 = ( 6 + 1 )
df-8 9372	|- 8 = ( 7 + 1 )
df-9 9373	|- 9 = ( 8 + 1 )
cn0 9568	class NN0
df-n0 9569	|- NN0 = ( NN u. { 0 } )
cxnn0 9635	class NN0*
df-xnn0 9636	|- NN0* = ( NN0 u. { +oo } )
cz 9649	class ZZ
df-z 9650	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9782	class ; A B
df-dec 9783	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9931	class ZZ>=
df-uz 9932	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 10029	class QQ
df-q 10030	|- QQ = ( / " ( ZZ X. NN ) )
crp 10065	class RR+
df-rp 10066	|- RR+ = { x e. RR | 0 < x }
cxne 10182	class -e A
cxad 10183	class +e
cxmu 10184	class xe
df-xneg 10185	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10186	|- +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 10187	|- 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 10301	class (,)
cioc 10302	class (,]
cico 10303	class [,)
cicc 10304	class [,]
df-ioo 10305	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10306	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10307	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10308	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10422	class ...
df-fz 10423	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10560	class ..^
df-fzo 10561	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10714	class |_
cceil 10715	class ⌈
df-fl 10716	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10717	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10774	class mod
df-mod 10775	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10899	class seq M ( .+ , F )
df-seqfrec 10900	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10990	class ^
df-exp 10991	|- ^ = ( 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 11179	class !
df-fac 11180	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11201	class _C
df-bc 11202	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11230	class ♯
df-ihash 11231	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11320	class Word S
df-word 11321	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11365	class lastS
df-lsw 11366	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11374	class ++
df-concat 11375	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11399	class <" A ">
df-s1 11400	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11433	class substr
df-substr 11434	|- 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 11460	class prefix
df-pfx 11461	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11537	class <" A B ">
cs3 11538	class <" A B C ">
cs4 11539	class <" A B C D ">
cs5 11540	class <" A B C D E ">
cs6 11541	class <" A B C D E F ">
cs7 11542	class <" A B C D E F G ">
cs8 11543	class <" A B C D E F G H ">
df-s2 11544	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11545	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11546	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11547	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11548	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11549	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11550	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11595	class shift
df-shft 11596	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11620	class *
cre 11621	class Re
cim 11622	class Im
df-cj 11623	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11624	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11625	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11778	class sqr
cabs 11779	class abs
df-rsqrt 11780	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11781	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 12063	class ~~>
df-clim 12064	|- ~~> = { <. 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 12138	class sum_ k e. A B
df-sumdc 12139	|- 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 12336	class prod_ k e. A B
df-proddc 12337	|- 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 12428	class exp
ceu 12429	class _e
csin 12430	class sin
ccos 12431	class cos
ctan 12432	class tan
cpi 12433	class pi
df-ef 12434	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12435	|- _e = ( exp ` 1 )
df-sin 12436	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12437	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12438	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12439	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12561	class tau
df-tau 12562	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12573	class ||
df-dvds 12574	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12726	class bits
df-bits 12727	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12749	class gcd
df-gcd 12750	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12857	class lcm
df-lcm 12858	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12904	class Prime
df-prm 12905	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12980	class numer
cdenom 12981	class denom
df-numer 12982	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12983	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 13009	class odZ
cphi 13010	class phi
df-odz 13011	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 13012	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 13086	class pCnt
df-pc 13087	|- 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 13171	class ZZ[_i]
df-gz 13172	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13400	class Struct
cnx 13401	class ndx
csts 13402	class sSet
cslot 13403	class Slot A
cbs 13404	class Base
cress 13405	class ↾s
df-struct 13406	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13407	|- ndx = ( _I |` NN )
df-slot 13408	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13410	|- Base = Slot 1
df-sets 13411	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13412	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13484	class +g
cmulr 13485	class .r
cstv 13486	class *r
csca 13487	class Scalar
cvsca 13488	class .s
cip 13489	class .i
cts 13490	class TopSet
cple 13491	class le
coc 13492	class oc
cds 13493	class dist
cunif 13494	class UnifSet
chom 13495	class Hom
cco 13496	class comp
df-plusg 13497	|- +g = Slot 2
df-mulr 13498	|- .r = Slot 3
df-starv 13499	|- *r = Slot 4
df-sca 13500	|- Scalar = Slot 5
df-vsca 13501	|- .s = Slot 6
df-ip 13502	|- .i = Slot 8
df-tset 13503	|- TopSet = Slot 9
df-ple 13504	|- le = Slot ; 1 0
df-ocomp 13505	|- oc = Slot ; 1 1
df-ds 13506	|- dist = Slot ; 1 2
df-unif 13507	|- UnifSet = Slot ; 1 3
df-hom 13508	|- Hom = Slot ; 1 4
df-cco 13509	|- comp = Slot ; 1 5
crest 13646	class ↾t
ctopn 13647	class TopOpen
df-rest 13648	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13649	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13661	class topGen
cpt 13662	class Xt_
c0g 13663	class 0g
cgzsu 13664	class gzsumgz
df-0g 13665	|- 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 13666	|- 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 13667	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13668	|- 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 13675	class "s
cqus 13676	class /.s
df-iimas 13677	|- "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 13678	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
cplusf 13726	class +f
cmgm 13727	class Mgm
df-plusf 13728	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13729	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13769	class Smgrp
df-sgrp 13770	|- 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 13782	class Mnd
df-mnd 13783	|- 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 13817	class MndHom
csubmnd 13818	class SubMnd
df-mhm 13819	|- 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 13820	|- 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 13858	class Grp
cminusg 13859	class invg
csg 13860	class -g
df-grp 13861	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13862	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13863	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13975	class .g
df-mulg 13976	|- .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 14023	class SubGrp
cnsg 14024	class NrmSGrp
cqg 14025	class ~QG
df-subg 14026	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 14027	|- 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 14028	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 14096	class GrpHom
df-ghm 14097	|- 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 ) ) ) } )
ccntz 14140	class Cntz
ccntr 14141	class Cntr
df-cntz 14142	|- Cntz = ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) )
df-cntr 14143	|- Cntr = ( m e. _V |-> ( (Cntz ` m ) ` ( Base ` m ) ) )
ccmn 14171	class CMnd
cabl 14172	class Abel
df-cmn 14173	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 14174	|- Abel = ( Grp i^i CMnd )
cgsu 14234	class gsumg
df-gsumfi 14235	|- 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 14253	class X_s
df-prds 14254	|- 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 14283	class X.s
df-xps 14284	|- 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 14286	class ^s
df-pws 14287	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cmgp 14301	class mulGrp
df-mgp 14302	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 14315	class Rng
df-rng 14316	|- 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 14346	class 1r
df-ur 14347	|- 1r = ( 0g o. mulGrp )
csrg 14351	class SRing
df-srg 14352	|- 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 14384	class Ring
ccrg 14385	class CRing
df-ring 14386	|- 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 14387	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14456	class oppr
df-oppr 14457	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14476	class ||r
cui 14477	class Unit
cir 14478	class Irred
df-dvdsr 14479	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14480	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14481	|- 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 14511	class invr
df-invr 14512	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14522	class /r
df-dvr 14523	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14541	class RingHom
crs 14542	class RingIso
df-rhm 14543	|- 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 14544	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14570	class NzRing
df-nzr 14571	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14581	class LRing
df-lring 14582	|- 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 14589	class SubRng
df-subrng 14590	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14609	class SubRing
crgspn 14610	class RingSpan
df-subrg 14611	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14612	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14647	class RLReg
cdomn 14648	class Domn
cidom 14649	class IDomn
df-rlreg 14650	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14651	|- 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 14652	|- IDomn = ( CRing i^i Domn )
capr 14673	class #r
df-apr 14674	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
cdr 14686	class DivRing
cfield 14687	class Field
df-drngap 14688	|- DivRing = { r e. Ring | (#r ` r ) TAp ( Base ` r ) }
df-field 14689	|- Field = ( DivRing i^i CRing )
clmod 14707	class LMod
cscaf 14708	class .sf
df-lmod 14709	|- 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 14710	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14773	class LSubSp
df-lssm 14774	|- 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 14807	class LSpan
df-lsp 14808	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14854	class subringAlg
crglmod 14855	class ringLMod
df-sra 14856	|- 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 14857	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14888	class LIdeal
crsp 14889	class RSpan
df-lidl 14890	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14891	|- RSpan = ( LSpan o. ringLMod )
c2idl 14920	class 2Ideal
df-2idl 14921	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14956	class PsMet
cxmet 14957	class *Met
cmet 14958	class Met
cbl 14959	class ball
cfbas 14960	class fBas
cfg 14961	class filGen
cmopn 14962	class MetOpen
cmetu 14963	class metUnif
df-psmet 14964	|- 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 14965	|- *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 14966	|- 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 14967	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14968	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14969	|- 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 14970	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14971	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14977	class ℂfld
df-cnfld 14978	|- ℂ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 15009	class ℤring
df-zring 15010	|- ℤring = (ℂfld ↾s ZZ )
czrh 15030	class ZRHom
czlm 15031	class ZMod
czn 15032	class ℤ/nℤ
df-zrh 15033	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 15034	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 15035	|- ℤ/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 ) >. ) )
casa 15080	class AssAlg
casp 15081	class AlgSpan
cascl 15082	class algSc
df-assa 15083	|- AssAlg = { w e. ( LMod i^i Ring ) | [. (Scalar ` w ) / f ]. A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) }
df-asp 15084	|- AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )
df-ascl 15085	|- algSc = ( w e. _V |-> ( x e. ( Base ` (Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) )
cmps 15129	class mPwSer
cmpl 15130	class mPoly
df-psr 15131	|- 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 15132	|- 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 15189	class Top
df-top 15190	|- 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 15202	class TopOn
df-topon 15203	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 15222	class TopSp
df-topsp 15223	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 15234	class TopBases
df-bases 15235	|- 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 15284	class Clsd
cnt 15285	class int
ccl 15286	class cls
df-cld 15287	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 15288	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 15289	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 15330	class nei
df-nei 15331	|- 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 15377	class Cn
ccnp 15378	class CnP
clm 15379	class ~~> t
df-cn 15380	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 15381	|- 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 15382	|- ~~> 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 15444	class tX
df-tx 15445	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15492	class Homeo
df-hmeo 15493	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15528	class *MetSp
cms 15529	class MetSp
ctms 15530	class toMetSp
df-xms 15531	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15532	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15533	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15762	class -cn->
df-cncf 15763	|- -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 15846	class lim CC
cdv 15847	class _D
df-limced 15848	|- 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 15849	|- _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 15920	class Poly
cidp 15921	class Xp
df-ply 15922	|- 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 15923	|- Xp = ( _I |` CC )
clog 16049	class log
ccxp 16050	class ^c
df-relog 16051	|- log = `' ( exp |` RR )
df-rpcxp 16052	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 16140	class logb
df-logb 16141	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
ccht 16194	class theta
cppi 16195	class π
csgm 16196	class sigma
df-cht 16197	|- theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )
df-ppi 16198	|- π = ( x e. RR |-> (♯ ` ( ( 0 [,] x ) i^i Prime ) ) )
df-sgm 16199	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 16282	class /L
df-lgs 16283	|- /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 16411	class .ef
df-edgf 16412	|- .ef = Slot ; 1 8
cvtx 16419	class Vtx
ciedg 16420	class iEdg
df-vtx 16421	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 16422	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 16464	class Edg
df-edg 16465	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 16474	class UHGraph
cushgr 16475	class USHGraph
df-uhgrm 16476	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 16477	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 16498	class UPGraph
cumgr 16499	class UMGraph
df-upgren 16500	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 16501	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16560	class USPGraph
cusgr 16561	class USGraph
df-uspgren 16562	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16563	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16660	class SubGraph
df-subgr 16661	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16693	class VtxDeg
df-vtxdg 16694	|- 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 16724	class Walks
df-wlks 16725	|- 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 16787	class Trails
df-trls 16788	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16798	class ClWWalks
df-clwwlk 16799	|- 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 16810	class ClWWalksN
df-clwwlkn 16811	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16833	class ClWWalksNOn
df-clwwlknon 16834	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16849	class EulerPaths
df-eupth 16850	|- 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 16987	wff A DECIDin B
df-dcin 16988	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 17004	wff BOUNDED ph
ax-bd0 17005	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 17006	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 17007	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 17008	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 17009	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 17010	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 17011	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 17012	|- BOUNDED x = y
ax-bdel 17013	|- BOUNDED x e. y
ax-bdsb 17014	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 17032	wff BOUNDED A
df-bdc 17033	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 17076	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 17116	|- BOUNDED ph   =>    |- DECID ph
wind 17118	wff Ind A
df-bj-ind 17119	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 17133	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 17160	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 17168	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 17174	|- 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 17179	|- 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 17181	|- ( ( ( 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 ) ) )
wwem 17206	wff WEXMID
df-wexmid 17207	|- (WEXMID <-> A. p e. ~P 1o ( -. p = 1o \/ -. -. p = 1o ) )
wals 17293	wff A.E. x ( ph -> ps )
wrals 17294	wff A.E. x e. A ( ph -> ps )
df-als 17295	|- ( A.E. x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-rals 17296	|- ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
walseu 17327	wff A.E! x ( ph -> ps )
wralseu 17328	wff A.E! x e. A ( ph -> ps )
df-alseu 17329	|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
df-ralseu 17330	|- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )