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-1 5	|- ( ph -> ( ps -> ph ) )
ax-2 6	|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
ax-mp 7	|- ph   &    |- ( ph -> ps )   =>    |- ps
wa 102	wff ( ph /\ ps )
wb 103	wff ( ph <-> ps )
ax-ia1 104	|- ( ( ph /\ ps ) -> ph )
ax-ia2 105	|- ( ( ph /\ ps ) -> ps )
ax-ia3 106	|- ( ph -> ( ps -> ( ph /\ ps ) ) )
df-bi 115	|- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
ax-in1 576	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 577	|- ( -. ph -> ( ph -> ps ) )
wo 661	wff ( ph \/ ps )
ax-io 662	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 772	wff STAB ph
df-stab 773	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 775	wff DECID ph
df-dc 776	|- (DECID ph <-> ( ph \/ -. ph ) )
w3o 918	wff ( ph \/ ps \/ ch )
w3a 919	wff ( ph /\ ps /\ ch )
df-3or 920	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 921	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1282	wff A. x ph
cv 1283	class x
wceq 1284	wff A = B
wtru 1285	wff T.
df-tru 1287	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1289	wff F.
df-fal 1290	|- ( F. <-> -. T. )
wxo 1306	wff ( ph \/_ ps )
df-xor 1307	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1376	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1377	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1378	|- ph   =>    |- A. x ph
wnf 1389	wff F/ x ph
df-nf 1390	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1421	wff E. x ph
ax-ie1 1422	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1423	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
wcel 1433	wff A e. B
ax-8 1435	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1436	|- ( A. x x = y -> A. y y = x )
ax-11 1437	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1438	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1439	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1440	|- ( A. x ph -> ph )
ax-13 1444	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 1445	|- ( x = y -> ( z e. x -> z e. y ) )
ax-17 1459	|- ( ph -> A. x ph )
ax-i9 1463	|- E. x x = y
ax-ial 1467	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1468	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1644	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1685	wff [ y / x ] ph
df-sb 1686	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1735	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1744	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 1941	wff E! x ph
wmo 1942	wff E* x ph
df-eu 1944	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 1945	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
ax-ext 2063	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2067	class { x | ph }
df-clab 2068	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2074	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2077	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2206	wff F/_ x A
df-nfc 2208	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2245	wff A =/= B
df-ne 2246	|- ( A =/= B <-> -. A = B )
wnel 2339	wff A e/ B
df-nel 2340	|- ( A e/ B <-> -. A e. B )
wral 2348	wff A. x e. A ph
wrex 2349	wff E. x e. A ph
wreu 2350	wff E! x e. A ph
wrmo 2351	wff E* x e. A ph
crab 2352	class { x e. A | ph }
df-ral 2353	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2354	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2355	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2356	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2357	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2601	class _V
df-v 2603	|- _V = { x | x = x }
wcdeq 2798	wff CondEq ( x = y -> ph )
df-cdeq 2799	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 2815	wff [. A / x ]. ph
df-sbc 2816	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 2908	class [_ A / x ]_ B
df-csb 2909	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 2970	class ( A \ B )
cun 2971	class ( A u. B )
cin 2972	class ( A i^i B )
wss 2973	wff A C_ B
df-dif 2975	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 2977	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 2979	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 2986	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3251	class (/)
df-nul 3252	|- (/) = ( _V \ _V )
cif 3351	class if ( ph , A , B )
df-if 3352	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3382	class ~P A
df-pw 3384	|- ~P A = { x | x C_ A }
csn 3398	class { A }
cpr 3399	class { A , B }
ctp 3400	class { A , B , C }
cop 3401	class <. A , B >.
cotp 3402	class <. A , B , C >.
df-sn 3404	|- { A } = { x | x = A }
df-pr 3405	|- { A , B } = ( { A } u. { B } )
df-tp 3406	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3407	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3408	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3601	class U. A
df-uni 3602	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3636	class |^| A
df-int 3637	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3678	class U_ x e. A B
ciin 3679	class |^|_ x e. A B
df-iun 3680	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3681	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 3766	wff Disj x e. A B
df-disj 3767	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 3785	wff A R B
df-br 3786	|- ( A R B <-> <. A , B >. e. R )
copab 3838	class { <. x , y >. | ph }
cmpt 3839	class ( x e. A |-> B )
df-opab 3840	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 3841	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 3875	wff Tr A
df-tr 3876	|- ( Tr A <-> U. A C_ A )
ax-coll 3893	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 3896	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 3904	|- E. x A. y -. y e. x
ax-pow 3948	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
ax-pr 3964	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4042	class _E
cid 4043	class _I
df-eprel 4044	|- _E = { <. x , y >. | x e. y }
df-id 4048	|- _I = { <. x , y >. | x = y }
wpo 4049	wff R Po A
wor 4050	wff R Or A
df-po 4051	|- ( 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 4052	|- ( 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 4082	wff FrFor R A S
wfr 4083	wff R Fr A
wse 4084	wff R Se A
wwe 4085	wff R We A
df-frfor 4086	|- (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 4087	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4088	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4089	|- ( 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 4117	wff Ord A
con0 4118	class On
wlim 4119	wff Lim A
csuc 4120	class suc A
df-iord 4121	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4123	|- On = { x | Ord x }
df-ilim 4124	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4126	|- suc A = ( A u. { A } )
ax-un 4188	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4280	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4329	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4331	class om
df-iom 4332	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4361	class ( A X. B )
ccnv 4362	class `' A
cdm 4363	class dom A
crn 4364	class ran A
cres 4365	class ( A |` B )
cima 4366	class ( A " B )
ccom 4367	class ( A o. B )
wrel 4368	wff Rel A
df-xp 4369	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4370	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4371	|- `' A = { <. x , y >. | y A x }
df-co 4372	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4373	|- dom A = { x | E. y x A y }
df-rn 4374	|- ran A = dom `' A
df-res 4375	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4376	|- ( A " B ) = ran ( A |` B )
cio 4885	class ( iota x ph )
df-iota 4887	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 4916	wff Fun A
wfn 4917	wff A Fn B
wf 4918	wff F : A --> B
wf1 4919	wff F : A -1-1-> B
wfo 4920	wff F : A -onto-> B
wf1o 4921	wff F : A -1-1-onto-> B
cfv 4922	class ( F ` A )
wiso 4923	wff H Isom R , S ( A , B )
df-fun 4924	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 4925	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 4926	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 4927	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 4928	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 4929	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 4930	|- ( F ` A ) = ( iota x A F x )
df-isom 4931	|- ( 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 5487	class ( iota_ x e. A ph )
df-riota 5488	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 5532	class ( A F B )
coprab 5533	class { <. <. x , y >. , z >. | ph }
cmpt2 5534	class ( x e. A , y e. B |-> C )
df-ov 5535	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 5536	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpt2 5537	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 5730	class oF R
cofr 5731	class oR R
df-of 5732	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 5733	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 5785	class 1st
c2nd 5786	class 2nd
df-1st 5787	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 5788	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 5882	class tpos F
df-tpos 5883	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 5923	wff Smo A
df-smo 5924	|- ( 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 5942	class recs ( F )
df-recs 5943	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 5979	class rec ( F , I )
df-irdg 5980	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6000	class frec ( F , I )
df-frec 6001	|- 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 6017	class 1o
c2o 6018	class 2o
c3o 6019	class 3o
c4o 6020	class 4o
coa 6021	class +o
comu 6022	class .o
coei 6023	class ↑𝑜
df-1o 6024	|- 1o = suc (/)
df-2o 6025	|- 2o = suc 1o
df-3o 6026	|- 3o = suc 2o
df-4o 6027	|- 4o = suc 3o
df-oadd 6028	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6029	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6030	|- ↑𝑜 = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6126	wff R Er A
cec 6127	class [ A ] R
cqs 6128	class ( A /. R )
df-er 6129	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6131	|- [ A ] R = ( R " { A } )
df-qs 6135	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cen 6242	class ~~
cdom 6243	class ~<_
cfn 6244	class Fin
df-en 6245	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6246	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6247	|- Fin = { x | E. y e. om x ~~ y }
csup 6395	class sup ( A , B , R )
cinf 6396	class inf ( A , B , R )
df-sup 6397	|- 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 6398	|- inf ( A , B , R ) = sup ( A , B , `' R )
ccrd 6448	class card
df-card 6449	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
cnpi 6462	class N.
cpli 6463	class +N
cmi 6464	class .N
clti 6465	class <N
cplpq 6466	class +pQ
cmpq 6467	class .pQ
cltpq 6468	class <pQ
ceq 6469	class ~Q
cnq 6470	class Q.
c1q 6471	class 1Q
cplq 6472	class +Q
cmq 6473	class .Q
crq 6474	class *Q
cltq 6475	class <Q
ceq0 6476	class ~Q0
cnq0 6477	class Q0
c0q0 6478	class 0Q0
cplq0 6479	class +Q0
cmq0 6480	class ·Q0
cnp 6481	class P.
c1p 6482	class 1P
cpp 6483	class +P.
cmp 6484	class .P.
cltp 6485	class <P
cer 6486	class ~R
cnr 6487	class R.
c0r 6488	class 0R
c1r 6489	class 1R
cm1r 6490	class -1R
cplr 6491	class +R
cmr 6492	class .R
cltr 6493	class <R
df-ni 6494	|- N. = ( om \ { (/) } )
df-pli 6495	|- +N = ( +o |` ( N. X. N. ) )
df-mi 6496	|- .N = ( .o |` ( N. X. N. ) )
df-lti 6497	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 6534	|- +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 6535	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 6536	|- <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 6537	|- ~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 6538	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 6539	|- +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 6540	|- .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 6541	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 6542	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 6543	|- <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 6614	|- ~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 6615	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 6616	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 6617	|- +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 6618	|- ·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 6656	|- 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 6657	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 6658	|- +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 6659	|- .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 6660	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 6903	|- ~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 6904	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 6905	|- +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 6906	|- .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 6907	|- <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 6908	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 6909	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 6910	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 6979	class CC
cr 6980	class RR
cc0 6981	class 0
c1 6982	class 1
ci 6983	class _i
caddc 6984	class +
cltrr 6985	class <RR
cmul 6986	class x.
df-c 6987	|- CC = ( R. X. R. )
df-0 6988	|- 0 = <. 0R , 0R >.
df-1 6989	|- 1 = <. 1R , 0R >.
df-i 6990	|- _i = <. 0R , 1R >.
df-r 6991	|- RR = ( R. X. { 0R } )
df-add 6992	|- + = { <. <. 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 6993	|- 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 6994	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 7067	|- CC e. _V
ax-resscn 7068	|- RR C_ CC
ax-1cn 7069	|- 1 e. CC
ax-1re 7070	|- 1 e. RR
ax-icn 7071	|- _i e. CC
ax-addcl 7072	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 7073	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 7074	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 7075	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 7076	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 7077	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 7078	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 7079	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 7080	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 7081	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 7082	|- 0 <RR 1
ax-1rid 7083	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 7084	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 7085	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 7086	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 7087	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 7088	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 7089	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 7090	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 7091	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 7092	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 7093	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 7094	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 7095	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 7096	|- 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 ) ) ) ) )
cpnf 7150	class +oo
cmnf 7151	class -oo
cxr 7152	class RR*
clt 7153	class <
cle 7154	class <_
df-pnf 7155	|- +oo = ~P U. CC
df-mnf 7156	|- -oo = ~P +oo
df-xr 7157	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 7158	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 7159	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 7279	class -
cneg 7280	class -u A
df-sub 7281	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 7282	|- -u A = ( 0 - A )
creap 7674	class #ℝ
df-reap 7675	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 7681	class #
df-ap 7682	|- # = { <. 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 7760	class /
df-div 7761	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 8039	class NN
df-inn 8040	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 8089	class 2
c3 8090	class 3
c4 8091	class 4
c5 8092	class 5
c6 8093	class 6
c7 8094	class 7
c8 8095	class 8
c9 8096	class 9
c10 8097	class 10
df-2 8098	|- 2 = ( 1 + 1 )
df-3 8099	|- 3 = ( 2 + 1 )
df-4 8100	|- 4 = ( 3 + 1 )
df-5 8101	|- 5 = ( 4 + 1 )
df-6 8102	|- 6 = ( 5 + 1 )
df-7 8103	|- 7 = ( 6 + 1 )
df-8 8104	|- 8 = ( 7 + 1 )
df-9 8105	|- 9 = ( 8 + 1 )
cn0 8288	class NN0
df-n0 8289	|- NN0 = ( NN u. { 0 } )
cz 8351	class ZZ
df-z 8352	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 8477	class ; A B
df-dec 8478	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 8619	class ZZ>=
df-uz 8620	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 8704	class QQ
df-q 8705	|- QQ = ( / " ( ZZ X. NN ) )
crp 8734	class RR+
df-rp 8735	|- RR+ = { x e. RR | 0 < x }
cxne 8840	class -e A
cxad 8841	class +e
cxmu 8842	class xe
df-xneg 8843	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 8844	|- +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 8845	|- 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 8911	class (,)
cioc 8912	class (,]
cico 8913	class [,)
cicc 8914	class [,]
df-ioo 8915	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 8916	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 8917	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 8918	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 9029	class ...
df-fz 9030	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 9152	class ..^
df-fzo 9153	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 9272	class |_
cceil 9273	class ⌈
df-fl 9274	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 9275	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 9324	class mod
df-mod 9325	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 9431	class seq M ( .+ , F , S )
df-iseq 9432	|- seq M ( .+ , F , S ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 9475	class ^
df-iexp 9476	|- ^ = ( x e. CC , y e. ZZ |-> if ( y = 0 , 1 , if ( 0 < y , ( seq 1 ( x. , ( NN X. { x } ) , CC ) ` y ) , ( 1 / ( seq 1 ( x. , ( NN X. { x } ) , CC ) ` -u y ) ) ) ) )
cfa 9652	class !
df-fac 9653	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I , CC ) )
cbc 9674	class _C
df-bc 9675	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
cshi 9702	class shift
df-shft 9703	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 9726	class *
cre 9727	class Re
cim 9728	class Im
df-cj 9729	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 9730	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 9731	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 9882	class sqr
cabs 9883	class abs
df-rsqrt 9884	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 9885	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 10117	class ~~>
df-clim 10118	|- ~~> = { <. 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 10190	class sum_ k e. A B
df-sum 10191	|- sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) , CC ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` m ) ) ) )
cdvds 10195	class ||
df-dvds 10196	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cgcd 10338	class gcd
df-gcd 10339	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 10442	class lcm
df-lcm 10443	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 10489	class Prime
df-prm 10490	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wbd 10603	wff BOUNDED ph
ax-bd0 10604	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 10605	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 10606	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 10607	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 10608	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 10609	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 10610	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 10611	|- BOUNDED x = y
ax-bdel 10612	|- BOUNDED x e. y
ax-bdsb 10613	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 10631	wff BOUNDED A
df-bdc 10632	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 10675	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 10715	|- BOUNDED ph   =>    |- DECID ph
wind 10721	wff Ind A
df-bj-ind 10722	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 10736	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 10763	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 10771	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 10777	|- A. a ( A. x e. a E. y ph -> E. b A. y ( y e. b <-> E. x e. a ph ) )
ax-sscoll 10782	|- 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 10784	|- ( ( ( 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 10787	wff A.! x ( ph -> ps )
walsc 10788	wff A.! x e. A ph
df-alsi 10789	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 10790	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )