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 7255	class card
wacn 7256	class AC A
df-card 7257	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7258	|- 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 7288	wff CHOICE
df-ac 7289	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7330	wff R Ap A
df-pap 7331	|- ( 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 7332	wff R TAp A
df-tap 7333	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7345	wff CCHOICE
df-cc 7346	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7356	class N.
cpli 7357	class +N
cmi 7358	class .N
clti 7359	class <N
cplpq 7360	class +pQ
cmpq 7361	class .pQ
cltpq 7362	class <pQ
ceq 7363	class ~Q
cnq 7364	class Q.
c1q 7365	class 1Q
cplq 7366	class +Q
cmq 7367	class .Q
crq 7368	class *Q
cltq 7369	class <Q
ceq0 7370	class ~Q0
cnq0 7371	class Q0
c0q0 7372	class 0Q0
cplq0 7373	class +Q0
cmq0 7374	class ·Q0
cnp 7375	class P.
c1p 7376	class 1P
cpp 7377	class +P.
cmp 7378	class .P.
cltp 7379	class <P
cer 7380	class ~R
cnr 7381	class R.
c0r 7382	class 0R
c1r 7383	class 1R
cm1r 7384	class -1R
cplr 7385	class +R
cmr 7386	class .R
cltr 7387	class <R
df-ni 7388	|- N. = ( om \ { (/) } )
df-pli 7389	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7390	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7391	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7428	|- +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 7429	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7430	|- <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 7431	|- ~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 7432	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7433	|- +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 7434	|- .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 7435	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7436	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7437	|- <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 7508	|- ~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 7509	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7510	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7511	|- +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 7512	|- ·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 7550	|- 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 7551	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7552	|- +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 7553	|- .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 7554	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7810	|- ~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 7811	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7812	|- +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 7813	|- .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 7814	|- <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 7815	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7816	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7817	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 7894	class CC
cr 7895	class RR
cc0 7896	class 0
c1 7897	class 1
ci 7898	class _i
caddc 7899	class +
cltrr 7900	class <RR
cmul 7901	class x.
df-c 7902	|- CC = ( R. X. R. )
df-0 7903	|- 0 = <. 0R , 0R >.
df-1 7904	|- 1 = <. 1R , 0R >.
df-i 7905	|- _i = <. 0R , 1R >.
df-r 7906	|- RR = ( R. X. { 0R } )
df-add 7907	|- + = { <. <. 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 7908	|- 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 7909	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 7987	|- CC e. _V
ax-resscn 7988	|- RR C_ CC
ax-1cn 7989	|- 1 e. CC
ax-1re 7990	|- 1 e. RR
ax-icn 7991	|- _i e. CC
ax-addcl 7992	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 7993	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 7994	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 7995	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 7996	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 7997	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 7998	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 7999	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8000	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8001	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8002	|- 0 <RR 1
ax-1rid 8003	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8004	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8005	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8006	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8007	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8008	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8009	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8010	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8011	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8012	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8013	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8014	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8015	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8016	|- 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 8017	|- ( ( ( 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 8018	|- + : ( CC X. CC ) --> CC
ax-mulf 8019	|- x. : ( CC X. CC ) --> CC
cpnf 8075	class +oo
cmnf 8076	class -oo
cxr 8077	class RR*
clt 8078	class <
cle 8079	class <_
df-pnf 8080	|- +oo = ~P U. CC
df-mnf 8081	|- -oo = ~P +oo
df-xr 8082	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8083	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8084	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8214	class -
cneg 8215	class -u A
df-sub 8216	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8217	|- -u A = ( 0 - A )
creap 8618	class #ℝ
df-reap 8619	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8625	class #
df-ap 8626	|- # = { <. 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 8716	class /
df-div 8717	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9007	class NN
df-inn 9008	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9058	class 2
c3 9059	class 3
c4 9060	class 4
c5 9061	class 5
c6 9062	class 6
c7 9063	class 7
c8 9064	class 8
c9 9065	class 9
df-2 9066	|- 2 = ( 1 + 1 )
df-3 9067	|- 3 = ( 2 + 1 )
df-4 9068	|- 4 = ( 3 + 1 )
df-5 9069	|- 5 = ( 4 + 1 )
df-6 9070	|- 6 = ( 5 + 1 )
df-7 9071	|- 7 = ( 6 + 1 )
df-8 9072	|- 8 = ( 7 + 1 )
df-9 9073	|- 9 = ( 8 + 1 )
cn0 9266	class NN0
df-n0 9267	|- NN0 = ( NN u. { 0 } )
cxnn0 9329	class NN0*
df-xnn0 9330	|- NN0* = ( NN0 u. { +oo } )
cz 9343	class ZZ
df-z 9344	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9474	class ; A B
df-dec 9475	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9618	class ZZ>=
df-uz 9619	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9710	class QQ
df-q 9711	|- QQ = ( / " ( ZZ X. NN ) )
crp 9745	class RR+
df-rp 9746	|- RR+ = { x e. RR | 0 < x }
cxne 9861	class -e A
cxad 9862	class +e
cxmu 9863	class xe
df-xneg 9864	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9865	|- +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 9866	|- 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 9980	class (,)
cioc 9981	class (,]
cico 9982	class [,)
cicc 9983	class [,]
df-ioo 9984	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 9985	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 9986	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 9987	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10100	class ...
df-fz 10101	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10234	class ..^
df-fzo 10235	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10375	class |_
cceil 10376	class ⌈
df-fl 10377	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10378	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10431	class mod
df-mod 10432	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10556	class seq M ( .+ , F )
df-seqfrec 10557	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10647	class ^
df-exp 10648	|- ^ = ( 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 10834	class !
df-fac 10835	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10856	class _C
df-bc 10857	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 10884	class ♯
df-ihash 10885	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 10952	class Word S
df-word 10953	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
cshi 10996	class shift
df-shft 10997	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11021	class *
cre 11022	class Re
cim 11023	class Im
df-cj 11024	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11025	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11026	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11178	class sqr
cabs 11179	class abs
df-rsqrt 11180	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11181	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11460	class ~~>
df-clim 11461	|- ~~> = { <. 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 11535	class sum_ k e. A B
df-sumdc 11536	|- 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 11732	class prod_ k e. A B
df-proddc 11733	|- 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 11824	class exp
ceu 11825	class _e
csin 11826	class sin
ccos 11827	class cos
ctan 11828	class tan
cpi 11829	class pi
df-ef 11830	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 11831	|- _e = ( exp ` 1 )
df-sin 11832	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 11833	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 11834	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 11835	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 11957	class tau
df-tau 11958	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 11969	class ||
df-dvds 11970	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12122	class bits
df-bits 12123	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12145	class gcd
df-gcd 12146	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12253	class lcm
df-lcm 12254	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12300	class Prime
df-prm 12301	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12374	class numer
cdenom 12375	class denom
df-numer 12376	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12377	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12401	class odZ
cphi 12402	class phi
df-odz 12403	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12404	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12478	class pCnt
df-pc 12479	|- 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 12563	class ZZ[_i]
df-gz 12564	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 12699	class Struct
cnx 12700	class ndx
csts 12701	class sSet
cslot 12702	class Slot A
cbs 12703	class Base
cress 12704	class ↾s
df-struct 12705	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 12706	|- ndx = ( _I |` NN )
df-slot 12707	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 12709	|- Base = Slot 1
df-sets 12710	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 12711	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 12780	class +g
cmulr 12781	class .r
cstv 12782	class *r
csca 12783	class Scalar
cvsca 12784	class .s
cip 12785	class .i
cts 12786	class TopSet
cple 12787	class le
coc 12788	class oc
cds 12789	class dist
cunif 12790	class UnifSet
chom 12791	class Hom
cco 12792	class comp
df-plusg 12793	|- +g = Slot 2
df-mulr 12794	|- .r = Slot 3
df-starv 12795	|- *r = Slot 4
df-sca 12796	|- Scalar = Slot 5
df-vsca 12797	|- .s = Slot 6
df-ip 12798	|- .i = Slot 8
df-tset 12799	|- TopSet = Slot 9
df-ple 12800	|- le = Slot ; 1 0
df-ocomp 12801	|- oc = Slot ; 1 1
df-ds 12802	|- dist = Slot ; 1 2
df-unif 12803	|- UnifSet = Slot ; 1 3
df-hom 12804	|- Hom = Slot ; 1 4
df-cco 12805	|- comp = Slot ; 1 5
crest 12941	class ↾t
ctopn 12942	class TopOpen
df-rest 12943	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 12944	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 12956	class topGen
cpt 12957	class Xt_
c0g 12958	class 0g
cgsu 12959	class gsumg
df-0g 12960	|- 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 12961	|- 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 12962	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 12963	|- 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 12967	class X_s
cpws 12968	class ^s
df-prds 12969	|- 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 12992	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13001	class "s
cqus 13002	class /.s
cxps 13003	class X.s
df-iimas 13004	|- "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 13005	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13006	|- 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 13055	class +f
cmgm 13056	class Mgm
df-plusf 13057	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13058	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13103	class Smgrp
df-sgrp 13104	|- 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 13118	class Mnd
df-mnd 13119	|- 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 13159	class MndHom
csubmnd 13160	class SubMnd
df-mhm 13161	|- 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 13162	|- 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 13202	class Grp
cminusg 13203	class invg
csg 13204	class -g
df-grp 13205	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13206	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13207	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13325	class .g
df-mulg 13326	|- .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 13373	class SubGrp
cnsg 13374	class NrmSGrp
cqg 13375	class ~QG
df-subg 13376	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13377	|- 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 13378	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13446	class GrpHom
df-ghm 13447	|- 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 13490	class CMnd
cabl 13491	class Abel
df-cmn 13492	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13493	|- Abel = ( Grp i^i CMnd )
cmgp 13552	class mulGrp
df-mgp 13553	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 13564	class Rng
df-rng 13565	|- 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 13591	class 1r
df-ur 13592	|- 1r = ( 0g o. mulGrp )
csrg 13595	class SRing
df-srg 13596	|- 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 13628	class Ring
ccrg 13629	class CRing
df-ring 13630	|- 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 13631	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 13699	class oppr
df-oppr 13700	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 13718	class ||r
cui 13719	class Unit
cir 13720	class Irred
df-dvdsr 13721	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 13722	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 13723	|- 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 13752	class invr
df-invr 13753	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 13763	class /r
df-dvr 13764	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 13782	class RingHom
crs 13783	class RingIso
df-rhm 13784	|- 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 13785	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 13811	class NzRing
df-nzr 13812	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 13822	class LRing
df-lring 13823	|- 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 13829	class SubRng
df-subrng 13830	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 13849	class SubRing
crgspn 13850	class RingSpan
df-subrg 13851	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 13852	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 13887	class RLReg
cdomn 13888	class Domn
cidom 13889	class IDomn
df-rlreg 13890	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 13891	|- 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 13892	|- IDomn = ( CRing i^i Domn )
capr 13912	class #r
df-apr 13913	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 13919	class LMod
cscaf 13920	class .sf
df-lmod 13921	|- 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 13922	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 13984	class LSubSp
df-lssm 13985	|- 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 14018	class LSpan
df-lsp 14019	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14065	class subringAlg
crglmod 14066	class ringLMod
df-sra 14067	|- 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 14068	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14099	class LIdeal
crsp 14100	class RSpan
df-lidl 14101	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14102	|- RSpan = ( LSpan o. ringLMod )
c2idl 14131	class 2Ideal
df-2idl 14132	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14167	class PsMet
cxmet 14168	class *Met
cmet 14169	class Met
cbl 14170	class ball
cfbas 14171	class fBas
cfg 14172	class filGen
cmopn 14173	class MetOpen
cmetu 14174	class metUnif
df-psmet 14175	|- 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 14176	|- *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 14177	|- 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 14178	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14179	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14180	|- 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 14181	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14182	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14188	class ℂfld
df-cnfld 14189	|- ℂ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 14222	class ℤring
df-zring 14223	|- ℤring = (ℂfld ↾s ZZ )
czrh 14243	class ZRHom
czlm 14244	class ZMod
czn 14245	class ℤ/nℤ
df-zrh 14246	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14247	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14248	|- ℤ/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 14293	class mPwSer
df-psr 14294	|- 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 ) } ) ) >. } ) )
ctop 14317	class Top
df-top 14318	|- 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 14330	class TopOn
df-topon 14331	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14350	class TopSp
df-topsp 14351	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14362	class TopBases
df-bases 14363	|- 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 14412	class Clsd
cnt 14413	class int
ccl 14414	class cls
df-cld 14415	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14416	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14417	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14458	class nei
df-nei 14459	|- 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 14505	class Cn
ccnp 14506	class CnP
clm 14507	class ~~> t
df-cn 14508	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 14509	|- 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 14510	|- ~~> 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 14572	class tX
df-tx 14573	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 14620	class Homeo
df-hmeo 14621	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 14656	class *MetSp
cms 14657	class MetSp
ctms 14658	class toMetSp
df-xms 14659	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 14660	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 14661	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 14890	class -cn->
df-cncf 14891	|- -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 14974	class lim CC
cdv 14975	class _D
df-limced 14976	|- 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 14977	|- _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 15048	class Poly
cidp 15049	class Xp
df-ply 15050	|- 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 15051	|- Xp = ( _I |` CC )
clog 15176	class log
ccxp 15177	class ^c
df-relog 15178	|- log = `' ( exp |` RR )
df-rpcxp 15179	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15263	class logb
df-logb 15264	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15301	class sigma
df-sgm 15302	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15322	class /L
df-lgs 15323	|- /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 15523	wff A DECIDin B
df-dcin 15524	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 15542	wff BOUNDED ph
ax-bd0 15543	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 15544	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 15545	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 15546	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 15547	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 15548	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 15549	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 15550	|- BOUNDED x = y
ax-bdel 15551	|- BOUNDED x e. y
ax-bdsb 15552	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 15570	wff BOUNDED A
df-bdc 15571	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 15614	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 15654	|- BOUNDED ph   =>    |- DECID ph
wind 15656	wff Ind A
df-bj-ind 15657	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 15671	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 15698	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 15706	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 15712	|- 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 15717	|- 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 15719	|- ( ( ( 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 15807	wff A.! x ( ph -> ps )
walsc 15808	wff A.! x e. A ph
df-alsi 15809	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 15810	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )