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 615	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 616	|- ( -. ph -> ( ph -> ps ) )
wo 709	wff ( ph \/ ps )
ax-io 710	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 831	wff STAB ph
df-stab 832	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 835	wff DECID ph
df-dc 836	|- (DECID ph <-> ( ph \/ -. ph ) )
w3o 979	wff ( ph \/ ps \/ ch )
w3a 980	wff ( ph /\ ps /\ ch )
df-3or 981	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 982	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1362	wff A. x ph
cv 1363	class x
wceq 1364	wff A = B
wtru 1365	wff T.
df-tru 1367	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1369	wff F.
df-fal 1370	|- ( F. <-> -. T. )
wxo 1386	wff ( ph \/_ ps )
df-xor 1387	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1461	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1462	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1463	|- ph   =>    |- A. x ph
wnf 1474	wff F/ x ph
df-nf 1475	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1506	wff E. x ph
ax-ie1 1507	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1508	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1518	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1519	|- ( A. x x = y -> A. y y = x )
ax-11 1520	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1521	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1523	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1524	|- ( A. x ph -> ph )
ax-17 1540	|- ( ph -> A. x ph )
ax-i9 1544	|- E. x x = y
ax-ial 1548	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1549	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1730	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1776	wff [ y / x ] ph
df-sb 1777	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1828	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1837	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2045	wff E! x ph
wmo 2046	wff E* x ph
df-eu 2048	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2049	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2167	wff A e. B
ax-13 2169	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2170	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2178	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2182	class { x | ph }
df-clab 2183	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2189	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2192	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2326	wff F/_ x A
df-nfc 2328	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2367	wff A =/= B
df-ne 2368	|- ( A =/= B <-> -. A = B )
wnel 2462	wff A e/ B
df-nel 2463	|- ( A e/ B <-> -. A e. B )
wral 2475	wff A. x e. A ph
wrex 2476	wff E. x e. A ph
wreu 2477	wff E! x e. A ph
wrmo 2478	wff E* x e. A ph
crab 2479	class { x e. A | ph }
df-ral 2480	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2481	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2482	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2483	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2484	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2763	class _V
df-v 2765	|- _V = { x | x = x }
wcdeq 2972	wff CondEq ( x = y -> ph )
df-cdeq 2973	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 2989	wff [. A / x ]. ph
df-sbc 2990	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3084	class [_ A / x ]_ B
df-csb 3085	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3154	class ( A \ B )
cun 3155	class ( A u. B )
cin 3156	class ( A i^i B )
wss 3157	wff A C_ B
df-dif 3159	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3161	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3163	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3170	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3451	class (/)
df-nul 3452	|- (/) = ( _V \ _V )
cif 3562	class if ( ph , A , B )
df-if 3563	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3606	class ~P A
df-pw 3608	|- ~P A = { x | x C_ A }
csn 3623	class { A }
cpr 3624	class { A , B }
ctp 3625	class { A , B , C }
cop 3626	class <. A , B >.
cotp 3627	class <. A , B , C >.
df-sn 3629	|- { A } = { x | x = A }
df-pr 3630	|- { A , B } = ( { A } u. { B } )
df-tp 3631	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3632	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3633	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3840	class U. A
df-uni 3841	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3875	class |^| A
df-int 3876	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3917	class U_ x e. A B
ciin 3918	class |^|_ x e. A B
df-iun 3919	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3920	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4011	wff Disj x e. A B
df-disj 4012	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4034	wff A R B
df-br 4035	|- ( A R B <-> <. A , B >. e. R )
copab 4094	class { <. x , y >. | ph }
cmpt 4095	class ( x e. A |-> B )
df-opab 4096	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4097	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4132	wff Tr A
df-tr 4133	|- ( Tr A <-> U. A C_ A )
ax-coll 4149	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4152	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4160	|- E. x A. y -. y e. x
ax-pow 4208	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4228	wff EXMID
df-exmid 4229	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4243	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4323	class _E
cid 4324	class _I
df-eprel 4325	|- _E = { <. x , y >. | x e. y }
df-id 4329	|- _I = { <. x , y >. | x = y }
wpo 4330	wff R Po A
wor 4331	wff R Or A
df-po 4332	|- ( 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 4333	|- ( 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 4363	wff FrFor R A S
wfr 4364	wff R Fr A
wse 4365	wff R Se A
wwe 4366	wff R We A
df-frfor 4367	|- (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 4368	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4369	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4370	|- ( 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 4398	wff Ord A
con0 4399	class On
wlim 4400	wff Lim A
csuc 4401	class suc A
df-iord 4402	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4404	|- On = { x | Ord x }
df-ilim 4405	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4407	|- suc A = ( A u. { A } )
ax-un 4469	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4574	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4625	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4627	class om
df-iom 4628	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4662	class ( A X. B )
ccnv 4663	class `' A
cdm 4664	class dom A
crn 4665	class ran A
cres 4666	class ( A |` B )
cima 4667	class ( A " B )
ccom 4668	class ( A o. B )
wrel 4669	wff Rel A
df-xp 4670	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4671	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4672	|- `' A = { <. x , y >. | y A x }
df-co 4673	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4674	|- dom A = { x | E. y x A y }
df-rn 4675	|- ran A = dom `' A
df-res 4676	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4677	|- ( A " B ) = ran ( A |` B )
cio 5218	class ( iota x ph )
df-iota 5220	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5253	wff Fun A
wfn 5254	wff A Fn B
wf 5255	wff F : A --> B
wf1 5256	wff F : A -1-1-> B
wfo 5257	wff F : A -onto-> B
wf1o 5258	wff F : A -1-1-onto-> B
cfv 5259	class ( F ` A )
wiso 5260	wff H Isom R , S ( A , B )
df-fun 5261	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5262	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5263	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5264	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5265	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5266	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5267	|- ( F ` A ) = ( iota x A F x )
df-isom 5268	|- ( 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 5879	class ( iota_ x e. A ph )
df-riota 5880	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 5925	class ( A F B )
coprab 5926	class { <. <. x , y >. , z >. | ph }
cmpo 5927	class ( x e. A , y e. B |-> C )
df-ov 5928	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 5929	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 5930	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6137	class oF R
cofr 6138	class oR R
df-of 6139	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6140	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6205	class 1st
c2nd 6206	class 2nd
df-1st 6207	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6208	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6311	class tpos F
df-tpos 6312	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6352	wff Smo A
df-smo 6353	|- ( 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 6371	class recs ( F )
df-recs 6372	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6436	class rec ( F , I )
df-irdg 6437	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6457	class frec ( F , I )
df-frec 6458	|- 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 6476	class 1o
c2o 6477	class 2o
c3o 6478	class 3o
c4o 6479	class 4o
coa 6480	class +o
comu 6481	class .o
coei 6482	class ↑o
df-1o 6483	|- 1o = suc (/)
df-2o 6484	|- 2o = suc 1o
df-3o 6485	|- 3o = suc 2o
df-4o 6486	|- 4o = suc 3o
df-oadd 6487	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6488	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6489	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6598	wff R Er A
cec 6599	class [ A ] R
cqs 6600	class ( A /. R )
df-er 6601	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6603	|- [ A ] R = ( R " { A } )
df-qs 6607	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6716	class ^m
cpm 6717	class ^pm
df-map 6718	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6719	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6766	class X_ x e. A B
df-ixp 6767	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6806	class ~~
cdom 6807	class ~<_
cfn 6808	class Fin
df-en 6809	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6810	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6811	|- Fin = { x | E. y e. om x ~~ y }
cfi 7043	class fi
df-fi 7044	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7057	class sup ( A , B , R )
cinf 7058	class inf ( A , B , R )
df-sup 7059	|- 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 7060	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7112	class ( A ⊔ B )
df-dju 7113	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7120	class inl
cinr 7121	class inr
df-inl 7122	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7123	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7158	class case ( R , S )
df-case 7159	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7177	class ( R ⊔d S )
df-djud 7178	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7194	class ℕ∞
df-nninf 7195	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7209	class Omni
df-omni 7210	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7226	class Markov
df-markov 7227	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7238	class WOmni
df-womni 7239	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7257	class card
wacn 7258	class AC A
df-card 7259	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7260	|- 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 7290	wff CHOICE
df-ac 7291	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7332	wff R Ap A
df-pap 7333	|- ( 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 7334	wff R TAp A
df-tap 7335	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7347	wff CCHOICE
df-cc 7348	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7358	class N.
cpli 7359	class +N
cmi 7360	class .N
clti 7361	class <N
cplpq 7362	class +pQ
cmpq 7363	class .pQ
cltpq 7364	class <pQ
ceq 7365	class ~Q
cnq 7366	class Q.
c1q 7367	class 1Q
cplq 7368	class +Q
cmq 7369	class .Q
crq 7370	class *Q
cltq 7371	class <Q
ceq0 7372	class ~Q0
cnq0 7373	class Q0
c0q0 7374	class 0Q0
cplq0 7375	class +Q0
cmq0 7376	class ·Q0
cnp 7377	class P.
c1p 7378	class 1P
cpp 7379	class +P.
cmp 7380	class .P.
cltp 7381	class <P
cer 7382	class ~R
cnr 7383	class R.
c0r 7384	class 0R
c1r 7385	class 1R
cm1r 7386	class -1R
cplr 7387	class +R
cmr 7388	class .R
cltr 7389	class <R
df-ni 7390	|- N. = ( om \ { (/) } )
df-pli 7391	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7392	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7393	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7430	|- +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 7431	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7432	|- <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 7433	|- ~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 7434	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7435	|- +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 7436	|- .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 7437	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7438	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7439	|- <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 7510	|- ~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 7511	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7512	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7513	|- +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 7514	|- ·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 7552	|- 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 7553	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7554	|- +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 7555	|- .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 7556	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7812	|- ~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 7813	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7814	|- +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 7815	|- .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 7816	|- <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 7817	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7818	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7819	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 7896	class CC
cr 7897	class RR
cc0 7898	class 0
c1 7899	class 1
ci 7900	class _i
caddc 7901	class +
cltrr 7902	class <RR
cmul 7903	class x.
df-c 7904	|- CC = ( R. X. R. )
df-0 7905	|- 0 = <. 0R , 0R >.
df-1 7906	|- 1 = <. 1R , 0R >.
df-i 7907	|- _i = <. 0R , 1R >.
df-r 7908	|- RR = ( R. X. { 0R } )
df-add 7909	|- + = { <. <. 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 7910	|- 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 7911	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 7989	|- CC e. _V
ax-resscn 7990	|- RR C_ CC
ax-1cn 7991	|- 1 e. CC
ax-1re 7992	|- 1 e. RR
ax-icn 7993	|- _i e. CC
ax-addcl 7994	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 7995	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 7996	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 7997	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 7998	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 7999	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8000	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8001	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8002	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8003	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8004	|- 0 <RR 1
ax-1rid 8005	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8006	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8007	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8008	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8009	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8010	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8011	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8012	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8013	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8014	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8015	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8016	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8017	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8018	|- 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 8019	|- ( ( ( 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 8020	|- + : ( CC X. CC ) --> CC
ax-mulf 8021	|- x. : ( CC X. CC ) --> CC
cpnf 8077	class +oo
cmnf 8078	class -oo
cxr 8079	class RR*
clt 8080	class <
cle 8081	class <_
df-pnf 8082	|- +oo = ~P U. CC
df-mnf 8083	|- -oo = ~P +oo
df-xr 8084	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8085	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8086	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8216	class -
cneg 8217	class -u A
df-sub 8218	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8219	|- -u A = ( 0 - A )
creap 8620	class #ℝ
df-reap 8621	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8627	class #
df-ap 8628	|- # = { <. 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 8718	class /
df-div 8719	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9009	class NN
df-inn 9010	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9060	class 2
c3 9061	class 3
c4 9062	class 4
c5 9063	class 5
c6 9064	class 6
c7 9065	class 7
c8 9066	class 8
c9 9067	class 9
df-2 9068	|- 2 = ( 1 + 1 )
df-3 9069	|- 3 = ( 2 + 1 )
df-4 9070	|- 4 = ( 3 + 1 )
df-5 9071	|- 5 = ( 4 + 1 )
df-6 9072	|- 6 = ( 5 + 1 )
df-7 9073	|- 7 = ( 6 + 1 )
df-8 9074	|- 8 = ( 7 + 1 )
df-9 9075	|- 9 = ( 8 + 1 )
cn0 9268	class NN0
df-n0 9269	|- NN0 = ( NN u. { 0 } )
cxnn0 9331	class NN0*
df-xnn0 9332	|- NN0* = ( NN0 u. { +oo } )
cz 9345	class ZZ
df-z 9346	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9476	class ; A B
df-dec 9477	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9620	class ZZ>=
df-uz 9621	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9712	class QQ
df-q 9713	|- QQ = ( / " ( ZZ X. NN ) )
crp 9747	class RR+
df-rp 9748	|- RR+ = { x e. RR | 0 < x }
cxne 9863	class -e A
cxad 9864	class +e
cxmu 9865	class xe
df-xneg 9866	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9867	|- +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 9868	|- 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 9982	class (,)
cioc 9983	class (,]
cico 9984	class [,)
cicc 9985	class [,]
df-ioo 9986	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 9987	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 9988	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 9989	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10102	class ...
df-fz 10103	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10236	class ..^
df-fzo 10237	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10377	class |_
cceil 10378	class ⌈
df-fl 10379	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10380	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10433	class mod
df-mod 10434	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10558	class seq M ( .+ , F )
df-seqfrec 10559	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10649	class ^
df-exp 10650	|- ^ = ( 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 10836	class !
df-fac 10837	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10858	class _C
df-bc 10859	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 10886	class ♯
df-ihash 10887	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 10954	class Word S
df-word 10955	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
cshi 10998	class shift
df-shft 10999	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11023	class *
cre 11024	class Re
cim 11025	class Im
df-cj 11026	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11027	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11028	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11180	class sqr
cabs 11181	class abs
df-rsqrt 11182	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11183	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11462	class ~~>
df-clim 11463	|- ~~> = { <. 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 11537	class sum_ k e. A B
df-sumdc 11538	|- 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 11734	class prod_ k e. A B
df-proddc 11735	|- 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 11826	class exp
ceu 11827	class _e
csin 11828	class sin
ccos 11829	class cos
ctan 11830	class tan
cpi 11831	class pi
df-ef 11832	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 11833	|- _e = ( exp ` 1 )
df-sin 11834	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 11835	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 11836	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 11837	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 11959	class tau
df-tau 11960	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 11971	class ||
df-dvds 11972	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12124	class bits
df-bits 12125	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12147	class gcd
df-gcd 12148	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12255	class lcm
df-lcm 12256	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12302	class Prime
df-prm 12303	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12376	class numer
cdenom 12377	class denom
df-numer 12378	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12379	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12403	class odZ
cphi 12404	class phi
df-odz 12405	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12406	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12480	class pCnt
df-pc 12481	|- 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 12565	class ZZ[_i]
df-gz 12566	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 12701	class Struct
cnx 12702	class ndx
csts 12703	class sSet
cslot 12704	class Slot A
cbs 12705	class Base
cress 12706	class ↾s
df-struct 12707	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 12708	|- ndx = ( _I |` NN )
df-slot 12709	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 12711	|- Base = Slot 1
df-sets 12712	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 12713	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 12782	class +g
cmulr 12783	class .r
cstv 12784	class *r
csca 12785	class Scalar
cvsca 12786	class .s
cip 12787	class .i
cts 12788	class TopSet
cple 12789	class le
coc 12790	class oc
cds 12791	class dist
cunif 12792	class UnifSet
chom 12793	class Hom
cco 12794	class comp
df-plusg 12795	|- +g = Slot 2
df-mulr 12796	|- .r = Slot 3
df-starv 12797	|- *r = Slot 4
df-sca 12798	|- Scalar = Slot 5
df-vsca 12799	|- .s = Slot 6
df-ip 12800	|- .i = Slot 8
df-tset 12801	|- TopSet = Slot 9
df-ple 12802	|- le = Slot ; 1 0
df-ocomp 12803	|- oc = Slot ; 1 1
df-ds 12804	|- dist = Slot ; 1 2
df-unif 12805	|- UnifSet = Slot ; 1 3
df-hom 12806	|- Hom = Slot ; 1 4
df-cco 12807	|- comp = Slot ; 1 5
crest 12943	class ↾t
ctopn 12944	class TopOpen
df-rest 12945	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 12946	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 12958	class topGen
cpt 12959	class Xt_
c0g 12960	class 0g
cgsu 12961	class gsumg
df-0g 12962	|- 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 12963	|- 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 12964	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 12965	|- 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 12969	class X_s
cpws 12970	class ^s
df-prds 12971	|- 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 12994	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13003	class "s
cqus 13004	class /.s
cxps 13005	class X.s
df-iimas 13006	|- "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 13007	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13008	|- 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 13057	class +f
cmgm 13058	class Mgm
df-plusf 13059	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13060	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13105	class Smgrp
df-sgrp 13106	|- 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 13120	class Mnd
df-mnd 13121	|- 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 13161	class MndHom
csubmnd 13162	class SubMnd
df-mhm 13163	|- 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 13164	|- 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 13204	class Grp
cminusg 13205	class invg
csg 13206	class -g
df-grp 13207	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13208	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13209	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13327	class .g
df-mulg 13328	|- .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 13375	class SubGrp
cnsg 13376	class NrmSGrp
cqg 13377	class ~QG
df-subg 13378	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13379	|- 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 13380	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13448	class GrpHom
df-ghm 13449	|- 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 13492	class CMnd
cabl 13493	class Abel
df-cmn 13494	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13495	|- Abel = ( Grp i^i CMnd )
cmgp 13554	class mulGrp
df-mgp 13555	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 13566	class Rng
df-rng 13567	|- 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 13593	class 1r
df-ur 13594	|- 1r = ( 0g o. mulGrp )
csrg 13597	class SRing
df-srg 13598	|- 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 13630	class Ring
ccrg 13631	class CRing
df-ring 13632	|- 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 13633	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 13701	class oppr
df-oppr 13702	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 13720	class ||r
cui 13721	class Unit
cir 13722	class Irred
df-dvdsr 13723	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 13724	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 13725	|- 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 13754	class invr
df-invr 13755	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 13765	class /r
df-dvr 13766	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 13784	class RingHom
crs 13785	class RingIso
df-rhm 13786	|- 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 13787	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 13813	class NzRing
df-nzr 13814	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 13824	class LRing
df-lring 13825	|- 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 13831	class SubRng
df-subrng 13832	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 13851	class SubRing
crgspn 13852	class RingSpan
df-subrg 13853	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 13854	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 13889	class RLReg
cdomn 13890	class Domn
cidom 13891	class IDomn
df-rlreg 13892	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 13893	|- 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 13894	|- IDomn = ( CRing i^i Domn )
capr 13914	class #r
df-apr 13915	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 13921	class LMod
cscaf 13922	class .sf
df-lmod 13923	|- 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 13924	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 13986	class LSubSp
df-lssm 13987	|- 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 14020	class LSpan
df-lsp 14021	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14067	class subringAlg
crglmod 14068	class ringLMod
df-sra 14069	|- 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 14070	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14101	class LIdeal
crsp 14102	class RSpan
df-lidl 14103	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14104	|- RSpan = ( LSpan o. ringLMod )
c2idl 14133	class 2Ideal
df-2idl 14134	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14169	class PsMet
cxmet 14170	class *Met
cmet 14171	class Met
cbl 14172	class ball
cfbas 14173	class fBas
cfg 14174	class filGen
cmopn 14175	class MetOpen
cmetu 14176	class metUnif
df-psmet 14177	|- 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 14178	|- *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 14179	|- 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 14180	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14181	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14182	|- 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 14183	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14184	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14190	class ℂfld
df-cnfld 14191	|- ℂ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 14224	class ℤring
df-zring 14225	|- ℤring = (ℂfld ↾s ZZ )
czrh 14245	class ZRHom
czlm 14246	class ZMod
czn 14247	class ℤ/nℤ
df-zrh 14248	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14249	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14250	|- ℤ/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 14295	class mPwSer
cmpl 14296	class mPoly
df-psr 14297	|- 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 14298	|- 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 14341	class Top
df-top 14342	|- 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 14354	class TopOn
df-topon 14355	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14374	class TopSp
df-topsp 14375	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14386	class TopBases
df-bases 14387	|- 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 14436	class Clsd
cnt 14437	class int
ccl 14438	class cls
df-cld 14439	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14440	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14441	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14482	class nei
df-nei 14483	|- 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 14529	class Cn
ccnp 14530	class CnP
clm 14531	class ~~> t
df-cn 14532	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 14533	|- 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 14534	|- ~~> 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 14596	class tX
df-tx 14597	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 14644	class Homeo
df-hmeo 14645	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 14680	class *MetSp
cms 14681	class MetSp
ctms 14682	class toMetSp
df-xms 14683	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 14684	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 14685	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 14914	class -cn->
df-cncf 14915	|- -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 14998	class lim CC
cdv 14999	class _D
df-limced 15000	|- 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 15001	|- _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 15072	class Poly
cidp 15073	class Xp
df-ply 15074	|- 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 15075	|- Xp = ( _I |` CC )
clog 15200	class log
ccxp 15201	class ^c
df-relog 15202	|- log = `' ( exp |` RR )
df-rpcxp 15203	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15287	class logb
df-logb 15288	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15325	class sigma
df-sgm 15326	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15346	class /L
df-lgs 15347	|- /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 ) ) ) ) )
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 15547	wff A DECIDin B
df-dcin 15548	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 15566	wff BOUNDED ph
ax-bd0 15567	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 15568	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 15569	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 15570	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 15571	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 15572	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 15573	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 15574	|- BOUNDED x = y
ax-bdel 15575	|- BOUNDED x e. y
ax-bdsb 15576	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 15594	wff BOUNDED A
df-bdc 15595	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 15638	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 15678	|- BOUNDED ph   =>    |- DECID ph
wind 15680	wff Ind A
df-bj-ind 15681	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 15695	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 15722	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 15730	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 15736	|- 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 15741	|- 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 15743	|- ( ( ( 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 15833	wff A.! x ( ph -> ps )
walsc 15834	wff A.! x e. A ph
df-alsi 15835	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 15836	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )