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 13909
[Adamek] p. 29Proposition 3.14(1)invinv 13923
[Adamek] p. 29Proposition 3.14(2)invco 13924  isoco 13926
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18614  df-nmoo 22095
[AkhiezerGlazman] p. 64Theoremhmopidmch 23505  hmopidmchi 23503
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 23553  pjcmul2i 23554
[AkhiezerGlazman] p. 72Theoremcnvunop 23270  unoplin 23272
[AkhiezerGlazman] p. 72Equation 2unopadj 23271  unopadj2 23290
[AkhiezerGlazman] p. 73Theoremelunop2 23365  lnopunii 23364
[AkhiezerGlazman] p. 80Proposition 1adjlnop 23438
[Apostol] p. 18Theorem I.1addcan 9183  addcan2d 9203  addcan2i 9193  addcand 9202  addcani 9192
[Apostol] p. 18Theorem I.2negeu 9229
[Apostol] p. 18Theorem I.3negsub 9282  negsubd 9350  negsubi 9311
[Apostol] p. 18Theorem I.4negneg 9284  negnegd 9335  negnegi 9303
[Apostol] p. 18Theorem I.5subdi 9400  subdid 9422  subdii 9415  subdir 9401  subdird 9423  subdiri 9416
[Apostol] p. 18Theorem I.6mul01 9178  mul01d 9198  mul01i 9189  mul02 9177  mul02d 9197  mul02i 9188
[Apostol] p. 18Theorem I.7mulcan 9592  mulcan2d 9589  mulcand 9588  mulcani 9594
[Apostol] p. 18Theorem I.8receu 9600  xreceu 24007
[Apostol] p. 18Theorem I.9divrec 9627  divrecd 9726  divreci 9692  divreczi 9685
[Apostol] p. 18Theorem I.10recrec 9644  recreci 9679
[Apostol] p. 18Theorem I.11mul0or 9595  mul0ord 9605  mul0ori 9603
[Apostol] p. 18Theorem I.12mul2neg 9406  mul2negd 9421  mul2negi 9414  mulneg1 9403  mulneg1d 9419  mulneg1i 9412
[Apostol] p. 18Theorem I.13divadddiv 9662  divadddivd 9767  divadddivi 9709
[Apostol] p. 18Theorem I.14divmuldiv 9647  divmuldivd 9764  divmuldivi 9707  rdivmuldivd 24057
[Apostol] p. 18Theorem I.15divdivdiv 9648  divdivdivd 9770  divdivdivi 9710
[Apostol] p. 20Axiom 7rpaddcl 10565  rpaddcld 10596  rpmulcl 10566  rpmulcld 10597
[Apostol] p. 20Axiom 8rpneg 10574
[Apostol] p. 20Axiom 90nrp 10575
[Apostol] p. 20Theorem I.17lttri 9132
[Apostol] p. 20Theorem I.18ltadd1d 9552  ltadd1dd 9570  ltadd1i 9514
[Apostol] p. 20Theorem I.19ltmul1 9793  ltmul1a 9792  ltmul1i 9862  ltmul1ii 9872  ltmul2 9794  ltmul2d 10619  ltmul2dd 10633  ltmul2i 9865
[Apostol] p. 20Theorem I.20msqgt0 9481  msqgt0d 9527  msqgt0i 9497
[Apostol] p. 20Theorem I.210lt1 9483
[Apostol] p. 20Theorem I.23lt0neg1 9467  lt0neg1d 9529  ltneg 9461  ltnegd 9537  ltnegi 9504
[Apostol] p. 20Theorem I.25lt2add 9446  lt2addd 9581  lt2addi 9522
[Apostol] p. 20Definition of positive numbersdf-rp 10546
[Apostol] p. 21Exercise 4recgt0 9787  recgt0d 9878  recgt0i 9848  recgt0ii 9849
[Apostol] p. 22Definition of integersdf-z 10216
[Apostol] p. 22Definition of positive integersdfnn3 9947
[Apostol] p. 22Definition of rationalsdf-q 10508
[Apostol] p. 24Theorem I.26supeu 7393
[Apostol] p. 26Theorem I.28nnunb 10150
[Apostol] p. 26Theorem I.29arch 10151
[Apostol] p. 28Exercise 2btwnz 10305
[Apostol] p. 28Exercise 3nnrecl 10152
[Apostol] p. 28Exercise 4rebtwnz 10506
[Apostol] p. 28Exercise 5zbtwnre 10505
[Apostol] p. 28Exercise 6qbtwnre 10718
[Apostol] p. 28Exercise 10(a)zneo 10285
[Apostol] p. 29Theorem I.35msqsqrd 12170  resqrth 11989  sqrth 12096  sqrthi 12102  sqsqrd 12169
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9936
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10475
[Apostol] p. 361Remarkcrreczi 11432
[Apostol] p. 363Remarkabsgt0i 12130
[Apostol] p. 363Exampleabssubd 12183  abssubi 12134
[Baer] p. 40Property (b)mapdord 31754
[Baer] p. 40Property (c)mapd11 31755
[Baer] p. 40Property (e)mapdin 31778  mapdlsm 31780
[Baer] p. 40Property (f)mapd0 31781
[Baer] p. 40Definition of projectivitydf-mapd 31741  mapd1o 31764
[Baer] p. 41Property (g)mapdat 31783
[Baer] p. 44Part (1)mapdpg 31822
[Baer] p. 45Part (2)hdmap1eq 31918  mapdheq 31844  mapdheq2 31845  mapdheq2biN 31846
[Baer] p. 45Part (3)baerlem3 31829
[Baer] p. 46Part (4)mapdheq4 31848  mapdheq4lem 31847
[Baer] p. 46Part (5)baerlem5a 31830  baerlem5abmN 31834  baerlem5amN 31832  baerlem5b 31831  baerlem5bmN 31833
[Baer] p. 47Part (6)hdmap1l6 31938  hdmap1l6a 31926  hdmap1l6e 31931  hdmap1l6f 31932  hdmap1l6g 31933  hdmap1l6lem1 31924  hdmap1l6lem2 31925  hdmap1p6N 31939  mapdh6N 31863  mapdh6aN 31851  mapdh6eN 31856  mapdh6fN 31857  mapdh6gN 31858  mapdh6lem1N 31849  mapdh6lem2N 31850
[Baer] p. 48Part 9hdmapval 31947
[Baer] p. 48Part 10hdmap10 31959
[Baer] p. 48Part 11hdmapadd 31962
[Baer] p. 48Part (6)hdmap1l6h 31934  mapdh6hN 31859
[Baer] p. 48Part (7)mapdh75cN 31869  mapdh75d 31870  mapdh75e 31868  mapdh75fN 31871  mapdh7cN 31865  mapdh7dN 31866  mapdh7eN 31864  mapdh7fN 31867
[Baer] p. 48Part (8)mapdh8 31905  mapdh8a 31891  mapdh8aa 31892  mapdh8ab 31893  mapdh8ac 31894  mapdh8ad 31895  mapdh8b 31896  mapdh8c 31897  mapdh8d 31899  mapdh8d0N 31898  mapdh8e 31900  mapdh8fN 31901  mapdh8g 31902  mapdh8i 31903  mapdh8j 31904
[Baer] p. 48Part (9)mapdh9a 31906
[Baer] p. 48Equation 10mapdhvmap 31885
[Baer] p. 49Part 12hdmap11 31967  hdmapeq0 31963  hdmapf1oN 31984  hdmapneg 31965  hdmaprnN 31983  hdmaprnlem1N 31968  hdmaprnlem3N 31969  hdmaprnlem3uN 31970  hdmaprnlem4N 31972  hdmaprnlem6N 31973  hdmaprnlem7N 31974  hdmaprnlem8N 31975  hdmaprnlem9N 31976  hdmapsub 31966
[Baer] p. 49Part 14hdmap14lem1 31987  hdmap14lem10 31996  hdmap14lem1a 31985  hdmap14lem2N 31988  hdmap14lem2a 31986  hdmap14lem3 31989  hdmap14lem8 31994  hdmap14lem9 31995
[Baer] p. 50Part 14hdmap14lem11 31997  hdmap14lem12 31998  hdmap14lem13 31999  hdmap14lem14 32000  hdmap14lem15 32001  hgmapval 32006
[Baer] p. 50Part 15hgmapadd 32013  hgmapmul 32014  hgmaprnlem2N 32016  hgmapvs 32010
[Baer] p. 50Part 16hgmaprnN 32020
[Baer] p. 110Lemma 1hdmapip0com 32036
[Baer] p. 110Line 27hdmapinvlem1 32037
[Baer] p. 110Line 28hdmapinvlem2 32038
[Baer] p. 110Line 30hdmapinvlem3 32039
[Baer] p. 110Part 1.2hdmapglem5 32041  hgmapvv 32045
[Baer] p. 110Proposition 1hdmapinvlem4 32040
[Baer] p. 111Line 10hgmapvvlem1 32042
[Baer] p. 111Line 15hdmapg 32049  hdmapglem7 32048
[BellMachover] p. 36Lemma 10.3id1 21
[BellMachover] p. 97Definition 10.1df-eu 2243
[BellMachover] p. 460Notationdf-mo 2244
[BellMachover] p. 460Definitionmo3 2270
[BellMachover] p. 461Axiom Extax-ext 2369
[BellMachover] p. 462Theorem 1.1bm1.1 2373
[BellMachover] p. 463Axiom Repaxrep5 4267
[BellMachover] p. 463Scheme Sepaxsep 4271
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4275
[BellMachover] p. 466Axiom Powaxpow3 4322
[BellMachover] p. 466Axiom Unionaxun2 4644
[BellMachover] p. 468Definitiondf-ord 4526
[BellMachover] p. 469Theorem 2.2(i)ordirr 4541
[BellMachover] p. 469Theorem 2.2(iii)onelon 4548
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4543
[BellMachover] p. 471Definition of Ndf-om 4787
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4727
[BellMachover] p. 471Definition of Limdf-lim 4528
[BellMachover] p. 472Axiom Infzfinf2 7531
[BellMachover] p. 473Theorem 2.8limom 4801
[BellMachover] p. 477Equation 3.1df-r1 7624
[BellMachover] p. 478Definitionrankval2 7678
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7642  r1ord3g 7639
[BellMachover] p. 480Axiom Regzfreg2 7498
[BellMachover] p. 488Axiom ACac5 8291  dfac4 7937
[BellMachover] p. 490Definition of alephalephval3 7925
[BeltramettiCassinelli] p. 98Remarkatlatmstc 29435
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 23705
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 23747  chirredi 23746
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 23735
[Beran] p. 3Definition of joinsshjval3 22705
[Beran] p. 39Theorem 2.3(i)cmcm2 22967  cmcm2i 22944  cmcm2ii 22949  cmt2N 29366
[Beran] p. 40Theorem 2.3(iii)lecm 22968  lecmi 22953  lecmii 22954
[Beran] p. 45Theorem 3.4cmcmlem 22942
[Beran] p. 49Theorem 4.2cm2j 22971  cm2ji 22976  cm2mi 22977
[Beran] p. 95Definitiondf-sh 22558  issh2 22560
[Beran] p. 95Lemma 3.1(S5)his5 22437
[Beran] p. 95Lemma 3.1(S6)his6 22450
[Beran] p. 95Lemma 3.1(S7)his7 22441
[Beran] p. 95Lemma 3.2(S8)ho01i 23180
[Beran] p. 95Lemma 3.2(S9)hoeq1 23182
[Beran] p. 95Lemma 3.2(S10)ho02i 23181
[Beran] p. 95Lemma 3.2(S11)hoeq2 23183
[Beran] p. 95Postulate (S1)ax-his1 22433  his1i 22451
[Beran] p. 95Postulate (S2)ax-his2 22434
[Beran] p. 95Postulate (S3)ax-his3 22435
[Beran] p. 95Postulate (S4)ax-his4 22436
[Beran] p. 96Definition of normdf-hnorm 22320  dfhnorm2 22473  normval 22475
[Beran] p. 96Definition for Cauchy sequencehcau 22535
[Beran] p. 96Definition of Cauchy sequencedf-hcau 22325
[Beran] p. 96Definition of complete subspaceisch3 22593
[Beran] p. 96Definition of convergedf-hlim 22324  hlimi 22539
[Beran] p. 97Theorem 3.3(i)norm-i-i 22484  norm-i 22480
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 22488  norm-ii 22489  normlem0 22460  normlem1 22461  normlem2 22462  normlem3 22463  normlem4 22464  normlem5 22465  normlem6 22466  normlem7 22467  normlem7tALT 22470
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 22490  norm-iii 22491
[Beran] p. 98Remark 3.4bcs 22532  bcsiALT 22530  bcsiHIL 22531
[Beran] p. 98Remark 3.4(B)normlem9at 22472  normpar 22506  normpari 22505
[Beran] p. 98Remark 3.4(C)normpyc 22497  normpyth 22496  normpythi 22493
[Beran] p. 99Remarklnfn0 23399  lnfn0i 23394  lnop0 23318  lnop0i 23322
[Beran] p. 99Theorem 3.5(i)nmcexi 23378  nmcfnex 23405  nmcfnexi 23403  nmcopex 23381  nmcopexi 23379
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 23406  nmcfnlbi 23404  nmcoplb 23382  nmcoplbi 23380
[Beran] p. 99Theorem 3.5(iii)lnfncon 23408  lnfnconi 23407  lnopcon 23387  lnopconi 23386
[Beran] p. 100Lemma 3.6normpar2i 22507
[Beran] p. 101Lemma 3.6norm3adifi 22504  norm3adifii 22499  norm3dif 22501  norm3difi 22498
[Beran] p. 102Theorem 3.7(i)chocunii 22652  pjhth 22744  pjhtheu 22745  pjpjhth 22776  pjpjhthi 22777  pjth 19208
[Beran] p. 102Theorem 3.7(ii)ococ 22757  ococi 22756
[Beran] p. 103Remark 3.8nlelchi 23413
[Beran] p. 104Theorem 3.9riesz3i 23414  riesz4 23416  riesz4i 23415
[Beran] p. 104Theorem 3.10cnlnadj 23431  cnlnadjeu 23430  cnlnadjeui 23429  cnlnadji 23428  cnlnadjlem1 23419  nmopadjlei 23440
[Beran] p. 106Theorem 3.11(i)adjeq0 23443
[Beran] p. 106Theorem 3.11(v)nmopadji 23442
[Beran] p. 106Theorem 3.11(ii)adjmul 23444
[Beran] p. 106Theorem 3.11(iv)adjadj 23288
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 23454  nmopcoadji 23453
[Beran] p. 106Theorem 3.11(iii)adjadd 23445
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 23455
[Beran] p. 106Theorem 3.11(viii)adjcoi 23452  pjadj2coi 23556  pjadjcoi 23513
[Beran] p. 107Definitiondf-ch 22573  isch2 22575
[Beran] p. 107Remark 3.12choccl 22657  isch3 22593  occl 22655  ocsh 22634  shoccl 22656  shocsh 22635
[Beran] p. 107Remark 3.12(B)ococin 22759
[Beran] p. 108Theorem 3.13chintcl 22683
[Beran] p. 109Property (i)pjadj2 23539  pjadj3 23540  pjadji 23036  pjadjii 23025
[Beran] p. 109Property (ii)pjidmco 23533  pjidmcoi 23529  pjidmi 23024
[Beran] p. 110Definition of projector orderingpjordi 23525
[Beran] p. 111Remarkho0val 23102  pjch1 23021
[Beran] p. 111Definitiondf-hfmul 23086  df-hfsum 23085  df-hodif 23084  df-homul 23083  df-hosum 23082
[Beran] p. 111Lemma 4.4(i)pjo 23022
[Beran] p. 111Lemma 4.4(ii)pjch 23045  pjchi 22783
[Beran] p. 111Lemma 4.4(iii)pjoc2 22790  pjoc2i 22789
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 23031
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 23517  pjssmii 23032
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 23516
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 23515
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 23520
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 23518  pjssge0ii 23033
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 23519  pjdifnormii 23034
[Bogachev] p. 116Definition 2.3.1df-fndm 24443
[Bogachev] p. 118Definition 2.4.1df-sitg 24441
[Bogachev] p. 118Definition 2.4.4df-itgm 24444
[Bollobas] p. 4Definitiondf-wlk 21382
[Bollobas] p. 5Notationdf-pth 21384
[Bollobas] p. 5Definitiondf-crct 21386  df-cycl 21387  df-trail 21383  df-wlkon 21388
[BourbakiEns] p. Proposition 8fcof1 5960  fcofo 5961
[BourbakiTop1] p. Remarkxnegmnf 10729  xnegpnf 10728
[BourbakiTop1] p. Remark rexneg 10730
[BourbakiTop1] p. Theoremneiss 17097
[BourbakiTop1] p. Remark 3ust0 18171  ustfilxp 18164
[BourbakiTop1] p. Axiom GT'tgpsubcn 18042
[BourbakiTop1] p. Example 1cstucnd 18236  iducn 18235  snfil 17818
[BourbakiTop1] p. Example 2neifil 17834
[BourbakiTop1] p. Theorem 1cnextcn 18020
[BourbakiTop1] p. Theorem 2ucnextcn 18256
[BourbakiTop1] p. Definitionistgp 18029
[BourbakiTop1] p. Propositioncnpco 17254  ishmeo 17713  neips 17101
[BourbakiTop1] p. Definition 1df-ucn 18228  df-ust 18152  filintn0 17815  ucnprima 18234
[BourbakiTop1] p. Definition 2df-cfilu 18239
[BourbakiTop1] p. Definition 3df-cusp 18250  df-usp 18209  df-utop 18183  trust 18181
[BourbakiTop1] p. Condition F_Iustssel 18157
[BourbakiTop1] p. Condition U_Iustdiag 18160
[BourbakiTop1] p. Property V_ivneiptopreu 17121
[BourbakiTop1] p. Proposition 1ucncn 18237  ustund 18173  ustuqtop 18198
[BourbakiTop1] p. Proposition 2neiptopreu 17121  utop2nei 18202  utop3cls 18203
[BourbakiTop1] p. Proposition 3fmucnd 18244  uspreg 18226  utopreg 18204
[BourbakiTop1] p. Proposition 4imasncld 17645  imasncls 17646  imasnopn 17644
[BourbakiTop1] p. Proposition 9cnpflf2 17954
[BourbakiTop1] p. Theorem 1 (d)iscncl 17256
[BourbakiTop1] p. Condition F_IIustincl 18159
[BourbakiTop1] p. Condition U_IIustinvel 18161
[BourbakiTop1] p. Proposition 11cnextucn 18255
[BourbakiTop1] p. Proposition Vissnei2 17104
[BourbakiTop1] p. Condition F_IIbustbasel 18158
[BourbakiTop1] p. Condition U_IIIustexhalf 18162
[BourbakiTop1] p. Definition C'''df-cmp 17373
[BourbakiTop1] p. Proposition Viiinnei 17113
[BourbakiTop1] p. Proposition Vivneissex 17115
[BourbakiTop1] p. Proposition Viiielnei 17099  ssnei 17098
[BourbakiTop1] p. Remark below def. 1filn0 17816
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17800
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17817
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27482  stoweid 27481
[BrosowskiDeutsh] p. 89Theorem for the non-trivial casestoweidlem62 27480
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27419  stoweidlem10 27428  stoweidlem14 27432  stoweidlem15 27433  stoweidlem35 27453  stoweidlem36 27454  stoweidlem37 27455  stoweidlem38 27456  stoweidlem40 27458  stoweidlem41 27459  stoweidlem43 27461  stoweidlem44 27462  stoweidlem46 27464  stoweidlem5 27423  stoweidlem50 27468  stoweidlem52 27470  stoweidlem53 27471  stoweidlem55 27473  stoweidlem56 27474
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27441  stoweidlem24 27442  stoweidlem27 27445  stoweidlem28 27446  stoweidlem30 27448
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27463  stoweidlem49 27467  stoweidlem7 27425
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27449  stoweidlem39 27457  stoweidlem42 27460  stoweidlem48 27466  stoweidlem51 27469  stoweidlem54 27472  stoweidlem57 27475  stoweidlem58 27476
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27443
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27452
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27435
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27477
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27478
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27436
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27429  stoweidlem26 27444
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27431
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27479
[ChoquetDD] p. 2Definition of mappingdf-mpt 4210
[Clemente] p. 10Definition ITnatded 21560
[Clemente] p. 10Definition I` `m,nnatded 21560
[Clemente] p. 11Definition E=>m,nnatded 21560
[Clemente] p. 11Definition I=>m,nnatded 21560
[Clemente] p. 11Definition E` `(1)natded 21560
[Clemente] p. 11Definition E` `(2)natded 21560
[Clemente] p. 12Definition E` `m,n,pnatded 21560
[Clemente] p. 12Definition I` `n(1)natded 21560
[Clemente] p. 12Definition I` `n(2)natded 21560
[Clemente] p. 13Definition I` `m,n,pnatded 21560
[Clemente] p. 14Definition E` `nnatded 21560
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 21562  ex-natded5.2 21561
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 21565  ex-natded5.3 21564
[Clemente] p. 18Theorem 5.5ex-natded5.5 21567
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 21569  ex-natded5.7 21568
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 21571  ex-natded5.8 21570
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 21573  ex-natded5.13 21572
[Clemente] p. 32Definition I` `nnatded 21560
[Clemente] p. 32Definition E` `m,n,p,anatded 21560
[Clemente] p. 32Definition E` `n,tnatded 21560
[Clemente] p. 32Definition I` `n,tnatded 21560
[Clemente] p. 43Theorem 9.20ex-natded9.20 21574
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 21575
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 21577  ex-natded9.26 21576
[Cohen] p. 301Remarkrelogoprlem 20353
[Cohen] p. 301Property 2relogmul 20354  relogmuld 20388
[Cohen] p. 301Property 3relogdiv 20355  relogdivd 20389
[Cohen] p. 301Property 4relogexp 20358
[Cohen] p. 301Property 1alog1 20348
[Cohen] p. 301Property 1bloge 20349
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 24430  sxbrsigalem4 24432
[Cohn] p. 81Section II.5acsdomd 14535  acsinfd 14534  acsinfdimd 14536  acsmap2d 14533  acsmapd 14532
[Cohn] p. 143Example 5.1.1sxbrsiga 24435
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 11170
[Crawley] p. 1Definition of posetdf-poset 14331
[Crawley] p. 107Theorem 13.2hlsupr 29501
[Crawley] p. 110Theorem 13.3arglem1N 30305  dalaw 30001
[Crawley] p. 111Theorem 13.4hlathil 32080
[Crawley] p. 111Definition of set Wdf-watsN 30105
[Crawley] p. 111Definition of dilationdf-dilN 30221  df-ldil 30219  isldil 30225
[Crawley] p. 111Definition of translationdf-ltrn 30220  df-trnN 30222  isltrn 30234  ltrnu 30236
[Crawley] p. 112Lemma Acdlema1N 29906  cdlema2N 29907  exatleN 29519
[Crawley] p. 112Lemma B1cvrat 29591  cdlemb 29909  cdlemb2 30156  cdlemb3 30721  idltrn 30265  l1cvat 29171  lhpat 30158  lhpat2 30160  lshpat 29172  ltrnel 30254  ltrnmw 30266
[Crawley] p. 112Lemma Ccdlemc1 30306  cdlemc2 30307  ltrnnidn 30289  trlat 30284  trljat1 30281  trljat2 30282  trljat3 30283  trlne 30300  trlnidat 30288  trlnle 30301
[Crawley] p. 112Definition of automorphismdf-pautN 30106
[Crawley] p. 113Lemma Ccdlemc 30312  cdlemc3 30308  cdlemc4 30309
[Crawley] p. 113Lemma Dcdlemd 30322  cdlemd1 30313  cdlemd2 30314  cdlemd3 30315  cdlemd4 30316  cdlemd5 30317  cdlemd6 30318  cdlemd7 30319  cdlemd8 30320  cdlemd9 30321  cdleme31sde 30500  cdleme31se 30497  cdleme31se2 30498  cdleme31snd 30501  cdleme32a 30556  cdleme32b 30557  cdleme32c 30558  cdleme32d 30559  cdleme32e 30560  cdleme32f 30561  cdleme32fva 30552  cdleme32fva1 30553  cdleme32fvcl 30555  cdleme32le 30562  cdleme48fv 30614  cdleme4gfv 30622  cdleme50eq 30656  cdleme50f 30657  cdleme50f1 30658  cdleme50f1o 30661  cdleme50laut 30662  cdleme50ldil 30663  cdleme50lebi 30655  cdleme50rn 30660  cdleme50rnlem 30659  cdlemeg49le 30626  cdlemeg49lebilem 30654
[Crawley] p. 113Lemma Ecdleme 30675  cdleme00a 30324  cdleme01N 30336  cdleme02N 30337  cdleme0a 30326  cdleme0aa 30325  cdleme0b 30327  cdleme0c 30328  cdleme0cp 30329  cdleme0cq 30330  cdleme0dN 30331  cdleme0e 30332  cdleme0ex1N 30338  cdleme0ex2N 30339  cdleme0fN 30333  cdleme0gN 30334  cdleme0moN 30340  cdleme1 30342  cdleme10 30369  cdleme10tN 30373  cdleme11 30385  cdleme11a 30375  cdleme11c 30376  cdleme11dN 30377  cdleme11e 30378  cdleme11fN 30379  cdleme11g 30380  cdleme11h 30381  cdleme11j 30382  cdleme11k 30383  cdleme11l 30384  cdleme12 30386  cdleme13 30387  cdleme14 30388  cdleme15 30393  cdleme15a 30389  cdleme15b 30390  cdleme15c 30391  cdleme15d 30392  cdleme16 30400  cdleme16aN 30374  cdleme16b 30394  cdleme16c 30395  cdleme16d 30396  cdleme16e 30397  cdleme16f 30398  cdleme16g 30399  cdleme19a 30418  cdleme19b 30419  cdleme19c 30420  cdleme19d 30421  cdleme19e 30422  cdleme19f 30423  cdleme1b 30341  cdleme2 30343  cdleme20aN 30424  cdleme20bN 30425  cdleme20c 30426  cdleme20d 30427  cdleme20e 30428  cdleme20f 30429  cdleme20g 30430  cdleme20h 30431  cdleme20i 30432  cdleme20j 30433  cdleme20k 30434  cdleme20l 30437  cdleme20l1 30435  cdleme20l2 30436  cdleme20m 30438  cdleme20y 30417  cdleme20zN 30416  cdleme21 30452  cdleme21d 30445  cdleme21e 30446  cdleme22a 30455  cdleme22aa 30454  cdleme22b 30456  cdleme22cN 30457  cdleme22d 30458  cdleme22e 30459  cdleme22eALTN 30460  cdleme22f 30461  cdleme22f2 30462  cdleme22g 30463  cdleme23a 30464  cdleme23b 30465  cdleme23c 30466  cdleme26e 30474  cdleme26eALTN 30476  cdleme26ee 30475  cdleme26f 30478  cdleme26f2 30480  cdleme26f2ALTN 30479  cdleme26fALTN 30477  cdleme27N 30484  cdleme27a 30482  cdleme27cl 30481  cdleme28c 30487  cdleme3 30352  cdleme30a 30493  cdleme31fv 30505  cdleme31fv1 30506  cdleme31fv1s 30507  cdleme31fv2 30508  cdleme31id 30509  cdleme31sc 30499  cdleme31sdnN 30502  cdleme31sn 30495  cdleme31sn1 30496  cdleme31sn1c 30503  cdleme31sn2 30504  cdleme31so 30494  cdleme35a 30563  cdleme35b 30565  cdleme35c 30566  cdleme35d 30567  cdleme35e 30568  cdleme35f 30569  cdleme35fnpq 30564  cdleme35g 30570  cdleme35h 30571  cdleme35h2 30572  cdleme35sn2aw 30573  cdleme35sn3a 30574  cdleme36a 30575  cdleme36m 30576  cdleme37m 30577  cdleme38m 30578  cdleme38n 30579  cdleme39a 30580  cdleme39n 30581  cdleme3b 30344  cdleme3c 30345  cdleme3d 30346  cdleme3e 30347  cdleme3fN 30348  cdleme3fa 30351  cdleme3g 30349  cdleme3h 30350  cdleme4 30353  cdleme40m 30582  cdleme40n 30583  cdleme40v 30584  cdleme40w 30585  cdleme41fva11 30592  cdleme41sn3aw 30589  cdleme41sn4aw 30590  cdleme41snaw 30591  cdleme42a 30586  cdleme42b 30593  cdleme42c 30587  cdleme42d 30588  cdleme42e 30594  cdleme42f 30595  cdleme42g 30596  cdleme42h 30597  cdleme42i 30598  cdleme42k 30599  cdleme42ke 30600  cdleme42keg 30601  cdleme42mN 30602  cdleme42mgN 30603  cdleme43aN 30604  cdleme43bN 30605  cdleme43cN 30606  cdleme43dN 30607  cdleme5 30355  cdleme50ex 30674  cdleme50ltrn 30672  cdleme51finvN 30671  cdleme51finvfvN 30670  cdleme51finvtrN 30673  cdleme6 30356  cdleme7 30364  cdleme7a 30358  cdleme7aa 30357  cdleme7b 30359  cdleme7c 30360  cdleme7d 30361  cdleme7e 30362  cdleme7ga 30363  cdleme8 30365  cdleme8tN 30370  cdleme9 30368  cdleme9a 30366  cdleme9b 30367  cdleme9tN 30372  cdleme9taN 30371  cdlemeda 30413  cdlemedb 30412  cdlemednpq 30414  cdlemednuN 30415  cdlemefr27cl 30518  cdlemefr32fva1 30525  cdlemefr32fvaN 30524  cdlemefrs32fva 30515  cdlemefrs32fva1 30516  cdlemefs27cl 30528  cdlemefs32fva1 30538  cdlemefs32fvaN 30537  cdlemesner 30411  cdlemeulpq 30335
[Crawley] p. 114Lemma E4atex 30191  4atexlem7 30190  cdleme0nex 30405  cdleme17a 30401  cdleme17c 30403  cdleme17d 30613  cdleme17d1 30404  cdleme17d2 30610  cdleme18a 30406  cdleme18b 30407  cdleme18c 30408  cdleme18d 30410  cdleme4a 30354
[Crawley] p. 115Lemma Ecdleme21a 30440  cdleme21at 30443  cdleme21b 30441  cdleme21c 30442  cdleme21ct 30444  cdleme21f 30447  cdleme21g 30448  cdleme21h 30449  cdleme21i 30450  cdleme22gb 30409
[Crawley] p. 116Lemma Fcdlemf 30678  cdlemf1 30676  cdlemf2 30677
[Crawley] p. 116Lemma Gcdlemftr1 30682  cdlemg16 30772  cdlemg28 30819  cdlemg28a 30808  cdlemg28b 30818  cdlemg3a 30712  cdlemg42 30844  cdlemg43 30845  cdlemg44 30848  cdlemg44a 30846  cdlemg46 30850  cdlemg47 30851  cdlemg9 30749  ltrnco 30834  ltrncom 30853  tgrpabl 30866  trlco 30842
[Crawley] p. 116Definition of Gdf-tgrp 30858
[Crawley] p. 117Lemma Gcdlemg17 30792  cdlemg17b 30777
[Crawley] p. 117Definition of Edf-edring-rN 30871  df-edring 30872
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30875
[Crawley] p. 118Remarktendopltp 30895
[Crawley] p. 118Lemma Hcdlemh 30932  cdlemh1 30930  cdlemh2 30931
[Crawley] p. 118Lemma Icdlemi 30935  cdlemi1 30933  cdlemi2 30934
[Crawley] p. 118Lemma Jcdlemj1 30936  cdlemj2 30937  cdlemj3 30938  tendocan 30939
[Crawley] p. 118Lemma Kcdlemk 31089  cdlemk1 30946  cdlemk10 30958  cdlemk11 30964  cdlemk11t 31061  cdlemk11ta 31044  cdlemk11tb 31046  cdlemk11tc 31060  cdlemk11u-2N 31004  cdlemk11u 30986  cdlemk12 30965  cdlemk12u-2N 31005  cdlemk12u 30987  cdlemk13-2N 30991  cdlemk13 30967  cdlemk14-2N 30993  cdlemk14 30969  cdlemk15-2N 30994  cdlemk15 30970  cdlemk16-2N 30995  cdlemk16 30972  cdlemk16a 30971  cdlemk17-2N 30996  cdlemk17 30973  cdlemk18-2N 31001  cdlemk18-3N 31015  cdlemk18 30983  cdlemk19-2N 31002  cdlemk19 30984  cdlemk19u 31085  cdlemk1u 30974  cdlemk2 30947  cdlemk20-2N 31007  cdlemk20 30989  cdlemk21-2N 31006  cdlemk21N 30988  cdlemk22-3 31016  cdlemk22 31008  cdlemk23-3 31017  cdlemk24-3 31018  cdlemk25-3 31019  cdlemk26-3 31021  cdlemk26b-3 31020  cdlemk27-3 31022  cdlemk28-3 31023  cdlemk29-3 31026  cdlemk3 30948  cdlemk30 31009  cdlemk31 31011  cdlemk32 31012  cdlemk33N 31024  cdlemk34 31025  cdlemk35 31027  cdlemk36 31028  cdlemk37 31029  cdlemk38 31030  cdlemk39 31031  cdlemk39u 31083  cdlemk4 30949  cdlemk41 31035  cdlemk42 31056  cdlemk42yN 31059  cdlemk43N 31078  cdlemk45 31062  cdlemk46 31063  cdlemk47 31064  cdlemk48 31065  cdlemk49 31066  cdlemk5 30951  cdlemk50 31067  cdlemk51 31068  cdlemk52 31069  cdlemk53 31072  cdlemk54 31073  cdlemk55 31076  cdlemk55u 31081  cdlemk56 31086  cdlemk5a 30950  cdlemk5auN 30975  cdlemk5u 30976  cdlemk6 30952  cdlemk6u 30977  cdlemk7 30963  cdlemk7u-2N 31003  cdlemk7u 30985  cdlemk8 30953  cdlemk9 30954  cdlemk9bN 30955  cdlemki 30956  cdlemkid 31051  cdlemkj-2N 30997  cdlemkj 30978  cdlemksat 30961  cdlemksel 30960  cdlemksv 30959  cdlemksv2 30962  cdlemkuat 30981  cdlemkuel-2N 30999  cdlemkuel-3 31013  cdlemkuel 30980  cdlemkuv-2N 30998  cdlemkuv2-2 31000  cdlemkuv2-3N 31014  cdlemkuv2 30982  cdlemkuvN 30979  cdlemkvcl 30957  cdlemky 31041  cdlemkyyN 31077  tendoex 31090
[Crawley] p. 120Remarkdva1dim 31100
[Crawley] p. 120Lemma Lcdleml1N 31091  cdleml2N 31092  cdleml3N 31093  cdleml4N 31094  cdleml5N 31095  cdleml6 31096  cdleml7 31097  cdleml8 31098  cdleml9 31099  dia1dim 31177
[Crawley] p. 120Lemma Mdia11N 31164  diaf11N 31165  dialss 31162  diaord 31163  dibf11N 31277  djajN 31253
[Crawley] p. 120Definition of isomorphism mapdiaval 31148
[Crawley] p. 121Lemma Mcdlemm10N 31234  dia2dimlem1 31180  dia2dimlem2 31181  dia2dimlem3 31182  dia2dimlem4 31183  dia2dimlem5 31184  diaf1oN 31246  diarnN 31245  dvheveccl 31228  dvhopN 31232
[Crawley] p. 121Lemma Ncdlemn 31328  cdlemn10 31322  cdlemn11 31327  cdlemn11a 31323  cdlemn11b 31324  cdlemn11c 31325  cdlemn11pre 31326  cdlemn2 31311  cdlemn2a 31312  cdlemn3 31313  cdlemn4 31314  cdlemn4a 31315  cdlemn5 31317  cdlemn5pre 31316  cdlemn6 31318  cdlemn7 31319  cdlemn8 31320  cdlemn9 31321  diclspsn 31310
[Crawley] p. 121Definition of phi(q)df-dic 31289
[Crawley] p. 122Lemma Ndih11 31381  dihf11 31383  dihjust 31333  dihjustlem 31332  dihord 31380  dihord1 31334  dihord10 31339  dihord11b 31338  dihord11c 31340  dihord2 31343  dihord2a 31335  dihord2b 31336  dihord2cN 31337  dihord2pre 31341  dihord2pre2 31342  dihordlem6 31329  dihordlem7 31330  dihordlem7b 31331
[Crawley] p. 122Definition of isomorphism mapdihffval 31346  dihfval 31347  dihval 31348
[Eisenberg] p. 67Definition 5.3df-dif 3267
[Eisenberg] p. 82Definition 6.3dfom3 7536
[Eisenberg] p. 125Definition 8.21df-map 6957
[Eisenberg] p. 216Example 13.2(4)omenps 7543
[Eisenberg] p. 310Theorem 19.8cardprc 7801
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8364
[Enderton] p. 18Axiom of Empty Setaxnul 4279
[Enderton] p. 19Definitiondf-tp 3766
[Enderton] p. 26Exercise 5unissb 3988
[Enderton] p. 26Exercise 10pwel 4357
[Enderton] p. 28Exercise 7(b)pwun 4433
[Enderton] p. 30Theorem "Distributive laws"iinin1 4104  iinin2 4103  iinun2 4099  iunin1 4098  iunin2 4097
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4102  iundif2 4100
[Enderton] p. 32Exercise 20unineq 3535
[Enderton] p. 33Exercise 23iinuni 4116
[Enderton] p. 33Exercise 25iununi 4117
[Enderton] p. 33Exercise 24(a)iinpw 4121
[Enderton] p. 33Exercise 24(b)iunpw 4700  iunpwss 4122
[Enderton] p. 36Definitionopthwiener 4400
[Enderton] p. 38Exercise 6(a)unipw 4356
[Enderton] p. 38Exercise 6(b)pwuni 4337
[Enderton] p. 41Lemma 3Dopeluu 4656  rnex 5074  rnexg 5072
[Enderton] p. 41Exercise 8dmuni 5020  rnuni 5224
[Enderton] p. 42Definition of a functiondffun7 5420  dffun8 5421
[Enderton] p. 43Definition of function valuefunfv2 5731
[Enderton] p. 43Definition of single-rootedfuncnv 5452
[Enderton] p. 44Definition (d)dfima2 5146  dfima3 5147
[Enderton] p. 47Theorem 3Hfvco2 5738
[Enderton] p. 49Axiom of Choice (first form)ac7 8287  ac7g 8288  df-ac 7931  dfac2 7945  dfac2a 7944  dfac3 7936  dfac7 7946
[Enderton] p. 50Theorem 3K(a)imauni 5933
[Enderton] p. 52Definitiondf-map 6957
[Enderton] p. 53Exercise 21coass 5329
[Enderton] p. 53Exercise 27dmco 5319
[Enderton] p. 53Exercise 14(a)funin 5461
[Enderton] p. 53Exercise 22(a)imass2 5181
[Enderton] p. 54Remarkixpf 7021  ixpssmap 7033
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7001
[Enderton] p. 55Axiom of Choice (second form)ac9 8297  ac9s 8307
[Enderton] p. 56Theorem 3Merref 6862
[Enderton] p. 57Lemma 3Nerthi 6888
[Enderton] p. 57Definitiondf-ec 6844
[Enderton] p. 58Definitiondf-qs 6848
[Enderton] p. 60Theorem 3Qth3q 6950  th3qcor 6949  th3qlem1 6947  th3qlem2 6948
[Enderton] p. 61Exercise 35df-ec 6844
[Enderton] p. 65Exercise 56(a)dmun 5017
[Enderton] p. 68Definition of successordf-suc 4529
[Enderton] p. 71Definitiondf-tr 4245  dftr4 4249
[Enderton] p. 72Theorem 4Eunisuc 4599
[Enderton] p. 73Exercise 6unisuc 4599
[Enderton] p. 73Exercise 5(a)truni 4258
[Enderton] p. 73Exercise 5(b)trint 4259  trintALT 28335
[Enderton] p. 79Theorem 4I(A1)nna0 6784
[Enderton] p. 79Theorem 4I(A2)nnasuc 6786  onasuc 6709
[Enderton] p. 79Definition of operation valuedf-ov 6024
[Enderton] p. 80Theorem 4J(A1)nnm0 6785
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6787  onmsuc 6710
[Enderton] p. 81Theorem 4K(1)nnaass 6802
[Enderton] p. 81Theorem 4K(2)nna0r 6789  nnacom 6797
[Enderton] p. 81Theorem 4K(3)nndi 6803
[Enderton] p. 81Theorem 4K(4)nnmass 6804
[Enderton] p. 81Theorem 4K(5)nnmcom 6806
[Enderton] p. 82Exercise 16nnm0r 6790  nnmsucr 6805
[Enderton] p. 88Exercise 23nnaordex 6818
[Enderton] p. 129Definitiondf-en 7047
[Enderton] p. 132Theorem 6B(b)canth 6476
[Enderton] p. 133Exercise 1xpomen 7831
[Enderton] p. 133Exercise 2qnnen 12741
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7228
[Enderton] p. 135Corollary 6Cphp3 7230
[Enderton] p. 136Corollary 6Enneneq 7227
[Enderton] p. 136Corollary 6D(a)pssinf 7256
[Enderton] p. 136Corollary 6D(b)ominf 7258
[Enderton] p. 137Lemma 6Fpssnn 7264
[Enderton] p. 138Corollary 6Gssfi 7266
[Enderton] p. 139Theorem 6H(c)mapen 7208
[Enderton] p. 142Theorem 6I(3)xpcdaen 7997
[Enderton] p. 142Theorem 6I(4)mapcdaen 7998
[Enderton] p. 143Theorem 6Jcda0en 7993  cda1en 7989
[Enderton] p. 144Exercise 13iunfi 7331  unifi 7332  unifi2 7333
[Enderton] p. 144Corollary 6Kundif2 3648  unfi 7311  unfi2 7313
[Enderton] p. 145Figure 38ffoss 5648
[Enderton] p. 145Definitiondf-dom 7048
[Enderton] p. 146Example 1domen 7058  domeng 7059
[Enderton] p. 146Example 3nndomo 7237  nnsdom 7542  nnsdomg 7303
[Enderton] p. 149Theorem 6L(a)cdadom2 8001
[Enderton] p. 149Theorem 6L(c)mapdom1 7209  xpdom1 7144  xpdom1g 7142  xpdom2g 7141
[Enderton] p. 149Theorem 6L(d)mapdom2 7215
[Enderton] p. 151Theorem 6Mzorn 8321  zorng 8318
[Enderton] p. 151Theorem 6M(4)ac8 8306  dfac5 7943
[Enderton] p. 159Theorem 6Qunictb 8384
[Enderton] p. 164Exampleinfdif 8023
[Enderton] p. 168Definitiondf-po 4445
[Enderton] p. 192Theorem 7M(a)oneli 4630
[Enderton] p. 192Theorem 7M(b)ontr1 4569
[Enderton] p. 192Theorem 7M(c)onirri 4629
[Enderton] p. 193Corollary 7N(b)0elon 4576
[Enderton] p. 193Corollary 7N(c)onsuci 4759
[Enderton] p. 193Corollary 7N(d)ssonunii 4709
[Enderton] p. 194Remarkonprc 4706
[Enderton] p. 194Exercise 16suc11 4626
[Enderton] p. 197Definitiondf-card 7760
[Enderton] p. 197Theorem 7Pcarden 8360
[Enderton] p. 200Exercise 25tfis 4775
[Enderton] p. 202Lemma 7Tr1tr 7636
[Enderton] p. 202Definitiondf-r1 7624
[Enderton] p. 202Theorem 7Qr1val1 7646
[Enderton] p. 204Theorem 7V(b)rankval4 7727
[Enderton] p. 206Theorem 7X(b)en2lp 7505
[Enderton] p. 207Exercise 30rankpr 7717  rankprb 7711  rankpw 7703  rankpwi 7683  rankuniss 7726
[Enderton] p. 207Exercise 34opthreg 7507
[Enderton] p. 208Exercise 35suc11reg 7508
[Enderton] p. 212Definition of alephalephval3 7925
[Enderton] p. 213Theorem 8A(a)alephord2 7891
[Enderton] p. 213Theorem 8A(b)cardalephex 7905
[Enderton] p. 218Theorem Schema 8Eonfununi 6540
[Enderton] p. 222Definition of kardkarden 7753  kardex 7752
[Enderton] p. 238Theorem 8Roeoa 6777
[Enderton] p. 238Theorem 8Soeoe 6779
[Enderton] p. 240Exercise 25oarec 6742
[Enderton] p. 257Definition of cofinalitycflm 8064
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13795
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13741
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14531  mrieqv2d 13792  mrieqvd 13791
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13796
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13801  mreexexlem2d 13798
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14537  mreexfidimd 13803
[Fremlin5] p. 193Proposition 563Gbnulmbl2 19299
[Fremlin5] p. 213Lemma 565Cauniioovol 19339
[Fremlin5] p. 214Lemma 565Cauniioombl 19349
[FreydScedrov] p. 283Axiom of Infinityax-inf 7527  inf1 7511  inf2 7512
[Gleason] p. 117Proposition 9-2.1df-enq 8722  enqer 8732
[Gleason] p. 117Proposition 9-2.2df-1nq 8727  df-nq 8723
[Gleason] p. 117Proposition 9-2.3df-plpq 8719  df-plq 8725
[Gleason] p. 119Proposition 9-2.4caovmo 6224  df-mpq 8720  df-mq 8726
[Gleason] p. 119Proposition 9-2.5df-rq 8728
[Gleason] p. 119Proposition 9-2.6ltexnq 8786
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8787  ltbtwnnq 8789
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8782
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8783
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8790
[Gleason] p. 121Definition 9-3.1df-np 8792
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8804
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8806
[Gleason] p. 122Definitiondf-1p 8793
[Gleason] p. 122Remark (1)prub 8805
[Gleason] p. 122Lemma 9-3.4prlem934 8844
[Gleason] p. 122Proposition 9-3.2df-ltp 8796
[Gleason] p. 122Proposition 9-3.3ltsopr 8843  psslinpr 8842  supexpr 8865  suplem1pr 8863  suplem2pr 8864
[Gleason] p. 123Proposition 9-3.5addclpr 8829  addclprlem1 8827  addclprlem2 8828  df-plp 8794
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8833
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8832
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8845
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8854  ltexprlem1 8847  ltexprlem2 8848  ltexprlem3 8849  ltexprlem4 8850  ltexprlem5 8851  ltexprlem6 8852  ltexprlem7 8853
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8856  ltaprlem 8855
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8857
[Gleason] p. 124Lemma 9-3.6prlem936 8858
[Gleason] p. 124Proposition 9-3.7df-mp 8795  mulclpr 8831  mulclprlem 8830  reclem2pr 8859
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8840
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8835
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8834
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8839
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8862  reclem3pr 8860  reclem4pr 8861
[Gleason] p. 126Proposition 9-4.1df-enr 8868  df-mpr 8867  df-plpr 8866  enrer 8877
[Gleason] p. 126Proposition 9-4.2df-0r 8873  df-1r 8874  df-nr 8869
[Gleason] p. 126Proposition 9-4.3df-mr 8871  df-plr 8870  negexsr 8911  recexsr 8916  recexsrlem 8912
[Gleason] p. 127Proposition 9-4.4df-ltr 8872
[Gleason] p. 130Proposition 10-1.3creui 9928  creur 9927  cru 9925
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8997  axcnre 8973
[Gleason] p. 132Definition 10-3.1crim 11848  crimd 11965  crimi 11926  crre 11847  crred 11964  crrei 11925
[Gleason] p. 132Definition 10-3.2remim 11850  remimd 11931
[Gleason] p. 133Definition 10.36absval2 12017  absval2d 12175  absval2i 12128
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11874  cjaddd 11953  cjaddi 11921
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11875  cjmuld 11954  cjmuli 11922
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11873  cjcjd 11932  cjcji 11904
[Gleason] p. 133Proposition 10-3.4(f)cjre 11872  cjreb 11856  cjrebd 11935  cjrebi 11907  cjred 11959  rere 11855  rereb 11853  rerebd 11934  rerebi 11906  rered 11957
[Gleason] p. 133Proposition 10-3.4(h)addcj 11881  addcjd 11945  addcji 11916
[Gleason] p. 133Proposition 10-3.7(a)absval 11971
[Gleason] p. 133Proposition 10-3.7(b)abscj 12012  abscjd 12180  abscji 12132
[Gleason] p. 133Proposition 10-3.7(c)abs00 12022  abs00d 12176  abs00i 12129  absne0d 12177
[Gleason] p. 133Proposition 10-3.7(d)releabs 12053  releabsd 12181  releabsi 12133
[Gleason] p. 133Proposition 10-3.7(f)absmul 12027  absmuld 12184  absmuli 12135
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 12015  sqabsaddi 12136
[Gleason] p. 133Proposition 10-3.7(h)abstri 12062  abstrid 12186  abstrii 12139
[Gleason] p. 134Definition 10-4.1df-exp 11311  exp0 11314  expp1 11316  expp1d 11452
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20438  cxpaddd 20476  expadd 11350  expaddd 11453  expaddz 11352
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20447  cxpmuld 20493  expmul 11353  expmuld 11454  expmulz 11354
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20444  mulcxpd 20487  mulexp 11347  mulexpd 11466  mulexpz 11348
[Gleason] p. 140Exercise 1znnen 12740
[Gleason] p. 141Definition 11-2.1fzval 10978
[Gleason] p. 168Proposition 12-2.1(a)climadd 12353  rlimadd 12364  rlimdiv 12367
[Gleason] p. 168Proposition 12-2.1(b)climsub 12355  rlimsub 12365
[Gleason] p. 168Proposition 12-2.1(c)climmul 12354  rlimmul 12366
[Gleason] p. 171Corollary 12-2.2climmulc2 12358
[Gleason] p. 172Corollary 12-2.5climrecl 12305
[Gleason] p. 172Proposition 12-2.4(c)climabs 12325  climcj 12326  climim 12328  climre 12327  rlimabs 12330  rlimcj 12331  rlimim 12333  rlimre 12332
[Gleason] p. 173Definition 12-3.1df-ltxr 9059  df-xr 9058  ltxr 10648
[Gleason] p. 175Definition 12-4.1df-limsup 12193  limsupval 12196
[Gleason] p. 180Theorem 12-5.1climsup 12391
[Gleason] p. 180Theorem 12-5.3caucvg 12400  caucvgb 12401  caucvgr 12397  climcau 12392
[Gleason] p. 182Exercise 3cvgcmp 12523
[Gleason] p. 182Exercise 4cvgrat 12588
[Gleason] p. 195Theorem 13-2.12abs1m 12067
[Gleason] p. 217Lemma 13-4.1btwnzge0 11158
[Gleason] p. 223Definition 14-1.1df-met 16621
[Gleason] p. 223Definition 14-1.1(a)met0 18283  xmet0 18282
[Gleason] p. 223Definition 14-1.1(b)metgt0 18298
[Gleason] p. 223Definition 14-1.1(c)metsym 18289
[Gleason] p. 223Definition 14-1.1(d)mettri 18291  mstri 18390  xmettri 18290  xmstri 18389
[Gleason] p. 225Definition 14-1.5xpsmet 18321
[Gleason] p. 230Proposition 14-2.6txlm 17602
[Gleason] p. 240Theorem 14-4.3metcnp4 19134
[Gleason] p. 240Proposition 14-4.2metcnp3 18461
[Gleason] p. 243Proposition 14-4.16addcn 18767  addcn2 12315  mulcn 18769  mulcn2 12317  subcn 18768  subcn2 12316
[Gleason] p. 295Remarkbcval3 11525  bcval4 11526
[Gleason] p. 295Equation 2bcpasc 11540
[Gleason] p. 295Definition of binomial coefficientbcval 11523  df-bc 11522
[Gleason] p. 296Remarkbcn0 11529  bcnn 11531
[Gleason] p. 296Theorem 15-2.8binom 12537
[Gleason] p. 308Equation 2ef0 12621
[Gleason] p. 308Equation 3efcj 12622
[Gleason] p. 309Corollary 15-4.3efne0 12626
[Gleason] p. 309Corollary 15-4.4efexp 12630
[Gleason] p. 310Equation 14sinadd 12693
[Gleason] p. 310Equation 15cosadd 12694
[Gleason] p. 311Equation 17sincossq 12705
[Gleason] p. 311Equation 18cosbnd 12710  sinbnd 12709
[Gleason] p. 311Lemma 15-4.7sqeqor 11423  sqeqori 11421
[Gleason] p. 311Definition of pidf-pi 12603
[Godowski] p. 730Equation SFgoeqi 23625
[GodowskiGreechie] p. 249Equation IV3oai 23019
[Gratzer] p. 23Section 0.6df-mre 13739
[Gratzer] p. 27Section 0.6df-mri 13741
[Halmos] p. 31Theorem 17.3riesz1 23417  riesz2 23418
[Halmos] p. 41Definition of Hermitianhmopadj2 23293
[Halmos] p. 42Definition of projector orderingpjordi 23525
[Halmos] p. 43Theorem 26.1elpjhmop 23537  elpjidm 23536  pjnmopi 23500
[Halmos] p. 44Remarkpjinormi 23038  pjinormii 23027
[Halmos] p. 44Theorem 26.2elpjch 23541  pjrn 23058  pjrni 23053  pjvec 23047
[Halmos] p. 44Theorem 26.3pjnorm2 23078
[Halmos] p. 44Theorem 26.4hmopidmpj 23506  hmopidmpji 23504
[Halmos] p. 45Theorem 27.1pjinvari 23543
[Halmos] p. 45Theorem 27.3pjoci 23532  pjocvec 23048
[Halmos] p. 45Theorem 27.4pjorthcoi 23521
[Halmos] p. 48Theorem 29.2pjssposi 23524
[Halmos] p. 48Theorem 29.3pjssdif1i 23527  pjssdif2i 23526
[Halmos] p. 50Definition of spectrumdf-spec 23207
[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 18889  df-phtpy 18868
[Hatcher] p. 26Definitiondf-pco 18902  df-pi1 18905
[Hatcher] p. 26Proposition 1.2phtpcer 18892
[Hatcher] p. 26Proposition 1.3pi1grp 18947
[Herstein] p. 54Exercise 28df-grpo 21628
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14749  grpoideu 21646  mndideu 14626
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14767  grpoinveu 21659
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14786  grpo2inv 21676
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14795  grpoinvop 21678
[Herstein] p. 57Exercise 1isgrp2d 21672  isgrp2i 21673
[Hitchcock] p. 5Rule A3mpto1 1539
[Hitchcock] p. 5Rule A4mpto2 1540
[Hitchcock] p. 5Rule A5mtp-xor 1542
[Holland] p. 1519Theorem 2sumdmdi 23772
[Holland] p. 1520Lemma 5cdj1i 23785  cdj3i 23793  cdj3lem1 23786  cdjreui 23784
[Holland] p. 1524Lemma 7mddmdin0i 23783
[Holland95] p. 13Theorem 3.6hlathil 32080
[Holland95] p. 14Line 15hgmapvs 32010
[Holland95] p. 14Line 16hdmaplkr 32032
[Holland95] p. 14Line 17hdmapellkr 32033
[Holland95] p. 14Line 19hdmapglnm2 32030
[Holland95] p. 14Line 20hdmapip0com 32036
[Holland95] p. 14Theorem 3.6hdmapevec2 31955
[Holland95] p. 14Lines 24 and 25hdmapoc 32050
[Holland95] p. 204Definition of involutiondf-srng 15862
[Holland95] p. 212Definition of subspacedf-psubsp 29618
[Holland95] p. 214Lemma 3.3lclkrlem2v 31644
[Holland95] p. 214Definition 3.2df-lpolN 31597
[Holland95] p. 214Definition of nonsingularpnonsingN 30048
[Holland95] p. 215Lemma 3.3(1)dihoml4 31493  poml4N 30068
[Holland95] p. 215Lemma 3.3(2)dochexmid 31584  pexmidALTN 30093  pexmidN 30084
[Holland95] p. 218Theorem 3.6lclkr 31649
[Holland95] p. 218Definition of dual vector spacedf-ldual 29240  ldualset 29241
[Holland95] p. 222Item 1df-lines 29616  df-pointsN 29617
[Holland95] p. 222Item 2df-polarityN 30018
[Holland95] p. 223Remarkispsubcl2N 30062  omllaw4 29362  pol1N 30025  polcon3N 30032
[Holland95] p. 223Definitiondf-psubclN 30050
[Holland95] p. 223Equation for polaritypolval2N 30021
[Hughes] p. 44Equation 1.21bax-his3 22435
[Hughes] p. 47Definition of projection operatordfpjop 23534
[Hughes] p. 49Equation 1.30eighmre 23315  eigre 23187  eigrei 23186
[Hughes] p. 49Equation 1.31eighmorth 23316  eigorth 23190  eigorthi 23189
[Hughes] p. 137Remark (ii)eigposi 23188
[Huneke] p. 1Theoremfrgrancvvdeq 27795  frgrancvvdgeq 27796
[Huneke] p. 1Lemma A for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemA 27790
[Huneke] p. 1Lemma B for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemB 27791
[Huneke] p. 1Lemma C for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemC 27792
[Huneke] p. 2Theoremfrgraregorufr 27806  frgraregorufr0 27805  frgrawopreg1 27803  frgrawopreg2 27804
[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 27800
[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 27801
[Indrzejczak] p. 33Definition ` `Enatded 21560  natded 21560
[Indrzejczak] p. 33Definition ` `Inatded 21560
[Indrzejczak] p. 34Definition ` `Enatded 21560  natded 21560
[Indrzejczak] p. 34Definition ` `Inatded 21560
[Jech] p. 4Definition of classcv 1648  cvjust 2383
[Jech] p. 42Lemma 6.1alephexp1 8388
[Jech] p. 42Equation 6.1alephadd 8386  alephmul 8387
[Jech] p. 43Lemma 6.2infmap 8385  infmap2 8032
[Jech] p. 71Lemma 9.3jech9.3 7674
[Jech] p. 72Equation 9.3scott0 7744  scottex 7743
[Jech] p. 72Exercise 9.1rankval4 7727
[Jech] p. 72Scheme "Collection Principle"cp 7749
[Jech] p. 78Definition implied by the footnoteopthprc 4866
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26670
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26766
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26767
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26682
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26686
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26687  rmyp1 26688
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26689  rmym1 26690
[JonesMatijasevic] p. 695Equation 2.11rmx0 26680  rmx1 26681  rmxluc 26691
[JonesMatijasevic] p. 695Equation 2.12rmy0 26684  rmy1 26685  rmyluc 26692
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26694
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26695
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26717  jm2.17b 26718  jm2.17c 26719
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26756
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26760
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26751
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26720  jm2.24nn 26716
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26765
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26771  rmygeid 26721
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26783
[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 22867  chabs1i 22869  chabs2 22868  chabs2i 22870  chjass 22884  chjassi 22837  latabs1 14444  latabs2 14445
[Kalmbach] p. 15Definition of atomdf-at 23690  ela 23691
[Kalmbach] p. 15Definition of coverscvbr2 23635  cvrval2 29390
[Kalmbach] p. 16Definitiondf-ol 29294  df-oml 29295
[Kalmbach] p. 20Definition of commutescmbr 22935  cmbri 22941  cmtvalN 29327  df-cm 22934  df-cmtN 29293
[Kalmbach] p. 22Remarkomllaw5N 29363  pjoml5 22964  pjoml5i 22939
[Kalmbach] p. 22Definitionpjoml2 22962  pjoml2i 22936
[Kalmbach] p. 22Theorem 2(v)cmcm 22965  cmcmi 22943  cmcmii 22948  cmtcomN 29365
[Kalmbach] p. 22Theorem 2(ii)omllaw3 29361  omlsi 22755  pjoml 22787  pjomli 22786
[Kalmbach] p. 22Definition of OML lawomllaw2N 29360
[Kalmbach] p. 23Remarkcmbr2i 22947  cmcm3 22966  cmcm3i 22945  cmcm3ii 22950  cmcm4i 22946  cmt3N 29367  cmt4N 29368  cmtbr2N 29369
[Kalmbach] p. 23Lemma 3cmbr3 22959  cmbr3i 22951  cmtbr3N 29370
[Kalmbach] p. 25Theorem 5fh1 22969  fh1i 22972  fh2 22970  fh2i 22973  omlfh1N 29374
[Kalmbach] p. 65Remarkchjatom 23709  chslej 22849  chsleji 22809  shslej 22731  shsleji 22721
[Kalmbach] p. 65Proposition 1chocin 22846  chocini 22805  chsupcl 22691  chsupval2 22761  h0elch 22606  helch 22595  hsupval2 22760  ocin 22647  ococss 22644  shococss 22645
[Kalmbach] p. 65Definition of subspace sumshsval 22663
[Kalmbach] p. 66Remarkdf-pjh 22746  pjssmi 23517  pjssmii 23032
[Kalmbach] p. 67Lemma 3osum 22996  osumi 22993
[Kalmbach] p. 67Lemma 4pjci 23552
[Kalmbach] p. 103Exercise 6atmd2 23752
[Kalmbach] p. 103Exercise 12mdsl0 23662
[Kalmbach] p. 140Remarkhatomic 23712  hatomici 23711  hatomistici 23714
[Kalmbach] p. 140Proposition 1atlatmstc 29435
[Kalmbach] p. 140Proposition 1(i)atexch 23733  lsatexch 29159
[Kalmbach] p. 140Proposition 1(ii)chcv1 23707  cvlcvr1 29455  cvr1 29525
[Kalmbach] p. 140Proposition 1(iii)cvexch 23726  cvexchi 23721  cvrexch 29535
[Kalmbach] p. 149Remark 2chrelati 23716  hlrelat 29517  hlrelat5N 29516  lrelat 29130
[Kalmbach] p. 153Exercise 5lsmcv 16141  lsmsatcv 29126  spansncv 23004  spansncvi 23003
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29145  spansncv2 23645
[Kalmbach] p. 266Definitiondf-st 23563
[Kalmbach2] p. 8Definition of adjointdf-adjh 23201
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8455  fpwwe2 8452
[KanamoriPincus] p. 416Corollary 1.3canth4 8456
[KanamoriPincus] p. 417Corollary 1.6canthp1 8463
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8458
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8460
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8473
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8477  gchxpidm 8478
[KanamoriPincus] p. 419Theorem 2.1gchacg 8481  gchhar 8480
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 8030  unxpwdom 7491
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8483
[Kreyszig] p. 3Property M1metcl 18272  xmetcl 18271
[Kreyszig] p. 4Property M2meteq0 18279
[Kreyszig] p. 8Definition 1.1-8dscmet 18492
[Kreyszig] p. 12Equation 5conjmul 9664  muleqadd 9599
[Kreyszig] p. 18Definition 1.3-2mopnval 18359
[Kreyszig] p. 19Remarkmopntopon 18360
[Kreyszig] p. 19Theorem T1mopn0 18419  mopnm 18365
[Kreyszig] p. 19Theorem T2unimopn 18417
[Kreyszig] p. 19Definition of neighborhoodneibl 18422
[Kreyszig] p. 20Definition 1.3-3metcnp2 18463
[Kreyszig] p. 25Definition 1.4-1lmbr 17245  lmmbr 19083  lmmbr2 19084
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17367
[Kreyszig] p. 28Theorem 1.4-5lmcau 19137
[Kreyszig] p. 28Definition 1.4-3iscau 19101  iscmet2 19119
[Kreyszig] p. 30Theorem 1.4-7cmetss 19139
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17446  metelcls 19129
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 19130  metcld2 19131
[Kreyszig] p. 51Equation 2clmvneg1 18988  lmodvneg1 15915  nvinv 21969  vcm 21899
[Kreyszig] p. 51Equation 1aclm0vs 18987  lmod0vs 15911  vc0 21897
[Kreyszig] p. 51Equation 1blmodvs0 15912  vcz 21898
[Kreyszig] p. 58Definition 2.2-1imsmet 22032
[Kreyszig] p. 59Equation 1imsdval 22027  imsdval2 22028
[Kreyszig] p. 63Problem 1nvnd 22029
[Kreyszig] p. 64Problem 2nvge0 22012  nvz 22007
[Kreyszig] p. 64Problem 3nvabs 22011
[Kreyszig] p. 91Definition 2.7-1isblo3i 22151
[Kreyszig] p. 92Equation 2df-nmoo 22095
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 22157  blocni 22155
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 22156
[Kreyszig] p. 129Definition 3.1-1cphipeq0 19038  ipeq0 16793  ipz 22067
[Kreyszig] p. 135Problem 2pythi 22200
[Kreyszig] p. 137Lemma 3-2.1(a)sii 22204
[Kreyszig] p. 144Equation 4supcvg 12563
[Kreyszig] p. 144Theorem 3.3-1minvec 19205  minveco 22235
[Kreyszig] p. 196Definition 3.9-1df-aj 22100
[Kreyszig] p. 247Theorem 4.7-2bcth 19152
[Kreyszig] p. 249Theorem 4.7-3ubth 22224
[Kreyszig] p. 470Definition of positive operator orderingleop 23475  leopg 23474
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 23493
[Kreyszig] p. 525Theorem 10.1-1htth 22270
[Kunen] p. 10Axiom 0a9e 1941  axnul 4279
[Kunen] p. 11Axiom 3axnul 4279
[Kunen] p. 12Axiom 6zfrep6 5908
[Kunen] p. 24Definition 10.24mapval 6967  mapvalg 6965
[Kunen] p. 30Lemma 10.20fodom 8336
[Kunen] p. 31Definition 10.24mapex 6961
[Kunen] p. 95Definition 2.1df-r1 7624
[Kunen] p. 97Lemma 2.10r1elss 7666  r1elssi 7665
[Kunen] p. 107Exercise 4rankop 7718  rankopb 7712  rankuni 7723  rankxplim 7737  rankxpsuc 7740
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4046
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27221
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27216
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27222
[LeBlanc] p. 277Rule R2axnul 4279
[Levy] p. 338Axiomdf-clab 2375  df-clel 2384  df-cleq 2381
[Levy58] p. 2Definition Iisfin1-3 8200
[Levy58] p. 2Definition IIdf-fin2 8100
[Levy58] p. 2Definition Iadf-fin1a 8099
[Levy58] p. 2Definition IIIdf-fin3 8102
[Levy58] p. 3Definition Vdf-fin5 8103
[Levy58] p. 3Definition IVdf-fin4 8101
[Levy58] p. 4Definition VIdf-fin6 8104
[Levy58] p. 4Definition VIIdf-fin7 8105
[Levy58], p. 3Theorem 1fin1a2 8229
[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 23760
[Maeda] p. 168Lemma 5mdsym 23764  mdsymi 23763
[Maeda] p. 168Lemma 4(i)mdsymlem4 23758  mdsymlem6 23760  mdsymlem7 23761
[Maeda] p. 168Lemma 4(ii)mdsymlem8 23762
[MaedaMaeda] p. 1Remarkssdmd1 23665  ssdmd2 23666  ssmd1 23663  ssmd2 23664
[MaedaMaeda] p. 1Lemma 1.2mddmd2 23661
[MaedaMaeda] p. 1Definition 1.1df-dmd 23633  df-md 23632  mdbr 23646
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 23683  mdslj1i 23671  mdslj2i 23672  mdslle1i 23669  mdslle2i 23670  mdslmd1i 23681  mdslmd2i 23682
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 23673  mdsl2bi 23675  mdsl2i 23674
[MaedaMaeda] p. 2Lemma 1.6mdexchi 23687
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 23684
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 23685
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 23662
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 23667  mdsl3 23668
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 23686
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23781
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 29437  hlrelat1 29515
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29155
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 23688  cvmdi 23676  cvnbtwn4 23641  cvrnbtwn4 29395
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 23689
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 29456  cvp 23727  cvrp 29531  lcvp 29156
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 23751
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 23750
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 29449  hlexch4N 29507
[MaedaMaeda] p. 34Exercise 7.1atabsi 23753
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 29558
[MaedaMaeda] p. 61Definition 15.10psubN 29864  atpsubN 29868  df-pointsN 29617  pointpsubN 29866
[MaedaMaeda] p. 62Theorem 15.5df-pmap 29619  pmap11 29877  pmaple 29876  pmapsub 29883  pmapval 29872
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29880  pmap1N 29882
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29885  pmapglb2N 29886  pmapglb2xN 29887  pmapglbx 29884
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 29967
[MaedaMaeda] p. 67Postulate PS1ps-1 29592
[MaedaMaeda] p. 68Lemma 16.2df-padd 29911  paddclN 29957  paddidm 29956
[MaedaMaeda] p. 68Condition PS2ps-2 29593
[MaedaMaeda] p. 68Equation 16.2.1paddass 29953
[MaedaMaeda] p. 69Lemma 16.4ps-1 29592
[MaedaMaeda] p. 69Theorem 16.4ps-2 29593
[MaedaMaeda] p. 70Theorem 16.9lsmmod 15235  lsmmod2 15236  lssats 29128  shatomici 23710  shatomistici 23713  shmodi 22741  shmodsi 22740
[MaedaMaeda] p. 130Remark 29.6dmdmd 23652  mdsymlem7 23761
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22940
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22844
[MaedaMaeda] p. 139Remarksumdmdii 23767
[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 28369
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 28370
[Margaris] p. 79Rule Cexinst01 28068  exinst11 28069
[Margaris] p. 89Theorem 19.219.2 1666  19.2g 1765  r19.2z 3661
[Margaris] p. 89Theorem 19.319.3 1793  19.3v 1672  rr19.3v 3021
[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 2763
[Margaris] p. 90Theorem 19.14exnal 1580
[Margaris] p. 90Theorem 19.152albi 27246  albi 1570  ralbi 2786
[Margaris] p. 90Theorem 19.1619.16 1872
[Margaris] p. 90Theorem 19.1719.17 1873
[Margaris] p. 90Theorem 19.182exbi 27248  exbi 1588
[Margaris] p. 90Theorem 19.1919.19 1874
[Margaris] p. 90Theorem 19.202alim 27245  alim 1564  alimd 1772  alimdh 1569  alimdv 1628  ralimdaa 2727  ralimdv 2729  ralimdva 2728  sbcimdv 3166
[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 27244  alrimd 1777  alrimdd 1776  alrimdh 1594  alrimdv 1640  alrimi 1773  alrimih 1571  alrimiv 1638  alrimivv 1639  r19.21 2736  r19.21be 2751  r19.21bi 2748  r19.21t 2735  r19.21v 2737  ralrimd 2738  ralrimdv 2739  ralrimdva 2740  ralrimdvv 2744  ralrimdvva 2745  ralrimi 2731  ralrimiv 2732  ralrimiva 2733  ralrimivv 2741  ralrimivva 2742  ralrimivvva 2743  ralrimivw 2734  rexlimi 2767
[Margaris] p. 90Theorem 19.222alimdv 1630  2exim 27247  2eximdv 1631  exim 1581  eximd 1778  eximdh 1595  eximdv 1629  rexim 2754  reximdai 2758  reximddv 23807  reximdv 2761  reximdv2 2759  reximdva 2762  reximdvai 2760  reximi2 2756
[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 27952  exlimi 1811  exlimih 1812  exlimiv 1641  exlimivv 1642  r19.23 2765  r19.23v 2766  rexlimd 2771  rexlimdv 2773  rexlimdv3a 2776  rexlimdva 2774  rexlimdvaa 2775  rexlimdvv 2780  rexlimdvva 2781  rexlimdvw 2777  rexlimiv 2768  rexlimiva 2769  rexlimivv 2779
[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 2783  r19.26-3 2784  r19.26 2782  r19.26m 2785
[Margaris] p. 90Theorem 19.2719.27 1831  19.27v 1906  r19.27av 2788  r19.27z 3670  r19.27zv 3671
[Margaris] p. 90Theorem 19.2819.28 1832  19.28v 1907  19.28vv 27254  r19.28av 2789  r19.28z 3664  r19.28zv 3667  rr19.28v 3022
[Margaris] p. 90Theorem 19.2919.29 1603  19.29r 1604  19.29r2 1605  19.29x 1606  r19.29 2790  r19.29d2r 2795  r19.29r 2791
[Margaris] p. 90Theorem 19.3019.30 1611  r19.30 2797
[Margaris] p. 90Theorem 19.3119.31 1886  19.31vv 27252
[Margaris] p. 90Theorem 19.3219.32 1885  r19.32 27614  r19.32v 2798
[Margaris] p. 90Theorem 19.3319.33-2 27250  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 2799
[Margaris] p. 90Theorem 19.3619.36 1881  19.36aiv 1909  19.36i 1882  19.36v 1908  19.36vv 27251  r19.36av 2800  r19.36zv 3672
[Margaris] p. 90Theorem 19.3719.37 1883  19.37aiv 1912  19.37v 1911  19.37vv 27253  r19.37 2801  r19.37av 2802  r19.37zv 3668
[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 2803
[Margaris] p. 90Theorem 19.4119.41 1889  19.41rg 27981  19.41v 1913  19.41vv 1914  19.41vvv 1915  19.41vvvv 1916  r19.41 2804  r19.41v 2805  r19.41vv 23815
[Margaris] p. 90Theorem 19.4219.42 1891  19.42v 1917  19.42vv 1919  19.42vvv 1920  r19.42v 2806
[Margaris] p. 90Theorem 19.4319.43 1612  r19.43 2807
[Margaris] p. 90Theorem 19.4419.44 1887  r19.44av 2808
[Margaris] p. 90Theorem 19.4519.45 1888  r19.45av 2809  r19.45zv 3669
[Margaris] p. 110Exercise 2(b)eu1 2260
[Mayet] p. 370Remarkjpi 23622  largei 23619  stri 23609
[Mayet3] p. 9Definition of CH-statesdf-hst 23564  ishst 23566
[Mayet3] p. 10Theoremhstrbi 23618  hstri 23617
[Mayet3] p. 1223Theorem 4.1mayete3i 23079
[Mayet3] p. 1240Theorem 7.1mayetes3i 23081
[MegPav2000] p. 2344Theorem 3.3stcltrthi 23630
[MegPav2000] p. 2345Definition 3.4-1chintcl 22683  chsupcl 22691
[MegPav2000] p. 2345Definition 3.4-2hatomic 23712
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 23706
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 23733
[MegPav2000] p. 2366Figure 7pl42N 30098
[MegPav2002] p. 362Lemma 2.2latj31 14456  latj32 14454  latjass 14452
[Megill] p. 444Axiom C5ax-17 1623  ax17o 2192
[Megill] p. 444Section 7conventions 21559
[Megill] p. 445Lemma L12aecom-o 2186  aecom 1996  ax-10 2175
[Megill] p. 446Lemma L17equtrr 1690
[Megill] p. 446Lemma L18ax9from9o 2183
[Megill] p. 446Lemma L19hbnae-o 2214  hbnae 2001
[Megill] p. 447Remark 9.1df-sb 1656  sbid 1936  sbidd-misc 27809  sbidd 27808
[Megill] p. 448Remark 9.6ax15 2055
[Megill] p. 448Scheme C4'ax-5o 2171
[Megill] p. 448Scheme C5'ax-4 2170  sp 1755
[Megill] p. 448Scheme C6'ax-7 1741
[Megill] p. 448Scheme C7'ax-6o 2172
[Megill] p. 448Scheme C8'ax-8 1682
[Megill] p. 448Scheme C9'ax-12o 2177
[Megill] p. 448Scheme C10'ax-9 1661  ax-9o 2173
[Megill] p. 448Scheme C11'ax-10o 2174
[Megill] p. 448Scheme C12'ax-13 1719
[Megill] p. 448Scheme C13'ax-14 1721
[Megill] p. 448Scheme C14'ax-15 2178
[Megill] p. 448Scheme C15'ax-11o 2176
[Megill] p. 448Scheme C16'ax-16 2179
[Megill] p. 448Theorem 9.4dral1-o 2189  dral1 2006  dral2-o 2216  dral2 2007  drex1 2008  drex2 2009  drsb1 2056  drsb2 2095
[Megill] p. 448Theorem 9.7conventions 21559
[Megill] p. 449Theorem 9.7sbcom2 2148  sbequ 2094  sbid2v 2158
[Megill] p. 450Example in Appendixhba1-o 2184  hba1 1794
[Mendelson] p. 35Axiom A3hirstL-ax3 27529
[Mendelson] p. 36Lemma 1.8id1 21
[Mendelson] p. 69Axiom 4rspsbc 3183  rspsbca 3184  stdpc4 2058
[Mendelson] p. 69Axiom 5ax-5o 2171  ra5 3189  stdpc5 1806
[Mendelson] p. 81Rule Cexlimiv 1641
[Mendelson] p. 95Axiom 6stdpc6 1694
[Mendelson] p. 95Axiom 7stdpc7 1931
[Mendelson] p. 225Axiom system NBGru 3104
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4400
[Mendelson] p. 231Exercise 4.10(k)inv1 3598
[Mendelson] p. 231Exercise 4.10(l)unv 3599
[Mendelson] p. 231Exercise 4.10(n)dfin3 3524
[Mendelson] p. 231Exercise 4.10(o)df-nul 3573
[Mendelson] p. 231Exercise 4.10(q)dfin4 3525
[Mendelson] p. 231Exercise 4.10(s)ddif 3423
[Mendelson] p. 231Definition of uniondfun3 3523
[Mendelson] p. 235Exercise 4.12(c)univ 4695
[Mendelson] p. 235Exercise 4.12(d)pwv 3957
[Mendelson] p. 235Exercise 4.12(j)pwin 4429
[Mendelson] p. 235Exercise 4.12(k)pwunss 4430
[Mendelson] p. 235Exercise 4.12(l)pwssun 4431
[Mendelson] p. 235Exercise 4.12(n)uniin 3978
[Mendelson] p. 235Exercise 4.12(p)reli 4943
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5331
[Mendelson] p. 244Proposition 4.8(g)epweon 4705
[Mendelson] p. 246Definition of successordf-suc 4529
[Mendelson] p. 250Exercise 4.36oelim2 6775
[Mendelson] p. 254Proposition 4.22(b)xpen 7207
[Mendelson] p. 254Proposition 4.22(c)xpsnen 7129  xpsneng 7130
[Mendelson] p. 254Proposition 4.22(d)xpcomen 7136  xpcomeng 7137
[Mendelson] p. 254Proposition 4.22(e)xpassen 7139
[Mendelson] p. 255Definitionbrsdom 7067
[Mendelson] p. 255Exercise 4.39endisj 7132
[Mendelson] p. 255Exercise 4.41mapprc 6959
[Mendelson] p. 255Exercise 4.43mapsnen 7121
[Mendelson] p. 255Exercise 4.45mapunen 7213
[Mendelson] p. 255Exercise 4.47xpmapen 7212
[Mendelson] p. 255Exercise 4.42(a)map0e 6988
[Mendelson] p. 255Exercise 4.42(b)map1 7122
[Mendelson] p. 257Proposition 4.24(a)undom 7133
[Mendelson] p. 258Exercise 4.56(b)cdaen 7987
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7996  cdacomen 7995
[Mendelson] p. 258Exercise 4.56(f)cdadom1 8000
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7994
[Mendelson] p. 258Definition of cardinal sumcdaval 7984  df-cda 7982
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6712
[Mendelson] p. 266Proposition 4.34(f)oaordex 6738
[Mendelson] p. 275Proposition 4.42(d)entri3 8368
[Mendelson] p. 281Definitiondf-r1 7624
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7673
[Mendelson] p. 287Axiom system MKru 3104
[MertziosUnger] p. 153Proposition 12pthfrgra 27765  2pthfrgrarn 27763  2pthfrgrarn2 27764  frconngra 27775  n4cyclfrgra 27772  vdgfrgragt2 27782  vdgn1frgrav2 27781  vdn1frgrav2 27780
[Mittelstaedt] p. 9Definitiondf-oc 22603
[Monk1] p. 22Remarkconventions 21559
[Monk1] p. 22Theorem 3.1conventions 21559
[Monk1] p. 26Theorem 2.8(vii)ssin 3507
[Monk1] p. 33Theorem 3.2(i)ssrel 4905
[Monk1] p. 33Theorem 3.2(ii)eqrel 4906
[Monk1] p. 34Definition 3.3df-opab 4209
[Monk1] p. 36Theorem 3.7(i)coi1 5326  coi2 5327
[Monk1] p. 36Theorem 3.8(v)dm0 5024  rn0 5068
[Monk1] p. 36Theorem 3.7(ii)cnvi 5217
[Monk1] p. 37Theorem 3.13(i)relxp 4924
[Monk1] p. 37Theorem 3.13(x)dmxp 5029  rnxp 5240
[Monk1] p. 37Theorem 3.13(ii)xp0 5232  xp0r 4897
[Monk1] p. 38Theorem 3.16(ii)ima0 5162
[Monk1] p. 38Theorem 3.16(viii)imai 5159
[Monk1] p. 39Theorem 3.17imaexg 5158
[Monk1] p. 39Theorem 3.16(xi)imassrn 5157
[Monk1] p. 41Theorem 4.3(i)fnopfv 5805  funfvop 5782
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5710
[Monk1] p. 42Theorem 4.4(iii)fvelima 5718
[Monk1] p. 43Theorem 4.6funun 5436
[Monk1] p. 43Theorem 4.8(iv)dff13 5944  dff13f 5946
[Monk1] p. 46Theorem 4.15(v)funex 5903  funrnex 5907
[Monk1] p. 50Definition 5.4fniunfv 5934
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5294
[Monk1] p. 52Theorem 5.11(viii)ssint 4009
[Monk1] p. 52Definition 5.13 (i)1stval2 6304  df-1st 6289
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6305  df-2nd 6290
[Monk1] p. 112Theorem 15.17(v)ranksn 7714  ranksnb 7687
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7715
[Monk1] p. 112Theorem 15.17(iii)rankun 7716  rankunb 7710
[Monk1] p. 113Theorem 15.18r1val3 7698
[Monk1] p. 113Definition 15.19df-r1 7624  r1val2 7697
[Monk1] p. 117Lemmazorn2 8320  zorn2g 8317
[Monk1] p. 133Theorem 18.11cardom 7807
[Monk1] p. 133Theorem 18.12canth3 8370
[Monk1] p. 133Theorem 18.14carduni 7802
[Monk2] p. 105Axiom C4ax-5 1563
[Monk2] p. 105Axiom C7ax-8 1682
[Monk2] p. 105Axiom C8ax-11 1753  ax-11o 2176
[Monk2] p. 105Axiom (C8)ax11v 2130
[Monk2] p. 108Lemma 5ax-5o 2171
[Monk2] p. 109Lemma 12ax-7 1741
[Monk2] p. 109Lemma 15equvin 2036  equvini 2024  eqvinop 4383
[Monk2] p. 113Axiom C5-1ax-17 1623  ax17o 2192
[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 2184  hba1 1794
[Monk2] p. 114Lemma 23nfia1 1868
[Monk2] p. 114Lemma 24nfa2 1867  nfra2 2704
[Moore] p. 53Part Idf-mre 13739
[Munkres] p. 77Example 2distop 16984  indistop 16990  indistopon 16989
[Munkres] p. 77Example 3fctop 16992  fctop2 16993
[Munkres] p. 77Example 4cctop 16994
[Munkres] p. 78Definition of basisdf-bases 16889  isbasis3g 16938
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13595  tgval2 16945
[Munkres] p. 79Remarktgcl 16958
[Munkres] p. 80Lemma 2.1tgval3 16952
[Munkres] p. 80Lemma 2.2tgss2 16976  tgss3 16975
[Munkres] p. 81Lemma 2.3basgen 16977  basgen2 16978
[Munkres] p. 89Definition of subspace topologyresttop 17147
[Munkres] p. 93Theorem 6.1(1)0cld 17026  topcld 17023
[Munkres] p. 93Theorem 6.1(2)iincld 17027
[Munkres] p. 93Theorem 6.1(3)uncld 17029
[Munkres] p. 94Definition of closureclsval 17025
[Munkres] p. 94Definition of interiorntrval 17024
[Munkres] p. 95Theorem 6.5(a)clsndisj 17063  elcls 17061
[Munkres] p. 95Theorem 6.5(b)elcls3 17071
[Munkres] p. 97Theorem 6.6clslp 17135  neindisj 17105
[Munkres] p. 97Corollary 6.7cldlp 17137
[Munkres] p. 97Definition of limit pointislp2 17133  lpval 17127
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17302
[Munkres] p. 102Definition of continuous functiondf-cn 17214  iscn 17222  iscn2 17225
[Munkres] p. 107Theorem 7.2(g)cncnp 17267  cncnp2 17268  cncnpi 17265  df-cnp 17215  iscnp 17224  iscnp2 17226
[Munkres] p. 127Theorem 10.1metcn 18464
[Munkres] p. 128Theorem 10.3metcn4 19135
[NielsenChuang] p. 195Equation 4.73unierri 23456
[Pfenning] p. 17Definition XMnatded 21560  natded 21560
[Pfenning] p. 17Definition NNCnatded 21560  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 21560
[Pfenning] p. 18Rule"natded 21560
[Pfenning] p. 18Definition /\Inatded 21560
[Pfenning] p. 18Definition ` `Enatded 21560  natded 21560  natded 21560  natded 21560  natded 21560
[Pfenning] p. 18Definition ` `Inatded 21560  natded 21560  natded 21560  natded 21560  natded 21560
[Pfenning] p. 18Definition ` `ELnatded 21560
[Pfenning] p. 18Definition ` `ERnatded 21560
[Pfenning] p. 18Definition ` `Ea,unatded 21560
[Pfenning] p. 18Definition ` `IRnatded 21560
[Pfenning] p. 18Definition ` `Ianatded 21560
[Pfenning] p. 127Definition =Enatded 21560
[Pfenning] p. 127Definition =Inatded 21560
[Ponnusamy] p. 361Theorem 6.44cphip0l 19036  df-dip 22046  dip0l 22066  ip0l 16791
[Ponnusamy] p. 361Equation 6.45ipval 22048
[Ponnusamy] p. 362Equation I1dipcj 22062
[Ponnusamy] p. 362Equation I3cphdir 19039  dipdir 22192  ipdir 16794  ipdiri 22180
[Ponnusamy] p. 362Equation I4ipidsq 22058
[Ponnusamy] p. 362Equation 6.46ip0i 22175
[Ponnusamy] p. 362Equation 6.47ip1i 22177
[Ponnusamy] p. 362Equation 6.48ip2i 22178
[Ponnusamy] p. 363Equation I2cphass 19045  dipass 22195  ipass 16800  ipassi 22191
[Prugovecki] p. 186Definition of brabraval 23296  df-bra 23202
[Prugovecki] p. 376Equation 8.1df-kb 23203  kbval 23306
[PtakPulmannova] p. 66Proposition 3.2.17atomli 23734
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30003
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 23748  atcvat4i 23749  cvrat3 29557  cvrat4 29558  lsatcvat3 29168
[PtakPulmannova] p. 68Definition 3.2.18cvbr 23634  cvrval 29385  df-cv 23631  df-lcv 29135  lspsncv0 16146
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30015
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30016
[Quine] p. 16Definition 2.1df-clab 2375  rabid 2828
[Quine] p. 17Definition 2.1''dfsb7 2156
[Quine] p. 18Definition 2.7df-cleq 2381
[Quine] p. 19Definition 2.9conventions 21559  df-v 2902
[Quine] p. 34Theorem 5.1abeq2 2493
[Quine] p. 35Theorem 5.2abid2 2505  abid2f 2549
[Quine] p. 40Theorem 6.1sb5 2134
[Quine] p. 40Theorem 6.2sb56 2132  sb6 2133
[Quine] p. 41Theorem 6.3df-clel 2384
[Quine] p. 41Theorem 6.4eqid 2388  eqid1 21610
[Quine] p. 41Theorem 6.5eqcom 2390
[Quine] p. 42Theorem 6.6df-sbc 3106
[Quine] p. 42Theorem 6.7dfsbcq 3107  dfsbcq2 3108
[Quine] p. 43Theorem 6.8vex 2903
[Quine] p. 43Theorem 6.9isset 2904
[Quine] p. 44Theorem 7.3spcgf 2975  spcgv 2980  spcimgf 2973
[Quine] p. 44Theorem 6.11spsbc 3117  spsbcd 3118
[Quine] p. 44Theorem 6.12elex 2908
[Quine] p. 44Theorem 6.13elab 3026  elabg 3027  elabgf 3024
[Quine] p. 44Theorem 6.14noel 3576
[Quine] p. 48Theorem 7.2snprc 3815
[Quine] p. 48Definition 7.1df-pr 3765  df-sn 3764
[Quine] p. 49Theorem 7.4snss 3870  snssg 3876
[Quine] p. 49Theorem 7.5prss 3896  prssg 3897
[Quine] p. 49Theorem 7.6prid1 3856  prid1g 3854  prid2 3857  prid2g 3855  snid 3785  snidg 3783
[Quine] p. 51Theorem 7.13prex 4348  snex 4347  snexALT 4327
[Quine] p. 53Theorem 8.2unisn 3974  unisnALT 28380  unisng 3975
[Quine] p. 53Theorem 8.3uniun 3977
[Quine] p. 54Theorem 8.6elssuni 3986
[Quine] p. 54Theorem 8.7uni0 3985
[Quine] p. 56Theorem 8.17uniabio 5369
[Quine] p. 56Definition 8.18dfiota2 5360
[Quine] p. 57Theorem 8.19iotaval 5370
[Quine] p. 57Theorem 8.22iotanul 5374
[Quine] p. 58Theorem 8.23iotaex 5376
[Quine] p. 58Definition 9.1df-op 3767
[Quine] p. 61Theorem 9.5opabid 4403  opelopab 4418  opelopaba 4413  opelopabaf 4420  opelopabf 4421  opelopabg 4415  opelopabga 4410  oprabid 6045
[Quine] p. 64Definition 9.11df-xp 4825
[Quine] p. 64Definition 9.12df-cnv 4827
[Quine] p. 64Definition 9.15df-id 4440
[Quine] p. 65Theorem 10.3fun0 5449
[Quine] p. 65Theorem 10.4funi 5424
[Quine] p. 65Theorem 10.5funsn 5440  funsng 5438
[Quine] p. 65Definition 10.1df-fun 5397
[Quine] p. 65Definition 10.2args 5173  dffv4 5666
[Quine] p. 68Definition 10.11conventions 21559  df-fv 5403  fv2 5664
[Quine] p. 124Theorem 17.3nn0opth2 11493  nn0opth2i 11492  nn0opthi 11491  omopthi 6837
[Quine] p. 177Definition 25.2df-rdg 6605
[Quine] p. 232Equation icarddom 8363
[Quine] p. 284Axiom 39(vi)funimaex 5472  funimaexg 5471
[Quine] p. 331Axiom system NFru 3104
[ReedSimon] p. 36Definition (iii)ax-his3 22435
[ReedSimon] p. 63Exercise 4(a)df-dip 22046  polid 22510  polid2i 22508  polidi 22509
[ReedSimon] p. 63Exercise 4(b)df-ph 22163
[ReedSimon] p. 195Remarklnophm 23371  lnophmi 23370
[Retherford] p. 49Exercise 1(i)leopadd 23484
[Retherford] p. 49Exercise 1(ii)leopmul 23486  leopmuli 23485
[Retherford] p. 49Exercise 1(iv)leoptr 23489
[Retherford] p. 49Definition VI.1df-leop 23204  leoppos 23478
[Retherford] p. 49Exercise 1(iii)leoptri 23488
[Retherford] p. 49Definition of operator orderingleop3 23477
[Rudin] p. 164Equation 27efcan 12625
[Rudin] p. 164Equation 30efzval 12631
[Rudin] p. 167Equation 48absefi 12725
[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 5190
[Schechter] p. 51Definition of irreflexivityintirr 5193
[Schechter] p. 51Definition of symmetrycnvsym 5189
[Schechter] p. 51Definition of transitivitycotr 5187
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13739
[Schechter] p. 79Definition of Moore closuredf-mrc 13740
[Schechter] p. 82Section 4.5df-mrc 13740
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13742
[Schechter] p. 139Definition AC3dfac9 7950
[Schechter] p. 141Definition (MC)dfac11 26830
[Schechter] p. 149Axiom DC1ax-dc 8260  axdc3 8268
[Schechter] p. 187Definition of ring with unitisrng 15596  isrngo 21815
[Schechter] p. 276Remark 11.6.espan0 22893
[Schechter] p. 276Definition of spandf-span 22660  spanval 22684
[Schechter] p. 428Definition 15.35bastop1 16982
[Schwabhauser] p. 10Axiom A1axcgrrflx 25568
[Schwabhauser] p. 10Axiom A2axcgrtr 25569
[Schwabhauser] p. 10Axiom A3axcgrid 25570
[Schwabhauser] p. 11Axiom A4axsegcon 25581
[Schwabhauser] p. 11Axiom A5ax5seg 25592
[Schwabhauser] p. 11Axiom A6axbtwnid 25593
[Schwabhauser] p. 12Axiom A7axpasch 25595
[Schwabhauser] p. 12Axiom A8axlowdim2 25614
[Schwabhauser] p. 13Axiom A10axeuclid 25617
[Schwabhauser] p. 13Axiom A11axcont 25630
[Schwabhauser] p. 27Theorem 2.1cgrrflx 25636
[Schwabhauser] p. 27Theorem 2.2cgrcomim 25638
[Schwabhauser] p. 27Theorem 2.3cgrtr 25641
[Schwabhauser] p. 27Theorem 2.4cgrcoml 25645
[Schwabhauser] p. 27Theorem 2.5cgrcomr 25646
[Schwabhauser] p. 28Theorem 2.8cgrtriv 25651
[Schwabhauser] p. 28Theorem 2.105segofs 25655
[Schwabhauser] p. 28Definition 2.10df-ofs 25632
[Schwabhauser] p. 29Theorem 2.11cgrextend 25657
[Schwabhauser] p. 29Theorem 2.12segconeq 25659
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 25671  btwntriv2 25661
[Schwabhauser] p. 30Theorem 3.2btwncomim 25662
[Schwabhauser] p. 30Theorem 3.3btwntriv1 25665
[Schwabhauser] p. 30Theorem 3.4btwnswapid 25666
[Schwabhauser] p. 30Theorem 3.5btwnexch2 25672  btwnintr 25668
[Schwabhauser] p. 30Theorem 3.6btwnexch 25674  btwnexch3 25669
[Schwabhauser] p. 30Theorem 3.7btwnouttr 25673
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25613
[Schwabhauser] p. 32Theorem 3.14btwndiff 25676
[Schwabhauser] p. 33Theorem 3.17trisegint 25677
[Schwabhauser] p. 34Theorem 4.2ifscgr 25693
[Schwabhauser] p. 34Definition 4.1df-ifs 25688
[Schwabhauser] p. 35Theorem 4.3cgrsub 25694
[Schwabhauser] p. 35Theorem 4.5cgrxfr 25704
[Schwabhauser] p. 35Definition 4.4df-cgr3 25689
[Schwabhauser] p. 36Theorem 4.6btwnxfr 25705
[Schwabhauser] p. 36Theorem 4.11colinearperm1 25711  colinearperm2 25713  colinearperm3 25712  colinearperm4 25714  colinearperm5 25715
[Schwabhauser] p. 36Definition 4.10df-colinear 25690
[Schwabhauser] p. 37Theorem 4.12colineartriv1 25716
[Schwabhauser] p. 37Theorem 4.13colinearxfr 25724
[Schwabhauser] p. 37Theorem 4.14lineext 25725
[Schwabhauser] p. 37Theorem 4.16fscgr 25729
[Schwabhauser] p. 37Theorem 4.17linecgr 25730
[Schwabhauser] p. 37Definition 4.15df-fs 25691
[Schwabhauser] p. 38Theorem 4.18lineid 25732
[Schwabhauser] p. 38Theorem 4.19idinside 25733
[Schwabhauser] p. 39Theorem 5.1btwnconn1 25750
[Schwabhauser] p. 41Theorem 5.2btwnconn2 25751
[Schwabhauser] p. 41Theorem 5.3btwnconn3 25752
[Schwabhauser] p. 41Theorem 5.5brsegle2 25758
[Schwabhauser] p. 41Definition 5.4df-segle 25756
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 25759
[Schwabhauser] p. 42Theorem 5.7seglerflx 25761
[Schwabhauser] p. 42Theorem 5.8segletr 25763
[Schwabhauser] p. 42Theorem 5.9segleantisym 25764
[Schwabhauser] p. 42Theorem 5.10seglelin 25765
[Schwabhauser] p. 42Theorem 5.11seglemin 25762
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 25767
[Schwabhauser] p. 43Theorem 6.2btwnoutside 25774
[Schwabhauser] p. 43Theorem 6.3broutsideof3 25775
[Schwabhauser] p. 43Theorem 6.4broutsideof 25770  df-outsideof 25769
[Schwabhauser] p. 43Definition 6.1broutsideof2 25771
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 25776
[Schwabhauser] p. 44Theorem 6.6outsideofcom 25777
[Schwabhauser] p. 44Theorem 6.7outsideoftr 25778
[Schwabhauser] p. 44Theorem 6.11outsideofeu 25780
[Schwabhauser] p. 44Definition 6.8df-ray 25787
[Schwabhauser] p. 45Part 2df-lines2 25788
[Schwabhauser] p. 45Theorem 6.13outsidele 25781
[Schwabhauser] p. 45Theorem 6.15lineunray 25796
[Schwabhauser] p. 45Theorem 6.16lineelsb2 25797
[Schwabhauser] p. 45Theorem 6.17linecom 25799  linerflx1 25798  linerflx2 25800
[Schwabhauser] p. 45Theorem 6.18linethru 25802
[Schwabhauser] p. 45Definition 6.14df-line2 25786
[Schwabhauser] p. 46Theorem 6.19linethrueu 25805
[Schwabhauser] p. 46Theorem 6.21lineintmo 25806
[Shapiro] p. 230Theorem 6.5.1dchrhash 20923  dchrsum 20921  dchrsum2 20920  sumdchr 20924
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20925  sum2dchr 20926
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15552  ablfacrp2 15553
[Shapiro], p. 328Equation 9.2.4vmasum 20868
[Shapiro], p. 329Equation 9.2.7logfac2 20869
[Shapiro], p. 329Equation 9.2.9logfacrlim 20876
[Shapiro], p. 331Equation 9.2.13vmadivsum 21044
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 21047
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 21101  vmalogdivsum2 21100
[Shapiro], p. 375Theorem 9.4.1dirith 21091  dirith2 21090
[Shapiro], p. 375Equation 9.4.3rplogsum 21089  rpvmasum 21088  rpvmasum2 21074
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 21049
[Shapiro], p. 376Equation 9.4.8dchrvmasum 21087
[Shapiro], p. 377Lemma 9.4.1dchrisum 21054  dchrisumlem1 21051  dchrisumlem2 21052  dchrisumlem3 21053  dchrisumlema 21050
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 21057
[Shapiro], p. 379Equation 9.4.16dchrmusum 21086  dchrmusumlem 21084  dchrvmasumlem 21085
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 21056
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 21058
[Shapiro], p. 382Lemma 9.4.4dchrisum0 21082  dchrisum0re 21075  dchrisumn0 21083
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 21068
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 21072
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 21073
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 21128  pntrsumbnd2 21129  pntrsumo1 21127
[Shapiro], p. 405Equation 10.2.1mudivsum 21092
[Shapiro], p. 406Equation 10.2.6mulogsum 21094
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 21096
[Shapiro], p. 407Equation 10.2.8mulog2sum 21099
[Shapiro], p. 418Equation 10.4.6logsqvma 21104
[Shapiro], p. 418Equation 10.4.8logsqvma2 21105
[Shapiro], p. 419Equation 10.4.10selberg 21110
[Shapiro], p. 420Equation 10.4.12selberg2lem 21112
[Shapiro], p. 420Equation 10.4.14selberg2 21113
[Shapiro], p. 422Equation 10.6.7selberg3 21121
[Shapiro], p. 422Equation 10.4.20selberg4lem1 21122
[Shapiro], p. 422Equation 10.4.21selberg3lem1 21119  selberg3lem2 21120
[Shapiro], p. 422Equation 10.4.23selberg4 21123
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 21117
[Shapiro], p. 428Equation 10.6.2selbergr 21130
[Shapiro], p. 429Equation 10.6.8selberg3r 21131
[Shapiro], p. 430Equation 10.6.11selberg4r 21132
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 21146
[Shapiro], p. 434Equation 10.6.27pntlema 21158  pntlemb 21159  pntlemc 21157  pntlemd 21156  pntlemg 21160
[Shapiro], p. 435Equation 10.6.29pntlema 21158
[Shapiro], p. 436Lemma 10.6.1pntpbnd 21150
[Shapiro], p. 436Lemma 10.6.2pntibnd 21155
[Shapiro], p. 436Equation 10.6.34pntlema 21158
[Shapiro], p. 436Equation 10.6.35pntlem3 21171  pntleml 21173
[Stoll] p. 13Definition of symmetric differencesymdif1 3550
[Stoll] p. 16Exercise 4.40dif 3643  dif0 3642
[Stoll] p. 16Exercise 4.8difdifdir 3659
[Stoll] p. 17Theorem 5.1(5)undifv 3646
[Stoll] p. 19Theorem 5.2(13)undm 3543
[Stoll] p. 19Theorem 5.2(13')indm 3544
[Stoll] p. 20Remarkinvdif 3526
[Stoll] p. 25Definition of ordered tripledf-ot 3768
[Stoll] p. 43Definitionuniiun 4086
[Stoll] p. 44Definitionintiin 4087
[Stoll] p. 45Definitiondf-iin 4039
[Stoll] p. 45Definition indexed uniondf-iun 4038
[Stoll] p. 176Theorem 3.4(27)iman 414
[Stoll] p. 262Example 4.1symdif1 3550
[Strang] p. 242Section 6.3expgrowth 27222
[Suppes] p. 22Theorem 2eq0 3586
[Suppes] p. 22Theorem 4eqss 3307  eqssd 3309  eqssi 3308
[Suppes] p. 23Theorem 5ss0 3602  ss0b 3601
[Suppes] p. 23Theorem 6sstr 3300  sstrALT2 28289
[Suppes] p. 23Theorem 7pssirr 3391
[Suppes] p. 23Theorem 8pssn2lp 3392
[Suppes] p. 23Theorem 9psstr 3395
[Suppes] p. 23Theorem 10pssss 3386
[Suppes] p. 25Theorem 12elin 3474  elun 3432
[Suppes] p. 26Theorem 15inidm 3494
[Suppes] p. 26Theorem 16in0 3597
[Suppes] p. 27Theorem 23unidm 3434
[Suppes] p. 27Theorem 24un0 3596
[Suppes] p. 27Theorem 25ssun1 3454
[Suppes] p. 27Theorem 26ssequn1 3461
[Suppes] p. 27Theorem 27unss 3465
[Suppes] p. 27Theorem 28indir 3533
[Suppes] p. 27Theorem 29undir 3534
[Suppes] p. 28Theorem 32difid 3640  difidALT 3641
[Suppes] p. 29Theorem 33difin 3522
[Suppes] p. 29Theorem 34indif 3527
[Suppes] p. 29Theorem 35undif1 3647
[Suppes] p. 29Theorem 36difun2 3651
[Suppes] p. 29Theorem 37difin0 3645
[Suppes] p. 29Theorem 38disjdif 3644
[Suppes] p. 29Theorem 39difundi 3537
[Suppes] p. 29Theorem 40difindi 3539
[Suppes] p. 30Theorem 41nalset 4282
[Suppes] p. 39Theorem 61uniss 3979
[Suppes] p. 39Theorem 65uniop 4401
[Suppes] p. 41Theorem 70intsn 4029
[Suppes] p. 42Theorem 71intpr 4026  intprg 4027
[Suppes] p. 42Theorem 73op1stb 4699
[Suppes] p. 42Theorem 78intun 4025
[Suppes] p. 44Definition 15(a)dfiun2 4068  dfiun2g 4066
[Suppes] p. 44Definition 15(b)dfiin2 4069
[Suppes] p. 47Theorem 86elpw 3749  elpw2 4306  elpw2g 4305  elpwg 3750  elpwgdedVD 28371
[Suppes] p. 47Theorem 87pwid 3756
[Suppes] p. 47Theorem 89pw0 3889
[Suppes] p. 48Theorem 90pwpw0 3890
[Suppes] p. 52Theorem 101xpss12 4922
[Suppes] p. 52Theorem 102xpindi 4949  xpindir 4950
[Suppes] p. 52Theorem 103xpundi 4871  xpundir 4872
[Suppes] p. 54Theorem 105elirrv 7499
[Suppes] p. 58Theorem 2relss 4904
[Suppes] p. 59Theorem 4eldm 5008  eldm2 5009  eldm2g 5007  eldmg 5006
[Suppes] p. 59Definition 3df-dm 4829
[Suppes] p. 60Theorem 6dmin 5018
[Suppes] p. 60Theorem 8rnun 5221
[Suppes] p. 60Theorem 9rnin 5222
[Suppes] p. 60Definition 4dfrn2 5000
[Suppes] p. 61Theorem 11brcnv 4996  brcnvg 4994
[Suppes] p. 62Equation 5elcnv 4990  elcnv2 4991
[Suppes] p. 62Theorem 12relcnv 5183
[Suppes] p. 62Theorem 15cnvin 5220
[Suppes] p. 62Theorem 16cnvun 5218
[Suppes] p. 63Theorem 20co02 5324
[Suppes] p. 63Theorem 21dmcoss 5076
[Suppes] p. 63Definition 7df-co 4828
[Suppes] p. 64Theorem 26cnvco 4997
[Suppes] p. 64Theorem 27coass 5329
[Suppes] p. 65Theorem 31resundi 5101
[Suppes] p. 65Theorem 34elima 5149  elima2 5150  elima3 5151  elimag 5148
[Suppes] p. 65Theorem 35imaundi 5225
[Suppes] p. 66Theorem 40dminss 5227
[Suppes] p. 66Theorem 41imainss 5228
[Suppes] p. 67Exercise 11cnvxp 5231
[Suppes] p. 81Definition 34dfec2 6845
[Suppes] p. 82Theorem 72elec 6881  elecg 6880
[Suppes] p. 82Theorem 73erth 6886  erth2 6887
[Suppes] p. 83Theorem 74erdisj 6889
[Suppes] p. 89Theorem 96map0b 6989
[Suppes] p. 89Theorem 97map0 6991  map0g 6990
[Suppes] p. 89Theorem 98mapsn 6992
[Suppes] p. 89Theorem 99mapss 6993
[Suppes] p. 91Definition 12(ii)alephsuc 7883
[Suppes] p. 91Definition 12(iii)alephlim 7882
[Suppes] p. 92Theorem 1enref 7077  enrefg 7076
[Suppes] p. 92Theorem 2ensym 7093  ensymb 7092  ensymi 7094
[Suppes] p. 92Theorem 3entr 7096
[Suppes] p. 92Theorem 4unen 7126
[Suppes] p. 94Theorem 15endom 7071
[Suppes] p. 94Theorem 16ssdomg 7090
[Suppes] p. 94Theorem 17domtr 7097
[Suppes] p. 95Theorem 18sbth 7164
[Suppes] p. 97Theorem 23canth2 7197  canth2g 7198
[Suppes] p. 97Definition 3brsdom2 7168  df-sdom 7049  dfsdom2 7167
[Suppes] p. 97Theorem 21(i)sdomirr 7181
[Suppes] p. 97Theorem 22(i)domnsym 7170
[Suppes] p. 97Theorem 21(ii)sdomnsym 7169
[Suppes] p. 97Theorem 22(ii)domsdomtr 7179
[Suppes] p. 97Theorem 22(iv)brdom2 7074
[Suppes] p. 97Theorem 21(iii)sdomtr 7182
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7177
[Suppes] p. 98Exercise 4fundmen 7117  fundmeng 7118
[Suppes] p. 98Exercise 6xpdom3 7143
[Suppes] p. 98Exercise 11sdomentr 7178
[Suppes] p. 104Theorem 37fofi 7329
[Suppes] p. 104Theorem 38pwfi 7338
[Suppes] p. 105Theorem 40pwfi 7338
[Suppes] p. 111Axiom for cardinal numberscarden 8360
[Suppes] p. 130Definition 3df-tr 4245
[Suppes] p. 132Theorem 9ssonuni 4708
[Suppes] p. 134Definition 6df-suc 4529
[Suppes] p. 136Theorem Schema 22findes 4816  finds 4812  finds1 4815  finds2 4814
[Suppes] p. 151Theorem 42isfinite 7541  isfinite2 7302  isfiniteg 7304  unbnn 7300
[Suppes] p. 162Definition 5df-ltnq 8729  df-ltpq 8721
[Suppes] p. 197Theorem Schema 4tfindes 4783  tfinds 4780  tfinds2 4784
[Suppes] p. 209Theorem 18oaord1 6731
[Suppes] p. 209Theorem 21oaword2 6733
[Suppes] p. 211Theorem 25oaass 6741
[Suppes] p. 225Definition 8iscard2 7797
[Suppes] p. 227Theorem 56ondomon 8372
[Suppes] p. 228Theorem 59harcard 7799
[Suppes] p. 228Definition 12(i)aleph0 7881
[Suppes] p. 228Theorem Schema 61onintss 4573
[Suppes] p. 228Theorem Schema 62onminesb 4719  onminsb 4720
[Suppes] p. 229Theorem 64alephval2 8381
[Suppes] p. 229Theorem 65alephcard 7885
[Suppes] p. 229Theorem 66alephord2i 7892
[Suppes] p. 229Theorem 67alephnbtwn 7886
[Suppes] p. 229Definition 12df-aleph 7761
[Suppes] p. 242Theorem 6weth 8309
[Suppes] p. 242Theorem 8entric 8366
[Suppes] p. 242Theorem 9carden 8360
[TakeutiZaring] p. 8Axiom 1ax-ext 2369
[TakeutiZaring] p. 13Definition 4.5df-cleq 2381
[TakeutiZaring] p. 13Proposition 4.6df-clel 2384
[TakeutiZaring] p. 13Proposition 4.9cvjust 2383
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2405
[TakeutiZaring] p. 14Definition 4.16df-oprab 6025
[TakeutiZaring] p. 14Proposition 4.14ru 3104
[TakeutiZaring] p. 15Axiom 2zfpair 4343
[TakeutiZaring] p. 15Exercise 1elpr 3776  elpr2 3777  elprg 3775
[TakeutiZaring] p. 15Exercise 2elsn 3773  elsnc 3781  elsnc2 3787  elsnc2g 3786  elsncg 3780
[TakeutiZaring] p. 15Exercise 3elop 4371
[TakeutiZaring] p. 15Exercise 4sneq 3769  sneqr 3909
[TakeutiZaring] p. 15Definition 5.1dfpr2 3774  dfsn2 3772
[TakeutiZaring] p. 16Axiom 3uniex 4646
[TakeutiZaring] p. 16Exercise 6opth 4377
[TakeutiZaring] p. 16Exercise 7opex 4369
[TakeutiZaring] p. 16Exercise 8rext 4354
[TakeutiZaring] p. 16Corollary 5.8unex 4648  unexg 4651
[TakeutiZaring] p. 16Definition 5.3dftp2 3798
[TakeutiZaring] p. 16Definition 5.5df-uni 3959
[TakeutiZaring] p. 16Definition 5.6df-in 3271  df-un 3269
[TakeutiZaring] p. 16Proposition 5.7unipr 3972  uniprg 3973
[TakeutiZaring] p. 17Axiom 4pwex 4324  pwexg 4325
[TakeutiZaring] p. 17Exercise 1eltp 3797
[TakeutiZaring] p. 17Exercise 5elsuc 4592  elsucg 4590  sstr2 3299
[TakeutiZaring] p. 17Exercise 6uncom 3435
[TakeutiZaring] p. 17Exercise 7incom 3477
[TakeutiZaring] p. 17Exercise 8unass 3448
[TakeutiZaring] p. 17Exercise 9inass 3495
[TakeutiZaring] p. 17Exercise 10indi 3531
[TakeutiZaring] p. 17Exercise 11undi 3532
[TakeutiZaring] p. 17Definition 5.9df-pss 3280  dfss2 3281
[TakeutiZaring] p. 17Definition 5.10df-pw 3745
[TakeutiZaring] p. 18Exercise 7unss2 3462
[TakeutiZaring] p. 18Exercise 9df-ss 3278  sseqin2 3504
[TakeutiZaring] p. 18Exercise 10ssid 3311
[TakeutiZaring] p. 18Exercise 12inss1 3505  inss2 3506
[TakeutiZaring] p. 18Exercise 13nss 3350
[TakeutiZaring] p. 18Exercise 15unieq 3967
[TakeutiZaring] p. 18Exercise 18sspwb 4355  sspwimp 28372  sspwimpALT 28379  sspwimpALT2 28383  sspwimpcf 28374
[TakeutiZaring] p. 18Exercise 19pweqb 4362
[TakeutiZaring] p. 19Axiom 5ax-rep 4262
[TakeutiZaring] p. 20Definitiondf-rab 2659
[TakeutiZaring] p. 20Corollary 5.160ex 4281
[TakeutiZaring] p. 20Definition 5.12df-dif 3267
[TakeutiZaring] p. 20Definition 5.14dfnul2 3574
[TakeutiZaring] p. 20Proposition 5.15difid 3640  difidALT 3641
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3581  n0f 3580  neq0 3582
[TakeutiZaring] p. 21Axiom 6zfreg 7497
[TakeutiZaring] p. 21Axiom 6'zfregs 7602
[TakeutiZaring] p. 21Theorem 5.22setind 7607
[TakeutiZaring] p. 21Definition 5.20df-v 2902
[TakeutiZaring] p. 21Proposition 5.21vprc 4283
[TakeutiZaring] p. 22Exercise 10ss 3600
[TakeutiZaring] p. 22Exercise 3ssex 4289  ssexg 4291
[TakeutiZaring] p. 22Exercise 4inex1 4286
[TakeutiZaring] p. 22Exercise 5ruv 7502
[TakeutiZaring] p. 22Exercise 6elirr 7500
[TakeutiZaring] p. 22Exercise 7ssdif0 3630
[TakeutiZaring] p. 22Exercise 11difdif 3417
[TakeutiZaring] p. 22Exercise 13undif3 3546  undif3VD 28336
[TakeutiZaring] p. 22Exercise 14difss 3418
[TakeutiZaring] p. 22Exercise 15sscon 3425
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2655
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2656
[TakeutiZaring] p. 23Proposition 6.2xpex 4931  xpexg 4930  xpexgALT 6237
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4826
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5454
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5588  fun11 5457
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5407  svrelfun 5455
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4999
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5001
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4831
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4832
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4828
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5266  dfrel2 5262
[TakeutiZaring] p. 25Exercise 3xpss 4923
[TakeutiZaring] p. 25Exercise 5relun 4932
[TakeutiZaring] p. 25Exercise 6reluni 4938
[TakeutiZaring] p. 25Exercise 9inxp 4948
[TakeutiZaring] p. 25Exercise 12relres 5115
[TakeutiZaring] p. 25Exercise 13opelres 5092  opelresg 5094
[TakeutiZaring] p. 25Exercise 14dmres 5108
[TakeutiZaring] p. 25Exercise 15resss 5111
[TakeutiZaring] p. 25Exercise 17resabs1 5116
[TakeutiZaring] p. 25Exercise 18funres 5433
[TakeutiZaring] p. 25Exercise 24relco 5309
[TakeutiZaring] p. 25Exercise 29funco 5432
[TakeutiZaring] p. 25Exercise 30f1co 5589
[TakeutiZaring] p. 26Definition 6.10eu2 2264
[TakeutiZaring] p. 26Definition 6.11conventions 21559  df-fv 5403  fv3 5685
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5347  cnvexg 5346
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5073  dmexg 5071
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5074  rnexg 5072
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27327
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27328
[TakeutiZaring] p. 27Corollary 6.13fvex 5683
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 27708  tz6.12-1 5688  tz6.12-afv 27707  tz6.12 5689  tz6.12c 5691
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5660  tz6.12i 5692
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5398
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5399
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5401  wfo 5393
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5400  wf1 5392
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5402  wf1o 5394
[TakeutiZaring] p. 28Exercise 4eqfnfv 5767  eqfnfv2 5768  eqfnfv2f 5771
[TakeutiZaring] p. 28Exercise 5fvco 5739
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5901  fnexALT 5902
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5897  resfunexgALT 5898
[TakeutiZaring] p. 29Exercise 9funimaex 5472  funimaexg 5471
[TakeutiZaring] p. 29Definition 6.18df-br 4155
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4446
[TakeutiZaring] p. 30Definition 6.21dffr2 4489  dffr3 5177  eliniseg 5174  iniseg 5176
[TakeutiZaring] p. 30Definition 6.22df-eprel 4436
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4502  fr3nr 4701  frirr 4501
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4483
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4703
[TakeutiZaring] p. 31Exercise 1frss 4491
[TakeutiZaring] p. 31Exercise 4wess 4511
[TakeutiZaring] p. 31Proposition 6.26tz6.26 25230  tz6.26i 25231  wefrc 4518  wereu2 4521
[TakeutiZaring] p. 32Theorem 6.27wfi 25232  wfii 25233
[TakeutiZaring] p. 32Definition 6.28df-isom 5404
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5989
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5990
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5996
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5997
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5998
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6002
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6009
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6011
[TakeutiZaring] p. 35Notationwtr 4244
[TakeutiZaring] p. 35Theorem 7.2trelpss 27329  tz7.2 4508
[TakeutiZaring] p. 35Definition 7.1dftr3 4248
[TakeutiZaring] p. 36Proposition 7.4ordwe 4536
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4544
[TakeutiZaring] p. 36Proposition 7.6ordelord 4545  ordelordALT 27966  ordelordALTVD 28321
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4551  ordelssne 4550
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4549
[TakeutiZaring] p. 37Proposition 7.9ordin 4553
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4710
[TakeutiZaring] p. 38Corollary 7.15ordsson 4711
[TakeutiZaring] p. 38Definition 7.11df-on 4527
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4555
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27979  ordon 4704
[TakeutiZaring] p. 38Proposition 7.13onprc 4706
[TakeutiZaring] p. 39Theorem 7.17tfi 4774
[TakeutiZaring] p. 40Exercise 3ontr2 4570
[TakeutiZaring] p. 40Exercise 7dftr2 4246
[TakeutiZaring] p. 40Exercise 9onssmin 4718
[TakeutiZaring] p. 40Exercise 11unon 4752
[TakeutiZaring] p. 40Exercise 12ordun 4624
[TakeutiZaring] p. 40Exercise 14ordequn 4623
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4707
[TakeutiZaring] p. 40Proposition 7.20elssuni 3986
[TakeutiZaring] p. 41Definition 7.22df-suc 4529
[TakeutiZaring] p. 41Proposition 7.23sssucid 4600  sucidg 4601
[TakeutiZaring] p. 41Proposition 7.24suceloni 4734
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4614  ordnbtwn 4613
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4749
[TakeutiZaring] p. 42Exercise 1df-lim 4528
[TakeutiZaring] p. 42Exercise 4omssnlim 4800
[TakeutiZaring] p. 42Exercise 7ssnlim 4804
[TakeutiZaring] p. 42Exercise 8onsucssi 4762  ordelsuc 4741
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4743
[TakeutiZaring] p. 42Definition 7.27nlimon 4772
[TakeutiZaring] p. 42Definition 7.28dfom2 4788
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4805
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4806
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4807
[TakeutiZaring] p. 43Remarkomon 4797
[TakeutiZaring] p. 43Axiom 7inf3 7524  omex 7532
[TakeutiZaring] p. 43Theorem 7.32ordom 4795
[TakeutiZaring] p. 43Corollary 7.31find 4811
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4808
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4809
[TakeutiZaring] p. 44Exercise 1limomss 4791
[TakeutiZaring] p. 44Exercise 2int0 4007  trint0 4261
[TakeutiZaring] p. 44Exercise 4intss1 4008
[TakeutiZaring] p. 44Exercise 5intex 4298
[TakeutiZaring] p. 44Exercise 6oninton 4721
[TakeutiZaring] p. 44Exercise 11ordintdif 4572
[TakeutiZaring] p. 44Definition 7.35df-int 3994
[TakeutiZaring] p. 44Proposition 7.34noinfep 7548
[TakeutiZaring] p. 45Exercise 4onint 4716
[TakeutiZaring] p. 47Lemma 1tfrlem1 6573
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6595
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6596
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6597
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6601  tz7.44-2 6602  tz7.44-3 6603
[TakeutiZaring] p. 50Exercise 1smogt 6566
[TakeutiZaring] p. 50Exercise 3smoiso 6561
[TakeutiZaring] p. 50Definition 7.46df-smo 6545
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6639  tz7.49c 6640
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6637
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6636
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6638
[TakeutiZaring] p. 53Proposition 7.532eu5 2323
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7827
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7828
[TakeutiZaring] p. 56Definition 8.1oalim 6713  oasuc 6705
[TakeutiZaring] p. 57Remarktfindsg 4781
[TakeutiZaring] p. 57Proposition 8.2oacl 6716
[TakeutiZaring] p. 57Proposition 8.3oa0 6697  oa0r 6719
[TakeutiZaring] p. 57Proposition 8.16omcl 6717
[TakeutiZaring] p. 58Corollary 8.5oacan 6728
[TakeutiZaring] p. 58Proposition 8.4nnaord 6799  nnaordi 6798  oaord 6727  oaordi 6726
[TakeutiZaring] p. 59Proposition 8.6iunss2 4078  uniss2 3989
[TakeutiZaring] p. 59Proposition 8.7oawordri 6730
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6735  oawordex 6737
[TakeutiZaring] p. 59Proposition 8.9nnacl 6791
[TakeutiZaring] p. 59Proposition 8.10oaabs 6824
[TakeutiZaring] p. 60Remarkoancom 7540
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6740
[TakeutiZaring] p. 62Exercise 1nnarcl 6796
[TakeutiZaring] p. 62Exercise 5oaword1 6732
[TakeutiZaring] p. 62Definition 8.15om0 6698  om0x 6700  omlim 6714  omsuc 6707
[TakeutiZaring] p. 63Proposition 8.17nnecl 6793  nnmcl 6792
[TakeutiZaring] p. 63Proposition 8.19nnmord 6812  nnmordi 6811  omord 6748  omordi 6746
[TakeutiZaring] p. 63Proposition 8.20omcan 6749
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6816  omwordri 6752
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6720
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6722  om1r 6723
[TakeutiZaring] p. 64Proposition 8.22om00 6755
[TakeutiZaring] p. 64Proposition 8.23omordlim 6757
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6758
[TakeutiZaring] p. 64Proposition 8.25odi 6759
[TakeutiZaring] p. 65Theorem 8.26omass 6760
[TakeutiZaring] p. 67Definition 8.30nnesuc 6788  oe0 6703  oelim 6715  oesuc 6708  onesuc 6711
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6701
[TakeutiZaring] p. 67Proposition 8.32oen0 6766
[TakeutiZaring] p. 67Proposition 8.33oeordi 6767
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6702
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6725
[TakeutiZaring] p. 68Corollary 8.34oeord 6768
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6774
[TakeutiZaring] p. 68Proposition 8.35oewordri 6772
[TakeutiZaring] p. 68Proposition 8.37oeworde 6773
[TakeutiZaring] p. 69Proposition 8.41oeoa 6777
[TakeutiZaring] p. 70Proposition 8.42oeoe 6779
[TakeutiZaring] p. 73Theorem 9.1trcl 7598  tz9.1 7599
[TakeutiZaring] p. 76Definition 9.9df-r1 7624  r10 7628  r1lim 7632  r1limg 7631  r1suc 7630  r1sucg 7629
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7640  r1ord2 7641  r1ordg 7638
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7650
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7675  tz9.13 7651  tz9.13g 7652
[TakeutiZaring] p. 79Definition 9.14df-rank 7625  rankval 7676  rankvalb 7657  rankvalg 7677
[TakeutiZaring] p. 79Proposition 9.16rankel 7699  rankelb 7684
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7713  rankval3 7700  rankval3b 7686
[TakeutiZaring] p. 79Proposition 9.18rankonid 7689
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7655
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7694  rankr1c 7681  rankr1g 7692
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7695
[TakeutiZaring] p. 80Exercise 1rankss 7709  rankssb 7708
[TakeutiZaring] p. 80Exercise 2unbndrank 7702
[TakeutiZaring] p. 80Proposition 9.19bndrank 7701
[TakeutiZaring] p. 83Axiom of Choiceac4 8289  dfac3 7936
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7845  numth 8286  numth2 8285
[TakeutiZaring] p. 85Definition 10.4cardval 8355
[TakeutiZaring] p. 85Proposition 10.5cardid 8356  cardid2 7774
[TakeutiZaring] p. 85Proposition 10.9oncard 7781
[TakeutiZaring] p. 85Proposition 10.10carden 8360
[TakeutiZaring] p. 85Proposition 10.11cardidm 7780
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7765
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7786
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7778
[TakeutiZaring] p. 87Proposition 10.15pwen 7217
[TakeutiZaring] p. 88Exercise 1en0 7107
[TakeutiZaring] p. 88Exercise 7infensuc 7222
[TakeutiZaring] p. 89Exercise 10omxpen 7147
[TakeutiZaring] p. 90Corollary 10.23cardnn 7784
[TakeutiZaring] p. 90Definition 10.27alephiso 7913
[TakeutiZaring] p. 90Proposition 10.20nneneq 7227
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7233
[TakeutiZaring] p. 90Proposition 10.26alephprc 7914
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7232
[TakeutiZaring] p. 91Exercise 2alephle 7903
[TakeutiZaring] p. 91Exercise 3aleph0 7881
[TakeutiZaring] p. 91Exercise 4cardlim 7793
[TakeutiZaring] p. 91Exercise 7infpss 8031
[TakeutiZaring] p. 91Exercise 8infcntss 7317
[TakeutiZaring] p. 91Definition 10.29df-fin 7050  isfi 7068
[TakeutiZaring] p. 92Proposition 10.32onfin 7234
[TakeutiZaring] p. 92Proposition 10.34imadomg 8346
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 7140
[TakeutiZaring] p. 93Proposition 10.35fodomb 8338
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8003  unxpdom 7253
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7795  cardsdomelir 7794
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7255
[TakeutiZaring] p. 94Proposition 10.39infxpen 7830
[TakeutiZaring] p. 95Definition 10.42df-map 6957
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8371  infxpidm2 7832
[TakeutiZaring] p. 95Proposition 10.41infcda 8022  infxp 8029
[TakeutiZaring] p. 96Proposition 10.44pw2en 7152  pw2f1o 7150
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7210
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8301
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8296  ac6s5 8305
[TakeutiZaring] p. 98Theorem 10.47unidom 8352
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8353  uniimadomf 8354
[TakeutiZaring] p. 100Definition 11.1cfcof 8088
[TakeutiZaring] p. 101Proposition 11.7cofsmo 8083
[TakeutiZaring] p. 102Exercise 1cfle 8068
[TakeutiZaring] p. 102Exercise 2cf0 8065
[TakeutiZaring] p. 102Exercise 3cfsuc 8071
[TakeutiZaring] p. 102Exercise 4cfom 8078
[TakeutiZaring] p. 102Proposition 11.9coftr 8087
[TakeutiZaring] p. 103Theorem 11.15alephreg 8391
[TakeutiZaring] p. 103Proposition 11.11cardcf 8066
[TakeutiZaring] p. 103Proposition 11.13alephsing 8090
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7912
[TakeutiZaring] p. 104Proposition 11.16carduniima 7911
[TakeutiZaring] p. 104Proposition 11.18alephfp 7923  alephfp2 7924
[TakeutiZaring] p. 106Theorem 11.20gchina 8508
[TakeutiZaring] p. 106Theorem 11.21mappwen 7927
[TakeutiZaring] p. 107Theorem 11.26konigth 8378
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8392
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8393
[Tarski] p. 67Axiom B5ax-4 2170
[Tarski] p. 67Scheme B5sp 1755
[Tarski] p. 68Lemma 6avril1 21606  equid 1683  equid1 2193  equid1ALT 2211
[Tarski] p. 69Lemma 7equcomi 1686
[Tarski] p. 70Lemma 14spim 1948  spime 1950  spimeh 1674
[Tarski] p. 70Lemma 16ax-11 1753  ax-11o 2176  ax11i 1654
[Tarski] p. 70Lemmas 16 and 17sb6 2133
[Tarski] p. 75Axiom B7ax9v 1662
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1623  ax17o 2192
[Tarski], p. 75Scheme B8 of system S2ax-13 1719  ax-14 1721  ax-8 1682
[Truss] p. 114Theorem 5.18ruc 12770
[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 2336  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 28381
[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 21559  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 25945
[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 25938
[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 27223
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27224
[WhiteheadRussell] p. 147Theorem *10.2219.26 1600
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27225
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27226
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27227
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1622
[WhiteheadRussell] p. 151Theorem *10.301albitr 27228
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27229
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27230
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27231
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27232
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27234
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27235
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27236
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27233
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2149
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27239
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27240
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27241
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1745
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27242
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27243
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27244
[WhiteheadRussell] p. 162Theorem *11.322alim 27245
[WhiteheadRussell] p. 162Theorem *11.332albi 27246
[WhiteheadRussell] p. 162Theorem *11.342exim 27247
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27249
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27248
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1617
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27251
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27252
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27250
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1579
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27253
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27254
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1587
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27255
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1905
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27256
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27261
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27257
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27258
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27259
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27260
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27265
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27262
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27263
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27264
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27266
[WhiteheadRussell] p. 175Definition *14.02df-eu 2243
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27277  pm13.13b 27278
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27279
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2623
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2624
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3020
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27285
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27286
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27280
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27983  pm13.193 27281
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27282
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27283
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27284
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27291
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27290
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27289
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3157
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27292  pm14.122b 27293  pm14.122c 27294
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27295  pm14.123b 27296  pm14.123c 27297
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27299
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27298
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27300
[WhiteheadRussell] p. 190Theorem *14.22iota4 5377
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27301
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5378
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27302
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27304
[WhiteheadRussell] p. 192Theorem *14.26eupick 2302  eupickbi 2305  sbaniota 27305
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27303
[WhiteheadRussell] p. 192Theorem *14.271eubi 27306
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27307
[WhiteheadRussell] p. 235Definition *30.01conventions 21559  df-fv 5403
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7821  pm54.43lem 7820
[Young] p. 141Definition of operator orderingleop2 23476
[Young] p. 142Example 12.2(i)0leop 23482  idleop 23483
[vandenDries] p. 42Lemma 61irrapx1 26583
[vandenDries] p. 43Theorem 62pellex 26590  pellexlem1 26584

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