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 3450	class (/)
df-nul 3451	|- (/) = ( _V \ _V )
cif 3561	class if ( ph , A , B )
df-if 3562	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3605	class ~P A
df-pw 3607	|- ~P A = { x | x C_ A }
csn 3622	class { A }
cpr 3623	class { A , B }
ctp 3624	class { A , B , C }
cop 3625	class <. A , B >.
cotp 3626	class <. A , B , C >.
df-sn 3628	|- { A } = { x | x = A }
df-pr 3629	|- { A , B } = ( { A } u. { B } )
df-tp 3630	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3631	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3632	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3839	class U. A
df-uni 3840	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3874	class |^| A
df-int 3875	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3916	class U_ x e. A B
ciin 3917	class |^|_ x e. A B
df-iun 3918	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3919	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4010	wff Disj x e. A B
df-disj 4011	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4033	wff A R B
df-br 4034	|- ( A R B <-> <. A , B >. e. R )
copab 4093	class { <. x , y >. | ph }
cmpt 4094	class ( x e. A |-> B )
df-opab 4095	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4096	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4131	wff Tr A
df-tr 4132	|- ( Tr A <-> U. A C_ A )
ax-coll 4148	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4151	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4159	|- E. x A. y -. y e. x
ax-pow 4207	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4227	wff EXMID
df-exmid 4228	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4242	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4322	class _E
cid 4323	class _I
df-eprel 4324	|- _E = { <. x , y >. | x e. y }
df-id 4328	|- _I = { <. x , y >. | x = y }
wpo 4329	wff R Po A
wor 4330	wff R Or A
df-po 4331	|- ( 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 4332	|- ( 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 4362	wff FrFor R A S
wfr 4363	wff R Fr A
wse 4364	wff R Se A
wwe 4365	wff R We A
df-frfor 4366	|- (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 4367	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4368	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4369	|- ( 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 4397	wff Ord A
con0 4398	class On
wlim 4399	wff Lim A
csuc 4400	class suc A
df-iord 4401	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4403	|- On = { x | Ord x }
df-ilim 4404	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4406	|- suc A = ( A u. { A } )
ax-un 4468	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4573	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4624	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4626	class om
df-iom 4627	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4661	class ( A X. B )
ccnv 4662	class `' A
cdm 4663	class dom A
crn 4664	class ran A
cres 4665	class ( A |` B )
cima 4666	class ( A " B )
ccom 4667	class ( A o. B )
wrel 4668	wff Rel A
df-xp 4669	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4670	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4671	|- `' A = { <. x , y >. | y A x }
df-co 4672	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4673	|- dom A = { x | E. y x A y }
df-rn 4674	|- ran A = dom `' A
df-res 4675	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4676	|- ( A " B ) = ran ( A |` B )
cio 5217	class ( iota x ph )
df-iota 5219	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5252	wff Fun A
wfn 5253	wff A Fn B
wf 5254	wff F : A --> B
wf1 5255	wff F : A -1-1-> B
wfo 5256	wff F : A -onto-> B
wf1o 5257	wff F : A -1-1-onto-> B
cfv 5258	class ( F ` A )
wiso 5259	wff H Isom R , S ( A , B )
df-fun 5260	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5261	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5262	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5263	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5264	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5265	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5266	|- ( F ` A ) = ( iota x A F x )
df-isom 5267	|- ( 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 5876	class ( iota_ x e. A ph )
df-riota 5877	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 5922	class ( A F B )
coprab 5923	class { <. <. x , y >. , z >. | ph }
cmpo 5924	class ( x e. A , y e. B |-> C )
df-ov 5925	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 5926	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 5927	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6133	class oF R
cofr 6134	class oR R
df-of 6135	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6136	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6196	class 1st
c2nd 6197	class 2nd
df-1st 6198	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6199	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6302	class tpos F
df-tpos 6303	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6343	wff Smo A
df-smo 6344	|- ( 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 6362	class recs ( F )
df-recs 6363	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6427	class rec ( F , I )
df-irdg 6428	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6448	class frec ( F , I )
df-frec 6449	|- 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 6467	class 1o
c2o 6468	class 2o
c3o 6469	class 3o
c4o 6470	class 4o
coa 6471	class +o
comu 6472	class .o
coei 6473	class ↑o
df-1o 6474	|- 1o = suc (/)
df-2o 6475	|- 2o = suc 1o
df-3o 6476	|- 3o = suc 2o
df-4o 6477	|- 4o = suc 3o
df-oadd 6478	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6479	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6480	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6589	wff R Er A
cec 6590	class [ A ] R
cqs 6591	class ( A /. R )
df-er 6592	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6594	|- [ A ] R = ( R " { A } )
df-qs 6598	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6707	class ^m
cpm 6708	class ^pm
df-map 6709	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6710	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6757	class X_ x e. A B
df-ixp 6758	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6797	class ~~
cdom 6798	class ~<_
cfn 6799	class Fin
df-en 6800	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6801	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6802	|- Fin = { x | E. y e. om x ~~ y }
cfi 7034	class fi
df-fi 7035	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7048	class sup ( A , B , R )
cinf 7049	class inf ( A , B , R )
df-sup 7050	|- 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 7051	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7103	class ( A ⊔ B )
df-dju 7104	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7111	class inl
cinr 7112	class inr
df-inl 7113	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7114	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7149	class case ( R , S )
df-case 7150	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7168	class ( R ⊔d S )
df-djud 7169	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7185	class ℕ∞
df-nninf 7186	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7200	class Omni
df-omni 7201	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7217	class Markov
df-markov 7218	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7229	class WOmni
df-womni 7230	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7246	class card
df-card 7247	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
wac 7272	wff CHOICE
df-ac 7273	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7314	wff R Ap A
df-pap 7315	|- ( 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 7316	wff R TAp A
df-tap 7317	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7329	wff CCHOICE
df-cc 7330	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7339	class N.
cpli 7340	class +N
cmi 7341	class .N
clti 7342	class <N
cplpq 7343	class +pQ
cmpq 7344	class .pQ
cltpq 7345	class <pQ
ceq 7346	class ~Q
cnq 7347	class Q.
c1q 7348	class 1Q
cplq 7349	class +Q
cmq 7350	class .Q
crq 7351	class *Q
cltq 7352	class <Q
ceq0 7353	class ~Q0
cnq0 7354	class Q0
c0q0 7355	class 0Q0
cplq0 7356	class +Q0
cmq0 7357	class ·Q0
cnp 7358	class P.
c1p 7359	class 1P
cpp 7360	class +P.
cmp 7361	class .P.
cltp 7362	class <P
cer 7363	class ~R
cnr 7364	class R.
c0r 7365	class 0R
c1r 7366	class 1R
cm1r 7367	class -1R
cplr 7368	class +R
cmr 7369	class .R
cltr 7370	class <R
df-ni 7371	|- N. = ( om \ { (/) } )
df-pli 7372	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7373	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7374	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7411	|- +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 7412	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7413	|- <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 7414	|- ~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 7415	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7416	|- +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 7417	|- .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 7418	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7419	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7420	|- <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 7491	|- ~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 7492	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7493	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7494	|- +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 7495	|- ·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 7533	|- 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 7534	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7535	|- +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 7536	|- .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 7537	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7793	|- ~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 7794	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7795	|- +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 7796	|- .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 7797	|- <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 7798	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7799	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7800	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 7877	class CC
cr 7878	class RR
cc0 7879	class 0
c1 7880	class 1
ci 7881	class _i
caddc 7882	class +
cltrr 7883	class <RR
cmul 7884	class x.
df-c 7885	|- CC = ( R. X. R. )
df-0 7886	|- 0 = <. 0R , 0R >.
df-1 7887	|- 1 = <. 1R , 0R >.
df-i 7888	|- _i = <. 0R , 1R >.
df-r 7889	|- RR = ( R. X. { 0R } )
df-add 7890	|- + = { <. <. 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 7891	|- 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 7892	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 7970	|- CC e. _V
ax-resscn 7971	|- RR C_ CC
ax-1cn 7972	|- 1 e. CC
ax-1re 7973	|- 1 e. RR
ax-icn 7974	|- _i e. CC
ax-addcl 7975	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 7976	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 7977	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 7978	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 7979	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 7980	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 7981	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 7982	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 7983	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 7984	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 7985	|- 0 <RR 1
ax-1rid 7986	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 7987	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 7988	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 7989	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 7990	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 7991	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 7992	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 7993	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 7994	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 7995	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 7996	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 7997	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 7998	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 7999	|- 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 8000	|- ( ( ( 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 8001	|- + : ( CC X. CC ) --> CC
ax-mulf 8002	|- x. : ( CC X. CC ) --> CC
cpnf 8058	class +oo
cmnf 8059	class -oo
cxr 8060	class RR*
clt 8061	class <
cle 8062	class <_
df-pnf 8063	|- +oo = ~P U. CC
df-mnf 8064	|- -oo = ~P +oo
df-xr 8065	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8066	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8067	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8197	class -
cneg 8198	class -u A
df-sub 8199	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8200	|- -u A = ( 0 - A )
creap 8601	class #ℝ
df-reap 8602	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8608	class #
df-ap 8609	|- # = { <. 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 8699	class /
df-div 8700	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 8990	class NN
df-inn 8991	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9041	class 2
c3 9042	class 3
c4 9043	class 4
c5 9044	class 5
c6 9045	class 6
c7 9046	class 7
c8 9047	class 8
c9 9048	class 9
df-2 9049	|- 2 = ( 1 + 1 )
df-3 9050	|- 3 = ( 2 + 1 )
df-4 9051	|- 4 = ( 3 + 1 )
df-5 9052	|- 5 = ( 4 + 1 )
df-6 9053	|- 6 = ( 5 + 1 )
df-7 9054	|- 7 = ( 6 + 1 )
df-8 9055	|- 8 = ( 7 + 1 )
df-9 9056	|- 9 = ( 8 + 1 )
cn0 9249	class NN0
df-n0 9250	|- NN0 = ( NN u. { 0 } )
cxnn0 9312	class NN0*
df-xnn0 9313	|- NN0* = ( NN0 u. { +oo } )
cz 9326	class ZZ
df-z 9327	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9457	class ; A B
df-dec 9458	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9601	class ZZ>=
df-uz 9602	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9693	class QQ
df-q 9694	|- QQ = ( / " ( ZZ X. NN ) )
crp 9728	class RR+
df-rp 9729	|- RR+ = { x e. RR | 0 < x }
cxne 9844	class -e A
cxad 9845	class +e
cxmu 9846	class xe
df-xneg 9847	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9848	|- +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 9849	|- 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 9963	class (,)
cioc 9964	class (,]
cico 9965	class [,)
cicc 9966	class [,]
df-ioo 9967	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 9968	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 9969	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 9970	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10083	class ...
df-fz 10084	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10217	class ..^
df-fzo 10218	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10358	class |_
cceil 10359	class ⌈
df-fl 10360	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10361	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10414	class mod
df-mod 10415	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10539	class seq M ( .+ , F )
df-seqfrec 10540	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10630	class ^
df-exp 10631	|- ^ = ( 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 10817	class !
df-fac 10818	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10839	class _C
df-bc 10840	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 10867	class ♯
df-ihash 10868	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 10935	class Word S
df-word 10936	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
cshi 10979	class shift
df-shft 10980	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11004	class *
cre 11005	class Re
cim 11006	class Im
df-cj 11007	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11008	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11009	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11161	class sqr
cabs 11162	class abs
df-rsqrt 11163	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11164	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11443	class ~~>
df-clim 11444	|- ~~> = { <. 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 11518	class sum_ k e. A B
df-sumdc 11519	|- 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 11715	class prod_ k e. A B
df-proddc 11716	|- 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 11807	class exp
ceu 11808	class _e
csin 11809	class sin
ccos 11810	class cos
ctan 11811	class tan
cpi 11812	class pi
df-ef 11813	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 11814	|- _e = ( exp ` 1 )
df-sin 11815	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 11816	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 11817	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 11818	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 11940	class tau
df-tau 11941	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 11952	class ||
df-dvds 11953	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12105	class bits
df-bits 12106	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12120	class gcd
df-gcd 12121	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12228	class lcm
df-lcm 12229	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12275	class Prime
df-prm 12276	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12349	class numer
cdenom 12350	class denom
df-numer 12351	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12352	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12376	class odZ
cphi 12377	class phi
df-odz 12378	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12379	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12453	class pCnt
df-pc 12454	|- 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 12538	class ZZ[_i]
df-gz 12539	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 12674	class Struct
cnx 12675	class ndx
csts 12676	class sSet
cslot 12677	class Slot A
cbs 12678	class Base
cress 12679	class ↾s
df-struct 12680	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 12681	|- ndx = ( _I |` NN )
df-slot 12682	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 12684	|- Base = Slot 1
df-sets 12685	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 12686	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 12755	class +g
cmulr 12756	class .r
cstv 12757	class *r
csca 12758	class Scalar
cvsca 12759	class .s
cip 12760	class .i
cts 12761	class TopSet
cple 12762	class le
coc 12763	class oc
cds 12764	class dist
cunif 12765	class UnifSet
chom 12766	class Hom
cco 12767	class comp
df-plusg 12768	|- +g = Slot 2
df-mulr 12769	|- .r = Slot 3
df-starv 12770	|- *r = Slot 4
df-sca 12771	|- Scalar = Slot 5
df-vsca 12772	|- .s = Slot 6
df-ip 12773	|- .i = Slot 8
df-tset 12774	|- TopSet = Slot 9
df-ple 12775	|- le = Slot ; 1 0
df-ocomp 12776	|- oc = Slot ; 1 1
df-ds 12777	|- dist = Slot ; 1 2
df-unif 12778	|- UnifSet = Slot ; 1 3
df-hom 12779	|- Hom = Slot ; 1 4
df-cco 12780	|- comp = Slot ; 1 5
crest 12910	class ↾t
ctopn 12911	class TopOpen
df-rest 12912	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 12913	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 12925	class topGen
cpt 12926	class Xt_
c0g 12927	class 0g
cgsu 12928	class gsumg
df-0g 12929	|- 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 12930	|- 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 12931	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 12932	|- 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 12936	class X_s
cpws 12937	class ^s
df-prds 12938	|- 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. ( c h ( 2nd ` a ) ) , 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 12941	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 12942	class "s
cqus 12943	class /.s
cxps 12944	class X.s
df-iimas 12945	|- "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 12946	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 12947	|- 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 12996	class +f
cmgm 12997	class Mgm
df-plusf 12998	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 12999	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13044	class Smgrp
df-sgrp 13045	|- 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 13057	class Mnd
df-mnd 13058	|- 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 13089	class MndHom
csubmnd 13090	class SubMnd
df-mhm 13091	|- 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 13092	|- 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 13132	class Grp
cminusg 13133	class invg
csg 13134	class -g
df-grp 13135	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13136	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13137	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13249	class .g
df-mulg 13250	|- .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 13297	class SubGrp
cnsg 13298	class NrmSGrp
cqg 13299	class ~QG
df-subg 13300	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13301	|- 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 13302	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13370	class GrpHom
df-ghm 13371	|- 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 13414	class CMnd
cabl 13415	class Abel
df-cmn 13416	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13417	|- Abel = ( Grp i^i CMnd )
cmgp 13476	class mulGrp
df-mgp 13477	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 13488	class Rng
df-rng 13489	|- 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 13515	class 1r
df-ur 13516	|- 1r = ( 0g o. mulGrp )
csrg 13519	class SRing
df-srg 13520	|- 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 13552	class Ring
ccrg 13553	class CRing
df-ring 13554	|- 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 13555	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 13623	class oppr
df-oppr 13624	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 13642	class ||r
cui 13643	class Unit
cir 13644	class Irred
df-dvdsr 13645	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 13646	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 13647	|- 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 13676	class invr
df-invr 13677	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 13687	class /r
df-dvr 13688	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 13706	class RingHom
crs 13707	class RingIso
df-rhm 13708	|- 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 13709	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 13735	class NzRing
df-nzr 13736	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 13746	class LRing
df-lring 13747	|- 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 13753	class SubRng
df-subrng 13754	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 13773	class SubRing
crgspn 13774	class RingSpan
df-subrg 13775	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 13776	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 13811	class RLReg
cdomn 13812	class Domn
cidom 13813	class IDomn
df-rlreg 13814	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 13815	|- 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 13816	|- IDomn = ( CRing i^i Domn )
capr 13836	class #r
df-apr 13837	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 13843	class LMod
cscaf 13844	class .sf
df-lmod 13845	|- 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 13846	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 13908	class LSubSp
df-lssm 13909	|- 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 13942	class LSpan
df-lsp 13943	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 13989	class subringAlg
crglmod 13990	class ringLMod
df-sra 13991	|- 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 13992	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14023	class LIdeal
crsp 14024	class RSpan
df-lidl 14025	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14026	|- RSpan = ( LSpan o. ringLMod )
c2idl 14055	class 2Ideal
df-2idl 14056	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14091	class PsMet
cxmet 14092	class *Met
cmet 14093	class Met
cbl 14094	class ball
cfbas 14095	class fBas
cfg 14096	class filGen
cmopn 14097	class MetOpen
cmetu 14098	class metUnif
df-psmet 14099	|- 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 14100	|- *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 14101	|- 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 14102	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14103	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14104	|- 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 14105	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14106	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14112	class ℂfld
df-cnfld 14113	|- ℂ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 14146	class ℤring
df-zring 14147	|- ℤring = (ℂfld ↾s ZZ )
czrh 14167	class ZRHom
czlm 14168	class ZMod
czn 14169	class ℤ/nℤ
df-zrh 14170	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14171	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14172	|- ℤ/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 14217	class mPwSer
df-psr 14218	|- 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 14233	class Top
df-top 14234	|- 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 14246	class TopOn
df-topon 14247	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14266	class TopSp
df-topsp 14267	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14278	class TopBases
df-bases 14279	|- 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 14328	class Clsd
cnt 14329	class int
ccl 14330	class cls
df-cld 14331	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14332	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14333	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14374	class nei
df-nei 14375	|- 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 14421	class Cn
ccnp 14422	class CnP
clm 14423	class ~~> t
df-cn 14424	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 14425	|- 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 14426	|- ~~> 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 14488	class tX
df-tx 14489	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 14536	class Homeo
df-hmeo 14537	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 14572	class *MetSp
cms 14573	class MetSp
ctms 14574	class toMetSp
df-xms 14575	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 14576	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 14577	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 14806	class -cn->
df-cncf 14807	|- -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 14890	class lim CC
cdv 14891	class _D
df-limced 14892	|- 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 14893	|- _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 14964	class Poly
cidp 14965	class Xp
df-ply 14966	|- 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 14967	|- Xp = ( _I |` CC )
clog 15092	class log
ccxp 15093	class ^c
df-relog 15094	|- log = `' ( exp |` RR )
df-rpcxp 15095	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15179	class logb
df-logb 15180	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15217	class sigma
df-sgm 15218	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15238	class /L
df-lgs 15239	|- /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 15439	wff A DECIDin B
df-dcin 15440	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 15458	wff BOUNDED ph
ax-bd0 15459	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 15460	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 15461	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 15462	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 15463	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 15464	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 15465	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 15466	|- BOUNDED x = y
ax-bdel 15467	|- BOUNDED x e. y
ax-bdsb 15468	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 15486	wff BOUNDED A
df-bdc 15487	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 15530	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 15570	|- BOUNDED ph   =>    |- DECID ph
wind 15572	wff Ind A
df-bj-ind 15573	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 15587	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 15614	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 15622	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 15628	|- 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 15633	|- 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 15635	|- ( ( ( 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 15720	wff A.! x ( ph -> ps )
walsc 15721	wff A.! x e. A ph
df-alsi 15722	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 15723	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )