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 17712
[Adamek] p. 21Condition 3.1(b)df-cat 17712
[Adamek] p. 22Example 3.3(1)df-setc 18129
[Adamek] p. 24Example 3.3(4.c)0cat 17733
[Adamek] p. 24Example 3.3(4.d)df-prstc 48863  prsthinc 48854
[Adamek] p. 24Example 3.3(4.e)df-mndtc 48886  df-mndtc 48886
[Adamek] p. 25Definition 3.5df-oppc 17756
[Adamek] p. 25Example 3.6(1)oduoppcciso 48881
[Adamek] p. 25Example 3.6(2)oppgoppcco 48899  oppgoppchom 48898  oppgoppcid 48900
[Adamek] p. 28Remark 3.9oppciso 17828
[Adamek] p. 28Remark 3.12invf1o 17816  invisoinvl 17837
[Adamek] p. 28Example 3.13idinv 17836  idiso 17835
[Adamek] p. 28Corollary 3.11inveq 17821
[Adamek] p. 28Definition 3.8df-inv 17795  df-iso 17796  dfiso2 17819
[Adamek] p. 28Proposition 3.10sectcan 17802
[Adamek] p. 29Remark 3.16cicer 17853
[Adamek] p. 29Definition 3.15cic 17846  df-cic 17843
[Adamek] p. 29Definition 3.17df-func 17908
[Adamek] p. 29Proposition 3.14(1)invinv 17817
[Adamek] p. 29Proposition 3.14(2)invco 17818  isoco 17824
[Adamek] p. 30Remark 3.19df-func 17908
[Adamek] p. 30Example 3.20(1)idfucl 17931
[Adamek] p. 32Proposition 3.21funciso 17924
[Adamek] p. 33Example 3.26(2)df-thinc 48819  prsthinc 48854  thincciso 48848  thinccisod 48849
[Adamek] p. 33Example 3.26(3)df-mndtc 48886
[Adamek] p. 33Proposition 3.23cofucl 17938
[Adamek] p. 34Remark 3.28(2)catciso 18164
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18222
[Adamek] p. 34Definition 3.27(2)df-fth 17958
[Adamek] p. 34Definition 3.27(3)df-full 17957
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18222
[Adamek] p. 35Corollary 3.32ffthiso 17982
[Adamek] p. 35Proposition 3.30(c)cofth 17988
[Adamek] p. 35Proposition 3.30(d)cofull 17987
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18207
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18207
[Adamek] p. 39Definition 3.41funcoppc 17925
[Adamek] p. 39Definition 3.44.df-catc 18152
[Adamek] p. 39Proposition 3.43(c)fthoppc 17976
[Adamek] p. 39Proposition 3.43(d)fulloppc 17975
[Adamek] p. 40Remark 3.48catccat 18161
[Adamek] p. 40Definition 3.47df-catc 18152
[Adamek] p. 48Example 4.3(1.a)0subcat 17888
[Adamek] p. 48Example 4.3(1.b)catsubcat 17889
[Adamek] p. 48Definition 4.1(2)fullsubc 17900
[Adamek] p. 48Definition 4.1(a)df-subc 17859
[Adamek] p. 49Remark 4.4(2)ressffth 17991
[Adamek] p. 83Definition 6.1df-nat 17997
[Adamek] p. 87Remark 6.14(a)fuccocl 18020
[Adamek] p. 87Remark 6.14(b)fucass 18024
[Adamek] p. 87Definition 6.15df-fuc 17998
[Adamek] p. 88Remark 6.16fuccat 18026
[Adamek] p. 101Definition 7.1df-inito 18037
[Adamek] p. 101Example 7.2 (6)irinitoringc 21507
[Adamek] p. 102Definition 7.4df-termo 18038
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18065
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18069
[Adamek] p. 103Definition 7.7df-zeroo 18039
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21508
[Adamek] p. 103Proposition 7.6termoeu1w 18072
[Adamek] p. 106Definition 7.19df-sect 17794
[Adamek] p. 185Section 10.67updjud 9971
[Adamek] p. 478Item Rngdf-ringc 20662
[AhoHopUll] p. 2Section 1.1df-bigo 48397
[AhoHopUll] p. 12Section 1.3df-blen 48419
[AhoHopUll] p. 318Section 9.1df-concat 14605  df-pfx 14705  df-substr 14675  df-word 14549  lencl 14567  wrd0 14573
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24744  df-nmoo 30773
[AkhiezerGlazman] p. 64Theoremhmopidmch 32181  hmopidmchi 32179
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32229  pjcmul2i 32230
[AkhiezerGlazman] p. 72Theoremcnvunop 31946  unoplin 31948
[AkhiezerGlazman] p. 72Equation 2unopadj 31947  unopadj2 31966
[AkhiezerGlazman] p. 73Theoremelunop2 32041  lnopunii 32040
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32114
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27975
[Alling] p. 184Axiom Bbdayfo 27736
[Alling] p. 184Axiom Osltso 27735
[Alling] p. 184Axiom SDnodense 27751
[Alling] p. 185Lemma 0nocvxmin 27837
[Alling] p. 185Theoremconway 27858
[Alling] p. 185Axiom FEnoeta 27802
[Alling] p. 186Theorem 4slerec 27878
[Alling], p. 2Definitionrp-brsslt 43412
[Alling], p. 3Notenla0001 43415  nla0002 43413  nla0003 43414
[Apostol] p. 18Theorem I.1addcan 11442  addcan2d 11462  addcan2i 11452  addcand 11461  addcani 11451
[Apostol] p. 18Theorem I.2negeu 11495
[Apostol] p. 18Theorem I.3negsub 11554  negsubd 11623  negsubi 11584
[Apostol] p. 18Theorem I.4negneg 11556  negnegd 11608  negnegi 11576
[Apostol] p. 18Theorem I.5subdi 11693  subdid 11716  subdii 11709  subdir 11694  subdird 11717  subdiri 11710
[Apostol] p. 18Theorem I.6mul01 11437  mul01d 11457  mul01i 11448  mul02 11436  mul02d 11456  mul02i 11447
[Apostol] p. 18Theorem I.7mulcan 11897  mulcan2d 11894  mulcand 11893  mulcani 11899
[Apostol] p. 18Theorem I.8receu 11905  xreceu 32888
[Apostol] p. 18Theorem I.9divrec 11935  divrecd 12043  divreci 12009  divreczi 12002
[Apostol] p. 18Theorem I.10recrec 11961  recreci 11996
[Apostol] p. 18Theorem I.11mul0or 11900  mul0ord 11910  mul0ori 11908
[Apostol] p. 18Theorem I.12mul2neg 11699  mul2negd 11715  mul2negi 11708  mulneg1 11696  mulneg1d 11713  mulneg1i 11706
[Apostol] p. 18Theorem I.13divadddiv 11979  divadddivd 12084  divadddivi 12026
[Apostol] p. 18Theorem I.14divmuldiv 11964  divmuldivd 12081  divmuldivi 12024  rdivmuldivd 20429
[Apostol] p. 18Theorem I.15divdivdiv 11965  divdivdivd 12087  divdivdivi 12027
[Apostol] p. 20Axiom 7rpaddcl 13054  rpaddcld 13089  rpmulcl 13055  rpmulcld 13090
[Apostol] p. 20Axiom 8rpneg 13064
[Apostol] p. 20Axiom 90nrp 13067
[Apostol] p. 20Theorem I.17lttri 11384
[Apostol] p. 20Theorem I.18ltadd1d 11853  ltadd1dd 11871  ltadd1i 11814
[Apostol] p. 20Theorem I.19ltmul1 12114  ltmul1a 12113  ltmul1i 12183  ltmul1ii 12193  ltmul2 12115  ltmul2d 13116  ltmul2dd 13130  ltmul2i 12186
[Apostol] p. 20Theorem I.20msqgt0 11780  msqgt0d 11827  msqgt0i 11797
[Apostol] p. 20Theorem I.210lt1 11782
[Apostol] p. 20Theorem I.23lt0neg1 11766  lt0neg1d 11829  ltneg 11760  ltnegd 11838  ltnegi 11804
[Apostol] p. 20Theorem I.25lt2add 11745  lt2addd 11883  lt2addi 11822
[Apostol] p. 20Definition of positive numbersdf-rp 13032
[Apostol] p. 21Exercise 4recgt0 12110  recgt0d 12199  recgt0i 12170  recgt0ii 12171
[Apostol] p. 22Definition of integersdf-z 12611
[Apostol] p. 22Definition of positive integersdfnn3 12277
[Apostol] p. 22Definition of rationalsdf-q 12988
[Apostol] p. 24Theorem I.26supeu 9491
[Apostol] p. 26Theorem I.28nnunb 12519
[Apostol] p. 26Theorem I.29arch 12520  archd 45104
[Apostol] p. 28Exercise 2btwnz 12718
[Apostol] p. 28Exercise 3nnrecl 12521
[Apostol] p. 28Exercise 4rebtwnz 12986
[Apostol] p. 28Exercise 5zbtwnre 12985
[Apostol] p. 28Exercise 6qbtwnre 13237
[Apostol] p. 28Exercise 10(a)zeneo 16372  zneo 12698  zneoALTV 47593
[Apostol] p. 29Theorem I.35cxpsqrtth 26786  msqsqrtd 15475  resqrtth 15290  sqrtth 15399  sqrtthi 15405  sqsqrtd 15474
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12266
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12952
[Apostol] p. 361Remarkcrreczi 14263
[Apostol] p. 363Remarkabsgt0i 15434
[Apostol] p. 363Exampleabssubd 15488  abssubi 15438
[ApostolNT] p. 7Remarkfmtno0 47464  fmtno1 47465  fmtno2 47474  fmtno3 47475  fmtno4 47476  fmtno5fac 47506  fmtnofz04prm 47501
[ApostolNT] p. 7Definitiondf-fmtno 47452
[ApostolNT] p. 8Definitiondf-ppi 27157
[ApostolNT] p. 14Definitiondf-dvds 16287
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16303
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16327
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16322
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16316
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16318
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16304
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16305
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16310
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16344
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16346
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16348
[ApostolNT] p. 15Definitiondf-gcd 16528  dfgcd2 16579
[ApostolNT] p. 16Definitionisprm2 16715
[ApostolNT] p. 16Theorem 1.5coprmdvds 16686
[ApostolNT] p. 16Theorem 1.7prminf 16948
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16546
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16580
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16582
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16561
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16553
[ApostolNT] p. 17Theorem 1.8coprm 16744
[ApostolNT] p. 17Theorem 1.9euclemma 16746
[ApostolNT] p. 17Theorem 1.101arith2 16961
[ApostolNT] p. 18Theorem 1.13prmrec 16955
[ApostolNT] p. 19Theorem 1.14divalg 16436
[ApostolNT] p. 20Theorem 1.15eucalg 16620
[ApostolNT] p. 24Definitiondf-mu 27158
[ApostolNT] p. 25Definitiondf-phi 16799
[ApostolNT] p. 25Theorem 2.1musum 27248
[ApostolNT] p. 26Theorem 2.2phisum 16823
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16809
[ApostolNT] p. 28Theorem 2.5(c)phimul 16813
[ApostolNT] p. 32Definitiondf-vma 27155
[ApostolNT] p. 32Theorem 2.9muinv 27250
[ApostolNT] p. 32Theorem 2.10vmasum 27274
[ApostolNT] p. 38Remarkdf-sgm 27159
[ApostolNT] p. 38Definitiondf-sgm 27159
[ApostolNT] p. 75Definitiondf-chp 27156  df-cht 27154
[ApostolNT] p. 104Definitioncongr 16697
[ApostolNT] p. 106Remarkdvdsval3 16290
[ApostolNT] p. 106Definitionmoddvds 16297
[ApostolNT] p. 107Example 2mod2eq0even 16379
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16380
[ApostolNT] p. 107Example 4zmod1congr 13924
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13962
[ApostolNT] p. 107Theorem 5.2(c)modexp 14273
[ApostolNT] p. 108Theorem 5.3modmulconst 16321
[ApostolNT] p. 109Theorem 5.4cncongr1 16700
[ApostolNT] p. 109Theorem 5.6gcdmodi 17107
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16702
[ApostolNT] p. 113Theorem 5.17eulerth 16816
[ApostolNT] p. 113Theorem 5.18vfermltl 16834
[ApostolNT] p. 114Theorem 5.19fermltl 16817
[ApostolNT] p. 116Theorem 5.24wilthimp 27129
[ApostolNT] p. 179Definitiondf-lgs 27353  lgsprme0 27397
[ApostolNT] p. 180Example 11lgs 27398
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27374
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27389
[ApostolNT] p. 181Theorem 9.4m1lgs 27446
[ApostolNT] p. 181Theorem 9.52lgs 27465  2lgsoddprm 27474
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27432
[ApostolNT] p. 185Theorem 9.8lgsquad 27441
[ApostolNT] p. 188Definitiondf-lgs 27353  lgs1 27399
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27390
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27392
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27400
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27401
[Baer] p. 40Property (b)mapdord 41620
[Baer] p. 40Property (c)mapd11 41621
[Baer] p. 40Property (e)mapdin 41644  mapdlsm 41646
[Baer] p. 40Property (f)mapd0 41647
[Baer] p. 40Definition of projectivitydf-mapd 41607  mapd1o 41630
[Baer] p. 41Property (g)mapdat 41649
[Baer] p. 44Part (1)mapdpg 41688
[Baer] p. 45Part (2)hdmap1eq 41783  mapdheq 41710  mapdheq2 41711  mapdheq2biN 41712
[Baer] p. 45Part (3)baerlem3 41695
[Baer] p. 46Part (4)mapdheq4 41714  mapdheq4lem 41713
[Baer] p. 46Part (5)baerlem5a 41696  baerlem5abmN 41700  baerlem5amN 41698  baerlem5b 41697  baerlem5bmN 41699
[Baer] p. 47Part (6)hdmap1l6 41803  hdmap1l6a 41791  hdmap1l6e 41796  hdmap1l6f 41797  hdmap1l6g 41798  hdmap1l6lem1 41789  hdmap1l6lem2 41790  mapdh6N 41729  mapdh6aN 41717  mapdh6eN 41722  mapdh6fN 41723  mapdh6gN 41724  mapdh6lem1N 41715  mapdh6lem2N 41716
[Baer] p. 48Part 9hdmapval 41810
[Baer] p. 48Part 10hdmap10 41822
[Baer] p. 48Part 11hdmapadd 41825
[Baer] p. 48Part (6)hdmap1l6h 41799  mapdh6hN 41725
[Baer] p. 48Part (7)mapdh75cN 41735  mapdh75d 41736  mapdh75e 41734  mapdh75fN 41737  mapdh7cN 41731  mapdh7dN 41732  mapdh7eN 41730  mapdh7fN 41733
[Baer] p. 48Part (8)mapdh8 41770  mapdh8a 41757  mapdh8aa 41758  mapdh8ab 41759  mapdh8ac 41760  mapdh8ad 41761  mapdh8b 41762  mapdh8c 41763  mapdh8d 41765  mapdh8d0N 41764  mapdh8e 41766  mapdh8g 41767  mapdh8i 41768  mapdh8j 41769
[Baer] p. 48Part (9)mapdh9a 41771
[Baer] p. 48Equation 10mapdhvmap 41751
[Baer] p. 49Part 12hdmap11 41830  hdmapeq0 41826  hdmapf1oN 41847  hdmapneg 41828  hdmaprnN 41846  hdmaprnlem1N 41831  hdmaprnlem3N 41832  hdmaprnlem3uN 41833  hdmaprnlem4N 41835  hdmaprnlem6N 41836  hdmaprnlem7N 41837  hdmaprnlem8N 41838  hdmaprnlem9N 41839  hdmapsub 41829
[Baer] p. 49Part 14hdmap14lem1 41850  hdmap14lem10 41859  hdmap14lem1a 41848  hdmap14lem2N 41851  hdmap14lem2a 41849  hdmap14lem3 41852  hdmap14lem8 41857  hdmap14lem9 41858
[Baer] p. 50Part 14hdmap14lem11 41860  hdmap14lem12 41861  hdmap14lem13 41862  hdmap14lem14 41863  hdmap14lem15 41864  hgmapval 41869
[Baer] p. 50Part 15hgmapadd 41876  hgmapmul 41877  hgmaprnlem2N 41879  hgmapvs 41873
[Baer] p. 50Part 16hgmaprnN 41883
[Baer] p. 110Lemma 1hdmapip0com 41899
[Baer] p. 110Line 27hdmapinvlem1 41900
[Baer] p. 110Line 28hdmapinvlem2 41901
[Baer] p. 110Line 30hdmapinvlem3 41902
[Baer] p. 110Part 1.2hdmapglem5 41904  hgmapvv 41908
[Baer] p. 110Proposition 1hdmapinvlem4 41903
[Baer] p. 111Line 10hgmapvvlem1 41905
[Baer] p. 111Line 15hdmapg 41912  hdmapglem7 41911
[Bauer], p. 483Theorem 1.22irrexpq 26787  2irrexpqALT 26857
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2566
[BellMachover] p. 460Notationdf-mo 2537
[BellMachover] p. 460Definitionmo3 2561
[BellMachover] p. 461Axiom Extax-ext 2705
[BellMachover] p. 462Theorem 1.1axextmo 2709
[BellMachover] p. 463Axiom Repaxrep5 5292
[BellMachover] p. 463Scheme Sepax-sep 5301
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37046  sepex 5305
[BellMachover] p. 466Problemaxpow2 5372
[BellMachover] p. 466Axiom Powaxpow3 5373
[BellMachover] p. 466Axiom Unionaxun2 7755
[BellMachover] p. 468Definitiondf-ord 6388
[BellMachover] p. 469Theorem 2.2(i)ordirr 6403
[BellMachover] p. 469Theorem 2.2(iii)onelon 6410
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6405
[BellMachover] p. 471Definition of Ndf-om 7887
[BellMachover] p. 471Problem 2.5(ii)uniordint 7820
[BellMachover] p. 471Definition of Limdf-lim 6390
[BellMachover] p. 472Axiom Infzfinf2 9679
[BellMachover] p. 473Theorem 2.8limom 7902
[BellMachover] p. 477Equation 3.1df-r1 9801
[BellMachover] p. 478Definitionrankval2 9855
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9819  r1ord3g 9816
[BellMachover] p. 480Axiom Regzfreg 9632
[BellMachover] p. 488Axiom ACac5 10514  dfac4 10159
[BellMachover] p. 490Definition of alephalephval3 10147
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39300
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32381
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32423  chirredi 32422
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32411
[Beran] p. 3Definition of joinsshjval3 31382
[Beran] p. 39Theorem 2.3(i)cmcm2 31644  cmcm2i 31621  cmcm2ii 31626  cmt2N 39231
[Beran] p. 40Theorem 2.3(iii)lecm 31645  lecmi 31630  lecmii 31631
[Beran] p. 45Theorem 3.4cmcmlem 31619
[Beran] p. 49Theorem 4.2cm2j 31648  cm2ji 31653  cm2mi 31654
[Beran] p. 95Definitiondf-sh 31235  issh2 31237
[Beran] p. 95Lemma 3.1(S5)his5 31114
[Beran] p. 95Lemma 3.1(S6)his6 31127
[Beran] p. 95Lemma 3.1(S7)his7 31118
[Beran] p. 95Lemma 3.2(S8)ho01i 31856
[Beran] p. 95Lemma 3.2(S9)hoeq1 31858
[Beran] p. 95Lemma 3.2(S10)ho02i 31857
[Beran] p. 95Lemma 3.2(S11)hoeq2 31859
[Beran] p. 95Postulate (S1)ax-his1 31110  his1i 31128
[Beran] p. 95Postulate (S2)ax-his2 31111
[Beran] p. 95Postulate (S3)ax-his3 31112
[Beran] p. 95Postulate (S4)ax-his4 31113
[Beran] p. 96Definition of normdf-hnorm 30996  dfhnorm2 31150  normval 31152
[Beran] p. 96Definition for Cauchy sequencehcau 31212
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31001
[Beran] p. 96Definition of complete subspaceisch3 31269
[Beran] p. 96Definition of convergedf-hlim 31000  hlimi 31216
[Beran] p. 97Theorem 3.3(i)norm-i-i 31161  norm-i 31157
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31165  norm-ii 31166  normlem0 31137  normlem1 31138  normlem2 31139  normlem3 31140  normlem4 31141  normlem5 31142  normlem6 31143  normlem7 31144  normlem7tALT 31147
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31167  norm-iii 31168
[Beran] p. 98Remark 3.4bcs 31209  bcsiALT 31207  bcsiHIL 31208
[Beran] p. 98Remark 3.4(B)normlem9at 31149  normpar 31183  normpari 31182
[Beran] p. 98Remark 3.4(C)normpyc 31174  normpyth 31173  normpythi 31170
[Beran] p. 99Remarklnfn0 32075  lnfn0i 32070  lnop0 31994  lnop0i 31998
[Beran] p. 99Theorem 3.5(i)nmcexi 32054  nmcfnex 32081  nmcfnexi 32079  nmcopex 32057  nmcopexi 32055
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32082  nmcfnlbi 32080  nmcoplb 32058  nmcoplbi 32056
[Beran] p. 99Theorem 3.5(iii)lnfncon 32084  lnfnconi 32083  lnopcon 32063  lnopconi 32062
[Beran] p. 100Lemma 3.6normpar2i 31184
[Beran] p. 101Lemma 3.6norm3adifi 31181  norm3adifii 31176  norm3dif 31178  norm3difi 31175
[Beran] p. 102Theorem 3.7(i)chocunii 31329  pjhth 31421  pjhtheu 31422  pjpjhth 31453  pjpjhthi 31454  pjth 25486
[Beran] p. 102Theorem 3.7(ii)ococ 31434  ococi 31433
[Beran] p. 103Remark 3.8nlelchi 32089
[Beran] p. 104Theorem 3.9riesz3i 32090  riesz4 32092  riesz4i 32091
[Beran] p. 104Theorem 3.10cnlnadj 32107  cnlnadjeu 32106  cnlnadjeui 32105  cnlnadji 32104  cnlnadjlem1 32095  nmopadjlei 32116
[Beran] p. 106Theorem 3.11(i)adjeq0 32119
[Beran] p. 106Theorem 3.11(v)nmopadji 32118
[Beran] p. 106Theorem 3.11(ii)adjmul 32120
[Beran] p. 106Theorem 3.11(iv)adjadj 31964
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32130  nmopcoadji 32129
[Beran] p. 106Theorem 3.11(iii)adjadd 32121
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32131
[Beran] p. 106Theorem 3.11(viii)adjcoi 32128  pjadj2coi 32232  pjadjcoi 32189
[Beran] p. 107Definitiondf-ch 31249  isch2 31251
[Beran] p. 107Remark 3.12choccl 31334  isch3 31269  occl 31332  ocsh 31311  shoccl 31333  shocsh 31312
[Beran] p. 107Remark 3.12(B)ococin 31436
[Beran] p. 108Theorem 3.13chintcl 31360
[Beran] p. 109Property (i)pjadj2 32215  pjadj3 32216  pjadji 31713  pjadjii 31702
[Beran] p. 109Property (ii)pjidmco 32209  pjidmcoi 32205  pjidmi 31701
[Beran] p. 110Definition of projector orderingpjordi 32201
[Beran] p. 111Remarkho0val 31778  pjch1 31698
[Beran] p. 111Definitiondf-hfmul 31762  df-hfsum 31761  df-hodif 31760  df-homul 31759  df-hosum 31758
[Beran] p. 111Lemma 4.4(i)pjo 31699
[Beran] p. 111Lemma 4.4(ii)pjch 31722  pjchi 31460
[Beran] p. 111Lemma 4.4(iii)pjoc2 31467  pjoc2i 31466
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31708
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32193  pjssmii 31709
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32192
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32191
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32196
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32194  pjssge0ii 31710
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32195  pjdifnormii 31711
[Bobzien] p. 116Statement T3stoic3 1772
[Bobzien] p. 117Statement T2stoic2a 1770
[Bobzien] p. 117Statement T4stoic4a 1773
[Bobzien] p. 117Conclusion the contradictorystoic1a 1768
[Bogachev] p. 16Definition 1.5df-oms 34273
[Bogachev] p. 17Lemma 1.5.4omssubadd 34281
[Bogachev] p. 17Example 1.5.2omsmon 34279
[Bogachev] p. 41Definition 1.11.2df-carsg 34283
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34303
[Bogachev] p. 116Definition 2.3.1df-itgm 34334  df-sitm 34312
[Bogachev] p. 118Chapter 2.4.4df-itgm 34334
[Bogachev] p. 118Definition 2.4.1df-sitg 34311
[Bollobas] p. 1Section I.1df-edg 29079  isuhgrop 29101  isusgrop 29193  isuspgrop 29192
[Bollobas] p. 2Section I.1df-isubgr 47784  df-subgr 29299  uhgrspan1 29334  uhgrspansubgr 29322
[Bollobas] p. 3Definitiondf-gric 47804  gricuspgr 47824  isuspgrim 47812
[Bollobas] p. 3Section I.1cusgrsize 29486  df-clnbgr 47743  df-cusgr 29443  df-nbgr 29364  fusgrmaxsize 29496
[Bollobas] p. 4Definitiondf-upwlks 47977  df-wlks 29631
[Bollobas] p. 4Section I.1finsumvtxdg2size 29582  finsumvtxdgeven 29584  fusgr1th 29583  fusgrvtxdgonume 29586  vtxdgoddnumeven 29585
[Bollobas] p. 5Notationdf-pths 29748
[Bollobas] p. 5Definitiondf-crcts 29818  df-cycls 29819  df-trls 29724  df-wlkson 29632
[Bollobas] p. 7Section I.1df-ushgr 29090
[BourbakiAlg1] p. 1Definition 1df-clintop 48043  df-cllaw 48029  df-mgm 18665  df-mgm2 48062
[BourbakiAlg1] p. 4Definition 5df-assintop 48044  df-asslaw 48031  df-sgrp 18744  df-sgrp2 48064
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48063  df-comlaw 48030
[BourbakiAlg1] p. 12Definition 2df-mnd 18760
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33013  mndlactf1o 33017  mndractf1 33015  mndractf1o 33018
[BourbakiAlg1] p. 92Definition 1df-ring 20252
[BourbakiAlg1] p. 93Section I.8.1df-rng 20170
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33660
[BourbakiAlg2] p. 113Chapter 5.assafld 33664  assarrginv 33663
[BourbakiCAlg2], p. 228Proposition 21arithidom 33544  dfufd2 33557
[BourbakiEns] p. Proposition 8fcof1 7306  fcofo 7307
[BourbakiTop1] p. Remarkxnegmnf 13248  xnegpnf 13247
[BourbakiTop1] p. Remark rexneg 13249
[BourbakiTop1] p. Remark 3ust0 24243  ustfilxp 24236
[BourbakiTop1] p. Axiom GT'tgpsubcn 24113
[BourbakiTop1] p. Criterionishmeo 23782
[BourbakiTop1] p. Example 1cstucnd 24308  iducn 24307  snfil 23887
[BourbakiTop1] p. Example 2neifil 23903
[BourbakiTop1] p. Theorem 1cnextcn 24090
[BourbakiTop1] p. Theorem 2ucnextcn 24328
[BourbakiTop1] p. Theorem 3df-hcmp 33917
[BourbakiTop1] p. Paragraph 3infil 23886
[BourbakiTop1] p. Definition 1df-ucn 24300  df-ust 24224  filintn0 23884  filn0 23885  istgp 24100  ucnprima 24306
[BourbakiTop1] p. Definition 2df-cfilu 24311
[BourbakiTop1] p. Definition 3df-cusp 24322  df-usp 24281  df-utop 24255  trust 24253
[BourbakiTop1] p. Definition 6df-pcmp 33816
[BourbakiTop1] p. Property V_issnei2 23139
[BourbakiTop1] p. Theorem 1(d)iscncl 23292
[BourbakiTop1] p. Condition F_Iustssel 24229
[BourbakiTop1] p. Condition U_Iustdiag 24232
[BourbakiTop1] p. Property V_iiinnei 23148
[BourbakiTop1] p. Property V_ivneiptopreu 23156  neissex 23150
[BourbakiTop1] p. Proposition 1neips 23136  neiss 23132  ucncn 24309  ustund 24245  ustuqtop 24270
[BourbakiTop1] p. Proposition 2cnpco 23290  neiptopreu 23156  utop2nei 24274  utop3cls 24275
[BourbakiTop1] p. Proposition 3fmucnd 24316  uspreg 24298  utopreg 24276
[BourbakiTop1] p. Proposition 4imasncld 23714  imasncls 23715  imasnopn 23713
[BourbakiTop1] p. Proposition 9cnpflf2 24023
[BourbakiTop1] p. Condition F_IIustincl 24231
[BourbakiTop1] p. Condition U_IIustinvel 24233
[BourbakiTop1] p. Property V_iiielnei 23134
[BourbakiTop1] p. Proposition 11cnextucn 24327
[BourbakiTop1] p. Condition F_IIbustbasel 24230
[BourbakiTop1] p. Condition U_IIIustexhalf 24234
[BourbakiTop1] p. Definition C'''df-cmp 23410
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23869
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22915
[BourbakiTop2] p. 195Definition 1df-ldlf 33813
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46017
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46019  stoweid 46018
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 45956  stoweidlem10 45965  stoweidlem14 45969  stoweidlem15 45970  stoweidlem35 45990  stoweidlem36 45991  stoweidlem37 45992  stoweidlem38 45993  stoweidlem40 45995  stoweidlem41 45996  stoweidlem43 45998  stoweidlem44 45999  stoweidlem46 46001  stoweidlem5 45960  stoweidlem50 46005  stoweidlem52 46007  stoweidlem53 46008  stoweidlem55 46010  stoweidlem56 46011
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 45978  stoweidlem24 45979  stoweidlem27 45982  stoweidlem28 45983  stoweidlem30 45985
[BrosowskiDeutsh] p. 91Proofstoweidlem34 45989  stoweidlem59 46014  stoweidlem60 46015
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46000  stoweidlem49 46004  stoweidlem7 45962
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 45986  stoweidlem39 45994  stoweidlem42 45997  stoweidlem48 46003  stoweidlem51 46006  stoweidlem54 46009  stoweidlem57 46012  stoweidlem58 46013
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 45980
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 45972
[BrosowskiDeutsh] p. 92Proofstoweidlem11 45966  stoweidlem13 45968  stoweidlem26 45981  stoweidlem61 46016
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 45973
[Bruck] p. 1Section I.1df-clintop 48043  df-mgm 18665  df-mgm2 48062
[Bruck] p. 23Section II.1df-sgrp 18744  df-sgrp2 48064
[Bruck] p. 28Theorem 3.2dfgrp3 19069
[ChoquetDD] p. 2Definition of mappingdf-mpt 5231
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 30431
[Clemente] p. 10Definition I` `m,nnatded 30431
[Clemente] p. 11Definition E=>m,nnatded 30431
[Clemente] p. 11Definition I=>m,nnatded 30431
[Clemente] p. 11Definition E` `(1)natded 30431
[Clemente] p. 11Definition E` `(2)natded 30431
[Clemente] p. 12Definition E` `m,n,pnatded 30431
[Clemente] p. 12Definition I` `n(1)natded 30431
[Clemente] p. 12Definition I` `n(2)natded 30431
[Clemente] p. 13Definition I` `m,n,pnatded 30431
[Clemente] p. 14Proof 5.11natded 30431
[Clemente] p. 14Definition E` `nnatded 30431
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30433  ex-natded5.2 30432
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30436  ex-natded5.3 30435
[Clemente] p. 18Theorem 5.5ex-natded5.5 30438
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30440  ex-natded5.7 30439
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30442  ex-natded5.8 30441
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30444  ex-natded5.13 30443
[Clemente] p. 32Definition I` `nnatded 30431
[Clemente] p. 32Definition E` `m,n,p,anatded 30431
[Clemente] p. 32Definition E` `n,tnatded 30431
[Clemente] p. 32Definition I` `n,tnatded 30431
[Clemente] p. 43Theorem 9.20ex-natded9.20 30445
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30446
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30448  ex-natded9.26 30447
[Cohen] p. 301Remarkrelogoprlem 26647
[Cohen] p. 301Property 2relogmul 26648  relogmuld 26681
[Cohen] p. 301Property 3relogdiv 26649  relogdivd 26682
[Cohen] p. 301Property 4relogexp 26652
[Cohen] p. 301Property 1alog1 26641
[Cohen] p. 301Property 1bloge 26642
[Cohen4] p. 348Observationrelogbcxpb 26844
[Cohen4] p. 349Propertyrelogbf 26848
[Cohen4] p. 352Definitionelogb 26827
[Cohen4] p. 361Property 2relogbmul 26834
[Cohen4] p. 361Property 3logbrec 26839  relogbdiv 26836
[Cohen4] p. 361Property 4relogbreexp 26832
[Cohen4] p. 361Property 6relogbexp 26837
[Cohen4] p. 361Property 1(a)logbid1 26825
[Cohen4] p. 361Property 1(b)logb1 26826
[Cohen4] p. 367Propertylogbchbase 26828
[Cohen4] p. 377Property 2logblt 26841
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34266  sxbrsigalem4 34268
[Cohn] p. 81Section II.5acsdomd 18614  acsinfd 18613  acsinfdimd 18615  acsmap2d 18612  acsmapd 18611
[Cohn] p. 143Example 5.1.1sxbrsiga 34271
[Connell] p. 57Definitiondf-scmat 22512  df-scmatalt 48244
[Conway] p. 4Definitionslerec 27878
[Conway] p. 5Definitionaddsval 28009  addsval2 28010  df-adds 28007  df-muls 28147  df-negs 28067
[Conway] p. 7Theorem0slt1s 27888
[Conway] p. 16Theorem 0(i)ssltright 27924
[Conway] p. 16Theorem 0(ii)ssltleft 27923
[Conway] p. 16Theorem 0(iii)slerflex 27822
[Conway] p. 17Theorem 3addsass 28052  addsassd 28053  addscom 28013  addscomd 28014  addsrid 28011  addsridd 28012
[Conway] p. 17Definitiondf-0s 27883
[Conway] p. 17Theorem 4(ii)negnegs 28090
[Conway] p. 17Theorem 4(iii)negsid 28087  negsidd 28088
[Conway] p. 18Theorem 5sleadd1 28036  sleadd1d 28042
[Conway] p. 18Definitiondf-1s 27884
[Conway] p. 18Theorem 6(ii)negscl 28082  negscld 28083
[Conway] p. 18Theorem 6(iii)addscld 28027
[Conway] p. 19Notemulsunif2 28210
[Conway] p. 19Theorem 7addsdi 28195  addsdid 28196  addsdird 28197  mulnegs1d 28200  mulnegs2d 28201  mulsass 28206  mulsassd 28207  mulscom 28179  mulscomd 28180
[Conway] p. 19Theorem 8(i)mulscl 28174  mulscld 28175
[Conway] p. 19Theorem 8(iii)slemuld 28178  sltmul 28176  sltmuld 28177
[Conway] p. 20Theorem 9mulsgt0 28184  mulsgt0d 28185
[Conway] p. 21Theorem 10(iv)precsex 28256
[Conway] p. 24Definitiondf-reno 28440
[Conway] p. 24Theorem 13(ii)readdscl 28445  remulscl 28448  renegscl 28444
[Conway] p. 27Definitiondf-ons 28289  elons2 28295
[Conway] p. 27Theorem 14sltonex 28298
[Conway] p. 29Remarkmadebday 27952  newbday 27954  oldbday 27953
[Conway] p. 29Definitiondf-made 27900  df-new 27902  df-old 27901
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13897
[Crawley] p. 1Definition of posetdf-poset 18370
[Crawley] p. 107Theorem 13.2hlsupr 39368
[Crawley] p. 110Theorem 13.3arglem1N 40172  dalaw 39868
[Crawley] p. 111Theorem 13.4hlathil 41947
[Crawley] p. 111Definition of set Wdf-watsN 39972
[Crawley] p. 111Definition of dilationdf-dilN 40088  df-ldil 40086  isldil 40092
[Crawley] p. 111Definition of translationdf-ltrn 40087  df-trnN 40089  isltrn 40101  ltrnu 40103
[Crawley] p. 112Lemma Acdlema1N 39773  cdlema2N 39774  exatleN 39386
[Crawley] p. 112Lemma B1cvrat 39458  cdlemb 39776  cdlemb2 40023  cdlemb3 40588  idltrn 40132  l1cvat 39036  lhpat 40025  lhpat2 40027  lshpat 39037  ltrnel 40121  ltrnmw 40133
[Crawley] p. 112Lemma Ccdlemc1 40173  cdlemc2 40174  ltrnnidn 40156  trlat 40151  trljat1 40148  trljat2 40149  trljat3 40150  trlne 40167  trlnidat 40155  trlnle 40168
[Crawley] p. 112Definition of automorphismdf-pautN 39973
[Crawley] p. 113Lemma Ccdlemc 40179  cdlemc3 40175  cdlemc4 40176
[Crawley] p. 113Lemma Dcdlemd 40189  cdlemd1 40180  cdlemd2 40181  cdlemd3 40182  cdlemd4 40183  cdlemd5 40184  cdlemd6 40185  cdlemd7 40186  cdlemd8 40187  cdlemd9 40188  cdleme31sde 40367  cdleme31se 40364  cdleme31se2 40365  cdleme31snd 40368  cdleme32a 40423  cdleme32b 40424  cdleme32c 40425  cdleme32d 40426  cdleme32e 40427  cdleme32f 40428  cdleme32fva 40419  cdleme32fva1 40420  cdleme32fvcl 40422  cdleme32le 40429  cdleme48fv 40481  cdleme4gfv 40489  cdleme50eq 40523  cdleme50f 40524  cdleme50f1 40525  cdleme50f1o 40528  cdleme50laut 40529  cdleme50ldil 40530  cdleme50lebi 40522  cdleme50rn 40527  cdleme50rnlem 40526  cdlemeg49le 40493  cdlemeg49lebilem 40521
[Crawley] p. 113Lemma Ecdleme 40542  cdleme00a 40191  cdleme01N 40203  cdleme02N 40204  cdleme0a 40193  cdleme0aa 40192  cdleme0b 40194  cdleme0c 40195  cdleme0cp 40196  cdleme0cq 40197  cdleme0dN 40198  cdleme0e 40199  cdleme0ex1N 40205  cdleme0ex2N 40206  cdleme0fN 40200  cdleme0gN 40201  cdleme0moN 40207  cdleme1 40209  cdleme10 40236  cdleme10tN 40240  cdleme11 40252  cdleme11a 40242  cdleme11c 40243  cdleme11dN 40244  cdleme11e 40245  cdleme11fN 40246  cdleme11g 40247  cdleme11h 40248  cdleme11j 40249  cdleme11k 40250  cdleme11l 40251  cdleme12 40253  cdleme13 40254  cdleme14 40255  cdleme15 40260  cdleme15a 40256  cdleme15b 40257  cdleme15c 40258  cdleme15d 40259  cdleme16 40267  cdleme16aN 40241  cdleme16b 40261  cdleme16c 40262  cdleme16d 40263  cdleme16e 40264  cdleme16f 40265  cdleme16g 40266  cdleme19a 40285  cdleme19b 40286  cdleme19c 40287  cdleme19d 40288  cdleme19e 40289  cdleme19f 40290  cdleme1b 40208  cdleme2 40210  cdleme20aN 40291  cdleme20bN 40292  cdleme20c 40293  cdleme20d 40294  cdleme20e 40295  cdleme20f 40296  cdleme20g 40297  cdleme20h 40298  cdleme20i 40299  cdleme20j 40300  cdleme20k 40301  cdleme20l 40304  cdleme20l1 40302  cdleme20l2 40303  cdleme20m 40305  cdleme20y 40284  cdleme20zN 40283  cdleme21 40319  cdleme21d 40312  cdleme21e 40313  cdleme22a 40322  cdleme22aa 40321  cdleme22b 40323  cdleme22cN 40324  cdleme22d 40325  cdleme22e 40326  cdleme22eALTN 40327  cdleme22f 40328  cdleme22f2 40329  cdleme22g 40330  cdleme23a 40331  cdleme23b 40332  cdleme23c 40333  cdleme26e 40341  cdleme26eALTN 40343  cdleme26ee 40342  cdleme26f 40345  cdleme26f2 40347  cdleme26f2ALTN 40346  cdleme26fALTN 40344  cdleme27N 40351  cdleme27a 40349  cdleme27cl 40348  cdleme28c 40354  cdleme3 40219  cdleme30a 40360  cdleme31fv 40372  cdleme31fv1 40373  cdleme31fv1s 40374  cdleme31fv2 40375  cdleme31id 40376  cdleme31sc 40366  cdleme31sdnN 40369  cdleme31sn 40362  cdleme31sn1 40363  cdleme31sn1c 40370  cdleme31sn2 40371  cdleme31so 40361  cdleme35a 40430  cdleme35b 40432  cdleme35c 40433  cdleme35d 40434  cdleme35e 40435  cdleme35f 40436  cdleme35fnpq 40431  cdleme35g 40437  cdleme35h 40438  cdleme35h2 40439  cdleme35sn2aw 40440  cdleme35sn3a 40441  cdleme36a 40442  cdleme36m 40443  cdleme37m 40444  cdleme38m 40445  cdleme38n 40446  cdleme39a 40447  cdleme39n 40448  cdleme3b 40211  cdleme3c 40212  cdleme3d 40213  cdleme3e 40214  cdleme3fN 40215  cdleme3fa 40218  cdleme3g 40216  cdleme3h 40217  cdleme4 40220  cdleme40m 40449  cdleme40n 40450  cdleme40v 40451  cdleme40w 40452  cdleme41fva11 40459  cdleme41sn3aw 40456  cdleme41sn4aw 40457  cdleme41snaw 40458  cdleme42a 40453  cdleme42b 40460  cdleme42c 40454  cdleme42d 40455  cdleme42e 40461  cdleme42f 40462  cdleme42g 40463  cdleme42h 40464  cdleme42i 40465  cdleme42k 40466  cdleme42ke 40467  cdleme42keg 40468  cdleme42mN 40469  cdleme42mgN 40470  cdleme43aN 40471  cdleme43bN 40472  cdleme43cN 40473  cdleme43dN 40474  cdleme5 40222  cdleme50ex 40541  cdleme50ltrn 40539  cdleme51finvN 40538  cdleme51finvfvN 40537  cdleme51finvtrN 40540  cdleme6 40223  cdleme7 40231  cdleme7a 40225  cdleme7aa 40224  cdleme7b 40226  cdleme7c 40227  cdleme7d 40228  cdleme7e 40229  cdleme7ga 40230  cdleme8 40232  cdleme8tN 40237  cdleme9 40235  cdleme9a 40233  cdleme9b 40234  cdleme9tN 40239  cdleme9taN 40238  cdlemeda 40280  cdlemedb 40279  cdlemednpq 40281  cdlemednuN 40282  cdlemefr27cl 40385  cdlemefr32fva1 40392  cdlemefr32fvaN 40391  cdlemefrs32fva 40382  cdlemefrs32fva1 40383  cdlemefs27cl 40395  cdlemefs32fva1 40405  cdlemefs32fvaN 40404  cdlemesner 40278  cdlemeulpq 40202
[Crawley] p. 114Lemma E4atex 40058  4atexlem7 40057  cdleme0nex 40272  cdleme17a 40268  cdleme17c 40270  cdleme17d 40480  cdleme17d1 40271  cdleme17d2 40477  cdleme18a 40273  cdleme18b 40274  cdleme18c 40275  cdleme18d 40277  cdleme4a 40221
[Crawley] p. 115Lemma Ecdleme21a 40307  cdleme21at 40310  cdleme21b 40308  cdleme21c 40309  cdleme21ct 40311  cdleme21f 40314  cdleme21g 40315  cdleme21h 40316  cdleme21i 40317  cdleme22gb 40276
[Crawley] p. 116Lemma Fcdlemf 40545  cdlemf1 40543  cdlemf2 40544
[Crawley] p. 116Lemma Gcdlemftr1 40549  cdlemg16 40639  cdlemg28 40686  cdlemg28a 40675  cdlemg28b 40685  cdlemg3a 40579  cdlemg42 40711  cdlemg43 40712  cdlemg44 40715  cdlemg44a 40713  cdlemg46 40717  cdlemg47 40718  cdlemg9 40616  ltrnco 40701  ltrncom 40720  tgrpabl 40733  trlco 40709
[Crawley] p. 116Definition of Gdf-tgrp 40725
[Crawley] p. 117Lemma Gcdlemg17 40659  cdlemg17b 40644
[Crawley] p. 117Definition of Edf-edring-rN 40738  df-edring 40739
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40742
[Crawley] p. 118Remarktendopltp 40762
[Crawley] p. 118Lemma Hcdlemh 40799  cdlemh1 40797  cdlemh2 40798
[Crawley] p. 118Lemma Icdlemi 40802  cdlemi1 40800  cdlemi2 40801
[Crawley] p. 118Lemma Jcdlemj1 40803  cdlemj2 40804  cdlemj3 40805  tendocan 40806
[Crawley] p. 118Lemma Kcdlemk 40956  cdlemk1 40813  cdlemk10 40825  cdlemk11 40831  cdlemk11t 40928  cdlemk11ta 40911  cdlemk11tb 40913  cdlemk11tc 40927  cdlemk11u-2N 40871  cdlemk11u 40853  cdlemk12 40832  cdlemk12u-2N 40872  cdlemk12u 40854  cdlemk13-2N 40858  cdlemk13 40834  cdlemk14-2N 40860  cdlemk14 40836  cdlemk15-2N 40861  cdlemk15 40837  cdlemk16-2N 40862  cdlemk16 40839  cdlemk16a 40838  cdlemk17-2N 40863  cdlemk17 40840  cdlemk18-2N 40868  cdlemk18-3N 40882  cdlemk18 40850  cdlemk19-2N 40869  cdlemk19 40851  cdlemk19u 40952  cdlemk1u 40841  cdlemk2 40814  cdlemk20-2N 40874  cdlemk20 40856  cdlemk21-2N 40873  cdlemk21N 40855  cdlemk22-3 40883  cdlemk22 40875  cdlemk23-3 40884  cdlemk24-3 40885  cdlemk25-3 40886  cdlemk26-3 40888  cdlemk26b-3 40887  cdlemk27-3 40889  cdlemk28-3 40890  cdlemk29-3 40893  cdlemk3 40815  cdlemk30 40876  cdlemk31 40878  cdlemk32 40879  cdlemk33N 40891  cdlemk34 40892  cdlemk35 40894  cdlemk36 40895  cdlemk37 40896  cdlemk38 40897  cdlemk39 40898  cdlemk39u 40950  cdlemk4 40816  cdlemk41 40902  cdlemk42 40923  cdlemk42yN 40926  cdlemk43N 40945  cdlemk45 40929  cdlemk46 40930  cdlemk47 40931  cdlemk48 40932  cdlemk49 40933  cdlemk5 40818  cdlemk50 40934  cdlemk51 40935  cdlemk52 40936  cdlemk53 40939  cdlemk54 40940  cdlemk55 40943  cdlemk55u 40948  cdlemk56 40953  cdlemk5a 40817  cdlemk5auN 40842  cdlemk5u 40843  cdlemk6 40819  cdlemk6u 40844  cdlemk7 40830  cdlemk7u-2N 40870  cdlemk7u 40852  cdlemk8 40820  cdlemk9 40821  cdlemk9bN 40822  cdlemki 40823  cdlemkid 40918  cdlemkj-2N 40864  cdlemkj 40845  cdlemksat 40828  cdlemksel 40827  cdlemksv 40826  cdlemksv2 40829  cdlemkuat 40848  cdlemkuel-2N 40866  cdlemkuel-3 40880  cdlemkuel 40847  cdlemkuv-2N 40865  cdlemkuv2-2 40867  cdlemkuv2-3N 40881  cdlemkuv2 40849  cdlemkuvN 40846  cdlemkvcl 40824  cdlemky 40908  cdlemkyyN 40944  tendoex 40957
[Crawley] p. 120Remarkdva1dim 40967
[Crawley] p. 120Lemma Lcdleml1N 40958  cdleml2N 40959  cdleml3N 40960  cdleml4N 40961  cdleml5N 40962  cdleml6 40963  cdleml7 40964  cdleml8 40965  cdleml9 40966  dia1dim 41043
[Crawley] p. 120Lemma Mdia11N 41030  diaf11N 41031  dialss 41028  diaord 41029  dibf11N 41143  djajN 41119
[Crawley] p. 120Definition of isomorphism mapdiaval 41014
[Crawley] p. 121Lemma Mcdlemm10N 41100  dia2dimlem1 41046  dia2dimlem2 41047  dia2dimlem3 41048  dia2dimlem4 41049  dia2dimlem5 41050  diaf1oN 41112  diarnN 41111  dvheveccl 41094  dvhopN 41098
[Crawley] p. 121Lemma Ncdlemn 41194  cdlemn10 41188  cdlemn11 41193  cdlemn11a 41189  cdlemn11b 41190  cdlemn11c 41191  cdlemn11pre 41192  cdlemn2 41177  cdlemn2a 41178  cdlemn3 41179  cdlemn4 41180  cdlemn4a 41181  cdlemn5 41183  cdlemn5pre 41182  cdlemn6 41184  cdlemn7 41185  cdlemn8 41186  cdlemn9 41187  diclspsn 41176
[Crawley] p. 121Definition of phi(q)df-dic 41155
[Crawley] p. 122Lemma Ndih11 41247  dihf11 41249  dihjust 41199  dihjustlem 41198  dihord 41246  dihord1 41200  dihord10 41205  dihord11b 41204  dihord11c 41206  dihord2 41209  dihord2a 41201  dihord2b 41202  dihord2cN 41203  dihord2pre 41207  dihord2pre2 41208  dihordlem6 41195  dihordlem7 41196  dihordlem7b 41197
[Crawley] p. 122Definition of isomorphism mapdihffval 41212  dihfval 41213  dihval 41214
[Diestel] p. 3Definitiondf-gric 47804  df-grim 47801  isuspgrim 47812
[Diestel] p. 3Section 1.1df-cusgr 29443  df-nbgr 29364
[Diestel] p. 3Definition by df-grisom 47800
[Diestel] p. 4Section 1.1df-isubgr 47784  df-subgr 29299  uhgrspan1 29334  uhgrspansubgr 29322
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29586  vtxdgoddnumeven 29585
[Diestel] p. 27Section 1.10df-ushgr 29090
[EGA] p. 80Notation 1.1.1rspecval 33824
[EGA] p. 80Proposition 1.1.2zartop 33836
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33828  zarcls1 33829
[EGA] p. 81Corollary 1.1.8zart0 33839
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33842
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33845
[Eisenberg] p. 67Definition 5.3df-dif 3965
[Eisenberg] p. 82Definition 6.3dfom3 9684
[Eisenberg] p. 125Definition 8.21df-map 8866
[Eisenberg] p. 216Example 13.2(4)omenps 9692
[Eisenberg] p. 310Theorem 19.8cardprc 10017
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10592
[Enderton] p. 18Axiom of Empty Setaxnul 5310
[Enderton] p. 19Definitiondf-tp 4635
[Enderton] p. 26Exercise 5unissb 4943
[Enderton] p. 26Exercise 10pwel 5386
[Enderton] p. 28Exercise 7(b)pwun 5580
[Enderton] p. 30Theorem "Distributive laws"iinin1 5083  iinin2 5082  iinun2 5077  iunin1 5076  iunin1f 32577  iunin2 5075  uniin1 32571  uniin2 32572
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5081  iundif2 5078
[Enderton] p. 32Exercise 20unineq 4293
[Enderton] p. 33Exercise 23iinuni 5102
[Enderton] p. 33Exercise 25iununi 5103
[Enderton] p. 33Exercise 24(a)iinpw 5110
[Enderton] p. 33Exercise 24(b)iunpw 7789  iunpwss 5111
[Enderton] p. 36Definitionopthwiener 5523
[Enderton] p. 38Exercise 6(a)unipw 5460
[Enderton] p. 38Exercise 6(b)pwuni 4949
[Enderton] p. 41Lemma 3Dopeluu 5480  rnex 7932  rnexg 7924
[Enderton] p. 41Exercise 8dmuni 5927  rnuni 6170
[Enderton] p. 42Definition of a functiondffun7 6594  dffun8 6595
[Enderton] p. 43Definition of function valuefunfv2 6996
[Enderton] p. 43Definition of single-rootedfuncnv 6636
[Enderton] p. 44Definition (d)dfima2 6081  dfima3 6082
[Enderton] p. 47Theorem 3Hfvco2 7005
[Enderton] p. 49Axiom of Choice (first form)ac7 10510  ac7g 10511  df-ac 10153  dfac2 10169  dfac2a 10167  dfac2b 10168  dfac3 10158  dfac7 10170
[Enderton] p. 50Theorem 3K(a)imauni 7265
[Enderton] p. 52Definitiondf-map 8866
[Enderton] p. 53Exercise 21coass 6286
[Enderton] p. 53Exercise 27dmco 6275
[Enderton] p. 53Exercise 14(a)funin 6643
[Enderton] p. 53Exercise 22(a)imass2 6122
[Enderton] p. 54Remarkixpf 8958  ixpssmap 8970
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8936
[Enderton] p. 55Axiom of Choice (second form)ac9 10520  ac9s 10530
[Enderton] p. 56Theorem 3Meqvrelref 38591  erref 8763
[Enderton] p. 57Lemma 3Neqvrelthi 38594  erthi 8796
[Enderton] p. 57Definitiondf-ec 8745
[Enderton] p. 58Definitiondf-qs 8749
[Enderton] p. 61Exercise 35df-ec 8745
[Enderton] p. 65Exercise 56(a)dmun 5923
[Enderton] p. 68Definition of successordf-suc 6391
[Enderton] p. 71Definitiondf-tr 5265  dftr4 5271
[Enderton] p. 72Theorem 4Eunisuc 6464  unisucg 6463
[Enderton] p. 73Exercise 6unisuc 6464  unisucg 6463
[Enderton] p. 73Exercise 5(a)truni 5280
[Enderton] p. 73Exercise 5(b)trint 5282  trintALT 44878
[Enderton] p. 79Theorem 4I(A1)nna0 8640
[Enderton] p. 79Theorem 4I(A2)nnasuc 8642  onasuc 8564
[Enderton] p. 79Definition of operation valuedf-ov 7433
[Enderton] p. 80Theorem 4J(A1)nnm0 8641
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8643  onmsuc 8565
[Enderton] p. 81Theorem 4K(1)nnaass 8658
[Enderton] p. 81Theorem 4K(2)nna0r 8645  nnacom 8653
[Enderton] p. 81Theorem 4K(3)nndi 8659
[Enderton] p. 81Theorem 4K(4)nnmass 8660
[Enderton] p. 81Theorem 4K(5)nnmcom 8662
[Enderton] p. 82Exercise 16nnm0r 8646  nnmsucr 8661
[Enderton] p. 88Exercise 23nnaordex 8674
[Enderton] p. 129Definitiondf-en 8984
[Enderton] p. 132Theorem 6B(b)canth 7384
[Enderton] p. 133Exercise 1xpomen 10052
[Enderton] p. 133Exercise 2qnnen 16245
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9244
[Enderton] p. 135Corollary 6Cphp3 9246
[Enderton] p. 136Corollary 6Enneneq 9243
[Enderton] p. 136Corollary 6D(a)pssinf 9289
[Enderton] p. 136Corollary 6D(b)ominf 9291
[Enderton] p. 137Lemma 6Fpssnn 9206
[Enderton] p. 138Corollary 6Gssfi 9211
[Enderton] p. 139Theorem 6H(c)mapen 9179
[Enderton] p. 142Theorem 6I(3)xpdjuen 10217
[Enderton] p. 142Theorem 6I(4)mapdjuen 10218
[Enderton] p. 143Theorem 6Jdju0en 10213  dju1en 10209
[Enderton] p. 144Exercise 13iunfi 9380  unifi 9381  unifi2 9382
[Enderton] p. 144Corollary 6Kundif2 4482  unfi 9209  unfi2 9345
[Enderton] p. 145Figure 38ffoss 7968
[Enderton] p. 145Definitiondf-dom 8985
[Enderton] p. 146Example 1domen 9000  domeng 9001
[Enderton] p. 146Example 3nndomo 9266  nnsdom 9691  nnsdomg 9332
[Enderton] p. 149Theorem 6L(a)djudom2 10221
[Enderton] p. 149Theorem 6L(c)mapdom1 9180  xpdom1 9109  xpdom1g 9107  xpdom2g 9106
[Enderton] p. 149Theorem 6L(d)mapdom2 9186
[Enderton] p. 151Theorem 6Mzorn 10544  zorng 10541
[Enderton] p. 151Theorem 6M(4)ac8 10529  dfac5 10166
[Enderton] p. 159Theorem 6Qunictb 10612
[Enderton] p. 164Exampleinfdif 10245
[Enderton] p. 168Definitiondf-po 5596
[Enderton] p. 192Theorem 7M(a)oneli 6499
[Enderton] p. 192Theorem 7M(b)ontr1 6431
[Enderton] p. 192Theorem 7M(c)onirri 6498
[Enderton] p. 193Corollary 7N(b)0elon 6439
[Enderton] p. 193Corollary 7N(c)onsuci 7858
[Enderton] p. 193Corollary 7N(d)ssonunii 7799
[Enderton] p. 194Remarkonprc 7796
[Enderton] p. 194Exercise 16suc11 6492
[Enderton] p. 197Definitiondf-card 9976
[Enderton] p. 197Theorem 7Pcarden 10588
[Enderton] p. 200Exercise 25tfis 7875
[Enderton] p. 202Lemma 7Tr1tr 9813
[Enderton] p. 202Definitiondf-r1 9801
[Enderton] p. 202Theorem 7Qr1val1 9823
[Enderton] p. 204Theorem 7V(b)rankval4 9904
[Enderton] p. 206Theorem 7X(b)en2lp 9643
[Enderton] p. 207Exercise 30rankpr 9894  rankprb 9888  rankpw 9880  rankpwi 9860  rankuniss 9903
[Enderton] p. 207Exercise 34opthreg 9655
[Enderton] p. 208Exercise 35suc11reg 9656
[Enderton] p. 212Definition of alephalephval3 10147
[Enderton] p. 213Theorem 8A(a)alephord2 10113
[Enderton] p. 213Theorem 8A(b)cardalephex 10127
[Enderton] p. 218Theorem Schema 8Eonfununi 8379
[Enderton] p. 222Definition of kardkarden 9932  kardex 9931
[Enderton] p. 238Theorem 8Roeoa 8633
[Enderton] p. 238Theorem 8Soeoe 8635
[Enderton] p. 240Exercise 25oarec 8598
[Enderton] p. 257Definition of cofinalitycflm 10287
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17686
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17632
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18610  mrieqv2d 17683  mrieqvd 17682
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17687
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17692  mreexexlem2d 17689
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18616  mreexfidimd 17694
[Frege1879] p. 11Statementdf3or2 43757
[Frege1879] p. 12Statementdf3an2 43758  dfxor4 43755  dfxor5 43756
[Frege1879] p. 26Axiom 1ax-frege1 43779
[Frege1879] p. 26Axiom 2ax-frege2 43780
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43784
[Frege1879] p. 31Proposition 4frege4 43788
[Frege1879] p. 32Proposition 5frege5 43789
[Frege1879] p. 33Proposition 6frege6 43795
[Frege1879] p. 34Proposition 7frege7 43797
[Frege1879] p. 35Axiom 8ax-frege8 43798  axfrege8 43796
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37427
[Frege1879] p. 35Proposition 9frege9 43801
[Frege1879] p. 36Proposition 10frege10 43809
[Frege1879] p. 36Proposition 11frege11 43803
[Frege1879] p. 37Proposition 12frege12 43802
[Frege1879] p. 37Proposition 13frege13 43811
[Frege1879] p. 37Proposition 14frege14 43812
[Frege1879] p. 38Proposition 15frege15 43815
[Frege1879] p. 38Proposition 16frege16 43805
[Frege1879] p. 39Proposition 17frege17 43810
[Frege1879] p. 39Proposition 18frege18 43807
[Frege1879] p. 39Proposition 19frege19 43813
[Frege1879] p. 40Proposition 20frege20 43817
[Frege1879] p. 40Proposition 21frege21 43816
[Frege1879] p. 41Proposition 22frege22 43808
[Frege1879] p. 42Proposition 23frege23 43814
[Frege1879] p. 42Proposition 24frege24 43804
[Frege1879] p. 42Proposition 25frege25 43806  rp-frege25 43794
[Frege1879] p. 42Proposition 26frege26 43799
[Frege1879] p. 43Axiom 28ax-frege28 43819
[Frege1879] p. 43Proposition 27frege27 43800
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43820
[Frege1879] p. 44Axiom 31ax-frege31 43823  axfrege31 43822
[Frege1879] p. 44Proposition 30frege30 43821
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43824
[Frege1879] p. 44Proposition 33frege33 43825
[Frege1879] p. 45Proposition 34frege34 43826
[Frege1879] p. 45Proposition 35frege35 43827
[Frege1879] p. 45Proposition 36frege36 43828
[Frege1879] p. 46Proposition 37frege37 43829
[Frege1879] p. 46Proposition 38frege38 43830
[Frege1879] p. 46Proposition 39frege39 43831
[Frege1879] p. 46Proposition 40frege40 43832
[Frege1879] p. 47Axiom 41ax-frege41 43834  axfrege41 43833
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43835
[Frege1879] p. 47Proposition 43frege43 43836
[Frege1879] p. 47Proposition 44frege44 43837
[Frege1879] p. 47Proposition 45frege45 43838
[Frege1879] p. 48Proposition 46frege46 43839
[Frege1879] p. 48Proposition 47frege47 43840
[Frege1879] p. 49Proposition 48frege48 43841
[Frege1879] p. 49Proposition 49frege49 43842
[Frege1879] p. 49Proposition 50frege50 43843
[Frege1879] p. 50Axiom 52ax-frege52a 43846  ax-frege52c 43877  frege52aid 43847  frege52b 43878
[Frege1879] p. 50Axiom 54ax-frege54a 43851  ax-frege54c 43881  frege54b 43882
[Frege1879] p. 50Proposition 51frege51 43844
[Frege1879] p. 50Proposition 52dfsbcq 3792
[Frege1879] p. 50Proposition 53frege53a 43849  frege53aid 43848  frege53b 43879  frege53c 43903
[Frege1879] p. 50Proposition 54biid 261  eqid 2734
[Frege1879] p. 50Proposition 55frege55a 43857  frege55aid 43854  frege55b 43886  frege55c 43907  frege55cor1a 43858  frege55lem2a 43856  frege55lem2b 43885  frege55lem2c 43906
[Frege1879] p. 50Proposition 56frege56a 43860  frege56aid 43859  frege56b 43887  frege56c 43908
[Frege1879] p. 51Axiom 58ax-frege58a 43864  ax-frege58b 43890  frege58bid 43891  frege58c 43910
[Frege1879] p. 51Proposition 57frege57a 43862  frege57aid 43861  frege57b 43888  frege57c 43909
[Frege1879] p. 51Proposition 58spsbc 3803
[Frege1879] p. 51Proposition 59frege59a 43866  frege59b 43893  frege59c 43911
[Frege1879] p. 52Proposition 60frege60a 43867  frege60b 43894  frege60c 43912
[Frege1879] p. 52Proposition 61frege61a 43868  frege61b 43895  frege61c 43913
[Frege1879] p. 52Proposition 62frege62a 43869  frege62b 43896  frege62c 43914
[Frege1879] p. 52Proposition 63frege63a 43870  frege63b 43897  frege63c 43915
[Frege1879] p. 53Proposition 64frege64a 43871  frege64b 43898  frege64c 43916
[Frege1879] p. 53Proposition 65frege65a 43872  frege65b 43899  frege65c 43917
[Frege1879] p. 54Proposition 66frege66a 43873  frege66b 43900  frege66c 43918
[Frege1879] p. 54Proposition 67frege67a 43874  frege67b 43901  frege67c 43919
[Frege1879] p. 54Proposition 68frege68a 43875  frege68b 43902  frege68c 43920
[Frege1879] p. 55Definition 69dffrege69 43921
[Frege1879] p. 58Proposition 70frege70 43922
[Frege1879] p. 59Proposition 71frege71 43923
[Frege1879] p. 59Proposition 72frege72 43924
[Frege1879] p. 59Proposition 73frege73 43925
[Frege1879] p. 60Definition 76dffrege76 43928
[Frege1879] p. 60Proposition 74frege74 43926
[Frege1879] p. 60Proposition 75frege75 43927
[Frege1879] p. 62Proposition 77frege77 43929  frege77d 43735
[Frege1879] p. 63Proposition 78frege78 43930
[Frege1879] p. 63Proposition 79frege79 43931
[Frege1879] p. 63Proposition 80frege80 43932
[Frege1879] p. 63Proposition 81frege81 43933  frege81d 43736
[Frege1879] p. 64Proposition 82frege82 43934
[Frege1879] p. 65Proposition 83frege83 43935  frege83d 43737
[Frege1879] p. 65Proposition 84frege84 43936
[Frege1879] p. 66Proposition 85frege85 43937
[Frege1879] p. 66Proposition 86frege86 43938
[Frege1879] p. 66Proposition 87frege87 43939  frege87d 43739
[Frege1879] p. 67Proposition 88frege88 43940
[Frege1879] p. 68Proposition 89frege89 43941
[Frege1879] p. 68Proposition 90frege90 43942
[Frege1879] p. 68Proposition 91frege91 43943  frege91d 43740
[Frege1879] p. 69Proposition 92frege92 43944
[Frege1879] p. 70Proposition 93frege93 43945
[Frege1879] p. 70Proposition 94frege94 43946
[Frege1879] p. 70Proposition 95frege95 43947
[Frege1879] p. 71Definition 99dffrege99 43951
[Frege1879] p. 71Proposition 96frege96 43948  frege96d 43738
[Frege1879] p. 71Proposition 97frege97 43949  frege97d 43741
[Frege1879] p. 71Proposition 98frege98 43950  frege98d 43742
[Frege1879] p. 72Proposition 100frege100 43952
[Frege1879] p. 72Proposition 101frege101 43953
[Frege1879] p. 72Proposition 102frege102 43954  frege102d 43743
[Frege1879] p. 73Proposition 103frege103 43955
[Frege1879] p. 73Proposition 104frege104 43956
[Frege1879] p. 73Proposition 105frege105 43957
[Frege1879] p. 73Proposition 106frege106 43958  frege106d 43744
[Frege1879] p. 74Proposition 107frege107 43959
[Frege1879] p. 74Proposition 108frege108 43960  frege108d 43745
[Frege1879] p. 74Proposition 109frege109 43961  frege109d 43746
[Frege1879] p. 75Proposition 110frege110 43962
[Frege1879] p. 75Proposition 111frege111 43963  frege111d 43748
[Frege1879] p. 76Proposition 112frege112 43964
[Frege1879] p. 76Proposition 113frege113 43965
[Frege1879] p. 76Proposition 114frege114 43966  frege114d 43747
[Frege1879] p. 77Definition 115dffrege115 43967
[Frege1879] p. 77Proposition 116frege116 43968
[Frege1879] p. 78Proposition 117frege117 43969
[Frege1879] p. 78Proposition 118frege118 43970
[Frege1879] p. 78Proposition 119frege119 43971
[Frege1879] p. 78Proposition 120frege120 43972
[Frege1879] p. 79Proposition 121frege121 43973
[Frege1879] p. 79Proposition 122frege122 43974  frege122d 43749
[Frege1879] p. 79Proposition 123frege123 43975
[Frege1879] p. 80Proposition 124frege124 43976  frege124d 43750
[Frege1879] p. 81Proposition 125frege125 43977
[Frege1879] p. 81Proposition 126frege126 43978  frege126d 43751
[Frege1879] p. 82Proposition 127frege127 43979
[Frege1879] p. 83Proposition 128frege128 43980
[Frege1879] p. 83Proposition 129frege129 43981  frege129d 43752
[Frege1879] p. 84Proposition 130frege130 43982
[Frege1879] p. 85Proposition 131frege131 43983  frege131d 43753
[Frege1879] p. 86Proposition 132frege132 43984
[Frege1879] p. 86Proposition 133frege133 43985  frege133d 43754
[Fremlin1] p. 13Definition 111G (b)df-salgen 46268
[Fremlin1] p. 13Definition 111G (d)borelmbl 46591
[Fremlin1] p. 13Proposition 111G (b)salgenss 46291
[Fremlin1] p. 14Definition 112Aismea 46406
[Fremlin1] p. 15Remark 112B (d)psmeasure 46426
[Fremlin1] p. 15Property 112C (a)meadjun 46417  meadjunre 46431
[Fremlin1] p. 15Property 112C (b)meassle 46418
[Fremlin1] p. 15Property 112C (c)meaunle 46419
[Fremlin1] p. 16Property 112C (d)iundjiun 46415  meaiunle 46424  meaiunlelem 46423
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46436  meaiuninc2 46437  meaiuninc3 46440  meaiuninc3v 46439  meaiunincf 46438  meaiuninclem 46435
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46442  meaiininc2 46443  meaiininclem 46441
[Fremlin1] p. 19Theorem 113Ccaragen0 46461  caragendifcl 46469  caratheodory 46483  omelesplit 46473
[Fremlin1] p. 19Definition 113Aisome 46449  isomennd 46486  isomenndlem 46485
[Fremlin1] p. 19Remark 113B (c)omeunle 46471
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46490  voncmpl 46576
[Fremlin1] p. 19Definition 113A (ii)omessle 46453
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46478  carageniuncllem1 46476  carageniuncllem2 46477  caragenuncl 46468  caragenuncllem 46467  caragenunicl 46479
[Fremlin1] p. 21Remark 113Dcaragenel2d 46487
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46481  caratheodorylem2 46482
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46490
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46549  hoidmv1lelem1 46546  hoidmv1lelem2 46547  hoidmv1lelem3 46548
[Fremlin1] p. 25Definition 114Eisvonmbl 46593
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46549  hoidmvle 46555  hoidmvlelem1 46550  hoidmvlelem2 46551  hoidmvlelem3 46552  hoidmvlelem4 46553  hoidmvlelem5 46554  hsphoidmvle2 46540  hsphoif 46531  hsphoival 46534
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46503
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46511
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46538  hoidmvn0val 46539  hoidmvval 46532  hoidmvval0 46542  hoidmvval0b 46545
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46543  hsphoidmvle 46541
[Fremlin1] p. 30Definition 115Cdf-ovoln 46492  df-voln 46494
[Fremlin1] p. 30Proposition 115D (a)dmovn 46559  ovn0 46521  ovn0lem 46520  ovnf 46518  ovnome 46528  ovnssle 46516  ovnsslelem 46515  ovnsupge0 46512
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46558  ovnhoilem1 46556  ovnhoilem2 46557  vonhoi 46622
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46575  hoidifhspf 46573  hoidifhspval 46563  hoidifhspval2 46570  hoidifhspval3 46574  hspmbl 46584  hspmbllem1 46581  hspmbllem2 46582  hspmbllem3 46583
[Fremlin1] p. 31Definition 115Evoncmpl 46576  vonmea 46529
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46527  ovnsubadd2 46601  ovnsubadd2lem 46600  ovnsubaddlem1 46525  ovnsubaddlem2 46526
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46586  hoimbl2 46620  hoimbllem 46585  hspdifhsp 46571  opnvonmbl 46589  opnvonmbllem2 46588
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46591
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46634  iccvonmbllem 46633  ioovonmbl 46632
[Fremlin1] p. 32Proposition 115G (d)vonicc 46640  vonicclem2 46639  vonioo 46637  vonioolem2 46636  vonn0icc 46643  vonn0icc2 46647  vonn0ioo 46642  vonn0ioo2 46645
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46644  snvonmbl 46641  vonct 46648  vonsn 46646
[Fremlin1] p. 35Lemma 121Asubsalsal 46314
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46313  subsaliuncllem 46312
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46680  salpreimalegt 46664  salpreimaltle 46681
[Fremlin1] p. 35Proposition 121B (i)issmf 46683  issmff 46689  issmflem 46682
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46700  issmflelem 46699  smfpreimale 46709
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46711  issmfgtlem 46710
[Fremlin1] p. 36Definition 121Cdf-smblfn 46651  issmf 46683  issmff 46689  issmfge 46725  issmfgelem 46724  issmfgt 46711  issmfgtlem 46710  issmfle 46700  issmflelem 46699  issmflem 46682
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46662  salpreimagtlt 46685  salpreimalelt 46684
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46725  issmfgelem 46724
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46708
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46706  cnfsmf 46695
[Fremlin1] p. 36Proposition 121D (c)decsmf 46722  decsmflem 46721  incsmf 46697  incsmflem 46696
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46656  pimconstlt1 46657  smfconst 46704
[Fremlin1] p. 37Proposition 121E (b)smfadd 46720  smfaddlem1 46718  smfaddlem2 46719
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46751
[Fremlin1] p. 37Proposition 121E (d)smfmul 46750  smfmullem1 46746  smfmullem2 46747  smfmullem3 46748  smfmullem4 46749
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46752
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46755  smfpimbor1lem2 46754
[Fremlin1] p. 37Proposition 121E (g)smfco 46757
[Fremlin1] p. 37Proposition 121E (h)smfres 46745
[Fremlin1] p. 38Proposition 121E (e)smfrec 46744
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46753  smfresal 46743
[Fremlin1] p. 38Proposition 121F (a)smflim 46732  smflim2 46761  smflimlem1 46726  smflimlem2 46727  smflimlem3 46728  smflimlem4 46729  smflimlem5 46730  smflimlem6 46731  smflimmpt 46765
[Fremlin1] p. 38Proposition 121F (b)smfsup 46769  smfsuplem1 46766  smfsuplem2 46767  smfsuplem3 46768  smfsupmpt 46770  smfsupxr 46771
[Fremlin1] p. 38Proposition 121F (c)smfinf 46773  smfinflem 46772  smfinfmpt 46774
[Fremlin1] p. 39Remark 121Gsmflim 46732  smflim2 46761  smflimmpt 46765
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46763
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46793  smfdivdmmbl2 46796  smfinfdmmbl 46804  smfinfdmmbllem 46803  smfsupdmmbl 46800  smfsupdmmbllem 46799
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46783  smflimsuplem2 46776  smflimsuplem6 46780  smflimsuplem7 46781  smflimsuplem8 46782  smflimsupmpt 46784
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46786  smfliminflem 46785  smfliminfmpt 46787
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46651
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46797  fsupdm2 46798
[Fremlin1], p. 39Proposition 121Hadddmmbl 46788  adddmmbl2 46789  finfdm 46801  finfdm2 46802  fsupdm 46797  fsupdm2 46798  muldmmbl 46790  muldmmbl2 46791
[Fremlin1], p. 39Proposition 121F (c)finfdm 46801  finfdm2 46802
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25584
[Fremlin5] p. 213Lemma 565Cauniioovol 25627
[Fremlin5] p. 214Lemma 565Cauniioombl 25637
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37684
[Fremlin5] p. 220Theorem 565Maftc1anc 37687
[FreydScedrov] p. 283Axiom of Infinityax-inf 9675  inf1 9659  inf2 9660
[Gleason] p. 117Proposition 9-2.1df-enq 10948  enqer 10958
[Gleason] p. 117Proposition 9-2.2df-1nq 10953  df-nq 10949
[Gleason] p. 117Proposition 9-2.3df-plpq 10945  df-plq 10951
[Gleason] p. 119Proposition 9-2.4caovmo 7669  df-mpq 10946  df-mq 10952
[Gleason] p. 119Proposition 9-2.5df-rq 10954
[Gleason] p. 119Proposition 9-2.6ltexnq 11012
[Gleason] p. 120Proposition 9-2.6(i)halfnq 11013  ltbtwnnq 11015
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 11008
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 11009
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 11016
[Gleason] p. 121Definition 9-3.1df-np 11018
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 11030
[Gleason] p. 121Definition 9-3.1(iii)prnmax 11032
[Gleason] p. 122Definitiondf-1p 11019
[Gleason] p. 122Remark (1)prub 11031
[Gleason] p. 122Lemma 9-3.4prlem934 11070
[Gleason] p. 122Proposition 9-3.2df-ltp 11022
[Gleason] p. 122Proposition 9-3.3ltsopr 11069  psslinpr 11068  supexpr 11091  suplem1pr 11089  suplem2pr 11090
[Gleason] p. 123Proposition 9-3.5addclpr 11055  addclprlem1 11053  addclprlem2 11054  df-plp 11020
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11059
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11058
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11071
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11080  ltexprlem1 11073  ltexprlem2 11074  ltexprlem3 11075  ltexprlem4 11076  ltexprlem5 11077  ltexprlem6 11078  ltexprlem7 11079
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11082  ltaprlem 11081
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11083
[Gleason] p. 124Lemma 9-3.6prlem936 11084
[Gleason] p. 124Proposition 9-3.7df-mp 11021  mulclpr 11057  mulclprlem 11056  reclem2pr 11085
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11066
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11061
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11060
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11065
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11088  reclem3pr 11086  reclem4pr 11087
[Gleason] p. 126Proposition 9-4.1df-enr 11092  enrer 11100
[Gleason] p. 126Proposition 9-4.2df-0r 11097  df-1r 11098  df-nr 11093
[Gleason] p. 126Proposition 9-4.3df-mr 11095  df-plr 11094  negexsr 11139  recexsr 11144  recexsrlem 11140
[Gleason] p. 127Proposition 9-4.4df-ltr 11096
[Gleason] p. 130Proposition 10-1.3creui 12258  creur 12257  cru 12255
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11225  axcnre 11201
[Gleason] p. 132Definition 10-3.1crim 15150  crimd 15267  crimi 15228  crre 15149  crred 15266  crrei 15227
[Gleason] p. 132Definition 10-3.2remim 15152  remimd 15233
[Gleason] p. 133Definition 10.36absval2 15319  absval2d 15480  absval2i 15432
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15176  cjaddd 15255  cjaddi 15223
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15177  cjmuld 15256  cjmuli 15224
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15175  cjcjd 15234  cjcji 15206
[Gleason] p. 133Proposition 10-3.4(f)cjre 15174  cjreb 15158  cjrebd 15237  cjrebi 15209  cjred 15261  rere 15157  rereb 15155  rerebd 15236  rerebi 15208  rered 15259
[Gleason] p. 133Proposition 10-3.4(h)addcj 15183  addcjd 15247  addcji 15218
[Gleason] p. 133Proposition 10-3.7(a)absval 15273
[Gleason] p. 133Proposition 10-3.7(b)abscj 15314  abscjd 15485  abscji 15436
[Gleason] p. 133Proposition 10-3.7(c)abs00 15324  abs00d 15481  abs00i 15433  absne0d 15482
[Gleason] p. 133Proposition 10-3.7(d)releabs 15356  releabsd 15486  releabsi 15437
[Gleason] p. 133Proposition 10-3.7(f)absmul 15329  absmuld 15489  absmuli 15439
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15317  sqabsaddi 15440
[Gleason] p. 133Proposition 10-3.7(h)abstri 15365  abstrid 15491  abstrii 15443
[Gleason] p. 134Definition 10-4.1df-exp 14099  exp0 14102  expp1 14105  expp1d 14183
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26735  cxpaddd 26773  expadd 14141  expaddd 14184  expaddz 14143
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26744  cxpmuld 26793  expmul 14144  expmuld 14185  expmulz 14145
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26741  mulcxpd 26784  mulexp 14138  mulexpd 14197  mulexpz 14139
[Gleason] p. 140Exercise 1znnen 16244
[Gleason] p. 141Definition 11-2.1fzval 13545
[Gleason] p. 168Proposition 12-2.1(a)climadd 15664  rlimadd 15675  rlimdiv 15678
[Gleason] p. 168Proposition 12-2.1(b)climsub 15666  rlimsub 15676
[Gleason] p. 168Proposition 12-2.1(c)climmul 15665  rlimmul 15677
[Gleason] p. 171Corollary 12-2.2climmulc2 15669
[Gleason] p. 172Corollary 12-2.5climrecl 15615
[Gleason] p. 172Proposition 12-2.4(c)climabs 15636  climcj 15637  climim 15639  climre 15638  rlimabs 15641  rlimcj 15642  rlimim 15644  rlimre 15643
[Gleason] p. 173Definition 12-3.1df-ltxr 11297  df-xr 11296  ltxr 13154
[Gleason] p. 175Definition 12-4.1df-limsup 15503  limsupval 15506
[Gleason] p. 180Theorem 12-5.1climsup 15702
[Gleason] p. 180Theorem 12-5.3caucvg 15711  caucvgb 15712  caucvgbf 45439  caucvgr 15708  climcau 15703
[Gleason] p. 182Exercise 3cvgcmp 15848
[Gleason] p. 182Exercise 4cvgrat 15915
[Gleason] p. 195Theorem 13-2.12abs1m 15370
[Gleason] p. 217Lemma 13-4.1btwnzge0 13864
[Gleason] p. 223Definition 14-1.1df-met 21375
[Gleason] p. 223Definition 14-1.1(a)met0 24368  xmet0 24367
[Gleason] p. 223Definition 14-1.1(b)metgt0 24384
[Gleason] p. 223Definition 14-1.1(c)metsym 24375
[Gleason] p. 223Definition 14-1.1(d)mettri 24377  mstri 24494  xmettri 24376  xmstri 24493
[Gleason] p. 225Definition 14-1.5xpsmet 24407
[Gleason] p. 230Proposition 14-2.6txlm 23671
[Gleason] p. 240Theorem 14-4.3metcnp4 25357
[Gleason] p. 240Proposition 14-4.2metcnp3 24568
[Gleason] p. 243Proposition 14-4.16addcn 24900  addcn2 15626  mulcn 24902  mulcn2 15628  subcn 24901  subcn2 15627
[Gleason] p. 295Remarkbcval3 14341  bcval4 14342
[Gleason] p. 295Equation 2bcpasc 14356
[Gleason] p. 295Definition of binomial coefficientbcval 14339  df-bc 14338
[Gleason] p. 296Remarkbcn0 14345  bcnn 14347
[Gleason] p. 296Theorem 15-2.8binom 15862
[Gleason] p. 308Equation 2ef0 16123
[Gleason] p. 308Equation 3efcj 16124
[Gleason] p. 309Corollary 15-4.3efne0 16129
[Gleason] p. 309Corollary 15-4.4efexp 16133
[Gleason] p. 310Equation 14sinadd 16196
[Gleason] p. 310Equation 15cosadd 16197
[Gleason] p. 311Equation 17sincossq 16208
[Gleason] p. 311Equation 18cosbnd 16213  sinbnd 16212
[Gleason] p. 311Lemma 15-4.7sqeqor 14251  sqeqori 14249
[Gleason] p. 311Definition of ` `df-pi 16104
[Godowski] p. 730Equation SFgoeqi 32301
[GodowskiGreechie] p. 249Equation IV3oai 31696
[Golan] p. 1Remarksrgisid 20226
[Golan] p. 1Definitiondf-srg 20204
[Golan] p. 149Definitiondf-slmd 33189
[Gonshor] p. 7Definitiondf-scut 27842
[Gonshor] p. 9Theorem 2.5slerec 27878
[Gonshor] p. 10Theorem 2.6cofcut1 27968  cofcut1d 27969
[Gonshor] p. 10Theorem 2.7cofcut2 27970  cofcut2d 27971
[Gonshor] p. 12Theorem 2.9cofcutr 27972  cofcutr1d 27973  cofcutr2d 27974
[Gonshor] p. 13Definitiondf-adds 28007
[Gonshor] p. 14Theorem 3.1addsprop 28023
[Gonshor] p. 15Theorem 3.2addsunif 28049
[Gonshor] p. 17Theorem 3.4mulsprop 28170
[Gonshor] p. 18Theorem 3.5mulsunif 28190
[Gonshor] p. 28Lemma 4.2halfcut 28430
[Gonshor] p. 28Theorem 4.2pw2cut 28434
[Gonshor] p. 30Theorem 4.2addhalfcut 28433
[Gonshor] p. 95Theorem 6.1addsbday 28064
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36140
[Gratzer] p. 23Section 0.6df-mre 17630
[Gratzer] p. 27Section 0.6df-mri 17632
[Hall] p. 1Section 1.1df-asslaw 48031  df-cllaw 48029  df-comlaw 48030
[Hall] p. 2Section 1.2df-clintop 48043
[Hall] p. 7Section 1.3df-sgrp2 48064
[Halmos] p. 28Partition ` `df-parts 38746  dfmembpart2 38751
[Halmos] p. 31Theorem 17.3riesz1 32093  riesz2 32094
[Halmos] p. 41Definition of Hermitianhmopadj2 31969
[Halmos] p. 42Definition of projector orderingpjordi 32201
[Halmos] p. 43Theorem 26.1elpjhmop 32213  elpjidm 32212  pjnmopi 32176
[Halmos] p. 44Remarkpjinormi 31715  pjinormii 31704
[Halmos] p. 44Theorem 26.2elpjch 32217  pjrn 31735  pjrni 31730  pjvec 31724
[Halmos] p. 44Theorem 26.3pjnorm2 31755
[Halmos] p. 44Theorem 26.4hmopidmpj 32182  hmopidmpji 32180
[Halmos] p. 45Theorem 27.1pjinvari 32219
[Halmos] p. 45Theorem 27.3pjoci 32208  pjocvec 31725
[Halmos] p. 45Theorem 27.4pjorthcoi 32197
[Halmos] p. 48Theorem 29.2pjssposi 32200
[Halmos] p. 48Theorem 29.3pjssdif1i 32203  pjssdif2i 32202
[Halmos] p. 50Definition of spectrumdf-spec 31883
[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 1791
[Hatcher] p. 25Definitiondf-phtpc 25037  df-phtpy 25016
[Hatcher] p. 26Definitiondf-pco 25051  df-pi1 25054
[Hatcher] p. 26Proposition 1.2phtpcer 25040
[Hatcher] p. 26Proposition 1.3pi1grp 25096
[Hefferon] p. 240Definition 3.12df-dmat 22511  df-dmatalt 48243
[Helfgott] p. 2Theoremtgoldbach 47741
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47726
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47738  bgoldbtbnd 47733  bgoldbtbnd 47733  tgblthelfgott 47739
[Helfgott] p. 5Proposition 1.1circlevma 34635
[Helfgott] p. 69Statement 7.49circlemethhgt 34636
[Helfgott] p. 69Statement 7.50hgt750lema 34650  hgt750lemb 34649  hgt750leme 34651  hgt750lemf 34646  hgt750lemg 34647
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47735  tgoldbachgt 34656  tgoldbachgtALTV 47736  tgoldbachgtd 34655
[Helfgott] p. 70Statement 7.49ax-hgt749 34637
[Herstein] p. 54Exercise 28df-grpo 30521
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18974  grpoideu 30537  mndideu 18770
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19004  grpoinveu 30547
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19035  grpo2inv 30559
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19048  grpoinvop 30561
[Herstein] p. 57Exercise 1dfgrp3e 19070
[Hitchcock] p. 5Rule A3mptnan 1764
[Hitchcock] p. 5Rule A4mptxor 1765
[Hitchcock] p. 5Rule A5mtpxor 1767
[Holland] p. 1519Theorem 2sumdmdi 32448
[Holland] p. 1520Lemma 5cdj1i 32461  cdj3i 32469  cdj3lem1 32462  cdjreui 32460
[Holland] p. 1524Lemma 7mddmdin0i 32459
[Holland95] p. 13Theorem 3.6hlathil 41947
[Holland95] p. 14Line 15hgmapvs 41873
[Holland95] p. 14Line 16hdmaplkr 41895
[Holland95] p. 14Line 17hdmapellkr 41896
[Holland95] p. 14Line 19hdmapglnm2 41893
[Holland95] p. 14Line 20hdmapip0com 41899
[Holland95] p. 14Theorem 3.6hdmapevec2 41818
[Holland95] p. 14Lines 24 and 25hdmapoc 41913
[Holland95] p. 204Definition of involutiondf-srng 20857
[Holland95] p. 212Definition of subspacedf-psubsp 39485
[Holland95] p. 214Lemma 3.3lclkrlem2v 41510
[Holland95] p. 214Definition 3.2df-lpolN 41463
[Holland95] p. 214Definition of nonsingularpnonsingN 39915
[Holland95] p. 215Lemma 3.3(1)dihoml4 41359  poml4N 39935
[Holland95] p. 215Lemma 3.3(2)dochexmid 41450  pexmidALTN 39960  pexmidN 39951
[Holland95] p. 218Theorem 3.6lclkr 41515
[Holland95] p. 218Definition of dual vector spacedf-ldual 39105  ldualset 39106
[Holland95] p. 222Item 1df-lines 39483  df-pointsN 39484
[Holland95] p. 222Item 2df-polarityN 39885
[Holland95] p. 223Remarkispsubcl2N 39929  omllaw4 39227  pol1N 39892  polcon3N 39899
[Holland95] p. 223Definitiondf-psubclN 39917
[Holland95] p. 223Equation for polaritypolval2N 39888
[Holmes] p. 40Definitiondf-xrn 38352
[Hughes] p. 44Equation 1.21bax-his3 31112
[Hughes] p. 47Definition of projection operatordfpjop 32210
[Hughes] p. 49Equation 1.30eighmre 31991  eigre 31863  eigrei 31862
[Hughes] p. 49Equation 1.31eighmorth 31992  eigorth 31866  eigorthi 31865
[Hughes] p. 137Remark (ii)eigposi 31864
[Huneke] p. 1Claim 1frgrncvvdeq 30337
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30333
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30334
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30335
[Huneke] p. 2Claim 2frgrregorufr 30353  frgrregorufr0 30352  frgrregorufrg 30354
[Huneke] p. 2Claim 3frgrhash2wsp 30360  frrusgrord 30369  frrusgrord0 30368
[Huneke] p. 2Statementdf-clwwlknon 30116
[Huneke] p. 2Statement 4frgrwopreglem4 30343
[Huneke] p. 2Statement 5frgrwopreg1 30346  frgrwopreg2 30347  frgrwopregasn 30344  frgrwopregbsn 30345
[Huneke] p. 2Statement 6frgrwopreglem5 30349
[Huneke] p. 2Statement 7fusgreghash2wspv 30363
[Huneke] p. 2Statement 8fusgreghash2wsp 30366
[Huneke] p. 2Statement 9clwlksndivn 30114  numclwlk1 30399  numclwlk1lem1 30397  numclwlk1lem2 30398  numclwwlk1 30389  numclwwlk8 30420
[Huneke] p. 2Definition 3frgrwopreglem1 30340
[Huneke] p. 2Definition 4df-clwlks 29803
[Huneke] p. 2Definition 62clwwlk 30375
[Huneke] p. 2Definition 7numclwwlkovh 30401  numclwwlkovh0 30400
[Huneke] p. 2Statement 10numclwwlk2 30409
[Huneke] p. 2Statement 11rusgrnumwlkg 30006
[Huneke] p. 2Statement 12numclwwlk3 30413
[Huneke] p. 2Statement 13numclwwlk5 30416
[Huneke] p. 2Statement 14numclwwlk7 30419
[Indrzejczak] p. 33Definition ` `Enatded 30431  natded 30431
[Indrzejczak] p. 33Definition ` `Inatded 30431
[Indrzejczak] p. 34Definition ` `Enatded 30431  natded 30431
[Indrzejczak] p. 34Definition ` `Inatded 30431
[Jech] p. 4Definition of classcv 1535  cvjust 2728
[Jech] p. 42Lemma 6.1alephexp1 10616
[Jech] p. 42Equation 6.1alephadd 10614  alephmul 10615
[Jech] p. 43Lemma 6.2infmap 10613  infmap2 10254
[Jech] p. 71Lemma 9.3jech9.3 9851
[Jech] p. 72Equation 9.3scott0 9923  scottex 9922
[Jech] p. 72Exercise 9.1rankval4 9904
[Jech] p. 72Scheme "Collection Principle"cp 9928
[Jech] p. 78Noteopthprc 5752
[JonesMatijasevic] p. 694Definition 2.3rmxyval 42903
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 42991
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 42992
[JonesMatijasevic] p. 695Equation 2.7rmxadd 42915
[JonesMatijasevic] p. 695Equation 2.8rmyadd 42919
[JonesMatijasevic] p. 695Equation 2.9rmxp1 42920  rmyp1 42921
[JonesMatijasevic] p. 695Equation 2.10rmxm1 42922  rmym1 42923
[JonesMatijasevic] p. 695Equation 2.11rmx0 42913  rmx1 42914  rmxluc 42924
[JonesMatijasevic] p. 695Equation 2.12rmy0 42917  rmy1 42918  rmyluc 42925
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 42927
[JonesMatijasevic] p. 695Equation 2.14rmydbl 42928
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42948  jm2.17b 42949  jm2.17c 42950
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 42981
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 42985
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 42976
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42951  jm2.24nn 42947
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 42990
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 42996  rmygeid 42952
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43008
[Juillerat] p. 11Section *5etransc 46238  etransclem47 46236  etransclem48 46237
[Juillerat] p. 12Equation (7)etransclem44 46233
[Juillerat] p. 12Equation *(7)etransclem46 46235
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46221
[Juillerat] p. 13Proofetransclem35 46224
[Juillerat] p. 13Part of case 2 proven inetransclem38 46227
[Juillerat] p. 13Part of case 2 provenetransclem24 46213
[Juillerat] p. 13Part of case 2: proven inetransclem41 46230
[Juillerat] p. 14Proofetransclem23 46212
[KalishMontague] p. 81Note 1ax-6 1964
[KalishMontague] p. 85Lemma 2equid 2008
[KalishMontague] p. 85Lemma 3equcomi 2013
[KalishMontague] p. 86Lemma 7cbvalivw 2003  cbvaliw 2002  wl-cbvmotv 37493  wl-motae 37495  wl-moteq 37494
[KalishMontague] p. 87Lemma 8spimvw 1992  spimw 1967
[KalishMontague] p. 87Lemma 9spfw 2029  spw 2030
[Kalmbach] p. 14Definition of latticechabs1 31544  chabs1i 31546  chabs2 31545  chabs2i 31547  chjass 31561  chjassi 31514  latabs1 18532  latabs2 18533
[Kalmbach] p. 15Definition of atomdf-at 32366  ela 32367
[Kalmbach] p. 15Definition of coverscvbr2 32311  cvrval2 39255
[Kalmbach] p. 16Definitiondf-ol 39159  df-oml 39160
[Kalmbach] p. 20Definition of commutescmbr 31612  cmbri 31618  cmtvalN 39192  df-cm 31611  df-cmtN 39158
[Kalmbach] p. 22Remarkomllaw5N 39228  pjoml5 31641  pjoml5i 31616
[Kalmbach] p. 22Definitionpjoml2 31639  pjoml2i 31613
[Kalmbach] p. 22Theorem 2(v)cmcm 31642  cmcmi 31620  cmcmii 31625  cmtcomN 39230
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39226  omlsi 31432  pjoml 31464  pjomli 31463
[Kalmbach] p. 22Definition of OML lawomllaw2N 39225
[Kalmbach] p. 23Remarkcmbr2i 31624  cmcm3 31643  cmcm3i 31622  cmcm3ii 31627  cmcm4i 31623  cmt3N 39232  cmt4N 39233  cmtbr2N 39234
[Kalmbach] p. 23Lemma 3cmbr3 31636  cmbr3i 31628  cmtbr3N 39235
[Kalmbach] p. 25Theorem 5fh1 31646  fh1i 31649  fh2 31647  fh2i 31650  omlfh1N 39239
[Kalmbach] p. 65Remarkchjatom 32385  chslej 31526  chsleji 31486  shslej 31408  shsleji 31398
[Kalmbach] p. 65Proposition 1chocin 31523  chocini 31482  chsupcl 31368  chsupval2 31438  h0elch 31283  helch 31271  hsupval2 31437  ocin 31324  ococss 31321  shococss 31322
[Kalmbach] p. 65Definition of subspace sumshsval 31340
[Kalmbach] p. 66Remarkdf-pjh 31423  pjssmi 32193  pjssmii 31709
[Kalmbach] p. 67Lemma 3osum 31673  osumi 31670
[Kalmbach] p. 67Lemma 4pjci 32228
[Kalmbach] p. 103Exercise 6atmd2 32428
[Kalmbach] p. 103Exercise 12mdsl0 32338
[Kalmbach] p. 140Remarkhatomic 32388  hatomici 32387  hatomistici 32390
[Kalmbach] p. 140Proposition 1atlatmstc 39300
[Kalmbach] p. 140Proposition 1(i)atexch 32409  lsatexch 39024
[Kalmbach] p. 140Proposition 1(ii)chcv1 32383  cvlcvr1 39320  cvr1 39392
[Kalmbach] p. 140Proposition 1(iii)cvexch 32402  cvexchi 32397  cvrexch 39402
[Kalmbach] p. 149Remark 2chrelati 32392  hlrelat 39384  hlrelat5N 39383  lrelat 38995
[Kalmbach] p. 153Exercise 5lsmcv 21160  lsmsatcv 38991  spansncv 31681  spansncvi 31680
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39010  spansncv2 32321
[Kalmbach] p. 266Definitiondf-st 32239
[Kalmbach2] p. 8Definition of adjointdf-adjh 31877
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10683  fpwwe2 10680
[KanamoriPincus] p. 416Corollary 1.3canth4 10684
[KanamoriPincus] p. 417Corollary 1.6canthp1 10691
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10686
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10688
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10701
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10705  gchxpidm 10706
[KanamoriPincus] p. 419Theorem 2.1gchacg 10717  gchhar 10716
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10252  unxpwdom 9626
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10707
[Kreyszig] p. 3Property M1metcl 24357  xmetcl 24356
[Kreyszig] p. 4Property M2meteq0 24364
[Kreyszig] p. 8Definition 1.1-8dscmet 24600
[Kreyszig] p. 12Equation 5conjmul 11981  muleqadd 11904
[Kreyszig] p. 18Definition 1.3-2mopnval 24463
[Kreyszig] p. 19Remarkmopntopon 24464
[Kreyszig] p. 19Theorem T1mopn0 24526  mopnm 24469
[Kreyszig] p. 19Theorem T2unimopn 24524
[Kreyszig] p. 19Definition of neighborhoodneibl 24529
[Kreyszig] p. 20Definition 1.3-3metcnp2 24570
[Kreyszig] p. 25Definition 1.4-1lmbr 23281  lmmbr 25305  lmmbr2 25306
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23403
[Kreyszig] p. 28Theorem 1.4-5lmcau 25360
[Kreyszig] p. 28Definition 1.4-3iscau 25323  iscmet2 25341
[Kreyszig] p. 30Theorem 1.4-7cmetss 25363
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23484  metelcls 25352
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25353  metcld2 25354
[Kreyszig] p. 51Equation 2clmvneg1 25145  lmodvneg1 20919  nvinv 30667  vcm 30604
[Kreyszig] p. 51Equation 1aclm0vs 25141  lmod0vs 20909  slmd0vs 33212  vc0 30602
[Kreyszig] p. 51Equation 1blmodvs0 20910  slmdvs0 33213  vcz 30603
[Kreyszig] p. 58Definition 2.2-1imsmet 30719  ngpmet 24631  nrmmetd 24602
[Kreyszig] p. 59Equation 1imsdval 30714  imsdval2 30715  ncvspds 25208  ngpds 24632
[Kreyszig] p. 63Problem 1nmval 24617  nvnd 30716
[Kreyszig] p. 64Problem 2nmeq0 24646  nmge0 24645  nvge0 30701  nvz 30697
[Kreyszig] p. 64Problem 3nmrtri 24652  nvabs 30700
[Kreyszig] p. 91Definition 2.7-1isblo3i 30829
[Kreyszig] p. 92Equation 2df-nmoo 30773
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30835  blocni 30833
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30834
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25251  ipeq0 21673  ipz 30747
[Kreyszig] p. 135Problem 2cphpyth 25263  pythi 30878
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30882
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25285
[Kreyszig] p. 144Equation 4supcvg 15888
[Kreyszig] p. 144Theorem 3.3-1minvec 25483  minveco 30912
[Kreyszig] p. 196Definition 3.9-1df-aj 30778
[Kreyszig] p. 247Theorem 4.7-2bcth 25376
[Kreyszig] p. 249Theorem 4.7-3ubth 30901
[Kreyszig] p. 470Definition of positive operator orderingleop 32151  leopg 32150
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32169
[Kreyszig] p. 525Theorem 10.1-1htth 30946
[Kulpa] p. 547Theorempoimir 37639
[Kulpa] p. 547Equation (1)poimirlem32 37638
[Kulpa] p. 547Equation (2)poimirlem31 37637
[Kulpa] p. 548Theorembroucube 37640
[Kulpa] p. 548Equation (6)poimirlem26 37632
[Kulpa] p. 548Equation (7)poimirlem27 37633
[Kunen] p. 10Axiom 0ax6e 2385  axnul 5310
[Kunen] p. 11Axiom 3axnul 5310
[Kunen] p. 12Axiom 6zfrep6 7977
[Kunen] p. 24Definition 10.24mapval 8876  mapvalg 8874
[Kunen] p. 30Lemma 10.20fodomg 10559
[Kunen] p. 31Definition 10.24mapex 7961
[Kunen] p. 95Definition 2.1df-r1 9801
[Kunen] p. 97Lemma 2.10r1elss 9843  r1elssi 9842
[Kunen] p. 107Exercise 4rankop 9895  rankopb 9889  rankuni 9900  rankxplim 9916  rankxpsuc 9919
[Kunen2] p. 111Lemma II.2.4(1)traxext 44937
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 44946
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 44947
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 44945
[Kunen2] p. 112Corollary II.2.5wfaxext 44948  wfaxpr 44951  wfaxrep 44949  wfaxsep 44950
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 5008
[Lang] , p. 225Corollary 1.3finexttrb 33689
[Lang] p. Definitiondf-rn 5699
[Lang] p. 3Statementlidrideqd 18694  mndbn0 18775
[Lang] p. 3Definitiondf-mnd 18760
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18712
[Lang] p. 4Property of composites. Second formulagsumccat 18866
[Lang] p. 5Equationgsumreidx 19949
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48025
[Lang] p. 6Examplenn0mnd 48022
[Lang] p. 6Equationgsumxp2 20012
[Lang] p. 6Statementcycsubm 19232
[Lang] p. 6Definitionmulgnn0gsum 19110
[Lang] p. 6Observationmndlsmidm 19702
[Lang] p. 7Definitiondfgrp2e 18993
[Lang] p. 30Definitiondf-tocyc 33109
[Lang] p. 32Property (a)cyc3genpm 33154
[Lang] p. 32Property (b)cyc3conja 33159  cycpmconjv 33144
[Lang] p. 53Definitiondf-cat 17712
[Lang] p. 53Axiom CAT 1cat1 18150  cat1lem 18149
[Lang] p. 54Definitiondf-iso 17796
[Lang] p. 57Definitiondf-inito 18037  df-termo 18038
[Lang] p. 58Exampleirinitoringc 21507
[Lang] p. 58Statementinitoeu1 18064  termoeu1 18071
[Lang] p. 62Definitiondf-func 17908
[Lang] p. 65Definitiondf-nat 17997
[Lang] p. 91Notedf-ringc 20662
[Lang] p. 92Statementmxidlprm 33477
[Lang] p. 92Definitionisprmidlc 33454
[Lang] p. 128Remarkdsmmlmod 21782
[Lang] p. 129Prooflincscm 48275  lincscmcl 48277  lincsum 48274  lincsumcl 48276
[Lang] p. 129Statementlincolss 48279
[Lang] p. 129Observationdsmmfi 21775
[Lang] p. 141Theorem 5.3dimkerim 33654  qusdimsum 33655
[Lang] p. 141Corollary 5.4lssdimle 33634
[Lang] p. 147Definitionsnlindsntor 48316
[Lang] p. 504Statementmat1 22468  matring 22464
[Lang] p. 504Definitiondf-mamu 22410
[Lang] p. 505Statementmamuass 22421  mamutpos 22479  matassa 22465  mattposvs 22476  tposmap 22478
[Lang] p. 513Definitionmdet1 22622  mdetf 22616
[Lang] p. 513Theorem 4.4cramer 22712
[Lang] p. 514Proposition 4.6mdetleib 22608
[Lang] p. 514Proposition 4.8mdettpos 22632
[Lang] p. 515Definitiondf-minmar1 22656  smadiadetr 22696
[Lang] p. 515Corollary 4.9mdetero 22631  mdetralt 22629
[Lang] p. 517Proposition 4.15mdetmul 22644
[Lang] p. 518Definitiondf-madu 22655
[Lang] p. 518Proposition 4.16madulid 22666  madurid 22665  matinv 22698
[Lang] p. 561Theorem 3.1cayleyhamilton 22911
[Lang], p. 224Proposition 1.2extdgmul 33688  fedgmul 33658
[Lang], p. 561Remarkchpmatply1 22853
[Lang], p. 561Definitiondf-chpmat 22848
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44329
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44324
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44330
[LeBlanc] p. 277Rule R2axnul 5310
[Levy] p. 12Axiom 4.3.1df-clab 2712
[Levy] p. 59Definitiondf-ttrcl 9745
[Levy] p. 64Theorem 5.6(ii)frinsg 9788
[Levy] p. 338Axiomdf-clel 2813  df-cleq 2726
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2813  df-cleq 2726
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2712
[Levy] p. 358Axiomdf-clab 2712
[Levy58] p. 2Definition Iisfin1-3 10423
[Levy58] p. 2Definition IIdf-fin2 10323
[Levy58] p. 2Definition Iadf-fin1a 10322
[Levy58] p. 2Definition IIIdf-fin3 10325
[Levy58] p. 3Definition Vdf-fin5 10326
[Levy58] p. 3Definition IVdf-fin4 10324
[Levy58] p. 4Definition VIdf-fin6 10327
[Levy58] p. 4Definition VIIdf-fin7 10328
[Levy58], p. 3Theorem 1fin1a2 10452
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27745
[Lipparini] p. 3Lemma 2.1.4noresle 27756
[Lipparini] p. 6Proposition 4.2noinfbnd1 27788  nosupbnd1 27773
[Lipparini] p. 6Proposition 4.3noinfbnd2 27790  nosupbnd2 27775
[Lipparini] p. 7Theorem 5.1noetasuplem3 27794  noetasuplem4 27795
[Lipparini] p. 7Corollary 4.4nosupinfsep 27791
[Lopez-Astorga] p. 12Rule 1mptnan 1764
[Lopez-Astorga] p. 12Rule 2mptxor 1765
[Lopez-Astorga] p. 12Rule 3mtpxor 1767
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32436
[Maeda] p. 168Lemma 5mdsym 32440  mdsymi 32439
[Maeda] p. 168Lemma 4(i)mdsymlem4 32434  mdsymlem6 32436  mdsymlem7 32437
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32438
[MaedaMaeda] p. 1Remarkssdmd1 32341  ssdmd2 32342  ssmd1 32339  ssmd2 32340
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32337
[MaedaMaeda] p. 1Definition 1.1df-dmd 32309  df-md 32308  mdbr 32322
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32359  mdslj1i 32347  mdslj2i 32348  mdslle1i 32345  mdslle2i 32346  mdslmd1i 32357  mdslmd2i 32358
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32349  mdsl2bi 32351  mdsl2i 32350
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32363
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32360
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32361
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32338
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32343  mdsl3 32344
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32362
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32457
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39302  hlrelat1 39382
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39020
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32364  cvmdi 32352  cvnbtwn4 32317  cvrnbtwn4 39260
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32365
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39321  cvp 32403  cvrp 39398  lcvp 39021
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32427
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32426
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39314  hlexch4N 39374
[MaedaMaeda] p. 34Exercise 7.1atabsi 32429
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39425
[MaedaMaeda] p. 61Definition 15.10psubN 39731  atpsubN 39735  df-pointsN 39484  pointpsubN 39733
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39486  pmap11 39744  pmaple 39743  pmapsub 39750  pmapval 39739
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39747  pmap1N 39749
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39752  pmapglb2N 39753  pmapglb2xN 39754  pmapglbx 39751
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39834
[MaedaMaeda] p. 67Postulate PS1ps-1 39459
[MaedaMaeda] p. 68Lemma 16.2df-padd 39778  paddclN 39824  paddidm 39823
[MaedaMaeda] p. 68Condition PS2ps-2 39460
[MaedaMaeda] p. 68Equation 16.2.1paddass 39820
[MaedaMaeda] p. 69Lemma 16.4ps-1 39459
[MaedaMaeda] p. 69Theorem 16.4ps-2 39460
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19707  lsmmod2 19708  lssats 38993  shatomici 32386  shatomistici 32389  shmodi 31418  shmodsi 31417
[MaedaMaeda] p. 130Remark 29.6dmdmd 32328  mdsymlem7 32437
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31617
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31521
[MaedaMaeda] p. 139Remarksumdmdii 32443
[Margaris] p. 40Rule Cexlimiv 1927
[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 1776  df-or 848  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30428
[Margaris] p. 59Section 14notnotrALTVD 44912
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 44913
[Margaris] p. 79Rule Cexinst01 44622  exinst11 44623
[Margaris] p. 89Theorem 19.219.2 1973  19.2g 2185  r19.2z 4500
[Margaris] p. 89Theorem 19.319.3 2199  rr19.3v 3666
[Margaris] p. 89Theorem 19.5alcom 2156
[Margaris] p. 89Theorem 19.6alex 1822
[Margaris] p. 89Theorem 19.7alnex 1777
[Margaris] p. 89Theorem 19.819.8a 2178
[Margaris] p. 89Theorem 19.919.9 2202  19.9h 2284  exlimd 2215  exlimdh 2288
[Margaris] p. 89Theorem 19.11excom 2159  excomim 2160
[Margaris] p. 89Theorem 19.1219.12 2325
[Margaris] p. 90Section 19conventions-labels 30429  conventions-labels 30429  conventions-labels 30429  conventions-labels 30429
[Margaris] p. 90Theorem 19.14exnal 1823
[Margaris] p. 90Theorem 19.152albi 44373  albi 1814
[Margaris] p. 90Theorem 19.1619.16 2222
[Margaris] p. 90Theorem 19.1719.17 2223
[Margaris] p. 90Theorem 19.182exbi 44375  exbi 1843
[Margaris] p. 90Theorem 19.1919.19 2226
[Margaris] p. 90Theorem 19.202alim 44372  2alimdv 1915  alimd 2209  alimdh 1813  alimdv 1913  ax-4 1805  ralimdaa 3257  ralimdv 3166  ralimdva 3164  ralimdvva 3203  sbcimdv 3864
[Margaris] p. 90Theorem 19.2119.21 2204  19.21h 2285  19.21t 2203  19.21vv 44371  alrimd 2212  alrimdd 2211  alrimdh 1860  alrimdv 1926  alrimi 2210  alrimih 1820  alrimiv 1924  alrimivv 1925  hbralrimi 3141  r19.21be 3249  r19.21bi 3248  ralrimd 3261  ralrimdv 3149  ralrimdva 3151  ralrimdvv 3200  ralrimdvva 3208  ralrimi 3254  ralrimia 3255  ralrimiv 3142  ralrimiva 3143  ralrimivv 3197  ralrimivva 3199  ralrimivvva 3202  ralrimivw 3147
[Margaris] p. 90Theorem 19.222exim 44374  2eximdv 1916  exim 1830  eximd 2213  eximdh 1861  eximdv 1914  rexim 3084  reximd2a 3266  reximdai 3258  reximdd 45090  reximddv 3168  reximddv2 3212  reximddv3 3169  reximdv 3167  reximdv2 3161  reximdva 3165  reximdvai 3162  reximdvva 3204  reximi2 3076
[Margaris] p. 90Theorem 19.2319.23 2208  19.23bi 2188  19.23h 2286  19.23t 2207  exlimdv 1930  exlimdvv 1931  exlimexi 44521  exlimiv 1927  exlimivv 1929  rexlimd3 45083  rexlimdv 3150  rexlimdv3a 3156  rexlimdva 3152  rexlimdva2 3154  rexlimdvaa 3153  rexlimdvv 3209  rexlimdvva 3210  rexlimdvvva 3211  rexlimdvw 3157  rexlimiv 3145  rexlimiva 3144  rexlimivv 3198
[Margaris] p. 90Theorem 19.2419.24 1982
[Margaris] p. 90Theorem 19.2519.25 1877
[Margaris] p. 90Theorem 19.2619.26 1867
[Margaris] p. 90Theorem 19.2719.27 2224  r19.27z 4510  r19.27zv 4511
[Margaris] p. 90Theorem 19.2819.28 2225  19.28vv 44381  r19.28z 4503  r19.28zf 45101  r19.28zv 4506  rr19.28v 3667
[Margaris] p. 90Theorem 19.2919.29 1870  r19.29d2r 3137  r19.29imd 3115
[Margaris] p. 90Theorem 19.3019.30 1878
[Margaris] p. 90Theorem 19.3119.31 2231  19.31vv 44379
[Margaris] p. 90Theorem 19.3219.32 2230  r19.32 47047
[Margaris] p. 90Theorem 19.3319.33-2 44377  19.33 1881
[Margaris] p. 90Theorem 19.3419.34 1983
[Margaris] p. 90Theorem 19.3519.35 1874
[Margaris] p. 90Theorem 19.3619.36 2227  19.36vv 44378  r19.36zv 4512
[Margaris] p. 90Theorem 19.3719.37 2229  19.37vv 44380  r19.37zv 4507
[Margaris] p. 90Theorem 19.3819.38 1835
[Margaris] p. 90Theorem 19.3919.39 1981
[Margaris] p. 90Theorem 19.4019.40-2 1884  19.40 1883  r19.40 3116
[Margaris] p. 90Theorem 19.4119.41 2232  19.41rg 44547
[Margaris] p. 90Theorem 19.4219.42 2233
[Margaris] p. 90Theorem 19.4319.43 1879
[Margaris] p. 90Theorem 19.4419.44 2234  r19.44zv 4509
[Margaris] p. 90Theorem 19.4519.45 2235  r19.45zv 4508
[Margaris] p. 110Exercise 2(b)eu1 2607
[Mayet] p. 370Remarkjpi 32298  largei 32295  stri 32285
[Mayet3] p. 9Definition of CH-statesdf-hst 32240  ishst 32242
[Mayet3] p. 10Theoremhstrbi 32294  hstri 32293
[Mayet3] p. 1223Theorem 4.1mayete3i 31756
[Mayet3] p. 1240Theorem 7.1mayetes3i 31757
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32306
[MegPav2000] p. 2345Definition 3.4-1chintcl 31360  chsupcl 31368
[MegPav2000] p. 2345Definition 3.4-2hatomic 32388
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32382
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32409
[MegPav2000] p. 2366Figure 7pl42N 39965
[MegPav2002] p. 362Lemma 2.2latj31 18544  latj32 18542  latjass 18540
[Megill] p. 444Axiom C5ax-5 1907  ax5ALT 38888
[Megill] p. 444Section 7conventions 30428
[Megill] p. 445Lemma L12aecom-o 38882  ax-c11n 38869  axc11n 2428
[Megill] p. 446Lemma L17equtrr 2018
[Megill] p. 446Lemma L18ax6fromc10 38877
[Megill] p. 446Lemma L19hbnae-o 38909  hbnae 2434
[Megill] p. 447Remark 9.1dfsb1 2483  sbid 2252  sbidd-misc 48949  sbidd 48948
[Megill] p. 448Remark 9.6axc14 2465
[Megill] p. 448Scheme C4'ax-c4 38865
[Megill] p. 448Scheme C5'ax-c5 38864  sp 2180
[Megill] p. 448Scheme C6'ax-11 2154
[Megill] p. 448Scheme C7'ax-c7 38866
[Megill] p. 448Scheme C8'ax-7 2004
[Megill] p. 448Scheme C9'ax-c9 38871
[Megill] p. 448Scheme C10'ax-6 1964  ax-c10 38867
[Megill] p. 448Scheme C11'ax-c11 38868
[Megill] p. 448Scheme C12'ax-8 2107
[Megill] p. 448Scheme C13'ax-9 2115
[Megill] p. 448Scheme C14'ax-c14 38872
[Megill] p. 448Scheme C15'ax-c15 38870
[Megill] p. 448Scheme C16'ax-c16 38873
[Megill] p. 448Theorem 9.4dral1-o 38885  dral1 2441  dral2-o 38911  dral2 2440  drex1 2443  drex2 2444  drsb1 2497  drsb2 2263
[Megill] p. 449Theorem 9.7sbcom2 2170  sbequ 2080  sbid2v 2511
[Megill] p. 450Example in Appendixhba1-o 38878  hba1 2291
[Mendelson] p. 35Axiom A3hirstL-ax3 46841
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3887  rspsbca 3888  stdpc4 2065
[Mendelson] p. 69Axiom 5ax-c4 38865  ra4 3894  stdpc5 2205
[Mendelson] p. 81Rule Cexlimiv 1927
[Mendelson] p. 95Axiom 6stdpc6 2024
[Mendelson] p. 95Axiom 7stdpc7 2247
[Mendelson] p. 225Axiom system NBGru 3788
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5523
[Mendelson] p. 231Exercise 4.10(k)inv1 4403
[Mendelson] p. 231Exercise 4.10(l)unv 4404
[Mendelson] p. 231Exercise 4.10(n)dfin3 4282
[Mendelson] p. 231Exercise 4.10(o)df-nul 4339
[Mendelson] p. 231Exercise 4.10(q)dfin4 4283
[Mendelson] p. 231Exercise 4.10(s)ddif 4150
[Mendelson] p. 231Definition of uniondfun3 4281
[Mendelson] p. 235Exercise 4.12(c)univ 5461
[Mendelson] p. 235Exercise 4.12(d)pwv 4908
[Mendelson] p. 235Exercise 4.12(j)pwin 5578
[Mendelson] p. 235Exercise 4.12(k)pwunss 4622
[Mendelson] p. 235Exercise 4.12(l)pwssun 5579
[Mendelson] p. 235Exercise 4.12(n)uniin 4935
[Mendelson] p. 235Exercise 4.12(p)reli 5838
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6289
[Mendelson] p. 244Proposition 4.8(g)epweon 7793
[Mendelson] p. 246Definition of successordf-suc 6391
[Mendelson] p. 250Exercise 4.36oelim2 8631
[Mendelson] p. 254Proposition 4.22(b)xpen 9178
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9093  xpsneng 9094
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9101  xpcomeng 9102
[Mendelson] p. 254Proposition 4.22(e)xpassen 9104
[Mendelson] p. 255Definitionbrsdom 9013
[Mendelson] p. 255Exercise 4.39endisj 9096
[Mendelson] p. 255Exercise 4.41mapprc 8868
[Mendelson] p. 255Exercise 4.43mapsnen 9075  mapsnend 9074
[Mendelson] p. 255Exercise 4.45mapunen 9184
[Mendelson] p. 255Exercise 4.47xpmapen 9183
[Mendelson] p. 255Exercise 4.42(a)map0e 8920
[Mendelson] p. 255Exercise 4.42(b)map1 9078
[Mendelson] p. 257Proposition 4.24(a)undom 9097
[Mendelson] p. 258Exercise 4.56(c)djuassen 10216  djucomen 10215
[Mendelson] p. 258Exercise 4.56(f)djudom1 10220
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10214
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8567
[Mendelson] p. 266Proposition 4.34(f)oaordex 8594
[Mendelson] p. 275Proposition 4.42(d)entri3 10596
[Mendelson] p. 281Definitiondf-r1 9801
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9850
[Mendelson] p. 287Axiom system MKru 3788
[MertziosUnger] p. 152Definitiondf-frgr 30287
[MertziosUnger] p. 153Remark 1frgrconngr 30322
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30324  vdgn1frgrv3 30325
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30326
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30319
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30312  2pthfrgrrn 30310  2pthfrgrrn2 30311
[Mittelstaedt] p. 9Definitiondf-oc 31280
[Monk1] p. 22Remarkconventions 30428
[Monk1] p. 22Theorem 3.1conventions 30428
[Monk1] p. 26Theorem 2.8(vii)ssin 4246
[Monk1] p. 33Theorem 3.2(i)ssrel 5794  ssrelf 32634
[Monk1] p. 33Theorem 3.2(ii)eqrel 5796
[Monk1] p. 34Definition 3.3df-opab 5210
[Monk1] p. 36Theorem 3.7(i)coi1 6283  coi2 6284
[Monk1] p. 36Theorem 3.8(v)dm0 5933  rn0 5938
[Monk1] p. 36Theorem 3.7(ii)cnvi 6163
[Monk1] p. 37Theorem 3.13(i)relxp 5706
[Monk1] p. 37Theorem 3.13(x)dmxp 5941  rnxp 6191
[Monk1] p. 37Theorem 3.13(ii)0xp 5786  xp0 6179
[Monk1] p. 38Theorem 3.16(ii)ima0 6096
[Monk1] p. 38Theorem 3.16(viii)imai 6093
[Monk1] p. 39Theorem 3.17imaex 7936  imaexALTV 38311  imaexg 7935
[Monk1] p. 39Theorem 3.16(xi)imassrn 6090
[Monk1] p. 41Theorem 4.3(i)fnopfv 7094  funfvop 7069
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6962
[Monk1] p. 42Theorem 4.4(iii)fvelima 6973
[Monk1] p. 43Theorem 4.6funun 6613
[Monk1] p. 43Theorem 4.8(iv)dff13 7274  dff13f 7275
[Monk1] p. 46Theorem 4.15(v)funex 7238  funrnex 7976
[Monk1] p. 50Definition 5.4fniunfv 7266
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6248
[Monk1] p. 52Theorem 5.11(viii)ssint 4968
[Monk1] p. 52Definition 5.13 (i)1stval2 8029  df-1st 8012
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8030  df-2nd 8013
[Monk1] p. 112Theorem 15.17(v)ranksn 9891  ranksnb 9864
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9892
[Monk1] p. 112Theorem 15.17(iii)rankun 9893  rankunb 9887
[Monk1] p. 113Theorem 15.18r1val3 9875
[Monk1] p. 113Definition 15.19df-r1 9801  r1val2 9874
[Monk1] p. 117Lemmazorn2 10543  zorn2g 10540
[Monk1] p. 133Theorem 18.11cardom 10023
[Monk1] p. 133Theorem 18.12canth3 10598
[Monk1] p. 133Theorem 18.14carduni 10018
[Monk2] p. 105Axiom C4ax-4 1805
[Monk2] p. 105Axiom C7ax-7 2004
[Monk2] p. 105Axiom C8ax-12 2174  ax-c15 38870  ax12v2 2176
[Monk2] p. 108Lemma 5ax-c4 38865
[Monk2] p. 109Lemma 12ax-11 2154
[Monk2] p. 109Lemma 15equvini 2457  equvinv 2025  eqvinop 5497
[Monk2] p. 113Axiom C5-1ax-5 1907  ax5ALT 38888
[Monk2] p. 113Axiom C5-2ax-10 2138
[Monk2] p. 113Axiom C5-3ax-11 2154
[Monk2] p. 114Lemma 21sp 2180
[Monk2] p. 114Lemma 22axc4 2319  hba1-o 38878  hba1 2291
[Monk2] p. 114Lemma 23nfia1 2150
[Monk2] p. 114Lemma 24nfa2 2173  nfra2 3373  nfra2w 3296
[Moore] p. 53Part Idf-mre 17630
[Munkres] p. 77Example 2distop 23017  indistop 23024  indistopon 23023
[Munkres] p. 77Example 3fctop 23026  fctop2 23027
[Munkres] p. 77Example 4cctop 23028
[Munkres] p. 78Definition of basisdf-bases 22968  isbasis3g 22971
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17489  tgval2 22978
[Munkres] p. 79Remarktgcl 22991
[Munkres] p. 80Lemma 2.1tgval3 22985
[Munkres] p. 80Lemma 2.2tgss2 23009  tgss3 23008
[Munkres] p. 81Lemma 2.3basgen 23010  basgen2 23011
[Munkres] p. 83Exercise 3topdifinf 37331  topdifinfeq 37332  topdifinffin 37330  topdifinfindis 37328
[Munkres] p. 89Definition of subspace topologyresttop 23183
[Munkres] p. 93Theorem 6.1(1)0cld 23061  topcld 23058
[Munkres] p. 93Theorem 6.1(2)iincld 23062
[Munkres] p. 93Theorem 6.1(3)uncld 23064
[Munkres] p. 94Definition of closureclsval 23060
[Munkres] p. 94Definition of interiorntrval 23059
[Munkres] p. 95Theorem 6.5(a)clsndisj 23098  elcls 23096
[Munkres] p. 95Theorem 6.5(b)elcls3 23106
[Munkres] p. 97Theorem 6.6clslp 23171  neindisj 23140
[Munkres] p. 97Corollary 6.7cldlp 23173
[Munkres] p. 97Definition of limit pointislp2 23168  lpval 23162
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23338
[Munkres] p. 102Definition of continuous functiondf-cn 23250  iscn 23258  iscn2 23261
[Munkres] p. 107Theorem 7.2(g)cncnp 23303  cncnp2 23304  cncnpi 23301  df-cnp 23251  iscnp 23260  iscnp2 23262
[Munkres] p. 127Theorem 10.1metcn 24571
[Munkres] p. 128Theorem 10.3metcn4 25358
[Nathanson] p. 123Remarkreprgt 34614  reprinfz1 34615  reprlt 34612
[Nathanson] p. 123Definitiondf-repr 34602
[Nathanson] p. 123Chapter 5.1circlemethnat 34634
[Nathanson] p. 123Propositionbreprexp 34626  breprexpnat 34627  itgexpif 34599
[NielsenChuang] p. 195Equation 4.73unierri 32132
[OeSilva] p. 2042Section 2ax-bgbltosilva 47734
[Pfenning] p. 17Definition XMnatded 30431
[Pfenning] p. 17Definition NNCnatded 30431  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30431
[Pfenning] p. 18Rule"natded 30431
[Pfenning] p. 18Definition /\Inatded 30431
[Pfenning] p. 18Definition ` `Enatded 30431  natded 30431  natded 30431  natded 30431  natded 30431
[Pfenning] p. 18Definition ` `Inatded 30431  natded 30431  natded 30431  natded 30431  natded 30431
[Pfenning] p. 18Definition ` `ELnatded 30431
[Pfenning] p. 18Definition ` `ERnatded 30431
[Pfenning] p. 18Definition ` `Ea,unatded 30431
[Pfenning] p. 18Definition ` `IRnatded 30431
[Pfenning] p. 18Definition ` `Ianatded 30431
[Pfenning] p. 127Definition =Enatded 30431
[Pfenning] p. 127Definition =Inatded 30431
[Ponnusamy] p. 361Theorem 6.44cphip0l 25249  df-dip 30729  dip0l 30746  ip0l 21671
[Ponnusamy] p. 361Equation 6.45cphipval 25290  ipval 30731
[Ponnusamy] p. 362Equation I1dipcj 30742  ipcj 21669
[Ponnusamy] p. 362Equation I3cphdir 25252  dipdir 30870  ipdir 21674  ipdiri 30858
[Ponnusamy] p. 362Equation I4ipidsq 30738  nmsq 25241
[Ponnusamy] p. 362Equation 6.46ip0i 30853
[Ponnusamy] p. 362Equation 6.47ip1i 30855
[Ponnusamy] p. 362Equation 6.48ip2i 30856
[Ponnusamy] p. 363Equation I2cphass 25258  dipass 30873  ipass 21680  ipassi 30869
[Prugovecki] p. 186Definition of brabraval 31972  df-bra 31878
[Prugovecki] p. 376Equation 8.1df-kb 31879  kbval 31982
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32410
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39870
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32424  atcvat4i 32425  cvrat3 39424  cvrat4 39425  lsatcvat3 39033
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32310  cvrval 39250  df-cv 32307  df-lcv 39000  lspsncv0 21165
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39882
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39883
[Quine] p. 16Definition 2.1df-clab 2712  rabid 3454  rabidd 45097
[Quine] p. 17Definition 2.1''dfsb7 2277
[Quine] p. 18Definition 2.7df-cleq 2726
[Quine] p. 19Definition 2.9conventions 30428  df-v 3479
[Quine] p. 34Theorem 5.1eqabb 2878
[Quine] p. 35Theorem 5.2abid1 2875  abid2f 2933
[Quine] p. 40Theorem 6.1sb5 2273
[Quine] p. 40Theorem 6.2sb6 2082  sbalex 2239
[Quine] p. 41Theorem 6.3df-clel 2813
[Quine] p. 41Theorem 6.4eqid 2734  eqid1 30495
[Quine] p. 41Theorem 6.5eqcom 2741
[Quine] p. 42Theorem 6.6df-sbc 3791
[Quine] p. 42Theorem 6.7dfsbcq 3792  dfsbcq2 3793
[Quine] p. 43Theorem 6.8vex 3481
[Quine] p. 43Theorem 6.9isset 3491
[Quine] p. 44Theorem 7.3spcgf 3590  spcgv 3595  spcimgf 3549
[Quine] p. 44Theorem 6.11spsbc 3803  spsbcd 3804
[Quine] p. 44Theorem 6.12elex 3498
[Quine] p. 44Theorem 6.13elab 3680  elabg 3676  elabgf 3674
[Quine] p. 44Theorem 6.14noel 4343
[Quine] p. 48Theorem 7.2snprc 4721
[Quine] p. 48Definition 7.1df-pr 4633  df-sn 4631
[Quine] p. 49Theorem 7.4snss 4789  snssg 4787
[Quine] p. 49Theorem 7.5prss 4824  prssg 4823
[Quine] p. 49Theorem 7.6prid1 4766  prid1g 4764  prid2 4767  prid2g 4765  snid 4666  snidg 4664
[Quine] p. 51Theorem 7.12snex 5441
[Quine] p. 51Theorem 7.13prex 5442
[Quine] p. 53Theorem 8.2unisn 4930  unisnALT 44923  unisng 4929
[Quine] p. 53Theorem 8.3uniun 4934
[Quine] p. 54Theorem 8.6elssuni 4941
[Quine] p. 54Theorem 8.7uni0 4939
[Quine] p. 56Theorem 8.17uniabio 6529
[Quine] p. 56Definition 8.18dfaiota2 47035  dfiota2 6516
[Quine] p. 57Theorem 8.19aiotaval 47044  iotaval 6533
[Quine] p. 57Theorem 8.22iotanul 6540
[Quine] p. 58Theorem 8.23iotaex 6535
[Quine] p. 58Definition 9.1df-op 4637
[Quine] p. 61Theorem 9.5opabid 5534  opabidw 5533  opelopab 5551  opelopaba 5545  opelopabaf 5553  opelopabf 5554  opelopabg 5547  opelopabga 5542  opelopabgf 5549  oprabid 7462  oprabidw 7461
[Quine] p. 64Definition 9.11df-xp 5694
[Quine] p. 64Definition 9.12df-cnv 5696
[Quine] p. 64Definition 9.15df-id 5582
[Quine] p. 65Theorem 10.3fun0 6632
[Quine] p. 65Theorem 10.4funi 6599
[Quine] p. 65Theorem 10.5funsn 6620  funsng 6618
[Quine] p. 65Definition 10.1df-fun 6564
[Quine] p. 65Definition 10.2args 6112  dffv4 6903
[Quine] p. 68Definition 10.11conventions 30428  df-fv 6570  fv2 6901
[Quine] p. 124Theorem 17.3nn0opth2 14307  nn0opth2i 14306  nn0opthi 14305  omopthi 8697
[Quine] p. 177Definition 25.2df-rdg 8448
[Quine] p. 232Equation icarddom 10591
[Quine] p. 284Axiom 39(vi)funimaex 6655  funimaexg 6653
[Quine] p. 331Axiom system NFru 3788
[ReedSimon] p. 36Definition (iii)ax-his3 31112
[ReedSimon] p. 63Exercise 4(a)df-dip 30729  polid 31187  polid2i 31185  polidi 31186
[ReedSimon] p. 63Exercise 4(b)df-ph 30841
[ReedSimon] p. 195Remarklnophm 32047  lnophmi 32046
[Retherford] p. 49Exercise 1(i)leopadd 32160
[Retherford] p. 49Exercise 1(ii)leopmul 32162  leopmuli 32161
[Retherford] p. 49Exercise 1(iv)leoptr 32165
[Retherford] p. 49Definition VI.1df-leop 31880  leoppos 32154
[Retherford] p. 49Exercise 1(iii)leoptri 32164
[Retherford] p. 49Definition of operator orderingleop3 32153
[Roman] p. 4Definitiondf-dmat 22511  df-dmatalt 48243
[Roman] p. 18Part Preliminariesdf-rng 20170
[Roman] p. 19Part Preliminariesdf-ring 20252
[Roman] p. 46Theorem 1.6isldepslvec2 48330
[Roman] p. 112Noteisldepslvec2 48330  ldepsnlinc 48353  zlmodzxznm 48342
[Roman] p. 112Examplezlmodzxzequa 48341  zlmodzxzequap 48344  zlmodzxzldep 48349
[Roman] p. 170Theorem 7.8cayleyhamilton 22911
[Rosenlicht] p. 80Theoremheicant 37641
[Rosser] p. 281Definitiondf-op 4637
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34638
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34639
[Rotman] p. 28Remarkpgrpgt2nabl 48210  pmtr3ncom 19507
[Rotman] p. 31Theorem 3.4symggen2 19503
[Rotman] p. 42Theorem 3.15cayley 19446  cayleyth 19447
[Rudin] p. 164Equation 27efcan 16128
[Rudin] p. 164Equation 30efzval 16134
[Rudin] p. 167Equation 48absefi 16228
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1767
[Sanford] p. 39Rule 4mptxor 1765
[Sanford] p. 40Rule 1mptnan 1764
[Schechter] p. 51Definition of antisymmetryintasym 6137
[Schechter] p. 51Definition of irreflexivityintirr 6140
[Schechter] p. 51Definition of symmetrycnvsym 6134
[Schechter] p. 51Definition of transitivitycotr 6132
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17630
[Schechter] p. 79Definition of Moore closuredf-mrc 17631
[Schechter] p. 82Section 4.5df-mrc 17631
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17633
[Schechter] p. 139Definition AC3dfac9 10174
[Schechter] p. 141Definition (MC)dfac11 43050
[Schechter] p. 149Axiom DC1ax-dc 10483  axdc3 10491
[Schechter] p. 187Definition of "ring with unit"isring 20254  isrngo 37883
[Schechter] p. 276Remark 11.6.espan0 31570
[Schechter] p. 276Definition of spandf-span 31337  spanval 31361
[Schechter] p. 428Definition 15.35bastop1 23015
[Schloeder] p. 1Lemma 1.3onelon 6410  onelord 43239  ordelon 6409  ordelord 6407
[Schloeder] p. 1Lemma 1.7onepsuc 43240  sucidg 6466
[Schloeder] p. 1Remark 1.50elon 6439  onsuc 7830  ord0 6438  ordsuci 7827
[Schloeder] p. 1Theorem 1.9epsoon 43241
[Schloeder] p. 1Definition 1.1dftr5 5268
[Schloeder] p. 1Definition 1.2dford3 43016  elon2 6396
[Schloeder] p. 1Definition 1.4df-suc 6391
[Schloeder] p. 1Definition 1.6epel 5591  epelg 5589
[Schloeder] p. 1Theorem 1.9(i)elirr 9634  epirron 43242  ordirr 6403
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43244  oneptr 43243  ontr1 6431
[Schloeder] p. 1Theorem 1.9(iii)oneltri 43246  oneptri 43245  ordtri3or 6417
[Schloeder] p. 2Lemma 1.10ondif1 8537  ord0eln0 6440
[Schloeder] p. 2Lemma 1.13elsuci 6452  onsucss 43255  trsucss 6473
[Schloeder] p. 2Lemma 1.14ordsucss 7837
[Schloeder] p. 2Lemma 1.15onnbtwn 6479  ordnbtwn 6478
[Schloeder] p. 2Lemma 1.16orddif0suc 43257  ordnexbtwnsuc 43256
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10438  onsucf1lem 43258  onsucf1o 43261  onsucf1olem 43259  onsucrn 43260
[Schloeder] p. 2Lemma 1.18dflim7 43262
[Schloeder] p. 2Remark 1.12ordzsl 7865
[Schloeder] p. 2Theorem 1.10ondif1i 43251  ordne0gt0 43250
[Schloeder] p. 2Definition 1.11dflim6 43253  limnsuc 43254  onsucelab 43252
[Schloeder] p. 3Remark 1.21omex 9680
[Schloeder] p. 3Theorem 1.19tfinds 7880
[Schloeder] p. 3Theorem 1.22omelon 9683  ordom 7896
[Schloeder] p. 3Definition 1.20dfom3 9684
[Schloeder] p. 4Lemma 2.21onn 8676
[Schloeder] p. 4Lemma 2.7ssonuni 7798  ssorduni 7797
[Schloeder] p. 4Remark 2.4oa1suc 8567
[Schloeder] p. 4Theorem 1.23dfom5 9687  limom 7902
[Schloeder] p. 4Definition 2.1df-1o 8504  df1o2 8511
[Schloeder] p. 4Definition 2.3oa0 8552  oa0suclim 43264  oalim 8568  oasuc 8560
[Schloeder] p. 4Definition 2.5om0 8553  om0suclim 43265  omlim 8569  omsuc 8562
[Schloeder] p. 4Definition 2.6oe0 8558  oe0m1 8557  oe0suclim 43266  oelim 8570  oesuc 8563
[Schloeder] p. 5Lemma 2.10onsupuni 43217
[Schloeder] p. 5Lemma 2.11onsupsucismax 43268
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43269
[Schloeder] p. 5Lemma 2.13limexissup 43270  limexissupab 43272  limiun 43271  limuni 6446
[Schloeder] p. 5Lemma 2.14oa0r 8574
[Schloeder] p. 5Lemma 2.15om1 8578  om1om1r 43273  om1r 8579
[Schloeder] p. 5Remark 2.8oacl 8571  oaomoecl 43267  oecl 8573  omcl 8572
[Schloeder] p. 5Definition 2.9onsupintrab 43219
[Schloeder] p. 6Lemma 2.16oe1 8580
[Schloeder] p. 6Lemma 2.17oe1m 8581
[Schloeder] p. 6Lemma 2.18oe0rif 43274
[Schloeder] p. 6Theorem 2.19oasubex 43275
[Schloeder] p. 6Theorem 2.20nnacl 8647  nnamecl 43276  nnecl 8649  nnmcl 8648
[Schloeder] p. 7Lemma 3.1onsucwordi 43277
[Schloeder] p. 7Lemma 3.2oaword1 8588
[Schloeder] p. 7Lemma 3.3oaword2 8589
[Schloeder] p. 7Lemma 3.4oalimcl 8596
[Schloeder] p. 7Lemma 3.5oaltublim 43279
[Schloeder] p. 8Lemma 3.6oaordi3 43280
[Schloeder] p. 8Lemma 3.81oaomeqom 43282
[Schloeder] p. 8Lemma 3.10oa00 8595
[Schloeder] p. 8Lemma 3.11omge1 43286  omword1 8609
[Schloeder] p. 8Remark 3.9oaordnr 43285  oaordnrex 43284
[Schloeder] p. 8Theorem 3.7oaord3 43281
[Schloeder] p. 9Lemma 3.12omge2 43287  omword2 8610
[Schloeder] p. 9Lemma 3.13omlim2 43288
[Schloeder] p. 9Lemma 3.14omord2lim 43289
[Schloeder] p. 9Lemma 3.15omord2i 43290  omordi 8602
[Schloeder] p. 9Theorem 3.16omord 8604  omord2com 43291
[Schloeder] p. 10Lemma 3.172omomeqom 43292  df-2o 8505
[Schloeder] p. 10Lemma 3.19oege1 43295  oewordi 8627
[Schloeder] p. 10Lemma 3.20oege2 43296  oeworde 8629
[Schloeder] p. 10Lemma 3.21rp-oelim2 43297
[Schloeder] p. 10Lemma 3.22oeord2lim 43298
[Schloeder] p. 10Remark 3.18omnord1 43294  omnord1ex 43293
[Schloeder] p. 11Lemma 3.23oeord2i 43299
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43301
[Schloeder] p. 11Remark 3.26oenord1 43305  oenord1ex 43304
[Schloeder] p. 11Theorem 4.1oaomoencom 43306
[Schloeder] p. 11Theorem 4.2oaass 8597
[Schloeder] p. 11Theorem 3.24oeord2com 43300
[Schloeder] p. 12Theorem 4.3odi 8615
[Schloeder] p. 13Theorem 4.4omass 8616
[Schloeder] p. 14Remark 4.6oenass 43308
[Schloeder] p. 14Theorem 4.7oeoa 8633
[Schloeder] p. 15Lemma 5.1cantnftermord 43309
[Schloeder] p. 15Lemma 5.2cantnfub 43310  cantnfub2 43311
[Schloeder] p. 16Theorem 5.3cantnf2 43314
[Schwabhauser] p. 10Axiom A1axcgrrflx 28943  axtgcgrrflx 28484
[Schwabhauser] p. 10Axiom A2axcgrtr 28944
[Schwabhauser] p. 10Axiom A3axcgrid 28945  axtgcgrid 28485
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28470
[Schwabhauser] p. 11Axiom A4axsegcon 28956  axtgsegcon 28486  df-trkgcb 28472
[Schwabhauser] p. 11Axiom A5ax5seg 28967  axtg5seg 28487  df-trkgcb 28472
[Schwabhauser] p. 11Axiom A6axbtwnid 28968  axtgbtwnid 28488  df-trkgb 28471
[Schwabhauser] p. 12Axiom A7axpasch 28970  axtgpasch 28489  df-trkgb 28471
[Schwabhauser] p. 12Axiom A8axlowdim2 28989  df-trkg2d 34658
[Schwabhauser] p. 13Axiom A8axtglowdim2 28492
[Schwabhauser] p. 13Axiom A9axtgupdim2 28493  df-trkg2d 34658
[Schwabhauser] p. 13Axiom A10axeuclid 28992  axtgeucl 28494  df-trkge 28473
[Schwabhauser] p. 13Axiom A11axcont 29005  axtgcont 28491  axtgcont1 28490  df-trkgb 28471
[Schwabhauser] p. 27Theorem 2.1cgrrflx 35968
[Schwabhauser] p. 27Theorem 2.2cgrcomim 35970
[Schwabhauser] p. 27Theorem 2.3cgrtr 35973
[Schwabhauser] p. 27Theorem 2.4cgrcoml 35977
[Schwabhauser] p. 27Theorem 2.5cgrcomr 35978  tgcgrcomimp 28499  tgcgrcoml 28501  tgcgrcomr 28500
[Schwabhauser] p. 28Theorem 2.8cgrtriv 35983  tgcgrtriv 28506
[Schwabhauser] p. 28Theorem 2.105segofs 35987  tg5segofs 34666
[Schwabhauser] p. 28Definition 2.10df-afs 34663  df-ofs 35964
[Schwabhauser] p. 29Theorem 2.11cgrextend 35989  tgcgrextend 28507
[Schwabhauser] p. 29Theorem 2.12segconeq 35991  tgsegconeq 28508
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36003  btwntriv2 35993  tgbtwntriv2 28509
[Schwabhauser] p. 30Theorem 3.2btwncomim 35994  tgbtwncom 28510
[Schwabhauser] p. 30Theorem 3.3btwntriv1 35997  tgbtwntriv1 28513
[Schwabhauser] p. 30Theorem 3.4btwnswapid 35998  tgbtwnswapid 28514
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36004  btwnintr 36000  tgbtwnexch2 28518  tgbtwnintr 28515
[Schwabhauser] p. 30Theorem 3.6btwnexch 36006  btwnexch3 36001  tgbtwnexch 28520  tgbtwnexch3 28516
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36005  tgbtwnouttr 28519  tgbtwnouttr2 28517
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28988
[Schwabhauser] p. 32Theorem 3.14btwndiff 36008  tgbtwndiff 28528
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28521  trisegint 36009
[Schwabhauser] p. 34Theorem 4.2ifscgr 36025  tgifscgr 28530
[Schwabhauser] p. 34Theorem 4.11colcom 28580  colrot1 28581  colrot2 28582  lncom 28644  lnrot1 28645  lnrot2 28646
[Schwabhauser] p. 34Definition 4.1df-ifs 36021
[Schwabhauser] p. 35Theorem 4.3cgrsub 36026  tgcgrsub 28531
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36036  tgcgrxfr 28540
[Schwabhauser] p. 35Statement 4.4ercgrg 28539
[Schwabhauser] p. 35Definition 4.4df-cgr3 36022  df-cgrg 28533
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28533
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36037  tgbtwnxfr 28552
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36043  colinearperm2 36045  colinearperm3 36044  colinearperm4 36046  colinearperm5 36047
[Schwabhauser] p. 36Definition 4.8df-ismt 28555
[Schwabhauser] p. 36Definition 4.10df-colinear 36020  tgellng 28575  tglng 28568
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36048
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36056  lnxfr 28588
[Schwabhauser] p. 37Theorem 4.14lineext 36057  lnext 28589
[Schwabhauser] p. 37Theorem 4.16fscgr 36061  tgfscgr 28590
[Schwabhauser] p. 37Theorem 4.17linecgr 36062  lncgr 28591
[Schwabhauser] p. 37Definition 4.15df-fs 36023
[Schwabhauser] p. 38Theorem 4.18lineid 36064  lnid 28592
[Schwabhauser] p. 38Theorem 4.19idinside 36065  tgidinside 28593
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36082  tgbtwnconn1 28597
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36083  tgbtwnconn2 28598
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36084  tgbtwnconn3 28599
[Schwabhauser] p. 41Theorem 5.5brsegle2 36090
[Schwabhauser] p. 41Definition 5.4df-segle 36088  legov 28607
[Schwabhauser] p. 41Definition 5.5legov2 28608
[Schwabhauser] p. 42Remark 5.13legso 28621
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36091
[Schwabhauser] p. 42Theorem 5.7seglerflx 36093
[Schwabhauser] p. 42Theorem 5.8segletr 36095
[Schwabhauser] p. 42Theorem 5.9segleantisym 36096
[Schwabhauser] p. 42Theorem 5.10seglelin 36097
[Schwabhauser] p. 42Theorem 5.11seglemin 36094
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36099
[Schwabhauser] p. 42Proposition 5.7legid 28609
[Schwabhauser] p. 42Proposition 5.8legtrd 28611
[Schwabhauser] p. 42Proposition 5.9legtri3 28612
[Schwabhauser] p. 42Proposition 5.10legtrid 28613
[Schwabhauser] p. 42Proposition 5.11leg0 28614
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36106
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36107
[Schwabhauser] p. 43Theorem 6.4broutsideof 36102  df-outsideof 36101
[Schwabhauser] p. 43Definition 6.1broutsideof2 36103  ishlg 28624
[Schwabhauser] p. 44Theorem 6.4hlln 28629
[Schwabhauser] p. 44Theorem 6.5hlid 28631  outsideofrflx 36108
[Schwabhauser] p. 44Theorem 6.6hlcomb 28625  hlcomd 28626  outsideofcom 36109
[Schwabhauser] p. 44Theorem 6.7hltr 28632  outsideoftr 36110
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28640  outsideofeu 36112
[Schwabhauser] p. 44Definition 6.8df-ray 36119
[Schwabhauser] p. 45Part 2df-lines2 36120
[Schwabhauser] p. 45Theorem 6.13outsidele 36113
[Schwabhauser] p. 45Theorem 6.15lineunray 36128
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36129  tglineelsb2 28654
[Schwabhauser] p. 45Theorem 6.17linecom 36131  linerflx1 36130  linerflx2 36132  tglinecom 28657  tglinerflx1 28655  tglinerflx2 28656
[Schwabhauser] p. 45Theorem 6.18linethru 36134  tglinethru 28658
[Schwabhauser] p. 45Definition 6.14df-line2 36118  tglng 28568
[Schwabhauser] p. 45Proposition 6.13legbtwn 28616
[Schwabhauser] p. 46Theorem 6.19linethrueu 36137  tglinethrueu 28661
[Schwabhauser] p. 46Theorem 6.21lineintmo 36138  tglineineq 28665  tglineinteq 28667  tglineintmo 28664
[Schwabhauser] p. 46Theorem 6.23colline 28671
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28672
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28673
[Schwabhauser] p. 49Theorem 7.3mirinv 28688
[Schwabhauser] p. 49Theorem 7.7mirmir 28684
[Schwabhauser] p. 49Theorem 7.8mirreu3 28676
[Schwabhauser] p. 49Definition 7.5df-mir 28675  ismir 28681  mirbtwn 28680  mircgr 28679  mirfv 28678  mirval 28677
[Schwabhauser] p. 50Theorem 7.8mirreu 28686
[Schwabhauser] p. 50Theorem 7.9mireq 28687
[Schwabhauser] p. 50Theorem 7.10mirinv 28688
[Schwabhauser] p. 50Theorem 7.11mirf1o 28691
[Schwabhauser] p. 50Theorem 7.13miriso 28692
[Schwabhauser] p. 51Theorem 7.14mirmot 28697
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28694  mirbtwni 28693
[Schwabhauser] p. 51Theorem 7.16mircgrs 28695
[Schwabhauser] p. 51Theorem 7.17miduniq 28707
[Schwabhauser] p. 52Lemma 7.21symquadlem 28711
[Schwabhauser] p. 52Theorem 7.18miduniq1 28708
[Schwabhauser] p. 52Theorem 7.19miduniq2 28709
[Schwabhauser] p. 52Theorem 7.20colmid 28710
[Schwabhauser] p. 53Lemma 7.22krippen 28713
[Schwabhauser] p. 55Lemma 7.25midexlem 28714
[Schwabhauser] p. 57Theorem 8.2ragcom 28720
[Schwabhauser] p. 57Definition 8.1df-rag 28716  israg 28719
[Schwabhauser] p. 58Theorem 8.3ragcol 28721
[Schwabhauser] p. 58Theorem 8.4ragmir 28722
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28724
[Schwabhauser] p. 58Theorem 8.6ragflat2 28725
[Schwabhauser] p. 58Theorem 8.7ragflat 28726
[Schwabhauser] p. 58Theorem 8.8ragtriva 28727
[Schwabhauser] p. 58Theorem 8.9ragflat3 28728  ragncol 28731
[Schwabhauser] p. 58Theorem 8.10ragcgr 28729
[Schwabhauser] p. 59Theorem 8.12perpcom 28735
[Schwabhauser] p. 59Theorem 8.13ragperp 28739
[Schwabhauser] p. 59Theorem 8.14perpneq 28736
[Schwabhauser] p. 59Definition 8.11df-perpg 28718  isperp 28734
[Schwabhauser] p. 59Definition 8.13isperp2 28737
[Schwabhauser] p. 60Theorem 8.18foot 28744
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28752  colperpexlem2 28753
[Schwabhauser] p. 63Theorem 8.21colperpex 28755  colperpexlem3 28754
[Schwabhauser] p. 64Theorem 8.22mideu 28760  midex 28759
[Schwabhauser] p. 66Lemma 8.24opphllem 28757
[Schwabhauser] p. 67Theorem 9.2oppcom 28766
[Schwabhauser] p. 67Definition 9.1islnopp 28761
[Schwabhauser] p. 68Lemma 9.3opphllem2 28770
[Schwabhauser] p. 68Lemma 9.4opphllem5 28773  opphllem6 28774
[Schwabhauser] p. 69Theorem 9.5opphl 28776
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28489
[Schwabhauser] p. 70Theorem 9.6outpasch 28777
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28785
[Schwabhauser] p. 71Definition 9.7df-hpg 28780  hpgbr 28782
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28787
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28786
[Schwabhauser] p. 72Theorem 9.11hpgid 28788
[Schwabhauser] p. 72Theorem 9.12hpgcom 28789
[Schwabhauser] p. 72Theorem 9.13hpgtr 28790
[Schwabhauser] p. 73Theorem 9.18colopp 28791
[Schwabhauser] p. 73Theorem 9.19colhp 28792
[Schwabhauser] p. 88Theorem 10.2lmieu 28806
[Schwabhauser] p. 88Definition 10.1df-mid 28796
[Schwabhauser] p. 89Theorem 10.4lmicom 28810
[Schwabhauser] p. 89Theorem 10.5lmilmi 28811
[Schwabhauser] p. 89Theorem 10.6lmireu 28812
[Schwabhauser] p. 89Theorem 10.7lmieq 28813
[Schwabhauser] p. 89Theorem 10.8lmiinv 28814
[Schwabhauser] p. 89Theorem 10.9lmif1o 28817
[Schwabhauser] p. 89Theorem 10.10lmiiso 28819
[Schwabhauser] p. 89Definition 10.3df-lmi 28797
[Schwabhauser] p. 90Theorem 10.11lmimot 28820
[Schwabhauser] p. 91Theorem 10.12hypcgr 28823
[Schwabhauser] p. 92Theorem 10.14lmiopp 28824
[Schwabhauser] p. 92Theorem 10.15lnperpex 28825
[Schwabhauser] p. 92Theorem 10.16trgcopy 28826  trgcopyeu 28828
[Schwabhauser] p. 95Definition 11.2dfcgra2 28852
[Schwabhauser] p. 95Definition 11.3iscgra 28831
[Schwabhauser] p. 95Proposition 11.4cgracgr 28840
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28838  cgrahl2 28839
[Schwabhauser] p. 96Theorem 11.6cgraid 28841
[Schwabhauser] p. 96Theorem 11.9cgraswap 28842
[Schwabhauser] p. 97Theorem 11.7cgracom 28844
[Schwabhauser] p. 97Theorem 11.8cgratr 28845
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28848  cgrahl 28849
[Schwabhauser] p. 98Theorem 11.13sacgr 28853
[Schwabhauser] p. 98Theorem 11.14oacgr 28854
[Schwabhauser] p. 98Theorem 11.15acopy 28855  acopyeu 28856
[Schwabhauser] p. 101Theorem 11.24inagswap 28863
[Schwabhauser] p. 101Theorem 11.25inaghl 28867
[Schwabhauser] p. 101Definition 11.23isinag 28860
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28875
[Schwabhauser] p. 102Definition 11.27df-leag 28868  isleag 28869
[Schwabhauser] p. 107Theorem 11.49tgsas 28877  tgsas1 28876  tgsas2 28878  tgsas3 28879
[Schwabhauser] p. 108Theorem 11.50tgasa 28881  tgasa1 28880
[Schwabhauser] p. 109Theorem 11.51tgsss1 28882  tgsss2 28883  tgsss3 28884
[Shapiro] p. 230Theorem 6.5.1dchrhash 27329  dchrsum 27327  dchrsum2 27326  sumdchr 27330
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27331  sum2dchr 27332
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20100  ablfacrp2 20101
[Shapiro], p. 328Equation 9.2.4vmasum 27274
[Shapiro], p. 329Equation 9.2.7logfac2 27275
[Shapiro], p. 329Equation 9.2.9logfacrlim 27282
[Shapiro], p. 331Equation 9.2.13vmadivsum 27540
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27543
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27597  vmalogdivsum2 27596
[Shapiro], p. 375Theorem 9.4.1dirith 27587  dirith2 27586
[Shapiro], p. 375Equation 9.4.3rplogsum 27585  rpvmasum 27584  rpvmasum2 27570
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27545
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27583
[Shapiro], p. 377Lemma 9.4.1dchrisum 27550  dchrisumlem1 27547  dchrisumlem2 27548  dchrisumlem3 27549  dchrisumlema 27546
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27553
[Shapiro], p. 379Equation 9.4.16dchrmusum 27582  dchrmusumlem 27580  dchrvmasumlem 27581
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27552
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27554
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27578  dchrisum0re 27571  dchrisumn0 27579
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27564
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27568
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27569
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27624  pntrsumbnd2 27625  pntrsumo1 27623
[Shapiro], p. 405Equation 10.2.1mudivsum 27588
[Shapiro], p. 406Equation 10.2.6mulogsum 27590
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27592
[Shapiro], p. 407Equation 10.2.8mulog2sum 27595
[Shapiro], p. 418Equation 10.4.6logsqvma 27600
[Shapiro], p. 418Equation 10.4.8logsqvma2 27601
[Shapiro], p. 419Equation 10.4.10selberg 27606
[Shapiro], p. 420Equation 10.4.12selberg2lem 27608
[Shapiro], p. 420Equation 10.4.14selberg2 27609
[Shapiro], p. 422Equation 10.6.7selberg3 27617
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27618
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27615  selberg3lem2 27616
[Shapiro], p. 422Equation 10.4.23selberg4 27619
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27613
[Shapiro], p. 428Equation 10.6.2selbergr 27626
[Shapiro], p. 429Equation 10.6.8selberg3r 27627
[Shapiro], p. 430Equation 10.6.11selberg4r 27628
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27642
[Shapiro], p. 434Equation 10.6.27pntlema 27654  pntlemb 27655  pntlemc 27653  pntlemd 27652  pntlemg 27656
[Shapiro], p. 435Equation 10.6.29pntlema 27654
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27646
[Shapiro], p. 436Lemma 10.6.2pntibnd 27651
[Shapiro], p. 436Equation 10.6.34pntlema 27654
[Shapiro], p. 436Equation 10.6.35pntlem3 27667  pntleml 27669
[Stoll] p. 13Definition corresponds to dfsymdif3 4311
[Stoll] p. 16Exercise 4.40dif 4410  dif0 4383
[Stoll] p. 16Exercise 4.8difdifdir 4497
[Stoll] p. 17Theorem 5.1(5)unvdif 4480
[Stoll] p. 19Theorem 5.2(13)undm 4302
[Stoll] p. 19Theorem 5.2(13')indm 4303
[Stoll] p. 20Remarkinvdif 4284
[Stoll] p. 25Definition of ordered tripledf-ot 4639
[Stoll] p. 43Definitionuniiun 5062
[Stoll] p. 44Definitionintiin 5063
[Stoll] p. 45Definitiondf-iin 4998
[Stoll] p. 45Definition indexed uniondf-iun 4997
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4311
[Strang] p. 242Section 6.3expgrowth 44330
[Suppes] p. 22Theorem 2eq0 4355  eq0f 4352
[Suppes] p. 22Theorem 4eqss 4010  eqssd 4012  eqssi 4011
[Suppes] p. 23Theorem 5ss0 4407  ss0b 4406
[Suppes] p. 23Theorem 6sstr 4003  sstrALT2 44832
[Suppes] p. 23Theorem 7pssirr 4112
[Suppes] p. 23Theorem 8pssn2lp 4113
[Suppes] p. 23Theorem 9psstr 4116
[Suppes] p. 23Theorem 10pssss 4107
[Suppes] p. 25Theorem 12elin 3978  elun 4162
[Suppes] p. 26Theorem 15inidm 4234
[Suppes] p. 26Theorem 16in0 4400
[Suppes] p. 27Theorem 23unidm 4166
[Suppes] p. 27Theorem 24un0 4399
[Suppes] p. 27Theorem 25ssun1 4187
[Suppes] p. 27Theorem 26ssequn1 4195
[Suppes] p. 27Theorem 27unss 4199
[Suppes] p. 27Theorem 28indir 4291
[Suppes] p. 27Theorem 29undir 4292
[Suppes] p. 28Theorem 32difid 4381
[Suppes] p. 29Theorem 33difin 4277
[Suppes] p. 29Theorem 34indif 4285
[Suppes] p. 29Theorem 35undif1 4481
[Suppes] p. 29Theorem 36difun2 4486
[Suppes] p. 29Theorem 37difin0 4479
[Suppes] p. 29Theorem 38disjdif 4477
[Suppes] p. 29Theorem 39difundi 4295
[Suppes] p. 29Theorem 40difindi 4297
[Suppes] p. 30Theorem 41nalset 5318
[Suppes] p. 39Theorem 61uniss 4919
[Suppes] p. 39Theorem 65uniop 5524
[Suppes] p. 41Theorem 70intsn 4988
[Suppes] p. 42Theorem 71intpr 4986  intprg 4985
[Suppes] p. 42Theorem 73op1stb 5481
[Suppes] p. 42Theorem 78intun 4984
[Suppes] p. 44Definition 15(a)dfiun2 5037  dfiun2g 5034
[Suppes] p. 44Definition 15(b)dfiin2 5038
[Suppes] p. 47Theorem 86elpw 4608  elpw2 5339  elpw2g 5338  elpwg 4607  elpwgdedVD 44914
[Suppes] p. 47Theorem 87pwid 4626
[Suppes] p. 47Theorem 89pw0 4816
[Suppes] p. 48Theorem 90pwpw0 4817
[Suppes] p. 52Theorem 101xpss12 5703
[Suppes] p. 52Theorem 102xpindi 5846  xpindir 5847
[Suppes] p. 52Theorem 103xpundi 5756  xpundir 5757
[Suppes] p. 54Theorem 105elirrv 9633
[Suppes] p. 58Theorem 2relss 5793
[Suppes] p. 59Theorem 4eldm 5913  eldm2 5914  eldm2g 5912  eldmg 5911
[Suppes] p. 59Definition 3df-dm 5698
[Suppes] p. 60Theorem 6dmin 5924
[Suppes] p. 60Theorem 8rnun 6167
[Suppes] p. 60Theorem 9rnin 6168
[Suppes] p. 60Definition 4dfrn2 5901
[Suppes] p. 61Theorem 11brcnv 5895  brcnvg 5892
[Suppes] p. 62Equation 5elcnv 5889  elcnv2 5890
[Suppes] p. 62Theorem 12relcnv 6124
[Suppes] p. 62Theorem 15cnvin 6166
[Suppes] p. 62Theorem 16cnvun 6164
[Suppes] p. 63Definitiondftrrels2 38556
[Suppes] p. 63Theorem 20co02 6281
[Suppes] p. 63Theorem 21dmcoss 5987
[Suppes] p. 63Definition 7df-co 5697
[Suppes] p. 64Theorem 26cnvco 5898
[Suppes] p. 64Theorem 27coass 6286
[Suppes] p. 65Theorem 31resundi 6013
[Suppes] p. 65Theorem 34elima 6084  elima2 6085  elima3 6086  elimag 6083
[Suppes] p. 65Theorem 35imaundi 6171
[Suppes] p. 66Theorem 40dminss 6174
[Suppes] p. 66Theorem 41imainss 6175
[Suppes] p. 67Exercise 11cnvxp 6178
[Suppes] p. 81Definition 34dfec2 8746
[Suppes] p. 82Theorem 72elec 8789  elecALTV 38247  elecg 8787
[Suppes] p. 82Theorem 73eqvrelth 38592  erth 8794  erth2 8795
[Suppes] p. 83Theorem 74eqvreldisj 38595  erdisj 8797
[Suppes] p. 83Definition 35, df-parts 38746  dfmembpart2 38751
[Suppes] p. 89Theorem 96map0b 8921
[Suppes] p. 89Theorem 97map0 8925  map0g 8922
[Suppes] p. 89Theorem 98mapsn 8926  mapsnd 8924
[Suppes] p. 89Theorem 99mapss 8927
[Suppes] p. 91Definition 12(ii)alephsuc 10105
[Suppes] p. 91Definition 12(iii)alephlim 10104
[Suppes] p. 92Theorem 1enref 9023  enrefg 9022
[Suppes] p. 92Theorem 2ensym 9041  ensymb 9040  ensymi 9042
[Suppes] p. 92Theorem 3entr 9044
[Suppes] p. 92Theorem 4unen 9084
[Suppes] p. 94Theorem 15endom 9017
[Suppes] p. 94Theorem 16ssdomg 9038
[Suppes] p. 94Theorem 17domtr 9045
[Suppes] p. 95Theorem 18sbth 9131
[Suppes] p. 97Theorem 23canth2 9168  canth2g 9169
[Suppes] p. 97Definition 3brsdom2 9135  df-sdom 8986  dfsdom2 9134
[Suppes] p. 97Theorem 21(i)sdomirr 9152
[Suppes] p. 97Theorem 22(i)domnsym 9137
[Suppes] p. 97Theorem 21(ii)sdomnsym 9136
[Suppes] p. 97Theorem 22(ii)domsdomtr 9150
[Suppes] p. 97Theorem 22(iv)brdom2 9020
[Suppes] p. 97Theorem 21(iii)sdomtr 9153
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9148
[Suppes] p. 98Exercise 4fundmen 9069  fundmeng 9070
[Suppes] p. 98Exercise 6xpdom3 9108
[Suppes] p. 98Exercise 11sdomentr 9149
[Suppes] p. 104Theorem 37fofi 9348
[Suppes] p. 104Theorem 38pwfi 9354
[Suppes] p. 105Theorem 40pwfi 9354
[Suppes] p. 111Axiom for cardinal numberscarden 10588
[Suppes] p. 130Definition 3df-tr 5265
[Suppes] p. 132Theorem 9ssonuni 7798
[Suppes] p. 134Definition 6df-suc 6391
[Suppes] p. 136Theorem Schema 22findes 7922  finds 7918  finds1 7921  finds2 7920
[Suppes] p. 151Theorem 42isfinite 9689  isfinite2 9331  isfiniteg 9334  unbnn 9329
[Suppes] p. 162Definition 5df-ltnq 10955  df-ltpq 10947
[Suppes] p. 197Theorem Schema 4tfindes 7883  tfinds 7880  tfinds2 7884
[Suppes] p. 209Theorem 18oaord1 8587
[Suppes] p. 209Theorem 21oaword2 8589
[Suppes] p. 211Theorem 25oaass 8597
[Suppes] p. 225Definition 8iscard2 10013
[Suppes] p. 227Theorem 56ondomon 10600
[Suppes] p. 228Theorem 59harcard 10015
[Suppes] p. 228Definition 12(i)aleph0 10103
[Suppes] p. 228Theorem Schema 61onintss 6436
[Suppes] p. 228Theorem Schema 62onminesb 7812  onminsb 7813
[Suppes] p. 229Theorem 64alephval2 10609
[Suppes] p. 229Theorem 65alephcard 10107
[Suppes] p. 229Theorem 66alephord2i 10114
[Suppes] p. 229Theorem 67alephnbtwn 10108
[Suppes] p. 229Definition 12df-aleph 9977
[Suppes] p. 242Theorem 6weth 10532
[Suppes] p. 242Theorem 8entric 10594
[Suppes] p. 242Theorem 9carden 10588
[Szendrei] p. 11Line 6df-cloneop 35675
[Szendrei] p. 11Paragraph 3df-suppos 35679
[TakeutiZaring] p. 8Axiom 1ax-ext 2705
[TakeutiZaring] p. 13Definition 4.5df-cleq 2726
[TakeutiZaring] p. 13Proposition 4.6df-clel 2813
[TakeutiZaring] p. 13Proposition 4.9cvjust 2728
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2757
[TakeutiZaring] p. 14Definition 4.16df-oprab 7434
[TakeutiZaring] p. 14Proposition 4.14ru 3788
[TakeutiZaring] p. 15Axiom 2zfpair 5426
[TakeutiZaring] p. 15Exercise 1elpr 4654  elpr2 4656  elpr2g 4655  elprg 4652
[TakeutiZaring] p. 15Exercise 2elsn 4645  elsn2 4669  elsn2g 4668  elsng 4644  velsn 4646
[TakeutiZaring] p. 15Exercise 3elop 5477
[TakeutiZaring] p. 15Exercise 4sneq 4640  sneqr 4844
[TakeutiZaring] p. 15Definition 5.1dfpr2 4650  dfsn2 4643  dfsn2ALT 4651
[TakeutiZaring] p. 16Axiom 3uniex 7759
[TakeutiZaring] p. 16Exercise 6opth 5486
[TakeutiZaring] p. 16Exercise 7opex 5474
[TakeutiZaring] p. 16Exercise 8rext 5458
[TakeutiZaring] p. 16Corollary 5.8unex 7762  unexg 7761
[TakeutiZaring] p. 16Definition 5.3dftp2 4695
[TakeutiZaring] p. 16Definition 5.5df-uni 4912
[TakeutiZaring] p. 16Definition 5.6df-in 3969  df-un 3967
[TakeutiZaring] p. 16Proposition 5.7unipr 4928  uniprg 4927
[TakeutiZaring] p. 17Axiom 4vpwex 5382
[TakeutiZaring] p. 17Exercise 1eltp 4693
[TakeutiZaring] p. 17Exercise 5elsuc 6455  elsucg 6453  sstr2 4001
[TakeutiZaring] p. 17Exercise 6uncom 4167
[TakeutiZaring] p. 17Exercise 7incom 4216
[TakeutiZaring] p. 17Exercise 8unass 4181
[TakeutiZaring] p. 17Exercise 9inass 4235
[TakeutiZaring] p. 17Exercise 10indi 4289
[TakeutiZaring] p. 17Exercise 11undi 4290
[TakeutiZaring] p. 17Definition 5.9df-pss 3982  df-ss 3979
[TakeutiZaring] p. 17Definition 5.10df-pw 4606
[TakeutiZaring] p. 18Exercise 7unss2 4196
[TakeutiZaring] p. 18Exercise 9dfss2 3980  sseqin2 4230
[TakeutiZaring] p. 18Exercise 10ssid 4017
[TakeutiZaring] p. 18Exercise 12inss1 4244  inss2 4245
[TakeutiZaring] p. 18Exercise 13nss 4059
[TakeutiZaring] p. 18Exercise 15unieq 4922
[TakeutiZaring] p. 18Exercise 18sspwb 5459  sspwimp 44915  sspwimpALT 44922  sspwimpALT2 44925  sspwimpcf 44917
[TakeutiZaring] p. 18Exercise 19pweqb 5466
[TakeutiZaring] p. 19Axiom 5ax-rep 5284
[TakeutiZaring] p. 20Definitiondf-rab 3433
[TakeutiZaring] p. 20Corollary 5.160ex 5312
[TakeutiZaring] p. 20Definition 5.12df-dif 3965
[TakeutiZaring] p. 20Definition 5.14dfnul2 4341
[TakeutiZaring] p. 20Proposition 5.15difid 4381
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4358  n0f 4354  neq0 4357  neq0f 4353
[TakeutiZaring] p. 21Axiom 6zfreg 9632
[TakeutiZaring] p. 21Axiom 6'zfregs 9769
[TakeutiZaring] p. 21Theorem 5.22setind 9771
[TakeutiZaring] p. 21Definition 5.20df-v 3479
[TakeutiZaring] p. 21Proposition 5.21vprc 5320
[TakeutiZaring] p. 22Exercise 10ss 4405
[TakeutiZaring] p. 22Exercise 3ssex 5326  ssexg 5328
[TakeutiZaring] p. 22Exercise 4inex1 5322
[TakeutiZaring] p. 22Exercise 5ruv 9639
[TakeutiZaring] p. 22Exercise 6elirr 9634
[TakeutiZaring] p. 22Exercise 7ssdif0 4371
[TakeutiZaring] p. 22Exercise 11difdif 4144
[TakeutiZaring] p. 22Exercise 13undif3 4305  undif3VD 44879
[TakeutiZaring] p. 22Exercise 14difss 4145
[TakeutiZaring] p. 22Exercise 15sscon 4152
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3059
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3068
[TakeutiZaring] p. 23Proposition 6.2xpex 7771  xpexg 7768
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5695
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6638
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6813  fun11 6641
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6578  svrelfun 6639
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5900
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5902
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5700
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5701
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5697
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6215  dfrel2 6210
[TakeutiZaring] p. 25Exercise 3xpss 5704
[TakeutiZaring] p. 25Exercise 5relun 5823
[TakeutiZaring] p. 25Exercise 6reluni 5830
[TakeutiZaring] p. 25Exercise 9inxp 5844
[TakeutiZaring] p. 25Exercise 12relres 6025
[TakeutiZaring] p. 25Exercise 13opelres 6005  opelresi 6007
[TakeutiZaring] p. 25Exercise 14dmres 6031
[TakeutiZaring] p. 25Exercise 15resss 6021
[TakeutiZaring] p. 25Exercise 17resabs1 6026
[TakeutiZaring] p. 25Exercise 18funres 6609
[TakeutiZaring] p. 25Exercise 24relco 6128
[TakeutiZaring] p. 25Exercise 29funco 6607
[TakeutiZaring] p. 25Exercise 30f1co 6815
[TakeutiZaring] p. 26Definition 6.10eu2 2606
[TakeutiZaring] p. 26Definition 6.11conventions 30428  df-fv 6570  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 44449
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7942
[TakeutiZaring] p. 27Corollary 6.13fvex 6919
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47123  tz6.12-1-afv2 47190  tz6.12-1 6929  tz6.12-afv 47122  tz6.12-afv2 47189  tz6.12 6931  tz6.12c-afv2 47191  tz6.12c 6928
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47186  tz6.12-2 6894  tz6.12i-afv2 47192  tz6.12i 6934
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6565
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6566
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6568  wfo 6560
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6567  wf1 6559
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6569  wf1o 6561
[TakeutiZaring] p. 28Exercise 4eqfnfv 7050  eqfnfv2 7051  eqfnfv2f 7054
[TakeutiZaring] p. 28Exercise 5fvco 7006
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7236
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7234
[TakeutiZaring] p. 29Exercise 9funimaex 6655  funimaexg 6653
[TakeutiZaring] p. 29Definition 6.18df-br 5148
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5597
[TakeutiZaring] p. 30Definition 6.21dffr2 5649  dffr3 6119  eliniseg 6114  iniseg 6117
[TakeutiZaring] p. 30Definition 6.22df-eprel 5588
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5665  fr3nr 7790  frirr 5664
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5640
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7792
[TakeutiZaring] p. 31Exercise 1frss 5652
[TakeutiZaring] p. 31Exercise 4wess 5674
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6369  tz6.26i 6371  wefrc 5682  wereu2 5685
[TakeutiZaring] p. 32Theorem 6.27wfi 6372  wfii 6374
[TakeutiZaring] p. 32Definition 6.28df-isom 6571
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7348
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7349
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7355
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7356
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7357
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7361
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7368
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7370
[TakeutiZaring] p. 35Notationwtr 5264
[TakeutiZaring] p. 35Theorem 7.2trelpss 44450  tz7.2 5671
[TakeutiZaring] p. 35Definition 7.1dftr3 5270
[TakeutiZaring] p. 36Proposition 7.4ordwe 6398
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6406
[TakeutiZaring] p. 36Proposition 7.6ordelord 6407  ordelordALT 44534  ordelordALTVD 44864
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6413  ordelssne 6412
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6411
[TakeutiZaring] p. 37Proposition 7.9ordin 6415
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7800
[TakeutiZaring] p. 38Corollary 7.15ordsson 7801
[TakeutiZaring] p. 38Definition 7.11df-on 6389
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6417
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44546  ordon 7795
[TakeutiZaring] p. 38Proposition 7.13onprc 7796
[TakeutiZaring] p. 39Theorem 7.17tfi 7873
[TakeutiZaring] p. 40Exercise 3ontr2 6432
[TakeutiZaring] p. 40Exercise 7dftr2 5266
[TakeutiZaring] p. 40Exercise 9onssmin 7811
[TakeutiZaring] p. 40Exercise 11unon 7850
[TakeutiZaring] p. 40Exercise 12ordun 6489
[TakeutiZaring] p. 40Exercise 14ordequn 6488
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7797
[TakeutiZaring] p. 40Proposition 7.20elssuni 4941
[TakeutiZaring] p. 41Definition 7.22df-suc 6391
[TakeutiZaring] p. 41Proposition 7.23sssucid 6465  sucidg 6466
[TakeutiZaring] p. 41Proposition 7.24onsuc 7830
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6479  ordnbtwn 6478
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7847
[TakeutiZaring] p. 42Exercise 1df-lim 6390
[TakeutiZaring] p. 42Exercise 4omssnlim 7901
[TakeutiZaring] p. 42Exercise 7ssnlim 7906
[TakeutiZaring] p. 42Exercise 8onsucssi 7861  ordelsuc 7839
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7841
[TakeutiZaring] p. 42Definition 7.27nlimon 7871
[TakeutiZaring] p. 42Definition 7.28dfom2 7888
[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 7898
[TakeutiZaring] p. 43Axiom 7inf3 9672  omex 9680
[TakeutiZaring] p. 43Theorem 7.32ordom 7896
[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 7891
[TakeutiZaring] p. 44Exercise 2int0 4966
[TakeutiZaring] p. 44Exercise 3trintss 5283
[TakeutiZaring] p. 44Exercise 4intss1 4967
[TakeutiZaring] p. 44Exercise 5intex 5349
[TakeutiZaring] p. 44Exercise 6oninton 7814
[TakeutiZaring] p. 44Exercise 11ordintdif 6435
[TakeutiZaring] p. 44Definition 7.35df-int 4951
[TakeutiZaring] p. 44Proposition 7.34noinfep 9697
[TakeutiZaring] p. 45Exercise 4onint 7809
[TakeutiZaring] p. 47Lemma 1tfrlem1 8414
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8435
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8436
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8437
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8444  tz7.44-2 8445  tz7.44-3 8446
[TakeutiZaring] p. 50Exercise 1smogt 8405
[TakeutiZaring] p. 50Exercise 3smoiso 8400
[TakeutiZaring] p. 50Definition 7.46df-smo 8384
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8483  tz7.49c 8484
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8481
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8480
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8482
[TakeutiZaring] p. 53Proposition 7.532eu5 2653
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10048
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10049
[TakeutiZaring] p. 56Definition 8.1oalim 8568  oasuc 8560
[TakeutiZaring] p. 57Remarktfindsg 7881
[TakeutiZaring] p. 57Proposition 8.2oacl 8571
[TakeutiZaring] p. 57Proposition 8.3oa0 8552  oa0r 8574
[TakeutiZaring] p. 57Proposition 8.16omcl 8572
[TakeutiZaring] p. 58Corollary 8.5oacan 8584
[TakeutiZaring] p. 58Proposition 8.4nnaord 8655  nnaordi 8654  oaord 8583  oaordi 8582
[TakeutiZaring] p. 59Proposition 8.6iunss2 5053  uniss2 4945
[TakeutiZaring] p. 59Proposition 8.7oawordri 8586
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8591  oawordex 8593
[TakeutiZaring] p. 59Proposition 8.9nnacl 8647
[TakeutiZaring] p. 59Proposition 8.10oaabs 8684
[TakeutiZaring] p. 60Remarkoancom 9688
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8596
[TakeutiZaring] p. 62Exercise 1nnarcl 8652
[TakeutiZaring] p. 62Exercise 5oaword1 8588
[TakeutiZaring] p. 62Definition 8.15om0x 8555  omlim 8569  omsuc 8562
[TakeutiZaring] p. 62Definition 8.15(a)om0 8553
[TakeutiZaring] p. 63Proposition 8.17nnecl 8649  nnmcl 8648
[TakeutiZaring] p. 63Proposition 8.19nnmord 8668  nnmordi 8667  omord 8604  omordi 8602
[TakeutiZaring] p. 63Proposition 8.20omcan 8605
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8672  omwordri 8608
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8575
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8578  om1r 8579
[TakeutiZaring] p. 64Proposition 8.22om00 8611
[TakeutiZaring] p. 64Proposition 8.23omordlim 8613
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8614
[TakeutiZaring] p. 64Proposition 8.25odi 8615
[TakeutiZaring] p. 65Theorem 8.26omass 8616
[TakeutiZaring] p. 67Definition 8.30nnesuc 8644  oe0 8558  oelim 8570  oesuc 8563  onesuc 8566
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8556
[TakeutiZaring] p. 67Proposition 8.32oen0 8622
[TakeutiZaring] p. 67Proposition 8.33oeordi 8623
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8557
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8581
[TakeutiZaring] p. 68Corollary 8.34oeord 8624
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8630
[TakeutiZaring] p. 68Proposition 8.35oewordri 8628
[TakeutiZaring] p. 68Proposition 8.37oeworde 8629
[TakeutiZaring] p. 69Proposition 8.41oeoa 8633
[TakeutiZaring] p. 70Proposition 8.42oeoe 8635
[TakeutiZaring] p. 73Theorem 9.1trcl 9765  tz9.1 9766
[TakeutiZaring] p. 76Definition 9.9df-r1 9801  r10 9805  r1lim 9809  r1limg 9808  r1suc 9807  r1sucg 9806
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9817  r1ord2 9818  r1ordg 9815
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9827
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9852  tz9.13 9828  tz9.13g 9829
[TakeutiZaring] p. 79Definition 9.14df-rank 9802  rankval 9853  rankvalb 9834  rankvalg 9854
[TakeutiZaring] p. 79Proposition 9.16rankel 9876  rankelb 9861
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9890  rankval3 9877  rankval3b 9863
[TakeutiZaring] p. 79Proposition 9.18rankonid 9866
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9832
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9871  rankr1c 9858  rankr1g 9869
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9872
[TakeutiZaring] p. 80Exercise 1rankss 9886  rankssb 9885
[TakeutiZaring] p. 80Exercise 2unbndrank 9879
[TakeutiZaring] p. 80Proposition 9.19bndrank 9878
[TakeutiZaring] p. 83Axiom of Choiceac4 10512  dfac3 10158
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10067  numth 10509  numth2 10508
[TakeutiZaring] p. 85Definition 10.4cardval 10583
[TakeutiZaring] p. 85Proposition 10.5cardid 10584  cardid2 9990
[TakeutiZaring] p. 85Proposition 10.9oncard 9997
[TakeutiZaring] p. 85Proposition 10.10carden 10588
[TakeutiZaring] p. 85Proposition 10.11cardidm 9996
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9981
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 10002
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9994
[TakeutiZaring] p. 87Proposition 10.15pwen 9188
[TakeutiZaring] p. 88Exercise 1en0 9056
[TakeutiZaring] p. 88Exercise 7infensuc 9193
[TakeutiZaring] p. 89Exercise 10omxpen 9112
[TakeutiZaring] p. 90Corollary 10.23cardnn 10000
[TakeutiZaring] p. 90Definition 10.27alephiso 10135
[TakeutiZaring] p. 90Proposition 10.20nneneq 9243
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9262
[TakeutiZaring] p. 90Proposition 10.26alephprc 10136
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9248
[TakeutiZaring] p. 91Exercise 2alephle 10125
[TakeutiZaring] p. 91Exercise 3aleph0 10103
[TakeutiZaring] p. 91Exercise 4cardlim 10009
[TakeutiZaring] p. 91Exercise 7infpss 10253
[TakeutiZaring] p. 91Exercise 8infcntss 9359
[TakeutiZaring] p. 91Definition 10.29df-fin 8987  isfi 9014
[TakeutiZaring] p. 92Proposition 10.32onfin 9264
[TakeutiZaring] p. 92Proposition 10.34imadomg 10571
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9105
[TakeutiZaring] p. 93Proposition 10.35fodomb 10563
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10223  unxpdom 9286
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 10011  cardsdomelir 10010
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9288
[TakeutiZaring] p. 94Proposition 10.39infxpen 10051
[TakeutiZaring] p. 95Definition 10.42df-map 8866
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10599  infxpidm2 10054
[TakeutiZaring] p. 95Proposition 10.41infdju 10244  infxp 10251
[TakeutiZaring] p. 96Proposition 10.44pw2en 9117  pw2f1o 9115
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9181
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10524
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10519  ac6s5 10528
[TakeutiZaring] p. 98Theorem 10.47unidom 10580
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10581  uniimadomf 10582
[TakeutiZaring] p. 100Definition 11.1cfcof 10311
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10306
[TakeutiZaring] p. 102Exercise 1cfle 10291
[TakeutiZaring] p. 102Exercise 2cf0 10288
[TakeutiZaring] p. 102Exercise 3cfsuc 10294
[TakeutiZaring] p. 102Exercise 4cfom 10301
[TakeutiZaring] p. 102Proposition 11.9coftr 10310
[TakeutiZaring] p. 103Theorem 11.15alephreg 10619
[TakeutiZaring] p. 103Proposition 11.11cardcf 10289
[TakeutiZaring] p. 103Proposition 11.13alephsing 10313
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10134
[TakeutiZaring] p. 104Proposition 11.16carduniima 10133
[TakeutiZaring] p. 104Proposition 11.18alephfp 10145  alephfp2 10146
[TakeutiZaring] p. 106Theorem 11.20gchina 10736
[TakeutiZaring] p. 106Theorem 11.21mappwen 10149
[TakeutiZaring] p. 107Theorem 11.26konigth 10606
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10620
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10621
[Tarski] p. 67Axiom B5ax-c5 38864
[Tarski] p. 67Scheme B5sp 2180
[Tarski] p. 68Lemma 6avril1 30491  equid 2008
[Tarski] p. 69Lemma 7equcomi 2013
[Tarski] p. 70Lemma 14spim 2389  spime 2391  spimew 1968
[Tarski] p. 70Lemma 16ax-12 2174  ax-c15 38870  ax12i 1963
[Tarski] p. 70Lemmas 16 and 17sb6 2082
[Tarski] p. 75Axiom B7ax6v 1965
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1907  ax5ALT 38888
[Tarski], p. 75Scheme B8 of system S2ax-7 2004  ax-8 2107  ax-9 2115
[Tarski1999] p. 178Axiom 4axtgsegcon 28486
[Tarski1999] p. 178Axiom 5axtg5seg 28487
[Tarski1999] p. 179Axiom 7axtgpasch 28489
[Tarski1999] p. 180Axiom 7.1axtgpasch 28489
[Tarski1999] p. 185Axiom 11axtgcont1 28490
[Truss] p. 114Theorem 5.18ruc 16275
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37645
[Viaclovsky8] p. 3Proposition 7ismblfin 37647
[Weierstrass] p. 272Definitiondf-mdet 22606  mdetuni 22643
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 903
[WhiteheadRussell] p. 96Axiom *1.3olc 868
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 869
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 919
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 969
[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 37427
[WhiteheadRussell] p. 100Theorem *2.05frege5 43789  imim2 58  wl-luk-imim2 37422
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 46968  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2660  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37425
[WhiteheadRussell] p. 101Theorem *2.11exmid 894
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 897
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 44924  wl-luk-notnotr 37426
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43819  axfrege28 43818  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 867
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 924
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37419
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 889
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 941
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30429  pm2.27 42  wl-luk-pm2.27 37417
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38344
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 923
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 971
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 972
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 970
[WhiteheadRussell] p. 105Definition *2.33df-3or 1087
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 906
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 907
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 944
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 881
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 882
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 191
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 883
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 884
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 885
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 851
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 852
[WhiteheadRussell] p. 107Theorem *2.55orel1 888
[WhiteheadRussell] p. 107Theorem *2.56orel2 890
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 899
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 942
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 943
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 891  pm2.67 892
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 898
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 974
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 900
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 975
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 976
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 933
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 931
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 973
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 977
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 932
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 993
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 994
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 995
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 996
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 997
[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 962  pm3.44 961
[WhiteheadRussell] p. 113Theorem *3.47anim12 809
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 965
[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 904  pm4.25 905
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1009
[WhiteheadRussell] p. 118Theorem *4.31orcom 870
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[WhiteheadRussell] p. 118Theorem *4.33orass 921
[WhiteheadRussell] p. 118Theorem *4.36anbi1 633
[WhiteheadRussell] p. 118Theorem *4.37orbi1 917
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 637
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 978
[WhiteheadRussell] p. 118Definition *4.34df-3an 1088
[WhiteheadRussell] p. 119Theorem *4.41ordi 1007
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1053
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1024
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 998
[WhiteheadRussell] p. 119Theorem *4.45orabs 1000  pm4.45 999  pm4.45im 828
[WhiteheadRussell] p. 120Theorem *4.5anor 984
[WhiteheadRussell] p. 120Theorem *4.6imor 853
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 983
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 986
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 987
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 988
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 989
[WhiteheadRussell] p. 120Theorem *4.56ioran 985  pm4.56 990
[WhiteheadRussell] p. 120Theorem *4.57oran 991  pm4.57 992
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 856
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 849
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 850
[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 951
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 936
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 963  pm4.77 964
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 934
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1005
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1025
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1026
[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 843
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 824
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 946  pm5.11g 945
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 947
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 949
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 948
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1014
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1015
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1013
[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 1016
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1049
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1050
[WhiteheadRussell] p. 124Theorem *5.25dfor2 901
[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 1003
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 955
[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 1006
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1019
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 950
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1002
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1020
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1021
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1029
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1030
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44353
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44354
[WhiteheadRussell] p. 147Theorem *10.2219.26 1867
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44355
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44356
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44357
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1890
[WhiteheadRussell] p. 151Theorem *10.301albitr 44358
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44359
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44360
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44361
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44362
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44364
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44365
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44366
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44363
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2087
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44369
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44370
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2067
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2157
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1825
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1826
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44371
[WhiteheadRussell] p. 162Theorem *11.322alim 44372
[WhiteheadRussell] p. 162Theorem *11.332albi 44373
[WhiteheadRussell] p. 162Theorem *11.342exim 44374
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44376
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44375
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1884
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44378
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44379
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44377
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1824
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44380
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44381
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1842
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44382
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2346
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1857
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44387
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44383
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44384
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44385
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44386
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44391
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44388
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44389
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44390
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44392
[WhiteheadRussell] p. 175Definition *14.02df-eu 2566
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44402  pm13.13b 44403
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44404
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3019
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3020
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3665
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44410
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44411
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44405
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44549  pm13.193 44406
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44407
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44408
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44409
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44416
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44415
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44414
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3858
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44417  pm14.122b 44418  pm14.122c 44419
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44420  pm14.123b 44421  pm14.123c 44422
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44424
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44423
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44425
[WhiteheadRussell] p. 190Theorem *14.22iota4 6543
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44426
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6544
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44427
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44429
[WhiteheadRussell] p. 192Theorem *14.26eupick 2630  eupickbi 2633  sbaniota 44430
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44428
[WhiteheadRussell] p. 192Theorem *14.271eubi 2581
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44432
[WhiteheadRussell] p. 235Definition *30.01conventions 30428  df-fv 6570
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 10038  pm54.43lem 10037
[Young] p. 141Definition of operator orderingleop2 32152
[Young] p. 142Example 12.2(i)0leop 32158  idleop 32159
[vandenDries] p. 42Lemma 61irrapx1 42815
[vandenDries] p. 43Theorem 62pellex 42822  pellexlem1 42816

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