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 13431
[Adamek] p. 29Proposition 3.14(1)invinv 13445
[Adamek] p. 29Proposition 3.14(2)invco 13446  isoco 13447
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25156
[AitkenIBCG] p. 3Definition 2df-angtrg 25152  df-trcng 25155
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25028  df-ig2 25027
[AitkenIBG] p. 2Definition 4df-li 25043
[AitkenIBG] p. 3Definition 5df-col 25057
[AitkenIBG] p. 3Definition 6df-con2 25062
[AitkenIBG] p. 3Proposition 4isconcl5a 25067  isconcl5ab 25068  isconcl6a 25069  isconcl6ab 25070
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25075
[AitkenIBG] p. 4Exercise 5tpne 25041
[AitkenIBG] p. 4Definition 8df-seg2 25097
[AitkenIBG] p. 4Definition 10df-sside 25129
[AitkenIBG] p. 4Definition 11df-ray2 25118
[AitkenIBG] p. 10Definition 17df-angle 25124
[AitkenIBG] p. 15Definition 23df-triangle 25126
[AitkenIBG] p. 15Definition 24df-cnvx 25145
[AitkenNG] p. 2Definition 1df-slices 25159
[AitkenNG] p. 2Definition 2df-Cut 25161
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25163
[AitkenNG] p. 4Definition 5df-crcl 25165
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 17889  df-nmoo 20948
[AkhiezerGlazman] p. 64Theoremhmopidmch 22358  hmopidmchi 22356
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22406  pjcmul2i 22407
[AkhiezerGlazman] p. 72Theoremcnvunop 22123  unoplin 22125
[AkhiezerGlazman] p. 72Equation 2unopadj 22124  unopadj2 22143
[AkhiezerGlazman] p. 73Theoremelunop2 22218  lnopunii 22217
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22291
[Apostol] p. 18Theorem I.1addcan 8849  addcan2d 8869  addcan2i 8859  addcand 8868  addcani 8858
[Apostol] p. 18Theorem I.2negeu 8891
[Apostol] p. 18Theorem I.3negsub 8944  negsubd 9008  negsubi 8973
[Apostol] p. 18Theorem I.4negneg 8946  negnegd 8997  negnegi 8965
[Apostol] p. 18Theorem I.5subdi 9051  subdid 9072  subdii 9065  subdir 9052  subdird 9073  subdiri 9066
[Apostol] p. 18Theorem I.6mul01 8844  mul01d 8864  mul01i 8855  mul02 8843  mul02d 8863  mul02i 8854
[Apostol] p. 18Theorem I.7mulcan 9239  mulcan2d 9238  mulcand 9237  mulcani 9241
[Apostol] p. 18Theorem I.8receu 9247
[Apostol] p. 18Theorem I.9divrec 9272  divrecd 9369  divreci 9335  divreczi 9328
[Apostol] p. 18Theorem I.10recrec 9289  recreci 9322
[Apostol] p. 18Theorem I.11mul0or 9242  mul0ord 9252  mul0ori 9250
[Apostol] p. 18Theorem I.12mul2neg 9057  mul2negd 9071  mul2negi 9064  mulneg1 9054  mulneg1d 9069  mulneg1i 9062
[Apostol] p. 18Theorem I.13divadddiv 9307  divadddivd 9406  divadddivi 9352
[Apostol] p. 18Theorem I.14divmuldiv 9292  divmuldivd 9403  divmuldivi 9350
[Apostol] p. 18Theorem I.15divdivdiv 9293  divdivdivd 9409  divdivdivi 9353
[Apostol] p. 20Axiom 7rpaddcl 10192  rpaddcld 10223  rpmulcl 10193  rpmulcld 10224
[Apostol] p. 20Axiom 8rpneg 10201
[Apostol] p. 20Axiom 90nrp 10202
[Apostol] p. 20Theorem I.17lttri 8798
[Apostol] p. 20Theorem I.18ltadd1d 9201  ltadd1dd 9219  ltadd1i 9164
[Apostol] p. 20Theorem I.19ltmul1 9426  ltmul1a 9425  ltmul1i 9495  ltmul1ii 9505  ltmul2 9427  ltmul2d 10246  ltmul2dd 10260  ltmul2i 9498
[Apostol] p. 20Theorem I.20msqgt0 9131  msqgt0d 9176  msqgt0i 9147
[Apostol] p. 20Theorem I.210lt1 9133
[Apostol] p. 20Theorem I.23lt0neg1 9117  lt0neg1d 9178  ltneg 9111  ltnegd 9186  ltnegi 9154
[Apostol] p. 20Theorem I.25lt2add 9096  lt2addd 9230  lt2addi 9172
[Apostol] p. 20Definition of positive numbersdf-rp 10173
[Apostol] p. 21Exercise 4recgt0 9420  recgt0d 9511  recgt0i 9481  recgt0ii 9482
[Apostol] p. 22Definition of integersdf-z 9843
[Apostol] p. 22Definition of positive integersdfnn3 9580
[Apostol] p. 22Definition of rationalsdf-q 10135
[Apostol] p. 24Theorem I.26supeu 7063
[Apostol] p. 26Theorem I.28nnunb 9779
[Apostol] p. 26Theorem I.29arch 9780
[Apostol] p. 28Exercise 2btwnz 9932
[Apostol] p. 28Exercise 3nnrecl 9781
[Apostol] p. 28Exercise 4rebtwnz 10133
[Apostol] p. 28Exercise 5zbtwnre 10132
[Apostol] p. 28Exercise 6qbtwnre 10343
[Apostol] p. 28Exercise 10(a)zneo 9912
[Apostol] p. 29Theorem I.35msqsqrd 11733  resqrth 11554  sqrth 11659  sqrthi 11665  sqsqrd 11732
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9569
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10102
[Apostol] p. 361Remarkcrreczi 11040
[Apostol] p. 363Remarkabsgt0i 11693
[Apostol] p. 363Exampleabssubd 11746  abssubi 11697
[Baer] p. 40Property (b)mapdord 30258
[Baer] p. 40Property (c)mapd11 30259
[Baer] p. 40Property (e)mapdin 30282  mapdlsm 30284
[Baer] p. 40Property (f)mapd0 30285
[Baer] p. 40Definition of projectivitydf-mapd 30245  mapd1o 30268
[Baer] p. 41Property (g)mapdat 30287
[Baer] p. 44Part (1)mapdpg 30326
[Baer] p. 45Part (2)hdmap1eq 30422  mapdheq 30348  mapdheq2 30349  mapdheq2biN 30350
[Baer] p. 45Part (3)baerlem3 30333
[Baer] p. 46Part (4)mapdheq4 30352  mapdheq4lem 30351
[Baer] p. 46Part (5)baerlem5a 30334  baerlem5abmN 30338  baerlem5amN 30336  baerlem5b 30335  baerlem5bmN 30337
[Baer] p. 47Part (6)hdmap1l6 30442  hdmap1l6a 30430  hdmap1l6e 30435  hdmap1l6f 30436  hdmap1l6g 30437  hdmap1l6lem1 30428  hdmap1l6lem2 30429  hdmap1p6N 30443  mapdh6N 30367  mapdh6aN 30355  mapdh6eN 30360  mapdh6fN 30361  mapdh6gN 30362  mapdh6lem1N 30353  mapdh6lem2N 30354
[Baer] p. 48Part 9hdmapval 30451
[Baer] p. 48Part 10hdmap10 30463
[Baer] p. 48Part 11hdmapadd 30466
[Baer] p. 48Part (6)hdmap1l6h 30438  mapdh6hN 30363
[Baer] p. 48Part (7)mapdh75cN 30373  mapdh75d 30374  mapdh75e 30372  mapdh75fN 30375  mapdh7cN 30369  mapdh7dN 30370  mapdh7eN 30368  mapdh7fN 30371
[Baer] p. 48Part (8)mapdh8 30409  mapdh8a 30395  mapdh8aa 30396  mapdh8ab 30397  mapdh8ac 30398  mapdh8ad 30399  mapdh8b 30400  mapdh8c 30401  mapdh8d 30403  mapdh8d0N 30402  mapdh8e 30404  mapdh8fN 30405  mapdh8g 30406  mapdh8i 30407  mapdh8j 30408
[Baer] p. 48Part (9)mapdh9a 30410
[Baer] p. 48Equation 10mapdhvmap 30389
[Baer] p. 49Part 12hdmap11 30471  hdmapeq0 30467  hdmapf1oN 30488  hdmapneg 30469  hdmaprnN 30487  hdmaprnlem1N 30472  hdmaprnlem3N 30473  hdmaprnlem3uN 30474  hdmaprnlem4N 30476  hdmaprnlem6N 30477  hdmaprnlem7N 30478  hdmaprnlem8N 30479  hdmaprnlem9N 30480  hdmapsub 30470
[Baer] p. 49Part 14hdmap14lem1 30491  hdmap14lem10 30500  hdmap14lem1a 30489  hdmap14lem2N 30492  hdmap14lem2a 30490  hdmap14lem3 30493  hdmap14lem8 30498  hdmap14lem9 30499
[Baer] p. 50Part 14hdmap14lem11 30501  hdmap14lem12 30502  hdmap14lem13 30503  hdmap14lem14 30504  hdmap14lem15 30505  hgmapval 30510
[Baer] p. 50Part 15hgmapadd 30517  hgmapmul 30518  hgmaprnlem2N 30520  hgmapvs 30514
[Baer] p. 50Part 16hgmaprnN 30524
[Baer] p. 110Lemma 1hdmapip0com 30540
[Baer] p. 110Line 27hdmapinvlem1 30541
[Baer] p. 110Line 28hdmapinvlem2 30542
[Baer] p. 110Line 30hdmapinvlem3 30543
[Baer] p. 110Part 1.2hdmapglem5 30545  hgmapvv 30549
[Baer] p. 110Proposition 1hdmapinvlem4 30544
[Baer] p. 111Line 10hgmapvvlem1 30546
[Baer] p. 111Line 15hdmapg 30553  hdmapglem7 30552
[BellMachover] p. 36Lemma 10.3id1 21
[BellMachover] p. 97Definition 10.1df-eu 2106
[BellMachover] p. 460Notationdf-mo 2107
[BellMachover] p. 460Definitionmo3 2132
[BellMachover] p. 461Axiom Extax-ext 2222
[BellMachover] p. 462Theorem 1.1bm1.1 2226
[BellMachover] p. 463Axiom Repaxrep5 4012
[BellMachover] p. 463Scheme Sepaxsep 4016
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4020
[BellMachover] p. 466Axiom Powaxpow3 4064
[BellMachover] p. 466Axiom Unionaxun2 4384
[BellMachover] p. 468Definitiondf-ord 4267
[BellMachover] p. 469Theorem 2.2(i)ordirr 4282
[BellMachover] p. 469Theorem 2.2(iii)onelon 4289
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4284
[BellMachover] p. 471Definition of Ndf-om 4527
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4467
[BellMachover] p. 471Definition of Limdf-lim 4269
[BellMachover] p. 472Axiom Infzfinf2 7201
[BellMachover] p. 473Theorem 2.8limom 4541
[BellMachover] p. 477Equation 3.1df-r1 7294
[BellMachover] p. 478Definitionrankval2 7348
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7312  r1ord3g 7309
[BellMachover] p. 480Axiom Regzfreg2 7168
[BellMachover] p. 488Axiom ACac5 7962  dfac4 7607
[BellMachover] p. 490Definition of alephalephval3 7595
[BeltramettiCassinelli] p. 98Remarkatlatmstc 27939
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22558
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22600  chirredi 22599
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22588
[Beran] p. 3Definition of joinsshjval3 21558
[Beran] p. 39Theorem 2.3(i)cmcm2 21838  cmcm2i 21815  cmcm2ii 21820  cmt2N 27870
[Beran] p. 40Theorem 2.3(iii)lecm 21839  lecmi 21824  lecmii 21825
[Beran] p. 45Theorem 3.4cmcmlem 21813
[Beran] p. 49Theorem 4.2cm2j 21842  cm2ji 21847  cm2mi 21848
[Beran] p. 95Definitiondf-sh 21411  issh2 21413
[Beran] p. 95Lemma 3.1(S5)his5 21290
[Beran] p. 95Lemma 3.1(S6)his6 21303
[Beran] p. 95Lemma 3.1(S7)his7 21294
[Beran] p. 95Lemma 3.2(S8)ho01i 22033
[Beran] p. 95Lemma 3.2(S9)hoeq1 22035
[Beran] p. 95Lemma 3.2(S10)ho02i 22034
[Beran] p. 95Lemma 3.2(S11)hoeq2 22036
[Beran] p. 95Postulate (S1)ax-his1 21286  his1i 21304
[Beran] p. 95Postulate (S2)ax-his2 21287
[Beran] p. 95Postulate (S3)ax-his3 21288
[Beran] p. 95Postulate (S4)ax-his4 21289
[Beran] p. 96Definition of normdf-hnorm 21173  dfhnorm2 21326  normval 21328
[Beran] p. 96Definition for Cauchy sequencehcau 21388
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21178
[Beran] p. 96Definition of complete subspaceisch3 21446
[Beran] p. 96Definition of convergedf-hlim 21177  hlimi 21392
[Beran] p. 97Theorem 3.3(i)norm-i-i 21337  norm-i 21333
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21341  norm-ii 21342  normlem0 21313  normlem1 21314  normlem2 21315  normlem3 21316  normlem4 21317  normlem5 21318  normlem6 21319  normlem7 21320  normlem7tALT 21323
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21343  norm-iii 21344
[Beran] p. 98Remark 3.4bcs 21385  bcsiALT 21383  bcsiHIL 21384
[Beran] p. 98Remark 3.4(B)normlem9at 21325  normpar 21359  normpari 21358
[Beran] p. 98Remark 3.4(C)normpyc 21350  normpyth 21349  normpythi 21346
[Beran] p. 99Remarklnfn0 22252  lnfn0i 22247  lnop0 22171  lnop0i 22175
[Beran] p. 99Theorem 3.5(i)nmcexi 22231  nmcfnex 22258  nmcfnexi 22256  nmcopex 22234  nmcopexi 22232
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22259  nmcfnlbi 22257  nmcoplb 22235  nmcoplbi 22233
[Beran] p. 99Theorem 3.5(iii)lnfncon 22261  lnfnconi 22260  lnopcon 22240  lnopconi 22239
[Beran] p. 100Lemma 3.6normpar2i 21360
[Beran] p. 101Lemma 3.6norm3adifi 21357  norm3adifii 21352  norm3dif 21354  norm3difi 21351
[Beran] p. 102Theorem 3.7(i)chocunii 21505  pjhth 21597  pjhtheu 21598  pjpjhth 21629  pjpjhthi 21630  pjth 18475
[Beran] p. 102Theorem 3.7(ii)ococ 21610  ococi 21609
[Beran] p. 103Remark 3.8nlelchi 22266
[Beran] p. 104Theorem 3.9riesz3i 22267  riesz4 22269  riesz4i 22268
[Beran] p. 104Theorem 3.10cnlnadj 22284  cnlnadjeu 22283  cnlnadjeui 22282  cnlnadji 22281  cnlnadjlem1 22272  nmopadjlei 22293
[Beran] p. 106Theorem 3.11(i)adjeq0 22296
[Beran] p. 106Theorem 3.11(v)nmopadji 22295
[Beran] p. 106Theorem 3.11(ii)adjmul 22297
[Beran] p. 106Theorem 3.11(iv)adjadj 22141
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22307  nmopcoadji 22306
[Beran] p. 106Theorem 3.11(iii)adjadd 22298
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22308
[Beran] p. 106Theorem 3.11(viii)adjcoi 22305  pjadj2coi 22409  pjadjcoi 22366
[Beran] p. 107Definitiondf-ch 21426  isch2 21428
[Beran] p. 107Remark 3.12choccl 21510  isch3 21446  occl 21508  ocsh 21487  shoccl 21509  shocsh 21488
[Beran] p. 107Remark 3.12(B)ococin 21612
[Beran] p. 108Theorem 3.13chintcl 21536
[Beran] p. 109Property (i)pjadj2 22392  pjadj3 22393  pjadji 21907  pjadjii 21896
[Beran] p. 109Property (ii)pjidmco 22386  pjidmcoi 22382  pjidmi 21895
[Beran] p. 110Definition of projector orderingpjordi 22378
[Beran] p. 111Remarkho0val 21955  pjch1 21892
[Beran] p. 111Definitiondf-hfmul 21791  df-hfsum 21790  df-hodif 21789  df-homul 21788  df-hosum 21787
[Beran] p. 111Lemma 4.4(i)pjo 21893
[Beran] p. 111Lemma 4.4(ii)pjch 21916  pjchi 21636
[Beran] p. 111Lemma 4.4(iii)pjoc2 21643  pjoc2i 21642
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 21902
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22370  pjssmii 21903
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22369
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22368
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22373
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22371  pjssge0ii 21904
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22372  pjdifnormii 21905
[BourbakiEns] p. Proposition 8fcof1 5624  fcofo 5625
[BourbakiFVR] p. Definition 1isder 24673
[BourbakiTop1] p. Remarkxnegmnf 10354  xnegpnf 10353
[BourbakiTop1] p. Remark rexneg 10355
[BourbakiTop1] p. Theoremneiss 16518
[BourbakiTop1] p. Axiom GT'tgpsubcn 17445
[BourbakiTop1] p. Example 1snfil 17231
[BourbakiTop1] p. Example 2neifil 17247
[BourbakiTop1] p. Definitionistgp 17432
[BourbakiTop1] p. Propositioncnpco 16668  ishmeo 17122  neips 16522
[BourbakiTop1] p. Definition 1filintn0 17228
[BourbakiTop1] p. Proposition 9cnpflf2 17367
[BourbakiTop1] p. Theorem 1 (d)iscncl 16670
[BourbakiTop1] p. Proposition Vissnei2 16525
[BourbakiTop1] p. Definition C'''df-cmp 16786
[BourbakiTop1] p. Proposition Viiinnei 16534
[BourbakiTop1] p. Proposition Vivneissex 16536
[BourbakiTop1] p. Proposition Viiielnei 16520  ssnei 16519
[BourbakiTop1] p. Remark below def. 1filn0 17229
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17213
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17230
[ChoquetDD] p. 2Definition of mappingdf-mpt 3956
[Cohen] p. 301Remarkrelogoprlem 19608
[Cohen] p. 301Property 2relogmul 19609  relogmuld 19638
[Cohen] p. 301Property 3relogdiv 19610  relogdivd 19639
[Cohen] p. 301Property 4relogexp 19613
[Cohen] p. 301Property 1alog1 19603
[Cohen] p. 301Property 1bloge 19604
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10780
[Crawley] p. 1Definition of posetdf-poset 13764
[Crawley] p. 107Theorem 13.2hlsupr 28005
[Crawley] p. 110Theorem 13.3arglem1N 28809  dalaw 28505
[Crawley] p. 111Theorem 13.4hlathil 30584
[Crawley] p. 111Definition of set Wdf-watsN 28609
[Crawley] p. 111Definition of dilationdf-dilN 28725  df-ldil 28723  isldil 28729
[Crawley] p. 111Definition of translationdf-ltrn 28724  df-trnN 28726  isltrn 28738  ltrnu 28740
[Crawley] p. 112Lemma Acdlema1N 28410  cdlema2N 28411  exatleN 28023
[Crawley] p. 112Lemma B1cvrat 28095  cdlemb 28413  cdlemb2 28660  cdlemb3 29225  idltrn 28769  l1cvat 27675  lhpat 28662  lhpat2 28664  lshpat 27676  ltrnel 28758  ltrnmw 28770
[Crawley] p. 112Lemma Ccdlemc1 28810  cdlemc2 28811  ltrnnidn 28793  trlat 28788  trljat1 28785  trljat2 28786  trljat3 28787  trlne 28804  trlnidat 28792  trlnle 28805
[Crawley] p. 112Definition of automorphismdf-pautN 28610
[Crawley] p. 113Lemma Ccdlemc 28816  cdlemc3 28812  cdlemc4 28813
[Crawley] p. 113Lemma Dcdlemd 28826  cdlemd1 28817  cdlemd2 28818  cdlemd3 28819  cdlemd4 28820  cdlemd5 28821  cdlemd6 28822  cdlemd7 28823  cdlemd8 28824  cdlemd9 28825  cdleme31sde 29004  cdleme31se 29001  cdleme31se2 29002  cdleme31snd 29005  cdleme32a 29060  cdleme32b 29061  cdleme32c 29062  cdleme32d 29063  cdleme32e 29064  cdleme32f 29065  cdleme32fva 29056  cdleme32fva1 29057  cdleme32fvcl 29059  cdleme32le 29066  cdleme48fv 29118  cdleme4gfv 29126  cdleme50eq 29160  cdleme50f 29161  cdleme50f1 29162  cdleme50f1o 29165  cdleme50laut 29166  cdleme50ldil 29167  cdleme50lebi 29159  cdleme50rn 29164  cdleme50rnlem 29163  cdlemeg49le 29130  cdlemeg49lebilem 29158
[Crawley] p. 113Lemma Ecdleme 29179  cdleme00a 28828  cdleme01N 28840  cdleme02N 28841  cdleme0a 28830  cdleme0aa 28829  cdleme0b 28831  cdleme0c 28832  cdleme0cp 28833  cdleme0cq 28834  cdleme0dN 28835  cdleme0e 28836  cdleme0ex1N 28842  cdleme0ex2N 28843  cdleme0fN 28837  cdleme0gN 28838  cdleme0moN 28844  cdleme1 28846  cdleme10 28873  cdleme10tN 28877  cdleme11 28889  cdleme11a 28879  cdleme11c 28880  cdleme11dN 28881  cdleme11e 28882  cdleme11fN 28883  cdleme11g 28884  cdleme11h 28885  cdleme11j 28886  cdleme11k 28887  cdleme11l 28888  cdleme12 28890  cdleme13 28891  cdleme14 28892  cdleme15 28897  cdleme15a 28893  cdleme15b 28894  cdleme15c 28895  cdleme15d 28896  cdleme16 28904  cdleme16aN 28878  cdleme16b 28898  cdleme16c 28899  cdleme16d 28900  cdleme16e 28901  cdleme16f 28902  cdleme16g 28903  cdleme19a 28922  cdleme19b 28923  cdleme19c 28924  cdleme19d 28925  cdleme19e 28926  cdleme19f 28927  cdleme1b 28845  cdleme2 28847  cdleme20aN 28928  cdleme20bN 28929  cdleme20c 28930  cdleme20d 28931  cdleme20e 28932  cdleme20f 28933  cdleme20g 28934  cdleme20h 28935  cdleme20i 28936  cdleme20j 28937  cdleme20k 28938  cdleme20l 28941  cdleme20l1 28939  cdleme20l2 28940  cdleme20m 28942  cdleme20y 28921  cdleme20zN 28920  cdleme21 28956  cdleme21d 28949  cdleme21e 28950  cdleme22a 28959  cdleme22aa 28958  cdleme22b 28960  cdleme22cN 28961  cdleme22d 28962  cdleme22e 28963  cdleme22eALTN 28964  cdleme22f 28965  cdleme22f2 28966  cdleme22g 28967  cdleme23a 28968  cdleme23b 28969  cdleme23c 28970  cdleme26e 28978  cdleme26eALTN 28980  cdleme26ee 28979  cdleme26f 28982  cdleme26f2 28984  cdleme26f2ALTN 28983  cdleme26fALTN 28981  cdleme27N 28988  cdleme27a 28986  cdleme27cl 28985  cdleme28c 28991  cdleme3 28856  cdleme30a 28997  cdleme31fv 29009  cdleme31fv1 29010  cdleme31fv1s 29011  cdleme31fv2 29012  cdleme31id 29013  cdleme31sc 29003  cdleme31sdnN 29006  cdleme31sn 28999  cdleme31sn1 29000  cdleme31sn1c 29007  cdleme31sn2 29008  cdleme31so 28998  cdleme35a 29067  cdleme35b 29069  cdleme35c 29070  cdleme35d 29071  cdleme35e 29072  cdleme35f 29073  cdleme35fnpq 29068  cdleme35g 29074  cdleme35h 29075  cdleme35h2 29076  cdleme35sn2aw 29077  cdleme35sn3a 29078  cdleme36a 29079  cdleme36m 29080  cdleme37m 29081  cdleme38m 29082  cdleme38n 29083  cdleme39a 29084  cdleme39n 29085  cdleme3b 28848  cdleme3c 28849  cdleme3d 28850  cdleme3e 28851  cdleme3fN 28852  cdleme3fa 28855  cdleme3g 28853  cdleme3h 28854  cdleme4 28857  cdleme40m 29086  cdleme40n 29087  cdleme40v 29088  cdleme40w 29089  cdleme41fva11 29096  cdleme41sn3aw 29093  cdleme41sn4aw 29094  cdleme41snaw 29095  cdleme42a 29090  cdleme42b 29097  cdleme42c 29091  cdleme42d 29092  cdleme42e 29098  cdleme42f 29099  cdleme42g 29100  cdleme42h 29101  cdleme42i 29102  cdleme42k 29103  cdleme42ke 29104  cdleme42keg 29105  cdleme42mN 29106  cdleme42mgN 29107  cdleme43aN 29108  cdleme43bN 29109  cdleme43cN 29110  cdleme43dN 29111  cdleme5 28859  cdleme50ex 29178  cdleme50ltrn 29176  cdleme51finvN 29175  cdleme51finvfvN 29174  cdleme51finvtrN 29177  cdleme6 28860  cdleme7 28868  cdleme7a 28862  cdleme7aa 28861  cdleme7b 28863  cdleme7c 28864  cdleme7d 28865  cdleme7e 28866  cdleme7ga 28867  cdleme8 28869  cdleme8tN 28874  cdleme9 28872  cdleme9a 28870  cdleme9b 28871  cdleme9tN 28876  cdleme9taN 28875  cdlemeda 28917  cdlemedb 28916  cdlemednpq 28918  cdlemednuN 28919  cdlemefr27cl 29022  cdlemefr32fva1 29029  cdlemefr32fvaN 29028  cdlemefrs32fva 29019  cdlemefrs32fva1 29020  cdlemefs27cl 29032  cdlemefs32fva1 29042  cdlemefs32fvaN 29041  cdlemesner 28915  cdlemeulpq 28839
[Crawley] p. 114Lemma E4atex 28695  4atexlem7 28694  cdleme0nex 28909  cdleme17a 28905  cdleme17c 28907  cdleme17d 29117  cdleme17d1 28908  cdleme17d2 29114  cdleme18a 28910  cdleme18b 28911  cdleme18c 28912  cdleme18d 28914  cdleme4a 28858
[Crawley] p. 115Lemma Ecdleme21a 28944  cdleme21at 28947  cdleme21b 28945  cdleme21c 28946  cdleme21ct 28948  cdleme21f 28951  cdleme21g 28952  cdleme21h 28953  cdleme21i 28954  cdleme22gb 28913
[Crawley] p. 116Lemma Fcdlemf 29182  cdlemf1 29180  cdlemf2 29181
[Crawley] p. 116Lemma Gcdlemftr1 29186  cdlemg16 29276  cdlemg28 29323  cdlemg28a 29312  cdlemg28b 29322  cdlemg3a 29216  cdlemg42 29348  cdlemg43 29349  cdlemg44 29352  cdlemg44a 29350  cdlemg46 29354  cdlemg47 29355  cdlemg9 29253  ltrnco 29338  ltrncom 29357  tgrpabl 29370  trlco 29346
[Crawley] p. 116Definition of Gdf-tgrp 29362
[Crawley] p. 117Lemma Gcdlemg17 29296  cdlemg17b 29281
[Crawley] p. 117Definition of Edf-edring-rN 29375  df-edring 29376
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 29379
[Crawley] p. 118Remarktendopltp 29399
[Crawley] p. 118Lemma Hcdlemh 29436  cdlemh1 29434  cdlemh2 29435
[Crawley] p. 118Lemma Icdlemi 29439  cdlemi1 29437  cdlemi2 29438
[Crawley] p. 118Lemma Jcdlemj1 29440  cdlemj2 29441  cdlemj3 29442  tendocan 29443
[Crawley] p. 118Lemma Kcdlemk 29593  cdlemk1 29450  cdlemk10 29462  cdlemk11 29468  cdlemk11t 29565  cdlemk11ta 29548  cdlemk11tb 29550  cdlemk11tc 29564  cdlemk11u-2N 29508  cdlemk11u 29490  cdlemk12 29469  cdlemk12u-2N 29509  cdlemk12u 29491  cdlemk13-2N 29495  cdlemk13 29471  cdlemk14-2N 29497  cdlemk14 29473  cdlemk15-2N 29498  cdlemk15 29474  cdlemk16-2N 29499  cdlemk16 29476  cdlemk16a 29475  cdlemk17-2N 29500  cdlemk17 29477  cdlemk18-2N 29505  cdlemk18-3N 29519  cdlemk18 29487  cdlemk19-2N 29506  cdlemk19 29488  cdlemk19u 29589  cdlemk1u 29478  cdlemk2 29451  cdlemk20-2N 29511  cdlemk20 29493  cdlemk21-2N 29510  cdlemk21N 29492  cdlemk22-3 29520  cdlemk22 29512  cdlemk23-3 29521  cdlemk24-3 29522  cdlemk25-3 29523  cdlemk26-3 29525  cdlemk26b-3 29524  cdlemk27-3 29526  cdlemk28-3 29527  cdlemk29-3 29530  cdlemk3 29452  cdlemk30 29513  cdlemk31 29515  cdlemk32 29516  cdlemk33N 29528  cdlemk34 29529  cdlemk35 29531  cdlemk36 29532  cdlemk37 29533  cdlemk38 29534  cdlemk39 29535  cdlemk39u 29587  cdlemk4 29453  cdlemk41 29539  cdlemk42 29560  cdlemk42yN 29563  cdlemk43N 29582  cdlemk45 29566  cdlemk46 29567  cdlemk47 29568  cdlemk48 29569  cdlemk49 29570  cdlemk5 29455  cdlemk50 29571  cdlemk51 29572  cdlemk52 29573  cdlemk53 29576  cdlemk54 29577  cdlemk55 29580  cdlemk55u 29585  cdlemk56 29590  cdlemk5a 29454  cdlemk5auN 29479  cdlemk5u 29480  cdlemk6 29456  cdlemk6u 29481  cdlemk7 29467  cdlemk7u-2N 29507  cdlemk7u 29489  cdlemk8 29457  cdlemk9 29458  cdlemk9bN 29459  cdlemki 29460  cdlemkid 29555  cdlemkj-2N 29501  cdlemkj 29482  cdlemksat 29465  cdlemksel 29464  cdlemksv 29463  cdlemksv2 29466  cdlemkuat 29485  cdlemkuel-2N 29503  cdlemkuel-3 29517  cdlemkuel 29484  cdlemkuv-2N 29502  cdlemkuv2-2 29504  cdlemkuv2-3N 29518  cdlemkuv2 29486  cdlemkuvN 29483  cdlemkvcl 29461  cdlemky 29545  cdlemkyyN 29581  tendoex 29594
[Crawley] p. 120Remarkdva1dim 29604
[Crawley] p. 120Lemma Lcdleml1N 29595  cdleml2N 29596  cdleml3N 29597  cdleml4N 29598  cdleml5N 29599  cdleml6 29600  cdleml7 29601  cdleml8 29602  cdleml9 29603  dia1dim 29681
[Crawley] p. 120Lemma Mdia11N 29668  diaf11N 29669  dialss 29666  diaord 29667  dibf11N 29781  djajN 29757
[Crawley] p. 120Definition of isomorphism mapdiaval 29652
[Crawley] p. 121Lemma Mcdlemm10N 29738  dia2dimlem1 29684  dia2dimlem2 29685  dia2dimlem3 29686  dia2dimlem4 29687  dia2dimlem5 29688  diaf1oN 29750  diarnN 29749  dvheveccl 29732  dvhopN 29736
[Crawley] p. 121Lemma Ncdlemn 29832  cdlemn10 29826  cdlemn11 29831  cdlemn11a 29827  cdlemn11b 29828  cdlemn11c 29829  cdlemn11pre 29830  cdlemn2 29815  cdlemn2a 29816  cdlemn3 29817  cdlemn4 29818  cdlemn4a 29819  cdlemn5 29821  cdlemn5pre 29820  cdlemn6 29822  cdlemn7 29823  cdlemn8 29824  cdlemn9 29825  diclspsn 29814
[Crawley] p. 121Definition of phi(q)df-dic 29793
[Crawley] p. 122Lemma Ndih11 29885  dihf11 29887  dihjust 29837  dihjustlem 29836  dihord 29884  dihord1 29838  dihord10 29843  dihord11b 29842  dihord11c 29844  dihord2 29847  dihord2a 29839  dihord2b 29840  dihord2cN 29841  dihord2pre 29845  dihord2pre2 29846  dihordlem6 29833  dihordlem7 29834  dihordlem7b 29835
[Crawley] p. 122Definition of isomorphism mapdihffval 29850  dihfval 29851  dihval 29852
[Eisenberg] p. 67Definition 5.3df-dif 3061
[Eisenberg] p. 82Definition 6.3dfom3 7206
[Eisenberg] p. 125Definition 8.21df-map 6634
[Eisenberg] p. 216Example 13.2(4)omenps 7213
[Eisenberg] p. 310Theorem 19.8cardprc 7471
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8033
[Enderton] p. 18Axiom of Empty Setaxnul 4024
[Enderton] p. 19Definitiondf-tp 3532
[Enderton] p. 26Exercise 5unissb 3735
[Enderton] p. 26Exercise 10pwel 4098
[Enderton] p. 28Exercise 7(b)pwun 4174
[Enderton] p. 30Theorem "Distributive laws"iinin1 3851  iinin2 3850  iinun2 3846  iunin1 3845  iunin2 3844
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3849  iundif2 3847
[Enderton] p. 32Exercise 20unineq 3306
[Enderton] p. 33Exercise 23iinuni 3863
[Enderton] p. 33Exercise 25iununi 3864
[Enderton] p. 33Exercise 24(a)iinpw 3868
[Enderton] p. 33Exercise 24(b)iunpw 4440  iunpwss 3869
[Enderton] p. 36Definitionopthwiener 4140
[Enderton] p. 38Exercise 6(a)unipw 4097
[Enderton] p. 38Exercise 6(b)pwuni 4079
[Enderton] p. 41Lemma 3Dopeluu 4396  rnex 4828  rnexg 4826
[Enderton] p. 41Exercise 8dmuni 4774  rnuni 4978
[Enderton] p. 42Definition of a functiondffun7 5117  dffun8 5118
[Enderton] p. 43Definition of function valuefunfv2 5414
[Enderton] p. 43Definition of single-rootedfuncnv 5146
[Enderton] p. 44Definition (d)dfima2 4900  dfima3 4901
[Enderton] p. 47Theorem 3Hfvco2 5421
[Enderton] p. 49Axiom of Choice (first form)ac7 7958  ac7g 7959  df-ac 7601  dfac2 7615  dfac2a 7614  dfac3 7606  dfac7 7616
[Enderton] p. 50Theorem 3K(a)imauni 5599
[Enderton] p. 52Definitiondf-map 6634
[Enderton] p. 53Exercise 21coass 5076
[Enderton] p. 53Exercise 27dmco 5066
[Enderton] p. 53Exercise 14(a)funin 5155
[Enderton] p. 53Exercise 22(a)imass2 4935
[Enderton] p. 54Remarkixpf 6698  ixpssmap 6710
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6678
[Enderton] p. 55Axiom of Choice (second form)ac9 7968  ac9s 7978
[Enderton] p. 56Theorem 3Merref 6540
[Enderton] p. 57Lemma 3Nerthi 6566
[Enderton] p. 57Definitiondf-ec 6522
[Enderton] p. 58Definitiondf-qs 6526
[Enderton] p. 60Theorem 3Qth3q 6627  th3qcor 6626  th3qlem1 6624  th3qlem2 6625
[Enderton] p. 61Exercise 35df-ec 6522
[Enderton] p. 65Exercise 56(a)dmun 4771
[Enderton] p. 68Definition of successordf-suc 4270
[Enderton] p. 71Definitiondf-tr 3990  dftr4 3994
[Enderton] p. 72Theorem 4Eunisuc 4340
[Enderton] p. 73Exercise 6unisuc 4340
[Enderton] p. 73Exercise 5(a)truni 4003
[Enderton] p. 73Exercise 5(b)trint 4004  trintALT 27088
[Enderton] p. 79Theorem 4I(A1)nna0 6462
[Enderton] p. 79Theorem 4I(A2)nnasuc 6464  onasuc 6387
[Enderton] p. 79Definition of operation valuedf-ov 5688
[Enderton] p. 80Theorem 4J(A1)nnm0 6463
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6465  onmsuc 6388
[Enderton] p. 81Theorem 4K(1)nnaass 6480
[Enderton] p. 81Theorem 4K(2)nna0r 6467  nnacom 6475
[Enderton] p. 81Theorem 4K(3)nndi 6481
[Enderton] p. 81Theorem 4K(4)nnmass 6482
[Enderton] p. 81Theorem 4K(5)nnmcom 6484
[Enderton] p. 82Exercise 16nnm0r 6468  nnmsucr 6483
[Enderton] p. 88Exercise 23nnaordex 6496
[Enderton] p. 129Definitiondf-en 6724
[Enderton] p. 132Theorem 6B(b)canth 6152
[Enderton] p. 133Exercise 1xpomen 7501
[Enderton] p. 133Exercise 2qnnen 12300
[Enderton] p. 134Theorem (Pigeonhole Principle)php 6904
[Enderton] p. 135Corollary 6Cphp3 6906
[Enderton] p. 136Corollary 6Enneneq 6903
[Enderton] p. 136Corollary 6D(a)pssinf 6932
[Enderton] p. 136Corollary 6D(b)ominf 6934
[Enderton] p. 137Lemma 6Fpssnn 6940
[Enderton] p. 138Corollary 6Gssfi 6942
[Enderton] p. 139Theorem 6H(c)mapen 6884
[Enderton] p. 142Theorem 6I(3)xpcdaen 7667
[Enderton] p. 142Theorem 6I(4)mapcdaen 7668
[Enderton] p. 143Theorem 6Jcda0en 7663  cda1en 7659
[Enderton] p. 144Exercise 13iunfi 7003  unifi 7004  unifi2 7005
[Enderton] p. 144Corollary 6Kundif2 3416  unfi 6983  unfi2 6985
[Enderton] p. 145Figure 38ffoss 5337
[Enderton] p. 145Definitiondf-dom 6725
[Enderton] p. 146Example 1domen 6735  domeng 6736
[Enderton] p. 146Example 3nndomo 6913  nnsdom 7212  nnsdomg 6975
[Enderton] p. 149Theorem 6L(a)cdadom2 7671
[Enderton] p. 149Theorem 6L(c)mapdom1 6885  xpdom1 6820  xpdom1g 6818  xpdom2g 6817
[Enderton] p. 149Theorem 6L(d)mapdom2 6891
[Enderton] p. 151Theorem 6Mzorn 7992  zorng 7989
[Enderton] p. 151Theorem 6M(4)ac8 7977  dfac5 7613
[Enderton] p. 159Theorem 6Qunictb 8051
[Enderton] p. 164Exampleinfdif 7693
[Enderton] p. 168Definitiondf-po 4186
[Enderton] p. 192Theorem 7M(a)oneli 4370
[Enderton] p. 192Theorem 7M(b)ontr1 4310
[Enderton] p. 192Theorem 7M(c)onirri 4369
[Enderton] p. 193Corollary 7N(b)0elon 4317
[Enderton] p. 193Corollary 7N(c)onsuci 4499
[Enderton] p. 193Corollary 7N(d)ssonunii 4449
[Enderton] p. 194Remarkonprc 4446
[Enderton] p. 194Exercise 16suc11 4366
[Enderton] p. 197Definitiondf-card 7430
[Enderton] p. 197Theorem 7Pcarden 8029
[Enderton] p. 200Exercise 25tfis 4515
[Enderton] p. 202Lemma 7Tr1tr 7306
[Enderton] p. 202Definitiondf-r1 7294
[Enderton] p. 202Theorem 7Qr1val1 7316
[Enderton] p. 204Theorem 7V(b)rankval4 7397
[Enderton] p. 206Theorem 7X(b)en2lp 7175
[Enderton] p. 207Exercise 30rankpr 7387  rankprb 7381  rankpw 7373  rankpwi 7353  rankuniss 7396
[Enderton] p. 207Exercise 34opthreg 7177
[Enderton] p. 208Exercise 35suc11reg 7178
[Enderton] p. 212Definition of alephalephval3 7595
[Enderton] p. 213Theorem 8A(a)alephord2 7561
[Enderton] p. 213Theorem 8A(b)cardalephex 7575
[Enderton] p. 218Theorem Schema 8Eonfununi 6218
[Enderton] p. 222Definition of kardkarden 7423  kardex 7422
[Enderton] p. 238Theorem 8Roeoa 6455
[Enderton] p. 238Theorem 8Soeoe 6457
[Enderton] p. 240Exercise 25oarec 6420
[Enderton] p. 257Definition of cofinalitycflm 7734
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18566
[Fremlin5] p. 213Lemma 565Cauniioovol 18606
[Fremlin5] p. 214Lemma 565Cauniioombl 18616
[FreydScedrov] p. 283Axiom of Infinityax-inf 7197  inf1 7181  inf2 7182
[Gleason] p. 117Proposition 9-2.1df-enq 8389  enqer 8399
[Gleason] p. 117Proposition 9-2.2df-1nq 8394  df-nq 8390
[Gleason] p. 117Proposition 9-2.3df-plpq 8386  df-plq 8392
[Gleason] p. 119Proposition 9-2.4caovmo 5883  df-mpq 8387  df-mq 8393
[Gleason] p. 119Proposition 9-2.5df-rq 8395
[Gleason] p. 119Proposition 9-2.6ltexnq 8453
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8454  ltbtwnnq 8456
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8449
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8450
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8457
[Gleason] p. 121Definition 9-3.1df-np 8459
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8471
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8473
[Gleason] p. 122Definitiondf-1p 8460
[Gleason] p. 122Remark (1)prub 8472
[Gleason] p. 122Lemma 9-3.4prlem934 8511
[Gleason] p. 122Proposition 9-3.2df-ltp 8463
[Gleason] p. 122Proposition 9-3.3ltsopr 8510  psslinpr 8509  supexpr 8532  suplem1pr 8530  suplem2pr 8531
[Gleason] p. 123Proposition 9-3.5addclpr 8496  addclprlem1 8494  addclprlem2 8495  df-plp 8461
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8500
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8499
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8512
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8521  ltexprlem1 8514  ltexprlem2 8515  ltexprlem3 8516  ltexprlem4 8517  ltexprlem5 8518  ltexprlem6 8519  ltexprlem7 8520
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8523  ltaprlem 8522
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8524
[Gleason] p. 124Lemma 9-3.6prlem936 8525
[Gleason] p. 124Proposition 9-3.7df-mp 8462  mulclpr 8498  mulclprlem 8497  reclem2pr 8526
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8507
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8502
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8501
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8506
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8529  reclem3pr 8527  reclem4pr 8528
[Gleason] p. 126Proposition 9-4.1df-enr 8535  df-mpr 8534  df-plpr 8533  enrer 8544
[Gleason] p. 126Proposition 9-4.2df-0r 8540  df-1r 8541  df-nr 8536
[Gleason] p. 126Proposition 9-4.3df-mr 8538  df-plr 8537  negexsr 8578  recexsr 8583  recexsrlem 8579
[Gleason] p. 127Proposition 9-4.4df-ltr 8539
[Gleason] p. 130Proposition 10-1.3creui 9561  creur 9560  cru 9558
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8664  axcnre 8640
[Gleason] p. 132Definition 10-3.1crim 11413  crimd 11530  crimi 11491  crre 11412  crred 11529  crrei 11490
[Gleason] p. 132Definition 10-3.2remim 11415  remimd 11496
[Gleason] p. 133Definition 10.36absval2 11582  absval2d 11738  absval2i 11691
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11439  cjaddd 11518  cjaddi 11486
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11440  cjmuld 11519  cjmuli 11487
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11438  cjcjd 11497  cjcji 11469
[Gleason] p. 133Proposition 10-3.4(f)cjre 11437  cjreb 11421  cjrebd 11500  cjrebi 11472  cjred 11524  rere 11420  rereb 11418  rerebd 11499  rerebi 11471  rered 11522
[Gleason] p. 133Proposition 10-3.4(h)addcj 11446  addcjd 11510  addcji 11481
[Gleason] p. 133Proposition 10-3.7(a)absval 11536
[Gleason] p. 133Proposition 10-3.7(b)abscj 11577  abscjd 11743  abscji 11695
[Gleason] p. 133Proposition 10-3.7(c)abs00 11587  abs00d 11739  abs00i 11692  absne0d 11740
[Gleason] p. 133Proposition 10-3.7(d)releabs 11616  releabsd 11744  releabsi 11696
[Gleason] p. 133Proposition 10-3.7(f)absmul 11590  absmuld 11747  absmuli 11698
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11580  sqabsaddi 11699
[Gleason] p. 133Proposition 10-3.7(h)abstri 11625  abstrid 11749  abstrii 11702
[Gleason] p. 134Definition 10-4.1df-exp 10920  exp0 10923  expp1 10925  expp1d 11060
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 19706  cxpaddd 19744  expadd 10959  expaddd 11061  expaddz 10961
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 19715  cxpmuld 19761  expmul 10962  expmuld 11062  expmulz 10963
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 19712  mulcxpd 19755  mulexp 10956  mulexpd 11074  mulexpz 10957
[Gleason] p. 140Exercise 1znnen 12299
[Gleason] p. 141Definition 11-2.1fzval 10599
[Gleason] p. 168Proposition 12-2.1(a)climadd 11916  rlimadd 11927  rlimdiv 11930
[Gleason] p. 168Proposition 12-2.1(b)climsub 11918  rlimsub 11928
[Gleason] p. 168Proposition 12-2.1(c)climmul 11917  rlimmul 11929
[Gleason] p. 171Corollary 12-2.2climmulc2 11921
[Gleason] p. 172Corollary 12-2.5climrecl 11868
[Gleason] p. 172Proposition 12-2.4(c)climabs 11888  climcj 11889  climim 11891  climre 11890  rlimabs 11893  rlimcj 11894  rlimim 11896  rlimre 11895
[Gleason] p. 173Definition 12-3.1df-ltxr 8726  df-xr 8725  ltxr 10275
[Gleason] p. 175Definition 12-4.1df-limsup 11756  limsupval 11759
[Gleason] p. 180Theorem 12-5.1climsup 11954
[Gleason] p. 180Theorem 12-5.3caucvg 11962  caucvgb 11963  caucvgr 11959  climcau 11955
[Gleason] p. 182Exercise 3cvgcmp 12085
[Gleason] p. 182Exercise 4cvgrat 12147
[Gleason] p. 195Theorem 13-2.12abs1m 11630
[Gleason] p. 217Lemma 13-4.1btwnzge0 10768
[Gleason] p. 223Definition 14-1.1df-met 16046
[Gleason] p. 223Definition 14-1.1(a)met0 17580  xmet0 17579
[Gleason] p. 223Definition 14-1.1(b)metgt0 17595
[Gleason] p. 223Definition 14-1.1(c)metsym 17586
[Gleason] p. 223Definition 14-1.1(d)mettri 17588  mstri 17687  xmettri 17587  xmstri 17686
[Gleason] p. 225Definition 14-1.5xpsmet 17618
[Gleason] p. 230Proposition 14-2.6txlm 17014
[Gleason] p. 240Theorem 14-4.3metcnp4 18407
[Gleason] p. 240Proposition 14-4.2metcnp3 17758
[Gleason] p. 243Proposition 14-4.16addcn 18041  addcn2 11878  mulcn 18043  mulcn2 11880  subcn 18042  subcn2 11879
[Gleason] p. 295Remarkbcval3 11133  bcval4 11134
[Gleason] p. 295Equation 2bcpasc 11147
[Gleason] p. 295Definition of binomial coefficientbcval 11131  df-bc 11130
[Gleason] p. 296Remarkbcn0 11137  bcnn 11138
[Gleason] p. 296Theorem 15-2.8binom 12099
[Gleason] p. 308Equation 2ef0 12180
[Gleason] p. 308Equation 3efcj 12181
[Gleason] p. 309Corollary 15-4.3efne0 12185
[Gleason] p. 309Corollary 15-4.4efexp 12189
[Gleason] p. 310Equation 14sinadd 12252
[Gleason] p. 310Equation 15cosadd 12253
[Gleason] p. 311Equation 17sincossq 12264
[Gleason] p. 311Equation 18cosbnd 12269  sinbnd 12268
[Gleason] p. 311Lemma 15-4.7sqeqor 11031  sqeqori 11029
[Gleason] p. 311Definition of pidf-pi 12162
[Godowski] p. 730Equation SFgoeqi 22478
[GodowskiGreechie] p. 249Equation IV3oai 21890
[Halmos] p. 31Theorem 17.3riesz1 22270  riesz2 22271
[Halmos] p. 41Definition of Hermitianhmopadj2 22146
[Halmos] p. 42Definition of projector orderingpjordi 22378
[Halmos] p. 43Theorem 26.1elpjhmop 22390  elpjidm 22389  pjnmopi 22353
[Halmos] p. 44Remarkpjinormi 21909  pjinormii 21898
[Halmos] p. 44Theorem 26.2elpjch 22394  pjrn 21929  pjrni 21924  pjvec 21918
[Halmos] p. 44Theorem 26.3pjnorm2 21949
[Halmos] p. 44Theorem 26.4hmopidmpj 22359  hmopidmpji 22357
[Halmos] p. 45Theorem 27.1pjinvari 22396
[Halmos] p. 45Theorem 27.3pjoci 22385  pjocvec 21919
[Halmos] p. 45Theorem 27.4pjorthcoi 22374
[Halmos] p. 48Theorem 29.2pjssposi 22377
[Halmos] p. 48Theorem 29.3pjssdif1i 22380  pjssdif2i 22379
[Halmos] p. 50Definition of spectrumdf-spec 22060
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)id1 21
[Hamilton] p. 73Rule 1ax-mp 9
[Hamilton] p. 74Rule 2ax-gen 1525
[Hatcher] p. 25Definitiondf-phtpc 18162  df-phtpy 18141
[Hatcher] p. 26Definitiondf-pco 18175  df-pi1 18178
[Hatcher] p. 26Proposition 1.2phtpcer 18165
[Hatcher] p. 26Proposition 1.3pi1grp 18220
[Herstein] p. 54Exercise 28df-grpo 20483
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14173  grpoideu 20501  mndideu 14050
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14191  grpoinveu 20514
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14210  grpo2inv 20531
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14219  grpoinvop 20533
[Herstein] p. 57Exercise 1isgrp2d 20527  isgrp2i 20528
[Hitchcock] p. 5Rule A3mpto1 1517
[Hitchcock] p. 5Rule A4mpto2 1518
[Hitchcock] p. 5Rule A5mtp-xor 1519
[Holland] p. 1519Theorem 2sumdmdi 22625
[Holland] p. 1520Lemma 5cdj1i 22638  cdj3i 22646  cdj3lem1 22639  cdjreui 22637
[Holland] p. 1524Lemma 7mddmdin0i 22636
[Holland95] p. 13Theorem 3.6hlathil 30584
[Holland95] p. 14Line 15hgmapvs 30514
[Holland95] p. 14Line 16hdmaplkr 30536
[Holland95] p. 14Line 17hdmapellkr 30537
[Holland95] p. 14Line 19hdmapglnm2 30534
[Holland95] p. 14Line 20hdmapip0com 30540
[Holland95] p. 14Theorem 3.6hdmapevec2 30459
[Holland95] p. 14Lines 24 and 25hdmapoc 30554
[Holland95] p. 204Definition of involutiondf-srng 15286
[Holland95] p. 212Definition of subspacedf-psubsp 28122
[Holland95] p. 214Lemma 3.3lclkrlem2v 30148
[Holland95] p. 214Definition 3.2df-lpolN 30101
[Holland95] p. 214Definition of nonsingularpnonsingN 28552
[Holland95] p. 215Lemma 3.3(1)dihoml4 29997  poml4N 28572
[Holland95] p. 215Lemma 3.3(2)dochexmid 30088  pexmidALTN 28597  pexmidN 28588
[Holland95] p. 218Theorem 3.6lclkr 30153
[Holland95] p. 218Definition of dual vector spacedf-ldual 27744  ldualset 27745
[Holland95] p. 222Item 1df-lines 28120  df-pointsN 28121
[Holland95] p. 222Item 2df-polarityN 28522
[Holland95] p. 223Remarkispsubcl2N 28566  omllaw4 27866  pol1N 28529  polcon3N 28536
[Holland95] p. 223Definitiondf-psubclN 28554
[Holland95] p. 223Equation for polaritypolval2N 28525
[Hughes] p. 44Equation 1.21bax-his3 21288
[Hughes] p. 47Definition of projection operatordfpjop 22387
[Hughes] p. 49Equation 1.30eighmre 22168  eigre 22040  eigrei 22039
[Hughes] p. 49Equation 1.31eighmorth 22169  eigorth 22043  eigorthi 22042
[Hughes] p. 137Remark (ii)eigposi 22041
[Jech] p. 4Definition of classcv 1607  cvjust 2236
[Jech] p. 42Lemma 6.1alephexp1 8055
[Jech] p. 42Equation 6.1alephadd 8053  alephmul 8054
[Jech] p. 43Lemma 6.2infmap 8052  infmap2 7702
[Jech] p. 71Lemma 9.3jech9.3 7344
[Jech] p. 72Equation 9.3scott0 7414  scottex 7413
[Jech] p. 72Exercise 9.1rankval4 7397
[Jech] p. 72Scheme "Collection Principle"cp 7419
[Jech] p. 78Definition implied by the footnoteopthprc 4622
[JonesMatijasevic] p. 694Definition 2.3rmxyval 25966
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26062
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26063
[JonesMatijasevic] p. 695Equation 2.7rmxadd 25978
[JonesMatijasevic] p. 695Equation 2.8rmyadd 25982
[JonesMatijasevic] p. 695Equation 2.9rmxp1 25983  rmyp1 25984
[JonesMatijasevic] p. 695Equation 2.10rmxm1 25985  rmym1 25986
[JonesMatijasevic] p. 695Equation 2.11rmx0 25976  rmx1 25977  rmxluc 25987
[JonesMatijasevic] p. 695Equation 2.12rmy0 25980  rmy1 25981  rmyluc 25988
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 25990
[JonesMatijasevic] p. 695Equation 2.14rmydbl 25991
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26013  jm2.17b 26014  jm2.17c 26015
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26052
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26056
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26047
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26016  jm2.24nn 26012
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26061
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26067  rmygeid 26017
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26079
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1673
[Kalmbach] p. 14Definition of latticechabs1 21720  chabs1i 21722  chabs2 21721  chabs2i 21723  chjass 21737  chjassi 21690  latabs1 13877  latabs2 13878
[Kalmbach] p. 15Definition of atomdf-at 22543  ela 22544
[Kalmbach] p. 15Definition of coverscvbr2 22488  cvrval2 27894
[Kalmbach] p. 16Definitiondf-ol 27798  df-oml 27799
[Kalmbach] p. 20Definition of commutescmbr 21806  cmbri 21812  cmtvalN 27831  df-cm 21805  df-cmtN 27797
[Kalmbach] p. 22Remarkomllaw5N 27867  pjoml5 21835  pjoml5i 21810
[Kalmbach] p. 22Definitionpjoml2 21833  pjoml2i 21807
[Kalmbach] p. 22Theorem 2(v)cmcm 21836  cmcmi 21814  cmcmii 21819  cmtcomN 27869
[Kalmbach] p. 22Theorem 2(ii)omllaw3 27865  omlsi 21608  pjoml 21640  pjomli 21639
[Kalmbach] p. 22Definition of OML lawomllaw2N 27864
[Kalmbach] p. 23Remarkcmbr2i 21818  cmcm3 21837  cmcm3i 21816  cmcm3ii 21821  cmcm4i 21817  cmt3N 27871  cmt4N 27872  cmtbr2N 27873
[Kalmbach] p. 23Lemma 3cmbr3 21830  cmbr3i 21822  cmtbr3N 27874
[Kalmbach] p. 25Theorem 5fh1 21840  fh1i 21843  fh2 21841  fh2i 21844  omlfh1N 27878
[Kalmbach] p. 65Remarkchjatom 22562  chslej 21702  chsleji 21662  shslej 21584  shsleji 21574
[Kalmbach] p. 65Proposition 1chocin 21699  chocini 21658  chsupcl 21544  chsupval2 21614  h0elch 21459  helch 21448  hsupval2 21613  ocin 21500  ococss 21497  shococss 21498
[Kalmbach] p. 65Definition of subspace sumshsval 21516
[Kalmbach] p. 66Remarkdf-pjh 21599  pjssmi 22370  pjssmii 21903
[Kalmbach] p. 67Lemma 3osum 21867  osumi 21864
[Kalmbach] p. 67Lemma 4pjci 22405
[Kalmbach] p. 103Exercise 6atmd2 22605
[Kalmbach] p. 103Exercise 12mdsl0 22515
[Kalmbach] p. 140Remarkhatomic 22565  hatomici 22564  hatomistici 22567
[Kalmbach] p. 140Proposition 1atlatmstc 27939
[Kalmbach] p. 140Proposition 1(i)atexch 22586  lsatexch 27663
[Kalmbach] p. 140Proposition 1(ii)chcv1 22560  cvlcvr1 27959  cvr1 28029
[Kalmbach] p. 140Proposition 1(iii)cvexch 22579  cvexchi 22574  cvrexch 28039
[Kalmbach] p. 149Remark 2chrelati 22569  hlrelat 28021  hlrelat5N 28020  lrelat 27634
[Kalmbach] p. 153Exercise 5lsmcv 15569  lsmsatcv 27630  spansncv 21875  spansncvi 21874
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 27649  spansncv2 22498
[Kalmbach] p. 266Definitiondf-st 22416
[Kalmbach2] p. 8Definition of adjointdf-adjh 22054
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8122  fpwwe2 8119
[KanamoriPincus] p. 416Corollary 1.3canth4 8123
[KanamoriPincus] p. 417Corollary 1.6canthp1 8130
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8125
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8127
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8140
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8144  gchxpidm 8145
[KanamoriPincus] p. 419Theorem 2.1gchacg 8148  gchhar 8147
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7700  unxpwdom 7161
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8150
[Kreyszig] p. 3Property M1metcl 17569  xmetcl 17568
[Kreyszig] p. 4Property M2meteq0 17576
[Kreyszig] p. 8Definition 1.1-8dscmet 17767
[Kreyszig] p. 12Equation 5conjmul 9309  muleqadd 9246
[Kreyszig] p. 18Definition 1.3-2mopnval 17656
[Kreyszig] p. 19Remarkmopntopon 17657
[Kreyszig] p. 19Theorem T1mopn0 17716  mopnm 17662
[Kreyszig] p. 19Theorem T2unimopn 17714
[Kreyszig] p. 19Definition of neighborhoodneibl 17719
[Kreyszig] p. 20Definition 1.3-3metcnp2 17760
[Kreyszig] p. 25Definition 1.4-1lmbr 16660  lmmbr 18356  lmmbr2 18357
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 16780
[Kreyszig] p. 28Theorem 1.4-5lmcau 18410
[Kreyszig] p. 28Definition 1.4-3iscau 18374  iscmet2 18392
[Kreyszig] p. 30Theorem 1.4-7cmetss 18412
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 16859  metelcls 18402
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18403  metcld2 18404
[Kreyszig] p. 51Equation 2clmvneg1 18261  lmodvneg1 15342  nvinv 20822  vcm 20752
[Kreyszig] p. 51Equation 1aclm0vs 18260  lmod0vs 15338  vc0 20750
[Kreyszig] p. 51Equation 1blmodvs0 15339  vcz 20751
[Kreyszig] p. 58Definition 2.2-1imsmet 20885
[Kreyszig] p. 59Equation 1imsdval 20880  imsdval2 20881
[Kreyszig] p. 63Problem 1nvnd 20882
[Kreyszig] p. 64Problem 2nvge0 20865  nvz 20860
[Kreyszig] p. 64Problem 3nvabs 20864
[Kreyszig] p. 91Definition 2.7-1isblo3i 21004
[Kreyszig] p. 92Equation 2df-nmoo 20948
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21010  blocni 21008
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21009
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18311  ipeq0 16214  ipz 20920
[Kreyszig] p. 135Problem 2pythi 21053
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21057
[Kreyszig] p. 144Equation 4supcvg 12122
[Kreyszig] p. 144Theorem 3.3-1minvec 18472  minveco 21088
[Kreyszig] p. 196Definition 3.9-1df-aj 20953
[Kreyszig] p. 247Theorem 4.7-2bcth 18423
[Kreyszig] p. 249Theorem 4.7-3ubth 21077
[Kreyszig] p. 470Definition of positive operator orderingleop 22328  leopg 22327
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22346
[Kreyszig] p. 525Theorem 10.1-1htth 21123
[Kunen] p. 10Axiom 0a9e 1806  axnul 4024
[Kunen] p. 11Axiom 3axnul 4024
[Kunen] p. 12Axiom 6zfrep6 5575
[Kunen] p. 24Definition 10.24mapval 6644  mapvalg 6642
[Kunen] p. 30Lemma 10.20fodom 8007
[Kunen] p. 31Definition 10.24mapex 6638
[Kunen] p. 95Definition 2.1df-r1 7294
[Kunen] p. 97Lemma 2.10r1elss 7336  r1elssi 7335
[Kunen] p. 107Exercise 4rankop 7388  rankopb 7382  rankuni 7393  rankxplim 7407  rankxpsuc 7410
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3793
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26517
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26512
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26518
[LeBlanc] p. 277Rule R2axnul 4024
[Levy] p. 338Axiomdf-clab 2228  df-clel 2237  df-cleq 2234
[Levy58] p. 2Definition Iisfin1-3 7870
[Levy58] p. 2Definition IIdf-fin2 7770
[Levy58] p. 2Definition Iadf-fin1a 7769
[Levy58] p. 2Definition IIIdf-fin3 7772
[Levy58] p. 3Definition Vdf-fin5 7773
[Levy58] p. 3Definition IVdf-fin4 7771
[Levy58] p. 4Definition VIdf-fin6 7774
[Levy58] p. 4Definition VIIdf-fin7 7775
[Levy58], p. 3Theorem 1fin1a2 7899
[Lopez-Astorga] p. 12Rule 1mpto1 1517
[Lopez-Astorga] p. 12Rule 2mpto2 1518
[Lopez-Astorga] p. 12Rule 3mtp-xor 1519
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 22613
[Maeda] p. 168Lemma 5mdsym 22617  mdsymi 22616
[Maeda] p. 168Lemma 4(i)mdsymlem4 22611  mdsymlem6 22613  mdsymlem7 22614
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22615
[MaedaMaeda] p. 1Remarkssdmd1 22518  ssdmd2 22519  ssmd1 22516  ssmd2 22517
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22514
[MaedaMaeda] p. 1Definition 1.1df-dmd 22486  df-md 22485  mdbr 22499
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22536  mdslj1i 22524  mdslj2i 22525  mdslle1i 22522  mdslle2i 22523  mdslmd1i 22534  mdslmd2i 22535
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22526  mdsl2bi 22528  mdsl2i 22527
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22540
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22537
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22538
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22515
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22520  mdsl3 22521
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22539
[MaedaMaeda] p. 4Theorem 1.14mdcompli 22634
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 27941  hlrelat1 28019
[MaedaMaeda] p. 31Lemma 7.5lcvexch 27659
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22541  cvmdi 22529  cvnbtwn4 22494  cvrnbtwn4 27899
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22542
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 27960  cvp 22580  cvrp 28035  lcvp 27660
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22604
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22603
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 27953  hlexch4N 28011
[MaedaMaeda] p. 34Exercise 7.1atabsi 22606
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28062
[MaedaMaeda] p. 61Definition 15.10psubN 28368  atpsubN 28372  df-pointsN 28121  pointpsubN 28370
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28123  pmap11 28381  pmaple 28380  pmapsub 28387  pmapval 28376
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 28384  pmap1N 28386
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 28389  pmapglb2N 28390  pmapglb2xN 28391  pmapglbx 28388
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 28471
[MaedaMaeda] p. 67Postulate PS1ps-1 28096
[MaedaMaeda] p. 68Lemma 16.2df-padd 28415  paddclN 28461  paddidm 28460
[MaedaMaeda] p. 68Condition PS2ps-2 28097
[MaedaMaeda] p. 68Equation 16.2.1paddass 28457
[MaedaMaeda] p. 69Lemma 16.4ps-1 28096
[MaedaMaeda] p. 69Theorem 16.4ps-2 28097
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14659  lsmmod2 14660  lssats 27632  shatomici 22563  shatomistici 22566  shmodi 21594  shmodsi 21593
[MaedaMaeda] p. 130Remark 29.6dmdmd 22505  mdsymlem7 22614
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 21811
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 21697
[MaedaMaeda] p. 139Remarksumdmdii 22620
[Margaris] p. 40Rule Cexlimiv 2011
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 359  df-ex 1527  df-or 358  dfbi2 606
[Margaris] p. 51Theorem 1id1 21
[Margaris] p. 56Theorem 3syld 41
[Margaris] p. 59Section 14notnot2ALTVD 27122
[Margaris] p. 60Theorem 8mth8 137
[Margaris] p. 60Section 14con3ALTVD 27123
[Margaris] p. 79Rule Cexinst01 26875  exinst11 26876
[Margaris] p. 89Theorem 19.219.2 1748  r19.2z 3429
[Margaris] p. 89Theorem 19.319.3 1749  rr19.3v 2831
[Margaris] p. 89Theorem 19.5alcom 1557
[Margaris] p. 89Theorem 19.6alex 1559
[Margaris] p. 89Theorem 19.7alnex 1558
[Margaris] p. 89Theorem 19.819.8a 1747
[Margaris] p. 89Theorem 19.919.9 1751  19.9v 1998
[Margaris] p. 89Theorem 19.11excom 1754  excomim 1753
[Margaris] p. 89Theorem 19.1219.12 1755  r19.12 2604
[Margaris] p. 90Theorem 19.14exnal 1561
[Margaris] p. 90Theorem 19.152albi 26542  albi 1541  ralbi 2627
[Margaris] p. 90Theorem 19.1619.16 1756
[Margaris] p. 90Theorem 19.1719.17 1757
[Margaris] p. 90Theorem 19.182exbi 26544  exbi 1568
[Margaris] p. 90Theorem 19.1919.19 1758
[Margaris] p. 90Theorem 19.202alim 26541  alim 1537  alimd 1694  alimdh 1540  alimdv 2005  ralimdaa 2568  ralimdv 2570  ralimdva 2569  sbcimdv 2963
[Margaris] p. 90Theorem 19.2119.21-2 1761  19.21 1760  19.21bi 1763  19.21t 1759  19.21v 1999  19.21vv 26540  alrimd 1699  alrimdd 1698  alrimdh 1574  alrimdv 2002  alrimi 1695  alrimih 1542  alrimiv 2000  alrimivv 2001  r19.21 2577  r19.21be 2592  r19.21bi 2589  r19.21t 2576  r19.21v 2578  ralrimd 2579  ralrimdv 2580  ralrimdva 2581  ralrimdvv 2585  ralrimdvva 2586  ralrimi 2572  ralrimiv 2573  ralrimiva 2574  ralrimivv 2582  ralrimivva 2583  ralrimivvva 2584  ralrimivw 2575  rexlimi 2608
[Margaris] p. 90Theorem 19.222alimdv 2007  2exim 26543  2eximdv 2008  exim 1562  eximd 1700  eximdh 1575  eximdv 2006  rexim 2595  reximdai 2599  reximdv 2602  reximdv2 2600  reximdva 2603  reximdvai 2601  reximi2 2597
[Margaris] p. 90Theorem 19.2319.23 1766  19.23bi 1772  19.23t 1765  19.23v 2009  19.23vv 2010  exlimd 1773  exlimdh 1774  exlimdv 1921  exlimdvv 2014  exlimexi 26769  exlimi 1770  exlimih 1771  exlimiv 2011  exlimivv 2013  r19.23 2606  r19.23v 2607  rexlimd 2612  rexlimdv 2614  rexlimdv3a 2617  rexlimdva 2615  rexlimdvaa 2616  rexlimdvv 2621  rexlimdvva 2622  rexlimdvw 2618  rexlimiv 2609  rexlimiva 2610  rexlimivv 2620
[Margaris] p. 90Theorem 19.2419.24 1782
[Margaris] p. 90Theorem 19.2519.25 1591
[Margaris] p. 90Theorem 19.2619.26-2 1582  19.26-3an 1583  19.26 1581  r19.26-2 2624  r19.26-2a 23899  r19.26-3 2625  r19.26 2623  r19.26m 2626
[Margaris] p. 90Theorem 19.2719.27 1775  19.27v 2015  r19.27av 2629  r19.27z 3438  r19.27zv 3439
[Margaris] p. 90Theorem 19.2819.28 1776  19.28v 2016  19.28vv 26550  r19.28av 2630  r19.28z 3432  r19.28zv 3435  rr19.28v 2832
[Margaris] p. 90Theorem 19.2919.29 1584  19.29r 1585  19.29r2 1586  19.29x 1587  r19.29 2631  r19.29r 2632
[Margaris] p. 90Theorem 19.3019.30 1592  r19.30 2633
[Margaris] p. 90Theorem 19.3119.31 1784  19.31vv 26548
[Margaris] p. 90Theorem 19.3219.32 1783  r19.32v 2634
[Margaris] p. 90Theorem 19.3319.33-2 26546  19.33 1595  19.33b 1596
[Margaris] p. 90Theorem 19.3419.34 1787
[Margaris] p. 90Theorem 19.3519.35 1588  19.35i 1589  19.35ri 1590  r19.35 2635
[Margaris] p. 90Theorem 19.3619.36 1777  19.36aiv 2018  19.36i 1778  19.36v 2017  19.36vv 26547  r19.36av 2636  r19.36zv 3440
[Margaris] p. 90Theorem 19.3719.37 1779  19.37aiv 2021  19.37v 2020  19.37vv 26549  r19.37 2637  r19.37av 2638  r19.37zv 3436
[Margaris] p. 90Theorem 19.3819.38 1780
[Margaris] p. 90Theorem 19.3919.39 1781
[Margaris] p. 90Theorem 19.4019.40-2 1598  19.40 1597  r19.40 2639
[Margaris] p. 90Theorem 19.4119.41 1788  19.41rg 26798  19.41v 2022  19.41vv 2023  19.41vvv 2024  19.41vvvv 2025  r19.41 2640  r19.41v 2641
[Margaris] p. 90Theorem 19.4219.42 1789  19.42v 2026  19.42vv 2028  19.42vvv 2029  r19.42v 2642
[Margaris] p. 90Theorem 19.4319.43 1593  r19.43 2643
[Margaris] p. 90Theorem 19.4419.44 1785  r19.44av 2644
[Margaris] p. 90Theorem 19.4519.45 1786  r19.45av 2645  r19.45zv 3437
[Margaris] p. 110Exercise 2(b)eu1 2122
[Mayet] p. 370Remarkjpi 22475  largei 22472  stri 22462
[Mayet3] p. 9Definition of CH-statesdf-hst 22417  ishst 22419
[Mayet3] p. 10Theoremhstrbi 22471  hstri 22470
[Mayet3] p. 1223Theorem 4.1mayete3i 21950
[Mayet3] p. 1240Theorem 7.1mayetes3i 21952
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22483
[MegPav2000] p. 2345Definition 3.4-1chintcl 21536  chsupcl 21544
[MegPav2000] p. 2345Definition 3.4-2hatomic 22565
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22559
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22586
[MegPav2000] p. 2366Figure 7pl42N 28602
[MegPav2002] p. 362Lemma 2.2latj31 13889  latj32 13887  latjass 13885
[Megill] p. 444Axiom C5ax-17 1617
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 1826  alequcom 1669  ax-10 1667
[Megill] p. 446Lemma L17equtrr 1816
[Megill] p. 446Lemma L18ax9from9o 1805
[Megill] p. 446Lemma L19hbnae-o 1834  hbnae 1833
[Megill] p. 447Remark 9.1df-sb 1872  sbid 1884
[Megill] p. 448Remark 9.6ax15 2089
[Megill] p. 448Scheme C4'ax-5o 1683
[Megill] p. 448Scheme C5'ax-4 1681
[Megill] p. 448Scheme C6'ax-7 1524
[Megill] p. 448Scheme C7'ax-6o 1686
[Megill] p. 448Scheme C8'ax-8 1612
[Megill] p. 448Scheme C9'ax-12o 1653
[Megill] p. 448Scheme C10'ax-9 1673  ax-9o 1804
[Megill] p. 448Scheme C11'ax-10o 1824
[Megill] p. 448Scheme C12'ax-13 1614
[Megill] p. 448Scheme C13'ax-14 1615
[Megill] p. 448Scheme C14'ax-15 2090
[Megill] p. 448Scheme C15'ax-11o 1928
[Megill] p. 448Scheme C16'ax-16 1915
[Megill] p. 448Theorem 9.4dral1-o 1845  dral1 1844  dral2-o 1847  dral2 1846  drex1 1848  drex2 1849  drsb1 1875  drsb2 1941
[Megill] p. 448Theorem 9.7conventions 3
[Megill] p. 449Theorem 9.7sbcom2 2062  sbequ 1940  sbid2v 2071
[Megill] p. 450Example in Appendixhba1 1707
[Mendelson] p. 35Axiom A3hirstL-ax3 26651
[Mendelson] p. 36Lemma 1.8id1 21
[Mendelson] p. 69Axiom 4ra4sbc 2980  ra4sbca 2981  stdpc4 1885
[Mendelson] p. 69Axiom 5ax-5o 1683  ra5 2985  stdpc5 1762
[Mendelson] p. 81Rule Cexlimiv 2011
[Mendelson] p. 95Axiom 6stdpc6 1810
[Mendelson] p. 95Axiom 7stdpc7 1880
[Mendelson] p. 225Axiom system NBGru 2905
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4140
[Mendelson] p. 231Exercise 4.10(k)inv1 3368
[Mendelson] p. 231Exercise 4.10(l)unv 3369
[Mendelson] p. 231Exercise 4.10(n)dfin3 3295
[Mendelson] p. 231Exercise 4.10(o)df-nul 3343
[Mendelson] p. 231Exercise 4.10(q)dfin4 3296
[Mendelson] p. 231Exercise 4.10(s)ddif 3202
[Mendelson] p. 231Definition of uniondfun3 3294
[Mendelson] p. 235Exercise 4.12(c)univ 4435
[Mendelson] p. 235Exercise 4.12(d)pwv 3706
[Mendelson] p. 235Exercise 4.12(j)pwin 4169
[Mendelson] p. 235Exercise 4.12(k)pwunss 4170
[Mendelson] p. 235Exercise 4.12(l)pwssun 4171
[Mendelson] p. 235Exercise 4.12(n)uniin 3727
[Mendelson] p. 235Exercise 4.12(p)reli 4699
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5078
[Mendelson] p. 244Proposition 4.8(g)epweon 4445
[Mendelson] p. 246Definition of successordf-suc 4270
[Mendelson] p. 250Exercise 4.36oelim2 6453
[Mendelson] p. 254Proposition 4.22(b)xpen 6883
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6805  xpsneng 6806
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6812  xpcomeng 6813
[Mendelson] p. 254Proposition 4.22(e)xpassen 6815
[Mendelson] p. 255Definitionbrsdom 6744
[Mendelson] p. 255Exercise 4.39endisj 6808
[Mendelson] p. 255Exercise 4.41mapprc 6636
[Mendelson] p. 255Exercise 4.43mapsnen 6797
[Mendelson] p. 255Exercise 4.45mapunen 6889
[Mendelson] p. 255Exercise 4.47xpmapen 6888
[Mendelson] p. 255Exercise 4.42(a)map0e 6665
[Mendelson] p. 255Exercise 4.42(b)map1 6798
[Mendelson] p. 257Proposition 4.24(a)undom 6809
[Mendelson] p. 258Exercise 4.56(b)cdaen 7657
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7666  cdacomen 7665
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7670
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7664
[Mendelson] p. 258Definition of cardinal sumcdaval 7654  df-cda 7652
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6390
[Mendelson] p. 266Proposition 4.34(f)oaordex 6416
[Mendelson] p. 275Proposition 4.42(d)entri3 8037
[Mendelson] p. 281Definitiondf-r1 7294
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7343
[Mendelson] p. 287Axiom system MKru 2905
[Mittelstaedt] p. 9Definitiondf-oc 21456
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3278
[Monk1] p. 33Theorem 3.2(i)ssrel 4662
[Monk1] p. 33Theorem 3.2(ii)eqrel 4663
[Monk1] p. 34Definition 3.3df-opab 3955
[Monk1] p. 36Theorem 3.7(i)coi1 5073  coi2 5074
[Monk1] p. 36Theorem 3.8(v)dm0 4778  rn0 4822
[Monk1] p. 36Theorem 3.7(ii)cnvi 4971
[Monk1] p. 37Theorem 3.13(i)relxp 4680
[Monk1] p. 37Theorem 3.13(x)dmxp 4783  rnxp 4992
[Monk1] p. 37Theorem 3.13(ii)xp0 4984  xp0r 4654
[Monk1] p. 38Theorem 3.16(ii)ima0 4916
[Monk1] p. 38Theorem 3.16(viii)imai 4913
[Monk1] p. 39Theorem 3.17imaexg 4912
[Monk1] p. 39Theorem 3.16(xi)imassrn 4911
[Monk1] p. 41Theorem 4.3(i)fnopfv 5487  funfvop 5464
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5393
[Monk1] p. 42Theorem 4.4(iii)fvelima 5401
[Monk1] p. 43Theorem 4.6funun 5132
[Monk1] p. 43Theorem 4.8(iv)dff13 5610  dff13f 5611
[Monk1] p. 46Theorem 4.15(v)funex 5570  funrnex 5574
[Monk1] p. 50Definition 5.4fniunfv 5600
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5041
[Monk1] p. 52Theorem 5.11(viii)ssint 3756
[Monk1] p. 52Definition 5.13 (i)1stval2 5963  df-1st 5948
[Monk1] p. 52Definition 5.13 (ii)2ndval2 5964  df-2nd 5949
[Monk1] p. 112Theorem 15.17(v)ranksn 7384  ranksnb 7357
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7385
[Monk1] p. 112Theorem 15.17(iii)rankun 7386  rankunb 7380
[Monk1] p. 113Theorem 15.18r1val3 7368
[Monk1] p. 113Definition 15.19df-r1 7294  r1val2 7367
[Monk1] p. 117Lemmazorn2 7991  zorn2g 7988
[Monk1] p. 133Theorem 18.11cardom 7477
[Monk1] p. 133Theorem 18.12canth3 8039
[Monk1] p. 133Theorem 18.14carduni 7472
[Monk2] p. 105Axiom C4ax-5 1522
[Monk2] p. 105Axiom C7ax-8 1612
[Monk2] p. 105Axiom C8ax-11 1613  ax-11o 1928
[Monk2] p. 105Axiom (C8)ax11v 1978
[Monk2] p. 108Lemma 5ax-5o 1683
[Monk2] p. 109Lemma 12ax-7 1524
[Monk2] p. 109Lemma 15equvin 1987  equvini 1868  eqvinop 4123
[Monk2] p. 113Axiom C5-1ax-17 1617
[Monk2] p. 113Axiom C5-2ax-6 1523
[Monk2] p. 113Axiom C5-3ax-7 1524
[Monk2] p. 114Lemma 21ax4 1680
[Monk2] p. 114Lemma 22ax5o 1682  hba1 1707
[Monk2] p. 114Lemma 23nfia1 1734
[Monk2] p. 114Lemma 24nfa2 1733  nfra2 2545
[Munkres] p. 77Example 2distop 16405  indistop 16411  indistopon 16410
[Munkres] p. 77Example 3fctop 16413  fctop2 16414
[Munkres] p. 77Example 4cctop 16415
[Munkres] p. 78Definition of basisdf-bases 16310  isbasis3g 16359
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13152  tgval2 16366
[Munkres] p. 79Remarktgcl 16379
[Munkres] p. 80Lemma 2.1tgval3 16373
[Munkres] p. 80Lemma 2.2tgss2 16397  tgss3 16396
[Munkres] p. 81Lemma 2.3basgen 16398  basgen2 16399
[Munkres] p. 89Definition of subspace topologyresttop 16563
[Munkres] p. 93Theorem 6.1(1)0cld 16447  topcld 16444
[Munkres] p. 93Theorem 6.1(2)iincld 16448
[Munkres] p. 93Theorem 6.1(3)uncld 16450
[Munkres] p. 94Definition of closureclsval 16446
[Munkres] p. 94Definition of interiorntrval 16445
[Munkres] p. 95Theorem 6.5(a)clsndisj 16484  elcls 16482
[Munkres] p. 95Theorem 6.5(b)elcls3 16492
[Munkres] p. 97Theorem 6.6clslp 16551  neindisj 16526
[Munkres] p. 97Corollary 6.7cldlp 16553
[Munkres] p. 97Definition of limit pointislp2 16549  lpval 16543
[Munkres] p. 98Definition of Hausdorff spacedf-haus 16715
[Munkres] p. 102Definition of continuous functiondf-cn 16629  iscn 16637  iscn2 16640
[Munkres] p. 107Theorem 7.2(g)cncnp 16681  cncnp2 16682  cncnpi 16679  df-cnp 16630  iscnp 16639  iscnp2 16641
[Munkres] p. 127Theorem 10.1metcn 17761
[Munkres] p. 128Theorem 10.3metcn4 18408
[NielsenChuang] p. 195Equation 4.73unierri 22309
[Ponnusamy] p. 361Theorem 6.44cphip0l 18309  df-dip 20899  dip0l 20919  ip0l 16212
[Ponnusamy] p. 361Equation 6.45ipval 20901
[Ponnusamy] p. 362Equation I1dipcj 20915
[Ponnusamy] p. 362Equation I3cphdir 18312  dipdir 21045  ipdir 16215  ipdiri 21033
[Ponnusamy] p. 362Equation I4ipidsq 20911
[Ponnusamy] p. 362Equation 6.46ip0i 21028
[Ponnusamy] p. 362Equation 6.47ip1i 21030
[Ponnusamy] p. 362Equation 6.48ip2i 21031
[Ponnusamy] p. 363Equation I2cphass 18318  dipass 21048  ipass 16221  ipassi 21044
[Prugovecki] p. 186Definition of brabraval 22149  df-bra 22055
[Prugovecki] p. 376Equation 8.1df-kb 22056  kbval 22159
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22587
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 28507
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22601  atcvat4i 22602  cvrat3 28061  cvrat4 28062  lsatcvat3 27672
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22487  cvrval 27889  df-cv 22484  df-lcv 27639  lspsncv0 15573
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 28519
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 28520
[Quine] p. 16Definition 2.1df-clab 2228  rabid 2661
[Quine] p. 17Definition 2.1''dfsb7 2067
[Quine] p. 18Definition 2.7df-cleq 2234
[Quine] p. 19Definition 2.9conventions 3  df-v 2714
[Quine] p. 34Theorem 5.1abeq2 2342
[Quine] p. 35Theorem 5.2abid2 2354  abid2f 2398
[Quine] p. 40Theorem 6.1sb5 1981
[Quine] p. 40Theorem 6.2sb56 1979  sb6 1980
[Quine] p. 41Theorem 6.3df-clel 2237
[Quine] p. 41Theorem 6.4eqid 2241  eqid1 20465
[Quine] p. 41Theorem 6.5eqcom 2243
[Quine] p. 42Theorem 6.6df-sbc 2907
[Quine] p. 42Theorem 6.7dfsbcq 2908  dfsbcq2 2909
[Quine] p. 43Theorem 6.8vex 2715
[Quine] p. 43Theorem 6.9isset 2716
[Quine] p. 44Theorem 7.3cla4gf 2786  cla4gv 2790  cla4imgf 2784
[Quine] p. 44Theorem 6.11a4sbc 2916
[Quine] p. 44Theorem 6.12elex 2720
[Quine] p. 44Theorem 6.13elab 2836  elabg 2837  elabgf 2834
[Quine] p. 44Theorem 6.14noel 3346
[Quine] p. 48Theorem 7.2snprc 3579
[Quine] p. 48Definition 7.1df-pr 3531  df-sn 3530
[Quine] p. 49Theorem 7.4snss 3632  snssg 3636
[Quine] p. 49Theorem 7.5prss 3649  prssg 3650
[Quine] p. 49Theorem 7.6prid1 3618  prid1g 3616  prid2 3619  prid2g 3617  snid 3551  snidg 3549
[Quine] p. 51Theorem 7.13prex 4090  snex 4089  snexALT 4069
[Quine] p. 53Theorem 8.2unisn 3723  unisnALT 27133  unisng 3724
[Quine] p. 53Theorem 8.3uniun 3726
[Quine] p. 54Theorem 8.6elssuni 3733
[Quine] p. 54Theorem 8.7uni0 3732
[Quine] p. 56Theorem 8.17uniabio 6127
[Quine] p. 56Definition 8.18dfiota2 6118
[Quine] p. 57Theorem 8.19iotaval 6128
[Quine] p. 57Theorem 8.22iotanul 6132
[Quine] p. 58Theorem 8.23iotaex 6134
[Quine] p. 58Definition 9.1df-op 3533
[Quine] p. 61Theorem 9.5opabid 4143  opelopab 4158  opelopaba 4153  opelopabaf 4160  opelopabf 4161  opelopabg 4155  opelopabga 4150  oprabid 5709
[Quine] p. 64Definition 9.11df-xp 4573
[Quine] p. 64Definition 9.12df-cnv 4575
[Quine] p. 64Definition 9.15df-id 4181
[Quine] p. 65Theorem 10.3fun0 5143
[Quine] p. 65Theorem 10.4funi 5121
[Quine] p. 65Theorem 10.5funsn 5136  funsng 5134
[Quine] p. 65Definition 10.1df-fun 4581
[Quine] p. 65Definition 10.2args 4927  df-fv 4587
[Quine] p. 68Definition 10.11conventions 3  df-fv 4587  fv2 5348
[Quine] p. 124Theorem 17.3nn0opth2 11101  nn0opth2i 11100  nn0opthi 11099  omopthi 6515
[Quine] p. 177Definition 25.2df-rdg 6283
[Quine] p. 232Equation icarddom 8032
[Quine] p. 284Axiom 39(vi)funimaex 5166  funimaexg 5165
[Quine] p. 331Axiom system NFru 2905
[ReedSimon] p. 36Definition (iii)ax-his3 21288
[ReedSimon] p. 63Exercise 4(a)df-dip 20899  polid 21363  polid2i 21361  polidi 21362
[ReedSimon] p. 63Exercise 4(b)df-ph 21016
[ReedSimon] p. 195Remarklnophm 22224  lnophmi 22223
[Retherford] p. 49Exercise 1(i)leopadd 22337
[Retherford] p. 49Exercise 1(ii)leopmul 22339  leopmuli 22338
[Retherford] p. 49Exercise 1(iv)leoptr 22342
[Retherford] p. 49Definition VI.1df-leop 22057  leoppos 22331
[Retherford] p. 49Exercise 1(iii)leoptri 22341
[Retherford] p. 49Definition of operator orderingleop3 22330
[Rudin] p. 164Equation 27efcan 12184
[Rudin] p. 164Equation 30efzval 12190
[Rudin] p. 167Equation 48absefi 12284
[Sanford] p. 39Rule 3mtp-xor 1519
[Sanford] p. 39Rule 4mpto2 1518
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 9
[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 166
[Sanford] p. 40Rule 1mpto1 1517
[Schechter] p. 51Definition of antisymmetryintasym 4944
[Schechter] p. 51Definition of irreflexivityintirr 4947
[Schechter] p. 51Definition of symmetrycnvsym 4943
[Schechter] p. 51Definition of transitivitycotr 4941
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13295
[Schechter] p. 79Definition of Moore closuredf-mrc 13296
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13297
[Schechter] p. 139Definition AC3dfac9 7620
[Schechter] p. 141Definition (MC)dfac11 26126
[Schechter] p. 149Axiom DC1ax-dc 7930  axdc3 7938
[Schechter] p. 187Definition of ring with unitisrng 15020  isrngo 20670
[Schechter] p. 276Remark 11.6.espan0 21746
[Schechter] p. 276Definition of spandf-span 21513  spanval 21537
[Schechter] p. 428Definition 15.35bastop1 16403
[Schwabhauser] p. 10Axiom A1axcgrrflx 23516
[Schwabhauser] p. 10Axiom A2axcgrtr 23517
[Schwabhauser] p. 10Axiom A3axcgrid 23518
[Schwabhauser] p. 11Axiom A4axsegcon 23529
[Schwabhauser] p. 11Axiom A5ax5seg 23540
[Schwabhauser] p. 11Axiom A6axbtwnid 23541
[Schwabhauser] p. 12Axiom A7axpasch 23543
[Schwabhauser] p. 12Axiom A8axlowdim2 23562
[Schwabhauser] p. 13Axiom A10axeuclid 23565
[Schwabhauser] p. 13Axiom A11axcont 23578
[Schwabhauser] p. 27Theorem 2.1cgrrflx 23584
[Schwabhauser] p. 27Theorem 2.2cgrcomim 23586
[Schwabhauser] p. 27Theorem 2.3cgrtr 23589
[Schwabhauser] p. 27Theorem 2.4cgrcoml 23593
[Schwabhauser] p. 27Theorem 2.5cgrcomr 23594
[Schwabhauser] p. 28Theorem 2.8cgrtriv 23599
[Schwabhauser] p. 28Theorem 2.105segofs 23603
[Schwabhauser] p. 28Definition 2.10df-ofs 23580
[Schwabhauser] p. 29Theorem 2.11cgrextend 23605
[Schwabhauser] p. 29Theorem 2.12segconeq 23607
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 23619  btwntriv2 23609
[Schwabhauser] p. 30Theorem 3.2btwncomim 23610
[Schwabhauser] p. 30Theorem 3.3btwntriv1 23613
[Schwabhauser] p. 30Theorem 3.4btwnswapid 23614
[Schwabhauser] p. 30Theorem 3.5btwnexch2 23620  btwnintr 23616
[Schwabhauser] p. 30Theorem 3.6btwnexch 23622  btwnexch3 23617
[Schwabhauser] p. 30Theorem 3.7btwnouttr 23621
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23561
[Schwabhauser] p. 32Theorem 3.14btwndiff 23624
[Schwabhauser] p. 33Theorem 3.17trisegint 23625
[Schwabhauser] p. 34Theorem 4.2ifscgr 23641
[Schwabhauser] p. 34Definition 4.1df-ifs 23636
[Schwabhauser] p. 35Theorem 4.3cgrsub 23642
[Schwabhauser] p. 35Theorem 4.5cgrxfr 23652
[Schwabhauser] p. 35Definition 4.4df-cgr3 23637
[Schwabhauser] p. 36Theorem 4.6btwnxfr 23653
[Schwabhauser] p. 36Theorem 4.11colinearperm1 23659  colinearperm2 23661  colinearperm3 23660  colinearperm4 23662  colinearperm5 23663
[Schwabhauser] p. 36Definition 4.10df-colinear 23638
[Schwabhauser] p. 37Theorem 4.12colineartriv1 23664
[Schwabhauser] p. 37Theorem 4.13colinearxfr 23672
[Schwabhauser] p. 37Theorem 4.14lineext 23673
[Schwabhauser] p. 37Theorem 4.16fscgr 23677
[Schwabhauser] p. 37Theorem 4.17linecgr 23678
[Schwabhauser] p. 37Definition 4.15df-fs 23639
[Schwabhauser] p. 38Theorem 4.18lineid 23680
[Schwabhauser] p. 38Theorem 4.19idinside 23681
[Schwabhauser] p. 39Theorem 5.1btwnconn1 23698
[Schwabhauser] p. 41Theorem 5.2btwnconn2 23699
[Schwabhauser] p. 41Theorem 5.3btwnconn3 23700
[Schwabhauser] p. 41Theorem 5.5brsegle2 23706
[Schwabhauser] p. 41Definition 5.4df-segle 23704
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 23707
[Schwabhauser] p. 42Theorem 5.7seglerflx 23709
[Schwabhauser] p. 42Theorem 5.8segletr 23711
[Schwabhauser] p. 42Theorem 5.9segleantisym 23712
[Schwabhauser] p. 42Theorem 5.10seglelin 23713
[Schwabhauser] p. 42Theorem 5.11seglemin 23710
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 23715
[Schwabhauser] p. 43Theorem 6.2btwnoutside 23722
[Schwabhauser] p. 43Theorem 6.3broutsideof3 23723
[Schwabhauser] p. 43Theorem 6.4broutsideof 23718  df-outsideof 23717
[Schwabhauser] p. 43Definition 6.1broutsideof2 23719
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 23724
[Schwabhauser] p. 44Theorem 6.6outsideofcom 23725
[Schwabhauser] p. 44Theorem 6.7outsideoftr 23726
[Schwabhauser] p. 44Theorem 6.11outsideofeu 23728
[Schwabhauser] p. 44Definition 6.8df-ray 23735
[Schwabhauser] p. 45Part 2df-lines2 23736
[Schwabhauser] p. 45Theorem 6.13outsidele 23729
[Schwabhauser] p. 45Theorem 6.15lineunray 23744
[Schwabhauser] p. 45Theorem 6.16lineelsb2 23745
[Schwabhauser] p. 45Theorem 6.17linecom 23747  linerflx1 23746  linerflx2 23748
[Schwabhauser] p. 45Theorem 6.18linethru 23750
[Schwabhauser] p. 45Definition 6.14df-line2 23734
[Schwabhauser] p. 46Theorem 6.19linethrueu 23753
[Schwabhauser] p. 46Theorem 6.21lineintmo 23754
[Shapiro] p. 230Theorem 6.5.1dchrhash 20154  dchrsum 20152  dchrsum2 20151  sumdchr 20155
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20156  sum2dchr 20157
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 14976  ablfacrp2 14977
[Shapiro], p. 328Equation 9.2.4vmasum 20099
[Shapiro], p. 329Equation 9.2.7logfac2 20100
[Shapiro], p. 329Equation 9.2.9logfacrlim 20107
[Shapiro], p. 331Equation 9.2.13vmadivsum 20275
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20278
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20332  vmalogdivsum2 20331
[Shapiro], p. 375Theorem 9.4.1dirith 20322  dirith2 20321
[Shapiro], p. 375Equation 9.4.3rplogsum 20320  rpvmasum 20319  rpvmasum2 20305
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20280
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20318
[Shapiro], p. 377Lemma 9.4.1dchrisum 20285  dchrisumlem1 20282  dchrisumlem2 20283  dchrisumlem3 20284  dchrisumlema 20281
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20288
[Shapiro], p. 379Equation 9.4.16dchrmusum 20317  dchrmusumlem 20315  dchrvmasumlem 20316
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20287
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20289
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20313  dchrisum0re 20306  dchrisumn0 20314
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20299
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20303
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20304
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20359  pntrsumbnd2 20360  pntrsumo1 20358
[Shapiro], p. 405Equation 10.2.1mudivsum 20323
[Shapiro], p. 406Equation 10.2.6mulogsum 20325
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20327
[Shapiro], p. 407Equation 10.2.8mulog2sum 20330
[Shapiro], p. 418Equation 10.4.6logsqvma 20335
[Shapiro], p. 418Equation 10.4.8logsqvma2 20336
[Shapiro], p. 419Equation 10.4.10selberg 20341
[Shapiro], p. 420Equation 10.4.12selberg2lem 20343
[Shapiro], p. 420Equation 10.4.14selberg2 20344
[Shapiro], p. 422Equation 10.6.7selberg3 20352
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20353
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20350  selberg3lem2 20351
[Shapiro], p. 422Equation 10.4.23selberg4 20354
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20348
[Shapiro], p. 428Equation 10.6.2selbergr 20361
[Shapiro], p. 429Equation 10.6.8selberg3r 20362
[Shapiro], p. 430Equation 10.6.11selberg4r 20363
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20377
[Shapiro], p. 434Equation 10.6.27pntlema 20389  pntlemb 20390  pntlemc 20388  pntlemd 20387  pntlemg 20391
[Shapiro], p. 435Equation 10.6.29pntlema 20389
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20381
[Shapiro], p. 436Lemma 10.6.2pntibnd 20386
[Shapiro], p. 436Equation 10.6.34pntlema 20389
[Shapiro], p. 436Equation 10.6.35pntlem3 20402  pntleml 20404
[Stoll] p. 13Definition of symmetric differencesymdif1 3320
[Stoll] p. 16Exercise 4.40dif 3411  dif0 3410
[Stoll] p. 16Exercise 4.8difdifdir 3427
[Stoll] p. 17Theorem 5.1(5)undifv 3414
[Stoll] p. 19Theorem 5.2(13)undm 3313
[Stoll] p. 19Theorem 5.2(13')indm 3314
[Stoll] p. 20Remarkinvdif 3297
[Stoll] p. 25Definition of ordered tripledf-ot 3534
[Stoll] p. 43Definitionuniiun 3833
[Stoll] p. 44Definitionintiin 3834
[Stoll] p. 45Definitiondf-iin 3786
[Stoll] p. 45Definition indexed uniondf-iun 3785
[Stoll] p. 176Theorem 3.4(27)iman 411
[Stoll] p. 262Example 4.1symdif1 3320
[Strang] p. 242Section 6.3expgrowth 26518
[Suppes] p. 22Theorem 2eq0 3356
[Suppes] p. 22Theorem 4eqss 3095  eqssd 3097  eqssi 3096
[Suppes] p. 23Theorem 5ss0 3372  ss0b 3371
[Suppes] p. 23Theorem 6sstr 3088  sstrALT2 27042
[Suppes] p. 23Theorem 7pssirr 3176
[Suppes] p. 23Theorem 8pssn2lp 3177
[Suppes] p. 23Theorem 9psstr 3180
[Suppes] p. 23Theorem 10pssss 3172
[Suppes] p. 25Theorem 12elin 3246  elun 3206
[Suppes] p. 26Theorem 15inidm 3265
[Suppes] p. 26Theorem 16in0 3367
[Suppes] p. 27Theorem 23unidm 3208
[Suppes] p. 27Theorem 24un0 3366
[Suppes] p. 27Theorem 25ssun1 3228
[Suppes] p. 27Theorem 26ssequn1 3235
[Suppes] p. 27Theorem 27unss 3239
[Suppes] p. 27Theorem 28indir 3304
[Suppes] p. 27Theorem 29undir 3305
[Suppes] p. 28Theorem 32difid 3408  difidALT 3409
[Suppes] p. 29Theorem 33difin 3293
[Suppes] p. 29Theorem 34indif 3298
[Suppes] p. 29Theorem 35undif1 3415
[Suppes] p. 29Theorem 36difun2 3419
[Suppes] p. 29Theorem 37difin0 3413
[Suppes] p. 29Theorem 38disjdif 3412
[Suppes] p. 29Theorem 39difundi 3308
[Suppes] p. 29Theorem 40difindi 3310
[Suppes] p. 30Theorem 41nalset 4027
[Suppes] p. 39Theorem 61uniss 3728
[Suppes] p. 39Theorem 65uniop 4141
[Suppes] p. 41Theorem 70intsn 3776
[Suppes] p. 42Theorem 71intpr 3773  intprg 3774
[Suppes] p. 42Theorem 73op1stb 4439
[Suppes] p. 42Theorem 78intun 3772
[Suppes] p. 44Definition 15(a)dfiun2 3815  dfiun2g 3813
[Suppes] p. 44Definition 15(b)dfiin2 3816
[Suppes] p. 47Theorem 86elpw 3516  elpw2 4043  elpw2g 4042  elpwg 3517  elpwgdedVD 27124
[Suppes] p. 47Theorem 87pwid 3522
[Suppes] p. 47Theorem 89pw0 3642
[Suppes] p. 48Theorem 90pwpw0 3643
[Suppes] p. 52Theorem 101xpss12 4678
[Suppes] p. 52Theorem 102xpindi 4705  xpindir 4706
[Suppes] p. 52Theorem 103xpundi 4627  xpundir 4628
[Suppes] p. 54Theorem 105elirrv 7169
[Suppes] p. 58Theorem 2relss 4661
[Suppes] p. 59Theorem 4eldm 4762  eldm2 4763  eldm2g 4761  eldmg 4760
[Suppes] p. 59Definition 3df-dm 4577
[Suppes] p. 60Theorem 6dmin 4772
[Suppes] p. 60Theorem 8rnun 4975
[Suppes] p. 60Theorem 9rnin 4976
[Suppes] p. 60Definition 4dfrn2 4754
[Suppes] p. 61Theorem 11brcnv 4750  brcnvg 4748
[Suppes] p. 62Equation 5elcnv 4744  elcnv2 4745
[Suppes] p. 62Theorem 12relcnv 4937
[Suppes] p. 62Theorem 15cnvin 4974
[Suppes] p. 62Theorem 16cnvun 4972
[Suppes] p. 63Theorem 20co02 5071
[Suppes] p. 63Theorem 21dmcoss 4830
[Suppes] p. 63Definition 7df-co 4576
[Suppes] p. 64Theorem 26cnvco 4751
[Suppes] p. 64Theorem 27coass 5076
[Suppes] p. 65Theorem 31resundi 4855
[Suppes] p. 65Theorem 34elima 4903  elima2 4904  elima3 4905  elimag 4902
[Suppes] p. 65Theorem 35imaundi 4979
[Suppes] p. 66Theorem 40dminss 4981
[Suppes] p. 66Theorem 41imainss 4982
[Suppes] p. 67Exercise 11cnvxp 4983
[Suppes] p. 81Definition 34dfec2 6523
[Suppes] p. 82Theorem 72elec 6559  elecg 6558
[Suppes] p. 82Theorem 73erth 6564  erth2 6565
[Suppes] p. 83Theorem 74erdisj 6567
[Suppes] p. 89Theorem 96map0b 6666
[Suppes] p. 89Theorem 97map0 6668  map0g 6667
[Suppes] p. 89Theorem 98mapsn 6669
[Suppes] p. 89Theorem 99mapss 6670
[Suppes] p. 91Definition 12(ii)alephsuc 7553
[Suppes] p. 91Definition 12(iii)alephlim 7552
[Suppes] p. 92Theorem 1enref 6754  enrefg 6753
[Suppes] p. 92Theorem 2ensym 6770  ensymb 6769  ensymi 6771
[Suppes] p. 92Theorem 3entr 6772
[Suppes] p. 92Theorem 4unen 6802
[Suppes] p. 94Theorem 15endom 6748
[Suppes] p. 94Theorem 16ssdomg 6767
[Suppes] p. 94Theorem 17domtr 6773
[Suppes] p. 95Theorem 18sbth 6840
[Suppes] p. 97Theorem 23canth2 6873  canth2g 6874
[Suppes] p. 97Definition 3brsdom2 6844  df-sdom 6726  dfsdom2 6843
[Suppes] p. 97Theorem 21(i)sdomirr 6857
[Suppes] p. 97Theorem 22(i)domnsym 6846
[Suppes] p. 97Theorem 21(ii)sdomnsym 6845
[Suppes] p. 97Theorem 22(ii)domsdomtr 6855
[Suppes] p. 97Theorem 22(iv)brdom2 6751
[Suppes] p. 97Theorem 21(iii)sdomtr 6858
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6853
[Suppes] p. 98Exercise 4fundmen 6793  fundmeng 6794
[Suppes] p. 98Exercise 6xpdom3 6819
[Suppes] p. 98Exercise 11sdomentr 6854
[Suppes] p. 104Theorem 37fofi 7001
[Suppes] p. 104Theorem 38pwfi 7009
[Suppes] p. 105Theorem 40pwfi 7009
[Suppes] p. 111Axiom for cardinal numberscarden 8029
[Suppes] p. 130Definition 3df-tr 3990
[Suppes] p. 132Theorem 9ssonuni 4448
[Suppes] p. 134Definition 6df-suc 4270
[Suppes] p. 136Theorem Schema 22findes 4556  finds 4552  finds1 4555  finds2 4554
[Suppes] p. 151Theorem 42isfinite 7211  isfinite2 6974  isfiniteg 6976  unbnn 6972
[Suppes] p. 162Definition 5df-ltnq 8396  df-ltpq 8388
[Suppes] p. 197Theorem Schema 4tfindes 4523  tfinds 4520  tfinds2 4524
[Suppes] p. 209Theorem 18oaord1 6409
[Suppes] p. 209Theorem 21oaword2 6411
[Suppes] p. 211Theorem 25oaass 6419
[Suppes] p. 225Definition 8iscard2 7467
[Suppes] p. 227Theorem 56ondomon 8041
[Suppes] p. 228Theorem 59harcard 7469
[Suppes] p. 228Definition 12(i)aleph0 7551
[Suppes] p. 228Theorem Schema 61onintss 4314
[Suppes] p. 228Theorem Schema 62onminesb 4459  onminsb 4460
[Suppes] p. 229Theorem 64alephval2 8048
[Suppes] p. 229Theorem 65alephcard 7555
[Suppes] p. 229Theorem 66alephord2i 7562
[Suppes] p. 229Theorem 67alephnbtwn 7556
[Suppes] p. 229Definition 12df-aleph 7431
[Suppes] p. 242Theorem 6weth 7980
[Suppes] p. 242Theorem 8entric 8035
[Suppes] p. 242Theorem 9carden 8029
[TakeutiZaring] p. 8Axiom 1ax-ext 2222
[TakeutiZaring] p. 13Definition 4.5df-cleq 2234
[TakeutiZaring] p. 13Proposition 4.6df-clel 2237
[TakeutiZaring] p. 13Proposition 4.9cvjust 2236
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2258
[TakeutiZaring] p. 14Definition 4.16df-oprab 5689
[TakeutiZaring] p. 14Proposition 4.14ru 2905
[TakeutiZaring] p. 15Axiom 2zfpair 4085
[TakeutiZaring] p. 15Exercise 1elpr 3542  elpr2 3543  elprg 3541
[TakeutiZaring] p. 15Exercise 2elsn 3539  elsnc 3547  elsnc2 3553  elsnc2g 3552  elsncg 3546
[TakeutiZaring] p. 15Exercise 3elop 4111
[TakeutiZaring] p. 15Exercise 4sneq 3535  sneqr 3660
[TakeutiZaring] p. 15Definition 5.1dfpr2 3540  dfsn2 3538
[TakeutiZaring] p. 16Axiom 3uniex 4386
[TakeutiZaring] p. 16Exercise 6opth 4117
[TakeutiZaring] p. 16Exercise 7opex 4109
[TakeutiZaring] p. 16Exercise 8rext 4095
[TakeutiZaring] p. 16Corollary 5.8unex 4388  unexg 4391
[TakeutiZaring] p. 16Definition 5.3dftp2 3563
[TakeutiZaring] p. 16Definition 5.5df-uni 3708
[TakeutiZaring] p. 16Definition 5.6df-in 3065  df-un 3063
[TakeutiZaring] p. 16Proposition 5.7unipr 3721  uniprg 3722
[TakeutiZaring] p. 17Axiom 4pwex 4066  pwexg 4067
[TakeutiZaring] p. 17Exercise 1eltp 3562
[TakeutiZaring] p. 17Exercise 5elsuc 4333  elsucg 4331  sstr2 3087
[TakeutiZaring] p. 17Exercise 6uncom 3209
[TakeutiZaring] p. 17Exercise 7incom 3249
[TakeutiZaring] p. 17Exercise 8unass 3222
[TakeutiZaring] p. 17Exercise 9inass 3266
[TakeutiZaring] p. 17Exercise 10indi 3302
[TakeutiZaring] p. 17Exercise 11undi 3303
[TakeutiZaring] p. 17Definition 5.9df-pss 3071  dfss2 3072
[TakeutiZaring] p. 17Definition 5.10df-pw 3512
[TakeutiZaring] p. 18Exercise 7unss2 3236
[TakeutiZaring] p. 18Exercise 9df-ss 3069  sseqin2 3275
[TakeutiZaring] p. 18Exercise 10ssid 3098
[TakeutiZaring] p. 18Exercise 12inss1 3276  inss2 3277
[TakeutiZaring] p. 18Exercise 13nss 3137
[TakeutiZaring] p. 18Exercise 15unieq 3716
[TakeutiZaring] p. 18Exercise 18sspwb 4096  sspwimp 27125  sspwimpALT 27132  sspwimpALT2 27136  sspwimpcf 27127
[TakeutiZaring] p. 18Exercise 19pweqb 4103
[TakeutiZaring] p. 19Axiom 5ax-rep 4007
[TakeutiZaring] p. 20Definitiondf-rab 2502
[TakeutiZaring] p. 20Corollary 5.160ex 4026
[TakeutiZaring] p. 20Definition 5.12df-dif 3061
[TakeutiZaring] p. 20Definition 5.14dfnul2 3344
[TakeutiZaring] p. 20Proposition 5.15difid 3408  difidALT 3409
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3351  n0f 3350  neq0 3352
[TakeutiZaring] p. 21Axiom 6zfreg 7167
[TakeutiZaring] p. 21Axiom 6'zfregs 7272
[TakeutiZaring] p. 21Theorem 5.22setind 7277
[TakeutiZaring] p. 21Definition 5.20df-v 2714
[TakeutiZaring] p. 21Proposition 5.21vprc 4028
[TakeutiZaring] p. 22Exercise 10ss 3370
[TakeutiZaring] p. 22Exercise 3ssex 4034  ssexg 4036
[TakeutiZaring] p. 22Exercise 4inex1 4031
[TakeutiZaring] p. 22Exercise 5ruv 7172
[TakeutiZaring] p. 22Exercise 6elirr 7170
[TakeutiZaring] p. 22Exercise 7ssdif0 3400
[TakeutiZaring] p. 22Exercise 11difdif 3199
[TakeutiZaring] p. 22Exercise 13undif3 3316  undif3VD 27089
[TakeutiZaring] p. 22Exercise 14difss 3200
[TakeutiZaring] p. 22Exercise 15sscon 3204
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2499
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2500
[TakeutiZaring] p. 23Proposition 6.2xpex 4687  xpexg 4686  xpexgALT 5896
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4574
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5148
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5280  fun11 5151
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5104  svrelfun 5149
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4753
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4755
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4579
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4580
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4576
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5014  dfrel2 5010
[TakeutiZaring] p. 25Exercise 3xpss 4679
[TakeutiZaring] p. 25Exercise 5relun 4688
[TakeutiZaring] p. 25Exercise 6reluni 4694
[TakeutiZaring] p. 25Exercise 9inxp 4704
[TakeutiZaring] p. 25Exercise 12relres 4869
[TakeutiZaring] p. 25Exercise 13opelres 4846  opelresg 4848
[TakeutiZaring] p. 25Exercise 14dmres 4862
[TakeutiZaring] p. 25Exercise 15resss 4865
[TakeutiZaring] p. 25Exercise 17resabs1 4870
[TakeutiZaring] p. 25Exercise 18funres 5129
[TakeutiZaring] p. 25Exercise 24relco 5056
[TakeutiZaring] p. 25Exercise 29funco 5128
[TakeutiZaring] p. 25Exercise 30f1co 5281
[TakeutiZaring] p. 26Definition 6.10eu2 2126
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 4587  fv3 5368
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5094  cnvexg 5093
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4827  dmexg 4825
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4828  rnexg 4826
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 26625
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 26626
[TakeutiZaring] p. 27Corollary 6.13fvex 5366
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5371  tz6.12 5372  tz6.12c 5375
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5374  tz6.12i 5376
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4582
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4583
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4585  wfo 4569
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4584  wf1 4568
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4586  wf1o 4570
[TakeutiZaring] p. 28Exercise 4eqfnfv 5449  eqfnfv2 5450  eqfnfv2f 5453
[TakeutiZaring] p. 28Exercise 5fvco 5422
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5568  fnexALT 5569
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5564  resfunexgALT 5565
[TakeutiZaring] p. 29Exercise 9funimaex 5166  funimaexg 5165
[TakeutiZaring] p. 29Definition 6.18df-br 3901
[TakeutiZaring] p. 30Definition 6.21dffr2 4230  dffr3 4931  eliniseg 4928  iniseg 4930
[TakeutiZaring] p. 30Definition 6.22df-eprel 4177
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4243  fr3nr 4441  frirr 4242
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4224
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4443
[TakeutiZaring] p. 31Exercise 1frss 4232
[TakeutiZaring] p. 31Exercise 4wess 4252
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23173  tz6.26i 23174  wefrc 4259  wereu2 4262
[TakeutiZaring] p. 32Theorem 6.27wfi 23175  wfii 23176
[TakeutiZaring] p. 32Definition 6.28df-isom 4588
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5653
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5654
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5660
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5661
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5662
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5666
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5673
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5675
[TakeutiZaring] p. 35Notationwtr 3989
[TakeutiZaring] p. 35Theorem 7.2trelpss 26627  tz7.2 4249
[TakeutiZaring] p. 35Definition 7.1dftr3 3993
[TakeutiZaring] p. 36Proposition 7.4ordwe 4277
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4285
[TakeutiZaring] p. 36Proposition 7.6ordelord 4286  ordelordALT 26783  ordelordALTVD 27074
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4292  ordelssne 4291
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4290
[TakeutiZaring] p. 37Proposition 7.9ordin 4294
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4450
[TakeutiZaring] p. 38Corollary 7.15ordsson 4451
[TakeutiZaring] p. 38Definition 7.11df-on 4268
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4296
[TakeutiZaring] p. 38Proposition 7.12onfrALT 26796  ordon 4444
[TakeutiZaring] p. 38Proposition 7.13onprc 4446
[TakeutiZaring] p. 39Theorem 7.17tfi 4514
[TakeutiZaring] p. 40Exercise 3ontr2 4311
[TakeutiZaring] p. 40Exercise 7dftr2 3991
[TakeutiZaring] p. 40Exercise 9onssmin 4458
[TakeutiZaring] p. 40Exercise 11unon 4492
[TakeutiZaring] p. 40Exercise 12ordun 4364
[TakeutiZaring] p. 40Exercise 14ordequn 4363
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4447
[TakeutiZaring] p. 40Proposition 7.20elssuni 3733
[TakeutiZaring] p. 41Definition 7.22df-suc 4270
[TakeutiZaring] p. 41Proposition 7.23sssucid 4341  sucidg 4342
[TakeutiZaring] p. 41Proposition 7.24suceloni 4474
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4356  ordnbtwn 4355
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4489
[TakeutiZaring] p. 42Exercise 1df-lim 4269
[TakeutiZaring] p. 42Exercise 4omssnlim 4540
[TakeutiZaring] p. 42Exercise 7ssnlim 4544
[TakeutiZaring] p. 42Exercise 8onsucssi 4502  ordelsuc 4481
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4483
[TakeutiZaring] p. 42Definition 7.27nlimon 4512
[TakeutiZaring] p. 42Definition 7.28dfom2 4528
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4545
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4546
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4547
[TakeutiZaring] p. 43Remarkomon 4537
[TakeutiZaring] p. 43Axiom 7inf3 7194  omex 7202
[TakeutiZaring] p. 43Theorem 7.32ordom 4535
[TakeutiZaring] p. 43Corollary 7.31find 4551
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4548
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4549
[TakeutiZaring] p. 44Exercise 1limomss 4531
[TakeutiZaring] p. 44Exercise 2int0 3754  trint0 4006
[TakeutiZaring] p. 44Exercise 4intss1 3755
[TakeutiZaring] p. 44Exercise 5intex 4044
[TakeutiZaring] p. 44Exercise 6oninton 4461
[TakeutiZaring] p. 44Exercise 11ordintdif 4313
[TakeutiZaring] p. 44Definition 7.35df-int 3741
[TakeutiZaring] p. 44Proposition 7.34noinfep 7218
[TakeutiZaring] p. 45Exercise 4onint 4456
[TakeutiZaring] p. 47Lemma 1tfrlem1 6251
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6273
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6274
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6275
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6279  tz7.44-2 6280  tz7.44-3 6281
[TakeutiZaring] p. 50Exercise 1smogt 6244
[TakeutiZaring] p. 50Exercise 3smoiso 6239
[TakeutiZaring] p. 50Definition 7.46df-smo 6223
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6317  tz7.49c 6318
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6315
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6314
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6316
[TakeutiZaring] p. 53Proposition 7.532eu5 2185
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7497
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7498
[TakeutiZaring] p. 56Definition 8.1oalim 6391  oasuc 6383
[TakeutiZaring] p. 57Remarktfindsg 4521
[TakeutiZaring] p. 57Proposition 8.2oacl 6394
[TakeutiZaring] p. 57Proposition 8.3oa0 6375  oa0r 6397
[TakeutiZaring] p. 57Proposition 8.16omcl 6395
[TakeutiZaring] p. 58Corollary 8.5oacan 6406
[TakeutiZaring] p. 58Proposition 8.4nnaord 6477  nnaordi 6476  oaord 6405  oaordi 6404
[TakeutiZaring] p. 59Proposition 8.6iunss2 3825  uniss2 3736
[TakeutiZaring] p. 59Proposition 8.7oawordri 6408
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6413  oawordex 6415
[TakeutiZaring] p. 59Proposition 8.9nnacl 6469
[TakeutiZaring] p. 59Proposition 8.10oaabs 6502
[TakeutiZaring] p. 60Remarkoancom 7210
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6418
[TakeutiZaring] p. 62Exercise 1nnarcl 6474
[TakeutiZaring] p. 62Exercise 5oaword1 6410
[TakeutiZaring] p. 62Definition 8.15om0 6376  om0x 6378  omlim 6392  omsuc 6385
[TakeutiZaring] p. 63Proposition 8.17nnecl 6471  nnmcl 6470
[TakeutiZaring] p. 63Proposition 8.19nnmord 6490  nnmordi 6489  omord 6426  omordi 6424
[TakeutiZaring] p. 63Proposition 8.20omcan 6427
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6494  omwordri 6430
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6398
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6400  om1r 6401
[TakeutiZaring] p. 64Proposition 8.22om00 6433
[TakeutiZaring] p. 64Proposition 8.23omordlim 6435
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6436
[TakeutiZaring] p. 64Proposition 8.25odi 6437
[TakeutiZaring] p. 65Theorem 8.26omass 6438
[TakeutiZaring] p. 67Definition 8.30nnesuc 6466  oe0 6381  oelim 6393  oesuc 6386  onesuc 6389
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6379
[TakeutiZaring] p. 67Proposition 8.32oen0 6444
[TakeutiZaring] p. 67Proposition 8.33oeordi 6445
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6380
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6403
[TakeutiZaring] p. 68Corollary 8.34oeord 6446
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6452
[TakeutiZaring] p. 68Proposition 8.35oewordri 6450
[TakeutiZaring] p. 68Proposition 8.37oeworde 6451
[TakeutiZaring] p. 69Proposition 8.41oeoa 6455
[TakeutiZaring] p. 70Proposition 8.42oeoe 6457
[TakeutiZaring] p. 73Theorem 9.1trcl 7268  tz9.1 7269
[TakeutiZaring] p. 76Definition 9.9df-r1 7294  r10 7298  r1lim 7302  r1limg 7301  r1suc 7300  r1sucg 7299
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7310  r1ord2 7311  r1ordg 7308
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7320
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7345  tz9.13 7321  tz9.13g 7322
[TakeutiZaring] p. 79Definition 9.14df-rank 7295  rankval 7346  rankvalb 7327  rankvalg 7347
[TakeutiZaring] p. 79Proposition 9.16rankel 7369  rankelb 7354
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7383  rankval3 7370  rankval3b 7356
[TakeutiZaring] p. 79Proposition 9.18rankonid 7359
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7325
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7364  rankr1c 7351  rankr1g 7362
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7365
[TakeutiZaring] p. 80Exercise 1rankss 7379  rankssb 7378
[TakeutiZaring] p. 80Exercise 2unbndrank 7372
[TakeutiZaring] p. 80Proposition 9.19bndrank 7371
[TakeutiZaring] p. 83Axiom of Choiceac4 7960  dfac3 7606
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7515  numth 7957  numth2 7956
[TakeutiZaring] p. 85Definition 10.4cardval 8026
[TakeutiZaring] p. 85Proposition 10.5cardid 8027  cardid2 7444
[TakeutiZaring] p. 85Proposition 10.9oncard 7451
[TakeutiZaring] p. 85Proposition 10.10carden 8029
[TakeutiZaring] p. 85Proposition 10.11cardidm 7450
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7435
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7456
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7448
[TakeutiZaring] p. 87Proposition 10.15pwen 6893
[TakeutiZaring] p. 88Exercise 1en0 6783
[TakeutiZaring] p. 88Exercise 7infensuc 6898
[TakeutiZaring] p. 89Exercise 10omxpen 6823
[TakeutiZaring] p. 90Corollary 10.23cardnn 7454
[TakeutiZaring] p. 90Definition 10.27alephiso 7583
[TakeutiZaring] p. 90Proposition 10.20nneneq 6903
[TakeutiZaring] p. 90Proposition 10.22onomeneq 6909
[TakeutiZaring] p. 90Proposition 10.26alephprc 7584
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6908
[TakeutiZaring] p. 91Exercise 2alephle 7573
[TakeutiZaring] p. 91Exercise 3aleph0 7551
[TakeutiZaring] p. 91Exercise 4cardlim 7463
[TakeutiZaring] p. 91Exercise 7infpss 7701
[TakeutiZaring] p. 91Exercise 8infcntss 6989
[TakeutiZaring] p. 91Definition 10.29df-fin 6727  isfi 6745
[TakeutiZaring] p. 92Proposition 10.32onfin 6910
[TakeutiZaring] p. 92Proposition 10.34imadomg 8017
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6816
[TakeutiZaring] p. 93Proposition 10.35fodomb 8009
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7673  unxpdom 6929
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7465  cardsdomelir 7464
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 6931
[TakeutiZaring] p. 94Proposition 10.39infxpen 7500
[TakeutiZaring] p. 95Definition 10.42df-map 6634
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8040  infxpidm2 7502
[TakeutiZaring] p. 95Proposition 10.41infcda 7692  infxp 7699  infxpg 24060
[TakeutiZaring] p. 96Proposition 10.44pw2en 6828  pw2f1o 6826
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6886
[TakeutiZaring] p. 97Theorem 10.46ac6s3 7972
[TakeutiZaring] p. 98Theorem 10.46ac6c5 7967  ac6s5 7976
[TakeutiZaring] p. 98Theorem 10.47unidom 8023
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8024  uniimadomf 8025
[TakeutiZaring] p. 100Definition 11.1cfcof 7758
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7753
[TakeutiZaring] p. 102Exercise 1cfle 7738
[TakeutiZaring] p. 102Exercise 2cf0 7735
[TakeutiZaring] p. 102Exercise 3cfsuc 7741
[TakeutiZaring] p. 102Exercise 4cfom 7748
[TakeutiZaring] p. 102Proposition 11.9coftr 7757
[TakeutiZaring] p. 103Theorem 11.15alephreg 8058
[TakeutiZaring] p. 103Proposition 11.11cardcf 7736
[TakeutiZaring] p. 103Proposition 11.13alephsing 7760
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7582
[TakeutiZaring] p. 104Proposition 11.16carduniima 7581
[TakeutiZaring] p. 104Proposition 11.18alephfp 7593  alephfp2 7594
[TakeutiZaring] p. 106Theorem 11.20gchina 8175
[TakeutiZaring] p. 106Theorem 11.21mappwen 7597
[TakeutiZaring] p. 107Theorem 11.26konigth 8045
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8059
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8060
[Tarski] p. 67Axiom B5ax-4 1681
[Tarski] p. 68Lemma 6avril1 20461  equid 1807  equid1 1809  equidALT 1808
[Tarski] p. 69Lemma 7equcomi-o 1812  equcomi 1811
[Tarski] p. 70Lemma 14a4im 1856  a4ime 1857
[Tarski] p. 70Lemma 16ax-11 1613  ax-11o 1928  ax11i 1822
[Tarski] p. 70Lemmas 16 and 17sb6 1980
[Tarski] p. 75Axiom B8ax-9v 1621
[Tarski] p. 75Scheme B7ax9vax9 27588
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1617
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1614  ax-14 1615
[Truss] p. 114Theorem 5.18ruc 12329
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 495
[WhiteheadRussell] p. 96Axiom *1.3olc 372
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 374
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 504
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 811
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 159
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 107
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 77
[WhiteheadRussell] p. 100Theorem *2.05imim2 50
[WhiteheadRussell] p. 100Theorem *2.06imim1 71
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 404
[WhiteheadRussell] p. 101Theorem *2.06barbara 2198  syl 16
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 384
[WhiteheadRussell] p. 101Theorem *2.08id 20  id1 21
[WhiteheadRussell] p. 101Theorem *2.11exmid 403
[WhiteheadRussell] p. 101Theorem *2.12notnot1 113
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 405
[WhiteheadRussell] p. 102Theorem *2.14notnot2 104  notnot2ALT2 27134
[WhiteheadRussell] p. 102Theorem *2.15con1 119
[WhiteheadRussell] p. 103Theorem *2.16con3 125  con3th 923
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 102
[WhiteheadRussell] p. 104Theorem *2.2orc 373
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 552
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 100
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 101
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 392
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 852
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 36
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 507
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 508
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 813
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 814
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 812
[WhiteheadRussell] p. 105Definition *2.33df-3or 934
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 555
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 553
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 554
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 48
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 385
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 386
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 143
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 161
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 387
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 388
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 389
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 144
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 146
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 361
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 362
[WhiteheadRussell] p. 107Theorem *2.55orel1 370
[WhiteheadRussell] p. 107Theorem *2.56orel2 371
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 162
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 397
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 760
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 761
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 163
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 390  pm2.67 391
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 145
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 396
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 820
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 398
[WhiteheadRussell] p. 108Theorem *2.69looinv 173
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 815
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 816
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 819
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 818
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 821
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 822
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 72
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 823
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 95
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 480
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 430  pm3.2im 136
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 481
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 482
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 483
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 484
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 431
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 432
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 851
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 567
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 427
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 428
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 439  simplim 142
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 443  simprim 141
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 565
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 566
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 559
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 540
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 538
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 539
[WhiteheadRussell] p. 113Theorem *3.44jao 494  pm3.44 493
[WhiteheadRussell] p. 113Theorem *3.47prth 551
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 829
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 804
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 803
[WhiteheadRussell] p. 116Theorem *4.1con34b 282
[WhiteheadRussell] p. 117Theorem *4.2biid 226
[WhiteheadRussell] p. 117Theorem *4.11notbi 285
[WhiteheadRussell] p. 117Theorem *4.12con2bi 317
[WhiteheadRussell] p. 117Theorem *4.13notnot 281
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 558
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 561
[WhiteheadRussell] p. 117Theorem *4.21bicom 190
[WhiteheadRussell] p. 117Theorem *4.22biantr 896  bitr 686  wl-bitr 23894
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 621
[WhiteheadRussell] p. 117Theorem *4.25oridm 496  pm4.25 497
[WhiteheadRussell] p. 118Theorem *4.3ancom 433
[WhiteheadRussell] p. 118Theorem *4.4andi 836
[WhiteheadRussell] p. 118Theorem *4.31orcom 375
[WhiteheadRussell] p. 118Theorem *4.32anass 627
[WhiteheadRussell] p. 118Theorem *4.33orass 506
[WhiteheadRussell] p. 118Theorem *4.36anbi1 684
[WhiteheadRussell] p. 118Theorem *4.37orbi1 683
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 841
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 840
[WhiteheadRussell] p. 118Definition *4.34df-3an 935
[WhiteheadRussell] p. 119Theorem *4.41ordi 831
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 925
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 892
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 557
[WhiteheadRussell] p. 119Theorem *4.45orabs 825  pm4.45 666  pm4.45im 541
[WhiteheadRussell] p. 120Theorem *4.5anor 471
[WhiteheadRussell] p. 120Theorem *4.6imor 400
[WhiteheadRussell] p. 120Theorem *4.7anclb 526
[WhiteheadRussell] p. 120Theorem *4.51ianor 470
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 473
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 474
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 475
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 476
[WhiteheadRussell] p. 120Theorem *4.56ioran 472  pm4.56 477
[WhiteheadRussell] p. 120Theorem *4.57oran 478  pm4.57 479
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 413
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 406
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 408
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 360
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 414
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 407
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 415
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 608  pm4.71d 612  pm4.71i 610  pm4.71r 609  pm4.71rd 613  pm4.71ri 611
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 845
[WhiteheadRussell] p. 121Theorem *4.73iba 485
[WhiteheadRussell] p. 121Theorem *4.74biorf 393
[WhiteheadRussell] p. 121Theorem *4.76jcab 830  pm4.76 835
[WhiteheadRussell] p. 121Theorem *4.77jaob 755  pm4.77 759
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 562
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 563
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 353
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 354
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 893
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 894
[WhiteheadRussell] p. 122Theorem *4.84imbi1 312
[WhiteheadRussell] p. 122Theorem *4.85imbi2 313
[WhiteheadRussell] p. 122Theorem *4.86bibi1 316  wl-bibi1 23887
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 349  impexp 429  pm4.87 564
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 827
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 853
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 854
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 856
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 855
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 858
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 859
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 857
[WhiteheadRussell] p. 124Theorem *5.18nbbn 346  pm5.18 344
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 348
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 828
[WhiteheadRussell] p. 124Theorem *5.22xor 860
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 862
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 863
[WhiteheadRussell] p. 124Theorem *5.25dfor2 399
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 689
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 350
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 325
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 877
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 899
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 568
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 614
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 847
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 868
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 848
[WhiteheadRussell] p. 125Theorem *5.41imdi 351  pm5.41 352
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 527
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 876
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 768
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 869
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 866
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 690
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 888
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 889
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 901
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 329
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 234
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 902
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 26519
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26520
[WhiteheadRussell] p. 147Theorem *10.2219.26 1581
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26521
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26522
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26523
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1606
[WhiteheadRussell] p. 151Theorem *10.301albitr 26524
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26525
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26526
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26527
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26528
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26530
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26531
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26532
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26529
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26535
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2063
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26536
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26537
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1599
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26538
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26539
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26540
[WhiteheadRussell] p. 162Theorem *11.322alim 26541
[WhiteheadRussell] p. 162Theorem *11.332albi 26542
[WhiteheadRussell] p. 162Theorem *11.342exim 26543
[WhiteheadRussell] p. 162Theorem *11.36a4sbce-2 26545
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26544
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1598
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26547
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26548
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26546
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1560
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26549
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26550
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1567
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26551
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2012  pm11.53g 23929
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26552
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26557
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26553
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26554
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26555
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26556
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26561
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26558
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26559
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26560
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26562
[WhiteheadRussell] p. 175Definition *14.02df-eu 2106
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 26574  pm13.13b 26575
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 26576
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2471
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2472
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2830
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 26582
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 26583
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 26577
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 26800  pm13.193 26578
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 26579
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 26580
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 26581
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 26588
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 26587
[WhiteheadRussell] p. 184Definition *14.01iotasbc 26586
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2954
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 26589  pm14.122b 26590  pm14.122c 26591
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 26592  pm14.123b 26593  pm14.123c 26594
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 26596
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 26595
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 26597
[WhiteheadRussell] p. 190Theorem *14.22iota4 6135
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 26598
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6136
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 26599
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 26601
[WhiteheadRussell] p. 192Theorem *14.26eupick 2164  eupickbi 2167  sbaniota 26602
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 26600
[WhiteheadRussell] p. 192Theorem *14.271eubi 26603
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 26604
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 4587
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7491  pm54.43lem 7490
[Young] p. 141Definition of operator orderingleop2 22329
[Young] p. 142Example 12.2(i)0leop 22335  idleop 22336
[vandenDries] p. 42Lemma 61irrapx1 25879
[vandenDries] p. 43Theorem 62pellex 25886  pellexlem1 25880

This page was last updated on 15-Jan-2017.
Copyright terms: Public domain