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 13502
[Adamek] p. 29Proposition 3.14(1)invinv 13516
[Adamek] p. 29Proposition 3.14(2)invco 13517  isoco 13519
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25356
[AitkenIBCG] p. 3Definition 2df-angtrg 25352  df-trcng 25355
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25228  df-ig2 25227
[AitkenIBG] p. 2Definition 4df-li 25243
[AitkenIBG] p. 3Definition 5df-col 25257
[AitkenIBG] p. 3Definition 6df-con2 25262
[AitkenIBG] p. 3Proposition 4isconcl5a 25267  isconcl5ab 25268  isconcl6a 25269  isconcl6ab 25270
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25275
[AitkenIBG] p. 4Exercise 5tpne 25241
[AitkenIBG] p. 4Definition 8df-seg2 25297
[AitkenIBG] p. 4Definition 10df-sside 25329
[AitkenIBG] p. 4Definition 11df-ray2 25318
[AitkenIBG] p. 10Definition 17df-angle 25324
[AitkenIBG] p. 15Definition 23df-triangle 25326
[AitkenIBG] p. 15Definition 24df-cnvx 25345
[AitkenNG] p. 2Definition 1df-slices 25359
[AitkenNG] p. 2Definition 2df-Cut 25361
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25363
[AitkenNG] p. 4Definition 5df-crcl 25365
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18049  df-nmoo 21153
[AkhiezerGlazman] p. 64Theoremhmopidmch 22563  hmopidmchi 22561
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22611  pjcmul2i 22612
[AkhiezerGlazman] p. 72Theoremcnvunop 22328  unoplin 22330
[AkhiezerGlazman] p. 72Equation 2unopadj 22329  unopadj2 22348
[AkhiezerGlazman] p. 73Theoremelunop2 22423  lnopunii 22422
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22496
[Apostol] p. 18Theorem I.1addcan 8876  addcan2d 8896  addcan2i 8886  addcand 8895  addcani 8885
[Apostol] p. 18Theorem I.2negeu 8922
[Apostol] p. 18Theorem I.3negsub 8975  negsubd 9043  negsubi 9004
[Apostol] p. 18Theorem I.4negneg 8977  negnegd 9028  negnegi 8996
[Apostol] p. 18Theorem I.5subdi 9093  subdid 9115  subdii 9108  subdir 9094  subdird 9116  subdiri 9109
[Apostol] p. 18Theorem I.6mul01 8871  mul01d 8891  mul01i 8882  mul02 8870  mul02d 8890  mul02i 8881
[Apostol] p. 18Theorem I.7mulcan 9285  mulcan2d 9282  mulcand 9281  mulcani 9287
[Apostol] p. 18Theorem I.8receu 9293
[Apostol] p. 18Theorem I.9divrec 9320  divrecd 9419  divreci 9385  divreczi 9378
[Apostol] p. 18Theorem I.10recrec 9337  recreci 9372
[Apostol] p. 18Theorem I.11mul0or 9288  mul0ord 9298  mul0ori 9296
[Apostol] p. 18Theorem I.12mul2neg 9099  mul2negd 9114  mul2negi 9107  mulneg1 9096  mulneg1d 9112  mulneg1i 9105
[Apostol] p. 18Theorem I.13divadddiv 9355  divadddivd 9460  divadddivi 9402
[Apostol] p. 18Theorem I.14divmuldiv 9340  divmuldivd 9457  divmuldivi 9400
[Apostol] p. 18Theorem I.15divdivdiv 9341  divdivdivd 9463  divdivdivi 9403
[Apostol] p. 20Axiom 7rpaddcl 10253  rpaddcld 10284  rpmulcl 10254  rpmulcld 10285
[Apostol] p. 20Axiom 8rpneg 10262
[Apostol] p. 20Axiom 90nrp 10263
[Apostol] p. 20Theorem I.17lttri 8825
[Apostol] p. 20Theorem I.18ltadd1d 9245  ltadd1dd 9263  ltadd1i 9207
[Apostol] p. 20Theorem I.19ltmul1 9486  ltmul1a 9485  ltmul1i 9555  ltmul1ii 9565  ltmul2 9487  ltmul2d 10307  ltmul2dd 10321  ltmul2i 9558
[Apostol] p. 20Theorem I.20msqgt0 9174  msqgt0d 9220  msqgt0i 9190
[Apostol] p. 20Theorem I.210lt1 9176
[Apostol] p. 20Theorem I.23lt0neg1 9160  lt0neg1d 9222  ltneg 9154  ltnegd 9230  ltnegi 9197
[Apostol] p. 20Theorem I.25lt2add 9139  lt2addd 9274  lt2addi 9215
[Apostol] p. 20Definition of positive numbersdf-rp 10234
[Apostol] p. 21Exercise 4recgt0 9480  recgt0d 9571  recgt0i 9541  recgt0ii 9542
[Apostol] p. 22Definition of integersdf-z 9904
[Apostol] p. 22Definition of positive integersdfnn3 9640
[Apostol] p. 22Definition of rationalsdf-q 10196
[Apostol] p. 24Theorem I.26supeu 7089
[Apostol] p. 26Theorem I.28nnunb 9840
[Apostol] p. 26Theorem I.29arch 9841
[Apostol] p. 28Exercise 2btwnz 9993
[Apostol] p. 28Exercise 3nnrecl 9842
[Apostol] p. 28Exercise 4rebtwnz 10194
[Apostol] p. 28Exercise 5zbtwnre 10193
[Apostol] p. 28Exercise 6qbtwnre 10404
[Apostol] p. 28Exercise 10(a)zneo 9973
[Apostol] p. 29Theorem I.35msqsqrd 11799  resqrth 11618  sqrth 11725  sqrthi 11731  sqsqrd 11798
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9629
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10163
[Apostol] p. 361Remarkcrreczi 11104
[Apostol] p. 363Remarkabsgt0i 11759
[Apostol] p. 363Exampleabssubd 11812  abssubi 11763
[Baer] p. 40Property (b)mapdord 30517
[Baer] p. 40Property (c)mapd11 30518
[Baer] p. 40Property (e)mapdin 30541  mapdlsm 30543
[Baer] p. 40Property (f)mapd0 30544
[Baer] p. 40Definition of projectivitydf-mapd 30504  mapd1o 30527
[Baer] p. 41Property (g)mapdat 30546
[Baer] p. 44Part (1)mapdpg 30585
[Baer] p. 45Part (2)hdmap1eq 30681  mapdheq 30607  mapdheq2 30608  mapdheq2biN 30609
[Baer] p. 45Part (3)baerlem3 30592
[Baer] p. 46Part (4)mapdheq4 30611  mapdheq4lem 30610
[Baer] p. 46Part (5)baerlem5a 30593  baerlem5abmN 30597  baerlem5amN 30595  baerlem5b 30594  baerlem5bmN 30596
[Baer] p. 47Part (6)hdmap1l6 30701  hdmap1l6a 30689  hdmap1l6e 30694  hdmap1l6f 30695  hdmap1l6g 30696  hdmap1l6lem1 30687  hdmap1l6lem2 30688  hdmap1p6N 30702  mapdh6N 30626  mapdh6aN 30614  mapdh6eN 30619  mapdh6fN 30620  mapdh6gN 30621  mapdh6lem1N 30612  mapdh6lem2N 30613
[Baer] p. 48Part 9hdmapval 30710
[Baer] p. 48Part 10hdmap10 30722
[Baer] p. 48Part 11hdmapadd 30725
[Baer] p. 48Part (6)hdmap1l6h 30697  mapdh6hN 30622
[Baer] p. 48Part (7)mapdh75cN 30632  mapdh75d 30633  mapdh75e 30631  mapdh75fN 30634  mapdh7cN 30628  mapdh7dN 30629  mapdh7eN 30627  mapdh7fN 30630
[Baer] p. 48Part (8)mapdh8 30668  mapdh8a 30654  mapdh8aa 30655  mapdh8ab 30656  mapdh8ac 30657  mapdh8ad 30658  mapdh8b 30659  mapdh8c 30660  mapdh8d 30662  mapdh8d0N 30661  mapdh8e 30663  mapdh8fN 30664  mapdh8g 30665  mapdh8i 30666  mapdh8j 30667
[Baer] p. 48Part (9)mapdh9a 30669
[Baer] p. 48Equation 10mapdhvmap 30648
[Baer] p. 49Part 12hdmap11 30730  hdmapeq0 30726  hdmapf1oN 30747  hdmapneg 30728  hdmaprnN 30746  hdmaprnlem1N 30731  hdmaprnlem3N 30732  hdmaprnlem3uN 30733  hdmaprnlem4N 30735  hdmaprnlem6N 30736  hdmaprnlem7N 30737  hdmaprnlem8N 30738  hdmaprnlem9N 30739  hdmapsub 30729
[Baer] p. 49Part 14hdmap14lem1 30750  hdmap14lem10 30759  hdmap14lem1a 30748  hdmap14lem2N 30751  hdmap14lem2a 30749  hdmap14lem3 30752  hdmap14lem8 30757  hdmap14lem9 30758
[Baer] p. 50Part 14hdmap14lem11 30760  hdmap14lem12 30761  hdmap14lem13 30762  hdmap14lem14 30763  hdmap14lem15 30764  hgmapval 30769
[Baer] p. 50Part 15hgmapadd 30776  hgmapmul 30777  hgmaprnlem2N 30779  hgmapvs 30773
[Baer] p. 50Part 16hgmaprnN 30783
[Baer] p. 110Lemma 1hdmapip0com 30799
[Baer] p. 110Line 27hdmapinvlem1 30800
[Baer] p. 110Line 28hdmapinvlem2 30801
[Baer] p. 110Line 30hdmapinvlem3 30802
[Baer] p. 110Part 1.2hdmapglem5 30804  hgmapvv 30808
[Baer] p. 110Proposition 1hdmapinvlem4 30803
[Baer] p. 111Line 10hgmapvvlem1 30805
[Baer] p. 111Line 15hdmapg 30812  hdmapglem7 30811
[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 4033
[BellMachover] p. 463Scheme Sepaxsep 4037
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4041
[BellMachover] p. 466Axiom Powaxpow3 4085
[BellMachover] p. 466Axiom Unionaxun2 4405
[BellMachover] p. 468Definitiondf-ord 4288
[BellMachover] p. 469Theorem 2.2(i)ordirr 4303
[BellMachover] p. 469Theorem 2.2(iii)onelon 4310
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4305
[BellMachover] p. 471Definition of Ndf-om 4548
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4488
[BellMachover] p. 471Definition of Limdf-lim 4290
[BellMachover] p. 472Axiom Infzfinf2 7227
[BellMachover] p. 473Theorem 2.8limom 4562
[BellMachover] p. 477Equation 3.1df-r1 7320
[BellMachover] p. 478Definitionrankval2 7374
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7338  r1ord3g 7335
[BellMachover] p. 480Axiom Regzfreg2 7194
[BellMachover] p. 488Axiom ACac5 7988  dfac4 7633
[BellMachover] p. 490Definition of alephalephval3 7621
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28198
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22763
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22805  chirredi 22804
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22793
[Beran] p. 3Definition of joinsshjval3 21763
[Beran] p. 39Theorem 2.3(i)cmcm2 22043  cmcm2i 22020  cmcm2ii 22025  cmt2N 28129
[Beran] p. 40Theorem 2.3(iii)lecm 22044  lecmi 22029  lecmii 22030
[Beran] p. 45Theorem 3.4cmcmlem 22018
[Beran] p. 49Theorem 4.2cm2j 22047  cm2ji 22052  cm2mi 22053
[Beran] p. 95Definitiondf-sh 21616  issh2 21618
[Beran] p. 95Lemma 3.1(S5)his5 21495
[Beran] p. 95Lemma 3.1(S6)his6 21508
[Beran] p. 95Lemma 3.1(S7)his7 21499
[Beran] p. 95Lemma 3.2(S8)ho01i 22238
[Beran] p. 95Lemma 3.2(S9)hoeq1 22240
[Beran] p. 95Lemma 3.2(S10)ho02i 22239
[Beran] p. 95Lemma 3.2(S11)hoeq2 22241
[Beran] p. 95Postulate (S1)ax-his1 21491  his1i 21509
[Beran] p. 95Postulate (S2)ax-his2 21492
[Beran] p. 95Postulate (S3)ax-his3 21493
[Beran] p. 95Postulate (S4)ax-his4 21494
[Beran] p. 96Definition of normdf-hnorm 21378  dfhnorm2 21531  normval 21533
[Beran] p. 96Definition for Cauchy sequencehcau 21593
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21383
[Beran] p. 96Definition of complete subspaceisch3 21651
[Beran] p. 96Definition of convergedf-hlim 21382  hlimi 21597
[Beran] p. 97Theorem 3.3(i)norm-i-i 21542  norm-i 21538
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21546  norm-ii 21547  normlem0 21518  normlem1 21519  normlem2 21520  normlem3 21521  normlem4 21522  normlem5 21523  normlem6 21524  normlem7 21525  normlem7tALT 21528
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21548  norm-iii 21549
[Beran] p. 98Remark 3.4bcs 21590  bcsiALT 21588  bcsiHIL 21589
[Beran] p. 98Remark 3.4(B)normlem9at 21530  normpar 21564  normpari 21563
[Beran] p. 98Remark 3.4(C)normpyc 21555  normpyth 21554  normpythi 21551
[Beran] p. 99Remarklnfn0 22457  lnfn0i 22452  lnop0 22376  lnop0i 22380
[Beran] p. 99Theorem 3.5(i)nmcexi 22436  nmcfnex 22463  nmcfnexi 22461  nmcopex 22439  nmcopexi 22437
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22464  nmcfnlbi 22462  nmcoplb 22440  nmcoplbi 22438
[Beran] p. 99Theorem 3.5(iii)lnfncon 22466  lnfnconi 22465  lnopcon 22445  lnopconi 22444
[Beran] p. 100Lemma 3.6normpar2i 21565
[Beran] p. 101Lemma 3.6norm3adifi 21562  norm3adifii 21557  norm3dif 21559  norm3difi 21556
[Beran] p. 102Theorem 3.7(i)chocunii 21710  pjhth 21802  pjhtheu 21803  pjpjhth 21834  pjpjhthi 21835  pjth 18635
[Beran] p. 102Theorem 3.7(ii)ococ 21815  ococi 21814
[Beran] p. 103Remark 3.8nlelchi 22471
[Beran] p. 104Theorem 3.9riesz3i 22472  riesz4 22474  riesz4i 22473
[Beran] p. 104Theorem 3.10cnlnadj 22489  cnlnadjeu 22488  cnlnadjeui 22487  cnlnadji 22486  cnlnadjlem1 22477  nmopadjlei 22498
[Beran] p. 106Theorem 3.11(i)adjeq0 22501
[Beran] p. 106Theorem 3.11(v)nmopadji 22500
[Beran] p. 106Theorem 3.11(ii)adjmul 22502
[Beran] p. 106Theorem 3.11(iv)adjadj 22346
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22512  nmopcoadji 22511
[Beran] p. 106Theorem 3.11(iii)adjadd 22503
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22513
[Beran] p. 106Theorem 3.11(viii)adjcoi 22510  pjadj2coi 22614  pjadjcoi 22571
[Beran] p. 107Definitiondf-ch 21631  isch2 21633
[Beran] p. 107Remark 3.12choccl 21715  isch3 21651  occl 21713  ocsh 21692  shoccl 21714  shocsh 21693
[Beran] p. 107Remark 3.12(B)ococin 21817
[Beran] p. 108Theorem 3.13chintcl 21741
[Beran] p. 109Property (i)pjadj2 22597  pjadj3 22598  pjadji 22112  pjadjii 22101
[Beran] p. 109Property (ii)pjidmco 22591  pjidmcoi 22587  pjidmi 22100
[Beran] p. 110Definition of projector orderingpjordi 22583
[Beran] p. 111Remarkho0val 22160  pjch1 22097
[Beran] p. 111Definitiondf-hfmul 21996  df-hfsum 21995  df-hodif 21994  df-homul 21993  df-hosum 21992
[Beran] p. 111Lemma 4.4(i)pjo 22098
[Beran] p. 111Lemma 4.4(ii)pjch 22121  pjchi 21841
[Beran] p. 111Lemma 4.4(iii)pjoc2 21848  pjoc2i 21847
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22107
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22575  pjssmii 22108
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22574
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22573
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22578
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22576  pjssge0ii 22109
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22577  pjdifnormii 22110
[BourbakiEns] p. Proposition 8fcof1 5649  fcofo 5650
[BourbakiFVR] p. Definition 1isder 24873
[BourbakiTop1] p. Remarkxnegmnf 10415  xnegpnf 10414
[BourbakiTop1] p. Remark rexneg 10416
[BourbakiTop1] p. Theoremneiss 16678
[BourbakiTop1] p. Axiom GT'tgpsubcn 17605
[BourbakiTop1] p. Example 1snfil 17391
[BourbakiTop1] p. Example 2neifil 17407
[BourbakiTop1] p. Definitionistgp 17592
[BourbakiTop1] p. Propositioncnpco 16828  ishmeo 17282  neips 16682
[BourbakiTop1] p. Definition 1filintn0 17388
[BourbakiTop1] p. Proposition 9cnpflf2 17527
[BourbakiTop1] p. Theorem 1 (d)iscncl 16830
[BourbakiTop1] p. Proposition Vissnei2 16685
[BourbakiTop1] p. Definition C'''df-cmp 16946
[BourbakiTop1] p. Proposition Viiinnei 16694
[BourbakiTop1] p. Proposition Vivneissex 16696
[BourbakiTop1] p. Proposition Viiielnei 16680  ssnei 16679
[BourbakiTop1] p. Remark below def. 1filn0 17389
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17373
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17390
[ChoquetDD] p. 2Definition of mappingdf-mpt 3976
[Cohen] p. 301Remarkrelogoprlem 19776
[Cohen] p. 301Property 2relogmul 19777  relogmuld 19808
[Cohen] p. 301Property 3relogdiv 19778  relogdivd 19809
[Cohen] p. 301Property 4relogexp 19781
[Cohen] p. 301Property 1alog1 19771
[Cohen] p. 301Property 1bloge 19772
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10843
[Crawley] p. 1Definition of posetdf-poset 13924
[Crawley] p. 107Theorem 13.2hlsupr 28264
[Crawley] p. 110Theorem 13.3arglem1N 29068  dalaw 28764
[Crawley] p. 111Theorem 13.4hlathil 30843
[Crawley] p. 111Definition of set Wdf-watsN 28868
[Crawley] p. 111Definition of dilationdf-dilN 28984  df-ldil 28982  isldil 28988
[Crawley] p. 111Definition of translationdf-ltrn 28983  df-trnN 28985  isltrn 28997  ltrnu 28999
[Crawley] p. 112Lemma Acdlema1N 28669  cdlema2N 28670  exatleN 28282
[Crawley] p. 112Lemma B1cvrat 28354  cdlemb 28672  cdlemb2 28919  cdlemb3 29484  idltrn 29028  l1cvat 27934  lhpat 28921  lhpat2 28923  lshpat 27935  ltrnel 29017  ltrnmw 29029
[Crawley] p. 112Lemma Ccdlemc1 29069  cdlemc2 29070  ltrnnidn 29052  trlat 29047  trljat1 29044  trljat2 29045  trljat3 29046  trlne 29063  trlnidat 29051  trlnle 29064
[Crawley] p. 112Definition of automorphismdf-pautN 28869
[Crawley] p. 113Lemma Ccdlemc 29075  cdlemc3 29071  cdlemc4 29072
[Crawley] p. 113Lemma Dcdlemd 29085  cdlemd1 29076  cdlemd2 29077  cdlemd3 29078  cdlemd4 29079  cdlemd5 29080  cdlemd6 29081  cdlemd7 29082  cdlemd8 29083  cdlemd9 29084  cdleme31sde 29263  cdleme31se 29260  cdleme31se2 29261  cdleme31snd 29264  cdleme32a 29319  cdleme32b 29320  cdleme32c 29321  cdleme32d 29322  cdleme32e 29323  cdleme32f 29324  cdleme32fva 29315  cdleme32fva1 29316  cdleme32fvcl 29318  cdleme32le 29325  cdleme48fv 29377  cdleme4gfv 29385  cdleme50eq 29419  cdleme50f 29420  cdleme50f1 29421  cdleme50f1o 29424  cdleme50laut 29425  cdleme50ldil 29426  cdleme50lebi 29418  cdleme50rn 29423  cdleme50rnlem 29422  cdlemeg49le 29389  cdlemeg49lebilem 29417
[Crawley] p. 113Lemma Ecdleme 29438  cdleme00a 29087  cdleme01N 29099  cdleme02N 29100  cdleme0a 29089  cdleme0aa 29088  cdleme0b 29090  cdleme0c 29091  cdleme0cp 29092  cdleme0cq 29093  cdleme0dN 29094  cdleme0e 29095  cdleme0ex1N 29101  cdleme0ex2N 29102  cdleme0fN 29096  cdleme0gN 29097  cdleme0moN 29103  cdleme1 29105  cdleme10 29132  cdleme10tN 29136  cdleme11 29148  cdleme11a 29138  cdleme11c 29139  cdleme11dN 29140  cdleme11e 29141  cdleme11fN 29142  cdleme11g 29143  cdleme11h 29144  cdleme11j 29145  cdleme11k 29146  cdleme11l 29147  cdleme12 29149  cdleme13 29150  cdleme14 29151  cdleme15 29156  cdleme15a 29152  cdleme15b 29153  cdleme15c 29154  cdleme15d 29155  cdleme16 29163  cdleme16aN 29137  cdleme16b 29157  cdleme16c 29158  cdleme16d 29159  cdleme16e 29160  cdleme16f 29161  cdleme16g 29162  cdleme19a 29181  cdleme19b 29182  cdleme19c 29183  cdleme19d 29184  cdleme19e 29185  cdleme19f 29186  cdleme1b 29104  cdleme2 29106  cdleme20aN 29187  cdleme20bN 29188  cdleme20c 29189  cdleme20d 29190  cdleme20e 29191  cdleme20f 29192  cdleme20g 29193  cdleme20h 29194  cdleme20i 29195  cdleme20j 29196  cdleme20k 29197  cdleme20l 29200  cdleme20l1 29198  cdleme20l2 29199  cdleme20m 29201  cdleme20y 29180  cdleme20zN 29179  cdleme21 29215  cdleme21d 29208  cdleme21e 29209  cdleme22a 29218  cdleme22aa 29217  cdleme22b 29219  cdleme22cN 29220  cdleme22d 29221  cdleme22e 29222  cdleme22eALTN 29223  cdleme22f 29224  cdleme22f2 29225  cdleme22g 29226  cdleme23a 29227  cdleme23b 29228  cdleme23c 29229  cdleme26e 29237  cdleme26eALTN 29239  cdleme26ee 29238  cdleme26f 29241  cdleme26f2 29243  cdleme26f2ALTN 29242  cdleme26fALTN 29240  cdleme27N 29247  cdleme27a 29245  cdleme27cl 29244  cdleme28c 29250  cdleme3 29115  cdleme30a 29256  cdleme31fv 29268  cdleme31fv1 29269  cdleme31fv1s 29270  cdleme31fv2 29271  cdleme31id 29272  cdleme31sc 29262  cdleme31sdnN 29265  cdleme31sn 29258  cdleme31sn1 29259  cdleme31sn1c 29266  cdleme31sn2 29267  cdleme31so 29257  cdleme35a 29326  cdleme35b 29328  cdleme35c 29329  cdleme35d 29330  cdleme35e 29331  cdleme35f 29332  cdleme35fnpq 29327  cdleme35g 29333  cdleme35h 29334  cdleme35h2 29335  cdleme35sn2aw 29336  cdleme35sn3a 29337  cdleme36a 29338  cdleme36m 29339  cdleme37m 29340  cdleme38m 29341  cdleme38n 29342  cdleme39a 29343  cdleme39n 29344  cdleme3b 29107  cdleme3c 29108  cdleme3d 29109  cdleme3e 29110  cdleme3fN 29111  cdleme3fa 29114  cdleme3g 29112  cdleme3h 29113  cdleme4 29116  cdleme40m 29345  cdleme40n 29346  cdleme40v 29347  cdleme40w 29348  cdleme41fva11 29355  cdleme41sn3aw 29352  cdleme41sn4aw 29353  cdleme41snaw 29354  cdleme42a 29349  cdleme42b 29356  cdleme42c 29350  cdleme42d 29351  cdleme42e 29357  cdleme42f 29358  cdleme42g 29359  cdleme42h 29360  cdleme42i 29361  cdleme42k 29362  cdleme42ke 29363  cdleme42keg 29364  cdleme42mN 29365  cdleme42mgN 29366  cdleme43aN 29367  cdleme43bN 29368  cdleme43cN 29369  cdleme43dN 29370  cdleme5 29118  cdleme50ex 29437  cdleme50ltrn 29435  cdleme51finvN 29434  cdleme51finvfvN 29433  cdleme51finvtrN 29436  cdleme6 29119  cdleme7 29127  cdleme7a 29121  cdleme7aa 29120  cdleme7b 29122  cdleme7c 29123  cdleme7d 29124  cdleme7e 29125  cdleme7ga 29126  cdleme8 29128  cdleme8tN 29133  cdleme9 29131  cdleme9a 29129  cdleme9b 29130  cdleme9tN 29135  cdleme9taN 29134  cdlemeda 29176  cdlemedb 29175  cdlemednpq 29177  cdlemednuN 29178  cdlemefr27cl 29281  cdlemefr32fva1 29288  cdlemefr32fvaN 29287  cdlemefrs32fva 29278  cdlemefrs32fva1 29279  cdlemefs27cl 29291  cdlemefs32fva1 29301  cdlemefs32fvaN 29300  cdlemesner 29174  cdlemeulpq 29098
[Crawley] p. 114Lemma E4atex 28954  4atexlem7 28953  cdleme0nex 29168  cdleme17a 29164  cdleme17c 29166  cdleme17d 29376  cdleme17d1 29167  cdleme17d2 29373  cdleme18a 29169  cdleme18b 29170  cdleme18c 29171  cdleme18d 29173  cdleme4a 29117
[Crawley] p. 115Lemma Ecdleme21a 29203  cdleme21at 29206  cdleme21b 29204  cdleme21c 29205  cdleme21ct 29207  cdleme21f 29210  cdleme21g 29211  cdleme21h 29212  cdleme21i 29213  cdleme22gb 29172
[Crawley] p. 116Lemma Fcdlemf 29441  cdlemf1 29439  cdlemf2 29440
[Crawley] p. 116Lemma Gcdlemftr1 29445  cdlemg16 29535  cdlemg28 29582  cdlemg28a 29571  cdlemg28b 29581  cdlemg3a 29475  cdlemg42 29607  cdlemg43 29608  cdlemg44 29611  cdlemg44a 29609  cdlemg46 29613  cdlemg47 29614  cdlemg9 29512  ltrnco 29597  ltrncom 29616  tgrpabl 29629  trlco 29605
[Crawley] p. 116Definition of Gdf-tgrp 29621
[Crawley] p. 117Lemma Gcdlemg17 29555  cdlemg17b 29540
[Crawley] p. 117Definition of Edf-edring-rN 29634  df-edring 29635
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 29638
[Crawley] p. 118Remarktendopltp 29658
[Crawley] p. 118Lemma Hcdlemh 29695  cdlemh1 29693  cdlemh2 29694
[Crawley] p. 118Lemma Icdlemi 29698  cdlemi1 29696  cdlemi2 29697
[Crawley] p. 118Lemma Jcdlemj1 29699  cdlemj2 29700  cdlemj3 29701  tendocan 29702
[Crawley] p. 118Lemma Kcdlemk 29852  cdlemk1 29709  cdlemk10 29721  cdlemk11 29727  cdlemk11t 29824  cdlemk11ta 29807  cdlemk11tb 29809  cdlemk11tc 29823  cdlemk11u-2N 29767  cdlemk11u 29749  cdlemk12 29728  cdlemk12u-2N 29768  cdlemk12u 29750  cdlemk13-2N 29754  cdlemk13 29730  cdlemk14-2N 29756  cdlemk14 29732  cdlemk15-2N 29757  cdlemk15 29733  cdlemk16-2N 29758  cdlemk16 29735  cdlemk16a 29734  cdlemk17-2N 29759  cdlemk17 29736  cdlemk18-2N 29764  cdlemk18-3N 29778  cdlemk18 29746  cdlemk19-2N 29765  cdlemk19 29747  cdlemk19u 29848  cdlemk1u 29737  cdlemk2 29710  cdlemk20-2N 29770  cdlemk20 29752  cdlemk21-2N 29769  cdlemk21N 29751  cdlemk22-3 29779  cdlemk22 29771  cdlemk23-3 29780  cdlemk24-3 29781  cdlemk25-3 29782  cdlemk26-3 29784  cdlemk26b-3 29783  cdlemk27-3 29785  cdlemk28-3 29786  cdlemk29-3 29789  cdlemk3 29711  cdlemk30 29772  cdlemk31 29774  cdlemk32 29775  cdlemk33N 29787  cdlemk34 29788  cdlemk35 29790  cdlemk36 29791  cdlemk37 29792  cdlemk38 29793  cdlemk39 29794  cdlemk39u 29846  cdlemk4 29712  cdlemk41 29798  cdlemk42 29819  cdlemk42yN 29822  cdlemk43N 29841  cdlemk45 29825  cdlemk46 29826  cdlemk47 29827  cdlemk48 29828  cdlemk49 29829  cdlemk5 29714  cdlemk50 29830  cdlemk51 29831  cdlemk52 29832  cdlemk53 29835  cdlemk54 29836  cdlemk55 29839  cdlemk55u 29844  cdlemk56 29849  cdlemk5a 29713  cdlemk5auN 29738  cdlemk5u 29739  cdlemk6 29715  cdlemk6u 29740  cdlemk7 29726  cdlemk7u-2N 29766  cdlemk7u 29748  cdlemk8 29716  cdlemk9 29717  cdlemk9bN 29718  cdlemki 29719  cdlemkid 29814  cdlemkj-2N 29760  cdlemkj 29741  cdlemksat 29724  cdlemksel 29723  cdlemksv 29722  cdlemksv2 29725  cdlemkuat 29744  cdlemkuel-2N 29762  cdlemkuel-3 29776  cdlemkuel 29743  cdlemkuv-2N 29761  cdlemkuv2-2 29763  cdlemkuv2-3N 29777  cdlemkuv2 29745  cdlemkuvN 29742  cdlemkvcl 29720  cdlemky 29804  cdlemkyyN 29840  tendoex 29853
[Crawley] p. 120Remarkdva1dim 29863
[Crawley] p. 120Lemma Lcdleml1N 29854  cdleml2N 29855  cdleml3N 29856  cdleml4N 29857  cdleml5N 29858  cdleml6 29859  cdleml7 29860  cdleml8 29861  cdleml9 29862  dia1dim 29940
[Crawley] p. 120Lemma Mdia11N 29927  diaf11N 29928  dialss 29925  diaord 29926  dibf11N 30040  djajN 30016
[Crawley] p. 120Definition of isomorphism mapdiaval 29911
[Crawley] p. 121Lemma Mcdlemm10N 29997  dia2dimlem1 29943  dia2dimlem2 29944  dia2dimlem3 29945  dia2dimlem4 29946  dia2dimlem5 29947  diaf1oN 30009  diarnN 30008  dvheveccl 29991  dvhopN 29995
[Crawley] p. 121Lemma Ncdlemn 30091  cdlemn10 30085  cdlemn11 30090  cdlemn11a 30086  cdlemn11b 30087  cdlemn11c 30088  cdlemn11pre 30089  cdlemn2 30074  cdlemn2a 30075  cdlemn3 30076  cdlemn4 30077  cdlemn4a 30078  cdlemn5 30080  cdlemn5pre 30079  cdlemn6 30081  cdlemn7 30082  cdlemn8 30083  cdlemn9 30084  diclspsn 30073
[Crawley] p. 121Definition of phi(q)df-dic 30052
[Crawley] p. 122Lemma Ndih11 30144  dihf11 30146  dihjust 30096  dihjustlem 30095  dihord 30143  dihord1 30097  dihord10 30102  dihord11b 30101  dihord11c 30103  dihord2 30106  dihord2a 30098  dihord2b 30099  dihord2cN 30100  dihord2pre 30104  dihord2pre2 30105  dihordlem6 30092  dihordlem7 30093  dihordlem7b 30094
[Crawley] p. 122Definition of isomorphism mapdihffval 30109  dihfval 30110  dihval 30111
[Eisenberg] p. 67Definition 5.3df-dif 3081
[Eisenberg] p. 82Definition 6.3dfom3 7232
[Eisenberg] p. 125Definition 8.21df-map 6660
[Eisenberg] p. 216Example 13.2(4)omenps 7239
[Eisenberg] p. 310Theorem 19.8cardprc 7497
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8059
[Enderton] p. 18Axiom of Empty Setaxnul 4045
[Enderton] p. 19Definitiondf-tp 3552
[Enderton] p. 26Exercise 5unissb 3755
[Enderton] p. 26Exercise 10pwel 4119
[Enderton] p. 28Exercise 7(b)pwun 4195
[Enderton] p. 30Theorem "Distributive laws"iinin1 3871  iinin2 3870  iinun2 3866  iunin1 3865  iunin2 3864
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3869  iundif2 3867
[Enderton] p. 32Exercise 20unineq 3326
[Enderton] p. 33Exercise 23iinuni 3883
[Enderton] p. 33Exercise 25iununi 3884
[Enderton] p. 33Exercise 24(a)iinpw 3888
[Enderton] p. 33Exercise 24(b)iunpw 4461  iunpwss 3889
[Enderton] p. 36Definitionopthwiener 4161
[Enderton] p. 38Exercise 6(a)unipw 4118
[Enderton] p. 38Exercise 6(b)pwuni 4100
[Enderton] p. 41Lemma 3Dopeluu 4417  rnex 4849  rnexg 4847
[Enderton] p. 41Exercise 8dmuni 4795  rnuni 4999
[Enderton] p. 42Definition of a functiondffun7 5138  dffun8 5139
[Enderton] p. 43Definition of function valuefunfv2 5439
[Enderton] p. 43Definition of single-rootedfuncnv 5167
[Enderton] p. 44Definition (d)dfima2 4921  dfima3 4922
[Enderton] p. 47Theorem 3Hfvco2 5446
[Enderton] p. 49Axiom of Choice (first form)ac7 7984  ac7g 7985  df-ac 7627  dfac2 7641  dfac2a 7640  dfac3 7632  dfac7 7642
[Enderton] p. 50Theorem 3K(a)imauni 5624
[Enderton] p. 52Definitiondf-map 6660
[Enderton] p. 53Exercise 21coass 5097
[Enderton] p. 53Exercise 27dmco 5087
[Enderton] p. 53Exercise 14(a)funin 5176
[Enderton] p. 53Exercise 22(a)imass2 4956
[Enderton] p. 54Remarkixpf 6724  ixpssmap 6736
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6704
[Enderton] p. 55Axiom of Choice (second form)ac9 7994  ac9s 8004
[Enderton] p. 56Theorem 3Merref 6566
[Enderton] p. 57Lemma 3Nerthi 6592
[Enderton] p. 57Definitiondf-ec 6548
[Enderton] p. 58Definitiondf-qs 6552
[Enderton] p. 60Theorem 3Qth3q 6653  th3qcor 6652  th3qlem1 6650  th3qlem2 6651
[Enderton] p. 61Exercise 35df-ec 6548
[Enderton] p. 65Exercise 56(a)dmun 4792
[Enderton] p. 68Definition of successordf-suc 4291
[Enderton] p. 71Definitiondf-tr 4011  dftr4 4015
[Enderton] p. 72Theorem 4Eunisuc 4361
[Enderton] p. 73Exercise 6unisuc 4361
[Enderton] p. 73Exercise 5(a)truni 4024
[Enderton] p. 73Exercise 5(b)trint 4025  trintALT 27347
[Enderton] p. 79Theorem 4I(A1)nna0 6488
[Enderton] p. 79Theorem 4I(A2)nnasuc 6490  onasuc 6413
[Enderton] p. 79Definition of operation valuedf-ov 5713
[Enderton] p. 80Theorem 4J(A1)nnm0 6489
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6491  onmsuc 6414
[Enderton] p. 81Theorem 4K(1)nnaass 6506
[Enderton] p. 81Theorem 4K(2)nna0r 6493  nnacom 6501
[Enderton] p. 81Theorem 4K(3)nndi 6507
[Enderton] p. 81Theorem 4K(4)nnmass 6508
[Enderton] p. 81Theorem 4K(5)nnmcom 6510
[Enderton] p. 82Exercise 16nnm0r 6494  nnmsucr 6509
[Enderton] p. 88Exercise 23nnaordex 6522
[Enderton] p. 129Definitiondf-en 6750
[Enderton] p. 132Theorem 6B(b)canth 6178
[Enderton] p. 133Exercise 1xpomen 7527
[Enderton] p. 133Exercise 2qnnen 12366
[Enderton] p. 134Theorem (Pigeonhole Principle)php 6930
[Enderton] p. 135Corollary 6Cphp3 6932
[Enderton] p. 136Corollary 6Enneneq 6929
[Enderton] p. 136Corollary 6D(a)pssinf 6958
[Enderton] p. 136Corollary 6D(b)ominf 6960
[Enderton] p. 137Lemma 6Fpssnn 6966
[Enderton] p. 138Corollary 6Gssfi 6968
[Enderton] p. 139Theorem 6H(c)mapen 6910
[Enderton] p. 142Theorem 6I(3)xpcdaen 7693
[Enderton] p. 142Theorem 6I(4)mapcdaen 7694
[Enderton] p. 143Theorem 6Jcda0en 7689  cda1en 7685
[Enderton] p. 144Exercise 13iunfi 7029  unifi 7030  unifi2 7031
[Enderton] p. 144Corollary 6Kundif2 3436  unfi 7009  unfi2 7011
[Enderton] p. 145Figure 38ffoss 5362
[Enderton] p. 145Definitiondf-dom 6751
[Enderton] p. 146Example 1domen 6761  domeng 6762
[Enderton] p. 146Example 3nndomo 6939  nnsdom 7238  nnsdomg 7001
[Enderton] p. 149Theorem 6L(a)cdadom2 7697
[Enderton] p. 149Theorem 6L(c)mapdom1 6911  xpdom1 6846  xpdom1g 6844  xpdom2g 6843
[Enderton] p. 149Theorem 6L(d)mapdom2 6917
[Enderton] p. 151Theorem 6Mzorn 8018  zorng 8015
[Enderton] p. 151Theorem 6M(4)ac8 8003  dfac5 7639
[Enderton] p. 159Theorem 6Qunictb 8077
[Enderton] p. 164Exampleinfdif 7719
[Enderton] p. 168Definitiondf-po 4207
[Enderton] p. 192Theorem 7M(a)oneli 4391
[Enderton] p. 192Theorem 7M(b)ontr1 4331
[Enderton] p. 192Theorem 7M(c)onirri 4390
[Enderton] p. 193Corollary 7N(b)0elon 4338
[Enderton] p. 193Corollary 7N(c)onsuci 4520
[Enderton] p. 193Corollary 7N(d)ssonunii 4470
[Enderton] p. 194Remarkonprc 4467
[Enderton] p. 194Exercise 16suc11 4387
[Enderton] p. 197Definitiondf-card 7456
[Enderton] p. 197Theorem 7Pcarden 8055
[Enderton] p. 200Exercise 25tfis 4536
[Enderton] p. 202Lemma 7Tr1tr 7332
[Enderton] p. 202Definitiondf-r1 7320
[Enderton] p. 202Theorem 7Qr1val1 7342
[Enderton] p. 204Theorem 7V(b)rankval4 7423
[Enderton] p. 206Theorem 7X(b)en2lp 7201
[Enderton] p. 207Exercise 30rankpr 7413  rankprb 7407  rankpw 7399  rankpwi 7379  rankuniss 7422
[Enderton] p. 207Exercise 34opthreg 7203
[Enderton] p. 208Exercise 35suc11reg 7204
[Enderton] p. 212Definition of alephalephval3 7621
[Enderton] p. 213Theorem 8A(a)alephord2 7587
[Enderton] p. 213Theorem 8A(b)cardalephex 7601
[Enderton] p. 218Theorem Schema 8Eonfununi 6244
[Enderton] p. 222Definition of kardkarden 7449  kardex 7448
[Enderton] p. 238Theorem 8Roeoa 6481
[Enderton] p. 238Theorem 8Soeoe 6483
[Enderton] p. 240Exercise 25oarec 6446
[Enderton] p. 257Definition of cofinalitycflm 7760
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18726
[Fremlin5] p. 213Lemma 565Cauniioovol 18766
[Fremlin5] p. 214Lemma 565Cauniioombl 18776
[FreydScedrov] p. 283Axiom of Infinityax-inf 7223  inf1 7207  inf2 7208
[Gleason] p. 117Proposition 9-2.1df-enq 8415  enqer 8425
[Gleason] p. 117Proposition 9-2.2df-1nq 8420  df-nq 8416
[Gleason] p. 117Proposition 9-2.3df-plpq 8412  df-plq 8418
[Gleason] p. 119Proposition 9-2.4caovmo 5909  df-mpq 8413  df-mq 8419
[Gleason] p. 119Proposition 9-2.5df-rq 8421
[Gleason] p. 119Proposition 9-2.6ltexnq 8479
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8480  ltbtwnnq 8482
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8475
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8476
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8483
[Gleason] p. 121Definition 9-3.1df-np 8485
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8497
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8499
[Gleason] p. 122Definitiondf-1p 8486
[Gleason] p. 122Remark (1)prub 8498
[Gleason] p. 122Lemma 9-3.4prlem934 8537
[Gleason] p. 122Proposition 9-3.2df-ltp 8489
[Gleason] p. 122Proposition 9-3.3ltsopr 8536  psslinpr 8535  supexpr 8558  suplem1pr 8556  suplem2pr 8557
[Gleason] p. 123Proposition 9-3.5addclpr 8522  addclprlem1 8520  addclprlem2 8521  df-plp 8487
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8526
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8525
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8538
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8547  ltexprlem1 8540  ltexprlem2 8541  ltexprlem3 8542  ltexprlem4 8543  ltexprlem5 8544  ltexprlem6 8545  ltexprlem7 8546
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8549  ltaprlem 8548
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8550
[Gleason] p. 124Lemma 9-3.6prlem936 8551
[Gleason] p. 124Proposition 9-3.7df-mp 8488  mulclpr 8524  mulclprlem 8523  reclem2pr 8552
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8533
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8528
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8527
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8532
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8555  reclem3pr 8553  reclem4pr 8554
[Gleason] p. 126Proposition 9-4.1df-enr 8561  df-mpr 8560  df-plpr 8559  enrer 8570
[Gleason] p. 126Proposition 9-4.2df-0r 8566  df-1r 8567  df-nr 8562
[Gleason] p. 126Proposition 9-4.3df-mr 8564  df-plr 8563  negexsr 8604  recexsr 8609  recexsrlem 8605
[Gleason] p. 127Proposition 9-4.4df-ltr 8565
[Gleason] p. 130Proposition 10-1.3creui 9621  creur 9620  cru 9618
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8690  axcnre 8666
[Gleason] p. 132Definition 10-3.1crim 11477  crimd 11594  crimi 11555  crre 11476  crred 11593  crrei 11554
[Gleason] p. 132Definition 10-3.2remim 11479  remimd 11560
[Gleason] p. 133Definition 10.36absval2 11646  absval2d 11804  absval2i 11757
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11503  cjaddd 11582  cjaddi 11550
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11504  cjmuld 11583  cjmuli 11551
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11502  cjcjd 11561  cjcji 11533
[Gleason] p. 133Proposition 10-3.4(f)cjre 11501  cjreb 11485  cjrebd 11564  cjrebi 11536  cjred 11588  rere 11484  rereb 11482  rerebd 11563  rerebi 11535  rered 11586
[Gleason] p. 133Proposition 10-3.4(h)addcj 11510  addcjd 11574  addcji 11545
[Gleason] p. 133Proposition 10-3.7(a)absval 11600
[Gleason] p. 133Proposition 10-3.7(b)abscj 11641  abscjd 11809  abscji 11761
[Gleason] p. 133Proposition 10-3.7(c)abs00 11651  abs00d 11805  abs00i 11758  absne0d 11806
[Gleason] p. 133Proposition 10-3.7(d)releabs 11682  releabsd 11810  releabsi 11762
[Gleason] p. 133Proposition 10-3.7(f)absmul 11656  absmuld 11813  absmuli 11764
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11644  sqabsaddi 11765
[Gleason] p. 133Proposition 10-3.7(h)abstri 11691  abstrid 11815  abstrii 11768
[Gleason] p. 134Definition 10-4.1df-exp 10983  exp0 10986  expp1 10988  expp1d 11124
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 19894  cxpaddd 19932  expadd 11022  expaddd 11125  expaddz 11024
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 19903  cxpmuld 19949  expmul 11025  expmuld 11126  expmulz 11026
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 19900  mulcxpd 19943  mulexp 11019  mulexpd 11138  mulexpz 11020
[Gleason] p. 140Exercise 1znnen 12365
[Gleason] p. 141Definition 11-2.1fzval 10662
[Gleason] p. 168Proposition 12-2.1(a)climadd 11982  rlimadd 11993  rlimdiv 11996
[Gleason] p. 168Proposition 12-2.1(b)climsub 11984  rlimsub 11994
[Gleason] p. 168Proposition 12-2.1(c)climmul 11983  rlimmul 11995
[Gleason] p. 171Corollary 12-2.2climmulc2 11987
[Gleason] p. 172Corollary 12-2.5climrecl 11934
[Gleason] p. 172Proposition 12-2.4(c)climabs 11954  climcj 11955  climim 11957  climre 11956  rlimabs 11959  rlimcj 11960  rlimim 11962  rlimre 11961
[Gleason] p. 173Definition 12-3.1df-ltxr 8752  df-xr 8751  ltxr 10336
[Gleason] p. 175Definition 12-4.1df-limsup 11822  limsupval 11825
[Gleason] p. 180Theorem 12-5.1climsup 12020
[Gleason] p. 180Theorem 12-5.3caucvg 12028  caucvgb 12029  caucvgr 12025  climcau 12021
[Gleason] p. 182Exercise 3cvgcmp 12151
[Gleason] p. 182Exercise 4cvgrat 12213
[Gleason] p. 195Theorem 13-2.12abs1m 11696
[Gleason] p. 217Lemma 13-4.1btwnzge0 10831
[Gleason] p. 223Definition 14-1.1df-met 16206
[Gleason] p. 223Definition 14-1.1(a)met0 17740  xmet0 17739
[Gleason] p. 223Definition 14-1.1(b)metgt0 17755
[Gleason] p. 223Definition 14-1.1(c)metsym 17746
[Gleason] p. 223Definition 14-1.1(d)mettri 17748  mstri 17847  xmettri 17747  xmstri 17846
[Gleason] p. 225Definition 14-1.5xpsmet 17778
[Gleason] p. 230Proposition 14-2.6txlm 17174
[Gleason] p. 240Theorem 14-4.3metcnp4 18567
[Gleason] p. 240Proposition 14-4.2metcnp3 17918
[Gleason] p. 243Proposition 14-4.16addcn 18201  addcn2 11944  mulcn 18203  mulcn2 11946  subcn 18202  subcn2 11945
[Gleason] p. 295Remarkbcval3 11197  bcval4 11198
[Gleason] p. 295Equation 2bcpasc 11211
[Gleason] p. 295Definition of binomial coefficientbcval 11195  df-bc 11194
[Gleason] p. 296Remarkbcn0 11201  bcnn 11202
[Gleason] p. 296Theorem 15-2.8binom 12165
[Gleason] p. 308Equation 2ef0 12246
[Gleason] p. 308Equation 3efcj 12247
[Gleason] p. 309Corollary 15-4.3efne0 12251
[Gleason] p. 309Corollary 15-4.4efexp 12255
[Gleason] p. 310Equation 14sinadd 12318
[Gleason] p. 310Equation 15cosadd 12319
[Gleason] p. 311Equation 17sincossq 12330
[Gleason] p. 311Equation 18cosbnd 12335  sinbnd 12334
[Gleason] p. 311Lemma 15-4.7sqeqor 11095  sqeqori 11093
[Gleason] p. 311Definition of pidf-pi 12228
[Godowski] p. 730Equation SFgoeqi 22683
[GodowskiGreechie] p. 249Equation IV3oai 22095
[Halmos] p. 31Theorem 17.3riesz1 22475  riesz2 22476
[Halmos] p. 41Definition of Hermitianhmopadj2 22351
[Halmos] p. 42Definition of projector orderingpjordi 22583
[Halmos] p. 43Theorem 26.1elpjhmop 22595  elpjidm 22594  pjnmopi 22558
[Halmos] p. 44Remarkpjinormi 22114  pjinormii 22103
[Halmos] p. 44Theorem 26.2elpjch 22599  pjrn 22134  pjrni 22129  pjvec 22123
[Halmos] p. 44Theorem 26.3pjnorm2 22154
[Halmos] p. 44Theorem 26.4hmopidmpj 22564  hmopidmpji 22562
[Halmos] p. 45Theorem 27.1pjinvari 22601
[Halmos] p. 45Theorem 27.3pjoci 22590  pjocvec 22124
[Halmos] p. 45Theorem 27.4pjorthcoi 22579
[Halmos] p. 48Theorem 29.2pjssposi 22582
[Halmos] p. 48Theorem 29.3pjssdif1i 22585  pjssdif2i 22584
[Halmos] p. 50Definition of spectrumdf-spec 22265
[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 18322  df-phtpy 18301
[Hatcher] p. 26Definitiondf-pco 18335  df-pi1 18338
[Hatcher] p. 26Proposition 1.2phtpcer 18325
[Hatcher] p. 26Proposition 1.3pi1grp 18380
[Herstein] p. 54Exercise 28df-grpo 20688
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14333  grpoideu 20706  mndideu 14210
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14351  grpoinveu 20719
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14370  grpo2inv 20736
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14379  grpoinvop 20738
[Herstein] p. 57Exercise 1isgrp2d 20732  isgrp2i 20733
[Hitchcock] p. 5Rule A3mpto1 1528
[Hitchcock] p. 5Rule A4mpto2 1529
[Hitchcock] p. 5Rule A5mtp-xor 1530
[Holland] p. 1519Theorem 2sumdmdi 22830
[Holland] p. 1520Lemma 5cdj1i 22843  cdj3i 22851  cdj3lem1 22844  cdjreui 22842
[Holland] p. 1524Lemma 7mddmdin0i 22841
[Holland95] p. 13Theorem 3.6hlathil 30843
[Holland95] p. 14Line 15hgmapvs 30773
[Holland95] p. 14Line 16hdmaplkr 30795
[Holland95] p. 14Line 17hdmapellkr 30796
[Holland95] p. 14Line 19hdmapglnm2 30793
[Holland95] p. 14Line 20hdmapip0com 30799
[Holland95] p. 14Theorem 3.6hdmapevec2 30718
[Holland95] p. 14Lines 24 and 25hdmapoc 30813
[Holland95] p. 204Definition of involutiondf-srng 15446
[Holland95] p. 212Definition of subspacedf-psubsp 28381
[Holland95] p. 214Lemma 3.3lclkrlem2v 30407
[Holland95] p. 214Definition 3.2df-lpolN 30360
[Holland95] p. 214Definition of nonsingularpnonsingN 28811
[Holland95] p. 215Lemma 3.3(1)dihoml4 30256  poml4N 28831
[Holland95] p. 215Lemma 3.3(2)dochexmid 30347  pexmidALTN 28856  pexmidN 28847
[Holland95] p. 218Theorem 3.6lclkr 30412
[Holland95] p. 218Definition of dual vector spacedf-ldual 28003  ldualset 28004
[Holland95] p. 222Item 1df-lines 28379  df-pointsN 28380
[Holland95] p. 222Item 2df-polarityN 28781
[Holland95] p. 223Remarkispsubcl2N 28825  omllaw4 28125  pol1N 28788  polcon3N 28795
[Holland95] p. 223Definitiondf-psubclN 28813
[Holland95] p. 223Equation for polaritypolval2N 28784
[Hughes] p. 44Equation 1.21bax-his3 21493
[Hughes] p. 47Definition of projection operatordfpjop 22592
[Hughes] p. 49Equation 1.30eighmre 22373  eigre 22245  eigrei 22244
[Hughes] p. 49Equation 1.31eighmorth 22374  eigorth 22248  eigorthi 22247
[Hughes] p. 137Remark (ii)eigposi 22246
[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 8081
[Jech] p. 42Equation 6.1alephadd 8079  alephmul 8080
[Jech] p. 43Lemma 6.2infmap 8078  infmap2 7728
[Jech] p. 71Lemma 9.3jech9.3 7370
[Jech] p. 72Equation 9.3scott0 7440  scottex 7439
[Jech] p. 72Exercise 9.1rankval4 7423
[Jech] p. 72Scheme "Collection Principle"cp 7445
[Jech] p. 78Definition implied by the footnoteopthprc 4643
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26166
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26262
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26263
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26178
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26182
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26183  rmyp1 26184
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26185  rmym1 26186
[JonesMatijasevic] p. 695Equation 2.11rmx0 26176  rmx1 26177  rmxluc 26187
[JonesMatijasevic] p. 695Equation 2.12rmy0 26180  rmy1 26181  rmyluc 26188
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26190
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26191
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26213  jm2.17b 26214  jm2.17c 26215
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26252
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26256
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26247
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26216  jm2.24nn 26212
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26261
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26267  rmygeid 26217
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26279
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1684
[Kalmbach] p. 14Definition of latticechabs1 21925  chabs1i 21927  chabs2 21926  chabs2i 21928  chjass 21942  chjassi 21895  latabs1 14037  latabs2 14038
[Kalmbach] p. 15Definition of atomdf-at 22748  ela 22749
[Kalmbach] p. 15Definition of coverscvbr2 22693  cvrval2 28153
[Kalmbach] p. 16Definitiondf-ol 28057  df-oml 28058
[Kalmbach] p. 20Definition of commutescmbr 22011  cmbri 22017  cmtvalN 28090  df-cm 22010  df-cmtN 28056
[Kalmbach] p. 22Remarkomllaw5N 28126  pjoml5 22040  pjoml5i 22015
[Kalmbach] p. 22Definitionpjoml2 22038  pjoml2i 22012
[Kalmbach] p. 22Theorem 2(v)cmcm 22041  cmcmi 22019  cmcmii 22024  cmtcomN 28128
[Kalmbach] p. 22Theorem 2(ii)omllaw3 28124  omlsi 21813  pjoml 21845  pjomli 21844
[Kalmbach] p. 22Definition of OML lawomllaw2N 28123
[Kalmbach] p. 23Remarkcmbr2i 22023  cmcm3 22042  cmcm3i 22021  cmcm3ii 22026  cmcm4i 22022  cmt3N 28130  cmt4N 28131  cmtbr2N 28132
[Kalmbach] p. 23Lemma 3cmbr3 22035  cmbr3i 22027  cmtbr3N 28133
[Kalmbach] p. 25Theorem 5fh1 22045  fh1i 22048  fh2 22046  fh2i 22049  omlfh1N 28137
[Kalmbach] p. 65Remarkchjatom 22767  chslej 21907  chsleji 21867  shslej 21789  shsleji 21779
[Kalmbach] p. 65Proposition 1chocin 21904  chocini 21863  chsupcl 21749  chsupval2 21819  h0elch 21664  helch 21653  hsupval2 21818  ocin 21705  ococss 21702  shococss 21703
[Kalmbach] p. 65Definition of subspace sumshsval 21721
[Kalmbach] p. 66Remarkdf-pjh 21804  pjssmi 22575  pjssmii 22108
[Kalmbach] p. 67Lemma 3osum 22072  osumi 22069
[Kalmbach] p. 67Lemma 4pjci 22610
[Kalmbach] p. 103Exercise 6atmd2 22810
[Kalmbach] p. 103Exercise 12mdsl0 22720
[Kalmbach] p. 140Remarkhatomic 22770  hatomici 22769  hatomistici 22772
[Kalmbach] p. 140Proposition 1atlatmstc 28198
[Kalmbach] p. 140Proposition 1(i)atexch 22791  lsatexch 27922
[Kalmbach] p. 140Proposition 1(ii)chcv1 22765  cvlcvr1 28218  cvr1 28288
[Kalmbach] p. 140Proposition 1(iii)cvexch 22784  cvexchi 22779  cvrexch 28298
[Kalmbach] p. 149Remark 2chrelati 22774  hlrelat 28280  hlrelat5N 28279  lrelat 27893
[Kalmbach] p. 153Exercise 5lsmcv 15729  lsmsatcv 27889  spansncv 22080  spansncvi 22079
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 27908  spansncv2 22703
[Kalmbach] p. 266Definitiondf-st 22621
[Kalmbach2] p. 8Definition of adjointdf-adjh 22259
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8148  fpwwe2 8145
[KanamoriPincus] p. 416Corollary 1.3canth4 8149
[KanamoriPincus] p. 417Corollary 1.6canthp1 8156
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8151
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8153
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8166
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8170  gchxpidm 8171
[KanamoriPincus] p. 419Theorem 2.1gchacg 8174  gchhar 8173
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7726  unxpwdom 7187
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8176
[Kreyszig] p. 3Property M1metcl 17729  xmetcl 17728
[Kreyszig] p. 4Property M2meteq0 17736
[Kreyszig] p. 8Definition 1.1-8dscmet 17927
[Kreyszig] p. 12Equation 5conjmul 9357  muleqadd 9292
[Kreyszig] p. 18Definition 1.3-2mopnval 17816
[Kreyszig] p. 19Remarkmopntopon 17817
[Kreyszig] p. 19Theorem T1mopn0 17876  mopnm 17822
[Kreyszig] p. 19Theorem T2unimopn 17874
[Kreyszig] p. 19Definition of neighborhoodneibl 17879
[Kreyszig] p. 20Definition 1.3-3metcnp2 17920
[Kreyszig] p. 25Definition 1.4-1lmbr 16820  lmmbr 18516  lmmbr2 18517
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 16940
[Kreyszig] p. 28Theorem 1.4-5lmcau 18570
[Kreyszig] p. 28Definition 1.4-3iscau 18534  iscmet2 18552
[Kreyszig] p. 30Theorem 1.4-7cmetss 18572
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17019  metelcls 18562
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18563  metcld2 18564
[Kreyszig] p. 51Equation 2clmvneg1 18421  lmodvneg1 15502  nvinv 21027  vcm 20957
[Kreyszig] p. 51Equation 1aclm0vs 18420  lmod0vs 15498  vc0 20955
[Kreyszig] p. 51Equation 1blmodvs0 15499  vcz 20956
[Kreyszig] p. 58Definition 2.2-1imsmet 21090
[Kreyszig] p. 59Equation 1imsdval 21085  imsdval2 21086
[Kreyszig] p. 63Problem 1nvnd 21087
[Kreyszig] p. 64Problem 2nvge0 21070  nvz 21065
[Kreyszig] p. 64Problem 3nvabs 21069
[Kreyszig] p. 91Definition 2.7-1isblo3i 21209
[Kreyszig] p. 92Equation 2df-nmoo 21153
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21215  blocni 21213
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21214
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18471  ipeq0 16374  ipz 21125
[Kreyszig] p. 135Problem 2pythi 21258
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21262
[Kreyszig] p. 144Equation 4supcvg 12188
[Kreyszig] p. 144Theorem 3.3-1minvec 18632  minveco 21293
[Kreyszig] p. 196Definition 3.9-1df-aj 21158
[Kreyszig] p. 247Theorem 4.7-2bcth 18583
[Kreyszig] p. 249Theorem 4.7-3ubth 21282
[Kreyszig] p. 470Definition of positive operator orderingleop 22533  leopg 22532
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22551
[Kreyszig] p. 525Theorem 10.1-1htth 21328
[Kunen] p. 10Axiom 0a9e 1817  axnul 4045
[Kunen] p. 11Axiom 3axnul 4045
[Kunen] p. 12Axiom 6zfrep6 5600
[Kunen] p. 24Definition 10.24mapval 6670  mapvalg 6668
[Kunen] p. 30Lemma 10.20fodom 8033
[Kunen] p. 31Definition 10.24mapex 6664
[Kunen] p. 95Definition 2.1df-r1 7320
[Kunen] p. 97Lemma 2.10r1elss 7362  r1elssi 7361
[Kunen] p. 107Exercise 4rankop 7414  rankopb 7408  rankuni 7419  rankxplim 7433  rankxpsuc 7436
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3813
[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 20650  ex-natded5.2 20649
[Laboreo] p. 16Theorem 5.3ex-natded5.3-2 20653  ex-natded5.3 20652
[Laboreo] p. 18Theorem 5.5ex-natded5.5 20655
[Laboreo] p. 19Theorem 5.7ex-natded5.7-2 20657  ex-natded5.7 20656
[Laboreo] p. 20Theorem 5.8ex-natded5.8-2 20659  ex-natded5.8 20658
[Laboreo] p. 20Theorem 5.13ex-natded5.13-2 20661  ex-natded5.13 20660
[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. 43Theorem 9.20ex-natded9.20 20662
[Laboreo] p. 45Theorem 9.20ex-natded9.20-2 20663
[Laboreo] p. 45Theorem 9.26ex-natded9.26-2 20665  ex-natded9.26 20664
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26717
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26712
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26718
[LeBlanc] p. 277Rule R2axnul 4045
[Levy] p. 338Axiomdf-clab 2240  df-clel 2249  df-cleq 2246
[Levy58] p. 2Definition Iisfin1-3 7896
[Levy58] p. 2Definition IIdf-fin2 7796
[Levy58] p. 2Definition Iadf-fin1a 7795
[Levy58] p. 2Definition IIIdf-fin3 7798
[Levy58] p. 3Definition Vdf-fin5 7799
[Levy58] p. 3Definition IVdf-fin4 7797
[Levy58] p. 4Definition VIdf-fin6 7800
[Levy58] p. 4Definition VIIdf-fin7 7801
[Levy58], p. 3Theorem 1fin1a2 7925
[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 22818
[Maeda] p. 168Lemma 5mdsym 22822  mdsymi 22821
[Maeda] p. 168Lemma 4(i)mdsymlem4 22816  mdsymlem6 22818  mdsymlem7 22819
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22820
[MaedaMaeda] p. 1Remarkssdmd1 22723  ssdmd2 22724  ssmd1 22721  ssmd2 22722
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22719
[MaedaMaeda] p. 1Definition 1.1df-dmd 22691  df-md 22690  mdbr 22704
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22741  mdslj1i 22729  mdslj2i 22730  mdslle1i 22727  mdslle2i 22728  mdslmd1i 22739  mdslmd2i 22740
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22731  mdsl2bi 22733  mdsl2i 22732
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22745
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22742
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22743
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22720
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22725  mdsl3 22726
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22744
[MaedaMaeda] p. 4Theorem 1.14mdcompli 22839
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28200  hlrelat1 28278
[MaedaMaeda] p. 31Lemma 7.5lcvexch 27918
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22746  cvmdi 22734  cvnbtwn4 22699  cvrnbtwn4 28158
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22747
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28219  cvp 22785  cvrp 28294  lcvp 27919
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22809
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22808
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28212  hlexch4N 28270
[MaedaMaeda] p. 34Exercise 7.1atabsi 22811
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28321
[MaedaMaeda] p. 61Definition 15.10psubN 28627  atpsubN 28631  df-pointsN 28380  pointpsubN 28629
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28382  pmap11 28640  pmaple 28639  pmapsub 28646  pmapval 28635
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 28643  pmap1N 28645
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 28648  pmapglb2N 28649  pmapglb2xN 28650  pmapglbx 28647
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 28730
[MaedaMaeda] p. 67Postulate PS1ps-1 28355
[MaedaMaeda] p. 68Lemma 16.2df-padd 28674  paddclN 28720  paddidm 28719
[MaedaMaeda] p. 68Condition PS2ps-2 28356
[MaedaMaeda] p. 68Equation 16.2.1paddass 28716
[MaedaMaeda] p. 69Lemma 16.4ps-1 28355
[MaedaMaeda] p. 69Theorem 16.4ps-2 28356
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14819  lsmmod2 14820  lssats 27891  shatomici 22768  shatomistici 22771  shmodi 21799  shmodsi 21798
[MaedaMaeda] p. 130Remark 29.6dmdmd 22710  mdsymlem7 22819
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22016
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 21902
[MaedaMaeda] p. 139Remarksumdmdii 22825
[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 27381
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27382
[Margaris] p. 79Rule Cexinst01 27087  exinst11 27088
[Margaris] p. 89Theorem 19.219.2 1759  r19.2z 3449
[Margaris] p. 89Theorem 19.319.3 1760  rr19.3v 2846
[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 2618
[Margaris] p. 90Theorem 19.14exnal 1572
[Margaris] p. 90Theorem 19.152albi 26742  albi 1552  ralbi 2641
[Margaris] p. 90Theorem 19.1619.16 1767
[Margaris] p. 90Theorem 19.1719.17 1768
[Margaris] p. 90Theorem 19.182exbi 26744  exbi 1579
[Margaris] p. 90Theorem 19.1919.19 1769
[Margaris] p. 90Theorem 19.202alim 26741  alim 1548  alimd 1705  alimdh 1551  alimdv 2017  ralimdaa 2582  ralimdv 2584  ralimdva 2583  sbcimdv 2982
[Margaris] p. 90Theorem 19.2119.21-2 1772  19.21 1771  19.21bi 1774  19.21t 1770  19.21v 2011  19.21vv 26740  alrimd 1710  alrimdd 1709  alrimdh 1585  alrimdv 2014  alrimi 1706  alrimih 1553  alrimiv 2012  alrimivv 2013  r19.21 2591  r19.21be 2606  r19.21bi 2603  r19.21t 2590  r19.21v 2592  ralrimd 2593  ralrimdv 2594  ralrimdva 2595  ralrimdvv 2599  ralrimdvva 2600  ralrimi 2586  ralrimiv 2587  ralrimiva 2588  ralrimivv 2596  ralrimivva 2597  ralrimivvva 2598  ralrimivw 2589  rexlimi 2622
[Margaris] p. 90Theorem 19.222alimdv 2019  2exim 26743  2eximdv 2020  exim 1573  eximd 1711  eximdh 1586  eximdv 2018  rexim 2609  reximdai 2613  reximdv 2616  reximdv2 2614  reximdva 2617  reximdvai 2615  reximi2 2611
[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 26980  exlimi 1781  exlimih 1782  exlimiv 2023  exlimivv 2025  r19.23 2620  r19.23v 2621  rexlimd 2626  rexlimdv 2628  rexlimdv3a 2631  rexlimdva 2629  rexlimdvaa 2630  rexlimdvv 2635  rexlimdvva 2636  rexlimdvw 2632  rexlimiv 2623  rexlimiva 2624  rexlimivv 2634
[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 2638  r19.26-2a 24099  r19.26-3 2639  r19.26 2637  r19.26m 2640
[Margaris] p. 90Theorem 19.2719.27 1786  19.27v 2027  r19.27av 2643  r19.27z 3458  r19.27zv 3459
[Margaris] p. 90Theorem 19.2819.28 1787  19.28v 2028  19.28vv 26750  r19.28av 2644  r19.28z 3452  r19.28zv 3455  rr19.28v 2847
[Margaris] p. 90Theorem 19.2919.29 1595  19.29r 1596  19.29r2 1597  19.29x 1598  r19.29 2645  r19.29r 2646
[Margaris] p. 90Theorem 19.3019.30 1603  r19.30 2647
[Margaris] p. 90Theorem 19.3119.31 1795  19.31vv 26748
[Margaris] p. 90Theorem 19.3219.32 1794  r19.32v 2648
[Margaris] p. 90Theorem 19.3319.33-2 26746  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 2649
[Margaris] p. 90Theorem 19.3619.36 1788  19.36aiv 2030  19.36i 1789  19.36v 2029  19.36vv 26747  r19.36av 2650  r19.36zv 3460
[Margaris] p. 90Theorem 19.3719.37 1790  19.37aiv 2033  19.37v 2032  19.37vv 26749  r19.37 2651  r19.37av 2652  r19.37zv 3456
[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 2653
[Margaris] p. 90Theorem 19.4119.41 1799  19.41rg 27009  19.41v 2034  19.41vv 2035  19.41vvv 2036  19.41vvvv 2037  r19.41 2654  r19.41v 2655
[Margaris] p. 90Theorem 19.4219.42 1800  19.42v 2038  19.42vv 2040  19.42vvv 2041  r19.42v 2656
[Margaris] p. 90Theorem 19.4319.43 1604  r19.43 2657
[Margaris] p. 90Theorem 19.4419.44 1796  r19.44av 2658
[Margaris] p. 90Theorem 19.4519.45 1797  r19.45av 2659  r19.45zv 3457
[Margaris] p. 110Exercise 2(b)eu1 2134
[Mayet] p. 370Remarkjpi 22680  largei 22677  stri 22667
[Mayet3] p. 9Definition of CH-statesdf-hst 22622  ishst 22624
[Mayet3] p. 10Theoremhstrbi 22676  hstri 22675
[Mayet3] p. 1223Theorem 4.1mayete3i 22155
[Mayet3] p. 1240Theorem 7.1mayetes3i 22157
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22688
[MegPav2000] p. 2345Definition 3.4-1chintcl 21741  chsupcl 21749
[MegPav2000] p. 2345Definition 3.4-2hatomic 22770
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22764
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22791
[MegPav2000] p. 2366Figure 7pl42N 28861
[MegPav2002] p. 362Lemma 2.2latj31 14049  latj32 14047  latjass 14045
[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  sbidd-misc 26878  sbidd 26877
[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 26851
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4ra4sbc 2999  ra4sbca 3000  stdpc4 1896
[Mendelson] p. 69Axiom 5ax-5o 1694  ra5 3005  stdpc5 1773
[Mendelson] p. 81Rule Cexlimiv 2023
[Mendelson] p. 95Axiom 6stdpc6 1821
[Mendelson] p. 95Axiom 7stdpc7 1891
[Mendelson] p. 225Axiom system NBGru 2920
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4161
[Mendelson] p. 231Exercise 4.10(k)inv1 3388
[Mendelson] p. 231Exercise 4.10(l)unv 3389
[Mendelson] p. 231Exercise 4.10(n)dfin3 3315
[Mendelson] p. 231Exercise 4.10(o)df-nul 3363
[Mendelson] p. 231Exercise 4.10(q)dfin4 3316
[Mendelson] p. 231Exercise 4.10(s)ddif 3222
[Mendelson] p. 231Definition of uniondfun3 3314
[Mendelson] p. 235Exercise 4.12(c)univ 4456
[Mendelson] p. 235Exercise 4.12(d)pwv 3726
[Mendelson] p. 235Exercise 4.12(j)pwin 4190
[Mendelson] p. 235Exercise 4.12(k)pwunss 4191
[Mendelson] p. 235Exercise 4.12(l)pwssun 4192
[Mendelson] p. 235Exercise 4.12(n)uniin 3747
[Mendelson] p. 235Exercise 4.12(p)reli 4720
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5099
[Mendelson] p. 244Proposition 4.8(g)epweon 4466
[Mendelson] p. 246Definition of successordf-suc 4291
[Mendelson] p. 250Exercise 4.36oelim2 6479
[Mendelson] p. 254Proposition 4.22(b)xpen 6909
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6831  xpsneng 6832
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6838  xpcomeng 6839
[Mendelson] p. 254Proposition 4.22(e)xpassen 6841
[Mendelson] p. 255Definitionbrsdom 6770
[Mendelson] p. 255Exercise 4.39endisj 6834
[Mendelson] p. 255Exercise 4.41mapprc 6662
[Mendelson] p. 255Exercise 4.43mapsnen 6823
[Mendelson] p. 255Exercise 4.45mapunen 6915
[Mendelson] p. 255Exercise 4.47xpmapen 6914
[Mendelson] p. 255Exercise 4.42(a)map0e 6691
[Mendelson] p. 255Exercise 4.42(b)map1 6824
[Mendelson] p. 257Proposition 4.24(a)undom 6835
[Mendelson] p. 258Exercise 4.56(b)cdaen 7683
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7692  cdacomen 7691
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7696
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7690
[Mendelson] p. 258Definition of cardinal sumcdaval 7680  df-cda 7678
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6416
[Mendelson] p. 266Proposition 4.34(f)oaordex 6442
[Mendelson] p. 275Proposition 4.42(d)entri3 8063
[Mendelson] p. 281Definitiondf-r1 7320
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7369
[Mendelson] p. 287Axiom system MKru 2920
[Mittelstaedt] p. 9Definitiondf-oc 21661
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3298
[Monk1] p. 33Theorem 3.2(i)ssrel 4683
[Monk1] p. 33Theorem 3.2(ii)eqrel 4684
[Monk1] p. 34Definition 3.3df-opab 3975
[Monk1] p. 36Theorem 3.7(i)coi1 5094  coi2 5095
[Monk1] p. 36Theorem 3.8(v)dm0 4799  rn0 4843
[Monk1] p. 36Theorem 3.7(ii)cnvi 4992
[Monk1] p. 37Theorem 3.13(i)relxp 4701
[Monk1] p. 37Theorem 3.13(x)dmxp 4804  rnxp 5013
[Monk1] p. 37Theorem 3.13(ii)xp0 5005  xp0r 4675
[Monk1] p. 38Theorem 3.16(ii)ima0 4937
[Monk1] p. 38Theorem 3.16(viii)imai 4934
[Monk1] p. 39Theorem 3.17imaexg 4933
[Monk1] p. 39Theorem 3.16(xi)imassrn 4932
[Monk1] p. 41Theorem 4.3(i)fnopfv 5512  funfvop 5489
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5418
[Monk1] p. 42Theorem 4.4(iii)fvelima 5426
[Monk1] p. 43Theorem 4.6funun 5153
[Monk1] p. 43Theorem 4.8(iv)dff13 5635  dff13f 5636
[Monk1] p. 46Theorem 4.15(v)funex 5595  funrnex 5599
[Monk1] p. 50Definition 5.4fniunfv 5625
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5062
[Monk1] p. 52Theorem 5.11(viii)ssint 3776
[Monk1] p. 52Definition 5.13 (i)1stval2 5989  df-1st 5974
[Monk1] p. 52Definition 5.13 (ii)2ndval2 5990  df-2nd 5975
[Monk1] p. 112Theorem 15.17(v)ranksn 7410  ranksnb 7383
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7411
[Monk1] p. 112Theorem 15.17(iii)rankun 7412  rankunb 7406
[Monk1] p. 113Theorem 15.18r1val3 7394
[Monk1] p. 113Definition 15.19df-r1 7320  r1val2 7393
[Monk1] p. 117Lemmazorn2 8017  zorn2g 8014
[Monk1] p. 133Theorem 18.11cardom 7503
[Monk1] p. 133Theorem 18.12canth3 8065
[Monk1] p. 133Theorem 18.14carduni 7498
[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 4144
[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 2559
[Munkres] p. 77Example 2distop 16565  indistop 16571  indistopon 16570
[Munkres] p. 77Example 3fctop 16573  fctop2 16574
[Munkres] p. 77Example 4cctop 16575
[Munkres] p. 78Definition of basisdf-bases 16470  isbasis3g 16519
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13218  tgval2 16526
[Munkres] p. 79Remarktgcl 16539
[Munkres] p. 80Lemma 2.1tgval3 16533
[Munkres] p. 80Lemma 2.2tgss2 16557  tgss3 16556
[Munkres] p. 81Lemma 2.3basgen 16558  basgen2 16559
[Munkres] p. 89Definition of subspace topologyresttop 16723
[Munkres] p. 93Theorem 6.1(1)0cld 16607  topcld 16604
[Munkres] p. 93Theorem 6.1(2)iincld 16608
[Munkres] p. 93Theorem 6.1(3)uncld 16610
[Munkres] p. 94Definition of closureclsval 16606
[Munkres] p. 94Definition of interiorntrval 16605
[Munkres] p. 95Theorem 6.5(a)clsndisj 16644  elcls 16642
[Munkres] p. 95Theorem 6.5(b)elcls3 16652
[Munkres] p. 97Theorem 6.6clslp 16711  neindisj 16686
[Munkres] p. 97Corollary 6.7cldlp 16713
[Munkres] p. 97Definition of limit pointislp2 16709  lpval 16703
[Munkres] p. 98Definition of Hausdorff spacedf-haus 16875
[Munkres] p. 102Definition of continuous functiondf-cn 16789  iscn 16797  iscn2 16800
[Munkres] p. 107Theorem 7.2(g)cncnp 16841  cncnp2 16842  cncnpi 16839  df-cnp 16790  iscnp 16799  iscnp2 16801
[Munkres] p. 127Theorem 10.1metcn 17921
[Munkres] p. 128Theorem 10.3metcn4 18568
[NielsenChuang] p. 195Equation 4.73unierri 22514
[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 18469  df-dip 21104  dip0l 21124  ip0l 16372
[Ponnusamy] p. 361Equation 6.45ipval 21106
[Ponnusamy] p. 362Equation I1dipcj 21120
[Ponnusamy] p. 362Equation I3cphdir 18472  dipdir 21250  ipdir 16375  ipdiri 21238
[Ponnusamy] p. 362Equation I4ipidsq 21116
[Ponnusamy] p. 362Equation 6.46ip0i 21233
[Ponnusamy] p. 362Equation 6.47ip1i 21235
[Ponnusamy] p. 362Equation 6.48ip2i 21236
[Ponnusamy] p. 363Equation I2cphass 18478  dipass 21253  ipass 16381  ipassi 21249
[Prugovecki] p. 186Definition of brabraval 22354  df-bra 22260
[Prugovecki] p. 376Equation 8.1df-kb 22261  kbval 22364
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22792
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 28766
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22806  atcvat4i 22807  cvrat3 28320  cvrat4 28321  lsatcvat3 27931
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22692  cvrval 28148  df-cv 22689  df-lcv 27898  lspsncv0 15733
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 28778
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 28779
[Quine] p. 16Definition 2.1df-clab 2240  rabid 2675
[Quine] p. 17Definition 2.1''dfsb7 2079
[Quine] p. 18Definition 2.7df-cleq 2246
[Quine] p. 19Definition 2.9conventions 3  df-v 2729
[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 20670
[Quine] p. 41Theorem 6.5eqcom 2255
[Quine] p. 42Theorem 6.6df-sbc 2922
[Quine] p. 42Theorem 6.7dfsbcq 2923  dfsbcq2 2924
[Quine] p. 43Theorem 6.8vex 2730
[Quine] p. 43Theorem 6.9isset 2731
[Quine] p. 44Theorem 7.3cla4gf 2801  cla4gv 2805  cla4imgf 2799
[Quine] p. 44Theorem 6.11a4sbc 2933  a4sbcd 2934
[Quine] p. 44Theorem 6.12elex 2735
[Quine] p. 44Theorem 6.13elab 2851  elabg 2852  elabgf 2849
[Quine] p. 44Theorem 6.14noel 3366
[Quine] p. 48Theorem 7.2snprc 3599
[Quine] p. 48Definition 7.1df-pr 3551  df-sn 3550
[Quine] p. 49Theorem 7.4snss 3652  snssg 3656
[Quine] p. 49Theorem 7.5prss 3669  prssg 3670
[Quine] p. 49Theorem 7.6prid1 3638  prid1g 3636  prid2 3639  prid2g 3637  snid 3571  snidg 3569
[Quine] p. 51Theorem 7.13prex 4111  snex 4110  snexALT 4090
[Quine] p. 53Theorem 8.2unisn 3743  unisnALT 27392  unisng 3744
[Quine] p. 53Theorem 8.3uniun 3746
[Quine] p. 54Theorem 8.6elssuni 3753
[Quine] p. 54Theorem 8.7uni0 3752
[Quine] p. 56Theorem 8.17uniabio 6153
[Quine] p. 56Definition 8.18dfiota2 6144
[Quine] p. 57Theorem 8.19iotaval 6154
[Quine] p. 57Theorem 8.22iotanul 6158
[Quine] p. 58Theorem 8.23iotaex 6160
[Quine] p. 58Definition 9.1df-op 3553
[Quine] p. 61Theorem 9.5opabid 4164  opelopab 4179  opelopaba 4174  opelopabaf 4181  opelopabf 4182  opelopabg 4176  opelopabga 4171  oprabid 5734
[Quine] p. 64Definition 9.11df-xp 4594
[Quine] p. 64Definition 9.12df-cnv 4596
[Quine] p. 64Definition 9.15df-id 4202
[Quine] p. 65Theorem 10.3fun0 5164
[Quine] p. 65Theorem 10.4funi 5142
[Quine] p. 65Theorem 10.5funsn 5157  funsng 5155
[Quine] p. 65Definition 10.1df-fun 4602
[Quine] p. 65Definition 10.2args 4948  df-fv 4608
[Quine] p. 68Definition 10.11conventions 3  df-fv 4608  fv2 5373
[Quine] p. 124Theorem 17.3nn0opth2 11165  nn0opth2i 11164  nn0opthi 11163  omopthi 6541
[Quine] p. 177Definition 25.2df-rdg 6309
[Quine] p. 232Equation icarddom 8058
[Quine] p. 284Axiom 39(vi)funimaex 5187  funimaexg 5186
[Quine] p. 331Axiom system NFru 2920
[ReedSimon] p. 36Definition (iii)ax-his3 21493
[ReedSimon] p. 63Exercise 4(a)df-dip 21104  polid 21568  polid2i 21566  polidi 21567
[ReedSimon] p. 63Exercise 4(b)df-ph 21221
[ReedSimon] p. 195Remarklnophm 22429  lnophmi 22428
[Retherford] p. 49Exercise 1(i)leopadd 22542
[Retherford] p. 49Exercise 1(ii)leopmul 22544  leopmuli 22543
[Retherford] p. 49Exercise 1(iv)leoptr 22547
[Retherford] p. 49Definition VI.1df-leop 22262  leoppos 22536
[Retherford] p. 49Exercise 1(iii)leoptri 22546
[Retherford] p. 49Definition of operator orderingleop3 22535
[Rudin] p. 164Equation 27efcan 12250
[Rudin] p. 164Equation 30efzval 12256
[Rudin] p. 167Equation 48absefi 12350
[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 4965
[Schechter] p. 51Definition of irreflexivityintirr 4968
[Schechter] p. 51Definition of symmetrycnvsym 4964
[Schechter] p. 51Definition of transitivitycotr 4962
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13361
[Schechter] p. 79Definition of Moore closuredf-mrc 13362
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13363
[Schechter] p. 139Definition AC3dfac9 7646
[Schechter] p. 141Definition (MC)dfac11 26326
[Schechter] p. 149Axiom DC1ax-dc 7956  axdc3 7964
[Schechter] p. 187Definition of ring with unitisrng 15180  isrngo 20875
[Schechter] p. 276Remark 11.6.espan0 21951
[Schechter] p. 276Definition of spandf-span 21718  spanval 21742
[Schechter] p. 428Definition 15.35bastop1 16563
[Schwabhauser] p. 10Axiom A1axcgrrflx 23716
[Schwabhauser] p. 10Axiom A2axcgrtr 23717
[Schwabhauser] p. 10Axiom A3axcgrid 23718
[Schwabhauser] p. 11Axiom A4axsegcon 23729
[Schwabhauser] p. 11Axiom A5ax5seg 23740
[Schwabhauser] p. 11Axiom A6axbtwnid 23741
[Schwabhauser] p. 12Axiom A7axpasch 23743
[Schwabhauser] p. 12Axiom A8axlowdim2 23762
[Schwabhauser] p. 13Axiom A10axeuclid 23765
[Schwabhauser] p. 13Axiom A11axcont 23778
[Schwabhauser] p. 27Theorem 2.1cgrrflx 23784
[Schwabhauser] p. 27Theorem 2.2cgrcomim 23786
[Schwabhauser] p. 27Theorem 2.3cgrtr 23789
[Schwabhauser] p. 27Theorem 2.4cgrcoml 23793
[Schwabhauser] p. 27Theorem 2.5cgrcomr 23794
[Schwabhauser] p. 28Theorem 2.8cgrtriv 23799
[Schwabhauser] p. 28Theorem 2.105segofs 23803
[Schwabhauser] p. 28Definition 2.10df-ofs 23780
[Schwabhauser] p. 29Theorem 2.11cgrextend 23805
[Schwabhauser] p. 29Theorem 2.12segconeq 23807
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 23819  btwntriv2 23809
[Schwabhauser] p. 30Theorem 3.2btwncomim 23810
[Schwabhauser] p. 30Theorem 3.3btwntriv1 23813
[Schwabhauser] p. 30Theorem 3.4btwnswapid 23814
[Schwabhauser] p. 30Theorem 3.5btwnexch2 23820  btwnintr 23816
[Schwabhauser] p. 30Theorem 3.6btwnexch 23822  btwnexch3 23817
[Schwabhauser] p. 30Theorem 3.7btwnouttr 23821
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23761
[Schwabhauser] p. 32Theorem 3.14btwndiff 23824
[Schwabhauser] p. 33Theorem 3.17trisegint 23825
[Schwabhauser] p. 34Theorem 4.2ifscgr 23841
[Schwabhauser] p. 34Definition 4.1df-ifs 23836
[Schwabhauser] p. 35Theorem 4.3cgrsub 23842
[Schwabhauser] p. 35Theorem 4.5cgrxfr 23852
[Schwabhauser] p. 35Definition 4.4df-cgr3 23837
[Schwabhauser] p. 36Theorem 4.6btwnxfr 23853
[Schwabhauser] p. 36Theorem 4.11colinearperm1 23859  colinearperm2 23861  colinearperm3 23860  colinearperm4 23862  colinearperm5 23863
[Schwabhauser] p. 36Definition 4.10df-colinear 23838
[Schwabhauser] p. 37Theorem 4.12colineartriv1 23864
[Schwabhauser] p. 37Theorem 4.13colinearxfr 23872
[Schwabhauser] p. 37Theorem 4.14lineext 23873
[Schwabhauser] p. 37Theorem 4.16fscgr 23877
[Schwabhauser] p. 37Theorem 4.17linecgr 23878
[Schwabhauser] p. 37Definition 4.15df-fs 23839
[Schwabhauser] p. 38Theorem 4.18lineid 23880
[Schwabhauser] p. 38Theorem 4.19idinside 23881
[Schwabhauser] p. 39Theorem 5.1btwnconn1 23898
[Schwabhauser] p. 41Theorem 5.2btwnconn2 23899
[Schwabhauser] p. 41Theorem 5.3btwnconn3 23900
[Schwabhauser] p. 41Theorem 5.5brsegle2 23906
[Schwabhauser] p. 41Definition 5.4df-segle 23904
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 23907
[Schwabhauser] p. 42Theorem 5.7seglerflx 23909
[Schwabhauser] p. 42Theorem 5.8segletr 23911
[Schwabhauser] p. 42Theorem 5.9segleantisym 23912
[Schwabhauser] p. 42Theorem 5.10seglelin 23913
[Schwabhauser] p. 42Theorem 5.11seglemin 23910
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 23915
[Schwabhauser] p. 43Theorem 6.2btwnoutside 23922
[Schwabhauser] p. 43Theorem 6.3broutsideof3 23923
[Schwabhauser] p. 43Theorem 6.4broutsideof 23918  df-outsideof 23917
[Schwabhauser] p. 43Definition 6.1broutsideof2 23919
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 23924
[Schwabhauser] p. 44Theorem 6.6outsideofcom 23925
[Schwabhauser] p. 44Theorem 6.7outsideoftr 23926
[Schwabhauser] p. 44Theorem 6.11outsideofeu 23928
[Schwabhauser] p. 44Definition 6.8df-ray 23935
[Schwabhauser] p. 45Part 2df-lines2 23936
[Schwabhauser] p. 45Theorem 6.13outsidele 23929
[Schwabhauser] p. 45Theorem 6.15lineunray 23944
[Schwabhauser] p. 45Theorem 6.16lineelsb2 23945
[Schwabhauser] p. 45Theorem 6.17linecom 23947  linerflx1 23946  linerflx2 23948
[Schwabhauser] p. 45Theorem 6.18linethru 23950
[Schwabhauser] p. 45Definition 6.14df-line2 23934
[Schwabhauser] p. 46Theorem 6.19linethrueu 23953
[Schwabhauser] p. 46Theorem 6.21lineintmo 23954
[Shapiro] p. 230Theorem 6.5.1dchrhash 20342  dchrsum 20340  dchrsum2 20339  sumdchr 20343
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20344  sum2dchr 20345
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15136  ablfacrp2 15137
[Shapiro], p. 328Equation 9.2.4vmasum 20287
[Shapiro], p. 329Equation 9.2.7logfac2 20288
[Shapiro], p. 329Equation 9.2.9logfacrlim 20295
[Shapiro], p. 331Equation 9.2.13vmadivsum 20463
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20466
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20520  vmalogdivsum2 20519
[Shapiro], p. 375Theorem 9.4.1dirith 20510  dirith2 20509
[Shapiro], p. 375Equation 9.4.3rplogsum 20508  rpvmasum 20507  rpvmasum2 20493
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20468
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20506
[Shapiro], p. 377Lemma 9.4.1dchrisum 20473  dchrisumlem1 20470  dchrisumlem2 20471  dchrisumlem3 20472  dchrisumlema 20469
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20476
[Shapiro], p. 379Equation 9.4.16dchrmusum 20505  dchrmusumlem 20503  dchrvmasumlem 20504
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20475
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20477
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20501  dchrisum0re 20494  dchrisumn0 20502
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20487
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20491
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20492
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20547  pntrsumbnd2 20548  pntrsumo1 20546
[Shapiro], p. 405Equation 10.2.1mudivsum 20511
[Shapiro], p. 406Equation 10.2.6mulogsum 20513
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20515
[Shapiro], p. 407Equation 10.2.8mulog2sum 20518
[Shapiro], p. 418Equation 10.4.6logsqvma 20523
[Shapiro], p. 418Equation 10.4.8logsqvma2 20524
[Shapiro], p. 419Equation 10.4.10selberg 20529
[Shapiro], p. 420Equation 10.4.12selberg2lem 20531
[Shapiro], p. 420Equation 10.4.14selberg2 20532
[Shapiro], p. 422Equation 10.6.7selberg3 20540
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20541
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20538  selberg3lem2 20539
[Shapiro], p. 422Equation 10.4.23selberg4 20542
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20536
[Shapiro], p. 428Equation 10.6.2selbergr 20549
[Shapiro], p. 429Equation 10.6.8selberg3r 20550
[Shapiro], p. 430Equation 10.6.11selberg4r 20551
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20565
[Shapiro], p. 434Equation 10.6.27pntlema 20577  pntlemb 20578  pntlemc 20576  pntlemd 20575  pntlemg 20579
[Shapiro], p. 435Equation 10.6.29pntlema 20577
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20569
[Shapiro], p. 436Lemma 10.6.2pntibnd 20574
[Shapiro], p. 436Equation 10.6.34pntlema 20577
[Shapiro], p. 436Equation 10.6.35pntlem3 20590  pntleml 20592
[Stoll] p. 13Definition of symmetric differencesymdif1 3340
[Stoll] p. 16Exercise 4.40dif 3431  dif0 3430
[Stoll] p. 16Exercise 4.8difdifdir 3447
[Stoll] p. 17Theorem 5.1(5)undifv 3434
[Stoll] p. 19Theorem 5.2(13)undm 3333
[Stoll] p. 19Theorem 5.2(13')indm 3334
[Stoll] p. 20Remarkinvdif 3317
[Stoll] p. 25Definition of ordered tripledf-ot 3554
[Stoll] p. 43Definitionuniiun 3853
[Stoll] p. 44Definitionintiin 3854
[Stoll] p. 45Definitiondf-iin 3806
[Stoll] p. 45Definition indexed uniondf-iun 3805
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3340
[Strang] p. 242Section 6.3expgrowth 26718
[Suppes] p. 22Theorem 2eq0 3376
[Suppes] p. 22Theorem 4eqss 3115  eqssd 3117  eqssi 3116
[Suppes] p. 23Theorem 5ss0 3392  ss0b 3391
[Suppes] p. 23Theorem 6sstr 3108  sstrALT2 27301
[Suppes] p. 23Theorem 7pssirr 3196
[Suppes] p. 23Theorem 8pssn2lp 3197
[Suppes] p. 23Theorem 9psstr 3200
[Suppes] p. 23Theorem 10pssss 3192
[Suppes] p. 25Theorem 12elin 3266  elun 3226
[Suppes] p. 26Theorem 15inidm 3285
[Suppes] p. 26Theorem 16in0 3387
[Suppes] p. 27Theorem 23unidm 3228
[Suppes] p. 27Theorem 24un0 3386
[Suppes] p. 27Theorem 25ssun1 3248
[Suppes] p. 27Theorem 26ssequn1 3255
[Suppes] p. 27Theorem 27unss 3259
[Suppes] p. 27Theorem 28indir 3324
[Suppes] p. 27Theorem 29undir 3325
[Suppes] p. 28Theorem 32difid 3428  difidALT 3429
[Suppes] p. 29Theorem 33difin 3313
[Suppes] p. 29Theorem 34indif 3318
[Suppes] p. 29Theorem 35undif1 3435
[Suppes] p. 29Theorem 36difun2 3439
[Suppes] p. 29Theorem 37difin0 3433
[Suppes] p. 29Theorem 38disjdif 3432
[Suppes] p. 29Theorem 39difundi 3328
[Suppes] p. 29Theorem 40difindi 3330
[Suppes] p. 30Theorem 41nalset 4048
[Suppes] p. 39Theorem 61uniss 3748
[Suppes] p. 39Theorem 65uniop 4162
[Suppes] p. 41Theorem 70intsn 3796
[Suppes] p. 42Theorem 71intpr 3793  intprg 3794
[Suppes] p. 42Theorem 73op1stb 4460
[Suppes] p. 42Theorem 78intun 3792
[Suppes] p. 44Definition 15(a)dfiun2 3835  dfiun2g 3833
[Suppes] p. 44Definition 15(b)dfiin2 3836
[Suppes] p. 47Theorem 86elpw 3536  elpw2 4064  elpw2g 4063  elpwg 3537  elpwgdedVD 27383
[Suppes] p. 47Theorem 87pwid 3542
[Suppes] p. 47Theorem 89pw0 3662
[Suppes] p. 48Theorem 90pwpw0 3663
[Suppes] p. 52Theorem 101xpss12 4699
[Suppes] p. 52Theorem 102xpindi 4726  xpindir 4727
[Suppes] p. 52Theorem 103xpundi 4648  xpundir 4649
[Suppes] p. 54Theorem 105elirrv 7195
[Suppes] p. 58Theorem 2relss 4682
[Suppes] p. 59Theorem 4eldm 4783  eldm2 4784  eldm2g 4782  eldmg 4781
[Suppes] p. 59Definition 3df-dm 4598
[Suppes] p. 60Theorem 6dmin 4793
[Suppes] p. 60Theorem 8rnun 4996
[Suppes] p. 60Theorem 9rnin 4997
[Suppes] p. 60Definition 4dfrn2 4775
[Suppes] p. 61Theorem 11brcnv 4771  brcnvg 4769
[Suppes] p. 62Equation 5elcnv 4765  elcnv2 4766
[Suppes] p. 62Theorem 12relcnv 4958
[Suppes] p. 62Theorem 15cnvin 4995
[Suppes] p. 62Theorem 16cnvun 4993
[Suppes] p. 63Theorem 20co02 5092
[Suppes] p. 63Theorem 21dmcoss 4851
[Suppes] p. 63Definition 7df-co 4597
[Suppes] p. 64Theorem 26cnvco 4772
[Suppes] p. 64Theorem 27coass 5097
[Suppes] p. 65Theorem 31resundi 4876
[Suppes] p. 65Theorem 34elima 4924  elima2 4925  elima3 4926  elimag 4923
[Suppes] p. 65Theorem 35imaundi 5000
[Suppes] p. 66Theorem 40dminss 5002
[Suppes] p. 66Theorem 41imainss 5003
[Suppes] p. 67Exercise 11cnvxp 5004
[Suppes] p. 81Definition 34dfec2 6549
[Suppes] p. 82Theorem 72elec 6585  elecg 6584
[Suppes] p. 82Theorem 73erth 6590  erth2 6591
[Suppes] p. 83Theorem 74erdisj 6593
[Suppes] p. 89Theorem 96map0b 6692
[Suppes] p. 89Theorem 97map0 6694  map0g 6693
[Suppes] p. 89Theorem 98mapsn 6695
[Suppes] p. 89Theorem 99mapss 6696
[Suppes] p. 91Definition 12(ii)alephsuc 7579
[Suppes] p. 91Definition 12(iii)alephlim 7578
[Suppes] p. 92Theorem 1enref 6780  enrefg 6779
[Suppes] p. 92Theorem 2ensym 6796  ensymb 6795  ensymi 6797
[Suppes] p. 92Theorem 3entr 6798
[Suppes] p. 92Theorem 4unen 6828
[Suppes] p. 94Theorem 15endom 6774
[Suppes] p. 94Theorem 16ssdomg 6793
[Suppes] p. 94Theorem 17domtr 6799
[Suppes] p. 95Theorem 18sbth 6866
[Suppes] p. 97Theorem 23canth2 6899  canth2g 6900
[Suppes] p. 97Definition 3brsdom2 6870  df-sdom 6752  dfsdom2 6869
[Suppes] p. 97Theorem 21(i)sdomirr 6883
[Suppes] p. 97Theorem 22(i)domnsym 6872
[Suppes] p. 97Theorem 21(ii)sdomnsym 6871
[Suppes] p. 97Theorem 22(ii)domsdomtr 6881
[Suppes] p. 97Theorem 22(iv)brdom2 6777
[Suppes] p. 97Theorem 21(iii)sdomtr 6884
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6879
[Suppes] p. 98Exercise 4fundmen 6819  fundmeng 6820
[Suppes] p. 98Exercise 6xpdom3 6845
[Suppes] p. 98Exercise 11sdomentr 6880
[Suppes] p. 104Theorem 37fofi 7027
[Suppes] p. 104Theorem 38pwfi 7035
[Suppes] p. 105Theorem 40pwfi 7035
[Suppes] p. 111Axiom for cardinal numberscarden 8055
[Suppes] p. 130Definition 3df-tr 4011
[Suppes] p. 132Theorem 9ssonuni 4469
[Suppes] p. 134Definition 6df-suc 4291
[Suppes] p. 136Theorem Schema 22findes 4577  finds 4573  finds1 4576  finds2 4575
[Suppes] p. 151Theorem 42isfinite 7237  isfinite2 7000  isfiniteg 7002  unbnn 6998
[Suppes] p. 162Definition 5df-ltnq 8422  df-ltpq 8414
[Suppes] p. 197Theorem Schema 4tfindes 4544  tfinds 4541  tfinds2 4545
[Suppes] p. 209Theorem 18oaord1 6435
[Suppes] p. 209Theorem 21oaword2 6437
[Suppes] p. 211Theorem 25oaass 6445
[Suppes] p. 225Definition 8iscard2 7493
[Suppes] p. 227Theorem 56ondomon 8067
[Suppes] p. 228Theorem 59harcard 7495
[Suppes] p. 228Definition 12(i)aleph0 7577
[Suppes] p. 228Theorem Schema 61onintss 4335
[Suppes] p. 228Theorem Schema 62onminesb 4480  onminsb 4481
[Suppes] p. 229Theorem 64alephval2 8074
[Suppes] p. 229Theorem 65alephcard 7581
[Suppes] p. 229Theorem 66alephord2i 7588
[Suppes] p. 229Theorem 67alephnbtwn 7582
[Suppes] p. 229Definition 12df-aleph 7457
[Suppes] p. 242Theorem 6weth 8006
[Suppes] p. 242Theorem 8entric 8061
[Suppes] p. 242Theorem 9carden 8055
[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 5714
[TakeutiZaring] p. 14Proposition 4.14ru 2920
[TakeutiZaring] p. 15Axiom 2zfpair 4106
[TakeutiZaring] p. 15Exercise 1elpr 3562  elpr2 3563  elprg 3561
[TakeutiZaring] p. 15Exercise 2elsn 3559  elsnc 3567  elsnc2 3573  elsnc2g 3572  elsncg 3566
[TakeutiZaring] p. 15Exercise 3elop 4132
[TakeutiZaring] p. 15Exercise 4sneq 3555  sneqr 3680
[TakeutiZaring] p. 15Definition 5.1dfpr2 3560  dfsn2 3558
[TakeutiZaring] p. 16Axiom 3uniex 4407
[TakeutiZaring] p. 16Exercise 6opth 4138
[TakeutiZaring] p. 16Exercise 7opex 4130
[TakeutiZaring] p. 16Exercise 8rext 4116
[TakeutiZaring] p. 16Corollary 5.8unex 4409  unexg 4412
[TakeutiZaring] p. 16Definition 5.3dftp2 3583
[TakeutiZaring] p. 16Definition 5.5df-uni 3728
[TakeutiZaring] p. 16Definition 5.6df-in 3085  df-un 3083
[TakeutiZaring] p. 16Proposition 5.7unipr 3741  uniprg 3742
[TakeutiZaring] p. 17Axiom 4pwex 4087  pwexg 4088
[TakeutiZaring] p. 17Exercise 1eltp 3582
[TakeutiZaring] p. 17Exercise 5elsuc 4354  elsucg 4352  sstr2 3107
[TakeutiZaring] p. 17Exercise 6uncom 3229
[TakeutiZaring] p. 17Exercise 7incom 3269
[TakeutiZaring] p. 17Exercise 8unass 3242
[TakeutiZaring] p. 17Exercise 9inass 3286
[TakeutiZaring] p. 17Exercise 10indi 3322
[TakeutiZaring] p. 17Exercise 11undi 3323
[TakeutiZaring] p. 17Definition 5.9df-pss 3091  dfss2 3092
[TakeutiZaring] p. 17Definition 5.10df-pw 3532
[TakeutiZaring] p. 18Exercise 7unss2 3256
[TakeutiZaring] p. 18Exercise 9df-ss 3089  sseqin2 3295
[TakeutiZaring] p. 18Exercise 10ssid 3118
[TakeutiZaring] p. 18Exercise 12inss1 3296  inss2 3297
[TakeutiZaring] p. 18Exercise 13nss 3157
[TakeutiZaring] p. 18Exercise 15unieq 3736
[TakeutiZaring] p. 18Exercise 18sspwb 4117  sspwimp 27384  sspwimpALT 27391  sspwimpALT2 27395  sspwimpcf 27386
[TakeutiZaring] p. 18Exercise 19pweqb 4124
[TakeutiZaring] p. 19Axiom 5ax-rep 4028
[TakeutiZaring] p. 20Definitiondf-rab 2516
[TakeutiZaring] p. 20Corollary 5.160ex 4047
[TakeutiZaring] p. 20Definition 5.12df-dif 3081
[TakeutiZaring] p. 20Definition 5.14dfnul2 3364
[TakeutiZaring] p. 20Proposition 5.15difid 3428  difidALT 3429
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3371  n0f 3370  neq0 3372
[TakeutiZaring] p. 21Axiom 6zfreg 7193
[TakeutiZaring] p. 21Axiom 6'zfregs 7298
[TakeutiZaring] p. 21Theorem 5.22setind 7303
[TakeutiZaring] p. 21Definition 5.20df-v 2729
[TakeutiZaring] p. 21Proposition 5.21vprc 4049
[TakeutiZaring] p. 22Exercise 10ss 3390
[TakeutiZaring] p. 22Exercise 3ssex 4055  ssexg 4057
[TakeutiZaring] p. 22Exercise 4inex1 4052
[TakeutiZaring] p. 22Exercise 5ruv 7198
[TakeutiZaring] p. 22Exercise 6elirr 7196
[TakeutiZaring] p. 22Exercise 7ssdif0 3420
[TakeutiZaring] p. 22Exercise 11difdif 3219
[TakeutiZaring] p. 22Exercise 13undif3 3336  undif3VD 27348
[TakeutiZaring] p. 22Exercise 14difss 3220
[TakeutiZaring] p. 22Exercise 15sscon 3224
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2513
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2514
[TakeutiZaring] p. 23Proposition 6.2xpex 4708  xpexg 4707  xpexgALT 5922
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4595
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5169
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5302  fun11 5172
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5125  svrelfun 5170
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4774
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4776
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4600
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4601
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4597
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5035  dfrel2 5031
[TakeutiZaring] p. 25Exercise 3xpss 4700
[TakeutiZaring] p. 25Exercise 5relun 4709
[TakeutiZaring] p. 25Exercise 6reluni 4715
[TakeutiZaring] p. 25Exercise 9inxp 4725
[TakeutiZaring] p. 25Exercise 12relres 4890
[TakeutiZaring] p. 25Exercise 13opelres 4867  opelresg 4869
[TakeutiZaring] p. 25Exercise 14dmres 4883
[TakeutiZaring] p. 25Exercise 15resss 4886
[TakeutiZaring] p. 25Exercise 17resabs1 4891
[TakeutiZaring] p. 25Exercise 18funres 5150
[TakeutiZaring] p. 25Exercise 24relco 5077
[TakeutiZaring] p. 25Exercise 29funco 5149
[TakeutiZaring] p. 25Exercise 30f1co 5303
[TakeutiZaring] p. 26Definition 6.10eu2 2138
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 4608  fv3 5393
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5115  cnvexg 5114
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4848  dmexg 4846
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4849  rnexg 4847
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 26825
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 26826
[TakeutiZaring] p. 27Corollary 6.13fvex 5391
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5396  tz6.12 5397  tz6.12c 5400
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5399  tz6.12i 5401
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4603
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4604
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4606  wfo 4590
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4605  wf1 4589
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4607  wf1o 4591
[TakeutiZaring] p. 28Exercise 4eqfnfv 5474  eqfnfv2 5475  eqfnfv2f 5478
[TakeutiZaring] p. 28Exercise 5fvco 5447
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5593  fnexALT 5594
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5589  resfunexgALT 5590
[TakeutiZaring] p. 29Exercise 9funimaex 5187  funimaexg 5186
[TakeutiZaring] p. 29Definition 6.18df-br 3921
[TakeutiZaring] p. 30Definition 6.21dffr2 4251  dffr3 4952  eliniseg 4949  iniseg 4951
[TakeutiZaring] p. 30Definition 6.22df-eprel 4198
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4264  fr3nr 4462  frirr 4263
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4245
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4464
[TakeutiZaring] p. 31Exercise 1frss 4253
[TakeutiZaring] p. 31Exercise 4wess 4273
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23373  tz6.26i 23374  wefrc 4280  wereu2 4283
[TakeutiZaring] p. 32Theorem 6.27wfi 23375  wfii 23376
[TakeutiZaring] p. 32Definition 6.28df-isom 4609
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5678
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5679
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5685
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5686
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5687
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5691
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5698
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5700
[TakeutiZaring] p. 35Notationwtr 4010
[TakeutiZaring] p. 35Theorem 7.2trelpss 26827  tz7.2 4270
[TakeutiZaring] p. 35Definition 7.1dftr3 4014
[TakeutiZaring] p. 36Proposition 7.4ordwe 4298
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4306
[TakeutiZaring] p. 36Proposition 7.6ordelord 4307  ordelordALT 26994  ordelordALTVD 27333
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4313  ordelssne 4312
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4311
[TakeutiZaring] p. 37Proposition 7.9ordin 4315
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4471
[TakeutiZaring] p. 38Corollary 7.15ordsson 4472
[TakeutiZaring] p. 38Definition 7.11df-on 4289
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4317
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27007  ordon 4465
[TakeutiZaring] p. 38Proposition 7.13onprc 4467
[TakeutiZaring] p. 39Theorem 7.17tfi 4535
[TakeutiZaring] p. 40Exercise 3ontr2 4332
[TakeutiZaring] p. 40Exercise 7dftr2 4012
[TakeutiZaring] p. 40Exercise 9onssmin 4479
[TakeutiZaring] p. 40Exercise 11unon 4513
[TakeutiZaring] p. 40Exercise 12ordun 4385
[TakeutiZaring] p. 40Exercise 14ordequn 4384
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4468
[TakeutiZaring] p. 40Proposition 7.20elssuni 3753
[TakeutiZaring] p. 41Definition 7.22df-suc 4291
[TakeutiZaring] p. 41Proposition 7.23sssucid 4362  sucidg 4363
[TakeutiZaring] p. 41Proposition 7.24suceloni 4495
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4377  ordnbtwn 4376
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4510
[TakeutiZaring] p. 42Exercise 1df-lim 4290
[TakeutiZaring] p. 42Exercise 4omssnlim 4561
[TakeutiZaring] p. 42Exercise 7ssnlim 4565
[TakeutiZaring] p. 42Exercise 8onsucssi 4523  ordelsuc 4502
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4504
[TakeutiZaring] p. 42Definition 7.27nlimon 4533
[TakeutiZaring] p. 42Definition 7.28dfom2 4549
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4566
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4567
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4568
[TakeutiZaring] p. 43Remarkomon 4558
[TakeutiZaring] p. 43Axiom 7inf3 7220  omex 7228
[TakeutiZaring] p. 43Theorem 7.32ordom 4556
[TakeutiZaring] p. 43Corollary 7.31find 4572
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4569
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4570
[TakeutiZaring] p. 44Exercise 1limomss 4552
[TakeutiZaring] p. 44Exercise 2int0 3774  trint0 4027
[TakeutiZaring] p. 44Exercise 4intss1 3775
[TakeutiZaring] p. 44Exercise 5intex 4065
[TakeutiZaring] p. 44Exercise 6oninton 4482
[TakeutiZaring] p. 44Exercise 11ordintdif 4334
[TakeutiZaring] p. 44Definition 7.35df-int 3761
[TakeutiZaring] p. 44Proposition 7.34noinfep 7244
[TakeutiZaring] p. 45Exercise 4onint 4477
[TakeutiZaring] p. 47Lemma 1tfrlem1 6277
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6299
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6300
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6301
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6305  tz7.44-2 6306  tz7.44-3 6307
[TakeutiZaring] p. 50Exercise 1smogt 6270
[TakeutiZaring] p. 50Exercise 3smoiso 6265
[TakeutiZaring] p. 50Definition 7.46df-smo 6249
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6343  tz7.49c 6344
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6341
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6340
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6342
[TakeutiZaring] p. 53Proposition 7.532eu5 2197
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7523
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7524
[TakeutiZaring] p. 56Definition 8.1oalim 6417  oasuc 6409
[TakeutiZaring] p. 57Remarktfindsg 4542
[TakeutiZaring] p. 57Proposition 8.2oacl 6420
[TakeutiZaring] p. 57Proposition 8.3oa0 6401  oa0r 6423
[TakeutiZaring] p. 57Proposition 8.16omcl 6421
[TakeutiZaring] p. 58Corollary 8.5oacan 6432
[TakeutiZaring] p. 58Proposition 8.4nnaord 6503  nnaordi 6502  oaord 6431  oaordi 6430
[TakeutiZaring] p. 59Proposition 8.6iunss2 3845  uniss2 3756
[TakeutiZaring] p. 59Proposition 8.7oawordri 6434
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6439  oawordex 6441
[TakeutiZaring] p. 59Proposition 8.9nnacl 6495
[TakeutiZaring] p. 59Proposition 8.10oaabs 6528
[TakeutiZaring] p. 60Remarkoancom 7236
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6444
[TakeutiZaring] p. 62Exercise 1nnarcl 6500
[TakeutiZaring] p. 62Exercise 5oaword1 6436
[TakeutiZaring] p. 62Definition 8.15om0 6402  om0x 6404  omlim 6418  omsuc 6411
[TakeutiZaring] p. 63Proposition 8.17nnecl 6497  nnmcl 6496
[TakeutiZaring] p. 63Proposition 8.19nnmord 6516  nnmordi 6515  omord 6452  omordi 6450
[TakeutiZaring] p. 63Proposition 8.20omcan 6453
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6520  omwordri 6456
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6424
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6426  om1r 6427
[TakeutiZaring] p. 64Proposition 8.22om00 6459
[TakeutiZaring] p. 64Proposition 8.23omordlim 6461
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6462
[TakeutiZaring] p. 64Proposition 8.25odi 6463
[TakeutiZaring] p. 65Theorem 8.26omass 6464
[TakeutiZaring] p. 67Definition 8.30nnesuc 6492  oe0 6407  oelim 6419  oesuc 6412  onesuc 6415
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6405
[TakeutiZaring] p. 67Proposition 8.32oen0 6470
[TakeutiZaring] p. 67Proposition 8.33oeordi 6471
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6406
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6429
[TakeutiZaring] p. 68Corollary 8.34oeord 6472
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6478
[TakeutiZaring] p. 68Proposition 8.35oewordri 6476
[TakeutiZaring] p. 68Proposition 8.37oeworde 6477
[TakeutiZaring] p. 69Proposition 8.41oeoa 6481
[TakeutiZaring] p. 70Proposition 8.42oeoe 6483
[TakeutiZaring] p. 73Theorem 9.1trcl 7294  tz9.1 7295
[TakeutiZaring] p. 76Definition 9.9df-r1 7320  r10 7324  r1lim 7328  r1limg 7327  r1suc 7326  r1sucg 7325
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7336  r1ord2 7337  r1ordg 7334
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7346
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7371  tz9.13 7347  tz9.13g 7348
[TakeutiZaring] p. 79Definition 9.14df-rank 7321  rankval 7372  rankvalb 7353  rankvalg 7373
[TakeutiZaring] p. 79Proposition 9.16rankel 7395  rankelb 7380
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7409  rankval3 7396  rankval3b 7382
[TakeutiZaring] p. 79Proposition 9.18rankonid 7385
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7351
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7390  rankr1c 7377  rankr1g 7388
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7391
[TakeutiZaring] p. 80Exercise 1rankss 7405  rankssb 7404
[TakeutiZaring] p. 80Exercise 2unbndrank 7398
[TakeutiZaring] p. 80Proposition 9.19bndrank 7397
[TakeutiZaring] p. 83Axiom of Choiceac4 7986  dfac3 7632
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7541  numth 7983  numth2 7982
[TakeutiZaring] p. 85Definition 10.4cardval 8052
[TakeutiZaring] p. 85Proposition 10.5cardid 8053  cardid2 7470
[TakeutiZaring] p. 85Proposition 10.9oncard 7477
[TakeutiZaring] p. 85Proposition 10.10carden 8055
[TakeutiZaring] p. 85Proposition 10.11cardidm 7476
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7461
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7482
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7474
[TakeutiZaring] p. 87Proposition 10.15pwen 6919
[TakeutiZaring] p. 88Exercise 1en0 6809
[TakeutiZaring] p. 88Exercise 7infensuc 6924
[TakeutiZaring] p. 89Exercise 10omxpen 6849
[TakeutiZaring] p. 90Corollary 10.23cardnn 7480
[TakeutiZaring] p. 90Definition 10.27alephiso 7609
[TakeutiZaring] p. 90Proposition 10.20nneneq 6929
[TakeutiZaring] p. 90Proposition 10.22onomeneq 6935
[TakeutiZaring] p. 90Proposition 10.26alephprc 7610
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6934
[TakeutiZaring] p. 91Exercise 2alephle 7599
[TakeutiZaring] p. 91Exercise 3aleph0 7577
[TakeutiZaring] p. 91Exercise 4cardlim 7489
[TakeutiZaring] p. 91Exercise 7infpss 7727
[TakeutiZaring] p. 91Exercise 8infcntss 7015
[TakeutiZaring] p. 91Definition 10.29df-fin 6753  isfi 6771
[TakeutiZaring] p. 92Proposition 10.32onfin 6936
[TakeutiZaring] p. 92Proposition 10.34imadomg 8043
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6842
[TakeutiZaring] p. 93Proposition 10.35fodomb 8035
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7699  unxpdom 6955
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7491  cardsdomelir 7490
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 6957
[TakeutiZaring] p. 94Proposition 10.39infxpen 7526
[TakeutiZaring] p. 95Definition 10.42df-map 6660
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8066  infxpidm2 7528
[TakeutiZaring] p. 95Proposition 10.41infcda 7718  infxp 7725  infxpg 24260
[TakeutiZaring] p. 96Proposition 10.44pw2en 6854  pw2f1o 6852
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6912
[TakeutiZaring] p. 97Theorem 10.46ac6s3 7998
[TakeutiZaring] p. 98Theorem 10.46ac6c5 7993  ac6s5 8002
[TakeutiZaring] p. 98Theorem 10.47unidom 8049
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8050  uniimadomf 8051
[TakeutiZaring] p. 100Definition 11.1cfcof 7784
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7779
[TakeutiZaring] p. 102Exercise 1cfle 7764
[TakeutiZaring] p. 102Exercise 2cf0 7761
[TakeutiZaring] p. 102Exercise 3cfsuc 7767
[TakeutiZaring] p. 102Exercise 4cfom 7774
[TakeutiZaring] p. 102Proposition 11.9coftr 7783
[TakeutiZaring] p. 103Theorem 11.15alephreg 8084
[TakeutiZaring] p. 103Proposition 11.11cardcf 7762
[TakeutiZaring] p. 103Proposition 11.13alephsing 7786
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7608
[TakeutiZaring] p. 104Proposition 11.16carduniima 7607
[TakeutiZaring] p. 104Proposition 11.18alephfp 7619  alephfp2 7620
[TakeutiZaring] p. 106Theorem 11.20gchina 8201
[TakeutiZaring] p. 106Theorem 11.21mappwen 7623
[TakeutiZaring] p. 107Theorem 11.26konigth 8071
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8085
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8086
[Tarski] p. 67Axiom B5ax-4 1692
[Tarski] p. 68Lemma 6avril1 20666  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 27847
[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 12395
[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 27393
[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 24094
[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 24087
[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 26719
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26720
[WhiteheadRussell] p. 147Theorem *10.2219.26 1592
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26721
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26722
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26723
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1617
[WhiteheadRussell] p. 151Theorem *10.301albitr 26724
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26725
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26726
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26727
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26728
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26730
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26731
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26732
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26729
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26735
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2075
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26736
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26737
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1610
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26738
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26739
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26740
[WhiteheadRussell] p. 162Theorem *11.322alim 26741
[WhiteheadRussell] p. 162Theorem *11.332albi 26742
[WhiteheadRussell] p. 162Theorem *11.342exim 26743
[WhiteheadRussell] p. 162Theorem *11.36a4sbce-2 26745
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26744
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1609
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26747
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26748
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26746
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1571
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26749
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26750
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1578
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26751
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2024  pm11.53g 24129
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26752
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26757
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26753
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26754
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26755
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26756
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26761
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26758
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26759
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26760
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26762
[WhiteheadRussell] p. 175Definition *14.02df-eu 2118
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 26774  pm13.13b 26775
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 26776
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2484
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2485
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2845
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 26782
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 26783
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 26777
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27011  pm13.193 26778
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 26779
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 26780
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 26781
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 26788
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 26787
[WhiteheadRussell] p. 184Definition *14.01iotasbc 26786
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2973
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 26789  pm14.122b 26790  pm14.122c 26791
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 26792  pm14.123b 26793  pm14.123c 26794
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 26796
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 26795
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 26797
[WhiteheadRussell] p. 190Theorem *14.22iota4 6161
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 26798
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6162
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 26799
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 26801
[WhiteheadRussell] p. 192Theorem *14.26eupick 2176  eupickbi 2179  sbaniota 26802
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 26800
[WhiteheadRussell] p. 192Theorem *14.271eubi 26803
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 26804
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 4608
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7517  pm54.43lem 7516
[Young] p. 141Definition of operator orderingleop2 22534
[Young] p. 142Example 12.2(i)0leop 22540  idleop 22541
[vandenDries] p. 42Lemma 61irrapx1 26079
[vandenDries] p. 43Theorem 62pellex 26086  pellexlem1 26080

This page was last updated on 1-Mar-2017.
Copyright terms: Public domain