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 603	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 604	|- ( -. ph -> ( ph -> ps ) )
wo 697	wff ( ph \/ ps )
ax-io 698	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 815	wff STAB ph
df-stab 816	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 819	wff DECID ph
df-dc 820	|- (DECID ph <-> ( ph \/ -. ph ) )
w3o 961	wff ( ph \/ ps \/ ch )
w3a 962	wff ( ph /\ ps /\ ch )
df-3or 963	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 964	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1329	wff A. x ph
cv 1330	class x
wceq 1331	wff A = B
wtru 1332	wff T.
df-tru 1334	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1336	wff F.
df-fal 1337	|- ( F. <-> -. T. )
wxo 1353	wff ( ph \/_ ps )
df-xor 1354	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1423	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1424	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1425	|- ph   =>    |- A. x ph
wnf 1436	wff F/ x ph
df-nf 1437	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1468	wff E. x ph
ax-ie1 1469	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1470	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
wcel 1480	wff A e. B
ax-8 1482	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1483	|- ( A. x x = y -> A. y y = x )
ax-11 1484	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1485	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1486	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1487	|- ( A. x ph -> ph )
ax-13 1491	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 1492	|- ( x = y -> ( z e. x -> z e. y ) )
ax-17 1506	|- ( ph -> A. x ph )
ax-i9 1510	|- E. x x = y
ax-ial 1514	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1515	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1694	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1735	wff [ y / x ] ph
df-sb 1736	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1786	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1795	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 1999	wff E! x ph
wmo 2000	wff E* x ph
df-eu 2002	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2003	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
ax-ext 2121	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2125	class { x | ph }
df-clab 2126	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2132	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2135	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2268	wff F/_ x A
df-nfc 2270	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2308	wff A =/= B
df-ne 2309	|- ( A =/= B <-> -. A = B )
wnel 2403	wff A e/ B
df-nel 2404	|- ( A e/ B <-> -. A e. B )
wral 2416	wff A. x e. A ph
wrex 2417	wff E. x e. A ph
wreu 2418	wff E! x e. A ph
wrmo 2419	wff E* x e. A ph
crab 2420	class { x e. A | ph }
df-ral 2421	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2422	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2423	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2424	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2425	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2686	class _V
df-v 2688	|- _V = { x | x = x }
wcdeq 2892	wff CondEq ( x = y -> ph )
df-cdeq 2893	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 2909	wff [. A / x ]. ph
df-sbc 2910	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3003	class [_ A / x ]_ B
df-csb 3004	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3068	class ( A \ B )
cun 3069	class ( A u. B )
cin 3070	class ( A i^i B )
wss 3071	wff A C_ B
df-dif 3073	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3075	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3077	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3084	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3363	class (/)
df-nul 3364	|- (/) = ( _V \ _V )
cif 3474	class if ( ph , A , B )
df-if 3475	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3510	class ~P A
df-pw 3512	|- ~P A = { x | x C_ A }
csn 3527	class { A }
cpr 3528	class { A , B }
ctp 3529	class { A , B , C }
cop 3530	class <. A , B >.
cotp 3531	class <. A , B , C >.
df-sn 3533	|- { A } = { x | x = A }
df-pr 3534	|- { A , B } = ( { A } u. { B } )
df-tp 3535	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3536	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3537	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3736	class U. A
df-uni 3737	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3771	class |^| A
df-int 3772	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3813	class U_ x e. A B
ciin 3814	class |^|_ x e. A B
df-iun 3815	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3816	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 3906	wff Disj x e. A B
df-disj 3907	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 3929	wff A R B
df-br 3930	|- ( A R B <-> <. A , B >. e. R )
copab 3988	class { <. x , y >. | ph }
cmpt 3989	class ( x e. A |-> B )
df-opab 3990	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 3991	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4026	wff Tr A
df-tr 4027	|- ( Tr A <-> U. A C_ A )
ax-coll 4043	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4046	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4054	|- E. x A. y -. y e. x
ax-pow 4098	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4118	wff EXMID
df-exmid 4119	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4131	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4209	class _E
cid 4210	class _I
df-eprel 4211	|- _E = { <. x , y >. | x e. y }
df-id 4215	|- _I = { <. x , y >. | x = y }
wpo 4216	wff R Po A
wor 4217	wff R Or A
df-po 4218	|- ( 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 4219	|- ( 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 4249	wff FrFor R A S
wfr 4250	wff R Fr A
wse 4251	wff R Se A
wwe 4252	wff R We A
df-frfor 4253	|- (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 4254	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4255	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4256	|- ( 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 4284	wff Ord A
con0 4285	class On
wlim 4286	wff Lim A
csuc 4287	class suc A
df-iord 4288	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4290	|- On = { x | Ord x }
df-ilim 4291	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4293	|- suc A = ( A u. { A } )
ax-un 4355	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4452	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4502	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4504	class om
df-iom 4505	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4537	class ( A X. B )
ccnv 4538	class `' A
cdm 4539	class dom A
crn 4540	class ran A
cres 4541	class ( A |` B )
cima 4542	class ( A " B )
ccom 4543	class ( A o. B )
wrel 4544	wff Rel A
df-xp 4545	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4546	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4547	|- `' A = { <. x , y >. | y A x }
df-co 4548	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4549	|- dom A = { x | E. y x A y }
df-rn 4550	|- ran A = dom `' A
df-res 4551	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4552	|- ( A " B ) = ran ( A |` B )
cio 5086	class ( iota x ph )
df-iota 5088	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5117	wff Fun A
wfn 5118	wff A Fn B
wf 5119	wff F : A --> B
wf1 5120	wff F : A -1-1-> B
wfo 5121	wff F : A -onto-> B
wf1o 5122	wff F : A -1-1-onto-> B
cfv 5123	class ( F ` A )
wiso 5124	wff H Isom R , S ( A , B )
df-fun 5125	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5126	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5127	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5128	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5129	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5130	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5131	|- ( F ` A ) = ( iota x A F x )
df-isom 5132	|- ( 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 5729	class ( iota_ x e. A ph )
df-riota 5730	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 5774	class ( A F B )
coprab 5775	class { <. <. x , y >. , z >. | ph }
cmpo 5776	class ( x e. A , y e. B |-> C )
df-ov 5777	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 5778	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 5779	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 5980	class oF R
cofr 5981	class oR R
df-of 5982	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 5983	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6036	class 1st
c2nd 6037	class 2nd
df-1st 6038	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6039	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6141	class tpos F
df-tpos 6142	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6182	wff Smo A
df-smo 6183	|- ( 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 6201	class recs ( F )
df-recs 6202	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6266	class rec ( F , I )
df-irdg 6267	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6287	class frec ( F , I )
df-frec 6288	|- 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 6306	class 1o
c2o 6307	class 2o
c3o 6308	class 3o
c4o 6309	class 4o
coa 6310	class +o
comu 6311	class .o
coei 6312	class ↑o
df-1o 6313	|- 1o = suc (/)
df-2o 6314	|- 2o = suc 1o
df-3o 6315	|- 3o = suc 2o
df-4o 6316	|- 4o = suc 3o
df-oadd 6317	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6318	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6319	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6426	wff R Er A
cec 6427	class [ A ] R
cqs 6428	class ( A /. R )
df-er 6429	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6431	|- [ A ] R = ( R " { A } )
df-qs 6435	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6542	class ^m
cpm 6543	class ^pm
df-map 6544	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6545	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6592	class X_ x e. A B
df-ixp 6593	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6632	class ~~
cdom 6633	class ~<_
cfn 6634	class Fin
df-en 6635	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6636	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6637	|- Fin = { x | E. y e. om x ~~ y }
cfi 6856	class fi
df-fi 6857	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 6869	class sup ( A , B , R )
cinf 6870	class inf ( A , B , R )
df-sup 6871	|- 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 6872	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 6922	class ( A ⊔ B )
df-dju 6923	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 6930	class inl
cinr 6931	class inr
df-inl 6932	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 6933	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 6968	class case ( R , S )
df-case 6969	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 6987	class ( R ⊔d S )
df-djud 6988	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
comni 7004	class Omni
xnninf 7005	class ℕ∞
df-omni 7006	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
df-nninf 7007	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
cmarkov 7025	class Markov
df-markov 7026	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
ccrd 7035	class card
df-card 7036	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
wac 7061	wff CHOICE
df-ac 7062	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wacc 7077	wff CCHOICE
df-cc 7078	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7080	class N.
cpli 7081	class +N
cmi 7082	class .N
clti 7083	class <N
cplpq 7084	class +pQ
cmpq 7085	class .pQ
cltpq 7086	class <pQ
ceq 7087	class ~Q
cnq 7088	class Q.
c1q 7089	class 1Q
cplq 7090	class +Q
cmq 7091	class .Q
crq 7092	class *Q
cltq 7093	class <Q
ceq0 7094	class ~Q0
cnq0 7095	class Q0
c0q0 7096	class 0Q0
cplq0 7097	class +Q0
cmq0 7098	class ·Q0
cnp 7099	class P.
c1p 7100	class 1P
cpp 7101	class +P.
cmp 7102	class .P.
cltp 7103	class <P
cer 7104	class ~R
cnr 7105	class R.
c0r 7106	class 0R
c1r 7107	class 1R
cm1r 7108	class -1R
cplr 7109	class +R
cmr 7110	class .R
cltr 7111	class <R
df-ni 7112	|- N. = ( om \ { (/) } )
df-pli 7113	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7114	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7115	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7152	|- +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 7153	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7154	|- <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 7155	|- ~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 7156	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7157	|- +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 7158	|- .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 7159	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7160	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7161	|- <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 7232	|- ~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 7233	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7234	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7235	|- +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 7236	|- ·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 7274	|- 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 7275	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7276	|- +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 7277	|- .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 7278	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7534	|- ~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 7535	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7536	|- +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 7537	|- .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 7538	|- <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 7539	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7540	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7541	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 7618	class CC
cr 7619	class RR
cc0 7620	class 0
c1 7621	class 1
ci 7622	class _i
caddc 7623	class +
cltrr 7624	class <RR
cmul 7625	class x.
df-c 7626	|- CC = ( R. X. R. )
df-0 7627	|- 0 = <. 0R , 0R >.
df-1 7628	|- 1 = <. 1R , 0R >.
df-i 7629	|- _i = <. 0R , 1R >.
df-r 7630	|- RR = ( R. X. { 0R } )
df-add 7631	|- + = { <. <. 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 7632	|- 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 7633	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 7711	|- CC e. _V
ax-resscn 7712	|- RR C_ CC
ax-1cn 7713	|- 1 e. CC
ax-1re 7714	|- 1 e. RR
ax-icn 7715	|- _i e. CC
ax-addcl 7716	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 7717	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 7718	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 7719	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 7720	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 7721	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 7722	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 7723	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 7724	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 7725	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 7726	|- 0 <RR 1
ax-1rid 7727	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 7728	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 7729	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 7730	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 7731	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 7732	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 7733	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 7734	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 7735	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 7736	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 7737	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 7738	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 7739	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 7740	|- 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 7741	|- ( ( ( 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 7742	|- + : ( CC X. CC ) --> CC
ax-mulf 7743	|- x. : ( CC X. CC ) --> CC
cpnf 7797	class +oo
cmnf 7798	class -oo
cxr 7799	class RR*
clt 7800	class <
cle 7801	class <_
df-pnf 7802	|- +oo = ~P U. CC
df-mnf 7803	|- -oo = ~P +oo
df-xr 7804	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 7805	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 7806	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 7933	class -
cneg 7934	class -u A
df-sub 7935	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 7936	|- -u A = ( 0 - A )
creap 8336	class #ℝ
df-reap 8337	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8343	class #
df-ap 8344	|- # = { <. 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 8432	class /
df-div 8433	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 8720	class NN
df-inn 8721	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 8771	class 2
c3 8772	class 3
c4 8773	class 4
c5 8774	class 5
c6 8775	class 6
c7 8776	class 7
c8 8777	class 8
c9 8778	class 9
df-2 8779	|- 2 = ( 1 + 1 )
df-3 8780	|- 3 = ( 2 + 1 )
df-4 8781	|- 4 = ( 3 + 1 )
df-5 8782	|- 5 = ( 4 + 1 )
df-6 8783	|- 6 = ( 5 + 1 )
df-7 8784	|- 7 = ( 6 + 1 )
df-8 8785	|- 8 = ( 7 + 1 )
df-9 8786	|- 9 = ( 8 + 1 )
cn0 8977	class NN0
df-n0 8978	|- NN0 = ( NN u. { 0 } )
cxnn0 9040	class NN0*
df-xnn0 9041	|- NN0* = ( NN0 u. { +oo } )
cz 9054	class ZZ
df-z 9055	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9182	class ; A B
df-dec 9183	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9326	class ZZ>=
df-uz 9327	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9411	class QQ
df-q 9412	|- QQ = ( / " ( ZZ X. NN ) )
crp 9441	class RR+
df-rp 9442	|- RR+ = { x e. RR | 0 < x }
cxne 9556	class -e A
cxad 9557	class +e
cxmu 9558	class xe
df-xneg 9559	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9560	|- +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 9561	|- 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 9671	class (,)
cioc 9672	class (,]
cico 9673	class [,)
cicc 9674	class [,]
df-ioo 9675	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 9676	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 9677	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 9678	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 9790	class ...
df-fz 9791	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 9919	class ..^
df-fzo 9920	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10041	class |_
cceil 10042	class ⌈
df-fl 10043	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10044	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10095	class mod
df-mod 10096	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10218	class seq M ( .+ , F )
df-seqfrec 10219	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10292	class ^
df-exp 10293	|- ^ = ( 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 10471	class !
df-fac 10472	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10493	class _C
df-bc 10494	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 10521	class ♯
df-ihash 10522	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cshi 10586	class shift
df-shft 10587	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 10611	class *
cre 10612	class Re
cim 10613	class Im
df-cj 10614	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 10615	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 10616	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 10768	class sqr
cabs 10769	class abs
df-rsqrt 10770	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 10771	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11047	class ~~>
df-clim 11048	|- ~~> = { <. 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 11122	class sum_ k e. A B
df-sumdc 11123	|- 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 11319	class prod_ k e. A B
df-proddc 11320	|- 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 11348	class exp
ceu 11349	class _e
csin 11350	class sin
ccos 11351	class cos
ctan 11352	class tan
cpi 11353	class pi
df-ef 11354	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 11355	|- _e = ( exp ` 1 )
df-sin 11356	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 11357	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 11358	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 11359	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 11481	class tau
df-tau 11482	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 11493	class ||
df-dvds 11494	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cgcd 11635	class gcd
df-gcd 11636	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 11741	class lcm
df-lcm 11742	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 11788	class Prime
df-prm 11789	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 11859	class numer
cdenom 11860	class denom
df-numer 11861	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 11862	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
cphi 11886	class phi
df-phi 11887	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cstr 11955	class Struct
cnx 11956	class ndx
csts 11957	class sSet
cslot 11958	class Slot A
cbs 11959	class Base
cress 11960	class ↾s
df-struct 11961	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 11962	|- ndx = ( _I |` NN )
df-slot 11963	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 11965	|- Base = Slot 1
df-sets 11966	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-ress 11967	|- ↾s = ( w e. _V , x e. _V |-> if ( ( Base ` w ) C_ x , w , ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) ) )
cplusg 12021	class +g
cmulr 12022	class .r
cstv 12023	class *r
csca 12024	class Scalar
cvsca 12025	class .s
cip 12026	class .i
cts 12027	class TopSet
cple 12028	class le
coc 12029	class oc
cds 12030	class dist
cunif 12031	class UnifSet
chom 12032	class Hom
cco 12033	class comp
df-plusg 12034	|- +g = Slot 2
df-mulr 12035	|- .r = Slot 3
df-starv 12036	|- *r = Slot 4
df-sca 12037	|- Scalar = Slot 5
df-vsca 12038	|- .s = Slot 6
df-ip 12039	|- .i = Slot 8
df-tset 12040	|- TopSet = Slot 9
df-ple 12041	|- le = Slot ; 1 0
df-ocomp 12042	|- oc = Slot ; 1 1
df-ds 12043	|- dist = Slot ; 1 2
df-unif 12044	|- UnifSet = Slot ; 1 3
df-hom 12045	|- Hom = Slot ; 1 4
df-cco 12046	|- comp = Slot ; 1 5
crest 12120	class ↾t
ctopn 12121	class TopOpen
df-rest 12122	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 12123	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 12135	class topGen
cpt 12136	class Xt_
c0g 12137	class 0g
cgsu 12138	class gsumg
df-0g 12139	|- 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 12140	|- 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 12141	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 12142	|- 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 12143	class X_s
cpws 12144	class ^s
df-prds 12145	|- 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 12147	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cpsmet 12148	class PsMet
cxmet 12149	class *Met
cmet 12150	class Met
cbl 12151	class ball
cfbas 12152	class fBas
cfg 12153	class filGen
cmopn 12154	class MetOpen
cmetu 12155	class metUnif
df-psmet 12156	|- 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 12157	|- *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 12158	|- 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 12159	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 12160	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 12161	|- 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 12162	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 12163	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ctop 12164	class Top
df-top 12165	|- 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 12177	class TopOn
df-topon 12178	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 12197	class TopSp
df-topsp 12198	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 12209	class TopBases
df-bases 12210	|- 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 12261	class Clsd
cnt 12262	class int
ccl 12263	class cls
df-cld 12264	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 12265	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 12266	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 12307	class nei
df-nei 12308	|- 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 12354	class Cn
ccnp 12355	class CnP
clm 12356	class ~~> t
df-cn 12357	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 12358	|- 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 12359	|- ~~> 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 12421	class tX
df-tx 12422	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 12469	class Homeo
df-hmeo 12470	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 12505	class *MetSp
cms 12506	class MetSp
ctms 12507	class toMetSp
df-xms 12508	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 12509	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 12510	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 12726	class -cn->
df-cncf 12727	|- -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 12792	class lim CC
cdv 12793	class _D
df-limced 12794	|- 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 12795	|- _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 ) ) )
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 13000	wff A DECIDin B
df-dcin 13001	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 13010	wff BOUNDED ph
ax-bd0 13011	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 13012	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 13013	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 13014	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 13015	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 13016	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 13017	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 13018	|- BOUNDED x = y
ax-bdel 13019	|- BOUNDED x e. y
ax-bdsb 13020	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 13038	wff BOUNDED A
df-bdc 13039	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 13082	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 13122	|- BOUNDED ph   =>    |- DECID ph
wind 13124	wff Ind A
df-bj-ind 13125	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 13139	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 13166	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 13174	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 13180	|- A. a ( A. x e. a E. y ph -> E. b A. y ( y e. b <-> E. x e. a ph ) )
ax-sscoll 13185	|- A. a A. b E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c A. y ( y e. d <-> E. x e. a ph ) )
ax-ddkcomp 13187	|- ( ( ( 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 13242	wff A.! x ( ph -> ps )
walsc 13243	wff A.! x e. A ph
df-alsi 13244	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 13245	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )