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 3887	class U. A
df-uni 3888	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3922	class |^| A
df-int 3923	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3964	class U_ x e. A B
ciin 3965	class |^|_ x e. A B
df-iun 3966	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3967	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4058	wff Disj x e. A B
df-disj 4059	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4082	wff A R B
df-br 4083	|- ( A R B <-> <. A , B >. e. R )
copab 4143	class { <. x , y >. | ph }
cmpt 4144	class ( x e. A |-> B )
df-opab 4145	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4146	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4181	wff Tr A
df-tr 4182	|- ( Tr A <-> U. A C_ A )
ax-coll 4198	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4201	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4209	|- E. x A. y -. y e. x
ax-pow 4257	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4277	wff EXMID
df-exmid 4278	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4292	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4375	class _E
cid 4376	class _I
df-eprel 4377	|- _E = { <. x , y >. | x e. y }
df-id 4381	|- _I = { <. x , y >. | x = y }
wpo 4382	wff R Po A
wor 4383	wff R Or A
df-po 4384	|- ( 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 4385	|- ( 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 4415	wff FrFor R A S
wfr 4416	wff R Fr A
wse 4417	wff R Se A
wwe 4418	wff R We A
df-frfor 4419	|- (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 4420	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4421	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4422	|- ( 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 4450	wff Ord A
con0 4451	class On
wlim 4452	wff Lim A
csuc 4453	class suc A
df-iord 4454	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4456	|- On = { x | Ord x }
df-ilim 4457	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4459	|- suc A = ( A u. { A } )
ax-un 4521	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4626	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4677	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4679	class om
df-iom 4680	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4714	class ( A X. B )
ccnv 4715	class `' A
cdm 4716	class dom A
crn 4717	class ran A
cres 4718	class ( A |` B )
cima 4719	class ( A " B )
ccom 4720	class ( A o. B )
wrel 4721	wff Rel A
df-xp 4722	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4723	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4724	|- `' A = { <. x , y >. | y A x }
df-co 4725	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4726	|- dom A = { x | E. y x A y }
df-rn 4727	|- ran A = dom `' A
df-res 4728	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4729	|- ( A " B ) = ran ( A |` B )
cio 5272	class ( iota x ph )
df-iota 5274	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5308	wff Fun A
wfn 5309	wff A Fn B
wf 5310	wff F : A --> B
wf1 5311	wff F : A -1-1-> B
wfo 5312	wff F : A -onto-> B
wf1o 5313	wff F : A -1-1-onto-> B
cfv 5314	class ( F ` A )
wiso 5315	wff H Isom R , S ( A , B )
df-fun 5316	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5317	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5318	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5319	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5320	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5321	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5322	|- ( F ` A ) = ( iota x A F x )
df-isom 5323	|- ( 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 5946	class ( iota_ x e. A ph )
df-riota 5947	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 5994	class ( A F B )
coprab 5995	class { <. <. x , y >. , z >. | ph }
cmpo 5996	class ( x e. A , y e. B |-> C )
df-ov 5997	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 5998	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 5999	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6206	class oF R
cofr 6207	class oR R
df-of 6208	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6209	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6274	class 1st
c2nd 6275	class 2nd
df-1st 6276	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6277	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6380	class tpos F
df-tpos 6381	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6421	wff Smo A
df-smo 6422	|- ( 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 6440	class recs ( F )
df-recs 6441	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6505	class rec ( F , I )
df-irdg 6506	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6526	class frec ( F , I )
df-frec 6527	|- 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 6545	class 1o
c2o 6546	class 2o
c3o 6547	class 3o
c4o 6548	class 4o
coa 6549	class +o
comu 6550	class .o
coei 6551	class ↑o
df-1o 6552	|- 1o = suc (/)
df-2o 6553	|- 2o = suc 1o
df-3o 6554	|- 3o = suc 2o
df-4o 6555	|- 4o = suc 3o
df-oadd 6556	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6557	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6558	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6667	wff R Er A
cec 6668	class [ A ] R
cqs 6669	class ( A /. R )
df-er 6670	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6672	|- [ A ] R = ( R " { A } )
df-qs 6676	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6785	class ^m
cpm 6786	class ^pm
df-map 6787	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6788	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6835	class X_ x e. A B
df-ixp 6836	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6875	class ~~
cdom 6876	class ~<_
cfn 6877	class Fin
df-en 6878	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6879	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6880	|- Fin = { x | E. y e. om x ~~ y }
cfi 7123	class fi
df-fi 7124	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7137	class sup ( A , B , R )
cinf 7138	class inf ( A , B , R )
df-sup 7139	|- 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 7140	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7192	class ( A ⊔ B )
df-dju 7193	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7200	class inl
cinr 7201	class inr
df-inl 7202	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7203	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7238	class case ( R , S )
df-case 7239	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7257	class ( R ⊔d S )
df-djud 7258	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7274	class ℕ∞
df-nninf 7275	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7289	class Omni
df-omni 7290	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7306	class Markov
df-markov 7307	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7318	class WOmni
df-womni 7319	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7337	class card
wacn 7338	class AC A
df-card 7339	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7340	|- 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 7375	wff CHOICE
df-ac 7376	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7421	wff R Ap A
df-pap 7422	|- ( 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 7423	wff R TAp A
df-tap 7424	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7436	wff CCHOICE
df-cc 7437	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7447	class N.
cpli 7448	class +N
cmi 7449	class .N
clti 7450	class <N
cplpq 7451	class +pQ
cmpq 7452	class .pQ
cltpq 7453	class <pQ
ceq 7454	class ~Q
cnq 7455	class Q.
c1q 7456	class 1Q
cplq 7457	class +Q
cmq 7458	class .Q
crq 7459	class *Q
cltq 7460	class <Q
ceq0 7461	class ~Q0
cnq0 7462	class Q0
c0q0 7463	class 0Q0
cplq0 7464	class +Q0
cmq0 7465	class ·Q0
cnp 7466	class P.
c1p 7467	class 1P
cpp 7468	class +P.
cmp 7469	class .P.
cltp 7470	class <P
cer 7471	class ~R
cnr 7472	class R.
c0r 7473	class 0R
c1r 7474	class 1R
cm1r 7475	class -1R
cplr 7476	class +R
cmr 7477	class .R
cltr 7478	class <R
df-ni 7479	|- N. = ( om \ { (/) } )
df-pli 7480	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7481	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7482	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7519	|- +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 7520	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7521	|- <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 7522	|- ~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 7523	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7524	|- +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 7525	|- .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 7526	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7527	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7528	|- <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 7599	|- ~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 7600	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7601	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7602	|- +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 7603	|- ·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 7641	|- 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 7642	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7643	|- +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 7644	|- .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 7645	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7901	|- ~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 7902	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7903	|- +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 7904	|- .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 7905	|- <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 7906	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7907	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7908	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 7985	class CC
cr 7986	class RR
cc0 7987	class 0
c1 7988	class 1
ci 7989	class _i
caddc 7990	class +
cltrr 7991	class <RR
cmul 7992	class x.
df-c 7993	|- CC = ( R. X. R. )
df-0 7994	|- 0 = <. 0R , 0R >.
df-1 7995	|- 1 = <. 1R , 0R >.
df-i 7996	|- _i = <. 0R , 1R >.
df-r 7997	|- RR = ( R. X. { 0R } )
df-add 7998	|- + = { <. <. 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 7999	|- 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 8000	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8078	|- CC e. _V
ax-resscn 8079	|- RR C_ CC
ax-1cn 8080	|- 1 e. CC
ax-1re 8081	|- 1 e. RR
ax-icn 8082	|- _i e. CC
ax-addcl 8083	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8084	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8085	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8086	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8087	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8088	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8089	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8090	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8091	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8092	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8093	|- 0 <RR 1
ax-1rid 8094	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8095	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8096	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8097	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8098	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8099	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8100	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8101	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8102	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8103	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8104	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8105	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8106	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8107	|- 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 8108	|- ( ( ( 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 8109	|- + : ( CC X. CC ) --> CC
ax-mulf 8110	|- x. : ( CC X. CC ) --> CC
cpnf 8166	class +oo
cmnf 8167	class -oo
cxr 8168	class RR*
clt 8169	class <
cle 8170	class <_
df-pnf 8171	|- +oo = ~P U. CC
df-mnf 8172	|- -oo = ~P +oo
df-xr 8173	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8174	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8175	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8305	class -
cneg 8306	class -u A
df-sub 8307	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8308	|- -u A = ( 0 - A )
creap 8709	class #ℝ
df-reap 8710	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8716	class #
df-ap 8717	|- # = { <. 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 8807	class /
df-div 8808	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9098	class NN
df-inn 9099	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9149	class 2
c3 9150	class 3
c4 9151	class 4
c5 9152	class 5
c6 9153	class 6
c7 9154	class 7
c8 9155	class 8
c9 9156	class 9
df-2 9157	|- 2 = ( 1 + 1 )
df-3 9158	|- 3 = ( 2 + 1 )
df-4 9159	|- 4 = ( 3 + 1 )
df-5 9160	|- 5 = ( 4 + 1 )
df-6 9161	|- 6 = ( 5 + 1 )
df-7 9162	|- 7 = ( 6 + 1 )
df-8 9163	|- 8 = ( 7 + 1 )
df-9 9164	|- 9 = ( 8 + 1 )
cn0 9357	class NN0
df-n0 9358	|- NN0 = ( NN u. { 0 } )
cxnn0 9420	class NN0*
df-xnn0 9421	|- NN0* = ( NN0 u. { +oo } )
cz 9434	class ZZ
df-z 9435	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9566	class ; A B
df-dec 9567	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9710	class ZZ>=
df-uz 9711	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9802	class QQ
df-q 9803	|- QQ = ( / " ( ZZ X. NN ) )
crp 9837	class RR+
df-rp 9838	|- RR+ = { x e. RR | 0 < x }
cxne 9953	class -e A
cxad 9954	class +e
cxmu 9955	class xe
df-xneg 9956	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9957	|- +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 9958	|- 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 10072	class (,)
cioc 10073	class (,]
cico 10074	class [,)
cicc 10075	class [,]
df-ioo 10076	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10077	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10078	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10079	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10192	class ...
df-fz 10193	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10326	class ..^
df-fzo 10327	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10475	class |_
cceil 10476	class ⌈
df-fl 10477	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10478	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10531	class mod
df-mod 10532	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10656	class seq M ( .+ , F )
df-seqfrec 10657	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10747	class ^
df-exp 10748	|- ^ = ( 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 10934	class !
df-fac 10935	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10956	class _C
df-bc 10957	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 10984	class ♯
df-ihash 10985	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11058	class Word S
df-word 11059	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11102	class lastS
df-lsw 11103	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11111	class ++
df-concat 11112	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11134	class <" A ">
df-s1 11135	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11163	class substr
df-substr 11164	|- 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 11190	class prefix
df-pfx 11191	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11267	class <" A B ">
cs3 11268	class <" A B C ">
cs4 11269	class <" A B C D ">
cs5 11270	class <" A B C D E ">
cs6 11271	class <" A B C D E F ">
cs7 11272	class <" A B C D E F G ">
cs8 11273	class <" A B C D E F G H ">
df-s2 11274	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11275	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11276	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11277	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11278	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11279	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11280	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11311	class shift
df-shft 11312	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11336	class *
cre 11337	class Re
cim 11338	class Im
df-cj 11339	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11340	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11341	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11493	class sqr
cabs 11494	class abs
df-rsqrt 11495	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11496	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11775	class ~~>
df-clim 11776	|- ~~> = { <. 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 11850	class sum_ k e. A B
df-sumdc 11851	|- 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 12047	class prod_ k e. A B
df-proddc 12048	|- 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 12139	class exp
ceu 12140	class _e
csin 12141	class sin
ccos 12142	class cos
ctan 12143	class tan
cpi 12144	class pi
df-ef 12145	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12146	|- _e = ( exp ` 1 )
df-sin 12147	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12148	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12149	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12150	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12272	class tau
df-tau 12273	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12284	class ||
df-dvds 12285	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12437	class bits
df-bits 12438	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12460	class gcd
df-gcd 12461	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12568	class lcm
df-lcm 12569	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12615	class Prime
df-prm 12616	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12689	class numer
cdenom 12690	class denom
df-numer 12691	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12692	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12716	class odZ
cphi 12717	class phi
df-odz 12718	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12719	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12793	class pCnt
df-pc 12794	|- 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 12878	class ZZ[_i]
df-gz 12879	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13014	class Struct
cnx 13015	class ndx
csts 13016	class sSet
cslot 13017	class Slot A
cbs 13018	class Base
cress 13019	class ↾s
df-struct 13020	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13021	|- ndx = ( _I |` NN )
df-slot 13022	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13024	|- Base = Slot 1
df-sets 13025	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13026	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13096	class +g
cmulr 13097	class .r
cstv 13098	class *r
csca 13099	class Scalar
cvsca 13100	class .s
cip 13101	class .i
cts 13102	class TopSet
cple 13103	class le
coc 13104	class oc
cds 13105	class dist
cunif 13106	class UnifSet
chom 13107	class Hom
cco 13108	class comp
df-plusg 13109	|- +g = Slot 2
df-mulr 13110	|- .r = Slot 3
df-starv 13111	|- *r = Slot 4
df-sca 13112	|- Scalar = Slot 5
df-vsca 13113	|- .s = Slot 6
df-ip 13114	|- .i = Slot 8
df-tset 13115	|- TopSet = Slot 9
df-ple 13116	|- le = Slot ; 1 0
df-ocomp 13117	|- oc = Slot ; 1 1
df-ds 13118	|- dist = Slot ; 1 2
df-unif 13119	|- UnifSet = Slot ; 1 3
df-hom 13120	|- Hom = Slot ; 1 4
df-cco 13121	|- comp = Slot ; 1 5
crest 13258	class ↾t
ctopn 13259	class TopOpen
df-rest 13260	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13261	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13273	class topGen
cpt 13274	class Xt_
c0g 13275	class 0g
cgsu 13276	class gsumg
df-0g 13277	|- 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 13278	|- 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 13279	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13280	|- 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 13284	class X_s
cpws 13285	class ^s
df-prds 13286	|- 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 13309	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13318	class "s
cqus 13319	class /.s
cxps 13320	class X.s
df-iimas 13321	|- "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 13322	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13323	|- 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 13372	class +f
cmgm 13373	class Mgm
df-plusf 13374	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13375	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13420	class Smgrp
df-sgrp 13421	|- 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 13435	class Mnd
df-mnd 13436	|- 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 13476	class MndHom
csubmnd 13477	class SubMnd
df-mhm 13478	|- 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 13479	|- 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 13519	class Grp
cminusg 13520	class invg
csg 13521	class -g
df-grp 13522	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13523	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13524	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13642	class .g
df-mulg 13643	|- .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 13690	class SubGrp
cnsg 13691	class NrmSGrp
cqg 13692	class ~QG
df-subg 13693	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13694	|- 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 13695	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13763	class GrpHom
df-ghm 13764	|- 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 13807	class CMnd
cabl 13808	class Abel
df-cmn 13809	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13810	|- Abel = ( Grp i^i CMnd )
cmgp 13869	class mulGrp
df-mgp 13870	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 13881	class Rng
df-rng 13882	|- 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 13908	class 1r
df-ur 13909	|- 1r = ( 0g o. mulGrp )
csrg 13912	class SRing
df-srg 13913	|- 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 13945	class Ring
ccrg 13946	class CRing
df-ring 13947	|- 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 13948	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14016	class oppr
df-oppr 14017	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14035	class ||r
cui 14036	class Unit
cir 14037	class Irred
df-dvdsr 14038	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14039	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14040	|- 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 14069	class invr
df-invr 14070	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14080	class /r
df-dvr 14081	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14099	class RingHom
crs 14100	class RingIso
df-rhm 14101	|- 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 14102	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14128	class NzRing
df-nzr 14129	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14139	class LRing
df-lring 14140	|- 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 14146	class SubRng
df-subrng 14147	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14166	class SubRing
crgspn 14167	class RingSpan
df-subrg 14168	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14169	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14204	class RLReg
cdomn 14205	class Domn
cidom 14206	class IDomn
df-rlreg 14207	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14208	|- 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 14209	|- IDomn = ( CRing i^i Domn )
capr 14229	class #r
df-apr 14230	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 14236	class LMod
cscaf 14237	class .sf
df-lmod 14238	|- 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 14239	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14301	class LSubSp
df-lssm 14302	|- 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 14335	class LSpan
df-lsp 14336	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14382	class subringAlg
crglmod 14383	class ringLMod
df-sra 14384	|- 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 14385	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14416	class LIdeal
crsp 14417	class RSpan
df-lidl 14418	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14419	|- RSpan = ( LSpan o. ringLMod )
c2idl 14448	class 2Ideal
df-2idl 14449	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14484	class PsMet
cxmet 14485	class *Met
cmet 14486	class Met
cbl 14487	class ball
cfbas 14488	class fBas
cfg 14489	class filGen
cmopn 14490	class MetOpen
cmetu 14491	class metUnif
df-psmet 14492	|- 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 14493	|- *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 14494	|- 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 14495	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14496	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14497	|- 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 14498	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14499	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14505	class ℂfld
df-cnfld 14506	|- ℂ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 14539	class ℤring
df-zring 14540	|- ℤring = (ℂfld ↾s ZZ )
czrh 14560	class ZRHom
czlm 14561	class ZMod
czn 14562	class ℤ/nℤ
df-zrh 14563	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14564	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14565	|- ℤ/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 14610	class mPwSer
cmpl 14611	class mPoly
df-psr 14612	|- 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 14613	|- 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 14656	class Top
df-top 14657	|- 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 14669	class TopOn
df-topon 14670	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14689	class TopSp
df-topsp 14690	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14701	class TopBases
df-bases 14702	|- 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 14751	class Clsd
cnt 14752	class int
ccl 14753	class cls
df-cld 14754	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14755	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14756	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14797	class nei
df-nei 14798	|- 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 14844	class Cn
ccnp 14845	class CnP
clm 14846	class ~~> t
df-cn 14847	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 14848	|- 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 14849	|- ~~> 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 14911	class tX
df-tx 14912	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 14959	class Homeo
df-hmeo 14960	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 14995	class *MetSp
cms 14996	class MetSp
ctms 14997	class toMetSp
df-xms 14998	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 14999	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15000	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15229	class -cn->
df-cncf 15230	|- -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 15313	class lim CC
cdv 15314	class _D
df-limced 15315	|- 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 15316	|- _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 15387	class Poly
cidp 15388	class Xp
df-ply 15389	|- 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 15390	|- Xp = ( _I |` CC )
clog 15515	class log
ccxp 15516	class ^c
df-relog 15517	|- log = `' ( exp |` RR )
df-rpcxp 15518	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15602	class logb
df-logb 15603	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15640	class sigma
df-sgm 15641	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15661	class /L
df-lgs 15662	|- /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 15790	class .ef
df-edgf 15791	|- .ef = Slot ; 1 8
cvtx 15798	class Vtx
ciedg 15799	class iEdg
df-vtx 15800	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 15801	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 15843	class Edg
df-edg 15844	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 15852	class UHGraph
cushgr 15853	class USHGraph
df-uhgrm 15854	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 15855	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 15876	class UPGraph
cumgr 15877	class UMGraph
df-upgren 15878	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 15879	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 15936	class USPGraph
cusgr 15937	class USGraph
df-uspgren 15938	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 15939	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 16087	wff A DECIDin B
df-dcin 16088	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16105	wff BOUNDED ph
ax-bd0 16106	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16107	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16108	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16109	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16110	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16111	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16112	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16113	|- BOUNDED x = y
ax-bdel 16114	|- BOUNDED x e. y
ax-bdsb 16115	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16133	wff BOUNDED A
df-bdc 16134	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16177	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16217	|- BOUNDED ph   =>    |- DECID ph
wind 16219	wff Ind A
df-bj-ind 16220	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16234	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16261	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16269	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16275	|- 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 16280	|- 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 16282	|- ( ( ( 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 16375	wff A.! x ( ph -> ps )
walsc 16376	wff A.! x e. A ph
df-alsi 16377	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 16378	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )