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 619	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 620	|- ( -. ph -> ( ph -> ps ) )
wo 716	wff ( ph \/ ps )
ax-io 717	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 838	wff STAB ph
df-stab 839	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 842	wff DECID ph
df-dc 843	|- (DECID ph <-> ( ph \/ -. ph ) )
wif 986	wff if- ( ph , ps , ch )
df-ifp 987	|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
w3o 1004	wff ( ph \/ ps \/ ch )
w3a 1005	wff ( ph /\ ps /\ ch )
df-3or 1006	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 1007	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1396	wff A. x ph
cv 1397	class x
wceq 1398	wff A = B
wtru 1399	wff T.
df-tru 1401	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1403	wff F.
df-fal 1404	|- ( F. <-> -. T. )
wxo 1420	wff ( ph \/_ ps )
df-xor 1421	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1496	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1497	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1498	|- ph   =>    |- A. x ph
wnf 1509	wff F/ x ph
df-nf 1510	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1541	wff E. x ph
ax-ie1 1542	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1543	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1553	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1554	|- ( A. x x = y -> A. y y = x )
ax-11 1555	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1556	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1558	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1559	|- ( A. x ph -> ph )
ax-17 1575	|- ( ph -> A. x ph )
ax-i9 1579	|- E. x x = y
ax-ial 1583	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1584	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1764	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1811	wff [ y / x ] ph
df-sb 1812	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1863	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1872	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2082	wff E! x ph
wmo 2083	wff E* x ph
df-eu 2085	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2086	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2205	wff A e. B
ax-13 2207	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2208	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2216	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2220	class { x | ph }
df-clab 2221	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2227	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2230	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2373	wff F/_ x A
df-nfc 2375	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2414	wff A =/= B
df-ne 2415	|- ( A =/= B <-> -. A = B )
wnel 2509	wff A e/ B
df-nel 2510	|- ( A e/ B <-> -. A e. B )
wral 2522	wff A. x e. A ph
wrex 2523	wff E. x e. A ph
wreu 2524	wff E! x e. A ph
wrmo 2525	wff E* x e. A ph
crab 2526	class { x e. A | ph }
df-ral 2527	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2528	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2529	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2530	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2531	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2815	class _V
df-v 2817	|- _V = { x | x = x }
wcdeq 3028	wff CondEq ( x = y -> ph )
df-cdeq 3029	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 3045	wff [. A / x ]. ph
df-sbc 3046	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3141	class [_ A / x ]_ B
df-csb 3142	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3211	class ( A \ B )
cun 3212	class ( A u. B )
cin 3213	class ( A i^i B )
wss 3214	wff A C_ B
df-dif 3216	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3218	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3220	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3227	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3512	class (/)
df-nul 3513	|- (/) = ( _V \ _V )
cif 3624	class if ( ph , A , B )
df-if 3625	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3674	class ~P A
df-pw 3676	|- ~P A = { x | x C_ A }
csn 3694	class { A }
cpr 3695	class { A , B }
ctp 3696	class { A , B , C }
cop 3697	class <. A , B >.
cotp 3698	class <. A , B , C >.
df-sn 3700	|- { A } = { x | x = A }
df-pr 3701	|- { A , B } = ( { A } u. { B } )
df-tp 3702	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3703	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3704	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3919	class U. A
df-uni 3920	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3954	class |^| A
df-int 3955	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3996	class U_ x e. A B
ciin 3997	class |^|_ x e. A B
df-iun 3998	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3999	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4090	wff Disj x e. A B
df-disj 4091	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4114	wff A R B
df-br 4115	|- ( A R B <-> <. A , B >. e. R )
copab 4175	class { <. x , y >. | ph }
cmpt 4176	class ( x e. A |-> B )
df-opab 4177	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4178	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4213	wff Tr A
df-tr 4214	|- ( Tr A <-> U. A C_ A )
ax-coll 4230	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4233	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4241	|- E. x A. y -. y e. x
ax-pow 4292	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4312	wff EXMID
df-exmid 4313	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4327	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4413	class _E
cid 4414	class _I
df-eprel 4415	|- _E = { <. x , y >. | x e. y }
df-id 4419	|- _I = { <. x , y >. | x = y }
wpo 4420	wff R Po A
wor 4421	wff R Or A
df-po 4422	|- ( 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 4423	|- ( 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 4453	wff FrFor R A S
wfr 4454	wff R Fr A
wse 4455	wff R Se A
wwe 4456	wff R We A
df-frfor 4457	|- (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 4458	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4459	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4460	|- ( 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 4488	wff Ord A
con0 4489	class On
wlim 4490	wff Lim A
csuc 4491	class suc A
df-iord 4492	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4494	|- On = { x | Ord x }
df-ilim 4495	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4497	|- suc A = ( A u. { A } )
ax-un 4559	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4664	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4715	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4717	class om
df-iom 4718	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4752	class ( A X. B )
ccnv 4753	class `' A
cdm 4754	class dom A
crn 4755	class ran A
cres 4756	class ( A |` B )
cima 4757	class ( A " B )
ccom 4758	class ( A o. B )
wrel 4759	wff Rel A
df-xp 4760	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4761	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4762	|- `' A = { <. x , y >. | y A x }
df-co 4763	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4764	|- dom A = { x | E. y x A y }
df-rn 4765	|- ran A = dom `' A
df-res 4766	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4767	|- ( A " B ) = ran ( A |` B )
cio 5315	class ( iota x ph )
df-iota 5317	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5351	wff Fun A
wfn 5352	wff A Fn B
wf 5353	wff F : A --> B
wf1 5354	wff F : A -1-1-> B
wfo 5355	wff F : A -onto-> B
wf1o 5356	wff F : A -1-1-onto-> B
cfv 5357	class ( F ` A )
wiso 5358	wff H Isom R , S ( A , B )
df-fun 5359	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5360	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5361	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5362	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5363	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5364	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5365	|- ( F ` A ) = ( iota x A F x )
df-isom 5366	|- ( 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 6010	class ( iota_ x e. A ph )
df-riota 6011	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6058	class ( A F B )
coprab 6059	class { <. <. x , y >. , z >. | ph }
cmpo 6060	class ( x e. A , y e. B |-> C )
df-ov 6061	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6062	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6063	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6273	class oF R
cofr 6274	class oR R
df-of 6275	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6276	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6345	class 1st
c2nd 6346	class 2nd
df-1st 6347	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6348	|- 2nd = ( x e. _V |-> U. ran { x } )
csupp 6448	class supp
df-supp 6449	|- supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
ctpos 6488	class tpos F
df-tpos 6489	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6529	wff Smo A
df-smo 6530	|- ( 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 6548	class recs ( F )
df-recs 6549	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6613	class rec ( F , I )
df-irdg 6614	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6634	class frec ( F , I )
df-frec 6635	|- 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 6653	class 1o
c2o 6654	class 2o
c3o 6655	class 3o
c4o 6656	class 4o
coa 6657	class +o
comu 6658	class .o
coei 6659	class ↑o
df-1o 6660	|- 1o = suc (/)
df-2o 6661	|- 2o = suc 1o
df-3o 6662	|- 3o = suc 2o
df-4o 6663	|- 4o = suc 3o
df-oadd 6664	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6665	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6666	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6777	wff R Er A
cec 6778	class [ A ] R
cqs 6779	class ( A /. R )
df-er 6780	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6782	|- [ A ] R = ( R " { A } )
df-qs 6786	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6895	class ^m
cpm 6896	class ^pm
df-map 6897	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6898	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6946	class X_ x e. A B
df-ixp 6947	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6986	class ~~
cdom 6987	class ~<_
cfn 6988	class Fin
df-en 6989	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6990	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6991	|- Fin = { x | E. y e. om x ~~ y }
cfsupp 7251	class finSupp
df-fsupp 7252	|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
cfi 7268	class fi
df-fi 7269	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7286	class sup ( A , B , R )
cinf 7287	class inf ( A , B , R )
df-sup 7288	|- 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 7289	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7341	class ( A ⊔ B )
df-dju 7342	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7349	class inl
cinr 7350	class inr
df-inl 7351	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7352	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7387	class case ( R , S )
df-case 7388	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7406	class ( R ⊔d S )
df-djud 7407	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7423	class ℕ∞
df-nninf 7424	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7438	class Omni
df-omni 7439	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7455	class Markov
df-markov 7456	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7467	class WOmni
df-womni 7468	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7486	class card
wacn 7487	class AC A
df-card 7488	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7489	|- 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 7525	wff CHOICE
df-ac 7526	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7571	wff R Ap A
df-pap 7572	|- ( 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 7578	wff R TAp A
df-tap 7579	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7592	wff CCHOICE
df-cc 7593	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7603	class N.
cpli 7604	class +N
cmi 7605	class .N
clti 7606	class <N
cplpq 7607	class +pQ
cmpq 7608	class .pQ
cltpq 7609	class <pQ
ceq 7610	class ~Q
cnq 7611	class Q.
c1q 7612	class 1Q
cplq 7613	class +Q
cmq 7614	class .Q
crq 7615	class *Q
cltq 7616	class <Q
ceq0 7617	class ~Q0
cnq0 7618	class Q0
c0q0 7619	class 0Q0
cplq0 7620	class +Q0
cmq0 7621	class ·Q0
cnp 7622	class P.
c1p 7623	class 1P
cpp 7624	class +P.
cmp 7625	class .P.
cltp 7626	class <P
cer 7627	class ~R
cnr 7628	class R.
c0r 7629	class 0R
c1r 7630	class 1R
cm1r 7631	class -1R
cplr 7632	class +R
cmr 7633	class .R
cltr 7634	class <R
df-ni 7635	|- N. = ( om \ { (/) } )
df-pli 7636	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7637	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7638	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7675	|- +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 7676	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7677	|- <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 7678	|- ~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 7679	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7680	|- +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 7681	|- .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 7682	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7683	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7684	|- <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 7755	|- ~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 7756	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7757	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7758	|- +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 7759	|- ·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 7797	|- 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 7798	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7799	|- +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 7800	|- .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 7801	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 8057	|- ~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 8058	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 8059	|- +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 8060	|- .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 8061	|- <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 8062	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 8063	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 8064	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8141	class CC
cr 8142	class RR
cc0 8143	class 0
c1 8144	class 1
ci 8145	class _i
caddc 8146	class +
cltrr 8147	class <RR
cmul 8148	class x.
df-c 8149	|- CC = ( R. X. R. )
df-0 8150	|- 0 = <. 0R , 0R >.
df-1 8151	|- 1 = <. 1R , 0R >.
df-i 8152	|- _i = <. 0R , 1R >.
df-r 8153	|- RR = ( R. X. { 0R } )
df-add 8154	|- + = { <. <. 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 8155	|- 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 8156	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8234	|- CC e. _V
ax-resscn 8235	|- RR C_ CC
ax-1cn 8236	|- 1 e. CC
ax-1re 8237	|- 1 e. RR
ax-icn 8238	|- _i e. CC
ax-addcl 8239	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8240	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8241	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8242	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8243	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8244	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8245	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8246	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8247	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8248	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8249	|- 0 <RR 1
ax-1rid 8250	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8251	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8252	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8253	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8254	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8255	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8256	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8257	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8258	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8259	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8260	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8261	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8262	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8263	|- 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 8264	|- ( ( ( 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 8265	|- + : ( CC X. CC ) --> CC
ax-mulf 8266	|- x. : ( CC X. CC ) --> CC
cpnf 8321	class +oo
cmnf 8322	class -oo
cxr 8323	class RR*
clt 8324	class <
cle 8325	class <_
df-pnf 8326	|- +oo = ~P U. CC
df-mnf 8327	|- -oo = ~P +oo
df-xr 8328	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8329	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8330	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8460	class -
cneg 8461	class -u A
df-sub 8462	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8463	|- -u A = ( 0 - A )
creap 8865	class #ℝ
df-reap 8866	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8872	class #
df-ap 8873	|- # = { <. 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 8963	class /
df-div 8964	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9254	class NN
df-inn 9255	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9305	class 2
c3 9306	class 3
c4 9307	class 4
c5 9308	class 5
c6 9309	class 6
c7 9310	class 7
c8 9311	class 8
c9 9312	class 9
df-2 9313	|- 2 = ( 1 + 1 )
df-3 9314	|- 3 = ( 2 + 1 )
df-4 9315	|- 4 = ( 3 + 1 )
df-5 9316	|- 5 = ( 4 + 1 )
df-6 9317	|- 6 = ( 5 + 1 )
df-7 9318	|- 7 = ( 6 + 1 )
df-8 9319	|- 8 = ( 7 + 1 )
df-9 9320	|- 9 = ( 8 + 1 )
cn0 9513	class NN0
df-n0 9514	|- NN0 = ( NN u. { 0 } )
cxnn0 9580	class NN0*
df-xnn0 9581	|- NN0* = ( NN0 u. { +oo } )
cz 9594	class ZZ
df-z 9595	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9727	class ; A B
df-dec 9728	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9871	class ZZ>=
df-uz 9872	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9969	class QQ
df-q 9970	|- QQ = ( / " ( ZZ X. NN ) )
crp 10004	class RR+
df-rp 10005	|- RR+ = { x e. RR | 0 < x }
cxne 10121	class -e A
cxad 10122	class +e
cxmu 10123	class xe
df-xneg 10124	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10125	|- +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 10126	|- 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 10240	class (,)
cioc 10241	class (,]
cico 10242	class [,)
cicc 10243	class [,]
df-ioo 10244	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10245	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10246	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10247	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10361	class ...
df-fz 10362	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10498	class ..^
df-fzo 10499	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10652	class |_
cceil 10653	class ⌈
df-fl 10654	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10655	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10708	class mod
df-mod 10709	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10833	class seq M ( .+ , F )
df-seqfrec 10834	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10924	class ^
df-exp 10925	|- ^ = ( 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 11112	class !
df-fac 11113	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11134	class _C
df-bc 11135	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11163	class ♯
df-ihash 11164	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11249	class Word S
df-word 11250	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11294	class lastS
df-lsw 11295	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11303	class ++
df-concat 11304	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11328	class <" A ">
df-s1 11329	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11362	class substr
df-substr 11363	|- 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 11389	class prefix
df-pfx 11390	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11466	class <" A B ">
cs3 11467	class <" A B C ">
cs4 11468	class <" A B C D ">
cs5 11469	class <" A B C D E ">
cs6 11470	class <" A B C D E F ">
cs7 11471	class <" A B C D E F G ">
cs8 11472	class <" A B C D E F G H ">
df-s2 11473	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11474	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11475	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11476	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11477	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11478	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11479	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11524	class shift
df-shft 11525	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11549	class *
cre 11550	class Re
cim 11551	class Im
df-cj 11552	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11553	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11554	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11706	class sqr
cabs 11707	class abs
df-rsqrt 11708	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11709	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11988	class ~~>
df-clim 11989	|- ~~> = { <. 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 12063	class sum_ k e. A B
df-sumdc 12064	|- 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 12261	class prod_ k e. A B
df-proddc 12262	|- 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 12353	class exp
ceu 12354	class _e
csin 12355	class sin
ccos 12356	class cos
ctan 12357	class tan
cpi 12358	class pi
df-ef 12359	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12360	|- _e = ( exp ` 1 )
df-sin 12361	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12362	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12363	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12364	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12486	class tau
df-tau 12487	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12498	class ||
df-dvds 12499	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12651	class bits
df-bits 12652	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12674	class gcd
df-gcd 12675	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12782	class lcm
df-lcm 12783	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12829	class Prime
df-prm 12830	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12903	class numer
cdenom 12904	class denom
df-numer 12905	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12906	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12930	class odZ
cphi 12931	class phi
df-odz 12932	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12933	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 13007	class pCnt
df-pc 13008	|- 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 13092	class ZZ[_i]
df-gz 13093	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13292	class Struct
cnx 13293	class ndx
csts 13294	class sSet
cslot 13295	class Slot A
cbs 13296	class Base
cress 13297	class ↾s
df-struct 13298	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13299	|- ndx = ( _I |` NN )
df-slot 13300	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13302	|- Base = Slot 1
df-sets 13303	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13304	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13374	class +g
cmulr 13375	class .r
cstv 13376	class *r
csca 13377	class Scalar
cvsca 13378	class .s
cip 13379	class .i
cts 13380	class TopSet
cple 13381	class le
coc 13382	class oc
cds 13383	class dist
cunif 13384	class UnifSet
chom 13385	class Hom
cco 13386	class comp
df-plusg 13387	|- +g = Slot 2
df-mulr 13388	|- .r = Slot 3
df-starv 13389	|- *r = Slot 4
df-sca 13390	|- Scalar = Slot 5
df-vsca 13391	|- .s = Slot 6
df-ip 13392	|- .i = Slot 8
df-tset 13393	|- TopSet = Slot 9
df-ple 13394	|- le = Slot ; 1 0
df-ocomp 13395	|- oc = Slot ; 1 1
df-ds 13396	|- dist = Slot ; 1 2
df-unif 13397	|- UnifSet = Slot ; 1 3
df-hom 13398	|- Hom = Slot ; 1 4
df-cco 13399	|- comp = Slot ; 1 5
crest 13536	class ↾t
ctopn 13537	class TopOpen
df-rest 13538	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13539	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13551	class topGen
cpt 13552	class Xt_
c0g 13553	class 0g
cgsu 13554	class gsumg
df-0g 13555	|- 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-igsum 13556	|- gsumg = ( 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 13557	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13558	|- 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 13565	class "s
cqus 13566	class /.s
df-iimas 13567	|- "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 13568	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
cplusf 13616	class +f
cmgm 13617	class Mgm
df-plusf 13618	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13619	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13664	class Smgrp
df-sgrp 13665	|- 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 13677	class Mnd
df-mnd 13678	|- 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 13712	class MndHom
csubmnd 13713	class SubMnd
df-mhm 13714	|- 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 13715	|- 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 13755	class Grp
cminusg 13756	class invg
csg 13757	class -g
df-grp 13758	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13759	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13760	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13872	class .g
df-mulg 13873	|- .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 13920	class SubGrp
cnsg 13921	class NrmSGrp
cqg 13922	class ~QG
df-subg 13923	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13924	|- 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 13925	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13993	class GrpHom
df-ghm 13994	|- 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 14037	class CMnd
cabl 14038	class Abel
df-cmn 14039	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 14040	|- Abel = ( Grp i^i CMnd )
cgfsu 14100	class gfsumgf
df-gfsum 14101	|- gfsumgf = ( 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 gsumg ( f o. g ) ) ) ) ) )
cprds 14111	class X_s
df-prds 14112	|- 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 14141	class X.s
df-xps 14142	|- 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 14144	class ^s
df-pws 14145	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cmgp 14159	class mulGrp
df-mgp 14160	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 14171	class Rng
df-rng 14172	|- 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 14202	class 1r
df-ur 14203	|- 1r = ( 0g o. mulGrp )
csrg 14206	class SRing
df-srg 14207	|- 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 14239	class Ring
ccrg 14240	class CRing
df-ring 14241	|- 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 14242	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14310	class oppr
df-oppr 14311	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14330	class ||r
cui 14331	class Unit
cir 14332	class Irred
df-dvdsr 14333	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14334	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14335	|- 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 14365	class invr
df-invr 14366	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14376	class /r
df-dvr 14377	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14395	class RingHom
crs 14396	class RingIso
df-rhm 14397	|- 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 14398	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14424	class NzRing
df-nzr 14425	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14435	class LRing
df-lring 14436	|- 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 14443	class SubRng
df-subrng 14444	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14463	class SubRing
crgspn 14464	class RingSpan
df-subrg 14465	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14466	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14501	class RLReg
cdomn 14502	class Domn
cidom 14503	class IDomn
df-rlreg 14504	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14505	|- 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 14506	|- IDomn = ( CRing i^i Domn )
capr 14527	class #r
df-apr 14528	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
cdr 14540	class DivRing
cfield 14541	class Field
df-drngap 14542	|- DivRing = { r e. Ring | (#r ` r ) TAp ( Base ` r ) }
df-field 14543	|- Field = ( DivRing i^i CRing )
clmod 14561	class LMod
cscaf 14562	class .sf
df-lmod 14563	|- 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 14564	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14626	class LSubSp
df-lssm 14627	|- 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 14660	class LSpan
df-lsp 14661	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14707	class subringAlg
crglmod 14708	class ringLMod
df-sra 14709	|- 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 14710	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14741	class LIdeal
crsp 14742	class RSpan
df-lidl 14743	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14744	|- RSpan = ( LSpan o. ringLMod )
c2idl 14773	class 2Ideal
df-2idl 14774	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14809	class PsMet
cxmet 14810	class *Met
cmet 14811	class Met
cbl 14812	class ball
cfbas 14813	class fBas
cfg 14814	class filGen
cmopn 14815	class MetOpen
cmetu 14816	class metUnif
df-psmet 14817	|- 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 14818	|- *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 14819	|- 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 14820	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14821	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14822	|- 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 14823	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14824	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14830	class ℂfld
df-cnfld 14831	|- ℂ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 14864	class ℤring
df-zring 14865	|- ℤring = (ℂfld ↾s ZZ )
czrh 14885	class ZRHom
czlm 14886	class ZMod
czn 14887	class ℤ/nℤ
df-zrh 14888	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14889	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14890	|- ℤ/nℤ = ( n e. NN0 |-> [_ℤring / z ]_ [_ ( z /.s ( z ~QG ( (RSpan ` z ) ` { n } ) ) ) / s ]_ ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. ) )
cmps 14935	class mPwSer
cmpl 14936	class mPoly
df-psr 14937	|- 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 14938	|- 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 14988	class Top
df-top 14989	|- 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 15001	class TopOn
df-topon 15002	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 15021	class TopSp
df-topsp 15022	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 15033	class TopBases
df-bases 15034	|- 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 15083	class Clsd
cnt 15084	class int
ccl 15085	class cls
df-cld 15086	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 15087	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 15088	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 15129	class nei
df-nei 15130	|- 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 15176	class Cn
ccnp 15177	class CnP
clm 15178	class ~~> t
df-cn 15179	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 15180	|- 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 15181	|- ~~> 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 15243	class tX
df-tx 15244	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15291	class Homeo
df-hmeo 15292	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15327	class *MetSp
cms 15328	class MetSp
ctms 15329	class toMetSp
df-xms 15330	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15331	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15332	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15561	class -cn->
df-cncf 15562	|- -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 15645	class lim CC
cdv 15646	class _D
df-limced 15647	|- 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 15648	|- _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 15719	class Poly
cidp 15720	class Xp
df-ply 15721	|- 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 15722	|- Xp = ( _I |` CC )
clog 15847	class log
ccxp 15848	class ^c
df-relog 15849	|- log = `' ( exp |` RR )
df-rpcxp 15850	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15934	class logb
df-logb 15935	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15975	class sigma
df-sgm 15976	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15996	class /L
df-lgs 15997	|- /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 16125	class .ef
df-edgf 16126	|- .ef = Slot ; 1 8
cvtx 16133	class Vtx
ciedg 16134	class iEdg
df-vtx 16135	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 16136	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 16178	class Edg
df-edg 16179	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 16188	class UHGraph
cushgr 16189	class USHGraph
df-uhgrm 16190	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 16191	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 16212	class UPGraph
cumgr 16213	class UMGraph
df-upgren 16214	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 16215	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16274	class USPGraph
cusgr 16275	class USGraph
df-uspgren 16276	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16277	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16374	class SubGraph
df-subgr 16375	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16407	class VtxDeg
df-vtxdg 16408	|- 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 16438	class Walks
df-wlks 16439	|- 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 16501	class Trails
df-trls 16502	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16512	class ClWWalks
df-clwwlk 16513	|- 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 16524	class ClWWalksN
df-clwwlkn 16525	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16547	class ClWWalksNOn
df-clwwlknon 16548	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16563	class EulerPaths
df-eupth 16564	|- 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 16691	wff A DECIDin B
df-dcin 16692	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16708	wff BOUNDED ph
ax-bd0 16709	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16710	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16711	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16712	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16713	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16714	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16715	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16716	|- BOUNDED x = y
ax-bdel 16717	|- BOUNDED x e. y
ax-bdsb 16718	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16736	wff BOUNDED A
df-bdc 16737	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16780	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16820	|- BOUNDED ph   =>    |- DECID ph
wind 16822	wff Ind A
df-bj-ind 16823	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16837	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16864	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16872	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16878	|- 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 16883	|- 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 16885	|- ( ( ( 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 ) ) )
walsi 16988	wff A.! x ( ph -> ps )
walsc 16989	wff A.! x e. A ph
df-alsi 16990	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 16991	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )