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 13464
[Adamek] p. 29Proposition 3.14(1)invinv 13478
[Adamek] p. 29Proposition 3.14(2)invco 13479  isoco 13481
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25287
[AitkenIBCG] p. 3Definition 2df-angtrg 25283  df-trcng 25286
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25159  df-ig2 25158
[AitkenIBG] p. 2Definition 4df-li 25174
[AitkenIBG] p. 3Definition 5df-col 25188
[AitkenIBG] p. 3Definition 6df-con2 25193
[AitkenIBG] p. 3Proposition 4isconcl5a 25198  isconcl5ab 25199  isconcl6a 25200  isconcl6ab 25201
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25206
[AitkenIBG] p. 4Exercise 5tpne 25172
[AitkenIBG] p. 4Definition 8df-seg2 25228
[AitkenIBG] p. 4Definition 10df-sside 25260
[AitkenIBG] p. 4Definition 11df-ray2 25249
[AitkenIBG] p. 10Definition 17df-angle 25255
[AitkenIBG] p. 15Definition 23df-triangle 25257
[AitkenIBG] p. 15Definition 24df-cnvx 25276
[AitkenNG] p. 2Definition 1df-slices 25290
[AitkenNG] p. 2Definition 2df-Cut 25292
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25294
[AitkenNG] p. 4Definition 5df-crcl 25296
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18011  df-nmoo 21084
[AkhiezerGlazman] p. 64Theoremhmopidmch 22494  hmopidmchi 22492
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22542  pjcmul2i 22543
[AkhiezerGlazman] p. 72Theoremcnvunop 22259  unoplin 22261
[AkhiezerGlazman] p. 72Equation 2unopadj 22260  unopadj2 22279
[AkhiezerGlazman] p. 73Theoremelunop2 22354  lnopunii 22353
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22427
[Apostol] p. 18Theorem I.1addcan 8872  addcan2d 8892  addcan2i 8882  addcand 8891  addcani 8881
[Apostol] p. 18Theorem I.2negeu 8914
[Apostol] p. 18Theorem I.3negsub 8967  negsubd 9031  negsubi 8996
[Apostol] p. 18Theorem I.4negneg 8969  negnegd 9020  negnegi 8988
[Apostol] p. 18Theorem I.5subdi 9074  subdid 9096  subdii 9089  subdir 9075  subdird 9097  subdiri 9090
[Apostol] p. 18Theorem I.6mul01 8867  mul01d 8887  mul01i 8878  mul02 8866  mul02d 8886  mul02i 8877
[Apostol] p. 18Theorem I.7mulcan 9263  mulcan2d 9262  mulcand 9261  mulcani 9265
[Apostol] p. 18Theorem I.8receu 9271
[Apostol] p. 18Theorem I.9divrec 9296  divrecd 9393  divreci 9359  divreczi 9352
[Apostol] p. 18Theorem I.10recrec 9313  recreci 9346
[Apostol] p. 18Theorem I.11mul0or 9266  mul0ord 9276  mul0ori 9274
[Apostol] p. 18Theorem I.12mul2neg 9080  mul2negd 9095  mul2negi 9088  mulneg1 9077  mulneg1d 9093  mulneg1i 9086
[Apostol] p. 18Theorem I.13divadddiv 9331  divadddivd 9430  divadddivi 9376
[Apostol] p. 18Theorem I.14divmuldiv 9316  divmuldivd 9427  divmuldivi 9374
[Apostol] p. 18Theorem I.15divdivdiv 9317  divdivdivd 9433  divdivdivi 9377
[Apostol] p. 20Axiom 7rpaddcl 10220  rpaddcld 10251  rpmulcl 10221  rpmulcld 10252
[Apostol] p. 20Axiom 8rpneg 10229
[Apostol] p. 20Axiom 90nrp 10230
[Apostol] p. 20Theorem I.17lttri 8821
[Apostol] p. 20Theorem I.18ltadd1d 9225  ltadd1dd 9243  ltadd1i 9188
[Apostol] p. 20Theorem I.19ltmul1 9454  ltmul1a 9453  ltmul1i 9523  ltmul1ii 9533  ltmul2 9455  ltmul2d 10274  ltmul2dd 10288  ltmul2i 9526
[Apostol] p. 20Theorem I.20msqgt0 9155  msqgt0d 9200  msqgt0i 9171
[Apostol] p. 20Theorem I.210lt1 9157
[Apostol] p. 20Theorem I.23lt0neg1 9141  lt0neg1d 9202  ltneg 9135  ltnegd 9210  ltnegi 9178
[Apostol] p. 20Theorem I.25lt2add 9120  lt2addd 9254  lt2addi 9196
[Apostol] p. 20Definition of positive numbersdf-rp 10201
[Apostol] p. 21Exercise 4recgt0 9448  recgt0d 9539  recgt0i 9509  recgt0ii 9510
[Apostol] p. 22Definition of integersdf-z 9871
[Apostol] p. 22Definition of positive integersdfnn3 9608
[Apostol] p. 22Definition of rationalsdf-q 10163
[Apostol] p. 24Theorem I.26supeu 7086
[Apostol] p. 26Theorem I.28nnunb 9807
[Apostol] p. 26Theorem I.29arch 9808
[Apostol] p. 28Exercise 2btwnz 9960
[Apostol] p. 28Exercise 3nnrecl 9809
[Apostol] p. 28Exercise 4rebtwnz 10161
[Apostol] p. 28Exercise 5zbtwnre 10160
[Apostol] p. 28Exercise 6qbtwnre 10371
[Apostol] p. 28Exercise 10(a)zneo 9940
[Apostol] p. 29Theorem I.35msqsqrd 11761  resqrth 11582  sqrth 11687  sqrthi 11693  sqsqrd 11760
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9597
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10130
[Apostol] p. 361Remarkcrreczi 11068
[Apostol] p. 363Remarkabsgt0i 11721
[Apostol] p. 363Exampleabssubd 11774  abssubi 11725
[Baer] p. 40Property (b)mapdord 30392
[Baer] p. 40Property (c)mapd11 30393
[Baer] p. 40Property (e)mapdin 30416  mapdlsm 30418
[Baer] p. 40Property (f)mapd0 30419
[Baer] p. 40Definition of projectivitydf-mapd 30379  mapd1o 30402
[Baer] p. 41Property (g)mapdat 30421
[Baer] p. 44Part (1)mapdpg 30460
[Baer] p. 45Part (2)hdmap1eq 30556  mapdheq 30482  mapdheq2 30483  mapdheq2biN 30484
[Baer] p. 45Part (3)baerlem3 30467
[Baer] p. 46Part (4)mapdheq4 30486  mapdheq4lem 30485
[Baer] p. 46Part (5)baerlem5a 30468  baerlem5abmN 30472  baerlem5amN 30470  baerlem5b 30469  baerlem5bmN 30471
[Baer] p. 47Part (6)hdmap1l6 30576  hdmap1l6a 30564  hdmap1l6e 30569  hdmap1l6f 30570  hdmap1l6g 30571  hdmap1l6lem1 30562  hdmap1l6lem2 30563  hdmap1p6N 30577  mapdh6N 30501  mapdh6aN 30489  mapdh6eN 30494  mapdh6fN 30495  mapdh6gN 30496  mapdh6lem1N 30487  mapdh6lem2N 30488
[Baer] p. 48Part 9hdmapval 30585
[Baer] p. 48Part 10hdmap10 30597
[Baer] p. 48Part 11hdmapadd 30600
[Baer] p. 48Part (6)hdmap1l6h 30572  mapdh6hN 30497
[Baer] p. 48Part (7)mapdh75cN 30507  mapdh75d 30508  mapdh75e 30506  mapdh75fN 30509  mapdh7cN 30503  mapdh7dN 30504  mapdh7eN 30502  mapdh7fN 30505
[Baer] p. 48Part (8)mapdh8 30543  mapdh8a 30529  mapdh8aa 30530  mapdh8ab 30531  mapdh8ac 30532  mapdh8ad 30533  mapdh8b 30534  mapdh8c 30535  mapdh8d 30537  mapdh8d0N 30536  mapdh8e 30538  mapdh8fN 30539  mapdh8g 30540  mapdh8i 30541  mapdh8j 30542
[Baer] p. 48Part (9)mapdh9a 30544
[Baer] p. 48Equation 10mapdhvmap 30523
[Baer] p. 49Part 12hdmap11 30605  hdmapeq0 30601  hdmapf1oN 30622  hdmapneg 30603  hdmaprnN 30621  hdmaprnlem1N 30606  hdmaprnlem3N 30607  hdmaprnlem3uN 30608  hdmaprnlem4N 30610  hdmaprnlem6N 30611  hdmaprnlem7N 30612  hdmaprnlem8N 30613  hdmaprnlem9N 30614  hdmapsub 30604
[Baer] p. 49Part 14hdmap14lem1 30625  hdmap14lem10 30634  hdmap14lem1a 30623  hdmap14lem2N 30626  hdmap14lem2a 30624  hdmap14lem3 30627  hdmap14lem8 30632  hdmap14lem9 30633
[Baer] p. 50Part 14hdmap14lem11 30635  hdmap14lem12 30636  hdmap14lem13 30637  hdmap14lem14 30638  hdmap14lem15 30639  hgmapval 30644
[Baer] p. 50Part 15hgmapadd 30651  hgmapmul 30652  hgmaprnlem2N 30654  hgmapvs 30648
[Baer] p. 50Part 16hgmaprnN 30658
[Baer] p. 110Lemma 1hdmapip0com 30674
[Baer] p. 110Line 27hdmapinvlem1 30675
[Baer] p. 110Line 28hdmapinvlem2 30676
[Baer] p. 110Line 30hdmapinvlem3 30677
[Baer] p. 110Part 1.2hdmapglem5 30679  hgmapvv 30683
[Baer] p. 110Proposition 1hdmapinvlem4 30678
[Baer] p. 111Line 10hgmapvvlem1 30680
[Baer] p. 111Line 15hdmapg 30687  hdmapglem7 30686
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2118
[BellMachover] p. 460Notationdf-mo 2119
[BellMachover] p. 460Definitionmo3 2144
[BellMachover] p. 461Axiom Extax-ext 2234
[BellMachover] p. 462Theorem 1.1bm1.1 2238
[BellMachover] p. 463Axiom Repaxrep5 4030
[BellMachover] p. 463Scheme Sepaxsep 4034
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4038
[BellMachover] p. 466Axiom Powaxpow3 4082
[BellMachover] p. 466Axiom Unionaxun2 4402
[BellMachover] p. 468Definitiondf-ord 4285
[BellMachover] p. 469Theorem 2.2(i)ordirr 4300
[BellMachover] p. 469Theorem 2.2(iii)onelon 4307
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4302
[BellMachover] p. 471Definition of Ndf-om 4545
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4485
[BellMachover] p. 471Definition of Limdf-lim 4287
[BellMachover] p. 472Axiom Infzfinf2 7224
[BellMachover] p. 473Theorem 2.8limom 4559
[BellMachover] p. 477Equation 3.1df-r1 7317
[BellMachover] p. 478Definitionrankval2 7371
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7335  r1ord3g 7332
[BellMachover] p. 480Axiom Regzfreg2 7191
[BellMachover] p. 488Axiom ACac5 7985  dfac4 7630
[BellMachover] p. 490Definition of alephalephval3 7618
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28073
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22694
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22736  chirredi 22735
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22724
[Beran] p. 3Definition of joinsshjval3 21694
[Beran] p. 39Theorem 2.3(i)cmcm2 21974  cmcm2i 21951  cmcm2ii 21956  cmt2N 28004
[Beran] p. 40Theorem 2.3(iii)lecm 21975  lecmi 21960  lecmii 21961
[Beran] p. 45Theorem 3.4cmcmlem 21949
[Beran] p. 49Theorem 4.2cm2j 21978  cm2ji 21983  cm2mi 21984
[Beran] p. 95Definitiondf-sh 21547  issh2 21549
[Beran] p. 95Lemma 3.1(S5)his5 21426
[Beran] p. 95Lemma 3.1(S6)his6 21439
[Beran] p. 95Lemma 3.1(S7)his7 21430
[Beran] p. 95Lemma 3.2(S8)ho01i 22169
[Beran] p. 95Lemma 3.2(S9)hoeq1 22171
[Beran] p. 95Lemma 3.2(S10)ho02i 22170
[Beran] p. 95Lemma 3.2(S11)hoeq2 22172
[Beran] p. 95Postulate (S1)ax-his1 21422  his1i 21440
[Beran] p. 95Postulate (S2)ax-his2 21423
[Beran] p. 95Postulate (S3)ax-his3 21424
[Beran] p. 95Postulate (S4)ax-his4 21425
[Beran] p. 96Definition of normdf-hnorm 21309  dfhnorm2 21462  normval 21464
[Beran] p. 96Definition for Cauchy sequencehcau 21524
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21314
[Beran] p. 96Definition of complete subspaceisch3 21582
[Beran] p. 96Definition of convergedf-hlim 21313  hlimi 21528
[Beran] p. 97Theorem 3.3(i)norm-i-i 21473  norm-i 21469
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21477  norm-ii 21478  normlem0 21449  normlem1 21450  normlem2 21451  normlem3 21452  normlem4 21453  normlem5 21454  normlem6 21455  normlem7 21456  normlem7tALT 21459
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21479  norm-iii 21480
[Beran] p. 98Remark 3.4bcs 21521  bcsiALT 21519  bcsiHIL 21520
[Beran] p. 98Remark 3.4(B)normlem9at 21461  normpar 21495  normpari 21494
[Beran] p. 98Remark 3.4(C)normpyc 21486  normpyth 21485  normpythi 21482
[Beran] p. 99Remarklnfn0 22388  lnfn0i 22383  lnop0 22307  lnop0i 22311
[Beran] p. 99Theorem 3.5(i)nmcexi 22367  nmcfnex 22394  nmcfnexi 22392  nmcopex 22370  nmcopexi 22368
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22395  nmcfnlbi 22393  nmcoplb 22371  nmcoplbi 22369
[Beran] p. 99Theorem 3.5(iii)lnfncon 22397  lnfnconi 22396  lnopcon 22376  lnopconi 22375
[Beran] p. 100Lemma 3.6normpar2i 21496
[Beran] p. 101Lemma 3.6norm3adifi 21493  norm3adifii 21488  norm3dif 21490  norm3difi 21487
[Beran] p. 102Theorem 3.7(i)chocunii 21641  pjhth 21733  pjhtheu 21734  pjpjhth 21765  pjpjhthi 21766  pjth 18597
[Beran] p. 102Theorem 3.7(ii)ococ 21746  ococi 21745
[Beran] p. 103Remark 3.8nlelchi 22402
[Beran] p. 104Theorem 3.9riesz3i 22403  riesz4 22405  riesz4i 22404
[Beran] p. 104Theorem 3.10cnlnadj 22420  cnlnadjeu 22419  cnlnadjeui 22418  cnlnadji 22417  cnlnadjlem1 22408  nmopadjlei 22429
[Beran] p. 106Theorem 3.11(i)adjeq0 22432
[Beran] p. 106Theorem 3.11(v)nmopadji 22431
[Beran] p. 106Theorem 3.11(ii)adjmul 22433
[Beran] p. 106Theorem 3.11(iv)adjadj 22277
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22443  nmopcoadji 22442
[Beran] p. 106Theorem 3.11(iii)adjadd 22434
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22444
[Beran] p. 106Theorem 3.11(viii)adjcoi 22441  pjadj2coi 22545  pjadjcoi 22502
[Beran] p. 107Definitiondf-ch 21562  isch2 21564
[Beran] p. 107Remark 3.12choccl 21646  isch3 21582  occl 21644  ocsh 21623  shoccl 21645  shocsh 21624
[Beran] p. 107Remark 3.12(B)ococin 21748
[Beran] p. 108Theorem 3.13chintcl 21672
[Beran] p. 109Property (i)pjadj2 22528  pjadj3 22529  pjadji 22043  pjadjii 22032
[Beran] p. 109Property (ii)pjidmco 22522  pjidmcoi 22518  pjidmi 22031
[Beran] p. 110Definition of projector orderingpjordi 22514
[Beran] p. 111Remarkho0val 22091  pjch1 22028
[Beran] p. 111Definitiondf-hfmul 21927  df-hfsum 21926  df-hodif 21925  df-homul 21924  df-hosum 21923
[Beran] p. 111Lemma 4.4(i)pjo 22029
[Beran] p. 111Lemma 4.4(ii)pjch 22052  pjchi 21772
[Beran] p. 111Lemma 4.4(iii)pjoc2 21779  pjoc2i 21778
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22038
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22506  pjssmii 22039
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22505
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22504
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22509
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22507  pjssge0ii 22040
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22508  pjdifnormii 22041
[BourbakiEns] p. Proposition 8fcof1 5646  fcofo 5647
[BourbakiFVR] p. Definition 1isder 24804
[BourbakiTop1] p. Remarkxnegmnf 10382  xnegpnf 10381
[BourbakiTop1] p. Remark rexneg 10383
[BourbakiTop1] p. Theoremneiss 16640
[BourbakiTop1] p. Axiom GT'tgpsubcn 17567
[BourbakiTop1] p. Example 1snfil 17353
[BourbakiTop1] p. Example 2neifil 17369
[BourbakiTop1] p. Definitionistgp 17554
[BourbakiTop1] p. Propositioncnpco 16790  ishmeo 17244  neips 16644
[BourbakiTop1] p. Definition 1filintn0 17350
[BourbakiTop1] p. Proposition 9cnpflf2 17489
[BourbakiTop1] p. Theorem 1 (d)iscncl 16792
[BourbakiTop1] p. Proposition Vissnei2 16647
[BourbakiTop1] p. Definition C'''df-cmp 16908
[BourbakiTop1] p. Proposition Viiinnei 16656
[BourbakiTop1] p. Proposition Vivneissex 16658
[BourbakiTop1] p. Proposition Viiielnei 16642  ssnei 16641
[BourbakiTop1] p. Remark below def. 1filn0 17351
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17335
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17352
[ChoquetDD] p. 2Definition of mappingdf-mpt 3973
[Cohen] p. 301Remarkrelogoprlem 19730
[Cohen] p. 301Property 2relogmul 19731  relogmuld 19760
[Cohen] p. 301Property 3relogdiv 19732  relogdivd 19761
[Cohen] p. 301Property 4relogexp 19735
[Cohen] p. 301Property 1alog1 19725
[Cohen] p. 301Property 1bloge 19726
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10808
[Crawley] p. 1Definition of posetdf-poset 13886
[Crawley] p. 107Theorem 13.2hlsupr 28139
[Crawley] p. 110Theorem 13.3arglem1N 28943  dalaw 28639
[Crawley] p. 111Theorem 13.4hlathil 30718
[Crawley] p. 111Definition of set Wdf-watsN 28743
[Crawley] p. 111Definition of dilationdf-dilN 28859  df-ldil 28857  isldil 28863
[Crawley] p. 111Definition of translationdf-ltrn 28858  df-trnN 28860  isltrn 28872  ltrnu 28874
[Crawley] p. 112Lemma Acdlema1N 28544  cdlema2N 28545  exatleN 28157
[Crawley] p. 112Lemma B1cvrat 28229  cdlemb 28547  cdlemb2 28794  cdlemb3 29359  idltrn 28903  l1cvat 27809  lhpat 28796  lhpat2 28798  lshpat 27810  ltrnel 28892  ltrnmw 28904
[Crawley] p. 112Lemma Ccdlemc1 28944  cdlemc2 28945  ltrnnidn 28927  trlat 28922  trljat1 28919  trljat2 28920  trljat3 28921  trlne 28938  trlnidat 28926  trlnle 28939
[Crawley] p. 112Definition of automorphismdf-pautN 28744
[Crawley] p. 113Lemma Ccdlemc 28950  cdlemc3 28946  cdlemc4 28947
[Crawley] p. 113Lemma Dcdlemd 28960  cdlemd1 28951  cdlemd2 28952  cdlemd3 28953  cdlemd4 28954  cdlemd5 28955  cdlemd6 28956  cdlemd7 28957  cdlemd8 28958  cdlemd9 28959  cdleme31sde 29138  cdleme31se 29135  cdleme31se2 29136  cdleme31snd 29139  cdleme32a 29194  cdleme32b 29195  cdleme32c 29196  cdleme32d 29197  cdleme32e 29198  cdleme32f 29199  cdleme32fva 29190  cdleme32fva1 29191  cdleme32fvcl 29193  cdleme32le 29200  cdleme48fv 29252  cdleme4gfv 29260  cdleme50eq 29294  cdleme50f 29295  cdleme50f1 29296  cdleme50f1o 29299  cdleme50laut 29300  cdleme50ldil 29301  cdleme50lebi 29293  cdleme50rn 29298  cdleme50rnlem 29297  cdlemeg49le 29264  cdlemeg49lebilem 29292
[Crawley] p. 113Lemma Ecdleme 29313  cdleme00a 28962  cdleme01N 28974  cdleme02N 28975  cdleme0a 28964  cdleme0aa 28963  cdleme0b 28965  cdleme0c 28966  cdleme0cp 28967  cdleme0cq 28968  cdleme0dN 28969  cdleme0e 28970  cdleme0ex1N 28976  cdleme0ex2N 28977  cdleme0fN 28971  cdleme0gN 28972  cdleme0moN 28978  cdleme1 28980  cdleme10 29007  cdleme10tN 29011  cdleme11 29023  cdleme11a 29013  cdleme11c 29014  cdleme11dN 29015  cdleme11e 29016  cdleme11fN 29017  cdleme11g 29018  cdleme11h 29019  cdleme11j 29020  cdleme11k 29021  cdleme11l 29022  cdleme12 29024  cdleme13 29025  cdleme14 29026  cdleme15 29031  cdleme15a 29027  cdleme15b 29028  cdleme15c 29029  cdleme15d 29030  cdleme16 29038  cdleme16aN 29012  cdleme16b 29032  cdleme16c 29033  cdleme16d 29034  cdleme16e 29035  cdleme16f 29036  cdleme16g 29037  cdleme19a 29056  cdleme19b 29057  cdleme19c 29058  cdleme19d 29059  cdleme19e 29060  cdleme19f 29061  cdleme1b 28979  cdleme2 28981  cdleme20aN 29062  cdleme20bN 29063  cdleme20c 29064  cdleme20d 29065  cdleme20e 29066  cdleme20f 29067  cdleme20g 29068  cdleme20h 29069  cdleme20i 29070  cdleme20j 29071  cdleme20k 29072  cdleme20l 29075  cdleme20l1 29073  cdleme20l2 29074  cdleme20m 29076  cdleme20y 29055  cdleme20zN 29054  cdleme21 29090  cdleme21d 29083  cdleme21e 29084  cdleme22a 29093  cdleme22aa 29092  cdleme22b 29094  cdleme22cN 29095  cdleme22d 29096  cdleme22e 29097  cdleme22eALTN 29098  cdleme22f 29099  cdleme22f2 29100  cdleme22g 29101  cdleme23a 29102  cdleme23b 29103  cdleme23c 29104  cdleme26e 29112  cdleme26eALTN 29114  cdleme26ee 29113  cdleme26f 29116  cdleme26f2 29118  cdleme26f2ALTN 29117  cdleme26fALTN 29115  cdleme27N 29122  cdleme27a 29120  cdleme27cl 29119  cdleme28c 29125  cdleme3 28990  cdleme30a 29131  cdleme31fv 29143  cdleme31fv1 29144  cdleme31fv1s 29145  cdleme31fv2 29146  cdleme31id 29147  cdleme31sc 29137  cdleme31sdnN 29140  cdleme31sn 29133  cdleme31sn1 29134  cdleme31sn1c 29141  cdleme31sn2 29142  cdleme31so 29132  cdleme35a 29201  cdleme35b 29203  cdleme35c 29204  cdleme35d 29205  cdleme35e 29206  cdleme35f 29207  cdleme35fnpq 29202  cdleme35g 29208  cdleme35h 29209  cdleme35h2 29210  cdleme35sn2aw 29211  cdleme35sn3a 29212  cdleme36a 29213  cdleme36m 29214  cdleme37m 29215  cdleme38m 29216  cdleme38n 29217  cdleme39a 29218  cdleme39n 29219  cdleme3b 28982  cdleme3c 28983  cdleme3d 28984  cdleme3e 28985  cdleme3fN 28986  cdleme3fa 28989  cdleme3g 28987  cdleme3h 28988  cdleme4 28991  cdleme40m 29220  cdleme40n 29221  cdleme40v 29222  cdleme40w 29223  cdleme41fva11 29230  cdleme41sn3aw 29227  cdleme41sn4aw 29228  cdleme41snaw 29229  cdleme42a 29224  cdleme42b 29231  cdleme42c 29225  cdleme42d 29226  cdleme42e 29232  cdleme42f 29233  cdleme42g 29234  cdleme42h 29235  cdleme42i 29236  cdleme42k 29237  cdleme42ke 29238  cdleme42keg 29239  cdleme42mN 29240  cdleme42mgN 29241  cdleme43aN 29242  cdleme43bN 29243  cdleme43cN 29244  cdleme43dN 29245  cdleme5 28993  cdleme50ex 29312  cdleme50ltrn 29310  cdleme51finvN 29309  cdleme51finvfvN 29308  cdleme51finvtrN 29311  cdleme6 28994  cdleme7 29002  cdleme7a 28996  cdleme7aa 28995  cdleme7b 28997  cdleme7c 28998  cdleme7d 28999  cdleme7e 29000  cdleme7ga 29001  cdleme8 29003  cdleme8tN 29008  cdleme9 29006  cdleme9a 29004  cdleme9b 29005  cdleme9tN 29010  cdleme9taN 29009  cdlemeda 29051  cdlemedb 29050  cdlemednpq 29052  cdlemednuN 29053  cdlemefr27cl 29156  cdlemefr32fva1 29163  cdlemefr32fvaN 29162  cdlemefrs32fva 29153  cdlemefrs32fva1 29154  cdlemefs27cl 29166  cdlemefs32fva1 29176  cdlemefs32fvaN 29175  cdlemesner 29049  cdlemeulpq 28973
[Crawley] p. 114Lemma E4atex 28829  4atexlem7 28828  cdleme0nex 29043  cdleme17a 29039  cdleme17c 29041  cdleme17d 29251  cdleme17d1 29042  cdleme17d2 29248  cdleme18a 29044  cdleme18b 29045  cdleme18c 29046  cdleme18d 29048  cdleme4a 28992
[Crawley] p. 115Lemma Ecdleme21a 29078  cdleme21at 29081  cdleme21b 29079  cdleme21c 29080  cdleme21ct 29082  cdleme21f 29085  cdleme21g 29086  cdleme21h 29087  cdleme21i 29088  cdleme22gb 29047
[Crawley] p. 116Lemma Fcdlemf 29316  cdlemf1 29314  cdlemf2 29315
[Crawley] p. 116Lemma Gcdlemftr1 29320  cdlemg16 29410  cdlemg28 29457  cdlemg28a 29446  cdlemg28b 29456  cdlemg3a 29350  cdlemg42 29482  cdlemg43 29483  cdlemg44 29486  cdlemg44a 29484  cdlemg46 29488  cdlemg47 29489  cdlemg9 29387  ltrnco 29472  ltrncom 29491  tgrpabl 29504  trlco 29480
[Crawley] p. 116Definition of Gdf-tgrp 29496
[Crawley] p. 117Lemma Gcdlemg17 29430  cdlemg17b 29415
[Crawley] p. 117Definition of Edf-edring-rN 29509  df-edring 29510
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 29513
[Crawley] p. 118Remarktendopltp 29533
[Crawley] p. 118Lemma Hcdlemh 29570  cdlemh1 29568  cdlemh2 29569
[Crawley] p. 118Lemma Icdlemi 29573  cdlemi1 29571  cdlemi2 29572
[Crawley] p. 118Lemma Jcdlemj1 29574  cdlemj2 29575  cdlemj3 29576  tendocan 29577
[Crawley] p. 118Lemma Kcdlemk 29727  cdlemk1 29584  cdlemk10 29596  cdlemk11 29602  cdlemk11t 29699  cdlemk11ta 29682  cdlemk11tb 29684  cdlemk11tc 29698  cdlemk11u-2N 29642  cdlemk11u 29624  cdlemk12 29603  cdlemk12u-2N 29643  cdlemk12u 29625  cdlemk13-2N 29629  cdlemk13 29605  cdlemk14-2N 29631  cdlemk14 29607  cdlemk15-2N 29632  cdlemk15 29608  cdlemk16-2N 29633  cdlemk16 29610  cdlemk16a 29609  cdlemk17-2N 29634  cdlemk17 29611  cdlemk18-2N 29639  cdlemk18-3N 29653  cdlemk18 29621  cdlemk19-2N 29640  cdlemk19 29622  cdlemk19u 29723  cdlemk1u 29612  cdlemk2 29585  cdlemk20-2N 29645  cdlemk20 29627  cdlemk21-2N 29644  cdlemk21N 29626  cdlemk22-3 29654  cdlemk22 29646  cdlemk23-3 29655  cdlemk24-3 29656  cdlemk25-3 29657  cdlemk26-3 29659  cdlemk26b-3 29658  cdlemk27-3 29660  cdlemk28-3 29661  cdlemk29-3 29664  cdlemk3 29586  cdlemk30 29647  cdlemk31 29649  cdlemk32 29650  cdlemk33N 29662  cdlemk34 29663  cdlemk35 29665  cdlemk36 29666  cdlemk37 29667  cdlemk38 29668  cdlemk39 29669  cdlemk39u 29721  cdlemk4 29587  cdlemk41 29673  cdlemk42 29694  cdlemk42yN 29697  cdlemk43N 29716  cdlemk45 29700  cdlemk46 29701  cdlemk47 29702  cdlemk48 29703  cdlemk49 29704  cdlemk5 29589  cdlemk50 29705  cdlemk51 29706  cdlemk52 29707  cdlemk53 29710  cdlemk54 29711  cdlemk55 29714  cdlemk55u 29719  cdlemk56 29724  cdlemk5a 29588  cdlemk5auN 29613  cdlemk5u 29614  cdlemk6 29590  cdlemk6u 29615  cdlemk7 29601  cdlemk7u-2N 29641  cdlemk7u 29623  cdlemk8 29591  cdlemk9 29592  cdlemk9bN 29593  cdlemki 29594  cdlemkid 29689  cdlemkj-2N 29635  cdlemkj 29616  cdlemksat 29599  cdlemksel 29598  cdlemksv 29597  cdlemksv2 29600  cdlemkuat 29619  cdlemkuel-2N 29637  cdlemkuel-3 29651  cdlemkuel 29618  cdlemkuv-2N 29636  cdlemkuv2-2 29638  cdlemkuv2-3N 29652  cdlemkuv2 29620  cdlemkuvN 29617  cdlemkvcl 29595  cdlemky 29679  cdlemkyyN 29715  tendoex 29728
[Crawley] p. 120Remarkdva1dim 29738
[Crawley] p. 120Lemma Lcdleml1N 29729  cdleml2N 29730  cdleml3N 29731  cdleml4N 29732  cdleml5N 29733  cdleml6 29734  cdleml7 29735  cdleml8 29736  cdleml9 29737  dia1dim 29815
[Crawley] p. 120Lemma Mdia11N 29802  diaf11N 29803  dialss 29800  diaord 29801  dibf11N 29915  djajN 29891
[Crawley] p. 120Definition of isomorphism mapdiaval 29786
[Crawley] p. 121Lemma Mcdlemm10N 29872  dia2dimlem1 29818  dia2dimlem2 29819  dia2dimlem3 29820  dia2dimlem4 29821  dia2dimlem5 29822  diaf1oN 29884  diarnN 29883  dvheveccl 29866  dvhopN 29870
[Crawley] p. 121Lemma Ncdlemn 29966  cdlemn10 29960  cdlemn11 29965  cdlemn11a 29961  cdlemn11b 29962  cdlemn11c 29963  cdlemn11pre 29964  cdlemn2 29949  cdlemn2a 29950  cdlemn3 29951  cdlemn4 29952  cdlemn4a 29953  cdlemn5 29955  cdlemn5pre 29954  cdlemn6 29956  cdlemn7 29957  cdlemn8 29958  cdlemn9 29959  diclspsn 29948
[Crawley] p. 121Definition of phi(q)df-dic 29927
[Crawley] p. 122Lemma Ndih11 30019  dihf11 30021  dihjust 29971  dihjustlem 29970  dihord 30018  dihord1 29972  dihord10 29977  dihord11b 29976  dihord11c 29978  dihord2 29981  dihord2a 29973  dihord2b 29974  dihord2cN 29975  dihord2pre 29979  dihord2pre2 29980  dihordlem6 29967  dihordlem7 29968  dihordlem7b 29969
[Crawley] p. 122Definition of isomorphism mapdihffval 29984  dihfval 29985  dihval 29986
[Eisenberg] p. 67Definition 5.3df-dif 3078
[Eisenberg] p. 82Definition 6.3dfom3 7229
[Eisenberg] p. 125Definition 8.21df-map 6657
[Eisenberg] p. 216Example 13.2(4)omenps 7236
[Eisenberg] p. 310Theorem 19.8cardprc 7494
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8056
[Enderton] p. 18Axiom of Empty Setaxnul 4042
[Enderton] p. 19Definitiondf-tp 3549
[Enderton] p. 26Exercise 5unissb 3752
[Enderton] p. 26Exercise 10pwel 4116
[Enderton] p. 28Exercise 7(b)pwun 4192
[Enderton] p. 30Theorem "Distributive laws"iinin1 3868  iinin2 3867  iinun2 3863  iunin1 3862  iunin2 3861
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3866  iundif2 3864
[Enderton] p. 32Exercise 20unineq 3323
[Enderton] p. 33Exercise 23iinuni 3880
[Enderton] p. 33Exercise 25iununi 3881
[Enderton] p. 33Exercise 24(a)iinpw 3885
[Enderton] p. 33Exercise 24(b)iunpw 4458  iunpwss 3886
[Enderton] p. 36Definitionopthwiener 4158
[Enderton] p. 38Exercise 6(a)unipw 4115
[Enderton] p. 38Exercise 6(b)pwuni 4097
[Enderton] p. 41Lemma 3Dopeluu 4414  rnex 4846  rnexg 4844
[Enderton] p. 41Exercise 8dmuni 4792  rnuni 4996
[Enderton] p. 42Definition of a functiondffun7 5135  dffun8 5136
[Enderton] p. 43Definition of function valuefunfv2 5436
[Enderton] p. 43Definition of single-rootedfuncnv 5164
[Enderton] p. 44Definition (d)dfima2 4918  dfima3 4919
[Enderton] p. 47Theorem 3Hfvco2 5443
[Enderton] p. 49Axiom of Choice (first form)ac7 7981  ac7g 7982  df-ac 7624  dfac2 7638  dfac2a 7637  dfac3 7629  dfac7 7639
[Enderton] p. 50Theorem 3K(a)imauni 5621
[Enderton] p. 52Definitiondf-map 6657
[Enderton] p. 53Exercise 21coass 5094
[Enderton] p. 53Exercise 27dmco 5084
[Enderton] p. 53Exercise 14(a)funin 5173
[Enderton] p. 53Exercise 22(a)imass2 4953
[Enderton] p. 54Remarkixpf 6721  ixpssmap 6733
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6701
[Enderton] p. 55Axiom of Choice (second form)ac9 7991  ac9s 8001
[Enderton] p. 56Theorem 3Merref 6563
[Enderton] p. 57Lemma 3Nerthi 6589
[Enderton] p. 57Definitiondf-ec 6545
[Enderton] p. 58Definitiondf-qs 6549
[Enderton] p. 60Theorem 3Qth3q 6650  th3qcor 6649  th3qlem1 6647  th3qlem2 6648
[Enderton] p. 61Exercise 35df-ec 6545
[Enderton] p. 65Exercise 56(a)dmun 4789
[Enderton] p. 68Definition of successordf-suc 4288
[Enderton] p. 71Definitiondf-tr 4008  dftr4 4012
[Enderton] p. 72Theorem 4Eunisuc 4358
[Enderton] p. 73Exercise 6unisuc 4358
[Enderton] p. 73Exercise 5(a)truni 4021
[Enderton] p. 73Exercise 5(b)trint 4022  trintALT 27222
[Enderton] p. 79Theorem 4I(A1)nna0 6485
[Enderton] p. 79Theorem 4I(A2)nnasuc 6487  onasuc 6410
[Enderton] p. 79Definition of operation valuedf-ov 5710
[Enderton] p. 80Theorem 4J(A1)nnm0 6486
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6488  onmsuc 6411
[Enderton] p. 81Theorem 4K(1)nnaass 6503
[Enderton] p. 81Theorem 4K(2)nna0r 6490  nnacom 6498
[Enderton] p. 81Theorem 4K(3)nndi 6504
[Enderton] p. 81Theorem 4K(4)nnmass 6505
[Enderton] p. 81Theorem 4K(5)nnmcom 6507
[Enderton] p. 82Exercise 16nnm0r 6491  nnmsucr 6506
[Enderton] p. 88Exercise 23nnaordex 6519
[Enderton] p. 129Definitiondf-en 6747
[Enderton] p. 132Theorem 6B(b)canth 6175
[Enderton] p. 133Exercise 1xpomen 7524
[Enderton] p. 133Exercise 2qnnen 12328
[Enderton] p. 134Theorem (Pigeonhole Principle)php 6927
[Enderton] p. 135Corollary 6Cphp3 6929
[Enderton] p. 136Corollary 6Enneneq 6926
[Enderton] p. 136Corollary 6D(a)pssinf 6955
[Enderton] p. 136Corollary 6D(b)ominf 6957
[Enderton] p. 137Lemma 6Fpssnn 6963
[Enderton] p. 138Corollary 6Gssfi 6965
[Enderton] p. 139Theorem 6H(c)mapen 6907
[Enderton] p. 142Theorem 6I(3)xpcdaen 7690
[Enderton] p. 142Theorem 6I(4)mapcdaen 7691
[Enderton] p. 143Theorem 6Jcda0en 7686  cda1en 7682
[Enderton] p. 144Exercise 13iunfi 7026  unifi 7027  unifi2 7028
[Enderton] p. 144Corollary 6Kundif2 3433  unfi 7006  unfi2 7008
[Enderton] p. 145Figure 38ffoss 5359
[Enderton] p. 145Definitiondf-dom 6748
[Enderton] p. 146Example 1domen 6758  domeng 6759
[Enderton] p. 146Example 3nndomo 6936  nnsdom 7235  nnsdomg 6998
[Enderton] p. 149Theorem 6L(a)cdadom2 7694
[Enderton] p. 149Theorem 6L(c)mapdom1 6908  xpdom1 6843  xpdom1g 6841  xpdom2g 6840
[Enderton] p. 149Theorem 6L(d)mapdom2 6914
[Enderton] p. 151Theorem 6Mzorn 8015  zorng 8012
[Enderton] p. 151Theorem 6M(4)ac8 8000  dfac5 7636
[Enderton] p. 159Theorem 6Qunictb 8074
[Enderton] p. 164Exampleinfdif 7716
[Enderton] p. 168Definitiondf-po 4204
[Enderton] p. 192Theorem 7M(a)oneli 4388
[Enderton] p. 192Theorem 7M(b)ontr1 4328
[Enderton] p. 192Theorem 7M(c)onirri 4387
[Enderton] p. 193Corollary 7N(b)0elon 4335
[Enderton] p. 193Corollary 7N(c)onsuci 4517
[Enderton] p. 193Corollary 7N(d)ssonunii 4467
[Enderton] p. 194Remarkonprc 4464
[Enderton] p. 194Exercise 16suc11 4384
[Enderton] p. 197Definitiondf-card 7453
[Enderton] p. 197Theorem 7Pcarden 8052
[Enderton] p. 200Exercise 25tfis 4533
[Enderton] p. 202Lemma 7Tr1tr 7329
[Enderton] p. 202Definitiondf-r1 7317
[Enderton] p. 202Theorem 7Qr1val1 7339
[Enderton] p. 204Theorem 7V(b)rankval4 7420
[Enderton] p. 206Theorem 7X(b)en2lp 7198
[Enderton] p. 207Exercise 30rankpr 7410  rankprb 7404  rankpw 7396  rankpwi 7376  rankuniss 7419
[Enderton] p. 207Exercise 34opthreg 7200
[Enderton] p. 208Exercise 35suc11reg 7201
[Enderton] p. 212Definition of alephalephval3 7618
[Enderton] p. 213Theorem 8A(a)alephord2 7584
[Enderton] p. 213Theorem 8A(b)cardalephex 7598
[Enderton] p. 218Theorem Schema 8Eonfununi 6241
[Enderton] p. 222Definition of kardkarden 7446  kardex 7445
[Enderton] p. 238Theorem 8Roeoa 6478
[Enderton] p. 238Theorem 8Soeoe 6480
[Enderton] p. 240Exercise 25oarec 6443
[Enderton] p. 257Definition of cofinalitycflm 7757
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18688
[Fremlin5] p. 213Lemma 565Cauniioovol 18728
[Fremlin5] p. 214Lemma 565Cauniioombl 18738
[FreydScedrov] p. 283Axiom of Infinityax-inf 7220  inf1 7204  inf2 7205
[Gleason] p. 117Proposition 9-2.1df-enq 8412  enqer 8422
[Gleason] p. 117Proposition 9-2.2df-1nq 8417  df-nq 8413
[Gleason] p. 117Proposition 9-2.3df-plpq 8409  df-plq 8415
[Gleason] p. 119Proposition 9-2.4caovmo 5906  df-mpq 8410  df-mq 8416
[Gleason] p. 119Proposition 9-2.5df-rq 8418
[Gleason] p. 119Proposition 9-2.6ltexnq 8476
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8477  ltbtwnnq 8479
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8472
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8473
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8480
[Gleason] p. 121Definition 9-3.1df-np 8482
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8494
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8496
[Gleason] p. 122Definitiondf-1p 8483
[Gleason] p. 122Remark (1)prub 8495
[Gleason] p. 122Lemma 9-3.4prlem934 8534
[Gleason] p. 122Proposition 9-3.2df-ltp 8486
[Gleason] p. 122Proposition 9-3.3ltsopr 8533  psslinpr 8532  supexpr 8555  suplem1pr 8553  suplem2pr 8554
[Gleason] p. 123Proposition 9-3.5addclpr 8519  addclprlem1 8517  addclprlem2 8518  df-plp 8484
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8523
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8522
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8535
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8544  ltexprlem1 8537  ltexprlem2 8538  ltexprlem3 8539  ltexprlem4 8540  ltexprlem5 8541  ltexprlem6 8542  ltexprlem7 8543
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8546  ltaprlem 8545
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8547
[Gleason] p. 124Lemma 9-3.6prlem936 8548
[Gleason] p. 124Proposition 9-3.7df-mp 8485  mulclpr 8521  mulclprlem 8520  reclem2pr 8549
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8530
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8525
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8524
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8529
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8552  reclem3pr 8550  reclem4pr 8551
[Gleason] p. 126Proposition 9-4.1df-enr 8558  df-mpr 8557  df-plpr 8556  enrer 8567
[Gleason] p. 126Proposition 9-4.2df-0r 8563  df-1r 8564  df-nr 8559
[Gleason] p. 126Proposition 9-4.3df-mr 8561  df-plr 8560  negexsr 8601  recexsr 8606  recexsrlem 8602
[Gleason] p. 127Proposition 9-4.4df-ltr 8562
[Gleason] p. 130Proposition 10-1.3creui 9589  creur 9588  cru 9586
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8687  axcnre 8663
[Gleason] p. 132Definition 10-3.1crim 11441  crimd 11558  crimi 11519  crre 11440  crred 11557  crrei 11518
[Gleason] p. 132Definition 10-3.2remim 11443  remimd 11524
[Gleason] p. 133Definition 10.36absval2 11610  absval2d 11766  absval2i 11719
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11467  cjaddd 11546  cjaddi 11514
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11468  cjmuld 11547  cjmuli 11515
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11466  cjcjd 11525  cjcji 11497
[Gleason] p. 133Proposition 10-3.4(f)cjre 11465  cjreb 11449  cjrebd 11528  cjrebi 11500  cjred 11552  rere 11448  rereb 11446  rerebd 11527  rerebi 11499  rered 11550
[Gleason] p. 133Proposition 10-3.4(h)addcj 11474  addcjd 11538  addcji 11509
[Gleason] p. 133Proposition 10-3.7(a)absval 11564
[Gleason] p. 133Proposition 10-3.7(b)abscj 11605  abscjd 11771  abscji 11723
[Gleason] p. 133Proposition 10-3.7(c)abs00 11615  abs00d 11767  abs00i 11720  absne0d 11768
[Gleason] p. 133Proposition 10-3.7(d)releabs 11644  releabsd 11772  releabsi 11724
[Gleason] p. 133Proposition 10-3.7(f)absmul 11618  absmuld 11775  absmuli 11726
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11608  sqabsaddi 11727
[Gleason] p. 133Proposition 10-3.7(h)abstri 11653  abstrid 11777  abstrii 11730
[Gleason] p. 134Definition 10-4.1df-exp 10948  exp0 10951  expp1 10953  expp1d 11088
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 19828  cxpaddd 19866  expadd 10987  expaddd 11089  expaddz 10989
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 19837  cxpmuld 19883  expmul 10990  expmuld 11090  expmulz 10991
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 19834  mulcxpd 19877  mulexp 10984  mulexpd 11102  mulexpz 10985
[Gleason] p. 140Exercise 1znnen 12327
[Gleason] p. 141Definition 11-2.1fzval 10627
[Gleason] p. 168Proposition 12-2.1(a)climadd 11944  rlimadd 11955  rlimdiv 11958
[Gleason] p. 168Proposition 12-2.1(b)climsub 11946  rlimsub 11956
[Gleason] p. 168Proposition 12-2.1(c)climmul 11945  rlimmul 11957
[Gleason] p. 171Corollary 12-2.2climmulc2 11949
[Gleason] p. 172Corollary 12-2.5climrecl 11896
[Gleason] p. 172Proposition 12-2.4(c)climabs 11916  climcj 11917  climim 11919  climre 11918  rlimabs 11921  rlimcj 11922  rlimim 11924  rlimre 11923
[Gleason] p. 173Definition 12-3.1df-ltxr 8749  df-xr 8748  ltxr 10303
[Gleason] p. 175Definition 12-4.1df-limsup 11784  limsupval 11787
[Gleason] p. 180Theorem 12-5.1climsup 11982
[Gleason] p. 180Theorem 12-5.3caucvg 11990  caucvgb 11991  caucvgr 11987  climcau 11983
[Gleason] p. 182Exercise 3cvgcmp 12113
[Gleason] p. 182Exercise 4cvgrat 12175
[Gleason] p. 195Theorem 13-2.12abs1m 11658
[Gleason] p. 217Lemma 13-4.1btwnzge0 10796
[Gleason] p. 223Definition 14-1.1df-met 16168
[Gleason] p. 223Definition 14-1.1(a)met0 17702  xmet0 17701
[Gleason] p. 223Definition 14-1.1(b)metgt0 17717
[Gleason] p. 223Definition 14-1.1(c)metsym 17708
[Gleason] p. 223Definition 14-1.1(d)mettri 17710  mstri 17809  xmettri 17709  xmstri 17808
[Gleason] p. 225Definition 14-1.5xpsmet 17740
[Gleason] p. 230Proposition 14-2.6txlm 17136
[Gleason] p. 240Theorem 14-4.3metcnp4 18529
[Gleason] p. 240Proposition 14-4.2metcnp3 17880
[Gleason] p. 243Proposition 14-4.16addcn 18163  addcn2 11906  mulcn 18165  mulcn2 11908  subcn 18164  subcn2 11907
[Gleason] p. 295Remarkbcval3 11161  bcval4 11162
[Gleason] p. 295Equation 2bcpasc 11175
[Gleason] p. 295Definition of binomial coefficientbcval 11159  df-bc 11158
[Gleason] p. 296Remarkbcn0 11165  bcnn 11166
[Gleason] p. 296Theorem 15-2.8binom 12127
[Gleason] p. 308Equation 2ef0 12208
[Gleason] p. 308Equation 3efcj 12209
[Gleason] p. 309Corollary 15-4.3efne0 12213
[Gleason] p. 309Corollary 15-4.4efexp 12217
[Gleason] p. 310Equation 14sinadd 12280
[Gleason] p. 310Equation 15cosadd 12281
[Gleason] p. 311Equation 17sincossq 12292
[Gleason] p. 311Equation 18cosbnd 12297  sinbnd 12296
[Gleason] p. 311Lemma 15-4.7sqeqor 11059  sqeqori 11057
[Gleason] p. 311Definition of pidf-pi 12190
[Godowski] p. 730Equation SFgoeqi 22614
[GodowskiGreechie] p. 249Equation IV3oai 22026
[Halmos] p. 31Theorem 17.3riesz1 22406  riesz2 22407
[Halmos] p. 41Definition of Hermitianhmopadj2 22282
[Halmos] p. 42Definition of projector orderingpjordi 22514
[Halmos] p. 43Theorem 26.1elpjhmop 22526  elpjidm 22525  pjnmopi 22489
[Halmos] p. 44Remarkpjinormi 22045  pjinormii 22034
[Halmos] p. 44Theorem 26.2elpjch 22530  pjrn 22065  pjrni 22060  pjvec 22054
[Halmos] p. 44Theorem 26.3pjnorm2 22085
[Halmos] p. 44Theorem 26.4hmopidmpj 22495  hmopidmpji 22493
[Halmos] p. 45Theorem 27.1pjinvari 22532
[Halmos] p. 45Theorem 27.3pjoci 22521  pjocvec 22055
[Halmos] p. 45Theorem 27.4pjorthcoi 22510
[Halmos] p. 48Theorem 29.2pjssposi 22513
[Halmos] p. 48Theorem 29.3pjssdif1i 22516  pjssdif2i 22515
[Halmos] p. 50Definition of spectrumdf-spec 22196
[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 18284  df-phtpy 18263
[Hatcher] p. 26Definitiondf-pco 18297  df-pi1 18300
[Hatcher] p. 26Proposition 1.2phtpcer 18287
[Hatcher] p. 26Proposition 1.3pi1grp 18342
[Herstein] p. 54Exercise 28df-grpo 20619
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14295  grpoideu 20637  mndideu 14172
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14313  grpoinveu 20650
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14332  grpo2inv 20667
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14341  grpoinvop 20669
[Herstein] p. 57Exercise 1isgrp2d 20663  isgrp2i 20664
[Hitchcock] p. 5Rule A3mpto1 1528
[Hitchcock] p. 5Rule A4mpto2 1529
[Hitchcock] p. 5Rule A5mtp-xor 1530
[Holland] p. 1519Theorem 2sumdmdi 22761
[Holland] p. 1520Lemma 5cdj1i 22774  cdj3i 22782  cdj3lem1 22775  cdjreui 22773
[Holland] p. 1524Lemma 7mddmdin0i 22772
[Holland95] p. 13Theorem 3.6hlathil 30718
[Holland95] p. 14Line 15hgmapvs 30648
[Holland95] p. 14Line 16hdmaplkr 30670
[Holland95] p. 14Line 17hdmapellkr 30671
[Holland95] p. 14Line 19hdmapglnm2 30668
[Holland95] p. 14Line 20hdmapip0com 30674
[Holland95] p. 14Theorem 3.6hdmapevec2 30593
[Holland95] p. 14Lines 24 and 25hdmapoc 30688
[Holland95] p. 204Definition of involutiondf-srng 15408
[Holland95] p. 212Definition of subspacedf-psubsp 28256
[Holland95] p. 214Lemma 3.3lclkrlem2v 30282
[Holland95] p. 214Definition 3.2df-lpolN 30235
[Holland95] p. 214Definition of nonsingularpnonsingN 28686
[Holland95] p. 215Lemma 3.3(1)dihoml4 30131  poml4N 28706
[Holland95] p. 215Lemma 3.3(2)dochexmid 30222  pexmidALTN 28731  pexmidN 28722
[Holland95] p. 218Theorem 3.6lclkr 30287
[Holland95] p. 218Definition of dual vector spacedf-ldual 27878  ldualset 27879
[Holland95] p. 222Item 1df-lines 28254  df-pointsN 28255
[Holland95] p. 222Item 2df-polarityN 28656
[Holland95] p. 223Remarkispsubcl2N 28700  omllaw4 28000  pol1N 28663  polcon3N 28670
[Holland95] p. 223Definitiondf-psubclN 28688
[Holland95] p. 223Equation for polaritypolval2N 28659
[Hughes] p. 44Equation 1.21bax-his3 21424
[Hughes] p. 47Definition of projection operatordfpjop 22523
[Hughes] p. 49Equation 1.30eighmre 22304  eigre 22176  eigrei 22175
[Hughes] p. 49Equation 1.31eighmorth 22305  eigorth 22179  eigorthi 22178
[Hughes] p. 137Remark (ii)eigposi 22177
[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 2248
[Jech] p. 42Lemma 6.1alephexp1 8078
[Jech] p. 42Equation 6.1alephadd 8076  alephmul 8077
[Jech] p. 43Lemma 6.2infmap 8075  infmap2 7725
[Jech] p. 71Lemma 9.3jech9.3 7367
[Jech] p. 72Equation 9.3scott0 7437  scottex 7436
[Jech] p. 72Exercise 9.1rankval4 7420
[Jech] p. 72Scheme "Collection Principle"cp 7442
[Jech] p. 78Definition implied by the footnoteopthprc 4640
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26097
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26193
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26194
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26109
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26113
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26114  rmyp1 26115
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26116  rmym1 26117
[JonesMatijasevic] p. 695Equation 2.11rmx0 26107  rmx1 26108  rmxluc 26118
[JonesMatijasevic] p. 695Equation 2.12rmy0 26111  rmy1 26112  rmyluc 26119
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26121
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26122
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26144  jm2.17b 26145  jm2.17c 26146
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26183
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26187
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26178
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26147  jm2.24nn 26143
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26192
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26198  rmygeid 26148
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26210
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1684
[Kalmbach] p. 14Definition of latticechabs1 21856  chabs1i 21858  chabs2 21857  chabs2i 21859  chjass 21873  chjassi 21826  latabs1 13999  latabs2 14000
[Kalmbach] p. 15Definition of atomdf-at 22679  ela 22680
[Kalmbach] p. 15Definition of coverscvbr2 22624  cvrval2 28028
[Kalmbach] p. 16Definitiondf-ol 27932  df-oml 27933
[Kalmbach] p. 20Definition of commutescmbr 21942  cmbri 21948  cmtvalN 27965  df-cm 21941  df-cmtN 27931
[Kalmbach] p. 22Remarkomllaw5N 28001  pjoml5 21971  pjoml5i 21946
[Kalmbach] p. 22Definitionpjoml2 21969  pjoml2i 21943
[Kalmbach] p. 22Theorem 2(v)cmcm 21972  cmcmi 21950  cmcmii 21955  cmtcomN 28003
[Kalmbach] p. 22Theorem 2(ii)omllaw3 27999  omlsi 21744  pjoml 21776  pjomli 21775
[Kalmbach] p. 22Definition of OML lawomllaw2N 27998
[Kalmbach] p. 23Remarkcmbr2i 21954  cmcm3 21973  cmcm3i 21952  cmcm3ii 21957  cmcm4i 21953  cmt3N 28005  cmt4N 28006  cmtbr2N 28007
[Kalmbach] p. 23Lemma 3cmbr3 21966  cmbr3i 21958  cmtbr3N 28008
[Kalmbach] p. 25Theorem 5fh1 21976  fh1i 21979  fh2 21977  fh2i 21980  omlfh1N 28012
[Kalmbach] p. 65Remarkchjatom 22698  chslej 21838  chsleji 21798  shslej 21720  shsleji 21710
[Kalmbach] p. 65Proposition 1chocin 21835  chocini 21794  chsupcl 21680  chsupval2 21750  h0elch 21595  helch 21584  hsupval2 21749  ocin 21636  ococss 21633  shococss 21634
[Kalmbach] p. 65Definition of subspace sumshsval 21652
[Kalmbach] p. 66Remarkdf-pjh 21735  pjssmi 22506  pjssmii 22039
[Kalmbach] p. 67Lemma 3osum 22003  osumi 22000
[Kalmbach] p. 67Lemma 4pjci 22541
[Kalmbach] p. 103Exercise 6atmd2 22741
[Kalmbach] p. 103Exercise 12mdsl0 22651
[Kalmbach] p. 140Remarkhatomic 22701  hatomici 22700  hatomistici 22703
[Kalmbach] p. 140Proposition 1atlatmstc 28073
[Kalmbach] p. 140Proposition 1(i)atexch 22722  lsatexch 27797
[Kalmbach] p. 140Proposition 1(ii)chcv1 22696  cvlcvr1 28093  cvr1 28163
[Kalmbach] p. 140Proposition 1(iii)cvexch 22715  cvexchi 22710  cvrexch 28173
[Kalmbach] p. 149Remark 2chrelati 22705  hlrelat 28155  hlrelat5N 28154  lrelat 27768
[Kalmbach] p. 153Exercise 5lsmcv 15691  lsmsatcv 27764  spansncv 22011  spansncvi 22010
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 27783  spansncv2 22634
[Kalmbach] p. 266Definitiondf-st 22552
[Kalmbach2] p. 8Definition of adjointdf-adjh 22190
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8145  fpwwe2 8142
[KanamoriPincus] p. 416Corollary 1.3canth4 8146
[KanamoriPincus] p. 417Corollary 1.6canthp1 8153
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8148
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8150
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8163
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8167  gchxpidm 8168
[KanamoriPincus] p. 419Theorem 2.1gchacg 8171  gchhar 8170
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7723  unxpwdom 7184
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8173
[Kreyszig] p. 3Property M1metcl 17691  xmetcl 17690
[Kreyszig] p. 4Property M2meteq0 17698
[Kreyszig] p. 8Definition 1.1-8dscmet 17889
[Kreyszig] p. 12Equation 5conjmul 9333  muleqadd 9270
[Kreyszig] p. 18Definition 1.3-2mopnval 17778
[Kreyszig] p. 19Remarkmopntopon 17779
[Kreyszig] p. 19Theorem T1mopn0 17838  mopnm 17784
[Kreyszig] p. 19Theorem T2unimopn 17836
[Kreyszig] p. 19Definition of neighborhoodneibl 17841
[Kreyszig] p. 20Definition 1.3-3metcnp2 17882
[Kreyszig] p. 25Definition 1.4-1lmbr 16782  lmmbr 18478  lmmbr2 18479
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 16902
[Kreyszig] p. 28Theorem 1.4-5lmcau 18532
[Kreyszig] p. 28Definition 1.4-3iscau 18496  iscmet2 18514
[Kreyszig] p. 30Theorem 1.4-7cmetss 18534
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 16981  metelcls 18524
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18525  metcld2 18526
[Kreyszig] p. 51Equation 2clmvneg1 18383  lmodvneg1 15464  nvinv 20958  vcm 20888
[Kreyszig] p. 51Equation 1aclm0vs 18382  lmod0vs 15460  vc0 20886
[Kreyszig] p. 51Equation 1blmodvs0 15461  vcz 20887
[Kreyszig] p. 58Definition 2.2-1imsmet 21021
[Kreyszig] p. 59Equation 1imsdval 21016  imsdval2 21017
[Kreyszig] p. 63Problem 1nvnd 21018
[Kreyszig] p. 64Problem 2nvge0 21001  nvz 20996
[Kreyszig] p. 64Problem 3nvabs 21000
[Kreyszig] p. 91Definition 2.7-1isblo3i 21140
[Kreyszig] p. 92Equation 2df-nmoo 21084
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21146  blocni 21144
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21145
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18433  ipeq0 16336  ipz 21056
[Kreyszig] p. 135Problem 2pythi 21189
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21193
[Kreyszig] p. 144Equation 4supcvg 12150
[Kreyszig] p. 144Theorem 3.3-1minvec 18594  minveco 21224
[Kreyszig] p. 196Definition 3.9-1df-aj 21089
[Kreyszig] p. 247Theorem 4.7-2bcth 18545
[Kreyszig] p. 249Theorem 4.7-3ubth 21213
[Kreyszig] p. 470Definition of positive operator orderingleop 22464  leopg 22463
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22482
[Kreyszig] p. 525Theorem 10.1-1htth 21259
[Kunen] p. 10Axiom 0a9e 1817  axnul 4042
[Kunen] p. 11Axiom 3axnul 4042
[Kunen] p. 12Axiom 6zfrep6 5597
[Kunen] p. 24Definition 10.24mapval 6667  mapvalg 6665
[Kunen] p. 30Lemma 10.20fodom 8030
[Kunen] p. 31Definition 10.24mapex 6661
[Kunen] p. 95Definition 2.1df-r1 7317
[Kunen] p. 97Lemma 2.10r1elss 7359  r1elssi 7358
[Kunen] p. 107Exercise 4rankop 7411  rankopb 7405  rankuni 7416  rankxplim 7430  rankxpsuc 7433
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3810
[Laboreo] p. 10Definition ITnatded 4
[Laboreo] p. 10Definition I` `m,nnatded 4
[Laboreo] p. 11Definition E=>m,nnatded 4
[Laboreo] p. 11Definition I=>m,nnatded 4
[Laboreo] p. 11Definition E` `(1)natded 4
[Laboreo] p. 11Definition E` `(2)natded 4
[Laboreo] p. 12Definition E` `m,n,pnatded 4
[Laboreo] p. 12Definition I` `n(1)natded 4
[Laboreo] p. 12Definition I` `n(2)natded 4
[Laboreo] p. 13Definition I` `m,n,pnatded 4
[Laboreo] p. 14Definition E` `nnatded 4
[Laboreo] p. 15Theorem 5.2ex-natded5.2-2 20584  ex-natded5.2 20583
[Laboreo] p. 16Theorem 5.3ex-natded5.3-2 20587  ex-natded5.3 20586
[Laboreo] p. 19Theorem 5.7ex-natded5.7-2 20590  ex-natded5.7 20589
[Laboreo] p. 20Theorem 5.8ex-natded5.8-2 20592  ex-natded5.8 20591
[Laboreo] p. 20Theorem 5.13ex-natded5.13-2 20594  ex-natded5.13 20593
[Laboreo] p. 32Definition I` `nnatded 4
[Laboreo] p. 32Definition E` `m,n,p,anatded 4
[Laboreo] p. 32Definition E` `n,tnatded 4
[Laboreo] p. 32Definition I` `n,tnatded 4
[Laboreo] p. 45Theorem 9.26ex-natded9.26-2 20596  ex-natded9.26 20595
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26648
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26643
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26649
[LeBlanc] p. 277Rule R2axnul 4042
[Levy] p. 338Axiomdf-clab 2240  df-clel 2249  df-cleq 2246
[Levy58] p. 2Definition Iisfin1-3 7893
[Levy58] p. 2Definition IIdf-fin2 7793
[Levy58] p. 2Definition Iadf-fin1a 7792
[Levy58] p. 2Definition IIIdf-fin3 7795
[Levy58] p. 3Definition Vdf-fin5 7796
[Levy58] p. 3Definition IVdf-fin4 7794
[Levy58] p. 4Definition VIdf-fin6 7797
[Levy58] p. 4Definition VIIdf-fin7 7798
[Levy58], p. 3Theorem 1fin1a2 7922
[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 22749
[Maeda] p. 168Lemma 5mdsym 22753  mdsymi 22752
[Maeda] p. 168Lemma 4(i)mdsymlem4 22747  mdsymlem6 22749  mdsymlem7 22750
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22751
[MaedaMaeda] p. 1Remarkssdmd1 22654  ssdmd2 22655  ssmd1 22652  ssmd2 22653
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22650
[MaedaMaeda] p. 1Definition 1.1df-dmd 22622  df-md 22621  mdbr 22635
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22672  mdslj1i 22660  mdslj2i 22661  mdslle1i 22658  mdslle2i 22659  mdslmd1i 22670  mdslmd2i 22671
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22662  mdsl2bi 22664  mdsl2i 22663
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22676
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22673
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22674
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22651
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22656  mdsl3 22657
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22675
[MaedaMaeda] p. 4Theorem 1.14mdcompli 22770
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28075  hlrelat1 28153
[MaedaMaeda] p. 31Lemma 7.5lcvexch 27793
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22677  cvmdi 22665  cvnbtwn4 22630  cvrnbtwn4 28033
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22678
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28094  cvp 22716  cvrp 28169  lcvp 27794
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22740
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22739
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28087  hlexch4N 28145
[MaedaMaeda] p. 34Exercise 7.1atabsi 22742
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28196
[MaedaMaeda] p. 61Definition 15.10psubN 28502  atpsubN 28506  df-pointsN 28255  pointpsubN 28504
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28257  pmap11 28515  pmaple 28514  pmapsub 28521  pmapval 28510
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 28518  pmap1N 28520
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 28523  pmapglb2N 28524  pmapglb2xN 28525  pmapglbx 28522
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 28605
[MaedaMaeda] p. 67Postulate PS1ps-1 28230
[MaedaMaeda] p. 68Lemma 16.2df-padd 28549  paddclN 28595  paddidm 28594
[MaedaMaeda] p. 68Condition PS2ps-2 28231
[MaedaMaeda] p. 68Equation 16.2.1paddass 28591
[MaedaMaeda] p. 69Lemma 16.4ps-1 28230
[MaedaMaeda] p. 69Theorem 16.4ps-2 28231
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14781  lsmmod2 14782  lssats 27766  shatomici 22699  shatomistici 22702  shmodi 21730  shmodsi 21729
[MaedaMaeda] p. 130Remark 29.6dmdmd 22641  mdsymlem7 22750
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 21947
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 21833
[MaedaMaeda] p. 139Remarksumdmdii 22756
[Margaris] p. 40Rule Cexlimiv 2023
[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 27256
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27257
[Margaris] p. 79Rule Cexinst01 27009  exinst11 27010
[Margaris] p. 89Theorem 19.219.2 1759  r19.2z 3446
[Margaris] p. 89Theorem 19.319.3 1760  rr19.3v 2844
[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 2010
[Margaris] p. 89Theorem 19.11excom 1765  excomim 1764
[Margaris] p. 89Theorem 19.1219.12 1766  r19.12 2616
[Margaris] p. 90Theorem 19.14exnal 1572
[Margaris] p. 90Theorem 19.152albi 26673  albi 1552  ralbi 2639
[Margaris] p. 90Theorem 19.1619.16 1767
[Margaris] p. 90Theorem 19.1719.17 1768
[Margaris] p. 90Theorem 19.182exbi 26675  exbi 1579
[Margaris] p. 90Theorem 19.1919.19 1769
[Margaris] p. 90Theorem 19.202alim 26672  alim 1548  alimd 1705  alimdh 1551  alimdv 2017  ralimdaa 2580  ralimdv 2582  ralimdva 2581  sbcimdv 2979
[Margaris] p. 90Theorem 19.2119.21-2 1772  19.21 1771  19.21bi 1774  19.21t 1770  19.21v 2011  19.21vv 26671  alrimd 1710  alrimdd 1709  alrimdh 1585  alrimdv 2014  alrimi 1706  alrimih 1553  alrimiv 2012  alrimivv 2013  r19.21 2589  r19.21be 2604  r19.21bi 2601  r19.21t 2588  r19.21v 2590  ralrimd 2591  ralrimdv 2592  ralrimdva 2593  ralrimdvv 2597  ralrimdvva 2598  ralrimi 2584  ralrimiv 2585  ralrimiva 2586  ralrimivv 2594  ralrimivva 2595  ralrimivvva 2596  ralrimivw 2587  rexlimi 2620
[Margaris] p. 90Theorem 19.222alimdv 2019  2exim 26674  2eximdv 2020  exim 1573  eximd 1711  eximdh 1586  eximdv 2018  rexim 2607  reximdai 2611  reximdv 2614  reximdv2 2612  reximdva 2615  reximdvai 2613  reximi2 2609
[Margaris] p. 90Theorem 19.2319.23 1777  19.23bi 1783  19.23t 1776  19.23v 2021  19.23vv 2022  exlimd 1784  exlimdh 1785  exlimdv 1932  exlimdvv 2026  exlimexi 26903  exlimi 1781  exlimih 1782  exlimiv 2023  exlimivv 2025  r19.23 2618  r19.23v 2619  rexlimd 2624  rexlimdv 2626  rexlimdv3a 2629  rexlimdva 2627  rexlimdvaa 2628  rexlimdvv 2633  rexlimdvva 2634  rexlimdvw 2630  rexlimiv 2621  rexlimiva 2622  rexlimivv 2632
[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 2636  r19.26-2a 24030  r19.26-3 2637  r19.26 2635  r19.26m 2638
[Margaris] p. 90Theorem 19.2719.27 1786  19.27v 2027  r19.27av 2641  r19.27z 3455  r19.27zv 3456
[Margaris] p. 90Theorem 19.2819.28 1787  19.28v 2028  19.28vv 26681  r19.28av 2642  r19.28z 3449  r19.28zv 3452  rr19.28v 2845
[Margaris] p. 90Theorem 19.2919.29 1595  19.29r 1596  19.29r2 1597  19.29x 1598  r19.29 2643  r19.29r 2644
[Margaris] p. 90Theorem 19.3019.30 1603  r19.30 2645
[Margaris] p. 90Theorem 19.3119.31 1795  19.31vv 26679
[Margaris] p. 90Theorem 19.3219.32 1794  r19.32v 2646
[Margaris] p. 90Theorem 19.3319.33-2 26677  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 2647
[Margaris] p. 90Theorem 19.3619.36 1788  19.36aiv 2030  19.36i 1789  19.36v 2029  19.36vv 26678  r19.36av 2648  r19.36zv 3457
[Margaris] p. 90Theorem 19.3719.37 1790  19.37aiv 2033  19.37v 2032  19.37vv 26680  r19.37 2649  r19.37av 2650  r19.37zv 3453
[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 2651
[Margaris] p. 90Theorem 19.4119.41 1799  19.41rg 26932  19.41v 2034  19.41vv 2035  19.41vvv 2036  19.41vvvv 2037  r19.41 2652  r19.41v 2653
[Margaris] p. 90Theorem 19.4219.42 1800  19.42v 2038  19.42vv 2040  19.42vvv 2041  r19.42v 2654
[Margaris] p. 90Theorem 19.4319.43 1604  r19.43 2655
[Margaris] p. 90Theorem 19.4419.44 1796  r19.44av 2656
[Margaris] p. 90Theorem 19.4519.45 1797  r19.45av 2657  r19.45zv 3454
[Margaris] p. 110Exercise 2(b)eu1 2134
[Mayet] p. 370Remarkjpi 22611  largei 22608  stri 22598
[Mayet3] p. 9Definition of CH-statesdf-hst 22553  ishst 22555
[Mayet3] p. 10Theoremhstrbi 22607  hstri 22606
[Mayet3] p. 1223Theorem 4.1mayete3i 22086
[Mayet3] p. 1240Theorem 7.1mayetes3i 22088
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22619
[MegPav2000] p. 2345Definition 3.4-1chintcl 21672  chsupcl 21680
[MegPav2000] p. 2345Definition 3.4-2hatomic 22701
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22695
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22722
[MegPav2000] p. 2366Figure 7pl42N 28736
[MegPav2002] p. 362Lemma 2.2latj31 14011  latj32 14009  latjass 14007
[Megill] p. 444Axiom C5ax-17 1628
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 1837  alequcom 1680  ax-10 1678
[Megill] p. 446Lemma L17equtrr 1827
[Megill] p. 446Lemma L18ax9from9o 1816
[Megill] p. 446Lemma L19hbnae-o 1845  hbnae 1844
[Megill] p. 447Remark 9.1df-sb 1883  sbid 1895
[Megill] p. 448Remark 9.6ax15 2101
[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 1835
[Megill] p. 448Scheme C12'ax-13 1625
[Megill] p. 448Scheme C13'ax-14 1626
[Megill] p. 448Scheme C14'ax-15 2102
[Megill] p. 448Scheme C15'ax-11o 1940
[Megill] p. 448Scheme C16'ax-16 1926
[Megill] p. 448Theorem 9.4dral1-o 1856  dral1 1855  dral2-o 1858  dral2 1857  drex1 1859  drex2 1860  drsb1 1886  drsb2 1953
[Megill] p. 448Theorem 9.7conventions 3
[Megill] p. 449Theorem 9.7sbcom2 2074  sbequ 1952  sbid2v 2083
[Megill] p. 450Example in Appendixhba1 1718
[Mendelson] p. 35Axiom A3hirstL-ax3 26782
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4ra4sbc 2996  ra4sbca 2997  stdpc4 1896
[Mendelson] p. 69Axiom 5ax-5o 1694  ra5 3002  stdpc5 1773
[Mendelson] p. 81Rule Cexlimiv 2023
[Mendelson] p. 95Axiom 6stdpc6 1821
[Mendelson] p. 95Axiom 7stdpc7 1891
[Mendelson] p. 225Axiom system NBGru 2918
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4158
[Mendelson] p. 231Exercise 4.10(k)inv1 3385
[Mendelson] p. 231Exercise 4.10(l)unv 3386
[Mendelson] p. 231Exercise 4.10(n)dfin3 3312
[Mendelson] p. 231Exercise 4.10(o)df-nul 3360
[Mendelson] p. 231Exercise 4.10(q)dfin4 3313
[Mendelson] p. 231Exercise 4.10(s)ddif 3219
[Mendelson] p. 231Definition of uniondfun3 3311
[Mendelson] p. 235Exercise 4.12(c)univ 4453
[Mendelson] p. 235Exercise 4.12(d)pwv 3723
[Mendelson] p. 235Exercise 4.12(j)pwin 4187
[Mendelson] p. 235Exercise 4.12(k)pwunss 4188
[Mendelson] p. 235Exercise 4.12(l)pwssun 4189
[Mendelson] p. 235Exercise 4.12(n)uniin 3744
[Mendelson] p. 235Exercise 4.12(p)reli 4717
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5096
[Mendelson] p. 244Proposition 4.8(g)epweon 4463
[Mendelson] p. 246Definition of successordf-suc 4288
[Mendelson] p. 250Exercise 4.36oelim2 6476
[Mendelson] p. 254Proposition 4.22(b)xpen 6906
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6828  xpsneng 6829
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6835  xpcomeng 6836
[Mendelson] p. 254Proposition 4.22(e)xpassen 6838
[Mendelson] p. 255Definitionbrsdom 6767
[Mendelson] p. 255Exercise 4.39endisj 6831
[Mendelson] p. 255Exercise 4.41mapprc 6659
[Mendelson] p. 255Exercise 4.43mapsnen 6820
[Mendelson] p. 255Exercise 4.45mapunen 6912
[Mendelson] p. 255Exercise 4.47xpmapen 6911
[Mendelson] p. 255Exercise 4.42(a)map0e 6688
[Mendelson] p. 255Exercise 4.42(b)map1 6821
[Mendelson] p. 257Proposition 4.24(a)undom 6832
[Mendelson] p. 258Exercise 4.56(b)cdaen 7680
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7689  cdacomen 7688
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7693
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7687
[Mendelson] p. 258Definition of cardinal sumcdaval 7677  df-cda 7675
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6413
[Mendelson] p. 266Proposition 4.34(f)oaordex 6439
[Mendelson] p. 275Proposition 4.42(d)entri3 8060
[Mendelson] p. 281Definitiondf-r1 7317
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7366
[Mendelson] p. 287Axiom system MKru 2918
[Mittelstaedt] p. 9Definitiondf-oc 21592
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3295
[Monk1] p. 33Theorem 3.2(i)ssrel 4680
[Monk1] p. 33Theorem 3.2(ii)eqrel 4681
[Monk1] p. 34Definition 3.3df-opab 3972
[Monk1] p. 36Theorem 3.7(i)coi1 5091  coi2 5092
[Monk1] p. 36Theorem 3.8(v)dm0 4796  rn0 4840
[Monk1] p. 36Theorem 3.7(ii)cnvi 4989
[Monk1] p. 37Theorem 3.13(i)relxp 4698
[Monk1] p. 37Theorem 3.13(x)dmxp 4801  rnxp 5010
[Monk1] p. 37Theorem 3.13(ii)xp0 5002  xp0r 4672
[Monk1] p. 38Theorem 3.16(ii)ima0 4934
[Monk1] p. 38Theorem 3.16(viii)imai 4931
[Monk1] p. 39Theorem 3.17imaexg 4930
[Monk1] p. 39Theorem 3.16(xi)imassrn 4929
[Monk1] p. 41Theorem 4.3(i)fnopfv 5509  funfvop 5486
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5415
[Monk1] p. 42Theorem 4.4(iii)fvelima 5423
[Monk1] p. 43Theorem 4.6funun 5150
[Monk1] p. 43Theorem 4.8(iv)dff13 5632  dff13f 5633
[Monk1] p. 46Theorem 4.15(v)funex 5592  funrnex 5596
[Monk1] p. 50Definition 5.4fniunfv 5622
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5059
[Monk1] p. 52Theorem 5.11(viii)ssint 3773
[Monk1] p. 52Definition 5.13 (i)1stval2 5986  df-1st 5971
[Monk1] p. 52Definition 5.13 (ii)2ndval2 5987  df-2nd 5972
[Monk1] p. 112Theorem 15.17(v)ranksn 7407  ranksnb 7380
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7408
[Monk1] p. 112Theorem 15.17(iii)rankun 7409  rankunb 7403
[Monk1] p. 113Theorem 15.18r1val3 7391
[Monk1] p. 113Definition 15.19df-r1 7317  r1val2 7390
[Monk1] p. 117Lemmazorn2 8014  zorn2g 8011
[Monk1] p. 133Theorem 18.11cardom 7500
[Monk1] p. 133Theorem 18.12canth3 8062
[Monk1] p. 133Theorem 18.14carduni 7495
[Monk2] p. 105Axiom C4ax-5 1533
[Monk2] p. 105Axiom C7ax-8 1623
[Monk2] p. 105Axiom C8ax-11 1624  ax-11o 1940
[Monk2] p. 105Axiom (C8)ax11v 1990
[Monk2] p. 108Lemma 5ax-5o 1694
[Monk2] p. 109Lemma 12ax-7 1535
[Monk2] p. 109Lemma 15equvin 1999  equvini 1879  eqvinop 4141
[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 2557
[Munkres] p. 77Example 2distop 16527  indistop 16533  indistopon 16532
[Munkres] p. 77Example 3fctop 16535  fctop2 16536
[Munkres] p. 77Example 4cctop 16537
[Munkres] p. 78Definition of basisdf-bases 16432  isbasis3g 16481
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13180  tgval2 16488
[Munkres] p. 79Remarktgcl 16501
[Munkres] p. 80Lemma 2.1tgval3 16495
[Munkres] p. 80Lemma 2.2tgss2 16519  tgss3 16518
[Munkres] p. 81Lemma 2.3basgen 16520  basgen2 16521
[Munkres] p. 89Definition of subspace topologyresttop 16685
[Munkres] p. 93Theorem 6.1(1)0cld 16569  topcld 16566
[Munkres] p. 93Theorem 6.1(2)iincld 16570
[Munkres] p. 93Theorem 6.1(3)uncld 16572
[Munkres] p. 94Definition of closureclsval 16568
[Munkres] p. 94Definition of interiorntrval 16567
[Munkres] p. 95Theorem 6.5(a)clsndisj 16606  elcls 16604
[Munkres] p. 95Theorem 6.5(b)elcls3 16614
[Munkres] p. 97Theorem 6.6clslp 16673  neindisj 16648
[Munkres] p. 97Corollary 6.7cldlp 16675
[Munkres] p. 97Definition of limit pointislp2 16671  lpval 16665
[Munkres] p. 98Definition of Hausdorff spacedf-haus 16837
[Munkres] p. 102Definition of continuous functiondf-cn 16751  iscn 16759  iscn2 16762
[Munkres] p. 107Theorem 7.2(g)cncnp 16803  cncnp2 16804  cncnpi 16801  df-cnp 16752  iscnp 16761  iscnp2 16763
[Munkres] p. 127Theorem 10.1metcn 17883
[Munkres] p. 128Theorem 10.3metcn4 18530
[NielsenChuang] p. 195Equation 4.73unierri 22445
[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 18431  df-dip 21035  dip0l 21055  ip0l 16334
[Ponnusamy] p. 361Equation 6.45ipval 21037
[Ponnusamy] p. 362Equation I1dipcj 21051
[Ponnusamy] p. 362Equation I3cphdir 18434  dipdir 21181  ipdir 16337  ipdiri 21169
[Ponnusamy] p. 362Equation I4ipidsq 21047
[Ponnusamy] p. 362Equation 6.46ip0i 21164
[Ponnusamy] p. 362Equation 6.47ip1i 21166
[Ponnusamy] p. 362Equation 6.48ip2i 21167
[Ponnusamy] p. 363Equation I2cphass 18440  dipass 21184  ipass 16343  ipassi 21180
[Prugovecki] p. 186Definition of brabraval 22285  df-bra 22191
[Prugovecki] p. 376Equation 8.1df-kb 22192  kbval 22295
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22723
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 28641
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22737  atcvat4i 22738  cvrat3 28195  cvrat4 28196  lsatcvat3 27806
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22623  cvrval 28023  df-cv 22620  df-lcv 27773  lspsncv0 15695
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 28653
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 28654
[Quine] p. 16Definition 2.1df-clab 2240  rabid 2673
[Quine] p. 17Definition 2.1''dfsb7 2079
[Quine] p. 18Definition 2.7df-cleq 2246
[Quine] p. 19Definition 2.9conventions 3  df-v 2727
[Quine] p. 34Theorem 5.1abeq2 2354
[Quine] p. 35Theorem 5.2abid2 2366  abid2f 2410
[Quine] p. 40Theorem 6.1sb5 1993
[Quine] p. 40Theorem 6.2sb56 1991  sb6 1992
[Quine] p. 41Theorem 6.3df-clel 2249
[Quine] p. 41Theorem 6.4eqid 2253  eqid1 20601
[Quine] p. 41Theorem 6.5eqcom 2255
[Quine] p. 42Theorem 6.6df-sbc 2920
[Quine] p. 42Theorem 6.7dfsbcq 2921  dfsbcq2 2922
[Quine] p. 43Theorem 6.8vex 2728
[Quine] p. 43Theorem 6.9isset 2729
[Quine] p. 44Theorem 7.3cla4gf 2799  cla4gv 2803  cla4imgf 2797
[Quine] p. 44Theorem 6.11a4sbc 2931  a4sbcd 2932
[Quine] p. 44Theorem 6.12elex 2733
[Quine] p. 44Theorem 6.13elab 2849  elabg 2850  elabgf 2847
[Quine] p. 44Theorem 6.14noel 3363
[Quine] p. 48Theorem 7.2snprc 3596
[Quine] p. 48Definition 7.1df-pr 3548  df-sn 3547
[Quine] p. 49Theorem 7.4snss 3649  snssg 3653
[Quine] p. 49Theorem 7.5prss 3666  prssg 3667
[Quine] p. 49Theorem 7.6prid1 3635  prid1g 3633  prid2 3636  prid2g 3634  snid 3568  snidg 3566
[Quine] p. 51Theorem 7.13prex 4108  snex 4107  snexALT 4087
[Quine] p. 53Theorem 8.2unisn 3740  unisnALT 27267  unisng 3741
[Quine] p. 53Theorem 8.3uniun 3743
[Quine] p. 54Theorem 8.6elssuni 3750
[Quine] p. 54Theorem 8.7uni0 3749
[Quine] p. 56Theorem 8.17uniabio 6150
[Quine] p. 56Definition 8.18dfiota2 6141
[Quine] p. 57Theorem 8.19iotaval 6151
[Quine] p. 57Theorem 8.22iotanul 6155
[Quine] p. 58Theorem 8.23iotaex 6157
[Quine] p. 58Definition 9.1df-op 3550
[Quine] p. 61Theorem 9.5opabid 4161  opelopab 4176  opelopaba 4171  opelopabaf 4178  opelopabf 4179  opelopabg 4173  opelopabga 4168  oprabid 5731
[Quine] p. 64Definition 9.11df-xp 4591
[Quine] p. 64Definition 9.12df-cnv 4593
[Quine] p. 64Definition 9.15df-id 4199
[Quine] p. 65Theorem 10.3fun0 5161
[Quine] p. 65Theorem 10.4funi 5139
[Quine] p. 65Theorem 10.5funsn 5154  funsng 5152
[Quine] p. 65Definition 10.1df-fun 4599
[Quine] p. 65Definition 10.2args 4945  df-fv 4605
[Quine] p. 68Definition 10.11conventions 3  df-fv 4605  fv2 5370
[Quine] p. 124Theorem 17.3nn0opth2 11129  nn0opth2i 11128  nn0opthi 11127  omopthi 6538
[Quine] p. 177Definition 25.2df-rdg 6306
[Quine] p. 232Equation icarddom 8055
[Quine] p. 284Axiom 39(vi)funimaex 5184  funimaexg 5183
[Quine] p. 331Axiom system NFru 2918
[ReedSimon] p. 36Definition (iii)ax-his3 21424
[ReedSimon] p. 63Exercise 4(a)df-dip 21035  polid 21499  polid2i 21497  polidi 21498
[ReedSimon] p. 63Exercise 4(b)df-ph 21152
[ReedSimon] p. 195Remarklnophm 22360  lnophmi 22359
[Retherford] p. 49Exercise 1(i)leopadd 22473
[Retherford] p. 49Exercise 1(ii)leopmul 22475  leopmuli 22474
[Retherford] p. 49Exercise 1(iv)leoptr 22478
[Retherford] p. 49Definition VI.1df-leop 22193  leoppos 22467
[Retherford] p. 49Exercise 1(iii)leoptri 22477
[Retherford] p. 49Definition of operator orderingleop3 22466
[Rudin] p. 164Equation 27efcan 12212
[Rudin] p. 164Equation 30efzval 12218
[Rudin] p. 167Equation 48absefi 12312
[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 4962
[Schechter] p. 51Definition of irreflexivityintirr 4965
[Schechter] p. 51Definition of symmetrycnvsym 4961
[Schechter] p. 51Definition of transitivitycotr 4959
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13323
[Schechter] p. 79Definition of Moore closuredf-mrc 13324
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13325
[Schechter] p. 139Definition AC3dfac9 7643
[Schechter] p. 141Definition (MC)dfac11 26257
[Schechter] p. 149Axiom DC1ax-dc 7953  axdc3 7961
[Schechter] p. 187Definition of ring with unitisrng 15142  isrngo 20806
[Schechter] p. 276Remark 11.6.espan0 21882
[Schechter] p. 276Definition of spandf-span 21649  spanval 21673
[Schechter] p. 428Definition 15.35bastop1 16525
[Schwabhauser] p. 10Axiom A1axcgrrflx 23647
[Schwabhauser] p. 10Axiom A2axcgrtr 23648
[Schwabhauser] p. 10Axiom A3axcgrid 23649
[Schwabhauser] p. 11Axiom A4axsegcon 23660
[Schwabhauser] p. 11Axiom A5ax5seg 23671
[Schwabhauser] p. 11Axiom A6axbtwnid 23672
[Schwabhauser] p. 12Axiom A7axpasch 23674
[Schwabhauser] p. 12Axiom A8axlowdim2 23693
[Schwabhauser] p. 13Axiom A10axeuclid 23696
[Schwabhauser] p. 13Axiom A11axcont 23709
[Schwabhauser] p. 27Theorem 2.1cgrrflx 23715
[Schwabhauser] p. 27Theorem 2.2cgrcomim 23717
[Schwabhauser] p. 27Theorem 2.3cgrtr 23720
[Schwabhauser] p. 27Theorem 2.4cgrcoml 23724
[Schwabhauser] p. 27Theorem 2.5cgrcomr 23725
[Schwabhauser] p. 28Theorem 2.8cgrtriv 23730
[Schwabhauser] p. 28Theorem 2.105segofs 23734
[Schwabhauser] p. 28Definition 2.10df-ofs 23711
[Schwabhauser] p. 29Theorem 2.11cgrextend 23736
[Schwabhauser] p. 29Theorem 2.12segconeq 23738
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 23750  btwntriv2 23740
[Schwabhauser] p. 30Theorem 3.2btwncomim 23741
[Schwabhauser] p. 30Theorem 3.3btwntriv1 23744
[Schwabhauser] p. 30Theorem 3.4btwnswapid 23745
[Schwabhauser] p. 30Theorem 3.5btwnexch2 23751  btwnintr 23747
[Schwabhauser] p. 30Theorem 3.6btwnexch 23753  btwnexch3 23748
[Schwabhauser] p. 30Theorem 3.7btwnouttr 23752
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23692
[Schwabhauser] p. 32Theorem 3.14btwndiff 23755
[Schwabhauser] p. 33Theorem 3.17trisegint 23756
[Schwabhauser] p. 34Theorem 4.2ifscgr 23772
[Schwabhauser] p. 34Definition 4.1df-ifs 23767
[Schwabhauser] p. 35Theorem 4.3cgrsub 23773
[Schwabhauser] p. 35Theorem 4.5cgrxfr 23783
[Schwabhauser] p. 35Definition 4.4df-cgr3 23768
[Schwabhauser] p. 36Theorem 4.6btwnxfr 23784
[Schwabhauser] p. 36Theorem 4.11colinearperm1 23790  colinearperm2 23792  colinearperm3 23791  colinearperm4 23793  colinearperm5 23794
[Schwabhauser] p. 36Definition 4.10df-colinear 23769
[Schwabhauser] p. 37Theorem 4.12colineartriv1 23795
[Schwabhauser] p. 37Theorem 4.13colinearxfr 23803
[Schwabhauser] p. 37Theorem 4.14lineext 23804
[Schwabhauser] p. 37Theorem 4.16fscgr 23808
[Schwabhauser] p. 37Theorem 4.17linecgr 23809
[Schwabhauser] p. 37Definition 4.15df-fs 23770
[Schwabhauser] p. 38Theorem 4.18lineid 23811
[Schwabhauser] p. 38Theorem 4.19idinside 23812
[Schwabhauser] p. 39Theorem 5.1btwnconn1 23829
[Schwabhauser] p. 41Theorem 5.2btwnconn2 23830
[Schwabhauser] p. 41Theorem 5.3btwnconn3 23831
[Schwabhauser] p. 41Theorem 5.5brsegle2 23837
[Schwabhauser] p. 41Definition 5.4df-segle 23835
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 23838
[Schwabhauser] p. 42Theorem 5.7seglerflx 23840
[Schwabhauser] p. 42Theorem 5.8segletr 23842
[Schwabhauser] p. 42Theorem 5.9segleantisym 23843
[Schwabhauser] p. 42Theorem 5.10seglelin 23844
[Schwabhauser] p. 42Theorem 5.11seglemin 23841
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 23846
[Schwabhauser] p. 43Theorem 6.2btwnoutside 23853
[Schwabhauser] p. 43Theorem 6.3broutsideof3 23854
[Schwabhauser] p. 43Theorem 6.4broutsideof 23849  df-outsideof 23848
[Schwabhauser] p. 43Definition 6.1broutsideof2 23850
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 23855
[Schwabhauser] p. 44Theorem 6.6outsideofcom 23856
[Schwabhauser] p. 44Theorem 6.7outsideoftr 23857
[Schwabhauser] p. 44Theorem 6.11outsideofeu 23859
[Schwabhauser] p. 44Definition 6.8df-ray 23866
[Schwabhauser] p. 45Part 2df-lines2 23867
[Schwabhauser] p. 45Theorem 6.13outsidele 23860
[Schwabhauser] p. 45Theorem 6.15lineunray 23875
[Schwabhauser] p. 45Theorem 6.16lineelsb2 23876
[Schwabhauser] p. 45Theorem 6.17linecom 23878  linerflx1 23877  linerflx2 23879
[Schwabhauser] p. 45Theorem 6.18linethru 23881
[Schwabhauser] p. 45Definition 6.14df-line2 23865
[Schwabhauser] p. 46Theorem 6.19linethrueu 23884
[Schwabhauser] p. 46Theorem 6.21lineintmo 23885
[Shapiro] p. 230Theorem 6.5.1dchrhash 20276  dchrsum 20274  dchrsum2 20273  sumdchr 20277
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20278  sum2dchr 20279
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15098  ablfacrp2 15099
[Shapiro], p. 328Equation 9.2.4vmasum 20221
[Shapiro], p. 329Equation 9.2.7logfac2 20222
[Shapiro], p. 329Equation 9.2.9logfacrlim 20229
[Shapiro], p. 331Equation 9.2.13vmadivsum 20397
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20400
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20454  vmalogdivsum2 20453
[Shapiro], p. 375Theorem 9.4.1dirith 20444  dirith2 20443
[Shapiro], p. 375Equation 9.4.3rplogsum 20442  rpvmasum 20441  rpvmasum2 20427
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20402
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20440
[Shapiro], p. 377Lemma 9.4.1dchrisum 20407  dchrisumlem1 20404  dchrisumlem2 20405  dchrisumlem3 20406  dchrisumlema 20403
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20410
[Shapiro], p. 379Equation 9.4.16dchrmusum 20439  dchrmusumlem 20437  dchrvmasumlem 20438
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20409
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20411
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20435  dchrisum0re 20428  dchrisumn0 20436
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20421
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20425
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20426
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20481  pntrsumbnd2 20482  pntrsumo1 20480
[Shapiro], p. 405Equation 10.2.1mudivsum 20445
[Shapiro], p. 406Equation 10.2.6mulogsum 20447
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20449
[Shapiro], p. 407Equation 10.2.8mulog2sum 20452
[Shapiro], p. 418Equation 10.4.6logsqvma 20457
[Shapiro], p. 418Equation 10.4.8logsqvma2 20458
[Shapiro], p. 419Equation 10.4.10selberg 20463
[Shapiro], p. 420Equation 10.4.12selberg2lem 20465
[Shapiro], p. 420Equation 10.4.14selberg2 20466
[Shapiro], p. 422Equation 10.6.7selberg3 20474
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20475
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20472  selberg3lem2 20473
[Shapiro], p. 422Equation 10.4.23selberg4 20476
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20470
[Shapiro], p. 428Equation 10.6.2selbergr 20483
[Shapiro], p. 429Equation 10.6.8selberg3r 20484
[Shapiro], p. 430Equation 10.6.11selberg4r 20485
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20499
[Shapiro], p. 434Equation 10.6.27pntlema 20511  pntlemb 20512  pntlemc 20510  pntlemd 20509  pntlemg 20513
[Shapiro], p. 435Equation 10.6.29pntlema 20511
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20503
[Shapiro], p. 436Lemma 10.6.2pntibnd 20508
[Shapiro], p. 436Equation 10.6.34pntlema 20511
[Shapiro], p. 436Equation 10.6.35pntlem3 20524  pntleml 20526
[Stoll] p. 13Definition of symmetric differencesymdif1 3337
[Stoll] p. 16Exercise 4.40dif 3428  dif0 3427
[Stoll] p. 16Exercise 4.8difdifdir 3444
[Stoll] p. 17Theorem 5.1(5)undifv 3431
[Stoll] p. 19Theorem 5.2(13)undm 3330
[Stoll] p. 19Theorem 5.2(13')indm 3331
[Stoll] p. 20Remarkinvdif 3314
[Stoll] p. 25Definition of ordered tripledf-ot 3551
[Stoll] p. 43Definitionuniiun 3850
[Stoll] p. 44Definitionintiin 3851
[Stoll] p. 45Definitiondf-iin 3803
[Stoll] p. 45Definition indexed uniondf-iun 3802
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3337
[Strang] p. 242Section 6.3expgrowth 26649
[Suppes] p. 22Theorem 2eq0 3373
[Suppes] p. 22Theorem 4eqss 3112  eqssd 3114  eqssi 3113
[Suppes] p. 23Theorem 5ss0 3389  ss0b 3388
[Suppes] p. 23Theorem 6sstr 3105  sstrALT2 27176
[Suppes] p. 23Theorem 7pssirr 3193
[Suppes] p. 23Theorem 8pssn2lp 3194
[Suppes] p. 23Theorem 9psstr 3197
[Suppes] p. 23Theorem 10pssss 3189
[Suppes] p. 25Theorem 12elin 3263  elun 3223
[Suppes] p. 26Theorem 15inidm 3282
[Suppes] p. 26Theorem 16in0 3384
[Suppes] p. 27Theorem 23unidm 3225
[Suppes] p. 27Theorem 24un0 3383
[Suppes] p. 27Theorem 25ssun1 3245
[Suppes] p. 27Theorem 26ssequn1 3252
[Suppes] p. 27Theorem 27unss 3256
[Suppes] p. 27Theorem 28indir 3321
[Suppes] p. 27Theorem 29undir 3322
[Suppes] p. 28Theorem 32difid 3425  difidALT 3426
[Suppes] p. 29Theorem 33difin 3310
[Suppes] p. 29Theorem 34indif 3315
[Suppes] p. 29Theorem 35undif1 3432
[Suppes] p. 29Theorem 36difun2 3436
[Suppes] p. 29Theorem 37difin0 3430
[Suppes] p. 29Theorem 38disjdif 3429
[Suppes] p. 29Theorem 39difundi 3325
[Suppes] p. 29Theorem 40difindi 3327
[Suppes] p. 30Theorem 41nalset 4045
[Suppes] p. 39Theorem 61uniss 3745
[Suppes] p. 39Theorem 65uniop 4159
[Suppes] p. 41Theorem 70intsn 3793
[Suppes] p. 42Theorem 71intpr 3790  intprg 3791
[Suppes] p. 42Theorem 73op1stb 4457
[Suppes] p. 42Theorem 78intun 3789
[Suppes] p. 44Definition 15(a)dfiun2 3832  dfiun2g 3830
[Suppes] p. 44Definition 15(b)dfiin2 3833
[Suppes] p. 47Theorem 86elpw 3533  elpw2 4061  elpw2g 4060  elpwg 3534  elpwgdedVD 27258
[Suppes] p. 47Theorem 87pwid 3539
[Suppes] p. 47Theorem 89pw0 3659
[Suppes] p. 48Theorem 90pwpw0 3660
[Suppes] p. 52Theorem 101xpss12 4696
[Suppes] p. 52Theorem 102xpindi 4723  xpindir 4724
[Suppes] p. 52Theorem 103xpundi 4645  xpundir 4646
[Suppes] p. 54Theorem 105elirrv 7192
[Suppes] p. 58Theorem 2relss 4679
[Suppes] p. 59Theorem 4eldm 4780  eldm2 4781  eldm2g 4779  eldmg 4778
[Suppes] p. 59Definition 3df-dm 4595
[Suppes] p. 60Theorem 6dmin 4790
[Suppes] p. 60Theorem 8rnun 4993
[Suppes] p. 60Theorem 9rnin 4994
[Suppes] p. 60Definition 4dfrn2 4772
[Suppes] p. 61Theorem 11brcnv 4768  brcnvg 4766
[Suppes] p. 62Equation 5elcnv 4762  elcnv2 4763
[Suppes] p. 62Theorem 12relcnv 4955
[Suppes] p. 62Theorem 15cnvin 4992
[Suppes] p. 62Theorem 16cnvun 4990
[Suppes] p. 63Theorem 20co02 5089
[Suppes] p. 63Theorem 21dmcoss 4848
[Suppes] p. 63Definition 7df-co 4594
[Suppes] p. 64Theorem 26cnvco 4769
[Suppes] p. 64Theorem 27coass 5094
[Suppes] p. 65Theorem 31resundi 4873
[Suppes] p. 65Theorem 34elima 4921  elima2 4922  elima3 4923  elimag 4920
[Suppes] p. 65Theorem 35imaundi 4997
[Suppes] p. 66Theorem 40dminss 4999
[Suppes] p. 66Theorem 41imainss 5000
[Suppes] p. 67Exercise 11cnvxp 5001
[Suppes] p. 81Definition 34dfec2 6546
[Suppes] p. 82Theorem 72elec 6582  elecg 6581
[Suppes] p. 82Theorem 73erth 6587  erth2 6588
[Suppes] p. 83Theorem 74erdisj 6590
[Suppes] p. 89Theorem 96map0b 6689
[Suppes] p. 89Theorem 97map0 6691  map0g 6690
[Suppes] p. 89Theorem 98mapsn 6692
[Suppes] p. 89Theorem 99mapss 6693
[Suppes] p. 91Definition 12(ii)alephsuc 7576
[Suppes] p. 91Definition 12(iii)alephlim 7575
[Suppes] p. 92Theorem 1enref 6777  enrefg 6776
[Suppes] p. 92Theorem 2ensym 6793  ensymb 6792  ensymi 6794
[Suppes] p. 92Theorem 3entr 6795
[Suppes] p. 92Theorem 4unen 6825
[Suppes] p. 94Theorem 15endom 6771
[Suppes] p. 94Theorem 16ssdomg 6790
[Suppes] p. 94Theorem 17domtr 6796
[Suppes] p. 95Theorem 18sbth 6863
[Suppes] p. 97Theorem 23canth2 6896  canth2g 6897
[Suppes] p. 97Definition 3brsdom2 6867  df-sdom 6749  dfsdom2 6866
[Suppes] p. 97Theorem 21(i)sdomirr 6880
[Suppes] p. 97Theorem 22(i)domnsym 6869
[Suppes] p. 97Theorem 21(ii)sdomnsym 6868
[Suppes] p. 97Theorem 22(ii)domsdomtr 6878
[Suppes] p. 97Theorem 22(iv)brdom2 6774
[Suppes] p. 97Theorem 21(iii)sdomtr 6881
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6876
[Suppes] p. 98Exercise 4fundmen 6816  fundmeng 6817
[Suppes] p. 98Exercise 6xpdom3 6842
[Suppes] p. 98Exercise 11sdomentr 6877
[Suppes] p. 104Theorem 37fofi 7024
[Suppes] p. 104Theorem 38pwfi 7032
[Suppes] p. 105Theorem 40pwfi 7032
[Suppes] p. 111Axiom for cardinal numberscarden 8052
[Suppes] p. 130Definition 3df-tr 4008
[Suppes] p. 132Theorem 9ssonuni 4466
[Suppes] p. 134Definition 6df-suc 4288
[Suppes] p. 136Theorem Schema 22findes 4574  finds 4570  finds1 4573  finds2 4572
[Suppes] p. 151Theorem 42isfinite 7234  isfinite2 6997  isfiniteg 6999  unbnn 6995
[Suppes] p. 162Definition 5df-ltnq 8419  df-ltpq 8411
[Suppes] p. 197Theorem Schema 4tfindes 4541  tfinds 4538  tfinds2 4542
[Suppes] p. 209Theorem 18oaord1 6432
[Suppes] p. 209Theorem 21oaword2 6434
[Suppes] p. 211Theorem 25oaass 6442
[Suppes] p. 225Definition 8iscard2 7490
[Suppes] p. 227Theorem 56ondomon 8064
[Suppes] p. 228Theorem 59harcard 7492
[Suppes] p. 228Definition 12(i)aleph0 7574
[Suppes] p. 228Theorem Schema 61onintss 4332
[Suppes] p. 228Theorem Schema 62onminesb 4477  onminsb 4478
[Suppes] p. 229Theorem 64alephval2 8071
[Suppes] p. 229Theorem 65alephcard 7578
[Suppes] p. 229Theorem 66alephord2i 7585
[Suppes] p. 229Theorem 67alephnbtwn 7579
[Suppes] p. 229Definition 12df-aleph 7454
[Suppes] p. 242Theorem 6weth 8003
[Suppes] p. 242Theorem 8entric 8058
[Suppes] p. 242Theorem 9carden 8052
[TakeutiZaring] p. 8Axiom 1ax-ext 2234
[TakeutiZaring] p. 13Definition 4.5df-cleq 2246
[TakeutiZaring] p. 13Proposition 4.6df-clel 2249
[TakeutiZaring] p. 13Proposition 4.9cvjust 2248
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2270
[TakeutiZaring] p. 14Definition 4.16df-oprab 5711
[TakeutiZaring] p. 14Proposition 4.14ru 2918
[TakeutiZaring] p. 15Axiom 2zfpair 4103
[TakeutiZaring] p. 15Exercise 1elpr 3559  elpr2 3560  elprg 3558
[TakeutiZaring] p. 15Exercise 2elsn 3556  elsnc 3564  elsnc2 3570  elsnc2g 3569  elsncg 3563
[TakeutiZaring] p. 15Exercise 3elop 4129
[TakeutiZaring] p. 15Exercise 4sneq 3552  sneqr 3677
[TakeutiZaring] p. 15Definition 5.1dfpr2 3557  dfsn2 3555
[TakeutiZaring] p. 16Axiom 3uniex 4404
[TakeutiZaring] p. 16Exercise 6opth 4135
[TakeutiZaring] p. 16Exercise 7opex 4127
[TakeutiZaring] p. 16Exercise 8rext 4113
[TakeutiZaring] p. 16Corollary 5.8unex 4406  unexg 4409
[TakeutiZaring] p. 16Definition 5.3dftp2 3580
[TakeutiZaring] p. 16Definition 5.5df-uni 3725
[TakeutiZaring] p. 16Definition 5.6df-in 3082  df-un 3080
[TakeutiZaring] p. 16Proposition 5.7unipr 3738  uniprg 3739
[TakeutiZaring] p. 17Axiom 4pwex 4084  pwexg 4085
[TakeutiZaring] p. 17Exercise 1eltp 3579
[TakeutiZaring] p. 17Exercise 5elsuc 4351  elsucg 4349  sstr2 3104
[TakeutiZaring] p. 17Exercise 6uncom 3226
[TakeutiZaring] p. 17Exercise 7incom 3266
[TakeutiZaring] p. 17Exercise 8unass 3239
[TakeutiZaring] p. 17Exercise 9inass 3283
[TakeutiZaring] p. 17Exercise 10indi 3319
[TakeutiZaring] p. 17Exercise 11undi 3320
[TakeutiZaring] p. 17Definition 5.9df-pss 3088  dfss2 3089
[TakeutiZaring] p. 17Definition 5.10df-pw 3529
[TakeutiZaring] p. 18Exercise 7unss2 3253
[TakeutiZaring] p. 18Exercise 9df-ss 3086  sseqin2 3292
[TakeutiZaring] p. 18Exercise 10ssid 3115
[TakeutiZaring] p. 18Exercise 12inss1 3293  inss2 3294
[TakeutiZaring] p. 18Exercise 13nss 3154
[TakeutiZaring] p. 18Exercise 15unieq 3733
[TakeutiZaring] p. 18Exercise 18sspwb 4114  sspwimp 27259  sspwimpALT 27266  sspwimpALT2 27270  sspwimpcf 27261
[TakeutiZaring] p. 18Exercise 19pweqb 4121
[TakeutiZaring] p. 19Axiom 5ax-rep 4025
[TakeutiZaring] p. 20Definitiondf-rab 2514
[TakeutiZaring] p. 20Corollary 5.160ex 4044
[TakeutiZaring] p. 20Definition 5.12df-dif 3078
[TakeutiZaring] p. 20Definition 5.14dfnul2 3361
[TakeutiZaring] p. 20Proposition 5.15difid 3425  difidALT 3426
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3368  n0f 3367  neq0 3369
[TakeutiZaring] p. 21Axiom 6zfreg 7190
[TakeutiZaring] p. 21Axiom 6'zfregs 7295
[TakeutiZaring] p. 21Theorem 5.22setind 7300
[TakeutiZaring] p. 21Definition 5.20df-v 2727
[TakeutiZaring] p. 21Proposition 5.21vprc 4046
[TakeutiZaring] p. 22Exercise 10ss 3387
[TakeutiZaring] p. 22Exercise 3ssex 4052  ssexg 4054
[TakeutiZaring] p. 22Exercise 4inex1 4049
[TakeutiZaring] p. 22Exercise 5ruv 7195
[TakeutiZaring] p. 22Exercise 6elirr 7193
[TakeutiZaring] p. 22Exercise 7ssdif0 3417
[TakeutiZaring] p. 22Exercise 11difdif 3216
[TakeutiZaring] p. 22Exercise 13undif3 3333  undif3VD 27223
[TakeutiZaring] p. 22Exercise 14difss 3217
[TakeutiZaring] p. 22Exercise 15sscon 3221
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2511
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2512
[TakeutiZaring] p. 23Proposition 6.2xpex 4705  xpexg 4704  xpexgALT 5919
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4592
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5166
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5299  fun11 5169
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5122  svrelfun 5167
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4771
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4773
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4597
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4598
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4594
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5032  dfrel2 5028
[TakeutiZaring] p. 25Exercise 3xpss 4697
[TakeutiZaring] p. 25Exercise 5relun 4706
[TakeutiZaring] p. 25Exercise 6reluni 4712
[TakeutiZaring] p. 25Exercise 9inxp 4722
[TakeutiZaring] p. 25Exercise 12relres 4887
[TakeutiZaring] p. 25Exercise 13opelres 4864  opelresg 4866
[TakeutiZaring] p. 25Exercise 14dmres 4880
[TakeutiZaring] p. 25Exercise 15resss 4883
[TakeutiZaring] p. 25Exercise 17resabs1 4888
[TakeutiZaring] p. 25Exercise 18funres 5147
[TakeutiZaring] p. 25Exercise 24relco 5074
[TakeutiZaring] p. 25Exercise 29funco 5146
[TakeutiZaring] p. 25Exercise 30f1co 5300
[TakeutiZaring] p. 26Definition 6.10eu2 2138
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 4605  fv3 5390
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5112  cnvexg 5111
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4845  dmexg 4843
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4846  rnexg 4844
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 26756
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 26757
[TakeutiZaring] p. 27Corollary 6.13fvex 5388
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5393  tz6.12 5394  tz6.12c 5397
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5396  tz6.12i 5398
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4600
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4601
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4603  wfo 4587
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4602  wf1 4586
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4604  wf1o 4588
[TakeutiZaring] p. 28Exercise 4eqfnfv 5471  eqfnfv2 5472  eqfnfv2f 5475
[TakeutiZaring] p. 28Exercise 5fvco 5444
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5590  fnexALT 5591
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5586  resfunexgALT 5587
[TakeutiZaring] p. 29Exercise 9funimaex 5184  funimaexg 5183
[TakeutiZaring] p. 29Definition 6.18df-br 3918
[TakeutiZaring] p. 30Definition 6.21dffr2 4248  dffr3 4949  eliniseg 4946  iniseg 4948
[TakeutiZaring] p. 30Definition 6.22df-eprel 4195
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4261  fr3nr 4459  frirr 4260
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4242
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4461
[TakeutiZaring] p. 31Exercise 1frss 4250
[TakeutiZaring] p. 31Exercise 4wess 4270
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23304  tz6.26i 23305  wefrc 4277  wereu2 4280
[TakeutiZaring] p. 32Theorem 6.27wfi 23306  wfii 23307
[TakeutiZaring] p. 32Definition 6.28df-isom 4606
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5675
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5676
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5682
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5683
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5684
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5688
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5695
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5697
[TakeutiZaring] p. 35Notationwtr 4007
[TakeutiZaring] p. 35Theorem 7.2trelpss 26758  tz7.2 4267
[TakeutiZaring] p. 35Definition 7.1dftr3 4011
[TakeutiZaring] p. 36Proposition 7.4ordwe 4295
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4303
[TakeutiZaring] p. 36Proposition 7.6ordelord 4304  ordelordALT 26917  ordelordALTVD 27208
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4310  ordelssne 4309
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4308
[TakeutiZaring] p. 37Proposition 7.9ordin 4312
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4468
[TakeutiZaring] p. 38Corollary 7.15ordsson 4469
[TakeutiZaring] p. 38Definition 7.11df-on 4286
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4314
[TakeutiZaring] p. 38Proposition 7.12onfrALT 26930  ordon 4462
[TakeutiZaring] p. 38Proposition 7.13onprc 4464
[TakeutiZaring] p. 39Theorem 7.17tfi 4532
[TakeutiZaring] p. 40Exercise 3ontr2 4329
[TakeutiZaring] p. 40Exercise 7dftr2 4009
[TakeutiZaring] p. 40Exercise 9onssmin 4476
[TakeutiZaring] p. 40Exercise 11unon 4510
[TakeutiZaring] p. 40Exercise 12ordun 4382
[TakeutiZaring] p. 40Exercise 14ordequn 4381
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4465
[TakeutiZaring] p. 40Proposition 7.20elssuni 3750
[TakeutiZaring] p. 41Definition 7.22df-suc 4288
[TakeutiZaring] p. 41Proposition 7.23sssucid 4359  sucidg 4360
[TakeutiZaring] p. 41Proposition 7.24suceloni 4492
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4374  ordnbtwn 4373
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4507
[TakeutiZaring] p. 42Exercise 1df-lim 4287
[TakeutiZaring] p. 42Exercise 4omssnlim 4558
[TakeutiZaring] p. 42Exercise 7ssnlim 4562
[TakeutiZaring] p. 42Exercise 8onsucssi 4520  ordelsuc 4499
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4501
[TakeutiZaring] p. 42Definition 7.27nlimon 4530
[TakeutiZaring] p. 42Definition 7.28dfom2 4546
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4563
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4564
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4565
[TakeutiZaring] p. 43Remarkomon 4555
[TakeutiZaring] p. 43Axiom 7inf3 7217  omex 7225
[TakeutiZaring] p. 43Theorem 7.32ordom 4553
[TakeutiZaring] p. 43Corollary 7.31find 4569
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4566
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4567
[TakeutiZaring] p. 44Exercise 1limomss 4549
[TakeutiZaring] p. 44Exercise 2int0 3771  trint0 4024
[TakeutiZaring] p. 44Exercise 4intss1 3772
[TakeutiZaring] p. 44Exercise 5intex 4062
[TakeutiZaring] p. 44Exercise 6oninton 4479
[TakeutiZaring] p. 44Exercise 11ordintdif 4331
[TakeutiZaring] p. 44Definition 7.35df-int 3758
[TakeutiZaring] p. 44Proposition 7.34noinfep 7241
[TakeutiZaring] p. 45Exercise 4onint 4474
[TakeutiZaring] p. 47Lemma 1tfrlem1 6274
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6296
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6297
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6298
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6302  tz7.44-2 6303  tz7.44-3 6304
[TakeutiZaring] p. 50Exercise 1smogt 6267
[TakeutiZaring] p. 50Exercise 3smoiso 6262
[TakeutiZaring] p. 50Definition 7.46df-smo 6246
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6340  tz7.49c 6341
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6338
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6337
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6339
[TakeutiZaring] p. 53Proposition 7.532eu5 2197
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7520
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7521
[TakeutiZaring] p. 56Definition 8.1oalim 6414  oasuc 6406
[TakeutiZaring] p. 57Remarktfindsg 4539
[TakeutiZaring] p. 57Proposition 8.2oacl 6417
[TakeutiZaring] p. 57Proposition 8.3oa0 6398  oa0r 6420
[TakeutiZaring] p. 57Proposition 8.16omcl 6418
[TakeutiZaring] p. 58Corollary 8.5oacan 6429
[TakeutiZaring] p. 58Proposition 8.4nnaord 6500  nnaordi 6499  oaord 6428  oaordi 6427
[TakeutiZaring] p. 59Proposition 8.6iunss2 3842  uniss2 3753
[TakeutiZaring] p. 59Proposition 8.7oawordri 6431
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6436  oawordex 6438
[TakeutiZaring] p. 59Proposition 8.9nnacl 6492
[TakeutiZaring] p. 59Proposition 8.10oaabs 6525
[TakeutiZaring] p. 60Remarkoancom 7233
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6441
[TakeutiZaring] p. 62Exercise 1nnarcl 6497
[TakeutiZaring] p. 62Exercise 5oaword1 6433
[TakeutiZaring] p. 62Definition 8.15om0 6399  om0x 6401  omlim 6415  omsuc 6408
[TakeutiZaring] p. 63Proposition 8.17nnecl 6494  nnmcl 6493
[TakeutiZaring] p. 63Proposition 8.19nnmord 6513  nnmordi 6512  omord 6449  omordi 6447
[TakeutiZaring] p. 63Proposition 8.20omcan 6450
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6517  omwordri 6453
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6421
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6423  om1r 6424
[TakeutiZaring] p. 64Proposition 8.22om00 6456
[TakeutiZaring] p. 64Proposition 8.23omordlim 6458
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6459
[TakeutiZaring] p. 64Proposition 8.25odi 6460
[TakeutiZaring] p. 65Theorem 8.26omass 6461
[TakeutiZaring] p. 67Definition 8.30nnesuc 6489  oe0 6404  oelim 6416  oesuc 6409  onesuc 6412
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6402
[TakeutiZaring] p. 67Proposition 8.32oen0 6467
[TakeutiZaring] p. 67Proposition 8.33oeordi 6468
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6403
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6426
[TakeutiZaring] p. 68Corollary 8.34oeord 6469
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6475
[TakeutiZaring] p. 68Proposition 8.35oewordri 6473
[TakeutiZaring] p. 68Proposition 8.37oeworde 6474
[TakeutiZaring] p. 69Proposition 8.41oeoa 6478
[TakeutiZaring] p. 70Proposition 8.42oeoe 6480
[TakeutiZaring] p. 73Theorem 9.1trcl 7291  tz9.1 7292
[TakeutiZaring] p. 76Definition 9.9df-r1 7317  r10 7321  r1lim 7325  r1limg 7324  r1suc 7323  r1sucg 7322
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7333  r1ord2 7334  r1ordg 7331
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7343
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7368  tz9.13 7344  tz9.13g 7345
[TakeutiZaring] p. 79Definition 9.14df-rank 7318  rankval 7369  rankvalb 7350  rankvalg 7370
[TakeutiZaring] p. 79Proposition 9.16rankel 7392  rankelb 7377
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7406  rankval3 7393  rankval3b 7379
[TakeutiZaring] p. 79Proposition 9.18rankonid 7382
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7348
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7387  rankr1c 7374  rankr1g 7385
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7388
[TakeutiZaring] p. 80Exercise 1rankss 7402  rankssb 7401
[TakeutiZaring] p. 80Exercise 2unbndrank 7395
[TakeutiZaring] p. 80Proposition 9.19bndrank 7394
[TakeutiZaring] p. 83Axiom of Choiceac4 7983  dfac3 7629
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7538  numth 7980  numth2 7979
[TakeutiZaring] p. 85Definition 10.4cardval 8049
[TakeutiZaring] p. 85Proposition 10.5cardid 8050  cardid2 7467
[TakeutiZaring] p. 85Proposition 10.9oncard 7474
[TakeutiZaring] p. 85Proposition 10.10carden 8052
[TakeutiZaring] p. 85Proposition 10.11cardidm 7473
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7458
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7479
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7471
[TakeutiZaring] p. 87Proposition 10.15pwen 6916
[TakeutiZaring] p. 88Exercise 1en0 6806
[TakeutiZaring] p. 88Exercise 7infensuc 6921
[TakeutiZaring] p. 89Exercise 10omxpen 6846
[TakeutiZaring] p. 90Corollary 10.23cardnn 7477
[TakeutiZaring] p. 90Definition 10.27alephiso 7606
[TakeutiZaring] p. 90Proposition 10.20nneneq 6926
[TakeutiZaring] p. 90Proposition 10.22onomeneq 6932
[TakeutiZaring] p. 90Proposition 10.26alephprc 7607
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6931
[TakeutiZaring] p. 91Exercise 2alephle 7596
[TakeutiZaring] p. 91Exercise 3aleph0 7574
[TakeutiZaring] p. 91Exercise 4cardlim 7486
[TakeutiZaring] p. 91Exercise 7infpss 7724
[TakeutiZaring] p. 91Exercise 8infcntss 7012
[TakeutiZaring] p. 91Definition 10.29df-fin 6750  isfi 6768
[TakeutiZaring] p. 92Proposition 10.32onfin 6933
[TakeutiZaring] p. 92Proposition 10.34imadomg 8040
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6839
[TakeutiZaring] p. 93Proposition 10.35fodomb 8032
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7696  unxpdom 6952
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7488  cardsdomelir 7487
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 6954
[TakeutiZaring] p. 94Proposition 10.39infxpen 7523
[TakeutiZaring] p. 95Definition 10.42df-map 6657
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8063  infxpidm2 7525
[TakeutiZaring] p. 95Proposition 10.41infcda 7715  infxp 7722  infxpg 24191
[TakeutiZaring] p. 96Proposition 10.44pw2en 6851  pw2f1o 6849
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6909
[TakeutiZaring] p. 97Theorem 10.46ac6s3 7995
[TakeutiZaring] p. 98Theorem 10.46ac6c5 7990  ac6s5 7999
[TakeutiZaring] p. 98Theorem 10.47unidom 8046
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8047  uniimadomf 8048
[TakeutiZaring] p. 100Definition 11.1cfcof 7781
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7776
[TakeutiZaring] p. 102Exercise 1cfle 7761
[TakeutiZaring] p. 102Exercise 2cf0 7758
[TakeutiZaring] p. 102Exercise 3cfsuc 7764
[TakeutiZaring] p. 102Exercise 4cfom 7771
[TakeutiZaring] p. 102Proposition 11.9coftr 7780
[TakeutiZaring] p. 103Theorem 11.15alephreg 8081
[TakeutiZaring] p. 103Proposition 11.11cardcf 7759
[TakeutiZaring] p. 103Proposition 11.13alephsing 7783
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7605
[TakeutiZaring] p. 104Proposition 11.16carduniima 7604
[TakeutiZaring] p. 104Proposition 11.18alephfp 7616  alephfp2 7617
[TakeutiZaring] p. 106Theorem 11.20gchina 8198
[TakeutiZaring] p. 106Theorem 11.21mappwen 7620
[TakeutiZaring] p. 107Theorem 11.26konigth 8068
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8082
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8083
[Tarski] p. 67Axiom B5ax-4 1692
[Tarski] p. 68Lemma 6avril1 20597  equid 1818  equid1 1820  equidALT 1819
[Tarski] p. 69Lemma 7equcomi-o 1823  equcomi 1822
[Tarski] p. 70Lemma 14a4im 1867  a4ime 1868
[Tarski] p. 70Lemma 16ax-11 1624  ax-11o 1940  ax11i 1833
[Tarski] p. 70Lemmas 16 and 17sb6 1992
[Tarski] p. 75Axiom B8ax-9v 1632
[Tarski] p. 75Scheme B7ax9vax9 27722
[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 12357
[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 2210  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 27268
[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 24025
[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 24018
[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 26650
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26651
[WhiteheadRussell] p. 147Theorem *10.2219.26 1592
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26652
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26653
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26654
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1617
[WhiteheadRussell] p. 151Theorem *10.301albitr 26655
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26656
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26657
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26658
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26659
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26661
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26662
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26663
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26660
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26666
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2075
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26667
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26668
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1610
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26669
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26670
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26671
[WhiteheadRussell] p. 162Theorem *11.322alim 26672
[WhiteheadRussell] p. 162Theorem *11.332albi 26673
[WhiteheadRussell] p. 162Theorem *11.342exim 26674
[WhiteheadRussell] p. 162Theorem *11.36a4sbce-2 26676
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26675
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1609
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26678
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26679
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26677
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1571
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26680
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26681
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1578
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26682
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2024  pm11.53g 24060
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26683
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26688
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26684
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26685
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26686
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26687
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26692
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26689
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26690
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26691
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26693
[WhiteheadRussell] p. 175Definition *14.02df-eu 2118
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 26705  pm13.13b 26706
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 26707
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2483
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2484
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2843
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 26713
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 26714
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 26708
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 26934  pm13.193 26709
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 26710
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 26711
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 26712
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 26719
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 26718
[WhiteheadRussell] p. 184Definition *14.01iotasbc 26717
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2970
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 26720  pm14.122b 26721  pm14.122c 26722
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 26723  pm14.123b 26724  pm14.123c 26725
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 26727
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 26726
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 26728
[WhiteheadRussell] p. 190Theorem *14.22iota4 6158
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 26729
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6159
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 26730
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 26732
[WhiteheadRussell] p. 192Theorem *14.26eupick 2176  eupickbi 2179  sbaniota 26733
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 26731
[WhiteheadRussell] p. 192Theorem *14.271eubi 26734
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 26735
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 4605
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7514  pm54.43lem 7513
[Young] p. 141Definition of operator orderingleop2 22465
[Young] p. 142Example 12.2(i)0leop 22471  idleop 22472
[vandenDries] p. 42Lemma 61irrapx1 26010
[vandenDries] p. 43Theorem 62pellex 26017  pellexlem1 26011

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