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 617	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 618	|- ( -. ph -> ( ph -> ps ) )
wo 713	wff ( ph \/ ps )
ax-io 714	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 835	wff STAB ph
df-stab 836	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 839	wff DECID ph
df-dc 840	|- (DECID ph <-> ( ph \/ -. ph ) )
wif 983	wff if- ( ph , ps , ch )
df-ifp 984	|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
w3o 1001	wff ( ph \/ ps \/ ch )
w3a 1002	wff ( ph /\ ps /\ ch )
df-3or 1003	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 1004	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1393	wff A. x ph
cv 1394	class x
wceq 1395	wff A = B
wtru 1396	wff T.
df-tru 1398	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1400	wff F.
df-fal 1401	|- ( F. <-> -. T. )
wxo 1417	wff ( ph \/_ ps )
df-xor 1418	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1493	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1494	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1495	|- ph   =>    |- A. x ph
wnf 1506	wff F/ x ph
df-nf 1507	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1538	wff E. x ph
ax-ie1 1539	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1540	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1550	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1551	|- ( A. x x = y -> A. y y = x )
ax-11 1552	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1553	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1555	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1556	|- ( A. x ph -> ph )
ax-17 1572	|- ( ph -> A. x ph )
ax-i9 1576	|- E. x x = y
ax-ial 1580	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1581	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1762	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1808	wff [ y / x ] ph
df-sb 1809	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1860	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1869	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2077	wff E! x ph
wmo 2078	wff E* x ph
df-eu 2080	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2081	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2200	wff A e. B
ax-13 2202	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2203	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2211	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2215	class { x | ph }
df-clab 2216	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2222	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2225	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2359	wff F/_ x A
df-nfc 2361	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2400	wff A =/= B
df-ne 2401	|- ( A =/= B <-> -. A = B )
wnel 2495	wff A e/ B
df-nel 2496	|- ( A e/ B <-> -. A e. B )
wral 2508	wff A. x e. A ph
wrex 2509	wff E. x e. A ph
wreu 2510	wff E! x e. A ph
wrmo 2511	wff E* x e. A ph
crab 2512	class { x e. A | ph }
df-ral 2513	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2514	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2515	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2516	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2517	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2799	class _V
df-v 2801	|- _V = { x | x = x }
wcdeq 3011	wff CondEq ( x = y -> ph )
df-cdeq 3012	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 3028	wff [. A / x ]. ph
df-sbc 3029	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3124	class [_ A / x ]_ B
df-csb 3125	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3194	class ( A \ B )
cun 3195	class ( A u. B )
cin 3196	class ( A i^i B )
wss 3197	wff A C_ B
df-dif 3199	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3201	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3203	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3210	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3491	class (/)
df-nul 3492	|- (/) = ( _V \ _V )
cif 3602	class if ( ph , A , B )
df-if 3603	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3649	class ~P A
df-pw 3651	|- ~P A = { x | x C_ A }
csn 3666	class { A }
cpr 3667	class { A , B }
ctp 3668	class { A , B , C }
cop 3669	class <. A , B >.
cotp 3670	class <. A , B , C >.
df-sn 3672	|- { A } = { x | x = A }
df-pr 3673	|- { A , B } = ( { A } u. { B } )
df-tp 3674	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3675	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3676	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3888	class U. A
df-uni 3889	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3923	class |^| A
df-int 3924	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3965	class U_ x e. A B
ciin 3966	class |^|_ x e. A B
df-iun 3967	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3968	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4059	wff Disj x e. A B
df-disj 4060	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4083	wff A R B
df-br 4084	|- ( A R B <-> <. A , B >. e. R )
copab 4144	class { <. x , y >. | ph }
cmpt 4145	class ( x e. A |-> B )
df-opab 4146	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4147	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4182	wff Tr A
df-tr 4183	|- ( Tr A <-> U. A C_ A )
ax-coll 4199	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4202	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4210	|- E. x A. y -. y e. x
ax-pow 4258	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4278	wff EXMID
df-exmid 4279	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4293	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4378	class _E
cid 4379	class _I
df-eprel 4380	|- _E = { <. x , y >. | x e. y }
df-id 4384	|- _I = { <. x , y >. | x = y }
wpo 4385	wff R Po A
wor 4386	wff R Or A
df-po 4387	|- ( 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 4388	|- ( 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 4418	wff FrFor R A S
wfr 4419	wff R Fr A
wse 4420	wff R Se A
wwe 4421	wff R We A
df-frfor 4422	|- (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 4423	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4424	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4425	|- ( 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 4453	wff Ord A
con0 4454	class On
wlim 4455	wff Lim A
csuc 4456	class suc A
df-iord 4457	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4459	|- On = { x | Ord x }
df-ilim 4460	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4462	|- suc A = ( A u. { A } )
ax-un 4524	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4629	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4680	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4682	class om
df-iom 4683	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4717	class ( A X. B )
ccnv 4718	class `' A
cdm 4719	class dom A
crn 4720	class ran A
cres 4721	class ( A |` B )
cima 4722	class ( A " B )
ccom 4723	class ( A o. B )
wrel 4724	wff Rel A
df-xp 4725	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4726	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4727	|- `' A = { <. x , y >. | y A x }
df-co 4728	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4729	|- dom A = { x | E. y x A y }
df-rn 4730	|- ran A = dom `' A
df-res 4731	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4732	|- ( A " B ) = ran ( A |` B )
cio 5276	class ( iota x ph )
df-iota 5278	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5312	wff Fun A
wfn 5313	wff A Fn B
wf 5314	wff F : A --> B
wf1 5315	wff F : A -1-1-> B
wfo 5316	wff F : A -onto-> B
wf1o 5317	wff F : A -1-1-onto-> B
cfv 5318	class ( F ` A )
wiso 5319	wff H Isom R , S ( A , B )
df-fun 5320	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5321	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5322	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5323	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5324	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5325	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5326	|- ( F ` A ) = ( iota x A F x )
df-isom 5327	|- ( 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 5959	class ( iota_ x e. A ph )
df-riota 5960	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6007	class ( A F B )
coprab 6008	class { <. <. x , y >. , z >. | ph }
cmpo 6009	class ( x e. A , y e. B |-> C )
df-ov 6010	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6011	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6012	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6222	class oF R
cofr 6223	class oR R
df-of 6224	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6225	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6290	class 1st
c2nd 6291	class 2nd
df-1st 6292	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6293	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6396	class tpos F
df-tpos 6397	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6437	wff Smo A
df-smo 6438	|- ( 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 6456	class recs ( F )
df-recs 6457	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6521	class rec ( F , I )
df-irdg 6522	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6542	class frec ( F , I )
df-frec 6543	|- 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 6561	class 1o
c2o 6562	class 2o
c3o 6563	class 3o
c4o 6564	class 4o
coa 6565	class +o
comu 6566	class .o
coei 6567	class ↑o
df-1o 6568	|- 1o = suc (/)
df-2o 6569	|- 2o = suc 1o
df-3o 6570	|- 3o = suc 2o
df-4o 6571	|- 4o = suc 3o
df-oadd 6572	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6573	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6574	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6685	wff R Er A
cec 6686	class [ A ] R
cqs 6687	class ( A /. R )
df-er 6688	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6690	|- [ A ] R = ( R " { A } )
df-qs 6694	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6803	class ^m
cpm 6804	class ^pm
df-map 6805	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6806	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6853	class X_ x e. A B
df-ixp 6854	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6893	class ~~
cdom 6894	class ~<_
cfn 6895	class Fin
df-en 6896	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6897	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6898	|- Fin = { x | E. y e. om x ~~ y }
cfi 7143	class fi
df-fi 7144	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7157	class sup ( A , B , R )
cinf 7158	class inf ( A , B , R )
df-sup 7159	|- 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 7160	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7212	class ( A ⊔ B )
df-dju 7213	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7220	class inl
cinr 7221	class inr
df-inl 7222	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7223	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7258	class case ( R , S )
df-case 7259	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7277	class ( R ⊔d S )
df-djud 7278	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7294	class ℕ∞
df-nninf 7295	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7309	class Omni
df-omni 7310	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7326	class Markov
df-markov 7327	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7338	class WOmni
df-womni 7339	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7357	class card
wacn 7358	class AC A
df-card 7359	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7360	|- 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 7395	wff CHOICE
df-ac 7396	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7441	wff R Ap A
df-pap 7442	|- ( 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 7443	wff R TAp A
df-tap 7444	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7456	wff CCHOICE
df-cc 7457	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7467	class N.
cpli 7468	class +N
cmi 7469	class .N
clti 7470	class <N
cplpq 7471	class +pQ
cmpq 7472	class .pQ
cltpq 7473	class <pQ
ceq 7474	class ~Q
cnq 7475	class Q.
c1q 7476	class 1Q
cplq 7477	class +Q
cmq 7478	class .Q
crq 7479	class *Q
cltq 7480	class <Q
ceq0 7481	class ~Q0
cnq0 7482	class Q0
c0q0 7483	class 0Q0
cplq0 7484	class +Q0
cmq0 7485	class ·Q0
cnp 7486	class P.
c1p 7487	class 1P
cpp 7488	class +P.
cmp 7489	class .P.
cltp 7490	class <P
cer 7491	class ~R
cnr 7492	class R.
c0r 7493	class 0R
c1r 7494	class 1R
cm1r 7495	class -1R
cplr 7496	class +R
cmr 7497	class .R
cltr 7498	class <R
df-ni 7499	|- N. = ( om \ { (/) } )
df-pli 7500	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7501	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7502	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7539	|- +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 7540	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7541	|- <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 7542	|- ~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 7543	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7544	|- +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 7545	|- .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 7546	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7547	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7548	|- <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 7619	|- ~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 7620	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7621	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7622	|- +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 7623	|- ·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 7661	|- 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 7662	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7663	|- +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 7664	|- .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 7665	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7921	|- ~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 7922	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7923	|- +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 7924	|- .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 7925	|- <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 7926	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7927	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7928	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8005	class CC
cr 8006	class RR
cc0 8007	class 0
c1 8008	class 1
ci 8009	class _i
caddc 8010	class +
cltrr 8011	class <RR
cmul 8012	class x.
df-c 8013	|- CC = ( R. X. R. )
df-0 8014	|- 0 = <. 0R , 0R >.
df-1 8015	|- 1 = <. 1R , 0R >.
df-i 8016	|- _i = <. 0R , 1R >.
df-r 8017	|- RR = ( R. X. { 0R } )
df-add 8018	|- + = { <. <. 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 8019	|- 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 8020	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8098	|- CC e. _V
ax-resscn 8099	|- RR C_ CC
ax-1cn 8100	|- 1 e. CC
ax-1re 8101	|- 1 e. RR
ax-icn 8102	|- _i e. CC
ax-addcl 8103	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8104	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8105	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8106	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8107	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8108	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8109	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8110	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8111	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8112	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8113	|- 0 <RR 1
ax-1rid 8114	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8115	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8116	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8117	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8118	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8119	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8120	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8121	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8122	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8123	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8124	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8125	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8126	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8127	|- 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 8128	|- ( ( ( 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 8129	|- + : ( CC X. CC ) --> CC
ax-mulf 8130	|- x. : ( CC X. CC ) --> CC
cpnf 8186	class +oo
cmnf 8187	class -oo
cxr 8188	class RR*
clt 8189	class <
cle 8190	class <_
df-pnf 8191	|- +oo = ~P U. CC
df-mnf 8192	|- -oo = ~P +oo
df-xr 8193	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8194	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8195	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8325	class -
cneg 8326	class -u A
df-sub 8327	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8328	|- -u A = ( 0 - A )
creap 8729	class #ℝ
df-reap 8730	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8736	class #
df-ap 8737	|- # = { <. 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 8827	class /
df-div 8828	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9118	class NN
df-inn 9119	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9169	class 2
c3 9170	class 3
c4 9171	class 4
c5 9172	class 5
c6 9173	class 6
c7 9174	class 7
c8 9175	class 8
c9 9176	class 9
df-2 9177	|- 2 = ( 1 + 1 )
df-3 9178	|- 3 = ( 2 + 1 )
df-4 9179	|- 4 = ( 3 + 1 )
df-5 9180	|- 5 = ( 4 + 1 )
df-6 9181	|- 6 = ( 5 + 1 )
df-7 9182	|- 7 = ( 6 + 1 )
df-8 9183	|- 8 = ( 7 + 1 )
df-9 9184	|- 9 = ( 8 + 1 )
cn0 9377	class NN0
df-n0 9378	|- NN0 = ( NN u. { 0 } )
cxnn0 9440	class NN0*
df-xnn0 9441	|- NN0* = ( NN0 u. { +oo } )
cz 9454	class ZZ
df-z 9455	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9586	class ; A B
df-dec 9587	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9730	class ZZ>=
df-uz 9731	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9822	class QQ
df-q 9823	|- QQ = ( / " ( ZZ X. NN ) )
crp 9857	class RR+
df-rp 9858	|- RR+ = { x e. RR | 0 < x }
cxne 9973	class -e A
cxad 9974	class +e
cxmu 9975	class xe
df-xneg 9976	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9977	|- +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 9978	|- 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 10092	class (,)
cioc 10093	class (,]
cico 10094	class [,)
cicc 10095	class [,]
df-ioo 10096	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10097	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10098	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10099	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10212	class ...
df-fz 10213	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10346	class ..^
df-fzo 10347	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10496	class |_
cceil 10497	class ⌈
df-fl 10498	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10499	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10552	class mod
df-mod 10553	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10677	class seq M ( .+ , F )
df-seqfrec 10678	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10768	class ^
df-exp 10769	|- ^ = ( 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 10955	class !
df-fac 10956	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10977	class _C
df-bc 10978	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11005	class ♯
df-ihash 11006	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11079	class Word S
df-word 11080	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11124	class lastS
df-lsw 11125	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11133	class ++
df-concat 11134	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11156	class <" A ">
df-s1 11157	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11185	class substr
df-substr 11186	|- 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 11212	class prefix
df-pfx 11213	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11289	class <" A B ">
cs3 11290	class <" A B C ">
cs4 11291	class <" A B C D ">
cs5 11292	class <" A B C D E ">
cs6 11293	class <" A B C D E F ">
cs7 11294	class <" A B C D E F G ">
cs8 11295	class <" A B C D E F G H ">
df-s2 11296	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11297	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11298	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11299	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11300	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11301	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11302	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11333	class shift
df-shft 11334	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11358	class *
cre 11359	class Re
cim 11360	class Im
df-cj 11361	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11362	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11363	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11515	class sqr
cabs 11516	class abs
df-rsqrt 11517	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11518	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11797	class ~~>
df-clim 11798	|- ~~> = { <. 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 11872	class sum_ k e. A B
df-sumdc 11873	|- 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 12069	class prod_ k e. A B
df-proddc 12070	|- 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 12161	class exp
ceu 12162	class _e
csin 12163	class sin
ccos 12164	class cos
ctan 12165	class tan
cpi 12166	class pi
df-ef 12167	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12168	|- _e = ( exp ` 1 )
df-sin 12169	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12170	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12171	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12172	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12294	class tau
df-tau 12295	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12306	class ||
df-dvds 12307	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12459	class bits
df-bits 12460	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12482	class gcd
df-gcd 12483	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12590	class lcm
df-lcm 12591	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12637	class Prime
df-prm 12638	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12711	class numer
cdenom 12712	class denom
df-numer 12713	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12714	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12738	class odZ
cphi 12739	class phi
df-odz 12740	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12741	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12815	class pCnt
df-pc 12816	|- 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 12900	class ZZ[_i]
df-gz 12901	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13036	class Struct
cnx 13037	class ndx
csts 13038	class sSet
cslot 13039	class Slot A
cbs 13040	class Base
cress 13041	class ↾s
df-struct 13042	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13043	|- ndx = ( _I |` NN )
df-slot 13044	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13046	|- Base = Slot 1
df-sets 13047	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13048	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13118	class +g
cmulr 13119	class .r
cstv 13120	class *r
csca 13121	class Scalar
cvsca 13122	class .s
cip 13123	class .i
cts 13124	class TopSet
cple 13125	class le
coc 13126	class oc
cds 13127	class dist
cunif 13128	class UnifSet
chom 13129	class Hom
cco 13130	class comp
df-plusg 13131	|- +g = Slot 2
df-mulr 13132	|- .r = Slot 3
df-starv 13133	|- *r = Slot 4
df-sca 13134	|- Scalar = Slot 5
df-vsca 13135	|- .s = Slot 6
df-ip 13136	|- .i = Slot 8
df-tset 13137	|- TopSet = Slot 9
df-ple 13138	|- le = Slot ; 1 0
df-ocomp 13139	|- oc = Slot ; 1 1
df-ds 13140	|- dist = Slot ; 1 2
df-unif 13141	|- UnifSet = Slot ; 1 3
df-hom 13142	|- Hom = Slot ; 1 4
df-cco 13143	|- comp = Slot ; 1 5
crest 13280	class ↾t
ctopn 13281	class TopOpen
df-rest 13282	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13283	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13295	class topGen
cpt 13296	class Xt_
c0g 13297	class 0g
cgsu 13298	class gsumg
df-0g 13299	|- 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 13300	|- 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 13301	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13302	|- 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 13306	class X_s
cpws 13307	class ^s
df-prds 13308	|- 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 13331	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13340	class "s
cqus 13341	class /.s
cxps 13342	class X.s
df-iimas 13343	|- "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 13344	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13345	|- 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 13394	class +f
cmgm 13395	class Mgm
df-plusf 13396	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13397	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13442	class Smgrp
df-sgrp 13443	|- 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 13457	class Mnd
df-mnd 13458	|- 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 13498	class MndHom
csubmnd 13499	class SubMnd
df-mhm 13500	|- 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 13501	|- 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 13541	class Grp
cminusg 13542	class invg
csg 13543	class -g
df-grp 13544	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13545	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13546	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13664	class .g
df-mulg 13665	|- .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 13712	class SubGrp
cnsg 13713	class NrmSGrp
cqg 13714	class ~QG
df-subg 13715	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13716	|- 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 13717	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13785	class GrpHom
df-ghm 13786	|- 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 13829	class CMnd
cabl 13830	class Abel
df-cmn 13831	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13832	|- Abel = ( Grp i^i CMnd )
cmgp 13891	class mulGrp
df-mgp 13892	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 13903	class Rng
df-rng 13904	|- 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 13930	class 1r
df-ur 13931	|- 1r = ( 0g o. mulGrp )
csrg 13934	class SRing
df-srg 13935	|- 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 13967	class Ring
ccrg 13968	class CRing
df-ring 13969	|- 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 13970	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14038	class oppr
df-oppr 14039	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14057	class ||r
cui 14058	class Unit
cir 14059	class Irred
df-dvdsr 14060	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14061	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14062	|- 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 14092	class invr
df-invr 14093	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14103	class /r
df-dvr 14104	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14122	class RingHom
crs 14123	class RingIso
df-rhm 14124	|- 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 14125	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14151	class NzRing
df-nzr 14152	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14162	class LRing
df-lring 14163	|- 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 14169	class SubRng
df-subrng 14170	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14189	class SubRing
crgspn 14190	class RingSpan
df-subrg 14191	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14192	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14227	class RLReg
cdomn 14228	class Domn
cidom 14229	class IDomn
df-rlreg 14230	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14231	|- 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 14232	|- IDomn = ( CRing i^i Domn )
capr 14252	class #r
df-apr 14253	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 14259	class LMod
cscaf 14260	class .sf
df-lmod 14261	|- 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 14262	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14324	class LSubSp
df-lssm 14325	|- 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 14358	class LSpan
df-lsp 14359	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14405	class subringAlg
crglmod 14406	class ringLMod
df-sra 14407	|- 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 14408	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14439	class LIdeal
crsp 14440	class RSpan
df-lidl 14441	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14442	|- RSpan = ( LSpan o. ringLMod )
c2idl 14471	class 2Ideal
df-2idl 14472	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14507	class PsMet
cxmet 14508	class *Met
cmet 14509	class Met
cbl 14510	class ball
cfbas 14511	class fBas
cfg 14512	class filGen
cmopn 14513	class MetOpen
cmetu 14514	class metUnif
df-psmet 14515	|- 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 14516	|- *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 14517	|- 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 14518	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14519	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14520	|- 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 14521	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14522	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14528	class ℂfld
df-cnfld 14529	|- ℂ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 14562	class ℤring
df-zring 14563	|- ℤring = (ℂfld ↾s ZZ )
czrh 14583	class ZRHom
czlm 14584	class ZMod
czn 14585	class ℤ/nℤ
df-zrh 14586	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14587	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14588	|- ℤ/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 14633	class mPwSer
cmpl 14634	class mPoly
df-psr 14635	|- 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 14636	|- 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 14679	class Top
df-top 14680	|- 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 14692	class TopOn
df-topon 14693	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14712	class TopSp
df-topsp 14713	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14724	class TopBases
df-bases 14725	|- 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 14774	class Clsd
cnt 14775	class int
ccl 14776	class cls
df-cld 14777	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14778	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14779	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14820	class nei
df-nei 14821	|- 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 14867	class Cn
ccnp 14868	class CnP
clm 14869	class ~~> t
df-cn 14870	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 14871	|- 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 14872	|- ~~> 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 14934	class tX
df-tx 14935	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 14982	class Homeo
df-hmeo 14983	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15018	class *MetSp
cms 15019	class MetSp
ctms 15020	class toMetSp
df-xms 15021	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15022	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15023	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15252	class -cn->
df-cncf 15253	|- -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 15336	class lim CC
cdv 15337	class _D
df-limced 15338	|- 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 15339	|- _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 15410	class Poly
cidp 15411	class Xp
df-ply 15412	|- 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 15413	|- Xp = ( _I |` CC )
clog 15538	class log
ccxp 15539	class ^c
df-relog 15540	|- log = `' ( exp |` RR )
df-rpcxp 15541	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15625	class logb
df-logb 15626	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15663	class sigma
df-sgm 15664	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15684	class /L
df-lgs 15685	|- /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 15813	class .ef
df-edgf 15814	|- .ef = Slot ; 1 8
cvtx 15821	class Vtx
ciedg 15822	class iEdg
df-vtx 15823	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 15824	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 15866	class Edg
df-edg 15867	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 15875	class UHGraph
cushgr 15876	class USHGraph
df-uhgrm 15877	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 15878	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 15899	class UPGraph
cumgr 15900	class UMGraph
df-upgren 15901	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 15902	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 15959	class USPGraph
cusgr 15960	class USGraph
df-uspgren 15961	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 15962	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
cwlks 16038	class Walks
df-wlks 16039	|- 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 16099	class Trails
df-trls 16100	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 16181	wff A DECIDin B
df-dcin 16182	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16199	wff BOUNDED ph
ax-bd0 16200	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16201	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16202	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16203	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16204	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16205	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16206	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16207	|- BOUNDED x = y
ax-bdel 16208	|- BOUNDED x e. y
ax-bdsb 16209	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16227	wff BOUNDED A
df-bdc 16228	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16271	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16311	|- BOUNDED ph   =>    |- DECID ph
wind 16313	wff Ind A
df-bj-ind 16314	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16328	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16355	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16363	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16369	|- 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 16374	|- 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 16376	|- ( ( ( A C_ RR /\ E. x x e. A ) /\ E. x e. RR A. y e. A y < x /\ A. x e. RR A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) ) -> E. x e. RR ( A. y e. A y <_ x /\ ( ( B e. R /\ A. y e. A y <_ B ) -> x <_ B ) ) )
walsi 16474	wff A.! x ( ph -> ps )
walsc 16475	wff A.! x e. A ph
df-alsi 16476	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 16477	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )