Metamath Proof Explorer Home Metamath Proof Explorer
Bibliographic Cross-References
 
Mirrors  >  Home  >  MPE Home  >  Bibliographic Cross-References

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the Metamath Proof Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular set theory book, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Bibliographic Cross-Reference for the Metamath Proof Explorer
Bibliographic ReferenceDescriptionMetamath Proof Explorer Page(s)
[Adamek] p. 28Proposition 3.10sectcan 13464
[Adamek] p. 29Proposition 3.14(1)invinv 13478
[Adamek] p. 29Proposition 3.14(2)invco 13479  isoco 13481
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25285
[AitkenIBCG] p. 3Definition 2df-angtrg 25281  df-trcng 25284
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25157  df-ig2 25156
[AitkenIBG] p. 2Definition 4df-li 25172
[AitkenIBG] p. 3Definition 5df-col 25186
[AitkenIBG] p. 3Definition 6df-con2 25191
[AitkenIBG] p. 3Proposition 4isconcl5a 25196  isconcl5ab 25197  isconcl6a 25198  isconcl6ab 25199
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25204
[AitkenIBG] p. 4Exercise 5tpne 25170
[AitkenIBG] p. 4Definition 8df-seg2 25226
[AitkenIBG] p. 4Definition 10df-sside 25258
[AitkenIBG] p. 4Definition 11df-ray2 25247
[AitkenIBG] p. 10Definition 17df-angle 25253
[AitkenIBG] p. 15Definition 23df-triangle 25255
[AitkenIBG] p. 15Definition 24df-cnvx 25274
[AitkenNG] p. 2Definition 1df-slices 25288
[AitkenNG] p. 2Definition 2df-Cut 25290
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25292
[AitkenNG] p. 4Definition 5df-crcl 25294
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18011  df-nmoo 21082
[AkhiezerGlazman] p. 64Theoremhmopidmch 22492  hmopidmchi 22490
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22540  pjcmul2i 22541
[AkhiezerGlazman] p. 72Theoremcnvunop 22257  unoplin 22259
[AkhiezerGlazman] p. 72Equation 2unopadj 22258  unopadj2 22277
[AkhiezerGlazman] p. 73Theoremelunop2 22352  lnopunii 22351
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22425
[Apostol] p. 18Theorem I.1addcan 8872  addcan2d 8892  addcan2i 8882  addcand 8891  addcani 8881
[Apostol] p. 18Theorem I.2negeu 8914
[Apostol] p. 18Theorem I.3negsub 8967  negsubd 9031  negsubi 8996
[Apostol] p. 18Theorem I.4negneg 8969  negnegd 9020  negnegi 8988
[Apostol] p. 18Theorem I.5subdi 9074  subdid 9096  subdii 9089  subdir 9075  subdird 9097  subdiri 9090
[Apostol] p. 18Theorem I.6mul01 8867  mul01d 8887  mul01i 8878  mul02 8866  mul02d 8886  mul02i 8877
[Apostol] p. 18Theorem I.7mulcan 9263  mulcan2d 9262  mulcand 9261  mulcani 9265
[Apostol] p. 18Theorem I.8receu 9271
[Apostol] p. 18Theorem I.9divrec 9296  divrecd 9393  divreci 9359  divreczi 9352
[Apostol] p. 18Theorem I.10recrec 9313  recreci 9346
[Apostol] p. 18Theorem I.11mul0or 9266  mul0ord 9276  mul0ori 9274
[Apostol] p. 18Theorem I.12mul2neg 9080  mul2negd 9095  mul2negi 9088  mulneg1 9077  mulneg1d 9093  mulneg1i 9086
[Apostol] p. 18Theorem I.13divadddiv 9331  divadddivd 9430  divadddivi 9376
[Apostol] p. 18Theorem I.14divmuldiv 9316  divmuldivd 9427  divmuldivi 9374
[Apostol] p. 18Theorem I.15divdivdiv 9317  divdivdivd 9433  divdivdivi 9377
[Apostol] p. 20Axiom 7rpaddcl 10220  rpaddcld 10251  rpmulcl 10221  rpmulcld 10252
[Apostol] p. 20Axiom 8rpneg 10229
[Apostol] p. 20Axiom 90nrp 10230
[Apostol] p. 20Theorem I.17lttri 8821
[Apostol] p. 20Theorem I.18ltadd1d 9225  ltadd1dd 9243  ltadd1i 9188
[Apostol] p. 20Theorem I.19ltmul1 9454  ltmul1a 9453  ltmul1i 9523  ltmul1ii 9533  ltmul2 9455  ltmul2d 10274  ltmul2dd 10288  ltmul2i 9526
[Apostol] p. 20Theorem I.20msqgt0 9155  msqgt0d 9200  msqgt0i 9171
[Apostol] p. 20Theorem I.210lt1 9157
[Apostol] p. 20Theorem I.23lt0neg1 9141  lt0neg1d 9202  ltneg 9135  ltnegd 9210  ltnegi 9178
[Apostol] p. 20Theorem I.25lt2add 9120  lt2addd 9254  lt2addi 9196
[Apostol] p. 20Definition of positive numbersdf-rp 10201
[Apostol] p. 21Exercise 4recgt0 9448  recgt0d 9539  recgt0i 9509  recgt0ii 9510
[Apostol] p. 22Definition of integersdf-z 9871
[Apostol] p. 22Definition of positive integersdfnn3 9608
[Apostol] p. 22Definition of rationalsdf-q 10163
[Apostol] p. 24Theorem I.26supeu 7086
[Apostol] p. 26Theorem I.28nnunb 9807
[Apostol] p. 26Theorem I.29arch 9808
[Apostol] p. 28Exercise 2btwnz 9960
[Apostol] p. 28Exercise 3nnrecl 9809
[Apostol] p. 28Exercise 4rebtwnz 10161
[Apostol] p. 28Exercise 5zbtwnre 10160
[Apostol] p. 28Exercise 6qbtwnre 10371
[Apostol] p. 28Exercise 10(a)zneo 9940
[Apostol] p. 29Theorem I.35msqsqrd 11761  resqrth 11582  sqrth 11687  sqrthi 11693  sqsqrd 11760
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9597
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10130
[Apostol] p. 361Remarkcrreczi 11068
[Apostol] p. 363Remarkabsgt0i 11721
[Apostol] p. 363Exampleabssubd 11774  abssubi 11725
[Baer] p. 40Property (b)mapdord 30455
[Baer] p. 40Property (c)mapd11 30456
[Baer] p. 40Property (e)mapdin 30479  mapdlsm 30481
[Baer] p. 40Property (f)mapd0 30482
[Baer] p. 40Definition of projectivitydf-mapd 30442  mapd1o 30465
[Baer] p. 41Property (g)mapdat 30484
[Baer] p. 44Part (1)mapdpg 30523
[Baer] p. 45Part (2)hdmap1eq 30619  mapdheq 30545  mapdheq2 30546  mapdheq2biN 30547
[Baer] p. 45Part (3)baerlem3 30530
[Baer] p. 46Part (4)mapdheq4 30549  mapdheq4lem 30548
[Baer] p. 46Part (5)baerlem5a 30531  baerlem5abmN 30535  baerlem5amN 30533  baerlem5b 30532  baerlem5bmN 30534
[Baer] p. 47Part (6)hdmap1l6 30639  hdmap1l6a 30627  hdmap1l6e 30632  hdmap1l6f 30633  hdmap1l6g 30634  hdmap1l6lem1 30625  hdmap1l6lem2 30626  hdmap1p6N 30640  mapdh6N 30564  mapdh6aN 30552  mapdh6eN 30557  mapdh6fN 30558  mapdh6gN 30559  mapdh6lem1N 30550  mapdh6lem2N 30551
[Baer] p. 48Part 9hdmapval 30648
[Baer] p. 48Part 10hdmap10 30660
[Baer] p. 48Part 11hdmapadd 30663
[Baer] p. 48Part (6)hdmap1l6h 30635  mapdh6hN 30560
[Baer] p. 48Part (7)mapdh75cN 30570  mapdh75d 30571  mapdh75e 30569  mapdh75fN 30572  mapdh7cN 30566  mapdh7dN 30567  mapdh7eN 30565  mapdh7fN 30568
[Baer] p. 48Part (8)mapdh8 30606  mapdh8a 30592  mapdh8aa 30593  mapdh8ab 30594  mapdh8ac 30595  mapdh8ad 30596  mapdh8b 30597  mapdh8c 30598  mapdh8d 30600  mapdh8d0N 30599  mapdh8e 30601  mapdh8fN 30602  mapdh8g 30603  mapdh8i 30604  mapdh8j 30605
[Baer] p. 48Part (9)mapdh9a 30607
[Baer] p. 48Equation 10mapdhvmap 30586
[Baer] p. 49Part 12hdmap11 30668  hdmapeq0 30664  hdmapf1oN 30685  hdmapneg 30666  hdmaprnN 30684  hdmaprnlem1N 30669  hdmaprnlem3N 30670  hdmaprnlem3uN 30671  hdmaprnlem4N 30673  hdmaprnlem6N 30674  hdmaprnlem7N 30675  hdmaprnlem8N 30676  hdmaprnlem9N 30677  hdmapsub 30667
[Baer] p. 49Part 14hdmap14lem1 30688  hdmap14lem10 30697  hdmap14lem1a 30686  hdmap14lem2N 30689  hdmap14lem2a 30687  hdmap14lem3 30690  hdmap14lem8 30695  hdmap14lem9 30696
[Baer] p. 50Part 14hdmap14lem11 30698  hdmap14lem12 30699  hdmap14lem13 30700  hdmap14lem14 30701  hdmap14lem15 30702  hgmapval 30707
[Baer] p. 50Part 15hgmapadd 30714  hgmapmul 30715  hgmaprnlem2N 30717  hgmapvs 30711
[Baer] p. 50Part 16hgmaprnN 30721
[Baer] p. 110Lemma 1hdmapip0com 30737
[Baer] p. 110Line 27hdmapinvlem1 30738
[Baer] p. 110Line 28hdmapinvlem2 30739
[Baer] p. 110Line 30hdmapinvlem3 30740
[Baer] p. 110Part 1.2hdmapglem5 30742  hgmapvv 30746
[Baer] p. 110Proposition 1hdmapinvlem4 30741
[Baer] p. 111Line 10hgmapvvlem1 30743
[Baer] p. 111Line 15hdmapg 30750  hdmapglem7 30749
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2118
[BellMachover] p. 460Notationdf-mo 2119
[BellMachover] p. 460Definitionmo3 2144
[BellMachover] p. 461Axiom Extax-ext 2234
[BellMachover] p. 462Theorem 1.1bm1.1 2238
[BellMachover] p. 463Axiom Repaxrep5 4030
[BellMachover] p. 463Scheme Sepaxsep 4034
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4038
[BellMachover] p. 466Axiom Powaxpow3 4082
[BellMachover] p. 466Axiom Unionaxun2 4402
[BellMachover] p. 468Definitiondf-ord 4285
[BellMachover] p. 469Theorem 2.2(i)ordirr 4300
[BellMachover] p. 469Theorem 2.2(iii)onelon 4307
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4302
[BellMachover] p. 471Definition of Ndf-om 4545
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4485
[BellMachover] p. 471Definition of Limdf-lim 4287
[BellMachover] p. 472Axiom Infzfinf2 7224
[BellMachover] p. 473Theorem 2.8limom 4559
[BellMachover] p. 477Equation 3.1df-r1 7317
[BellMachover] p. 478Definitionrankval2 7371
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7335  r1ord3g 7332
[BellMachover] p. 480Axiom Regzfreg2 7191
[BellMachover] p. 488Axiom ACac5 7985  dfac4 7630
[BellMachover] p. 490Definition of alephalephval3 7618
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28136
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22692
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22734  chirredi 22733
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22722
[Beran] p. 3Definition of joinsshjval3 21692
[Beran] p. 39Theorem 2.3(i)cmcm2 21972  cmcm2i 21949  cmcm2ii 21954  cmt2N 28067
[Beran] p. 40Theorem 2.3(iii)lecm 21973  lecmi 21958  lecmii 21959
[Beran] p. 45Theorem 3.4cmcmlem 21947
[Beran] p. 49Theorem 4.2cm2j 21976  cm2ji 21981  cm2mi 21982
[Beran] p. 95Definitiondf-sh 21545  issh2 21547
[Beran] p. 95Lemma 3.1(S5)his5 21424
[Beran] p. 95Lemma 3.1(S6)his6 21437
[Beran] p. 95Lemma 3.1(S7)his7 21428
[Beran] p. 95Lemma 3.2(S8)ho01i 22167
[Beran] p. 95Lemma 3.2(S9)hoeq1 22169
[Beran] p. 95Lemma 3.2(S10)ho02i 22168
[Beran] p. 95Lemma 3.2(S11)hoeq2 22170
[Beran] p. 95Postulate (S1)ax-his1 21420  his1i 21438
[Beran] p. 95Postulate (S2)ax-his2 21421
[Beran] p. 95Postulate (S3)ax-his3 21422
[Beran] p. 95Postulate (S4)ax-his4 21423
[Beran] p. 96Definition of normdf-hnorm 21307  dfhnorm2 21460  normval 21462
[Beran] p. 96Definition for Cauchy sequencehcau 21522
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21312
[Beran] p. 96Definition of complete subspaceisch3 21580
[Beran] p. 96Definition of convergedf-hlim 21311  hlimi 21526
[Beran] p. 97Theorem 3.3(i)norm-i-i 21471  norm-i 21467
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21475  norm-ii 21476  normlem0 21447  normlem1 21448  normlem2 21449  normlem3 21450  normlem4 21451  normlem5 21452  normlem6 21453  normlem7 21454  normlem7tALT 21457
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21477  norm-iii 21478
[Beran] p. 98Remark 3.4bcs 21519  bcsiALT 21517  bcsiHIL 21518
[Beran] p. 98Remark 3.4(B)normlem9at 21459  normpar 21493  normpari 21492
[Beran] p. 98Remark 3.4(C)normpyc 21484  normpyth 21483  normpythi 21480
[Beran] p. 99Remarklnfn0 22386  lnfn0i 22381  lnop0 22305  lnop0i 22309
[Beran] p. 99Theorem 3.5(i)nmcexi 22365  nmcfnex 22392  nmcfnexi 22390  nmcopex 22368  nmcopexi 22366
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22393  nmcfnlbi 22391  nmcoplb 22369  nmcoplbi 22367
[Beran] p. 99Theorem 3.5(iii)lnfncon 22395  lnfnconi 22394  lnopcon 22374  lnopconi 22373
[Beran] p. 100Lemma 3.6normpar2i 21494
[Beran] p. 101Lemma 3.6norm3adifi 21491  norm3adifii 21486  norm3dif 21488  norm3difi 21485
[Beran] p. 102Theorem 3.7(i)chocunii 21639  pjhth 21731  pjhtheu 21732  pjpjhth 21763  pjpjhthi 21764  pjth 18597
[Beran] p. 102Theorem 3.7(ii)ococ 21744  ococi 21743
[Beran] p. 103Remark 3.8nlelchi 22400
[Beran] p. 104Theorem 3.9riesz3i 22401  riesz4 22403  riesz4i 22402
[Beran] p. 104Theorem 3.10cnlnadj 22418  cnlnadjeu 22417  cnlnadjeui 22416  cnlnadji 22415  cnlnadjlem1 22406  nmopadjlei 22427
[Beran] p. 106Theorem 3.11(i)adjeq0 22430
[Beran] p. 106Theorem 3.11(v)nmopadji 22429
[Beran] p. 106Theorem 3.11(ii)adjmul 22431
[Beran] p. 106Theorem 3.11(iv)adjadj 22275
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22441  nmopcoadji 22440
[Beran] p. 106Theorem 3.11(iii)adjadd 22432
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22442
[Beran] p. 106Theorem 3.11(viii)adjcoi 22439  pjadj2coi 22543  pjadjcoi 22500
[Beran] p. 107Definitiondf-ch 21560  isch2 21562
[Beran] p. 107Remark 3.12choccl 21644  isch3 21580  occl 21642  ocsh 21621  shoccl 21643  shocsh 21622
[Beran] p. 107Remark 3.12(B)ococin 21746
[Beran] p. 108Theorem 3.13chintcl 21670
[Beran] p. 109Property (i)pjadj2 22526  pjadj3 22527  pjadji 22041  pjadjii 22030
[Beran] p. 109Property (ii)pjidmco 22520  pjidmcoi 22516  pjidmi 22029
[Beran] p. 110Definition of projector orderingpjordi 22512
[Beran] p. 111Remarkho0val 22089  pjch1 22026
[Beran] p. 111Definitiondf-hfmul 21925  df-hfsum 21924  df-hodif 21923  df-homul 21922  df-hosum 21921
[Beran] p. 111Lemma 4.4(i)pjo 22027
[Beran] p. 111Lemma 4.4(ii)pjch 22050  pjchi 21770
[Beran] p. 111Lemma 4.4(iii)pjoc2 21777  pjoc2i 21776
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22036
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22504  pjssmii 22037
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22503
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22502
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22507
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22505  pjssge0ii 22038
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22506  pjdifnormii 22039
[BourbakiEns] p. Proposition 8fcof1 5646  fcofo 5647
[BourbakiFVR] p. Definition 1isder 24802
[BourbakiTop1] p. Remarkxnegmnf 10382  xnegpnf 10381
[BourbakiTop1] p. Remark rexneg 10383
[BourbakiTop1] p. Theoremneiss 16640
[BourbakiTop1] p. Axiom GT'tgpsubcn 17567
[BourbakiTop1] p. Example 1snfil 17353
[BourbakiTop1] p. Example 2neifil 17369
[BourbakiTop1] p. Definitionistgp 17554
[BourbakiTop1] p. Propositioncnpco 16790  ishmeo 17244  neips 16644
[BourbakiTop1] p. Definition 1filintn0 17350
[BourbakiTop1] p. Proposition 9cnpflf2 17489
[BourbakiTop1] p. Theorem 1 (d)iscncl 16792
[BourbakiTop1] p. Proposition Vissnei2 16647
[BourbakiTop1] p. Definition C'''df-cmp 16908
[BourbakiTop1] p. Proposition Viiinnei 16656
[BourbakiTop1] p. Proposition Vivneissex 16658
[BourbakiTop1] p. Proposition Viiielnei 16642  ssnei 16641
[BourbakiTop1] p. Remark below def. 1filn0 17351
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17335
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17352
[ChoquetDD] p. 2Definition of mappingdf-mpt 3973
[Cohen] p. 301Remarkrelogoprlem 19730
[Cohen] p. 301Property 2relogmul 19731  relogmuld 19760
[Cohen] p. 301Property 3relogdiv 19732  relogdivd 19761
[Cohen] p. 301Property 4relogexp 19735
[Cohen] p. 301Property 1alog1 19725
[Cohen] p. 301Property 1bloge 19726
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10808
[Crawley] p. 1Definition of posetdf-poset 13886
[Crawley] p. 107Theorem 13.2hlsupr 28202
[Crawley] p. 110Theorem 13.3arglem1N 29006  dalaw 28702
[Crawley] p. 111Theorem 13.4hlathil 30781
[Crawley] p. 111Definition of set Wdf-watsN 28806
[Crawley] p. 111Definition of dilationdf-dilN 28922  df-ldil 28920  isldil 28926
[Crawley] p. 111Definition of translationdf-ltrn 28921  df-trnN 28923  isltrn 28935  ltrnu 28937
[Crawley] p. 112Lemma Acdlema1N 28607  cdlema2N 28608  exatleN 28220
[Crawley] p. 112Lemma B1cvrat 28292  cdlemb 28610  cdlemb2 28857  cdlemb3 29422  idltrn 28966  l1cvat 27872  lhpat 28859  lhpat2 28861  lshpat 27873  ltrnel 28955  ltrnmw 28967
[Crawley] p. 112Lemma Ccdlemc1 29007  cdlemc2 29008  ltrnnidn 28990  trlat 28985  trljat1 28982  trljat2 28983  trljat3 28984  trlne 29001  trlnidat 28989  trlnle 29002
[Crawley] p. 112Definition of automorphismdf-pautN 28807
[Crawley] p. 113Lemma Ccdlemc 29013  cdlemc3 29009  cdlemc4 29010
[Crawley] p. 113Lemma Dcdlemd 29023  cdlemd1 29014  cdlemd2 29015  cdlemd3 29016  cdlemd4 29017  cdlemd5 29018  cdlemd6 29019  cdlemd7 29020  cdlemd8 29021  cdlemd9 29022  cdleme31sde 29201  cdleme31se 29198  cdleme31se2 29199  cdleme31snd 29202  cdleme32a 29257  cdleme32b 29258  cdleme32c 29259  cdleme32d 29260  cdleme32e 29261  cdleme32f 29262  cdleme32fva 29253  cdleme32fva1 29254  cdleme32fvcl 29256  cdleme32le 29263  cdleme48fv 29315  cdleme4gfv 29323  cdleme50eq 29357  cdleme50f 29358  cdleme50f1 29359  cdleme50f1o 29362  cdleme50laut 29363  cdleme50ldil 29364  cdleme50lebi 29356  cdleme50rn 29361  cdleme50rnlem 29360  cdlemeg49le 29327  cdlemeg49lebilem 29355
[Crawley] p. 113Lemma Ecdleme 29376  cdleme00a 29025  cdleme01N 29037  cdleme02N 29038  cdleme0a 29027  cdleme0aa 29026  cdleme0b 29028  cdleme0c 29029  cdleme0cp 29030  cdleme0cq 29031  cdleme0dN 29032  cdleme0e 29033  cdleme0ex1N 29039  cdleme0ex2N 29040  cdleme0fN 29034  cdleme0gN 29035  cdleme0moN 29041  cdleme1 29043  cdleme10 29070  cdleme10tN 29074  cdleme11 29086  cdleme11a 29076  cdleme11c 29077  cdleme11dN 29078  cdleme11e 29079  cdleme11fN 29080  cdleme11g 29081  cdleme11h 29082  cdleme11j 29083  cdleme11k 29084  cdleme11l 29085  cdleme12 29087  cdleme13 29088  cdleme14 29089  cdleme15 29094  cdleme15a 29090  cdleme15b 29091  cdleme15c 29092  cdleme15d 29093  cdleme16 29101  cdleme16aN 29075  cdleme16b 29095  cdleme16c 29096  cdleme16d 29097  cdleme16e 29098  cdleme16f 29099  cdleme16g 29100  cdleme19a 29119  cdleme19b 29120  cdleme19c 29121  cdleme19d 29122  cdleme19e 29123  cdleme19f 29124  cdleme1b 29042  cdleme2 29044  cdleme20aN 29125  cdleme20bN 29126  cdleme20c 29127  cdleme20d 29128  cdleme20e 29129  cdleme20f 29130  cdleme20g 29131  cdleme20h 29132  cdleme20i 29133  cdleme20j 29134  cdleme20k 29135  cdleme20l 29138  cdleme20l1 29136  cdleme20l2 29137  cdleme20m 29139  cdleme20y 29118  cdleme20zN 29117  cdleme21 29153  cdleme21d 29146  cdleme21e 29147  cdleme22a 29156  cdleme22aa 29155  cdleme22b 29157  cdleme22cN 29158  cdleme22d 29159  cdleme22e 29160  cdleme22eALTN 29161  cdleme22f 29162  cdleme22f2 29163  cdleme22g 29164  cdleme23a 29165  cdleme23b 29166  cdleme23c 29167  cdleme26e 29175  cdleme26eALTN 29177  cdleme26ee 29176  cdleme26f 29179  cdleme26f2 29181  cdleme26f2ALTN 29180  cdleme26fALTN 29178  cdleme27N 29185  cdleme27a 29183  cdleme27cl 29182  cdleme28c 29188  cdleme3 29053  cdleme30a 29194  cdleme31fv 29206  cdleme31fv1 29207  cdleme31fv1s 29208  cdleme31fv2 29209  cdleme31id 29210  cdleme31sc 29200  cdleme31sdnN 29203  cdleme31sn 29196  cdleme31sn1 29197  cdleme31sn1c 29204  cdleme31sn2 29205  cdleme31so 29195  cdleme35a 29264  cdleme35b 29266  cdleme35c 29267  cdleme35d 29268  cdleme35e 29269  cdleme35f 29270  cdleme35fnpq 29265  cdleme35g 29271  cdleme35h 29272  cdleme35h2 29273  cdleme35sn2aw 29274  cdleme35sn3a 29275  cdleme36a 29276  cdleme36m 29277  cdleme37m 29278  cdleme38m 29279  cdleme38n 29280  cdleme39a 29281  cdleme39n 29282  cdleme3b 29045  cdleme3c 29046  cdleme3d 29047  cdleme3e 29048  cdleme3fN 29049  cdleme3fa 29052  cdleme3g 29050  cdleme3h 29051  cdleme4 29054  cdleme40m 29283  cdleme40n 29284  cdleme40v 29285  cdleme40w 29286  cdleme41fva11 29293  cdleme41sn3aw 29290  cdleme41sn4aw 29291  cdleme41snaw 29292  cdleme42a 29287  cdleme42b 29294  cdleme42c 29288  cdleme42d 29289  cdleme42e 29295  cdleme42f 29296  cdleme42g 29297  cdleme42h 29298  cdleme42i 29299  cdleme42k 29300  cdleme42ke 29301  cdleme42keg 29302  cdleme42mN 29303  cdleme42mgN 29304  cdleme43aN 29305  cdleme43bN 29306  cdleme43cN 29307  cdleme43dN 29308  cdleme5 29056  cdleme50ex 29375  cdleme50ltrn 29373  cdleme51finvN 29372  cdleme51finvfvN 29371  cdleme51finvtrN 29374  cdleme6 29057  cdleme7 29065  cdleme7a 29059  cdleme7aa 29058  cdleme7b 29060  cdleme7c 29061  cdleme7d 29062  cdleme7e 29063  cdleme7ga 29064  cdleme8 29066  cdleme8tN 29071  cdleme9 29069  cdleme9a 29067  cdleme9b 29068  cdleme9tN 29073  cdleme9taN 29072  cdlemeda 29114  cdlemedb 29113  cdlemednpq 29115  cdlemednuN 29116  cdlemefr27cl 29219  cdlemefr32fva1 29226  cdlemefr32fvaN 29225  cdlemefrs32fva 29216  cdlemefrs32fva1 29217  cdlemefs27cl 29229  cdlemefs32fva1 29239  cdlemefs32fvaN 29238  cdlemesner 29112  cdlemeulpq 29036
[Crawley] p. 114Lemma E4atex 28892  4atexlem7 28891  cdleme0nex 29106  cdleme17a 29102  cdleme17c 29104  cdleme17d 29314  cdleme17d1 29105  cdleme17d2 29311  cdleme18a 29107  cdleme18b 29108  cdleme18c 29109  cdleme18d 29111  cdleme4a 29055
[Crawley] p. 115Lemma Ecdleme21a 29141  cdleme21at 29144  cdleme21b 29142  cdleme21c 29143  cdleme21ct 29145  cdleme21f 29148  cdleme21g 29149  cdleme21h 29150  cdleme21i 29151  cdleme22gb 29110
[Crawley] p. 116Lemma Fcdlemf 29379  cdlemf1 29377  cdlemf2 29378
[Crawley] p. 116Lemma Gcdlemftr1 29383  cdlemg16 29473  cdlemg28 29520  cdlemg28a 29509  cdlemg28b 29519  cdlemg3a 29413  cdlemg42 29545  cdlemg43 29546  cdlemg44 29549  cdlemg44a 29547  cdlemg46 29551  cdlemg47 29552  cdlemg9 29450  ltrnco 29535  ltrncom 29554  tgrpabl 29567  trlco 29543
[Crawley] p. 116Definition of Gdf-tgrp 29559
[Crawley] p. 117Lemma Gcdlemg17 29493  cdlemg17b 29478
[Crawley] p. 117Definition of Edf-edring-rN 29572  df-edring 29573
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 29576
[Crawley] p. 118Remarktendopltp 29596
[Crawley] p. 118Lemma Hcdlemh 29633  cdlemh1 29631  cdlemh2 29632
[Crawley] p. 118Lemma Icdlemi 29636  cdlemi1 29634  cdlemi2 29635
[Crawley] p. 118Lemma Jcdlemj1 29637  cdlemj2 29638  cdlemj3 29639  tendocan 29640
[Crawley] p. 118Lemma Kcdlemk 29790  cdlemk1 29647  cdlemk10 29659  cdlemk11 29665  cdlemk11t 29762  cdlemk11ta 29745  cdlemk11tb 29747  cdlemk11tc 29761  cdlemk11u-2N 29705  cdlemk11u 29687  cdlemk12 29666  cdlemk12u-2N 29706  cdlemk12u 29688  cdlemk13-2N 29692  cdlemk13 29668  cdlemk14-2N 29694  cdlemk14 29670  cdlemk15-2N 29695  cdlemk15 29671  cdlemk16-2N 29696  cdlemk16 29673  cdlemk16a 29672  cdlemk17-2N 29697  cdlemk17 29674  cdlemk18-2N 29702  cdlemk18-3N 29716  cdlemk18 29684  cdlemk19-2N 29703  cdlemk19 29685  cdlemk19u 29786  cdlemk1u 29675  cdlemk2 29648  cdlemk20-2N 29708  cdlemk20 29690  cdlemk21-2N 29707  cdlemk21N 29689  cdlemk22-3 29717  cdlemk22 29709  cdlemk23-3 29718  cdlemk24-3 29719  cdlemk25-3 29720  cdlemk26-3 29722  cdlemk26b-3 29721  cdlemk27-3 29723  cdlemk28-3 29724  cdlemk29-3 29727  cdlemk3 29649  cdlemk30 29710  cdlemk31 29712  cdlemk32 29713  cdlemk33N 29725  cdlemk34 29726  cdlemk35 29728  cdlemk36 29729  cdlemk37 29730  cdlemk38 29731  cdlemk39 29732  cdlemk39u 29784  cdlemk4 29650  cdlemk41 29736  cdlemk42 29757  cdlemk42yN 29760  cdlemk43N 29779  cdlemk45 29763  cdlemk46 29764  cdlemk47 29765  cdlemk48 29766  cdlemk49 29767  cdlemk5 29652  cdlemk50 29768  cdlemk51 29769  cdlemk52 29770  cdlemk53 29773  cdlemk54 29774  cdlemk55 29777  cdlemk55u 29782  cdlemk56 29787  cdlemk5a 29651  cdlemk5auN 29676  cdlemk5u 29677  cdlemk6 29653  cdlemk6u 29678  cdlemk7 29664  cdlemk7u-2N 29704  cdlemk7u 29686  cdlemk8 29654  cdlemk9 29655  cdlemk9bN 29656  cdlemki 29657  cdlemkid 29752  cdlemkj-2N 29698  cdlemkj 29679  cdlemksat 29662  cdlemksel 29661  cdlemksv 29660  cdlemksv2 29663  cdlemkuat 29682  cdlemkuel-2N 29700  cdlemkuel-3 29714  cdlemkuel 29681  cdlemkuv-2N 29699  cdlemkuv2-2 29701  cdlemkuv2-3N 29715  cdlemkuv2 29683  cdlemkuvN 29680  cdlemkvcl 29658  cdlemky 29742  cdlemkyyN 29778  tendoex 29791
[Crawley] p. 120Remarkdva1dim 29801
[Crawley] p. 120Lemma Lcdleml1N 29792  cdleml2N 29793  cdleml3N 29794  cdleml4N 29795  cdleml5N 29796  cdleml6 29797  cdleml7 29798  cdleml8 29799  cdleml9 29800  dia1dim 29878
[Crawley] p. 120Lemma Mdia11N 29865  diaf11N 29866  dialss 29863  diaord 29864  dibf11N 29978  djajN 29954
[Crawley] p. 120Definition of isomorphism mapdiaval 29849
[Crawley] p. 121Lemma Mcdlemm10N 29935  dia2dimlem1 29881  dia2dimlem2 29882  dia2dimlem3 29883  dia2dimlem4 29884  dia2dimlem5 29885  diaf1oN 29947  diarnN 29946  dvheveccl 29929  dvhopN 29933
[Crawley] p. 121Lemma Ncdlemn 30029  cdlemn10 30023  cdlemn11 30028  cdlemn11a 30024  cdlemn11b 30025  cdlemn11c 30026  cdlemn11pre 30027  cdlemn2 30012  cdlemn2a 30013  cdlemn3 30014  cdlemn4 30015  cdlemn4a 30016  cdlemn5 30018  cdlemn5pre 30017  cdlemn6 30019  cdlemn7 30020  cdlemn8 30021  cdlemn9 30022  diclspsn 30011
[Crawley] p. 121Definition of phi(q)df-dic 29990
[Crawley] p. 122Lemma Ndih11 30082  dihf11 30084  dihjust 30034  dihjustlem 30033  dihord 30081  dihord1 30035  dihord10 30040  dihord11b 30039  dihord11c 30041  dihord2 30044  dihord2a 30036  dihord2b 30037  dihord2cN 30038  dihord2pre 30042  dihord2pre2 30043  dihordlem6 30030  dihordlem7 30031  dihordlem7b 30032
[Crawley] p. 122Definition of isomorphism mapdihffval 30047  dihfval 30048  dihval 30049
[Eisenberg] p. 67Definition 5.3df-dif 3078
[Eisenberg] p. 82Definition 6.3dfom3 7229
[Eisenberg] p. 125Definition 8.21df-map 6657
[Eisenberg] p. 216Example 13.2(4)omenps 7236
[Eisenberg] p. 310Theorem 19.8cardprc 7494
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8056
[Enderton] p. 18Axiom of Empty Setaxnul 4042
[Enderton] p. 19Definitiondf-tp 3549
[Enderton] p. 26Exercise 5unissb 3752
[Enderton] p. 26Exercise 10pwel 4116
[Enderton] p. 28Exercise 7(b)pwun 4192
[Enderton] p. 30Theorem "Distributive laws"iinin1 3868  iinin2 3867  iinun2 3863  iunin1 3862  iunin2 3861
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3866  iundif2 3864
[Enderton] p. 32Exercise 20unineq 3323
[Enderton] p. 33Exercise 23iinuni 3880
[Enderton] p. 33Exercise 25iununi 3881
[Enderton] p. 33Exercise 24(a)iinpw 3885
[Enderton] p. 33Exercise 24(b)iunpw 4458  iunpwss 3886
[Enderton] p. 36Definitionopthwiener 4158
[Enderton] p. 38Exercise 6(a)unipw 4115
[Enderton] p. 38Exercise 6(b)pwuni 4097
[Enderton] p. 41Lemma 3Dopeluu 4414  rnex 4846  rnexg 4844
[Enderton] p. 41Exercise 8dmuni 4792  rnuni 4996
[Enderton] p. 42Definition of a functiondffun7 5135  dffun8 5136
[Enderton] p. 43Definition of function valuefunfv2 5436
[Enderton] p. 43Definition of single-rootedfuncnv 5164
[Enderton] p. 44Definition (d)dfima2 4918  dfima3 4919
[Enderton] p. 47Theorem 3Hfvco2 5443
[Enderton] p. 49Axiom of Choice (first form)ac7 7981  ac7g 7982  df-ac 7624  dfac2 7638  dfac2a 7637  dfac3 7629  dfac7 7639
[Enderton] p. 50Theorem 3K(a)imauni 5621
[Enderton] p. 52Definitiondf-map 6657
[Enderton] p. 53Exercise 21coass 5094
[Enderton] p. 53Exercise 27dmco 5084
[Enderton] p. 53Exercise 14(a)funin 5173
[Enderton] p. 53Exercise 22(a)imass2 4953
[Enderton] p. 54Remarkixpf 6721  ixpssmap 6733
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6701
[Enderton] p. 55Axiom of Choice (second form)ac9 7991  ac9s 8001
[Enderton] p. 56Theorem 3Merref 6563
[Enderton] p. 57Lemma 3Nerthi 6589
[Enderton] p. 57Definitiondf-ec 6545
[Enderton] p. 58Definitiondf-qs 6549
[Enderton] p. 60Theorem 3Qth3q 6650  th3qcor 6649  th3qlem1 6647  th3qlem2 6648
[Enderton] p. 61Exercise 35df-ec 6545
[Enderton] p. 65Exercise 56(a)dmun 4789
[Enderton] p. 68Definition of successordf-suc 4288
[Enderton] p. 71Definitiondf-tr 4008  dftr4 4012
[Enderton] p. 72Theorem 4Eunisuc 4358
[Enderton] p. 73Exercise 6unisuc 4358
[Enderton] p. 73Exercise 5(a)truni 4021
[Enderton] p. 73Exercise 5(b)trint 4022  trintALT 27285
[Enderton] p. 79Theorem 4I(A1)nna0 6485
[Enderton] p. 79Theorem 4I(A2)nnasuc 6487  onasuc 6410
[Enderton] p. 79Definition of operation valuedf-ov 5710
[Enderton] p. 80Theorem 4J(A1)nnm0 6486
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6488  onmsuc 6411
[Enderton] p. 81Theorem 4K(1)nnaass 6503
[Enderton] p. 81Theorem 4K(2)nna0r 6490  nnacom 6498
[Enderton] p. 81Theorem 4K(3)nndi 6504
[Enderton] p. 81Theorem 4K(4)nnmass 6505
[Enderton] p. 81Theorem 4K(5)nnmcom 6507
[Enderton] p. 82Exercise 16nnm0r 6491  nnmsucr 6506
[Enderton] p. 88Exercise 23nnaordex 6519
[Enderton] p. 129Definitiondf-en 6747
[Enderton] p. 132Theorem 6B(b)canth 6175
[Enderton] p. 133Exercise 1xpomen 7524
[Enderton] p. 133Exercise 2qnnen 12328
[Enderton] p. 134Theorem (Pigeonhole Principle)php 6927
[Enderton] p. 135Corollary 6Cphp3 6929
[Enderton] p. 136Corollary 6Enneneq 6926
[Enderton] p. 136Corollary 6D(a)pssinf 6955
[Enderton] p. 136Corollary 6D(b)ominf 6957
[Enderton] p. 137Lemma 6Fpssnn 6963
[Enderton] p. 138Corollary 6Gssfi 6965
[Enderton] p. 139Theorem 6H(c)mapen 6907
[Enderton] p. 142Theorem 6I(3)xpcdaen 7690
[Enderton] p. 142Theorem 6I(4)mapcdaen 7691
[Enderton] p. 143Theorem 6Jcda0en 7686  cda1en 7682
[Enderton] p. 144Exercise 13iunfi 7026  unifi 7027  unifi2 7028
[Enderton] p. 144Corollary 6Kundif2 3433  unfi 7006  unfi2 7008
[Enderton] p. 145Figure 38ffoss 5359
[Enderton] p. 145Definitiondf-dom 6748
[Enderton] p. 146Example 1domen 6758  domeng 6759
[Enderton] p. 146Example 3nndomo 6936  nnsdom 7235  nnsdomg 6998
[Enderton] p. 149Theorem 6L(a)cdadom2 7694
[Enderton] p. 149Theorem 6L(c)mapdom1 6908  xpdom1 6843  xpdom1g 6841  xpdom2g 6840
[Enderton] p. 149Theorem 6L(d)mapdom2 6914
[Enderton] p. 151Theorem 6Mzorn 8015  zorng 8012
[Enderton] p. 151Theorem 6M(4)ac8 8000  dfac5 7636
[Enderton] p. 159Theorem 6Qunictb 8074
[Enderton] p. 164Exampleinfdif 7716
[Enderton] p. 168Definitiondf-po 4204
[Enderton] p. 192Theorem 7M(a)oneli 4388
[Enderton] p. 192Theorem 7M(b)ontr1 4328
[Enderton] p. 192Theorem 7M(c)onirri 4387
[Enderton] p. 193Corollary 7N(b)0elon 4335
[Enderton] p. 193Corollary 7N(c)onsuci 4517
[Enderton] p. 193Corollary 7N(d)ssonunii 4467
[Enderton] p. 194Remarkonprc 4464
[Enderton] p. 194Exercise 16suc11 4384
[Enderton] p. 197Definitiondf-card 7453
[Enderton] p. 197Theorem 7Pcarden 8052
[Enderton] p. 200Exercise 25tfis 4533
[Enderton] p. 202Lemma 7Tr1tr 7329
[Enderton] p. 202Definitiondf-r1 7317
[Enderton] p. 202Theorem 7Qr1val1 7339
[Enderton] p. 204Theorem 7V(b)rankval4 7420
[Enderton] p. 206Theorem 7X(b)en2lp 7198
[Enderton] p. 207Exercise 30rankpr 7410  rankprb 7404  rankpw 7396  rankpwi 7376  rankuniss 7419
[Enderton] p. 207Exercise 34opthreg 7200
[Enderton] p. 208Exercise 35suc11reg 7201
[Enderton] p. 212Definition of alephalephval3 7618
[Enderton] p. 213Theorem 8A(a)alephord2 7584
[Enderton] p. 213Theorem 8A(b)cardalephex 7598
[Enderton] p. 218Theorem Schema 8Eonfununi 6241
[Enderton] p. 222Definition of kardkarden 7446  kardex 7445
[Enderton] p. 238Theorem 8Roeoa 6478
[Enderton] p. 238Theorem 8Soeoe 6480
[Enderton] p. 240Exercise 25oarec 6443
[Enderton] p. 257Definition of cofinalitycflm 7757
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18688
[Fremlin5] p. 213Lemma 565Cauniioovol 18728
[Fremlin5] p. 214Lemma 565Cauniioombl 18738
[FreydScedrov] p. 283Axiom of Infinityax-inf 7220  inf1 7204  inf2 7205
[Gleason] p. 117Proposition 9-2.1df-enq 8412  enqer 8422
[Gleason] p. 117Proposition 9-2.2df-1nq 8417  df-nq 8413
[Gleason] p. 117Proposition 9-2.3df-plpq 8409  df-plq 8415
[Gleason] p. 119Proposition 9-2.4caovmo 5906  df-mpq 8410  df-mq 8416
[Gleason] p. 119Proposition 9-2.5df-rq 8418
[Gleason] p. 119Proposition 9-2.6ltexnq 8476
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8477  ltbtwnnq 8479
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8472
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8473
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8480
[Gleason] p. 121Definition 9-3.1df-np 8482
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8494
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8496
[Gleason] p. 122Definitiondf-1p 8483
[Gleason] p. 122Remark (1)prub 8495
[Gleason] p. 122Lemma 9-3.4prlem934 8534
[Gleason] p. 122Proposition 9-3.2df-ltp 8486
[Gleason] p. 122Proposition 9-3.3ltsopr 8533  psslinpr 8532  supexpr 8555  suplem1pr 8553  suplem2pr 8554
[Gleason] p. 123Proposition 9-3.5addclpr 8519  addclprlem1 8517  addclprlem2 8518  df-plp 8484
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8523
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8522
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8535
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8544  ltexprlem1 8537  ltexprlem2 8538  ltexprlem3 8539  ltexprlem4 8540  ltexprlem5 8541  ltexprlem6 8542  ltexprlem7 8543
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8546  ltaprlem 8545
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8547
[Gleason] p. 124Lemma 9-3.6prlem936 8548
[Gleason] p. 124Proposition 9-3.7df-mp 8485  mulclpr 8521  mulclprlem 8520  reclem2pr 8549
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8530
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8525
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8524
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8529
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8552  reclem3pr 8550  reclem4pr 8551
[Gleason] p. 126Proposition 9-4.1df-enr 8558  df-mpr 8557  df-plpr 8556  enrer 8567
[Gleason] p. 126Proposition 9-4.2df-0r 8563  df-1r 8564  df-nr 8559
[Gleason] p. 126Proposition 9-4.3df-mr 8561  df-plr 8560  negexsr 8601  recexsr 8606  recexsrlem 8602
[Gleason] p. 127Proposition 9-4.4df-ltr 8562
[Gleason] p. 130Proposition 10-1.3creui 9589  creur 9588  cru 9586
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8687  axcnre 8663
[Gleason] p. 132Definition 10-3.1crim 11441  crimd 11558  crimi 11519  crre 11440  crred 11557  crrei 11518
[Gleason] p. 132Definition 10-3.2remim 11443  remimd 11524
[Gleason] p. 133Definition 10.36absval2 11610  absval2d 11766  absval2i 11719
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11467  cjaddd 11546  cjaddi 11514
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11468  cjmuld 11547  cjmuli 11515
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11466  cjcjd 11525  cjcji 11497
[Gleason] p. 133Proposition 10-3.4(f)cjre 11465  cjreb 11449  cjrebd 11528  cjrebi 11500  cjred 11552  rere 11448  rereb 11446  rerebd 11527  rerebi 11499  rered 11550
[Gleason] p. 133Proposition 10-3.4(h)addcj 11474  addcjd 11538  addcji 11509
[Gleason] p. 133Proposition 10-3.7(a)absval 11564
[Gleason] p. 133Proposition 10-3.7(b)abscj 11605  abscjd 11771  abscji 11723
[Gleason] p. 133Proposition 10-3.7(c)abs00 11615  abs00d 11767  abs00i 11720  absne0d 11768
[Gleason] p. 133Proposition 10-3.7(d)releabs 11644  releabsd 11772  releabsi 11724
[Gleason] p. 133Proposition 10-3.7(f)absmul 11618  absmuld 11775  absmuli 11726
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11608  sqabsaddi 11727
[Gleason] p. 133Proposition 10-3.7(h)abstri 11653  abstrid 11777  abstrii 11730
[Gleason] p. 134Definition 10-4.1df-exp 10948  exp0 10951  expp1 10953  expp1d 11088
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 19828  cxpaddd 19866  expadd 10987  expaddd 11089  expaddz 10989
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 19837  cxpmuld 19883  expmul 10990  expmuld 11090  expmulz 10991
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 19834  mulcxpd 19877  mulexp 10984  mulexpd 11102  mulexpz 10985
[Gleason] p. 140Exercise 1znnen 12327
[Gleason] p. 141Definition 11-2.1fzval 10627
[Gleason] p. 168Proposition 12-2.1(a)climadd 11944  rlimadd 11955  rlimdiv 11958
[Gleason] p. 168Proposition 12-2.1(b)climsub 11946  rlimsub 11956
[Gleason] p. 168Proposition 12-2.1(c)climmul 11945  rlimmul 11957
[Gleason] p. 171Corollary 12-2.2climmulc2 11949
[Gleason] p. 172Corollary 12-2.5climrecl 11896
[Gleason] p. 172Proposition 12-2.4(c)climabs 11916  climcj 11917  climim 11919  climre 11918  rlimabs 11921  rlimcj 11922  rlimim 11924  rlimre 11923
[Gleason] p. 173Definition 12-3.1df-ltxr 8749  df-xr 8748  ltxr 10303
[Gleason] p. 175Definition 12-4.1df-limsup 11784  limsupval 11787
[Gleason] p. 180Theorem 12-5.1climsup 11982
[Gleason] p. 180Theorem 12-5.3caucvg 11990  caucvgb 11991  caucvgr 11987  climcau 11983
[Gleason] p. 182Exercise 3cvgcmp 12113
[Gleason] p. 182Exercise 4cvgrat 12175
[Gleason] p. 195Theorem 13-2.12abs1m 11658
[Gleason] p. 217Lemma 13-4.1btwnzge0 10796
[Gleason] p. 223Definition 14-1.1df-met 16168
[Gleason] p. 223Definition 14-1.1(a)met0 17702  xmet0 17701
[Gleason] p. 223Definition 14-1.1(b)metgt0 17717
[Gleason] p. 223Definition 14-1.1(c)metsym 17708
[Gleason] p. 223Definition 14-1.1(d)mettri 17710  mstri 17809  xmettri 17709  xmstri 17808
[Gleason] p. 225Definition 14-1.5xpsmet 17740
[Gleason] p. 230Proposition 14-2.6txlm 17136
[Gleason] p. 240Theorem 14-4.3metcnp4 18529
[Gleason] p. 240Proposition 14-4.2metcnp3 17880
[Gleason] p. 243Proposition 14-4.16addcn 18163  addcn2 11906  mulcn 18165  mulcn2 11908  subcn 18164  subcn2 11907
[Gleason] p. 295Remarkbcval3 11161  bcval4 11162
[Gleason] p. 295Equation 2bcpasc 11175
[Gleason] p. 295Definition of binomial coefficientbcval 11159  df-bc 11158
[Gleason] p. 296Remarkbcn0 11165  bcnn 11166
[Gleason] p. 296Theorem 15-2.8binom 12127
[Gleason] p. 308Equation 2ef0 12208
[Gleason] p. 308Equation 3efcj 12209
[Gleason] p. 309Corollary 15-4.3efne0 12213
[Gleason] p. 309Corollary 15-4.4efexp 12217
[Gleason] p. 310Equation 14sinadd 12280
[Gleason] p. 310Equation 15cosadd 12281
[Gleason] p. 311Equation 17sincossq 12292
[Gleason] p. 311Equation 18cosbnd 12297  sinbnd 12296
[Gleason] p. 311Lemma 15-4.7sqeqor 11059  sqeqori 11057
[Gleason] p. 311Definition of pidf-pi 12190
[Godowski] p. 730Equation SFgoeqi 22612
[GodowskiGreechie] p. 249Equation IV3oai 22024
[Halmos] p. 31Theorem 17.3riesz1 22404  riesz2 22405
[Halmos] p. 41Definition of Hermitianhmopadj2 22280
[Halmos] p. 42Definition of projector orderingpjordi 22512
[Halmos] p. 43Theorem 26.1elpjhmop 22524  elpjidm 22523  pjnmopi 22487
[Halmos] p. 44Remarkpjinormi 22043  pjinormii 22032
[Halmos] p. 44Theorem 26.2elpjch 22528  pjrn 22063  pjrni 22058  pjvec 22052
[Halmos] p. 44Theorem 26.3pjnorm2 22083
[Halmos] p. 44Theorem 26.4hmopidmpj 22493  hmopidmpji 22491
[Halmos] p. 45Theorem 27.1pjinvari 22530
[Halmos] p. 45Theorem 27.3pjoci 22519  pjocvec 22053
[Halmos] p. 45Theorem 27.4pjorthcoi 22508
[Halmos] p. 48Theorem 29.2pjssposi 22511
[Halmos] p. 48Theorem 29.3pjssdif1i 22514  pjssdif2i 22513
[Halmos] p. 50Definition of spectrumdf-spec 22194
[Hamilton] p. 28Definition 2.1ax-1 7
[Hamilton] p. 31Example 2.7(a)id1 22
[Hamilton] p. 73Rule 1ax-mp 10
[Hamilton] p. 74Rule 2ax-gen 1536
[Hatcher] p. 25Definitiondf-phtpc 18284  df-phtpy 18263
[Hatcher] p. 26Definitiondf-pco 18297  df-pi1 18300
[Hatcher] p. 26Proposition 1.2phtpcer 18287
[Hatcher] p. 26Proposition 1.3pi1grp 18342
[Herstein] p. 54Exercise 28df-grpo 20617
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14295  grpoideu 20635  mndideu 14172
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14313  grpoinveu 20648
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14332  grpo2inv 20665
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14341  grpoinvop 20667
[Herstein] p. 57Exercise 1isgrp2d 20661  isgrp2i 20662
[Hitchcock] p. 5Rule A3mpto1 1528
[Hitchcock] p. 5Rule A4mpto2 1529
[Hitchcock] p. 5Rule A5mtp-xor 1530
[Holland] p. 1519Theorem 2sumdmdi 22759
[Holland] p. 1520Lemma 5cdj1i 22772  cdj3i 22780  cdj3lem1 22773  cdjreui 22771
[Holland] p. 1524Lemma 7mddmdin0i 22770
[Holland95] p. 13Theorem 3.6hlathil 30781
[Holland95] p. 14Line 15hgmapvs 30711
[Holland95] p. 14Line 16hdmaplkr 30733
[Holland95] p. 14Line 17hdmapellkr 30734
[Holland95] p. 14Line 19hdmapglnm2 30731
[Holland95] p. 14Line 20hdmapip0com 30737
[Holland95] p. 14Theorem 3.6hdmapevec2 30656
[Holland95] p. 14Lines 24 and 25hdmapoc 30751
[Holland95] p. 204Definition of involutiondf-srng 15408
[Holland95] p. 212Definition of subspacedf-psubsp 28319
[Holland95] p. 214Lemma 3.3lclkrlem2v 30345
[Holland95] p. 214Definition 3.2df-lpolN 30298
[Holland95] p. 214Definition of nonsingularpnonsingN 28749
[Holland95] p. 215Lemma 3.3(1)dihoml4 30194  poml4N 28769
[Holland95] p. 215Lemma 3.3(2)dochexmid 30285  pexmidALTN 28794  pexmidN 28785
[Holland95] p. 218Theorem 3.6lclkr 30350
[Holland95] p. 218Definition of dual vector spacedf-ldual 27941  ldualset 27942
[Holland95] p. 222Item 1df-lines 28317  df-pointsN 28318
[Holland95] p. 222Item 2df-polarityN 28719
[Holland95] p. 223Remarkispsubcl2N 28763  omllaw4 28063  pol1N 28726  polcon3N 28733
[Holland95] p. 223Definitiondf-psubclN 28751
[Holland95] p. 223Equation for polaritypolval2N 28722
[Hughes] p. 44Equation 1.21bax-his3 21422
[Hughes] p. 47Definition of projection operatordfpjop 22521
[Hughes] p. 49Equation 1.30eighmre 22302  eigre 22174  eigrei 22173
[Hughes] p. 49Equation 1.31eighmorth 22303  eigorth 22177  eigorthi 22176
[Hughes] p. 137Remark (ii)eigposi 22175
[Indrzejczak] p. 33Definition ` `Enatded 4  natded 4
[Indrzejczak] p. 33Definition ` `Inatded 4
[Indrzejczak] p. 34Definition ` `Enatded 4  natded 4
[Indrzejczak] p. 34Definition ` `Inatded 4
[Jech] p. 4Definition of classcv 1618  cvjust 2248
[Jech] p. 42Lemma 6.1alephexp1 8078
[Jech] p. 42Equation 6.1alephadd 8076  alephmul 8077
[Jech] p. 43Lemma 6.2infmap 8075  infmap2 7725
[Jech] p. 71Lemma 9.3jech9.3 7367
[Jech] p. 72Equation 9.3scott0 7437  scottex 7436
[Jech] p. 72Exercise 9.1rankval4 7420
[Jech] p. 72Scheme "Collection Principle"cp 7442
[Jech] p. 78Definition implied by the footnoteopthprc 4640
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26095
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26191
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26192
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26107
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26111
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26112  rmyp1 26113
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26114  rmym1 26115
[JonesMatijasevic] p. 695Equation 2.11rmx0 26105  rmx1 26106  rmxluc 26116
[JonesMatijasevic] p. 695Equation 2.12rmy0 26109  rmy1 26110  rmyluc 26117
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26119
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26120
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26142  jm2.17b 26143  jm2.17c 26144
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26181
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26185
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26176
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26145  jm2.24nn 26141
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26190
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26196  rmygeid 26146
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26208
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1684
[Kalmbach] p. 14Definition of latticechabs1 21854  chabs1i 21856  chabs2 21855  chabs2i 21857  chjass 21871  chjassi 21824  latabs1 13999  latabs2 14000
[Kalmbach] p. 15Definition of atomdf-at 22677  ela 22678
[Kalmbach] p. 15Definition of coverscvbr2 22622  cvrval2 28091
[Kalmbach] p. 16Definitiondf-ol 27995  df-oml 27996
[Kalmbach] p. 20Definition of commutescmbr 21940  cmbri 21946  cmtvalN 28028  df-cm 21939  df-cmtN 27994
[Kalmbach] p. 22Remarkomllaw5N 28064  pjoml5 21969  pjoml5i 21944
[Kalmbach] p. 22Definitionpjoml2 21967  pjoml2i 21941
[Kalmbach] p. 22Theorem 2(v)cmcm 21970  cmcmi 21948  cmcmii 21953  cmtcomN 28066
[Kalmbach] p. 22Theorem 2(ii)omllaw3 28062  omlsi 21742  pjoml 21774  pjomli 21773
[Kalmbach] p. 22Definition of OML lawomllaw2N 28061
[Kalmbach] p. 23Remarkcmbr2i 21952  cmcm3 21971  cmcm3i 21950  cmcm3ii 21955  cmcm4i 21951  cmt3N 28068  cmt4N 28069  cmtbr2N 28070
[Kalmbach] p. 23Lemma 3cmbr3 21964  cmbr3i 21956  cmtbr3N 28071
[Kalmbach] p. 25Theorem 5fh1 21974  fh1i 21977  fh2 21975  fh2i 21978  omlfh1N 28075
[Kalmbach] p. 65Remarkchjatom 22696  chslej 21836  chsleji 21796  shslej 21718  shsleji 21708
[Kalmbach] p. 65Proposition 1chocin 21833  chocini 21792  chsupcl 21678  chsupval2 21748  h0elch 21593  helch 21582  hsupval2 21747  ocin 21634  ococss 21631  shococss 21632
[Kalmbach] p. 65Definition of subspace sumshsval 21650
[Kalmbach] p. 66Remarkdf-pjh 21733  pjssmi 22504  pjssmii 22037
[Kalmbach] p. 67Lemma 3osum 22001  osumi 21998
[Kalmbach] p. 67Lemma 4pjci 22539
[Kalmbach] p. 103Exercise 6atmd2 22739
[Kalmbach] p. 103Exercise 12mdsl0 22649
[Kalmbach] p. 140Remarkhatomic 22699  hatomici 22698  hatomistici 22701
[Kalmbach] p. 140Proposition 1atlatmstc 28136
[Kalmbach] p. 140Proposition 1(i)atexch 22720  lsatexch 27860
[Kalmbach] p. 140Proposition 1(ii)chcv1 22694  cvlcvr1 28156  cvr1 28226
[Kalmbach] p. 140Proposition 1(iii)cvexch 22713  cvexchi 22708  cvrexch 28236
[Kalmbach] p. 149Remark 2chrelati 22703  hlrelat 28218  hlrelat5N 28217  lrelat 27831
[Kalmbach] p. 153Exercise 5lsmcv 15691  lsmsatcv 27827  spansncv 22009  spansncvi 22008
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 27846  spansncv2 22632
[Kalmbach] p. 266Definitiondf-st 22550
[Kalmbach2] p. 8Definition of adjointdf-adjh 22188
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8145  fpwwe2 8142
[KanamoriPincus] p. 416Corollary 1.3canth4 8146
[KanamoriPincus] p. 417Corollary 1.6canthp1 8153
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8148
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8150
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8163
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8167  gchxpidm 8168
[KanamoriPincus] p. 419Theorem 2.1gchacg 8171  gchhar 8170
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7723  unxpwdom 7184
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8173
[Kreyszig] p. 3Property M1metcl 17691  xmetcl 17690
[Kreyszig] p. 4Property M2meteq0 17698
[Kreyszig] p. 8Definition 1.1-8dscmet 17889
[Kreyszig] p. 12Equation 5conjmul 9333  muleqadd 9270
[Kreyszig] p. 18Definition 1.3-2mopnval 17778
[Kreyszig] p. 19Remarkmopntopon 17779
[Kreyszig] p. 19Theorem T1mopn0 17838  mopnm 17784
[Kreyszig] p. 19Theorem T2unimopn 17836
[Kreyszig] p. 19Definition of neighborhoodneibl 17841
[Kreyszig] p. 20Definition 1.3-3metcnp2 17882
[Kreyszig] p. 25Definition 1.4-1lmbr 16782  lmmbr 18478  lmmbr2 18479
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 16902
[Kreyszig] p. 28Theorem 1.4-5lmcau 18532
[Kreyszig] p. 28Definition 1.4-3iscau 18496  iscmet2 18514
[Kreyszig] p. 30Theorem 1.4-7cmetss 18534
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 16981  metelcls 18524
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18525  metcld2 18526
[Kreyszig] p. 51Equation 2clmvneg1 18383  lmodvneg1 15464  nvinv 20956  vcm 20886
[Kreyszig] p. 51Equation 1aclm0vs 18382  lmod0vs 15460  vc0 20884
[Kreyszig] p. 51Equation 1blmodvs0 15461  vcz 20885
[Kreyszig] p. 58Definition 2.2-1imsmet 21019
[Kreyszig] p. 59Equation 1imsdval 21014  imsdval2 21015
[Kreyszig] p. 63Problem 1nvnd 21016
[Kreyszig] p. 64Problem 2nvge0 20999  nvz 20994
[Kreyszig] p. 64Problem 3nvabs 20998
[Kreyszig] p. 91Definition 2.7-1isblo3i 21138
[Kreyszig] p. 92Equation 2df-nmoo 21082
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21144  blocni 21142
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21143
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18433  ipeq0 16336  ipz 21054
[Kreyszig] p. 135Problem 2pythi 21187
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21191
[Kreyszig] p. 144Equation 4supcvg 12150
[Kreyszig] p. 144Theorem 3.3-1minvec 18594  minveco 21222
[Kreyszig] p. 196Definition 3.9-1df-aj 21087
[Kreyszig] p. 247Theorem 4.7-2bcth 18545
[Kreyszig] p. 249Theorem 4.7-3ubth 21211
[Kreyszig] p. 470Definition of positive operator orderingleop 22462  leopg 22461
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22480
[Kreyszig] p. 525Theorem 10.1-1htth 21257
[Kunen] p. 10Axiom 0a9e 1817  axnul 4042
[Kunen] p. 11Axiom 3axnul 4042
[Kunen] p. 12Axiom 6zfrep6 5597
[Kunen] p. 24Definition 10.24mapval 6667  mapvalg 6665
[Kunen] p. 30Lemma 10.20fodom 8030
[Kunen] p. 31Definition 10.24mapex 6661
[Kunen] p. 95Definition 2.1df-r1 7317
[Kunen] p. 97Lemma 2.10r1elss 7359  r1elssi 7358
[Kunen] p. 107Exercise 4rankop 7411  rankopb 7405  rankuni 7416  rankxplim 7430  rankxpsuc 7433
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3810
[Laboreo] p. 10Definition ITnatded 4
[Laboreo] p. 10Definition I` `m,nnatded 4
[Laboreo] p. 11Definition E=>m,nnatded 4
[Laboreo] p. 11Definition I=>m,nnatded 4
[Laboreo] p. 11Definition E` `(1)natded 4
[Laboreo] p. 11Definition E` `(2)natded 4
[Laboreo] p. 12Definition E` `m,n,pnatded 4
[Laboreo] p. 12Definition I` `n(1)natded 4
[Laboreo] p. 12Definition I` `n(2)natded 4
[Laboreo] p. 13Definition I` `m,n,pnatded 4
[Laboreo] p. 14Definition E` `nnatded 4
[Laboreo] p. 15Theorem 5.2ex-natded5.2-2 20584  ex-natded5.2 20583
[Laboreo] p. 16Theorem 5.3ex-natded5.3-2 20587  ex-natded5.3 20586
[Laboreo] p. 18Theorem 5.5ex-natded5.5 26809
[Laboreo] p. 19Theorem 5.7ex-natded5.7-2 20590  ex-natded5.7 20589
[Laboreo] p. 20Theorem 5.8ex-natded5.8-2 20592  ex-natded5.8 20591
[Laboreo] p. 20Theorem 5.13ex-natded5.13-2 20594  ex-natded5.13 20593
[Laboreo] p. 32Definition I` `nnatded 4
[Laboreo] p. 32Definition E` `m,n,p,anatded 4
[Laboreo] p. 32Definition E` `n,tnatded 4
[Laboreo] p. 32Definition I` `n,tnatded 4
[Laboreo] p. 43Theorem 9.20ex-natded9.20 26810
[Laboreo] p. 45Theorem 9.20ex-natded9.20-2 26811
[Laboreo] p. 45Theorem 9.26ex-natded9.26-2 26815  ex-natded9.26-wheeler1 26816  ex-natded9.26-wheeler2 26813  ex-natded9.26-wheeler3 26812  ex-natded9.26 26814
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26646
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26641
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26647
[LeBlanc] p. 277Rule R2axnul 4042
[Levy] p. 338Axiomdf-clab 2240  df-clel 2249  df-cleq 2246
[Levy58] p. 2Definition Iisfin1-3 7893
[Levy58] p. 2Definition IIdf-fin2 7793
[Levy58] p. 2Definition Iadf-fin1a 7792
[Levy58] p. 2Definition IIIdf-fin3 7795
[Levy58] p. 3Definition Vdf-fin5 7796
[Levy58] p. 3Definition IVdf-fin4 7794
[Levy58] p. 4Definition VIdf-fin6 7797
[Levy58] p. 4Definition VIIdf-fin7 7798
[Levy58], p. 3Theorem 1fin1a2 7922
[Lopez-Astorga] p. 12Rule 1mpto1 1528
[Lopez-Astorga] p. 12Rule 2mpto2 1529
[Lopez-Astorga] p. 12Rule 3mtp-xor 1530
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 22747
[Maeda] p. 168Lemma 5mdsym 22751  mdsymi 22750
[Maeda] p. 168Lemma 4(i)mdsymlem4 22745  mdsymlem6 22747  mdsymlem7 22748
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22749
[MaedaMaeda] p. 1Remarkssdmd1 22652  ssdmd2 22653  ssmd1 22650  ssmd2 22651
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22648
[MaedaMaeda] p. 1Definition 1.1df-dmd 22620  df-md 22619  mdbr 22633
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22670  mdslj1i 22658  mdslj2i 22659  mdslle1i 22656  mdslle2i 22657  mdslmd1i 22668  mdslmd2i 22669
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22660  mdsl2bi 22662  mdsl2i 22661
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22674
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22671
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22672
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22649
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22654  mdsl3 22655
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22673
[MaedaMaeda] p. 4Theorem 1.14mdcompli 22768
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28138  hlrelat1 28216
[MaedaMaeda] p. 31Lemma 7.5lcvexch 27856
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22675  cvmdi 22663  cvnbtwn4 22628  cvrnbtwn4 28096
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22676
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28157  cvp 22714  cvrp 28232  lcvp 27857
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22738
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22737
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28150  hlexch4N 28208
[MaedaMaeda] p. 34Exercise 7.1atabsi 22740
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28259
[MaedaMaeda] p. 61Definition 15.10psubN 28565  atpsubN 28569  df-pointsN 28318  pointpsubN 28567
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28320  pmap11 28578  pmaple 28577  pmapsub 28584  pmapval 28573
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 28581  pmap1N 28583
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 28586  pmapglb2N 28587  pmapglb2xN 28588  pmapglbx 28585
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 28668
[MaedaMaeda] p. 67Postulate PS1ps-1 28293
[MaedaMaeda] p. 68Lemma 16.2df-padd 28612  paddclN 28658  paddidm 28657
[MaedaMaeda] p. 68Condition PS2ps-2 28294
[MaedaMaeda] p. 68Equation 16.2.1paddass 28654
[MaedaMaeda] p. 69Lemma 16.4ps-1 28293
[MaedaMaeda] p. 69Theorem 16.4ps-2 28294
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14781  lsmmod2 14782  lssats 27829  shatomici 22697  shatomistici 22700  shmodi 21728  shmodsi 21727
[MaedaMaeda] p. 130Remark 29.6dmdmd 22639  mdsymlem7 22748
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 21945
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 21831
[MaedaMaeda] p. 139Remarksumdmdii 22754
[Margaris] p. 40Rule Cexlimiv 2023
[Margaris] p. 49Axiom A1ax-1 7
[Margaris] p. 49Axiom A2ax-2 8
[Margaris] p. 49Axiom A3ax-3 9
[Margaris] p. 49Definitiondf-an 362  df-ex 1538  df-or 361  dfbi2 612
[Margaris] p. 51Theorem 1id1 22
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 27319
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27320
[Margaris] p. 79Rule Cexinst01 27025  exinst11 27026
[Margaris] p. 89Theorem 19.219.2 1759  r19.2z 3446
[Margaris] p. 89Theorem 19.319.3 1760  rr19.3v 2844
[Margaris] p. 89Theorem 19.5alcom 1568
[Margaris] p. 89Theorem 19.6alex 1570
[Margaris] p. 89Theorem 19.7alnex 1569
[Margaris] p. 89Theorem 19.819.8a 1758
[Margaris] p. 89Theorem 19.919.9 1762  19.9v 2010
[Margaris] p. 89Theorem 19.11excom 1765  excomim 1764
[Margaris] p. 89Theorem 19.1219.12 1766  r19.12 2616
[Margaris] p. 90Theorem 19.14exnal 1572
[Margaris] p. 90Theorem 19.152albi 26671  albi 1552  ralbi 2639
[Margaris] p. 90Theorem 19.1619.16 1767
[Margaris] p. 90Theorem 19.1719.17 1768
[Margaris] p. 90Theorem 19.182exbi 26673  exbi 1579
[Margaris] p. 90Theorem 19.1919.19 1769
[Margaris] p. 90Theorem 19.202alim 26670  alim 1548  alimd 1705  alimdh 1551  alimdv 2017  ralimdaa 2580  ralimdv 2582  ralimdva 2581  sbcimdv 2979
[Margaris] p. 90Theorem 19.2119.21-2 1772  19.21 1771  19.21bi 1774  19.21t 1770  19.21v 2011  19.21vv 26669  alrimd 1710  alrimdd 1709  alrimdh 1585  alrimdv 2014  alrimi 1706  alrimih 1553  alrimiv 2012  alrimivv 2013  r19.21 2589  r19.21be 2604  r19.21bi 2601  r19.21t 2588  r19.21v 2590  ralrimd 2591  ralrimdv 2592  ralrimdva 2593  ralrimdvv 2597  ralrimdvva 2598  ralrimi 2584  ralrimiv 2585  ralrimiva 2586  ralrimivv 2594  ralrimivva 2595  ralrimivvva 2596  ralrimivw 2587  rexlimi 2620
[Margaris] p. 90Theorem 19.222alimdv 2019  2exim 26672  2eximdv 2020  exim 1573  eximd 1711  eximdh 1586  eximdv 2018  rexim 2607  reximdai 2611  reximdv 2614  reximdv2 2612  reximdva 2615  reximdvai 2613  reximi2 2609
[Margaris] p. 90Theorem 19.2319.23 1777  19.23bi 1783  19.23t 1776  19.23v 2021  19.23vv 2022  exlimd 1784  exlimdh 1785  exlimdv 1932  exlimdvv 2026  exlimexi 26918  exlimi 1781  exlimih 1782  exlimiv 2023  exlimivv 2025  r19.23 2618  r19.23v 2619  rexlimd 2624  rexlimdv 2626  rexlimdv3a 2629  rexlimdva 2627  rexlimdvaa 2628  rexlimdvv 2633  rexlimdvva 2634  rexlimdvw 2630  rexlimiv 2621  rexlimiva 2622  rexlimivv 2632
[Margaris] p. 90Theorem 19.2419.24 1793
[Margaris] p. 90Theorem 19.2519.25 1602
[Margaris] p. 90Theorem 19.2619.26-2 1593  19.26-3an 1594  19.26 1592  r19.26-2 2636  r19.26-2a 24028  r19.26-3 2637  r19.26 2635  r19.26m 2638
[Margaris] p. 90Theorem 19.2719.27 1786  19.27v 2027  r19.27av 2641  r19.27z 3455  r19.27zv 3456
[Margaris] p. 90Theorem 19.2819.28 1787  19.28v 2028  19.28vv 26679  r19.28av 2642  r19.28z 3449  r19.28zv 3452  rr19.28v 2845
[Margaris] p. 90Theorem 19.2919.29 1595  19.29r 1596  19.29r2 1597  19.29x 1598  r19.29 2643  r19.29r 2644
[Margaris] p. 90Theorem 19.3019.30 1603  r19.30 2645
[Margaris] p. 90Theorem 19.3119.31 1795  19.31vv 26677
[Margaris] p. 90Theorem 19.3219.32 1794  r19.32v 2646
[Margaris] p. 90Theorem 19.3319.33-2 26675  19.33 1606  19.33b 1607
[Margaris] p. 90Theorem 19.3419.34 1798
[Margaris] p. 90Theorem 19.3519.35 1599  19.35i 1600  19.35ri 1601  r19.35 2647
[Margaris] p. 90Theorem 19.3619.36 1788  19.36aiv 2030  19.36i 1789  19.36v 2029  19.36vv 26676  r19.36av 2648  r19.36zv 3457
[Margaris] p. 90Theorem 19.3719.37 1790  19.37aiv 2033  19.37v 2032  19.37vv 26678  r19.37 2649  r19.37av 2650  r19.37zv 3453
[Margaris] p. 90Theorem 19.3819.38 1791
[Margaris] p. 90Theorem 19.3919.39 1792
[Margaris] p. 90Theorem 19.4019.40-2 1609  19.40 1608  r19.40 2651
[Margaris] p. 90Theorem 19.4119.41 1799  19.41rg 26947  19.41v 2034  19.41vv 2035  19.41vvv 2036  19.41vvvv 2037  r19.41 2652  r19.41v 2653
[Margaris] p. 90Theorem 19.4219.42 1800  19.42v 2038  19.42vv 2040  19.42vvv 2041  r19.42v 2654
[Margaris] p. 90Theorem 19.4319.43 1604  r19.43 2655
[Margaris] p. 90Theorem 19.4419.44 1796  r19.44av 2656
[Margaris] p. 90Theorem 19.4519.45 1797  r19.45av 2657  r19.45zv 3454
[Margaris] p. 110Exercise 2(b)eu1 2134
[Mayet] p. 370Remarkjpi 22609  largei 22606  stri 22596
[Mayet3] p. 9Definition of CH-statesdf-hst 22551  ishst 22553
[Mayet3] p. 10Theoremhstrbi 22605  hstri 22604
[Mayet3] p. 1223Theorem 4.1mayete3i 22084
[Mayet3] p. 1240Theorem 7.1mayetes3i 22086
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22617
[MegPav2000] p. 2345Definition 3.4-1chintcl 21670  chsupcl 21678
[MegPav2000] p. 2345Definition 3.4-2hatomic 22699
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22693
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22720
[MegPav2000] p. 2366Figure 7pl42N 28799
[MegPav2002] p. 362Lemma 2.2latj31 14011  latj32 14009  latjass 14007
[Megill] p. 444Axiom C5ax-17 1628
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 1837  alequcom 1680  ax-10 1678
[Megill] p. 446Lemma L17equtrr 1827
[Megill] p. 446Lemma L18ax9from9o 1816
[Megill] p. 446Lemma L19hbnae-o 1845  hbnae 1844
[Megill] p. 447Remark 9.1df-sb 1883  sbid 1895  sbidd-misc 26807  sbidd 26806
[Megill] p. 448Remark 9.6ax15 2101
[Megill] p. 448Scheme C4'ax-5o 1694
[Megill] p. 448Scheme C5'ax-4 1692
[Megill] p. 448Scheme C6'ax-7 1535
[Megill] p. 448Scheme C7'ax-6o 1697
[Megill] p. 448Scheme C8'ax-8 1623
[Megill] p. 448Scheme C9'ax-12o 1664
[Megill] p. 448Scheme C10'ax-9 1684  ax-9o 1815
[Megill] p. 448Scheme C11'ax-10o 1835
[Megill] p. 448Scheme C12'ax-13 1625
[Megill] p. 448Scheme C13'ax-14 1626
[Megill] p. 448Scheme C14'ax-15 2102
[Megill] p. 448Scheme C15'ax-11o 1940
[Megill] p. 448Scheme C16'ax-16 1926
[Megill] p. 448Theorem 9.4dral1-o 1856  dral1 1855  dral2-o 1858  dral2 1857  drex1 1859  drex2 1860  drsb1 1886  drsb2 1953
[Megill] p. 448Theorem 9.7conventions 3
[Megill] p. 449Theorem 9.7sbcom2 2074  sbequ 1952  sbid2v 2083
[Megill] p. 450Example in Appendixhba1 1718
[Mendelson] p. 35Axiom A3hirstL-ax3 26780
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4ra4sbc 2996  ra4sbca 2997  stdpc4 1896
[Mendelson] p. 69Axiom 5ax-5o 1694  ra5 3002  stdpc5 1773
[Mendelson] p. 81Rule Cexlimiv 2023
[Mendelson] p. 95Axiom 6stdpc6 1821
[Mendelson] p. 95Axiom 7stdpc7 1891
[Mendelson] p. 225Axiom system NBGru 2918
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4158
[Mendelson] p. 231Exercise 4.10(k)inv1 3385
[Mendelson] p. 231Exercise 4.10(l)unv 3386
[Mendelson] p. 231Exercise 4.10(n)dfin3 3312
[Mendelson] p. 231Exercise 4.10(o)df-nul 3360
[Mendelson] p. 231Exercise 4.10(q)dfin4 3313
[Mendelson] p. 231Exercise 4.10(s)ddif 3219
[Mendelson] p. 231Definition of uniondfun3 3311
[Mendelson] p. 235Exercise 4.12(c)univ 4453
[Mendelson] p. 235Exercise 4.12(d)pwv 3723
[Mendelson] p. 235Exercise 4.12(j)pwin 4187
[Mendelson] p. 235Exercise 4.12(k)pwunss 4188
[Mendelson] p. 235Exercise 4.12(l)pwssun 4189
[Mendelson] p. 235Exercise 4.12(n)uniin 3744
[Mendelson] p. 235Exercise 4.12(p)reli 4717
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5096
[Mendelson] p. 244Proposition 4.8(g)epweon 4463
[Mendelson] p. 246Definition of successordf-suc 4288
[Mendelson] p. 250Exercise 4.36oelim2 6476
[Mendelson] p. 254Proposition 4.22(b)xpen 6906
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6828  xpsneng 6829
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6835  xpcomeng 6836
[Mendelson] p. 254Proposition 4.22(e)xpassen 6838
[Mendelson] p. 255Definitionbrsdom 6767
[Mendelson] p. 255Exercise 4.39endisj 6831
[Mendelson] p. 255Exercise 4.41mapprc 6659
[Mendelson] p. 255Exercise 4.43mapsnen 6820
[Mendelson] p. 255Exercise 4.45mapunen 6912
[Mendelson] p. 255Exercise 4.47xpmapen 6911
[Mendelson] p. 255Exercise 4.42(a)map0e 6688
[Mendelson] p. 255Exercise 4.42(b)map1 6821
[Mendelson] p. 257Proposition 4.24(a)undom 6832
[Mendelson] p. 258Exercise 4.56(b)cdaen 7680
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7689  cdacomen 7688
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7693
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7687
[Mendelson] p. 258Definition of cardinal sumcdaval 7677  df-cda 7675
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6413
[Mendelson] p. 266Proposition 4.34(f)oaordex 6439
[Mendelson] p. 275Proposition 4.42(d)entri3 8060
[Mendelson] p. 281Definitiondf-r1 7317
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7366
[Mendelson] p. 287Axiom system MKru 2918
[Mittelstaedt] p. 9Definitiondf-oc 21590
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3295
[Monk1] p. 33Theorem 3.2(i)ssrel 4680
[Monk1] p. 33Theorem 3.2(ii)eqrel 4681
[Monk1] p. 34Definition 3.3df-opab 3972
[Monk1] p. 36Theorem 3.7(i)coi1 5091  coi2 5092
[Monk1] p. 36Theorem 3.8(v)dm0 4796  rn0 4840
[Monk1] p. 36Theorem 3.7(ii)cnvi 4989
[Monk1] p. 37Theorem 3.13(i)relxp 4698
[Monk1] p. 37Theorem 3.13(x)dmxp 4801  rnxp 5010
[Monk1] p. 37Theorem 3.13(ii)xp0 5002  xp0r 4672
[Monk1] p. 38Theorem 3.16(ii)ima0 4934
[Monk1] p. 38Theorem 3.16(viii)imai 4931
[Monk1] p. 39Theorem 3.17imaexg 4930
[Monk1] p. 39Theorem 3.16(xi)imassrn 4929
[Monk1] p. 41Theorem 4.3(i)fnopfv 5509  funfvop 5486
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5415
[Monk1] p. 42Theorem 4.4(iii)fvelima 5423
[Monk1] p. 43Theorem 4.6funun 5150
[Monk1] p. 43Theorem 4.8(iv)dff13 5632  dff13f 5633
[Monk1] p. 46Theorem 4.15(v)funex 5592  funrnex 5596
[Monk1] p. 50Definition 5.4fniunfv 5622
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5059
[Monk1] p. 52Theorem 5.11(viii)ssint 3773
[Monk1] p. 52Definition 5.13 (i)1stval2 5986  df-1st 5971
[Monk1] p. 52Definition 5.13 (ii)2ndval2 5987  df-2nd 5972
[Monk1] p. 112Theorem 15.17(v)ranksn 7407  ranksnb 7380
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7408
[Monk1] p. 112Theorem 15.17(iii)rankun 7409  rankunb 7403
[Monk1] p. 113Theorem 15.18r1val3 7391
[Monk1] p. 113Definition 15.19df-r1 7317  r1val2 7390
[Monk1] p. 117Lemmazorn2 8014  zorn2g 8011
[Monk1] p. 133Theorem 18.11cardom 7500
[Monk1] p. 133Theorem 18.12canth3 8062
[Monk1] p. 133Theorem 18.14carduni 7495
[Monk2] p. 105Axiom C4ax-5 1533
[Monk2] p. 105Axiom C7ax-8 1623
[Monk2] p. 105Axiom C8ax-11 1624  ax-11o 1940
[Monk2] p. 105Axiom (C8)ax11v 1990
[Monk2] p. 108Lemma 5ax-5o 1694
[Monk2] p. 109Lemma 12ax-7 1535
[Monk2] p. 109Lemma 15equvin 1999  equvini 1879  eqvinop 4141
[Monk2] p. 113Axiom C5-1ax-17 1628
[Monk2] p. 113Axiom C5-2ax-6 1534
[Monk2] p. 113Axiom C5-3ax-7 1535
[Monk2] p. 114Lemma 21ax4 1691
[Monk2] p. 114Lemma 22ax5o 1693  hba1 1718
[Monk2] p. 114Lemma 23nfia1 1745
[Monk2] p. 114Lemma 24nfa2 1744  nfra2 2557
[Munkres] p. 77Example 2distop 16527  indistop 16533  indistopon 16532
[Munkres] p. 77Example 3fctop 16535  fctop2 16536
[Munkres] p. 77Example 4cctop 16537
[Munkres] p. 78Definition of basisdf-bases 16432  isbasis3g 16481
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13180  tgval2 16488
[Munkres] p. 79Remarktgcl 16501
[Munkres] p. 80Lemma 2.1tgval3 16495
[Munkres] p. 80Lemma 2.2tgss2 16519  tgss3 16518
[Munkres] p. 81Lemma 2.3basgen 16520  basgen2 16521
[Munkres] p. 89Definition of subspace topologyresttop 16685
[Munkres] p. 93Theorem 6.1(1)0cld 16569  topcld 16566
[Munkres] p. 93Theorem 6.1(2)iincld 16570
[Munkres] p. 93Theorem 6.1(3)uncld 16572
[Munkres] p. 94Definition of closureclsval 16568
[Munkres] p. 94Definition of interiorntrval 16567
[Munkres] p. 95Theorem 6.5(a)clsndisj 16606  elcls 16604
[Munkres] p. 95Theorem 6.5(b)elcls3 16614
[Munkres] p. 97Theorem 6.6clslp 16673  neindisj 16648
[Munkres] p. 97Corollary 6.7cldlp 16675
[Munkres] p. 97Definition of limit pointislp2 16671  lpval 16665
[Munkres] p. 98Definition of Hausdorff spacedf-haus 16837
[Munkres] p. 102Definition of continuous functiondf-cn 16751  iscn 16759  iscn2 16762
[Munkres] p. 107Theorem 7.2(g)cncnp 16803  cncnp2 16804  cncnpi 16801  df-cnp 16752  iscnp 16761  iscnp2 16763
[Munkres] p. 127Theorem 10.1metcn 17883
[Munkres] p. 128Theorem 10.3metcn4 18530
[NielsenChuang] p. 195Equation 4.73unierri 22443
[Pfenning] p. 17Definition XMnatded 4  natded 4
[Pfenning] p. 17Definition NNCnatded 4  notnotrd 107
[Pfenning] p. 17Definition ` `Cnatded 4
[Pfenning] p. 18Rule"natded 4
[Pfenning] p. 18Definition /\Inatded 4
[Pfenning] p. 18Definition ` `Enatded 4  natded 4  natded 4  natded 4  natded 4
[Pfenning] p. 18Definition ` `Inatded 4  natded 4  natded 4  natded 4  natded 4
[Pfenning] p. 18Definition ` `ELnatded 4
[Pfenning] p. 18Definition ` `ERnatded 4
[Pfenning] p. 18Definition ` `Ea,unatded 4
[Pfenning] p. 18Definition ` `IRnatded 4
[Pfenning] p. 18Definition ` `Ianatded 4
[Pfenning] p. 127Definition =Enatded 4
[Pfenning] p. 127Definition =Inatded 4
[Ponnusamy] p. 361Theorem 6.44cphip0l 18431  df-dip 21033  dip0l 21053  ip0l 16334
[Ponnusamy] p. 361Equation 6.45ipval 21035
[Ponnusamy] p. 362Equation I1dipcj 21049
[Ponnusamy] p. 362Equation I3cphdir 18434  dipdir 21179  ipdir 16337  ipdiri 21167
[Ponnusamy] p. 362Equation I4ipidsq 21045
[Ponnusamy] p. 362Equation 6.46ip0i 21162
[Ponnusamy] p. 362Equation 6.47ip1i 21164
[Ponnusamy] p. 362Equation 6.48ip2i 21165
[Ponnusamy] p. 363Equation I2cphass 18440  dipass 21182  ipass 16343  ipassi 21178
[Prugovecki] p. 186Definition of brabraval 22283  df-bra 22189
[Prugovecki] p. 376Equation 8.1df-kb 22190  kbval 22293
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22721
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 28704
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22735  atcvat4i 22736  cvrat3 28258  cvrat4 28259  lsatcvat3 27869
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22621  cvrval 28086  df-cv 22618  df-lcv 27836  lspsncv0 15695
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 28716
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 28717
[Quine] p. 16Definition 2.1df-clab 2240  rabid 2673
[Quine] p. 17Definition 2.1''dfsb7 2079
[Quine] p. 18Definition 2.7df-cleq 2246
[Quine] p. 19Definition 2.9conventions 3  df-v 2727
[Quine] p. 34Theorem 5.1abeq2 2354
[Quine] p. 35Theorem 5.2abid2 2366  abid2f 2410
[Quine] p. 40Theorem 6.1sb5 1993
[Quine] p. 40Theorem 6.2sb56 1991  sb6 1992
[Quine] p. 41Theorem 6.3df-clel 2249
[Quine] p. 41Theorem 6.4eqid 2253  eqid1 20599
[Quine] p. 41Theorem 6.5eqcom 2255
[Quine] p. 42Theorem 6.6df-sbc 2920
[Quine] p. 42Theorem 6.7dfsbcq 2921  dfsbcq2 2922
[Quine] p. 43Theorem 6.8vex 2728
[Quine] p. 43Theorem 6.9isset 2729
[Quine] p. 44Theorem 7.3cla4gf 2799  cla4gv 2803  cla4imgf 2797
[Quine] p. 44Theorem 6.11a4sbc 2931  a4sbcd 2932
[Quine] p. 44Theorem 6.12elex 2733
[Quine] p. 44Theorem 6.13elab 2849  elabg 2850  elabgf 2847
[Quine] p. 44Theorem 6.14noel 3363
[Quine] p. 48Theorem 7.2snprc 3596
[Quine] p. 48Definition 7.1df-pr 3548  df-sn 3547
[Quine] p. 49Theorem 7.4snss 3649  snssg 3653
[Quine] p. 49Theorem 7.5prss 3666  prssg 3667
[Quine] p. 49Theorem 7.6prid1 3635  prid1g 3633  prid2 3636  prid2g 3634  snid 3568  snidg 3566
[Quine] p. 51Theorem 7.13prex 4108  snex 4107  snexALT 4087
[Quine] p. 53Theorem 8.2unisn 3740  unisnALT 27330  unisng 3741
[Quine] p. 53Theorem 8.3uniun 3743
[Quine] p. 54Theorem 8.6elssuni 3750
[Quine] p. 54Theorem 8.7uni0 3749
[Quine] p. 56Theorem 8.17uniabio 6150
[Quine] p. 56Definition 8.18dfiota2 6141
[Quine] p. 57Theorem 8.19iotaval 6151
[Quine] p. 57Theorem 8.22iotanul 6155
[Quine] p. 58Theorem 8.23iotaex 6157
[Quine] p. 58Definition 9.1df-op 3550
[Quine] p. 61Theorem 9.5opabid 4161  opelopab 4176  opelopaba 4171  opelopabaf 4178  opelopabf 4179  opelopabg 4173  opelopabga 4168  oprabid 5731
[Quine] p. 64Definition 9.11df-xp 4591
[Quine] p. 64Definition 9.12df-cnv 4593
[Quine] p. 64Definition 9.15df-id 4199
[Quine] p. 65Theorem 10.3fun0 5161
[Quine] p. 65Theorem 10.4funi 5139
[Quine] p. 65Theorem 10.5funsn 5154  funsng 5152
[Quine] p. 65Definition 10.1df-fun 4599
[Quine] p. 65Definition 10.2args 4945  df-fv 4605
[Quine] p. 68Definition 10.11conventions 3  df-fv 4605  fv2 5370
[Quine] p. 124Theorem 17.3nn0opth2 11129  nn0opth2i 11128  nn0opthi 11127  omopthi 6538
[Quine] p. 177Definition 25.2df-rdg 6306
[Quine] p. 232Equation icarddom 8055
[Quine] p. 284Axiom 39(vi)funimaex 5184  funimaexg 5183
[Quine] p. 331Axiom system NFru 2918
[ReedSimon] p. 36Definition (iii)ax-his3 21422
[ReedSimon] p. 63Exercise 4(a)df-dip 21033  polid 21497  polid2i 21495  polidi 21496
[ReedSimon] p. 63Exercise 4(b)df-ph 21150
[ReedSimon] p. 195Remarklnophm 22358  lnophmi 22357
[Retherford] p. 49Exercise 1(i)leopadd 22471
[Retherford] p. 49Exercise 1(ii)leopmul 22473  leopmuli 22472
[Retherford] p. 49Exercise 1(iv)leoptr 22476
[Retherford] p. 49Definition VI.1df-leop 22191  leoppos 22465
[Retherford] p. 49Exercise 1(iii)leoptri 22475
[Retherford] p. 49Definition of operator orderingleop3 22464
[Rudin] p. 164Equation 27efcan 12212
[Rudin] p. 164Equation 30efzval 12218
[Rudin] p. 167Equation 48absefi 12312
[Sanford] p. 39Rule 3mtp-xor 1530
[Sanford] p. 39Rule 4mpto2 1529
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 10
[Sanford] p. 39Rule says, "if ` ` is not true, and ` ` implies ` ` , then ` ` must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" mto 169
[Sanford] p. 40Rule 1mpto1 1528
[Schechter] p. 51Definition of antisymmetryintasym 4962
[Schechter] p. 51Definition of irreflexivityintirr 4965
[Schechter] p. 51Definition of symmetrycnvsym 4961
[Schechter] p. 51Definition of transitivitycotr 4959
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13323
[Schechter] p. 79Definition of Moore closuredf-mrc 13324
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13325
[Schechter] p. 139Definition AC3dfac9 7643
[Schechter] p. 141Definition (MC)dfac11 26255
[Schechter] p. 149Axiom DC1ax-dc 7953  axdc3 7961
[Schechter] p. 187Definition of ring with unitisrng 15142  isrngo 20804
[Schechter] p. 276Remark 11.6.espan0 21880
[Schechter] p. 276Definition of spandf-span 21647  spanval 21671
[Schechter] p. 428Definition 15.35bastop1 16525
[Schwabhauser] p. 10Axiom A1axcgrrflx 23645
[Schwabhauser] p. 10Axiom A2axcgrtr 23646
[Schwabhauser] p. 10Axiom A3axcgrid 23647
[Schwabhauser] p. 11Axiom A4axsegcon 23658
[Schwabhauser] p. 11Axiom A5ax5seg 23669
[Schwabhauser] p. 11Axiom A6axbtwnid 23670
[Schwabhauser] p. 12Axiom A7axpasch 23672
[Schwabhauser] p. 12Axiom A8axlowdim2 23691
[Schwabhauser] p. 13Axiom A10axeuclid 23694
[Schwabhauser] p. 13Axiom A11axcont 23707
[Schwabhauser] p. 27Theorem 2.1cgrrflx 23713
[Schwabhauser] p. 27Theorem 2.2cgrcomim 23715
[Schwabhauser] p. 27Theorem 2.3cgrtr 23718
[Schwabhauser] p. 27Theorem 2.4cgrcoml 23722
[Schwabhauser] p. 27Theorem 2.5cgrcomr 23723
[Schwabhauser] p. 28Theorem 2.8cgrtriv 23728
[Schwabhauser] p. 28Theorem 2.105segofs 23732
[Schwabhauser] p. 28Definition 2.10df-ofs 23709
[Schwabhauser] p. 29Theorem 2.11cgrextend 23734
[Schwabhauser] p. 29Theorem 2.12segconeq 23736
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 23748  btwntriv2 23738
[Schwabhauser] p. 30Theorem 3.2btwncomim 23739
[Schwabhauser] p. 30Theorem 3.3btwntriv1 23742
[Schwabhauser] p. 30Theorem 3.4btwnswapid 23743
[Schwabhauser] p. 30Theorem 3.5btwnexch2 23749  btwnintr 23745
[Schwabhauser] p. 30Theorem 3.6btwnexch 23751  btwnexch3 23746
[Schwabhauser] p. 30Theorem 3.7btwnouttr 23750
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23690
[Schwabhauser] p. 32Theorem 3.14btwndiff 23753
[Schwabhauser] p. 33Theorem 3.17trisegint 23754
[Schwabhauser] p. 34Theorem 4.2ifscgr 23770
[Schwabhauser] p. 34Definition 4.1df-ifs 23765
[Schwabhauser] p. 35Theorem 4.3cgrsub 23771
[Schwabhauser] p. 35Theorem 4.5cgrxfr 23781
[Schwabhauser] p. 35Definition 4.4df-cgr3 23766
[Schwabhauser] p. 36Theorem 4.6btwnxfr 23782
[Schwabhauser] p. 36Theorem 4.11colinearperm1 23788  colinearperm2 23790  colinearperm3 23789  colinearperm4 23791  colinearperm5 23792
[Schwabhauser] p. 36Definition 4.10df-colinear 23767
[Schwabhauser] p. 37Theorem 4.12colineartriv1 23793
[Schwabhauser] p. 37Theorem 4.13colinearxfr 23801
[Schwabhauser] p. 37Theorem 4.14lineext 23802
[Schwabhauser] p. 37Theorem 4.16fscgr 23806
[Schwabhauser] p. 37Theorem 4.17linecgr 23807
[Schwabhauser] p. 37Definition 4.15df-fs 23768
[Schwabhauser] p. 38Theorem 4.18lineid 23809
[Schwabhauser] p. 38Theorem 4.19idinside 23810
[Schwabhauser] p. 39Theorem 5.1btwnconn1 23827
[Schwabhauser] p. 41Theorem 5.2btwnconn2 23828
[Schwabhauser] p. 41Theorem 5.3btwnconn3 23829
[Schwabhauser] p. 41Theorem 5.5brsegle2 23835
[Schwabhauser] p. 41Definition 5.4df-segle 23833
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 23836
[Schwabhauser] p. 42Theorem 5.7seglerflx 23838
[Schwabhauser] p. 42Theorem 5.8segletr 23840
[Schwabhauser] p. 42Theorem 5.9segleantisym 23841
[Schwabhauser] p. 42Theorem 5.10seglelin 23842
[Schwabhauser] p. 42Theorem 5.11seglemin 23839
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 23844
[Schwabhauser] p. 43Theorem 6.2btwnoutside 23851
[Schwabhauser] p. 43Theorem 6.3broutsideof3 23852
[Schwabhauser] p. 43Theorem 6.4broutsideof 23847  df-outsideof 23846
[Schwabhauser] p. 43Definition 6.1broutsideof2 23848
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 23853
[Schwabhauser] p. 44Theorem 6.6outsideofcom 23854
[Schwabhauser] p. 44Theorem 6.7outsideoftr 23855
[Schwabhauser] p. 44Theorem 6.11outsideofeu 23857
[Schwabhauser] p. 44Definition 6.8df-ray 23864
[Schwabhauser] p. 45Part 2df-lines2 23865
[Schwabhauser] p. 45Theorem 6.13outsidele 23858
[Schwabhauser] p. 45Theorem 6.15lineunray 23873
[Schwabhauser] p. 45Theorem 6.16lineelsb2 23874
[Schwabhauser] p. 45Theorem 6.17linecom 23876  linerflx1 23875  linerflx2 23877
[Schwabhauser] p. 45Theorem 6.18linethru 23879
[Schwabhauser] p. 45Definition 6.14df-line2 23863
[Schwabhauser] p. 46Theorem 6.19linethrueu 23882
[Schwabhauser] p. 46Theorem 6.21lineintmo 23883
[Shapiro] p. 230Theorem 6.5.1dchrhash 20276  dchrsum 20274  dchrsum2 20273  sumdchr 20277
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20278  sum2dchr 20279
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15098  ablfacrp2 15099
[Shapiro], p. 328Equation 9.2.4vmasum 20221
[Shapiro], p. 329Equation 9.2.7logfac2 20222
[Shapiro], p. 329Equation 9.2.9logfacrlim 20229
[Shapiro], p. 331Equation 9.2.13vmadivsum 20397
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20400
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20454  vmalogdivsum2 20453
[Shapiro], p. 375Theorem 9.4.1dirith 20444  dirith2 20443
[Shapiro], p. 375Equation 9.4.3rplogsum 20442  rpvmasum 20441  rpvmasum2 20427
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20402
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20440
[Shapiro], p. 377Lemma 9.4.1dchrisum 20407  dchrisumlem1 20404  dchrisumlem2 20405  dchrisumlem3 20406  dchrisumlema 20403
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20410
[Shapiro], p. 379Equation 9.4.16dchrmusum 20439  dchrmusumlem 20437  dchrvmasumlem 20438
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20409
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20411
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20435  dchrisum0re 20428  dchrisumn0 20436
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20421
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20425
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20426
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20481  pntrsumbnd2 20482  pntrsumo1 20480
[Shapiro], p. 405Equation 10.2.1mudivsum 20445
[Shapiro], p. 406Equation 10.2.6mulogsum 20447
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20449
[Shapiro], p. 407Equation 10.2.8mulog2sum 20452
[Shapiro], p. 418Equation 10.4.6logsqvma 20457
[Shapiro], p. 418Equation 10.4.8logsqvma2 20458
[Shapiro], p. 419Equation 10.4.10selberg 20463
[Shapiro], p. 420Equation 10.4.12selberg2lem 20465
[Shapiro], p. 420Equation 10.4.14selberg2 20466
[Shapiro], p. 422Equation 10.6.7selberg3 20474
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20475
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20472  selberg3lem2 20473
[Shapiro], p. 422Equation 10.4.23selberg4 20476
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20470
[Shapiro], p. 428Equation 10.6.2selbergr 20483
[Shapiro], p. 429Equation 10.6.8selberg3r 20484
[Shapiro], p. 430Equation 10.6.11selberg4r 20485
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20499
[Shapiro], p. 434Equation 10.6.27pntlema 20511  pntlemb 20512  pntlemc 20510  pntlemd 20509  pntlemg 20513
[Shapiro], p. 435Equation 10.6.29pntlema 20511
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20503
[Shapiro], p. 436Lemma 10.6.2pntibnd 20508
[Shapiro], p. 436Equation 10.6.34pntlema 20511
[Shapiro], p. 436Equation 10.6.35pntlem3 20524  pntleml 20526
[Stoll] p. 13Definition of symmetric differencesymdif1 3337
[Stoll] p. 16Exercise 4.40dif 3428  dif0 3427
[Stoll] p. 16Exercise 4.8difdifdir 3444
[Stoll] p. 17Theorem 5.1(5)undifv 3431
[Stoll] p. 19Theorem 5.2(13)undm 3330
[Stoll] p. 19Theorem 5.2(13')indm 3331
[Stoll] p. 20Remarkinvdif 3314
[Stoll] p. 25Definition of ordered tripledf-ot 3551
[Stoll] p. 43Definitionuniiun 3850
[Stoll] p. 44Definitionintiin 3851
[Stoll] p. 45Definitiondf-iin 3803
[Stoll] p. 45Definition indexed uniondf-iun 3802
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3337
[Strang] p. 242Section 6.3expgrowth 26647
[Suppes] p. 22Theorem 2eq0 3373
[Suppes] p. 22Theorem 4eqss 3112  eqssd 3114  eqssi 3113
[Suppes] p. 23Theorem 5ss0 3389  ss0b 3388
[Suppes] p. 23Theorem 6sstr 3105  sstrALT2 27239
[Suppes] p. 23Theorem 7pssirr 3193
[Suppes] p. 23Theorem 8pssn2lp 3194
[Suppes] p. 23Theorem 9psstr 3197
[Suppes] p. 23Theorem 10pssss 3189
[Suppes] p. 25Theorem 12elin 3263  elun 3223
[Suppes] p. 26Theorem 15inidm 3282
[Suppes] p. 26Theorem 16in0 3384
[Suppes] p. 27Theorem 23unidm 3225
[Suppes] p. 27Theorem 24un0 3383
[Suppes] p. 27Theorem 25ssun1 3245
[Suppes] p. 27Theorem 26ssequn1 3252
[Suppes] p. 27Theorem 27unss 3256
[Suppes] p. 27Theorem 28indir 3321
[Suppes] p. 27Theorem 29undir 3322
[Suppes] p. 28Theorem 32difid 3425  difidALT 3426
[Suppes] p. 29Theorem 33difin 3310
[Suppes] p. 29Theorem 34indif 3315
[Suppes] p. 29Theorem 35undif1 3432
[Suppes] p. 29Theorem 36difun2 3436
[Suppes] p. 29Theorem 37difin0 3430
[Suppes] p. 29Theorem 38disjdif 3429
[Suppes] p. 29Theorem 39difundi 3325
[Suppes] p. 29Theorem 40difindi 3327
[Suppes] p. 30Theorem 41nalset 4045
[Suppes] p. 39Theorem 61uniss 3745
[Suppes] p. 39Theorem 65uniop 4159
[Suppes] p. 41Theorem 70intsn 3793
[Suppes] p. 42Theorem 71intpr 3790  intprg 3791
[Suppes] p. 42Theorem 73op1stb 4457
[Suppes] p. 42Theorem 78intun 3789
[Suppes] p. 44Definition 15(a)dfiun2 3832  dfiun2g 3830
[Suppes] p. 44Definition 15(b)dfiin2 3833
[Suppes] p. 47Theorem 86elpw 3533  elpw2 4061  elpw2g 4060  elpwg 3534  elpwgdedVD 27321
[Suppes] p. 47Theorem 87pwid 3539
[Suppes] p. 47Theorem 89pw0 3659
[Suppes] p. 48Theorem 90pwpw0 3660
[Suppes] p. 52Theorem 101xpss12 4696
[Suppes] p. 52Theorem 102xpindi 4723  xpindir 4724
[Suppes] p. 52Theorem 103xpundi 4645  xpundir 4646
[Suppes] p. 54Theorem 105elirrv 7192
[Suppes] p. 58Theorem 2relss 4679
[Suppes] p. 59Theorem 4eldm 4780  eldm2 4781  eldm2g 4779  eldmg 4778
[Suppes] p. 59Definition 3df-dm 4595
[Suppes] p. 60Theorem 6dmin 4790
[Suppes] p. 60Theorem 8rnun 4993
[Suppes] p. 60Theorem 9rnin 4994
[Suppes] p. 60Definition 4dfrn2 4772
[Suppes] p. 61Theorem 11brcnv 4768  brcnvg 4766
[Suppes] p. 62Equation 5elcnv 4762  elcnv2 4763
[Suppes] p. 62Theorem 12relcnv 4955
[Suppes] p. 62Theorem 15cnvin 4992
[Suppes] p. 62Theorem 16cnvun 4990
[Suppes] p. 63Theorem 20co02 5089
[Suppes] p. 63Theorem 21dmcoss 4848
[Suppes] p. 63Definition 7df-co 4594
[Suppes] p. 64Theorem 26cnvco 4769
[Suppes] p. 64Theorem 27coass 5094
[Suppes] p. 65Theorem 31resundi 4873
[Suppes] p. 65Theorem 34elima 4921  elima2 4922  elima3 4923  elimag 4920
[Suppes] p. 65Theorem 35imaundi 4997
[Suppes] p. 66Theorem 40dminss 4999
[Suppes] p. 66Theorem 41imainss 5000
[Suppes] p. 67Exercise 11cnvxp 5001
[Suppes] p. 81Definition 34dfec2 6546
[Suppes] p. 82Theorem 72elec 6582  elecg 6581
[Suppes] p. 82Theorem 73erth 6587  erth2 6588
[Suppes] p. 83Theorem 74erdisj 6590
[Suppes] p. 89Theorem 96map0b 6689
[Suppes] p. 89Theorem 97map0 6691  map0g 6690
[Suppes] p. 89Theorem 98mapsn 6692
[Suppes] p. 89Theorem 99mapss 6693
[Suppes] p. 91Definition 12(ii)alephsuc 7576
[Suppes] p. 91Definition 12(iii)alephlim 7575
[Suppes] p. 92Theorem 1enref 6777  enrefg 6776
[Suppes] p. 92Theorem 2ensym 6793  ensymb 6792  ensymi 6794
[Suppes] p. 92Theorem 3entr 6795
[Suppes] p. 92Theorem 4unen 6825
[Suppes] p. 94Theorem 15endom 6771
[Suppes] p. 94Theorem 16ssdomg 6790
[Suppes] p. 94Theorem 17domtr 6796
[Suppes] p. 95Theorem 18sbth 6863
[Suppes] p. 97Theorem 23canth2 6896  canth2g 6897
[Suppes] p. 97Definition 3brsdom2 6867  df-sdom 6749  dfsdom2 6866
[Suppes] p. 97Theorem 21(i)sdomirr 6880
[Suppes] p. 97Theorem 22(i)domnsym 6869
[Suppes] p. 97Theorem 21(ii)sdomnsym 6868
[Suppes] p. 97Theorem 22(ii)domsdomtr 6878
[Suppes] p. 97Theorem 22(iv)brdom2 6774
[Suppes] p. 97Theorem 21(iii)sdomtr 6881
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6876
[Suppes] p. 98Exercise 4fundmen 6816  fundmeng 6817
[Suppes] p. 98Exercise 6xpdom3 6842
[Suppes] p. 98Exercise 11sdomentr 6877
[Suppes] p. 104Theorem 37fofi 7024
[Suppes] p. 104Theorem 38pwfi 7032
[Suppes] p. 105Theorem 40pwfi 7032
[Suppes] p. 111Axiom for cardinal numberscarden 8052
[Suppes] p. 130Definition 3df-tr 4008
[Suppes] p. 132Theorem 9ssonuni 4466
[Suppes] p. 134Definition 6df-suc 4288
[Suppes] p. 136Theorem Schema 22findes 4574  finds 4570  finds1 4573  finds2 4572
[Suppes] p. 151Theorem 42isfinite 7234  isfinite2 6997  isfiniteg 6999  unbnn 6995
[Suppes] p. 162Definition 5df-ltnq 8419  df-ltpq 8411
[Suppes] p. 197Theorem Schema 4tfindes 4541  tfinds 4538  tfinds2 4542
[Suppes] p. 209Theorem 18oaord1 6432
[Suppes] p. 209Theorem 21oaword2 6434
[Suppes] p. 211Theorem 25oaass 6442
[Suppes] p. 225Definition 8iscard2 7490
[Suppes] p. 227Theorem 56ondomon 8064
[Suppes] p. 228Theorem 59harcard 7492
[Suppes] p. 228Definition 12(i)aleph0 7574
[Suppes] p. 228Theorem Schema 61onintss 4332
[Suppes] p. 228Theorem Schema 62onminesb 4477  onminsb 4478
[Suppes] p. 229Theorem 64alephval2 8071
[Suppes] p. 229Theorem 65alephcard 7578
[Suppes] p. 229Theorem 66alephord2i 7585
[Suppes] p. 229Theorem 67alephnbtwn 7579
[Suppes] p. 229Definition 12df-aleph 7454
[Suppes] p. 242Theorem 6weth 8003
[Suppes] p. 242Theorem 8entric 8058
[Suppes] p. 242Theorem 9carden 8052
[TakeutiZaring] p. 8Axiom 1ax-ext 2234
[TakeutiZaring] p. 13Definition 4.5df-cleq 2246
[TakeutiZaring] p. 13Proposition 4.6df-clel 2249
[TakeutiZaring] p. 13Proposition 4.9cvjust 2248
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2270
[TakeutiZaring] p. 14Definition 4.16df-oprab 5711
[TakeutiZaring] p. 14Proposition 4.14ru 2918
[TakeutiZaring] p. 15Axiom 2zfpair 4103
[TakeutiZaring] p. 15Exercise 1elpr 3559  elpr2 3560  elprg 3558
[TakeutiZaring] p. 15Exercise 2elsn 3556  elsnc 3564  elsnc2 3570  elsnc2g 3569  elsncg 3563
[TakeutiZaring] p. 15Exercise 3elop 4129
[TakeutiZaring] p. 15Exercise 4sneq 3552  sneqr 3677
[TakeutiZaring] p. 15Definition 5.1dfpr2 3557  dfsn2 3555
[TakeutiZaring] p. 16Axiom 3uniex 4404
[TakeutiZaring] p. 16Exercise 6opth 4135
[TakeutiZaring] p. 16Exercise 7opex 4127
[TakeutiZaring] p. 16Exercise 8rext 4113
[TakeutiZaring] p. 16Corollary 5.8unex 4406  unexg 4409
[TakeutiZaring] p. 16Definition 5.3dftp2 3580
[TakeutiZaring] p. 16Definition 5.5df-uni 3725
[TakeutiZaring] p. 16Definition 5.6df-in 3082  df-un 3080
[TakeutiZaring] p. 16Proposition 5.7unipr 3738  uniprg 3739
[TakeutiZaring] p. 17Axiom 4pwex 4084  pwexg 4085
[TakeutiZaring] p. 17Exercise 1eltp 3579
[TakeutiZaring] p. 17Exercise 5elsuc 4351  elsucg 4349  sstr2 3104
[TakeutiZaring] p. 17Exercise 6uncom 3226
[TakeutiZaring] p. 17Exercise 7incom 3266
[TakeutiZaring] p. 17Exercise 8unass 3239
[TakeutiZaring] p. 17Exercise 9inass 3283
[TakeutiZaring] p. 17Exercise 10indi 3319
[TakeutiZaring] p. 17Exercise 11undi 3320
[TakeutiZaring] p. 17Definition 5.9df-pss 3088  dfss2 3089
[TakeutiZaring] p. 17Definition 5.10df-pw 3529
[TakeutiZaring] p. 18Exercise 7unss2 3253
[TakeutiZaring] p. 18Exercise 9df-ss 3086  sseqin2 3292
[TakeutiZaring] p. 18Exercise 10ssid 3115
[TakeutiZaring] p. 18Exercise 12inss1 3293  inss2 3294
[TakeutiZaring] p. 18Exercise 13nss 3154
[TakeutiZaring] p. 18Exercise 15unieq 3733
[TakeutiZaring] p. 18Exercise 18sspwb 4114  sspwimp 27322  sspwimpALT 27329  sspwimpALT2 27333  sspwimpcf 27324
[TakeutiZaring] p. 18Exercise 19pweqb 4121
[TakeutiZaring] p. 19Axiom 5ax-rep 4025
[TakeutiZaring] p. 20Definitiondf-rab 2514
[TakeutiZaring] p. 20Corollary 5.160ex 4044
[TakeutiZaring] p. 20Definition 5.12df-dif 3078
[TakeutiZaring] p. 20Definition 5.14dfnul2 3361
[TakeutiZaring] p. 20Proposition 5.15difid 3425  difidALT 3426
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3368  n0f 3367  neq0 3369
[TakeutiZaring] p. 21Axiom 6zfreg 7190
[TakeutiZaring] p. 21Axiom 6'zfregs 7295
[TakeutiZaring] p. 21Theorem 5.22setind 7300
[TakeutiZaring] p. 21Definition 5.20df-v 2727
[TakeutiZaring] p. 21Proposition 5.21vprc 4046
[TakeutiZaring] p. 22Exercise 10ss 3387
[TakeutiZaring] p. 22Exercise 3ssex 4052  ssexg 4054
[TakeutiZaring] p. 22Exercise 4inex1 4049
[TakeutiZaring] p. 22Exercise 5ruv 7195
[TakeutiZaring] p. 22Exercise 6elirr 7193
[TakeutiZaring] p. 22Exercise 7ssdif0 3417
[TakeutiZaring] p. 22Exercise 11difdif 3216
[TakeutiZaring] p. 22Exercise 13undif3 3333  undif3VD 27286
[TakeutiZaring] p. 22Exercise 14difss 3217
[TakeutiZaring] p. 22Exercise 15sscon 3221
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2511
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2512
[TakeutiZaring] p. 23Proposition 6.2xpex 4705  xpexg 4704  xpexgALT 5919
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4592
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5166
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5299  fun11 5169
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5122  svrelfun 5167
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4771
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4773
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4597
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4598
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4594
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5032  dfrel2 5028
[TakeutiZaring] p. 25Exercise 3xpss 4697
[TakeutiZaring] p. 25Exercise 5relun 4706
[TakeutiZaring] p. 25Exercise 6reluni 4712
[TakeutiZaring] p. 25Exercise 9inxp 4722
[TakeutiZaring] p. 25Exercise 12relres 4887
[TakeutiZaring] p. 25Exercise 13opelres 4864  opelresg 4866
[TakeutiZaring] p. 25Exercise 14dmres 4880
[TakeutiZaring] p. 25Exercise 15resss 4883
[TakeutiZaring] p. 25Exercise 17resabs1 4888
[TakeutiZaring] p. 25Exercise 18funres 5147
[TakeutiZaring] p. 25Exercise 24relco 5074
[TakeutiZaring] p. 25Exercise 29funco 5146
[TakeutiZaring] p. 25Exercise 30f1co 5300
[TakeutiZaring] p. 26Definition 6.10eu2 2138
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 4605  fv3 5390
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5112  cnvexg 5111
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4845  dmexg 4843
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4846  rnexg 4844
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 26754
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 26755
[TakeutiZaring] p. 27Corollary 6.13fvex 5388
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5393  tz6.12 5394  tz6.12c 5397
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5396  tz6.12i 5398
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4600
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4601
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4603  wfo 4587
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4602  wf1 4586
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4604  wf1o 4588
[TakeutiZaring] p. 28Exercise 4eqfnfv 5471  eqfnfv2 5472  eqfnfv2f 5475
[TakeutiZaring] p. 28Exercise 5fvco 5444
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5590  fnexALT 5591
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5586  resfunexgALT 5587
[TakeutiZaring] p. 29Exercise 9funimaex 5184  funimaexg 5183
[TakeutiZaring] p. 29Definition 6.18df-br 3918
[TakeutiZaring] p. 30Definition 6.21dffr2 4248  dffr3 4949  eliniseg 4946  iniseg 4948
[TakeutiZaring] p. 30Definition 6.22df-eprel 4195
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4261  fr3nr 4459  frirr 4260
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4242
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4461
[TakeutiZaring] p. 31Exercise 1frss 4250
[TakeutiZaring] p. 31Exercise 4wess 4270
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23302  tz6.26i 23303  wefrc 4277  wereu2 4280
[TakeutiZaring] p. 32Theorem 6.27wfi 23304  wfii 23305
[TakeutiZaring] p. 32Definition 6.28df-isom 4606
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5675
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5676
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5682
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5683
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5684
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5688
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5695
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5697
[TakeutiZaring] p. 35Notationwtr 4007
[TakeutiZaring] p. 35Theorem 7.2trelpss 26756  tz7.2 4267
[TakeutiZaring] p. 35Definition 7.1dftr3 4011
[TakeutiZaring] p. 36Proposition 7.4ordwe 4295
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4303
[TakeutiZaring] p. 36Proposition 7.6ordelord 4304  ordelordALT 26932  ordelordALTVD 27271
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4310  ordelssne 4309
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4308
[TakeutiZaring] p. 37Proposition 7.9ordin 4312
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4468
[TakeutiZaring] p. 38Corollary 7.15ordsson 4469
[TakeutiZaring] p. 38Definition 7.11df-on 4286
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4314
[TakeutiZaring] p. 38Proposition 7.12onfrALT 26945  ordon 4462
[TakeutiZaring] p. 38Proposition 7.13onprc 4464
[TakeutiZaring] p. 39Theorem 7.17tfi 4532
[TakeutiZaring] p. 40Exercise 3ontr2 4329
[TakeutiZaring] p. 40Exercise 7dftr2 4009
[TakeutiZaring] p. 40Exercise 9onssmin 4476
[TakeutiZaring] p. 40Exercise 11unon 4510
[TakeutiZaring] p. 40Exercise 12ordun 4382
[TakeutiZaring] p. 40Exercise 14ordequn 4381
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4465
[TakeutiZaring] p. 40Proposition 7.20elssuni 3750
[TakeutiZaring] p. 41Definition 7.22df-suc 4288
[TakeutiZaring] p. 41Proposition 7.23sssucid 4359  sucidg 4360
[TakeutiZaring] p. 41Proposition 7.24suceloni 4492
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4374  ordnbtwn 4373
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4507
[TakeutiZaring] p. 42Exercise 1df-lim 4287
[TakeutiZaring] p. 42Exercise 4omssnlim 4558
[TakeutiZaring] p. 42Exercise 7ssnlim 4562
[TakeutiZaring] p. 42Exercise 8onsucssi 4520  ordelsuc 4499
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4501
[TakeutiZaring] p. 42Definition 7.27nlimon 4530
[TakeutiZaring] p. 42Definition 7.28dfom2 4546
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4563
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4564
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4565
[TakeutiZaring] p. 43Remarkomon 4555
[TakeutiZaring] p. 43Axiom 7inf3 7217  omex 7225
[TakeutiZaring] p. 43Theorem 7.32ordom 4553
[TakeutiZaring] p. 43Corollary 7.31find 4569
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4566
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4567
[TakeutiZaring] p. 44Exercise 1limomss 4549
[TakeutiZaring] p. 44Exercise 2int0 3771  trint0 4024
[TakeutiZaring] p. 44Exercise 4intss1 3772
[TakeutiZaring] p. 44Exercise 5intex 4062
[TakeutiZaring] p. 44Exercise 6oninton 4479
[TakeutiZaring] p. 44Exercise 11ordintdif 4331
[TakeutiZaring] p. 44Definition 7.35df-int 3758
[TakeutiZaring] p. 44Proposition 7.34noinfep 7241
[TakeutiZaring] p. 45Exercise 4onint 4474
[TakeutiZaring] p. 47Lemma 1tfrlem1 6274
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6296
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6297
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6298
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6302  tz7.44-2 6303  tz7.44-3 6304
[TakeutiZaring] p. 50Exercise 1smogt 6267
[TakeutiZaring] p. 50Exercise 3smoiso 6262
[TakeutiZaring] p. 50Definition 7.46df-smo 6246
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6340  tz7.49c 6341
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6338
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6337
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6339
[TakeutiZaring] p. 53Proposition 7.532eu5 2197
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7520
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7521
[TakeutiZaring] p. 56Definition 8.1oalim 6414  oasuc 6406
[TakeutiZaring] p. 57Remarktfindsg 4539
[TakeutiZaring] p. 57Proposition 8.2oacl 6417
[TakeutiZaring] p. 57Proposition 8.3oa0 6398  oa0r 6420
[TakeutiZaring] p. 57Proposition 8.16omcl 6418
[TakeutiZaring] p. 58Corollary 8.5oacan 6429
[TakeutiZaring] p. 58Proposition 8.4nnaord 6500  nnaordi 6499  oaord 6428  oaordi 6427
[TakeutiZaring] p. 59Proposition 8.6iunss2 3842  uniss2 3753
[TakeutiZaring] p. 59Proposition 8.7oawordri 6431
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6436  oawordex 6438
[TakeutiZaring] p. 59Proposition 8.9nnacl 6492
[TakeutiZaring] p. 59Proposition 8.10oaabs 6525
[TakeutiZaring] p. 60Remarkoancom 7233
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6441
[TakeutiZaring] p. 62Exercise 1nnarcl 6497
[TakeutiZaring] p. 62Exercise 5oaword1 6433
[TakeutiZaring] p. 62Definition 8.15om0 6399  om0x 6401  omlim 6415  omsuc 6408
[TakeutiZaring] p. 63Proposition 8.17nnecl 6494  nnmcl 6493
[TakeutiZaring] p. 63Proposition 8.19nnmord 6513  nnmordi 6512  omord 6449  omordi 6447
[TakeutiZaring] p. 63Proposition 8.20omcan 6450
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6517  omwordri 6453
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6421
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6423  om1r 6424
[TakeutiZaring] p. 64Proposition 8.22om00 6456
[TakeutiZaring] p. 64Proposition 8.23omordlim 6458
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6459
[TakeutiZaring] p. 64Proposition 8.25odi 6460
[TakeutiZaring] p. 65Theorem 8.26omass 6461
[TakeutiZaring] p. 67Definition 8.30nnesuc 6489  oe0 6404  oelim 6416  oesuc 6409  onesuc 6412
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6402
[TakeutiZaring] p. 67Proposition 8.32oen0 6467
[TakeutiZaring] p. 67Proposition 8.33oeordi 6468
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6403
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6426
[TakeutiZaring] p. 68Corollary 8.34oeord 6469
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6475
[TakeutiZaring] p. 68Proposition 8.35oewordri 6473
[TakeutiZaring] p. 68Proposition 8.37oeworde 6474
[TakeutiZaring] p. 69Proposition 8.41oeoa 6478
[TakeutiZaring] p. 70Proposition 8.42oeoe 6480
[TakeutiZaring] p. 73Theorem 9.1trcl 7291  tz9.1 7292
[TakeutiZaring] p. 76Definition 9.9df-r1 7317  r10 7321  r1lim 7325  r1limg 7324  r1suc 7323  r1sucg 7322
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7333  r1ord2 7334  r1ordg 7331
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7343
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7368  tz9.13 7344  tz9.13g 7345
[TakeutiZaring] p. 79Definition 9.14df-rank 7318  rankval 7369  rankvalb 7350  rankvalg 7370
[TakeutiZaring] p. 79Proposition 9.16rankel 7392  rankelb 7377
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7406  rankval3 7393  rankval3b 7379
[TakeutiZaring] p. 79Proposition 9.18rankonid 7382
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7348
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7387  rankr1c 7374  rankr1g 7385
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7388
[TakeutiZaring] p. 80Exercise 1rankss 7402  rankssb 7401
[TakeutiZaring] p. 80Exercise 2unbndrank 7395
[TakeutiZaring] p. 80Proposition 9.19bndrank 7394
[TakeutiZaring] p. 83Axiom of Choiceac4 7983  dfac3 7629
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7538  numth 7980  numth2 7979
[TakeutiZaring] p. 85Definition 10.4cardval 8049
[TakeutiZaring] p. 85Proposition 10.5cardid 8050  cardid2 7467
[TakeutiZaring] p. 85Proposition 10.9oncard 7474
[TakeutiZaring] p. 85Proposition 10.10carden 8052
[TakeutiZaring] p. 85Proposition 10.11cardidm 7473
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7458
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7479
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7471
[TakeutiZaring] p. 87Proposition 10.15pwen 6916
[TakeutiZaring] p. 88Exercise 1en0 6806
[TakeutiZaring] p. 88Exercise 7infensuc 6921
[TakeutiZaring] p. 89Exercise 10omxpen 6846
[TakeutiZaring] p. 90Corollary 10.23cardnn 7477
[TakeutiZaring] p. 90Definition 10.27alephiso 7606
[TakeutiZaring] p. 90Proposition 10.20nneneq 6926
[TakeutiZaring] p. 90Proposition 10.22onomeneq 6932
[TakeutiZaring] p. 90Proposition 10.26alephprc 7607
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6931
[TakeutiZaring] p. 91Exercise 2alephle 7596
[TakeutiZaring] p. 91Exercise 3aleph0 7574
[TakeutiZaring] p. 91Exercise 4cardlim 7486
[TakeutiZaring] p. 91Exercise 7infpss 7724
[TakeutiZaring] p. 91Exercise 8infcntss 7012
[TakeutiZaring] p. 91Definition 10.29df-fin 6750  isfi 6768
[TakeutiZaring] p. 92Proposition 10.32onfin 6933
[TakeutiZaring] p. 92Proposition 10.34imadomg 8040
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6839
[TakeutiZaring] p. 93Proposition 10.35fodomb 8032
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7696  unxpdom 6952
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7488  cardsdomelir 7487
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 6954
[TakeutiZaring] p. 94Proposition 10.39infxpen 7523
[TakeutiZaring] p. 95Definition 10.42df-map 6657
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8063  infxpidm2 7525
[TakeutiZaring] p. 95Proposition 10.41infcda 7715  infxp 7722  infxpg 24189
[TakeutiZaring] p. 96Proposition 10.44pw2en 6851  pw2f1o 6849
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6909
[TakeutiZaring] p. 97Theorem 10.46ac6s3 7995
[TakeutiZaring] p. 98Theorem 10.46ac6c5 7990  ac6s5 7999
[TakeutiZaring] p. 98Theorem 10.47unidom 8046
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8047  uniimadomf 8048
[TakeutiZaring] p. 100Definition 11.1cfcof 7781
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7776
[TakeutiZaring] p. 102Exercise 1cfle 7761
[TakeutiZaring] p. 102Exercise 2cf0 7758
[TakeutiZaring] p. 102Exercise 3cfsuc 7764
[TakeutiZaring] p. 102Exercise 4cfom 7771
[TakeutiZaring] p. 102Proposition 11.9coftr 7780
[TakeutiZaring] p. 103Theorem 11.15alephreg 8081
[TakeutiZaring] p. 103Proposition 11.11cardcf 7759
[TakeutiZaring] p. 103Proposition 11.13alephsing 7783
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7605
[TakeutiZaring] p. 104Proposition 11.16carduniima 7604
[TakeutiZaring] p. 104Proposition 11.18alephfp 7616  alephfp2 7617
[TakeutiZaring] p. 106Theorem 11.20gchina 8198
[TakeutiZaring] p. 106Theorem 11.21mappwen 7620
[TakeutiZaring] p. 107Theorem 11.26konigth 8068
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8082
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8083
[Tarski] p. 67Axiom B5ax-4 1692
[Tarski] p. 68Lemma 6avril1 20595  equid 1818  equid1 1820  equidALT 1819
[Tarski] p. 69Lemma 7equcomi-o 1823  equcomi 1822
[Tarski] p. 70Lemma 14a4im 1867  a4ime 1868
[Tarski] p. 70Lemma 16ax-11 1624  ax-11o 1940  ax11i 1833
[Tarski] p. 70Lemmas 16 and 17sb6 1992
[Tarski] p. 75Axiom B8ax-9v 1632
[Tarski] p. 75Scheme B7ax9vax9 27785
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1628
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1625  ax-14 1626
[Truss] p. 114Theorem 5.18ruc 12357
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 501
[WhiteheadRussell] p. 96Axiom *1.3olc 375
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 377
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 510
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 817
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 162
[WhiteheadRussell] p. 100Theorem *2.02ax-1 7
[WhiteheadRussell] p. 100Theorem *2.03con2 110
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 78
[WhiteheadRussell] p. 100Theorem *2.05imim2 51
[WhiteheadRussell] p. 100Theorem *2.06imim1 72
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 408
[WhiteheadRussell] p. 101Theorem *2.06barbara 2210  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 387
[WhiteheadRussell] p. 101Theorem *2.08id 21  id1 22
[WhiteheadRussell] p. 101Theorem *2.11exmid 406
[WhiteheadRussell] p. 101Theorem *2.12notnot1 116
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 409
[WhiteheadRussell] p. 102Theorem *2.14notnot2 106  notnot2ALT2 27331
[WhiteheadRussell] p. 102Theorem *2.15con1 122
[WhiteheadRussell] p. 103Theorem *2.16con3 128  con3th 929
[WhiteheadRussell] p. 103Theorem *2.17ax-3 9
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 104
[WhiteheadRussell] p. 104Theorem *2.2orc 376
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 558
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 102
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 103
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 395
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 858
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 37
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 513
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 514
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 819
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 820
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 818
[WhiteheadRussell] p. 105Definition *2.33df-3or 940
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 561
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 559
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 560
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 49
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 388
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 389
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 146
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 164
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 390
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 391
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 392
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 147
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 149
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 364
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 365
[WhiteheadRussell] p. 107Theorem *2.55orel1 373
[WhiteheadRussell] p. 107Theorem *2.56orel2 374
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 165
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 400
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 766
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 767
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 166
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 393  pm2.67 394
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 148
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 399
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 826
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 401
[WhiteheadRussell] p. 108Theorem *2.69looinv 176
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 821
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 822
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 825
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 824
[WhiteheadRussell] p. 108Theorem *2.77ax-2 8
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 827
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 828
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 73
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 829
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 96
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 486
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 436  pm3.2im 139
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 487
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 488
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 489
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 490
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 437
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 438
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 857
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 573
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 433
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 434
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 445  simplim 145
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 449  simprim 144
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 571
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 572
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 565
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 546
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 544
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 545
[WhiteheadRussell] p. 113Theorem *3.44jao 500  pm3.44 499
[WhiteheadRussell] p. 113Theorem *3.47prth 557
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 835
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 810
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 809
[WhiteheadRussell] p. 116Theorem *4.1con34b 285
[WhiteheadRussell] p. 117Theorem *4.2biid 229
[WhiteheadRussell] p. 117Theorem *4.11notbi 288
[WhiteheadRussell] p. 117Theorem *4.12con2bi 320
[WhiteheadRussell] p. 117Theorem *4.13notnot 284
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 564
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 567
[WhiteheadRussell] p. 117Theorem *4.21bicom 193
[WhiteheadRussell] p. 117Theorem *4.22biantr 902  bitr 692  wl-bitr 24023
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 627
[WhiteheadRussell] p. 117Theorem *4.25oridm 502  pm4.25 503
[WhiteheadRussell] p. 118Theorem *4.3ancom 439
[WhiteheadRussell] p. 118Theorem *4.4andi 842
[WhiteheadRussell] p. 118Theorem *4.31orcom 378
[WhiteheadRussell] p. 118Theorem *4.32anass 633
[WhiteheadRussell] p. 118Theorem *4.33orass 512
[WhiteheadRussell] p. 118Theorem *4.36anbi1 690
[WhiteheadRussell] p. 118Theorem *4.37orbi1 689
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 847
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 846
[WhiteheadRussell] p. 118Definition *4.34df-3an 941
[WhiteheadRussell] p. 119Theorem *4.41ordi 837
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 931
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 898
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 563
[WhiteheadRussell] p. 119Theorem *4.45orabs 831  pm4.45 672  pm4.45im 547
[WhiteheadRussell] p. 120Theorem *4.5anor 477
[WhiteheadRussell] p. 120Theorem *4.6imor 403
[WhiteheadRussell] p. 120Theorem *4.7anclb 532
[WhiteheadRussell] p. 120Theorem *4.51ianor 476
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 479
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 480
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 481
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 482
[WhiteheadRussell] p. 120Theorem *4.56ioran 478  pm4.56 483
[WhiteheadRussell] p. 120Theorem *4.57oran 484  pm4.57 485
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 417
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 410
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 412
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 363
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 418
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 411
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 419
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 614  pm4.71d 618  pm4.71i 616  pm4.71r 615  pm4.71rd 619  pm4.71ri 617
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 851
[WhiteheadRussell] p. 121Theorem *4.73iba 491
[WhiteheadRussell] p. 121Theorem *4.74biorf 396
[WhiteheadRussell] p. 121Theorem *4.76jcab 836  pm4.76 841
[WhiteheadRussell] p. 121Theorem *4.77jaob 761  pm4.77 765
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 568
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 569
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 356
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 357
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 899
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 900
[WhiteheadRussell] p. 122Theorem *4.84imbi1 315
[WhiteheadRussell] p. 122Theorem *4.85imbi2 316
[WhiteheadRussell] p. 122Theorem *4.86bibi1 319  wl-bibi1 24016
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 352  impexp 435  pm4.87 570
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 833
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 859
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 860
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 862
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 861
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 864
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 865
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 863
[WhiteheadRussell] p. 124Theorem *5.18nbbn 349  pm5.18 347
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 351
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 834
[WhiteheadRussell] p. 124Theorem *5.22xor 866
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 868
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 869
[WhiteheadRussell] p. 124Theorem *5.25dfor2 402
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 695
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 353
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 328
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 883
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 905
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 574
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 620
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 853
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 874
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 854
[WhiteheadRussell] p. 125Theorem *5.41imdi 354  pm5.41 355
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 533
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 882
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 774
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 875
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 872
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 696
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 894
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 895
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 907
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 332
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 237
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 908
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 26648
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26649
[WhiteheadRussell] p. 147Theorem *10.2219.26 1592
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26650
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26651
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26652
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1617
[WhiteheadRussell] p. 151Theorem *10.301albitr 26653
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26654
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26655
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26656
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26657
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26659
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26660
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26661
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26658
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26664
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2075
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26665
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26666
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1610
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26667
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26668
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26669
[WhiteheadRussell] p. 162Theorem *11.322alim 26670
[WhiteheadRussell] p. 162Theorem *11.332albi 26671
[WhiteheadRussell] p. 162Theorem *11.342exim 26672
[WhiteheadRussell] p. 162Theorem *11.36a4sbce-2 26674
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26673
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1609
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26676
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26677
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26675
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1571
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26678
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26679
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1578
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26680
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2024  pm11.53g 24058
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26681
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26686
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26682
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26683
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26684
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26685
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26690
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26687
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26688
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26689
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26691
[WhiteheadRussell] p. 175Definition *14.02df-eu 2118
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 26703  pm13.13b 26704
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 26705
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2483
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2484
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2843
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 26711
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 26712
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 26706
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 26949  pm13.193 26707
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 26708
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 26709
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 26710
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 26717
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 26716
[WhiteheadRussell] p. 184Definition *14.01iotasbc 26715
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2970
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 26718  pm14.122b 26719  pm14.122c 26720
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 26721  pm14.123b 26722  pm14.123c 26723
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 26725
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 26724
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 26726
[WhiteheadRussell] p. 190Theorem *14.22iota4 6158
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 26727
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6159
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 26728
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 26730
[WhiteheadRussell] p. 192Theorem *14.26eupick 2176  eupickbi 2179  sbaniota 26731
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 26729
[WhiteheadRussell] p. 192Theorem *14.271eubi 26732
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 26733
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 4605
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7514  pm54.43lem 7513
[Young] p. 141Definition of operator orderingleop2 22463
[Young] p. 142Example 12.2(i)0leop 22469  idleop 22470
[vandenDries] p. 42Lemma 61irrapx1 26008
[vandenDries] p. 43Theorem 62pellex 26015  pellexlem1 26009

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