Metamath Proof Explorer Home Metamath Proof Explorer
Bibliographic Cross-References
 
Mirrors  >  Home  >  MPE Home  >  Bibliographic Cross-References

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the Metamath Proof Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular set theory book, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Bibliographic Cross-Reference for the Metamath Proof Explorer
Bibliographic ReferenceDescriptionMetamath Proof Explorer Page(s)
[Adamek] p. 21Definition 3.1df-cat 17711
[Adamek] p. 21Condition 3.1(b)df-cat 17711
[Adamek] p. 22Example 3.3(1)df-setc 18121
[Adamek] p. 24Example 3.3(4.c)0cat 17732  df-termc 49120
[Adamek] p. 24Example 3.3(4.d)df-prstc 49152  prsthinc 49111
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49175  df-mndtc 49175
[Adamek] p. 25Definition 3.5df-oppc 17755
[Adamek] p. 25Example 3.6(1)oduoppcciso 49170
[Adamek] p. 25Example 3.6(2)oppgoppcco 49188  oppgoppchom 49187  oppgoppcid 49189
[Adamek] p. 28Remark 3.9oppciso 17825
[Adamek] p. 28Remark 3.12invf1o 17813  invisoinvl 17834
[Adamek] p. 28Example 3.13idinv 17833  idiso 17832
[Adamek] p. 28Corollary 3.11inveq 17818
[Adamek] p. 28Definition 3.8df-inv 17792  df-iso 17793  dfiso2 17816
[Adamek] p. 28Proposition 3.10sectcan 17799
[Adamek] p. 29Remark 3.16cicer 17850
[Adamek] p. 29Definition 3.15cic 17843  df-cic 17840
[Adamek] p. 29Definition 3.17df-func 17903
[Adamek] p. 29Proposition 3.14(1)invinv 17814
[Adamek] p. 29Proposition 3.14(2)invco 17815  isoco 17821
[Adamek] p. 30Remark 3.19df-func 17903
[Adamek] p. 30Example 3.20(1)idfucl 17926
[Adamek] p. 32Proposition 3.21funciso 17919
[Adamek] p. 33Example 3.26(2)df-thinc 49068  prsthinc 49111  thincciso 49102  thincciso2 49104  thincciso3 49105  thinccisod 49103
[Adamek] p. 33Example 3.26(3)df-mndtc 49175
[Adamek] p. 33Proposition 3.23cofucl 17933
[Adamek] p. 34Remark 3.28(2)catciso 18156
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18212
[Adamek] p. 34Definition 3.27(2)df-fth 17952
[Adamek] p. 34Definition 3.27(3)df-full 17951
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18212
[Adamek] p. 35Corollary 3.32ffthiso 17976
[Adamek] p. 35Proposition 3.30(c)cofth 17982
[Adamek] p. 35Proposition 3.30(d)cofull 17981
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18197
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18197
[Adamek] p. 39Definition 3.41funcoppc 17920
[Adamek] p. 39Definition 3.44.df-catc 18144
[Adamek] p. 39Proposition 3.43(c)fthoppc 17970
[Adamek] p. 39Proposition 3.43(d)fulloppc 17969
[Adamek] p. 40Remark 3.48catccat 18153
[Adamek] p. 40Definition 3.47df-catc 18144
[Adamek] p. 48Example 4.3(1.a)0subcat 17883
[Adamek] p. 48Example 4.3(1.b)catsubcat 17884
[Adamek] p. 48Definition 4.1(2)fullsubc 17895
[Adamek] p. 48Definition 4.1(a)df-subc 17856
[Adamek] p. 49Remark 4.4(2)ressffth 17985
[Adamek] p. 83Definition 6.1df-nat 17991
[Adamek] p. 87Remark 6.14(a)fuccocl 18012
[Adamek] p. 87Remark 6.14(b)fucass 18016
[Adamek] p. 87Definition 6.15df-fuc 17992
[Adamek] p. 88Remark 6.16fuccat 18018
[Adamek] p. 101Definition 7.1df-inito 18029
[Adamek] p. 101Example 7.2 (6)irinitoringc 21490
[Adamek] p. 102Definition 7.4df-termo 18030
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18057
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18061
[Adamek] p. 103Definition 7.7df-zeroo 18031
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21491
[Adamek] p. 103Proposition 7.6termoeu1w 18064
[Adamek] p. 106Definition 7.19df-sect 17791
[Adamek] p. 185Section 10.67updjud 9974
[Adamek] p. 478Item Rngdf-ringc 20646
[AhoHopUll] p. 2Section 1.1df-bigo 48469
[AhoHopUll] p. 12Section 1.3df-blen 48491
[AhoHopUll] p. 318Section 9.1df-concat 14609  df-pfx 14709  df-substr 14679  df-word 14553  lencl 14571  wrd0 14577
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24729  df-nmoo 30764
[AkhiezerGlazman] p. 64Theoremhmopidmch 32172  hmopidmchi 32170
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32220  pjcmul2i 32221
[AkhiezerGlazman] p. 72Theoremcnvunop 31937  unoplin 31939
[AkhiezerGlazman] p. 72Equation 2unopadj 31938  unopadj2 31957
[AkhiezerGlazman] p. 73Theoremelunop2 32032  lnopunii 32031
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32105
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27961
[Alling] p. 184Axiom Bbdayfo 27722
[Alling] p. 184Axiom Osltso 27721
[Alling] p. 184Axiom SDnodense 27737
[Alling] p. 185Lemma 0nocvxmin 27823
[Alling] p. 185Theoremconway 27844
[Alling] p. 185Axiom FEnoeta 27788
[Alling] p. 186Theorem 4slerec 27864
[Alling], p. 2Definitionrp-brsslt 43436
[Alling], p. 3Notenla0001 43439  nla0002 43437  nla0003 43438
[Apostol] p. 18Theorem I.1addcan 11445  addcan2d 11465  addcan2i 11455  addcand 11464  addcani 11454
[Apostol] p. 18Theorem I.2negeu 11498
[Apostol] p. 18Theorem I.3negsub 11557  negsubd 11626  negsubi 11587
[Apostol] p. 18Theorem I.4negneg 11559  negnegd 11611  negnegi 11579
[Apostol] p. 18Theorem I.5subdi 11696  subdid 11719  subdii 11712  subdir 11697  subdird 11720  subdiri 11713
[Apostol] p. 18Theorem I.6mul01 11440  mul01d 11460  mul01i 11451  mul02 11439  mul02d 11459  mul02i 11450
[Apostol] p. 18Theorem I.7mulcan 11900  mulcan2d 11897  mulcand 11896  mulcani 11902
[Apostol] p. 18Theorem I.8receu 11908  xreceu 32904
[Apostol] p. 18Theorem I.9divrec 11938  divrecd 12046  divreci 12012  divreczi 12005
[Apostol] p. 18Theorem I.10recrec 11964  recreci 11999
[Apostol] p. 18Theorem I.11mul0or 11903  mul0ord 11913  mul0ori 11911
[Apostol] p. 18Theorem I.12mul2neg 11702  mul2negd 11718  mul2negi 11711  mulneg1 11699  mulneg1d 11716  mulneg1i 11709
[Apostol] p. 18Theorem I.13divadddiv 11982  divadddivd 12087  divadddivi 12029
[Apostol] p. 18Theorem I.14divmuldiv 11967  divmuldivd 12084  divmuldivi 12027  rdivmuldivd 20413
[Apostol] p. 18Theorem I.15divdivdiv 11968  divdivdivd 12090  divdivdivi 12030
[Apostol] p. 20Axiom 7rpaddcl 13057  rpaddcld 13092  rpmulcl 13058  rpmulcld 13093
[Apostol] p. 20Axiom 8rpneg 13067
[Apostol] p. 20Axiom 90nrp 13070
[Apostol] p. 20Theorem I.17lttri 11387
[Apostol] p. 20Theorem I.18ltadd1d 11856  ltadd1dd 11874  ltadd1i 11817
[Apostol] p. 20Theorem I.19ltmul1 12117  ltmul1a 12116  ltmul1i 12186  ltmul1ii 12196  ltmul2 12118  ltmul2d 13119  ltmul2dd 13133  ltmul2i 12189
[Apostol] p. 20Theorem I.20msqgt0 11783  msqgt0d 11830  msqgt0i 11800
[Apostol] p. 20Theorem I.210lt1 11785
[Apostol] p. 20Theorem I.23lt0neg1 11769  lt0neg1d 11832  ltneg 11763  ltnegd 11841  ltnegi 11807
[Apostol] p. 20Theorem I.25lt2add 11748  lt2addd 11886  lt2addi 11825
[Apostol] p. 20Definition of positive numbersdf-rp 13035
[Apostol] p. 21Exercise 4recgt0 12113  recgt0d 12202  recgt0i 12173  recgt0ii 12174
[Apostol] p. 22Definition of integersdf-z 12614
[Apostol] p. 22Definition of positive integersdfnn3 12280
[Apostol] p. 22Definition of rationalsdf-q 12991
[Apostol] p. 24Theorem I.26supeu 9494
[Apostol] p. 26Theorem I.28nnunb 12522
[Apostol] p. 26Theorem I.29arch 12523  archd 45167
[Apostol] p. 28Exercise 2btwnz 12721
[Apostol] p. 28Exercise 3nnrecl 12524
[Apostol] p. 28Exercise 4rebtwnz 12989
[Apostol] p. 28Exercise 5zbtwnre 12988
[Apostol] p. 28Exercise 6qbtwnre 13241
[Apostol] p. 28Exercise 10(a)zeneo 16376  zneo 12701  zneoALTV 47656
[Apostol] p. 29Theorem I.35cxpsqrtth 26772  msqsqrtd 15479  resqrtth 15294  sqrtth 15403  sqrtthi 15409  sqsqrtd 15478
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12269
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12955
[Apostol] p. 361Remarkcrreczi 14267
[Apostol] p. 363Remarkabsgt0i 15438
[Apostol] p. 363Exampleabssubd 15492  abssubi 15442
[ApostolNT] p. 7Remarkfmtno0 47527  fmtno1 47528  fmtno2 47537  fmtno3 47538  fmtno4 47539  fmtno5fac 47569  fmtnofz04prm 47564
[ApostolNT] p. 7Definitiondf-fmtno 47515
[ApostolNT] p. 8Definitiondf-ppi 27143
[ApostolNT] p. 14Definitiondf-dvds 16291
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16307
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16331
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16326
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16320
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16322
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16308
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16309
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16314
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16348
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16350
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16352
[ApostolNT] p. 15Definitiondf-gcd 16532  dfgcd2 16583
[ApostolNT] p. 16Definitionisprm2 16719
[ApostolNT] p. 16Theorem 1.5coprmdvds 16690
[ApostolNT] p. 16Theorem 1.7prminf 16953
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16550
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16584
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16586
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16565
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16557
[ApostolNT] p. 17Theorem 1.8coprm 16748
[ApostolNT] p. 17Theorem 1.9euclemma 16750
[ApostolNT] p. 17Theorem 1.101arith2 16966
[ApostolNT] p. 18Theorem 1.13prmrec 16960
[ApostolNT] p. 19Theorem 1.14divalg 16440
[ApostolNT] p. 20Theorem 1.15eucalg 16624
[ApostolNT] p. 24Definitiondf-mu 27144
[ApostolNT] p. 25Definitiondf-phi 16803
[ApostolNT] p. 25Theorem 2.1musum 27234
[ApostolNT] p. 26Theorem 2.2phisum 16828
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16813
[ApostolNT] p. 28Theorem 2.5(c)phimul 16817
[ApostolNT] p. 32Definitiondf-vma 27141
[ApostolNT] p. 32Theorem 2.9muinv 27236
[ApostolNT] p. 32Theorem 2.10vmasum 27260
[ApostolNT] p. 38Remarkdf-sgm 27145
[ApostolNT] p. 38Definitiondf-sgm 27145
[ApostolNT] p. 75Definitiondf-chp 27142  df-cht 27140
[ApostolNT] p. 104Definitioncongr 16701
[ApostolNT] p. 106Remarkdvdsval3 16294
[ApostolNT] p. 106Definitionmoddvds 16301
[ApostolNT] p. 107Example 2mod2eq0even 16383
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16384
[ApostolNT] p. 107Example 4zmod1congr 13928
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13966
[ApostolNT] p. 107Theorem 5.2(c)modexp 14277
[ApostolNT] p. 108Theorem 5.3modmulconst 16325
[ApostolNT] p. 109Theorem 5.4cncongr1 16704
[ApostolNT] p. 109Theorem 5.6gcdmodi 17112
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16706
[ApostolNT] p. 113Theorem 5.17eulerth 16820
[ApostolNT] p. 113Theorem 5.18vfermltl 16839
[ApostolNT] p. 114Theorem 5.19fermltl 16821
[ApostolNT] p. 116Theorem 5.24wilthimp 27115
[ApostolNT] p. 179Definitiondf-lgs 27339  lgsprme0 27383
[ApostolNT] p. 180Example 11lgs 27384
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27360
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27375
[ApostolNT] p. 181Theorem 9.4m1lgs 27432
[ApostolNT] p. 181Theorem 9.52lgs 27451  2lgsoddprm 27460
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27418
[ApostolNT] p. 185Theorem 9.8lgsquad 27427
[ApostolNT] p. 188Definitiondf-lgs 27339  lgs1 27385
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27376
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27378
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27386
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27387
[Baer] p. 40Property (b)mapdord 41640
[Baer] p. 40Property (c)mapd11 41641
[Baer] p. 40Property (e)mapdin 41664  mapdlsm 41666
[Baer] p. 40Property (f)mapd0 41667
[Baer] p. 40Definition of projectivitydf-mapd 41627  mapd1o 41650
[Baer] p. 41Property (g)mapdat 41669
[Baer] p. 44Part (1)mapdpg 41708
[Baer] p. 45Part (2)hdmap1eq 41803  mapdheq 41730  mapdheq2 41731  mapdheq2biN 41732
[Baer] p. 45Part (3)baerlem3 41715
[Baer] p. 46Part (4)mapdheq4 41734  mapdheq4lem 41733
[Baer] p. 46Part (5)baerlem5a 41716  baerlem5abmN 41720  baerlem5amN 41718  baerlem5b 41717  baerlem5bmN 41719
[Baer] p. 47Part (6)hdmap1l6 41823  hdmap1l6a 41811  hdmap1l6e 41816  hdmap1l6f 41817  hdmap1l6g 41818  hdmap1l6lem1 41809  hdmap1l6lem2 41810  mapdh6N 41749  mapdh6aN 41737  mapdh6eN 41742  mapdh6fN 41743  mapdh6gN 41744  mapdh6lem1N 41735  mapdh6lem2N 41736
[Baer] p. 48Part 9hdmapval 41830
[Baer] p. 48Part 10hdmap10 41842
[Baer] p. 48Part 11hdmapadd 41845
[Baer] p. 48Part (6)hdmap1l6h 41819  mapdh6hN 41745
[Baer] p. 48Part (7)mapdh75cN 41755  mapdh75d 41756  mapdh75e 41754  mapdh75fN 41757  mapdh7cN 41751  mapdh7dN 41752  mapdh7eN 41750  mapdh7fN 41753
[Baer] p. 48Part (8)mapdh8 41790  mapdh8a 41777  mapdh8aa 41778  mapdh8ab 41779  mapdh8ac 41780  mapdh8ad 41781  mapdh8b 41782  mapdh8c 41783  mapdh8d 41785  mapdh8d0N 41784  mapdh8e 41786  mapdh8g 41787  mapdh8i 41788  mapdh8j 41789
[Baer] p. 48Part (9)mapdh9a 41791
[Baer] p. 48Equation 10mapdhvmap 41771
[Baer] p. 49Part 12hdmap11 41850  hdmapeq0 41846  hdmapf1oN 41867  hdmapneg 41848  hdmaprnN 41866  hdmaprnlem1N 41851  hdmaprnlem3N 41852  hdmaprnlem3uN 41853  hdmaprnlem4N 41855  hdmaprnlem6N 41856  hdmaprnlem7N 41857  hdmaprnlem8N 41858  hdmaprnlem9N 41859  hdmapsub 41849
[Baer] p. 49Part 14hdmap14lem1 41870  hdmap14lem10 41879  hdmap14lem1a 41868  hdmap14lem2N 41871  hdmap14lem2a 41869  hdmap14lem3 41872  hdmap14lem8 41877  hdmap14lem9 41878
[Baer] p. 50Part 14hdmap14lem11 41880  hdmap14lem12 41881  hdmap14lem13 41882  hdmap14lem14 41883  hdmap14lem15 41884  hgmapval 41889
[Baer] p. 50Part 15hgmapadd 41896  hgmapmul 41897  hgmaprnlem2N 41899  hgmapvs 41893
[Baer] p. 50Part 16hgmaprnN 41903
[Baer] p. 110Lemma 1hdmapip0com 41919
[Baer] p. 110Line 27hdmapinvlem1 41920
[Baer] p. 110Line 28hdmapinvlem2 41921
[Baer] p. 110Line 30hdmapinvlem3 41922
[Baer] p. 110Part 1.2hdmapglem5 41924  hgmapvv 41928
[Baer] p. 110Proposition 1hdmapinvlem4 41923
[Baer] p. 111Line 10hgmapvvlem1 41925
[Baer] p. 111Line 15hdmapg 41932  hdmapglem7 41931
[Bauer], p. 483Theorem 1.22irrexpq 26773  2irrexpqALT 26843
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2569
[BellMachover] p. 460Notationdf-mo 2540
[BellMachover] p. 460Definitionmo3 2564
[BellMachover] p. 461Axiom Extax-ext 2708
[BellMachover] p. 462Theorem 1.1axextmo 2712
[BellMachover] p. 463Axiom Repaxrep5 5287
[BellMachover] p. 463Scheme Sepax-sep 5296
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37065  sepex 5300
[BellMachover] p. 466Problemaxpow2 5367
[BellMachover] p. 466Axiom Powaxpow3 5368
[BellMachover] p. 466Axiom Unionaxun2 7757
[BellMachover] p. 468Definitiondf-ord 6387
[BellMachover] p. 469Theorem 2.2(i)ordirr 6402
[BellMachover] p. 469Theorem 2.2(iii)onelon 6409
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6404
[BellMachover] p. 471Definition of Ndf-om 7888
[BellMachover] p. 471Problem 2.5(ii)uniordint 7821
[BellMachover] p. 471Definition of Limdf-lim 6389
[BellMachover] p. 472Axiom Infzfinf2 9682
[BellMachover] p. 473Theorem 2.8limom 7903
[BellMachover] p. 477Equation 3.1df-r1 9804
[BellMachover] p. 478Definitionrankval2 9858
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9822  r1ord3g 9819
[BellMachover] p. 480Axiom Regzfreg 9635
[BellMachover] p. 488Axiom ACac5 10517  dfac4 10162
[BellMachover] p. 490Definition of alephalephval3 10150
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39320
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32372
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32414  chirredi 32413
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32402
[Beran] p. 3Definition of joinsshjval3 31373
[Beran] p. 39Theorem 2.3(i)cmcm2 31635  cmcm2i 31612  cmcm2ii 31617  cmt2N 39251
[Beran] p. 40Theorem 2.3(iii)lecm 31636  lecmi 31621  lecmii 31622
[Beran] p. 45Theorem 3.4cmcmlem 31610
[Beran] p. 49Theorem 4.2cm2j 31639  cm2ji 31644  cm2mi 31645
[Beran] p. 95Definitiondf-sh 31226  issh2 31228
[Beran] p. 95Lemma 3.1(S5)his5 31105
[Beran] p. 95Lemma 3.1(S6)his6 31118
[Beran] p. 95Lemma 3.1(S7)his7 31109
[Beran] p. 95Lemma 3.2(S8)ho01i 31847
[Beran] p. 95Lemma 3.2(S9)hoeq1 31849
[Beran] p. 95Lemma 3.2(S10)ho02i 31848
[Beran] p. 95Lemma 3.2(S11)hoeq2 31850
[Beran] p. 95Postulate (S1)ax-his1 31101  his1i 31119
[Beran] p. 95Postulate (S2)ax-his2 31102
[Beran] p. 95Postulate (S3)ax-his3 31103
[Beran] p. 95Postulate (S4)ax-his4 31104
[Beran] p. 96Definition of normdf-hnorm 30987  dfhnorm2 31141  normval 31143
[Beran] p. 96Definition for Cauchy sequencehcau 31203
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30992
[Beran] p. 96Definition of complete subspaceisch3 31260
[Beran] p. 96Definition of convergedf-hlim 30991  hlimi 31207
[Beran] p. 97Theorem 3.3(i)norm-i-i 31152  norm-i 31148
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31156  norm-ii 31157  normlem0 31128  normlem1 31129  normlem2 31130  normlem3 31131  normlem4 31132  normlem5 31133  normlem6 31134  normlem7 31135  normlem7tALT 31138
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31158  norm-iii 31159
[Beran] p. 98Remark 3.4bcs 31200  bcsiALT 31198  bcsiHIL 31199
[Beran] p. 98Remark 3.4(B)normlem9at 31140  normpar 31174  normpari 31173
[Beran] p. 98Remark 3.4(C)normpyc 31165  normpyth 31164  normpythi 31161
[Beran] p. 99Remarklnfn0 32066  lnfn0i 32061  lnop0 31985  lnop0i 31989
[Beran] p. 99Theorem 3.5(i)nmcexi 32045  nmcfnex 32072  nmcfnexi 32070  nmcopex 32048  nmcopexi 32046
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32073  nmcfnlbi 32071  nmcoplb 32049  nmcoplbi 32047
[Beran] p. 99Theorem 3.5(iii)lnfncon 32075  lnfnconi 32074  lnopcon 32054  lnopconi 32053
[Beran] p. 100Lemma 3.6normpar2i 31175
[Beran] p. 101Lemma 3.6norm3adifi 31172  norm3adifii 31167  norm3dif 31169  norm3difi 31166
[Beran] p. 102Theorem 3.7(i)chocunii 31320  pjhth 31412  pjhtheu 31413  pjpjhth 31444  pjpjhthi 31445  pjth 25473
[Beran] p. 102Theorem 3.7(ii)ococ 31425  ococi 31424
[Beran] p. 103Remark 3.8nlelchi 32080
[Beran] p. 104Theorem 3.9riesz3i 32081  riesz4 32083  riesz4i 32082
[Beran] p. 104Theorem 3.10cnlnadj 32098  cnlnadjeu 32097  cnlnadjeui 32096  cnlnadji 32095  cnlnadjlem1 32086  nmopadjlei 32107
[Beran] p. 106Theorem 3.11(i)adjeq0 32110
[Beran] p. 106Theorem 3.11(v)nmopadji 32109
[Beran] p. 106Theorem 3.11(ii)adjmul 32111
[Beran] p. 106Theorem 3.11(iv)adjadj 31955
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32121  nmopcoadji 32120
[Beran] p. 106Theorem 3.11(iii)adjadd 32112
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32122
[Beran] p. 106Theorem 3.11(viii)adjcoi 32119  pjadj2coi 32223  pjadjcoi 32180
[Beran] p. 107Definitiondf-ch 31240  isch2 31242
[Beran] p. 107Remark 3.12choccl 31325  isch3 31260  occl 31323  ocsh 31302  shoccl 31324  shocsh 31303
[Beran] p. 107Remark 3.12(B)ococin 31427
[Beran] p. 108Theorem 3.13chintcl 31351
[Beran] p. 109Property (i)pjadj2 32206  pjadj3 32207  pjadji 31704  pjadjii 31693
[Beran] p. 109Property (ii)pjidmco 32200  pjidmcoi 32196  pjidmi 31692
[Beran] p. 110Definition of projector orderingpjordi 32192
[Beran] p. 111Remarkho0val 31769  pjch1 31689
[Beran] p. 111Definitiondf-hfmul 31753  df-hfsum 31752  df-hodif 31751  df-homul 31750  df-hosum 31749
[Beran] p. 111Lemma 4.4(i)pjo 31690
[Beran] p. 111Lemma 4.4(ii)pjch 31713  pjchi 31451
[Beran] p. 111Lemma 4.4(iii)pjoc2 31458  pjoc2i 31457
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31699
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32184  pjssmii 31700
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32183
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32182
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32187
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32185  pjssge0ii 31701
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32186  pjdifnormii 31702
[Bobzien] p. 116Statement T3stoic3 1776
[Bobzien] p. 117Statement T2stoic2a 1774
[Bobzien] p. 117Statement T4stoic4a 1777
[Bobzien] p. 117Conclusion the contradictorystoic1a 1772
[Bogachev] p. 16Definition 1.5df-oms 34294
[Bogachev] p. 17Lemma 1.5.4omssubadd 34302
[Bogachev] p. 17Example 1.5.2omsmon 34300
[Bogachev] p. 41Definition 1.11.2df-carsg 34304
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34324
[Bogachev] p. 116Definition 2.3.1df-itgm 34355  df-sitm 34333
[Bogachev] p. 118Chapter 2.4.4df-itgm 34355
[Bogachev] p. 118Definition 2.4.1df-sitg 34332
[Bollobas] p. 1Section I.1df-edg 29065  isuhgrop 29087  isusgrop 29179  isuspgrop 29178
[Bollobas] p. 2Section I.1df-isubgr 47847  df-subgr 29285  uhgrspan1 29320  uhgrspansubgr 29308
[Bollobas] p. 3Definitiondf-gric 47867  gricuspgr 47887  isuspgrim 47875
[Bollobas] p. 3Section I.1cusgrsize 29472  df-clnbgr 47806  df-cusgr 29429  df-nbgr 29350  fusgrmaxsize 29482
[Bollobas] p. 4Definitiondf-upwlks 48050  df-wlks 29617
[Bollobas] p. 4Section I.1finsumvtxdg2size 29568  finsumvtxdgeven 29570  fusgr1th 29569  fusgrvtxdgonume 29572  vtxdgoddnumeven 29571
[Bollobas] p. 5Notationdf-pths 29734
[Bollobas] p. 5Definitiondf-crcts 29806  df-cycls 29807  df-trls 29710  df-wlkson 29618
[Bollobas] p. 7Section I.1df-ushgr 29076
[BourbakiAlg1] p. 1Definition 1df-clintop 48116  df-cllaw 48102  df-mgm 18653  df-mgm2 48135
[BourbakiAlg1] p. 4Definition 5df-assintop 48117  df-asslaw 48104  df-sgrp 18732  df-sgrp2 48137
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48136  df-comlaw 48103
[BourbakiAlg1] p. 12Definition 2df-mnd 18748
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33031  mndlactf1o 33035  mndractf1 33033  mndractf1o 33036
[BourbakiAlg1] p. 92Definition 1df-ring 20232
[BourbakiAlg1] p. 93Section I.8.1df-rng 20150
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33684
[BourbakiAlg2] p. 113Chapter 5.assafld 33688  assarrginv 33687
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33728  fldextrspunfld 33726  fldextrspunlem1 33725  fldextrspunlem2 33727  fldextrspunlsp 33724  fldextrspunlsplem 33723
[BourbakiCAlg2], p. 228Proposition 21arithidom 33565  dfufd2 33578
[BourbakiEns] p. Proposition 8fcof1 7307  fcofo 7308
[BourbakiTop1] p. Remarkxnegmnf 13252  xnegpnf 13251
[BourbakiTop1] p. Remark rexneg 13253
[BourbakiTop1] p. Remark 3ust0 24228  ustfilxp 24221
[BourbakiTop1] p. Axiom GT'tgpsubcn 24098
[BourbakiTop1] p. Criterionishmeo 23767
[BourbakiTop1] p. Example 1cstucnd 24293  iducn 24292  snfil 23872
[BourbakiTop1] p. Example 2neifil 23888
[BourbakiTop1] p. Theorem 1cnextcn 24075
[BourbakiTop1] p. Theorem 2ucnextcn 24313
[BourbakiTop1] p. Theorem 3df-hcmp 33956
[BourbakiTop1] p. Paragraph 3infil 23871
[BourbakiTop1] p. Definition 1df-ucn 24285  df-ust 24209  filintn0 23869  filn0 23870  istgp 24085  ucnprima 24291
[BourbakiTop1] p. Definition 2df-cfilu 24296
[BourbakiTop1] p. Definition 3df-cusp 24307  df-usp 24266  df-utop 24240  trust 24238
[BourbakiTop1] p. Definition 6df-pcmp 33855
[BourbakiTop1] p. Property V_issnei2 23124
[BourbakiTop1] p. Theorem 1(d)iscncl 23277
[BourbakiTop1] p. Condition F_Iustssel 24214
[BourbakiTop1] p. Condition U_Iustdiag 24217
[BourbakiTop1] p. Property V_iiinnei 23133
[BourbakiTop1] p. Property V_ivneiptopreu 23141  neissex 23135
[BourbakiTop1] p. Proposition 1neips 23121  neiss 23117  ucncn 24294  ustund 24230  ustuqtop 24255
[BourbakiTop1] p. Proposition 2cnpco 23275  neiptopreu 23141  utop2nei 24259  utop3cls 24260
[BourbakiTop1] p. Proposition 3fmucnd 24301  uspreg 24283  utopreg 24261
[BourbakiTop1] p. Proposition 4imasncld 23699  imasncls 23700  imasnopn 23698
[BourbakiTop1] p. Proposition 9cnpflf2 24008
[BourbakiTop1] p. Condition F_IIustincl 24216
[BourbakiTop1] p. Condition U_IIustinvel 24218
[BourbakiTop1] p. Property V_iiielnei 23119
[BourbakiTop1] p. Proposition 11cnextucn 24312
[BourbakiTop1] p. Condition F_IIbustbasel 24215
[BourbakiTop1] p. Condition U_IIIustexhalf 24219
[BourbakiTop1] p. Definition C'''df-cmp 23395
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23854
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22900
[BourbakiTop2] p. 195Definition 1df-ldlf 33852
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46077
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46079  stoweid 46078
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46016  stoweidlem10 46025  stoweidlem14 46029  stoweidlem15 46030  stoweidlem35 46050  stoweidlem36 46051  stoweidlem37 46052  stoweidlem38 46053  stoweidlem40 46055  stoweidlem41 46056  stoweidlem43 46058  stoweidlem44 46059  stoweidlem46 46061  stoweidlem5 46020  stoweidlem50 46065  stoweidlem52 46067  stoweidlem53 46068  stoweidlem55 46070  stoweidlem56 46071
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46038  stoweidlem24 46039  stoweidlem27 46042  stoweidlem28 46043  stoweidlem30 46045
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46049  stoweidlem59 46074  stoweidlem60 46075
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46060  stoweidlem49 46064  stoweidlem7 46022
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46046  stoweidlem39 46054  stoweidlem42 46057  stoweidlem48 46063  stoweidlem51 46066  stoweidlem54 46069  stoweidlem57 46072  stoweidlem58 46073
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46040
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46032
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46026  stoweidlem13 46028  stoweidlem26 46041  stoweidlem61 46076
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46033
[Bruck] p. 1Section I.1df-clintop 48116  df-mgm 18653  df-mgm2 48135
[Bruck] p. 23Section II.1df-sgrp 18732  df-sgrp2 48137
[Bruck] p. 28Theorem 3.2dfgrp3 19057
[ChoquetDD] p. 2Definition of mappingdf-mpt 5226
[Church] p. 129Section II.24df-ifp 1064  dfifp2 1065
[Clemente] p. 10Definition ITnatded 30422
[Clemente] p. 10Definition I` `m,nnatded 30422
[Clemente] p. 11Definition E=>m,nnatded 30422
[Clemente] p. 11Definition I=>m,nnatded 30422
[Clemente] p. 11Definition E` `(1)natded 30422
[Clemente] p. 11Definition E` `(2)natded 30422
[Clemente] p. 12Definition E` `m,n,pnatded 30422
[Clemente] p. 12Definition I` `n(1)natded 30422
[Clemente] p. 12Definition I` `n(2)natded 30422
[Clemente] p. 13Definition I` `m,n,pnatded 30422
[Clemente] p. 14Proof 5.11natded 30422
[Clemente] p. 14Definition E` `nnatded 30422
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30424  ex-natded5.2 30423
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30427  ex-natded5.3 30426
[Clemente] p. 18Theorem 5.5ex-natded5.5 30429
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30431  ex-natded5.7 30430
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30433  ex-natded5.8 30432
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30435  ex-natded5.13 30434
[Clemente] p. 32Definition I` `nnatded 30422
[Clemente] p. 32Definition E` `m,n,p,anatded 30422
[Clemente] p. 32Definition E` `n,tnatded 30422
[Clemente] p. 32Definition I` `n,tnatded 30422
[Clemente] p. 43Theorem 9.20ex-natded9.20 30436
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30437
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30439  ex-natded9.26 30438
[Cohen] p. 301Remarkrelogoprlem 26633
[Cohen] p. 301Property 2relogmul 26634  relogmuld 26667
[Cohen] p. 301Property 3relogdiv 26635  relogdivd 26668
[Cohen] p. 301Property 4relogexp 26638
[Cohen] p. 301Property 1alog1 26627
[Cohen] p. 301Property 1bloge 26628
[Cohen4] p. 348Observationrelogbcxpb 26830
[Cohen4] p. 349Propertyrelogbf 26834
[Cohen4] p. 352Definitionelogb 26813
[Cohen4] p. 361Property 2relogbmul 26820
[Cohen4] p. 361Property 3logbrec 26825  relogbdiv 26822
[Cohen4] p. 361Property 4relogbreexp 26818
[Cohen4] p. 361Property 6relogbexp 26823
[Cohen4] p. 361Property 1(a)logbid1 26811
[Cohen4] p. 361Property 1(b)logb1 26812
[Cohen4] p. 367Propertylogbchbase 26814
[Cohen4] p. 377Property 2logblt 26827
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34287  sxbrsigalem4 34289
[Cohn] p. 81Section II.5acsdomd 18602  acsinfd 18601  acsinfdimd 18603  acsmap2d 18600  acsmapd 18599
[Cohn] p. 143Example 5.1.1sxbrsiga 34292
[Connell] p. 57Definitiondf-scmat 22497  df-scmatalt 48316
[Conway] p. 4Definitionslerec 27864
[Conway] p. 5Definitionaddsval 27995  addsval2 27996  df-adds 27993  df-muls 28133  df-negs 28053
[Conway] p. 7Theorem0slt1s 27874
[Conway] p. 16Theorem 0(i)ssltright 27910
[Conway] p. 16Theorem 0(ii)ssltleft 27909
[Conway] p. 16Theorem 0(iii)slerflex 27808
[Conway] p. 17Theorem 3addsass 28038  addsassd 28039  addscom 27999  addscomd 28000  addsrid 27997  addsridd 27998
[Conway] p. 17Definitiondf-0s 27869
[Conway] p. 17Theorem 4(ii)negnegs 28076
[Conway] p. 17Theorem 4(iii)negsid 28073  negsidd 28074
[Conway] p. 18Theorem 5sleadd1 28022  sleadd1d 28028
[Conway] p. 18Definitiondf-1s 27870
[Conway] p. 18Theorem 6(ii)negscl 28068  negscld 28069
[Conway] p. 18Theorem 6(iii)addscld 28013
[Conway] p. 19Notemulsunif2 28196
[Conway] p. 19Theorem 7addsdi 28181  addsdid 28182  addsdird 28183  mulnegs1d 28186  mulnegs2d 28187  mulsass 28192  mulsassd 28193  mulscom 28165  mulscomd 28166
[Conway] p. 19Theorem 8(i)mulscl 28160  mulscld 28161
[Conway] p. 19Theorem 8(iii)slemuld 28164  sltmul 28162  sltmuld 28163
[Conway] p. 20Theorem 9mulsgt0 28170  mulsgt0d 28171
[Conway] p. 21Theorem 10(iv)precsex 28242
[Conway] p. 24Definitiondf-reno 28426
[Conway] p. 24Theorem 13(ii)readdscl 28431  remulscl 28434  renegscl 28430
[Conway] p. 27Definitiondf-ons 28275  elons2 28281
[Conway] p. 27Theorem 14sltonex 28284
[Conway] p. 29Remarkmadebday 27938  newbday 27940  oldbday 27939
[Conway] p. 29Definitiondf-made 27886  df-new 27888  df-old 27887
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13901
[Crawley] p. 1Definition of posetdf-poset 18359
[Crawley] p. 107Theorem 13.2hlsupr 39388
[Crawley] p. 110Theorem 13.3arglem1N 40192  dalaw 39888
[Crawley] p. 111Theorem 13.4hlathil 41967
[Crawley] p. 111Definition of set Wdf-watsN 39992
[Crawley] p. 111Definition of dilationdf-dilN 40108  df-ldil 40106  isldil 40112
[Crawley] p. 111Definition of translationdf-ltrn 40107  df-trnN 40109  isltrn 40121  ltrnu 40123
[Crawley] p. 112Lemma Acdlema1N 39793  cdlema2N 39794  exatleN 39406
[Crawley] p. 112Lemma B1cvrat 39478  cdlemb 39796  cdlemb2 40043  cdlemb3 40608  idltrn 40152  l1cvat 39056  lhpat 40045  lhpat2 40047  lshpat 39057  ltrnel 40141  ltrnmw 40153
[Crawley] p. 112Lemma Ccdlemc1 40193  cdlemc2 40194  ltrnnidn 40176  trlat 40171  trljat1 40168  trljat2 40169  trljat3 40170  trlne 40187  trlnidat 40175  trlnle 40188
[Crawley] p. 112Definition of automorphismdf-pautN 39993
[Crawley] p. 113Lemma Ccdlemc 40199  cdlemc3 40195  cdlemc4 40196
[Crawley] p. 113Lemma Dcdlemd 40209  cdlemd1 40200  cdlemd2 40201  cdlemd3 40202  cdlemd4 40203  cdlemd5 40204  cdlemd6 40205  cdlemd7 40206  cdlemd8 40207  cdlemd9 40208  cdleme31sde 40387  cdleme31se 40384  cdleme31se2 40385  cdleme31snd 40388  cdleme32a 40443  cdleme32b 40444  cdleme32c 40445  cdleme32d 40446  cdleme32e 40447  cdleme32f 40448  cdleme32fva 40439  cdleme32fva1 40440  cdleme32fvcl 40442  cdleme32le 40449  cdleme48fv 40501  cdleme4gfv 40509  cdleme50eq 40543  cdleme50f 40544  cdleme50f1 40545  cdleme50f1o 40548  cdleme50laut 40549  cdleme50ldil 40550  cdleme50lebi 40542  cdleme50rn 40547  cdleme50rnlem 40546  cdlemeg49le 40513  cdlemeg49lebilem 40541
[Crawley] p. 113Lemma Ecdleme 40562  cdleme00a 40211  cdleme01N 40223  cdleme02N 40224  cdleme0a 40213  cdleme0aa 40212  cdleme0b 40214  cdleme0c 40215  cdleme0cp 40216  cdleme0cq 40217  cdleme0dN 40218  cdleme0e 40219  cdleme0ex1N 40225  cdleme0ex2N 40226  cdleme0fN 40220  cdleme0gN 40221  cdleme0moN 40227  cdleme1 40229  cdleme10 40256  cdleme10tN 40260  cdleme11 40272  cdleme11a 40262  cdleme11c 40263  cdleme11dN 40264  cdleme11e 40265  cdleme11fN 40266  cdleme11g 40267  cdleme11h 40268  cdleme11j 40269  cdleme11k 40270  cdleme11l 40271  cdleme12 40273  cdleme13 40274  cdleme14 40275  cdleme15 40280  cdleme15a 40276  cdleme15b 40277  cdleme15c 40278  cdleme15d 40279  cdleme16 40287  cdleme16aN 40261  cdleme16b 40281  cdleme16c 40282  cdleme16d 40283  cdleme16e 40284  cdleme16f 40285  cdleme16g 40286  cdleme19a 40305  cdleme19b 40306  cdleme19c 40307  cdleme19d 40308  cdleme19e 40309  cdleme19f 40310  cdleme1b 40228  cdleme2 40230  cdleme20aN 40311  cdleme20bN 40312  cdleme20c 40313  cdleme20d 40314  cdleme20e 40315  cdleme20f 40316  cdleme20g 40317  cdleme20h 40318  cdleme20i 40319  cdleme20j 40320  cdleme20k 40321  cdleme20l 40324  cdleme20l1 40322  cdleme20l2 40323  cdleme20m 40325  cdleme20y 40304  cdleme20zN 40303  cdleme21 40339  cdleme21d 40332  cdleme21e 40333  cdleme22a 40342  cdleme22aa 40341  cdleme22b 40343  cdleme22cN 40344  cdleme22d 40345  cdleme22e 40346  cdleme22eALTN 40347  cdleme22f 40348  cdleme22f2 40349  cdleme22g 40350  cdleme23a 40351  cdleme23b 40352  cdleme23c 40353  cdleme26e 40361  cdleme26eALTN 40363  cdleme26ee 40362  cdleme26f 40365  cdleme26f2 40367  cdleme26f2ALTN 40366  cdleme26fALTN 40364  cdleme27N 40371  cdleme27a 40369  cdleme27cl 40368  cdleme28c 40374  cdleme3 40239  cdleme30a 40380  cdleme31fv 40392  cdleme31fv1 40393  cdleme31fv1s 40394  cdleme31fv2 40395  cdleme31id 40396  cdleme31sc 40386  cdleme31sdnN 40389  cdleme31sn 40382  cdleme31sn1 40383  cdleme31sn1c 40390  cdleme31sn2 40391  cdleme31so 40381  cdleme35a 40450  cdleme35b 40452  cdleme35c 40453  cdleme35d 40454  cdleme35e 40455  cdleme35f 40456  cdleme35fnpq 40451  cdleme35g 40457  cdleme35h 40458  cdleme35h2 40459  cdleme35sn2aw 40460  cdleme35sn3a 40461  cdleme36a 40462  cdleme36m 40463  cdleme37m 40464  cdleme38m 40465  cdleme38n 40466  cdleme39a 40467  cdleme39n 40468  cdleme3b 40231  cdleme3c 40232  cdleme3d 40233  cdleme3e 40234  cdleme3fN 40235  cdleme3fa 40238  cdleme3g 40236  cdleme3h 40237  cdleme4 40240  cdleme40m 40469  cdleme40n 40470  cdleme40v 40471  cdleme40w 40472  cdleme41fva11 40479  cdleme41sn3aw 40476  cdleme41sn4aw 40477  cdleme41snaw 40478  cdleme42a 40473  cdleme42b 40480  cdleme42c 40474  cdleme42d 40475  cdleme42e 40481  cdleme42f 40482  cdleme42g 40483  cdleme42h 40484  cdleme42i 40485  cdleme42k 40486  cdleme42ke 40487  cdleme42keg 40488  cdleme42mN 40489  cdleme42mgN 40490  cdleme43aN 40491  cdleme43bN 40492  cdleme43cN 40493  cdleme43dN 40494  cdleme5 40242  cdleme50ex 40561  cdleme50ltrn 40559  cdleme51finvN 40558  cdleme51finvfvN 40557  cdleme51finvtrN 40560  cdleme6 40243  cdleme7 40251  cdleme7a 40245  cdleme7aa 40244  cdleme7b 40246  cdleme7c 40247  cdleme7d 40248  cdleme7e 40249  cdleme7ga 40250  cdleme8 40252  cdleme8tN 40257  cdleme9 40255  cdleme9a 40253  cdleme9b 40254  cdleme9tN 40259  cdleme9taN 40258  cdlemeda 40300  cdlemedb 40299  cdlemednpq 40301  cdlemednuN 40302  cdlemefr27cl 40405  cdlemefr32fva1 40412  cdlemefr32fvaN 40411  cdlemefrs32fva 40402  cdlemefrs32fva1 40403  cdlemefs27cl 40415  cdlemefs32fva1 40425  cdlemefs32fvaN 40424  cdlemesner 40298  cdlemeulpq 40222
[Crawley] p. 114Lemma E4atex 40078  4atexlem7 40077  cdleme0nex 40292  cdleme17a 40288  cdleme17c 40290  cdleme17d 40500  cdleme17d1 40291  cdleme17d2 40497  cdleme18a 40293  cdleme18b 40294  cdleme18c 40295  cdleme18d 40297  cdleme4a 40241
[Crawley] p. 115Lemma Ecdleme21a 40327  cdleme21at 40330  cdleme21b 40328  cdleme21c 40329  cdleme21ct 40331  cdleme21f 40334  cdleme21g 40335  cdleme21h 40336  cdleme21i 40337  cdleme22gb 40296
[Crawley] p. 116Lemma Fcdlemf 40565  cdlemf1 40563  cdlemf2 40564
[Crawley] p. 116Lemma Gcdlemftr1 40569  cdlemg16 40659  cdlemg28 40706  cdlemg28a 40695  cdlemg28b 40705  cdlemg3a 40599  cdlemg42 40731  cdlemg43 40732  cdlemg44 40735  cdlemg44a 40733  cdlemg46 40737  cdlemg47 40738  cdlemg9 40636  ltrnco 40721  ltrncom 40740  tgrpabl 40753  trlco 40729
[Crawley] p. 116Definition of Gdf-tgrp 40745
[Crawley] p. 117Lemma Gcdlemg17 40679  cdlemg17b 40664
[Crawley] p. 117Definition of Edf-edring-rN 40758  df-edring 40759
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40762
[Crawley] p. 118Remarktendopltp 40782
[Crawley] p. 118Lemma Hcdlemh 40819  cdlemh1 40817  cdlemh2 40818
[Crawley] p. 118Lemma Icdlemi 40822  cdlemi1 40820  cdlemi2 40821
[Crawley] p. 118Lemma Jcdlemj1 40823  cdlemj2 40824  cdlemj3 40825  tendocan 40826
[Crawley] p. 118Lemma Kcdlemk 40976  cdlemk1 40833  cdlemk10 40845  cdlemk11 40851  cdlemk11t 40948  cdlemk11ta 40931  cdlemk11tb 40933  cdlemk11tc 40947  cdlemk11u-2N 40891  cdlemk11u 40873  cdlemk12 40852  cdlemk12u-2N 40892  cdlemk12u 40874  cdlemk13-2N 40878  cdlemk13 40854  cdlemk14-2N 40880  cdlemk14 40856  cdlemk15-2N 40881  cdlemk15 40857  cdlemk16-2N 40882  cdlemk16 40859  cdlemk16a 40858  cdlemk17-2N 40883  cdlemk17 40860  cdlemk18-2N 40888  cdlemk18-3N 40902  cdlemk18 40870  cdlemk19-2N 40889  cdlemk19 40871  cdlemk19u 40972  cdlemk1u 40861  cdlemk2 40834  cdlemk20-2N 40894  cdlemk20 40876  cdlemk21-2N 40893  cdlemk21N 40875  cdlemk22-3 40903  cdlemk22 40895  cdlemk23-3 40904  cdlemk24-3 40905  cdlemk25-3 40906  cdlemk26-3 40908  cdlemk26b-3 40907  cdlemk27-3 40909  cdlemk28-3 40910  cdlemk29-3 40913  cdlemk3 40835  cdlemk30 40896  cdlemk31 40898  cdlemk32 40899  cdlemk33N 40911  cdlemk34 40912  cdlemk35 40914  cdlemk36 40915  cdlemk37 40916  cdlemk38 40917  cdlemk39 40918  cdlemk39u 40970  cdlemk4 40836  cdlemk41 40922  cdlemk42 40943  cdlemk42yN 40946  cdlemk43N 40965  cdlemk45 40949  cdlemk46 40950  cdlemk47 40951  cdlemk48 40952  cdlemk49 40953  cdlemk5 40838  cdlemk50 40954  cdlemk51 40955  cdlemk52 40956  cdlemk53 40959  cdlemk54 40960  cdlemk55 40963  cdlemk55u 40968  cdlemk56 40973  cdlemk5a 40837  cdlemk5auN 40862  cdlemk5u 40863  cdlemk6 40839  cdlemk6u 40864  cdlemk7 40850  cdlemk7u-2N 40890  cdlemk7u 40872  cdlemk8 40840  cdlemk9 40841  cdlemk9bN 40842  cdlemki 40843  cdlemkid 40938  cdlemkj-2N 40884  cdlemkj 40865  cdlemksat 40848  cdlemksel 40847  cdlemksv 40846  cdlemksv2 40849  cdlemkuat 40868  cdlemkuel-2N 40886  cdlemkuel-3 40900  cdlemkuel 40867  cdlemkuv-2N 40885  cdlemkuv2-2 40887  cdlemkuv2-3N 40901  cdlemkuv2 40869  cdlemkuvN 40866  cdlemkvcl 40844  cdlemky 40928  cdlemkyyN 40964  tendoex 40977
[Crawley] p. 120Remarkdva1dim 40987
[Crawley] p. 120Lemma Lcdleml1N 40978  cdleml2N 40979  cdleml3N 40980  cdleml4N 40981  cdleml5N 40982  cdleml6 40983  cdleml7 40984  cdleml8 40985  cdleml9 40986  dia1dim 41063
[Crawley] p. 120Lemma Mdia11N 41050  diaf11N 41051  dialss 41048  diaord 41049  dibf11N 41163  djajN 41139
[Crawley] p. 120Definition of isomorphism mapdiaval 41034
[Crawley] p. 121Lemma Mcdlemm10N 41120  dia2dimlem1 41066  dia2dimlem2 41067  dia2dimlem3 41068  dia2dimlem4 41069  dia2dimlem5 41070  diaf1oN 41132  diarnN 41131  dvheveccl 41114  dvhopN 41118
[Crawley] p. 121Lemma Ncdlemn 41214  cdlemn10 41208  cdlemn11 41213  cdlemn11a 41209  cdlemn11b 41210  cdlemn11c 41211  cdlemn11pre 41212  cdlemn2 41197  cdlemn2a 41198  cdlemn3 41199  cdlemn4 41200  cdlemn4a 41201  cdlemn5 41203  cdlemn5pre 41202  cdlemn6 41204  cdlemn7 41205  cdlemn8 41206  cdlemn9 41207  diclspsn 41196
[Crawley] p. 121Definition of phi(q)df-dic 41175
[Crawley] p. 122Lemma Ndih11 41267  dihf11 41269  dihjust 41219  dihjustlem 41218  dihord 41266  dihord1 41220  dihord10 41225  dihord11b 41224  dihord11c 41226  dihord2 41229  dihord2a 41221  dihord2b 41222  dihord2cN 41223  dihord2pre 41227  dihord2pre2 41228  dihordlem6 41215  dihordlem7 41216  dihordlem7b 41217
[Crawley] p. 122Definition of isomorphism mapdihffval 41232  dihfval 41233  dihval 41234
[Diestel] p. 3Definitiondf-gric 47867  df-grim 47864  isuspgrim 47875
[Diestel] p. 3Section 1.1df-cusgr 29429  df-nbgr 29350
[Diestel] p. 3Definition by df-grisom 47863
[Diestel] p. 4Section 1.1df-isubgr 47847  df-subgr 29285  uhgrspan1 29320  uhgrspansubgr 29308
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29572  vtxdgoddnumeven 29571
[Diestel] p. 27Section 1.10df-ushgr 29076
[EGA] p. 80Notation 1.1.1rspecval 33863
[EGA] p. 80Proposition 1.1.2zartop 33875
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33867  zarcls1 33868
[EGA] p. 81Corollary 1.1.8zart0 33878
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33881
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33884
[Eisenberg] p. 67Definition 5.3df-dif 3954
[Eisenberg] p. 82Definition 6.3dfom3 9687
[Eisenberg] p. 125Definition 8.21df-map 8868
[Eisenberg] p. 216Example 13.2(4)omenps 9695
[Eisenberg] p. 310Theorem 19.8cardprc 10020
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10595
[Enderton] p. 18Axiom of Empty Setaxnul 5305
[Enderton] p. 19Definitiondf-tp 4631
[Enderton] p. 26Exercise 5unissb 4939
[Enderton] p. 26Exercise 10pwel 5381
[Enderton] p. 28Exercise 7(b)pwun 5576
[Enderton] p. 30Theorem "Distributive laws"iinin1 5079  iinin2 5078  iinun2 5073  iunin1 5072  iunin1f 32570  iunin2 5071  uniin1 32564  uniin2 32565
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5077  iundif2 5074
[Enderton] p. 32Exercise 20unineq 4288
[Enderton] p. 33Exercise 23iinuni 5098
[Enderton] p. 33Exercise 25iununi 5099
[Enderton] p. 33Exercise 24(a)iinpw 5106
[Enderton] p. 33Exercise 24(b)iunpw 7791  iunpwss 5107
[Enderton] p. 36Definitionopthwiener 5519
[Enderton] p. 38Exercise 6(a)unipw 5455
[Enderton] p. 38Exercise 6(b)pwuni 4945
[Enderton] p. 41Lemma 3Dopeluu 5475  rnex 7932  rnexg 7924
[Enderton] p. 41Exercise 8dmuni 5925  rnuni 6168
[Enderton] p. 42Definition of a functiondffun7 6593  dffun8 6594
[Enderton] p. 43Definition of function valuefunfv2 6997
[Enderton] p. 43Definition of single-rootedfuncnv 6635
[Enderton] p. 44Definition (d)dfima2 6080  dfima3 6081
[Enderton] p. 47Theorem 3Hfvco2 7006
[Enderton] p. 49Axiom of Choice (first form)ac7 10513  ac7g 10514  df-ac 10156  dfac2 10172  dfac2a 10170  dfac2b 10171  dfac3 10161  dfac7 10173
[Enderton] p. 50Theorem 3K(a)imauni 7266
[Enderton] p. 52Definitiondf-map 8868
[Enderton] p. 53Exercise 21coass 6285
[Enderton] p. 53Exercise 27dmco 6274
[Enderton] p. 53Exercise 14(a)funin 6642
[Enderton] p. 53Exercise 22(a)imass2 6120
[Enderton] p. 54Remarkixpf 8960  ixpssmap 8972
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8938
[Enderton] p. 55Axiom of Choice (second form)ac9 10523  ac9s 10533
[Enderton] p. 56Theorem 3Meqvrelref 38611  erref 8765
[Enderton] p. 57Lemma 3Neqvrelthi 38614  erthi 8798
[Enderton] p. 57Definitiondf-ec 8747
[Enderton] p. 58Definitiondf-qs 8751
[Enderton] p. 61Exercise 35df-ec 8747
[Enderton] p. 65Exercise 56(a)dmun 5921
[Enderton] p. 68Definition of successordf-suc 6390
[Enderton] p. 71Definitiondf-tr 5260  dftr4 5266
[Enderton] p. 72Theorem 4Eunisuc 6463  unisucg 6462
[Enderton] p. 73Exercise 6unisuc 6463  unisucg 6462
[Enderton] p. 73Exercise 5(a)truni 5275
[Enderton] p. 73Exercise 5(b)trint 5277  trintALT 44901
[Enderton] p. 79Theorem 4I(A1)nna0 8642
[Enderton] p. 79Theorem 4I(A2)nnasuc 8644  onasuc 8566
[Enderton] p. 79Definition of operation valuedf-ov 7434
[Enderton] p. 80Theorem 4J(A1)nnm0 8643
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8645  onmsuc 8567
[Enderton] p. 81Theorem 4K(1)nnaass 8660
[Enderton] p. 81Theorem 4K(2)nna0r 8647  nnacom 8655
[Enderton] p. 81Theorem 4K(3)nndi 8661
[Enderton] p. 81Theorem 4K(4)nnmass 8662
[Enderton] p. 81Theorem 4K(5)nnmcom 8664
[Enderton] p. 82Exercise 16nnm0r 8648  nnmsucr 8663
[Enderton] p. 88Exercise 23nnaordex 8676
[Enderton] p. 129Definitiondf-en 8986
[Enderton] p. 132Theorem 6B(b)canth 7385
[Enderton] p. 133Exercise 1xpomen 10055
[Enderton] p. 133Exercise 2qnnen 16249
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9247
[Enderton] p. 135Corollary 6Cphp3 9249
[Enderton] p. 136Corollary 6Enneneq 9246
[Enderton] p. 136Corollary 6D(a)pssinf 9292
[Enderton] p. 136Corollary 6D(b)ominf 9294
[Enderton] p. 137Lemma 6Fpssnn 9208
[Enderton] p. 138Corollary 6Gssfi 9213
[Enderton] p. 139Theorem 6H(c)mapen 9181
[Enderton] p. 142Theorem 6I(3)xpdjuen 10220
[Enderton] p. 142Theorem 6I(4)mapdjuen 10221
[Enderton] p. 143Theorem 6Jdju0en 10216  dju1en 10212
[Enderton] p. 144Exercise 13iunfi 9383  unifi 9384  unifi2 9385
[Enderton] p. 144Corollary 6Kundif2 4477  unfi 9211  unfi2 9348
[Enderton] p. 145Figure 38ffoss 7970
[Enderton] p. 145Definitiondf-dom 8987
[Enderton] p. 146Example 1domen 9002  domeng 9003
[Enderton] p. 146Example 3nndomo 9269  nnsdom 9694  nnsdomg 9335
[Enderton] p. 149Theorem 6L(a)djudom2 10224
[Enderton] p. 149Theorem 6L(c)mapdom1 9182  xpdom1 9111  xpdom1g 9109  xpdom2g 9108
[Enderton] p. 149Theorem 6L(d)mapdom2 9188
[Enderton] p. 151Theorem 6Mzorn 10547  zorng 10544
[Enderton] p. 151Theorem 6M(4)ac8 10532  dfac5 10169
[Enderton] p. 159Theorem 6Qunictb 10615
[Enderton] p. 164Exampleinfdif 10248
[Enderton] p. 168Definitiondf-po 5592
[Enderton] p. 192Theorem 7M(a)oneli 6498
[Enderton] p. 192Theorem 7M(b)ontr1 6430
[Enderton] p. 192Theorem 7M(c)onirri 6497
[Enderton] p. 193Corollary 7N(b)0elon 6438
[Enderton] p. 193Corollary 7N(c)onsuci 7859
[Enderton] p. 193Corollary 7N(d)ssonunii 7801
[Enderton] p. 194Remarkonprc 7798
[Enderton] p. 194Exercise 16suc11 6491
[Enderton] p. 197Definitiondf-card 9979
[Enderton] p. 197Theorem 7Pcarden 10591
[Enderton] p. 200Exercise 25tfis 7876
[Enderton] p. 202Lemma 7Tr1tr 9816
[Enderton] p. 202Definitiondf-r1 9804
[Enderton] p. 202Theorem 7Qr1val1 9826
[Enderton] p. 204Theorem 7V(b)rankval4 9907
[Enderton] p. 206Theorem 7X(b)en2lp 9646
[Enderton] p. 207Exercise 30rankpr 9897  rankprb 9891  rankpw 9883  rankpwi 9863  rankuniss 9906
[Enderton] p. 207Exercise 34opthreg 9658
[Enderton] p. 208Exercise 35suc11reg 9659
[Enderton] p. 212Definition of alephalephval3 10150
[Enderton] p. 213Theorem 8A(a)alephord2 10116
[Enderton] p. 213Theorem 8A(b)cardalephex 10130
[Enderton] p. 218Theorem Schema 8Eonfununi 8381
[Enderton] p. 222Definition of kardkarden 9935  kardex 9934
[Enderton] p. 238Theorem 8Roeoa 8635
[Enderton] p. 238Theorem 8Soeoe 8637
[Enderton] p. 240Exercise 25oarec 8600
[Enderton] p. 257Definition of cofinalitycflm 10290
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17685
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17631
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18598  mrieqv2d 17682  mrieqvd 17681
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17686
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17691  mreexexlem2d 17688
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18604  mreexfidimd 17693
[Frege1879] p. 11Statementdf3or2 43781
[Frege1879] p. 12Statementdf3an2 43782  dfxor4 43779  dfxor5 43780
[Frege1879] p. 26Axiom 1ax-frege1 43803
[Frege1879] p. 26Axiom 2ax-frege2 43804
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43808
[Frege1879] p. 31Proposition 4frege4 43812
[Frege1879] p. 32Proposition 5frege5 43813
[Frege1879] p. 33Proposition 6frege6 43819
[Frege1879] p. 34Proposition 7frege7 43821
[Frege1879] p. 35Axiom 8ax-frege8 43822  axfrege8 43820
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37446
[Frege1879] p. 35Proposition 9frege9 43825
[Frege1879] p. 36Proposition 10frege10 43833
[Frege1879] p. 36Proposition 11frege11 43827
[Frege1879] p. 37Proposition 12frege12 43826
[Frege1879] p. 37Proposition 13frege13 43835
[Frege1879] p. 37Proposition 14frege14 43836
[Frege1879] p. 38Proposition 15frege15 43839
[Frege1879] p. 38Proposition 16frege16 43829
[Frege1879] p. 39Proposition 17frege17 43834
[Frege1879] p. 39Proposition 18frege18 43831
[Frege1879] p. 39Proposition 19frege19 43837
[Frege1879] p. 40Proposition 20frege20 43841
[Frege1879] p. 40Proposition 21frege21 43840
[Frege1879] p. 41Proposition 22frege22 43832
[Frege1879] p. 42Proposition 23frege23 43838
[Frege1879] p. 42Proposition 24frege24 43828
[Frege1879] p. 42Proposition 25frege25 43830  rp-frege25 43818
[Frege1879] p. 42Proposition 26frege26 43823
[Frege1879] p. 43Axiom 28ax-frege28 43843
[Frege1879] p. 43Proposition 27frege27 43824
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43844
[Frege1879] p. 44Axiom 31ax-frege31 43847  axfrege31 43846
[Frege1879] p. 44Proposition 30frege30 43845
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43848
[Frege1879] p. 44Proposition 33frege33 43849
[Frege1879] p. 45Proposition 34frege34 43850
[Frege1879] p. 45Proposition 35frege35 43851
[Frege1879] p. 45Proposition 36frege36 43852
[Frege1879] p. 46Proposition 37frege37 43853
[Frege1879] p. 46Proposition 38frege38 43854
[Frege1879] p. 46Proposition 39frege39 43855
[Frege1879] p. 46Proposition 40frege40 43856
[Frege1879] p. 47Axiom 41ax-frege41 43858  axfrege41 43857
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43859
[Frege1879] p. 47Proposition 43frege43 43860
[Frege1879] p. 47Proposition 44frege44 43861
[Frege1879] p. 47Proposition 45frege45 43862
[Frege1879] p. 48Proposition 46frege46 43863
[Frege1879] p. 48Proposition 47frege47 43864
[Frege1879] p. 49Proposition 48frege48 43865
[Frege1879] p. 49Proposition 49frege49 43866
[Frege1879] p. 49Proposition 50frege50 43867
[Frege1879] p. 50Axiom 52ax-frege52a 43870  ax-frege52c 43901  frege52aid 43871  frege52b 43902
[Frege1879] p. 50Axiom 54ax-frege54a 43875  ax-frege54c 43905  frege54b 43906
[Frege1879] p. 50Proposition 51frege51 43868
[Frege1879] p. 50Proposition 52dfsbcq 3790
[Frege1879] p. 50Proposition 53frege53a 43873  frege53aid 43872  frege53b 43903  frege53c 43927
[Frege1879] p. 50Proposition 54biid 261  eqid 2737
[Frege1879] p. 50Proposition 55frege55a 43881  frege55aid 43878  frege55b 43910  frege55c 43931  frege55cor1a 43882  frege55lem2a 43880  frege55lem2b 43909  frege55lem2c 43930
[Frege1879] p. 50Proposition 56frege56a 43884  frege56aid 43883  frege56b 43911  frege56c 43932
[Frege1879] p. 51Axiom 58ax-frege58a 43888  ax-frege58b 43914  frege58bid 43915  frege58c 43934
[Frege1879] p. 51Proposition 57frege57a 43886  frege57aid 43885  frege57b 43912  frege57c 43933
[Frege1879] p. 51Proposition 58spsbc 3801
[Frege1879] p. 51Proposition 59frege59a 43890  frege59b 43917  frege59c 43935
[Frege1879] p. 52Proposition 60frege60a 43891  frege60b 43918  frege60c 43936
[Frege1879] p. 52Proposition 61frege61a 43892  frege61b 43919  frege61c 43937
[Frege1879] p. 52Proposition 62frege62a 43893  frege62b 43920  frege62c 43938
[Frege1879] p. 52Proposition 63frege63a 43894  frege63b 43921  frege63c 43939
[Frege1879] p. 53Proposition 64frege64a 43895  frege64b 43922  frege64c 43940
[Frege1879] p. 53Proposition 65frege65a 43896  frege65b 43923  frege65c 43941
[Frege1879] p. 54Proposition 66frege66a 43897  frege66b 43924  frege66c 43942
[Frege1879] p. 54Proposition 67frege67a 43898  frege67b 43925  frege67c 43943
[Frege1879] p. 54Proposition 68frege68a 43899  frege68b 43926  frege68c 43944
[Frege1879] p. 55Definition 69dffrege69 43945
[Frege1879] p. 58Proposition 70frege70 43946
[Frege1879] p. 59Proposition 71frege71 43947
[Frege1879] p. 59Proposition 72frege72 43948
[Frege1879] p. 59Proposition 73frege73 43949
[Frege1879] p. 60Definition 76dffrege76 43952
[Frege1879] p. 60Proposition 74frege74 43950
[Frege1879] p. 60Proposition 75frege75 43951
[Frege1879] p. 62Proposition 77frege77 43953  frege77d 43759
[Frege1879] p. 63Proposition 78frege78 43954
[Frege1879] p. 63Proposition 79frege79 43955
[Frege1879] p. 63Proposition 80frege80 43956
[Frege1879] p. 63Proposition 81frege81 43957  frege81d 43760
[Frege1879] p. 64Proposition 82frege82 43958
[Frege1879] p. 65Proposition 83frege83 43959  frege83d 43761
[Frege1879] p. 65Proposition 84frege84 43960
[Frege1879] p. 66Proposition 85frege85 43961
[Frege1879] p. 66Proposition 86frege86 43962
[Frege1879] p. 66Proposition 87frege87 43963  frege87d 43763
[Frege1879] p. 67Proposition 88frege88 43964
[Frege1879] p. 68Proposition 89frege89 43965
[Frege1879] p. 68Proposition 90frege90 43966
[Frege1879] p. 68Proposition 91frege91 43967  frege91d 43764
[Frege1879] p. 69Proposition 92frege92 43968
[Frege1879] p. 70Proposition 93frege93 43969
[Frege1879] p. 70Proposition 94frege94 43970
[Frege1879] p. 70Proposition 95frege95 43971
[Frege1879] p. 71Definition 99dffrege99 43975
[Frege1879] p. 71Proposition 96frege96 43972  frege96d 43762
[Frege1879] p. 71Proposition 97frege97 43973  frege97d 43765
[Frege1879] p. 71Proposition 98frege98 43974  frege98d 43766
[Frege1879] p. 72Proposition 100frege100 43976
[Frege1879] p. 72Proposition 101frege101 43977
[Frege1879] p. 72Proposition 102frege102 43978  frege102d 43767
[Frege1879] p. 73Proposition 103frege103 43979
[Frege1879] p. 73Proposition 104frege104 43980
[Frege1879] p. 73Proposition 105frege105 43981
[Frege1879] p. 73Proposition 106frege106 43982  frege106d 43768
[Frege1879] p. 74Proposition 107frege107 43983
[Frege1879] p. 74Proposition 108frege108 43984  frege108d 43769
[Frege1879] p. 74Proposition 109frege109 43985  frege109d 43770
[Frege1879] p. 75Proposition 110frege110 43986
[Frege1879] p. 75Proposition 111frege111 43987  frege111d 43772
[Frege1879] p. 76Proposition 112frege112 43988
[Frege1879] p. 76Proposition 113frege113 43989
[Frege1879] p. 76Proposition 114frege114 43990  frege114d 43771
[Frege1879] p. 77Definition 115dffrege115 43991
[Frege1879] p. 77Proposition 116frege116 43992
[Frege1879] p. 78Proposition 117frege117 43993
[Frege1879] p. 78Proposition 118frege118 43994
[Frege1879] p. 78Proposition 119frege119 43995
[Frege1879] p. 78Proposition 120frege120 43996
[Frege1879] p. 79Proposition 121frege121 43997
[Frege1879] p. 79Proposition 122frege122 43998  frege122d 43773
[Frege1879] p. 79Proposition 123frege123 43999
[Frege1879] p. 80Proposition 124frege124 44000  frege124d 43774
[Frege1879] p. 81Proposition 125frege125 44001
[Frege1879] p. 81Proposition 126frege126 44002  frege126d 43775
[Frege1879] p. 82Proposition 127frege127 44003
[Frege1879] p. 83Proposition 128frege128 44004
[Frege1879] p. 83Proposition 129frege129 44005  frege129d 43776
[Frege1879] p. 84Proposition 130frege130 44006
[Frege1879] p. 85Proposition 131frege131 44007  frege131d 43777
[Frege1879] p. 86Proposition 132frege132 44008
[Frege1879] p. 86Proposition 133frege133 44009  frege133d 43778
[Fremlin1] p. 13Definition 111G (b)df-salgen 46328
[Fremlin1] p. 13Definition 111G (d)borelmbl 46651
[Fremlin1] p. 13Proposition 111G (b)salgenss 46351
[Fremlin1] p. 14Definition 112Aismea 46466
[Fremlin1] p. 15Remark 112B (d)psmeasure 46486
[Fremlin1] p. 15Property 112C (a)meadjun 46477  meadjunre 46491
[Fremlin1] p. 15Property 112C (b)meassle 46478
[Fremlin1] p. 15Property 112C (c)meaunle 46479
[Fremlin1] p. 16Property 112C (d)iundjiun 46475  meaiunle 46484  meaiunlelem 46483
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46496  meaiuninc2 46497  meaiuninc3 46500  meaiuninc3v 46499  meaiunincf 46498  meaiuninclem 46495
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46502  meaiininc2 46503  meaiininclem 46501
[Fremlin1] p. 19Theorem 113Ccaragen0 46521  caragendifcl 46529  caratheodory 46543  omelesplit 46533
[Fremlin1] p. 19Definition 113Aisome 46509  isomennd 46546  isomenndlem 46545
[Fremlin1] p. 19Remark 113B (c)omeunle 46531
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46550  voncmpl 46636
[Fremlin1] p. 19Definition 113A (ii)omessle 46513
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46538  carageniuncllem1 46536  carageniuncllem2 46537  caragenuncl 46528  caragenuncllem 46527  caragenunicl 46539
[Fremlin1] p. 21Remark 113Dcaragenel2d 46547
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46541  caratheodorylem2 46542
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46550
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46609  hoidmv1lelem1 46606  hoidmv1lelem2 46607  hoidmv1lelem3 46608
[Fremlin1] p. 25Definition 114Eisvonmbl 46653
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46609  hoidmvle 46615  hoidmvlelem1 46610  hoidmvlelem2 46611  hoidmvlelem3 46612  hoidmvlelem4 46613  hoidmvlelem5 46614  hsphoidmvle2 46600  hsphoif 46591  hsphoival 46594
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46563
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46571
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46598  hoidmvn0val 46599  hoidmvval 46592  hoidmvval0 46602  hoidmvval0b 46605
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46603  hsphoidmvle 46601
[Fremlin1] p. 30Definition 115Cdf-ovoln 46552  df-voln 46554
[Fremlin1] p. 30Proposition 115D (a)dmovn 46619  ovn0 46581  ovn0lem 46580  ovnf 46578  ovnome 46588  ovnssle 46576  ovnsslelem 46575  ovnsupge0 46572
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46618  ovnhoilem1 46616  ovnhoilem2 46617  vonhoi 46682
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46635  hoidifhspf 46633  hoidifhspval 46623  hoidifhspval2 46630  hoidifhspval3 46634  hspmbl 46644  hspmbllem1 46641  hspmbllem2 46642  hspmbllem3 46643
[Fremlin1] p. 31Definition 115Evoncmpl 46636  vonmea 46589
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46587  ovnsubadd2 46661  ovnsubadd2lem 46660  ovnsubaddlem1 46585  ovnsubaddlem2 46586
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46646  hoimbl2 46680  hoimbllem 46645  hspdifhsp 46631  opnvonmbl 46649  opnvonmbllem2 46648
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46651
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46694  iccvonmbllem 46693  ioovonmbl 46692
[Fremlin1] p. 32Proposition 115G (d)vonicc 46700  vonicclem2 46699  vonioo 46697  vonioolem2 46696  vonn0icc 46703  vonn0icc2 46707  vonn0ioo 46702  vonn0ioo2 46705
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46704  snvonmbl 46701  vonct 46708  vonsn 46706
[Fremlin1] p. 35Lemma 121Asubsalsal 46374
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46373  subsaliuncllem 46372
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46740  salpreimalegt 46724  salpreimaltle 46741
[Fremlin1] p. 35Proposition 121B (i)issmf 46743  issmff 46749  issmflem 46742
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46760  issmflelem 46759  smfpreimale 46769
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46771  issmfgtlem 46770
[Fremlin1] p. 36Definition 121Cdf-smblfn 46711  issmf 46743  issmff 46749  issmfge 46785  issmfgelem 46784  issmfgt 46771  issmfgtlem 46770  issmfle 46760  issmflelem 46759  issmflem 46742
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46722  salpreimagtlt 46745  salpreimalelt 46744
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46785  issmfgelem 46784
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46768
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46766  cnfsmf 46755
[Fremlin1] p. 36Proposition 121D (c)decsmf 46782  decsmflem 46781  incsmf 46757  incsmflem 46756
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46716  pimconstlt1 46717  smfconst 46764
[Fremlin1] p. 37Proposition 121E (b)smfadd 46780  smfaddlem1 46778  smfaddlem2 46779
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46811
[Fremlin1] p. 37Proposition 121E (d)smfmul 46810  smfmullem1 46806  smfmullem2 46807  smfmullem3 46808  smfmullem4 46809
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46812
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46815  smfpimbor1lem2 46814
[Fremlin1] p. 37Proposition 121E (g)smfco 46817
[Fremlin1] p. 37Proposition 121E (h)smfres 46805
[Fremlin1] p. 38Proposition 121E (e)smfrec 46804
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46813  smfresal 46803
[Fremlin1] p. 38Proposition 121F (a)smflim 46792  smflim2 46821  smflimlem1 46786  smflimlem2 46787  smflimlem3 46788  smflimlem4 46789  smflimlem5 46790  smflimlem6 46791  smflimmpt 46825
[Fremlin1] p. 38Proposition 121F (b)smfsup 46829  smfsuplem1 46826  smfsuplem2 46827  smfsuplem3 46828  smfsupmpt 46830  smfsupxr 46831
[Fremlin1] p. 38Proposition 121F (c)smfinf 46833  smfinflem 46832  smfinfmpt 46834
[Fremlin1] p. 39Remark 121Gsmflim 46792  smflim2 46821  smflimmpt 46825
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46823
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46853  smfdivdmmbl2 46856  smfinfdmmbl 46864  smfinfdmmbllem 46863  smfsupdmmbl 46860  smfsupdmmbllem 46859
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46843  smflimsuplem2 46836  smflimsuplem6 46840  smflimsuplem7 46841  smflimsuplem8 46842  smflimsupmpt 46844
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46846  smfliminflem 46845  smfliminfmpt 46847
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46711
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46857  fsupdm2 46858
[Fremlin1], p. 39Proposition 121Hadddmmbl 46848  adddmmbl2 46849  finfdm 46861  finfdm2 46862  fsupdm 46857  fsupdm2 46858  muldmmbl 46850  muldmmbl2 46851
[Fremlin1], p. 39Proposition 121F (c)finfdm 46861  finfdm2 46862
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25571
[Fremlin5] p. 213Lemma 565Cauniioovol 25614
[Fremlin5] p. 214Lemma 565Cauniioombl 25624
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37705
[Fremlin5] p. 220Theorem 565Maftc1anc 37708
[FreydScedrov] p. 283Axiom of Infinityax-inf 9678  inf1 9662  inf2 9663
[Gleason] p. 117Proposition 9-2.1df-enq 10951  enqer 10961
[Gleason] p. 117Proposition 9-2.2df-1nq 10956  df-nq 10952
[Gleason] p. 117Proposition 9-2.3df-plpq 10948  df-plq 10954
[Gleason] p. 119Proposition 9-2.4caovmo 7670  df-mpq 10949  df-mq 10955
[Gleason] p. 119Proposition 9-2.5df-rq 10957
[Gleason] p. 119Proposition 9-2.6ltexnq 11015
[Gleason] p. 120Proposition 9-2.6(i)halfnq 11016  ltbtwnnq 11018
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 11011
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 11012
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 11019
[Gleason] p. 121Definition 9-3.1df-np 11021
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 11033
[Gleason] p. 121Definition 9-3.1(iii)prnmax 11035
[Gleason] p. 122Definitiondf-1p 11022
[Gleason] p. 122Remark (1)prub 11034
[Gleason] p. 122Lemma 9-3.4prlem934 11073
[Gleason] p. 122Proposition 9-3.2df-ltp 11025
[Gleason] p. 122Proposition 9-3.3ltsopr 11072  psslinpr 11071  supexpr 11094  suplem1pr 11092  suplem2pr 11093
[Gleason] p. 123Proposition 9-3.5addclpr 11058  addclprlem1 11056  addclprlem2 11057  df-plp 11023
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11062
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11061
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11074
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11083  ltexprlem1 11076  ltexprlem2 11077  ltexprlem3 11078  ltexprlem4 11079  ltexprlem5 11080  ltexprlem6 11081  ltexprlem7 11082
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11085  ltaprlem 11084
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11086
[Gleason] p. 124Lemma 9-3.6prlem936 11087
[Gleason] p. 124Proposition 9-3.7df-mp 11024  mulclpr 11060  mulclprlem 11059  reclem2pr 11088
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11069
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11064
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11063
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11068
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11091  reclem3pr 11089  reclem4pr 11090
[Gleason] p. 126Proposition 9-4.1df-enr 11095  enrer 11103
[Gleason] p. 126Proposition 9-4.2df-0r 11100  df-1r 11101  df-nr 11096
[Gleason] p. 126Proposition 9-4.3df-mr 11098  df-plr 11097  negexsr 11142  recexsr 11147  recexsrlem 11143
[Gleason] p. 127Proposition 9-4.4df-ltr 11099
[Gleason] p. 130Proposition 10-1.3creui 12261  creur 12260  cru 12258
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11228  axcnre 11204
[Gleason] p. 132Definition 10-3.1crim 15154  crimd 15271  crimi 15232  crre 15153  crred 15270  crrei 15231
[Gleason] p. 132Definition 10-3.2remim 15156  remimd 15237
[Gleason] p. 133Definition 10.36absval2 15323  absval2d 15484  absval2i 15436
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15180  cjaddd 15259  cjaddi 15227
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15181  cjmuld 15260  cjmuli 15228
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15179  cjcjd 15238  cjcji 15210
[Gleason] p. 133Proposition 10-3.4(f)cjre 15178  cjreb 15162  cjrebd 15241  cjrebi 15213  cjred 15265  rere 15161  rereb 15159  rerebd 15240  rerebi 15212  rered 15263
[Gleason] p. 133Proposition 10-3.4(h)addcj 15187  addcjd 15251  addcji 15222
[Gleason] p. 133Proposition 10-3.7(a)absval 15277
[Gleason] p. 133Proposition 10-3.7(b)abscj 15318  abscjd 15489  abscji 15440
[Gleason] p. 133Proposition 10-3.7(c)abs00 15328  abs00d 15485  abs00i 15437  absne0d 15486
[Gleason] p. 133Proposition 10-3.7(d)releabs 15360  releabsd 15490  releabsi 15441
[Gleason] p. 133Proposition 10-3.7(f)absmul 15333  absmuld 15493  absmuli 15443
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15321  sqabsaddi 15444
[Gleason] p. 133Proposition 10-3.7(h)abstri 15369  abstrid 15495  abstrii 15447
[Gleason] p. 134Definition 10-4.1df-exp 14103  exp0 14106  expp1 14109  expp1d 14187
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26721  cxpaddd 26759  expadd 14145  expaddd 14188  expaddz 14147
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26730  cxpmuld 26779  expmul 14148  expmuld 14189  expmulz 14149
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26727  mulcxpd 26770  mulexp 14142  mulexpd 14201  mulexpz 14143
[Gleason] p. 140Exercise 1znnen 16248
[Gleason] p. 141Definition 11-2.1fzval 13549
[Gleason] p. 168Proposition 12-2.1(a)climadd 15668  rlimadd 15679  rlimdiv 15682
[Gleason] p. 168Proposition 12-2.1(b)climsub 15670  rlimsub 15680
[Gleason] p. 168Proposition 12-2.1(c)climmul 15669  rlimmul 15681
[Gleason] p. 171Corollary 12-2.2climmulc2 15673
[Gleason] p. 172Corollary 12-2.5climrecl 15619
[Gleason] p. 172Proposition 12-2.4(c)climabs 15640  climcj 15641  climim 15643  climre 15642  rlimabs 15645  rlimcj 15646  rlimim 15648  rlimre 15647
[Gleason] p. 173Definition 12-3.1df-ltxr 11300  df-xr 11299  ltxr 13157
[Gleason] p. 175Definition 12-4.1df-limsup 15507  limsupval 15510
[Gleason] p. 180Theorem 12-5.1climsup 15706
[Gleason] p. 180Theorem 12-5.3caucvg 15715  caucvgb 15716  caucvgbf 45500  caucvgr 15712  climcau 15707
[Gleason] p. 182Exercise 3cvgcmp 15852
[Gleason] p. 182Exercise 4cvgrat 15919
[Gleason] p. 195Theorem 13-2.12abs1m 15374
[Gleason] p. 217Lemma 13-4.1btwnzge0 13868
[Gleason] p. 223Definition 14-1.1df-met 21358
[Gleason] p. 223Definition 14-1.1(a)met0 24353  xmet0 24352
[Gleason] p. 223Definition 14-1.1(b)metgt0 24369
[Gleason] p. 223Definition 14-1.1(c)metsym 24360
[Gleason] p. 223Definition 14-1.1(d)mettri 24362  mstri 24479  xmettri 24361  xmstri 24478
[Gleason] p. 225Definition 14-1.5xpsmet 24392
[Gleason] p. 230Proposition 14-2.6txlm 23656
[Gleason] p. 240Theorem 14-4.3metcnp4 25344
[Gleason] p. 240Proposition 14-4.2metcnp3 24553
[Gleason] p. 243Proposition 14-4.16addcn 24887  addcn2 15630  mulcn 24889  mulcn2 15632  subcn 24888  subcn2 15631
[Gleason] p. 295Remarkbcval3 14345  bcval4 14346
[Gleason] p. 295Equation 2bcpasc 14360
[Gleason] p. 295Definition of binomial coefficientbcval 14343  df-bc 14342
[Gleason] p. 296Remarkbcn0 14349  bcnn 14351
[Gleason] p. 296Theorem 15-2.8binom 15866
[Gleason] p. 308Equation 2ef0 16127
[Gleason] p. 308Equation 3efcj 16128
[Gleason] p. 309Corollary 15-4.3efne0 16133
[Gleason] p. 309Corollary 15-4.4efexp 16137
[Gleason] p. 310Equation 14sinadd 16200
[Gleason] p. 310Equation 15cosadd 16201
[Gleason] p. 311Equation 17sincossq 16212
[Gleason] p. 311Equation 18cosbnd 16217  sinbnd 16216
[Gleason] p. 311Lemma 15-4.7sqeqor 14255  sqeqori 14253
[Gleason] p. 311Definition of ` `df-pi 16108
[Godowski] p. 730Equation SFgoeqi 32292
[GodowskiGreechie] p. 249Equation IV3oai 31687
[Golan] p. 1Remarksrgisid 20206
[Golan] p. 1Definitiondf-srg 20184
[Golan] p. 149Definitiondf-slmd 33207
[Gonshor] p. 7Definitiondf-scut 27828
[Gonshor] p. 9Theorem 2.5slerec 27864
[Gonshor] p. 10Theorem 2.6cofcut1 27954  cofcut1d 27955
[Gonshor] p. 10Theorem 2.7cofcut2 27956  cofcut2d 27957
[Gonshor] p. 12Theorem 2.9cofcutr 27958  cofcutr1d 27959  cofcutr2d 27960
[Gonshor] p. 13Definitiondf-adds 27993
[Gonshor] p. 14Theorem 3.1addsprop 28009
[Gonshor] p. 15Theorem 3.2addsunif 28035
[Gonshor] p. 17Theorem 3.4mulsprop 28156
[Gonshor] p. 18Theorem 3.5mulsunif 28176
[Gonshor] p. 28Lemma 4.2halfcut 28416
[Gonshor] p. 28Theorem 4.2pw2cut 28420
[Gonshor] p. 30Theorem 4.2addhalfcut 28419
[Gonshor] p. 95Theorem 6.1addsbday 28050
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36160
[Gratzer] p. 23Section 0.6df-mre 17629
[Gratzer] p. 27Section 0.6df-mri 17631
[Hall] p. 1Section 1.1df-asslaw 48104  df-cllaw 48102  df-comlaw 48103
[Hall] p. 2Section 1.2df-clintop 48116
[Hall] p. 7Section 1.3df-sgrp2 48137
[Halmos] p. 28Partition ` `df-parts 38766  dfmembpart2 38771
[Halmos] p. 31Theorem 17.3riesz1 32084  riesz2 32085
[Halmos] p. 41Definition of Hermitianhmopadj2 31960
[Halmos] p. 42Definition of projector orderingpjordi 32192
[Halmos] p. 43Theorem 26.1elpjhmop 32204  elpjidm 32203  pjnmopi 32167
[Halmos] p. 44Remarkpjinormi 31706  pjinormii 31695
[Halmos] p. 44Theorem 26.2elpjch 32208  pjrn 31726  pjrni 31721  pjvec 31715
[Halmos] p. 44Theorem 26.3pjnorm2 31746
[Halmos] p. 44Theorem 26.4hmopidmpj 32173  hmopidmpji 32171
[Halmos] p. 45Theorem 27.1pjinvari 32210
[Halmos] p. 45Theorem 27.3pjoci 32199  pjocvec 31716
[Halmos] p. 45Theorem 27.4pjorthcoi 32188
[Halmos] p. 48Theorem 29.2pjssposi 32191
[Halmos] p. 48Theorem 29.3pjssdif1i 32194  pjssdif2i 32193
[Halmos] p. 50Definition of spectrumdf-spec 31874
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1795
[Hatcher] p. 25Definitiondf-phtpc 25024  df-phtpy 25003
[Hatcher] p. 26Definitiondf-pco 25038  df-pi1 25041
[Hatcher] p. 26Proposition 1.2phtpcer 25027
[Hatcher] p. 26Proposition 1.3pi1grp 25083
[Hefferon] p. 240Definition 3.12df-dmat 22496  df-dmatalt 48315
[Helfgott] p. 2Theoremtgoldbach 47804
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47789
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47801  bgoldbtbnd 47796  bgoldbtbnd 47796  tgblthelfgott 47802
[Helfgott] p. 5Proposition 1.1circlevma 34657
[Helfgott] p. 69Statement 7.49circlemethhgt 34658
[Helfgott] p. 69Statement 7.50hgt750lema 34672  hgt750lemb 34671  hgt750leme 34673  hgt750lemf 34668  hgt750lemg 34669
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47798  tgoldbachgt 34678  tgoldbachgtALTV 47799  tgoldbachgtd 34677
[Helfgott] p. 70Statement 7.49ax-hgt749 34659
[Herstein] p. 54Exercise 28df-grpo 30512
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18962  grpoideu 30528  mndideu 18758
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18992  grpoinveu 30538
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19023  grpo2inv 30550
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19036  grpoinvop 30552
[Herstein] p. 57Exercise 1dfgrp3e 19058
[Hitchcock] p. 5Rule A3mptnan 1768
[Hitchcock] p. 5Rule A4mptxor 1769
[Hitchcock] p. 5Rule A5mtpxor 1771
[Holland] p. 1519Theorem 2sumdmdi 32439
[Holland] p. 1520Lemma 5cdj1i 32452  cdj3i 32460  cdj3lem1 32453  cdjreui 32451
[Holland] p. 1524Lemma 7mddmdin0i 32450
[Holland95] p. 13Theorem 3.6hlathil 41967
[Holland95] p. 14Line 15hgmapvs 41893
[Holland95] p. 14Line 16hdmaplkr 41915
[Holland95] p. 14Line 17hdmapellkr 41916
[Holland95] p. 14Line 19hdmapglnm2 41913
[Holland95] p. 14Line 20hdmapip0com 41919
[Holland95] p. 14Theorem 3.6hdmapevec2 41838
[Holland95] p. 14Lines 24 and 25hdmapoc 41933
[Holland95] p. 204Definition of involutiondf-srng 20841
[Holland95] p. 212Definition of subspacedf-psubsp 39505
[Holland95] p. 214Lemma 3.3lclkrlem2v 41530
[Holland95] p. 214Definition 3.2df-lpolN 41483
[Holland95] p. 214Definition of nonsingularpnonsingN 39935
[Holland95] p. 215Lemma 3.3(1)dihoml4 41379  poml4N 39955
[Holland95] p. 215Lemma 3.3(2)dochexmid 41470  pexmidALTN 39980  pexmidN 39971
[Holland95] p. 218Theorem 3.6lclkr 41535
[Holland95] p. 218Definition of dual vector spacedf-ldual 39125  ldualset 39126
[Holland95] p. 222Item 1df-lines 39503  df-pointsN 39504
[Holland95] p. 222Item 2df-polarityN 39905
[Holland95] p. 223Remarkispsubcl2N 39949  omllaw4 39247  pol1N 39912  polcon3N 39919
[Holland95] p. 223Definitiondf-psubclN 39937
[Holland95] p. 223Equation for polaritypolval2N 39908
[Holmes] p. 40Definitiondf-xrn 38372
[Hughes] p. 44Equation 1.21bax-his3 31103
[Hughes] p. 47Definition of projection operatordfpjop 32201
[Hughes] p. 49Equation 1.30eighmre 31982  eigre 31854  eigrei 31853
[Hughes] p. 49Equation 1.31eighmorth 31983  eigorth 31857  eigorthi 31856
[Hughes] p. 137Remark (ii)eigposi 31855
[Huneke] p. 1Claim 1frgrncvvdeq 30328
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30324
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30325
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30326
[Huneke] p. 2Claim 2frgrregorufr 30344  frgrregorufr0 30343  frgrregorufrg 30345
[Huneke] p. 2Claim 3frgrhash2wsp 30351  frrusgrord 30360  frrusgrord0 30359
[Huneke] p. 2Statementdf-clwwlknon 30107
[Huneke] p. 2Statement 4frgrwopreglem4 30334
[Huneke] p. 2Statement 5frgrwopreg1 30337  frgrwopreg2 30338  frgrwopregasn 30335  frgrwopregbsn 30336
[Huneke] p. 2Statement 6frgrwopreglem5 30340
[Huneke] p. 2Statement 7fusgreghash2wspv 30354
[Huneke] p. 2Statement 8fusgreghash2wsp 30357
[Huneke] p. 2Statement 9clwlksndivn 30105  numclwlk1 30390  numclwlk1lem1 30388  numclwlk1lem2 30389  numclwwlk1 30380  numclwwlk8 30411
[Huneke] p. 2Definition 3frgrwopreglem1 30331
[Huneke] p. 2Definition 4df-clwlks 29791
[Huneke] p. 2Definition 62clwwlk 30366
[Huneke] p. 2Definition 7numclwwlkovh 30392  numclwwlkovh0 30391
[Huneke] p. 2Statement 10numclwwlk2 30400
[Huneke] p. 2Statement 11rusgrnumwlkg 29997
[Huneke] p. 2Statement 12numclwwlk3 30404
[Huneke] p. 2Statement 13numclwwlk5 30407
[Huneke] p. 2Statement 14numclwwlk7 30410
[Indrzejczak] p. 33Definition ` `Enatded 30422  natded 30422
[Indrzejczak] p. 33Definition ` `Inatded 30422
[Indrzejczak] p. 34Definition ` `Enatded 30422  natded 30422
[Indrzejczak] p. 34Definition ` `Inatded 30422
[Jech] p. 4Definition of classcv 1539  cvjust 2731
[Jech] p. 42Lemma 6.1alephexp1 10619
[Jech] p. 42Equation 6.1alephadd 10617  alephmul 10618
[Jech] p. 43Lemma 6.2infmap 10616  infmap2 10257
[Jech] p. 71Lemma 9.3jech9.3 9854
[Jech] p. 72Equation 9.3scott0 9926  scottex 9925
[Jech] p. 72Exercise 9.1rankval4 9907
[Jech] p. 72Scheme "Collection Principle"cp 9931
[Jech] p. 78Noteopthprc 5749
[JonesMatijasevic] p. 694Definition 2.3rmxyval 42927
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43015
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43016
[JonesMatijasevic] p. 695Equation 2.7rmxadd 42939
[JonesMatijasevic] p. 695Equation 2.8rmyadd 42943
[JonesMatijasevic] p. 695Equation 2.9rmxp1 42944  rmyp1 42945
[JonesMatijasevic] p. 695Equation 2.10rmxm1 42946  rmym1 42947
[JonesMatijasevic] p. 695Equation 2.11rmx0 42937  rmx1 42938  rmxluc 42948
[JonesMatijasevic] p. 695Equation 2.12rmy0 42941  rmy1 42942  rmyluc 42949
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 42951
[JonesMatijasevic] p. 695Equation 2.14rmydbl 42952
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42972  jm2.17b 42973  jm2.17c 42974
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43005
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43009
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43000
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42975  jm2.24nn 42971
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43014
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43020  rmygeid 42976
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43032
[Juillerat] p. 11Section *5etransc 46298  etransclem47 46296  etransclem48 46297
[Juillerat] p. 12Equation (7)etransclem44 46293
[Juillerat] p. 12Equation *(7)etransclem46 46295
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46281
[Juillerat] p. 13Proofetransclem35 46284
[Juillerat] p. 13Part of case 2 proven inetransclem38 46287
[Juillerat] p. 13Part of case 2 provenetransclem24 46273
[Juillerat] p. 13Part of case 2: proven inetransclem41 46290
[Juillerat] p. 14Proofetransclem23 46272
[KalishMontague] p. 81Note 1ax-6 1967
[KalishMontague] p. 85Lemma 2equid 2011
[KalishMontague] p. 85Lemma 3equcomi 2016
[KalishMontague] p. 86Lemma 7cbvalivw 2006  cbvaliw 2005  wl-cbvmotv 37514  wl-motae 37516  wl-moteq 37515
[KalishMontague] p. 87Lemma 8spimvw 1995  spimw 1970
[KalishMontague] p. 87Lemma 9spfw 2032  spw 2033
[Kalmbach] p. 14Definition of latticechabs1 31535  chabs1i 31537  chabs2 31536  chabs2i 31538  chjass 31552  chjassi 31505  latabs1 18520  latabs2 18521
[Kalmbach] p. 15Definition of atomdf-at 32357  ela 32358
[Kalmbach] p. 15Definition of coverscvbr2 32302  cvrval2 39275
[Kalmbach] p. 16Definitiondf-ol 39179  df-oml 39180
[Kalmbach] p. 20Definition of commutescmbr 31603  cmbri 31609  cmtvalN 39212  df-cm 31602  df-cmtN 39178
[Kalmbach] p. 22Remarkomllaw5N 39248  pjoml5 31632  pjoml5i 31607
[Kalmbach] p. 22Definitionpjoml2 31630  pjoml2i 31604
[Kalmbach] p. 22Theorem 2(v)cmcm 31633  cmcmi 31611  cmcmii 31616  cmtcomN 39250
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39246  omlsi 31423  pjoml 31455  pjomli 31454
[Kalmbach] p. 22Definition of OML lawomllaw2N 39245
[Kalmbach] p. 23Remarkcmbr2i 31615  cmcm3 31634  cmcm3i 31613  cmcm3ii 31618  cmcm4i 31614  cmt3N 39252  cmt4N 39253  cmtbr2N 39254
[Kalmbach] p. 23Lemma 3cmbr3 31627  cmbr3i 31619  cmtbr3N 39255
[Kalmbach] p. 25Theorem 5fh1 31637  fh1i 31640  fh2 31638  fh2i 31641  omlfh1N 39259
[Kalmbach] p. 65Remarkchjatom 32376  chslej 31517  chsleji 31477  shslej 31399  shsleji 31389
[Kalmbach] p. 65Proposition 1chocin 31514  chocini 31473  chsupcl 31359  chsupval2 31429  h0elch 31274  helch 31262  hsupval2 31428  ocin 31315  ococss 31312  shococss 31313
[Kalmbach] p. 65Definition of subspace sumshsval 31331
[Kalmbach] p. 66Remarkdf-pjh 31414  pjssmi 32184  pjssmii 31700
[Kalmbach] p. 67Lemma 3osum 31664  osumi 31661
[Kalmbach] p. 67Lemma 4pjci 32219
[Kalmbach] p. 103Exercise 6atmd2 32419
[Kalmbach] p. 103Exercise 12mdsl0 32329
[Kalmbach] p. 140Remarkhatomic 32379  hatomici 32378  hatomistici 32381
[Kalmbach] p. 140Proposition 1atlatmstc 39320
[Kalmbach] p. 140Proposition 1(i)atexch 32400  lsatexch 39044
[Kalmbach] p. 140Proposition 1(ii)chcv1 32374  cvlcvr1 39340  cvr1 39412
[Kalmbach] p. 140Proposition 1(iii)cvexch 32393  cvexchi 32388  cvrexch 39422
[Kalmbach] p. 149Remark 2chrelati 32383  hlrelat 39404  hlrelat5N 39403  lrelat 39015
[Kalmbach] p. 153Exercise 5lsmcv 21143  lsmsatcv 39011  spansncv 31672  spansncvi 31671
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39030  spansncv2 32312
[Kalmbach] p. 266Definitiondf-st 32230
[Kalmbach2] p. 8Definition of adjointdf-adjh 31868
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10686  fpwwe2 10683
[KanamoriPincus] p. 416Corollary 1.3canth4 10687
[KanamoriPincus] p. 417Corollary 1.6canthp1 10694
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10689
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10691
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10704
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10708  gchxpidm 10709
[KanamoriPincus] p. 419Theorem 2.1gchacg 10720  gchhar 10719
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10255  unxpwdom 9629
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10710
[Kreyszig] p. 3Property M1metcl 24342  xmetcl 24341
[Kreyszig] p. 4Property M2meteq0 24349
[Kreyszig] p. 8Definition 1.1-8dscmet 24585
[Kreyszig] p. 12Equation 5conjmul 11984  muleqadd 11907
[Kreyszig] p. 18Definition 1.3-2mopnval 24448
[Kreyszig] p. 19Remarkmopntopon 24449
[Kreyszig] p. 19Theorem T1mopn0 24511  mopnm 24454
[Kreyszig] p. 19Theorem T2unimopn 24509
[Kreyszig] p. 19Definition of neighborhoodneibl 24514
[Kreyszig] p. 20Definition 1.3-3metcnp2 24555
[Kreyszig] p. 25Definition 1.4-1lmbr 23266  lmmbr 25292  lmmbr2 25293
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23388
[Kreyszig] p. 28Theorem 1.4-5lmcau 25347
[Kreyszig] p. 28Definition 1.4-3iscau 25310  iscmet2 25328
[Kreyszig] p. 30Theorem 1.4-7cmetss 25350
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23469  metelcls 25339
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25340  metcld2 25341
[Kreyszig] p. 51Equation 2clmvneg1 25132  lmodvneg1 20903  nvinv 30658  vcm 30595
[Kreyszig] p. 51Equation 1aclm0vs 25128  lmod0vs 20893  slmd0vs 33230  vc0 30593
[Kreyszig] p. 51Equation 1blmodvs0 20894  slmdvs0 33231  vcz 30594
[Kreyszig] p. 58Definition 2.2-1imsmet 30710  ngpmet 24616  nrmmetd 24587
[Kreyszig] p. 59Equation 1imsdval 30705  imsdval2 30706  ncvspds 25195  ngpds 24617
[Kreyszig] p. 63Problem 1nmval 24602  nvnd 30707
[Kreyszig] p. 64Problem 2nmeq0 24631  nmge0 24630  nvge0 30692  nvz 30688
[Kreyszig] p. 64Problem 3nmrtri 24637  nvabs 30691
[Kreyszig] p. 91Definition 2.7-1isblo3i 30820
[Kreyszig] p. 92Equation 2df-nmoo 30764
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30826  blocni 30824
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30825
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25238  ipeq0 21656  ipz 30738
[Kreyszig] p. 135Problem 2cphpyth 25250  pythi 30869
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30873
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25272
[Kreyszig] p. 144Equation 4supcvg 15892
[Kreyszig] p. 144Theorem 3.3-1minvec 25470  minveco 30903
[Kreyszig] p. 196Definition 3.9-1df-aj 30769
[Kreyszig] p. 247Theorem 4.7-2bcth 25363
[Kreyszig] p. 249Theorem 4.7-3ubth 30892
[Kreyszig] p. 470Definition of positive operator orderingleop 32142  leopg 32141
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32160
[Kreyszig] p. 525Theorem 10.1-1htth 30937
[Kulpa] p. 547Theorempoimir 37660
[Kulpa] p. 547Equation (1)poimirlem32 37659
[Kulpa] p. 547Equation (2)poimirlem31 37658
[Kulpa] p. 548Theorembroucube 37661
[Kulpa] p. 548Equation (6)poimirlem26 37653
[Kulpa] p. 548Equation (7)poimirlem27 37654
[Kunen] p. 10Axiom 0ax6e 2388  axnul 5305
[Kunen] p. 11Axiom 3axnul 5305
[Kunen] p. 12Axiom 6zfrep6 7979
[Kunen] p. 24Definition 10.24mapval 8878  mapvalg 8876
[Kunen] p. 30Lemma 10.20fodomg 10562
[Kunen] p. 31Definition 10.24mapex 7963
[Kunen] p. 95Definition 2.1df-r1 9804
[Kunen] p. 97Lemma 2.10r1elss 9846  r1elssi 9845
[Kunen] p. 107Exercise 4rankop 9898  rankopb 9892  rankuni 9903  rankxplim 9919  rankxpsuc 9922
[Kunen2] p. 47Lemma I.9.9relpfr 44975
[Kunen2] p. 53Lemma I.9.21trfr 44979
[Kunen2] p. 53Lemma I.9.24(2)wffr 44978
[Kunen2] p. 53Definition I.9.20tcfr 44980
[Kunen2] p. 95Lemma I.16.2ralabso 44985  rexabso 44986
[Kunen2] p. 96Example I.16.3disjabso 44992  n0abso 44993  ssabso 44991
[Kunen2] p. 111Lemma II.2.4(1)traxext 44994
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45004
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 44999
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45002
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45003
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 44998
[Kunen2] p. 112Corollary II.2.5wfaxext 45010  wfaxpr 45015  wfaxreg 45017  wfaxrep 45011  wfaxsep 45012  wfaxun 45016
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45001
[Kunen2] p. 113Corollary II.2.9wfaxpow 45014
[Kunen2] p. 114Theorem II.2.13wfaxext 45010
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45009  omelaxinf2 45006
[Kunen2] p. 114Corollary II.2.12wfac8prim 45019  wfaxinf2 45018
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 5004
[Lang] , p. 225Corollary 1.3finexttrb 33715
[Lang] p. Definitiondf-rn 5696
[Lang] p. 3Statementlidrideqd 18682  mndbn0 18763
[Lang] p. 3Definitiondf-mnd 18748
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18700
[Lang] p. 4Property of composites. Second formulagsumccat 18854
[Lang] p. 5Equationgsumreidx 19935
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48098
[Lang] p. 6Examplenn0mnd 48095
[Lang] p. 6Equationgsumxp2 19998
[Lang] p. 6Statementcycsubm 19220
[Lang] p. 6Definitionmulgnn0gsum 19098
[Lang] p. 6Observationmndlsmidm 19688
[Lang] p. 7Definitiondfgrp2e 18981
[Lang] p. 30Definitiondf-tocyc 33127
[Lang] p. 32Property (a)cyc3genpm 33172
[Lang] p. 32Property (b)cyc3conja 33177  cycpmconjv 33162
[Lang] p. 53Definitiondf-cat 17711
[Lang] p. 53Axiom CAT 1cat1 18142  cat1lem 18141
[Lang] p. 54Definitiondf-iso 17793
[Lang] p. 57Definitiondf-inito 18029  df-termo 18030
[Lang] p. 58Exampleirinitoringc 21490
[Lang] p. 58Statementinitoeu1 18056  termoeu1 18063
[Lang] p. 62Definitiondf-func 17903
[Lang] p. 65Definitiondf-nat 17991
[Lang] p. 91Notedf-ringc 20646
[Lang] p. 92Statementmxidlprm 33498
[Lang] p. 92Definitionisprmidlc 33475
[Lang] p. 128Remarkdsmmlmod 21765
[Lang] p. 129Prooflincscm 48347  lincscmcl 48349  lincsum 48346  lincsumcl 48348
[Lang] p. 129Statementlincolss 48351
[Lang] p. 129Observationdsmmfi 21758
[Lang] p. 141Theorem 5.3dimkerim 33678  qusdimsum 33679
[Lang] p. 141Corollary 5.4lssdimle 33658
[Lang] p. 147Definitionsnlindsntor 48388
[Lang] p. 504Statementmat1 22453  matring 22449
[Lang] p. 504Definitiondf-mamu 22395
[Lang] p. 505Statementmamuass 22406  mamutpos 22464  matassa 22450  mattposvs 22461  tposmap 22463
[Lang] p. 513Definitionmdet1 22607  mdetf 22601
[Lang] p. 513Theorem 4.4cramer 22697
[Lang] p. 514Proposition 4.6mdetleib 22593
[Lang] p. 514Proposition 4.8mdettpos 22617
[Lang] p. 515Definitiondf-minmar1 22641  smadiadetr 22681
[Lang] p. 515Corollary 4.9mdetero 22616  mdetralt 22614
[Lang] p. 517Proposition 4.15mdetmul 22629
[Lang] p. 518Definitiondf-madu 22640
[Lang] p. 518Proposition 4.16madulid 22651  madurid 22650  matinv 22683
[Lang] p. 561Theorem 3.1cayleyhamilton 22896
[Lang], p. 224Proposition 1.2extdgmul 33714  fedgmul 33682
[Lang], p. 561Remarkchpmatply1 22838
[Lang], p. 561Definitiondf-chpmat 22833
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44353
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44348
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44354
[LeBlanc] p. 277Rule R2axnul 5305
[Levy] p. 12Axiom 4.3.1df-clab 2715
[Levy] p. 59Definitiondf-ttrcl 9748
[Levy] p. 64Theorem 5.6(ii)frinsg 9791
[Levy] p. 338Axiomdf-clel 2816  df-cleq 2729
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2816  df-cleq 2729
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2715
[Levy] p. 358Axiomdf-clab 2715
[Levy58] p. 2Definition Iisfin1-3 10426
[Levy58] p. 2Definition IIdf-fin2 10326
[Levy58] p. 2Definition Iadf-fin1a 10325
[Levy58] p. 2Definition IIIdf-fin3 10328
[Levy58] p. 3Definition Vdf-fin5 10329
[Levy58] p. 3Definition IVdf-fin4 10327
[Levy58] p. 4Definition VIdf-fin6 10330
[Levy58] p. 4Definition VIIdf-fin7 10331
[Levy58], p. 3Theorem 1fin1a2 10455
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27731
[Lipparini] p. 3Lemma 2.1.4noresle 27742
[Lipparini] p. 6Proposition 4.2noinfbnd1 27774  nosupbnd1 27759
[Lipparini] p. 6Proposition 4.3noinfbnd2 27776  nosupbnd2 27761
[Lipparini] p. 7Theorem 5.1noetasuplem3 27780  noetasuplem4 27781
[Lipparini] p. 7Corollary 4.4nosupinfsep 27777
[Lopez-Astorga] p. 12Rule 1mptnan 1768
[Lopez-Astorga] p. 12Rule 2mptxor 1769
[Lopez-Astorga] p. 12Rule 3mtpxor 1771
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32427
[Maeda] p. 168Lemma 5mdsym 32431  mdsymi 32430
[Maeda] p. 168Lemma 4(i)mdsymlem4 32425  mdsymlem6 32427  mdsymlem7 32428
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32429
[MaedaMaeda] p. 1Remarkssdmd1 32332  ssdmd2 32333  ssmd1 32330  ssmd2 32331
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32328
[MaedaMaeda] p. 1Definition 1.1df-dmd 32300  df-md 32299  mdbr 32313
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32350  mdslj1i 32338  mdslj2i 32339  mdslle1i 32336  mdslle2i 32337  mdslmd1i 32348  mdslmd2i 32349
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32340  mdsl2bi 32342  mdsl2i 32341
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32354
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32351
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32352
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32329
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32334  mdsl3 32335
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32353
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32448
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39322  hlrelat1 39402
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39040
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32355  cvmdi 32343  cvnbtwn4 32308  cvrnbtwn4 39280
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32356
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39341  cvp 32394  cvrp 39418  lcvp 39041
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32418
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32417
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39334  hlexch4N 39394
[MaedaMaeda] p. 34Exercise 7.1atabsi 32420
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39445
[MaedaMaeda] p. 61Definition 15.10psubN 39751  atpsubN 39755  df-pointsN 39504  pointpsubN 39753
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39506  pmap11 39764  pmaple 39763  pmapsub 39770  pmapval 39759
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39767  pmap1N 39769
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39772  pmapglb2N 39773  pmapglb2xN 39774  pmapglbx 39771
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39854
[MaedaMaeda] p. 67Postulate PS1ps-1 39479
[MaedaMaeda] p. 68Lemma 16.2df-padd 39798  paddclN 39844  paddidm 39843
[MaedaMaeda] p. 68Condition PS2ps-2 39480
[MaedaMaeda] p. 68Equation 16.2.1paddass 39840
[MaedaMaeda] p. 69Lemma 16.4ps-1 39479
[MaedaMaeda] p. 69Theorem 16.4ps-2 39480
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19693  lsmmod2 19694  lssats 39013  shatomici 32377  shatomistici 32380  shmodi 31409  shmodsi 31408
[MaedaMaeda] p. 130Remark 29.6dmdmd 32319  mdsymlem7 32428
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31608
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31512
[MaedaMaeda] p. 139Remarksumdmdii 32434
[Margaris] p. 40Rule Cexlimiv 1930
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 396  df-ex 1780  df-or 849  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30419
[Margaris] p. 59Section 14notnotrALTVD 44935
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 44936
[Margaris] p. 79Rule Cexinst01 44645  exinst11 44646
[Margaris] p. 89Theorem 19.219.2 1976  19.2g 2188  r19.2z 4495
[Margaris] p. 89Theorem 19.319.3 2202  rr19.3v 3667
[Margaris] p. 89Theorem 19.5alcom 2159
[Margaris] p. 89Theorem 19.6alex 1826
[Margaris] p. 89Theorem 19.7alnex 1781
[Margaris] p. 89Theorem 19.819.8a 2181
[Margaris] p. 89Theorem 19.919.9 2205  19.9h 2286  exlimd 2218  exlimdh 2290
[Margaris] p. 89Theorem 19.11excom 2162  excomim 2163
[Margaris] p. 89Theorem 19.1219.12 2327
[Margaris] p. 90Section 19conventions-labels 30420  conventions-labels 30420  conventions-labels 30420  conventions-labels 30420
[Margaris] p. 90Theorem 19.14exnal 1827
[Margaris] p. 90Theorem 19.152albi 44397  albi 1818
[Margaris] p. 90Theorem 19.1619.16 2225
[Margaris] p. 90Theorem 19.1719.17 2226
[Margaris] p. 90Theorem 19.182exbi 44399  exbi 1847
[Margaris] p. 90Theorem 19.1919.19 2229
[Margaris] p. 90Theorem 19.202alim 44396  2alimdv 1918  alimd 2212  alimdh 1817  alimdv 1916  ax-4 1809  ralimdaa 3260  ralimdv 3169  ralimdva 3167  ralimdvva 3206  sbcimdv 3859
[Margaris] p. 90Theorem 19.2119.21 2207  19.21h 2287  19.21t 2206  19.21vv 44395  alrimd 2215  alrimdd 2214  alrimdh 1863  alrimdv 1929  alrimi 2213  alrimih 1824  alrimiv 1927  alrimivv 1928  hbralrimi 3144  r19.21be 3252  r19.21bi 3251  ralrimd 3264  ralrimdv 3152  ralrimdva 3154  ralrimdvv 3203  ralrimdvva 3211  ralrimi 3257  ralrimia 3258  ralrimiv 3145  ralrimiva 3146  ralrimivv 3200  ralrimivva 3202  ralrimivvva 3205  ralrimivw 3150
[Margaris] p. 90Theorem 19.222exim 44398  2eximdv 1919  exim 1834  eximd 2216  eximdh 1864  eximdv 1917  rexim 3087  reximd2a 3269  reximdai 3261  reximdd 45153  reximddv 3171  reximddv2 3215  reximddv3 3172  reximdv 3170  reximdv2 3164  reximdva 3168  reximdvai 3165  reximdvva 3207  reximi2 3079
[Margaris] p. 90Theorem 19.2319.23 2211  19.23bi 2191  19.23h 2288  19.23t 2210  exlimdv 1933  exlimdvv 1934  exlimexi 44544  exlimiv 1930  exlimivv 1932  rexlimd3 45149  rexlimdv 3153  rexlimdv3a 3159  rexlimdva 3155  rexlimdva2 3157  rexlimdvaa 3156  rexlimdvv 3212  rexlimdvva 3213  rexlimdvvva 3214  rexlimdvw 3160  rexlimiv 3148  rexlimiva 3147  rexlimivv 3201
[Margaris] p. 90Theorem 19.2419.24 1985
[Margaris] p. 90Theorem 19.2519.25 1880
[Margaris] p. 90Theorem 19.2619.26 1870
[Margaris] p. 90Theorem 19.2719.27 2227  r19.27z 4505  r19.27zv 4506
[Margaris] p. 90Theorem 19.2819.28 2228  19.28vv 44405  r19.28z 4498  r19.28zf 45164  r19.28zv 4501  rr19.28v 3668
[Margaris] p. 90Theorem 19.2919.29 1873  r19.29d2r 3140  r19.29imd 3118
[Margaris] p. 90Theorem 19.3019.30 1881
[Margaris] p. 90Theorem 19.3119.31 2234  19.31vv 44403
[Margaris] p. 90Theorem 19.3219.32 2233  r19.32 47110
[Margaris] p. 90Theorem 19.3319.33-2 44401  19.33 1884
[Margaris] p. 90Theorem 19.3419.34 1986
[Margaris] p. 90Theorem 19.3519.35 1877
[Margaris] p. 90Theorem 19.3619.36 2230  19.36vv 44402  r19.36zv 4507
[Margaris] p. 90Theorem 19.3719.37 2232  19.37vv 44404  r19.37zv 4502
[Margaris] p. 90Theorem 19.3819.38 1839
[Margaris] p. 90Theorem 19.3919.39 1984
[Margaris] p. 90Theorem 19.4019.40-2 1887  19.40 1886  r19.40 3119
[Margaris] p. 90Theorem 19.4119.41 2235  19.41rg 44570
[Margaris] p. 90Theorem 19.4219.42 2236
[Margaris] p. 90Theorem 19.4319.43 1882
[Margaris] p. 90Theorem 19.4419.44 2237  r19.44zv 4504
[Margaris] p. 90Theorem 19.4519.45 2238  r19.45zv 4503
[Margaris] p. 110Exercise 2(b)eu1 2610
[Mayet] p. 370Remarkjpi 32289  largei 32286  stri 32276
[Mayet3] p. 9Definition of CH-statesdf-hst 32231  ishst 32233
[Mayet3] p. 10Theoremhstrbi 32285  hstri 32284
[Mayet3] p. 1223Theorem 4.1mayete3i 31747
[Mayet3] p. 1240Theorem 7.1mayetes3i 31748
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32297
[MegPav2000] p. 2345Definition 3.4-1chintcl 31351  chsupcl 31359
[MegPav2000] p. 2345Definition 3.4-2hatomic 32379
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32373
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32400
[MegPav2000] p. 2366Figure 7pl42N 39985
[MegPav2002] p. 362Lemma 2.2latj31 18532  latj32 18530  latjass 18528
[Megill] p. 444Axiom C5ax-5 1910  ax5ALT 38908
[Megill] p. 444Section 7conventions 30419
[Megill] p. 445Lemma L12aecom-o 38902  ax-c11n 38889  axc11n 2431
[Megill] p. 446Lemma L17equtrr 2021
[Megill] p. 446Lemma L18ax6fromc10 38897
[Megill] p. 446Lemma L19hbnae-o 38929  hbnae 2437
[Megill] p. 447Remark 9.1dfsb1 2486  sbid 2255  sbidd-misc 49238  sbidd 49237
[Megill] p. 448Remark 9.6axc14 2468
[Megill] p. 448Scheme C4'ax-c4 38885
[Megill] p. 448Scheme C5'ax-c5 38884  sp 2183
[Megill] p. 448Scheme C6'ax-11 2157
[Megill] p. 448Scheme C7'ax-c7 38886
[Megill] p. 448Scheme C8'ax-7 2007
[Megill] p. 448Scheme C9'ax-c9 38891
[Megill] p. 448Scheme C10'ax-6 1967  ax-c10 38887
[Megill] p. 448Scheme C11'ax-c11 38888
[Megill] p. 448Scheme C12'ax-8 2110
[Megill] p. 448Scheme C13'ax-9 2118
[Megill] p. 448Scheme C14'ax-c14 38892
[Megill] p. 448Scheme C15'ax-c15 38890
[Megill] p. 448Scheme C16'ax-c16 38893
[Megill] p. 448Theorem 9.4dral1-o 38905  dral1 2444  dral2-o 38931  dral2 2443  drex1 2446  drex2 2447  drsb1 2500  drsb2 2266
[Megill] p. 449Theorem 9.7sbcom2 2173  sbequ 2083  sbid2v 2514
[Megill] p. 450Example in Appendixhba1-o 38898  hba1 2293
[Mendelson] p. 35Axiom A3hirstL-ax3 46904
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3879  rspsbca 3880  stdpc4 2068
[Mendelson] p. 69Axiom 5ax-c4 38885  ra4 3886  stdpc5 2208
[Mendelson] p. 81Rule Cexlimiv 1930
[Mendelson] p. 95Axiom 6stdpc6 2027
[Mendelson] p. 95Axiom 7stdpc7 2250
[Mendelson] p. 225Axiom system NBGru 3786
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5519
[Mendelson] p. 231Exercise 4.10(k)inv1 4398
[Mendelson] p. 231Exercise 4.10(l)unv 4399
[Mendelson] p. 231Exercise 4.10(n)dfin3 4277
[Mendelson] p. 231Exercise 4.10(o)df-nul 4334
[Mendelson] p. 231Exercise 4.10(q)dfin4 4278
[Mendelson] p. 231Exercise 4.10(s)ddif 4141
[Mendelson] p. 231Definition of uniondfun3 4276
[Mendelson] p. 235Exercise 4.12(c)univ 5456
[Mendelson] p. 235Exercise 4.12(d)pwv 4904
[Mendelson] p. 235Exercise 4.12(j)pwin 5574
[Mendelson] p. 235Exercise 4.12(k)pwunss 4618
[Mendelson] p. 235Exercise 4.12(l)pwssun 5575
[Mendelson] p. 235Exercise 4.12(n)uniin 4931
[Mendelson] p. 235Exercise 4.12(p)reli 5836
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6288
[Mendelson] p. 244Proposition 4.8(g)epweon 7795
[Mendelson] p. 246Definition of successordf-suc 6390
[Mendelson] p. 250Exercise 4.36oelim2 8633
[Mendelson] p. 254Proposition 4.22(b)xpen 9180
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9095  xpsneng 9096
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9103  xpcomeng 9104
[Mendelson] p. 254Proposition 4.22(e)xpassen 9106
[Mendelson] p. 255Definitionbrsdom 9015
[Mendelson] p. 255Exercise 4.39endisj 9098
[Mendelson] p. 255Exercise 4.41mapprc 8870
[Mendelson] p. 255Exercise 4.43mapsnen 9077  mapsnend 9076
[Mendelson] p. 255Exercise 4.45mapunen 9186
[Mendelson] p. 255Exercise 4.47xpmapen 9185
[Mendelson] p. 255Exercise 4.42(a)map0e 8922
[Mendelson] p. 255Exercise 4.42(b)map1 9080
[Mendelson] p. 257Proposition 4.24(a)undom 9099
[Mendelson] p. 258Exercise 4.56(c)djuassen 10219  djucomen 10218
[Mendelson] p. 258Exercise 4.56(f)djudom1 10223
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10217
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8569
[Mendelson] p. 266Proposition 4.34(f)oaordex 8596
[Mendelson] p. 275Proposition 4.42(d)entri3 10599
[Mendelson] p. 281Definitiondf-r1 9804
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9853
[Mendelson] p. 287Axiom system MKru 3786
[MertziosUnger] p. 152Definitiondf-frgr 30278
[MertziosUnger] p. 153Remark 1frgrconngr 30313
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30315  vdgn1frgrv3 30316
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30317
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30310
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30303  2pthfrgrrn 30301  2pthfrgrrn2 30302
[Mittelstaedt] p. 9Definitiondf-oc 31271
[Monk1] p. 22Remarkconventions 30419
[Monk1] p. 22Theorem 3.1conventions 30419
[Monk1] p. 26Theorem 2.8(vii)ssin 4239
[Monk1] p. 33Theorem 3.2(i)ssrel 5792  ssrelf 32627
[Monk1] p. 33Theorem 3.2(ii)eqrel 5794
[Monk1] p. 34Definition 3.3df-opab 5206
[Monk1] p. 36Theorem 3.7(i)coi1 6282  coi2 6283
[Monk1] p. 36Theorem 3.8(v)dm0 5931  rn0 5936
[Monk1] p. 36Theorem 3.7(ii)cnvi 6161
[Monk1] p. 37Theorem 3.13(i)relxp 5703
[Monk1] p. 37Theorem 3.13(x)dmxp 5939  rnxp 6190
[Monk1] p. 37Theorem 3.13(ii)0xp 5784  xp0 6178
[Monk1] p. 38Theorem 3.16(ii)ima0 6095
[Monk1] p. 38Theorem 3.16(viii)imai 6092
[Monk1] p. 39Theorem 3.17imaex 7936  imaexALTV 38331  imaexg 7935
[Monk1] p. 39Theorem 3.16(xi)imassrn 6089
[Monk1] p. 41Theorem 4.3(i)fnopfv 7095  funfvop 7070
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6963
[Monk1] p. 42Theorem 4.4(iii)fvelima 6974
[Monk1] p. 43Theorem 4.6funun 6612
[Monk1] p. 43Theorem 4.8(iv)dff13 7275  dff13f 7276
[Monk1] p. 46Theorem 4.15(v)funex 7239  funrnex 7978
[Monk1] p. 50Definition 5.4fniunfv 7267
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6247
[Monk1] p. 52Theorem 5.11(viii)ssint 4964
[Monk1] p. 52Definition 5.13 (i)1stval2 8031  df-1st 8014
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8032  df-2nd 8015
[Monk1] p. 112Theorem 15.17(v)ranksn 9894  ranksnb 9867
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9895
[Monk1] p. 112Theorem 15.17(iii)rankun 9896  rankunb 9890
[Monk1] p. 113Theorem 15.18r1val3 9878
[Monk1] p. 113Definition 15.19df-r1 9804  r1val2 9877
[Monk1] p. 117Lemmazorn2 10546  zorn2g 10543
[Monk1] p. 133Theorem 18.11cardom 10026
[Monk1] p. 133Theorem 18.12canth3 10601
[Monk1] p. 133Theorem 18.14carduni 10021
[Monk2] p. 105Axiom C4ax-4 1809
[Monk2] p. 105Axiom C7ax-7 2007
[Monk2] p. 105Axiom C8ax-12 2177  ax-c15 38890  ax12v2 2179
[Monk2] p. 108Lemma 5ax-c4 38885
[Monk2] p. 109Lemma 12ax-11 2157
[Monk2] p. 109Lemma 15equvini 2460  equvinv 2028  eqvinop 5492
[Monk2] p. 113Axiom C5-1ax-5 1910  ax5ALT 38908
[Monk2] p. 113Axiom C5-2ax-10 2141
[Monk2] p. 113Axiom C5-3ax-11 2157
[Monk2] p. 114Lemma 21sp 2183
[Monk2] p. 114Lemma 22axc4 2321  hba1-o 38898  hba1 2293
[Monk2] p. 114Lemma 23nfia1 2153
[Monk2] p. 114Lemma 24nfa2 2176  nfra2 3376  nfra2w 3299
[Moore] p. 53Part Idf-mre 17629
[Munkres] p. 77Example 2distop 23002  indistop 23009  indistopon 23008
[Munkres] p. 77Example 3fctop 23011  fctop2 23012
[Munkres] p. 77Example 4cctop 23013
[Munkres] p. 78Definition of basisdf-bases 22953  isbasis3g 22956
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17488  tgval2 22963
[Munkres] p. 79Remarktgcl 22976
[Munkres] p. 80Lemma 2.1tgval3 22970
[Munkres] p. 80Lemma 2.2tgss2 22994  tgss3 22993
[Munkres] p. 81Lemma 2.3basgen 22995  basgen2 22996
[Munkres] p. 83Exercise 3topdifinf 37350  topdifinfeq 37351  topdifinffin 37349  topdifinfindis 37347
[Munkres] p. 89Definition of subspace topologyresttop 23168
[Munkres] p. 93Theorem 6.1(1)0cld 23046  topcld 23043
[Munkres] p. 93Theorem 6.1(2)iincld 23047
[Munkres] p. 93Theorem 6.1(3)uncld 23049
[Munkres] p. 94Definition of closureclsval 23045
[Munkres] p. 94Definition of interiorntrval 23044
[Munkres] p. 95Theorem 6.5(a)clsndisj 23083  elcls 23081
[Munkres] p. 95Theorem 6.5(b)elcls3 23091
[Munkres] p. 97Theorem 6.6clslp 23156  neindisj 23125
[Munkres] p. 97Corollary 6.7cldlp 23158
[Munkres] p. 97Definition of limit pointislp2 23153  lpval 23147
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23323
[Munkres] p. 102Definition of continuous functiondf-cn 23235  iscn 23243  iscn2 23246
[Munkres] p. 107Theorem 7.2(g)cncnp 23288  cncnp2 23289  cncnpi 23286  df-cnp 23236  iscnp 23245  iscnp2 23247
[Munkres] p. 127Theorem 10.1metcn 24556
[Munkres] p. 128Theorem 10.3metcn4 25345
[Nathanson] p. 123Remarkreprgt 34636  reprinfz1 34637  reprlt 34634
[Nathanson] p. 123Definitiondf-repr 34624
[Nathanson] p. 123Chapter 5.1circlemethnat 34656
[Nathanson] p. 123Propositionbreprexp 34648  breprexpnat 34649  itgexpif 34621
[NielsenChuang] p. 195Equation 4.73unierri 32123
[OeSilva] p. 2042Section 2ax-bgbltosilva 47797
[Pfenning] p. 17Definition XMnatded 30422
[Pfenning] p. 17Definition NNCnatded 30422  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30422
[Pfenning] p. 18Rule"natded 30422
[Pfenning] p. 18Definition /\Inatded 30422
[Pfenning] p. 18Definition ` `Enatded 30422  natded 30422  natded 30422  natded 30422  natded 30422
[Pfenning] p. 18Definition ` `Inatded 30422  natded 30422  natded 30422  natded 30422  natded 30422
[Pfenning] p. 18Definition ` `ELnatded 30422
[Pfenning] p. 18Definition ` `ERnatded 30422
[Pfenning] p. 18Definition ` `Ea,unatded 30422
[Pfenning] p. 18Definition ` `IRnatded 30422
[Pfenning] p. 18Definition ` `Ianatded 30422
[Pfenning] p. 127Definition =Enatded 30422
[Pfenning] p. 127Definition =Inatded 30422
[Ponnusamy] p. 361Theorem 6.44cphip0l 25236  df-dip 30720  dip0l 30737  ip0l 21654
[Ponnusamy] p. 361Equation 6.45cphipval 25277  ipval 30722
[Ponnusamy] p. 362Equation I1dipcj 30733  ipcj 21652
[Ponnusamy] p. 362Equation I3cphdir 25239  dipdir 30861  ipdir 21657  ipdiri 30849
[Ponnusamy] p. 362Equation I4ipidsq 30729  nmsq 25228
[Ponnusamy] p. 362Equation 6.46ip0i 30844
[Ponnusamy] p. 362Equation 6.47ip1i 30846
[Ponnusamy] p. 362Equation 6.48ip2i 30847
[Ponnusamy] p. 363Equation I2cphass 25245  dipass 30864  ipass 21663  ipassi 30860
[Prugovecki] p. 186Definition of brabraval 31963  df-bra 31869
[Prugovecki] p. 376Equation 8.1df-kb 31870  kbval 31973
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32401
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39890
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32415  atcvat4i 32416  cvrat3 39444  cvrat4 39445  lsatcvat3 39053
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32301  cvrval 39270  df-cv 32298  df-lcv 39020  lspsncv0 21148
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39902
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39903
[Quine] p. 16Definition 2.1df-clab 2715  rabid 3458  rabidd 45160
[Quine] p. 17Definition 2.1''dfsb7 2279
[Quine] p. 18Definition 2.7df-cleq 2729
[Quine] p. 19Definition 2.9conventions 30419  df-v 3482
[Quine] p. 34Theorem 5.1eqabb 2881
[Quine] p. 35Theorem 5.2abid1 2878  abid2f 2936
[Quine] p. 40Theorem 6.1sb5 2276
[Quine] p. 40Theorem 6.2sb6 2085  sbalex 2242
[Quine] p. 41Theorem 6.3df-clel 2816
[Quine] p. 41Theorem 6.4eqid 2737  eqid1 30486
[Quine] p. 41Theorem 6.5eqcom 2744
[Quine] p. 42Theorem 6.6df-sbc 3789
[Quine] p. 42Theorem 6.7dfsbcq 3790  dfsbcq2 3791
[Quine] p. 43Theorem 6.8vex 3484
[Quine] p. 43Theorem 6.9isset 3494
[Quine] p. 44Theorem 7.3spcgf 3591  spcgv 3596  spcimgf 3550
[Quine] p. 44Theorem 6.11spsbc 3801  spsbcd 3802
[Quine] p. 44Theorem 6.12elex 3501
[Quine] p. 44Theorem 6.13elab 3679  elabg 3676  elabgf 3674
[Quine] p. 44Theorem 6.14noel 4338
[Quine] p. 48Theorem 7.2snprc 4717
[Quine] p. 48Definition 7.1df-pr 4629  df-sn 4627
[Quine] p. 49Theorem 7.4snss 4785  snssg 4783
[Quine] p. 49Theorem 7.5prss 4820  prssg 4819
[Quine] p. 49Theorem 7.6prid1 4762  prid1g 4760  prid2 4763  prid2g 4761  snid 4662  snidg 4660
[Quine] p. 51Theorem 7.12snex 5436
[Quine] p. 51Theorem 7.13prex 5437
[Quine] p. 53Theorem 8.2unisn 4926  unisnALT 44946  unisng 4925
[Quine] p. 53Theorem 8.3uniun 4930
[Quine] p. 54Theorem 8.6elssuni 4937
[Quine] p. 54Theorem 8.7uni0 4935
[Quine] p. 56Theorem 8.17uniabio 6528
[Quine] p. 56Definition 8.18dfaiota2 47098  dfiota2 6515
[Quine] p. 57Theorem 8.19aiotaval 47107  iotaval 6532
[Quine] p. 57Theorem 8.22iotanul 6539
[Quine] p. 58Theorem 8.23iotaex 6534
[Quine] p. 58Definition 9.1df-op 4633
[Quine] p. 61Theorem 9.5opabid 5530  opabidw 5529  opelopab 5547  opelopaba 5541  opelopabaf 5549  opelopabf 5550  opelopabg 5543  opelopabga 5538  opelopabgf 5545  oprabid 7463  oprabidw 7462
[Quine] p. 64Definition 9.11df-xp 5691
[Quine] p. 64Definition 9.12df-cnv 5693
[Quine] p. 64Definition 9.15df-id 5578
[Quine] p. 65Theorem 10.3fun0 6631
[Quine] p. 65Theorem 10.4funi 6598
[Quine] p. 65Theorem 10.5funsn 6619  funsng 6617
[Quine] p. 65Definition 10.1df-fun 6563
[Quine] p. 65Definition 10.2args 6110  dffv4 6903
[Quine] p. 68Definition 10.11conventions 30419  df-fv 6569  fv2 6901
[Quine] p. 124Theorem 17.3nn0opth2 14311  nn0opth2i 14310  nn0opthi 14309  omopthi 8699
[Quine] p. 177Definition 25.2df-rdg 8450
[Quine] p. 232Equation icarddom 10594
[Quine] p. 284Axiom 39(vi)funimaex 6655  funimaexg 6653
[Quine] p. 331Axiom system NFru 3786
[ReedSimon] p. 36Definition (iii)ax-his3 31103
[ReedSimon] p. 63Exercise 4(a)df-dip 30720  polid 31178  polid2i 31176  polidi 31177
[ReedSimon] p. 63Exercise 4(b)df-ph 30832
[ReedSimon] p. 195Remarklnophm 32038  lnophmi 32037
[Retherford] p. 49Exercise 1(i)leopadd 32151
[Retherford] p. 49Exercise 1(ii)leopmul 32153  leopmuli 32152
[Retherford] p. 49Exercise 1(iv)leoptr 32156
[Retherford] p. 49Definition VI.1df-leop 31871  leoppos 32145
[Retherford] p. 49Exercise 1(iii)leoptri 32155
[Retherford] p. 49Definition of operator orderingleop3 32144
[Roman] p. 4Definitiondf-dmat 22496  df-dmatalt 48315
[Roman] p. 18Part Preliminariesdf-rng 20150
[Roman] p. 19Part Preliminariesdf-ring 20232
[Roman] p. 46Theorem 1.6isldepslvec2 48402
[Roman] p. 112Noteisldepslvec2 48402  ldepsnlinc 48425  zlmodzxznm 48414
[Roman] p. 112Examplezlmodzxzequa 48413  zlmodzxzequap 48416  zlmodzxzldep 48421
[Roman] p. 170Theorem 7.8cayleyhamilton 22896
[Rosenlicht] p. 80Theoremheicant 37662
[Rosser] p. 281Definitiondf-op 4633
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34660
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34661
[Rotman] p. 28Remarkpgrpgt2nabl 48282  pmtr3ncom 19493
[Rotman] p. 31Theorem 3.4symggen2 19489
[Rotman] p. 42Theorem 3.15cayley 19432  cayleyth 19433
[Rudin] p. 164Equation 27efcan 16132
[Rudin] p. 164Equation 30efzval 16138
[Rudin] p. 167Equation 48absefi 16232
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1771
[Sanford] p. 39Rule 4mptxor 1769
[Sanford] p. 40Rule 1mptnan 1768
[Schechter] p. 51Definition of antisymmetryintasym 6135
[Schechter] p. 51Definition of irreflexivityintirr 6138
[Schechter] p. 51Definition of symmetrycnvsym 6132
[Schechter] p. 51Definition of transitivitycotr 6130
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17629
[Schechter] p. 79Definition of Moore closuredf-mrc 17630
[Schechter] p. 82Section 4.5df-mrc 17630
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17632
[Schechter] p. 139Definition AC3dfac9 10177
[Schechter] p. 141Definition (MC)dfac11 43074
[Schechter] p. 149Axiom DC1ax-dc 10486  axdc3 10494
[Schechter] p. 187Definition of "ring with unit"isring 20234  isrngo 37904
[Schechter] p. 276Remark 11.6.espan0 31561
[Schechter] p. 276Definition of spandf-span 31328  spanval 31352
[Schechter] p. 428Definition 15.35bastop1 23000
[Schloeder] p. 1Lemma 1.3onelon 6409  onelord 43263  ordelon 6408  ordelord 6406
[Schloeder] p. 1Lemma 1.7onepsuc 43264  sucidg 6465
[Schloeder] p. 1Remark 1.50elon 6438  onsuc 7831  ord0 6437  ordsuci 7828
[Schloeder] p. 1Theorem 1.9epsoon 43265
[Schloeder] p. 1Definition 1.1dftr5 5263
[Schloeder] p. 1Definition 1.2dford3 43040  elon2 6395
[Schloeder] p. 1Definition 1.4df-suc 6390
[Schloeder] p. 1Definition 1.6epel 5587  epelg 5585
[Schloeder] p. 1Theorem 1.9(i)elirr 9637  epirron 43266  ordirr 6402
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43268  oneptr 43267  ontr1 6430
[Schloeder] p. 1Theorem 1.9(iii)oneltri 43270  oneptri 43269  ordtri3or 6416
[Schloeder] p. 2Lemma 1.10ondif1 8539  ord0eln0 6439
[Schloeder] p. 2Lemma 1.13elsuci 6451  onsucss 43279  trsucss 6472
[Schloeder] p. 2Lemma 1.14ordsucss 7838
[Schloeder] p. 2Lemma 1.15onnbtwn 6478  ordnbtwn 6477
[Schloeder] p. 2Lemma 1.16orddif0suc 43281  ordnexbtwnsuc 43280
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10441  onsucf1lem 43282  onsucf1o 43285  onsucf1olem 43283  onsucrn 43284
[Schloeder] p. 2Lemma 1.18dflim7 43286
[Schloeder] p. 2Remark 1.12ordzsl 7866
[Schloeder] p. 2Theorem 1.10ondif1i 43275  ordne0gt0 43274
[Schloeder] p. 2Definition 1.11dflim6 43277  limnsuc 43278  onsucelab 43276
[Schloeder] p. 3Remark 1.21omex 9683
[Schloeder] p. 3Theorem 1.19tfinds 7881
[Schloeder] p. 3Theorem 1.22omelon 9686  ordom 7897
[Schloeder] p. 3Definition 1.20dfom3 9687
[Schloeder] p. 4Lemma 2.21onn 8678
[Schloeder] p. 4Lemma 2.7ssonuni 7800  ssorduni 7799
[Schloeder] p. 4Remark 2.4oa1suc 8569
[Schloeder] p. 4Theorem 1.23dfom5 9690  limom 7903
[Schloeder] p. 4Definition 2.1df-1o 8506  df1o2 8513
[Schloeder] p. 4Definition 2.3oa0 8554  oa0suclim 43288  oalim 8570  oasuc 8562
[Schloeder] p. 4Definition 2.5om0 8555  om0suclim 43289  omlim 8571  omsuc 8564
[Schloeder] p. 4Definition 2.6oe0 8560  oe0m1 8559  oe0suclim 43290  oelim 8572  oesuc 8565
[Schloeder] p. 5Lemma 2.10onsupuni 43241
[Schloeder] p. 5Lemma 2.11onsupsucismax 43292
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43293
[Schloeder] p. 5Lemma 2.13limexissup 43294  limexissupab 43296  limiun 43295  limuni 6445
[Schloeder] p. 5Lemma 2.14oa0r 8576
[Schloeder] p. 5Lemma 2.15om1 8580  om1om1r 43297  om1r 8581
[Schloeder] p. 5Remark 2.8oacl 8573  oaomoecl 43291  oecl 8575  omcl 8574
[Schloeder] p. 5Definition 2.9onsupintrab 43243
[Schloeder] p. 6Lemma 2.16oe1 8582
[Schloeder] p. 6Lemma 2.17oe1m 8583
[Schloeder] p. 6Lemma 2.18oe0rif 43298
[Schloeder] p. 6Theorem 2.19oasubex 43299
[Schloeder] p. 6Theorem 2.20nnacl 8649  nnamecl 43300  nnecl 8651  nnmcl 8650
[Schloeder] p. 7Lemma 3.1onsucwordi 43301
[Schloeder] p. 7Lemma 3.2oaword1 8590
[Schloeder] p. 7Lemma 3.3oaword2 8591
[Schloeder] p. 7Lemma 3.4oalimcl 8598
[Schloeder] p. 7Lemma 3.5oaltublim 43303
[Schloeder] p. 8Lemma 3.6oaordi3 43304
[Schloeder] p. 8Lemma 3.81oaomeqom 43306
[Schloeder] p. 8Lemma 3.10oa00 8597
[Schloeder] p. 8Lemma 3.11omge1 43310  omword1 8611
[Schloeder] p. 8Remark 3.9oaordnr 43309  oaordnrex 43308
[Schloeder] p. 8Theorem 3.7oaord3 43305
[Schloeder] p. 9Lemma 3.12omge2 43311  omword2 8612
[Schloeder] p. 9Lemma 3.13omlim2 43312
[Schloeder] p. 9Lemma 3.14omord2lim 43313
[Schloeder] p. 9Lemma 3.15omord2i 43314  omordi 8604
[Schloeder] p. 9Theorem 3.16omord 8606  omord2com 43315
[Schloeder] p. 10Lemma 3.172omomeqom 43316  df-2o 8507
[Schloeder] p. 10Lemma 3.19oege1 43319  oewordi 8629
[Schloeder] p. 10Lemma 3.20oege2 43320  oeworde 8631
[Schloeder] p. 10Lemma 3.21rp-oelim2 43321
[Schloeder] p. 10Lemma 3.22oeord2lim 43322
[Schloeder] p. 10Remark 3.18omnord1 43318  omnord1ex 43317
[Schloeder] p. 11Lemma 3.23oeord2i 43323
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43325
[Schloeder] p. 11Remark 3.26oenord1 43329  oenord1ex 43328
[Schloeder] p. 11Theorem 4.1oaomoencom 43330
[Schloeder] p. 11Theorem 4.2oaass 8599
[Schloeder] p. 11Theorem 3.24oeord2com 43324
[Schloeder] p. 12Theorem 4.3odi 8617
[Schloeder] p. 13Theorem 4.4omass 8618
[Schloeder] p. 14Remark 4.6oenass 43332
[Schloeder] p. 14Theorem 4.7oeoa 8635
[Schloeder] p. 15Lemma 5.1cantnftermord 43333
[Schloeder] p. 15Lemma 5.2cantnfub 43334  cantnfub2 43335
[Schloeder] p. 16Theorem 5.3cantnf2 43338
[Schwabhauser] p. 10Axiom A1axcgrrflx 28929  axtgcgrrflx 28470
[Schwabhauser] p. 10Axiom A2axcgrtr 28930
[Schwabhauser] p. 10Axiom A3axcgrid 28931  axtgcgrid 28471
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28456
[Schwabhauser] p. 11Axiom A4axsegcon 28942  axtgsegcon 28472  df-trkgcb 28458
[Schwabhauser] p. 11Axiom A5ax5seg 28953  axtg5seg 28473  df-trkgcb 28458
[Schwabhauser] p. 11Axiom A6axbtwnid 28954  axtgbtwnid 28474  df-trkgb 28457
[Schwabhauser] p. 12Axiom A7axpasch 28956  axtgpasch 28475  df-trkgb 28457
[Schwabhauser] p. 12Axiom A8axlowdim2 28975  df-trkg2d 34680
[Schwabhauser] p. 13Axiom A8axtglowdim2 28478
[Schwabhauser] p. 13Axiom A9axtgupdim2 28479  df-trkg2d 34680
[Schwabhauser] p. 13Axiom A10axeuclid 28978  axtgeucl 28480  df-trkge 28459
[Schwabhauser] p. 13Axiom A11axcont 28991  axtgcont 28477  axtgcont1 28476  df-trkgb 28457
[Schwabhauser] p. 27Theorem 2.1cgrrflx 35988
[Schwabhauser] p. 27Theorem 2.2cgrcomim 35990
[Schwabhauser] p. 27Theorem 2.3cgrtr 35993
[Schwabhauser] p. 27Theorem 2.4cgrcoml 35997
[Schwabhauser] p. 27Theorem 2.5cgrcomr 35998  tgcgrcomimp 28485  tgcgrcoml 28487  tgcgrcomr 28486
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36003  tgcgrtriv 28492
[Schwabhauser] p. 28Theorem 2.105segofs 36007  tg5segofs 34688
[Schwabhauser] p. 28Definition 2.10df-afs 34685  df-ofs 35984
[Schwabhauser] p. 29Theorem 2.11cgrextend 36009  tgcgrextend 28493
[Schwabhauser] p. 29Theorem 2.12segconeq 36011  tgsegconeq 28494
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36023  btwntriv2 36013  tgbtwntriv2 28495
[Schwabhauser] p. 30Theorem 3.2btwncomim 36014  tgbtwncom 28496
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36017  tgbtwntriv1 28499
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36018  tgbtwnswapid 28500
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36024  btwnintr 36020  tgbtwnexch2 28504  tgbtwnintr 28501
[Schwabhauser] p. 30Theorem 3.6btwnexch 36026  btwnexch3 36021  tgbtwnexch 28506  tgbtwnexch3 28502
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36025  tgbtwnouttr 28505  tgbtwnouttr2 28503
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28974
[Schwabhauser] p. 32Theorem 3.14btwndiff 36028  tgbtwndiff 28514
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28507  trisegint 36029
[Schwabhauser] p. 34Theorem 4.2ifscgr 36045  tgifscgr 28516
[Schwabhauser] p. 34Theorem 4.11colcom 28566  colrot1 28567  colrot2 28568  lncom 28630  lnrot1 28631  lnrot2 28632
[Schwabhauser] p. 34Definition 4.1df-ifs 36041
[Schwabhauser] p. 35Theorem 4.3cgrsub 36046  tgcgrsub 28517
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36056  tgcgrxfr 28526
[Schwabhauser] p. 35Statement 4.4ercgrg 28525
[Schwabhauser] p. 35Definition 4.4df-cgr3 36042  df-cgrg 28519
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28519
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36057  tgbtwnxfr 28538
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36063  colinearperm2 36065  colinearperm3 36064  colinearperm4 36066  colinearperm5 36067
[Schwabhauser] p. 36Definition 4.8df-ismt 28541
[Schwabhauser] p. 36Definition 4.10df-colinear 36040  tgellng 28561  tglng 28554
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36068
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36076  lnxfr 28574
[Schwabhauser] p. 37Theorem 4.14lineext 36077  lnext 28575
[Schwabhauser] p. 37Theorem 4.16fscgr 36081  tgfscgr 28576
[Schwabhauser] p. 37Theorem 4.17linecgr 36082  lncgr 28577
[Schwabhauser] p. 37Definition 4.15df-fs 36043
[Schwabhauser] p. 38Theorem 4.18lineid 36084  lnid 28578
[Schwabhauser] p. 38Theorem 4.19idinside 36085  tgidinside 28579
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36102  tgbtwnconn1 28583
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36103  tgbtwnconn2 28584
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36104  tgbtwnconn3 28585
[Schwabhauser] p. 41Theorem 5.5brsegle2 36110
[Schwabhauser] p. 41Definition 5.4df-segle 36108  legov 28593
[Schwabhauser] p. 41Definition 5.5legov2 28594
[Schwabhauser] p. 42Remark 5.13legso 28607
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36111
[Schwabhauser] p. 42Theorem 5.7seglerflx 36113
[Schwabhauser] p. 42Theorem 5.8segletr 36115
[Schwabhauser] p. 42Theorem 5.9segleantisym 36116
[Schwabhauser] p. 42Theorem 5.10seglelin 36117
[Schwabhauser] p. 42Theorem 5.11seglemin 36114
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36119
[Schwabhauser] p. 42Proposition 5.7legid 28595
[Schwabhauser] p. 42Proposition 5.8legtrd 28597
[Schwabhauser] p. 42Proposition 5.9legtri3 28598
[Schwabhauser] p. 42Proposition 5.10legtrid 28599
[Schwabhauser] p. 42Proposition 5.11leg0 28600
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36126
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36127
[Schwabhauser] p. 43Theorem 6.4broutsideof 36122  df-outsideof 36121
[Schwabhauser] p. 43Definition 6.1broutsideof2 36123  ishlg 28610
[Schwabhauser] p. 44Theorem 6.4hlln 28615
[Schwabhauser] p. 44Theorem 6.5hlid 28617  outsideofrflx 36128
[Schwabhauser] p. 44Theorem 6.6hlcomb 28611  hlcomd 28612  outsideofcom 36129
[Schwabhauser] p. 44Theorem 6.7hltr 28618  outsideoftr 36130
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28626  outsideofeu 36132
[Schwabhauser] p. 44Definition 6.8df-ray 36139
[Schwabhauser] p. 45Part 2df-lines2 36140
[Schwabhauser] p. 45Theorem 6.13outsidele 36133
[Schwabhauser] p. 45Theorem 6.15lineunray 36148
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36149  tglineelsb2 28640
[Schwabhauser] p. 45Theorem 6.17linecom 36151  linerflx1 36150  linerflx2 36152  tglinecom 28643  tglinerflx1 28641  tglinerflx2 28642
[Schwabhauser] p. 45Theorem 6.18linethru 36154  tglinethru 28644
[Schwabhauser] p. 45Definition 6.14df-line2 36138  tglng 28554
[Schwabhauser] p. 45Proposition 6.13legbtwn 28602
[Schwabhauser] p. 46Theorem 6.19linethrueu 36157  tglinethrueu 28647
[Schwabhauser] p. 46Theorem 6.21lineintmo 36158  tglineineq 28651  tglineinteq 28653  tglineintmo 28650
[Schwabhauser] p. 46Theorem 6.23colline 28657
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28658
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28659
[Schwabhauser] p. 49Theorem 7.3mirinv 28674
[Schwabhauser] p. 49Theorem 7.7mirmir 28670
[Schwabhauser] p. 49Theorem 7.8mirreu3 28662
[Schwabhauser] p. 49Definition 7.5df-mir 28661  ismir 28667  mirbtwn 28666  mircgr 28665  mirfv 28664  mirval 28663
[Schwabhauser] p. 50Theorem 7.8mirreu 28672
[Schwabhauser] p. 50Theorem 7.9mireq 28673
[Schwabhauser] p. 50Theorem 7.10mirinv 28674
[Schwabhauser] p. 50Theorem 7.11mirf1o 28677
[Schwabhauser] p. 50Theorem 7.13miriso 28678
[Schwabhauser] p. 51Theorem 7.14mirmot 28683
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28680  mirbtwni 28679
[Schwabhauser] p. 51Theorem 7.16mircgrs 28681
[Schwabhauser] p. 51Theorem 7.17miduniq 28693
[Schwabhauser] p. 52Lemma 7.21symquadlem 28697
[Schwabhauser] p. 52Theorem 7.18miduniq1 28694
[Schwabhauser] p. 52Theorem 7.19miduniq2 28695
[Schwabhauser] p. 52Theorem 7.20colmid 28696
[Schwabhauser] p. 53Lemma 7.22krippen 28699
[Schwabhauser] p. 55Lemma 7.25midexlem 28700
[Schwabhauser] p. 57Theorem 8.2ragcom 28706
[Schwabhauser] p. 57Definition 8.1df-rag 28702  israg 28705
[Schwabhauser] p. 58Theorem 8.3ragcol 28707
[Schwabhauser] p. 58Theorem 8.4ragmir 28708
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28710
[Schwabhauser] p. 58Theorem 8.6ragflat2 28711
[Schwabhauser] p. 58Theorem 8.7ragflat 28712
[Schwabhauser] p. 58Theorem 8.8ragtriva 28713
[Schwabhauser] p. 58Theorem 8.9ragflat3 28714  ragncol 28717
[Schwabhauser] p. 58Theorem 8.10ragcgr 28715
[Schwabhauser] p. 59Theorem 8.12perpcom 28721
[Schwabhauser] p. 59Theorem 8.13ragperp 28725
[Schwabhauser] p. 59Theorem 8.14perpneq 28722
[Schwabhauser] p. 59Definition 8.11df-perpg 28704  isperp 28720
[Schwabhauser] p. 59Definition 8.13isperp2 28723
[Schwabhauser] p. 60Theorem 8.18foot 28730
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28738  colperpexlem2 28739
[Schwabhauser] p. 63Theorem 8.21colperpex 28741  colperpexlem3 28740
[Schwabhauser] p. 64Theorem 8.22mideu 28746  midex 28745
[Schwabhauser] p. 66Lemma 8.24opphllem 28743
[Schwabhauser] p. 67Theorem 9.2oppcom 28752
[Schwabhauser] p. 67Definition 9.1islnopp 28747
[Schwabhauser] p. 68Lemma 9.3opphllem2 28756
[Schwabhauser] p. 68Lemma 9.4opphllem5 28759  opphllem6 28760
[Schwabhauser] p. 69Theorem 9.5opphl 28762
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28475
[Schwabhauser] p. 70Theorem 9.6outpasch 28763
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28771
[Schwabhauser] p. 71Definition 9.7df-hpg 28766  hpgbr 28768
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28773
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28772
[Schwabhauser] p. 72Theorem 9.11hpgid 28774
[Schwabhauser] p. 72Theorem 9.12hpgcom 28775
[Schwabhauser] p. 72Theorem 9.13hpgtr 28776
[Schwabhauser] p. 73Theorem 9.18colopp 28777
[Schwabhauser] p. 73Theorem 9.19colhp 28778
[Schwabhauser] p. 88Theorem 10.2lmieu 28792
[Schwabhauser] p. 88Definition 10.1df-mid 28782
[Schwabhauser] p. 89Theorem 10.4lmicom 28796
[Schwabhauser] p. 89Theorem 10.5lmilmi 28797
[Schwabhauser] p. 89Theorem 10.6lmireu 28798
[Schwabhauser] p. 89Theorem 10.7lmieq 28799
[Schwabhauser] p. 89Theorem 10.8lmiinv 28800
[Schwabhauser] p. 89Theorem 10.9lmif1o 28803
[Schwabhauser] p. 89Theorem 10.10lmiiso 28805
[Schwabhauser] p. 89Definition 10.3df-lmi 28783
[Schwabhauser] p. 90Theorem 10.11lmimot 28806
[Schwabhauser] p. 91Theorem 10.12hypcgr 28809
[Schwabhauser] p. 92Theorem 10.14lmiopp 28810
[Schwabhauser] p. 92Theorem 10.15lnperpex 28811
[Schwabhauser] p. 92Theorem 10.16trgcopy 28812  trgcopyeu 28814
[Schwabhauser] p. 95Definition 11.2dfcgra2 28838
[Schwabhauser] p. 95Definition 11.3iscgra 28817
[Schwabhauser] p. 95Proposition 11.4cgracgr 28826
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28824  cgrahl2 28825
[Schwabhauser] p. 96Theorem 11.6cgraid 28827
[Schwabhauser] p. 96Theorem 11.9cgraswap 28828
[Schwabhauser] p. 97Theorem 11.7cgracom 28830
[Schwabhauser] p. 97Theorem 11.8cgratr 28831
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28834  cgrahl 28835
[Schwabhauser] p. 98Theorem 11.13sacgr 28839
[Schwabhauser] p. 98Theorem 11.14oacgr 28840
[Schwabhauser] p. 98Theorem 11.15acopy 28841  acopyeu 28842
[Schwabhauser] p. 101Theorem 11.24inagswap 28849
[Schwabhauser] p. 101Theorem 11.25inaghl 28853
[Schwabhauser] p. 101Definition 11.23isinag 28846
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28861
[Schwabhauser] p. 102Definition 11.27df-leag 28854  isleag 28855
[Schwabhauser] p. 107Theorem 11.49tgsas 28863  tgsas1 28862  tgsas2 28864  tgsas3 28865
[Schwabhauser] p. 108Theorem 11.50tgasa 28867  tgasa1 28866
[Schwabhauser] p. 109Theorem 11.51tgsss1 28868  tgsss2 28869  tgsss3 28870
[Shapiro] p. 230Theorem 6.5.1dchrhash 27315  dchrsum 27313  dchrsum2 27312  sumdchr 27316
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27317  sum2dchr 27318
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20086  ablfacrp2 20087
[Shapiro], p. 328Equation 9.2.4vmasum 27260
[Shapiro], p. 329Equation 9.2.7logfac2 27261
[Shapiro], p. 329Equation 9.2.9logfacrlim 27268
[Shapiro], p. 331Equation 9.2.13vmadivsum 27526
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27529
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27583  vmalogdivsum2 27582
[Shapiro], p. 375Theorem 9.4.1dirith 27573  dirith2 27572
[Shapiro], p. 375Equation 9.4.3rplogsum 27571  rpvmasum 27570  rpvmasum2 27556
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27531
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27569
[Shapiro], p. 377Lemma 9.4.1dchrisum 27536  dchrisumlem1 27533  dchrisumlem2 27534  dchrisumlem3 27535  dchrisumlema 27532
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27539
[Shapiro], p. 379Equation 9.4.16dchrmusum 27568  dchrmusumlem 27566  dchrvmasumlem 27567
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27538
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27540
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27564  dchrisum0re 27557  dchrisumn0 27565
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27550
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27554
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27555
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27610  pntrsumbnd2 27611  pntrsumo1 27609
[Shapiro], p. 405Equation 10.2.1mudivsum 27574
[Shapiro], p. 406Equation 10.2.6mulogsum 27576
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27578
[Shapiro], p. 407Equation 10.2.8mulog2sum 27581
[Shapiro], p. 418Equation 10.4.6logsqvma 27586
[Shapiro], p. 418Equation 10.4.8logsqvma2 27587
[Shapiro], p. 419Equation 10.4.10selberg 27592
[Shapiro], p. 420Equation 10.4.12selberg2lem 27594
[Shapiro], p. 420Equation 10.4.14selberg2 27595
[Shapiro], p. 422Equation 10.6.7selberg3 27603
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27604
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27601  selberg3lem2 27602
[Shapiro], p. 422Equation 10.4.23selberg4 27605
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27599
[Shapiro], p. 428Equation 10.6.2selbergr 27612
[Shapiro], p. 429Equation 10.6.8selberg3r 27613
[Shapiro], p. 430Equation 10.6.11selberg4r 27614
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27628
[Shapiro], p. 434Equation 10.6.27pntlema 27640  pntlemb 27641  pntlemc 27639  pntlemd 27638  pntlemg 27642
[Shapiro], p. 435Equation 10.6.29pntlema 27640
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27632
[Shapiro], p. 436Lemma 10.6.2pntibnd 27637
[Shapiro], p. 436Equation 10.6.34pntlema 27640
[Shapiro], p. 436Equation 10.6.35pntlem3 27653  pntleml 27655
[Stoll] p. 13Definition corresponds to dfsymdif3 4306
[Stoll] p. 16Exercise 4.40dif 4405  dif0 4378
[Stoll] p. 16Exercise 4.8difdifdir 4492
[Stoll] p. 17Theorem 5.1(5)unvdif 4475
[Stoll] p. 19Theorem 5.2(13)undm 4297
[Stoll] p. 19Theorem 5.2(13')indm 4298
[Stoll] p. 20Remarkinvdif 4279
[Stoll] p. 25Definition of ordered tripledf-ot 4635
[Stoll] p. 43Definitionuniiun 5058
[Stoll] p. 44Definitionintiin 5059
[Stoll] p. 45Definitiondf-iin 4994
[Stoll] p. 45Definition indexed uniondf-iun 4993
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4306
[Strang] p. 242Section 6.3expgrowth 44354
[Suppes] p. 22Theorem 2eq0 4350  eq0f 4347
[Suppes] p. 22Theorem 4eqss 3999  eqssd 4001  eqssi 4000
[Suppes] p. 23Theorem 5ss0 4402  ss0b 4401
[Suppes] p. 23Theorem 6sstr 3992  sstrALT2 44855
[Suppes] p. 23Theorem 7pssirr 4103
[Suppes] p. 23Theorem 8pssn2lp 4104
[Suppes] p. 23Theorem 9psstr 4107
[Suppes] p. 23Theorem 10pssss 4098
[Suppes] p. 25Theorem 12elin 3967  elun 4153
[Suppes] p. 26Theorem 15inidm 4227
[Suppes] p. 26Theorem 16in0 4395
[Suppes] p. 27Theorem 23unidm 4157
[Suppes] p. 27Theorem 24un0 4394
[Suppes] p. 27Theorem 25ssun1 4178
[Suppes] p. 27Theorem 26ssequn1 4186
[Suppes] p. 27Theorem 27unss 4190
[Suppes] p. 27Theorem 28indir 4286
[Suppes] p. 27Theorem 29undir 4287
[Suppes] p. 28Theorem 32difid 4376
[Suppes] p. 29Theorem 33difin 4272
[Suppes] p. 29Theorem 34indif 4280
[Suppes] p. 29Theorem 35undif1 4476
[Suppes] p. 29Theorem 36difun2 4481
[Suppes] p. 29Theorem 37difin0 4474
[Suppes] p. 29Theorem 38disjdif 4472
[Suppes] p. 29Theorem 39difundi 4290
[Suppes] p. 29Theorem 40difindi 4292
[Suppes] p. 30Theorem 41nalset 5313
[Suppes] p. 39Theorem 61uniss 4915
[Suppes] p. 39Theorem 65uniop 5520
[Suppes] p. 41Theorem 70intsn 4984
[Suppes] p. 42Theorem 71intpr 4982  intprg 4981
[Suppes] p. 42Theorem 73op1stb 5476
[Suppes] p. 42Theorem 78intun 4980
[Suppes] p. 44Definition 15(a)dfiun2 5033  dfiun2g 5030
[Suppes] p. 44Definition 15(b)dfiin2 5034
[Suppes] p. 47Theorem 86elpw 4604  elpw2 5334  elpw2g 5333  elpwg 4603  elpwgdedVD 44937
[Suppes] p. 47Theorem 87pwid 4622
[Suppes] p. 47Theorem 89pw0 4812
[Suppes] p. 48Theorem 90pwpw0 4813
[Suppes] p. 52Theorem 101xpss12 5700
[Suppes] p. 52Theorem 102xpindi 5844  xpindir 5845
[Suppes] p. 52Theorem 103xpundi 5754  xpundir 5755
[Suppes] p. 54Theorem 105elirrv 9636
[Suppes] p. 58Theorem 2relss 5791
[Suppes] p. 59Theorem 4eldm 5911  eldm2 5912  eldm2g 5910  eldmg 5909
[Suppes] p. 59Definition 3df-dm 5695
[Suppes] p. 60Theorem 6dmin 5922
[Suppes] p. 60Theorem 8rnun 6165
[Suppes] p. 60Theorem 9rnin 6166
[Suppes] p. 60Definition 4dfrn2 5899
[Suppes] p. 61Theorem 11brcnv 5893  brcnvg 5890
[Suppes] p. 62Equation 5elcnv 5887  elcnv2 5888
[Suppes] p. 62Theorem 12relcnv 6122
[Suppes] p. 62Theorem 15cnvin 6164
[Suppes] p. 62Theorem 16cnvun 6162
[Suppes] p. 63Definitiondftrrels2 38576
[Suppes] p. 63Theorem 20co02 6280
[Suppes] p. 63Theorem 21dmcoss 5985
[Suppes] p. 63Definition 7df-co 5694
[Suppes] p. 64Theorem 26cnvco 5896
[Suppes] p. 64Theorem 27coass 6285
[Suppes] p. 65Theorem 31resundi 6011
[Suppes] p. 65Theorem 34elima 6083  elima2 6084  elima3 6085  elimag 6082
[Suppes] p. 65Theorem 35imaundi 6169
[Suppes] p. 66Theorem 40dminss 6173
[Suppes] p. 66Theorem 41imainss 6174
[Suppes] p. 67Exercise 11cnvxp 6177
[Suppes] p. 81Definition 34dfec2 8748
[Suppes] p. 82Theorem 72elec 8791  elecALTV 38267  elecg 8789
[Suppes] p. 82Theorem 73eqvrelth 38612  erth 8796  erth2 8797
[Suppes] p. 83Theorem 74eqvreldisj 38615  erdisj 8799
[Suppes] p. 83Definition 35, df-parts 38766  dfmembpart2 38771
[Suppes] p. 89Theorem 96map0b 8923
[Suppes] p. 89Theorem 97map0 8927  map0g 8924
[Suppes] p. 89Theorem 98mapsn 8928  mapsnd 8926
[Suppes] p. 89Theorem 99mapss 8929
[Suppes] p. 91Definition 12(ii)alephsuc 10108
[Suppes] p. 91Definition 12(iii)alephlim 10107
[Suppes] p. 92Theorem 1enref 9025  enrefg 9024
[Suppes] p. 92Theorem 2ensym 9043  ensymb 9042  ensymi 9044
[Suppes] p. 92Theorem 3entr 9046
[Suppes] p. 92Theorem 4unen 9086
[Suppes] p. 94Theorem 15endom 9019
[Suppes] p. 94Theorem 16ssdomg 9040
[Suppes] p. 94Theorem 17domtr 9047
[Suppes] p. 95Theorem 18sbth 9133
[Suppes] p. 97Theorem 23canth2 9170  canth2g 9171
[Suppes] p. 97Definition 3brsdom2 9137  df-sdom 8988  dfsdom2 9136
[Suppes] p. 97Theorem 21(i)sdomirr 9154
[Suppes] p. 97Theorem 22(i)domnsym 9139
[Suppes] p. 97Theorem 21(ii)sdomnsym 9138
[Suppes] p. 97Theorem 22(ii)domsdomtr 9152
[Suppes] p. 97Theorem 22(iv)brdom2 9022
[Suppes] p. 97Theorem 21(iii)sdomtr 9155
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9150
[Suppes] p. 98Exercise 4fundmen 9071  fundmeng 9072
[Suppes] p. 98Exercise 6xpdom3 9110
[Suppes] p. 98Exercise 11sdomentr 9151
[Suppes] p. 104Theorem 37fofi 9351
[Suppes] p. 104Theorem 38pwfi 9357
[Suppes] p. 105Theorem 40pwfi 9357
[Suppes] p. 111Axiom for cardinal numberscarden 10591
[Suppes] p. 130Definition 3df-tr 5260
[Suppes] p. 132Theorem 9ssonuni 7800
[Suppes] p. 134Definition 6df-suc 6390
[Suppes] p. 136Theorem Schema 22findes 7922  finds 7918  finds1 7921  finds2 7920
[Suppes] p. 151Theorem 42isfinite 9692  isfinite2 9334  isfiniteg 9337  unbnn 9332
[Suppes] p. 162Definition 5df-ltnq 10958  df-ltpq 10950
[Suppes] p. 197Theorem Schema 4tfindes 7884  tfinds 7881  tfinds2 7885
[Suppes] p. 209Theorem 18oaord1 8589
[Suppes] p. 209Theorem 21oaword2 8591
[Suppes] p. 211Theorem 25oaass 8599
[Suppes] p. 225Definition 8iscard2 10016
[Suppes] p. 227Theorem 56ondomon 10603
[Suppes] p. 228Theorem 59harcard 10018
[Suppes] p. 228Definition 12(i)aleph0 10106
[Suppes] p. 228Theorem Schema 61onintss 6435
[Suppes] p. 228Theorem Schema 62onminesb 7813  onminsb 7814
[Suppes] p. 229Theorem 64alephval2 10612
[Suppes] p. 229Theorem 65alephcard 10110
[Suppes] p. 229Theorem 66alephord2i 10117
[Suppes] p. 229Theorem 67alephnbtwn 10111
[Suppes] p. 229Definition 12df-aleph 9980
[Suppes] p. 242Theorem 6weth 10535
[Suppes] p. 242Theorem 8entric 10597
[Suppes] p. 242Theorem 9carden 10591
[Szendrei] p. 11Line 6df-cloneop 35696
[Szendrei] p. 11Paragraph 3df-suppos 35700
[TakeutiZaring] p. 8Axiom 1ax-ext 2708
[TakeutiZaring] p. 13Definition 4.5df-cleq 2729
[TakeutiZaring] p. 13Proposition 4.6df-clel 2816
[TakeutiZaring] p. 13Proposition 4.9cvjust 2731
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2760
[TakeutiZaring] p. 14Definition 4.16df-oprab 7435
[TakeutiZaring] p. 14Proposition 4.14ru 3786
[TakeutiZaring] p. 15Axiom 2zfpair 5421
[TakeutiZaring] p. 15Exercise 1elpr 4650  elpr2 4652  elpr2g 4651  elprg 4648
[TakeutiZaring] p. 15Exercise 2elsn 4641  elsn2 4665  elsn2g 4664  elsng 4640  velsn 4642
[TakeutiZaring] p. 15Exercise 3elop 5472
[TakeutiZaring] p. 15Exercise 4sneq 4636  sneqr 4840
[TakeutiZaring] p. 15Definition 5.1dfpr2 4646  dfsn2 4639  dfsn2ALT 4647
[TakeutiZaring] p. 16Axiom 3uniex 7761
[TakeutiZaring] p. 16Exercise 6opth 5481
[TakeutiZaring] p. 16Exercise 7opex 5469
[TakeutiZaring] p. 16Exercise 8rext 5453
[TakeutiZaring] p. 16Corollary 5.8unex 7764  unexg 7763
[TakeutiZaring] p. 16Definition 5.3dftp2 4691
[TakeutiZaring] p. 16Definition 5.5df-uni 4908
[TakeutiZaring] p. 16Definition 5.6df-in 3958  df-un 3956
[TakeutiZaring] p. 16Proposition 5.7unipr 4924  uniprg 4923
[TakeutiZaring] p. 17Axiom 4vpwex 5377
[TakeutiZaring] p. 17Exercise 1eltp 4689
[TakeutiZaring] p. 17Exercise 5elsuc 6454  elsucg 6452  sstr2 3990
[TakeutiZaring] p. 17Exercise 6uncom 4158
[TakeutiZaring] p. 17Exercise 7incom 4209
[TakeutiZaring] p. 17Exercise 8unass 4172
[TakeutiZaring] p. 17Exercise 9inass 4228
[TakeutiZaring] p. 17Exercise 10indi 4284
[TakeutiZaring] p. 17Exercise 11undi 4285
[TakeutiZaring] p. 17Definition 5.9df-pss 3971  df-ss 3968
[TakeutiZaring] p. 17Definition 5.10df-pw 4602
[TakeutiZaring] p. 18Exercise 7unss2 4187
[TakeutiZaring] p. 18Exercise 9dfss2 3969  sseqin2 4223
[TakeutiZaring] p. 18Exercise 10ssid 4006
[TakeutiZaring] p. 18Exercise 12inss1 4237  inss2 4238
[TakeutiZaring] p. 18Exercise 13nss 4048
[TakeutiZaring] p. 18Exercise 15unieq 4918
[TakeutiZaring] p. 18Exercise 18sspwb 5454  sspwimp 44938  sspwimpALT 44945  sspwimpALT2 44948  sspwimpcf 44940
[TakeutiZaring] p. 18Exercise 19pweqb 5461
[TakeutiZaring] p. 19Axiom 5ax-rep 5279
[TakeutiZaring] p. 20Definitiondf-rab 3437
[TakeutiZaring] p. 20Corollary 5.160ex 5307
[TakeutiZaring] p. 20Definition 5.12df-dif 3954
[TakeutiZaring] p. 20Definition 5.14dfnul2 4336
[TakeutiZaring] p. 20Proposition 5.15difid 4376
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4353  n0f 4349  neq0 4352  neq0f 4348
[TakeutiZaring] p. 21Axiom 6zfreg 9635
[TakeutiZaring] p. 21Axiom 6'zfregs 9772
[TakeutiZaring] p. 21Theorem 5.22setind 9774
[TakeutiZaring] p. 21Definition 5.20df-v 3482
[TakeutiZaring] p. 21Proposition 5.21vprc 5315
[TakeutiZaring] p. 22Exercise 10ss 4400
[TakeutiZaring] p. 22Exercise 3ssex 5321  ssexg 5323
[TakeutiZaring] p. 22Exercise 4inex1 5317
[TakeutiZaring] p. 22Exercise 5ruv 9642
[TakeutiZaring] p. 22Exercise 6elirr 9637
[TakeutiZaring] p. 22Exercise 7ssdif0 4366
[TakeutiZaring] p. 22Exercise 11difdif 4135
[TakeutiZaring] p. 22Exercise 13undif3 4300  undif3VD 44902
[TakeutiZaring] p. 22Exercise 14difss 4136
[TakeutiZaring] p. 22Exercise 15sscon 4143
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3062
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3071
[TakeutiZaring] p. 23Proposition 6.2xpex 7773  xpexg 7770
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5692
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6637
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6813  fun11 6640
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6577  svrelfun 6638
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5898
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5900
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5697
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5698
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5694
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6214  dfrel2 6209
[TakeutiZaring] p. 25Exercise 3xpss 5701
[TakeutiZaring] p. 25Exercise 5relun 5821
[TakeutiZaring] p. 25Exercise 6reluni 5828
[TakeutiZaring] p. 25Exercise 9inxp 5842
[TakeutiZaring] p. 25Exercise 12relres 6023
[TakeutiZaring] p. 25Exercise 13opelres 6003  opelresi 6005
[TakeutiZaring] p. 25Exercise 14dmres 6030
[TakeutiZaring] p. 25Exercise 15resss 6019
[TakeutiZaring] p. 25Exercise 17resabs1 6024
[TakeutiZaring] p. 25Exercise 18funres 6608
[TakeutiZaring] p. 25Exercise 24relco 6126
[TakeutiZaring] p. 25Exercise 29funco 6606
[TakeutiZaring] p. 25Exercise 30f1co 6815
[TakeutiZaring] p. 26Definition 6.10eu2 2609
[TakeutiZaring] p. 26Definition 6.11conventions 30419  df-fv 6569  fv3 6924
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7947  cnvexg 7946
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7931  dmexg 7923
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7932  rnexg 7924
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44473
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7942
[TakeutiZaring] p. 27Corollary 6.13fvex 6919
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47186  tz6.12-1-afv2 47253  tz6.12-1 6929  tz6.12-afv 47185  tz6.12-afv2 47252  tz6.12 6931  tz6.12c-afv2 47254  tz6.12c 6928
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47249  tz6.12-2 6894  tz6.12i-afv2 47255  tz6.12i 6934
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6564
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6565
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6567  wfo 6559
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6566  wf1 6558
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6568  wf1o 6560
[TakeutiZaring] p. 28Exercise 4eqfnfv 7051  eqfnfv2 7052  eqfnfv2f 7055
[TakeutiZaring] p. 28Exercise 5fvco 7007
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7237
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7235
[TakeutiZaring] p. 29Exercise 9funimaex 6655  funimaexg 6653
[TakeutiZaring] p. 29Definition 6.18df-br 5144
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5593
[TakeutiZaring] p. 30Definition 6.21dffr2 5646  dffr3 6117  eliniseg 6112  iniseg 6115
[TakeutiZaring] p. 30Definition 6.22df-eprel 5584
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5662  fr3nr 7792  frirr 5661
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5637
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7794
[TakeutiZaring] p. 31Exercise 1frss 5649
[TakeutiZaring] p. 31Exercise 4wess 5671
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6368  tz6.26i 6370  wefrc 5679  wereu2 5682
[TakeutiZaring] p. 32Theorem 6.27wfi 6371  wfii 6373
[TakeutiZaring] p. 32Definition 6.28df-isom 6570
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7349
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7350
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7356
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7357
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7358
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7362
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7369
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7371
[TakeutiZaring] p. 35Notationwtr 5259
[TakeutiZaring] p. 35Theorem 7.2trelpss 44474  tz7.2 5668
[TakeutiZaring] p. 35Definition 7.1dftr3 5265
[TakeutiZaring] p. 36Proposition 7.4ordwe 6397
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6405
[TakeutiZaring] p. 36Proposition 7.6ordelord 6406  ordelordALT 44557  ordelordALTVD 44887
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6412  ordelssne 6411
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6410
[TakeutiZaring] p. 37Proposition 7.9ordin 6414
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7802
[TakeutiZaring] p. 38Corollary 7.15ordsson 7803
[TakeutiZaring] p. 38Definition 7.11df-on 6388
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6416
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44569  ordon 7797
[TakeutiZaring] p. 38Proposition 7.13onprc 7798
[TakeutiZaring] p. 39Theorem 7.17tfi 7874
[TakeutiZaring] p. 40Exercise 3ontr2 6431
[TakeutiZaring] p. 40Exercise 7dftr2 5261
[TakeutiZaring] p. 40Exercise 9onssmin 7812
[TakeutiZaring] p. 40Exercise 11unon 7851
[TakeutiZaring] p. 40Exercise 12ordun 6488
[TakeutiZaring] p. 40Exercise 14ordequn 6487
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7799
[TakeutiZaring] p. 40Proposition 7.20elssuni 4937
[TakeutiZaring] p. 41Definition 7.22df-suc 6390
[TakeutiZaring] p. 41Proposition 7.23sssucid 6464  sucidg 6465
[TakeutiZaring] p. 41Proposition 7.24onsuc 7831
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6478  ordnbtwn 6477
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7848
[TakeutiZaring] p. 42Exercise 1df-lim 6389
[TakeutiZaring] p. 42Exercise 4omssnlim 7902
[TakeutiZaring] p. 42Exercise 7ssnlim 7907
[TakeutiZaring] p. 42Exercise 8onsucssi 7862  ordelsuc 7840
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7842
[TakeutiZaring] p. 42Definition 7.27nlimon 7872
[TakeutiZaring] p. 42Definition 7.28dfom2 7889
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7910
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7912
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7913
[TakeutiZaring] p. 43Remarkomon 7899
[TakeutiZaring] p. 43Axiom 7inf3 9675  omex 9683
[TakeutiZaring] p. 43Theorem 7.32ordom 7897
[TakeutiZaring] p. 43Corollary 7.31find 7917
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7914
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7915
[TakeutiZaring] p. 44Exercise 1limomss 7892
[TakeutiZaring] p. 44Exercise 2int0 4962
[TakeutiZaring] p. 44Exercise 3trintss 5278
[TakeutiZaring] p. 44Exercise 4intss1 4963
[TakeutiZaring] p. 44Exercise 5intex 5344
[TakeutiZaring] p. 44Exercise 6oninton 7815
[TakeutiZaring] p. 44Exercise 11ordintdif 6434
[TakeutiZaring] p. 44Definition 7.35df-int 4947
[TakeutiZaring] p. 44Proposition 7.34noinfep 9700
[TakeutiZaring] p. 45Exercise 4onint 7810
[TakeutiZaring] p. 47Lemma 1tfrlem1 8416
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8437
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8438
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8439
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8446  tz7.44-2 8447  tz7.44-3 8448
[TakeutiZaring] p. 50Exercise 1smogt 8407
[TakeutiZaring] p. 50Exercise 3smoiso 8402
[TakeutiZaring] p. 50Definition 7.46df-smo 8386
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8485  tz7.49c 8486
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8483
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8482
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8484
[TakeutiZaring] p. 53Proposition 7.532eu5 2656
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10051
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10052
[TakeutiZaring] p. 56Definition 8.1oalim 8570  oasuc 8562
[TakeutiZaring] p. 57Remarktfindsg 7882
[TakeutiZaring] p. 57Proposition 8.2oacl 8573
[TakeutiZaring] p. 57Proposition 8.3oa0 8554  oa0r 8576
[TakeutiZaring] p. 57Proposition 8.16omcl 8574
[TakeutiZaring] p. 58Corollary 8.5oacan 8586
[TakeutiZaring] p. 58Proposition 8.4nnaord 8657  nnaordi 8656  oaord 8585  oaordi 8584
[TakeutiZaring] p. 59Proposition 8.6iunss2 5049  uniss2 4941
[TakeutiZaring] p. 59Proposition 8.7oawordri 8588
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8593  oawordex 8595
[TakeutiZaring] p. 59Proposition 8.9nnacl 8649
[TakeutiZaring] p. 59Proposition 8.10oaabs 8686
[TakeutiZaring] p. 60Remarkoancom 9691
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8598
[TakeutiZaring] p. 62Exercise 1nnarcl 8654
[TakeutiZaring] p. 62Exercise 5oaword1 8590
[TakeutiZaring] p. 62Definition 8.15om0x 8557  omlim 8571  omsuc 8564
[TakeutiZaring] p. 62Definition 8.15(a)om0 8555
[TakeutiZaring] p. 63Proposition 8.17nnecl 8651  nnmcl 8650
[TakeutiZaring] p. 63Proposition 8.19nnmord 8670  nnmordi 8669  omord 8606  omordi 8604
[TakeutiZaring] p. 63Proposition 8.20omcan 8607
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8674  omwordri 8610
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8577
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8580  om1r 8581
[TakeutiZaring] p. 64Proposition 8.22om00 8613
[TakeutiZaring] p. 64Proposition 8.23omordlim 8615
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8616
[TakeutiZaring] p. 64Proposition 8.25odi 8617
[TakeutiZaring] p. 65Theorem 8.26omass 8618
[TakeutiZaring] p. 67Definition 8.30nnesuc 8646  oe0 8560  oelim 8572  oesuc 8565  onesuc 8568
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8558
[TakeutiZaring] p. 67Proposition 8.32oen0 8624
[TakeutiZaring] p. 67Proposition 8.33oeordi 8625
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8559
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8583
[TakeutiZaring] p. 68Corollary 8.34oeord 8626
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8632
[TakeutiZaring] p. 68Proposition 8.35oewordri 8630
[TakeutiZaring] p. 68Proposition 8.37oeworde 8631
[TakeutiZaring] p. 69Proposition 8.41oeoa 8635
[TakeutiZaring] p. 70Proposition 8.42oeoe 8637
[TakeutiZaring] p. 73Theorem 9.1trcl 9768  tz9.1 9769
[TakeutiZaring] p. 76Definition 9.9df-r1 9804  r10 9808  r1lim 9812  r1limg 9811  r1suc 9810  r1sucg 9809
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9820  r1ord2 9821  r1ordg 9818
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9830
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9855  tz9.13 9831  tz9.13g 9832
[TakeutiZaring] p. 79Definition 9.14df-rank 9805  rankval 9856  rankvalb 9837  rankvalg 9857
[TakeutiZaring] p. 79Proposition 9.16rankel 9879  rankelb 9864
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9893  rankval3 9880  rankval3b 9866
[TakeutiZaring] p. 79Proposition 9.18rankonid 9869
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9835
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9874  rankr1c 9861  rankr1g 9872
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9875
[TakeutiZaring] p. 80Exercise 1rankss 9889  rankssb 9888
[TakeutiZaring] p. 80Exercise 2unbndrank 9882
[TakeutiZaring] p. 80Proposition 9.19bndrank 9881
[TakeutiZaring] p. 83Axiom of Choiceac4 10515  dfac3 10161
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10070  numth 10512  numth2 10511
[TakeutiZaring] p. 85Definition 10.4cardval 10586
[TakeutiZaring] p. 85Proposition 10.5cardid 10587  cardid2 9993
[TakeutiZaring] p. 85Proposition 10.9oncard 10000
[TakeutiZaring] p. 85Proposition 10.10carden 10591
[TakeutiZaring] p. 85Proposition 10.11cardidm 9999
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9984
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 10005
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9997
[TakeutiZaring] p. 87Proposition 10.15pwen 9190
[TakeutiZaring] p. 88Exercise 1en0 9058
[TakeutiZaring] p. 88Exercise 7infensuc 9195
[TakeutiZaring] p. 89Exercise 10omxpen 9114
[TakeutiZaring] p. 90Corollary 10.23cardnn 10003
[TakeutiZaring] p. 90Definition 10.27alephiso 10138
[TakeutiZaring] p. 90Proposition 10.20nneneq 9246
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9265
[TakeutiZaring] p. 90Proposition 10.26alephprc 10139
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9251
[TakeutiZaring] p. 91Exercise 2alephle 10128
[TakeutiZaring] p. 91Exercise 3aleph0 10106
[TakeutiZaring] p. 91Exercise 4cardlim 10012
[TakeutiZaring] p. 91Exercise 7infpss 10256
[TakeutiZaring] p. 91Exercise 8infcntss 9362
[TakeutiZaring] p. 91Definition 10.29df-fin 8989  isfi 9016
[TakeutiZaring] p. 92Proposition 10.32onfin 9267
[TakeutiZaring] p. 92Proposition 10.34imadomg 10574
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9107
[TakeutiZaring] p. 93Proposition 10.35fodomb 10566
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10226  unxpdom 9289
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 10014  cardsdomelir 10013
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9291
[TakeutiZaring] p. 94Proposition 10.39infxpen 10054
[TakeutiZaring] p. 95Definition 10.42df-map 8868
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10602  infxpidm2 10057
[TakeutiZaring] p. 95Proposition 10.41infdju 10247  infxp 10254
[TakeutiZaring] p. 96Proposition 10.44pw2en 9119  pw2f1o 9117
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9183
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10527
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10522  ac6s5 10531
[TakeutiZaring] p. 98Theorem 10.47unidom 10583
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10584  uniimadomf 10585
[TakeutiZaring] p. 100Definition 11.1cfcof 10314
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10309
[TakeutiZaring] p. 102Exercise 1cfle 10294
[TakeutiZaring] p. 102Exercise 2cf0 10291
[TakeutiZaring] p. 102Exercise 3cfsuc 10297
[TakeutiZaring] p. 102Exercise 4cfom 10304
[TakeutiZaring] p. 102Proposition 11.9coftr 10313
[TakeutiZaring] p. 103Theorem 11.15alephreg 10622
[TakeutiZaring] p. 103Proposition 11.11cardcf 10292
[TakeutiZaring] p. 103Proposition 11.13alephsing 10316
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10137
[TakeutiZaring] p. 104Proposition 11.16carduniima 10136
[TakeutiZaring] p. 104Proposition 11.18alephfp 10148  alephfp2 10149
[TakeutiZaring] p. 106Theorem 11.20gchina 10739
[TakeutiZaring] p. 106Theorem 11.21mappwen 10152
[TakeutiZaring] p. 107Theorem 11.26konigth 10609
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10623
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10624
[Tarski] p. 67Axiom B5ax-c5 38884
[Tarski] p. 67Scheme B5sp 2183
[Tarski] p. 68Lemma 6avril1 30482  equid 2011
[Tarski] p. 69Lemma 7equcomi 2016
[Tarski] p. 70Lemma 14spim 2392  spime 2394  spimew 1971
[Tarski] p. 70Lemma 16ax-12 2177  ax-c15 38890  ax12i 1966
[Tarski] p. 70Lemmas 16 and 17sb6 2085
[Tarski] p. 75Axiom B7ax6v 1968
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1910  ax5ALT 38908
[Tarski], p. 75Scheme B8 of system S2ax-7 2007  ax-8 2110  ax-9 2118
[Tarski1999] p. 178Axiom 4axtgsegcon 28472
[Tarski1999] p. 178Axiom 5axtg5seg 28473
[Tarski1999] p. 179Axiom 7axtgpasch 28475
[Tarski1999] p. 180Axiom 7.1axtgpasch 28475
[Tarski1999] p. 185Axiom 11axtgcont1 28476
[Truss] p. 114Theorem 5.18ruc 16279
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37666
[Viaclovsky8] p. 3Proposition 7ismblfin 37668
[Weierstrass] p. 272Definitiondf-mdet 22591  mdetuni 22628
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 904
[WhiteheadRussell] p. 96Axiom *1.3olc 869
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 870
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 920
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 970
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 188
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 37446
[WhiteheadRussell] p. 100Theorem *2.05frege5 43813  imim2 58  wl-luk-imim2 37441
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47031  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 897
[WhiteheadRussell] p. 101Theorem *2.06barbara 2663  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 903
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37444
[WhiteheadRussell] p. 101Theorem *2.11exmid 895
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 898
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 44947  wl-luk-notnotr 37445
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43843  axfrege28 43842  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 868
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 925
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37438
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 890
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 942
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30420  pm2.27 42  wl-luk-pm2.27 37436
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 923
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38364
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 924
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 972
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 973
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 971
[WhiteheadRussell] p. 105Definition *2.33df-3or 1088
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 907
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 908
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 945
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 882
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 883
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 191
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 884
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 885
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 886
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 852
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 853
[WhiteheadRussell] p. 107Theorem *2.55orel1 889
[WhiteheadRussell] p. 107Theorem *2.56orel2 891
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 900
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 943
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 944
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 892  pm2.67 893
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 899
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 975
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 901
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 976
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 977
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 934
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 932
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 974
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 978
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 933
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 994
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 995
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 996
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 997
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 998
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 471
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 459
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 402
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 803
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 448
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 449
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 482  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 484  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 765
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 766
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 808
[WhiteheadRussell] p. 113Fact)pm3.45 622
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 810
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 492
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 493
[WhiteheadRussell] p. 113Theorem *3.44jao 963  pm3.44 962
[WhiteheadRussell] p. 113Theorem *3.47anim12 809
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 966
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 261
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 353
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 807
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 833
[WhiteheadRussell] p. 117Theorem *4.21bicom 222
[WhiteheadRussell] p. 117Theorem *4.22biantr 806  bitr 805
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 563
[WhiteheadRussell] p. 117Theorem *4.25oridm 905  pm4.25 906
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1010
[WhiteheadRussell] p. 118Theorem *4.31orcom 871
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[WhiteheadRussell] p. 118Theorem *4.33orass 922
[WhiteheadRussell] p. 118Theorem *4.36anbi1 633
[WhiteheadRussell] p. 118Theorem *4.37orbi1 918
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 637
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 979
[WhiteheadRussell] p. 118Definition *4.34df-3an 1089
[WhiteheadRussell] p. 119Theorem *4.41ordi 1008
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1054
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1025
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 999
[WhiteheadRussell] p. 119Theorem *4.45orabs 1001  pm4.45 1000  pm4.45im 828
[WhiteheadRussell] p. 120Theorem *4.5anor 985
[WhiteheadRussell] p. 120Theorem *4.6imor 854
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 984
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 987
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 988
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 989
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 990
[WhiteheadRussell] p. 120Theorem *4.56ioran 986  pm4.56 991
[WhiteheadRussell] p. 120Theorem *4.57oran 992  pm4.57 993
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 857
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 850
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 851
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 398
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 557  pm4.71d 561  pm4.71i 559  pm4.71r 558  pm4.71rd 562  pm4.71ri 560
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 952
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 937
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 964  pm4.77 965
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 935
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1006
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1026
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1027
[WhiteheadRussell] p. 122Theorem *4.84imbi1 347
[WhiteheadRussell] p. 122Theorem *4.85imbi2 348
[WhiteheadRussell] p. 122Theorem *4.86bibi1 351
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 387  impexp 450  pm4.87 844
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 824
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 947  pm5.11g 946
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 948
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 950
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 949
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1015
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1016
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1014
[WhiteheadRussell] p. 124Theorem *5.18nbbn 383  pm5.18 381
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 386
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 825
[WhiteheadRussell] p. 124Theorem *5.22xor 1017
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1050
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1051
[WhiteheadRussell] p. 124Theorem *5.25dfor2 902
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 572
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 388
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 361
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1004
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 956
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 831
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 573
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 836
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 826
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 834
[WhiteheadRussell] p. 125Theorem *5.41imdi 389  pm5.41 390
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 543
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 542
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1007
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1020
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 951
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1003
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1021
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1022
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1030
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1031
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44377
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44378
[WhiteheadRussell] p. 147Theorem *10.2219.26 1870
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44379
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44380
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44381
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1893
[WhiteheadRussell] p. 151Theorem *10.301albitr 44382
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44383
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44384
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44385
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44386
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44388
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44389
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44390
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44387
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2090
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44393
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44394
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2070
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2160
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1829
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1830
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44395
[WhiteheadRussell] p. 162Theorem *11.322alim 44396
[WhiteheadRussell] p. 162Theorem *11.332albi 44397
[WhiteheadRussell] p. 162Theorem *11.342exim 44398
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44400
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44399
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1887
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44402
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44403
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44401
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1828
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44404
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44405
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1846
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44406
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2348
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1860
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44411
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44407
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44408
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44409
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44410
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44415
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44412
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44413
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44414
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44416
[WhiteheadRussell] p. 175Definition *14.02df-eu 2569
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44426  pm13.13b 44427
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44428
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3022
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3023
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3666
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44434
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44435
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44429
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44572  pm13.193 44430
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44431
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44432
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44433
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44440
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44439
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44438
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3853
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44441  pm14.122b 44442  pm14.122c 44443
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44444  pm14.123b 44445  pm14.123c 44446
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44448
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44447
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44449
[WhiteheadRussell] p. 190Theorem *14.22iota4 6542
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44450
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6543
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44451
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44453
[WhiteheadRussell] p. 192Theorem *14.26eupick 2633  eupickbi 2636  sbaniota 44454
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44452
[WhiteheadRussell] p. 192Theorem *14.271eubi 2584
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44456
[WhiteheadRussell] p. 235Definition *30.01conventions 30419  df-fv 6569
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 10041  pm54.43lem 10040
[Young] p. 141Definition of operator orderingleop2 32143
[Young] p. 142Example 12.2(i)0leop 32149  idleop 32150
[vandenDries] p. 42Lemma 61irrapx1 42839
[vandenDries] p. 43Theorem 62pellex 42846  pellexlem1 42840

This page was last updated on 29-Oct-2025.
Copyright terms: Public domain