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. 28Proposition 3.10sectcan 13908
[Adamek] p. 29Proposition 3.14(1)invinv 13922
[Adamek] p. 29Proposition 3.14(2)invco 13923  isoco 13925
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18613  df-nmoo 22094
[AkhiezerGlazman] p. 64Theoremhmopidmch 23504  hmopidmchi 23502
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 23552  pjcmul2i 23553
[AkhiezerGlazman] p. 72Theoremcnvunop 23269  unoplin 23271
[AkhiezerGlazman] p. 72Equation 2unopadj 23270  unopadj2 23289
[AkhiezerGlazman] p. 73Theoremelunop2 23364  lnopunii 23363
[AkhiezerGlazman] p. 80Proposition 1adjlnop 23437
[Apostol] p. 18Theorem I.1addcan 9182  addcan2d 9202  addcan2i 9192  addcand 9201  addcani 9191
[Apostol] p. 18Theorem I.2negeu 9228
[Apostol] p. 18Theorem I.3negsub 9281  negsubd 9349  negsubi 9310
[Apostol] p. 18Theorem I.4negneg 9283  negnegd 9334  negnegi 9302
[Apostol] p. 18Theorem I.5subdi 9399  subdid 9421  subdii 9414  subdir 9400  subdird 9422  subdiri 9415
[Apostol] p. 18Theorem I.6mul01 9177  mul01d 9197  mul01i 9188  mul02 9176  mul02d 9196  mul02i 9187
[Apostol] p. 18Theorem I.7mulcan 9591  mulcan2d 9588  mulcand 9587  mulcani 9593
[Apostol] p. 18Theorem I.8receu 9599  xreceu 24006
[Apostol] p. 18Theorem I.9divrec 9626  divrecd 9725  divreci 9691  divreczi 9684
[Apostol] p. 18Theorem I.10recrec 9643  recreci 9678
[Apostol] p. 18Theorem I.11mul0or 9594  mul0ord 9604  mul0ori 9602
[Apostol] p. 18Theorem I.12mul2neg 9405  mul2negd 9420  mul2negi 9413  mulneg1 9402  mulneg1d 9418  mulneg1i 9411
[Apostol] p. 18Theorem I.13divadddiv 9661  divadddivd 9766  divadddivi 9708
[Apostol] p. 18Theorem I.14divmuldiv 9646  divmuldivd 9763  divmuldivi 9706  rdivmuldivd 24056
[Apostol] p. 18Theorem I.15divdivdiv 9647  divdivdivd 9769  divdivdivi 9709
[Apostol] p. 20Axiom 7rpaddcl 10564  rpaddcld 10595  rpmulcl 10565  rpmulcld 10596
[Apostol] p. 20Axiom 8rpneg 10573
[Apostol] p. 20Axiom 90nrp 10574
[Apostol] p. 20Theorem I.17lttri 9131
[Apostol] p. 20Theorem I.18ltadd1d 9551  ltadd1dd 9569  ltadd1i 9513
[Apostol] p. 20Theorem I.19ltmul1 9792  ltmul1a 9791  ltmul1i 9861  ltmul1ii 9871  ltmul2 9793  ltmul2d 10618  ltmul2dd 10632  ltmul2i 9864
[Apostol] p. 20Theorem I.20msqgt0 9480  msqgt0d 9526  msqgt0i 9496
[Apostol] p. 20Theorem I.210lt1 9482
[Apostol] p. 20Theorem I.23lt0neg1 9466  lt0neg1d 9528  ltneg 9460  ltnegd 9536  ltnegi 9503
[Apostol] p. 20Theorem I.25lt2add 9445  lt2addd 9580  lt2addi 9521
[Apostol] p. 20Definition of positive numbersdf-rp 10545
[Apostol] p. 21Exercise 4recgt0 9786  recgt0d 9877  recgt0i 9847  recgt0ii 9848
[Apostol] p. 22Definition of integersdf-z 10215
[Apostol] p. 22Definition of positive integersdfnn3 9946
[Apostol] p. 22Definition of rationalsdf-q 10507
[Apostol] p. 24Theorem I.26supeu 7392
[Apostol] p. 26Theorem I.28nnunb 10149
[Apostol] p. 26Theorem I.29arch 10150
[Apostol] p. 28Exercise 2btwnz 10304
[Apostol] p. 28Exercise 3nnrecl 10151
[Apostol] p. 28Exercise 4rebtwnz 10505
[Apostol] p. 28Exercise 5zbtwnre 10504
[Apostol] p. 28Exercise 6qbtwnre 10717
[Apostol] p. 28Exercise 10(a)zneo 10284
[Apostol] p. 29Theorem I.35msqsqrd 12169  resqrth 11988  sqrth 12095  sqrthi 12101  sqsqrd 12168
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9935
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10474
[Apostol] p. 361Remarkcrreczi 11431
[Apostol] p. 363Remarkabsgt0i 12129
[Apostol] p. 363Exampleabssubd 12182  abssubi 12133
[Baer] p. 40Property (b)mapdord 31753
[Baer] p. 40Property (c)mapd11 31754
[Baer] p. 40Property (e)mapdin 31777  mapdlsm 31779
[Baer] p. 40Property (f)mapd0 31780
[Baer] p. 40Definition of projectivitydf-mapd 31740  mapd1o 31763
[Baer] p. 41Property (g)mapdat 31782
[Baer] p. 44Part (1)mapdpg 31821
[Baer] p. 45Part (2)hdmap1eq 31917  mapdheq 31843  mapdheq2 31844  mapdheq2biN 31845
[Baer] p. 45Part (3)baerlem3 31828
[Baer] p. 46Part (4)mapdheq4 31847  mapdheq4lem 31846
[Baer] p. 46Part (5)baerlem5a 31829  baerlem5abmN 31833  baerlem5amN 31831  baerlem5b 31830  baerlem5bmN 31832
[Baer] p. 47Part (6)hdmap1l6 31937  hdmap1l6a 31925  hdmap1l6e 31930  hdmap1l6f 31931  hdmap1l6g 31932  hdmap1l6lem1 31923  hdmap1l6lem2 31924  hdmap1p6N 31938  mapdh6N 31862  mapdh6aN 31850  mapdh6eN 31855  mapdh6fN 31856  mapdh6gN 31857  mapdh6lem1N 31848  mapdh6lem2N 31849
[Baer] p. 48Part 9hdmapval 31946
[Baer] p. 48Part 10hdmap10 31958
[Baer] p. 48Part 11hdmapadd 31961
[Baer] p. 48Part (6)hdmap1l6h 31933  mapdh6hN 31858
[Baer] p. 48Part (7)mapdh75cN 31868  mapdh75d 31869  mapdh75e 31867  mapdh75fN 31870  mapdh7cN 31864  mapdh7dN 31865  mapdh7eN 31863  mapdh7fN 31866
[Baer] p. 48Part (8)mapdh8 31904  mapdh8a 31890  mapdh8aa 31891  mapdh8ab 31892  mapdh8ac 31893  mapdh8ad 31894  mapdh8b 31895  mapdh8c 31896  mapdh8d 31898  mapdh8d0N 31897  mapdh8e 31899  mapdh8fN 31900  mapdh8g 31901  mapdh8i 31902  mapdh8j 31903
[Baer] p. 48Part (9)mapdh9a 31905
[Baer] p. 48Equation 10mapdhvmap 31884
[Baer] p. 49Part 12hdmap11 31966  hdmapeq0 31962  hdmapf1oN 31983  hdmapneg 31964  hdmaprnN 31982  hdmaprnlem1N 31967  hdmaprnlem3N 31968  hdmaprnlem3uN 31969  hdmaprnlem4N 31971  hdmaprnlem6N 31972  hdmaprnlem7N 31973  hdmaprnlem8N 31974  hdmaprnlem9N 31975  hdmapsub 31965
[Baer] p. 49Part 14hdmap14lem1 31986  hdmap14lem10 31995  hdmap14lem1a 31984  hdmap14lem2N 31987  hdmap14lem2a 31985  hdmap14lem3 31988  hdmap14lem8 31993  hdmap14lem9 31994
[Baer] p. 50Part 14hdmap14lem11 31996  hdmap14lem12 31997  hdmap14lem13 31998  hdmap14lem14 31999  hdmap14lem15 32000  hgmapval 32005
[Baer] p. 50Part 15hgmapadd 32012  hgmapmul 32013  hgmaprnlem2N 32015  hgmapvs 32009
[Baer] p. 50Part 16hgmaprnN 32019
[Baer] p. 110Lemma 1hdmapip0com 32035
[Baer] p. 110Line 27hdmapinvlem1 32036
[Baer] p. 110Line 28hdmapinvlem2 32037
[Baer] p. 110Line 30hdmapinvlem3 32038
[Baer] p. 110Part 1.2hdmapglem5 32040  hgmapvv 32044
[Baer] p. 110Proposition 1hdmapinvlem4 32039
[Baer] p. 111Line 10hgmapvvlem1 32041
[Baer] p. 111Line 15hdmapg 32048  hdmapglem7 32047
[BellMachover] p. 36Lemma 10.3id1 21
[BellMachover] p. 97Definition 10.1df-eu 2242
[BellMachover] p. 460Notationdf-mo 2243
[BellMachover] p. 460Definitionmo3 2269
[BellMachover] p. 461Axiom Extax-ext 2368
[BellMachover] p. 462Theorem 1.1bm1.1 2372
[BellMachover] p. 463Axiom Repaxrep5 4266
[BellMachover] p. 463Scheme Sepaxsep 4270
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4274
[BellMachover] p. 466Axiom Powaxpow3 4321
[BellMachover] p. 466Axiom Unionaxun2 4643
[BellMachover] p. 468Definitiondf-ord 4525
[BellMachover] p. 469Theorem 2.2(i)ordirr 4540
[BellMachover] p. 469Theorem 2.2(iii)onelon 4547
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4542
[BellMachover] p. 471Definition of Ndf-om 4786
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4726
[BellMachover] p. 471Definition of Limdf-lim 4527
[BellMachover] p. 472Axiom Infzfinf2 7530
[BellMachover] p. 473Theorem 2.8limom 4800
[BellMachover] p. 477Equation 3.1df-r1 7623
[BellMachover] p. 478Definitionrankval2 7677
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7641  r1ord3g 7638
[BellMachover] p. 480Axiom Regzfreg2 7497
[BellMachover] p. 488Axiom ACac5 8290  dfac4 7936
[BellMachover] p. 490Definition of alephalephval3 7924
[BeltramettiCassinelli] p. 98Remarkatlatmstc 29434
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 23704
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 23746  chirredi 23745
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 23734
[Beran] p. 3Definition of joinsshjval3 22704
[Beran] p. 39Theorem 2.3(i)cmcm2 22966  cmcm2i 22943  cmcm2ii 22948  cmt2N 29365
[Beran] p. 40Theorem 2.3(iii)lecm 22967  lecmi 22952  lecmii 22953
[Beran] p. 45Theorem 3.4cmcmlem 22941
[Beran] p. 49Theorem 4.2cm2j 22970  cm2ji 22975  cm2mi 22976
[Beran] p. 95Definitiondf-sh 22557  issh2 22559
[Beran] p. 95Lemma 3.1(S5)his5 22436
[Beran] p. 95Lemma 3.1(S6)his6 22449
[Beran] p. 95Lemma 3.1(S7)his7 22440
[Beran] p. 95Lemma 3.2(S8)ho01i 23179
[Beran] p. 95Lemma 3.2(S9)hoeq1 23181
[Beran] p. 95Lemma 3.2(S10)ho02i 23180
[Beran] p. 95Lemma 3.2(S11)hoeq2 23182
[Beran] p. 95Postulate (S1)ax-his1 22432  his1i 22450
[Beran] p. 95Postulate (S2)ax-his2 22433
[Beran] p. 95Postulate (S3)ax-his3 22434
[Beran] p. 95Postulate (S4)ax-his4 22435
[Beran] p. 96Definition of normdf-hnorm 22319  dfhnorm2 22472  normval 22474
[Beran] p. 96Definition for Cauchy sequencehcau 22534
[Beran] p. 96Definition of Cauchy sequencedf-hcau 22324
[Beran] p. 96Definition of complete subspaceisch3 22592
[Beran] p. 96Definition of convergedf-hlim 22323  hlimi 22538
[Beran] p. 97Theorem 3.3(i)norm-i-i 22483  norm-i 22479
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 22487  norm-ii 22488  normlem0 22459  normlem1 22460  normlem2 22461  normlem3 22462  normlem4 22463  normlem5 22464  normlem6 22465  normlem7 22466  normlem7tALT 22469
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 22489  norm-iii 22490
[Beran] p. 98Remark 3.4bcs 22531  bcsiALT 22529  bcsiHIL 22530
[Beran] p. 98Remark 3.4(B)normlem9at 22471  normpar 22505  normpari 22504
[Beran] p. 98Remark 3.4(C)normpyc 22496  normpyth 22495  normpythi 22492
[Beran] p. 99Remarklnfn0 23398  lnfn0i 23393  lnop0 23317  lnop0i 23321
[Beran] p. 99Theorem 3.5(i)nmcexi 23377  nmcfnex 23404  nmcfnexi 23402  nmcopex 23380  nmcopexi 23378
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 23405  nmcfnlbi 23403  nmcoplb 23381  nmcoplbi 23379
[Beran] p. 99Theorem 3.5(iii)lnfncon 23407  lnfnconi 23406  lnopcon 23386  lnopconi 23385
[Beran] p. 100Lemma 3.6normpar2i 22506
[Beran] p. 101Lemma 3.6norm3adifi 22503  norm3adifii 22498  norm3dif 22500  norm3difi 22497
[Beran] p. 102Theorem 3.7(i)chocunii 22651  pjhth 22743  pjhtheu 22744  pjpjhth 22775  pjpjhthi 22776  pjth 19207
[Beran] p. 102Theorem 3.7(ii)ococ 22756  ococi 22755
[Beran] p. 103Remark 3.8nlelchi 23412
[Beran] p. 104Theorem 3.9riesz3i 23413  riesz4 23415  riesz4i 23414
[Beran] p. 104Theorem 3.10cnlnadj 23430  cnlnadjeu 23429  cnlnadjeui 23428  cnlnadji 23427  cnlnadjlem1 23418  nmopadjlei 23439
[Beran] p. 106Theorem 3.11(i)adjeq0 23442
[Beran] p. 106Theorem 3.11(v)nmopadji 23441
[Beran] p. 106Theorem 3.11(ii)adjmul 23443
[Beran] p. 106Theorem 3.11(iv)adjadj 23287
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 23453  nmopcoadji 23452
[Beran] p. 106Theorem 3.11(iii)adjadd 23444
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 23454
[Beran] p. 106Theorem 3.11(viii)adjcoi 23451  pjadj2coi 23555  pjadjcoi 23512
[Beran] p. 107Definitiondf-ch 22572  isch2 22574
[Beran] p. 107Remark 3.12choccl 22656  isch3 22592  occl 22654  ocsh 22633  shoccl 22655  shocsh 22634
[Beran] p. 107Remark 3.12(B)ococin 22758
[Beran] p. 108Theorem 3.13chintcl 22682
[Beran] p. 109Property (i)pjadj2 23538  pjadj3 23539  pjadji 23035  pjadjii 23024
[Beran] p. 109Property (ii)pjidmco 23532  pjidmcoi 23528  pjidmi 23023
[Beran] p. 110Definition of projector orderingpjordi 23524
[Beran] p. 111Remarkho0val 23101  pjch1 23020
[Beran] p. 111Definitiondf-hfmul 23085  df-hfsum 23084  df-hodif 23083  df-homul 23082  df-hosum 23081
[Beran] p. 111Lemma 4.4(i)pjo 23021
[Beran] p. 111Lemma 4.4(ii)pjch 23044  pjchi 22782
[Beran] p. 111Lemma 4.4(iii)pjoc2 22789  pjoc2i 22788
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 23030
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 23516  pjssmii 23031
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 23515
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 23514
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 23519
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 23517  pjssge0ii 23032
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 23518  pjdifnormii 23033
[Bogachev] p. 116Definition 2.3.1df-fndm 24442
[Bogachev] p. 118Definition 2.4.1df-sitg 24440
[Bogachev] p. 118Definition 2.4.4df-itgm 24443
[Bollobas] p. 4Definitiondf-wlk 21381
[Bollobas] p. 5Notationdf-pth 21383
[Bollobas] p. 5Definitiondf-crct 21385  df-cycl 21386  df-trail 21382  df-wlkon 21387
[BourbakiEns] p. Proposition 8fcof1 5959  fcofo 5960
[BourbakiTop1] p. Remarkxnegmnf 10728  xnegpnf 10727
[BourbakiTop1] p. Remark rexneg 10729
[BourbakiTop1] p. Theoremneiss 17096
[BourbakiTop1] p. Remark 3ust0 18170  ustfilxp 18163
[BourbakiTop1] p. Axiom GT'tgpsubcn 18041
[BourbakiTop1] p. Example 1cstucnd 18235  iducn 18234  snfil 17817
[BourbakiTop1] p. Example 2neifil 17833
[BourbakiTop1] p. Theorem 1cnextcn 18019
[BourbakiTop1] p. Theorem 2ucnextcn 18255
[BourbakiTop1] p. Definitionistgp 18028
[BourbakiTop1] p. Propositioncnpco 17253  ishmeo 17712  neips 17100
[BourbakiTop1] p. Definition 1df-ucn 18227  df-ust 18151  filintn0 17814  ucnprima 18233
[BourbakiTop1] p. Definition 2df-cfilu 18238
[BourbakiTop1] p. Definition 3df-cusp 18249  df-usp 18208  df-utop 18182  trust 18180
[BourbakiTop1] p. Condition F_Iustssel 18156
[BourbakiTop1] p. Condition U_Iustdiag 18159
[BourbakiTop1] p. Property V_ivneiptopreu 17120
[BourbakiTop1] p. Proposition 1ucncn 18236  ustund 18172  ustuqtop 18197
[BourbakiTop1] p. Proposition 2neiptopreu 17120  utop2nei 18201  utop3cls 18202
[BourbakiTop1] p. Proposition 3fmucnd 18243  uspreg 18225  utopreg 18203
[BourbakiTop1] p. Proposition 4imasncld 17644  imasncls 17645  imasnopn 17643
[BourbakiTop1] p. Proposition 9cnpflf2 17953
[BourbakiTop1] p. Theorem 1 (d)iscncl 17255
[BourbakiTop1] p. Condition F_IIustincl 18158
[BourbakiTop1] p. Condition U_IIustinvel 18160
[BourbakiTop1] p. Proposition 11cnextucn 18254
[BourbakiTop1] p. Proposition Vissnei2 17103
[BourbakiTop1] p. Condition F_IIbustbasel 18157
[BourbakiTop1] p. Condition U_IIIustexhalf 18161
[BourbakiTop1] p. Definition C'''df-cmp 17372
[BourbakiTop1] p. Proposition Viiinnei 17112
[BourbakiTop1] p. Proposition Vivneissex 17114
[BourbakiTop1] p. Proposition Viiielnei 17098  ssnei 17097
[BourbakiTop1] p. Remark below def. 1filn0 17815
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17799
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17816
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27481  stoweid 27480
[BrosowskiDeutsh] p. 89Theorem for the non-trivial casestoweidlem62 27479
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27418  stoweidlem10 27427  stoweidlem14 27431  stoweidlem15 27432  stoweidlem35 27452  stoweidlem36 27453  stoweidlem37 27454  stoweidlem38 27455  stoweidlem40 27457  stoweidlem41 27458  stoweidlem43 27460  stoweidlem44 27461  stoweidlem46 27463  stoweidlem5 27422  stoweidlem50 27467  stoweidlem52 27469  stoweidlem53 27470  stoweidlem55 27472  stoweidlem56 27473
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27440  stoweidlem24 27441  stoweidlem27 27444  stoweidlem28 27445  stoweidlem30 27447
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27462  stoweidlem49 27466  stoweidlem7 27424
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27448  stoweidlem39 27456  stoweidlem42 27459  stoweidlem48 27465  stoweidlem51 27468  stoweidlem54 27471  stoweidlem57 27474  stoweidlem58 27475
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27442
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27451
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27434
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27476
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27477
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27435
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27428  stoweidlem26 27443
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27430
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27478
[ChoquetDD] p. 2Definition of mappingdf-mpt 4209
[Clemente] p. 10Definition ITnatded 21559
[Clemente] p. 10Definition I` `m,nnatded 21559
[Clemente] p. 11Definition E=>m,nnatded 21559
[Clemente] p. 11Definition I=>m,nnatded 21559
[Clemente] p. 11Definition E` `(1)natded 21559
[Clemente] p. 11Definition E` `(2)natded 21559
[Clemente] p. 12Definition E` `m,n,pnatded 21559
[Clemente] p. 12Definition I` `n(1)natded 21559
[Clemente] p. 12Definition I` `n(2)natded 21559
[Clemente] p. 13Definition I` `m,n,pnatded 21559
[Clemente] p. 14Definition E` `nnatded 21559
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 21561  ex-natded5.2 21560
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 21564  ex-natded5.3 21563
[Clemente] p. 18Theorem 5.5ex-natded5.5 21566
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 21568  ex-natded5.7 21567
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 21570  ex-natded5.8 21569
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 21572  ex-natded5.13 21571
[Clemente] p. 32Definition I` `nnatded 21559
[Clemente] p. 32Definition E` `m,n,p,anatded 21559
[Clemente] p. 32Definition E` `n,tnatded 21559
[Clemente] p. 32Definition I` `n,tnatded 21559
[Clemente] p. 43Theorem 9.20ex-natded9.20 21573
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 21574
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 21576  ex-natded9.26 21575
[Cohen] p. 301Remarkrelogoprlem 20352
[Cohen] p. 301Property 2relogmul 20353  relogmuld 20387
[Cohen] p. 301Property 3relogdiv 20354  relogdivd 20388
[Cohen] p. 301Property 4relogexp 20357
[Cohen] p. 301Property 1alog1 20347
[Cohen] p. 301Property 1bloge 20348
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 24429  sxbrsigalem4 24431
[Cohn] p. 81Section II.5acsdomd 14534  acsinfd 14533  acsinfdimd 14535  acsmap2d 14532  acsmapd 14531
[Cohn] p. 143Example 5.1.1sxbrsiga 24434
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 11169
[Crawley] p. 1Definition of posetdf-poset 14330
[Crawley] p. 107Theorem 13.2hlsupr 29500
[Crawley] p. 110Theorem 13.3arglem1N 30304  dalaw 30000
[Crawley] p. 111Theorem 13.4hlathil 32079
[Crawley] p. 111Definition of set Wdf-watsN 30104
[Crawley] p. 111Definition of dilationdf-dilN 30220  df-ldil 30218  isldil 30224
[Crawley] p. 111Definition of translationdf-ltrn 30219  df-trnN 30221  isltrn 30233  ltrnu 30235
[Crawley] p. 112Lemma Acdlema1N 29905  cdlema2N 29906  exatleN 29518
[Crawley] p. 112Lemma B1cvrat 29590  cdlemb 29908  cdlemb2 30155  cdlemb3 30720  idltrn 30264  l1cvat 29170  lhpat 30157  lhpat2 30159  lshpat 29171  ltrnel 30253  ltrnmw 30265
[Crawley] p. 112Lemma Ccdlemc1 30305  cdlemc2 30306  ltrnnidn 30288  trlat 30283  trljat1 30280  trljat2 30281  trljat3 30282  trlne 30299  trlnidat 30287  trlnle 30300
[Crawley] p. 112Definition of automorphismdf-pautN 30105
[Crawley] p. 113Lemma Ccdlemc 30311  cdlemc3 30307  cdlemc4 30308
[Crawley] p. 113Lemma Dcdlemd 30321  cdlemd1 30312  cdlemd2 30313  cdlemd3 30314  cdlemd4 30315  cdlemd5 30316  cdlemd6 30317  cdlemd7 30318  cdlemd8 30319  cdlemd9 30320  cdleme31sde 30499  cdleme31se 30496  cdleme31se2 30497  cdleme31snd 30500  cdleme32a 30555  cdleme32b 30556  cdleme32c 30557  cdleme32d 30558  cdleme32e 30559  cdleme32f 30560  cdleme32fva 30551  cdleme32fva1 30552  cdleme32fvcl 30554  cdleme32le 30561  cdleme48fv 30613  cdleme4gfv 30621  cdleme50eq 30655  cdleme50f 30656  cdleme50f1 30657  cdleme50f1o 30660  cdleme50laut 30661  cdleme50ldil 30662  cdleme50lebi 30654  cdleme50rn 30659  cdleme50rnlem 30658  cdlemeg49le 30625  cdlemeg49lebilem 30653
[Crawley] p. 113Lemma Ecdleme 30674  cdleme00a 30323  cdleme01N 30335  cdleme02N 30336  cdleme0a 30325  cdleme0aa 30324  cdleme0b 30326  cdleme0c 30327  cdleme0cp 30328  cdleme0cq 30329  cdleme0dN 30330  cdleme0e 30331  cdleme0ex1N 30337  cdleme0ex2N 30338  cdleme0fN 30332  cdleme0gN 30333  cdleme0moN 30339  cdleme1 30341  cdleme10 30368  cdleme10tN 30372  cdleme11 30384  cdleme11a 30374  cdleme11c 30375  cdleme11dN 30376  cdleme11e 30377  cdleme11fN 30378  cdleme11g 30379  cdleme11h 30380  cdleme11j 30381  cdleme11k 30382  cdleme11l 30383  cdleme12 30385  cdleme13 30386  cdleme14 30387  cdleme15 30392  cdleme15a 30388  cdleme15b 30389  cdleme15c 30390  cdleme15d 30391  cdleme16 30399  cdleme16aN 30373  cdleme16b 30393  cdleme16c 30394  cdleme16d 30395  cdleme16e 30396  cdleme16f 30397  cdleme16g 30398  cdleme19a 30417  cdleme19b 30418  cdleme19c 30419  cdleme19d 30420  cdleme19e 30421  cdleme19f 30422  cdleme1b 30340  cdleme2 30342  cdleme20aN 30423  cdleme20bN 30424  cdleme20c 30425  cdleme20d 30426  cdleme20e 30427  cdleme20f 30428  cdleme20g 30429  cdleme20h 30430  cdleme20i 30431  cdleme20j 30432  cdleme20k 30433  cdleme20l 30436  cdleme20l1 30434  cdleme20l2 30435  cdleme20m 30437  cdleme20y 30416  cdleme20zN 30415  cdleme21 30451  cdleme21d 30444  cdleme21e 30445  cdleme22a 30454  cdleme22aa 30453  cdleme22b 30455  cdleme22cN 30456  cdleme22d 30457  cdleme22e 30458  cdleme22eALTN 30459  cdleme22f 30460  cdleme22f2 30461  cdleme22g 30462  cdleme23a 30463  cdleme23b 30464  cdleme23c 30465  cdleme26e 30473  cdleme26eALTN 30475  cdleme26ee 30474  cdleme26f 30477  cdleme26f2 30479  cdleme26f2ALTN 30478  cdleme26fALTN 30476  cdleme27N 30483  cdleme27a 30481  cdleme27cl 30480  cdleme28c 30486  cdleme3 30351  cdleme30a 30492  cdleme31fv 30504  cdleme31fv1 30505  cdleme31fv1s 30506  cdleme31fv2 30507  cdleme31id 30508  cdleme31sc 30498  cdleme31sdnN 30501  cdleme31sn 30494  cdleme31sn1 30495  cdleme31sn1c 30502  cdleme31sn2 30503  cdleme31so 30493  cdleme35a 30562  cdleme35b 30564  cdleme35c 30565  cdleme35d 30566  cdleme35e 30567  cdleme35f 30568  cdleme35fnpq 30563  cdleme35g 30569  cdleme35h 30570  cdleme35h2 30571  cdleme35sn2aw 30572  cdleme35sn3a 30573  cdleme36a 30574  cdleme36m 30575  cdleme37m 30576  cdleme38m 30577  cdleme38n 30578  cdleme39a 30579  cdleme39n 30580  cdleme3b 30343  cdleme3c 30344  cdleme3d 30345  cdleme3e 30346  cdleme3fN 30347  cdleme3fa 30350  cdleme3g 30348  cdleme3h 30349  cdleme4 30352  cdleme40m 30581  cdleme40n 30582  cdleme40v 30583  cdleme40w 30584  cdleme41fva11 30591  cdleme41sn3aw 30588  cdleme41sn4aw 30589  cdleme41snaw 30590  cdleme42a 30585  cdleme42b 30592  cdleme42c 30586  cdleme42d 30587  cdleme42e 30593  cdleme42f 30594  cdleme42g 30595  cdleme42h 30596  cdleme42i 30597  cdleme42k 30598  cdleme42ke 30599  cdleme42keg 30600  cdleme42mN 30601  cdleme42mgN 30602  cdleme43aN 30603  cdleme43bN 30604  cdleme43cN 30605  cdleme43dN 30606  cdleme5 30354  cdleme50ex 30673  cdleme50ltrn 30671  cdleme51finvN 30670  cdleme51finvfvN 30669  cdleme51finvtrN 30672  cdleme6 30355  cdleme7 30363  cdleme7a 30357  cdleme7aa 30356  cdleme7b 30358  cdleme7c 30359  cdleme7d 30360  cdleme7e 30361  cdleme7ga 30362  cdleme8 30364  cdleme8tN 30369  cdleme9 30367  cdleme9a 30365  cdleme9b 30366  cdleme9tN 30371  cdleme9taN 30370  cdlemeda 30412  cdlemedb 30411  cdlemednpq 30413  cdlemednuN 30414  cdlemefr27cl 30517  cdlemefr32fva1 30524  cdlemefr32fvaN 30523  cdlemefrs32fva 30514  cdlemefrs32fva1 30515  cdlemefs27cl 30527  cdlemefs32fva1 30537  cdlemefs32fvaN 30536  cdlemesner 30410  cdlemeulpq 30334
[Crawley] p. 114Lemma E4atex 30190  4atexlem7 30189  cdleme0nex 30404  cdleme17a 30400  cdleme17c 30402  cdleme17d 30612  cdleme17d1 30403  cdleme17d2 30609  cdleme18a 30405  cdleme18b 30406  cdleme18c 30407  cdleme18d 30409  cdleme4a 30353
[Crawley] p. 115Lemma Ecdleme21a 30439  cdleme21at 30442  cdleme21b 30440  cdleme21c 30441  cdleme21ct 30443  cdleme21f 30446  cdleme21g 30447  cdleme21h 30448  cdleme21i 30449  cdleme22gb 30408
[Crawley] p. 116Lemma Fcdlemf 30677  cdlemf1 30675  cdlemf2 30676
[Crawley] p. 116Lemma Gcdlemftr1 30681  cdlemg16 30771  cdlemg28 30818  cdlemg28a 30807  cdlemg28b 30817  cdlemg3a 30711  cdlemg42 30843  cdlemg43 30844  cdlemg44 30847  cdlemg44a 30845  cdlemg46 30849  cdlemg47 30850  cdlemg9 30748  ltrnco 30833  ltrncom 30852  tgrpabl 30865  trlco 30841
[Crawley] p. 116Definition of Gdf-tgrp 30857
[Crawley] p. 117Lemma Gcdlemg17 30791  cdlemg17b 30776
[Crawley] p. 117Definition of Edf-edring-rN 30870  df-edring 30871
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30874
[Crawley] p. 118Remarktendopltp 30894
[Crawley] p. 118Lemma Hcdlemh 30931  cdlemh1 30929  cdlemh2 30930
[Crawley] p. 118Lemma Icdlemi 30934  cdlemi1 30932  cdlemi2 30933
[Crawley] p. 118Lemma Jcdlemj1 30935  cdlemj2 30936  cdlemj3 30937  tendocan 30938
[Crawley] p. 118Lemma Kcdlemk 31088  cdlemk1 30945  cdlemk10 30957  cdlemk11 30963  cdlemk11t 31060  cdlemk11ta 31043  cdlemk11tb 31045  cdlemk11tc 31059  cdlemk11u-2N 31003  cdlemk11u 30985  cdlemk12 30964  cdlemk12u-2N 31004  cdlemk12u 30986  cdlemk13-2N 30990  cdlemk13 30966  cdlemk14-2N 30992  cdlemk14 30968  cdlemk15-2N 30993  cdlemk15 30969  cdlemk16-2N 30994  cdlemk16 30971  cdlemk16a 30970  cdlemk17-2N 30995  cdlemk17 30972  cdlemk18-2N 31000  cdlemk18-3N 31014  cdlemk18 30982  cdlemk19-2N 31001  cdlemk19 30983  cdlemk19u 31084  cdlemk1u 30973  cdlemk2 30946  cdlemk20-2N 31006  cdlemk20 30988  cdlemk21-2N 31005  cdlemk21N 30987  cdlemk22-3 31015  cdlemk22 31007  cdlemk23-3 31016  cdlemk24-3 31017  cdlemk25-3 31018  cdlemk26-3 31020  cdlemk26b-3 31019  cdlemk27-3 31021  cdlemk28-3 31022  cdlemk29-3 31025  cdlemk3 30947  cdlemk30 31008  cdlemk31 31010  cdlemk32 31011  cdlemk33N 31023  cdlemk34 31024  cdlemk35 31026  cdlemk36 31027  cdlemk37 31028  cdlemk38 31029  cdlemk39 31030  cdlemk39u 31082  cdlemk4 30948  cdlemk41 31034  cdlemk42 31055  cdlemk42yN 31058  cdlemk43N 31077  cdlemk45 31061  cdlemk46 31062  cdlemk47 31063  cdlemk48 31064  cdlemk49 31065  cdlemk5 30950  cdlemk50 31066  cdlemk51 31067  cdlemk52 31068  cdlemk53 31071  cdlemk54 31072  cdlemk55 31075  cdlemk55u 31080  cdlemk56 31085  cdlemk5a 30949  cdlemk5auN 30974  cdlemk5u 30975  cdlemk6 30951  cdlemk6u 30976  cdlemk7 30962  cdlemk7u-2N 31002  cdlemk7u 30984  cdlemk8 30952  cdlemk9 30953  cdlemk9bN 30954  cdlemki 30955  cdlemkid 31050  cdlemkj-2N 30996  cdlemkj 30977  cdlemksat 30960  cdlemksel 30959  cdlemksv 30958  cdlemksv2 30961  cdlemkuat 30980  cdlemkuel-2N 30998  cdlemkuel-3 31012  cdlemkuel 30979  cdlemkuv-2N 30997  cdlemkuv2-2 30999  cdlemkuv2-3N 31013  cdlemkuv2 30981  cdlemkuvN 30978  cdlemkvcl 30956  cdlemky 31040  cdlemkyyN 31076  tendoex 31089
[Crawley] p. 120Remarkdva1dim 31099
[Crawley] p. 120Lemma Lcdleml1N 31090  cdleml2N 31091  cdleml3N 31092  cdleml4N 31093  cdleml5N 31094  cdleml6 31095  cdleml7 31096  cdleml8 31097  cdleml9 31098  dia1dim 31176
[Crawley] p. 120Lemma Mdia11N 31163  diaf11N 31164  dialss 31161  diaord 31162  dibf11N 31276  djajN 31252
[Crawley] p. 120Definition of isomorphism mapdiaval 31147
[Crawley] p. 121Lemma Mcdlemm10N 31233  dia2dimlem1 31179  dia2dimlem2 31180  dia2dimlem3 31181  dia2dimlem4 31182  dia2dimlem5 31183  diaf1oN 31245  diarnN 31244  dvheveccl 31227  dvhopN 31231
[Crawley] p. 121Lemma Ncdlemn 31327  cdlemn10 31321  cdlemn11 31326  cdlemn11a 31322  cdlemn11b 31323  cdlemn11c 31324  cdlemn11pre 31325  cdlemn2 31310  cdlemn2a 31311  cdlemn3 31312  cdlemn4 31313  cdlemn4a 31314  cdlemn5 31316  cdlemn5pre 31315  cdlemn6 31317  cdlemn7 31318  cdlemn8 31319  cdlemn9 31320  diclspsn 31309
[Crawley] p. 121Definition of phi(q)df-dic 31288
[Crawley] p. 122Lemma Ndih11 31380  dihf11 31382  dihjust 31332  dihjustlem 31331  dihord 31379  dihord1 31333  dihord10 31338  dihord11b 31337  dihord11c 31339  dihord2 31342  dihord2a 31334  dihord2b 31335  dihord2cN 31336  dihord2pre 31340  dihord2pre2 31341  dihordlem6 31328  dihordlem7 31329  dihordlem7b 31330
[Crawley] p. 122Definition of isomorphism mapdihffval 31345  dihfval 31346  dihval 31347
[Eisenberg] p. 67Definition 5.3df-dif 3266
[Eisenberg] p. 82Definition 6.3dfom3 7535
[Eisenberg] p. 125Definition 8.21df-map 6956
[Eisenberg] p. 216Example 13.2(4)omenps 7542
[Eisenberg] p. 310Theorem 19.8cardprc 7800
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8363
[Enderton] p. 18Axiom of Empty Setaxnul 4278
[Enderton] p. 19Definitiondf-tp 3765
[Enderton] p. 26Exercise 5unissb 3987
[Enderton] p. 26Exercise 10pwel 4356
[Enderton] p. 28Exercise 7(b)pwun 4432
[Enderton] p. 30Theorem "Distributive laws"iinin1 4103  iinin2 4102  iinun2 4098  iunin1 4097  iunin2 4096
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4101  iundif2 4099
[Enderton] p. 32Exercise 20unineq 3534
[Enderton] p. 33Exercise 23iinuni 4115
[Enderton] p. 33Exercise 25iununi 4116
[Enderton] p. 33Exercise 24(a)iinpw 4120
[Enderton] p. 33Exercise 24(b)iunpw 4699  iunpwss 4121
[Enderton] p. 36Definitionopthwiener 4399
[Enderton] p. 38Exercise 6(a)unipw 4355
[Enderton] p. 38Exercise 6(b)pwuni 4336
[Enderton] p. 41Lemma 3Dopeluu 4655  rnex 5073  rnexg 5071
[Enderton] p. 41Exercise 8dmuni 5019  rnuni 5223
[Enderton] p. 42Definition of a functiondffun7 5419  dffun8 5420
[Enderton] p. 43Definition of function valuefunfv2 5730
[Enderton] p. 43Definition of single-rootedfuncnv 5451
[Enderton] p. 44Definition (d)dfima2 5145  dfima3 5146
[Enderton] p. 47Theorem 3Hfvco2 5737
[Enderton] p. 49Axiom of Choice (first form)ac7 8286  ac7g 8287  df-ac 7930  dfac2 7944  dfac2a 7943  dfac3 7935  dfac7 7945
[Enderton] p. 50Theorem 3K(a)imauni 5932
[Enderton] p. 52Definitiondf-map 6956
[Enderton] p. 53Exercise 21coass 5328
[Enderton] p. 53Exercise 27dmco 5318
[Enderton] p. 53Exercise 14(a)funin 5460
[Enderton] p. 53Exercise 22(a)imass2 5180
[Enderton] p. 54Remarkixpf 7020  ixpssmap 7032
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7000
[Enderton] p. 55Axiom of Choice (second form)ac9 8296  ac9s 8306
[Enderton] p. 56Theorem 3Merref 6861
[Enderton] p. 57Lemma 3Nerthi 6887
[Enderton] p. 57Definitiondf-ec 6843
[Enderton] p. 58Definitiondf-qs 6847
[Enderton] p. 60Theorem 3Qth3q 6949  th3qcor 6948  th3qlem1 6946  th3qlem2 6947
[Enderton] p. 61Exercise 35df-ec 6843
[Enderton] p. 65Exercise 56(a)dmun 5016
[Enderton] p. 68Definition of successordf-suc 4528
[Enderton] p. 71Definitiondf-tr 4244  dftr4 4248
[Enderton] p. 72Theorem 4Eunisuc 4598
[Enderton] p. 73Exercise 6unisuc 4598
[Enderton] p. 73Exercise 5(a)truni 4257
[Enderton] p. 73Exercise 5(b)trint 4258  trintALT 28334
[Enderton] p. 79Theorem 4I(A1)nna0 6783
[Enderton] p. 79Theorem 4I(A2)nnasuc 6785  onasuc 6708
[Enderton] p. 79Definition of operation valuedf-ov 6023
[Enderton] p. 80Theorem 4J(A1)nnm0 6784
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6786  onmsuc 6709
[Enderton] p. 81Theorem 4K(1)nnaass 6801
[Enderton] p. 81Theorem 4K(2)nna0r 6788  nnacom 6796
[Enderton] p. 81Theorem 4K(3)nndi 6802
[Enderton] p. 81Theorem 4K(4)nnmass 6803
[Enderton] p. 81Theorem 4K(5)nnmcom 6805
[Enderton] p. 82Exercise 16nnm0r 6789  nnmsucr 6804
[Enderton] p. 88Exercise 23nnaordex 6817
[Enderton] p. 129Definitiondf-en 7046
[Enderton] p. 132Theorem 6B(b)canth 6475
[Enderton] p. 133Exercise 1xpomen 7830
[Enderton] p. 133Exercise 2qnnen 12740
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7227
[Enderton] p. 135Corollary 6Cphp3 7229
[Enderton] p. 136Corollary 6Enneneq 7226
[Enderton] p. 136Corollary 6D(a)pssinf 7255
[Enderton] p. 136Corollary 6D(b)ominf 7257
[Enderton] p. 137Lemma 6Fpssnn 7263
[Enderton] p. 138Corollary 6Gssfi 7265
[Enderton] p. 139Theorem 6H(c)mapen 7207
[Enderton] p. 142Theorem 6I(3)xpcdaen 7996
[Enderton] p. 142Theorem 6I(4)mapcdaen 7997
[Enderton] p. 143Theorem 6Jcda0en 7992  cda1en 7988
[Enderton] p. 144Exercise 13iunfi 7330  unifi 7331  unifi2 7332
[Enderton] p. 144Corollary 6Kundif2 3647  unfi 7310  unfi2 7312
[Enderton] p. 145Figure 38ffoss 5647
[Enderton] p. 145Definitiondf-dom 7047
[Enderton] p. 146Example 1domen 7057  domeng 7058
[Enderton] p. 146Example 3nndomo 7236  nnsdom 7541  nnsdomg 7302
[Enderton] p. 149Theorem 6L(a)cdadom2 8000
[Enderton] p. 149Theorem 6L(c)mapdom1 7208  xpdom1 7143  xpdom1g 7141  xpdom2g 7140
[Enderton] p. 149Theorem 6L(d)mapdom2 7214
[Enderton] p. 151Theorem 6Mzorn 8320  zorng 8317
[Enderton] p. 151Theorem 6M(4)ac8 8305  dfac5 7942
[Enderton] p. 159Theorem 6Qunictb 8383
[Enderton] p. 164Exampleinfdif 8022
[Enderton] p. 168Definitiondf-po 4444
[Enderton] p. 192Theorem 7M(a)oneli 4629
[Enderton] p. 192Theorem 7M(b)ontr1 4568
[Enderton] p. 192Theorem 7M(c)onirri 4628
[Enderton] p. 193Corollary 7N(b)0elon 4575
[Enderton] p. 193Corollary 7N(c)onsuci 4758
[Enderton] p. 193Corollary 7N(d)ssonunii 4708
[Enderton] p. 194Remarkonprc 4705
[Enderton] p. 194Exercise 16suc11 4625
[Enderton] p. 197Definitiondf-card 7759
[Enderton] p. 197Theorem 7Pcarden 8359
[Enderton] p. 200Exercise 25tfis 4774
[Enderton] p. 202Lemma 7Tr1tr 7635
[Enderton] p. 202Definitiondf-r1 7623
[Enderton] p. 202Theorem 7Qr1val1 7645
[Enderton] p. 204Theorem 7V(b)rankval4 7726
[Enderton] p. 206Theorem 7X(b)en2lp 7504
[Enderton] p. 207Exercise 30rankpr 7716  rankprb 7710  rankpw 7702  rankpwi 7682  rankuniss 7725
[Enderton] p. 207Exercise 34opthreg 7506
[Enderton] p. 208Exercise 35suc11reg 7507
[Enderton] p. 212Definition of alephalephval3 7924
[Enderton] p. 213Theorem 8A(a)alephord2 7890
[Enderton] p. 213Theorem 8A(b)cardalephex 7904
[Enderton] p. 218Theorem Schema 8Eonfununi 6539
[Enderton] p. 222Definition of kardkarden 7752  kardex 7751
[Enderton] p. 238Theorem 8Roeoa 6776
[Enderton] p. 238Theorem 8Soeoe 6778
[Enderton] p. 240Exercise 25oarec 6741
[Enderton] p. 257Definition of cofinalitycflm 8063
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13794
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13740
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14530  mrieqv2d 13791  mrieqvd 13790
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13795
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13800  mreexexlem2d 13797
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14536  mreexfidimd 13802
[Fremlin5] p. 193Proposition 563Gbnulmbl2 19298
[Fremlin5] p. 213Lemma 565Cauniioovol 19338
[Fremlin5] p. 214Lemma 565Cauniioombl 19348
[FreydScedrov] p. 283Axiom of Infinityax-inf 7526  inf1 7510  inf2 7511
[Gleason] p. 117Proposition 9-2.1df-enq 8721  enqer 8731
[Gleason] p. 117Proposition 9-2.2df-1nq 8726  df-nq 8722
[Gleason] p. 117Proposition 9-2.3df-plpq 8718  df-plq 8724
[Gleason] p. 119Proposition 9-2.4caovmo 6223  df-mpq 8719  df-mq 8725
[Gleason] p. 119Proposition 9-2.5df-rq 8727
[Gleason] p. 119Proposition 9-2.6ltexnq 8785
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8786  ltbtwnnq 8788
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8781
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8782
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8789
[Gleason] p. 121Definition 9-3.1df-np 8791
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8803
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8805
[Gleason] p. 122Definitiondf-1p 8792
[Gleason] p. 122Remark (1)prub 8804
[Gleason] p. 122Lemma 9-3.4prlem934 8843
[Gleason] p. 122Proposition 9-3.2df-ltp 8795
[Gleason] p. 122Proposition 9-3.3ltsopr 8842  psslinpr 8841  supexpr 8864  suplem1pr 8862  suplem2pr 8863
[Gleason] p. 123Proposition 9-3.5addclpr 8828  addclprlem1 8826  addclprlem2 8827  df-plp 8793
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8832
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8831
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8844
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8853  ltexprlem1 8846  ltexprlem2 8847  ltexprlem3 8848  ltexprlem4 8849  ltexprlem5 8850  ltexprlem6 8851  ltexprlem7 8852
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8855  ltaprlem 8854
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8856
[Gleason] p. 124Lemma 9-3.6prlem936 8857
[Gleason] p. 124Proposition 9-3.7df-mp 8794  mulclpr 8830  mulclprlem 8829  reclem2pr 8858
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8839
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8834
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8833
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8838
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8861  reclem3pr 8859  reclem4pr 8860
[Gleason] p. 126Proposition 9-4.1df-enr 8867  df-mpr 8866  df-plpr 8865  enrer 8876
[Gleason] p. 126Proposition 9-4.2df-0r 8872  df-1r 8873  df-nr 8868
[Gleason] p. 126Proposition 9-4.3df-mr 8870  df-plr 8869  negexsr 8910  recexsr 8915  recexsrlem 8911
[Gleason] p. 127Proposition 9-4.4df-ltr 8871
[Gleason] p. 130Proposition 10-1.3creui 9927  creur 9926  cru 9924
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8996  axcnre 8972
[Gleason] p. 132Definition 10-3.1crim 11847  crimd 11964  crimi 11925  crre 11846  crred 11963  crrei 11924
[Gleason] p. 132Definition 10-3.2remim 11849  remimd 11930
[Gleason] p. 133Definition 10.36absval2 12016  absval2d 12174  absval2i 12127
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11873  cjaddd 11952  cjaddi 11920
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11874  cjmuld 11953  cjmuli 11921
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11872  cjcjd 11931  cjcji 11903
[Gleason] p. 133Proposition 10-3.4(f)cjre 11871  cjreb 11855  cjrebd 11934  cjrebi 11906  cjred 11958  rere 11854  rereb 11852  rerebd 11933  rerebi 11905  rered 11956
[Gleason] p. 133Proposition 10-3.4(h)addcj 11880  addcjd 11944  addcji 11915
[Gleason] p. 133Proposition 10-3.7(a)absval 11970
[Gleason] p. 133Proposition 10-3.7(b)abscj 12011  abscjd 12179  abscji 12131
[Gleason] p. 133Proposition 10-3.7(c)abs00 12021  abs00d 12175  abs00i 12128  absne0d 12176
[Gleason] p. 133Proposition 10-3.7(d)releabs 12052  releabsd 12180  releabsi 12132
[Gleason] p. 133Proposition 10-3.7(f)absmul 12026  absmuld 12183  absmuli 12134
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 12014  sqabsaddi 12135
[Gleason] p. 133Proposition 10-3.7(h)abstri 12061  abstrid 12185  abstrii 12138
[Gleason] p. 134Definition 10-4.1df-exp 11310  exp0 11313  expp1 11315  expp1d 11451
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20437  cxpaddd 20475  expadd 11349  expaddd 11452  expaddz 11351
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20446  cxpmuld 20492  expmul 11352  expmuld 11453  expmulz 11353
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20443  mulcxpd 20486  mulexp 11346  mulexpd 11465  mulexpz 11347
[Gleason] p. 140Exercise 1znnen 12739
[Gleason] p. 141Definition 11-2.1fzval 10977
[Gleason] p. 168Proposition 12-2.1(a)climadd 12352  rlimadd 12363  rlimdiv 12366
[Gleason] p. 168Proposition 12-2.1(b)climsub 12354  rlimsub 12364
[Gleason] p. 168Proposition 12-2.1(c)climmul 12353  rlimmul 12365
[Gleason] p. 171Corollary 12-2.2climmulc2 12357
[Gleason] p. 172Corollary 12-2.5climrecl 12304
[Gleason] p. 172Proposition 12-2.4(c)climabs 12324  climcj 12325  climim 12327  climre 12326  rlimabs 12329  rlimcj 12330  rlimim 12332  rlimre 12331
[Gleason] p. 173Definition 12-3.1df-ltxr 9058  df-xr 9057  ltxr 10647
[Gleason] p. 175Definition 12-4.1df-limsup 12192  limsupval 12195
[Gleason] p. 180Theorem 12-5.1climsup 12390
[Gleason] p. 180Theorem 12-5.3caucvg 12399  caucvgb 12400  caucvgr 12396  climcau 12391
[Gleason] p. 182Exercise 3cvgcmp 12522
[Gleason] p. 182Exercise 4cvgrat 12587
[Gleason] p. 195Theorem 13-2.12abs1m 12066
[Gleason] p. 217Lemma 13-4.1btwnzge0 11157
[Gleason] p. 223Definition 14-1.1df-met 16620
[Gleason] p. 223Definition 14-1.1(a)met0 18282  xmet0 18281
[Gleason] p. 223Definition 14-1.1(b)metgt0 18297
[Gleason] p. 223Definition 14-1.1(c)metsym 18288
[Gleason] p. 223Definition 14-1.1(d)mettri 18290  mstri 18389  xmettri 18289  xmstri 18388
[Gleason] p. 225Definition 14-1.5xpsmet 18320
[Gleason] p. 230Proposition 14-2.6txlm 17601
[Gleason] p. 240Theorem 14-4.3metcnp4 19133
[Gleason] p. 240Proposition 14-4.2metcnp3 18460
[Gleason] p. 243Proposition 14-4.16addcn 18766  addcn2 12314  mulcn 18768  mulcn2 12316  subcn 18767  subcn2 12315
[Gleason] p. 295Remarkbcval3 11524  bcval4 11525
[Gleason] p. 295Equation 2bcpasc 11539
[Gleason] p. 295Definition of binomial coefficientbcval 11522  df-bc 11521
[Gleason] p. 296Remarkbcn0 11528  bcnn 11530
[Gleason] p. 296Theorem 15-2.8binom 12536
[Gleason] p. 308Equation 2ef0 12620
[Gleason] p. 308Equation 3efcj 12621
[Gleason] p. 309Corollary 15-4.3efne0 12625
[Gleason] p. 309Corollary 15-4.4efexp 12629
[Gleason] p. 310Equation 14sinadd 12692
[Gleason] p. 310Equation 15cosadd 12693
[Gleason] p. 311Equation 17sincossq 12704
[Gleason] p. 311Equation 18cosbnd 12709  sinbnd 12708
[Gleason] p. 311Lemma 15-4.7sqeqor 11422  sqeqori 11420
[Gleason] p. 311Definition of pidf-pi 12602
[Godowski] p. 730Equation SFgoeqi 23624
[GodowskiGreechie] p. 249Equation IV3oai 23018
[Gratzer] p. 23Section 0.6df-mre 13738
[Gratzer] p. 27Section 0.6df-mri 13740
[Halmos] p. 31Theorem 17.3riesz1 23416  riesz2 23417
[Halmos] p. 41Definition of Hermitianhmopadj2 23292
[Halmos] p. 42Definition of projector orderingpjordi 23524
[Halmos] p. 43Theorem 26.1elpjhmop 23536  elpjidm 23535  pjnmopi 23499
[Halmos] p. 44Remarkpjinormi 23037  pjinormii 23026
[Halmos] p. 44Theorem 26.2elpjch 23540  pjrn 23057  pjrni 23052  pjvec 23046
[Halmos] p. 44Theorem 26.3pjnorm2 23077
[Halmos] p. 44Theorem 26.4hmopidmpj 23505  hmopidmpji 23503
[Halmos] p. 45Theorem 27.1pjinvari 23542
[Halmos] p. 45Theorem 27.3pjoci 23531  pjocvec 23047
[Halmos] p. 45Theorem 27.4pjorthcoi 23520
[Halmos] p. 48Theorem 29.2pjssposi 23523
[Halmos] p. 48Theorem 29.3pjssdif1i 23526  pjssdif2i 23525
[Halmos] p. 50Definition of spectrumdf-spec 23206
[Hamilton] p. 28Definition 2.1ax-1 5
[Hamilton] p. 31Example 2.7(a)id1 21
[Hamilton] p. 73Rule 1ax-mp 8
[Hamilton] p. 74Rule 2ax-gen 1552
[Hatcher] p. 25Definitiondf-phtpc 18888  df-phtpy 18867
[Hatcher] p. 26Definitiondf-pco 18901  df-pi1 18904
[Hatcher] p. 26Proposition 1.2phtpcer 18891
[Hatcher] p. 26Proposition 1.3pi1grp 18946
[Herstein] p. 54Exercise 28df-grpo 21627
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14748  grpoideu 21645  mndideu 14625
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14766  grpoinveu 21658
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14785  grpo2inv 21675
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14794  grpoinvop 21677
[Herstein] p. 57Exercise 1isgrp2d 21671  isgrp2i 21672
[Hitchcock] p. 5Rule A3mpto1 1539
[Hitchcock] p. 5Rule A4mpto2 1540
[Hitchcock] p. 5Rule A5mtp-xor 1542
[Holland] p. 1519Theorem 2sumdmdi 23771
[Holland] p. 1520Lemma 5cdj1i 23784  cdj3i 23792  cdj3lem1 23785  cdjreui 23783
[Holland] p. 1524Lemma 7mddmdin0i 23782
[Holland95] p. 13Theorem 3.6hlathil 32079
[Holland95] p. 14Line 15hgmapvs 32009
[Holland95] p. 14Line 16hdmaplkr 32031
[Holland95] p. 14Line 17hdmapellkr 32032
[Holland95] p. 14Line 19hdmapglnm2 32029
[Holland95] p. 14Line 20hdmapip0com 32035
[Holland95] p. 14Theorem 3.6hdmapevec2 31954
[Holland95] p. 14Lines 24 and 25hdmapoc 32049
[Holland95] p. 204Definition of involutiondf-srng 15861
[Holland95] p. 212Definition of subspacedf-psubsp 29617
[Holland95] p. 214Lemma 3.3lclkrlem2v 31643
[Holland95] p. 214Definition 3.2df-lpolN 31596
[Holland95] p. 214Definition of nonsingularpnonsingN 30047
[Holland95] p. 215Lemma 3.3(1)dihoml4 31492  poml4N 30067
[Holland95] p. 215Lemma 3.3(2)dochexmid 31583  pexmidALTN 30092  pexmidN 30083
[Holland95] p. 218Theorem 3.6lclkr 31648
[Holland95] p. 218Definition of dual vector spacedf-ldual 29239  ldualset 29240
[Holland95] p. 222Item 1df-lines 29615  df-pointsN 29616
[Holland95] p. 222Item 2df-polarityN 30017
[Holland95] p. 223Remarkispsubcl2N 30061  omllaw4 29361  pol1N 30024  polcon3N 30031
[Holland95] p. 223Definitiondf-psubclN 30049
[Holland95] p. 223Equation for polaritypolval2N 30020
[Hughes] p. 44Equation 1.21bax-his3 22434
[Hughes] p. 47Definition of projection operatordfpjop 23533
[Hughes] p. 49Equation 1.30eighmre 23314  eigre 23186  eigrei 23185
[Hughes] p. 49Equation 1.31eighmorth 23315  eigorth 23189  eigorthi 23188
[Hughes] p. 137Remark (ii)eigposi 23187
[Huneke] p. 1Theoremfrgrancvvdeq 27794  frgrancvvdgeq 27795
[Huneke] p. 1Lemma A for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemA 27789
[Huneke] p. 1Lemma B for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemB 27790
[Huneke] p. 1Lemma C for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemC 27791
[Huneke] p. 2Theoremfrgraregorufr 27805  frgraregorufr0 27804  frgrawopreg1 27802  frgrawopreg2 27803
[Huneke] p. 2Lemma 4 for ~ frgrawopreg . In a friendship graph each vertex with degree K is connected with a vertex with degree other than K. This corresponds to the observation in the prooffrgrawopreglem4 27799
[Huneke] p. 2Lemma 5 for ~ frgrawopreg . If A as well as B contain at least two vertices in a friendship graph, there is a 4-cycle in the graph. This corresponds to the observation in the prooffrgrawopreglem5 27800
[Indrzejczak] p. 33Definition ` `Enatded 21559  natded 21559
[Indrzejczak] p. 33Definition ` `Inatded 21559
[Indrzejczak] p. 34Definition ` `Enatded 21559  natded 21559
[Indrzejczak] p. 34Definition ` `Inatded 21559
[Jech] p. 4Definition of classcv 1648  cvjust 2382
[Jech] p. 42Lemma 6.1alephexp1 8387
[Jech] p. 42Equation 6.1alephadd 8385  alephmul 8386
[Jech] p. 43Lemma 6.2infmap 8384  infmap2 8031
[Jech] p. 71Lemma 9.3jech9.3 7673
[Jech] p. 72Equation 9.3scott0 7743  scottex 7742
[Jech] p. 72Exercise 9.1rankval4 7726
[Jech] p. 72Scheme "Collection Principle"cp 7748
[Jech] p. 78Definition implied by the footnoteopthprc 4865
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26669
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26765
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26766
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26681
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26685
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26686  rmyp1 26687
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26688  rmym1 26689
[JonesMatijasevic] p. 695Equation 2.11rmx0 26679  rmx1 26680  rmxluc 26690
[JonesMatijasevic] p. 695Equation 2.12rmy0 26683  rmy1 26684  rmyluc 26691
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26693
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26694
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26716  jm2.17b 26717  jm2.17c 26718
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26755
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26759
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26750
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26719  jm2.24nn 26715
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26764
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26770  rmygeid 26720
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26782
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1661
[KalishMontague] p. 85Lemma 2equid 1683
[KalishMontague] p. 85Lemma 3equcomi 1686
[KalishMontague] p. 86Lemma 7cbvalivw 1681  cbvaliw 1680
[KalishMontague] p. 87Lemma 8spimvw 1676  spimw 1675
[KalishMontague] p. 87Lemma 9spfw 1698  spw 1701
[Kalmbach] p. 14Definition of latticechabs1 22866  chabs1i 22868  chabs2 22867  chabs2i 22869  chjass 22883  chjassi 22836  latabs1 14443  latabs2 14444
[Kalmbach] p. 15Definition of atomdf-at 23689  ela 23690
[Kalmbach] p. 15Definition of coverscvbr2 23634  cvrval2 29389
[Kalmbach] p. 16Definitiondf-ol 29293  df-oml 29294
[Kalmbach] p. 20Definition of commutescmbr 22934  cmbri 22940  cmtvalN 29326  df-cm 22933  df-cmtN 29292
[Kalmbach] p. 22Remarkomllaw5N 29362  pjoml5 22963  pjoml5i 22938
[Kalmbach] p. 22Definitionpjoml2 22961  pjoml2i 22935
[Kalmbach] p. 22Theorem 2(v)cmcm 22964  cmcmi 22942  cmcmii 22947  cmtcomN 29364
[Kalmbach] p. 22Theorem 2(ii)omllaw3 29360  omlsi 22754  pjoml 22786  pjomli 22785
[Kalmbach] p. 22Definition of OML lawomllaw2N 29359
[Kalmbach] p. 23Remarkcmbr2i 22946  cmcm3 22965  cmcm3i 22944  cmcm3ii 22949  cmcm4i 22945  cmt3N 29366  cmt4N 29367  cmtbr2N 29368
[Kalmbach] p. 23Lemma 3cmbr3 22958  cmbr3i 22950  cmtbr3N 29369
[Kalmbach] p. 25Theorem 5fh1 22968  fh1i 22971  fh2 22969  fh2i 22972  omlfh1N 29373
[Kalmbach] p. 65Remarkchjatom 23708  chslej 22848  chsleji 22808  shslej 22730  shsleji 22720
[Kalmbach] p. 65Proposition 1chocin 22845  chocini 22804  chsupcl 22690  chsupval2 22760  h0elch 22605  helch 22594  hsupval2 22759  ocin 22646  ococss 22643  shococss 22644
[Kalmbach] p. 65Definition of subspace sumshsval 22662
[Kalmbach] p. 66Remarkdf-pjh 22745  pjssmi 23516  pjssmii 23031
[Kalmbach] p. 67Lemma 3osum 22995  osumi 22992
[Kalmbach] p. 67Lemma 4pjci 23551
[Kalmbach] p. 103Exercise 6atmd2 23751
[Kalmbach] p. 103Exercise 12mdsl0 23661
[Kalmbach] p. 140Remarkhatomic 23711  hatomici 23710  hatomistici 23713
[Kalmbach] p. 140Proposition 1atlatmstc 29434
[Kalmbach] p. 140Proposition 1(i)atexch 23732  lsatexch 29158
[Kalmbach] p. 140Proposition 1(ii)chcv1 23706  cvlcvr1 29454  cvr1 29524
[Kalmbach] p. 140Proposition 1(iii)cvexch 23725  cvexchi 23720  cvrexch 29534
[Kalmbach] p. 149Remark 2chrelati 23715  hlrelat 29516  hlrelat5N 29515  lrelat 29129
[Kalmbach] p. 153Exercise 5lsmcv 16140  lsmsatcv 29125  spansncv 23003  spansncvi 23002
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29144  spansncv2 23644
[Kalmbach] p. 266Definitiondf-st 23562
[Kalmbach2] p. 8Definition of adjointdf-adjh 23200
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8454  fpwwe2 8451
[KanamoriPincus] p. 416Corollary 1.3canth4 8455
[KanamoriPincus] p. 417Corollary 1.6canthp1 8462
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8457
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8459
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8472
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8476  gchxpidm 8477
[KanamoriPincus] p. 419Theorem 2.1gchacg 8480  gchhar 8479
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 8029  unxpwdom 7490
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8482
[Kreyszig] p. 3Property M1metcl 18271  xmetcl 18270
[Kreyszig] p. 4Property M2meteq0 18278
[Kreyszig] p. 8Definition 1.1-8dscmet 18491
[Kreyszig] p. 12Equation 5conjmul 9663  muleqadd 9598
[Kreyszig] p. 18Definition 1.3-2mopnval 18358
[Kreyszig] p. 19Remarkmopntopon 18359
[Kreyszig] p. 19Theorem T1mopn0 18418  mopnm 18364
[Kreyszig] p. 19Theorem T2unimopn 18416
[Kreyszig] p. 19Definition of neighborhoodneibl 18421
[Kreyszig] p. 20Definition 1.3-3metcnp2 18462
[Kreyszig] p. 25Definition 1.4-1lmbr 17244  lmmbr 19082  lmmbr2 19083
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17366
[Kreyszig] p. 28Theorem 1.4-5lmcau 19136
[Kreyszig] p. 28Definition 1.4-3iscau 19100  iscmet2 19118
[Kreyszig] p. 30Theorem 1.4-7cmetss 19138
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17445  metelcls 19128
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 19129  metcld2 19130
[Kreyszig] p. 51Equation 2clmvneg1 18987  lmodvneg1 15914  nvinv 21968  vcm 21898
[Kreyszig] p. 51Equation 1aclm0vs 18986  lmod0vs 15910  vc0 21896
[Kreyszig] p. 51Equation 1blmodvs0 15911  vcz 21897
[Kreyszig] p. 58Definition 2.2-1imsmet 22031
[Kreyszig] p. 59Equation 1imsdval 22026  imsdval2 22027
[Kreyszig] p. 63Problem 1nvnd 22028
[Kreyszig] p. 64Problem 2nvge0 22011  nvz 22006
[Kreyszig] p. 64Problem 3nvabs 22010
[Kreyszig] p. 91Definition 2.7-1isblo3i 22150
[Kreyszig] p. 92Equation 2df-nmoo 22094
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 22156  blocni 22154
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 22155
[Kreyszig] p. 129Definition 3.1-1cphipeq0 19037  ipeq0 16792  ipz 22066
[Kreyszig] p. 135Problem 2pythi 22199
[Kreyszig] p. 137Lemma 3-2.1(a)sii 22203
[Kreyszig] p. 144Equation 4supcvg 12562
[Kreyszig] p. 144Theorem 3.3-1minvec 19204  minveco 22234
[Kreyszig] p. 196Definition 3.9-1df-aj 22099
[Kreyszig] p. 247Theorem 4.7-2bcth 19151
[Kreyszig] p. 249Theorem 4.7-3ubth 22223
[Kreyszig] p. 470Definition of positive operator orderingleop 23474  leopg 23473
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 23492
[Kreyszig] p. 525Theorem 10.1-1htth 22269
[Kunen] p. 10Axiom 0a9e 1941  axnul 4278
[Kunen] p. 11Axiom 3axnul 4278
[Kunen] p. 12Axiom 6zfrep6 5907
[Kunen] p. 24Definition 10.24mapval 6966  mapvalg 6964
[Kunen] p. 30Lemma 10.20fodom 8335
[Kunen] p. 31Definition 10.24mapex 6960
[Kunen] p. 95Definition 2.1df-r1 7623
[Kunen] p. 97Lemma 2.10r1elss 7665  r1elssi 7664
[Kunen] p. 107Exercise 4rankop 7717  rankopb 7711  rankuni 7722  rankxplim 7736  rankxpsuc 7739
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4045
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27220
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27215
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27221
[LeBlanc] p. 277Rule R2axnul 4278
[Levy] p. 338Axiomdf-clab 2374  df-clel 2383  df-cleq 2380
[Levy58] p. 2Definition Iisfin1-3 8199
[Levy58] p. 2Definition IIdf-fin2 8099
[Levy58] p. 2Definition Iadf-fin1a 8098
[Levy58] p. 2Definition IIIdf-fin3 8101
[Levy58] p. 3Definition Vdf-fin5 8102
[Levy58] p. 3Definition IVdf-fin4 8100
[Levy58] p. 4Definition VIdf-fin6 8103
[Levy58] p. 4Definition VIIdf-fin7 8104
[Levy58], p. 3Theorem 1fin1a2 8228
[Lopez-Astorga] p. 12Rule 1mpto1 1539
[Lopez-Astorga] p. 12Rule 2mpto2 1540
[Lopez-Astorga] p. 12Rule 3mtp-xor 1542
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 23759
[Maeda] p. 168Lemma 5mdsym 23763  mdsymi 23762
[Maeda] p. 168Lemma 4(i)mdsymlem4 23757  mdsymlem6 23759  mdsymlem7 23760
[Maeda] p. 168Lemma 4(ii)mdsymlem8 23761
[MaedaMaeda] p. 1Remarkssdmd1 23664  ssdmd2 23665  ssmd1 23662  ssmd2 23663
[MaedaMaeda] p. 1Lemma 1.2mddmd2 23660
[MaedaMaeda] p. 1Definition 1.1df-dmd 23632  df-md 23631  mdbr 23645
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 23682  mdslj1i 23670  mdslj2i 23671  mdslle1i 23668  mdslle2i 23669  mdslmd1i 23680  mdslmd2i 23681
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 23672  mdsl2bi 23674  mdsl2i 23673
[MaedaMaeda] p. 2Lemma 1.6mdexchi 23686
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 23683
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 23684
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 23661
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 23666  mdsl3 23667
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 23685
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23780
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 29436  hlrelat1 29514
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29154
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 23687  cvmdi 23675  cvnbtwn4 23640  cvrnbtwn4 29394
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 23688
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 29455  cvp 23726  cvrp 29530  lcvp 29155
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 23750
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 23749
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 29448  hlexch4N 29506
[MaedaMaeda] p. 34Exercise 7.1atabsi 23752
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 29557
[MaedaMaeda] p. 61Definition 15.10psubN 29863  atpsubN 29867  df-pointsN 29616  pointpsubN 29865
[MaedaMaeda] p. 62Theorem 15.5df-pmap 29618  pmap11 29876  pmaple 29875  pmapsub 29882  pmapval 29871
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29879  pmap1N 29881
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29884  pmapglb2N 29885  pmapglb2xN 29886  pmapglbx 29883
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 29966
[MaedaMaeda] p. 67Postulate PS1ps-1 29591
[MaedaMaeda] p. 68Lemma 16.2df-padd 29910  paddclN 29956  paddidm 29955
[MaedaMaeda] p. 68Condition PS2ps-2 29592
[MaedaMaeda] p. 68Equation 16.2.1paddass 29952
[MaedaMaeda] p. 69Lemma 16.4ps-1 29591
[MaedaMaeda] p. 69Theorem 16.4ps-2 29592
[MaedaMaeda] p. 70Theorem 16.9lsmmod 15234  lsmmod2 15235  lssats 29127  shatomici 23709  shatomistici 23712  shmodi 22740  shmodsi 22739
[MaedaMaeda] p. 130Remark 29.6dmdmd 23651  mdsymlem7 23760
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22939
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22843
[MaedaMaeda] p. 139Remarksumdmdii 23766
[Margaris] p. 40Rule Cexlimiv 1641
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 7
[Margaris] p. 49Definitiondf-an 361  df-ex 1548  df-or 360  dfbi2 610
[Margaris] p. 51Theorem 1id1 21
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 28368
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 28369
[Margaris] p. 79Rule Cexinst01 28067  exinst11 28068
[Margaris] p. 89Theorem 19.219.2 1666  19.2g 1765  r19.2z 3660
[Margaris] p. 89Theorem 19.319.3 1793  19.3v 1672  rr19.3v 3020
[Margaris] p. 89Theorem 19.5alcom 1744
[Margaris] p. 89Theorem 19.6alex 1578
[Margaris] p. 89Theorem 19.7alnex 1549
[Margaris] p. 89Theorem 19.819.8a 1754
[Margaris] p. 89Theorem 19.919.9 1791  19.9h 1788  19.9v 1671  exlimd 1814  exlimdh 1816
[Margaris] p. 89Theorem 19.11excom 1748  excomim 1749
[Margaris] p. 89Theorem 19.1219.12 1859  r19.12 2762
[Margaris] p. 90Theorem 19.14exnal 1580
[Margaris] p. 90Theorem 19.152albi 27245  albi 1570  ralbi 2785
[Margaris] p. 90Theorem 19.1619.16 1872
[Margaris] p. 90Theorem 19.1719.17 1873
[Margaris] p. 90Theorem 19.182exbi 27247  exbi 1588
[Margaris] p. 90Theorem 19.1919.19 1874
[Margaris] p. 90Theorem 19.202alim 27244  alim 1564  alimd 1772  alimdh 1569  alimdv 1628  ralimdaa 2726  ralimdv 2728  ralimdva 2727  sbcimdv 3165
[Margaris] p. 90Theorem 19.2119.21-2 1876  19.21 1804  19.21bi 1766  19.21h 1805  19.21t 1803  19.21v 1902  19.21vv 27243  alrimd 1777  alrimdd 1776  alrimdh 1594  alrimdv 1640  alrimi 1773  alrimih 1571  alrimiv 1638  alrimivv 1639  r19.21 2735  r19.21be 2750  r19.21bi 2747  r19.21t 2734  r19.21v 2736  ralrimd 2737  ralrimdv 2738  ralrimdva 2739  ralrimdvv 2743  ralrimdvva 2744  ralrimi 2730  ralrimiv 2731  ralrimiva 2732  ralrimivv 2740  ralrimivva 2741  ralrimivvva 2742  ralrimivw 2733  rexlimi 2766
[Margaris] p. 90Theorem 19.222alimdv 1630  2exim 27246  2eximdv 1631  exim 1581  eximd 1778  eximdh 1595  eximdv 1629  rexim 2753  reximdai 2757  reximddv 23806  reximdv 2760  reximdv2 2758  reximdva 2761  reximdvai 2759  reximi2 2755
[Margaris] p. 90Theorem 19.2319.23 1809  19.23bi 1767  19.23h 1810  19.23t 1808  19.23v 1903  19.23vv 1904  exlimdv 1643  exlimdvv 1644  exlimexi 27951  exlimi 1811  exlimih 1812  exlimiv 1641  exlimivv 1642  r19.23 2764  r19.23v 2765  rexlimd 2770  rexlimdv 2772  rexlimdv3a 2775  rexlimdva 2773  rexlimdvaa 2774  rexlimdvv 2779  rexlimdvva 2780  rexlimdvw 2776  rexlimiv 2767  rexlimiva 2768  rexlimivv 2778
[Margaris] p. 90Theorem 19.2419.24 1669
[Margaris] p. 90Theorem 19.2519.25 1610
[Margaris] p. 90Theorem 19.2619.26-2 1601  19.26-3an 1602  19.26 1600  r19.26-2 2782  r19.26-3 2783  r19.26 2781  r19.26m 2784
[Margaris] p. 90Theorem 19.2719.27 1831  19.27v 1906  r19.27av 2787  r19.27z 3669  r19.27zv 3670
[Margaris] p. 90Theorem 19.2819.28 1832  19.28v 1907  19.28vv 27253  r19.28av 2788  r19.28z 3663  r19.28zv 3666  rr19.28v 3021
[Margaris] p. 90Theorem 19.2919.29 1603  19.29r 1604  19.29r2 1605  19.29x 1606  r19.29 2789  r19.29d2r 2794  r19.29r 2790
[Margaris] p. 90Theorem 19.3019.30 1611  r19.30 2796
[Margaris] p. 90Theorem 19.3119.31 1886  19.31vv 27251
[Margaris] p. 90Theorem 19.3219.32 1885  r19.32 27613  r19.32v 2797
[Margaris] p. 90Theorem 19.3319.33-2 27249  19.33 1614  19.33b 1615
[Margaris] p. 90Theorem 19.3419.34 1670
[Margaris] p. 90Theorem 19.3519.35 1607  19.35i 1608  19.35ri 1609  r19.35 2798
[Margaris] p. 90Theorem 19.3619.36 1881  19.36aiv 1909  19.36i 1882  19.36v 1908  19.36vv 27250  r19.36av 2799  r19.36zv 3671
[Margaris] p. 90Theorem 19.3719.37 1883  19.37aiv 1912  19.37v 1911  19.37vv 27252  r19.37 2800  r19.37av 2801  r19.37zv 3667
[Margaris] p. 90Theorem 19.3819.38 1802
[Margaris] p. 90Theorem 19.3919.39 1668
[Margaris] p. 90Theorem 19.4019.40-2 1617  19.40 1616  r19.40 2802
[Margaris] p. 90Theorem 19.4119.41 1889  19.41rg 27980  19.41v 1913  19.41vv 1914  19.41vvv 1915  19.41vvvv 1916  r19.41 2803  r19.41v 2804  r19.41vv 23814
[Margaris] p. 90Theorem 19.4219.42 1891  19.42v 1917  19.42vv 1919  19.42vvv 1920  r19.42v 2805
[Margaris] p. 90Theorem 19.4319.43 1612  r19.43 2806
[Margaris] p. 90Theorem 19.4419.44 1887  r19.44av 2807
[Margaris] p. 90Theorem 19.4519.45 1888  r19.45av 2808  r19.45zv 3668
[Margaris] p. 110Exercise 2(b)eu1 2259
[Mayet] p. 370Remarkjpi 23621  largei 23618  stri 23608
[Mayet3] p. 9Definition of CH-statesdf-hst 23563  ishst 23565
[Mayet3] p. 10Theoremhstrbi 23617  hstri 23616
[Mayet3] p. 1223Theorem 4.1mayete3i 23078
[Mayet3] p. 1240Theorem 7.1mayetes3i 23080
[MegPav2000] p. 2344Theorem 3.3stcltrthi 23629
[MegPav2000] p. 2345Definition 3.4-1chintcl 22682  chsupcl 22690
[MegPav2000] p. 2345Definition 3.4-2hatomic 23711
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 23705
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 23732
[MegPav2000] p. 2366Figure 7pl42N 30097
[MegPav2002] p. 362Lemma 2.2latj31 14455  latj32 14453  latjass 14451
[Megill] p. 444Axiom C5ax-17 1623  ax17o 2191
[Megill] p. 444Section 7conventions 21558
[Megill] p. 445Lemma L12aecom-o 2185  aecom 1994  ax-10 2174
[Megill] p. 446Lemma L17equtrr 1690
[Megill] p. 446Lemma L18ax9from9o 2182
[Megill] p. 446Lemma L19hbnae-o 2213  hbnae 1999
[Megill] p. 447Remark 9.1df-sb 1656  sbid 1936  sbidd-misc 27808  sbidd 27807
[Megill] p. 448Remark 9.6ax15 2054
[Megill] p. 448Scheme C4'ax-5o 2170
[Megill] p. 448Scheme C5'ax-4 2169  sp 1755
[Megill] p. 448Scheme C6'ax-7 1741
[Megill] p. 448Scheme C7'ax-6o 2171
[Megill] p. 448Scheme C8'ax-8 1682
[Megill] p. 448Scheme C9'ax-12o 2176
[Megill] p. 448Scheme C10'ax-9 1661  ax-9o 2172
[Megill] p. 448Scheme C11'ax-10o 2173
[Megill] p. 448Scheme C12'ax-13 1719
[Megill] p. 448Scheme C13'ax-14 1721
[Megill] p. 448Scheme C14'ax-15 2177
[Megill] p. 448Scheme C15'ax-11o 2175
[Megill] p. 448Scheme C16'ax-16 2178
[Megill] p. 448Theorem 9.4dral1-o 2188  dral1 2004  dral2-o 2215  dral2 2005  drex1 2006  drex2 2007  drsb1 2055  drsb2 2094
[Megill] p. 448Theorem 9.7conventions 21558
[Megill] p. 449Theorem 9.7sbcom2 2147  sbequ 2093  sbid2v 2157
[Megill] p. 450Example in Appendixhba1-o 2183  hba1 1794
[Mendelson] p. 35Axiom A3hirstL-ax3 27528
[Mendelson] p. 36Lemma 1.8id1 21
[Mendelson] p. 69Axiom 4rspsbc 3182  rspsbca 3183  stdpc4 2057
[Mendelson] p. 69Axiom 5ax-5o 2170  ra5 3188  stdpc5 1806
[Mendelson] p. 81Rule Cexlimiv 1641
[Mendelson] p. 95Axiom 6stdpc6 1694
[Mendelson] p. 95Axiom 7stdpc7 1931
[Mendelson] p. 225Axiom system NBGru 3103
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4399
[Mendelson] p. 231Exercise 4.10(k)inv1 3597
[Mendelson] p. 231Exercise 4.10(l)unv 3598
[Mendelson] p. 231Exercise 4.10(n)dfin3 3523
[Mendelson] p. 231Exercise 4.10(o)df-nul 3572
[Mendelson] p. 231Exercise 4.10(q)dfin4 3524
[Mendelson] p. 231Exercise 4.10(s)ddif 3422
[Mendelson] p. 231Definition of uniondfun3 3522
[Mendelson] p. 235Exercise 4.12(c)univ 4694
[Mendelson] p. 235Exercise 4.12(d)pwv 3956
[Mendelson] p. 235Exercise 4.12(j)pwin 4428
[Mendelson] p. 235Exercise 4.12(k)pwunss 4429
[Mendelson] p. 235Exercise 4.12(l)pwssun 4430
[Mendelson] p. 235Exercise 4.12(n)uniin 3977
[Mendelson] p. 235Exercise 4.12(p)reli 4942
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5330
[Mendelson] p. 244Proposition 4.8(g)epweon 4704
[Mendelson] p. 246Definition of successordf-suc 4528
[Mendelson] p. 250Exercise 4.36oelim2 6774
[Mendelson] p. 254Proposition 4.22(b)xpen 7206
[Mendelson] p. 254Proposition 4.22(c)xpsnen 7128  xpsneng 7129
[Mendelson] p. 254Proposition 4.22(d)xpcomen 7135  xpcomeng 7136
[Mendelson] p. 254Proposition 4.22(e)xpassen 7138
[Mendelson] p. 255Definitionbrsdom 7066
[Mendelson] p. 255Exercise 4.39endisj 7131
[Mendelson] p. 255Exercise 4.41mapprc 6958
[Mendelson] p. 255Exercise 4.43mapsnen 7120
[Mendelson] p. 255Exercise 4.45mapunen 7212
[Mendelson] p. 255Exercise 4.47xpmapen 7211
[Mendelson] p. 255Exercise 4.42(a)map0e 6987
[Mendelson] p. 255Exercise 4.42(b)map1 7121
[Mendelson] p. 257Proposition 4.24(a)undom 7132
[Mendelson] p. 258Exercise 4.56(b)cdaen 7986
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7995  cdacomen 7994
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7999
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7993
[Mendelson] p. 258Definition of cardinal sumcdaval 7983  df-cda 7981
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6711
[Mendelson] p. 266Proposition 4.34(f)oaordex 6737
[Mendelson] p. 275Proposition 4.42(d)entri3 8367
[Mendelson] p. 281Definitiondf-r1 7623
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7672
[Mendelson] p. 287Axiom system MKru 3103
[MertziosUnger] p. 153Proposition 12pthfrgra 27764  2pthfrgrarn 27762  2pthfrgrarn2 27763  frconngra 27774  n4cyclfrgra 27771  vdgfrgragt2 27781  vdgn1frgrav2 27780  vdn1frgrav2 27779
[Mittelstaedt] p. 9Definitiondf-oc 22602
[Monk1] p. 22Remarkconventions 21558
[Monk1] p. 22Theorem 3.1conventions 21558
[Monk1] p. 26Theorem 2.8(vii)ssin 3506
[Monk1] p. 33Theorem 3.2(i)ssrel 4904
[Monk1] p. 33Theorem 3.2(ii)eqrel 4905
[Monk1] p. 34Definition 3.3df-opab 4208
[Monk1] p. 36Theorem 3.7(i)coi1 5325  coi2 5326
[Monk1] p. 36Theorem 3.8(v)dm0 5023  rn0 5067
[Monk1] p. 36Theorem 3.7(ii)cnvi 5216
[Monk1] p. 37Theorem 3.13(i)relxp 4923
[Monk1] p. 37Theorem 3.13(x)dmxp 5028  rnxp 5239
[Monk1] p. 37Theorem 3.13(ii)xp0 5231  xp0r 4896
[Monk1] p. 38Theorem 3.16(ii)ima0 5161
[Monk1] p. 38Theorem 3.16(viii)imai 5158
[Monk1] p. 39Theorem 3.17imaexg 5157
[Monk1] p. 39Theorem 3.16(xi)imassrn 5156
[Monk1] p. 41Theorem 4.3(i)fnopfv 5804  funfvop 5781
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5709
[Monk1] p. 42Theorem 4.4(iii)fvelima 5717
[Monk1] p. 43Theorem 4.6funun 5435
[Monk1] p. 43Theorem 4.8(iv)dff13 5943  dff13f 5945
[Monk1] p. 46Theorem 4.15(v)funex 5902  funrnex 5906
[Monk1] p. 50Definition 5.4fniunfv 5933
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5293
[Monk1] p. 52Theorem 5.11(viii)ssint 4008
[Monk1] p. 52Definition 5.13 (i)1stval2 6303  df-1st 6288
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6304  df-2nd 6289
[Monk1] p. 112Theorem 15.17(v)ranksn 7713  ranksnb 7686
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7714
[Monk1] p. 112Theorem 15.17(iii)rankun 7715  rankunb 7709
[Monk1] p. 113Theorem 15.18r1val3 7697
[Monk1] p. 113Definition 15.19df-r1 7623  r1val2 7696
[Monk1] p. 117Lemmazorn2 8319  zorn2g 8316
[Monk1] p. 133Theorem 18.11cardom 7806
[Monk1] p. 133Theorem 18.12canth3 8369
[Monk1] p. 133Theorem 18.14carduni 7801
[Monk2] p. 105Axiom C4ax-5 1563
[Monk2] p. 105Axiom C7ax-8 1682
[Monk2] p. 105Axiom C8ax-11 1753  ax-11o 2175
[Monk2] p. 105Axiom (C8)ax11v 2129
[Monk2] p. 108Lemma 5ax-5o 2170
[Monk2] p. 109Lemma 12ax-7 1741
[Monk2] p. 109Lemma 15equvin 2035  equvini 2022  eqvinop 4382
[Monk2] p. 113Axiom C5-1ax-17 1623  ax17o 2191
[Monk2] p. 113Axiom C5-2ax-6 1736
[Monk2] p. 113Axiom C5-3ax-7 1741
[Monk2] p. 114Lemma 21sp 1755
[Monk2] p. 114Lemma 22ax5o 1757  hba1-o 2183  hba1 1794
[Monk2] p. 114Lemma 23nfia1 1868
[Monk2] p. 114Lemma 24nfa2 1867  nfra2 2703
[Moore] p. 53Part Idf-mre 13738
[Munkres] p. 77Example 2distop 16983  indistop 16989  indistopon 16988
[Munkres] p. 77Example 3fctop 16991  fctop2 16992
[Munkres] p. 77Example 4cctop 16993
[Munkres] p. 78Definition of basisdf-bases 16888  isbasis3g 16937
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13594  tgval2 16944
[Munkres] p. 79Remarktgcl 16957
[Munkres] p. 80Lemma 2.1tgval3 16951
[Munkres] p. 80Lemma 2.2tgss2 16975  tgss3 16974
[Munkres] p. 81Lemma 2.3basgen 16976  basgen2 16977
[Munkres] p. 89Definition of subspace topologyresttop 17146
[Munkres] p. 93Theorem 6.1(1)0cld 17025  topcld 17022
[Munkres] p. 93Theorem 6.1(2)iincld 17026
[Munkres] p. 93Theorem 6.1(3)uncld 17028
[Munkres] p. 94Definition of closureclsval 17024
[Munkres] p. 94Definition of interiorntrval 17023
[Munkres] p. 95Theorem 6.5(a)clsndisj 17062  elcls 17060
[Munkres] p. 95Theorem 6.5(b)elcls3 17070
[Munkres] p. 97Theorem 6.6clslp 17134  neindisj 17104
[Munkres] p. 97Corollary 6.7cldlp 17136
[Munkres] p. 97Definition of limit pointislp2 17132  lpval 17126
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17301
[Munkres] p. 102Definition of continuous functiondf-cn 17213  iscn 17221  iscn2 17224
[Munkres] p. 107Theorem 7.2(g)cncnp 17266  cncnp2 17267  cncnpi 17264  df-cnp 17214  iscnp 17223  iscnp2 17225
[Munkres] p. 127Theorem 10.1metcn 18463
[Munkres] p. 128Theorem 10.3metcn4 19134
[NielsenChuang] p. 195Equation 4.73unierri 23455
[Pfenning] p. 17Definition XMnatded 21559  natded 21559
[Pfenning] p. 17Definition NNCnatded 21559  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 21559
[Pfenning] p. 18Rule"natded 21559
[Pfenning] p. 18Definition /\Inatded 21559
[Pfenning] p. 18Definition ` `Enatded 21559  natded 21559  natded 21559  natded 21559  natded 21559
[Pfenning] p. 18Definition ` `Inatded 21559  natded 21559  natded 21559  natded 21559  natded 21559
[Pfenning] p. 18Definition ` `ELnatded 21559
[Pfenning] p. 18Definition ` `ERnatded 21559
[Pfenning] p. 18Definition ` `Ea,unatded 21559
[Pfenning] p. 18Definition ` `IRnatded 21559
[Pfenning] p. 18Definition ` `Ianatded 21559
[Pfenning] p. 127Definition =Enatded 21559
[Pfenning] p. 127Definition =Inatded 21559
[Ponnusamy] p. 361Theorem 6.44cphip0l 19035  df-dip 22045  dip0l 22065  ip0l 16790
[Ponnusamy] p. 361Equation 6.45ipval 22047
[Ponnusamy] p. 362Equation I1dipcj 22061
[Ponnusamy] p. 362Equation I3cphdir 19038  dipdir 22191  ipdir 16793  ipdiri 22179
[Ponnusamy] p. 362Equation I4ipidsq 22057
[Ponnusamy] p. 362Equation 6.46ip0i 22174
[Ponnusamy] p. 362Equation 6.47ip1i 22176
[Ponnusamy] p. 362Equation 6.48ip2i 22177
[Ponnusamy] p. 363Equation I2cphass 19044  dipass 22194  ipass 16799  ipassi 22190
[Prugovecki] p. 186Definition of brabraval 23295  df-bra 23201
[Prugovecki] p. 376Equation 8.1df-kb 23202  kbval 23305
[PtakPulmannova] p. 66Proposition 3.2.17atomli 23733
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30002
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 23747  atcvat4i 23748  cvrat3 29556  cvrat4 29557  lsatcvat3 29167
[PtakPulmannova] p. 68Definition 3.2.18cvbr 23633  cvrval 29384  df-cv 23630  df-lcv 29134  lspsncv0 16145
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30014
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30015
[Quine] p. 16Definition 2.1df-clab 2374  rabid 2827
[Quine] p. 17Definition 2.1''dfsb7 2155
[Quine] p. 18Definition 2.7df-cleq 2380
[Quine] p. 19Definition 2.9conventions 21558  df-v 2901
[Quine] p. 34Theorem 5.1abeq2 2492
[Quine] p. 35Theorem 5.2abid2 2504  abid2f 2548
[Quine] p. 40Theorem 6.1sb5 2133
[Quine] p. 40Theorem 6.2sb56 2131  sb6 2132
[Quine] p. 41Theorem 6.3df-clel 2383
[Quine] p. 41Theorem 6.4eqid 2387  eqid1 21609
[Quine] p. 41Theorem 6.5eqcom 2389
[Quine] p. 42Theorem 6.6df-sbc 3105
[Quine] p. 42Theorem 6.7dfsbcq 3106  dfsbcq2 3107
[Quine] p. 43Theorem 6.8vex 2902
[Quine] p. 43Theorem 6.9isset 2903
[Quine] p. 44Theorem 7.3spcgf 2974  spcgv 2979  spcimgf 2972
[Quine] p. 44Theorem 6.11spsbc 3116  spsbcd 3117
[Quine] p. 44Theorem 6.12elex 2907
[Quine] p. 44Theorem 6.13elab 3025  elabg 3026  elabgf 3023
[Quine] p. 44Theorem 6.14noel 3575
[Quine] p. 48Theorem 7.2snprc 3814
[Quine] p. 48Definition 7.1df-pr 3764  df-sn 3763
[Quine] p. 49Theorem 7.4snss 3869  snssg 3875
[Quine] p. 49Theorem 7.5prss 3895  prssg 3896
[Quine] p. 49Theorem 7.6prid1 3855  prid1g 3853  prid2 3856  prid2g 3854  snid 3784  snidg 3782
[Quine] p. 51Theorem 7.13prex 4347  snex 4346  snexALT 4326
[Quine] p. 53Theorem 8.2unisn 3973  unisnALT 28379  unisng 3974
[Quine] p. 53Theorem 8.3uniun 3976
[Quine] p. 54Theorem 8.6elssuni 3985
[Quine] p. 54Theorem 8.7uni0 3984
[Quine] p. 56Theorem 8.17uniabio 5368
[Quine] p. 56Definition 8.18dfiota2 5359
[Quine] p. 57Theorem 8.19iotaval 5369
[Quine] p. 57Theorem 8.22iotanul 5373
[Quine] p. 58Theorem 8.23iotaex 5375
[Quine] p. 58Definition 9.1df-op 3766
[Quine] p. 61Theorem 9.5opabid 4402  opelopab 4417  opelopaba 4412  opelopabaf 4419  opelopabf 4420  opelopabg 4414  opelopabga 4409  oprabid 6044
[Quine] p. 64Definition 9.11df-xp 4824
[Quine] p. 64Definition 9.12df-cnv 4826
[Quine] p. 64Definition 9.15df-id 4439
[Quine] p. 65Theorem 10.3fun0 5448
[Quine] p. 65Theorem 10.4funi 5423
[Quine] p. 65Theorem 10.5funsn 5439  funsng 5437
[Quine] p. 65Definition 10.1df-fun 5396
[Quine] p. 65Definition 10.2args 5172  dffv4 5665
[Quine] p. 68Definition 10.11conventions 21558  df-fv 5402  fv2 5663
[Quine] p. 124Theorem 17.3nn0opth2 11492  nn0opth2i 11491  nn0opthi 11490  omopthi 6836
[Quine] p. 177Definition 25.2df-rdg 6604
[Quine] p. 232Equation icarddom 8362
[Quine] p. 284Axiom 39(vi)funimaex 5471  funimaexg 5470
[Quine] p. 331Axiom system NFru 3103
[ReedSimon] p. 36Definition (iii)ax-his3 22434
[ReedSimon] p. 63Exercise 4(a)df-dip 22045  polid 22509  polid2i 22507  polidi 22508
[ReedSimon] p. 63Exercise 4(b)df-ph 22162
[ReedSimon] p. 195Remarklnophm 23370  lnophmi 23369
[Retherford] p. 49Exercise 1(i)leopadd 23483
[Retherford] p. 49Exercise 1(ii)leopmul 23485  leopmuli 23484
[Retherford] p. 49Exercise 1(iv)leoptr 23488
[Retherford] p. 49Definition VI.1df-leop 23203  leoppos 23477
[Retherford] p. 49Exercise 1(iii)leoptri 23487
[Retherford] p. 49Definition of operator orderingleop3 23476
[Rudin] p. 164Equation 27efcan 12624
[Rudin] p. 164Equation 30efzval 12630
[Rudin] p. 167Equation 48absefi 12724
[Sanford] p. 39Rule 3mtp-xor 1542
[Sanford] p. 39Rule 4mpto2 1540
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 8
[Sanford] p. 39Rule says, "if ` ` is not true, and ` ` implies ` ` , then ` ` must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" mto 169
[Sanford] p. 40Rule 1mpto1 1539
[Schechter] p. 51Definition of antisymmetryintasym 5189
[Schechter] p. 51Definition of irreflexivityintirr 5192
[Schechter] p. 51Definition of symmetrycnvsym 5188
[Schechter] p. 51Definition of transitivitycotr 5186
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13738
[Schechter] p. 79Definition of Moore closuredf-mrc 13739
[Schechter] p. 82Section 4.5df-mrc 13739
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13741
[Schechter] p. 139Definition AC3dfac9 7949
[Schechter] p. 141Definition (MC)dfac11 26829
[Schechter] p. 149Axiom DC1ax-dc 8259  axdc3 8267
[Schechter] p. 187Definition of ring with unitisrng 15595  isrngo 21814
[Schechter] p. 276Remark 11.6.espan0 22892
[Schechter] p. 276Definition of spandf-span 22659  spanval 22683
[Schechter] p. 428Definition 15.35bastop1 16981
[Schwabhauser] p. 10Axiom A1axcgrrflx 25567
[Schwabhauser] p. 10Axiom A2axcgrtr 25568
[Schwabhauser] p. 10Axiom A3axcgrid 25569
[Schwabhauser] p. 11Axiom A4axsegcon 25580
[Schwabhauser] p. 11Axiom A5ax5seg 25591
[Schwabhauser] p. 11Axiom A6axbtwnid 25592
[Schwabhauser] p. 12Axiom A7axpasch 25594
[Schwabhauser] p. 12Axiom A8axlowdim2 25613
[Schwabhauser] p. 13Axiom A10axeuclid 25616
[Schwabhauser] p. 13Axiom A11axcont 25629
[Schwabhauser] p. 27Theorem 2.1cgrrflx 25635
[Schwabhauser] p. 27Theorem 2.2cgrcomim 25637
[Schwabhauser] p. 27Theorem 2.3cgrtr 25640
[Schwabhauser] p. 27Theorem 2.4cgrcoml 25644
[Schwabhauser] p. 27Theorem 2.5cgrcomr 25645
[Schwabhauser] p. 28Theorem 2.8cgrtriv 25650
[Schwabhauser] p. 28Theorem 2.105segofs 25654
[Schwabhauser] p. 28Definition 2.10df-ofs 25631
[Schwabhauser] p. 29Theorem 2.11cgrextend 25656
[Schwabhauser] p. 29Theorem 2.12segconeq 25658
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 25670  btwntriv2 25660
[Schwabhauser] p. 30Theorem 3.2btwncomim 25661
[Schwabhauser] p. 30Theorem 3.3btwntriv1 25664
[Schwabhauser] p. 30Theorem 3.4btwnswapid 25665
[Schwabhauser] p. 30Theorem 3.5btwnexch2 25671  btwnintr 25667
[Schwabhauser] p. 30Theorem 3.6btwnexch 25673  btwnexch3 25668
[Schwabhauser] p. 30Theorem 3.7btwnouttr 25672
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25612
[Schwabhauser] p. 32Theorem 3.14btwndiff 25675
[Schwabhauser] p. 33Theorem 3.17trisegint 25676
[Schwabhauser] p. 34Theorem 4.2ifscgr 25692
[Schwabhauser] p. 34Definition 4.1df-ifs 25687
[Schwabhauser] p. 35Theorem 4.3cgrsub 25693
[Schwabhauser] p. 35Theorem 4.5cgrxfr 25703
[Schwabhauser] p. 35Definition 4.4df-cgr3 25688
[Schwabhauser] p. 36Theorem 4.6btwnxfr 25704
[Schwabhauser] p. 36Theorem 4.11colinearperm1 25710  colinearperm2 25712  colinearperm3 25711  colinearperm4 25713  colinearperm5 25714
[Schwabhauser] p. 36Definition 4.10df-colinear 25689
[Schwabhauser] p. 37Theorem 4.12colineartriv1 25715
[Schwabhauser] p. 37Theorem 4.13colinearxfr 25723
[Schwabhauser] p. 37Theorem 4.14lineext 25724
[Schwabhauser] p. 37Theorem 4.16fscgr 25728
[Schwabhauser] p. 37Theorem 4.17linecgr 25729
[Schwabhauser] p. 37Definition 4.15df-fs 25690
[Schwabhauser] p. 38Theorem 4.18lineid 25731
[Schwabhauser] p. 38Theorem 4.19idinside 25732
[Schwabhauser] p. 39Theorem 5.1btwnconn1 25749
[Schwabhauser] p. 41Theorem 5.2btwnconn2 25750
[Schwabhauser] p. 41Theorem 5.3btwnconn3 25751
[Schwabhauser] p. 41Theorem 5.5brsegle2 25757
[Schwabhauser] p. 41Definition 5.4df-segle 25755
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 25758
[Schwabhauser] p. 42Theorem 5.7seglerflx 25760
[Schwabhauser] p. 42Theorem 5.8segletr 25762
[Schwabhauser] p. 42Theorem 5.9segleantisym 25763
[Schwabhauser] p. 42Theorem 5.10seglelin 25764
[Schwabhauser] p. 42Theorem 5.11seglemin 25761
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 25766
[Schwabhauser] p. 43Theorem 6.2btwnoutside 25773
[Schwabhauser] p. 43Theorem 6.3broutsideof3 25774
[Schwabhauser] p. 43Theorem 6.4broutsideof 25769  df-outsideof 25768
[Schwabhauser] p. 43Definition 6.1broutsideof2 25770
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 25775
[Schwabhauser] p. 44Theorem 6.6outsideofcom 25776
[Schwabhauser] p. 44Theorem 6.7outsideoftr 25777
[Schwabhauser] p. 44Theorem 6.11outsideofeu 25779
[Schwabhauser] p. 44Definition 6.8df-ray 25786
[Schwabhauser] p. 45Part 2df-lines2 25787
[Schwabhauser] p. 45Theorem 6.13outsidele 25780
[Schwabhauser] p. 45Theorem 6.15lineunray 25795
[Schwabhauser] p. 45Theorem 6.16lineelsb2 25796
[Schwabhauser] p. 45Theorem 6.17linecom 25798  linerflx1 25797  linerflx2 25799
[Schwabhauser] p. 45Theorem 6.18linethru 25801
[Schwabhauser] p. 45Definition 6.14df-line2 25785
[Schwabhauser] p. 46Theorem 6.19linethrueu 25804
[Schwabhauser] p. 46Theorem 6.21lineintmo 25805
[Shapiro] p. 230Theorem 6.5.1dchrhash 20922  dchrsum 20920  dchrsum2 20919  sumdchr 20923
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20924  sum2dchr 20925
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15551  ablfacrp2 15552
[Shapiro], p. 328Equation 9.2.4vmasum 20867
[Shapiro], p. 329Equation 9.2.7logfac2 20868
[Shapiro], p. 329Equation 9.2.9logfacrlim 20875
[Shapiro], p. 331Equation 9.2.13vmadivsum 21043
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 21046
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 21100  vmalogdivsum2 21099
[Shapiro], p. 375Theorem 9.4.1dirith 21090  dirith2 21089
[Shapiro], p. 375Equation 9.4.3rplogsum 21088  rpvmasum 21087  rpvmasum2 21073
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 21048
[Shapiro], p. 376Equation 9.4.8dchrvmasum 21086
[Shapiro], p. 377Lemma 9.4.1dchrisum 21053  dchrisumlem1 21050  dchrisumlem2 21051  dchrisumlem3 21052  dchrisumlema 21049
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 21056
[Shapiro], p. 379Equation 9.4.16dchrmusum 21085  dchrmusumlem 21083  dchrvmasumlem 21084
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 21055
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 21057
[Shapiro], p. 382Lemma 9.4.4dchrisum0 21081  dchrisum0re 21074  dchrisumn0 21082
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 21067
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 21071
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 21072
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 21127  pntrsumbnd2 21128  pntrsumo1 21126
[Shapiro], p. 405Equation 10.2.1mudivsum 21091
[Shapiro], p. 406Equation 10.2.6mulogsum 21093
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 21095
[Shapiro], p. 407Equation 10.2.8mulog2sum 21098
[Shapiro], p. 418Equation 10.4.6logsqvma 21103
[Shapiro], p. 418Equation 10.4.8logsqvma2 21104
[Shapiro], p. 419Equation 10.4.10selberg 21109
[Shapiro], p. 420Equation 10.4.12selberg2lem 21111
[Shapiro], p. 420Equation 10.4.14selberg2 21112
[Shapiro], p. 422Equation 10.6.7selberg3 21120
[Shapiro], p. 422Equation 10.4.20selberg4lem1 21121
[Shapiro], p. 422Equation 10.4.21selberg3lem1 21118  selberg3lem2 21119
[Shapiro], p. 422Equation 10.4.23selberg4 21122
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 21116
[Shapiro], p. 428Equation 10.6.2selbergr 21129
[Shapiro], p. 429Equation 10.6.8selberg3r 21130
[Shapiro], p. 430Equation 10.6.11selberg4r 21131
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 21145
[Shapiro], p. 434Equation 10.6.27pntlema 21157  pntlemb 21158  pntlemc 21156  pntlemd 21155  pntlemg 21159
[Shapiro], p. 435Equation 10.6.29pntlema 21157
[Shapiro], p. 436Lemma 10.6.1pntpbnd 21149
[Shapiro], p. 436Lemma 10.6.2pntibnd 21154
[Shapiro], p. 436Equation 10.6.34pntlema 21157
[Shapiro], p. 436Equation 10.6.35pntlem3 21170  pntleml 21172
[Stoll] p. 13Definition of symmetric differencesymdif1 3549
[Stoll] p. 16Exercise 4.40dif 3642  dif0 3641
[Stoll] p. 16Exercise 4.8difdifdir 3658
[Stoll] p. 17Theorem 5.1(5)undifv 3645
[Stoll] p. 19Theorem 5.2(13)undm 3542
[Stoll] p. 19Theorem 5.2(13')indm 3543
[Stoll] p. 20Remarkinvdif 3525
[Stoll] p. 25Definition of ordered tripledf-ot 3767
[Stoll] p. 43Definitionuniiun 4085
[Stoll] p. 44Definitionintiin 4086
[Stoll] p. 45Definitiondf-iin 4038
[Stoll] p. 45Definition indexed uniondf-iun 4037
[Stoll] p. 176Theorem 3.4(27)iman 414
[Stoll] p. 262Example 4.1symdif1 3549
[Strang] p. 242Section 6.3expgrowth 27221
[Suppes] p. 22Theorem 2eq0 3585
[Suppes] p. 22Theorem 4eqss 3306  eqssd 3308  eqssi 3307
[Suppes] p. 23Theorem 5ss0 3601  ss0b 3600
[Suppes] p. 23Theorem 6sstr 3299  sstrALT2 28288
[Suppes] p. 23Theorem 7pssirr 3390
[Suppes] p. 23Theorem 8pssn2lp 3391
[Suppes] p. 23Theorem 9psstr 3394
[Suppes] p. 23Theorem 10pssss 3385
[Suppes] p. 25Theorem 12elin 3473  elun 3431
[Suppes] p. 26Theorem 15inidm 3493
[Suppes] p. 26Theorem 16in0 3596
[Suppes] p. 27Theorem 23unidm 3433
[Suppes] p. 27Theorem 24un0 3595
[Suppes] p. 27Theorem 25ssun1 3453
[Suppes] p. 27Theorem 26ssequn1 3460
[Suppes] p. 27Theorem 27unss 3464
[Suppes] p. 27Theorem 28indir 3532
[Suppes] p. 27Theorem 29undir 3533
[Suppes] p. 28Theorem 32difid 3639  difidALT 3640
[Suppes] p. 29Theorem 33difin 3521
[Suppes] p. 29Theorem 34indif 3526
[Suppes] p. 29Theorem 35undif1 3646
[Suppes] p. 29Theorem 36difun2 3650
[Suppes] p. 29Theorem 37difin0 3644
[Suppes] p. 29Theorem 38disjdif 3643
[Suppes] p. 29Theorem 39difundi 3536
[Suppes] p. 29Theorem 40difindi 3538
[Suppes] p. 30Theorem 41nalset 4281
[Suppes] p. 39Theorem 61uniss 3978
[Suppes] p. 39Theorem 65uniop 4400
[Suppes] p. 41Theorem 70intsn 4028
[Suppes] p. 42Theorem 71intpr 4025  intprg 4026
[Suppes] p. 42Theorem 73op1stb 4698
[Suppes] p. 42Theorem 78intun 4024
[Suppes] p. 44Definition 15(a)dfiun2 4067  dfiun2g 4065
[Suppes] p. 44Definition 15(b)dfiin2 4068
[Suppes] p. 47Theorem 86elpw 3748  elpw2 4305  elpw2g 4304  elpwg 3749  elpwgdedVD 28370
[Suppes] p. 47Theorem 87pwid 3755
[Suppes] p. 47Theorem 89pw0 3888
[Suppes] p. 48Theorem 90pwpw0 3889
[Suppes] p. 52Theorem 101xpss12 4921
[Suppes] p. 52Theorem 102xpindi 4948  xpindir 4949
[Suppes] p. 52Theorem 103xpundi 4870  xpundir 4871
[Suppes] p. 54Theorem 105elirrv 7498
[Suppes] p. 58Theorem 2relss 4903
[Suppes] p. 59Theorem 4eldm 5007  eldm2 5008  eldm2g 5006  eldmg 5005
[Suppes] p. 59Definition 3df-dm 4828
[Suppes] p. 60Theorem 6dmin 5017
[Suppes] p. 60Theorem 8rnun 5220
[Suppes] p. 60Theorem 9rnin 5221
[Suppes] p. 60Definition 4dfrn2 4999
[Suppes] p. 61Theorem 11brcnv 4995  brcnvg 4993
[Suppes] p. 62Equation 5elcnv 4989  elcnv2 4990
[Suppes] p. 62Theorem 12relcnv 5182
[Suppes] p. 62Theorem 15cnvin 5219
[Suppes] p. 62Theorem 16cnvun 5217
[Suppes] p. 63Theorem 20co02 5323
[Suppes] p. 63Theorem 21dmcoss 5075
[Suppes] p. 63Definition 7df-co 4827
[Suppes] p. 64Theorem 26cnvco 4996
[Suppes] p. 64Theorem 27coass 5328
[Suppes] p. 65Theorem 31resundi 5100
[Suppes] p. 65Theorem 34elima 5148  elima2 5149  elima3 5150  elimag 5147
[Suppes] p. 65Theorem 35imaundi 5224
[Suppes] p. 66Theorem 40dminss 5226
[Suppes] p. 66Theorem 41imainss 5227
[Suppes] p. 67Exercise 11cnvxp 5230
[Suppes] p. 81Definition 34dfec2 6844
[Suppes] p. 82Theorem 72elec 6880  elecg 6879
[Suppes] p. 82Theorem 73erth 6885  erth2 6886
[Suppes] p. 83Theorem 74erdisj 6888
[Suppes] p. 89Theorem 96map0b 6988
[Suppes] p. 89Theorem 97map0 6990  map0g 6989
[Suppes] p. 89Theorem 98mapsn 6991
[Suppes] p. 89Theorem 99mapss 6992
[Suppes] p. 91Definition 12(ii)alephsuc 7882
[Suppes] p. 91Definition 12(iii)alephlim 7881
[Suppes] p. 92Theorem 1enref 7076  enrefg 7075
[Suppes] p. 92Theorem 2ensym 7092  ensymb 7091  ensymi 7093
[Suppes] p. 92Theorem 3entr 7095
[Suppes] p. 92Theorem 4unen 7125
[Suppes] p. 94Theorem 15endom 7070
[Suppes] p. 94Theorem 16ssdomg 7089
[Suppes] p. 94Theorem 17domtr 7096
[Suppes] p. 95Theorem 18sbth 7163
[Suppes] p. 97Theorem 23canth2 7196  canth2g 7197
[Suppes] p. 97Definition 3brsdom2 7167  df-sdom 7048  dfsdom2 7166
[Suppes] p. 97Theorem 21(i)sdomirr 7180
[Suppes] p. 97Theorem 22(i)domnsym 7169
[Suppes] p. 97Theorem 21(ii)sdomnsym 7168
[Suppes] p. 97Theorem 22(ii)domsdomtr 7178
[Suppes] p. 97Theorem 22(iv)brdom2 7073
[Suppes] p. 97Theorem 21(iii)sdomtr 7181
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7176
[Suppes] p. 98Exercise 4fundmen 7116  fundmeng 7117
[Suppes] p. 98Exercise 6xpdom3 7142
[Suppes] p. 98Exercise 11sdomentr 7177
[Suppes] p. 104Theorem 37fofi 7328
[Suppes] p. 104Theorem 38pwfi 7337
[Suppes] p. 105Theorem 40pwfi 7337
[Suppes] p. 111Axiom for cardinal numberscarden 8359
[Suppes] p. 130Definition 3df-tr 4244
[Suppes] p. 132Theorem 9ssonuni 4707
[Suppes] p. 134Definition 6df-suc 4528
[Suppes] p. 136Theorem Schema 22findes 4815  finds 4811  finds1 4814  finds2 4813
[Suppes] p. 151Theorem 42isfinite 7540  isfinite2 7301  isfiniteg 7303  unbnn 7299
[Suppes] p. 162Definition 5df-ltnq 8728  df-ltpq 8720
[Suppes] p. 197Theorem Schema 4tfindes 4782  tfinds 4779  tfinds2 4783
[Suppes] p. 209Theorem 18oaord1 6730
[Suppes] p. 209Theorem 21oaword2 6732
[Suppes] p. 211Theorem 25oaass 6740
[Suppes] p. 225Definition 8iscard2 7796
[Suppes] p. 227Theorem 56ondomon 8371
[Suppes] p. 228Theorem 59harcard 7798
[Suppes] p. 228Definition 12(i)aleph0 7880
[Suppes] p. 228Theorem Schema 61onintss 4572
[Suppes] p. 228Theorem Schema 62onminesb 4718  onminsb 4719
[Suppes] p. 229Theorem 64alephval2 8380
[Suppes] p. 229Theorem 65alephcard 7884
[Suppes] p. 229Theorem 66alephord2i 7891
[Suppes] p. 229Theorem 67alephnbtwn 7885
[Suppes] p. 229Definition 12df-aleph 7760
[Suppes] p. 242Theorem 6weth 8308
[Suppes] p. 242Theorem 8entric 8365
[Suppes] p. 242Theorem 9carden 8359
[TakeutiZaring] p. 8Axiom 1ax-ext 2368
[TakeutiZaring] p. 13Definition 4.5df-cleq 2380
[TakeutiZaring] p. 13Proposition 4.6df-clel 2383
[TakeutiZaring] p. 13Proposition 4.9cvjust 2382
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2404
[TakeutiZaring] p. 14Definition 4.16df-oprab 6024
[TakeutiZaring] p. 14Proposition 4.14ru 3103
[TakeutiZaring] p. 15Axiom 2zfpair 4342
[TakeutiZaring] p. 15Exercise 1elpr 3775  elpr2 3776  elprg 3774
[TakeutiZaring] p. 15Exercise 2elsn 3772  elsnc 3780  elsnc2 3786  elsnc2g 3785  elsncg 3779
[TakeutiZaring] p. 15Exercise 3elop 4370
[TakeutiZaring] p. 15Exercise 4sneq 3768  sneqr 3908
[TakeutiZaring] p. 15Definition 5.1dfpr2 3773  dfsn2 3771
[TakeutiZaring] p. 16Axiom 3uniex 4645
[TakeutiZaring] p. 16Exercise 6opth 4376
[TakeutiZaring] p. 16Exercise 7opex 4368
[TakeutiZaring] p. 16Exercise 8rext 4353
[TakeutiZaring] p. 16Corollary 5.8unex 4647  unexg 4650
[TakeutiZaring] p. 16Definition 5.3dftp2 3797
[TakeutiZaring] p. 16Definition 5.5df-uni 3958
[TakeutiZaring] p. 16Definition 5.6df-in 3270  df-un 3268
[TakeutiZaring] p. 16Proposition 5.7unipr 3971  uniprg 3972
[TakeutiZaring] p. 17Axiom 4pwex 4323  pwexg 4324
[TakeutiZaring] p. 17Exercise 1eltp 3796
[TakeutiZaring] p. 17Exercise 5elsuc 4591  elsucg 4589  sstr2 3298
[TakeutiZaring] p. 17Exercise 6uncom 3434
[TakeutiZaring] p. 17Exercise 7incom 3476
[TakeutiZaring] p. 17Exercise 8unass 3447
[TakeutiZaring] p. 17Exercise 9inass 3494
[TakeutiZaring] p. 17Exercise 10indi 3530
[TakeutiZaring] p. 17Exercise 11undi 3531
[TakeutiZaring] p. 17Definition 5.9df-pss 3279  dfss2 3280
[TakeutiZaring] p. 17Definition 5.10df-pw 3744
[TakeutiZaring] p. 18Exercise 7unss2 3461
[TakeutiZaring] p. 18Exercise 9df-ss 3277  sseqin2 3503
[TakeutiZaring] p. 18Exercise 10ssid 3310
[TakeutiZaring] p. 18Exercise 12inss1 3504  inss2 3505
[TakeutiZaring] p. 18Exercise 13nss 3349
[TakeutiZaring] p. 18Exercise 15unieq 3966
[TakeutiZaring] p. 18Exercise 18sspwb 4354  sspwimp 28371  sspwimpALT 28378  sspwimpALT2 28382  sspwimpcf 28373
[TakeutiZaring] p. 18Exercise 19pweqb 4361
[TakeutiZaring] p. 19Axiom 5ax-rep 4261
[TakeutiZaring] p. 20Definitiondf-rab 2658
[TakeutiZaring] p. 20Corollary 5.160ex 4280
[TakeutiZaring] p. 20Definition 5.12df-dif 3266
[TakeutiZaring] p. 20Definition 5.14dfnul2 3573
[TakeutiZaring] p. 20Proposition 5.15difid 3639  difidALT 3640
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3580  n0f 3579  neq0 3581
[TakeutiZaring] p. 21Axiom 6zfreg 7496
[TakeutiZaring] p. 21Axiom 6'zfregs 7601
[TakeutiZaring] p. 21Theorem 5.22setind 7606
[TakeutiZaring] p. 21Definition 5.20df-v 2901
[TakeutiZaring] p. 21Proposition 5.21vprc 4282
[TakeutiZaring] p. 22Exercise 10ss 3599
[TakeutiZaring] p. 22Exercise 3ssex 4288  ssexg 4290
[TakeutiZaring] p. 22Exercise 4inex1 4285
[TakeutiZaring] p. 22Exercise 5ruv 7501
[TakeutiZaring] p. 22Exercise 6elirr 7499
[TakeutiZaring] p. 22Exercise 7ssdif0 3629
[TakeutiZaring] p. 22Exercise 11difdif 3416
[TakeutiZaring] p. 22Exercise 13undif3 3545  undif3VD 28335
[TakeutiZaring] p. 22Exercise 14difss 3417
[TakeutiZaring] p. 22Exercise 15sscon 3424
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2654
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2655
[TakeutiZaring] p. 23Proposition 6.2xpex 4930  xpexg 4929  xpexgALT 6236
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4825
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5453
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5587  fun11 5456
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5406  svrelfun 5454
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4998
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5000
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4830
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4831
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4827
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5265  dfrel2 5261
[TakeutiZaring] p. 25Exercise 3xpss 4922
[TakeutiZaring] p. 25Exercise 5relun 4931
[TakeutiZaring] p. 25Exercise 6reluni 4937
[TakeutiZaring] p. 25Exercise 9inxp 4947
[TakeutiZaring] p. 25Exercise 12relres 5114
[TakeutiZaring] p. 25Exercise 13opelres 5091  opelresg 5093
[TakeutiZaring] p. 25Exercise 14dmres 5107
[TakeutiZaring] p. 25Exercise 15resss 5110
[TakeutiZaring] p. 25Exercise 17resabs1 5115
[TakeutiZaring] p. 25Exercise 18funres 5432
[TakeutiZaring] p. 25Exercise 24relco 5308
[TakeutiZaring] p. 25Exercise 29funco 5431
[TakeutiZaring] p. 25Exercise 30f1co 5588
[TakeutiZaring] p. 26Definition 6.10eu2 2263
[TakeutiZaring] p. 26Definition 6.11conventions 21558  df-fv 5402  fv3 5684
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5346  cnvexg 5345
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5072  dmexg 5070
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5073  rnexg 5071
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27326
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27327
[TakeutiZaring] p. 27Corollary 6.13fvex 5682
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 27707  tz6.12-1 5687  tz6.12-afv 27706  tz6.12 5688  tz6.12c 5690
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5659  tz6.12i 5691
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5397
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5398
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5400  wfo 5392
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5399  wf1 5391
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5401  wf1o 5393
[TakeutiZaring] p. 28Exercise 4eqfnfv 5766  eqfnfv2 5767  eqfnfv2f 5770
[TakeutiZaring] p. 28Exercise 5fvco 5738
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5900  fnexALT 5901
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5896  resfunexgALT 5897
[TakeutiZaring] p. 29Exercise 9funimaex 5471  funimaexg 5470
[TakeutiZaring] p. 29Definition 6.18df-br 4154
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4445
[TakeutiZaring] p. 30Definition 6.21dffr2 4488  dffr3 5176  eliniseg 5173  iniseg 5175
[TakeutiZaring] p. 30Definition 6.22df-eprel 4435
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4501  fr3nr 4700  frirr 4500
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4482
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4702
[TakeutiZaring] p. 31Exercise 1frss 4490
[TakeutiZaring] p. 31Exercise 4wess 4510
[TakeutiZaring] p. 31Proposition 6.26tz6.26 25229  tz6.26i 25230  wefrc 4517  wereu2 4520
[TakeutiZaring] p. 32Theorem 6.27wfi 25231  wfii 25232
[TakeutiZaring] p. 32Definition 6.28df-isom 5403
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5988
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5989
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5995
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5996
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5997
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6001
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6008
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6010
[TakeutiZaring] p. 35Notationwtr 4243
[TakeutiZaring] p. 35Theorem 7.2trelpss 27328  tz7.2 4507
[TakeutiZaring] p. 35Definition 7.1dftr3 4247
[TakeutiZaring] p. 36Proposition 7.4ordwe 4535
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4543
[TakeutiZaring] p. 36Proposition 7.6ordelord 4544  ordelordALT 27965  ordelordALTVD 28320
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4550  ordelssne 4549
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4548
[TakeutiZaring] p. 37Proposition 7.9ordin 4552
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4709
[TakeutiZaring] p. 38Corollary 7.15ordsson 4710
[TakeutiZaring] p. 38Definition 7.11df-on 4526
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4554
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27978  ordon 4703
[TakeutiZaring] p. 38Proposition 7.13onprc 4705
[TakeutiZaring] p. 39Theorem 7.17tfi 4773
[TakeutiZaring] p. 40Exercise 3ontr2 4569
[TakeutiZaring] p. 40Exercise 7dftr2 4245
[TakeutiZaring] p. 40Exercise 9onssmin 4717
[TakeutiZaring] p. 40Exercise 11unon 4751
[TakeutiZaring] p. 40Exercise 12ordun 4623
[TakeutiZaring] p. 40Exercise 14ordequn 4622
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4706
[TakeutiZaring] p. 40Proposition 7.20elssuni 3985
[TakeutiZaring] p. 41Definition 7.22df-suc 4528
[TakeutiZaring] p. 41Proposition 7.23sssucid 4599  sucidg 4600
[TakeutiZaring] p. 41Proposition 7.24suceloni 4733
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4613  ordnbtwn 4612
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4748
[TakeutiZaring] p. 42Exercise 1df-lim 4527
[TakeutiZaring] p. 42Exercise 4omssnlim 4799
[TakeutiZaring] p. 42Exercise 7ssnlim 4803
[TakeutiZaring] p. 42Exercise 8onsucssi 4761  ordelsuc 4740
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4742
[TakeutiZaring] p. 42Definition 7.27nlimon 4771
[TakeutiZaring] p. 42Definition 7.28dfom2 4787
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4804
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4805
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4806
[TakeutiZaring] p. 43Remarkomon 4796
[TakeutiZaring] p. 43Axiom 7inf3 7523  omex 7531
[TakeutiZaring] p. 43Theorem 7.32ordom 4794
[TakeutiZaring] p. 43Corollary 7.31find 4810
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4807
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4808
[TakeutiZaring] p. 44Exercise 1limomss 4790
[TakeutiZaring] p. 44Exercise 2int0 4006  trint0 4260
[TakeutiZaring] p. 44Exercise 4intss1 4007
[TakeutiZaring] p. 44Exercise 5intex 4297
[TakeutiZaring] p. 44Exercise 6oninton 4720
[TakeutiZaring] p. 44Exercise 11ordintdif 4571
[TakeutiZaring] p. 44Definition 7.35df-int 3993
[TakeutiZaring] p. 44Proposition 7.34noinfep 7547
[TakeutiZaring] p. 45Exercise 4onint 4715
[TakeutiZaring] p. 47Lemma 1tfrlem1 6572
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6594
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6595
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6596
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6600  tz7.44-2 6601  tz7.44-3 6602
[TakeutiZaring] p. 50Exercise 1smogt 6565
[TakeutiZaring] p. 50Exercise 3smoiso 6560
[TakeutiZaring] p. 50Definition 7.46df-smo 6544
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6638  tz7.49c 6639
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6636
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6635
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6637
[TakeutiZaring] p. 53Proposition 7.532eu5 2322
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7826
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7827
[TakeutiZaring] p. 56Definition 8.1oalim 6712  oasuc 6704
[TakeutiZaring] p. 57Remarktfindsg 4780
[TakeutiZaring] p. 57Proposition 8.2oacl 6715
[TakeutiZaring] p. 57Proposition 8.3oa0 6696  oa0r 6718
[TakeutiZaring] p. 57Proposition 8.16omcl 6716
[TakeutiZaring] p. 58Corollary 8.5oacan 6727
[TakeutiZaring] p. 58Proposition 8.4nnaord 6798  nnaordi 6797  oaord 6726  oaordi 6725
[TakeutiZaring] p. 59Proposition 8.6iunss2 4077  uniss2 3988
[TakeutiZaring] p. 59Proposition 8.7oawordri 6729
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6734  oawordex 6736
[TakeutiZaring] p. 59Proposition 8.9nnacl 6790
[TakeutiZaring] p. 59Proposition 8.10oaabs 6823
[TakeutiZaring] p. 60Remarkoancom 7539
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6739
[TakeutiZaring] p. 62Exercise 1nnarcl 6795
[TakeutiZaring] p. 62Exercise 5oaword1 6731
[TakeutiZaring] p. 62Definition 8.15om0 6697  om0x 6699  omlim 6713  omsuc 6706
[TakeutiZaring] p. 63Proposition 8.17nnecl 6792  nnmcl 6791
[TakeutiZaring] p. 63Proposition 8.19nnmord 6811  nnmordi 6810  omord 6747  omordi 6745
[TakeutiZaring] p. 63Proposition 8.20omcan 6748
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6815  omwordri 6751
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6719
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6721  om1r 6722
[TakeutiZaring] p. 64Proposition 8.22om00 6754
[TakeutiZaring] p. 64Proposition 8.23omordlim 6756
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6757
[TakeutiZaring] p. 64Proposition 8.25odi 6758
[TakeutiZaring] p. 65Theorem 8.26omass 6759
[TakeutiZaring] p. 67Definition 8.30nnesuc 6787  oe0 6702  oelim 6714  oesuc 6707  onesuc 6710
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6700
[TakeutiZaring] p. 67Proposition 8.32oen0 6765
[TakeutiZaring] p. 67Proposition 8.33oeordi 6766
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6701
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6724
[TakeutiZaring] p. 68Corollary 8.34oeord 6767
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6773
[TakeutiZaring] p. 68Proposition 8.35oewordri 6771
[TakeutiZaring] p. 68Proposition 8.37oeworde 6772
[TakeutiZaring] p. 69Proposition 8.41oeoa 6776
[TakeutiZaring] p. 70Proposition 8.42oeoe 6778
[TakeutiZaring] p. 73Theorem 9.1trcl 7597  tz9.1 7598
[TakeutiZaring] p. 76Definition 9.9df-r1 7623  r10 7627  r1lim 7631  r1limg 7630  r1suc 7629  r1sucg 7628
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7639  r1ord2 7640  r1ordg 7637
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7649
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7674  tz9.13 7650  tz9.13g 7651
[TakeutiZaring] p. 79Definition 9.14df-rank 7624  rankval 7675  rankvalb 7656  rankvalg 7676
[TakeutiZaring] p. 79Proposition 9.16rankel 7698  rankelb 7683
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7712  rankval3 7699  rankval3b 7685
[TakeutiZaring] p. 79Proposition 9.18rankonid 7688
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7654
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7693  rankr1c 7680  rankr1g 7691
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7694
[TakeutiZaring] p. 80Exercise 1rankss 7708  rankssb 7707
[TakeutiZaring] p. 80Exercise 2unbndrank 7701
[TakeutiZaring] p. 80Proposition 9.19bndrank 7700
[TakeutiZaring] p. 83Axiom of Choiceac4 8288  dfac3 7935
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7844  numth 8285  numth2 8284
[TakeutiZaring] p. 85Definition 10.4cardval 8354
[TakeutiZaring] p. 85Proposition 10.5cardid 8355  cardid2 7773
[TakeutiZaring] p. 85Proposition 10.9oncard 7780
[TakeutiZaring] p. 85Proposition 10.10carden 8359
[TakeutiZaring] p. 85Proposition 10.11cardidm 7779
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7764
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7785
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7777
[TakeutiZaring] p. 87Proposition 10.15pwen 7216
[TakeutiZaring] p. 88Exercise 1en0 7106
[TakeutiZaring] p. 88Exercise 7infensuc 7221
[TakeutiZaring] p. 89Exercise 10omxpen 7146
[TakeutiZaring] p. 90Corollary 10.23cardnn 7783
[TakeutiZaring] p. 90Definition 10.27alephiso 7912
[TakeutiZaring] p. 90Proposition 10.20nneneq 7226
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7232
[TakeutiZaring] p. 90Proposition 10.26alephprc 7913
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7231
[TakeutiZaring] p. 91Exercise 2alephle 7902
[TakeutiZaring] p. 91Exercise 3aleph0 7880
[TakeutiZaring] p. 91Exercise 4cardlim 7792
[TakeutiZaring] p. 91Exercise 7infpss 8030
[TakeutiZaring] p. 91Exercise 8infcntss 7316
[TakeutiZaring] p. 91Definition 10.29df-fin 7049  isfi 7067
[TakeutiZaring] p. 92Proposition 10.32onfin 7233
[TakeutiZaring] p. 92Proposition 10.34imadomg 8345
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 7139
[TakeutiZaring] p. 93Proposition 10.35fodomb 8337
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8002  unxpdom 7252
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7794  cardsdomelir 7793
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7254
[TakeutiZaring] p. 94Proposition 10.39infxpen 7829
[TakeutiZaring] p. 95Definition 10.42df-map 6956
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8370  infxpidm2 7831
[TakeutiZaring] p. 95Proposition 10.41infcda 8021  infxp 8028
[TakeutiZaring] p. 96Proposition 10.44pw2en 7151  pw2f1o 7149
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7209
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8300
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8295  ac6s5 8304
[TakeutiZaring] p. 98Theorem 10.47unidom 8351
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8352  uniimadomf 8353
[TakeutiZaring] p. 100Definition 11.1cfcof 8087
[TakeutiZaring] p. 101Proposition 11.7cofsmo 8082
[TakeutiZaring] p. 102Exercise 1cfle 8067
[TakeutiZaring] p. 102Exercise 2cf0 8064
[TakeutiZaring] p. 102Exercise 3cfsuc 8070
[TakeutiZaring] p. 102Exercise 4cfom 8077
[TakeutiZaring] p. 102Proposition 11.9coftr 8086
[TakeutiZaring] p. 103Theorem 11.15alephreg 8390
[TakeutiZaring] p. 103Proposition 11.11cardcf 8065
[TakeutiZaring] p. 103Proposition 11.13alephsing 8089
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7911
[TakeutiZaring] p. 104Proposition 11.16carduniima 7910
[TakeutiZaring] p. 104Proposition 11.18alephfp 7922  alephfp2 7923
[TakeutiZaring] p. 106Theorem 11.20gchina 8507
[TakeutiZaring] p. 106Theorem 11.21mappwen 7926
[TakeutiZaring] p. 107Theorem 11.26konigth 8377
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8391
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8392
[Tarski] p. 67Axiom B5ax-4 2169
[Tarski] p. 67Scheme B5sp 1755
[Tarski] p. 68Lemma 6avril1 21605  equid 1683  equid1 2192  equid1ALT 2210
[Tarski] p. 69Lemma 7equcomi 1686
[Tarski] p. 70Lemma 14spim 1948  spime 1950  spimeh 1674
[Tarski] p. 70Lemma 16ax-11 1753  ax-11o 2175  ax11i 1654
[Tarski] p. 70Lemmas 16 and 17sb6 2132
[Tarski] p. 75Axiom B7ax9v 1662
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1623  ax17o 2191
[Tarski], p. 75Scheme B8 of system S2ax-13 1719  ax-14 1721  ax-8 1682
[Truss] p. 114Theorem 5.18ruc 12769
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 500
[WhiteheadRussell] p. 96Axiom *1.3olc 374
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 376
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 509
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 815
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 162
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 110
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 78
[WhiteheadRussell] p. 100Theorem *2.05imim2 51
[WhiteheadRussell] p. 100Theorem *2.06imim1 72
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 407
[WhiteheadRussell] p. 101Theorem *2.06barbara 2335  syl 16
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 386
[WhiteheadRussell] p. 101Theorem *2.08id 20  id1 21
[WhiteheadRussell] p. 101Theorem *2.11exmid 405
[WhiteheadRussell] p. 101Theorem *2.12notnot1 116
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 408
[WhiteheadRussell] p. 102Theorem *2.14notnot2 106  notnot2ALT2 28380
[WhiteheadRussell] p. 102Theorem *2.15con1 122
[WhiteheadRussell] p. 103Theorem *2.16con3 128  con3th 925
[WhiteheadRussell] p. 103Theorem *2.17ax-3 7
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 104
[WhiteheadRussell] p. 104Theorem *2.2orc 375
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 556
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 102
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 103
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 394
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 854
[WhiteheadRussell] p. 104Theorem *2.27conventions 21558  pm2.27 37
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 512
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 513
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 817
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 818
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 816
[WhiteheadRussell] p. 105Definition *2.33df-3or 937
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 559
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 557
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 558
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 49
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 387
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 388
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 146
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 164
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 389
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 390
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 391
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 147
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 149
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 363
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 364
[WhiteheadRussell] p. 107Theorem *2.55orel1 372
[WhiteheadRussell] p. 107Theorem *2.56orel2 373
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 165
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 399
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 764
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 765
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 166
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 392  pm2.67 393
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 148
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 398
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 824
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 400
[WhiteheadRussell] p. 108Theorem *2.69looinv 175
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 819
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 820
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 823
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 822
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 825
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 826
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 73
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 827
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 96
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 485
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 435  pm3.2im 139
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 486
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 487
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 488
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 489
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 436
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 437
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 853
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 571
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 432
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 433
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 444  simplim 145
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 448  simprim 144
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 569
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 570
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 563
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 545
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 543
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 544
[WhiteheadRussell] p. 113Theorem *3.44jao 499  pm3.44 498
[WhiteheadRussell] p. 113Theorem *3.47prth 555
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 833
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 808
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 807
[WhiteheadRussell] p. 116Theorem *4.1con34b 284
[WhiteheadRussell] p. 117Theorem *4.2biid 228
[WhiteheadRussell] p. 117Theorem *4.11notbi 287
[WhiteheadRussell] p. 117Theorem *4.12con2bi 319
[WhiteheadRussell] p. 117Theorem *4.13notnot 283
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 562
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 565
[WhiteheadRussell] p. 117Theorem *4.21bicom 192
[WhiteheadRussell] p. 117Theorem *4.22biantr 898  bitr 690  wl-bitr 25944
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 625
[WhiteheadRussell] p. 117Theorem *4.25oridm 501  pm4.25 502
[WhiteheadRussell] p. 118Theorem *4.3ancom 438
[WhiteheadRussell] p. 118Theorem *4.4andi 838
[WhiteheadRussell] p. 118Theorem *4.31orcom 377
[WhiteheadRussell] p. 118Theorem *4.32anass 631
[WhiteheadRussell] p. 118Theorem *4.33orass 511
[WhiteheadRussell] p. 118Theorem *4.36anbi1 688
[WhiteheadRussell] p. 118Theorem *4.37orbi1 687
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 843
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 842
[WhiteheadRussell] p. 118Definition *4.34df-3an 938
[WhiteheadRussell] p. 119Theorem *4.41ordi 835
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 927
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 894
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 561
[WhiteheadRussell] p. 119Theorem *4.45orabs 829  pm4.45 670  pm4.45im 546
[WhiteheadRussell] p. 120Theorem *4.5anor 476
[WhiteheadRussell] p. 120Theorem *4.6imor 402
[WhiteheadRussell] p. 120Theorem *4.7anclb 531
[WhiteheadRussell] p. 120Theorem *4.51ianor 475
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 478
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 479
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 480
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 481
[WhiteheadRussell] p. 120Theorem *4.56ioran 477  pm4.56 482
[WhiteheadRussell] p. 120Theorem *4.57oran 483  pm4.57 484
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 416
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 409
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 411
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 362
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 417
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 410
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 418
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 612  pm4.71d 616  pm4.71i 614  pm4.71r 613  pm4.71rd 617  pm4.71ri 615
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 847
[WhiteheadRussell] p. 121Theorem *4.73iba 490
[WhiteheadRussell] p. 121Theorem *4.74biorf 395
[WhiteheadRussell] p. 121Theorem *4.76jcab 834  pm4.76 837
[WhiteheadRussell] p. 121Theorem *4.77jaob 759  pm4.77 763
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 566
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 567
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 355
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 356
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 895
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 896
[WhiteheadRussell] p. 122Theorem *4.84imbi1 314
[WhiteheadRussell] p. 122Theorem *4.85imbi2 315
[WhiteheadRussell] p. 122Theorem *4.86bibi1 318  wl-bibi1 25937
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 351  impexp 434  pm4.87 568
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 831
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 855
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 856
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 858
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 857
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 860
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 861
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 859
[WhiteheadRussell] p. 124Theorem *5.18nbbn 348  pm5.18 346
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 350
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 832
[WhiteheadRussell] p. 124Theorem *5.22xor 862
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 864
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 865
[WhiteheadRussell] p. 124Theorem *5.25dfor2 401
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 693
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 352
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 327
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 879
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 901
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 572
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 618
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 849
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 870
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 850
[WhiteheadRussell] p. 125Theorem *5.41imdi 353  pm5.41 354
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 532
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 878
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 772
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 871
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 868
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 694
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 890
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 891
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 903
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 331
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 236
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 904
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 27222
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27223
[WhiteheadRussell] p. 147Theorem *10.2219.26 1600
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27224
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27225
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27226
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1622
[WhiteheadRussell] p. 151Theorem *10.301albitr 27227
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27228
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27229
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27230
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27231
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27233
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27234
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27235
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27232
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2148
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27238
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27239
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27240
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1745
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27241
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27242
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27243
[WhiteheadRussell] p. 162Theorem *11.322alim 27244
[WhiteheadRussell] p. 162Theorem *11.332albi 27245
[WhiteheadRussell] p. 162Theorem *11.342exim 27246
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27248
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27247
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1617
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27250
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27251
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27249
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1579
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27252
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27253
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1587
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27254
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1905
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27255
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27260
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27256
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27257
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27258
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27259
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27264
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27261
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27262
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27263
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27265
[WhiteheadRussell] p. 175Definition *14.02df-eu 2242
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27276  pm13.13b 27277
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27278
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2622
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2623
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3019
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27284
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27285
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27279
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27982  pm13.193 27280
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27281
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27282
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27283
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27290
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27289
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27288
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3156
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27291  pm14.122b 27292  pm14.122c 27293
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27294  pm14.123b 27295  pm14.123c 27296
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27298
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27297
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27299
[WhiteheadRussell] p. 190Theorem *14.22iota4 5376
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27300
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5377
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27301
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27303
[WhiteheadRussell] p. 192Theorem *14.26eupick 2301  eupickbi 2304  sbaniota 27304
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27302
[WhiteheadRussell] p. 192Theorem *14.271eubi 27305
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27306
[WhiteheadRussell] p. 235Definition *30.01conventions 21558  df-fv 5402
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7820  pm54.43lem 7819
[Young] p. 141Definition of operator orderingleop2 23475
[Young] p. 142Example 12.2(i)0leop 23481  idleop 23482
[vandenDries] p. 42Lemma 61irrapx1 26582
[vandenDries] p. 43Theorem 62pellex 26589  pellexlem1 26583

This page was last updated on 19-Feb-2018.
Copyright terms: Public domain