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 8497	class -
cneg 8498	class -u A
df-sub 8499	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8500	|- -u A = ( 0 - A )
creap 8902	class #ℝ
df-reap 8903	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8909	class #
df-ap 8910	|- # = { <. 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 9002	class /
df-div 9003	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cind 9293	class 𝟭
df-ind 9294	|- 𝟭 = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )
cn 9304	class NN
df-inn 9305	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9355	class 2
c3 9356	class 3
c4 9357	class 4
c5 9358	class 5
c6 9359	class 6
c7 9360	class 7
c8 9361	class 8
c9 9362	class 9
df-2 9363	|- 2 = ( 1 + 1 )
df-3 9364	|- 3 = ( 2 + 1 )
df-4 9365	|- 4 = ( 3 + 1 )
df-5 9366	|- 5 = ( 4 + 1 )
df-6 9367	|- 6 = ( 5 + 1 )
df-7 9368	|- 7 = ( 6 + 1 )
df-8 9369	|- 8 = ( 7 + 1 )
df-9 9370	|- 9 = ( 8 + 1 )
cn0 9563	class NN0
df-n0 9564	|- NN0 = ( NN u. { 0 } )
cxnn0 9630	class NN0*
df-xnn0 9631	|- NN0* = ( NN0 u. { +oo } )
cz 9644	class ZZ
df-z 9645	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9777	class ; A B
df-dec 9778	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9921	class ZZ>=
df-uz 9922	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 10019	class QQ
df-q 10020	|- QQ = ( / " ( ZZ X. NN ) )
crp 10054	class RR+
df-rp 10055	|- RR+ = { x e. RR | 0 < x }
cxne 10171	class -e A
cxad 10172	class +e
cxmu 10173	class xe
df-xneg 10174	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10175	|- +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 10176	|- 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 10290	class (,)
cioc 10291	class (,]
cico 10292	class [,)
cicc 10293	class [,]
df-ioo 10294	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10295	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10296	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10297	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10411	class ...
df-fz 10412	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10549	class ..^
df-fzo 10550	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10703	class |_
cceil 10704	class ⌈
df-fl 10705	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10706	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10759	class mod
df-mod 10760	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10884	class seq M ( .+ , F )
df-seqfrec 10885	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10975	class ^
df-exp 10976	|- ^ = ( 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 11163	class !
df-fac 11164	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11185	class _C
df-bc 11186	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11214	class ♯
df-ihash 11215	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11304	class Word S
df-word 11305	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11349	class lastS
df-lsw 11350	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11358	class ++
df-concat 11359	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11383	class <" A ">
df-s1 11384	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11417	class substr
df-substr 11418	|- 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 11444	class prefix
df-pfx 11445	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11521	class <" A B ">
cs3 11522	class <" A B C ">
cs4 11523	class <" A B C D ">
cs5 11524	class <" A B C D E ">
cs6 11525	class <" A B C D E F ">
cs7 11526	class <" A B C D E F G ">
cs8 11527	class <" A B C D E F G H ">
df-s2 11528	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11529	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11530	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11531	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11532	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11533	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11534	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11579	class shift
df-shft 11580	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11604	class *
cre 11605	class Re
cim 11606	class Im
df-cj 11607	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11608	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11609	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11762	class sqr
cabs 11763	class abs
df-rsqrt 11764	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11765	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 12044	class ~~>
df-clim 12045	|- ~~> = { <. 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 12119	class sum_ k e. A B
df-sumdc 12120	|- 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 12317	class prod_ k e. A B
df-proddc 12318	|- 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 12409	class exp
ceu 12410	class _e
csin 12411	class sin
ccos 12412	class cos
ctan 12413	class tan
cpi 12414	class pi
df-ef 12415	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12416	|- _e = ( exp ` 1 )
df-sin 12417	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12418	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12419	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12420	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12542	class tau
df-tau 12543	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12554	class ||
df-dvds 12555	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12707	class bits
df-bits 12708	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12730	class gcd
df-gcd 12731	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12838	class lcm
df-lcm 12839	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12885	class Prime
df-prm 12886	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12959	class numer
cdenom 12960	class denom
df-numer 12961	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12962	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12986	class odZ
cphi 12987	class phi
df-odz 12988	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12989	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 13063	class pCnt
df-pc 13064	|- 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 13148	class ZZ[_i]
df-gz 13149	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13348	class Struct
cnx 13349	class ndx
csts 13350	class sSet
cslot 13351	class Slot A
cbs 13352	class Base
cress 13353	class ↾s
df-struct 13354	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13355	|- ndx = ( _I |` NN )
df-slot 13356	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13358	|- Base = Slot 1
df-sets 13359	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13360	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13431	class +g
cmulr 13432	class .r
cstv 13433	class *r
csca 13434	class Scalar
cvsca 13435	class .s
cip 13436	class .i
cts 13437	class TopSet
cple 13438	class le
coc 13439	class oc
cds 13440	class dist
cunif 13441	class UnifSet
chom 13442	class Hom
cco 13443	class comp
df-plusg 13444	|- +g = Slot 2
df-mulr 13445	|- .r = Slot 3
df-starv 13446	|- *r = Slot 4
df-sca 13447	|- Scalar = Slot 5
df-vsca 13448	|- .s = Slot 6
df-ip 13449	|- .i = Slot 8
df-tset 13450	|- TopSet = Slot 9
df-ple 13451	|- le = Slot ; 1 0
df-ocomp 13452	|- oc = Slot ; 1 1
df-ds 13453	|- dist = Slot ; 1 2
df-unif 13454	|- UnifSet = Slot ; 1 3
df-hom 13455	|- Hom = Slot ; 1 4
df-cco 13456	|- comp = Slot ; 1 5
crest 13593	class ↾t
ctopn 13594	class TopOpen
df-rest 13595	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13596	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13608	class topGen
cpt 13609	class Xt_
c0g 13610	class 0g
cgzsu 13611	class gzsumgz
df-0g 13612	|- 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 13613	|- 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 13614	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13615	|- 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 13622	class "s
cqus 13623	class /.s
df-iimas 13624	|- "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 13625	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
cplusf 13673	class +f
cmgm 13674	class Mgm
df-plusf 13675	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13676	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13716	class Smgrp
df-sgrp 13717	|- 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 13729	class Mnd
df-mnd 13730	|- 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 13764	class MndHom
csubmnd 13765	class SubMnd
df-mhm 13766	|- 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 13767	|- 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 13805	class Grp
cminusg 13806	class invg
csg 13807	class -g
df-grp 13808	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13809	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13810	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13922	class .g
df-mulg 13923	|- .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 13970	class SubGrp
cnsg 13971	class NrmSGrp
cqg 13972	class ~QG
df-subg 13973	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13974	|- 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 13975	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 14043	class GrpHom
df-ghm 14044	|- 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 14087	class CMnd
cabl 14088	class Abel
df-cmn 14089	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 14090	|- Abel = ( Grp i^i CMnd )
cgsu 14150	class gsumg
df-gsumfi 14151	|- 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 14169	class X_s
df-prds 14170	|- 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 14199	class X.s
df-xps 14200	|- 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 14202	class ^s
df-pws 14203	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cmgp 14217	class mulGrp
df-mgp 14218	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 14231	class Rng
df-rng 14232	|- 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 14262	class 1r
df-ur 14263	|- 1r = ( 0g o. mulGrp )
csrg 14267	class SRing
df-srg 14268	|- 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 14300	class Ring
ccrg 14301	class CRing
df-ring 14302	|- 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 14303	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14372	class oppr
df-oppr 14373	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14392	class ||r
cui 14393	class Unit
cir 14394	class Irred
df-dvdsr 14395	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14396	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14397	|- 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 14427	class invr
df-invr 14428	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14438	class /r
df-dvr 14439	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14457	class RingHom
crs 14458	class RingIso
df-rhm 14459	|- 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 14460	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14486	class NzRing
df-nzr 14487	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14497	class LRing
df-lring 14498	|- 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 14505	class SubRng
df-subrng 14506	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14525	class SubRing
crgspn 14526	class RingSpan
df-subrg 14527	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14528	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14563	class RLReg
cdomn 14564	class Domn
cidom 14565	class IDomn
df-rlreg 14566	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14567	|- 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 14568	|- IDomn = ( CRing i^i Domn )
capr 14589	class #r
df-apr 14590	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
cdr 14602	class DivRing
cfield 14603	class Field
df-drngap 14604	|- DivRing = { r e. Ring | (#r ` r ) TAp ( Base ` r ) }
df-field 14605	|- Field = ( DivRing i^i CRing )
clmod 14623	class LMod
cscaf 14624	class .sf
df-lmod 14625	|- 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 14626	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14689	class LSubSp
df-lssm 14690	|- 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 14723	class LSpan
df-lsp 14724	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14770	class subringAlg
crglmod 14771	class ringLMod
df-sra 14772	|- 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 14773	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14804	class LIdeal
crsp 14805	class RSpan
df-lidl 14806	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14807	|- RSpan = ( LSpan o. ringLMod )
c2idl 14836	class 2Ideal
df-2idl 14837	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14872	class PsMet
cxmet 14873	class *Met
cmet 14874	class Met
cbl 14875	class ball
cfbas 14876	class fBas
cfg 14877	class filGen
cmopn 14878	class MetOpen
cmetu 14879	class metUnif
df-psmet 14880	|- 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 14881	|- *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 14882	|- 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 14883	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14884	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14885	|- 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 14886	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14887	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14893	class ℂfld
df-cnfld 14894	|- ℂ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 14925	class ℤring
df-zring 14926	|- ℤring = (ℂfld ↾s ZZ )
czrh 14946	class ZRHom
czlm 14947	class ZMod
czn 14948	class ℤ/nℤ
df-zrh 14949	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14950	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14951	|- ℤ/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 14996	class AssAlg
casp 14997	class AlgSpan
cascl 14998	class algSc
df-assa 14999	|- 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 15000	|- AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )
df-ascl 15001	|- algSc = ( w e. _V |-> ( x e. ( Base ` (Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) )
cmps 15045	class mPwSer
cmpl 15046	class mPoly
df-psr 15047	|- 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 15048	|- 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 15098	class Top
df-top 15099	|- 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 15111	class TopOn
df-topon 15112	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 15131	class TopSp
df-topsp 15132	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 15143	class TopBases
df-bases 15144	|- 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 15193	class Clsd
cnt 15194	class int
ccl 15195	class cls
df-cld 15196	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 15197	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 15198	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 15239	class nei
df-nei 15240	|- 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 15286	class Cn
ccnp 15287	class CnP
clm 15288	class ~~> t
df-cn 15289	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 15290	|- 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 15291	|- ~~> 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 15353	class tX
df-tx 15354	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15401	class Homeo
df-hmeo 15402	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15437	class *MetSp
cms 15438	class MetSp
ctms 15439	class toMetSp
df-xms 15440	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15441	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15442	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15671	class -cn->
df-cncf 15672	|- -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 15755	class lim CC
cdv 15756	class _D
df-limced 15757	|- 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 15758	|- _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 15829	class Poly
cidp 15830	class Xp
df-ply 15831	|- 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 15832	|- Xp = ( _I |` CC )
clog 15957	class log
ccxp 15958	class ^c
df-relog 15959	|- log = `' ( exp |` RR )
df-rpcxp 15960	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 16045	class logb
df-logb 16046	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 16095	class sigma
df-sgm 16096	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 16116	class /L
df-lgs 16117	|- /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 16245	class .ef
df-edgf 16246	|- .ef = Slot ; 1 8
cvtx 16253	class Vtx
ciedg 16254	class iEdg
df-vtx 16255	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 16256	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 16298	class Edg
df-edg 16299	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 16308	class UHGraph
cushgr 16309	class USHGraph
df-uhgrm 16310	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 16311	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 16332	class UPGraph
cumgr 16333	class UMGraph
df-upgren 16334	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 16335	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16394	class USPGraph
cusgr 16395	class USGraph
df-uspgren 16396	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16397	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16494	class SubGraph
df-subgr 16495	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16527	class VtxDeg
df-vtxdg 16528	|- 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 16558	class Walks
df-wlks 16559	|- 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 16621	class Trails
df-trls 16622	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16632	class ClWWalks
df-clwwlk 16633	|- 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 16644	class ClWWalksN
df-clwwlkn 16645	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16667	class ClWWalksNOn
df-clwwlknon 16668	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16683	class EulerPaths
df-eupth 16684	|- 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 16821	wff A DECIDin B
df-dcin 16822	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16838	wff BOUNDED ph
ax-bd0 16839	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16840	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16841	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16842	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16843	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16844	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16845	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16846	|- BOUNDED x = y
ax-bdel 16847	|- BOUNDED x e. y
ax-bdsb 16848	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16866	wff BOUNDED A
df-bdc 16867	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16910	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16950	|- BOUNDED ph   =>    |- DECID ph
wind 16952	wff Ind A
df-bj-ind 16953	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16967	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16994	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 17002	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 17008	|- 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 17013	|- 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 17015	|- ( ( ( 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 17040	wff WEXMID
df-wexmid 17041	|- (WEXMID <-> A. p e. ~P 1o ( -. p = 1o \/ -. -. p = 1o ) )
wals 17126	wff A.E. x ( ph -> ps )
wrals 17127	wff A.E. x e. A ( ph -> ps )
df-als 17128	|- ( A.E. x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-rals 17129	|- ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
walseu 17160	wff A.E! x ( ph -> ps )
wralseu 17161	wff A.E! x e. A ( ph -> ps )
df-alseu 17162	|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
df-ralseu 17163	|- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )