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 13964
[Adamek] p. 29Proposition 3.14(1)invinv 13978
[Adamek] p. 29Proposition 3.14(2)invco 13979  isoco 13981
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18725  df-nmoo 22229
[AkhiezerGlazman] p. 64Theoremhmopidmch 23639  hmopidmchi 23637
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 23687  pjcmul2i 23688
[AkhiezerGlazman] p. 72Theoremcnvunop 23404  unoplin 23406
[AkhiezerGlazman] p. 72Equation 2unopadj 23405  unopadj2 23424
[AkhiezerGlazman] p. 73Theoremelunop2 23499  lnopunii 23498
[AkhiezerGlazman] p. 80Proposition 1adjlnop 23572
[Apostol] p. 18Theorem I.1addcan 9234  addcan2d 9254  addcan2i 9244  addcand 9253  addcani 9243
[Apostol] p. 18Theorem I.2negeu 9280
[Apostol] p. 18Theorem I.3negsub 9333  negsubd 9401  negsubi 9362
[Apostol] p. 18Theorem I.4negneg 9335  negnegd 9386  negnegi 9354
[Apostol] p. 18Theorem I.5subdi 9451  subdid 9473  subdii 9466  subdir 9452  subdird 9474  subdiri 9467
[Apostol] p. 18Theorem I.6mul01 9229  mul01d 9249  mul01i 9240  mul02 9228  mul02d 9248  mul02i 9239
[Apostol] p. 18Theorem I.7mulcan 9643  mulcan2d 9640  mulcand 9639  mulcani 9645
[Apostol] p. 18Theorem I.8receu 9651  xreceu 24151
[Apostol] p. 18Theorem I.9divrec 9678  divrecd 9777  divreci 9743  divreczi 9736
[Apostol] p. 18Theorem I.10recrec 9695  recreci 9730
[Apostol] p. 18Theorem I.11mul0or 9646  mul0ord 9656  mul0ori 9654
[Apostol] p. 18Theorem I.12mul2neg 9457  mul2negd 9472  mul2negi 9465  mulneg1 9454  mulneg1d 9470  mulneg1i 9463
[Apostol] p. 18Theorem I.13divadddiv 9713  divadddivd 9818  divadddivi 9760
[Apostol] p. 18Theorem I.14divmuldiv 9698  divmuldivd 9815  divmuldivi 9758  rdivmuldivd 24210
[Apostol] p. 18Theorem I.15divdivdiv 9699  divdivdivd 9821  divdivdivi 9761
[Apostol] p. 20Axiom 7rpaddcl 10616  rpaddcld 10647  rpmulcl 10617  rpmulcld 10648
[Apostol] p. 20Axiom 8rpneg 10625
[Apostol] p. 20Axiom 90nrp 10626
[Apostol] p. 20Theorem I.17lttri 9183
[Apostol] p. 20Theorem I.18ltadd1d 9603  ltadd1dd 9621  ltadd1i 9565
[Apostol] p. 20Theorem I.19ltmul1 9844  ltmul1a 9843  ltmul1i 9913  ltmul1ii 9923  ltmul2 9845  ltmul2d 10670  ltmul2dd 10684  ltmul2i 9916
[Apostol] p. 20Theorem I.20msqgt0 9532  msqgt0d 9578  msqgt0i 9548
[Apostol] p. 20Theorem I.210lt1 9534
[Apostol] p. 20Theorem I.23lt0neg1 9518  lt0neg1d 9580  ltneg 9512  ltnegd 9588  ltnegi 9555
[Apostol] p. 20Theorem I.25lt2add 9497  lt2addd 9632  lt2addi 9573
[Apostol] p. 20Definition of positive numbersdf-rp 10597
[Apostol] p. 21Exercise 4recgt0 9838  recgt0d 9929  recgt0i 9899  recgt0ii 9900
[Apostol] p. 22Definition of integersdf-z 10267
[Apostol] p. 22Definition of positive integersdfnn3 9998
[Apostol] p. 22Definition of rationalsdf-q 10559
[Apostol] p. 24Theorem I.26supeu 7443
[Apostol] p. 26Theorem I.28nnunb 10201
[Apostol] p. 26Theorem I.29arch 10202
[Apostol] p. 28Exercise 2btwnz 10356
[Apostol] p. 28Exercise 3nnrecl 10203
[Apostol] p. 28Exercise 4rebtwnz 10557
[Apostol] p. 28Exercise 5zbtwnre 10556
[Apostol] p. 28Exercise 6qbtwnre 10769
[Apostol] p. 28Exercise 10(a)zneo 10336
[Apostol] p. 29Theorem I.35msqsqrd 12225  resqrth 12044  sqrth 12151  sqrthi 12157  sqsqrd 12224
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9987
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10526
[Apostol] p. 361Remarkcrreczi 11487
[Apostol] p. 363Remarkabsgt0i 12185
[Apostol] p. 363Exampleabssubd 12238  abssubi 12189
[Baer] p. 40Property (b)mapdord 32167
[Baer] p. 40Property (c)mapd11 32168
[Baer] p. 40Property (e)mapdin 32191  mapdlsm 32193
[Baer] p. 40Property (f)mapd0 32194
[Baer] p. 40Definition of projectivitydf-mapd 32154  mapd1o 32177
[Baer] p. 41Property (g)mapdat 32196
[Baer] p. 44Part (1)mapdpg 32235
[Baer] p. 45Part (2)hdmap1eq 32331  mapdheq 32257  mapdheq2 32258  mapdheq2biN 32259
[Baer] p. 45Part (3)baerlem3 32242
[Baer] p. 46Part (4)mapdheq4 32261  mapdheq4lem 32260
[Baer] p. 46Part (5)baerlem5a 32243  baerlem5abmN 32247  baerlem5amN 32245  baerlem5b 32244  baerlem5bmN 32246
[Baer] p. 47Part (6)hdmap1l6 32351  hdmap1l6a 32339  hdmap1l6e 32344  hdmap1l6f 32345  hdmap1l6g 32346  hdmap1l6lem1 32337  hdmap1l6lem2 32338  hdmap1p6N 32352  mapdh6N 32276  mapdh6aN 32264  mapdh6eN 32269  mapdh6fN 32270  mapdh6gN 32271  mapdh6lem1N 32262  mapdh6lem2N 32263
[Baer] p. 48Part 9hdmapval 32360
[Baer] p. 48Part 10hdmap10 32372
[Baer] p. 48Part 11hdmapadd 32375
[Baer] p. 48Part (6)hdmap1l6h 32347  mapdh6hN 32272
[Baer] p. 48Part (7)mapdh75cN 32282  mapdh75d 32283  mapdh75e 32281  mapdh75fN 32284  mapdh7cN 32278  mapdh7dN 32279  mapdh7eN 32277  mapdh7fN 32280
[Baer] p. 48Part (8)mapdh8 32318  mapdh8a 32304  mapdh8aa 32305  mapdh8ab 32306  mapdh8ac 32307  mapdh8ad 32308  mapdh8b 32309  mapdh8c 32310  mapdh8d 32312  mapdh8d0N 32311  mapdh8e 32313  mapdh8fN 32314  mapdh8g 32315  mapdh8i 32316  mapdh8j 32317
[Baer] p. 48Part (9)mapdh9a 32319
[Baer] p. 48Equation 10mapdhvmap 32298
[Baer] p. 49Part 12hdmap11 32380  hdmapeq0 32376  hdmapf1oN 32397  hdmapneg 32378  hdmaprnN 32396  hdmaprnlem1N 32381  hdmaprnlem3N 32382  hdmaprnlem3uN 32383  hdmaprnlem4N 32385  hdmaprnlem6N 32386  hdmaprnlem7N 32387  hdmaprnlem8N 32388  hdmaprnlem9N 32389  hdmapsub 32379
[Baer] p. 49Part 14hdmap14lem1 32400  hdmap14lem10 32409  hdmap14lem1a 32398  hdmap14lem2N 32401  hdmap14lem2a 32399  hdmap14lem3 32402  hdmap14lem8 32407  hdmap14lem9 32408
[Baer] p. 50Part 14hdmap14lem11 32410  hdmap14lem12 32411  hdmap14lem13 32412  hdmap14lem14 32413  hdmap14lem15 32414  hgmapval 32419
[Baer] p. 50Part 15hgmapadd 32426  hgmapmul 32427  hgmaprnlem2N 32429  hgmapvs 32423
[Baer] p. 50Part 16hgmaprnN 32433
[Baer] p. 110Lemma 1hdmapip0com 32449
[Baer] p. 110Line 27hdmapinvlem1 32450
[Baer] p. 110Line 28hdmapinvlem2 32451
[Baer] p. 110Line 30hdmapinvlem3 32452
[Baer] p. 110Part 1.2hdmapglem5 32454  hgmapvv 32458
[Baer] p. 110Proposition 1hdmapinvlem4 32453
[Baer] p. 111Line 10hgmapvvlem1 32455
[Baer] p. 111Line 15hdmapg 32462  hdmapglem7 32461
[BellMachover] p. 36Lemma 10.3id1 21
[BellMachover] p. 97Definition 10.1df-eu 2284
[BellMachover] p. 460Notationdf-mo 2285
[BellMachover] p. 460Definitionmo3 2311
[BellMachover] p. 461Axiom Extax-ext 2411
[BellMachover] p. 462Theorem 1.1bm1.1 2415
[BellMachover] p. 463Axiom Repaxrep5 4312
[BellMachover] p. 463Scheme Sepaxsep 4316
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4320
[BellMachover] p. 466Axiom Powaxpow3 4367
[BellMachover] p. 466Axiom Unionaxun2 4689
[BellMachover] p. 468Definitiondf-ord 4571
[BellMachover] p. 469Theorem 2.2(i)ordirr 4586
[BellMachover] p. 469Theorem 2.2(iii)onelon 4593
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4588
[BellMachover] p. 471Definition of Ndf-om 4832
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4772
[BellMachover] p. 471Definition of Limdf-lim 4573
[BellMachover] p. 472Axiom Infzfinf2 7581
[BellMachover] p. 473Theorem 2.8limom 4846
[BellMachover] p. 477Equation 3.1df-r1 7674
[BellMachover] p. 478Definitionrankval2 7728
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7692  r1ord3g 7689
[BellMachover] p. 480Axiom Regzfreg2 7548
[BellMachover] p. 488Axiom ACac5 8341  dfac4 7987
[BellMachover] p. 490Definition of alephalephval3 7975
[BeltramettiCassinelli] p. 98Remarkatlatmstc 29848
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 23839
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 23881  chirredi 23880
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 23869
[Beran] p. 3Definition of joinsshjval3 22839
[Beran] p. 39Theorem 2.3(i)cmcm2 23101  cmcm2i 23078  cmcm2ii 23083  cmt2N 29779
[Beran] p. 40Theorem 2.3(iii)lecm 23102  lecmi 23087  lecmii 23088
[Beran] p. 45Theorem 3.4cmcmlem 23076
[Beran] p. 49Theorem 4.2cm2j 23105  cm2ji 23110  cm2mi 23111
[Beran] p. 95Definitiondf-sh 22692  issh2 22694
[Beran] p. 95Lemma 3.1(S5)his5 22571
[Beran] p. 95Lemma 3.1(S6)his6 22584
[Beran] p. 95Lemma 3.1(S7)his7 22575
[Beran] p. 95Lemma 3.2(S8)ho01i 23314
[Beran] p. 95Lemma 3.2(S9)hoeq1 23316
[Beran] p. 95Lemma 3.2(S10)ho02i 23315
[Beran] p. 95Lemma 3.2(S11)hoeq2 23317
[Beran] p. 95Postulate (S1)ax-his1 22567  his1i 22585
[Beran] p. 95Postulate (S2)ax-his2 22568
[Beran] p. 95Postulate (S3)ax-his3 22569
[Beran] p. 95Postulate (S4)ax-his4 22570
[Beran] p. 96Definition of normdf-hnorm 22454  dfhnorm2 22607  normval 22609
[Beran] p. 96Definition for Cauchy sequencehcau 22669
[Beran] p. 96Definition of Cauchy sequencedf-hcau 22459
[Beran] p. 96Definition of complete subspaceisch3 22727
[Beran] p. 96Definition of convergedf-hlim 22458  hlimi 22673
[Beran] p. 97Theorem 3.3(i)norm-i-i 22618  norm-i 22614
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 22622  norm-ii 22623  normlem0 22594  normlem1 22595  normlem2 22596  normlem3 22597  normlem4 22598  normlem5 22599  normlem6 22600  normlem7 22601  normlem7tALT 22604
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 22624  norm-iii 22625
[Beran] p. 98Remark 3.4bcs 22666  bcsiALT 22664  bcsiHIL 22665
[Beran] p. 98Remark 3.4(B)normlem9at 22606  normpar 22640  normpari 22639
[Beran] p. 98Remark 3.4(C)normpyc 22631  normpyth 22630  normpythi 22627
[Beran] p. 99Remarklnfn0 23533  lnfn0i 23528  lnop0 23452  lnop0i 23456
[Beran] p. 99Theorem 3.5(i)nmcexi 23512  nmcfnex 23539  nmcfnexi 23537  nmcopex 23515  nmcopexi 23513
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 23540  nmcfnlbi 23538  nmcoplb 23516  nmcoplbi 23514
[Beran] p. 99Theorem 3.5(iii)lnfncon 23542  lnfnconi 23541  lnopcon 23521  lnopconi 23520
[Beran] p. 100Lemma 3.6normpar2i 22641
[Beran] p. 101Lemma 3.6norm3adifi 22638  norm3adifii 22633  norm3dif 22635  norm3difi 22632
[Beran] p. 102Theorem 3.7(i)chocunii 22786  pjhth 22878  pjhtheu 22879  pjpjhth 22910  pjpjhthi 22911  pjth 19323
[Beran] p. 102Theorem 3.7(ii)ococ 22891  ococi 22890
[Beran] p. 103Remark 3.8nlelchi 23547
[Beran] p. 104Theorem 3.9riesz3i 23548  riesz4 23550  riesz4i 23549
[Beran] p. 104Theorem 3.10cnlnadj 23565  cnlnadjeu 23564  cnlnadjeui 23563  cnlnadji 23562  cnlnadjlem1 23553  nmopadjlei 23574
[Beran] p. 106Theorem 3.11(i)adjeq0 23577
[Beran] p. 106Theorem 3.11(v)nmopadji 23576
[Beran] p. 106Theorem 3.11(ii)adjmul 23578
[Beran] p. 106Theorem 3.11(iv)adjadj 23422
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 23588  nmopcoadji 23587
[Beran] p. 106Theorem 3.11(iii)adjadd 23579
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 23589
[Beran] p. 106Theorem 3.11(viii)adjcoi 23586  pjadj2coi 23690  pjadjcoi 23647
[Beran] p. 107Definitiondf-ch 22707  isch2 22709
[Beran] p. 107Remark 3.12choccl 22791  isch3 22727  occl 22789  ocsh 22768  shoccl 22790  shocsh 22769
[Beran] p. 107Remark 3.12(B)ococin 22893
[Beran] p. 108Theorem 3.13chintcl 22817
[Beran] p. 109Property (i)pjadj2 23673  pjadj3 23674  pjadji 23170  pjadjii 23159
[Beran] p. 109Property (ii)pjidmco 23667  pjidmcoi 23663  pjidmi 23158
[Beran] p. 110Definition of projector orderingpjordi 23659
[Beran] p. 111Remarkho0val 23236  pjch1 23155
[Beran] p. 111Definitiondf-hfmul 23220  df-hfsum 23219  df-hodif 23218  df-homul 23217  df-hosum 23216
[Beran] p. 111Lemma 4.4(i)pjo 23156
[Beran] p. 111Lemma 4.4(ii)pjch 23179  pjchi 22917
[Beran] p. 111Lemma 4.4(iii)pjoc2 22924  pjoc2i 22923
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 23165
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 23651  pjssmii 23166
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 23650
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 23649
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 23654
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 23652  pjssge0ii 23167
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 23653  pjdifnormii 23168
[Bogachev] p. 116Definition 2.3.1df-itgm 24647  df-sitm 24629
[Bogachev] p. 118Chapter 2.4.4df-itgm 24647
[Bogachev] p. 118Definition 2.4.1df-sitg 24628
[Bollobas] p. 4Definitiondf-wlk 21499
[Bollobas] p. 5Notationdf-pth 21501
[Bollobas] p. 5Definitiondf-crct 21503  df-cycl 21504  df-trail 21500  df-wlkon 21505
[BourbakiEns] p. Proposition 8fcof1 6006  fcofo 6007
[BourbakiTop1] p. Remarkxnegmnf 10780  xnegpnf 10779
[BourbakiTop1] p. Remark rexneg 10781
[BourbakiTop1] p. Theoremneiss 17156
[BourbakiTop1] p. Remark 3ust0 18232  ustfilxp 18225
[BourbakiTop1] p. Axiom GT'tgpsubcn 18103
[BourbakiTop1] p. Example 1cstucnd 18297  iducn 18296  snfil 17879
[BourbakiTop1] p. Example 2neifil 17895
[BourbakiTop1] p. Theorem 1cnextcn 18081
[BourbakiTop1] p. Theorem 2ucnextcn 18317
[BourbakiTop1] p. Theorem 3df-hcmp 24324
[BourbakiTop1] p. Definitionistgp 18090
[BourbakiTop1] p. Propositioncnpco 17314  ishmeo 17774  neips 17160
[BourbakiTop1] p. Definition 1df-ucn 18289  df-ust 18213  filintn0 17876  ucnprima 18295
[BourbakiTop1] p. Definition 2df-cfilu 18300
[BourbakiTop1] p. Definition 3df-cusp 18311  df-usp 18270  df-utop 18244  trust 18242
[BourbakiTop1] p. Condition F_Iustssel 18218
[BourbakiTop1] p. Condition U_Iustdiag 18221
[BourbakiTop1] p. Property V_ivneiptopreu 17180
[BourbakiTop1] p. Proposition 1ucncn 18298  ustund 18234  ustuqtop 18259
[BourbakiTop1] p. Proposition 2neiptopreu 17180  utop2nei 18263  utop3cls 18264
[BourbakiTop1] p. Proposition 3fmucnd 18305  uspreg 18287  utopreg 18265
[BourbakiTop1] p. Proposition 4imasncld 17706  imasncls 17707  imasnopn 17705
[BourbakiTop1] p. Proposition 9cnpflf2 18015
[BourbakiTop1] p. Theorem 1 (d)iscncl 17316
[BourbakiTop1] p. Condition F_IIustincl 18220
[BourbakiTop1] p. Condition U_IIustinvel 18222
[BourbakiTop1] p. Proposition 11cnextucn 18316
[BourbakiTop1] p. Proposition Vissnei2 17163
[BourbakiTop1] p. Condition F_IIbustbasel 18219
[BourbakiTop1] p. Condition U_IIIustexhalf 18223
[BourbakiTop1] p. Definition C'''df-cmp 17433
[BourbakiTop1] p. Proposition Viiinnei 17172
[BourbakiTop1] p. Proposition Vivneissex 17174
[BourbakiTop1] p. Proposition Viiielnei 17158  ssnei 17157
[BourbakiTop1] p. Remark below def. 1filn0 17877
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17861
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17878
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27722  stoweid 27721
[BrosowskiDeutsh] p. 89Theorem for the non-trivial casestoweidlem62 27720
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27659  stoweidlem10 27668  stoweidlem14 27672  stoweidlem15 27673  stoweidlem35 27693  stoweidlem36 27694  stoweidlem37 27695  stoweidlem38 27696  stoweidlem40 27698  stoweidlem41 27699  stoweidlem43 27701  stoweidlem44 27702  stoweidlem46 27704  stoweidlem5 27663  stoweidlem50 27708  stoweidlem52 27710  stoweidlem53 27711  stoweidlem55 27713  stoweidlem56 27714
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27681  stoweidlem24 27682  stoweidlem27 27685  stoweidlem28 27686  stoweidlem30 27688
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27703  stoweidlem49 27707  stoweidlem7 27665
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27689  stoweidlem39 27697  stoweidlem42 27700  stoweidlem48 27706  stoweidlem51 27709  stoweidlem54 27712  stoweidlem57 27715  stoweidlem58 27716
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27683
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27692
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27675
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27717
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27718
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27676
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27669  stoweidlem26 27684
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27671
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27719
[ChoquetDD] p. 2Definition of mappingdf-mpt 4255
[Clemente] p. 10Definition ITnatded 21694
[Clemente] p. 10Definition I` `m,nnatded 21694
[Clemente] p. 11Definition E=>m,nnatded 21694
[Clemente] p. 11Definition I=>m,nnatded 21694
[Clemente] p. 11Definition E` `(1)natded 21694
[Clemente] p. 11Definition E` `(2)natded 21694
[Clemente] p. 12Definition E` `m,n,pnatded 21694
[Clemente] p. 12Definition I` `n(1)natded 21694
[Clemente] p. 12Definition I` `n(2)natded 21694
[Clemente] p. 13Definition I` `m,n,pnatded 21694
[Clemente] p. 14Definition E` `nnatded 21694
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 21696  ex-natded5.2 21695
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 21699  ex-natded5.3 21698
[Clemente] p. 18Theorem 5.5ex-natded5.5 21701
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 21703  ex-natded5.7 21702
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 21705  ex-natded5.8 21704
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 21707  ex-natded5.13 21706
[Clemente] p. 32Definition I` `nnatded 21694
[Clemente] p. 32Definition E` `m,n,p,anatded 21694
[Clemente] p. 32Definition E` `n,tnatded 21694
[Clemente] p. 32Definition I` `n,tnatded 21694
[Clemente] p. 43Theorem 9.20ex-natded9.20 21708
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 21709
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 21711  ex-natded9.26 21710
[Cohen] p. 301Remarkrelogoprlem 20468
[Cohen] p. 301Property 2relogmul 20469  relogmuld 20503
[Cohen] p. 301Property 3relogdiv 20470  relogdivd 20504
[Cohen] p. 301Property 4relogexp 20473
[Cohen] p. 301Property 1alog1 20463
[Cohen] p. 301Property 1bloge 20464
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 24618  sxbrsigalem4 24620
[Cohn] p. 81Section II.5acsdomd 14590  acsinfd 14589  acsinfdimd 14591  acsmap2d 14588  acsmapd 14587
[Cohn] p. 143Example 5.1.1sxbrsiga 24623
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 11225
[Crawley] p. 1Definition of posetdf-poset 14386
[Crawley] p. 107Theorem 13.2hlsupr 29914
[Crawley] p. 110Theorem 13.3arglem1N 30718  dalaw 30414
[Crawley] p. 111Theorem 13.4hlathil 32493
[Crawley] p. 111Definition of set Wdf-watsN 30518
[Crawley] p. 111Definition of dilationdf-dilN 30634  df-ldil 30632  isldil 30638
[Crawley] p. 111Definition of translationdf-ltrn 30633  df-trnN 30635  isltrn 30647  ltrnu 30649
[Crawley] p. 112Lemma Acdlema1N 30319  cdlema2N 30320  exatleN 29932
[Crawley] p. 112Lemma B1cvrat 30004  cdlemb 30322  cdlemb2 30569  cdlemb3 31134  idltrn 30678  l1cvat 29584  lhpat 30571  lhpat2 30573  lshpat 29585  ltrnel 30667  ltrnmw 30679
[Crawley] p. 112Lemma Ccdlemc1 30719  cdlemc2 30720  ltrnnidn 30702  trlat 30697  trljat1 30694  trljat2 30695  trljat3 30696  trlne 30713  trlnidat 30701  trlnle 30714
[Crawley] p. 112Definition of automorphismdf-pautN 30519
[Crawley] p. 113Lemma Ccdlemc 30725  cdlemc3 30721  cdlemc4 30722
[Crawley] p. 113Lemma Dcdlemd 30735  cdlemd1 30726  cdlemd2 30727  cdlemd3 30728  cdlemd4 30729  cdlemd5 30730  cdlemd6 30731  cdlemd7 30732  cdlemd8 30733  cdlemd9 30734  cdleme31sde 30913  cdleme31se 30910  cdleme31se2 30911  cdleme31snd 30914  cdleme32a 30969  cdleme32b 30970  cdleme32c 30971  cdleme32d 30972  cdleme32e 30973  cdleme32f 30974  cdleme32fva 30965  cdleme32fva1 30966  cdleme32fvcl 30968  cdleme32le 30975  cdleme48fv 31027  cdleme4gfv 31035  cdleme50eq 31069  cdleme50f 31070  cdleme50f1 31071  cdleme50f1o 31074  cdleme50laut 31075  cdleme50ldil 31076  cdleme50lebi 31068  cdleme50rn 31073  cdleme50rnlem 31072  cdlemeg49le 31039  cdlemeg49lebilem 31067
[Crawley] p. 113Lemma Ecdleme 31088  cdleme00a 30737  cdleme01N 30749  cdleme02N 30750  cdleme0a 30739  cdleme0aa 30738  cdleme0b 30740  cdleme0c 30741  cdleme0cp 30742  cdleme0cq 30743  cdleme0dN 30744  cdleme0e 30745  cdleme0ex1N 30751  cdleme0ex2N 30752  cdleme0fN 30746  cdleme0gN 30747  cdleme0moN 30753  cdleme1 30755  cdleme10 30782  cdleme10tN 30786  cdleme11 30798  cdleme11a 30788  cdleme11c 30789  cdleme11dN 30790  cdleme11e 30791  cdleme11fN 30792  cdleme11g 30793  cdleme11h 30794  cdleme11j 30795  cdleme11k 30796  cdleme11l 30797  cdleme12 30799  cdleme13 30800  cdleme14 30801  cdleme15 30806  cdleme15a 30802  cdleme15b 30803  cdleme15c 30804  cdleme15d 30805  cdleme16 30813  cdleme16aN 30787  cdleme16b 30807  cdleme16c 30808  cdleme16d 30809  cdleme16e 30810  cdleme16f 30811  cdleme16g 30812  cdleme19a 30831  cdleme19b 30832  cdleme19c 30833  cdleme19d 30834  cdleme19e 30835  cdleme19f 30836  cdleme1b 30754  cdleme2 30756  cdleme20aN 30837  cdleme20bN 30838  cdleme20c 30839  cdleme20d 30840  cdleme20e 30841  cdleme20f 30842  cdleme20g 30843  cdleme20h 30844  cdleme20i 30845  cdleme20j 30846  cdleme20k 30847  cdleme20l 30850  cdleme20l1 30848  cdleme20l2 30849  cdleme20m 30851  cdleme20y 30830  cdleme20zN 30829  cdleme21 30865  cdleme21d 30858  cdleme21e 30859  cdleme22a 30868  cdleme22aa 30867  cdleme22b 30869  cdleme22cN 30870  cdleme22d 30871  cdleme22e 30872  cdleme22eALTN 30873  cdleme22f 30874  cdleme22f2 30875  cdleme22g 30876  cdleme23a 30877  cdleme23b 30878  cdleme23c 30879  cdleme26e 30887  cdleme26eALTN 30889  cdleme26ee 30888  cdleme26f 30891  cdleme26f2 30893  cdleme26f2ALTN 30892  cdleme26fALTN 30890  cdleme27N 30897  cdleme27a 30895  cdleme27cl 30894  cdleme28c 30900  cdleme3 30765  cdleme30a 30906  cdleme31fv 30918  cdleme31fv1 30919  cdleme31fv1s 30920  cdleme31fv2 30921  cdleme31id 30922  cdleme31sc 30912  cdleme31sdnN 30915  cdleme31sn 30908  cdleme31sn1 30909  cdleme31sn1c 30916  cdleme31sn2 30917  cdleme31so 30907  cdleme35a 30976  cdleme35b 30978  cdleme35c 30979  cdleme35d 30980  cdleme35e 30981  cdleme35f 30982  cdleme35fnpq 30977  cdleme35g 30983  cdleme35h 30984  cdleme35h2 30985  cdleme35sn2aw 30986  cdleme35sn3a 30987  cdleme36a 30988  cdleme36m 30989  cdleme37m 30990  cdleme38m 30991  cdleme38n 30992  cdleme39a 30993  cdleme39n 30994  cdleme3b 30757  cdleme3c 30758  cdleme3d 30759  cdleme3e 30760  cdleme3fN 30761  cdleme3fa 30764  cdleme3g 30762  cdleme3h 30763  cdleme4 30766  cdleme40m 30995  cdleme40n 30996  cdleme40v 30997  cdleme40w 30998  cdleme41fva11 31005  cdleme41sn3aw 31002  cdleme41sn4aw 31003  cdleme41snaw 31004  cdleme42a 30999  cdleme42b 31006  cdleme42c 31000  cdleme42d 31001  cdleme42e 31007  cdleme42f 31008  cdleme42g 31009  cdleme42h 31010  cdleme42i 31011  cdleme42k 31012  cdleme42ke 31013  cdleme42keg 31014  cdleme42mN 31015  cdleme42mgN 31016  cdleme43aN 31017  cdleme43bN 31018  cdleme43cN 31019  cdleme43dN 31020  cdleme5 30768  cdleme50ex 31087  cdleme50ltrn 31085  cdleme51finvN 31084  cdleme51finvfvN 31083  cdleme51finvtrN 31086  cdleme6 30769  cdleme7 30777  cdleme7a 30771  cdleme7aa 30770  cdleme7b 30772  cdleme7c 30773  cdleme7d 30774  cdleme7e 30775  cdleme7ga 30776  cdleme8 30778  cdleme8tN 30783  cdleme9 30781  cdleme9a 30779  cdleme9b 30780  cdleme9tN 30785  cdleme9taN 30784  cdlemeda 30826  cdlemedb 30825  cdlemednpq 30827  cdlemednuN 30828  cdlemefr27cl 30931  cdlemefr32fva1 30938  cdlemefr32fvaN 30937  cdlemefrs32fva 30928  cdlemefrs32fva1 30929  cdlemefs27cl 30941  cdlemefs32fva1 30951  cdlemefs32fvaN 30950  cdlemesner 30824  cdlemeulpq 30748
[Crawley] p. 114Lemma E4atex 30604  4atexlem7 30603  cdleme0nex 30818  cdleme17a 30814  cdleme17c 30816  cdleme17d 31026  cdleme17d1 30817  cdleme17d2 31023  cdleme18a 30819  cdleme18b 30820  cdleme18c 30821  cdleme18d 30823  cdleme4a 30767
[Crawley] p. 115Lemma Ecdleme21a 30853  cdleme21at 30856  cdleme21b 30854  cdleme21c 30855  cdleme21ct 30857  cdleme21f 30860  cdleme21g 30861  cdleme21h 30862  cdleme21i 30863  cdleme22gb 30822
[Crawley] p. 116Lemma Fcdlemf 31091  cdlemf1 31089  cdlemf2 31090
[Crawley] p. 116Lemma Gcdlemftr1 31095  cdlemg16 31185  cdlemg28 31232  cdlemg28a 31221  cdlemg28b 31231  cdlemg3a 31125  cdlemg42 31257  cdlemg43 31258  cdlemg44 31261  cdlemg44a 31259  cdlemg46 31263  cdlemg47 31264  cdlemg9 31162  ltrnco 31247  ltrncom 31266  tgrpabl 31279  trlco 31255
[Crawley] p. 116Definition of Gdf-tgrp 31271
[Crawley] p. 117Lemma Gcdlemg17 31205  cdlemg17b 31190
[Crawley] p. 117Definition of Edf-edring-rN 31284  df-edring 31285
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 31288
[Crawley] p. 118Remarktendopltp 31308
[Crawley] p. 118Lemma Hcdlemh 31345  cdlemh1 31343  cdlemh2 31344
[Crawley] p. 118Lemma Icdlemi 31348  cdlemi1 31346  cdlemi2 31347
[Crawley] p. 118Lemma Jcdlemj1 31349  cdlemj2 31350  cdlemj3 31351  tendocan 31352
[Crawley] p. 118Lemma Kcdlemk 31502  cdlemk1 31359  cdlemk10 31371  cdlemk11 31377  cdlemk11t 31474  cdlemk11ta 31457  cdlemk11tb 31459  cdlemk11tc 31473  cdlemk11u-2N 31417  cdlemk11u 31399  cdlemk12 31378  cdlemk12u-2N 31418  cdlemk12u 31400  cdlemk13-2N 31404  cdlemk13 31380  cdlemk14-2N 31406  cdlemk14 31382  cdlemk15-2N 31407  cdlemk15 31383  cdlemk16-2N 31408  cdlemk16 31385  cdlemk16a 31384  cdlemk17-2N 31409  cdlemk17 31386  cdlemk18-2N 31414  cdlemk18-3N 31428  cdlemk18 31396  cdlemk19-2N 31415  cdlemk19 31397  cdlemk19u 31498  cdlemk1u 31387  cdlemk2 31360  cdlemk20-2N 31420  cdlemk20 31402  cdlemk21-2N 31419  cdlemk21N 31401  cdlemk22-3 31429  cdlemk22 31421  cdlemk23-3 31430  cdlemk24-3 31431  cdlemk25-3 31432  cdlemk26-3 31434  cdlemk26b-3 31433  cdlemk27-3 31435  cdlemk28-3 31436  cdlemk29-3 31439  cdlemk3 31361  cdlemk30 31422  cdlemk31 31424  cdlemk32 31425  cdlemk33N 31437  cdlemk34 31438  cdlemk35 31440  cdlemk36 31441  cdlemk37 31442  cdlemk38 31443  cdlemk39 31444  cdlemk39u 31496  cdlemk4 31362  cdlemk41 31448  cdlemk42 31469  cdlemk42yN 31472  cdlemk43N 31491  cdlemk45 31475  cdlemk46 31476  cdlemk47 31477  cdlemk48 31478  cdlemk49 31479  cdlemk5 31364  cdlemk50 31480  cdlemk51 31481  cdlemk52 31482  cdlemk53 31485  cdlemk54 31486  cdlemk55 31489  cdlemk55u 31494  cdlemk56 31499  cdlemk5a 31363  cdlemk5auN 31388  cdlemk5u 31389  cdlemk6 31365  cdlemk6u 31390  cdlemk7 31376  cdlemk7u-2N 31416  cdlemk7u 31398  cdlemk8 31366  cdlemk9 31367  cdlemk9bN 31368  cdlemki 31369  cdlemkid 31464  cdlemkj-2N 31410  cdlemkj 31391  cdlemksat 31374  cdlemksel 31373  cdlemksv 31372  cdlemksv2 31375  cdlemkuat 31394  cdlemkuel-2N 31412  cdlemkuel-3 31426  cdlemkuel 31393  cdlemkuv-2N 31411  cdlemkuv2-2 31413  cdlemkuv2-3N 31427  cdlemkuv2 31395  cdlemkuvN 31392  cdlemkvcl 31370  cdlemky 31454  cdlemkyyN 31490  tendoex 31503
[Crawley] p. 120Remarkdva1dim 31513
[Crawley] p. 120Lemma Lcdleml1N 31504  cdleml2N 31505  cdleml3N 31506  cdleml4N 31507  cdleml5N 31508  cdleml6 31509  cdleml7 31510  cdleml8 31511  cdleml9 31512  dia1dim 31590
[Crawley] p. 120Lemma Mdia11N 31577  diaf11N 31578  dialss 31575  diaord 31576  dibf11N 31690  djajN 31666
[Crawley] p. 120Definition of isomorphism mapdiaval 31561
[Crawley] p. 121Lemma Mcdlemm10N 31647  dia2dimlem1 31593  dia2dimlem2 31594  dia2dimlem3 31595  dia2dimlem4 31596  dia2dimlem5 31597  diaf1oN 31659  diarnN 31658  dvheveccl 31641  dvhopN 31645
[Crawley] p. 121Lemma Ncdlemn 31741  cdlemn10 31735  cdlemn11 31740  cdlemn11a 31736  cdlemn11b 31737  cdlemn11c 31738  cdlemn11pre 31739  cdlemn2 31724  cdlemn2a 31725  cdlemn3 31726  cdlemn4 31727  cdlemn4a 31728  cdlemn5 31730  cdlemn5pre 31729  cdlemn6 31731  cdlemn7 31732  cdlemn8 31733  cdlemn9 31734  diclspsn 31723
[Crawley] p. 121Definition of phi(q)df-dic 31702
[Crawley] p. 122Lemma Ndih11 31794  dihf11 31796  dihjust 31746  dihjustlem 31745  dihord 31793  dihord1 31747  dihord10 31752  dihord11b 31751  dihord11c 31753  dihord2 31756  dihord2a 31748  dihord2b 31749  dihord2cN 31750  dihord2pre 31754  dihord2pre2 31755  dihordlem6 31742  dihordlem7 31743  dihordlem7b 31744
[Crawley] p. 122Definition of isomorphism mapdihffval 31759  dihfval 31760  dihval 31761
[Eisenberg] p. 67Definition 5.3df-dif 3310
[Eisenberg] p. 82Definition 6.3dfom3 7586
[Eisenberg] p. 125Definition 8.21df-map 7006
[Eisenberg] p. 216Example 13.2(4)omenps 7593
[Eisenberg] p. 310Theorem 19.8cardprc 7851
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8414
[Enderton] p. 18Axiom of Empty Setaxnul 4324
[Enderton] p. 19Definitiondf-tp 3809
[Enderton] p. 26Exercise 5unissb 4032
[Enderton] p. 26Exercise 10pwel 4402
[Enderton] p. 28Exercise 7(b)pwun 4478
[Enderton] p. 30Theorem "Distributive laws"iinin1 4149  iinin2 4148  iinun2 4144  iunin1 4143  iunin2 4142
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4147  iundif2 4145
[Enderton] p. 32Exercise 20unineq 3578
[Enderton] p. 33Exercise 23iinuni 4161
[Enderton] p. 33Exercise 25iununi 4162
[Enderton] p. 33Exercise 24(a)iinpw 4166
[Enderton] p. 33Exercise 24(b)iunpw 4745  iunpwss 4167
[Enderton] p. 36Definitionopthwiener 4445
[Enderton] p. 38Exercise 6(a)unipw 4401
[Enderton] p. 38Exercise 6(b)pwuni 4382
[Enderton] p. 41Lemma 3Dopeluu 4701  rnex 5119  rnexg 5117
[Enderton] p. 41Exercise 8dmuni 5065  rnuni 5269
[Enderton] p. 42Definition of a functiondffun7 5465  dffun8 5466
[Enderton] p. 43Definition of function valuefunfv2 5777
[Enderton] p. 43Definition of single-rootedfuncnv 5497
[Enderton] p. 44Definition (d)dfima2 5191  dfima3 5192
[Enderton] p. 47Theorem 3Hfvco2 5784
[Enderton] p. 49Axiom of Choice (first form)ac7 8337  ac7g 8338  df-ac 7981  dfac2 7995  dfac2a 7994  dfac3 7986  dfac7 7996
[Enderton] p. 50Theorem 3K(a)imauni 5979
[Enderton] p. 52Definitiondf-map 7006
[Enderton] p. 53Exercise 21coass 5374
[Enderton] p. 53Exercise 27dmco 5364
[Enderton] p. 53Exercise 14(a)funin 5506
[Enderton] p. 53Exercise 22(a)imass2 5226
[Enderton] p. 54Remarkixpf 7070  ixpssmap 7082
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7050
[Enderton] p. 55Axiom of Choice (second form)ac9 8347  ac9s 8357
[Enderton] p. 56Theorem 3Merref 6911
[Enderton] p. 57Lemma 3Nerthi 6937
[Enderton] p. 57Definitiondf-ec 6893
[Enderton] p. 58Definitiondf-qs 6897
[Enderton] p. 60Theorem 3Qth3q 6999  th3qcor 6998  th3qlem1 6996  th3qlem2 6997
[Enderton] p. 61Exercise 35df-ec 6893
[Enderton] p. 65Exercise 56(a)dmun 5062
[Enderton] p. 68Definition of successordf-suc 4574
[Enderton] p. 71Definitiondf-tr 4290  dftr4 4294
[Enderton] p. 72Theorem 4Eunisuc 4644
[Enderton] p. 73Exercise 6unisuc 4644
[Enderton] p. 73Exercise 5(a)truni 4303
[Enderton] p. 73Exercise 5(b)trint 4304  trintALT 28745
[Enderton] p. 79Theorem 4I(A1)nna0 6833
[Enderton] p. 79Theorem 4I(A2)nnasuc 6835  onasuc 6758
[Enderton] p. 79Definition of operation valuedf-ov 6070
[Enderton] p. 80Theorem 4J(A1)nnm0 6834
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6836  onmsuc 6759
[Enderton] p. 81Theorem 4K(1)nnaass 6851
[Enderton] p. 81Theorem 4K(2)nna0r 6838  nnacom 6846
[Enderton] p. 81Theorem 4K(3)nndi 6852
[Enderton] p. 81Theorem 4K(4)nnmass 6853
[Enderton] p. 81Theorem 4K(5)nnmcom 6855
[Enderton] p. 82Exercise 16nnm0r 6839  nnmsucr 6854
[Enderton] p. 88Exercise 23nnaordex 6867
[Enderton] p. 129Definitiondf-en 7096
[Enderton] p. 132Theorem 6B(b)canth 6525
[Enderton] p. 133Exercise 1xpomen 7881
[Enderton] p. 133Exercise 2qnnen 12796
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7277
[Enderton] p. 135Corollary 6Cphp3 7279
[Enderton] p. 136Corollary 6Enneneq 7276
[Enderton] p. 136Corollary 6D(a)pssinf 7305
[Enderton] p. 136Corollary 6D(b)ominf 7307
[Enderton] p. 137Lemma 6Fpssnn 7313
[Enderton] p. 138Corollary 6Gssfi 7315
[Enderton] p. 139Theorem 6H(c)mapen 7257
[Enderton] p. 142Theorem 6I(3)xpcdaen 8047
[Enderton] p. 142Theorem 6I(4)mapcdaen 8048
[Enderton] p. 143Theorem 6Jcda0en 8043  cda1en 8039
[Enderton] p. 144Exercise 13iunfi 7380  unifi 7381  unifi2 7382
[Enderton] p. 144Corollary 6Kundif2 3691  unfi 7360  unfi2 7362
[Enderton] p. 145Figure 38ffoss 5693
[Enderton] p. 145Definitiondf-dom 7097
[Enderton] p. 146Example 1domen 7107  domeng 7108
[Enderton] p. 146Example 3nndomo 7286  nnsdom 7592  nnsdomg 7352
[Enderton] p. 149Theorem 6L(a)cdadom2 8051
[Enderton] p. 149Theorem 6L(c)mapdom1 7258  xpdom1 7193  xpdom1g 7191  xpdom2g 7190
[Enderton] p. 149Theorem 6L(d)mapdom2 7264
[Enderton] p. 151Theorem 6Mzorn 8371  zorng 8368
[Enderton] p. 151Theorem 6M(4)ac8 8356  dfac5 7993
[Enderton] p. 159Theorem 6Qunictb 8434
[Enderton] p. 164Exampleinfdif 8073
[Enderton] p. 168Definitiondf-po 4490
[Enderton] p. 192Theorem 7M(a)oneli 4675
[Enderton] p. 192Theorem 7M(b)ontr1 4614
[Enderton] p. 192Theorem 7M(c)onirri 4674
[Enderton] p. 193Corollary 7N(b)0elon 4621
[Enderton] p. 193Corollary 7N(c)onsuci 4804
[Enderton] p. 193Corollary 7N(d)ssonunii 4754
[Enderton] p. 194Remarkonprc 4751
[Enderton] p. 194Exercise 16suc11 4671
[Enderton] p. 197Definitiondf-card 7810
[Enderton] p. 197Theorem 7Pcarden 8410
[Enderton] p. 200Exercise 25tfis 4820
[Enderton] p. 202Lemma 7Tr1tr 7686
[Enderton] p. 202Definitiondf-r1 7674
[Enderton] p. 202Theorem 7Qr1val1 7696
[Enderton] p. 204Theorem 7V(b)rankval4 7777
[Enderton] p. 206Theorem 7X(b)en2lp 7555
[Enderton] p. 207Exercise 30rankpr 7767  rankprb 7761  rankpw 7753  rankpwi 7733  rankuniss 7776
[Enderton] p. 207Exercise 34opthreg 7557
[Enderton] p. 208Exercise 35suc11reg 7558
[Enderton] p. 212Definition of alephalephval3 7975
[Enderton] p. 213Theorem 8A(a)alephord2 7941
[Enderton] p. 213Theorem 8A(b)cardalephex 7955
[Enderton] p. 218Theorem Schema 8Eonfununi 6589
[Enderton] p. 222Definition of kardkarden 7803  kardex 7802
[Enderton] p. 238Theorem 8Roeoa 6826
[Enderton] p. 238Theorem 8Soeoe 6828
[Enderton] p. 240Exercise 25oarec 6791
[Enderton] p. 257Definition of cofinalitycflm 8114
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13850
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13796
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14586  mrieqv2d 13847  mrieqvd 13846
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13851
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13856  mreexexlem2d 13853
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14592  mreexfidimd 13858
[Fremlin5] p. 193Proposition 563Gbnulmbl2 19414
[Fremlin5] p. 213Lemma 565Cauniioovol 19454
[Fremlin5] p. 214Lemma 565Cauniioombl 19464
[FreydScedrov] p. 283Axiom of Infinityax-inf 7577  inf1 7561  inf2 7562
[Gleason] p. 117Proposition 9-2.1df-enq 8772  enqer 8782
[Gleason] p. 117Proposition 9-2.2df-1nq 8777  df-nq 8773
[Gleason] p. 117Proposition 9-2.3df-plpq 8769  df-plq 8775
[Gleason] p. 119Proposition 9-2.4caovmo 6270  df-mpq 8770  df-mq 8776
[Gleason] p. 119Proposition 9-2.5df-rq 8778
[Gleason] p. 119Proposition 9-2.6ltexnq 8836
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8837  ltbtwnnq 8839
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8832
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8833
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8840
[Gleason] p. 121Definition 9-3.1df-np 8842
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8854
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8856
[Gleason] p. 122Definitiondf-1p 8843
[Gleason] p. 122Remark (1)prub 8855
[Gleason] p. 122Lemma 9-3.4prlem934 8894
[Gleason] p. 122Proposition 9-3.2df-ltp 8846
[Gleason] p. 122Proposition 9-3.3ltsopr 8893  psslinpr 8892  supexpr 8915  suplem1pr 8913  suplem2pr 8914
[Gleason] p. 123Proposition 9-3.5addclpr 8879  addclprlem1 8877  addclprlem2 8878  df-plp 8844
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8883
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8882
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8895
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8904  ltexprlem1 8897  ltexprlem2 8898  ltexprlem3 8899  ltexprlem4 8900  ltexprlem5 8901  ltexprlem6 8902  ltexprlem7 8903
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8906  ltaprlem 8905
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8907
[Gleason] p. 124Lemma 9-3.6prlem936 8908
[Gleason] p. 124Proposition 9-3.7df-mp 8845  mulclpr 8881  mulclprlem 8880  reclem2pr 8909
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8890
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8885
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8884
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8889
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8912  reclem3pr 8910  reclem4pr 8911
[Gleason] p. 126Proposition 9-4.1df-enr 8918  df-mpr 8917  df-plpr 8916  enrer 8927
[Gleason] p. 126Proposition 9-4.2df-0r 8923  df-1r 8924  df-nr 8919
[Gleason] p. 126Proposition 9-4.3df-mr 8921  df-plr 8920  negexsr 8961  recexsr 8966  recexsrlem 8962
[Gleason] p. 127Proposition 9-4.4df-ltr 8922
[Gleason] p. 130Proposition 10-1.3creui 9979  creur 9978  cru 9976
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 9047  axcnre 9023
[Gleason] p. 132Definition 10-3.1crim 11903  crimd 12020  crimi 11981  crre 11902  crred 12019  crrei 11980
[Gleason] p. 132Definition 10-3.2remim 11905  remimd 11986
[Gleason] p. 133Definition 10.36absval2 12072  absval2d 12230  absval2i 12183
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11929  cjaddd 12008  cjaddi 11976
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11930  cjmuld 12009  cjmuli 11977
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11928  cjcjd 11987  cjcji 11959
[Gleason] p. 133Proposition 10-3.4(f)cjre 11927  cjreb 11911  cjrebd 11990  cjrebi 11962  cjred 12014  rere 11910  rereb 11908  rerebd 11989  rerebi 11961  rered 12012
[Gleason] p. 133Proposition 10-3.4(h)addcj 11936  addcjd 12000  addcji 11971
[Gleason] p. 133Proposition 10-3.7(a)absval 12026
[Gleason] p. 133Proposition 10-3.7(b)abscj 12067  abscjd 12235  abscji 12187
[Gleason] p. 133Proposition 10-3.7(c)abs00 12077  abs00d 12231  abs00i 12184  absne0d 12232
[Gleason] p. 133Proposition 10-3.7(d)releabs 12108  releabsd 12236  releabsi 12188
[Gleason] p. 133Proposition 10-3.7(f)absmul 12082  absmuld 12239  absmuli 12190
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 12070  sqabsaddi 12191
[Gleason] p. 133Proposition 10-3.7(h)abstri 12117  abstrid 12241  abstrii 12194
[Gleason] p. 134Definition 10-4.1df-exp 11366  exp0 11369  expp1 11371  expp1d 11507
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20553  cxpaddd 20591  expadd 11405  expaddd 11508  expaddz 11407
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20562  cxpmuld 20608  expmul 11408  expmuld 11509  expmulz 11409
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20559  mulcxpd 20602  mulexp 11402  mulexpd 11521  mulexpz 11403
[Gleason] p. 140Exercise 1znnen 12795
[Gleason] p. 141Definition 11-2.1fzval 11029
[Gleason] p. 168Proposition 12-2.1(a)climadd 12408  rlimadd 12419  rlimdiv 12422
[Gleason] p. 168Proposition 12-2.1(b)climsub 12410  rlimsub 12420
[Gleason] p. 168Proposition 12-2.1(c)climmul 12409  rlimmul 12421
[Gleason] p. 171Corollary 12-2.2climmulc2 12413
[Gleason] p. 172Corollary 12-2.5climrecl 12360
[Gleason] p. 172Proposition 12-2.4(c)climabs 12380  climcj 12381  climim 12383  climre 12382  rlimabs 12385  rlimcj 12386  rlimim 12388  rlimre 12387
[Gleason] p. 173Definition 12-3.1df-ltxr 9109  df-xr 9108  ltxr 10699
[Gleason] p. 175Definition 12-4.1df-limsup 12248  limsupval 12251
[Gleason] p. 180Theorem 12-5.1climsup 12446
[Gleason] p. 180Theorem 12-5.3caucvg 12455  caucvgb 12456  caucvgr 12452  climcau 12447
[Gleason] p. 182Exercise 3cvgcmp 12578
[Gleason] p. 182Exercise 4cvgrat 12643
[Gleason] p. 195Theorem 13-2.12abs1m 12122
[Gleason] p. 217Lemma 13-4.1btwnzge0 11213
[Gleason] p. 223Definition 14-1.1df-met 16679
[Gleason] p. 223Definition 14-1.1(a)met0 18356  xmet0 18355
[Gleason] p. 223Definition 14-1.1(b)metgt0 18372
[Gleason] p. 223Definition 14-1.1(c)metsym 18363
[Gleason] p. 223Definition 14-1.1(d)mettri 18365  mstri 18482  xmettri 18364  xmstri 18481
[Gleason] p. 225Definition 14-1.5xpsmet 18395
[Gleason] p. 230Proposition 14-2.6txlm 17663
[Gleason] p. 240Theorem 14-4.3metcnp4 19245
[Gleason] p. 240Proposition 14-4.2metcnp3 18553
[Gleason] p. 243Proposition 14-4.16addcn 18878  addcn2 12370  mulcn 18880  mulcn2 12372  subcn 18879  subcn2 12371
[Gleason] p. 295Remarkbcval3 11580  bcval4 11581
[Gleason] p. 295Equation 2bcpasc 11595
[Gleason] p. 295Definition of binomial coefficientbcval 11578  df-bc 11577
[Gleason] p. 296Remarkbcn0 11584  bcnn 11586
[Gleason] p. 296Theorem 15-2.8binom 12592
[Gleason] p. 308Equation 2ef0 12676
[Gleason] p. 308Equation 3efcj 12677
[Gleason] p. 309Corollary 15-4.3efne0 12681
[Gleason] p. 309Corollary 15-4.4efexp 12685
[Gleason] p. 310Equation 14sinadd 12748
[Gleason] p. 310Equation 15cosadd 12749
[Gleason] p. 311Equation 17sincossq 12760
[Gleason] p. 311Equation 18cosbnd 12765  sinbnd 12764
[Gleason] p. 311Lemma 15-4.7sqeqor 11478  sqeqori 11476
[Gleason] p. 311Definition of pidf-pi 12658
[Godowski] p. 730Equation SFgoeqi 23759
[GodowskiGreechie] p. 249Equation IV3oai 23153
[Gratzer] p. 23Section 0.6df-mre 13794
[Gratzer] p. 27Section 0.6df-mri 13796
[Halmos] p. 31Theorem 17.3riesz1 23551  riesz2 23552
[Halmos] p. 41Definition of Hermitianhmopadj2 23427
[Halmos] p. 42Definition of projector orderingpjordi 23659
[Halmos] p. 43Theorem 26.1elpjhmop 23671  elpjidm 23670  pjnmopi 23634
[Halmos] p. 44Remarkpjinormi 23172  pjinormii 23161
[Halmos] p. 44Theorem 26.2elpjch 23675  pjrn 23192  pjrni 23187  pjvec 23181
[Halmos] p. 44Theorem 26.3pjnorm2 23212
[Halmos] p. 44Theorem 26.4hmopidmpj 23640  hmopidmpji 23638
[Halmos] p. 45Theorem 27.1pjinvari 23677
[Halmos] p. 45Theorem 27.3pjoci 23666  pjocvec 23182
[Halmos] p. 45Theorem 27.4pjorthcoi 23655
[Halmos] p. 48Theorem 29.2pjssposi 23658
[Halmos] p. 48Theorem 29.3pjssdif1i 23661  pjssdif2i 23660
[Halmos] p. 50Definition of spectrumdf-spec 23341
[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 1555
[Hatcher] p. 25Definitiondf-phtpc 19000  df-phtpy 18979
[Hatcher] p. 26Definitiondf-pco 19013  df-pi1 19016
[Hatcher] p. 26Proposition 1.2phtpcer 19003
[Hatcher] p. 26Proposition 1.3pi1grp 19058
[Herstein] p. 54Exercise 28df-grpo 21762
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14804  grpoideu 21780  mndideu 14681
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14822  grpoinveu 21793
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14841  grpo2inv 21810
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14850  grpoinvop 21812
[Herstein] p. 57Exercise 1isgrp2d 21806  isgrp2i 21807
[Hitchcock] p. 5Rule A3mpto1 1542
[Hitchcock] p. 5Rule A4mpto2 1543
[Hitchcock] p. 5Rule A5mtp-xor 1545
[Holland] p. 1519Theorem 2sumdmdi 23906
[Holland] p. 1520Lemma 5cdj1i 23919  cdj3i 23927  cdj3lem1 23920  cdjreui 23918
[Holland] p. 1524Lemma 7mddmdin0i 23917
[Holland95] p. 13Theorem 3.6hlathil 32493
[Holland95] p. 14Line 15hgmapvs 32423
[Holland95] p. 14Line 16hdmaplkr 32445
[Holland95] p. 14Line 17hdmapellkr 32446
[Holland95] p. 14Line 19hdmapglnm2 32443
[Holland95] p. 14Line 20hdmapip0com 32449
[Holland95] p. 14Theorem 3.6hdmapevec2 32368
[Holland95] p. 14Lines 24 and 25hdmapoc 32463
[Holland95] p. 204Definition of involutiondf-srng 15917
[Holland95] p. 212Definition of subspacedf-psubsp 30031
[Holland95] p. 214Lemma 3.3lclkrlem2v 32057
[Holland95] p. 214Definition 3.2df-lpolN 32010
[Holland95] p. 214Definition of nonsingularpnonsingN 30461
[Holland95] p. 215Lemma 3.3(1)dihoml4 31906  poml4N 30481
[Holland95] p. 215Lemma 3.3(2)dochexmid 31997  pexmidALTN 30506  pexmidN 30497
[Holland95] p. 218Theorem 3.6lclkr 32062
[Holland95] p. 218Definition of dual vector spacedf-ldual 29653  ldualset 29654
[Holland95] p. 222Item 1df-lines 30029  df-pointsN 30030
[Holland95] p. 222Item 2df-polarityN 30431
[Holland95] p. 223Remarkispsubcl2N 30475  omllaw4 29775  pol1N 30438  polcon3N 30445
[Holland95] p. 223Definitiondf-psubclN 30463
[Holland95] p. 223Equation for polaritypolval2N 30434
[Hughes] p. 44Equation 1.21bax-his3 22569
[Hughes] p. 47Definition of projection operatordfpjop 23668
[Hughes] p. 49Equation 1.30eighmre 23449  eigre 23321  eigrei 23320
[Hughes] p. 49Equation 1.31eighmorth 23450  eigorth 23324  eigorthi 23323
[Hughes] p. 137Remark (ii)eigposi 23322
[Huneke] p. 1Theoremfrgrancvvdeq 28187  frgrancvvdgeq 28188
[Huneke] p. 1Lemma A for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemA 28182
[Huneke] p. 1Lemma B for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemB 28183
[Huneke] p. 1Lemma C for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemC 28184
[Huneke] p. 2Theoremfrghash2spot 28208  frgraregorufr 28198  frgraregorufr0 28197  frgrawopreg1 28195  frgrawopreg2 28196  frgregordn0 28215  usgreghash2spot 28214  usgreghash2spotv 28211
[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 28192
[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 28193
[Indrzejczak] p. 33Definition ` `Enatded 21694  natded 21694
[Indrzejczak] p. 33Definition ` `Inatded 21694
[Indrzejczak] p. 34Definition ` `Enatded 21694  natded 21694
[Indrzejczak] p. 34Definition ` `Inatded 21694
[Jech] p. 4Definition of classcv 1651  cvjust 2425
[Jech] p. 42Lemma 6.1alephexp1 8438
[Jech] p. 42Equation 6.1alephadd 8436  alephmul 8437
[Jech] p. 43Lemma 6.2infmap 8435  infmap2 8082
[Jech] p. 71Lemma 9.3jech9.3 7724
[Jech] p. 72Equation 9.3scott0 7794  scottex 7793
[Jech] p. 72Exercise 9.1rankval4 7777
[Jech] p. 72Scheme "Collection Principle"cp 7799
[Jech] p. 78Definition implied by the footnoteopthprc 4911
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26910
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 27006
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 27007
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26922
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26926
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26927  rmyp1 26928
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26929  rmym1 26930
[JonesMatijasevic] p. 695Equation 2.11rmx0 26920  rmx1 26921  rmxluc 26931
[JonesMatijasevic] p. 695Equation 2.12rmy0 26924  rmy1 26925  rmyluc 26932
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26934
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26935
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26957  jm2.17b 26958  jm2.17c 26959
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26996
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 27000
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26991
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26960  jm2.24nn 26956
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 27005
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 27011  rmygeid 26961
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 27023
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1666
[KalishMontague] p. 85Lemma 2equid 1688
[KalishMontague] p. 85Lemma 3equcomi 1691
[KalishMontague] p. 86Lemma 7cbvalivw 1686  cbvaliw 1685
[KalishMontague] p. 87Lemma 8spimvw 1681  spimw 1680
[KalishMontague] p. 87Lemma 9spfw 1703  spw 1706
[Kalmbach] p. 14Definition of latticechabs1 23001  chabs1i 23003  chabs2 23002  chabs2i 23004  chjass 23018  chjassi 22971  latabs1 14499  latabs2 14500
[Kalmbach] p. 15Definition of atomdf-at 23824  ela 23825
[Kalmbach] p. 15Definition of coverscvbr2 23769  cvrval2 29803
[Kalmbach] p. 16Definitiondf-ol 29707  df-oml 29708
[Kalmbach] p. 20Definition of commutescmbr 23069  cmbri 23075  cmtvalN 29740  df-cm 23068  df-cmtN 29706
[Kalmbach] p. 22Remarkomllaw5N 29776  pjoml5 23098  pjoml5i 23073
[Kalmbach] p. 22Definitionpjoml2 23096  pjoml2i 23070
[Kalmbach] p. 22Theorem 2(v)cmcm 23099  cmcmi 23077  cmcmii 23082  cmtcomN 29778
[Kalmbach] p. 22Theorem 2(ii)omllaw3 29774  omlsi 22889  pjoml 22921  pjomli 22920
[Kalmbach] p. 22Definition of OML lawomllaw2N 29773
[Kalmbach] p. 23Remarkcmbr2i 23081  cmcm3 23100  cmcm3i 23079  cmcm3ii 23084  cmcm4i 23080  cmt3N 29780  cmt4N 29781  cmtbr2N 29782
[Kalmbach] p. 23Lemma 3cmbr3 23093  cmbr3i 23085  cmtbr3N 29783
[Kalmbach] p. 25Theorem 5fh1 23103  fh1i 23106  fh2 23104  fh2i 23107  omlfh1N 29787
[Kalmbach] p. 65Remarkchjatom 23843  chslej 22983  chsleji 22943  shslej 22865  shsleji 22855
[Kalmbach] p. 65Proposition 1chocin 22980  chocini 22939  chsupcl 22825  chsupval2 22895  h0elch 22740  helch 22729  hsupval2 22894  ocin 22781  ococss 22778  shococss 22779
[Kalmbach] p. 65Definition of subspace sumshsval 22797
[Kalmbach] p. 66Remarkdf-pjh 22880  pjssmi 23651  pjssmii 23166
[Kalmbach] p. 67Lemma 3osum 23130  osumi 23127
[Kalmbach] p. 67Lemma 4pjci 23686
[Kalmbach] p. 103Exercise 6atmd2 23886
[Kalmbach] p. 103Exercise 12mdsl0 23796
[Kalmbach] p. 140Remarkhatomic 23846  hatomici 23845  hatomistici 23848
[Kalmbach] p. 140Proposition 1atlatmstc 29848
[Kalmbach] p. 140Proposition 1(i)atexch 23867  lsatexch 29572
[Kalmbach] p. 140Proposition 1(ii)chcv1 23841  cvlcvr1 29868  cvr1 29938
[Kalmbach] p. 140Proposition 1(iii)cvexch 23860  cvexchi 23855  cvrexch 29948
[Kalmbach] p. 149Remark 2chrelati 23850  hlrelat 29930  hlrelat5N 29929  lrelat 29543
[Kalmbach] p. 153Exercise 5lsmcv 16196  lsmsatcv 29539  spansncv 23138  spansncvi 23137
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29558  spansncv2 23779
[Kalmbach] p. 266Definitiondf-st 23697
[Kalmbach2] p. 8Definition of adjointdf-adjh 23335
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8505  fpwwe2 8502
[KanamoriPincus] p. 416Corollary 1.3canth4 8506
[KanamoriPincus] p. 417Corollary 1.6canthp1 8513
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8508
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8510
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8523
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8527  gchxpidm 8528
[KanamoriPincus] p. 419Theorem 2.1gchacg 8531  gchhar 8530
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 8080  unxpwdom 7541
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8533
[Kreyszig] p. 3Property M1metcl 18345  xmetcl 18344
[Kreyszig] p. 4Property M2meteq0 18352
[Kreyszig] p. 8Definition 1.1-8dscmet 18603
[Kreyszig] p. 12Equation 5conjmul 9715  muleqadd 9650
[Kreyszig] p. 18Definition 1.3-2mopnval 18451
[Kreyszig] p. 19Remarkmopntopon 18452
[Kreyszig] p. 19Theorem T1mopn0 18511  mopnm 18457
[Kreyszig] p. 19Theorem T2unimopn 18509
[Kreyszig] p. 19Definition of neighborhoodneibl 18514
[Kreyszig] p. 20Definition 1.3-3metcnp2 18555
[Kreyszig] p. 25Definition 1.4-1lmbr 17305  lmmbr 19194  lmmbr2 19195
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17427
[Kreyszig] p. 28Theorem 1.4-5lmcau 19248
[Kreyszig] p. 28Definition 1.4-3iscau 19212  iscmet2 19230
[Kreyszig] p. 30Theorem 1.4-7cmetss 19250
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17507  metelcls 19240
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 19241  metcld2 19242
[Kreyszig] p. 51Equation 2clmvneg1 19099  lmodvneg1 15970  nvinv 22103  vcm 22033
[Kreyszig] p. 51Equation 1aclm0vs 19098  lmod0vs 15966  vc0 22031
[Kreyszig] p. 51Equation 1blmodvs0 15967  vcz 22032
[Kreyszig] p. 58Definition 2.2-1imsmet 22166
[Kreyszig] p. 59Equation 1imsdval 22161  imsdval2 22162
[Kreyszig] p. 63Problem 1nvnd 22163
[Kreyszig] p. 64Problem 2nvge0 22146  nvz 22141
[Kreyszig] p. 64Problem 3nvabs 22145
[Kreyszig] p. 91Definition 2.7-1isblo3i 22285
[Kreyszig] p. 92Equation 2df-nmoo 22229
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 22291  blocni 22289
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 22290
[Kreyszig] p. 129Definition 3.1-1cphipeq0 19149  ipeq0 16852  ipz 22201
[Kreyszig] p. 135Problem 2pythi 22334
[Kreyszig] p. 137Lemma 3-2.1(a)sii 22338
[Kreyszig] p. 144Equation 4supcvg 12618
[Kreyszig] p. 144Theorem 3.3-1minvec 19320  minveco 22369
[Kreyszig] p. 196Definition 3.9-1df-aj 22234
[Kreyszig] p. 247Theorem 4.7-2bcth 19265
[Kreyszig] p. 249Theorem 4.7-3ubth 22358
[Kreyszig] p. 470Definition of positive operator orderingleop 23609  leopg 23608
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 23627
[Kreyszig] p. 525Theorem 10.1-1htth 22404
[Kunen] p. 10Axiom 0a9e 1952  axnul 4324
[Kunen] p. 11Axiom 3axnul 4324
[Kunen] p. 12Axiom 6zfrep6 5954
[Kunen] p. 24Definition 10.24mapval 7016  mapvalg 7014
[Kunen] p. 30Lemma 10.20fodom 8386
[Kunen] p. 31Definition 10.24mapex 7010
[Kunen] p. 95Definition 2.1df-r1 7674
[Kunen] p. 97Lemma 2.10r1elss 7716  r1elssi 7715
[Kunen] p. 107Exercise 4rankop 7768  rankopb 7762  rankuni 7773  rankxplim 7787  rankxpsuc 7790
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4090
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27461
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27456
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27462
[LeBlanc] p. 277Rule R2axnul 4324
[Levy] p. 338Axiomdf-clab 2417  df-clel 2426  df-cleq 2423
[Levy58] p. 2Definition Iisfin1-3 8250
[Levy58] p. 2Definition IIdf-fin2 8150
[Levy58] p. 2Definition Iadf-fin1a 8149
[Levy58] p. 2Definition IIIdf-fin3 8152
[Levy58] p. 3Definition Vdf-fin5 8153
[Levy58] p. 3Definition IVdf-fin4 8151
[Levy58] p. 4Definition VIdf-fin6 8154
[Levy58] p. 4Definition VIIdf-fin7 8155
[Levy58], p. 3Theorem 1fin1a2 8279
[Lopez-Astorga] p. 12Rule 1mpto1 1542
[Lopez-Astorga] p. 12Rule 2mpto2 1543
[Lopez-Astorga] p. 12Rule 3mtp-xor 1545
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 23894
[Maeda] p. 168Lemma 5mdsym 23898  mdsymi 23897
[Maeda] p. 168Lemma 4(i)mdsymlem4 23892  mdsymlem6 23894  mdsymlem7 23895
[Maeda] p. 168Lemma 4(ii)mdsymlem8 23896
[MaedaMaeda] p. 1Remarkssdmd1 23799  ssdmd2 23800  ssmd1 23797  ssmd2 23798
[MaedaMaeda] p. 1Lemma 1.2mddmd2 23795
[MaedaMaeda] p. 1Definition 1.1df-dmd 23767  df-md 23766  mdbr 23780
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 23817  mdslj1i 23805  mdslj2i 23806  mdslle1i 23803  mdslle2i 23804  mdslmd1i 23815  mdslmd2i 23816
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 23807  mdsl2bi 23809  mdsl2i 23808
[MaedaMaeda] p. 2Lemma 1.6mdexchi 23821
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 23818
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 23819
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 23796
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 23801  mdsl3 23802
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 23820
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23915
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 29850  hlrelat1 29928
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29568
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 23822  cvmdi 23810  cvnbtwn4 23775  cvrnbtwn4 29808
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 23823
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 29869  cvp 23861  cvrp 29944  lcvp 29569
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 23885
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 23884
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 29862  hlexch4N 29920
[MaedaMaeda] p. 34Exercise 7.1atabsi 23887
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 29971
[MaedaMaeda] p. 61Definition 15.10psubN 30277  atpsubN 30281  df-pointsN 30030  pointpsubN 30279
[MaedaMaeda] p. 62Theorem 15.5df-pmap 30032  pmap11 30290  pmaple 30289  pmapsub 30296  pmapval 30285
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 30293  pmap1N 30295
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 30298  pmapglb2N 30299  pmapglb2xN 30300  pmapglbx 30297
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 30380
[MaedaMaeda] p. 67Postulate PS1ps-1 30005
[MaedaMaeda] p. 68Lemma 16.2df-padd 30324  paddclN 30370  paddidm 30369
[MaedaMaeda] p. 68Condition PS2ps-2 30006
[MaedaMaeda] p. 68Equation 16.2.1paddass 30366
[MaedaMaeda] p. 69Lemma 16.4ps-1 30005
[MaedaMaeda] p. 69Theorem 16.4ps-2 30006
[MaedaMaeda] p. 70Theorem 16.9lsmmod 15290  lsmmod2 15291  lssats 29541  shatomici 23844  shatomistici 23847  shmodi 22875  shmodsi 22874
[MaedaMaeda] p. 130Remark 29.6dmdmd 23786  mdsymlem7 23895
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 23074
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22978
[MaedaMaeda] p. 139Remarksumdmdii 23901
[Margaris] p. 40Rule Cexlimiv 1644
[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 1551  df-or 360  dfbi2 610
[Margaris] p. 51Theorem 1id1 21
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 28779
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 28780
[Margaris] p. 79Rule Cexinst01 28478  exinst11 28479
[Margaris] p. 89Theorem 19.219.2 1671  19.2g 1773  r19.2z 3704
[Margaris] p. 89Theorem 19.319.3 1791  19.3v 1677  rr19.3v 3064
[Margaris] p. 89Theorem 19.5alcom 1752
[Margaris] p. 89Theorem 19.6alex 1581
[Margaris] p. 89Theorem 19.7alnex 1552
[Margaris] p. 89Theorem 19.819.8a 1762
[Margaris] p. 89Theorem 19.919.9 1797  19.9h 1794  19.9v 1676  exlimd 1824  exlimdh 1826
[Margaris] p. 89Theorem 19.11excom 1756  excomim 1757
[Margaris] p. 89Theorem 19.1219.12 1869  r19.12 2806
[Margaris] p. 90Theorem 19.14exnal 1583
[Margaris] p. 90Theorem 19.152albi 27486  albi 1573  ralbi 2829
[Margaris] p. 90Theorem 19.1619.16 1883
[Margaris] p. 90Theorem 19.1719.17 1884
[Margaris] p. 90Theorem 19.182exbi 27488  exbi 1591
[Margaris] p. 90Theorem 19.1919.19 1885
[Margaris] p. 90Theorem 19.202alim 27485  alim 1567  alimd 1780  alimdh 1572  alimdv 1631  ralimdaa 2770  ralimdv 2772  ralimdva 2771  sbcimdv 3209
[Margaris] p. 90Theorem 19.2119.21-2 1887  19.21 1814  19.21bi 1774  19.21h 1815  19.21t 1813  19.21v 1913  19.21vv 27484  alrimd 1785  alrimdd 1784  alrimdh 1597  alrimdv 1643  alrimi 1781  alrimih 1574  alrimiv 1641  alrimivv 1642  r19.21 2779  r19.21be 2794  r19.21bi 2791  r19.21t 2778  r19.21v 2780  ralrimd 2781  ralrimdv 2782  ralrimdva 2783  ralrimdvv 2787  ralrimdvva 2788  ralrimi 2774  ralrimiv 2775  ralrimiva 2776  ralrimivv 2784  ralrimivva 2785  ralrimivvva 2786  ralrimivw 2777  rexlimi 2810
[Margaris] p. 90Theorem 19.222alimdv 1633  2exim 27487  2eximdv 1634  exim 1584  eximd 1786  eximdh 1598  eximdv 1632  rexim 2797  reximdai 2801  reximddv 23945  reximdv 2804  reximdv2 2802  reximdva 2805  reximdvai 2803  reximi2 2799
[Margaris] p. 90Theorem 19.2319.23 1819  19.23bi 1775  19.23h 1820  19.23t 1818  19.23v 1914  19.23vv 1915  exlimdv 1646  exlimdvv 1647  exlimexi 28361  exlimi 1821  exlimih 1822  exlimiv 1644  exlimivv 1645  r19.23 2808  r19.23v 2809  rexlimd 2814  rexlimdv 2816  rexlimdv3a 2819  rexlimdva 2817  rexlimdvaa 2818  rexlimdvv 2823  rexlimdvva 2824  rexlimdvw 2820  rexlimiv 2811  rexlimiva 2812  rexlimivv 2822
[Margaris] p. 90Theorem 19.2419.24 1674
[Margaris] p. 90Theorem 19.2519.25 1613
[Margaris] p. 90Theorem 19.2619.26-2 1604  19.26-3an 1605  19.26 1603  r19.26-2 2826  r19.26-3 2827  r19.26 2825  r19.26m 2828
[Margaris] p. 90Theorem 19.2719.27 1841  19.27v 1917  r19.27av 2831  r19.27z 3713  r19.27zv 3714
[Margaris] p. 90Theorem 19.2819.28 1842  19.28v 1918  19.28vv 27494  r19.28av 2832  r19.28z 3707  r19.28zv 3710  rr19.28v 3065
[Margaris] p. 90Theorem 19.2919.29 1606  19.29r 1607  19.29r2 1608  19.29x 1609  r19.29 2833  r19.29d2r 2838  r19.29r 2834
[Margaris] p. 90Theorem 19.3019.30 1614  r19.30 2840
[Margaris] p. 90Theorem 19.3119.31 1897  19.31vv 27492
[Margaris] p. 90Theorem 19.3219.32 1896  r19.32 27854  r19.32v 2841
[Margaris] p. 90Theorem 19.3319.33-2 27490  19.33 1617  19.33b 1618
[Margaris] p. 90Theorem 19.3419.34 1675
[Margaris] p. 90Theorem 19.3519.35 1610  19.35i 1611  19.35ri 1612  r19.35 2842
[Margaris] p. 90Theorem 19.3619.36 1892  19.36aiv 1920  19.36i 1893  19.36v 1919  19.36vv 27491  r19.36av 2843  r19.36zv 3715
[Margaris] p. 90Theorem 19.3719.37 1894  19.37aiv 1923  19.37v 1922  19.37vv 27493  r19.37 2844  r19.37av 2845  r19.37zv 3711
[Margaris] p. 90Theorem 19.3819.38 1812
[Margaris] p. 90Theorem 19.3919.39 1673
[Margaris] p. 90Theorem 19.4019.40-2 1620  19.40 1619  r19.40 2846
[Margaris] p. 90Theorem 19.4119.41 1900  19.41rg 28390  19.41v 1924  19.41vv 1925  19.41vvv 1926  19.41vvvv 1927  r19.41 2847  r19.41v 2848  r19.41vv 23953
[Margaris] p. 90Theorem 19.4219.42 1902  19.42v 1928  19.42vv 1930  19.42vvv 1931  r19.42v 2849
[Margaris] p. 90Theorem 19.4319.43 1615  r19.43 2850
[Margaris] p. 90Theorem 19.4419.44 1898  r19.44av 2851
[Margaris] p. 90Theorem 19.4519.45 1899  r19.45av 2852  r19.45zv 3712
[Margaris] p. 110Exercise 2(b)eu1 2301
[Mayet] p. 370Remarkjpi 23756  largei 23753  stri 23743
[Mayet3] p. 9Definition of CH-statesdf-hst 23698  ishst 23700
[Mayet3] p. 10Theoremhstrbi 23752  hstri 23751
[Mayet3] p. 1223Theorem 4.1mayete3i 23213
[Mayet3] p. 1240Theorem 7.1mayetes3i 23215
[MegPav2000] p. 2344Theorem 3.3stcltrthi 23764
[MegPav2000] p. 2345Definition 3.4-1chintcl 22817  chsupcl 22825
[MegPav2000] p. 2345Definition 3.4-2hatomic 23846
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 23840
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 23867
[MegPav2000] p. 2366Figure 7pl42N 30511
[MegPav2002] p. 362Lemma 2.2latj31 14511  latj32 14509  latjass 14507
[Megill] p. 444Axiom C5ax-17 1626  ax17o 2233
[Megill] p. 444Section 7conventions 21693
[Megill] p. 445Lemma L12aecom-o 2227  aecom 2035  ax-10 2216
[Megill] p. 446Lemma L17equtrr 1695
[Megill] p. 446Lemma L18ax9from9o 2224
[Megill] p. 446Lemma L19hbnae-o 2255  hbnae 2043
[Megill] p. 447Remark 9.1df-sb 1659  sbid 1947  sbidd-misc 28218  sbidd 28217
[Megill] p. 448Remark 9.6ax15 2101
[Megill] p. 448Scheme C4'ax-5o 2212
[Megill] p. 448Scheme C5'ax-4 2211  sp 1763
[Megill] p. 448Scheme C6'ax-7 1749
[Megill] p. 448Scheme C7'ax-6o 2213
[Megill] p. 448Scheme C8'ax-8 1687
[Megill] p. 448Scheme C9'ax-12o 2218
[Megill] p. 448Scheme C10'ax-9 1666  ax-9o 2214
[Megill] p. 448Scheme C11'ax-10o 2215
[Megill] p. 448Scheme C12'ax-13 1727
[Megill] p. 448Scheme C13'ax-14 1729
[Megill] p. 448Scheme C14'ax-15 2219
[Megill] p. 448Scheme C15'ax-11o 2217
[Megill] p. 448Scheme C16'ax-16 2220
[Megill] p. 448Theorem 9.4dral1-o 2230  dral1 2053  dral2-o 2257  dral2 2051  drex1 2055  drex2 2056  drsb1 2102  drsb2 2139
[Megill] p. 448Theorem 9.7conventions 21693
[Megill] p. 449Theorem 9.7sbcom2 2189  sbequ 2138  sbid2v 2199
[Megill] p. 450Example in Appendixhba1-o 2225  hba1 1804
[Mendelson] p. 35Axiom A3hirstL-ax3 27769
[Mendelson] p. 36Lemma 1.8id1 21
[Mendelson] p. 69Axiom 4rspsbc 3226  rspsbca 3227  stdpc4 2087
[Mendelson] p. 69Axiom 5ax-5o 2212  ra5 3232  stdpc5 1816
[Mendelson] p. 81Rule Cexlimiv 1644
[Mendelson] p. 95Axiom 6stdpc6 1699
[Mendelson] p. 95Axiom 7stdpc7 1942
[Mendelson] p. 225Axiom system NBGru 3147
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4445
[Mendelson] p. 231Exercise 4.10(k)inv1 3641
[Mendelson] p. 231Exercise 4.10(l)unv 3642
[Mendelson] p. 231Exercise 4.10(n)dfin3 3567
[Mendelson] p. 231Exercise 4.10(o)df-nul 3616
[Mendelson] p. 231Exercise 4.10(q)dfin4 3568
[Mendelson] p. 231Exercise 4.10(s)ddif 3466
[Mendelson] p. 231Definition of uniondfun3 3566
[Mendelson] p. 235Exercise 4.12(c)univ 4740
[Mendelson] p. 235Exercise 4.12(d)pwv 4001
[Mendelson] p. 235Exercise 4.12(j)pwin 4474
[Mendelson] p. 235Exercise 4.12(k)pwunss 4475
[Mendelson] p. 235Exercise 4.12(l)pwssun 4476
[Mendelson] p. 235Exercise 4.12(n)uniin 4022
[Mendelson] p. 235Exercise 4.12(p)reli 4988
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5376
[Mendelson] p. 244Proposition 4.8(g)epweon 4750
[Mendelson] p. 246Definition of successordf-suc 4574
[Mendelson] p. 250Exercise 4.36oelim2 6824
[Mendelson] p. 254Proposition 4.22(b)xpen 7256
[Mendelson] p. 254Proposition 4.22(c)xpsnen 7178  xpsneng 7179
[Mendelson] p. 254Proposition 4.22(d)xpcomen 7185  xpcomeng 7186
[Mendelson] p. 254Proposition 4.22(e)xpassen 7188
[Mendelson] p. 255Definitionbrsdom 7116
[Mendelson] p. 255Exercise 4.39endisj 7181
[Mendelson] p. 255Exercise 4.41mapprc 7008
[Mendelson] p. 255Exercise 4.43mapsnen 7170
[Mendelson] p. 255Exercise 4.45mapunen 7262
[Mendelson] p. 255Exercise 4.47xpmapen 7261
[Mendelson] p. 255Exercise 4.42(a)map0e 7037
[Mendelson] p. 255Exercise 4.42(b)map1 7171
[Mendelson] p. 257Proposition 4.24(a)undom 7182
[Mendelson] p. 258Exercise 4.56(b)cdaen 8037
[Mendelson] p. 258Exercise 4.56(c)cdaassen 8046  cdacomen 8045
[Mendelson] p. 258Exercise 4.56(f)cdadom1 8050
[Mendelson] p. 258Exercise 4.56(g)xp2cda 8044
[Mendelson] p. 258Definition of cardinal sumcdaval 8034  df-cda 8032
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6761
[Mendelson] p. 266Proposition 4.34(f)oaordex 6787
[Mendelson] p. 275Proposition 4.42(d)entri3 8418
[Mendelson] p. 281Definitiondf-r1 7674
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7723
[Mendelson] p. 287Axiom system MKru 3147
[MertziosUnger] p. 153Proposition 12pthfrgra 28157  2pthfrgrarn 28155  2pthfrgrarn2 28156  frconngra 28167  n4cyclfrgra 28164  vdgfrgragt2 28174  vdgn1frgrav2 28173  vdn1frgrav2 28172
[Mittelstaedt] p. 9Definitiondf-oc 22737
[Monk1] p. 22Remarkconventions 21693
[Monk1] p. 22Theorem 3.1conventions 21693
[Monk1] p. 26Theorem 2.8(vii)ssin 3550
[Monk1] p. 33Theorem 3.2(i)ssrel 4950
[Monk1] p. 33Theorem 3.2(ii)eqrel 4951
[Monk1] p. 34Definition 3.3df-opab 4254
[Monk1] p. 36Theorem 3.7(i)coi1 5371  coi2 5372
[Monk1] p. 36Theorem 3.8(v)dm0 5069  rn0 5113
[Monk1] p. 36Theorem 3.7(ii)cnvi 5262
[Monk1] p. 37Theorem 3.13(i)relxp 4969
[Monk1] p. 37Theorem 3.13(x)dmxp 5074  rnxp 5285
[Monk1] p. 37Theorem 3.13(ii)xp0 5277  xp0r 4942
[Monk1] p. 38Theorem 3.16(ii)ima0 5207
[Monk1] p. 38Theorem 3.16(viii)imai 5204
[Monk1] p. 39Theorem 3.17imaexg 5203
[Monk1] p. 39Theorem 3.16(xi)imassrn 5202
[Monk1] p. 41Theorem 4.3(i)fnopfv 5851  funfvop 5828
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5756
[Monk1] p. 42Theorem 4.4(iii)fvelima 5764
[Monk1] p. 43Theorem 4.6funun 5481
[Monk1] p. 43Theorem 4.8(iv)dff13 5990  dff13f 5992
[Monk1] p. 46Theorem 4.15(v)funex 5949  funrnex 5953
[Monk1] p. 50Definition 5.4fniunfv 5980
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5339
[Monk1] p. 52Theorem 5.11(viii)ssint 4053
[Monk1] p. 52Definition 5.13 (i)1stval2 6350  df-1st 6335
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6351  df-2nd 6336
[Monk1] p. 112Theorem 15.17(v)ranksn 7764  ranksnb 7737
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7765
[Monk1] p. 112Theorem 15.17(iii)rankun 7766  rankunb 7760
[Monk1] p. 113Theorem 15.18r1val3 7748
[Monk1] p. 113Definition 15.19df-r1 7674  r1val2 7747
[Monk1] p. 117Lemmazorn2 8370  zorn2g 8367
[Monk1] p. 133Theorem 18.11cardom 7857
[Monk1] p. 133Theorem 18.12canth3 8420
[Monk1] p. 133Theorem 18.14carduni 7852
[Monk2] p. 105Axiom C4ax-5 1566
[Monk2] p. 105Axiom C7ax-8 1687
[Monk2] p. 105Axiom C8ax-11 1761  ax-11o 2217
[Monk2] p. 105Axiom (C8)ax11v 2171
[Monk2] p. 108Lemma 5ax-5o 2212
[Monk2] p. 109Lemma 12ax-7 1749
[Monk2] p. 109Lemma 15equvin 2083  equvini 2079  eqvinop 4428
[Monk2] p. 113Axiom C5-1ax-17 1626  ax17o 2233
[Monk2] p. 113Axiom C5-2ax-6 1744
[Monk2] p. 113Axiom C5-3ax-7 1749
[Monk2] p. 114Lemma 21sp 1763
[Monk2] p. 114Lemma 22ax5o 1765  hba1-o 2225  hba1 1804
[Monk2] p. 114Lemma 23nfia1 1875
[Monk2] p. 114Lemma 24nfa2 1874  nfra2 2747
[Moore] p. 53Part Idf-mre 13794
[Munkres] p. 77Example 2distop 17043  indistop 17049  indistopon 17048
[Munkres] p. 77Example 3fctop 17051  fctop2 17052
[Munkres] p. 77Example 4cctop 17053
[Munkres] p. 78Definition of basisdf-bases 16948  isbasis3g 16997
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13650  tgval2 17004
[Munkres] p. 79Remarktgcl 17017
[Munkres] p. 80Lemma 2.1tgval3 17011
[Munkres] p. 80Lemma 2.2tgss2 17035  tgss3 17034
[Munkres] p. 81Lemma 2.3basgen 17036  basgen2 17037
[Munkres] p. 89Definition of subspace topologyresttop 17207
[Munkres] p. 93Theorem 6.1(1)0cld 17085  topcld 17082
[Munkres] p. 93Theorem 6.1(2)iincld 17086
[Munkres] p. 93Theorem 6.1(3)uncld 17088
[Munkres] p. 94Definition of closureclsval 17084
[Munkres] p. 94Definition of interiorntrval 17083
[Munkres] p. 95Theorem 6.5(a)clsndisj 17122  elcls 17120
[Munkres] p. 95Theorem 6.5(b)elcls3 17130
[Munkres] p. 97Theorem 6.6clslp 17195  neindisj 17164
[Munkres] p. 97Corollary 6.7cldlp 17197
[Munkres] p. 97Definition of limit pointislp2 17192  lpval 17186
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17362
[Munkres] p. 102Definition of continuous functiondf-cn 17274  iscn 17282  iscn2 17285
[Munkres] p. 107Theorem 7.2(g)cncnp 17327  cncnp2 17328  cncnpi 17325  df-cnp 17275  iscnp 17284  iscnp2 17286
[Munkres] p. 127Theorem 10.1metcn 18556
[Munkres] p. 128Theorem 10.3metcn4 19246
[NielsenChuang] p. 195Equation 4.73unierri 23590
[Pfenning] p. 17Definition XMnatded 21694  natded 21694
[Pfenning] p. 17Definition NNCnatded 21694  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 21694
[Pfenning] p. 18Rule"natded 21694
[Pfenning] p. 18Definition /\Inatded 21694
[Pfenning] p. 18Definition ` `Enatded 21694  natded 21694  natded 21694  natded 21694  natded 21694
[Pfenning] p. 18Definition ` `Inatded 21694  natded 21694  natded 21694  natded 21694  natded 21694
[Pfenning] p. 18Definition ` `ELnatded 21694
[Pfenning] p. 18Definition ` `ERnatded 21694
[Pfenning] p. 18Definition ` `Ea,unatded 21694
[Pfenning] p. 18Definition ` `IRnatded 21694
[Pfenning] p. 18Definition ` `Ianatded 21694
[Pfenning] p. 127Definition =Enatded 21694
[Pfenning] p. 127Definition =Inatded 21694
[Ponnusamy] p. 361Theorem 6.44cphip0l 19147  df-dip 22180  dip0l 22200  ip0l 16850
[Ponnusamy] p. 361Equation 6.45ipval 22182
[Ponnusamy] p. 362Equation I1dipcj 22196
[Ponnusamy] p. 362Equation I3cphdir 19150  dipdir 22326  ipdir 16853  ipdiri 22314
[Ponnusamy] p. 362Equation I4ipidsq 22192
[Ponnusamy] p. 362Equation 6.46ip0i 22309
[Ponnusamy] p. 362Equation 6.47ip1i 22311
[Ponnusamy] p. 362Equation 6.48ip2i 22312
[Ponnusamy] p. 363Equation I2cphass 19156  dipass 22329  ipass 16859  ipassi 22325
[Prugovecki] p. 186Definition of brabraval 23430  df-bra 23336
[Prugovecki] p. 376Equation 8.1df-kb 23337  kbval 23440
[PtakPulmannova] p. 66Proposition 3.2.17atomli 23868
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30416
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 23882  atcvat4i 23883  cvrat3 29970  cvrat4 29971  lsatcvat3 29581
[PtakPulmannova] p. 68Definition 3.2.18cvbr 23768  cvrval 29798  df-cv 23765  df-lcv 29548  lspsncv0 16201
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30428
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30429
[Quine] p. 16Definition 2.1df-clab 2417  rabid 2871
[Quine] p. 17Definition 2.1''dfsb7 2197
[Quine] p. 18Definition 2.7df-cleq 2423
[Quine] p. 19Definition 2.9conventions 21693  df-v 2945
[Quine] p. 34Theorem 5.1abeq2 2535
[Quine] p. 35Theorem 5.2abid2 2547  abid2f 2591
[Quine] p. 40Theorem 6.1sb5 2175
[Quine] p. 40Theorem 6.2sb56 2173  sb6 2174
[Quine] p. 41Theorem 6.3df-clel 2426
[Quine] p. 41Theorem 6.4eqid 2430  eqid1 21744
[Quine] p. 41Theorem 6.5eqcom 2432
[Quine] p. 42Theorem 6.6df-sbc 3149
[Quine] p. 42Theorem 6.7dfsbcq 3150  dfsbcq2 3151
[Quine] p. 43Theorem 6.8vex 2946
[Quine] p. 43Theorem 6.9isset 2947
[Quine] p. 44Theorem 7.3spcgf 3018  spcgv 3023  spcimgf 3016
[Quine] p. 44Theorem 6.11spsbc 3160  spsbcd 3161
[Quine] p. 44Theorem 6.12elex 2951
[Quine] p. 44Theorem 6.13elab 3069  elabg 3070  elabgf 3067
[Quine] p. 44Theorem 6.14noel 3619
[Quine] p. 48Theorem 7.2snprc 3858
[Quine] p. 48Definition 7.1df-pr 3808  df-sn 3807
[Quine] p. 49Theorem 7.4snss 3913  snssg 3919
[Quine] p. 49Theorem 7.5prss 3939  prssg 3940
[Quine] p. 49Theorem 7.6prid1 3899  prid1g 3897  prid2 3900  prid2g 3898  snid 3828  snidg 3826
[Quine] p. 51Theorem 7.13prex 4393  snex 4392  snexALT 4372
[Quine] p. 53Theorem 8.2unisn 4018  unisnALT 28790  unisng 4019
[Quine] p. 53Theorem 8.3uniun 4021
[Quine] p. 54Theorem 8.6elssuni 4030
[Quine] p. 54Theorem 8.7uni0 4029
[Quine] p. 56Theorem 8.17uniabio 5414
[Quine] p. 56Definition 8.18dfiota2 5405
[Quine] p. 57Theorem 8.19iotaval 5415
[Quine] p. 57Theorem 8.22iotanul 5419
[Quine] p. 58Theorem 8.23iotaex 5421
[Quine] p. 58Definition 9.1df-op 3810
[Quine] p. 61Theorem 9.5opabid 4448  opelopab 4463  opelopaba 4458  opelopabaf 4465  opelopabf 4466  opelopabg 4460  opelopabga 4455  oprabid 6091
[Quine] p. 64Definition 9.11df-xp 4870
[Quine] p. 64Definition 9.12df-cnv 4872
[Quine] p. 64Definition 9.15df-id 4485
[Quine] p. 65Theorem 10.3fun0 5494
[Quine] p. 65Theorem 10.4funi 5469
[Quine] p. 65Theorem 10.5funsn 5485  funsng 5483
[Quine] p. 65Definition 10.1df-fun 5442
[Quine] p. 65Definition 10.2args 5218  dffv4 5711
[Quine] p. 68Definition 10.11conventions 21693  df-fv 5448  fv2 5709
[Quine] p. 124Theorem 17.3nn0opth2 11548  nn0opth2i 11547  nn0opthi 11546  omopthi 6886
[Quine] p. 177Definition 25.2df-rdg 6654
[Quine] p. 232Equation icarddom 8413
[Quine] p. 284Axiom 39(vi)funimaex 5517  funimaexg 5516
[Quine] p. 331Axiom system NFru 3147
[ReedSimon] p. 36Definition (iii)ax-his3 22569
[ReedSimon] p. 63Exercise 4(a)df-dip 22180  polid 22644  polid2i 22642  polidi 22643
[ReedSimon] p. 63Exercise 4(b)df-ph 22297
[ReedSimon] p. 195Remarklnophm 23505  lnophmi 23504
[Retherford] p. 49Exercise 1(i)leopadd 23618
[Retherford] p. 49Exercise 1(ii)leopmul 23620  leopmuli 23619
[Retherford] p. 49Exercise 1(iv)leoptr 23623
[Retherford] p. 49Definition VI.1df-leop 23338  leoppos 23612
[Retherford] p. 49Exercise 1(iii)leoptri 23622
[Retherford] p. 49Definition of operator orderingleop3 23611
[Rudin] p. 164Equation 27efcan 12680
[Rudin] p. 164Equation 30efzval 12686
[Rudin] p. 167Equation 48absefi 12780
[Sanford] p. 39Rule 3mtp-xor 1545
[Sanford] p. 39Rule 4mpto2 1543
[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 1542
[Schechter] p. 51Definition of antisymmetryintasym 5235
[Schechter] p. 51Definition of irreflexivityintirr 5238
[Schechter] p. 51Definition of symmetrycnvsym 5234
[Schechter] p. 51Definition of transitivitycotr 5232
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13794
[Schechter] p. 79Definition of Moore closuredf-mrc 13795
[Schechter] p. 82Section 4.5df-mrc 13795
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13797
[Schechter] p. 139Definition AC3dfac9 8000
[Schechter] p. 141Definition (MC)dfac11 27070
[Schechter] p. 149Axiom DC1ax-dc 8310  axdc3 8318
[Schechter] p. 187Definition of ring with unitisrng 15651  isrngo 21949
[Schechter] p. 276Remark 11.6.espan0 23027
[Schechter] p. 276Definition of spandf-span 22794  spanval 22818
[Schechter] p. 428Definition 15.35bastop1 17041
[Schwabhauser] p. 10Axiom A1axcgrrflx 25796
[Schwabhauser] p. 10Axiom A2axcgrtr 25797
[Schwabhauser] p. 10Axiom A3axcgrid 25798
[Schwabhauser] p. 11Axiom A4axsegcon 25809
[Schwabhauser] p. 11Axiom A5ax5seg 25820
[Schwabhauser] p. 11Axiom A6axbtwnid 25821
[Schwabhauser] p. 12Axiom A7axpasch 25823
[Schwabhauser] p. 12Axiom A8axlowdim2 25842
[Schwabhauser] p. 13Axiom A10axeuclid 25845
[Schwabhauser] p. 13Axiom A11axcont 25858
[Schwabhauser] p. 27Theorem 2.1cgrrflx 25864
[Schwabhauser] p. 27Theorem 2.2cgrcomim 25866
[Schwabhauser] p. 27Theorem 2.3cgrtr 25869
[Schwabhauser] p. 27Theorem 2.4cgrcoml 25873
[Schwabhauser] p. 27Theorem 2.5cgrcomr 25874
[Schwabhauser] p. 28Theorem 2.8cgrtriv 25879
[Schwabhauser] p. 28Theorem 2.105segofs 25883
[Schwabhauser] p. 28Definition 2.10df-ofs 25860
[Schwabhauser] p. 29Theorem 2.11cgrextend 25885
[Schwabhauser] p. 29Theorem 2.12segconeq 25887
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 25899  btwntriv2 25889
[Schwabhauser] p. 30Theorem 3.2btwncomim 25890
[Schwabhauser] p. 30Theorem 3.3btwntriv1 25893
[Schwabhauser] p. 30Theorem 3.4btwnswapid 25894
[Schwabhauser] p. 30Theorem 3.5btwnexch2 25900  btwnintr 25896
[Schwabhauser] p. 30Theorem 3.6btwnexch 25902  btwnexch3 25897
[Schwabhauser] p. 30Theorem 3.7btwnouttr 25901
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25841
[Schwabhauser] p. 32Theorem 3.14btwndiff 25904
[Schwabhauser] p. 33Theorem 3.17trisegint 25905
[Schwabhauser] p. 34Theorem 4.2ifscgr 25921
[Schwabhauser] p. 34Definition 4.1df-ifs 25916
[Schwabhauser] p. 35Theorem 4.3cgrsub 25922
[Schwabhauser] p. 35Theorem 4.5cgrxfr 25932
[Schwabhauser] p. 35Definition 4.4df-cgr3 25917
[Schwabhauser] p. 36Theorem 4.6btwnxfr 25933
[Schwabhauser] p. 36Theorem 4.11colinearperm1 25939  colinearperm2 25941  colinearperm3 25940  colinearperm4 25942  colinearperm5 25943
[Schwabhauser] p. 36Definition 4.10df-colinear 25918
[Schwabhauser] p. 37Theorem 4.12colineartriv1 25944
[Schwabhauser] p. 37Theorem 4.13colinearxfr 25952
[Schwabhauser] p. 37Theorem 4.14lineext 25953
[Schwabhauser] p. 37Theorem 4.16fscgr 25957
[Schwabhauser] p. 37Theorem 4.17linecgr 25958
[Schwabhauser] p. 37Definition 4.15df-fs 25919
[Schwabhauser] p. 38Theorem 4.18lineid 25960
[Schwabhauser] p. 38Theorem 4.19idinside 25961
[Schwabhauser] p. 39Theorem 5.1btwnconn1 25978
[Schwabhauser] p. 41Theorem 5.2btwnconn2 25979
[Schwabhauser] p. 41Theorem 5.3btwnconn3 25980
[Schwabhauser] p. 41Theorem 5.5brsegle2 25986
[Schwabhauser] p. 41Definition 5.4df-segle 25984
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 25987
[Schwabhauser] p. 42Theorem 5.7seglerflx 25989
[Schwabhauser] p. 42Theorem 5.8segletr 25991
[Schwabhauser] p. 42Theorem 5.9segleantisym 25992
[Schwabhauser] p. 42Theorem 5.10seglelin 25993
[Schwabhauser] p. 42Theorem 5.11seglemin 25990
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 25995
[Schwabhauser] p. 43Theorem 6.2btwnoutside 26002
[Schwabhauser] p. 43Theorem 6.3broutsideof3 26003
[Schwabhauser] p. 43Theorem 6.4broutsideof 25998  df-outsideof 25997
[Schwabhauser] p. 43Definition 6.1broutsideof2 25999
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 26004
[Schwabhauser] p. 44Theorem 6.6outsideofcom 26005
[Schwabhauser] p. 44Theorem 6.7outsideoftr 26006
[Schwabhauser] p. 44Theorem 6.11outsideofeu 26008
[Schwabhauser] p. 44Definition 6.8df-ray 26015
[Schwabhauser] p. 45Part 2df-lines2 26016
[Schwabhauser] p. 45Theorem 6.13outsidele 26009
[Schwabhauser] p. 45Theorem 6.15lineunray 26024
[Schwabhauser] p. 45Theorem 6.16lineelsb2 26025
[Schwabhauser] p. 45Theorem 6.17linecom 26027  linerflx1 26026  linerflx2 26028
[Schwabhauser] p. 45Theorem 6.18linethru 26030
[Schwabhauser] p. 45Definition 6.14df-line2 26014
[Schwabhauser] p. 46Theorem 6.19linethrueu 26033
[Schwabhauser] p. 46Theorem 6.21lineintmo 26034
[Shapiro] p. 230Theorem 6.5.1dchrhash 21038  dchrsum 21036  dchrsum2 21035  sumdchr 21039
[Shapiro] p. 232Theorem 6.5.2dchr2sum 21040  sum2dchr 21041
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15607  ablfacrp2 15608
[Shapiro], p. 328Equation 9.2.4vmasum 20983
[Shapiro], p. 329Equation 9.2.7logfac2 20984
[Shapiro], p. 329Equation 9.2.9logfacrlim 20991
[Shapiro], p. 331Equation 9.2.13vmadivsum 21159
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 21162
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 21216  vmalogdivsum2 21215
[Shapiro], p. 375Theorem 9.4.1dirith 21206  dirith2 21205
[Shapiro], p. 375Equation 9.4.3rplogsum 21204  rpvmasum 21203  rpvmasum2 21189
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 21164
[Shapiro], p. 376Equation 9.4.8dchrvmasum 21202
[Shapiro], p. 377Lemma 9.4.1dchrisum 21169  dchrisumlem1 21166  dchrisumlem2 21167  dchrisumlem3 21168  dchrisumlema 21165
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 21172
[Shapiro], p. 379Equation 9.4.16dchrmusum 21201  dchrmusumlem 21199  dchrvmasumlem 21200
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 21171
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 21173
[Shapiro], p. 382Lemma 9.4.4dchrisum0 21197  dchrisum0re 21190  dchrisumn0 21198
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 21183
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 21187
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 21188
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 21243  pntrsumbnd2 21244  pntrsumo1 21242
[Shapiro], p. 405Equation 10.2.1mudivsum 21207
[Shapiro], p. 406Equation 10.2.6mulogsum 21209
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 21211
[Shapiro], p. 407Equation 10.2.8mulog2sum 21214
[Shapiro], p. 418Equation 10.4.6logsqvma 21219
[Shapiro], p. 418Equation 10.4.8logsqvma2 21220
[Shapiro], p. 419Equation 10.4.10selberg 21225
[Shapiro], p. 420Equation 10.4.12selberg2lem 21227
[Shapiro], p. 420Equation 10.4.14selberg2 21228
[Shapiro], p. 422Equation 10.6.7selberg3 21236
[Shapiro], p. 422Equation 10.4.20selberg4lem1 21237
[Shapiro], p. 422Equation 10.4.21selberg3lem1 21234  selberg3lem2 21235
[Shapiro], p. 422Equation 10.4.23selberg4 21238
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 21232
[Shapiro], p. 428Equation 10.6.2selbergr 21245
[Shapiro], p. 429Equation 10.6.8selberg3r 21246
[Shapiro], p. 430Equation 10.6.11selberg4r 21247
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 21261
[Shapiro], p. 434Equation 10.6.27pntlema 21273  pntlemb 21274  pntlemc 21272  pntlemd 21271  pntlemg 21275
[Shapiro], p. 435Equation 10.6.29pntlema 21273
[Shapiro], p. 436Lemma 10.6.1pntpbnd 21265
[Shapiro], p. 436Lemma 10.6.2pntibnd 21270
[Shapiro], p. 436Equation 10.6.34pntlema 21273
[Shapiro], p. 436Equation 10.6.35pntlem3 21286  pntleml 21288
[Stoll] p. 13Definition of symmetric differencesymdif1 3593
[Stoll] p. 16Exercise 4.40dif 3686  dif0 3685
[Stoll] p. 16Exercise 4.8difdifdir 3702
[Stoll] p. 17Theorem 5.1(5)undifv 3689
[Stoll] p. 19Theorem 5.2(13)undm 3586
[Stoll] p. 19Theorem 5.2(13')indm 3587
[Stoll] p. 20Remarkinvdif 3569
[Stoll] p. 25Definition of ordered tripledf-ot 3811
[Stoll] p. 43Definitionuniiun 4131
[Stoll] p. 44Definitionintiin 4132
[Stoll] p. 45Definitiondf-iin 4083
[Stoll] p. 45Definition indexed uniondf-iun 4082
[Stoll] p. 176Theorem 3.4(27)iman 414
[Stoll] p. 262Example 4.1symdif1 3593
[Strang] p. 242Section 6.3expgrowth 27462
[Suppes] p. 22Theorem 2eq0 3629
[Suppes] p. 22Theorem 4eqss 3350  eqssd 3352  eqssi 3351
[Suppes] p. 23Theorem 5ss0 3645  ss0b 3644
[Suppes] p. 23Theorem 6sstr 3343  sstrALT2 28699
[Suppes] p. 23Theorem 7pssirr 3434
[Suppes] p. 23Theorem 8pssn2lp 3435
[Suppes] p. 23Theorem 9psstr 3438
[Suppes] p. 23Theorem 10pssss 3429
[Suppes] p. 25Theorem 12elin 3517  elun 3475
[Suppes] p. 26Theorem 15inidm 3537
[Suppes] p. 26Theorem 16in0 3640
[Suppes] p. 27Theorem 23unidm 3477
[Suppes] p. 27Theorem 24un0 3639
[Suppes] p. 27Theorem 25ssun1 3497
[Suppes] p. 27Theorem 26ssequn1 3504
[Suppes] p. 27Theorem 27unss 3508
[Suppes] p. 27Theorem 28indir 3576
[Suppes] p. 27Theorem 29undir 3577
[Suppes] p. 28Theorem 32difid 3683  difidALT 3684
[Suppes] p. 29Theorem 33difin 3565
[Suppes] p. 29Theorem 34indif 3570
[Suppes] p. 29Theorem 35undif1 3690
[Suppes] p. 29Theorem 36difun2 3694
[Suppes] p. 29Theorem 37difin0 3688
[Suppes] p. 29Theorem 38disjdif 3687
[Suppes] p. 29Theorem 39difundi 3580
[Suppes] p. 29Theorem 40difindi 3582
[Suppes] p. 30Theorem 41nalset 4327
[Suppes] p. 39Theorem 61uniss 4023
[Suppes] p. 39Theorem 65uniop 4446
[Suppes] p. 41Theorem 70intsn 4073
[Suppes] p. 42Theorem 71intpr 4070  intprg 4071
[Suppes] p. 42Theorem 73op1stb 4744
[Suppes] p. 42Theorem 78intun 4069
[Suppes] p. 44Definition 15(a)dfiun2 4112  dfiun2g 4110
[Suppes] p. 44Definition 15(b)dfiin2 4113
[Suppes] p. 47Theorem 86elpw 3792  elpw2 4351  elpw2g 4350  elpwg 3793  elpwgdedVD 28781
[Suppes] p. 47Theorem 87pwid 3799
[Suppes] p. 47Theorem 89pw0 3932
[Suppes] p. 48Theorem 90pwpw0 3933
[Suppes] p. 52Theorem 101xpss12 4967
[Suppes] p. 52Theorem 102xpindi 4994  xpindir 4995
[Suppes] p. 52Theorem 103xpundi 4916  xpundir 4917
[Suppes] p. 54Theorem 105elirrv 7549
[Suppes] p. 58Theorem 2relss 4949
[Suppes] p. 59Theorem 4eldm 5053  eldm2 5054  eldm2g 5052  eldmg 5051
[Suppes] p. 59Definition 3df-dm 4874
[Suppes] p. 60Theorem 6dmin 5063
[Suppes] p. 60Theorem 8rnun 5266
[Suppes] p. 60Theorem 9rnin 5267
[Suppes] p. 60Definition 4dfrn2 5045
[Suppes] p. 61Theorem 11brcnv 5041  brcnvg 5039
[Suppes] p. 62Equation 5elcnv 5035  elcnv2 5036
[Suppes] p. 62Theorem 12relcnv 5228
[Suppes] p. 62Theorem 15cnvin 5265
[Suppes] p. 62Theorem 16cnvun 5263
[Suppes] p. 63Theorem 20co02 5369
[Suppes] p. 63Theorem 21dmcoss 5121
[Suppes] p. 63Definition 7df-co 4873
[Suppes] p. 64Theorem 26cnvco 5042
[Suppes] p. 64Theorem 27coass 5374
[Suppes] p. 65Theorem 31resundi 5146
[Suppes] p. 65Theorem 34elima 5194  elima2 5195  elima3 5196  elimag 5193
[Suppes] p. 65Theorem 35imaundi 5270
[Suppes] p. 66Theorem 40dminss 5272
[Suppes] p. 66Theorem 41imainss 5273
[Suppes] p. 67Exercise 11cnvxp 5276
[Suppes] p. 81Definition 34dfec2 6894
[Suppes] p. 82Theorem 72elec 6930  elecg 6929
[Suppes] p. 82Theorem 73erth 6935  erth2 6936
[Suppes] p. 83Theorem 74erdisj 6938
[Suppes] p. 89Theorem 96map0b 7038
[Suppes] p. 89Theorem 97map0 7040  map0g 7039
[Suppes] p. 89Theorem 98mapsn 7041
[Suppes] p. 89Theorem 99mapss 7042
[Suppes] p. 91Definition 12(ii)alephsuc 7933
[Suppes] p. 91Definition 12(iii)alephlim 7932
[Suppes] p. 92Theorem 1enref 7126  enrefg 7125
[Suppes] p. 92Theorem 2ensym 7142  ensymb 7141  ensymi 7143
[Suppes] p. 92Theorem 3entr 7145
[Suppes] p. 92Theorem 4unen 7175
[Suppes] p. 94Theorem 15endom 7120
[Suppes] p. 94Theorem 16ssdomg 7139
[Suppes] p. 94Theorem 17domtr 7146
[Suppes] p. 95Theorem 18sbth 7213
[Suppes] p. 97Theorem 23canth2 7246  canth2g 7247
[Suppes] p. 97Definition 3brsdom2 7217  df-sdom 7098  dfsdom2 7216
[Suppes] p. 97Theorem 21(i)sdomirr 7230
[Suppes] p. 97Theorem 22(i)domnsym 7219
[Suppes] p. 97Theorem 21(ii)sdomnsym 7218
[Suppes] p. 97Theorem 22(ii)domsdomtr 7228
[Suppes] p. 97Theorem 22(iv)brdom2 7123
[Suppes] p. 97Theorem 21(iii)sdomtr 7231
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7226
[Suppes] p. 98Exercise 4fundmen 7166  fundmeng 7167
[Suppes] p. 98Exercise 6xpdom3 7192
[Suppes] p. 98Exercise 11sdomentr 7227
[Suppes] p. 104Theorem 37fofi 7378
[Suppes] p. 104Theorem 38pwfi 7388
[Suppes] p. 105Theorem 40pwfi 7388
[Suppes] p. 111Axiom for cardinal numberscarden 8410
[Suppes] p. 130Definition 3df-tr 4290
[Suppes] p. 132Theorem 9ssonuni 4753
[Suppes] p. 134Definition 6df-suc 4574
[Suppes] p. 136Theorem Schema 22findes 4861  finds 4857  finds1 4860  finds2 4859
[Suppes] p. 151Theorem 42isfinite 7591  isfinite2 7351  isfiniteg 7353  unbnn 7349
[Suppes] p. 162Definition 5df-ltnq 8779  df-ltpq 8771
[Suppes] p. 197Theorem Schema 4tfindes 4828  tfinds 4825  tfinds2 4829
[Suppes] p. 209Theorem 18oaord1 6780
[Suppes] p. 209Theorem 21oaword2 6782
[Suppes] p. 211Theorem 25oaass 6790
[Suppes] p. 225Definition 8iscard2 7847
[Suppes] p. 227Theorem 56ondomon 8422
[Suppes] p. 228Theorem 59harcard 7849
[Suppes] p. 228Definition 12(i)aleph0 7931
[Suppes] p. 228Theorem Schema 61onintss 4618
[Suppes] p. 228Theorem Schema 62onminesb 4764  onminsb 4765
[Suppes] p. 229Theorem 64alephval2 8431
[Suppes] p. 229Theorem 65alephcard 7935
[Suppes] p. 229Theorem 66alephord2i 7942
[Suppes] p. 229Theorem 67alephnbtwn 7936
[Suppes] p. 229Definition 12df-aleph 7811
[Suppes] p. 242Theorem 6weth 8359
[Suppes] p. 242Theorem 8entric 8416
[Suppes] p. 242Theorem 9carden 8410
[TakeutiZaring] p. 8Axiom 1ax-ext 2411
[TakeutiZaring] p. 13Definition 4.5df-cleq 2423
[TakeutiZaring] p. 13Proposition 4.6df-clel 2426
[TakeutiZaring] p. 13Proposition 4.9cvjust 2425
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2447
[TakeutiZaring] p. 14Definition 4.16df-oprab 6071
[TakeutiZaring] p. 14Proposition 4.14ru 3147
[TakeutiZaring] p. 15Axiom 2zfpair 4388
[TakeutiZaring] p. 15Exercise 1elpr 3819  elpr2 3820  elprg 3818
[TakeutiZaring] p. 15Exercise 2elsn 3816  elsnc 3824  elsnc2 3830  elsnc2g 3829  elsncg 3823
[TakeutiZaring] p. 15Exercise 3elop 4416
[TakeutiZaring] p. 15Exercise 4sneq 3812  sneqr 3953
[TakeutiZaring] p. 15Definition 5.1dfpr2 3817  dfsn2 3815
[TakeutiZaring] p. 16Axiom 3uniex 4691
[TakeutiZaring] p. 16Exercise 6opth 4422
[TakeutiZaring] p. 16Exercise 7opex 4414
[TakeutiZaring] p. 16Exercise 8rext 4399
[TakeutiZaring] p. 16Corollary 5.8unex 4693  unexg 4696
[TakeutiZaring] p. 16Definition 5.3dftp2 3841
[TakeutiZaring] p. 16Definition 5.5df-uni 4003
[TakeutiZaring] p. 16Definition 5.6df-in 3314  df-un 3312
[TakeutiZaring] p. 16Proposition 5.7unipr 4016  uniprg 4017
[TakeutiZaring] p. 17Axiom 4pwex 4369  pwexg 4370
[TakeutiZaring] p. 17Exercise 1eltp 3840
[TakeutiZaring] p. 17Exercise 5elsuc 4637  elsucg 4635  sstr2 3342
[TakeutiZaring] p. 17Exercise 6uncom 3478
[TakeutiZaring] p. 17Exercise 7incom 3520
[TakeutiZaring] p. 17Exercise 8unass 3491
[TakeutiZaring] p. 17Exercise 9inass 3538
[TakeutiZaring] p. 17Exercise 10indi 3574
[TakeutiZaring] p. 17Exercise 11undi 3575
[TakeutiZaring] p. 17Definition 5.9df-pss 3323  dfss2 3324
[TakeutiZaring] p. 17Definition 5.10df-pw 3788
[TakeutiZaring] p. 18Exercise 7unss2 3505
[TakeutiZaring] p. 18Exercise 9df-ss 3321  sseqin2 3547
[TakeutiZaring] p. 18Exercise 10ssid 3354
[TakeutiZaring] p. 18Exercise 12inss1 3548  inss2 3549
[TakeutiZaring] p. 18Exercise 13nss 3393
[TakeutiZaring] p. 18Exercise 15unieq 4011
[TakeutiZaring] p. 18Exercise 18sspwb 4400  sspwimp 28782  sspwimpALT 28789  sspwimpALT2 28793  sspwimpcf 28784
[TakeutiZaring] p. 18Exercise 19pweqb 4407
[TakeutiZaring] p. 19Axiom 5ax-rep 4307
[TakeutiZaring] p. 20Definitiondf-rab 2701
[TakeutiZaring] p. 20Corollary 5.160ex 4326
[TakeutiZaring] p. 20Definition 5.12df-dif 3310
[TakeutiZaring] p. 20Definition 5.14dfnul2 3617
[TakeutiZaring] p. 20Proposition 5.15difid 3683  difidALT 3684
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3624  n0f 3623  neq0 3625
[TakeutiZaring] p. 21Axiom 6zfreg 7547
[TakeutiZaring] p. 21Axiom 6'zfregs 7652
[TakeutiZaring] p. 21Theorem 5.22setind 7657
[TakeutiZaring] p. 21Definition 5.20df-v 2945
[TakeutiZaring] p. 21Proposition 5.21vprc 4328
[TakeutiZaring] p. 22Exercise 10ss 3643
[TakeutiZaring] p. 22Exercise 3ssex 4334  ssexg 4336
[TakeutiZaring] p. 22Exercise 4inex1 4331
[TakeutiZaring] p. 22Exercise 5ruv 7552
[TakeutiZaring] p. 22Exercise 6elirr 7550
[TakeutiZaring] p. 22Exercise 7ssdif0 3673
[TakeutiZaring] p. 22Exercise 11difdif 3460
[TakeutiZaring] p. 22Exercise 13undif3 3589  undif3VD 28746
[TakeutiZaring] p. 22Exercise 14difss 3461
[TakeutiZaring] p. 22Exercise 15sscon 3468
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2697
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2698
[TakeutiZaring] p. 23Proposition 6.2xpex 4976  xpexg 4975  xpexgALT 6283
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4871
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5499
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5633  fun11 5502
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5452  svrelfun 5500
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5044
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5046
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4876
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4877
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4873
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5311  dfrel2 5307
[TakeutiZaring] p. 25Exercise 3xpss 4968
[TakeutiZaring] p. 25Exercise 5relun 4977
[TakeutiZaring] p. 25Exercise 6reluni 4983
[TakeutiZaring] p. 25Exercise 9inxp 4993
[TakeutiZaring] p. 25Exercise 12relres 5160
[TakeutiZaring] p. 25Exercise 13opelres 5137  opelresg 5139
[TakeutiZaring] p. 25Exercise 14dmres 5153
[TakeutiZaring] p. 25Exercise 15resss 5156
[TakeutiZaring] p. 25Exercise 17resabs1 5161
[TakeutiZaring] p. 25Exercise 18funres 5478
[TakeutiZaring] p. 25Exercise 24relco 5354
[TakeutiZaring] p. 25Exercise 29funco 5477
[TakeutiZaring] p. 25Exercise 30f1co 5634
[TakeutiZaring] p. 26Definition 6.10eu2 2305
[TakeutiZaring] p. 26Definition 6.11conventions 21693  df-fv 5448  fv3 5730
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5392  cnvexg 5391
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5118  dmexg 5116
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5119  rnexg 5117
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27567
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27568
[TakeutiZaring] p. 27Corollary 6.13fvex 5728
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 27947  tz6.12-1 5733  tz6.12-afv 27946  tz6.12 5734  tz6.12c 5736
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5705  tz6.12i 5737
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5443
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5444
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5446  wfo 5438
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5445  wf1 5437
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5447  wf1o 5439
[TakeutiZaring] p. 28Exercise 4eqfnfv 5813  eqfnfv2 5814  eqfnfv2f 5817
[TakeutiZaring] p. 28Exercise 5fvco 5785
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5947  fnexALT 5948
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5943  resfunexgALT 5944
[TakeutiZaring] p. 29Exercise 9funimaex 5517  funimaexg 5516
[TakeutiZaring] p. 29Definition 6.18df-br 4200
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4491
[TakeutiZaring] p. 30Definition 6.21dffr2 4534  dffr3 5222  eliniseg 5219  iniseg 5221
[TakeutiZaring] p. 30Definition 6.22df-eprel 4481
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4547  fr3nr 4746  frirr 4546
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4528
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4748
[TakeutiZaring] p. 31Exercise 1frss 4536
[TakeutiZaring] p. 31Exercise 4wess 4556
[TakeutiZaring] p. 31Proposition 6.26tz6.26 25455  tz6.26i 25456  wefrc 4563  wereu2 4566
[TakeutiZaring] p. 32Theorem 6.27wfi 25457  wfii 25458
[TakeutiZaring] p. 32Definition 6.28df-isom 5449
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6035
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6036
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6042
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6043
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6044
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6048
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6055
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6057
[TakeutiZaring] p. 35Notationwtr 4289
[TakeutiZaring] p. 35Theorem 7.2trelpss 27569  tz7.2 4553
[TakeutiZaring] p. 35Definition 7.1dftr3 4293
[TakeutiZaring] p. 36Proposition 7.4ordwe 4581
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4589
[TakeutiZaring] p. 36Proposition 7.6ordelord 4590  ordelordALT 28375  ordelordALTVD 28731
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4596  ordelssne 4595
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4594
[TakeutiZaring] p. 37Proposition 7.9ordin 4598
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4755
[TakeutiZaring] p. 38Corollary 7.15ordsson 4756
[TakeutiZaring] p. 38Definition 7.11df-on 4572
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4600
[TakeutiZaring] p. 38Proposition 7.12onfrALT 28388  ordon 4749
[TakeutiZaring] p. 38Proposition 7.13onprc 4751
[TakeutiZaring] p. 39Theorem 7.17tfi 4819
[TakeutiZaring] p. 40Exercise 3ontr2 4615
[TakeutiZaring] p. 40Exercise 7dftr2 4291
[TakeutiZaring] p. 40Exercise 9onssmin 4763
[TakeutiZaring] p. 40Exercise 11unon 4797
[TakeutiZaring] p. 40Exercise 12ordun 4669
[TakeutiZaring] p. 40Exercise 14ordequn 4668
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4752
[TakeutiZaring] p. 40Proposition 7.20elssuni 4030
[TakeutiZaring] p. 41Definition 7.22df-suc 4574
[TakeutiZaring] p. 41Proposition 7.23sssucid 4645  sucidg 4646
[TakeutiZaring] p. 41Proposition 7.24suceloni 4779
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4659  ordnbtwn 4658
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4794
[TakeutiZaring] p. 42Exercise 1df-lim 4573
[TakeutiZaring] p. 42Exercise 4omssnlim 4845
[TakeutiZaring] p. 42Exercise 7ssnlim 4849
[TakeutiZaring] p. 42Exercise 8onsucssi 4807  ordelsuc 4786
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4788
[TakeutiZaring] p. 42Definition 7.27nlimon 4817
[TakeutiZaring] p. 42Definition 7.28dfom2 4833
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4850
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4851
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4852
[TakeutiZaring] p. 43Remarkomon 4842
[TakeutiZaring] p. 43Axiom 7inf3 7574  omex 7582
[TakeutiZaring] p. 43Theorem 7.32ordom 4840
[TakeutiZaring] p. 43Corollary 7.31find 4856
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4853
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4854
[TakeutiZaring] p. 44Exercise 1limomss 4836
[TakeutiZaring] p. 44Exercise 2int0 4051  trint0 4306
[TakeutiZaring] p. 44Exercise 4intss1 4052
[TakeutiZaring] p. 44Exercise 5intex 4343
[TakeutiZaring] p. 44Exercise 6oninton 4766
[TakeutiZaring] p. 44Exercise 11ordintdif 4617
[TakeutiZaring] p. 44Definition 7.35df-int 4038
[TakeutiZaring] p. 44Proposition 7.34noinfep 7598
[TakeutiZaring] p. 45Exercise 4onint 4761
[TakeutiZaring] p. 47Lemma 1tfrlem1 6622
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6644
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6645
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6646
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6650  tz7.44-2 6651  tz7.44-3 6652
[TakeutiZaring] p. 50Exercise 1smogt 6615
[TakeutiZaring] p. 50Exercise 3smoiso 6610
[TakeutiZaring] p. 50Definition 7.46df-smo 6594
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6688  tz7.49c 6689
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6686
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6685
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6687
[TakeutiZaring] p. 53Proposition 7.532eu5 2364
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7877
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7878
[TakeutiZaring] p. 56Definition 8.1oalim 6762  oasuc 6754
[TakeutiZaring] p. 57Remarktfindsg 4826
[TakeutiZaring] p. 57Proposition 8.2oacl 6765
[TakeutiZaring] p. 57Proposition 8.3oa0 6746  oa0r 6768
[TakeutiZaring] p. 57Proposition 8.16omcl 6766
[TakeutiZaring] p. 58Corollary 8.5oacan 6777
[TakeutiZaring] p. 58Proposition 8.4nnaord 6848  nnaordi 6847  oaord 6776  oaordi 6775
[TakeutiZaring] p. 59Proposition 8.6iunss2 4123  uniss2 4033
[TakeutiZaring] p. 59Proposition 8.7oawordri 6779
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6784  oawordex 6786
[TakeutiZaring] p. 59Proposition 8.9nnacl 6840
[TakeutiZaring] p. 59Proposition 8.10oaabs 6873
[TakeutiZaring] p. 60Remarkoancom 7590
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6789
[TakeutiZaring] p. 62Exercise 1nnarcl 6845
[TakeutiZaring] p. 62Exercise 5oaword1 6781
[TakeutiZaring] p. 62Definition 8.15om0 6747  om0x 6749  omlim 6763  omsuc 6756
[TakeutiZaring] p. 63Proposition 8.17nnecl 6842  nnmcl 6841
[TakeutiZaring] p. 63Proposition 8.19nnmord 6861  nnmordi 6860  omord 6797  omordi 6795
[TakeutiZaring] p. 63Proposition 8.20omcan 6798
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6865  omwordri 6801
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6769
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6771  om1r 6772
[TakeutiZaring] p. 64Proposition 8.22om00 6804
[TakeutiZaring] p. 64Proposition 8.23omordlim 6806
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6807
[TakeutiZaring] p. 64Proposition 8.25odi 6808
[TakeutiZaring] p. 65Theorem 8.26omass 6809
[TakeutiZaring] p. 67Definition 8.30nnesuc 6837  oe0 6752  oelim 6764  oesuc 6757  onesuc 6760
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6750
[TakeutiZaring] p. 67Proposition 8.32oen0 6815
[TakeutiZaring] p. 67Proposition 8.33oeordi 6816
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6751
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6774
[TakeutiZaring] p. 68Corollary 8.34oeord 6817
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6823
[TakeutiZaring] p. 68Proposition 8.35oewordri 6821
[TakeutiZaring] p. 68Proposition 8.37oeworde 6822
[TakeutiZaring] p. 69Proposition 8.41oeoa 6826
[TakeutiZaring] p. 70Proposition 8.42oeoe 6828
[TakeutiZaring] p. 73Theorem 9.1trcl 7648  tz9.1 7649
[TakeutiZaring] p. 76Definition 9.9df-r1 7674  r10 7678  r1lim 7682  r1limg 7681  r1suc 7680  r1sucg 7679
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7690  r1ord2 7691  r1ordg 7688
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7700
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7725  tz9.13 7701  tz9.13g 7702
[TakeutiZaring] p. 79Definition 9.14df-rank 7675  rankval 7726  rankvalb 7707  rankvalg 7727
[TakeutiZaring] p. 79Proposition 9.16rankel 7749  rankelb 7734
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7763  rankval3 7750  rankval3b 7736
[TakeutiZaring] p. 79Proposition 9.18rankonid 7739
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7705
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7744  rankr1c 7731  rankr1g 7742
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7745
[TakeutiZaring] p. 80Exercise 1rankss 7759  rankssb 7758
[TakeutiZaring] p. 80Exercise 2unbndrank 7752
[TakeutiZaring] p. 80Proposition 9.19bndrank 7751
[TakeutiZaring] p. 83Axiom of Choiceac4 8339  dfac3 7986
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7895  numth 8336  numth2 8335
[TakeutiZaring] p. 85Definition 10.4cardval 8405
[TakeutiZaring] p. 85Proposition 10.5cardid 8406  cardid2 7824
[TakeutiZaring] p. 85Proposition 10.9oncard 7831
[TakeutiZaring] p. 85Proposition 10.10carden 8410
[TakeutiZaring] p. 85Proposition 10.11cardidm 7830
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7815
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7836
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7828
[TakeutiZaring] p. 87Proposition 10.15pwen 7266
[TakeutiZaring] p. 88Exercise 1en0 7156
[TakeutiZaring] p. 88Exercise 7infensuc 7271
[TakeutiZaring] p. 89Exercise 10omxpen 7196
[TakeutiZaring] p. 90Corollary 10.23cardnn 7834
[TakeutiZaring] p. 90Definition 10.27alephiso 7963
[TakeutiZaring] p. 90Proposition 10.20nneneq 7276
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7282
[TakeutiZaring] p. 90Proposition 10.26alephprc 7964
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7281
[TakeutiZaring] p. 91Exercise 2alephle 7953
[TakeutiZaring] p. 91Exercise 3aleph0 7931
[TakeutiZaring] p. 91Exercise 4cardlim 7843
[TakeutiZaring] p. 91Exercise 7infpss 8081
[TakeutiZaring] p. 91Exercise 8infcntss 7366
[TakeutiZaring] p. 91Definition 10.29df-fin 7099  isfi 7117
[TakeutiZaring] p. 92Proposition 10.32onfin 7283
[TakeutiZaring] p. 92Proposition 10.34imadomg 8396
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 7189
[TakeutiZaring] p. 93Proposition 10.35fodomb 8388
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8053  unxpdom 7302
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7845  cardsdomelir 7844
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7304
[TakeutiZaring] p. 94Proposition 10.39infxpen 7880
[TakeutiZaring] p. 95Definition 10.42df-map 7006
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8421  infxpidm2 7882
[TakeutiZaring] p. 95Proposition 10.41infcda 8072  infxp 8079
[TakeutiZaring] p. 96Proposition 10.44pw2en 7201  pw2f1o 7199
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7259
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8351
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8346  ac6s5 8355
[TakeutiZaring] p. 98Theorem 10.47unidom 8402
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8403  uniimadomf 8404
[TakeutiZaring] p. 100Definition 11.1cfcof 8138
[TakeutiZaring] p. 101Proposition 11.7cofsmo 8133
[TakeutiZaring] p. 102Exercise 1cfle 8118
[TakeutiZaring] p. 102Exercise 2cf0 8115
[TakeutiZaring] p. 102Exercise 3cfsuc 8121
[TakeutiZaring] p. 102Exercise 4cfom 8128
[TakeutiZaring] p. 102Proposition 11.9coftr 8137
[TakeutiZaring] p. 103Theorem 11.15alephreg 8441
[TakeutiZaring] p. 103Proposition 11.11cardcf 8116
[TakeutiZaring] p. 103Proposition 11.13alephsing 8140
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7962
[TakeutiZaring] p. 104Proposition 11.16carduniima 7961
[TakeutiZaring] p. 104Proposition 11.18alephfp 7973  alephfp2 7974
[TakeutiZaring] p. 106Theorem 11.20gchina 8558
[TakeutiZaring] p. 106Theorem 11.21mappwen 7977
[TakeutiZaring] p. 107Theorem 11.26konigth 8428
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8442
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8443
[Tarski] p. 67Axiom B5ax-4 2211
[Tarski] p. 67Scheme B5sp 1763
[Tarski] p. 68Lemma 6avril1 21740  equid 1688  equid1 2234  equid1ALT 2252
[Tarski] p. 69Lemma 7equcomi 1691
[Tarski] p. 70Lemma 14spim 1957  spime 1962  spimeh 1679
[Tarski] p. 70Lemma 16ax-11 1761  ax-11o 2217  ax11i 1657
[Tarski] p. 70Lemmas 16 and 17sb6 2174
[Tarski] p. 75Axiom B7ax9v 1667
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1626  ax17o 2233
[Tarski], p. 75Scheme B8 of system S2ax-13 1727  ax-14 1729  ax-8 1687
[Truss] p. 114Theorem 5.18ruc 12825
[Viaclovsky7] p. 3Proposition 0.3mblfinlem2 26186
[Viaclovsky8] p. 3Proposition 7ismblfin 26188
[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 2377  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 28791
[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 21693  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 26173
[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 26166
[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 27463
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27464
[WhiteheadRussell] p. 147Theorem *10.2219.26 1603
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27465
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27466
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27467
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1625
[WhiteheadRussell] p. 151Theorem *10.301albitr 27468
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27469
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27470
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27471
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27472
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27474
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27475
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27476
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27473
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2190
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27479
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27480
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27481
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1753
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27482
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27483
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27484
[WhiteheadRussell] p. 162Theorem *11.322alim 27485
[WhiteheadRussell] p. 162Theorem *11.332albi 27486
[WhiteheadRussell] p. 162Theorem *11.342exim 27487
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27489
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27488
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1620
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27491
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27492
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27490
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1582
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27493
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27494
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1590
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27495
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1916
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27496
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27501
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27497
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27498
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27499
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27500
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27505
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27502
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27503
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27504
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27506
[WhiteheadRussell] p. 175Definition *14.02df-eu 2284
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27517  pm13.13b 27518
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27519
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2665
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2666
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3063
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27525
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27526
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27520
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 28392  pm13.193 27521
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27522
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27523
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27524
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27531
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27530
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27529
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3200
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27532  pm14.122b 27533  pm14.122c 27534
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27535  pm14.123b 27536  pm14.123c 27537
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27539
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27538
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27540
[WhiteheadRussell] p. 190Theorem *14.22iota4 5422
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27541
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5423
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27542
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27544
[WhiteheadRussell] p. 192Theorem *14.26eupick 2343  eupickbi 2346  sbaniota 27545
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27543
[WhiteheadRussell] p. 192Theorem *14.271eubi 27546
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27547
[WhiteheadRussell] p. 235Definition *30.01conventions 21693  df-fv 5448
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7871  pm54.43lem 7870
[Young] p. 141Definition of operator orderingleop2 23610
[Young] p. 142Example 12.2(i)0leop 23616  idleop 23617
[vandenDries] p. 42Lemma 61irrapx1 26823
[vandenDries] p. 43Theorem 62pellex 26830  pellexlem1 26824

This page was last updated on 15-May-2018.
Copyright terms: Public domain