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 609	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 610	|- ( -. ph -> ( ph -> ps ) )
wo 703	wff ( ph \/ ps )
ax-io 704	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 825	wff STAB ph
df-stab 826	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 829	wff DECID ph
df-dc 830	|- (DECID ph <-> ( ph \/ -. ph ) )
w3o 972	wff ( ph \/ ps \/ ch )
w3a 973	wff ( ph /\ ps /\ ch )
df-3or 974	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 975	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1346	wff A. x ph
cv 1347	class x
wceq 1348	wff A = B
wtru 1349	wff T.
df-tru 1351	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1353	wff F.
df-fal 1354	|- ( F. <-> -. T. )
wxo 1370	wff ( ph \/_ ps )
df-xor 1371	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1440	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1441	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1442	|- ph   =>    |- A. x ph
wnf 1453	wff F/ x ph
df-nf 1454	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1485	wff E. x ph
ax-ie1 1486	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1487	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1497	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1498	|- ( A. x x = y -> A. y y = x )
ax-11 1499	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1500	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1502	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1503	|- ( A. x ph -> ph )
ax-17 1519	|- ( ph -> A. x ph )
ax-i9 1523	|- E. x x = y
ax-ial 1527	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1528	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1709	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1755	wff [ y / x ] ph
df-sb 1756	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1807	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1816	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2019	wff E! x ph
wmo 2020	wff E* x ph
df-eu 2022	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2023	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2141	wff A e. B
ax-13 2143	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2144	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2152	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2156	class { x | ph }
df-clab 2157	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2163	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2166	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2299	wff F/_ x A
df-nfc 2301	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2340	wff A =/= B
df-ne 2341	|- ( A =/= B <-> -. A = B )
wnel 2435	wff A e/ B
df-nel 2436	|- ( A e/ B <-> -. A e. B )
wral 2448	wff A. x e. A ph
wrex 2449	wff E. x e. A ph
wreu 2450	wff E! x e. A ph
wrmo 2451	wff E* x e. A ph
crab 2452	class { x e. A | ph }
df-ral 2453	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2454	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2455	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2456	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2457	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2730	class _V
df-v 2732	|- _V = { x | x = x }
wcdeq 2938	wff CondEq ( x = y -> ph )
df-cdeq 2939	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 2955	wff [. A / x ]. ph
df-sbc 2956	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3049	class [_ A / x ]_ B
df-csb 3050	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3118	class ( A \ B )
cun 3119	class ( A u. B )
cin 3120	class ( A i^i B )
wss 3121	wff A C_ B
df-dif 3123	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3125	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3127	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3134	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3414	class (/)
df-nul 3415	|- (/) = ( _V \ _V )
cif 3526	class if ( ph , A , B )
df-if 3527	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3566	class ~P A
df-pw 3568	|- ~P A = { x | x C_ A }
csn 3583	class { A }
cpr 3584	class { A , B }
ctp 3585	class { A , B , C }
cop 3586	class <. A , B >.
cotp 3587	class <. A , B , C >.
df-sn 3589	|- { A } = { x | x = A }
df-pr 3590	|- { A , B } = ( { A } u. { B } )
df-tp 3591	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3592	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3593	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3796	class U. A
df-uni 3797	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3831	class |^| A
df-int 3832	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3873	class U_ x e. A B
ciin 3874	class |^|_ x e. A B
df-iun 3875	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3876	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 3966	wff Disj x e. A B
df-disj 3967	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 3989	wff A R B
df-br 3990	|- ( A R B <-> <. A , B >. e. R )
copab 4049	class { <. x , y >. | ph }
cmpt 4050	class ( x e. A |-> B )
df-opab 4051	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4052	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4087	wff Tr A
df-tr 4088	|- ( Tr A <-> U. A C_ A )
ax-coll 4104	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4107	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4115	|- E. x A. y -. y e. x
ax-pow 4160	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4180	wff EXMID
df-exmid 4181	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4194	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4272	class _E
cid 4273	class _I
df-eprel 4274	|- _E = { <. x , y >. | x e. y }
df-id 4278	|- _I = { <. x , y >. | x = y }
wpo 4279	wff R Po A
wor 4280	wff R Or A
df-po 4281	|- ( 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 4282	|- ( 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 4312	wff FrFor R A S
wfr 4313	wff R Fr A
wse 4314	wff R Se A
wwe 4315	wff R We A
df-frfor 4316	|- (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 4317	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4318	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4319	|- ( 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 4347	wff Ord A
con0 4348	class On
wlim 4349	wff Lim A
csuc 4350	class suc A
df-iord 4351	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4353	|- On = { x | Ord x }
df-ilim 4354	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4356	|- suc A = ( A u. { A } )
ax-un 4418	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4521	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4572	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4574	class om
df-iom 4575	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4609	class ( A X. B )
ccnv 4610	class `' A
cdm 4611	class dom A
crn 4612	class ran A
cres 4613	class ( A |` B )
cima 4614	class ( A " B )
ccom 4615	class ( A o. B )
wrel 4616	wff Rel A
df-xp 4617	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4618	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4619	|- `' A = { <. x , y >. | y A x }
df-co 4620	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4621	|- dom A = { x | E. y x A y }
df-rn 4622	|- ran A = dom `' A
df-res 4623	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4624	|- ( A " B ) = ran ( A |` B )
cio 5158	class ( iota x ph )
df-iota 5160	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5192	wff Fun A
wfn 5193	wff A Fn B
wf 5194	wff F : A --> B
wf1 5195	wff F : A -1-1-> B
wfo 5196	wff F : A -onto-> B
wf1o 5197	wff F : A -1-1-onto-> B
cfv 5198	class ( F ` A )
wiso 5199	wff H Isom R , S ( A , B )
df-fun 5200	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5201	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5202	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5203	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5204	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5205	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5206	|- ( F ` A ) = ( iota x A F x )
df-isom 5207	|- ( 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 5808	class ( iota_ x e. A ph )
df-riota 5809	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 5853	class ( A F B )
coprab 5854	class { <. <. x , y >. , z >. | ph }
cmpo 5855	class ( x e. A , y e. B |-> C )
df-ov 5856	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 5857	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 5858	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6059	class oF R
cofr 6060	class oR R
df-of 6061	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6062	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6117	class 1st
c2nd 6118	class 2nd
df-1st 6119	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6120	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6223	class tpos F
df-tpos 6224	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6264	wff Smo A
df-smo 6265	|- ( 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 6283	class recs ( F )
df-recs 6284	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6348	class rec ( F , I )
df-irdg 6349	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6369	class frec ( F , I )
df-frec 6370	|- 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 6388	class 1o
c2o 6389	class 2o
c3o 6390	class 3o
c4o 6391	class 4o
coa 6392	class +o
comu 6393	class .o
coei 6394	class ↑o
df-1o 6395	|- 1o = suc (/)
df-2o 6396	|- 2o = suc 1o
df-3o 6397	|- 3o = suc 2o
df-4o 6398	|- 4o = suc 3o
df-oadd 6399	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6400	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6401	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6510	wff R Er A
cec 6511	class [ A ] R
cqs 6512	class ( A /. R )
df-er 6513	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6515	|- [ A ] R = ( R " { A } )
df-qs 6519	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6626	class ^m
cpm 6627	class ^pm
df-map 6628	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6629	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6676	class X_ x e. A B
df-ixp 6677	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6716	class ~~
cdom 6717	class ~<_
cfn 6718	class Fin
df-en 6719	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6720	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6721	|- Fin = { x | E. y e. om x ~~ y }
cfi 6945	class fi
df-fi 6946	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 6959	class sup ( A , B , R )
cinf 6960	class inf ( A , B , R )
df-sup 6961	|- 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 6962	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7014	class ( A ⊔ B )
df-dju 7015	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7022	class inl
cinr 7023	class inr
df-inl 7024	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7025	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7060	class case ( R , S )
df-case 7061	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7079	class ( R ⊔d S )
df-djud 7080	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7096	class ℕ∞
df-nninf 7097	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7110	class Omni
df-omni 7111	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7127	class Markov
df-markov 7128	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7139	class WOmni
df-womni 7140	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7156	class card
df-card 7157	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
wac 7182	wff CHOICE
df-ac 7183	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wacc 7224	wff CCHOICE
df-cc 7225	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7234	class N.
cpli 7235	class +N
cmi 7236	class .N
clti 7237	class <N
cplpq 7238	class +pQ
cmpq 7239	class .pQ
cltpq 7240	class <pQ
ceq 7241	class ~Q
cnq 7242	class Q.
c1q 7243	class 1Q
cplq 7244	class +Q
cmq 7245	class .Q
crq 7246	class *Q
cltq 7247	class <Q
ceq0 7248	class ~Q0
cnq0 7249	class Q0
c0q0 7250	class 0Q0
cplq0 7251	class +Q0
cmq0 7252	class ·Q0
cnp 7253	class P.
c1p 7254	class 1P
cpp 7255	class +P.
cmp 7256	class .P.
cltp 7257	class <P
cer 7258	class ~R
cnr 7259	class R.
c0r 7260	class 0R
c1r 7261	class 1R
cm1r 7262	class -1R
cplr 7263	class +R
cmr 7264	class .R
cltr 7265	class <R
df-ni 7266	|- N. = ( om \ { (/) } )
df-pli 7267	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7268	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7269	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7306	|- +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 7307	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7308	|- <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 7309	|- ~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 7310	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7311	|- +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 7312	|- .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 7313	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7314	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7315	|- <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 7386	|- ~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 7387	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7388	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7389	|- +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 7390	|- ·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 7428	|- 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 7429	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7430	|- +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 7431	|- .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 7432	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7688	|- ~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 7689	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7690	|- +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 7691	|- .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 7692	|- <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 7693	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7694	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7695	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 7772	class CC
cr 7773	class RR
cc0 7774	class 0
c1 7775	class 1
ci 7776	class _i
caddc 7777	class +
cltrr 7778	class <RR
cmul 7779	class x.
df-c 7780	|- CC = ( R. X. R. )
df-0 7781	|- 0 = <. 0R , 0R >.
df-1 7782	|- 1 = <. 1R , 0R >.
df-i 7783	|- _i = <. 0R , 1R >.
df-r 7784	|- RR = ( R. X. { 0R } )
df-add 7785	|- + = { <. <. 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 7786	|- 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 7787	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 7865	|- CC e. _V
ax-resscn 7866	|- RR C_ CC
ax-1cn 7867	|- 1 e. CC
ax-1re 7868	|- 1 e. RR
ax-icn 7869	|- _i e. CC
ax-addcl 7870	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 7871	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 7872	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 7873	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 7874	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 7875	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 7876	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 7877	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 7878	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 7879	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 7880	|- 0 <RR 1
ax-1rid 7881	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 7882	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 7883	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 7884	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 7885	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 7886	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 7887	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 7888	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 7889	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 7890	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 7891	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 7892	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 7893	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 7894	|- 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 7895	|- ( ( ( 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 7896	|- + : ( CC X. CC ) --> CC
ax-mulf 7897	|- x. : ( CC X. CC ) --> CC
cpnf 7951	class +oo
cmnf 7952	class -oo
cxr 7953	class RR*
clt 7954	class <
cle 7955	class <_
df-pnf 7956	|- +oo = ~P U. CC
df-mnf 7957	|- -oo = ~P +oo
df-xr 7958	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 7959	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 7960	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8090	class -
cneg 8091	class -u A
df-sub 8092	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8093	|- -u A = ( 0 - A )
creap 8493	class #ℝ
df-reap 8494	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8500	class #
df-ap 8501	|- # = { <. 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 8589	class /
df-div 8590	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 8878	class NN
df-inn 8879	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 8929	class 2
c3 8930	class 3
c4 8931	class 4
c5 8932	class 5
c6 8933	class 6
c7 8934	class 7
c8 8935	class 8
c9 8936	class 9
df-2 8937	|- 2 = ( 1 + 1 )
df-3 8938	|- 3 = ( 2 + 1 )
df-4 8939	|- 4 = ( 3 + 1 )
df-5 8940	|- 5 = ( 4 + 1 )
df-6 8941	|- 6 = ( 5 + 1 )
df-7 8942	|- 7 = ( 6 + 1 )
df-8 8943	|- 8 = ( 7 + 1 )
df-9 8944	|- 9 = ( 8 + 1 )
cn0 9135	class NN0
df-n0 9136	|- NN0 = ( NN u. { 0 } )
cxnn0 9198	class NN0*
df-xnn0 9199	|- NN0* = ( NN0 u. { +oo } )
cz 9212	class ZZ
df-z 9213	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9343	class ; A B
df-dec 9344	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9487	class ZZ>=
df-uz 9488	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9578	class QQ
df-q 9579	|- QQ = ( / " ( ZZ X. NN ) )
crp 9610	class RR+
df-rp 9611	|- RR+ = { x e. RR | 0 < x }
cxne 9726	class -e A
cxad 9727	class +e
cxmu 9728	class xe
df-xneg 9729	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9730	|- +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 9731	|- 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 9845	class (,)
cioc 9846	class (,]
cico 9847	class [,)
cicc 9848	class [,]
df-ioo 9849	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 9850	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 9851	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 9852	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 9965	class ...
df-fz 9966	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10098	class ..^
df-fzo 10099	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10224	class |_
cceil 10225	class ⌈
df-fl 10226	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10227	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10278	class mod
df-mod 10279	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10401	class seq M ( .+ , F )
df-seqfrec 10402	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10475	class ^
df-exp 10476	|- ^ = ( 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 10659	class !
df-fac 10660	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10681	class _C
df-bc 10682	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 10709	class ♯
df-ihash 10710	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cshi 10778	class shift
df-shft 10779	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 10803	class *
cre 10804	class Re
cim 10805	class Im
df-cj 10806	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 10807	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 10808	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 10960	class sqr
cabs 10961	class abs
df-rsqrt 10962	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 10963	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11241	class ~~>
df-clim 11242	|- ~~> = { <. 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 11316	class sum_ k e. A B
df-sumdc 11317	|- 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 11513	class prod_ k e. A B
df-proddc 11514	|- 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 11605	class exp
ceu 11606	class _e
csin 11607	class sin
ccos 11608	class cos
ctan 11609	class tan
cpi 11610	class pi
df-ef 11611	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 11612	|- _e = ( exp ` 1 )
df-sin 11613	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 11614	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 11615	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 11616	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 11737	class tau
df-tau 11738	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 11749	class ||
df-dvds 11750	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cgcd 11897	class gcd
df-gcd 11898	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12014	class lcm
df-lcm 12015	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12061	class Prime
df-prm 12062	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12135	class numer
cdenom 12136	class denom
df-numer 12137	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12138	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12162	class odZ
cphi 12163	class phi
df-odz 12164	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12165	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12238	class pCnt
df-pc 12239	|- 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 12321	class ZZ[_i]
df-gz 12322	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 12412	class Struct
cnx 12413	class ndx
csts 12414	class sSet
cslot 12415	class Slot A
cbs 12416	class Base
cress 12417	class ↾s
df-struct 12418	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 12419	|- ndx = ( _I |` NN )
df-slot 12420	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 12422	|- Base = Slot 1
df-sets 12423	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-ress 12424	|- ↾s = ( w e. _V , x e. _V |-> if ( ( Base ` w ) C_ x , w , ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) ) )
cplusg 12480	class +g
cmulr 12481	class .r
cstv 12482	class *r
csca 12483	class Scalar
cvsca 12484	class .s
cip 12485	class .i
cts 12486	class TopSet
cple 12487	class le
coc 12488	class oc
cds 12489	class dist
cunif 12490	class UnifSet
chom 12491	class Hom
cco 12492	class comp
df-plusg 12493	|- +g = Slot 2
df-mulr 12494	|- .r = Slot 3
df-starv 12495	|- *r = Slot 4
df-sca 12496	|- Scalar = Slot 5
df-vsca 12497	|- .s = Slot 6
df-ip 12498	|- .i = Slot 8
df-tset 12499	|- TopSet = Slot 9
df-ple 12500	|- le = Slot ; 1 0
df-ocomp 12501	|- oc = Slot ; 1 1
df-ds 12502	|- dist = Slot ; 1 2
df-unif 12503	|- UnifSet = Slot ; 1 3
df-hom 12504	|- Hom = Slot ; 1 4
df-cco 12505	|- comp = Slot ; 1 5
crest 12579	class ↾t
ctopn 12580	class TopOpen
df-rest 12581	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 12582	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 12594	class topGen
cpt 12595	class Xt_
c0g 12596	class 0g
cgsu 12597	class gsumg
df-0g 12598	|- 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 12599	|- 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 12600	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 12601	|- 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 12602	class X_s
cpws 12603	class ^s
df-prds 12604	|- 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 12606	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cplusf 12607	class +f
cmgm 12608	class Mgm
df-plusf 12609	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 12610	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 12642	class Smgrp
df-sgrp 12643	|- Smgrp = { g e. Mgm | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) }
cmnd 12652	class Mnd
df-mnd 12653	|- Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }
cmhm 12681	class MndHom
csubmnd 12682	class SubMnd
df-mhm 12683	|- MndHom = ( s e. Mnd , t e. Mnd |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )
df-submnd 12684	|- SubMnd = ( s e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } )
cgrp 12708	class Grp
cminusg 12709	class invg
csg 12710	class -g
df-grp 12711	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 12712	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 12713	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cpsmet 12773	class PsMet
cxmet 12774	class *Met
cmet 12775	class Met
cbl 12776	class ball
cfbas 12777	class fBas
cfg 12778	class filGen
cmopn 12779	class MetOpen
cmetu 12780	class metUnif
df-psmet 12781	|- 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 12782	|- *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 12783	|- 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 12784	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 12785	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 12786	|- 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 12787	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 12788	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ctop 12789	class Top
df-top 12790	|- 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 12802	class TopOn
df-topon 12803	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 12822	class TopSp
df-topsp 12823	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 12834	class TopBases
df-bases 12835	|- 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 12886	class Clsd
cnt 12887	class int
ccl 12888	class cls
df-cld 12889	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 12890	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 12891	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 12932	class nei
df-nei 12933	|- 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 12979	class Cn
ccnp 12980	class CnP
clm 12981	class ~~> t
df-cn 12982	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 12983	|- 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 12984	|- ~~> 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 13046	class tX
df-tx 13047	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 13094	class Homeo
df-hmeo 13095	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 13130	class *MetSp
cms 13131	class MetSp
ctms 13132	class toMetSp
df-xms 13133	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 13134	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 13135	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 13351	class -cn->
df-cncf 13352	|- -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 13417	class lim CC
cdv 13418	class _D
df-limced 13419	|- 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 13420	|- _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 13571	class log
ccxp 13572	class ^c
df-relog 13573	|- log = `' ( exp |` RR )
df-rpcxp 13574	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 13655	class logb
df-logb 13656	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
clgs 13692	class /L
df-lgs 13693	|- /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 13828	wff A DECIDin B
df-dcin 13829	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 13847	wff BOUNDED ph
ax-bd0 13848	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 13849	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 13850	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 13851	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 13852	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 13853	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 13854	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 13855	|- BOUNDED x = y
ax-bdel 13856	|- BOUNDED x e. y
ax-bdsb 13857	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 13875	wff BOUNDED A
df-bdc 13876	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 13919	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 13959	|- BOUNDED ph   =>    |- DECID ph
wind 13961	wff Ind A
df-bj-ind 13962	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 13976	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 14003	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 14011	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 14017	|- 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 14022	|- 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 14024	|- ( ( ( 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 14105	wff A.! x ( ph -> ps )
walsc 14106	wff A.! x e. A ph
df-alsi 14107	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 14108	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )