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 13658
[Adamek] p. 29Proposition 3.14(1)invinv 13672
[Adamek] p. 29Proposition 3.14(2)invco 13673  isoco 13675
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 26190
[AitkenIBCG] p. 3Definition 2df-angtrg 26186  df-trcng 26189
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 26062  df-ig2 26061
[AitkenIBG] p. 2Definition 4df-li 26077
[AitkenIBG] p. 3Definition 5df-col 26091
[AitkenIBG] p. 3Definition 6df-con2 26096
[AitkenIBG] p. 3Proposition 4isconcl5a 26101  isconcl5ab 26102  isconcl6a 26103  isconcl6ab 26104
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 26109
[AitkenIBG] p. 4Exercise 5tpne 26075
[AitkenIBG] p. 4Definition 8df-seg2 26131
[AitkenIBG] p. 4Definition 10df-sside 26163
[AitkenIBG] p. 4Definition 11df-ray2 26152
[AitkenIBG] p. 10Definition 17df-angle 26158
[AitkenIBG] p. 15Definition 23df-triangle 26160
[AitkenIBG] p. 15Definition 24df-cnvx 26179
[AitkenNG] p. 2Definition 1df-slices 26193
[AitkenNG] p. 2Definition 2df-Cut 26195
[AitkenNG] p. 3Axiom of Dedekinddf-neug 26197
[AitkenNG] p. 4Definition 5df-crcl 26199
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18217  df-nmoo 21323
[AkhiezerGlazman] p. 64Theoremhmopidmch 22733  hmopidmchi 22731
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22781  pjcmul2i 22782
[AkhiezerGlazman] p. 72Theoremcnvunop 22498  unoplin 22500
[AkhiezerGlazman] p. 72Equation 2unopadj 22499  unopadj2 22518
[AkhiezerGlazman] p. 73Theoremelunop2 22593  lnopunii 22592
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22666
[Apostol] p. 18Theorem I.1addcan 8996  addcan2d 9016  addcan2i 9006  addcand 9015  addcani 9005
[Apostol] p. 18Theorem I.2negeu 9042
[Apostol] p. 18Theorem I.3negsub 9095  negsubd 9163  negsubi 9124
[Apostol] p. 18Theorem I.4negneg 9097  negnegd 9148  negnegi 9116
[Apostol] p. 18Theorem I.5subdi 9213  subdid 9235  subdii 9228  subdir 9214  subdird 9236  subdiri 9229
[Apostol] p. 18Theorem I.6mul01 8991  mul01d 9011  mul01i 9002  mul02 8990  mul02d 9010  mul02i 9001
[Apostol] p. 18Theorem I.7mulcan 9405  mulcan2d 9402  mulcand 9401  mulcani 9407
[Apostol] p. 18Theorem I.8receu 9413  xreceu 23105
[Apostol] p. 18Theorem I.9divrec 9440  divrecd 9539  divreci 9505  divreczi 9498
[Apostol] p. 18Theorem I.10recrec 9457  recreci 9492
[Apostol] p. 18Theorem I.11mul0or 9408  mul0ord 9418  mul0ori 9416
[Apostol] p. 18Theorem I.12mul2neg 9219  mul2negd 9234  mul2negi 9227  mulneg1 9216  mulneg1d 9232  mulneg1i 9225
[Apostol] p. 18Theorem I.13divadddiv 9475  divadddivd 9580  divadddivi 9522
[Apostol] p. 18Theorem I.14divmuldiv 9460  divmuldivd 9577  divmuldivi 9520
[Apostol] p. 18Theorem I.15divdivdiv 9461  divdivdivd 9583  divdivdivi 9523
[Apostol] p. 20Axiom 7rpaddcl 10374  rpaddcld 10405  rpmulcl 10375  rpmulcld 10406
[Apostol] p. 20Axiom 8rpneg 10383
[Apostol] p. 20Axiom 90nrp 10384
[Apostol] p. 20Theorem I.17lttri 8945
[Apostol] p. 20Theorem I.18ltadd1d 9365  ltadd1dd 9383  ltadd1i 9327
[Apostol] p. 20Theorem I.19ltmul1 9606  ltmul1a 9605  ltmul1i 9675  ltmul1ii 9685  ltmul2 9607  ltmul2d 10428  ltmul2dd 10442  ltmul2i 9678
[Apostol] p. 20Theorem I.20msqgt0 9294  msqgt0d 9340  msqgt0i 9310
[Apostol] p. 20Theorem I.210lt1 9296
[Apostol] p. 20Theorem I.23lt0neg1 9280  lt0neg1d 9342  ltneg 9274  ltnegd 9350  ltnegi 9317
[Apostol] p. 20Theorem I.25lt2add 9259  lt2addd 9394  lt2addi 9335
[Apostol] p. 20Definition of positive numbersdf-rp 10355
[Apostol] p. 21Exercise 4recgt0 9600  recgt0d 9691  recgt0i 9661  recgt0ii 9662
[Apostol] p. 22Definition of integersdf-z 10025
[Apostol] p. 22Definition of positive integersdfnn3 9760
[Apostol] p. 22Definition of rationalsdf-q 10317
[Apostol] p. 24Theorem I.26supeu 7205
[Apostol] p. 26Theorem I.28nnunb 9961
[Apostol] p. 26Theorem I.29arch 9962
[Apostol] p. 28Exercise 2btwnz 10114
[Apostol] p. 28Exercise 3nnrecl 9963
[Apostol] p. 28Exercise 4rebtwnz 10315
[Apostol] p. 28Exercise 5zbtwnre 10314
[Apostol] p. 28Exercise 6qbtwnre 10526
[Apostol] p. 28Exercise 10(a)zneo 10094
[Apostol] p. 29Theorem I.35msqsqrd 11922  resqrth 11741  sqrth 11848  sqrthi 11854  sqsqrd 11921
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9749
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10284
[Apostol] p. 361Remarkcrreczi 11226
[Apostol] p. 363Remarkabsgt0i 11882
[Apostol] p. 363Exampleabssubd 11935  abssubi 11886
[Baer] p. 40Property (b)mapdord 31828
[Baer] p. 40Property (c)mapd11 31829
[Baer] p. 40Property (e)mapdin 31852  mapdlsm 31854
[Baer] p. 40Property (f)mapd0 31855
[Baer] p. 40Definition of projectivitydf-mapd 31815  mapd1o 31838
[Baer] p. 41Property (g)mapdat 31857
[Baer] p. 44Part (1)mapdpg 31896
[Baer] p. 45Part (2)hdmap1eq 31992  mapdheq 31918  mapdheq2 31919  mapdheq2biN 31920
[Baer] p. 45Part (3)baerlem3 31903
[Baer] p. 46Part (4)mapdheq4 31922  mapdheq4lem 31921
[Baer] p. 46Part (5)baerlem5a 31904  baerlem5abmN 31908  baerlem5amN 31906  baerlem5b 31905  baerlem5bmN 31907
[Baer] p. 47Part (6)hdmap1l6 32012  hdmap1l6a 32000  hdmap1l6e 32005  hdmap1l6f 32006  hdmap1l6g 32007  hdmap1l6lem1 31998  hdmap1l6lem2 31999  hdmap1p6N 32013  mapdh6N 31937  mapdh6aN 31925  mapdh6eN 31930  mapdh6fN 31931  mapdh6gN 31932  mapdh6lem1N 31923  mapdh6lem2N 31924
[Baer] p. 48Part 9hdmapval 32021
[Baer] p. 48Part 10hdmap10 32033
[Baer] p. 48Part 11hdmapadd 32036
[Baer] p. 48Part (6)hdmap1l6h 32008  mapdh6hN 31933
[Baer] p. 48Part (7)mapdh75cN 31943  mapdh75d 31944  mapdh75e 31942  mapdh75fN 31945  mapdh7cN 31939  mapdh7dN 31940  mapdh7eN 31938  mapdh7fN 31941
[Baer] p. 48Part (8)mapdh8 31979  mapdh8a 31965  mapdh8aa 31966  mapdh8ab 31967  mapdh8ac 31968  mapdh8ad 31969  mapdh8b 31970  mapdh8c 31971  mapdh8d 31973  mapdh8d0N 31972  mapdh8e 31974  mapdh8fN 31975  mapdh8g 31976  mapdh8i 31977  mapdh8j 31978
[Baer] p. 48Part (9)mapdh9a 31980
[Baer] p. 48Equation 10mapdhvmap 31959
[Baer] p. 49Part 12hdmap11 32041  hdmapeq0 32037  hdmapf1oN 32058  hdmapneg 32039  hdmaprnN 32057  hdmaprnlem1N 32042  hdmaprnlem3N 32043  hdmaprnlem3uN 32044  hdmaprnlem4N 32046  hdmaprnlem6N 32047  hdmaprnlem7N 32048  hdmaprnlem8N 32049  hdmaprnlem9N 32050  hdmapsub 32040
[Baer] p. 49Part 14hdmap14lem1 32061  hdmap14lem10 32070  hdmap14lem1a 32059  hdmap14lem2N 32062  hdmap14lem2a 32060  hdmap14lem3 32063  hdmap14lem8 32068  hdmap14lem9 32069
[Baer] p. 50Part 14hdmap14lem11 32071  hdmap14lem12 32072  hdmap14lem13 32073  hdmap14lem14 32074  hdmap14lem15 32075  hgmapval 32080
[Baer] p. 50Part 15hgmapadd 32087  hgmapmul 32088  hgmaprnlem2N 32090  hgmapvs 32084
[Baer] p. 50Part 16hgmaprnN 32094
[Baer] p. 110Lemma 1hdmapip0com 32110
[Baer] p. 110Line 27hdmapinvlem1 32111
[Baer] p. 110Line 28hdmapinvlem2 32112
[Baer] p. 110Line 30hdmapinvlem3 32113
[Baer] p. 110Part 1.2hdmapglem5 32115  hgmapvv 32119
[Baer] p. 110Proposition 1hdmapinvlem4 32114
[Baer] p. 111Line 10hgmapvvlem1 32116
[Baer] p. 111Line 15hdmapg 32123  hdmapglem7 32122
[BellMachover] p. 36Lemma 10.3id1 20
[BellMachover] p. 97Definition 10.1df-eu 2147
[BellMachover] p. 460Notationdf-mo 2148
[BellMachover] p. 460Definitionmo3 2174
[BellMachover] p. 461Axiom Extax-ext 2264
[BellMachover] p. 462Theorem 1.1bm1.1 2268
[BellMachover] p. 463Axiom Repaxrep5 4136
[BellMachover] p. 463Scheme Sepaxsep 4140
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4144
[BellMachover] p. 466Axiom Powaxpow3 4191
[BellMachover] p. 466Axiom Unionaxun2 4514
[BellMachover] p. 468Definitiondf-ord 4395
[BellMachover] p. 469Theorem 2.2(i)ordirr 4410
[BellMachover] p. 469Theorem 2.2(iii)onelon 4417
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4412
[BellMachover] p. 471Definition of Ndf-om 4657
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4597
[BellMachover] p. 471Definition of Limdf-lim 4397
[BellMachover] p. 472Axiom Infzfinf2 7343
[BellMachover] p. 473Theorem 2.8limom 4671
[BellMachover] p. 477Equation 3.1df-r1 7436
[BellMachover] p. 478Definitionrankval2 7490
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7454  r1ord3g 7451
[BellMachover] p. 480Axiom Regzfreg2 7310
[BellMachover] p. 488Axiom ACac5 8104  dfac4 7749
[BellMachover] p. 490Definition of alephalephval3 7737
[BeltramettiCassinelli] p. 98Remarkatlatmstc 29509
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22933
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22975  chirredi 22974
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22963
[Beran] p. 3Definition of joinsshjval3 21933
[Beran] p. 39Theorem 2.3(i)cmcm2 22195  cmcm2i 22172  cmcm2ii 22177  cmt2N 29440
[Beran] p. 40Theorem 2.3(iii)lecm 22196  lecmi 22181  lecmii 22182
[Beran] p. 45Theorem 3.4cmcmlem 22170
[Beran] p. 49Theorem 4.2cm2j 22199  cm2ji 22204  cm2mi 22205
[Beran] p. 95Definitiondf-sh 21786  issh2 21788
[Beran] p. 95Lemma 3.1(S5)his5 21665
[Beran] p. 95Lemma 3.1(S6)his6 21678
[Beran] p. 95Lemma 3.1(S7)his7 21669
[Beran] p. 95Lemma 3.2(S8)ho01i 22408
[Beran] p. 95Lemma 3.2(S9)hoeq1 22410
[Beran] p. 95Lemma 3.2(S10)ho02i 22409
[Beran] p. 95Lemma 3.2(S11)hoeq2 22411
[Beran] p. 95Postulate (S1)ax-his1 21661  his1i 21679
[Beran] p. 95Postulate (S2)ax-his2 21662
[Beran] p. 95Postulate (S3)ax-his3 21663
[Beran] p. 95Postulate (S4)ax-his4 21664
[Beran] p. 96Definition of normdf-hnorm 21548  dfhnorm2 21701  normval 21703
[Beran] p. 96Definition for Cauchy sequencehcau 21763
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21553
[Beran] p. 96Definition of complete subspaceisch3 21821
[Beran] p. 96Definition of convergedf-hlim 21552  hlimi 21767
[Beran] p. 97Theorem 3.3(i)norm-i-i 21712  norm-i 21708
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21716  norm-ii 21717  normlem0 21688  normlem1 21689  normlem2 21690  normlem3 21691  normlem4 21692  normlem5 21693  normlem6 21694  normlem7 21695  normlem7tALT 21698
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21718  norm-iii 21719
[Beran] p. 98Remark 3.4bcs 21760  bcsiALT 21758  bcsiHIL 21759
[Beran] p. 98Remark 3.4(B)normlem9at 21700  normpar 21734  normpari 21733
[Beran] p. 98Remark 3.4(C)normpyc 21725  normpyth 21724  normpythi 21721
[Beran] p. 99Remarklnfn0 22627  lnfn0i 22622  lnop0 22546  lnop0i 22550
[Beran] p. 99Theorem 3.5(i)nmcexi 22606  nmcfnex 22633  nmcfnexi 22631  nmcopex 22609  nmcopexi 22607
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22634  nmcfnlbi 22632  nmcoplb 22610  nmcoplbi 22608
[Beran] p. 99Theorem 3.5(iii)lnfncon 22636  lnfnconi 22635  lnopcon 22615  lnopconi 22614
[Beran] p. 100Lemma 3.6normpar2i 21735
[Beran] p. 101Lemma 3.6norm3adifi 21732  norm3adifii 21727  norm3dif 21729  norm3difi 21726
[Beran] p. 102Theorem 3.7(i)chocunii 21880  pjhth 21972  pjhtheu 21973  pjpjhth 22004  pjpjhthi 22005  pjth 18803
[Beran] p. 102Theorem 3.7(ii)ococ 21985  ococi 21984
[Beran] p. 103Remark 3.8nlelchi 22641
[Beran] p. 104Theorem 3.9riesz3i 22642  riesz4 22644  riesz4i 22643
[Beran] p. 104Theorem 3.10cnlnadj 22659  cnlnadjeu 22658  cnlnadjeui 22657  cnlnadji 22656  cnlnadjlem1 22647  nmopadjlei 22668
[Beran] p. 106Theorem 3.11(i)adjeq0 22671
[Beran] p. 106Theorem 3.11(v)nmopadji 22670
[Beran] p. 106Theorem 3.11(ii)adjmul 22672
[Beran] p. 106Theorem 3.11(iv)adjadj 22516
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22682  nmopcoadji 22681
[Beran] p. 106Theorem 3.11(iii)adjadd 22673
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22683
[Beran] p. 106Theorem 3.11(viii)adjcoi 22680  pjadj2coi 22784  pjadjcoi 22741
[Beran] p. 107Definitiondf-ch 21801  isch2 21803
[Beran] p. 107Remark 3.12choccl 21885  isch3 21821  occl 21883  ocsh 21862  shoccl 21884  shocsh 21863
[Beran] p. 107Remark 3.12(B)ococin 21987
[Beran] p. 108Theorem 3.13chintcl 21911
[Beran] p. 109Property (i)pjadj2 22767  pjadj3 22768  pjadji 22264  pjadjii 22253
[Beran] p. 109Property (ii)pjidmco 22761  pjidmcoi 22757  pjidmi 22252
[Beran] p. 110Definition of projector orderingpjordi 22753
[Beran] p. 111Remarkho0val 22330  pjch1 22249
[Beran] p. 111Definitiondf-hfmul 22314  df-hfsum 22313  df-hodif 22312  df-homul 22311  df-hosum 22310
[Beran] p. 111Lemma 4.4(i)pjo 22250
[Beran] p. 111Lemma 4.4(ii)pjch 22273  pjchi 22011
[Beran] p. 111Lemma 4.4(iii)pjoc2 22018  pjoc2i 22017
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22259
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22745  pjssmii 22260
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22744
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22743
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22748
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22746  pjssge0ii 22261
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22747  pjdifnormii 22262
[BourbakiEns] p. Proposition 8fcof1 5797  fcofo 5798
[BourbakiFVR] p. Definition 1isder 25707
[BourbakiTop1] p. Remarkxnegmnf 10537  xnegpnf 10536
[BourbakiTop1] p. Remark rexneg 10538
[BourbakiTop1] p. Theoremneiss 16846
[BourbakiTop1] p. Axiom GT'tgpsubcn 17773
[BourbakiTop1] p. Example 1snfil 17559
[BourbakiTop1] p. Example 2neifil 17575
[BourbakiTop1] p. Definitionistgp 17760
[BourbakiTop1] p. Propositioncnpco 16996  ishmeo 17450  neips 16850
[BourbakiTop1] p. Definition 1filintn0 17556
[BourbakiTop1] p. Proposition 9cnpflf2 17695
[BourbakiTop1] p. Theorem 1 (d)iscncl 16998
[BourbakiTop1] p. Proposition Vissnei2 16853
[BourbakiTop1] p. Definition C'''df-cmp 17114
[BourbakiTop1] p. Proposition Viiinnei 16862
[BourbakiTop1] p. Proposition Vivneissex 16864
[BourbakiTop1] p. Proposition Viiielnei 16848  ssnei 16847
[BourbakiTop1] p. Remark below def. 1filn0 17557
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17541
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17558
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27813  stoweid 27812
[BrosowskiDeutsh] p. 89Theorem for the non trivial casestoweidlem62 27811
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27750  stoweidlem10 27759  stoweidlem14 27763  stoweidlem15 27764  stoweidlem35 27784  stoweidlem36 27785  stoweidlem37 27786  stoweidlem38 27787  stoweidlem40 27789  stoweidlem41 27790  stoweidlem43 27792  stoweidlem44 27793  stoweidlem46 27795  stoweidlem5 27754  stoweidlem50 27799  stoweidlem52 27801  stoweidlem53 27802  stoweidlem55 27804  stoweidlem56 27805
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27772  stoweidlem24 27773  stoweidlem27 27776  stoweidlem28 27777  stoweidlem30 27779
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27794  stoweidlem49 27798  stoweidlem7 27756
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27780  stoweidlem39 27788  stoweidlem42 27791  stoweidlem48 27797  stoweidlem51 27800  stoweidlem54 27803  stoweidlem57 27806  stoweidlem58 27807
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27774
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27783
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27766
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27808
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27809
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27767
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27760  stoweidlem26 27775
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27762
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27810
[ChoquetDD] p. 2Definition of mappingdf-mpt 4079
[Clemente] p. 10Definition ITnatded 20790
[Clemente] p. 10Definition I` `m,nnatded 20790
[Clemente] p. 11Definition E=>m,nnatded 20790
[Clemente] p. 11Definition I=>m,nnatded 20790
[Clemente] p. 11Definition E` `(1)natded 20790
[Clemente] p. 11Definition E` `(2)natded 20790
[Clemente] p. 12Definition E` `m,n,pnatded 20790
[Clemente] p. 12Definition I` `n(1)natded 20790
[Clemente] p. 12Definition I` `n(2)natded 20790
[Clemente] p. 13Definition I` `m,n,pnatded 20790
[Clemente] p. 14Definition E` `nnatded 20790
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 20792  ex-natded5.2 20791
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 20795  ex-natded5.3 20794
[Clemente] p. 18Theorem 5.5ex-natded5.5 20797
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 20799  ex-natded5.7 20798
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 20801  ex-natded5.8 20800
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 20803  ex-natded5.13 20802
[Clemente] p. 32Definition I` `nnatded 20790
[Clemente] p. 32Definition E` `m,n,p,anatded 20790
[Clemente] p. 32Definition E` `n,tnatded 20790
[Clemente] p. 32Definition I` `n,tnatded 20790
[Clemente] p. 43Theorem 9.20ex-natded9.20 20804
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 20805
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 20807  ex-natded9.26 20806
[Cohen] p. 301Remarkrelogoprlem 19944
[Cohen] p. 301Property 2relogmul 19945  relogmuld 19976
[Cohen] p. 301Property 3relogdiv 19946  relogdivd 19977
[Cohen] p. 301Property 4relogexp 19949
[Cohen] p. 301Property 1alog1 19939
[Cohen] p. 301Property 1bloge 19940
[Cohn] p. 81Section II.5acsdomd 14284  acsinfd 14283  acsinfdimd 14285  acsmap2d 14282  acsmapd 14281
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10965
[Crawley] p. 1Definition of posetdf-poset 14080
[Crawley] p. 107Theorem 13.2hlsupr 29575
[Crawley] p. 110Theorem 13.3arglem1N 30379  dalaw 30075
[Crawley] p. 111Theorem 13.4hlathil 32154
[Crawley] p. 111Definition of set Wdf-watsN 30179
[Crawley] p. 111Definition of dilationdf-dilN 30295  df-ldil 30293  isldil 30299
[Crawley] p. 111Definition of translationdf-ltrn 30294  df-trnN 30296  isltrn 30308  ltrnu 30310
[Crawley] p. 112Lemma Acdlema1N 29980  cdlema2N 29981  exatleN 29593
[Crawley] p. 112Lemma B1cvrat 29665  cdlemb 29983  cdlemb2 30230  cdlemb3 30795  idltrn 30339  l1cvat 29245  lhpat 30232  lhpat2 30234  lshpat 29246  ltrnel 30328  ltrnmw 30340
[Crawley] p. 112Lemma Ccdlemc1 30380  cdlemc2 30381  ltrnnidn 30363  trlat 30358  trljat1 30355  trljat2 30356  trljat3 30357  trlne 30374  trlnidat 30362  trlnle 30375
[Crawley] p. 112Definition of automorphismdf-pautN 30180
[Crawley] p. 113Lemma Ccdlemc 30386  cdlemc3 30382  cdlemc4 30383
[Crawley] p. 113Lemma Dcdlemd 30396  cdlemd1 30387  cdlemd2 30388  cdlemd3 30389  cdlemd4 30390  cdlemd5 30391  cdlemd6 30392  cdlemd7 30393  cdlemd8 30394  cdlemd9 30395  cdleme31sde 30574  cdleme31se 30571  cdleme31se2 30572  cdleme31snd 30575  cdleme32a 30630  cdleme32b 30631  cdleme32c 30632  cdleme32d 30633  cdleme32e 30634  cdleme32f 30635  cdleme32fva 30626  cdleme32fva1 30627  cdleme32fvcl 30629  cdleme32le 30636  cdleme48fv 30688  cdleme4gfv 30696  cdleme50eq 30730  cdleme50f 30731  cdleme50f1 30732  cdleme50f1o 30735  cdleme50laut 30736  cdleme50ldil 30737  cdleme50lebi 30729  cdleme50rn 30734  cdleme50rnlem 30733  cdlemeg49le 30700  cdlemeg49lebilem 30728
[Crawley] p. 113Lemma Ecdleme 30749  cdleme00a 30398  cdleme01N 30410  cdleme02N 30411  cdleme0a 30400  cdleme0aa 30399  cdleme0b 30401  cdleme0c 30402  cdleme0cp 30403  cdleme0cq 30404  cdleme0dN 30405  cdleme0e 30406  cdleme0ex1N 30412  cdleme0ex2N 30413  cdleme0fN 30407  cdleme0gN 30408  cdleme0moN 30414  cdleme1 30416  cdleme10 30443  cdleme10tN 30447  cdleme11 30459  cdleme11a 30449  cdleme11c 30450  cdleme11dN 30451  cdleme11e 30452  cdleme11fN 30453  cdleme11g 30454  cdleme11h 30455  cdleme11j 30456  cdleme11k 30457  cdleme11l 30458  cdleme12 30460  cdleme13 30461  cdleme14 30462  cdleme15 30467  cdleme15a 30463  cdleme15b 30464  cdleme15c 30465  cdleme15d 30466  cdleme16 30474  cdleme16aN 30448  cdleme16b 30468  cdleme16c 30469  cdleme16d 30470  cdleme16e 30471  cdleme16f 30472  cdleme16g 30473  cdleme19a 30492  cdleme19b 30493  cdleme19c 30494  cdleme19d 30495  cdleme19e 30496  cdleme19f 30497  cdleme1b 30415  cdleme2 30417  cdleme20aN 30498  cdleme20bN 30499  cdleme20c 30500  cdleme20d 30501  cdleme20e 30502  cdleme20f 30503  cdleme20g 30504  cdleme20h 30505  cdleme20i 30506  cdleme20j 30507  cdleme20k 30508  cdleme20l 30511  cdleme20l1 30509  cdleme20l2 30510  cdleme20m 30512  cdleme20y 30491  cdleme20zN 30490  cdleme21 30526  cdleme21d 30519  cdleme21e 30520  cdleme22a 30529  cdleme22aa 30528  cdleme22b 30530  cdleme22cN 30531  cdleme22d 30532  cdleme22e 30533  cdleme22eALTN 30534  cdleme22f 30535  cdleme22f2 30536  cdleme22g 30537  cdleme23a 30538  cdleme23b 30539  cdleme23c 30540  cdleme26e 30548  cdleme26eALTN 30550  cdleme26ee 30549  cdleme26f 30552  cdleme26f2 30554  cdleme26f2ALTN 30553  cdleme26fALTN 30551  cdleme27N 30558  cdleme27a 30556  cdleme27cl 30555  cdleme28c 30561  cdleme3 30426  cdleme30a 30567  cdleme31fv 30579  cdleme31fv1 30580  cdleme31fv1s 30581  cdleme31fv2 30582  cdleme31id 30583  cdleme31sc 30573  cdleme31sdnN 30576  cdleme31sn 30569  cdleme31sn1 30570  cdleme31sn1c 30577  cdleme31sn2 30578  cdleme31so 30568  cdleme35a 30637  cdleme35b 30639  cdleme35c 30640  cdleme35d 30641  cdleme35e 30642  cdleme35f 30643  cdleme35fnpq 30638  cdleme35g 30644  cdleme35h 30645  cdleme35h2 30646  cdleme35sn2aw 30647  cdleme35sn3a 30648  cdleme36a 30649  cdleme36m 30650  cdleme37m 30651  cdleme38m 30652  cdleme38n 30653  cdleme39a 30654  cdleme39n 30655  cdleme3b 30418  cdleme3c 30419  cdleme3d 30420  cdleme3e 30421  cdleme3fN 30422  cdleme3fa 30425  cdleme3g 30423  cdleme3h 30424  cdleme4 30427  cdleme40m 30656  cdleme40n 30657  cdleme40v 30658  cdleme40w 30659  cdleme41fva11 30666  cdleme41sn3aw 30663  cdleme41sn4aw 30664  cdleme41snaw 30665  cdleme42a 30660  cdleme42b 30667  cdleme42c 30661  cdleme42d 30662  cdleme42e 30668  cdleme42f 30669  cdleme42g 30670  cdleme42h 30671  cdleme42i 30672  cdleme42k 30673  cdleme42ke 30674  cdleme42keg 30675  cdleme42mN 30676  cdleme42mgN 30677  cdleme43aN 30678  cdleme43bN 30679  cdleme43cN 30680  cdleme43dN 30681  cdleme5 30429  cdleme50ex 30748  cdleme50ltrn 30746  cdleme51finvN 30745  cdleme51finvfvN 30744  cdleme51finvtrN 30747  cdleme6 30430  cdleme7 30438  cdleme7a 30432  cdleme7aa 30431  cdleme7b 30433  cdleme7c 30434  cdleme7d 30435  cdleme7e 30436  cdleme7ga 30437  cdleme8 30439  cdleme8tN 30444  cdleme9 30442  cdleme9a 30440  cdleme9b 30441  cdleme9tN 30446  cdleme9taN 30445  cdlemeda 30487  cdlemedb 30486  cdlemednpq 30488  cdlemednuN 30489  cdlemefr27cl 30592  cdlemefr32fva1 30599  cdlemefr32fvaN 30598  cdlemefrs32fva 30589  cdlemefrs32fva1 30590  cdlemefs27cl 30602  cdlemefs32fva1 30612  cdlemefs32fvaN 30611  cdlemesner 30485  cdlemeulpq 30409
[Crawley] p. 114Lemma E4atex 30265  4atexlem7 30264  cdleme0nex 30479  cdleme17a 30475  cdleme17c 30477  cdleme17d 30687  cdleme17d1 30478  cdleme17d2 30684  cdleme18a 30480  cdleme18b 30481  cdleme18c 30482  cdleme18d 30484  cdleme4a 30428
[Crawley] p. 115Lemma Ecdleme21a 30514  cdleme21at 30517  cdleme21b 30515  cdleme21c 30516  cdleme21ct 30518  cdleme21f 30521  cdleme21g 30522  cdleme21h 30523  cdleme21i 30524  cdleme22gb 30483
[Crawley] p. 116Lemma Fcdlemf 30752  cdlemf1 30750  cdlemf2 30751
[Crawley] p. 116Lemma Gcdlemftr1 30756  cdlemg16 30846  cdlemg28 30893  cdlemg28a 30882  cdlemg28b 30892  cdlemg3a 30786  cdlemg42 30918  cdlemg43 30919  cdlemg44 30922  cdlemg44a 30920  cdlemg46 30924  cdlemg47 30925  cdlemg9 30823  ltrnco 30908  ltrncom 30927  tgrpabl 30940  trlco 30916
[Crawley] p. 116Definition of Gdf-tgrp 30932
[Crawley] p. 117Lemma Gcdlemg17 30866  cdlemg17b 30851
[Crawley] p. 117Definition of Edf-edring-rN 30945  df-edring 30946
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30949
[Crawley] p. 118Remarktendopltp 30969
[Crawley] p. 118Lemma Hcdlemh 31006  cdlemh1 31004  cdlemh2 31005
[Crawley] p. 118Lemma Icdlemi 31009  cdlemi1 31007  cdlemi2 31008
[Crawley] p. 118Lemma Jcdlemj1 31010  cdlemj2 31011  cdlemj3 31012  tendocan 31013
[Crawley] p. 118Lemma Kcdlemk 31163  cdlemk1 31020  cdlemk10 31032  cdlemk11 31038  cdlemk11t 31135  cdlemk11ta 31118  cdlemk11tb 31120  cdlemk11tc 31134  cdlemk11u-2N 31078  cdlemk11u 31060  cdlemk12 31039  cdlemk12u-2N 31079  cdlemk12u 31061  cdlemk13-2N 31065  cdlemk13 31041  cdlemk14-2N 31067  cdlemk14 31043  cdlemk15-2N 31068  cdlemk15 31044  cdlemk16-2N 31069  cdlemk16 31046  cdlemk16a 31045  cdlemk17-2N 31070  cdlemk17 31047  cdlemk18-2N 31075  cdlemk18-3N 31089  cdlemk18 31057  cdlemk19-2N 31076  cdlemk19 31058  cdlemk19u 31159  cdlemk1u 31048  cdlemk2 31021  cdlemk20-2N 31081  cdlemk20 31063  cdlemk21-2N 31080  cdlemk21N 31062  cdlemk22-3 31090  cdlemk22 31082  cdlemk23-3 31091  cdlemk24-3 31092  cdlemk25-3 31093  cdlemk26-3 31095  cdlemk26b-3 31094  cdlemk27-3 31096  cdlemk28-3 31097  cdlemk29-3 31100  cdlemk3 31022  cdlemk30 31083  cdlemk31 31085  cdlemk32 31086  cdlemk33N 31098  cdlemk34 31099  cdlemk35 31101  cdlemk36 31102  cdlemk37 31103  cdlemk38 31104  cdlemk39 31105  cdlemk39u 31157  cdlemk4 31023  cdlemk41 31109  cdlemk42 31130  cdlemk42yN 31133  cdlemk43N 31152  cdlemk45 31136  cdlemk46 31137  cdlemk47 31138  cdlemk48 31139  cdlemk49 31140  cdlemk5 31025  cdlemk50 31141  cdlemk51 31142  cdlemk52 31143  cdlemk53 31146  cdlemk54 31147  cdlemk55 31150  cdlemk55u 31155  cdlemk56 31160  cdlemk5a 31024  cdlemk5auN 31049  cdlemk5u 31050  cdlemk6 31026  cdlemk6u 31051  cdlemk7 31037  cdlemk7u-2N 31077  cdlemk7u 31059  cdlemk8 31027  cdlemk9 31028  cdlemk9bN 31029  cdlemki 31030  cdlemkid 31125  cdlemkj-2N 31071  cdlemkj 31052  cdlemksat 31035  cdlemksel 31034  cdlemksv 31033  cdlemksv2 31036  cdlemkuat 31055  cdlemkuel-2N 31073  cdlemkuel-3 31087  cdlemkuel 31054  cdlemkuv-2N 31072  cdlemkuv2-2 31074  cdlemkuv2-3N 31088  cdlemkuv2 31056  cdlemkuvN 31053  cdlemkvcl 31031  cdlemky 31115  cdlemkyyN 31151  tendoex 31164
[Crawley] p. 120Remarkdva1dim 31174
[Crawley] p. 120Lemma Lcdleml1N 31165  cdleml2N 31166  cdleml3N 31167  cdleml4N 31168  cdleml5N 31169  cdleml6 31170  cdleml7 31171  cdleml8 31172  cdleml9 31173  dia1dim 31251
[Crawley] p. 120Lemma Mdia11N 31238  diaf11N 31239  dialss 31236  diaord 31237  dibf11N 31351  djajN 31327
[Crawley] p. 120Definition of isomorphism mapdiaval 31222
[Crawley] p. 121Lemma Mcdlemm10N 31308  dia2dimlem1 31254  dia2dimlem2 31255  dia2dimlem3 31256  dia2dimlem4 31257  dia2dimlem5 31258  diaf1oN 31320  diarnN 31319  dvheveccl 31302  dvhopN 31306
[Crawley] p. 121Lemma Ncdlemn 31402  cdlemn10 31396  cdlemn11 31401  cdlemn11a 31397  cdlemn11b 31398  cdlemn11c 31399  cdlemn11pre 31400  cdlemn2 31385  cdlemn2a 31386  cdlemn3 31387  cdlemn4 31388  cdlemn4a 31389  cdlemn5 31391  cdlemn5pre 31390  cdlemn6 31392  cdlemn7 31393  cdlemn8 31394  cdlemn9 31395  diclspsn 31384
[Crawley] p. 121Definition of phi(q)df-dic 31363
[Crawley] p. 122Lemma Ndih11 31455  dihf11 31457  dihjust 31407  dihjustlem 31406  dihord 31454  dihord1 31408  dihord10 31413  dihord11b 31412  dihord11c 31414  dihord2 31417  dihord2a 31409  dihord2b 31410  dihord2cN 31411  dihord2pre 31415  dihord2pre2 31416  dihordlem6 31403  dihordlem7 31404  dihordlem7b 31405
[Crawley] p. 122Definition of isomorphism mapdihffval 31420  dihfval 31421  dihval 31422
[Eisenberg] p. 67Definition 5.3df-dif 3155
[Eisenberg] p. 82Definition 6.3dfom3 7348
[Eisenberg] p. 125Definition 8.21df-map 6774
[Eisenberg] p. 216Example 13.2(4)omenps 7355
[Eisenberg] p. 310Theorem 19.8cardprc 7613
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8177
[Enderton] p. 18Axiom of Empty Setaxnul 4148
[Enderton] p. 19Definitiondf-tp 3648
[Enderton] p. 26Exercise 5unissb 3857
[Enderton] p. 26Exercise 10pwel 4225
[Enderton] p. 28Exercise 7(b)pwun 4302
[Enderton] p. 30Theorem "Distributive laws"iinin1 3973  iinin2 3972  iinun2 3968  iunin1 3967  iunin2 3966
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3971  iundif2 3969
[Enderton] p. 32Exercise 20unineq 3419
[Enderton] p. 33Exercise 23iinuni 3985
[Enderton] p. 33Exercise 25iununi 3986
[Enderton] p. 33Exercise 24(a)iinpw 3990
[Enderton] p. 33Exercise 24(b)iunpw 4570  iunpwss 3991
[Enderton] p. 36Definitionopthwiener 4268
[Enderton] p. 38Exercise 6(a)unipw 4224
[Enderton] p. 38Exercise 6(b)pwuni 4206
[Enderton] p. 41Lemma 3Dopeluu 4526  rnex 4942  rnexg 4940
[Enderton] p. 41Exercise 8dmuni 4888  rnuni 5092
[Enderton] p. 42Definition of a functiondffun7 5280  dffun8 5281
[Enderton] p. 43Definition of function valuefunfv2 5587
[Enderton] p. 43Definition of single-rootedfuncnv 5310
[Enderton] p. 44Definition (d)dfima2 5014  dfima3 5015
[Enderton] p. 47Theorem 3Hfvco2 5594
[Enderton] p. 49Axiom of Choice (first form)ac7 8100  ac7g 8101  df-ac 7743  dfac2 7757  dfac2a 7756  dfac3 7748  dfac7 7758
[Enderton] p. 50Theorem 3K(a)imauni 5772
[Enderton] p. 52Definitiondf-map 6774
[Enderton] p. 53Exercise 21coass 5191
[Enderton] p. 53Exercise 27dmco 5181
[Enderton] p. 53Exercise 14(a)funin 5319
[Enderton] p. 53Exercise 22(a)imass2 5049
[Enderton] p. 54Remarkixpf 6838  ixpssmap 6850
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6818
[Enderton] p. 55Axiom of Choice (second form)ac9 8110  ac9s 8120
[Enderton] p. 56Theorem 3Merref 6680
[Enderton] p. 57Lemma 3Nerthi 6706
[Enderton] p. 57Definitiondf-ec 6662
[Enderton] p. 58Definitiondf-qs 6666
[Enderton] p. 60Theorem 3Qth3q 6767  th3qcor 6766  th3qlem1 6764  th3qlem2 6765
[Enderton] p. 61Exercise 35df-ec 6662
[Enderton] p. 65Exercise 56(a)dmun 4885
[Enderton] p. 68Definition of successordf-suc 4398
[Enderton] p. 71Definitiondf-tr 4114  dftr4 4118
[Enderton] p. 72Theorem 4Eunisuc 4468
[Enderton] p. 73Exercise 6unisuc 4468
[Enderton] p. 73Exercise 5(a)truni 4127
[Enderton] p. 73Exercise 5(b)trint 4128  trintALT 28657
[Enderton] p. 79Theorem 4I(A1)nna0 6602
[Enderton] p. 79Theorem 4I(A2)nnasuc 6604  onasuc 6527
[Enderton] p. 79Definition of operation valuedf-ov 5861
[Enderton] p. 80Theorem 4J(A1)nnm0 6603
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6605  onmsuc 6528
[Enderton] p. 81Theorem 4K(1)nnaass 6620
[Enderton] p. 81Theorem 4K(2)nna0r 6607  nnacom 6615
[Enderton] p. 81Theorem 4K(3)nndi 6621
[Enderton] p. 81Theorem 4K(4)nnmass 6622
[Enderton] p. 81Theorem 4K(5)nnmcom 6624
[Enderton] p. 82Exercise 16nnm0r 6608  nnmsucr 6623
[Enderton] p. 88Exercise 23nnaordex 6636
[Enderton] p. 129Definitiondf-en 6864
[Enderton] p. 132Theorem 6B(b)canth 6294
[Enderton] p. 133Exercise 1xpomen 7643
[Enderton] p. 133Exercise 2qnnen 12492
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7045
[Enderton] p. 135Corollary 6Cphp3 7047
[Enderton] p. 136Corollary 6Enneneq 7044
[Enderton] p. 136Corollary 6D(a)pssinf 7073
[Enderton] p. 136Corollary 6D(b)ominf 7075
[Enderton] p. 137Lemma 6Fpssnn 7081
[Enderton] p. 138Corollary 6Gssfi 7083
[Enderton] p. 139Theorem 6H(c)mapen 7025
[Enderton] p. 142Theorem 6I(3)xpcdaen 7809
[Enderton] p. 142Theorem 6I(4)mapcdaen 7810
[Enderton] p. 143Theorem 6Jcda0en 7805  cda1en 7801
[Enderton] p. 144Exercise 13iunfi 7144  unifi 7145  unifi2 7146
[Enderton] p. 144Corollary 6Kundif2 3530  unfi 7124  unfi2 7126
[Enderton] p. 145Figure 38ffoss 5505
[Enderton] p. 145Definitiondf-dom 6865
[Enderton] p. 146Example 1domen 6875  domeng 6876
[Enderton] p. 146Example 3nndomo 7054  nnsdom 7354  nnsdomg 7116
[Enderton] p. 149Theorem 6L(a)cdadom2 7813
[Enderton] p. 149Theorem 6L(c)mapdom1 7026  xpdom1 6961  xpdom1g 6959  xpdom2g 6958
[Enderton] p. 149Theorem 6L(d)mapdom2 7032
[Enderton] p. 151Theorem 6Mzorn 8134  zorng 8131
[Enderton] p. 151Theorem 6M(4)ac8 8119  dfac5 7755
[Enderton] p. 159Theorem 6Qunictb 8197
[Enderton] p. 164Exampleinfdif 7835
[Enderton] p. 168Definitiondf-po 4314
[Enderton] p. 192Theorem 7M(a)oneli 4500
[Enderton] p. 192Theorem 7M(b)ontr1 4438
[Enderton] p. 192Theorem 7M(c)onirri 4499
[Enderton] p. 193Corollary 7N(b)0elon 4445
[Enderton] p. 193Corollary 7N(c)onsuci 4629
[Enderton] p. 193Corollary 7N(d)ssonunii 4579
[Enderton] p. 194Remarkonprc 4576
[Enderton] p. 194Exercise 16suc11 4496
[Enderton] p. 197Definitiondf-card 7572
[Enderton] p. 197Theorem 7Pcarden 8173
[Enderton] p. 200Exercise 25tfis 4645
[Enderton] p. 202Lemma 7Tr1tr 7448
[Enderton] p. 202Definitiondf-r1 7436
[Enderton] p. 202Theorem 7Qr1val1 7458
[Enderton] p. 204Theorem 7V(b)rankval4 7539
[Enderton] p. 206Theorem 7X(b)en2lp 7317
[Enderton] p. 207Exercise 30rankpr 7529  rankprb 7523  rankpw 7515  rankpwi 7495  rankuniss 7538
[Enderton] p. 207Exercise 34opthreg 7319
[Enderton] p. 208Exercise 35suc11reg 7320
[Enderton] p. 212Definition of alephalephval3 7737
[Enderton] p. 213Theorem 8A(a)alephord2 7703
[Enderton] p. 213Theorem 8A(b)cardalephex 7717
[Enderton] p. 218Theorem Schema 8Eonfununi 6358
[Enderton] p. 222Definition of kardkarden 7565  kardex 7564
[Enderton] p. 238Theorem 8Roeoa 6595
[Enderton] p. 238Theorem 8Soeoe 6597
[Enderton] p. 240Exercise 25oarec 6560
[Enderton] p. 257Definition of cofinalitycflm 7876
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13544
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13490
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14280  mrieqv2d 13541  mrieqvd 13540
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13545
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13550  mreexexlem2d 13547
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14286  mreexfidimd 13552
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18894
[Fremlin5] p. 213Lemma 565Cauniioovol 18934
[Fremlin5] p. 214Lemma 565Cauniioombl 18944
[FreydScedrov] p. 283Axiom of Infinityax-inf 7339  inf1 7323  inf2 7324
[Gleason] p. 117Proposition 9-2.1df-enq 8535  enqer 8545
[Gleason] p. 117Proposition 9-2.2df-1nq 8540  df-nq 8536
[Gleason] p. 117Proposition 9-2.3df-plpq 8532  df-plq 8538
[Gleason] p. 119Proposition 9-2.4caovmo 6057  df-mpq 8533  df-mq 8539
[Gleason] p. 119Proposition 9-2.5df-rq 8541
[Gleason] p. 119Proposition 9-2.6ltexnq 8599
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8600  ltbtwnnq 8602
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8595
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8596
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8603
[Gleason] p. 121Definition 9-3.1df-np 8605
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8617
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8619
[Gleason] p. 122Definitiondf-1p 8606
[Gleason] p. 122Remark (1)prub 8618
[Gleason] p. 122Lemma 9-3.4prlem934 8657
[Gleason] p. 122Proposition 9-3.2df-ltp 8609
[Gleason] p. 122Proposition 9-3.3ltsopr 8656  psslinpr 8655  supexpr 8678  suplem1pr 8676  suplem2pr 8677
[Gleason] p. 123Proposition 9-3.5addclpr 8642  addclprlem1 8640  addclprlem2 8641  df-plp 8607
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8646
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8645
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8658
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8667  ltexprlem1 8660  ltexprlem2 8661  ltexprlem3 8662  ltexprlem4 8663  ltexprlem5 8664  ltexprlem6 8665  ltexprlem7 8666
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8669  ltaprlem 8668
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8670
[Gleason] p. 124Lemma 9-3.6prlem936 8671
[Gleason] p. 124Proposition 9-3.7df-mp 8608  mulclpr 8644  mulclprlem 8643  reclem2pr 8672
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8653
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8648
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8647
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8652
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8675  reclem3pr 8673  reclem4pr 8674
[Gleason] p. 126Proposition 9-4.1df-enr 8681  df-mpr 8680  df-plpr 8679  enrer 8690
[Gleason] p. 126Proposition 9-4.2df-0r 8686  df-1r 8687  df-nr 8682
[Gleason] p. 126Proposition 9-4.3df-mr 8684  df-plr 8683  negexsr 8724  recexsr 8729  recexsrlem 8725
[Gleason] p. 127Proposition 9-4.4df-ltr 8685
[Gleason] p. 130Proposition 10-1.3creui 9741  creur 9740  cru 9738
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8810  axcnre 8786
[Gleason] p. 132Definition 10-3.1crim 11600  crimd 11717  crimi 11678  crre 11599  crred 11716  crrei 11677
[Gleason] p. 132Definition 10-3.2remim 11602  remimd 11683
[Gleason] p. 133Definition 10.36absval2 11769  absval2d 11927  absval2i 11880
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11626  cjaddd 11705  cjaddi 11673
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11627  cjmuld 11706  cjmuli 11674
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11625  cjcjd 11684  cjcji 11656
[Gleason] p. 133Proposition 10-3.4(f)cjre 11624  cjreb 11608  cjrebd 11687  cjrebi 11659  cjred 11711  rere 11607  rereb 11605  rerebd 11686  rerebi 11658  rered 11709
[Gleason] p. 133Proposition 10-3.4(h)addcj 11633  addcjd 11697  addcji 11668
[Gleason] p. 133Proposition 10-3.7(a)absval 11723
[Gleason] p. 133Proposition 10-3.7(b)abscj 11764  abscjd 11932  abscji 11884
[Gleason] p. 133Proposition 10-3.7(c)abs00 11774  abs00d 11928  abs00i 11881  absne0d 11929
[Gleason] p. 133Proposition 10-3.7(d)releabs 11805  releabsd 11933  releabsi 11885
[Gleason] p. 133Proposition 10-3.7(f)absmul 11779  absmuld 11936  absmuli 11887
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11767  sqabsaddi 11888
[Gleason] p. 133Proposition 10-3.7(h)abstri 11814  abstrid 11938  abstrii 11891
[Gleason] p. 134Definition 10-4.1df-exp 11105  exp0 11108  expp1 11110  expp1d 11246
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20026  cxpaddd 20064  expadd 11144  expaddd 11247  expaddz 11146
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20035  cxpmuld 20081  expmul 11147  expmuld 11248  expmulz 11148
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20032  mulcxpd 20075  mulexp 11141  mulexpd 11260  mulexpz 11142
[Gleason] p. 140Exercise 1znnen 12491
[Gleason] p. 141Definition 11-2.1fzval 10784
[Gleason] p. 168Proposition 12-2.1(a)climadd 12105  rlimadd 12116  rlimdiv 12119
[Gleason] p. 168Proposition 12-2.1(b)climsub 12107  rlimsub 12117
[Gleason] p. 168Proposition 12-2.1(c)climmul 12106  rlimmul 12118
[Gleason] p. 171Corollary 12-2.2climmulc2 12110
[Gleason] p. 172Corollary 12-2.5climrecl 12057
[Gleason] p. 172Proposition 12-2.4(c)climabs 12077  climcj 12078  climim 12080  climre 12079  rlimabs 12082  rlimcj 12083  rlimim 12085  rlimre 12084
[Gleason] p. 173Definition 12-3.1df-ltxr 8872  df-xr 8871  ltxr 10457
[Gleason] p. 175Definition 12-4.1df-limsup 11945  limsupval 11948
[Gleason] p. 180Theorem 12-5.1climsup 12143
[Gleason] p. 180Theorem 12-5.3caucvg 12151  caucvgb 12152  caucvgr 12148  climcau 12144
[Gleason] p. 182Exercise 3cvgcmp 12274
[Gleason] p. 182Exercise 4cvgrat 12339
[Gleason] p. 195Theorem 13-2.12abs1m 11819
[Gleason] p. 217Lemma 13-4.1btwnzge0 10953
[Gleason] p. 223Definition 14-1.1df-met 16374
[Gleason] p. 223Definition 14-1.1(a)met0 17908  xmet0 17907
[Gleason] p. 223Definition 14-1.1(b)metgt0 17923
[Gleason] p. 223Definition 14-1.1(c)metsym 17914
[Gleason] p. 223Definition 14-1.1(d)mettri 17916  mstri 18015  xmettri 17915  xmstri 18014
[Gleason] p. 225Definition 14-1.5xpsmet 17946
[Gleason] p. 230Proposition 14-2.6txlm 17342
[Gleason] p. 240Theorem 14-4.3metcnp4 18735
[Gleason] p. 240Proposition 14-4.2metcnp3 18086
[Gleason] p. 243Proposition 14-4.16addcn 18369  addcn2 12067  mulcn 18371  mulcn2 12069  subcn 18370  subcn2 12068
[Gleason] p. 295Remarkbcval3 11319  bcval4 11320
[Gleason] p. 295Equation 2bcpasc 11333
[Gleason] p. 295Definition of binomial coefficientbcval 11317  df-bc 11316
[Gleason] p. 296Remarkbcn0 11323  bcnn 11324
[Gleason] p. 296Theorem 15-2.8binom 12288
[Gleason] p. 308Equation 2ef0 12372
[Gleason] p. 308Equation 3efcj 12373
[Gleason] p. 309Corollary 15-4.3efne0 12377
[Gleason] p. 309Corollary 15-4.4efexp 12381
[Gleason] p. 310Equation 14sinadd 12444
[Gleason] p. 310Equation 15cosadd 12445
[Gleason] p. 311Equation 17sincossq 12456
[Gleason] p. 311Equation 18cosbnd 12461  sinbnd 12460
[Gleason] p. 311Lemma 15-4.7sqeqor 11217  sqeqori 11215
[Gleason] p. 311Definition of pidf-pi 12354
[Godowski] p. 730Equation SFgoeqi 22853
[GodowskiGreechie] p. 249Equation IV3oai 22247
[Gratzer] p. 23Section 0.6df-mre 13488
[Gratzer] p. 27Section 0.6df-mri 13490
[Halmos] p. 31Theorem 17.3riesz1 22645  riesz2 22646
[Halmos] p. 41Definition of Hermitianhmopadj2 22521
[Halmos] p. 42Definition of projector orderingpjordi 22753
[Halmos] p. 43Theorem 26.1elpjhmop 22765  elpjidm 22764  pjnmopi 22728
[Halmos] p. 44Remarkpjinormi 22266  pjinormii 22255
[Halmos] p. 44Theorem 26.2elpjch 22769  pjrn 22286  pjrni 22281  pjvec 22275
[Halmos] p. 44Theorem 26.3pjnorm2 22306
[Halmos] p. 44Theorem 26.4hmopidmpj 22734  hmopidmpji 22732
[Halmos] p. 45Theorem 27.1pjinvari 22771
[Halmos] p. 45Theorem 27.3pjoci 22760  pjocvec 22276
[Halmos] p. 45Theorem 27.4pjorthcoi 22749
[Halmos] p. 48Theorem 29.2pjssposi 22752
[Halmos] p. 48Theorem 29.3pjssdif1i 22755  pjssdif2i 22754
[Halmos] p. 50Definition of spectrumdf-spec 22435
[Hamilton] p. 28Definition 2.1ax-1 5
[Hamilton] p. 31Example 2.7(a)id1 20
[Hamilton] p. 73Rule 1ax-mp 8
[Hamilton] p. 74Rule 2ax-gen 1533
[Hatcher] p. 25Definitiondf-phtpc 18490  df-phtpy 18469
[Hatcher] p. 26Definitiondf-pco 18503  df-pi1 18506
[Hatcher] p. 26Proposition 1.2phtpcer 18493
[Hatcher] p. 26Proposition 1.3pi1grp 18548
[Herstein] p. 54Exercise 28df-grpo 20858
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14498  grpoideu 20876  mndideu 14375
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14516  grpoinveu 20889
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14535  grpo2inv 20906
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14544  grpoinvop 20908
[Herstein] p. 57Exercise 1isgrp2d 20902  isgrp2i 20903
[Hitchcock] p. 5Rule A3mpto1 1523
[Hitchcock] p. 5Rule A4mpto2 1524
[Hitchcock] p. 5Rule A5mtp-xor 1525
[Holland] p. 1519Theorem 2sumdmdi 23000
[Holland] p. 1520Lemma 5cdj1i 23013  cdj3i 23021  cdj3lem1 23014  cdjreui 23012
[Holland] p. 1524Lemma 7mddmdin0i 23011
[Holland95] p. 13Theorem 3.6hlathil 32154
[Holland95] p. 14Line 15hgmapvs 32084
[Holland95] p. 14Line 16hdmaplkr 32106
[Holland95] p. 14Line 17hdmapellkr 32107
[Holland95] p. 14Line 19hdmapglnm2 32104
[Holland95] p. 14Line 20hdmapip0com 32110
[Holland95] p. 14Theorem 3.6hdmapevec2 32029
[Holland95] p. 14Lines 24 and 25hdmapoc 32124
[Holland95] p. 204Definition of involutiondf-srng 15611
[Holland95] p. 212Definition of subspacedf-psubsp 29692
[Holland95] p. 214Lemma 3.3lclkrlem2v 31718
[Holland95] p. 214Definition 3.2df-lpolN 31671
[Holland95] p. 214Definition of nonsingularpnonsingN 30122
[Holland95] p. 215Lemma 3.3(1)dihoml4 31567  poml4N 30142
[Holland95] p. 215Lemma 3.3(2)dochexmid 31658  pexmidALTN 30167  pexmidN 30158
[Holland95] p. 218Theorem 3.6lclkr 31723
[Holland95] p. 218Definition of dual vector spacedf-ldual 29314  ldualset 29315
[Holland95] p. 222Item 1df-lines 29690  df-pointsN 29691
[Holland95] p. 222Item 2df-polarityN 30092
[Holland95] p. 223Remarkispsubcl2N 30136  omllaw4 29436  pol1N 30099  polcon3N 30106
[Holland95] p. 223Definitiondf-psubclN 30124
[Holland95] p. 223Equation for polaritypolval2N 30095
[Hughes] p. 44Equation 1.21bax-his3 21663
[Hughes] p. 47Definition of projection operatordfpjop 22762
[Hughes] p. 49Equation 1.30eighmre 22543  eigre 22415  eigrei 22414
[Hughes] p. 49Equation 1.31eighmorth 22544  eigorth 22418  eigorthi 22417
[Hughes] p. 137Remark (ii)eigposi 22416
[Indrzejczak] p. 33Definition ` `Enatded 20790  natded 20790
[Indrzejczak] p. 33Definition ` `Inatded 20790
[Indrzejczak] p. 34Definition ` `Enatded 20790  natded 20790
[Indrzejczak] p. 34Definition ` `Inatded 20790
[Jech] p. 4Definition of classcv 1622  cvjust 2278
[Jech] p. 42Lemma 6.1alephexp1 8201
[Jech] p. 42Equation 6.1alephadd 8199  alephmul 8200
[Jech] p. 43Lemma 6.2infmap 8198  infmap2 7844
[Jech] p. 71Lemma 9.3jech9.3 7486
[Jech] p. 72Equation 9.3scott0 7556  scottex 7555
[Jech] p. 72Exercise 9.1rankval4 7539
[Jech] p. 72Scheme "Collection Principle"cp 7561
[Jech] p. 78Definition implied by the footnoteopthprc 4736
[JonesMatijasevic] p. 694Definition 2.3rmxyval 27000
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 27096
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 27097
[JonesMatijasevic] p. 695Equation 2.7rmxadd 27012
[JonesMatijasevic] p. 695Equation 2.8rmyadd 27016
[JonesMatijasevic] p. 695Equation 2.9rmxp1 27017  rmyp1 27018
[JonesMatijasevic] p. 695Equation 2.10rmxm1 27019  rmym1 27020
[JonesMatijasevic] p. 695Equation 2.11rmx0 27010  rmx1 27011  rmxluc 27021
[JonesMatijasevic] p. 695Equation 2.12rmy0 27014  rmy1 27015  rmyluc 27022
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 27024
[JonesMatijasevic] p. 695Equation 2.14rmydbl 27025
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 27047  jm2.17b 27048  jm2.17c 27049
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 27086
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 27090
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 27081
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 27050  jm2.24nn 27046
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 27095
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 27101  rmygeid 27051
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 27113
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1635
[KalishMontague] p. 85Lemma 2equid 1644
[KalishMontague] p. 85Lemma 3equcomi 1646
[KalishMontague] p. 86Lemma 7cbvalivw 1642  cbvaliw 1641
[KalishMontague] p. 87Lemma 8spimvw 1639  spimw 1638
[KalishMontague] p. 87Lemma 9spfw 1657  spw 1660
[Kalmbach] p. 14Definition of latticechabs1 22095  chabs1i 22097  chabs2 22096  chabs2i 22098  chjass 22112  chjassi 22065  latabs1 14193  latabs2 14194
[Kalmbach] p. 15Definition of atomdf-at 22918  ela 22919
[Kalmbach] p. 15Definition of coverscvbr2 22863  cvrval2 29464
[Kalmbach] p. 16Definitiondf-ol 29368  df-oml 29369
[Kalmbach] p. 20Definition of commutescmbr 22163  cmbri 22169  cmtvalN 29401  df-cm 22162  df-cmtN 29367
[Kalmbach] p. 22Remarkomllaw5N 29437  pjoml5 22192  pjoml5i 22167
[Kalmbach] p. 22Definitionpjoml2 22190  pjoml2i 22164
[Kalmbach] p. 22Theorem 2(v)cmcm 22193  cmcmi 22171  cmcmii 22176  cmtcomN 29439
[Kalmbach] p. 22Theorem 2(ii)omllaw3 29435  omlsi 21983  pjoml 22015  pjomli 22014
[Kalmbach] p. 22Definition of OML lawomllaw2N 29434
[Kalmbach] p. 23Remarkcmbr2i 22175  cmcm3 22194  cmcm3i 22173  cmcm3ii 22178  cmcm4i 22174  cmt3N 29441  cmt4N 29442  cmtbr2N 29443
[Kalmbach] p. 23Lemma 3cmbr3 22187  cmbr3i 22179  cmtbr3N 29444
[Kalmbach] p. 25Theorem 5fh1 22197  fh1i 22200  fh2 22198  fh2i 22201  omlfh1N 29448
[Kalmbach] p. 65Remarkchjatom 22937  chslej 22077  chsleji 22037  shslej 21959  shsleji 21949
[Kalmbach] p. 65Proposition 1chocin 22074  chocini 22033  chsupcl 21919  chsupval2 21989  h0elch 21834  helch 21823  hsupval2 21988  ocin 21875  ococss 21872  shococss 21873
[Kalmbach] p. 65Definition of subspace sumshsval 21891
[Kalmbach] p. 66Remarkdf-pjh 21974  pjssmi 22745  pjssmii 22260
[Kalmbach] p. 67Lemma 3osum 22224  osumi 22221
[Kalmbach] p. 67Lemma 4pjci 22780
[Kalmbach] p. 103Exercise 6atmd2 22980
[Kalmbach] p. 103Exercise 12mdsl0 22890
[Kalmbach] p. 140Remarkhatomic 22940  hatomici 22939  hatomistici 22942
[Kalmbach] p. 140Proposition 1atlatmstc 29509
[Kalmbach] p. 140Proposition 1(i)atexch 22961  lsatexch 29233
[Kalmbach] p. 140Proposition 1(ii)chcv1 22935  cvlcvr1 29529  cvr1 29599
[Kalmbach] p. 140Proposition 1(iii)cvexch 22954  cvexchi 22949  cvrexch 29609
[Kalmbach] p. 149Remark 2chrelati 22944  hlrelat 29591  hlrelat5N 29590  lrelat 29204
[Kalmbach] p. 153Exercise 5lsmcv 15894  lsmsatcv 29200  spansncv 22232  spansncvi 22231
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 29219  spansncv2 22873
[Kalmbach] p. 266Definitiondf-st 22791
[Kalmbach2] p. 8Definition of adjointdf-adjh 22429
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8268  fpwwe2 8265
[KanamoriPincus] p. 416Corollary 1.3canth4 8269
[KanamoriPincus] p. 417Corollary 1.6canthp1 8276
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8271
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8273
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8286
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8290  gchxpidm 8291
[KanamoriPincus] p. 419Theorem 2.1gchacg 8294  gchhar 8293
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7842  unxpwdom 7303
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8296
[Kreyszig] p. 3Property M1metcl 17897  xmetcl 17896
[Kreyszig] p. 4Property M2meteq0 17904
[Kreyszig] p. 8Definition 1.1-8dscmet 18095
[Kreyszig] p. 12Equation 5conjmul 9477  muleqadd 9412
[Kreyszig] p. 18Definition 1.3-2mopnval 17984
[Kreyszig] p. 19Remarkmopntopon 17985
[Kreyszig] p. 19Theorem T1mopn0 18044  mopnm 17990
[Kreyszig] p. 19Theorem T2unimopn 18042
[Kreyszig] p. 19Definition of neighborhoodneibl 18047
[Kreyszig] p. 20Definition 1.3-3metcnp2 18088
[Kreyszig] p. 25Definition 1.4-1lmbr 16988  lmmbr 18684  lmmbr2 18685
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17108
[Kreyszig] p. 28Theorem 1.4-5lmcau 18738
[Kreyszig] p. 28Definition 1.4-3iscau 18702  iscmet2 18720
[Kreyszig] p. 30Theorem 1.4-7cmetss 18740
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17187  metelcls 18730
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18731  metcld2 18732
[Kreyszig] p. 51Equation 2clmvneg1 18589  lmodvneg1 15667  nvinv 21197  vcm 21127
[Kreyszig] p. 51Equation 1aclm0vs 18588  lmod0vs 15663  vc0 21125
[Kreyszig] p. 51Equation 1blmodvs0 15664  vcz 21126
[Kreyszig] p. 58Definition 2.2-1imsmet 21260
[Kreyszig] p. 59Equation 1imsdval 21255  imsdval2 21256
[Kreyszig] p. 63Problem 1nvnd 21257
[Kreyszig] p. 64Problem 2nvge0 21240  nvz 21235
[Kreyszig] p. 64Problem 3nvabs 21239
[Kreyszig] p. 91Definition 2.7-1isblo3i 21379
[Kreyszig] p. 92Equation 2df-nmoo 21323
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21385  blocni 21383
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21384
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18639  ipeq0 16542  ipz 21295
[Kreyszig] p. 135Problem 2pythi 21428
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21432
[Kreyszig] p. 144Equation 4supcvg 12314
[Kreyszig] p. 144Theorem 3.3-1minvec 18800  minveco 21463
[Kreyszig] p. 196Definition 3.9-1df-aj 21328
[Kreyszig] p. 247Theorem 4.7-2bcth 18751
[Kreyszig] p. 249Theorem 4.7-3ubth 21452
[Kreyszig] p. 470Definition of positive operator orderingleop 22703  leopg 22702
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22721
[Kreyszig] p. 525Theorem 10.1-1htth 21498
[Kunen] p. 10Axiom 0a9e 1891  axnul 4148
[Kunen] p. 11Axiom 3axnul 4148
[Kunen] p. 12Axiom 6zfrep6 5748
[Kunen] p. 24Definition 10.24mapval 6784  mapvalg 6782
[Kunen] p. 30Lemma 10.20fodom 8149
[Kunen] p. 31Definition 10.24mapex 6778
[Kunen] p. 95Definition 2.1df-r1 7436
[Kunen] p. 97Lemma 2.10r1elss 7478  r1elssi 7477
[Kunen] p. 107Exercise 4rankop 7530  rankopb 7524  rankuni 7535  rankxplim 7549  rankxpsuc 7552
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3915
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 27551
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 27546
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 27552
[LeBlanc] p. 277Rule R2axnul 4148
[Levy] p. 338Axiomdf-clab 2270  df-clel 2279  df-cleq 2276
[Levy58] p. 2Definition Iisfin1-3 8012
[Levy58] p. 2Definition IIdf-fin2 7912
[Levy58] p. 2Definition Iadf-fin1a 7911
[Levy58] p. 2Definition IIIdf-fin3 7914
[Levy58] p. 3Definition Vdf-fin5 7915
[Levy58] p. 3Definition IVdf-fin4 7913
[Levy58] p. 4Definition VIdf-fin6 7916
[Levy58] p. 4Definition VIIdf-fin7 7917
[Levy58], p. 3Theorem 1fin1a2 8041
[Lopez-Astorga] p. 12Rule 1mpto1 1523
[Lopez-Astorga] p. 12Rule 2mpto2 1524
[Lopez-Astorga] p. 12Rule 3mtp-xor 1525
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 22988
[Maeda] p. 168Lemma 5mdsym 22992  mdsymi 22991
[Maeda] p. 168Lemma 4(i)mdsymlem4 22986  mdsymlem6 22988  mdsymlem7 22989
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22990
[MaedaMaeda] p. 1Remarkssdmd1 22893  ssdmd2 22894  ssmd1 22891  ssmd2 22892
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22889
[MaedaMaeda] p. 1Definition 1.1df-dmd 22861  df-md 22860  mdbr 22874
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22911  mdslj1i 22899  mdslj2i 22900  mdslle1i 22897  mdslle2i 22898  mdslmd1i 22909  mdslmd2i 22910
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22901  mdsl2bi 22903  mdsl2i 22902
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22915
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22912
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22913
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22890
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22895  mdsl3 22896
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22914
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23009
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 29511  hlrelat1 29589
[MaedaMaeda] p. 31Lemma 7.5lcvexch 29229
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22916  cvmdi 22904  cvnbtwn4 22869  cvrnbtwn4 29469
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22917
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 29530  cvp 22955  cvrp 29605  lcvp 29230
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22979
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22978
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 29523  hlexch4N 29581
[MaedaMaeda] p. 34Exercise 7.1atabsi 22981
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 29632
[MaedaMaeda] p. 61Definition 15.10psubN 29938  atpsubN 29942  df-pointsN 29691  pointpsubN 29940
[MaedaMaeda] p. 62Theorem 15.5df-pmap 29693  pmap11 29951  pmaple 29950  pmapsub 29957  pmapval 29946
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29954  pmap1N 29956
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29959  pmapglb2N 29960  pmapglb2xN 29961  pmapglbx 29958
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 30041
[MaedaMaeda] p. 67Postulate PS1ps-1 29666
[MaedaMaeda] p. 68Lemma 16.2df-padd 29985  paddclN 30031  paddidm 30030
[MaedaMaeda] p. 68Condition PS2ps-2 29667
[MaedaMaeda] p. 68Equation 16.2.1paddass 30027
[MaedaMaeda] p. 69Lemma 16.4ps-1 29666
[MaedaMaeda] p. 69Theorem 16.4ps-2 29667
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14984  lsmmod2 14985  lssats 29202  shatomici 22938  shatomistici 22941  shmodi 21969  shmodsi 21968
[MaedaMaeda] p. 130Remark 29.6dmdmd 22880  mdsymlem7 22989
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22168
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22072
[MaedaMaeda] p. 139Remarksumdmdii 22995
[Margaris] p. 40Rule Cexlimiv 1666
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 7
[Margaris] p. 49Definitiondf-an 360  df-ex 1529  df-or 359  dfbi2 609
[Margaris] p. 51Theorem 1id1 20
[Margaris] p. 56Theorem 3syld 40
[Margaris] p. 59Section 14notnot2ALTVD 28691
[Margaris] p. 60Theorem 8mth8 138
[Margaris] p. 60Section 14con3ALTVD 28692
[Margaris] p. 79Rule Cexinst01 28397  exinst11 28398
[Margaris] p. 89Theorem 19.219.2 1671  19.2g 1780  r19.2z 3543
[Margaris] p. 89Theorem 19.319.3 1781  19.3v 1662  rr19.3v 2909
[Margaris] p. 89Theorem 19.5alcom 1711
[Margaris] p. 89Theorem 19.6alex 1559
[Margaris] p. 89Theorem 19.7alnex 1530
[Margaris] p. 89Theorem 19.819.8a 1718
[Margaris] p. 89Theorem 19.919.9 1783  19.9h 1727  19.9v 1663
[Margaris] p. 89Theorem 19.11excom 1786  excomim 1785
[Margaris] p. 89Theorem 19.1219.12 1734  r19.12 2656
[Margaris] p. 90Theorem 19.14exnal 1561
[Margaris] p. 90Theorem 19.152albi 27576  albi 1551  ralbi 2679
[Margaris] p. 90Theorem 19.1619.16 1787
[Margaris] p. 90Theorem 19.1719.17 1788
[Margaris] p. 90Theorem 19.182exbi 27578  exbi 1568
[Margaris] p. 90Theorem 19.1919.19 1789
[Margaris] p. 90Theorem 19.202alim 27575  alim 1545  alimd 1744  alimdh 1550  alimdv 1607  ralimdaa 2620  ralimdv 2622  ralimdva 2621  sbcimdv 3052
[Margaris] p. 90Theorem 19.2119.21-2 1792  19.21 1791  19.21bi 1794  19.21h 1731  19.21t 1790  19.21v 1831  19.21vv 27574  alrimd 1749  alrimdd 1748  alrimdh 1574  alrimdv 1619  alrimi 1745  alrimih 1552  alrimiv 1617  alrimivv 1618  r19.21 2629  r19.21be 2644  r19.21bi 2641  r19.21t 2628  r19.21v 2630  ralrimd 2631  ralrimdv 2632  ralrimdva 2633  ralrimdvv 2637  ralrimdvva 2638  ralrimi 2624  ralrimiv 2625  ralrimiva 2626  ralrimivv 2634  ralrimivva 2635  ralrimivvva 2636  ralrimivw 2627  rexlimi 2660
[Margaris] p. 90Theorem 19.222alimdv 1609  2exim 27577  2eximdv 1610  exim 1562  eximd 1750  eximdh 1575  eximdv 1608  rexim 2647  reximdai 2651  reximddv 23028  reximdv 2654  reximdv2 2652  reximdva 2655  reximdvai 2653  reximi2 2649
[Margaris] p. 90Theorem 19.2319.23 1797  19.23bi 1802  19.23h 1728  19.23t 1796  19.23v 1832  19.23vv 1833  exlimd 1803  exlimdh 1804  exlimdv 1664  exlimdvv 1668  exlimexi 28287  exlimi 1801  exlimih 1729  exlimiv 1666  exlimivv 1667  r19.23 2658  r19.23v 2659  rexlimd 2664  rexlimdv 2666  rexlimdv3a 2669  rexlimdva 2667  rexlimdvaa 2668  rexlimdvv 2673  rexlimdvva 2674  rexlimdvw 2670  rexlimiv 2661  rexlimiva 2662  rexlimivv 2672
[Margaris] p. 90Theorem 19.2419.24 1673
[Margaris] p. 90Theorem 19.2519.25 1590
[Margaris] p. 90Theorem 19.2619.26-2 1581  19.26-3an 1582  19.26 1580  r19.26-2 2676  r19.26-2a 24934  r19.26-3 2677  r19.26 2675  r19.26m 2678
[Margaris] p. 90Theorem 19.2719.27 1805  19.27v 1835  r19.27av 2681  r19.27z 3552  r19.27zv 3553
[Margaris] p. 90Theorem 19.2819.28 1806  19.28v 1836  19.28vv 27584  r19.28av 2682  r19.28z 3546  r19.28zv 3549  rr19.28v 2910
[Margaris] p. 90Theorem 19.2919.29 1583  19.29r 1584  19.29r2 1585  19.29x 1586  r19.29 2683  r19.29d2r 23181  r19.29r 2684
[Margaris] p. 90Theorem 19.3019.30 1591  r19.30 2685
[Margaris] p. 90Theorem 19.3119.31 1812  19.31vv 27582
[Margaris] p. 90Theorem 19.3219.32 1811  r19.32 27945  r19.32v 2686
[Margaris] p. 90Theorem 19.3319.33-2 27580  19.33 1594  19.33b 1595
[Margaris] p. 90Theorem 19.3419.34 1674
[Margaris] p. 90Theorem 19.3519.35 1587  19.35i 1588  19.35ri 1589  r19.35 2687
[Margaris] p. 90Theorem 19.3619.36 1807  19.36aiv 1838  19.36i 1808  19.36v 1837  19.36vv 27581  r19.36av 2688  r19.36zv 3554
[Margaris] p. 90Theorem 19.3719.37 1809  19.37aiv 1841  19.37v 1840  19.37vv 27583  r19.37 2689  r19.37av 2690  r19.37zv 3550
[Margaris] p. 90Theorem 19.3819.38 1810
[Margaris] p. 90Theorem 19.3919.39 1672
[Margaris] p. 90Theorem 19.4019.40-2 1597  19.40 1596  r19.40 2691
[Margaris] p. 90Theorem 19.4119.41 1815  19.41rg 28316  19.41v 1842  19.41vv 1843  19.41vvv 1844  19.41vvvv 1845  r19.41 2692  r19.41v 2693  r19.41vv 23163
[Margaris] p. 90Theorem 19.4219.42 1816  19.42v 1846  19.42vv 1848  19.42vvv 1849  r19.42v 2694
[Margaris] p. 90Theorem 19.4319.43 1592  r19.43 2695
[Margaris] p. 90Theorem 19.4419.44 1813  r19.44av 2696
[Margaris] p. 90Theorem 19.4519.45 1814  r19.45av 2697  r19.45zv 3551
[Margaris] p. 110Exercise 2(b)eu1 2164
[Mayet] p. 370Remarkjpi 22850  largei 22847  stri 22837
[Mayet3] p. 9Definition of CH-statesdf-hst 22792  ishst 22794
[Mayet3] p. 10Theoremhstrbi 22846  hstri 22845
[Mayet3] p. 1223Theorem 4.1mayete3i 22307
[Mayet3] p. 1240Theorem 7.1mayetes3i 22309
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22858
[MegPav2000] p. 2345Definition 3.4-1chintcl 21911  chsupcl 21919
[MegPav2000] p. 2345Definition 3.4-2hatomic 22940
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22934
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22961
[MegPav2000] p. 2366Figure 7pl42N 30172
[MegPav2002] p. 362Lemma 2.2latj31 14205  latj32 14203  latjass 14201
[Megill] p. 444Axiom C5ax-17 1603  ax17o 2096
[Megill] p. 444Section 7conventions 20789
[Megill] p. 445Lemma L12aecom-o 2090  aecom 1886  ax-10 2079
[Megill] p. 446Lemma L17equtrr 1653
[Megill] p. 446Lemma L18ax9from9o 2087
[Megill] p. 446Lemma L19hbnae-o 2118  hbnae 1895
[Megill] p. 447Remark 9.1df-sb 1630  sbid 1863  sbidd-misc 28189  sbidd 28188
[Megill] p. 448Remark 9.6ax15 1961
[Megill] p. 448Scheme C4'ax-5o 2075
[Megill] p. 448Scheme C5'ax-4 2074  sp 1716
[Megill] p. 448Scheme C6'ax-7 1708
[Megill] p. 448Scheme C7'ax-6o 2076
[Megill] p. 448Scheme C8'ax-8 1643
[Megill] p. 448Scheme C9'ax-12o 2081
[Megill] p. 448Scheme C10'ax-9 1635  ax-9o 2077
[Megill] p. 448Scheme C11'ax-10o 2078
[Megill] p. 448Scheme C12'ax-13 1686
[Megill] p. 448Scheme C13'ax-14 1688
[Megill] p. 448Scheme C14'ax-15 2082
[Megill] p. 448Scheme C15'ax-11o 2080
[Megill] p. 448Scheme C16'ax-16 2083
[Megill] p. 448Theorem 9.4dral1-o 2093  dral1 1905  dral2-o 2120  dral2 1906  drex1 1907  drex2 1908  drsb1 1962  drsb2 2001
[Megill] p. 448Theorem 9.7conventions 20789
[Megill] p. 449Theorem 9.7sbcom2 2053  sbequ 2000  sbid2v 2062
[Megill] p. 450Example in Appendixhba1-o 2088  hba1 1719
[Mendelson] p. 35Axiom A3hirstL-ax3 27860
[Mendelson] p. 36Lemma 1.8id1 20
[Mendelson] p. 69Axiom 4rspsbc 3069  rspsbca 3070  stdpc4 1964
[Mendelson] p. 69Axiom 5ax-5o 2075  ra5 3075  stdpc5 1793
[Mendelson] p. 81Rule Cexlimiv 1666
[Mendelson] p. 95Axiom 6stdpc6 1650
[Mendelson] p. 95Axiom 7stdpc7 1858
[Mendelson] p. 225Axiom system NBGru 2990
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4268
[Mendelson] p. 231Exercise 4.10(k)inv1 3481
[Mendelson] p. 231Exercise 4.10(l)unv 3482
[Mendelson] p. 231Exercise 4.10(n)dfin3 3408
[Mendelson] p. 231Exercise 4.10(o)df-nul 3456
[Mendelson] p. 231Exercise 4.10(q)dfin4 3409
[Mendelson] p. 231Exercise 4.10(s)ddif 3308
[Mendelson] p. 231Definition of uniondfun3 3407
[Mendelson] p. 235Exercise 4.12(c)univ 4565
[Mendelson] p. 235Exercise 4.12(d)pwv 3826
[Mendelson] p. 235Exercise 4.12(j)pwin 4297
[Mendelson] p. 235Exercise 4.12(k)pwunss 4298
[Mendelson] p. 235Exercise 4.12(l)pwssun 4299
[Mendelson] p. 235Exercise 4.12(n)uniin 3847
[Mendelson] p. 235Exercise 4.12(p)reli 4813
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5193
[Mendelson] p. 244Proposition 4.8(g)epweon 4575
[Mendelson] p. 246Definition of successordf-suc 4398
[Mendelson] p. 250Exercise 4.36oelim2 6593
[Mendelson] p. 254Proposition 4.22(b)xpen 7024
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6946  xpsneng 6947
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6953  xpcomeng 6954
[Mendelson] p. 254Proposition 4.22(e)xpassen 6956
[Mendelson] p. 255Definitionbrsdom 6884
[Mendelson] p. 255Exercise 4.39endisj 6949
[Mendelson] p. 255Exercise 4.41mapprc 6776
[Mendelson] p. 255Exercise 4.43mapsnen 6938
[Mendelson] p. 255Exercise 4.45mapunen 7030
[Mendelson] p. 255Exercise 4.47xpmapen 7029
[Mendelson] p. 255Exercise 4.42(a)map0e 6805
[Mendelson] p. 255Exercise 4.42(b)map1 6939
[Mendelson] p. 257Proposition 4.24(a)undom 6950
[Mendelson] p. 258Exercise 4.56(b)cdaen 7799
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7808  cdacomen 7807
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7812
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7806
[Mendelson] p. 258Definition of cardinal sumcdaval 7796  df-cda 7794
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6530
[Mendelson] p. 266Proposition 4.34(f)oaordex 6556
[Mendelson] p. 275Proposition 4.42(d)entri3 8181
[Mendelson] p. 281Definitiondf-r1 7436
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7485
[Mendelson] p. 287Axiom system MKru 2990
[Mittelstaedt] p. 9Definitiondf-oc 21831
[Monk1] p. 22Remarkconventions 20789
[Monk1] p. 22Theorem 3.1conventions 20789
[Monk1] p. 26Theorem 2.8(vii)ssin 3391
[Monk1] p. 33Theorem 3.2(i)ssrel 4776
[Monk1] p. 33Theorem 3.2(ii)eqrel 4777
[Monk1] p. 34Definition 3.3df-opab 4078
[Monk1] p. 36Theorem 3.7(i)coi1 5188  coi2 5189
[Monk1] p. 36Theorem 3.8(v)dm0 4892  rn0 4936
[Monk1] p. 36Theorem 3.7(ii)cnvi 5085
[Monk1] p. 37Theorem 3.13(i)relxp 4794
[Monk1] p. 37Theorem 3.13(x)dmxp 4897  rnxp 5106
[Monk1] p. 37Theorem 3.13(ii)xp0 5098  xp0r 4768
[Monk1] p. 38Theorem 3.16(ii)ima0 5030
[Monk1] p. 38Theorem 3.16(viii)imai 5027
[Monk1] p. 39Theorem 3.17imaexg 5026
[Monk1] p. 39Theorem 3.16(xi)imassrn 5025
[Monk1] p. 41Theorem 4.3(i)fnopfv 5660  funfvop 5637
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5566
[Monk1] p. 42Theorem 4.4(iii)fvelima 5574
[Monk1] p. 43Theorem 4.6funun 5296
[Monk1] p. 43Theorem 4.8(iv)dff13 5783  dff13f 5784
[Monk1] p. 46Theorem 4.15(v)funex 5743  funrnex 5747
[Monk1] p. 50Definition 5.4fniunfv 5773
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5156
[Monk1] p. 52Theorem 5.11(viii)ssint 3878
[Monk1] p. 52Definition 5.13 (i)1stval2 6137  df-1st 6122
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6138  df-2nd 6123
[Monk1] p. 112Theorem 15.17(v)ranksn 7526  ranksnb 7499
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7527
[Monk1] p. 112Theorem 15.17(iii)rankun 7528  rankunb 7522
[Monk1] p. 113Theorem 15.18r1val3 7510
[Monk1] p. 113Definition 15.19df-r1 7436  r1val2 7509
[Monk1] p. 117Lemmazorn2 8133  zorn2g 8130
[Monk1] p. 133Theorem 18.11cardom 7619
[Monk1] p. 133Theorem 18.12canth3 8183
[Monk1] p. 133Theorem 18.14carduni 7614
[Monk2] p. 105Axiom C4ax-5 1544
[Monk2] p. 105Axiom C7ax-8 1643
[Monk2] p. 105Axiom C8ax-11 1715  ax-11o 2080
[Monk2] p. 105Axiom (C8)ax11v 2036
[Monk2] p. 108Lemma 5ax-5o 2075
[Monk2] p. 109Lemma 12ax-7 1708
[Monk2] p. 109Lemma 15equvin 1941  equvini 1927  eqvinop 4251
[Monk2] p. 113Axiom C5-1ax-17 1603  ax17o 2096
[Monk2] p. 113Axiom C5-2ax-6 1703
[Monk2] p. 113Axiom C5-3ax-7 1708
[Monk2] p. 114Lemma 21sp 1716
[Monk2] p. 114Lemma 22ax5o 1717  hba1-o 2088  hba1 1719
[Monk2] p. 114Lemma 23nfia1 1778
[Monk2] p. 114Lemma 24nfa2 1777  nfra2 2597
[Moore] p. 53Part Idf-mre 13488
[Munkres] p. 77Example 2distop 16733  indistop 16739  indistopon 16738
[Munkres] p. 77Example 3fctop 16741  fctop2 16742
[Munkres] p. 77Example 4cctop 16743
[Munkres] p. 78Definition of basisdf-bases 16638  isbasis3g 16687
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13344  tgval2 16694
[Munkres] p. 79Remarktgcl 16707
[Munkres] p. 80Lemma 2.1tgval3 16701
[Munkres] p. 80Lemma 2.2tgss2 16725  tgss3 16724
[Munkres] p. 81Lemma 2.3basgen 16726  basgen2 16727
[Munkres] p. 89Definition of subspace topologyresttop 16891
[Munkres] p. 93Theorem 6.1(1)0cld 16775  topcld 16772
[Munkres] p. 93Theorem 6.1(2)iincld 16776
[Munkres] p. 93Theorem 6.1(3)uncld 16778
[Munkres] p. 94Definition of closureclsval 16774
[Munkres] p. 94Definition of interiorntrval 16773
[Munkres] p. 95Theorem 6.5(a)clsndisj 16812  elcls 16810
[Munkres] p. 95Theorem 6.5(b)elcls3 16820
[Munkres] p. 97Theorem 6.6clslp 16879  neindisj 16854
[Munkres] p. 97Corollary 6.7cldlp 16881
[Munkres] p. 97Definition of limit pointislp2 16877  lpval 16871
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17043
[Munkres] p. 102Definition of continuous functiondf-cn 16957  iscn 16965  iscn2 16968
[Munkres] p. 107Theorem 7.2(g)cncnp 17009  cncnp2 17010  cncnpi 17007  df-cnp 16958  iscnp 16967  iscnp2 16969
[Munkres] p. 127Theorem 10.1metcn 18089
[Munkres] p. 128Theorem 10.3metcn4 18736
[NielsenChuang] p. 195Equation 4.73unierri 22684
[Pfenning] p. 17Definition XMnatded 20790  natded 20790
[Pfenning] p. 17Definition NNCnatded 20790  notnotrd 105
[Pfenning] p. 17Definition ` `Cnatded 20790
[Pfenning] p. 18Rule"natded 20790
[Pfenning] p. 18Definition /\Inatded 20790
[Pfenning] p. 18Definition ` `Enatded 20790  natded 20790  natded 20790  natded 20790  natded 20790
[Pfenning] p. 18Definition ` `Inatded 20790  natded 20790  natded 20790  natded 20790  natded 20790
[Pfenning] p. 18Definition ` `ELnatded 20790
[Pfenning] p. 18Definition ` `ERnatded 20790
[Pfenning] p. 18Definition ` `Ea,unatded 20790
[Pfenning] p. 18Definition ` `IRnatded 20790
[Pfenning] p. 18Definition ` `Ianatded 20790
[Pfenning] p. 127Definition =Enatded 20790
[Pfenning] p. 127Definition =Inatded 20790
[Ponnusamy] p. 361Theorem 6.44cphip0l 18637  df-dip 21274  dip0l 21294  ip0l 16540
[Ponnusamy] p. 361Equation 6.45ipval 21276
[Ponnusamy] p. 362Equation I1dipcj 21290
[Ponnusamy] p. 362Equation I3cphdir 18640  dipdir 21420  ipdir 16543  ipdiri 21408
[Ponnusamy] p. 362Equation I4ipidsq 21286
[Ponnusamy] p. 362Equation 6.46ip0i 21403
[Ponnusamy] p. 362Equation 6.47ip1i 21405
[Ponnusamy] p. 362Equation 6.48ip2i 21406
[Ponnusamy] p. 363Equation I2cphass 18646  dipass 21423  ipass 16549  ipassi 21419
[Prugovecki] p. 186Definition of brabraval 22524  df-bra 22430
[Prugovecki] p. 376Equation 8.1df-kb 22431  kbval 22534
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22962
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 30077
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22976  atcvat4i 22977  cvrat3 29631  cvrat4 29632  lsatcvat3 29242
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22862  cvrval 29459  df-cv 22859  df-lcv 29209  lspsncv0 15899
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 30089
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 30090
[Quine] p. 16Definition 2.1df-clab 2270  rabid 2716
[Quine] p. 17Definition 2.1''dfsb7 2058
[Quine] p. 18Definition 2.7df-cleq 2276
[Quine] p. 19Definition 2.9conventions 20789  df-v 2790
[Quine] p. 34Theorem 5.1abeq2 2388
[Quine] p. 35Theorem 5.2abid2 2400  abid2f 2444
[Quine] p. 40Theorem 6.1sb5 2039
[Quine] p. 40Theorem 6.2sb56 2037  sb6 2038
[Quine] p. 41Theorem 6.3df-clel 2279
[Quine] p. 41Theorem 6.4eqid 2283  eqid1 20840
[Quine] p. 41Theorem 6.5eqcom 2285
[Quine] p. 42Theorem 6.6df-sbc 2992
[Quine] p. 42Theorem 6.7dfsbcq 2993  dfsbcq2 2994
[Quine] p. 43Theorem 6.8vex 2791
[Quine] p. 43Theorem 6.9isset 2792
[Quine] p. 44Theorem 7.3spcgf 2863  spcgv 2868  spcimgf 2861
[Quine] p. 44Theorem 6.11spsbc 3003  spsbcd 3004
[Quine] p. 44Theorem 6.12elex 2796
[Quine] p. 44Theorem 6.13elab 2914  elabg 2915  elabgf 2912
[Quine] p. 44Theorem 6.14noel 3459
[Quine] p. 48Theorem 7.2snprc 3695
[Quine] p. 48Definition 7.1df-pr 3647  df-sn 3646
[Quine] p. 49Theorem 7.4snss 3748  snssg 3754
[Quine] p. 49Theorem 7.5prss 3769  prssg 3770
[Quine] p. 49Theorem 7.6prid1 3734  prid1g 3732  prid2 3735  prid2g 3733  snid 3667  snidg 3665
[Quine] p. 51Theorem 7.13prex 4217  snex 4216  snexALT 4196
[Quine] p. 53Theorem 8.2unisn 3843  unisnALT 28702  unisng 3844
[Quine] p. 53Theorem 8.3uniun 3846
[Quine] p. 54Theorem 8.6elssuni 3855
[Quine] p. 54Theorem 8.7uni0 3854
[Quine] p. 56Theorem 8.17uniabio 5229
[Quine] p. 56Definition 8.18dfiota2 5220
[Quine] p. 57Theorem 8.19iotaval 5230
[Quine] p. 57Theorem 8.22iotanul 5234
[Quine] p. 58Theorem 8.23iotaex 5236
[Quine] p. 58Definition 9.1df-op 3649
[Quine] p. 61Theorem 9.5opabid 4271  opelopab 4286  opelopaba 4281  opelopabaf 4288  opelopabf 4289  opelopabg 4283  opelopabga 4278  oprabid 5882
[Quine] p. 64Definition 9.11df-xp 4695
[Quine] p. 64Definition 9.12df-cnv 4697
[Quine] p. 64Definition 9.15df-id 4309
[Quine] p. 65Theorem 10.3fun0 5307
[Quine] p. 65Theorem 10.4funi 5284
[Quine] p. 65Theorem 10.5funsn 5300  funsng 5298
[Quine] p. 65Definition 10.1df-fun 5257
[Quine] p. 65Definition 10.2args 5041  dffv4 5522
[Quine] p. 68Definition 10.11conventions 20789  df-fv 5263  fv2 5520
[Quine] p. 124Theorem 17.3nn0opth2 11287  nn0opth2i 11286  nn0opthi 11285  omopthi 6655
[Quine] p. 177Definition 25.2df-rdg 6423
[Quine] p. 232Equation icarddom 8176
[Quine] p. 284Axiom 39(vi)funimaex 5330  funimaexg 5329
[Quine] p. 331Axiom system NFru 2990
[ReedSimon] p. 36Definition (iii)ax-his3 21663
[ReedSimon] p. 63Exercise 4(a)df-dip 21274  polid 21738  polid2i 21736  polidi 21737
[ReedSimon] p. 63Exercise 4(b)df-ph 21391
[ReedSimon] p. 195Remarklnophm 22599  lnophmi 22598
[Retherford] p. 49Exercise 1(i)leopadd 22712
[Retherford] p. 49Exercise 1(ii)leopmul 22714  leopmuli 22713
[Retherford] p. 49Exercise 1(iv)leoptr 22717
[Retherford] p. 49Definition VI.1df-leop 22432  leoppos 22706
[Retherford] p. 49Exercise 1(iii)leoptri 22716
[Retherford] p. 49Definition of operator orderingleop3 22705
[Rudin] p. 164Equation 27efcan 12376
[Rudin] p. 164Equation 30efzval 12382
[Rudin] p. 167Equation 48absefi 12476
[Sanford] p. 39Rule 3mtp-xor 1525
[Sanford] p. 39Rule 4mpto2 1524
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 8
[Sanford] p. 39Rule says, "if ` ` is not true, and ` ` implies ` ` , then ` ` must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" mto 167
[Sanford] p. 40Rule 1mpto1 1523
[Schechter] p. 51Definition of antisymmetryintasym 5058
[Schechter] p. 51Definition of irreflexivityintirr 5061
[Schechter] p. 51Definition of symmetrycnvsym 5057
[Schechter] p. 51Definition of transitivitycotr 5055
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13488
[Schechter] p. 79Definition of Moore closuredf-mrc 13489
[Schechter] p. 82Section 4.5df-mrc 13489
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13491
[Schechter] p. 139Definition AC3dfac9 7762
[Schechter] p. 141Definition (MC)dfac11 27160
[Schechter] p. 149Axiom DC1ax-dc 8072  axdc3 8080
[Schechter] p. 187Definition of ring with unitisrng 15345  isrngo 21045
[Schechter] p. 276Remark 11.6.espan0 22121
[Schechter] p. 276Definition of spandf-span 21888  spanval 21912
[Schechter] p. 428Definition 15.35bastop1 16731
[Schwabhauser] p. 10Axiom A1axcgrrflx 24542
[Schwabhauser] p. 10Axiom A2axcgrtr 24543
[Schwabhauser] p. 10Axiom A3axcgrid 24544
[Schwabhauser] p. 11Axiom A4axsegcon 24555
[Schwabhauser] p. 11Axiom A5ax5seg 24566
[Schwabhauser] p. 11Axiom A6axbtwnid 24567
[Schwabhauser] p. 12Axiom A7axpasch 24569
[Schwabhauser] p. 12Axiom A8axlowdim2 24588
[Schwabhauser] p. 13Axiom A10axeuclid 24591
[Schwabhauser] p. 13Axiom A11axcont 24604
[Schwabhauser] p. 27Theorem 2.1cgrrflx 24610
[Schwabhauser] p. 27Theorem 2.2cgrcomim 24612
[Schwabhauser] p. 27Theorem 2.3cgrtr 24615
[Schwabhauser] p. 27Theorem 2.4cgrcoml 24619
[Schwabhauser] p. 27Theorem 2.5cgrcomr 24620
[Schwabhauser] p. 28Theorem 2.8cgrtriv 24625
[Schwabhauser] p. 28Theorem 2.105segofs 24629
[Schwabhauser] p. 28Definition 2.10df-ofs 24606
[Schwabhauser] p. 29Theorem 2.11cgrextend 24631
[Schwabhauser] p. 29Theorem 2.12segconeq 24633
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 24645  btwntriv2 24635
[Schwabhauser] p. 30Theorem 3.2btwncomim 24636
[Schwabhauser] p. 30Theorem 3.3btwntriv1 24639
[Schwabhauser] p. 30Theorem 3.4btwnswapid 24640
[Schwabhauser] p. 30Theorem 3.5btwnexch2 24646  btwnintr 24642
[Schwabhauser] p. 30Theorem 3.6btwnexch 24648  btwnexch3 24643
[Schwabhauser] p. 30Theorem 3.7btwnouttr 24647
[Schwabhauser] p. 32Theorem 3.13axlowdim1 24587
[Schwabhauser] p. 32Theorem 3.14btwndiff 24650
[Schwabhauser] p. 33Theorem 3.17trisegint 24651
[Schwabhauser] p. 34Theorem 4.2ifscgr 24667
[Schwabhauser] p. 34Definition 4.1df-ifs 24662
[Schwabhauser] p. 35Theorem 4.3cgrsub 24668
[Schwabhauser] p. 35Theorem 4.5cgrxfr 24678
[Schwabhauser] p. 35Definition 4.4df-cgr3 24663
[Schwabhauser] p. 36Theorem 4.6btwnxfr 24679
[Schwabhauser] p. 36Theorem 4.11colinearperm1 24685  colinearperm2 24687  colinearperm3 24686  colinearperm4 24688  colinearperm5 24689
[Schwabhauser] p. 36Definition 4.10df-colinear 24664
[Schwabhauser] p. 37Theorem 4.12colineartriv1 24690
[Schwabhauser] p. 37Theorem 4.13colinearxfr 24698
[Schwabhauser] p. 37Theorem 4.14lineext 24699
[Schwabhauser] p. 37Theorem 4.16fscgr 24703
[Schwabhauser] p. 37Theorem 4.17linecgr 24704
[Schwabhauser] p. 37Definition 4.15df-fs 24665
[Schwabhauser] p. 38Theorem 4.18lineid 24706
[Schwabhauser] p. 38Theorem 4.19idinside 24707
[Schwabhauser] p. 39Theorem 5.1btwnconn1 24724
[Schwabhauser] p. 41Theorem 5.2btwnconn2 24725
[Schwabhauser] p. 41Theorem 5.3btwnconn3 24726
[Schwabhauser] p. 41Theorem 5.5brsegle2 24732
[Schwabhauser] p. 41Definition 5.4df-segle 24730
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 24733
[Schwabhauser] p. 42Theorem 5.7seglerflx 24735
[Schwabhauser] p. 42Theorem 5.8segletr 24737
[Schwabhauser] p. 42Theorem 5.9segleantisym 24738
[Schwabhauser] p. 42Theorem 5.10seglelin 24739
[Schwabhauser] p. 42Theorem 5.11seglemin 24736
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 24741
[Schwabhauser] p. 43Theorem 6.2btwnoutside 24748
[Schwabhauser] p. 43Theorem 6.3broutsideof3 24749
[Schwabhauser] p. 43Theorem 6.4broutsideof 24744  df-outsideof 24743
[Schwabhauser] p. 43Definition 6.1broutsideof2 24745
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 24750
[Schwabhauser] p. 44Theorem 6.6outsideofcom 24751
[Schwabhauser] p. 44Theorem 6.7outsideoftr 24752
[Schwabhauser] p. 44Theorem 6.11outsideofeu 24754
[Schwabhauser] p. 44Definition 6.8df-ray 24761
[Schwabhauser] p. 45Part 2df-lines2 24762
[Schwabhauser] p. 45Theorem 6.13outsidele 24755
[Schwabhauser] p. 45Theorem 6.15lineunray 24770
[Schwabhauser] p. 45Theorem 6.16lineelsb2 24771
[Schwabhauser] p. 45Theorem 6.17linecom 24773  linerflx1 24772  linerflx2 24774
[Schwabhauser] p. 45Theorem 6.18linethru 24776
[Schwabhauser] p. 45Definition 6.14df-line2 24760
[Schwabhauser] p. 46Theorem 6.19linethrueu 24779
[Schwabhauser] p. 46Theorem 6.21lineintmo 24780
[Shapiro] p. 230Theorem 6.5.1dchrhash 20510  dchrsum 20508  dchrsum2 20507  sumdchr 20511
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20512  sum2dchr 20513
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15301  ablfacrp2 15302
[Shapiro], p. 328Equation 9.2.4vmasum 20455
[Shapiro], p. 329Equation 9.2.7logfac2 20456
[Shapiro], p. 329Equation 9.2.9logfacrlim 20463
[Shapiro], p. 331Equation 9.2.13vmadivsum 20631
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20634
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20688  vmalogdivsum2 20687
[Shapiro], p. 375Theorem 9.4.1dirith 20678  dirith2 20677
[Shapiro], p. 375Equation 9.4.3rplogsum 20676  rpvmasum 20675  rpvmasum2 20661
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20636
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20674
[Shapiro], p. 377Lemma 9.4.1dchrisum 20641  dchrisumlem1 20638  dchrisumlem2 20639  dchrisumlem3 20640  dchrisumlema 20637
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20644
[Shapiro], p. 379Equation 9.4.16dchrmusum 20673  dchrmusumlem 20671  dchrvmasumlem 20672
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20643
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20645
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20669  dchrisum0re 20662  dchrisumn0 20670
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20655
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20659
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20660
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20715  pntrsumbnd2 20716  pntrsumo1 20714
[Shapiro], p. 405Equation 10.2.1mudivsum 20679
[Shapiro], p. 406Equation 10.2.6mulogsum 20681
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20683
[Shapiro], p. 407Equation 10.2.8mulog2sum 20686
[Shapiro], p. 418Equation 10.4.6logsqvma 20691
[Shapiro], p. 418Equation 10.4.8logsqvma2 20692
[Shapiro], p. 419Equation 10.4.10selberg 20697
[Shapiro], p. 420Equation 10.4.12selberg2lem 20699
[Shapiro], p. 420Equation 10.4.14selberg2 20700
[Shapiro], p. 422Equation 10.6.7selberg3 20708
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20709
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20706  selberg3lem2 20707
[Shapiro], p. 422Equation 10.4.23selberg4 20710
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20704
[Shapiro], p. 428Equation 10.6.2selbergr 20717
[Shapiro], p. 429Equation 10.6.8selberg3r 20718
[Shapiro], p. 430Equation 10.6.11selberg4r 20719
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20733
[Shapiro], p. 434Equation 10.6.27pntlema 20745  pntlemb 20746  pntlemc 20744  pntlemd 20743  pntlemg 20747
[Shapiro], p. 435Equation 10.6.29pntlema 20745
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20737
[Shapiro], p. 436Lemma 10.6.2pntibnd 20742
[Shapiro], p. 436Equation 10.6.34pntlema 20745
[Shapiro], p. 436Equation 10.6.35pntlem3 20758  pntleml 20760
[Stoll] p. 13Definition of symmetric differencesymdif1 3433
[Stoll] p. 16Exercise 4.40dif 3525  dif0 3524
[Stoll] p. 16Exercise 4.8difdifdir 3541
[Stoll] p. 17Theorem 5.1(5)undifv 3528
[Stoll] p. 19Theorem 5.2(13)undm 3426
[Stoll] p. 19Theorem 5.2(13')indm 3427
[Stoll] p. 20Remarkinvdif 3410
[Stoll] p. 25Definition of ordered tripledf-ot 3650
[Stoll] p. 43Definitionuniiun 3955
[Stoll] p. 44Definitionintiin 3956
[Stoll] p. 45Definitiondf-iin 3908
[Stoll] p. 45Definition indexed uniondf-iun 3907
[Stoll] p. 176Theorem 3.4(27)iman 413
[Stoll] p. 262Example 4.1symdif1 3433
[Strang] p. 242Section 6.3expgrowth 27552
[Suppes] p. 22Theorem 2eq0 3469
[Suppes] p. 22Theorem 4eqss 3194  eqssd 3196  eqssi 3195
[Suppes] p. 23Theorem 5ss0 3485  ss0b 3484
[Suppes] p. 23Theorem 6sstr 3187  sstrALT2 28611
[Suppes] p. 23Theorem 7pssirr 3276
[Suppes] p. 23Theorem 8pssn2lp 3277
[Suppes] p. 23Theorem 9psstr 3280
[Suppes] p. 23Theorem 10pssss 3271
[Suppes] p. 25Theorem 12elin 3358  elun 3316
[Suppes] p. 26Theorem 15inidm 3378
[Suppes] p. 26Theorem 16in0 3480
[Suppes] p. 27Theorem 23unidm 3318
[Suppes] p. 27Theorem 24un0 3479
[Suppes] p. 27Theorem 25ssun1 3338
[Suppes] p. 27Theorem 26ssequn1 3345
[Suppes] p. 27Theorem 27unss 3349
[Suppes] p. 27Theorem 28indir 3417
[Suppes] p. 27Theorem 29undir 3418
[Suppes] p. 28Theorem 32difid 3522  difidALT 3523
[Suppes] p. 29Theorem 33difin 3406
[Suppes] p. 29Theorem 34indif 3411
[Suppes] p. 29Theorem 35undif1 3529
[Suppes] p. 29Theorem 36difun2 3533
[Suppes] p. 29Theorem 37difin0 3527
[Suppes] p. 29Theorem 38disjdif 3526
[Suppes] p. 29Theorem 39difundi 3421
[Suppes] p. 29Theorem 40difindi 3423
[Suppes] p. 30Theorem 41nalset 4151
[Suppes] p. 39Theorem 61uniss 3848
[Suppes] p. 39Theorem 65uniop 4269
[Suppes] p. 41Theorem 70intsn 3898
[Suppes] p. 42Theorem 71intpr 3895  intprg 3896
[Suppes] p. 42Theorem 73op1stb 4569
[Suppes] p. 42Theorem 78intun 3894
[Suppes] p. 44Definition 15(a)dfiun2 3937  dfiun2g 3935
[Suppes] p. 44Definition 15(b)dfiin2 3938
[Suppes] p. 47Theorem 86elpw 3631  elpw2 4175  elpw2g 4174  elpwg 3632  elpwgdedVD 28693
[Suppes] p. 47Theorem 87pwid 3638
[Suppes] p. 47Theorem 89pw0 3762
[Suppes] p. 48Theorem 90pwpw0 3763
[Suppes] p. 52Theorem 101xpss12 4792
[Suppes] p. 52Theorem 102xpindi 4819  xpindir 4820
[Suppes] p. 52Theorem 103xpundi 4741  xpundir 4742
[Suppes] p. 54Theorem 105elirrv 7311
[Suppes] p. 58Theorem 2relss 4775
[Suppes] p. 59Theorem 4eldm 4876  eldm2 4877  eldm2g 4875  eldmg 4874
[Suppes] p. 59Definition 3df-dm 4699
[Suppes] p. 60Theorem 6dmin 4886
[Suppes] p. 60Theorem 8rnun 5089
[Suppes] p. 60Theorem 9rnin 5090
[Suppes] p. 60Definition 4dfrn2 4868
[Suppes] p. 61Theorem 11brcnv 4864  brcnvg 4862
[Suppes] p. 62Equation 5elcnv 4858  elcnv2 4859
[Suppes] p. 62Theorem 12relcnv 5051
[Suppes] p. 62Theorem 15cnvin 5088
[Suppes] p. 62Theorem 16cnvun 5086
[Suppes] p. 63Theorem 20co02 5186
[Suppes] p. 63Theorem 21dmcoss 4944
[Suppes] p. 63Definition 7df-co 4698
[Suppes] p. 64Theorem 26cnvco 4865
[Suppes] p. 64Theorem 27coass 5191
[Suppes] p. 65Theorem 31resundi 4969
[Suppes] p. 65Theorem 34elima 5017  elima2 5018  elima3 5019  elimag 5016
[Suppes] p. 65Theorem 35imaundi 5093
[Suppes] p. 66Theorem 40dminss 5095
[Suppes] p. 66Theorem 41imainss 5096
[Suppes] p. 67Exercise 11cnvxp 5097
[Suppes] p. 81Definition 34dfec2 6663
[Suppes] p. 82Theorem 72elec 6699  elecg 6698
[Suppes] p. 82Theorem 73erth 6704  erth2 6705
[Suppes] p. 83Theorem 74erdisj 6707
[Suppes] p. 89Theorem 96map0b 6806
[Suppes] p. 89Theorem 97map0 6808  map0g 6807
[Suppes] p. 89Theorem 98mapsn 6809
[Suppes] p. 89Theorem 99mapss 6810
[Suppes] p. 91Definition 12(ii)alephsuc 7695
[Suppes] p. 91Definition 12(iii)alephlim 7694
[Suppes] p. 92Theorem 1enref 6894  enrefg 6893
[Suppes] p. 92Theorem 2ensym 6910  ensymb 6909  ensymi 6911
[Suppes] p. 92Theorem 3entr 6913
[Suppes] p. 92Theorem 4unen 6943
[Suppes] p. 94Theorem 15endom 6888
[Suppes] p. 94Theorem 16ssdomg 6907
[Suppes] p. 94Theorem 17domtr 6914
[Suppes] p. 95Theorem 18sbth 6981
[Suppes] p. 97Theorem 23canth2 7014  canth2g 7015
[Suppes] p. 97Definition 3brsdom2 6985  df-sdom 6866  dfsdom2 6984
[Suppes] p. 97Theorem 21(i)sdomirr 6998
[Suppes] p. 97Theorem 22(i)domnsym 6987
[Suppes] p. 97Theorem 21(ii)sdomnsym 6986
[Suppes] p. 97Theorem 22(ii)domsdomtr 6996
[Suppes] p. 97Theorem 22(iv)brdom2 6891
[Suppes] p. 97Theorem 21(iii)sdomtr 6999
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6994
[Suppes] p. 98Exercise 4fundmen 6934  fundmeng 6935
[Suppes] p. 98Exercise 6xpdom3 6960
[Suppes] p. 98Exercise 11sdomentr 6995
[Suppes] p. 104Theorem 37fofi 7142
[Suppes] p. 104Theorem 38pwfi 7151
[Suppes] p. 105Theorem 40pwfi 7151
[Suppes] p. 111Axiom for cardinal numberscarden 8173
[Suppes] p. 130Definition 3df-tr 4114
[Suppes] p. 132Theorem 9ssonuni 4578
[Suppes] p. 134Definition 6df-suc 4398
[Suppes] p. 136Theorem Schema 22findes 4686  finds 4682  finds1 4685  finds2 4684
[Suppes] p. 151Theorem 42isfinite 7353  isfinite2 7115  isfiniteg 7117  unbnn 7113
[Suppes] p. 162Definition 5df-ltnq 8542  df-ltpq 8534
[Suppes] p. 197Theorem Schema 4tfindes 4653  tfinds 4650  tfinds2 4654
[Suppes] p. 209Theorem 18oaord1 6549
[Suppes] p. 209Theorem 21oaword2 6551
[Suppes] p. 211Theorem 25oaass 6559
[Suppes] p. 225Definition 8iscard2 7609
[Suppes] p. 227Theorem 56ondomon 8185
[Suppes] p. 228Theorem 59harcard 7611
[Suppes] p. 228Definition 12(i)aleph0 7693
[Suppes] p. 228Theorem Schema 61onintss 4442
[Suppes] p. 228Theorem Schema 62onminesb 4589  onminsb 4590
[Suppes] p. 229Theorem 64alephval2 8194
[Suppes] p. 229Theorem 65alephcard 7697
[Suppes] p. 229Theorem 66alephord2i 7704
[Suppes] p. 229Theorem 67alephnbtwn 7698
[Suppes] p. 229Definition 12df-aleph 7573
[Suppes] p. 242Theorem 6weth 8122
[Suppes] p. 242Theorem 8entric 8179
[Suppes] p. 242Theorem 9carden 8173
[TakeutiZaring] p. 8Axiom 1ax-ext 2264
[TakeutiZaring] p. 13Definition 4.5df-cleq 2276
[TakeutiZaring] p. 13Proposition 4.6df-clel 2279
[TakeutiZaring] p. 13Proposition 4.9cvjust 2278
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2300
[TakeutiZaring] p. 14Definition 4.16df-oprab 5862
[TakeutiZaring] p. 14Proposition 4.14ru 2990
[TakeutiZaring] p. 15Axiom 2zfpair 4212
[TakeutiZaring] p. 15Exercise 1elpr 3658  elpr2 3659  elprg 3657
[TakeutiZaring] p. 15Exercise 2elsn 3655  elsnc 3663  elsnc2 3669  elsnc2g 3668  elsncg 3662
[TakeutiZaring] p. 15Exercise 3elop 4239
[TakeutiZaring] p. 15Exercise 4sneq 3651  sneqr 3780
[TakeutiZaring] p. 15Definition 5.1dfpr2 3656  dfsn2 3654
[TakeutiZaring] p. 16Axiom 3uniex 4516
[TakeutiZaring] p. 16Exercise 6opth 4245
[TakeutiZaring] p. 16Exercise 7opex 4237
[TakeutiZaring] p. 16Exercise 8rext 4222
[TakeutiZaring] p. 16Corollary 5.8unex 4518  unexg 4521
[TakeutiZaring] p. 16Definition 5.3dftp2 3679
[TakeutiZaring] p. 16Definition 5.5df-uni 3828
[TakeutiZaring] p. 16Definition 5.6df-in 3159  df-un 3157
[TakeutiZaring] p. 16Proposition 5.7unipr 3841  uniprg 3842
[TakeutiZaring] p. 17Axiom 4pwex 4193  pwexg 4194
[TakeutiZaring] p. 17Exercise 1eltp 3678
[TakeutiZaring] p. 17Exercise 5elsuc 4461  elsucg 4459  sstr2 3186
[TakeutiZaring] p. 17Exercise 6uncom 3319
[TakeutiZaring] p. 17Exercise 7incom 3361
[TakeutiZaring] p. 17Exercise 8unass 3332
[TakeutiZaring] p. 17Exercise 9inass 3379
[TakeutiZaring] p. 17Exercise 10indi 3415
[TakeutiZaring] p. 17Exercise 11undi 3416
[TakeutiZaring] p. 17Definition 5.9df-pss 3168  dfss2 3169
[TakeutiZaring] p. 17Definition 5.10df-pw 3627
[TakeutiZaring] p. 18Exercise 7unss2 3346
[TakeutiZaring] p. 18Exercise 9df-ss 3166  sseqin2 3388
[TakeutiZaring] p. 18Exercise 10ssid 3197
[TakeutiZaring] p. 18Exercise 12inss1 3389  inss2 3390
[TakeutiZaring] p. 18Exercise 13nss 3236
[TakeutiZaring] p. 18Exercise 15unieq 3836
[TakeutiZaring] p. 18Exercise 18sspwb 4223  sspwimp 28694  sspwimpALT 28701  sspwimpALT2 28705  sspwimpcf 28696
[TakeutiZaring] p. 18Exercise 19pweqb 4230
[TakeutiZaring] p. 19Axiom 5ax-rep 4131
[TakeutiZaring] p. 20Definitiondf-rab 2552
[TakeutiZaring] p. 20Corollary 5.160ex 4150
[TakeutiZaring] p. 20Definition 5.12df-dif 3155
[TakeutiZaring] p. 20Definition 5.14dfnul2 3457
[TakeutiZaring] p. 20Proposition 5.15difid 3522  difidALT 3523
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3464  n0f 3463  neq0 3465
[TakeutiZaring] p. 21Axiom 6zfreg 7309
[TakeutiZaring] p. 21Axiom 6'zfregs 7414
[TakeutiZaring] p. 21Theorem 5.22setind 7419
[TakeutiZaring] p. 21Definition 5.20df-v 2790
[TakeutiZaring] p. 21Proposition 5.21vprc 4152
[TakeutiZaring] p. 22Exercise 10ss 3483
[TakeutiZaring] p. 22Exercise 3ssex 4158  ssexg 4160
[TakeutiZaring] p. 22Exercise 4inex1 4155
[TakeutiZaring] p. 22Exercise 5ruv 7314
[TakeutiZaring] p. 22Exercise 6elirr 7312
[TakeutiZaring] p. 22Exercise 7ssdif0 3513
[TakeutiZaring] p. 22Exercise 11difdif 3302
[TakeutiZaring] p. 22Exercise 13undif3 3429  undif3VD 28658
[TakeutiZaring] p. 22Exercise 14difss 3303
[TakeutiZaring] p. 22Exercise 15sscon 3310
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2548
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2549
[TakeutiZaring] p. 23Proposition 6.2xpex 4801  xpexg 4800  xpexgALT 6070
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4696
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5312
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5445  fun11 5315
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5267  svrelfun 5313
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4867
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4869
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4701
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4702
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4698
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5128  dfrel2 5124
[TakeutiZaring] p. 25Exercise 3xpss 4793
[TakeutiZaring] p. 25Exercise 5relun 4802
[TakeutiZaring] p. 25Exercise 6reluni 4808
[TakeutiZaring] p. 25Exercise 9inxp 4818
[TakeutiZaring] p. 25Exercise 12relres 4983
[TakeutiZaring] p. 25Exercise 13opelres 4960  opelresg 4962
[TakeutiZaring] p. 25Exercise 14dmres 4976
[TakeutiZaring] p. 25Exercise 15resss 4979
[TakeutiZaring] p. 25Exercise 17resabs1 4984
[TakeutiZaring] p. 25Exercise 18funres 5293
[TakeutiZaring] p. 25Exercise 24relco 5171
[TakeutiZaring] p. 25Exercise 29funco 5292
[TakeutiZaring] p. 25Exercise 30f1co 5446
[TakeutiZaring] p. 26Definition 6.10eu2 2168
[TakeutiZaring] p. 26Definition 6.11conventions 20789  df-fv 5263  fv3 5541
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5209  cnvexg 5208
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4941  dmexg 4939
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4942  rnexg 4940
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27658
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27659
[TakeutiZaring] p. 27Corollary 6.13fvex 5539
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5544  tz6.12-afv 28035  tz6.12 5545  tz6.12c 5547
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5516  tz6.12i 5548
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5258
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5259
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5261  wfo 5253
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5260  wf1 5252
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5262  wf1o 5254
[TakeutiZaring] p. 28Exercise 4eqfnfv 5622  eqfnfv2 5623  eqfnfv2f 5626
[TakeutiZaring] p. 28Exercise 5fvco 5595
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5741  fnexALT 5742
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5737  resfunexgALT 5738
[TakeutiZaring] p. 29Exercise 9funimaex 5330  funimaexg 5329
[TakeutiZaring] p. 29Definition 6.18df-br 4024
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4315
[TakeutiZaring] p. 30Definition 6.21dffr2 4358  dffr3 5045  eliniseg 5042  iniseg 5044
[TakeutiZaring] p. 30Definition 6.22df-eprel 4305
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4371  fr3nr 4571  frirr 4370
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4352
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4573
[TakeutiZaring] p. 31Exercise 1frss 4360
[TakeutiZaring] p. 31Exercise 4wess 4380
[TakeutiZaring] p. 31Proposition 6.26tz6.26 24205  tz6.26i 24206  wefrc 4387  wereu2 4390
[TakeutiZaring] p. 32Theorem 6.27wfi 24207  wfii 24208
[TakeutiZaring] p. 32Definition 6.28df-isom 5264
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5826
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5827
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5833
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5834
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5835
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5839
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5846
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5848
[TakeutiZaring] p. 35Notationwtr 4113
[TakeutiZaring] p. 35Theorem 7.2trelpss 27660  tz7.2 4377
[TakeutiZaring] p. 35Definition 7.1dftr3 4117
[TakeutiZaring] p. 36Proposition 7.4ordwe 4405
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4413
[TakeutiZaring] p. 36Proposition 7.6ordelord 4414  ordelordALT 28301  ordelordALTVD 28643
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4420  ordelssne 4419
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4418
[TakeutiZaring] p. 37Proposition 7.9ordin 4422
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4580
[TakeutiZaring] p. 38Corollary 7.15ordsson 4581
[TakeutiZaring] p. 38Definition 7.11df-on 4396
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4424
[TakeutiZaring] p. 38Proposition 7.12onfrALT 28314  ordon 4574
[TakeutiZaring] p. 38Proposition 7.13onprc 4576
[TakeutiZaring] p. 39Theorem 7.17tfi 4644
[TakeutiZaring] p. 40Exercise 3ontr2 4439
[TakeutiZaring] p. 40Exercise 7dftr2 4115
[TakeutiZaring] p. 40Exercise 9onssmin 4588
[TakeutiZaring] p. 40Exercise 11unon 4622
[TakeutiZaring] p. 40Exercise 12ordun 4494
[TakeutiZaring] p. 40Exercise 14ordequn 4493
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4577
[TakeutiZaring] p. 40Proposition 7.20elssuni 3855
[TakeutiZaring] p. 41Definition 7.22df-suc 4398
[TakeutiZaring] p. 41Proposition 7.23sssucid 4469  sucidg 4470
[TakeutiZaring] p. 41Proposition 7.24suceloni 4604
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4484  ordnbtwn 4483
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4619
[TakeutiZaring] p. 42Exercise 1df-lim 4397
[TakeutiZaring] p. 42Exercise 4omssnlim 4670
[TakeutiZaring] p. 42Exercise 7ssnlim 4674
[TakeutiZaring] p. 42Exercise 8onsucssi 4632  ordelsuc 4611
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4613
[TakeutiZaring] p. 42Definition 7.27nlimon 4642
[TakeutiZaring] p. 42Definition 7.28dfom2 4658
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4675
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4676
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4677
[TakeutiZaring] p. 43Remarkomon 4667
[TakeutiZaring] p. 43Axiom 7inf3 7336  omex 7344
[TakeutiZaring] p. 43Theorem 7.32ordom 4665
[TakeutiZaring] p. 43Corollary 7.31find 4681
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4678
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4679
[TakeutiZaring] p. 44Exercise 1limomss 4661
[TakeutiZaring] p. 44Exercise 2int0 3876  trint0 4130
[TakeutiZaring] p. 44Exercise 4intss1 3877
[TakeutiZaring] p. 44Exercise 5intex 4167
[TakeutiZaring] p. 44Exercise 6oninton 4591
[TakeutiZaring] p. 44Exercise 11ordintdif 4441
[TakeutiZaring] p. 44Definition 7.35df-int 3863
[TakeutiZaring] p. 44Proposition 7.34noinfep 7360
[TakeutiZaring] p. 45Exercise 4onint 4586
[TakeutiZaring] p. 47Lemma 1tfrlem1 6391
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6413
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6414
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6415
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6419  tz7.44-2 6420  tz7.44-3 6421
[TakeutiZaring] p. 50Exercise 1smogt 6384
[TakeutiZaring] p. 50Exercise 3smoiso 6379
[TakeutiZaring] p. 50Definition 7.46df-smo 6363
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6457  tz7.49c 6458
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6455
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6454
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6456
[TakeutiZaring] p. 53Proposition 7.532eu5 2227
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7639
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7640
[TakeutiZaring] p. 56Definition 8.1oalim 6531  oasuc 6523
[TakeutiZaring] p. 57Remarktfindsg 4651
[TakeutiZaring] p. 57Proposition 8.2oacl 6534
[TakeutiZaring] p. 57Proposition 8.3oa0 6515  oa0r 6537
[TakeutiZaring] p. 57Proposition 8.16omcl 6535
[TakeutiZaring] p. 58Corollary 8.5oacan 6546
[TakeutiZaring] p. 58Proposition 8.4nnaord 6617  nnaordi 6616  oaord 6545  oaordi 6544
[TakeutiZaring] p. 59Proposition 8.6iunss2 3947  uniss2 3858
[TakeutiZaring] p. 59Proposition 8.7oawordri 6548
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6553  oawordex 6555
[TakeutiZaring] p. 59Proposition 8.9nnacl 6609
[TakeutiZaring] p. 59Proposition 8.10oaabs 6642
[TakeutiZaring] p. 60Remarkoancom 7352
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6558
[TakeutiZaring] p. 62Exercise 1nnarcl 6614
[TakeutiZaring] p. 62Exercise 5oaword1 6550
[TakeutiZaring] p. 62Definition 8.15om0 6516  om0x 6518  omlim 6532  omsuc 6525
[TakeutiZaring] p. 63Proposition 8.17nnecl 6611  nnmcl 6610
[TakeutiZaring] p. 63Proposition 8.19nnmord 6630  nnmordi 6629  omord 6566  omordi 6564
[TakeutiZaring] p. 63Proposition 8.20omcan 6567
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6634  omwordri 6570
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6538
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6540  om1r 6541
[TakeutiZaring] p. 64Proposition 8.22om00 6573
[TakeutiZaring] p. 64Proposition 8.23omordlim 6575
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6576
[TakeutiZaring] p. 64Proposition 8.25odi 6577
[TakeutiZaring] p. 65Theorem 8.26omass 6578
[TakeutiZaring] p. 67Definition 8.30nnesuc 6606  oe0 6521  oelim 6533  oesuc 6526  onesuc 6529
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6519
[TakeutiZaring] p. 67Proposition 8.32oen0 6584
[TakeutiZaring] p. 67Proposition 8.33oeordi 6585
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6520
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6543
[TakeutiZaring] p. 68Corollary 8.34oeord 6586
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6592
[TakeutiZaring] p. 68Proposition 8.35oewordri 6590
[TakeutiZaring] p. 68Proposition 8.37oeworde 6591
[TakeutiZaring] p. 69Proposition 8.41oeoa 6595
[TakeutiZaring] p. 70Proposition 8.42oeoe 6597
[TakeutiZaring] p. 73Theorem 9.1trcl 7410  tz9.1 7411
[TakeutiZaring] p. 76Definition 9.9df-r1 7436  r10 7440  r1lim 7444  r1limg 7443  r1suc 7442  r1sucg 7441
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7452  r1ord2 7453  r1ordg 7450
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7462
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7487  tz9.13 7463  tz9.13g 7464
[TakeutiZaring] p. 79Definition 9.14df-rank 7437  rankval 7488  rankvalb 7469  rankvalg 7489
[TakeutiZaring] p. 79Proposition 9.16rankel 7511  rankelb 7496
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7525  rankval3 7512  rankval3b 7498
[TakeutiZaring] p. 79Proposition 9.18rankonid 7501
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7467
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7506  rankr1c 7493  rankr1g 7504
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7507
[TakeutiZaring] p. 80Exercise 1rankss 7521  rankssb 7520
[TakeutiZaring] p. 80Exercise 2unbndrank 7514
[TakeutiZaring] p. 80Proposition 9.19bndrank 7513
[TakeutiZaring] p. 83Axiom of Choiceac4 8102  dfac3 7748
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7657  numth 8099  numth2 8098
[TakeutiZaring] p. 85Definition 10.4cardval 8168
[TakeutiZaring] p. 85Proposition 10.5cardid 8169  cardid2 7586
[TakeutiZaring] p. 85Proposition 10.9oncard 7593
[TakeutiZaring] p. 85Proposition 10.10carden 8173
[TakeutiZaring] p. 85Proposition 10.11cardidm 7592
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7577
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7598
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7590
[TakeutiZaring] p. 87Proposition 10.15pwen 7034
[TakeutiZaring] p. 88Exercise 1en0 6924
[TakeutiZaring] p. 88Exercise 7infensuc 7039
[TakeutiZaring] p. 89Exercise 10omxpen 6964
[TakeutiZaring] p. 90Corollary 10.23cardnn 7596
[TakeutiZaring] p. 90Definition 10.27alephiso 7725
[TakeutiZaring] p. 90Proposition 10.20nneneq 7044
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7050
[TakeutiZaring] p. 90Proposition 10.26alephprc 7726
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7049
[TakeutiZaring] p. 91Exercise 2alephle 7715
[TakeutiZaring] p. 91Exercise 3aleph0 7693
[TakeutiZaring] p. 91Exercise 4cardlim 7605
[TakeutiZaring] p. 91Exercise 7infpss 7843
[TakeutiZaring] p. 91Exercise 8infcntss 7130
[TakeutiZaring] p. 91Definition 10.29df-fin 6867  isfi 6885
[TakeutiZaring] p. 92Proposition 10.32onfin 7051
[TakeutiZaring] p. 92Proposition 10.34imadomg 8159
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6957
[TakeutiZaring] p. 93Proposition 10.35fodomb 8151
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7815  unxpdom 7070
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7607  cardsdomelir 7606
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7072
[TakeutiZaring] p. 94Proposition 10.39infxpen 7642
[TakeutiZaring] p. 95Definition 10.42df-map 6774
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8184  infxpidm2 7644
[TakeutiZaring] p. 95Proposition 10.41infcda 7834  infxp 7841  infxpg 25095
[TakeutiZaring] p. 96Proposition 10.44pw2en 6969  pw2f1o 6967
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7027
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8114
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8109  ac6s5 8118
[TakeutiZaring] p. 98Theorem 10.47unidom 8165
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8166  uniimadomf 8167
[TakeutiZaring] p. 100Definition 11.1cfcof 7900
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7895
[TakeutiZaring] p. 102Exercise 1cfle 7880
[TakeutiZaring] p. 102Exercise 2cf0 7877
[TakeutiZaring] p. 102Exercise 3cfsuc 7883
[TakeutiZaring] p. 102Exercise 4cfom 7890
[TakeutiZaring] p. 102Proposition 11.9coftr 7899
[TakeutiZaring] p. 103Theorem 11.15alephreg 8204
[TakeutiZaring] p. 103Proposition 11.11cardcf 7878
[TakeutiZaring] p. 103Proposition 11.13alephsing 7902
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7724
[TakeutiZaring] p. 104Proposition 11.16carduniima 7723
[TakeutiZaring] p. 104Proposition 11.18alephfp 7735  alephfp2 7736
[TakeutiZaring] p. 106Theorem 11.20gchina 8321
[TakeutiZaring] p. 106Theorem 11.21mappwen 7739
[TakeutiZaring] p. 107Theorem 11.26konigth 8191
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8205
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8206
[Tarski] p. 67Axiom B5ax-4 2074
[Tarski] p. 67Scheme B5sp 1716
[Tarski] p. 68Lemma 6avril1 20836  equid 1644  equid1 2097  equid1ALT 2115
[Tarski] p. 69Lemma 7equcomi 1646
[Tarski] p. 70Lemma 14spim 1915  spime 1916  spimeh 1722
[Tarski] p. 70Lemma 16ax-11 1715  ax-11o 2080  ax11i 1628
[Tarski] p. 70Lemmas 16 and 17sb6 2038
[Tarski] p. 75Axiom B7ax9v 1636
[Tarski] p. 75Scheme B7ax9vax9 29158
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1603  ax17o 2096
[Tarski], p. 75Scheme B8 of system S2ax-13 1686  ax-14 1688  ax-8 1643
[Truss] p. 114Theorem 5.18ruc 12521
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 499
[WhiteheadRussell] p. 96Axiom *1.3olc 373
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 375
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 508
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 814
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 160
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 108
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 76
[WhiteheadRussell] p. 100Theorem *2.05imim2 49
[WhiteheadRussell] p. 100Theorem *2.06imim1 70
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 406
[WhiteheadRussell] p. 101Theorem *2.06barbara 2240  syl 15
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 385
[WhiteheadRussell] p. 101Theorem *2.08id 19  id1 20
[WhiteheadRussell] p. 101Theorem *2.11exmid 404
[WhiteheadRussell] p. 101Theorem *2.12notnot1 114
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 407
[WhiteheadRussell] p. 102Theorem *2.14notnot2 104  notnot2ALT2 28703
[WhiteheadRussell] p. 102Theorem *2.15con1 120
[WhiteheadRussell] p. 103Theorem *2.16con3 126  con3th 924
[WhiteheadRussell] p. 103Theorem *2.17ax-3 7
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 102
[WhiteheadRussell] p. 104Theorem *2.2orc 374
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 555
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 100
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 101
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 393
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 853
[WhiteheadRussell] p. 104Theorem *2.27conventions 20789  pm2.27 35
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 511
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 512
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 816
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 817
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 815
[WhiteheadRussell] p. 105Definition *2.33df-3or 935
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 558
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 556
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 557
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 47
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 386
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 387
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 144
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 162
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 388
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 389
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 390
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 145
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 147
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 362
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 363
[WhiteheadRussell] p. 107Theorem *2.55orel1 371
[WhiteheadRussell] p. 107Theorem *2.56orel2 372
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 163
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 398
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 763
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 764
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 164
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 391  pm2.67 392
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 146
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 397
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 823
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 399
[WhiteheadRussell] p. 108Theorem *2.69looinv 174
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 818
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 819
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 822
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 821
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 824
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 825
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 71
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 826
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 94
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 484
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 434  pm3.2im 137
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 485
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 486
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 487
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 488
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 435
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 436
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 852
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 570
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 431
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 432
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 443  simplim 143
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 447  simprim 142
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 568
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 569
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 562
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 544
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 542
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 543
[WhiteheadRussell] p. 113Theorem *3.44jao 498  pm3.44 497
[WhiteheadRussell] p. 113Theorem *3.47prth 554
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 832
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 807
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 806
[WhiteheadRussell] p. 116Theorem *4.1con34b 283
[WhiteheadRussell] p. 117Theorem *4.2biid 227
[WhiteheadRussell] p. 117Theorem *4.11notbi 286
[WhiteheadRussell] p. 117Theorem *4.12con2bi 318
[WhiteheadRussell] p. 117Theorem *4.13notnot 282
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 561
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 564
[WhiteheadRussell] p. 117Theorem *4.21bicom 191
[WhiteheadRussell] p. 117Theorem *4.22biantr 897  bitr 689  wl-bitr 24920
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 624
[WhiteheadRussell] p. 117Theorem *4.25oridm 500  pm4.25 501
[WhiteheadRussell] p. 118Theorem *4.3ancom 437
[WhiteheadRussell] p. 118Theorem *4.4andi 837
[WhiteheadRussell] p. 118Theorem *4.31orcom 376
[WhiteheadRussell] p. 118Theorem *4.32anass 630
[WhiteheadRussell] p. 118Theorem *4.33orass 510
[WhiteheadRussell] p. 118Theorem *4.36anbi1 687
[WhiteheadRussell] p. 118Theorem *4.37orbi1 686
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 842
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 841
[WhiteheadRussell] p. 118Definition *4.34df-3an 936
[WhiteheadRussell] p. 119Theorem *4.41ordi 834
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 926
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 893
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 560
[WhiteheadRussell] p. 119Theorem *4.45orabs 828  pm4.45 669  pm4.45im 545
[WhiteheadRussell] p. 120Theorem *4.5anor 475
[WhiteheadRussell] p. 120Theorem *4.6imor 401
[WhiteheadRussell] p. 120Theorem *4.7anclb 530
[WhiteheadRussell] p. 120Theorem *4.51ianor 474
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 477
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 478
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 479
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 480
[WhiteheadRussell] p. 120Theorem *4.56ioran 476  pm4.56 481
[WhiteheadRussell] p. 120Theorem *4.57oran 482  pm4.57 483
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 415
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 408
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 410
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 361
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 416
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 409
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 417
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 611  pm4.71d 615  pm4.71i 613  pm4.71r 612  pm4.71rd 616  pm4.71ri 614
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 846
[WhiteheadRussell] p. 121Theorem *4.73iba 489
[WhiteheadRussell] p. 121Theorem *4.74biorf 394
[WhiteheadRussell] p. 121Theorem *4.76jcab 833  pm4.76 836
[WhiteheadRussell] p. 121Theorem *4.77jaob 758  pm4.77 762
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 565
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 566
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 354
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 355
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 894
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 895
[WhiteheadRussell] p. 122Theorem *4.84imbi1 313
[WhiteheadRussell] p. 122Theorem *4.85imbi2 314
[WhiteheadRussell] p. 122Theorem *4.86bibi1 317  wl-bibi1 24913
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 350  impexp 433  pm4.87 567
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 830
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 854
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 855
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 857
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 856
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 859
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 860
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 858
[WhiteheadRussell] p. 124Theorem *5.18nbbn 347  pm5.18 345
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 349
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 831
[WhiteheadRussell] p. 124Theorem *5.22xor 861
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 863
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 864
[WhiteheadRussell] p. 124Theorem *5.25dfor2 400
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 692
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 351
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 326
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 878
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 900
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 571
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 617
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 848
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 869
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 849
[WhiteheadRussell] p. 125Theorem *5.41imdi 352  pm5.41 353
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 531
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 877
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 771
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 870
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 867
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 693
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 889
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 890
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 902
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 330
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 235
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 903
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 27553
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 27554
[WhiteheadRussell] p. 147Theorem *10.2219.26 1580
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 27555
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 27556
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 27557
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1602
[WhiteheadRussell] p. 151Theorem *10.301albitr 27558
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 27559
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 27560
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 27561
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 27562
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 27564
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 27565
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 27566
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 27563
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 27569
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2054
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 27570
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 27571
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1712
[WhiteheadRussell] p. 160Theorem *11.222exnaln 27572
[WhiteheadRussell] p. 160Theorem *11.252nexaln 27573
[WhiteheadRussell] p. 161Theorem *11.319.21vv 27574
[WhiteheadRussell] p. 162Theorem *11.322alim 27575
[WhiteheadRussell] p. 162Theorem *11.332albi 27576
[WhiteheadRussell] p. 162Theorem *11.342exim 27577
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 27579
[WhiteheadRussell] p. 162Theorem *11.3412exbi 27578
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1597
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 27581
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 27582
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 27580
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1560
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 27583
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 27584
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1567
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 27585
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1834  pm11.53g 24964
[WhiteheadRussell] p. 164Theorem *11.5212exanali 27586
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 27591
[WhiteheadRussell] p. 165Theorem *11.56aaanv 27587
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 27588
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 27589
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 27590
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 27595
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 27592
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 27593
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 27594
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 27596
[WhiteheadRussell] p. 175Definition *14.02df-eu 2147
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27607  pm13.13b 27608
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27609
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2518
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2519
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2908
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27615
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27616
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27610
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 28318  pm13.193 27611
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27612
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27613
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27614
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27621
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27620
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27619
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3043
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27622  pm14.122b 27623  pm14.122c 27624
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27625  pm14.123b 27626  pm14.123c 27627
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27629
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27628
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27630
[WhiteheadRussell] p. 190Theorem *14.22iota4 5237
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27631
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5238
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27632
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27634
[WhiteheadRussell] p. 192Theorem *14.26eupick 2206  eupickbi 2209  sbaniota 27635
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27633
[WhiteheadRussell] p. 192Theorem *14.271eubi 27636
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27637
[WhiteheadRussell] p. 235Definition *30.01conventions 20789  df-fv 5263
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7633  pm54.43lem 7632
[Young] p. 141Definition of operator orderingleop2 22704
[Young] p. 142Example 12.2(i)0leop 22710  idleop 22711
[vandenDries] p. 42Lemma 61irrapx1 26913
[vandenDries] p. 43Theorem 62pellex 26920  pellexlem1 26914

This page was last updated on 16-Oct-2017.
Copyright terms: Public domain