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 4131	wff A R B
df-br 4132	|- ( A R B <-> <. A , B >. e. R )
copab 4192	class { <. x , y >. | ph }
cmpt 4193	class ( x e. A |-> B )
df-opab 4194	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4195	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4231	wff Tr A
df-tr 4232	|- ( Tr A <-> U. A C_ A )
ax-coll 4248	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4251	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4261	|- E. x A. y -. y e. x
ax-pow 4313	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4333	wff EXMID
df-exmid 4334	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4348	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4434	class _E
cid 4435	class _I
df-eprel 4436	|- _E = { <. x , y >. | x e. y }
df-id 4440	|- _I = { <. x , y >. | x = y }
wpo 4441	wff R Po A
wor 4442	wff R Or A
df-po 4443	|- ( 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 4444	|- ( 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 4474	wff FrFor R A S
wfr 4475	wff R Fr A
wse 4476	wff R Se A
wwe 4477	wff R We A
df-frfor 4478	|- (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 4479	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4480	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4481	|- ( 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 4509	wff Ord A
con0 4510	class On
wlim 4511	wff Lim A
csuc 4512	class suc A
df-iord 4513	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4515	|- On = { x | Ord x }
df-ilim 4516	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4518	|- suc A = ( A u. { A } )
ax-un 4580	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4686	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4737	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4739	class om
df-iom 4740	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4774	class ( A X. B )
ccnv 4775	class `' A
cdm 4776	class dom A
crn 4777	class ran A
cres 4778	class ( A |` B )
cima 4779	class ( A " B )
ccom 4780	class ( A o. B )
wrel 4781	wff Rel A
df-xp 4782	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4783	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4784	|- `' A = { <. x , y >. | y A x }
df-co 4785	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4786	|- dom A = { x | E. y x A y }
df-rn 4787	|- ran A = dom `' A
df-res 4788	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4789	|- ( A " B ) = ran ( A |` B )
cio 5338	class ( iota x ph )
df-iota 5340	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5374	wff Fun A
wfn 5375	wff A Fn B
wf 5376	wff F : A --> B
wf1 5377	wff F : A -1-1-> B
wfo 5378	wff F : A -onto-> B
wf1o 5379	wff F : A -1-1-onto-> B
cfv 5380	class ( F ` A )
wiso 5381	wff H Isom R , S ( A , B )
df-fun 5382	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5383	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5384	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5385	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5386	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5387	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5388	|- ( F ` A ) = ( iota x A F x )
df-isom 5389	|- ( 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 6040	class ( iota_ x e. A ph )
df-riota 6041	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6088	class ( A F B )
coprab 6089	class { <. <. x , y >. , z >. | ph }
cmpo 6090	class ( x e. A , y e. B |-> C )
df-ov 6091	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6092	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6093	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6303	class oF R
cofr 6304	class oR R
df-of 6305	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6306	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6376	class 1st
c2nd 6377	class 2nd
df-1st 6378	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6379	|- 2nd = ( x e. _V |-> U. ran { x } )
csupp 6479	class supp
df-supp 6480	|- supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
ctpos 6519	class tpos F
df-tpos 6520	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6560	wff Smo A
df-smo 6561	|- ( 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 6579	class recs ( F )
df-recs 6580	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6644	class rec ( F , I )
df-irdg 6645	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6665	class frec ( F , I )
df-frec 6666	|- 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 6684	class 1o
c2o 6685	class 2o
c3o 6686	class 3o
c4o 6687	class 4o
coa 6688	class +o
comu 6689	class .o
coei 6690	class ↑o
df-1o 6691	|- 1o = suc (/)
df-2o 6692	|- 2o = suc 1o
df-3o 6693	|- 3o = suc 2o
df-4o 6694	|- 4o = suc 3o
df-oadd 6695	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6696	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6697	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6808	wff R Er A
cec 6809	class [ A ] R
cqs 6810	class ( A /. R )
df-er 6811	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6813	|- [ A ] R = ( R " { A } )
df-qs 6817	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6926	class ^m
cpm 6927	class ^pm
df-map 6928	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6929	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6984	class X_ x e. A B
df-ixp 6985	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 7024	class ~~
cdom 7025	class ~<_
cfn 7026	class Fin
df-en 7027	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 7028	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 7029	|- Fin = { x | E. y e. om x ~~ y }
cfsupp 7290	class finSupp
df-fsupp 7291	|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
cfi 7307	class fi
df-fi 7308	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7328	class sup ( A , B , R )
cinf 7329	class inf ( A , B , R )
df-sup 7330	|- 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 7331	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7383	class ( A ⊔ B )
df-dju 7384	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7391	class inl
cinr 7392	class inr
df-inl 7393	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7394	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7429	class case ( R , S )
df-case 7430	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7448	class ( R ⊔d S )
df-djud 7449	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7465	class ℕ∞
df-nninf 7466	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7480	class Omni
df-omni 7481	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7497	class Markov
df-markov 7498	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7509	class WOmni
df-womni 7510	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7528	class card
wacn 7529	class AC A
df-card 7530	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7531	|- 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 7567	wff CHOICE
df-ac 7568	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7613	wff R Ap A
df-pap 7614	|- ( 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 7620	wff R TAp A
df-tap 7621	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7634	wff CCHOICE
df-cc 7635	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7645	class N.
cpli 7646	class +N
cmi 7647	class .N
clti 7648	class <N
cplpq 7649	class +pQ
cmpq 7650	class .pQ
cltpq 7651	class <pQ
ceq 7652	class ~Q
cnq 7653	class Q.
c1q 7654	class 1Q
cplq 7655	class +Q
cmq 7656	class .Q
crq 7657	class *Q
cltq 7658	class <Q
ceq0 7659	class ~Q0
cnq0 7660	class Q0
c0q0 7661	class 0Q0
cplq0 7662	class +Q0
cmq0 7663	class ·Q0
cnp 7664	class P.
c1p 7665	class 1P
cpp 7666	class +P.
cmp 7667	class .P.
cltp 7668	class <P
cer 7669	class ~R
cnr 7670	class R.
c0r 7671	class 0R
c1r 7672	class 1R
cm1r 7673	class -1R
cplr 7674	class +R
cmr 7675	class .R
cltr 7676	class <R
df-ni 7677	|- N. = ( om \ { (/) } )
df-pli 7678	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7679	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7680	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7717	|- +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 7718	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7719	|- <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 7720	|- ~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 7721	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7722	|- +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 7723	|- .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 7724	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7725	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7726	|- <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 7797	|- ~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 7798	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7799	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7800	|- +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 7801	|- ·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 7839	|- 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 7840	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7841	|- +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 7842	|- .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 7843	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 8099	|- ~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 8100	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 8101	|- +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 8102	|- .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 8103	|- <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 8104	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 8105	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 8106	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8183	class CC
cr 8184	class RR
cc0 8185	class 0
c1 8186	class 1
ci 8187	class _i
caddc 8188	class +
cltrr 8189	class <RR
cmul 8190	class x.
df-c 8191	|- CC = ( R. X. R. )
df-0 8192	|- 0 = <. 0R , 0R >.
df-1 8193	|- 1 = <. 1R , 0R >.
df-i 8194	|- _i = <. 0R , 1R >.
df-r 8195	|- RR = ( R. X. { 0R } )
df-add 8196	|- + = { <. <. 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 8197	|- 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 8198	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8276	|- CC e. _V
ax-resscn 8277	|- RR C_ CC
ax-1cn 8278	|- 1 e. CC
ax-1re 8279	|- 1 e. RR
ax-icn 8280	|- _i e. CC
ax-addcl 8281	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8282	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8283	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8284	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8285	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8286	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8287	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8288	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8289	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8290	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8291	|- 0 <RR 1
ax-1rid 8292	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8293	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8294	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8295	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8296	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8297	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8298	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8299	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8300	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8301	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8302	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8303	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8304	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8305	|- 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 8306	|- ( ( ( 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 8307	|- + : ( CC X. CC ) --> CC
ax-mulf 8308	|- x. : ( CC X. CC ) --> CC
cpnf 8363	class +oo
cmnf 8364	class -oo
cxr 8365	class RR*
clt 8366	class <
cle 8367	class <_
df-pnf 8368	|- +oo = ~P U. CC
df-mnf 8369	|- -oo = ~P +oo
df-xr 8370	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8371	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8372	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8504	class -
cneg 8505	class -u A
df-sub 8506	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8507	|- -u A = ( 0 - A )
creap 8910	class #ℝ
df-reap 8911	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8917	class #
df-ap 8918	|- # = { <. 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 9010	class /
df-div 9011	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cind 9302	class 𝟭
df-ind 9303	|- 𝟭 = ( o e. _V |-> ( a e. ~P o |-> ( x e. o |-> if ( x e. a , 1 , 0 ) ) ) )
cn 9313	class NN
df-inn 9314	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9364	class 2
c3 9365	class 3
c4 9366	class 4
c5 9367	class 5
c6 9368	class 6
c7 9369	class 7
c8 9370	class 8
c9 9371	class 9
df-2 9372	|- 2 = ( 1 + 1 )
df-3 9373	|- 3 = ( 2 + 1 )
df-4 9374	|- 4 = ( 3 + 1 )
df-5 9375	|- 5 = ( 4 + 1 )
df-6 9376	|- 6 = ( 5 + 1 )
df-7 9377	|- 7 = ( 6 + 1 )
df-8 9378	|- 8 = ( 7 + 1 )
df-9 9379	|- 9 = ( 8 + 1 )
cn0 9574	class NN0
df-n0 9575	|- NN0 = ( NN u. { 0 } )
cxnn0 9641	class NN0*
df-xnn0 9642	|- NN0* = ( NN0 u. { +oo } )
cz 9655	class ZZ
df-z 9656	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9788	class ; A B
df-dec 9789	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9937	class ZZ>=
df-uz 9938	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 10035	class QQ
df-q 10036	|- QQ = ( / " ( ZZ X. NN ) )
crp 10071	class RR+
df-rp 10072	|- RR+ = { x e. RR | 0 < x }
cxne 10188	class -e A
cxad 10189	class +e
cxmu 10190	class xe
df-xneg 10191	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10192	|- +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 10193	|- 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 10307	class (,)
cioc 10308	class (,]
cico 10309	class [,)
cicc 10310	class [,]
df-ioo 10311	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10312	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10313	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10314	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10428	class ...
df-fz 10429	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10566	class ..^
df-fzo 10567	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10720	class |_
cceil 10721	class ⌈
df-fl 10722	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10723	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10780	class mod
df-mod 10781	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10905	class seq M ( .+ , F )
df-seqfrec 10906	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10996	class ^
df-exp 10997	|- ^ = ( 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 11185	class !
df-fac 11186	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11207	class _C
df-bc 11208	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11236	class ♯
df-ihash 11237	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11326	class Word S
df-word 11327	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11371	class lastS
df-lsw 11372	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11380	class ++
df-concat 11381	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11405	class <" A ">
df-s1 11406	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11439	class substr
df-substr 11440	|- 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 11466	class prefix
df-pfx 11467	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11543	class <" A B ">
cs3 11544	class <" A B C ">
cs4 11545	class <" A B C D ">
cs5 11546	class <" A B C D E ">
cs6 11547	class <" A B C D E F ">
cs7 11548	class <" A B C D E F G ">
cs8 11549	class <" A B C D E F G H ">
df-s2 11550	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11551	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11552	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11553	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11554	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11555	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11556	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11601	class shift
df-shft 11602	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11626	class *
cre 11627	class Re
cim 11628	class Im
df-cj 11629	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11630	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11631	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11784	class sqr
cabs 11785	class abs
df-rsqrt 11786	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11787	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 12069	class ~~>
df-clim 12070	|- ~~> = { <. 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 12144	class sum_ k e. A B
df-sumdc 12145	|- 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 12342	class prod_ k e. A B
df-proddc 12343	|- 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 12434	class exp
ceu 12435	class _e
csin 12436	class sin
ccos 12437	class cos
ctan 12438	class tan
cpi 12439	class pi
df-ef 12440	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12441	|- _e = ( exp ` 1 )
df-sin 12442	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12443	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12444	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12445	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12567	class tau
df-tau 12568	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12579	class ||
df-dvds 12580	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12732	class bits
df-bits 12733	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12755	class gcd
df-gcd 12756	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12863	class lcm
df-lcm 12864	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12910	class Prime
df-prm 12911	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12986	class numer
cdenom 12987	class denom
df-numer 12988	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12989	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 13015	class odZ
cphi 13016	class phi
df-odz 13017	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 13018	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 13092	class pCnt
df-pc 13093	|- 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 13177	class ZZ[_i]
df-gz 13178	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13406	class Struct
cnx 13407	class ndx
csts 13408	class sSet
cslot 13409	class Slot A
cbs 13410	class Base
cress 13411	class ↾s
df-struct 13412	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13413	|- ndx = ( _I |` NN )
df-slot 13414	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13416	|- Base = Slot 1
df-sets 13417	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13418	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13490	class +g
cmulr 13491	class .r
cstv 13492	class *r
csca 13493	class Scalar
cvsca 13494	class .s
cip 13495	class .i
cts 13496	class TopSet
cple 13497	class le
coc 13498	class oc
cds 13499	class dist
cunif 13500	class UnifSet
chom 13501	class Hom
cco 13502	class comp
df-plusg 13503	|- +g = Slot 2
df-mulr 13504	|- .r = Slot 3
df-starv 13505	|- *r = Slot 4
df-sca 13506	|- Scalar = Slot 5
df-vsca 13507	|- .s = Slot 6
df-ip 13508	|- .i = Slot 8
df-tset 13509	|- TopSet = Slot 9
df-ple 13510	|- le = Slot ; 1 0
df-ocomp 13511	|- oc = Slot ; 1 1
df-ds 13512	|- dist = Slot ; 1 2
df-unif 13513	|- UnifSet = Slot ; 1 3
df-hom 13514	|- Hom = Slot ; 1 4
df-cco 13515	|- comp = Slot ; 1 5
crest 13652	class ↾t
ctopn 13653	class TopOpen
df-rest 13654	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13655	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13667	class topGen
cpt 13668	class Xt_
c0g 13669	class 0g
cgzsu 13670	class gzsumgz
df-0g 13671	|- 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 13672	|- 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 13673	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13674	|- 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 13681	class "s
cqus 13682	class /.s
df-iimas 13683	|- "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 13684	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
cplusf 13732	class +f
cmgm 13733	class Mgm
df-plusf 13734	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13735	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13775	class Smgrp
df-sgrp 13776	|- 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 13788	class Mnd
df-mnd 13789	|- 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 13823	class MndHom
csubmnd 13824	class SubMnd
df-mhm 13825	|- 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 13826	|- 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 13864	class Grp
cminusg 13865	class invg
csg 13866	class -g
df-grp 13867	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13868	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13869	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13981	class .g
df-mulg 13982	|- .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 14029	class SubGrp
cnsg 14030	class NrmSGrp
cqg 14031	class ~QG
df-subg 14032	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 14033	|- 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 14034	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 14102	class GrpHom
df-ghm 14103	|- GrpHom = ( s e. Grp , t e. Grp |-> { g | [. ( Base ` s ) / w ]. ( g : w --> ( Base ` t ) /\ A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) ) ) } )
ccntz 14146	class Cntz
ccntr 14147	class Cntr
df-cntz 14148	|- Cntz = ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) )
df-cntr 14149	|- Cntr = ( m e. _V |-> ( (Cntz ` m ) ` ( Base ` m ) ) )
ccmn 14177	class CMnd
cabl 14178	class Abel
df-cmn 14179	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 14180	|- Abel = ( Grp i^i CMnd )
cgsu 14240	class gsumg
df-gsumfi 14241	|- 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 14276	class X_s
df-prds 14277	|- 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 14306	class X.s
df-xps 14307	|- 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 14309	class ^s
df-pws 14310	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cmgp 14324	class mulGrp
df-mgp 14325	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 14338	class Rng
df-rng 14339	|- 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 14369	class 1r
df-ur 14370	|- 1r = ( 0g o. mulGrp )
csrg 14374	class SRing
df-srg 14375	|- 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 14407	class Ring
ccrg 14408	class CRing
df-ring 14409	|- 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 14410	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14481	class oppr
df-oppr 14482	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14501	class ||r
cui 14502	class Unit
cir 14503	class Irred
df-dvdsr 14504	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14505	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14506	|- 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 14536	class invr
df-invr 14537	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14547	class /r
df-dvr 14548	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14566	class RingHom
crs 14567	class RingIso
df-rhm 14568	|- 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 14569	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14595	class NzRing
df-nzr 14596	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14606	class LRing
df-lring 14607	|- 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 14614	class SubRng
df-subrng 14615	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14634	class SubRing
crgspn 14635	class RingSpan
df-subrg 14636	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14637	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14672	class RLReg
cdomn 14673	class Domn
cidom 14674	class IDomn
df-rlreg 14675	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14676	|- 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 14677	|- IDomn = ( CRing i^i Domn )
capr 14698	class #r
df-apr 14699	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
cdr 14711	class DivRing
cfield 14712	class Field
df-drngap 14713	|- DivRing = { r e. Ring | ( #r ` r ) TAp ( Base ` r ) }
df-field 14714	|- Field = ( DivRing i^i CRing )
clmod 14732	class LMod
cscaf 14733	class .sf
df-lmod 14734	|- 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 14735	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14798	class LSubSp
df-lssm 14799	|- 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 14832	class LSpan
df-lsp 14833	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14879	class subringAlg
crglmod 14880	class ringLMod
df-sra 14881	|- 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 14882	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14913	class LIdeal
crsp 14914	class RSpan
df-lidl 14915	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14916	|- RSpan = ( LSpan o. ringLMod )
c2idl 14945	class 2Ideal
df-2idl 14946	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14981	class PsMet
cxmet 14982	class *Met
cmet 14983	class Met
cbl 14984	class ball
cfbas 14985	class fBas
cfg 14986	class filGen
cmopn 14987	class MetOpen
cmetu 14988	class metUnif
df-psmet 14989	|- 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 14990	|- *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 14991	|- 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 14992	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14993	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14994	|- 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 14995	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14996	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 15002	class ℂfld
df-cnfld 15003	|- ℂ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 15034	class ℤring
df-zring 15035	|- ℤring = (ℂfld ↾s ZZ )
czrh 15055	class ZRHom
czlm 15056	class ZMod
czn 15057	class ℤ/nℤ
df-zrh 15058	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 15059	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 15060	|- ℤ/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 15105	class AssAlg
casp 15106	class AlgSpan
cascl 15107	class algSc
df-assa 15108	|- 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 15109	|- AlgSpan = ( w e. AssAlg |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( (SubRing ` w ) i^i ( LSubSp ` w ) ) | s C_ t } ) )
df-ascl 15110	|- algSc = ( w e. _V |-> ( x e. ( Base ` (Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) )
cmps 15154	class mPwSer
cmpl 15155	class mPoly
df-psr 15156	|- 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 15157	|- 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 15223	class Top
df-top 15224	|- 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 15236	class TopOn
df-topon 15237	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 15256	class TopSp
df-topsp 15257	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 15268	class TopBases
df-bases 15269	|- 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 15318	class Clsd
cnt 15319	class int
ccl 15320	class cls
df-cld 15321	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 15322	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 15323	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 15364	class nei
df-nei 15365	|- 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 15411	class Cn
ccnp 15412	class CnP
clm 15413	class ~~> t
df-cn 15414	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 15415	|- 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 15416	|- ~~> 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 15478	class tX
df-tx 15479	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15526	class Homeo
df-hmeo 15527	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15562	class *MetSp
cms 15563	class MetSp
ctms 15564	class toMetSp
df-xms 15565	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15566	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15567	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15796	class -cn->
df-cncf 15797	|- -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 15880	class lim CC
cdv 15881	class _D
df-limced 15882	|- 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 15883	|- _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 15954	class Poly
cidp 15955	class Xp
df-ply 15956	|- 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 15957	|- Xp = ( _I |` CC )
clog 16085	class log
ccxp 16086	class ^c
df-relog 16087	|- log = `' ( exp |` RR )
df-rpcxp 16088	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 16179	class logb
df-logb 16180	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
ccht 16233	class theta
cppi 16234	class π
csgm 16235	class sigma
df-cht 16236	|- theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )
df-ppi 16237	|- π = ( x e. RR |-> (♯ ` ( ( 0 [,] x ) i^i Prime ) ) )
df-sgm 16238	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 16321	class /L
df-lgs 16322	|- /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 16450	class .ef
df-edgf 16451	|- .ef = Slot ; 1 8
cvtx 16458	class Vtx
ciedg 16459	class iEdg
df-vtx 16460	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 16461	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 16503	class Edg
df-edg 16504	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 16513	class UHGraph
cushgr 16514	class USHGraph
df-uhgrm 16515	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 16516	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 16537	class UPGraph
cumgr 16538	class UMGraph
df-upgren 16539	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 16540	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16599	class USPGraph
cusgr 16600	class USGraph
df-uspgren 16601	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16602	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16699	class SubGraph
df-subgr 16700	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16732	class VtxDeg
df-vtxdg 16733	|- 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 16763	class Walks
df-wlks 16764	|- 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 16826	class Trails
df-trls 16827	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16837	class ClWWalks
df-clwwlk 16838	|- 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 16849	class ClWWalksN
df-clwwlkn 16850	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16872	class ClWWalksNOn
df-clwwlknon 16873	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16888	class EulerPaths
df-eupth 16889	|- 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 17026	wff A DECIDin B
df-dcin 17027	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 17043	wff BOUNDED ph
ax-bd0 17044	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 17045	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 17046	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 17047	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 17048	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 17049	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 17050	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 17051	|- BOUNDED x = y
ax-bdel 17052	|- BOUNDED x e. y
ax-bdsb 17053	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 17071	wff BOUNDED A
df-bdc 17072	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 17115	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 17155	|- BOUNDED ph   =>    |- DECID ph
wind 17157	wff Ind A
df-bj-ind 17158	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 17172	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 17199	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 17207	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 17213	|- 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 17218	|- 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 17220	|- ( ( ( 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 17245	wff WEXMID
df-wexmid 17246	|- (WEXMID <-> A. p e. ~P 1o ( -. p = 1o \/ -. -. p = 1o ) )
wals 17333	wff A.E. x ( ph -> ps )
wrals 17334	wff A.E. x e. A ( ph -> ps )
df-als 17335	|- ( A.E. x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-rals 17336	|- ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
walseu 17367	wff A.E! x ( ph -> ps )
wralseu 17368	wff A.E! x e. A ( ph -> ps )
df-alseu 17369	|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
df-ralseu 17370	|- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )