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 13652
[Adamek] p. 29Proposition 3.14(1)invinv 13666
[Adamek] p. 29Proposition 3.14(2)invco 13667  isoco 13669
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25589
[AitkenIBCG] p. 3Definition 2df-angtrg 25585  df-trcng 25588
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25461  df-ig2 25460
[AitkenIBG] p. 2Definition 4df-li 25476
[AitkenIBG] p. 3Definition 5df-col 25490
[AitkenIBG] p. 3Definition 6df-con2 25495
[AitkenIBG] p. 3Proposition 4isconcl5a 25500  isconcl5ab 25501  isconcl6a 25502  isconcl6ab 25503
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25508
[AitkenIBG] p. 4Exercise 5tpne 25474
[AitkenIBG] p. 4Definition 8df-seg2 25530
[AitkenIBG] p. 4Definition 10df-sside 25562
[AitkenIBG] p. 4Definition 11df-ray2 25551
[AitkenIBG] p. 10Definition 17df-angle 25557
[AitkenIBG] p. 15Definition 23df-triangle 25559
[AitkenIBG] p. 15Definition 24df-cnvx 25578
[AitkenNG] p. 2Definition 1df-slices 25592
[AitkenNG] p. 2Definition 2df-Cut 25594
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25596
[AitkenNG] p. 4Definition 5df-crcl 25598
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18211  df-nmoo 21315
[AkhiezerGlazman] p. 64Theoremhmopidmch 22725  hmopidmchi 22723
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22773  pjcmul2i 22774
[AkhiezerGlazman] p. 72Theoremcnvunop 22490  unoplin 22492
[AkhiezerGlazman] p. 72Equation 2unopadj 22491  unopadj2 22510
[AkhiezerGlazman] p. 73Theoremelunop2 22585  lnopunii 22584
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22658
[Apostol] p. 18Theorem I.1addcan 8991  addcan2d 9011  addcan2i 9001  addcand 9010  addcani 9000
[Apostol] p. 18Theorem I.2negeu 9037
[Apostol] p. 18Theorem I.3negsub 9090  negsubd 9158  negsubi 9119
[Apostol] p. 18Theorem I.4negneg 9092  negnegd 9143  negnegi 9111
[Apostol] p. 18Theorem I.5subdi 9208  subdid 9230  subdii 9223  subdir 9209  subdird 9231  subdiri 9224
[Apostol] p. 18Theorem I.6mul01 8986  mul01d 9006  mul01i 8997  mul02 8985  mul02d 9005  mul02i 8996
[Apostol] p. 18Theorem I.7mulcan 9400  mulcan2d 9397  mulcand 9396  mulcani 9402
[Apostol] p. 18Theorem I.8receu 9408
[Apostol] p. 18Theorem I.9divrec 9435  divrecd 9534  divreci 9500  divreczi 9493
[Apostol] p. 18Theorem I.10recrec 9452  recreci 9487
[Apostol] p. 18Theorem I.11mul0or 9403  mul0ord 9413  mul0ori 9411
[Apostol] p. 18Theorem I.12mul2neg 9214  mul2negd 9229  mul2negi 9222  mulneg1 9211  mulneg1d 9227  mulneg1i 9220
[Apostol] p. 18Theorem I.13divadddiv 9470  divadddivd 9575  divadddivi 9517
[Apostol] p. 18Theorem I.14divmuldiv 9455  divmuldivd 9572  divmuldivi 9515
[Apostol] p. 18Theorem I.15divdivdiv 9456  divdivdivd 9578  divdivdivi 9518
[Apostol] p. 20Axiom 7rpaddcl 10369  rpaddcld 10400  rpmulcl 10370  rpmulcld 10401
[Apostol] p. 20Axiom 8rpneg 10378
[Apostol] p. 20Axiom 90nrp 10379
[Apostol] p. 20Theorem I.17lttri 8940
[Apostol] p. 20Theorem I.18ltadd1d 9360  ltadd1dd 9378  ltadd1i 9322
[Apostol] p. 20Theorem I.19ltmul1 9601  ltmul1a 9600  ltmul1i 9670  ltmul1ii 9680  ltmul2 9602  ltmul2d 10423  ltmul2dd 10437  ltmul2i 9673
[Apostol] p. 20Theorem I.20msqgt0 9289  msqgt0d 9335  msqgt0i 9305
[Apostol] p. 20Theorem I.210lt1 9291
[Apostol] p. 20Theorem I.23lt0neg1 9275  lt0neg1d 9337  ltneg 9269  ltnegd 9345  ltnegi 9312
[Apostol] p. 20Theorem I.25lt2add 9254  lt2addd 9389  lt2addi 9330
[Apostol] p. 20Definition of positive numbersdf-rp 10350
[Apostol] p. 21Exercise 4recgt0 9595  recgt0d 9686  recgt0i 9656  recgt0ii 9657
[Apostol] p. 22Definition of integersdf-z 10020
[Apostol] p. 22Definition of positive integersdfnn3 9755
[Apostol] p. 22Definition of rationalsdf-q 10312
[Apostol] p. 24Theorem I.26supeu 7200
[Apostol] p. 26Theorem I.28nnunb 9956
[Apostol] p. 26Theorem I.29arch 9957
[Apostol] p. 28Exercise 2btwnz 10109
[Apostol] p. 28Exercise 3nnrecl 9958
[Apostol] p. 28Exercise 4rebtwnz 10310
[Apostol] p. 28Exercise 5zbtwnre 10309
[Apostol] p. 28Exercise 6qbtwnre 10520
[Apostol] p. 28Exercise 10(a)zneo 10089
[Apostol] p. 29Theorem I.35msqsqrd 11916  resqrth 11735  sqrth 11842  sqrthi 11848  sqsqrd 11915
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9744
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10279
[Apostol] p. 361Remarkcrreczi 11220
[Apostol] p. 363Remarkabsgt0i 11876
[Apostol] p. 363Exampleabssubd 11929  abssubi 11880
[Baer] p. 40Property (b)mapdord 31095
[Baer] p. 40Property (c)mapd11 31096
[Baer] p. 40Property (e)mapdin 31119  mapdlsm 31121
[Baer] p. 40Property (f)mapd0 31122
[Baer] p. 40Definition of projectivitydf-mapd 31082  mapd1o 31105
[Baer] p. 41Property (g)mapdat 31124
[Baer] p. 44Part (1)mapdpg 31163
[Baer] p. 45Part (2)hdmap1eq 31259  mapdheq 31185  mapdheq2 31186  mapdheq2biN 31187
[Baer] p. 45Part (3)baerlem3 31170
[Baer] p. 46Part (4)mapdheq4 31189  mapdheq4lem 31188
[Baer] p. 46Part (5)baerlem5a 31171  baerlem5abmN 31175  baerlem5amN 31173  baerlem5b 31172  baerlem5bmN 31174
[Baer] p. 47Part (6)hdmap1l6 31279  hdmap1l6a 31267  hdmap1l6e 31272  hdmap1l6f 31273  hdmap1l6g 31274  hdmap1l6lem1 31265  hdmap1l6lem2 31266  hdmap1p6N 31280  mapdh6N 31204  mapdh6aN 31192  mapdh6eN 31197  mapdh6fN 31198  mapdh6gN 31199  mapdh6lem1N 31190  mapdh6lem2N 31191
[Baer] p. 48Part 9hdmapval 31288
[Baer] p. 48Part 10hdmap10 31300
[Baer] p. 48Part 11hdmapadd 31303
[Baer] p. 48Part (6)hdmap1l6h 31275  mapdh6hN 31200
[Baer] p. 48Part (7)mapdh75cN 31210  mapdh75d 31211  mapdh75e 31209  mapdh75fN 31212  mapdh7cN 31206  mapdh7dN 31207  mapdh7eN 31205  mapdh7fN 31208
[Baer] p. 48Part (8)mapdh8 31246  mapdh8a 31232  mapdh8aa 31233  mapdh8ab 31234  mapdh8ac 31235  mapdh8ad 31236  mapdh8b 31237  mapdh8c 31238  mapdh8d 31240  mapdh8d0N 31239  mapdh8e 31241  mapdh8fN 31242  mapdh8g 31243  mapdh8i 31244  mapdh8j 31245
[Baer] p. 48Part (9)mapdh9a 31247
[Baer] p. 48Equation 10mapdhvmap 31226
[Baer] p. 49Part 12hdmap11 31308  hdmapeq0 31304  hdmapf1oN 31325  hdmapneg 31306  hdmaprnN 31324  hdmaprnlem1N 31309  hdmaprnlem3N 31310  hdmaprnlem3uN 31311  hdmaprnlem4N 31313  hdmaprnlem6N 31314  hdmaprnlem7N 31315  hdmaprnlem8N 31316  hdmaprnlem9N 31317  hdmapsub 31307
[Baer] p. 49Part 14hdmap14lem1 31328  hdmap14lem10 31337  hdmap14lem1a 31326  hdmap14lem2N 31329  hdmap14lem2a 31327  hdmap14lem3 31330  hdmap14lem8 31335  hdmap14lem9 31336
[Baer] p. 50Part 14hdmap14lem11 31338  hdmap14lem12 31339  hdmap14lem13 31340  hdmap14lem14 31341  hdmap14lem15 31342  hgmapval 31347
[Baer] p. 50Part 15hgmapadd 31354  hgmapmul 31355  hgmaprnlem2N 31357  hgmapvs 31351
[Baer] p. 50Part 16hgmaprnN 31361
[Baer] p. 110Lemma 1hdmapip0com 31377
[Baer] p. 110Line 27hdmapinvlem1 31378
[Baer] p. 110Line 28hdmapinvlem2 31379
[Baer] p. 110Line 30hdmapinvlem3 31380
[Baer] p. 110Part 1.2hdmapglem5 31382  hgmapvv 31386
[Baer] p. 110Proposition 1hdmapinvlem4 31381
[Baer] p. 111Line 10hgmapvvlem1 31383
[Baer] p. 111Line 15hdmapg 31390  hdmapglem7 31389
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2148
[BellMachover] p. 460Notationdf-mo 2149
[BellMachover] p. 460Definitionmo3 2175
[BellMachover] p. 461Axiom Extax-ext 2265
[BellMachover] p. 462Theorem 1.1bm1.1 2269
[BellMachover] p. 463Axiom Repaxrep5 4137
[BellMachover] p. 463Scheme Sepaxsep 4141
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4145
[BellMachover] p. 466Axiom Powaxpow3 4190
[BellMachover] p. 466Axiom Unionaxun2 4513
[BellMachover] p. 468Definitiondf-ord 4394
[BellMachover] p. 469Theorem 2.2(i)ordirr 4409
[BellMachover] p. 469Theorem 2.2(iii)onelon 4416
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4411
[BellMachover] p. 471Definition of Ndf-om 4656
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4596
[BellMachover] p. 471Definition of Limdf-lim 4396
[BellMachover] p. 472Axiom Infzfinf2 7338
[BellMachover] p. 473Theorem 2.8limom 4670
[BellMachover] p. 477Equation 3.1df-r1 7431
[BellMachover] p. 478Definitionrankval2 7485
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7449  r1ord3g 7446
[BellMachover] p. 480Axiom Regzfreg2 7305
[BellMachover] p. 488Axiom ACac5 8099  dfac4 7744
[BellMachover] p. 490Definition of alephalephval3 7732
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28776
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22925
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22967  chirredi 22966
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22955
[Beran] p. 3Definition of joinsshjval3 21925
[Beran] p. 39Theorem 2.3(i)cmcm2 22187  cmcm2i 22164  cmcm2ii 22169  cmt2N 28707
[Beran] p. 40Theorem 2.3(iii)lecm 22188  lecmi 22173  lecmii 22174
[Beran] p. 45Theorem 3.4cmcmlem 22162
[Beran] p. 49Theorem 4.2cm2j 22191  cm2ji 22196  cm2mi 22197
[Beran] p. 95Definitiondf-sh 21778  issh2 21780
[Beran] p. 95Lemma 3.1(S5)his5 21657
[Beran] p. 95Lemma 3.1(S6)his6 21670
[Beran] p. 95Lemma 3.1(S7)his7 21661
[Beran] p. 95Lemma 3.2(S8)ho01i 22400
[Beran] p. 95Lemma 3.2(S9)hoeq1 22402
[Beran] p. 95Lemma 3.2(S10)ho02i 22401
[Beran] p. 95Lemma 3.2(S11)hoeq2 22403
[Beran] p. 95Postulate (S1)ax-his1 21653  his1i 21671
[Beran] p. 95Postulate (S2)ax-his2 21654
[Beran] p. 95Postulate (S3)ax-his3 21655
[Beran] p. 95Postulate (S4)ax-his4 21656
[Beran] p. 96Definition of normdf-hnorm 21540  dfhnorm2 21693  normval 21695
[Beran] p. 96Definition for Cauchy sequencehcau 21755
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21545
[Beran] p. 96Definition of complete subspaceisch3 21813
[Beran] p. 96Definition of convergedf-hlim 21544  hlimi 21759
[Beran] p. 97Theorem 3.3(i)norm-i-i 21704  norm-i 21700
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21708  norm-ii 21709  normlem0 21680  normlem1 21681  normlem2 21682  normlem3 21683  normlem4 21684  normlem5 21685  normlem6 21686  normlem7 21687  normlem7tALT 21690
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21710  norm-iii 21711
[Beran] p. 98Remark 3.4bcs 21752  bcsiALT 21750  bcsiHIL 21751
[Beran] p. 98Remark 3.4(B)normlem9at 21692  normpar 21726  normpari 21725
[Beran] p. 98Remark 3.4(C)normpyc 21717  normpyth 21716  normpythi 21713
[Beran] p. 99Remarklnfn0 22619  lnfn0i 22614  lnop0 22538  lnop0i 22542
[Beran] p. 99Theorem 3.5(i)nmcexi 22598  nmcfnex 22625  nmcfnexi 22623  nmcopex 22601  nmcopexi 22599
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22626  nmcfnlbi 22624  nmcoplb 22602  nmcoplbi 22600
[Beran] p. 99Theorem 3.5(iii)lnfncon 22628  lnfnconi 22627  lnopcon 22607  lnopconi 22606
[Beran] p. 100Lemma 3.6normpar2i 21727
[Beran] p. 101Lemma 3.6norm3adifi 21724  norm3adifii 21719  norm3dif 21721  norm3difi 21718
[Beran] p. 102Theorem 3.7(i)chocunii 21872  pjhth 21964  pjhtheu 21965  pjpjhth 21996  pjpjhthi 21997  pjth 18797
[Beran] p. 102Theorem 3.7(ii)ococ 21977  ococi 21976
[Beran] p. 103Remark 3.8nlelchi 22633
[Beran] p. 104Theorem 3.9riesz3i 22634  riesz4 22636  riesz4i 22635
[Beran] p. 104Theorem 3.10cnlnadj 22651  cnlnadjeu 22650  cnlnadjeui 22649  cnlnadji 22648  cnlnadjlem1 22639  nmopadjlei 22660
[Beran] p. 106Theorem 3.11(i)adjeq0 22663
[Beran] p. 106Theorem 3.11(v)nmopadji 22662
[Beran] p. 106Theorem 3.11(ii)adjmul 22664
[Beran] p. 106Theorem 3.11(iv)adjadj 22508
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22674  nmopcoadji 22673
[Beran] p. 106Theorem 3.11(iii)adjadd 22665
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22675
[Beran] p. 106Theorem 3.11(viii)adjcoi 22672  pjadj2coi 22776  pjadjcoi 22733
[Beran] p. 107Definitiondf-ch 21793  isch2 21795
[Beran] p. 107Remark 3.12choccl 21877  isch3 21813  occl 21875  ocsh 21854  shoccl 21876  shocsh 21855
[Beran] p. 107Remark 3.12(B)ococin 21979
[Beran] p. 108Theorem 3.13chintcl 21903
[Beran] p. 109Property (i)pjadj2 22759  pjadj3 22760  pjadji 22256  pjadjii 22245
[Beran] p. 109Property (ii)pjidmco 22753  pjidmcoi 22749  pjidmi 22244
[Beran] p. 110Definition of projector orderingpjordi 22745
[Beran] p. 111Remarkho0val 22322  pjch1 22241
[Beran] p. 111Definitiondf-hfmul 22306  df-hfsum 22305  df-hodif 22304  df-homul 22303  df-hosum 22302
[Beran] p. 111Lemma 4.4(i)pjo 22242
[Beran] p. 111Lemma 4.4(ii)pjch 22265  pjchi 22003
[Beran] p. 111Lemma 4.4(iii)pjoc2 22010  pjoc2i 22009
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22251
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22737  pjssmii 22252
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22736
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22735
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22740
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22738  pjssge0ii 22253
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22739  pjdifnormii 22254
[BourbakiEns] p. Proposition 8fcof1 5758  fcofo 5759
[BourbakiFVR] p. Definition 1isder 25106
[BourbakiTop1] p. Remarkxnegmnf 10531  xnegpnf 10530
[BourbakiTop1] p. Remark rexneg 10532
[BourbakiTop1] p. Theoremneiss 16840
[BourbakiTop1] p. Axiom GT'tgpsubcn 17767
[BourbakiTop1] p. Example 1snfil 17553
[BourbakiTop1] p. Example 2neifil 17569
[BourbakiTop1] p. Definitionistgp 17754
[BourbakiTop1] p. Propositioncnpco 16990  ishmeo 17444  neips 16844
[BourbakiTop1] p. Definition 1filintn0 17550
[BourbakiTop1] p. Proposition 9cnpflf2 17689
[BourbakiTop1] p. Theorem 1 (d)iscncl 16992
[BourbakiTop1] p. Proposition Vissnei2 16847
[BourbakiTop1] p. Definition C'''df-cmp 17108
[BourbakiTop1] p. Proposition Viiinnei 16856
[BourbakiTop1] p. Proposition Vivneissex 16858
[BourbakiTop1] p. Proposition Viiielnei 16842  ssnei 16841
[BourbakiTop1] p. Remark below def. 1filn0 17551
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17535
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17552
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27212  stoweid 27211
[BrosowskiDeutsh] p. 89Theorem for the non trivial casestoweidlem62 27210
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27149  stoweidlem10 27158  stoweidlem14 27162  stoweidlem15 27163  stoweidlem35 27183  stoweidlem36 27184  stoweidlem37 27185  stoweidlem38 27186  stoweidlem40 27188  stoweidlem41 27189  stoweidlem43 27191  stoweidlem44 27192  stoweidlem46 27194  stoweidlem5 27153  stoweidlem50 27198  stoweidlem52 27200  stoweidlem53 27201  stoweidlem55 27203  stoweidlem56 27204
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27171  stoweidlem24 27172  stoweidlem27 27175  stoweidlem28 27176  stoweidlem30 27178
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27193  stoweidlem49 27197  stoweidlem7 27155
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27179  stoweidlem39 27187  stoweidlem42 27190  stoweidlem48 27196  stoweidlem51 27199  stoweidlem54 27202  stoweidlem57 27205  stoweidlem58 27206
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27173
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27182
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27165
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27207
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27208
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27166
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27159  stoweidlem26 27174
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27161
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27209
[ChoquetDD] p. 2Definition of mappingdf-mpt 4080
[Clemente] p. 10Definition ITnatded 4
[Clemente] p. 10Definition I` `m,nnatded 4
[Clemente] p. 11Definition E=>m,nnatded 4
[Clemente] p. 11Definition I=>m,nnatded 4
[Clemente] p. 11Definition E` `(1)natded 4
[Clemente] p. 11Definition E` `(2)natded 4
[Clemente] p. 12Definition E` `m,n,pnatded 4
[Clemente] p. 12Definition I` `n(1)natded 4
[Clemente] p. 12Definition I` `n(2)natded 4
[Clemente] p. 13Definition I` `m,n,pnatded 4
[Clemente] p. 14Definition E` `nnatded 4
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 20812  ex-natded5.2 20811
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 20815  ex-natded5.3 20814
[Clemente] p. 18Theorem 5.5ex-natded5.5 20817
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 20819  ex-natded5.7 20818
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 20821  ex-natded5.8 20820
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 20823  ex-natded5.13 20822
[Clemente] p. 32Definition I` `nnatded 4
[Clemente] p. 32Definition E` `m,n,p,anatded 4
[Clemente] p. 32Definition E` `n,tnatded 4
[Clemente] p. 32Definition I` `n,tnatded 4
[Clemente] p. 43Theorem 9.20ex-natded9.20 20824
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 20825
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 20827  ex-natded9.26 20826
[Cohen] p. 301Remarkrelogoprlem 19938
[Cohen] p. 301Property 2relogmul 19939  relogmuld 19970
[Cohen] p. 301Property 3relogdiv 19940  relogdivd 19971
[Cohen] p. 301Property 4relogexp 19943
[Cohen] p. 301Property 1alog1 19933
[Cohen] p. 301Property 1bloge 19934
[Cohn] p. 81Section II.5acsdomd 14278  acsinfd 14277  acsinfdimd 14279  acsmap2d 14276  acsmapd 14275
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10959
[Crawley] p. 1Definition of posetdf-poset 14074
[Crawley] p. 107Theorem 13.2hlsupr 28842
[Crawley] p. 110Theorem 13.3arglem1N 29646  dalaw 29342
[Crawley] p. 111Theorem 13.4hlathil 31421
[Crawley] p. 111Definition of set Wdf-watsN 29446
[Crawley] p. 111Definition of dilationdf-dilN 29562  df-ldil 29560  isldil 29566
[Crawley] p. 111Definition of translationdf-ltrn 29561  df-trnN 29563  isltrn 29575  ltrnu 29577
[Crawley] p. 112Lemma Acdlema1N 29247  cdlema2N 29248  exatleN 28860
[Crawley] p. 112Lemma B1cvrat 28932  cdlemb 29250  cdlemb2 29497  cdlemb3 30062  idltrn 29606  l1cvat 28512  lhpat 29499  lhpat2 29501  lshpat 28513  ltrnel 29595  ltrnmw 29607
[Crawley] p. 112Lemma Ccdlemc1 29647  cdlemc2 29648  ltrnnidn 29630  trlat 29625  trljat1 29622  trljat2 29623  trljat3 29624  trlne 29641  trlnidat 29629  trlnle 29642
[Crawley] p. 112Definition of automorphismdf-pautN 29447
[Crawley] p. 113Lemma Ccdlemc 29653  cdlemc3 29649  cdlemc4 29650
[Crawley] p. 113Lemma Dcdlemd 29663  cdlemd1 29654  cdlemd2 29655  cdlemd3 29656  cdlemd4 29657  cdlemd5 29658  cdlemd6 29659  cdlemd7 29660  cdlemd8 29661  cdlemd9 29662  cdleme31sde 29841  cdleme31se 29838  cdleme31se2 29839  cdleme31snd 29842  cdleme32a 29897  cdleme32b 29898  cdleme32c 29899  cdleme32d 29900  cdleme32e 29901  cdleme32f 29902  cdleme32fva 29893  cdleme32fva1 29894  cdleme32fvcl 29896  cdleme32le 29903  cdleme48fv 29955  cdleme4gfv 29963  cdleme50eq 29997  cdleme50f 29998  cdleme50f1 29999  cdleme50f1o 30002  cdleme50laut 30003  cdleme50ldil 30004  cdleme50lebi 29996  cdleme50rn 30001  cdleme50rnlem 30000  cdlemeg49le 29967  cdlemeg49lebilem 29995
[Crawley] p. 113Lemma Ecdleme 30016  cdleme00a 29665  cdleme01N 29677  cdleme02N 29678  cdleme0a 29667  cdleme0aa 29666  cdleme0b 29668  cdleme0c 29669  cdleme0cp 29670  cdleme0cq 29671  cdleme0dN 29672  cdleme0e 29673  cdleme0ex1N 29679  cdleme0ex2N 29680  cdleme0fN 29674  cdleme0gN 29675  cdleme0moN 29681  cdleme1 29683  cdleme10 29710  cdleme10tN 29714  cdleme11 29726  cdleme11a 29716  cdleme11c 29717  cdleme11dN 29718  cdleme11e 29719  cdleme11fN 29720  cdleme11g 29721  cdleme11h 29722  cdleme11j 29723  cdleme11k 29724  cdleme11l 29725  cdleme12 29727  cdleme13 29728  cdleme14 29729  cdleme15 29734  cdleme15a 29730  cdleme15b 29731  cdleme15c 29732  cdleme15d 29733  cdleme16 29741  cdleme16aN 29715  cdleme16b 29735  cdleme16c 29736  cdleme16d 29737  cdleme16e 29738  cdleme16f 29739  cdleme16g 29740  cdleme19a 29759  cdleme19b 29760  cdleme19c 29761  cdleme19d 29762  cdleme19e 29763  cdleme19f 29764  cdleme1b 29682  cdleme2 29684  cdleme20aN 29765  cdleme20bN 29766  cdleme20c 29767  cdleme20d 29768  cdleme20e 29769  cdleme20f 29770  cdleme20g 29771  cdleme20h 29772  cdleme20i 29773  cdleme20j 29774  cdleme20k 29775  cdleme20l 29778  cdleme20l1 29776  cdleme20l2 29777  cdleme20m 29779  cdleme20y 29758  cdleme20zN 29757  cdleme21 29793  cdleme21d 29786  cdleme21e 29787  cdleme22a 29796  cdleme22aa 29795  cdleme22b 29797  cdleme22cN 29798  cdleme22d 29799  cdleme22e 29800  cdleme22eALTN 29801  cdleme22f 29802  cdleme22f2 29803  cdleme22g 29804  cdleme23a 29805  cdleme23b 29806  cdleme23c 29807  cdleme26e 29815  cdleme26eALTN 29817  cdleme26ee 29816  cdleme26f 29819  cdleme26f2 29821  cdleme26f2ALTN 29820  cdleme26fALTN 29818  cdleme27N 29825  cdleme27a 29823  cdleme27cl 29822  cdleme28c 29828  cdleme3 29693  cdleme30a 29834  cdleme31fv 29846  cdleme31fv1 29847  cdleme31fv1s 29848  cdleme31fv2 29849  cdleme31id 29850  cdleme31sc 29840  cdleme31sdnN 29843  cdleme31sn 29836  cdleme31sn1 29837  cdleme31sn1c 29844  cdleme31sn2 29845  cdleme31so 29835  cdleme35a 29904  cdleme35b 29906  cdleme35c 29907  cdleme35d 29908  cdleme35e 29909  cdleme35f 29910  cdleme35fnpq 29905  cdleme35g 29911  cdleme35h 29912  cdleme35h2 29913  cdleme35sn2aw 29914  cdleme35sn3a 29915  cdleme36a 29916  cdleme36m 29917  cdleme37m 29918  cdleme38m 29919  cdleme38n 29920  cdleme39a 29921  cdleme39n 29922  cdleme3b 29685  cdleme3c 29686  cdleme3d 29687  cdleme3e 29688  cdleme3fN 29689  cdleme3fa 29692  cdleme3g 29690  cdleme3h 29691  cdleme4 29694  cdleme40m 29923  cdleme40n 29924  cdleme40v 29925  cdleme40w 29926  cdleme41fva11 29933  cdleme41sn3aw 29930  cdleme41sn4aw 29931  cdleme41snaw 29932  cdleme42a 29927  cdleme42b 29934  cdleme42c 29928  cdleme42d 29929  cdleme42e 29935  cdleme42f 29936  cdleme42g 29937  cdleme42h 29938  cdleme42i 29939  cdleme42k 29940  cdleme42ke 29941  cdleme42keg 29942  cdleme42mN 29943  cdleme42mgN 29944  cdleme43aN 29945  cdleme43bN 29946  cdleme43cN 29947  cdleme43dN 29948  cdleme5 29696  cdleme50ex 30015  cdleme50ltrn 30013  cdleme51finvN 30012  cdleme51finvfvN 30011  cdleme51finvtrN 30014  cdleme6 29697  cdleme7 29705  cdleme7a 29699  cdleme7aa 29698  cdleme7b 29700  cdleme7c 29701  cdleme7d 29702  cdleme7e 29703  cdleme7ga 29704  cdleme8 29706  cdleme8tN 29711  cdleme9 29709  cdleme9a 29707  cdleme9b 29708  cdleme9tN 29713  cdleme9taN 29712  cdlemeda 29754  cdlemedb 29753  cdlemednpq 29755  cdlemednuN 29756  cdlemefr27cl 29859  cdlemefr32fva1 29866  cdlemefr32fvaN 29865  cdlemefrs32fva 29856  cdlemefrs32fva1 29857  cdlemefs27cl 29869  cdlemefs32fva1 29879  cdlemefs32fvaN 29878  cdlemesner 29752  cdlemeulpq 29676
[Crawley] p. 114Lemma E4atex 29532  4atexlem7 29531  cdleme0nex 29746  cdleme17a 29742  cdleme17c 29744  cdleme17d 29954  cdleme17d1 29745  cdleme17d2 29951  cdleme18a 29747  cdleme18b 29748  cdleme18c 29749  cdleme18d 29751  cdleme4a 29695
[Crawley] p. 115Lemma Ecdleme21a 29781  cdleme21at 29784  cdleme21b 29782  cdleme21c 29783  cdleme21ct 29785  cdleme21f 29788  cdleme21g 29789  cdleme21h 29790  cdleme21i 29791  cdleme22gb 29750
[Crawley] p. 116Lemma Fcdlemf 30019  cdlemf1 30017  cdlemf2 30018
[Crawley] p. 116Lemma Gcdlemftr1 30023  cdlemg16 30113  cdlemg28 30160  cdlemg28a 30149  cdlemg28b 30159  cdlemg3a 30053  cdlemg42 30185  cdlemg43 30186  cdlemg44 30189  cdlemg44a 30187  cdlemg46 30191  cdlemg47 30192  cdlemg9 30090  ltrnco 30175  ltrncom 30194  tgrpabl 30207  trlco 30183
[Crawley] p. 116Definition of Gdf-tgrp 30199
[Crawley] p. 117Lemma Gcdlemg17 30133  cdlemg17b 30118
[Crawley] p. 117Definition of Edf-edring-rN 30212  df-edring 30213
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30216
[Crawley] p. 118Remarktendopltp 30236
[Crawley] p. 118Lemma Hcdlemh 30273  cdlemh1 30271  cdlemh2 30272
[Crawley] p. 118Lemma Icdlemi 30276  cdlemi1 30274  cdlemi2 30275
[Crawley] p. 118Lemma Jcdlemj1 30277  cdlemj2 30278  cdlemj3 30279  tendocan 30280
[Crawley] p. 118Lemma Kcdlemk 30430  cdlemk1 30287  cdlemk10 30299  cdlemk11 30305  cdlemk11t 30402  cdlemk11ta 30385  cdlemk11tb 30387  cdlemk11tc 30401  cdlemk11u-2N 30345  cdlemk11u 30327  cdlemk12 30306  cdlemk12u-2N 30346  cdlemk12u 30328  cdlemk13-2N 30332  cdlemk13 30308  cdlemk14-2N 30334  cdlemk14 30310  cdlemk15-2N 30335  cdlemk15 30311  cdlemk16-2N 30336  cdlemk16 30313  cdlemk16a 30312  cdlemk17-2N 30337  cdlemk17 30314  cdlemk18-2N 30342  cdlemk18-3N 30356  cdlemk18 30324  cdlemk19-2N 30343  cdlemk19 30325  cdlemk19u 30426  cdlemk1u 30315  cdlemk2 30288  cdlemk20-2N 30348  cdlemk20 30330  cdlemk21-2N 30347  cdlemk21N 30329  cdlemk22-3 30357  cdlemk22 30349  cdlemk23-3 30358  cdlemk24-3 30359  cdlemk25-3 30360  cdlemk26-3 30362  cdlemk26b-3 30361  cdlemk27-3 30363  cdlemk28-3 30364  cdlemk29-3 30367  cdlemk3 30289  cdlemk30 30350  cdlemk31 30352  cdlemk32 30353  cdlemk33N 30365  cdlemk34 30366  cdlemk35 30368  cdlemk36 30369  cdlemk37 30370  cdlemk38 30371  cdlemk39 30372  cdlemk39u 30424  cdlemk4 30290  cdlemk41 30376  cdlemk42 30397  cdlemk42yN 30400  cdlemk43N 30419  cdlemk45 30403  cdlemk46 30404  cdlemk47 30405  cdlemk48 30406  cdlemk49 30407  cdlemk5 30292  cdlemk50 30408  cdlemk51 30409  cdlemk52 30410  cdlemk53 30413  cdlemk54 30414  cdlemk55 30417  cdlemk55u 30422  cdlemk56 30427  cdlemk5a 30291  cdlemk5auN 30316  cdlemk5u 30317  cdlemk6 30293  cdlemk6u 30318  cdlemk7 30304  cdlemk7u-2N 30344  cdlemk7u 30326  cdlemk8 30294  cdlemk9 30295  cdlemk9bN 30296  cdlemki 30297  cdlemkid 30392  cdlemkj-2N 30338  cdlemkj 30319  cdlemksat 30302  cdlemksel 30301  cdlemksv 30300  cdlemksv2 30303  cdlemkuat 30322  cdlemkuel-2N 30340  cdlemkuel-3 30354  cdlemkuel 30321  cdlemkuv-2N 30339  cdlemkuv2-2 30341  cdlemkuv2-3N 30355  cdlemkuv2 30323  cdlemkuvN 30320  cdlemkvcl 30298  cdlemky 30382  cdlemkyyN 30418  tendoex 30431
[Crawley] p. 120Remarkdva1dim 30441
[Crawley] p. 120Lemma Lcdleml1N 30432  cdleml2N 30433  cdleml3N 30434  cdleml4N 30435  cdleml5N 30436  cdleml6 30437  cdleml7 30438  cdleml8 30439  cdleml9 30440  dia1dim 30518
[Crawley] p. 120Lemma Mdia11N 30505  diaf11N 30506  dialss 30503  diaord 30504  dibf11N 30618  djajN 30594
[Crawley] p. 120Definition of isomorphism mapdiaval 30489
[Crawley] p. 121Lemma Mcdlemm10N 30575  dia2dimlem1 30521  dia2dimlem2 30522  dia2dimlem3 30523  dia2dimlem4 30524  dia2dimlem5 30525  diaf1oN 30587  diarnN 30586  dvheveccl 30569  dvhopN 30573
[Crawley] p. 121Lemma Ncdlemn 30669  cdlemn10 30663  cdlemn11 30668  cdlemn11a 30664  cdlemn11b 30665  cdlemn11c 30666  cdlemn11pre 30667  cdlemn2 30652  cdlemn2a 30653  cdlemn3 30654  cdlemn4 30655  cdlemn4a 30656  cdlemn5 30658  cdlemn5pre 30657  cdlemn6 30659  cdlemn7 30660  cdlemn8 30661  cdlemn9 30662  diclspsn 30651
[Crawley] p. 121Definition of phi(q)df-dic 30630
[Crawley] p. 122Lemma Ndih11 30722  dihf11 30724  dihjust 30674  dihjustlem 30673  dihord 30721  dihord1 30675  dihord10 30680  dihord11b 30679  dihord11c 30681  dihord2 30684  dihord2a 30676  dihord2b 30677  dihord2cN 30678  dihord2pre 30682  dihord2pre2 30683  dihordlem6 30670  dihordlem7 30671  dihordlem7b 30672
[Crawley] p. 122Definition of isomorphism mapdihffval 30687  dihfval 30688  dihval 30689
[Eisenberg] p. 67Definition 5.3df-dif 3156
[Eisenberg] p. 82Definition 6.3dfom3 7343
[Eisenberg] p. 125Definition 8.21df-map 6769
[Eisenberg] p. 216Example 13.2(4)omenps 7350
[Eisenberg] p. 310Theorem 19.8cardprc 7608
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8172
[Enderton] p. 18Axiom of Empty Setaxnul 4149
[Enderton] p. 19Definitiondf-tp 3649
[Enderton] p. 26Exercise 5unissb 3858
[Enderton] p. 26Exercise 10pwel 4224
[Enderton] p. 28Exercise 7(b)pwun 4301
[Enderton] p. 30Theorem "Distributive laws"iinin1 3974  iinin2 3973  iinun2 3969  iunin1 3968  iunin2 3967
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3972  iundif2 3970
[Enderton] p. 32Exercise 20unineq 3420
[Enderton] p. 33Exercise 23iinuni 3986
[Enderton] p. 33Exercise 25iununi 3987
[Enderton] p. 33Exercise 24(a)iinpw 3991
[Enderton] p. 33Exercise 24(b)iunpw 4569  iunpwss 3992
[Enderton] p. 36Definitionopthwiener 4267
[Enderton] p. 38Exercise 6(a)unipw 4223
[Enderton] p. 38Exercise 6(b)pwuni 4205
[Enderton] p. 41Lemma 3Dopeluu 4525  rnex 4941  rnexg 4939
[Enderton] p. 41Exercise 8dmuni 4887  rnuni 5091
[Enderton] p. 42Definition of a functiondffun7 5246  dffun8 5247
[Enderton] p. 43Definition of function valuefunfv2 5548
[Enderton] p. 43Definition of single-rootedfuncnv 5275
[Enderton] p. 44Definition (d)dfima2 5013  dfima3 5014
[Enderton] p. 47Theorem 3Hfvco2 5555
[Enderton] p. 49Axiom of Choice (first form)ac7 8095  ac7g 8096  df-ac 7738  dfac2 7752  dfac2a 7751  dfac3 7743  dfac7 7753
[Enderton] p. 50Theorem 3K(a)imauni 5733
[Enderton] p. 52Definitiondf-map 6769
[Enderton] p. 53Exercise 21coass 5189
[Enderton] p. 53Exercise 27dmco 5179
[Enderton] p. 53Exercise 14(a)funin 5284
[Enderton] p. 53Exercise 22(a)imass2 5048
[Enderton] p. 54Remarkixpf 6833  ixpssmap 6845
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6813
[Enderton] p. 55Axiom of Choice (second form)ac9 8105  ac9s 8115
[Enderton] p. 56Theorem 3Merref 6675
[Enderton] p. 57Lemma 3Nerthi 6701
[Enderton] p. 57Definitiondf-ec 6657
[Enderton] p. 58Definitiondf-qs 6661
[Enderton] p. 60Theorem 3Qth3q 6762  th3qcor 6761  th3qlem1 6759  th3qlem2 6760
[Enderton] p. 61Exercise 35df-ec 6657
[Enderton] p. 65Exercise 56(a)dmun 4884
[Enderton] p. 68Definition of successordf-suc 4397
[Enderton] p. 71Definitiondf-tr 4115  dftr4 4119
[Enderton] p. 72Theorem 4Eunisuc 4467
[Enderton] p. 73Exercise 6unisuc 4467
[Enderton] p. 73Exercise 5(a)truni 4128
[Enderton] p. 73Exercise 5(b)trint 4129  trintALT 27925
[Enderton] p. 79Theorem 4I(A1)nna0 6597
[Enderton] p. 79Theorem 4I(A2)nnasuc 6599  onasuc 6522
[Enderton] p. 79Definition of operation valuedf-ov 5822
[Enderton] p. 80Theorem 4J(A1)nnm0 6598
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6600  onmsuc 6523
[Enderton] p. 81Theorem 4K(1)nnaass 6615
[Enderton] p. 81Theorem 4K(2)nna0r 6602  nnacom 6610
[Enderton] p. 81Theorem 4K(3)nndi 6616
[Enderton] p. 81Theorem 4K(4)nnmass 6617
[Enderton] p. 81Theorem 4K(5)nnmcom 6619
[Enderton] p. 82Exercise 16nnm0r 6603  nnmsucr 6618
[Enderton] p. 88Exercise 23nnaordex 6631
[Enderton] p. 129Definitiondf-en 6859
[Enderton] p. 132Theorem 6B(b)canth 6287
[Enderton] p. 133Exercise 1xpomen 7638
[Enderton] p. 133Exercise 2qnnen 12486
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7040
[Enderton] p. 135Corollary 6Cphp3 7042
[Enderton] p. 136Corollary 6Enneneq 7039
[Enderton] p. 136Corollary 6D(a)pssinf 7068
[Enderton] p. 136Corollary 6D(b)ominf 7070
[Enderton] p. 137Lemma 6Fpssnn 7076
[Enderton] p. 138Corollary 6Gssfi 7078
[Enderton] p. 139Theorem 6H(c)mapen 7020
[Enderton] p. 142Theorem 6I(3)xpcdaen 7804
[Enderton] p. 142Theorem 6I(4)mapcdaen 7805
[Enderton] p. 143Theorem 6Jcda0en 7800  cda1en 7796
[Enderton] p. 144Exercise 13iunfi 7139  unifi 7140  unifi2 7141
[Enderton] p. 144Corollary 6Kundif2 3531  unfi 7119  unfi2 7121
[Enderton] p. 145Figure 38ffoss 5470
[Enderton] p. 145Definitiondf-dom 6860
[Enderton] p. 146Example 1domen 6870  domeng 6871
[Enderton] p. 146Example 3nndomo 7049  nnsdom 7349  nnsdomg 7111
[Enderton] p. 149Theorem 6L(a)cdadom2 7808
[Enderton] p. 149Theorem 6L(c)mapdom1 7021  xpdom1 6956  xpdom1g 6954  xpdom2g 6953
[Enderton] p. 149Theorem 6L(d)mapdom2 7027
[Enderton] p. 151Theorem 6Mzorn 8129  zorng 8126
[Enderton] p. 151Theorem 6M(4)ac8 8114  dfac5 7750
[Enderton] p. 159Theorem 6Qunictb 8192
[Enderton] p. 164Exampleinfdif 7830
[Enderton] p. 168Definitiondf-po 4313
[Enderton] p. 192Theorem 7M(a)oneli 4499
[Enderton] p. 192Theorem 7M(b)ontr1 4437
[Enderton] p. 192Theorem 7M(c)onirri 4498
[Enderton] p. 193Corollary 7N(b)0elon 4444
[Enderton] p. 193Corollary 7N(c)onsuci 4628
[Enderton] p. 193Corollary 7N(d)ssonunii 4578
[Enderton] p. 194Remarkonprc 4575
[Enderton] p. 194Exercise 16suc11 4495
[Enderton] p. 197Definitiondf-card 7567
[Enderton] p. 197Theorem 7Pcarden 8168
[Enderton] p. 200Exercise 25tfis 4644
[Enderton] p. 202Lemma 7Tr1tr 7443
[Enderton] p. 202Definitiondf-r1 7431
[Enderton] p. 202Theorem 7Qr1val1 7453
[Enderton] p. 204Theorem 7V(b)rankval4 7534
[Enderton] p. 206Theorem 7X(b)en2lp 7312
[Enderton] p. 207Exercise 30rankpr 7524  rankprb 7518  rankpw 7510  rankpwi 7490  rankuniss 7533
[Enderton] p. 207Exercise 34opthreg 7314
[Enderton] p. 208Exercise 35suc11reg 7315
[Enderton] p. 212Definition of alephalephval3 7732
[Enderton] p. 213Theorem 8A(a)alephord2 7698
[Enderton] p. 213Theorem 8A(b)cardalephex 7712
[Enderton] p. 218Theorem Schema 8Eonfununi 6353
[Enderton] p. 222Definition of kardkarden 7560  kardex 7559
[Enderton] p. 238Theorem 8Roeoa 6590
[Enderton] p. 238Theorem 8Soeoe 6592
[Enderton] p. 240Exercise 25oarec 6555
[Enderton] p. 257Definition of cofinalitycflm 7871
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13538
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13484
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14274  mrieqv2d 13535  mrieqvd 13534
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13539
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13544  mreexexlem2d 13541
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14280  mreexfidimd 13546
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18888
[Fremlin5] p. 213Lemma 565Cauniioovol 18928
[Fremlin5] p. 214Lemma 565Cauniioombl 18938
[FreydScedrov] p. 283Axiom of Infinityax-inf 7334  inf1 7318  inf2 7319
[Gleason] p. 117Proposition 9-2.1df-enq 8530  enqer 8540
[Gleason] p. 117Proposition 9-2.2df-1nq 8535  df-nq 8531
[Gleason] p. 117Proposition 9-2.3df-plpq 8527  df-plq 8533
[Gleason] p. 119Proposition 9-2.4caovmo 6018  df-mpq 8528  df-mq 8534
[Gleason] p. 119Proposition 9-2.5df-rq 8536
[Gleason] p. 119Proposition 9-2.6ltexnq 8594
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8595  ltbtwnnq 8597
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8590
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8591
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8598
[Gleason] p. 121Definition 9-3.1df-np 8600
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8612
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8614
[Gleason] p. 122Definitiondf-1p 8601
[Gleason] p. 122Remark (1)prub 8613
[Gleason] p. 122Lemma 9-3.4prlem934 8652
[Gleason] p. 122Proposition 9-3.2df-ltp 8604
[Gleason] p. 122Proposition 9-3.3ltsopr 8651  psslinpr 8650  supexpr 8673  suplem1pr 8671  suplem2pr 8672
[Gleason] p. 123Proposition 9-3.5addclpr 8637  addclprlem1 8635  addclprlem2 8636  df-plp 8602
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8641
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8640
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8653
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8662  ltexprlem1 8655  ltexprlem2 8656  ltexprlem3 8657  ltexprlem4 8658  ltexprlem5 8659  ltexprlem6 8660  ltexprlem7 8661
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8664  ltaprlem 8663
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8665
[Gleason] p. 124Lemma 9-3.6prlem936 8666
[Gleason] p. 124Proposition 9-3.7df-mp 8603  mulclpr 8639  mulclprlem 8638  reclem2pr 8667
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8648
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8643
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8642
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8647
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8670  reclem3pr 8668  reclem4pr 8669
[Gleason] p. 126Proposition 9-4.1df-enr 8676  df-mpr 8675  df-plpr 8674  enrer 8685
[Gleason] p. 126Proposition 9-4.2df-0r 8681  df-1r 8682  df-nr 8677
[Gleason] p. 126Proposition 9-4.3df-mr 8679  df-plr 8678  negexsr 8719  recexsr 8724  recexsrlem 8720
[Gleason] p. 127Proposition 9-4.4df-ltr 8680
[Gleason] p. 130Proposition 10-1.3creui 9736  creur 9735  cru 9733
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8805  axcnre 8781
[Gleason] p. 132Definition 10-3.1crim 11594  crimd 11711  crimi 11672  crre 11593  crred 11710  crrei 11671
[Gleason] p. 132Definition 10-3.2remim 11596  remimd 11677
[Gleason] p. 133Definition 10.36absval2 11763  absval2d 11921  absval2i 11874
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11620  cjaddd 11699  cjaddi 11667
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11621  cjmuld 11700  cjmuli 11668
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11619  cjcjd 11678  cjcji 11650
[Gleason] p. 133Proposition 10-3.4(f)cjre 11618  cjreb 11602  cjrebd 11681  cjrebi 11653  cjred 11705  rere 11601  rereb 11599  rerebd 11680  rerebi 11652  rered 11703
[Gleason] p. 133Proposition 10-3.4(h)addcj 11627  addcjd 11691  addcji 11662
[Gleason] p. 133Proposition 10-3.7(a)absval 11717
[Gleason] p. 133Proposition 10-3.7(b)abscj 11758  abscjd 11926  abscji 11878
[Gleason] p. 133Proposition 10-3.7(c)abs00 11768  abs00d 11922  abs00i 11875  absne0d 11923
[Gleason] p. 133Proposition 10-3.7(d)releabs 11799  releabsd 11927  releabsi 11879
[Gleason] p. 133Proposition 10-3.7(f)absmul 11773  absmuld 11930  absmuli 11881
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11761  sqabsaddi 11882
[Gleason] p. 133Proposition 10-3.7(h)abstri 11808  abstrid 11932  abstrii 11885
[Gleason] p. 134Definition 10-4.1df-exp 11099  exp0 11102  expp1 11104  expp1d 11240
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20020  cxpaddd 20058  expadd 11138  expaddd 11241  expaddz 11140
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20029  cxpmuld 20075  expmul 11141  expmuld 11242  expmulz 11142
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20026  mulcxpd 20069  mulexp 11135  mulexpd 11254  mulexpz 11136
[Gleason] p. 140Exercise 1znnen 12485
[Gleason] p. 141Definition 11-2.1fzval 10778
[Gleason] p. 168Proposition 12-2.1(a)climadd 12099  rlimadd 12110  rlimdiv 12113
[Gleason] p. 168Proposition 12-2.1(b)climsub 12101  rlimsub 12111
[Gleason] p. 168Proposition 12-2.1(c)climmul 12100  rlimmul 12112
[Gleason] p. 171Corollary 12-2.2climmulc2 12104
[Gleason] p. 172Corollary 12-2.5climrecl 12051
[Gleason] p. 172Proposition 12-2.4(c)climabs 12071  climcj 12072  climim 12074  climre 12073  rlimabs 12076  rlimcj 12077  rlimim 12079  rlimre 12078
[Gleason] p. 173Definition 12-3.1df-ltxr 8867  df-xr 8866  ltxr 10452
[Gleason] p. 175Definition 12-4.1df-limsup 11939  limsupval 11942
[Gleason] p. 180Theorem 12-5.1climsup 12137
[Gleason] p. 180Theorem 12-5.3caucvg 12145  caucvgb 12146  caucvgr 12142  climcau 12138
[Gleason] p. 182Exercise 3cvgcmp 12268
[Gleason] p. 182Exercise 4cvgrat 12333
[Gleason] p. 195Theorem 13-2.12abs1m 11813
[Gleason] p. 217Lemma 13-4.1btwnzge0 10947
[Gleason] p. 223Definition 14-1.1df-met 16368
[Gleason] p. 223Definition 14-1.1(a)met0 17902  xmet0 17901
[Gleason] p. 223Definition 14-1.1(b)metgt0 17917
[Gleason] p. 223Definition 14-1.1(c)metsym 17908
[Gleason] p. 223Definition 14-1.1(d)mettri 17910  mstri 18009  xmettri 17909  xmstri 18008
[Gleason] p. 225Definition 14-1.5xpsmet 17940
[Gleason] p. 230Proposition 14-2.6txlm 17336
[Gleason] p. 240Theorem 14-4.3metcnp4 18729
[Gleason] p. 240Proposition 14-4.2metcnp3 18080
[Gleason] p. 243Proposition 14-4.16addcn 18363  addcn2 12061  mulcn 18365  mulcn2 12063  subcn 18364  subcn2 12062
[Gleason] p. 295Remarkbcval3 11313  bcval4 11314
[Gleason] p. 295Equation 2bcpasc 11327
[Gleason] p. 295Definition of binomial coefficientbcval 11311  df-bc 11310
[Gleason] p. 296Remarkbcn0 11317  bcnn 11318
[Gleason] p. 296Theorem 15-2.8binom 12282
[Gleason] p. 308Equation 2ef0 12366
[Gleason] p. 308Equation 3efcj 12367
[Gleason] p. 309Corollary 15-4.3efne0 12371
[Gleason] p. 309Corollary 15-4.4efexp 12375
[Gleason] p. 310Equation 14sinadd 12438
[Gleason] p. 310Equation 15cosadd 12439
[Gleason] p. 311Equation 17sincossq 12450
[Gleason] p. 311Equation 18cosbnd 12455  sinbnd 12454
[Gleason] p. 311Lemma 15-4.7sqeqor 11211  sqeqori 11209
[Gleason] p. 311Definition of pidf-pi 12348
[Godowski] p. 730Equation SFgoeqi 22845
[GodowskiGreechie] p. 249Equation IV3oai 22239
[Gratzer] p. 23Section 0.6df-mre 13482
[Gratzer] p. 27Section 0.6df-mri 13484
[Halmos] p. 31Theorem 17.3riesz1 22637  riesz2 22638
[Halmos] p. 41Definition of Hermitianhmopadj2 22513
[Halmos] p. 42Definition of projector orderingpjordi 22745
[Halmos] p. 43Theorem 26.1elpjhmop 22757  elpjidm 22756  pjnmopi 22720
[Halmos] p. 44Remarkpjinormi 22258  pjinormii 22247
[Halmos] p. 44Theorem 26.2elpjch 22761  pjrn 22278  pjrni 22273  pjvec 22267
[Halmos] p. 44Theorem 26.3pjnorm2 22298
[Halmos] p. 44Theorem 26.4hmopidmpj 22726  hmopidmpji 22724
[Halmos] p. 45Theorem 27.1pjinvari 22763
[Halmos] p. 45Theorem 27.3pjoci 22752  pjocvec 22268
[Halmos] p. 45Theorem 27.4pjorthcoi 22741
[Halmos] p. 48Theorem 29.2pjssposi 22744
[Halmos] p. 48Theorem 29.3pjssdif1i 22747  pjssdif2i 22746
[Halmos] p. 50Definition of spectrumdf-spec 22427
[Hamilton] p. 28Definition 2.1ax-1 7
[Hamilton] p. 31Example 2.7(a)id1 22
[Hamilton] p. 73Rule 1ax-mp 10
[Hamilton] p. 74Rule 2ax-gen 1538
[Hatcher] p. 25Definitiondf-phtpc 18484  df-phtpy 18463
[Hatcher] p. 26Definitiondf-pco 18497  df-pi1 18500
[Hatcher] p. 26Proposition 1.2phtpcer 18487
[Hatcher] p. 26Proposition 1.3pi1grp 18542
[Herstein] p. 54Exercise 28df-grpo 20850
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14492  grpoideu 20868  mndideu 14369
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14510  grpoinveu 20881
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14529  grpo2inv 20898
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14538  grpoinvop 20900
[Herstein] p. 57Exercise 1isgrp2d 20894  isgrp2i 20895
[Hitchcock] p. 5Rule A3mpto1 1528
[Hitchcock] p. 5Rule A4mpto2 1529
[Hitchcock] p. 5Rule A5mtp-xor 1530
[Holland] p. 1519Theorem 2sumdmdi 22992
[Holland] p. 1520Lemma 5cdj1i 23005  cdj3i 23013  cdj3lem1 23006  cdjreui 23004
[Holland] p. 1524Lemma 7mddmdin0i 23003
[Holland95] p. 13Theorem 3.6hlathil 31421
[Holland95] p. 14Line 15hgmapvs 31351
[Holland95] p. 14Line 16hdmaplkr 31373
[Holland95] p. 14Line 17hdmapellkr 31374
[Holland95] p. 14Line 19hdmapglnm2 31371
[Holland95] p. 14Line 20hdmapip0com 31377
[Holland95] p. 14Theorem 3.6hdmapevec2 31296
[Holland95] p. 14Lines 24 and 25hdmapoc 31391
[Holland95] p. 204Definition of involutiondf-srng 15605
[Holland95] p. 212Definition of subspacedf-psubsp 28959
[Holland95] p. 214Lemma 3.3lclkrlem2v 30985
[Holland95] p. 214Definition 3.2df-lpolN 30938
[Holland95] p. 214Definition of nonsingularpnonsingN 29389
[Holland95] p. 215Lemma 3.3(1)dihoml4 30834  poml4N 29409
[Holland95] p. 215Lemma 3.3(2)dochexmid 30925  pexmidALTN 29434  pexmidN 29425
[Holland95] p. 218Theorem 3.6lclkr 30990
[Holland95] p. 218Definition of dual vector spacedf-ldual 28581  ldualset 28582
[Holland95] p. 222Item 1df-lines 28957  df-pointsN 28958
[Holland95] p. 222Item 2df-polarityN 29359
[Holland95] p. 223Remarkispsubcl2N 29403  omllaw4 28703  pol1N 29366  polcon3N 29373
[Holland95] p. 223Definitiondf-psubclN 29391
[Holland95] p. 223Equation for polaritypolval2N 29362
[Hughes] p. 44Equation 1.21bax-his3 21655
[Hughes] p. 47Definition of projection operatordfpjop 22754
[Hughes] p. 49Equation 1.30eighmre 22535  eigre 22407  eigrei 22406
[Hughes] p. 49Equation 1.31eighmorth 22536  eigorth 22410  eigorthi 22409
[Hughes] p. 137Remark (ii)eigposi 22408
[Indrzejczak] p. 33Definition ` `Enatded 4  natded 4
[Indrzejczak] p. 33Definition ` `Inatded 4
[Indrzejczak] p. 34Definition ` `Enatded 4  natded 4
[Indrzejczak] p. 34Definition ` `Inatded 4
[Jech] p. 4Definition of classcv 1627  cvjust 2279
[Jech] p. 42Lemma 6.1alephexp1 8196
[Jech] p. 42Equation 6.1alephadd 8194  alephmul 8195
[Jech] p. 43Lemma 6.2infmap 8193  infmap2 7839
[Jech] p. 71Lemma 9.3jech9.3 7481
[Jech] p. 72Equation 9.3scott0 7551  scottex 7550
[Jech] p. 72Exercise 9.1rankval4 7534
[Jech] p. 72Scheme "Collection Principle"cp 7556
[Jech] p. 78Definition implied by the footnoteopthprc 4735
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26399
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26495
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26496
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26411
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26415
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26416  rmyp1 26417
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26418  rmym1 26419
[JonesMatijasevic] p. 695Equation 2.11rmx0 26409  rmx1 26410  rmxluc 26420
[JonesMatijasevic] p. 695Equation 2.12rmy0 26413  rmy1 26414  rmyluc 26421
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26423
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26424
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26446  jm2.17b 26447  jm2.17c 26448
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26485
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26489
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26480
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26449  jm2.24nn 26445
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26494
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26500  rmygeid 26450
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26512
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1641
[KalishMontague] p. 85Lemma 2equid 1649
[KalishMontague] p. 85Lemma 3equcomi 1650
[KalishMontague] p. 86Lemma 7cbvalivw 1647  cbvaliw 1646
[KalishMontague] p. 87Lemma 8spimvw 1645  spimw 1644
[KalishMontague] p. 87Lemma 9spfw 1661  spw 1664
[Kalmbach] p. 14Definition of latticechabs1 22087  chabs1i 22089  chabs2 22088  chabs2i 22090  chjass 22104  chjassi 22057  latabs1 14187  latabs2 14188
[Kalmbach] p. 15Definition of atomdf-at 22910  ela 22911
[Kalmbach] p. 15Definition of coverscvbr2 22855  cvrval2 28731
[Kalmbach] p. 16Definitiondf-ol 28635  df-oml 28636
[Kalmbach] p. 20Definition of commutescmbr 22155  cmbri 22161  cmtvalN 28668  df-cm 22154  df-cmtN 28634
[Kalmbach] p. 22Remarkomllaw5N 28704  pjoml5 22184  pjoml5i 22159
[Kalmbach] p. 22Definitionpjoml2 22182  pjoml2i 22156
[Kalmbach] p. 22Theorem 2(v)cmcm 22185  cmcmi 22163  cmcmii 22168  cmtcomN 28706
[Kalmbach] p. 22Theorem 2(ii)omllaw3 28702  omlsi 21975  pjoml 22007  pjomli 22006
[Kalmbach] p. 22Definition of OML lawomllaw2N 28701
[Kalmbach] p. 23Remarkcmbr2i 22167  cmcm3 22186  cmcm3i 22165  cmcm3ii 22170  cmcm4i 22166  cmt3N 28708  cmt4N 28709  cmtbr2N 28710
[Kalmbach] p. 23Lemma 3cmbr3 22179  cmbr3i 22171  cmtbr3N 28711
[Kalmbach] p. 25Theorem 5fh1 22189  fh1i 22192  fh2 22190  fh2i 22193  omlfh1N 28715
[Kalmbach] p. 65Remarkchjatom 22929  chslej 22069  chsleji 22029  shslej 21951  shsleji 21941
[Kalmbach] p. 65Proposition 1chocin 22066  chocini 22025  chsupcl 21911  chsupval2 21981  h0elch 21826  helch 21815  hsupval2 21980  ocin 21867  ococss 21864  shococss 21865
[Kalmbach] p. 65Definition of subspace sumshsval 21883
[Kalmbach] p. 66Remarkdf-pjh 21966  pjssmi 22737  pjssmii 22252
[Kalmbach] p. 67Lemma 3osum 22216  osumi 22213
[Kalmbach] p. 67Lemma 4pjci 22772
[Kalmbach] p. 103Exercise 6atmd2 22972
[Kalmbach] p. 103Exercise 12mdsl0 22882
[Kalmbach] p. 140Remarkhatomic 22932  hatomici 22931  hatomistici 22934
[Kalmbach] p. 140Proposition 1atlatmstc 28776
[Kalmbach] p. 140Proposition 1(i)atexch 22953  lsatexch 28500
[Kalmbach] p. 140Proposition 1(ii)chcv1 22927  cvlcvr1 28796  cvr1 28866
[Kalmbach] p. 140Proposition 1(iii)cvexch 22946  cvexchi 22941  cvrexch 28876
[Kalmbach] p. 149Remark 2chrelati 22936  hlrelat 28858  hlrelat5N 28857  lrelat 28471
[Kalmbach] p. 153Exercise 5lsmcv 15888  lsmsatcv 28467  spansncv 22224  spansncvi 22223
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 28486  spansncv2 22865
[Kalmbach] p. 266Definitiondf-st 22783
[Kalmbach2] p. 8Definition of adjointdf-adjh 22421
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8263  fpwwe2 8260
[KanamoriPincus] p. 416Corollary 1.3canth4 8264
[KanamoriPincus] p. 417Corollary 1.6canthp1 8271
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8266
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8268
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8281
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8285  gchxpidm 8286
[KanamoriPincus] p. 419Theorem 2.1gchacg 8289  gchhar 8288
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7837  unxpwdom 7298
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8291
[Kreyszig] p. 3Property M1metcl 17891  xmetcl 17890
[Kreyszig] p. 4Property M2meteq0 17898
[Kreyszig] p. 8Definition 1.1-8dscmet 18089
[Kreyszig] p. 12Equation 5conjmul 9472  muleqadd 9407
[Kreyszig] p. 18Definition 1.3-2mopnval 17978
[Kreyszig] p. 19Remarkmopntopon 17979
[Kreyszig] p. 19Theorem T1mopn0 18038  mopnm 17984
[Kreyszig] p. 19Theorem T2unimopn 18036
[Kreyszig] p. 19Definition of neighborhoodneibl 18041
[Kreyszig] p. 20Definition 1.3-3metcnp2 18082
[Kreyszig] p. 25Definition 1.4-1lmbr 16982  lmmbr 18678  lmmbr2 18679
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17102
[Kreyszig] p. 28Theorem 1.4-5lmcau 18732
[Kreyszig] p. 28Definition 1.4-3iscau 18696  iscmet2 18714
[Kreyszig] p. 30Theorem 1.4-7cmetss 18734
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17181  metelcls 18724
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18725  metcld2 18726
[Kreyszig] p. 51Equation 2clmvneg1 18583  lmodvneg1 15661  nvinv 21189  vcm 21119
[Kreyszig] p. 51Equation 1aclm0vs 18582  lmod0vs 15657  vc0 21117
[Kreyszig] p. 51Equation 1blmodvs0 15658  vcz 21118
[Kreyszig] p. 58Definition 2.2-1imsmet 21252
[Kreyszig] p. 59Equation 1imsdval 21247  imsdval2 21248
[Kreyszig] p. 63Problem 1nvnd 21249
[Kreyszig] p. 64Problem 2nvge0 21232  nvz 21227
[Kreyszig] p. 64Problem 3nvabs 21231
[Kreyszig] p. 91Definition 2.7-1isblo3i 21371
[Kreyszig] p. 92Equation 2df-nmoo 21315
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21377  blocni 21375
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21376
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18633  ipeq0 16536  ipz 21287
[Kreyszig] p. 135Problem 2pythi 21420
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21424
[Kreyszig] p. 144Equation 4supcvg 12308
[Kreyszig] p. 144Theorem 3.3-1minvec 18794  minveco 21455
[Kreyszig] p. 196Definition 3.9-1df-aj 21320
[Kreyszig] p. 247Theorem 4.7-2bcth 18745
[Kreyszig] p. 249Theorem 4.7-3ubth 21444
[Kreyszig] p. 470Definition of positive operator orderingleop 22695  leopg 22694
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22713
[Kreyszig] p. 525Theorem 10.1-1htth 21490
[Kunen] p. 10Axiom 0a9e 1894  axnul 4149
[Kunen] p. 11Axiom 3axnul 4149
[Kunen] p. 12Axiom 6zfrep6 5709
[Kunen] p. 24Definition 10.24mapval 6779  mapvalg 6777
[Kunen] p. 30Lemma 10.20fodom 8144
[Kunen] p. 31Definition 10.24mapex 6773
[Kunen] p. 95Definition 2.1df-r1 7431
[Kunen] p. 97Lemma 2.10r1elss 7473  r1elssi 7472
[Kunen] p. 107Exercise 4rankop 7525  rankopb 7519  rankuni 7530  rankxplim 7544  rankxpsuc 7547
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3916
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26950
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26945
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26951
[LeBlanc] p. 277Rule R2axnul 4149
[Levy] p. 338Axiomdf-clab 2271  df-clel 2280  df-cleq 2277
[Levy58] p. 2Definition Iisfin1-3 8007
[Levy58] p. 2Definition IIdf-fin2 7907
[Levy58] p. 2Definition Iadf-fin1a 7906
[Levy58] p. 2Definition IIIdf-fin3 7909
[Levy58] p. 3Definition Vdf-fin5 7910
[Levy58] p. 3Definition IVdf-fin4 7908
[Levy58] p. 4Definition VIdf-fin6 7911
[Levy58] p. 4Definition VIIdf-fin7 7912
[Levy58], p. 3Theorem 1fin1a2 8036
[Lopez-Astorga] p. 12Rule 1mpto1 1528
[Lopez-Astorga] p. 12Rule 2mpto2 1529
[Lopez-Astorga] p. 12Rule 3mtp-xor 1530
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 22980
[Maeda] p. 168Lemma 5mdsym 22984  mdsymi 22983
[Maeda] p. 168Lemma 4(i)mdsymlem4 22978  mdsymlem6 22980  mdsymlem7 22981
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22982
[MaedaMaeda] p. 1Remarkssdmd1 22885  ssdmd2 22886  ssmd1 22883  ssmd2 22884
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22881
[MaedaMaeda] p. 1Definition 1.1df-dmd 22853  df-md 22852  mdbr 22866
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22903  mdslj1i 22891  mdslj2i 22892  mdslle1i 22889  mdslle2i 22890  mdslmd1i 22901  mdslmd2i 22902
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22893  mdsl2bi 22895  mdsl2i 22894
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22907
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22904
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22905
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22882
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22887  mdsl3 22888
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22906
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23001
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28778  hlrelat1 28856
[MaedaMaeda] p. 31Lemma 7.5lcvexch 28496
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22908  cvmdi 22896  cvnbtwn4 22861  cvrnbtwn4 28736
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22909
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28797  cvp 22947  cvrp 28872  lcvp 28497
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22971
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22970
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28790  hlexch4N 28848
[MaedaMaeda] p. 34Exercise 7.1atabsi 22973
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28899
[MaedaMaeda] p. 61Definition 15.10psubN 29205  atpsubN 29209  df-pointsN 28958  pointpsubN 29207
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28960  pmap11 29218  pmaple 29217  pmapsub 29224  pmapval 29213
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29221  pmap1N 29223
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29226  pmapglb2N 29227  pmapglb2xN 29228  pmapglbx 29225
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 29308
[MaedaMaeda] p. 67Postulate PS1ps-1 28933
[MaedaMaeda] p. 68Lemma 16.2df-padd 29252  paddclN 29298  paddidm 29297
[MaedaMaeda] p. 68Condition PS2ps-2 28934
[MaedaMaeda] p. 68Equation 16.2.1paddass 29294
[MaedaMaeda] p. 69Lemma 16.4ps-1 28933
[MaedaMaeda] p. 69Theorem 16.4ps-2 28934
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14978  lsmmod2 14979  lssats 28469  shatomici 22930  shatomistici 22933  shmodi 21961  shmodsi 21960
[MaedaMaeda] p. 130Remark 29.6dmdmd 22872  mdsymlem7 22981
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22160
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22064
[MaedaMaeda] p. 139Remarksumdmdii 22987
[Margaris] p. 40Rule Cexlimiv 1670
[Margaris] p. 49Axiom A1ax-1 7
[Margaris] p. 49Axiom A2ax-2 8
[Margaris] p. 49Axiom A3ax-3 9
[Margaris] p. 49Definitiondf-an 362  df-ex 1534  df-or 361  dfbi2 612
[Margaris] p. 51Theorem 1id1 22
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 27959
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27960
[Margaris] p. 79Rule Cexinst01 27665  exinst11 27666
[Margaris] p. 89Theorem 19.219.2 1675  19.2g 1784  r19.2z 3544
[Margaris] p. 89Theorem 19.319.3 1785  19.3v 1666  rr19.3v 2910
[Margaris] p. 89Theorem 19.5alcom 1715
[Margaris] p. 89Theorem 19.6alex 1564
[Margaris] p. 89Theorem 19.7alnex 1535
[Margaris] p. 89Theorem 19.819.8a 1722
[Margaris] p. 89Theorem 19.919.9 1787  19.9h 1731  19.9v 1667
[Margaris] p. 89Theorem 19.11excom 1790  excomim 1789
[Margaris] p. 89Theorem 19.1219.12 1738  r19.12 2657
[Margaris] p. 90Theorem 19.14exnal 1566
[Margaris] p. 90Theorem 19.152albi 26975  albi 1556  ralbi 2680
[Margaris] p. 90Theorem 19.1619.16 1791
[Margaris] p. 90Theorem 19.1719.17 1792
[Margaris] p. 90Theorem 19.182exbi 26977  exbi 1573
[Margaris] p. 90Theorem 19.1919.19 1793
[Margaris] p. 90Theorem 19.202alim 26974  alim 1550  alimd 1748  alimdh 1555  alimdv 1612  ralimdaa 2621  ralimdv 2623  ralimdva 2622  sbcimdv 3053
[Margaris] p. 90Theorem 19.2119.21-2 1796  19.21 1795  19.21bi 1798  19.21h 1735  19.21t 1794  19.21v 1842  19.21vv 26973  alrimd 1753  alrimdd 1752  alrimdh 1579  alrimdv 1624  alrimi 1749  alrimih 1557  alrimiv 1622  alrimivv 1623  r19.21 2630  r19.21be 2645  r19.21bi 2642  r19.21t 2629  r19.21v 2631  ralrimd 2632  ralrimdv 2633  ralrimdva 2634  ralrimdvv 2638  ralrimdvva 2639  ralrimi 2625  ralrimiv 2626  ralrimiva 2627  ralrimivv 2635  ralrimivva 2636  ralrimivvva 2637  ralrimivw 2628  rexlimi 2661
[Margaris] p. 90Theorem 19.222alimdv 1614  2exim 26976  2eximdv 1615  exim 1567  eximd 1754  eximdh 1580  eximdv 1613  rexim 2648  reximdai 2652  reximddv 23020  reximdv 2655  reximdv2 2653  reximdva 2656  reximdvai 2654  reximi2 2650
[Margaris] p. 90Theorem 19.2319.23 1801  19.23bi 1806  19.23h 1732  19.23t 1800  19.23v 1843  19.23vv 1844  exlimd 1807  exlimdh 1808  exlimdv 1668  exlimdvv 1672  exlimexi 27558  exlimi 1805  exlimih 1733  exlimiv 1670  exlimivv 1671  r19.23 2659  r19.23v 2660  rexlimd 2665  rexlimdv 2667  rexlimdv3a 2670  rexlimdva 2668  rexlimdvaa 2669  rexlimdvv 2674  rexlimdvva 2675  rexlimdvw 2671  rexlimiv 2662  rexlimiva 2663  rexlimivv 2673
[Margaris] p. 90Theorem 19.2419.24 1677
[Margaris] p. 90Theorem 19.2519.25 1595
[Margaris] p. 90Theorem 19.2619.26-2 1586  19.26-3an 1587  19.26 1585  r19.26-2 2677  r19.26-2a 24332  r19.26-3 2678  r19.26 2676  r19.26m 2679
[Margaris] p. 90Theorem 19.2719.27 1809  19.27v 1846  r19.27av 2682  r19.27z 3553  r19.27zv 3554
[Margaris] p. 90Theorem 19.2819.28 1810  19.28v 1847  19.28vv 26983  r19.28av 2683  r19.28z 3547  r19.28zv 3550  rr19.28v 2911
[Margaris] p. 90Theorem 19.2919.29 1588  19.29r 1589  19.29r2 1590  19.29x 1591  r19.29 2684  r19.29r 2685
[Margaris] p. 90Theorem 19.3019.30 1596  r19.30 2686
[Margaris] p. 90Theorem 19.3119.31 1816  19.31vv 26981
[Margaris] p. 90Theorem 19.3219.32 1815  r19.32 27324  r19.32v 2687
[Margaris] p. 90Theorem 19.3319.33-2 26979  19.33 1599  19.33b 1600
[Margaris] p. 90Theorem 19.3419.34 1678
[Margaris] p. 90Theorem 19.3519.35 1592  19.35i 1593  19.35ri 1594  r19.35 2688
[Margaris] p. 90Theorem 19.3619.36 1811  19.36aiv 1849  19.36i 1812  19.36v 1848  19.36vv 26980  r19.36av 2689  r19.36zv 3555
[Margaris] p. 90Theorem 19.3719.37 1813  19.37aiv 1852  19.37v 1851  19.37vv 26982  r19.37 2690  r19.37av 2691  r19.37zv 3551
[Margaris] p. 90Theorem 19.3819.38 1814
[Margaris] p. 90Theorem 19.3919.39 1676
[Margaris] p. 90Theorem 19.4019.40-2 1602  19.40 1601  r19.40 2692
[Margaris] p. 90Theorem 19.4119.41 1819  19.41rg 27587  19.41v 1853  19.41vv 1854  19.41vvv 1855  19.41vvvv 1856  r19.41 2693  r19.41v 2694
[Margaris] p. 90Theorem 19.4219.42 1820  19.42v 1857  19.42vv 1859  19.42vvv 1860  r19.42v 2695
[Margaris] p. 90Theorem 19.4319.43 1597  r19.43 2696
[Margaris] p. 90Theorem 19.4419.44 1817  r19.44av 2697
[Margaris] p. 90Theorem 19.4519.45 1818  r19.45av 2698  r19.45zv 3552
[Margaris] p. 110Exercise 2(b)eu1 2165
[Mayet] p. 370Remarkjpi 22842  largei 22839  stri 22829
[Mayet3] p. 9Definition of CH-statesdf-hst 22784  ishst 22786
[Mayet3] p. 10Theoremhstrbi 22838  hstri 22837
[Mayet3] p. 1223Theorem 4.1mayete3i 22299
[Mayet3] p. 1240Theorem 7.1mayetes3i 22301
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22850
[MegPav2000] p. 2345Definition 3.4-1chintcl 21903  chsupcl 21911
[MegPav2000] p. 2345Definition 3.4-2hatomic 22932
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22926
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22953
[MegPav2000] p. 2366Figure 7pl42N 29439
[MegPav2002] p. 362Lemma 2.2latj31 14199  latj32 14197  latjass 14195
[Megill] p. 444Axiom C5ax-17 1608
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 2093  alequcom 1889  ax-10 2083
[Megill] p. 446Lemma L17equtrr 1657
[Megill] p. 446Lemma L18ax9from9o 2090
[Megill] p. 446Lemma L19hbnae-o 2120  hbnae 1899
[Megill] p. 447Remark 9.1df-sb 1636  sbid 1836  sbidd-misc 27449  sbidd 27448
[Megill] p. 448Remark 9.6ax15 2077
[Megill] p. 448Scheme C4'ax-5o 2079
[Megill] p. 448Scheme C5'ax-4 2078
[Megill] p. 448Scheme C6'ax-7 1712
[Megill] p. 448Scheme C7'ax-6o 2080
[Megill] p. 448Scheme C8'ax-8 1648
[Megill] p. 448Scheme C9'ax-12o 2085
[Megill] p. 448Scheme C10'ax-9 1641  ax-9o 2081
[Megill] p. 448Scheme C11'ax-10o 2082
[Megill] p. 448Scheme C12'ax-13 1690
[Megill] p. 448Scheme C13'ax-14 1692
[Megill] p. 448Scheme C14'ax-15 2086
[Megill] p. 448Scheme C15'ax-11o 2084
[Megill] p. 448Scheme C16'ax-16 2087
[Megill] p. 448Theorem 9.4dral1-o 2096  dral1 1908  dral2-o 2122  dral2 1909  drex1 1910  drex2 1911  drsb1 1932  drsb2 1975
[Megill] p. 448Theorem 9.7conventions 3
[Megill] p. 449Theorem 9.7sbcom2 2051  sbequ 1974  sbid2v 2060
[Megill] p. 450Example in Appendixhba1-o 2091  hba1 1723
[Mendelson] p. 35Axiom A3hirstL-ax3 27239
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4rspsbc 3070  rspsbca 3071  stdpc4 1934
[Mendelson] p. 69Axiom 5ax-5o 2079  ra5 3076  stdpc5 1797
[Mendelson] p. 81Rule Cexlimiv 1670
[Mendelson] p. 95Axiom 6stdpc6 1654
[Mendelson] p. 95Axiom 7stdpc7 1660
[Mendelson] p. 225Axiom system NBGru 2991
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4267
[Mendelson] p. 231Exercise 4.10(k)inv1 3482
[Mendelson] p. 231Exercise 4.10(l)unv 3483
[Mendelson] p. 231Exercise 4.10(n)dfin3 3409
[Mendelson] p. 231Exercise 4.10(o)df-nul 3457
[Mendelson] p. 231Exercise 4.10(q)dfin4 3410
[Mendelson] p. 231Exercise 4.10(s)ddif 3309
[Mendelson] p. 231Definition of uniondfun3 3408
[Mendelson] p. 235Exercise 4.12(c)univ 4564
[Mendelson] p. 235Exercise 4.12(d)pwv 3827
[Mendelson] p. 235Exercise 4.12(j)pwin 4296
[Mendelson] p. 235Exercise 4.12(k)pwunss 4297
[Mendelson] p. 235Exercise 4.12(l)pwssun 4298
[Mendelson] p. 235Exercise 4.12(n)uniin 3848
[Mendelson] p. 235Exercise 4.12(p)reli 4812
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5191
[Mendelson] p. 244Proposition 4.8(g)epweon 4574
[Mendelson] p. 246Definition of successordf-suc 4397
[Mendelson] p. 250Exercise 4.36oelim2 6588
[Mendelson] p. 254Proposition 4.22(b)xpen 7019
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6941  xpsneng 6942
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6948  xpcomeng 6949
[Mendelson] p. 254Proposition 4.22(e)xpassen 6951
[Mendelson] p. 255Definitionbrsdom 6879
[Mendelson] p. 255Exercise 4.39endisj 6944
[Mendelson] p. 255Exercise 4.41mapprc 6771
[Mendelson] p. 255Exercise 4.43mapsnen 6933
[Mendelson] p. 255Exercise 4.45mapunen 7025
[Mendelson] p. 255Exercise 4.47xpmapen 7024
[Mendelson] p. 255Exercise 4.42(a)map0e 6800
[Mendelson] p. 255Exercise 4.42(b)map1 6934
[Mendelson] p. 257Proposition 4.24(a)undom 6945
[Mendelson] p. 258Exercise 4.56(b)cdaen 7794
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7803  cdacomen 7802
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7807
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7801
[Mendelson] p. 258Definition of cardinal sumcdaval 7791  df-cda 7789
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6525
[Mendelson] p. 266Proposition 4.34(f)oaordex 6551
[Mendelson] p. 275Proposition 4.42(d)entri3 8176
[Mendelson] p. 281Definitiondf-r1 7431
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7480
[Mendelson] p. 287Axiom system MKru 2991
[Mittelstaedt] p. 9Definitiondf-oc 21823
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3392
[Monk1] p. 33Theorem 3.2(i)ssrel 4775
[Monk1] p. 33Theorem 3.2(ii)eqrel 4776
[Monk1] p. 34Definition 3.3df-opab 4079
[Monk1] p. 36Theorem 3.7(i)coi1 5186  coi2 5187
[Monk1] p. 36Theorem 3.8(v)dm0 4891  rn0 4935
[Monk1] p. 36Theorem 3.7(ii)cnvi 5084
[Monk1] p. 37Theorem 3.13(i)relxp 4793
[Monk1] p. 37Theorem 3.13(x)dmxp 4896  rnxp 5105
[Monk1] p. 37Theorem 3.13(ii)xp0 5097  xp0r 4767
[Monk1] p. 38Theorem 3.16(ii)ima0 5029
[Monk1] p. 38Theorem 3.16(viii)imai 5026
[Monk1] p. 39Theorem 3.17imaexg 5025
[Monk1] p. 39Theorem 3.16(xi)imassrn 5024
[Monk1] p. 41Theorem 4.3(i)fnopfv 5621  funfvop 5598
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5527
[Monk1] p. 42Theorem 4.4(iii)fvelima 5535
[Monk1] p. 43Theorem 4.6funun 5261
[Monk1] p. 43Theorem 4.8(iv)dff13 5744  dff13f 5745
[Monk1] p. 46Theorem 4.15(v)funex 5704  funrnex 5708
[Monk1] p. 50Definition 5.4fniunfv 5734
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5154
[Monk1] p. 52Theorem 5.11(viii)ssint 3879
[Monk1] p. 52Definition 5.13 (i)1stval2 6098  df-1st 6083
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6099  df-2nd 6084
[Monk1] p. 112Theorem 15.17(v)ranksn 7521  ranksnb 7494
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7522
[Monk1] p. 112Theorem 15.17(iii)rankun 7523  rankunb 7517
[Monk1] p. 113Theorem 15.18r1val3 7505
[Monk1] p. 113Definition 15.19df-r1 7431  r1val2 7504
[Monk1] p. 117Lemmazorn2 8128  zorn2g 8125
[Monk1] p. 133Theorem 18.11cardom 7614
[Monk1] p. 133Theorem 18.12canth3 8178
[Monk1] p. 133Theorem 18.14carduni 7609
[Monk2] p. 105Axiom C4ax-5 1549
[Monk2] p. 105Axiom C7ax-8 1648
[Monk2] p. 105Axiom C8ax-11 1719  ax-11o 2084
[Monk2] p. 105Axiom (C8)ax11v 2014
[Monk2] p. 108Lemma 5ax-5o 2079
[Monk2] p. 109Lemma 12ax-7 1712
[Monk2] p. 109Lemma 15equvin 2021  equvini 1930  eqvinop 4250
[Monk2] p. 113Axiom C5-1ax-17 1608
[Monk2] p. 113Axiom C5-2ax-6 1707
[Monk2] p. 113Axiom C5-3ax-7 1712
[Monk2] p. 114Lemma 21ax4 1720
[Monk2] p. 114Lemma 22ax5o 1721  hba1-o 2091  hba1 1723
[Monk2] p. 114Lemma 23nfia1 1782
[Monk2] p. 114Lemma 24nfa2 1781  nfra2 2598
[Moore] p. 53Part Idf-mre 13482
[Munkres] p. 77Example 2distop 16727  indistop 16733  indistopon 16732
[Munkres] p. 77Example 3fctop 16735  fctop2 16736
[Munkres] p. 77Example 4cctop 16737
[Munkres] p. 78Definition of basisdf-bases 16632  isbasis3g 16681
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13338  tgval2 16688
[Munkres] p. 79Remarktgcl 16701
[Munkres] p. 80Lemma 2.1tgval3 16695
[Munkres] p. 80Lemma 2.2tgss2 16719  tgss3 16718
[Munkres] p. 81Lemma 2.3basgen 16720  basgen2 16721
[Munkres] p. 89Definition of subspace topologyresttop 16885
[Munkres] p. 93Theorem 6.1(1)0cld 16769  topcld 16766
[Munkres] p. 93Theorem 6.1(2)iincld 16770
[Munkres] p. 93Theorem 6.1(3)uncld 16772
[Munkres] p. 94Definition of closureclsval 16768
[Munkres] p. 94Definition of interiorntrval 16767
[Munkres] p. 95Theorem 6.5(a)clsndisj 16806  elcls 16804
[Munkres] p. 95Theorem 6.5(b)elcls3 16814
[Munkres] p. 97Theorem 6.6clslp 16873  neindisj 16848
[Munkres] p. 97Corollary 6.7cldlp 16875
[Munkres] p. 97Definition of limit pointislp2 16871  lpval 16865
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17037
[Munkres] p. 102Definition of continuous functiondf-cn 16951  iscn 16959  iscn2 16962
[Munkres] p. 107Theorem 7.2(g)cncnp 17003  cncnp2 17004  cncnpi 17001  df-cnp 16952  iscnp 16961  iscnp2 16963
[Munkres] p. 127Theorem 10.1metcn 18083
[Munkres] p. 128Theorem 10.3metcn4 18730
[NielsenChuang] p. 195Equation 4.73unierri 22676
[Pfenning] p. 17Definition XMnatded 4  natded 4
[Pfenning] p. 17Definition NNCnatded 4  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 4
[Pfenning] p. 18Rule"natded 4
[Pfenning] p. 18Definition /\Inatded 4
[Pfenning] p. 18Definition ` `Enatded 4  natded 4  natded 4  natded 4  natded 4
[Pfenning] p. 18Definition ` `Inatded 4  natded 4  natded 4  natded 4  natded 4
[Pfenning] p. 18Definition ` `ELnatded 4
[Pfenning] p. 18Definition ` `ERnatded 4
[Pfenning] p. 18Definition ` `Ea,unatded 4
[Pfenning] p. 18Definition ` `IRnatded 4
[Pfenning] p. 18Definition ` `Ianatded 4
[Pfenning] p. 127Definition =Enatded 4
[Pfenning] p. 127Definition =Inatded 4
[Ponnusamy] p. 361Theorem 6.44cphip0l 18631  df-dip 21266  dip0l 21286  ip0l 16534
[Ponnusamy] p. 361Equation 6.45ipval 21268
[Ponnusamy] p. 362Equation I1dipcj 21282
[Ponnusamy] p. 362Equation I3cphdir 18634  dipdir 21412  ipdir 16537  ipdiri 21400
[Ponnusamy] p. 362Equation I4ipidsq 21278
[Ponnusamy] p. 362Equation 6.46ip0i 21395
[Ponnusamy] p. 362Equation 6.47ip1i 21397
[Ponnusamy] p. 362Equation 6.48ip2i 21398
[Ponnusamy] p. 363Equation I2cphass 18640  dipass 21415  ipass 16543  ipassi 21411
[Prugovecki] p. 186Definition of brabraval 22516  df-bra 22422
[Prugovecki] p. 376Equation 8.1df-kb 22423  kbval 22526
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22954
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 29344
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22968  atcvat4i 22969  cvrat3 28898  cvrat4 28899  lsatcvat3 28509
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22854  cvrval 28726  df-cv 22851  df-lcv 28476  lspsncv0 15893
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 29356
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 29357
[Quine] p. 16Definition 2.1df-clab 2271  rabid 2717
[Quine] p. 17Definition 2.1''dfsb7 2056
[Quine] p. 18Definition 2.7df-cleq 2277
[Quine] p. 19Definition 2.9conventions 3  df-v 2791
[Quine] p. 34Theorem 5.1abeq2 2389
[Quine] p. 35Theorem 5.2abid2 2401  abid2f 2445
[Quine] p. 40Theorem 6.1sb5 2017
[Quine] p. 40Theorem 6.2sb56 2015  sb6 2016
[Quine] p. 41Theorem 6.3df-clel 2280
[Quine] p. 41Theorem 6.4eqid 2284  eqid1 20832
[Quine] p. 41Theorem 6.5eqcom 2286
[Quine] p. 42Theorem 6.6df-sbc 2993
[Quine] p. 42Theorem 6.7dfsbcq 2994  dfsbcq2 2995
[Quine] p. 43Theorem 6.8vex 2792
[Quine] p. 43Theorem 6.9isset 2793
[Quine] p. 44Theorem 7.3spcgf 2864  spcgv 2869  spcimgf 2862
[Quine] p. 44Theorem 6.11spsbc 3004  spsbcd 3005
[Quine] p. 44Theorem 6.12elex 2797
[Quine] p. 44Theorem 6.13elab 2915  elabg 2916  elabgf 2913
[Quine] p. 44Theorem 6.14noel 3460
[Quine] p. 48Theorem 7.2snprc 3696
[Quine] p. 48Definition 7.1df-pr 3648  df-sn 3647
[Quine] p. 49Theorem 7.4snss 3749  snssg 3755
[Quine] p. 49Theorem 7.5prss 3770  prssg 3771
[Quine] p. 49Theorem 7.6prid1 3735  prid1g 3733  prid2 3736  prid2g 3734  snid 3668  snidg 3666
[Quine] p. 51Theorem 7.13prex 4216  snex 4215  snexALT 4195
[Quine] p. 53Theorem 8.2unisn 3844  unisnALT 27970  unisng 3845
[Quine] p. 53Theorem 8.3uniun 3847
[Quine] p. 54Theorem 8.6elssuni 3856
[Quine] p. 54Theorem 8.7uni0 3855
[Quine] p. 56Theorem 8.17uniabio 6262
[Quine] p. 56Definition 8.18dfiota2 6253
[Quine] p. 57Theorem 8.19iotaval 6263
[Quine] p. 57Theorem 8.22iotanul 6267
[Quine] p. 58Theorem 8.23iotaex 6269
[Quine] p. 58Definition 9.1df-op 3650
[Quine] p. 61Theorem 9.5opabid 4270  opelopab 4285  opelopaba 4280  opelopabaf 4287  opelopabf 4288  opelopabg 4282  opelopabga 4277  oprabid 5843
[Quine] p. 64Definition 9.11df-xp 4694
[Quine] p. 64Definition 9.12df-cnv 4696
[Quine] p. 64Definition 9.15df-id 4308
[Quine] p. 65Theorem 10.3fun0 5272
[Quine] p. 65Theorem 10.4funi 5250
[Quine] p. 65Theorem 10.5funsn 5265  funsng 5263
[Quine] p. 65Definition 10.1df-fun 5223
[Quine] p. 65Definition 10.2args 5040  df-fv 5229
[Quine] p. 68Definition 10.11conventions 3  df-fv 5229  fv2 5481
[Quine] p. 124Theorem 17.3nn0opth2 11281  nn0opth2i 11280  nn0opthi 11279  omopthi 6650
[Quine] p. 177Definition 25.2df-rdg 6418
[Quine] p. 232Equation icarddom 8171
[Quine] p. 284Axiom 39(vi)funimaex 5295  funimaexg 5294
[Quine] p. 331Axiom system NFru 2991
[ReedSimon] p. 36Definition (iii)ax-his3 21655
[ReedSimon] p. 63Exercise 4(a)df-dip 21266  polid 21730  polid2i 21728  polidi 21729
[ReedSimon] p. 63Exercise 4(b)df-ph 21383
[ReedSimon] p. 195Remarklnophm 22591  lnophmi 22590
[Retherford] p. 49Exercise 1(i)leopadd 22704
[Retherford] p. 49Exercise 1(ii)leopmul 22706  leopmuli 22705
[Retherford] p. 49Exercise 1(iv)leoptr 22709
[Retherford] p. 49Definition VI.1df-leop 22424  leoppos 22698
[Retherford] p. 49Exercise 1(iii)leoptri 22708
[Retherford] p. 49Definition of operator orderingleop3 22697
[Rudin] p. 164Equation 27efcan 12370
[Rudin] p. 164Equation 30efzval 12376
[Rudin] p. 167Equation 48absefi 12470
[Sanford] p. 39Rule 3mtp-xor 1530
[Sanford] p. 39Rule 4mpto2 1529
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 10
[Sanford] p. 39Rule says, "if ` ` is not true, and ` ` implies ` ` , then ` ` must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" mto 169
[Sanford] p. 40Rule 1mpto1 1528
[Schechter] p. 51Definition of antisymmetryintasym 5057
[Schechter] p. 51Definition of irreflexivityintirr 5060
[Schechter] p. 51Definition of symmetrycnvsym 5056
[Schechter] p. 51Definition of transitivitycotr 5054
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13482
[Schechter] p. 79Definition of Moore closuredf-mrc 13483
[Schechter] p. 82Section 4.5df-mrc 13483
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13485
[Schechter] p. 139Definition AC3dfac9 7757
[Schechter] p. 141Definition (MC)dfac11 26559
[Schechter] p. 149Axiom DC1ax-dc 8067  axdc3 8075
[Schechter] p. 187Definition of ring with unitisrng 15339  isrngo 21037
[Schechter] p. 276Remark 11.6.espan0 22113
[Schechter] p. 276Definition of spandf-span 21880  spanval 21904
[Schechter] p. 428Definition 15.35bastop1 16725
[Schwabhauser] p. 10Axiom A1axcgrrflx 23949
[Schwabhauser] p. 10Axiom A2axcgrtr 23950
[Schwabhauser] p. 10Axiom A3axcgrid 23951
[Schwabhauser] p. 11Axiom A4axsegcon 23962
[Schwabhauser] p. 11Axiom A5ax5seg 23973
[Schwabhauser] p. 11Axiom A6axbtwnid 23974
[Schwabhauser] p. 12Axiom A7axpasch 23976
[Schwabhauser] p. 12Axiom A8axlowdim2 23995
[Schwabhauser] p. 13Axiom A10axeuclid 23998
[Schwabhauser] p. 13Axiom A11axcont 24011
[Schwabhauser] p. 27Theorem 2.1cgrrflx 24017
[Schwabhauser] p. 27Theorem 2.2cgrcomim 24019
[Schwabhauser] p. 27Theorem 2.3cgrtr 24022
[Schwabhauser] p. 27Theorem 2.4cgrcoml 24026
[Schwabhauser] p. 27Theorem 2.5cgrcomr 24027
[Schwabhauser] p. 28Theorem 2.8cgrtriv 24032
[Schwabhauser] p. 28Theorem 2.105segofs 24036
[Schwabhauser] p. 28Definition 2.10df-ofs 24013
[Schwabhauser] p. 29Theorem 2.11cgrextend 24038
[Schwabhauser] p. 29Theorem 2.12segconeq 24040
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 24052  btwntriv2 24042
[Schwabhauser] p. 30Theorem 3.2btwncomim 24043
[Schwabhauser] p. 30Theorem 3.3btwntriv1 24046
[Schwabhauser] p. 30Theorem 3.4btwnswapid 24047
[Schwabhauser] p. 30Theorem 3.5btwnexch2 24053  btwnintr 24049
[Schwabhauser] p. 30Theorem 3.6btwnexch 24055  btwnexch3 24050
[Schwabhauser] p. 30Theorem 3.7btwnouttr 24054
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23994
[Schwabhauser] p. 32Theorem 3.14btwndiff 24057
[Schwabhauser] p. 33Theorem 3.17trisegint 24058
[Schwabhauser] p. 34Theorem 4.2ifscgr 24074
[Schwabhauser] p. 34Definition 4.1df-ifs 24069
[Schwabhauser] p. 35Theorem 4.3cgrsub 24075
[Schwabhauser] p. 35Theorem 4.5cgrxfr 24085
[Schwabhauser] p. 35Definition 4.4df-cgr3 24070
[Schwabhauser] p. 36Theorem 4.6btwnxfr 24086
[Schwabhauser] p. 36Theorem 4.11colinearperm1 24092  colinearperm2 24094  colinearperm3 24093  colinearperm4 24095  colinearperm5 24096
[Schwabhauser] p. 36Definition 4.10df-colinear 24071
[Schwabhauser] p. 37Theorem 4.12colineartriv1 24097
[Schwabhauser] p. 37Theorem 4.13colinearxfr 24105
[Schwabhauser] p. 37Theorem 4.14lineext 24106
[Schwabhauser] p. 37Theorem 4.16fscgr 24110
[Schwabhauser] p. 37Theorem 4.17linecgr 24111
[Schwabhauser] p. 37Definition 4.15df-fs 24072
[Schwabhauser] p. 38Theorem 4.18lineid 24113
[Schwabhauser] p. 38Theorem 4.19idinside 24114
[Schwabhauser] p. 39Theorem 5.1btwnconn1 24131
[Schwabhauser] p. 41Theorem 5.2btwnconn2 24132
[Schwabhauser] p. 41Theorem 5.3btwnconn3 24133
[Schwabhauser] p. 41Theorem 5.5brsegle2 24139
[Schwabhauser] p. 41Definition 5.4df-segle 24137
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 24140
[Schwabhauser] p. 42Theorem 5.7seglerflx 24142
[Schwabhauser] p. 42Theorem 5.8segletr 24144
[Schwabhauser] p. 42Theorem 5.9segleantisym 24145
[Schwabhauser] p. 42Theorem 5.10seglelin 24146
[Schwabhauser] p. 42Theorem 5.11seglemin 24143
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 24148
[Schwabhauser] p. 43Theorem 6.2btwnoutside 24155
[Schwabhauser] p. 43Theorem 6.3broutsideof3 24156
[Schwabhauser] p. 43Theorem 6.4broutsideof 24151  df-outsideof 24150
[Schwabhauser] p. 43Definition 6.1broutsideof2 24152
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 24157
[Schwabhauser] p. 44Theorem 6.6outsideofcom 24158
[Schwabhauser] p. 44Theorem 6.7outsideoftr 24159
[Schwabhauser] p. 44Theorem 6.11outsideofeu 24161
[Schwabhauser] p. 44Definition 6.8df-ray 24168
[Schwabhauser] p. 45Part 2df-lines2 24169
[Schwabhauser] p. 45Theorem 6.13outsidele 24162
[Schwabhauser] p. 45Theorem 6.15lineunray 24177
[Schwabhauser] p. 45Theorem 6.16lineelsb2 24178
[Schwabhauser] p. 45Theorem 6.17linecom 24180  linerflx1 24179  linerflx2 24181
[Schwabhauser] p. 45Theorem 6.18linethru 24183
[Schwabhauser] p. 45Definition 6.14df-line2 24167
[Schwabhauser] p. 46Theorem 6.19linethrueu 24186
[Schwabhauser] p. 46Theorem 6.21lineintmo 24187
[Shapiro] p. 230Theorem 6.5.1dchrhash 20504  dchrsum 20502  dchrsum2 20501  sumdchr 20505
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20506  sum2dchr 20507
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15295  ablfacrp2 15296
[Shapiro], p. 328Equation 9.2.4vmasum 20449
[Shapiro], p. 329Equation 9.2.7logfac2 20450
[Shapiro], p. 329Equation 9.2.9logfacrlim 20457
[Shapiro], p. 331Equation 9.2.13vmadivsum 20625
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20628
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20682  vmalogdivsum2 20681
[Shapiro], p. 375Theorem 9.4.1dirith 20672  dirith2 20671
[Shapiro], p. 375Equation 9.4.3rplogsum 20670  rpvmasum 20669  rpvmasum2 20655
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20630
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20668
[Shapiro], p. 377Lemma 9.4.1dchrisum 20635  dchrisumlem1 20632  dchrisumlem2 20633  dchrisumlem3 20634  dchrisumlema 20631
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20638
[Shapiro], p. 379Equation 9.4.16dchrmusum 20667  dchrmusumlem 20665  dchrvmasumlem 20666
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20637
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20639
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20663  dchrisum0re 20656  dchrisumn0 20664
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20649
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20653
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20654
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20709  pntrsumbnd2 20710  pntrsumo1 20708
[Shapiro], p. 405Equation 10.2.1mudivsum 20673
[Shapiro], p. 406Equation 10.2.6mulogsum 20675
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20677
[Shapiro], p. 407Equation 10.2.8mulog2sum 20680
[Shapiro], p. 418Equation 10.4.6logsqvma 20685
[Shapiro], p. 418Equation 10.4.8logsqvma2 20686
[Shapiro], p. 419Equation 10.4.10selberg 20691
[Shapiro], p. 420Equation 10.4.12selberg2lem 20693
[Shapiro], p. 420Equation 10.4.14selberg2 20694
[Shapiro], p. 422Equation 10.6.7selberg3 20702
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20703
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20700  selberg3lem2 20701
[Shapiro], p. 422Equation 10.4.23selberg4 20704
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20698
[Shapiro], p. 428Equation 10.6.2selbergr 20711
[Shapiro], p. 429Equation 10.6.8selberg3r 20712
[Shapiro], p. 430Equation 10.6.11selberg4r 20713
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20727
[Shapiro], p. 434Equation 10.6.27pntlema 20739  pntlemb 20740  pntlemc 20738  pntlemd 20737  pntlemg 20741
[Shapiro], p. 435Equation 10.6.29pntlema 20739
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20731
[Shapiro], p. 436Lemma 10.6.2pntibnd 20736
[Shapiro], p. 436Equation 10.6.34pntlema 20739
[Shapiro], p. 436Equation 10.6.35pntlem3 20752  pntleml 20754
[Stoll] p. 13Definition of symmetric differencesymdif1 3434
[Stoll] p. 16Exercise 4.40dif 3526  dif0 3525
[Stoll] p. 16Exercise 4.8difdifdir 3542
[Stoll] p. 17Theorem 5.1(5)undifv 3529
[Stoll] p. 19Theorem 5.2(13)undm 3427
[Stoll] p. 19Theorem 5.2(13')indm 3428
[Stoll] p. 20Remarkinvdif 3411
[Stoll] p. 25Definition of ordered tripledf-ot 3651
[Stoll] p. 43Definitionuniiun 3956
[Stoll] p. 44Definitionintiin 3957
[Stoll] p. 45Definitiondf-iin 3909
[Stoll] p. 45Definition indexed uniondf-iun 3908
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3434
[Strang] p. 242Section 6.3expgrowth 26951
[Suppes] p. 22Theorem 2eq0 3470
[Suppes] p. 22Theorem 4eqss 3195  eqssd 3197  eqssi 3196
[Suppes] p. 23Theorem 5ss0 3486  ss0b 3485
[Suppes] p. 23Theorem 6sstr 3188  sstrALT2 27879
[Suppes] p. 23Theorem 7pssirr 3277
[Suppes] p. 23Theorem 8pssn2lp 3278
[Suppes] p. 23Theorem 9psstr 3281
[Suppes] p. 23Theorem 10pssss 3272
[Suppes] p. 25Theorem 12elin 3359  elun 3317
[Suppes] p. 26Theorem 15inidm 3379
[Suppes] p. 26Theorem 16in0 3481
[Suppes] p. 27Theorem 23unidm 3319
[Suppes] p. 27Theorem 24un0 3480
[Suppes] p. 27Theorem 25ssun1 3339
[Suppes] p. 27Theorem 26ssequn1 3346
[Suppes] p. 27Theorem 27unss 3350
[Suppes] p. 27Theorem 28indir 3418
[Suppes] p. 27Theorem 29undir 3419
[Suppes] p. 28Theorem 32difid 3523  difidALT 3524
[Suppes] p. 29Theorem 33difin 3407
[Suppes] p. 29Theorem 34indif 3412
[Suppes] p. 29Theorem 35undif1 3530
[Suppes] p. 29Theorem 36difun2 3534
[Suppes] p. 29Theorem 37difin0 3528
[Suppes] p. 29Theorem 38disjdif 3527
[Suppes] p. 29Theorem 39difundi 3422
[Suppes] p. 29Theorem 40difindi 3424
[Suppes] p. 30Theorem 41nalset 4152
[Suppes] p. 39Theorem 61uniss 3849
[Suppes] p. 39Theorem 65uniop 4268
[Suppes] p. 41Theorem 70intsn 3899
[Suppes] p. 42Theorem 71intpr 3896  intprg 3897
[Suppes] p. 42Theorem 73op1stb 4568
[Suppes] p. 42Theorem 78intun 3895
[Suppes] p. 44Definition 15(a)dfiun2 3938  dfiun2g 3936
[Suppes] p. 44Definition 15(b)dfiin2 3939
[Suppes] p. 47Theorem 86elpw 3632  elpw2 4169  elpw2g 4168  elpwg 3633  elpwgdedVD 27961
[Suppes] p. 47Theorem 87pwid 3639
[Suppes] p. 47Theorem 89pw0 3763
[Suppes] p. 48Theorem 90pwpw0 3764
[Suppes] p. 52Theorem 101xpss12 4791
[Suppes] p. 52Theorem 102xpindi 4818  xpindir 4819
[Suppes] p. 52Theorem 103xpundi 4740  xpundir 4741
[Suppes] p. 54Theorem 105elirrv 7306
[Suppes] p. 58Theorem 2relss 4774
[Suppes] p. 59Theorem 4eldm 4875  eldm2 4876  eldm2g 4874  eldmg 4873
[Suppes] p. 59Definition 3df-dm 4698
[Suppes] p. 60Theorem 6dmin 4885
[Suppes] p. 60Theorem 8rnun 5088
[Suppes] p. 60Theorem 9rnin 5089
[Suppes] p. 60Definition 4dfrn2 4867
[Suppes] p. 61Theorem 11brcnv 4863  brcnvg 4861
[Suppes] p. 62Equation 5elcnv 4857  elcnv2 4858
[Suppes] p. 62Theorem 12relcnv 5050
[Suppes] p. 62Theorem 15cnvin 5087
[Suppes] p. 62Theorem 16cnvun 5085
[Suppes] p. 63Theorem 20co02 5184
[Suppes] p. 63Theorem 21dmcoss 4943
[Suppes] p. 63Definition 7df-co 4697
[Suppes] p. 64Theorem 26cnvco 4864
[Suppes] p. 64Theorem 27coass 5189
[Suppes] p. 65Theorem 31resundi 4968
[Suppes] p. 65Theorem 34elima 5016  elima2 5017  elima3 5018  elimag 5015
[Suppes] p. 65Theorem 35imaundi 5092
[Suppes] p. 66Theorem 40dminss 5094
[Suppes] p. 66Theorem 41imainss 5095
[Suppes] p. 67Exercise 11cnvxp 5096
[Suppes] p. 81Definition 34dfec2 6658
[Suppes] p. 82Theorem 72elec 6694  elecg 6693
[Suppes] p. 82Theorem 73erth 6699  erth2 6700
[Suppes] p. 83Theorem 74erdisj 6702
[Suppes] p. 89Theorem 96map0b 6801
[Suppes] p. 89Theorem 97map0 6803  map0g 6802
[Suppes] p. 89Theorem 98mapsn 6804
[Suppes] p. 89Theorem 99mapss 6805
[Suppes] p. 91Definition 12(ii)alephsuc 7690
[Suppes] p. 91Definition 12(iii)alephlim 7689
[Suppes] p. 92Theorem 1enref 6889  enrefg 6888
[Suppes] p. 92Theorem 2ensym 6905  ensymb 6904  ensymi 6906
[Suppes] p. 92Theorem 3entr 6908
[Suppes] p. 92Theorem 4unen 6938
[Suppes] p. 94Theorem 15endom 6883
[Suppes] p. 94Theorem 16ssdomg 6902
[Suppes] p. 94Theorem 17domtr 6909
[Suppes] p. 95Theorem 18sbth 6976
[Suppes] p. 97Theorem 23canth2 7009  canth2g 7010
[Suppes] p. 97Definition 3brsdom2 6980  df-sdom 6861  dfsdom2 6979
[Suppes] p. 97Theorem 21(i)sdomirr 6993
[Suppes] p. 97Theorem 22(i)domnsym 6982
[Suppes] p. 97Theorem 21(ii)sdomnsym 6981
[Suppes] p. 97Theorem 22(ii)domsdomtr 6991
[Suppes] p. 97Theorem 22(iv)brdom2 6886
[Suppes] p. 97Theorem 21(iii)sdomtr 6994
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6989
[Suppes] p. 98Exercise 4fundmen 6929  fundmeng 6930
[Suppes] p. 98Exercise 6xpdom3 6955
[Suppes] p. 98Exercise 11sdomentr 6990
[Suppes] p. 104Theorem 37fofi 7137
[Suppes] p. 104Theorem 38pwfi 7146
[Suppes] p. 105Theorem 40pwfi 7146
[Suppes] p. 111Axiom for cardinal numberscarden 8168
[Suppes] p. 130Definition 3df-tr 4115
[Suppes] p. 132Theorem 9ssonuni 4577
[Suppes] p. 134Definition 6df-suc 4397
[Suppes] p. 136Theorem Schema 22findes 4685  finds 4681  finds1 4684  finds2 4683
[Suppes] p. 151Theorem 42isfinite 7348  isfinite2 7110  isfiniteg 7112  unbnn 7108
[Suppes] p. 162Definition 5df-ltnq 8537  df-ltpq 8529
[Suppes] p. 197Theorem Schema 4tfindes 4652  tfinds 4649  tfinds2 4653
[Suppes] p. 209Theorem 18oaord1 6544
[Suppes] p. 209Theorem 21oaword2 6546
[Suppes] p. 211Theorem 25oaass 6554
[Suppes] p. 225Definition 8iscard2 7604
[Suppes] p. 227Theorem 56ondomon 8180
[Suppes] p. 228Theorem 59harcard 7606
[Suppes] p. 228Definition 12(i)aleph0 7688
[Suppes] p. 228Theorem Schema 61onintss 4441
[Suppes] p. 228Theorem Schema 62onminesb 4588  onminsb 4589
[Suppes] p. 229Theorem 64alephval2 8189
[Suppes] p. 229Theorem 65alephcard 7692
[Suppes] p. 229Theorem 66alephord2i 7699
[Suppes] p. 229Theorem 67alephnbtwn 7693
[Suppes] p. 229Definition 12df-aleph 7568
[Suppes] p. 242Theorem 6weth 8117
[Suppes] p. 242Theorem 8entric 8174
[Suppes] p. 242Theorem 9carden 8168
[TakeutiZaring] p. 8Axiom 1ax-ext 2265
[TakeutiZaring] p. 13Definition 4.5df-cleq 2277
[TakeutiZaring] p. 13Proposition 4.6df-clel 2280
[TakeutiZaring] p. 13Proposition 4.9cvjust 2279
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2301
[TakeutiZaring] p. 14Definition 4.16df-oprab 5823
[TakeutiZaring] p. 14Proposition 4.14ru 2991
[TakeutiZaring] p. 15Axiom 2zfpair 4211
[TakeutiZaring] p. 15Exercise 1elpr 3659  elpr2 3660  elprg 3658
[TakeutiZaring] p. 15Exercise 2elsn 3656  elsnc 3664  elsnc2 3670  elsnc2g 3669  elsncg 3663
[TakeutiZaring] p. 15Exercise 3elop 4238
[TakeutiZaring] p. 15Exercise 4sneq 3652  sneqr 3781
[TakeutiZaring] p. 15Definition 5.1dfpr2 3657  dfsn2 3655
[TakeutiZaring] p. 16Axiom 3uniex 4515
[TakeutiZaring] p. 16Exercise 6opth 4244
[TakeutiZaring] p. 16Exercise 7opex 4236
[TakeutiZaring] p. 16Exercise 8rext 4221
[TakeutiZaring] p. 16Corollary 5.8unex 4517  unexg 4520
[TakeutiZaring] p. 16Definition 5.3dftp2 3680
[TakeutiZaring] p. 16Definition 5.5df-uni 3829
[TakeutiZaring] p. 16Definition 5.6df-in 3160  df-un 3158
[TakeutiZaring] p. 16Proposition 5.7unipr 3842  uniprg 3843
[TakeutiZaring] p. 17Axiom 4pwex 4192  pwexg 4193
[TakeutiZaring] p. 17Exercise 1eltp 3679
[TakeutiZaring] p. 17Exercise 5elsuc 4460  elsucg 4458  sstr2 3187
[TakeutiZaring] p. 17Exercise 6uncom 3320
[TakeutiZaring] p. 17Exercise 7incom 3362
[TakeutiZaring] p. 17Exercise 8unass 3333
[TakeutiZaring] p. 17Exercise 9inass 3380
[TakeutiZaring] p. 17Exercise 10indi 3416
[TakeutiZaring] p. 17Exercise 11undi 3417
[TakeutiZaring] p. 17Definition 5.9df-pss 3169  dfss2 3170
[TakeutiZaring] p. 17Definition 5.10df-pw 3628
[TakeutiZaring] p. 18Exercise 7unss2 3347
[TakeutiZaring] p. 18Exercise 9df-ss 3167  sseqin2 3389
[TakeutiZaring] p. 18Exercise 10ssid 3198
[TakeutiZaring] p. 18Exercise 12inss1 3390  inss2 3391
[TakeutiZaring] p. 18Exercise 13nss 3237
[TakeutiZaring] p. 18Exercise 15unieq 3837
[TakeutiZaring] p. 18Exercise 18sspwb 4222  sspwimp 27962  sspwimpALT 27969  sspwimpALT2 27973  sspwimpcf 27964
[TakeutiZaring] p. 18Exercise 19pweqb 4229
[TakeutiZaring] p. 19Axiom 5ax-rep 4132
[TakeutiZaring] p. 20Definitiondf-rab 2553
[TakeutiZaring] p. 20Corollary 5.160ex 4151
[TakeutiZaring] p. 20Definition 5.12df-dif 3156
[TakeutiZaring] p. 20Definition 5.14dfnul2 3458
[TakeutiZaring] p. 20Proposition 5.15difid 3523  difidALT 3524
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3465  n0f 3464  neq0 3466
[TakeutiZaring] p. 21Axiom 6zfreg 7304
[TakeutiZaring] p. 21Axiom 6'zfregs 7409
[TakeutiZaring] p. 21Theorem 5.22setind 7414
[TakeutiZaring] p. 21Definition 5.20df-v 2791
[TakeutiZaring] p. 21Proposition 5.21vprc 4153
[TakeutiZaring] p. 22Exercise 10ss 3484
[TakeutiZaring] p. 22Exercise 3ssex 4159  ssexg 4161
[TakeutiZaring] p. 22Exercise 4inex1 4156
[TakeutiZaring] p. 22Exercise 5ruv 7309
[TakeutiZaring] p. 22Exercise 6elirr 7307
[TakeutiZaring] p. 22Exercise 7ssdif0 3514
[TakeutiZaring] p. 22Exercise 11difdif 3303
[TakeutiZaring] p. 22Exercise 13undif3 3430  undif3VD 27926
[TakeutiZaring] p. 22Exercise 14difss 3304
[TakeutiZaring] p. 22Exercise 15sscon 3311
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2549
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2550
[TakeutiZaring] p. 23Proposition 6.2xpex 4800  xpexg 4799  xpexgALT 6031
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4695
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5277
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5410  fun11 5280
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5233  svrelfun 5278
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4866
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4868
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4700
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4701
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4697
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5127  dfrel2 5123
[TakeutiZaring] p. 25Exercise 3xpss 4792
[TakeutiZaring] p. 25Exercise 5relun 4801
[TakeutiZaring] p. 25Exercise 6reluni 4807
[TakeutiZaring] p. 25Exercise 9inxp 4817
[TakeutiZaring] p. 25Exercise 12relres 4982
[TakeutiZaring] p. 25Exercise 13opelres 4959  opelresg 4961
[TakeutiZaring] p. 25Exercise 14dmres 4975
[TakeutiZaring] p. 25Exercise 15resss 4978
[TakeutiZaring] p. 25Exercise 17resabs1 4983
[TakeutiZaring] p. 25Exercise 18funres 5258
[TakeutiZaring] p. 25Exercise 24relco 5169
[TakeutiZaring] p. 25Exercise 29funco 5257
[TakeutiZaring] p. 25Exercise 30f1co 5411
[TakeutiZaring] p. 26Definition 6.10eu2 2169
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 5229  fv3 5501
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5207  cnvexg 5206
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4940  dmexg 4938
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4941  rnexg 4939
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27057
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27058
[TakeutiZaring] p. 27Corollary 6.13fvex 5499
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5504  tz6.12-afv 27412  tz6.12 5505  tz6.12c 5508
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5507  tz6.12i 5509
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5224
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5225
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5227  wfo 5219
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5226  wf1 5218
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5228  wf1o 5220
[TakeutiZaring] p. 28Exercise 4eqfnfv 5583  eqfnfv2 5584  eqfnfv2f 5587
[TakeutiZaring] p. 28Exercise 5fvco 5556
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5702  fnexALT 5703
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5698  resfunexgALT 5699
[TakeutiZaring] p. 29Exercise 9funimaex 5295  funimaexg 5294
[TakeutiZaring] p. 29Definition 6.18df-br 4025
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4314
[TakeutiZaring] p. 30Definition 6.21dffr2 4357  dffr3 5044  eliniseg 5041  iniseg 5043
[TakeutiZaring] p. 30Definition 6.22df-eprel 4304
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4370  fr3nr 4570  frirr 4369
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4351
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4572
[TakeutiZaring] p. 31Exercise 1frss 4359
[TakeutiZaring] p. 31Exercise 4wess 4379
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23606  tz6.26i 23607  wefrc 4386  wereu2 4389
[TakeutiZaring] p. 32Theorem 6.27wfi 23608  wfii 23609
[TakeutiZaring] p. 32Definition 6.28df-isom 5230
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5787
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5788
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5794
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5795
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5796
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5800
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5807
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5809
[TakeutiZaring] p. 35Notationwtr 4114
[TakeutiZaring] p. 35Theorem 7.2trelpss 27059  tz7.2 4376
[TakeutiZaring] p. 35Definition 7.1dftr3 4118
[TakeutiZaring] p. 36Proposition 7.4ordwe 4404
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4412
[TakeutiZaring] p. 36Proposition 7.6ordelord 4413  ordelordALT 27572  ordelordALTVD 27911
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4419  ordelssne 4418
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4417
[TakeutiZaring] p. 37Proposition 7.9ordin 4421
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4579
[TakeutiZaring] p. 38Corollary 7.15ordsson 4580
[TakeutiZaring] p. 38Definition 7.11df-on 4395
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4423
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27585  ordon 4573
[TakeutiZaring] p. 38Proposition 7.13onprc 4575
[TakeutiZaring] p. 39Theorem 7.17tfi 4643
[TakeutiZaring] p. 40Exercise 3ontr2 4438
[TakeutiZaring] p. 40Exercise 7dftr2 4116
[TakeutiZaring] p. 40Exercise 9onssmin 4587
[TakeutiZaring] p. 40Exercise 11unon 4621
[TakeutiZaring] p. 40Exercise 12ordun 4493
[TakeutiZaring] p. 40Exercise 14ordequn 4492
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4576
[TakeutiZaring] p. 40Proposition 7.20elssuni 3856
[TakeutiZaring] p. 41Definition 7.22df-suc 4397
[TakeutiZaring] p. 41Proposition 7.23sssucid 4468  sucidg 4469
[TakeutiZaring] p. 41Proposition 7.24suceloni 4603
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4483  ordnbtwn 4482
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4618
[TakeutiZaring] p. 42Exercise 1df-lim 4396
[TakeutiZaring] p. 42Exercise 4omssnlim 4669
[TakeutiZaring] p. 42Exercise 7ssnlim 4673
[TakeutiZaring] p. 42Exercise 8onsucssi 4631  ordelsuc 4610
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4612
[TakeutiZaring] p. 42Definition 7.27nlimon 4641
[TakeutiZaring] p. 42Definition 7.28dfom2 4657
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4674
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4675
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4676
[TakeutiZaring] p. 43Remarkomon 4666
[TakeutiZaring] p. 43Axiom 7inf3 7331  omex 7339
[TakeutiZaring] p. 43Theorem 7.32ordom 4664
[TakeutiZaring] p. 43Corollary 7.31find 4680
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4677
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4678
[TakeutiZaring] p. 44Exercise 1limomss 4660
[TakeutiZaring] p. 44Exercise 2int0 3877  trint0 4131
[TakeutiZaring] p. 44Exercise 4intss1 3878
[TakeutiZaring] p. 44Exercise 5intex 4170
[TakeutiZaring] p. 44Exercise 6oninton 4590
[TakeutiZaring] p. 44Exercise 11ordintdif 4440
[TakeutiZaring] p. 44Definition 7.35df-int 3864
[TakeutiZaring] p. 44Proposition 7.34noinfep 7355
[TakeutiZaring] p. 45Exercise 4onint 4585
[TakeutiZaring] p. 47Lemma 1tfrlem1 6386
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6408
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6409
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6410
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6414  tz7.44-2 6415  tz7.44-3 6416
[TakeutiZaring] p. 50Exercise 1smogt 6379
[TakeutiZaring] p. 50Exercise 3smoiso 6374
[TakeutiZaring] p. 50Definition 7.46df-smo 6358
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6452  tz7.49c 6453
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6450
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6449
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6451
[TakeutiZaring] p. 53Proposition 7.532eu5 2228
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7634
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7635
[TakeutiZaring] p. 56Definition 8.1oalim 6526  oasuc 6518
[TakeutiZaring] p. 57Remarktfindsg 4650
[TakeutiZaring] p. 57Proposition 8.2oacl 6529
[TakeutiZaring] p. 57Proposition 8.3oa0 6510  oa0r 6532
[TakeutiZaring] p. 57Proposition 8.16omcl 6530
[TakeutiZaring] p. 58Corollary 8.5oacan 6541
[TakeutiZaring] p. 58Proposition 8.4nnaord 6612  nnaordi 6611  oaord 6540  oaordi 6539
[TakeutiZaring] p. 59Proposition 8.6iunss2 3948  uniss2 3859
[TakeutiZaring] p. 59Proposition 8.7oawordri 6543
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6548  oawordex 6550
[TakeutiZaring] p. 59Proposition 8.9nnacl 6604
[TakeutiZaring] p. 59Proposition 8.10oaabs 6637
[TakeutiZaring] p. 60Remarkoancom 7347
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6553
[TakeutiZaring] p. 62Exercise 1nnarcl 6609
[TakeutiZaring] p. 62Exercise 5oaword1 6545
[TakeutiZaring] p. 62Definition 8.15om0 6511  om0x 6513  omlim 6527  omsuc 6520
[TakeutiZaring] p. 63Proposition 8.17nnecl 6606  nnmcl 6605
[TakeutiZaring] p. 63Proposition 8.19nnmord 6625  nnmordi 6624  omord 6561  omordi 6559
[TakeutiZaring] p. 63Proposition 8.20omcan 6562
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6629  omwordri 6565
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6533
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6535  om1r 6536
[TakeutiZaring] p. 64Proposition 8.22om00 6568
[TakeutiZaring] p. 64Proposition 8.23omordlim 6570
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6571
[TakeutiZaring] p. 64Proposition 8.25odi 6572
[TakeutiZaring] p. 65Theorem 8.26omass 6573
[TakeutiZaring] p. 67Definition 8.30nnesuc 6601  oe0 6516  oelim 6528  oesuc 6521  onesuc 6524
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6514
[TakeutiZaring] p. 67Proposition 8.32oen0 6579
[TakeutiZaring] p. 67Proposition 8.33oeordi 6580
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6515
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6538
[TakeutiZaring] p. 68Corollary 8.34oeord 6581
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6587
[TakeutiZaring] p. 68Proposition 8.35oewordri 6585
[TakeutiZaring] p. 68Proposition 8.37oeworde 6586
[TakeutiZaring] p. 69Proposition 8.41oeoa 6590
[TakeutiZaring] p. 70Proposition 8.42oeoe 6592
[TakeutiZaring] p. 73Theorem 9.1trcl 7405  tz9.1 7406
[TakeutiZaring] p. 76Definition 9.9df-r1 7431  r10 7435  r1lim 7439  r1limg 7438  r1suc 7437  r1sucg 7436
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7447  r1ord2 7448  r1ordg 7445
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7457
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7482  tz9.13 7458  tz9.13g 7459
[TakeutiZaring] p. 79Definition 9.14df-rank 7432  rankval 7483  rankvalb 7464  rankvalg 7484
[TakeutiZaring] p. 79Proposition 9.16rankel 7506  rankelb 7491
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7520  rankval3 7507  rankval3b 7493
[TakeutiZaring] p. 79Proposition 9.18rankonid 7496
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7462
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7501  rankr1c 7488  rankr1g 7499
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7502
[TakeutiZaring] p. 80Exercise 1rankss 7516  rankssb 7515
[TakeutiZaring] p. 80Exercise 2unbndrank 7509
[TakeutiZaring] p. 80Proposition 9.19bndrank 7508
[TakeutiZaring] p. 83Axiom of Choiceac4 8097  dfac3 7743
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7652  numth 8094  numth2 8093
[TakeutiZaring] p. 85Definition 10.4cardval 8163
[TakeutiZaring] p. 85Proposition 10.5cardid 8164  cardid2 7581
[TakeutiZaring] p. 85Proposition 10.9oncard 7588
[TakeutiZaring] p. 85Proposition 10.10carden 8168
[TakeutiZaring] p. 85Proposition 10.11cardidm 7587
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7572
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7593
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7585
[TakeutiZaring] p. 87Proposition 10.15pwen 7029
[TakeutiZaring] p. 88Exercise 1en0 6919
[TakeutiZaring] p. 88Exercise 7infensuc 7034
[TakeutiZaring] p. 89Exercise 10omxpen 6959
[TakeutiZaring] p. 90Corollary 10.23cardnn 7591
[TakeutiZaring] p. 90Definition 10.27alephiso 7720
[TakeutiZaring] p. 90Proposition 10.20nneneq 7039
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7045
[TakeutiZaring] p. 90Proposition 10.26alephprc 7721
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7044
[TakeutiZaring] p. 91Exercise 2alephle 7710
[TakeutiZaring] p. 91Exercise 3aleph0 7688
[TakeutiZaring] p. 91Exercise 4cardlim 7600
[TakeutiZaring] p. 91Exercise 7infpss 7838
[TakeutiZaring] p. 91Exercise 8infcntss 7125
[TakeutiZaring] p. 91Definition 10.29df-fin 6862  isfi 6880
[TakeutiZaring] p. 92Proposition 10.32onfin 7046
[TakeutiZaring] p. 92Proposition 10.34imadomg 8154
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6952
[TakeutiZaring] p. 93Proposition 10.35fodomb 8146
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7810  unxpdom 7065
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7602  cardsdomelir 7601
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7067
[TakeutiZaring] p. 94Proposition 10.39infxpen 7637
[TakeutiZaring] p. 95Definition 10.42df-map 6769
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8179  infxpidm2 7639
[TakeutiZaring] p. 95Proposition 10.41infcda 7829  infxp 7836  infxpg 24493
[TakeutiZaring] p. 96Proposition 10.44pw2en 6964  pw2f1o 6962
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7022
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8109
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8104  ac6s5 8113
[TakeutiZaring] p. 98Theorem 10.47unidom 8160
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8161  uniimadomf 8162
[TakeutiZaring] p. 100Definition 11.1cfcof 7895
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7890
[TakeutiZaring] p. 102Exercise 1cfle 7875
[TakeutiZaring] p. 102Exercise 2cf0 7872
[TakeutiZaring] p. 102Exercise 3cfsuc 7878
[TakeutiZaring] p. 102Exercise 4cfom 7885
[TakeutiZaring] p. 102Proposition 11.9coftr 7894
[TakeutiZaring] p. 103Theorem 11.15alephreg 8199
[TakeutiZaring] p. 103Proposition 11.11cardcf 7873
[TakeutiZaring] p. 103Proposition 11.13alephsing 7897
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7719
[TakeutiZaring] p. 104Proposition 11.16carduniima 7718
[TakeutiZaring] p. 104Proposition 11.18alephfp 7730  alephfp2 7731
[TakeutiZaring] p. 106Theorem 11.20gchina 8316
[TakeutiZaring] p. 106Theorem 11.21mappwen 7734
[TakeutiZaring] p. 107Theorem 11.26konigth 8186
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8200
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8201
[Tarski] p. 67Axiom B5ax-4 2078
[Tarski] p. 68Lemma 6avril1 20828  equid 1649  equid1 2099  equid1ALT 2117
[Tarski] p. 69Lemma 7equcomi 1650
[Tarski] p. 70Lemma 14spim 1918  spime 1919  spimeh 1726
[Tarski] p. 70Lemma 16ax-11 1719  ax-11o 2084  ax11i 1633
[Tarski] p. 70Lemmas 16 and 17sb6 2016
[Tarski] p. 75Axiom B7ax9v 1642
[Tarski] p. 75Scheme B7ax9vax9 28425
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1608
[Tarski], p. 75Scheme B8 of system S2ax-13 1690  ax-14 1692  ax-8 1648
[Truss] p. 114Theorem 5.18ruc 12515
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 501
[WhiteheadRussell] p. 96Axiom *1.3olc 375
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 377
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 510
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 817
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 162
[WhiteheadRussell] p. 100Theorem *2.02ax-1 7
[WhiteheadRussell] p. 100Theorem *2.03con2 110
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 78
[WhiteheadRussell] p. 100Theorem *2.05imim2 51
[WhiteheadRussell] p. 100Theorem *2.06imim1 72
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 408
[WhiteheadRussell] p. 101Theorem *2.06barbara 2241  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 387
[WhiteheadRussell] p. 101Theorem *2.08id 21  id1 22
[WhiteheadRussell] p. 101Theorem *2.11exmid 406
[WhiteheadRussell] p. 101Theorem *2.12notnot1 116
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 409
[WhiteheadRussell] p. 102Theorem *2.14notnot2 106  notnot2ALT2 27971
[WhiteheadRussell] p. 102Theorem *2.15con1 122
[WhiteheadRussell] p. 103Theorem *2.16con3 128  con3th 929
[WhiteheadRussell] p. 103Theorem *2.17ax-3 9
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 104
[WhiteheadRussell] p. 104Theorem *2.2orc 376
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 558
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 102
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 103
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 395
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 858
[WhiteheadRussell] p. 104Theorem *2.27conventions 3  pm2.27 37
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 513
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 514
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 819
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 820
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 818
[WhiteheadRussell] p. 105Definition *2.33df-3or 940
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 561
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 559
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 560
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 49
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 388
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 389
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 146
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 164
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 390
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 391
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 392
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 147
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 149
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 364
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 365
[WhiteheadRussell] p. 107Theorem *2.55orel1 373
[WhiteheadRussell] p. 107Theorem *2.56orel2 374
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 165
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 400
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 766
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 767
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 166
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 393  pm2.67 394
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 148
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 399
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 826
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 401
[WhiteheadRussell] p. 108Theorem *2.69looinv 176
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 821
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 822
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 825
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 824
[WhiteheadRussell] p. 108Theorem *2.77ax-2 8
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 827
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 828
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 73
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 829
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 96
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 486
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 436  pm3.2im 139
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 487
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 488
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 489
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 490
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 437
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 438
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 857
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 573
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 433
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 434
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 445  simplim 145
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 449  simprim 144
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 571
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 572
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 565
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 546
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 544
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 545
[WhiteheadRussell] p. 113Theorem *3.44jao 500  pm3.44 499
[WhiteheadRussell] p. 113Theorem *3.47prth 557
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 835
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 810
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 809
[WhiteheadRussell] p. 116Theorem *4.1con34b 285
[WhiteheadRussell] p. 117Theorem *4.2biid 229
[WhiteheadRussell] p. 117Theorem *4.11notbi 288
[WhiteheadRussell] p. 117Theorem *4.12con2bi 320
[WhiteheadRussell] p. 117Theorem *4.13notnot 284
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 564
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 567
[WhiteheadRussell] p. 117Theorem *4.21bicom 193
[WhiteheadRussell] p. 117Theorem *4.22biantr 902  bitr 692  wl-bitr 24327
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 627
[WhiteheadRussell] p. 117Theorem *4.25oridm 502  pm4.25 503
[WhiteheadRussell] p. 118Theorem *4.3ancom 439
[WhiteheadRussell] p. 118Theorem *4.4andi 842
[WhiteheadRussell] p. 118Theorem *4.31orcom 378
[WhiteheadRussell] p. 118Theorem *4.32anass 633
[WhiteheadRussell] p. 118Theorem *4.33orass 512
[WhiteheadRussell] p. 118Theorem *4.36anbi1 690
[WhiteheadRussell] p. 118Theorem *4.37orbi1 689
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 847
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 846
[WhiteheadRussell] p. 118Definition *4.34df-3an 941
[WhiteheadRussell] p. 119Theorem *4.41ordi 837
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 931
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 898
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 563
[WhiteheadRussell] p. 119Theorem *4.45orabs 831  pm4.45 672  pm4.45im 547
[WhiteheadRussell] p. 120Theorem *4.5anor 477
[WhiteheadRussell] p. 120Theorem *4.6imor 403
[WhiteheadRussell] p. 120Theorem *4.7anclb 532
[WhiteheadRussell] p. 120Theorem *4.51ianor 476
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 479
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 480
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 481
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 482
[WhiteheadRussell] p. 120Theorem *4.56ioran 478  pm4.56 483
[WhiteheadRussell] p. 120Theorem *4.57oran 484  pm4.57 485
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 417
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 410
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 412
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 363
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 418
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 411
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 419
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 614  pm4.71d 618  pm4.71i 616  pm4.71r 615  pm4.71rd 619  pm4.71ri 617
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 851
[WhiteheadRussell] p. 121Theorem *4.73iba 491
[WhiteheadRussell] p. 121Theorem *4.74biorf 396
[WhiteheadRussell] p. 121Theorem *4.76jcab 836  pm4.76 841
[WhiteheadRussell] p. 121Theorem *4.77jaob 761  pm4.77 765
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 568
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 569
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 356
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 357
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 899
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 900
[WhiteheadRussell] p. 122Theorem *4.84imbi1 315
[WhiteheadRussell] p. 122Theorem *4.85imbi2 316
[WhiteheadRussell] p. 122Theorem *4.86bibi1 319  wl-bibi1 24320
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 352  impexp 435  pm4.87 570
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 833
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 859
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 860
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 862
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 861
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 864
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 865
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 863
[WhiteheadRussell] p. 124Theorem *5.18nbbn 349  pm5.18 347
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 351
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 834
[WhiteheadRussell] p. 124Theorem *5.22xor 866
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 868
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 869
[WhiteheadRussell] p. 124Theorem *5.25dfor2 402
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 695
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 353
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 328
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 883
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 905
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 574
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 620
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 853
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 874
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 854
[WhiteheadRussell] p. 125Theorem *5.41imdi 354  pm5.41 355
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 533
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 882
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 774
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 875
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 872
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 696
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 894
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 895
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 907
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 332
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 237
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 908
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 26952
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26953
[WhiteheadRussell] p. 147Theorem *10.2219.26 1585
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26954
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26955
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26956
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1607
[WhiteheadRussell] p. 151Theorem *10.301albitr 26957
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26958
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26959
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26960
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26961
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26963
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26964
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26965
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26962
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26968
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2052
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26969
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26970
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1716
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26971
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26972
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26973
[WhiteheadRussell] p. 162Theorem *11.322alim 26974
[WhiteheadRussell] p. 162Theorem *11.332albi 26975
[WhiteheadRussell] p. 162Theorem *11.342exim 26976
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 26978
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26977
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1602
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26980
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26981
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26979
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1565
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26982
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26983
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1572
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26984
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1845  pm11.53g 24362
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26985
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26990
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26986
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26987
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26988
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26989
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26994
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26991
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26992
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26993
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26995
[WhiteheadRussell] p. 175Definition *14.02df-eu 2148
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27006  pm13.13b 27007
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27008
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2519
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2520
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2909
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27014
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27015
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27009
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27589  pm13.193 27010
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27011
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27012
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27013
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27020
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27019
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27018
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3044
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27021  pm14.122b 27022  pm14.122c 27023
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27024  pm14.123b 27025  pm14.123c 27026
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27028
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27027
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27029
[WhiteheadRussell] p. 190Theorem *14.22iota4 6270
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27030
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6271
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27031
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27033
[WhiteheadRussell] p. 192Theorem *14.26eupick 2207  eupickbi 2210  sbaniota 27034
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27032
[WhiteheadRussell] p. 192Theorem *14.271eubi 27035
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27036
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 5229
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7628  pm54.43lem 7627
[Young] p. 141Definition of operator orderingleop2 22696
[Young] p. 142Example 12.2(i)0leop 22702  idleop 22703
[vandenDries] p. 42Lemma 61irrapx1 26312
[vandenDries] p. 43Theorem 62pellex 26319  pellexlem1 26313

This page was last updated on 10-Aug-2017.
Copyright terms: Public domain