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 1810	wff [ y / x ] ph
df-sb 1811	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1862	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1871	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2079	wff E! x ph
wmo 2080	wff E* x ph
df-eu 2082	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2083	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2202	wff A e. B
ax-13 2204	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2205	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2213	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2217	class { x | ph }
df-clab 2218	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2224	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2227	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2362	wff F/_ x A
df-nfc 2364	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2403	wff A =/= B
df-ne 2404	|- ( A =/= B <-> -. A = B )
wnel 2498	wff A e/ B
df-nel 2499	|- ( A e/ B <-> -. A e. B )
wral 2511	wff A. x e. A ph
wrex 2512	wff E. x e. A ph
wreu 2513	wff E! x e. A ph
wrmo 2514	wff E* x e. A ph
crab 2515	class { x e. A | ph }
df-ral 2516	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2517	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2518	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2519	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2520	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2803	class _V
df-v 2805	|- _V = { x | x = x }
wcdeq 3015	wff CondEq ( x = y -> ph )
df-cdeq 3016	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 3032	wff [. A / x ]. ph
df-sbc 3033	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3128	class [_ A / x ]_ B
df-csb 3129	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3198	class ( A \ B )
cun 3199	class ( A u. B )
cin 3200	class ( A i^i B )
wss 3201	wff A C_ B
df-dif 3203	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3205	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3207	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3214	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3496	class (/)
df-nul 3497	|- (/) = ( _V \ _V )
cif 3607	class if ( ph , A , B )
df-if 3608	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3656	class ~P A
df-pw 3658	|- ~P A = { x | x C_ A }
csn 3673	class { A }
cpr 3674	class { A , B }
ctp 3675	class { A , B , C }
cop 3676	class <. A , B >.
cotp 3677	class <. A , B , C >.
df-sn 3679	|- { A } = { x | x = A }
df-pr 3680	|- { A , B } = ( { A } u. { B } )
df-tp 3681	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3682	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3683	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3898	class U. A
df-uni 3899	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3933	class |^| A
df-int 3934	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3975	class U_ x e. A B
ciin 3976	class |^|_ x e. A B
df-iun 3977	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3978	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4069	wff Disj x e. A B
df-disj 4070	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4093	wff A R B
df-br 4094	|- ( A R B <-> <. A , B >. e. R )
copab 4154	class { <. x , y >. | ph }
cmpt 4155	class ( x e. A |-> B )
df-opab 4156	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4157	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4192	wff Tr A
df-tr 4193	|- ( Tr A <-> U. A C_ A )
ax-coll 4209	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4212	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4220	|- E. x A. y -. y e. x
ax-pow 4270	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4290	wff EXMID
df-exmid 4291	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4305	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4390	class _E
cid 4391	class _I
df-eprel 4392	|- _E = { <. x , y >. | x e. y }
df-id 4396	|- _I = { <. x , y >. | x = y }
wpo 4397	wff R Po A
wor 4398	wff R Or A
df-po 4399	|- ( 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 4400	|- ( 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 4430	wff FrFor R A S
wfr 4431	wff R Fr A
wse 4432	wff R Se A
wwe 4433	wff R We A
df-frfor 4434	|- (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 4435	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4436	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4437	|- ( 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 4465	wff Ord A
con0 4466	class On
wlim 4467	wff Lim A
csuc 4468	class suc A
df-iord 4469	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4471	|- On = { x | Ord x }
df-ilim 4472	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4474	|- suc A = ( A u. { A } )
ax-un 4536	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4641	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4692	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4694	class om
df-iom 4695	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4729	class ( A X. B )
ccnv 4730	class `' A
cdm 4731	class dom A
crn 4732	class ran A
cres 4733	class ( A |` B )
cima 4734	class ( A " B )
ccom 4735	class ( A o. B )
wrel 4736	wff Rel A
df-xp 4737	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4738	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4739	|- `' A = { <. x , y >. | y A x }
df-co 4740	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4741	|- dom A = { x | E. y x A y }
df-rn 4742	|- ran A = dom `' A
df-res 4743	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4744	|- ( A " B ) = ran ( A |` B )
cio 5291	class ( iota x ph )
df-iota 5293	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5327	wff Fun A
wfn 5328	wff A Fn B
wf 5329	wff F : A --> B
wf1 5330	wff F : A -1-1-> B
wfo 5331	wff F : A -onto-> B
wf1o 5332	wff F : A -1-1-onto-> B
cfv 5333	class ( F ` A )
wiso 5334	wff H Isom R , S ( A , B )
df-fun 5335	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5336	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5337	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5338	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5339	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5340	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5341	|- ( F ` A ) = ( iota x A F x )
df-isom 5342	|- ( 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 5980	class ( iota_ x e. A ph )
df-riota 5981	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6028	class ( A F B )
coprab 6029	class { <. <. x , y >. , z >. | ph }
cmpo 6030	class ( x e. A , y e. B |-> C )
df-ov 6031	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6032	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6033	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6242	class oF R
cofr 6243	class oR R
df-of 6244	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6245	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6310	class 1st
c2nd 6311	class 2nd
df-1st 6312	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6313	|- 2nd = ( x e. _V |-> U. ran { x } )
csupp 6413	class supp
df-supp 6414	|- supp = ( x e. _V , z e. _V |-> { i e. dom x | ( x " { i } ) =/= { z } } )
ctpos 6453	class tpos F
df-tpos 6454	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6494	wff Smo A
df-smo 6495	|- ( 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 6513	class recs ( F )
df-recs 6514	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6578	class rec ( F , I )
df-irdg 6579	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6599	class frec ( F , I )
df-frec 6600	|- 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 6618	class 1o
c2o 6619	class 2o
c3o 6620	class 3o
c4o 6621	class 4o
coa 6622	class +o
comu 6623	class .o
coei 6624	class ↑o
df-1o 6625	|- 1o = suc (/)
df-2o 6626	|- 2o = suc 1o
df-3o 6627	|- 3o = suc 2o
df-4o 6628	|- 4o = suc 3o
df-oadd 6629	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6630	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6631	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6742	wff R Er A
cec 6743	class [ A ] R
cqs 6744	class ( A /. R )
df-er 6745	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6747	|- [ A ] R = ( R " { A } )
df-qs 6751	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6860	class ^m
cpm 6861	class ^pm
df-map 6862	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6863	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6910	class X_ x e. A B
df-ixp 6911	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6950	class ~~
cdom 6951	class ~<_
cfn 6952	class Fin
df-en 6953	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6954	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6955	|- Fin = { x | E. y e. om x ~~ y }
cfsupp 7210	class finSupp
df-fsupp 7211	|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
cfi 7227	class fi
df-fi 7228	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7241	class sup ( A , B , R )
cinf 7242	class inf ( A , B , R )
df-sup 7243	|- 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 7244	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7296	class ( A ⊔ B )
df-dju 7297	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7304	class inl
cinr 7305	class inr
df-inl 7306	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7307	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7342	class case ( R , S )
df-case 7343	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7361	class ( R ⊔d S )
df-djud 7362	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7378	class ℕ∞
df-nninf 7379	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7393	class Omni
df-omni 7394	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7410	class Markov
df-markov 7411	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7422	class WOmni
df-womni 7423	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7441	class card
wacn 7442	class AC A
df-card 7443	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7444	|- 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 7480	wff CHOICE
df-ac 7481	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7526	wff R Ap A
df-pap 7527	|- ( 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 7528	wff R TAp A
df-tap 7529	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7541	wff CCHOICE
df-cc 7542	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7552	class N.
cpli 7553	class +N
cmi 7554	class .N
clti 7555	class <N
cplpq 7556	class +pQ
cmpq 7557	class .pQ
cltpq 7558	class <pQ
ceq 7559	class ~Q
cnq 7560	class Q.
c1q 7561	class 1Q
cplq 7562	class +Q
cmq 7563	class .Q
crq 7564	class *Q
cltq 7565	class <Q
ceq0 7566	class ~Q0
cnq0 7567	class Q0
c0q0 7568	class 0Q0
cplq0 7569	class +Q0
cmq0 7570	class ·Q0
cnp 7571	class P.
c1p 7572	class 1P
cpp 7573	class +P.
cmp 7574	class .P.
cltp 7575	class <P
cer 7576	class ~R
cnr 7577	class R.
c0r 7578	class 0R
c1r 7579	class 1R
cm1r 7580	class -1R
cplr 7581	class +R
cmr 7582	class .R
cltr 7583	class <R
df-ni 7584	|- N. = ( om \ { (/) } )
df-pli 7585	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7586	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7587	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7624	|- +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 7625	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7626	|- <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 7627	|- ~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 7628	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7629	|- +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 7630	|- .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 7631	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7632	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7633	|- <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 7704	|- ~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 7705	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7706	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7707	|- +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 7708	|- ·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 7746	|- 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 7747	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7748	|- +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 7749	|- .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 7750	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 8006	|- ~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 8007	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 8008	|- +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 8009	|- .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 8010	|- <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 8011	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 8012	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 8013	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8090	class CC
cr 8091	class RR
cc0 8092	class 0
c1 8093	class 1
ci 8094	class _i
caddc 8095	class +
cltrr 8096	class <RR
cmul 8097	class x.
df-c 8098	|- CC = ( R. X. R. )
df-0 8099	|- 0 = <. 0R , 0R >.
df-1 8100	|- 1 = <. 1R , 0R >.
df-i 8101	|- _i = <. 0R , 1R >.
df-r 8102	|- RR = ( R. X. { 0R } )
df-add 8103	|- + = { <. <. 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 8104	|- 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 8105	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8183	|- CC e. _V
ax-resscn 8184	|- RR C_ CC
ax-1cn 8185	|- 1 e. CC
ax-1re 8186	|- 1 e. RR
ax-icn 8187	|- _i e. CC
ax-addcl 8188	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8189	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8190	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8191	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8192	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8193	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8194	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8195	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8196	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8197	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8198	|- 0 <RR 1
ax-1rid 8199	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8200	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8201	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8202	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8203	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8204	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8205	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8206	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8207	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8208	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8209	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8210	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8211	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8212	|- 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 8213	|- ( ( ( 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 8214	|- + : ( CC X. CC ) --> CC
ax-mulf 8215	|- x. : ( CC X. CC ) --> CC
cpnf 8270	class +oo
cmnf 8271	class -oo
cxr 8272	class RR*
clt 8273	class <
cle 8274	class <_
df-pnf 8275	|- +oo = ~P U. CC
df-mnf 8276	|- -oo = ~P +oo
df-xr 8277	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8278	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8279	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8409	class -
cneg 8410	class -u A
df-sub 8411	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8412	|- -u A = ( 0 - A )
creap 8813	class #ℝ
df-reap 8814	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8820	class #
df-ap 8821	|- # = { <. 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 8911	class /
df-div 8912	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9202	class NN
df-inn 9203	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9253	class 2
c3 9254	class 3
c4 9255	class 4
c5 9256	class 5
c6 9257	class 6
c7 9258	class 7
c8 9259	class 8
c9 9260	class 9
df-2 9261	|- 2 = ( 1 + 1 )
df-3 9262	|- 3 = ( 2 + 1 )
df-4 9263	|- 4 = ( 3 + 1 )
df-5 9264	|- 5 = ( 4 + 1 )
df-6 9265	|- 6 = ( 5 + 1 )
df-7 9266	|- 7 = ( 6 + 1 )
df-8 9267	|- 8 = ( 7 + 1 )
df-9 9268	|- 9 = ( 8 + 1 )
cn0 9461	class NN0
df-n0 9462	|- NN0 = ( NN u. { 0 } )
cxnn0 9526	class NN0*
df-xnn0 9527	|- NN0* = ( NN0 u. { +oo } )
cz 9540	class ZZ
df-z 9541	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9672	class ; A B
df-dec 9673	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9816	class ZZ>=
df-uz 9817	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9914	class QQ
df-q 9915	|- QQ = ( / " ( ZZ X. NN ) )
crp 9949	class RR+
df-rp 9950	|- RR+ = { x e. RR | 0 < x }
cxne 10065	class -e A
cxad 10066	class +e
cxmu 10067	class xe
df-xneg 10068	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10069	|- +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 10070	|- 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 10184	class (,)
cioc 10185	class (,]
cico 10186	class [,)
cicc 10187	class [,]
df-ioo 10188	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10189	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10190	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10191	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10305	class ...
df-fz 10306	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10439	class ..^
df-fzo 10440	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10591	class |_
cceil 10592	class ⌈
df-fl 10593	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10594	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10647	class mod
df-mod 10648	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10772	class seq M ( .+ , F )
df-seqfrec 10773	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10863	class ^
df-exp 10864	|- ^ = ( 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 11050	class !
df-fac 11051	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11072	class _C
df-bc 11073	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11100	class ♯
df-ihash 11101	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11179	class Word S
df-word 11180	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11224	class lastS
df-lsw 11225	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11233	class ++
df-concat 11234	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11258	class <" A ">
df-s1 11259	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11292	class substr
df-substr 11293	|- 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 11319	class prefix
df-pfx 11320	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11396	class <" A B ">
cs3 11397	class <" A B C ">
cs4 11398	class <" A B C D ">
cs5 11399	class <" A B C D E ">
cs6 11400	class <" A B C D E F ">
cs7 11401	class <" A B C D E F G ">
cs8 11402	class <" A B C D E F G H ">
df-s2 11403	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11404	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11405	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11406	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11407	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11408	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11409	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11454	class shift
df-shft 11455	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11479	class *
cre 11480	class Re
cim 11481	class Im
df-cj 11482	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11483	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11484	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11636	class sqr
cabs 11637	class abs
df-rsqrt 11638	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11639	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11918	class ~~>
df-clim 11919	|- ~~> = { <. 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 11993	class sum_ k e. A B
df-sumdc 11994	|- 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 12191	class prod_ k e. A B
df-proddc 12192	|- 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 12283	class exp
ceu 12284	class _e
csin 12285	class sin
ccos 12286	class cos
ctan 12287	class tan
cpi 12288	class pi
df-ef 12289	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12290	|- _e = ( exp ` 1 )
df-sin 12291	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12292	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12293	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12294	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12416	class tau
df-tau 12417	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12428	class ||
df-dvds 12429	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12581	class bits
df-bits 12582	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12604	class gcd
df-gcd 12605	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12712	class lcm
df-lcm 12713	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12759	class Prime
df-prm 12760	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12833	class numer
cdenom 12834	class denom
df-numer 12835	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12836	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12860	class odZ
cphi 12861	class phi
df-odz 12862	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12863	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12937	class pCnt
df-pc 12938	|- 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 13022	class ZZ[_i]
df-gz 13023	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13158	class Struct
cnx 13159	class ndx
csts 13160	class sSet
cslot 13161	class Slot A
cbs 13162	class Base
cress 13163	class ↾s
df-struct 13164	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13165	|- ndx = ( _I |` NN )
df-slot 13166	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13168	|- Base = Slot 1
df-sets 13169	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13170	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13240	class +g
cmulr 13241	class .r
cstv 13242	class *r
csca 13243	class Scalar
cvsca 13244	class .s
cip 13245	class .i
cts 13246	class TopSet
cple 13247	class le
coc 13248	class oc
cds 13249	class dist
cunif 13250	class UnifSet
chom 13251	class Hom
cco 13252	class comp
df-plusg 13253	|- +g = Slot 2
df-mulr 13254	|- .r = Slot 3
df-starv 13255	|- *r = Slot 4
df-sca 13256	|- Scalar = Slot 5
df-vsca 13257	|- .s = Slot 6
df-ip 13258	|- .i = Slot 8
df-tset 13259	|- TopSet = Slot 9
df-ple 13260	|- le = Slot ; 1 0
df-ocomp 13261	|- oc = Slot ; 1 1
df-ds 13262	|- dist = Slot ; 1 2
df-unif 13263	|- UnifSet = Slot ; 1 3
df-hom 13264	|- Hom = Slot ; 1 4
df-cco 13265	|- comp = Slot ; 1 5
crest 13402	class ↾t
ctopn 13403	class TopOpen
df-rest 13404	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13405	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13417	class topGen
cpt 13418	class Xt_
c0g 13419	class 0g
cgsu 13420	class gsumg
df-0g 13421	|- 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 13422	|- 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 13423	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13424	|- 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 13428	class X_s
cpws 13429	class ^s
df-prds 13430	|- 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 13453	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13462	class "s
cqus 13463	class /.s
cxps 13464	class X.s
df-iimas 13465	|- "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 13466	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13467	|- 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 13516	class +f
cmgm 13517	class Mgm
df-plusf 13518	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13519	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13564	class Smgrp
df-sgrp 13565	|- 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 13579	class Mnd
df-mnd 13580	|- 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 13620	class MndHom
csubmnd 13621	class SubMnd
df-mhm 13622	|- 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 13623	|- 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 13663	class Grp
cminusg 13664	class invg
csg 13665	class -g
df-grp 13666	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13667	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13668	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13786	class .g
df-mulg 13787	|- .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 13834	class SubGrp
cnsg 13835	class NrmSGrp
cqg 13836	class ~QG
df-subg 13837	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13838	|- 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 13839	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13907	class GrpHom
df-ghm 13908	|- 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 13951	class CMnd
cabl 13952	class Abel
df-cmn 13953	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13954	|- Abel = ( Grp i^i CMnd )
cmgp 14014	class mulGrp
df-mgp 14015	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 14026	class Rng
df-rng 14027	|- 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 14053	class 1r
df-ur 14054	|- 1r = ( 0g o. mulGrp )
csrg 14057	class SRing
df-srg 14058	|- 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 14090	class Ring
ccrg 14091	class CRing
df-ring 14092	|- 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 14093	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14161	class oppr
df-oppr 14162	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14180	class ||r
cui 14181	class Unit
cir 14182	class Irred
df-dvdsr 14183	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14184	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14185	|- 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 14215	class invr
df-invr 14216	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14226	class /r
df-dvr 14227	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14245	class RingHom
crs 14246	class RingIso
df-rhm 14247	|- 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 14248	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14274	class NzRing
df-nzr 14275	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14285	class LRing
df-lring 14286	|- 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 14292	class SubRng
df-subrng 14293	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14312	class SubRing
crgspn 14313	class RingSpan
df-subrg 14314	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14315	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14350	class RLReg
cdomn 14351	class Domn
cidom 14352	class IDomn
df-rlreg 14353	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14354	|- 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 14355	|- IDomn = ( CRing i^i Domn )
capr 14376	class #r
df-apr 14377	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 14383	class LMod
cscaf 14384	class .sf
df-lmod 14385	|- 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 14386	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14448	class LSubSp
df-lssm 14449	|- 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 14482	class LSpan
df-lsp 14483	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14529	class subringAlg
crglmod 14530	class ringLMod
df-sra 14531	|- 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 14532	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14563	class LIdeal
crsp 14564	class RSpan
df-lidl 14565	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14566	|- RSpan = ( LSpan o. ringLMod )
c2idl 14595	class 2Ideal
df-2idl 14596	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14631	class PsMet
cxmet 14632	class *Met
cmet 14633	class Met
cbl 14634	class ball
cfbas 14635	class fBas
cfg 14636	class filGen
cmopn 14637	class MetOpen
cmetu 14638	class metUnif
df-psmet 14639	|- 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 14640	|- *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 14641	|- 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 14642	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14643	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14644	|- 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 14645	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14646	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14652	class ℂfld
df-cnfld 14653	|- ℂ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 14686	class ℤring
df-zring 14687	|- ℤring = (ℂfld ↾s ZZ )
czrh 14707	class ZRHom
czlm 14708	class ZMod
czn 14709	class ℤ/nℤ
df-zrh 14710	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14711	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14712	|- ℤ/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 14757	class mPwSer
cmpl 14758	class mPoly
df-psr 14759	|- 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 14760	|- 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 14808	class Top
df-top 14809	|- 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 14821	class TopOn
df-topon 14822	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14841	class TopSp
df-topsp 14842	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14853	class TopBases
df-bases 14854	|- 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 14903	class Clsd
cnt 14904	class int
ccl 14905	class cls
df-cld 14906	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14907	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14908	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14949	class nei
df-nei 14950	|- 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 14996	class Cn
ccnp 14997	class CnP
clm 14998	class ~~> t
df-cn 14999	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 15000	|- 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 15001	|- ~~> 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 15063	class tX
df-tx 15064	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15111	class Homeo
df-hmeo 15112	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15147	class *MetSp
cms 15148	class MetSp
ctms 15149	class toMetSp
df-xms 15150	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15151	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15152	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15381	class -cn->
df-cncf 15382	|- -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 15465	class lim CC
cdv 15466	class _D
df-limced 15467	|- 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 15468	|- _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 15539	class Poly
cidp 15540	class Xp
df-ply 15541	|- 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 15542	|- Xp = ( _I |` CC )
clog 15667	class log
ccxp 15668	class ^c
df-relog 15669	|- log = `' ( exp |` RR )
df-rpcxp 15670	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15754	class logb
df-logb 15755	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15795	class sigma
df-sgm 15796	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15816	class /L
df-lgs 15817	|- /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 15945	class .ef
df-edgf 15946	|- .ef = Slot ; 1 8
cvtx 15953	class Vtx
ciedg 15954	class iEdg
df-vtx 15955	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 15956	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 15998	class Edg
df-edg 15999	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 16008	class UHGraph
cushgr 16009	class USHGraph
df-uhgrm 16010	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 16011	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 16032	class UPGraph
cumgr 16033	class UMGraph
df-upgren 16034	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 16035	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16094	class USPGraph
cusgr 16095	class USGraph
df-uspgren 16096	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16097	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16194	class SubGraph
df-subgr 16195	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16227	class VtxDeg
df-vtxdg 16228	|- 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 16258	class Walks
df-wlks 16259	|- 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 16321	class Trails
df-trls 16322	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16332	class ClWWalks
df-clwwlk 16333	|- 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 16344	class ClWWalksN
df-clwwlkn 16345	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16367	class ClWWalksNOn
df-clwwlknon 16368	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16383	class EulerPaths
df-eupth 16384	|- 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 16511	wff A DECIDin B
df-dcin 16512	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16528	wff BOUNDED ph
ax-bd0 16529	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16530	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16531	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16532	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16533	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16534	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16535	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16536	|- BOUNDED x = y
ax-bdel 16537	|- BOUNDED x e. y
ax-bdsb 16538	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16556	wff BOUNDED A
df-bdc 16557	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16600	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16640	|- BOUNDED ph   =>    |- DECID ph
wind 16642	wff Ind A
df-bj-ind 16643	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16657	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16684	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16692	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16698	|- 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 16703	|- 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 16705	|- ( ( ( 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 16807	class gfsumgf
df-gfsum 16808	|- 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 16819	wff A.! x ( ph -> ps )
walsc 16820	wff A.! x e. A ph
df-alsi 16821	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 16822	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )