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 13606
[Adamek] p. 29Proposition 3.14(1)invinv 13620
[Adamek] p. 29Proposition 3.14(2)invco 13621  isoco 13623
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25543
[AitkenIBCG] p. 3Definition 2df-angtrg 25539  df-trcng 25542
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25415  df-ig2 25414
[AitkenIBG] p. 2Definition 4df-li 25430
[AitkenIBG] p. 3Definition 5df-col 25444
[AitkenIBG] p. 3Definition 6df-con2 25449
[AitkenIBG] p. 3Proposition 4isconcl5a 25454  isconcl5ab 25455  isconcl6a 25456  isconcl6ab 25457
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25462
[AitkenIBG] p. 4Exercise 5tpne 25428
[AitkenIBG] p. 4Definition 8df-seg2 25484
[AitkenIBG] p. 4Definition 10df-sside 25516
[AitkenIBG] p. 4Definition 11df-ray2 25505
[AitkenIBG] p. 10Definition 17df-angle 25511
[AitkenIBG] p. 15Definition 23df-triangle 25513
[AitkenIBG] p. 15Definition 24df-cnvx 25532
[AitkenNG] p. 2Definition 1df-slices 25546
[AitkenNG] p. 2Definition 2df-Cut 25548
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25550
[AitkenNG] p. 4Definition 5df-crcl 25552
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18165  df-nmoo 21269
[AkhiezerGlazman] p. 64Theoremhmopidmch 22679  hmopidmchi 22677
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22727  pjcmul2i 22728
[AkhiezerGlazman] p. 72Theoremcnvunop 22444  unoplin 22446
[AkhiezerGlazman] p. 72Equation 2unopadj 22445  unopadj2 22464
[AkhiezerGlazman] p. 73Theoremelunop2 22539  lnopunii 22538
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22612
[Apostol] p. 18Theorem I.1addcan 8950  addcan2d 8970  addcan2i 8960  addcand 8969  addcani 8959
[Apostol] p. 18Theorem I.2negeu 8996
[Apostol] p. 18Theorem I.3negsub 9049  negsubd 9117  negsubi 9078
[Apostol] p. 18Theorem I.4negneg 9051  negnegd 9102  negnegi 9070
[Apostol] p. 18Theorem I.5subdi 9167  subdid 9189  subdii 9182  subdir 9168  subdird 9190  subdiri 9183
[Apostol] p. 18Theorem I.6mul01 8945  mul01d 8965  mul01i 8956  mul02 8944  mul02d 8964  mul02i 8955
[Apostol] p. 18Theorem I.7mulcan 9359  mulcan2d 9356  mulcand 9355  mulcani 9361
[Apostol] p. 18Theorem I.8receu 9367
[Apostol] p. 18Theorem I.9divrec 9394  divrecd 9493  divreci 9459  divreczi 9452
[Apostol] p. 18Theorem I.10recrec 9411  recreci 9446
[Apostol] p. 18Theorem I.11mul0or 9362  mul0ord 9372  mul0ori 9370
[Apostol] p. 18Theorem I.12mul2neg 9173  mul2negd 9188  mul2negi 9181  mulneg1 9170  mulneg1d 9186  mulneg1i 9179
[Apostol] p. 18Theorem I.13divadddiv 9429  divadddivd 9534  divadddivi 9476
[Apostol] p. 18Theorem I.14divmuldiv 9414  divmuldivd 9531  divmuldivi 9474
[Apostol] p. 18Theorem I.15divdivdiv 9415  divdivdivd 9537  divdivdivi 9477
[Apostol] p. 20Axiom 7rpaddcl 10327  rpaddcld 10358  rpmulcl 10328  rpmulcld 10359
[Apostol] p. 20Axiom 8rpneg 10336
[Apostol] p. 20Axiom 90nrp 10337
[Apostol] p. 20Theorem I.17lttri 8899
[Apostol] p. 20Theorem I.18ltadd1d 9319  ltadd1dd 9337  ltadd1i 9281
[Apostol] p. 20Theorem I.19ltmul1 9560  ltmul1a 9559  ltmul1i 9629  ltmul1ii 9639  ltmul2 9561  ltmul2d 10381  ltmul2dd 10395  ltmul2i 9632
[Apostol] p. 20Theorem I.20msqgt0 9248  msqgt0d 9294  msqgt0i 9264
[Apostol] p. 20Theorem I.210lt1 9250
[Apostol] p. 20Theorem I.23lt0neg1 9234  lt0neg1d 9296  ltneg 9228  ltnegd 9304  ltnegi 9271
[Apostol] p. 20Theorem I.25lt2add 9213  lt2addd 9348  lt2addi 9289
[Apostol] p. 20Definition of positive numbersdf-rp 10308
[Apostol] p. 21Exercise 4recgt0 9554  recgt0d 9645  recgt0i 9615  recgt0ii 9616
[Apostol] p. 22Definition of integersdf-z 9978
[Apostol] p. 22Definition of positive integersdfnn3 9714
[Apostol] p. 22Definition of rationalsdf-q 10270
[Apostol] p. 24Theorem I.26supeu 7159
[Apostol] p. 26Theorem I.28nnunb 9914
[Apostol] p. 26Theorem I.29arch 9915
[Apostol] p. 28Exercise 2btwnz 10067
[Apostol] p. 28Exercise 3nnrecl 9916
[Apostol] p. 28Exercise 4rebtwnz 10268
[Apostol] p. 28Exercise 5zbtwnre 10267
[Apostol] p. 28Exercise 6qbtwnre 10478
[Apostol] p. 28Exercise 10(a)zneo 10047
[Apostol] p. 29Theorem I.35msqsqrd 11873  resqrth 11692  sqrth 11799  sqrthi 11805  sqsqrd 11872
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9703
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10237
[Apostol] p. 361Remarkcrreczi 11178
[Apostol] p. 363Remarkabsgt0i 11833
[Apostol] p. 363Exampleabssubd 11886  abssubi 11837
[Baer] p. 40Property (b)mapdord 30979
[Baer] p. 40Property (c)mapd11 30980
[Baer] p. 40Property (e)mapdin 31003  mapdlsm 31005
[Baer] p. 40Property (f)mapd0 31006
[Baer] p. 40Definition of projectivitydf-mapd 30966  mapd1o 30989
[Baer] p. 41Property (g)mapdat 31008
[Baer] p. 44Part (1)mapdpg 31047
[Baer] p. 45Part (2)hdmap1eq 31143  mapdheq 31069  mapdheq2 31070  mapdheq2biN 31071
[Baer] p. 45Part (3)baerlem3 31054
[Baer] p. 46Part (4)mapdheq4 31073  mapdheq4lem 31072
[Baer] p. 46Part (5)baerlem5a 31055  baerlem5abmN 31059  baerlem5amN 31057  baerlem5b 31056  baerlem5bmN 31058
[Baer] p. 47Part (6)hdmap1l6 31163  hdmap1l6a 31151  hdmap1l6e 31156  hdmap1l6f 31157  hdmap1l6g 31158  hdmap1l6lem1 31149  hdmap1l6lem2 31150  hdmap1p6N 31164  mapdh6N 31088  mapdh6aN 31076  mapdh6eN 31081  mapdh6fN 31082  mapdh6gN 31083  mapdh6lem1N 31074  mapdh6lem2N 31075
[Baer] p. 48Part 9hdmapval 31172
[Baer] p. 48Part 10hdmap10 31184
[Baer] p. 48Part 11hdmapadd 31187
[Baer] p. 48Part (6)hdmap1l6h 31159  mapdh6hN 31084
[Baer] p. 48Part (7)mapdh75cN 31094  mapdh75d 31095  mapdh75e 31093  mapdh75fN 31096  mapdh7cN 31090  mapdh7dN 31091  mapdh7eN 31089  mapdh7fN 31092
[Baer] p. 48Part (8)mapdh8 31130  mapdh8a 31116  mapdh8aa 31117  mapdh8ab 31118  mapdh8ac 31119  mapdh8ad 31120  mapdh8b 31121  mapdh8c 31122  mapdh8d 31124  mapdh8d0N 31123  mapdh8e 31125  mapdh8fN 31126  mapdh8g 31127  mapdh8i 31128  mapdh8j 31129
[Baer] p. 48Part (9)mapdh9a 31131
[Baer] p. 48Equation 10mapdhvmap 31110
[Baer] p. 49Part 12hdmap11 31192  hdmapeq0 31188  hdmapf1oN 31209  hdmapneg 31190  hdmaprnN 31208  hdmaprnlem1N 31193  hdmaprnlem3N 31194  hdmaprnlem3uN 31195  hdmaprnlem4N 31197  hdmaprnlem6N 31198  hdmaprnlem7N 31199  hdmaprnlem8N 31200  hdmaprnlem9N 31201  hdmapsub 31191
[Baer] p. 49Part 14hdmap14lem1 31212  hdmap14lem10 31221  hdmap14lem1a 31210  hdmap14lem2N 31213  hdmap14lem2a 31211  hdmap14lem3 31214  hdmap14lem8 31219  hdmap14lem9 31220
[Baer] p. 50Part 14hdmap14lem11 31222  hdmap14lem12 31223  hdmap14lem13 31224  hdmap14lem14 31225  hdmap14lem15 31226  hgmapval 31231
[Baer] p. 50Part 15hgmapadd 31238  hgmapmul 31239  hgmaprnlem2N 31241  hgmapvs 31235
[Baer] p. 50Part 16hgmaprnN 31245
[Baer] p. 110Lemma 1hdmapip0com 31261
[Baer] p. 110Line 27hdmapinvlem1 31262
[Baer] p. 110Line 28hdmapinvlem2 31263
[Baer] p. 110Line 30hdmapinvlem3 31264
[Baer] p. 110Part 1.2hdmapglem5 31266  hgmapvv 31270
[Baer] p. 110Proposition 1hdmapinvlem4 31265
[Baer] p. 111Line 10hgmapvvlem1 31267
[Baer] p. 111Line 15hdmapg 31274  hdmapglem7 31273
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2121
[BellMachover] p. 460Notationdf-mo 2122
[BellMachover] p. 460Definitionmo3 2147
[BellMachover] p. 461Axiom Extax-ext 2237
[BellMachover] p. 462Theorem 1.1bm1.1 2241
[BellMachover] p. 463Axiom Repaxrep5 4096
[BellMachover] p. 463Scheme Sepaxsep 4100
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4104
[BellMachover] p. 466Axiom Powaxpow3 4149
[BellMachover] p. 466Axiom Unionaxun2 4472
[BellMachover] p. 468Definitiondf-ord 4353
[BellMachover] p. 469Theorem 2.2(i)ordirr 4368
[BellMachover] p. 469Theorem 2.2(iii)onelon 4375
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4370
[BellMachover] p. 471Definition of Ndf-om 4615
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4555
[BellMachover] p. 471Definition of Limdf-lim 4355
[BellMachover] p. 472Axiom Infzfinf2 7297
[BellMachover] p. 473Theorem 2.8limom 4629
[BellMachover] p. 477Equation 3.1df-r1 7390
[BellMachover] p. 478Definitionrankval2 7444
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7408  r1ord3g 7405
[BellMachover] p. 480Axiom Regzfreg2 7264
[BellMachover] p. 488Axiom ACac5 8058  dfac4 7703
[BellMachover] p. 490Definition of alephalephval3 7691
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28660
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22879
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22921  chirredi 22920
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22909
[Beran] p. 3Definition of joinsshjval3 21879
[Beran] p. 39Theorem 2.3(i)cmcm2 22159  cmcm2i 22136  cmcm2ii 22141  cmt2N 28591
[Beran] p. 40Theorem 2.3(iii)lecm 22160  lecmi 22145  lecmii 22146
[Beran] p. 45Theorem 3.4cmcmlem 22134
[Beran] p. 49Theorem 4.2cm2j 22163  cm2ji 22168  cm2mi 22169
[Beran] p. 95Definitiondf-sh 21732  issh2 21734
[Beran] p. 95Lemma 3.1(S5)his5 21611
[Beran] p. 95Lemma 3.1(S6)his6 21624
[Beran] p. 95Lemma 3.1(S7)his7 21615
[Beran] p. 95Lemma 3.2(S8)ho01i 22354
[Beran] p. 95Lemma 3.2(S9)hoeq1 22356
[Beran] p. 95Lemma 3.2(S10)ho02i 22355
[Beran] p. 95Lemma 3.2(S11)hoeq2 22357
[Beran] p. 95Postulate (S1)ax-his1 21607  his1i 21625
[Beran] p. 95Postulate (S2)ax-his2 21608
[Beran] p. 95Postulate (S3)ax-his3 21609
[Beran] p. 95Postulate (S4)ax-his4 21610
[Beran] p. 96Definition of normdf-hnorm 21494  dfhnorm2 21647  normval 21649
[Beran] p. 96Definition for Cauchy sequencehcau 21709
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21499
[Beran] p. 96Definition of complete subspaceisch3 21767
[Beran] p. 96Definition of convergedf-hlim 21498  hlimi 21713
[Beran] p. 97Theorem 3.3(i)norm-i-i 21658  norm-i 21654
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21662  norm-ii 21663  normlem0 21634  normlem1 21635  normlem2 21636  normlem3 21637  normlem4 21638  normlem5 21639  normlem6 21640  normlem7 21641  normlem7tALT 21644
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21664  norm-iii 21665
[Beran] p. 98Remark 3.4bcs 21706  bcsiALT 21704  bcsiHIL 21705
[Beran] p. 98Remark 3.4(B)normlem9at 21646  normpar 21680  normpari 21679
[Beran] p. 98Remark 3.4(C)normpyc 21671  normpyth 21670  normpythi 21667
[Beran] p. 99Remarklnfn0 22573  lnfn0i 22568  lnop0 22492  lnop0i 22496
[Beran] p. 99Theorem 3.5(i)nmcexi 22552  nmcfnex 22579  nmcfnexi 22577  nmcopex 22555  nmcopexi 22553
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22580  nmcfnlbi 22578  nmcoplb 22556  nmcoplbi 22554
[Beran] p. 99Theorem 3.5(iii)lnfncon 22582  lnfnconi 22581  lnopcon 22561  lnopconi 22560
[Beran] p. 100Lemma 3.6normpar2i 21681
[Beran] p. 101Lemma 3.6norm3adifi 21678  norm3adifii 21673  norm3dif 21675  norm3difi 21672
[Beran] p. 102Theorem 3.7(i)chocunii 21826  pjhth 21918  pjhtheu 21919  pjpjhth 21950  pjpjhthi 21951  pjth 18751
[Beran] p. 102Theorem 3.7(ii)ococ 21931  ococi 21930
[Beran] p. 103Remark 3.8nlelchi 22587
[Beran] p. 104Theorem 3.9riesz3i 22588  riesz4 22590  riesz4i 22589
[Beran] p. 104Theorem 3.10cnlnadj 22605  cnlnadjeu 22604  cnlnadjeui 22603  cnlnadji 22602  cnlnadjlem1 22593  nmopadjlei 22614
[Beran] p. 106Theorem 3.11(i)adjeq0 22617
[Beran] p. 106Theorem 3.11(v)nmopadji 22616
[Beran] p. 106Theorem 3.11(ii)adjmul 22618
[Beran] p. 106Theorem 3.11(iv)adjadj 22462
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22628  nmopcoadji 22627
[Beran] p. 106Theorem 3.11(iii)adjadd 22619
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22629
[Beran] p. 106Theorem 3.11(viii)adjcoi 22626  pjadj2coi 22730  pjadjcoi 22687
[Beran] p. 107Definitiondf-ch 21747  isch2 21749
[Beran] p. 107Remark 3.12choccl 21831  isch3 21767  occl 21829  ocsh 21808  shoccl 21830  shocsh 21809
[Beran] p. 107Remark 3.12(B)ococin 21933
[Beran] p. 108Theorem 3.13chintcl 21857
[Beran] p. 109Property (i)pjadj2 22713  pjadj3 22714  pjadji 22228  pjadjii 22217
[Beran] p. 109Property (ii)pjidmco 22707  pjidmcoi 22703  pjidmi 22216
[Beran] p. 110Definition of projector orderingpjordi 22699
[Beran] p. 111Remarkho0val 22276  pjch1 22213
[Beran] p. 111Definitiondf-hfmul 22112  df-hfsum 22111  df-hodif 22110  df-homul 22109  df-hosum 22108
[Beran] p. 111Lemma 4.4(i)pjo 22214
[Beran] p. 111Lemma 4.4(ii)pjch 22237  pjchi 21957
[Beran] p. 111Lemma 4.4(iii)pjoc2 21964  pjoc2i 21963
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22223
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22691  pjssmii 22224
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22690
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22689
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22694
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22692  pjssge0ii 22225
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22693  pjdifnormii 22226
[BourbakiEns] p. Proposition 8fcof1 5717  fcofo 5718
[BourbakiFVR] p. Definition 1isder 25060
[BourbakiTop1] p. Remarkxnegmnf 10489  xnegpnf 10488
[BourbakiTop1] p. Remark rexneg 10490
[BourbakiTop1] p. Theoremneiss 16794
[BourbakiTop1] p. Axiom GT'tgpsubcn 17721
[BourbakiTop1] p. Example 1snfil 17507
[BourbakiTop1] p. Example 2neifil 17523
[BourbakiTop1] p. Definitionistgp 17708
[BourbakiTop1] p. Propositioncnpco 16944  ishmeo 17398  neips 16798
[BourbakiTop1] p. Definition 1filintn0 17504
[BourbakiTop1] p. Proposition 9cnpflf2 17643
[BourbakiTop1] p. Theorem 1 (d)iscncl 16946
[BourbakiTop1] p. Proposition Vissnei2 16801
[BourbakiTop1] p. Definition C'''df-cmp 17062
[BourbakiTop1] p. Proposition Viiinnei 16810
[BourbakiTop1] p. Proposition Vivneissex 16812
[BourbakiTop1] p. Proposition Viiielnei 16796  ssnei 16795
[BourbakiTop1] p. Remark below def. 1filn0 17505
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17489
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17506
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27134  stoweid 27133
[BrosowskiDeutsh] p. 89Theorem for the non trivial casestoweidlem62 27132
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27071  stoweidlem10 27080  stoweidlem14 27084  stoweidlem15 27085  stoweidlem35 27105  stoweidlem36 27106  stoweidlem37 27107  stoweidlem38 27108  stoweidlem40 27110  stoweidlem41 27111  stoweidlem43 27113  stoweidlem44 27114  stoweidlem46 27116  stoweidlem5 27075  stoweidlem50 27120  stoweidlem52 27122  stoweidlem53 27123  stoweidlem55 27125  stoweidlem56 27126
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27093  stoweidlem24 27094  stoweidlem27 27097  stoweidlem28 27098  stoweidlem30 27100
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27115  stoweidlem49 27119  stoweidlem7 27077
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27101  stoweidlem39 27109  stoweidlem42 27112  stoweidlem48 27118  stoweidlem51 27121  stoweidlem54 27124  stoweidlem57 27127  stoweidlem58 27128
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27095
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27104
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27087
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27129
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27130
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27088
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27081  stoweidlem26 27096
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27083
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27131
[ChoquetDD] p. 2Definition of mappingdf-mpt 4039
[Cohen] p. 301Remarkrelogoprlem 19892
[Cohen] p. 301Property 2relogmul 19893  relogmuld 19924
[Cohen] p. 301Property 3relogdiv 19894  relogdivd 19925
[Cohen] p. 301Property 4relogexp 19897
[Cohen] p. 301Property 1alog1 19887
[Cohen] p. 301Property 1bloge 19888
[Cohn] p. 81Section II.5acsdomd 14232  acsinfd 14231  acsinfdimd 14233  acsmap2d 14230  acsmapd 14229
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10917
[Crawley] p. 1Definition of posetdf-poset 14028
[Crawley] p. 107Theorem 13.2hlsupr 28726
[Crawley] p. 110Theorem 13.3arglem1N 29530  dalaw 29226
[Crawley] p. 111Theorem 13.4hlathil 31305
[Crawley] p. 111Definition of set Wdf-watsN 29330
[Crawley] p. 111Definition of dilationdf-dilN 29446  df-ldil 29444  isldil 29450
[Crawley] p. 111Definition of translationdf-ltrn 29445  df-trnN 29447  isltrn 29459  ltrnu 29461
[Crawley] p. 112Lemma Acdlema1N 29131  cdlema2N 29132  exatleN 28744
[Crawley] p. 112Lemma B1cvrat 28816  cdlemb 29134  cdlemb2 29381  cdlemb3 29946  idltrn 29490  l1cvat 28396  lhpat 29383  lhpat2 29385  lshpat 28397  ltrnel 29479  ltrnmw 29491
[Crawley] p. 112Lemma Ccdlemc1 29531  cdlemc2 29532  ltrnnidn 29514  trlat 29509  trljat1 29506  trljat2 29507  trljat3 29508  trlne 29525  trlnidat 29513  trlnle 29526
[Crawley] p. 112Definition of automorphismdf-pautN 29331
[Crawley] p. 113Lemma Ccdlemc 29537  cdlemc3 29533  cdlemc4 29534
[Crawley] p. 113Lemma Dcdlemd 29547  cdlemd1 29538  cdlemd2 29539  cdlemd3 29540  cdlemd4 29541  cdlemd5 29542  cdlemd6 29543  cdlemd7 29544  cdlemd8 29545  cdlemd9 29546  cdleme31sde 29725  cdleme31se 29722  cdleme31se2 29723  cdleme31snd 29726  cdleme32a 29781  cdleme32b 29782  cdleme32c 29783  cdleme32d 29784  cdleme32e 29785  cdleme32f 29786  cdleme32fva 29777  cdleme32fva1 29778  cdleme32fvcl 29780  cdleme32le 29787  cdleme48fv 29839  cdleme4gfv 29847  cdleme50eq 29881  cdleme50f 29882  cdleme50f1 29883  cdleme50f1o 29886  cdleme50laut 29887  cdleme50ldil 29888  cdleme50lebi 29880  cdleme50rn 29885  cdleme50rnlem 29884  cdlemeg49le 29851  cdlemeg49lebilem 29879
[Crawley] p. 113Lemma Ecdleme 29900  cdleme00a 29549  cdleme01N 29561  cdleme02N 29562  cdleme0a 29551  cdleme0aa 29550  cdleme0b 29552  cdleme0c 29553  cdleme0cp 29554  cdleme0cq 29555  cdleme0dN 29556  cdleme0e 29557  cdleme0ex1N 29563  cdleme0ex2N 29564  cdleme0fN 29558  cdleme0gN 29559  cdleme0moN 29565  cdleme1 29567  cdleme10 29594  cdleme10tN 29598  cdleme11 29610  cdleme11a 29600  cdleme11c 29601  cdleme11dN 29602  cdleme11e 29603  cdleme11fN 29604  cdleme11g 29605  cdleme11h 29606  cdleme11j 29607  cdleme11k 29608  cdleme11l 29609  cdleme12 29611  cdleme13 29612  cdleme14 29613  cdleme15 29618  cdleme15a 29614  cdleme15b 29615  cdleme15c 29616  cdleme15d 29617  cdleme16 29625  cdleme16aN 29599  cdleme16b 29619  cdleme16c 29620  cdleme16d 29621  cdleme16e 29622  cdleme16f 29623  cdleme16g 29624  cdleme19a 29643  cdleme19b 29644  cdleme19c 29645  cdleme19d 29646  cdleme19e 29647  cdleme19f 29648  cdleme1b 29566  cdleme2 29568  cdleme20aN 29649  cdleme20bN 29650  cdleme20c 29651  cdleme20d 29652  cdleme20e 29653  cdleme20f 29654  cdleme20g 29655  cdleme20h 29656  cdleme20i 29657  cdleme20j 29658  cdleme20k 29659  cdleme20l 29662  cdleme20l1 29660  cdleme20l2 29661  cdleme20m 29663  cdleme20y 29642  cdleme20zN 29641  cdleme21 29677  cdleme21d 29670  cdleme21e 29671  cdleme22a 29680  cdleme22aa 29679  cdleme22b 29681  cdleme22cN 29682  cdleme22d 29683  cdleme22e 29684  cdleme22eALTN 29685  cdleme22f 29686  cdleme22f2 29687  cdleme22g 29688  cdleme23a 29689  cdleme23b 29690  cdleme23c 29691  cdleme26e 29699  cdleme26eALTN 29701  cdleme26ee 29700  cdleme26f 29703  cdleme26f2 29705  cdleme26f2ALTN 29704  cdleme26fALTN 29702  cdleme27N 29709  cdleme27a 29707  cdleme27cl 29706  cdleme28c 29712  cdleme3 29577  cdleme30a 29718  cdleme31fv 29730  cdleme31fv1 29731  cdleme31fv1s 29732  cdleme31fv2 29733  cdleme31id 29734  cdleme31sc 29724  cdleme31sdnN 29727  cdleme31sn 29720  cdleme31sn1 29721  cdleme31sn1c 29728  cdleme31sn2 29729  cdleme31so 29719  cdleme35a 29788  cdleme35b 29790  cdleme35c 29791  cdleme35d 29792  cdleme35e 29793  cdleme35f 29794  cdleme35fnpq 29789  cdleme35g 29795  cdleme35h 29796  cdleme35h2 29797  cdleme35sn2aw 29798  cdleme35sn3a 29799  cdleme36a 29800  cdleme36m 29801  cdleme37m 29802  cdleme38m 29803  cdleme38n 29804  cdleme39a 29805  cdleme39n 29806  cdleme3b 29569  cdleme3c 29570  cdleme3d 29571  cdleme3e 29572  cdleme3fN 29573  cdleme3fa 29576  cdleme3g 29574  cdleme3h 29575  cdleme4 29578  cdleme40m 29807  cdleme40n 29808  cdleme40v 29809  cdleme40w 29810  cdleme41fva11 29817  cdleme41sn3aw 29814  cdleme41sn4aw 29815  cdleme41snaw 29816  cdleme42a 29811  cdleme42b 29818  cdleme42c 29812  cdleme42d 29813  cdleme42e 29819  cdleme42f 29820  cdleme42g 29821  cdleme42h 29822  cdleme42i 29823  cdleme42k 29824  cdleme42ke 29825  cdleme42keg 29826  cdleme42mN 29827  cdleme42mgN 29828  cdleme43aN 29829  cdleme43bN 29830  cdleme43cN 29831  cdleme43dN 29832  cdleme5 29580  cdleme50ex 29899  cdleme50ltrn 29897  cdleme51finvN 29896  cdleme51finvfvN 29895  cdleme51finvtrN 29898  cdleme6 29581  cdleme7 29589  cdleme7a 29583  cdleme7aa 29582  cdleme7b 29584  cdleme7c 29585  cdleme7d 29586  cdleme7e 29587  cdleme7ga 29588  cdleme8 29590  cdleme8tN 29595  cdleme9 29593  cdleme9a 29591  cdleme9b 29592  cdleme9tN 29597  cdleme9taN 29596  cdlemeda 29638  cdlemedb 29637  cdlemednpq 29639  cdlemednuN 29640  cdlemefr27cl 29743  cdlemefr32fva1 29750  cdlemefr32fvaN 29749  cdlemefrs32fva 29740  cdlemefrs32fva1 29741  cdlemefs27cl 29753  cdlemefs32fva1 29763  cdlemefs32fvaN 29762  cdlemesner 29636  cdlemeulpq 29560
[Crawley] p. 114Lemma E4atex 29416  4atexlem7 29415  cdleme0nex 29630  cdleme17a 29626  cdleme17c 29628  cdleme17d 29838  cdleme17d1 29629  cdleme17d2 29835  cdleme18a 29631  cdleme18b 29632  cdleme18c 29633  cdleme18d 29635  cdleme4a 29579
[Crawley] p. 115Lemma Ecdleme21a 29665  cdleme21at 29668  cdleme21b 29666  cdleme21c 29667  cdleme21ct 29669  cdleme21f 29672  cdleme21g 29673  cdleme21h 29674  cdleme21i 29675  cdleme22gb 29634
[Crawley] p. 116Lemma Fcdlemf 29903  cdlemf1 29901  cdlemf2 29902
[Crawley] p. 116Lemma Gcdlemftr1 29907  cdlemg16 29997  cdlemg28 30044  cdlemg28a 30033  cdlemg28b 30043  cdlemg3a 29937  cdlemg42 30069  cdlemg43 30070  cdlemg44 30073  cdlemg44a 30071  cdlemg46 30075  cdlemg47 30076  cdlemg9 29974  ltrnco 30059  ltrncom 30078  tgrpabl 30091  trlco 30067
[Crawley] p. 116Definition of Gdf-tgrp 30083
[Crawley] p. 117Lemma Gcdlemg17 30017  cdlemg17b 30002
[Crawley] p. 117Definition of Edf-edring-rN 30096  df-edring 30097
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30100
[Crawley] p. 118Remarktendopltp 30120
[Crawley] p. 118Lemma Hcdlemh 30157  cdlemh1 30155  cdlemh2 30156
[Crawley] p. 118Lemma Icdlemi 30160  cdlemi1 30158  cdlemi2 30159
[Crawley] p. 118Lemma Jcdlemj1 30161  cdlemj2 30162  cdlemj3 30163  tendocan 30164
[Crawley] p. 118Lemma Kcdlemk 30314  cdlemk1 30171  cdlemk10 30183  cdlemk11 30189  cdlemk11t 30286  cdlemk11ta 30269  cdlemk11tb 30271  cdlemk11tc 30285  cdlemk11u-2N 30229  cdlemk11u 30211  cdlemk12 30190  cdlemk12u-2N 30230  cdlemk12u 30212  cdlemk13-2N 30216  cdlemk13 30192  cdlemk14-2N 30218  cdlemk14 30194  cdlemk15-2N 30219  cdlemk15 30195  cdlemk16-2N 30220  cdlemk16 30197  cdlemk16a 30196  cdlemk17-2N 30221  cdlemk17 30198  cdlemk18-2N 30226  cdlemk18-3N 30240  cdlemk18 30208  cdlemk19-2N 30227  cdlemk19 30209  cdlemk19u 30310  cdlemk1u 30199  cdlemk2 30172  cdlemk20-2N 30232  cdlemk20 30214  cdlemk21-2N 30231  cdlemk21N 30213  cdlemk22-3 30241  cdlemk22 30233  cdlemk23-3 30242  cdlemk24-3 30243  cdlemk25-3 30244  cdlemk26-3 30246  cdlemk26b-3 30245  cdlemk27-3 30247  cdlemk28-3 30248  cdlemk29-3 30251  cdlemk3 30173  cdlemk30 30234  cdlemk31 30236  cdlemk32 30237  cdlemk33N 30249  cdlemk34 30250  cdlemk35 30252  cdlemk36 30253  cdlemk37 30254  cdlemk38 30255  cdlemk39 30256  cdlemk39u 30308  cdlemk4 30174  cdlemk41 30260  cdlemk42 30281  cdlemk42yN 30284  cdlemk43N 30303  cdlemk45 30287  cdlemk46 30288  cdlemk47 30289  cdlemk48 30290  cdlemk49 30291  cdlemk5 30176  cdlemk50 30292  cdlemk51 30293  cdlemk52 30294  cdlemk53 30297  cdlemk54 30298  cdlemk55 30301  cdlemk55u 30306  cdlemk56 30311  cdlemk5a 30175  cdlemk5auN 30200  cdlemk5u 30201  cdlemk6 30177  cdlemk6u 30202  cdlemk7 30188  cdlemk7u-2N 30228  cdlemk7u 30210  cdlemk8 30178  cdlemk9 30179  cdlemk9bN 30180  cdlemki 30181  cdlemkid 30276  cdlemkj-2N 30222  cdlemkj 30203  cdlemksat 30186  cdlemksel 30185  cdlemksv 30184  cdlemksv2 30187  cdlemkuat 30206  cdlemkuel-2N 30224  cdlemkuel-3 30238  cdlemkuel 30205  cdlemkuv-2N 30223  cdlemkuv2-2 30225  cdlemkuv2-3N 30239  cdlemkuv2 30207  cdlemkuvN 30204  cdlemkvcl 30182  cdlemky 30266  cdlemkyyN 30302  tendoex 30315
[Crawley] p. 120Remarkdva1dim 30325
[Crawley] p. 120Lemma Lcdleml1N 30316  cdleml2N 30317  cdleml3N 30318  cdleml4N 30319  cdleml5N 30320  cdleml6 30321  cdleml7 30322  cdleml8 30323  cdleml9 30324  dia1dim 30402
[Crawley] p. 120Lemma Mdia11N 30389  diaf11N 30390  dialss 30387  diaord 30388  dibf11N 30502  djajN 30478
[Crawley] p. 120Definition of isomorphism mapdiaval 30373
[Crawley] p. 121Lemma Mcdlemm10N 30459  dia2dimlem1 30405  dia2dimlem2 30406  dia2dimlem3 30407  dia2dimlem4 30408  dia2dimlem5 30409  diaf1oN 30471  diarnN 30470  dvheveccl 30453  dvhopN 30457
[Crawley] p. 121Lemma Ncdlemn 30553  cdlemn10 30547  cdlemn11 30552  cdlemn11a 30548  cdlemn11b 30549  cdlemn11c 30550  cdlemn11pre 30551  cdlemn2 30536  cdlemn2a 30537  cdlemn3 30538  cdlemn4 30539  cdlemn4a 30540  cdlemn5 30542  cdlemn5pre 30541  cdlemn6 30543  cdlemn7 30544  cdlemn8 30545  cdlemn9 30546  diclspsn 30535
[Crawley] p. 121Definition of phi(q)df-dic 30514
[Crawley] p. 122Lemma Ndih11 30606  dihf11 30608  dihjust 30558  dihjustlem 30557  dihord 30605  dihord1 30559  dihord10 30564  dihord11b 30563  dihord11c 30565  dihord2 30568  dihord2a 30560  dihord2b 30561  dihord2cN 30562  dihord2pre 30566  dihord2pre2 30567  dihordlem6 30554  dihordlem7 30555  dihordlem7b 30556
[Crawley] p. 122Definition of isomorphism mapdihffval 30571  dihfval 30572  dihval 30573
[Eisenberg] p. 67Definition 5.3df-dif 3116
[Eisenberg] p. 82Definition 6.3dfom3 7302
[Eisenberg] p. 125Definition 8.21df-map 6728
[Eisenberg] p. 216Example 13.2(4)omenps 7309
[Eisenberg] p. 310Theorem 19.8cardprc 7567
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8131
[Enderton] p. 18Axiom of Empty Setaxnul 4108
[Enderton] p. 19Definitiondf-tp 3608
[Enderton] p. 26Exercise 5unissb 3817
[Enderton] p. 26Exercise 10pwel 4183
[Enderton] p. 28Exercise 7(b)pwun 4260
[Enderton] p. 30Theorem "Distributive laws"iinin1 3933  iinin2 3932  iinun2 3928  iunin1 3927  iunin2 3926
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3931  iundif2 3929
[Enderton] p. 32Exercise 20unineq 3380
[Enderton] p. 33Exercise 23iinuni 3945
[Enderton] p. 33Exercise 25iununi 3946
[Enderton] p. 33Exercise 24(a)iinpw 3950
[Enderton] p. 33Exercise 24(b)iunpw 4528  iunpwss 3951
[Enderton] p. 36Definitionopthwiener 4226
[Enderton] p. 38Exercise 6(a)unipw 4182
[Enderton] p. 38Exercise 6(b)pwuni 4164
[Enderton] p. 41Lemma 3Dopeluu 4484  rnex 4916  rnexg 4914
[Enderton] p. 41Exercise 8dmuni 4862  rnuni 5066
[Enderton] p. 42Definition of a functiondffun7 5205  dffun8 5206
[Enderton] p. 43Definition of function valuefunfv2 5507
[Enderton] p. 43Definition of single-rootedfuncnv 5234
[Enderton] p. 44Definition (d)dfima2 4988  dfima3 4989
[Enderton] p. 47Theorem 3Hfvco2 5514
[Enderton] p. 49Axiom of Choice (first form)ac7 8054  ac7g 8055  df-ac 7697  dfac2 7711  dfac2a 7710  dfac3 7702  dfac7 7712
[Enderton] p. 50Theorem 3K(a)imauni 5692
[Enderton] p. 52Definitiondf-map 6728
[Enderton] p. 53Exercise 21coass 5164
[Enderton] p. 53Exercise 27dmco 5154
[Enderton] p. 53Exercise 14(a)funin 5243
[Enderton] p. 53Exercise 22(a)imass2 5023
[Enderton] p. 54Remarkixpf 6792  ixpssmap 6804
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6772
[Enderton] p. 55Axiom of Choice (second form)ac9 8064  ac9s 8074
[Enderton] p. 56Theorem 3Merref 6634
[Enderton] p. 57Lemma 3Nerthi 6660
[Enderton] p. 57Definitiondf-ec 6616
[Enderton] p. 58Definitiondf-qs 6620
[Enderton] p. 60Theorem 3Qth3q 6721  th3qcor 6720  th3qlem1 6718  th3qlem2 6719
[Enderton] p. 61Exercise 35df-ec 6616
[Enderton] p. 65Exercise 56(a)dmun 4859
[Enderton] p. 68Definition of successordf-suc 4356
[Enderton] p. 71Definitiondf-tr 4074  dftr4 4078
[Enderton] p. 72Theorem 4Eunisuc 4426
[Enderton] p. 73Exercise 6unisuc 4426
[Enderton] p. 73Exercise 5(a)truni 4087
[Enderton] p. 73Exercise 5(b)trint 4088  trintALT 27691
[Enderton] p. 79Theorem 4I(A1)nna0 6556
[Enderton] p. 79Theorem 4I(A2)nnasuc 6558  onasuc 6481
[Enderton] p. 79Definition of operation valuedf-ov 5781
[Enderton] p. 80Theorem 4J(A1)nnm0 6557
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6559  onmsuc 6482
[Enderton] p. 81Theorem 4K(1)nnaass 6574
[Enderton] p. 81Theorem 4K(2)nna0r 6561  nnacom 6569
[Enderton] p. 81Theorem 4K(3)nndi 6575
[Enderton] p. 81Theorem 4K(4)nnmass 6576
[Enderton] p. 81Theorem 4K(5)nnmcom 6578
[Enderton] p. 82Exercise 16nnm0r 6562  nnmsucr 6577
[Enderton] p. 88Exercise 23nnaordex 6590
[Enderton] p. 129Definitiondf-en 6818
[Enderton] p. 132Theorem 6B(b)canth 6246
[Enderton] p. 133Exercise 1xpomen 7597
[Enderton] p. 133Exercise 2qnnen 12440
[Enderton] p. 134Theorem (Pigeonhole Principle)php 6999
[Enderton] p. 135Corollary 6Cphp3 7001
[Enderton] p. 136Corollary 6Enneneq 6998
[Enderton] p. 136Corollary 6D(a)pssinf 7027
[Enderton] p. 136Corollary 6D(b)ominf 7029
[Enderton] p. 137Lemma 6Fpssnn 7035
[Enderton] p. 138Corollary 6Gssfi 7037
[Enderton] p. 139Theorem 6H(c)mapen 6979
[Enderton] p. 142Theorem 6I(3)xpcdaen 7763
[Enderton] p. 142Theorem 6I(4)mapcdaen 7764
[Enderton] p. 143Theorem 6Jcda0en 7759  cda1en 7755
[Enderton] p. 144Exercise 13iunfi 7098  unifi 7099  unifi2 7100
[Enderton] p. 144Corollary 6Kundif2 3491  unfi 7078  unfi2 7080
[Enderton] p. 145Figure 38ffoss 5429
[Enderton] p. 145Definitiondf-dom 6819
[Enderton] p. 146Example 1domen 6829  domeng 6830
[Enderton] p. 146Example 3nndomo 7008  nnsdom 7308  nnsdomg 7070
[Enderton] p. 149Theorem 6L(a)cdadom2 7767
[Enderton] p. 149Theorem 6L(c)mapdom1 6980  xpdom1 6915  xpdom1g 6913  xpdom2g 6912
[Enderton] p. 149Theorem 6L(d)mapdom2 6986
[Enderton] p. 151Theorem 6Mzorn 8088  zorng 8085
[Enderton] p. 151Theorem 6M(4)ac8 8073  dfac5 7709
[Enderton] p. 159Theorem 6Qunictb 8151
[Enderton] p. 164Exampleinfdif 7789
[Enderton] p. 168Definitiondf-po 4272
[Enderton] p. 192Theorem 7M(a)oneli 4458
[Enderton] p. 192Theorem 7M(b)ontr1 4396
[Enderton] p. 192Theorem 7M(c)onirri 4457
[Enderton] p. 193Corollary 7N(b)0elon 4403
[Enderton] p. 193Corollary 7N(c)onsuci 4587
[Enderton] p. 193Corollary 7N(d)ssonunii 4537
[Enderton] p. 194Remarkonprc 4534
[Enderton] p. 194Exercise 16suc11 4454
[Enderton] p. 197Definitiondf-card 7526
[Enderton] p. 197Theorem 7Pcarden 8127
[Enderton] p. 200Exercise 25tfis 4603
[Enderton] p. 202Lemma 7Tr1tr 7402
[Enderton] p. 202Definitiondf-r1 7390
[Enderton] p. 202Theorem 7Qr1val1 7412
[Enderton] p. 204Theorem 7V(b)rankval4 7493
[Enderton] p. 206Theorem 7X(b)en2lp 7271
[Enderton] p. 207Exercise 30rankpr 7483  rankprb 7477  rankpw 7469  rankpwi 7449  rankuniss 7492
[Enderton] p. 207Exercise 34opthreg 7273
[Enderton] p. 208Exercise 35suc11reg 7274
[Enderton] p. 212Definition of alephalephval3 7691
[Enderton] p. 213Theorem 8A(a)alephord2 7657
[Enderton] p. 213Theorem 8A(b)cardalephex 7671
[Enderton] p. 218Theorem Schema 8Eonfununi 6312
[Enderton] p. 222Definition of kardkarden 7519  kardex 7518
[Enderton] p. 238Theorem 8Roeoa 6549
[Enderton] p. 238Theorem 8Soeoe 6551
[Enderton] p. 240Exercise 25oarec 6514
[Enderton] p. 257Definition of cofinalitycflm 7830
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13492
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13438
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14228  mrieqv2d 13489  mrieqvd 13488
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13493
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13498  mreexexlem2d 13495
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14234  mreexfidimd 13500
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18842
[Fremlin5] p. 213Lemma 565Cauniioovol 18882
[Fremlin5] p. 214Lemma 565Cauniioombl 18892
[FreydScedrov] p. 283Axiom of Infinityax-inf 7293  inf1 7277  inf2 7278
[Gleason] p. 117Proposition 9-2.1df-enq 8489  enqer 8499
[Gleason] p. 117Proposition 9-2.2df-1nq 8494  df-nq 8490
[Gleason] p. 117Proposition 9-2.3df-plpq 8486  df-plq 8492
[Gleason] p. 119Proposition 9-2.4caovmo 5977  df-mpq 8487  df-mq 8493
[Gleason] p. 119Proposition 9-2.5df-rq 8495
[Gleason] p. 119Proposition 9-2.6ltexnq 8553
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8554  ltbtwnnq 8556
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8549
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8550
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8557
[Gleason] p. 121Definition 9-3.1df-np 8559
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8571
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8573
[Gleason] p. 122Definitiondf-1p 8560
[Gleason] p. 122Remark (1)prub 8572
[Gleason] p. 122Lemma 9-3.4prlem934 8611
[Gleason] p. 122Proposition 9-3.2df-ltp 8563
[Gleason] p. 122Proposition 9-3.3ltsopr 8610  psslinpr 8609  supexpr 8632  suplem1pr 8630  suplem2pr 8631
[Gleason] p. 123Proposition 9-3.5addclpr 8596  addclprlem1 8594  addclprlem2 8595  df-plp 8561
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8600
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8599
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8612
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8621  ltexprlem1 8614  ltexprlem2 8615  ltexprlem3 8616  ltexprlem4 8617  ltexprlem5 8618  ltexprlem6 8619  ltexprlem7 8620
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8623  ltaprlem 8622
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8624
[Gleason] p. 124Lemma 9-3.6prlem936 8625
[Gleason] p. 124Proposition 9-3.7df-mp 8562  mulclpr 8598  mulclprlem 8597  reclem2pr 8626
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8607
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8602
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8601
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8606
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8629  reclem3pr 8627  reclem4pr 8628
[Gleason] p. 126Proposition 9-4.1df-enr 8635  df-mpr 8634  df-plpr 8633  enrer 8644
[Gleason] p. 126Proposition 9-4.2df-0r 8640  df-1r 8641  df-nr 8636
[Gleason] p. 126Proposition 9-4.3df-mr 8638  df-plr 8637  negexsr 8678  recexsr 8683  recexsrlem 8679
[Gleason] p. 127Proposition 9-4.4df-ltr 8639
[Gleason] p. 130Proposition 10-1.3creui 9695  creur 9694  cru 9692
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8764  axcnre 8740
[Gleason] p. 132Definition 10-3.1crim 11551  crimd 11668  crimi 11629  crre 11550  crred 11667  crrei 11628
[Gleason] p. 132Definition 10-3.2remim 11553  remimd 11634
[Gleason] p. 133Definition 10.36absval2 11720  absval2d 11878  absval2i 11831
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11577  cjaddd 11656  cjaddi 11624
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11578  cjmuld 11657  cjmuli 11625
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11576  cjcjd 11635  cjcji 11607
[Gleason] p. 133Proposition 10-3.4(f)cjre 11575  cjreb 11559  cjrebd 11638  cjrebi 11610  cjred 11662  rere 11558  rereb 11556  rerebd 11637  rerebi 11609  rered 11660
[Gleason] p. 133Proposition 10-3.4(h)addcj 11584  addcjd 11648  addcji 11619
[Gleason] p. 133Proposition 10-3.7(a)absval 11674
[Gleason] p. 133Proposition 10-3.7(b)abscj 11715  abscjd 11883  abscji 11835
[Gleason] p. 133Proposition 10-3.7(c)abs00 11725  abs00d 11879  abs00i 11832  absne0d 11880
[Gleason] p. 133Proposition 10-3.7(d)releabs 11756  releabsd 11884  releabsi 11836
[Gleason] p. 133Proposition 10-3.7(f)absmul 11730  absmuld 11887  absmuli 11838
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11718  sqabsaddi 11839
[Gleason] p. 133Proposition 10-3.7(h)abstri 11765  abstrid 11889  abstrii 11842
[Gleason] p. 134Definition 10-4.1df-exp 11057  exp0 11060  expp1 11062  expp1d 11198
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 19974  cxpaddd 20012  expadd 11096  expaddd 11199  expaddz 11098
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 19983  cxpmuld 20029  expmul 11099  expmuld 11200  expmulz 11100
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 19980  mulcxpd 20023  mulexp 11093  mulexpd 11212  mulexpz 11094
[Gleason] p. 140Exercise 1znnen 12439
[Gleason] p. 141Definition 11-2.1fzval 10736
[Gleason] p. 168Proposition 12-2.1(a)climadd 12056  rlimadd 12067  rlimdiv 12070
[Gleason] p. 168Proposition 12-2.1(b)climsub 12058  rlimsub 12068
[Gleason] p. 168Proposition 12-2.1(c)climmul 12057  rlimmul 12069
[Gleason] p. 171Corollary 12-2.2climmulc2 12061
[Gleason] p. 172Corollary 12-2.5climrecl 12008
[Gleason] p. 172Proposition 12-2.4(c)climabs 12028  climcj 12029  climim 12031  climre 12030  rlimabs 12033  rlimcj 12034  rlimim 12036  rlimre 12035
[Gleason] p. 173Definition 12-3.1df-ltxr 8826  df-xr 8825  ltxr 10410
[Gleason] p. 175Definition 12-4.1df-limsup 11896  limsupval 11899
[Gleason] p. 180Theorem 12-5.1climsup 12094
[Gleason] p. 180Theorem 12-5.3caucvg 12102  caucvgb 12103  caucvgr 12099  climcau 12095
[Gleason] p. 182Exercise 3cvgcmp 12225
[Gleason] p. 182Exercise 4cvgrat 12287
[Gleason] p. 195Theorem 13-2.12abs1m 11770
[Gleason] p. 217Lemma 13-4.1btwnzge0 10905
[Gleason] p. 223Definition 14-1.1df-met 16322
[Gleason] p. 223Definition 14-1.1(a)met0 17856  xmet0 17855
[Gleason] p. 223Definition 14-1.1(b)metgt0 17871
[Gleason] p. 223Definition 14-1.1(c)metsym 17862
[Gleason] p. 223Definition 14-1.1(d)mettri 17864  mstri 17963  xmettri 17863  xmstri 17962
[Gleason] p. 225Definition 14-1.5xpsmet 17894
[Gleason] p. 230Proposition 14-2.6txlm 17290
[Gleason] p. 240Theorem 14-4.3metcnp4 18683
[Gleason] p. 240Proposition 14-4.2metcnp3 18034
[Gleason] p. 243Proposition 14-4.16addcn 18317  addcn2 12018  mulcn 18319  mulcn2 12020  subcn 18318  subcn2 12019
[Gleason] p. 295Remarkbcval3 11271  bcval4 11272
[Gleason] p. 295Equation 2bcpasc 11285
[Gleason] p. 295Definition of binomial coefficientbcval 11269  df-bc 11268
[Gleason] p. 296Remarkbcn0 11275  bcnn 11276
[Gleason] p. 296Theorem 15-2.8binom 12239
[Gleason] p. 308Equation 2ef0 12320
[Gleason] p. 308Equation 3efcj 12321
[Gleason] p. 309Corollary 15-4.3efne0 12325
[Gleason] p. 309Corollary 15-4.4efexp 12329
[Gleason] p. 310Equation 14sinadd 12392
[Gleason] p. 310Equation 15cosadd 12393
[Gleason] p. 311Equation 17sincossq 12404
[Gleason] p. 311Equation 18cosbnd 12409  sinbnd 12408
[Gleason] p. 311Lemma 15-4.7sqeqor 11169  sqeqori 11167
[Gleason] p. 311Definition of pidf-pi 12302
[Godowski] p. 730Equation SFgoeqi 22799
[GodowskiGreechie] p. 249Equation IV3oai 22211
[Gratzer] p. 23Section 0.6df-mre 13436
[Gratzer] p. 27Section 0.6df-mri 13438
[Halmos] p. 31Theorem 17.3riesz1 22591  riesz2 22592
[Halmos] p. 41Definition of Hermitianhmopadj2 22467
[Halmos] p. 42Definition of projector orderingpjordi 22699
[Halmos] p. 43Theorem 26.1elpjhmop 22711  elpjidm 22710  pjnmopi 22674
[Halmos] p. 44Remarkpjinormi 22230  pjinormii 22219
[Halmos] p. 44Theorem 26.2elpjch 22715  pjrn 22250  pjrni 22245  pjvec 22239
[Halmos] p. 44Theorem 26.3pjnorm2 22270
[Halmos] p. 44Theorem 26.4hmopidmpj 22680  hmopidmpji 22678
[Halmos] p. 45Theorem 27.1pjinvari 22717
[Halmos] p. 45Theorem 27.3pjoci 22706  pjocvec 22240
[Halmos] p. 45Theorem 27.4pjorthcoi 22695
[Halmos] p. 48Theorem 29.2pjssposi 22698
[Halmos] p. 48Theorem 29.3pjssdif1i 22701  pjssdif2i 22700
[Halmos] p. 50Definition of spectrumdf-spec 22381
[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 18438  df-phtpy 18417
[Hatcher] p. 26Definitiondf-pco 18451  df-pi1 18454
[Hatcher] p. 26Proposition 1.2phtpcer 18441
[Hatcher] p. 26Proposition 1.3pi1grp 18496
[Herstein] p. 54Exercise 28df-grpo 20804
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14446  grpoideu 20822  mndideu 14323
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14464  grpoinveu 20835
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14483  grpo2inv 20852
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14492  grpoinvop 20854
[Herstein] p. 57Exercise 1isgrp2d 20848  isgrp2i 20849
[Hitchcock] p. 5Rule A3mpto1 1528
[Hitchcock] p. 5Rule A4mpto2 1529
[Hitchcock] p. 5Rule A5mtp-xor 1530
[Holland] p. 1519Theorem 2sumdmdi 22946
[Holland] p. 1520Lemma 5cdj1i 22959  cdj3i 22967  cdj3lem1 22960  cdjreui 22958
[Holland] p. 1524Lemma 7mddmdin0i 22957
[Holland95] p. 13Theorem 3.6hlathil 31305
[Holland95] p. 14Line 15hgmapvs 31235
[Holland95] p. 14Line 16hdmaplkr 31257
[Holland95] p. 14Line 17hdmapellkr 31258
[Holland95] p. 14Line 19hdmapglnm2 31255
[Holland95] p. 14Line 20hdmapip0com 31261
[Holland95] p. 14Theorem 3.6hdmapevec2 31180
[Holland95] p. 14Lines 24 and 25hdmapoc 31275
[Holland95] p. 204Definition of involutiondf-srng 15559
[Holland95] p. 212Definition of subspacedf-psubsp 28843
[Holland95] p. 214Lemma 3.3lclkrlem2v 30869
[Holland95] p. 214Definition 3.2df-lpolN 30822
[Holland95] p. 214Definition of nonsingularpnonsingN 29273
[Holland95] p. 215Lemma 3.3(1)dihoml4 30718  poml4N 29293
[Holland95] p. 215Lemma 3.3(2)dochexmid 30809  pexmidALTN 29318  pexmidN 29309
[Holland95] p. 218Theorem 3.6lclkr 30874
[Holland95] p. 218Definition of dual vector spacedf-ldual 28465  ldualset 28466
[Holland95] p. 222Item 1df-lines 28841  df-pointsN 28842
[Holland95] p. 222Item 2df-polarityN 29243
[Holland95] p. 223Remarkispsubcl2N 29287  omllaw4 28587  pol1N 29250  polcon3N 29257
[Holland95] p. 223Definitiondf-psubclN 29275
[Holland95] p. 223Equation for polaritypolval2N 29246
[Hughes] p. 44Equation 1.21bax-his3 21609
[Hughes] p. 47Definition of projection operatordfpjop 22708
[Hughes] p. 49Equation 1.30eighmre 22489  eigre 22361  eigrei 22360
[Hughes] p. 49Equation 1.31eighmorth 22490  eigorth 22364  eigorthi 22363
[Hughes] p. 137Remark (ii)eigposi 22362
[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 2251
[Jech] p. 42Lemma 6.1alephexp1 8155
[Jech] p. 42Equation 6.1alephadd 8153  alephmul 8154
[Jech] p. 43Lemma 6.2infmap 8152  infmap2 7798
[Jech] p. 71Lemma 9.3jech9.3 7440
[Jech] p. 72Equation 9.3scott0 7510  scottex 7509
[Jech] p. 72Exercise 9.1rankval4 7493
[Jech] p. 72Scheme "Collection Principle"cp 7515
[Jech] p. 78Definition implied by the footnoteopthprc 4710
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26353
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26449
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26450
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26365
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26369
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26370  rmyp1 26371
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26372  rmym1 26373
[JonesMatijasevic] p. 695Equation 2.11rmx0 26363  rmx1 26364  rmxluc 26374
[JonesMatijasevic] p. 695Equation 2.12rmy0 26367  rmy1 26368  rmyluc 26375
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26377
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26378
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26400  jm2.17b 26401  jm2.17c 26402
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26439
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26443
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26434
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26403  jm2.24nn 26399
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26448
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26454  rmygeid 26404
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26466
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1684
[KalishMontague] p. 81Schemes B4 through B8equidK 28136
[KalishMontague] p. 85Lemma 2equidK 28136
[KalishMontague] p. 85Lemma 3equcomiK 28137
[KalishMontague] p. 85Theorem 1equidK 28136
[KalishMontague] p. 86Lemma 5albiiK 28143  alimdK 28144  alimdvK 28145
[KalishMontague] p. 86Lemma 7cbvaliK 28160  cbvalivK 28161
[KalishMontague] p. 86Lemma 9ax4wK 28153  ax4wfK 28152  equidK 28136
[KalishMontague] p. 87Lemma 8a4imK 28150  a4imvK 28151
[Kalmbach] p. 14Definition of latticechabs1 22041  chabs1i 22043  chabs2 22042  chabs2i 22044  chjass 22058  chjassi 22011  latabs1 14141  latabs2 14142
[Kalmbach] p. 15Definition of atomdf-at 22864  ela 22865
[Kalmbach] p. 15Definition of coverscvbr2 22809  cvrval2 28615
[Kalmbach] p. 16Definitiondf-ol 28519  df-oml 28520
[Kalmbach] p. 20Definition of commutescmbr 22127  cmbri 22133  cmtvalN 28552  df-cm 22126  df-cmtN 28518
[Kalmbach] p. 22Remarkomllaw5N 28588  pjoml5 22156  pjoml5i 22131
[Kalmbach] p. 22Definitionpjoml2 22154  pjoml2i 22128
[Kalmbach] p. 22Theorem 2(v)cmcm 22157  cmcmi 22135  cmcmii 22140  cmtcomN 28590
[Kalmbach] p. 22Theorem 2(ii)omllaw3 28586  omlsi 21929  pjoml 21961  pjomli 21960
[Kalmbach] p. 22Definition of OML lawomllaw2N 28585
[Kalmbach] p. 23Remarkcmbr2i 22139  cmcm3 22158  cmcm3i 22137  cmcm3ii 22142  cmcm4i 22138  cmt3N 28592  cmt4N 28593  cmtbr2N 28594
[Kalmbach] p. 23Lemma 3cmbr3 22151  cmbr3i 22143  cmtbr3N 28595
[Kalmbach] p. 25Theorem 5fh1 22161  fh1i 22164  fh2 22162  fh2i 22165  omlfh1N 28599
[Kalmbach] p. 65Remarkchjatom 22883  chslej 22023  chsleji 21983  shslej 21905  shsleji 21895
[Kalmbach] p. 65Proposition 1chocin 22020  chocini 21979  chsupcl 21865  chsupval2 21935  h0elch 21780  helch 21769  hsupval2 21934  ocin 21821  ococss 21818  shococss 21819
[Kalmbach] p. 65Definition of subspace sumshsval 21837
[Kalmbach] p. 66Remarkdf-pjh 21920  pjssmi 22691  pjssmii 22224
[Kalmbach] p. 67Lemma 3osum 22188  osumi 22185
[Kalmbach] p. 67Lemma 4pjci 22726
[Kalmbach] p. 103Exercise 6atmd2 22926
[Kalmbach] p. 103Exercise 12mdsl0 22836
[Kalmbach] p. 140Remarkhatomic 22886  hatomici 22885  hatomistici 22888
[Kalmbach] p. 140Proposition 1atlatmstc 28660
[Kalmbach] p. 140Proposition 1(i)atexch 22907  lsatexch 28384
[Kalmbach] p. 140Proposition 1(ii)chcv1 22881  cvlcvr1 28680  cvr1 28750
[Kalmbach] p. 140Proposition 1(iii)cvexch 22900  cvexchi 22895  cvrexch 28760
[Kalmbach] p. 149Remark 2chrelati 22890  hlrelat 28742  hlrelat5N 28741  lrelat 28355
[Kalmbach] p. 153Exercise 5lsmcv 15842  lsmsatcv 28351  spansncv 22196  spansncvi 22195
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 28370  spansncv2 22819
[Kalmbach] p. 266Definitiondf-st 22737
[Kalmbach2] p. 8Definition of adjointdf-adjh 22375
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8222  fpwwe2 8219
[KanamoriPincus] p. 416Corollary 1.3canth4 8223
[KanamoriPincus] p. 417Corollary 1.6canthp1 8230
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8225
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8227
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8240
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8244  gchxpidm 8245
[KanamoriPincus] p. 419Theorem 2.1gchacg 8248  gchhar 8247
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7796  unxpwdom 7257
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8250
[Kreyszig] p. 3Property M1metcl 17845  xmetcl 17844
[Kreyszig] p. 4Property M2meteq0 17852
[Kreyszig] p. 8Definition 1.1-8dscmet 18043
[Kreyszig] p. 12Equation 5conjmul 9431  muleqadd 9366
[Kreyszig] p. 18Definition 1.3-2mopnval 17932
[Kreyszig] p. 19Remarkmopntopon 17933
[Kreyszig] p. 19Theorem T1mopn0 17992  mopnm 17938
[Kreyszig] p. 19Theorem T2unimopn 17990
[Kreyszig] p. 19Definition of neighborhoodneibl 17995
[Kreyszig] p. 20Definition 1.3-3metcnp2 18036
[Kreyszig] p. 25Definition 1.4-1lmbr 16936  lmmbr 18632  lmmbr2 18633
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17056
[Kreyszig] p. 28Theorem 1.4-5lmcau 18686
[Kreyszig] p. 28Definition 1.4-3iscau 18650  iscmet2 18668
[Kreyszig] p. 30Theorem 1.4-7cmetss 18688
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17135  metelcls 18678
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18679  metcld2 18680
[Kreyszig] p. 51Equation 2clmvneg1 18537  lmodvneg1 15615  nvinv 21143  vcm 21073
[Kreyszig] p. 51Equation 1aclm0vs 18536  lmod0vs 15611  vc0 21071
[Kreyszig] p. 51Equation 1blmodvs0 15612  vcz 21072
[Kreyszig] p. 58Definition 2.2-1imsmet 21206
[Kreyszig] p. 59Equation 1imsdval 21201  imsdval2 21202
[Kreyszig] p. 63Problem 1nvnd 21203
[Kreyszig] p. 64Problem 2nvge0 21186  nvz 21181
[Kreyszig] p. 64Problem 3nvabs 21185
[Kreyszig] p. 91Definition 2.7-1isblo3i 21325
[Kreyszig] p. 92Equation 2df-nmoo 21269
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21331  blocni 21329
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21330
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18587  ipeq0 16490  ipz 21241
[Kreyszig] p. 135Problem 2pythi 21374
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21378
[Kreyszig] p. 144Equation 4supcvg 12262
[Kreyszig] p. 144Theorem 3.3-1minvec 18748  minveco 21409
[Kreyszig] p. 196Definition 3.9-1df-aj 21274
[Kreyszig] p. 247Theorem 4.7-2bcth 18699
[Kreyszig] p. 249Theorem 4.7-3ubth 21398
[Kreyszig] p. 470Definition of positive operator orderingleop 22649  leopg 22648
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22667
[Kreyszig] p. 525Theorem 10.1-1htth 21444
[Kunen] p. 10Axiom 0a9e 1817  axnul 4108
[Kunen] p. 11Axiom 3axnul 4108
[Kunen] p. 12Axiom 6zfrep6 5668
[Kunen] p. 24Definition 10.24mapval 6738  mapvalg 6736
[Kunen] p. 30Lemma 10.20fodom 8103
[Kunen] p. 31Definition 10.24mapex 6732
[Kunen] p. 95Definition 2.1df-r1 7390
[Kunen] p. 97Lemma 2.10r1elss 7432  r1elssi 7431
[Kunen] p. 107Exercise 4rankop 7484  rankopb 7478  rankuni 7489  rankxplim 7503  rankxpsuc 7506
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3875
[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 20766  ex-natded5.2 20765
[Laboreo] p. 16Theorem 5.3ex-natded5.3-2 20769  ex-natded5.3 20768
[Laboreo] p. 18Theorem 5.5ex-natded5.5 20771
[Laboreo] p. 19Theorem 5.7ex-natded5.7-2 20773  ex-natded5.7 20772
[Laboreo] p. 20Theorem 5.8ex-natded5.8-2 20775  ex-natded5.8 20774
[Laboreo] p. 20Theorem 5.13ex-natded5.13-2 20777  ex-natded5.13 20776
[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 20778
[Laboreo] p. 45Theorem 9.20ex-natded9.20-2 20779
[Laboreo] p. 45Theorem 9.26ex-natded9.26-2 20781  ex-natded9.26 20780
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26904
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26899
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26905
[LeBlanc] p. 277Rule R2axnul 4108
[Levy] p. 338Axiomdf-clab 2243  df-clel 2252  df-cleq 2249
[Levy58] p. 2Definition Iisfin1-3 7966
[Levy58] p. 2Definition IIdf-fin2 7866
[Levy58] p. 2Definition Iadf-fin1a 7865
[Levy58] p. 2Definition IIIdf-fin3 7868
[Levy58] p. 3Definition Vdf-fin5 7869
[Levy58] p. 3Definition IVdf-fin4 7867
[Levy58] p. 4Definition VIdf-fin6 7870
[Levy58] p. 4Definition VIIdf-fin7 7871
[Levy58], p. 3Theorem 1fin1a2 7995
[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 22934
[Maeda] p. 168Lemma 5mdsym 22938  mdsymi 22937
[Maeda] p. 168Lemma 4(i)mdsymlem4 22932  mdsymlem6 22934  mdsymlem7 22935
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22936
[MaedaMaeda] p. 1Remarkssdmd1 22839  ssdmd2 22840  ssmd1 22837  ssmd2 22838
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22835
[MaedaMaeda] p. 1Definition 1.1df-dmd 22807  df-md 22806  mdbr 22820
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22857  mdslj1i 22845  mdslj2i 22846  mdslle1i 22843  mdslle2i 22844  mdslmd1i 22855  mdslmd2i 22856
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22847  mdsl2bi 22849  mdsl2i 22848
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22861
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22858
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22859
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22836
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22841  mdsl3 22842
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22860
[MaedaMaeda] p. 4Theorem 1.14mdcompli 22955
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28662  hlrelat1 28740
[MaedaMaeda] p. 31Lemma 7.5lcvexch 28380
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22862  cvmdi 22850  cvnbtwn4 22815  cvrnbtwn4 28620
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22863
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28681  cvp 22901  cvrp 28756  lcvp 28381
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22925
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22924
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28674  hlexch4N 28732
[MaedaMaeda] p. 34Exercise 7.1atabsi 22927
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28783
[MaedaMaeda] p. 61Definition 15.10psubN 29089  atpsubN 29093  df-pointsN 28842  pointpsubN 29091
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28844  pmap11 29102  pmaple 29101  pmapsub 29108  pmapval 29097
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29105  pmap1N 29107
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29110  pmapglb2N 29111  pmapglb2xN 29112  pmapglbx 29109
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 29192
[MaedaMaeda] p. 67Postulate PS1ps-1 28817
[MaedaMaeda] p. 68Lemma 16.2df-padd 29136  paddclN 29182  paddidm 29181
[MaedaMaeda] p. 68Condition PS2ps-2 28818
[MaedaMaeda] p. 68Equation 16.2.1paddass 29178
[MaedaMaeda] p. 69Lemma 16.4ps-1 28817
[MaedaMaeda] p. 69Theorem 16.4ps-2 28818
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14932  lsmmod2 14933  lssats 28353  shatomici 22884  shatomistici 22887  shmodi 21915  shmodsi 21914
[MaedaMaeda] p. 130Remark 29.6dmdmd 22826  mdsymlem7 22935
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22132
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22018
[MaedaMaeda] p. 139Remarksumdmdii 22941
[Margaris] p. 40Rule Cexlimiv 2024
[Margaris] p. 49Axiom A1ax-1 7
[Margaris] p. 49Axiom A2ax-2 8
[Margaris] p. 49Axiom A3ax-3 9
[Margaris] p. 49Definitiondf-an 362  df-ex 1538  df-or 361  dfbi2 612
[Margaris] p. 51Theorem 1id1 22
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 27725
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27726
[Margaris] p. 79Rule Cexinst01 27431  exinst11 27432
[Margaris] p. 89Theorem 19.219.2 1759  19.2K 28159  r19.2z 3504
[Margaris] p. 89Theorem 19.319.3 1760  rr19.3v 2877
[Margaris] p. 89Theorem 19.5alcom 1568
[Margaris] p. 89Theorem 19.6alex 1570
[Margaris] p. 89Theorem 19.7alnex 1569
[Margaris] p. 89Theorem 19.819.8a 1758
[Margaris] p. 89Theorem 19.919.9 1762  19.9v 2011
[Margaris] p. 89Theorem 19.11excom 1765  excomim 1764
[Margaris] p. 89Theorem 19.1219.12 1766  r19.12 2629
[Margaris] p. 90Theorem 19.14exnal 1572
[Margaris] p. 90Theorem 19.152albi 26929  albi 1552  ralbi 2652
[Margaris] p. 90Theorem 19.1619.16 1767
[Margaris] p. 90Theorem 19.1719.17 1768
[Margaris] p. 90Theorem 19.182exbi 26931  exbi 1579
[Margaris] p. 90Theorem 19.1919.19 1769
[Margaris] p. 90Theorem 19.202alim 26928  alim 1548  alimd 1705  alimdh 1551  alimdv 2018  ralimdaa 2593  ralimdv 2595  ralimdva 2594  sbcimdv 3013
[Margaris] p. 90Theorem 19.2119.21-2 1772  19.21 1771  19.21bi 1774  19.21t 1770  19.21v 2012  19.21vv 26927  alrimd 1710  alrimdd 1709  alrimdh 1585  alrimdv 2015  alrimi 1706  alrimih 1553  alrimiv 2013  alrimivv 2014  r19.21 2602  r19.21be 2617  r19.21bi 2614  r19.21t 2601  r19.21v 2603  ralrimd 2604  ralrimdv 2605  ralrimdva 2606  ralrimdvv 2610  ralrimdvva 2611  ralrimi 2597  ralrimiv 2598  ralrimiva 2599  ralrimivv 2607  ralrimivva 2608  ralrimivvva 2609  ralrimivw 2600  rexlimi 2633
[Margaris] p. 90Theorem 19.222alimdv 2020  2exim 26930  2eximdv 2021  exim 1573  eximd 1711  eximdh 1586  eximdv 2019  rexim 2620  reximdai 2624  reximddv 22974  reximdv 2627  reximdv2 2625  reximdva 2628  reximdvai 2626  reximi2 2622
[Margaris] p. 90Theorem 19.2319.23 1777  19.23bi 1783  19.23t 1776  19.23v 2022  19.23vv 2023  exlimd 1784  exlimdh 1785  exlimdv 1933  exlimdvv 2027  exlimexi 27324  exlimi 1781  exlimih 1782  exlimiv 2024  exlimivv 2026  r19.23 2631  r19.23v 2632  rexlimd 2637  rexlimdv 2639  rexlimdv3a 2642  rexlimdva 2640  rexlimdvaa 2641  rexlimdvv 2646  rexlimdvva 2647  rexlimdvw 2643  rexlimiv 2634  rexlimiva 2635  rexlimivv 2645
[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 2649  r19.26-2a 24286  r19.26-3 2650  r19.26 2648  r19.26m 2651
[Margaris] p. 90Theorem 19.2719.27 1786  19.27v 2028  r19.27av 2654  r19.27z 3513  r19.27zv 3514
[Margaris] p. 90Theorem 19.2819.28 1787  19.28v 2029  19.28vv 26937  r19.28av 2655  r19.28z 3507  r19.28zv 3510  rr19.28v 2878
[Margaris] p. 90Theorem 19.2919.29 1595  19.29r 1596  19.29r2 1597  19.29x 1598  r19.29 2656  r19.29r 2657
[Margaris] p. 90Theorem 19.3019.30 1603  r19.30 2658
[Margaris] p. 90Theorem 19.3119.31 1795  19.31vv 26935
[Margaris] p. 90Theorem 19.3219.32 1794  r19.32v 2659
[Margaris] p. 90Theorem 19.3319.33-2 26933  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 2660
[Margaris] p. 90Theorem 19.3619.36 1788  19.36aiv 2031  19.36i 1789  19.36v 2030  19.36vv 26934  r19.36av 2661  r19.36zv 3515
[Margaris] p. 90Theorem 19.3719.37 1790  19.37aiv 2034  19.37v 2033  19.37vv 26936  r19.37 2662  r19.37av 2663  r19.37zv 3511
[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 2664
[Margaris] p. 90Theorem 19.4119.41 1799  19.41rg 27353  19.41v 2035  19.41vv 2036  19.41vvv 2037  19.41vvvv 2038  r19.41 2665  r19.41v 2666
[Margaris] p. 90Theorem 19.4219.42 1800  19.42v 2039  19.42vv 2041  19.42vvv 2042  r19.42v 2667
[Margaris] p. 90Theorem 19.4319.43 1604  r19.43 2668
[Margaris] p. 90Theorem 19.4419.44 1796  r19.44av 2669
[Margaris] p. 90Theorem 19.4519.45 1797  r19.45av 2670  r19.45zv 3512
[Margaris] p. 110Exercise 2(b)eu1 2137
[Mayet] p. 370Remarkjpi 22796  largei 22793  stri 22783
[Mayet3] p. 9Definition of CH-statesdf-hst 22738  ishst 22740
[Mayet3] p. 10Theoremhstrbi 22792  hstri 22791
[Mayet3] p. 1223Theorem 4.1mayete3i 22271
[Mayet3] p. 1240Theorem 7.1mayetes3i 22273
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22804
[MegPav2000] p. 2345Definition 3.4-1chintcl 21857  chsupcl 21865
[MegPav2000] p. 2345Definition 3.4-2hatomic 22886
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22880
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22907
[MegPav2000] p. 2366Figure 7pl42N 29323
[MegPav2002] p. 362Lemma 2.2latj31 14153  latj32 14151  latjass 14149
[Megill] p. 444Axiom C5ax-17 1628
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 1838  alequcom 1680  alequcomX 28250  ax-10 1678
[Megill] p. 446Lemma L17equtrr 1827
[Megill] p. 446Lemma L18ax9from9o 1816
[Megill] p. 446Lemma L19hbnae-o 1846  hbnae 1845
[Megill] p. 447Remark 9.1df-sb 1884  sbid 1896  sbidd-misc 27222  sbidd 27221
[Megill] p. 448Remark 9.6ax15 2104
[Megill] p. 448Scheme C4'ax-5o 1694
[Megill] p. 448Scheme C5'ax-4 1692
[Megill] p. 448Scheme C6'ax-7 1535
[Megill] p. 448Scheme C7'ax-6o 1697
[Megill] p. 448Scheme C8'ax-8 1623
[Megill] p. 448Scheme C9'ax-12o 1664
[Megill] p. 448Scheme C10'ax-9 1684  ax-9o 1815
[Megill] p. 448Scheme C11'ax-10o 1836
[Megill] p. 448Scheme C12'ax-13 1625
[Megill] p. 448Scheme C13'ax-14 1626
[Megill] p. 448Scheme C14'ax-15 2105
[Megill] p. 448Scheme C15'ax-11o 1941
[Megill] p. 448Scheme C16'ax-16 1927
[Megill] p. 448Theorem 9.4dral1-o 1857  dral1 1856  dral2-o 1859  dral2 1858  drex1 1860  drex2 1861  drsb1 1887  drsb2 1954
[Megill] p. 448Theorem 9.7conventions 3
[Megill] p. 449Theorem 9.7sbcom2 2077  sbequ 1953  sbid2v 2086
[Megill] p. 450Example in Appendixhba1 1718
[Mendelson] p. 35Axiom A3hirstL-ax3 27135
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4ra4sbc 3030  ra4sbca 3031  stdpc4 1897
[Mendelson] p. 69Axiom 5ax-5o 1694  ra5 3036  stdpc5 1773
[Mendelson] p. 81Rule Cexlimiv 2024
[Mendelson] p. 95Axiom 6stdpc6 1821
[Mendelson] p. 95Axiom 7stdpc7 1892
[Mendelson] p. 225Axiom system NBGru 2951
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4226
[Mendelson] p. 231Exercise 4.10(k)inv1 3442
[Mendelson] p. 231Exercise 4.10(l)unv 3443
[Mendelson] p. 231Exercise 4.10(n)dfin3 3369
[Mendelson] p. 231Exercise 4.10(o)df-nul 3417
[Mendelson] p. 231Exercise 4.10(q)dfin4 3370
[Mendelson] p. 231Exercise 4.10(s)ddif 3269
[Mendelson] p. 231Definition of uniondfun3 3368
[Mendelson] p. 235Exercise 4.12(c)univ 4523
[Mendelson] p. 235Exercise 4.12(d)pwv 3786
[Mendelson] p. 235Exercise 4.12(j)pwin 4255
[Mendelson] p. 235Exercise 4.12(k)pwunss 4256
[Mendelson] p. 235Exercise 4.12(l)pwssun 4257
[Mendelson] p. 235Exercise 4.12(n)uniin 3807
[Mendelson] p. 235Exercise 4.12(p)reli 4787
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5166
[Mendelson] p. 244Proposition 4.8(g)epweon 4533
[Mendelson] p. 246Definition of successordf-suc 4356
[Mendelson] p. 250Exercise 4.36oelim2 6547
[Mendelson] p. 254Proposition 4.22(b)xpen 6978
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6900  xpsneng 6901
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6907  xpcomeng 6908
[Mendelson] p. 254Proposition 4.22(e)xpassen 6910
[Mendelson] p. 255Definitionbrsdom 6838
[Mendelson] p. 255Exercise 4.39endisj 6903
[Mendelson] p. 255Exercise 4.41mapprc 6730
[Mendelson] p. 255Exercise 4.43mapsnen 6892
[Mendelson] p. 255Exercise 4.45mapunen 6984
[Mendelson] p. 255Exercise 4.47xpmapen 6983
[Mendelson] p. 255Exercise 4.42(a)map0e 6759
[Mendelson] p. 255Exercise 4.42(b)map1 6893
[Mendelson] p. 257Proposition 4.24(a)undom 6904
[Mendelson] p. 258Exercise 4.56(b)cdaen 7753
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7762  cdacomen 7761
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7766
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7760
[Mendelson] p. 258Definition of cardinal sumcdaval 7750  df-cda 7748
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6484
[Mendelson] p. 266Proposition 4.34(f)oaordex 6510
[Mendelson] p. 275Proposition 4.42(d)entri3 8135
[Mendelson] p. 281Definitiondf-r1 7390
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7439
[Mendelson] p. 287Axiom system MKru 2951
[Mittelstaedt] p. 9Definitiondf-oc 21777
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3352
[Monk1] p. 33Theorem 3.2(i)ssrel 4750
[Monk1] p. 33Theorem 3.2(ii)eqrel 4751
[Monk1] p. 34Definition 3.3df-opab 4038
[Monk1] p. 36Theorem 3.7(i)coi1 5161  coi2 5162
[Monk1] p. 36Theorem 3.8(v)dm0 4866  rn0 4910
[Monk1] p. 36Theorem 3.7(ii)cnvi 5059
[Monk1] p. 37Theorem 3.13(i)relxp 4768
[Monk1] p. 37Theorem 3.13(x)dmxp 4871  rnxp 5080
[Monk1] p. 37Theorem 3.13(ii)xp0 5072  xp0r 4742
[Monk1] p. 38Theorem 3.16(ii)ima0 5004
[Monk1] p. 38Theorem 3.16(viii)imai 5001
[Monk1] p. 39Theorem 3.17imaexg 5000
[Monk1] p. 39Theorem 3.16(xi)imassrn 4999
[Monk1] p. 41Theorem 4.3(i)fnopfv 5580  funfvop 5557
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5486
[Monk1] p. 42Theorem 4.4(iii)fvelima 5494
[Monk1] p. 43Theorem 4.6funun 5220
[Monk1] p. 43Theorem 4.8(iv)dff13 5703  dff13f 5704
[Monk1] p. 46Theorem 4.15(v)funex 5663  funrnex 5667
[Monk1] p. 50Definition 5.4fniunfv 5693
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5129
[Monk1] p. 52Theorem 5.11(viii)ssint 3838
[Monk1] p. 52Definition 5.13 (i)1stval2 6057  df-1st 6042
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6058  df-2nd 6043
[Monk1] p. 112Theorem 15.17(v)ranksn 7480  ranksnb 7453
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7481
[Monk1] p. 112Theorem 15.17(iii)rankun 7482  rankunb 7476
[Monk1] p. 113Theorem 15.18r1val3 7464
[Monk1] p. 113Definition 15.19df-r1 7390  r1val2 7463
[Monk1] p. 117Lemmazorn2 8087  zorn2g 8084
[Monk1] p. 133Theorem 18.11cardom 7573
[Monk1] p. 133Theorem 18.12canth3 8137
[Monk1] p. 133Theorem 18.14carduni 7568
[Monk2] p. 105Axiom C4ax-5 1533
[Monk2] p. 105Axiom C7ax-8 1623
[Monk2] p. 105Axiom C8ax-11 1624  ax-11o 1941
[Monk2] p. 105Axiom (C8)ax11v 1991
[Monk2] p. 108Lemma 5ax-5o 1694
[Monk2] p. 109Lemma 12ax-7 1535
[Monk2] p. 109Lemma 15equvin 2000  equvini 1880  eqvinop 4209
[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 2570
[Moore] p. 53Part Idf-mre 13436
[Munkres] p. 77Example 2distop 16681  indistop 16687  indistopon 16686
[Munkres] p. 77Example 3fctop 16689  fctop2 16690
[Munkres] p. 77Example 4cctop 16691
[Munkres] p. 78Definition of basisdf-bases 16586  isbasis3g 16635
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13292  tgval2 16642
[Munkres] p. 79Remarktgcl 16655
[Munkres] p. 80Lemma 2.1tgval3 16649
[Munkres] p. 80Lemma 2.2tgss2 16673  tgss3 16672
[Munkres] p. 81Lemma 2.3basgen 16674  basgen2 16675
[Munkres] p. 89Definition of subspace topologyresttop 16839
[Munkres] p. 93Theorem 6.1(1)0cld 16723  topcld 16720
[Munkres] p. 93Theorem 6.1(2)iincld 16724
[Munkres] p. 93Theorem 6.1(3)uncld 16726
[Munkres] p. 94Definition of closureclsval 16722
[Munkres] p. 94Definition of interiorntrval 16721
[Munkres] p. 95Theorem 6.5(a)clsndisj 16760  elcls 16758
[Munkres] p. 95Theorem 6.5(b)elcls3 16768
[Munkres] p. 97Theorem 6.6clslp 16827  neindisj 16802
[Munkres] p. 97Corollary 6.7cldlp 16829
[Munkres] p. 97Definition of limit pointislp2 16825  lpval 16819
[Munkres] p. 98Definition of Hausdorff spacedf-haus 16991
[Munkres] p. 102Definition of continuous functiondf-cn 16905  iscn 16913  iscn2 16916
[Munkres] p. 107Theorem 7.2(g)cncnp 16957  cncnp2 16958  cncnpi 16955  df-cnp 16906  iscnp 16915  iscnp2 16917
[Munkres] p. 127Theorem 10.1metcn 18037
[Munkres] p. 128Theorem 10.3metcn4 18684
[NielsenChuang] p. 195Equation 4.73unierri 22630
[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 18585  df-dip 21220  dip0l 21240  ip0l 16488
[Ponnusamy] p. 361Equation 6.45ipval 21222
[Ponnusamy] p. 362Equation I1dipcj 21236
[Ponnusamy] p. 362Equation I3cphdir 18588  dipdir 21366  ipdir 16491  ipdiri 21354
[Ponnusamy] p. 362Equation I4ipidsq 21232
[Ponnusamy] p. 362Equation 6.46ip0i 21349
[Ponnusamy] p. 362Equation 6.47ip1i 21351
[Ponnusamy] p. 362Equation 6.48ip2i 21352
[Ponnusamy] p. 363Equation I2cphass 18594  dipass 21369  ipass 16497  ipassi 21365
[Prugovecki] p. 186Definition of brabraval 22470  df-bra 22376
[Prugovecki] p. 376Equation 8.1df-kb 22377  kbval 22480
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22908
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 29228
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22922  atcvat4i 22923  cvrat3 28782  cvrat4 28783  lsatcvat3 28393
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22808  cvrval 28610  df-cv 22805  df-lcv 28360  lspsncv0 15847
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 29240
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 29241
[Quine] p. 16Definition 2.1df-clab 2243  rabid 2689
[Quine] p. 17Definition 2.1''dfsb7 2082
[Quine] p. 18Definition 2.7df-cleq 2249
[Quine] p. 19Definition 2.9conventions 3  df-v 2759
[Quine] p. 34Theorem 5.1abeq2 2361
[Quine] p. 35Theorem 5.2abid2 2373  abid2f 2417
[Quine] p. 40Theorem 6.1sb5 1994
[Quine] p. 40Theorem 6.2sb56 1992  sb6 1993
[Quine] p. 41Theorem 6.3df-clel 2252
[Quine] p. 41Theorem 6.4eqid 2256  eqid1 20786
[Quine] p. 41Theorem 6.5eqcom 2258
[Quine] p. 42Theorem 6.6df-sbc 2953
[Quine] p. 42Theorem 6.7dfsbcq 2954  dfsbcq2 2955
[Quine] p. 43Theorem 6.8vex 2760
[Quine] p. 43Theorem 6.9isset 2761
[Quine] p. 44Theorem 7.3cla4gf 2831  cla4gv 2836  cla4imgf 2829
[Quine] p. 44Theorem 6.11a4sbc 2964  a4sbcd 2965
[Quine] p. 44Theorem 6.12elex 2765
[Quine] p. 44Theorem 6.13elab 2882  elabg 2883  elabgf 2880
[Quine] p. 44Theorem 6.14noel 3420
[Quine] p. 48Theorem 7.2snprc 3655
[Quine] p. 48Definition 7.1df-pr 3607  df-sn 3606
[Quine] p. 49Theorem 7.4snss 3708  snssg 3714
[Quine] p. 49Theorem 7.5prss 3729  prssg 3730
[Quine] p. 49Theorem 7.6prid1 3694  prid1g 3692  prid2 3695  prid2g 3693  snid 3627  snidg 3625
[Quine] p. 51Theorem 7.13prex 4175  snex 4174  snexALT 4154
[Quine] p. 53Theorem 8.2unisn 3803  unisnALT 27736  unisng 3804
[Quine] p. 53Theorem 8.3uniun 3806
[Quine] p. 54Theorem 8.6elssuni 3815
[Quine] p. 54Theorem 8.7uni0 3814
[Quine] p. 56Theorem 8.17uniabio 6221
[Quine] p. 56Definition 8.18dfiota2 6212
[Quine] p. 57Theorem 8.19iotaval 6222
[Quine] p. 57Theorem 8.22iotanul 6226
[Quine] p. 58Theorem 8.23iotaex 6228
[Quine] p. 58Definition 9.1df-op 3609
[Quine] p. 61Theorem 9.5opabid 4229  opelopab 4244  opelopaba 4239  opelopabaf 4246  opelopabf 4247  opelopabg 4241  opelopabga 4236  oprabid 5802
[Quine] p. 64Definition 9.11df-xp 4661
[Quine] p. 64Definition 9.12df-cnv 4663
[Quine] p. 64Definition 9.15df-id 4267
[Quine] p. 65Theorem 10.3fun0 5231
[Quine] p. 65Theorem 10.4funi 5209
[Quine] p. 65Theorem 10.5funsn 5224  funsng 5222
[Quine] p. 65Definition 10.1df-fun 4669
[Quine] p. 65Definition 10.2args 5015  df-fv 4675
[Quine] p. 68Definition 10.11conventions 3  df-fv 4675  fv2 5440
[Quine] p. 124Theorem 17.3nn0opth2 11239  nn0opth2i 11238  nn0opthi 11237  omopthi 6609
[Quine] p. 177Definition 25.2df-rdg 6377
[Quine] p. 232Equation icarddom 8130
[Quine] p. 284Axiom 39(vi)funimaex 5254  funimaexg 5253
[Quine] p. 331Axiom system NFru 2951
[ReedSimon] p. 36Definition (iii)ax-his3 21609
[ReedSimon] p. 63Exercise 4(a)df-dip 21220  polid 21684  polid2i 21682  polidi 21683
[ReedSimon] p. 63Exercise 4(b)df-ph 21337
[ReedSimon] p. 195Remarklnophm 22545  lnophmi 22544
[Retherford] p. 49Exercise 1(i)leopadd 22658
[Retherford] p. 49Exercise 1(ii)leopmul 22660  leopmuli 22659
[Retherford] p. 49Exercise 1(iv)leoptr 22663
[Retherford] p. 49Definition VI.1df-leop 22378  leoppos 22652
[Retherford] p. 49Exercise 1(iii)leoptri 22662
[Retherford] p. 49Definition of operator orderingleop3 22651
[Rudin] p. 164Equation 27efcan 12324
[Rudin] p. 164Equation 30efzval 12330
[Rudin] p. 167Equation 48absefi 12424
[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 5032
[Schechter] p. 51Definition of irreflexivityintirr 5035
[Schechter] p. 51Definition of symmetrycnvsym 5031
[Schechter] p. 51Definition of transitivitycotr 5029
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13436
[Schechter] p. 79Definition of Moore closuredf-mrc 13437
[Schechter] p. 82Section 4.5df-mrc 13437
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13439
[Schechter] p. 139Definition AC3dfac9 7716
[Schechter] p. 141Definition (MC)dfac11 26513
[Schechter] p. 149Axiom DC1ax-dc 8026  axdc3 8034
[Schechter] p. 187Definition of ring with unitisrng 15293  isrngo 20991
[Schechter] p. 276Remark 11.6.espan0 22067
[Schechter] p. 276Definition of spandf-span 21834  spanval 21858
[Schechter] p. 428Definition 15.35bastop1 16679
[Schwabhauser] p. 10Axiom A1axcgrrflx 23903
[Schwabhauser] p. 10Axiom A2axcgrtr 23904
[Schwabhauser] p. 10Axiom A3axcgrid 23905
[Schwabhauser] p. 11Axiom A4axsegcon 23916
[Schwabhauser] p. 11Axiom A5ax5seg 23927
[Schwabhauser] p. 11Axiom A6axbtwnid 23928
[Schwabhauser] p. 12Axiom A7axpasch 23930
[Schwabhauser] p. 12Axiom A8axlowdim2 23949
[Schwabhauser] p. 13Axiom A10axeuclid 23952
[Schwabhauser] p. 13Axiom A11axcont 23965
[Schwabhauser] p. 27Theorem 2.1cgrrflx 23971
[Schwabhauser] p. 27Theorem 2.2cgrcomim 23973
[Schwabhauser] p. 27Theorem 2.3cgrtr 23976
[Schwabhauser] p. 27Theorem 2.4cgrcoml 23980
[Schwabhauser] p. 27Theorem 2.5cgrcomr 23981
[Schwabhauser] p. 28Theorem 2.8cgrtriv 23986
[Schwabhauser] p. 28Theorem 2.105segofs 23990
[Schwabhauser] p. 28Definition 2.10df-ofs 23967
[Schwabhauser] p. 29Theorem 2.11cgrextend 23992
[Schwabhauser] p. 29Theorem 2.12segconeq 23994
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 24006  btwntriv2 23996
[Schwabhauser] p. 30Theorem 3.2btwncomim 23997
[Schwabhauser] p. 30Theorem 3.3btwntriv1 24000
[Schwabhauser] p. 30Theorem 3.4btwnswapid 24001
[Schwabhauser] p. 30Theorem 3.5btwnexch2 24007  btwnintr 24003
[Schwabhauser] p. 30Theorem 3.6btwnexch 24009  btwnexch3 24004
[Schwabhauser] p. 30Theorem 3.7btwnouttr 24008
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23948
[Schwabhauser] p. 32Theorem 3.14btwndiff 24011
[Schwabhauser] p. 33Theorem 3.17trisegint 24012
[Schwabhauser] p. 34Theorem 4.2ifscgr 24028
[Schwabhauser] p. 34Definition 4.1df-ifs 24023
[Schwabhauser] p. 35Theorem 4.3cgrsub 24029
[Schwabhauser] p. 35Theorem 4.5cgrxfr 24039
[Schwabhauser] p. 35Definition 4.4df-cgr3 24024
[Schwabhauser] p. 36Theorem 4.6btwnxfr 24040
[Schwabhauser] p. 36Theorem 4.11colinearperm1 24046  colinearperm2 24048  colinearperm3 24047  colinearperm4 24049  colinearperm5 24050
[Schwabhauser] p. 36Definition 4.10df-colinear 24025
[Schwabhauser] p. 37Theorem 4.12colineartriv1 24051
[Schwabhauser] p. 37Theorem 4.13colinearxfr 24059
[Schwabhauser] p. 37Theorem 4.14lineext 24060
[Schwabhauser] p. 37Theorem 4.16fscgr 24064
[Schwabhauser] p. 37Theorem 4.17linecgr 24065
[Schwabhauser] p. 37Definition 4.15df-fs 24026
[Schwabhauser] p. 38Theorem 4.18lineid 24067
[Schwabhauser] p. 38Theorem 4.19idinside 24068
[Schwabhauser] p. 39Theorem 5.1btwnconn1 24085
[Schwabhauser] p. 41Theorem 5.2btwnconn2 24086
[Schwabhauser] p. 41Theorem 5.3btwnconn3 24087
[Schwabhauser] p. 41Theorem 5.5brsegle2 24093
[Schwabhauser] p. 41Definition 5.4df-segle 24091
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 24094
[Schwabhauser] p. 42Theorem 5.7seglerflx 24096
[Schwabhauser] p. 42Theorem 5.8segletr 24098
[Schwabhauser] p. 42Theorem 5.9segleantisym 24099
[Schwabhauser] p. 42Theorem 5.10seglelin 24100
[Schwabhauser] p. 42Theorem 5.11seglemin 24097
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 24102
[Schwabhauser] p. 43Theorem 6.2btwnoutside 24109
[Schwabhauser] p. 43Theorem 6.3broutsideof3 24110
[Schwabhauser] p. 43Theorem 6.4broutsideof 24105  df-outsideof 24104
[Schwabhauser] p. 43Definition 6.1broutsideof2 24106
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 24111
[Schwabhauser] p. 44Theorem 6.6outsideofcom 24112
[Schwabhauser] p. 44Theorem 6.7outsideoftr 24113
[Schwabhauser] p. 44Theorem 6.11outsideofeu 24115
[Schwabhauser] p. 44Definition 6.8df-ray 24122
[Schwabhauser] p. 45Part 2df-lines2 24123
[Schwabhauser] p. 45Theorem 6.13outsidele 24116
[Schwabhauser] p. 45Theorem 6.15lineunray 24131
[Schwabhauser] p. 45Theorem 6.16lineelsb2 24132
[Schwabhauser] p. 45Theorem 6.17linecom 24134  linerflx1 24133  linerflx2 24135
[Schwabhauser] p. 45Theorem 6.18linethru 24137
[Schwabhauser] p. 45Definition 6.14df-line2 24121
[Schwabhauser] p. 46Theorem 6.19linethrueu 24140
[Schwabhauser] p. 46Theorem 6.21lineintmo 24141
[Shapiro] p. 230Theorem 6.5.1dchrhash 20458  dchrsum 20456  dchrsum2 20455  sumdchr 20459
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20460  sum2dchr 20461
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15249  ablfacrp2 15250
[Shapiro], p. 328Equation 9.2.4vmasum 20403
[Shapiro], p. 329Equation 9.2.7logfac2 20404
[Shapiro], p. 329Equation 9.2.9logfacrlim 20411
[Shapiro], p. 331Equation 9.2.13vmadivsum 20579
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20582
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20636  vmalogdivsum2 20635
[Shapiro], p. 375Theorem 9.4.1dirith 20626  dirith2 20625
[Shapiro], p. 375Equation 9.4.3rplogsum 20624  rpvmasum 20623  rpvmasum2 20609
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20584
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20622
[Shapiro], p. 377Lemma 9.4.1dchrisum 20589  dchrisumlem1 20586  dchrisumlem2 20587  dchrisumlem3 20588  dchrisumlema 20585
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20592
[Shapiro], p. 379Equation 9.4.16dchrmusum 20621  dchrmusumlem 20619  dchrvmasumlem 20620
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20591
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20593
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20617  dchrisum0re 20610  dchrisumn0 20618
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20603
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20607
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20608
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20663  pntrsumbnd2 20664  pntrsumo1 20662
[Shapiro], p. 405Equation 10.2.1mudivsum 20627
[Shapiro], p. 406Equation 10.2.6mulogsum 20629
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20631
[Shapiro], p. 407Equation 10.2.8mulog2sum 20634
[Shapiro], p. 418Equation 10.4.6logsqvma 20639
[Shapiro], p. 418Equation 10.4.8logsqvma2 20640
[Shapiro], p. 419Equation 10.4.10selberg 20645
[Shapiro], p. 420Equation 10.4.12selberg2lem 20647
[Shapiro], p. 420Equation 10.4.14selberg2 20648
[Shapiro], p. 422Equation 10.6.7selberg3 20656
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20657
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20654  selberg3lem2 20655
[Shapiro], p. 422Equation 10.4.23selberg4 20658
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20652
[Shapiro], p. 428Equation 10.6.2selbergr 20665
[Shapiro], p. 429Equation 10.6.8selberg3r 20666
[Shapiro], p. 430Equation 10.6.11selberg4r 20667
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20681
[Shapiro], p. 434Equation 10.6.27pntlema 20693  pntlemb 20694  pntlemc 20692  pntlemd 20691  pntlemg 20695
[Shapiro], p. 435Equation 10.6.29pntlema 20693
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20685
[Shapiro], p. 436Lemma 10.6.2pntibnd 20690
[Shapiro], p. 436Equation 10.6.34pntlema 20693
[Shapiro], p. 436Equation 10.6.35pntlem3 20706  pntleml 20708
[Stoll] p. 13Definition of symmetric differencesymdif1 3394
[Stoll] p. 16Exercise 4.40dif 3486  dif0 3485
[Stoll] p. 16Exercise 4.8difdifdir 3502
[Stoll] p. 17Theorem 5.1(5)undifv 3489
[Stoll] p. 19Theorem 5.2(13)undm 3387
[Stoll] p. 19Theorem 5.2(13')indm 3388
[Stoll] p. 20Remarkinvdif 3371
[Stoll] p. 25Definition of ordered tripledf-ot 3610
[Stoll] p. 43Definitionuniiun 3915
[Stoll] p. 44Definitionintiin 3916
[Stoll] p. 45Definitiondf-iin 3868
[Stoll] p. 45Definition indexed uniondf-iun 3867
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3394
[Strang] p. 242Section 6.3expgrowth 26905
[Suppes] p. 22Theorem 2eq0 3430
[Suppes] p. 22Theorem 4eqss 3155  eqssd 3157  eqssi 3156
[Suppes] p. 23Theorem 5ss0 3446  ss0b 3445
[Suppes] p. 23Theorem 6sstr 3148  sstrALT2 27645
[Suppes] p. 23Theorem 7pssirr 3237
[Suppes] p. 23Theorem 8pssn2lp 3238
[Suppes] p. 23Theorem 9psstr 3241
[Suppes] p. 23Theorem 10pssss 3232
[Suppes] p. 25Theorem 12elin 3319  elun 3277
[Suppes] p. 26Theorem 15inidm 3339
[Suppes] p. 26Theorem 16in0 3441
[Suppes] p. 27Theorem 23unidm 3279
[Suppes] p. 27Theorem 24un0 3440
[Suppes] p. 27Theorem 25ssun1 3299
[Suppes] p. 27Theorem 26ssequn1 3306
[Suppes] p. 27Theorem 27unss 3310
[Suppes] p. 27Theorem 28indir 3378
[Suppes] p. 27Theorem 29undir 3379
[Suppes] p. 28Theorem 32difid 3483  difidALT 3484
[Suppes] p. 29Theorem 33difin 3367
[Suppes] p. 29Theorem 34indif 3372
[Suppes] p. 29Theorem 35undif1 3490
[Suppes] p. 29Theorem 36difun2 3494
[Suppes] p. 29Theorem 37difin0 3488
[Suppes] p. 29Theorem 38disjdif 3487
[Suppes] p. 29Theorem 39difundi 3382
[Suppes] p. 29Theorem 40difindi 3384
[Suppes] p. 30Theorem 41nalset 4111
[Suppes] p. 39Theorem 61uniss 3808
[Suppes] p. 39Theorem 65uniop 4227
[Suppes] p. 41Theorem 70intsn 3858
[Suppes] p. 42Theorem 71intpr 3855  intprg 3856
[Suppes] p. 42Theorem 73op1stb 4527
[Suppes] p. 42Theorem 78intun 3854
[Suppes] p. 44Definition 15(a)dfiun2 3897  dfiun2g 3895
[Suppes] p. 44Definition 15(b)dfiin2 3898
[Suppes] p. 47Theorem 86elpw 3591  elpw2 4128  elpw2g 4127  elpwg 3592  elpwgdedVD 27727
[Suppes] p. 47Theorem 87pwid 3598
[Suppes] p. 47Theorem 89pw0 3722
[Suppes] p. 48Theorem 90pwpw0 3723
[Suppes] p. 52Theorem 101xpss12 4766
[Suppes] p. 52Theorem 102xpindi 4793  xpindir 4794
[Suppes] p. 52Theorem 103xpundi 4715  xpundir 4716
[Suppes] p. 54Theorem 105elirrv 7265
[Suppes] p. 58Theorem 2relss 4749
[Suppes] p. 59Theorem 4eldm 4850  eldm2 4851  eldm2g 4849  eldmg 4848
[Suppes] p. 59Definition 3df-dm 4665
[Suppes] p. 60Theorem 6dmin 4860
[Suppes] p. 60Theorem 8rnun 5063
[Suppes] p. 60Theorem 9rnin 5064
[Suppes] p. 60Definition 4dfrn2 4842
[Suppes] p. 61Theorem 11brcnv 4838  brcnvg 4836
[Suppes] p. 62Equation 5elcnv 4832  elcnv2 4833
[Suppes] p. 62Theorem 12relcnv 5025
[Suppes] p. 62Theorem 15cnvin 5062
[Suppes] p. 62Theorem 16cnvun 5060
[Suppes] p. 63Theorem 20co02 5159
[Suppes] p. 63Theorem 21dmcoss 4918
[Suppes] p. 63Definition 7df-co 4664
[Suppes] p. 64Theorem 26cnvco 4839
[Suppes] p. 64Theorem 27coass 5164
[Suppes] p. 65Theorem 31resundi 4943
[Suppes] p. 65Theorem 34elima 4991  elima2 4992  elima3 4993  elimag 4990
[Suppes] p. 65Theorem 35imaundi 5067
[Suppes] p. 66Theorem 40dminss 5069
[Suppes] p. 66Theorem 41imainss 5070
[Suppes] p. 67Exercise 11cnvxp 5071
[Suppes] p. 81Definition 34dfec2 6617
[Suppes] p. 82Theorem 72elec 6653  elecg 6652
[Suppes] p. 82Theorem 73erth 6658  erth2 6659
[Suppes] p. 83Theorem 74erdisj 6661
[Suppes] p. 89Theorem 96map0b 6760
[Suppes] p. 89Theorem 97map0 6762  map0g 6761
[Suppes] p. 89Theorem 98mapsn 6763
[Suppes] p. 89Theorem 99mapss 6764
[Suppes] p. 91Definition 12(ii)alephsuc 7649
[Suppes] p. 91Definition 12(iii)alephlim 7648
[Suppes] p. 92Theorem 1enref 6848  enrefg 6847
[Suppes] p. 92Theorem 2ensym 6864  ensymb 6863  ensymi 6865
[Suppes] p. 92Theorem 3entr 6867
[Suppes] p. 92Theorem 4unen 6897
[Suppes] p. 94Theorem 15endom 6842
[Suppes] p. 94Theorem 16ssdomg 6861
[Suppes] p. 94Theorem 17domtr 6868
[Suppes] p. 95Theorem 18sbth 6935
[Suppes] p. 97Theorem 23canth2 6968  canth2g 6969
[Suppes] p. 97Definition 3brsdom2 6939  df-sdom 6820  dfsdom2 6938
[Suppes] p. 97Theorem 21(i)sdomirr 6952
[Suppes] p. 97Theorem 22(i)domnsym 6941
[Suppes] p. 97Theorem 21(ii)sdomnsym 6940
[Suppes] p. 97Theorem 22(ii)domsdomtr 6950
[Suppes] p. 97Theorem 22(iv)brdom2 6845
[Suppes] p. 97Theorem 21(iii)sdomtr 6953
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6948
[Suppes] p. 98Exercise 4fundmen 6888  fundmeng 6889
[Suppes] p. 98Exercise 6xpdom3 6914
[Suppes] p. 98Exercise 11sdomentr 6949
[Suppes] p. 104Theorem 37fofi 7096
[Suppes] p. 104Theorem 38pwfi 7105
[Suppes] p. 105Theorem 40pwfi 7105
[Suppes] p. 111Axiom for cardinal numberscarden 8127
[Suppes] p. 130Definition 3df-tr 4074
[Suppes] p. 132Theorem 9ssonuni 4536
[Suppes] p. 134Definition 6df-suc 4356
[Suppes] p. 136Theorem Schema 22findes 4644  finds 4640  finds1 4643  finds2 4642
[Suppes] p. 151Theorem 42isfinite 7307  isfinite2 7069  isfiniteg 7071  unbnn 7067
[Suppes] p. 162Definition 5df-ltnq 8496  df-ltpq 8488
[Suppes] p. 197Theorem Schema 4tfindes 4611  tfinds 4608  tfinds2 4612
[Suppes] p. 209Theorem 18oaord1 6503
[Suppes] p. 209Theorem 21oaword2 6505
[Suppes] p. 211Theorem 25oaass 6513
[Suppes] p. 225Definition 8iscard2 7563
[Suppes] p. 227Theorem 56ondomon 8139
[Suppes] p. 228Theorem 59harcard 7565
[Suppes] p. 228Definition 12(i)aleph0 7647
[Suppes] p. 228Theorem Schema 61onintss 4400
[Suppes] p. 228Theorem Schema 62onminesb 4547  onminsb 4548
[Suppes] p. 229Theorem 64alephval2 8148
[Suppes] p. 229Theorem 65alephcard 7651
[Suppes] p. 229Theorem 66alephord2i 7658
[Suppes] p. 229Theorem 67alephnbtwn 7652
[Suppes] p. 229Definition 12df-aleph 7527
[Suppes] p. 242Theorem 6weth 8076
[Suppes] p. 242Theorem 8entric 8133
[Suppes] p. 242Theorem 9carden 8127
[TakeutiZaring] p. 8Axiom 1ax-ext 2237
[TakeutiZaring] p. 13Definition 4.5df-cleq 2249
[TakeutiZaring] p. 13Proposition 4.6df-clel 2252
[TakeutiZaring] p. 13Proposition 4.9cvjust 2251
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2273
[TakeutiZaring] p. 14Definition 4.16df-oprab 5782
[TakeutiZaring] p. 14Proposition 4.14ru 2951
[TakeutiZaring] p. 15Axiom 2zfpair 4170
[TakeutiZaring] p. 15Exercise 1elpr 3618  elpr2 3619  elprg 3617
[TakeutiZaring] p. 15Exercise 2elsn 3615  elsnc 3623  elsnc2 3629  elsnc2g 3628  elsncg 3622
[TakeutiZaring] p. 15Exercise 3elop 4197
[TakeutiZaring] p. 15Exercise 4sneq 3611  sneqr 3740
[TakeutiZaring] p. 15Definition 5.1dfpr2 3616  dfsn2 3614
[TakeutiZaring] p. 16Axiom 3uniex 4474
[TakeutiZaring] p. 16Exercise 6opth 4203
[TakeutiZaring] p. 16Exercise 7opex 4195
[TakeutiZaring] p. 16Exercise 8rext 4180
[TakeutiZaring] p. 16Corollary 5.8unex 4476  unexg 4479
[TakeutiZaring] p. 16Definition 5.3dftp2 3639
[TakeutiZaring] p. 16Definition 5.5df-uni 3788
[TakeutiZaring] p. 16Definition 5.6df-in 3120  df-un 3118
[TakeutiZaring] p. 16Proposition 5.7unipr 3801  uniprg 3802
[TakeutiZaring] p. 17Axiom 4pwex 4151  pwexg 4152
[TakeutiZaring] p. 17Exercise 1eltp 3638
[TakeutiZaring] p. 17Exercise 5elsuc 4419  elsucg 4417  sstr2 3147
[TakeutiZaring] p. 17Exercise 6uncom 3280
[TakeutiZaring] p. 17Exercise 7incom 3322
[TakeutiZaring] p. 17Exercise 8unass 3293
[TakeutiZaring] p. 17Exercise 9inass 3340
[TakeutiZaring] p. 17Exercise 10indi 3376
[TakeutiZaring] p. 17Exercise 11undi 3377
[TakeutiZaring] p. 17Definition 5.9df-pss 3129  dfss2 3130
[TakeutiZaring] p. 17Definition 5.10df-pw 3587
[TakeutiZaring] p. 18Exercise 7unss2 3307
[TakeutiZaring] p. 18Exercise 9df-ss 3127  sseqin2 3349
[TakeutiZaring] p. 18Exercise 10ssid 3158
[TakeutiZaring] p. 18Exercise 12inss1 3350  inss2 3351
[TakeutiZaring] p. 18Exercise 13nss 3197
[TakeutiZaring] p. 18Exercise 15unieq 3796
[TakeutiZaring] p. 18Exercise 18sspwb 4181  sspwimp 27728  sspwimpALT 27735  sspwimpALT2 27739  sspwimpcf 27730
[TakeutiZaring] p. 18Exercise 19pweqb 4188
[TakeutiZaring] p. 19Axiom 5ax-rep 4091
[TakeutiZaring] p. 20Definitiondf-rab 2525
[TakeutiZaring] p. 20Corollary 5.160ex 4110
[TakeutiZaring] p. 20Definition 5.12df-dif 3116
[TakeutiZaring] p. 20Definition 5.14dfnul2 3418
[TakeutiZaring] p. 20Proposition 5.15difid 3483  difidALT 3484
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3425  n0f 3424  neq0 3426
[TakeutiZaring] p. 21Axiom 6zfreg 7263
[TakeutiZaring] p. 21Axiom 6'zfregs 7368
[TakeutiZaring] p. 21Theorem 5.22setind 7373
[TakeutiZaring] p. 21Definition 5.20df-v 2759
[TakeutiZaring] p. 21Proposition 5.21vprc 4112
[TakeutiZaring] p. 22Exercise 10ss 3444
[TakeutiZaring] p. 22Exercise 3ssex 4118  ssexg 4120
[TakeutiZaring] p. 22Exercise 4inex1 4115
[TakeutiZaring] p. 22Exercise 5ruv 7268
[TakeutiZaring] p. 22Exercise 6elirr 7266
[TakeutiZaring] p. 22Exercise 7ssdif0 3474
[TakeutiZaring] p. 22Exercise 11difdif 3263
[TakeutiZaring] p. 22Exercise 13undif3 3390  undif3VD 27692
[TakeutiZaring] p. 22Exercise 14difss 3264
[TakeutiZaring] p. 22Exercise 15sscon 3271
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2521
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2522
[TakeutiZaring] p. 23Proposition 6.2xpex 4775  xpexg 4774  xpexgALT 5990
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4662
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5236
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5369  fun11 5239
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5192  svrelfun 5237
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4841
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4843
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4667
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4668
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4664
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5102  dfrel2 5098
[TakeutiZaring] p. 25Exercise 3xpss 4767
[TakeutiZaring] p. 25Exercise 5relun 4776
[TakeutiZaring] p. 25Exercise 6reluni 4782
[TakeutiZaring] p. 25Exercise 9inxp 4792
[TakeutiZaring] p. 25Exercise 12relres 4957
[TakeutiZaring] p. 25Exercise 13opelres 4934  opelresg 4936
[TakeutiZaring] p. 25Exercise 14dmres 4950
[TakeutiZaring] p. 25Exercise 15resss 4953
[TakeutiZaring] p. 25Exercise 17resabs1 4958
[TakeutiZaring] p. 25Exercise 18funres 5217
[TakeutiZaring] p. 25Exercise 24relco 5144
[TakeutiZaring] p. 25Exercise 29funco 5216
[TakeutiZaring] p. 25Exercise 30f1co 5370
[TakeutiZaring] p. 26Definition 6.10eu2 2141
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 4675  fv3 5460
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5182  cnvexg 5181
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4915  dmexg 4913
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4916  rnexg 4914
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27012
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27013
[TakeutiZaring] p. 27Corollary 6.13fvex 5458
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5463  tz6.12 5464  tz6.12c 5467
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5466  tz6.12i 5468
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4670
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4671
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4673  wfo 4657
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4672  wf1 4656
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4674  wf1o 4658
[TakeutiZaring] p. 28Exercise 4eqfnfv 5542  eqfnfv2 5543  eqfnfv2f 5546
[TakeutiZaring] p. 28Exercise 5fvco 5515
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5661  fnexALT 5662
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5657  resfunexgALT 5658
[TakeutiZaring] p. 29Exercise 9funimaex 5254  funimaexg 5253
[TakeutiZaring] p. 29Definition 6.18df-br 3984
[TakeutiZaring] p. 30Definition 6.21dffr2 4316  dffr3 5019  eliniseg 5016  iniseg 5018
[TakeutiZaring] p. 30Definition 6.22df-eprel 4263
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4329  fr3nr 4529  frirr 4328
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4310
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4531
[TakeutiZaring] p. 31Exercise 1frss 4318
[TakeutiZaring] p. 31Exercise 4wess 4338
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23560  tz6.26i 23561  wefrc 4345  wereu2 4348
[TakeutiZaring] p. 32Theorem 6.27wfi 23562  wfii 23563
[TakeutiZaring] p. 32Definition 6.28df-isom 4676
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5746
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5747
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5753
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5754
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5755
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5759
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5766
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5768
[TakeutiZaring] p. 35Notationwtr 4073
[TakeutiZaring] p. 35Theorem 7.2trelpss 27014  tz7.2 4335
[TakeutiZaring] p. 35Definition 7.1dftr3 4077
[TakeutiZaring] p. 36Proposition 7.4ordwe 4363
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4371
[TakeutiZaring] p. 36Proposition 7.6ordelord 4372  ordelordALT 27338  ordelordALTVD 27677
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4378  ordelssne 4377
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4376
[TakeutiZaring] p. 37Proposition 7.9ordin 4380
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4538
[TakeutiZaring] p. 38Corollary 7.15ordsson 4539
[TakeutiZaring] p. 38Definition 7.11df-on 4354
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4382
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27351  ordon 4532
[TakeutiZaring] p. 38Proposition 7.13onprc 4534
[TakeutiZaring] p. 39Theorem 7.17tfi 4602
[TakeutiZaring] p. 40Exercise 3ontr2 4397
[TakeutiZaring] p. 40Exercise 7dftr2 4075
[TakeutiZaring] p. 40Exercise 9onssmin 4546
[TakeutiZaring] p. 40Exercise 11unon 4580
[TakeutiZaring] p. 40Exercise 12ordun 4452
[TakeutiZaring] p. 40Exercise 14ordequn 4451
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4535
[TakeutiZaring] p. 40Proposition 7.20elssuni 3815
[TakeutiZaring] p. 41Definition 7.22df-suc 4356
[TakeutiZaring] p. 41Proposition 7.23sssucid 4427  sucidg 4428
[TakeutiZaring] p. 41Proposition 7.24suceloni 4562
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4442  ordnbtwn 4441
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4577
[TakeutiZaring] p. 42Exercise 1df-lim 4355
[TakeutiZaring] p. 42Exercise 4omssnlim 4628
[TakeutiZaring] p. 42Exercise 7ssnlim 4632
[TakeutiZaring] p. 42Exercise 8onsucssi 4590  ordelsuc 4569
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4571
[TakeutiZaring] p. 42Definition 7.27nlimon 4600
[TakeutiZaring] p. 42Definition 7.28dfom2 4616
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4633
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4634
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4635
[TakeutiZaring] p. 43Remarkomon 4625
[TakeutiZaring] p. 43Axiom 7inf3 7290  omex 7298
[TakeutiZaring] p. 43Theorem 7.32ordom 4623
[TakeutiZaring] p. 43Corollary 7.31find 4639
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4636
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4637
[TakeutiZaring] p. 44Exercise 1limomss 4619
[TakeutiZaring] p. 44Exercise 2int0 3836  trint0 4090
[TakeutiZaring] p. 44Exercise 4intss1 3837
[TakeutiZaring] p. 44Exercise 5intex 4129
[TakeutiZaring] p. 44Exercise 6oninton 4549
[TakeutiZaring] p. 44Exercise 11ordintdif 4399
[TakeutiZaring] p. 44Definition 7.35df-int 3823
[TakeutiZaring] p. 44Proposition 7.34noinfep 7314
[TakeutiZaring] p. 45Exercise 4onint 4544
[TakeutiZaring] p. 47Lemma 1tfrlem1 6345
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6367
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6368
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6369
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6373  tz7.44-2 6374  tz7.44-3 6375
[TakeutiZaring] p. 50Exercise 1smogt 6338
[TakeutiZaring] p. 50Exercise 3smoiso 6333
[TakeutiZaring] p. 50Definition 7.46df-smo 6317
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6411  tz7.49c 6412
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6409
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6408
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6410
[TakeutiZaring] p. 53Proposition 7.532eu5 2200
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7593
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7594
[TakeutiZaring] p. 56Definition 8.1oalim 6485  oasuc 6477
[TakeutiZaring] p. 57Remarktfindsg 4609
[TakeutiZaring] p. 57Proposition 8.2oacl 6488
[TakeutiZaring] p. 57Proposition 8.3oa0 6469  oa0r 6491
[TakeutiZaring] p. 57Proposition 8.16omcl 6489
[TakeutiZaring] p. 58Corollary 8.5oacan 6500
[TakeutiZaring] p. 58Proposition 8.4nnaord 6571  nnaordi 6570  oaord 6499  oaordi 6498
[TakeutiZaring] p. 59Proposition 8.6iunss2 3907  uniss2 3818
[TakeutiZaring] p. 59Proposition 8.7oawordri 6502
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6507  oawordex 6509
[TakeutiZaring] p. 59Proposition 8.9nnacl 6563
[TakeutiZaring] p. 59Proposition 8.10oaabs 6596
[TakeutiZaring] p. 60Remarkoancom 7306
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6512
[TakeutiZaring] p. 62Exercise 1nnarcl 6568
[TakeutiZaring] p. 62Exercise 5oaword1 6504
[TakeutiZaring] p. 62Definition 8.15om0 6470  om0x 6472  omlim 6486  omsuc 6479
[TakeutiZaring] p. 63Proposition 8.17nnecl 6565  nnmcl 6564
[TakeutiZaring] p. 63Proposition 8.19nnmord 6584  nnmordi 6583  omord 6520  omordi 6518
[TakeutiZaring] p. 63Proposition 8.20omcan 6521
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6588  omwordri 6524
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6492
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6494  om1r 6495
[TakeutiZaring] p. 64Proposition 8.22om00 6527
[TakeutiZaring] p. 64Proposition 8.23omordlim 6529
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6530
[TakeutiZaring] p. 64Proposition 8.25odi 6531
[TakeutiZaring] p. 65Theorem 8.26omass 6532
[TakeutiZaring] p. 67Definition 8.30nnesuc 6560  oe0 6475  oelim 6487  oesuc 6480  onesuc 6483
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6473
[TakeutiZaring] p. 67Proposition 8.32oen0 6538
[TakeutiZaring] p. 67Proposition 8.33oeordi 6539
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6474
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6497
[TakeutiZaring] p. 68Corollary 8.34oeord 6540
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6546
[TakeutiZaring] p. 68Proposition 8.35oewordri 6544
[TakeutiZaring] p. 68Proposition 8.37oeworde 6545
[TakeutiZaring] p. 69Proposition 8.41oeoa 6549
[TakeutiZaring] p. 70Proposition 8.42oeoe 6551
[TakeutiZaring] p. 73Theorem 9.1trcl 7364  tz9.1 7365
[TakeutiZaring] p. 76Definition 9.9df-r1 7390  r10 7394  r1lim 7398  r1limg 7397  r1suc 7396  r1sucg 7395
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7406  r1ord2 7407  r1ordg 7404
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7416
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7441  tz9.13 7417  tz9.13g 7418
[TakeutiZaring] p. 79Definition 9.14df-rank 7391  rankval 7442  rankvalb 7423  rankvalg 7443
[TakeutiZaring] p. 79Proposition 9.16rankel 7465  rankelb 7450
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7479  rankval3 7466  rankval3b 7452
[TakeutiZaring] p. 79Proposition 9.18rankonid 7455
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7421
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7460  rankr1c 7447  rankr1g 7458
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7461
[TakeutiZaring] p. 80Exercise 1rankss 7475  rankssb 7474
[TakeutiZaring] p. 80Exercise 2unbndrank 7468
[TakeutiZaring] p. 80Proposition 9.19bndrank 7467
[TakeutiZaring] p. 83Axiom of Choiceac4 8056  dfac3 7702
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7611  numth 8053  numth2 8052
[TakeutiZaring] p. 85Definition 10.4cardval 8122
[TakeutiZaring] p. 85Proposition 10.5cardid 8123  cardid2 7540
[TakeutiZaring] p. 85Proposition 10.9oncard 7547
[TakeutiZaring] p. 85Proposition 10.10carden 8127
[TakeutiZaring] p. 85Proposition 10.11cardidm 7546
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7531
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7552
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7544
[TakeutiZaring] p. 87Proposition 10.15pwen 6988
[TakeutiZaring] p. 88Exercise 1en0 6878
[TakeutiZaring] p. 88Exercise 7infensuc 6993
[TakeutiZaring] p. 89Exercise 10omxpen 6918
[TakeutiZaring] p. 90Corollary 10.23cardnn 7550
[TakeutiZaring] p. 90Definition 10.27alephiso 7679
[TakeutiZaring] p. 90Proposition 10.20nneneq 6998
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7004
[TakeutiZaring] p. 90Proposition 10.26alephprc 7680
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7003
[TakeutiZaring] p. 91Exercise 2alephle 7669
[TakeutiZaring] p. 91Exercise 3aleph0 7647
[TakeutiZaring] p. 91Exercise 4cardlim 7559
[TakeutiZaring] p. 91Exercise 7infpss 7797
[TakeutiZaring] p. 91Exercise 8infcntss 7084
[TakeutiZaring] p. 91Definition 10.29df-fin 6821  isfi 6839
[TakeutiZaring] p. 92Proposition 10.32onfin 7005
[TakeutiZaring] p. 92Proposition 10.34imadomg 8113
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6911
[TakeutiZaring] p. 93Proposition 10.35fodomb 8105
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7769  unxpdom 7024
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7561  cardsdomelir 7560
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7026
[TakeutiZaring] p. 94Proposition 10.39infxpen 7596
[TakeutiZaring] p. 95Definition 10.42df-map 6728
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8138  infxpidm2 7598
[TakeutiZaring] p. 95Proposition 10.41infcda 7788  infxp 7795  infxpg 24447
[TakeutiZaring] p. 96Proposition 10.44pw2en 6923  pw2f1o 6921
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6981
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8068
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8063  ac6s5 8072
[TakeutiZaring] p. 98Theorem 10.47unidom 8119
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8120  uniimadomf 8121
[TakeutiZaring] p. 100Definition 11.1cfcof 7854
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7849
[TakeutiZaring] p. 102Exercise 1cfle 7834
[TakeutiZaring] p. 102Exercise 2cf0 7831
[TakeutiZaring] p. 102Exercise 3cfsuc 7837
[TakeutiZaring] p. 102Exercise 4cfom 7844
[TakeutiZaring] p. 102Proposition 11.9coftr 7853
[TakeutiZaring] p. 103Theorem 11.15alephreg 8158
[TakeutiZaring] p. 103Proposition 11.11cardcf 7832
[TakeutiZaring] p. 103Proposition 11.13alephsing 7856
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7678
[TakeutiZaring] p. 104Proposition 11.16carduniima 7677
[TakeutiZaring] p. 104Proposition 11.18alephfp 7689  alephfp2 7690
[TakeutiZaring] p. 106Theorem 11.20gchina 8275
[TakeutiZaring] p. 106Theorem 11.21mappwen 7693
[TakeutiZaring] p. 107Theorem 11.26konigth 8145
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8159
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8160
[Tarski] p. 67Axiom B5ax-4 1692
[Tarski] p. 68Lemma 6avril1 20782  equid 1818  equid1 1820  equidALT 1819
[Tarski] p. 69Lemma 7equcomi-o 1823  equcomi 1822
[Tarski] p. 70Lemma 14a4im 1868  a4ime 1869
[Tarski] p. 70Lemma 16ax-11 1624  ax-11o 1941  ax11i 1833
[Tarski] p. 70Lemmas 16 and 17sb6 1993
[Tarski] p. 75Axiom B8ax-9v 1632
[Tarski] p. 75Scheme B7ax9vax9 28309
[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 12469
[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 2213  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 27737
[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 24281
[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 24274
[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 26906
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26907
[WhiteheadRussell] p. 147Theorem *10.2219.26 1592
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26908
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26909
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26910
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1617
[WhiteheadRussell] p. 151Theorem *10.301albitr 26911
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26912
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26913
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26914
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26915
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26917
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26918
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26919
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26916
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26922
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2078
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26923
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26924
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1610
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26925
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26926
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26927
[WhiteheadRussell] p. 162Theorem *11.322alim 26928
[WhiteheadRussell] p. 162Theorem *11.332albi 26929
[WhiteheadRussell] p. 162Theorem *11.342exim 26930
[WhiteheadRussell] p. 162Theorem *11.36a4sbce-2 26932
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26931
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1609
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26934
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26935
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26933
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1571
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26936
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26937
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1578
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26938
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2025  pm11.53g 24316
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26939
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26944
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26940
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26941
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26942
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26943
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26948
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26945
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26946
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26947
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26949
[WhiteheadRussell] p. 175Definition *14.02df-eu 2121
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 26961  pm13.13b 26962
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 26963
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2491
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2492
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2876
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 26969
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 26970
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 26964
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27355  pm13.193 26965
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 26966
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 26967
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 26968
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 26975
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 26974
[WhiteheadRussell] p. 184Definition *14.01iotasbc 26973
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3004
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 26976  pm14.122b 26977  pm14.122c 26978
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 26979  pm14.123b 26980  pm14.123c 26981
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 26983
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 26982
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 26984
[WhiteheadRussell] p. 190Theorem *14.22iota4 6229
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 26985
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6230
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 26986
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 26988
[WhiteheadRussell] p. 192Theorem *14.26eupick 2179  eupickbi 2182  sbaniota 26989
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 26987
[WhiteheadRussell] p. 192Theorem *14.271eubi 26990
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 26991
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 4675
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7587  pm54.43lem 7586
[Young] p. 141Definition of operator orderingleop2 22650
[Young] p. 142Example 12.2(i)0leop 22656  idleop 22657
[vandenDries] p. 42Lemma 61irrapx1 26266
[vandenDries] p. 43Theorem 62pellex 26273  pellexlem1 26267

This page was last updated on 18-Jun-2017.
Copyright terms: Public domain