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 13944
[Adamek] p. 29Proposition 3.14(1)invinv 13958
[Adamek] p. 29Proposition 3.14(2)invco 13959  isoco 13961
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18703  df-nmoo 22207
[AkhiezerGlazman] p. 64Theoremhmopidmch 23617  hmopidmchi 23615
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 23665  pjcmul2i 23666
[AkhiezerGlazman] p. 72Theoremcnvunop 23382  unoplin 23384
[AkhiezerGlazman] p. 72Equation 2unopadj 23383  unopadj2 23402
[AkhiezerGlazman] p. 73Theoremelunop2 23477  lnopunii 23476
[AkhiezerGlazman] p. 80Proposition 1adjlnop 23550
[Apostol] p. 18Theorem I.1addcan 9214  addcan2d 9234  addcan2i 9224  addcand 9233  addcani 9223
[Apostol] p. 18Theorem I.2negeu 9260
[Apostol] p. 18Theorem I.3negsub 9313  negsubd 9381  negsubi 9342
[Apostol] p. 18Theorem I.4negneg 9315  negnegd 9366  negnegi 9334
[Apostol] p. 18Theorem I.5subdi 9431  subdid 9453  subdii 9446  subdir 9432  subdird 9454  subdiri 9447
[Apostol] p. 18Theorem I.6mul01 9209  mul01d 9229  mul01i 9220  mul02 9208  mul02d 9228  mul02i 9219
[Apostol] p. 18Theorem I.7mulcan 9623  mulcan2d 9620  mulcand 9619  mulcani 9625
[Apostol] p. 18Theorem I.8receu 9631  xreceu 24129
[Apostol] p. 18Theorem I.9divrec 9658  divrecd 9757  divreci 9723  divreczi 9716
[Apostol] p. 18Theorem I.10recrec 9675  recreci 9710
[Apostol] p. 18Theorem I.11mul0or 9626  mul0ord 9636  mul0ori 9634
[Apostol] p. 18Theorem I.12mul2neg 9437  mul2negd 9452  mul2negi 9445  mulneg1 9434  mulneg1d 9450  mulneg1i 9443
[Apostol] p. 18Theorem I.13divadddiv 9693  divadddivd 9798  divadddivi 9740
[Apostol] p. 18Theorem I.14divmuldiv 9678  divmuldivd 9795  divmuldivi 9738  rdivmuldivd 24188
[Apostol] p. 18Theorem I.15divdivdiv 9679  divdivdivd 9801  divdivdivi 9741
[Apostol] p. 20Axiom 7rpaddcl 10596  rpaddcld 10627  rpmulcl 10597  rpmulcld 10628
[Apostol] p. 20Axiom 8rpneg 10605
[Apostol] p. 20Axiom 90nrp 10606
[Apostol] p. 20Theorem I.17lttri 9163
[Apostol] p. 20Theorem I.18ltadd1d 9583  ltadd1dd 9601  ltadd1i 9545
[Apostol] p. 20Theorem I.19ltmul1 9824  ltmul1a 9823  ltmul1i 9893  ltmul1ii 9903  ltmul2 9825  ltmul2d 10650  ltmul2dd 10664  ltmul2i 9896
[Apostol] p. 20Theorem I.20msqgt0 9512  msqgt0d 9558  msqgt0i 9528
[Apostol] p. 20Theorem I.210lt1 9514
[Apostol] p. 20Theorem I.23lt0neg1 9498  lt0neg1d 9560  ltneg 9492  ltnegd 9568  ltnegi 9535
[Apostol] p. 20Theorem I.25lt2add 9477  lt2addd 9612  lt2addi 9553
[Apostol] p. 20Definition of positive numbersdf-rp 10577
[Apostol] p. 21Exercise 4recgt0 9818  recgt0d 9909  recgt0i 9879  recgt0ii 9880
[Apostol] p. 22Definition of integersdf-z 10247
[Apostol] p. 22Definition of positive integersdfnn3 9978
[Apostol] p. 22Definition of rationalsdf-q 10539
[Apostol] p. 24Theorem I.26supeu 7423
[Apostol] p. 26Theorem I.28nnunb 10181
[Apostol] p. 26Theorem I.29arch 10182
[Apostol] p. 28Exercise 2btwnz 10336
[Apostol] p. 28Exercise 3nnrecl 10183
[Apostol] p. 28Exercise 4rebtwnz 10537
[Apostol] p. 28Exercise 5zbtwnre 10536
[Apostol] p. 28Exercise 6qbtwnre 10749
[Apostol] p. 28Exercise 10(a)zneo 10316
[Apostol] p. 29Theorem I.35msqsqrd 12205  resqrth 12024  sqrth 12131  sqrthi 12137  sqsqrd 12204
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9967
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10506
[Apostol] p. 361Remarkcrreczi 11467
[Apostol] p. 363Remarkabsgt0i 12165
[Apostol] p. 363Exampleabssubd 12218  abssubi 12169
[Baer] p. 40Property (b)mapdord 32133
[Baer] p. 40Property (c)mapd11 32134
[Baer] p. 40Property (e)mapdin 32157  mapdlsm 32159
[Baer] p. 40Property (f)mapd0 32160
[Baer] p. 40Definition of projectivitydf-mapd 32120  mapd1o 32143
[Baer] p. 41Property (g)mapdat 32162
[Baer] p. 44Part (1)mapdpg 32201
[Baer] p. 45Part (2)hdmap1eq 32297  mapdheq 32223  mapdheq2 32224  mapdheq2biN 32225
[Baer] p. 45Part (3)baerlem3 32208
[Baer] p. 46Part (4)mapdheq4 32227  mapdheq4lem 32226
[Baer] p. 46Part (5)baerlem5a 32209  baerlem5abmN 32213  baerlem5amN 32211  baerlem5b 32210  baerlem5bmN 32212
[Baer] p. 47Part (6)hdmap1l6 32317  hdmap1l6a 32305  hdmap1l6e 32310  hdmap1l6f 32311  hdmap1l6g 32312  hdmap1l6lem1 32303  hdmap1l6lem2 32304  hdmap1p6N 32318  mapdh6N 32242  mapdh6aN 32230  mapdh6eN 32235  mapdh6fN 32236  mapdh6gN 32237  mapdh6lem1N 32228  mapdh6lem2N 32229
[Baer] p. 48Part 9hdmapval 32326
[Baer] p. 48Part 10hdmap10 32338
[Baer] p. 48Part 11hdmapadd 32341
[Baer] p. 48Part (6)hdmap1l6h 32313  mapdh6hN 32238
[Baer] p. 48Part (7)mapdh75cN 32248  mapdh75d 32249  mapdh75e 32247  mapdh75fN 32250  mapdh7cN 32244  mapdh7dN 32245  mapdh7eN 32243  mapdh7fN 32246
[Baer] p. 48Part (8)mapdh8 32284  mapdh8a 32270  mapdh8aa 32271  mapdh8ab 32272  mapdh8ac 32273  mapdh8ad 32274  mapdh8b 32275  mapdh8c 32276  mapdh8d 32278  mapdh8d0N 32277  mapdh8e 32279  mapdh8fN 32280  mapdh8g 32281  mapdh8i 32282  mapdh8j 32283
[Baer] p. 48Part (9)mapdh9a 32285
[Baer] p. 48Equation 10mapdhvmap 32264
[Baer] p. 49Part 12hdmap11 32346  hdmapeq0 32342  hdmapf1oN 32363  hdmapneg 32344  hdmaprnN 32362  hdmaprnlem1N 32347  hdmaprnlem3N 32348  hdmaprnlem3uN 32349  hdmaprnlem4N 32351  hdmaprnlem6N 32352  hdmaprnlem7N 32353  hdmaprnlem8N 32354  hdmaprnlem9N 32355  hdmapsub 32345
[Baer] p. 49Part 14hdmap14lem1 32366  hdmap14lem10 32375  hdmap14lem1a 32364  hdmap14lem2N 32367  hdmap14lem2a 32365  hdmap14lem3 32368  hdmap14lem8 32373  hdmap14lem9 32374
[Baer] p. 50Part 14hdmap14lem11 32376  hdmap14lem12 32377  hdmap14lem13 32378  hdmap14lem14 32379  hdmap14lem15 32380  hgmapval 32385
[Baer] p. 50Part 15hgmapadd 32392  hgmapmul 32393  hgmaprnlem2N 32395  hgmapvs 32389
[Baer] p. 50Part 16hgmaprnN 32399
[Baer] p. 110Lemma 1hdmapip0com 32415
[Baer] p. 110Line 27hdmapinvlem1 32416
[Baer] p. 110Line 28hdmapinvlem2 32417
[Baer] p. 110Line 30hdmapinvlem3 32418
[Baer] p. 110Part 1.2hdmapglem5 32420  hgmapvv 32424
[Baer] p. 110Proposition 1hdmapinvlem4 32419
[Baer] p. 111Line 10hgmapvvlem1 32421
[Baer] p. 111Line 15hdmapg 32428  hdmapglem7 32427
[BellMachover] p. 36Lemma 10.3id1 21
[BellMachover] p. 97Definition 10.1df-eu 2266
[BellMachover] p. 460Notationdf-mo 2267
[BellMachover] p. 460Definitionmo3 2293
[BellMachover] p. 461Axiom Extax-ext 2393
[BellMachover] p. 462Theorem 1.1bm1.1 2397
[BellMachover] p. 463Axiom Repaxrep5 4293
[BellMachover] p. 463Scheme Sepaxsep 4297
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4301
[BellMachover] p. 466Axiom Powaxpow3 4348
[BellMachover] p. 466Axiom Unionaxun2 4670
[BellMachover] p. 468Definitiondf-ord 4552
[BellMachover] p. 469Theorem 2.2(i)ordirr 4567
[BellMachover] p. 469Theorem 2.2(iii)onelon 4574
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4569
[BellMachover] p. 471Definition of Ndf-om 4813
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4753
[BellMachover] p. 471Definition of Limdf-lim 4554
[BellMachover] p. 472Axiom Infzfinf2 7561
[BellMachover] p. 473Theorem 2.8limom 4827
[BellMachover] p. 477Equation 3.1df-r1 7654
[BellMachover] p. 478Definitionrankval2 7708
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7672  r1ord3g 7669
[BellMachover] p. 480Axiom Regzfreg2 7528
[BellMachover] p. 488Axiom ACac5 8321  dfac4 7967
[BellMachover] p. 490Definition of alephalephval3 7955
[BeltramettiCassinelli] p. 98Remarkatlatmstc 29814
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 23817
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 23859  chirredi 23858
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 23847
[Beran] p. 3Definition of joinsshjval3 22817
[Beran] p. 39Theorem 2.3(i)cmcm2 23079  cmcm2i 23056  cmcm2ii 23061  cmt2N 29745
[Beran] p. 40Theorem 2.3(iii)lecm 23080  lecmi 23065  lecmii 23066
[Beran] p. 45Theorem 3.4cmcmlem 23054
[Beran] p. 49Theorem 4.2cm2j 23083  cm2ji 23088  cm2mi 23089
[Beran] p. 95Definitiondf-sh 22670  issh2 22672
[Beran] p. 95Lemma 3.1(S5)his5 22549
[Beran] p. 95Lemma 3.1(S6)his6 22562
[Beran] p. 95Lemma 3.1(S7)his7 22553
[Beran] p. 95Lemma 3.2(S8)ho01i 23292
[Beran] p. 95Lemma 3.2(S9)hoeq1 23294
[Beran] p. 95Lemma 3.2(S10)ho02i 23293
[Beran] p. 95Lemma 3.2(S11)hoeq2 23295
[Beran] p. 95Postulate (S1)ax-his1 22545  his1i 22563
[Beran] p. 95Postulate (S2)ax-his2 22546
[Beran] p. 95Postulate (S3)ax-his3 22547
[Beran] p. 95Postulate (S4)ax-his4 22548
[Beran] p. 96Definition of normdf-hnorm 22432  dfhnorm2 22585  normval 22587
[Beran] p. 96Definition for Cauchy sequencehcau 22647
[Beran] p. 96Definition of Cauchy sequencedf-hcau 22437
[Beran] p. 96Definition of complete subspaceisch3 22705
[Beran] p. 96Definition of convergedf-hlim 22436  hlimi 22651
[Beran] p. 97Theorem 3.3(i)norm-i-i 22596  norm-i 22592
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 22600  norm-ii 22601  normlem0 22572  normlem1 22573  normlem2 22574  normlem3 22575  normlem4 22576  normlem5 22577  normlem6 22578  normlem7 22579  normlem7tALT 22582
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 22602  norm-iii 22603
[Beran] p. 98Remark 3.4bcs 22644  bcsiALT 22642  bcsiHIL 22643
[Beran] p. 98Remark 3.4(B)normlem9at 22584  normpar 22618  normpari 22617
[Beran] p. 98Remark 3.4(C)normpyc 22609  normpyth 22608  normpythi 22605
[Beran] p. 99Remarklnfn0 23511  lnfn0i 23506  lnop0 23430  lnop0i 23434
[Beran] p. 99Theorem 3.5(i)nmcexi 23490  nmcfnex 23517  nmcfnexi 23515  nmcopex 23493  nmcopexi 23491
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 23518  nmcfnlbi 23516  nmcoplb 23494  nmcoplbi 23492
[Beran] p. 99Theorem 3.5(iii)lnfncon 23520  lnfnconi 23519  lnopcon 23499  lnopconi 23498
[Beran] p. 100Lemma 3.6normpar2i 22619
[Beran] p. 101Lemma 3.6norm3adifi 22616  norm3adifii 22611  norm3dif 22613  norm3difi 22610
[Beran] p. 102Theorem 3.7(i)chocunii 22764  pjhth 22856  pjhtheu 22857  pjpjhth 22888  pjpjhthi 22889  pjth 19301
[Beran] p. 102Theorem 3.7(ii)ococ 22869  ococi 22868
[Beran] p. 103Remark 3.8nlelchi 23525
[Beran] p. 104Theorem 3.9riesz3i 23526  riesz4 23528  riesz4i 23527
[Beran] p. 104Theorem 3.10cnlnadj 23543  cnlnadjeu 23542  cnlnadjeui 23541  cnlnadji 23540  cnlnadjlem1 23531  nmopadjlei 23552
[Beran] p. 106Theorem 3.11(i)adjeq0 23555
[Beran] p. 106Theorem 3.11(v)nmopadji 23554
[Beran] p. 106Theorem 3.11(ii)adjmul 23556
[Beran] p. 106Theorem 3.11(iv)adjadj 23400
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 23566  nmopcoadji 23565
[Beran] p. 106Theorem 3.11(iii)adjadd 23557
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 23567
[Beran] p. 106Theorem 3.11(viii)adjcoi 23564  pjadj2coi 23668  pjadjcoi 23625
[Beran] p. 107Definitiondf-ch 22685  isch2 22687
[Beran] p. 107Remark 3.12choccl 22769  isch3 22705  occl 22767  ocsh 22746  shoccl 22768  shocsh 22747
[Beran] p. 107Remark 3.12(B)ococin 22871
[Beran] p. 108Theorem 3.13chintcl 22795
[Beran] p. 109Property (i)pjadj2 23651  pjadj3 23652  pjadji 23148  pjadjii 23137
[Beran] p. 109Property (ii)pjidmco 23645  pjidmcoi 23641  pjidmi 23136
[Beran] p. 110Definition of projector orderingpjordi 23637
[Beran] p. 111Remarkho0val 23214  pjch1 23133
[Beran] p. 111Definitiondf-hfmul 23198  df-hfsum 23197  df-hodif 23196  df-homul 23195  df-hosum 23194
[Beran] p. 111Lemma 4.4(i)pjo 23134
[Beran] p. 111Lemma 4.4(ii)pjch 23157  pjchi 22895
[Beran] p. 111Lemma 4.4(iii)pjoc2 22902  pjoc2i 22901
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 23143
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 23629  pjssmii 23144
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 23628
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 23627
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 23632
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 23630  pjssge0ii 23145
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 23631  pjdifnormii 23146
[Bogachev] p. 116Definition 2.3.1df-itgm 24625  df-sitm 24607
[Bogachev] p. 118Chapter 2.4.4df-itgm 24625
[Bogachev] p. 118Definition 2.4.1df-sitg 24606
[Bollobas] p. 4Definitiondf-wlk 21477
[Bollobas] p. 5Notationdf-pth 21479
[Bollobas] p. 5Definitiondf-crct 21481  df-cycl 21482  df-trail 21478  df-wlkon 21483
[BourbakiEns] p. Proposition 8fcof1 5987  fcofo 5988
[BourbakiTop1] p. Remarkxnegmnf 10760  xnegpnf 10759
[BourbakiTop1] p. Remark rexneg 10761
[BourbakiTop1] p. Theoremneiss 17136
[BourbakiTop1] p. Remark 3ust0 18210  ustfilxp 18203
[BourbakiTop1] p. Axiom GT'tgpsubcn 18081
[BourbakiTop1] p. Example 1cstucnd 18275  iducn 18274  snfil 17857
[BourbakiTop1] p. Example 2neifil 17873
[BourbakiTop1] p. Theorem 1cnextcn 18059
[BourbakiTop1] p. Theorem 2ucnextcn 18295
[BourbakiTop1] p. Theorem 3df-hcmp 24302
[BourbakiTop1] p. Definitionistgp 18068
[BourbakiTop1] p. Propositioncnpco 17293  ishmeo 17752  neips 17140
[BourbakiTop1] p. Definition 1df-ucn 18267  df-ust 18191  filintn0 17854  ucnprima 18273
[BourbakiTop1] p. Definition 2df-cfilu 18278
[BourbakiTop1] p. Definition 3df-cusp 18289  df-usp 18248  df-utop 18222  trust 18220
[BourbakiTop1] p. Condition F_Iustssel 18196
[BourbakiTop1] p. Condition U_Iustdiag 18199
[BourbakiTop1] p. Property V_ivneiptopreu 17160
[BourbakiTop1] p. Proposition 1ucncn 18276  ustund 18212  ustuqtop 18237
[BourbakiTop1] p. Proposition 2neiptopreu 17160  utop2nei 18241  utop3cls 18242
[BourbakiTop1] p. Proposition 3fmucnd 18283  uspreg 18265  utopreg 18243
[BourbakiTop1] p. Proposition 4imasncld 17684  imasncls 17685  imasnopn 17683
[BourbakiTop1] p. Proposition 9cnpflf2 17993
[BourbakiTop1] p. Theorem 1 (d)iscncl 17295
[BourbakiTop1] p. Condition F_IIustincl 18198
[BourbakiTop1] p. Condition U_IIustinvel 18200
[BourbakiTop1] p. Proposition 11cnextucn 18294
[BourbakiTop1] p. Proposition Vissnei2 17143
[BourbakiTop1] p. Condition F_IIbustbasel 18197
[BourbakiTop1] p. Condition U_IIIustexhalf 18201
[BourbakiTop1] p. Definition C'''df-cmp 17412
[BourbakiTop1] p. Proposition Viiinnei 17152
[BourbakiTop1] p. Proposition Vivneissex 17154
[BourbakiTop1] p. Proposition Viiielnei 17138  ssnei 17137
[BourbakiTop1] p. Remark below def. 1filn0 17855
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17839
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17856
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27688  stoweid 27687
[BrosowskiDeutsh] p. 89Theorem for the non-trivial casestoweidlem62 27686
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27625  stoweidlem10 27634  stoweidlem14 27638  stoweidlem15 27639  stoweidlem35 27659  stoweidlem36 27660  stoweidlem37 27661  stoweidlem38 27662  stoweidlem40 27664  stoweidlem41 27665  stoweidlem43 27667  stoweidlem44 27668  stoweidlem46 27670  stoweidlem5 27629  stoweidlem50 27674  stoweidlem52 27676  stoweidlem53 27677  stoweidlem55 27679  stoweidlem56 27680
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27647  stoweidlem24 27648  stoweidlem27 27651  stoweidlem28 27652  stoweidlem30 27654
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27669  stoweidlem49 27673  stoweidlem7 27631
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27655  stoweidlem39 27663  stoweidlem42 27666  stoweidlem48 27672  stoweidlem51 27675  stoweidlem54 27678  stoweidlem57 27681  stoweidlem58 27682
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27649
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27658
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27641
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27683
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27684
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27642
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27635  stoweidlem26 27650
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27637
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27685
[ChoquetDD] p. 2Definition of mappingdf-mpt 4236
[Clemente] p. 10Definition ITnatded 21672
[Clemente] p. 10Definition I` `m,nnatded 21672
[Clemente] p. 11Definition E=>m,nnatded 21672
[Clemente] p. 11Definition I=>m,nnatded 21672
[Clemente] p. 11Definition E` `(1)natded 21672
[Clemente] p. 11Definition E` `(2)natded 21672
[Clemente] p. 12Definition E` `m,n,pnatded 21672
[Clemente] p. 12Definition I` `n(1)natded 21672
[Clemente] p. 12Definition I` `n(2)natded 21672
[Clemente] p. 13Definition I` `m,n,pnatded 21672
[Clemente] p. 14Definition E` `nnatded 21672
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 21674  ex-natded5.2 21673
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 21677  ex-natded5.3 21676
[Clemente] p. 18Theorem 5.5ex-natded5.5 21679
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 21681  ex-natded5.7 21680
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 21683  ex-natded5.8 21682
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 21685  ex-natded5.13 21684
[Clemente] p. 32Definition I` `nnatded 21672
[Clemente] p. 32Definition E` `m,n,p,anatded 21672
[Clemente] p. 32Definition E` `n,tnatded 21672
[Clemente] p. 32Definition I` `n,tnatded 21672
[Clemente] p. 43Theorem 9.20ex-natded9.20 21686
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 21687
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 21689  ex-natded9.26 21688
[Cohen] p. 301Remarkrelogoprlem 20446
[Cohen] p. 301Property 2relogmul 20447  relogmuld 20481
[Cohen] p. 301Property 3relogdiv 20448  relogdivd 20482
[Cohen] p. 301Property 4relogexp 20451
[Cohen] p. 301Property 1alog1 20441
[Cohen] p. 301Property 1bloge 20442
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 24596  sxbrsigalem4 24598
[Cohn] p. 81Section II.5acsdomd 14570  acsinfd 14569  acsinfdimd 14571  acsmap2d 14568  acsmapd 14567
[Cohn] p. 143Example 5.1.1sxbrsiga 24601
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 11205
[Crawley] p. 1Definition of posetdf-poset 14366
[Crawley] p. 107Theorem 13.2hlsupr 29880
[Crawley] p. 110Theorem 13.3arglem1N 30684  dalaw 30380
[Crawley] p. 111Theorem 13.4hlathil 32459
[Crawley] p. 111Definition of set Wdf-watsN 30484
[Crawley] p. 111Definition of dilationdf-dilN 30600  df-ldil 30598  isldil 30604
[Crawley] p. 111Definition of translationdf-ltrn 30599  df-trnN 30601  isltrn 30613  ltrnu 30615
[Crawley] p. 112Lemma Acdlema1N 30285  cdlema2N 30286  exatleN 29898
[Crawley] p. 112Lemma B1cvrat 29970  cdlemb 30288  cdlemb2 30535  cdlemb3 31100  idltrn 30644  l1cvat 29550  lhpat 30537  lhpat2 30539  lshpat 29551  ltrnel 30633  ltrnmw 30645
[Crawley] p. 112Lemma Ccdlemc1 30685  cdlemc2 30686  ltrnnidn 30668  trlat 30663  trljat1 30660  trljat2 30661  trljat3 30662  trlne 30679  trlnidat 30667  trlnle 30680
[Crawley] p. 112Definition of automorphismdf-pautN 30485
[Crawley] p. 113Lemma Ccdlemc 30691  cdlemc3 30687  cdlemc4 30688
[Crawley] p. 113Lemma Dcdlemd 30701  cdlemd1 30692  cdlemd2 30693  cdlemd3 30694  cdlemd4 30695  cdlemd5 30696  cdlemd6 30697  cdlemd7 30698  cdlemd8 30699  cdlemd9 30700  cdleme31sde 30879  cdleme31se 30876  cdleme31se2 30877  cdleme31snd 30880  cdleme32a 30935  cdleme32b 30936  cdleme32c 30937  cdleme32d 30938  cdleme32e 30939  cdleme32f 30940  cdleme32fva 30931  cdleme32fva1 30932  cdleme32fvcl 30934  cdleme32le 30941  cdleme48fv 30993  cdleme4gfv 31001  cdleme50eq 31035  cdleme50f 31036  cdleme50f1 31037  cdleme50f1o 31040  cdleme50laut 31041  cdleme50ldil 31042  cdleme50lebi 31034  cdleme50rn 31039  cdleme50rnlem 31038  cdlemeg49le 31005  cdlemeg49lebilem 31033
[Crawley] p. 113Lemma Ecdleme 31054  cdleme00a 30703  cdleme01N 30715  cdleme02N 30716  cdleme0a 30705  cdleme0aa 30704  cdleme0b 30706  cdleme0c 30707  cdleme0cp 30708  cdleme0cq 30709  cdleme0dN 30710  cdleme0e 30711  cdleme0ex1N 30717  cdleme0ex2N 30718  cdleme0fN 30712  cdleme0gN 30713  cdleme0moN 30719  cdleme1 30721  cdleme10 30748  cdleme10tN 30752  cdleme11 30764  cdleme11a 30754  cdleme11c 30755  cdleme11dN 30756  cdleme11e 30757  cdleme11fN 30758  cdleme11g 30759  cdleme11h 30760  cdleme11j 30761  cdleme11k 30762  cdleme11l 30763  cdleme12 30765  cdleme13 30766  cdleme14 30767  cdleme15 30772  cdleme15a 30768  cdleme15b 30769  cdleme15c 30770  cdleme15d 30771  cdleme16 30779  cdleme16aN 30753  cdleme16b 30773  cdleme16c 30774  cdleme16d 30775  cdleme16e 30776  cdleme16f 30777  cdleme16g 30778  cdleme19a 30797  cdleme19b 30798  cdleme19c 30799  cdleme19d 30800  cdleme19e 30801  cdleme19f 30802  cdleme1b 30720  cdleme2 30722  cdleme20aN 30803  cdleme20bN 30804  cdleme20c 30805  cdleme20d 30806  cdleme20e 30807  cdleme20f 30808  cdleme20g 30809  cdleme20h 30810  cdleme20i 30811  cdleme20j 30812  cdleme20k 30813  cdleme20l 30816  cdleme20l1 30814  cdleme20l2 30815  cdleme20m 30817  cdleme20y 30796  cdleme20zN 30795  cdleme21 30831  cdleme21d 30824  cdleme21e 30825  cdleme22a 30834  cdleme22aa 30833  cdleme22b 30835  cdleme22cN 30836  cdleme22d 30837  cdleme22e 30838  cdleme22eALTN 30839  cdleme22f 30840  cdleme22f2 30841  cdleme22g 30842  cdleme23a 30843  cdleme23b 30844  cdleme23c 30845  cdleme26e 30853  cdleme26eALTN 30855  cdleme26ee 30854  cdleme26f 30857  cdleme26f2 30859  cdleme26f2ALTN 30858  cdleme26fALTN 30856  cdleme27N 30863  cdleme27a 30861  cdleme27cl 30860  cdleme28c 30866  cdleme3 30731  cdleme30a 30872  cdleme31fv 30884  cdleme31fv1 30885  cdleme31fv1s 30886  cdleme31fv2 30887  cdleme31id 30888  cdleme31sc 30878  cdleme31sdnN 30881  cdleme31sn 30874  cdleme31sn1 30875  cdleme31sn1c 30882  cdleme31sn2 30883  cdleme31so 30873  cdleme35a 30942  cdleme35b 30944  cdleme35c 30945  cdleme35d 30946  cdleme35e 30947  cdleme35f 30948  cdleme35fnpq 30943  cdleme35g 30949  cdleme35h 30950  cdleme35h2 30951  cdleme35sn2aw 30952  cdleme35sn3a 30953  cdleme36a 30954  cdleme36m 30955  cdleme37m 30956  cdleme38m 30957  cdleme38n 30958  cdleme39a 30959  cdleme39n 30960  cdleme3b 30723  cdleme3c 30724  cdleme3d 30725  cdleme3e 30726  cdleme3fN 30727  cdleme3fa 30730  cdleme3g 30728  cdleme3h 30729  cdleme4 30732  cdleme40m 30961  cdleme40n 30962  cdleme40v 30963  cdleme40w 30964  cdleme41fva11 30971  cdleme41sn3aw 30968  cdleme41sn4aw 30969  cdleme41snaw 30970  cdleme42a 30965  cdleme42b 30972  cdleme42c 30966  cdleme42d 30967  cdleme42e 30973  cdleme42f 30974  cdleme42g 30975  cdleme42h 30976  cdleme42i 30977  cdleme42k 30978  cdleme42ke 30979  cdleme42keg 30980  cdleme42mN 30981  cdleme42mgN 30982  cdleme43aN 30983  cdleme43bN 30984  cdleme43cN 30985  cdleme43dN 30986  cdleme5 30734  cdleme50ex 31053  cdleme50ltrn 31051  cdleme51finvN 31050  cdleme51finvfvN 31049  cdleme51finvtrN 31052  cdleme6 30735  cdleme7 30743  cdleme7a 30737  cdleme7aa 30736  cdleme7b 30738  cdleme7c 30739  cdleme7d 30740  cdleme7e 30741  cdleme7ga 30742  cdleme8 30744  cdleme8tN 30749  cdleme9 30747  cdleme9a 30745  cdleme9b 30746  cdleme9tN 30751  cdleme9taN 30750  cdlemeda 30792  cdlemedb 30791  cdlemednpq 30793  cdlemednuN 30794  cdlemefr27cl 30897  cdlemefr32fva1 30904  cdlemefr32fvaN 30903  cdlemefrs32fva 30894  cdlemefrs32fva1 30895  cdlemefs27cl 30907  cdlemefs32fva1 30917  cdlemefs32fvaN 30916  cdlemesner 30790  cdlemeulpq 30714
[Crawley] p. 114Lemma E4atex 30570  4atexlem7 30569  cdleme0nex 30784  cdleme17a 30780  cdleme17c 30782  cdleme17d 30992  cdleme17d1 30783  cdleme17d2 30989  cdleme18a 30785  cdleme18b 30786  cdleme18c 30787  cdleme18d 30789  cdleme4a 30733
[Crawley] p. 115Lemma Ecdleme21a 30819  cdleme21at 30822  cdleme21b 30820  cdleme21c 30821  cdleme21ct 30823  cdleme21f 30826  cdleme21g 30827  cdleme21h 30828  cdleme21i 30829  cdleme22gb 30788
[Crawley] p. 116Lemma Fcdlemf 31057  cdlemf1 31055  cdlemf2 31056
[Crawley] p. 116Lemma Gcdlemftr1 31061  cdlemg16 31151  cdlemg28 31198  cdlemg28a 31187  cdlemg28b 31197  cdlemg3a 31091  cdlemg42 31223  cdlemg43 31224  cdlemg44 31227  cdlemg44a 31225  cdlemg46 31229  cdlemg47 31230  cdlemg9 31128  ltrnco 31213  ltrncom 31232  tgrpabl 31245  trlco 31221
[Crawley] p. 116Definition of Gdf-tgrp 31237
[Crawley] p. 117Lemma Gcdlemg17 31171  cdlemg17b 31156
[Crawley] p. 117Definition of Edf-edring-rN 31250  df-edring 31251
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 31254
[Crawley] p. 118Remarktendopltp 31274
[Crawley] p. 118Lemma Hcdlemh 31311  cdlemh1 31309  cdlemh2 31310
[Crawley] p. 118Lemma Icdlemi 31314  cdlemi1 31312  cdlemi2 31313
[Crawley] p. 118Lemma Jcdlemj1 31315  cdlemj2 31316  cdlemj3 31317  tendocan 31318
[Crawley] p. 118Lemma Kcdlemk 31468  cdlemk1 31325  cdlemk10 31337  cdlemk11 31343  cdlemk11t 31440  cdlemk11ta 31423  cdlemk11tb 31425  cdlemk11tc 31439  cdlemk11u-2N 31383  cdlemk11u 31365  cdlemk12 31344  cdlemk12u-2N 31384  cdlemk12u 31366  cdlemk13-2N 31370  cdlemk13 31346  cdlemk14-2N 31372  cdlemk14 31348  cdlemk15-2N 31373  cdlemk15 31349  cdlemk16-2N 31374  cdlemk16 31351  cdlemk16a 31350  cdlemk17-2N 31375  cdlemk17 31352  cdlemk18-2N 31380  cdlemk18-3N 31394  cdlemk18 31362  cdlemk19-2N 31381  cdlemk19 31363  cdlemk19u 31464  cdlemk1u 31353  cdlemk2 31326  cdlemk20-2N 31386  cdlemk20 31368  cdlemk21-2N 31385  cdlemk21N 31367  cdlemk22-3 31395  cdlemk22 31387  cdlemk23-3 31396  cdlemk24-3 31397  cdlemk25-3 31398  cdlemk26-3 31400  cdlemk26b-3 31399  cdlemk27-3 31401  cdlemk28-3 31402  cdlemk29-3 31405  cdlemk3 31327  cdlemk30 31388  cdlemk31 31390  cdlemk32 31391  cdlemk33N 31403  cdlemk34 31404  cdlemk35 31406  cdlemk36 31407  cdlemk37 31408  cdlemk38 31409  cdlemk39 31410  cdlemk39u 31462  cdlemk4 31328  cdlemk41 31414  cdlemk42 31435  cdlemk42yN 31438  cdlemk43N 31457  cdlemk45 31441  cdlemk46 31442  cdlemk47 31443  cdlemk48 31444  cdlemk49 31445  cdlemk5 31330  cdlemk50 31446  cdlemk51 31447  cdlemk52 31448  cdlemk53 31451  cdlemk54 31452  cdlemk55 31455  cdlemk55u 31460  cdlemk56 31465  cdlemk5a 31329  cdlemk5auN 31354  cdlemk5u 31355  cdlemk6 31331  cdlemk6u 31356  cdlemk7 31342  cdlemk7u-2N 31382  cdlemk7u 31364  cdlemk8 31332  cdlemk9 31333  cdlemk9bN 31334  cdlemki 31335  cdlemkid 31430  cdlemkj-2N 31376  cdlemkj 31357  cdlemksat 31340  cdlemksel 31339  cdlemksv 31338  cdlemksv2 31341  cdlemkuat 31360  cdlemkuel-2N 31378  cdlemkuel-3 31392  cdlemkuel 31359  cdlemkuv-2N 31377  cdlemkuv2-2 31379  cdlemkuv2-3N 31393  cdlemkuv2 31361  cdlemkuvN 31358  cdlemkvcl 31336  cdlemky 31420  cdlemkyyN 31456  tendoex 31469
[Crawley] p. 120Remarkdva1dim 31479
[Crawley] p. 120Lemma Lcdleml1N 31470  cdleml2N 31471  cdleml3N 31472  cdleml4N 31473  cdleml5N 31474  cdleml6 31475  cdleml7 31476  cdleml8 31477  cdleml9 31478  dia1dim 31556
[Crawley] p. 120Lemma Mdia11N 31543  diaf11N 31544  dialss 31541  diaord 31542  dibf11N 31656  djajN 31632
[Crawley] p. 120Definition of isomorphism mapdiaval 31527
[Crawley] p. 121Lemma Mcdlemm10N 31613  dia2dimlem1 31559  dia2dimlem2 31560  dia2dimlem3 31561  dia2dimlem4 31562  dia2dimlem5 31563  diaf1oN 31625  diarnN 31624  dvheveccl 31607  dvhopN 31611
[Crawley] p. 121Lemma Ncdlemn 31707  cdlemn10 31701  cdlemn11 31706  cdlemn11a 31702  cdlemn11b 31703  cdlemn11c 31704  cdlemn11pre 31705  cdlemn2 31690  cdlemn2a 31691  cdlemn3 31692  cdlemn4 31693  cdlemn4a 31694  cdlemn5 31696  cdlemn5pre 31695  cdlemn6 31697  cdlemn7 31698  cdlemn8 31699  cdlemn9 31700  diclspsn 31689
[Crawley] p. 121Definition of phi(q)df-dic 31668
[Crawley] p. 122Lemma Ndih11 31760  dihf11 31762  dihjust 31712  dihjustlem 31711  dihord 31759  dihord1 31713  dihord10 31718  dihord11b 31717  dihord11c 31719  dihord2 31722  dihord2a 31714  dihord2b 31715  dihord2cN 31716  dihord2pre 31720  dihord2pre2 31721  dihordlem6 31708  dihordlem7 31709  dihordlem7b 31710
[Crawley] p. 122Definition of isomorphism mapdihffval 31725  dihfval 31726  dihval 31727
[Eisenberg] p. 67Definition 5.3df-dif 3291
[Eisenberg] p. 82Definition 6.3dfom3 7566
[Eisenberg] p. 125Definition 8.21df-map 6987
[Eisenberg] p. 216Example 13.2(4)omenps 7573
[Eisenberg] p. 310Theorem 19.8cardprc 7831
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8394
[Enderton] p. 18Axiom of Empty Setaxnul 4305
[Enderton] p. 19Definitiondf-tp 3790
[Enderton] p. 26Exercise 5unissb 4013
[Enderton] p. 26Exercise 10pwel 4383
[Enderton] p. 28Exercise 7(b)pwun 4459
[Enderton] p. 30Theorem "Distributive laws"iinin1 4130  iinin2 4129  iinun2 4125  iunin1 4124  iunin2 4123
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4128  iundif2 4126
[Enderton] p. 32Exercise 20unineq 3559
[Enderton] p. 33Exercise 23iinuni 4142
[Enderton] p. 33Exercise 25iununi 4143
[Enderton] p. 33Exercise 24(a)iinpw 4147
[Enderton] p. 33Exercise 24(b)iunpw 4726  iunpwss 4148
[Enderton] p. 36Definitionopthwiener 4426
[Enderton] p. 38Exercise 6(a)unipw 4382
[Enderton] p. 38Exercise 6(b)pwuni 4363
[Enderton] p. 41Lemma 3Dopeluu 4682  rnex 5100  rnexg 5098
[Enderton] p. 41Exercise 8dmuni 5046  rnuni 5250
[Enderton] p. 42Definition of a functiondffun7 5446  dffun8 5447
[Enderton] p. 43Definition of function valuefunfv2 5758
[Enderton] p. 43Definition of single-rootedfuncnv 5478
[Enderton] p. 44Definition (d)dfima2 5172  dfima3 5173
[Enderton] p. 47Theorem 3Hfvco2 5765
[Enderton] p. 49Axiom of Choice (first form)ac7 8317  ac7g 8318  df-ac 7961  dfac2 7975  dfac2a 7974  dfac3 7966  dfac7 7976
[Enderton] p. 50Theorem 3K(a)imauni 5960
[Enderton] p. 52Definitiondf-map 6987
[Enderton] p. 53Exercise 21coass 5355
[Enderton] p. 53Exercise 27dmco 5345
[Enderton] p. 53Exercise 14(a)funin 5487
[Enderton] p. 53Exercise 22(a)imass2 5207
[Enderton] p. 54Remarkixpf 7051  ixpssmap 7063
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7031
[Enderton] p. 55Axiom of Choice (second form)ac9 8327  ac9s 8337
[Enderton] p. 56Theorem 3Merref 6892
[Enderton] p. 57Lemma 3Nerthi 6918
[Enderton] p. 57Definitiondf-ec 6874
[Enderton] p. 58Definitiondf-qs 6878
[Enderton] p. 60Theorem 3Qth3q 6980  th3qcor 6979  th3qlem1 6977  th3qlem2 6978
[Enderton] p. 61Exercise 35df-ec 6874
[Enderton] p. 65Exercise 56(a)dmun 5043
[Enderton] p. 68Definition of successordf-suc 4555
[Enderton] p. 71Definitiondf-tr 4271  dftr4 4275
[Enderton] p. 72Theorem 4Eunisuc 4625
[Enderton] p. 73Exercise 6unisuc 4625
[Enderton] p. 73Exercise 5(a)truni 4284
[Enderton] p. 73Exercise 5(b)trint 4285  trintALT 28711
[Enderton] p. 79Theorem 4I(A1)nna0 6814
[Enderton] p. 79Theorem 4I(A2)nnasuc 6816  onasuc 6739
[Enderton] p. 79Definition of operation valuedf-ov 6051
[Enderton] p. 80Theorem 4J(A1)nnm0 6815
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6817  onmsuc 6740
[Enderton] p. 81Theorem 4K(1)nnaass 6832
[Enderton] p. 81Theorem 4K(2)nna0r 6819  nnacom 6827
[Enderton] p. 81Theorem 4K(3)nndi 6833
[Enderton] p. 81Theorem 4K(4)nnmass 6834
[Enderton] p. 81Theorem 4K(5)nnmcom 6836
[Enderton] p. 82Exercise 16nnm0r 6820  nnmsucr 6835
[Enderton] p. 88Exercise 23nnaordex 6848
[Enderton] p. 129Definitiondf-en 7077
[Enderton] p. 132Theorem 6B(b)canth 6506
[Enderton] p. 133Exercise 1xpomen 7861
[Enderton] p. 133Exercise 2qnnen 12776
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7258
[Enderton] p. 135Corollary 6Cphp3 7260
[Enderton] p. 136Corollary 6Enneneq 7257
[Enderton] p. 136Corollary 6D(a)pssinf 7286
[Enderton] p. 136Corollary 6D(b)ominf 7288
[Enderton] p. 137Lemma 6Fpssnn 7294
[Enderton] p. 138Corollary 6Gssfi 7296
[Enderton] p. 139Theorem 6H(c)mapen 7238
[Enderton] p. 142Theorem 6I(3)xpcdaen 8027
[Enderton] p. 142Theorem 6I(4)mapcdaen 8028
[Enderton] p. 143Theorem 6Jcda0en 8023  cda1en 8019
[Enderton] p. 144Exercise 13iunfi 7361  unifi 7362  unifi2 7363
[Enderton] p. 144Corollary 6Kundif2 3672  unfi 7341  unfi2 7343
[Enderton] p. 145Figure 38ffoss 5674
[Enderton] p. 145Definitiondf-dom 7078
[Enderton] p. 146Example 1domen 7088  domeng 7089
[Enderton] p. 146Example 3nndomo 7267  nnsdom 7572  nnsdomg 7333
[Enderton] p. 149Theorem 6L(a)cdadom2 8031
[Enderton] p. 149Theorem 6L(c)mapdom1 7239  xpdom1 7174  xpdom1g 7172  xpdom2g 7171
[Enderton] p. 149Theorem 6L(d)mapdom2 7245
[Enderton] p. 151Theorem 6Mzorn 8351  zorng 8348
[Enderton] p. 151Theorem 6M(4)ac8 8336  dfac5 7973
[Enderton] p. 159Theorem 6Qunictb 8414
[Enderton] p. 164Exampleinfdif 8053
[Enderton] p. 168Definitiondf-po 4471
[Enderton] p. 192Theorem 7M(a)oneli 4656
[Enderton] p. 192Theorem 7M(b)ontr1 4595
[Enderton] p. 192Theorem 7M(c)onirri 4655
[Enderton] p. 193Corollary 7N(b)0elon 4602
[Enderton] p. 193Corollary 7N(c)onsuci 4785
[Enderton] p. 193Corollary 7N(d)ssonunii 4735
[Enderton] p. 194Remarkonprc 4732
[Enderton] p. 194Exercise 16suc11 4652
[Enderton] p. 197Definitiondf-card 7790
[Enderton] p. 197Theorem 7Pcarden 8390
[Enderton] p. 200Exercise 25tfis 4801
[Enderton] p. 202Lemma 7Tr1tr 7666
[Enderton] p. 202Definitiondf-r1 7654
[Enderton] p. 202Theorem 7Qr1val1 7676
[Enderton] p. 204Theorem 7V(b)rankval4 7757
[Enderton] p. 206Theorem 7X(b)en2lp 7535
[Enderton] p. 207Exercise 30rankpr 7747  rankprb 7741  rankpw 7733  rankpwi 7713  rankuniss 7756
[Enderton] p. 207Exercise 34opthreg 7537
[Enderton] p. 208Exercise 35suc11reg 7538
[Enderton] p. 212Definition of alephalephval3 7955
[Enderton] p. 213Theorem 8A(a)alephord2 7921
[Enderton] p. 213Theorem 8A(b)cardalephex 7935
[Enderton] p. 218Theorem Schema 8Eonfununi 6570
[Enderton] p. 222Definition of kardkarden 7783  kardex 7782
[Enderton] p. 238Theorem 8Roeoa 6807
[Enderton] p. 238Theorem 8Soeoe 6809
[Enderton] p. 240Exercise 25oarec 6772
[Enderton] p. 257Definition of cofinalitycflm 8094
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13830
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13776
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14566  mrieqv2d 13827  mrieqvd 13826
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13831
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13836  mreexexlem2d 13833
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14572  mreexfidimd 13838
[Fremlin5] p. 193Proposition 563Gbnulmbl2 19392
[Fremlin5] p. 213Lemma 565Cauniioovol 19432
[Fremlin5] p. 214Lemma 565Cauniioombl 19442
[FreydScedrov] p. 283Axiom of Infinityax-inf 7557  inf1 7541  inf2 7542
[Gleason] p. 117Proposition 9-2.1df-enq 8752  enqer 8762
[Gleason] p. 117Proposition 9-2.2df-1nq 8757  df-nq 8753
[Gleason] p. 117Proposition 9-2.3df-plpq 8749  df-plq 8755
[Gleason] p. 119Proposition 9-2.4caovmo 6251  df-mpq 8750  df-mq 8756
[Gleason] p. 119Proposition 9-2.5df-rq 8758
[Gleason] p. 119Proposition 9-2.6ltexnq 8816
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8817  ltbtwnnq 8819
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8812
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8813
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8820
[Gleason] p. 121Definition 9-3.1df-np 8822
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8834
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8836
[Gleason] p. 122Definitiondf-1p 8823
[Gleason] p. 122Remark (1)prub 8835
[Gleason] p. 122Lemma 9-3.4prlem934 8874
[Gleason] p. 122Proposition 9-3.2df-ltp 8826
[Gleason] p. 122Proposition 9-3.3ltsopr 8873  psslinpr 8872  supexpr 8895  suplem1pr 8893  suplem2pr 8894
[Gleason] p. 123Proposition 9-3.5addclpr 8859  addclprlem1 8857  addclprlem2 8858  df-plp 8824
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8863
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8862
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8875
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8884  ltexprlem1 8877  ltexprlem2 8878  ltexprlem3 8879  ltexprlem4 8880  ltexprlem5 8881  ltexprlem6 8882  ltexprlem7 8883
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8886  ltaprlem 8885
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8887
[Gleason] p. 124Lemma 9-3.6prlem936 8888
[Gleason] p. 124Proposition 9-3.7df-mp 8825  mulclpr 8861  mulclprlem 8860  reclem2pr 8889
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8870
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8865
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8864
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8869
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8892  reclem3pr 8890  reclem4pr 8891
[Gleason] p. 126Proposition 9-4.1df-enr 8898  df-mpr 8897  df-plpr 8896  enrer 8907
[Gleason] p. 126Proposition 9-4.2df-0r 8903  df-1r 8904  df-nr 8899
[Gleason] p. 126Proposition 9-4.3df-mr 8901  df-plr 8900  negexsr 8941  recexsr 8946  recexsrlem 8942
[Gleason] p. 127Proposition 9-4.4df-ltr 8902
[Gleason] p. 130Proposition 10-1.3creui 9959  creur 9958  cru 9956
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 9027  axcnre 9003
[Gleason] p. 132Definition 10-3.1crim 11883  crimd 12000  crimi 11961  crre 11882  crred 11999  crrei 11960
[Gleason] p. 132Definition 10-3.2remim 11885  remimd 11966
[Gleason] p. 133Definition 10.36absval2 12052  absval2d 12210  absval2i 12163
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11909  cjaddd 11988  cjaddi 11956
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11910  cjmuld 11989  cjmuli 11957
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11908  cjcjd 11967  cjcji 11939
[Gleason] p. 133Proposition 10-3.4(f)cjre 11907  cjreb 11891  cjrebd 11970  cjrebi 11942  cjred 11994  rere 11890  rereb 11888  rerebd 11969  rerebi 11941  rered 11992
[Gleason] p. 133Proposition 10-3.4(h)addcj 11916  addcjd 11980  addcji 11951
[Gleason] p. 133Proposition 10-3.7(a)absval 12006
[Gleason] p. 133Proposition 10-3.7(b)abscj 12047  abscjd 12215  abscji 12167
[Gleason] p. 133Proposition 10-3.7(c)abs00 12057  abs00d 12211  abs00i 12164  absne0d 12212
[Gleason] p. 133Proposition 10-3.7(d)releabs 12088  releabsd 12216  releabsi 12168
[Gleason] p. 133Proposition 10-3.7(f)absmul 12062  absmuld 12219  absmuli 12170
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 12050  sqabsaddi 12171
[Gleason] p. 133Proposition 10-3.7(h)abstri 12097  abstrid 12221  abstrii 12174
[Gleason] p. 134Definition 10-4.1df-exp 11346  exp0 11349  expp1 11351  expp1d 11487
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20531  cxpaddd 20569  expadd 11385  expaddd 11488  expaddz 11387
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20540  cxpmuld 20586  expmul 11388  expmuld 11489  expmulz 11389
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20537  mulcxpd 20580  mulexp 11382  mulexpd 11501  mulexpz 11383
[Gleason] p. 140Exercise 1znnen 12775
[Gleason] p. 141Definition 11-2.1fzval 11009
[Gleason] p. 168Proposition 12-2.1(a)climadd 12388  rlimadd 12399  rlimdiv 12402
[Gleason] p. 168Proposition 12-2.1(b)climsub 12390  rlimsub 12400
[Gleason] p. 168Proposition 12-2.1(c)climmul 12389  rlimmul 12401
[Gleason] p. 171Corollary 12-2.2climmulc2 12393
[Gleason] p. 172Corollary 12-2.5climrecl 12340
[Gleason] p. 172Proposition 12-2.4(c)climabs 12360  climcj 12361  climim 12363  climre 12362  rlimabs 12365  rlimcj 12366  rlimim 12368  rlimre 12367
[Gleason] p. 173Definition 12-3.1df-ltxr 9089  df-xr 9088  ltxr 10679
[Gleason] p. 175Definition 12-4.1df-limsup 12228  limsupval 12231
[Gleason] p. 180Theorem 12-5.1climsup 12426
[Gleason] p. 180Theorem 12-5.3caucvg 12435  caucvgb 12436  caucvgr 12432  climcau 12427
[Gleason] p. 182Exercise 3cvgcmp 12558
[Gleason] p. 182Exercise 4cvgrat 12623
[Gleason] p. 195Theorem 13-2.12abs1m 12102
[Gleason] p. 217Lemma 13-4.1btwnzge0 11193
[Gleason] p. 223Definition 14-1.1df-met 16659
[Gleason] p. 223Definition 14-1.1(a)met0 18334  xmet0 18333
[Gleason] p. 223Definition 14-1.1(b)metgt0 18350
[Gleason] p. 223Definition 14-1.1(c)metsym 18341
[Gleason] p. 223Definition 14-1.1(d)mettri 18343  mstri 18460  xmettri 18342  xmstri 18459
[Gleason] p. 225Definition 14-1.5xpsmet 18373
[Gleason] p. 230Proposition 14-2.6txlm 17641
[Gleason] p. 240Theorem 14-4.3metcnp4 19223
[Gleason] p. 240Proposition 14-4.2metcnp3 18531
[Gleason] p. 243Proposition 14-4.16addcn 18856  addcn2 12350  mulcn 18858  mulcn2 12352  subcn 18857  subcn2 12351
[Gleason] p. 295Remarkbcval3 11560  bcval4 11561
[Gleason] p. 295Equation 2bcpasc 11575
[Gleason] p. 295Definition of binomial coefficientbcval 11558  df-bc 11557
[Gleason] p. 296Remarkbcn0 11564  bcnn 11566
[Gleason] p. 296Theorem 15-2.8binom 12572
[Gleason] p. 308Equation 2ef0 12656
[Gleason] p. 308Equation 3efcj 12657
[Gleason] p. 309Corollary 15-4.3efne0 12661
[Gleason] p. 309Corollary 15-4.4efexp 12665
[Gleason] p. 310Equation 14sinadd 12728
[Gleason] p. 310Equation 15cosadd 12729
[Gleason] p. 311Equation 17sincossq 12740
[Gleason] p. 311Equation 18cosbnd 12745  sinbnd 12744
[Gleason] p. 311Lemma 15-4.7sqeqor 11458  sqeqori 11456
[Gleason] p. 311Definition of pidf-pi 12638
[Godowski] p. 730Equation SFgoeqi 23737
[GodowskiGreechie] p. 249Equation IV3oai 23131
[Gratzer] p. 23Section 0.6df-mre 13774
[Gratzer] p. 27Section 0.6df-mri 13776
[Halmos] p. 31Theorem 17.3riesz1 23529  riesz2 23530
[Halmos] p. 41Definition of Hermitianhmopadj2 23405
[Halmos] p. 42Definition of projector orderingpjordi 23637
[Halmos] p. 43Theorem 26.1elpjhmop 23649  elpjidm 23648  pjnmopi 23612
[Halmos] p. 44Remarkpjinormi 23150  pjinormii 23139
[Halmos] p. 44Theorem 26.2elpjch 23653  pjrn 23170  pjrni 23165  pjvec 23159
[Halmos] p. 44Theorem 26.3pjnorm2 23190
[Halmos] p. 44Theorem 26.4hmopidmpj 23618  hmopidmpji 23616
[Halmos] p. 45Theorem 27.1pjinvari 23655
[Halmos] p. 45Theorem 27.3pjoci 23644  pjocvec 23160
[Halmos] p. 45Theorem 27.4pjorthcoi 23633
[Halmos] p. 48Theorem 29.2pjssposi 23636
[Halmos] p. 48Theorem 29.3pjssdif1i 23639  pjssdif2i 23638
[Halmos] p. 50Definition of spectrumdf-spec 23319
[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 18978  df-phtpy 18957
[Hatcher] p. 26Definitiondf-pco 18991  df-pi1 18994
[Hatcher] p. 26Proposition 1.2phtpcer 18981
[Hatcher] p. 26Proposition 1.3pi1grp 19036
[Herstein] p. 54Exercise 28df-grpo 21740
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14784  grpoideu 21758  mndideu 14661
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14802  grpoinveu 21771
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14821  grpo2inv 21788
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14830  grpoinvop 21790
[Herstein] p. 57Exercise 1isgrp2d 21784  isgrp2i 21785
[Hitchcock] p. 5Rule A3mpto1 1539
[Hitchcock] p. 5Rule A4mpto2 1540
[Hitchcock] p. 5Rule A5mtp-xor 1542
[Holland] p. 1519Theorem 2sumdmdi 23884
[Holland] p. 1520Lemma 5cdj1i 23897  cdj3i 23905  cdj3lem1 23898  cdjreui 23896
[Holland] p. 1524Lemma 7mddmdin0i 23895
[Holland95] p. 13Theorem 3.6hlathil 32459
[Holland95] p. 14Line 15hgmapvs 32389
[Holland95] p. 14Line 16hdmaplkr 32411
[Holland95] p. 14Line 17hdmapellkr 32412
[Holland95] p. 14Line 19hdmapglnm2 32409
[Holland95] p. 14Line 20hdmapip0com 32415
[Holland95] p. 14Theorem 3.6hdmapevec2 32334
[Holland95] p. 14Lines 24 and 25hdmapoc 32429
[Holland95] p. 204Definition of involutiondf-srng 15897
[Holland95] p. 212Definition of subspacedf-psubsp 29997
[Holland95] p. 214Lemma 3.3lclkrlem2v 32023
[Holland95] p. 214Definition 3.2df-lpolN 31976
[Holland95] p. 214Definition of nonsingularpnonsingN 30427
[Holland95] p. 215Lemma 3.3(1)dihoml4 31872  poml4N 30447
[Holland95] p. 215Lemma 3.3(2)dochexmid 31963  pexmidALTN 30472  pexmidN 30463
[Holland95] p. 218Theorem 3.6lclkr 32028
[Holland95] p. 218Definition of dual vector spacedf-ldual 29619  ldualset 29620
[Holland95] p. 222Item 1df-lines 29995  df-pointsN 29996
[Holland95] p. 222Item 2df-polarityN 30397
[Holland95] p. 223Remarkispsubcl2N 30441  omllaw4 29741  pol1N 30404  polcon3N 30411
[Holland95] p. 223Definitiondf-psubclN 30429
[Holland95] p. 223Equation for polaritypolval2N 30400
[Hughes] p. 44Equation 1.21bax-his3 22547
[Hughes] p. 47Definition of projection operatordfpjop 23646
[Hughes] p. 49Equation 1.30eighmre 23427  eigre 23299  eigrei 23298
[Hughes] p. 49Equation 1.31eighmorth 23428  eigorth 23302  eigorthi 23301
[Hughes] p. 137Remark (ii)eigposi 23300
[Huneke] p. 1Theoremfrgrancvvdeq 28153  frgrancvvdgeq 28154
[Huneke] p. 1Lemma A for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemA 28148
[Huneke] p. 1Lemma B for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemB 28149
[Huneke] p. 1Lemma C for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemC 28150
[Huneke] p. 2Theoremfrghash2spot 28174  frgraregorufr 28164  frgraregorufr0 28163  frgrawopreg1 28161  frgrawopreg2 28162  frgregordn0 28181  usgreghash2spot 28180  usgreghash2spotv 28177
[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 28158
[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 28159
[Indrzejczak] p. 33Definition ` `Enatded 21672  natded 21672
[Indrzejczak] p. 33Definition ` `Inatded 21672
[Indrzejczak] p. 34Definition ` `Enatded 21672  natded 21672
[Indrzejczak] p. 34Definition ` `Inatded 21672
[Jech] p. 4Definition of classcv 1648  cvjust 2407
[Jech] p. 42Lemma 6.1alephexp1 8418
[Jech] p. 42Equation 6.1alephadd 8416  alephmul 8417
[Jech] p. 43Lemma 6.2infmap 8415  infmap2 8062
[Jech] p. 71Lemma 9.3jech9.3 7704
[Jech] p. 72Equation 9.3scott0 7774  scottex 7773
[Jech] p. 72Exercise 9.1rankval4 7757
[Jech] p. 72Scheme "Collection Principle"cp 7779
[Jech] p. 78Definition implied by the footnoteopthprc 4892
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26876
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26972
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26973
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26888
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26892
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26893  rmyp1 26894
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26895  rmym1 26896
[JonesMatijasevic] p. 695Equation 2.11rmx0 26886  rmx1 26887  rmxluc 26897
[JonesMatijasevic] p. 695Equation 2.12rmy0 26890  rmy1 26891  rmyluc 26898
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26900
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26901
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26923  jm2.17b 26924  jm2.17c 26925
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26962
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26966
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26957
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26926  jm2.24nn 26922
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26971
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26977  rmygeid 26927
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26989
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1662
[KalishMontague] p. 85Lemma 2equid 1684
[KalishMontague] p. 85Lemma 3equcomi 1687
[KalishMontague] p. 86Lemma 7cbvalivw 1682  cbvaliw 1681
[KalishMontague] p. 87Lemma 8spimvw 1677  spimw 1676
[KalishMontague] p. 87Lemma 9spfw 1699  spw 1702
[Kalmbach] p. 14Definition of latticechabs1 22979  chabs1i 22981  chabs2 22980  chabs2i 22982  chjass 22996  chjassi 22949  latabs1 14479  latabs2 14480
[Kalmbach] p. 15Definition of atomdf-at 23802  ela 23803
[Kalmbach] p. 15Definition of coverscvbr2 23747  cvrval2 29769
[Kalmbach] p. 16Definitiondf-ol 29673  df-oml 29674
[Kalmbach] p. 20Definition of commutescmbr 23047  cmbri 23053  cmtvalN 29706  df-cm 23046  df-cmtN 29672
[Kalmbach] p. 22Remarkomllaw5N 29742  pjoml5 23076  pjoml5i 23051
[Kalmbach] p. 22Definitionpjoml2 23074  pjoml2i 23048
[Kalmbach] p. 22Theorem 2(v)cmcm 23077  cmcmi 23055  cmcmii 23060  cmtcomN 29744
[Kalmbach] p. 22Theorem 2(ii)omllaw3 29740  omlsi 22867  pjoml 22899  pjomli 22898
[Kalmbach] p. 22Definition of OML lawomllaw2N 29739
[Kalmbach] p. 23Remarkcmbr2i 23059  cmcm3 23078  cmcm3i 23057  cmcm3ii 23062  cmcm4i 23058  cmt3N 29746  cmt4N 29747  cmtbr2N 29748
[Kalmbach] p. 23Lemma 3cmbr3 23071  cmbr3i 23063  cmtbr3N 29749
[Kalmbach] p. 25Theorem 5fh1 23081  fh1i 23084  fh2 23082  fh2i 23085  omlfh1N 29753
[Kalmbach] p. 65Remarkchjatom 23821  chslej 22961  chsleji 22921  shslej 22843  shsleji 22833
[Kalmbach] p. 65Proposition 1chocin 22958  chocini 22917  chsupcl 22803  chsupval2 22873  h0elch 22718  helch 22707  hsupval2 22872  ocin 22759  ococss 22756  shococss 22757
[Kalmbach] p. 65Definition of subspace sumshsval 22775
[Kalmbach] p. 66Remarkdf-pjh 22858  pjssmi 23629  pjssmii 23144
[Kalmbach] p. 67Lemma 3osum 23108  osumi 23105
[Kalmbach] p. 67Lemma 4pjci 23664
[Kalmbach] p. 103Exercise 6atmd2 23864
[Kalmbach] p. 103Exercise 12mdsl0 23774
[Kalmbach] p. 140Remarkhatomic 23824  hatomici 23823  hatomistici 23826
[Kalmbach] p. 140Proposition 1atlatmstc 29814
[Kalmbach] p. 140Proposition 1(i)atexch 23845  lsatexch 29538
[Kalmbach] p. 140Proposition 1(ii)chcv1 23819  cvlcvr1 29834  cvr1 29904
[Kalmbach] p. 140Proposition 1(iii)cvexch 23838  cvexchi 23833  cvrexch 29914
[Kalmbach] p. 149Remark 2chrelati 23828  hlrelat 29896  hlrelat5N 29895  lrelat 29509
[Kalmbach] p. 153Exercise 5lsmcv 16176  lsmsatcv 29505  spansncv 23116  spansncvi 23115
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29524  spansncv2 23757
[Kalmbach] p. 266Definitiondf-st 23675
[Kalmbach2] p. 8Definition of adjointdf-adjh 23313
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8485  fpwwe2 8482
[KanamoriPincus] p. 416Corollary 1.3canth4 8486
[KanamoriPincus] p. 417Corollary 1.6canthp1 8493
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8488
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8490
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8503
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8507  gchxpidm 8508
[KanamoriPincus] p. 419Theorem 2.1gchacg 8511  gchhar 8510
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 8060  unxpwdom 7521
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8513
[Kreyszig] p. 3Property M1metcl 18323  xmetcl 18322
[Kreyszig] p. 4Property M2meteq0 18330
[Kreyszig] p. 8Definition 1.1-8dscmet 18581
[Kreyszig] p. 12Equation 5conjmul 9695  muleqadd 9630
[Kreyszig] p. 18Definition 1.3-2mopnval 18429
[Kreyszig] p. 19Remarkmopntopon 18430
[Kreyszig] p. 19Theorem T1mopn0 18489  mopnm 18435
[Kreyszig] p. 19Theorem T2unimopn 18487
[Kreyszig] p. 19Definition of neighborhoodneibl 18492
[Kreyszig] p. 20Definition 1.3-3metcnp2 18533
[Kreyszig] p. 25Definition 1.4-1lmbr 17284  lmmbr 19172  lmmbr2 19173
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17406
[Kreyszig] p. 28Theorem 1.4-5lmcau 19226
[Kreyszig] p. 28Definition 1.4-3iscau 19190  iscmet2 19208
[Kreyszig] p. 30Theorem 1.4-7cmetss 19228
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17485  metelcls 19218
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 19219  metcld2 19220
[Kreyszig] p. 51Equation 2clmvneg1 19077  lmodvneg1 15950  nvinv 22081  vcm 22011
[Kreyszig] p. 51Equation 1aclm0vs 19076  lmod0vs 15946  vc0 22009
[Kreyszig] p. 51Equation 1blmodvs0 15947  vcz 22010
[Kreyszig] p. 58Definition 2.2-1imsmet 22144
[Kreyszig] p. 59Equation 1imsdval 22139  imsdval2 22140
[Kreyszig] p. 63Problem 1nvnd 22141
[Kreyszig] p. 64Problem 2nvge0 22124  nvz 22119
[Kreyszig] p. 64Problem 3nvabs 22123
[Kreyszig] p. 91Definition 2.7-1isblo3i 22263
[Kreyszig] p. 92Equation 2df-nmoo 22207
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 22269  blocni 22267
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 22268
[Kreyszig] p. 129Definition 3.1-1cphipeq0 19127  ipeq0 16832  ipz 22179
[Kreyszig] p. 135Problem 2pythi 22312
[Kreyszig] p. 137Lemma 3-2.1(a)sii 22316
[Kreyszig] p. 144Equation 4supcvg 12598
[Kreyszig] p. 144Theorem 3.3-1minvec 19298  minveco 22347
[Kreyszig] p. 196Definition 3.9-1df-aj 22212
[Kreyszig] p. 247Theorem 4.7-2bcth 19243
[Kreyszig] p. 249Theorem 4.7-3ubth 22336
[Kreyszig] p. 470Definition of positive operator orderingleop 23587  leopg 23586
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 23605
[Kreyszig] p. 525Theorem 10.1-1htth 22382
[Kunen] p. 10Axiom 0a9e 1948  axnul 4305
[Kunen] p. 11Axiom 3axnul 4305
[Kunen] p. 12Axiom 6zfrep6 5935
[Kunen] p. 24Definition 10.24mapval 6997  mapvalg 6995
[Kunen] p. 30Lemma 10.20fodom 8366
[Kunen] p. 31Definition 10.24mapex 6991
[Kunen] p. 95Definition 2.1df-r1 7654
[Kunen] p. 97Lemma 2.10r1elss 7696  r1elssi 7695
[Kunen] p. 107Exercise 4rankop 7748  rankopb 7742  rankuni 7753  rankxplim 7767  rankxpsuc 7770
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4071
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27427
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27422
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27428
[LeBlanc] p. 277Rule R2axnul 4305
[Levy] p. 338Axiomdf-clab 2399  df-clel 2408  df-cleq 2405
[Levy58] p. 2Definition Iisfin1-3 8230
[Levy58] p. 2Definition IIdf-fin2 8130
[Levy58] p. 2Definition Iadf-fin1a 8129
[Levy58] p. 2Definition IIIdf-fin3 8132
[Levy58] p. 3Definition Vdf-fin5 8133
[Levy58] p. 3Definition IVdf-fin4 8131
[Levy58] p. 4Definition VIdf-fin6 8134
[Levy58] p. 4Definition VIIdf-fin7 8135
[Levy58], p. 3Theorem 1fin1a2 8259
[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 23872
[Maeda] p. 168Lemma 5mdsym 23876  mdsymi 23875
[Maeda] p. 168Lemma 4(i)mdsymlem4 23870  mdsymlem6 23872  mdsymlem7 23873
[Maeda] p. 168Lemma 4(ii)mdsymlem8 23874
[MaedaMaeda] p. 1Remarkssdmd1 23777  ssdmd2 23778  ssmd1 23775  ssmd2 23776
[MaedaMaeda] p. 1Lemma 1.2mddmd2 23773
[MaedaMaeda] p. 1Definition 1.1df-dmd 23745  df-md 23744  mdbr 23758
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 23795  mdslj1i 23783  mdslj2i 23784  mdslle1i 23781  mdslle2i 23782  mdslmd1i 23793  mdslmd2i 23794
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 23785  mdsl2bi 23787  mdsl2i 23786
[MaedaMaeda] p. 2Lemma 1.6mdexchi 23799
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 23796
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 23797
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 23774
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 23779  mdsl3 23780
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 23798
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23893
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 29816  hlrelat1 29894
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29534
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 23800  cvmdi 23788  cvnbtwn4 23753  cvrnbtwn4 29774
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 23801
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 29835  cvp 23839  cvrp 29910  lcvp 29535
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 23863
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 23862
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 29828  hlexch4N 29886
[MaedaMaeda] p. 34Exercise 7.1atabsi 23865
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 29937
[MaedaMaeda] p. 61Definition 15.10psubN 30243  atpsubN 30247  df-pointsN 29996  pointpsubN 30245
[MaedaMaeda] p. 62Theorem 15.5df-pmap 29998  pmap11 30256  pmaple 30255  pmapsub 30262  pmapval 30251
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 30259  pmap1N 30261
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 30264  pmapglb2N 30265  pmapglb2xN 30266  pmapglbx 30263
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 30346
[MaedaMaeda] p. 67Postulate PS1ps-1 29971
[MaedaMaeda] p. 68Lemma 16.2df-padd 30290  paddclN 30336  paddidm 30335
[MaedaMaeda] p. 68Condition PS2ps-2 29972
[MaedaMaeda] p. 68Equation 16.2.1paddass 30332
[MaedaMaeda] p. 69Lemma 16.4ps-1 29971
[MaedaMaeda] p. 69Theorem 16.4ps-2 29972
[MaedaMaeda] p. 70Theorem 16.9lsmmod 15270  lsmmod2 15271  lssats 29507  shatomici 23822  shatomistici 23825  shmodi 22853  shmodsi 22852
[MaedaMaeda] p. 130Remark 29.6dmdmd 23764  mdsymlem7 23873
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 23052
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22956
[MaedaMaeda] p. 139Remarksumdmdii 23879
[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 28745
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 28746
[Margaris] p. 79Rule Cexinst01 28444  exinst11 28445
[Margaris] p. 89Theorem 19.219.2 1667  19.2g 1769  r19.2z 3685
[Margaris] p. 89Theorem 19.319.3 1787  19.3v 1673  rr19.3v 3045
[Margaris] p. 89Theorem 19.5alcom 1748
[Margaris] p. 89Theorem 19.6alex 1578
[Margaris] p. 89Theorem 19.7alnex 1549
[Margaris] p. 89Theorem 19.819.8a 1758
[Margaris] p. 89Theorem 19.919.9 1793  19.9h 1790  19.9v 1672  exlimd 1820  exlimdh 1822
[Margaris] p. 89Theorem 19.11excom 1752  excomim 1753
[Margaris] p. 89Theorem 19.1219.12 1865  r19.12 2787
[Margaris] p. 90Theorem 19.14exnal 1580
[Margaris] p. 90Theorem 19.152albi 27452  albi 1570  ralbi 2810
[Margaris] p. 90Theorem 19.1619.16 1879
[Margaris] p. 90Theorem 19.1719.17 1880
[Margaris] p. 90Theorem 19.182exbi 27454  exbi 1588
[Margaris] p. 90Theorem 19.1919.19 1881
[Margaris] p. 90Theorem 19.202alim 27451  alim 1564  alimd 1776  alimdh 1569  alimdv 1628  ralimdaa 2751  ralimdv 2753  ralimdva 2752  sbcimdv 3190
[Margaris] p. 90Theorem 19.2119.21-2 1883  19.21 1810  19.21bi 1770  19.21h 1811  19.21t 1809  19.21v 1909  19.21vv 27450  alrimd 1781  alrimdd 1780  alrimdh 1594  alrimdv 1640  alrimi 1777  alrimih 1571  alrimiv 1638  alrimivv 1639  r19.21 2760  r19.21be 2775  r19.21bi 2772  r19.21t 2759  r19.21v 2761  ralrimd 2762  ralrimdv 2763  ralrimdva 2764  ralrimdvv 2768  ralrimdvva 2769  ralrimi 2755  ralrimiv 2756  ralrimiva 2757  ralrimivv 2765  ralrimivva 2766  ralrimivvva 2767  ralrimivw 2758  rexlimi 2791
[Margaris] p. 90Theorem 19.222alimdv 1630  2exim 27453  2eximdv 1631  exim 1581  eximd 1782  eximdh 1595  eximdv 1629  rexim 2778  reximdai 2782  reximddv 23923  reximdv 2785  reximdv2 2783  reximdva 2786  reximdvai 2784  reximi2 2780
[Margaris] p. 90Theorem 19.2319.23 1815  19.23bi 1771  19.23h 1816  19.23t 1814  19.23v 1910  19.23vv 1911  exlimdv 1643  exlimdvv 1644  exlimexi 28327  exlimi 1817  exlimih 1818  exlimiv 1641  exlimivv 1642  r19.23 2789  r19.23v 2790  rexlimd 2795  rexlimdv 2797  rexlimdv3a 2800  rexlimdva 2798  rexlimdvaa 2799  rexlimdvv 2804  rexlimdvva 2805  rexlimdvw 2801  rexlimiv 2792  rexlimiva 2793  rexlimivv 2803
[Margaris] p. 90Theorem 19.2419.24 1670
[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 2807  r19.26-3 2808  r19.26 2806  r19.26m 2809
[Margaris] p. 90Theorem 19.2719.27 1837  19.27v 1913  r19.27av 2812  r19.27z 3694  r19.27zv 3695
[Margaris] p. 90Theorem 19.2819.28 1838  19.28v 1914  19.28vv 27460  r19.28av 2813  r19.28z 3688  r19.28zv 3691  rr19.28v 3046
[Margaris] p. 90Theorem 19.2919.29 1603  19.29r 1604  19.29r2 1605  19.29x 1606  r19.29 2814  r19.29d2r 2819  r19.29r 2815
[Margaris] p. 90Theorem 19.3019.30 1611  r19.30 2821
[Margaris] p. 90Theorem 19.3119.31 1893  19.31vv 27458
[Margaris] p. 90Theorem 19.3219.32 1892  r19.32 27820  r19.32v 2822
[Margaris] p. 90Theorem 19.3319.33-2 27456  19.33 1614  19.33b 1615
[Margaris] p. 90Theorem 19.3419.34 1671
[Margaris] p. 90Theorem 19.3519.35 1607  19.35i 1608  19.35ri 1609  r19.35 2823
[Margaris] p. 90Theorem 19.3619.36 1888  19.36aiv 1916  19.36i 1889  19.36v 1915  19.36vv 27457  r19.36av 2824  r19.36zv 3696
[Margaris] p. 90Theorem 19.3719.37 1890  19.37aiv 1919  19.37v 1918  19.37vv 27459  r19.37 2825  r19.37av 2826  r19.37zv 3692
[Margaris] p. 90Theorem 19.3819.38 1808
[Margaris] p. 90Theorem 19.3919.39 1669
[Margaris] p. 90Theorem 19.4019.40-2 1617  19.40 1616  r19.40 2827
[Margaris] p. 90Theorem 19.4119.41 1896  19.41rg 28356  19.41v 1920  19.41vv 1921  19.41vvv 1922  19.41vvvv 1923  r19.41 2828  r19.41v 2829  r19.41vv 23931
[Margaris] p. 90Theorem 19.4219.42 1898  19.42v 1924  19.42vv 1926  19.42vvv 1927  r19.42v 2830
[Margaris] p. 90Theorem 19.4319.43 1612  r19.43 2831
[Margaris] p. 90Theorem 19.4419.44 1894  r19.44av 2832
[Margaris] p. 90Theorem 19.4519.45 1895  r19.45av 2833  r19.45zv 3693
[Margaris] p. 110Exercise 2(b)eu1 2283
[Mayet] p. 370Remarkjpi 23734  largei 23731  stri 23721
[Mayet3] p. 9Definition of CH-statesdf-hst 23676  ishst 23678
[Mayet3] p. 10Theoremhstrbi 23730  hstri 23729
[Mayet3] p. 1223Theorem 4.1mayete3i 23191
[Mayet3] p. 1240Theorem 7.1mayetes3i 23193
[MegPav2000] p. 2344Theorem 3.3stcltrthi 23742
[MegPav2000] p. 2345Definition 3.4-1chintcl 22795  chsupcl 22803
[MegPav2000] p. 2345Definition 3.4-2hatomic 23824
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 23818
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 23845
[MegPav2000] p. 2366Figure 7pl42N 30477
[MegPav2002] p. 362Lemma 2.2latj31 14491  latj32 14489  latjass 14487
[Megill] p. 444Axiom C5ax-17 1623  ax17o 2215
[Megill] p. 444Section 7conventions 21671
[Megill] p. 445Lemma L12aecom-o 2209  aecom 2001  ax-10 2198
[Megill] p. 446Lemma L17equtrr 1691
[Megill] p. 446Lemma L18ax9from9o 2206
[Megill] p. 446Lemma L19hbnae-o 2237  hbnae 2009
[Megill] p. 447Remark 9.1df-sb 1656  sbid 1943  sbidd-misc 28184  sbidd 28183
[Megill] p. 448Remark 9.6ax15 2077
[Megill] p. 448Scheme C4'ax-5o 2194
[Megill] p. 448Scheme C5'ax-4 2193  sp 1759
[Megill] p. 448Scheme C6'ax-7 1745
[Megill] p. 448Scheme C7'ax-6o 2195
[Megill] p. 448Scheme C8'ax-8 1683
[Megill] p. 448Scheme C9'ax-12o 2200
[Megill] p. 448Scheme C10'ax-9 1662  ax-9o 2196
[Megill] p. 448Scheme C11'ax-10o 2197
[Megill] p. 448Scheme C12'ax-13 1723
[Megill] p. 448Scheme C13'ax-14 1725
[Megill] p. 448Scheme C14'ax-15 2201
[Megill] p. 448Scheme C15'ax-11o 2199
[Megill] p. 448Scheme C16'ax-16 2202
[Megill] p. 448Theorem 9.4dral1-o 2212  dral1 2032  dral2-o 2239  dral2 2030  drex1 2034  drex2 2035  drsb1 2078  drsb2 2118
[Megill] p. 448Theorem 9.7conventions 21671
[Megill] p. 449Theorem 9.7sbcom2 2171  sbequ 2117  sbid2v 2181
[Megill] p. 450Example in Appendixhba1-o 2207  hba1 1800
[Mendelson] p. 35Axiom A3hirstL-ax3 27735
[Mendelson] p. 36Lemma 1.8id1 21
[Mendelson] p. 69Axiom 4rspsbc 3207  rspsbca 3208  stdpc4 2080
[Mendelson] p. 69Axiom 5ax-5o 2194  ra5 3213  stdpc5 1812
[Mendelson] p. 81Rule Cexlimiv 1641
[Mendelson] p. 95Axiom 6stdpc6 1695
[Mendelson] p. 95Axiom 7stdpc7 1938
[Mendelson] p. 225Axiom system NBGru 3128
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4426
[Mendelson] p. 231Exercise 4.10(k)inv1 3622
[Mendelson] p. 231Exercise 4.10(l)unv 3623
[Mendelson] p. 231Exercise 4.10(n)dfin3 3548
[Mendelson] p. 231Exercise 4.10(o)df-nul 3597
[Mendelson] p. 231Exercise 4.10(q)dfin4 3549
[Mendelson] p. 231Exercise 4.10(s)ddif 3447
[Mendelson] p. 231Definition of uniondfun3 3547
[Mendelson] p. 235Exercise 4.12(c)univ 4721
[Mendelson] p. 235Exercise 4.12(d)pwv 3982
[Mendelson] p. 235Exercise 4.12(j)pwin 4455
[Mendelson] p. 235Exercise 4.12(k)pwunss 4456
[Mendelson] p. 235Exercise 4.12(l)pwssun 4457
[Mendelson] p. 235Exercise 4.12(n)uniin 4003
[Mendelson] p. 235Exercise 4.12(p)reli 4969
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5357
[Mendelson] p. 244Proposition 4.8(g)epweon 4731
[Mendelson] p. 246Definition of successordf-suc 4555
[Mendelson] p. 250Exercise 4.36oelim2 6805
[Mendelson] p. 254Proposition 4.22(b)xpen 7237
[Mendelson] p. 254Proposition 4.22(c)xpsnen 7159  xpsneng 7160
[Mendelson] p. 254Proposition 4.22(d)xpcomen 7166  xpcomeng 7167
[Mendelson] p. 254Proposition 4.22(e)xpassen 7169
[Mendelson] p. 255Definitionbrsdom 7097
[Mendelson] p. 255Exercise 4.39endisj 7162
[Mendelson] p. 255Exercise 4.41mapprc 6989
[Mendelson] p. 255Exercise 4.43mapsnen 7151
[Mendelson] p. 255Exercise 4.45mapunen 7243
[Mendelson] p. 255Exercise 4.47xpmapen 7242
[Mendelson] p. 255Exercise 4.42(a)map0e 7018
[Mendelson] p. 255Exercise 4.42(b)map1 7152
[Mendelson] p. 257Proposition 4.24(a)undom 7163
[Mendelson] p. 258Exercise 4.56(b)cdaen 8017
[Mendelson] p. 258Exercise 4.56(c)cdaassen 8026  cdacomen 8025
[Mendelson] p. 258Exercise 4.56(f)cdadom1 8030
[Mendelson] p. 258Exercise 4.56(g)xp2cda 8024
[Mendelson] p. 258Definition of cardinal sumcdaval 8014  df-cda 8012
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6742
[Mendelson] p. 266Proposition 4.34(f)oaordex 6768
[Mendelson] p. 275Proposition 4.42(d)entri3 8398
[Mendelson] p. 281Definitiondf-r1 7654
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7703
[Mendelson] p. 287Axiom system MKru 3128
[MertziosUnger] p. 153Proposition 12pthfrgra 28123  2pthfrgrarn 28121  2pthfrgrarn2 28122  frconngra 28133  n4cyclfrgra 28130  vdgfrgragt2 28140  vdgn1frgrav2 28139  vdn1frgrav2 28138
[Mittelstaedt] p. 9Definitiondf-oc 22715
[Monk1] p. 22Remarkconventions 21671
[Monk1] p. 22Theorem 3.1conventions 21671
[Monk1] p. 26Theorem 2.8(vii)ssin 3531
[Monk1] p. 33Theorem 3.2(i)ssrel 4931
[Monk1] p. 33Theorem 3.2(ii)eqrel 4932
[Monk1] p. 34Definition 3.3df-opab 4235
[Monk1] p. 36Theorem 3.7(i)coi1 5352  coi2 5353
[Monk1] p. 36Theorem 3.8(v)dm0 5050  rn0 5094
[Monk1] p. 36Theorem 3.7(ii)cnvi 5243
[Monk1] p. 37Theorem 3.13(i)relxp 4950
[Monk1] p. 37Theorem 3.13(x)dmxp 5055  rnxp 5266
[Monk1] p. 37Theorem 3.13(ii)xp0 5258  xp0r 4923
[Monk1] p. 38Theorem 3.16(ii)ima0 5188
[Monk1] p. 38Theorem 3.16(viii)imai 5185
[Monk1] p. 39Theorem 3.17imaexg 5184
[Monk1] p. 39Theorem 3.16(xi)imassrn 5183
[Monk1] p. 41Theorem 4.3(i)fnopfv 5832  funfvop 5809
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5737
[Monk1] p. 42Theorem 4.4(iii)fvelima 5745
[Monk1] p. 43Theorem 4.6funun 5462
[Monk1] p. 43Theorem 4.8(iv)dff13 5971  dff13f 5973
[Monk1] p. 46Theorem 4.15(v)funex 5930  funrnex 5934
[Monk1] p. 50Definition 5.4fniunfv 5961
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5320
[Monk1] p. 52Theorem 5.11(viii)ssint 4034
[Monk1] p. 52Definition 5.13 (i)1stval2 6331  df-1st 6316
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6332  df-2nd 6317
[Monk1] p. 112Theorem 15.17(v)ranksn 7744  ranksnb 7717
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7745
[Monk1] p. 112Theorem 15.17(iii)rankun 7746  rankunb 7740
[Monk1] p. 113Theorem 15.18r1val3 7728
[Monk1] p. 113Definition 15.19df-r1 7654  r1val2 7727
[Monk1] p. 117Lemmazorn2 8350  zorn2g 8347
[Monk1] p. 133Theorem 18.11cardom 7837
[Monk1] p. 133Theorem 18.12canth3 8400
[Monk1] p. 133Theorem 18.14carduni 7832
[Monk2] p. 105Axiom C4ax-5 1563
[Monk2] p. 105Axiom C7ax-8 1683
[Monk2] p. 105Axiom C8ax-11 1757  ax-11o 2199
[Monk2] p. 105Axiom (C8)ax11v 2153
[Monk2] p. 108Lemma 5ax-5o 2194
[Monk2] p. 109Lemma 12ax-7 1745
[Monk2] p. 109Lemma 15equvin 2046  equvini 2042  eqvinop 4409
[Monk2] p. 113Axiom C5-1ax-17 1623  ax17o 2215
[Monk2] p. 113Axiom C5-2ax-6 1740
[Monk2] p. 113Axiom C5-3ax-7 1745
[Monk2] p. 114Lemma 21sp 1759
[Monk2] p. 114Lemma 22ax5o 1761  hba1-o 2207  hba1 1800
[Monk2] p. 114Lemma 23nfia1 1871
[Monk2] p. 114Lemma 24nfa2 1870  nfra2 2728
[Moore] p. 53Part Idf-mre 13774
[Munkres] p. 77Example 2distop 17023  indistop 17029  indistopon 17028
[Munkres] p. 77Example 3fctop 17031  fctop2 17032
[Munkres] p. 77Example 4cctop 17033
[Munkres] p. 78Definition of basisdf-bases 16928  isbasis3g 16977
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13630  tgval2 16984
[Munkres] p. 79Remarktgcl 16997
[Munkres] p. 80Lemma 2.1tgval3 16991
[Munkres] p. 80Lemma 2.2tgss2 17015  tgss3 17014
[Munkres] p. 81Lemma 2.3basgen 17016  basgen2 17017
[Munkres] p. 89Definition of subspace topologyresttop 17186
[Munkres] p. 93Theorem 6.1(1)0cld 17065  topcld 17062
[Munkres] p. 93Theorem 6.1(2)iincld 17066
[Munkres] p. 93Theorem 6.1(3)uncld 17068
[Munkres] p. 94Definition of closureclsval 17064
[Munkres] p. 94Definition of interiorntrval 17063
[Munkres] p. 95Theorem 6.5(a)clsndisj 17102  elcls 17100
[Munkres] p. 95Theorem 6.5(b)elcls3 17110
[Munkres] p. 97Theorem 6.6clslp 17174  neindisj 17144
[Munkres] p. 97Corollary 6.7cldlp 17176
[Munkres] p. 97Definition of limit pointislp2 17172  lpval 17166
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17341
[Munkres] p. 102Definition of continuous functiondf-cn 17253  iscn 17261  iscn2 17264
[Munkres] p. 107Theorem 7.2(g)cncnp 17306  cncnp2 17307  cncnpi 17304  df-cnp 17254  iscnp 17263  iscnp2 17265
[Munkres] p. 127Theorem 10.1metcn 18534
[Munkres] p. 128Theorem 10.3metcn4 19224
[NielsenChuang] p. 195Equation 4.73unierri 23568
[Pfenning] p. 17Definition XMnatded 21672  natded 21672
[Pfenning] p. 17Definition NNCnatded 21672  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 21672
[Pfenning] p. 18Rule"natded 21672
[Pfenning] p. 18Definition /\Inatded 21672
[Pfenning] p. 18Definition ` `Enatded 21672  natded 21672  natded 21672  natded 21672  natded 21672
[Pfenning] p. 18Definition ` `Inatded 21672  natded 21672  natded 21672  natded 21672  natded 21672
[Pfenning] p. 18Definition ` `ELnatded 21672
[Pfenning] p. 18Definition ` `ERnatded 21672
[Pfenning] p. 18Definition ` `Ea,unatded 21672
[Pfenning] p. 18Definition ` `IRnatded 21672
[Pfenning] p. 18Definition ` `Ianatded 21672
[Pfenning] p. 127Definition =Enatded 21672
[Pfenning] p. 127Definition =Inatded 21672
[Ponnusamy] p. 361Theorem 6.44cphip0l 19125  df-dip 22158  dip0l 22178  ip0l 16830
[Ponnusamy] p. 361Equation 6.45ipval 22160
[Ponnusamy] p. 362Equation I1dipcj 22174
[Ponnusamy] p. 362Equation I3cphdir 19128  dipdir 22304  ipdir 16833  ipdiri 22292
[Ponnusamy] p. 362Equation I4ipidsq 22170
[Ponnusamy] p. 362Equation 6.46ip0i 22287
[Ponnusamy] p. 362Equation 6.47ip1i 22289
[Ponnusamy] p. 362Equation 6.48ip2i 22290
[Ponnusamy] p. 363Equation I2cphass 19134  dipass 22307  ipass 16839  ipassi 22303
[Prugovecki] p. 186Definition of brabraval 23408  df-bra 23314
[Prugovecki] p. 376Equation 8.1df-kb 23315  kbval 23418
[PtakPulmannova] p. 66Proposition 3.2.17atomli 23846
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30382
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 23860  atcvat4i 23861  cvrat3 29936  cvrat4 29937  lsatcvat3 29547
[PtakPulmannova] p. 68Definition 3.2.18cvbr 23746  cvrval 29764  df-cv 23743  df-lcv 29514  lspsncv0 16181
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30394
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30395
[Quine] p. 16Definition 2.1df-clab 2399  rabid 2852
[Quine] p. 17Definition 2.1''dfsb7 2179
[Quine] p. 18Definition 2.7df-cleq 2405
[Quine] p. 19Definition 2.9conventions 21671  df-v 2926
[Quine] p. 34Theorem 5.1abeq2 2517
[Quine] p. 35Theorem 5.2abid2 2529  abid2f 2573
[Quine] p. 40Theorem 6.1sb5 2157
[Quine] p. 40Theorem 6.2sb56 2155  sb6 2156
[Quine] p. 41Theorem 6.3df-clel 2408
[Quine] p. 41Theorem 6.4eqid 2412  eqid1 21722
[Quine] p. 41Theorem 6.5eqcom 2414
[Quine] p. 42Theorem 6.6df-sbc 3130
[Quine] p. 42Theorem 6.7dfsbcq 3131  dfsbcq2 3132
[Quine] p. 43Theorem 6.8vex 2927
[Quine] p. 43Theorem 6.9isset 2928
[Quine] p. 44Theorem 7.3spcgf 2999  spcgv 3004  spcimgf 2997
[Quine] p. 44Theorem 6.11spsbc 3141  spsbcd 3142
[Quine] p. 44Theorem 6.12elex 2932
[Quine] p. 44Theorem 6.13elab 3050  elabg 3051  elabgf 3048
[Quine] p. 44Theorem 6.14noel 3600
[Quine] p. 48Theorem 7.2snprc 3839
[Quine] p. 48Definition 7.1df-pr 3789  df-sn 3788
[Quine] p. 49Theorem 7.4snss 3894  snssg 3900
[Quine] p. 49Theorem 7.5prss 3920  prssg 3921
[Quine] p. 49Theorem 7.6prid1 3880  prid1g 3878  prid2 3881  prid2g 3879  snid 3809  snidg 3807
[Quine] p. 51Theorem 7.13prex 4374  snex 4373  snexALT 4353
[Quine] p. 53Theorem 8.2unisn 3999  unisnALT 28756  unisng 4000
[Quine] p. 53Theorem 8.3uniun 4002
[Quine] p. 54Theorem 8.6elssuni 4011
[Quine] p. 54Theorem 8.7uni0 4010
[Quine] p. 56Theorem 8.17uniabio 5395
[Quine] p. 56Definition 8.18dfiota2 5386
[Quine] p. 57Theorem 8.19iotaval 5396
[Quine] p. 57Theorem 8.22iotanul 5400
[Quine] p. 58Theorem 8.23iotaex 5402
[Quine] p. 58Definition 9.1df-op 3791
[Quine] p. 61Theorem 9.5opabid 4429  opelopab 4444  opelopaba 4439  opelopabaf 4446  opelopabf 4447  opelopabg 4441  opelopabga 4436  oprabid 6072
[Quine] p. 64Definition 9.11df-xp 4851
[Quine] p. 64Definition 9.12df-cnv 4853
[Quine] p. 64Definition 9.15df-id 4466
[Quine] p. 65Theorem 10.3fun0 5475
[Quine] p. 65Theorem 10.4funi 5450
[Quine] p. 65Theorem 10.5funsn 5466  funsng 5464
[Quine] p. 65Definition 10.1df-fun 5423
[Quine] p. 65Definition 10.2args 5199  dffv4 5692
[Quine] p. 68Definition 10.11conventions 21671  df-fv 5429  fv2 5690
[Quine] p. 124Theorem 17.3nn0opth2 11528  nn0opth2i 11527  nn0opthi 11526  omopthi 6867
[Quine] p. 177Definition 25.2df-rdg 6635
[Quine] p. 232Equation icarddom 8393
[Quine] p. 284Axiom 39(vi)funimaex 5498  funimaexg 5497
[Quine] p. 331Axiom system NFru 3128
[ReedSimon] p. 36Definition (iii)ax-his3 22547
[ReedSimon] p. 63Exercise 4(a)df-dip 22158  polid 22622  polid2i 22620  polidi 22621
[ReedSimon] p. 63Exercise 4(b)df-ph 22275
[ReedSimon] p. 195Remarklnophm 23483  lnophmi 23482
[Retherford] p. 49Exercise 1(i)leopadd 23596
[Retherford] p. 49Exercise 1(ii)leopmul 23598  leopmuli 23597
[Retherford] p. 49Exercise 1(iv)leoptr 23601
[Retherford] p. 49Definition VI.1df-leop 23316  leoppos 23590
[Retherford] p. 49Exercise 1(iii)leoptri 23600
[Retherford] p. 49Definition of operator orderingleop3 23589
[Rudin] p. 164Equation 27efcan 12660
[Rudin] p. 164Equation 30efzval 12666
[Rudin] p. 167Equation 48absefi 12760
[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 5216
[Schechter] p. 51Definition of irreflexivityintirr 5219
[Schechter] p. 51Definition of symmetrycnvsym 5215
[Schechter] p. 51Definition of transitivitycotr 5213
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13774
[Schechter] p. 79Definition of Moore closuredf-mrc 13775
[Schechter] p. 82Section 4.5df-mrc 13775
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13777
[Schechter] p. 139Definition AC3dfac9 7980
[Schechter] p. 141Definition (MC)dfac11 27036
[Schechter] p. 149Axiom DC1ax-dc 8290  axdc3 8298
[Schechter] p. 187Definition of ring with unitisrng 15631  isrngo 21927
[Schechter] p. 276Remark 11.6.espan0 23005
[Schechter] p. 276Definition of spandf-span 22772  spanval 22796
[Schechter] p. 428Definition 15.35bastop1 17021
[Schwabhauser] p. 10Axiom A1axcgrrflx 25765
[Schwabhauser] p. 10Axiom A2axcgrtr 25766
[Schwabhauser] p. 10Axiom A3axcgrid 25767
[Schwabhauser] p. 11Axiom A4axsegcon 25778
[Schwabhauser] p. 11Axiom A5ax5seg 25789
[Schwabhauser] p. 11Axiom A6axbtwnid 25790
[Schwabhauser] p. 12Axiom A7axpasch 25792
[Schwabhauser] p. 12Axiom A8axlowdim2 25811
[Schwabhauser] p. 13Axiom A10axeuclid 25814
[Schwabhauser] p. 13Axiom A11axcont 25827
[Schwabhauser] p. 27Theorem 2.1cgrrflx 25833
[Schwabhauser] p. 27Theorem 2.2cgrcomim 25835
[Schwabhauser] p. 27Theorem 2.3cgrtr 25838
[Schwabhauser] p. 27Theorem 2.4cgrcoml 25842
[Schwabhauser] p. 27Theorem 2.5cgrcomr 25843
[Schwabhauser] p. 28Theorem 2.8cgrtriv 25848
[Schwabhauser] p. 28Theorem 2.105segofs 25852
[Schwabhauser] p. 28Definition 2.10df-ofs 25829
[Schwabhauser] p. 29Theorem 2.11cgrextend 25854
[Schwabhauser] p. 29Theorem 2.12segconeq 25856
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 25868  btwntriv2 25858
[Schwabhauser] p. 30Theorem 3.2btwncomim 25859
[Schwabhauser] p. 30Theorem 3.3btwntriv1 25862
[Schwabhauser] p. 30Theorem 3.4btwnswapid 25863
[Schwabhauser] p. 30Theorem 3.5btwnexch2 25869  btwnintr 25865
[Schwabhauser] p. 30Theorem 3.6btwnexch 25871  btwnexch3 25866
[Schwabhauser] p. 30Theorem 3.7btwnouttr 25870
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25810
[Schwabhauser] p. 32Theorem 3.14btwndiff 25873
[Schwabhauser] p. 33Theorem 3.17trisegint 25874
[Schwabhauser] p. 34Theorem 4.2ifscgr 25890
[Schwabhauser] p. 34Definition 4.1df-ifs 25885
[Schwabhauser] p. 35Theorem 4.3cgrsub 25891
[Schwabhauser] p. 35Theorem 4.5cgrxfr 25901
[Schwabhauser] p. 35Definition 4.4df-cgr3 25886
[Schwabhauser] p. 36Theorem 4.6btwnxfr 25902
[Schwabhauser] p. 36Theorem 4.11colinearperm1 25908  colinearperm2 25910  colinearperm3 25909  colinearperm4 25911  colinearperm5 25912
[Schwabhauser] p. 36Definition 4.10df-colinear 25887
[Schwabhauser] p. 37Theorem 4.12colineartriv1 25913
[Schwabhauser] p. 37Theorem 4.13colinearxfr 25921
[Schwabhauser] p. 37Theorem 4.14lineext 25922
[Schwabhauser] p. 37Theorem 4.16fscgr 25926
[Schwabhauser] p. 37Theorem 4.17linecgr 25927
[Schwabhauser] p. 37Definition 4.15df-fs 25888
[Schwabhauser] p. 38Theorem 4.18lineid 25929
[Schwabhauser] p. 38Theorem 4.19idinside 25930
[Schwabhauser] p. 39Theorem 5.1btwnconn1 25947
[Schwabhauser] p. 41Theorem 5.2btwnconn2 25948
[Schwabhauser] p. 41Theorem 5.3btwnconn3 25949
[Schwabhauser] p. 41Theorem 5.5brsegle2 25955
[Schwabhauser] p. 41Definition 5.4df-segle 25953
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 25956
[Schwabhauser] p. 42Theorem 5.7seglerflx 25958
[Schwabhauser] p. 42Theorem 5.8segletr 25960
[Schwabhauser] p. 42Theorem 5.9segleantisym 25961
[Schwabhauser] p. 42Theorem 5.10seglelin 25962
[Schwabhauser] p. 42Theorem 5.11seglemin 25959
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 25964
[Schwabhauser] p. 43Theorem 6.2btwnoutside 25971
[Schwabhauser] p. 43Theorem 6.3broutsideof3 25972
[Schwabhauser] p. 43Theorem 6.4broutsideof 25967  df-outsideof 25966
[Schwabhauser] p. 43Definition 6.1broutsideof2 25968
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 25973
[Schwabhauser] p. 44Theorem 6.6outsideofcom 25974
[Schwabhauser] p. 44Theorem 6.7outsideoftr 25975
[Schwabhauser] p. 44Theorem 6.11outsideofeu 25977
[Schwabhauser] p. 44Definition 6.8df-ray 25984
[Schwabhauser] p. 45Part 2df-lines2 25985
[Schwabhauser] p. 45Theorem 6.13outsidele 25978
[Schwabhauser] p. 45Theorem 6.15lineunray 25993
[Schwabhauser] p. 45Theorem 6.16lineelsb2 25994
[Schwabhauser] p. 45Theorem 6.17linecom 25996  linerflx1 25995  linerflx2 25997
[Schwabhauser] p. 45Theorem 6.18linethru 25999
[Schwabhauser] p. 45Definition 6.14df-line2 25983
[Schwabhauser] p. 46Theorem 6.19linethrueu 26002
[Schwabhauser] p. 46Theorem 6.21lineintmo 26003
[Shapiro] p. 230Theorem 6.5.1dchrhash 21016  dchrsum 21014  dchrsum2 21013  sumdchr 21017
[Shapiro] p. 232Theorem 6.5.2dchr2sum 21018  sum2dchr 21019
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15587  ablfacrp2 15588
[Shapiro], p. 328Equation 9.2.4vmasum 20961
[Shapiro], p. 329Equation 9.2.7logfac2 20962
[Shapiro], p. 329Equation 9.2.9logfacrlim 20969
[Shapiro], p. 331Equation 9.2.13vmadivsum 21137
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 21140
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 21194  vmalogdivsum2 21193
[Shapiro], p. 375Theorem 9.4.1dirith 21184  dirith2 21183
[Shapiro], p. 375Equation 9.4.3rplogsum 21182  rpvmasum 21181  rpvmasum2 21167
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 21142
[Shapiro], p. 376Equation 9.4.8dchrvmasum 21180
[Shapiro], p. 377Lemma 9.4.1dchrisum 21147  dchrisumlem1 21144  dchrisumlem2 21145  dchrisumlem3 21146  dchrisumlema 21143
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 21150
[Shapiro], p. 379Equation 9.4.16dchrmusum 21179  dchrmusumlem 21177  dchrvmasumlem 21178
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 21149
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 21151
[Shapiro], p. 382Lemma 9.4.4dchrisum0 21175  dchrisum0re 21168  dchrisumn0 21176
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 21161
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 21165
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 21166
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 21221  pntrsumbnd2 21222  pntrsumo1 21220
[Shapiro], p. 405Equation 10.2.1mudivsum 21185
[Shapiro], p. 406Equation 10.2.6mulogsum 21187
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 21189
[Shapiro], p. 407Equation 10.2.8mulog2sum 21192
[Shapiro], p. 418Equation 10.4.6logsqvma 21197
[Shapiro], p. 418Equation 10.4.8logsqvma2 21198
[Shapiro], p. 419Equation 10.4.10selberg 21203
[Shapiro], p. 420Equation 10.4.12selberg2lem 21205
[Shapiro], p. 420Equation 10.4.14selberg2 21206
[Shapiro], p. 422Equation 10.6.7selberg3 21214
[Shapiro], p. 422Equation 10.4.20selberg4lem1 21215
[Shapiro], p. 422Equation 10.4.21selberg3lem1 21212  selberg3lem2 21213
[Shapiro], p. 422Equation 10.4.23selberg4 21216
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 21210
[Shapiro], p. 428Equation 10.6.2selbergr 21223
[Shapiro], p. 429Equation 10.6.8selberg3r 21224
[Shapiro], p. 430Equation 10.6.11selberg4r 21225
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 21239
[Shapiro], p. 434Equation 10.6.27pntlema 21251  pntlemb 21252  pntlemc 21250  pntlemd 21249  pntlemg 21253
[Shapiro], p. 435Equation 10.6.29pntlema 21251
[Shapiro], p. 436Lemma 10.6.1pntpbnd 21243
[Shapiro], p. 436Lemma 10.6.2pntibnd 21248
[Shapiro], p. 436Equation 10.6.34pntlema 21251
[Shapiro], p. 436Equation 10.6.35pntlem3 21264  pntleml 21266
[Stoll] p. 13Definition of symmetric differencesymdif1 3574
[Stoll] p. 16Exercise 4.40dif 3667  dif0 3666
[Stoll] p. 16Exercise 4.8difdifdir 3683
[Stoll] p. 17Theorem 5.1(5)undifv 3670
[Stoll] p. 19Theorem 5.2(13)undm 3567
[Stoll] p. 19Theorem 5.2(13')indm 3568
[Stoll] p. 20Remarkinvdif 3550
[Stoll] p. 25Definition of ordered tripledf-ot 3792
[Stoll] p. 43Definitionuniiun 4112
[Stoll] p. 44Definitionintiin 4113
[Stoll] p. 45Definitiondf-iin 4064
[Stoll] p. 45Definition indexed uniondf-iun 4063
[Stoll] p. 176Theorem 3.4(27)iman 414
[Stoll] p. 262Example 4.1symdif1 3574
[Strang] p. 242Section 6.3expgrowth 27428
[Suppes] p. 22Theorem 2eq0 3610
[Suppes] p. 22Theorem 4eqss 3331  eqssd 3333  eqssi 3332
[Suppes] p. 23Theorem 5ss0 3626  ss0b 3625
[Suppes] p. 23Theorem 6sstr 3324  sstrALT2 28665
[Suppes] p. 23Theorem 7pssirr 3415
[Suppes] p. 23Theorem 8pssn2lp 3416
[Suppes] p. 23Theorem 9psstr 3419
[Suppes] p. 23Theorem 10pssss 3410
[Suppes] p. 25Theorem 12elin 3498  elun 3456
[Suppes] p. 26Theorem 15inidm 3518
[Suppes] p. 26Theorem 16in0 3621
[Suppes] p. 27Theorem 23unidm 3458
[Suppes] p. 27Theorem 24un0 3620
[Suppes] p. 27Theorem 25ssun1 3478
[Suppes] p. 27Theorem 26ssequn1 3485
[Suppes] p. 27Theorem 27unss 3489
[Suppes] p. 27Theorem 28indir 3557
[Suppes] p. 27Theorem 29undir 3558
[Suppes] p. 28Theorem 32difid 3664  difidALT 3665
[Suppes] p. 29Theorem 33difin 3546
[Suppes] p. 29Theorem 34indif 3551
[Suppes] p. 29Theorem 35undif1 3671
[Suppes] p. 29Theorem 36difun2 3675
[Suppes] p. 29Theorem 37difin0 3669
[Suppes] p. 29Theorem 38disjdif 3668
[Suppes] p. 29Theorem 39difundi 3561
[Suppes] p. 29Theorem 40difindi 3563
[Suppes] p. 30Theorem 41nalset 4308
[Suppes] p. 39Theorem 61uniss 4004
[Suppes] p. 39Theorem 65uniop 4427
[Suppes] p. 41Theorem 70intsn 4054
[Suppes] p. 42Theorem 71intpr 4051  intprg 4052
[Suppes] p. 42Theorem 73op1stb 4725
[Suppes] p. 42Theorem 78intun 4050
[Suppes] p. 44Definition 15(a)dfiun2 4093  dfiun2g 4091
[Suppes] p. 44Definition 15(b)dfiin2 4094
[Suppes] p. 47Theorem 86elpw 3773  elpw2 4332  elpw2g 4331  elpwg 3774  elpwgdedVD 28747
[Suppes] p. 47Theorem 87pwid 3780
[Suppes] p. 47Theorem 89pw0 3913
[Suppes] p. 48Theorem 90pwpw0 3914
[Suppes] p. 52Theorem 101xpss12 4948
[Suppes] p. 52Theorem 102xpindi 4975  xpindir 4976
[Suppes] p. 52Theorem 103xpundi 4897  xpundir 4898
[Suppes] p. 54Theorem 105elirrv 7529
[Suppes] p. 58Theorem 2relss 4930
[Suppes] p. 59Theorem 4eldm 5034  eldm2 5035  eldm2g 5033  eldmg 5032
[Suppes] p. 59Definition 3df-dm 4855
[Suppes] p. 60Theorem 6dmin 5044
[Suppes] p. 60Theorem 8rnun 5247
[Suppes] p. 60Theorem 9rnin 5248
[Suppes] p. 60Definition 4dfrn2 5026
[Suppes] p. 61Theorem 11brcnv 5022  brcnvg 5020
[Suppes] p. 62Equation 5elcnv 5016  elcnv2 5017
[Suppes] p. 62Theorem 12relcnv 5209
[Suppes] p. 62Theorem 15cnvin 5246
[Suppes] p. 62Theorem 16cnvun 5244
[Suppes] p. 63Theorem 20co02 5350
[Suppes] p. 63Theorem 21dmcoss 5102
[Suppes] p. 63Definition 7df-co 4854
[Suppes] p. 64Theorem 26cnvco 5023
[Suppes] p. 64Theorem 27coass 5355
[Suppes] p. 65Theorem 31resundi 5127
[Suppes] p. 65Theorem 34elima 5175  elima2 5176  elima3 5177  elimag 5174
[Suppes] p. 65Theorem 35imaundi 5251
[Suppes] p. 66Theorem 40dminss 5253
[Suppes] p. 66Theorem 41imainss 5254
[Suppes] p. 67Exercise 11cnvxp 5257
[Suppes] p. 81Definition 34dfec2 6875
[Suppes] p. 82Theorem 72elec 6911  elecg 6910
[Suppes] p. 82Theorem 73erth 6916  erth2 6917
[Suppes] p. 83Theorem 74erdisj 6919
[Suppes] p. 89Theorem 96map0b 7019
[Suppes] p. 89Theorem 97map0 7021  map0g 7020
[Suppes] p. 89Theorem 98mapsn 7022
[Suppes] p. 89Theorem 99mapss 7023
[Suppes] p. 91Definition 12(ii)alephsuc 7913
[Suppes] p. 91Definition 12(iii)alephlim 7912
[Suppes] p. 92Theorem 1enref 7107  enrefg 7106
[Suppes] p. 92Theorem 2ensym 7123  ensymb 7122  ensymi 7124
[Suppes] p. 92Theorem 3entr 7126
[Suppes] p. 92Theorem 4unen 7156
[Suppes] p. 94Theorem 15endom 7101
[Suppes] p. 94Theorem 16ssdomg 7120
[Suppes] p. 94Theorem 17domtr 7127
[Suppes] p. 95Theorem 18sbth 7194
[Suppes] p. 97Theorem 23canth2 7227  canth2g 7228
[Suppes] p. 97Definition 3brsdom2 7198  df-sdom 7079  dfsdom2 7197
[Suppes] p. 97Theorem 21(i)sdomirr 7211
[Suppes] p. 97Theorem 22(i)domnsym 7200
[Suppes] p. 97Theorem 21(ii)sdomnsym 7199
[Suppes] p. 97Theorem 22(ii)domsdomtr 7209
[Suppes] p. 97Theorem 22(iv)brdom2 7104
[Suppes] p. 97Theorem 21(iii)sdomtr 7212
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7207
[Suppes] p. 98Exercise 4fundmen 7147  fundmeng 7148
[Suppes] p. 98Exercise 6xpdom3 7173
[Suppes] p. 98Exercise 11sdomentr 7208
[Suppes] p. 104Theorem 37fofi 7359
[Suppes] p. 104Theorem 38pwfi 7368
[Suppes] p. 105Theorem 40pwfi 7368
[Suppes] p. 111Axiom for cardinal numberscarden 8390
[Suppes] p. 130Definition 3df-tr 4271
[Suppes] p. 132Theorem 9ssonuni 4734
[Suppes] p. 134Definition 6df-suc 4555
[Suppes] p. 136Theorem Schema 22findes 4842  finds 4838  finds1 4841  finds2 4840
[Suppes] p. 151Theorem 42isfinite 7571  isfinite2 7332  isfiniteg 7334  unbnn 7330
[Suppes] p. 162Definition 5df-ltnq 8759  df-ltpq 8751
[Suppes] p. 197Theorem Schema 4tfindes 4809  tfinds 4806  tfinds2 4810
[Suppes] p. 209Theorem 18oaord1 6761
[Suppes] p. 209Theorem 21oaword2 6763
[Suppes] p. 211Theorem 25oaass 6771
[Suppes] p. 225Definition 8iscard2 7827
[Suppes] p. 227Theorem 56ondomon 8402
[Suppes] p. 228Theorem 59harcard 7829
[Suppes] p. 228Definition 12(i)aleph0 7911
[Suppes] p. 228Theorem Schema 61onintss 4599
[Suppes] p. 228Theorem Schema 62onminesb 4745  onminsb 4746
[Suppes] p. 229Theorem 64alephval2 8411
[Suppes] p. 229Theorem 65alephcard 7915
[Suppes] p. 229Theorem 66alephord2i 7922
[Suppes] p. 229Theorem 67alephnbtwn 7916
[Suppes] p. 229Definition 12df-aleph 7791
[Suppes] p. 242Theorem 6weth 8339
[Suppes] p. 242Theorem 8entric 8396
[Suppes] p. 242Theorem 9carden 8390
[TakeutiZaring] p. 8Axiom 1ax-ext 2393
[TakeutiZaring] p. 13Definition 4.5df-cleq 2405
[TakeutiZaring] p. 13Proposition 4.6df-clel 2408
[TakeutiZaring] p. 13Proposition 4.9cvjust 2407
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2429
[TakeutiZaring] p. 14Definition 4.16df-oprab 6052
[TakeutiZaring] p. 14Proposition 4.14ru 3128
[TakeutiZaring] p. 15Axiom 2zfpair 4369
[TakeutiZaring] p. 15Exercise 1elpr 3800  elpr2 3801  elprg 3799
[TakeutiZaring] p. 15Exercise 2elsn 3797  elsnc 3805  elsnc2 3811  elsnc2g 3810  elsncg 3804
[TakeutiZaring] p. 15Exercise 3elop 4397
[TakeutiZaring] p. 15Exercise 4sneq 3793  sneqr 3934
[TakeutiZaring] p. 15Definition 5.1dfpr2 3798  dfsn2 3796
[TakeutiZaring] p. 16Axiom 3uniex 4672
[TakeutiZaring] p. 16Exercise 6opth 4403
[TakeutiZaring] p. 16Exercise 7opex 4395
[TakeutiZaring] p. 16Exercise 8rext 4380
[TakeutiZaring] p. 16Corollary 5.8unex 4674  unexg 4677
[TakeutiZaring] p. 16Definition 5.3dftp2 3822
[TakeutiZaring] p. 16Definition 5.5df-uni 3984
[TakeutiZaring] p. 16Definition 5.6df-in 3295  df-un 3293
[TakeutiZaring] p. 16Proposition 5.7unipr 3997  uniprg 3998
[TakeutiZaring] p. 17Axiom 4pwex 4350  pwexg 4351
[TakeutiZaring] p. 17Exercise 1eltp 3821
[TakeutiZaring] p. 17Exercise 5elsuc 4618  elsucg 4616  sstr2 3323
[TakeutiZaring] p. 17Exercise 6uncom 3459
[TakeutiZaring] p. 17Exercise 7incom 3501
[TakeutiZaring] p. 17Exercise 8unass 3472
[TakeutiZaring] p. 17Exercise 9inass 3519
[TakeutiZaring] p. 17Exercise 10indi 3555
[TakeutiZaring] p. 17Exercise 11undi 3556
[TakeutiZaring] p. 17Definition 5.9df-pss 3304  dfss2 3305
[TakeutiZaring] p. 17Definition 5.10df-pw 3769
[TakeutiZaring] p. 18Exercise 7unss2 3486
[TakeutiZaring] p. 18Exercise 9df-ss 3302  sseqin2 3528
[TakeutiZaring] p. 18Exercise 10ssid 3335
[TakeutiZaring] p. 18Exercise 12inss1 3529  inss2 3530
[TakeutiZaring] p. 18Exercise 13nss 3374
[TakeutiZaring] p. 18Exercise 15unieq 3992
[TakeutiZaring] p. 18Exercise 18sspwb 4381  sspwimp 28748  sspwimpALT 28755  sspwimpALT2 28759  sspwimpcf 28750
[TakeutiZaring] p. 18Exercise 19pweqb 4388
[TakeutiZaring] p. 19Axiom 5ax-rep 4288
[TakeutiZaring] p. 20Definitiondf-rab 2683
[TakeutiZaring] p. 20Corollary 5.160ex 4307
[TakeutiZaring] p. 20Definition 5.12df-dif 3291
[TakeutiZaring] p. 20Definition 5.14dfnul2 3598
[TakeutiZaring] p. 20Proposition 5.15difid 3664  difidALT 3665
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3605  n0f 3604  neq0 3606
[TakeutiZaring] p. 21Axiom 6zfreg 7527
[TakeutiZaring] p. 21Axiom 6'zfregs 7632
[TakeutiZaring] p. 21Theorem 5.22setind 7637
[TakeutiZaring] p. 21Definition 5.20df-v 2926
[TakeutiZaring] p. 21Proposition 5.21vprc 4309
[TakeutiZaring] p. 22Exercise 10ss 3624
[TakeutiZaring] p. 22Exercise 3ssex 4315  ssexg 4317
[TakeutiZaring] p. 22Exercise 4inex1 4312
[TakeutiZaring] p. 22Exercise 5ruv 7532
[TakeutiZaring] p. 22Exercise 6elirr 7530
[TakeutiZaring] p. 22Exercise 7ssdif0 3654
[TakeutiZaring] p. 22Exercise 11difdif 3441
[TakeutiZaring] p. 22Exercise 13undif3 3570  undif3VD 28712
[TakeutiZaring] p. 22Exercise 14difss 3442
[TakeutiZaring] p. 22Exercise 15sscon 3449
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2679
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2680
[TakeutiZaring] p. 23Proposition 6.2xpex 4957  xpexg 4956  xpexgALT 6264
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4852
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5480
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5614  fun11 5483
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5433  svrelfun 5481
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5025
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5027
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4857
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4858
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4854
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5292  dfrel2 5288
[TakeutiZaring] p. 25Exercise 3xpss 4949
[TakeutiZaring] p. 25Exercise 5relun 4958
[TakeutiZaring] p. 25Exercise 6reluni 4964
[TakeutiZaring] p. 25Exercise 9inxp 4974
[TakeutiZaring] p. 25Exercise 12relres 5141
[TakeutiZaring] p. 25Exercise 13opelres 5118  opelresg 5120
[TakeutiZaring] p. 25Exercise 14dmres 5134
[TakeutiZaring] p. 25Exercise 15resss 5137
[TakeutiZaring] p. 25Exercise 17resabs1 5142
[TakeutiZaring] p. 25Exercise 18funres 5459
[TakeutiZaring] p. 25Exercise 24relco 5335
[TakeutiZaring] p. 25Exercise 29funco 5458
[TakeutiZaring] p. 25Exercise 30f1co 5615
[TakeutiZaring] p. 26Definition 6.10eu2 2287
[TakeutiZaring] p. 26Definition 6.11conventions 21671  df-fv 5429  fv3 5711
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5373  cnvexg 5372
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5099  dmexg 5097
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5100  rnexg 5098
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27533
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27534
[TakeutiZaring] p. 27Corollary 6.13fvex 5709
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 27913  tz6.12-1 5714  tz6.12-afv 27912  tz6.12 5715  tz6.12c 5717
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5686  tz6.12i 5718
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5424
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5425
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5427  wfo 5419
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5426  wf1 5418
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5428  wf1o 5420
[TakeutiZaring] p. 28Exercise 4eqfnfv 5794  eqfnfv2 5795  eqfnfv2f 5798
[TakeutiZaring] p. 28Exercise 5fvco 5766
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5928  fnexALT 5929
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5924  resfunexgALT 5925
[TakeutiZaring] p. 29Exercise 9funimaex 5498  funimaexg 5497
[TakeutiZaring] p. 29Definition 6.18df-br 4181
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4472
[TakeutiZaring] p. 30Definition 6.21dffr2 4515  dffr3 5203  eliniseg 5200  iniseg 5202
[TakeutiZaring] p. 30Definition 6.22df-eprel 4462
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4528  fr3nr 4727  frirr 4527
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4509
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4729
[TakeutiZaring] p. 31Exercise 1frss 4517
[TakeutiZaring] p. 31Exercise 4wess 4537
[TakeutiZaring] p. 31Proposition 6.26tz6.26 25427  tz6.26i 25428  wefrc 4544  wereu2 4547
[TakeutiZaring] p. 32Theorem 6.27wfi 25429  wfii 25430
[TakeutiZaring] p. 32Definition 6.28df-isom 5430
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6016
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6017
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6023
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6024
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6025
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6029
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6036
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6038
[TakeutiZaring] p. 35Notationwtr 4270
[TakeutiZaring] p. 35Theorem 7.2trelpss 27535  tz7.2 4534
[TakeutiZaring] p. 35Definition 7.1dftr3 4274
[TakeutiZaring] p. 36Proposition 7.4ordwe 4562
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4570
[TakeutiZaring] p. 36Proposition 7.6ordelord 4571  ordelordALT 28341  ordelordALTVD 28697
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4577  ordelssne 4576
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4575
[TakeutiZaring] p. 37Proposition 7.9ordin 4579
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4736
[TakeutiZaring] p. 38Corollary 7.15ordsson 4737
[TakeutiZaring] p. 38Definition 7.11df-on 4553
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4581
[TakeutiZaring] p. 38Proposition 7.12onfrALT 28354  ordon 4730
[TakeutiZaring] p. 38Proposition 7.13onprc 4732
[TakeutiZaring] p. 39Theorem 7.17tfi 4800
[TakeutiZaring] p. 40Exercise 3ontr2 4596
[TakeutiZaring] p. 40Exercise 7dftr2 4272
[TakeutiZaring] p. 40Exercise 9onssmin 4744
[TakeutiZaring] p. 40Exercise 11unon 4778
[TakeutiZaring] p. 40Exercise 12ordun 4650
[TakeutiZaring] p. 40Exercise 14ordequn 4649
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4733
[TakeutiZaring] p. 40Proposition 7.20elssuni 4011
[TakeutiZaring] p. 41Definition 7.22df-suc 4555
[TakeutiZaring] p. 41Proposition 7.23sssucid 4626  sucidg 4627
[TakeutiZaring] p. 41Proposition 7.24suceloni 4760
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4640  ordnbtwn 4639
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4775
[TakeutiZaring] p. 42Exercise 1df-lim 4554
[TakeutiZaring] p. 42Exercise 4omssnlim 4826
[TakeutiZaring] p. 42Exercise 7ssnlim 4830
[TakeutiZaring] p. 42Exercise 8onsucssi 4788  ordelsuc 4767
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4769
[TakeutiZaring] p. 42Definition 7.27nlimon 4798
[TakeutiZaring] p. 42Definition 7.28dfom2 4814
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4831
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4832
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4833
[TakeutiZaring] p. 43Remarkomon 4823
[TakeutiZaring] p. 43Axiom 7inf3 7554  omex 7562
[TakeutiZaring] p. 43Theorem 7.32ordom 4821
[TakeutiZaring] p. 43Corollary 7.31find 4837
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4834
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4835
[TakeutiZaring] p. 44Exercise 1limomss 4817
[TakeutiZaring] p. 44Exercise 2int0 4032  trint0 4287
[TakeutiZaring] p. 44Exercise 4intss1 4033
[TakeutiZaring] p. 44Exercise 5intex 4324
[TakeutiZaring] p. 44Exercise 6oninton 4747
[TakeutiZaring] p. 44Exercise 11ordintdif 4598
[TakeutiZaring] p. 44Definition 7.35df-int 4019
[TakeutiZaring] p. 44Proposition 7.34noinfep 7578
[TakeutiZaring] p. 45Exercise 4onint 4742
[TakeutiZaring] p. 47Lemma 1tfrlem1 6603
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6625
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6626
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6627
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6631  tz7.44-2 6632  tz7.44-3 6633
[TakeutiZaring] p. 50Exercise 1smogt 6596
[TakeutiZaring] p. 50Exercise 3smoiso 6591
[TakeutiZaring] p. 50Definition 7.46df-smo 6575
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6669  tz7.49c 6670
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6667
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6666
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6668
[TakeutiZaring] p. 53Proposition 7.532eu5 2346
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7857
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7858
[TakeutiZaring] p. 56Definition 8.1oalim 6743  oasuc 6735
[TakeutiZaring] p. 57Remarktfindsg 4807
[TakeutiZaring] p. 57Proposition 8.2oacl 6746
[TakeutiZaring] p. 57Proposition 8.3oa0 6727  oa0r 6749
[TakeutiZaring] p. 57Proposition 8.16omcl 6747
[TakeutiZaring] p. 58Corollary 8.5oacan 6758
[TakeutiZaring] p. 58Proposition 8.4nnaord 6829  nnaordi 6828  oaord 6757  oaordi 6756
[TakeutiZaring] p. 59Proposition 8.6iunss2 4104  uniss2 4014
[TakeutiZaring] p. 59Proposition 8.7oawordri 6760
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6765  oawordex 6767
[TakeutiZaring] p. 59Proposition 8.9nnacl 6821
[TakeutiZaring] p. 59Proposition 8.10oaabs 6854
[TakeutiZaring] p. 60Remarkoancom 7570
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6770
[TakeutiZaring] p. 62Exercise 1nnarcl 6826
[TakeutiZaring] p. 62Exercise 5oaword1 6762
[TakeutiZaring] p. 62Definition 8.15om0 6728  om0x 6730  omlim 6744  omsuc 6737
[TakeutiZaring] p. 63Proposition 8.17nnecl 6823  nnmcl 6822
[TakeutiZaring] p. 63Proposition 8.19nnmord 6842  nnmordi 6841  omord 6778  omordi 6776
[TakeutiZaring] p. 63Proposition 8.20omcan 6779
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6846  omwordri 6782
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6750
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6752  om1r 6753
[TakeutiZaring] p. 64Proposition 8.22om00 6785
[TakeutiZaring] p. 64Proposition 8.23omordlim 6787
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6788
[TakeutiZaring] p. 64Proposition 8.25odi 6789
[TakeutiZaring] p. 65Theorem 8.26omass 6790
[TakeutiZaring] p. 67Definition 8.30nnesuc 6818  oe0 6733  oelim 6745  oesuc 6738  onesuc 6741
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6731
[TakeutiZaring] p. 67Proposition 8.32oen0 6796
[TakeutiZaring] p. 67Proposition 8.33oeordi 6797
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6732
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6755
[TakeutiZaring] p. 68Corollary 8.34oeord 6798
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6804
[TakeutiZaring] p. 68Proposition 8.35oewordri 6802
[TakeutiZaring] p. 68Proposition 8.37oeworde 6803
[TakeutiZaring] p. 69Proposition 8.41oeoa 6807
[TakeutiZaring] p. 70Proposition 8.42oeoe 6809
[TakeutiZaring] p. 73Theorem 9.1trcl 7628  tz9.1 7629
[TakeutiZaring] p. 76Definition 9.9df-r1 7654  r10 7658  r1lim 7662  r1limg 7661  r1suc 7660  r1sucg 7659
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7670  r1ord2 7671  r1ordg 7668
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7680
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7705  tz9.13 7681  tz9.13g 7682
[TakeutiZaring] p. 79Definition 9.14df-rank 7655  rankval 7706  rankvalb 7687  rankvalg 7707
[TakeutiZaring] p. 79Proposition 9.16rankel 7729  rankelb 7714
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7743  rankval3 7730  rankval3b 7716
[TakeutiZaring] p. 79Proposition 9.18rankonid 7719
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7685
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7724  rankr1c 7711  rankr1g 7722
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7725
[TakeutiZaring] p. 80Exercise 1rankss 7739  rankssb 7738
[TakeutiZaring] p. 80Exercise 2unbndrank 7732
[TakeutiZaring] p. 80Proposition 9.19bndrank 7731
[TakeutiZaring] p. 83Axiom of Choiceac4 8319  dfac3 7966
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7875  numth 8316  numth2 8315
[TakeutiZaring] p. 85Definition 10.4cardval 8385
[TakeutiZaring] p. 85Proposition 10.5cardid 8386  cardid2 7804
[TakeutiZaring] p. 85Proposition 10.9oncard 7811
[TakeutiZaring] p. 85Proposition 10.10carden 8390
[TakeutiZaring] p. 85Proposition 10.11cardidm 7810
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7795
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7816
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7808
[TakeutiZaring] p. 87Proposition 10.15pwen 7247
[TakeutiZaring] p. 88Exercise 1en0 7137
[TakeutiZaring] p. 88Exercise 7infensuc 7252
[TakeutiZaring] p. 89Exercise 10omxpen 7177
[TakeutiZaring] p. 90Corollary 10.23cardnn 7814
[TakeutiZaring] p. 90Definition 10.27alephiso 7943
[TakeutiZaring] p. 90Proposition 10.20nneneq 7257
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7263
[TakeutiZaring] p. 90Proposition 10.26alephprc 7944
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7262
[TakeutiZaring] p. 91Exercise 2alephle 7933
[TakeutiZaring] p. 91Exercise 3aleph0 7911
[TakeutiZaring] p. 91Exercise 4cardlim 7823
[TakeutiZaring] p. 91Exercise 7infpss 8061
[TakeutiZaring] p. 91Exercise 8infcntss 7347
[TakeutiZaring] p. 91Definition 10.29df-fin 7080  isfi 7098
[TakeutiZaring] p. 92Proposition 10.32onfin 7264
[TakeutiZaring] p. 92Proposition 10.34imadomg 8376
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 7170
[TakeutiZaring] p. 93Proposition 10.35fodomb 8368
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8033  unxpdom 7283
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7825  cardsdomelir 7824
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7285
[TakeutiZaring] p. 94Proposition 10.39infxpen 7860
[TakeutiZaring] p. 95Definition 10.42df-map 6987
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8401  infxpidm2 7862
[TakeutiZaring] p. 95Proposition 10.41infcda 8052  infxp 8059
[TakeutiZaring] p. 96Proposition 10.44pw2en 7182  pw2f1o 7180
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7240
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8331
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8326  ac6s5 8335
[TakeutiZaring] p. 98Theorem 10.47unidom 8382
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8383  uniimadomf 8384
[TakeutiZaring] p. 100Definition 11.1cfcof 8118
[TakeutiZaring] p. 101Proposition 11.7cofsmo 8113
[TakeutiZaring] p. 102Exercise 1cfle 8098
[TakeutiZaring] p. 102Exercise 2cf0 8095
[TakeutiZaring] p. 102Exercise 3cfsuc 8101
[TakeutiZaring] p. 102Exercise 4cfom 8108
[TakeutiZaring] p. 102Proposition 11.9coftr 8117
[TakeutiZaring] p. 103Theorem 11.15alephreg 8421
[TakeutiZaring] p. 103Proposition 11.11cardcf 8096
[TakeutiZaring] p. 103Proposition 11.13alephsing 8120
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7942
[TakeutiZaring] p. 104Proposition 11.16carduniima 7941
[TakeutiZaring] p. 104Proposition 11.18alephfp 7953  alephfp2 7954
[TakeutiZaring] p. 106Theorem 11.20gchina 8538
[TakeutiZaring] p. 106Theorem 11.21mappwen 7957
[TakeutiZaring] p. 107Theorem 11.26konigth 8408
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8422
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8423
[Tarski] p. 67Axiom B5ax-4 2193
[Tarski] p. 67Scheme B5sp 1759
[Tarski] p. 68Lemma 6avril1 21718  equid 1684  equid1 2216  equid1ALT 2234
[Tarski] p. 69Lemma 7equcomi 1687
[Tarski] p. 70Lemma 14spim 1955  spime 1960  spimeh 1675
[Tarski] p. 70Lemma 16ax-11 1757  ax-11o 2199  ax11i 1654
[Tarski] p. 70Lemmas 16 and 17sb6 2156
[Tarski] p. 75Axiom B7ax9v 1663
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1623  ax17o 2215
[Tarski], p. 75Scheme B8 of system S2ax-13 1723  ax-14 1725  ax-8 1683
[Truss] p. 114Theorem 5.18ruc 12805
[Viaclovsky7] p. 3Proposition 0.3mblfinlem2 26152
[Viaclovsky8] p. 3Proposition 7ismblfin 26154
[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 2359  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 28757
[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 21671  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 26142
[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 26135
[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 27429
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27430
[WhiteheadRussell] p. 147Theorem *10.2219.26 1600
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27431
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27432
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27433
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1622
[WhiteheadRussell] p. 151Theorem *10.301albitr 27434
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27435
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27436
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27437
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27438
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27440
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27441
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27442
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27439
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2172
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27445
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27446
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27447
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1749
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27448
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27449
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27450
[WhiteheadRussell] p. 162Theorem *11.322alim 27451
[WhiteheadRussell] p. 162Theorem *11.332albi 27452
[WhiteheadRussell] p. 162Theorem *11.342exim 27453
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27455
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27454
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1617
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27457
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27458
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27456
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1579
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27459
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27460
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1587
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27461
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1912
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27462
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27467
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27463
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27464
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27465
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27466
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27471
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27468
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27469
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27470
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27472
[WhiteheadRussell] p. 175Definition *14.02df-eu 2266
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27483  pm13.13b 27484
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27485
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2647
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2648
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3044
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27491
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27492
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27486
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 28358  pm13.193 27487
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27488
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27489
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27490
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27497
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27496
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27495
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3181
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27498  pm14.122b 27499  pm14.122c 27500
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27501  pm14.123b 27502  pm14.123c 27503
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27505
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27504
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27506
[WhiteheadRussell] p. 190Theorem *14.22iota4 5403
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27507
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5404
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27508
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27510
[WhiteheadRussell] p. 192Theorem *14.26eupick 2325  eupickbi 2328  sbaniota 27511
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27509
[WhiteheadRussell] p. 192Theorem *14.271eubi 27512
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27513
[WhiteheadRussell] p. 235Definition *30.01conventions 21671  df-fv 5429
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7851  pm54.43lem 7850
[Young] p. 141Definition of operator orderingleop2 23588
[Young] p. 142Example 12.2(i)0leop 23594  idleop 23595
[vandenDries] p. 42Lemma 61irrapx1 26789
[vandenDries] p. 43Theorem 62pellex 26796  pellexlem1 26790

This page was last updated on 23-Apr-2018.
Copyright terms: Public domain