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 13981
[Adamek] p. 29Proposition 3.14(1)invinv 13995
[Adamek] p. 29Proposition 3.14(2)invco 13996  isoco 13998
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18742  df-nmoo 22246
[AkhiezerGlazman] p. 64Theoremhmopidmch 23656  hmopidmchi 23654
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 23704  pjcmul2i 23705
[AkhiezerGlazman] p. 72Theoremcnvunop 23421  unoplin 23423
[AkhiezerGlazman] p. 72Equation 2unopadj 23422  unopadj2 23441
[AkhiezerGlazman] p. 73Theoremelunop2 23516  lnopunii 23515
[AkhiezerGlazman] p. 80Proposition 1adjlnop 23589
[Apostol] p. 18Theorem I.1addcan 9250  addcan2d 9270  addcan2i 9260  addcand 9269  addcani 9259
[Apostol] p. 18Theorem I.2negeu 9296
[Apostol] p. 18Theorem I.3negsub 9349  negsubd 9417  negsubi 9378
[Apostol] p. 18Theorem I.4negneg 9351  negnegd 9402  negnegi 9370
[Apostol] p. 18Theorem I.5subdi 9467  subdid 9489  subdii 9482  subdir 9468  subdird 9490  subdiri 9483
[Apostol] p. 18Theorem I.6mul01 9245  mul01d 9265  mul01i 9256  mul02 9244  mul02d 9264  mul02i 9255
[Apostol] p. 18Theorem I.7mulcan 9659  mulcan2d 9656  mulcand 9655  mulcani 9661
[Apostol] p. 18Theorem I.8receu 9667  xreceu 24168
[Apostol] p. 18Theorem I.9divrec 9694  divrecd 9793  divreci 9759  divreczi 9752
[Apostol] p. 18Theorem I.10recrec 9711  recreci 9746
[Apostol] p. 18Theorem I.11mul0or 9662  mul0ord 9672  mul0ori 9670
[Apostol] p. 18Theorem I.12mul2neg 9473  mul2negd 9488  mul2negi 9481  mulneg1 9470  mulneg1d 9486  mulneg1i 9479
[Apostol] p. 18Theorem I.13divadddiv 9729  divadddivd 9834  divadddivi 9776
[Apostol] p. 18Theorem I.14divmuldiv 9714  divmuldivd 9831  divmuldivi 9774  rdivmuldivd 24227
[Apostol] p. 18Theorem I.15divdivdiv 9715  divdivdivd 9837  divdivdivi 9777
[Apostol] p. 20Axiom 7rpaddcl 10632  rpaddcld 10663  rpmulcl 10633  rpmulcld 10664
[Apostol] p. 20Axiom 8rpneg 10641
[Apostol] p. 20Axiom 90nrp 10642
[Apostol] p. 20Theorem I.17lttri 9199
[Apostol] p. 20Theorem I.18ltadd1d 9619  ltadd1dd 9637  ltadd1i 9581
[Apostol] p. 20Theorem I.19ltmul1 9860  ltmul1a 9859  ltmul1i 9929  ltmul1ii 9939  ltmul2 9861  ltmul2d 10686  ltmul2dd 10700  ltmul2i 9932
[Apostol] p. 20Theorem I.20msqgt0 9548  msqgt0d 9594  msqgt0i 9564
[Apostol] p. 20Theorem I.210lt1 9550
[Apostol] p. 20Theorem I.23lt0neg1 9534  lt0neg1d 9596  ltneg 9528  ltnegd 9604  ltnegi 9571
[Apostol] p. 20Theorem I.25lt2add 9513  lt2addd 9648  lt2addi 9589
[Apostol] p. 20Definition of positive numbersdf-rp 10613
[Apostol] p. 21Exercise 4recgt0 9854  recgt0d 9945  recgt0i 9915  recgt0ii 9916
[Apostol] p. 22Definition of integersdf-z 10283
[Apostol] p. 22Definition of positive integersdfnn3 10014
[Apostol] p. 22Definition of rationalsdf-q 10575
[Apostol] p. 24Theorem I.26supeu 7459
[Apostol] p. 26Theorem I.28nnunb 10217
[Apostol] p. 26Theorem I.29arch 10218
[Apostol] p. 28Exercise 2btwnz 10372
[Apostol] p. 28Exercise 3nnrecl 10219
[Apostol] p. 28Exercise 4rebtwnz 10573
[Apostol] p. 28Exercise 5zbtwnre 10572
[Apostol] p. 28Exercise 6qbtwnre 10785
[Apostol] p. 28Exercise 10(a)zneo 10352
[Apostol] p. 29Theorem I.35msqsqrd 12242  resqrth 12061  sqrth 12168  sqrthi 12174  sqsqrd 12241
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 10003
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10542
[Apostol] p. 361Remarkcrreczi 11504
[Apostol] p. 363Remarkabsgt0i 12202
[Apostol] p. 363Exampleabssubd 12255  abssubi 12206
[Baer] p. 40Property (b)mapdord 32436
[Baer] p. 40Property (c)mapd11 32437
[Baer] p. 40Property (e)mapdin 32460  mapdlsm 32462
[Baer] p. 40Property (f)mapd0 32463
[Baer] p. 40Definition of projectivitydf-mapd 32423  mapd1o 32446
[Baer] p. 41Property (g)mapdat 32465
[Baer] p. 44Part (1)mapdpg 32504
[Baer] p. 45Part (2)hdmap1eq 32600  mapdheq 32526  mapdheq2 32527  mapdheq2biN 32528
[Baer] p. 45Part (3)baerlem3 32511
[Baer] p. 46Part (4)mapdheq4 32530  mapdheq4lem 32529
[Baer] p. 46Part (5)baerlem5a 32512  baerlem5abmN 32516  baerlem5amN 32514  baerlem5b 32513  baerlem5bmN 32515
[Baer] p. 47Part (6)hdmap1l6 32620  hdmap1l6a 32608  hdmap1l6e 32613  hdmap1l6f 32614  hdmap1l6g 32615  hdmap1l6lem1 32606  hdmap1l6lem2 32607  hdmap1p6N 32621  mapdh6N 32545  mapdh6aN 32533  mapdh6eN 32538  mapdh6fN 32539  mapdh6gN 32540  mapdh6lem1N 32531  mapdh6lem2N 32532
[Baer] p. 48Part 9hdmapval 32629
[Baer] p. 48Part 10hdmap10 32641
[Baer] p. 48Part 11hdmapadd 32644
[Baer] p. 48Part (6)hdmap1l6h 32616  mapdh6hN 32541
[Baer] p. 48Part (7)mapdh75cN 32551  mapdh75d 32552  mapdh75e 32550  mapdh75fN 32553  mapdh7cN 32547  mapdh7dN 32548  mapdh7eN 32546  mapdh7fN 32549
[Baer] p. 48Part (8)mapdh8 32587  mapdh8a 32573  mapdh8aa 32574  mapdh8ab 32575  mapdh8ac 32576  mapdh8ad 32577  mapdh8b 32578  mapdh8c 32579  mapdh8d 32581  mapdh8d0N 32580  mapdh8e 32582  mapdh8fN 32583  mapdh8g 32584  mapdh8i 32585  mapdh8j 32586
[Baer] p. 48Part (9)mapdh9a 32588
[Baer] p. 48Equation 10mapdhvmap 32567
[Baer] p. 49Part 12hdmap11 32649  hdmapeq0 32645  hdmapf1oN 32666  hdmapneg 32647  hdmaprnN 32665  hdmaprnlem1N 32650  hdmaprnlem3N 32651  hdmaprnlem3uN 32652  hdmaprnlem4N 32654  hdmaprnlem6N 32655  hdmaprnlem7N 32656  hdmaprnlem8N 32657  hdmaprnlem9N 32658  hdmapsub 32648
[Baer] p. 49Part 14hdmap14lem1 32669  hdmap14lem10 32678  hdmap14lem1a 32667  hdmap14lem2N 32670  hdmap14lem2a 32668  hdmap14lem3 32671  hdmap14lem8 32676  hdmap14lem9 32677
[Baer] p. 50Part 14hdmap14lem11 32679  hdmap14lem12 32680  hdmap14lem13 32681  hdmap14lem14 32682  hdmap14lem15 32683  hgmapval 32688
[Baer] p. 50Part 15hgmapadd 32695  hgmapmul 32696  hgmaprnlem2N 32698  hgmapvs 32692
[Baer] p. 50Part 16hgmaprnN 32702
[Baer] p. 110Lemma 1hdmapip0com 32718
[Baer] p. 110Line 27hdmapinvlem1 32719
[Baer] p. 110Line 28hdmapinvlem2 32720
[Baer] p. 110Line 30hdmapinvlem3 32721
[Baer] p. 110Part 1.2hdmapglem5 32723  hgmapvv 32727
[Baer] p. 110Proposition 1hdmapinvlem4 32722
[Baer] p. 111Line 10hgmapvvlem1 32724
[Baer] p. 111Line 15hdmapg 32731  hdmapglem7 32730
[BellMachover] p. 36Lemma 10.3id1 21
[BellMachover] p. 97Definition 10.1df-eu 2285
[BellMachover] p. 460Notationdf-mo 2286
[BellMachover] p. 460Definitionmo3 2312
[BellMachover] p. 461Axiom Extax-ext 2417
[BellMachover] p. 462Theorem 1.1bm1.1 2421
[BellMachover] p. 463Axiom Repaxrep5 4325
[BellMachover] p. 463Scheme Sepaxsep 4329
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4333
[BellMachover] p. 466Axiom Powaxpow3 4380
[BellMachover] p. 466Axiom Unionaxun2 4703
[BellMachover] p. 468Definitiondf-ord 4584
[BellMachover] p. 469Theorem 2.2(i)ordirr 4599
[BellMachover] p. 469Theorem 2.2(iii)onelon 4606
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4601
[BellMachover] p. 471Definition of Ndf-om 4846
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4786
[BellMachover] p. 471Definition of Limdf-lim 4586
[BellMachover] p. 472Axiom Infzfinf2 7597
[BellMachover] p. 473Theorem 2.8limom 4860
[BellMachover] p. 477Equation 3.1df-r1 7690
[BellMachover] p. 478Definitionrankval2 7744
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7708  r1ord3g 7705
[BellMachover] p. 480Axiom Regzfreg2 7564
[BellMachover] p. 488Axiom ACac5 8357  dfac4 8003
[BellMachover] p. 490Definition of alephalephval3 7991
[BeltramettiCassinelli] p. 98Remarkatlatmstc 30117
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 23856
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 23898  chirredi 23897
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 23886
[Beran] p. 3Definition of joinsshjval3 22856
[Beran] p. 39Theorem 2.3(i)cmcm2 23118  cmcm2i 23095  cmcm2ii 23100  cmt2N 30048
[Beran] p. 40Theorem 2.3(iii)lecm 23119  lecmi 23104  lecmii 23105
[Beran] p. 45Theorem 3.4cmcmlem 23093
[Beran] p. 49Theorem 4.2cm2j 23122  cm2ji 23127  cm2mi 23128
[Beran] p. 95Definitiondf-sh 22709  issh2 22711
[Beran] p. 95Lemma 3.1(S5)his5 22588
[Beran] p. 95Lemma 3.1(S6)his6 22601
[Beran] p. 95Lemma 3.1(S7)his7 22592
[Beran] p. 95Lemma 3.2(S8)ho01i 23331
[Beran] p. 95Lemma 3.2(S9)hoeq1 23333
[Beran] p. 95Lemma 3.2(S10)ho02i 23332
[Beran] p. 95Lemma 3.2(S11)hoeq2 23334
[Beran] p. 95Postulate (S1)ax-his1 22584  his1i 22602
[Beran] p. 95Postulate (S2)ax-his2 22585
[Beran] p. 95Postulate (S3)ax-his3 22586
[Beran] p. 95Postulate (S4)ax-his4 22587
[Beran] p. 96Definition of normdf-hnorm 22471  dfhnorm2 22624  normval 22626
[Beran] p. 96Definition for Cauchy sequencehcau 22686
[Beran] p. 96Definition of Cauchy sequencedf-hcau 22476
[Beran] p. 96Definition of complete subspaceisch3 22744
[Beran] p. 96Definition of convergedf-hlim 22475  hlimi 22690
[Beran] p. 97Theorem 3.3(i)norm-i-i 22635  norm-i 22631
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 22639  norm-ii 22640  normlem0 22611  normlem1 22612  normlem2 22613  normlem3 22614  normlem4 22615  normlem5 22616  normlem6 22617  normlem7 22618  normlem7tALT 22621
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 22641  norm-iii 22642
[Beran] p. 98Remark 3.4bcs 22683  bcsiALT 22681  bcsiHIL 22682
[Beran] p. 98Remark 3.4(B)normlem9at 22623  normpar 22657  normpari 22656
[Beran] p. 98Remark 3.4(C)normpyc 22648  normpyth 22647  normpythi 22644
[Beran] p. 99Remarklnfn0 23550  lnfn0i 23545  lnop0 23469  lnop0i 23473
[Beran] p. 99Theorem 3.5(i)nmcexi 23529  nmcfnex 23556  nmcfnexi 23554  nmcopex 23532  nmcopexi 23530
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 23557  nmcfnlbi 23555  nmcoplb 23533  nmcoplbi 23531
[Beran] p. 99Theorem 3.5(iii)lnfncon 23559  lnfnconi 23558  lnopcon 23538  lnopconi 23537
[Beran] p. 100Lemma 3.6normpar2i 22658
[Beran] p. 101Lemma 3.6norm3adifi 22655  norm3adifii 22650  norm3dif 22652  norm3difi 22649
[Beran] p. 102Theorem 3.7(i)chocunii 22803  pjhth 22895  pjhtheu 22896  pjpjhth 22927  pjpjhthi 22928  pjth 19340
[Beran] p. 102Theorem 3.7(ii)ococ 22908  ococi 22907
[Beran] p. 103Remark 3.8nlelchi 23564
[Beran] p. 104Theorem 3.9riesz3i 23565  riesz4 23567  riesz4i 23566
[Beran] p. 104Theorem 3.10cnlnadj 23582  cnlnadjeu 23581  cnlnadjeui 23580  cnlnadji 23579  cnlnadjlem1 23570  nmopadjlei 23591
[Beran] p. 106Theorem 3.11(i)adjeq0 23594
[Beran] p. 106Theorem 3.11(v)nmopadji 23593
[Beran] p. 106Theorem 3.11(ii)adjmul 23595
[Beran] p. 106Theorem 3.11(iv)adjadj 23439
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 23605  nmopcoadji 23604
[Beran] p. 106Theorem 3.11(iii)adjadd 23596
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 23606
[Beran] p. 106Theorem 3.11(viii)adjcoi 23603  pjadj2coi 23707  pjadjcoi 23664
[Beran] p. 107Definitiondf-ch 22724  isch2 22726
[Beran] p. 107Remark 3.12choccl 22808  isch3 22744  occl 22806  ocsh 22785  shoccl 22807  shocsh 22786
[Beran] p. 107Remark 3.12(B)ococin 22910
[Beran] p. 108Theorem 3.13chintcl 22834
[Beran] p. 109Property (i)pjadj2 23690  pjadj3 23691  pjadji 23187  pjadjii 23176
[Beran] p. 109Property (ii)pjidmco 23684  pjidmcoi 23680  pjidmi 23175
[Beran] p. 110Definition of projector orderingpjordi 23676
[Beran] p. 111Remarkho0val 23253  pjch1 23172
[Beran] p. 111Definitiondf-hfmul 23237  df-hfsum 23236  df-hodif 23235  df-homul 23234  df-hosum 23233
[Beran] p. 111Lemma 4.4(i)pjo 23173
[Beran] p. 111Lemma 4.4(ii)pjch 23196  pjchi 22934
[Beran] p. 111Lemma 4.4(iii)pjoc2 22941  pjoc2i 22940
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 23182
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 23668  pjssmii 23183
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 23667
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 23666
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 23671
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 23669  pjssge0ii 23184
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 23670  pjdifnormii 23185
[Bogachev] p. 116Definition 2.3.1df-itgm 24664  df-sitm 24646
[Bogachev] p. 118Chapter 2.4.4df-itgm 24664
[Bogachev] p. 118Definition 2.4.1df-sitg 24645
[Bollobas] p. 4Definitiondf-wlk 21516
[Bollobas] p. 5Notationdf-pth 21518
[Bollobas] p. 5Definitiondf-crct 21520  df-cycl 21521  df-trail 21517  df-wlkon 21522
[BourbakiEns] p. Proposition 8fcof1 6020  fcofo 6021
[BourbakiTop1] p. Remarkxnegmnf 10796  xnegpnf 10795
[BourbakiTop1] p. Remark rexneg 10797
[BourbakiTop1] p. Theoremneiss 17173
[BourbakiTop1] p. Remark 3ust0 18249  ustfilxp 18242
[BourbakiTop1] p. Axiom GT'tgpsubcn 18120
[BourbakiTop1] p. Example 1cstucnd 18314  iducn 18313  snfil 17896
[BourbakiTop1] p. Example 2neifil 17912
[BourbakiTop1] p. Theorem 1cnextcn 18098
[BourbakiTop1] p. Theorem 2ucnextcn 18334
[BourbakiTop1] p. Theorem 3df-hcmp 24341
[BourbakiTop1] p. Definitionistgp 18107
[BourbakiTop1] p. Propositioncnpco 17331  ishmeo 17791  neips 17177
[BourbakiTop1] p. Definition 1df-ucn 18306  df-ust 18230  filintn0 17893  ucnprima 18312
[BourbakiTop1] p. Definition 2df-cfilu 18317
[BourbakiTop1] p. Definition 3df-cusp 18328  df-usp 18287  df-utop 18261  trust 18259
[BourbakiTop1] p. Condition F_Iustssel 18235
[BourbakiTop1] p. Condition U_Iustdiag 18238
[BourbakiTop1] p. Property V_ivneiptopreu 17197
[BourbakiTop1] p. Proposition 1ucncn 18315  ustund 18251  ustuqtop 18276
[BourbakiTop1] p. Proposition 2neiptopreu 17197  utop2nei 18280  utop3cls 18281
[BourbakiTop1] p. Proposition 3fmucnd 18322  uspreg 18304  utopreg 18282
[BourbakiTop1] p. Proposition 4imasncld 17723  imasncls 17724  imasnopn 17722
[BourbakiTop1] p. Proposition 9cnpflf2 18032
[BourbakiTop1] p. Theorem 1 (d)iscncl 17333
[BourbakiTop1] p. Condition F_IIustincl 18237
[BourbakiTop1] p. Condition U_IIustinvel 18239
[BourbakiTop1] p. Proposition 11cnextucn 18333
[BourbakiTop1] p. Proposition Vissnei2 17180
[BourbakiTop1] p. Condition F_IIbustbasel 18236
[BourbakiTop1] p. Condition U_IIIustexhalf 18240
[BourbakiTop1] p. Definition C'''df-cmp 17450
[BourbakiTop1] p. Proposition Viiinnei 17189
[BourbakiTop1] p. Proposition Vivneissex 17191
[BourbakiTop1] p. Proposition Viiielnei 17175  ssnei 17174
[BourbakiTop1] p. Remark below def. 1filn0 17894
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17878
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17895
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 27787
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27789  stoweid 27788
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27726  stoweidlem10 27735  stoweidlem14 27739  stoweidlem15 27740  stoweidlem35 27760  stoweidlem36 27761  stoweidlem37 27762  stoweidlem38 27763  stoweidlem40 27765  stoweidlem41 27766  stoweidlem43 27768  stoweidlem44 27769  stoweidlem46 27771  stoweidlem5 27730  stoweidlem50 27775  stoweidlem52 27777  stoweidlem53 27778  stoweidlem55 27780  stoweidlem56 27781
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27748  stoweidlem24 27749  stoweidlem27 27752  stoweidlem28 27753  stoweidlem30 27755
[BrosowskiDeutsh] p. 91Proofstoweidlem34 27759  stoweidlem59 27784  stoweidlem60 27785
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27770  stoweidlem49 27774  stoweidlem7 27732
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27756  stoweidlem39 27764  stoweidlem42 27767  stoweidlem48 27773  stoweidlem51 27776  stoweidlem54 27779  stoweidlem57 27782  stoweidlem58 27783
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27750
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27742
[BrosowskiDeutsh] p. 92Proofstoweidlem11 27736  stoweidlem13 27738  stoweidlem26 27751  stoweidlem61 27786
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27743
[ChoquetDD] p. 2Definition of mappingdf-mpt 4268
[Clemente] p. 10Definition ITnatded 21711
[Clemente] p. 10Definition I` `m,nnatded 21711
[Clemente] p. 11Definition E=>m,nnatded 21711
[Clemente] p. 11Definition I=>m,nnatded 21711
[Clemente] p. 11Definition E` `(1)natded 21711
[Clemente] p. 11Definition E` `(2)natded 21711
[Clemente] p. 12Definition E` `m,n,pnatded 21711
[Clemente] p. 12Definition I` `n(1)natded 21711
[Clemente] p. 12Definition I` `n(2)natded 21711
[Clemente] p. 13Definition I` `m,n,pnatded 21711
[Clemente] p. 14Proof 5.11natded 21711
[Clemente] p. 14Definition E` `nnatded 21711
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 21713  ex-natded5.2 21712
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 21716  ex-natded5.3 21715
[Clemente] p. 18Theorem 5.5ex-natded5.5 21718
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 21720  ex-natded5.7 21719
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 21722  ex-natded5.8 21721
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 21724  ex-natded5.13 21723
[Clemente] p. 32Definition I` `nnatded 21711
[Clemente] p. 32Definition E` `m,n,p,anatded 21711
[Clemente] p. 32Definition E` `n,tnatded 21711
[Clemente] p. 32Definition I` `n,tnatded 21711
[Clemente] p. 43Theorem 9.20ex-natded9.20 21725
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 21726
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 21728  ex-natded9.26 21727
[Cohen] p. 301Remarkrelogoprlem 20485
[Cohen] p. 301Property 2relogmul 20486  relogmuld 20520
[Cohen] p. 301Property 3relogdiv 20487  relogdivd 20521
[Cohen] p. 301Property 4relogexp 20490
[Cohen] p. 301Property 1alog1 20480
[Cohen] p. 301Property 1bloge 20481
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 24635  sxbrsigalem4 24637
[Cohn] p. 81Section II.5acsdomd 14607  acsinfd 14606  acsinfdimd 14608  acsmap2d 14605  acsmapd 14604
[Cohn] p. 143Example 5.1.1sxbrsiga 24640
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 11242
[Crawley] p. 1Definition of posetdf-poset 14403
[Crawley] p. 107Theorem 13.2hlsupr 30183
[Crawley] p. 110Theorem 13.3arglem1N 30987  dalaw 30683
[Crawley] p. 111Theorem 13.4hlathil 32762
[Crawley] p. 111Definition of set Wdf-watsN 30787
[Crawley] p. 111Definition of dilationdf-dilN 30903  df-ldil 30901  isldil 30907
[Crawley] p. 111Definition of translationdf-ltrn 30902  df-trnN 30904  isltrn 30916  ltrnu 30918
[Crawley] p. 112Lemma Acdlema1N 30588  cdlema2N 30589  exatleN 30201
[Crawley] p. 112Lemma B1cvrat 30273  cdlemb 30591  cdlemb2 30838  cdlemb3 31403  idltrn 30947  l1cvat 29853  lhpat 30840  lhpat2 30842  lshpat 29854  ltrnel 30936  ltrnmw 30948
[Crawley] p. 112Lemma Ccdlemc1 30988  cdlemc2 30989  ltrnnidn 30971  trlat 30966  trljat1 30963  trljat2 30964  trljat3 30965  trlne 30982  trlnidat 30970  trlnle 30983
[Crawley] p. 112Definition of automorphismdf-pautN 30788
[Crawley] p. 113Lemma Ccdlemc 30994  cdlemc3 30990  cdlemc4 30991
[Crawley] p. 113Lemma Dcdlemd 31004  cdlemd1 30995  cdlemd2 30996  cdlemd3 30997  cdlemd4 30998  cdlemd5 30999  cdlemd6 31000  cdlemd7 31001  cdlemd8 31002  cdlemd9 31003  cdleme31sde 31182  cdleme31se 31179  cdleme31se2 31180  cdleme31snd 31183  cdleme32a 31238  cdleme32b 31239  cdleme32c 31240  cdleme32d 31241  cdleme32e 31242  cdleme32f 31243  cdleme32fva 31234  cdleme32fva1 31235  cdleme32fvcl 31237  cdleme32le 31244  cdleme48fv 31296  cdleme4gfv 31304  cdleme50eq 31338  cdleme50f 31339  cdleme50f1 31340  cdleme50f1o 31343  cdleme50laut 31344  cdleme50ldil 31345  cdleme50lebi 31337  cdleme50rn 31342  cdleme50rnlem 31341  cdlemeg49le 31308  cdlemeg49lebilem 31336
[Crawley] p. 113Lemma Ecdleme 31357  cdleme00a 31006  cdleme01N 31018  cdleme02N 31019  cdleme0a 31008  cdleme0aa 31007  cdleme0b 31009  cdleme0c 31010  cdleme0cp 31011  cdleme0cq 31012  cdleme0dN 31013  cdleme0e 31014  cdleme0ex1N 31020  cdleme0ex2N 31021  cdleme0fN 31015  cdleme0gN 31016  cdleme0moN 31022  cdleme1 31024  cdleme10 31051  cdleme10tN 31055  cdleme11 31067  cdleme11a 31057  cdleme11c 31058  cdleme11dN 31059  cdleme11e 31060  cdleme11fN 31061  cdleme11g 31062  cdleme11h 31063  cdleme11j 31064  cdleme11k 31065  cdleme11l 31066  cdleme12 31068  cdleme13 31069  cdleme14 31070  cdleme15 31075  cdleme15a 31071  cdleme15b 31072  cdleme15c 31073  cdleme15d 31074  cdleme16 31082  cdleme16aN 31056  cdleme16b 31076  cdleme16c 31077  cdleme16d 31078  cdleme16e 31079  cdleme16f 31080  cdleme16g 31081  cdleme19a 31100  cdleme19b 31101  cdleme19c 31102  cdleme19d 31103  cdleme19e 31104  cdleme19f 31105  cdleme1b 31023  cdleme2 31025  cdleme20aN 31106  cdleme20bN 31107  cdleme20c 31108  cdleme20d 31109  cdleme20e 31110  cdleme20f 31111  cdleme20g 31112  cdleme20h 31113  cdleme20i 31114  cdleme20j 31115  cdleme20k 31116  cdleme20l 31119  cdleme20l1 31117  cdleme20l2 31118  cdleme20m 31120  cdleme20y 31099  cdleme20zN 31098  cdleme21 31134  cdleme21d 31127  cdleme21e 31128  cdleme22a 31137  cdleme22aa 31136  cdleme22b 31138  cdleme22cN 31139  cdleme22d 31140  cdleme22e 31141  cdleme22eALTN 31142  cdleme22f 31143  cdleme22f2 31144  cdleme22g 31145  cdleme23a 31146  cdleme23b 31147  cdleme23c 31148  cdleme26e 31156  cdleme26eALTN 31158  cdleme26ee 31157  cdleme26f 31160  cdleme26f2 31162  cdleme26f2ALTN 31161  cdleme26fALTN 31159  cdleme27N 31166  cdleme27a 31164  cdleme27cl 31163  cdleme28c 31169  cdleme3 31034  cdleme30a 31175  cdleme31fv 31187  cdleme31fv1 31188  cdleme31fv1s 31189  cdleme31fv2 31190  cdleme31id 31191  cdleme31sc 31181  cdleme31sdnN 31184  cdleme31sn 31177  cdleme31sn1 31178  cdleme31sn1c 31185  cdleme31sn2 31186  cdleme31so 31176  cdleme35a 31245  cdleme35b 31247  cdleme35c 31248  cdleme35d 31249  cdleme35e 31250  cdleme35f 31251  cdleme35fnpq 31246  cdleme35g 31252  cdleme35h 31253  cdleme35h2 31254  cdleme35sn2aw 31255  cdleme35sn3a 31256  cdleme36a 31257  cdleme36m 31258  cdleme37m 31259  cdleme38m 31260  cdleme38n 31261  cdleme39a 31262  cdleme39n 31263  cdleme3b 31026  cdleme3c 31027  cdleme3d 31028  cdleme3e 31029  cdleme3fN 31030  cdleme3fa 31033  cdleme3g 31031  cdleme3h 31032  cdleme4 31035  cdleme40m 31264  cdleme40n 31265  cdleme40v 31266  cdleme40w 31267  cdleme41fva11 31274  cdleme41sn3aw 31271  cdleme41sn4aw 31272  cdleme41snaw 31273  cdleme42a 31268  cdleme42b 31275  cdleme42c 31269  cdleme42d 31270  cdleme42e 31276  cdleme42f 31277  cdleme42g 31278  cdleme42h 31279  cdleme42i 31280  cdleme42k 31281  cdleme42ke 31282  cdleme42keg 31283  cdleme42mN 31284  cdleme42mgN 31285  cdleme43aN 31286  cdleme43bN 31287  cdleme43cN 31288  cdleme43dN 31289  cdleme5 31037  cdleme50ex 31356  cdleme50ltrn 31354  cdleme51finvN 31353  cdleme51finvfvN 31352  cdleme51finvtrN 31355  cdleme6 31038  cdleme7 31046  cdleme7a 31040  cdleme7aa 31039  cdleme7b 31041  cdleme7c 31042  cdleme7d 31043  cdleme7e 31044  cdleme7ga 31045  cdleme8 31047  cdleme8tN 31052  cdleme9 31050  cdleme9a 31048  cdleme9b 31049  cdleme9tN 31054  cdleme9taN 31053  cdlemeda 31095  cdlemedb 31094  cdlemednpq 31096  cdlemednuN 31097  cdlemefr27cl 31200  cdlemefr32fva1 31207  cdlemefr32fvaN 31206  cdlemefrs32fva 31197  cdlemefrs32fva1 31198  cdlemefs27cl 31210  cdlemefs32fva1 31220  cdlemefs32fvaN 31219  cdlemesner 31093  cdlemeulpq 31017
[Crawley] p. 114Lemma E4atex 30873  4atexlem7 30872  cdleme0nex 31087  cdleme17a 31083  cdleme17c 31085  cdleme17d 31295  cdleme17d1 31086  cdleme17d2 31292  cdleme18a 31088  cdleme18b 31089  cdleme18c 31090  cdleme18d 31092  cdleme4a 31036
[Crawley] p. 115Lemma Ecdleme21a 31122  cdleme21at 31125  cdleme21b 31123  cdleme21c 31124  cdleme21ct 31126  cdleme21f 31129  cdleme21g 31130  cdleme21h 31131  cdleme21i 31132  cdleme22gb 31091
[Crawley] p. 116Lemma Fcdlemf 31360  cdlemf1 31358  cdlemf2 31359
[Crawley] p. 116Lemma Gcdlemftr1 31364  cdlemg16 31454  cdlemg28 31501  cdlemg28a 31490  cdlemg28b 31500  cdlemg3a 31394  cdlemg42 31526  cdlemg43 31527  cdlemg44 31530  cdlemg44a 31528  cdlemg46 31532  cdlemg47 31533  cdlemg9 31431  ltrnco 31516  ltrncom 31535  tgrpabl 31548  trlco 31524
[Crawley] p. 116Definition of Gdf-tgrp 31540
[Crawley] p. 117Lemma Gcdlemg17 31474  cdlemg17b 31459
[Crawley] p. 117Definition of Edf-edring-rN 31553  df-edring 31554
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 31557
[Crawley] p. 118Remarktendopltp 31577
[Crawley] p. 118Lemma Hcdlemh 31614  cdlemh1 31612  cdlemh2 31613
[Crawley] p. 118Lemma Icdlemi 31617  cdlemi1 31615  cdlemi2 31616
[Crawley] p. 118Lemma Jcdlemj1 31618  cdlemj2 31619  cdlemj3 31620  tendocan 31621
[Crawley] p. 118Lemma Kcdlemk 31771  cdlemk1 31628  cdlemk10 31640  cdlemk11 31646  cdlemk11t 31743  cdlemk11ta 31726  cdlemk11tb 31728  cdlemk11tc 31742  cdlemk11u-2N 31686  cdlemk11u 31668  cdlemk12 31647  cdlemk12u-2N 31687  cdlemk12u 31669  cdlemk13-2N 31673  cdlemk13 31649  cdlemk14-2N 31675  cdlemk14 31651  cdlemk15-2N 31676  cdlemk15 31652  cdlemk16-2N 31677  cdlemk16 31654  cdlemk16a 31653  cdlemk17-2N 31678  cdlemk17 31655  cdlemk18-2N 31683  cdlemk18-3N 31697  cdlemk18 31665  cdlemk19-2N 31684  cdlemk19 31666  cdlemk19u 31767  cdlemk1u 31656  cdlemk2 31629  cdlemk20-2N 31689  cdlemk20 31671  cdlemk21-2N 31688  cdlemk21N 31670  cdlemk22-3 31698  cdlemk22 31690  cdlemk23-3 31699  cdlemk24-3 31700  cdlemk25-3 31701  cdlemk26-3 31703  cdlemk26b-3 31702  cdlemk27-3 31704  cdlemk28-3 31705  cdlemk29-3 31708  cdlemk3 31630  cdlemk30 31691  cdlemk31 31693  cdlemk32 31694  cdlemk33N 31706  cdlemk34 31707  cdlemk35 31709  cdlemk36 31710  cdlemk37 31711  cdlemk38 31712  cdlemk39 31713  cdlemk39u 31765  cdlemk4 31631  cdlemk41 31717  cdlemk42 31738  cdlemk42yN 31741  cdlemk43N 31760  cdlemk45 31744  cdlemk46 31745  cdlemk47 31746  cdlemk48 31747  cdlemk49 31748  cdlemk5 31633  cdlemk50 31749  cdlemk51 31750  cdlemk52 31751  cdlemk53 31754  cdlemk54 31755  cdlemk55 31758  cdlemk55u 31763  cdlemk56 31768  cdlemk5a 31632  cdlemk5auN 31657  cdlemk5u 31658  cdlemk6 31634  cdlemk6u 31659  cdlemk7 31645  cdlemk7u-2N 31685  cdlemk7u 31667  cdlemk8 31635  cdlemk9 31636  cdlemk9bN 31637  cdlemki 31638  cdlemkid 31733  cdlemkj-2N 31679  cdlemkj 31660  cdlemksat 31643  cdlemksel 31642  cdlemksv 31641  cdlemksv2 31644  cdlemkuat 31663  cdlemkuel-2N 31681  cdlemkuel-3 31695  cdlemkuel 31662  cdlemkuv-2N 31680  cdlemkuv2-2 31682  cdlemkuv2-3N 31696  cdlemkuv2 31664  cdlemkuvN 31661  cdlemkvcl 31639  cdlemky 31723  cdlemkyyN 31759  tendoex 31772
[Crawley] p. 120Remarkdva1dim 31782
[Crawley] p. 120Lemma Lcdleml1N 31773  cdleml2N 31774  cdleml3N 31775  cdleml4N 31776  cdleml5N 31777  cdleml6 31778  cdleml7 31779  cdleml8 31780  cdleml9 31781  dia1dim 31859
[Crawley] p. 120Lemma Mdia11N 31846  diaf11N 31847  dialss 31844  diaord 31845  dibf11N 31959  djajN 31935
[Crawley] p. 120Definition of isomorphism mapdiaval 31830
[Crawley] p. 121Lemma Mcdlemm10N 31916  dia2dimlem1 31862  dia2dimlem2 31863  dia2dimlem3 31864  dia2dimlem4 31865  dia2dimlem5 31866  diaf1oN 31928  diarnN 31927  dvheveccl 31910  dvhopN 31914
[Crawley] p. 121Lemma Ncdlemn 32010  cdlemn10 32004  cdlemn11 32009  cdlemn11a 32005  cdlemn11b 32006  cdlemn11c 32007  cdlemn11pre 32008  cdlemn2 31993  cdlemn2a 31994  cdlemn3 31995  cdlemn4 31996  cdlemn4a 31997  cdlemn5 31999  cdlemn5pre 31998  cdlemn6 32000  cdlemn7 32001  cdlemn8 32002  cdlemn9 32003  diclspsn 31992
[Crawley] p. 121Definition of phi(q)df-dic 31971
[Crawley] p. 122Lemma Ndih11 32063  dihf11 32065  dihjust 32015  dihjustlem 32014  dihord 32062  dihord1 32016  dihord10 32021  dihord11b 32020  dihord11c 32022  dihord2 32025  dihord2a 32017  dihord2b 32018  dihord2cN 32019  dihord2pre 32023  dihord2pre2 32024  dihordlem6 32011  dihordlem7 32012  dihordlem7b 32013
[Crawley] p. 122Definition of isomorphism mapdihffval 32028  dihfval 32029  dihval 32030
[Eisenberg] p. 67Definition 5.3df-dif 3323
[Eisenberg] p. 82Definition 6.3dfom3 7602
[Eisenberg] p. 125Definition 8.21df-map 7020
[Eisenberg] p. 216Example 13.2(4)omenps 7609
[Eisenberg] p. 310Theorem 19.8cardprc 7867
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8430
[Enderton] p. 18Axiom of Empty Setaxnul 4337
[Enderton] p. 19Definitiondf-tp 3822
[Enderton] p. 26Exercise 5unissb 4045
[Enderton] p. 26Exercise 10pwel 4415
[Enderton] p. 28Exercise 7(b)pwun 4491
[Enderton] p. 30Theorem "Distributive laws"iinin1 4162  iinin2 4161  iinun2 4157  iunin1 4156  iunin2 4155
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4160  iundif2 4158
[Enderton] p. 32Exercise 20unineq 3591
[Enderton] p. 33Exercise 23iinuni 4174
[Enderton] p. 33Exercise 25iununi 4175
[Enderton] p. 33Exercise 24(a)iinpw 4179
[Enderton] p. 33Exercise 24(b)iunpw 4759  iunpwss 4180
[Enderton] p. 36Definitionopthwiener 4458
[Enderton] p. 38Exercise 6(a)unipw 4414
[Enderton] p. 38Exercise 6(b)pwuni 4395
[Enderton] p. 41Lemma 3Dopeluu 4715  rnex 5133  rnexg 5131
[Enderton] p. 41Exercise 8dmuni 5079  rnuni 5283
[Enderton] p. 42Definition of a functiondffun7 5479  dffun8 5480
[Enderton] p. 43Definition of function valuefunfv2 5791
[Enderton] p. 43Definition of single-rootedfuncnv 5511
[Enderton] p. 44Definition (d)dfima2 5205  dfima3 5206
[Enderton] p. 47Theorem 3Hfvco2 5798
[Enderton] p. 49Axiom of Choice (first form)ac7 8353  ac7g 8354  df-ac 7997  dfac2 8011  dfac2a 8010  dfac3 8002  dfac7 8012
[Enderton] p. 50Theorem 3K(a)imauni 5993
[Enderton] p. 52Definitiondf-map 7020
[Enderton] p. 53Exercise 21coass 5388
[Enderton] p. 53Exercise 27dmco 5378
[Enderton] p. 53Exercise 14(a)funin 5520
[Enderton] p. 53Exercise 22(a)imass2 5240
[Enderton] p. 54Remarkixpf 7084  ixpssmap 7096
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7064
[Enderton] p. 55Axiom of Choice (second form)ac9 8363  ac9s 8373
[Enderton] p. 56Theorem 3Merref 6925
[Enderton] p. 57Lemma 3Nerthi 6951
[Enderton] p. 57Definitiondf-ec 6907
[Enderton] p. 58Definitiondf-qs 6911
[Enderton] p. 60Theorem 3Qth3q 7013  th3qcor 7012  th3qlem1 7010  th3qlem2 7011
[Enderton] p. 61Exercise 35df-ec 6907
[Enderton] p. 65Exercise 56(a)dmun 5076
[Enderton] p. 68Definition of successordf-suc 4587
[Enderton] p. 71Definitiondf-tr 4303  dftr4 4307
[Enderton] p. 72Theorem 4Eunisuc 4657
[Enderton] p. 73Exercise 6unisuc 4657
[Enderton] p. 73Exercise 5(a)truni 4316
[Enderton] p. 73Exercise 5(b)trint 4317  trintALT 28993
[Enderton] p. 79Theorem 4I(A1)nna0 6847
[Enderton] p. 79Theorem 4I(A2)nnasuc 6849  onasuc 6772
[Enderton] p. 79Definition of operation valuedf-ov 6084
[Enderton] p. 80Theorem 4J(A1)nnm0 6848
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6850  onmsuc 6773
[Enderton] p. 81Theorem 4K(1)nnaass 6865
[Enderton] p. 81Theorem 4K(2)nna0r 6852  nnacom 6860
[Enderton] p. 81Theorem 4K(3)nndi 6866
[Enderton] p. 81Theorem 4K(4)nnmass 6867
[Enderton] p. 81Theorem 4K(5)nnmcom 6869
[Enderton] p. 82Exercise 16nnm0r 6853  nnmsucr 6868
[Enderton] p. 88Exercise 23nnaordex 6881
[Enderton] p. 129Definitiondf-en 7110
[Enderton] p. 132Theorem 6B(b)canth 6539
[Enderton] p. 133Exercise 1xpomen 7897
[Enderton] p. 133Exercise 2qnnen 12813
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7291
[Enderton] p. 135Corollary 6Cphp3 7293
[Enderton] p. 136Corollary 6Enneneq 7290
[Enderton] p. 136Corollary 6D(a)pssinf 7319
[Enderton] p. 136Corollary 6D(b)ominf 7321
[Enderton] p. 137Lemma 6Fpssnn 7327
[Enderton] p. 138Corollary 6Gssfi 7329
[Enderton] p. 139Theorem 6H(c)mapen 7271
[Enderton] p. 142Theorem 6I(3)xpcdaen 8063
[Enderton] p. 142Theorem 6I(4)mapcdaen 8064
[Enderton] p. 143Theorem 6Jcda0en 8059  cda1en 8055
[Enderton] p. 144Exercise 13iunfi 7394  unifi 7395  unifi2 7396
[Enderton] p. 144Corollary 6Kundif2 3704  unfi 7374  unfi2 7376
[Enderton] p. 145Figure 38ffoss 5707
[Enderton] p. 145Definitiondf-dom 7111
[Enderton] p. 146Example 1domen 7121  domeng 7122
[Enderton] p. 146Example 3nndomo 7300  nnsdom 7608  nnsdomg 7366
[Enderton] p. 149Theorem 6L(a)cdadom2 8067
[Enderton] p. 149Theorem 6L(c)mapdom1 7272  xpdom1 7207  xpdom1g 7205  xpdom2g 7204
[Enderton] p. 149Theorem 6L(d)mapdom2 7278
[Enderton] p. 151Theorem 6Mzorn 8387  zorng 8384
[Enderton] p. 151Theorem 6M(4)ac8 8372  dfac5 8009
[Enderton] p. 159Theorem 6Qunictb 8450
[Enderton] p. 164Exampleinfdif 8089
[Enderton] p. 168Definitiondf-po 4503
[Enderton] p. 192Theorem 7M(a)oneli 4689
[Enderton] p. 192Theorem 7M(b)ontr1 4627
[Enderton] p. 192Theorem 7M(c)onirri 4688
[Enderton] p. 193Corollary 7N(b)0elon 4634
[Enderton] p. 193Corollary 7N(c)onsuci 4818
[Enderton] p. 193Corollary 7N(d)ssonunii 4768
[Enderton] p. 194Remarkonprc 4765
[Enderton] p. 194Exercise 16suc11 4685
[Enderton] p. 197Definitiondf-card 7826
[Enderton] p. 197Theorem 7Pcarden 8426
[Enderton] p. 200Exercise 25tfis 4834
[Enderton] p. 202Lemma 7Tr1tr 7702
[Enderton] p. 202Definitiondf-r1 7690
[Enderton] p. 202Theorem 7Qr1val1 7712
[Enderton] p. 204Theorem 7V(b)rankval4 7793
[Enderton] p. 206Theorem 7X(b)en2lp 7571
[Enderton] p. 207Exercise 30rankpr 7783  rankprb 7777  rankpw 7769  rankpwi 7749  rankuniss 7792
[Enderton] p. 207Exercise 34opthreg 7573
[Enderton] p. 208Exercise 35suc11reg 7574
[Enderton] p. 212Definition of alephalephval3 7991
[Enderton] p. 213Theorem 8A(a)alephord2 7957
[Enderton] p. 213Theorem 8A(b)cardalephex 7971
[Enderton] p. 218Theorem Schema 8Eonfununi 6603
[Enderton] p. 222Definition of kardkarden 7819  kardex 7818
[Enderton] p. 238Theorem 8Roeoa 6840
[Enderton] p. 238Theorem 8Soeoe 6842
[Enderton] p. 240Exercise 25oarec 6805
[Enderton] p. 257Definition of cofinalitycflm 8130
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13867
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13813
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14603  mrieqv2d 13864  mrieqvd 13863
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13868
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13873  mreexexlem2d 13870
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14609  mreexfidimd 13875
[Fremlin5] p. 193Proposition 563Gbnulmbl2 19431
[Fremlin5] p. 213Lemma 565Cauniioovol 19471
[Fremlin5] p. 214Lemma 565Cauniioombl 19481
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 26285
[Fremlin5] p. 220Theorem 565Maftc1anc 26288
[FreydScedrov] p. 283Axiom of Infinityax-inf 7593  inf1 7577  inf2 7578
[Gleason] p. 117Proposition 9-2.1df-enq 8788  enqer 8798
[Gleason] p. 117Proposition 9-2.2df-1nq 8793  df-nq 8789
[Gleason] p. 117Proposition 9-2.3df-plpq 8785  df-plq 8791
[Gleason] p. 119Proposition 9-2.4caovmo 6284  df-mpq 8786  df-mq 8792
[Gleason] p. 119Proposition 9-2.5df-rq 8794
[Gleason] p. 119Proposition 9-2.6ltexnq 8852
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8853  ltbtwnnq 8855
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8848
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8849
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8856
[Gleason] p. 121Definition 9-3.1df-np 8858
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8870
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8872
[Gleason] p. 122Definitiondf-1p 8859
[Gleason] p. 122Remark (1)prub 8871
[Gleason] p. 122Lemma 9-3.4prlem934 8910
[Gleason] p. 122Proposition 9-3.2df-ltp 8862
[Gleason] p. 122Proposition 9-3.3ltsopr 8909  psslinpr 8908  supexpr 8931  suplem1pr 8929  suplem2pr 8930
[Gleason] p. 123Proposition 9-3.5addclpr 8895  addclprlem1 8893  addclprlem2 8894  df-plp 8860
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8899
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8898
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8911
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8920  ltexprlem1 8913  ltexprlem2 8914  ltexprlem3 8915  ltexprlem4 8916  ltexprlem5 8917  ltexprlem6 8918  ltexprlem7 8919
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8922  ltaprlem 8921
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8923
[Gleason] p. 124Lemma 9-3.6prlem936 8924
[Gleason] p. 124Proposition 9-3.7df-mp 8861  mulclpr 8897  mulclprlem 8896  reclem2pr 8925
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8906
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8901
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8900
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8905
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8928  reclem3pr 8926  reclem4pr 8927
[Gleason] p. 126Proposition 9-4.1df-enr 8934  df-mpr 8933  df-plpr 8932  enrer 8943
[Gleason] p. 126Proposition 9-4.2df-0r 8939  df-1r 8940  df-nr 8935
[Gleason] p. 126Proposition 9-4.3df-mr 8937  df-plr 8936  negexsr 8977  recexsr 8982  recexsrlem 8978
[Gleason] p. 127Proposition 9-4.4df-ltr 8938
[Gleason] p. 130Proposition 10-1.3creui 9995  creur 9994  cru 9992
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 9063  axcnre 9039
[Gleason] p. 132Definition 10-3.1crim 11920  crimd 12037  crimi 11998  crre 11919  crred 12036  crrei 11997
[Gleason] p. 132Definition 10-3.2remim 11922  remimd 12003
[Gleason] p. 133Definition 10.36absval2 12089  absval2d 12247  absval2i 12200
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11946  cjaddd 12025  cjaddi 11993
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11947  cjmuld 12026  cjmuli 11994
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11945  cjcjd 12004  cjcji 11976
[Gleason] p. 133Proposition 10-3.4(f)cjre 11944  cjreb 11928  cjrebd 12007  cjrebi 11979  cjred 12031  rere 11927  rereb 11925  rerebd 12006  rerebi 11978  rered 12029
[Gleason] p. 133Proposition 10-3.4(h)addcj 11953  addcjd 12017  addcji 11988
[Gleason] p. 133Proposition 10-3.7(a)absval 12043
[Gleason] p. 133Proposition 10-3.7(b)abscj 12084  abscjd 12252  abscji 12204
[Gleason] p. 133Proposition 10-3.7(c)abs00 12094  abs00d 12248  abs00i 12201  absne0d 12249
[Gleason] p. 133Proposition 10-3.7(d)releabs 12125  releabsd 12253  releabsi 12205
[Gleason] p. 133Proposition 10-3.7(f)absmul 12099  absmuld 12256  absmuli 12207
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 12087  sqabsaddi 12208
[Gleason] p. 133Proposition 10-3.7(h)abstri 12134  abstrid 12258  abstrii 12211
[Gleason] p. 134Definition 10-4.1df-exp 11383  exp0 11386  expp1 11388  expp1d 11524
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20570  cxpaddd 20608  expadd 11422  expaddd 11525  expaddz 11424
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20579  cxpmuld 20625  expmul 11425  expmuld 11526  expmulz 11426
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20576  mulcxpd 20619  mulexp 11419  mulexpd 11538  mulexpz 11420
[Gleason] p. 140Exercise 1znnen 12812
[Gleason] p. 141Definition 11-2.1fzval 11045
[Gleason] p. 168Proposition 12-2.1(a)climadd 12425  rlimadd 12436  rlimdiv 12439
[Gleason] p. 168Proposition 12-2.1(b)climsub 12427  rlimsub 12437
[Gleason] p. 168Proposition 12-2.1(c)climmul 12426  rlimmul 12438
[Gleason] p. 171Corollary 12-2.2climmulc2 12430
[Gleason] p. 172Corollary 12-2.5climrecl 12377
[Gleason] p. 172Proposition 12-2.4(c)climabs 12397  climcj 12398  climim 12400  climre 12399  rlimabs 12402  rlimcj 12403  rlimim 12405  rlimre 12404
[Gleason] p. 173Definition 12-3.1df-ltxr 9125  df-xr 9124  ltxr 10715
[Gleason] p. 175Definition 12-4.1df-limsup 12265  limsupval 12268
[Gleason] p. 180Theorem 12-5.1climsup 12463
[Gleason] p. 180Theorem 12-5.3caucvg 12472  caucvgb 12473  caucvgr 12469  climcau 12464
[Gleason] p. 182Exercise 3cvgcmp 12595
[Gleason] p. 182Exercise 4cvgrat 12660
[Gleason] p. 195Theorem 13-2.12abs1m 12139
[Gleason] p. 217Lemma 13-4.1btwnzge0 11230
[Gleason] p. 223Definition 14-1.1df-met 16696
[Gleason] p. 223Definition 14-1.1(a)met0 18373  xmet0 18372
[Gleason] p. 223Definition 14-1.1(b)metgt0 18389
[Gleason] p. 223Definition 14-1.1(c)metsym 18380
[Gleason] p. 223Definition 14-1.1(d)mettri 18382  mstri 18499  xmettri 18381  xmstri 18498
[Gleason] p. 225Definition 14-1.5xpsmet 18412
[Gleason] p. 230Proposition 14-2.6txlm 17680
[Gleason] p. 240Theorem 14-4.3metcnp4 19262
[Gleason] p. 240Proposition 14-4.2metcnp3 18570
[Gleason] p. 243Proposition 14-4.16addcn 18895  addcn2 12387  mulcn 18897  mulcn2 12389  subcn 18896  subcn2 12388
[Gleason] p. 295Remarkbcval3 11597  bcval4 11598
[Gleason] p. 295Equation 2bcpasc 11612
[Gleason] p. 295Definition of binomial coefficientbcval 11595  df-bc 11594
[Gleason] p. 296Remarkbcn0 11601  bcnn 11603
[Gleason] p. 296Theorem 15-2.8binom 12609
[Gleason] p. 308Equation 2ef0 12693
[Gleason] p. 308Equation 3efcj 12694
[Gleason] p. 309Corollary 15-4.3efne0 12698
[Gleason] p. 309Corollary 15-4.4efexp 12702
[Gleason] p. 310Equation 14sinadd 12765
[Gleason] p. 310Equation 15cosadd 12766
[Gleason] p. 311Equation 17sincossq 12777
[Gleason] p. 311Equation 18cosbnd 12782  sinbnd 12781
[Gleason] p. 311Lemma 15-4.7sqeqor 11495  sqeqori 11493
[Gleason] p. 311Definition of pidf-pi 12675
[Godowski] p. 730Equation SFgoeqi 23776
[GodowskiGreechie] p. 249Equation IV3oai 23170
[Gratzer] p. 23Section 0.6df-mre 13811
[Gratzer] p. 27Section 0.6df-mri 13813
[Halmos] p. 31Theorem 17.3riesz1 23568  riesz2 23569
[Halmos] p. 41Definition of Hermitianhmopadj2 23444
[Halmos] p. 42Definition of projector orderingpjordi 23676
[Halmos] p. 43Theorem 26.1elpjhmop 23688  elpjidm 23687  pjnmopi 23651
[Halmos] p. 44Remarkpjinormi 23189  pjinormii 23178
[Halmos] p. 44Theorem 26.2elpjch 23692  pjrn 23209  pjrni 23204  pjvec 23198
[Halmos] p. 44Theorem 26.3pjnorm2 23229
[Halmos] p. 44Theorem 26.4hmopidmpj 23657  hmopidmpji 23655
[Halmos] p. 45Theorem 27.1pjinvari 23694
[Halmos] p. 45Theorem 27.3pjoci 23683  pjocvec 23199
[Halmos] p. 45Theorem 27.4pjorthcoi 23672
[Halmos] p. 48Theorem 29.2pjssposi 23675
[Halmos] p. 48Theorem 29.3pjssdif1i 23678  pjssdif2i 23677
[Halmos] p. 50Definition of spectrumdf-spec 23358
[Hamilton] p. 28Definition 2.1ax-1 5
[Hamilton] p. 31Example 2.7(a)id1 21
[Hamilton] p. 73Rule 1ax-mp 8
[Hamilton] p. 74Rule 2ax-gen 1555
[Hatcher] p. 25Definitiondf-phtpc 19017  df-phtpy 18996
[Hatcher] p. 26Definitiondf-pco 19030  df-pi1 19033
[Hatcher] p. 26Proposition 1.2phtpcer 19020
[Hatcher] p. 26Proposition 1.3pi1grp 19075
[Herstein] p. 54Exercise 28df-grpo 21779
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14821  grpoideu 21797  mndideu 14698
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14839  grpoinveu 21810
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14858  grpo2inv 21827
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14867  grpoinvop 21829
[Herstein] p. 57Exercise 1isgrp2d 21823  isgrp2i 21824
[Hitchcock] p. 5Rule A3mpto1 1542
[Hitchcock] p. 5Rule A4mpto2 1543
[Hitchcock] p. 5Rule A5mtp-xor 1545
[Holland] p. 1519Theorem 2sumdmdi 23923
[Holland] p. 1520Lemma 5cdj1i 23936  cdj3i 23944  cdj3lem1 23937  cdjreui 23935
[Holland] p. 1524Lemma 7mddmdin0i 23934
[Holland95] p. 13Theorem 3.6hlathil 32762
[Holland95] p. 14Line 15hgmapvs 32692
[Holland95] p. 14Line 16hdmaplkr 32714
[Holland95] p. 14Line 17hdmapellkr 32715
[Holland95] p. 14Line 19hdmapglnm2 32712
[Holland95] p. 14Line 20hdmapip0com 32718
[Holland95] p. 14Theorem 3.6hdmapevec2 32637
[Holland95] p. 14Lines 24 and 25hdmapoc 32732
[Holland95] p. 204Definition of involutiondf-srng 15934
[Holland95] p. 212Definition of subspacedf-psubsp 30300
[Holland95] p. 214Lemma 3.3lclkrlem2v 32326
[Holland95] p. 214Definition 3.2df-lpolN 32279
[Holland95] p. 214Definition of nonsingularpnonsingN 30730
[Holland95] p. 215Lemma 3.3(1)dihoml4 32175  poml4N 30750
[Holland95] p. 215Lemma 3.3(2)dochexmid 32266  pexmidALTN 30775  pexmidN 30766
[Holland95] p. 218Theorem 3.6lclkr 32331
[Holland95] p. 218Definition of dual vector spacedf-ldual 29922  ldualset 29923
[Holland95] p. 222Item 1df-lines 30298  df-pointsN 30299
[Holland95] p. 222Item 2df-polarityN 30700
[Holland95] p. 223Remarkispsubcl2N 30744  omllaw4 30044  pol1N 30707  polcon3N 30714
[Holland95] p. 223Definitiondf-psubclN 30732
[Holland95] p. 223Equation for polaritypolval2N 30703
[Hughes] p. 44Equation 1.21bax-his3 22586
[Hughes] p. 47Definition of projection operatordfpjop 23685
[Hughes] p. 49Equation 1.30eighmre 23466  eigre 23338  eigrei 23337
[Hughes] p. 49Equation 1.31eighmorth 23467  eigorth 23341  eigorthi 23340
[Hughes] p. 137Remark (ii)eigposi 23339
[Huneke] p. 1Theoremfrgrancvvdeq 28431  frgrancvvdgeq 28432
[Huneke] p. 1ObservationfrgrancvvdeqlemA 28426  frgrancvvdeqlemB 28427  frgrancvvdeqlemC 28428
[Huneke] p. 2Prooffrgrawopreglem4 28436  frgrawopreglem5 28437
[Huneke] p. 2Theoremfrghash2spot 28452  frgraregorufr 28442  frgraregorufr0 28441  frgrawopreg1 28439  frgrawopreg2 28440  frgregordn0 28459  usgreghash2spot 28458  usgreghash2spotv 28455
[Indrzejczak] p. 33Definition ` `Enatded 21711  natded 21711
[Indrzejczak] p. 33Definition ` `Inatded 21711
[Indrzejczak] p. 34Definition ` `Enatded 21711  natded 21711
[Indrzejczak] p. 34Definition ` `Inatded 21711
[Jech] p. 4Definition of classcv 1651  cvjust 2431
[Jech] p. 42Lemma 6.1alephexp1 8454
[Jech] p. 42Equation 6.1alephadd 8452  alephmul 8453
[Jech] p. 43Lemma 6.2infmap 8451  infmap2 8098
[Jech] p. 71Lemma 9.3jech9.3 7740
[Jech] p. 72Equation 9.3scott0 7810  scottex 7809
[Jech] p. 72Exercise 9.1rankval4 7793
[Jech] p. 72Scheme "Collection Principle"cp 7815
[Jech] p. 78Definition implied by the footnoteopthprc 4925
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26978
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 27074
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 27075
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26990
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26994
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26995  rmyp1 26996
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26997  rmym1 26998
[JonesMatijasevic] p. 695Equation 2.11rmx0 26988  rmx1 26989  rmxluc 26999
[JonesMatijasevic] p. 695Equation 2.12rmy0 26992  rmy1 26993  rmyluc 27000
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 27002
[JonesMatijasevic] p. 695Equation 2.14rmydbl 27003
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 27025  jm2.17b 27026  jm2.17c 27027
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 27064
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 27068
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 27059
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 27028  jm2.24nn 27024
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 27073
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 27079  rmygeid 27029
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 27091
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1666
[KalishMontague] p. 85Lemma 2equid 1688
[KalishMontague] p. 85Lemma 3equcomi 1691
[KalishMontague] p. 86Lemma 7cbvalivw 1686  cbvaliw 1685
[KalishMontague] p. 87Lemma 8spimvw 1681  spimw 1680
[KalishMontague] p. 87Lemma 9spfw 1703  spw 1706
[Kalmbach] p. 14Definition of latticechabs1 23018  chabs1i 23020  chabs2 23019  chabs2i 23021  chjass 23035  chjassi 22988  latabs1 14516  latabs2 14517
[Kalmbach] p. 15Definition of atomdf-at 23841  ela 23842
[Kalmbach] p. 15Definition of coverscvbr2 23786  cvrval2 30072
[Kalmbach] p. 16Definitiondf-ol 29976  df-oml 29977
[Kalmbach] p. 20Definition of commutescmbr 23086  cmbri 23092  cmtvalN 30009  df-cm 23085  df-cmtN 29975
[Kalmbach] p. 22Remarkomllaw5N 30045  pjoml5 23115  pjoml5i 23090
[Kalmbach] p. 22Definitionpjoml2 23113  pjoml2i 23087
[Kalmbach] p. 22Theorem 2(v)cmcm 23116  cmcmi 23094  cmcmii 23099  cmtcomN 30047
[Kalmbach] p. 22Theorem 2(ii)omllaw3 30043  omlsi 22906  pjoml 22938  pjomli 22937
[Kalmbach] p. 22Definition of OML lawomllaw2N 30042
[Kalmbach] p. 23Remarkcmbr2i 23098  cmcm3 23117  cmcm3i 23096  cmcm3ii 23101  cmcm4i 23097  cmt3N 30049  cmt4N 30050  cmtbr2N 30051
[Kalmbach] p. 23Lemma 3cmbr3 23110  cmbr3i 23102  cmtbr3N 30052
[Kalmbach] p. 25Theorem 5fh1 23120  fh1i 23123  fh2 23121  fh2i 23124  omlfh1N 30056
[Kalmbach] p. 65Remarkchjatom 23860  chslej 23000  chsleji 22960  shslej 22882  shsleji 22872
[Kalmbach] p. 65Proposition 1chocin 22997  chocini 22956  chsupcl 22842  chsupval2 22912  h0elch 22757  helch 22746  hsupval2 22911  ocin 22798  ococss 22795  shococss 22796
[Kalmbach] p. 65Definition of subspace sumshsval 22814
[Kalmbach] p. 66Remarkdf-pjh 22897  pjssmi 23668  pjssmii 23183
[Kalmbach] p. 67Lemma 3osum 23147  osumi 23144
[Kalmbach] p. 67Lemma 4pjci 23703
[Kalmbach] p. 103Exercise 6atmd2 23903
[Kalmbach] p. 103Exercise 12mdsl0 23813
[Kalmbach] p. 140Remarkhatomic 23863  hatomici 23862  hatomistici 23865
[Kalmbach] p. 140Proposition 1atlatmstc 30117
[Kalmbach] p. 140Proposition 1(i)atexch 23884  lsatexch 29841
[Kalmbach] p. 140Proposition 1(ii)chcv1 23858  cvlcvr1 30137  cvr1 30207
[Kalmbach] p. 140Proposition 1(iii)cvexch 23877  cvexchi 23872  cvrexch 30217
[Kalmbach] p. 149Remark 2chrelati 23867  hlrelat 30199  hlrelat5N 30198  lrelat 29812
[Kalmbach] p. 153Exercise 5lsmcv 16213  lsmsatcv 29808  spansncv 23155  spansncvi 23154
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29827  spansncv2 23796
[Kalmbach] p. 266Definitiondf-st 23714
[Kalmbach2] p. 8Definition of adjointdf-adjh 23352
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8521  fpwwe2 8518
[KanamoriPincus] p. 416Corollary 1.3canth4 8522
[KanamoriPincus] p. 417Corollary 1.6canthp1 8529
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8524
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8526
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8539
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8543  gchxpidm 8544
[KanamoriPincus] p. 419Theorem 2.1gchacg 8547  gchhar 8546
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 8096  unxpwdom 7557
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8549
[Kreyszig] p. 3Property M1metcl 18362  xmetcl 18361
[Kreyszig] p. 4Property M2meteq0 18369
[Kreyszig] p. 8Definition 1.1-8dscmet 18620
[Kreyszig] p. 12Equation 5conjmul 9731  muleqadd 9666
[Kreyszig] p. 18Definition 1.3-2mopnval 18468
[Kreyszig] p. 19Remarkmopntopon 18469
[Kreyszig] p. 19Theorem T1mopn0 18528  mopnm 18474
[Kreyszig] p. 19Theorem T2unimopn 18526
[Kreyszig] p. 19Definition of neighborhoodneibl 18531
[Kreyszig] p. 20Definition 1.3-3metcnp2 18572
[Kreyszig] p. 25Definition 1.4-1lmbr 17322  lmmbr 19211  lmmbr2 19212
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17444
[Kreyszig] p. 28Theorem 1.4-5lmcau 19265
[Kreyszig] p. 28Definition 1.4-3iscau 19229  iscmet2 19247
[Kreyszig] p. 30Theorem 1.4-7cmetss 19267
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17524  metelcls 19257
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 19258  metcld2 19259
[Kreyszig] p. 51Equation 2clmvneg1 19116  lmodvneg1 15987  nvinv 22120  vcm 22050
[Kreyszig] p. 51Equation 1aclm0vs 19115  lmod0vs 15983  vc0 22048
[Kreyszig] p. 51Equation 1blmodvs0 15984  vcz 22049
[Kreyszig] p. 58Definition 2.2-1imsmet 22183
[Kreyszig] p. 59Equation 1imsdval 22178  imsdval2 22179
[Kreyszig] p. 63Problem 1nvnd 22180
[Kreyszig] p. 64Problem 2nvge0 22163  nvz 22158
[Kreyszig] p. 64Problem 3nvabs 22162
[Kreyszig] p. 91Definition 2.7-1isblo3i 22302
[Kreyszig] p. 92Equation 2df-nmoo 22246
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 22308  blocni 22306
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 22307
[Kreyszig] p. 129Definition 3.1-1cphipeq0 19166  ipeq0 16869  ipz 22218
[Kreyszig] p. 135Problem 2pythi 22351
[Kreyszig] p. 137Lemma 3-2.1(a)sii 22355
[Kreyszig] p. 144Equation 4supcvg 12635
[Kreyszig] p. 144Theorem 3.3-1minvec 19337  minveco 22386
[Kreyszig] p. 196Definition 3.9-1df-aj 22251
[Kreyszig] p. 247Theorem 4.7-2bcth 19282
[Kreyszig] p. 249Theorem 4.7-3ubth 22375
[Kreyszig] p. 470Definition of positive operator orderingleop 23626  leopg 23625
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 23644
[Kreyszig] p. 525Theorem 10.1-1htth 22421
[Kunen] p. 10Axiom 0a9e 1952  axnul 4337
[Kunen] p. 11Axiom 3axnul 4337
[Kunen] p. 12Axiom 6zfrep6 5968
[Kunen] p. 24Definition 10.24mapval 7030  mapvalg 7028
[Kunen] p. 30Lemma 10.20fodom 8402
[Kunen] p. 31Definition 10.24mapex 7024
[Kunen] p. 95Definition 2.1df-r1 7690
[Kunen] p. 97Lemma 2.10r1elss 7732  r1elssi 7731
[Kunen] p. 107Exercise 4rankop 7784  rankopb 7778  rankuni 7789  rankxplim 7803  rankxpsuc 7806
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4103
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27528
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27523
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27529
[LeBlanc] p. 277Rule R2axnul 4337
[Levy] p. 338Axiomdf-clab 2423  df-clel 2432  df-cleq 2429
[Levy58] p. 2Definition Iisfin1-3 8266
[Levy58] p. 2Definition IIdf-fin2 8166
[Levy58] p. 2Definition Iadf-fin1a 8165
[Levy58] p. 2Definition IIIdf-fin3 8168
[Levy58] p. 3Definition Vdf-fin5 8169
[Levy58] p. 3Definition IVdf-fin4 8167
[Levy58] p. 4Definition VIdf-fin6 8170
[Levy58] p. 4Definition VIIdf-fin7 8171
[Levy58], p. 3Theorem 1fin1a2 8295
[Lopez-Astorga] p. 12Rule 1mpto1 1542
[Lopez-Astorga] p. 12Rule 2mpto2 1543
[Lopez-Astorga] p. 12Rule 3mtp-xor 1545
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 23911
[Maeda] p. 168Lemma 5mdsym 23915  mdsymi 23914
[Maeda] p. 168Lemma 4(i)mdsymlem4 23909  mdsymlem6 23911  mdsymlem7 23912
[Maeda] p. 168Lemma 4(ii)mdsymlem8 23913
[MaedaMaeda] p. 1Remarkssdmd1 23816  ssdmd2 23817  ssmd1 23814  ssmd2 23815
[MaedaMaeda] p. 1Lemma 1.2mddmd2 23812
[MaedaMaeda] p. 1Definition 1.1df-dmd 23784  df-md 23783  mdbr 23797
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 23834  mdslj1i 23822  mdslj2i 23823  mdslle1i 23820  mdslle2i 23821  mdslmd1i 23832  mdslmd2i 23833
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 23824  mdsl2bi 23826  mdsl2i 23825
[MaedaMaeda] p. 2Lemma 1.6mdexchi 23838
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 23835
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 23836
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 23813
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 23818  mdsl3 23819
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 23837
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23932
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 30119  hlrelat1 30197
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29837
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 23839  cvmdi 23827  cvnbtwn4 23792  cvrnbtwn4 30077
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 23840
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 30138  cvp 23878  cvrp 30213  lcvp 29838
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 23902
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 23901
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 30131  hlexch4N 30189
[MaedaMaeda] p. 34Exercise 7.1atabsi 23904
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 30240
[MaedaMaeda] p. 61Definition 15.10psubN 30546  atpsubN 30550  df-pointsN 30299  pointpsubN 30548
[MaedaMaeda] p. 62Theorem 15.5df-pmap 30301  pmap11 30559  pmaple 30558  pmapsub 30565  pmapval 30554
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 30562  pmap1N 30564
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 30567  pmapglb2N 30568  pmapglb2xN 30569  pmapglbx 30566
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 30649
[MaedaMaeda] p. 67Postulate PS1ps-1 30274
[MaedaMaeda] p. 68Lemma 16.2df-padd 30593  paddclN 30639  paddidm 30638
[MaedaMaeda] p. 68Condition PS2ps-2 30275
[MaedaMaeda] p. 68Equation 16.2.1paddass 30635
[MaedaMaeda] p. 69Lemma 16.4ps-1 30274
[MaedaMaeda] p. 69Theorem 16.4ps-2 30275
[MaedaMaeda] p. 70Theorem 16.9lsmmod 15307  lsmmod2 15308  lssats 29810  shatomici 23861  shatomistici 23864  shmodi 22892  shmodsi 22891
[MaedaMaeda] p. 130Remark 29.6dmdmd 23803  mdsymlem7 23912
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 23091
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22995
[MaedaMaeda] p. 139Remarksumdmdii 23918
[Margaris] p. 40Rule Cexlimiv 1644
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 7
[Margaris] p. 49Definitiondf-an 361  df-ex 1551  df-or 360  dfbi2 610
[Margaris] p. 51Theorem 1id1 21
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 29027
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 29028
[Margaris] p. 79Rule Cexinst01 28726  exinst11 28727
[Margaris] p. 89Theorem 19.219.2 1671  19.2g 1773  r19.2z 3717
[Margaris] p. 89Theorem 19.319.3 1791  19.3v 1677  rr19.3v 3077
[Margaris] p. 89Theorem 19.5alcom 1752
[Margaris] p. 89Theorem 19.6alex 1581
[Margaris] p. 89Theorem 19.7alnex 1552
[Margaris] p. 89Theorem 19.819.8a 1762
[Margaris] p. 89Theorem 19.919.9 1797  19.9h 1794  19.9v 1676  exlimd 1824  exlimdh 1826
[Margaris] p. 89Theorem 19.11excom 1756  excomim 1757
[Margaris] p. 89Theorem 19.1219.12 1869  r19.12 2819
[Margaris] p. 90Theorem 19.14exnal 1583
[Margaris] p. 90Theorem 19.152albi 27553  albi 1573  ralbi 2842
[Margaris] p. 90Theorem 19.1619.16 1883
[Margaris] p. 90Theorem 19.1719.17 1884
[Margaris] p. 90Theorem 19.182exbi 27555  exbi 1591
[Margaris] p. 90Theorem 19.1919.19 1885
[Margaris] p. 90Theorem 19.202alim 27552  alim 1567  alimd 1780  alimdh 1572  alimdv 1631  ralimdaa 2783  ralimdv 2785  ralimdva 2784  sbcimdv 3222
[Margaris] p. 90Theorem 19.2119.21-2 1887  19.21 1814  19.21bi 1774  19.21h 1815  19.21t 1813  19.21v 1913  19.21vv 27551  alrimd 1785  alrimdd 1784  alrimdh 1597  alrimdv 1643  alrimi 1781  alrimih 1574  alrimiv 1641  alrimivv 1642  r19.21 2792  r19.21be 2807  r19.21bi 2804  r19.21t 2791  r19.21v 2793  ralrimd 2794  ralrimdv 2795  ralrimdva 2796  ralrimdvv 2800  ralrimdvva 2801  ralrimi 2787  ralrimiv 2788  ralrimiva 2789  ralrimivv 2797  ralrimivva 2798  ralrimivvva 2799  ralrimivw 2790  rexlimi 2823
[Margaris] p. 90Theorem 19.222alimdv 1633  2exim 27554  2eximdv 1634  exim 1584  eximd 1786  eximdh 1598  eximdv 1632  rexim 2810  reximdai 2814  reximddv 23962  reximdv 2817  reximdv2 2815  reximdva 2818  reximdvai 2816  reximi2 2812
[Margaris] p. 90Theorem 19.2319.23 1819  19.23bi 1775  19.23h 1820  19.23t 1818  19.23v 1914  19.23vv 1915  exlimdv 1646  exlimdvv 1647  exlimexi 28608  exlimi 1821  exlimih 1822  exlimiv 1644  exlimivv 1645  r19.23 2821  r19.23v 2822  rexlimd 2827  rexlimdv 2829  rexlimdv3a 2832  rexlimdva 2830  rexlimdvaa 2831  rexlimdvv 2836  rexlimdvva 2837  rexlimdvw 2833  rexlimiv 2824  rexlimiva 2825  rexlimivv 2835
[Margaris] p. 90Theorem 19.2419.24 1674
[Margaris] p. 90Theorem 19.2519.25 1613
[Margaris] p. 90Theorem 19.2619.26-2 1604  19.26-3an 1605  19.26 1603  r19.26-2 2839  r19.26-3 2840  r19.26 2838  r19.26m 2841
[Margaris] p. 90Theorem 19.2719.27 1841  19.27v 1917  r19.27av 2844  r19.27z 3726  r19.27zv 3727
[Margaris] p. 90Theorem 19.2819.28 1842  19.28v 1918  19.28vv 27561  r19.28av 2845  r19.28z 3720  r19.28zv 3723  rr19.28v 3078
[Margaris] p. 90Theorem 19.2919.29 1606  19.29r 1607  19.29r2 1608  19.29x 1609  r19.29 2846  r19.29d2r 2851  r19.29r 2847
[Margaris] p. 90Theorem 19.3019.30 1614  r19.30 2853
[Margaris] p. 90Theorem 19.3119.31 1897  19.31vv 27559
[Margaris] p. 90Theorem 19.3219.32 1896  r19.32 27921  r19.32v 2854
[Margaris] p. 90Theorem 19.3319.33-2 27557  19.33 1617  19.33b 1618
[Margaris] p. 90Theorem 19.3419.34 1675
[Margaris] p. 90Theorem 19.3519.35 1610  19.35i 1611  19.35ri 1612  r19.35 2855
[Margaris] p. 90Theorem 19.3619.36 1892  19.36aiv 1920  19.36i 1893  19.36v 1919  19.36vv 27558  r19.36av 2856  r19.36zv 3728
[Margaris] p. 90Theorem 19.3719.37 1894  19.37aiv 1923  19.37v 1922  19.37vv 27560  r19.37 2857  r19.37av 2858  r19.37zv 3724
[Margaris] p. 90Theorem 19.3819.38 1812
[Margaris] p. 90Theorem 19.3919.39 1673
[Margaris] p. 90Theorem 19.4019.40-2 1620  19.40 1619  r19.40 2859
[Margaris] p. 90Theorem 19.4119.41 1900  19.41rg 28637  19.41v 1924  19.41vv 1925  19.41vvv 1926  19.41vvvv 1927  r19.41 2860  r19.41v 2861  r19.41vv 23970
[Margaris] p. 90Theorem 19.4219.42 1902  19.42v 1928  19.42vv 1930  19.42vvv 1931  r19.42v 2862
[Margaris] p. 90Theorem 19.4319.43 1615  r19.43 2863
[Margaris] p. 90Theorem 19.4419.44 1898  r19.44av 2864
[Margaris] p. 90Theorem 19.4519.45 1899  r19.45av 2865  r19.45zv 3725
[Margaris] p. 110Exercise 2(b)eu1 2302
[Mayet] p. 370Remarkjpi 23773  largei 23770  stri 23760
[Mayet3] p. 9Definition of CH-statesdf-hst 23715  ishst 23717
[Mayet3] p. 10Theoremhstrbi 23769  hstri 23768
[Mayet3] p. 1223Theorem 4.1mayete3i 23230
[Mayet3] p. 1240Theorem 7.1mayetes3i 23232
[MegPav2000] p. 2344Theorem 3.3stcltrthi 23781
[MegPav2000] p. 2345Definition 3.4-1chintcl 22834  chsupcl 22842
[MegPav2000] p. 2345Definition 3.4-2hatomic 23863
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 23857
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 23884
[MegPav2000] p. 2366Figure 7pl42N 30780
[MegPav2002] p. 362Lemma 2.2latj31 14528  latj32 14526  latjass 14524
[Megill] p. 444Axiom C5ax-17 1626  ax17o 2234
[Megill] p. 444Section 7conventions 21710
[Megill] p. 445Lemma L12aecom-o 2228  aecom 2035  ax-10 2217
[Megill] p. 446Lemma L17equtrr 1695
[Megill] p. 446Lemma L18ax9from9o 2225
[Megill] p. 446Lemma L19hbnae-o 2256  hbnae 2043
[Megill] p. 447Remark 9.1df-sb 1659  sbid 1947  sbidd-misc 28462  sbidd 28461
[Megill] p. 448Remark 9.6ax15 2107
[Megill] p. 448Scheme C4'ax-5o 2213
[Megill] p. 448Scheme C5'ax-4 2212  sp 1763
[Megill] p. 448Scheme C6'ax-7 1749
[Megill] p. 448Scheme C7'ax-6o 2214
[Megill] p. 448Scheme C8'ax-8 1687
[Megill] p. 448Scheme C9'ax-12o 2219
[Megill] p. 448Scheme C10'ax-9 1666  ax-9o 2215
[Megill] p. 448Scheme C11'ax-10o 2216
[Megill] p. 448Scheme C12'ax-13 1727
[Megill] p. 448Scheme C13'ax-14 1729
[Megill] p. 448Scheme C14'ax-15 2220
[Megill] p. 448Scheme C15'ax-11o 2218
[Megill] p. 448Scheme C16'ax-16 2221
[Megill] p. 448Theorem 9.4dral1-o 2231  dral1 2057  dral2-o 2258  dral2 2055  drex1 2059  drex2 2060  drsb1 2112  drsb2 2113
[Megill] p. 448Theorem 9.7conventions 21710
[Megill] p. 449Theorem 9.7sbcom2 2190  sbequ 2111  sbid2v 2200
[Megill] p. 450Example in Appendixhba1-o 2226  hba1 1804
[Mendelson] p. 35Axiom A3hirstL-ax3 27836
[Mendelson] p. 36Lemma 1.8id1 21
[Mendelson] p. 69Axiom 4rspsbc 3239  rspsbca 3240  stdpc4 2091
[Mendelson] p. 69Axiom 5ax-5o 2213  ra5 3245  stdpc5 1816
[Mendelson] p. 81Rule Cexlimiv 1644
[Mendelson] p. 95Axiom 6stdpc6 1699
[Mendelson] p. 95Axiom 7stdpc7 1942
[Mendelson] p. 225Axiom system NBGru 3160
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4458
[Mendelson] p. 231Exercise 4.10(k)inv1 3654
[Mendelson] p. 231Exercise 4.10(l)unv 3655
[Mendelson] p. 231Exercise 4.10(n)dfin3 3580
[Mendelson] p. 231Exercise 4.10(o)df-nul 3629
[Mendelson] p. 231Exercise 4.10(q)dfin4 3581
[Mendelson] p. 231Exercise 4.10(s)ddif 3479
[Mendelson] p. 231Definition of uniondfun3 3579
[Mendelson] p. 235Exercise 4.12(c)univ 4754
[Mendelson] p. 235Exercise 4.12(d)pwv 4014
[Mendelson] p. 235Exercise 4.12(j)pwin 4487
[Mendelson] p. 235Exercise 4.12(k)pwunss 4488
[Mendelson] p. 235Exercise 4.12(l)pwssun 4489
[Mendelson] p. 235Exercise 4.12(n)uniin 4035
[Mendelson] p. 235Exercise 4.12(p)reli 5002
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5390
[Mendelson] p. 244Proposition 4.8(g)epweon 4764
[Mendelson] p. 246Definition of successordf-suc 4587
[Mendelson] p. 250Exercise 4.36oelim2 6838
[Mendelson] p. 254Proposition 4.22(b)xpen 7270
[Mendelson] p. 254Proposition 4.22(c)xpsnen 7192  xpsneng 7193
[Mendelson] p. 254Proposition 4.22(d)xpcomen 7199  xpcomeng 7200
[Mendelson] p. 254Proposition 4.22(e)xpassen 7202
[Mendelson] p. 255Definitionbrsdom 7130
[Mendelson] p. 255Exercise 4.39endisj 7195
[Mendelson] p. 255Exercise 4.41mapprc 7022
[Mendelson] p. 255Exercise 4.43mapsnen 7184
[Mendelson] p. 255Exercise 4.45mapunen 7276
[Mendelson] p. 255Exercise 4.47xpmapen 7275
[Mendelson] p. 255Exercise 4.42(a)map0e 7051
[Mendelson] p. 255Exercise 4.42(b)map1 7185
[Mendelson] p. 257Proposition 4.24(a)undom 7196
[Mendelson] p. 258Exercise 4.56(b)cdaen 8053
[Mendelson] p. 258Exercise 4.56(c)cdaassen 8062  cdacomen 8061
[Mendelson] p. 258Exercise 4.56(f)cdadom1 8066
[Mendelson] p. 258Exercise 4.56(g)xp2cda 8060
[Mendelson] p. 258Definition of cardinal sumcdaval 8050  df-cda 8048
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6775
[Mendelson] p. 266Proposition 4.34(f)oaordex 6801
[Mendelson] p. 275Proposition 4.42(d)entri3 8434
[Mendelson] p. 281Definitiondf-r1 7690
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7739
[Mendelson] p. 287Axiom system MKru 3160
[MertziosUnger] p. 153Proposition 12pthfrgra 28401  2pthfrgrarn 28399  2pthfrgrarn2 28400  frconngra 28411  n4cyclfrgra 28408  vdgfrgragt2 28418  vdgn1frgrav2 28417  vdn1frgrav2 28416
[Mittelstaedt] p. 9Definitiondf-oc 22754
[Monk1] p. 22Remarkconventions 21710
[Monk1] p. 22Theorem 3.1conventions 21710
[Monk1] p. 26Theorem 2.8(vii)ssin 3563
[Monk1] p. 33Theorem 3.2(i)ssrel 4964
[Monk1] p. 33Theorem 3.2(ii)eqrel 4965
[Monk1] p. 34Definition 3.3df-opab 4267
[Monk1] p. 36Theorem 3.7(i)coi1 5385  coi2 5386
[Monk1] p. 36Theorem 3.8(v)dm0 5083  rn0 5127
[Monk1] p. 36Theorem 3.7(ii)cnvi 5276
[Monk1] p. 37Theorem 3.13(i)relxp 4983
[Monk1] p. 37Theorem 3.13(x)dmxp 5088  rnxp 5299
[Monk1] p. 37Theorem 3.13(ii)xp0 5291  xp0r 4956
[Monk1] p. 38Theorem 3.16(ii)ima0 5221
[Monk1] p. 38Theorem 3.16(viii)imai 5218
[Monk1] p. 39Theorem 3.17imaexg 5217
[Monk1] p. 39Theorem 3.16(xi)imassrn 5216
[Monk1] p. 41Theorem 4.3(i)fnopfv 5865  funfvop 5842
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5770
[Monk1] p. 42Theorem 4.4(iii)fvelima 5778
[Monk1] p. 43Theorem 4.6funun 5495
[Monk1] p. 43Theorem 4.8(iv)dff13 6004  dff13f 6006
[Monk1] p. 46Theorem 4.15(v)funex 5963  funrnex 5967
[Monk1] p. 50Definition 5.4fniunfv 5994
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5353
[Monk1] p. 52Theorem 5.11(viii)ssint 4066
[Monk1] p. 52Definition 5.13 (i)1stval2 6364  df-1st 6349
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6365  df-2nd 6350
[Monk1] p. 112Theorem 15.17(v)ranksn 7780  ranksnb 7753
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7781
[Monk1] p. 112Theorem 15.17(iii)rankun 7782  rankunb 7776
[Monk1] p. 113Theorem 15.18r1val3 7764
[Monk1] p. 113Definition 15.19df-r1 7690  r1val2 7763
[Monk1] p. 117Lemmazorn2 8386  zorn2g 8383
[Monk1] p. 133Theorem 18.11cardom 7873
[Monk1] p. 133Theorem 18.12canth3 8436
[Monk1] p. 133Theorem 18.14carduni 7868
[Monk2] p. 105Axiom C4ax-5 1566
[Monk2] p. 105Axiom C7ax-8 1687
[Monk2] p. 105Axiom C8ax-11 1761  ax-11o 2218
[Monk2] p. 105Axiom (C8)ax11v 2172
[Monk2] p. 108Lemma 5ax-5o 2213
[Monk2] p. 109Lemma 12ax-7 1749
[Monk2] p. 109Lemma 15equvin 2087  equvini 2083  eqvinop 4441
[Monk2] p. 113Axiom C5-1ax-17 1626  ax17o 2234
[Monk2] p. 113Axiom C5-2ax-6 1744
[Monk2] p. 113Axiom C5-3ax-7 1749
[Monk2] p. 114Lemma 21sp 1763
[Monk2] p. 114Lemma 22ax5o 1765  hba1-o 2226  hba1 1804
[Monk2] p. 114Lemma 23nfia1 1875
[Monk2] p. 114Lemma 24nfa2 1874  nfra2 2760
[Moore] p. 53Part Idf-mre 13811
[Munkres] p. 77Example 2distop 17060  indistop 17066  indistopon 17065
[Munkres] p. 77Example 3fctop 17068  fctop2 17069
[Munkres] p. 77Example 4cctop 17070
[Munkres] p. 78Definition of basisdf-bases 16965  isbasis3g 17014
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13667  tgval2 17021
[Munkres] p. 79Remarktgcl 17034
[Munkres] p. 80Lemma 2.1tgval3 17028
[Munkres] p. 80Lemma 2.2tgss2 17052  tgss3 17051
[Munkres] p. 81Lemma 2.3basgen 17053  basgen2 17054
[Munkres] p. 89Definition of subspace topologyresttop 17224
[Munkres] p. 93Theorem 6.1(1)0cld 17102  topcld 17099
[Munkres] p. 93Theorem 6.1(2)iincld 17103
[Munkres] p. 93Theorem 6.1(3)uncld 17105
[Munkres] p. 94Definition of closureclsval 17101
[Munkres] p. 94Definition of interiorntrval 17100
[Munkres] p. 95Theorem 6.5(a)clsndisj 17139  elcls 17137
[Munkres] p. 95Theorem 6.5(b)elcls3 17147
[Munkres] p. 97Theorem 6.6clslp 17212  neindisj 17181
[Munkres] p. 97Corollary 6.7cldlp 17214
[Munkres] p. 97Definition of limit pointislp2 17209  lpval 17203
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17379
[Munkres] p. 102Definition of continuous functiondf-cn 17291  iscn 17299  iscn2 17302
[Munkres] p. 107Theorem 7.2(g)cncnp 17344  cncnp2 17345  cncnpi 17342  df-cnp 17292  iscnp 17301  iscnp2 17303
[Munkres] p. 127Theorem 10.1metcn 18573
[Munkres] p. 128Theorem 10.3metcn4 19263
[NielsenChuang] p. 195Equation 4.73unierri 23607
[Pfenning] p. 17Definition XMnatded 21711
[Pfenning] p. 17Definition NNCnatded 21711  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 21711
[Pfenning] p. 18Rule"natded 21711
[Pfenning] p. 18Definition /\Inatded 21711
[Pfenning] p. 18Definition ` `Enatded 21711  natded 21711  natded 21711  natded 21711  natded 21711
[Pfenning] p. 18Definition ` `Inatded 21711  natded 21711  natded 21711  natded 21711  natded 21711
[Pfenning] p. 18Definition ` `ELnatded 21711
[Pfenning] p. 18Definition ` `ERnatded 21711
[Pfenning] p. 18Definition ` `Ea,unatded 21711
[Pfenning] p. 18Definition ` `IRnatded 21711
[Pfenning] p. 18Definition ` `Ianatded 21711
[Pfenning] p. 127Definition =Enatded 21711
[Pfenning] p. 127Definition =Inatded 21711
[Ponnusamy] p. 361Theorem 6.44cphip0l 19164  df-dip 22197  dip0l 22217  ip0l 16867
[Ponnusamy] p. 361Equation 6.45ipval 22199
[Ponnusamy] p. 362Equation I1dipcj 22213
[Ponnusamy] p. 362Equation I3cphdir 19167  dipdir 22343  ipdir 16870  ipdiri 22331
[Ponnusamy] p. 362Equation I4ipidsq 22209
[Ponnusamy] p. 362Equation 6.46ip0i 22326
[Ponnusamy] p. 362Equation 6.47ip1i 22328
[Ponnusamy] p. 362Equation 6.48ip2i 22329
[Ponnusamy] p. 363Equation I2cphass 19173  dipass 22346  ipass 16876  ipassi 22342
[Prugovecki] p. 186Definition of brabraval 23447  df-bra 23353
[Prugovecki] p. 376Equation 8.1df-kb 23354  kbval 23457
[PtakPulmannova] p. 66Proposition 3.2.17atomli 23885
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30685
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 23899  atcvat4i 23900  cvrat3 30239  cvrat4 30240  lsatcvat3 29850
[PtakPulmannova] p. 68Definition 3.2.18cvbr 23785  cvrval 30067  df-cv 23782  df-lcv 29817  lspsncv0 16218
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30697
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30698
[Quine] p. 16Definition 2.1df-clab 2423  rabid 2884
[Quine] p. 17Definition 2.1''dfsb7 2198
[Quine] p. 18Definition 2.7df-cleq 2429
[Quine] p. 19Definition 2.9conventions 21710  df-v 2958
[Quine] p. 34Theorem 5.1abeq2 2541
[Quine] p. 35Theorem 5.2abid2 2553  abid2f 2597
[Quine] p. 40Theorem 6.1sb5 2176
[Quine] p. 40Theorem 6.2sb56 2174  sb6 2175
[Quine] p. 41Theorem 6.3df-clel 2432
[Quine] p. 41Theorem 6.4eqid 2436  eqid1 21761
[Quine] p. 41Theorem 6.5eqcom 2438
[Quine] p. 42Theorem 6.6df-sbc 3162
[Quine] p. 42Theorem 6.7dfsbcq 3163  dfsbcq2 3164
[Quine] p. 43Theorem 6.8vex 2959
[Quine] p. 43Theorem 6.9isset 2960
[Quine] p. 44Theorem 7.3spcgf 3031  spcgv 3036  spcimgf 3029
[Quine] p. 44Theorem 6.11spsbc 3173  spsbcd 3174
[Quine] p. 44Theorem 6.12elex 2964
[Quine] p. 44Theorem 6.13elab 3082  elabg 3083  elabgf 3080
[Quine] p. 44Theorem 6.14noel 3632
[Quine] p. 48Theorem 7.2snprc 3871
[Quine] p. 48Definition 7.1df-pr 3821  df-sn 3820
[Quine] p. 49Theorem 7.4snss 3926  snssg 3932
[Quine] p. 49Theorem 7.5prss 3952  prssg 3953
[Quine] p. 49Theorem 7.6prid1 3912  prid1g 3910  prid2 3913  prid2g 3911  snid 3841  snidg 3839
[Quine] p. 51Theorem 7.13prex 4406  snex 4405  snexALT 4385
[Quine] p. 53Theorem 8.2unisn 4031  unisnALT 29038  unisng 4032
[Quine] p. 53Theorem 8.3uniun 4034
[Quine] p. 54Theorem 8.6elssuni 4043
[Quine] p. 54Theorem 8.7uni0 4042
[Quine] p. 56Theorem 8.17uniabio 5428
[Quine] p. 56Definition 8.18dfiota2 5419
[Quine] p. 57Theorem 8.19iotaval 5429
[Quine] p. 57Theorem 8.22iotanul 5433
[Quine] p. 58Theorem 8.23iotaex 5435
[Quine] p. 58Definition 9.1df-op 3823
[Quine] p. 61Theorem 9.5opabid 4461  opelopab 4476  opelopaba 4471  opelopabaf 4478  opelopabf 4479  opelopabg 4473  opelopabga 4468  opelopabgf 28071  oprabid 6105
[Quine] p. 64Definition 9.11df-xp 4884
[Quine] p. 64Definition 9.12df-cnv 4886
[Quine] p. 64Definition 9.15df-id 4498
[Quine] p. 65Theorem 10.3fun0 5508
[Quine] p. 65Theorem 10.4funi 5483
[Quine] p. 65Theorem 10.5funsn 5499  funsng 5497
[Quine] p. 65Definition 10.1df-fun 5456
[Quine] p. 65Definition 10.2args 5232  dffv4 5725
[Quine] p. 68Definition 10.11conventions 21710  df-fv 5462  fv2 5723
[Quine] p. 124Theorem 17.3nn0opth2 11565  nn0opth2i 11564  nn0opthi 11563  omopthi 6900
[Quine] p. 177Definition 25.2df-rdg 6668
[Quine] p. 232Equation icarddom 8429
[Quine] p. 284Axiom 39(vi)funimaex 5531  funimaexg 5530
[Quine] p. 331Axiom system NFru 3160
[ReedSimon] p. 36Definition (iii)ax-his3 22586
[ReedSimon] p. 63Exercise 4(a)df-dip 22197  polid 22661  polid2i 22659  polidi 22660
[ReedSimon] p. 63Exercise 4(b)df-ph 22314
[ReedSimon] p. 195Remarklnophm 23522  lnophmi 23521
[Retherford] p. 49Exercise 1(i)leopadd 23635
[Retherford] p. 49Exercise 1(ii)leopmul 23637  leopmuli 23636
[Retherford] p. 49Exercise 1(iv)leoptr 23640
[Retherford] p. 49Definition VI.1df-leop 23355  leoppos 23629
[Retherford] p. 49Exercise 1(iii)leoptri 23639
[Retherford] p. 49Definition of operator orderingleop3 23628
[Rudin] p. 164Equation 27efcan 12697
[Rudin] p. 164Equation 30efzval 12703
[Rudin] p. 167Equation 48absefi 12797
[Sanford] p. 39Remarkax-mp 8  mto 169
[Sanford] p. 39Rule 3mtp-xor 1545
[Sanford] p. 39Rule 4mpto2 1543
[Sanford] p. 40Rule 1mpto1 1542
[Schechter] p. 51Definition of antisymmetryintasym 5249
[Schechter] p. 51Definition of irreflexivityintirr 5252
[Schechter] p. 51Definition of symmetrycnvsym 5248
[Schechter] p. 51Definition of transitivitycotr 5246
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13811
[Schechter] p. 79Definition of Moore closuredf-mrc 13812
[Schechter] p. 82Section 4.5df-mrc 13812
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13814
[Schechter] p. 139Definition AC3dfac9 8016
[Schechter] p. 141Definition (MC)dfac11 27137
[Schechter] p. 149Axiom DC1ax-dc 8326  axdc3 8334
[Schechter] p. 187Definition of ring with unitisrng 15668  isrngo 21966
[Schechter] p. 276Remark 11.6.espan0 23044
[Schechter] p. 276Definition of spandf-span 22811  spanval 22835
[Schechter] p. 428Definition 15.35bastop1 17058
[Schwabhauser] p. 10Axiom A1axcgrrflx 25853
[Schwabhauser] p. 10Axiom A2axcgrtr 25854
[Schwabhauser] p. 10Axiom A3axcgrid 25855
[Schwabhauser] p. 11Axiom A4axsegcon 25866
[Schwabhauser] p. 11Axiom A5ax5seg 25877
[Schwabhauser] p. 11Axiom A6axbtwnid 25878
[Schwabhauser] p. 12Axiom A7axpasch 25880
[Schwabhauser] p. 12Axiom A8axlowdim2 25899
[Schwabhauser] p. 13Axiom A10axeuclid 25902
[Schwabhauser] p. 13Axiom A11axcont 25915
[Schwabhauser] p. 27Theorem 2.1cgrrflx 25921
[Schwabhauser] p. 27Theorem 2.2cgrcomim 25923
[Schwabhauser] p. 27Theorem 2.3cgrtr 25926
[Schwabhauser] p. 27Theorem 2.4cgrcoml 25930
[Schwabhauser] p. 27Theorem 2.5cgrcomr 25931
[Schwabhauser] p. 28Theorem 2.8cgrtriv 25936
[Schwabhauser] p. 28Theorem 2.105segofs 25940
[Schwabhauser] p. 28Definition 2.10df-ofs 25917
[Schwabhauser] p. 29Theorem 2.11cgrextend 25942
[Schwabhauser] p. 29Theorem 2.12segconeq 25944
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 25956  btwntriv2 25946
[Schwabhauser] p. 30Theorem 3.2btwncomim 25947
[Schwabhauser] p. 30Theorem 3.3btwntriv1 25950
[Schwabhauser] p. 30Theorem 3.4btwnswapid 25951
[Schwabhauser] p. 30Theorem 3.5btwnexch2 25957  btwnintr 25953
[Schwabhauser] p. 30Theorem 3.6btwnexch 25959  btwnexch3 25954
[Schwabhauser] p. 30Theorem 3.7btwnouttr 25958
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25898
[Schwabhauser] p. 32Theorem 3.14btwndiff 25961
[Schwabhauser] p. 33Theorem 3.17trisegint 25962
[Schwabhauser] p. 34Theorem 4.2ifscgr 25978
[Schwabhauser] p. 34Definition 4.1df-ifs 25973
[Schwabhauser] p. 35Theorem 4.3cgrsub 25979
[Schwabhauser] p. 35Theorem 4.5cgrxfr 25989
[Schwabhauser] p. 35Definition 4.4df-cgr3 25974
[Schwabhauser] p. 36Theorem 4.6btwnxfr 25990
[Schwabhauser] p. 36Theorem 4.11colinearperm1 25996  colinearperm2 25998  colinearperm3 25997  colinearperm4 25999  colinearperm5 26000
[Schwabhauser] p. 36Definition 4.10df-colinear 25975
[Schwabhauser] p. 37Theorem 4.12colineartriv1 26001
[Schwabhauser] p. 37Theorem 4.13colinearxfr 26009
[Schwabhauser] p. 37Theorem 4.14lineext 26010
[Schwabhauser] p. 37Theorem 4.16fscgr 26014
[Schwabhauser] p. 37Theorem 4.17linecgr 26015
[Schwabhauser] p. 37Definition 4.15df-fs 25976
[Schwabhauser] p. 38Theorem 4.18lineid 26017
[Schwabhauser] p. 38Theorem 4.19idinside 26018
[Schwabhauser] p. 39Theorem 5.1btwnconn1 26035
[Schwabhauser] p. 41Theorem 5.2btwnconn2 26036
[Schwabhauser] p. 41Theorem 5.3btwnconn3 26037
[Schwabhauser] p. 41Theorem 5.5brsegle2 26043
[Schwabhauser] p. 41Definition 5.4df-segle 26041
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 26044
[Schwabhauser] p. 42Theorem 5.7seglerflx 26046
[Schwabhauser] p. 42Theorem 5.8segletr 26048
[Schwabhauser] p. 42Theorem 5.9segleantisym 26049
[Schwabhauser] p. 42Theorem 5.10seglelin 26050
[Schwabhauser] p. 42Theorem 5.11seglemin 26047
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 26052
[Schwabhauser] p. 43Theorem 6.2btwnoutside 26059
[Schwabhauser] p. 43Theorem 6.3broutsideof3 26060
[Schwabhauser] p. 43Theorem 6.4broutsideof 26055  df-outsideof 26054
[Schwabhauser] p. 43Definition 6.1broutsideof2 26056
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 26061
[Schwabhauser] p. 44Theorem 6.6outsideofcom 26062
[Schwabhauser] p. 44Theorem 6.7outsideoftr 26063
[Schwabhauser] p. 44Theorem 6.11outsideofeu 26065
[Schwabhauser] p. 44Definition 6.8df-ray 26072
[Schwabhauser] p. 45Part 2df-lines2 26073
[Schwabhauser] p. 45Theorem 6.13outsidele 26066
[Schwabhauser] p. 45Theorem 6.15lineunray 26081
[Schwabhauser] p. 45Theorem 6.16lineelsb2 26082
[Schwabhauser] p. 45Theorem 6.17linecom 26084  linerflx1 26083  linerflx2 26085
[Schwabhauser] p. 45Theorem 6.18linethru 26087
[Schwabhauser] p. 45Definition 6.14df-line2 26071
[Schwabhauser] p. 46Theorem 6.19linethrueu 26090
[Schwabhauser] p. 46Theorem 6.21lineintmo 26091
[Shapiro] p. 230Theorem 6.5.1dchrhash 21055  dchrsum 21053  dchrsum2 21052  sumdchr 21056
[Shapiro] p. 232Theorem 6.5.2dchr2sum 21057  sum2dchr 21058
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15624  ablfacrp2 15625
[Shapiro], p. 328Equation 9.2.4vmasum 21000
[Shapiro], p. 329Equation 9.2.7logfac2 21001
[Shapiro], p. 329Equation 9.2.9logfacrlim 21008
[Shapiro], p. 331Equation 9.2.13vmadivsum 21176
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 21179
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 21233  vmalogdivsum2 21232
[Shapiro], p. 375Theorem 9.4.1dirith 21223  dirith2 21222
[Shapiro], p. 375Equation 9.4.3rplogsum 21221  rpvmasum 21220  rpvmasum2 21206
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 21181
[Shapiro], p. 376Equation 9.4.8dchrvmasum 21219
[Shapiro], p. 377Lemma 9.4.1dchrisum 21186  dchrisumlem1 21183  dchrisumlem2 21184  dchrisumlem3 21185  dchrisumlema 21182
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 21189
[Shapiro], p. 379Equation 9.4.16dchrmusum 21218  dchrmusumlem 21216  dchrvmasumlem 21217
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 21188
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 21190
[Shapiro], p. 382Lemma 9.4.4dchrisum0 21214  dchrisum0re 21207  dchrisumn0 21215
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 21200
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 21204
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 21205
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 21260  pntrsumbnd2 21261  pntrsumo1 21259
[Shapiro], p. 405Equation 10.2.1mudivsum 21224
[Shapiro], p. 406Equation 10.2.6mulogsum 21226
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 21228
[Shapiro], p. 407Equation 10.2.8mulog2sum 21231
[Shapiro], p. 418Equation 10.4.6logsqvma 21236
[Shapiro], p. 418Equation 10.4.8logsqvma2 21237
[Shapiro], p. 419Equation 10.4.10selberg 21242
[Shapiro], p. 420Equation 10.4.12selberg2lem 21244
[Shapiro], p. 420Equation 10.4.14selberg2 21245
[Shapiro], p. 422Equation 10.6.7selberg3 21253
[Shapiro], p. 422Equation 10.4.20selberg4lem1 21254
[Shapiro], p. 422Equation 10.4.21selberg3lem1 21251  selberg3lem2 21252
[Shapiro], p. 422Equation 10.4.23selberg4 21255
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 21249
[Shapiro], p. 428Equation 10.6.2selbergr 21262
[Shapiro], p. 429Equation 10.6.8selberg3r 21263
[Shapiro], p. 430Equation 10.6.11selberg4r 21264
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 21278
[Shapiro], p. 434Equation 10.6.27pntlema 21290  pntlemb 21291  pntlemc 21289  pntlemd 21288  pntlemg 21292
[Shapiro], p. 435Equation 10.6.29pntlema 21290
[Shapiro], p. 436Lemma 10.6.1pntpbnd 21282
[Shapiro], p. 436Lemma 10.6.2pntibnd 21287
[Shapiro], p. 436Equation 10.6.34pntlema 21290
[Shapiro], p. 436Equation 10.6.35pntlem3 21303  pntleml 21305
[Stoll] p. 13Definition of symmetric differencesymdif1 3606
[Stoll] p. 16Exercise 4.40dif 3699  dif0 3698
[Stoll] p. 16Exercise 4.8difdifdir 3715
[Stoll] p. 17Theorem 5.1(5)undifv 3702
[Stoll] p. 19Theorem 5.2(13)undm 3599
[Stoll] p. 19Theorem 5.2(13')indm 3600
[Stoll] p. 20Remarkinvdif 3582
[Stoll] p. 25Definition of ordered tripledf-ot 3824
[Stoll] p. 43Definitionuniiun 4144
[Stoll] p. 44Definitionintiin 4145
[Stoll] p. 45Definitiondf-iin 4096
[Stoll] p. 45Definition indexed uniondf-iun 4095
[Stoll] p. 176Theorem 3.4(27)iman 414
[Stoll] p. 262Example 4.1symdif1 3606
[Strang] p. 242Section 6.3expgrowth 27529
[Suppes] p. 22Theorem 2eq0 3642
[Suppes] p. 22Theorem 4eqss 3363  eqssd 3365  eqssi 3364
[Suppes] p. 23Theorem 5ss0 3658  ss0b 3657
[Suppes] p. 23Theorem 6sstr 3356  sstrALT2 28947
[Suppes] p. 23Theorem 7pssirr 3447
[Suppes] p. 23Theorem 8pssn2lp 3448
[Suppes] p. 23Theorem 9psstr 3451
[Suppes] p. 23Theorem 10pssss 3442
[Suppes] p. 25Theorem 12elin 3530  elun 3488
[Suppes] p. 26Theorem 15inidm 3550
[Suppes] p. 26Theorem 16in0 3653
[Suppes] p. 27Theorem 23unidm 3490
[Suppes] p. 27Theorem 24un0 3652
[Suppes] p. 27Theorem 25ssun1 3510
[Suppes] p. 27Theorem 26ssequn1 3517
[Suppes] p. 27Theorem 27unss 3521
[Suppes] p. 27Theorem 28indir 3589
[Suppes] p. 27Theorem 29undir 3590
[Suppes] p. 28Theorem 32difid 3696  difidALT 3697
[Suppes] p. 29Theorem 33difin 3578
[Suppes] p. 29Theorem 34indif 3583
[Suppes] p. 29Theorem 35undif1 3703
[Suppes] p. 29Theorem 36difun2 3707
[Suppes] p. 29Theorem 37difin0 3701
[Suppes] p. 29Theorem 38disjdif 3700
[Suppes] p. 29Theorem 39difundi 3593
[Suppes] p. 29Theorem 40difindi 3595
[Suppes] p. 30Theorem 41nalset 4340
[Suppes] p. 39Theorem 61uniss 4036
[Suppes] p. 39Theorem 65uniop 4459
[Suppes] p. 41Theorem 70intsn 4086
[Suppes] p. 42Theorem 71intpr 4083  intprg 4084
[Suppes] p. 42Theorem 73op1stb 4758
[Suppes] p. 42Theorem 78intun 4082
[Suppes] p. 44Definition 15(a)dfiun2 4125  dfiun2g 4123
[Suppes] p. 44Definition 15(b)dfiin2 4126
[Suppes] p. 47Theorem 86elpw 3805  elpw2 4364  elpw2g 4363  elpwg 3806  elpwgdedVD 29029
[Suppes] p. 47Theorem 87pwid 3812
[Suppes] p. 47Theorem 89pw0 3945
[Suppes] p. 48Theorem 90pwpw0 3946
[Suppes] p. 52Theorem 101xpss12 4981
[Suppes] p. 52Theorem 102xpindi 5008  xpindir 5009
[Suppes] p. 52Theorem 103xpundi 4930  xpundir 4931
[Suppes] p. 54Theorem 105elirrv 7565
[Suppes] p. 58Theorem 2relss 4963
[Suppes] p. 59Theorem 4eldm 5067  eldm2 5068  eldm2g 5066  eldmg 5065
[Suppes] p. 59Definition 3df-dm 4888
[Suppes] p. 60Theorem 6dmin 5077
[Suppes] p. 60Theorem 8rnun 5280
[Suppes] p. 60Theorem 9rnin 5281
[Suppes] p. 60Definition 4dfrn2 5059
[Suppes] p. 61Theorem 11brcnv 5055  brcnvg 5053
[Suppes] p. 62Equation 5elcnv 5049  elcnv2 5050
[Suppes] p. 62Theorem 12relcnv 5242
[Suppes] p. 62Theorem 15cnvin 5279
[Suppes] p. 62Theorem 16cnvun 5277
[Suppes] p. 63Theorem 20co02 5383
[Suppes] p. 63Theorem 21dmcoss 5135
[Suppes] p. 63Definition 7df-co 4887
[Suppes] p. 64Theorem 26cnvco 5056
[Suppes] p. 64Theorem 27coass 5388
[Suppes] p. 65Theorem 31resundi 5160
[Suppes] p. 65Theorem 34elima 5208  elima2 5209  elima3 5210  elimag 5207
[Suppes] p. 65Theorem 35imaundi 5284
[Suppes] p. 66Theorem 40dminss 5286
[Suppes] p. 66Theorem 41imainss 5287
[Suppes] p. 67Exercise 11cnvxp 5290
[Suppes] p. 81Definition 34dfec2 6908
[Suppes] p. 82Theorem 72elec 6944  elecg 6943
[Suppes] p. 82Theorem 73erth 6949  erth2 6950
[Suppes] p. 83Theorem 74erdisj 6952
[Suppes] p. 89Theorem 96map0b 7052
[Suppes] p. 89Theorem 97map0 7054  map0g 7053
[Suppes] p. 89Theorem 98mapsn 7055
[Suppes] p. 89Theorem 99mapss 7056
[Suppes] p. 91Definition 12(ii)alephsuc 7949
[Suppes] p. 91Definition 12(iii)alephlim 7948
[Suppes] p. 92Theorem 1enref 7140  enrefg 7139
[Suppes] p. 92Theorem 2ensym 7156  ensymb 7155  ensymi 7157
[Suppes] p. 92Theorem 3entr 7159
[Suppes] p. 92Theorem 4unen 7189
[Suppes] p. 94Theorem 15endom 7134
[Suppes] p. 94Theorem 16ssdomg 7153
[Suppes] p. 94Theorem 17domtr 7160
[Suppes] p. 95Theorem 18sbth 7227
[Suppes] p. 97Theorem 23canth2 7260  canth2g 7261
[Suppes] p. 97Definition 3brsdom2 7231  df-sdom 7112  dfsdom2 7230
[Suppes] p. 97Theorem 21(i)sdomirr 7244
[Suppes] p. 97Theorem 22(i)domnsym 7233
[Suppes] p. 97Theorem 21(ii)sdomnsym 7232
[Suppes] p. 97Theorem 22(ii)domsdomtr 7242
[Suppes] p. 97Theorem 22(iv)brdom2 7137
[Suppes] p. 97Theorem 21(iii)sdomtr 7245
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7240
[Suppes] p. 98Exercise 4fundmen 7180  fundmeng 7181
[Suppes] p. 98Exercise 6xpdom3 7206
[Suppes] p. 98Exercise 11sdomentr 7241
[Suppes] p. 104Theorem 37fofi 7392
[Suppes] p. 104Theorem 38pwfi 7402
[Suppes] p. 105Theorem 40pwfi 7402
[Suppes] p. 111Axiom for cardinal numberscarden 8426
[Suppes] p. 130Definition 3df-tr 4303
[Suppes] p. 132Theorem 9ssonuni 4767
[Suppes] p. 134Definition 6df-suc 4587
[Suppes] p. 136Theorem Schema 22findes 4875  finds 4871  finds1 4874  finds2 4873
[Suppes] p. 151Theorem 42isfinite 7607  isfinite2 7365  isfiniteg 7367  unbnn 7363
[Suppes] p. 162Definition 5df-ltnq 8795  df-ltpq 8787
[Suppes] p. 197Theorem Schema 4tfindes 4842  tfinds 4839  tfinds2 4843
[Suppes] p. 209Theorem 18oaord1 6794
[Suppes] p. 209Theorem 21oaword2 6796
[Suppes] p. 211Theorem 25oaass 6804
[Suppes] p. 225Definition 8iscard2 7863
[Suppes] p. 227Theorem 56ondomon 8438
[Suppes] p. 228Theorem 59harcard 7865
[Suppes] p. 228Definition 12(i)aleph0 7947
[Suppes] p. 228Theorem Schema 61onintss 4631
[Suppes] p. 228Theorem Schema 62onminesb 4778  onminsb 4779
[Suppes] p. 229Theorem 64alephval2 8447
[Suppes] p. 229Theorem 65alephcard 7951
[Suppes] p. 229Theorem 66alephord2i 7958
[Suppes] p. 229Theorem 67alephnbtwn 7952
[Suppes] p. 229Definition 12df-aleph 7827
[Suppes] p. 242Theorem 6weth 8375
[Suppes] p. 242Theorem 8entric 8432
[Suppes] p. 242Theorem 9carden 8426
[TakeutiZaring] p. 8Axiom 1ax-ext 2417
[TakeutiZaring] p. 13Definition 4.5df-cleq 2429
[TakeutiZaring] p. 13Proposition 4.6df-clel 2432
[TakeutiZaring] p. 13Proposition 4.9cvjust 2431
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2453
[TakeutiZaring] p. 14Definition 4.16df-oprab 6085
[TakeutiZaring] p. 14Proposition 4.14ru 3160
[TakeutiZaring] p. 15Axiom 2zfpair 4401
[TakeutiZaring] p. 15Exercise 1elpr 3832  elpr2 3833  elprg 3831
[TakeutiZaring] p. 15Exercise 2elsn 3829  elsnc 3837  elsnc2 3843  elsnc2g 3842  elsncg 3836
[TakeutiZaring] p. 15Exercise 3elop 4429
[TakeutiZaring] p. 15Exercise 4sneq 3825  sneqr 3966
[TakeutiZaring] p. 15Definition 5.1dfpr2 3830  dfsn2 3828
[TakeutiZaring] p. 16Axiom 3uniex 4705
[TakeutiZaring] p. 16Exercise 6opth 4435
[TakeutiZaring] p. 16Exercise 7opex 4427
[TakeutiZaring] p. 16Exercise 8rext 4412
[TakeutiZaring] p. 16Corollary 5.8unex 4707  unexg 4710
[TakeutiZaring] p. 16Definition 5.3dftp2 3854
[TakeutiZaring] p. 16Definition 5.5df-uni 4016
[TakeutiZaring] p. 16Definition 5.6df-in 3327  df-un 3325
[TakeutiZaring] p. 16Proposition 5.7unipr 4029  uniprg 4030
[TakeutiZaring] p. 17Axiom 4pwex 4382  pwexg 4383
[TakeutiZaring] p. 17Exercise 1eltp 3853
[TakeutiZaring] p. 17Exercise 5elsuc 4650  elsucg 4648  sstr2 3355
[TakeutiZaring] p. 17Exercise 6uncom 3491
[TakeutiZaring] p. 17Exercise 7incom 3533
[TakeutiZaring] p. 17Exercise 8unass 3504
[TakeutiZaring] p. 17Exercise 9inass 3551
[TakeutiZaring] p. 17Exercise 10indi 3587
[TakeutiZaring] p. 17Exercise 11undi 3588
[TakeutiZaring] p. 17Definition 5.9df-pss 3336  dfss2 3337
[TakeutiZaring] p. 17Definition 5.10df-pw 3801
[TakeutiZaring] p. 18Exercise 7unss2 3518
[TakeutiZaring] p. 18Exercise 9df-ss 3334  sseqin2 3560
[TakeutiZaring] p. 18Exercise 10ssid 3367
[TakeutiZaring] p. 18Exercise 12inss1 3561  inss2 3562
[TakeutiZaring] p. 18Exercise 13nss 3406
[TakeutiZaring] p. 18Exercise 15unieq 4024
[TakeutiZaring] p. 18Exercise 18sspwb 4413  sspwimp 29030  sspwimpALT 29037  sspwimpALT2 29040  sspwimpcf 29032
[TakeutiZaring] p. 18Exercise 19pweqb 4420
[TakeutiZaring] p. 19Axiom 5ax-rep 4320
[TakeutiZaring] p. 20Definitiondf-rab 2714
[TakeutiZaring] p. 20Corollary 5.160ex 4339
[TakeutiZaring] p. 20Definition 5.12df-dif 3323
[TakeutiZaring] p. 20Definition 5.14dfnul2 3630
[TakeutiZaring] p. 20Proposition 5.15difid 3696  difidALT 3697
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3637  n0f 3636  neq0 3638
[TakeutiZaring] p. 21Axiom 6zfreg 7563
[TakeutiZaring] p. 21Axiom 6'zfregs 7668
[TakeutiZaring] p. 21Theorem 5.22setind 7673
[TakeutiZaring] p. 21Definition 5.20df-v 2958
[TakeutiZaring] p. 21Proposition 5.21vprc 4341
[TakeutiZaring] p. 22Exercise 10ss 3656
[TakeutiZaring] p. 22Exercise 3ssex 4347  ssexg 4349
[TakeutiZaring] p. 22Exercise 4inex1 4344
[TakeutiZaring] p. 22Exercise 5ruv 7568
[TakeutiZaring] p. 22Exercise 6elirr 7566
[TakeutiZaring] p. 22Exercise 7ssdif0 3686
[TakeutiZaring] p. 22Exercise 11difdif 3473
[TakeutiZaring] p. 22Exercise 13undif3 3602  undif3VD 28994
[TakeutiZaring] p. 22Exercise 14difss 3474
[TakeutiZaring] p. 22Exercise 15sscon 3481
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2710
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2711
[TakeutiZaring] p. 23Proposition 6.2xpex 4990  xpexg 4989  xpexgALT 6297
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4885
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5513
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5647  fun11 5516
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5466  svrelfun 5514
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5058
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5060
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4890
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4891
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4887
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5325  dfrel2 5321
[TakeutiZaring] p. 25Exercise 3xpss 4982
[TakeutiZaring] p. 25Exercise 5relun 4991
[TakeutiZaring] p. 25Exercise 6reluni 4997
[TakeutiZaring] p. 25Exercise 9inxp 5007
[TakeutiZaring] p. 25Exercise 12relres 5174
[TakeutiZaring] p. 25Exercise 13opelres 5151  opelresg 5153
[TakeutiZaring] p. 25Exercise 14dmres 5167
[TakeutiZaring] p. 25Exercise 15resss 5170
[TakeutiZaring] p. 25Exercise 17resabs1 5175
[TakeutiZaring] p. 25Exercise 18funres 5492
[TakeutiZaring] p. 25Exercise 24relco 5368
[TakeutiZaring] p. 25Exercise 29funco 5491
[TakeutiZaring] p. 25Exercise 30f1co 5648
[TakeutiZaring] p. 26Definition 6.10eu2 2306
[TakeutiZaring] p. 26Definition 6.11conventions 21710  df-fv 5462  fv3 5744
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5406  cnvexg 5405
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5132  dmexg 5130
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5133  rnexg 5131
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27634
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27635
[TakeutiZaring] p. 27Corollary 6.13fvex 5742
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 28014  tz6.12-1 5747  tz6.12-afv 28013  tz6.12 5748  tz6.12c 5750
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5719  tz6.12i 5751
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5457
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5458
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5460  wfo 5452
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5459  wf1 5451
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5461  wf1o 5453
[TakeutiZaring] p. 28Exercise 4eqfnfv 5827  eqfnfv2 5828  eqfnfv2f 5831
[TakeutiZaring] p. 28Exercise 5fvco 5799
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5961  fnexALT 5962
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5957  resfunexgALT 5958
[TakeutiZaring] p. 29Exercise 9funimaex 5531  funimaexg 5530
[TakeutiZaring] p. 29Definition 6.18df-br 4213
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4504
[TakeutiZaring] p. 30Definition 6.21dffr2 4547  dffr3 5236  eliniseg 5233  iniseg 5235
[TakeutiZaring] p. 30Definition 6.22df-eprel 4494
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4560  fr3nr 4760  frirr 4559
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4541
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4762
[TakeutiZaring] p. 31Exercise 1frss 4549
[TakeutiZaring] p. 31Exercise 4wess 4569
[TakeutiZaring] p. 31Proposition 6.26tz6.26 25480  tz6.26i 25481  wefrc 4576  wereu2 4579
[TakeutiZaring] p. 32Theorem 6.27wfi 25482  wfii 25483
[TakeutiZaring] p. 32Definition 6.28df-isom 5463
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6049
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6050
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6056
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6057
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6058
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6062
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6069
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6071
[TakeutiZaring] p. 35Notationwtr 4302
[TakeutiZaring] p. 35Theorem 7.2trelpss 27636  tz7.2 4566
[TakeutiZaring] p. 35Definition 7.1dftr3 4306
[TakeutiZaring] p. 36Proposition 7.4ordwe 4594
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4602
[TakeutiZaring] p. 36Proposition 7.6ordelord 4603  ordelordALT 28622  ordelordALTVD 28979
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4609  ordelssne 4608
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4607
[TakeutiZaring] p. 37Proposition 7.9ordin 4611
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4769
[TakeutiZaring] p. 38Corollary 7.15ordsson 4770
[TakeutiZaring] p. 38Definition 7.11df-on 4585
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4613
[TakeutiZaring] p. 38Proposition 7.12onfrALT 28635  ordon 4763
[TakeutiZaring] p. 38Proposition 7.13onprc 4765
[TakeutiZaring] p. 39Theorem 7.17tfi 4833
[TakeutiZaring] p. 40Exercise 3ontr2 4628
[TakeutiZaring] p. 40Exercise 7dftr2 4304
[TakeutiZaring] p. 40Exercise 9onssmin 4777
[TakeutiZaring] p. 40Exercise 11unon 4811
[TakeutiZaring] p. 40Exercise 12ordun 4683
[TakeutiZaring] p. 40Exercise 14ordequn 4682
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4766
[TakeutiZaring] p. 40Proposition 7.20elssuni 4043
[TakeutiZaring] p. 41Definition 7.22df-suc 4587
[TakeutiZaring] p. 41Proposition 7.23sssucid 4658  sucidg 4659
[TakeutiZaring] p. 41Proposition 7.24suceloni 4793
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4673  ordnbtwn 4672
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4808
[TakeutiZaring] p. 42Exercise 1df-lim 4586
[TakeutiZaring] p. 42Exercise 4omssnlim 4859
[TakeutiZaring] p. 42Exercise 7ssnlim 4863
[TakeutiZaring] p. 42Exercise 8onsucssi 4821  ordelsuc 4800
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4802
[TakeutiZaring] p. 42Definition 7.27nlimon 4831
[TakeutiZaring] p. 42Definition 7.28dfom2 4847
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4864
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4865
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4866
[TakeutiZaring] p. 43Remarkomon 4856
[TakeutiZaring] p. 43Axiom 7inf3 7590  omex 7598
[TakeutiZaring] p. 43Theorem 7.32ordom 4854
[TakeutiZaring] p. 43Corollary 7.31find 4870
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4867
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4868
[TakeutiZaring] p. 44Exercise 1limomss 4850
[TakeutiZaring] p. 44Exercise 2int0 4064  trint0 4319
[TakeutiZaring] p. 44Exercise 4intss1 4065
[TakeutiZaring] p. 44Exercise 5intex 4356
[TakeutiZaring] p. 44Exercise 6oninton 4780
[TakeutiZaring] p. 44Exercise 11ordintdif 4630
[TakeutiZaring] p. 44Definition 7.35df-int 4051
[TakeutiZaring] p. 44Proposition 7.34noinfep 7614
[TakeutiZaring] p. 45Exercise 4onint 4775
[TakeutiZaring] p. 47Lemma 1tfrlem1 6636
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6658
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6659
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6660
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6664  tz7.44-2 6665  tz7.44-3 6666
[TakeutiZaring] p. 50Exercise 1smogt 6629
[TakeutiZaring] p. 50Exercise 3smoiso 6624
[TakeutiZaring] p. 50Definition 7.46df-smo 6608
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6702  tz7.49c 6703
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6700
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6699
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6701
[TakeutiZaring] p. 53Proposition 7.532eu5 2365
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7893
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7894
[TakeutiZaring] p. 56Definition 8.1oalim 6776  oasuc 6768
[TakeutiZaring] p. 57Remarktfindsg 4840
[TakeutiZaring] p. 57Proposition 8.2oacl 6779
[TakeutiZaring] p. 57Proposition 8.3oa0 6760  oa0r 6782
[TakeutiZaring] p. 57Proposition 8.16omcl 6780
[TakeutiZaring] p. 58Corollary 8.5oacan 6791
[TakeutiZaring] p. 58Proposition 8.4nnaord 6862  nnaordi 6861  oaord 6790  oaordi 6789
[TakeutiZaring] p. 59Proposition 8.6iunss2 4136  uniss2 4046
[TakeutiZaring] p. 59Proposition 8.7oawordri 6793
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6798  oawordex 6800
[TakeutiZaring] p. 59Proposition 8.9nnacl 6854
[TakeutiZaring] p. 59Proposition 8.10oaabs 6887
[TakeutiZaring] p. 60Remarkoancom 7606
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6803
[TakeutiZaring] p. 62Exercise 1nnarcl 6859
[TakeutiZaring] p. 62Exercise 5oaword1 6795
[TakeutiZaring] p. 62Definition 8.15om0 6761  om0x 6763  omlim 6777  omsuc 6770
[TakeutiZaring] p. 63Proposition 8.17nnecl 6856  nnmcl 6855
[TakeutiZaring] p. 63Proposition 8.19nnmord 6875  nnmordi 6874  omord 6811  omordi 6809
[TakeutiZaring] p. 63Proposition 8.20omcan 6812
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6879  omwordri 6815
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6783
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6785  om1r 6786
[TakeutiZaring] p. 64Proposition 8.22om00 6818
[TakeutiZaring] p. 64Proposition 8.23omordlim 6820
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6821
[TakeutiZaring] p. 64Proposition 8.25odi 6822
[TakeutiZaring] p. 65Theorem 8.26omass 6823
[TakeutiZaring] p. 67Definition 8.30nnesuc 6851  oe0 6766  oelim 6778  oesuc 6771  onesuc 6774
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6764
[TakeutiZaring] p. 67Proposition 8.32oen0 6829
[TakeutiZaring] p. 67Proposition 8.33oeordi 6830
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6765
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6788
[TakeutiZaring] p. 68Corollary 8.34oeord 6831
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6837
[TakeutiZaring] p. 68Proposition 8.35oewordri 6835
[TakeutiZaring] p. 68Proposition 8.37oeworde 6836
[TakeutiZaring] p. 69Proposition 8.41oeoa 6840
[TakeutiZaring] p. 70Proposition 8.42oeoe 6842
[TakeutiZaring] p. 73Theorem 9.1trcl 7664  tz9.1 7665
[TakeutiZaring] p. 76Definition 9.9df-r1 7690  r10 7694  r1lim 7698  r1limg 7697  r1suc 7696  r1sucg 7695
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7706  r1ord2 7707  r1ordg 7704
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7716
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7741  tz9.13 7717  tz9.13g 7718
[TakeutiZaring] p. 79Definition 9.14df-rank 7691  rankval 7742  rankvalb 7723  rankvalg 7743
[TakeutiZaring] p. 79Proposition 9.16rankel 7765  rankelb 7750
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7779  rankval3 7766  rankval3b 7752
[TakeutiZaring] p. 79Proposition 9.18rankonid 7755
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7721
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7760  rankr1c 7747  rankr1g 7758
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7761
[TakeutiZaring] p. 80Exercise 1rankss 7775  rankssb 7774
[TakeutiZaring] p. 80Exercise 2unbndrank 7768
[TakeutiZaring] p. 80Proposition 9.19bndrank 7767
[TakeutiZaring] p. 83Axiom of Choiceac4 8355  dfac3 8002
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7911  numth 8352  numth2 8351
[TakeutiZaring] p. 85Definition 10.4cardval 8421
[TakeutiZaring] p. 85Proposition 10.5cardid 8422  cardid2 7840
[TakeutiZaring] p. 85Proposition 10.9oncard 7847
[TakeutiZaring] p. 85Proposition 10.10carden 8426
[TakeutiZaring] p. 85Proposition 10.11cardidm 7846
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7831
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7852
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7844
[TakeutiZaring] p. 87Proposition 10.15pwen 7280
[TakeutiZaring] p. 88Exercise 1en0 7170
[TakeutiZaring] p. 88Exercise 7infensuc 7285
[TakeutiZaring] p. 89Exercise 10omxpen 7210
[TakeutiZaring] p. 90Corollary 10.23cardnn 7850
[TakeutiZaring] p. 90Definition 10.27alephiso 7979
[TakeutiZaring] p. 90Proposition 10.20nneneq 7290
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7296
[TakeutiZaring] p. 90Proposition 10.26alephprc 7980
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7295
[TakeutiZaring] p. 91Exercise 2alephle 7969
[TakeutiZaring] p. 91Exercise 3aleph0 7947
[TakeutiZaring] p. 91Exercise 4cardlim 7859
[TakeutiZaring] p. 91Exercise 7infpss 8097
[TakeutiZaring] p. 91Exercise 8infcntss 7380
[TakeutiZaring] p. 91Definition 10.29df-fin 7113  isfi 7131
[TakeutiZaring] p. 92Proposition 10.32onfin 7297
[TakeutiZaring] p. 92Proposition 10.34imadomg 8412
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 7203
[TakeutiZaring] p. 93Proposition 10.35fodomb 8404
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8069  unxpdom 7316
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7861  cardsdomelir 7860
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7318
[TakeutiZaring] p. 94Proposition 10.39infxpen 7896
[TakeutiZaring] p. 95Definition 10.42df-map 7020
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8437  infxpidm2 7898
[TakeutiZaring] p. 95Proposition 10.41infcda 8088  infxp 8095
[TakeutiZaring] p. 96Proposition 10.44pw2en 7215  pw2f1o 7213
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7273
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8367
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8362  ac6s5 8371
[TakeutiZaring] p. 98Theorem 10.47unidom 8418
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8419  uniimadomf 8420
[TakeutiZaring] p. 100Definition 11.1cfcof 8154
[TakeutiZaring] p. 101Proposition 11.7cofsmo 8149
[TakeutiZaring] p. 102Exercise 1cfle 8134
[TakeutiZaring] p. 102Exercise 2cf0 8131
[TakeutiZaring] p. 102Exercise 3cfsuc 8137
[TakeutiZaring] p. 102Exercise 4cfom 8144
[TakeutiZaring] p. 102Proposition 11.9coftr 8153
[TakeutiZaring] p. 103Theorem 11.15alephreg 8457
[TakeutiZaring] p. 103Proposition 11.11cardcf 8132
[TakeutiZaring] p. 103Proposition 11.13alephsing 8156
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7978
[TakeutiZaring] p. 104Proposition 11.16carduniima 7977
[TakeutiZaring] p. 104Proposition 11.18alephfp 7989  alephfp2 7990
[TakeutiZaring] p. 106Theorem 11.20gchina 8574
[TakeutiZaring] p. 106Theorem 11.21mappwen 7993
[TakeutiZaring] p. 107Theorem 11.26konigth 8444
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8458
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8459
[Tarski] p. 67Axiom B5ax-4 2212
[Tarski] p. 67Scheme B5sp 1763
[Tarski] p. 68Lemma 6avril1 21757  equid 1688  equid1 2235  equid1ALT 2253
[Tarski] p. 69Lemma 7equcomi 1691
[Tarski] p. 70Lemma 14spim 1957  spime 1962  spimeh 1679
[Tarski] p. 70Lemma 16ax-11 1761  ax-11o 2218  ax11i 1657
[Tarski] p. 70Lemmas 16 and 17sb6 2175
[Tarski] p. 75Axiom B7ax9v 1667
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1626  ax17o 2234
[Tarski], p. 75Scheme B8 of system S2ax-13 1727  ax-14 1729  ax-8 1687
[Truss] p. 114Theorem 5.18ruc 12842
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 26245
[Viaclovsky8] p. 3Proposition 7ismblfin 26247
[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 2378  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 29039
[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 21710  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 26230
[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 26223
[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 27530
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27531
[WhiteheadRussell] p. 147Theorem *10.2219.26 1603
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27532
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27533
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27534
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1625
[WhiteheadRussell] p. 151Theorem *10.301albitr 27535
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27536
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27537
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27538
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27539
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27541
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27542
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27543
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27540
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2191
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27546
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27547
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27548
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1753
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27549
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27550
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27551
[WhiteheadRussell] p. 162Theorem *11.322alim 27552
[WhiteheadRussell] p. 162Theorem *11.332albi 27553
[WhiteheadRussell] p. 162Theorem *11.342exim 27554
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27556
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27555
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1620
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27558
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27559
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27557
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1582
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27560
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27561
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1590
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27562
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1916
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27563
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27568
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27564
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27565
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27566
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27567
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27572
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27569
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27570
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27571
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27573
[WhiteheadRussell] p. 175Definition *14.02df-eu 2285
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27584  pm13.13b 27585
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27586
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2676
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2677
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3076
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27592
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27593
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27587
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 28639  pm13.193 27588
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27589
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27590
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27591
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27598
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27597
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27596
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3213
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27599  pm14.122b 27600  pm14.122c 27601
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27602  pm14.123b 27603  pm14.123c 27604
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27606
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27605
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27607
[WhiteheadRussell] p. 190Theorem *14.22iota4 5436
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27608
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5437
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27609
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27611
[WhiteheadRussell] p. 192Theorem *14.26eupick 2344  eupickbi 2347  sbaniota 27612
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27610
[WhiteheadRussell] p. 192Theorem *14.271eubi 27613
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27614
[WhiteheadRussell] p. 235Definition *30.01conventions 21710  df-fv 5462
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7887  pm54.43lem 7886
[Young] p. 141Definition of operator orderingleop2 23627
[Young] p. 142Example 12.2(i)0leop 23633  idleop 23634
[vandenDries] p. 42Lemma 61irrapx1 26891
[vandenDries] p. 43Theorem 62pellex 26898  pellexlem1 26892

This page was last updated on 14-Jul-2018.
Copyright terms: Public domain