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 13936
[Adamek] p. 29Proposition 3.14(1)invinv 13950
[Adamek] p. 29Proposition 3.14(2)invco 13951  isoco 13953
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18695  df-nmoo 22199
[AkhiezerGlazman] p. 64Theoremhmopidmch 23609  hmopidmchi 23607
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 23657  pjcmul2i 23658
[AkhiezerGlazman] p. 72Theoremcnvunop 23374  unoplin 23376
[AkhiezerGlazman] p. 72Equation 2unopadj 23375  unopadj2 23394
[AkhiezerGlazman] p. 73Theoremelunop2 23469  lnopunii 23468
[AkhiezerGlazman] p. 80Proposition 1adjlnop 23542
[Apostol] p. 18Theorem I.1addcan 9206  addcan2d 9226  addcan2i 9216  addcand 9225  addcani 9215
[Apostol] p. 18Theorem I.2negeu 9252
[Apostol] p. 18Theorem I.3negsub 9305  negsubd 9373  negsubi 9334
[Apostol] p. 18Theorem I.4negneg 9307  negnegd 9358  negnegi 9326
[Apostol] p. 18Theorem I.5subdi 9423  subdid 9445  subdii 9438  subdir 9424  subdird 9446  subdiri 9439
[Apostol] p. 18Theorem I.6mul01 9201  mul01d 9221  mul01i 9212  mul02 9200  mul02d 9220  mul02i 9211
[Apostol] p. 18Theorem I.7mulcan 9615  mulcan2d 9612  mulcand 9611  mulcani 9617
[Apostol] p. 18Theorem I.8receu 9623  xreceu 24121
[Apostol] p. 18Theorem I.9divrec 9650  divrecd 9749  divreci 9715  divreczi 9708
[Apostol] p. 18Theorem I.10recrec 9667  recreci 9702
[Apostol] p. 18Theorem I.11mul0or 9618  mul0ord 9628  mul0ori 9626
[Apostol] p. 18Theorem I.12mul2neg 9429  mul2negd 9444  mul2negi 9437  mulneg1 9426  mulneg1d 9442  mulneg1i 9435
[Apostol] p. 18Theorem I.13divadddiv 9685  divadddivd 9790  divadddivi 9732
[Apostol] p. 18Theorem I.14divmuldiv 9670  divmuldivd 9787  divmuldivi 9730  rdivmuldivd 24180
[Apostol] p. 18Theorem I.15divdivdiv 9671  divdivdivd 9793  divdivdivi 9733
[Apostol] p. 20Axiom 7rpaddcl 10588  rpaddcld 10619  rpmulcl 10589  rpmulcld 10620
[Apostol] p. 20Axiom 8rpneg 10597
[Apostol] p. 20Axiom 90nrp 10598
[Apostol] p. 20Theorem I.17lttri 9155
[Apostol] p. 20Theorem I.18ltadd1d 9575  ltadd1dd 9593  ltadd1i 9537
[Apostol] p. 20Theorem I.19ltmul1 9816  ltmul1a 9815  ltmul1i 9885  ltmul1ii 9895  ltmul2 9817  ltmul2d 10642  ltmul2dd 10656  ltmul2i 9888
[Apostol] p. 20Theorem I.20msqgt0 9504  msqgt0d 9550  msqgt0i 9520
[Apostol] p. 20Theorem I.210lt1 9506
[Apostol] p. 20Theorem I.23lt0neg1 9490  lt0neg1d 9552  ltneg 9484  ltnegd 9560  ltnegi 9527
[Apostol] p. 20Theorem I.25lt2add 9469  lt2addd 9604  lt2addi 9545
[Apostol] p. 20Definition of positive numbersdf-rp 10569
[Apostol] p. 21Exercise 4recgt0 9810  recgt0d 9901  recgt0i 9871  recgt0ii 9872
[Apostol] p. 22Definition of integersdf-z 10239
[Apostol] p. 22Definition of positive integersdfnn3 9970
[Apostol] p. 22Definition of rationalsdf-q 10531
[Apostol] p. 24Theorem I.26supeu 7415
[Apostol] p. 26Theorem I.28nnunb 10173
[Apostol] p. 26Theorem I.29arch 10174
[Apostol] p. 28Exercise 2btwnz 10328
[Apostol] p. 28Exercise 3nnrecl 10175
[Apostol] p. 28Exercise 4rebtwnz 10529
[Apostol] p. 28Exercise 5zbtwnre 10528
[Apostol] p. 28Exercise 6qbtwnre 10741
[Apostol] p. 28Exercise 10(a)zneo 10308
[Apostol] p. 29Theorem I.35msqsqrd 12197  resqrth 12016  sqrth 12123  sqrthi 12129  sqsqrd 12196
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9959
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10498
[Apostol] p. 361Remarkcrreczi 11459
[Apostol] p. 363Remarkabsgt0i 12157
[Apostol] p. 363Exampleabssubd 12210  abssubi 12161
[Baer] p. 40Property (b)mapdord 32121
[Baer] p. 40Property (c)mapd11 32122
[Baer] p. 40Property (e)mapdin 32145  mapdlsm 32147
[Baer] p. 40Property (f)mapd0 32148
[Baer] p. 40Definition of projectivitydf-mapd 32108  mapd1o 32131
[Baer] p. 41Property (g)mapdat 32150
[Baer] p. 44Part (1)mapdpg 32189
[Baer] p. 45Part (2)hdmap1eq 32285  mapdheq 32211  mapdheq2 32212  mapdheq2biN 32213
[Baer] p. 45Part (3)baerlem3 32196
[Baer] p. 46Part (4)mapdheq4 32215  mapdheq4lem 32214
[Baer] p. 46Part (5)baerlem5a 32197  baerlem5abmN 32201  baerlem5amN 32199  baerlem5b 32198  baerlem5bmN 32200
[Baer] p. 47Part (6)hdmap1l6 32305  hdmap1l6a 32293  hdmap1l6e 32298  hdmap1l6f 32299  hdmap1l6g 32300  hdmap1l6lem1 32291  hdmap1l6lem2 32292  hdmap1p6N 32306  mapdh6N 32230  mapdh6aN 32218  mapdh6eN 32223  mapdh6fN 32224  mapdh6gN 32225  mapdh6lem1N 32216  mapdh6lem2N 32217
[Baer] p. 48Part 9hdmapval 32314
[Baer] p. 48Part 10hdmap10 32326
[Baer] p. 48Part 11hdmapadd 32329
[Baer] p. 48Part (6)hdmap1l6h 32301  mapdh6hN 32226
[Baer] p. 48Part (7)mapdh75cN 32236  mapdh75d 32237  mapdh75e 32235  mapdh75fN 32238  mapdh7cN 32232  mapdh7dN 32233  mapdh7eN 32231  mapdh7fN 32234
[Baer] p. 48Part (8)mapdh8 32272  mapdh8a 32258  mapdh8aa 32259  mapdh8ab 32260  mapdh8ac 32261  mapdh8ad 32262  mapdh8b 32263  mapdh8c 32264  mapdh8d 32266  mapdh8d0N 32265  mapdh8e 32267  mapdh8fN 32268  mapdh8g 32269  mapdh8i 32270  mapdh8j 32271
[Baer] p. 48Part (9)mapdh9a 32273
[Baer] p. 48Equation 10mapdhvmap 32252
[Baer] p. 49Part 12hdmap11 32334  hdmapeq0 32330  hdmapf1oN 32351  hdmapneg 32332  hdmaprnN 32350  hdmaprnlem1N 32335  hdmaprnlem3N 32336  hdmaprnlem3uN 32337  hdmaprnlem4N 32339  hdmaprnlem6N 32340  hdmaprnlem7N 32341  hdmaprnlem8N 32342  hdmaprnlem9N 32343  hdmapsub 32333
[Baer] p. 49Part 14hdmap14lem1 32354  hdmap14lem10 32363  hdmap14lem1a 32352  hdmap14lem2N 32355  hdmap14lem2a 32353  hdmap14lem3 32356  hdmap14lem8 32361  hdmap14lem9 32362
[Baer] p. 50Part 14hdmap14lem11 32364  hdmap14lem12 32365  hdmap14lem13 32366  hdmap14lem14 32367  hdmap14lem15 32368  hgmapval 32373
[Baer] p. 50Part 15hgmapadd 32380  hgmapmul 32381  hgmaprnlem2N 32383  hgmapvs 32377
[Baer] p. 50Part 16hgmaprnN 32387
[Baer] p. 110Lemma 1hdmapip0com 32403
[Baer] p. 110Line 27hdmapinvlem1 32404
[Baer] p. 110Line 28hdmapinvlem2 32405
[Baer] p. 110Line 30hdmapinvlem3 32406
[Baer] p. 110Part 1.2hdmapglem5 32408  hgmapvv 32412
[Baer] p. 110Proposition 1hdmapinvlem4 32407
[Baer] p. 111Line 10hgmapvvlem1 32409
[Baer] p. 111Line 15hdmapg 32416  hdmapglem7 32415
[BellMachover] p. 36Lemma 10.3id1 21
[BellMachover] p. 97Definition 10.1df-eu 2258
[BellMachover] p. 460Notationdf-mo 2259
[BellMachover] p. 460Definitionmo3 2285
[BellMachover] p. 461Axiom Extax-ext 2385
[BellMachover] p. 462Theorem 1.1bm1.1 2389
[BellMachover] p. 463Axiom Repaxrep5 4285
[BellMachover] p. 463Scheme Sepaxsep 4289
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4293
[BellMachover] p. 466Axiom Powaxpow3 4340
[BellMachover] p. 466Axiom Unionaxun2 4662
[BellMachover] p. 468Definitiondf-ord 4544
[BellMachover] p. 469Theorem 2.2(i)ordirr 4559
[BellMachover] p. 469Theorem 2.2(iii)onelon 4566
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4561
[BellMachover] p. 471Definition of Ndf-om 4805
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4745
[BellMachover] p. 471Definition of Limdf-lim 4546
[BellMachover] p. 472Axiom Infzfinf2 7553
[BellMachover] p. 473Theorem 2.8limom 4819
[BellMachover] p. 477Equation 3.1df-r1 7646
[BellMachover] p. 478Definitionrankval2 7700
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7664  r1ord3g 7661
[BellMachover] p. 480Axiom Regzfreg2 7520
[BellMachover] p. 488Axiom ACac5 8313  dfac4 7959
[BellMachover] p. 490Definition of alephalephval3 7947
[BeltramettiCassinelli] p. 98Remarkatlatmstc 29802
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 23809
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 23851  chirredi 23850
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 23839
[Beran] p. 3Definition of joinsshjval3 22809
[Beran] p. 39Theorem 2.3(i)cmcm2 23071  cmcm2i 23048  cmcm2ii 23053  cmt2N 29733
[Beran] p. 40Theorem 2.3(iii)lecm 23072  lecmi 23057  lecmii 23058
[Beran] p. 45Theorem 3.4cmcmlem 23046
[Beran] p. 49Theorem 4.2cm2j 23075  cm2ji 23080  cm2mi 23081
[Beran] p. 95Definitiondf-sh 22662  issh2 22664
[Beran] p. 95Lemma 3.1(S5)his5 22541
[Beran] p. 95Lemma 3.1(S6)his6 22554
[Beran] p. 95Lemma 3.1(S7)his7 22545
[Beran] p. 95Lemma 3.2(S8)ho01i 23284
[Beran] p. 95Lemma 3.2(S9)hoeq1 23286
[Beran] p. 95Lemma 3.2(S10)ho02i 23285
[Beran] p. 95Lemma 3.2(S11)hoeq2 23287
[Beran] p. 95Postulate (S1)ax-his1 22537  his1i 22555
[Beran] p. 95Postulate (S2)ax-his2 22538
[Beran] p. 95Postulate (S3)ax-his3 22539
[Beran] p. 95Postulate (S4)ax-his4 22540
[Beran] p. 96Definition of normdf-hnorm 22424  dfhnorm2 22577  normval 22579
[Beran] p. 96Definition for Cauchy sequencehcau 22639
[Beran] p. 96Definition of Cauchy sequencedf-hcau 22429
[Beran] p. 96Definition of complete subspaceisch3 22697
[Beran] p. 96Definition of convergedf-hlim 22428  hlimi 22643
[Beran] p. 97Theorem 3.3(i)norm-i-i 22588  norm-i 22584
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 22592  norm-ii 22593  normlem0 22564  normlem1 22565  normlem2 22566  normlem3 22567  normlem4 22568  normlem5 22569  normlem6 22570  normlem7 22571  normlem7tALT 22574
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 22594  norm-iii 22595
[Beran] p. 98Remark 3.4bcs 22636  bcsiALT 22634  bcsiHIL 22635
[Beran] p. 98Remark 3.4(B)normlem9at 22576  normpar 22610  normpari 22609
[Beran] p. 98Remark 3.4(C)normpyc 22601  normpyth 22600  normpythi 22597
[Beran] p. 99Remarklnfn0 23503  lnfn0i 23498  lnop0 23422  lnop0i 23426
[Beran] p. 99Theorem 3.5(i)nmcexi 23482  nmcfnex 23509  nmcfnexi 23507  nmcopex 23485  nmcopexi 23483
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 23510  nmcfnlbi 23508  nmcoplb 23486  nmcoplbi 23484
[Beran] p. 99Theorem 3.5(iii)lnfncon 23512  lnfnconi 23511  lnopcon 23491  lnopconi 23490
[Beran] p. 100Lemma 3.6normpar2i 22611
[Beran] p. 101Lemma 3.6norm3adifi 22608  norm3adifii 22603  norm3dif 22605  norm3difi 22602
[Beran] p. 102Theorem 3.7(i)chocunii 22756  pjhth 22848  pjhtheu 22849  pjpjhth 22880  pjpjhthi 22881  pjth 19293
[Beran] p. 102Theorem 3.7(ii)ococ 22861  ococi 22860
[Beran] p. 103Remark 3.8nlelchi 23517
[Beran] p. 104Theorem 3.9riesz3i 23518  riesz4 23520  riesz4i 23519
[Beran] p. 104Theorem 3.10cnlnadj 23535  cnlnadjeu 23534  cnlnadjeui 23533  cnlnadji 23532  cnlnadjlem1 23523  nmopadjlei 23544
[Beran] p. 106Theorem 3.11(i)adjeq0 23547
[Beran] p. 106Theorem 3.11(v)nmopadji 23546
[Beran] p. 106Theorem 3.11(ii)adjmul 23548
[Beran] p. 106Theorem 3.11(iv)adjadj 23392
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 23558  nmopcoadji 23557
[Beran] p. 106Theorem 3.11(iii)adjadd 23549
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 23559
[Beran] p. 106Theorem 3.11(viii)adjcoi 23556  pjadj2coi 23660  pjadjcoi 23617
[Beran] p. 107Definitiondf-ch 22677  isch2 22679
[Beran] p. 107Remark 3.12choccl 22761  isch3 22697  occl 22759  ocsh 22738  shoccl 22760  shocsh 22739
[Beran] p. 107Remark 3.12(B)ococin 22863
[Beran] p. 108Theorem 3.13chintcl 22787
[Beran] p. 109Property (i)pjadj2 23643  pjadj3 23644  pjadji 23140  pjadjii 23129
[Beran] p. 109Property (ii)pjidmco 23637  pjidmcoi 23633  pjidmi 23128
[Beran] p. 110Definition of projector orderingpjordi 23629
[Beran] p. 111Remarkho0val 23206  pjch1 23125
[Beran] p. 111Definitiondf-hfmul 23190  df-hfsum 23189  df-hodif 23188  df-homul 23187  df-hosum 23186
[Beran] p. 111Lemma 4.4(i)pjo 23126
[Beran] p. 111Lemma 4.4(ii)pjch 23149  pjchi 22887
[Beran] p. 111Lemma 4.4(iii)pjoc2 22894  pjoc2i 22893
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 23135
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 23621  pjssmii 23136
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 23620
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 23619
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 23624
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 23622  pjssge0ii 23137
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 23623  pjdifnormii 23138
[Bogachev] p. 116Definition 2.3.1df-itgm 24617  df-sitm 24599
[Bogachev] p. 118Chapter 2.4.4df-itgm 24617
[Bogachev] p. 118Definition 2.4.1df-sitg 24598
[Bollobas] p. 4Definitiondf-wlk 21469
[Bollobas] p. 5Notationdf-pth 21471
[Bollobas] p. 5Definitiondf-crct 21473  df-cycl 21474  df-trail 21470  df-wlkon 21475
[BourbakiEns] p. Proposition 8fcof1 5979  fcofo 5980
[BourbakiTop1] p. Remarkxnegmnf 10752  xnegpnf 10751
[BourbakiTop1] p. Remark rexneg 10753
[BourbakiTop1] p. Theoremneiss 17128
[BourbakiTop1] p. Remark 3ust0 18202  ustfilxp 18195
[BourbakiTop1] p. Axiom GT'tgpsubcn 18073
[BourbakiTop1] p. Example 1cstucnd 18267  iducn 18266  snfil 17849
[BourbakiTop1] p. Example 2neifil 17865
[BourbakiTop1] p. Theorem 1cnextcn 18051
[BourbakiTop1] p. Theorem 2ucnextcn 18287
[BourbakiTop1] p. Theorem 3df-hcmp 24294
[BourbakiTop1] p. Definitionistgp 18060
[BourbakiTop1] p. Propositioncnpco 17285  ishmeo 17744  neips 17132
[BourbakiTop1] p. Definition 1df-ucn 18259  df-ust 18183  filintn0 17846  ucnprima 18265
[BourbakiTop1] p. Definition 2df-cfilu 18270
[BourbakiTop1] p. Definition 3df-cusp 18281  df-usp 18240  df-utop 18214  trust 18212
[BourbakiTop1] p. Condition F_Iustssel 18188
[BourbakiTop1] p. Condition U_Iustdiag 18191
[BourbakiTop1] p. Property V_ivneiptopreu 17152
[BourbakiTop1] p. Proposition 1ucncn 18268  ustund 18204  ustuqtop 18229
[BourbakiTop1] p. Proposition 2neiptopreu 17152  utop2nei 18233  utop3cls 18234
[BourbakiTop1] p. Proposition 3fmucnd 18275  uspreg 18257  utopreg 18235
[BourbakiTop1] p. Proposition 4imasncld 17676  imasncls 17677  imasnopn 17675
[BourbakiTop1] p. Proposition 9cnpflf2 17985
[BourbakiTop1] p. Theorem 1 (d)iscncl 17287
[BourbakiTop1] p. Condition F_IIustincl 18190
[BourbakiTop1] p. Condition U_IIustinvel 18192
[BourbakiTop1] p. Proposition 11cnextucn 18286
[BourbakiTop1] p. Proposition Vissnei2 17135
[BourbakiTop1] p. Condition F_IIbustbasel 18189
[BourbakiTop1] p. Condition U_IIIustexhalf 18193
[BourbakiTop1] p. Definition C'''df-cmp 17404
[BourbakiTop1] p. Proposition Viiinnei 17144
[BourbakiTop1] p. Proposition Vivneissex 17146
[BourbakiTop1] p. Proposition Viiielnei 17130  ssnei 17129
[BourbakiTop1] p. Remark below def. 1filn0 17847
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17831
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17848
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27680  stoweid 27679
[BrosowskiDeutsh] p. 89Theorem for the non-trivial casestoweidlem62 27678
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27617  stoweidlem10 27626  stoweidlem14 27630  stoweidlem15 27631  stoweidlem35 27651  stoweidlem36 27652  stoweidlem37 27653  stoweidlem38 27654  stoweidlem40 27656  stoweidlem41 27657  stoweidlem43 27659  stoweidlem44 27660  stoweidlem46 27662  stoweidlem5 27621  stoweidlem50 27666  stoweidlem52 27668  stoweidlem53 27669  stoweidlem55 27671  stoweidlem56 27672
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27639  stoweidlem24 27640  stoweidlem27 27643  stoweidlem28 27644  stoweidlem30 27646
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27661  stoweidlem49 27665  stoweidlem7 27623
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27647  stoweidlem39 27655  stoweidlem42 27658  stoweidlem48 27664  stoweidlem51 27667  stoweidlem54 27670  stoweidlem57 27673  stoweidlem58 27674
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27641
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27650
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27633
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27675
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27676
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27634
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27627  stoweidlem26 27642
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27629
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27677
[ChoquetDD] p. 2Definition of mappingdf-mpt 4228
[Clemente] p. 10Definition ITnatded 21664
[Clemente] p. 10Definition I` `m,nnatded 21664
[Clemente] p. 11Definition E=>m,nnatded 21664
[Clemente] p. 11Definition I=>m,nnatded 21664
[Clemente] p. 11Definition E` `(1)natded 21664
[Clemente] p. 11Definition E` `(2)natded 21664
[Clemente] p. 12Definition E` `m,n,pnatded 21664
[Clemente] p. 12Definition I` `n(1)natded 21664
[Clemente] p. 12Definition I` `n(2)natded 21664
[Clemente] p. 13Definition I` `m,n,pnatded 21664
[Clemente] p. 14Definition E` `nnatded 21664
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 21666  ex-natded5.2 21665
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 21669  ex-natded5.3 21668
[Clemente] p. 18Theorem 5.5ex-natded5.5 21671
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 21673  ex-natded5.7 21672
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 21675  ex-natded5.8 21674
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 21677  ex-natded5.13 21676
[Clemente] p. 32Definition I` `nnatded 21664
[Clemente] p. 32Definition E` `m,n,p,anatded 21664
[Clemente] p. 32Definition E` `n,tnatded 21664
[Clemente] p. 32Definition I` `n,tnatded 21664
[Clemente] p. 43Theorem 9.20ex-natded9.20 21678
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 21679
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 21681  ex-natded9.26 21680
[Cohen] p. 301Remarkrelogoprlem 20438
[Cohen] p. 301Property 2relogmul 20439  relogmuld 20473
[Cohen] p. 301Property 3relogdiv 20440  relogdivd 20474
[Cohen] p. 301Property 4relogexp 20443
[Cohen] p. 301Property 1alog1 20433
[Cohen] p. 301Property 1bloge 20434
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 24588  sxbrsigalem4 24590
[Cohn] p. 81Section II.5acsdomd 14562  acsinfd 14561  acsinfdimd 14563  acsmap2d 14560  acsmapd 14559
[Cohn] p. 143Example 5.1.1sxbrsiga 24593
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 11197
[Crawley] p. 1Definition of posetdf-poset 14358
[Crawley] p. 107Theorem 13.2hlsupr 29868
[Crawley] p. 110Theorem 13.3arglem1N 30672  dalaw 30368
[Crawley] p. 111Theorem 13.4hlathil 32447
[Crawley] p. 111Definition of set Wdf-watsN 30472
[Crawley] p. 111Definition of dilationdf-dilN 30588  df-ldil 30586  isldil 30592
[Crawley] p. 111Definition of translationdf-ltrn 30587  df-trnN 30589  isltrn 30601  ltrnu 30603
[Crawley] p. 112Lemma Acdlema1N 30273  cdlema2N 30274  exatleN 29886
[Crawley] p. 112Lemma B1cvrat 29958  cdlemb 30276  cdlemb2 30523  cdlemb3 31088  idltrn 30632  l1cvat 29538  lhpat 30525  lhpat2 30527  lshpat 29539  ltrnel 30621  ltrnmw 30633
[Crawley] p. 112Lemma Ccdlemc1 30673  cdlemc2 30674  ltrnnidn 30656  trlat 30651  trljat1 30648  trljat2 30649  trljat3 30650  trlne 30667  trlnidat 30655  trlnle 30668
[Crawley] p. 112Definition of automorphismdf-pautN 30473
[Crawley] p. 113Lemma Ccdlemc 30679  cdlemc3 30675  cdlemc4 30676
[Crawley] p. 113Lemma Dcdlemd 30689  cdlemd1 30680  cdlemd2 30681  cdlemd3 30682  cdlemd4 30683  cdlemd5 30684  cdlemd6 30685  cdlemd7 30686  cdlemd8 30687  cdlemd9 30688  cdleme31sde 30867  cdleme31se 30864  cdleme31se2 30865  cdleme31snd 30868  cdleme32a 30923  cdleme32b 30924  cdleme32c 30925  cdleme32d 30926  cdleme32e 30927  cdleme32f 30928  cdleme32fva 30919  cdleme32fva1 30920  cdleme32fvcl 30922  cdleme32le 30929  cdleme48fv 30981  cdleme4gfv 30989  cdleme50eq 31023  cdleme50f 31024  cdleme50f1 31025  cdleme50f1o 31028  cdleme50laut 31029  cdleme50ldil 31030  cdleme50lebi 31022  cdleme50rn 31027  cdleme50rnlem 31026  cdlemeg49le 30993  cdlemeg49lebilem 31021
[Crawley] p. 113Lemma Ecdleme 31042  cdleme00a 30691  cdleme01N 30703  cdleme02N 30704  cdleme0a 30693  cdleme0aa 30692  cdleme0b 30694  cdleme0c 30695  cdleme0cp 30696  cdleme0cq 30697  cdleme0dN 30698  cdleme0e 30699  cdleme0ex1N 30705  cdleme0ex2N 30706  cdleme0fN 30700  cdleme0gN 30701  cdleme0moN 30707  cdleme1 30709  cdleme10 30736  cdleme10tN 30740  cdleme11 30752  cdleme11a 30742  cdleme11c 30743  cdleme11dN 30744  cdleme11e 30745  cdleme11fN 30746  cdleme11g 30747  cdleme11h 30748  cdleme11j 30749  cdleme11k 30750  cdleme11l 30751  cdleme12 30753  cdleme13 30754  cdleme14 30755  cdleme15 30760  cdleme15a 30756  cdleme15b 30757  cdleme15c 30758  cdleme15d 30759  cdleme16 30767  cdleme16aN 30741  cdleme16b 30761  cdleme16c 30762  cdleme16d 30763  cdleme16e 30764  cdleme16f 30765  cdleme16g 30766  cdleme19a 30785  cdleme19b 30786  cdleme19c 30787  cdleme19d 30788  cdleme19e 30789  cdleme19f 30790  cdleme1b 30708  cdleme2 30710  cdleme20aN 30791  cdleme20bN 30792  cdleme20c 30793  cdleme20d 30794  cdleme20e 30795  cdleme20f 30796  cdleme20g 30797  cdleme20h 30798  cdleme20i 30799  cdleme20j 30800  cdleme20k 30801  cdleme20l 30804  cdleme20l1 30802  cdleme20l2 30803  cdleme20m 30805  cdleme20y 30784  cdleme20zN 30783  cdleme21 30819  cdleme21d 30812  cdleme21e 30813  cdleme22a 30822  cdleme22aa 30821  cdleme22b 30823  cdleme22cN 30824  cdleme22d 30825  cdleme22e 30826  cdleme22eALTN 30827  cdleme22f 30828  cdleme22f2 30829  cdleme22g 30830  cdleme23a 30831  cdleme23b 30832  cdleme23c 30833  cdleme26e 30841  cdleme26eALTN 30843  cdleme26ee 30842  cdleme26f 30845  cdleme26f2 30847  cdleme26f2ALTN 30846  cdleme26fALTN 30844  cdleme27N 30851  cdleme27a 30849  cdleme27cl 30848  cdleme28c 30854  cdleme3 30719  cdleme30a 30860  cdleme31fv 30872  cdleme31fv1 30873  cdleme31fv1s 30874  cdleme31fv2 30875  cdleme31id 30876  cdleme31sc 30866  cdleme31sdnN 30869  cdleme31sn 30862  cdleme31sn1 30863  cdleme31sn1c 30870  cdleme31sn2 30871  cdleme31so 30861  cdleme35a 30930  cdleme35b 30932  cdleme35c 30933  cdleme35d 30934  cdleme35e 30935  cdleme35f 30936  cdleme35fnpq 30931  cdleme35g 30937  cdleme35h 30938  cdleme35h2 30939  cdleme35sn2aw 30940  cdleme35sn3a 30941  cdleme36a 30942  cdleme36m 30943  cdleme37m 30944  cdleme38m 30945  cdleme38n 30946  cdleme39a 30947  cdleme39n 30948  cdleme3b 30711  cdleme3c 30712  cdleme3d 30713  cdleme3e 30714  cdleme3fN 30715  cdleme3fa 30718  cdleme3g 30716  cdleme3h 30717  cdleme4 30720  cdleme40m 30949  cdleme40n 30950  cdleme40v 30951  cdleme40w 30952  cdleme41fva11 30959  cdleme41sn3aw 30956  cdleme41sn4aw 30957  cdleme41snaw 30958  cdleme42a 30953  cdleme42b 30960  cdleme42c 30954  cdleme42d 30955  cdleme42e 30961  cdleme42f 30962  cdleme42g 30963  cdleme42h 30964  cdleme42i 30965  cdleme42k 30966  cdleme42ke 30967  cdleme42keg 30968  cdleme42mN 30969  cdleme42mgN 30970  cdleme43aN 30971  cdleme43bN 30972  cdleme43cN 30973  cdleme43dN 30974  cdleme5 30722  cdleme50ex 31041  cdleme50ltrn 31039  cdleme51finvN 31038  cdleme51finvfvN 31037  cdleme51finvtrN 31040  cdleme6 30723  cdleme7 30731  cdleme7a 30725  cdleme7aa 30724  cdleme7b 30726  cdleme7c 30727  cdleme7d 30728  cdleme7e 30729  cdleme7ga 30730  cdleme8 30732  cdleme8tN 30737  cdleme9 30735  cdleme9a 30733  cdleme9b 30734  cdleme9tN 30739  cdleme9taN 30738  cdlemeda 30780  cdlemedb 30779  cdlemednpq 30781  cdlemednuN 30782  cdlemefr27cl 30885  cdlemefr32fva1 30892  cdlemefr32fvaN 30891  cdlemefrs32fva 30882  cdlemefrs32fva1 30883  cdlemefs27cl 30895  cdlemefs32fva1 30905  cdlemefs32fvaN 30904  cdlemesner 30778  cdlemeulpq 30702
[Crawley] p. 114Lemma E4atex 30558  4atexlem7 30557  cdleme0nex 30772  cdleme17a 30768  cdleme17c 30770  cdleme17d 30980  cdleme17d1 30771  cdleme17d2 30977  cdleme18a 30773  cdleme18b 30774  cdleme18c 30775  cdleme18d 30777  cdleme4a 30721
[Crawley] p. 115Lemma Ecdleme21a 30807  cdleme21at 30810  cdleme21b 30808  cdleme21c 30809  cdleme21ct 30811  cdleme21f 30814  cdleme21g 30815  cdleme21h 30816  cdleme21i 30817  cdleme22gb 30776
[Crawley] p. 116Lemma Fcdlemf 31045  cdlemf1 31043  cdlemf2 31044
[Crawley] p. 116Lemma Gcdlemftr1 31049  cdlemg16 31139  cdlemg28 31186  cdlemg28a 31175  cdlemg28b 31185  cdlemg3a 31079  cdlemg42 31211  cdlemg43 31212  cdlemg44 31215  cdlemg44a 31213  cdlemg46 31217  cdlemg47 31218  cdlemg9 31116  ltrnco 31201  ltrncom 31220  tgrpabl 31233  trlco 31209
[Crawley] p. 116Definition of Gdf-tgrp 31225
[Crawley] p. 117Lemma Gcdlemg17 31159  cdlemg17b 31144
[Crawley] p. 117Definition of Edf-edring-rN 31238  df-edring 31239
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 31242
[Crawley] p. 118Remarktendopltp 31262
[Crawley] p. 118Lemma Hcdlemh 31299  cdlemh1 31297  cdlemh2 31298
[Crawley] p. 118Lemma Icdlemi 31302  cdlemi1 31300  cdlemi2 31301
[Crawley] p. 118Lemma Jcdlemj1 31303  cdlemj2 31304  cdlemj3 31305  tendocan 31306
[Crawley] p. 118Lemma Kcdlemk 31456  cdlemk1 31313  cdlemk10 31325  cdlemk11 31331  cdlemk11t 31428  cdlemk11ta 31411  cdlemk11tb 31413  cdlemk11tc 31427  cdlemk11u-2N 31371  cdlemk11u 31353  cdlemk12 31332  cdlemk12u-2N 31372  cdlemk12u 31354  cdlemk13-2N 31358  cdlemk13 31334  cdlemk14-2N 31360  cdlemk14 31336  cdlemk15-2N 31361  cdlemk15 31337  cdlemk16-2N 31362  cdlemk16 31339  cdlemk16a 31338  cdlemk17-2N 31363  cdlemk17 31340  cdlemk18-2N 31368  cdlemk18-3N 31382  cdlemk18 31350  cdlemk19-2N 31369  cdlemk19 31351  cdlemk19u 31452  cdlemk1u 31341  cdlemk2 31314  cdlemk20-2N 31374  cdlemk20 31356  cdlemk21-2N 31373  cdlemk21N 31355  cdlemk22-3 31383  cdlemk22 31375  cdlemk23-3 31384  cdlemk24-3 31385  cdlemk25-3 31386  cdlemk26-3 31388  cdlemk26b-3 31387  cdlemk27-3 31389  cdlemk28-3 31390  cdlemk29-3 31393  cdlemk3 31315  cdlemk30 31376  cdlemk31 31378  cdlemk32 31379  cdlemk33N 31391  cdlemk34 31392  cdlemk35 31394  cdlemk36 31395  cdlemk37 31396  cdlemk38 31397  cdlemk39 31398  cdlemk39u 31450  cdlemk4 31316  cdlemk41 31402  cdlemk42 31423  cdlemk42yN 31426  cdlemk43N 31445  cdlemk45 31429  cdlemk46 31430  cdlemk47 31431  cdlemk48 31432  cdlemk49 31433  cdlemk5 31318  cdlemk50 31434  cdlemk51 31435  cdlemk52 31436  cdlemk53 31439  cdlemk54 31440  cdlemk55 31443  cdlemk55u 31448  cdlemk56 31453  cdlemk5a 31317  cdlemk5auN 31342  cdlemk5u 31343  cdlemk6 31319  cdlemk6u 31344  cdlemk7 31330  cdlemk7u-2N 31370  cdlemk7u 31352  cdlemk8 31320  cdlemk9 31321  cdlemk9bN 31322  cdlemki 31323  cdlemkid 31418  cdlemkj-2N 31364  cdlemkj 31345  cdlemksat 31328  cdlemksel 31327  cdlemksv 31326  cdlemksv2 31329  cdlemkuat 31348  cdlemkuel-2N 31366  cdlemkuel-3 31380  cdlemkuel 31347  cdlemkuv-2N 31365  cdlemkuv2-2 31367  cdlemkuv2-3N 31381  cdlemkuv2 31349  cdlemkuvN 31346  cdlemkvcl 31324  cdlemky 31408  cdlemkyyN 31444  tendoex 31457
[Crawley] p. 120Remarkdva1dim 31467
[Crawley] p. 120Lemma Lcdleml1N 31458  cdleml2N 31459  cdleml3N 31460  cdleml4N 31461  cdleml5N 31462  cdleml6 31463  cdleml7 31464  cdleml8 31465  cdleml9 31466  dia1dim 31544
[Crawley] p. 120Lemma Mdia11N 31531  diaf11N 31532  dialss 31529  diaord 31530  dibf11N 31644  djajN 31620
[Crawley] p. 120Definition of isomorphism mapdiaval 31515
[Crawley] p. 121Lemma Mcdlemm10N 31601  dia2dimlem1 31547  dia2dimlem2 31548  dia2dimlem3 31549  dia2dimlem4 31550  dia2dimlem5 31551  diaf1oN 31613  diarnN 31612  dvheveccl 31595  dvhopN 31599
[Crawley] p. 121Lemma Ncdlemn 31695  cdlemn10 31689  cdlemn11 31694  cdlemn11a 31690  cdlemn11b 31691  cdlemn11c 31692  cdlemn11pre 31693  cdlemn2 31678  cdlemn2a 31679  cdlemn3 31680  cdlemn4 31681  cdlemn4a 31682  cdlemn5 31684  cdlemn5pre 31683  cdlemn6 31685  cdlemn7 31686  cdlemn8 31687  cdlemn9 31688  diclspsn 31677
[Crawley] p. 121Definition of phi(q)df-dic 31656
[Crawley] p. 122Lemma Ndih11 31748  dihf11 31750  dihjust 31700  dihjustlem 31699  dihord 31747  dihord1 31701  dihord10 31706  dihord11b 31705  dihord11c 31707  dihord2 31710  dihord2a 31702  dihord2b 31703  dihord2cN 31704  dihord2pre 31708  dihord2pre2 31709  dihordlem6 31696  dihordlem7 31697  dihordlem7b 31698
[Crawley] p. 122Definition of isomorphism mapdihffval 31713  dihfval 31714  dihval 31715
[Eisenberg] p. 67Definition 5.3df-dif 3283
[Eisenberg] p. 82Definition 6.3dfom3 7558
[Eisenberg] p. 125Definition 8.21df-map 6979
[Eisenberg] p. 216Example 13.2(4)omenps 7565
[Eisenberg] p. 310Theorem 19.8cardprc 7823
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8386
[Enderton] p. 18Axiom of Empty Setaxnul 4297
[Enderton] p. 19Definitiondf-tp 3782
[Enderton] p. 26Exercise 5unissb 4005
[Enderton] p. 26Exercise 10pwel 4375
[Enderton] p. 28Exercise 7(b)pwun 4451
[Enderton] p. 30Theorem "Distributive laws"iinin1 4122  iinin2 4121  iinun2 4117  iunin1 4116  iunin2 4115
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4120  iundif2 4118
[Enderton] p. 32Exercise 20unineq 3551
[Enderton] p. 33Exercise 23iinuni 4134
[Enderton] p. 33Exercise 25iununi 4135
[Enderton] p. 33Exercise 24(a)iinpw 4139
[Enderton] p. 33Exercise 24(b)iunpw 4718  iunpwss 4140
[Enderton] p. 36Definitionopthwiener 4418
[Enderton] p. 38Exercise 6(a)unipw 4374
[Enderton] p. 38Exercise 6(b)pwuni 4355
[Enderton] p. 41Lemma 3Dopeluu 4674  rnex 5092  rnexg 5090
[Enderton] p. 41Exercise 8dmuni 5038  rnuni 5242
[Enderton] p. 42Definition of a functiondffun7 5438  dffun8 5439
[Enderton] p. 43Definition of function valuefunfv2 5750
[Enderton] p. 43Definition of single-rootedfuncnv 5470
[Enderton] p. 44Definition (d)dfima2 5164  dfima3 5165
[Enderton] p. 47Theorem 3Hfvco2 5757
[Enderton] p. 49Axiom of Choice (first form)ac7 8309  ac7g 8310  df-ac 7953  dfac2 7967  dfac2a 7966  dfac3 7958  dfac7 7968
[Enderton] p. 50Theorem 3K(a)imauni 5952
[Enderton] p. 52Definitiondf-map 6979
[Enderton] p. 53Exercise 21coass 5347
[Enderton] p. 53Exercise 27dmco 5337
[Enderton] p. 53Exercise 14(a)funin 5479
[Enderton] p. 53Exercise 22(a)imass2 5199
[Enderton] p. 54Remarkixpf 7043  ixpssmap 7055
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7023
[Enderton] p. 55Axiom of Choice (second form)ac9 8319  ac9s 8329
[Enderton] p. 56Theorem 3Merref 6884
[Enderton] p. 57Lemma 3Nerthi 6910
[Enderton] p. 57Definitiondf-ec 6866
[Enderton] p. 58Definitiondf-qs 6870
[Enderton] p. 60Theorem 3Qth3q 6972  th3qcor 6971  th3qlem1 6969  th3qlem2 6970
[Enderton] p. 61Exercise 35df-ec 6866
[Enderton] p. 65Exercise 56(a)dmun 5035
[Enderton] p. 68Definition of successordf-suc 4547
[Enderton] p. 71Definitiondf-tr 4263  dftr4 4267
[Enderton] p. 72Theorem 4Eunisuc 4617
[Enderton] p. 73Exercise 6unisuc 4617
[Enderton] p. 73Exercise 5(a)truni 4276
[Enderton] p. 73Exercise 5(b)trint 4277  trintALT 28702
[Enderton] p. 79Theorem 4I(A1)nna0 6806
[Enderton] p. 79Theorem 4I(A2)nnasuc 6808  onasuc 6731
[Enderton] p. 79Definition of operation valuedf-ov 6043
[Enderton] p. 80Theorem 4J(A1)nnm0 6807
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6809  onmsuc 6732
[Enderton] p. 81Theorem 4K(1)nnaass 6824
[Enderton] p. 81Theorem 4K(2)nna0r 6811  nnacom 6819
[Enderton] p. 81Theorem 4K(3)nndi 6825
[Enderton] p. 81Theorem 4K(4)nnmass 6826
[Enderton] p. 81Theorem 4K(5)nnmcom 6828
[Enderton] p. 82Exercise 16nnm0r 6812  nnmsucr 6827
[Enderton] p. 88Exercise 23nnaordex 6840
[Enderton] p. 129Definitiondf-en 7069
[Enderton] p. 132Theorem 6B(b)canth 6498
[Enderton] p. 133Exercise 1xpomen 7853
[Enderton] p. 133Exercise 2qnnen 12768
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7250
[Enderton] p. 135Corollary 6Cphp3 7252
[Enderton] p. 136Corollary 6Enneneq 7249
[Enderton] p. 136Corollary 6D(a)pssinf 7278
[Enderton] p. 136Corollary 6D(b)ominf 7280
[Enderton] p. 137Lemma 6Fpssnn 7286
[Enderton] p. 138Corollary 6Gssfi 7288
[Enderton] p. 139Theorem 6H(c)mapen 7230
[Enderton] p. 142Theorem 6I(3)xpcdaen 8019
[Enderton] p. 142Theorem 6I(4)mapcdaen 8020
[Enderton] p. 143Theorem 6Jcda0en 8015  cda1en 8011
[Enderton] p. 144Exercise 13iunfi 7353  unifi 7354  unifi2 7355
[Enderton] p. 144Corollary 6Kundif2 3664  unfi 7333  unfi2 7335
[Enderton] p. 145Figure 38ffoss 5666
[Enderton] p. 145Definitiondf-dom 7070
[Enderton] p. 146Example 1domen 7080  domeng 7081
[Enderton] p. 146Example 3nndomo 7259  nnsdom 7564  nnsdomg 7325
[Enderton] p. 149Theorem 6L(a)cdadom2 8023
[Enderton] p. 149Theorem 6L(c)mapdom1 7231  xpdom1 7166  xpdom1g 7164  xpdom2g 7163
[Enderton] p. 149Theorem 6L(d)mapdom2 7237
[Enderton] p. 151Theorem 6Mzorn 8343  zorng 8340
[Enderton] p. 151Theorem 6M(4)ac8 8328  dfac5 7965
[Enderton] p. 159Theorem 6Qunictb 8406
[Enderton] p. 164Exampleinfdif 8045
[Enderton] p. 168Definitiondf-po 4463
[Enderton] p. 192Theorem 7M(a)oneli 4648
[Enderton] p. 192Theorem 7M(b)ontr1 4587
[Enderton] p. 192Theorem 7M(c)onirri 4647
[Enderton] p. 193Corollary 7N(b)0elon 4594
[Enderton] p. 193Corollary 7N(c)onsuci 4777
[Enderton] p. 193Corollary 7N(d)ssonunii 4727
[Enderton] p. 194Remarkonprc 4724
[Enderton] p. 194Exercise 16suc11 4644
[Enderton] p. 197Definitiondf-card 7782
[Enderton] p. 197Theorem 7Pcarden 8382
[Enderton] p. 200Exercise 25tfis 4793
[Enderton] p. 202Lemma 7Tr1tr 7658
[Enderton] p. 202Definitiondf-r1 7646
[Enderton] p. 202Theorem 7Qr1val1 7668
[Enderton] p. 204Theorem 7V(b)rankval4 7749
[Enderton] p. 206Theorem 7X(b)en2lp 7527
[Enderton] p. 207Exercise 30rankpr 7739  rankprb 7733  rankpw 7725  rankpwi 7705  rankuniss 7748
[Enderton] p. 207Exercise 34opthreg 7529
[Enderton] p. 208Exercise 35suc11reg 7530
[Enderton] p. 212Definition of alephalephval3 7947
[Enderton] p. 213Theorem 8A(a)alephord2 7913
[Enderton] p. 213Theorem 8A(b)cardalephex 7927
[Enderton] p. 218Theorem Schema 8Eonfununi 6562
[Enderton] p. 222Definition of kardkarden 7775  kardex 7774
[Enderton] p. 238Theorem 8Roeoa 6799
[Enderton] p. 238Theorem 8Soeoe 6801
[Enderton] p. 240Exercise 25oarec 6764
[Enderton] p. 257Definition of cofinalitycflm 8086
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13822
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13768
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14558  mrieqv2d 13819  mrieqvd 13818
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13823
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13828  mreexexlem2d 13825
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14564  mreexfidimd 13830
[Fremlin5] p. 193Proposition 563Gbnulmbl2 19384
[Fremlin5] p. 213Lemma 565Cauniioovol 19424
[Fremlin5] p. 214Lemma 565Cauniioombl 19434
[FreydScedrov] p. 283Axiom of Infinityax-inf 7549  inf1 7533  inf2 7534
[Gleason] p. 117Proposition 9-2.1df-enq 8744  enqer 8754
[Gleason] p. 117Proposition 9-2.2df-1nq 8749  df-nq 8745
[Gleason] p. 117Proposition 9-2.3df-plpq 8741  df-plq 8747
[Gleason] p. 119Proposition 9-2.4caovmo 6243  df-mpq 8742  df-mq 8748
[Gleason] p. 119Proposition 9-2.5df-rq 8750
[Gleason] p. 119Proposition 9-2.6ltexnq 8808
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8809  ltbtwnnq 8811
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8804
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8805
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8812
[Gleason] p. 121Definition 9-3.1df-np 8814
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8826
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8828
[Gleason] p. 122Definitiondf-1p 8815
[Gleason] p. 122Remark (1)prub 8827
[Gleason] p. 122Lemma 9-3.4prlem934 8866
[Gleason] p. 122Proposition 9-3.2df-ltp 8818
[Gleason] p. 122Proposition 9-3.3ltsopr 8865  psslinpr 8864  supexpr 8887  suplem1pr 8885  suplem2pr 8886
[Gleason] p. 123Proposition 9-3.5addclpr 8851  addclprlem1 8849  addclprlem2 8850  df-plp 8816
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8855
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8854
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8867
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8876  ltexprlem1 8869  ltexprlem2 8870  ltexprlem3 8871  ltexprlem4 8872  ltexprlem5 8873  ltexprlem6 8874  ltexprlem7 8875
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8878  ltaprlem 8877
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8879
[Gleason] p. 124Lemma 9-3.6prlem936 8880
[Gleason] p. 124Proposition 9-3.7df-mp 8817  mulclpr 8853  mulclprlem 8852  reclem2pr 8881
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8862
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8857
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8856
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8861
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8884  reclem3pr 8882  reclem4pr 8883
[Gleason] p. 126Proposition 9-4.1df-enr 8890  df-mpr 8889  df-plpr 8888  enrer 8899
[Gleason] p. 126Proposition 9-4.2df-0r 8895  df-1r 8896  df-nr 8891
[Gleason] p. 126Proposition 9-4.3df-mr 8893  df-plr 8892  negexsr 8933  recexsr 8938  recexsrlem 8934
[Gleason] p. 127Proposition 9-4.4df-ltr 8894
[Gleason] p. 130Proposition 10-1.3creui 9951  creur 9950  cru 9948
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 9019  axcnre 8995
[Gleason] p. 132Definition 10-3.1crim 11875  crimd 11992  crimi 11953  crre 11874  crred 11991  crrei 11952
[Gleason] p. 132Definition 10-3.2remim 11877  remimd 11958
[Gleason] p. 133Definition 10.36absval2 12044  absval2d 12202  absval2i 12155
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11901  cjaddd 11980  cjaddi 11948
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11902  cjmuld 11981  cjmuli 11949
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11900  cjcjd 11959  cjcji 11931
[Gleason] p. 133Proposition 10-3.4(f)cjre 11899  cjreb 11883  cjrebd 11962  cjrebi 11934  cjred 11986  rere 11882  rereb 11880  rerebd 11961  rerebi 11933  rered 11984
[Gleason] p. 133Proposition 10-3.4(h)addcj 11908  addcjd 11972  addcji 11943
[Gleason] p. 133Proposition 10-3.7(a)absval 11998
[Gleason] p. 133Proposition 10-3.7(b)abscj 12039  abscjd 12207  abscji 12159
[Gleason] p. 133Proposition 10-3.7(c)abs00 12049  abs00d 12203  abs00i 12156  absne0d 12204
[Gleason] p. 133Proposition 10-3.7(d)releabs 12080  releabsd 12208  releabsi 12160
[Gleason] p. 133Proposition 10-3.7(f)absmul 12054  absmuld 12211  absmuli 12162
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 12042  sqabsaddi 12163
[Gleason] p. 133Proposition 10-3.7(h)abstri 12089  abstrid 12213  abstrii 12166
[Gleason] p. 134Definition 10-4.1df-exp 11338  exp0 11341  expp1 11343  expp1d 11479
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20523  cxpaddd 20561  expadd 11377  expaddd 11480  expaddz 11379
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20532  cxpmuld 20578  expmul 11380  expmuld 11481  expmulz 11381
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20529  mulcxpd 20572  mulexp 11374  mulexpd 11493  mulexpz 11375
[Gleason] p. 140Exercise 1znnen 12767
[Gleason] p. 141Definition 11-2.1fzval 11001
[Gleason] p. 168Proposition 12-2.1(a)climadd 12380  rlimadd 12391  rlimdiv 12394
[Gleason] p. 168Proposition 12-2.1(b)climsub 12382  rlimsub 12392
[Gleason] p. 168Proposition 12-2.1(c)climmul 12381  rlimmul 12393
[Gleason] p. 171Corollary 12-2.2climmulc2 12385
[Gleason] p. 172Corollary 12-2.5climrecl 12332
[Gleason] p. 172Proposition 12-2.4(c)climabs 12352  climcj 12353  climim 12355  climre 12354  rlimabs 12357  rlimcj 12358  rlimim 12360  rlimre 12359
[Gleason] p. 173Definition 12-3.1df-ltxr 9081  df-xr 9080  ltxr 10671
[Gleason] p. 175Definition 12-4.1df-limsup 12220  limsupval 12223
[Gleason] p. 180Theorem 12-5.1climsup 12418
[Gleason] p. 180Theorem 12-5.3caucvg 12427  caucvgb 12428  caucvgr 12424  climcau 12419
[Gleason] p. 182Exercise 3cvgcmp 12550
[Gleason] p. 182Exercise 4cvgrat 12615
[Gleason] p. 195Theorem 13-2.12abs1m 12094
[Gleason] p. 217Lemma 13-4.1btwnzge0 11185
[Gleason] p. 223Definition 14-1.1df-met 16651
[Gleason] p. 223Definition 14-1.1(a)met0 18326  xmet0 18325
[Gleason] p. 223Definition 14-1.1(b)metgt0 18342
[Gleason] p. 223Definition 14-1.1(c)metsym 18333
[Gleason] p. 223Definition 14-1.1(d)mettri 18335  mstri 18452  xmettri 18334  xmstri 18451
[Gleason] p. 225Definition 14-1.5xpsmet 18365
[Gleason] p. 230Proposition 14-2.6txlm 17633
[Gleason] p. 240Theorem 14-4.3metcnp4 19215
[Gleason] p. 240Proposition 14-4.2metcnp3 18523
[Gleason] p. 243Proposition 14-4.16addcn 18848  addcn2 12342  mulcn 18850  mulcn2 12344  subcn 18849  subcn2 12343
[Gleason] p. 295Remarkbcval3 11552  bcval4 11553
[Gleason] p. 295Equation 2bcpasc 11567
[Gleason] p. 295Definition of binomial coefficientbcval 11550  df-bc 11549
[Gleason] p. 296Remarkbcn0 11556  bcnn 11558
[Gleason] p. 296Theorem 15-2.8binom 12564
[Gleason] p. 308Equation 2ef0 12648
[Gleason] p. 308Equation 3efcj 12649
[Gleason] p. 309Corollary 15-4.3efne0 12653
[Gleason] p. 309Corollary 15-4.4efexp 12657
[Gleason] p. 310Equation 14sinadd 12720
[Gleason] p. 310Equation 15cosadd 12721
[Gleason] p. 311Equation 17sincossq 12732
[Gleason] p. 311Equation 18cosbnd 12737  sinbnd 12736
[Gleason] p. 311Lemma 15-4.7sqeqor 11450  sqeqori 11448
[Gleason] p. 311Definition of pidf-pi 12630
[Godowski] p. 730Equation SFgoeqi 23729
[GodowskiGreechie] p. 249Equation IV3oai 23123
[Gratzer] p. 23Section 0.6df-mre 13766
[Gratzer] p. 27Section 0.6df-mri 13768
[Halmos] p. 31Theorem 17.3riesz1 23521  riesz2 23522
[Halmos] p. 41Definition of Hermitianhmopadj2 23397
[Halmos] p. 42Definition of projector orderingpjordi 23629
[Halmos] p. 43Theorem 26.1elpjhmop 23641  elpjidm 23640  pjnmopi 23604
[Halmos] p. 44Remarkpjinormi 23142  pjinormii 23131
[Halmos] p. 44Theorem 26.2elpjch 23645  pjrn 23162  pjrni 23157  pjvec 23151
[Halmos] p. 44Theorem 26.3pjnorm2 23182
[Halmos] p. 44Theorem 26.4hmopidmpj 23610  hmopidmpji 23608
[Halmos] p. 45Theorem 27.1pjinvari 23647
[Halmos] p. 45Theorem 27.3pjoci 23636  pjocvec 23152
[Halmos] p. 45Theorem 27.4pjorthcoi 23625
[Halmos] p. 48Theorem 29.2pjssposi 23628
[Halmos] p. 48Theorem 29.3pjssdif1i 23631  pjssdif2i 23630
[Halmos] p. 50Definition of spectrumdf-spec 23311
[Hamilton] p. 28Definition 2.1ax-1 5
[Hamilton] p. 31Example 2.7(a)id1 21
[Hamilton] p. 73Rule 1ax-mp 8
[Hamilton] p. 74Rule 2ax-gen 1552
[Hatcher] p. 25Definitiondf-phtpc 18970  df-phtpy 18949
[Hatcher] p. 26Definitiondf-pco 18983  df-pi1 18986
[Hatcher] p. 26Proposition 1.2phtpcer 18973
[Hatcher] p. 26Proposition 1.3pi1grp 19028
[Herstein] p. 54Exercise 28df-grpo 21732
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14776  grpoideu 21750  mndideu 14653
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14794  grpoinveu 21763
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14813  grpo2inv 21780
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14822  grpoinvop 21782
[Herstein] p. 57Exercise 1isgrp2d 21776  isgrp2i 21777
[Hitchcock] p. 5Rule A3mpto1 1539
[Hitchcock] p. 5Rule A4mpto2 1540
[Hitchcock] p. 5Rule A5mtp-xor 1542
[Holland] p. 1519Theorem 2sumdmdi 23876
[Holland] p. 1520Lemma 5cdj1i 23889  cdj3i 23897  cdj3lem1 23890  cdjreui 23888
[Holland] p. 1524Lemma 7mddmdin0i 23887
[Holland95] p. 13Theorem 3.6hlathil 32447
[Holland95] p. 14Line 15hgmapvs 32377
[Holland95] p. 14Line 16hdmaplkr 32399
[Holland95] p. 14Line 17hdmapellkr 32400
[Holland95] p. 14Line 19hdmapglnm2 32397
[Holland95] p. 14Line 20hdmapip0com 32403
[Holland95] p. 14Theorem 3.6hdmapevec2 32322
[Holland95] p. 14Lines 24 and 25hdmapoc 32417
[Holland95] p. 204Definition of involutiondf-srng 15889
[Holland95] p. 212Definition of subspacedf-psubsp 29985
[Holland95] p. 214Lemma 3.3lclkrlem2v 32011
[Holland95] p. 214Definition 3.2df-lpolN 31964
[Holland95] p. 214Definition of nonsingularpnonsingN 30415
[Holland95] p. 215Lemma 3.3(1)dihoml4 31860  poml4N 30435
[Holland95] p. 215Lemma 3.3(2)dochexmid 31951  pexmidALTN 30460  pexmidN 30451
[Holland95] p. 218Theorem 3.6lclkr 32016
[Holland95] p. 218Definition of dual vector spacedf-ldual 29607  ldualset 29608
[Holland95] p. 222Item 1df-lines 29983  df-pointsN 29984
[Holland95] p. 222Item 2df-polarityN 30385
[Holland95] p. 223Remarkispsubcl2N 30429  omllaw4 29729  pol1N 30392  polcon3N 30399
[Holland95] p. 223Definitiondf-psubclN 30417
[Holland95] p. 223Equation for polaritypolval2N 30388
[Hughes] p. 44Equation 1.21bax-his3 22539
[Hughes] p. 47Definition of projection operatordfpjop 23638
[Hughes] p. 49Equation 1.30eighmre 23419  eigre 23291  eigrei 23290
[Hughes] p. 49Equation 1.31eighmorth 23420  eigorth 23294  eigorthi 23293
[Hughes] p. 137Remark (ii)eigposi 23292
[Huneke] p. 1Theoremfrgrancvvdeq 28145  frgrancvvdgeq 28146
[Huneke] p. 1Lemma A for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemA 28140
[Huneke] p. 1Lemma B for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemB 28141
[Huneke] p. 1Lemma C for ~ frgrancvvdeq . This corresponds to the following observationfrgrancvvdeqlemC 28142
[Huneke] p. 2Theoremfrghash2spot 28166  frgraregorufr 28156  frgraregorufr0 28155  frgrawopreg1 28153  frgrawopreg2 28154  frgregordn0 28173  usgreghash2spot 28172  usgreghash2spotv 28169
[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 28150
[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 28151
[Indrzejczak] p. 33Definition ` `Enatded 21664  natded 21664
[Indrzejczak] p. 33Definition ` `Inatded 21664
[Indrzejczak] p. 34Definition ` `Enatded 21664  natded 21664
[Indrzejczak] p. 34Definition ` `Inatded 21664
[Jech] p. 4Definition of classcv 1648  cvjust 2399
[Jech] p. 42Lemma 6.1alephexp1 8410
[Jech] p. 42Equation 6.1alephadd 8408  alephmul 8409
[Jech] p. 43Lemma 6.2infmap 8407  infmap2 8054
[Jech] p. 71Lemma 9.3jech9.3 7696
[Jech] p. 72Equation 9.3scott0 7766  scottex 7765
[Jech] p. 72Exercise 9.1rankval4 7749
[Jech] p. 72Scheme "Collection Principle"cp 7771
[Jech] p. 78Definition implied by the footnoteopthprc 4884
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26868
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26964
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26965
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26880
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26884
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26885  rmyp1 26886
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26887  rmym1 26888
[JonesMatijasevic] p. 695Equation 2.11rmx0 26878  rmx1 26879  rmxluc 26889
[JonesMatijasevic] p. 695Equation 2.12rmy0 26882  rmy1 26883  rmyluc 26890
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26892
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26893
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26915  jm2.17b 26916  jm2.17c 26917
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26954
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26958
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26949
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26918  jm2.24nn 26914
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26963
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26969  rmygeid 26919
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26981
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1662
[KalishMontague] p. 85Lemma 2equid 1684
[KalishMontague] p. 85Lemma 3equcomi 1687
[KalishMontague] p. 86Lemma 7cbvalivw 1682  cbvaliw 1681
[KalishMontague] p. 87Lemma 8spimvw 1677  spimw 1676
[KalishMontague] p. 87Lemma 9spfw 1699  spw 1702
[Kalmbach] p. 14Definition of latticechabs1 22971  chabs1i 22973  chabs2 22972  chabs2i 22974  chjass 22988  chjassi 22941  latabs1 14471  latabs2 14472
[Kalmbach] p. 15Definition of atomdf-at 23794  ela 23795
[Kalmbach] p. 15Definition of coverscvbr2 23739  cvrval2 29757
[Kalmbach] p. 16Definitiondf-ol 29661  df-oml 29662
[Kalmbach] p. 20Definition of commutescmbr 23039  cmbri 23045  cmtvalN 29694  df-cm 23038  df-cmtN 29660
[Kalmbach] p. 22Remarkomllaw5N 29730  pjoml5 23068  pjoml5i 23043
[Kalmbach] p. 22Definitionpjoml2 23066  pjoml2i 23040
[Kalmbach] p. 22Theorem 2(v)cmcm 23069  cmcmi 23047  cmcmii 23052  cmtcomN 29732
[Kalmbach] p. 22Theorem 2(ii)omllaw3 29728  omlsi 22859  pjoml 22891  pjomli 22890
[Kalmbach] p. 22Definition of OML lawomllaw2N 29727
[Kalmbach] p. 23Remarkcmbr2i 23051  cmcm3 23070  cmcm3i 23049  cmcm3ii 23054  cmcm4i 23050  cmt3N 29734  cmt4N 29735  cmtbr2N 29736
[Kalmbach] p. 23Lemma 3cmbr3 23063  cmbr3i 23055  cmtbr3N 29737
[Kalmbach] p. 25Theorem 5fh1 23073  fh1i 23076  fh2 23074  fh2i 23077  omlfh1N 29741
[Kalmbach] p. 65Remarkchjatom 23813  chslej 22953  chsleji 22913  shslej 22835  shsleji 22825
[Kalmbach] p. 65Proposition 1chocin 22950  chocini 22909  chsupcl 22795  chsupval2 22865  h0elch 22710  helch 22699  hsupval2 22864  ocin 22751  ococss 22748  shococss 22749
[Kalmbach] p. 65Definition of subspace sumshsval 22767
[Kalmbach] p. 66Remarkdf-pjh 22850  pjssmi 23621  pjssmii 23136
[Kalmbach] p. 67Lemma 3osum 23100  osumi 23097
[Kalmbach] p. 67Lemma 4pjci 23656
[Kalmbach] p. 103Exercise 6atmd2 23856
[Kalmbach] p. 103Exercise 12mdsl0 23766
[Kalmbach] p. 140Remarkhatomic 23816  hatomici 23815  hatomistici 23818
[Kalmbach] p. 140Proposition 1atlatmstc 29802
[Kalmbach] p. 140Proposition 1(i)atexch 23837  lsatexch 29526
[Kalmbach] p. 140Proposition 1(ii)chcv1 23811  cvlcvr1 29822  cvr1 29892
[Kalmbach] p. 140Proposition 1(iii)cvexch 23830  cvexchi 23825  cvrexch 29902
[Kalmbach] p. 149Remark 2chrelati 23820  hlrelat 29884  hlrelat5N 29883  lrelat 29497
[Kalmbach] p. 153Exercise 5lsmcv 16168  lsmsatcv 29493  spansncv 23108  spansncvi 23107
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29512  spansncv2 23749
[Kalmbach] p. 266Definitiondf-st 23667
[Kalmbach2] p. 8Definition of adjointdf-adjh 23305
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8477  fpwwe2 8474
[KanamoriPincus] p. 416Corollary 1.3canth4 8478
[KanamoriPincus] p. 417Corollary 1.6canthp1 8485
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8480
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8482
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8495
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8499  gchxpidm 8500
[KanamoriPincus] p. 419Theorem 2.1gchacg 8503  gchhar 8502
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 8052  unxpwdom 7513
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8505
[Kreyszig] p. 3Property M1metcl 18315  xmetcl 18314
[Kreyszig] p. 4Property M2meteq0 18322
[Kreyszig] p. 8Definition 1.1-8dscmet 18573
[Kreyszig] p. 12Equation 5conjmul 9687  muleqadd 9622
[Kreyszig] p. 18Definition 1.3-2mopnval 18421
[Kreyszig] p. 19Remarkmopntopon 18422
[Kreyszig] p. 19Theorem T1mopn0 18481  mopnm 18427
[Kreyszig] p. 19Theorem T2unimopn 18479
[Kreyszig] p. 19Definition of neighborhoodneibl 18484
[Kreyszig] p. 20Definition 1.3-3metcnp2 18525
[Kreyszig] p. 25Definition 1.4-1lmbr 17276  lmmbr 19164  lmmbr2 19165
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17398
[Kreyszig] p. 28Theorem 1.4-5lmcau 19218
[Kreyszig] p. 28Definition 1.4-3iscau 19182  iscmet2 19200
[Kreyszig] p. 30Theorem 1.4-7cmetss 19220
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17477  metelcls 19210
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 19211  metcld2 19212
[Kreyszig] p. 51Equation 2clmvneg1 19069  lmodvneg1 15942  nvinv 22073  vcm 22003
[Kreyszig] p. 51Equation 1aclm0vs 19068  lmod0vs 15938  vc0 22001
[Kreyszig] p. 51Equation 1blmodvs0 15939  vcz 22002
[Kreyszig] p. 58Definition 2.2-1imsmet 22136
[Kreyszig] p. 59Equation 1imsdval 22131  imsdval2 22132
[Kreyszig] p. 63Problem 1nvnd 22133
[Kreyszig] p. 64Problem 2nvge0 22116  nvz 22111
[Kreyszig] p. 64Problem 3nvabs 22115
[Kreyszig] p. 91Definition 2.7-1isblo3i 22255
[Kreyszig] p. 92Equation 2df-nmoo 22199
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 22261  blocni 22259
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 22260
[Kreyszig] p. 129Definition 3.1-1cphipeq0 19119  ipeq0 16824  ipz 22171
[Kreyszig] p. 135Problem 2pythi 22304
[Kreyszig] p. 137Lemma 3-2.1(a)sii 22308
[Kreyszig] p. 144Equation 4supcvg 12590
[Kreyszig] p. 144Theorem 3.3-1minvec 19290  minveco 22339
[Kreyszig] p. 196Definition 3.9-1df-aj 22204
[Kreyszig] p. 247Theorem 4.7-2bcth 19235
[Kreyszig] p. 249Theorem 4.7-3ubth 22328
[Kreyszig] p. 470Definition of positive operator orderingleop 23579  leopg 23578
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 23597
[Kreyszig] p. 525Theorem 10.1-1htth 22374
[Kunen] p. 10Axiom 0a9e 1948  axnul 4297
[Kunen] p. 11Axiom 3axnul 4297
[Kunen] p. 12Axiom 6zfrep6 5927
[Kunen] p. 24Definition 10.24mapval 6989  mapvalg 6987
[Kunen] p. 30Lemma 10.20fodom 8358
[Kunen] p. 31Definition 10.24mapex 6983
[Kunen] p. 95Definition 2.1df-r1 7646
[Kunen] p. 97Lemma 2.10r1elss 7688  r1elssi 7687
[Kunen] p. 107Exercise 4rankop 7740  rankopb 7734  rankuni 7745  rankxplim 7759  rankxpsuc 7762
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4063
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27419
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27414
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27420
[LeBlanc] p. 277Rule R2axnul 4297
[Levy] p. 338Axiomdf-clab 2391  df-clel 2400  df-cleq 2397
[Levy58] p. 2Definition Iisfin1-3 8222
[Levy58] p. 2Definition IIdf-fin2 8122
[Levy58] p. 2Definition Iadf-fin1a 8121
[Levy58] p. 2Definition IIIdf-fin3 8124
[Levy58] p. 3Definition Vdf-fin5 8125
[Levy58] p. 3Definition IVdf-fin4 8123
[Levy58] p. 4Definition VIdf-fin6 8126
[Levy58] p. 4Definition VIIdf-fin7 8127
[Levy58], p. 3Theorem 1fin1a2 8251
[Lopez-Astorga] p. 12Rule 1mpto1 1539
[Lopez-Astorga] p. 12Rule 2mpto2 1540
[Lopez-Astorga] p. 12Rule 3mtp-xor 1542
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 23864
[Maeda] p. 168Lemma 5mdsym 23868  mdsymi 23867
[Maeda] p. 168Lemma 4(i)mdsymlem4 23862  mdsymlem6 23864  mdsymlem7 23865
[Maeda] p. 168Lemma 4(ii)mdsymlem8 23866
[MaedaMaeda] p. 1Remarkssdmd1 23769  ssdmd2 23770  ssmd1 23767  ssmd2 23768
[MaedaMaeda] p. 1Lemma 1.2mddmd2 23765
[MaedaMaeda] p. 1Definition 1.1df-dmd 23737  df-md 23736  mdbr 23750
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 23787  mdslj1i 23775  mdslj2i 23776  mdslle1i 23773  mdslle2i 23774  mdslmd1i 23785  mdslmd2i 23786
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 23777  mdsl2bi 23779  mdsl2i 23778
[MaedaMaeda] p. 2Lemma 1.6mdexchi 23791
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 23788
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 23789
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 23766
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 23771  mdsl3 23772
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 23790
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23885
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 29804  hlrelat1 29882
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29522
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 23792  cvmdi 23780  cvnbtwn4 23745  cvrnbtwn4 29762
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 23793
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 29823  cvp 23831  cvrp 29898  lcvp 29523
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 23855
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 23854
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 29816  hlexch4N 29874
[MaedaMaeda] p. 34Exercise 7.1atabsi 23857
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 29925
[MaedaMaeda] p. 61Definition 15.10psubN 30231  atpsubN 30235  df-pointsN 29984  pointpsubN 30233
[MaedaMaeda] p. 62Theorem 15.5df-pmap 29986  pmap11 30244  pmaple 30243  pmapsub 30250  pmapval 30239
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 30247  pmap1N 30249
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 30252  pmapglb2N 30253  pmapglb2xN 30254  pmapglbx 30251
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 30334
[MaedaMaeda] p. 67Postulate PS1ps-1 29959
[MaedaMaeda] p. 68Lemma 16.2df-padd 30278  paddclN 30324  paddidm 30323
[MaedaMaeda] p. 68Condition PS2ps-2 29960
[MaedaMaeda] p. 68Equation 16.2.1paddass 30320
[MaedaMaeda] p. 69Lemma 16.4ps-1 29959
[MaedaMaeda] p. 69Theorem 16.4ps-2 29960
[MaedaMaeda] p. 70Theorem 16.9lsmmod 15262  lsmmod2 15263  lssats 29495  shatomici 23814  shatomistici 23817  shmodi 22845  shmodsi 22844
[MaedaMaeda] p. 130Remark 29.6dmdmd 23756  mdsymlem7 23865
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 23044
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22948
[MaedaMaeda] p. 139Remarksumdmdii 23871
[Margaris] p. 40Rule Cexlimiv 1641
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 7
[Margaris] p. 49Definitiondf-an 361  df-ex 1548  df-or 360  dfbi2 610
[Margaris] p. 51Theorem 1id1 21
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 28736
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 28737
[Margaris] p. 79Rule Cexinst01 28435  exinst11 28436
[Margaris] p. 89Theorem 19.219.2 1667  19.2g 1769  r19.2z 3677
[Margaris] p. 89Theorem 19.319.3 1787  19.3v 1673  rr19.3v 3037
[Margaris] p. 89Theorem 19.5alcom 1748
[Margaris] p. 89Theorem 19.6alex 1578
[Margaris] p. 89Theorem 19.7alnex 1549
[Margaris] p. 89Theorem 19.819.8a 1758
[Margaris] p. 89Theorem 19.919.9 1793  19.9h 1790  19.9v 1672  exlimd 1820  exlimdh 1822
[Margaris] p. 89Theorem 19.11excom 1752  excomim 1753
[Margaris] p. 89Theorem 19.1219.12 1865  r19.12 2779
[Margaris] p. 90Theorem 19.14exnal 1580
[Margaris] p. 90Theorem 19.152albi 27444  albi 1570  ralbi 2802
[Margaris] p. 90Theorem 19.1619.16 1879
[Margaris] p. 90Theorem 19.1719.17 1880
[Margaris] p. 90Theorem 19.182exbi 27446  exbi 1588
[Margaris] p. 90Theorem 19.1919.19 1881
[Margaris] p. 90Theorem 19.202alim 27443  alim 1564  alimd 1776  alimdh 1569  alimdv 1628  ralimdaa 2743  ralimdv 2745  ralimdva 2744  sbcimdv 3182
[Margaris] p. 90Theorem 19.2119.21-2 1883  19.21 1810  19.21bi 1770  19.21h 1811  19.21t 1809  19.21v 1909  19.21vv 27442  alrimd 1781  alrimdd 1780  alrimdh 1594  alrimdv 1640  alrimi 1777  alrimih 1571  alrimiv 1638  alrimivv 1639  r19.21 2752  r19.21be 2767  r19.21bi 2764  r19.21t 2751  r19.21v 2753  ralrimd 2754  ralrimdv 2755  ralrimdva 2756  ralrimdvv 2760  ralrimdvva 2761  ralrimi 2747  ralrimiv 2748  ralrimiva 2749  ralrimivv 2757  ralrimivva 2758  ralrimivvva 2759  ralrimivw 2750  rexlimi 2783
[Margaris] p. 90Theorem 19.222alimdv 1630  2exim 27445  2eximdv 1631  exim 1581  eximd 1782  eximdh 1595  eximdv 1629  rexim 2770  reximdai 2774  reximddv 23915  reximdv 2777  reximdv2 2775  reximdva 2778  reximdvai 2776  reximi2 2772
[Margaris] p. 90Theorem 19.2319.23 1815  19.23bi 1771  19.23h 1816  19.23t 1814  19.23v 1910  19.23vv 1911  exlimdv 1643  exlimdvv 1644  exlimexi 28319  exlimi 1817  exlimih 1818  exlimiv 1641  exlimivv 1642  r19.23 2781  r19.23v 2782  rexlimd 2787  rexlimdv 2789  rexlimdv3a 2792  rexlimdva 2790  rexlimdvaa 2791  rexlimdvv 2796  rexlimdvva 2797  rexlimdvw 2793  rexlimiv 2784  rexlimiva 2785  rexlimivv 2795
[Margaris] p. 90Theorem 19.2419.24 1670
[Margaris] p. 90Theorem 19.2519.25 1610
[Margaris] p. 90Theorem 19.2619.26-2 1601  19.26-3an 1602  19.26 1600  r19.26-2 2799  r19.26-3 2800  r19.26 2798  r19.26m 2801
[Margaris] p. 90Theorem 19.2719.27 1837  19.27v 1913  r19.27av 2804  r19.27z 3686  r19.27zv 3687
[Margaris] p. 90Theorem 19.2819.28 1838  19.28v 1914  19.28vv 27452  r19.28av 2805  r19.28z 3680  r19.28zv 3683  rr19.28v 3038
[Margaris] p. 90Theorem 19.2919.29 1603  19.29r 1604  19.29r2 1605  19.29x 1606  r19.29 2806  r19.29d2r 2811  r19.29r 2807
[Margaris] p. 90Theorem 19.3019.30 1611  r19.30 2813
[Margaris] p. 90Theorem 19.3119.31 1893  19.31vv 27450
[Margaris] p. 90Theorem 19.3219.32 1892  r19.32 27812  r19.32v 2814
[Margaris] p. 90Theorem 19.3319.33-2 27448  19.33 1614  19.33b 1615
[Margaris] p. 90Theorem 19.3419.34 1671
[Margaris] p. 90Theorem 19.3519.35 1607  19.35i 1608  19.35ri 1609  r19.35 2815
[Margaris] p. 90Theorem 19.3619.36 1888  19.36aiv 1916  19.36i 1889  19.36v 1915  19.36vv 27449  r19.36av 2816  r19.36zv 3688
[Margaris] p. 90Theorem 19.3719.37 1890  19.37aiv 1919  19.37v 1918  19.37vv 27451  r19.37 2817  r19.37av 2818  r19.37zv 3684
[Margaris] p. 90Theorem 19.3819.38 1808
[Margaris] p. 90Theorem 19.3919.39 1669
[Margaris] p. 90Theorem 19.4019.40-2 1617  19.40 1616  r19.40 2819
[Margaris] p. 90Theorem 19.4119.41 1896  19.41rg 28348  19.41v 1920  19.41vv 1921  19.41vvv 1922  19.41vvvv 1923  r19.41 2820  r19.41v 2821  r19.41vv 23923
[Margaris] p. 90Theorem 19.4219.42 1898  19.42v 1924  19.42vv 1926  19.42vvv 1927  r19.42v 2822
[Margaris] p. 90Theorem 19.4319.43 1612  r19.43 2823
[Margaris] p. 90Theorem 19.4419.44 1894  r19.44av 2824
[Margaris] p. 90Theorem 19.4519.45 1895  r19.45av 2825  r19.45zv 3685
[Margaris] p. 110Exercise 2(b)eu1 2275
[Mayet] p. 370Remarkjpi 23726  largei 23723  stri 23713
[Mayet3] p. 9Definition of CH-statesdf-hst 23668  ishst 23670
[Mayet3] p. 10Theoremhstrbi 23722  hstri 23721
[Mayet3] p. 1223Theorem 4.1mayete3i 23183
[Mayet3] p. 1240Theorem 7.1mayetes3i 23185
[MegPav2000] p. 2344Theorem 3.3stcltrthi 23734
[MegPav2000] p. 2345Definition 3.4-1chintcl 22787  chsupcl 22795
[MegPav2000] p. 2345Definition 3.4-2hatomic 23816
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 23810
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 23837
[MegPav2000] p. 2366Figure 7pl42N 30465
[MegPav2002] p. 362Lemma 2.2latj31 14483  latj32 14481  latjass 14479
[Megill] p. 444Axiom C5ax-17 1623  ax17o 2207
[Megill] p. 444Section 7conventions 21663
[Megill] p. 445Lemma L12aecom-o 2201  aecom 2002  ax-10 2190
[Megill] p. 446Lemma L17equtrr 1691
[Megill] p. 446Lemma L18ax9from9o 2198
[Megill] p. 446Lemma L19hbnae-o 2229  hbnae 2007
[Megill] p. 447Remark 9.1df-sb 1656  sbid 1943  sbidd-misc 28176  sbidd 28175
[Megill] p. 448Remark 9.6ax15 2070
[Megill] p. 448Scheme C4'ax-5o 2186
[Megill] p. 448Scheme C5'ax-4 2185  sp 1759
[Megill] p. 448Scheme C6'ax-7 1745
[Megill] p. 448Scheme C7'ax-6o 2187
[Megill] p. 448Scheme C8'ax-8 1683
[Megill] p. 448Scheme C9'ax-12o 2192
[Megill] p. 448Scheme C10'ax-9 1662  ax-9o 2188
[Megill] p. 448Scheme C11'ax-10o 2189
[Megill] p. 448Scheme C12'ax-13 1723
[Megill] p. 448Scheme C13'ax-14 1725
[Megill] p. 448Scheme C14'ax-15 2193
[Megill] p. 448Scheme C15'ax-11o 2191
[Megill] p. 448Scheme C16'ax-16 2194
[Megill] p. 448Theorem 9.4dral1-o 2204  dral1 2022  dral2-o 2231  dral2 2020  drex1 2024  drex2 2025  drsb1 2071  drsb2 2110
[Megill] p. 448Theorem 9.7conventions 21663
[Megill] p. 449Theorem 9.7sbcom2 2163  sbequ 2109  sbid2v 2173
[Megill] p. 450Example in Appendixhba1-o 2199  hba1 1800
[Mendelson] p. 35Axiom A3hirstL-ax3 27727
[Mendelson] p. 36Lemma 1.8id1 21
[Mendelson] p. 69Axiom 4rspsbc 3199  rspsbca 3200  stdpc4 2073
[Mendelson] p. 69Axiom 5ax-5o 2186  ra5 3205  stdpc5 1812
[Mendelson] p. 81Rule Cexlimiv 1641
[Mendelson] p. 95Axiom 6stdpc6 1695
[Mendelson] p. 95Axiom 7stdpc7 1938
[Mendelson] p. 225Axiom system NBGru 3120
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4418
[Mendelson] p. 231Exercise 4.10(k)inv1 3614
[Mendelson] p. 231Exercise 4.10(l)unv 3615
[Mendelson] p. 231Exercise 4.10(n)dfin3 3540
[Mendelson] p. 231Exercise 4.10(o)df-nul 3589
[Mendelson] p. 231Exercise 4.10(q)dfin4 3541
[Mendelson] p. 231Exercise 4.10(s)ddif 3439
[Mendelson] p. 231Definition of uniondfun3 3539
[Mendelson] p. 235Exercise 4.12(c)univ 4713
[Mendelson] p. 235Exercise 4.12(d)pwv 3974
[Mendelson] p. 235Exercise 4.12(j)pwin 4447
[Mendelson] p. 235Exercise 4.12(k)pwunss 4448
[Mendelson] p. 235Exercise 4.12(l)pwssun 4449
[Mendelson] p. 235Exercise 4.12(n)uniin 3995
[Mendelson] p. 235Exercise 4.12(p)reli 4961
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5349
[Mendelson] p. 244Proposition 4.8(g)epweon 4723
[Mendelson] p. 246Definition of successordf-suc 4547
[Mendelson] p. 250Exercise 4.36oelim2 6797
[Mendelson] p. 254Proposition 4.22(b)xpen 7229
[Mendelson] p. 254Proposition 4.22(c)xpsnen 7151  xpsneng 7152
[Mendelson] p. 254Proposition 4.22(d)xpcomen 7158  xpcomeng 7159
[Mendelson] p. 254Proposition 4.22(e)xpassen 7161
[Mendelson] p. 255Definitionbrsdom 7089
[Mendelson] p. 255Exercise 4.39endisj 7154
[Mendelson] p. 255Exercise 4.41mapprc 6981
[Mendelson] p. 255Exercise 4.43mapsnen 7143
[Mendelson] p. 255Exercise 4.45mapunen 7235
[Mendelson] p. 255Exercise 4.47xpmapen 7234
[Mendelson] p. 255Exercise 4.42(a)map0e 7010
[Mendelson] p. 255Exercise 4.42(b)map1 7144
[Mendelson] p. 257Proposition 4.24(a)undom 7155
[Mendelson] p. 258Exercise 4.56(b)cdaen 8009
[Mendelson] p. 258Exercise 4.56(c)cdaassen 8018  cdacomen 8017
[Mendelson] p. 258Exercise 4.56(f)cdadom1 8022
[Mendelson] p. 258Exercise 4.56(g)xp2cda 8016
[Mendelson] p. 258Definition of cardinal sumcdaval 8006  df-cda 8004
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6734
[Mendelson] p. 266Proposition 4.34(f)oaordex 6760
[Mendelson] p. 275Proposition 4.42(d)entri3 8390
[Mendelson] p. 281Definitiondf-r1 7646
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7695
[Mendelson] p. 287Axiom system MKru 3120
[MertziosUnger] p. 153Proposition 12pthfrgra 28115  2pthfrgrarn 28113  2pthfrgrarn2 28114  frconngra 28125  n4cyclfrgra 28122  vdgfrgragt2 28132  vdgn1frgrav2 28131  vdn1frgrav2 28130
[Mittelstaedt] p. 9Definitiondf-oc 22707
[Monk1] p. 22Remarkconventions 21663
[Monk1] p. 22Theorem 3.1conventions 21663
[Monk1] p. 26Theorem 2.8(vii)ssin 3523
[Monk1] p. 33Theorem 3.2(i)ssrel 4923
[Monk1] p. 33Theorem 3.2(ii)eqrel 4924
[Monk1] p. 34Definition 3.3df-opab 4227
[Monk1] p. 36Theorem 3.7(i)coi1 5344  coi2 5345
[Monk1] p. 36Theorem 3.8(v)dm0 5042  rn0 5086
[Monk1] p. 36Theorem 3.7(ii)cnvi 5235
[Monk1] p. 37Theorem 3.13(i)relxp 4942
[Monk1] p. 37Theorem 3.13(x)dmxp 5047  rnxp 5258
[Monk1] p. 37Theorem 3.13(ii)xp0 5250  xp0r 4915
[Monk1] p. 38Theorem 3.16(ii)ima0 5180
[Monk1] p. 38Theorem 3.16(viii)imai 5177
[Monk1] p. 39Theorem 3.17imaexg 5176
[Monk1] p. 39Theorem 3.16(xi)imassrn 5175
[Monk1] p. 41Theorem 4.3(i)fnopfv 5824  funfvop 5801
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5729
[Monk1] p. 42Theorem 4.4(iii)fvelima 5737
[Monk1] p. 43Theorem 4.6funun 5454
[Monk1] p. 43Theorem 4.8(iv)dff13 5963  dff13f 5965
[Monk1] p. 46Theorem 4.15(v)funex 5922  funrnex 5926
[Monk1] p. 50Definition 5.4fniunfv 5953
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5312
[Monk1] p. 52Theorem 5.11(viii)ssint 4026
[Monk1] p. 52Definition 5.13 (i)1stval2 6323  df-1st 6308
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6324  df-2nd 6309
[Monk1] p. 112Theorem 15.17(v)ranksn 7736  ranksnb 7709
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7737
[Monk1] p. 112Theorem 15.17(iii)rankun 7738  rankunb 7732
[Monk1] p. 113Theorem 15.18r1val3 7720
[Monk1] p. 113Definition 15.19df-r1 7646  r1val2 7719
[Monk1] p. 117Lemmazorn2 8342  zorn2g 8339
[Monk1] p. 133Theorem 18.11cardom 7829
[Monk1] p. 133Theorem 18.12canth3 8392
[Monk1] p. 133Theorem 18.14carduni 7824
[Monk2] p. 105Axiom C4ax-5 1563
[Monk2] p. 105Axiom C7ax-8 1683
[Monk2] p. 105Axiom C8ax-11 1757  ax-11o 2191
[Monk2] p. 105Axiom (C8)ax11v 2145
[Monk2] p. 108Lemma 5ax-5o 2186
[Monk2] p. 109Lemma 12ax-7 1745
[Monk2] p. 109Lemma 15equvin 2051  equvini 2040  eqvinop 4401
[Monk2] p. 113Axiom C5-1ax-17 1623  ax17o 2207
[Monk2] p. 113Axiom C5-2ax-6 1740
[Monk2] p. 113Axiom C5-3ax-7 1745
[Monk2] p. 114Lemma 21sp 1759
[Monk2] p. 114Lemma 22ax5o 1761  hba1-o 2199  hba1 1800
[Monk2] p. 114Lemma 23nfia1 1871
[Monk2] p. 114Lemma 24nfa2 1870  nfra2 2720
[Moore] p. 53Part Idf-mre 13766
[Munkres] p. 77Example 2distop 17015  indistop 17021  indistopon 17020
[Munkres] p. 77Example 3fctop 17023  fctop2 17024
[Munkres] p. 77Example 4cctop 17025
[Munkres] p. 78Definition of basisdf-bases 16920  isbasis3g 16969
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13622  tgval2 16976
[Munkres] p. 79Remarktgcl 16989
[Munkres] p. 80Lemma 2.1tgval3 16983
[Munkres] p. 80Lemma 2.2tgss2 17007  tgss3 17006
[Munkres] p. 81Lemma 2.3basgen 17008  basgen2 17009
[Munkres] p. 89Definition of subspace topologyresttop 17178
[Munkres] p. 93Theorem 6.1(1)0cld 17057  topcld 17054
[Munkres] p. 93Theorem 6.1(2)iincld 17058
[Munkres] p. 93Theorem 6.1(3)uncld 17060
[Munkres] p. 94Definition of closureclsval 17056
[Munkres] p. 94Definition of interiorntrval 17055
[Munkres] p. 95Theorem 6.5(a)clsndisj 17094  elcls 17092
[Munkres] p. 95Theorem 6.5(b)elcls3 17102
[Munkres] p. 97Theorem 6.6clslp 17166  neindisj 17136
[Munkres] p. 97Corollary 6.7cldlp 17168
[Munkres] p. 97Definition of limit pointislp2 17164  lpval 17158
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17333
[Munkres] p. 102Definition of continuous functiondf-cn 17245  iscn 17253  iscn2 17256
[Munkres] p. 107Theorem 7.2(g)cncnp 17298  cncnp2 17299  cncnpi 17296  df-cnp 17246  iscnp 17255  iscnp2 17257
[Munkres] p. 127Theorem 10.1metcn 18526
[Munkres] p. 128Theorem 10.3metcn4 19216
[NielsenChuang] p. 195Equation 4.73unierri 23560
[Pfenning] p. 17Definition XMnatded 21664  natded 21664
[Pfenning] p. 17Definition NNCnatded 21664  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 21664
[Pfenning] p. 18Rule"natded 21664
[Pfenning] p. 18Definition /\Inatded 21664
[Pfenning] p. 18Definition ` `Enatded 21664  natded 21664  natded 21664  natded 21664  natded 21664
[Pfenning] p. 18Definition ` `Inatded 21664  natded 21664  natded 21664  natded 21664  natded 21664
[Pfenning] p. 18Definition ` `ELnatded 21664
[Pfenning] p. 18Definition ` `ERnatded 21664
[Pfenning] p. 18Definition ` `Ea,unatded 21664
[Pfenning] p. 18Definition ` `IRnatded 21664
[Pfenning] p. 18Definition ` `Ianatded 21664
[Pfenning] p. 127Definition =Enatded 21664
[Pfenning] p. 127Definition =Inatded 21664
[Ponnusamy] p. 361Theorem 6.44cphip0l 19117  df-dip 22150  dip0l 22170  ip0l 16822
[Ponnusamy] p. 361Equation 6.45ipval 22152
[Ponnusamy] p. 362Equation I1dipcj 22166
[Ponnusamy] p. 362Equation I3cphdir 19120  dipdir 22296  ipdir 16825  ipdiri 22284
[Ponnusamy] p. 362Equation I4ipidsq 22162
[Ponnusamy] p. 362Equation 6.46ip0i 22279
[Ponnusamy] p. 362Equation 6.47ip1i 22281
[Ponnusamy] p. 362Equation 6.48ip2i 22282
[Ponnusamy] p. 363Equation I2cphass 19126  dipass 22299  ipass 16831  ipassi 22295
[Prugovecki] p. 186Definition of brabraval 23400  df-bra 23306
[Prugovecki] p. 376Equation 8.1df-kb 23307  kbval 23410
[PtakPulmannova] p. 66Proposition 3.2.17atomli 23838
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30370
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 23852  atcvat4i 23853  cvrat3 29924  cvrat4 29925  lsatcvat3 29535
[PtakPulmannova] p. 68Definition 3.2.18cvbr 23738  cvrval 29752  df-cv 23735  df-lcv 29502  lspsncv0 16173
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30382
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30383
[Quine] p. 16Definition 2.1df-clab 2391  rabid 2844
[Quine] p. 17Definition 2.1''dfsb7 2171
[Quine] p. 18Definition 2.7df-cleq 2397
[Quine] p. 19Definition 2.9conventions 21663  df-v 2918
[Quine] p. 34Theorem 5.1abeq2 2509
[Quine] p. 35Theorem 5.2abid2 2521  abid2f 2565
[Quine] p. 40Theorem 6.1sb5 2149
[Quine] p. 40Theorem 6.2sb56 2147  sb6 2148
[Quine] p. 41Theorem 6.3df-clel 2400
[Quine] p. 41Theorem 6.4eqid 2404  eqid1 21714
[Quine] p. 41Theorem 6.5eqcom 2406
[Quine] p. 42Theorem 6.6df-sbc 3122
[Quine] p. 42Theorem 6.7dfsbcq 3123  dfsbcq2 3124
[Quine] p. 43Theorem 6.8vex 2919
[Quine] p. 43Theorem 6.9isset 2920
[Quine] p. 44Theorem 7.3spcgf 2991  spcgv 2996  spcimgf 2989
[Quine] p. 44Theorem 6.11spsbc 3133  spsbcd 3134
[Quine] p. 44Theorem 6.12elex 2924
[Quine] p. 44Theorem 6.13elab 3042  elabg 3043  elabgf 3040
[Quine] p. 44Theorem 6.14noel 3592
[Quine] p. 48Theorem 7.2snprc 3831
[Quine] p. 48Definition 7.1df-pr 3781  df-sn 3780
[Quine] p. 49Theorem 7.4snss 3886  snssg 3892
[Quine] p. 49Theorem 7.5prss 3912  prssg 3913
[Quine] p. 49Theorem 7.6prid1 3872  prid1g 3870  prid2 3873  prid2g 3871  snid 3801  snidg 3799
[Quine] p. 51Theorem 7.13prex 4366  snex 4365  snexALT 4345
[Quine] p. 53Theorem 8.2unisn 3991  unisnALT 28747  unisng 3992
[Quine] p. 53Theorem 8.3uniun 3994
[Quine] p. 54Theorem 8.6elssuni 4003
[Quine] p. 54Theorem 8.7uni0 4002
[Quine] p. 56Theorem 8.17uniabio 5387
[Quine] p. 56Definition 8.18dfiota2 5378
[Quine] p. 57Theorem 8.19iotaval 5388
[Quine] p. 57Theorem 8.22iotanul 5392
[Quine] p. 58Theorem 8.23iotaex 5394
[Quine] p. 58Definition 9.1df-op 3783
[Quine] p. 61Theorem 9.5opabid 4421  opelopab 4436  opelopaba 4431  opelopabaf 4438  opelopabf 4439  opelopabg 4433  opelopabga 4428  oprabid 6064
[Quine] p. 64Definition 9.11df-xp 4843
[Quine] p. 64Definition 9.12df-cnv 4845
[Quine] p. 64Definition 9.15df-id 4458
[Quine] p. 65Theorem 10.3fun0 5467
[Quine] p. 65Theorem 10.4funi 5442
[Quine] p. 65Theorem 10.5funsn 5458  funsng 5456
[Quine] p. 65Definition 10.1df-fun 5415
[Quine] p. 65Definition 10.2args 5191  dffv4 5684
[Quine] p. 68Definition 10.11conventions 21663  df-fv 5421  fv2 5682
[Quine] p. 124Theorem 17.3nn0opth2 11520  nn0opth2i 11519  nn0opthi 11518  omopthi 6859
[Quine] p. 177Definition 25.2df-rdg 6627
[Quine] p. 232Equation icarddom 8385
[Quine] p. 284Axiom 39(vi)funimaex 5490  funimaexg 5489
[Quine] p. 331Axiom system NFru 3120
[ReedSimon] p. 36Definition (iii)ax-his3 22539
[ReedSimon] p. 63Exercise 4(a)df-dip 22150  polid 22614  polid2i 22612  polidi 22613
[ReedSimon] p. 63Exercise 4(b)df-ph 22267
[ReedSimon] p. 195Remarklnophm 23475  lnophmi 23474
[Retherford] p. 49Exercise 1(i)leopadd 23588
[Retherford] p. 49Exercise 1(ii)leopmul 23590  leopmuli 23589
[Retherford] p. 49Exercise 1(iv)leoptr 23593
[Retherford] p. 49Definition VI.1df-leop 23308  leoppos 23582
[Retherford] p. 49Exercise 1(iii)leoptri 23592
[Retherford] p. 49Definition of operator orderingleop3 23581
[Rudin] p. 164Equation 27efcan 12652
[Rudin] p. 164Equation 30efzval 12658
[Rudin] p. 167Equation 48absefi 12752
[Sanford] p. 39Rule 3mtp-xor 1542
[Sanford] p. 39Rule 4mpto2 1540
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 8
[Sanford] p. 39Rule says, "if ` ` is not true, and ` ` implies ` ` , then ` ` must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" mto 169
[Sanford] p. 40Rule 1mpto1 1539
[Schechter] p. 51Definition of antisymmetryintasym 5208
[Schechter] p. 51Definition of irreflexivityintirr 5211
[Schechter] p. 51Definition of symmetrycnvsym 5207
[Schechter] p. 51Definition of transitivitycotr 5205
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13766
[Schechter] p. 79Definition of Moore closuredf-mrc 13767
[Schechter] p. 82Section 4.5df-mrc 13767
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13769
[Schechter] p. 139Definition AC3dfac9 7972
[Schechter] p. 141Definition (MC)dfac11 27028
[Schechter] p. 149Axiom DC1ax-dc 8282  axdc3 8290
[Schechter] p. 187Definition of ring with unitisrng 15623  isrngo 21919
[Schechter] p. 276Remark 11.6.espan0 22997
[Schechter] p. 276Definition of spandf-span 22764  spanval 22788
[Schechter] p. 428Definition 15.35bastop1 17013
[Schwabhauser] p. 10Axiom A1axcgrrflx 25757
[Schwabhauser] p. 10Axiom A2axcgrtr 25758
[Schwabhauser] p. 10Axiom A3axcgrid 25759
[Schwabhauser] p. 11Axiom A4axsegcon 25770
[Schwabhauser] p. 11Axiom A5ax5seg 25781
[Schwabhauser] p. 11Axiom A6axbtwnid 25782
[Schwabhauser] p. 12Axiom A7axpasch 25784
[Schwabhauser] p. 12Axiom A8axlowdim2 25803
[Schwabhauser] p. 13Axiom A10axeuclid 25806
[Schwabhauser] p. 13Axiom A11axcont 25819
[Schwabhauser] p. 27Theorem 2.1cgrrflx 25825
[Schwabhauser] p. 27Theorem 2.2cgrcomim 25827
[Schwabhauser] p. 27Theorem 2.3cgrtr 25830
[Schwabhauser] p. 27Theorem 2.4cgrcoml 25834
[Schwabhauser] p. 27Theorem 2.5cgrcomr 25835
[Schwabhauser] p. 28Theorem 2.8cgrtriv 25840
[Schwabhauser] p. 28Theorem 2.105segofs 25844
[Schwabhauser] p. 28Definition 2.10df-ofs 25821
[Schwabhauser] p. 29Theorem 2.11cgrextend 25846
[Schwabhauser] p. 29Theorem 2.12segconeq 25848
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 25860  btwntriv2 25850
[Schwabhauser] p. 30Theorem 3.2btwncomim 25851
[Schwabhauser] p. 30Theorem 3.3btwntriv1 25854
[Schwabhauser] p. 30Theorem 3.4btwnswapid 25855
[Schwabhauser] p. 30Theorem 3.5btwnexch2 25861  btwnintr 25857
[Schwabhauser] p. 30Theorem 3.6btwnexch 25863  btwnexch3 25858
[Schwabhauser] p. 30Theorem 3.7btwnouttr 25862
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25802
[Schwabhauser] p. 32Theorem 3.14btwndiff 25865
[Schwabhauser] p. 33Theorem 3.17trisegint 25866
[Schwabhauser] p. 34Theorem 4.2ifscgr 25882
[Schwabhauser] p. 34Definition 4.1df-ifs 25877
[Schwabhauser] p. 35Theorem 4.3cgrsub 25883
[Schwabhauser] p. 35Theorem 4.5cgrxfr 25893
[Schwabhauser] p. 35Definition 4.4df-cgr3 25878
[Schwabhauser] p. 36Theorem 4.6btwnxfr 25894
[Schwabhauser] p. 36Theorem 4.11colinearperm1 25900  colinearperm2 25902  colinearperm3 25901  colinearperm4 25903  colinearperm5 25904
[Schwabhauser] p. 36Definition 4.10df-colinear 25879
[Schwabhauser] p. 37Theorem 4.12colineartriv1 25905
[Schwabhauser] p. 37Theorem 4.13colinearxfr 25913
[Schwabhauser] p. 37Theorem 4.14lineext 25914
[Schwabhauser] p. 37Theorem 4.16fscgr 25918
[Schwabhauser] p. 37Theorem 4.17linecgr 25919
[Schwabhauser] p. 37Definition 4.15df-fs 25880
[Schwabhauser] p. 38Theorem 4.18lineid 25921
[Schwabhauser] p. 38Theorem 4.19idinside 25922
[Schwabhauser] p. 39Theorem 5.1btwnconn1 25939
[Schwabhauser] p. 41Theorem 5.2btwnconn2 25940
[Schwabhauser] p. 41Theorem 5.3btwnconn3 25941
[Schwabhauser] p. 41Theorem 5.5brsegle2 25947
[Schwabhauser] p. 41Definition 5.4df-segle 25945
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 25948
[Schwabhauser] p. 42Theorem 5.7seglerflx 25950
[Schwabhauser] p. 42Theorem 5.8segletr 25952
[Schwabhauser] p. 42Theorem 5.9segleantisym 25953
[Schwabhauser] p. 42Theorem 5.10seglelin 25954
[Schwabhauser] p. 42Theorem 5.11seglemin 25951
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 25956
[Schwabhauser] p. 43Theorem 6.2btwnoutside 25963
[Schwabhauser] p. 43Theorem 6.3broutsideof3 25964
[Schwabhauser] p. 43Theorem 6.4broutsideof 25959  df-outsideof 25958
[Schwabhauser] p. 43Definition 6.1broutsideof2 25960
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 25965
[Schwabhauser] p. 44Theorem 6.6outsideofcom 25966
[Schwabhauser] p. 44Theorem 6.7outsideoftr 25967
[Schwabhauser] p. 44Theorem 6.11outsideofeu 25969
[Schwabhauser] p. 44Definition 6.8df-ray 25976
[Schwabhauser] p. 45Part 2df-lines2 25977
[Schwabhauser] p. 45Theorem 6.13outsidele 25970
[Schwabhauser] p. 45Theorem 6.15lineunray 25985
[Schwabhauser] p. 45Theorem 6.16lineelsb2 25986
[Schwabhauser] p. 45Theorem 6.17linecom 25988  linerflx1 25987  linerflx2 25989
[Schwabhauser] p. 45Theorem 6.18linethru 25991
[Schwabhauser] p. 45Definition 6.14df-line2 25975
[Schwabhauser] p. 46Theorem 6.19linethrueu 25994
[Schwabhauser] p. 46Theorem 6.21lineintmo 25995
[Shapiro] p. 230Theorem 6.5.1dchrhash 21008  dchrsum 21006  dchrsum2 21005  sumdchr 21009
[Shapiro] p. 232Theorem 6.5.2dchr2sum 21010  sum2dchr 21011
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15579  ablfacrp2 15580
[Shapiro], p. 328Equation 9.2.4vmasum 20953
[Shapiro], p. 329Equation 9.2.7logfac2 20954
[Shapiro], p. 329Equation 9.2.9logfacrlim 20961
[Shapiro], p. 331Equation 9.2.13vmadivsum 21129
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 21132
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 21186  vmalogdivsum2 21185
[Shapiro], p. 375Theorem 9.4.1dirith 21176  dirith2 21175
[Shapiro], p. 375Equation 9.4.3rplogsum 21174  rpvmasum 21173  rpvmasum2 21159
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 21134
[Shapiro], p. 376Equation 9.4.8dchrvmasum 21172
[Shapiro], p. 377Lemma 9.4.1dchrisum 21139  dchrisumlem1 21136  dchrisumlem2 21137  dchrisumlem3 21138  dchrisumlema 21135
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 21142
[Shapiro], p. 379Equation 9.4.16dchrmusum 21171  dchrmusumlem 21169  dchrvmasumlem 21170
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 21141
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 21143
[Shapiro], p. 382Lemma 9.4.4dchrisum0 21167  dchrisum0re 21160  dchrisumn0 21168
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 21153
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 21157
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 21158
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 21213  pntrsumbnd2 21214  pntrsumo1 21212
[Shapiro], p. 405Equation 10.2.1mudivsum 21177
[Shapiro], p. 406Equation 10.2.6mulogsum 21179
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 21181
[Shapiro], p. 407Equation 10.2.8mulog2sum 21184
[Shapiro], p. 418Equation 10.4.6logsqvma 21189
[Shapiro], p. 418Equation 10.4.8logsqvma2 21190
[Shapiro], p. 419Equation 10.4.10selberg 21195
[Shapiro], p. 420Equation 10.4.12selberg2lem 21197
[Shapiro], p. 420Equation 10.4.14selberg2 21198
[Shapiro], p. 422Equation 10.6.7selberg3 21206
[Shapiro], p. 422Equation 10.4.20selberg4lem1 21207
[Shapiro], p. 422Equation 10.4.21selberg3lem1 21204  selberg3lem2 21205
[Shapiro], p. 422Equation 10.4.23selberg4 21208
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 21202
[Shapiro], p. 428Equation 10.6.2selbergr 21215
[Shapiro], p. 429Equation 10.6.8selberg3r 21216
[Shapiro], p. 430Equation 10.6.11selberg4r 21217
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 21231
[Shapiro], p. 434Equation 10.6.27pntlema 21243  pntlemb 21244  pntlemc 21242  pntlemd 21241  pntlemg 21245
[Shapiro], p. 435Equation 10.6.29pntlema 21243
[Shapiro], p. 436Lemma 10.6.1pntpbnd 21235
[Shapiro], p. 436Lemma 10.6.2pntibnd 21240
[Shapiro], p. 436Equation 10.6.34pntlema 21243
[Shapiro], p. 436Equation 10.6.35pntlem3 21256  pntleml 21258
[Stoll] p. 13Definition of symmetric differencesymdif1 3566
[Stoll] p. 16Exercise 4.40dif 3659  dif0 3658
[Stoll] p. 16Exercise 4.8difdifdir 3675
[Stoll] p. 17Theorem 5.1(5)undifv 3662
[Stoll] p. 19Theorem 5.2(13)undm 3559
[Stoll] p. 19Theorem 5.2(13')indm 3560
[Stoll] p. 20Remarkinvdif 3542
[Stoll] p. 25Definition of ordered tripledf-ot 3784
[Stoll] p. 43Definitionuniiun 4104
[Stoll] p. 44Definitionintiin 4105
[Stoll] p. 45Definitiondf-iin 4056
[Stoll] p. 45Definition indexed uniondf-iun 4055
[Stoll] p. 176Theorem 3.4(27)iman 414
[Stoll] p. 262Example 4.1symdif1 3566
[Strang] p. 242Section 6.3expgrowth 27420
[Suppes] p. 22Theorem 2eq0 3602
[Suppes] p. 22Theorem 4eqss 3323  eqssd 3325  eqssi 3324
[Suppes] p. 23Theorem 5ss0 3618  ss0b 3617
[Suppes] p. 23Theorem 6sstr 3316  sstrALT2 28656
[Suppes] p. 23Theorem 7pssirr 3407
[Suppes] p. 23Theorem 8pssn2lp 3408
[Suppes] p. 23Theorem 9psstr 3411
[Suppes] p. 23Theorem 10pssss 3402
[Suppes] p. 25Theorem 12elin 3490  elun 3448
[Suppes] p. 26Theorem 15inidm 3510
[Suppes] p. 26Theorem 16in0 3613
[Suppes] p. 27Theorem 23unidm 3450
[Suppes] p. 27Theorem 24un0 3612
[Suppes] p. 27Theorem 25ssun1 3470
[Suppes] p. 27Theorem 26ssequn1 3477
[Suppes] p. 27Theorem 27unss 3481
[Suppes] p. 27Theorem 28indir 3549
[Suppes] p. 27Theorem 29undir 3550
[Suppes] p. 28Theorem 32difid 3656  difidALT 3657
[Suppes] p. 29Theorem 33difin 3538
[Suppes] p. 29Theorem 34indif 3543
[Suppes] p. 29Theorem 35undif1 3663
[Suppes] p. 29Theorem 36difun2 3667
[Suppes] p. 29Theorem 37difin0 3661
[Suppes] p. 29Theorem 38disjdif 3660
[Suppes] p. 29Theorem 39difundi 3553
[Suppes] p. 29Theorem 40difindi 3555
[Suppes] p. 30Theorem 41nalset 4300
[Suppes] p. 39Theorem 61uniss 3996
[Suppes] p. 39Theorem 65uniop 4419
[Suppes] p. 41Theorem 70intsn 4046
[Suppes] p. 42Theorem 71intpr 4043  intprg 4044
[Suppes] p. 42Theorem 73op1stb 4717
[Suppes] p. 42Theorem 78intun 4042
[Suppes] p. 44Definition 15(a)dfiun2 4085  dfiun2g 4083
[Suppes] p. 44Definition 15(b)dfiin2 4086
[Suppes] p. 47Theorem 86elpw 3765  elpw2 4324  elpw2g 4323  elpwg 3766  elpwgdedVD 28738
[Suppes] p. 47Theorem 87pwid 3772
[Suppes] p. 47Theorem 89pw0 3905
[Suppes] p. 48Theorem 90pwpw0 3906
[Suppes] p. 52Theorem 101xpss12 4940
[Suppes] p. 52Theorem 102xpindi 4967  xpindir 4968
[Suppes] p. 52Theorem 103xpundi 4889  xpundir 4890
[Suppes] p. 54Theorem 105elirrv 7521
[Suppes] p. 58Theorem 2relss 4922
[Suppes] p. 59Theorem 4eldm 5026  eldm2 5027  eldm2g 5025  eldmg 5024
[Suppes] p. 59Definition 3df-dm 4847
[Suppes] p. 60Theorem 6dmin 5036
[Suppes] p. 60Theorem 8rnun 5239
[Suppes] p. 60Theorem 9rnin 5240
[Suppes] p. 60Definition 4dfrn2 5018
[Suppes] p. 61Theorem 11brcnv 5014  brcnvg 5012
[Suppes] p. 62Equation 5elcnv 5008  elcnv2 5009
[Suppes] p. 62Theorem 12relcnv 5201
[Suppes] p. 62Theorem 15cnvin 5238
[Suppes] p. 62Theorem 16cnvun 5236
[Suppes] p. 63Theorem 20co02 5342
[Suppes] p. 63Theorem 21dmcoss 5094
[Suppes] p. 63Definition 7df-co 4846
[Suppes] p. 64Theorem 26cnvco 5015
[Suppes] p. 64Theorem 27coass 5347
[Suppes] p. 65Theorem 31resundi 5119
[Suppes] p. 65Theorem 34elima 5167  elima2 5168  elima3 5169  elimag 5166
[Suppes] p. 65Theorem 35imaundi 5243
[Suppes] p. 66Theorem 40dminss 5245
[Suppes] p. 66Theorem 41imainss 5246
[Suppes] p. 67Exercise 11cnvxp 5249
[Suppes] p. 81Definition 34dfec2 6867
[Suppes] p. 82Theorem 72elec 6903  elecg 6902
[Suppes] p. 82Theorem 73erth 6908  erth2 6909
[Suppes] p. 83Theorem 74erdisj 6911
[Suppes] p. 89Theorem 96map0b 7011
[Suppes] p. 89Theorem 97map0 7013  map0g 7012
[Suppes] p. 89Theorem 98mapsn 7014
[Suppes] p. 89Theorem 99mapss 7015
[Suppes] p. 91Definition 12(ii)alephsuc 7905
[Suppes] p. 91Definition 12(iii)alephlim 7904
[Suppes] p. 92Theorem 1enref 7099  enrefg 7098
[Suppes] p. 92Theorem 2ensym 7115  ensymb 7114  ensymi 7116
[Suppes] p. 92Theorem 3entr 7118
[Suppes] p. 92Theorem 4unen 7148
[Suppes] p. 94Theorem 15endom 7093
[Suppes] p. 94Theorem 16ssdomg 7112
[Suppes] p. 94Theorem 17domtr 7119
[Suppes] p. 95Theorem 18sbth 7186
[Suppes] p. 97Theorem 23canth2 7219  canth2g 7220
[Suppes] p. 97Definition 3brsdom2 7190  df-sdom 7071  dfsdom2 7189
[Suppes] p. 97Theorem 21(i)sdomirr 7203
[Suppes] p. 97Theorem 22(i)domnsym 7192
[Suppes] p. 97Theorem 21(ii)sdomnsym 7191
[Suppes] p. 97Theorem 22(ii)domsdomtr 7201
[Suppes] p. 97Theorem 22(iv)brdom2 7096
[Suppes] p. 97Theorem 21(iii)sdomtr 7204
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7199
[Suppes] p. 98Exercise 4fundmen 7139  fundmeng 7140
[Suppes] p. 98Exercise 6xpdom3 7165
[Suppes] p. 98Exercise 11sdomentr 7200
[Suppes] p. 104Theorem 37fofi 7351
[Suppes] p. 104Theorem 38pwfi 7360
[Suppes] p. 105Theorem 40pwfi 7360
[Suppes] p. 111Axiom for cardinal numberscarden 8382
[Suppes] p. 130Definition 3df-tr 4263
[Suppes] p. 132Theorem 9ssonuni 4726
[Suppes] p. 134Definition 6df-suc 4547
[Suppes] p. 136Theorem Schema 22findes 4834  finds 4830  finds1 4833  finds2 4832
[Suppes] p. 151Theorem 42isfinite 7563  isfinite2 7324  isfiniteg 7326  unbnn 7322
[Suppes] p. 162Definition 5df-ltnq 8751  df-ltpq 8743
[Suppes] p. 197Theorem Schema 4tfindes 4801  tfinds 4798  tfinds2 4802
[Suppes] p. 209Theorem 18oaord1 6753
[Suppes] p. 209Theorem 21oaword2 6755
[Suppes] p. 211Theorem 25oaass 6763
[Suppes] p. 225Definition 8iscard2 7819
[Suppes] p. 227Theorem 56ondomon 8394
[Suppes] p. 228Theorem 59harcard 7821
[Suppes] p. 228Definition 12(i)aleph0 7903
[Suppes] p. 228Theorem Schema 61onintss 4591
[Suppes] p. 228Theorem Schema 62onminesb 4737  onminsb 4738
[Suppes] p. 229Theorem 64alephval2 8403
[Suppes] p. 229Theorem 65alephcard 7907
[Suppes] p. 229Theorem 66alephord2i 7914
[Suppes] p. 229Theorem 67alephnbtwn 7908
[Suppes] p. 229Definition 12df-aleph 7783
[Suppes] p. 242Theorem 6weth 8331
[Suppes] p. 242Theorem 8entric 8388
[Suppes] p. 242Theorem 9carden 8382
[TakeutiZaring] p. 8Axiom 1ax-ext 2385
[TakeutiZaring] p. 13Definition 4.5df-cleq 2397
[TakeutiZaring] p. 13Proposition 4.6df-clel 2400
[TakeutiZaring] p. 13Proposition 4.9cvjust 2399
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2421
[TakeutiZaring] p. 14Definition 4.16df-oprab 6044
[TakeutiZaring] p. 14Proposition 4.14ru 3120
[TakeutiZaring] p. 15Axiom 2zfpair 4361
[TakeutiZaring] p. 15Exercise 1elpr 3792  elpr2 3793  elprg 3791
[TakeutiZaring] p. 15Exercise 2elsn 3789  elsnc 3797  elsnc2 3803  elsnc2g 3802  elsncg 3796
[TakeutiZaring] p. 15Exercise 3elop 4389
[TakeutiZaring] p. 15Exercise 4sneq 3785  sneqr 3926
[TakeutiZaring] p. 15Definition 5.1dfpr2 3790  dfsn2 3788
[TakeutiZaring] p. 16Axiom 3uniex 4664
[TakeutiZaring] p. 16Exercise 6opth 4395
[TakeutiZaring] p. 16Exercise 7opex 4387
[TakeutiZaring] p. 16Exercise 8rext 4372
[TakeutiZaring] p. 16Corollary 5.8unex 4666  unexg 4669
[TakeutiZaring] p. 16Definition 5.3dftp2 3814
[TakeutiZaring] p. 16Definition 5.5df-uni 3976
[TakeutiZaring] p. 16Definition 5.6df-in 3287  df-un 3285
[TakeutiZaring] p. 16Proposition 5.7unipr 3989  uniprg 3990
[TakeutiZaring] p. 17Axiom 4pwex 4342  pwexg 4343
[TakeutiZaring] p. 17Exercise 1eltp 3813
[TakeutiZaring] p. 17Exercise 5elsuc 4610  elsucg 4608  sstr2 3315
[TakeutiZaring] p. 17Exercise 6uncom 3451
[TakeutiZaring] p. 17Exercise 7incom 3493
[TakeutiZaring] p. 17Exercise 8unass 3464
[TakeutiZaring] p. 17Exercise 9inass 3511
[TakeutiZaring] p. 17Exercise 10indi 3547
[TakeutiZaring] p. 17Exercise 11undi 3548
[TakeutiZaring] p. 17Definition 5.9df-pss 3296  dfss2 3297
[TakeutiZaring] p. 17Definition 5.10df-pw 3761
[TakeutiZaring] p. 18Exercise 7unss2 3478
[TakeutiZaring] p. 18Exercise 9df-ss 3294  sseqin2 3520
[TakeutiZaring] p. 18Exercise 10ssid 3327
[TakeutiZaring] p. 18Exercise 12inss1 3521  inss2 3522
[TakeutiZaring] p. 18Exercise 13nss 3366
[TakeutiZaring] p. 18Exercise 15unieq 3984
[TakeutiZaring] p. 18Exercise 18sspwb 4373  sspwimp 28739  sspwimpALT 28746  sspwimpALT2 28750  sspwimpcf 28741
[TakeutiZaring] p. 18Exercise 19pweqb 4380
[TakeutiZaring] p. 19Axiom 5ax-rep 4280
[TakeutiZaring] p. 20Definitiondf-rab 2675
[TakeutiZaring] p. 20Corollary 5.160ex 4299
[TakeutiZaring] p. 20Definition 5.12df-dif 3283
[TakeutiZaring] p. 20Definition 5.14dfnul2 3590
[TakeutiZaring] p. 20Proposition 5.15difid 3656  difidALT 3657
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3597  n0f 3596  neq0 3598
[TakeutiZaring] p. 21Axiom 6zfreg 7519
[TakeutiZaring] p. 21Axiom 6'zfregs 7624
[TakeutiZaring] p. 21Theorem 5.22setind 7629
[TakeutiZaring] p. 21Definition 5.20df-v 2918
[TakeutiZaring] p. 21Proposition 5.21vprc 4301
[TakeutiZaring] p. 22Exercise 10ss 3616
[TakeutiZaring] p. 22Exercise 3ssex 4307  ssexg 4309
[TakeutiZaring] p. 22Exercise 4inex1 4304
[TakeutiZaring] p. 22Exercise 5ruv 7524
[TakeutiZaring] p. 22Exercise 6elirr 7522
[TakeutiZaring] p. 22Exercise 7ssdif0 3646
[TakeutiZaring] p. 22Exercise 11difdif 3433
[TakeutiZaring] p. 22Exercise 13undif3 3562  undif3VD 28703
[TakeutiZaring] p. 22Exercise 14difss 3434
[TakeutiZaring] p. 22Exercise 15sscon 3441
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2671
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2672
[TakeutiZaring] p. 23Proposition 6.2xpex 4949  xpexg 4948  xpexgALT 6256
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4844
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5472
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5606  fun11 5475
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5425  svrelfun 5473
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5017
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5019
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4849
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4850
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4846
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5284  dfrel2 5280
[TakeutiZaring] p. 25Exercise 3xpss 4941
[TakeutiZaring] p. 25Exercise 5relun 4950
[TakeutiZaring] p. 25Exercise 6reluni 4956
[TakeutiZaring] p. 25Exercise 9inxp 4966
[TakeutiZaring] p. 25Exercise 12relres 5133
[TakeutiZaring] p. 25Exercise 13opelres 5110  opelresg 5112
[TakeutiZaring] p. 25Exercise 14dmres 5126
[TakeutiZaring] p. 25Exercise 15resss 5129
[TakeutiZaring] p. 25Exercise 17resabs1 5134
[TakeutiZaring] p. 25Exercise 18funres 5451
[TakeutiZaring] p. 25Exercise 24relco 5327
[TakeutiZaring] p. 25Exercise 29funco 5450
[TakeutiZaring] p. 25Exercise 30f1co 5607
[TakeutiZaring] p. 26Definition 6.10eu2 2279
[TakeutiZaring] p. 26Definition 6.11conventions 21663  df-fv 5421  fv3 5703
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5365  cnvexg 5364
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5091  dmexg 5089
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5092  rnexg 5090
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27525
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27526
[TakeutiZaring] p. 27Corollary 6.13fvex 5701
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 27905  tz6.12-1 5706  tz6.12-afv 27904  tz6.12 5707  tz6.12c 5709
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5678  tz6.12i 5710
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5416
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5417
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5419  wfo 5411
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5418  wf1 5410
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5420  wf1o 5412
[TakeutiZaring] p. 28Exercise 4eqfnfv 5786  eqfnfv2 5787  eqfnfv2f 5790
[TakeutiZaring] p. 28Exercise 5fvco 5758
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5920  fnexALT 5921
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5916  resfunexgALT 5917
[TakeutiZaring] p. 29Exercise 9funimaex 5490  funimaexg 5489
[TakeutiZaring] p. 29Definition 6.18df-br 4173
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4464
[TakeutiZaring] p. 30Definition 6.21dffr2 4507  dffr3 5195  eliniseg 5192  iniseg 5194
[TakeutiZaring] p. 30Definition 6.22df-eprel 4454
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4520  fr3nr 4719  frirr 4519
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4501
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4721
[TakeutiZaring] p. 31Exercise 1frss 4509
[TakeutiZaring] p. 31Exercise 4wess 4529
[TakeutiZaring] p. 31Proposition 6.26tz6.26 25419  tz6.26i 25420  wefrc 4536  wereu2 4539
[TakeutiZaring] p. 32Theorem 6.27wfi 25421  wfii 25422
[TakeutiZaring] p. 32Definition 6.28df-isom 5422
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6008
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6009
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6015
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6016
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6017
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6021
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6028
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6030
[TakeutiZaring] p. 35Notationwtr 4262
[TakeutiZaring] p. 35Theorem 7.2trelpss 27527  tz7.2 4526
[TakeutiZaring] p. 35Definition 7.1dftr3 4266
[TakeutiZaring] p. 36Proposition 7.4ordwe 4554
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4562
[TakeutiZaring] p. 36Proposition 7.6ordelord 4563  ordelordALT 28333  ordelordALTVD 28688
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4569  ordelssne 4568
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4567
[TakeutiZaring] p. 37Proposition 7.9ordin 4571
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4728
[TakeutiZaring] p. 38Corollary 7.15ordsson 4729
[TakeutiZaring] p. 38Definition 7.11df-on 4545
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4573
[TakeutiZaring] p. 38Proposition 7.12onfrALT 28346  ordon 4722
[TakeutiZaring] p. 38Proposition 7.13onprc 4724
[TakeutiZaring] p. 39Theorem 7.17tfi 4792
[TakeutiZaring] p. 40Exercise 3ontr2 4588
[TakeutiZaring] p. 40Exercise 7dftr2 4264
[TakeutiZaring] p. 40Exercise 9onssmin 4736
[TakeutiZaring] p. 40Exercise 11unon 4770
[TakeutiZaring] p. 40Exercise 12ordun 4642
[TakeutiZaring] p. 40Exercise 14ordequn 4641
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4725
[TakeutiZaring] p. 40Proposition 7.20elssuni 4003
[TakeutiZaring] p. 41Definition 7.22df-suc 4547
[TakeutiZaring] p. 41Proposition 7.23sssucid 4618  sucidg 4619
[TakeutiZaring] p. 41Proposition 7.24suceloni 4752
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4632  ordnbtwn 4631
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4767
[TakeutiZaring] p. 42Exercise 1df-lim 4546
[TakeutiZaring] p. 42Exercise 4omssnlim 4818
[TakeutiZaring] p. 42Exercise 7ssnlim 4822
[TakeutiZaring] p. 42Exercise 8onsucssi 4780  ordelsuc 4759
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4761
[TakeutiZaring] p. 42Definition 7.27nlimon 4790
[TakeutiZaring] p. 42Definition 7.28dfom2 4806
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4823
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4824
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4825
[TakeutiZaring] p. 43Remarkomon 4815
[TakeutiZaring] p. 43Axiom 7inf3 7546  omex 7554
[TakeutiZaring] p. 43Theorem 7.32ordom 4813
[TakeutiZaring] p. 43Corollary 7.31find 4829
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4826
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4827
[TakeutiZaring] p. 44Exercise 1limomss 4809
[TakeutiZaring] p. 44Exercise 2int0 4024  trint0 4279
[TakeutiZaring] p. 44Exercise 4intss1 4025
[TakeutiZaring] p. 44Exercise 5intex 4316
[TakeutiZaring] p. 44Exercise 6oninton 4739
[TakeutiZaring] p. 44Exercise 11ordintdif 4590
[TakeutiZaring] p. 44Definition 7.35df-int 4011
[TakeutiZaring] p. 44Proposition 7.34noinfep 7570
[TakeutiZaring] p. 45Exercise 4onint 4734
[TakeutiZaring] p. 47Lemma 1tfrlem1 6595
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6617
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6618
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6619
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6623  tz7.44-2 6624  tz7.44-3 6625
[TakeutiZaring] p. 50Exercise 1smogt 6588
[TakeutiZaring] p. 50Exercise 3smoiso 6583
[TakeutiZaring] p. 50Definition 7.46df-smo 6567
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6661  tz7.49c 6662
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6659
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6658
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6660
[TakeutiZaring] p. 53Proposition 7.532eu5 2338
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7849
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7850
[TakeutiZaring] p. 56Definition 8.1oalim 6735  oasuc 6727
[TakeutiZaring] p. 57Remarktfindsg 4799
[TakeutiZaring] p. 57Proposition 8.2oacl 6738
[TakeutiZaring] p. 57Proposition 8.3oa0 6719  oa0r 6741
[TakeutiZaring] p. 57Proposition 8.16omcl 6739
[TakeutiZaring] p. 58Corollary 8.5oacan 6750
[TakeutiZaring] p. 58Proposition 8.4nnaord 6821  nnaordi 6820  oaord 6749  oaordi 6748
[TakeutiZaring] p. 59Proposition 8.6iunss2 4096  uniss2 4006
[TakeutiZaring] p. 59Proposition 8.7oawordri 6752
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6757  oawordex 6759
[TakeutiZaring] p. 59Proposition 8.9nnacl 6813
[TakeutiZaring] p. 59Proposition 8.10oaabs 6846
[TakeutiZaring] p. 60Remarkoancom 7562
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6762
[TakeutiZaring] p. 62Exercise 1nnarcl 6818
[TakeutiZaring] p. 62Exercise 5oaword1 6754
[TakeutiZaring] p. 62Definition 8.15om0 6720  om0x 6722  omlim 6736  omsuc 6729
[TakeutiZaring] p. 63Proposition 8.17nnecl 6815  nnmcl 6814
[TakeutiZaring] p. 63Proposition 8.19nnmord 6834  nnmordi 6833  omord 6770  omordi 6768
[TakeutiZaring] p. 63Proposition 8.20omcan 6771
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6838  omwordri 6774
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6742
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6744  om1r 6745
[TakeutiZaring] p. 64Proposition 8.22om00 6777
[TakeutiZaring] p. 64Proposition 8.23omordlim 6779
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6780
[TakeutiZaring] p. 64Proposition 8.25odi 6781
[TakeutiZaring] p. 65Theorem 8.26omass 6782
[TakeutiZaring] p. 67Definition 8.30nnesuc 6810  oe0 6725  oelim 6737  oesuc 6730  onesuc 6733
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6723
[TakeutiZaring] p. 67Proposition 8.32oen0 6788
[TakeutiZaring] p. 67Proposition 8.33oeordi 6789
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6724
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6747
[TakeutiZaring] p. 68Corollary 8.34oeord 6790
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6796
[TakeutiZaring] p. 68Proposition 8.35oewordri 6794
[TakeutiZaring] p. 68Proposition 8.37oeworde 6795
[TakeutiZaring] p. 69Proposition 8.41oeoa 6799
[TakeutiZaring] p. 70Proposition 8.42oeoe 6801
[TakeutiZaring] p. 73Theorem 9.1trcl 7620  tz9.1 7621
[TakeutiZaring] p. 76Definition 9.9df-r1 7646  r10 7650  r1lim 7654  r1limg 7653  r1suc 7652  r1sucg 7651
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7662  r1ord2 7663  r1ordg 7660
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7672
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7697  tz9.13 7673  tz9.13g 7674
[TakeutiZaring] p. 79Definition 9.14df-rank 7647  rankval 7698  rankvalb 7679  rankvalg 7699
[TakeutiZaring] p. 79Proposition 9.16rankel 7721  rankelb 7706
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7735  rankval3 7722  rankval3b 7708
[TakeutiZaring] p. 79Proposition 9.18rankonid 7711
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7677
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7716  rankr1c 7703  rankr1g 7714
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7717
[TakeutiZaring] p. 80Exercise 1rankss 7731  rankssb 7730
[TakeutiZaring] p. 80Exercise 2unbndrank 7724
[TakeutiZaring] p. 80Proposition 9.19bndrank 7723
[TakeutiZaring] p. 83Axiom of Choiceac4 8311  dfac3 7958
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7867  numth 8308  numth2 8307
[TakeutiZaring] p. 85Definition 10.4cardval 8377
[TakeutiZaring] p. 85Proposition 10.5cardid 8378  cardid2 7796
[TakeutiZaring] p. 85Proposition 10.9oncard 7803
[TakeutiZaring] p. 85Proposition 10.10carden 8382
[TakeutiZaring] p. 85Proposition 10.11cardidm 7802
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7787
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7808
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7800
[TakeutiZaring] p. 87Proposition 10.15pwen 7239
[TakeutiZaring] p. 88Exercise 1en0 7129
[TakeutiZaring] p. 88Exercise 7infensuc 7244
[TakeutiZaring] p. 89Exercise 10omxpen 7169
[TakeutiZaring] p. 90Corollary 10.23cardnn 7806
[TakeutiZaring] p. 90Definition 10.27alephiso 7935
[TakeutiZaring] p. 90Proposition 10.20nneneq 7249
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7255
[TakeutiZaring] p. 90Proposition 10.26alephprc 7936
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7254
[TakeutiZaring] p. 91Exercise 2alephle 7925
[TakeutiZaring] p. 91Exercise 3aleph0 7903
[TakeutiZaring] p. 91Exercise 4cardlim 7815
[TakeutiZaring] p. 91Exercise 7infpss 8053
[TakeutiZaring] p. 91Exercise 8infcntss 7339
[TakeutiZaring] p. 91Definition 10.29df-fin 7072  isfi 7090
[TakeutiZaring] p. 92Proposition 10.32onfin 7256
[TakeutiZaring] p. 92Proposition 10.34imadomg 8368
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 7162
[TakeutiZaring] p. 93Proposition 10.35fodomb 8360
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8025  unxpdom 7275
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7817  cardsdomelir 7816
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7277
[TakeutiZaring] p. 94Proposition 10.39infxpen 7852
[TakeutiZaring] p. 95Definition 10.42df-map 6979
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8393  infxpidm2 7854
[TakeutiZaring] p. 95Proposition 10.41infcda 8044  infxp 8051
[TakeutiZaring] p. 96Proposition 10.44pw2en 7174  pw2f1o 7172
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7232
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8323
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8318  ac6s5 8327
[TakeutiZaring] p. 98Theorem 10.47unidom 8374
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8375  uniimadomf 8376
[TakeutiZaring] p. 100Definition 11.1cfcof 8110
[TakeutiZaring] p. 101Proposition 11.7cofsmo 8105
[TakeutiZaring] p. 102Exercise 1cfle 8090
[TakeutiZaring] p. 102Exercise 2cf0 8087
[TakeutiZaring] p. 102Exercise 3cfsuc 8093
[TakeutiZaring] p. 102Exercise 4cfom 8100
[TakeutiZaring] p. 102Proposition 11.9coftr 8109
[TakeutiZaring] p. 103Theorem 11.15alephreg 8413
[TakeutiZaring] p. 103Proposition 11.11cardcf 8088
[TakeutiZaring] p. 103Proposition 11.13alephsing 8112
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7934
[TakeutiZaring] p. 104Proposition 11.16carduniima 7933
[TakeutiZaring] p. 104Proposition 11.18alephfp 7945  alephfp2 7946
[TakeutiZaring] p. 106Theorem 11.20gchina 8530
[TakeutiZaring] p. 106Theorem 11.21mappwen 7949
[TakeutiZaring] p. 107Theorem 11.26konigth 8400
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8414
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8415
[Tarski] p. 67Axiom B5ax-4 2185
[Tarski] p. 67Scheme B5sp 1759
[Tarski] p. 68Lemma 6avril1 21710  equid 1684  equid1 2208  equid1ALT 2226
[Tarski] p. 69Lemma 7equcomi 1687
[Tarski] p. 70Lemma 14spim 1955  spime 1960  spimeh 1675
[Tarski] p. 70Lemma 16ax-11 1757  ax-11o 2191  ax11i 1654
[Tarski] p. 70Lemmas 16 and 17sb6 2148
[Tarski] p. 75Axiom B7ax9v 1663
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1623  ax17o 2207
[Tarski], p. 75Scheme B8 of system S2ax-13 1723  ax-14 1725  ax-8 1683
[Truss] p. 114Theorem 5.18ruc 12797
[Viaclovsky7] p. 3Proposition 0.3mblfinlem2 26144
[Viaclovsky8] p. 3Proposition 7ismblfin 26146
[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 2351  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 28748
[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 21663  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 26134
[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 26127
[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 27421
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27422
[WhiteheadRussell] p. 147Theorem *10.2219.26 1600
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27423
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27424
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27425
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1622
[WhiteheadRussell] p. 151Theorem *10.301albitr 27426
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27427
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27428
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27429
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27430
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27432
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27433
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27434
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27431
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2164
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27437
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27438
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27439
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1749
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27440
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27441
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27442
[WhiteheadRussell] p. 162Theorem *11.322alim 27443
[WhiteheadRussell] p. 162Theorem *11.332albi 27444
[WhiteheadRussell] p. 162Theorem *11.342exim 27445
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27447
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27446
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1617
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27449
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27450
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27448
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1579
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27451
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27452
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1587
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27453
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1912
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27454
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27459
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27455
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27456
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27457
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27458
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27463
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27460
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27461
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27462
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27464
[WhiteheadRussell] p. 175Definition *14.02df-eu 2258
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27475  pm13.13b 27476
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27477
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2639
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2640
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3036
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27483
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27484
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27478
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 28350  pm13.193 27479
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27480
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27481
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27482
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27489
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27488
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27487
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3173
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27490  pm14.122b 27491  pm14.122c 27492
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27493  pm14.123b 27494  pm14.123c 27495
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27497
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27496
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27498
[WhiteheadRussell] p. 190Theorem *14.22iota4 5395
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27499
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5396
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27500
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27502
[WhiteheadRussell] p. 192Theorem *14.26eupick 2317  eupickbi 2320  sbaniota 27503
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27501
[WhiteheadRussell] p. 192Theorem *14.271eubi 27504
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27505
[WhiteheadRussell] p. 235Definition *30.01conventions 21663  df-fv 5421
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7843  pm54.43lem 7842
[Young] p. 141Definition of operator orderingleop2 23580
[Young] p. 142Example 12.2(i)0leop 23586  idleop 23587
[vandenDries] p. 42Lemma 61irrapx1 26781
[vandenDries] p. 43Theorem 62pellex 26788  pellexlem1 26782

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