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 13621
[Adamek] p. 29Proposition 3.14(1)invinv 13635
[Adamek] p. 29Proposition 3.14(2)invco 13636  isoco 13638
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25558
[AitkenIBCG] p. 3Definition 2df-angtrg 25554  df-trcng 25557
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25430  df-ig2 25429
[AitkenIBG] p. 2Definition 4df-li 25445
[AitkenIBG] p. 3Definition 5df-col 25459
[AitkenIBG] p. 3Definition 6df-con2 25464
[AitkenIBG] p. 3Proposition 4isconcl5a 25469  isconcl5ab 25470  isconcl6a 25471  isconcl6ab 25472
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25477
[AitkenIBG] p. 4Exercise 5tpne 25443
[AitkenIBG] p. 4Definition 8df-seg2 25499
[AitkenIBG] p. 4Definition 10df-sside 25531
[AitkenIBG] p. 4Definition 11df-ray2 25520
[AitkenIBG] p. 10Definition 17df-angle 25526
[AitkenIBG] p. 15Definition 23df-triangle 25528
[AitkenIBG] p. 15Definition 24df-cnvx 25547
[AitkenNG] p. 2Definition 1df-slices 25561
[AitkenNG] p. 2Definition 2df-Cut 25563
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25565
[AitkenNG] p. 4Definition 5df-crcl 25567
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18180  df-nmoo 21284
[AkhiezerGlazman] p. 64Theoremhmopidmch 22694  hmopidmchi 22692
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22742  pjcmul2i 22743
[AkhiezerGlazman] p. 72Theoremcnvunop 22459  unoplin 22461
[AkhiezerGlazman] p. 72Equation 2unopadj 22460  unopadj2 22479
[AkhiezerGlazman] p. 73Theoremelunop2 22554  lnopunii 22553
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22627
[Apostol] p. 18Theorem I.1addcan 8964  addcan2d 8984  addcan2i 8974  addcand 8983  addcani 8973
[Apostol] p. 18Theorem I.2negeu 9010
[Apostol] p. 18Theorem I.3negsub 9063  negsubd 9131  negsubi 9092
[Apostol] p. 18Theorem I.4negneg 9065  negnegd 9116  negnegi 9084
[Apostol] p. 18Theorem I.5subdi 9181  subdid 9203  subdii 9196  subdir 9182  subdird 9204  subdiri 9197
[Apostol] p. 18Theorem I.6mul01 8959  mul01d 8979  mul01i 8970  mul02 8958  mul02d 8978  mul02i 8969
[Apostol] p. 18Theorem I.7mulcan 9373  mulcan2d 9370  mulcand 9369  mulcani 9375
[Apostol] p. 18Theorem I.8receu 9381
[Apostol] p. 18Theorem I.9divrec 9408  divrecd 9507  divreci 9473  divreczi 9466
[Apostol] p. 18Theorem I.10recrec 9425  recreci 9460
[Apostol] p. 18Theorem I.11mul0or 9376  mul0ord 9386  mul0ori 9384
[Apostol] p. 18Theorem I.12mul2neg 9187  mul2negd 9202  mul2negi 9195  mulneg1 9184  mulneg1d 9200  mulneg1i 9193
[Apostol] p. 18Theorem I.13divadddiv 9443  divadddivd 9548  divadddivi 9490
[Apostol] p. 18Theorem I.14divmuldiv 9428  divmuldivd 9545  divmuldivi 9488
[Apostol] p. 18Theorem I.15divdivdiv 9429  divdivdivd 9551  divdivdivi 9491
[Apostol] p. 20Axiom 7rpaddcl 10342  rpaddcld 10373  rpmulcl 10343  rpmulcld 10374
[Apostol] p. 20Axiom 8rpneg 10351
[Apostol] p. 20Axiom 90nrp 10352
[Apostol] p. 20Theorem I.17lttri 8913
[Apostol] p. 20Theorem I.18ltadd1d 9333  ltadd1dd 9351  ltadd1i 9295
[Apostol] p. 20Theorem I.19ltmul1 9574  ltmul1a 9573  ltmul1i 9643  ltmul1ii 9653  ltmul2 9575  ltmul2d 10396  ltmul2dd 10410  ltmul2i 9646
[Apostol] p. 20Theorem I.20msqgt0 9262  msqgt0d 9308  msqgt0i 9278
[Apostol] p. 20Theorem I.210lt1 9264
[Apostol] p. 20Theorem I.23lt0neg1 9248  lt0neg1d 9310  ltneg 9242  ltnegd 9318  ltnegi 9285
[Apostol] p. 20Theorem I.25lt2add 9227  lt2addd 9362  lt2addi 9303
[Apostol] p. 20Definition of positive numbersdf-rp 10323
[Apostol] p. 21Exercise 4recgt0 9568  recgt0d 9659  recgt0i 9629  recgt0ii 9630
[Apostol] p. 22Definition of integersdf-z 9993
[Apostol] p. 22Definition of positive integersdfnn3 9728
[Apostol] p. 22Definition of rationalsdf-q 10285
[Apostol] p. 24Theorem I.26supeu 7173
[Apostol] p. 26Theorem I.28nnunb 9929
[Apostol] p. 26Theorem I.29arch 9930
[Apostol] p. 28Exercise 2btwnz 10082
[Apostol] p. 28Exercise 3nnrecl 9931
[Apostol] p. 28Exercise 4rebtwnz 10283
[Apostol] p. 28Exercise 5zbtwnre 10282
[Apostol] p. 28Exercise 6qbtwnre 10493
[Apostol] p. 28Exercise 10(a)zneo 10062
[Apostol] p. 29Theorem I.35msqsqrd 11888  resqrth 11707  sqrth 11814  sqrthi 11820  sqsqrd 11887
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9717
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10252
[Apostol] p. 361Remarkcrreczi 11193
[Apostol] p. 363Remarkabsgt0i 11848
[Apostol] p. 363Exampleabssubd 11901  abssubi 11852
[Baer] p. 40Property (b)mapdord 31078
[Baer] p. 40Property (c)mapd11 31079
[Baer] p. 40Property (e)mapdin 31102  mapdlsm 31104
[Baer] p. 40Property (f)mapd0 31105
[Baer] p. 40Definition of projectivitydf-mapd 31065  mapd1o 31088
[Baer] p. 41Property (g)mapdat 31107
[Baer] p. 44Part (1)mapdpg 31146
[Baer] p. 45Part (2)hdmap1eq 31242  mapdheq 31168  mapdheq2 31169  mapdheq2biN 31170
[Baer] p. 45Part (3)baerlem3 31153
[Baer] p. 46Part (4)mapdheq4 31172  mapdheq4lem 31171
[Baer] p. 46Part (5)baerlem5a 31154  baerlem5abmN 31158  baerlem5amN 31156  baerlem5b 31155  baerlem5bmN 31157
[Baer] p. 47Part (6)hdmap1l6 31262  hdmap1l6a 31250  hdmap1l6e 31255  hdmap1l6f 31256  hdmap1l6g 31257  hdmap1l6lem1 31248  hdmap1l6lem2 31249  hdmap1p6N 31263  mapdh6N 31187  mapdh6aN 31175  mapdh6eN 31180  mapdh6fN 31181  mapdh6gN 31182  mapdh6lem1N 31173  mapdh6lem2N 31174
[Baer] p. 48Part 9hdmapval 31271
[Baer] p. 48Part 10hdmap10 31283
[Baer] p. 48Part 11hdmapadd 31286
[Baer] p. 48Part (6)hdmap1l6h 31258  mapdh6hN 31183
[Baer] p. 48Part (7)mapdh75cN 31193  mapdh75d 31194  mapdh75e 31192  mapdh75fN 31195  mapdh7cN 31189  mapdh7dN 31190  mapdh7eN 31188  mapdh7fN 31191
[Baer] p. 48Part (8)mapdh8 31229  mapdh8a 31215  mapdh8aa 31216  mapdh8ab 31217  mapdh8ac 31218  mapdh8ad 31219  mapdh8b 31220  mapdh8c 31221  mapdh8d 31223  mapdh8d0N 31222  mapdh8e 31224  mapdh8fN 31225  mapdh8g 31226  mapdh8i 31227  mapdh8j 31228
[Baer] p. 48Part (9)mapdh9a 31230
[Baer] p. 48Equation 10mapdhvmap 31209
[Baer] p. 49Part 12hdmap11 31291  hdmapeq0 31287  hdmapf1oN 31308  hdmapneg 31289  hdmaprnN 31307  hdmaprnlem1N 31292  hdmaprnlem3N 31293  hdmaprnlem3uN 31294  hdmaprnlem4N 31296  hdmaprnlem6N 31297  hdmaprnlem7N 31298  hdmaprnlem8N 31299  hdmaprnlem9N 31300  hdmapsub 31290
[Baer] p. 49Part 14hdmap14lem1 31311  hdmap14lem10 31320  hdmap14lem1a 31309  hdmap14lem2N 31312  hdmap14lem2a 31310  hdmap14lem3 31313  hdmap14lem8 31318  hdmap14lem9 31319
[Baer] p. 50Part 14hdmap14lem11 31321  hdmap14lem12 31322  hdmap14lem13 31323  hdmap14lem14 31324  hdmap14lem15 31325  hgmapval 31330
[Baer] p. 50Part 15hgmapadd 31337  hgmapmul 31338  hgmaprnlem2N 31340  hgmapvs 31334
[Baer] p. 50Part 16hgmaprnN 31344
[Baer] p. 110Lemma 1hdmapip0com 31360
[Baer] p. 110Line 27hdmapinvlem1 31361
[Baer] p. 110Line 28hdmapinvlem2 31362
[Baer] p. 110Line 30hdmapinvlem3 31363
[Baer] p. 110Part 1.2hdmapglem5 31365  hgmapvv 31369
[Baer] p. 110Proposition 1hdmapinvlem4 31364
[Baer] p. 111Line 10hgmapvvlem1 31366
[Baer] p. 111Line 15hdmapg 31373  hdmapglem7 31372
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2122
[BellMachover] p. 460Notationdf-mo 2123
[BellMachover] p. 460Definitionmo3 2149
[BellMachover] p. 461Axiom Extax-ext 2239
[BellMachover] p. 462Theorem 1.1bm1.1 2243
[BellMachover] p. 463Axiom Repaxrep5 4110
[BellMachover] p. 463Scheme Sepaxsep 4114
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4118
[BellMachover] p. 466Axiom Powaxpow3 4163
[BellMachover] p. 466Axiom Unionaxun2 4486
[BellMachover] p. 468Definitiondf-ord 4367
[BellMachover] p. 469Theorem 2.2(i)ordirr 4382
[BellMachover] p. 469Theorem 2.2(iii)onelon 4389
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4384
[BellMachover] p. 471Definition of Ndf-om 4629
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4569
[BellMachover] p. 471Definition of Limdf-lim 4369
[BellMachover] p. 472Axiom Infzfinf2 7311
[BellMachover] p. 473Theorem 2.8limom 4643
[BellMachover] p. 477Equation 3.1df-r1 7404
[BellMachover] p. 478Definitionrankval2 7458
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7422  r1ord3g 7419
[BellMachover] p. 480Axiom Regzfreg2 7278
[BellMachover] p. 488Axiom ACac5 8072  dfac4 7717
[BellMachover] p. 490Definition of alephalephval3 7705
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28759
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22894
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22936  chirredi 22935
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22924
[Beran] p. 3Definition of joinsshjval3 21894
[Beran] p. 39Theorem 2.3(i)cmcm2 22156  cmcm2i 22133  cmcm2ii 22138  cmt2N 28690
[Beran] p. 40Theorem 2.3(iii)lecm 22157  lecmi 22142  lecmii 22143
[Beran] p. 45Theorem 3.4cmcmlem 22131
[Beran] p. 49Theorem 4.2cm2j 22160  cm2ji 22165  cm2mi 22166
[Beran] p. 95Definitiondf-sh 21747  issh2 21749
[Beran] p. 95Lemma 3.1(S5)his5 21626
[Beran] p. 95Lemma 3.1(S6)his6 21639
[Beran] p. 95Lemma 3.1(S7)his7 21630
[Beran] p. 95Lemma 3.2(S8)ho01i 22369
[Beran] p. 95Lemma 3.2(S9)hoeq1 22371
[Beran] p. 95Lemma 3.2(S10)ho02i 22370
[Beran] p. 95Lemma 3.2(S11)hoeq2 22372
[Beran] p. 95Postulate (S1)ax-his1 21622  his1i 21640
[Beran] p. 95Postulate (S2)ax-his2 21623
[Beran] p. 95Postulate (S3)ax-his3 21624
[Beran] p. 95Postulate (S4)ax-his4 21625
[Beran] p. 96Definition of normdf-hnorm 21509  dfhnorm2 21662  normval 21664
[Beran] p. 96Definition for Cauchy sequencehcau 21724
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21514
[Beran] p. 96Definition of complete subspaceisch3 21782
[Beran] p. 96Definition of convergedf-hlim 21513  hlimi 21728
[Beran] p. 97Theorem 3.3(i)norm-i-i 21673  norm-i 21669
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21677  norm-ii 21678  normlem0 21649  normlem1 21650  normlem2 21651  normlem3 21652  normlem4 21653  normlem5 21654  normlem6 21655  normlem7 21656  normlem7tALT 21659
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21679  norm-iii 21680
[Beran] p. 98Remark 3.4bcs 21721  bcsiALT 21719  bcsiHIL 21720
[Beran] p. 98Remark 3.4(B)normlem9at 21661  normpar 21695  normpari 21694
[Beran] p. 98Remark 3.4(C)normpyc 21686  normpyth 21685  normpythi 21682
[Beran] p. 99Remarklnfn0 22588  lnfn0i 22583  lnop0 22507  lnop0i 22511
[Beran] p. 99Theorem 3.5(i)nmcexi 22567  nmcfnex 22594  nmcfnexi 22592  nmcopex 22570  nmcopexi 22568
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22595  nmcfnlbi 22593  nmcoplb 22571  nmcoplbi 22569
[Beran] p. 99Theorem 3.5(iii)lnfncon 22597  lnfnconi 22596  lnopcon 22576  lnopconi 22575
[Beran] p. 100Lemma 3.6normpar2i 21696
[Beran] p. 101Lemma 3.6norm3adifi 21693  norm3adifii 21688  norm3dif 21690  norm3difi 21687
[Beran] p. 102Theorem 3.7(i)chocunii 21841  pjhth 21933  pjhtheu 21934  pjpjhth 21965  pjpjhthi 21966  pjth 18766
[Beran] p. 102Theorem 3.7(ii)ococ 21946  ococi 21945
[Beran] p. 103Remark 3.8nlelchi 22602
[Beran] p. 104Theorem 3.9riesz3i 22603  riesz4 22605  riesz4i 22604
[Beran] p. 104Theorem 3.10cnlnadj 22620  cnlnadjeu 22619  cnlnadjeui 22618  cnlnadji 22617  cnlnadjlem1 22608  nmopadjlei 22629
[Beran] p. 106Theorem 3.11(i)adjeq0 22632
[Beran] p. 106Theorem 3.11(v)nmopadji 22631
[Beran] p. 106Theorem 3.11(ii)adjmul 22633
[Beran] p. 106Theorem 3.11(iv)adjadj 22477
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22643  nmopcoadji 22642
[Beran] p. 106Theorem 3.11(iii)adjadd 22634
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22644
[Beran] p. 106Theorem 3.11(viii)adjcoi 22641  pjadj2coi 22745  pjadjcoi 22702
[Beran] p. 107Definitiondf-ch 21762  isch2 21764
[Beran] p. 107Remark 3.12choccl 21846  isch3 21782  occl 21844  ocsh 21823  shoccl 21845  shocsh 21824
[Beran] p. 107Remark 3.12(B)ococin 21948
[Beran] p. 108Theorem 3.13chintcl 21872
[Beran] p. 109Property (i)pjadj2 22728  pjadj3 22729  pjadji 22225  pjadjii 22214
[Beran] p. 109Property (ii)pjidmco 22722  pjidmcoi 22718  pjidmi 22213
[Beran] p. 110Definition of projector orderingpjordi 22714
[Beran] p. 111Remarkho0val 22291  pjch1 22210
[Beran] p. 111Definitiondf-hfmul 22275  df-hfsum 22274  df-hodif 22273  df-homul 22272  df-hosum 22271
[Beran] p. 111Lemma 4.4(i)pjo 22211
[Beran] p. 111Lemma 4.4(ii)pjch 22234  pjchi 21972
[Beran] p. 111Lemma 4.4(iii)pjoc2 21979  pjoc2i 21978
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22220
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22706  pjssmii 22221
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22705
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22704
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22709
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22707  pjssge0ii 22222
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22708  pjdifnormii 22223
[BourbakiEns] p. Proposition 8fcof1 5731  fcofo 5732
[BourbakiFVR] p. Definition 1isder 25075
[BourbakiTop1] p. Remarkxnegmnf 10504  xnegpnf 10503
[BourbakiTop1] p. Remark rexneg 10505
[BourbakiTop1] p. Theoremneiss 16809
[BourbakiTop1] p. Axiom GT'tgpsubcn 17736
[BourbakiTop1] p. Example 1snfil 17522
[BourbakiTop1] p. Example 2neifil 17538
[BourbakiTop1] p. Definitionistgp 17723
[BourbakiTop1] p. Propositioncnpco 16959  ishmeo 17413  neips 16813
[BourbakiTop1] p. Definition 1filintn0 17519
[BourbakiTop1] p. Proposition 9cnpflf2 17658
[BourbakiTop1] p. Theorem 1 (d)iscncl 16961
[BourbakiTop1] p. Proposition Vissnei2 16816
[BourbakiTop1] p. Definition C'''df-cmp 17077
[BourbakiTop1] p. Proposition Viiinnei 16825
[BourbakiTop1] p. Proposition Vivneissex 16827
[BourbakiTop1] p. Proposition Viiielnei 16811  ssnei 16810
[BourbakiTop1] p. Remark below def. 1filn0 17520
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17504
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17521
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27182  stoweid 27181
[BrosowskiDeutsh] p. 89Theorem for the non trivial casestoweidlem62 27180
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27119  stoweidlem10 27128  stoweidlem14 27132  stoweidlem15 27133  stoweidlem35 27153  stoweidlem36 27154  stoweidlem37 27155  stoweidlem38 27156  stoweidlem40 27158  stoweidlem41 27159  stoweidlem43 27161  stoweidlem44 27162  stoweidlem46 27164  stoweidlem5 27123  stoweidlem50 27168  stoweidlem52 27170  stoweidlem53 27171  stoweidlem55 27173  stoweidlem56 27174
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27141  stoweidlem24 27142  stoweidlem27 27145  stoweidlem28 27146  stoweidlem30 27148
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27163  stoweidlem49 27167  stoweidlem7 27125
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27149  stoweidlem39 27157  stoweidlem42 27160  stoweidlem48 27166  stoweidlem51 27169  stoweidlem54 27172  stoweidlem57 27175  stoweidlem58 27176
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27143
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27152
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27135
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27177
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27178
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27136
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27129  stoweidlem26 27144
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27131
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27179
[ChoquetDD] p. 2Definition of mappingdf-mpt 4053
[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 20781  ex-natded5.2 20780
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 20784  ex-natded5.3 20783
[Clemente] p. 18Theorem 5.5ex-natded5.5 20786
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 20788  ex-natded5.7 20787
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 20790  ex-natded5.8 20789
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 20792  ex-natded5.13 20791
[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 20793
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 20794
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 20796  ex-natded9.26 20795
[Cohen] p. 301Remarkrelogoprlem 19907
[Cohen] p. 301Property 2relogmul 19908  relogmuld 19939
[Cohen] p. 301Property 3relogdiv 19909  relogdivd 19940
[Cohen] p. 301Property 4relogexp 19912
[Cohen] p. 301Property 1alog1 19902
[Cohen] p. 301Property 1bloge 19903
[Cohn] p. 81Section II.5acsdomd 14247  acsinfd 14246  acsinfdimd 14248  acsmap2d 14245  acsmapd 14244
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10932
[Crawley] p. 1Definition of posetdf-poset 14043
[Crawley] p. 107Theorem 13.2hlsupr 28825
[Crawley] p. 110Theorem 13.3arglem1N 29629  dalaw 29325
[Crawley] p. 111Theorem 13.4hlathil 31404
[Crawley] p. 111Definition of set Wdf-watsN 29429
[Crawley] p. 111Definition of dilationdf-dilN 29545  df-ldil 29543  isldil 29549
[Crawley] p. 111Definition of translationdf-ltrn 29544  df-trnN 29546  isltrn 29558  ltrnu 29560
[Crawley] p. 112Lemma Acdlema1N 29230  cdlema2N 29231  exatleN 28843
[Crawley] p. 112Lemma B1cvrat 28915  cdlemb 29233  cdlemb2 29480  cdlemb3 30045  idltrn 29589  l1cvat 28495  lhpat 29482  lhpat2 29484  lshpat 28496  ltrnel 29578  ltrnmw 29590
[Crawley] p. 112Lemma Ccdlemc1 29630  cdlemc2 29631  ltrnnidn 29613  trlat 29608  trljat1 29605  trljat2 29606  trljat3 29607  trlne 29624  trlnidat 29612  trlnle 29625
[Crawley] p. 112Definition of automorphismdf-pautN 29430
[Crawley] p. 113Lemma Ccdlemc 29636  cdlemc3 29632  cdlemc4 29633
[Crawley] p. 113Lemma Dcdlemd 29646  cdlemd1 29637  cdlemd2 29638  cdlemd3 29639  cdlemd4 29640  cdlemd5 29641  cdlemd6 29642  cdlemd7 29643  cdlemd8 29644  cdlemd9 29645  cdleme31sde 29824  cdleme31se 29821  cdleme31se2 29822  cdleme31snd 29825  cdleme32a 29880  cdleme32b 29881  cdleme32c 29882  cdleme32d 29883  cdleme32e 29884  cdleme32f 29885  cdleme32fva 29876  cdleme32fva1 29877  cdleme32fvcl 29879  cdleme32le 29886  cdleme48fv 29938  cdleme4gfv 29946  cdleme50eq 29980  cdleme50f 29981  cdleme50f1 29982  cdleme50f1o 29985  cdleme50laut 29986  cdleme50ldil 29987  cdleme50lebi 29979  cdleme50rn 29984  cdleme50rnlem 29983  cdlemeg49le 29950  cdlemeg49lebilem 29978
[Crawley] p. 113Lemma Ecdleme 29999  cdleme00a 29648  cdleme01N 29660  cdleme02N 29661  cdleme0a 29650  cdleme0aa 29649  cdleme0b 29651  cdleme0c 29652  cdleme0cp 29653  cdleme0cq 29654  cdleme0dN 29655  cdleme0e 29656  cdleme0ex1N 29662  cdleme0ex2N 29663  cdleme0fN 29657  cdleme0gN 29658  cdleme0moN 29664  cdleme1 29666  cdleme10 29693  cdleme10tN 29697  cdleme11 29709  cdleme11a 29699  cdleme11c 29700  cdleme11dN 29701  cdleme11e 29702  cdleme11fN 29703  cdleme11g 29704  cdleme11h 29705  cdleme11j 29706  cdleme11k 29707  cdleme11l 29708  cdleme12 29710  cdleme13 29711  cdleme14 29712  cdleme15 29717  cdleme15a 29713  cdleme15b 29714  cdleme15c 29715  cdleme15d 29716  cdleme16 29724  cdleme16aN 29698  cdleme16b 29718  cdleme16c 29719  cdleme16d 29720  cdleme16e 29721  cdleme16f 29722  cdleme16g 29723  cdleme19a 29742  cdleme19b 29743  cdleme19c 29744  cdleme19d 29745  cdleme19e 29746  cdleme19f 29747  cdleme1b 29665  cdleme2 29667  cdleme20aN 29748  cdleme20bN 29749  cdleme20c 29750  cdleme20d 29751  cdleme20e 29752  cdleme20f 29753  cdleme20g 29754  cdleme20h 29755  cdleme20i 29756  cdleme20j 29757  cdleme20k 29758  cdleme20l 29761  cdleme20l1 29759  cdleme20l2 29760  cdleme20m 29762  cdleme20y 29741  cdleme20zN 29740  cdleme21 29776  cdleme21d 29769  cdleme21e 29770  cdleme22a 29779  cdleme22aa 29778  cdleme22b 29780  cdleme22cN 29781  cdleme22d 29782  cdleme22e 29783  cdleme22eALTN 29784  cdleme22f 29785  cdleme22f2 29786  cdleme22g 29787  cdleme23a 29788  cdleme23b 29789  cdleme23c 29790  cdleme26e 29798  cdleme26eALTN 29800  cdleme26ee 29799  cdleme26f 29802  cdleme26f2 29804  cdleme26f2ALTN 29803  cdleme26fALTN 29801  cdleme27N 29808  cdleme27a 29806  cdleme27cl 29805  cdleme28c 29811  cdleme3 29676  cdleme30a 29817  cdleme31fv 29829  cdleme31fv1 29830  cdleme31fv1s 29831  cdleme31fv2 29832  cdleme31id 29833  cdleme31sc 29823  cdleme31sdnN 29826  cdleme31sn 29819  cdleme31sn1 29820  cdleme31sn1c 29827  cdleme31sn2 29828  cdleme31so 29818  cdleme35a 29887  cdleme35b 29889  cdleme35c 29890  cdleme35d 29891  cdleme35e 29892  cdleme35f 29893  cdleme35fnpq 29888  cdleme35g 29894  cdleme35h 29895  cdleme35h2 29896  cdleme35sn2aw 29897  cdleme35sn3a 29898  cdleme36a 29899  cdleme36m 29900  cdleme37m 29901  cdleme38m 29902  cdleme38n 29903  cdleme39a 29904  cdleme39n 29905  cdleme3b 29668  cdleme3c 29669  cdleme3d 29670  cdleme3e 29671  cdleme3fN 29672  cdleme3fa 29675  cdleme3g 29673  cdleme3h 29674  cdleme4 29677  cdleme40m 29906  cdleme40n 29907  cdleme40v 29908  cdleme40w 29909  cdleme41fva11 29916  cdleme41sn3aw 29913  cdleme41sn4aw 29914  cdleme41snaw 29915  cdleme42a 29910  cdleme42b 29917  cdleme42c 29911  cdleme42d 29912  cdleme42e 29918  cdleme42f 29919  cdleme42g 29920  cdleme42h 29921  cdleme42i 29922  cdleme42k 29923  cdleme42ke 29924  cdleme42keg 29925  cdleme42mN 29926  cdleme42mgN 29927  cdleme43aN 29928  cdleme43bN 29929  cdleme43cN 29930  cdleme43dN 29931  cdleme5 29679  cdleme50ex 29998  cdleme50ltrn 29996  cdleme51finvN 29995  cdleme51finvfvN 29994  cdleme51finvtrN 29997  cdleme6 29680  cdleme7 29688  cdleme7a 29682  cdleme7aa 29681  cdleme7b 29683  cdleme7c 29684  cdleme7d 29685  cdleme7e 29686  cdleme7ga 29687  cdleme8 29689  cdleme8tN 29694  cdleme9 29692  cdleme9a 29690  cdleme9b 29691  cdleme9tN 29696  cdleme9taN 29695  cdlemeda 29737  cdlemedb 29736  cdlemednpq 29738  cdlemednuN 29739  cdlemefr27cl 29842  cdlemefr32fva1 29849  cdlemefr32fvaN 29848  cdlemefrs32fva 29839  cdlemefrs32fva1 29840  cdlemefs27cl 29852  cdlemefs32fva1 29862  cdlemefs32fvaN 29861  cdlemesner 29735  cdlemeulpq 29659
[Crawley] p. 114Lemma E4atex 29515  4atexlem7 29514  cdleme0nex 29729  cdleme17a 29725  cdleme17c 29727  cdleme17d 29937  cdleme17d1 29728  cdleme17d2 29934  cdleme18a 29730  cdleme18b 29731  cdleme18c 29732  cdleme18d 29734  cdleme4a 29678
[Crawley] p. 115Lemma Ecdleme21a 29764  cdleme21at 29767  cdleme21b 29765  cdleme21c 29766  cdleme21ct 29768  cdleme21f 29771  cdleme21g 29772  cdleme21h 29773  cdleme21i 29774  cdleme22gb 29733
[Crawley] p. 116Lemma Fcdlemf 30002  cdlemf1 30000  cdlemf2 30001
[Crawley] p. 116Lemma Gcdlemftr1 30006  cdlemg16 30096  cdlemg28 30143  cdlemg28a 30132  cdlemg28b 30142  cdlemg3a 30036  cdlemg42 30168  cdlemg43 30169  cdlemg44 30172  cdlemg44a 30170  cdlemg46 30174  cdlemg47 30175  cdlemg9 30073  ltrnco 30158  ltrncom 30177  tgrpabl 30190  trlco 30166
[Crawley] p. 116Definition of Gdf-tgrp 30182
[Crawley] p. 117Lemma Gcdlemg17 30116  cdlemg17b 30101
[Crawley] p. 117Definition of Edf-edring-rN 30195  df-edring 30196
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30199
[Crawley] p. 118Remarktendopltp 30219
[Crawley] p. 118Lemma Hcdlemh 30256  cdlemh1 30254  cdlemh2 30255
[Crawley] p. 118Lemma Icdlemi 30259  cdlemi1 30257  cdlemi2 30258
[Crawley] p. 118Lemma Jcdlemj1 30260  cdlemj2 30261  cdlemj3 30262  tendocan 30263
[Crawley] p. 118Lemma Kcdlemk 30413  cdlemk1 30270  cdlemk10 30282  cdlemk11 30288  cdlemk11t 30385  cdlemk11ta 30368  cdlemk11tb 30370  cdlemk11tc 30384  cdlemk11u-2N 30328  cdlemk11u 30310  cdlemk12 30289  cdlemk12u-2N 30329  cdlemk12u 30311  cdlemk13-2N 30315  cdlemk13 30291  cdlemk14-2N 30317  cdlemk14 30293  cdlemk15-2N 30318  cdlemk15 30294  cdlemk16-2N 30319  cdlemk16 30296  cdlemk16a 30295  cdlemk17-2N 30320  cdlemk17 30297  cdlemk18-2N 30325  cdlemk18-3N 30339  cdlemk18 30307  cdlemk19-2N 30326  cdlemk19 30308  cdlemk19u 30409  cdlemk1u 30298  cdlemk2 30271  cdlemk20-2N 30331  cdlemk20 30313  cdlemk21-2N 30330  cdlemk21N 30312  cdlemk22-3 30340  cdlemk22 30332  cdlemk23-3 30341  cdlemk24-3 30342  cdlemk25-3 30343  cdlemk26-3 30345  cdlemk26b-3 30344  cdlemk27-3 30346  cdlemk28-3 30347  cdlemk29-3 30350  cdlemk3 30272  cdlemk30 30333  cdlemk31 30335  cdlemk32 30336  cdlemk33N 30348  cdlemk34 30349  cdlemk35 30351  cdlemk36 30352  cdlemk37 30353  cdlemk38 30354  cdlemk39 30355  cdlemk39u 30407  cdlemk4 30273  cdlemk41 30359  cdlemk42 30380  cdlemk42yN 30383  cdlemk43N 30402  cdlemk45 30386  cdlemk46 30387  cdlemk47 30388  cdlemk48 30389  cdlemk49 30390  cdlemk5 30275  cdlemk50 30391  cdlemk51 30392  cdlemk52 30393  cdlemk53 30396  cdlemk54 30397  cdlemk55 30400  cdlemk55u 30405  cdlemk56 30410  cdlemk5a 30274  cdlemk5auN 30299  cdlemk5u 30300  cdlemk6 30276  cdlemk6u 30301  cdlemk7 30287  cdlemk7u-2N 30327  cdlemk7u 30309  cdlemk8 30277  cdlemk9 30278  cdlemk9bN 30279  cdlemki 30280  cdlemkid 30375  cdlemkj-2N 30321  cdlemkj 30302  cdlemksat 30285  cdlemksel 30284  cdlemksv 30283  cdlemksv2 30286  cdlemkuat 30305  cdlemkuel-2N 30323  cdlemkuel-3 30337  cdlemkuel 30304  cdlemkuv-2N 30322  cdlemkuv2-2 30324  cdlemkuv2-3N 30338  cdlemkuv2 30306  cdlemkuvN 30303  cdlemkvcl 30281  cdlemky 30365  cdlemkyyN 30401  tendoex 30414
[Crawley] p. 120Remarkdva1dim 30424
[Crawley] p. 120Lemma Lcdleml1N 30415  cdleml2N 30416  cdleml3N 30417  cdleml4N 30418  cdleml5N 30419  cdleml6 30420  cdleml7 30421  cdleml8 30422  cdleml9 30423  dia1dim 30501
[Crawley] p. 120Lemma Mdia11N 30488  diaf11N 30489  dialss 30486  diaord 30487  dibf11N 30601  djajN 30577
[Crawley] p. 120Definition of isomorphism mapdiaval 30472
[Crawley] p. 121Lemma Mcdlemm10N 30558  dia2dimlem1 30504  dia2dimlem2 30505  dia2dimlem3 30506  dia2dimlem4 30507  dia2dimlem5 30508  diaf1oN 30570  diarnN 30569  dvheveccl 30552  dvhopN 30556
[Crawley] p. 121Lemma Ncdlemn 30652  cdlemn10 30646  cdlemn11 30651  cdlemn11a 30647  cdlemn11b 30648  cdlemn11c 30649  cdlemn11pre 30650  cdlemn2 30635  cdlemn2a 30636  cdlemn3 30637  cdlemn4 30638  cdlemn4a 30639  cdlemn5 30641  cdlemn5pre 30640  cdlemn6 30642  cdlemn7 30643  cdlemn8 30644  cdlemn9 30645  diclspsn 30634
[Crawley] p. 121Definition of phi(q)df-dic 30613
[Crawley] p. 122Lemma Ndih11 30705  dihf11 30707  dihjust 30657  dihjustlem 30656  dihord 30704  dihord1 30658  dihord10 30663  dihord11b 30662  dihord11c 30664  dihord2 30667  dihord2a 30659  dihord2b 30660  dihord2cN 30661  dihord2pre 30665  dihord2pre2 30666  dihordlem6 30653  dihordlem7 30654  dihordlem7b 30655
[Crawley] p. 122Definition of isomorphism mapdihffval 30670  dihfval 30671  dihval 30672
[Eisenberg] p. 67Definition 5.3df-dif 3130
[Eisenberg] p. 82Definition 6.3dfom3 7316
[Eisenberg] p. 125Definition 8.21df-map 6742
[Eisenberg] p. 216Example 13.2(4)omenps 7323
[Eisenberg] p. 310Theorem 19.8cardprc 7581
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8145
[Enderton] p. 18Axiom of Empty Setaxnul 4122
[Enderton] p. 19Definitiondf-tp 3622
[Enderton] p. 26Exercise 5unissb 3831
[Enderton] p. 26Exercise 10pwel 4197
[Enderton] p. 28Exercise 7(b)pwun 4274
[Enderton] p. 30Theorem "Distributive laws"iinin1 3947  iinin2 3946  iinun2 3942  iunin1 3941  iunin2 3940
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3945  iundif2 3943
[Enderton] p. 32Exercise 20unineq 3394
[Enderton] p. 33Exercise 23iinuni 3959
[Enderton] p. 33Exercise 25iununi 3960
[Enderton] p. 33Exercise 24(a)iinpw 3964
[Enderton] p. 33Exercise 24(b)iunpw 4542  iunpwss 3965
[Enderton] p. 36Definitionopthwiener 4240
[Enderton] p. 38Exercise 6(a)unipw 4196
[Enderton] p. 38Exercise 6(b)pwuni 4178
[Enderton] p. 41Lemma 3Dopeluu 4498  rnex 4930  rnexg 4928
[Enderton] p. 41Exercise 8dmuni 4876  rnuni 5080
[Enderton] p. 42Definition of a functiondffun7 5219  dffun8 5220
[Enderton] p. 43Definition of function valuefunfv2 5521
[Enderton] p. 43Definition of single-rootedfuncnv 5248
[Enderton] p. 44Definition (d)dfima2 5002  dfima3 5003
[Enderton] p. 47Theorem 3Hfvco2 5528
[Enderton] p. 49Axiom of Choice (first form)ac7 8068  ac7g 8069  df-ac 7711  dfac2 7725  dfac2a 7724  dfac3 7716  dfac7 7726
[Enderton] p. 50Theorem 3K(a)imauni 5706
[Enderton] p. 52Definitiondf-map 6742
[Enderton] p. 53Exercise 21coass 5178
[Enderton] p. 53Exercise 27dmco 5168
[Enderton] p. 53Exercise 14(a)funin 5257
[Enderton] p. 53Exercise 22(a)imass2 5037
[Enderton] p. 54Remarkixpf 6806  ixpssmap 6818
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6786
[Enderton] p. 55Axiom of Choice (second form)ac9 8078  ac9s 8088
[Enderton] p. 56Theorem 3Merref 6648
[Enderton] p. 57Lemma 3Nerthi 6674
[Enderton] p. 57Definitiondf-ec 6630
[Enderton] p. 58Definitiondf-qs 6634
[Enderton] p. 60Theorem 3Qth3q 6735  th3qcor 6734  th3qlem1 6732  th3qlem2 6733
[Enderton] p. 61Exercise 35df-ec 6630
[Enderton] p. 65Exercise 56(a)dmun 4873
[Enderton] p. 68Definition of successordf-suc 4370
[Enderton] p. 71Definitiondf-tr 4088  dftr4 4092
[Enderton] p. 72Theorem 4Eunisuc 4440
[Enderton] p. 73Exercise 6unisuc 4440
[Enderton] p. 73Exercise 5(a)truni 4101
[Enderton] p. 73Exercise 5(b)trint 4102  trintALT 27790
[Enderton] p. 79Theorem 4I(A1)nna0 6570
[Enderton] p. 79Theorem 4I(A2)nnasuc 6572  onasuc 6495
[Enderton] p. 79Definition of operation valuedf-ov 5795
[Enderton] p. 80Theorem 4J(A1)nnm0 6571
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6573  onmsuc 6496
[Enderton] p. 81Theorem 4K(1)nnaass 6588
[Enderton] p. 81Theorem 4K(2)nna0r 6575  nnacom 6583
[Enderton] p. 81Theorem 4K(3)nndi 6589
[Enderton] p. 81Theorem 4K(4)nnmass 6590
[Enderton] p. 81Theorem 4K(5)nnmcom 6592
[Enderton] p. 82Exercise 16nnm0r 6576  nnmsucr 6591
[Enderton] p. 88Exercise 23nnaordex 6604
[Enderton] p. 129Definitiondf-en 6832
[Enderton] p. 132Theorem 6B(b)canth 6260
[Enderton] p. 133Exercise 1xpomen 7611
[Enderton] p. 133Exercise 2qnnen 12455
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7013
[Enderton] p. 135Corollary 6Cphp3 7015
[Enderton] p. 136Corollary 6Enneneq 7012
[Enderton] p. 136Corollary 6D(a)pssinf 7041
[Enderton] p. 136Corollary 6D(b)ominf 7043
[Enderton] p. 137Lemma 6Fpssnn 7049
[Enderton] p. 138Corollary 6Gssfi 7051
[Enderton] p. 139Theorem 6H(c)mapen 6993
[Enderton] p. 142Theorem 6I(3)xpcdaen 7777
[Enderton] p. 142Theorem 6I(4)mapcdaen 7778
[Enderton] p. 143Theorem 6Jcda0en 7773  cda1en 7769
[Enderton] p. 144Exercise 13iunfi 7112  unifi 7113  unifi2 7114
[Enderton] p. 144Corollary 6Kundif2 3505  unfi 7092  unfi2 7094
[Enderton] p. 145Figure 38ffoss 5443
[Enderton] p. 145Definitiondf-dom 6833
[Enderton] p. 146Example 1domen 6843  domeng 6844
[Enderton] p. 146Example 3nndomo 7022  nnsdom 7322  nnsdomg 7084
[Enderton] p. 149Theorem 6L(a)cdadom2 7781
[Enderton] p. 149Theorem 6L(c)mapdom1 6994  xpdom1 6929  xpdom1g 6927  xpdom2g 6926
[Enderton] p. 149Theorem 6L(d)mapdom2 7000
[Enderton] p. 151Theorem 6Mzorn 8102  zorng 8099
[Enderton] p. 151Theorem 6M(4)ac8 8087  dfac5 7723
[Enderton] p. 159Theorem 6Qunictb 8165
[Enderton] p. 164Exampleinfdif 7803
[Enderton] p. 168Definitiondf-po 4286
[Enderton] p. 192Theorem 7M(a)oneli 4472
[Enderton] p. 192Theorem 7M(b)ontr1 4410
[Enderton] p. 192Theorem 7M(c)onirri 4471
[Enderton] p. 193Corollary 7N(b)0elon 4417
[Enderton] p. 193Corollary 7N(c)onsuci 4601
[Enderton] p. 193Corollary 7N(d)ssonunii 4551
[Enderton] p. 194Remarkonprc 4548
[Enderton] p. 194Exercise 16suc11 4468
[Enderton] p. 197Definitiondf-card 7540
[Enderton] p. 197Theorem 7Pcarden 8141
[Enderton] p. 200Exercise 25tfis 4617
[Enderton] p. 202Lemma 7Tr1tr 7416
[Enderton] p. 202Definitiondf-r1 7404
[Enderton] p. 202Theorem 7Qr1val1 7426
[Enderton] p. 204Theorem 7V(b)rankval4 7507
[Enderton] p. 206Theorem 7X(b)en2lp 7285
[Enderton] p. 207Exercise 30rankpr 7497  rankprb 7491  rankpw 7483  rankpwi 7463  rankuniss 7506
[Enderton] p. 207Exercise 34opthreg 7287
[Enderton] p. 208Exercise 35suc11reg 7288
[Enderton] p. 212Definition of alephalephval3 7705
[Enderton] p. 213Theorem 8A(a)alephord2 7671
[Enderton] p. 213Theorem 8A(b)cardalephex 7685
[Enderton] p. 218Theorem Schema 8Eonfununi 6326
[Enderton] p. 222Definition of kardkarden 7533  kardex 7532
[Enderton] p. 238Theorem 8Roeoa 6563
[Enderton] p. 238Theorem 8Soeoe 6565
[Enderton] p. 240Exercise 25oarec 6528
[Enderton] p. 257Definition of cofinalitycflm 7844
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13507
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13453
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14243  mrieqv2d 13504  mrieqvd 13503
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13508
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13513  mreexexlem2d 13510
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14249  mreexfidimd 13515
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18857
[Fremlin5] p. 213Lemma 565Cauniioovol 18897
[Fremlin5] p. 214Lemma 565Cauniioombl 18907
[FreydScedrov] p. 283Axiom of Infinityax-inf 7307  inf1 7291  inf2 7292
[Gleason] p. 117Proposition 9-2.1df-enq 8503  enqer 8513
[Gleason] p. 117Proposition 9-2.2df-1nq 8508  df-nq 8504
[Gleason] p. 117Proposition 9-2.3df-plpq 8500  df-plq 8506
[Gleason] p. 119Proposition 9-2.4caovmo 5991  df-mpq 8501  df-mq 8507
[Gleason] p. 119Proposition 9-2.5df-rq 8509
[Gleason] p. 119Proposition 9-2.6ltexnq 8567
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8568  ltbtwnnq 8570
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8563
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8564
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8571
[Gleason] p. 121Definition 9-3.1df-np 8573
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8585
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8587
[Gleason] p. 122Definitiondf-1p 8574
[Gleason] p. 122Remark (1)prub 8586
[Gleason] p. 122Lemma 9-3.4prlem934 8625
[Gleason] p. 122Proposition 9-3.2df-ltp 8577
[Gleason] p. 122Proposition 9-3.3ltsopr 8624  psslinpr 8623  supexpr 8646  suplem1pr 8644  suplem2pr 8645
[Gleason] p. 123Proposition 9-3.5addclpr 8610  addclprlem1 8608  addclprlem2 8609  df-plp 8575
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8614
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8613
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8626
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8635  ltexprlem1 8628  ltexprlem2 8629  ltexprlem3 8630  ltexprlem4 8631  ltexprlem5 8632  ltexprlem6 8633  ltexprlem7 8634
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8637  ltaprlem 8636
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8638
[Gleason] p. 124Lemma 9-3.6prlem936 8639
[Gleason] p. 124Proposition 9-3.7df-mp 8576  mulclpr 8612  mulclprlem 8611  reclem2pr 8640
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8621
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8616
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8615
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8620
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8643  reclem3pr 8641  reclem4pr 8642
[Gleason] p. 126Proposition 9-4.1df-enr 8649  df-mpr 8648  df-plpr 8647  enrer 8658
[Gleason] p. 126Proposition 9-4.2df-0r 8654  df-1r 8655  df-nr 8650
[Gleason] p. 126Proposition 9-4.3df-mr 8652  df-plr 8651  negexsr 8692  recexsr 8697  recexsrlem 8693
[Gleason] p. 127Proposition 9-4.4df-ltr 8653
[Gleason] p. 130Proposition 10-1.3creui 9709  creur 9708  cru 9706
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8778  axcnre 8754
[Gleason] p. 132Definition 10-3.1crim 11566  crimd 11683  crimi 11644  crre 11565  crred 11682  crrei 11643
[Gleason] p. 132Definition 10-3.2remim 11568  remimd 11649
[Gleason] p. 133Definition 10.36absval2 11735  absval2d 11893  absval2i 11846
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11592  cjaddd 11671  cjaddi 11639
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11593  cjmuld 11672  cjmuli 11640
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11591  cjcjd 11650  cjcji 11622
[Gleason] p. 133Proposition 10-3.4(f)cjre 11590  cjreb 11574  cjrebd 11653  cjrebi 11625  cjred 11677  rere 11573  rereb 11571  rerebd 11652  rerebi 11624  rered 11675
[Gleason] p. 133Proposition 10-3.4(h)addcj 11599  addcjd 11663  addcji 11634
[Gleason] p. 133Proposition 10-3.7(a)absval 11689
[Gleason] p. 133Proposition 10-3.7(b)abscj 11730  abscjd 11898  abscji 11850
[Gleason] p. 133Proposition 10-3.7(c)abs00 11740  abs00d 11894  abs00i 11847  absne0d 11895
[Gleason] p. 133Proposition 10-3.7(d)releabs 11771  releabsd 11899  releabsi 11851
[Gleason] p. 133Proposition 10-3.7(f)absmul 11745  absmuld 11902  absmuli 11853
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11733  sqabsaddi 11854
[Gleason] p. 133Proposition 10-3.7(h)abstri 11780  abstrid 11904  abstrii 11857
[Gleason] p. 134Definition 10-4.1df-exp 11072  exp0 11075  expp1 11077  expp1d 11213
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 19989  cxpaddd 20027  expadd 11111  expaddd 11214  expaddz 11113
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 19998  cxpmuld 20044  expmul 11114  expmuld 11215  expmulz 11115
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 19995  mulcxpd 20038  mulexp 11108  mulexpd 11227  mulexpz 11109
[Gleason] p. 140Exercise 1znnen 12454
[Gleason] p. 141Definition 11-2.1fzval 10751
[Gleason] p. 168Proposition 12-2.1(a)climadd 12071  rlimadd 12082  rlimdiv 12085
[Gleason] p. 168Proposition 12-2.1(b)climsub 12073  rlimsub 12083
[Gleason] p. 168Proposition 12-2.1(c)climmul 12072  rlimmul 12084
[Gleason] p. 171Corollary 12-2.2climmulc2 12076
[Gleason] p. 172Corollary 12-2.5climrecl 12023
[Gleason] p. 172Proposition 12-2.4(c)climabs 12043  climcj 12044  climim 12046  climre 12045  rlimabs 12048  rlimcj 12049  rlimim 12051  rlimre 12050
[Gleason] p. 173Definition 12-3.1df-ltxr 8840  df-xr 8839  ltxr 10425
[Gleason] p. 175Definition 12-4.1df-limsup 11911  limsupval 11914
[Gleason] p. 180Theorem 12-5.1climsup 12109
[Gleason] p. 180Theorem 12-5.3caucvg 12117  caucvgb 12118  caucvgr 12114  climcau 12110
[Gleason] p. 182Exercise 3cvgcmp 12240
[Gleason] p. 182Exercise 4cvgrat 12302
[Gleason] p. 195Theorem 13-2.12abs1m 11785
[Gleason] p. 217Lemma 13-4.1btwnzge0 10920
[Gleason] p. 223Definition 14-1.1df-met 16337
[Gleason] p. 223Definition 14-1.1(a)met0 17871  xmet0 17870
[Gleason] p. 223Definition 14-1.1(b)metgt0 17886
[Gleason] p. 223Definition 14-1.1(c)metsym 17877
[Gleason] p. 223Definition 14-1.1(d)mettri 17879  mstri 17978  xmettri 17878  xmstri 17977
[Gleason] p. 225Definition 14-1.5xpsmet 17909
[Gleason] p. 230Proposition 14-2.6txlm 17305
[Gleason] p. 240Theorem 14-4.3metcnp4 18698
[Gleason] p. 240Proposition 14-4.2metcnp3 18049
[Gleason] p. 243Proposition 14-4.16addcn 18332  addcn2 12033  mulcn 18334  mulcn2 12035  subcn 18333  subcn2 12034
[Gleason] p. 295Remarkbcval3 11286  bcval4 11287
[Gleason] p. 295Equation 2bcpasc 11300
[Gleason] p. 295Definition of binomial coefficientbcval 11284  df-bc 11283
[Gleason] p. 296Remarkbcn0 11290  bcnn 11291
[Gleason] p. 296Theorem 15-2.8binom 12254
[Gleason] p. 308Equation 2ef0 12335
[Gleason] p. 308Equation 3efcj 12336
[Gleason] p. 309Corollary 15-4.3efne0 12340
[Gleason] p. 309Corollary 15-4.4efexp 12344
[Gleason] p. 310Equation 14sinadd 12407
[Gleason] p. 310Equation 15cosadd 12408
[Gleason] p. 311Equation 17sincossq 12419
[Gleason] p. 311Equation 18cosbnd 12424  sinbnd 12423
[Gleason] p. 311Lemma 15-4.7sqeqor 11184  sqeqori 11182
[Gleason] p. 311Definition of pidf-pi 12317
[Godowski] p. 730Equation SFgoeqi 22814
[GodowskiGreechie] p. 249Equation IV3oai 22208
[Gratzer] p. 23Section 0.6df-mre 13451
[Gratzer] p. 27Section 0.6df-mri 13453
[Halmos] p. 31Theorem 17.3riesz1 22606  riesz2 22607
[Halmos] p. 41Definition of Hermitianhmopadj2 22482
[Halmos] p. 42Definition of projector orderingpjordi 22714
[Halmos] p. 43Theorem 26.1elpjhmop 22726  elpjidm 22725  pjnmopi 22689
[Halmos] p. 44Remarkpjinormi 22227  pjinormii 22216
[Halmos] p. 44Theorem 26.2elpjch 22730  pjrn 22247  pjrni 22242  pjvec 22236
[Halmos] p. 44Theorem 26.3pjnorm2 22267
[Halmos] p. 44Theorem 26.4hmopidmpj 22695  hmopidmpji 22693
[Halmos] p. 45Theorem 27.1pjinvari 22732
[Halmos] p. 45Theorem 27.3pjoci 22721  pjocvec 22237
[Halmos] p. 45Theorem 27.4pjorthcoi 22710
[Halmos] p. 48Theorem 29.2pjssposi 22713
[Halmos] p. 48Theorem 29.3pjssdif1i 22716  pjssdif2i 22715
[Halmos] p. 50Definition of spectrumdf-spec 22396
[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 1536
[Hatcher] p. 25Definitiondf-phtpc 18453  df-phtpy 18432
[Hatcher] p. 26Definitiondf-pco 18466  df-pi1 18469
[Hatcher] p. 26Proposition 1.2phtpcer 18456
[Hatcher] p. 26Proposition 1.3pi1grp 18511
[Herstein] p. 54Exercise 28df-grpo 20819
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14461  grpoideu 20837  mndideu 14338
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14479  grpoinveu 20850
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14498  grpo2inv 20867
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14507  grpoinvop 20869
[Herstein] p. 57Exercise 1isgrp2d 20863  isgrp2i 20864
[Hitchcock] p. 5Rule A3mpto1 1528
[Hitchcock] p. 5Rule A4mpto2 1529
[Hitchcock] p. 5Rule A5mtp-xor 1530
[Holland] p. 1519Theorem 2sumdmdi 22961
[Holland] p. 1520Lemma 5cdj1i 22974  cdj3i 22982  cdj3lem1 22975  cdjreui 22973
[Holland] p. 1524Lemma 7mddmdin0i 22972
[Holland95] p. 13Theorem 3.6hlathil 31404
[Holland95] p. 14Line 15hgmapvs 31334
[Holland95] p. 14Line 16hdmaplkr 31356
[Holland95] p. 14Line 17hdmapellkr 31357
[Holland95] p. 14Line 19hdmapglnm2 31354
[Holland95] p. 14Line 20hdmapip0com 31360
[Holland95] p. 14Theorem 3.6hdmapevec2 31279
[Holland95] p. 14Lines 24 and 25hdmapoc 31374
[Holland95] p. 204Definition of involutiondf-srng 15574
[Holland95] p. 212Definition of subspacedf-psubsp 28942
[Holland95] p. 214Lemma 3.3lclkrlem2v 30968
[Holland95] p. 214Definition 3.2df-lpolN 30921
[Holland95] p. 214Definition of nonsingularpnonsingN 29372
[Holland95] p. 215Lemma 3.3(1)dihoml4 30817  poml4N 29392
[Holland95] p. 215Lemma 3.3(2)dochexmid 30908  pexmidALTN 29417  pexmidN 29408
[Holland95] p. 218Theorem 3.6lclkr 30973
[Holland95] p. 218Definition of dual vector spacedf-ldual 28564  ldualset 28565
[Holland95] p. 222Item 1df-lines 28940  df-pointsN 28941
[Holland95] p. 222Item 2df-polarityN 29342
[Holland95] p. 223Remarkispsubcl2N 29386  omllaw4 28686  pol1N 29349  polcon3N 29356
[Holland95] p. 223Definitiondf-psubclN 29374
[Holland95] p. 223Equation for polaritypolval2N 29345
[Hughes] p. 44Equation 1.21bax-his3 21624
[Hughes] p. 47Definition of projection operatordfpjop 22723
[Hughes] p. 49Equation 1.30eighmre 22504  eigre 22376  eigrei 22375
[Hughes] p. 49Equation 1.31eighmorth 22505  eigorth 22379  eigorthi 22378
[Hughes] p. 137Remark (ii)eigposi 22377
[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 1618  cvjust 2253
[Jech] p. 42Lemma 6.1alephexp1 8169
[Jech] p. 42Equation 6.1alephadd 8167  alephmul 8168
[Jech] p. 43Lemma 6.2infmap 8166  infmap2 7812
[Jech] p. 71Lemma 9.3jech9.3 7454
[Jech] p. 72Equation 9.3scott0 7524  scottex 7523
[Jech] p. 72Exercise 9.1rankval4 7507
[Jech] p. 72Scheme "Collection Principle"cp 7529
[Jech] p. 78Definition implied by the footnoteopthprc 4724
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26368
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26464
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26465
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26380
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26384
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26385  rmyp1 26386
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26387  rmym1 26388
[JonesMatijasevic] p. 695Equation 2.11rmx0 26378  rmx1 26379  rmxluc 26389
[JonesMatijasevic] p. 695Equation 2.12rmy0 26382  rmy1 26383  rmyluc 26390
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26392
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26393
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26415  jm2.17b 26416  jm2.17c 26417
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26454
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26458
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26449
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26418  jm2.24nn 26414
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26463
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26469  rmygeid 26419
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26481
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1684
[KalishMontague] p. 81Schemes B4 through B8equidK 28235
[KalishMontague] p. 85Lemma 2equidK 28235
[KalishMontague] p. 85Lemma 3equcomiK 28236
[KalishMontague] p. 85Theorem 1equidK 28235
[KalishMontague] p. 86Lemma 5albiiK 28242  alimdK 28243  alimdvK 28244
[KalishMontague] p. 86Lemma 7cbvaliK 28259  cbvalivK 28260
[KalishMontague] p. 86Lemma 9ax4wK 28252  ax4wfK 28251  equidK 28235
[KalishMontague] p. 87Lemma 8a4imK 28249  a4imvK 28250
[Kalmbach] p. 14Definition of latticechabs1 22056  chabs1i 22058  chabs2 22057  chabs2i 22059  chjass 22073  chjassi 22026  latabs1 14156  latabs2 14157
[Kalmbach] p. 15Definition of atomdf-at 22879  ela 22880
[Kalmbach] p. 15Definition of coverscvbr2 22824  cvrval2 28714
[Kalmbach] p. 16Definitiondf-ol 28618  df-oml 28619
[Kalmbach] p. 20Definition of commutescmbr 22124  cmbri 22130  cmtvalN 28651  df-cm 22123  df-cmtN 28617
[Kalmbach] p. 22Remarkomllaw5N 28687  pjoml5 22153  pjoml5i 22128
[Kalmbach] p. 22Definitionpjoml2 22151  pjoml2i 22125
[Kalmbach] p. 22Theorem 2(v)cmcm 22154  cmcmi 22132  cmcmii 22137  cmtcomN 28689
[Kalmbach] p. 22Theorem 2(ii)omllaw3 28685  omlsi 21944  pjoml 21976  pjomli 21975
[Kalmbach] p. 22Definition of OML lawomllaw2N 28684
[Kalmbach] p. 23Remarkcmbr2i 22136  cmcm3 22155  cmcm3i 22134  cmcm3ii 22139  cmcm4i 22135  cmt3N 28691  cmt4N 28692  cmtbr2N 28693
[Kalmbach] p. 23Lemma 3cmbr3 22148  cmbr3i 22140  cmtbr3N 28694
[Kalmbach] p. 25Theorem 5fh1 22158  fh1i 22161  fh2 22159  fh2i 22162  omlfh1N 28698
[Kalmbach] p. 65Remarkchjatom 22898  chslej 22038  chsleji 21998  shslej 21920  shsleji 21910
[Kalmbach] p. 65Proposition 1chocin 22035  chocini 21994  chsupcl 21880  chsupval2 21950  h0elch 21795  helch 21784  hsupval2 21949  ocin 21836  ococss 21833  shococss 21834
[Kalmbach] p. 65Definition of subspace sumshsval 21852
[Kalmbach] p. 66Remarkdf-pjh 21935  pjssmi 22706  pjssmii 22221
[Kalmbach] p. 67Lemma 3osum 22185  osumi 22182
[Kalmbach] p. 67Lemma 4pjci 22741
[Kalmbach] p. 103Exercise 6atmd2 22941
[Kalmbach] p. 103Exercise 12mdsl0 22851
[Kalmbach] p. 140Remarkhatomic 22901  hatomici 22900  hatomistici 22903
[Kalmbach] p. 140Proposition 1atlatmstc 28759
[Kalmbach] p. 140Proposition 1(i)atexch 22922  lsatexch 28483
[Kalmbach] p. 140Proposition 1(ii)chcv1 22896  cvlcvr1 28779  cvr1 28849
[Kalmbach] p. 140Proposition 1(iii)cvexch 22915  cvexchi 22910  cvrexch 28859
[Kalmbach] p. 149Remark 2chrelati 22905  hlrelat 28841  hlrelat5N 28840  lrelat 28454
[Kalmbach] p. 153Exercise 5lsmcv 15857  lsmsatcv 28450  spansncv 22193  spansncvi 22192
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 28469  spansncv2 22834
[Kalmbach] p. 266Definitiondf-st 22752
[Kalmbach2] p. 8Definition of adjointdf-adjh 22390
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8236  fpwwe2 8233
[KanamoriPincus] p. 416Corollary 1.3canth4 8237
[KanamoriPincus] p. 417Corollary 1.6canthp1 8244
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8239
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8241
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8254
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8258  gchxpidm 8259
[KanamoriPincus] p. 419Theorem 2.1gchacg 8262  gchhar 8261
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7810  unxpwdom 7271
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8264
[Kreyszig] p. 3Property M1metcl 17860  xmetcl 17859
[Kreyszig] p. 4Property M2meteq0 17867
[Kreyszig] p. 8Definition 1.1-8dscmet 18058
[Kreyszig] p. 12Equation 5conjmul 9445  muleqadd 9380
[Kreyszig] p. 18Definition 1.3-2mopnval 17947
[Kreyszig] p. 19Remarkmopntopon 17948
[Kreyszig] p. 19Theorem T1mopn0 18007  mopnm 17953
[Kreyszig] p. 19Theorem T2unimopn 18005
[Kreyszig] p. 19Definition of neighborhoodneibl 18010
[Kreyszig] p. 20Definition 1.3-3metcnp2 18051
[Kreyszig] p. 25Definition 1.4-1lmbr 16951  lmmbr 18647  lmmbr2 18648
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17071
[Kreyszig] p. 28Theorem 1.4-5lmcau 18701
[Kreyszig] p. 28Definition 1.4-3iscau 18665  iscmet2 18683
[Kreyszig] p. 30Theorem 1.4-7cmetss 18703
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17150  metelcls 18693
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18694  metcld2 18695
[Kreyszig] p. 51Equation 2clmvneg1 18552  lmodvneg1 15630  nvinv 21158  vcm 21088
[Kreyszig] p. 51Equation 1aclm0vs 18551  lmod0vs 15626  vc0 21086
[Kreyszig] p. 51Equation 1blmodvs0 15627  vcz 21087
[Kreyszig] p. 58Definition 2.2-1imsmet 21221
[Kreyszig] p. 59Equation 1imsdval 21216  imsdval2 21217
[Kreyszig] p. 63Problem 1nvnd 21218
[Kreyszig] p. 64Problem 2nvge0 21201  nvz 21196
[Kreyszig] p. 64Problem 3nvabs 21200
[Kreyszig] p. 91Definition 2.7-1isblo3i 21340
[Kreyszig] p. 92Equation 2df-nmoo 21284
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21346  blocni 21344
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21345
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18602  ipeq0 16505  ipz 21256
[Kreyszig] p. 135Problem 2pythi 21389
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21393
[Kreyszig] p. 144Equation 4supcvg 12277
[Kreyszig] p. 144Theorem 3.3-1minvec 18763  minveco 21424
[Kreyszig] p. 196Definition 3.9-1df-aj 21289
[Kreyszig] p. 247Theorem 4.7-2bcth 18714
[Kreyszig] p. 249Theorem 4.7-3ubth 21413
[Kreyszig] p. 470Definition of positive operator orderingleop 22664  leopg 22663
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22682
[Kreyszig] p. 525Theorem 10.1-1htth 21459
[Kunen] p. 10Axiom 0a9e 1817  axnul 4122
[Kunen] p. 11Axiom 3axnul 4122
[Kunen] p. 12Axiom 6zfrep6 5682
[Kunen] p. 24Definition 10.24mapval 6752  mapvalg 6750
[Kunen] p. 30Lemma 10.20fodom 8117
[Kunen] p. 31Definition 10.24mapex 6746
[Kunen] p. 95Definition 2.1df-r1 7404
[Kunen] p. 97Lemma 2.10r1elss 7446  r1elssi 7445
[Kunen] p. 107Exercise 4rankop 7498  rankopb 7492  rankuni 7503  rankxplim 7517  rankxpsuc 7520
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3889
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26919
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26914
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26920
[LeBlanc] p. 277Rule R2axnul 4122
[Levy] p. 338Axiomdf-clab 2245  df-clel 2254  df-cleq 2251
[Levy58] p. 2Definition Iisfin1-3 7980
[Levy58] p. 2Definition IIdf-fin2 7880
[Levy58] p. 2Definition Iadf-fin1a 7879
[Levy58] p. 2Definition IIIdf-fin3 7882
[Levy58] p. 3Definition Vdf-fin5 7883
[Levy58] p. 3Definition IVdf-fin4 7881
[Levy58] p. 4Definition VIdf-fin6 7884
[Levy58] p. 4Definition VIIdf-fin7 7885
[Levy58], p. 3Theorem 1fin1a2 8009
[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 22949
[Maeda] p. 168Lemma 5mdsym 22953  mdsymi 22952
[Maeda] p. 168Lemma 4(i)mdsymlem4 22947  mdsymlem6 22949  mdsymlem7 22950
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22951
[MaedaMaeda] p. 1Remarkssdmd1 22854  ssdmd2 22855  ssmd1 22852  ssmd2 22853
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22850
[MaedaMaeda] p. 1Definition 1.1df-dmd 22822  df-md 22821  mdbr 22835
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22872  mdslj1i 22860  mdslj2i 22861  mdslle1i 22858  mdslle2i 22859  mdslmd1i 22870  mdslmd2i 22871
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22862  mdsl2bi 22864  mdsl2i 22863
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22876
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22873
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22874
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22851
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22856  mdsl3 22857
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22875
[MaedaMaeda] p. 4Theorem 1.14mdcompli 22970
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28761  hlrelat1 28839
[MaedaMaeda] p. 31Lemma 7.5lcvexch 28479
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22877  cvmdi 22865  cvnbtwn4 22830  cvrnbtwn4 28719
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22878
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28780  cvp 22916  cvrp 28855  lcvp 28480
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22940
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22939
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28773  hlexch4N 28831
[MaedaMaeda] p. 34Exercise 7.1atabsi 22942
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28882
[MaedaMaeda] p. 61Definition 15.10psubN 29188  atpsubN 29192  df-pointsN 28941  pointpsubN 29190
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28943  pmap11 29201  pmaple 29200  pmapsub 29207  pmapval 29196
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29204  pmap1N 29206
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29209  pmapglb2N 29210  pmapglb2xN 29211  pmapglbx 29208
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 29291
[MaedaMaeda] p. 67Postulate PS1ps-1 28916
[MaedaMaeda] p. 68Lemma 16.2df-padd 29235  paddclN 29281  paddidm 29280
[MaedaMaeda] p. 68Condition PS2ps-2 28917
[MaedaMaeda] p. 68Equation 16.2.1paddass 29277
[MaedaMaeda] p. 69Lemma 16.4ps-1 28916
[MaedaMaeda] p. 69Theorem 16.4ps-2 28917
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14947  lsmmod2 14948  lssats 28452  shatomici 22899  shatomistici 22902  shmodi 21930  shmodsi 21929
[MaedaMaeda] p. 130Remark 29.6dmdmd 22841  mdsymlem7 22950
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22129
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22033
[MaedaMaeda] p. 139Remarksumdmdii 22956
[Margaris] p. 40Rule Cexlimiv 2024
[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 1538  df-or 361  dfbi2 612
[Margaris] p. 51Theorem 1id1 22
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 27824
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27825
[Margaris] p. 79Rule Cexinst01 27530  exinst11 27531
[Margaris] p. 89Theorem 19.219.2 1759  19.2K 28258  r19.2z 3518
[Margaris] p. 89Theorem 19.319.3 1760  rr19.3v 2884
[Margaris] p. 89Theorem 19.5alcom 1568
[Margaris] p. 89Theorem 19.6alex 1570
[Margaris] p. 89Theorem 19.7alnex 1569
[Margaris] p. 89Theorem 19.819.8a 1758
[Margaris] p. 89Theorem 19.919.9 1762  19.9v 2011
[Margaris] p. 89Theorem 19.11excom 1765  excomim 1764
[Margaris] p. 89Theorem 19.1219.12 1766  r19.12 2631
[Margaris] p. 90Theorem 19.14exnal 1572
[Margaris] p. 90Theorem 19.152albi 26944  albi 1552  ralbi 2654
[Margaris] p. 90Theorem 19.1619.16 1767
[Margaris] p. 90Theorem 19.1719.17 1768
[Margaris] p. 90Theorem 19.182exbi 26946  exbi 1579
[Margaris] p. 90Theorem 19.1919.19 1769
[Margaris] p. 90Theorem 19.202alim 26943  alim 1548  alimd 1705  alimdh 1551  alimdv 2018  ralimdaa 2595  ralimdv 2597  ralimdva 2596  sbcimdv 3027
[Margaris] p. 90Theorem 19.2119.21-2 1772  19.21 1771  19.21bi 1774  19.21t 1770  19.21v 2012  19.21vv 26942  alrimd 1710  alrimdd 1709  alrimdh 1585  alrimdv 2015  alrimi 1706  alrimih 1553  alrimiv 2013  alrimivv 2014  r19.21 2604  r19.21be 2619  r19.21bi 2616  r19.21t 2603  r19.21v 2605  ralrimd 2606  ralrimdv 2607  ralrimdva 2608  ralrimdvv 2612  ralrimdvva 2613  ralrimi 2599  ralrimiv 2600  ralrimiva 2601  ralrimivv 2609  ralrimivva 2610  ralrimivvva 2611  ralrimivw 2602  rexlimi 2635
[Margaris] p. 90Theorem 19.222alimdv 2020  2exim 26945  2eximdv 2021  exim 1573  eximd 1711  eximdh 1586  eximdv 2019  rexim 2622  reximdai 2626  reximddv 22989  reximdv 2629  reximdv2 2627  reximdva 2630  reximdvai 2628  reximi2 2624
[Margaris] p. 90Theorem 19.2319.23 1777  19.23bi 1783  19.23t 1776  19.23v 2022  19.23vv 2023  exlimd 1784  exlimdh 1785  exlimdv 1933  exlimdvv 2027  exlimexi 27423  exlimi 1781  exlimih 1782  exlimiv 2024  exlimivv 2026  r19.23 2633  r19.23v 2634  rexlimd 2639  rexlimdv 2641  rexlimdv3a 2644  rexlimdva 2642  rexlimdvaa 2643  rexlimdvv 2648  rexlimdvva 2649  rexlimdvw 2645  rexlimiv 2636  rexlimiva 2637  rexlimivv 2647
[Margaris] p. 90Theorem 19.2419.24 1793
[Margaris] p. 90Theorem 19.2519.25 1602
[Margaris] p. 90Theorem 19.2619.26-2 1593  19.26-3an 1594  19.26 1592  r19.26-2 2651  r19.26-2a 24301  r19.26-3 2652  r19.26 2650  r19.26m 2653
[Margaris] p. 90Theorem 19.2719.27 1786  19.27v 2028  r19.27av 2656  r19.27z 3527  r19.27zv 3528
[Margaris] p. 90Theorem 19.2819.28 1787  19.28v 2029  19.28vv 26952  r19.28av 2657  r19.28z 3521  r19.28zv 3524  rr19.28v 2885
[Margaris] p. 90Theorem 19.2919.29 1595  19.29r 1596  19.29r2 1597  19.29x 1598  r19.29 2658  r19.29r 2659
[Margaris] p. 90Theorem 19.3019.30 1603  r19.30 2660
[Margaris] p. 90Theorem 19.3119.31 1795  19.31vv 26950
[Margaris] p. 90Theorem 19.3219.32 1794  r19.32 27294  r19.32v 2661
[Margaris] p. 90Theorem 19.3319.33-2 26948  19.33 1606  19.33b 1607
[Margaris] p. 90Theorem 19.3419.34 1798
[Margaris] p. 90Theorem 19.3519.35 1599  19.35i 1600  19.35ri 1601  r19.35 2662
[Margaris] p. 90Theorem 19.3619.36 1788  19.36aiv 2031  19.36i 1789  19.36v 2030  19.36vv 26949  r19.36av 2663  r19.36zv 3529
[Margaris] p. 90Theorem 19.3719.37 1790  19.37aiv 2034  19.37v 2033  19.37vv 26951  r19.37 2664  r19.37av 2665  r19.37zv 3525
[Margaris] p. 90Theorem 19.3819.38 1791
[Margaris] p. 90Theorem 19.3919.39 1792
[Margaris] p. 90Theorem 19.4019.40-2 1609  19.40 1608  r19.40 2666
[Margaris] p. 90Theorem 19.4119.41 1799  19.41rg 27452  19.41v 2035  19.41vv 2036  19.41vvv 2037  19.41vvvv 2038  r19.41 2667  r19.41v 2668
[Margaris] p. 90Theorem 19.4219.42 1800  19.42v 2039  19.42vv 2041  19.42vvv 2042  r19.42v 2669
[Margaris] p. 90Theorem 19.4319.43 1604  r19.43 2670
[Margaris] p. 90Theorem 19.4419.44 1796  r19.44av 2671
[Margaris] p. 90Theorem 19.4519.45 1797  r19.45av 2672  r19.45zv 3526
[Margaris] p. 110Exercise 2(b)eu1 2139
[Mayet] p. 370Remarkjpi 22811  largei 22808  stri 22798
[Mayet3] p. 9Definition of CH-statesdf-hst 22753  ishst 22755
[Mayet3] p. 10Theoremhstrbi 22807  hstri 22806
[Mayet3] p. 1223Theorem 4.1mayete3i 22268
[Mayet3] p. 1240Theorem 7.1mayetes3i 22270
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22819
[MegPav2000] p. 2345Definition 3.4-1chintcl 21872  chsupcl 21880
[MegPav2000] p. 2345Definition 3.4-2hatomic 22901
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22895
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22922
[MegPav2000] p. 2366Figure 7pl42N 29422
[MegPav2002] p. 362Lemma 2.2latj31 14168  latj32 14166  latjass 14164
[Megill] p. 444Axiom C5ax-17 1628
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 1838  alequcom 1680  alequcomX 28349  ax-10 1678
[Megill] p. 446Lemma L17equtrr 1827
[Megill] p. 446Lemma L18ax9from9o 1816
[Megill] p. 446Lemma L19hbnae-o 1846  hbnae 1845
[Megill] p. 447Remark 9.1df-sb 1884  sbid 1896  sbidd-misc 27322  sbidd 27321
[Megill] p. 448Remark 9.6ax15 2105
[Megill] p. 448Scheme C4'ax-5o 1694
[Megill] p. 448Scheme C5'ax-4 1692
[Megill] p. 448Scheme C6'ax-7 1535
[Megill] p. 448Scheme C7'ax-6o 1697
[Megill] p. 448Scheme C8'ax-8 1623
[Megill] p. 448Scheme C9'ax-12o 1664
[Megill] p. 448Scheme C10'ax-9 1684  ax-9o 1815
[Megill] p. 448Scheme C11'ax-10o 1836
[Megill] p. 448Scheme C12'ax-13 1625
[Megill] p. 448Scheme C13'ax-14 1626
[Megill] p. 448Scheme C14'ax-15 2106
[Megill] p. 448Scheme C15'ax-11o 1941
[Megill] p. 448Scheme C16'ax-16 1927
[Megill] p. 448Theorem 9.4dral1-o 1857  dral1 1856  dral2-o 1859  dral2 1858  drex1 1860  drex2 1861  drsb1 1887  drsb2 1954
[Megill] p. 448Theorem 9.7conventions 3
[Megill] p. 449Theorem 9.7sbcom2 2077  sbequ 1953  sbid2v 2086
[Megill] p. 450Example in Appendixhba1 1718
[Mendelson] p. 35Axiom A3hirstL-ax3 27209
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4ra4sbc 3044  ra4sbca 3045  stdpc4 1897
[Mendelson] p. 69Axiom 5ax-5o 1694  ra5 3050  stdpc5 1773
[Mendelson] p. 81Rule Cexlimiv 2024
[Mendelson] p. 95Axiom 6stdpc6 1821
[Mendelson] p. 95Axiom 7stdpc7 1892
[Mendelson] p. 225Axiom system NBGru 2965
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4240
[Mendelson] p. 231Exercise 4.10(k)inv1 3456
[Mendelson] p. 231Exercise 4.10(l)unv 3457
[Mendelson] p. 231Exercise 4.10(n)dfin3 3383
[Mendelson] p. 231Exercise 4.10(o)df-nul 3431
[Mendelson] p. 231Exercise 4.10(q)dfin4 3384
[Mendelson] p. 231Exercise 4.10(s)ddif 3283
[Mendelson] p. 231Definition of uniondfun3 3382
[Mendelson] p. 235Exercise 4.12(c)univ 4537
[Mendelson] p. 235Exercise 4.12(d)pwv 3800
[Mendelson] p. 235Exercise 4.12(j)pwin 4269
[Mendelson] p. 235Exercise 4.12(k)pwunss 4270
[Mendelson] p. 235Exercise 4.12(l)pwssun 4271
[Mendelson] p. 235Exercise 4.12(n)uniin 3821
[Mendelson] p. 235Exercise 4.12(p)reli 4801
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5180
[Mendelson] p. 244Proposition 4.8(g)epweon 4547
[Mendelson] p. 246Definition of successordf-suc 4370
[Mendelson] p. 250Exercise 4.36oelim2 6561
[Mendelson] p. 254Proposition 4.22(b)xpen 6992
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6914  xpsneng 6915
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6921  xpcomeng 6922
[Mendelson] p. 254Proposition 4.22(e)xpassen 6924
[Mendelson] p. 255Definitionbrsdom 6852
[Mendelson] p. 255Exercise 4.39endisj 6917
[Mendelson] p. 255Exercise 4.41mapprc 6744
[Mendelson] p. 255Exercise 4.43mapsnen 6906
[Mendelson] p. 255Exercise 4.45mapunen 6998
[Mendelson] p. 255Exercise 4.47xpmapen 6997
[Mendelson] p. 255Exercise 4.42(a)map0e 6773
[Mendelson] p. 255Exercise 4.42(b)map1 6907
[Mendelson] p. 257Proposition 4.24(a)undom 6918
[Mendelson] p. 258Exercise 4.56(b)cdaen 7767
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7776  cdacomen 7775
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7780
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7774
[Mendelson] p. 258Definition of cardinal sumcdaval 7764  df-cda 7762
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6498
[Mendelson] p. 266Proposition 4.34(f)oaordex 6524
[Mendelson] p. 275Proposition 4.42(d)entri3 8149
[Mendelson] p. 281Definitiondf-r1 7404
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7453
[Mendelson] p. 287Axiom system MKru 2965
[Mittelstaedt] p. 9Definitiondf-oc 21792
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3366
[Monk1] p. 33Theorem 3.2(i)ssrel 4764
[Monk1] p. 33Theorem 3.2(ii)eqrel 4765
[Monk1] p. 34Definition 3.3df-opab 4052
[Monk1] p. 36Theorem 3.7(i)coi1 5175  coi2 5176
[Monk1] p. 36Theorem 3.8(v)dm0 4880  rn0 4924
[Monk1] p. 36Theorem 3.7(ii)cnvi 5073
[Monk1] p. 37Theorem 3.13(i)relxp 4782
[Monk1] p. 37Theorem 3.13(x)dmxp 4885  rnxp 5094
[Monk1] p. 37Theorem 3.13(ii)xp0 5086  xp0r 4756
[Monk1] p. 38Theorem 3.16(ii)ima0 5018
[Monk1] p. 38Theorem 3.16(viii)imai 5015
[Monk1] p. 39Theorem 3.17imaexg 5014
[Monk1] p. 39Theorem 3.16(xi)imassrn 5013
[Monk1] p. 41Theorem 4.3(i)fnopfv 5594  funfvop 5571
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5500
[Monk1] p. 42Theorem 4.4(iii)fvelima 5508
[Monk1] p. 43Theorem 4.6funun 5234
[Monk1] p. 43Theorem 4.8(iv)dff13 5717  dff13f 5718
[Monk1] p. 46Theorem 4.15(v)funex 5677  funrnex 5681
[Monk1] p. 50Definition 5.4fniunfv 5707
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5143
[Monk1] p. 52Theorem 5.11(viii)ssint 3852
[Monk1] p. 52Definition 5.13 (i)1stval2 6071  df-1st 6056
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6072  df-2nd 6057
[Monk1] p. 112Theorem 15.17(v)ranksn 7494  ranksnb 7467
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7495
[Monk1] p. 112Theorem 15.17(iii)rankun 7496  rankunb 7490
[Monk1] p. 113Theorem 15.18r1val3 7478
[Monk1] p. 113Definition 15.19df-r1 7404  r1val2 7477
[Monk1] p. 117Lemmazorn2 8101  zorn2g 8098
[Monk1] p. 133Theorem 18.11cardom 7587
[Monk1] p. 133Theorem 18.12canth3 8151
[Monk1] p. 133Theorem 18.14carduni 7582
[Monk2] p. 105Axiom C4ax-5 1533
[Monk2] p. 105Axiom C7ax-8 1623
[Monk2] p. 105Axiom C8ax-11 1624  ax-11o 1941
[Monk2] p. 105Axiom (C8)ax11v 1991
[Monk2] p. 108Lemma 5ax-5o 1694
[Monk2] p. 109Lemma 12ax-7 1535
[Monk2] p. 109Lemma 15equvin 2000  equvini 1880  eqvinop 4223
[Monk2] p. 113Axiom C5-1ax-17 1628
[Monk2] p. 113Axiom C5-2ax-6 1534
[Monk2] p. 113Axiom C5-3ax-7 1535
[Monk2] p. 114Lemma 21ax4 1691
[Monk2] p. 114Lemma 22ax5o 1693  hba1 1718
[Monk2] p. 114Lemma 23nfia1 1745
[Monk2] p. 114Lemma 24nfa2 1744  nfra2 2572
[Moore] p. 53Part Idf-mre 13451
[Munkres] p. 77Example 2distop 16696  indistop 16702  indistopon 16701
[Munkres] p. 77Example 3fctop 16704  fctop2 16705
[Munkres] p. 77Example 4cctop 16706
[Munkres] p. 78Definition of basisdf-bases 16601  isbasis3g 16650
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13307  tgval2 16657
[Munkres] p. 79Remarktgcl 16670
[Munkres] p. 80Lemma 2.1tgval3 16664
[Munkres] p. 80Lemma 2.2tgss2 16688  tgss3 16687
[Munkres] p. 81Lemma 2.3basgen 16689  basgen2 16690
[Munkres] p. 89Definition of subspace topologyresttop 16854
[Munkres] p. 93Theorem 6.1(1)0cld 16738  topcld 16735
[Munkres] p. 93Theorem 6.1(2)iincld 16739
[Munkres] p. 93Theorem 6.1(3)uncld 16741
[Munkres] p. 94Definition of closureclsval 16737
[Munkres] p. 94Definition of interiorntrval 16736
[Munkres] p. 95Theorem 6.5(a)clsndisj 16775  elcls 16773
[Munkres] p. 95Theorem 6.5(b)elcls3 16783
[Munkres] p. 97Theorem 6.6clslp 16842  neindisj 16817
[Munkres] p. 97Corollary 6.7cldlp 16844
[Munkres] p. 97Definition of limit pointislp2 16840  lpval 16834
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17006
[Munkres] p. 102Definition of continuous functiondf-cn 16920  iscn 16928  iscn2 16931
[Munkres] p. 107Theorem 7.2(g)cncnp 16972  cncnp2 16973  cncnpi 16970  df-cnp 16921  iscnp 16930  iscnp2 16932
[Munkres] p. 127Theorem 10.1metcn 18052
[Munkres] p. 128Theorem 10.3metcn4 18699
[NielsenChuang] p. 195Equation 4.73unierri 22645
[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 18600  df-dip 21235  dip0l 21255  ip0l 16503
[Ponnusamy] p. 361Equation 6.45ipval 21237
[Ponnusamy] p. 362Equation I1dipcj 21251
[Ponnusamy] p. 362Equation I3cphdir 18603  dipdir 21381  ipdir 16506  ipdiri 21369
[Ponnusamy] p. 362Equation I4ipidsq 21247
[Ponnusamy] p. 362Equation 6.46ip0i 21364
[Ponnusamy] p. 362Equation 6.47ip1i 21366
[Ponnusamy] p. 362Equation 6.48ip2i 21367
[Ponnusamy] p. 363Equation I2cphass 18609  dipass 21384  ipass 16512  ipassi 21380
[Prugovecki] p. 186Definition of brabraval 22485  df-bra 22391
[Prugovecki] p. 376Equation 8.1df-kb 22392  kbval 22495
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22923
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 29327
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22937  atcvat4i 22938  cvrat3 28881  cvrat4 28882  lsatcvat3 28492
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22823  cvrval 28709  df-cv 22820  df-lcv 28459  lspsncv0 15862
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 29339
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 29340
[Quine] p. 16Definition 2.1df-clab 2245  rabid 2691
[Quine] p. 17Definition 2.1''dfsb7 2082
[Quine] p. 18Definition 2.7df-cleq 2251
[Quine] p. 19Definition 2.9conventions 3  df-v 2765
[Quine] p. 34Theorem 5.1abeq2 2363
[Quine] p. 35Theorem 5.2abid2 2375  abid2f 2419
[Quine] p. 40Theorem 6.1sb5 1994
[Quine] p. 40Theorem 6.2sb56 1992  sb6 1993
[Quine] p. 41Theorem 6.3df-clel 2254
[Quine] p. 41Theorem 6.4eqid 2258  eqid1 20801
[Quine] p. 41Theorem 6.5eqcom 2260
[Quine] p. 42Theorem 6.6df-sbc 2967
[Quine] p. 42Theorem 6.7dfsbcq 2968  dfsbcq2 2969
[Quine] p. 43Theorem 6.8vex 2766
[Quine] p. 43Theorem 6.9isset 2767
[Quine] p. 44Theorem 7.3cla4gf 2838  cla4gv 2843  cla4imgf 2836
[Quine] p. 44Theorem 6.11a4sbc 2978  a4sbcd 2979
[Quine] p. 44Theorem 6.12elex 2771
[Quine] p. 44Theorem 6.13elab 2889  elabg 2890  elabgf 2887
[Quine] p. 44Theorem 6.14noel 3434
[Quine] p. 48Theorem 7.2snprc 3669
[Quine] p. 48Definition 7.1df-pr 3621  df-sn 3620
[Quine] p. 49Theorem 7.4snss 3722  snssg 3728
[Quine] p. 49Theorem 7.5prss 3743  prssg 3744
[Quine] p. 49Theorem 7.6prid1 3708  prid1g 3706  prid2 3709  prid2g 3707  snid 3641  snidg 3639
[Quine] p. 51Theorem 7.13prex 4189  snex 4188  snexALT 4168
[Quine] p. 53Theorem 8.2unisn 3817  unisnALT 27835  unisng 3818
[Quine] p. 53Theorem 8.3uniun 3820
[Quine] p. 54Theorem 8.6elssuni 3829
[Quine] p. 54Theorem 8.7uni0 3828
[Quine] p. 56Theorem 8.17uniabio 6235
[Quine] p. 56Definition 8.18dfiota2 6226
[Quine] p. 57Theorem 8.19iotaval 6236
[Quine] p. 57Theorem 8.22iotanul 6240
[Quine] p. 58Theorem 8.23iotaex 6242
[Quine] p. 58Definition 9.1df-op 3623
[Quine] p. 61Theorem 9.5opabid 4243  opelopab 4258  opelopaba 4253  opelopabaf 4260  opelopabf 4261  opelopabg 4255  opelopabga 4250  oprabid 5816
[Quine] p. 64Definition 9.11df-xp 4675
[Quine] p. 64Definition 9.12df-cnv 4677
[Quine] p. 64Definition 9.15df-id 4281
[Quine] p. 65Theorem 10.3fun0 5245
[Quine] p. 65Theorem 10.4funi 5223
[Quine] p. 65Theorem 10.5funsn 5238  funsng 5236
[Quine] p. 65Definition 10.1df-fun 4683
[Quine] p. 65Definition 10.2args 5029  df-fv 4689
[Quine] p. 68Definition 10.11conventions 3  df-fv 4689  fv2 5454
[Quine] p. 124Theorem 17.3nn0opth2 11254  nn0opth2i 11253  nn0opthi 11252  omopthi 6623
[Quine] p. 177Definition 25.2df-rdg 6391
[Quine] p. 232Equation icarddom 8144
[Quine] p. 284Axiom 39(vi)funimaex 5268  funimaexg 5267
[Quine] p. 331Axiom system NFru 2965
[ReedSimon] p. 36Definition (iii)ax-his3 21624
[ReedSimon] p. 63Exercise 4(a)df-dip 21235  polid 21699  polid2i 21697  polidi 21698
[ReedSimon] p. 63Exercise 4(b)df-ph 21352
[ReedSimon] p. 195Remarklnophm 22560  lnophmi 22559
[Retherford] p. 49Exercise 1(i)leopadd 22673
[Retherford] p. 49Exercise 1(ii)leopmul 22675  leopmuli 22674
[Retherford] p. 49Exercise 1(iv)leoptr 22678
[Retherford] p. 49Definition VI.1df-leop 22393  leoppos 22667
[Retherford] p. 49Exercise 1(iii)leoptri 22677
[Retherford] p. 49Definition of operator orderingleop3 22666
[Rudin] p. 164Equation 27efcan 12339
[Rudin] p. 164Equation 30efzval 12345
[Rudin] p. 167Equation 48absefi 12439
[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 5046
[Schechter] p. 51Definition of irreflexivityintirr 5049
[Schechter] p. 51Definition of symmetrycnvsym 5045
[Schechter] p. 51Definition of transitivitycotr 5043
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13451
[Schechter] p. 79Definition of Moore closuredf-mrc 13452
[Schechter] p. 82Section 4.5df-mrc 13452
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13454
[Schechter] p. 139Definition AC3dfac9 7730
[Schechter] p. 141Definition (MC)dfac11 26528
[Schechter] p. 149Axiom DC1ax-dc 8040  axdc3 8048
[Schechter] p. 187Definition of ring with unitisrng 15308  isrngo 21006
[Schechter] p. 276Remark 11.6.espan0 22082
[Schechter] p. 276Definition of spandf-span 21849  spanval 21873
[Schechter] p. 428Definition 15.35bastop1 16694
[Schwabhauser] p. 10Axiom A1axcgrrflx 23918
[Schwabhauser] p. 10Axiom A2axcgrtr 23919
[Schwabhauser] p. 10Axiom A3axcgrid 23920
[Schwabhauser] p. 11Axiom A4axsegcon 23931
[Schwabhauser] p. 11Axiom A5ax5seg 23942
[Schwabhauser] p. 11Axiom A6axbtwnid 23943
[Schwabhauser] p. 12Axiom A7axpasch 23945
[Schwabhauser] p. 12Axiom A8axlowdim2 23964
[Schwabhauser] p. 13Axiom A10axeuclid 23967
[Schwabhauser] p. 13Axiom A11axcont 23980
[Schwabhauser] p. 27Theorem 2.1cgrrflx 23986
[Schwabhauser] p. 27Theorem 2.2cgrcomim 23988
[Schwabhauser] p. 27Theorem 2.3cgrtr 23991
[Schwabhauser] p. 27Theorem 2.4cgrcoml 23995
[Schwabhauser] p. 27Theorem 2.5cgrcomr 23996
[Schwabhauser] p. 28Theorem 2.8cgrtriv 24001
[Schwabhauser] p. 28Theorem 2.105segofs 24005
[Schwabhauser] p. 28Definition 2.10df-ofs 23982
[Schwabhauser] p. 29Theorem 2.11cgrextend 24007
[Schwabhauser] p. 29Theorem 2.12segconeq 24009
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 24021  btwntriv2 24011
[Schwabhauser] p. 30Theorem 3.2btwncomim 24012
[Schwabhauser] p. 30Theorem 3.3btwntriv1 24015
[Schwabhauser] p. 30Theorem 3.4btwnswapid 24016
[Schwabhauser] p. 30Theorem 3.5btwnexch2 24022  btwnintr 24018
[Schwabhauser] p. 30Theorem 3.6btwnexch 24024  btwnexch3 24019
[Schwabhauser] p. 30Theorem 3.7btwnouttr 24023
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23963
[Schwabhauser] p. 32Theorem 3.14btwndiff 24026
[Schwabhauser] p. 33Theorem 3.17trisegint 24027
[Schwabhauser] p. 34Theorem 4.2ifscgr 24043
[Schwabhauser] p. 34Definition 4.1df-ifs 24038
[Schwabhauser] p. 35Theorem 4.3cgrsub 24044
[Schwabhauser] p. 35Theorem 4.5cgrxfr 24054
[Schwabhauser] p. 35Definition 4.4df-cgr3 24039
[Schwabhauser] p. 36Theorem 4.6btwnxfr 24055
[Schwabhauser] p. 36Theorem 4.11colinearperm1 24061  colinearperm2 24063  colinearperm3 24062  colinearperm4 24064  colinearperm5 24065
[Schwabhauser] p. 36Definition 4.10df-colinear 24040
[Schwabhauser] p. 37Theorem 4.12colineartriv1 24066
[Schwabhauser] p. 37Theorem 4.13colinearxfr 24074
[Schwabhauser] p. 37Theorem 4.14lineext 24075
[Schwabhauser] p. 37Theorem 4.16fscgr 24079
[Schwabhauser] p. 37Theorem 4.17linecgr 24080
[Schwabhauser] p. 37Definition 4.15df-fs 24041
[Schwabhauser] p. 38Theorem 4.18lineid 24082
[Schwabhauser] p. 38Theorem 4.19idinside 24083
[Schwabhauser] p. 39Theorem 5.1btwnconn1 24100
[Schwabhauser] p. 41Theorem 5.2btwnconn2 24101
[Schwabhauser] p. 41Theorem 5.3btwnconn3 24102
[Schwabhauser] p. 41Theorem 5.5brsegle2 24108
[Schwabhauser] p. 41Definition 5.4df-segle 24106
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 24109
[Schwabhauser] p. 42Theorem 5.7seglerflx 24111
[Schwabhauser] p. 42Theorem 5.8segletr 24113
[Schwabhauser] p. 42Theorem 5.9segleantisym 24114
[Schwabhauser] p. 42Theorem 5.10seglelin 24115
[Schwabhauser] p. 42Theorem 5.11seglemin 24112
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 24117
[Schwabhauser] p. 43Theorem 6.2btwnoutside 24124
[Schwabhauser] p. 43Theorem 6.3broutsideof3 24125
[Schwabhauser] p. 43Theorem 6.4broutsideof 24120  df-outsideof 24119
[Schwabhauser] p. 43Definition 6.1broutsideof2 24121
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 24126
[Schwabhauser] p. 44Theorem 6.6outsideofcom 24127
[Schwabhauser] p. 44Theorem 6.7outsideoftr 24128
[Schwabhauser] p. 44Theorem 6.11outsideofeu 24130
[Schwabhauser] p. 44Definition 6.8df-ray 24137
[Schwabhauser] p. 45Part 2df-lines2 24138
[Schwabhauser] p. 45Theorem 6.13outsidele 24131
[Schwabhauser] p. 45Theorem 6.15lineunray 24146
[Schwabhauser] p. 45Theorem 6.16lineelsb2 24147
[Schwabhauser] p. 45Theorem 6.17linecom 24149  linerflx1 24148  linerflx2 24150
[Schwabhauser] p. 45Theorem 6.18linethru 24152
[Schwabhauser] p. 45Definition 6.14df-line2 24136
[Schwabhauser] p. 46Theorem 6.19linethrueu 24155
[Schwabhauser] p. 46Theorem 6.21lineintmo 24156
[Shapiro] p. 230Theorem 6.5.1dchrhash 20473  dchrsum 20471  dchrsum2 20470  sumdchr 20474
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20475  sum2dchr 20476
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15264  ablfacrp2 15265
[Shapiro], p. 328Equation 9.2.4vmasum 20418
[Shapiro], p. 329Equation 9.2.7logfac2 20419
[Shapiro], p. 329Equation 9.2.9logfacrlim 20426
[Shapiro], p. 331Equation 9.2.13vmadivsum 20594
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20597
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20651  vmalogdivsum2 20650
[Shapiro], p. 375Theorem 9.4.1dirith 20641  dirith2 20640
[Shapiro], p. 375Equation 9.4.3rplogsum 20639  rpvmasum 20638  rpvmasum2 20624
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20599
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20637
[Shapiro], p. 377Lemma 9.4.1dchrisum 20604  dchrisumlem1 20601  dchrisumlem2 20602  dchrisumlem3 20603  dchrisumlema 20600
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20607
[Shapiro], p. 379Equation 9.4.16dchrmusum 20636  dchrmusumlem 20634  dchrvmasumlem 20635
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20606
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20608
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20632  dchrisum0re 20625  dchrisumn0 20633
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20618
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20622
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20623
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20678  pntrsumbnd2 20679  pntrsumo1 20677
[Shapiro], p. 405Equation 10.2.1mudivsum 20642
[Shapiro], p. 406Equation 10.2.6mulogsum 20644
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20646
[Shapiro], p. 407Equation 10.2.8mulog2sum 20649
[Shapiro], p. 418Equation 10.4.6logsqvma 20654
[Shapiro], p. 418Equation 10.4.8logsqvma2 20655
[Shapiro], p. 419Equation 10.4.10selberg 20660
[Shapiro], p. 420Equation 10.4.12selberg2lem 20662
[Shapiro], p. 420Equation 10.4.14selberg2 20663
[Shapiro], p. 422Equation 10.6.7selberg3 20671
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20672
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20669  selberg3lem2 20670
[Shapiro], p. 422Equation 10.4.23selberg4 20673
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20667
[Shapiro], p. 428Equation 10.6.2selbergr 20680
[Shapiro], p. 429Equation 10.6.8selberg3r 20681
[Shapiro], p. 430Equation 10.6.11selberg4r 20682
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20696
[Shapiro], p. 434Equation 10.6.27pntlema 20708  pntlemb 20709  pntlemc 20707  pntlemd 20706  pntlemg 20710
[Shapiro], p. 435Equation 10.6.29pntlema 20708
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20700
[Shapiro], p. 436Lemma 10.6.2pntibnd 20705
[Shapiro], p. 436Equation 10.6.34pntlema 20708
[Shapiro], p. 436Equation 10.6.35pntlem3 20721  pntleml 20723
[Stoll] p. 13Definition of symmetric differencesymdif1 3408
[Stoll] p. 16Exercise 4.40dif 3500  dif0 3499
[Stoll] p. 16Exercise 4.8difdifdir 3516
[Stoll] p. 17Theorem 5.1(5)undifv 3503
[Stoll] p. 19Theorem 5.2(13)undm 3401
[Stoll] p. 19Theorem 5.2(13')indm 3402
[Stoll] p. 20Remarkinvdif 3385
[Stoll] p. 25Definition of ordered tripledf-ot 3624
[Stoll] p. 43Definitionuniiun 3929
[Stoll] p. 44Definitionintiin 3930
[Stoll] p. 45Definitiondf-iin 3882
[Stoll] p. 45Definition indexed uniondf-iun 3881
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3408
[Strang] p. 242Section 6.3expgrowth 26920
[Suppes] p. 22Theorem 2eq0 3444
[Suppes] p. 22Theorem 4eqss 3169  eqssd 3171  eqssi 3170
[Suppes] p. 23Theorem 5ss0 3460  ss0b 3459
[Suppes] p. 23Theorem 6sstr 3162  sstrALT2 27744
[Suppes] p. 23Theorem 7pssirr 3251
[Suppes] p. 23Theorem 8pssn2lp 3252
[Suppes] p. 23Theorem 9psstr 3255
[Suppes] p. 23Theorem 10pssss 3246
[Suppes] p. 25Theorem 12elin 3333  elun 3291
[Suppes] p. 26Theorem 15inidm 3353
[Suppes] p. 26Theorem 16in0 3455
[Suppes] p. 27Theorem 23unidm 3293
[Suppes] p. 27Theorem 24un0 3454
[Suppes] p. 27Theorem 25ssun1 3313
[Suppes] p. 27Theorem 26ssequn1 3320
[Suppes] p. 27Theorem 27unss 3324
[Suppes] p. 27Theorem 28indir 3392
[Suppes] p. 27Theorem 29undir 3393
[Suppes] p. 28Theorem 32difid 3497  difidALT 3498
[Suppes] p. 29Theorem 33difin 3381
[Suppes] p. 29Theorem 34indif 3386
[Suppes] p. 29Theorem 35undif1 3504
[Suppes] p. 29Theorem 36difun2 3508
[Suppes] p. 29Theorem 37difin0 3502
[Suppes] p. 29Theorem 38disjdif 3501
[Suppes] p. 29Theorem 39difundi 3396
[Suppes] p. 29Theorem 40difindi 3398
[Suppes] p. 30Theorem 41nalset 4125
[Suppes] p. 39Theorem 61uniss 3822
[Suppes] p. 39Theorem 65uniop 4241
[Suppes] p. 41Theorem 70intsn 3872
[Suppes] p. 42Theorem 71intpr 3869  intprg 3870
[Suppes] p. 42Theorem 73op1stb 4541
[Suppes] p. 42Theorem 78intun 3868
[Suppes] p. 44Definition 15(a)dfiun2 3911  dfiun2g 3909
[Suppes] p. 44Definition 15(b)dfiin2 3912
[Suppes] p. 47Theorem 86elpw 3605  elpw2 4142  elpw2g 4141  elpwg 3606  elpwgdedVD 27826
[Suppes] p. 47Theorem 87pwid 3612
[Suppes] p. 47Theorem 89pw0 3736
[Suppes] p. 48Theorem 90pwpw0 3737
[Suppes] p. 52Theorem 101xpss12 4780
[Suppes] p. 52Theorem 102xpindi 4807  xpindir 4808
[Suppes] p. 52Theorem 103xpundi 4729  xpundir 4730
[Suppes] p. 54Theorem 105elirrv 7279
[Suppes] p. 58Theorem 2relss 4763
[Suppes] p. 59Theorem 4eldm 4864  eldm2 4865  eldm2g 4863  eldmg 4862
[Suppes] p. 59Definition 3df-dm 4679
[Suppes] p. 60Theorem 6dmin 4874
[Suppes] p. 60Theorem 8rnun 5077
[Suppes] p. 60Theorem 9rnin 5078
[Suppes] p. 60Definition 4dfrn2 4856
[Suppes] p. 61Theorem 11brcnv 4852  brcnvg 4850
[Suppes] p. 62Equation 5elcnv 4846  elcnv2 4847
[Suppes] p. 62Theorem 12relcnv 5039
[Suppes] p. 62Theorem 15cnvin 5076
[Suppes] p. 62Theorem 16cnvun 5074
[Suppes] p. 63Theorem 20co02 5173
[Suppes] p. 63Theorem 21dmcoss 4932
[Suppes] p. 63Definition 7df-co 4678
[Suppes] p. 64Theorem 26cnvco 4853
[Suppes] p. 64Theorem 27coass 5178
[Suppes] p. 65Theorem 31resundi 4957
[Suppes] p. 65Theorem 34elima 5005  elima2 5006  elima3 5007  elimag 5004
[Suppes] p. 65Theorem 35imaundi 5081
[Suppes] p. 66Theorem 40dminss 5083
[Suppes] p. 66Theorem 41imainss 5084
[Suppes] p. 67Exercise 11cnvxp 5085
[Suppes] p. 81Definition 34dfec2 6631
[Suppes] p. 82Theorem 72elec 6667  elecg 6666
[Suppes] p. 82Theorem 73erth 6672  erth2 6673
[Suppes] p. 83Theorem 74erdisj 6675
[Suppes] p. 89Theorem 96map0b 6774
[Suppes] p. 89Theorem 97map0 6776  map0g 6775
[Suppes] p. 89Theorem 98mapsn 6777
[Suppes] p. 89Theorem 99mapss 6778
[Suppes] p. 91Definition 12(ii)alephsuc 7663
[Suppes] p. 91Definition 12(iii)alephlim 7662
[Suppes] p. 92Theorem 1enref 6862  enrefg 6861
[Suppes] p. 92Theorem 2ensym 6878  ensymb 6877  ensymi 6879
[Suppes] p. 92Theorem 3entr 6881
[Suppes] p. 92Theorem 4unen 6911
[Suppes] p. 94Theorem 15endom 6856
[Suppes] p. 94Theorem 16ssdomg 6875
[Suppes] p. 94Theorem 17domtr 6882
[Suppes] p. 95Theorem 18sbth 6949
[Suppes] p. 97Theorem 23canth2 6982  canth2g 6983
[Suppes] p. 97Definition 3brsdom2 6953  df-sdom 6834  dfsdom2 6952
[Suppes] p. 97Theorem 21(i)sdomirr 6966
[Suppes] p. 97Theorem 22(i)domnsym 6955
[Suppes] p. 97Theorem 21(ii)sdomnsym 6954
[Suppes] p. 97Theorem 22(ii)domsdomtr 6964
[Suppes] p. 97Theorem 22(iv)brdom2 6859
[Suppes] p. 97Theorem 21(iii)sdomtr 6967
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6962
[Suppes] p. 98Exercise 4fundmen 6902  fundmeng 6903
[Suppes] p. 98Exercise 6xpdom3 6928
[Suppes] p. 98Exercise 11sdomentr 6963
[Suppes] p. 104Theorem 37fofi 7110
[Suppes] p. 104Theorem 38pwfi 7119
[Suppes] p. 105Theorem 40pwfi 7119
[Suppes] p. 111Axiom for cardinal numberscarden 8141
[Suppes] p. 130Definition 3df-tr 4088
[Suppes] p. 132Theorem 9ssonuni 4550
[Suppes] p. 134Definition 6df-suc 4370
[Suppes] p. 136Theorem Schema 22findes 4658  finds 4654  finds1 4657  finds2 4656
[Suppes] p. 151Theorem 42isfinite 7321  isfinite2 7083  isfiniteg 7085  unbnn 7081
[Suppes] p. 162Definition 5df-ltnq 8510  df-ltpq 8502
[Suppes] p. 197Theorem Schema 4tfindes 4625  tfinds 4622  tfinds2 4626
[Suppes] p. 209Theorem 18oaord1 6517
[Suppes] p. 209Theorem 21oaword2 6519
[Suppes] p. 211Theorem 25oaass 6527
[Suppes] p. 225Definition 8iscard2 7577
[Suppes] p. 227Theorem 56ondomon 8153
[Suppes] p. 228Theorem 59harcard 7579
[Suppes] p. 228Definition 12(i)aleph0 7661
[Suppes] p. 228Theorem Schema 61onintss 4414
[Suppes] p. 228Theorem Schema 62onminesb 4561  onminsb 4562
[Suppes] p. 229Theorem 64alephval2 8162
[Suppes] p. 229Theorem 65alephcard 7665
[Suppes] p. 229Theorem 66alephord2i 7672
[Suppes] p. 229Theorem 67alephnbtwn 7666
[Suppes] p. 229Definition 12df-aleph 7541
[Suppes] p. 242Theorem 6weth 8090
[Suppes] p. 242Theorem 8entric 8147
[Suppes] p. 242Theorem 9carden 8141
[TakeutiZaring] p. 8Axiom 1ax-ext 2239
[TakeutiZaring] p. 13Definition 4.5df-cleq 2251
[TakeutiZaring] p. 13Proposition 4.6df-clel 2254
[TakeutiZaring] p. 13Proposition 4.9cvjust 2253
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2275
[TakeutiZaring] p. 14Definition 4.16df-oprab 5796
[TakeutiZaring] p. 14Proposition 4.14ru 2965
[TakeutiZaring] p. 15Axiom 2zfpair 4184
[TakeutiZaring] p. 15Exercise 1elpr 3632  elpr2 3633  elprg 3631
[TakeutiZaring] p. 15Exercise 2elsn 3629  elsnc 3637  elsnc2 3643  elsnc2g 3642  elsncg 3636
[TakeutiZaring] p. 15Exercise 3elop 4211
[TakeutiZaring] p. 15Exercise 4sneq 3625  sneqr 3754
[TakeutiZaring] p. 15Definition 5.1dfpr2 3630  dfsn2 3628
[TakeutiZaring] p. 16Axiom 3uniex 4488
[TakeutiZaring] p. 16Exercise 6opth 4217
[TakeutiZaring] p. 16Exercise 7opex 4209
[TakeutiZaring] p. 16Exercise 8rext 4194
[TakeutiZaring] p. 16Corollary 5.8unex 4490  unexg 4493
[TakeutiZaring] p. 16Definition 5.3dftp2 3653
[TakeutiZaring] p. 16Definition 5.5df-uni 3802
[TakeutiZaring] p. 16Definition 5.6df-in 3134  df-un 3132
[TakeutiZaring] p. 16Proposition 5.7unipr 3815  uniprg 3816
[TakeutiZaring] p. 17Axiom 4pwex 4165  pwexg 4166
[TakeutiZaring] p. 17Exercise 1eltp 3652
[TakeutiZaring] p. 17Exercise 5elsuc 4433  elsucg 4431  sstr2 3161
[TakeutiZaring] p. 17Exercise 6uncom 3294
[TakeutiZaring] p. 17Exercise 7incom 3336
[TakeutiZaring] p. 17Exercise 8unass 3307
[TakeutiZaring] p. 17Exercise 9inass 3354
[TakeutiZaring] p. 17Exercise 10indi 3390
[TakeutiZaring] p. 17Exercise 11undi 3391
[TakeutiZaring] p. 17Definition 5.9df-pss 3143  dfss2 3144
[TakeutiZaring] p. 17Definition 5.10df-pw 3601
[TakeutiZaring] p. 18Exercise 7unss2 3321
[TakeutiZaring] p. 18Exercise 9df-ss 3141  sseqin2 3363
[TakeutiZaring] p. 18Exercise 10ssid 3172
[TakeutiZaring] p. 18Exercise 12inss1 3364  inss2 3365
[TakeutiZaring] p. 18Exercise 13nss 3211
[TakeutiZaring] p. 18Exercise 15unieq 3810
[TakeutiZaring] p. 18Exercise 18sspwb 4195  sspwimp 27827  sspwimpALT 27834  sspwimpALT2 27838  sspwimpcf 27829
[TakeutiZaring] p. 18Exercise 19pweqb 4202
[TakeutiZaring] p. 19Axiom 5ax-rep 4105
[TakeutiZaring] p. 20Definitiondf-rab 2527
[TakeutiZaring] p. 20Corollary 5.160ex 4124
[TakeutiZaring] p. 20Definition 5.12df-dif 3130
[TakeutiZaring] p. 20Definition 5.14dfnul2 3432
[TakeutiZaring] p. 20Proposition 5.15difid 3497  difidALT 3498
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3439  n0f 3438  neq0 3440
[TakeutiZaring] p. 21Axiom 6zfreg 7277
[TakeutiZaring] p. 21Axiom 6'zfregs 7382
[TakeutiZaring] p. 21Theorem 5.22setind 7387
[TakeutiZaring] p. 21Definition 5.20df-v 2765
[TakeutiZaring] p. 21Proposition 5.21vprc 4126
[TakeutiZaring] p. 22Exercise 10ss 3458
[TakeutiZaring] p. 22Exercise 3ssex 4132  ssexg 4134
[TakeutiZaring] p. 22Exercise 4inex1 4129
[TakeutiZaring] p. 22Exercise 5ruv 7282
[TakeutiZaring] p. 22Exercise 6elirr 7280
[TakeutiZaring] p. 22Exercise 7ssdif0 3488
[TakeutiZaring] p. 22Exercise 11difdif 3277
[TakeutiZaring] p. 22Exercise 13undif3 3404  undif3VD 27791
[TakeutiZaring] p. 22Exercise 14difss 3278
[TakeutiZaring] p. 22Exercise 15sscon 3285
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2523
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2524
[TakeutiZaring] p. 23Proposition 6.2xpex 4789  xpexg 4788  xpexgALT 6004
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4676
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5250
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5383  fun11 5253
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5206  svrelfun 5251
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4855
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4857
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4681
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4682
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4678
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5116  dfrel2 5112
[TakeutiZaring] p. 25Exercise 3xpss 4781
[TakeutiZaring] p. 25Exercise 5relun 4790
[TakeutiZaring] p. 25Exercise 6reluni 4796
[TakeutiZaring] p. 25Exercise 9inxp 4806
[TakeutiZaring] p. 25Exercise 12relres 4971
[TakeutiZaring] p. 25Exercise 13opelres 4948  opelresg 4950
[TakeutiZaring] p. 25Exercise 14dmres 4964
[TakeutiZaring] p. 25Exercise 15resss 4967
[TakeutiZaring] p. 25Exercise 17resabs1 4972
[TakeutiZaring] p. 25Exercise 18funres 5231
[TakeutiZaring] p. 25Exercise 24relco 5158
[TakeutiZaring] p. 25Exercise 29funco 5230
[TakeutiZaring] p. 25Exercise 30f1co 5384
[TakeutiZaring] p. 26Definition 6.10eu2 2143
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 4689  fv3 5474
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5196  cnvexg 5195
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4929  dmexg 4927
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4930  rnexg 4928
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27027
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27028
[TakeutiZaring] p. 27Corollary 6.13fvex 5472
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5477  tz6.12 5478  tz6.12c 5481
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5480  tz6.12i 5482
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4684
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4685
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4687  wfo 4671
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4686  wf1 4670
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4688  wf1o 4672
[TakeutiZaring] p. 28Exercise 4eqfnfv 5556  eqfnfv2 5557  eqfnfv2f 5560
[TakeutiZaring] p. 28Exercise 5fvco 5529
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5675  fnexALT 5676
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5671  resfunexgALT 5672
[TakeutiZaring] p. 29Exercise 9funimaex 5268  funimaexg 5267
[TakeutiZaring] p. 29Definition 6.18df-br 3998
[TakeutiZaring] p. 30Definition 6.21dffr2 4330  dffr3 5033  eliniseg 5030  iniseg 5032
[TakeutiZaring] p. 30Definition 6.22df-eprel 4277
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4343  fr3nr 4543  frirr 4342
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4324
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4545
[TakeutiZaring] p. 31Exercise 1frss 4332
[TakeutiZaring] p. 31Exercise 4wess 4352
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23575  tz6.26i 23576  wefrc 4359  wereu2 4362
[TakeutiZaring] p. 32Theorem 6.27wfi 23577  wfii 23578
[TakeutiZaring] p. 32Definition 6.28df-isom 4690
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5760
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5761
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5767
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5768
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5769
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5773
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5780
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5782
[TakeutiZaring] p. 35Notationwtr 4087
[TakeutiZaring] p. 35Theorem 7.2trelpss 27029  tz7.2 4349
[TakeutiZaring] p. 35Definition 7.1dftr3 4091
[TakeutiZaring] p. 36Proposition 7.4ordwe 4377
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4385
[TakeutiZaring] p. 36Proposition 7.6ordelord 4386  ordelordALT 27437  ordelordALTVD 27776
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4392  ordelssne 4391
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4390
[TakeutiZaring] p. 37Proposition 7.9ordin 4394
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4552
[TakeutiZaring] p. 38Corollary 7.15ordsson 4553
[TakeutiZaring] p. 38Definition 7.11df-on 4368
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4396
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27450  ordon 4546
[TakeutiZaring] p. 38Proposition 7.13onprc 4548
[TakeutiZaring] p. 39Theorem 7.17tfi 4616
[TakeutiZaring] p. 40Exercise 3ontr2 4411
[TakeutiZaring] p. 40Exercise 7dftr2 4089
[TakeutiZaring] p. 40Exercise 9onssmin 4560
[TakeutiZaring] p. 40Exercise 11unon 4594
[TakeutiZaring] p. 40Exercise 12ordun 4466
[TakeutiZaring] p. 40Exercise 14ordequn 4465
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4549
[TakeutiZaring] p. 40Proposition 7.20elssuni 3829
[TakeutiZaring] p. 41Definition 7.22df-suc 4370
[TakeutiZaring] p. 41Proposition 7.23sssucid 4441  sucidg 4442
[TakeutiZaring] p. 41Proposition 7.24suceloni 4576
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4456  ordnbtwn 4455
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4591
[TakeutiZaring] p. 42Exercise 1df-lim 4369
[TakeutiZaring] p. 42Exercise 4omssnlim 4642
[TakeutiZaring] p. 42Exercise 7ssnlim 4646
[TakeutiZaring] p. 42Exercise 8onsucssi 4604  ordelsuc 4583
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4585
[TakeutiZaring] p. 42Definition 7.27nlimon 4614
[TakeutiZaring] p. 42Definition 7.28dfom2 4630
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4647
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4648
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4649
[TakeutiZaring] p. 43Remarkomon 4639
[TakeutiZaring] p. 43Axiom 7inf3 7304  omex 7312
[TakeutiZaring] p. 43Theorem 7.32ordom 4637
[TakeutiZaring] p. 43Corollary 7.31find 4653
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4650
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4651
[TakeutiZaring] p. 44Exercise 1limomss 4633
[TakeutiZaring] p. 44Exercise 2int0 3850  trint0 4104
[TakeutiZaring] p. 44Exercise 4intss1 3851
[TakeutiZaring] p. 44Exercise 5intex 4143
[TakeutiZaring] p. 44Exercise 6oninton 4563
[TakeutiZaring] p. 44Exercise 11ordintdif 4413
[TakeutiZaring] p. 44Definition 7.35df-int 3837
[TakeutiZaring] p. 44Proposition 7.34noinfep 7328
[TakeutiZaring] p. 45Exercise 4onint 4558
[TakeutiZaring] p. 47Lemma 1tfrlem1 6359
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6381
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6382
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6383
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6387  tz7.44-2 6388  tz7.44-3 6389
[TakeutiZaring] p. 50Exercise 1smogt 6352
[TakeutiZaring] p. 50Exercise 3smoiso 6347
[TakeutiZaring] p. 50Definition 7.46df-smo 6331
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6425  tz7.49c 6426
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6423
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6422
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6424
[TakeutiZaring] p. 53Proposition 7.532eu5 2202
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7607
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7608
[TakeutiZaring] p. 56Definition 8.1oalim 6499  oasuc 6491
[TakeutiZaring] p. 57Remarktfindsg 4623
[TakeutiZaring] p. 57Proposition 8.2oacl 6502
[TakeutiZaring] p. 57Proposition 8.3oa0 6483  oa0r 6505
[TakeutiZaring] p. 57Proposition 8.16omcl 6503
[TakeutiZaring] p. 58Corollary 8.5oacan 6514
[TakeutiZaring] p. 58Proposition 8.4nnaord 6585  nnaordi 6584  oaord 6513  oaordi 6512
[TakeutiZaring] p. 59Proposition 8.6iunss2 3921  uniss2 3832
[TakeutiZaring] p. 59Proposition 8.7oawordri 6516
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6521  oawordex 6523
[TakeutiZaring] p. 59Proposition 8.9nnacl 6577
[TakeutiZaring] p. 59Proposition 8.10oaabs 6610
[TakeutiZaring] p. 60Remarkoancom 7320
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6526
[TakeutiZaring] p. 62Exercise 1nnarcl 6582
[TakeutiZaring] p. 62Exercise 5oaword1 6518
[TakeutiZaring] p. 62Definition 8.15om0 6484  om0x 6486  omlim 6500  omsuc 6493
[TakeutiZaring] p. 63Proposition 8.17nnecl 6579  nnmcl 6578
[TakeutiZaring] p. 63Proposition 8.19nnmord 6598  nnmordi 6597  omord 6534  omordi 6532
[TakeutiZaring] p. 63Proposition 8.20omcan 6535
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6602  omwordri 6538
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6506
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6508  om1r 6509
[TakeutiZaring] p. 64Proposition 8.22om00 6541
[TakeutiZaring] p. 64Proposition 8.23omordlim 6543
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6544
[TakeutiZaring] p. 64Proposition 8.25odi 6545
[TakeutiZaring] p. 65Theorem 8.26omass 6546
[TakeutiZaring] p. 67Definition 8.30nnesuc 6574  oe0 6489  oelim 6501  oesuc 6494  onesuc 6497
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6487
[TakeutiZaring] p. 67Proposition 8.32oen0 6552
[TakeutiZaring] p. 67Proposition 8.33oeordi 6553
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6488
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6511
[TakeutiZaring] p. 68Corollary 8.34oeord 6554
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6560
[TakeutiZaring] p. 68Proposition 8.35oewordri 6558
[TakeutiZaring] p. 68Proposition 8.37oeworde 6559
[TakeutiZaring] p. 69Proposition 8.41oeoa 6563
[TakeutiZaring] p. 70Proposition 8.42oeoe 6565
[TakeutiZaring] p. 73Theorem 9.1trcl 7378  tz9.1 7379
[TakeutiZaring] p. 76Definition 9.9df-r1 7404  r10 7408  r1lim 7412  r1limg 7411  r1suc 7410  r1sucg 7409
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7420  r1ord2 7421  r1ordg 7418
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7430
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7455  tz9.13 7431  tz9.13g 7432
[TakeutiZaring] p. 79Definition 9.14df-rank 7405  rankval 7456  rankvalb 7437  rankvalg 7457
[TakeutiZaring] p. 79Proposition 9.16rankel 7479  rankelb 7464
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7493  rankval3 7480  rankval3b 7466
[TakeutiZaring] p. 79Proposition 9.18rankonid 7469
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7435
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7474  rankr1c 7461  rankr1g 7472
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7475
[TakeutiZaring] p. 80Exercise 1rankss 7489  rankssb 7488
[TakeutiZaring] p. 80Exercise 2unbndrank 7482
[TakeutiZaring] p. 80Proposition 9.19bndrank 7481
[TakeutiZaring] p. 83Axiom of Choiceac4 8070  dfac3 7716
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7625  numth 8067  numth2 8066
[TakeutiZaring] p. 85Definition 10.4cardval 8136
[TakeutiZaring] p. 85Proposition 10.5cardid 8137  cardid2 7554
[TakeutiZaring] p. 85Proposition 10.9oncard 7561
[TakeutiZaring] p. 85Proposition 10.10carden 8141
[TakeutiZaring] p. 85Proposition 10.11cardidm 7560
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7545
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7566
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7558
[TakeutiZaring] p. 87Proposition 10.15pwen 7002
[TakeutiZaring] p. 88Exercise 1en0 6892
[TakeutiZaring] p. 88Exercise 7infensuc 7007
[TakeutiZaring] p. 89Exercise 10omxpen 6932
[TakeutiZaring] p. 90Corollary 10.23cardnn 7564
[TakeutiZaring] p. 90Definition 10.27alephiso 7693
[TakeutiZaring] p. 90Proposition 10.20nneneq 7012
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7018
[TakeutiZaring] p. 90Proposition 10.26alephprc 7694
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7017
[TakeutiZaring] p. 91Exercise 2alephle 7683
[TakeutiZaring] p. 91Exercise 3aleph0 7661
[TakeutiZaring] p. 91Exercise 4cardlim 7573
[TakeutiZaring] p. 91Exercise 7infpss 7811
[TakeutiZaring] p. 91Exercise 8infcntss 7098
[TakeutiZaring] p. 91Definition 10.29df-fin 6835  isfi 6853
[TakeutiZaring] p. 92Proposition 10.32onfin 7019
[TakeutiZaring] p. 92Proposition 10.34imadomg 8127
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6925
[TakeutiZaring] p. 93Proposition 10.35fodomb 8119
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7783  unxpdom 7038
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7575  cardsdomelir 7574
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7040
[TakeutiZaring] p. 94Proposition 10.39infxpen 7610
[TakeutiZaring] p. 95Definition 10.42df-map 6742
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8152  infxpidm2 7612
[TakeutiZaring] p. 95Proposition 10.41infcda 7802  infxp 7809  infxpg 24462
[TakeutiZaring] p. 96Proposition 10.44pw2en 6937  pw2f1o 6935
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6995
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8082
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8077  ac6s5 8086
[TakeutiZaring] p. 98Theorem 10.47unidom 8133
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8134  uniimadomf 8135
[TakeutiZaring] p. 100Definition 11.1cfcof 7868
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7863
[TakeutiZaring] p. 102Exercise 1cfle 7848
[TakeutiZaring] p. 102Exercise 2cf0 7845
[TakeutiZaring] p. 102Exercise 3cfsuc 7851
[TakeutiZaring] p. 102Exercise 4cfom 7858
[TakeutiZaring] p. 102Proposition 11.9coftr 7867
[TakeutiZaring] p. 103Theorem 11.15alephreg 8172
[TakeutiZaring] p. 103Proposition 11.11cardcf 7846
[TakeutiZaring] p. 103Proposition 11.13alephsing 7870
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7692
[TakeutiZaring] p. 104Proposition 11.16carduniima 7691
[TakeutiZaring] p. 104Proposition 11.18alephfp 7703  alephfp2 7704
[TakeutiZaring] p. 106Theorem 11.20gchina 8289
[TakeutiZaring] p. 106Theorem 11.21mappwen 7707
[TakeutiZaring] p. 107Theorem 11.26konigth 8159
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8173
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8174
[Tarski] p. 67Axiom B5ax-4 1692
[Tarski] p. 68Lemma 6avril1 20797  equid 1818  equid1 1820  equidALT 1819
[Tarski] p. 69Lemma 7equcomi-o 1823  equcomi 1822
[Tarski] p. 70Lemma 14a4im 1868  a4ime 1869
[Tarski] p. 70Lemma 16ax-11 1624  ax-11o 1941  ax11i 1833
[Tarski] p. 70Lemmas 16 and 17sb6 1993
[Tarski] p. 75Axiom B8ax-9v 1632
[Tarski] p. 75Scheme B7ax9vax9 28408
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1628
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1625  ax-14 1626
[Truss] p. 114Theorem 5.18ruc 12484
[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 2215  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 27836
[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.27pm2.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 24296
[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 24289
[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 26921
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26922
[WhiteheadRussell] p. 147Theorem *10.2219.26 1592
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26923
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26924
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26925
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1617
[WhiteheadRussell] p. 151Theorem *10.301albitr 26926
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26927
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26928
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26929
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26930
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26932
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26933
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26934
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26931
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26937
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2078
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26938
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26939
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1610
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26940
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26941
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26942
[WhiteheadRussell] p. 162Theorem *11.322alim 26943
[WhiteheadRussell] p. 162Theorem *11.332albi 26944
[WhiteheadRussell] p. 162Theorem *11.342exim 26945
[WhiteheadRussell] p. 162Theorem *11.36a4sbce-2 26947
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26946
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1609
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26949
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26950
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26948
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1571
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26951
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26952
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1578
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26953
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2025  pm11.53g 24331
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26954
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26959
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26955
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26956
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26957
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26958
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26963
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26960
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26961
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26962
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26964
[WhiteheadRussell] p. 175Definition *14.02df-eu 2122
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 26976  pm13.13b 26977
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 26978
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2493
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2494
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2883
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 26984
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 26985
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 26979
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27454  pm13.193 26980
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 26981
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 26982
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 26983
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 26990
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 26989
[WhiteheadRussell] p. 184Definition *14.01iotasbc 26988
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3018
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 26991  pm14.122b 26992  pm14.122c 26993
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 26994  pm14.123b 26995  pm14.123c 26996
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 26998
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 26997
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 26999
[WhiteheadRussell] p. 190Theorem *14.22iota4 6243
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27000
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6244
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27001
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27003
[WhiteheadRussell] p. 192Theorem *14.26eupick 2181  eupickbi 2184  sbaniota 27004
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27002
[WhiteheadRussell] p. 192Theorem *14.271eubi 27005
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27006
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 4689
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7601  pm54.43lem 7600
[Young] p. 141Definition of operator orderingleop2 22665
[Young] p. 142Example 12.2(i)0leop 22671  idleop 22672
[vandenDries] p. 42Lemma 61irrapx1 26281
[vandenDries] p. 43Theorem 62pellex 26288  pellexlem1 26282

This page was last updated on 13-Jul-2017.
Copyright terms: Public domain