mmdefinitions - Intuitionistic Logic Explorer

List of Syntax, Axioms (ax-) and Definitions (df-)

Ref	Expression (see link for any distinct variable requirements)
wn 3	wff -. ph
wi 4	wff ( ph -> ps )
ax-mp 5	|- ph   &    |- ( ph -> ps )   =>    |- ps
ax-1 6	|- ( ph -> ( ps -> ph ) )
ax-2 7	|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
wa 104	wff ( ph /\ ps )
wb 105	wff ( ph <-> ps )
ax-ia1 106	|- ( ( ph /\ ps ) -> ph )
ax-ia2 107	|- ( ( ph /\ ps ) -> ps )
ax-ia3 108	|- ( ph -> ( ps -> ( ph /\ ps ) ) )
df-bi 117	|- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
ax-in1 617	|- ( ( ph -> -. ph ) -> -. ph )
ax-in2 618	|- ( -. ph -> ( ph -> ps ) )
wo 713	wff ( ph \/ ps )
ax-io 714	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )
wstab 835	wff STAB ph
df-stab 836	|- (STAB ph <-> ( -. -. ph -> ph ) )
wdc 839	wff DECID ph
df-dc 840	|- (DECID ph <-> ( ph \/ -. ph ) )
wif 983	wff if- ( ph , ps , ch )
df-ifp 984	|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
w3o 1001	wff ( ph \/ ps \/ ch )
w3a 1002	wff ( ph /\ ps /\ ch )
df-3or 1003	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
df-3an 1004	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
wal 1393	wff A. x ph
cv 1394	class x
wceq 1395	wff A = B
wtru 1396	wff T.
df-tru 1398	|- ( T. <-> ( A. x x = x -> A. x x = x ) )
wfal 1400	wff F.
df-fal 1401	|- ( F. <-> -. T. )
wxo 1417	wff ( ph \/_ ps )
df-xor 1418	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
ax-5 1493	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
ax-7 1494	|- ( A. x A. y ph -> A. y A. x ph )
ax-gen 1495	|- ph   =>    |- A. x ph
wnf 1506	wff F/ x ph
df-nf 1507	|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
wex 1538	wff E. x ph
ax-ie1 1539	|- ( E. x ph -> A. x E. x ph )
ax-ie2 1540	|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
ax-8 1550	|- ( x = y -> ( x = z -> y = z ) )
ax-10 1551	|- ( A. x x = y -> A. y y = x )
ax-11 1552	|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
ax-i12 1553	|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
ax-bndl 1555	|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
ax-4 1556	|- ( A. x ph -> ph )
ax-17 1572	|- ( ph -> A. x ph )
ax-i9 1576	|- E. x x = y
ax-ial 1580	|- ( A. x ph -> A. x A. x ph )
ax-i5r 1581	|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
ax-10o 1762	|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
wsb 1808	wff [ y / x ] ph
df-sb 1809	|- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
ax-16 1860	|- ( A. x x = y -> ( ph -> A. x ph ) )
ax-11o 1869	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
weu 2077	wff E! x ph
wmo 2078	wff E* x ph
df-eu 2080	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
df-mo 2081	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
wcel 2200	wff A e. B
ax-13 2202	|- ( x = y -> ( x e. z -> y e. z ) )
ax-14 2203	|- ( x = y -> ( z e. x -> z e. y ) )
ax-ext 2211	|- ( A. z ( z e. x <-> z e. y ) -> x = y )
cab 2215	class { x | ph }
df-clab 2216	|- ( x e. { y | ph } <-> [ x / y ] ph )
df-cleq 2222	|- ( A. x ( x e. y <-> x e. z ) -> y = z )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
df-clel 2225	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
wnfc 2359	wff F/_ x A
df-nfc 2361	|- ( F/_ x A <-> A. y F/ x y e. A )
wne 2400	wff A =/= B
df-ne 2401	|- ( A =/= B <-> -. A = B )
wnel 2495	wff A e/ B
df-nel 2496	|- ( A e/ B <-> -. A e. B )
wral 2508	wff A. x e. A ph
wrex 2509	wff E. x e. A ph
wreu 2510	wff E! x e. A ph
wrmo 2511	wff E* x e. A ph
crab 2512	class { x e. A | ph }
df-ral 2513	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
df-rex 2514	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
df-reu 2515	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
df-rmo 2516	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
df-rab 2517	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
cvv 2800	class _V
df-v 2802	|- _V = { x | x = x }
wcdeq 3012	wff CondEq ( x = y -> ph )
df-cdeq 3013	|- (CondEq ( x = y -> ph ) <-> ( x = y -> ph ) )
wsbc 3029	wff [. A / x ]. ph
df-sbc 3030	|- ( [. A / x ]. ph <-> A e. { x | ph } )
csb 3125	class [_ A / x ]_ B
df-csb 3126	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }
cdif 3195	class ( A \ B )
cun 3196	class ( A u. B )
cin 3197	class ( A i^i B )
wss 3198	wff A C_ B
df-dif 3200	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }
df-un 3202	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
df-in 3204	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
df-ss 3211	|- ( A C_ B <-> ( A i^i B ) = A )
c0 3492	class (/)
df-nul 3493	|- (/) = ( _V \ _V )
cif 3603	class if ( ph , A , B )
df-if 3604	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
cpw 3650	class ~P A
df-pw 3652	|- ~P A = { x | x C_ A }
csn 3667	class { A }
cpr 3668	class { A , B }
ctp 3669	class { A , B , C }
cop 3670	class <. A , B >.
cotp 3671	class <. A , B , C >.
df-sn 3673	|- { A } = { x | x = A }
df-pr 3674	|- { A , B } = ( { A } u. { B } )
df-tp 3675	|- { A , B , C } = ( { A , B } u. { C } )
df-op 3676	|- <. A , B >. = { x | ( A e. _V /\ B e. _V /\ x e. { { A } , { A , B } } ) }
df-ot 3677	|- <. A , B , C >. = <. <. A , B >. , C >.
cuni 3889	class U. A
df-uni 3890	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
cint 3924	class |^| A
df-int 3925	|- |^| A = { x | A. y ( y e. A -> x e. y ) }
ciun 3966	class U_ x e. A B
ciin 3967	class |^|_ x e. A B
df-iun 3968	|- U_ x e. A B = { y | E. x e. A y e. B }
df-iin 3969	|- |^|_ x e. A B = { y | A. x e. A y e. B }
wdisj 4060	wff Disj x e. A B
df-disj 4061	|- (Disj x e. A B <-> A. y E* x e. A y e. B )
wbr 4084	wff A R B
df-br 4085	|- ( A R B <-> <. A , B >. e. R )
copab 4145	class { <. x , y >. | ph }
cmpt 4146	class ( x e. A |-> B )
df-opab 4147	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
df-mpt 4148	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
wtr 4183	wff Tr A
df-tr 4184	|- ( Tr A <-> U. A C_ A )
ax-coll 4200	|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
ax-sep 4203	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
ax-nul 4211	|- E. x A. y -. y e. x
ax-pow 4260	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
wem 4280	wff EXMID
df-exmid 4281	|- (EXMID <-> A. x ( x C_ { (/) } -> DECID (/) e. x ) )
ax-pr 4295	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )
cep 4380	class _E
cid 4381	class _I
df-eprel 4382	|- _E = { <. x , y >. | x e. y }
df-id 4386	|- _I = { <. x , y >. | x = y }
wpo 4387	wff R Po A
wor 4388	wff R Or A
df-po 4389	|- ( 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 4390	|- ( 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 4420	wff FrFor R A S
wfr 4421	wff R Fr A
wse 4422	wff R Se A
wwe 4423	wff R We A
df-frfor 4424	|- (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 4425	|- ( R Fr A <-> A. sFrFor R A s )
df-se 4426	|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
df-wetr 4427	|- ( 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 4455	wff Ord A
con0 4456	class On
wlim 4457	wff Lim A
csuc 4458	class suc A
df-iord 4459	|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
df-on 4461	|- On = { x | Ord x }
df-ilim 4462	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
df-suc 4464	|- suc A = ( A u. { A } )
ax-un 4526	|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
ax-setind 4631	|- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-iinf 4682	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
com 4684	class om
df-iom 4685	|- om = |^| { x | ( (/) e. x /\ A. y e. x suc y e. x ) }
cxp 4719	class ( A X. B )
ccnv 4720	class `' A
cdm 4721	class dom A
crn 4722	class ran A
cres 4723	class ( A |` B )
cima 4724	class ( A " B )
ccom 4725	class ( A o. B )
wrel 4726	wff Rel A
df-xp 4727	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
df-rel 4728	|- ( Rel A <-> A C_ ( _V X. _V ) )
df-cnv 4729	|- `' A = { <. x , y >. | y A x }
df-co 4730	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
df-dm 4731	|- dom A = { x | E. y x A y }
df-rn 4732	|- ran A = dom `' A
df-res 4733	|- ( A |` B ) = ( A i^i ( B X. _V ) )
df-ima 4734	|- ( A " B ) = ran ( A |` B )
cio 5280	class ( iota x ph )
df-iota 5282	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
wfun 5316	wff Fun A
wfn 5317	wff A Fn B
wf 5318	wff F : A --> B
wf1 5319	wff F : A -1-1-> B
wfo 5320	wff F : A -onto-> B
wf1o 5321	wff F : A -1-1-onto-> B
cfv 5322	class ( F ` A )
wiso 5323	wff H Isom R , S ( A , B )
df-fun 5324	|- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
df-fn 5325	|- ( A Fn B <-> ( Fun A /\ dom A = B ) )
df-f 5326	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
df-f1 5327	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
df-fo 5328	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
df-f1o 5329	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
df-fv 5330	|- ( F ` A ) = ( iota x A F x )
df-isom 5331	|- ( 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 5963	class ( iota_ x e. A ph )
df-riota 5964	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
co 6011	class ( A F B )
coprab 6012	class { <. <. x , y >. , z >. | ph }
cmpo 6013	class ( x e. A , y e. B |-> C )
df-ov 6014	|- ( A F B ) = ( F ` <. A , B >. )
df-oprab 6015	|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
df-mpo 6016	|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
cof 6226	class oF R
cofr 6227	class oR R
df-of 6228	|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
df-ofr 6229	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
c1st 6294	class 1st
c2nd 6295	class 2nd
df-1st 6296	|- 1st = ( x e. _V |-> U. dom { x } )
df-2nd 6297	|- 2nd = ( x e. _V |-> U. ran { x } )
ctpos 6403	class tpos F
df-tpos 6404	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
wsmo 6444	wff Smo A
df-smo 6445	|- ( 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 6463	class recs ( F )
df-recs 6464	|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
crdg 6528	class rec ( F , I )
df-irdg 6529	|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
cfrec 6549	class frec ( F , I )
df-frec 6550	|- 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 6568	class 1o
c2o 6569	class 2o
c3o 6570	class 3o
c4o 6571	class 4o
coa 6572	class +o
comu 6573	class .o
coei 6574	class ↑o
df-1o 6575	|- 1o = suc (/)
df-2o 6576	|- 2o = suc 1o
df-3o 6577	|- 3o = suc 2o
df-4o 6578	|- 4o = suc 3o
df-oadd 6579	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
df-omul 6580	|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
df-oexpi 6581	|- ↑o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
wer 6692	wff R Er A
cec 6693	class [ A ] R
cqs 6694	class ( A /. R )
df-er 6695	|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
df-ec 6697	|- [ A ] R = ( R " { A } )
df-qs 6701	|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
cmap 6810	class ^m
cpm 6811	class ^pm
df-map 6812	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
df-pm 6813	|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
cixp 6860	class X_ x e. A B
df-ixp 6861	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
cen 6900	class ~~
cdom 6901	class ~<_
cfn 6902	class Fin
df-en 6903	|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
df-dom 6904	|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
df-fin 6905	|- Fin = { x | E. y e. om x ~~ y }
cfi 7156	class fi
df-fi 7157	|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
csup 7170	class sup ( A , B , R )
cinf 7171	class inf ( A , B , R )
df-sup 7172	|- 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 7173	|- inf ( A , B , R ) = sup ( A , B , `' R )
cdju 7225	class ( A ⊔ B )
df-dju 7226	|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
cinl 7233	class inl
cinr 7234	class inr
df-inl 7235	|- inl = ( x e. _V |-> <. (/) , x >. )
df-inr 7236	|- inr = ( x e. _V |-> <. 1o , x >. )
cdjucase 7271	class case ( R , S )
df-case 7272	|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
cdjud 7290	class ( R ⊔d S )
df-djud 7291	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
xnninf 7307	class ℕ∞
df-nninf 7308	|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
comni 7322	class Omni
df-omni 7323	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
cmarkov 7339	class Markov
df-markov 7340	|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
cwomni 7351	class WOmni
df-womni 7352	|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
ccrd 7370	class card
wacn 7371	class AC A
df-card 7372	|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
df-acnm 7373	|- AC A = { x | ( A e. _V /\ A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
wac 7408	wff CHOICE
df-ac 7409	|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
wap 7454	wff R Ap A
df-pap 7455	|- ( R Ap A <-> ( ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) /\ ( A. x e. A A. y e. A ( x R y -> y R x ) /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) ) ) )
wtap 7456	wff R TAp A
df-tap 7457	|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
wacc 7469	wff CCHOICE
df-cc 7470	|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
cnpi 7480	class N.
cpli 7481	class +N
cmi 7482	class .N
clti 7483	class <N
cplpq 7484	class +pQ
cmpq 7485	class .pQ
cltpq 7486	class <pQ
ceq 7487	class ~Q
cnq 7488	class Q.
c1q 7489	class 1Q
cplq 7490	class +Q
cmq 7491	class .Q
crq 7492	class *Q
cltq 7493	class <Q
ceq0 7494	class ~Q0
cnq0 7495	class Q0
c0q0 7496	class 0Q0
cplq0 7497	class +Q0
cmq0 7498	class ·Q0
cnp 7499	class P.
c1p 7500	class 1P
cpp 7501	class +P.
cmp 7502	class .P.
cltp 7503	class <P
cer 7504	class ~R
cnr 7505	class R.
c0r 7506	class 0R
c1r 7507	class 1R
cm1r 7508	class -1R
cplr 7509	class +R
cmr 7510	class .R
cltr 7511	class <R
df-ni 7512	|- N. = ( om \ { (/) } )
df-pli 7513	|- +N = ( +o |` ( N. X. N. ) )
df-mi 7514	|- .N = ( .o |` ( N. X. N. ) )
df-lti 7515	|- <N = ( _E i^i ( N. X. N. ) )
df-plpq 7552	|- +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 7553	|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
df-ltpq 7554	|- <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 7555	|- ~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 7556	|- Q. = ( ( N. X. N. ) /. ~Q )
df-plqqs 7557	|- +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 7558	|- .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 7559	|- 1Q = [ <. 1o , 1o >. ] ~Q
df-rq 7560	|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
df-ltnqqs 7561	|- <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 7632	|- ~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 7633	|- Q0 = ( ( om X. N. ) /. ~Q0 )
df-0nq0 7634	|- 0Q0 = [ <. (/) , 1o >. ] ~Q0
df-plq0 7635	|- +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 7636	|- ·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 7674	|- 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 7675	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
df-iplp 7676	|- +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 7677	|- .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 7678	|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
df-enr 7934	|- ~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 7935	|- R. = ( ( P. X. P. ) /. ~R )
df-plr 7936	|- +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 7937	|- .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 7938	|- <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 7939	|- 0R = [ <. 1P , 1P >. ] ~R
df-1r 7940	|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
df-m1r 7941	|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
cc 8018	class CC
cr 8019	class RR
cc0 8020	class 0
c1 8021	class 1
ci 8022	class _i
caddc 8023	class +
cltrr 8024	class <RR
cmul 8025	class x.
df-c 8026	|- CC = ( R. X. R. )
df-0 8027	|- 0 = <. 0R , 0R >.
df-1 8028	|- 1 = <. 1R , 0R >.
df-i 8029	|- _i = <. 0R , 1R >.
df-r 8030	|- RR = ( R. X. { 0R } )
df-add 8031	|- + = { <. <. 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 8032	|- 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 8033	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
ax-cnex 8111	|- CC e. _V
ax-resscn 8112	|- RR C_ CC
ax-1cn 8113	|- 1 e. CC
ax-1re 8114	|- 1 e. RR
ax-icn 8115	|- _i e. CC
ax-addcl 8116	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
ax-addrcl 8117	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
ax-mulcl 8118	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
ax-mulrcl 8119	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
ax-addcom 8120	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
ax-mulcom 8121	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
ax-addass 8122	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
ax-mulass 8123	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
ax-distr 8124	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
ax-i2m1 8125	|- ( ( _i x. _i ) + 1 ) = 0
ax-0lt1 8126	|- 0 <RR 1
ax-1rid 8127	|- ( A e. RR -> ( A x. 1 ) = A )
ax-0id 8128	|- ( A e. CC -> ( A + 0 ) = A )
ax-rnegex 8129	|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
ax-precex 8130	|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
ax-cnre 8131	|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
ax-pre-ltirr 8132	|- ( A e. RR -> -. A <RR A )
ax-pre-ltwlin 8133	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
ax-pre-lttrn 8134	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
ax-pre-apti 8135	|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
ax-pre-ltadd 8136	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
ax-pre-mulgt0 8137	|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
ax-pre-mulext 8138	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
ax-arch 8139	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
ax-caucvg 8140	|- 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 8141	|- ( ( ( 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 8142	|- + : ( CC X. CC ) --> CC
ax-mulf 8143	|- x. : ( CC X. CC ) --> CC
cpnf 8199	class +oo
cmnf 8200	class -oo
cxr 8201	class RR*
clt 8202	class <
cle 8203	class <_
df-pnf 8204	|- +oo = ~P U. CC
df-mnf 8205	|- -oo = ~P +oo
df-xr 8206	|- RR* = ( RR u. { +oo , -oo } )
df-ltxr 8207	|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
df-le 8208	|- <_ = ( ( RR* X. RR* ) \ `' < )
cmin 8338	class -
cneg 8339	class -u A
df-sub 8340	|- - = ( x e. CC , y e. CC |-> ( iota_ z e. CC ( y + z ) = x ) )
df-neg 8341	|- -u A = ( 0 - A )
creap 8742	class #ℝ
df-reap 8743	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
cap 8749	class #
df-ap 8750	|- # = { <. 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 8840	class /
df-div 8841	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
cn 9131	class NN
df-inn 9132	|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
c2 9182	class 2
c3 9183	class 3
c4 9184	class 4
c5 9185	class 5
c6 9186	class 6
c7 9187	class 7
c8 9188	class 8
c9 9189	class 9
df-2 9190	|- 2 = ( 1 + 1 )
df-3 9191	|- 3 = ( 2 + 1 )
df-4 9192	|- 4 = ( 3 + 1 )
df-5 9193	|- 5 = ( 4 + 1 )
df-6 9194	|- 6 = ( 5 + 1 )
df-7 9195	|- 7 = ( 6 + 1 )
df-8 9196	|- 8 = ( 7 + 1 )
df-9 9197	|- 9 = ( 8 + 1 )
cn0 9390	class NN0
df-n0 9391	|- NN0 = ( NN u. { 0 } )
cxnn0 9453	class NN0*
df-xnn0 9454	|- NN0* = ( NN0 u. { +oo } )
cz 9467	class ZZ
df-z 9468	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
cdc 9599	class ; A B
df-dec 9600	|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
cuz 9743	class ZZ>=
df-uz 9744	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
cq 9841	class QQ
df-q 9842	|- QQ = ( / " ( ZZ X. NN ) )
crp 9876	class RR+
df-rp 9877	|- RR+ = { x e. RR | 0 < x }
cxne 9992	class -e A
cxad 9993	class +e
cxmu 9994	class xe
df-xneg 9995	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
df-xadd 9996	|- +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 9997	|- 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 10111	class (,)
cioc 10112	class (,]
cico 10113	class [,)
cicc 10114	class [,]
df-ioo 10115	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
df-ioc 10116	|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
df-ico 10117	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
df-icc 10118	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
cfz 10231	class ...
df-fz 10232	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
cfzo 10365	class ..^
df-fzo 10366	|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
cfl 10516	class |_
cceil 10517	class ⌈
df-fl 10518	|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
df-ceil 10519	|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
cmo 10572	class mod
df-mod 10573	|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
cseq 10697	class seq M ( .+ , F )
df-seqfrec 10698	|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
cexp 10788	class ^
df-exp 10789	|- ^ = ( 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 10975	class !
df-fac 10976	|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
cbc 10997	class _C
df-bc 10998	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
chash 11025	class ♯
df-ihash 11026	|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
cword 11100	class Word S
df-word 11101	|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }
clsw 11145	class lastS
df-lsw 11146	|- lastS = ( w e. _V |-> ( w ` ( (♯ ` w ) - 1 ) ) )
cconcat 11154	class ++
df-concat 11155	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
cs1 11179	class <" A ">
df-s1 11180	|- <" A "> = { <. 0 , ( _I ` A ) >. }
csubstr 11213	class substr
df-substr 11214	|- substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )
cpfx 11240	class prefix
df-pfx 11241	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
cs2 11317	class <" A B ">
cs3 11318	class <" A B C ">
cs4 11319	class <" A B C D ">
cs5 11320	class <" A B C D E ">
cs6 11321	class <" A B C D E F ">
cs7 11322	class <" A B C D E F G ">
cs8 11323	class <" A B C D E F G H ">
df-s2 11324	|- <" A B "> = ( <" A "> ++ <" B "> )
df-s3 11325	|- <" A B C "> = ( <" A B "> ++ <" C "> )
df-s4 11326	|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
df-s5 11327	|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
df-s6 11328	|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
df-s7 11329	|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
df-s8 11330	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )
cshi 11362	class shift
df-shft 11363	|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
ccj 11387	class *
cre 11388	class Re
cim 11389	class Im
df-cj 11390	|- * = ( x e. CC |-> ( iota_ y e. CC ( ( x + y ) e. RR /\ ( _i x. ( x - y ) ) e. RR ) ) )
df-re 11391	|- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) )
df-im 11392	|- Im = ( x e. CC |-> ( Re ` ( x / _i ) ) )
csqrt 11544	class sqr
cabs 11545	class abs
df-rsqrt 11546	|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
df-abs 11547	|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
cli 11826	class ~~>
df-clim 11827	|- ~~> = { <. 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 11901	class sum_ k e. A B
df-sumdc 11902	|- 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 12098	class prod_ k e. A B
df-proddc 12099	|- 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 12190	class exp
ceu 12191	class _e
csin 12192	class sin
ccos 12193	class cos
ctan 12194	class tan
cpi 12195	class pi
df-ef 12196	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
df-e 12197	|- _e = ( exp ` 1 )
df-sin 12198	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
df-cos 12199	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
df-tan 12200	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
df-pi 12201	|- pi = inf ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , < )
ctau 12323	class tau
df-tau 12324	|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
cdvds 12335	class ||
df-dvds 12336	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
cbits 12488	class bits
df-bits 12489	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
cgcd 12511	class gcd
df-gcd 12512	|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
clcm 12619	class lcm
df-lcm 12620	|- lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
cprime 12666	class Prime
df-prm 12667	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
cnumer 12740	class numer
cdenom 12741	class denom
df-numer 12742	|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
df-denom 12743	|- denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
codz 12767	class odZ
cphi 12768	class phi
df-odz 12769	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
df-phi 12770	|- phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
cpc 12844	class pCnt
df-pc 12845	|- 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 12929	class ZZ[_i]
df-gz 12930	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
cstr 13065	class Struct
cnx 13066	class ndx
csts 13067	class sSet
cslot 13068	class Slot A
cbs 13069	class Base
cress 13070	class ↾s
df-struct 13071	|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
df-ndx 13072	|- ndx = ( _I |` NN )
df-slot 13073	|- Slot A = ( x e. _V |-> ( x ` A ) )
df-base 13075	|- Base = Slot 1
df-sets 13076	|- sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
df-iress 13077	|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
cplusg 13147	class +g
cmulr 13148	class .r
cstv 13149	class *r
csca 13150	class Scalar
cvsca 13151	class .s
cip 13152	class .i
cts 13153	class TopSet
cple 13154	class le
coc 13155	class oc
cds 13156	class dist
cunif 13157	class UnifSet
chom 13158	class Hom
cco 13159	class comp
df-plusg 13160	|- +g = Slot 2
df-mulr 13161	|- .r = Slot 3
df-starv 13162	|- *r = Slot 4
df-sca 13163	|- Scalar = Slot 5
df-vsca 13164	|- .s = Slot 6
df-ip 13165	|- .i = Slot 8
df-tset 13166	|- TopSet = Slot 9
df-ple 13167	|- le = Slot ; 1 0
df-ocomp 13168	|- oc = Slot ; 1 1
df-ds 13169	|- dist = Slot ; 1 2
df-unif 13170	|- UnifSet = Slot ; 1 3
df-hom 13171	|- Hom = Slot ; 1 4
df-cco 13172	|- comp = Slot ; 1 5
crest 13309	class ↾t
ctopn 13310	class TopOpen
df-rest 13311	|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
df-topn 13312	|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
ctg 13324	class topGen
cpt 13325	class Xt_
c0g 13326	class 0g
cgsu 13327	class gsumg
df-0g 13328	|- 0g = ( g e. _V |-> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) )
df-igsum 13329	|- gsumg = ( w e. _V , f e. _V |-> ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) ) )
df-topgen 13330	|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
df-pt 13331	|- 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 13335	class X_s
cpws 13336	class ^s
df-prds 13337	|- 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. ( ( 2nd ` a ) h c ) , 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 13360	|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
cimas 13369	class "s
cqus 13370	class /.s
cxps 13371	class X.s
df-iimas 13372	|- "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } )
df-qus 13373	|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
df-xps 13374	|- X.s = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( (Scalar ` r ) X_s { <. (/) , r >. , <. 1o , s >. } ) ) )
cplusf 13423	class +f
cmgm 13424	class Mgm
df-plusf 13425	|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
df-mgm 13426	|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
csgrp 13471	class Smgrp
df-sgrp 13472	|- 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 13486	class Mnd
df-mnd 13487	|- 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 13527	class MndHom
csubmnd 13528	class SubMnd
df-mhm 13529	|- 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 13530	|- 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 13570	class Grp
cminusg 13571	class invg
csg 13572	class -g
df-grp 13573	|- Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
df-minusg 13574	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
df-sbg 13575	|- -g = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) ( ( invg ` g ) ` y ) ) ) )
cmg 13693	class .g
df-mulg 13694	|- .g = ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) )
csubg 13741	class SubGrp
cnsg 13742	class NrmSGrp
cqg 13743	class ~QG
df-subg 13744	|- SubGrp = ( w e. Grp |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Grp } )
df-nsg 13745	|- NrmSGrp = ( w e. Grp |-> { s e. (SubGrp ` w ) | [. ( Base ` w ) / b ]. [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s ) } )
df-eqg 13746	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
cghm 13814	class GrpHom
df-ghm 13815	|- GrpHom = ( s e. Grp , t e. Grp |-> { g | [. ( Base ` s ) / w ]. ( g : w --> ( Base ` t ) /\ A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) ) ) } )
ccmn 13858	class CMnd
cabl 13859	class Abel
df-cmn 13860	|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
df-abl 13861	|- Abel = ( Grp i^i CMnd )
cmgp 13920	class mulGrp
df-mgp 13921	|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
crng 13932	class Rng
df-rng 13933	|- Rng = { f e. Abel | ( (mulGrp ` f ) e. Smgrp /\ [. ( Base ` f ) / b ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. b A. y e. b A. z e. b ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
cur 13959	class 1r
df-ur 13960	|- 1r = ( 0g o. mulGrp )
csrg 13963	class SRing
df-srg 13964	|- SRing = { f e. CMnd | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. [. ( 0g ` f ) / n ]. A. x e. r ( A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) /\ ( ( n t x ) = n /\ ( x t n ) = n ) ) ) }
crg 13996	class Ring
ccrg 13997	class CRing
df-ring 13998	|- Ring = { f e. Grp | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
df-cring 13999	|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
coppr 14067	class oppr
df-oppr 14068	|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
cdsr 14086	class ||r
cui 14087	class Unit
cir 14088	class Irred
df-dvdsr 14089	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
df-unit 14090	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
df-irred 14091	|- Irred = ( w e. _V |-> [_ ( ( Base ` w ) \ (Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z } )
cinvr 14121	class invr
df-invr 14122	|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
cdvr 14132	class /r
df-dvr 14133	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
crh 14151	class RingHom
crs 14152	class RingIso
df-rhm 14153	|- RingHom = ( r e. Ring , s e. Ring |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } )
df-rim 14154	|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
cnzr 14180	class NzRing
df-nzr 14181	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
clring 14191	class LRing
df-lring 14192	|- LRing = { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. (Unit ` r ) \/ y e. (Unit ` r ) ) ) }
csubrng 14198	class SubRng
df-subrng 14199	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
csubrg 14218	class SubRing
crgspn 14219	class RingSpan
df-subrg 14220	|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
df-rgspn 14221	|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
crlreg 14256	class RLReg
cdomn 14257	class Domn
cidom 14258	class IDomn
df-rlreg 14259	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
df-domn 14260	|- Domn = { r e. NzRing | [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) }
df-idom 14261	|- IDomn = ( CRing i^i Domn )
capr 14281	class #r
df-apr 14282	|- #r = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( x ( -g ` w ) y ) e. (Unit ` w ) ) } )
clmod 14288	class LMod
cscaf 14289	class .sf
df-lmod 14290	|- LMod = { g e. Grp | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) ) }
df-scaf 14291	|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
clss 14353	class LSubSp
df-lssm 14354	|- LSubSp = ( w e. _V |-> { s e. ~P ( Base ` w ) | ( E. j j e. s /\ A. x e. ( Base ` (Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s ) } )
clspn 14387	class LSpan
df-lsp 14388	|- LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
csra 14434	class subringAlg
crglmod 14435	class ringLMod
df-sra 14436	|- subringAlg = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) )
df-rgmod 14437	|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
clidl 14468	class LIdeal
crsp 14469	class RSpan
df-lidl 14470	|- LIdeal = ( LSubSp o. ringLMod )
df-rsp 14471	|- RSpan = ( LSpan o. ringLMod )
c2idl 14500	class 2Ideal
df-2idl 14501	|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
cpsmet 14536	class PsMet
cxmet 14537	class *Met
cmet 14538	class Met
cbl 14539	class ball
cfbas 14540	class fBas
cfg 14541	class filGen
cmopn 14542	class MetOpen
cmetu 14543	class metUnif
df-psmet 14544	|- 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 14545	|- *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 14546	|- 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 14547	|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
df-mopn 14548	|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
df-fbas 14549	|- 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 14550	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
df-metu 14551	|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
ccnfld 14557	class ℂfld
df-cnfld 14558	|- ℂfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( x e. CC , y e. CC |-> ( x + y ) ) >. , <. ( .r ` ndx ) , ( x e. CC , y e. CC |-> ( x x. y ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } ) )
czring 14591	class ℤring
df-zring 14592	|- ℤring = (ℂfld ↾s ZZ )
czrh 14612	class ZRHom
czlm 14613	class ZMod
czn 14614	class ℤ/nℤ
df-zrh 14615	|- ZRHom = ( r e. _V |-> U. (ℤring RingHom r ) )
df-zlm 14616	|- ZMod = ( g e. _V |-> ( ( g sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , (.g ` g ) >. ) )
df-zn 14617	|- ℤ/nℤ = ( n e. NN0 |-> [_ℤring / z ]_ [_ ( z /.s ( z ~QG ( (RSpan ` z ) ` { n } ) ) ) / s ]_ ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. ) )
cmps 14662	class mPwSer
cmpl 14663	class mPoly
df-psr 14664	|- mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
df-mplcoe 14665	|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )
ctop 14708	class Top
df-top 14709	|- 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 14721	class TopOn
df-topon 14722	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
ctps 14741	class TopSp
df-topsp 14742	|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
ctb 14753	class TopBases
df-bases 14754	|- 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 14803	class Clsd
cnt 14804	class int
ccl 14805	class cls
df-cld 14806	|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
df-ntr 14807	|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
df-cls 14808	|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
cnei 14849	class nei
df-nei 14850	|- 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 14896	class Cn
ccnp 14897	class CnP
clm 14898	class ~~> t
df-cn 14899	|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
df-cnp 14900	|- 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 14901	|- ~~> 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 14963	class tX
df-tx 14964	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
chmeo 15011	class Homeo
df-hmeo 15012	|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
cxms 15047	class *MetSp
cms 15048	class MetSp
ctms 15049	class toMetSp
df-xms 15050	|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
df-ms 15051	|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
df-tms 15052	|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
ccncf 15281	class -cn->
df-cncf 15282	|- -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 15365	class lim CC
cdv 15366	class _D
df-limced 15367	|- 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 15368	|- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )
cply 15439	class Poly
cidp 15440	class Xp
df-ply 15441	|- Poly = ( x e. ~P CC |-> { f | E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
df-idp 15442	|- Xp = ( _I |` CC )
clog 15567	class log
ccxp 15568	class ^c
df-relog 15569	|- log = `' ( exp |` RR )
df-rpcxp 15570	|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
clogb 15654	class logb
df-logb 15655	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
csgm 15692	class sigma
df-sgm 15693	|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
clgs 15713	class /L
df-lgs 15714	|- /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 ) ) ) ) )
cedgf 15842	class .ef
df-edgf 15843	|- .ef = Slot ; 1 8
cvtx 15850	class Vtx
ciedg 15851	class iEdg
df-vtx 15852	|- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
df-iedg 15853	|- iEdg = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , (.ef ` g ) ) )
cedg 15895	class Edg
df-edg 15896	|- Edg = ( g e. _V |-> ran (iEdg ` g ) )
cuhgr 15904	class UHGraph
cushgr 15905	class USHGraph
df-uhgrm 15906	|- UHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
df-ushgrm 15907	|- USHGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
cupgr 15928	class UPGraph
cumgr 15929	class UMGraph
df-upgren 15930	|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-umgren 15931	|- UMGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
cuspgr 15988	class USPGraph
cusgr 15989	class USGraph
df-uspgren 15990	|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
df-usgren 15991	|- USGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | x ~~ 2o } }
cvtxdg 16088	class VtxDeg
df-vtxdg 16089	|- VtxDeg = ( g e. _V |-> [_ (Vtx ` g ) / v ]_ [_ (iEdg ` g ) / e ]_ ( u e. v |-> ( (♯ ` { x e. dom e | u e. ( e ` x ) } ) +e (♯ ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )
cwlks 16105	class Walks
df-wlks 16106	|- Walks = ( g e. _V |-> { <. f , p >. | ( f e. Word dom (iEdg ` g ) /\ p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g ) /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) ) ) } )
ctrls 16166	class Trails
df-trls 16167	|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
cclwwlk 16176	class ClWWalks
df-clwwlk 16177	|- ClWWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )
cclwwlkn 16188	class ClWWalksN
df-clwwlkn 16189	|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
cclwwlknon 16211	class ClWWalksNOn
df-clwwlknon 16212	|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 16299	wff A DECIDin B
df-dcin 16300	|- ( A DECIDin B <-> A. x e. B DECID x e. A )
wbd 16317	wff BOUNDED ph
ax-bd0 16318	|- ( ph <-> ps )   =>    |- (BOUNDED ph -> BOUNDED ps )
ax-bdim 16319	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph -> ps )
ax-bdan 16320	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph /\ ps )
ax-bdor 16321	|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/ ps )
ax-bdn 16322	|- BOUNDED ph   =>    |- BOUNDED -. ph
ax-bdal 16323	|- BOUNDED ph   =>    |- BOUNDED A. x e. y ph
ax-bdex 16324	|- BOUNDED ph   =>    |- BOUNDED E. x e. y ph
ax-bdeq 16325	|- BOUNDED x = y
ax-bdel 16326	|- BOUNDED x e. y
ax-bdsb 16327	|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
wbdc 16345	wff BOUNDED A
df-bdc 16346	|- (BOUNDED A <-> A. xBOUNDED x e. A )
ax-bdsep 16389	|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
ax-bj-d0cl 16429	|- BOUNDED ph   =>    |- DECID ph
wind 16431	wff Ind A
df-bj-ind 16432	|- (Ind A <-> ( (/) e. A /\ A. x e. A suc x e. A ) )
ax-infvn 16446	|- E. x (Ind x /\ A. y (Ind y -> x C_ y ) )
ax-bdsetind 16473	|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
ax-inf2 16481	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
ax-strcoll 16487	|- 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 16492	|- 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 16494	|- ( ( ( 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 16590	wff A.! x ( ph -> ps )
walsc 16591	wff A.! x e. A ph
df-alsi 16592	|- ( A.! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
df-alsc 16593	|- ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )