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 103	wff ( ph /\ ps )
wb 104	wff ( ph <-> ps )
ax-ia1 105	|- ( ( ph /\ ps ) -> ph )
ax-ia2 106	|- ( ( ph /\ ps ) -> ps )
ax-ia3 107	|- ( ph -> ( ps -> ( ph /\ ps ) ) )
df-bi 116	|- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
ax-in1 604	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 605	|- ( -. ph -> ( ph -> ps ) )
wo 698	wff ( ph \/ ps )
ax-io 699	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 820	wff STAB ph
df-stab 821	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 824	wff DECID ph
df-dc 825	|- (DECID ph <-> ( ph \/ -. ph ) )
w3o 967	wff ( ph \/ ps \/ ch )
w3a 968	wff ( ph /\ ps /\ ch )
df-3or 969	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 970	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1341	wff A. x ph
cv 1342	class x
wceq 1343	wff A = B
wtru 1344	wff T.
df-tru 1346	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1348	wff F.
df-fal 1349	|- ( F. <-> -. T. )
wxo 1365	wff ( ph \/_ ps )
df-xor 1366	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1435	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1436	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1437	|- ph   =>    |- A. x ph
wnf 1448	wff F/ x ph
df-nf 1449	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1480	wff E. x ph
ax-ie1 1481	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1482	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1492	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1493	|- ( A. x x = y -> A. y y = x )
ax-11 1494	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1495	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1497	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1498	|- ( A. x ph -> ph )
ax-17 1514	|- ( ph -> A. x ph )
ax-i9 1518	|- E. x x = y
ax-ial 1522	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1523	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1704	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1750	wff [ y / x ] ph
df-sb 1751	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1802	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1811	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2014	wff E! x ph
wmo 2015	wff E* x ph
df-eu 2017	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2018	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2136	wff A e. B
ax-13 2138	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2139	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2147	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2151	class { x | ph }
df-clab 2152	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2158	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2161	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2294	wff F/_ x A
df-nfc 2296	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2335	wff A =/= B
df-ne 2336	|- ( A =/= B <-> -. A = B )
wnel 2430	wff A e/ B
df-nel 2431	|- ( A e/ B <-> -. A e. B )
wral 2443	wff A. x e. A ph
wrex 2444	wff E. x e. A ph
wreu 2445	wff E! x e. A ph
wrmo 2446	wff E* x e. A ph
crab 2447	class { x e. A | ph }
df-ral 2448	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2449	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2450	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2451	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2452	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2725	class _V
df-v 2727	|- _V = { x | x = x }
wcdeq 2933	wff CondEq ( x = y -> ph )
df-cdeq 2934	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 2950	wff [. A / x ]. ph
df-sbc 2951	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3044	class [_ A / x ]_ B
df-csb 3045	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3112	class ( A \ B )
cun 3113	class ( A u. B )
cin 3114	class ( A i^i B )
wss 3115	wff A C_ B
df-dif 3117	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3119	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3121	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3128	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3408	class (/)
df-nul 3409	|- (/) = ( _V \ _V )
cif 3519	class if ( ph , A , B )
df-if 3520	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3558	class ~P A
df-pw 3560	|- ~P A = { x | x C_ A }
csn 3575	class { A }
cpr 3576	class { A , B }
ctp 3577	class { A , B , C }
cop 3578	class <. A , B >.
cotp 3579	class <. A , B , C >.
df-sn 3581	|- { A } = { x | x = A }
df-pr 3582	|- { A , B } = ( { A } u. { B } )
df-tp 3583	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3584	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3585	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3788	class U. A
df-uni 3789	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3823	class |^| A
df-int 3824	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3865	class U_ x e. A B
ciin 3866	class |^|_ x e. A B
df-iun 3867	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3868	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 3958	wff Disj x e. A B
df-disj 3959	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 3981	wff A R B
df-br 3982	|- ( A R B <-> <. A , B >. e. R )
copab 4041	class { <. x , y >. | ph }
cmpt 4042	class ( x e. A |-> B )
df-opab 4043	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4044	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4079	wff Tr A
df-tr 4080	|- ( Tr A <-> U. A C_ A )
ax-coll 4096	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4099	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4107	|- E. x A. y -. y e. x
ax-pow 4152	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4172	wff EXMID
df-exmid 4173	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4186	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4264	class _E
cid 4265	class _I
df-eprel 4266	|- _E = { <. x , y >. | x e. y }
df-id 4270	|- _I = { <. x , y >. | x = y }
wpo 4271	wff R Po A
wor 4272	wff R Or A
df-po 4273	|- ( 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 4274	|- ( 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 4304	wff FrFor R A S
wfr 4305	wff R Fr A
wse 4306	wff R Se A
wwe 4307	wff R We A
df-frfor 4308	|- (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 4309	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4310	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4311	|- ( 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 4339	wff Ord A
con0 4340	class On
wlim 4341	wff Lim A
csuc 4342	class suc A
df-iord 4343	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4345	|- On = { x | Ord x }
df-ilim 4346	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4348	|- suc A = ( A u. { A } )
ax-un 4410	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4513	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4564	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4566	class om
df-iom 4567	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4601	class ( A X. B )
ccnv 4602	class `' A
cdm 4603	class dom A
crn 4604	class ran A
cres 4605	class ( A |` B )
cima 4606	class ( A " B )
ccom 4607	class ( A o. B )
wrel 4608	wff Rel A
df-xp 4609	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4610	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4611	|- `' A = { <. x , y >. | y A x }
df-co 4612	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4613	|- dom A = { x | E. y x A y }
df-rn 4614	|- ran A = dom `' A
df-res 4615	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4616	|- ( A " B ) = ran ( A |` B )
cio 5150	class ( iota x ph )
df-iota 5152	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5181	wff Fun A
wfn 5182	wff A Fn B
wf 5183	wff F : A --> B
wf1 5184	wff F : A -1-1-> B
wfo 5185	wff F : A -onto-> B
wf1o 5186	wff F : A -1-1-onto-> B
cfv 5187	class ( F ` A )
wiso 5188	wff H Isom R , S ( A , B )
df-fun 5189	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5190	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5191	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5192	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5193	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5194	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5195	|- ( F ` A ) = ( iota x A F x )
df-isom 5196	|- ( 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 5796	class ( iota_ x e. A ph )
df-riota 5797	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 5841	class ( A F B )
coprab 5842	class { <. <. x , y >. , z >. | ph }
cmpo 5843	class ( x e. A , y e. B |-> C )
df-ov 5844	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 5845	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 5846	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6047	class oF R
cofr 6048	class oR R
df-of 6049	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6050	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6103	class 1st
c2nd 6104	class 2nd
df-1st 6105	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6106	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6208	class tpos F
df-tpos 6209	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6249	wff Smo A
df-smo 6250	|- ( 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 6268	class recs ( F )
df-recs 6269	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6333	class rec ( F , I )
df-irdg 6334	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6354	class frec ( F , I )
df-frec 6355	|- 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 6373	class 1o
c2o 6374	class 2o
c3o 6375	class 3o
c4o 6376	class 4o
coa 6377	class +o
comu 6378	class .o
coei 6379	class ↑o
df-1o 6380	|- 1o = suc (/)
df-2o 6381	|- 2o = suc 1o
df-3o 6382	|- 3o = suc 2o
df-4o 6383	|- 4o = suc 3o
df-oadd 6384	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6385	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6386	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6494	wff R Er A
cec 6495	class [ A ] R
cqs 6496	class ( A /. R )
df-er 6497	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6499	|- [ A ] R = ( R " { A } )
df-qs 6503	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6610	class ^m
cpm 6611	class ^pm
df-map 6612	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6613	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6660	class X_ x e. A B
df-ixp 6661	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6700	class ~~
cdom 6701	class ~<_
cfn 6702	class Fin
df-en 6703	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6704	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6705	|- Fin = { x | E. y e. om x ~~ y }
cfi 6929	class fi
df-fi 6930	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 6943	class sup ( A , B , R )
cinf 6944	class inf ( A , B , R )
df-sup 6945	|- 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 6946	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 6998	class ( A ⊔ B )
df-dju 6999	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7006	class inl
cinr 7007	class inr
df-inl 7008	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7009	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7044	class case ( R , S )
df-case 7045	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7063	class ( R ⊔d S )
df-djud 7064	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7080	class ℕ∞
df-nninf 7081	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7094	class Omni
df-omni 7095	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7111	class Markov
df-markov 7112	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7123	class WOmni
df-womni 7124	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7131	class card
df-card 7132	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
wac 7157	wff CHOICE
df-ac 7158	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wacc 7199	wff CCHOICE
df-cc 7200	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7209	class N.
cpli 7210	class +N
cmi 7211	class .N
clti 7212	class <N
cplpq 7213	class +pQ
cmpq 7214	class .pQ
cltpq 7215	class <pQ
ceq 7216	class ~Q
cnq 7217	class Q.
c1q 7218	class 1Q
cplq 7219	class +Q
cmq 7220	class .Q
crq 7221	class *Q
cltq 7222	class <Q
ceq0 7223	class ~Q0
cnq0 7224	class Q0
c0q0 7225	class 0Q0
cplq0 7226	class +Q0
cmq0 7227	class ·Q0
cnp 7228	class P.
c1p 7229	class 1P
cpp 7230	class +P.
cmp 7231	class .P.
cltp 7232	class <P
cer 7233	class ~R
cnr 7234	class R.
c0r 7235	class 0R
c1r 7236	class 1R
cm1r 7237	class -1R
cplr 7238	class +R
cmr 7239	class .R
cltr 7240	class <R
df-ni 7241	|- N. = ( om \ { (/) } )
df-pli 7242	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7243	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7244	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7281	|- +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 7282	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7283	|- <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 7284	|- ~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 7285	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7286	|- +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 7287	|- .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 7288	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7289	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7290	|- <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 7361	|- ~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 7362	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7363	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7364	|- +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 7365	|- ·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 7403	|- 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 7404	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7405	|- +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 7406	|- .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 7407	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7663	|- ~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 7664	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7665	|- +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 7666	|- .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 7667	|- <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 7668	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7669	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7670	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 7747	class CC
cr 7748	class RR
cc0 7749	class 0
c1 7750	class 1
ci 7751	class _i
caddc 7752	class +
cltrr 7753	class <RR
cmul 7754	class x.
df-c 7755	|- CC = ( R. X. R. )
df-0 7756	|- 0 = <. 0R , 0R >.
df-1 7757	|- 1 = <. 1R , 0R >.
df-i 7758	|- _i = <. 0R , 1R >.
df-r 7759	|- RR = ( R. X. { 0R } )
df-add 7760	|- + = { <. <. 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 7761	|- 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 7762	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 7840	|- CC e. _V
ax-resscn 7841	|- RR C_ CC
ax-1cn 7842	|- 1 e. CC
ax-1re 7843	|- 1 e. RR
ax-icn 7844	|- _i e. CC
ax-addcl 7845	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 7846	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 7847	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 7848	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 7849	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 7850	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 7851	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 7852	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 7853	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 7854	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 7855	|- 0 <RR 1
ax-1rid 7856	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 7857	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 7858	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 7859	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 7860	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 7861	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 7862	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 7863	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 7864	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 7865	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 7866	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 7867	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 7868	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 7869	|- 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 7870	|- ( ( ( 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 7871	|- + : ( CC X. CC ) --> CC
ax-mulf 7872	|- x. : ( CC X. CC ) --> CC
cpnf 7926	class +oo
cmnf 7927	class -oo
cxr 7928	class RR*
clt 7929	class <
cle 7930	class <_
df-pnf 7931	|- +oo = ~P U. CC
df-mnf 7932	|- -oo = ~P +oo
df-xr 7933	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 7934	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 7935	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8065	class -
cneg 8066	class -u A
df-sub 8067	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8068	|- -u A = ( 0 - A )
creap 8468	class #ℝ
df-reap 8469	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8475	class #
df-ap 8476	|- # = { <. 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 8564	class /
df-div 8565	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 8853	class NN
df-inn 8854	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 8904	class 2
c3 8905	class 3
c4 8906	class 4
c5 8907	class 5
c6 8908	class 6
c7 8909	class 7
c8 8910	class 8
c9 8911	class 9
df-2 8912	|- 2 = ( 1 + 1 )
df-3 8913	|- 3 = ( 2 + 1 )
df-4 8914	|- 4 = ( 3 + 1 )
df-5 8915	|- 5 = ( 4 + 1 )
df-6 8916	|- 6 = ( 5 + 1 )
df-7 8917	|- 7 = ( 6 + 1 )
df-8 8918	|- 8 = ( 7 + 1 )
df-9 8919	|- 9 = ( 8 + 1 )
cn0 9110	class NN0
df-n0 9111	|- NN0 = ( NN u. { 0 } )
cxnn0 9173	class NN0*
df-xnn0 9174	|- NN0* = ( NN0 u. { +oo } )
cz 9187	class ZZ
df-z 9188	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9318	class ; A B
df-dec 9319	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9462	class ZZ>=
df-uz 9463	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9553	class QQ
df-q 9554	|- QQ = ( / " ( ZZ X. NN ) )
crp 9585	class RR+
df-rp 9586	|- RR+ = { x e. RR | 0 < x }
cxne 9701	class -e A
cxad 9702	class +e
cxmu 9703	class xe
df-xneg 9704	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9705	|- +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 9706	|- 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 9820	class (,)
cioc 9821	class (,]
cico 9822	class [,)
cicc 9823	class [,]
df-ioo 9824	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 9825	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 9826	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 9827	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 9940	class ...
df-fz 9941	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10073	class ..^
df-fzo 10074	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10199	class |_
cceil 10200	class ⌈
df-fl 10201	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10202	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10253	class mod
df-mod 10254	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10376	class seq M ( .+ , F )
df-seqfrec 10377	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10450	class ^
df-exp 10451	|- ^ = ( 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 10634	class !
df-fac 10635	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10656	class _C
df-bc 10657	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 10684	class ♯
df-ihash 10685	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cshi 10752	class shift
df-shft 10753	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 10777	class *
cre 10778	class Re
cim 10779	class Im
df-cj 10780	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 10781	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 10782	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 10934	class sqr
cabs 10935	class abs
df-rsqrt 10936	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 10937	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11215	class ~~>
df-clim 11216	|- ~~> = { <. 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 11290	class sum_ k e. A B
df-sumdc 11291	|- 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 11487	class prod_ k e. A B
df-proddc 11488	|- 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 11579	class exp
ceu 11580	class _e
csin 11581	class sin
ccos 11582	class cos
ctan 11583	class tan
cpi 11584	class pi
df-ef 11585	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 11586	|- _e = ( exp ` 1 )
df-sin 11587	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 11588	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 11589	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 11590	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 11711	class tau
df-tau 11712	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 11723	class ||
df-dvds 11724	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cgcd 11871	class gcd
df-gcd 11872	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 11988	class lcm
df-lcm 11989	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12035	class Prime
df-prm 12036	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12109	class numer
cdenom 12110	class denom
df-numer 12111	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12112	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12136	class odZ
cphi 12137	class phi
df-odz 12138	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12139	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12212	class pCnt
df-pc 12213	|- 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 12295	class ZZ[_i]
df-gz 12296	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 12386	class Struct
cnx 12387	class ndx
csts 12388	class sSet
cslot 12389	class Slot A
cbs 12390	class Base
cress 12391	class ↾s
df-struct 12392	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 12393	|- ndx = ( _I |` NN )
df-slot 12394	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 12396	|- Base = Slot 1
df-sets 12397	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-ress 12398	|- ↾s = ( w e. _V , x e. _V |-> if ( ( Base ` w ) C_ x , w , ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) ) )
cplusg 12452	class +g
cmulr 12453	class .r
cstv 12454	class *r
csca 12455	class Scalar
cvsca 12456	class .s
cip 12457	class .i
cts 12458	class TopSet
cple 12459	class le
coc 12460	class oc
cds 12461	class dist
cunif 12462	class UnifSet
chom 12463	class Hom
cco 12464	class comp
df-plusg 12465	|- +g = Slot 2
df-mulr 12466	|- .r = Slot 3
df-starv 12467	|- *r = Slot 4
df-sca 12468	|- Scalar = Slot 5
df-vsca 12469	|- .s = Slot 6
df-ip 12470	|- .i = Slot 8
df-tset 12471	|- TopSet = Slot 9
df-ple 12472	|- le = Slot ; 1 0
df-ocomp 12473	|- oc = Slot ; 1 1
df-ds 12474	|- dist = Slot ; 1 2
df-unif 12475	|- UnifSet = Slot ; 1 3
df-hom 12476	|- Hom = Slot ; 1 4
df-cco 12477	|- comp = Slot ; 1 5
crest 12551	class ↾t
ctopn 12552	class TopOpen
df-rest 12553	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 12554	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 12566	class topGen
cpt 12567	class Xt_
c0g 12568	class 0g
cgsu 12569	class gsumg
df-0g 12570	|- 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-gsum 12571	|- gsumg = ( w e. _V , f e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran f C_ o , ( 0g ` w ) , if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... (♯ ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` (♯ ` y ) ) ) ) ) ) )
df-topgen 12572	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 12573	|- 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 12574	class X_s
cpws 12575	class ^s
df-prds 12576	|- 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 12578	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cpsmet 12579	class PsMet
cxmet 12580	class *Met
cmet 12581	class Met
cbl 12582	class ball
cfbas 12583	class fBas
cfg 12584	class filGen
cmopn 12585	class MetOpen
cmetu 12586	class metUnif
df-psmet 12587	|- 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 12588	|- *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 12589	|- 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 12590	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 12591	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 12592	|- 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 12593	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 12594	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ctop 12595	class Top
df-top 12596	|- 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 12608	class TopOn
df-topon 12609	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 12628	class TopSp
df-topsp 12629	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 12640	class TopBases
df-bases 12641	|- 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 12692	class Clsd
cnt 12693	class int
ccl 12694	class cls
df-cld 12695	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 12696	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 12697	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 12738	class nei
df-nei 12739	|- 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 12785	class Cn
ccnp 12786	class CnP
clm 12787	class ~~> t
df-cn 12788	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 12789	|- 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 12790	|- ~~> 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 12852	class tX
df-tx 12853	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 12900	class Homeo
df-hmeo 12901	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 12936	class *MetSp
cms 12937	class MetSp
ctms 12938	class toMetSp
df-xms 12939	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 12940	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 12941	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 13157	class -cn->
df-cncf 13158	|- -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 13223	class lim CC
cdv 13224	class _D
df-limced 13225	|- 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 13226	|- _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 ) ) )
clog 13377	class log
ccxp 13378	class ^c
df-relog 13379	|- log = `' ( exp |` RR )
df-rpcxp 13380	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 13461	class logb
df-logb 13462	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
clgs 13498	class /L
df-lgs 13499	|- /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 13634	wff A DECIDin B
df-dcin 13635	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 13654	wff BOUNDED ph
ax-bd0 13655	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 13656	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 13657	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 13658	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 13659	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 13660	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 13661	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 13662	|- BOUNDED x = y
ax-bdel 13663	|- BOUNDED x e. y
ax-bdsb 13664	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 13682	wff BOUNDED A
df-bdc 13683	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 13726	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 13766	|- BOUNDED ph   =>    |- DECID ph
wind 13768	wff Ind A
df-bj-ind 13769	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 13783	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 13810	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 13818	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 13824	|- 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 13829	|- 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 13831	|- ( ( ( 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 13912	wff A.! x ( ph -> ps )
walsc 13913	wff A.! x e. A ph
df-alsi 13914	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 13915	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )