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 13983
[Adamek] p. 29Proposition 3.14(1)invinv 13997
[Adamek] p. 29Proposition 3.14(2)invco 13998  isoco 14000
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18744  df-nmoo 22248
[AkhiezerGlazman] p. 64Theoremhmopidmch 23658  hmopidmchi 23656
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 23706  pjcmul2i 23707
[AkhiezerGlazman] p. 72Theoremcnvunop 23423  unoplin 23425
[AkhiezerGlazman] p. 72Equation 2unopadj 23424  unopadj2 23443
[AkhiezerGlazman] p. 73Theoremelunop2 23518  lnopunii 23517
[AkhiezerGlazman] p. 80Proposition 1adjlnop 23591
[Apostol] p. 18Theorem I.1addcan 9252  addcan2d 9272  addcan2i 9262  addcand 9271  addcani 9261
[Apostol] p. 18Theorem I.2negeu 9298
[Apostol] p. 18Theorem I.3negsub 9351  negsubd 9419  negsubi 9380
[Apostol] p. 18Theorem I.4negneg 9353  negnegd 9404  negnegi 9372
[Apostol] p. 18Theorem I.5subdi 9469  subdid 9491  subdii 9484  subdir 9470  subdird 9492  subdiri 9485
[Apostol] p. 18Theorem I.6mul01 9247  mul01d 9267  mul01i 9258  mul02 9246  mul02d 9266  mul02i 9257
[Apostol] p. 18Theorem I.7mulcan 9661  mulcan2d 9658  mulcand 9657  mulcani 9663
[Apostol] p. 18Theorem I.8receu 9669  xreceu 24170
[Apostol] p. 18Theorem I.9divrec 9696  divrecd 9795  divreci 9761  divreczi 9754
[Apostol] p. 18Theorem I.10recrec 9713  recreci 9748
[Apostol] p. 18Theorem I.11mul0or 9664  mul0ord 9674  mul0ori 9672
[Apostol] p. 18Theorem I.12mul2neg 9475  mul2negd 9490  mul2negi 9483  mulneg1 9472  mulneg1d 9488  mulneg1i 9481
[Apostol] p. 18Theorem I.13divadddiv 9731  divadddivd 9836  divadddivi 9778
[Apostol] p. 18Theorem I.14divmuldiv 9716  divmuldivd 9833  divmuldivi 9776  rdivmuldivd 24229
[Apostol] p. 18Theorem I.15divdivdiv 9717  divdivdivd 9839  divdivdivi 9779
[Apostol] p. 20Axiom 7rpaddcl 10634  rpaddcld 10665  rpmulcl 10635  rpmulcld 10666
[Apostol] p. 20Axiom 8rpneg 10643
[Apostol] p. 20Axiom 90nrp 10644
[Apostol] p. 20Theorem I.17lttri 9201
[Apostol] p. 20Theorem I.18ltadd1d 9621  ltadd1dd 9639  ltadd1i 9583
[Apostol] p. 20Theorem I.19ltmul1 9862  ltmul1a 9861  ltmul1i 9931  ltmul1ii 9941  ltmul2 9863  ltmul2d 10688  ltmul2dd 10702  ltmul2i 9934
[Apostol] p. 20Theorem I.20msqgt0 9550  msqgt0d 9596  msqgt0i 9566
[Apostol] p. 20Theorem I.210lt1 9552
[Apostol] p. 20Theorem I.23lt0neg1 9536  lt0neg1d 9598  ltneg 9530  ltnegd 9606  ltnegi 9573
[Apostol] p. 20Theorem I.25lt2add 9515  lt2addd 9650  lt2addi 9591
[Apostol] p. 20Definition of positive numbersdf-rp 10615
[Apostol] p. 21Exercise 4recgt0 9856  recgt0d 9947  recgt0i 9917  recgt0ii 9918
[Apostol] p. 22Definition of integersdf-z 10285
[Apostol] p. 22Definition of positive integersdfnn3 10016
[Apostol] p. 22Definition of rationalsdf-q 10577
[Apostol] p. 24Theorem I.26supeu 7461
[Apostol] p. 26Theorem I.28nnunb 10219
[Apostol] p. 26Theorem I.29arch 10220
[Apostol] p. 28Exercise 2btwnz 10374
[Apostol] p. 28Exercise 3nnrecl 10221
[Apostol] p. 28Exercise 4rebtwnz 10575
[Apostol] p. 28Exercise 5zbtwnre 10574
[Apostol] p. 28Exercise 6qbtwnre 10787
[Apostol] p. 28Exercise 10(a)zneo 10354
[Apostol] p. 29Theorem I.35msqsqrd 12244  resqrth 12063  sqrth 12170  sqrthi 12176  sqsqrd 12243
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 10005
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10544
[Apostol] p. 361Remarkcrreczi 11506
[Apostol] p. 363Remarkabsgt0i 12204
[Apostol] p. 363Exampleabssubd 12257  abssubi 12208
[Baer] p. 40Property (b)mapdord 32498
[Baer] p. 40Property (c)mapd11 32499
[Baer] p. 40Property (e)mapdin 32522  mapdlsm 32524
[Baer] p. 40Property (f)mapd0 32525
[Baer] p. 40Definition of projectivitydf-mapd 32485  mapd1o 32508
[Baer] p. 41Property (g)mapdat 32527
[Baer] p. 44Part (1)mapdpg 32566
[Baer] p. 45Part (2)hdmap1eq 32662  mapdheq 32588  mapdheq2 32589  mapdheq2biN 32590
[Baer] p. 45Part (3)baerlem3 32573
[Baer] p. 46Part (4)mapdheq4 32592  mapdheq4lem 32591
[Baer] p. 46Part (5)baerlem5a 32574  baerlem5abmN 32578  baerlem5amN 32576  baerlem5b 32575  baerlem5bmN 32577
[Baer] p. 47Part (6)hdmap1l6 32682  hdmap1l6a 32670  hdmap1l6e 32675  hdmap1l6f 32676  hdmap1l6g 32677  hdmap1l6lem1 32668  hdmap1l6lem2 32669  hdmap1p6N 32683  mapdh6N 32607  mapdh6aN 32595  mapdh6eN 32600  mapdh6fN 32601  mapdh6gN 32602  mapdh6lem1N 32593  mapdh6lem2N 32594
[Baer] p. 48Part 9hdmapval 32691
[Baer] p. 48Part 10hdmap10 32703
[Baer] p. 48Part 11hdmapadd 32706
[Baer] p. 48Part (6)hdmap1l6h 32678  mapdh6hN 32603
[Baer] p. 48Part (7)mapdh75cN 32613  mapdh75d 32614  mapdh75e 32612  mapdh75fN 32615  mapdh7cN 32609  mapdh7dN 32610  mapdh7eN 32608  mapdh7fN 32611
[Baer] p. 48Part (8)mapdh8 32649  mapdh8a 32635  mapdh8aa 32636  mapdh8ab 32637  mapdh8ac 32638  mapdh8ad 32639  mapdh8b 32640  mapdh8c 32641  mapdh8d 32643  mapdh8d0N 32642  mapdh8e 32644  mapdh8fN 32645  mapdh8g 32646  mapdh8i 32647  mapdh8j 32648
[Baer] p. 48Part (9)mapdh9a 32650
[Baer] p. 48Equation 10mapdhvmap 32629
[Baer] p. 49Part 12hdmap11 32711  hdmapeq0 32707  hdmapf1oN 32728  hdmapneg 32709  hdmaprnN 32727  hdmaprnlem1N 32712  hdmaprnlem3N 32713  hdmaprnlem3uN 32714  hdmaprnlem4N 32716  hdmaprnlem6N 32717  hdmaprnlem7N 32718  hdmaprnlem8N 32719  hdmaprnlem9N 32720  hdmapsub 32710
[Baer] p. 49Part 14hdmap14lem1 32731  hdmap14lem10 32740  hdmap14lem1a 32729  hdmap14lem2N 32732  hdmap14lem2a 32730  hdmap14lem3 32733  hdmap14lem8 32738  hdmap14lem9 32739
[Baer] p. 50Part 14hdmap14lem11 32741  hdmap14lem12 32742  hdmap14lem13 32743  hdmap14lem14 32744  hdmap14lem15 32745  hgmapval 32750
[Baer] p. 50Part 15hgmapadd 32757  hgmapmul 32758  hgmaprnlem2N 32760  hgmapvs 32754
[Baer] p. 50Part 16hgmaprnN 32764
[Baer] p. 110Lemma 1hdmapip0com 32780
[Baer] p. 110Line 27hdmapinvlem1 32781
[Baer] p. 110Line 28hdmapinvlem2 32782
[Baer] p. 110Line 30hdmapinvlem3 32783
[Baer] p. 110Part 1.2hdmapglem5 32785  hgmapvv 32789
[Baer] p. 110Proposition 1hdmapinvlem4 32784
[Baer] p. 111Line 10hgmapvvlem1 32786
[Baer] p. 111Line 15hdmapg 32793  hdmapglem7 32792
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2287
[BellMachover] p. 460Notationdf-mo 2288
[BellMachover] p. 460Definitionmo3 2314
[BellMachover] p. 461Axiom Extax-ext 2419
[BellMachover] p. 462Theorem 1.1bm1.1 2423
[BellMachover] p. 463Axiom Repaxrep5 4327
[BellMachover] p. 463Scheme Sepaxsep 4331
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4335
[BellMachover] p. 466Axiom Powaxpow3 4382
[BellMachover] p. 466Axiom Unionaxun2 4705
[BellMachover] p. 468Definitiondf-ord 4586
[BellMachover] p. 469Theorem 2.2(i)ordirr 4601
[BellMachover] p. 469Theorem 2.2(iii)onelon 4608
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4603
[BellMachover] p. 471Definition of Ndf-om 4848
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4788
[BellMachover] p. 471Definition of Limdf-lim 4588
[BellMachover] p. 472Axiom Infzfinf2 7599
[BellMachover] p. 473Theorem 2.8limom 4862
[BellMachover] p. 477Equation 3.1df-r1 7692
[BellMachover] p. 478Definitionrankval2 7746
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7710  r1ord3g 7707
[BellMachover] p. 480Axiom Regzfreg2 7566
[BellMachover] p. 488Axiom ACac5 8359  dfac4 8005
[BellMachover] p. 490Definition of alephalephval3 7993
[BeltramettiCassinelli] p. 98Remarkatlatmstc 30179
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 23858
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 23900  chirredi 23899
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 23888
[Beran] p. 3Definition of joinsshjval3 22858
[Beran] p. 39Theorem 2.3(i)cmcm2 23120  cmcm2i 23097  cmcm2ii 23102  cmt2N 30110
[Beran] p. 40Theorem 2.3(iii)lecm 23121  lecmi 23106  lecmii 23107
[Beran] p. 45Theorem 3.4cmcmlem 23095
[Beran] p. 49Theorem 4.2cm2j 23124  cm2ji 23129  cm2mi 23130
[Beran] p. 95Definitiondf-sh 22711  issh2 22713
[Beran] p. 95Lemma 3.1(S5)his5 22590
[Beran] p. 95Lemma 3.1(S6)his6 22603
[Beran] p. 95Lemma 3.1(S7)his7 22594
[Beran] p. 95Lemma 3.2(S8)ho01i 23333
[Beran] p. 95Lemma 3.2(S9)hoeq1 23335
[Beran] p. 95Lemma 3.2(S10)ho02i 23334
[Beran] p. 95Lemma 3.2(S11)hoeq2 23336
[Beran] p. 95Postulate (S1)ax-his1 22586  his1i 22604
[Beran] p. 95Postulate (S2)ax-his2 22587
[Beran] p. 95Postulate (S3)ax-his3 22588
[Beran] p. 95Postulate (S4)ax-his4 22589
[Beran] p. 96Definition of normdf-hnorm 22473  dfhnorm2 22626  normval 22628
[Beran] p. 96Definition for Cauchy sequencehcau 22688
[Beran] p. 96Definition of Cauchy sequencedf-hcau 22478
[Beran] p. 96Definition of complete subspaceisch3 22746
[Beran] p. 96Definition of convergedf-hlim 22477  hlimi 22692
[Beran] p. 97Theorem 3.3(i)norm-i-i 22637  norm-i 22633
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 22641  norm-ii 22642  normlem0 22613  normlem1 22614  normlem2 22615  normlem3 22616  normlem4 22617  normlem5 22618  normlem6 22619  normlem7 22620  normlem7tALT 22623
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 22643  norm-iii 22644
[Beran] p. 98Remark 3.4bcs 22685  bcsiALT 22683  bcsiHIL 22684
[Beran] p. 98Remark 3.4(B)normlem9at 22625  normpar 22659  normpari 22658
[Beran] p. 98Remark 3.4(C)normpyc 22650  normpyth 22649  normpythi 22646
[Beran] p. 99Remarklnfn0 23552  lnfn0i 23547  lnop0 23471  lnop0i 23475
[Beran] p. 99Theorem 3.5(i)nmcexi 23531  nmcfnex 23558  nmcfnexi 23556  nmcopex 23534  nmcopexi 23532
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 23559  nmcfnlbi 23557  nmcoplb 23535  nmcoplbi 23533
[Beran] p. 99Theorem 3.5(iii)lnfncon 23561  lnfnconi 23560  lnopcon 23540  lnopconi 23539
[Beran] p. 100Lemma 3.6normpar2i 22660
[Beran] p. 101Lemma 3.6norm3adifi 22657  norm3adifii 22652  norm3dif 22654  norm3difi 22651
[Beran] p. 102Theorem 3.7(i)chocunii 22805  pjhth 22897  pjhtheu 22898  pjpjhth 22929  pjpjhthi 22930  pjth 19342
[Beran] p. 102Theorem 3.7(ii)ococ 22910  ococi 22909
[Beran] p. 103Remark 3.8nlelchi 23566
[Beran] p. 104Theorem 3.9riesz3i 23567  riesz4 23569  riesz4i 23568
[Beran] p. 104Theorem 3.10cnlnadj 23584  cnlnadjeu 23583  cnlnadjeui 23582  cnlnadji 23581  cnlnadjlem1 23572  nmopadjlei 23593
[Beran] p. 106Theorem 3.11(i)adjeq0 23596
[Beran] p. 106Theorem 3.11(v)nmopadji 23595
[Beran] p. 106Theorem 3.11(ii)adjmul 23597
[Beran] p. 106Theorem 3.11(iv)adjadj 23441
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 23607  nmopcoadji 23606
[Beran] p. 106Theorem 3.11(iii)adjadd 23598
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 23608
[Beran] p. 106Theorem 3.11(viii)adjcoi 23605  pjadj2coi 23709  pjadjcoi 23666
[Beran] p. 107Definitiondf-ch 22726  isch2 22728
[Beran] p. 107Remark 3.12choccl 22810  isch3 22746  occl 22808  ocsh 22787  shoccl 22809  shocsh 22788
[Beran] p. 107Remark 3.12(B)ococin 22912
[Beran] p. 108Theorem 3.13chintcl 22836
[Beran] p. 109Property (i)pjadj2 23692  pjadj3 23693  pjadji 23189  pjadjii 23178
[Beran] p. 109Property (ii)pjidmco 23686  pjidmcoi 23682  pjidmi 23177
[Beran] p. 110Definition of projector orderingpjordi 23678
[Beran] p. 111Remarkho0val 23255  pjch1 23174
[Beran] p. 111Definitiondf-hfmul 23239  df-hfsum 23238  df-hodif 23237  df-homul 23236  df-hosum 23235
[Beran] p. 111Lemma 4.4(i)pjo 23175
[Beran] p. 111Lemma 4.4(ii)pjch 23198  pjchi 22936
[Beran] p. 111Lemma 4.4(iii)pjoc2 22943  pjoc2i 22942
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 23184
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 23670  pjssmii 23185
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 23669
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 23668
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 23673
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 23671  pjssge0ii 23186
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 23672  pjdifnormii 23187
[Bogachev] p. 116Definition 2.3.1df-itgm 24666  df-sitm 24648
[Bogachev] p. 118Chapter 2.4.4df-itgm 24666
[Bogachev] p. 118Definition 2.4.1df-sitg 24647
[Bollobas] p. 4Definitiondf-wlk 21518
[Bollobas] p. 5Notationdf-pth 21520
[Bollobas] p. 5Definitiondf-crct 21522  df-cycl 21523  df-trail 21519  df-wlkon 21524
[BourbakiEns] p. Proposition 8fcof1 6022  fcofo 6023
[BourbakiTop1] p. Remarkxnegmnf 10798  xnegpnf 10797
[BourbakiTop1] p. Remark rexneg 10799
[BourbakiTop1] p. Theoremneiss 17175
[BourbakiTop1] p. Remark 3ust0 18251  ustfilxp 18244
[BourbakiTop1] p. Axiom GT'tgpsubcn 18122
[BourbakiTop1] p. Example 1cstucnd 18316  iducn 18315  snfil 17898
[BourbakiTop1] p. Example 2neifil 17914
[BourbakiTop1] p. Theorem 1cnextcn 18100
[BourbakiTop1] p. Theorem 2ucnextcn 18336
[BourbakiTop1] p. Theorem 3df-hcmp 24343
[BourbakiTop1] p. Definitionistgp 18109
[BourbakiTop1] p. Propositioncnpco 17333  ishmeo 17793  neips 17179
[BourbakiTop1] p. Definition 1df-ucn 18308  df-ust 18232  filintn0 17895  ucnprima 18314
[BourbakiTop1] p. Definition 2df-cfilu 18319
[BourbakiTop1] p. Definition 3df-cusp 18330  df-usp 18289  df-utop 18263  trust 18261
[BourbakiTop1] p. Condition F_Iustssel 18237
[BourbakiTop1] p. Condition U_Iustdiag 18240
[BourbakiTop1] p. Property V_ivneiptopreu 17199
[BourbakiTop1] p. Proposition 1ucncn 18317  ustund 18253  ustuqtop 18278
[BourbakiTop1] p. Proposition 2neiptopreu 17199  utop2nei 18282  utop3cls 18283
[BourbakiTop1] p. Proposition 3fmucnd 18324  uspreg 18306  utopreg 18284
[BourbakiTop1] p. Proposition 4imasncld 17725  imasncls 17726  imasnopn 17724
[BourbakiTop1] p. Proposition 9cnpflf2 18034
[BourbakiTop1] p. Theorem 1 (d)iscncl 17335
[BourbakiTop1] p. Condition F_IIustincl 18239
[BourbakiTop1] p. Condition U_IIustinvel 18241
[BourbakiTop1] p. Proposition 11cnextucn 18335
[BourbakiTop1] p. Proposition Vissnei2 17182
[BourbakiTop1] p. Condition F_IIbustbasel 18238
[BourbakiTop1] p. Condition U_IIIustexhalf 18242
[BourbakiTop1] p. Definition C'''df-cmp 17452
[BourbakiTop1] p. Proposition Viiinnei 17191
[BourbakiTop1] p. Proposition Vivneissex 17193
[BourbakiTop1] p. Proposition Viiielnei 17177  ssnei 17176
[BourbakiTop1] p. Remark below def. 1filn0 17896
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17880
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17897
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 27789
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27791  stoweid 27790
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27728  stoweidlem10 27737  stoweidlem14 27741  stoweidlem15 27742  stoweidlem35 27762  stoweidlem36 27763  stoweidlem37 27764  stoweidlem38 27765  stoweidlem40 27767  stoweidlem41 27768  stoweidlem43 27770  stoweidlem44 27771  stoweidlem46 27773  stoweidlem5 27732  stoweidlem50 27777  stoweidlem52 27779  stoweidlem53 27780  stoweidlem55 27782  stoweidlem56 27783
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27750  stoweidlem24 27751  stoweidlem27 27754  stoweidlem28 27755  stoweidlem30 27757
[BrosowskiDeutsh] p. 91Proofstoweidlem34 27761  stoweidlem59 27786  stoweidlem60 27787
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27772  stoweidlem49 27776  stoweidlem7 27734
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27758  stoweidlem39 27766  stoweidlem42 27769  stoweidlem48 27775  stoweidlem51 27778  stoweidlem54 27781  stoweidlem57 27784  stoweidlem58 27785
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27752
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27744
[BrosowskiDeutsh] p. 92Proofstoweidlem11 27738  stoweidlem13 27740  stoweidlem26 27753  stoweidlem61 27788
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27745
[ChoquetDD] p. 2Definition of mappingdf-mpt 4270
[Clemente] p. 10Definition ITnatded 21713
[Clemente] p. 10Definition I` `m,nnatded 21713
[Clemente] p. 11Definition E=>m,nnatded 21713
[Clemente] p. 11Definition I=>m,nnatded 21713
[Clemente] p. 11Definition E` `(1)natded 21713
[Clemente] p. 11Definition E` `(2)natded 21713
[Clemente] p. 12Definition E` `m,n,pnatded 21713
[Clemente] p. 12Definition I` `n(1)natded 21713
[Clemente] p. 12Definition I` `n(2)natded 21713
[Clemente] p. 13Definition I` `m,n,pnatded 21713
[Clemente] p. 14Proof 5.11natded 21713
[Clemente] p. 14Definition E` `nnatded 21713
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 21715  ex-natded5.2 21714
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 21718  ex-natded5.3 21717
[Clemente] p. 18Theorem 5.5ex-natded5.5 21720
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 21722  ex-natded5.7 21721
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 21724  ex-natded5.8 21723
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 21726  ex-natded5.13 21725
[Clemente] p. 32Definition I` `nnatded 21713
[Clemente] p. 32Definition E` `m,n,p,anatded 21713
[Clemente] p. 32Definition E` `n,tnatded 21713
[Clemente] p. 32Definition I` `n,tnatded 21713
[Clemente] p. 43Theorem 9.20ex-natded9.20 21727
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 21728
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 21730  ex-natded9.26 21729
[Cohen] p. 301Remarkrelogoprlem 20487
[Cohen] p. 301Property 2relogmul 20488  relogmuld 20522
[Cohen] p. 301Property 3relogdiv 20489  relogdivd 20523
[Cohen] p. 301Property 4relogexp 20492
[Cohen] p. 301Property 1alog1 20482
[Cohen] p. 301Property 1bloge 20483
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 24637  sxbrsigalem4 24639
[Cohn] p. 81Section II.5acsdomd 14609  acsinfd 14608  acsinfdimd 14610  acsmap2d 14607  acsmapd 14606
[Cohn] p. 143Example 5.1.1sxbrsiga 24642
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 11244
[Crawley] p. 1Definition of posetdf-poset 14405
[Crawley] p. 107Theorem 13.2hlsupr 30245
[Crawley] p. 110Theorem 13.3arglem1N 31049  dalaw 30745
[Crawley] p. 111Theorem 13.4hlathil 32824
[Crawley] p. 111Definition of set Wdf-watsN 30849
[Crawley] p. 111Definition of dilationdf-dilN 30965  df-ldil 30963  isldil 30969
[Crawley] p. 111Definition of translationdf-ltrn 30964  df-trnN 30966  isltrn 30978  ltrnu 30980
[Crawley] p. 112Lemma Acdlema1N 30650  cdlema2N 30651  exatleN 30263
[Crawley] p. 112Lemma B1cvrat 30335  cdlemb 30653  cdlemb2 30900  cdlemb3 31465  idltrn 31009  l1cvat 29915  lhpat 30902  lhpat2 30904  lshpat 29916  ltrnel 30998  ltrnmw 31010
[Crawley] p. 112Lemma Ccdlemc1 31050  cdlemc2 31051  ltrnnidn 31033  trlat 31028  trljat1 31025  trljat2 31026  trljat3 31027  trlne 31044  trlnidat 31032  trlnle 31045
[Crawley] p. 112Definition of automorphismdf-pautN 30850
[Crawley] p. 113Lemma Ccdlemc 31056  cdlemc3 31052  cdlemc4 31053
[Crawley] p. 113Lemma Dcdlemd 31066  cdlemd1 31057  cdlemd2 31058  cdlemd3 31059  cdlemd4 31060  cdlemd5 31061  cdlemd6 31062  cdlemd7 31063  cdlemd8 31064  cdlemd9 31065  cdleme31sde 31244  cdleme31se 31241  cdleme31se2 31242  cdleme31snd 31245  cdleme32a 31300  cdleme32b 31301  cdleme32c 31302  cdleme32d 31303  cdleme32e 31304  cdleme32f 31305  cdleme32fva 31296  cdleme32fva1 31297  cdleme32fvcl 31299  cdleme32le 31306  cdleme48fv 31358  cdleme4gfv 31366  cdleme50eq 31400  cdleme50f 31401  cdleme50f1 31402  cdleme50f1o 31405  cdleme50laut 31406  cdleme50ldil 31407  cdleme50lebi 31399  cdleme50rn 31404  cdleme50rnlem 31403  cdlemeg49le 31370  cdlemeg49lebilem 31398
[Crawley] p. 113Lemma Ecdleme 31419  cdleme00a 31068  cdleme01N 31080  cdleme02N 31081  cdleme0a 31070  cdleme0aa 31069  cdleme0b 31071  cdleme0c 31072  cdleme0cp 31073  cdleme0cq 31074  cdleme0dN 31075  cdleme0e 31076  cdleme0ex1N 31082  cdleme0ex2N 31083  cdleme0fN 31077  cdleme0gN 31078  cdleme0moN 31084  cdleme1 31086  cdleme10 31113  cdleme10tN 31117  cdleme11 31129  cdleme11a 31119  cdleme11c 31120  cdleme11dN 31121  cdleme11e 31122  cdleme11fN 31123  cdleme11g 31124  cdleme11h 31125  cdleme11j 31126  cdleme11k 31127  cdleme11l 31128  cdleme12 31130  cdleme13 31131  cdleme14 31132  cdleme15 31137  cdleme15a 31133  cdleme15b 31134  cdleme15c 31135  cdleme15d 31136  cdleme16 31144  cdleme16aN 31118  cdleme16b 31138  cdleme16c 31139  cdleme16d 31140  cdleme16e 31141  cdleme16f 31142  cdleme16g 31143  cdleme19a 31162  cdleme19b 31163  cdleme19c 31164  cdleme19d 31165  cdleme19e 31166  cdleme19f 31167  cdleme1b 31085  cdleme2 31087  cdleme20aN 31168  cdleme20bN 31169  cdleme20c 31170  cdleme20d 31171  cdleme20e 31172  cdleme20f 31173  cdleme20g 31174  cdleme20h 31175  cdleme20i 31176  cdleme20j 31177  cdleme20k 31178  cdleme20l 31181  cdleme20l1 31179  cdleme20l2 31180  cdleme20m 31182  cdleme20y 31161  cdleme20zN 31160  cdleme21 31196  cdleme21d 31189  cdleme21e 31190  cdleme22a 31199  cdleme22aa 31198  cdleme22b 31200  cdleme22cN 31201  cdleme22d 31202  cdleme22e 31203  cdleme22eALTN 31204  cdleme22f 31205  cdleme22f2 31206  cdleme22g 31207  cdleme23a 31208  cdleme23b 31209  cdleme23c 31210  cdleme26e 31218  cdleme26eALTN 31220  cdleme26ee 31219  cdleme26f 31222  cdleme26f2 31224  cdleme26f2ALTN 31223  cdleme26fALTN 31221  cdleme27N 31228  cdleme27a 31226  cdleme27cl 31225  cdleme28c 31231  cdleme3 31096  cdleme30a 31237  cdleme31fv 31249  cdleme31fv1 31250  cdleme31fv1s 31251  cdleme31fv2 31252  cdleme31id 31253  cdleme31sc 31243  cdleme31sdnN 31246  cdleme31sn 31239  cdleme31sn1 31240  cdleme31sn1c 31247  cdleme31sn2 31248  cdleme31so 31238  cdleme35a 31307  cdleme35b 31309  cdleme35c 31310  cdleme35d 31311  cdleme35e 31312  cdleme35f 31313  cdleme35fnpq 31308  cdleme35g 31314  cdleme35h 31315  cdleme35h2 31316  cdleme35sn2aw 31317  cdleme35sn3a 31318  cdleme36a 31319  cdleme36m 31320  cdleme37m 31321  cdleme38m 31322  cdleme38n 31323  cdleme39a 31324  cdleme39n 31325  cdleme3b 31088  cdleme3c 31089  cdleme3d 31090  cdleme3e 31091  cdleme3fN 31092  cdleme3fa 31095  cdleme3g 31093  cdleme3h 31094  cdleme4 31097  cdleme40m 31326  cdleme40n 31327  cdleme40v 31328  cdleme40w 31329  cdleme41fva11 31336  cdleme41sn3aw 31333  cdleme41sn4aw 31334  cdleme41snaw 31335  cdleme42a 31330  cdleme42b 31337  cdleme42c 31331  cdleme42d 31332  cdleme42e 31338  cdleme42f 31339  cdleme42g 31340  cdleme42h 31341  cdleme42i 31342  cdleme42k 31343  cdleme42ke 31344  cdleme42keg 31345  cdleme42mN 31346  cdleme42mgN 31347  cdleme43aN 31348  cdleme43bN 31349  cdleme43cN 31350  cdleme43dN 31351  cdleme5 31099  cdleme50ex 31418  cdleme50ltrn 31416  cdleme51finvN 31415  cdleme51finvfvN 31414  cdleme51finvtrN 31417  cdleme6 31100  cdleme7 31108  cdleme7a 31102  cdleme7aa 31101  cdleme7b 31103  cdleme7c 31104  cdleme7d 31105  cdleme7e 31106  cdleme7ga 31107  cdleme8 31109  cdleme8tN 31114  cdleme9 31112  cdleme9a 31110  cdleme9b 31111  cdleme9tN 31116  cdleme9taN 31115  cdlemeda 31157  cdlemedb 31156  cdlemednpq 31158  cdlemednuN 31159  cdlemefr27cl 31262  cdlemefr32fva1 31269  cdlemefr32fvaN 31268  cdlemefrs32fva 31259  cdlemefrs32fva1 31260  cdlemefs27cl 31272  cdlemefs32fva1 31282  cdlemefs32fvaN 31281  cdlemesner 31155  cdlemeulpq 31079
[Crawley] p. 114Lemma E4atex 30935  4atexlem7 30934  cdleme0nex 31149  cdleme17a 31145  cdleme17c 31147  cdleme17d 31357  cdleme17d1 31148  cdleme17d2 31354  cdleme18a 31150  cdleme18b 31151  cdleme18c 31152  cdleme18d 31154  cdleme4a 31098
[Crawley] p. 115Lemma Ecdleme21a 31184  cdleme21at 31187  cdleme21b 31185  cdleme21c 31186  cdleme21ct 31188  cdleme21f 31191  cdleme21g 31192  cdleme21h 31193  cdleme21i 31194  cdleme22gb 31153
[Crawley] p. 116Lemma Fcdlemf 31422  cdlemf1 31420  cdlemf2 31421
[Crawley] p. 116Lemma Gcdlemftr1 31426  cdlemg16 31516  cdlemg28 31563  cdlemg28a 31552  cdlemg28b 31562  cdlemg3a 31456  cdlemg42 31588  cdlemg43 31589  cdlemg44 31592  cdlemg44a 31590  cdlemg46 31594  cdlemg47 31595  cdlemg9 31493  ltrnco 31578  ltrncom 31597  tgrpabl 31610  trlco 31586
[Crawley] p. 116Definition of Gdf-tgrp 31602
[Crawley] p. 117Lemma Gcdlemg17 31536  cdlemg17b 31521
[Crawley] p. 117Definition of Edf-edring-rN 31615  df-edring 31616
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 31619
[Crawley] p. 118Remarktendopltp 31639
[Crawley] p. 118Lemma Hcdlemh 31676  cdlemh1 31674  cdlemh2 31675
[Crawley] p. 118Lemma Icdlemi 31679  cdlemi1 31677  cdlemi2 31678
[Crawley] p. 118Lemma Jcdlemj1 31680  cdlemj2 31681  cdlemj3 31682  tendocan 31683
[Crawley] p. 118Lemma Kcdlemk 31833  cdlemk1 31690  cdlemk10 31702  cdlemk11 31708  cdlemk11t 31805  cdlemk11ta 31788  cdlemk11tb 31790  cdlemk11tc 31804  cdlemk11u-2N 31748  cdlemk11u 31730  cdlemk12 31709  cdlemk12u-2N 31749  cdlemk12u 31731  cdlemk13-2N 31735  cdlemk13 31711  cdlemk14-2N 31737  cdlemk14 31713  cdlemk15-2N 31738  cdlemk15 31714  cdlemk16-2N 31739  cdlemk16 31716  cdlemk16a 31715  cdlemk17-2N 31740  cdlemk17 31717  cdlemk18-2N 31745  cdlemk18-3N 31759  cdlemk18 31727  cdlemk19-2N 31746  cdlemk19 31728  cdlemk19u 31829  cdlemk1u 31718  cdlemk2 31691  cdlemk20-2N 31751  cdlemk20 31733  cdlemk21-2N 31750  cdlemk21N 31732  cdlemk22-3 31760  cdlemk22 31752  cdlemk23-3 31761  cdlemk24-3 31762  cdlemk25-3 31763  cdlemk26-3 31765  cdlemk26b-3 31764  cdlemk27-3 31766  cdlemk28-3 31767  cdlemk29-3 31770  cdlemk3 31692  cdlemk30 31753  cdlemk31 31755  cdlemk32 31756  cdlemk33N 31768  cdlemk34 31769  cdlemk35 31771  cdlemk36 31772  cdlemk37 31773  cdlemk38 31774  cdlemk39 31775  cdlemk39u 31827  cdlemk4 31693  cdlemk41 31779  cdlemk42 31800  cdlemk42yN 31803  cdlemk43N 31822  cdlemk45 31806  cdlemk46 31807  cdlemk47 31808  cdlemk48 31809  cdlemk49 31810  cdlemk5 31695  cdlemk50 31811  cdlemk51 31812  cdlemk52 31813  cdlemk53 31816  cdlemk54 31817  cdlemk55 31820  cdlemk55u 31825  cdlemk56 31830  cdlemk5a 31694  cdlemk5auN 31719  cdlemk5u 31720  cdlemk6 31696  cdlemk6u 31721  cdlemk7 31707  cdlemk7u-2N 31747  cdlemk7u 31729  cdlemk8 31697  cdlemk9 31698  cdlemk9bN 31699  cdlemki 31700  cdlemkid 31795  cdlemkj-2N 31741  cdlemkj 31722  cdlemksat 31705  cdlemksel 31704  cdlemksv 31703  cdlemksv2 31706  cdlemkuat 31725  cdlemkuel-2N 31743  cdlemkuel-3 31757  cdlemkuel 31724  cdlemkuv-2N 31742  cdlemkuv2-2 31744  cdlemkuv2-3N 31758  cdlemkuv2 31726  cdlemkuvN 31723  cdlemkvcl 31701  cdlemky 31785  cdlemkyyN 31821  tendoex 31834
[Crawley] p. 120Remarkdva1dim 31844
[Crawley] p. 120Lemma Lcdleml1N 31835  cdleml2N 31836  cdleml3N 31837  cdleml4N 31838  cdleml5N 31839  cdleml6 31840  cdleml7 31841  cdleml8 31842  cdleml9 31843  dia1dim 31921
[Crawley] p. 120Lemma Mdia11N 31908  diaf11N 31909  dialss 31906  diaord 31907  dibf11N 32021  djajN 31997
[Crawley] p. 120Definition of isomorphism mapdiaval 31892
[Crawley] p. 121Lemma Mcdlemm10N 31978  dia2dimlem1 31924  dia2dimlem2 31925  dia2dimlem3 31926  dia2dimlem4 31927  dia2dimlem5 31928  diaf1oN 31990  diarnN 31989  dvheveccl 31972  dvhopN 31976
[Crawley] p. 121Lemma Ncdlemn 32072  cdlemn10 32066  cdlemn11 32071  cdlemn11a 32067  cdlemn11b 32068  cdlemn11c 32069  cdlemn11pre 32070  cdlemn2 32055  cdlemn2a 32056  cdlemn3 32057  cdlemn4 32058  cdlemn4a 32059  cdlemn5 32061  cdlemn5pre 32060  cdlemn6 32062  cdlemn7 32063  cdlemn8 32064  cdlemn9 32065  diclspsn 32054
[Crawley] p. 121Definition of phi(q)df-dic 32033
[Crawley] p. 122Lemma Ndih11 32125  dihf11 32127  dihjust 32077  dihjustlem 32076  dihord 32124  dihord1 32078  dihord10 32083  dihord11b 32082  dihord11c 32084  dihord2 32087  dihord2a 32079  dihord2b 32080  dihord2cN 32081  dihord2pre 32085  dihord2pre2 32086  dihordlem6 32073  dihordlem7 32074  dihordlem7b 32075
[Crawley] p. 122Definition of isomorphism mapdihffval 32090  dihfval 32091  dihval 32092
[Eisenberg] p. 67Definition 5.3df-dif 3325
[Eisenberg] p. 82Definition 6.3dfom3 7604
[Eisenberg] p. 125Definition 8.21df-map 7022
[Eisenberg] p. 216Example 13.2(4)omenps 7611
[Eisenberg] p. 310Theorem 19.8cardprc 7869
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8432
[Enderton] p. 18Axiom of Empty Setaxnul 4339
[Enderton] p. 19Definitiondf-tp 3824
[Enderton] p. 26Exercise 5unissb 4047
[Enderton] p. 26Exercise 10pwel 4417
[Enderton] p. 28Exercise 7(b)pwun 4493
[Enderton] p. 30Theorem "Distributive laws"iinin1 4164  iinin2 4163  iinun2 4159  iunin1 4158  iunin2 4157
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4162  iundif2 4160
[Enderton] p. 32Exercise 20unineq 3593
[Enderton] p. 33Exercise 23iinuni 4176
[Enderton] p. 33Exercise 25iununi 4177
[Enderton] p. 33Exercise 24(a)iinpw 4181
[Enderton] p. 33Exercise 24(b)iunpw 4761  iunpwss 4182
[Enderton] p. 36Definitionopthwiener 4460
[Enderton] p. 38Exercise 6(a)unipw 4416
[Enderton] p. 38Exercise 6(b)pwuni 4397
[Enderton] p. 41Lemma 3Dopeluu 4717  rnex 5135  rnexg 5133
[Enderton] p. 41Exercise 8dmuni 5081  rnuni 5285
[Enderton] p. 42Definition of a functiondffun7 5481  dffun8 5482
[Enderton] p. 43Definition of function valuefunfv2 5793
[Enderton] p. 43Definition of single-rootedfuncnv 5513
[Enderton] p. 44Definition (d)dfima2 5207  dfima3 5208
[Enderton] p. 47Theorem 3Hfvco2 5800
[Enderton] p. 49Axiom of Choice (first form)ac7 8355  ac7g 8356  df-ac 7999  dfac2 8013  dfac2a 8012  dfac3 8004  dfac7 8014
[Enderton] p. 50Theorem 3K(a)imauni 5995
[Enderton] p. 52Definitiondf-map 7022
[Enderton] p. 53Exercise 21coass 5390
[Enderton] p. 53Exercise 27dmco 5380
[Enderton] p. 53Exercise 14(a)funin 5522
[Enderton] p. 53Exercise 22(a)imass2 5242
[Enderton] p. 54Remarkixpf 7086  ixpssmap 7098
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7066
[Enderton] p. 55Axiom of Choice (second form)ac9 8365  ac9s 8375
[Enderton] p. 56Theorem 3Merref 6927
[Enderton] p. 57Lemma 3Nerthi 6953
[Enderton] p. 57Definitiondf-ec 6909
[Enderton] p. 58Definitiondf-qs 6913
[Enderton] p. 60Theorem 3Qth3q 7015  th3qcor 7014  th3qlem1 7012  th3qlem2 7013
[Enderton] p. 61Exercise 35df-ec 6909
[Enderton] p. 65Exercise 56(a)dmun 5078
[Enderton] p. 68Definition of successordf-suc 4589
[Enderton] p. 71Definitiondf-tr 4305  dftr4 4309
[Enderton] p. 72Theorem 4Eunisuc 4659
[Enderton] p. 73Exercise 6unisuc 4659
[Enderton] p. 73Exercise 5(a)truni 4318
[Enderton] p. 73Exercise 5(b)trint 4319  trintALT 29055
[Enderton] p. 79Theorem 4I(A1)nna0 6849
[Enderton] p. 79Theorem 4I(A2)nnasuc 6851  onasuc 6774
[Enderton] p. 79Definition of operation valuedf-ov 6086
[Enderton] p. 80Theorem 4J(A1)nnm0 6850
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6852  onmsuc 6775
[Enderton] p. 81Theorem 4K(1)nnaass 6867
[Enderton] p. 81Theorem 4K(2)nna0r 6854  nnacom 6862
[Enderton] p. 81Theorem 4K(3)nndi 6868
[Enderton] p. 81Theorem 4K(4)nnmass 6869
[Enderton] p. 81Theorem 4K(5)nnmcom 6871
[Enderton] p. 82Exercise 16nnm0r 6855  nnmsucr 6870
[Enderton] p. 88Exercise 23nnaordex 6883
[Enderton] p. 129Definitiondf-en 7112
[Enderton] p. 132Theorem 6B(b)canth 6541
[Enderton] p. 133Exercise 1xpomen 7899
[Enderton] p. 133Exercise 2qnnen 12815
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7293
[Enderton] p. 135Corollary 6Cphp3 7295
[Enderton] p. 136Corollary 6Enneneq 7292
[Enderton] p. 136Corollary 6D(a)pssinf 7321
[Enderton] p. 136Corollary 6D(b)ominf 7323
[Enderton] p. 137Lemma 6Fpssnn 7329
[Enderton] p. 138Corollary 6Gssfi 7331
[Enderton] p. 139Theorem 6H(c)mapen 7273
[Enderton] p. 142Theorem 6I(3)xpcdaen 8065
[Enderton] p. 142Theorem 6I(4)mapcdaen 8066
[Enderton] p. 143Theorem 6Jcda0en 8061  cda1en 8057
[Enderton] p. 144Exercise 13iunfi 7396  unifi 7397  unifi2 7398
[Enderton] p. 144Corollary 6Kundif2 3706  unfi 7376  unfi2 7378
[Enderton] p. 145Figure 38ffoss 5709
[Enderton] p. 145Definitiondf-dom 7113
[Enderton] p. 146Example 1domen 7123  domeng 7124
[Enderton] p. 146Example 3nndomo 7302  nnsdom 7610  nnsdomg 7368
[Enderton] p. 149Theorem 6L(a)cdadom2 8069
[Enderton] p. 149Theorem 6L(c)mapdom1 7274  xpdom1 7209  xpdom1g 7207  xpdom2g 7206
[Enderton] p. 149Theorem 6L(d)mapdom2 7280
[Enderton] p. 151Theorem 6Mzorn 8389  zorng 8386
[Enderton] p. 151Theorem 6M(4)ac8 8374  dfac5 8011
[Enderton] p. 159Theorem 6Qunictb 8452
[Enderton] p. 164Exampleinfdif 8091
[Enderton] p. 168Definitiondf-po 4505
[Enderton] p. 192Theorem 7M(a)oneli 4691
[Enderton] p. 192Theorem 7M(b)ontr1 4629
[Enderton] p. 192Theorem 7M(c)onirri 4690
[Enderton] p. 193Corollary 7N(b)0elon 4636
[Enderton] p. 193Corollary 7N(c)onsuci 4820
[Enderton] p. 193Corollary 7N(d)ssonunii 4770
[Enderton] p. 194Remarkonprc 4767
[Enderton] p. 194Exercise 16suc11 4687
[Enderton] p. 197Definitiondf-card 7828
[Enderton] p. 197Theorem 7Pcarden 8428
[Enderton] p. 200Exercise 25tfis 4836
[Enderton] p. 202Lemma 7Tr1tr 7704
[Enderton] p. 202Definitiondf-r1 7692
[Enderton] p. 202Theorem 7Qr1val1 7714
[Enderton] p. 204Theorem 7V(b)rankval4 7795
[Enderton] p. 206Theorem 7X(b)en2lp 7573
[Enderton] p. 207Exercise 30rankpr 7785  rankprb 7779  rankpw 7771  rankpwi 7751  rankuniss 7794
[Enderton] p. 207Exercise 34opthreg 7575
[Enderton] p. 208Exercise 35suc11reg 7576
[Enderton] p. 212Definition of alephalephval3 7993
[Enderton] p. 213Theorem 8A(a)alephord2 7959
[Enderton] p. 213Theorem 8A(b)cardalephex 7973
[Enderton] p. 218Theorem Schema 8Eonfununi 6605
[Enderton] p. 222Definition of kardkarden 7821  kardex 7820
[Enderton] p. 238Theorem 8Roeoa 6842
[Enderton] p. 238Theorem 8Soeoe 6844
[Enderton] p. 240Exercise 25oarec 6807
[Enderton] p. 257Definition of cofinalitycflm 8132
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13869
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13815
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14605  mrieqv2d 13866  mrieqvd 13865
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13870
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13875  mreexexlem2d 13872
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14611  mreexfidimd 13877
[Fremlin5] p. 193Proposition 563Gbnulmbl2 19433
[Fremlin5] p. 213Lemma 565Cauniioovol 19473
[Fremlin5] p. 214Lemma 565Cauniioombl 19483
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 26287
[Fremlin5] p. 220Theorem 565Maftc1anc 26290
[FreydScedrov] p. 283Axiom of Infinityax-inf 7595  inf1 7579  inf2 7580
[Gleason] p. 117Proposition 9-2.1df-enq 8790  enqer 8800
[Gleason] p. 117Proposition 9-2.2df-1nq 8795  df-nq 8791
[Gleason] p. 117Proposition 9-2.3df-plpq 8787  df-plq 8793
[Gleason] p. 119Proposition 9-2.4caovmo 6286  df-mpq 8788  df-mq 8794
[Gleason] p. 119Proposition 9-2.5df-rq 8796
[Gleason] p. 119Proposition 9-2.6ltexnq 8854
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8855  ltbtwnnq 8857
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8850
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8851
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8858
[Gleason] p. 121Definition 9-3.1df-np 8860
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8872
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8874
[Gleason] p. 122Definitiondf-1p 8861
[Gleason] p. 122Remark (1)prub 8873
[Gleason] p. 122Lemma 9-3.4prlem934 8912
[Gleason] p. 122Proposition 9-3.2df-ltp 8864
[Gleason] p. 122Proposition 9-3.3ltsopr 8911  psslinpr 8910  supexpr 8933  suplem1pr 8931  suplem2pr 8932
[Gleason] p. 123Proposition 9-3.5addclpr 8897  addclprlem1 8895  addclprlem2 8896  df-plp 8862
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8901
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8900
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8913
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8922  ltexprlem1 8915  ltexprlem2 8916  ltexprlem3 8917  ltexprlem4 8918  ltexprlem5 8919  ltexprlem6 8920  ltexprlem7 8921
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8924  ltaprlem 8923
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8925
[Gleason] p. 124Lemma 9-3.6prlem936 8926
[Gleason] p. 124Proposition 9-3.7df-mp 8863  mulclpr 8899  mulclprlem 8898  reclem2pr 8927
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8908
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8903
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8902
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8907
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8930  reclem3pr 8928  reclem4pr 8929
[Gleason] p. 126Proposition 9-4.1df-enr 8936  df-mpr 8935  df-plpr 8934  enrer 8945
[Gleason] p. 126Proposition 9-4.2df-0r 8941  df-1r 8942  df-nr 8937
[Gleason] p. 126Proposition 9-4.3df-mr 8939  df-plr 8938  negexsr 8979  recexsr 8984  recexsrlem 8980
[Gleason] p. 127Proposition 9-4.4df-ltr 8940
[Gleason] p. 130Proposition 10-1.3creui 9997  creur 9996  cru 9994
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 9065  axcnre 9041
[Gleason] p. 132Definition 10-3.1crim 11922  crimd 12039  crimi 12000  crre 11921  crred 12038  crrei 11999
[Gleason] p. 132Definition 10-3.2remim 11924  remimd 12005
[Gleason] p. 133Definition 10.36absval2 12091  absval2d 12249  absval2i 12202
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11948  cjaddd 12027  cjaddi 11995
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11949  cjmuld 12028  cjmuli 11996
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11947  cjcjd 12006  cjcji 11978
[Gleason] p. 133Proposition 10-3.4(f)cjre 11946  cjreb 11930  cjrebd 12009  cjrebi 11981  cjred 12033  rere 11929  rereb 11927  rerebd 12008  rerebi 11980  rered 12031
[Gleason] p. 133Proposition 10-3.4(h)addcj 11955  addcjd 12019  addcji 11990
[Gleason] p. 133Proposition 10-3.7(a)absval 12045
[Gleason] p. 133Proposition 10-3.7(b)abscj 12086  abscjd 12254  abscji 12206
[Gleason] p. 133Proposition 10-3.7(c)abs00 12096  abs00d 12250  abs00i 12203  absne0d 12251
[Gleason] p. 133Proposition 10-3.7(d)releabs 12127  releabsd 12255  releabsi 12207
[Gleason] p. 133Proposition 10-3.7(f)absmul 12101  absmuld 12258  absmuli 12209
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 12089  sqabsaddi 12210
[Gleason] p. 133Proposition 10-3.7(h)abstri 12136  abstrid 12260  abstrii 12213
[Gleason] p. 134Definition 10-4.1df-exp 11385  exp0 11388  expp1 11390  expp1d 11526
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20572  cxpaddd 20610  expadd 11424  expaddd 11527  expaddz 11426
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20581  cxpmuld 20627  expmul 11427  expmuld 11528  expmulz 11428
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20578  mulcxpd 20621  mulexp 11421  mulexpd 11540  mulexpz 11422
[Gleason] p. 140Exercise 1znnen 12814
[Gleason] p. 141Definition 11-2.1fzval 11047
[Gleason] p. 168Proposition 12-2.1(a)climadd 12427  rlimadd 12438  rlimdiv 12441
[Gleason] p. 168Proposition 12-2.1(b)climsub 12429  rlimsub 12439
[Gleason] p. 168Proposition 12-2.1(c)climmul 12428  rlimmul 12440
[Gleason] p. 171Corollary 12-2.2climmulc2 12432
[Gleason] p. 172Corollary 12-2.5climrecl 12379
[Gleason] p. 172Proposition 12-2.4(c)climabs 12399  climcj 12400  climim 12402  climre 12401  rlimabs 12404  rlimcj 12405  rlimim 12407  rlimre 12406
[Gleason] p. 173Definition 12-3.1df-ltxr 9127  df-xr 9126  ltxr 10717
[Gleason] p. 175Definition 12-4.1df-limsup 12267  limsupval 12270
[Gleason] p. 180Theorem 12-5.1climsup 12465
[Gleason] p. 180Theorem 12-5.3caucvg 12474  caucvgb 12475  caucvgr 12471  climcau 12466
[Gleason] p. 182Exercise 3cvgcmp 12597
[Gleason] p. 182Exercise 4cvgrat 12662
[Gleason] p. 195Theorem 13-2.12abs1m 12141
[Gleason] p. 217Lemma 13-4.1btwnzge0 11232
[Gleason] p. 223Definition 14-1.1df-met 16698
[Gleason] p. 223Definition 14-1.1(a)met0 18375  xmet0 18374
[Gleason] p. 223Definition 14-1.1(b)metgt0 18391
[Gleason] p. 223Definition 14-1.1(c)metsym 18382
[Gleason] p. 223Definition 14-1.1(d)mettri 18384  mstri 18501  xmettri 18383  xmstri 18500
[Gleason] p. 225Definition 14-1.5xpsmet 18414
[Gleason] p. 230Proposition 14-2.6txlm 17682
[Gleason] p. 240Theorem 14-4.3metcnp4 19264
[Gleason] p. 240Proposition 14-4.2metcnp3 18572
[Gleason] p. 243Proposition 14-4.16addcn 18897  addcn2 12389  mulcn 18899  mulcn2 12391  subcn 18898  subcn2 12390
[Gleason] p. 295Remarkbcval3 11599  bcval4 11600
[Gleason] p. 295Equation 2bcpasc 11614
[Gleason] p. 295Definition of binomial coefficientbcval 11597  df-bc 11596
[Gleason] p. 296Remarkbcn0 11603  bcnn 11605
[Gleason] p. 296Theorem 15-2.8binom 12611
[Gleason] p. 308Equation 2ef0 12695
[Gleason] p. 308Equation 3efcj 12696
[Gleason] p. 309Corollary 15-4.3efne0 12700
[Gleason] p. 309Corollary 15-4.4efexp 12704
[Gleason] p. 310Equation 14sinadd 12767
[Gleason] p. 310Equation 15cosadd 12768
[Gleason] p. 311Equation 17sincossq 12779
[Gleason] p. 311Equation 18cosbnd 12784  sinbnd 12783
[Gleason] p. 311Lemma 15-4.7sqeqor 11497  sqeqori 11495
[Gleason] p. 311Definition of pidf-pi 12677
[Godowski] p. 730Equation SFgoeqi 23778
[GodowskiGreechie] p. 249Equation IV3oai 23172
[Gratzer] p. 23Section 0.6df-mre 13813
[Gratzer] p. 27Section 0.6df-mri 13815
[Halmos] p. 31Theorem 17.3riesz1 23570  riesz2 23571
[Halmos] p. 41Definition of Hermitianhmopadj2 23446
[Halmos] p. 42Definition of projector orderingpjordi 23678
[Halmos] p. 43Theorem 26.1elpjhmop 23690  elpjidm 23689  pjnmopi 23653
[Halmos] p. 44Remarkpjinormi 23191  pjinormii 23180
[Halmos] p. 44Theorem 26.2elpjch 23694  pjrn 23211  pjrni 23206  pjvec 23200
[Halmos] p. 44Theorem 26.3pjnorm2 23231
[Halmos] p. 44Theorem 26.4hmopidmpj 23659  hmopidmpji 23657
[Halmos] p. 45Theorem 27.1pjinvari 23696
[Halmos] p. 45Theorem 27.3pjoci 23685  pjocvec 23201
[Halmos] p. 45Theorem 27.4pjorthcoi 23674
[Halmos] p. 48Theorem 29.2pjssposi 23677
[Halmos] p. 48Theorem 29.3pjssdif1i 23680  pjssdif2i 23679
[Halmos] p. 50Definition of spectrumdf-spec 23360
[Hamilton] p. 28Definition 2.1ax-1 5
[Hamilton] p. 31Example 2.7(a)id1 22
[Hamilton] p. 73Rule 1ax-mp 8
[Hamilton] p. 74Rule 2ax-gen 1556
[Hatcher] p. 25Definitiondf-phtpc 19019  df-phtpy 18998
[Hatcher] p. 26Definitiondf-pco 19032  df-pi1 19035
[Hatcher] p. 26Proposition 1.2phtpcer 19022
[Hatcher] p. 26Proposition 1.3pi1grp 19077
[Herstein] p. 54Exercise 28df-grpo 21781
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14823  grpoideu 21799  mndideu 14700
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14841  grpoinveu 21812
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14860  grpo2inv 21829
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14869  grpoinvop 21831
[Herstein] p. 57Exercise 1isgrp2d 21825  isgrp2i 21826
[Hitchcock] p. 5Rule A3mpto1 1543
[Hitchcock] p. 5Rule A4mpto2 1544
[Hitchcock] p. 5Rule A5mtp-xor 1546
[Holland] p. 1519Theorem 2sumdmdi 23925
[Holland] p. 1520Lemma 5cdj1i 23938  cdj3i 23946  cdj3lem1 23939  cdjreui 23937
[Holland] p. 1524Lemma 7mddmdin0i 23936
[Holland95] p. 13Theorem 3.6hlathil 32824
[Holland95] p. 14Line 15hgmapvs 32754
[Holland95] p. 14Line 16hdmaplkr 32776
[Holland95] p. 14Line 17hdmapellkr 32777
[Holland95] p. 14Line 19hdmapglnm2 32774
[Holland95] p. 14Line 20hdmapip0com 32780
[Holland95] p. 14Theorem 3.6hdmapevec2 32699
[Holland95] p. 14Lines 24 and 25hdmapoc 32794
[Holland95] p. 204Definition of involutiondf-srng 15936
[Holland95] p. 212Definition of subspacedf-psubsp 30362
[Holland95] p. 214Lemma 3.3lclkrlem2v 32388
[Holland95] p. 214Definition 3.2df-lpolN 32341
[Holland95] p. 214Definition of nonsingularpnonsingN 30792
[Holland95] p. 215Lemma 3.3(1)dihoml4 32237  poml4N 30812
[Holland95] p. 215Lemma 3.3(2)dochexmid 32328  pexmidALTN 30837  pexmidN 30828
[Holland95] p. 218Theorem 3.6lclkr 32393
[Holland95] p. 218Definition of dual vector spacedf-ldual 29984  ldualset 29985
[Holland95] p. 222Item 1df-lines 30360  df-pointsN 30361
[Holland95] p. 222Item 2df-polarityN 30762
[Holland95] p. 223Remarkispsubcl2N 30806  omllaw4 30106  pol1N 30769  polcon3N 30776
[Holland95] p. 223Definitiondf-psubclN 30794
[Holland95] p. 223Equation for polaritypolval2N 30765
[Hughes] p. 44Equation 1.21bax-his3 22588
[Hughes] p. 47Definition of projection operatordfpjop 23687
[Hughes] p. 49Equation 1.30eighmre 23468  eigre 23340  eigrei 23339
[Hughes] p. 49Equation 1.31eighmorth 23469  eigorth 23343  eigorthi 23342
[Hughes] p. 137Remark (ii)eigposi 23341
[Huneke] p. 1Theoremfrgrancvvdeq 28493  frgrancvvdgeq 28494
[Huneke] p. 1ObservationfrgrancvvdeqlemA 28488  frgrancvvdeqlemB 28489  frgrancvvdeqlemC 28490
[Huneke] p. 2Prooffrgrawopreglem4 28498  frgrawopreglem5 28499
[Huneke] p. 2Theoremfrghash2spot 28514  frgraregorufr 28504  frgraregorufr0 28503  frgrawopreg1 28501  frgrawopreg2 28502  frgregordn0 28521  usgreghash2spot 28520  usgreghash2spotv 28517
[Indrzejczak] p. 33Definition ` `Enatded 21713  natded 21713
[Indrzejczak] p. 33Definition ` `Inatded 21713
[Indrzejczak] p. 34Definition ` `Enatded 21713  natded 21713
[Indrzejczak] p. 34Definition ` `Inatded 21713
[Jech] p. 4Definition of classcv 1652  cvjust 2433
[Jech] p. 42Lemma 6.1alephexp1 8456
[Jech] p. 42Equation 6.1alephadd 8454  alephmul 8455
[Jech] p. 43Lemma 6.2infmap 8453  infmap2 8100
[Jech] p. 71Lemma 9.3jech9.3 7742
[Jech] p. 72Equation 9.3scott0 7812  scottex 7811
[Jech] p. 72Exercise 9.1rankval4 7795
[Jech] p. 72Scheme "Collection Principle"cp 7817
[Jech] p. 78Definition implied by the footnoteopthprc 4927
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26980
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 27076
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 27077
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26992
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26996
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26997  rmyp1 26998
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26999  rmym1 27000
[JonesMatijasevic] p. 695Equation 2.11rmx0 26990  rmx1 26991  rmxluc 27001
[JonesMatijasevic] p. 695Equation 2.12rmy0 26994  rmy1 26995  rmyluc 27002
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 27004
[JonesMatijasevic] p. 695Equation 2.14rmydbl 27005
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 27027  jm2.17b 27028  jm2.17c 27029
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 27066
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 27070
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 27061
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 27030  jm2.24nn 27026
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 27075
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 27081  rmygeid 27031
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 27093
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1667
[KalishMontague] p. 85Lemma 2equid 1689
[KalishMontague] p. 85Lemma 3equcomi 1692
[KalishMontague] p. 86Lemma 7cbvalivw 1687  cbvaliw 1686
[KalishMontague] p. 87Lemma 8spimvw 1682  spimw 1681
[KalishMontague] p. 87Lemma 9spfw 1704  spw 1707
[Kalmbach] p. 14Definition of latticechabs1 23020  chabs1i 23022  chabs2 23021  chabs2i 23023  chjass 23037  chjassi 22990  latabs1 14518  latabs2 14519
[Kalmbach] p. 15Definition of atomdf-at 23843  ela 23844
[Kalmbach] p. 15Definition of coverscvbr2 23788  cvrval2 30134
[Kalmbach] p. 16Definitiondf-ol 30038  df-oml 30039
[Kalmbach] p. 20Definition of commutescmbr 23088  cmbri 23094  cmtvalN 30071  df-cm 23087  df-cmtN 30037
[Kalmbach] p. 22Remarkomllaw5N 30107  pjoml5 23117  pjoml5i 23092
[Kalmbach] p. 22Definitionpjoml2 23115  pjoml2i 23089
[Kalmbach] p. 22Theorem 2(v)cmcm 23118  cmcmi 23096  cmcmii 23101  cmtcomN 30109
[Kalmbach] p. 22Theorem 2(ii)omllaw3 30105  omlsi 22908  pjoml 22940  pjomli 22939
[Kalmbach] p. 22Definition of OML lawomllaw2N 30104
[Kalmbach] p. 23Remarkcmbr2i 23100  cmcm3 23119  cmcm3i 23098  cmcm3ii 23103  cmcm4i 23099  cmt3N 30111  cmt4N 30112  cmtbr2N 30113
[Kalmbach] p. 23Lemma 3cmbr3 23112  cmbr3i 23104  cmtbr3N 30114
[Kalmbach] p. 25Theorem 5fh1 23122  fh1i 23125  fh2 23123  fh2i 23126  omlfh1N 30118
[Kalmbach] p. 65Remarkchjatom 23862  chslej 23002  chsleji 22962  shslej 22884  shsleji 22874
[Kalmbach] p. 65Proposition 1chocin 22999  chocini 22958  chsupcl 22844  chsupval2 22914  h0elch 22759  helch 22748  hsupval2 22913  ocin 22800  ococss 22797  shococss 22798
[Kalmbach] p. 65Definition of subspace sumshsval 22816
[Kalmbach] p. 66Remarkdf-pjh 22899  pjssmi 23670  pjssmii 23185
[Kalmbach] p. 67Lemma 3osum 23149  osumi 23146
[Kalmbach] p. 67Lemma 4pjci 23705
[Kalmbach] p. 103Exercise 6atmd2 23905
[Kalmbach] p. 103Exercise 12mdsl0 23815
[Kalmbach] p. 140Remarkhatomic 23865  hatomici 23864  hatomistici 23867
[Kalmbach] p. 140Proposition 1atlatmstc 30179
[Kalmbach] p. 140Proposition 1(i)atexch 23886  lsatexch 29903
[Kalmbach] p. 140Proposition 1(ii)chcv1 23860  cvlcvr1 30199  cvr1 30269
[Kalmbach] p. 140Proposition 1(iii)cvexch 23879  cvexchi 23874  cvrexch 30279
[Kalmbach] p. 149Remark 2chrelati 23869  hlrelat 30261  hlrelat5N 30260  lrelat 29874
[Kalmbach] p. 153Exercise 5lsmcv 16215  lsmsatcv 29870  spansncv 23157  spansncvi 23156
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29889  spansncv2 23798
[Kalmbach] p. 266Definitiondf-st 23716
[Kalmbach2] p. 8Definition of adjointdf-adjh 23354
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8523  fpwwe2 8520
[KanamoriPincus] p. 416Corollary 1.3canth4 8524
[KanamoriPincus] p. 417Corollary 1.6canthp1 8531
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8526
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8528
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8541
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8545  gchxpidm 8546
[KanamoriPincus] p. 419Theorem 2.1gchacg 8549  gchhar 8548
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 8098  unxpwdom 7559
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8551
[Kreyszig] p. 3Property M1metcl 18364  xmetcl 18363
[Kreyszig] p. 4Property M2meteq0 18371
[Kreyszig] p. 8Definition 1.1-8dscmet 18622
[Kreyszig] p. 12Equation 5conjmul 9733  muleqadd 9668
[Kreyszig] p. 18Definition 1.3-2mopnval 18470
[Kreyszig] p. 19Remarkmopntopon 18471
[Kreyszig] p. 19Theorem T1mopn0 18530  mopnm 18476
[Kreyszig] p. 19Theorem T2unimopn 18528
[Kreyszig] p. 19Definition of neighborhoodneibl 18533
[Kreyszig] p. 20Definition 1.3-3metcnp2 18574
[Kreyszig] p. 25Definition 1.4-1lmbr 17324  lmmbr 19213  lmmbr2 19214
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17446
[Kreyszig] p. 28Theorem 1.4-5lmcau 19267
[Kreyszig] p. 28Definition 1.4-3iscau 19231  iscmet2 19249
[Kreyszig] p. 30Theorem 1.4-7cmetss 19269
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17526  metelcls 19259
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 19260  metcld2 19261
[Kreyszig] p. 51Equation 2clmvneg1 19118  lmodvneg1 15989  nvinv 22122  vcm 22052
[Kreyszig] p. 51Equation 1aclm0vs 19117  lmod0vs 15985  vc0 22050
[Kreyszig] p. 51Equation 1blmodvs0 15986  vcz 22051
[Kreyszig] p. 58Definition 2.2-1imsmet 22185
[Kreyszig] p. 59Equation 1imsdval 22180  imsdval2 22181
[Kreyszig] p. 63Problem 1nvnd 22182
[Kreyszig] p. 64Problem 2nvge0 22165  nvz 22160
[Kreyszig] p. 64Problem 3nvabs 22164
[Kreyszig] p. 91Definition 2.7-1isblo3i 22304
[Kreyszig] p. 92Equation 2df-nmoo 22248
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 22310  blocni 22308
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 22309
[Kreyszig] p. 129Definition 3.1-1cphipeq0 19168  ipeq0 16871  ipz 22220
[Kreyszig] p. 135Problem 2pythi 22353
[Kreyszig] p. 137Lemma 3-2.1(a)sii 22357
[Kreyszig] p. 144Equation 4supcvg 12637
[Kreyszig] p. 144Theorem 3.3-1minvec 19339  minveco 22388
[Kreyszig] p. 196Definition 3.9-1df-aj 22253
[Kreyszig] p. 247Theorem 4.7-2bcth 19284
[Kreyszig] p. 249Theorem 4.7-3ubth 22377
[Kreyszig] p. 470Definition of positive operator orderingleop 23628  leopg 23627
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 23646
[Kreyszig] p. 525Theorem 10.1-1htth 22423
[Kunen] p. 10Axiom 0a9e 1953  axnul 4339
[Kunen] p. 11Axiom 3axnul 4339
[Kunen] p. 12Axiom 6zfrep6 5970
[Kunen] p. 24Definition 10.24mapval 7032  mapvalg 7030
[Kunen] p. 30Lemma 10.20fodom 8404
[Kunen] p. 31Definition 10.24mapex 7026
[Kunen] p. 95Definition 2.1df-r1 7692
[Kunen] p. 97Lemma 2.10r1elss 7734  r1elssi 7733
[Kunen] p. 107Exercise 4rankop 7786  rankopb 7780  rankuni 7791  rankxplim 7805  rankxpsuc 7808
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4105
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27530
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27525
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27531
[LeBlanc] p. 277Rule R2axnul 4339
[Levy] p. 338Axiomdf-clab 2425  df-clel 2434  df-cleq 2431
[Levy58] p. 2Definition Iisfin1-3 8268
[Levy58] p. 2Definition IIdf-fin2 8168
[Levy58] p. 2Definition Iadf-fin1a 8167
[Levy58] p. 2Definition IIIdf-fin3 8170
[Levy58] p. 3Definition Vdf-fin5 8171
[Levy58] p. 3Definition IVdf-fin4 8169
[Levy58] p. 4Definition VIdf-fin6 8172
[Levy58] p. 4Definition VIIdf-fin7 8173
[Levy58], p. 3Theorem 1fin1a2 8297
[Lopez-Astorga] p. 12Rule 1mpto1 1543
[Lopez-Astorga] p. 12Rule 2mpto2 1544
[Lopez-Astorga] p. 12Rule 3mtp-xor 1546
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 23913
[Maeda] p. 168Lemma 5mdsym 23917  mdsymi 23916
[Maeda] p. 168Lemma 4(i)mdsymlem4 23911  mdsymlem6 23913  mdsymlem7 23914
[Maeda] p. 168Lemma 4(ii)mdsymlem8 23915
[MaedaMaeda] p. 1Remarkssdmd1 23818  ssdmd2 23819  ssmd1 23816  ssmd2 23817
[MaedaMaeda] p. 1Lemma 1.2mddmd2 23814
[MaedaMaeda] p. 1Definition 1.1df-dmd 23786  df-md 23785  mdbr 23799
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 23836  mdslj1i 23824  mdslj2i 23825  mdslle1i 23822  mdslle2i 23823  mdslmd1i 23834  mdslmd2i 23835
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 23826  mdsl2bi 23828  mdsl2i 23827
[MaedaMaeda] p. 2Lemma 1.6mdexchi 23840
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 23837
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 23838
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 23815
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 23820  mdsl3 23821
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 23839
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23934
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 30181  hlrelat1 30259
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29899
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 23841  cvmdi 23829  cvnbtwn4 23794  cvrnbtwn4 30139
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 23842
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 30200  cvp 23880  cvrp 30275  lcvp 29900
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 23904
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 23903
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 30193  hlexch4N 30251
[MaedaMaeda] p. 34Exercise 7.1atabsi 23906
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 30302
[MaedaMaeda] p. 61Definition 15.10psubN 30608  atpsubN 30612  df-pointsN 30361  pointpsubN 30610
[MaedaMaeda] p. 62Theorem 15.5df-pmap 30363  pmap11 30621  pmaple 30620  pmapsub 30627  pmapval 30616
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 30624  pmap1N 30626
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 30629  pmapglb2N 30630  pmapglb2xN 30631  pmapglbx 30628
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 30711
[MaedaMaeda] p. 67Postulate PS1ps-1 30336
[MaedaMaeda] p. 68Lemma 16.2df-padd 30655  paddclN 30701  paddidm 30700
[MaedaMaeda] p. 68Condition PS2ps-2 30337
[MaedaMaeda] p. 68Equation 16.2.1paddass 30697
[MaedaMaeda] p. 69Lemma 16.4ps-1 30336
[MaedaMaeda] p. 69Theorem 16.4ps-2 30337
[MaedaMaeda] p. 70Theorem 16.9lsmmod 15309  lsmmod2 15310  lssats 29872  shatomici 23863  shatomistici 23866  shmodi 22894  shmodsi 22893
[MaedaMaeda] p. 130Remark 29.6dmdmd 23805  mdsymlem7 23914
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 23093
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22997
[MaedaMaeda] p. 139Remarksumdmdii 23920
[Margaris] p. 40Rule Cexlimiv 1645
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 7
[Margaris] p. 49Definitiondf-an 362  df-ex 1552  df-or 361  dfbi2 611
[Margaris] p. 51Theorem 1id1 22
[Margaris] p. 56Theorem 3syld 43
[Margaris] p. 59Section 14notnot2ALTVD 29089
[Margaris] p. 60Theorem 8mth8 141
[Margaris] p. 60Section 14con3ALTVD 29090
[Margaris] p. 79Rule Cexinst01 28788  exinst11 28789
[Margaris] p. 89Theorem 19.219.2 1672  19.2g 1774  r19.2z 3719
[Margaris] p. 89Theorem 19.319.3 1792  19.3v 1678  rr19.3v 3079
[Margaris] p. 89Theorem 19.5alcom 1753
[Margaris] p. 89Theorem 19.6alex 1582
[Margaris] p. 89Theorem 19.7alnex 1553
[Margaris] p. 89Theorem 19.819.8a 1763
[Margaris] p. 89Theorem 19.919.9 1798  19.9h 1795  19.9v 1677  exlimd 1825  exlimdh 1827
[Margaris] p. 89Theorem 19.11excom 1757  excomim 1758
[Margaris] p. 89Theorem 19.1219.12 1870  r19.12 2821
[Margaris] p. 90Theorem 19.14exnal 1584
[Margaris] p. 90Theorem 19.152albi 27555  albi 1574  ralbi 2844
[Margaris] p. 90Theorem 19.1619.16 1884
[Margaris] p. 90Theorem 19.1719.17 1885
[Margaris] p. 90Theorem 19.182exbi 27557  exbi 1592
[Margaris] p. 90Theorem 19.1919.19 1886
[Margaris] p. 90Theorem 19.202alim 27554  alim 1568  alimd 1781  alimdh 1573  alimdv 1632  ralimdaa 2785  ralimdv 2787  ralimdva 2786  sbcimdv 3224
[Margaris] p. 90Theorem 19.2119.21-2 1888  19.21 1815  19.21bi 1775  19.21h 1816  19.21t 1814  19.21v 1914  19.21vv 27553  alrimd 1786  alrimdd 1785  alrimdh 1598  alrimdv 1644  alrimi 1782  alrimih 1575  alrimiv 1642  alrimivv 1643  r19.21 2794  r19.21be 2809  r19.21bi 2806  r19.21t 2793  r19.21v 2795  ralrimd 2796  ralrimdv 2797  ralrimdva 2798  ralrimdvv 2802  ralrimdvva 2803  ralrimi 2789  ralrimiv 2790  ralrimiva 2791  ralrimivv 2799  ralrimivva 2800  ralrimivvva 2801  ralrimivw 2792  rexlimi 2825
[Margaris] p. 90Theorem 19.222alimdv 1634  2exim 27556  2eximdv 1635  exim 1585  eximd 1787  eximdh 1599  eximdv 1633  rexim 2812  reximdai 2816  reximddv 23964  reximdv 2819  reximdv2 2817  reximdva 2820  reximdvai 2818  reximi2 2814
[Margaris] p. 90Theorem 19.2319.23 1820  19.23bi 1776  19.23h 1821  19.23t 1819  19.23v 1915  19.23vv 1916  exlimdv 1647  exlimdvv 1648  exlimexi 28670  exlimi 1822  exlimih 1823  exlimiv 1645  exlimivv 1646  r19.23 2823  r19.23v 2824  rexlimd 2829  rexlimdv 2831  rexlimdv3a 2834  rexlimdva 2832  rexlimdvaa 2833  rexlimdvv 2838  rexlimdvva 2839  rexlimdvw 2835  rexlimiv 2826  rexlimiva 2827  rexlimivv 2837
[Margaris] p. 90Theorem 19.2419.24 1675
[Margaris] p. 90Theorem 19.2519.25 1614
[Margaris] p. 90Theorem 19.2619.26-2 1605  19.26-3an 1606  19.26 1604  r19.26-2 2841  r19.26-3 2842  r19.26 2840  r19.26m 2843
[Margaris] p. 90Theorem 19.2719.27 1842  19.27v 1918  r19.27av 2846  r19.27z 3728  r19.27zv 3729
[Margaris] p. 90Theorem 19.2819.28 1843  19.28v 1919  19.28vv 27563  r19.28av 2847  r19.28z 3722  r19.28zv 3725  rr19.28v 3080
[Margaris] p. 90Theorem 19.2919.29 1607  19.29r 1608  19.29r2 1609  19.29x 1610  r19.29 2848  r19.29d2r 2853  r19.29r 2849
[Margaris] p. 90Theorem 19.3019.30 1615  r19.30 2855
[Margaris] p. 90Theorem 19.3119.31 1898  19.31vv 27561
[Margaris] p. 90Theorem 19.3219.32 1897  r19.32 27923  r19.32v 2856
[Margaris] p. 90Theorem 19.3319.33-2 27559  19.33 1618  19.33b 1619
[Margaris] p. 90Theorem 19.3419.34 1676
[Margaris] p. 90Theorem 19.3519.35 1611  19.35i 1612  19.35ri 1613  r19.35 2857
[Margaris] p. 90Theorem 19.3619.36 1893  19.36aiv 1921  19.36i 1894  19.36v 1920  19.36vv 27560  r19.36av 2858  r19.36zv 3730
[Margaris] p. 90Theorem 19.3719.37 1895  19.37aiv 1924  19.37v 1923  19.37vv 27562  r19.37 2859  r19.37av 2860  r19.37zv 3726
[Margaris] p. 90Theorem 19.3819.38 1813
[Margaris] p. 90Theorem 19.3919.39 1674
[Margaris] p. 90Theorem 19.4019.40-2 1621  19.40 1620  r19.40 2861
[Margaris] p. 90Theorem 19.4119.41 1901  19.41rg 28699  19.41v 1925  19.41vv 1926  19.41vvv 1927  19.41vvvv 1928  r19.41 2862  r19.41v 2863  r19.41vv 23972
[Margaris] p. 90Theorem 19.4219.42 1903  19.42v 1929  19.42vv 1931  19.42vvv 1932  r19.42v 2864
[Margaris] p. 90Theorem 19.4319.43 1616  r19.43 2865
[Margaris] p. 90Theorem 19.4419.44 1899  r19.44av 2866
[Margaris] p. 90Theorem 19.4519.45 1900  r19.45av 2867  r19.45zv 3727
[Margaris] p. 110Exercise 2(b)eu1 2304
[Mayet] p. 370Remarkjpi 23775  largei 23772  stri 23762
[Mayet3] p. 9Definition of CH-statesdf-hst 23717  ishst 23719
[Mayet3] p. 10Theoremhstrbi 23771  hstri 23770
[Mayet3] p. 1223Theorem 4.1mayete3i 23232
[Mayet3] p. 1240Theorem 7.1mayetes3i 23234
[MegPav2000] p. 2344Theorem 3.3stcltrthi 23783
[MegPav2000] p. 2345Definition 3.4-1chintcl 22836  chsupcl 22844
[MegPav2000] p. 2345Definition 3.4-2hatomic 23865
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 23859
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 23886
[MegPav2000] p. 2366Figure 7pl42N 30842
[MegPav2002] p. 362Lemma 2.2latj31 14530  latj32 14528  latjass 14526
[Megill] p. 444Axiom C5ax-17 1627  ax17o 2236
[Megill] p. 444Section 7conventions 21712
[Megill] p. 445Lemma L12aecom-o 2230  aecom 2036  ax-10 2219
[Megill] p. 446Lemma L17equtrr 1696
[Megill] p. 446Lemma L18ax9from9o 2227
[Megill] p. 446Lemma L19hbnae-o 2258  hbnae 2044
[Megill] p. 447Remark 9.1df-sb 1660  sbid 1948  sbidd-misc 28524  sbidd 28523
[Megill] p. 448Remark 9.6ax15 2109
[Megill] p. 448Scheme C4'ax-5o 2215
[Megill] p. 448Scheme C5'ax-4 2214  sp 1764
[Megill] p. 448Scheme C6'ax-7 1750
[Megill] p. 448Scheme C7'ax-6o 2216
[Megill] p. 448Scheme C8'ax-8 1688
[Megill] p. 448Scheme C9'ax-12o 2221
[Megill] p. 448Scheme C10'ax-9 1667  ax-9o 2217
[Megill] p. 448Scheme C11'ax-10o 2218
[Megill] p. 448Scheme C12'ax-13 1728
[Megill] p. 448Scheme C13'ax-14 1730
[Megill] p. 448Scheme C14'ax-15 2222
[Megill] p. 448Scheme C15'ax-11o 2220
[Megill] p. 448Scheme C16'ax-16 2223
[Megill] p. 448Theorem 9.4dral1-o 2233  dral1 2058  dral2-o 2260  dral2 2056  drex1 2060  drex2 2061  drsb1 2114  drsb2 2115
[Megill] p. 448Theorem 9.7conventions 21712
[Megill] p. 449Theorem 9.7sbcom2 2192  sbequ 2113  sbid2v 2202
[Megill] p. 450Example in Appendixhba1-o 2228  hba1 1805
[Mendelson] p. 35Axiom A3hirstL-ax3 27838
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4rspsbc 3241  rspsbca 3242  stdpc4 2092
[Mendelson] p. 69Axiom 5ax-5o 2215  ra5 3247  stdpc5 1817
[Mendelson] p. 81Rule Cexlimiv 1645
[Mendelson] p. 95Axiom 6stdpc6 1700
[Mendelson] p. 95Axiom 7stdpc7 1943
[Mendelson] p. 225Axiom system NBGru 3162
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4460
[Mendelson] p. 231Exercise 4.10(k)inv1 3656
[Mendelson] p. 231Exercise 4.10(l)unv 3657
[Mendelson] p. 231Exercise 4.10(n)dfin3 3582
[Mendelson] p. 231Exercise 4.10(o)df-nul 3631
[Mendelson] p. 231Exercise 4.10(q)dfin4 3583
[Mendelson] p. 231Exercise 4.10(s)ddif 3481
[Mendelson] p. 231Definition of uniondfun3 3581
[Mendelson] p. 235Exercise 4.12(c)univ 4756
[Mendelson] p. 235Exercise 4.12(d)pwv 4016
[Mendelson] p. 235Exercise 4.12(j)pwin 4489
[Mendelson] p. 235Exercise 4.12(k)pwunss 4490
[Mendelson] p. 235Exercise 4.12(l)pwssun 4491
[Mendelson] p. 235Exercise 4.12(n)uniin 4037
[Mendelson] p. 235Exercise 4.12(p)reli 5004
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5392
[Mendelson] p. 244Proposition 4.8(g)epweon 4766
[Mendelson] p. 246Definition of successordf-suc 4589
[Mendelson] p. 250Exercise 4.36oelim2 6840
[Mendelson] p. 254Proposition 4.22(b)xpen 7272
[Mendelson] p. 254Proposition 4.22(c)xpsnen 7194  xpsneng 7195
[Mendelson] p. 254Proposition 4.22(d)xpcomen 7201  xpcomeng 7202
[Mendelson] p. 254Proposition 4.22(e)xpassen 7204
[Mendelson] p. 255Definitionbrsdom 7132
[Mendelson] p. 255Exercise 4.39endisj 7197
[Mendelson] p. 255Exercise 4.41mapprc 7024
[Mendelson] p. 255Exercise 4.43mapsnen 7186
[Mendelson] p. 255Exercise 4.45mapunen 7278
[Mendelson] p. 255Exercise 4.47xpmapen 7277
[Mendelson] p. 255Exercise 4.42(a)map0e 7053
[Mendelson] p. 255Exercise 4.42(b)map1 7187
[Mendelson] p. 257Proposition 4.24(a)undom 7198
[Mendelson] p. 258Exercise 4.56(b)cdaen 8055
[Mendelson] p. 258Exercise 4.56(c)cdaassen 8064  cdacomen 8063
[Mendelson] p. 258Exercise 4.56(f)cdadom1 8068
[Mendelson] p. 258Exercise 4.56(g)xp2cda 8062
[Mendelson] p. 258Definition of cardinal sumcdaval 8052  df-cda 8050
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6777
[Mendelson] p. 266Proposition 4.34(f)oaordex 6803
[Mendelson] p. 275Proposition 4.42(d)entri3 8436
[Mendelson] p. 281Definitiondf-r1 7692
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7741
[Mendelson] p. 287Axiom system MKru 3162
[MertziosUnger] p. 153Proposition 12pthfrgra 28463  2pthfrgrarn 28461  2pthfrgrarn2 28462  frconngra 28473  n4cyclfrgra 28470  vdgfrgragt2 28480  vdgn1frgrav2 28479  vdn1frgrav2 28478
[Mittelstaedt] p. 9Definitiondf-oc 22756
[Monk1] p. 22Remarkconventions 21712
[Monk1] p. 22Theorem 3.1conventions 21712
[Monk1] p. 26Theorem 2.8(vii)ssin 3565
[Monk1] p. 33Theorem 3.2(i)ssrel 4966
[Monk1] p. 33Theorem 3.2(ii)eqrel 4967
[Monk1] p. 34Definition 3.3df-opab 4269
[Monk1] p. 36Theorem 3.7(i)coi1 5387  coi2 5388
[Monk1] p. 36Theorem 3.8(v)dm0 5085  rn0 5129
[Monk1] p. 36Theorem 3.7(ii)cnvi 5278
[Monk1] p. 37Theorem 3.13(i)relxp 4985
[Monk1] p. 37Theorem 3.13(x)dmxp 5090  rnxp 5301
[Monk1] p. 37Theorem 3.13(ii)xp0 5293  xp0r 4958
[Monk1] p. 38Theorem 3.16(ii)ima0 5223
[Monk1] p. 38Theorem 3.16(viii)imai 5220
[Monk1] p. 39Theorem 3.17imaexg 5219
[Monk1] p. 39Theorem 3.16(xi)imassrn 5218
[Monk1] p. 41Theorem 4.3(i)fnopfv 5867  funfvop 5844
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5772
[Monk1] p. 42Theorem 4.4(iii)fvelima 5780
[Monk1] p. 43Theorem 4.6funun 5497
[Monk1] p. 43Theorem 4.8(iv)dff13 6006  dff13f 6008
[Monk1] p. 46Theorem 4.15(v)funex 5965  funrnex 5969
[Monk1] p. 50Definition 5.4fniunfv 5996
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5355
[Monk1] p. 52Theorem 5.11(viii)ssint 4068
[Monk1] p. 52Definition 5.13 (i)1stval2 6366  df-1st 6351
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6367  df-2nd 6352
[Monk1] p. 112Theorem 15.17(v)ranksn 7782  ranksnb 7755
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7783
[Monk1] p. 112Theorem 15.17(iii)rankun 7784  rankunb 7778
[Monk1] p. 113Theorem 15.18r1val3 7766
[Monk1] p. 113Definition 15.19df-r1 7692  r1val2 7765
[Monk1] p. 117Lemmazorn2 8388  zorn2g 8385
[Monk1] p. 133Theorem 18.11cardom 7875
[Monk1] p. 133Theorem 18.12canth3 8438
[Monk1] p. 133Theorem 18.14carduni 7870
[Monk2] p. 105Axiom C4ax-5 1567
[Monk2] p. 105Axiom C7ax-8 1688
[Monk2] p. 105Axiom C8ax-11 1762  ax-11o 2220
[Monk2] p. 105Axiom (C8)ax11v 2174
[Monk2] p. 108Lemma 5ax-5o 2215
[Monk2] p. 109Lemma 12ax-7 1750
[Monk2] p. 109Lemma 15equvin 2088  equvini 2084  eqvinop 4443
[Monk2] p. 113Axiom C5-1ax-17 1627  ax17o 2236
[Monk2] p. 113Axiom C5-2ax-6 1745
[Monk2] p. 113Axiom C5-3ax-7 1750
[Monk2] p. 114Lemma 21sp 1764
[Monk2] p. 114Lemma 22ax5o 1766  hba1-o 2228  hba1 1805
[Monk2] p. 114Lemma 23nfia1 1876
[Monk2] p. 114Lemma 24nfa2 1875  nfra2 2762
[Moore] p. 53Part Idf-mre 13813
[Munkres] p. 77Example 2distop 17062  indistop 17068  indistopon 17067
[Munkres] p. 77Example 3fctop 17070  fctop2 17071
[Munkres] p. 77Example 4cctop 17072
[Munkres] p. 78Definition of basisdf-bases 16967  isbasis3g 17016
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13669  tgval2 17023
[Munkres] p. 79Remarktgcl 17036
[Munkres] p. 80Lemma 2.1tgval3 17030
[Munkres] p. 80Lemma 2.2tgss2 17054  tgss3 17053
[Munkres] p. 81Lemma 2.3basgen 17055  basgen2 17056
[Munkres] p. 89Definition of subspace topologyresttop 17226
[Munkres] p. 93Theorem 6.1(1)0cld 17104  topcld 17101
[Munkres] p. 93Theorem 6.1(2)iincld 17105
[Munkres] p. 93Theorem 6.1(3)uncld 17107
[Munkres] p. 94Definition of closureclsval 17103
[Munkres] p. 94Definition of interiorntrval 17102
[Munkres] p. 95Theorem 6.5(a)clsndisj 17141  elcls 17139
[Munkres] p. 95Theorem 6.5(b)elcls3 17149
[Munkres] p. 97Theorem 6.6clslp 17214  neindisj 17183
[Munkres] p. 97Corollary 6.7cldlp 17216
[Munkres] p. 97Definition of limit pointislp2 17211  lpval 17205
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17381
[Munkres] p. 102Definition of continuous functiondf-cn 17293  iscn 17301  iscn2 17304
[Munkres] p. 107Theorem 7.2(g)cncnp 17346  cncnp2 17347  cncnpi 17344  df-cnp 17294  iscnp 17303  iscnp2 17305
[Munkres] p. 127Theorem 10.1metcn 18575
[Munkres] p. 128Theorem 10.3metcn4 19265
[NielsenChuang] p. 195Equation 4.73unierri 23609
[Pfenning] p. 17Definition XMnatded 21713
[Pfenning] p. 17Definition NNCnatded 21713  notnotrd 108
[Pfenning] p. 17Definition ` `Cnatded 21713
[Pfenning] p. 18Rule"natded 21713
[Pfenning] p. 18Definition /\Inatded 21713
[Pfenning] p. 18Definition ` `Enatded 21713  natded 21713  natded 21713  natded 21713  natded 21713
[Pfenning] p. 18Definition ` `Inatded 21713  natded 21713  natded 21713  natded 21713  natded 21713
[Pfenning] p. 18Definition ` `ELnatded 21713
[Pfenning] p. 18Definition ` `ERnatded 21713
[Pfenning] p. 18Definition ` `Ea,unatded 21713
[Pfenning] p. 18Definition ` `IRnatded 21713
[Pfenning] p. 18Definition ` `Ianatded 21713
[Pfenning] p. 127Definition =Enatded 21713
[Pfenning] p. 127Definition =Inatded 21713
[Ponnusamy] p. 361Theorem 6.44cphip0l 19166  df-dip 22199  dip0l 22219  ip0l 16869
[Ponnusamy] p. 361Equation 6.45ipval 22201
[Ponnusamy] p. 362Equation I1dipcj 22215
[Ponnusamy] p. 362Equation I3cphdir 19169  dipdir 22345  ipdir 16872  ipdiri 22333
[Ponnusamy] p. 362Equation I4ipidsq 22211
[Ponnusamy] p. 362Equation 6.46ip0i 22328
[Ponnusamy] p. 362Equation 6.47ip1i 22330
[Ponnusamy] p. 362Equation 6.48ip2i 22331
[Ponnusamy] p. 363Equation I2cphass 19175  dipass 22348  ipass 16878  ipassi 22344
[Prugovecki] p. 186Definition of brabraval 23449  df-bra 23355
[Prugovecki] p. 376Equation 8.1df-kb 23356  kbval 23459
[PtakPulmannova] p. 66Proposition 3.2.17atomli 23887
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30747
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 23901  atcvat4i 23902  cvrat3 30301  cvrat4 30302  lsatcvat3 29912
[PtakPulmannova] p. 68Definition 3.2.18cvbr 23787  cvrval 30129  df-cv 23784  df-lcv 29879  lspsncv0 16220
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30759
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30760
[Quine] p. 16Definition 2.1df-clab 2425  rabid 2886
[Quine] p. 17Definition 2.1''dfsb7 2200
[Quine] p. 18Definition 2.7df-cleq 2431
[Quine] p. 19Definition 2.9conventions 21712  df-v 2960
[Quine] p. 34Theorem 5.1abeq2 2543
[Quine] p. 35Theorem 5.2abid2 2555  abid2f 2599
[Quine] p. 40Theorem 6.1sb5 2178
[Quine] p. 40Theorem 6.2sb56 2176  sb6 2177
[Quine] p. 41Theorem 6.3df-clel 2434
[Quine] p. 41Theorem 6.4eqid 2438  eqid1 21763
[Quine] p. 41Theorem 6.5eqcom 2440
[Quine] p. 42Theorem 6.6df-sbc 3164
[Quine] p. 42Theorem 6.7dfsbcq 3165  dfsbcq2 3166
[Quine] p. 43Theorem 6.8vex 2961
[Quine] p. 43Theorem 6.9isset 2962
[Quine] p. 44Theorem 7.3spcgf 3033  spcgv 3038  spcimgf 3031
[Quine] p. 44Theorem 6.11spsbc 3175  spsbcd 3176
[Quine] p. 44Theorem 6.12elex 2966
[Quine] p. 44Theorem 6.13elab 3084  elabg 3085  elabgf 3082
[Quine] p. 44Theorem 6.14noel 3634
[Quine] p. 48Theorem 7.2snprc 3873
[Quine] p. 48Definition 7.1df-pr 3823  df-sn 3822
[Quine] p. 49Theorem 7.4snss 3928  snssg 3934
[Quine] p. 49Theorem 7.5prss 3954  prssg 3955
[Quine] p. 49Theorem 7.6prid1 3914  prid1g 3912  prid2 3915  prid2g 3913  snid 3843  snidg 3841
[Quine] p. 51Theorem 7.13prex 4408  snex 4407  snexALT 4387
[Quine] p. 53Theorem 8.2unisn 4033  unisnALT 29100  unisng 4034
[Quine] p. 53Theorem 8.3uniun 4036
[Quine] p. 54Theorem 8.6elssuni 4045
[Quine] p. 54Theorem 8.7uni0 4044
[Quine] p. 56Theorem 8.17uniabio 5430
[Quine] p. 56Definition 8.18dfiota2 5421
[Quine] p. 57Theorem 8.19iotaval 5431
[Quine] p. 57Theorem 8.22iotanul 5435
[Quine] p. 58Theorem 8.23iotaex 5437
[Quine] p. 58Definition 9.1df-op 3825
[Quine] p. 61Theorem 9.5opabid 4463  opelopab 4478  opelopaba 4473  opelopabaf 4480  opelopabf 4481  opelopabg 4475  opelopabga 4470  opelopabgf 28074  oprabid 6107
[Quine] p. 64Definition 9.11df-xp 4886
[Quine] p. 64Definition 9.12df-cnv 4888
[Quine] p. 64Definition 9.15df-id 4500
[Quine] p. 65Theorem 10.3fun0 5510
[Quine] p. 65Theorem 10.4funi 5485
[Quine] p. 65Theorem 10.5funsn 5501  funsng 5499
[Quine] p. 65Definition 10.1df-fun 5458
[Quine] p. 65Definition 10.2args 5234  dffv4 5727
[Quine] p. 68Definition 10.11conventions 21712  df-fv 5464  fv2 5725
[Quine] p. 124Theorem 17.3nn0opth2 11567  nn0opth2i 11566  nn0opthi 11565  omopthi 6902
[Quine] p. 177Definition 25.2df-rdg 6670
[Quine] p. 232Equation icarddom 8431
[Quine] p. 284Axiom 39(vi)funimaex 5533  funimaexg 5532
[Quine] p. 331Axiom system NFru 3162
[ReedSimon] p. 36Definition (iii)ax-his3 22588
[ReedSimon] p. 63Exercise 4(a)df-dip 22199  polid 22663  polid2i 22661  polidi 22662
[ReedSimon] p. 63Exercise 4(b)df-ph 22316
[ReedSimon] p. 195Remarklnophm 23524  lnophmi 23523
[Retherford] p. 49Exercise 1(i)leopadd 23637
[Retherford] p. 49Exercise 1(ii)leopmul 23639  leopmuli 23638
[Retherford] p. 49Exercise 1(iv)leoptr 23642
[Retherford] p. 49Definition VI.1df-leop 23357  leoppos 23631
[Retherford] p. 49Exercise 1(iii)leoptri 23641
[Retherford] p. 49Definition of operator orderingleop3 23630
[Rudin] p. 164Equation 27efcan 12699
[Rudin] p. 164Equation 30efzval 12705
[Rudin] p. 167Equation 48absefi 12799
[Sanford] p. 39Remarkax-mp 8  mto 170
[Sanford] p. 39Rule 3mtp-xor 1546
[Sanford] p. 39Rule 4mpto2 1544
[Sanford] p. 40Rule 1mpto1 1543
[Schechter] p. 51Definition of antisymmetryintasym 5251
[Schechter] p. 51Definition of irreflexivityintirr 5254
[Schechter] p. 51Definition of symmetrycnvsym 5250
[Schechter] p. 51Definition of transitivitycotr 5248
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13813
[Schechter] p. 79Definition of Moore closuredf-mrc 13814
[Schechter] p. 82Section 4.5df-mrc 13814
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13816
[Schechter] p. 139Definition AC3dfac9 8018
[Schechter] p. 141Definition (MC)dfac11 27139
[Schechter] p. 149Axiom DC1ax-dc 8328  axdc3 8336
[Schechter] p. 187Definition of ring with unitisrng 15670  isrngo 21968
[Schechter] p. 276Remark 11.6.espan0 23046
[Schechter] p. 276Definition of spandf-span 22813  spanval 22837
[Schechter] p. 428Definition 15.35bastop1 17060
[Schwabhauser] p. 10Axiom A1axcgrrflx 25855
[Schwabhauser] p. 10Axiom A2axcgrtr 25856
[Schwabhauser] p. 10Axiom A3axcgrid 25857
[Schwabhauser] p. 11Axiom A4axsegcon 25868
[Schwabhauser] p. 11Axiom A5ax5seg 25879
[Schwabhauser] p. 11Axiom A6axbtwnid 25880
[Schwabhauser] p. 12Axiom A7axpasch 25882
[Schwabhauser] p. 12Axiom A8axlowdim2 25901
[Schwabhauser] p. 13Axiom A10axeuclid 25904
[Schwabhauser] p. 13Axiom A11axcont 25917
[Schwabhauser] p. 27Theorem 2.1cgrrflx 25923
[Schwabhauser] p. 27Theorem 2.2cgrcomim 25925
[Schwabhauser] p. 27Theorem 2.3cgrtr 25928
[Schwabhauser] p. 27Theorem 2.4cgrcoml 25932
[Schwabhauser] p. 27Theorem 2.5cgrcomr 25933
[Schwabhauser] p. 28Theorem 2.8cgrtriv 25938
[Schwabhauser] p. 28Theorem 2.105segofs 25942
[Schwabhauser] p. 28Definition 2.10df-ofs 25919
[Schwabhauser] p. 29Theorem 2.11cgrextend 25944
[Schwabhauser] p. 29Theorem 2.12segconeq 25946
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 25958  btwntriv2 25948
[Schwabhauser] p. 30Theorem 3.2btwncomim 25949
[Schwabhauser] p. 30Theorem 3.3btwntriv1 25952
[Schwabhauser] p. 30Theorem 3.4btwnswapid 25953
[Schwabhauser] p. 30Theorem 3.5btwnexch2 25959  btwnintr 25955
[Schwabhauser] p. 30Theorem 3.6btwnexch 25961  btwnexch3 25956
[Schwabhauser] p. 30Theorem 3.7btwnouttr 25960
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25900
[Schwabhauser] p. 32Theorem 3.14btwndiff 25963
[Schwabhauser] p. 33Theorem 3.17trisegint 25964
[Schwabhauser] p. 34Theorem 4.2ifscgr 25980
[Schwabhauser] p. 34Definition 4.1df-ifs 25975
[Schwabhauser] p. 35Theorem 4.3cgrsub 25981
[Schwabhauser] p. 35Theorem 4.5cgrxfr 25991
[Schwabhauser] p. 35Definition 4.4df-cgr3 25976
[Schwabhauser] p. 36Theorem 4.6btwnxfr 25992
[Schwabhauser] p. 36Theorem 4.11colinearperm1 25998  colinearperm2 26000  colinearperm3 25999  colinearperm4 26001  colinearperm5 26002
[Schwabhauser] p. 36Definition 4.10df-colinear 25977
[Schwabhauser] p. 37Theorem 4.12colineartriv1 26003
[Schwabhauser] p. 37Theorem 4.13colinearxfr 26011
[Schwabhauser] p. 37Theorem 4.14lineext 26012
[Schwabhauser] p. 37Theorem 4.16fscgr 26016
[Schwabhauser] p. 37Theorem 4.17linecgr 26017
[Schwabhauser] p. 37Definition 4.15df-fs 25978
[Schwabhauser] p. 38Theorem 4.18lineid 26019
[Schwabhauser] p. 38Theorem 4.19idinside 26020
[Schwabhauser] p. 39Theorem 5.1btwnconn1 26037
[Schwabhauser] p. 41Theorem 5.2btwnconn2 26038
[Schwabhauser] p. 41Theorem 5.3btwnconn3 26039
[Schwabhauser] p. 41Theorem 5.5brsegle2 26045
[Schwabhauser] p. 41Definition 5.4df-segle 26043
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 26046
[Schwabhauser] p. 42Theorem 5.7seglerflx 26048
[Schwabhauser] p. 42Theorem 5.8segletr 26050
[Schwabhauser] p. 42Theorem 5.9segleantisym 26051
[Schwabhauser] p. 42Theorem 5.10seglelin 26052
[Schwabhauser] p. 42Theorem 5.11seglemin 26049
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 26054
[Schwabhauser] p. 43Theorem 6.2btwnoutside 26061
[Schwabhauser] p. 43Theorem 6.3broutsideof3 26062
[Schwabhauser] p. 43Theorem 6.4broutsideof 26057  df-outsideof 26056
[Schwabhauser] p. 43Definition 6.1broutsideof2 26058
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 26063
[Schwabhauser] p. 44Theorem 6.6outsideofcom 26064
[Schwabhauser] p. 44Theorem 6.7outsideoftr 26065
[Schwabhauser] p. 44Theorem 6.11outsideofeu 26067
[Schwabhauser] p. 44Definition 6.8df-ray 26074
[Schwabhauser] p. 45Part 2df-lines2 26075
[Schwabhauser] p. 45Theorem 6.13outsidele 26068
[Schwabhauser] p. 45Theorem 6.15lineunray 26083
[Schwabhauser] p. 45Theorem 6.16lineelsb2 26084
[Schwabhauser] p. 45Theorem 6.17linecom 26086  linerflx1 26085  linerflx2 26087
[Schwabhauser] p. 45Theorem 6.18linethru 26089
[Schwabhauser] p. 45Definition 6.14df-line2 26073
[Schwabhauser] p. 46Theorem 6.19linethrueu 26092
[Schwabhauser] p. 46Theorem 6.21lineintmo 26093
[Shapiro] p. 230Theorem 6.5.1dchrhash 21057  dchrsum 21055  dchrsum2 21054  sumdchr 21058
[Shapiro] p. 232Theorem 6.5.2dchr2sum 21059  sum2dchr 21060
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15626  ablfacrp2 15627
[Shapiro], p. 328Equation 9.2.4vmasum 21002
[Shapiro], p. 329Equation 9.2.7logfac2 21003
[Shapiro], p. 329Equation 9.2.9logfacrlim 21010
[Shapiro], p. 331Equation 9.2.13vmadivsum 21178
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 21181
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 21235  vmalogdivsum2 21234
[Shapiro], p. 375Theorem 9.4.1dirith 21225  dirith2 21224
[Shapiro], p. 375Equation 9.4.3rplogsum 21223  rpvmasum 21222  rpvmasum2 21208
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 21183
[Shapiro], p. 376Equation 9.4.8dchrvmasum 21221
[Shapiro], p. 377Lemma 9.4.1dchrisum 21188  dchrisumlem1 21185  dchrisumlem2 21186  dchrisumlem3 21187  dchrisumlema 21184
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 21191
[Shapiro], p. 379Equation 9.4.16dchrmusum 21220  dchrmusumlem 21218  dchrvmasumlem 21219
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 21190
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 21192
[Shapiro], p. 382Lemma 9.4.4dchrisum0 21216  dchrisum0re 21209  dchrisumn0 21217
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 21202
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 21206
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 21207
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 21262  pntrsumbnd2 21263  pntrsumo1 21261
[Shapiro], p. 405Equation 10.2.1mudivsum 21226
[Shapiro], p. 406Equation 10.2.6mulogsum 21228
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 21230
[Shapiro], p. 407Equation 10.2.8mulog2sum 21233
[Shapiro], p. 418Equation 10.4.6logsqvma 21238
[Shapiro], p. 418Equation 10.4.8logsqvma2 21239
[Shapiro], p. 419Equation 10.4.10selberg 21244
[Shapiro], p. 420Equation 10.4.12selberg2lem 21246
[Shapiro], p. 420Equation 10.4.14selberg2 21247
[Shapiro], p. 422Equation 10.6.7selberg3 21255
[Shapiro], p. 422Equation 10.4.20selberg4lem1 21256
[Shapiro], p. 422Equation 10.4.21selberg3lem1 21253  selberg3lem2 21254
[Shapiro], p. 422Equation 10.4.23selberg4 21257
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 21251
[Shapiro], p. 428Equation 10.6.2selbergr 21264
[Shapiro], p. 429Equation 10.6.8selberg3r 21265
[Shapiro], p. 430Equation 10.6.11selberg4r 21266
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 21280
[Shapiro], p. 434Equation 10.6.27pntlema 21292  pntlemb 21293  pntlemc 21291  pntlemd 21290  pntlemg 21294
[Shapiro], p. 435Equation 10.6.29pntlema 21292
[Shapiro], p. 436Lemma 10.6.1pntpbnd 21284
[Shapiro], p. 436Lemma 10.6.2pntibnd 21289
[Shapiro], p. 436Equation 10.6.34pntlema 21292
[Shapiro], p. 436Equation 10.6.35pntlem3 21305  pntleml 21307
[Stoll] p. 13Definition of symmetric differencesymdif1 3608
[Stoll] p. 16Exercise 4.40dif 3701  dif0 3700
[Stoll] p. 16Exercise 4.8difdifdir 3717
[Stoll] p. 17Theorem 5.1(5)undifv 3704
[Stoll] p. 19Theorem 5.2(13)undm 3601
[Stoll] p. 19Theorem 5.2(13')indm 3602
[Stoll] p. 20Remarkinvdif 3584
[Stoll] p. 25Definition of ordered tripledf-ot 3826
[Stoll] p. 43Definitionuniiun 4146
[Stoll] p. 44Definitionintiin 4147
[Stoll] p. 45Definitiondf-iin 4098
[Stoll] p. 45Definition indexed uniondf-iun 4097
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3608
[Strang] p. 242Section 6.3expgrowth 27531
[Suppes] p. 22Theorem 2eq0 3644
[Suppes] p. 22Theorem 4eqss 3365  eqssd 3367  eqssi 3366
[Suppes] p. 23Theorem 5ss0 3660  ss0b 3659
[Suppes] p. 23Theorem 6sstr 3358  sstrALT2 29009
[Suppes] p. 23Theorem 7pssirr 3449
[Suppes] p. 23Theorem 8pssn2lp 3450
[Suppes] p. 23Theorem 9psstr 3453
[Suppes] p. 23Theorem 10pssss 3444
[Suppes] p. 25Theorem 12elin 3532  elun 3490
[Suppes] p. 26Theorem 15inidm 3552
[Suppes] p. 26Theorem 16in0 3655
[Suppes] p. 27Theorem 23unidm 3492
[Suppes] p. 27Theorem 24un0 3654
[Suppes] p. 27Theorem 25ssun1 3512
[Suppes] p. 27Theorem 26ssequn1 3519
[Suppes] p. 27Theorem 27unss 3523
[Suppes] p. 27Theorem 28indir 3591
[Suppes] p. 27Theorem 29undir 3592
[Suppes] p. 28Theorem 32difid 3698  difidALT 3699
[Suppes] p. 29Theorem 33difin 3580
[Suppes] p. 29Theorem 34indif 3585
[Suppes] p. 29Theorem 35undif1 3705
[Suppes] p. 29Theorem 36difun2 3709
[Suppes] p. 29Theorem 37difin0 3703
[Suppes] p. 29Theorem 38disjdif 3702
[Suppes] p. 29Theorem 39difundi 3595
[Suppes] p. 29Theorem 40difindi 3597
[Suppes] p. 30Theorem 41nalset 4342
[Suppes] p. 39Theorem 61uniss 4038
[Suppes] p. 39Theorem 65uniop 4461
[Suppes] p. 41Theorem 70intsn 4088
[Suppes] p. 42Theorem 71intpr 4085  intprg 4086
[Suppes] p. 42Theorem 73op1stb 4760
[Suppes] p. 42Theorem 78intun 4084
[Suppes] p. 44Definition 15(a)dfiun2 4127  dfiun2g 4125
[Suppes] p. 44Definition 15(b)dfiin2 4128
[Suppes] p. 47Theorem 86elpw 3807  elpw2 4366  elpw2g 4365  elpwg 3808  elpwgdedVD 29091
[Suppes] p. 47Theorem 87pwid 3814
[Suppes] p. 47Theorem 89pw0 3947
[Suppes] p. 48Theorem 90pwpw0 3948
[Suppes] p. 52Theorem 101xpss12 4983
[Suppes] p. 52Theorem 102xpindi 5010  xpindir 5011
[Suppes] p. 52Theorem 103xpundi 4932  xpundir 4933
[Suppes] p. 54Theorem 105elirrv 7567
[Suppes] p. 58Theorem 2relss 4965
[Suppes] p. 59Theorem 4eldm 5069  eldm2 5070  eldm2g 5068  eldmg 5067
[Suppes] p. 59Definition 3df-dm 4890
[Suppes] p. 60Theorem 6dmin 5079
[Suppes] p. 60Theorem 8rnun 5282
[Suppes] p. 60Theorem 9rnin 5283
[Suppes] p. 60Definition 4dfrn2 5061
[Suppes] p. 61Theorem 11brcnv 5057  brcnvg 5055
[Suppes] p. 62Equation 5elcnv 5051  elcnv2 5052
[Suppes] p. 62Theorem 12relcnv 5244
[Suppes] p. 62Theorem 15cnvin 5281
[Suppes] p. 62Theorem 16cnvun 5279
[Suppes] p. 63Theorem 20co02 5385
[Suppes] p. 63Theorem 21dmcoss 5137
[Suppes] p. 63Definition 7df-co 4889
[Suppes] p. 64Theorem 26cnvco 5058
[Suppes] p. 64Theorem 27coass 5390
[Suppes] p. 65Theorem 31resundi 5162
[Suppes] p. 65Theorem 34elima 5210  elima2 5211  elima3 5212  elimag 5209
[Suppes] p. 65Theorem 35imaundi 5286
[Suppes] p. 66Theorem 40dminss 5288
[Suppes] p. 66Theorem 41imainss 5289
[Suppes] p. 67Exercise 11cnvxp 5292
[Suppes] p. 81Definition 34dfec2 6910
[Suppes] p. 82Theorem 72elec 6946  elecg 6945
[Suppes] p. 82Theorem 73erth 6951  erth2 6952
[Suppes] p. 83Theorem 74erdisj 6954
[Suppes] p. 89Theorem 96map0b 7054
[Suppes] p. 89Theorem 97map0 7056  map0g 7055
[Suppes] p. 89Theorem 98mapsn 7057
[Suppes] p. 89Theorem 99mapss 7058
[Suppes] p. 91Definition 12(ii)alephsuc 7951
[Suppes] p. 91Definition 12(iii)alephlim 7950
[Suppes] p. 92Theorem 1enref 7142  enrefg 7141
[Suppes] p. 92Theorem 2ensym 7158  ensymb 7157  ensymi 7159
[Suppes] p. 92Theorem 3entr 7161
[Suppes] p. 92Theorem 4unen 7191
[Suppes] p. 94Theorem 15endom 7136
[Suppes] p. 94Theorem 16ssdomg 7155
[Suppes] p. 94Theorem 17domtr 7162
[Suppes] p. 95Theorem 18sbth 7229
[Suppes] p. 97Theorem 23canth2 7262  canth2g 7263
[Suppes] p. 97Definition 3brsdom2 7233  df-sdom 7114  dfsdom2 7232
[Suppes] p. 97Theorem 21(i)sdomirr 7246
[Suppes] p. 97Theorem 22(i)domnsym 7235
[Suppes] p. 97Theorem 21(ii)sdomnsym 7234
[Suppes] p. 97Theorem 22(ii)domsdomtr 7244
[Suppes] p. 97Theorem 22(iv)brdom2 7139
[Suppes] p. 97Theorem 21(iii)sdomtr 7247
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7242
[Suppes] p. 98Exercise 4fundmen 7182  fundmeng 7183
[Suppes] p. 98Exercise 6xpdom3 7208
[Suppes] p. 98Exercise 11sdomentr 7243
[Suppes] p. 104Theorem 37fofi 7394
[Suppes] p. 104Theorem 38pwfi 7404
[Suppes] p. 105Theorem 40pwfi 7404
[Suppes] p. 111Axiom for cardinal numberscarden 8428
[Suppes] p. 130Definition 3df-tr 4305
[Suppes] p. 132Theorem 9ssonuni 4769
[Suppes] p. 134Definition 6df-suc 4589
[Suppes] p. 136Theorem Schema 22findes 4877  finds 4873  finds1 4876  finds2 4875
[Suppes] p. 151Theorem 42isfinite 7609  isfinite2 7367  isfiniteg 7369  unbnn 7365
[Suppes] p. 162Definition 5df-ltnq 8797  df-ltpq 8789
[Suppes] p. 197Theorem Schema 4tfindes 4844  tfinds 4841  tfinds2 4845
[Suppes] p. 209Theorem 18oaord1 6796
[Suppes] p. 209Theorem 21oaword2 6798
[Suppes] p. 211Theorem 25oaass 6806
[Suppes] p. 225Definition 8iscard2 7865
[Suppes] p. 227Theorem 56ondomon 8440
[Suppes] p. 228Theorem 59harcard 7867
[Suppes] p. 228Definition 12(i)aleph0 7949
[Suppes] p. 228Theorem Schema 61onintss 4633
[Suppes] p. 228Theorem Schema 62onminesb 4780  onminsb 4781
[Suppes] p. 229Theorem 64alephval2 8449
[Suppes] p. 229Theorem 65alephcard 7953
[Suppes] p. 229Theorem 66alephord2i 7960
[Suppes] p. 229Theorem 67alephnbtwn 7954
[Suppes] p. 229Definition 12df-aleph 7829
[Suppes] p. 242Theorem 6weth 8377
[Suppes] p. 242Theorem 8entric 8434
[Suppes] p. 242Theorem 9carden 8428
[TakeutiZaring] p. 8Axiom 1ax-ext 2419
[TakeutiZaring] p. 13Definition 4.5df-cleq 2431
[TakeutiZaring] p. 13Proposition 4.6df-clel 2434
[TakeutiZaring] p. 13Proposition 4.9cvjust 2433
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2455
[TakeutiZaring] p. 14Definition 4.16df-oprab 6087
[TakeutiZaring] p. 14Proposition 4.14ru 3162
[TakeutiZaring] p. 15Axiom 2zfpair 4403
[TakeutiZaring] p. 15Exercise 1elpr 3834  elpr2 3835  elprg 3833
[TakeutiZaring] p. 15Exercise 2elsn 3831  elsnc 3839  elsnc2 3845  elsnc2g 3844  elsncg 3838
[TakeutiZaring] p. 15Exercise 3elop 4431
[TakeutiZaring] p. 15Exercise 4sneq 3827  sneqr 3968
[TakeutiZaring] p. 15Definition 5.1dfpr2 3832  dfsn2 3830
[TakeutiZaring] p. 16Axiom 3uniex 4707
[TakeutiZaring] p. 16Exercise 6opth 4437
[TakeutiZaring] p. 16Exercise 7opex 4429
[TakeutiZaring] p. 16Exercise 8rext 4414
[TakeutiZaring] p. 16Corollary 5.8unex 4709  unexg 4712
[TakeutiZaring] p. 16Definition 5.3dftp2 3856
[TakeutiZaring] p. 16Definition 5.5df-uni 4018
[TakeutiZaring] p. 16Definition 5.6df-in 3329  df-un 3327
[TakeutiZaring] p. 16Proposition 5.7unipr 4031  uniprg 4032
[TakeutiZaring] p. 17Axiom 4pwex 4384  pwexg 4385
[TakeutiZaring] p. 17Exercise 1eltp 3855
[TakeutiZaring] p. 17Exercise 5elsuc 4652  elsucg 4650  sstr2 3357
[TakeutiZaring] p. 17Exercise 6uncom 3493
[TakeutiZaring] p. 17Exercise 7incom 3535
[TakeutiZaring] p. 17Exercise 8unass 3506
[TakeutiZaring] p. 17Exercise 9inass 3553
[TakeutiZaring] p. 17Exercise 10indi 3589
[TakeutiZaring] p. 17Exercise 11undi 3590
[TakeutiZaring] p. 17Definition 5.9df-pss 3338  dfss2 3339
[TakeutiZaring] p. 17Definition 5.10df-pw 3803
[TakeutiZaring] p. 18Exercise 7unss2 3520
[TakeutiZaring] p. 18Exercise 9df-ss 3336  sseqin2 3562
[TakeutiZaring] p. 18Exercise 10ssid 3369
[TakeutiZaring] p. 18Exercise 12inss1 3563  inss2 3564
[TakeutiZaring] p. 18Exercise 13nss 3408
[TakeutiZaring] p. 18Exercise 15unieq 4026
[TakeutiZaring] p. 18Exercise 18sspwb 4415  sspwimp 29092  sspwimpALT 29099  sspwimpALT2 29102  sspwimpcf 29094
[TakeutiZaring] p. 18Exercise 19pweqb 4422
[TakeutiZaring] p. 19Axiom 5ax-rep 4322
[TakeutiZaring] p. 20Definitiondf-rab 2716
[TakeutiZaring] p. 20Corollary 5.160ex 4341
[TakeutiZaring] p. 20Definition 5.12df-dif 3325
[TakeutiZaring] p. 20Definition 5.14dfnul2 3632
[TakeutiZaring] p. 20Proposition 5.15difid 3698  difidALT 3699
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3639  n0f 3638  neq0 3640
[TakeutiZaring] p. 21Axiom 6zfreg 7565
[TakeutiZaring] p. 21Axiom 6'zfregs 7670
[TakeutiZaring] p. 21Theorem 5.22setind 7675
[TakeutiZaring] p. 21Definition 5.20df-v 2960
[TakeutiZaring] p. 21Proposition 5.21vprc 4343
[TakeutiZaring] p. 22Exercise 10ss 3658
[TakeutiZaring] p. 22Exercise 3ssex 4349  ssexg 4351
[TakeutiZaring] p. 22Exercise 4inex1 4346
[TakeutiZaring] p. 22Exercise 5ruv 7570
[TakeutiZaring] p. 22Exercise 6elirr 7568
[TakeutiZaring] p. 22Exercise 7ssdif0 3688
[TakeutiZaring] p. 22Exercise 11difdif 3475
[TakeutiZaring] p. 22Exercise 13undif3 3604  undif3VD 29056
[TakeutiZaring] p. 22Exercise 14difss 3476
[TakeutiZaring] p. 22Exercise 15sscon 3483
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2712
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2713
[TakeutiZaring] p. 23Proposition 6.2xpex 4992  xpexg 4991  xpexgALT 6299
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4887
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5515
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5649  fun11 5518
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5468  svrelfun 5516
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5060
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5062
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4892
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4893
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4889
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5327  dfrel2 5323
[TakeutiZaring] p. 25Exercise 3xpss 4984
[TakeutiZaring] p. 25Exercise 5relun 4993
[TakeutiZaring] p. 25Exercise 6reluni 4999
[TakeutiZaring] p. 25Exercise 9inxp 5009
[TakeutiZaring] p. 25Exercise 12relres 5176
[TakeutiZaring] p. 25Exercise 13opelres 5153  opelresg 5155
[TakeutiZaring] p. 25Exercise 14dmres 5169
[TakeutiZaring] p. 25Exercise 15resss 5172
[TakeutiZaring] p. 25Exercise 17resabs1 5177
[TakeutiZaring] p. 25Exercise 18funres 5494
[TakeutiZaring] p. 25Exercise 24relco 5370
[TakeutiZaring] p. 25Exercise 29funco 5493
[TakeutiZaring] p. 25Exercise 30f1co 5650
[TakeutiZaring] p. 26Definition 6.10eu2 2308
[TakeutiZaring] p. 26Definition 6.11conventions 21712  df-fv 5464  fv3 5746
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5408  cnvexg 5407
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5134  dmexg 5132
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5135  rnexg 5133
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27636
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27637
[TakeutiZaring] p. 27Corollary 6.13fvex 5744
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 28016  tz6.12-1 5749  tz6.12-afv 28015  tz6.12 5750  tz6.12c 5752
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5721  tz6.12i 5753
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5459
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5460
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5462  wfo 5454
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5461  wf1 5453
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5463  wf1o 5455
[TakeutiZaring] p. 28Exercise 4eqfnfv 5829  eqfnfv2 5830  eqfnfv2f 5833
[TakeutiZaring] p. 28Exercise 5fvco 5801
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5963  fnexALT 5964
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5959  resfunexgALT 5960
[TakeutiZaring] p. 29Exercise 9funimaex 5533  funimaexg 5532
[TakeutiZaring] p. 29Definition 6.18df-br 4215
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4506
[TakeutiZaring] p. 30Definition 6.21dffr2 4549  dffr3 5238  eliniseg 5235  iniseg 5237
[TakeutiZaring] p. 30Definition 6.22df-eprel 4496
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4562  fr3nr 4762  frirr 4561
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4543
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4764
[TakeutiZaring] p. 31Exercise 1frss 4551
[TakeutiZaring] p. 31Exercise 4wess 4571
[TakeutiZaring] p. 31Proposition 6.26tz6.26 25482  tz6.26i 25483  wefrc 4578  wereu2 4581
[TakeutiZaring] p. 32Theorem 6.27wfi 25484  wfii 25485
[TakeutiZaring] p. 32Definition 6.28df-isom 5465
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6051
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6052
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6058
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6059
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6060
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6064
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6071
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6073
[TakeutiZaring] p. 35Notationwtr 4304
[TakeutiZaring] p. 35Theorem 7.2trelpss 27638  tz7.2 4568
[TakeutiZaring] p. 35Definition 7.1dftr3 4308
[TakeutiZaring] p. 36Proposition 7.4ordwe 4596
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4604
[TakeutiZaring] p. 36Proposition 7.6ordelord 4605  ordelordALT 28684  ordelordALTVD 29041
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4611  ordelssne 4610
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4609
[TakeutiZaring] p. 37Proposition 7.9ordin 4613
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4771
[TakeutiZaring] p. 38Corollary 7.15ordsson 4772
[TakeutiZaring] p. 38Definition 7.11df-on 4587
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4615
[TakeutiZaring] p. 38Proposition 7.12onfrALT 28697  ordon 4765
[TakeutiZaring] p. 38Proposition 7.13onprc 4767
[TakeutiZaring] p. 39Theorem 7.17tfi 4835
[TakeutiZaring] p. 40Exercise 3ontr2 4630
[TakeutiZaring] p. 40Exercise 7dftr2 4306
[TakeutiZaring] p. 40Exercise 9onssmin 4779
[TakeutiZaring] p. 40Exercise 11unon 4813
[TakeutiZaring] p. 40Exercise 12ordun 4685
[TakeutiZaring] p. 40Exercise 14ordequn 4684
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4768
[TakeutiZaring] p. 40Proposition 7.20elssuni 4045
[TakeutiZaring] p. 41Definition 7.22df-suc 4589
[TakeutiZaring] p. 41Proposition 7.23sssucid 4660  sucidg 4661
[TakeutiZaring] p. 41Proposition 7.24suceloni 4795
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4675  ordnbtwn 4674
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4810
[TakeutiZaring] p. 42Exercise 1df-lim 4588
[TakeutiZaring] p. 42Exercise 4omssnlim 4861
[TakeutiZaring] p. 42Exercise 7ssnlim 4865
[TakeutiZaring] p. 42Exercise 8onsucssi 4823  ordelsuc 4802
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4804
[TakeutiZaring] p. 42Definition 7.27nlimon 4833
[TakeutiZaring] p. 42Definition 7.28dfom2 4849
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4866
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4867
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4868
[TakeutiZaring] p. 43Remarkomon 4858
[TakeutiZaring] p. 43Axiom 7inf3 7592  omex 7600
[TakeutiZaring] p. 43Theorem 7.32ordom 4856
[TakeutiZaring] p. 43Corollary 7.31find 4872
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4869
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4870
[TakeutiZaring] p. 44Exercise 1limomss 4852
[TakeutiZaring] p. 44Exercise 2int0 4066  trint0 4321
[TakeutiZaring] p. 44Exercise 4intss1 4067
[TakeutiZaring] p. 44Exercise 5intex 4358
[TakeutiZaring] p. 44Exercise 6oninton 4782
[TakeutiZaring] p. 44Exercise 11ordintdif 4632
[TakeutiZaring] p. 44Definition 7.35df-int 4053
[TakeutiZaring] p. 44Proposition 7.34noinfep 7616
[TakeutiZaring] p. 45Exercise 4onint 4777
[TakeutiZaring] p. 47Lemma 1tfrlem1 6638
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6660
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6661
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6662
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6666  tz7.44-2 6667  tz7.44-3 6668
[TakeutiZaring] p. 50Exercise 1smogt 6631
[TakeutiZaring] p. 50Exercise 3smoiso 6626
[TakeutiZaring] p. 50Definition 7.46df-smo 6610
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6704  tz7.49c 6705
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6702
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6701
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6703
[TakeutiZaring] p. 53Proposition 7.532eu5 2367
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7895
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7896
[TakeutiZaring] p. 56Definition 8.1oalim 6778  oasuc 6770
[TakeutiZaring] p. 57Remarktfindsg 4842
[TakeutiZaring] p. 57Proposition 8.2oacl 6781
[TakeutiZaring] p. 57Proposition 8.3oa0 6762  oa0r 6784
[TakeutiZaring] p. 57Proposition 8.16omcl 6782
[TakeutiZaring] p. 58Corollary 8.5oacan 6793
[TakeutiZaring] p. 58Proposition 8.4nnaord 6864  nnaordi 6863  oaord 6792  oaordi 6791
[TakeutiZaring] p. 59Proposition 8.6iunss2 4138  uniss2 4048
[TakeutiZaring] p. 59Proposition 8.7oawordri 6795
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6800  oawordex 6802
[TakeutiZaring] p. 59Proposition 8.9nnacl 6856
[TakeutiZaring] p. 59Proposition 8.10oaabs 6889
[TakeutiZaring] p. 60Remarkoancom 7608
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6805
[TakeutiZaring] p. 62Exercise 1nnarcl 6861
[TakeutiZaring] p. 62Exercise 5oaword1 6797
[TakeutiZaring] p. 62Definition 8.15om0 6763  om0x 6765  omlim 6779  omsuc 6772
[TakeutiZaring] p. 63Proposition 8.17nnecl 6858  nnmcl 6857
[TakeutiZaring] p. 63Proposition 8.19nnmord 6877  nnmordi 6876  omord 6813  omordi 6811
[TakeutiZaring] p. 63Proposition 8.20omcan 6814
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6881  omwordri 6817
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6785
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6787  om1r 6788
[TakeutiZaring] p. 64Proposition 8.22om00 6820
[TakeutiZaring] p. 64Proposition 8.23omordlim 6822
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6823
[TakeutiZaring] p. 64Proposition 8.25odi 6824
[TakeutiZaring] p. 65Theorem 8.26omass 6825
[TakeutiZaring] p. 67Definition 8.30nnesuc 6853  oe0 6768  oelim 6780  oesuc 6773  onesuc 6776
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6766
[TakeutiZaring] p. 67Proposition 8.32oen0 6831
[TakeutiZaring] p. 67Proposition 8.33oeordi 6832
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6767
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6790
[TakeutiZaring] p. 68Corollary 8.34oeord 6833
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6839
[TakeutiZaring] p. 68Proposition 8.35oewordri 6837
[TakeutiZaring] p. 68Proposition 8.37oeworde 6838
[TakeutiZaring] p. 69Proposition 8.41oeoa 6842
[TakeutiZaring] p. 70Proposition 8.42oeoe 6844
[TakeutiZaring] p. 73Theorem 9.1trcl 7666  tz9.1 7667
[TakeutiZaring] p. 76Definition 9.9df-r1 7692  r10 7696  r1lim 7700  r1limg 7699  r1suc 7698  r1sucg 7697
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7708  r1ord2 7709  r1ordg 7706
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7718
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7743  tz9.13 7719  tz9.13g 7720
[TakeutiZaring] p. 79Definition 9.14df-rank 7693  rankval 7744  rankvalb 7725  rankvalg 7745
[TakeutiZaring] p. 79Proposition 9.16rankel 7767  rankelb 7752
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7781  rankval3 7768  rankval3b 7754
[TakeutiZaring] p. 79Proposition 9.18rankonid 7757
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7723
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7762  rankr1c 7749  rankr1g 7760
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7763
[TakeutiZaring] p. 80Exercise 1rankss 7777  rankssb 7776
[TakeutiZaring] p. 80Exercise 2unbndrank 7770
[TakeutiZaring] p. 80Proposition 9.19bndrank 7769
[TakeutiZaring] p. 83Axiom of Choiceac4 8357  dfac3 8004
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7913  numth 8354  numth2 8353
[TakeutiZaring] p. 85Definition 10.4cardval 8423
[TakeutiZaring] p. 85Proposition 10.5cardid 8424  cardid2 7842
[TakeutiZaring] p. 85Proposition 10.9oncard 7849
[TakeutiZaring] p. 85Proposition 10.10carden 8428
[TakeutiZaring] p. 85Proposition 10.11cardidm 7848
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7833
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7854
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7846
[TakeutiZaring] p. 87Proposition 10.15pwen 7282
[TakeutiZaring] p. 88Exercise 1en0 7172
[TakeutiZaring] p. 88Exercise 7infensuc 7287
[TakeutiZaring] p. 89Exercise 10omxpen 7212
[TakeutiZaring] p. 90Corollary 10.23cardnn 7852
[TakeutiZaring] p. 90Definition 10.27alephiso 7981
[TakeutiZaring] p. 90Proposition 10.20nneneq 7292
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7298
[TakeutiZaring] p. 90Proposition 10.26alephprc 7982
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7297
[TakeutiZaring] p. 91Exercise 2alephle 7971
[TakeutiZaring] p. 91Exercise 3aleph0 7949
[TakeutiZaring] p. 91Exercise 4cardlim 7861
[TakeutiZaring] p. 91Exercise 7infpss 8099
[TakeutiZaring] p. 91Exercise 8infcntss 7382
[TakeutiZaring] p. 91Definition 10.29df-fin 7115  isfi 7133
[TakeutiZaring] p. 92Proposition 10.32onfin 7299
[TakeutiZaring] p. 92Proposition 10.34imadomg 8414
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 7205
[TakeutiZaring] p. 93Proposition 10.35fodomb 8406
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8071  unxpdom 7318
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7863  cardsdomelir 7862
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7320
[TakeutiZaring] p. 94Proposition 10.39infxpen 7898
[TakeutiZaring] p. 95Definition 10.42df-map 7022
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8439  infxpidm2 7900
[TakeutiZaring] p. 95Proposition 10.41infcda 8090  infxp 8097
[TakeutiZaring] p. 96Proposition 10.44pw2en 7217  pw2f1o 7215
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7275
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8369
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8364  ac6s5 8373
[TakeutiZaring] p. 98Theorem 10.47unidom 8420
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8421  uniimadomf 8422
[TakeutiZaring] p. 100Definition 11.1cfcof 8156
[TakeutiZaring] p. 101Proposition 11.7cofsmo 8151
[TakeutiZaring] p. 102Exercise 1cfle 8136
[TakeutiZaring] p. 102Exercise 2cf0 8133
[TakeutiZaring] p. 102Exercise 3cfsuc 8139
[TakeutiZaring] p. 102Exercise 4cfom 8146
[TakeutiZaring] p. 102Proposition 11.9coftr 8155
[TakeutiZaring] p. 103Theorem 11.15alephreg 8459
[TakeutiZaring] p. 103Proposition 11.11cardcf 8134
[TakeutiZaring] p. 103Proposition 11.13alephsing 8158
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7980
[TakeutiZaring] p. 104Proposition 11.16carduniima 7979
[TakeutiZaring] p. 104Proposition 11.18alephfp 7991  alephfp2 7992
[TakeutiZaring] p. 106Theorem 11.20gchina 8576
[TakeutiZaring] p. 106Theorem 11.21mappwen 7995
[TakeutiZaring] p. 107Theorem 11.26konigth 8446
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8460
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8461
[Tarski] p. 67Axiom B5ax-4 2214
[Tarski] p. 67Scheme B5sp 1764
[Tarski] p. 68Lemma 6avril1 21759  equid 1689  equid1 2237  equid1ALT 2255
[Tarski] p. 69Lemma 7equcomi 1692
[Tarski] p. 70Lemma 14spim 1958  spime 1963  spimeh 1680
[Tarski] p. 70Lemma 16ax-11 1762  ax-11o 2220  ax11i 1658
[Tarski] p. 70Lemmas 16 and 17sb6 2177
[Tarski] p. 75Axiom B7ax9v 1668
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1627  ax17o 2236
[Tarski], p. 75Scheme B8 of system S2ax-13 1728  ax-14 1730  ax-8 1688
[Truss] p. 114Theorem 5.18ruc 12844
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 26247
[Viaclovsky8] p. 3Proposition 7ismblfin 26249
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 501
[WhiteheadRussell] p. 96Axiom *1.3olc 375
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 377
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 510
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 816
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 163
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 111
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 79
[WhiteheadRussell] p. 100Theorem *2.05imim2 52
[WhiteheadRussell] p. 100Theorem *2.06imim1 73
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 408
[WhiteheadRussell] p. 101Theorem *2.06barbara 2380  syl 16
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 387
[WhiteheadRussell] p. 101Theorem *2.08id 21  id1 22
[WhiteheadRussell] p. 101Theorem *2.11exmid 406
[WhiteheadRussell] p. 101Theorem *2.12notnot1 117
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 409
[WhiteheadRussell] p. 102Theorem *2.14notnot2 107  notnot2ALT2 29101
[WhiteheadRussell] p. 102Theorem *2.15con1 123
[WhiteheadRussell] p. 103Theorem *2.16con3 129  con3th 926
[WhiteheadRussell] p. 103Theorem *2.17ax-3 7
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 105
[WhiteheadRussell] p. 104Theorem *2.2orc 376
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 557
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 103
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 104
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 395
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 855
[WhiteheadRussell] p. 104Theorem *2.27conventions 21712  pm2.27 38
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 513
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 514
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 818
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 819
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 817
[WhiteheadRussell] p. 105Definition *2.33df-3or 938
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 560
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 558
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 559
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 50
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 388
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 389
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 147
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 165
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 390
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 391
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 392
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 148
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 150
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 364
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 365
[WhiteheadRussell] p. 107Theorem *2.55orel1 373
[WhiteheadRussell] p. 107Theorem *2.56orel2 374
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 166
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 400
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 765
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 766
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 167
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 393  pm2.67 394
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 149
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 399
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 825
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 401
[WhiteheadRussell] p. 108Theorem *2.69looinv 176
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 820
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 821
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 824
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 823
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 826
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 827
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 74
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 828
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 97
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 486
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 436  pm3.2im 140
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 487
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 488
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 489
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 490
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 437
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 438
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 854
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 572
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 433
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 434
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 445  simplim 146
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 449  simprim 145
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 570
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 571
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 564
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 546
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 544
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 545
[WhiteheadRussell] p. 113Theorem *3.44jao 500  pm3.44 499
[WhiteheadRussell] p. 113Theorem *3.47prth 556
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 834
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 809
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 808
[WhiteheadRussell] p. 116Theorem *4.1con34b 285
[WhiteheadRussell] p. 117Theorem *4.2biid 229
[WhiteheadRussell] p. 117Theorem *4.11notbi 288
[WhiteheadRussell] p. 117Theorem *4.12con2bi 320
[WhiteheadRussell] p. 117Theorem *4.13notnot 284
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 563
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 566
[WhiteheadRussell] p. 117Theorem *4.21bicom 193
[WhiteheadRussell] p. 117Theorem *4.22biantr 899  bitr 691  wl-bitr 26232
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 626
[WhiteheadRussell] p. 117Theorem *4.25oridm 502  pm4.25 503
[WhiteheadRussell] p. 118Theorem *4.3ancom 439
[WhiteheadRussell] p. 118Theorem *4.4andi 839
[WhiteheadRussell] p. 118Theorem *4.31orcom 378
[WhiteheadRussell] p. 118Theorem *4.32anass 632
[WhiteheadRussell] p. 118Theorem *4.33orass 512
[WhiteheadRussell] p. 118Theorem *4.36anbi1 689
[WhiteheadRussell] p. 118Theorem *4.37orbi1 688
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 844
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 843
[WhiteheadRussell] p. 118Definition *4.34df-3an 939
[WhiteheadRussell] p. 119Theorem *4.41ordi 836
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 928
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 895
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 562
[WhiteheadRussell] p. 119Theorem *4.45orabs 830  pm4.45 671  pm4.45im 547
[WhiteheadRussell] p. 120Theorem *4.5anor 477
[WhiteheadRussell] p. 120Theorem *4.6imor 403
[WhiteheadRussell] p. 120Theorem *4.7anclb 532
[WhiteheadRussell] p. 120Theorem *4.51ianor 476
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 479
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 480
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 481
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 482
[WhiteheadRussell] p. 120Theorem *4.56ioran 478  pm4.56 483
[WhiteheadRussell] p. 120Theorem *4.57oran 484  pm4.57 485
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 417
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 410
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 412
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 363
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 418
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 411
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 419
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 613  pm4.71d 617  pm4.71i 615  pm4.71r 614  pm4.71rd 618  pm4.71ri 616
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 848
[WhiteheadRussell] p. 121Theorem *4.73iba 491
[WhiteheadRussell] p. 121Theorem *4.74biorf 396
[WhiteheadRussell] p. 121Theorem *4.76jcab 835  pm4.76 838
[WhiteheadRussell] p. 121Theorem *4.77jaob 760  pm4.77 764
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 567
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 568
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 356
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 357
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 896
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 897
[WhiteheadRussell] p. 122Theorem *4.84imbi1 315
[WhiteheadRussell] p. 122Theorem *4.85imbi2 316
[WhiteheadRussell] p. 122Theorem *4.86bibi1 319  wl-bibi1 26225
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 352  impexp 435  pm4.87 569
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 832
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 856
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 857
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 859
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 858
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 861
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 862
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 860
[WhiteheadRussell] p. 124Theorem *5.18nbbn 349  pm5.18 347
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 351
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 833
[WhiteheadRussell] p. 124Theorem *5.22xor 863
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 865
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 866
[WhiteheadRussell] p. 124Theorem *5.25dfor2 402
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 694
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 353
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 328
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 880
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 902
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 573
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 619
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 850
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 871
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 851
[WhiteheadRussell] p. 125Theorem *5.41imdi 354  pm5.41 355
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 533
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 879
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 773
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 872
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 869
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 695
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 891
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 892
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 904
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 332
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 237
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 905
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 27532
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27533
[WhiteheadRussell] p. 147Theorem *10.2219.26 1604
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27534
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27535
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27536
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1626
[WhiteheadRussell] p. 151Theorem *10.301albitr 27537
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27538
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27539
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27540
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27541
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27543
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27544
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27545
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27542
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2193
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27548
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27549
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27550
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1754
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27551
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27552
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27553
[WhiteheadRussell] p. 162Theorem *11.322alim 27554
[WhiteheadRussell] p. 162Theorem *11.332albi 27555
[WhiteheadRussell] p. 162Theorem *11.342exim 27556
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27558
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27557
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1621
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27560
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27561
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27559
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1583
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27562
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27563
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1591
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27564
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1917
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27565
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27570
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27566
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27567
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27568
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27569
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27574
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27571
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27572
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27573
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27575
[WhiteheadRussell] p. 175Definition *14.02df-eu 2287
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27586  pm13.13b 27587
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27588
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2678
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2679
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3078
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27594
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27595
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27589
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 28701  pm13.193 27590
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27591
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27592
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27593
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27600
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27599
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27598
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3215
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27601  pm14.122b 27602  pm14.122c 27603
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27604  pm14.123b 27605  pm14.123c 27606
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27608
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27607
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27609
[WhiteheadRussell] p. 190Theorem *14.22iota4 5438
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27610
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5439
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27611
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27613
[WhiteheadRussell] p. 192Theorem *14.26eupick 2346  eupickbi 2349  sbaniota 27614
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27612
[WhiteheadRussell] p. 192Theorem *14.271eubi 27615
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27616
[WhiteheadRussell] p. 235Definition *30.01conventions 21712  df-fv 5464
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7889  pm54.43lem 7888
[Young] p. 141Definition of operator orderingleop2 23629
[Young] p. 142Example 12.2(i)0leop 23635  idleop 23636
[vandenDries] p. 42Lemma 61irrapx1 26893
[vandenDries] p. 43Theorem 62pellex 26900  pellexlem1 26894

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