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 13653
[Adamek] p. 29Proposition 3.14(1)invinv 13667
[Adamek] p. 29Proposition 3.14(2)invco 13668  isoco 13670
[AitkenIBCG] p. 2Axiom C-1 C-2, C-3, C-4, C-5, C-6df-ibcg 25590
[AitkenIBCG] p. 3Definition 2df-angtrg 25586  df-trcng 25589
[AitkenIBG] p. 1Definition of an Incidence-Betweenness Geometrybisig0 25462  df-ig2 25461
[AitkenIBG] p. 2Definition 4df-li 25477
[AitkenIBG] p. 3Definition 5df-col 25491
[AitkenIBG] p. 3Definition 6df-con2 25496
[AitkenIBG] p. 3Proposition 4isconcl5a 25501  isconcl5ab 25502  isconcl6a 25503  isconcl6ab 25504
[AitkenIBG] p. 3Axioms B-1, B-2, B-3, B-4df-ibg2 25509
[AitkenIBG] p. 4Exercise 5tpne 25475
[AitkenIBG] p. 4Definition 8df-seg2 25531
[AitkenIBG] p. 4Definition 10df-sside 25563
[AitkenIBG] p. 4Definition 11df-ray2 25552
[AitkenIBG] p. 10Definition 17df-angle 25558
[AitkenIBG] p. 15Definition 23df-triangle 25560
[AitkenIBG] p. 15Definition 24df-cnvx 25579
[AitkenNG] p. 2Definition 1df-slices 25593
[AitkenNG] p. 2Definition 2df-Cut 25595
[AitkenNG] p. 3Axiom of Dedekinddf-neug 25597
[AitkenNG] p. 4Definition 5df-crcl 25599
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 18212  df-nmoo 21316
[AkhiezerGlazman] p. 64Theoremhmopidmch 22726  hmopidmchi 22724
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 22774  pjcmul2i 22775
[AkhiezerGlazman] p. 72Theoremcnvunop 22491  unoplin 22493
[AkhiezerGlazman] p. 72Equation 2unopadj 22492  unopadj2 22511
[AkhiezerGlazman] p. 73Theoremelunop2 22586  lnopunii 22585
[AkhiezerGlazman] p. 80Proposition 1adjlnop 22659
[Apostol] p. 18Theorem I.1addcan 8992  addcan2d 9012  addcan2i 9002  addcand 9011  addcani 9001
[Apostol] p. 18Theorem I.2negeu 9038
[Apostol] p. 18Theorem I.3negsub 9091  negsubd 9159  negsubi 9120
[Apostol] p. 18Theorem I.4negneg 9093  negnegd 9144  negnegi 9112
[Apostol] p. 18Theorem I.5subdi 9209  subdid 9231  subdii 9224  subdir 9210  subdird 9232  subdiri 9225
[Apostol] p. 18Theorem I.6mul01 8987  mul01d 9007  mul01i 8998  mul02 8986  mul02d 9006  mul02i 8997
[Apostol] p. 18Theorem I.7mulcan 9401  mulcan2d 9398  mulcand 9397  mulcani 9403
[Apostol] p. 18Theorem I.8receu 9409
[Apostol] p. 18Theorem I.9divrec 9436  divrecd 9535  divreci 9501  divreczi 9494
[Apostol] p. 18Theorem I.10recrec 9453  recreci 9488
[Apostol] p. 18Theorem I.11mul0or 9404  mul0ord 9414  mul0ori 9412
[Apostol] p. 18Theorem I.12mul2neg 9215  mul2negd 9230  mul2negi 9223  mulneg1 9212  mulneg1d 9228  mulneg1i 9221
[Apostol] p. 18Theorem I.13divadddiv 9471  divadddivd 9576  divadddivi 9518
[Apostol] p. 18Theorem I.14divmuldiv 9456  divmuldivd 9573  divmuldivi 9516
[Apostol] p. 18Theorem I.15divdivdiv 9457  divdivdivd 9579  divdivdivi 9519
[Apostol] p. 20Axiom 7rpaddcl 10370  rpaddcld 10401  rpmulcl 10371  rpmulcld 10402
[Apostol] p. 20Axiom 8rpneg 10379
[Apostol] p. 20Axiom 90nrp 10380
[Apostol] p. 20Theorem I.17lttri 8941
[Apostol] p. 20Theorem I.18ltadd1d 9361  ltadd1dd 9379  ltadd1i 9323
[Apostol] p. 20Theorem I.19ltmul1 9602  ltmul1a 9601  ltmul1i 9671  ltmul1ii 9681  ltmul2 9603  ltmul2d 10424  ltmul2dd 10438  ltmul2i 9674
[Apostol] p. 20Theorem I.20msqgt0 9290  msqgt0d 9336  msqgt0i 9306
[Apostol] p. 20Theorem I.210lt1 9292
[Apostol] p. 20Theorem I.23lt0neg1 9276  lt0neg1d 9338  ltneg 9270  ltnegd 9346  ltnegi 9313
[Apostol] p. 20Theorem I.25lt2add 9255  lt2addd 9390  lt2addi 9331
[Apostol] p. 20Definition of positive numbersdf-rp 10351
[Apostol] p. 21Exercise 4recgt0 9596  recgt0d 9687  recgt0i 9657  recgt0ii 9658
[Apostol] p. 22Definition of integersdf-z 10021
[Apostol] p. 22Definition of positive integersdfnn3 9756
[Apostol] p. 22Definition of rationalsdf-q 10313
[Apostol] p. 24Theorem I.26supeu 7201
[Apostol] p. 26Theorem I.28nnunb 9957
[Apostol] p. 26Theorem I.29arch 9958
[Apostol] p. 28Exercise 2btwnz 10110
[Apostol] p. 28Exercise 3nnrecl 9959
[Apostol] p. 28Exercise 4rebtwnz 10311
[Apostol] p. 28Exercise 5zbtwnre 10310
[Apostol] p. 28Exercise 6qbtwnre 10521
[Apostol] p. 28Exercise 10(a)zneo 10090
[Apostol] p. 29Theorem I.35msqsqrd 11917  resqrth 11736  sqrth 11843  sqrthi 11849  sqsqrd 11916
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 9745
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 10280
[Apostol] p. 361Remarkcrreczi 11221
[Apostol] p. 363Remarkabsgt0i 11877
[Apostol] p. 363Exampleabssubd 11930  abssubi 11881
[Baer] p. 40Property (b)mapdord 31096
[Baer] p. 40Property (c)mapd11 31097
[Baer] p. 40Property (e)mapdin 31120  mapdlsm 31122
[Baer] p. 40Property (f)mapd0 31123
[Baer] p. 40Definition of projectivitydf-mapd 31083  mapd1o 31106
[Baer] p. 41Property (g)mapdat 31125
[Baer] p. 44Part (1)mapdpg 31164
[Baer] p. 45Part (2)hdmap1eq 31260  mapdheq 31186  mapdheq2 31187  mapdheq2biN 31188
[Baer] p. 45Part (3)baerlem3 31171
[Baer] p. 46Part (4)mapdheq4 31190  mapdheq4lem 31189
[Baer] p. 46Part (5)baerlem5a 31172  baerlem5abmN 31176  baerlem5amN 31174  baerlem5b 31173  baerlem5bmN 31175
[Baer] p. 47Part (6)hdmap1l6 31280  hdmap1l6a 31268  hdmap1l6e 31273  hdmap1l6f 31274  hdmap1l6g 31275  hdmap1l6lem1 31266  hdmap1l6lem2 31267  hdmap1p6N 31281  mapdh6N 31205  mapdh6aN 31193  mapdh6eN 31198  mapdh6fN 31199  mapdh6gN 31200  mapdh6lem1N 31191  mapdh6lem2N 31192
[Baer] p. 48Part 9hdmapval 31289
[Baer] p. 48Part 10hdmap10 31301
[Baer] p. 48Part 11hdmapadd 31304
[Baer] p. 48Part (6)hdmap1l6h 31276  mapdh6hN 31201
[Baer] p. 48Part (7)mapdh75cN 31211  mapdh75d 31212  mapdh75e 31210  mapdh75fN 31213  mapdh7cN 31207  mapdh7dN 31208  mapdh7eN 31206  mapdh7fN 31209
[Baer] p. 48Part (8)mapdh8 31247  mapdh8a 31233  mapdh8aa 31234  mapdh8ab 31235  mapdh8ac 31236  mapdh8ad 31237  mapdh8b 31238  mapdh8c 31239  mapdh8d 31241  mapdh8d0N 31240  mapdh8e 31242  mapdh8fN 31243  mapdh8g 31244  mapdh8i 31245  mapdh8j 31246
[Baer] p. 48Part (9)mapdh9a 31248
[Baer] p. 48Equation 10mapdhvmap 31227
[Baer] p. 49Part 12hdmap11 31309  hdmapeq0 31305  hdmapf1oN 31326  hdmapneg 31307  hdmaprnN 31325  hdmaprnlem1N 31310  hdmaprnlem3N 31311  hdmaprnlem3uN 31312  hdmaprnlem4N 31314  hdmaprnlem6N 31315  hdmaprnlem7N 31316  hdmaprnlem8N 31317  hdmaprnlem9N 31318  hdmapsub 31308
[Baer] p. 49Part 14hdmap14lem1 31329  hdmap14lem10 31338  hdmap14lem1a 31327  hdmap14lem2N 31330  hdmap14lem2a 31328  hdmap14lem3 31331  hdmap14lem8 31336  hdmap14lem9 31337
[Baer] p. 50Part 14hdmap14lem11 31339  hdmap14lem12 31340  hdmap14lem13 31341  hdmap14lem14 31342  hdmap14lem15 31343  hgmapval 31348
[Baer] p. 50Part 15hgmapadd 31355  hgmapmul 31356  hgmaprnlem2N 31358  hgmapvs 31352
[Baer] p. 50Part 16hgmaprnN 31362
[Baer] p. 110Lemma 1hdmapip0com 31378
[Baer] p. 110Line 27hdmapinvlem1 31379
[Baer] p. 110Line 28hdmapinvlem2 31380
[Baer] p. 110Line 30hdmapinvlem3 31381
[Baer] p. 110Part 1.2hdmapglem5 31383  hgmapvv 31387
[Baer] p. 110Proposition 1hdmapinvlem4 31382
[Baer] p. 111Line 10hgmapvvlem1 31384
[Baer] p. 111Line 15hdmapg 31391  hdmapglem7 31390
[BellMachover] p. 36Lemma 10.3id1 22
[BellMachover] p. 97Definition 10.1df-eu 2149
[BellMachover] p. 460Notationdf-mo 2150
[BellMachover] p. 460Definitionmo3 2176
[BellMachover] p. 461Axiom Extax-ext 2266
[BellMachover] p. 462Theorem 1.1bm1.1 2270
[BellMachover] p. 463Axiom Repaxrep5 4138
[BellMachover] p. 463Scheme Sepaxsep 4142
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4146
[BellMachover] p. 466Axiom Powaxpow3 4191
[BellMachover] p. 466Axiom Unionaxun2 4514
[BellMachover] p. 468Definitiondf-ord 4395
[BellMachover] p. 469Theorem 2.2(i)ordirr 4410
[BellMachover] p. 469Theorem 2.2(iii)onelon 4417
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4412
[BellMachover] p. 471Definition of Ndf-om 4657
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4597
[BellMachover] p. 471Definition of Limdf-lim 4397
[BellMachover] p. 472Axiom Infzfinf2 7339
[BellMachover] p. 473Theorem 2.8limom 4671
[BellMachover] p. 477Equation 3.1df-r1 7432
[BellMachover] p. 478Definitionrankval2 7486
[BellMachover] p. 478Theorem 3.3(i)r1ord3 7450  r1ord3g 7447
[BellMachover] p. 480Axiom Regzfreg2 7306
[BellMachover] p. 488Axiom ACac5 8100  dfac4 7745
[BellMachover] p. 490Definition of alephalephval3 7733
[BeltramettiCassinelli] p. 98Remarkatlatmstc 28777
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 22926
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 22968  chirredi 22967
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 22956
[Beran] p. 3Definition of joinsshjval3 21926
[Beran] p. 39Theorem 2.3(i)cmcm2 22188  cmcm2i 22165  cmcm2ii 22170  cmt2N 28708
[Beran] p. 40Theorem 2.3(iii)lecm 22189  lecmi 22174  lecmii 22175
[Beran] p. 45Theorem 3.4cmcmlem 22163
[Beran] p. 49Theorem 4.2cm2j 22192  cm2ji 22197  cm2mi 22198
[Beran] p. 95Definitiondf-sh 21779  issh2 21781
[Beran] p. 95Lemma 3.1(S5)his5 21658
[Beran] p. 95Lemma 3.1(S6)his6 21671
[Beran] p. 95Lemma 3.1(S7)his7 21662
[Beran] p. 95Lemma 3.2(S8)ho01i 22401
[Beran] p. 95Lemma 3.2(S9)hoeq1 22403
[Beran] p. 95Lemma 3.2(S10)ho02i 22402
[Beran] p. 95Lemma 3.2(S11)hoeq2 22404
[Beran] p. 95Postulate (S1)ax-his1 21654  his1i 21672
[Beran] p. 95Postulate (S2)ax-his2 21655
[Beran] p. 95Postulate (S3)ax-his3 21656
[Beran] p. 95Postulate (S4)ax-his4 21657
[Beran] p. 96Definition of normdf-hnorm 21541  dfhnorm2 21694  normval 21696
[Beran] p. 96Definition for Cauchy sequencehcau 21756
[Beran] p. 96Definition of Cauchy sequencedf-hcau 21546
[Beran] p. 96Definition of complete subspaceisch3 21814
[Beran] p. 96Definition of convergedf-hlim 21545  hlimi 21760
[Beran] p. 97Theorem 3.3(i)norm-i-i 21705  norm-i 21701
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 21709  norm-ii 21710  normlem0 21681  normlem1 21682  normlem2 21683  normlem3 21684  normlem4 21685  normlem5 21686  normlem6 21687  normlem7 21688  normlem7tALT 21691
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 21711  norm-iii 21712
[Beran] p. 98Remark 3.4bcs 21753  bcsiALT 21751  bcsiHIL 21752
[Beran] p. 98Remark 3.4(B)normlem9at 21693  normpar 21727  normpari 21726
[Beran] p. 98Remark 3.4(C)normpyc 21718  normpyth 21717  normpythi 21714
[Beran] p. 99Remarklnfn0 22620  lnfn0i 22615  lnop0 22539  lnop0i 22543
[Beran] p. 99Theorem 3.5(i)nmcexi 22599  nmcfnex 22626  nmcfnexi 22624  nmcopex 22602  nmcopexi 22600
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 22627  nmcfnlbi 22625  nmcoplb 22603  nmcoplbi 22601
[Beran] p. 99Theorem 3.5(iii)lnfncon 22629  lnfnconi 22628  lnopcon 22608  lnopconi 22607
[Beran] p. 100Lemma 3.6normpar2i 21728
[Beran] p. 101Lemma 3.6norm3adifi 21725  norm3adifii 21720  norm3dif 21722  norm3difi 21719
[Beran] p. 102Theorem 3.7(i)chocunii 21873  pjhth 21965  pjhtheu 21966  pjpjhth 21997  pjpjhthi 21998  pjth 18798
[Beran] p. 102Theorem 3.7(ii)ococ 21978  ococi 21977
[Beran] p. 103Remark 3.8nlelchi 22634
[Beran] p. 104Theorem 3.9riesz3i 22635  riesz4 22637  riesz4i 22636
[Beran] p. 104Theorem 3.10cnlnadj 22652  cnlnadjeu 22651  cnlnadjeui 22650  cnlnadji 22649  cnlnadjlem1 22640  nmopadjlei 22661
[Beran] p. 106Theorem 3.11(i)adjeq0 22664
[Beran] p. 106Theorem 3.11(v)nmopadji 22663
[Beran] p. 106Theorem 3.11(ii)adjmul 22665
[Beran] p. 106Theorem 3.11(iv)adjadj 22509
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 22675  nmopcoadji 22674
[Beran] p. 106Theorem 3.11(iii)adjadd 22666
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 22676
[Beran] p. 106Theorem 3.11(viii)adjcoi 22673  pjadj2coi 22777  pjadjcoi 22734
[Beran] p. 107Definitiondf-ch 21794  isch2 21796
[Beran] p. 107Remark 3.12choccl 21878  isch3 21814  occl 21876  ocsh 21855  shoccl 21877  shocsh 21856
[Beran] p. 107Remark 3.12(B)ococin 21980
[Beran] p. 108Theorem 3.13chintcl 21904
[Beran] p. 109Property (i)pjadj2 22760  pjadj3 22761  pjadji 22257  pjadjii 22246
[Beran] p. 109Property (ii)pjidmco 22754  pjidmcoi 22750  pjidmi 22245
[Beran] p. 110Definition of projector orderingpjordi 22746
[Beran] p. 111Remarkho0val 22323  pjch1 22242
[Beran] p. 111Definitiondf-hfmul 22307  df-hfsum 22306  df-hodif 22305  df-homul 22304  df-hosum 22303
[Beran] p. 111Lemma 4.4(i)pjo 22243
[Beran] p. 111Lemma 4.4(ii)pjch 22266  pjchi 22004
[Beran] p. 111Lemma 4.4(iii)pjoc2 22011  pjoc2i 22010
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 22252
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 22738  pjssmii 22253
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 22737
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 22736
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 22741
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 22739  pjssge0ii 22254
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 22740  pjdifnormii 22255
[BourbakiEns] p. Proposition 8fcof1 5759  fcofo 5760
[BourbakiFVR] p. Definition 1isder 25107
[BourbakiTop1] p. Remarkxnegmnf 10532  xnegpnf 10531
[BourbakiTop1] p. Remark rexneg 10533
[BourbakiTop1] p. Theoremneiss 16841
[BourbakiTop1] p. Axiom GT'tgpsubcn 17768
[BourbakiTop1] p. Example 1snfil 17554
[BourbakiTop1] p. Example 2neifil 17570
[BourbakiTop1] p. Definitionistgp 17755
[BourbakiTop1] p. Propositioncnpco 16991  ishmeo 17445  neips 16845
[BourbakiTop1] p. Definition 1filintn0 17551
[BourbakiTop1] p. Proposition 9cnpflf2 17690
[BourbakiTop1] p. Theorem 1 (d)iscncl 16993
[BourbakiTop1] p. Proposition Vissnei2 16848
[BourbakiTop1] p. Definition C'''df-cmp 17109
[BourbakiTop1] p. Proposition Viiinnei 16857
[BourbakiTop1] p. Proposition Vivneissex 16859
[BourbakiTop1] p. Proposition Viiielnei 16843  ssnei 16842
[BourbakiTop1] p. Remark below def. 1filn0 17552
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 17536
[BourbakiTop1] p. Section of a finite set of filters. Paragraph 3infil 17553
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 27213  stoweid 27212
[BrosowskiDeutsh] p. 89Theorem for the non trivial casestoweidlem62 27211
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 27150  stoweidlem10 27159  stoweidlem14 27163  stoweidlem15 27164  stoweidlem35 27184  stoweidlem36 27185  stoweidlem37 27186  stoweidlem38 27187  stoweidlem40 27189  stoweidlem41 27190  stoweidlem43 27192  stoweidlem44 27193  stoweidlem46 27195  stoweidlem5 27154  stoweidlem50 27199  stoweidlem52 27201  stoweidlem53 27202  stoweidlem55 27204  stoweidlem56 27205
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 27172  stoweidlem24 27173  stoweidlem27 27176  stoweidlem28 27177  stoweidlem30 27179
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 27194  stoweidlem49 27198  stoweidlem7 27156
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 27180  stoweidlem39 27188  stoweidlem42 27191  stoweidlem48 27197  stoweidlem51 27200  stoweidlem54 27203  stoweidlem57 27206  stoweidlem58 27207
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 27174
[BrosowskiDeutsh] p. 91Lemma proves that for all ` ` in ` ` there is a ` ` as in the proofstoweidlem34 27183
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 27166
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function ` ` as in the proofstoweidlem59 27208
[BrosowskiDeutsh] p. 91Lemma proves that there exists a function g as in the proofstoweidlem60 27209
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 27167
[BrosowskiDeutsh] p. 92Lemma is used to prove that there is a function ` ` as in the proofstoweidlem11 27160  stoweidlem26 27175
[BrosowskiDeutsh] p. 92Lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon ,stoweidlem13 27162
[BrosowskiDeutsh] p. 92Lemma proves that there exists a function ` ` as in the proofstoweidlem61 27210
[ChoquetDD] p. 2Definition of mappingdf-mpt 4081
[Clemente] p. 10Definition ITnatded 4
[Clemente] p. 10Definition I` `m,nnatded 4
[Clemente] p. 11Definition E=>m,nnatded 4
[Clemente] p. 11Definition I=>m,nnatded 4
[Clemente] p. 11Definition E` `(1)natded 4
[Clemente] p. 11Definition E` `(2)natded 4
[Clemente] p. 12Definition E` `m,n,pnatded 4
[Clemente] p. 12Definition I` `n(1)natded 4
[Clemente] p. 12Definition I` `n(2)natded 4
[Clemente] p. 13Definition I` `m,n,pnatded 4
[Clemente] p. 14Definition E` `nnatded 4
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 20813  ex-natded5.2 20812
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 20816  ex-natded5.3 20815
[Clemente] p. 18Theorem 5.5ex-natded5.5 20818
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 20820  ex-natded5.7 20819
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 20822  ex-natded5.8 20821
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 20824  ex-natded5.13 20823
[Clemente] p. 32Definition I` `nnatded 4
[Clemente] p. 32Definition E` `m,n,p,anatded 4
[Clemente] p. 32Definition E` `n,tnatded 4
[Clemente] p. 32Definition I` `n,tnatded 4
[Clemente] p. 43Theorem 9.20ex-natded9.20 20825
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 20826
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 20828  ex-natded9.26 20827
[Cohen] p. 301Remarkrelogoprlem 19939
[Cohen] p. 301Property 2relogmul 19940  relogmuld 19971
[Cohen] p. 301Property 3relogdiv 19941  relogdivd 19972
[Cohen] p. 301Property 4relogexp 19944
[Cohen] p. 301Property 1alog1 19934
[Cohen] p. 301Property 1bloge 19935
[Cohn] p. 81Section II.5acsdomd 14279  acsinfd 14278  acsinfdimd 14280  acsmap2d 14277  acsmapd 14276
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 10960
[Crawley] p. 1Definition of posetdf-poset 14075
[Crawley] p. 107Theorem 13.2hlsupr 28843
[Crawley] p. 110Theorem 13.3arglem1N 29647  dalaw 29343
[Crawley] p. 111Theorem 13.4hlathil 31422
[Crawley] p. 111Definition of set Wdf-watsN 29447
[Crawley] p. 111Definition of dilationdf-dilN 29563  df-ldil 29561  isldil 29567
[Crawley] p. 111Definition of translationdf-ltrn 29562  df-trnN 29564  isltrn 29576  ltrnu 29578
[Crawley] p. 112Lemma Acdlema1N 29248  cdlema2N 29249  exatleN 28861
[Crawley] p. 112Lemma B1cvrat 28933  cdlemb 29251  cdlemb2 29498  cdlemb3 30063  idltrn 29607  l1cvat 28513  lhpat 29500  lhpat2 29502  lshpat 28514  ltrnel 29596  ltrnmw 29608
[Crawley] p. 112Lemma Ccdlemc1 29648  cdlemc2 29649  ltrnnidn 29631  trlat 29626  trljat1 29623  trljat2 29624  trljat3 29625  trlne 29642  trlnidat 29630  trlnle 29643
[Crawley] p. 112Definition of automorphismdf-pautN 29448
[Crawley] p. 113Lemma Ccdlemc 29654  cdlemc3 29650  cdlemc4 29651
[Crawley] p. 113Lemma Dcdlemd 29664  cdlemd1 29655  cdlemd2 29656  cdlemd3 29657  cdlemd4 29658  cdlemd5 29659  cdlemd6 29660  cdlemd7 29661  cdlemd8 29662  cdlemd9 29663  cdleme31sde 29842  cdleme31se 29839  cdleme31se2 29840  cdleme31snd 29843  cdleme32a 29898  cdleme32b 29899  cdleme32c 29900  cdleme32d 29901  cdleme32e 29902  cdleme32f 29903  cdleme32fva 29894  cdleme32fva1 29895  cdleme32fvcl 29897  cdleme32le 29904  cdleme48fv 29956  cdleme4gfv 29964  cdleme50eq 29998  cdleme50f 29999  cdleme50f1 30000  cdleme50f1o 30003  cdleme50laut 30004  cdleme50ldil 30005  cdleme50lebi 29997  cdleme50rn 30002  cdleme50rnlem 30001  cdlemeg49le 29968  cdlemeg49lebilem 29996
[Crawley] p. 113Lemma Ecdleme 30017  cdleme00a 29666  cdleme01N 29678  cdleme02N 29679  cdleme0a 29668  cdleme0aa 29667  cdleme0b 29669  cdleme0c 29670  cdleme0cp 29671  cdleme0cq 29672  cdleme0dN 29673  cdleme0e 29674  cdleme0ex1N 29680  cdleme0ex2N 29681  cdleme0fN 29675  cdleme0gN 29676  cdleme0moN 29682  cdleme1 29684  cdleme10 29711  cdleme10tN 29715  cdleme11 29727  cdleme11a 29717  cdleme11c 29718  cdleme11dN 29719  cdleme11e 29720  cdleme11fN 29721  cdleme11g 29722  cdleme11h 29723  cdleme11j 29724  cdleme11k 29725  cdleme11l 29726  cdleme12 29728  cdleme13 29729  cdleme14 29730  cdleme15 29735  cdleme15a 29731  cdleme15b 29732  cdleme15c 29733  cdleme15d 29734  cdleme16 29742  cdleme16aN 29716  cdleme16b 29736  cdleme16c 29737  cdleme16d 29738  cdleme16e 29739  cdleme16f 29740  cdleme16g 29741  cdleme19a 29760  cdleme19b 29761  cdleme19c 29762  cdleme19d 29763  cdleme19e 29764  cdleme19f 29765  cdleme1b 29683  cdleme2 29685  cdleme20aN 29766  cdleme20bN 29767  cdleme20c 29768  cdleme20d 29769  cdleme20e 29770  cdleme20f 29771  cdleme20g 29772  cdleme20h 29773  cdleme20i 29774  cdleme20j 29775  cdleme20k 29776  cdleme20l 29779  cdleme20l1 29777  cdleme20l2 29778  cdleme20m 29780  cdleme20y 29759  cdleme20zN 29758  cdleme21 29794  cdleme21d 29787  cdleme21e 29788  cdleme22a 29797  cdleme22aa 29796  cdleme22b 29798  cdleme22cN 29799  cdleme22d 29800  cdleme22e 29801  cdleme22eALTN 29802  cdleme22f 29803  cdleme22f2 29804  cdleme22g 29805  cdleme23a 29806  cdleme23b 29807  cdleme23c 29808  cdleme26e 29816  cdleme26eALTN 29818  cdleme26ee 29817  cdleme26f 29820  cdleme26f2 29822  cdleme26f2ALTN 29821  cdleme26fALTN 29819  cdleme27N 29826  cdleme27a 29824  cdleme27cl 29823  cdleme28c 29829  cdleme3 29694  cdleme30a 29835  cdleme31fv 29847  cdleme31fv1 29848  cdleme31fv1s 29849  cdleme31fv2 29850  cdleme31id 29851  cdleme31sc 29841  cdleme31sdnN 29844  cdleme31sn 29837  cdleme31sn1 29838  cdleme31sn1c 29845  cdleme31sn2 29846  cdleme31so 29836  cdleme35a 29905  cdleme35b 29907  cdleme35c 29908  cdleme35d 29909  cdleme35e 29910  cdleme35f 29911  cdleme35fnpq 29906  cdleme35g 29912  cdleme35h 29913  cdleme35h2 29914  cdleme35sn2aw 29915  cdleme35sn3a 29916  cdleme36a 29917  cdleme36m 29918  cdleme37m 29919  cdleme38m 29920  cdleme38n 29921  cdleme39a 29922  cdleme39n 29923  cdleme3b 29686  cdleme3c 29687  cdleme3d 29688  cdleme3e 29689  cdleme3fN 29690  cdleme3fa 29693  cdleme3g 29691  cdleme3h 29692  cdleme4 29695  cdleme40m 29924  cdleme40n 29925  cdleme40v 29926  cdleme40w 29927  cdleme41fva11 29934  cdleme41sn3aw 29931  cdleme41sn4aw 29932  cdleme41snaw 29933  cdleme42a 29928  cdleme42b 29935  cdleme42c 29929  cdleme42d 29930  cdleme42e 29936  cdleme42f 29937  cdleme42g 29938  cdleme42h 29939  cdleme42i 29940  cdleme42k 29941  cdleme42ke 29942  cdleme42keg 29943  cdleme42mN 29944  cdleme42mgN 29945  cdleme43aN 29946  cdleme43bN 29947  cdleme43cN 29948  cdleme43dN 29949  cdleme5 29697  cdleme50ex 30016  cdleme50ltrn 30014  cdleme51finvN 30013  cdleme51finvfvN 30012  cdleme51finvtrN 30015  cdleme6 29698  cdleme7 29706  cdleme7a 29700  cdleme7aa 29699  cdleme7b 29701  cdleme7c 29702  cdleme7d 29703  cdleme7e 29704  cdleme7ga 29705  cdleme8 29707  cdleme8tN 29712  cdleme9 29710  cdleme9a 29708  cdleme9b 29709  cdleme9tN 29714  cdleme9taN 29713  cdlemeda 29755  cdlemedb 29754  cdlemednpq 29756  cdlemednuN 29757  cdlemefr27cl 29860  cdlemefr32fva1 29867  cdlemefr32fvaN 29866  cdlemefrs32fva 29857  cdlemefrs32fva1 29858  cdlemefs27cl 29870  cdlemefs32fva1 29880  cdlemefs32fvaN 29879  cdlemesner 29753  cdlemeulpq 29677
[Crawley] p. 114Lemma E4atex 29533  4atexlem7 29532  cdleme0nex 29747  cdleme17a 29743  cdleme17c 29745  cdleme17d 29955  cdleme17d1 29746  cdleme17d2 29952  cdleme18a 29748  cdleme18b 29749  cdleme18c 29750  cdleme18d 29752  cdleme4a 29696
[Crawley] p. 115Lemma Ecdleme21a 29782  cdleme21at 29785  cdleme21b 29783  cdleme21c 29784  cdleme21ct 29786  cdleme21f 29789  cdleme21g 29790  cdleme21h 29791  cdleme21i 29792  cdleme22gb 29751
[Crawley] p. 116Lemma Fcdlemf 30020  cdlemf1 30018  cdlemf2 30019
[Crawley] p. 116Lemma Gcdlemftr1 30024  cdlemg16 30114  cdlemg28 30161  cdlemg28a 30150  cdlemg28b 30160  cdlemg3a 30054  cdlemg42 30186  cdlemg43 30187  cdlemg44 30190  cdlemg44a 30188  cdlemg46 30192  cdlemg47 30193  cdlemg9 30091  ltrnco 30176  ltrncom 30195  tgrpabl 30208  trlco 30184
[Crawley] p. 116Definition of Gdf-tgrp 30200
[Crawley] p. 117Lemma Gcdlemg17 30134  cdlemg17b 30119
[Crawley] p. 117Definition of Edf-edring-rN 30213  df-edring 30214
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 30217
[Crawley] p. 118Remarktendopltp 30237
[Crawley] p. 118Lemma Hcdlemh 30274  cdlemh1 30272  cdlemh2 30273
[Crawley] p. 118Lemma Icdlemi 30277  cdlemi1 30275  cdlemi2 30276
[Crawley] p. 118Lemma Jcdlemj1 30278  cdlemj2 30279  cdlemj3 30280  tendocan 30281
[Crawley] p. 118Lemma Kcdlemk 30431  cdlemk1 30288  cdlemk10 30300  cdlemk11 30306  cdlemk11t 30403  cdlemk11ta 30386  cdlemk11tb 30388  cdlemk11tc 30402  cdlemk11u-2N 30346  cdlemk11u 30328  cdlemk12 30307  cdlemk12u-2N 30347  cdlemk12u 30329  cdlemk13-2N 30333  cdlemk13 30309  cdlemk14-2N 30335  cdlemk14 30311  cdlemk15-2N 30336  cdlemk15 30312  cdlemk16-2N 30337  cdlemk16 30314  cdlemk16a 30313  cdlemk17-2N 30338  cdlemk17 30315  cdlemk18-2N 30343  cdlemk18-3N 30357  cdlemk18 30325  cdlemk19-2N 30344  cdlemk19 30326  cdlemk19u 30427  cdlemk1u 30316  cdlemk2 30289  cdlemk20-2N 30349  cdlemk20 30331  cdlemk21-2N 30348  cdlemk21N 30330  cdlemk22-3 30358  cdlemk22 30350  cdlemk23-3 30359  cdlemk24-3 30360  cdlemk25-3 30361  cdlemk26-3 30363  cdlemk26b-3 30362  cdlemk27-3 30364  cdlemk28-3 30365  cdlemk29-3 30368  cdlemk3 30290  cdlemk30 30351  cdlemk31 30353  cdlemk32 30354  cdlemk33N 30366  cdlemk34 30367  cdlemk35 30369  cdlemk36 30370  cdlemk37 30371  cdlemk38 30372  cdlemk39 30373  cdlemk39u 30425  cdlemk4 30291  cdlemk41 30377  cdlemk42 30398  cdlemk42yN 30401  cdlemk43N 30420  cdlemk45 30404  cdlemk46 30405  cdlemk47 30406  cdlemk48 30407  cdlemk49 30408  cdlemk5 30293  cdlemk50 30409  cdlemk51 30410  cdlemk52 30411  cdlemk53 30414  cdlemk54 30415  cdlemk55 30418  cdlemk55u 30423  cdlemk56 30428  cdlemk5a 30292  cdlemk5auN 30317  cdlemk5u 30318  cdlemk6 30294  cdlemk6u 30319  cdlemk7 30305  cdlemk7u-2N 30345  cdlemk7u 30327  cdlemk8 30295  cdlemk9 30296  cdlemk9bN 30297  cdlemki 30298  cdlemkid 30393  cdlemkj-2N 30339  cdlemkj 30320  cdlemksat 30303  cdlemksel 30302  cdlemksv 30301  cdlemksv2 30304  cdlemkuat 30323  cdlemkuel-2N 30341  cdlemkuel-3 30355  cdlemkuel 30322  cdlemkuv-2N 30340  cdlemkuv2-2 30342  cdlemkuv2-3N 30356  cdlemkuv2 30324  cdlemkuvN 30321  cdlemkvcl 30299  cdlemky 30383  cdlemkyyN 30419  tendoex 30432
[Crawley] p. 120Remarkdva1dim 30442
[Crawley] p. 120Lemma Lcdleml1N 30433  cdleml2N 30434  cdleml3N 30435  cdleml4N 30436  cdleml5N 30437  cdleml6 30438  cdleml7 30439  cdleml8 30440  cdleml9 30441  dia1dim 30519
[Crawley] p. 120Lemma Mdia11N 30506  diaf11N 30507  dialss 30504  diaord 30505  dibf11N 30619  djajN 30595
[Crawley] p. 120Definition of isomorphism mapdiaval 30490
[Crawley] p. 121Lemma Mcdlemm10N 30576  dia2dimlem1 30522  dia2dimlem2 30523  dia2dimlem3 30524  dia2dimlem4 30525  dia2dimlem5 30526  diaf1oN 30588  diarnN 30587  dvheveccl 30570  dvhopN 30574
[Crawley] p. 121Lemma Ncdlemn 30670  cdlemn10 30664  cdlemn11 30669  cdlemn11a 30665  cdlemn11b 30666  cdlemn11c 30667  cdlemn11pre 30668  cdlemn2 30653  cdlemn2a 30654  cdlemn3 30655  cdlemn4 30656  cdlemn4a 30657  cdlemn5 30659  cdlemn5pre 30658  cdlemn6 30660  cdlemn7 30661  cdlemn8 30662  cdlemn9 30663  diclspsn 30652
[Crawley] p. 121Definition of phi(q)df-dic 30631
[Crawley] p. 122Lemma Ndih11 30723  dihf11 30725  dihjust 30675  dihjustlem 30674  dihord 30722  dihord1 30676  dihord10 30681  dihord11b 30680  dihord11c 30682  dihord2 30685  dihord2a 30677  dihord2b 30678  dihord2cN 30679  dihord2pre 30683  dihord2pre2 30684  dihordlem6 30671  dihordlem7 30672  dihordlem7b 30673
[Crawley] p. 122Definition of isomorphism mapdihffval 30688  dihfval 30689  dihval 30690
[Eisenberg] p. 67Definition 5.3df-dif 3157
[Eisenberg] p. 82Definition 6.3dfom3 7344
[Eisenberg] p. 125Definition 8.21df-map 6770
[Eisenberg] p. 216Example 13.2(4)omenps 7351
[Eisenberg] p. 310Theorem 19.8cardprc 7609
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 8173
[Enderton] p. 18Axiom of Empty Setaxnul 4150
[Enderton] p. 19Definitiondf-tp 3650
[Enderton] p. 26Exercise 5unissb 3859
[Enderton] p. 26Exercise 10pwel 4225
[Enderton] p. 28Exercise 7(b)pwun 4302
[Enderton] p. 30Theorem "Distributive laws"iinin1 3975  iinin2 3974  iinun2 3970  iunin1 3969  iunin2 3968
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3973  iundif2 3971
[Enderton] p. 32Exercise 20unineq 3421
[Enderton] p. 33Exercise 23iinuni 3987
[Enderton] p. 33Exercise 25iununi 3988
[Enderton] p. 33Exercise 24(a)iinpw 3992
[Enderton] p. 33Exercise 24(b)iunpw 4570  iunpwss 3993
[Enderton] p. 36Definitionopthwiener 4268
[Enderton] p. 38Exercise 6(a)unipw 4224
[Enderton] p. 38Exercise 6(b)pwuni 4206
[Enderton] p. 41Lemma 3Dopeluu 4526  rnex 4942  rnexg 4940
[Enderton] p. 41Exercise 8dmuni 4888  rnuni 5092
[Enderton] p. 42Definition of a functiondffun7 5247  dffun8 5248
[Enderton] p. 43Definition of function valuefunfv2 5549
[Enderton] p. 43Definition of single-rootedfuncnv 5276
[Enderton] p. 44Definition (d)dfima2 5014  dfima3 5015
[Enderton] p. 47Theorem 3Hfvco2 5556
[Enderton] p. 49Axiom of Choice (first form)ac7 8096  ac7g 8097  df-ac 7739  dfac2 7753  dfac2a 7752  dfac3 7744  dfac7 7754
[Enderton] p. 50Theorem 3K(a)imauni 5734
[Enderton] p. 52Definitiondf-map 6770
[Enderton] p. 53Exercise 21coass 5190
[Enderton] p. 53Exercise 27dmco 5180
[Enderton] p. 53Exercise 14(a)funin 5285
[Enderton] p. 53Exercise 22(a)imass2 5049
[Enderton] p. 54Remarkixpf 6834  ixpssmap 6846
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6814
[Enderton] p. 55Axiom of Choice (second form)ac9 8106  ac9s 8116
[Enderton] p. 56Theorem 3Merref 6676
[Enderton] p. 57Lemma 3Nerthi 6702
[Enderton] p. 57Definitiondf-ec 6658
[Enderton] p. 58Definitiondf-qs 6662
[Enderton] p. 60Theorem 3Qth3q 6763  th3qcor 6762  th3qlem1 6760  th3qlem2 6761
[Enderton] p. 61Exercise 35df-ec 6658
[Enderton] p. 65Exercise 56(a)dmun 4885
[Enderton] p. 68Definition of successordf-suc 4398
[Enderton] p. 71Definitiondf-tr 4116  dftr4 4120
[Enderton] p. 72Theorem 4Eunisuc 4468
[Enderton] p. 73Exercise 6unisuc 4468
[Enderton] p. 73Exercise 5(a)truni 4129
[Enderton] p. 73Exercise 5(b)trint 4130  trintALT 27926
[Enderton] p. 79Theorem 4I(A1)nna0 6598
[Enderton] p. 79Theorem 4I(A2)nnasuc 6600  onasuc 6523
[Enderton] p. 79Definition of operation valuedf-ov 5823
[Enderton] p. 80Theorem 4J(A1)nnm0 6599
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6601  onmsuc 6524
[Enderton] p. 81Theorem 4K(1)nnaass 6616
[Enderton] p. 81Theorem 4K(2)nna0r 6603  nnacom 6611
[Enderton] p. 81Theorem 4K(3)nndi 6617
[Enderton] p. 81Theorem 4K(4)nnmass 6618
[Enderton] p. 81Theorem 4K(5)nnmcom 6620
[Enderton] p. 82Exercise 16nnm0r 6604  nnmsucr 6619
[Enderton] p. 88Exercise 23nnaordex 6632
[Enderton] p. 129Definitiondf-en 6860
[Enderton] p. 132Theorem 6B(b)canth 6288
[Enderton] p. 133Exercise 1xpomen 7639
[Enderton] p. 133Exercise 2qnnen 12487
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7041
[Enderton] p. 135Corollary 6Cphp3 7043
[Enderton] p. 136Corollary 6Enneneq 7040
[Enderton] p. 136Corollary 6D(a)pssinf 7069
[Enderton] p. 136Corollary 6D(b)ominf 7071
[Enderton] p. 137Lemma 6Fpssnn 7077
[Enderton] p. 138Corollary 6Gssfi 7079
[Enderton] p. 139Theorem 6H(c)mapen 7021
[Enderton] p. 142Theorem 6I(3)xpcdaen 7805
[Enderton] p. 142Theorem 6I(4)mapcdaen 7806
[Enderton] p. 143Theorem 6Jcda0en 7801  cda1en 7797
[Enderton] p. 144Exercise 13iunfi 7140  unifi 7141  unifi2 7142
[Enderton] p. 144Corollary 6Kundif2 3532  unfi 7120  unfi2 7122
[Enderton] p. 145Figure 38ffoss 5471
[Enderton] p. 145Definitiondf-dom 6861
[Enderton] p. 146Example 1domen 6871  domeng 6872
[Enderton] p. 146Example 3nndomo 7050  nnsdom 7350  nnsdomg 7112
[Enderton] p. 149Theorem 6L(a)cdadom2 7809
[Enderton] p. 149Theorem 6L(c)mapdom1 7022  xpdom1 6957  xpdom1g 6955  xpdom2g 6954
[Enderton] p. 149Theorem 6L(d)mapdom2 7028
[Enderton] p. 151Theorem 6Mzorn 8130  zorng 8127
[Enderton] p. 151Theorem 6M(4)ac8 8115  dfac5 7751
[Enderton] p. 159Theorem 6Qunictb 8193
[Enderton] p. 164Exampleinfdif 7831
[Enderton] p. 168Definitiondf-po 4314
[Enderton] p. 192Theorem 7M(a)oneli 4500
[Enderton] p. 192Theorem 7M(b)ontr1 4438
[Enderton] p. 192Theorem 7M(c)onirri 4499
[Enderton] p. 193Corollary 7N(b)0elon 4445
[Enderton] p. 193Corollary 7N(c)onsuci 4629
[Enderton] p. 193Corollary 7N(d)ssonunii 4579
[Enderton] p. 194Remarkonprc 4576
[Enderton] p. 194Exercise 16suc11 4496
[Enderton] p. 197Definitiondf-card 7568
[Enderton] p. 197Theorem 7Pcarden 8169
[Enderton] p. 200Exercise 25tfis 4645
[Enderton] p. 202Lemma 7Tr1tr 7444
[Enderton] p. 202Definitiondf-r1 7432
[Enderton] p. 202Theorem 7Qr1val1 7454
[Enderton] p. 204Theorem 7V(b)rankval4 7535
[Enderton] p. 206Theorem 7X(b)en2lp 7313
[Enderton] p. 207Exercise 30rankpr 7525  rankprb 7519  rankpw 7511  rankpwi 7491  rankuniss 7534
[Enderton] p. 207Exercise 34opthreg 7315
[Enderton] p. 208Exercise 35suc11reg 7316
[Enderton] p. 212Definition of alephalephval3 7733
[Enderton] p. 213Theorem 8A(a)alephord2 7699
[Enderton] p. 213Theorem 8A(b)cardalephex 7713
[Enderton] p. 218Theorem Schema 8Eonfununi 6354
[Enderton] p. 222Definition of kardkarden 7561  kardex 7560
[Enderton] p. 238Theorem 8Roeoa 6591
[Enderton] p. 238Theorem 8Soeoe 6593
[Enderton] p. 240Exercise 25oarec 6556
[Enderton] p. 257Definition of cofinalitycflm 7872
[FaureFrolicher] p. 57Definition 3.1.9mreexd 13539
[FaureFrolicher] p. 83Definition 4.1.1df-mri 13485
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 14275  mrieqv2d 13536  mrieqvd 13535
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 13540
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 13545  mreexexlem2d 13542
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 14281  mreexfidimd 13547
[Fremlin5] p. 193Proposition 563Gbnulmbl2 18889
[Fremlin5] p. 213Lemma 565Cauniioovol 18929
[Fremlin5] p. 214Lemma 565Cauniioombl 18939
[FreydScedrov] p. 283Axiom of Infinityax-inf 7335  inf1 7319  inf2 7320
[Gleason] p. 117Proposition 9-2.1df-enq 8531  enqer 8541
[Gleason] p. 117Proposition 9-2.2df-1nq 8536  df-nq 8532
[Gleason] p. 117Proposition 9-2.3df-plpq 8528  df-plq 8534
[Gleason] p. 119Proposition 9-2.4caovmo 6019  df-mpq 8529  df-mq 8535
[Gleason] p. 119Proposition 9-2.5df-rq 8537
[Gleason] p. 119Proposition 9-2.6ltexnq 8595
[Gleason] p. 120Proposition 9-2.6(i)halfnq 8596  ltbtwnnq 8598
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 8591
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 8592
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 8599
[Gleason] p. 121Definition 9-3.1df-np 8601
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 8613
[Gleason] p. 121Definition 9-3.1(iii)prnmax 8615
[Gleason] p. 122Definitiondf-1p 8602
[Gleason] p. 122Remark (1)prub 8614
[Gleason] p. 122Lemma 9-3.4prlem934 8653
[Gleason] p. 122Proposition 9-3.2df-ltp 8605
[Gleason] p. 122Proposition 9-3.3ltsopr 8652  psslinpr 8651  supexpr 8674  suplem1pr 8672  suplem2pr 8673
[Gleason] p. 123Proposition 9-3.5addclpr 8638  addclprlem1 8636  addclprlem2 8637  df-plp 8603
[Gleason] p. 123Proposition 9-3.5(i)addasspr 8642
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 8641
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 8654
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 8663  ltexprlem1 8656  ltexprlem2 8657  ltexprlem3 8658  ltexprlem4 8659  ltexprlem5 8660  ltexprlem6 8661  ltexprlem7 8662
[Gleason] p. 123Proposition 9-3.5(v)ltapr 8665  ltaprlem 8664
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 8666
[Gleason] p. 124Lemma 9-3.6prlem936 8667
[Gleason] p. 124Proposition 9-3.7df-mp 8604  mulclpr 8640  mulclprlem 8639  reclem2pr 8668
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 8649
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 8644
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 8643
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 8648
[Gleason] p. 124Proposition 9-3.7(v)recexpr 8671  reclem3pr 8669  reclem4pr 8670
[Gleason] p. 126Proposition 9-4.1df-enr 8677  df-mpr 8676  df-plpr 8675  enrer 8686
[Gleason] p. 126Proposition 9-4.2df-0r 8682  df-1r 8683  df-nr 8678
[Gleason] p. 126Proposition 9-4.3df-mr 8680  df-plr 8679  negexsr 8720  recexsr 8725  recexsrlem 8721
[Gleason] p. 127Proposition 9-4.4df-ltr 8681
[Gleason] p. 130Proposition 10-1.3creui 9737  creur 9736  cru 9734
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 8806  axcnre 8782
[Gleason] p. 132Definition 10-3.1crim 11595  crimd 11712  crimi 11673  crre 11594  crred 11711  crrei 11672
[Gleason] p. 132Definition 10-3.2remim 11597  remimd 11678
[Gleason] p. 133Definition 10.36absval2 11764  absval2d 11922  absval2i 11875
[Gleason] p. 133Proposition 10-3.4(a)cjadd 11621  cjaddd 11700  cjaddi 11668
[Gleason] p. 133Proposition 10-3.4(c)cjmul 11622  cjmuld 11701  cjmuli 11669
[Gleason] p. 133Proposition 10-3.4(e)cjcj 11620  cjcjd 11679  cjcji 11651
[Gleason] p. 133Proposition 10-3.4(f)cjre 11619  cjreb 11603  cjrebd 11682  cjrebi 11654  cjred 11706  rere 11602  rereb 11600  rerebd 11681  rerebi 11653  rered 11704
[Gleason] p. 133Proposition 10-3.4(h)addcj 11628  addcjd 11692  addcji 11663
[Gleason] p. 133Proposition 10-3.7(a)absval 11718
[Gleason] p. 133Proposition 10-3.7(b)abscj 11759  abscjd 11927  abscji 11879
[Gleason] p. 133Proposition 10-3.7(c)abs00 11769  abs00d 11923  abs00i 11876  absne0d 11924
[Gleason] p. 133Proposition 10-3.7(d)releabs 11800  releabsd 11928  releabsi 11880
[Gleason] p. 133Proposition 10-3.7(f)absmul 11774  absmuld 11931  absmuli 11882
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11762  sqabsaddi 11883
[Gleason] p. 133Proposition 10-3.7(h)abstri 11809  abstrid 11933  abstrii 11886
[Gleason] p. 134Definition 10-4.1df-exp 11100  exp0 11103  expp1 11105  expp1d 11241
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 20021  cxpaddd 20059  expadd 11139  expaddd 11242  expaddz 11141
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 20030  cxpmuld 20076  expmul 11142  expmuld 11243  expmulz 11143
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 20027  mulcxpd 20070  mulexp 11136  mulexpd 11255  mulexpz 11137
[Gleason] p. 140Exercise 1znnen 12486
[Gleason] p. 141Definition 11-2.1fzval 10779
[Gleason] p. 168Proposition 12-2.1(a)climadd 12100  rlimadd 12111  rlimdiv 12114
[Gleason] p. 168Proposition 12-2.1(b)climsub 12102  rlimsub 12112
[Gleason] p. 168Proposition 12-2.1(c)climmul 12101  rlimmul 12113
[Gleason] p. 171Corollary 12-2.2climmulc2 12105
[Gleason] p. 172Corollary 12-2.5climrecl 12052
[Gleason] p. 172Proposition 12-2.4(c)climabs 12072  climcj 12073  climim 12075  climre 12074  rlimabs 12077  rlimcj 12078  rlimim 12080  rlimre 12079
[Gleason] p. 173Definition 12-3.1df-ltxr 8868  df-xr 8867  ltxr 10453
[Gleason] p. 175Definition 12-4.1df-limsup 11940  limsupval 11943
[Gleason] p. 180Theorem 12-5.1climsup 12138
[Gleason] p. 180Theorem 12-5.3caucvg 12146  caucvgb 12147  caucvgr 12143  climcau 12139
[Gleason] p. 182Exercise 3cvgcmp 12269
[Gleason] p. 182Exercise 4cvgrat 12334
[Gleason] p. 195Theorem 13-2.12abs1m 11814
[Gleason] p. 217Lemma 13-4.1btwnzge0 10948
[Gleason] p. 223Definition 14-1.1df-met 16369
[Gleason] p. 223Definition 14-1.1(a)met0 17903  xmet0 17902
[Gleason] p. 223Definition 14-1.1(b)metgt0 17918
[Gleason] p. 223Definition 14-1.1(c)metsym 17909
[Gleason] p. 223Definition 14-1.1(d)mettri 17911  mstri 18010  xmettri 17910  xmstri 18009
[Gleason] p. 225Definition 14-1.5xpsmet 17941
[Gleason] p. 230Proposition 14-2.6txlm 17337
[Gleason] p. 240Theorem 14-4.3metcnp4 18730
[Gleason] p. 240Proposition 14-4.2metcnp3 18081
[Gleason] p. 243Proposition 14-4.16addcn 18364  addcn2 12062  mulcn 18366  mulcn2 12064  subcn 18365  subcn2 12063
[Gleason] p. 295Remarkbcval3 11314  bcval4 11315
[Gleason] p. 295Equation 2bcpasc 11328
[Gleason] p. 295Definition of binomial coefficientbcval 11312  df-bc 11311
[Gleason] p. 296Remarkbcn0 11318  bcnn 11319
[Gleason] p. 296Theorem 15-2.8binom 12283
[Gleason] p. 308Equation 2ef0 12367
[Gleason] p. 308Equation 3efcj 12368
[Gleason] p. 309Corollary 15-4.3efne0 12372
[Gleason] p. 309Corollary 15-4.4efexp 12376
[Gleason] p. 310Equation 14sinadd 12439
[Gleason] p. 310Equation 15cosadd 12440
[Gleason] p. 311Equation 17sincossq 12451
[Gleason] p. 311Equation 18cosbnd 12456  sinbnd 12455
[Gleason] p. 311Lemma 15-4.7sqeqor 11212  sqeqori 11210
[Gleason] p. 311Definition of pidf-pi 12349
[Godowski] p. 730Equation SFgoeqi 22846
[GodowskiGreechie] p. 249Equation IV3oai 22240
[Gratzer] p. 23Section 0.6df-mre 13483
[Gratzer] p. 27Section 0.6df-mri 13485
[Halmos] p. 31Theorem 17.3riesz1 22638  riesz2 22639
[Halmos] p. 41Definition of Hermitianhmopadj2 22514
[Halmos] p. 42Definition of projector orderingpjordi 22746
[Halmos] p. 43Theorem 26.1elpjhmop 22758  elpjidm 22757  pjnmopi 22721
[Halmos] p. 44Remarkpjinormi 22259  pjinormii 22248
[Halmos] p. 44Theorem 26.2elpjch 22762  pjrn 22279  pjrni 22274  pjvec 22268
[Halmos] p. 44Theorem 26.3pjnorm2 22299
[Halmos] p. 44Theorem 26.4hmopidmpj 22727  hmopidmpji 22725
[Halmos] p. 45Theorem 27.1pjinvari 22764
[Halmos] p. 45Theorem 27.3pjoci 22753  pjocvec 22269
[Halmos] p. 45Theorem 27.4pjorthcoi 22742
[Halmos] p. 48Theorem 29.2pjssposi 22745
[Halmos] p. 48Theorem 29.3pjssdif1i 22748  pjssdif2i 22747
[Halmos] p. 50Definition of spectrumdf-spec 22428
[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 1534
[Hatcher] p. 25Definitiondf-phtpc 18485  df-phtpy 18464
[Hatcher] p. 26Definitiondf-pco 18498  df-pi1 18501
[Hatcher] p. 26Proposition 1.2phtpcer 18488
[Hatcher] p. 26Proposition 1.3pi1grp 18543
[Herstein] p. 54Exercise 28df-grpo 20851
[Herstein] p. 55Lemma 2.2.1(a)grpideu 14493  grpoideu 20869  mndideu 14370
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 14511  grpoinveu 20882
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 14530  grpo2inv 20899
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 14539  grpoinvop 20901
[Herstein] p. 57Exercise 1isgrp2d 20895  isgrp2i 20896
[Hitchcock] p. 5Rule A3mpto1 1524
[Hitchcock] p. 5Rule A4mpto2 1525
[Hitchcock] p. 5Rule A5mtp-xor 1526
[Holland] p. 1519Theorem 2sumdmdi 22993
[Holland] p. 1520Lemma 5cdj1i 23006  cdj3i 23014  cdj3lem1 23007  cdjreui 23005
[Holland] p. 1524Lemma 7mddmdin0i 23004
[Holland95] p. 13Theorem 3.6hlathil 31422
[Holland95] p. 14Line 15hgmapvs 31352
[Holland95] p. 14Line 16hdmaplkr 31374
[Holland95] p. 14Line 17hdmapellkr 31375
[Holland95] p. 14Line 19hdmapglnm2 31372
[Holland95] p. 14Line 20hdmapip0com 31378
[Holland95] p. 14Theorem 3.6hdmapevec2 31297
[Holland95] p. 14Lines 24 and 25hdmapoc 31392
[Holland95] p. 204Definition of involutiondf-srng 15606
[Holland95] p. 212Definition of subspacedf-psubsp 28960
[Holland95] p. 214Lemma 3.3lclkrlem2v 30986
[Holland95] p. 214Definition 3.2df-lpolN 30939
[Holland95] p. 214Definition of nonsingularpnonsingN 29390
[Holland95] p. 215Lemma 3.3(1)dihoml4 30835  poml4N 29410
[Holland95] p. 215Lemma 3.3(2)dochexmid 30926  pexmidALTN 29435  pexmidN 29426
[Holland95] p. 218Theorem 3.6lclkr 30991
[Holland95] p. 218Definition of dual vector spacedf-ldual 28582  ldualset 28583
[Holland95] p. 222Item 1df-lines 28958  df-pointsN 28959
[Holland95] p. 222Item 2df-polarityN 29360
[Holland95] p. 223Remarkispsubcl2N 29404  omllaw4 28704  pol1N 29367  polcon3N 29374
[Holland95] p. 223Definitiondf-psubclN 29392
[Holland95] p. 223Equation for polaritypolval2N 29363
[Hughes] p. 44Equation 1.21bax-his3 21656
[Hughes] p. 47Definition of projection operatordfpjop 22755
[Hughes] p. 49Equation 1.30eighmre 22536  eigre 22408  eigrei 22407
[Hughes] p. 49Equation 1.31eighmorth 22537  eigorth 22411  eigorthi 22410
[Hughes] p. 137Remark (ii)eigposi 22409
[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 1623  cvjust 2280
[Jech] p. 42Lemma 6.1alephexp1 8197
[Jech] p. 42Equation 6.1alephadd 8195  alephmul 8196
[Jech] p. 43Lemma 6.2infmap 8194  infmap2 7840
[Jech] p. 71Lemma 9.3jech9.3 7482
[Jech] p. 72Equation 9.3scott0 7552  scottex 7551
[Jech] p. 72Exercise 9.1rankval4 7535
[Jech] p. 72Scheme "Collection Principle"cp 7557
[Jech] p. 78Definition implied by the footnoteopthprc 4736
[JonesMatijasevic] p. 694Definition 2.3rmxyval 26400
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 26496
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 26497
[JonesMatijasevic] p. 695Equation 2.7rmxadd 26412
[JonesMatijasevic] p. 695Equation 2.8rmyadd 26416
[JonesMatijasevic] p. 695Equation 2.9rmxp1 26417  rmyp1 26418
[JonesMatijasevic] p. 695Equation 2.10rmxm1 26419  rmym1 26420
[JonesMatijasevic] p. 695Equation 2.11rmx0 26410  rmx1 26411  rmxluc 26421
[JonesMatijasevic] p. 695Equation 2.12rmy0 26414  rmy1 26415  rmyluc 26422
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 26424
[JonesMatijasevic] p. 695Equation 2.14rmydbl 26425
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 26447  jm2.17b 26448  jm2.17c 26449
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 26486
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 26490
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 26481
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 26450  jm2.24nn 26446
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 26495
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 26501  rmygeid 26451
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 26513
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1637
[KalishMontague] p. 85Lemma 2equid 1646
[KalishMontague] p. 85Lemma 3equcomi 1647
[KalishMontague] p. 86Lemma 7cbvalivw 1644  cbvaliw 1643
[KalishMontague] p. 87Lemma 8spimvw 1641  spimw 1640
[KalishMontague] p. 87Lemma 9spfw 1658  spw 1661
[Kalmbach] p. 14Definition of latticechabs1 22088  chabs1i 22090  chabs2 22089  chabs2i 22091  chjass 22105  chjassi 22058  latabs1 14188  latabs2 14189
[Kalmbach] p. 15Definition of atomdf-at 22911  ela 22912
[Kalmbach] p. 15Definition of coverscvbr2 22856  cvrval2 28732
[Kalmbach] p. 16Definitiondf-ol 28636  df-oml 28637
[Kalmbach] p. 20Definition of commutescmbr 22156  cmbri 22162  cmtvalN 28669  df-cm 22155  df-cmtN 28635
[Kalmbach] p. 22Remarkomllaw5N 28705  pjoml5 22185  pjoml5i 22160
[Kalmbach] p. 22Definitionpjoml2 22183  pjoml2i 22157
[Kalmbach] p. 22Theorem 2(v)cmcm 22186  cmcmi 22164  cmcmii 22169  cmtcomN 28707
[Kalmbach] p. 22Theorem 2(ii)omllaw3 28703  omlsi 21976  pjoml 22008  pjomli 22007
[Kalmbach] p. 22Definition of OML lawomllaw2N 28702
[Kalmbach] p. 23Remarkcmbr2i 22168  cmcm3 22187  cmcm3i 22166  cmcm3ii 22171  cmcm4i 22167  cmt3N 28709  cmt4N 28710  cmtbr2N 28711
[Kalmbach] p. 23Lemma 3cmbr3 22180  cmbr3i 22172  cmtbr3N 28712
[Kalmbach] p. 25Theorem 5fh1 22190  fh1i 22193  fh2 22191  fh2i 22194  omlfh1N 28716
[Kalmbach] p. 65Remarkchjatom 22930  chslej 22070  chsleji 22030  shslej 21952  shsleji 21942
[Kalmbach] p. 65Proposition 1chocin 22067  chocini 22026  chsupcl 21912  chsupval2 21982  h0elch 21827  helch 21816  hsupval2 21981  ocin 21868  ococss 21865  shococss 21866
[Kalmbach] p. 65Definition of subspace sumshsval 21884
[Kalmbach] p. 66Remarkdf-pjh 21967  pjssmi 22738  pjssmii 22253
[Kalmbach] p. 67Lemma 3osum 22217  osumi 22214
[Kalmbach] p. 67Lemma 4pjci 22773
[Kalmbach] p. 103Exercise 6atmd2 22973
[Kalmbach] p. 103Exercise 12mdsl0 22883
[Kalmbach] p. 140Remarkhatomic 22933  hatomici 22932  hatomistici 22935
[Kalmbach] p. 140Proposition 1atlatmstc 28777
[Kalmbach] p. 140Proposition 1(i)atexch 22954  lsatexch 28501
[Kalmbach] p. 140Proposition 1(ii)chcv1 22928  cvlcvr1 28797  cvr1 28867
[Kalmbach] p. 140Proposition 1(iii)cvexch 22947  cvexchi 22942  cvrexch 28877
[Kalmbach] p. 149Remark 2chrelati 22937  hlrelat 28859  hlrelat5N 28858  lrelat 28472
[Kalmbach] p. 153Exercise 5lsmcv 15889  lsmsatcv 28468  spansncv 22225  spansncvi 22224
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 28487  spansncv2 22866
[Kalmbach] p. 266Definitiondf-st 22784
[Kalmbach2] p. 8Definition of adjointdf-adjh 22422
[KanamoriPincus] p. 415Theorem 1.1fpwwe 8264  fpwwe2 8261
[KanamoriPincus] p. 416Corollary 1.3canth4 8265
[KanamoriPincus] p. 417Corollary 1.6canthp1 8272
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 8267
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 8269
[KanamoriPincus] p. 418Proposition 1.7pwfseq 8282
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 8286  gchxpidm 8287
[KanamoriPincus] p. 419Theorem 2.1gchacg 8290  gchhar 8289
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 7838  unxpwdom 7299
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 8292
[Kreyszig] p. 3Property M1metcl 17892  xmetcl 17891
[Kreyszig] p. 4Property M2meteq0 17899
[Kreyszig] p. 8Definition 1.1-8dscmet 18090
[Kreyszig] p. 12Equation 5conjmul 9473  muleqadd 9408
[Kreyszig] p. 18Definition 1.3-2mopnval 17979
[Kreyszig] p. 19Remarkmopntopon 17980
[Kreyszig] p. 19Theorem T1mopn0 18039  mopnm 17985
[Kreyszig] p. 19Theorem T2unimopn 18037
[Kreyszig] p. 19Definition of neighborhoodneibl 18042
[Kreyszig] p. 20Definition 1.3-3metcnp2 18083
[Kreyszig] p. 25Definition 1.4-1lmbr 16983  lmmbr 18679  lmmbr2 18680
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 17103
[Kreyszig] p. 28Theorem 1.4-5lmcau 18733
[Kreyszig] p. 28Definition 1.4-3iscau 18697  iscmet2 18715
[Kreyszig] p. 30Theorem 1.4-7cmetss 18735
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 17182  metelcls 18725
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 18726  metcld2 18727
[Kreyszig] p. 51Equation 2clmvneg1 18584  lmodvneg1 15662  nvinv 21190  vcm 21120
[Kreyszig] p. 51Equation 1aclm0vs 18583  lmod0vs 15658  vc0 21118
[Kreyszig] p. 51Equation 1blmodvs0 15659  vcz 21119
[Kreyszig] p. 58Definition 2.2-1imsmet 21253
[Kreyszig] p. 59Equation 1imsdval 21248  imsdval2 21249
[Kreyszig] p. 63Problem 1nvnd 21250
[Kreyszig] p. 64Problem 2nvge0 21233  nvz 21228
[Kreyszig] p. 64Problem 3nvabs 21232
[Kreyszig] p. 91Definition 2.7-1isblo3i 21372
[Kreyszig] p. 92Equation 2df-nmoo 21316
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 21378  blocni 21376
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 21377
[Kreyszig] p. 129Definition 3.1-1cphipeq0 18634  ipeq0 16537  ipz 21288
[Kreyszig] p. 135Problem 2pythi 21421
[Kreyszig] p. 137Lemma 3-2.1(a)sii 21425
[Kreyszig] p. 144Equation 4supcvg 12309
[Kreyszig] p. 144Theorem 3.3-1minvec 18795  minveco 21456
[Kreyszig] p. 196Definition 3.9-1df-aj 21321
[Kreyszig] p. 247Theorem 4.7-2bcth 18746
[Kreyszig] p. 249Theorem 4.7-3ubth 21445
[Kreyszig] p. 470Definition of positive operator orderingleop 22696  leopg 22695
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 22714
[Kreyszig] p. 525Theorem 10.1-1htth 21491
[Kunen] p. 10Axiom 0a9e 1893  axnul 4150
[Kunen] p. 11Axiom 3axnul 4150
[Kunen] p. 12Axiom 6zfrep6 5710
[Kunen] p. 24Definition 10.24mapval 6780  mapvalg 6778
[Kunen] p. 30Lemma 10.20fodom 8145
[Kunen] p. 31Definition 10.24mapex 6774
[Kunen] p. 95Definition 2.1df-r1 7432
[Kunen] p. 97Lemma 2.10r1elss 7474  r1elssi 7473
[Kunen] p. 107Exercise 4rankop 7526  rankopb 7520  rankuni 7531  rankxplim 7545  rankxpsuc 7548
[KuratowskiMostowski] p. 109Section. Eq. 14 iniuniin 3917
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 26951
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 26946
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 26952
[LeBlanc] p. 277Rule R2axnul 4150
[Levy] p. 338Axiomdf-clab 2272  df-clel 2281  df-cleq 2278
[Levy58] p. 2Definition Iisfin1-3 8008
[Levy58] p. 2Definition IIdf-fin2 7908
[Levy58] p. 2Definition Iadf-fin1a 7907
[Levy58] p. 2Definition IIIdf-fin3 7910
[Levy58] p. 3Definition Vdf-fin5 7911
[Levy58] p. 3Definition IVdf-fin4 7909
[Levy58] p. 4Definition VIdf-fin6 7912
[Levy58] p. 4Definition VIIdf-fin7 7913
[Levy58], p. 3Theorem 1fin1a2 8037
[Lopez-Astorga] p. 12Rule 1mpto1 1524
[Lopez-Astorga] p. 12Rule 2mpto2 1525
[Lopez-Astorga] p. 12Rule 3mtp-xor 1526
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 22981
[Maeda] p. 168Lemma 5mdsym 22985  mdsymi 22984
[Maeda] p. 168Lemma 4(i)mdsymlem4 22979  mdsymlem6 22981  mdsymlem7 22982
[Maeda] p. 168Lemma 4(ii)mdsymlem8 22983
[MaedaMaeda] p. 1Remarkssdmd1 22886  ssdmd2 22887  ssmd1 22884  ssmd2 22885
[MaedaMaeda] p. 1Lemma 1.2mddmd2 22882
[MaedaMaeda] p. 1Definition 1.1df-dmd 22854  df-md 22853  mdbr 22867
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 22904  mdslj1i 22892  mdslj2i 22893  mdslle1i 22890  mdslle2i 22891  mdslmd1i 22902  mdslmd2i 22903
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 22894  mdsl2bi 22896  mdsl2i 22895
[MaedaMaeda] p. 2Lemma 1.6mdexchi 22908
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 22905
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 22906
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 22883
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 22888  mdsl3 22889
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 22907
[MaedaMaeda] p. 4Theorem 1.14mdcompli 23002
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 28779  hlrelat1 28857
[MaedaMaeda] p. 31Lemma 7.5lcvexch 28497
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 22909  cvmdi 22897  cvnbtwn4 22862  cvrnbtwn4 28737
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 22910
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 28798  cvp 22948  cvrp 28873  lcvp 28498
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 22972
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 22971
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 28791  hlexch4N 28849
[MaedaMaeda] p. 34Exercise 7.1atabsi 22974
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 28900
[MaedaMaeda] p. 61Definition 15.10psubN 29206  atpsubN 29210  df-pointsN 28959  pointpsubN 29208
[MaedaMaeda] p. 62Theorem 15.5df-pmap 28961  pmap11 29219  pmaple 29218  pmapsub 29225  pmapval 29214
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 29222  pmap1N 29224
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 29227  pmapglb2N 29228  pmapglb2xN 29229  pmapglbx 29226
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 29309
[MaedaMaeda] p. 67Postulate PS1ps-1 28934
[MaedaMaeda] p. 68Lemma 16.2df-padd 29253  paddclN 29299  paddidm 29298
[MaedaMaeda] p. 68Condition PS2ps-2 28935
[MaedaMaeda] p. 68Equation 16.2.1paddass 29295
[MaedaMaeda] p. 69Lemma 16.4ps-1 28934
[MaedaMaeda] p. 69Theorem 16.4ps-2 28935
[MaedaMaeda] p. 70Theorem 16.9lsmmod 14979  lsmmod2 14980  lssats 28470  shatomici 22931  shatomistici 22934  shmodi 21962  shmodsi 21961
[MaedaMaeda] p. 130Remark 29.6dmdmd 22873  mdsymlem7 22982
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 22161
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 22065
[MaedaMaeda] p. 139Remarksumdmdii 22988
[Margaris] p. 40Rule Cexlimiv 1667
[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 1530  df-or 361  dfbi2 611
[Margaris] p. 51Theorem 1id1 22
[Margaris] p. 56Theorem 3syld 42
[Margaris] p. 59Section 14notnot2ALTVD 27960
[Margaris] p. 60Theorem 8mth8 140
[Margaris] p. 60Section 14con3ALTVD 27961
[Margaris] p. 79Rule Cexinst01 27666  exinst11 27667
[Margaris] p. 89Theorem 19.219.2 1672  19.2g 1782  r19.2z 3545
[Margaris] p. 89Theorem 19.319.3 1783  19.3v 1663  rr19.3v 2911
[Margaris] p. 89Theorem 19.5alcom 1712
[Margaris] p. 89Theorem 19.6alex 1560
[Margaris] p. 89Theorem 19.7alnex 1531
[Margaris] p. 89Theorem 19.819.8a 1720
[Margaris] p. 89Theorem 19.919.9 1785  19.9h 1729  19.9v 1664
[Margaris] p. 89Theorem 19.11excom 1788  excomim 1787
[Margaris] p. 89Theorem 19.1219.12 1736  r19.12 2658
[Margaris] p. 90Theorem 19.14exnal 1562
[Margaris] p. 90Theorem 19.152albi 26976  albi 1552  ralbi 2681
[Margaris] p. 90Theorem 19.1619.16 1789
[Margaris] p. 90Theorem 19.1719.17 1790
[Margaris] p. 90Theorem 19.182exbi 26978  exbi 1569
[Margaris] p. 90Theorem 19.1919.19 1791
[Margaris] p. 90Theorem 19.202alim 26975  alim 1546  alimd 1746  alimdh 1551  alimdv 1608  ralimdaa 2622  ralimdv 2624  ralimdva 2623  sbcimdv 3054
[Margaris] p. 90Theorem 19.2119.21-2 1794  19.21 1793  19.21bi 1796  19.21h 1733  19.21t 1792  19.21v 1833  19.21vv 26974  alrimd 1751  alrimdd 1750  alrimdh 1575  alrimdv 1620  alrimi 1747  alrimih 1553  alrimiv 1618  alrimivv 1619  r19.21 2631  r19.21be 2646  r19.21bi 2643  r19.21t 2630  r19.21v 2632  ralrimd 2633  ralrimdv 2634  ralrimdva 2635  ralrimdvv 2639  ralrimdvva 2640  ralrimi 2626  ralrimiv 2627  ralrimiva 2628  ralrimivv 2636  ralrimivva 2637  ralrimivvva 2638  ralrimivw 2629  rexlimi 2662
[Margaris] p. 90Theorem 19.222alimdv 1610  2exim 26977  2eximdv 1611  exim 1563  eximd 1752  eximdh 1576  eximdv 1609  rexim 2649  reximdai 2653  reximddv 23021  reximdv 2656  reximdv2 2654  reximdva 2657  reximdvai 2655  reximi2 2651
[Margaris] p. 90Theorem 19.2319.23 1799  19.23bi 1804  19.23h 1730  19.23t 1798  19.23v 1834  19.23vv 1835  exlimd 1805  exlimdh 1806  exlimdv 1665  exlimdvv 1669  exlimexi 27559  exlimi 1803  exlimih 1731  exlimiv 1667  exlimivv 1668  r19.23 2660  r19.23v 2661  rexlimd 2666  rexlimdv 2668  rexlimdv3a 2671  rexlimdva 2669  rexlimdvaa 2670  rexlimdvv 2675  rexlimdvva 2676  rexlimdvw 2672  rexlimiv 2663  rexlimiva 2664  rexlimivv 2674
[Margaris] p. 90Theorem 19.2419.24 1674
[Margaris] p. 90Theorem 19.2519.25 1591
[Margaris] p. 90Theorem 19.2619.26-2 1582  19.26-3an 1583  19.26 1581  r19.26-2 2678  r19.26-2a 24333  r19.26-3 2679  r19.26 2677  r19.26m 2680
[Margaris] p. 90Theorem 19.2719.27 1807  19.27v 1837  r19.27av 2683  r19.27z 3554  r19.27zv 3555
[Margaris] p. 90Theorem 19.2819.28 1808  19.28v 1838  19.28vv 26984  r19.28av 2684  r19.28z 3548  r19.28zv 3551  rr19.28v 2912
[Margaris] p. 90Theorem 19.2919.29 1584  19.29r 1585  19.29r2 1586  19.29x 1587  r19.29 2685  r19.29r 2686
[Margaris] p. 90Theorem 19.3019.30 1592  r19.30 2687
[Margaris] p. 90Theorem 19.3119.31 1814  19.31vv 26982
[Margaris] p. 90Theorem 19.3219.32 1813  r19.32 27325  r19.32v 2688
[Margaris] p. 90Theorem 19.3319.33-2 26980  19.33 1595  19.33b 1596
[Margaris] p. 90Theorem 19.3419.34 1675
[Margaris] p. 90Theorem 19.3519.35 1588  19.35i 1589  19.35ri 1590  r19.35 2689
[Margaris] p. 90Theorem 19.3619.36 1809  19.36aiv 1840  19.36i 1810  19.36v 1839  19.36vv 26981  r19.36av 2690  r19.36zv 3556
[Margaris] p. 90Theorem 19.3719.37 1811  19.37aiv 1843  19.37v 1842  19.37vv 26983  r19.37 2691  r19.37av 2692  r19.37zv 3552
[Margaris] p. 90Theorem 19.3819.38 1812
[Margaris] p. 90Theorem 19.3919.39 1673
[Margaris] p. 90Theorem 19.4019.40-2 1598  19.40 1597  r19.40 2693
[Margaris] p. 90Theorem 19.4119.41 1817  19.41rg 27588  19.41v 1844  19.41vv 1845  19.41vvv 1846  19.41vvvv 1847  r19.41 2694  r19.41v 2695
[Margaris] p. 90Theorem 19.4219.42 1818  19.42v 1848  19.42vv 1850  19.42vvv 1851  r19.42v 2696
[Margaris] p. 90Theorem 19.4319.43 1593  r19.43 2697
[Margaris] p. 90Theorem 19.4419.44 1815  r19.44av 2698
[Margaris] p. 90Theorem 19.4519.45 1816  r19.45av 2699  r19.45zv 3553
[Margaris] p. 110Exercise 2(b)eu1 2166
[Mayet] p. 370Remarkjpi 22843  largei 22840  stri 22830
[Mayet3] p. 9Definition of CH-statesdf-hst 22785  ishst 22787
[Mayet3] p. 10Theoremhstrbi 22839  hstri 22838
[Mayet3] p. 1223Theorem 4.1mayete3i 22300
[Mayet3] p. 1240Theorem 7.1mayetes3i 22302
[MegPav2000] p. 2344Theorem 3.3stcltrthi 22851
[MegPav2000] p. 2345Definition 3.4-1chintcl 21904  chsupcl 21912
[MegPav2000] p. 2345Definition 3.4-2hatomic 22933
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 22927
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 22954
[MegPav2000] p. 2366Figure 7pl42N 29440
[MegPav2002] p. 362Lemma 2.2latj31 14200  latj32 14198  latjass 14196
[Megill] p. 444Axiom C5ax-17 1604  ax17o 2099
[Megill] p. 444Section 7conventions 3
[Megill] p. 445Lemma L12alequcom-o 2093  alequcom 1888  ax-10 2083
[Megill] p. 446Lemma L17equtrr 1654
[Megill] p. 446Lemma L18ax9from9o 2090
[Megill] p. 446Lemma L19hbnae-o 2121  hbnae 1898
[Megill] p. 447Remark 9.1df-sb 1632  sbid 1865  sbidd-misc 27450  sbidd 27449
[Megill] p. 448Remark 9.6ax15 1967
[Megill] p. 448Scheme C4'ax-5o 2079
[Megill] p. 448Scheme C5'ax-4 2078  sp 1717
[Megill] p. 448Scheme C6'ax-7 1709
[Megill] p. 448Scheme C7'ax-6o 2080
[Megill] p. 448Scheme C8'ax-8 1645
[Megill] p. 448Scheme C9'ax-12o 2085
[Megill] p. 448Scheme C10'ax-9 1637  ax-9o 2081
[Megill] p. 448Scheme C11'ax-10o 2082
[Megill] p. 448Scheme C12'ax-13 1687
[Megill] p. 448Scheme C13'ax-14 1689
[Megill] p. 448Scheme C14'ax-15 2086
[Megill] p. 448Scheme C15'ax-11o 2084
[Megill] p. 448Scheme C16'ax-16 2087
[Megill] p. 448Theorem 9.4dral1-o 2096  dral1 1908  dral2-o 2123  dral2 1909  drex1 1910  drex2 1911  drsb1 1968  drsb2 2001
[Megill] p. 448Theorem 9.7conventions 3
[Megill] p. 449Theorem 9.7sbcom2 2057  sbequ 2000  sbid2v 2066
[Megill] p. 450Example in Appendixhba1-o 2091  hba1 1721
[Mendelson] p. 35Axiom A3hirstL-ax3 27240
[Mendelson] p. 36Lemma 1.8id1 22
[Mendelson] p. 69Axiom 4rspsbc 3071  rspsbca 3072  stdpc4 1970
[Mendelson] p. 69Axiom 5ax-5o 2079  ra5 3077  stdpc5 1795
[Mendelson] p. 81Rule Cexlimiv 1667
[Mendelson] p. 95Axiom 6stdpc6 1651
[Mendelson] p. 95Axiom 7stdpc7 1860
[Mendelson] p. 225Axiom system NBGru 2992
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4268
[Mendelson] p. 231Exercise 4.10(k)inv1 3483
[Mendelson] p. 231Exercise 4.10(l)unv 3484
[Mendelson] p. 231Exercise 4.10(n)dfin3 3410
[Mendelson] p. 231Exercise 4.10(o)df-nul 3458
[Mendelson] p. 231Exercise 4.10(q)dfin4 3411
[Mendelson] p. 231Exercise 4.10(s)ddif 3310
[Mendelson] p. 231Definition of uniondfun3 3409
[Mendelson] p. 235Exercise 4.12(c)univ 4565
[Mendelson] p. 235Exercise 4.12(d)pwv 3828
[Mendelson] p. 235Exercise 4.12(j)pwin 4297
[Mendelson] p. 235Exercise 4.12(k)pwunss 4298
[Mendelson] p. 235Exercise 4.12(l)pwssun 4299
[Mendelson] p. 235Exercise 4.12(n)uniin 3849
[Mendelson] p. 235Exercise 4.12(p)reli 4813
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5192
[Mendelson] p. 244Proposition 4.8(g)epweon 4575
[Mendelson] p. 246Definition of successordf-suc 4398
[Mendelson] p. 250Exercise 4.36oelim2 6589
[Mendelson] p. 254Proposition 4.22(b)xpen 7020
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6942  xpsneng 6943
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6949  xpcomeng 6950
[Mendelson] p. 254Proposition 4.22(e)xpassen 6952
[Mendelson] p. 255Definitionbrsdom 6880
[Mendelson] p. 255Exercise 4.39endisj 6945
[Mendelson] p. 255Exercise 4.41mapprc 6772
[Mendelson] p. 255Exercise 4.43mapsnen 6934
[Mendelson] p. 255Exercise 4.45mapunen 7026
[Mendelson] p. 255Exercise 4.47xpmapen 7025
[Mendelson] p. 255Exercise 4.42(a)map0e 6801
[Mendelson] p. 255Exercise 4.42(b)map1 6935
[Mendelson] p. 257Proposition 4.24(a)undom 6946
[Mendelson] p. 258Exercise 4.56(b)cdaen 7795
[Mendelson] p. 258Exercise 4.56(c)cdaassen 7804  cdacomen 7803
[Mendelson] p. 258Exercise 4.56(f)cdadom1 7808
[Mendelson] p. 258Exercise 4.56(g)xp2cda 7802
[Mendelson] p. 258Definition of cardinal sumcdaval 7792  df-cda 7790
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6526
[Mendelson] p. 266Proposition 4.34(f)oaordex 6552
[Mendelson] p. 275Proposition 4.42(d)entri3 8177
[Mendelson] p. 281Definitiondf-r1 7432
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 7481
[Mendelson] p. 287Axiom system MKru 2992
[Mittelstaedt] p. 9Definitiondf-oc 21824
[Monk1] p. 22Remarkconventions 3
[Monk1] p. 22Theorem 3.1conventions 3
[Monk1] p. 26Theorem 2.8(vii)ssin 3393
[Monk1] p. 33Theorem 3.2(i)ssrel 4776
[Monk1] p. 33Theorem 3.2(ii)eqrel 4777
[Monk1] p. 34Definition 3.3df-opab 4080
[Monk1] p. 36Theorem 3.7(i)coi1 5187  coi2 5188
[Monk1] p. 36Theorem 3.8(v)dm0 4892  rn0 4936
[Monk1] p. 36Theorem 3.7(ii)cnvi 5085
[Monk1] p. 37Theorem 3.13(i)relxp 4794
[Monk1] p. 37Theorem 3.13(x)dmxp 4897  rnxp 5106
[Monk1] p. 37Theorem 3.13(ii)xp0 5098  xp0r 4768
[Monk1] p. 38Theorem 3.16(ii)ima0 5030
[Monk1] p. 38Theorem 3.16(viii)imai 5027
[Monk1] p. 39Theorem 3.17imaexg 5026
[Monk1] p. 39Theorem 3.16(xi)imassrn 5025
[Monk1] p. 41Theorem 4.3(i)fnopfv 5622  funfvop 5599
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5528
[Monk1] p. 42Theorem 4.4(iii)fvelima 5536
[Monk1] p. 43Theorem 4.6funun 5262
[Monk1] p. 43Theorem 4.8(iv)dff13 5745  dff13f 5746
[Monk1] p. 46Theorem 4.15(v)funex 5705  funrnex 5709
[Monk1] p. 50Definition 5.4fniunfv 5735
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5155
[Monk1] p. 52Theorem 5.11(viii)ssint 3880
[Monk1] p. 52Definition 5.13 (i)1stval2 6099  df-1st 6084
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6100  df-2nd 6085
[Monk1] p. 112Theorem 15.17(v)ranksn 7522  ranksnb 7495
[Monk1] p. 112Theorem 15.17(iv)rankuni2 7523
[Monk1] p. 112Theorem 15.17(iii)rankun 7524  rankunb 7518
[Monk1] p. 113Theorem 15.18r1val3 7506
[Monk1] p. 113Definition 15.19df-r1 7432  r1val2 7505
[Monk1] p. 117Lemmazorn2 8129  zorn2g 8126
[Monk1] p. 133Theorem 18.11cardom 7615
[Monk1] p. 133Theorem 18.12canth3 8179
[Monk1] p. 133Theorem 18.14carduni 7610
[Monk2] p. 105Axiom C4ax-5 1545
[Monk2] p. 105Axiom C7ax-8 1645
[Monk2] p. 105Axiom C8ax-11 1716  ax-11o 2084
[Monk2] p. 105Axiom (C8)ax11v 2037
[Monk2] p. 108Lemma 5ax-5o 2079
[Monk2] p. 109Lemma 12ax-7 1709
[Monk2] p. 109Lemma 15equvin 1947  equvini 1930  eqvinop 4251
[Monk2] p. 113Axiom C5-1ax-17 1604  ax17o 2099
[Monk2] p. 113Axiom C5-2ax-6 1704
[Monk2] p. 113Axiom C5-3ax-7 1709
[Monk2] p. 114Lemma 21sp 1717
[Monk2] p. 114Lemma 22ax5o 1719  hba1-o 2091  hba1 1721
[Monk2] p. 114Lemma 23nfia1 1780
[Monk2] p. 114Lemma 24nfa2 1779  nfra2 2599
[Moore] p. 53Part Idf-mre 13483
[Munkres] p. 77Example 2distop 16728  indistop 16734  indistopon 16733
[Munkres] p. 77Example 3fctop 16736  fctop2 16737
[Munkres] p. 77Example 4cctop 16738
[Munkres] p. 78Definition of basisdf-bases 16633  isbasis3g 16682
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 13339  tgval2 16689
[Munkres] p. 79Remarktgcl 16702
[Munkres] p. 80Lemma 2.1tgval3 16696
[Munkres] p. 80Lemma 2.2tgss2 16720  tgss3 16719
[Munkres] p. 81Lemma 2.3basgen 16721  basgen2 16722
[Munkres] p. 89Definition of subspace topologyresttop 16886
[Munkres] p. 93Theorem 6.1(1)0cld 16770  topcld 16767
[Munkres] p. 93Theorem 6.1(2)iincld 16771
[Munkres] p. 93Theorem 6.1(3)uncld 16773
[Munkres] p. 94Definition of closureclsval 16769
[Munkres] p. 94Definition of interiorntrval 16768
[Munkres] p. 95Theorem 6.5(a)clsndisj 16807  elcls 16805
[Munkres] p. 95Theorem 6.5(b)elcls3 16815
[Munkres] p. 97Theorem 6.6clslp 16874  neindisj 16849
[Munkres] p. 97Corollary 6.7cldlp 16876
[Munkres] p. 97Definition of limit pointislp2 16872  lpval 16866
[Munkres] p. 98Definition of Hausdorff spacedf-haus 17038
[Munkres] p. 102Definition of continuous functiondf-cn 16952  iscn 16960  iscn2 16963
[Munkres] p. 107Theorem 7.2(g)cncnp 17004  cncnp2 17005  cncnpi 17002  df-cnp 16953  iscnp 16962  iscnp2 16964
[Munkres] p. 127Theorem 10.1metcn 18084
[Munkres] p. 128Theorem 10.3metcn4 18731
[NielsenChuang] p. 195Equation 4.73unierri 22677
[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 18632  df-dip 21267  dip0l 21287  ip0l 16535
[Ponnusamy] p. 361Equation 6.45ipval 21269
[Ponnusamy] p. 362Equation I1dipcj 21283
[Ponnusamy] p. 362Equation I3cphdir 18635  dipdir 21413  ipdir 16538  ipdiri 21401
[Ponnusamy] p. 362Equation I4ipidsq 21279
[Ponnusamy] p. 362Equation 6.46ip0i 21396
[Ponnusamy] p. 362Equation 6.47ip1i 21398
[Ponnusamy] p. 362Equation 6.48ip2i 21399
[Ponnusamy] p. 363Equation I2cphass 18641  dipass 21416  ipass 16544  ipassi 21412
[Prugovecki] p. 186Definition of brabraval 22517  df-bra 22423
[Prugovecki] p. 376Equation 8.1df-kb 22424  kbval 22527
[PtakPulmannova] p. 66Proposition 3.2.17atomli 22955
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 29345
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 22969  atcvat4i 22970  cvrat3 28899  cvrat4 28900  lsatcvat3 28510
[PtakPulmannova] p. 68Definition 3.2.18cvbr 22855  cvrval 28727  df-cv 22852  df-lcv 28477  lspsncv0 15894
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 29357
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 29358
[Quine] p. 16Definition 2.1df-clab 2272  rabid 2718
[Quine] p. 17Definition 2.1''dfsb7 2062
[Quine] p. 18Definition 2.7df-cleq 2278
[Quine] p. 19Definition 2.9conventions 3  df-v 2792
[Quine] p. 34Theorem 5.1abeq2 2390
[Quine] p. 35Theorem 5.2abid2 2402  abid2f 2446
[Quine] p. 40Theorem 6.1sb5 2040
[Quine] p. 40Theorem 6.2sb56 2038  sb6 2039
[Quine] p. 41Theorem 6.3df-clel 2281
[Quine] p. 41Theorem 6.4eqid 2285  eqid1 20833
[Quine] p. 41Theorem 6.5eqcom 2287
[Quine] p. 42Theorem 6.6df-sbc 2994
[Quine] p. 42Theorem 6.7dfsbcq 2995  dfsbcq2 2996
[Quine] p. 43Theorem 6.8vex 2793
[Quine] p. 43Theorem 6.9isset 2794
[Quine] p. 44Theorem 7.3spcgf 2865  spcgv 2870  spcimgf 2863
[Quine] p. 44Theorem 6.11spsbc 3005  spsbcd 3006
[Quine] p. 44Theorem 6.12elex 2798
[Quine] p. 44Theorem 6.13elab 2916  elabg 2917  elabgf 2914
[Quine] p. 44Theorem 6.14noel 3461
[Quine] p. 48Theorem 7.2snprc 3697
[Quine] p. 48Definition 7.1df-pr 3649  df-sn 3648
[Quine] p. 49Theorem 7.4snss 3750  snssg 3756
[Quine] p. 49Theorem 7.5prss 3771  prssg 3772
[Quine] p. 49Theorem 7.6prid1 3736  prid1g 3734  prid2 3737  prid2g 3735  snid 3669  snidg 3667
[Quine] p. 51Theorem 7.13prex 4217  snex 4216  snexALT 4196
[Quine] p. 53Theorem 8.2unisn 3845  unisnALT 27971  unisng 3846
[Quine] p. 53Theorem 8.3uniun 3848
[Quine] p. 54Theorem 8.6elssuni 3857
[Quine] p. 54Theorem 8.7uni0 3856
[Quine] p. 56Theorem 8.17uniabio 6263
[Quine] p. 56Definition 8.18dfiota2 6254
[Quine] p. 57Theorem 8.19iotaval 6264
[Quine] p. 57Theorem 8.22iotanul 6268
[Quine] p. 58Theorem 8.23iotaex 6270
[Quine] p. 58Definition 9.1df-op 3651
[Quine] p. 61Theorem 9.5opabid 4271  opelopab 4286  opelopaba 4281  opelopabaf 4288  opelopabf 4289  opelopabg 4283  opelopabga 4278  oprabid 5844
[Quine] p. 64Definition 9.11df-xp 4695
[Quine] p. 64Definition 9.12df-cnv 4697
[Quine] p. 64Definition 9.15df-id 4309
[Quine] p. 65Theorem 10.3fun0 5273
[Quine] p. 65Theorem 10.4funi 5251
[Quine] p. 65Theorem 10.5funsn 5266  funsng 5264
[Quine] p. 65Definition 10.1df-fun 5224
[Quine] p. 65Definition 10.2args 5041  df-fv 5230
[Quine] p. 68Definition 10.11conventions 3  df-fv 5230  fv2 5482
[Quine] p. 124Theorem 17.3nn0opth2 11282  nn0opth2i 11281  nn0opthi 11280  omopthi 6651
[Quine] p. 177Definition 25.2df-rdg 6419
[Quine] p. 232Equation icarddom 8172
[Quine] p. 284Axiom 39(vi)funimaex 5296  funimaexg 5295
[Quine] p. 331Axiom system NFru 2992
[ReedSimon] p. 36Definition (iii)ax-his3 21656
[ReedSimon] p. 63Exercise 4(a)df-dip 21267  polid 21731  polid2i 21729  polidi 21730
[ReedSimon] p. 63Exercise 4(b)df-ph 21384
[ReedSimon] p. 195Remarklnophm 22592  lnophmi 22591
[Retherford] p. 49Exercise 1(i)leopadd 22705
[Retherford] p. 49Exercise 1(ii)leopmul 22707  leopmuli 22706
[Retherford] p. 49Exercise 1(iv)leoptr 22710
[Retherford] p. 49Definition VI.1df-leop 22425  leoppos 22699
[Retherford] p. 49Exercise 1(iii)leoptri 22709
[Retherford] p. 49Definition of operator orderingleop3 22698
[Rudin] p. 164Equation 27efcan 12371
[Rudin] p. 164Equation 30efzval 12377
[Rudin] p. 167Equation 48absefi 12471
[Sanford] p. 39Rule 3mtp-xor 1526
[Sanford] p. 39Rule 4mpto2 1525
[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 1524
[Schechter] p. 51Definition of antisymmetryintasym 5058
[Schechter] p. 51Definition of irreflexivityintirr 5061
[Schechter] p. 51Definition of symmetrycnvsym 5057
[Schechter] p. 51Definition of transitivitycotr 5055
[Schechter] p. 78Definition of Moore collection of setsdf-mre 13483
[Schechter] p. 79Definition of Moore closuredf-mrc 13484
[Schechter] p. 82Section 4.5df-mrc 13484
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 13486
[Schechter] p. 139Definition AC3dfac9 7758
[Schechter] p. 141Definition (MC)dfac11 26560
[Schechter] p. 149Axiom DC1ax-dc 8068  axdc3 8076
[Schechter] p. 187Definition of ring with unitisrng 15340  isrngo 21038
[Schechter] p. 276Remark 11.6.espan0 22114
[Schechter] p. 276Definition of spandf-span 21881  spanval 21905
[Schechter] p. 428Definition 15.35bastop1 16726
[Schwabhauser] p. 10Axiom A1axcgrrflx 23950
[Schwabhauser] p. 10Axiom A2axcgrtr 23951
[Schwabhauser] p. 10Axiom A3axcgrid 23952
[Schwabhauser] p. 11Axiom A4axsegcon 23963
[Schwabhauser] p. 11Axiom A5ax5seg 23974
[Schwabhauser] p. 11Axiom A6axbtwnid 23975
[Schwabhauser] p. 12Axiom A7axpasch 23977
[Schwabhauser] p. 12Axiom A8axlowdim2 23996
[Schwabhauser] p. 13Axiom A10axeuclid 23999
[Schwabhauser] p. 13Axiom A11axcont 24012
[Schwabhauser] p. 27Theorem 2.1cgrrflx 24018
[Schwabhauser] p. 27Theorem 2.2cgrcomim 24020
[Schwabhauser] p. 27Theorem 2.3cgrtr 24023
[Schwabhauser] p. 27Theorem 2.4cgrcoml 24027
[Schwabhauser] p. 27Theorem 2.5cgrcomr 24028
[Schwabhauser] p. 28Theorem 2.8cgrtriv 24033
[Schwabhauser] p. 28Theorem 2.105segofs 24037
[Schwabhauser] p. 28Definition 2.10df-ofs 24014
[Schwabhauser] p. 29Theorem 2.11cgrextend 24039
[Schwabhauser] p. 29Theorem 2.12segconeq 24041
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 24053  btwntriv2 24043
[Schwabhauser] p. 30Theorem 3.2btwncomim 24044
[Schwabhauser] p. 30Theorem 3.3btwntriv1 24047
[Schwabhauser] p. 30Theorem 3.4btwnswapid 24048
[Schwabhauser] p. 30Theorem 3.5btwnexch2 24054  btwnintr 24050
[Schwabhauser] p. 30Theorem 3.6btwnexch 24056  btwnexch3 24051
[Schwabhauser] p. 30Theorem 3.7btwnouttr 24055
[Schwabhauser] p. 32Theorem 3.13axlowdim1 23995
[Schwabhauser] p. 32Theorem 3.14btwndiff 24058
[Schwabhauser] p. 33Theorem 3.17trisegint 24059
[Schwabhauser] p. 34Theorem 4.2ifscgr 24075
[Schwabhauser] p. 34Definition 4.1df-ifs 24070
[Schwabhauser] p. 35Theorem 4.3cgrsub 24076
[Schwabhauser] p. 35Theorem 4.5cgrxfr 24086
[Schwabhauser] p. 35Definition 4.4df-cgr3 24071
[Schwabhauser] p. 36Theorem 4.6btwnxfr 24087
[Schwabhauser] p. 36Theorem 4.11colinearperm1 24093  colinearperm2 24095  colinearperm3 24094  colinearperm4 24096  colinearperm5 24097
[Schwabhauser] p. 36Definition 4.10df-colinear 24072
[Schwabhauser] p. 37Theorem 4.12colineartriv1 24098
[Schwabhauser] p. 37Theorem 4.13colinearxfr 24106
[Schwabhauser] p. 37Theorem 4.14lineext 24107
[Schwabhauser] p. 37Theorem 4.16fscgr 24111
[Schwabhauser] p. 37Theorem 4.17linecgr 24112
[Schwabhauser] p. 37Definition 4.15df-fs 24073
[Schwabhauser] p. 38Theorem 4.18lineid 24114
[Schwabhauser] p. 38Theorem 4.19idinside 24115
[Schwabhauser] p. 39Theorem 5.1btwnconn1 24132
[Schwabhauser] p. 41Theorem 5.2btwnconn2 24133
[Schwabhauser] p. 41Theorem 5.3btwnconn3 24134
[Schwabhauser] p. 41Theorem 5.5brsegle2 24140
[Schwabhauser] p. 41Definition 5.4df-segle 24138
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 24141
[Schwabhauser] p. 42Theorem 5.7seglerflx 24143
[Schwabhauser] p. 42Theorem 5.8segletr 24145
[Schwabhauser] p. 42Theorem 5.9segleantisym 24146
[Schwabhauser] p. 42Theorem 5.10seglelin 24147
[Schwabhauser] p. 42Theorem 5.11seglemin 24144
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 24149
[Schwabhauser] p. 43Theorem 6.2btwnoutside 24156
[Schwabhauser] p. 43Theorem 6.3broutsideof3 24157
[Schwabhauser] p. 43Theorem 6.4broutsideof 24152  df-outsideof 24151
[Schwabhauser] p. 43Definition 6.1broutsideof2 24153
[Schwabhauser] p. 44Theorem 6.5outsideofrflx 24158
[Schwabhauser] p. 44Theorem 6.6outsideofcom 24159
[Schwabhauser] p. 44Theorem 6.7outsideoftr 24160
[Schwabhauser] p. 44Theorem 6.11outsideofeu 24162
[Schwabhauser] p. 44Definition 6.8df-ray 24169
[Schwabhauser] p. 45Part 2df-lines2 24170
[Schwabhauser] p. 45Theorem 6.13outsidele 24163
[Schwabhauser] p. 45Theorem 6.15lineunray 24178
[Schwabhauser] p. 45Theorem 6.16lineelsb2 24179
[Schwabhauser] p. 45Theorem 6.17linecom 24181  linerflx1 24180  linerflx2 24182
[Schwabhauser] p. 45Theorem 6.18linethru 24184
[Schwabhauser] p. 45Definition 6.14df-line2 24168
[Schwabhauser] p. 46Theorem 6.19linethrueu 24187
[Schwabhauser] p. 46Theorem 6.21lineintmo 24188
[Shapiro] p. 230Theorem 6.5.1dchrhash 20505  dchrsum 20503  dchrsum2 20502  sumdchr 20506
[Shapiro] p. 232Theorem 6.5.2dchr2sum 20507  sum2dchr 20508
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 15296  ablfacrp2 15297
[Shapiro], p. 328Equation 9.2.4vmasum 20450
[Shapiro], p. 329Equation 9.2.7logfac2 20451
[Shapiro], p. 329Equation 9.2.9logfacrlim 20458
[Shapiro], p. 331Equation 9.2.13vmadivsum 20626
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 20629
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 20683  vmalogdivsum2 20682
[Shapiro], p. 375Theorem 9.4.1dirith 20673  dirith2 20672
[Shapiro], p. 375Equation 9.4.3rplogsum 20671  rpvmasum 20670  rpvmasum2 20656
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 20631
[Shapiro], p. 376Equation 9.4.8dchrvmasum 20669
[Shapiro], p. 377Lemma 9.4.1dchrisum 20636  dchrisumlem1 20633  dchrisumlem2 20634  dchrisumlem3 20635  dchrisumlema 20632
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 20639
[Shapiro], p. 379Equation 9.4.16dchrmusum 20668  dchrmusumlem 20666  dchrvmasumlem 20667
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 20638
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 20640
[Shapiro], p. 382Lemma 9.4.4dchrisum0 20664  dchrisum0re 20657  dchrisumn0 20665
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 20650
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 20654
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 20655
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 20710  pntrsumbnd2 20711  pntrsumo1 20709
[Shapiro], p. 405Equation 10.2.1mudivsum 20674
[Shapiro], p. 406Equation 10.2.6mulogsum 20676
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 20678
[Shapiro], p. 407Equation 10.2.8mulog2sum 20681
[Shapiro], p. 418Equation 10.4.6logsqvma 20686
[Shapiro], p. 418Equation 10.4.8logsqvma2 20687
[Shapiro], p. 419Equation 10.4.10selberg 20692
[Shapiro], p. 420Equation 10.4.12selberg2lem 20694
[Shapiro], p. 420Equation 10.4.14selberg2 20695
[Shapiro], p. 422Equation 10.6.7selberg3 20703
[Shapiro], p. 422Equation 10.4.20selberg4lem1 20704
[Shapiro], p. 422Equation 10.4.21selberg3lem1 20701  selberg3lem2 20702
[Shapiro], p. 422Equation 10.4.23selberg4 20705
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 20699
[Shapiro], p. 428Equation 10.6.2selbergr 20712
[Shapiro], p. 429Equation 10.6.8selberg3r 20713
[Shapiro], p. 430Equation 10.6.11selberg4r 20714
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 20728
[Shapiro], p. 434Equation 10.6.27pntlema 20740  pntlemb 20741  pntlemc 20739  pntlemd 20738  pntlemg 20742
[Shapiro], p. 435Equation 10.6.29pntlema 20740
[Shapiro], p. 436Lemma 10.6.1pntpbnd 20732
[Shapiro], p. 436Lemma 10.6.2pntibnd 20737
[Shapiro], p. 436Equation 10.6.34pntlema 20740
[Shapiro], p. 436Equation 10.6.35pntlem3 20753  pntleml 20755
[Stoll] p. 13Definition of symmetric differencesymdif1 3435
[Stoll] p. 16Exercise 4.40dif 3527  dif0 3526
[Stoll] p. 16Exercise 4.8difdifdir 3543
[Stoll] p. 17Theorem 5.1(5)undifv 3530
[Stoll] p. 19Theorem 5.2(13)undm 3428
[Stoll] p. 19Theorem 5.2(13')indm 3429
[Stoll] p. 20Remarkinvdif 3412
[Stoll] p. 25Definition of ordered tripledf-ot 3652
[Stoll] p. 43Definitionuniiun 3957
[Stoll] p. 44Definitionintiin 3958
[Stoll] p. 45Definitiondf-iin 3910
[Stoll] p. 45Definition indexed uniondf-iun 3909
[Stoll] p. 176Theorem 3.4(27)iman 415
[Stoll] p. 262Example 4.1symdif1 3435
[Strang] p. 242Section 6.3expgrowth 26952
[Suppes] p. 22Theorem 2eq0 3471
[Suppes] p. 22Theorem 4eqss 3196  eqssd 3198  eqssi 3197
[Suppes] p. 23Theorem 5ss0 3487  ss0b 3486
[Suppes] p. 23Theorem 6sstr 3189  sstrALT2 27880
[Suppes] p. 23Theorem 7pssirr 3278
[Suppes] p. 23Theorem 8pssn2lp 3279
[Suppes] p. 23Theorem 9psstr 3282
[Suppes] p. 23Theorem 10pssss 3273
[Suppes] p. 25Theorem 12elin 3360  elun 3318
[Suppes] p. 26Theorem 15inidm 3380
[Suppes] p. 26Theorem 16in0 3482
[Suppes] p. 27Theorem 23unidm 3320
[Suppes] p. 27Theorem 24un0 3481
[Suppes] p. 27Theorem 25ssun1 3340
[Suppes] p. 27Theorem 26ssequn1 3347
[Suppes] p. 27Theorem 27unss 3351
[Suppes] p. 27Theorem 28indir 3419
[Suppes] p. 27Theorem 29undir 3420
[Suppes] p. 28Theorem 32difid 3524  difidALT 3525
[Suppes] p. 29Theorem 33difin 3408
[Suppes] p. 29Theorem 34indif 3413
[Suppes] p. 29Theorem 35undif1 3531
[Suppes] p. 29Theorem 36difun2 3535
[Suppes] p. 29Theorem 37difin0 3529
[Suppes] p. 29Theorem 38disjdif 3528
[Suppes] p. 29Theorem 39difundi 3423
[Suppes] p. 29Theorem 40difindi 3425
[Suppes] p. 30Theorem 41nalset 4153
[Suppes] p. 39Theorem 61uniss 3850
[Suppes] p. 39Theorem 65uniop 4269
[Suppes] p. 41Theorem 70intsn 3900
[Suppes] p. 42Theorem 71intpr 3897  intprg 3898
[Suppes] p. 42Theorem 73op1stb 4569
[Suppes] p. 42Theorem 78intun 3896
[Suppes] p. 44Definition 15(a)dfiun2 3939  dfiun2g 3937
[Suppes] p. 44Definition 15(b)dfiin2 3940
[Suppes] p. 47Theorem 86elpw 3633  elpw2 4170  elpw2g 4169  elpwg 3634  elpwgdedVD 27962
[Suppes] p. 47Theorem 87pwid 3640
[Suppes] p. 47Theorem 89pw0 3764
[Suppes] p. 48Theorem 90pwpw0 3765
[Suppes] p. 52Theorem 101xpss12 4792
[Suppes] p. 52Theorem 102xpindi 4819  xpindir 4820
[Suppes] p. 52Theorem 103xpundi 4741  xpundir 4742
[Suppes] p. 54Theorem 105elirrv 7307
[Suppes] p. 58Theorem 2relss 4775
[Suppes] p. 59Theorem 4eldm 4876  eldm2 4877  eldm2g 4875  eldmg 4874
[Suppes] p. 59Definition 3df-dm 4699
[Suppes] p. 60Theorem 6dmin 4886
[Suppes] p. 60Theorem 8rnun 5089
[Suppes] p. 60Theorem 9rnin 5090
[Suppes] p. 60Definition 4dfrn2 4868
[Suppes] p. 61Theorem 11brcnv 4864  brcnvg 4862
[Suppes] p. 62Equation 5elcnv 4858  elcnv2 4859
[Suppes] p. 62Theorem 12relcnv 5051
[Suppes] p. 62Theorem 15cnvin 5088
[Suppes] p. 62Theorem 16cnvun 5086
[Suppes] p. 63Theorem 20co02 5185
[Suppes] p. 63Theorem 21dmcoss 4944
[Suppes] p. 63Definition 7df-co 4698
[Suppes] p. 64Theorem 26cnvco 4865
[Suppes] p. 64Theorem 27coass 5190
[Suppes] p. 65Theorem 31resundi 4969
[Suppes] p. 65Theorem 34elima 5017  elima2 5018  elima3 5019  elimag 5016
[Suppes] p. 65Theorem 35imaundi 5093
[Suppes] p. 66Theorem 40dminss 5095
[Suppes] p. 66Theorem 41imainss 5096
[Suppes] p. 67Exercise 11cnvxp 5097
[Suppes] p. 81Definition 34dfec2 6659
[Suppes] p. 82Theorem 72elec 6695  elecg 6694
[Suppes] p. 82Theorem 73erth 6700  erth2 6701
[Suppes] p. 83Theorem 74erdisj 6703
[Suppes] p. 89Theorem 96map0b 6802
[Suppes] p. 89Theorem 97map0 6804  map0g 6803
[Suppes] p. 89Theorem 98mapsn 6805
[Suppes] p. 89Theorem 99mapss 6806
[Suppes] p. 91Definition 12(ii)alephsuc 7691
[Suppes] p. 91Definition 12(iii)alephlim 7690
[Suppes] p. 92Theorem 1enref 6890  enrefg 6889
[Suppes] p. 92Theorem 2ensym 6906  ensymb 6905  ensymi 6907
[Suppes] p. 92Theorem 3entr 6909
[Suppes] p. 92Theorem 4unen 6939
[Suppes] p. 94Theorem 15endom 6884
[Suppes] p. 94Theorem 16ssdomg 6903
[Suppes] p. 94Theorem 17domtr 6910
[Suppes] p. 95Theorem 18sbth 6977
[Suppes] p. 97Theorem 23canth2 7010  canth2g 7011
[Suppes] p. 97Definition 3brsdom2 6981  df-sdom 6862  dfsdom2 6980
[Suppes] p. 97Theorem 21(i)sdomirr 6994
[Suppes] p. 97Theorem 22(i)domnsym 6983
[Suppes] p. 97Theorem 21(ii)sdomnsym 6982
[Suppes] p. 97Theorem 22(ii)domsdomtr 6992
[Suppes] p. 97Theorem 22(iv)brdom2 6887
[Suppes] p. 97Theorem 21(iii)sdomtr 6995
[Suppes] p. 97Theorem 22(iii)sdomdomtr 6990
[Suppes] p. 98Exercise 4fundmen 6930  fundmeng 6931
[Suppes] p. 98Exercise 6xpdom3 6956
[Suppes] p. 98Exercise 11sdomentr 6991
[Suppes] p. 104Theorem 37fofi 7138
[Suppes] p. 104Theorem 38pwfi 7147
[Suppes] p. 105Theorem 40pwfi 7147
[Suppes] p. 111Axiom for cardinal numberscarden 8169
[Suppes] p. 130Definition 3df-tr 4116
[Suppes] p. 132Theorem 9ssonuni 4578
[Suppes] p. 134Definition 6df-suc 4398
[Suppes] p. 136Theorem Schema 22findes 4686  finds 4682  finds1 4685  finds2 4684
[Suppes] p. 151Theorem 42isfinite 7349  isfinite2 7111  isfiniteg 7113  unbnn 7109
[Suppes] p. 162Definition 5df-ltnq 8538  df-ltpq 8530
[Suppes] p. 197Theorem Schema 4tfindes 4653  tfinds 4650  tfinds2 4654
[Suppes] p. 209Theorem 18oaord1 6545
[Suppes] p. 209Theorem 21oaword2 6547
[Suppes] p. 211Theorem 25oaass 6555
[Suppes] p. 225Definition 8iscard2 7605
[Suppes] p. 227Theorem 56ondomon 8181
[Suppes] p. 228Theorem 59harcard 7607
[Suppes] p. 228Definition 12(i)aleph0 7689
[Suppes] p. 228Theorem Schema 61onintss 4442
[Suppes] p. 228Theorem Schema 62onminesb 4589  onminsb 4590
[Suppes] p. 229Theorem 64alephval2 8190
[Suppes] p. 229Theorem 65alephcard 7693
[Suppes] p. 229Theorem 66alephord2i 7700
[Suppes] p. 229Theorem 67alephnbtwn 7694
[Suppes] p. 229Definition 12df-aleph 7569
[Suppes] p. 242Theorem 6weth 8118
[Suppes] p. 242Theorem 8entric 8175
[Suppes] p. 242Theorem 9carden 8169
[TakeutiZaring] p. 8Axiom 1ax-ext 2266
[TakeutiZaring] p. 13Definition 4.5df-cleq 2278
[TakeutiZaring] p. 13Proposition 4.6df-clel 2281
[TakeutiZaring] p. 13Proposition 4.9cvjust 2280
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2302
[TakeutiZaring] p. 14Definition 4.16df-oprab 5824
[TakeutiZaring] p. 14Proposition 4.14ru 2992
[TakeutiZaring] p. 15Axiom 2zfpair 4212
[TakeutiZaring] p. 15Exercise 1elpr 3660  elpr2 3661  elprg 3659
[TakeutiZaring] p. 15Exercise 2elsn 3657  elsnc 3665  elsnc2 3671  elsnc2g 3670  elsncg 3664
[TakeutiZaring] p. 15Exercise 3elop 4239
[TakeutiZaring] p. 15Exercise 4sneq 3653  sneqr 3782
[TakeutiZaring] p. 15Definition 5.1dfpr2 3658  dfsn2 3656
[TakeutiZaring] p. 16Axiom 3uniex 4516
[TakeutiZaring] p. 16Exercise 6opth 4245
[TakeutiZaring] p. 16Exercise 7opex 4237
[TakeutiZaring] p. 16Exercise 8rext 4222
[TakeutiZaring] p. 16Corollary 5.8unex 4518  unexg 4521
[TakeutiZaring] p. 16Definition 5.3dftp2 3681
[TakeutiZaring] p. 16Definition 5.5df-uni 3830
[TakeutiZaring] p. 16Definition 5.6df-in 3161  df-un 3159
[TakeutiZaring] p. 16Proposition 5.7unipr 3843  uniprg 3844
[TakeutiZaring] p. 17Axiom 4pwex 4193  pwexg 4194
[TakeutiZaring] p. 17Exercise 1eltp 3680
[TakeutiZaring] p. 17Exercise 5elsuc 4461  elsucg 4459  sstr2 3188
[TakeutiZaring] p. 17Exercise 6uncom 3321
[TakeutiZaring] p. 17Exercise 7incom 3363
[TakeutiZaring] p. 17Exercise 8unass 3334
[TakeutiZaring] p. 17Exercise 9inass 3381
[TakeutiZaring] p. 17Exercise 10indi 3417
[TakeutiZaring] p. 17Exercise 11undi 3418
[TakeutiZaring] p. 17Definition 5.9df-pss 3170  dfss2 3171
[TakeutiZaring] p. 17Definition 5.10df-pw 3629
[TakeutiZaring] p. 18Exercise 7unss2 3348
[TakeutiZaring] p. 18Exercise 9df-ss 3168  sseqin2 3390
[TakeutiZaring] p. 18Exercise 10ssid 3199
[TakeutiZaring] p. 18Exercise 12inss1 3391  inss2 3392
[TakeutiZaring] p. 18Exercise 13nss 3238
[TakeutiZaring] p. 18Exercise 15unieq 3838
[TakeutiZaring] p. 18Exercise 18sspwb 4223  sspwimp 27963  sspwimpALT 27970  sspwimpALT2 27974  sspwimpcf 27965
[TakeutiZaring] p. 18Exercise 19pweqb 4230
[TakeutiZaring] p. 19Axiom 5ax-rep 4133
[TakeutiZaring] p. 20Definitiondf-rab 2554
[TakeutiZaring] p. 20Corollary 5.160ex 4152
[TakeutiZaring] p. 20Definition 5.12df-dif 3157
[TakeutiZaring] p. 20Definition 5.14dfnul2 3459
[TakeutiZaring] p. 20Proposition 5.15difid 3524  difidALT 3525
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3466  n0f 3465  neq0 3467
[TakeutiZaring] p. 21Axiom 6zfreg 7305
[TakeutiZaring] p. 21Axiom 6'zfregs 7410
[TakeutiZaring] p. 21Theorem 5.22setind 7415
[TakeutiZaring] p. 21Definition 5.20df-v 2792
[TakeutiZaring] p. 21Proposition 5.21vprc 4154
[TakeutiZaring] p. 22Exercise 10ss 3485
[TakeutiZaring] p. 22Exercise 3ssex 4160  ssexg 4162
[TakeutiZaring] p. 22Exercise 4inex1 4157
[TakeutiZaring] p. 22Exercise 5ruv 7310
[TakeutiZaring] p. 22Exercise 6elirr 7308
[TakeutiZaring] p. 22Exercise 7ssdif0 3515
[TakeutiZaring] p. 22Exercise 11difdif 3304
[TakeutiZaring] p. 22Exercise 13undif3 3431  undif3VD 27927
[TakeutiZaring] p. 22Exercise 14difss 3305
[TakeutiZaring] p. 22Exercise 15sscon 3312
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2550
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2551
[TakeutiZaring] p. 23Proposition 6.2xpex 4801  xpexg 4800  xpexgALT 6032
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4696
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5278
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5411  fun11 5281
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5234  svrelfun 5279
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4867
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4869
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4701
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4702
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4698
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5128  dfrel2 5124
[TakeutiZaring] p. 25Exercise 3xpss 4793
[TakeutiZaring] p. 25Exercise 5relun 4802
[TakeutiZaring] p. 25Exercise 6reluni 4808
[TakeutiZaring] p. 25Exercise 9inxp 4818
[TakeutiZaring] p. 25Exercise 12relres 4983
[TakeutiZaring] p. 25Exercise 13opelres 4960  opelresg 4962
[TakeutiZaring] p. 25Exercise 14dmres 4976
[TakeutiZaring] p. 25Exercise 15resss 4979
[TakeutiZaring] p. 25Exercise 17resabs1 4984
[TakeutiZaring] p. 25Exercise 18funres 5259
[TakeutiZaring] p. 25Exercise 24relco 5170
[TakeutiZaring] p. 25Exercise 29funco 5258
[TakeutiZaring] p. 25Exercise 30f1co 5412
[TakeutiZaring] p. 26Definition 6.10eu2 2170
[TakeutiZaring] p. 26Definition 6.11conventions 3  df-fv 5230  fv3 5502
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5208  cnvexg 5207
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4941  dmexg 4939
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4942  rnexg 4940
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 27058
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 27059
[TakeutiZaring] p. 27Corollary 6.13fvex 5500
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5505  tz6.12-afv 27415  tz6.12 5506  tz6.12c 5509
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5508  tz6.12i 5510
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5225
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5226
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5228  wfo 5220
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5227  wf1 5219
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5229  wf1o 5221
[TakeutiZaring] p. 28Exercise 4eqfnfv 5584  eqfnfv2 5585  eqfnfv2f 5588
[TakeutiZaring] p. 28Exercise 5fvco 5557
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5703  fnexALT 5704
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5699  resfunexgALT 5700
[TakeutiZaring] p. 29Exercise 9funimaex 5296  funimaexg 5295
[TakeutiZaring] p. 29Definition 6.18df-br 4026
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4315
[TakeutiZaring] p. 30Definition 6.21dffr2 4358  dffr3 5045  eliniseg 5042  iniseg 5044
[TakeutiZaring] p. 30Definition 6.22df-eprel 4305
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4371  fr3nr 4571  frirr 4370
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4352
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 4573
[TakeutiZaring] p. 31Exercise 1frss 4360
[TakeutiZaring] p. 31Exercise 4wess 4380
[TakeutiZaring] p. 31Proposition 6.26tz6.26 23607  tz6.26i 23608  wefrc 4387  wereu2 4390
[TakeutiZaring] p. 32Theorem 6.27wfi 23609  wfii 23610
[TakeutiZaring] p. 32Definition 6.28df-isom 5231
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5788
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5789
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5795
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5796
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5797
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 5801
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 5808
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5810
[TakeutiZaring] p. 35Notationwtr 4115
[TakeutiZaring] p. 35Theorem 7.2trelpss 27060  tz7.2 4377
[TakeutiZaring] p. 35Definition 7.1dftr3 4119
[TakeutiZaring] p. 36Proposition 7.4ordwe 4405
[TakeutiZaring] p. 36Proposition 7.5tz7.5 4413
[TakeutiZaring] p. 36Proposition 7.6ordelord 4414  ordelordALT 27573  ordelordALTVD 27912
[TakeutiZaring] p. 37Corollary 7.8ordelpss 4420  ordelssne 4419
[TakeutiZaring] p. 37Proposition 7.7tz7.7 4418
[TakeutiZaring] p. 37Proposition 7.9ordin 4422
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 4580
[TakeutiZaring] p. 38Corollary 7.15ordsson 4581
[TakeutiZaring] p. 38Definition 7.11df-on 4396
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 4424
[TakeutiZaring] p. 38Proposition 7.12onfrALT 27586  ordon 4574
[TakeutiZaring] p. 38Proposition 7.13onprc 4576
[TakeutiZaring] p. 39Theorem 7.17tfi 4644
[TakeutiZaring] p. 40Exercise 3ontr2 4439
[TakeutiZaring] p. 40Exercise 7dftr2 4117
[TakeutiZaring] p. 40Exercise 9onssmin 4588
[TakeutiZaring] p. 40Exercise 11unon 4622
[TakeutiZaring] p. 40Exercise 12ordun 4494
[TakeutiZaring] p. 40Exercise 14ordequn 4493
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4577
[TakeutiZaring] p. 40Proposition 7.20elssuni 3857
[TakeutiZaring] p. 41Definition 7.22df-suc 4398
[TakeutiZaring] p. 41Proposition 7.23sssucid 4469  sucidg 4470
[TakeutiZaring] p. 41Proposition 7.24suceloni 4604
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 4484  ordnbtwn 4483
[TakeutiZaring] p. 41Proposition 7.26onsucuni 4619
[TakeutiZaring] p. 42Exercise 1df-lim 4397
[TakeutiZaring] p. 42Exercise 4omssnlim 4670
[TakeutiZaring] p. 42Exercise 7ssnlim 4674
[TakeutiZaring] p. 42Exercise 8onsucssi 4632  ordelsuc 4611
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 4613
[TakeutiZaring] p. 42Definition 7.27nlimon 4642
[TakeutiZaring] p. 42Definition 7.28dfom2 4658
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4675
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4676
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4677
[TakeutiZaring] p. 43Remarkomon 4667
[TakeutiZaring] p. 43Axiom 7inf3 7332  omex 7340
[TakeutiZaring] p. 43Theorem 7.32ordom 4665
[TakeutiZaring] p. 43Corollary 7.31find 4681
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4678
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4679
[TakeutiZaring] p. 44Exercise 1limomss 4661
[TakeutiZaring] p. 44Exercise 2int0 3878  trint0 4132
[TakeutiZaring] p. 44Exercise 4intss1 3879
[TakeutiZaring] p. 44Exercise 5intex 4171
[TakeutiZaring] p. 44Exercise 6oninton 4591
[TakeutiZaring] p. 44Exercise 11ordintdif 4441
[TakeutiZaring] p. 44Definition 7.35df-int 3865
[TakeutiZaring] p. 44Proposition 7.34noinfep 7356
[TakeutiZaring] p. 45Exercise 4onint 4586
[TakeutiZaring] p. 47Lemma 1tfrlem1 6387
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 6409
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 6410
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 6411
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 6415  tz7.44-2 6416  tz7.44-3 6417
[TakeutiZaring] p. 50Exercise 1smogt 6380
[TakeutiZaring] p. 50Exercise 3smoiso 6375
[TakeutiZaring] p. 50Definition 7.46df-smo 6359
[TakeutiZaring] p. 51Proposition 7.49tz7.49 6453  tz7.49c 6454
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 6451
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 6450
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 6452
[TakeutiZaring] p. 53Proposition 7.532eu5 2229
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 7635
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 7636
[TakeutiZaring] p. 56Definition 8.1oalim 6527  oasuc 6519
[TakeutiZaring] p. 57Remarktfindsg 4651
[TakeutiZaring] p. 57Proposition 8.2oacl 6530
[TakeutiZaring] p. 57Proposition 8.3oa0 6511  oa0r 6533
[TakeutiZaring] p. 57Proposition 8.16omcl 6531
[TakeutiZaring] p. 58Corollary 8.5oacan 6542
[TakeutiZaring] p. 58Proposition 8.4nnaord 6613  nnaordi 6612  oaord 6541  oaordi 6540
[TakeutiZaring] p. 59Proposition 8.6iunss2 3949  uniss2 3860
[TakeutiZaring] p. 59Proposition 8.7oawordri 6544
[TakeutiZaring] p. 59Proposition 8.8oawordeu 6549  oawordex 6551
[TakeutiZaring] p. 59Proposition 8.9nnacl 6605
[TakeutiZaring] p. 59Proposition 8.10oaabs 6638
[TakeutiZaring] p. 60Remarkoancom 7348
[TakeutiZaring] p. 60Proposition 8.11oalimcl 6554
[TakeutiZaring] p. 62Exercise 1nnarcl 6610
[TakeutiZaring] p. 62Exercise 5oaword1 6546
[TakeutiZaring] p. 62Definition 8.15om0 6512  om0x 6514  omlim 6528  omsuc 6521
[TakeutiZaring] p. 63Proposition 8.17nnecl 6607  nnmcl 6606
[TakeutiZaring] p. 63Proposition 8.19nnmord 6626  nnmordi 6625  omord 6562  omordi 6560
[TakeutiZaring] p. 63Proposition 8.20omcan 6563
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 6630  omwordri 6566
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 6534
[TakeutiZaring] p. 63Proposition 8.18(2)om1 6536  om1r 6537
[TakeutiZaring] p. 64Proposition 8.22om00 6569
[TakeutiZaring] p. 64Proposition 8.23omordlim 6571
[TakeutiZaring] p. 64Proposition 8.24omlimcl 6572
[TakeutiZaring] p. 64Proposition 8.25odi 6573
[TakeutiZaring] p. 65Theorem 8.26omass 6574
[TakeutiZaring] p. 67Definition 8.30nnesuc 6602  oe0 6517  oelim 6529  oesuc 6522  onesuc 6525
[TakeutiZaring] p. 67Proposition 8.31oe0m0 6515
[TakeutiZaring] p. 67Proposition 8.32oen0 6580
[TakeutiZaring] p. 67Proposition 8.33oeordi 6581
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 6516
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 6539
[TakeutiZaring] p. 68Corollary 8.34oeord 6582
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 6588
[TakeutiZaring] p. 68Proposition 8.35oewordri 6586
[TakeutiZaring] p. 68Proposition 8.37oeworde 6587
[TakeutiZaring] p. 69Proposition 8.41oeoa 6591
[TakeutiZaring] p. 70Proposition 8.42oeoe 6593
[TakeutiZaring] p. 73Theorem 9.1trcl 7406  tz9.1 7407
[TakeutiZaring] p. 76Definition 9.9df-r1 7432  r10 7436  r1lim 7440  r1limg 7439  r1suc 7438  r1sucg 7437
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 7448  r1ord2 7449  r1ordg 7446
[TakeutiZaring] p. 78Proposition 9.12tz9.12 7458
[TakeutiZaring] p. 78Proposition 9.13rankwflem 7483  tz9.13 7459  tz9.13g 7460
[TakeutiZaring] p. 79Definition 9.14df-rank 7433  rankval 7484  rankvalb 7465  rankvalg 7485
[TakeutiZaring] p. 79Proposition 9.16rankel 7507  rankelb 7492
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 7521  rankval3 7508  rankval3b 7494
[TakeutiZaring] p. 79Proposition 9.18rankonid 7497
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 7463
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 7502  rankr1c 7489  rankr1g 7500
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 7503
[TakeutiZaring] p. 80Exercise 1rankss 7517  rankssb 7516
[TakeutiZaring] p. 80Exercise 2unbndrank 7510
[TakeutiZaring] p. 80Proposition 9.19bndrank 7509
[TakeutiZaring] p. 83Axiom of Choiceac4 8098  dfac3 7744
[TakeutiZaring] p. 84Theorem 10.3dfac8a 7653  numth 8095  numth2 8094
[TakeutiZaring] p. 85Definition 10.4cardval 8164
[TakeutiZaring] p. 85Proposition 10.5cardid 8165  cardid2 7582
[TakeutiZaring] p. 85Proposition 10.9oncard 7589
[TakeutiZaring] p. 85Proposition 10.10carden 8169
[TakeutiZaring] p. 85Proposition 10.11cardidm 7588
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 7573
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 7594
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7586
[TakeutiZaring] p. 87Proposition 10.15pwen 7030
[TakeutiZaring] p. 88Exercise 1en0 6920
[TakeutiZaring] p. 88Exercise 7infensuc 7035
[TakeutiZaring] p. 89Exercise 10omxpen 6960
[TakeutiZaring] p. 90Corollary 10.23cardnn 7592
[TakeutiZaring] p. 90Definition 10.27alephiso 7721
[TakeutiZaring] p. 90Proposition 10.20nneneq 7040
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7046
[TakeutiZaring] p. 90Proposition 10.26alephprc 7722
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7045
[TakeutiZaring] p. 91Exercise 2alephle 7711
[TakeutiZaring] p. 91Exercise 3aleph0 7689
[TakeutiZaring] p. 91Exercise 4cardlim 7601
[TakeutiZaring] p. 91Exercise 7infpss 7839
[TakeutiZaring] p. 91Exercise 8infcntss 7126
[TakeutiZaring] p. 91Definition 10.29df-fin 6863  isfi 6881
[TakeutiZaring] p. 92Proposition 10.32onfin 7047
[TakeutiZaring] p. 92Proposition 10.34imadomg 8155
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6953
[TakeutiZaring] p. 93Proposition 10.35fodomb 8147
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 7811  unxpdom 7066
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 7603  cardsdomelir 7602
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7068
[TakeutiZaring] p. 94Proposition 10.39infxpen 7638
[TakeutiZaring] p. 95Definition 10.42df-map 6770
[TakeutiZaring] p. 95Proposition 10.40infxpidm 8180  infxpidm2 7640
[TakeutiZaring] p. 95Proposition 10.41infcda 7830  infxp 7837  infxpg 24494
[TakeutiZaring] p. 96Proposition 10.44pw2en 6965  pw2f1o 6963
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7023
[TakeutiZaring] p. 97Theorem 10.46ac6s3 8110
[TakeutiZaring] p. 98Theorem 10.46ac6c5 8105  ac6s5 8114
[TakeutiZaring] p. 98Theorem 10.47unidom 8161
[TakeutiZaring] p. 99Theorem 10.48uniimadom 8162  uniimadomf 8163
[TakeutiZaring] p. 100Definition 11.1cfcof 7896
[TakeutiZaring] p. 101Proposition 11.7cofsmo 7891
[TakeutiZaring] p. 102Exercise 1cfle 7876
[TakeutiZaring] p. 102Exercise 2cf0 7873
[TakeutiZaring] p. 102Exercise 3cfsuc 7879
[TakeutiZaring] p. 102Exercise 4cfom 7886
[TakeutiZaring] p. 102Proposition 11.9coftr 7895
[TakeutiZaring] p. 103Theorem 11.15alephreg 8200
[TakeutiZaring] p. 103Proposition 11.11cardcf 7874
[TakeutiZaring] p. 103Proposition 11.13alephsing 7898
[TakeutiZaring] p. 104Corollary 11.17cardinfima 7720
[TakeutiZaring] p. 104Proposition 11.16carduniima 7719
[TakeutiZaring] p. 104Proposition 11.18alephfp 7731  alephfp2 7732
[TakeutiZaring] p. 106Theorem 11.20gchina 8317
[TakeutiZaring] p. 106Theorem 11.21mappwen 7735
[TakeutiZaring] p. 107Theorem 11.26konigth 8187
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 8201
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 8202
[Tarski] p. 67Axiom B5ax-4 2078
[Tarski] p. 67Scheme B5sp 1717
[Tarski] p. 68Lemma 6avril1 20829  equid 1646  equid1 2100  equid1ALT 2118
[Tarski] p. 69Lemma 7equcomi 1647
[Tarski] p. 70Lemma 14spim 1918  spime 1919  spimeh 1724
[Tarski] p. 70Lemma 16ax-11 1716  ax-11o 2084  ax11i 1629
[Tarski] p. 70Lemmas 16 and 17sb6 2039
[Tarski] p. 75Axiom B7ax9v 1638
[Tarski] p. 75Scheme B7ax9vax9 28426
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1604  ax17o 2099
[Tarski], p. 75Scheme B8 of system S2ax-13 1687  ax-14 1689  ax-8 1645
[Truss] p. 114Theorem 5.18ruc 12516
[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 816
[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 2242  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 27972
[WhiteheadRussell] p. 102Theorem *2.15con1 122
[WhiteheadRussell] p. 103Theorem *2.16con3 128  con3th 926
[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 557
[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 855
[WhiteheadRussell] p. 104Theorem *2.27conventions 3  pm2.27 37
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 513
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 514
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 818
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 819
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 817
[WhiteheadRussell] p. 105Definition *2.33df-3or 937
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 560
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 558
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 559
[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 765
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 766
[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 825
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 401
[WhiteheadRussell] p. 108Theorem *2.69looinv 176
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 820
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 821
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 824
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 823
[WhiteheadRussell] p. 108Theorem *2.77ax-2 8
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 826
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 827
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 73
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 828
[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 854
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 572
[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 570
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 571
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 564
[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 556
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 834
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 809
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 808
[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 563
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 566
[WhiteheadRussell] p. 117Theorem *4.21bicom 193
[WhiteheadRussell] p. 117Theorem *4.22biantr 899  bitr 691  wl-bitr 24328
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 626
[WhiteheadRussell] p. 117Theorem *4.25oridm 502  pm4.25 503
[WhiteheadRussell] p. 118Theorem *4.3ancom 439
[WhiteheadRussell] p. 118Theorem *4.4andi 839
[WhiteheadRussell] p. 118Theorem *4.31orcom 378
[WhiteheadRussell] p. 118Theorem *4.32anass 632
[WhiteheadRussell] p. 118Theorem *4.33orass 512
[WhiteheadRussell] p. 118Theorem *4.36anbi1 689
[WhiteheadRussell] p. 118Theorem *4.37orbi1 688
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 844
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 843
[WhiteheadRussell] p. 118Definition *4.34df-3an 938
[WhiteheadRussell] p. 119Theorem *4.41ordi 836
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 928
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 895
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 562
[WhiteheadRussell] p. 119Theorem *4.45orabs 830  pm4.45 671  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 613  pm4.71d 617  pm4.71i 615  pm4.71r 614  pm4.71rd 618  pm4.71ri 616
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 848
[WhiteheadRussell] p. 121Theorem *4.73iba 491
[WhiteheadRussell] p. 121Theorem *4.74biorf 396
[WhiteheadRussell] p. 121Theorem *4.76jcab 835  pm4.76 838
[WhiteheadRussell] p. 121Theorem *4.77jaob 760  pm4.77 764
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 567
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 568
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 356
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 357
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 896
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 897
[WhiteheadRussell] p. 122Theorem *4.84imbi1 315
[WhiteheadRussell] p. 122Theorem *4.85imbi2 316
[WhiteheadRussell] p. 122Theorem *4.86bibi1 319  wl-bibi1 24321
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 352  impexp 435  pm4.87 569
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 832
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 856
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 857
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 859
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 858
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 861
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 862
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 860
[WhiteheadRussell] p. 124Theorem *5.18nbbn 349  pm5.18 347
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 351
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 833
[WhiteheadRussell] p. 124Theorem *5.22xor 863
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 865
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 866
[WhiteheadRussell] p. 124Theorem *5.25dfor2 402
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 694
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 353
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 328
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 880
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 902
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 573
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 619
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 850
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 871
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 851
[WhiteheadRussell] p. 125Theorem *5.41imdi 354  pm5.41 355
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 533
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 879
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 773
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 872
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 869
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 695
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 891
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 892
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 904
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 332
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 237
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 905
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 26953
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 26954
[WhiteheadRussell] p. 147Theorem *10.2219.26 1581
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 26955
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 26956
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 26957
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1603
[WhiteheadRussell] p. 151Theorem *10.301albitr 26958
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 26959
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 26960
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 26961
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 26962
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 26964
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 26965
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 26966
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 26963
[WhiteheadRussell] p. 159Theorem *11.1stdpc4-2 26969
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2058
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 26970
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 26971
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1713
[WhiteheadRussell] p. 160Theorem *11.222exnaln 26972
[WhiteheadRussell] p. 160Theorem *11.252nexaln 26973
[WhiteheadRussell] p. 161Theorem *11.319.21vv 26974
[WhiteheadRussell] p. 162Theorem *11.322alim 26975
[WhiteheadRussell] p. 162Theorem *11.332albi 26976
[WhiteheadRussell] p. 162Theorem *11.342exim 26977
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 26979
[WhiteheadRussell] p. 162Theorem *11.3412exbi 26978
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1598
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 26981
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 26982
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 26980
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1561
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 26983
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 26984
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1568
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 26985
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1836  pm11.53g 24363
[WhiteheadRussell] p. 164Theorem *11.5212exanali 26986
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 26991
[WhiteheadRussell] p. 165Theorem *11.56aaanv 26987
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 26988
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 26989
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 26990
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 26995
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 26992
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 26993
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 26994
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 26996
[WhiteheadRussell] p. 175Definition *14.02df-eu 2149
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 27007  pm13.13b 27008
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 27009
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2520
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2521
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2910
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 27015
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 27016
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 27010
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 27590  pm13.193 27011
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 27012
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 27013
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 27014
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 27021
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 27020
[WhiteheadRussell] p. 184Definition *14.01iotasbc 27019
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3045
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 27022  pm14.122b 27023  pm14.122c 27024
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 27025  pm14.123b 27026  pm14.123c 27027
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 27029
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 27028
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 27030
[WhiteheadRussell] p. 190Theorem *14.22iota4 6271
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 27031
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6272
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 27032
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 27034
[WhiteheadRussell] p. 192Theorem *14.26eupick 2208  eupickbi 2211  sbaniota 27035
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 27033
[WhiteheadRussell] p. 192Theorem *14.271eubi 27036
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 27037
[WhiteheadRussell] p. 235Definition *30.01conventions 3  df-fv 5230
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7629  pm54.43lem 7628
[Young] p. 141Definition of operator orderingleop2 22697
[Young] p. 142Example 12.2(i)0leop 22703  idleop 22704
[vandenDries] p. 42Lemma 61irrapx1 26313
[vandenDries] p. 43Theorem 62pellex 26320  pellexlem1 26314

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