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 715	wff ( ph \/ ps )
ax-io 716	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 837	wff STAB ph
df-stab 838	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 841	wff DECID ph
df-dc 842	|- (DECID ph <-> ( ph \/ -. ph ) )
wif 985	wff if- ( ph , ps , ch )
df-ifp 986	|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
w3o 1003	wff ( ph \/ ps \/ ch )
w3a 1004	wff ( ph /\ ps /\ ch )
df-3or 1005	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 1006	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1395	wff A. x ph
cv 1396	class x
wceq 1397	wff A = B
wtru 1398	wff T.
df-tru 1400	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1402	wff F.
df-fal 1403	|- ( F. <-> -. T. )
wxo 1419	wff ( ph \/_ ps )
df-xor 1420	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1495	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1496	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1497	|- ph   =>    |- A. x ph
wnf 1508	wff F/ x ph
df-nf 1509	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1540	wff E. x ph
ax-ie1 1541	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1542	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1552	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1553	|- ( A. x x = y -> A. y y = x )
ax-11 1554	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1555	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1557	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1558	|- ( A. x ph -> ph )
ax-17 1574	|- ( ph -> A. x ph )
ax-i9 1578	|- E. x x = y
ax-ial 1582	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1583	|- ( ( 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 2361	wff F/_ x A
df-nfc 2363	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2402	wff A =/= B
df-ne 2403	|- ( A =/= B <-> -. A = B )
wnel 2497	wff A e/ B
df-nel 2498	|- ( A e/ B <-> -. A e. B )
wral 2510	wff A. x e. A ph
wrex 2511	wff E. x e. A ph
wreu 2512	wff E! x e. A ph
wrmo 2513	wff E* x e. A ph
crab 2514	class { x e. A | ph }
df-ral 2515	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2516	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2517	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2518	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2519	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2802	class _V
df-v 2804	|- _V = { x | x = x }
wcdeq 3014	wff CondEq ( x = y -> ph )
df-cdeq 3015	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 3031	wff [. A / x ]. ph
df-sbc 3032	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3127	class [_ A / x ]_ B
df-csb 3128	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3197	class ( A \ B )
cun 3198	class ( A u. B )
cin 3199	class ( A i^i B )
wss 3200	wff A C_ B
df-dif 3202	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3204	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3206	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3213	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3494	class (/)
df-nul 3495	|- (/) = ( _V \ _V )
cif 3605	class if ( ph , A , B )
df-if 3606	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3652	class ~P A
df-pw 3654	|- ~P A = { x | x C_ A }
csn 3669	class { A }
cpr 3670	class { A , B }
ctp 3671	class { A , B , C }
cop 3672	class <. A , B >.
cotp 3673	class <. A , B , C >.
df-sn 3675	|- { A } = { x | x = A }
df-pr 3676	|- { A , B } = ( { A } u. { B } )
df-tp 3677	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3678	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3679	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3893	class U. A
df-uni 3894	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3928	class |^| A
df-int 3929	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3970	class U_ x e. A B
ciin 3971	class |^|_ x e. A B
df-iun 3972	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3973	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4064	wff Disj x e. A B
df-disj 4065	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4088	wff A R B
df-br 4089	|- ( A R B <-> <. A , B >. e. R )
copab 4149	class { <. x , y >. | ph }
cmpt 4150	class ( x e. A |-> B )
df-opab 4151	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4152	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4187	wff Tr A
df-tr 4188	|- ( Tr A <-> U. A C_ A )
ax-coll 4204	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4207	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4215	|- E. x A. y -. y e. x
ax-pow 4264	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4284	wff EXMID
df-exmid 4285	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4299	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4384	class _E
cid 4385	class _I
df-eprel 4386	|- _E = { <. x , y >. | x e. y }
df-id 4390	|- _I = { <. x , y >. | x = y }
wpo 4391	wff R Po A
wor 4392	wff R Or A
df-po 4393	|- ( 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 4394	|- ( 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 4424	wff FrFor R A S
wfr 4425	wff R Fr A
wse 4426	wff R Se A
wwe 4427	wff R We A
df-frfor 4428	|- (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 4429	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4430	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4431	|- ( 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 4459	wff Ord A
con0 4460	class On
wlim 4461	wff Lim A
csuc 4462	class suc A
df-iord 4463	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4465	|- On = { x | Ord x }
df-ilim 4466	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4468	|- suc A = ( A u. { A } )
ax-un 4530	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4635	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4686	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4688	class om
df-iom 4689	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4723	class ( A X. B )
ccnv 4724	class `' A
cdm 4725	class dom A
crn 4726	class ran A
cres 4727	class ( A |` B )
cima 4728	class ( A " B )
ccom 4729	class ( A o. B )
wrel 4730	wff Rel A
df-xp 4731	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4732	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4733	|- `' A = { <. x , y >. | y A x }
df-co 4734	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4735	|- dom A = { x | E. y x A y }
df-rn 4736	|- ran A = dom `' A
df-res 4737	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4738	|- ( A " B ) = ran ( A |` B )
cio 5284	class ( iota x ph )
df-iota 5286	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5320	wff Fun A
wfn 5321	wff A Fn B
wf 5322	wff F : A --> B
wf1 5323	wff F : A -1-1-> B
wfo 5324	wff F : A -onto-> B
wf1o 5325	wff F : A -1-1-onto-> B
cfv 5326	class ( F ` A )
wiso 5327	wff H Isom R , S ( A , B )
df-fun 5328	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5329	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5330	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5331	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5332	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5333	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5334	|- ( F ` A ) = ( iota x A F x )
df-isom 5335	|- ( 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 5973	class ( iota_ x e. A ph )
df-riota 5974	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6021	class ( A F B )
coprab 6022	class { <. <. x , y >. , z >. | ph }
cmpo 6023	class ( x e. A , y e. B |-> C )
df-ov 6024	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6025	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6026	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6236	class oF R
cofr 6237	class oR R
df-of 6238	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6239	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6304	class 1st
c2nd 6305	class 2nd
df-1st 6306	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6307	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6413	class tpos F
df-tpos 6414	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6454	wff Smo A
df-smo 6455	|- ( 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 6473	class recs ( F )
df-recs 6474	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6538	class rec ( F , I )
df-irdg 6539	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6559	class frec ( F , I )
df-frec 6560	|- 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 6578	class 1o
c2o 6579	class 2o
c3o 6580	class 3o
c4o 6581	class 4o
coa 6582	class +o
comu 6583	class .o
coei 6584	class ↑o
df-1o 6585	|- 1o = suc (/)
df-2o 6586	|- 2o = suc 1o
df-3o 6587	|- 3o = suc 2o
df-4o 6588	|- 4o = suc 3o
df-oadd 6589	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6590	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6591	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6702	wff R Er A
cec 6703	class [ A ] R
cqs 6704	class ( A /. R )
df-er 6705	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6707	|- [ A ] R = ( R " { A } )
df-qs 6711	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6820	class ^m
cpm 6821	class ^pm
df-map 6822	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6823	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6870	class X_ x e. A B
df-ixp 6871	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6910	class ~~
cdom 6911	class ~<_
cfn 6912	class Fin
df-en 6913	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6914	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6915	|- Fin = { x | E. y e. om x ~~ y }
cfi 7170	class fi
df-fi 7171	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7184	class sup ( A , B , R )
cinf 7185	class inf ( A , B , R )
df-sup 7186	|- 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 7187	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7239	class ( A ⊔ B )
df-dju 7240	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7247	class inl
cinr 7248	class inr
df-inl 7249	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7250	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7285	class case ( R , S )
df-case 7286	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7304	class ( R ⊔d S )
df-djud 7305	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7321	class ℕ∞
df-nninf 7322	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7336	class Omni
df-omni 7337	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7353	class Markov
df-markov 7354	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7365	class WOmni
df-womni 7366	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7384	class card
wacn 7385	class AC A
df-card 7386	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7387	|- 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 7423	wff CHOICE
df-ac 7424	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7469	wff R Ap A
df-pap 7470	|- ( 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 7471	wff R TAp A
df-tap 7472	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7484	wff CCHOICE
df-cc 7485	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7495	class N.
cpli 7496	class +N
cmi 7497	class .N
clti 7498	class <N
cplpq 7499	class +pQ
cmpq 7500	class .pQ
cltpq 7501	class <pQ
ceq 7502	class ~Q
cnq 7503	class Q.
c1q 7504	class 1Q
cplq 7505	class +Q
cmq 7506	class .Q
crq 7507	class *Q
cltq 7508	class <Q
ceq0 7509	class ~Q0
cnq0 7510	class Q0
c0q0 7511	class 0Q0
cplq0 7512	class +Q0
cmq0 7513	class ·Q0
cnp 7514	class P.
c1p 7515	class 1P
cpp 7516	class +P.
cmp 7517	class .P.
cltp 7518	class <P
cer 7519	class ~R
cnr 7520	class R.
c0r 7521	class 0R
c1r 7522	class 1R
cm1r 7523	class -1R
cplr 7524	class +R
cmr 7525	class .R
cltr 7526	class <R
df-ni 7527	|- N. = ( om \ { (/) } )
df-pli 7528	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7529	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7530	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7567	|- +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 7568	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7569	|- <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 7570	|- ~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 7571	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7572	|- +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 7573	|- .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 7574	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7575	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7576	|- <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 7647	|- ~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 7648	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7649	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7650	|- +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 7651	|- ·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 7689	|- 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 7690	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7691	|- +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 7692	|- .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 7693	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7949	|- ~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 7950	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7951	|- +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 7952	|- .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 7953	|- <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 7954	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7955	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7956	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8033	class CC
cr 8034	class RR
cc0 8035	class 0
c1 8036	class 1
ci 8037	class _i
caddc 8038	class +
cltrr 8039	class <RR
cmul 8040	class x.
df-c 8041	|- CC = ( R. X. R. )
df-0 8042	|- 0 = <. 0R , 0R >.
df-1 8043	|- 1 = <. 1R , 0R >.
df-i 8044	|- _i = <. 0R , 1R >.
df-r 8045	|- RR = ( R. X. { 0R } )
df-add 8046	|- + = { <. <. 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 8047	|- 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 8048	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8126	|- CC e. _V
ax-resscn 8127	|- RR C_ CC
ax-1cn 8128	|- 1 e. CC
ax-1re 8129	|- 1 e. RR
ax-icn 8130	|- _i e. CC
ax-addcl 8131	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8132	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8133	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8134	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8135	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8136	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8137	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8138	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8139	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8140	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8141	|- 0 <RR 1
ax-1rid 8142	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8143	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8144	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8145	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8146	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8147	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8148	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8149	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8150	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8151	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8152	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8153	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8154	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8155	|- 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 8156	|- ( ( ( 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 8157	|- + : ( CC X. CC ) --> CC
ax-mulf 8158	|- x. : ( CC X. CC ) --> CC
cpnf 8214	class +oo
cmnf 8215	class -oo
cxr 8216	class RR*
clt 8217	class <
cle 8218	class <_
df-pnf 8219	|- +oo = ~P U. CC
df-mnf 8220	|- -oo = ~P +oo
df-xr 8221	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8222	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8223	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8353	class -
cneg 8354	class -u A
df-sub 8355	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8356	|- -u A = ( 0 - A )
creap 8757	class #ℝ
df-reap 8758	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8764	class #
df-ap 8765	|- # = { <. 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 8855	class /
df-div 8856	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9146	class NN
df-inn 9147	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9197	class 2
c3 9198	class 3
c4 9199	class 4
c5 9200	class 5
c6 9201	class 6
c7 9202	class 7
c8 9203	class 8
c9 9204	class 9
df-2 9205	|- 2 = ( 1 + 1 )
df-3 9206	|- 3 = ( 2 + 1 )
df-4 9207	|- 4 = ( 3 + 1 )
df-5 9208	|- 5 = ( 4 + 1 )
df-6 9209	|- 6 = ( 5 + 1 )
df-7 9210	|- 7 = ( 6 + 1 )
df-8 9211	|- 8 = ( 7 + 1 )
df-9 9212	|- 9 = ( 8 + 1 )
cn0 9405	class NN0
df-n0 9406	|- NN0 = ( NN u. { 0 } )
cxnn0 9468	class NN0*
df-xnn0 9469	|- NN0* = ( NN0 u. { +oo } )
cz 9482	class ZZ
df-z 9483	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9614	class ; A B
df-dec 9615	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9758	class ZZ>=
df-uz 9759	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9856	class QQ
df-q 9857	|- QQ = ( / " ( ZZ X. NN ) )
crp 9891	class RR+
df-rp 9892	|- RR+ = { x e. RR | 0 < x }
cxne 10007	class -e A
cxad 10008	class +e
cxmu 10009	class xe
df-xneg 10010	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 10011	|- +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 10012	|- 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 10126	class (,)
cioc 10127	class (,]
cico 10128	class [,)
cicc 10129	class [,]
df-ioo 10130	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10131	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10132	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10133	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10246	class ...
df-fz 10247	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10380	class ..^
df-fzo 10381	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10532	class |_
cceil 10533	class ⌈
df-fl 10534	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10535	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10588	class mod
df-mod 10589	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10713	class seq M ( .+ , F )
df-seqfrec 10714	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10804	class ^
df-exp 10805	|- ^ = ( 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 10991	class !
df-fac 10992	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 11013	class _C
df-bc 11014	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11041	class ♯
df-ihash 11042	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11120	class Word S
df-word 11121	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11165	class lastS
df-lsw 11166	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11174	class ++
df-concat 11175	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11199	class <" A ">
df-s1 11200	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11233	class substr
df-substr 11234	|- 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 11260	class prefix
df-pfx 11261	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11337	class <" A B ">
cs3 11338	class <" A B C ">
cs4 11339	class <" A B C D ">
cs5 11340	class <" A B C D E ">
cs6 11341	class <" A B C D E F ">
cs7 11342	class <" A B C D E F G ">
cs8 11343	class <" A B C D E F G H ">
df-s2 11344	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11345	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11346	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11347	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11348	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11349	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11350	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11395	class shift
df-shft 11396	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11420	class *
cre 11421	class Re
cim 11422	class Im
df-cj 11423	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11424	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11425	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11577	class sqr
cabs 11578	class abs
df-rsqrt 11579	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11580	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11859	class ~~>
df-clim 11860	|- ~~> = { <. 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 11934	class sum_ k e. A B
df-sumdc 11935	|- 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 12132	class prod_ k e. A B
df-proddc 12133	|- 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 12224	class exp
ceu 12225	class _e
csin 12226	class sin
ccos 12227	class cos
ctan 12228	class tan
cpi 12229	class pi
df-ef 12230	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12231	|- _e = ( exp ` 1 )
df-sin 12232	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12233	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12234	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12235	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12357	class tau
df-tau 12358	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12369	class ||
df-dvds 12370	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12522	class bits
df-bits 12523	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12545	class gcd
df-gcd 12546	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12653	class lcm
df-lcm 12654	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12700	class Prime
df-prm 12701	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12774	class numer
cdenom 12775	class denom
df-numer 12776	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12777	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12801	class odZ
cphi 12802	class phi
df-odz 12803	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12804	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12878	class pCnt
df-pc 12879	|- 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 12963	class ZZ[_i]
df-gz 12964	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13099	class Struct
cnx 13100	class ndx
csts 13101	class sSet
cslot 13102	class Slot A
cbs 13103	class Base
cress 13104	class ↾s
df-struct 13105	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13106	|- ndx = ( _I |` NN )
df-slot 13107	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13109	|- Base = Slot 1
df-sets 13110	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13111	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13181	class +g
cmulr 13182	class .r
cstv 13183	class *r
csca 13184	class Scalar
cvsca 13185	class .s
cip 13186	class .i
cts 13187	class TopSet
cple 13188	class le
coc 13189	class oc
cds 13190	class dist
cunif 13191	class UnifSet
chom 13192	class Hom
cco 13193	class comp
df-plusg 13194	|- +g = Slot 2
df-mulr 13195	|- .r = Slot 3
df-starv 13196	|- *r = Slot 4
df-sca 13197	|- Scalar = Slot 5
df-vsca 13198	|- .s = Slot 6
df-ip 13199	|- .i = Slot 8
df-tset 13200	|- TopSet = Slot 9
df-ple 13201	|- le = Slot ; 1 0
df-ocomp 13202	|- oc = Slot ; 1 1
df-ds 13203	|- dist = Slot ; 1 2
df-unif 13204	|- UnifSet = Slot ; 1 3
df-hom 13205	|- Hom = Slot ; 1 4
df-cco 13206	|- comp = Slot ; 1 5
crest 13343	class ↾t
ctopn 13344	class TopOpen
df-rest 13345	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13346	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13358	class topGen
cpt 13359	class Xt_
c0g 13360	class 0g
cgsu 13361	class gsumg
df-0g 13362	|- 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 13363	|- 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 13364	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13365	|- 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 13369	class X_s
cpws 13370	class ^s
df-prds 13371	|- 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 13394	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13403	class "s
cqus 13404	class /.s
cxps 13405	class X.s
df-iimas 13406	|- "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 13407	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13408	|- 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 13457	class +f
cmgm 13458	class Mgm
df-plusf 13459	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13460	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13505	class Smgrp
df-sgrp 13506	|- 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 13520	class Mnd
df-mnd 13521	|- 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 13561	class MndHom
csubmnd 13562	class SubMnd
df-mhm 13563	|- 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 13564	|- 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 13604	class Grp
cminusg 13605	class invg
csg 13606	class -g
df-grp 13607	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13608	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13609	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13727	class .g
df-mulg 13728	|- .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 13775	class SubGrp
cnsg 13776	class NrmSGrp
cqg 13777	class ~QG
df-subg 13778	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13779	|- 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 13780	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13848	class GrpHom
df-ghm 13849	|- 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 13892	class CMnd
cabl 13893	class Abel
df-cmn 13894	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13895	|- Abel = ( Grp i^i CMnd )
cmgp 13955	class mulGrp
df-mgp 13956	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 13967	class Rng
df-rng 13968	|- 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 13994	class 1r
df-ur 13995	|- 1r = ( 0g o. mulGrp )
csrg 13998	class SRing
df-srg 13999	|- 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 14031	class Ring
ccrg 14032	class CRing
df-ring 14033	|- 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 14034	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14102	class oppr
df-oppr 14103	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14121	class ||r
cui 14122	class Unit
cir 14123	class Irred
df-dvdsr 14124	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14125	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14126	|- 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 14156	class invr
df-invr 14157	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14167	class /r
df-dvr 14168	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14186	class RingHom
crs 14187	class RingIso
df-rhm 14188	|- 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 14189	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14215	class NzRing
df-nzr 14216	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14226	class LRing
df-lring 14227	|- 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 14233	class SubRng
df-subrng 14234	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14253	class SubRing
crgspn 14254	class RingSpan
df-subrg 14255	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14256	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14291	class RLReg
cdomn 14292	class Domn
cidom 14293	class IDomn
df-rlreg 14294	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14295	|- 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 14296	|- IDomn = ( CRing i^i Domn )
capr 14316	class #r
df-apr 14317	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 14323	class LMod
cscaf 14324	class .sf
df-lmod 14325	|- 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 14326	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14388	class LSubSp
df-lssm 14389	|- 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 14422	class LSpan
df-lsp 14423	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14469	class subringAlg
crglmod 14470	class ringLMod
df-sra 14471	|- 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 14472	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14503	class LIdeal
crsp 14504	class RSpan
df-lidl 14505	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14506	|- RSpan = ( LSpan o. ringLMod )
c2idl 14535	class 2Ideal
df-2idl 14536	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14571	class PsMet
cxmet 14572	class *Met
cmet 14573	class Met
cbl 14574	class ball
cfbas 14575	class fBas
cfg 14576	class filGen
cmopn 14577	class MetOpen
cmetu 14578	class metUnif
df-psmet 14579	|- 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 14580	|- *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 14581	|- 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 14582	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14583	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14584	|- 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 14585	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14586	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14592	class ℂfld
df-cnfld 14593	|- ℂ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 14626	class ℤring
df-zring 14627	|- ℤring = (ℂfld ↾s ZZ )
czrh 14647	class ZRHom
czlm 14648	class ZMod
czn 14649	class ℤ/nℤ
df-zrh 14650	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14651	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14652	|- ℤ/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 14697	class mPwSer
cmpl 14698	class mPoly
df-psr 14699	|- 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 14700	|- 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 14748	class Top
df-top 14749	|- 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 14761	class TopOn
df-topon 14762	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14781	class TopSp
df-topsp 14782	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14793	class TopBases
df-bases 14794	|- 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 14843	class Clsd
cnt 14844	class int
ccl 14845	class cls
df-cld 14846	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14847	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14848	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14889	class nei
df-nei 14890	|- 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 14936	class Cn
ccnp 14937	class CnP
clm 14938	class ~~> t
df-cn 14939	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 14940	|- 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 14941	|- ~~> 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 15003	class tX
df-tx 15004	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15051	class Homeo
df-hmeo 15052	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15087	class *MetSp
cms 15088	class MetSp
ctms 15089	class toMetSp
df-xms 15090	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15091	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15092	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15321	class -cn->
df-cncf 15322	|- -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 15405	class lim CC
cdv 15406	class _D
df-limced 15407	|- 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 15408	|- _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 15479	class Poly
cidp 15480	class Xp
df-ply 15481	|- 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 15482	|- Xp = ( _I |` CC )
clog 15607	class log
ccxp 15608	class ^c
df-relog 15609	|- log = `' ( exp |` RR )
df-rpcxp 15610	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15694	class logb
df-logb 15695	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15732	class sigma
df-sgm 15733	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15753	class /L
df-lgs 15754	|- /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 15882	class .ef
df-edgf 15883	|- .ef = Slot ; 1 8
cvtx 15890	class Vtx
ciedg 15891	class iEdg
df-vtx 15892	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 15893	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 15935	class Edg
df-edg 15936	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 15945	class UHGraph
cushgr 15946	class USHGraph
df-uhgrm 15947	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 15948	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 15969	class UPGraph
cumgr 15970	class UMGraph
df-upgren 15971	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 15972	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 16031	class USPGraph
cusgr 16032	class USGraph
df-uspgren 16033	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 16034	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
csubgr 16131	class SubGraph
df-subgr 16132	|- SubGraph = { <. s , g >. | ( (Vtx ` s ) C_ (Vtx ` g ) /\ (iEdg ` s ) = ( (iEdg ` g ) |` dom (iEdg ` s ) ) /\ (Edg ` s ) C_ ~P (Vtx ` s ) ) }
cvtxdg 16164	class VtxDeg
df-vtxdg 16165	|- 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 16195	class Walks
df-wlks 16196	|- 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 16258	class Trails
df-trls 16259	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16269	class ClWWalks
df-clwwlk 16270	|- 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 16281	class ClWWalksN
df-clwwlkn 16282	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16304	class ClWWalksNOn
df-clwwlknon 16305	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
ceupth 16320	class EulerPaths
df-eupth 16321	|- 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 16448	wff A DECIDin B
df-dcin 16449	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16466	wff BOUNDED ph
ax-bd0 16467	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16468	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16469	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16470	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16471	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16472	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16473	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16474	|- BOUNDED x = y
ax-bdel 16475	|- BOUNDED x e. y
ax-bdsb 16476	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16494	wff BOUNDED A
df-bdc 16495	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16538	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16578	|- BOUNDED ph   =>    |- DECID ph
wind 16580	wff Ind A
df-bj-ind 16581	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16595	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16622	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16630	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16636	|- 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 16641	|- 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 16643	|- ( ( ( 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 16738	class gfsumgf
df-gfsum 16739	|- 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 16750	wff A.! x ( ph -> ps )
walsc 16751	wff A.! x e. A ph
df-alsi 16752	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 16753	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )