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 7322	class sup ( A , B , R )
cinf 7323	class inf ( A , B , R )
df-sup 7324	|- 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 7325	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7377	class ( A ⊔ B )
df-dju 7378	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7385	class inl
cinr 7386	class inr
df-inl 7387	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7388	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7423	class case ( R , S )
df-case 7424	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7442	class ( R ⊔d S )
df-djud 7443	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7459	class ℕ∞
df-nninf 7460	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7474	class Omni
df-omni 7475	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7491	class Markov
df-markov 7492	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7503	class WOmni
df-womni 7504	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7522	class card
wacn 7523	class AC A
df-card 7524	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7525	|- 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 7561	wff CHOICE
df-ac 7562	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7607	wff R Ap A
df-pap 7608	|- ( 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 7614	wff R TAp A
df-tap 7615	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7628	wff CCHOICE
df-cc 7629	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7639	class N.
cpli 7640	class +N
cmi 7641	class .N
clti 7642	class <N
cplpq 7643	class +pQ
cmpq 7644	class .pQ
cltpq 7645	class <pQ
ceq 7646	class ~Q
cnq 7647	class Q.
c1q 7648	class 1Q
cplq 7649	class +Q
cmq 7650	class .Q
crq 7651	class *Q
cltq 7652	class <Q
ceq0 7653	class ~Q0
cnq0 7654	class Q0
c0q0 7655	class 0Q0
cplq0 7656	class +Q0
cmq0 7657	class ·Q0
cnp 7658	class P.
c1p 7659	class 1P
cpp 7660	class +P.
cmp 7661	class .P.
cltp 7662	class <P
cer 7663	class ~R
cnr 7664	class R.
c0r 7665	class 0R
c1r 7666	class 1R
cm1r 7667	class -1R
cplr 7668	class +R
cmr 7669	class .R
cltr 7670	class <R
df-ni 7671	|- N. = ( om \ { (/) } )
df-pli 7672	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7673	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7674	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7711	|- +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 7712	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7713	|- <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 7714	|- ~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 7715	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7716	|- +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 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-1nqqs 7718	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7719	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7720	|- <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 7791	|- ~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 7792	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7793	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7794	|- +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 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 u ) , ( v .o f ) >. ] ~Q0 ) ) }
df-inp 7833	|- 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 7834	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7835	|- +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 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-iltp 7837	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 8093	|- ~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 8094	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 8095	|- +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 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 ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R ) ) }
df-ltr 8097	|- <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 8098	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 8099	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 8100	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8177	class CC
cr 8178	class RR
cc0 8179	class 0
c1 8180	class 1
ci 8181	class _i
caddc 8182	class +
cltrr 8183	class <RR
cmul 8184	class x.
df-c 8185	|- CC = ( R. X. R. )
df-0 8186	|- 0 = <. 0R , 0R >.
df-1 8187	|- 1 = <. 1R , 0R >.
df-i 8188	|- _i = <. 0R , 1R >.
df-r 8189	|- RR = ( R. X. { 0R } )
df-add 8190	|- + = { <. <. 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 8191	|- 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 8192	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8270	|- CC e. _V
ax-resscn 8271	|- RR C_ CC
ax-1cn 8272	|- 1 e. CC
ax-1re 8273	|- 1 e. RR
ax-icn 8274	|- _i e. CC
ax-addcl 8275	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8276	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8277	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8278	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8279	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8280	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8281	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8282	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8283	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8284	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8285	|- 0 <RR 1
ax-1rid 8286	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8287	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8288	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8289	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8290	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8291	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8292	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8293	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8294	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8295	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8296	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8297	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8298	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8299	|- 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 8300	|- ( ( ( 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 8301	|- + : ( CC X. CC ) --> CC
ax-mulf 8302	|- x. : ( CC X. CC ) --> CC
cpnf 8357	class +oo
cmnf 8358	class -oo
cxr 8359	class RR*
clt 8360	class <
cle 8361	class <_
df-pnf 8362	|- +oo = ~P U. CC
df-mnf 8363	|- -oo = ~P +oo
df-xr 8364	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8365	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8366	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8498	class -
cneg 8499	class -u A
df-sub 8500	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8501	|- -u A = ( 0 - A )
creap 8904	class #ℝ
df-reap 8905	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8911	class #
df-ap 8912	|- # = { <. 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 9004	class /
df-div 9005	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cind 9295	class 𝟭
df-ind 9296	|- 𝟭 = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )
cn 9306	class NN
df-inn 9307	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9357	class 2
c3 9358	class 3
c4 9359	class 4
c5 9360	class 5
c6 9361	class 6
c7 9362	class 7
c8 9363	class 8
c9 9364	class 9
df-2 9365	|- 2 = ( 1 + 1 )
df-3 9366	|- 3 = ( 2 + 1 )
df-4 9367	|- 4 = ( 3 + 1 )
df-5 9368	|- 5 = ( 4 + 1 )
df-6 9369	|- 6 = ( 5 + 1 )
df-7 9370	|- 7 = ( 6 + 1 )
df-8 9371	|- 8 = ( 7 + 1 )
df-9 9372	|- 9 = ( 8 + 1 )
cn0 9567	class NN0
df-n0 9568	|- NN0 = ( NN u. { 0 } )
cxnn0 9634	class NN0*
df-xnn0 9635	|- NN0* = ( NN0 u. { +oo } )
cz 9648	class ZZ
df-z 9649	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9781	class ; A B
df-dec 9782	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9930	class ZZ>=
df-uz 9931	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 10028	class QQ
df-q 10029	|- QQ = ( / " ( ZZ X. NN ) )
crp 10064	class RR+
df-rp 10065	|- RR+ = { x e. RR | 0 < x }
cxne 10181	class -e A
cxad 10182	class +e
cxmu 10183	class xe
df-xneg 10184	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10185	|- +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 10186	|- 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 10300	class (,)
cioc 10301	class (,]
cico 10302	class [,)
cicc 10303	class [,]
df-ioo 10304	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10305	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10306	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10307	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10421	class ...
df-fz 10422	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10559	class ..^
df-fzo 10560	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10713	class |_
cceil 10714	class ⌈
df-fl 10715	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10716	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10772	class mod
df-mod 10773	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10897	class seq M ( .+ , F )
df-seqfrec 10898	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10988	class ^
df-exp 10989	|- ^ = ( 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 11177	class !
df-fac 11178	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11199	class _C
df-bc 11200	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11228	class ♯
df-ihash 11229	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11318	class Word S
df-word 11319	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11363	class lastS
df-lsw 11364	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11372	class ++
df-concat 11373	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11397	class <" A ">
df-s1 11398	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11431	class substr
df-substr 11432	|- 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 11458	class prefix
df-pfx 11459	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11535	class <" A B ">
cs3 11536	class <" A B C ">
cs4 11537	class <" A B C D ">
cs5 11538	class <" A B C D E ">
cs6 11539	class <" A B C D E F ">
cs7 11540	class <" A B C D E F G ">
cs8 11541	class <" A B C D E F G H ">
df-s2 11542	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11543	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11544	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11545	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11546	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11547	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11548	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11593	class shift
df-shft 11594	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11618	class *
cre 11619	class Re
cim 11620	class Im
df-cj 11621	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11622	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11623	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11776	class sqr
cabs 11777	class abs
df-rsqrt 11778	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11779	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 12060	class ~~>
df-clim 12061	|- ~~> = { <. 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 12135	class sum_ k e. A B
df-sumdc 12136	|- 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 12333	class prod_ k e. A B
df-proddc 12334	|- 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 12425	class exp
ceu 12426	class _e
csin 12427	class sin
ccos 12428	class cos
ctan 12429	class tan
cpi 12430	class pi
df-ef 12431	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12432	|- _e = ( exp ` 1 )
df-sin 12433	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12434	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12435	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12436	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12558	class tau
df-tau 12559	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12570	class ||
df-dvds 12571	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12723	class bits
df-bits 12724	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12746	class gcd
df-gcd 12747	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12854	class lcm
df-lcm 12855	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12901	class Prime
df-prm 12902	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12977	class numer
cdenom 12978	class denom
df-numer 12979	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12980	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 13006	class odZ
cphi 13007	class phi
df-odz 13008	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 13009	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 13083	class pCnt
df-pc 13084	|- 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 13168	class ZZ[_i]
df-gz 13169	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13397	class Struct
cnx 13398	class ndx
csts 13399	class sSet
cslot 13400	class Slot A
cbs 13401	class Base
cress 13402	class ↾s
df-struct 13403	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13404	|- ndx = ( _I |` NN )
df-slot 13405	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13407	|- Base = Slot 1
df-sets 13408	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13409	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13480	class +g
cmulr 13481	class .r
cstv 13482	class *r
csca 13483	class Scalar
cvsca 13484	class .s
cip 13485	class .i
cts 13486	class TopSet
cple 13487	class le
coc 13488	class oc
cds 13489	class dist
cunif 13490	class UnifSet
chom 13491	class Hom
cco 13492	class comp
df-plusg 13493	|- +g = Slot 2
df-mulr 13494	|- .r = Slot 3
df-starv 13495	|- *r = Slot 4
df-sca 13496	|- Scalar = Slot 5
df-vsca 13497	|- .s = Slot 6
df-ip 13498	|- .i = Slot 8
df-tset 13499	|- TopSet = Slot 9
df-ple 13500	|- le = Slot ; 1 0
df-ocomp 13501	|- oc = Slot ; 1 1
df-ds 13502	|- dist = Slot ; 1 2
df-unif 13503	|- UnifSet = Slot ; 1 3
df-hom 13504	|- Hom = Slot ; 1 4
df-cco 13505	|- comp = Slot ; 1 5
crest 13642	class ↾t
ctopn 13643	class TopOpen
df-rest 13644	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13645	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13657	class topGen
cpt 13658	class Xt_
c0g 13659	class 0g
cgzsu 13660	class gzsumgz
df-0g 13661	|- 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 13662	|- 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 13663	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13664	|- 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 13671	class "s
cqus 13672	class /.s
df-iimas 13673	|- "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 13674	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
cplusf 13722	class +f
cmgm 13723	class Mgm
df-plusf 13724	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13725	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13765	class Smgrp
df-sgrp 13766	|- 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 13778	class Mnd
df-mnd 13779	|- 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 13813	class MndHom
csubmnd 13814	class SubMnd
df-mhm 13815	|- 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 13816	|- 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 13854	class Grp
cminusg 13855	class invg
csg 13856	class -g
df-grp 13857	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13858	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13859	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13971	class .g
df-mulg 13972	|- .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 14019	class SubGrp
cnsg 14020	class NrmSGrp
cqg 14021	class ~QG
df-subg 14022	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 14023	|- 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 14024	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 14092	class GrpHom
df-ghm 14093	|- 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 14136	class CMnd
cabl 14137	class Abel
df-cmn 14138	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 14139	|- Abel = ( Grp i^i CMnd )
cgsu 14199	class gsumg
df-gsumfi 14200	|- 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 14218	class X_s
df-prds 14219	|- 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 14248	class X.s
df-xps 14249	|- 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 14251	class ^s
df-pws 14252	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cmgp 14266	class mulGrp
df-mgp 14267	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 14280	class Rng
df-rng 14281	|- 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 14311	class 1r
df-ur 14312	|- 1r = ( 0g o. mulGrp )
csrg 14316	class SRing
df-srg 14317	|- 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 14349	class Ring
ccrg 14350	class CRing
df-ring 14351	|- 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 14352	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14421	class oppr
df-oppr 14422	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14441	class ||r
cui 14442	class Unit
cir 14443	class Irred
df-dvdsr 14444	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14445	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14446	|- 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 14476	class invr
df-invr 14477	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14487	class /r
df-dvr 14488	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14506	class RingHom
crs 14507	class RingIso
df-rhm 14508	|- 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 14509	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14535	class NzRing
df-nzr 14536	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14546	class LRing
df-lring 14547	|- 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 14554	class SubRng
df-subrng 14555	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14574	class SubRing
crgspn 14575	class RingSpan
df-subrg 14576	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14577	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14612	class RLReg
cdomn 14613	class Domn
cidom 14614	class IDomn
df-rlreg 14615	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14616	|- 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 14617	|- IDomn = ( CRing i^i Domn )
capr 14638	class #r
df-apr 14639	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
cdr 14651	class DivRing
cfield 14652	class Field
df-drngap 14653	|- DivRing = { r e. Ring | (#r ` r ) TAp ( Base ` r ) }
df-field 14654	|- Field = ( DivRing i^i CRing )
clmod 14672	class LMod
cscaf 14673	class .sf
df-lmod 14674	|- 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 14675	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14738	class LSubSp
df-lssm 14739	|- 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 14772	class LSpan
df-lsp 14773	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14819	class subringAlg
crglmod 14820	class ringLMod
df-sra 14821	|- 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 14822	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14853	class LIdeal
crsp 14854	class RSpan
df-lidl 14855	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14856	|- RSpan = ( LSpan o. ringLMod )
c2idl 14885	class 2Ideal
df-2idl 14886	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14921	class PsMet
cxmet 14922	class *Met
cmet 14923	class Met
cbl 14924	class ball
cfbas 14925	class fBas
cfg 14926	class filGen
cmopn 14927	class MetOpen
cmetu 14928	class metUnif
df-psmet 14929	|- 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 14930	|- *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 14931	|- 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 14932	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14933	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14934	|- 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 14935	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14936	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14942	class ℂfld
df-cnfld 14943	|- ℂ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 14974	class ℤring
df-zring 14975	|- ℤring = (ℂfld ↾s ZZ )
czrh 14995	class ZRHom
czlm 14996	class ZMod
czn 14997	class ℤ/nℤ
df-zrh 14998	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14999	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 15000	|- ℤ/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 15045	class AssAlg
casp 15046	class AlgSpan
cascl 15047	class algSc
df-assa 15048	|- 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 15049	|- AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )
df-ascl 15050	|- algSc = ( w e. _V |-> ( x e. ( Base ` (Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) )
cmps 15094	class mPwSer
cmpl 15095	class mPoly
df-psr 15096	|- 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 15097	|- 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 15147	class Top
df-top 15148	|- 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 15160	class TopOn
df-topon 15161	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 15180	class TopSp
df-topsp 15181	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 15192	class TopBases
df-bases 15193	|- 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 15242	class Clsd
cnt 15243	class int
ccl 15244	class cls
df-cld 15245	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 15246	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 15247	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 15288	class nei
df-nei 15289	|- 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 15335	class Cn
ccnp 15336	class CnP
clm 15337	class ~~> t
df-cn 15338	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 15339	|- 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 15340	|- ~~> 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 15402	class tX
df-tx 15403	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15450	class Homeo
df-hmeo 15451	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15486	class *MetSp
cms 15487	class MetSp
ctms 15488	class toMetSp
df-xms 15489	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15490	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15491	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15720	class -cn->
df-cncf 15721	|- -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 15804	class lim CC
cdv 15805	class _D
df-limced 15806	|- 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 15807	|- _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 15878	class Poly
cidp 15879	class Xp
df-ply 15880	|- 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 15881	|- Xp = ( _I |` CC )
clog 16007	class log
ccxp 16008	class ^c
df-relog 16009	|- log = `' ( exp |` RR )
df-rpcxp 16010	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 16098	class logb
df-logb 16099	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
cppi 16152	class π
csgm 16153	class sigma
df-ppi 16154	|- π = ( x e. RR |-> (♯ ` ( ( 0 [,] x ) i^i Prime ) ) )
df-sgm 16155	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 16214	class /L
df-lgs 16215	|- /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 16343	class .ef
df-edgf 16344	|- .ef = Slot ; 1 8
cvtx 16351	class Vtx
ciedg 16352	class iEdg
df-vtx 16353	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 16354	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 16396	class Edg
df-edg 16397	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 16406	class UHGraph
cushgr 16407	class USHGraph
df-uhgrm 16408	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 16409	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 16430	class UPGraph
cumgr 16431	class UMGraph
df-upgren 16432	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 16433	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16492	class USPGraph
cusgr 16493	class USGraph
df-uspgren 16494	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16495	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16592	class SubGraph
df-subgr 16593	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16625	class VtxDeg
df-vtxdg 16626	|- 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 16656	class Walks
df-wlks 16657	|- 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 16719	class Trails
df-trls 16720	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16730	class ClWWalks
df-clwwlk 16731	|- 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 16742	class ClWWalksN
df-clwwlkn 16743	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16765	class ClWWalksNOn
df-clwwlknon 16766	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16781	class EulerPaths
df-eupth 16782	|- 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 16919	wff A DECIDin B
df-dcin 16920	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16936	wff BOUNDED ph
ax-bd0 16937	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16938	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16939	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16940	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16941	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16942	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16943	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16944	|- BOUNDED x = y
ax-bdel 16945	|- BOUNDED x e. y
ax-bdsb 16946	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16964	wff BOUNDED A
df-bdc 16965	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 17008	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 17048	|- BOUNDED ph   =>    |- DECID ph
wind 17050	wff Ind A
df-bj-ind 17051	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 17065	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 17092	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 17100	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 17106	|- 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 17111	|- 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 17113	|- ( ( ( 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 17138	wff WEXMID
df-wexmid 17139	|- (WEXMID <-> A. p e. ~P 1o ( -. p = 1o \/ -. -. p = 1o ) )
wals 17224	wff A.E. x ( ph -> ps )
wrals 17225	wff A.E. x e. A ( ph -> ps )
df-als 17226	|- ( A.E. x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-rals 17227	|- ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
walseu 17258	wff A.E! x ( ph -> ps )
wralseu 17259	wff A.E! x e. A ( ph -> ps )
df-alseu 17260	|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
df-ralseu 17261	|- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )