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 3027	wff CondEq ( x = y -> ph )
df-cdeq 3028	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 3044	wff [. A / x ]. ph
df-sbc 3045	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3140	class [_ A / x ]_ B
df-csb 3141	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3210	class ( A \ B )
cun 3211	class ( A u. B )
cin 3212	class ( A i^i B )
wss 3213	wff A C_ B
df-dif 3215	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3217	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3219	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3226	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3510	class (/)
df-nul 3511	|- (/) = ( _V \ _V )
cif 3622	class if ( ph , A , B )
df-if 3623	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3671	class ~P A
df-pw 3673	|- ~P A = { x | x C_ A }
csn 3691	class { A }
cpr 3692	class { A , B }
ctp 3693	class { A , B , C }
cop 3694	class <. A , B >.
cotp 3695	class <. A , B , C >.
df-sn 3697	|- { A } = { x | x = A }
df-pr 3698	|- { A , B } = ( { A } u. { B } )
df-tp 3699	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3700	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3701	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3916	class U. A
df-uni 3917	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3951	class |^| A
df-int 3952	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3993	class U_ x e. A B
ciin 3994	class |^|_ x e. A B
df-iun 3995	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3996	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4087	wff Disj x e. A B
df-disj 4088	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4111	wff A R B
df-br 4112	|- ( A R B <-> <. A , B >. e. R )
copab 4172	class { <. x , y >. | ph }
cmpt 4173	class ( x e. A |-> B )
df-opab 4174	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4175	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4210	wff Tr A
df-tr 4211	|- ( Tr A <-> U. A C_ A )
ax-coll 4227	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4230	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4238	|- E. x A. y -. y e. x
ax-pow 4289	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4309	wff EXMID
df-exmid 4310	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4324	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4410	class _E
cid 4411	class _I
df-eprel 4412	|- _E = { <. x , y >. | x e. y }
df-id 4416	|- _I = { <. x , y >. | x = y }
wpo 4417	wff R Po A
wor 4418	wff R Or A
df-po 4419	|- ( 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 4420	|- ( 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 4450	wff FrFor R A S
wfr 4451	wff R Fr A
wse 4452	wff R Se A
wwe 4453	wff R We A
df-frfor 4454	|- (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 4455	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4456	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4457	|- ( 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 4485	wff Ord A
con0 4486	class On
wlim 4487	wff Lim A
csuc 4488	class suc A
df-iord 4489	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4491	|- On = { x | Ord x }
df-ilim 4492	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4494	|- suc A = ( A u. { A } )
ax-un 4556	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4661	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4712	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4714	class om
df-iom 4715	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4749	class ( A X. B )
ccnv 4750	class `' A
cdm 4751	class dom A
crn 4752	class ran A
cres 4753	class ( A |` B )
cima 4754	class ( A " B )
ccom 4755	class ( A o. B )
wrel 4756	wff Rel A
df-xp 4757	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4758	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4759	|- `' A = { <. x , y >. | y A x }
df-co 4760	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4761	|- dom A = { x | E. y x A y }
df-rn 4762	|- ran A = dom `' A
df-res 4763	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4764	|- ( A " B ) = ran ( A |` B )
cio 5312	class ( iota x ph )
df-iota 5314	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5348	wff Fun A
wfn 5349	wff A Fn B
wf 5350	wff F : A --> B
wf1 5351	wff F : A -1-1-> B
wfo 5352	wff F : A -onto-> B
wf1o 5353	wff F : A -1-1-onto-> B
cfv 5354	class ( F ` A )
wiso 5355	wff H Isom R , S ( A , B )
df-fun 5356	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5357	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5358	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5359	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5360	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5361	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5362	|- ( F ` A ) = ( iota x A F x )
df-isom 5363	|- ( 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 6004	class ( iota_ x e. A ph )
df-riota 6005	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6052	class ( A F B )
coprab 6053	class { <. <. x , y >. , z >. | ph }
cmpo 6054	class ( x e. A , y e. B |-> C )
df-ov 6055	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6056	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6057	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6266	class oF R
cofr 6267	class oR R
df-of 6268	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6269	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6334	class 1st
c2nd 6335	class 2nd
df-1st 6336	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6337	|- 2nd = ( x e. _V |-> U. ran { x } )
csupp 6437	class supp
df-supp 6438	|- supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
ctpos 6477	class tpos F
df-tpos 6478	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6518	wff Smo A
df-smo 6519	|- ( 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 6537	class recs ( F )
df-recs 6538	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6602	class rec ( F , I )
df-irdg 6603	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6623	class frec ( F , I )
df-frec 6624	|- 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 6642	class 1o
c2o 6643	class 2o
c3o 6644	class 3o
c4o 6645	class 4o
coa 6646	class +o
comu 6647	class .o
coei 6648	class ↑o
df-1o 6649	|- 1o = suc (/)
df-2o 6650	|- 2o = suc 1o
df-3o 6651	|- 3o = suc 2o
df-4o 6652	|- 4o = suc 3o
df-oadd 6653	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6654	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6655	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6766	wff R Er A
cec 6767	class [ A ] R
cqs 6768	class ( A /. R )
df-er 6769	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6771	|- [ A ] R = ( R " { A } )
df-qs 6775	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6884	class ^m
cpm 6885	class ^pm
df-map 6886	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6887	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6935	class X_ x e. A B
df-ixp 6936	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6975	class ~~
cdom 6976	class ~<_
cfn 6977	class Fin
df-en 6978	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6979	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6980	|- Fin = { x | E. y e. om x ~~ y }
cfsupp 7240	class finSupp
df-fsupp 7241	|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
cfi 7257	class fi
df-fi 7258	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7275	class sup ( A , B , R )
cinf 7276	class inf ( A , B , R )
df-sup 7277	|- 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 7278	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7330	class ( A ⊔ B )
df-dju 7331	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7338	class inl
cinr 7339	class inr
df-inl 7340	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7341	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7376	class case ( R , S )
df-case 7377	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7395	class ( R ⊔d S )
df-djud 7396	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7412	class ℕ∞
df-nninf 7413	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7427	class Omni
df-omni 7428	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7444	class Markov
df-markov 7445	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7456	class WOmni
df-womni 7457	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7475	class card
wacn 7476	class AC A
df-card 7477	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7478	|- 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 7514	wff CHOICE
df-ac 7515	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7560	wff R Ap A
df-pap 7561	|- ( 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 7565	wff R TAp A
df-tap 7566	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7578	wff CCHOICE
df-cc 7579	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7589	class N.
cpli 7590	class +N
cmi 7591	class .N
clti 7592	class <N
cplpq 7593	class +pQ
cmpq 7594	class .pQ
cltpq 7595	class <pQ
ceq 7596	class ~Q
cnq 7597	class Q.
c1q 7598	class 1Q
cplq 7599	class +Q
cmq 7600	class .Q
crq 7601	class *Q
cltq 7602	class <Q
ceq0 7603	class ~Q0
cnq0 7604	class Q0
c0q0 7605	class 0Q0
cplq0 7606	class +Q0
cmq0 7607	class ·Q0
cnp 7608	class P.
c1p 7609	class 1P
cpp 7610	class +P.
cmp 7611	class .P.
cltp 7612	class <P
cer 7613	class ~R
cnr 7614	class R.
c0r 7615	class 0R
c1r 7616	class 1R
cm1r 7617	class -1R
cplr 7618	class +R
cmr 7619	class .R
cltr 7620	class <R
df-ni 7621	|- N. = ( om \ { (/) } )
df-pli 7622	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7623	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7624	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7661	|- +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 7662	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7663	|- <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 7664	|- ~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 7665	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7666	|- +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 7667	|- .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 7668	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7669	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7670	|- <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 7741	|- ~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 7742	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7743	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7744	|- +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 7745	|- ·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 7783	|- 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 7784	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7785	|- +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 7786	|- .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 7787	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 8043	|- ~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 8044	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 8045	|- +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 8046	|- .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 8047	|- <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 8048	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 8049	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 8050	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8127	class CC
cr 8128	class RR
cc0 8129	class 0
c1 8130	class 1
ci 8131	class _i
caddc 8132	class +
cltrr 8133	class <RR
cmul 8134	class x.
df-c 8135	|- CC = ( R. X. R. )
df-0 8136	|- 0 = <. 0R , 0R >.
df-1 8137	|- 1 = <. 1R , 0R >.
df-i 8138	|- _i = <. 0R , 1R >.
df-r 8139	|- RR = ( R. X. { 0R } )
df-add 8140	|- + = { <. <. 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 8141	|- 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 8142	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8220	|- CC e. _V
ax-resscn 8221	|- RR C_ CC
ax-1cn 8222	|- 1 e. CC
ax-1re 8223	|- 1 e. RR
ax-icn 8224	|- _i e. CC
ax-addcl 8225	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8226	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8227	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8228	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8229	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8230	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8231	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8232	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8233	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8234	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8235	|- 0 <RR 1
ax-1rid 8236	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8237	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8238	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8239	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8240	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8241	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8242	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8243	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8244	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8245	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8246	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8247	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8248	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8249	|- 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 8250	|- ( ( ( 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 8251	|- + : ( CC X. CC ) --> CC
ax-mulf 8252	|- x. : ( CC X. CC ) --> CC
cpnf 8307	class +oo
cmnf 8308	class -oo
cxr 8309	class RR*
clt 8310	class <
cle 8311	class <_
df-pnf 8312	|- +oo = ~P U. CC
df-mnf 8313	|- -oo = ~P +oo
df-xr 8314	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8315	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8316	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8446	class -
cneg 8447	class -u A
df-sub 8448	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8449	|- -u A = ( 0 - A )
creap 8850	class #ℝ
df-reap 8851	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8857	class #
df-ap 8858	|- # = { <. 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 8948	class /
df-div 8949	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9239	class NN
df-inn 9240	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9290	class 2
c3 9291	class 3
c4 9292	class 4
c5 9293	class 5
c6 9294	class 6
c7 9295	class 7
c8 9296	class 8
c9 9297	class 9
df-2 9298	|- 2 = ( 1 + 1 )
df-3 9299	|- 3 = ( 2 + 1 )
df-4 9300	|- 4 = ( 3 + 1 )
df-5 9301	|- 5 = ( 4 + 1 )
df-6 9302	|- 6 = ( 5 + 1 )
df-7 9303	|- 7 = ( 6 + 1 )
df-8 9304	|- 8 = ( 7 + 1 )
df-9 9305	|- 9 = ( 8 + 1 )
cn0 9498	class NN0
df-n0 9499	|- NN0 = ( NN u. { 0 } )
cxnn0 9565	class NN0*
df-xnn0 9566	|- NN0* = ( NN0 u. { +oo } )
cz 9579	class ZZ
df-z 9580	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9712	class ; A B
df-dec 9713	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9856	class ZZ>=
df-uz 9857	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9954	class QQ
df-q 9955	|- QQ = ( / " ( ZZ X. NN ) )
crp 9989	class RR+
df-rp 9990	|- RR+ = { x e. RR | 0 < x }
cxne 10105	class -e A
cxad 10106	class +e
cxmu 10107	class xe
df-xneg 10108	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10109	|- +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 10110	|- 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 10224	class (,)
cioc 10225	class (,]
cico 10226	class [,)
cicc 10227	class [,]
df-ioo 10228	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10229	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10230	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10231	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10345	class ...
df-fz 10346	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10480	class ..^
df-fzo 10481	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10632	class |_
cceil 10633	class ⌈
df-fl 10634	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10635	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10688	class mod
df-mod 10689	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10813	class seq M ( .+ , F )
df-seqfrec 10814	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10904	class ^
df-exp 10905	|- ^ = ( 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 11091	class !
df-fac 11092	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11113	class _C
df-bc 11114	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11142	class ♯
df-ihash 11143	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11228	class Word S
df-word 11229	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11273	class lastS
df-lsw 11274	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11282	class ++
df-concat 11283	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11307	class <" A ">
df-s1 11308	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11341	class substr
df-substr 11342	|- 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 11368	class prefix
df-pfx 11369	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11445	class <" A B ">
cs3 11446	class <" A B C ">
cs4 11447	class <" A B C D ">
cs5 11448	class <" A B C D E ">
cs6 11449	class <" A B C D E F ">
cs7 11450	class <" A B C D E F G ">
cs8 11451	class <" A B C D E F G H ">
df-s2 11452	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11453	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11454	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11455	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11456	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11457	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11458	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11503	class shift
df-shft 11504	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11528	class *
cre 11529	class Re
cim 11530	class Im
df-cj 11531	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11532	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11533	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11685	class sqr
cabs 11686	class abs
df-rsqrt 11687	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11688	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11967	class ~~>
df-clim 11968	|- ~~> = { <. 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 12042	class sum_ k e. A B
df-sumdc 12043	|- 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 12240	class prod_ k e. A B
df-proddc 12241	|- 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 12332	class exp
ceu 12333	class _e
csin 12334	class sin
ccos 12335	class cos
ctan 12336	class tan
cpi 12337	class pi
df-ef 12338	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12339	|- _e = ( exp ` 1 )
df-sin 12340	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12341	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12342	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12343	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12465	class tau
df-tau 12466	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12477	class ||
df-dvds 12478	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12630	class bits
df-bits 12631	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12653	class gcd
df-gcd 12654	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12761	class lcm
df-lcm 12762	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12808	class Prime
df-prm 12809	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12882	class numer
cdenom 12883	class denom
df-numer 12884	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12885	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12909	class odZ
cphi 12910	class phi
df-odz 12911	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12912	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12986	class pCnt
df-pc 12987	|- 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 13071	class ZZ[_i]
df-gz 13072	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13225	class Struct
cnx 13226	class ndx
csts 13227	class sSet
cslot 13228	class Slot A
cbs 13229	class Base
cress 13230	class ↾s
df-struct 13231	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13232	|- ndx = ( _I |` NN )
df-slot 13233	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13235	|- Base = Slot 1
df-sets 13236	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13237	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13307	class +g
cmulr 13308	class .r
cstv 13309	class *r
csca 13310	class Scalar
cvsca 13311	class .s
cip 13312	class .i
cts 13313	class TopSet
cple 13314	class le
coc 13315	class oc
cds 13316	class dist
cunif 13317	class UnifSet
chom 13318	class Hom
cco 13319	class comp
df-plusg 13320	|- +g = Slot 2
df-mulr 13321	|- .r = Slot 3
df-starv 13322	|- *r = Slot 4
df-sca 13323	|- Scalar = Slot 5
df-vsca 13324	|- .s = Slot 6
df-ip 13325	|- .i = Slot 8
df-tset 13326	|- TopSet = Slot 9
df-ple 13327	|- le = Slot ; 1 0
df-ocomp 13328	|- oc = Slot ; 1 1
df-ds 13329	|- dist = Slot ; 1 2
df-unif 13330	|- UnifSet = Slot ; 1 3
df-hom 13331	|- Hom = Slot ; 1 4
df-cco 13332	|- comp = Slot ; 1 5
crest 13469	class ↾t
ctopn 13470	class TopOpen
df-rest 13471	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13472	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13484	class topGen
cpt 13485	class Xt_
c0g 13486	class 0g
cgsu 13487	class gsumg
df-0g 13488	|- 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 13489	|- 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 13490	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13491	|- 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 ) ) } ) )
cprds 13495	class X_s
cpws 13496	class ^s
df-prds 13497	|- 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 ) ) ) ) ) >. } ) ) )
df-pws 13520	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13529	class "s
cqus 13530	class /.s
cxps 13531	class X.s
df-iimas 13532	|- "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 13533	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13534	|- 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 >. } ) ) )
cplusf 13583	class +f
cmgm 13584	class Mgm
df-plusf 13585	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13586	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13631	class Smgrp
df-sgrp 13632	|- 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 13646	class Mnd
df-mnd 13647	|- 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 13687	class MndHom
csubmnd 13688	class SubMnd
df-mhm 13689	|- 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 13690	|- 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 13730	class Grp
cminusg 13731	class invg
csg 13732	class -g
df-grp 13733	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13734	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13735	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13853	class .g
df-mulg 13854	|- .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 13901	class SubGrp
cnsg 13902	class NrmSGrp
cqg 13903	class ~QG
df-subg 13904	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13905	|- 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 13906	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13974	class GrpHom
df-ghm 13975	|- 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 14018	class CMnd
cabl 14019	class Abel
df-cmn 14020	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 14021	|- Abel = ( Grp i^i CMnd )
cmgp 14081	class mulGrp
df-mgp 14082	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 14093	class Rng
df-rng 14094	|- 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 14120	class 1r
df-ur 14121	|- 1r = ( 0g o. mulGrp )
csrg 14124	class SRing
df-srg 14125	|- 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 14157	class Ring
ccrg 14158	class CRing
df-ring 14159	|- 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 14160	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14228	class oppr
df-oppr 14229	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14247	class ||r
cui 14248	class Unit
cir 14249	class Irred
df-dvdsr 14250	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14251	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14252	|- 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 14282	class invr
df-invr 14283	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14293	class /r
df-dvr 14294	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14312	class RingHom
crs 14313	class RingIso
df-rhm 14314	|- 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 14315	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14341	class NzRing
df-nzr 14342	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14352	class LRing
df-lring 14353	|- 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 14359	class SubRng
df-subrng 14360	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14379	class SubRing
crgspn 14380	class RingSpan
df-subrg 14381	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14382	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14417	class RLReg
cdomn 14418	class Domn
cidom 14419	class IDomn
df-rlreg 14420	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14421	|- 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 14422	|- IDomn = ( CRing i^i Domn )
capr 14443	class #r
df-apr 14444	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 14452	class LMod
cscaf 14453	class .sf
df-lmod 14454	|- 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 14455	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14517	class LSubSp
df-lssm 14518	|- 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 14551	class LSpan
df-lsp 14552	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14598	class subringAlg
crglmod 14599	class ringLMod
df-sra 14600	|- 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 14601	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14632	class LIdeal
crsp 14633	class RSpan
df-lidl 14634	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14635	|- RSpan = ( LSpan o. ringLMod )
c2idl 14664	class 2Ideal
df-2idl 14665	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14700	class PsMet
cxmet 14701	class *Met
cmet 14702	class Met
cbl 14703	class ball
cfbas 14704	class fBas
cfg 14705	class filGen
cmopn 14706	class MetOpen
cmetu 14707	class metUnif
df-psmet 14708	|- 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 14709	|- *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 14710	|- 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 14711	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14712	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14713	|- 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 14714	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14715	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14721	class ℂfld
df-cnfld 14722	|- ℂ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 14755	class ℤring
df-zring 14756	|- ℤring = (ℂfld ↾s ZZ )
czrh 14776	class ZRHom
czlm 14777	class ZMod
czn 14778	class ℤ/nℤ
df-zrh 14779	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14780	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14781	|- ℤ/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 14826	class mPwSer
cmpl 14827	class mPoly
df-psr 14828	|- 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 14829	|- 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 14879	class Top
df-top 14880	|- 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 14892	class TopOn
df-topon 14893	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14912	class TopSp
df-topsp 14913	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14924	class TopBases
df-bases 14925	|- 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 14974	class Clsd
cnt 14975	class int
ccl 14976	class cls
df-cld 14977	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14978	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14979	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 15020	class nei
df-nei 15021	|- 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 15067	class Cn
ccnp 15068	class CnP
clm 15069	class ~~> t
df-cn 15070	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 15071	|- 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 15072	|- ~~> 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 15134	class tX
df-tx 15135	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15182	class Homeo
df-hmeo 15183	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15218	class *MetSp
cms 15219	class MetSp
ctms 15220	class toMetSp
df-xms 15221	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15222	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15223	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15452	class -cn->
df-cncf 15453	|- -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 15536	class lim CC
cdv 15537	class _D
df-limced 15538	|- 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 15539	|- _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 15610	class Poly
cidp 15611	class Xp
df-ply 15612	|- 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 15613	|- Xp = ( _I |` CC )
clog 15738	class log
ccxp 15739	class ^c
df-relog 15740	|- log = `' ( exp |` RR )
df-rpcxp 15741	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15825	class logb
df-logb 15826	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15866	class sigma
df-sgm 15867	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15887	class /L
df-lgs 15888	|- /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 16016	class .ef
df-edgf 16017	|- .ef = Slot ; 1 8
cvtx 16024	class Vtx
ciedg 16025	class iEdg
df-vtx 16026	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 16027	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 16069	class Edg
df-edg 16070	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 16079	class UHGraph
cushgr 16080	class USHGraph
df-uhgrm 16081	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 16082	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 16103	class UPGraph
cumgr 16104	class UMGraph
df-upgren 16105	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 16106	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16165	class USPGraph
cusgr 16166	class USGraph
df-uspgren 16167	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16168	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16265	class SubGraph
df-subgr 16266	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16298	class VtxDeg
df-vtxdg 16299	|- 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 16329	class Walks
df-wlks 16330	|- 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 16392	class Trails
df-trls 16393	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16403	class ClWWalks
df-clwwlk 16404	|- 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 16415	class ClWWalksN
df-clwwlkn 16416	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16438	class ClWWalksNOn
df-clwwlknon 16439	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16454	class EulerPaths
df-eupth 16455	|- 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 16582	wff A DECIDin B
df-dcin 16583	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16599	wff BOUNDED ph
ax-bd0 16600	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16601	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16602	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16603	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16604	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16605	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16606	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16607	|- BOUNDED x = y
ax-bdel 16608	|- BOUNDED x e. y
ax-bdsb 16609	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16627	wff BOUNDED A
df-bdc 16628	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16671	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16711	|- BOUNDED ph   =>    |- DECID ph
wind 16713	wff Ind A
df-bj-ind 16714	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16728	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16755	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16763	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16769	|- 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 16774	|- 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 16776	|- ( ( ( 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 ) ) )
cgfsu 16877	class gfsumgf
df-gfsum 16878	|- 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 ) ) ) ) ) )
walsi 16890	wff A.! x ( ph -> ps )
walsc 16891	wff A.! x e. A ph
df-alsi 16892	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 16893	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )