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 Hilbert Space Explorer User Mathboxes

Bibliographic Cross-Reference for the Metamath Proof Explorer
Bibliographic ReferenceDescriptionMetamath Proof Explorer Page(s)
[Adamek] p. 28Remark 3.12invf1o 17035  invisoinvl 17056
[Adamek] p. 28Example 3.13idinv 17055  idiso 17054
[Adamek] p. 28Definition 3.8df-inv 17014  df-iso 17015  dfiso2 17038
[Adamek] p. 29Definition 3.15cic 17065  df-cic 17062
[Adamek] p. 29Proposition 3.14(2)invco 17037  isoco 17043
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 17413
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 17413
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 17398
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 17398
[Adamek] p. 101Example 7.2 (6)irinitoringc 44556
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17268
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17272
[Adamek] p. 103Example 7.9 (3)nzerooringczr 44559
[AhoHopUll] p. 2Section 1.1df-bigo 44824
[AhoHopUll] p. 12Section 1.3df-blen 44846
[AhoHopUll] p. 318Section 9.1df-concat 13919  df-pfx 14029  df-substr 13999  df-word 13863  lencl 13881  wrd0 13887
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 23310  df-nmoo 28524
[AkhiezerGlazman] p. 64Theoremhmopidmch 29932  hmopidmchi 29930
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 29980  pjcmul2i 29981
[AkhiezerGlazman] p. 72Theoremcnvunop 29697  unoplin 29699
[AkhiezerGlazman] p. 73Theoremelunop2 29792  lnopunii 29791
[Apostol] p. 18Theorem I.2negeu 10868
[Apostol] p. 18Theorem I.3negsub 10926  negsubd 10995  negsubi 10956
[Apostol] p. 18Theorem I.4negneg 10928  negnegd 10980  negnegi 10948
[Apostol] p. 18Theorem I.5subdi 11065  subdid 11088  subdii 11081  subdir 11066  subdird 11089  subdiri 11082
[Apostol] p. 18Theorem I.6mul01 10811  mul01d 10831  mul01i 10822  mul02 10810  mul02d 10830  mul02i 10821
[Apostol] p. 18Theorem I.7mulcan 11269  mulcan2d 11266  mulcand 11265  mulcani 11271
[Apostol] p. 18Theorem I.8receu 11277  xreceu 30602
[Apostol] p. 18Theorem I.9divrec 11306  divrecd 11411  divreci 11377  divreczi 11370
[Apostol] p. 18Theorem I.10recrec 11329  recreci 11364
[Apostol] p. 18Theorem I.11mul0or 11272  mul0ord 11282  mul0ori 11280
[Apostol] p. 18Theorem I.12mul2neg 11071  mul2negd 11087  mul2negi 11080  mulneg1 11068  mulneg1d 11085  mulneg1i 11078
[Apostol] p. 18Theorem I.14divmuldiv 11332  divmuldivd 11449  divmuldivi 11392  rdivmuldivd 30887
[Apostol] p. 18Theorem I.15divdivdiv 11333  divdivdivd 11455  divdivdivi 11395
[Apostol] p. 20Axiom 8rpneg 12414
[Apostol] p. 20Axiom 90nrp 12417
[Apostol] p. 20Theorem I.17lttri 10758
[Apostol] p. 20Theorem I.19ltmul1 11482  ltmul1a 11481  ltmul1i 11550  ltmul1ii 11560  ltmul2 11483  ltmul2d 12466  ltmul2dd 12480  ltmul2i 11553
[Apostol] p. 20Theorem I.20msqgt0 11152  msqgt0d 11199  msqgt0i 11169
[Apostol] p. 20Theorem I.210lt1 11154
[Apostol] p. 20Theorem I.23lt0neg1 11138  lt0neg1d 11201  ltneg 11132  ltnegd 11210  ltnegi 11176
[Apostol] p. 20Definition of positive numbersdf-rp 12383
[Apostol] p. 21Exercise 4recgt0 11478  recgt0d 11566  recgt0i 11537  recgt0ii 11538
[Apostol] p. 22Definition of integersdf-z 11975
[Apostol] p. 22Definition of positive integersdfnn3 11644
[Apostol] p. 22Definition of rationalsdf-q 12342
[Apostol] p. 24Theorem I.26supeu 8909
[Apostol] p. 26Theorem I.28nnunb 11886
[Apostol] p. 26Theorem I.29arch 11887
[Apostol] p. 28Exercise 2btwnz 12077
[Apostol] p. 28Exercise 3nnrecl 11888
[Apostol] p. 28Exercise 4rebtwnz 12340
[Apostol] p. 28Exercise 5zbtwnre 12339
[Apostol] p. 28Exercise 6qbtwnre 12585
[Apostol] p. 28Exercise 10(a)zeneo 15684  zneo 12058  zneoALTV 44050
[Apostol] p. 29Theorem I.35cxpsqrtth 25316  msqsqrtd 14796  resqrtth 14611  sqrtth 14720  sqrtthi 14726  sqsqrtd 14795
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 11633
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12306
[Apostol] p. 361Remarkcrreczi 13590
[Apostol] p. 363Remarkabsgt0i 14755
[Apostol] p. 363Exampleabssubd 14809  abssubi 14759
[ApostolNT] p. 7Remarkfmtno0 43920  fmtno1 43921  fmtno2 43930  fmtno3 43931  fmtno4 43932  fmtno5fac 43962  fmtnofz04prm 43957
[ApostolNT] p. 7Definitiondf-fmtno 43908
[ApostolNT] p. 8Definitiondf-ppi 25681
[ApostolNT] p. 14Definitiondf-dvds 15604
[ApostolNT] p. 14Theorem 1.1(a)iddvds 15619
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 15642
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 15638
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 15632
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 15634
[ApostolNT] p. 14Theorem 1.1(f)1dvds 15620
[ApostolNT] p. 14Theorem 1.1(g)dvds0 15621
[ApostolNT] p. 14Theorem 1.1(h)0dvds 15626
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 15657
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 15659
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 15661
[ApostolNT] p. 15Definitiondf-gcd 15838  dfgcd2 15888
[ApostolNT] p. 16Definitionisprm2 16020
[ApostolNT] p. 16Theorem 1.5coprmdvds 15991
[ApostolNT] p. 16Theorem 1.7prminf 16245
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 15856
[ApostolNT] p. 16Theorem 1.4(b)gcdass 15889
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 15891
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 15870
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 15862
[ApostolNT] p. 17Theorem 1.8coprm 16049
[ApostolNT] p. 17Theorem 1.9euclemma 16051
[ApostolNT] p. 17Theorem 1.101arith2 16258
[ApostolNT] p. 18Theorem 1.13prmrec 16252
[ApostolNT] p. 19Theorem 1.14divalg 15748
[ApostolNT] p. 20Theorem 1.15eucalg 15925
[ApostolNT] p. 24Definitiondf-mu 25682
[ApostolNT] p. 25Definitiondf-phi 16097
[ApostolNT] p. 25Theorem 2.1musum 25772
[ApostolNT] p. 26Theorem 2.2phisum 16121
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16107
[ApostolNT] p. 28Theorem 2.5(c)phimul 16111
[ApostolNT] p. 32Definitiondf-vma 25679
[ApostolNT] p. 32Theorem 2.9muinv 25774
[ApostolNT] p. 32Theorem 2.10vmasum 25796
[ApostolNT] p. 38Remarkdf-sgm 25683
[ApostolNT] p. 38Definitiondf-sgm 25683
[ApostolNT] p. 75Definitiondf-chp 25680  df-cht 25678
[ApostolNT] p. 104Definitioncongr 16002
[ApostolNT] p. 106Remarkdvdsval3 15607
[ApostolNT] p. 106Definitionmoddvds 15614
[ApostolNT] p. 107Example 2mod2eq0even 15691
[ApostolNT] p. 107Example 3mod2eq1n2dvds 15692
[ApostolNT] p. 107Example 4zmod1congr 13256
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13293
[ApostolNT] p. 107Theorem 5.2(c)modexp 13600
[ApostolNT] p. 108Theorem 5.3modmulconst 15637
[ApostolNT] p. 109Theorem 5.4cncongr1 16005
[ApostolNT] p. 109Theorem 5.6gcdmodi 16404
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16007
[ApostolNT] p. 113Theorem 5.17eulerth 16114
[ApostolNT] p. 113Theorem 5.18vfermltl 16132
[ApostolNT] p. 114Theorem 5.19fermltl 16115
[ApostolNT] p. 116Theorem 5.24wilthimp 25653
[ApostolNT] p. 179Definitiondf-lgs 25875  lgsprme0 25919
[ApostolNT] p. 180Example 11lgs 25920
[ApostolNT] p. 180Theorem 9.2lgsvalmod 25896
[ApostolNT] p. 180Theorem 9.3lgsdirprm 25911
[ApostolNT] p. 181Theorem 9.4m1lgs 25968
[ApostolNT] p. 181Theorem 9.52lgs 25987  2lgsoddprm 25996
[ApostolNT] p. 182Theorem 9.6gausslemma2d 25954
[ApostolNT] p. 188Definitiondf-lgs 25875  lgs1 25921
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 25912
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 25914
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 25922
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 25923
[Baer] p. 40Property (b)mapdord 38844
[Baer] p. 40Property (c)mapd11 38845
[Baer] p. 40Property (e)mapdin 38868  mapdlsm 38870
[Baer] p. 40Property (f)mapd0 38871
[Baer] p. 40Definition of projectivitydf-mapd 38831  mapd1o 38854
[Baer] p. 41Property (g)mapdat 38873
[Baer] p. 44Part (1)mapdpg 38912
[Baer] p. 45Part (2)hdmap1eq 39007  mapdheq 38934  mapdheq2 38935  mapdheq2biN 38936
[Baer] p. 45Part (3)baerlem3 38919
[Baer] p. 46Part (4)mapdheq4 38938  mapdheq4lem 38937
[Baer] p. 46Part (5)baerlem5a 38920  baerlem5abmN 38924  baerlem5amN 38922  baerlem5b 38921  baerlem5bmN 38923
[Baer] p. 47Part (6)hdmap1l6 39027  hdmap1l6a 39015  hdmap1l6e 39020  hdmap1l6f 39021  hdmap1l6g 39022  hdmap1l6lem1 39013  hdmap1l6lem2 39014  mapdh6N 38953  mapdh6aN 38941  mapdh6eN 38946  mapdh6fN 38947  mapdh6gN 38948  mapdh6lem1N 38939  mapdh6lem2N 38940
[Baer] p. 48Part 9hdmapval 39034
[Baer] p. 48Part 10hdmap10 39046
[Baer] p. 48Part (6)hdmap1l6h 39023  mapdh6hN 38949
[Baer] p. 48Part (7)mapdh75cN 38959  mapdh75d 38960  mapdh75e 38958  mapdh75fN 38961  mapdh7cN 38955  mapdh7dN 38956  mapdh7eN 38954  mapdh7fN 38957
[Baer] p. 48Part (8)mapdh8 38994  mapdh8a 38981  mapdh8aa 38982  mapdh8ab 38983  mapdh8ac 38984  mapdh8ad 38985  mapdh8b 38986  mapdh8c 38987  mapdh8d 38989  mapdh8d0N 38988  mapdh8e 38990  mapdh8g 38991  mapdh8i 38992  mapdh8j 38993
[Baer] p. 48Part (9)mapdh9a 38995
[Baer] p. 48Equation 10mapdhvmap 38975
[Baer] p. 49Part 12hdmap11 39054  hdmapeq0 39050  hdmapf1oN 39071  hdmapneg 39052  hdmaprnN 39070  hdmaprnlem1N 39055  hdmaprnlem3N 39056  hdmaprnlem3uN 39057  hdmaprnlem4N 39059  hdmaprnlem6N 39060  hdmaprnlem7N 39061  hdmaprnlem8N 39062  hdmaprnlem9N 39063  hdmapsub 39053
[Baer] p. 49Part 14hdmap14lem1 39074  hdmap14lem10 39083  hdmap14lem1a 39072  hdmap14lem2N 39075  hdmap14lem2a 39073  hdmap14lem3 39076  hdmap14lem8 39081  hdmap14lem9 39082
[Baer] p. 50Part 14hdmap14lem11 39084  hdmap14lem12 39085  hdmap14lem13 39086  hdmap14lem14 39087  hdmap14lem15 39088  hgmapval 39093
[Baer] p. 50Part 15hgmapadd 39100  hgmapmul 39101  hgmaprnlem2N 39103  hgmapvs 39097
[Baer] p. 50Part 16hgmaprnN 39107
[Baer] p. 110Lemma 1hdmapip0com 39123
[Baer] p. 110Line 27hdmapinvlem1 39124
[Baer] p. 110Line 28hdmapinvlem2 39125
[Baer] p. 110Line 30hdmapinvlem3 39126
[Baer] p. 110Part 1.2hdmapglem5 39128  hgmapvv 39132
[Baer] p. 110Proposition 1hdmapinvlem4 39127
[Baer] p. 111Line 10hgmapvvlem1 39129
[Baer] p. 111Line 15hdmapg 39136  hdmapglem7 39135
[Bauer], p. 483Theorem 1.22irrexpq 25317  2irrexpqALT 25382
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2655
[BellMachover] p. 460Notationdf-mo 2624
[BellMachover] p. 460Definitionmo3 2649
[BellMachover] p. 461Axiom Extax-ext 2796
[BellMachover] p. 462Theorem 1.1axextmo 2800
[BellMachover] p. 463Axiom Repaxrep5 5182
[BellMachover] p. 463Scheme Sepax-sep 5189
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 34393  bm1.3ii 5192
[BellMachover] p. 466Problemaxpow2 5255
[BellMachover] p. 466Axiom Powaxpow3 5256
[BellMachover] p. 466Axiom Unionaxun2 7453
[BellMachover] p. 468Definitiondf-ord 6181
[BellMachover] p. 469Theorem 2.2(i)ordirr 6196
[BellMachover] p. 469Theorem 2.2(iii)onelon 6203
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6198
[BellMachover] p. 471Definition of Ndf-om 7571
[BellMachover] p. 471Problem 2.5(ii)uniordint 7511
[BellMachover] p. 471Definition of Limdf-lim 6183
[BellMachover] p. 472Axiom Infzfinf2 9096
[BellMachover] p. 473Theorem 2.8limom 7585
[BellMachover] p. 477Equation 3.1df-r1 9184
[BellMachover] p. 478Definitionrankval2 9238
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9202  r1ord3g 9199
[BellMachover] p. 480Axiom Regzfreg 9050
[BellMachover] p. 488Axiom ACac5 9891  dfac4 9540
[BellMachover] p. 490Definition of alephalephval3 9528
[BeltramettiCassinelli] p. 98Remarkatlatmstc 36525
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 30132
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 30174  chirredi 30173
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 30162
[Beran] p. 3Definition of joinsshjval3 29133
[Beran] p. 39Theorem 2.3(i)cmcm2 29395  cmcm2i 29372  cmcm2ii 29377  cmt2N 36456
[Beran] p. 40Theorem 2.3(iii)lecm 29396  lecmi 29381  lecmii 29382
[Beran] p. 45Theorem 3.4cmcmlem 29370
[Beran] p. 49Theorem 4.2cm2j 29399  cm2ji 29404  cm2mi 29405
[Beran] p. 95Definitiondf-sh 28986  issh2 28988
[Beran] p. 95Lemma 3.1(S5)his5 28865
[Beran] p. 95Lemma 3.1(S6)his6 28878
[Beran] p. 95Lemma 3.1(S7)his7 28869
[Beran] p. 95Lemma 3.2(S8)ho01i 29607
[Beran] p. 95Lemma 3.2(S9)hoeq1 29609
[Beran] p. 95Lemma 3.2(S10)ho02i 29608
[Beran] p. 95Lemma 3.2(S11)hoeq2 29610
[Beran] p. 95Postulate (S1)ax-his1 28861  his1i 28879
[Beran] p. 95Postulate (S2)ax-his2 28862
[Beran] p. 95Postulate (S3)ax-his3 28863
[Beran] p. 95Postulate (S4)ax-his4 28864
[Beran] p. 96Definition of normdf-hnorm 28747  dfhnorm2 28901  normval 28903
[Beran] p. 96Definition for Cauchy sequencehcau 28963
[Beran] p. 96Definition of Cauchy sequencedf-hcau 28752
[Beran] p. 96Definition of complete subspaceisch3 29020
[Beran] p. 96Definition of convergedf-hlim 28751  hlimi 28967
[Beran] p. 97Theorem 3.3(i)norm-i-i 28912  norm-i 28908
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 28916  norm-ii 28917  normlem0 28888  normlem1 28889  normlem2 28890  normlem3 28891  normlem4 28892  normlem5 28893  normlem6 28894  normlem7 28895  normlem7tALT 28898
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 28918  norm-iii 28919
[Beran] p. 98Remark 3.4bcs 28960  bcsiALT 28958  bcsiHIL 28959
[Beran] p. 98Remark 3.4(B)normlem9at 28900  normpar 28934  normpari 28933
[Beran] p. 98Remark 3.4(C)normpyc 28925  normpyth 28924  normpythi 28921
[Beran] p. 99Remarklnfn0 29826  lnfn0i 29821  lnop0 29745  lnop0i 29749
[Beran] p. 99Theorem 3.5(i)nmcexi 29805  nmcfnex 29832  nmcfnexi 29830  nmcopex 29808  nmcopexi 29806
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 29833  nmcfnlbi 29831  nmcoplb 29809  nmcoplbi 29807
[Beran] p. 99Theorem 3.5(iii)lnfncon 29835  lnfnconi 29834  lnopcon 29814  lnopconi 29813
[Beran] p. 100Lemma 3.6normpar2i 28935
[Beran] p. 102Theorem 3.7(i)chocunii 29080  pjhth 29172  pjhtheu 29173  pjpjhth 29204  pjpjhthi 29205  pjth 24039
[Beran] p. 102Theorem 3.7(ii)ococ 29185  ococi 29184
[Beran] p. 103Remark 3.8nlelchi 29840
[Beran] p. 104Theorem 3.9riesz3i 29841  riesz4 29843  riesz4i 29842
[Beran] p. 107Definitiondf-ch 29000  isch2 29002
[Beran] p. 107Remark 3.12choccl 29085  isch3 29020  occl 29083  ocsh 29062  shoccl 29084  shocsh 29063
[Beran] p. 107Remark 3.12(B)ococin 29187
[Beran] p. 108Theorem 3.13chintcl 29111
[Beran] p. 109Property (ii)pjidmco 29960  pjidmcoi 29956  pjidmi 29452
[Beran] p. 110Definition of projector orderingpjordi 29952
[Beran] p. 111Remarkho0val 29529  pjch1 29449
[Beran] p. 111Definitiondf-hfmul 29513  df-hfsum 29512  df-hodif 29511  df-homul 29510  df-hosum 29509
[Beran] p. 111Lemma 4.4(i)pjo 29450
[Beran] p. 111Lemma 4.4(ii)pjch 29473  pjchi 29211
[Beran] p. 111Lemma 4.4(iii)pjoc2 29218  pjoc2i 29217
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 29459
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 29944  pjssmii 29460
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 29943
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 29942
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 29947
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 29945  pjssge0ii 29461
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 29946  pjdifnormii 29462
[Bobzien] p. 116Statement T3stoic3 1778
[Bobzien] p. 117Statement T2stoic2a 1776
[Bobzien] p. 117Statement T4stoic4a 1779
[Bobzien] p. 117Conclusion the contradictorystoic1a 1774
[Bogachev] p. 16Definition 1.5df-oms 31575
[Bogachev] p. 17Example 1.5.2omsmon 31581
[Bogachev] p. 41Definition 1.11.2df-carsg 31585
[Bogachev] p. 42Theorem 1.11.4carsgsiga 31605
[Bogachev] p. 116Definition 2.3.1df-itgm 31636  df-sitm 31614
[Bogachev] p. 118Chapter 2.4.4df-itgm 31636
[Bogachev] p. 118Definition 2.4.1df-sitg 31613
[Bollobas] p. 1Section I.1df-edg 26837  isuhgrop 26859  isusgrop 26951  isuspgrop 26950
[Bollobas] p. 2Section I.1df-subgr 27054  uhgrspan1 27089  uhgrspansubgr 27077
[Bollobas] p. 3Definitionisomuspgr 44215
[Bollobas] p. 3Section I.1cusgrsize 27240  df-cusgr 27198  df-nbgr 27119  fusgrmaxsize 27250
[Bollobas] p. 4Definitiondf-upwlks 44225  df-wlks 27385
[Bollobas] p. 4Section I.1finsumvtxdg2size 27336  finsumvtxdgeven 27338  fusgr1th 27337  fusgrvtxdgonume 27340  vtxdgoddnumeven 27339
[Bollobas] p. 5Notationdf-pths 27501
[Bollobas] p. 5Definitiondf-crcts 27571  df-cycls 27572  df-trls 27478  df-wlkson 27386
[Bollobas] p. 7Section I.1df-ushgr 26848
[BourbakiAlg1] p. 1Definition 1df-clintop 44323  df-cllaw 44309  df-mgm 17848  df-mgm2 44342
[BourbakiAlg1] p. 4Definition 5df-assintop 44324  df-asslaw 44311  df-sgrp 17897  df-sgrp2 44344
[BourbakiAlg1] p. 7Definition 8df-cmgm2 44343  df-comlaw 44310
[BourbakiAlg1] p. 12Definition 2df-mnd 17908
[BourbakiAlg1] p. 92Definition 1df-ring 19295
[BourbakiAlg1] p. 93Section I.8.1df-rng0 44362
[BourbakiEns] p. Proposition 8fcof1 7032  fcofo 7033
[BourbakiTop1] p. Remarkxnegmnf 12596  xnegpnf 12595
[BourbakiTop1] p. Remark rexneg 12597
[BourbakiTop1] p. Remark 3ust0 22821  ustfilxp 22814
[BourbakiTop1] p. Axiom GT'tgpsubcn 22691
[BourbakiTop1] p. Criterionishmeo 22360
[BourbakiTop1] p. Example 1cstucnd 22886  iducn 22885  snfil 22465
[BourbakiTop1] p. Example 2neifil 22481
[BourbakiTop1] p. Theorem 1cnextcn 22668
[BourbakiTop1] p. Theorem 2ucnextcn 22906
[BourbakiTop1] p. Theorem 3df-hcmp 31225
[BourbakiTop1] p. Paragraph 3infil 22464
[BourbakiTop1] p. Definition 1df-ucn 22878  df-ust 22802  filintn0 22462  filn0 22463  istgp 22678  ucnprima 22884
[BourbakiTop1] p. Definition 2df-cfilu 22889
[BourbakiTop1] p. Definition 3df-cusp 22900  df-usp 22859  df-utop 22833  trust 22831
[BourbakiTop1] p. Definition 6df-pcmp 31148
[BourbakiTop1] p. Property V_issnei2 21717
[BourbakiTop1] p. Theorem 1(d)iscncl 21870
[BourbakiTop1] p. Condition F_Iustssel 22807
[BourbakiTop1] p. Condition U_Iustdiag 22810
[BourbakiTop1] p. Property V_iiinnei 21726
[BourbakiTop1] p. Property V_ivneiptopreu 21734  neissex 21728
[BourbakiTop1] p. Proposition 1neips 21714  neiss 21710  ucncn 22887  ustund 22823  ustuqtop 22848
[BourbakiTop1] p. Proposition 2cnpco 21868  neiptopreu 21734  utop2nei 22852  utop3cls 22853
[BourbakiTop1] p. Proposition 3fmucnd 22894  uspreg 22876  utopreg 22854
[BourbakiTop1] p. Proposition 4imasncld 22292  imasncls 22293  imasnopn 22291
[BourbakiTop1] p. Proposition 9cnpflf2 22601
[BourbakiTop1] p. Condition F_IIustincl 22809
[BourbakiTop1] p. Condition U_IIustinvel 22811
[BourbakiTop1] p. Property V_iiielnei 21712
[BourbakiTop1] p. Proposition 11cnextucn 22905
[BourbakiTop1] p. Condition F_IIbustbasel 22808
[BourbakiTop1] p. Condition U_IIIustexhalf 22812
[BourbakiTop1] p. Definition C'''df-cmp 21988
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 22447
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 21495
[BourbakiTop2] p. 195Definition 1df-ldlf 31145
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 42567
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 42569  stoweid 42568
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 42506  stoweidlem10 42515  stoweidlem14 42519  stoweidlem15 42520  stoweidlem35 42540  stoweidlem36 42541  stoweidlem37 42542  stoweidlem38 42543  stoweidlem40 42545  stoweidlem41 42546  stoweidlem43 42548  stoweidlem44 42549  stoweidlem46 42551  stoweidlem5 42510  stoweidlem50 42555  stoweidlem52 42557  stoweidlem53 42558  stoweidlem55 42560  stoweidlem56 42561
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 42528  stoweidlem24 42529  stoweidlem27 42532  stoweidlem28 42533  stoweidlem30 42535
[BrosowskiDeutsh] p. 91Proofstoweidlem34 42539  stoweidlem59 42564  stoweidlem60 42565
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 42550  stoweidlem49 42554  stoweidlem7 42512
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 42536  stoweidlem39 42544  stoweidlem42 42547  stoweidlem48 42553  stoweidlem51 42556  stoweidlem54 42559  stoweidlem57 42562  stoweidlem58 42563
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 42530
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 42522
[BrosowskiDeutsh] p. 92Proofstoweidlem11 42516  stoweidlem13 42518  stoweidlem26 42531  stoweidlem61 42566
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 42523
[Bruck] p. 1Section I.1df-clintop 44323  df-mgm 17848  df-mgm2 44342
[Bruck] p. 23Section II.1df-sgrp 17897  df-sgrp2 44344
[Bruck] p. 28Theorem 3.2dfgrp3 18194
[ChoquetDD] p. 2Definition of mappingdf-mpt 5133
[Church] p. 129Section II.24df-ifp 1059  dfifp2 1060
[Clemente] p. 10Definition ITnatded 28184
[Clemente] p. 10Definition I` `m,nnatded 28184
[Clemente] p. 11Definition E=>m,nnatded 28184
[Clemente] p. 11Definition I=>m,nnatded 28184
[Clemente] p. 11Definition E` `(1)natded 28184
[Clemente] p. 11Definition E` `(2)natded 28184
[Clemente] p. 12Definition E` `m,n,pnatded 28184
[Clemente] p. 12Definition I` `n(1)natded 28184
[Clemente] p. 12Definition I` `n(2)natded 28184
[Clemente] p. 13Definition I` `m,n,pnatded 28184
[Clemente] p. 14Proof 5.11natded 28184
[Clemente] p. 14Definition E` `nnatded 28184
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 28186  ex-natded5.2 28185
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 28189  ex-natded5.3 28188
[Clemente] p. 18Theorem 5.5ex-natded5.5 28191
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 28193  ex-natded5.7 28192
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 28195  ex-natded5.8 28194
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 28197  ex-natded5.13 28196
[Clemente] p. 32Definition I` `nnatded 28184
[Clemente] p. 32Definition E` `m,n,p,anatded 28184
[Clemente] p. 32Definition E` `n,tnatded 28184
[Clemente] p. 32Definition I` `n,tnatded 28184
[Clemente] p. 43Theorem 9.20ex-natded9.20 28198
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 28199
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 28201  ex-natded9.26 28200
[Cohen] p. 301Remarkrelogoprlem 25178
[Cohen] p. 301Property 2relogmul 25179  relogmuld 25212
[Cohen] p. 301Property 3relogdiv 25180  relogdivd 25213
[Cohen] p. 301Property 4relogexp 25183
[Cohen] p. 301Property 1alog1 25173
[Cohen] p. 301Property 1bloge 25174
[Cohen4] p. 348Observationrelogbcxpb 25369
[Cohen4] p. 349Propertyrelogbf 25373
[Cohen4] p. 352Definitionelogb 25352
[Cohen4] p. 361Property 2relogbmul 25359
[Cohen4] p. 361Property 3logbrec 25364  relogbdiv 25361
[Cohen4] p. 361Property 4relogbreexp 25357
[Cohen4] p. 361Property 6relogbexp 25362
[Cohen4] p. 361Property 1(a)logbid1 25350
[Cohen4] p. 361Property 1(b)logb1 25351
[Cohen4] p. 367Propertylogbchbase 25353
[Cohen4] p. 377Property 2logblt 25366
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 31568  sxbrsigalem4 31570
[Cohn] p. 81Section II.5acsdomd 17787  acsinfd 17786  acsinfdimd 17788  acsmap2d 17785  acsmapd 17784
[Cohn] p. 143Example 5.1.1sxbrsiga 31573
[Connell] p. 57Definitiondf-scmat 21093  df-scmatalt 44670
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13229
[Crawley] p. 1Definition of posetdf-poset 17552
[Crawley] p. 107Theorem 13.2hlsupr 36592
[Crawley] p. 110Theorem 13.3arglem1N 37396  dalaw 37092
[Crawley] p. 111Theorem 13.4hlathil 39167
[Crawley] p. 111Definition of set Wdf-watsN 37196
[Crawley] p. 111Definition of dilationdf-dilN 37312  df-ldil 37310  isldil 37316
[Crawley] p. 111Definition of translationdf-ltrn 37311  df-trnN 37313  isltrn 37325  ltrnu 37327
[Crawley] p. 112Lemma Acdlema1N 36997  cdlema2N 36998  exatleN 36610
[Crawley] p. 112Lemma B1cvrat 36682  cdlemb 37000  cdlemb2 37247  cdlemb3 37812  idltrn 37356  l1cvat 36261  lhpat 37249  lhpat2 37251  lshpat 36262  ltrnel 37345  ltrnmw 37357
[Crawley] p. 112Lemma Ccdlemc1 37397  cdlemc2 37398  ltrnnidn 37380  trlat 37375  trljat1 37372  trljat2 37373  trljat3 37374  trlne 37391  trlnidat 37379  trlnle 37392
[Crawley] p. 112Definition of automorphismdf-pautN 37197
[Crawley] p. 113Lemma Ccdlemc 37403  cdlemc3 37399  cdlemc4 37400
[Crawley] p. 113Lemma Dcdlemd 37413  cdlemd1 37404  cdlemd2 37405  cdlemd3 37406  cdlemd4 37407  cdlemd5 37408  cdlemd6 37409  cdlemd7 37410  cdlemd8 37411  cdlemd9 37412  cdleme31sde 37591  cdleme31se 37588  cdleme31se2 37589  cdleme31snd 37592  cdleme32a 37647  cdleme32b 37648  cdleme32c 37649  cdleme32d 37650  cdleme32e 37651  cdleme32f 37652  cdleme32fva 37643  cdleme32fva1 37644  cdleme32fvcl 37646  cdleme32le 37653  cdleme48fv 37705  cdleme4gfv 37713  cdleme50eq 37747  cdleme50f 37748  cdleme50f1 37749  cdleme50f1o 37752  cdleme50laut 37753  cdleme50ldil 37754  cdleme50lebi 37746  cdleme50rn 37751  cdleme50rnlem 37750  cdlemeg49le 37717  cdlemeg49lebilem 37745
[Crawley] p. 113Lemma Ecdleme 37766  cdleme00a 37415  cdleme01N 37427  cdleme02N 37428  cdleme0a 37417  cdleme0aa 37416  cdleme0b 37418  cdleme0c 37419  cdleme0cp 37420  cdleme0cq 37421  cdleme0dN 37422  cdleme0e 37423  cdleme0ex1N 37429  cdleme0ex2N 37430  cdleme0fN 37424  cdleme0gN 37425  cdleme0moN 37431  cdleme1 37433  cdleme10 37460  cdleme10tN 37464  cdleme11 37476  cdleme11a 37466  cdleme11c 37467  cdleme11dN 37468  cdleme11e 37469  cdleme11fN 37470  cdleme11g 37471  cdleme11h 37472  cdleme11j 37473  cdleme11k 37474  cdleme11l 37475  cdleme12 37477  cdleme13 37478  cdleme14 37479  cdleme15 37484  cdleme15a 37480  cdleme15b 37481  cdleme15c 37482  cdleme15d 37483  cdleme16 37491  cdleme16aN 37465  cdleme16b 37485  cdleme16c 37486  cdleme16d 37487  cdleme16e 37488  cdleme16f 37489  cdleme16g 37490  cdleme19a 37509  cdleme19b 37510  cdleme19c 37511  cdleme19d 37512  cdleme19e 37513  cdleme19f 37514  cdleme1b 37432  cdleme2 37434  cdleme20aN 37515  cdleme20bN 37516  cdleme20c 37517  cdleme20d 37518  cdleme20e 37519  cdleme20f 37520  cdleme20g 37521  cdleme20h 37522  cdleme20i 37523  cdleme20j 37524  cdleme20k 37525  cdleme20l 37528  cdleme20l1 37526  cdleme20l2 37527  cdleme20m 37529  cdleme20y 37508  cdleme20zN 37507  cdleme21 37543  cdleme21d 37536  cdleme21e 37537  cdleme22a 37546  cdleme22aa 37545  cdleme22b 37547  cdleme22cN 37548  cdleme22d 37549  cdleme22e 37550  cdleme22eALTN 37551  cdleme22f 37552  cdleme22f2 37553  cdleme22g 37554  cdleme23a 37555  cdleme23b 37556  cdleme23c 37557  cdleme26e 37565  cdleme26eALTN 37567  cdleme26ee 37566  cdleme26f 37569  cdleme26f2 37571  cdleme26f2ALTN 37570  cdleme26fALTN 37568  cdleme27N 37575  cdleme27a 37573  cdleme27cl 37572  cdleme28c 37578  cdleme3 37443  cdleme30a 37584  cdleme31fv 37596  cdleme31fv1 37597  cdleme31fv1s 37598  cdleme31fv2 37599  cdleme31id 37600  cdleme31sc 37590  cdleme31sdnN 37593  cdleme31sn 37586  cdleme31sn1 37587  cdleme31sn1c 37594  cdleme31sn2 37595  cdleme31so 37585  cdleme35a 37654  cdleme35b 37656  cdleme35c 37657  cdleme35d 37658  cdleme35e 37659  cdleme35f 37660  cdleme35fnpq 37655  cdleme35g 37661  cdleme35h 37662  cdleme35h2 37663  cdleme35sn2aw 37664  cdleme35sn3a 37665  cdleme36a 37666  cdleme36m 37667  cdleme37m 37668  cdleme38m 37669  cdleme38n 37670  cdleme39a 37671  cdleme39n 37672  cdleme3b 37435  cdleme3c 37436  cdleme3d 37437  cdleme3e 37438  cdleme3fN 37439  cdleme3fa 37442  cdleme3g 37440  cdleme3h 37441  cdleme4 37444  cdleme40m 37673  cdleme40n 37674  cdleme40v 37675  cdleme40w 37676  cdleme41fva11 37683  cdleme41sn3aw 37680  cdleme41sn4aw 37681  cdleme41snaw 37682  cdleme42a 37677  cdleme42b 37684  cdleme42c 37678  cdleme42d 37679  cdleme42e 37685  cdleme42f 37686  cdleme42g 37687  cdleme42h 37688  cdleme42i 37689  cdleme42k 37690  cdleme42ke 37691  cdleme42keg 37692  cdleme42mN 37693  cdleme42mgN 37694  cdleme43aN 37695  cdleme43bN 37696  cdleme43cN 37697  cdleme43dN 37698  cdleme5 37446  cdleme50ex 37765  cdleme50ltrn 37763  cdleme51finvN 37762  cdleme51finvfvN 37761  cdleme51finvtrN 37764  cdleme6 37447  cdleme7 37455  cdleme7a 37449  cdleme7aa 37448  cdleme7b 37450  cdleme7c 37451  cdleme7d 37452  cdleme7e 37453  cdleme7ga 37454  cdleme8 37456  cdleme8tN 37461  cdleme9 37459  cdleme9a 37457  cdleme9b 37458  cdleme9tN 37463  cdleme9taN 37462  cdlemeda 37504  cdlemedb 37503  cdlemednpq 37505  cdlemednuN 37506  cdlemefr27cl 37609  cdlemefr32fva1 37616  cdlemefr32fvaN 37615  cdlemefrs32fva 37606  cdlemefrs32fva1 37607  cdlemefs27cl 37619  cdlemefs32fva1 37629  cdlemefs32fvaN 37628  cdlemesner 37502  cdlemeulpq 37426
[Crawley] p. 114Lemma E4atex 37282  4atexlem7 37281  cdleme0nex 37496  cdleme17a 37492  cdleme17c 37494  cdleme17d 37704  cdleme17d1 37495  cdleme17d2 37701  cdleme18a 37497  cdleme18b 37498  cdleme18c 37499  cdleme18d 37501  cdleme4a 37445
[Crawley] p. 115Lemma Ecdleme21a 37531  cdleme21at 37534  cdleme21b 37532  cdleme21c 37533  cdleme21ct 37535  cdleme21f 37538  cdleme21g 37539  cdleme21h 37540  cdleme21i 37541  cdleme22gb 37500
[Crawley] p. 116Lemma Fcdlemf 37769  cdlemf1 37767  cdlemf2 37768
[Crawley] p. 116Lemma Gcdlemftr1 37773  cdlemg16 37863  cdlemg28 37910  cdlemg28a 37899  cdlemg28b 37909  cdlemg3a 37803  cdlemg42 37935  cdlemg43 37936  cdlemg44 37939  cdlemg44a 37937  cdlemg46 37941  cdlemg47 37942  cdlemg9 37840  ltrnco 37925  ltrncom 37944  tgrpabl 37957  trlco 37933
[Crawley] p. 116Definition of Gdf-tgrp 37949
[Crawley] p. 117Lemma Gcdlemg17 37883  cdlemg17b 37868
[Crawley] p. 117Definition of Edf-edring-rN 37962  df-edring 37963
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 37966
[Crawley] p. 118Remarktendopltp 37986
[Crawley] p. 118Lemma Hcdlemh 38023  cdlemh1 38021  cdlemh2 38022
[Crawley] p. 118Lemma Icdlemi 38026  cdlemi1 38024  cdlemi2 38025
[Crawley] p. 118Lemma Jcdlemj1 38027  cdlemj2 38028  cdlemj3 38029  tendocan 38030
[Crawley] p. 118Lemma Kcdlemk 38180  cdlemk1 38037  cdlemk10 38049  cdlemk11 38055  cdlemk11t 38152  cdlemk11ta 38135  cdlemk11tb 38137  cdlemk11tc 38151  cdlemk11u-2N 38095  cdlemk11u 38077  cdlemk12 38056  cdlemk12u-2N 38096  cdlemk12u 38078  cdlemk13-2N 38082  cdlemk13 38058  cdlemk14-2N 38084  cdlemk14 38060  cdlemk15-2N 38085  cdlemk15 38061  cdlemk16-2N 38086  cdlemk16 38063  cdlemk16a 38062  cdlemk17-2N 38087  cdlemk17 38064  cdlemk18-2N 38092  cdlemk18-3N 38106  cdlemk18 38074  cdlemk19-2N 38093  cdlemk19 38075  cdlemk19u 38176  cdlemk1u 38065  cdlemk2 38038  cdlemk20-2N 38098  cdlemk20 38080  cdlemk21-2N 38097  cdlemk21N 38079  cdlemk22-3 38107  cdlemk22 38099  cdlemk23-3 38108  cdlemk24-3 38109  cdlemk25-3 38110  cdlemk26-3 38112  cdlemk26b-3 38111  cdlemk27-3 38113  cdlemk28-3 38114  cdlemk29-3 38117  cdlemk3 38039  cdlemk30 38100  cdlemk31 38102  cdlemk32 38103  cdlemk33N 38115  cdlemk34 38116  cdlemk35 38118  cdlemk36 38119  cdlemk37 38120  cdlemk38 38121  cdlemk39 38122  cdlemk39u 38174  cdlemk4 38040  cdlemk41 38126  cdlemk42 38147  cdlemk42yN 38150  cdlemk43N 38169  cdlemk45 38153  cdlemk46 38154  cdlemk47 38155  cdlemk48 38156  cdlemk49 38157  cdlemk5 38042  cdlemk50 38158  cdlemk51 38159  cdlemk52 38160  cdlemk53 38163  cdlemk54 38164  cdlemk55 38167  cdlemk55u 38172  cdlemk56 38177  cdlemk5a 38041  cdlemk5auN 38066  cdlemk5u 38067  cdlemk6 38043  cdlemk6u 38068  cdlemk7 38054  cdlemk7u-2N 38094  cdlemk7u 38076  cdlemk8 38044  cdlemk9 38045  cdlemk9bN 38046  cdlemki 38047  cdlemkid 38142  cdlemkj-2N 38088  cdlemkj 38069  cdlemksat 38052  cdlemksel 38051  cdlemksv 38050  cdlemksv2 38053  cdlemkuat 38072  cdlemkuel-2N 38090  cdlemkuel-3 38104  cdlemkuel 38071  cdlemkuv-2N 38089  cdlemkuv2-2 38091  cdlemkuv2-3N 38105  cdlemkuv2 38073  cdlemkuvN 38070  cdlemkvcl 38048  cdlemky 38132  cdlemkyyN 38168  tendoex 38181
[Crawley] p. 120Remarkdva1dim 38191
[Crawley] p. 120Lemma Lcdleml1N 38182  cdleml2N 38183  cdleml3N 38184  cdleml4N 38185  cdleml5N 38186  cdleml6 38187  cdleml7 38188  cdleml8 38189  cdleml9 38190  dia1dim 38267
[Crawley] p. 120Lemma Mdia11N 38254  diaf11N 38255  dialss 38252  diaord 38253  dibf11N 38367  djajN 38343
[Crawley] p. 120Definition of isomorphism mapdiaval 38238
[Crawley] p. 121Lemma Mcdlemm10N 38324  dia2dimlem1 38270  dia2dimlem2 38271  dia2dimlem3 38272  dia2dimlem4 38273  dia2dimlem5 38274  diaf1oN 38336  diarnN 38335  dvheveccl 38318  dvhopN 38322
[Crawley] p. 121Lemma Ncdlemn 38418  cdlemn10 38412  cdlemn11 38417  cdlemn11a 38413  cdlemn11b 38414  cdlemn11c 38415  cdlemn11pre 38416  cdlemn2 38401  cdlemn2a 38402  cdlemn3 38403  cdlemn4 38404  cdlemn4a 38405  cdlemn5 38407  cdlemn5pre 38406  cdlemn6 38408  cdlemn7 38409  cdlemn8 38410  cdlemn9 38411  diclspsn 38400
[Crawley] p. 121Definition of phi(q)df-dic 38379
[Crawley] p. 122Lemma Ndih11 38471  dihf11 38473  dihjust 38423  dihjustlem 38422  dihord 38470  dihord1 38424  dihord10 38429  dihord11b 38428  dihord11c 38430  dihord2 38433  dihord2a 38425  dihord2b 38426  dihord2cN 38427  dihord2pre 38431  dihord2pre2 38432  dihordlem6 38419  dihordlem7 38420  dihordlem7b 38421
[Crawley] p. 122Definition of isomorphism mapdihffval 38436  dihfval 38437  dihval 38438
[Diestel] p. 3Section 1.1df-cusgr 27198  df-nbgr 27119
[Diestel] p. 4Section 1.1df-subgr 27054  uhgrspan1 27089  uhgrspansubgr 27077
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 27340  vtxdgoddnumeven 27339
[Diestel] p. 27Section 1.10df-ushgr 26848
[Eisenberg] p. 67Definition 5.3df-dif 3922
[Eisenberg] p. 82Definition 6.3dfom3 9101
[Eisenberg] p. 125Definition 8.21df-map 8398
[Eisenberg] p. 216Example 13.2(4)omenps 9109
[Eisenberg] p. 310Theorem 19.8cardprc 9400
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 9969
[Enderton] p. 18Axiom of Empty Setaxnul 5195
[Enderton] p. 19Definitiondf-tp 4554
[Enderton] p. 26Exercise 5unissb 4856
[Enderton] p. 26Exercise 10pwel 5269
[Enderton] p. 28Exercise 7(b)pwun 5445
[Enderton] p. 30Theorem "Distributive laws"iinin1 4987  iinin2 4986  iinun2 4981  iunin1 4980  iunin1f 30313  iunin2 4979  uniin1 30307  uniin2 30308
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4985  iundif2 4982
[Enderton] p. 32Exercise 20unineq 4238
[Enderton] p. 33Exercise 23iinuni 5006
[Enderton] p. 33Exercise 25iununi 5007
[Enderton] p. 33Exercise 24(a)iinpw 5014
[Enderton] p. 33Exercise 24(b)iunpw 7483  iunpwss 5015
[Enderton] p. 36Definitionopthwiener 5391
[Enderton] p. 38Exercise 6(a)unipw 5330
[Enderton] p. 38Exercise 6(b)pwuni 4861
[Enderton] p. 41Lemma 3Dopeluu 5349  rnex 7607  rnexg 7604
[Enderton] p. 41Exercise 8dmuni 5770  rnuni 5994
[Enderton] p. 42Definition of a functiondffun7 6370  dffun8 6371
[Enderton] p. 43Definition of function valuefunfv2 6739
[Enderton] p. 43Definition of single-rootedfuncnv 6411
[Enderton] p. 44Definition (d)dfima2 5918  dfima3 5919
[Enderton] p. 47Theorem 3Hfvco2 6746
[Enderton] p. 49Axiom of Choice (first form)ac7 9887  ac7g 9888  df-ac 9534  dfac2 9549  dfac2a 9547  dfac2b 9548  dfac3 9539  dfac7 9550
[Enderton] p. 50Theorem 3K(a)imauni 6994
[Enderton] p. 52Definitiondf-map 8398
[Enderton] p. 53Exercise 21coass 6105
[Enderton] p. 53Exercise 27dmco 6094
[Enderton] p. 53Exercise 14(a)funin 6418
[Enderton] p. 53Exercise 22(a)imass2 5952
[Enderton] p. 54Remarkixpf 8474  ixpssmap 8486
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8452
[Enderton] p. 55Axiom of Choice (second form)ac9 9897  ac9s 9907
[Enderton] p. 56Theorem 3Meqvrelref 35915  erref 8299
[Enderton] p. 57Lemma 3Neqvrelthi 35918  erthi 8330
[Enderton] p. 57Definitiondf-ec 8281
[Enderton] p. 58Definitiondf-qs 8285
[Enderton] p. 61Exercise 35df-ec 8281
[Enderton] p. 65Exercise 56(a)dmun 5766
[Enderton] p. 68Definition of successordf-suc 6184
[Enderton] p. 71Definitiondf-tr 5159  dftr4 5163
[Enderton] p. 72Theorem 4Eunisuc 6254
[Enderton] p. 73Exercise 6unisuc 6254
[Enderton] p. 73Exercise 5(a)truni 5172
[Enderton] p. 73Exercise 5(b)trint 5174  trintALT 41444
[Enderton] p. 79Theorem 4I(A1)nna0 8220
[Enderton] p. 79Theorem 4I(A2)nnasuc 8222  onasuc 8143
[Enderton] p. 79Definition of operation valuedf-ov 7148
[Enderton] p. 80Theorem 4J(A1)nnm0 8221
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8223  onmsuc 8144
[Enderton] p. 81Theorem 4K(1)nnaass 8238
[Enderton] p. 81Theorem 4K(2)nna0r 8225  nnacom 8233
[Enderton] p. 81Theorem 4K(3)nndi 8239
[Enderton] p. 81Theorem 4K(4)nnmass 8240
[Enderton] p. 81Theorem 4K(5)nnmcom 8242
[Enderton] p. 82Exercise 16nnm0r 8226  nnmsucr 8241
[Enderton] p. 88Exercise 23nnaordex 8254
[Enderton] p. 129Definitiondf-en 8500
[Enderton] p. 132Theorem 6B(b)canth 7100
[Enderton] p. 133Exercise 1xpomen 9433
[Enderton] p. 133Exercise 2qnnen 15562
[Enderton] p. 134Theorem (Pigeonhole Principle)php 8692
[Enderton] p. 135Corollary 6Cphp3 8694
[Enderton] p. 136Corollary 6Enneneq 8691
[Enderton] p. 136Corollary 6D(a)pssinf 8719
[Enderton] p. 136Corollary 6D(b)ominf 8721
[Enderton] p. 137Lemma 6Fpssnn 8727
[Enderton] p. 138Corollary 6Gssfi 8729
[Enderton] p. 139Theorem 6H(c)mapen 8672
[Enderton] p. 142Theorem 6I(3)xpdjuen 9597
[Enderton] p. 142Theorem 6I(4)mapdjuen 9598
[Enderton] p. 143Theorem 6Jdju0en 9593  dju1en 9589
[Enderton] p. 144Exercise 13iunfi 8803  unifi 8804  unifi2 8805
[Enderton] p. 144Corollary 6Kundif2 4407  unfi 8776  unfi2 8778
[Enderton] p. 145Figure 38ffoss 7637
[Enderton] p. 145Definitiondf-dom 8501
[Enderton] p. 146Example 1domen 8512  domeng 8513
[Enderton] p. 146Example 3nndomo 8704  nnsdom 9108  nnsdomg 8768
[Enderton] p. 149Theorem 6L(a)djudom2 9601
[Enderton] p. 149Theorem 6L(c)mapdom1 8673  xpdom1 8606  xpdom1g 8604  xpdom2g 8603
[Enderton] p. 149Theorem 6L(d)mapdom2 8679
[Enderton] p. 151Theorem 6Mzorn 9921  zorng 9918
[Enderton] p. 151Theorem 6M(4)ac8 9906  dfac5 9546
[Enderton] p. 159Theorem 6Qunictb 9989
[Enderton] p. 164Exampleinfdif 9623
[Enderton] p. 168Definitiondf-po 5461
[Enderton] p. 192Theorem 7M(a)oneli 6285
[Enderton] p. 192Theorem 7M(b)ontr1 6224
[Enderton] p. 192Theorem 7M(c)onirri 6284
[Enderton] p. 193Corollary 7N(b)0elon 6231
[Enderton] p. 193Corollary 7N(c)onsuci 7543
[Enderton] p. 193Corollary 7N(d)ssonunii 7492
[Enderton] p. 194Remarkonprc 7489
[Enderton] p. 194Exercise 16suc11 6281
[Enderton] p. 197Definitiondf-card 9359
[Enderton] p. 197Theorem 7Pcarden 9965
[Enderton] p. 200Exercise 25tfis 7559
[Enderton] p. 202Lemma 7Tr1tr 9196
[Enderton] p. 202Definitiondf-r1 9184
[Enderton] p. 202Theorem 7Qr1val1 9206
[Enderton] p. 204Theorem 7V(b)rankval4 9287
[Enderton] p. 206Theorem 7X(b)en2lp 9060
[Enderton] p. 207Exercise 30rankpr 9277  rankprb 9271  rankpw 9263  rankpwi 9243  rankuniss 9286
[Enderton] p. 207Exercise 34opthreg 9072
[Enderton] p. 208Exercise 35suc11reg 9073
[Enderton] p. 212Definition of alephalephval3 9528
[Enderton] p. 213Theorem 8A(a)alephord2 9494
[Enderton] p. 213Theorem 8A(b)cardalephex 9508
[Enderton] p. 218Theorem Schema 8Eonfununi 7968
[Enderton] p. 222Definition of kardkarden 9315  kardex 9314
[Enderton] p. 238Theorem 8Roeoa 8213
[Enderton] p. 238Theorem 8Soeoe 8215
[Enderton] p. 240Exercise 25oarec 8178
[Enderton] p. 257Definition of cofinalitycflm 9664
[FaureFrolicher] p. 57Definition 3.1.9mreexd 16909
[FaureFrolicher] p. 83Definition 4.1.1df-mri 16855
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 17783  mrieqv2d 16906  mrieqvd 16905
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 16910
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 16915  mreexexlem2d 16912
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 17789  mreexfidimd 16917
[Frege1879] p. 11Statementdf3or2 40322
[Frege1879] p. 12Statementdf3an2 40323  dfxor4 40320  dfxor5 40321
[Frege1879] p. 26Axiom 1ax-frege1 40345
[Frege1879] p. 26Axiom 2ax-frege2 40346
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 40350
[Frege1879] p. 31Proposition 4frege4 40354
[Frege1879] p. 32Proposition 5frege5 40355
[Frege1879] p. 33Proposition 6frege6 40361
[Frege1879] p. 34Proposition 7frege7 40363
[Frege1879] p. 35Axiom 8ax-frege8 40364  axfrege8 40362
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 34774
[Frege1879] p. 35Proposition 9frege9 40367
[Frege1879] p. 36Proposition 10frege10 40375
[Frege1879] p. 36Proposition 11frege11 40369
[Frege1879] p. 37Proposition 12frege12 40368
[Frege1879] p. 37Proposition 13frege13 40377
[Frege1879] p. 37Proposition 14frege14 40378
[Frege1879] p. 38Proposition 15frege15 40381
[Frege1879] p. 38Proposition 16frege16 40371
[Frege1879] p. 39Proposition 17frege17 40376
[Frege1879] p. 39Proposition 18frege18 40373
[Frege1879] p. 39Proposition 19frege19 40379
[Frege1879] p. 40Proposition 20frege20 40383
[Frege1879] p. 40Proposition 21frege21 40382
[Frege1879] p. 41Proposition 22frege22 40374
[Frege1879] p. 42Proposition 23frege23 40380
[Frege1879] p. 42Proposition 24frege24 40370
[Frege1879] p. 42Proposition 25frege25 40372  rp-frege25 40360
[Frege1879] p. 42Proposition 26frege26 40365
[Frege1879] p. 43Axiom 28ax-frege28 40385
[Frege1879] p. 43Proposition 27frege27 40366
[Frege1879] p. 43Proposition 28con3 156
[Frege1879] p. 43Proposition 29frege29 40386
[Frege1879] p. 44Axiom 31ax-frege31 40389  axfrege31 40388
[Frege1879] p. 44Proposition 30frege30 40387
[Frege1879] p. 44Proposition 31notnotr 132
[Frege1879] p. 44Proposition 32frege32 40390
[Frege1879] p. 44Proposition 33frege33 40391
[Frege1879] p. 45Proposition 34frege34 40392
[Frege1879] p. 45Proposition 35frege35 40393
[Frege1879] p. 45Proposition 36frege36 40394
[Frege1879] p. 46Proposition 37frege37 40395
[Frege1879] p. 46Proposition 38frege38 40396
[Frege1879] p. 46Proposition 39frege39 40397
[Frege1879] p. 46Proposition 40frege40 40398
[Frege1879] p. 47Axiom 41ax-frege41 40400  axfrege41 40399
[Frege1879] p. 47Proposition 41notnot 144
[Frege1879] p. 47Proposition 42frege42 40401
[Frege1879] p. 47Proposition 43frege43 40402
[Frege1879] p. 47Proposition 44frege44 40403
[Frege1879] p. 47Proposition 45frege45 40404
[Frege1879] p. 48Proposition 46frege46 40405
[Frege1879] p. 48Proposition 47frege47 40406
[Frege1879] p. 49Proposition 48frege48 40407
[Frege1879] p. 49Proposition 49frege49 40408
[Frege1879] p. 49Proposition 50frege50 40409
[Frege1879] p. 50Axiom 52ax-frege52a 40412  ax-frege52c 40443  frege52aid 40413  frege52b 40444
[Frege1879] p. 50Axiom 54ax-frege54a 40417  ax-frege54c 40447  frege54b 40448
[Frege1879] p. 50Proposition 51frege51 40410
[Frege1879] p. 50Proposition 52dfsbcq 3760
[Frege1879] p. 50Proposition 53frege53a 40415  frege53aid 40414  frege53b 40445  frege53c 40469
[Frege1879] p. 50Proposition 54biid 264  eqid 2824
[Frege1879] p. 50Proposition 55frege55a 40423  frege55aid 40420  frege55b 40452  frege55c 40473  frege55cor1a 40424  frege55lem2a 40422  frege55lem2b 40451  frege55lem2c 40472
[Frege1879] p. 50Proposition 56frege56a 40426  frege56aid 40425  frege56b 40453  frege56c 40474
[Frege1879] p. 51Axiom 58ax-frege58a 40430  ax-frege58b 40456  frege58bid 40457  frege58c 40476
[Frege1879] p. 51Proposition 57frege57a 40428  frege57aid 40427  frege57b 40454  frege57c 40475
[Frege1879] p. 51Proposition 58spsbc 3771
[Frege1879] p. 51Proposition 59frege59a 40432  frege59b 40459  frege59c 40477
[Frege1879] p. 52Proposition 60frege60a 40433  frege60b 40460  frege60c 40478
[Frege1879] p. 52Proposition 61frege61a 40434  frege61b 40461  frege61c 40479
[Frege1879] p. 52Proposition 62frege62a 40435  frege62b 40462  frege62c 40480
[Frege1879] p. 52Proposition 63frege63a 40436  frege63b 40463  frege63c 40481
[Frege1879] p. 53Proposition 64frege64a 40437  frege64b 40464  frege64c 40482
[Frege1879] p. 53Proposition 65frege65a 40438  frege65b 40465  frege65c 40483
[Frege1879] p. 54Proposition 66frege66a 40439  frege66b 40466  frege66c 40484
[Frege1879] p. 54Proposition 67frege67a 40440  frege67b 40467  frege67c 40485
[Frege1879] p. 54Proposition 68frege68a 40441  frege68b 40468  frege68c 40486
[Frege1879] p. 55Definition 69dffrege69 40487
[Frege1879] p. 58Proposition 70frege70 40488
[Frege1879] p. 59Proposition 71frege71 40489
[Frege1879] p. 59Proposition 72frege72 40490
[Frege1879] p. 59Proposition 73frege73 40491
[Frege1879] p. 60Definition 76dffrege76 40494
[Frege1879] p. 60Proposition 74frege74 40492
[Frege1879] p. 60Proposition 75frege75 40493
[Frege1879] p. 62Proposition 77frege77 40495  frege77d 40300
[Frege1879] p. 63Proposition 78frege78 40496
[Frege1879] p. 63Proposition 79frege79 40497
[Frege1879] p. 63Proposition 80frege80 40498
[Frege1879] p. 63Proposition 81frege81 40499  frege81d 40301
[Frege1879] p. 64Proposition 82frege82 40500
[Frege1879] p. 65Proposition 83frege83 40501  frege83d 40302
[Frege1879] p. 65Proposition 84frege84 40502
[Frege1879] p. 66Proposition 85frege85 40503
[Frege1879] p. 66Proposition 86frege86 40504
[Frege1879] p. 66Proposition 87frege87 40505  frege87d 40304
[Frege1879] p. 67Proposition 88frege88 40506
[Frege1879] p. 68Proposition 89frege89 40507
[Frege1879] p. 68Proposition 90frege90 40508
[Frege1879] p. 68Proposition 91frege91 40509  frege91d 40305
[Frege1879] p. 69Proposition 92frege92 40510
[Frege1879] p. 70Proposition 93frege93 40511
[Frege1879] p. 70Proposition 94frege94 40512
[Frege1879] p. 70Proposition 95frege95 40513
[Frege1879] p. 71Definition 99dffrege99 40517
[Frege1879] p. 71Proposition 96frege96 40514  frege96d 40303
[Frege1879] p. 71Proposition 97frege97 40515  frege97d 40306
[Frege1879] p. 71Proposition 98frege98 40516  frege98d 40307
[Frege1879] p. 72Proposition 100frege100 40518
[Frege1879] p. 72Proposition 101frege101 40519
[Frege1879] p. 72Proposition 102frege102 40520  frege102d 40308
[Frege1879] p. 73Proposition 103frege103 40521
[Frege1879] p. 73Proposition 104frege104 40522
[Frege1879] p. 73Proposition 105frege105 40523
[Frege1879] p. 73Proposition 106frege106 40524  frege106d 40309
[Frege1879] p. 74Proposition 107frege107 40525
[Frege1879] p. 74Proposition 108frege108 40526  frege108d 40310
[Frege1879] p. 74Proposition 109frege109 40527  frege109d 40311
[Frege1879] p. 75Proposition 110frege110 40528
[Frege1879] p. 75Proposition 111frege111 40529  frege111d 40313
[Frege1879] p. 76Proposition 112frege112 40530
[Frege1879] p. 76Proposition 113frege113 40531
[Frege1879] p. 76Proposition 114frege114 40532  frege114d 40312
[Frege1879] p. 77Definition 115dffrege115 40533
[Frege1879] p. 77Proposition 116frege116 40534
[Frege1879] p. 78Proposition 117frege117 40535
[Frege1879] p. 78Proposition 118frege118 40536
[Frege1879] p. 78Proposition 119frege119 40537
[Frege1879] p. 78Proposition 120frege120 40538
[Frege1879] p. 79Proposition 121frege121 40539
[Frege1879] p. 79Proposition 122frege122 40540  frege122d 40314
[Frege1879] p. 79Proposition 123frege123 40541
[Frege1879] p. 80Proposition 124frege124 40542  frege124d 40315
[Frege1879] p. 81Proposition 125frege125 40543
[Frege1879] p. 81Proposition 126frege126 40544  frege126d 40316
[Frege1879] p. 82Proposition 127frege127 40545
[Frege1879] p. 83Proposition 128frege128 40546
[Frege1879] p. 83Proposition 129frege129 40547  frege129d 40317
[Frege1879] p. 84Proposition 130frege130 40548
[Frege1879] p. 85Proposition 131frege131 40549  frege131d 40318
[Frege1879] p. 86Proposition 132frege132 40550
[Frege1879] p. 86Proposition 133frege133 40551  frege133d 40319
[Fremlin1] p. 13Definition 111G (b)df-salgen 42818
[Fremlin1] p. 13Definition 111G (d)borelmbl 43138
[Fremlin1] p. 13Proposition 111G (b)salgenss 42839
[Fremlin1] p. 14Definition 112Aismea 42953
[Fremlin1] p. 15Remark 112B (d)psmeasure 42973
[Fremlin1] p. 15Property 112C (b)meassle 42965
[Fremlin1] p. 15Property 112C (c)meaunle 42966
[Fremlin1] p. 16Property 112C (d)iundjiun 42962  meaiunle 42971  meaiunlelem 42970
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 42983  meaiuninc2 42984  meaiuninc3 42987  meaiuninc3v 42986  meaiunincf 42985  meaiuninclem 42982
[Fremlin1] p. 16Proposition 112C (f)meaiininc 42989  meaiininc2 42990  meaiininclem 42988
[Fremlin1] p. 19Theorem 113Ccaragen0 43008  caragendifcl 43016  caratheodory 43030  omelesplit 43020
[Fremlin1] p. 19Definition 113Aisome 42996  isomennd 43033  isomenndlem 43032
[Fremlin1] p. 19Remark 113B (c)omeunle 43018
[Fremlin1] p. 19Definition 112Dfcaragencmpl 43037  voncmpl 43123
[Fremlin1] p. 19Definition 113A (ii)omessle 43000
[Fremlin1] p. 20Theorem 113Ccarageniuncl 43025  carageniuncllem1 43023  carageniuncllem2 43024  caragenuncl 43015  caragenuncllem 43014  caragenunicl 43026
[Fremlin1] p. 21Remark 113Dcaragenel2d 43034
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 43028  caratheodorylem2 43029
[Fremlin1] p. 21Exercise 113Xacaragencmpl 43037
[Fremlin1] p. 23Lemma 114Bhoidmv1le 43096  hoidmv1lelem1 43093  hoidmv1lelem2 43094  hoidmv1lelem3 43095
[Fremlin1] p. 25Definition 114Eisvonmbl 43140
[Fremlin1] p. 29Lemma 115Bhoidmv1le 43096  hoidmvle 43102  hoidmvlelem1 43097  hoidmvlelem2 43098  hoidmvlelem3 43099  hoidmvlelem4 43100  hoidmvlelem5 43101  hsphoidmvle2 43087  hsphoif 43078  hsphoival 43081
[Fremlin1] p. 29Definition 1135 (b)hoicvr 43050
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 43058
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 43085  hoidmvn0val 43086  hoidmvval 43079  hoidmvval0 43089  hoidmvval0b 43092
[Fremlin1] p. 30Lemma 115Bhoiprodp1 43090  hsphoidmvle 43088
[Fremlin1] p. 30Definition 115Cdf-ovoln 43039  df-voln 43041
[Fremlin1] p. 30Proposition 115D (a)dmovn 43106  ovn0 43068  ovn0lem 43067  ovnf 43065  ovnome 43075  ovnssle 43063  ovnsslelem 43062  ovnsupge0 43059
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 43105  ovnhoilem1 43103  ovnhoilem2 43104  vonhoi 43169
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 43122  hoidifhspf 43120  hoidifhspval 43110  hoidifhspval2 43117  hoidifhspval3 43121  hspmbl 43131  hspmbllem1 43128  hspmbllem2 43129  hspmbllem3 43130
[Fremlin1] p. 31Definition 115Evoncmpl 43123  vonmea 43076
[Fremlin1] p. 32Proposition 115G (a)hoimbl 43133  hoimbl2 43167  hoimbllem 43132  hspdifhsp 43118  opnvonmbl 43136  opnvonmbllem2 43135
[Fremlin1] p. 32Proposition 115G (b)borelmbl 43138
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 43181  iccvonmbllem 43180  ioovonmbl 43179
[Fremlin1] p. 32Proposition 115G (d)vonicc 43187  vonicclem2 43186  vonioo 43184  vonioolem2 43183  vonn0icc 43190  vonn0icc2 43194  vonn0ioo 43189  vonn0ioo2 43192
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 43191  snvonmbl 43188  vonct 43195  vonsn 43193
[Fremlin1] p. 35Lemma 121Asubsalsal 42862
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 42861  subsaliuncllem 42860
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 43222  salpreimalegt 43208  salpreimaltle 43223
[Fremlin1] p. 35Proposition 121B (i)issmf 43225  issmff 43231  issmflem 43224
[Fremlin1] p. 35Proposition 121B (ii)issmfle 43242  issmflelem 43241  smfpreimale 43251
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 43253  issmfgtlem 43252
[Fremlin1] p. 36Definition 121Cdf-smblfn 43198  issmf 43225  issmff 43231  issmfge 43266  issmfgelem 43265  issmfgt 43253  issmfgtlem 43252  issmfle 43242  issmflelem 43241  issmflem 43224
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 43206  salpreimagtlt 43227  salpreimalelt 43226
[Fremlin1] p. 36Proposition 121B (iv)issmfge 43266  issmfgelem 43265
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 43250
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 43248  cnfsmf 43237
[Fremlin1] p. 36Proposition 121D (c)decsmf 43263  decsmflem 43262  incsmf 43239  incsmflem 43238
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 43202  pimconstlt1 43203  smfconst 43246
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 43291
[Fremlin1] p. 37Proposition 121E (d)smfmul 43290  smfmullem1 43286  smfmullem2 43287  smfmullem3 43288  smfmullem4 43289
[Fremlin1] p. 37Proposition 121E (e)smfdiv 43292
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 43295  smfpimbor1lem2 43294
[Fremlin1] p. 37Proposition 121E (g)smfco 43297
[Fremlin1] p. 37Proposition 121E (h)smfres 43285
[Fremlin1] p. 38Proposition 121E (e)smfrec 43284
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 43293  smfresal 43283
[Fremlin1] p. 38Proposition 121F (a)smflim 43273  smflim2 43300  smflimlem1 43267  smflimlem2 43268  smflimlem3 43269  smflimlem4 43270  smflimlem5 43271  smflimlem6 43272  smflimmpt 43304
[Fremlin1] p. 38Proposition 121F (b)smfsup 43308  smfsuplem1 43305  smfsuplem2 43306  smfsuplem3 43307  smfsupmpt 43309  smfsupxr 43310
[Fremlin1] p. 38Proposition 121F (c)smfinf 43312  smfinflem 43311  smfinfmpt 43313
[Fremlin1] p. 39Remark 121Gsmflim 43273  smflim2 43300  smflimmpt 43304
[Fremlin1] p. 39Proposition 121Fsmfpimcc 43302
[Fremlin1] p. 39Proposition 121F (d)smflimsup 43322  smflimsuplem2 43315  smflimsuplem6 43319  smflimsuplem7 43320  smflimsuplem8 43321  smflimsupmpt 43323
[Fremlin1] p. 39Proposition 121F (e)smfliminf 43325  smfliminflem 43324  smfliminfmpt 43326
[Fremlin1] p. 80Definition 135E (b)df-smblfn 43198
[Fremlin5] p. 193Proposition 563Gbnulmbl2 24136
[Fremlin5] p. 213Lemma 565Cauniioovol 24179
[Fremlin5] p. 214Lemma 565Cauniioombl 24189
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 35045
[Fremlin5] p. 220Theorem 565Maftc1anc 35048
[FreydScedrov] p. 283Axiom of Infinityax-inf 9092  inf1 9076  inf2 9077
[Gleason] p. 117Proposition 9-2.1df-enq 10325  enqer 10335
[Gleason] p. 117Proposition 9-2.2df-1nq 10330  df-nq 10326
[Gleason] p. 117Proposition 9-2.3df-plpq 10322  df-plq 10328
[Gleason] p. 119Proposition 9-2.4caovmo 7375  df-mpq 10323  df-mq 10329
[Gleason] p. 119Proposition 9-2.5df-rq 10331
[Gleason] p. 119Proposition 9-2.6ltexnq 10389
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10390  ltbtwnnq 10392
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10385
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10386
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10393
[Gleason] p. 121Definition 9-3.1df-np 10395
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10407
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10409
[Gleason] p. 122Definitiondf-1p 10396
[Gleason] p. 122Remark (1)prub 10408
[Gleason] p. 122Lemma 9-3.4prlem934 10447
[Gleason] p. 122Proposition 9-3.2df-ltp 10399
[Gleason] p. 122Proposition 9-3.3ltsopr 10446  psslinpr 10445  supexpr 10468  suplem1pr 10466  suplem2pr 10467
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10457  ltexprlem1 10450  ltexprlem2 10451  ltexprlem3 10452  ltexprlem4 10453  ltexprlem5 10454  ltexprlem6 10455  ltexprlem7 10456
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10459  ltaprlem 10458
[Gleason] p. 124Lemma 9-3.6prlem936 10461
[Gleason] p. 124Proposition 9-3.7df-mp 10398  mulclpr 10434  mulclprlem 10433  reclem2pr 10462
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10443
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10438
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10437
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10442
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10465  reclem3pr 10463  reclem4pr 10464
[Gleason] p. 126Proposition 9-4.1df-enr 10469  enrer 10477
[Gleason] p. 126Proposition 9-4.2df-0r 10474  df-1r 10475  df-nr 10470
[Gleason] p. 126Proposition 9-4.3df-mr 10472  df-plr 10471  negexsr 10516  recexsr 10521  recexsrlem 10517
[Gleason] p. 127Proposition 9-4.4df-ltr 10473
[Gleason] p. 130Proposition 10-1.3creui 11625  creur 11624  cru 11622
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 10602  axcnre 10578
[Gleason] p. 132Definition 10-3.1crim 14470  crimd 14587  crimi 14548  crre 14469  crred 14586  crrei 14547
[Gleason] p. 132Definition 10-3.2remim 14472  remimd 14553
[Gleason] p. 133Definition 10.36absval2 14640  absval2d 14801  absval2i 14753
[Gleason] p. 133Proposition 10-3.4(c)cjmul 14497  cjmuld 14576  cjmuli 14544
[Gleason] p. 133Proposition 10-3.4(e)cjcj 14495  cjcjd 14554  cjcji 14526
[Gleason] p. 133Proposition 10-3.4(f)cjre 14494  cjreb 14478  cjrebd 14557  cjrebi 14529  cjred 14581  rere 14477  rereb 14475  rerebd 14556  rerebi 14528  rered 14579
[Gleason] p. 133Proposition 10-3.7(a)absval 14593
[Gleason] p. 133Proposition 10-3.7(b)abscj 14635  abscjd 14806  abscji 14757
[Gleason] p. 133Proposition 10-3.7(c)abs00 14645  abs00d 14802  abs00i 14754  absne0d 14803
[Gleason] p. 133Proposition 10-3.7(d)releabs 14677  releabsd 14807  releabsi 14758
[Gleason] p. 133Proposition 10-3.7(f)absmul 14650  absmuld 14810  absmuli 14760
[Gleason] p. 133Proposition 10-3.7(h)abstri 14686  abstrid 14812  abstrii 14764
[Gleason] p. 134Definition 10-4.10exp0e1 13435  df-exp 13431  exp0 13434  expp1 13437  expp1d 13512
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 25275  cxpmuld 25323  expmul 13475  expmuld 13514  expmulz 13476
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 25272  mulcxpd 25315  mulexp 13469  mulexpd 13526  mulexpz 13470
[Gleason] p. 140Exercise 1znnen 15561
[Gleason] p. 141Definition 11-2.1fzval 12892
[Gleason] p. 168Proposition 12-2.1(b)climsub 14986  rlimsub 14996
[Gleason] p. 168Proposition 12-2.1(c)climmul 14985  rlimmul 14997
[Gleason] p. 171Corollary 12-2.2climmulc2 14989
[Gleason] p. 172Corollary 12-2.5climrecl 14936
[Gleason] p. 172Proposition 12-2.4(c)climabs 14956  climcj 14957  climim 14959  climre 14958  rlimabs 14961  rlimcj 14962  rlimim 14964  rlimre 14963
[Gleason] p. 173Definition 12-3.1df-ltxr 10672  df-xr 10671  ltxr 12503
[Gleason] p. 175Definition 12-4.1df-limsup 14824  limsupval 14827
[Gleason] p. 180Theorem 12-5.1climsup 15022
[Gleason] p. 180Theorem 12-5.3caucvg 15031  caucvgb 15032  caucvgr 15028  climcau 15023
[Gleason] p. 182Exercise 3cvgcmp 15167
[Gleason] p. 182Exercise 4cvgrat 15235
[Gleason] p. 195Theorem 13-2.12abs1m 14691
[Gleason] p. 217Lemma 13-4.1btwnzge0 13198
[Gleason] p. 223Definition 14-1.1df-met 20532
[Gleason] p. 223Definition 14-1.1(a)met0 22946  xmet0 22945
[Gleason] p. 223Definition 14-1.1(b)metgt0 22962
[Gleason] p. 223Definition 14-1.1(c)metsym 22953
[Gleason] p. 223Definition 14-1.1(d)mettri 22955  mstri 23072  xmettri 22954  xmstri 23071
[Gleason] p. 225Definition 14-1.5xpsmet 22985
[Gleason] p. 230Proposition 14-2.6txlm 22249
[Gleason] p. 240Theorem 14-4.3metcnp4 23910
[Gleason] p. 240Proposition 14-4.2metcnp3 23143
[Gleason] p. 243Proposition 14-4.16addcn 23466  addcn2 14946  mulcn 23468  mulcn2 14948  subcn 23467  subcn2 14947
[Gleason] p. 295Remarkbcval3 13667  bcval4 13668
[Gleason] p. 295Equation 2bcpasc 13682
[Gleason] p. 295Definition of binomial coefficientbcval 13665  df-bc 13664
[Gleason] p. 296Remarkbcn0 13671  bcnn 13673
[Gleason] p. 296Theorem 15-2.8binom 15181
[Gleason] p. 308Equation 2ef0 15440
[Gleason] p. 308Equation 3efcj 15441
[Gleason] p. 309Corollary 15-4.3efne0 15446
[Gleason] p. 309Corollary 15-4.4efexp 15450
[Gleason] p. 311Equation 17sincossq 15525
[Gleason] p. 311Equation 18cosbnd 15530  sinbnd 15529
[Gleason] p. 311Lemma 15-4.7sqeqor 13579  sqeqori 13577
[Gleason] p. 311Definition of ` `df-pi 15422
[Godowski] p. 730Equation SFgoeqi 30052
[GodowskiGreechie] p. 249Equation IV3oai 29447
[Golan] p. 1Remarksrgisid 19274
[Golan] p. 1Definitiondf-srg 19252
[Golan] p. 149Definitiondf-slmd 30854
[GramKnuthPat], p. 47Definition 2.42df-fwddif 33645
[Gratzer] p. 23Section 0.6df-mre 16853
[Gratzer] p. 27Section 0.6df-mri 16855
[Hall] p. 1Section 1.1df-asslaw 44311  df-cllaw 44309  df-comlaw 44310
[Hall] p. 2Section 1.2df-clintop 44323
[Hall] p. 7Section 1.3df-sgrp2 44344
[Halmos] p. 31Theorem 17.3riesz1 29844  riesz2 29845
[Halmos] p. 41Definition of Hermitianhmopadj2 29720
[Halmos] p. 42Definition of projector orderingpjordi 29952
[Halmos] p. 43Theorem 26.1elpjhmop 29964  elpjidm 29963  pjnmopi 29927
[Halmos] p. 44Remarkpjinormi 29466  pjinormii 29455
[Halmos] p. 44Theorem 26.2elpjch 29968  pjrn 29486  pjrni 29481  pjvec 29475
[Halmos] p. 44Theorem 26.3pjnorm2 29506
[Halmos] p. 44Theorem 26.4hmopidmpj 29933  hmopidmpji 29931
[Halmos] p. 45Theorem 27.1pjinvari 29970
[Halmos] p. 45Theorem 27.3pjoci 29959  pjocvec 29476
[Halmos] p. 45Theorem 27.4pjorthcoi 29948
[Halmos] p. 48Theorem 29.2pjssposi 29951
[Halmos] p. 48Theorem 29.3pjssdif1i 29954  pjssdif2i 29953
[Halmos] p. 50Definition of spectrumdf-spec 29634
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1797
[Hatcher] p. 25Definitiondf-phtpc 23593  df-phtpy 23572
[Hatcher] p. 26Definitiondf-pco 23606  df-pi1 23609
[Hatcher] p. 26Proposition 1.2phtpcer 23596
[Hatcher] p. 26Proposition 1.3pi1grp 23651
[Hefferon] p. 240Definition 3.12df-dmat 21092  df-dmatalt 44669
[Helfgott] p. 2Theoremtgoldbach 44198
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 44183
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 44195  bgoldbtbnd 44190  bgoldbtbnd 44190  tgblthelfgott 44196
[Helfgott] p. 5Proposition 1.1circlevma 31938
[Helfgott] p. 69Statement 7.49circlemethhgt 31939
[Helfgott] p. 69Statement 7.50hgt750lema 31953  hgt750lemb 31952  hgt750leme 31954  hgt750lemf 31949  hgt750lemg 31950
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 44192  tgoldbachgt 31959  tgoldbachgtALTV 44193  tgoldbachgtd 31958
[Helfgott] p. 70Statement 7.49ax-hgt749 31940
[Herstein] p. 54Exercise 28df-grpo 28272
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18110  grpoideu 28288  mndideu 17918
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18134  grpoinveu 28298
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18162  grpo2inv 28310
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18173  grpoinvop 28312
[Herstein] p. 57Exercise 1dfgrp3e 18195
[Hitchcock] p. 5Rule A3mptnan 1770
[Hitchcock] p. 5Rule A4mptxor 1771
[Hitchcock] p. 5Rule A5mtpxor 1773
[Holland] p. 1519Theorem 2sumdmdi 30199
[Holland] p. 1520Lemma 5cdj1i 30212  cdj3i 30220  cdj3lem1 30213  cdjreui 30211
[Holland] p. 1524Lemma 7mddmdin0i 30210
[Holland95] p. 13Theorem 3.6hlathil 39167
[Holland95] p. 14Line 15hgmapvs 39097
[Holland95] p. 14Line 16hdmaplkr 39119
[Holland95] p. 14Line 17hdmapellkr 39120
[Holland95] p. 14Line 19hdmapglnm2 39117
[Holland95] p. 14Line 20hdmapip0com 39123
[Holland95] p. 14Theorem 3.6hdmapevec2 39042
[Holland95] p. 14Lines 24 and 25hdmapoc 39137
[Holland95] p. 204Definition of involutiondf-srng 19610
[Holland95] p. 212Definition of subspacedf-psubsp 36709
[Holland95] p. 214Lemma 3.3lclkrlem2v 38734
[Holland95] p. 214Definition 3.2df-lpolN 38687
[Holland95] p. 214Definition of nonsingularpnonsingN 37139
[Holland95] p. 215Lemma 3.3(1)dihoml4 38583  poml4N 37159
[Holland95] p. 215Lemma 3.3(2)dochexmid 38674  pexmidALTN 37184  pexmidN 37175
[Holland95] p. 218Theorem 3.6lclkr 38739
[Holland95] p. 218Definition of dual vector spacedf-ldual 36330  ldualset 36331
[Holland95] p. 222Item 1df-lines 36707  df-pointsN 36708
[Holland95] p. 222Item 2df-polarityN 37109
[Holland95] p. 223Remarkispsubcl2N 37153  omllaw4 36452  pol1N 37116  polcon3N 37123
[Holland95] p. 223Definitiondf-psubclN 37141
[Holland95] p. 223Equation for polaritypolval2N 37112
[Holmes] p. 40Definitiondf-xrn 35693
[Hughes] p. 44Equation 1.21bax-his3 28863
[Hughes] p. 47Definition of projection operatordfpjop 29961
[Hughes] p. 49Equation 1.30eighmre 29742  eigre 29614  eigrei 29613
[Hughes] p. 49Equation 1.31eighmorth 29743  eigorth 29617  eigorthi 29616
[Hughes] p. 137Remark (ii)eigposi 29615
[Huneke] p. 1Claim 1frgrncvvdeq 28090
[Huneke] p. 1Statement 1frgrncvvdeqlem7 28086
[Huneke] p. 1Statement 2frgrncvvdeqlem8 28087
[Huneke] p. 1Statement 3frgrncvvdeqlem9 28088
[Huneke] p. 2Claim 2frgrregorufr 28106  frgrregorufr0 28105  frgrregorufrg 28107
[Huneke] p. 2Claim 3frgrhash2wsp 28113  frrusgrord 28122  frrusgrord0 28121
[Huneke] p. 2Statementdf-clwwlknon 27869
[Huneke] p. 2Statement 4frgrwopreglem4 28096
[Huneke] p. 2Statement 5frgrwopreg1 28099  frgrwopreg2 28100  frgrwopregasn 28097  frgrwopregbsn 28098
[Huneke] p. 2Statement 6frgrwopreglem5 28102
[Huneke] p. 2Statement 7fusgreghash2wspv 28116
[Huneke] p. 2Statement 8fusgreghash2wsp 28119
[Huneke] p. 2Statement 9clwlksndivn 27867  numclwlk1 28152  numclwlk1lem1 28150  numclwlk1lem2 28151  numclwwlk1 28142  numclwwlk8 28173
[Huneke] p. 2Definition 3frgrwopreglem1 28093
[Huneke] p. 2Definition 4df-clwlks 27556
[Huneke] p. 2Definition 62clwwlk 28128
[Huneke] p. 2Definition 7numclwwlkovh 28154  numclwwlkovh0 28153
[Huneke] p. 2Statement 10numclwwlk2 28162
[Huneke] p. 2Statement 11rusgrnumwlkg 27759
[Huneke] p. 2Statement 12numclwwlk3 28166
[Huneke] p. 2Statement 13numclwwlk5 28169
[Huneke] p. 2Statement 14numclwwlk7 28172
[Indrzejczak] p. 33Definition ` `Enatded 28184  natded 28184
[Indrzejczak] p. 33Definition ` `Inatded 28184
[Indrzejczak] p. 34Definition ` `Enatded 28184  natded 28184
[Indrzejczak] p. 34Definition ` `Inatded 28184
[Jech] p. 4Definition of classcv 1537  cvjust 2819
[Jech] p. 42Lemma 6.1alephexp1 9993
[Jech] p. 42Equation 6.1alephadd 9991  alephmul 9992
[Jech] p. 43Lemma 6.2infmap 9990  infmap2 9632
[Jech] p. 71Lemma 9.3jech9.3 9234
[Jech] p. 72Equation 9.3scott0 9306  scottex 9305
[Jech] p. 72Exercise 9.1rankval4 9287
[Jech] p. 72Scheme "Collection Principle"cp 9311
[Jech] p. 78Noteopthprc 5603
[JonesMatijasevic] p. 694Definition 2.3rmxyval 39709
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 39797
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 39798
[JonesMatijasevic] p. 695Equation 2.9rmxp1 39726  rmyp1 39727
[JonesMatijasevic] p. 695Equation 2.10rmxm1 39728  rmym1 39729
[JonesMatijasevic] p. 695Equation 2.11rmx0 39719  rmx1 39720  rmxluc 39730
[JonesMatijasevic] p. 695Equation 2.12rmy0 39723  rmy1 39724  rmyluc 39731
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 39733
[JonesMatijasevic] p. 695Equation 2.14rmydbl 39734
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 39754  jm2.17b 39755  jm2.17c 39756
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 39787
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 39791
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 39782
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 39757  jm2.24nn 39753
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 39796
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 39802  rmygeid 39758
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 39814
[Juillerat] p. 11Section *5etransc 42788  etransclem47 42786  etransclem48 42787
[Juillerat] p. 12Equation (7)etransclem44 42783
[Juillerat] p. 12Equation *(7)etransclem46 42785
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 42771
[Juillerat] p. 13Proofetransclem35 42774
[Juillerat] p. 13Part of case 2 proven inetransclem38 42777
[Juillerat] p. 13Part of case 2 provenetransclem24 42763
[Juillerat] p. 13Part of case 2: proven inetransclem41 42780
[Juillerat] p. 14Proofetransclem23 42762
[KalishMontague] p. 81Note 1ax-6 1971
[KalishMontague] p. 85Lemma 2equid 2020
[KalishMontague] p. 85Lemma 3equcomi 2025
[KalishMontague] p. 86Lemma 7cbvalivw 2015  cbvaliw 2014  wl-cbvmotv 34828  wl-motae 34830  wl-moteq 34829
[KalishMontague] p. 87Lemma 8spimvw 2003  spimw 1974
[KalishMontague] p. 87Lemma 9spfw 2041  spw 2042
[Kalmbach] p. 14Definition of latticechabs1 29295  chabs1i 29297  chabs2 29296  chabs2i 29298  chjass 29312  chjassi 29265  latabs1 17693  latabs2 17694
[Kalmbach] p. 15Definition of atomdf-at 30117  ela 30118
[Kalmbach] p. 15Definition of coverscvbr2 30062  cvrval2 36480
[Kalmbach] p. 16Definitiondf-ol 36384  df-oml 36385
[Kalmbach] p. 20Definition of commutescmbr 29363  cmbri 29369  cmtvalN 36417  df-cm 29362  df-cmtN 36383
[Kalmbach] p. 22Remarkomllaw5N 36453  pjoml5 29392  pjoml5i 29367
[Kalmbach] p. 22Definitionpjoml2 29390  pjoml2i 29364
[Kalmbach] p. 22Theorem 2(v)cmcm 29393  cmcmi 29371  cmcmii 29376  cmtcomN 36455
[Kalmbach] p. 22Theorem 2(ii)omllaw3 36451  omlsi 29183  pjoml 29215  pjomli 29214
[Kalmbach] p. 22Definition of OML lawomllaw2N 36450
[Kalmbach] p. 23Remarkcmbr2i 29375  cmcm3 29394  cmcm3i 29373  cmcm3ii 29378  cmcm4i 29374  cmt3N 36457  cmt4N 36458  cmtbr2N 36459
[Kalmbach] p. 23Lemma 3cmbr3 29387  cmbr3i 29379  cmtbr3N 36460
[Kalmbach] p. 25Theorem 5fh1 29397  fh1i 29400  fh2 29398  fh2i 29401  omlfh1N 36464
[Kalmbach] p. 65Remarkchjatom 30136  chslej 29277  chsleji 29237  shslej 29159  shsleji 29149
[Kalmbach] p. 65Proposition 1chocin 29274  chocini 29233  chsupcl 29119  chsupval2 29189  h0elch 29034  helch 29022  hsupval2 29188  ocin 29075  ococss 29072  shococss 29073
[Kalmbach] p. 65Definition of subspace sumshsval 29091
[Kalmbach] p. 66Remarkdf-pjh 29174  pjssmi 29944  pjssmii 29460
[Kalmbach] p. 67Lemma 3osum 29424  osumi 29421
[Kalmbach] p. 67Lemma 4pjci 29979
[Kalmbach] p. 103Exercise 6atmd2 30179
[Kalmbach] p. 103Exercise 12mdsl0 30089
[Kalmbach] p. 140Remarkhatomic 30139  hatomici 30138  hatomistici 30141
[Kalmbach] p. 140Proposition 1atlatmstc 36525
[Kalmbach] p. 140Proposition 1(i)atexch 30160  lsatexch 36249
[Kalmbach] p. 140Proposition 1(ii)chcv1 30134  cvlcvr1 36545  cvr1 36616
[Kalmbach] p. 140Proposition 1(iii)cvexch 30153  cvexchi 30148  cvrexch 36626
[Kalmbach] p. 149Remark 2chrelati 30143  hlrelat 36608  hlrelat5N 36607  lrelat 36220
[Kalmbach] p. 153Exercise 5lsmcv 19906  lsmsatcv 36216  spansncv 29432  spansncvi 29431
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 36235  spansncv2 30072
[Kalmbach] p. 266Definitiondf-st 29990
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10060  fpwwe2 10057
[KanamoriPincus] p. 416Corollary 1.3canth4 10061
[KanamoriPincus] p. 417Corollary 1.6canthp1 10068
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10063
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10065
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10078
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10082  gchxpidm 10083
[KanamoriPincus] p. 419Theorem 2.1gchacg 10094  gchhar 10093
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 9630  unxpwdom 9044
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10084
[Kreyszig] p. 3Property M1metcl 22935  xmetcl 22934
[Kreyszig] p. 4Property M2meteq0 22942
[Kreyszig] p. 8Definition 1.1-8dscmet 23175
[Kreyszig] p. 12Equation 5conjmul 11349  muleqadd 11276
[Kreyszig] p. 18Definition 1.3-2mopnval 23041
[Kreyszig] p. 19Remarkmopntopon 23042
[Kreyszig] p. 19Theorem T1mopn0 23101  mopnm 23047
[Kreyszig] p. 19Theorem T2unimopn 23099
[Kreyszig] p. 19Definition of neighborhoodneibl 23104
[Kreyszig] p. 20Definition 1.3-3metcnp2 23145
[Kreyszig] p. 25Definition 1.4-1lmbr 21859  lmmbr 23858  lmmbr2 23859
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 21981
[Kreyszig] p. 28Theorem 1.4-5lmcau 23913
[Kreyszig] p. 28Definition 1.4-3iscau 23876  iscmet2 23894
[Kreyszig] p. 30Theorem 1.4-7cmetss 23916
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 22062  metelcls 23905
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 23906  metcld2 23907
[Kreyszig] p. 51Equation 2clmvneg1 23700  lmodvneg1 19670  nvinv 28418  vcm 28355
[Kreyszig] p. 51Equation 1aclm0vs 23696  lmod0vs 19660  slmd0vs 30877  vc0 28353
[Kreyszig] p. 51Equation 1blmodvs0 19661  slmdvs0 30878  vcz 28354
[Kreyszig] p. 58Definition 2.2-1imsmet 28470  ngpmet 23205  nrmmetd 23177
[Kreyszig] p. 59Equation 1imsdval 28465  imsdval2 28466  ncvspds 23762  ngpds 23206
[Kreyszig] p. 63Problem 1nmval 23192  nvnd 28467
[Kreyszig] p. 64Problem 2nmeq0 23220  nmge0 23219  nvge0 28452  nvz 28448
[Kreyszig] p. 64Problem 3nmrtri 23226  nvabs 28451
[Kreyszig] p. 91Definition 2.7-1isblo3i 28580
[Kreyszig] p. 92Equation 2df-nmoo 28524
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 28586  blocni 28584
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 28585
[Kreyszig] p. 129Definition 3.1-1cphipeq0 23805  ipeq0 20775  ipz 28498
[Kreyszig] p. 135Problem 2pythi 28629
[Kreyszig] p. 137Lemma 3-2.1(a)sii 28633
[Kreyszig] p. 144Equation 4supcvg 15207
[Kreyszig] p. 144Theorem 3.3-1minvec 24036  minveco 28663
[Kreyszig] p. 196Definition 3.9-1df-aj 28529
[Kreyszig] p. 247Theorem 4.7-2bcth 23929
[Kreyszig] p. 249Theorem 4.7-3ubth 28652
[Kreyszig] p. 470Definition of positive operator orderingleop 29902  leopg 29901
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 29920
[Kreyszig] p. 525Theorem 10.1-1htth 28697
[Kulpa] p. 547Theorempoimir 35000
[Kulpa] p. 547Equation (1)poimirlem32 34999
[Kulpa] p. 547Equation (2)poimirlem31 34998
[Kulpa] p. 548Theorembroucube 35001
[Kulpa] p. 548Equation (6)poimirlem26 34993
[Kulpa] p. 548Equation (7)poimirlem27 34994
[Kunen] p. 10Axiom 0ax6e 2403  axnul 5195
[Kunen] p. 11Axiom 3axnul 5195
[Kunen] p. 12Axiom 6zfrep6 7646
[Kunen] p. 24Definition 10.24mapval 8408  mapvalg 8406
[Kunen] p. 30Lemma 10.20fodomg 9936
[Kunen] p. 31Definition 10.24mapex 8402
[Kunen] p. 95Definition 2.1df-r1 9184
[Kunen] p. 97Lemma 2.10r1elss 9226  r1elssi 9225
[Kunen] p. 107Exercise 4rankop 9278  rankopb 9272  rankuni 9283  rankxplim 9299  rankxpsuc 9302
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4917
[Lang] , p. 225Corollary 1.3finexttrb 31080
[Lang] p. Definitiondf-rn 5553
[Lang] p. 3Statementlidrideqd 17875  mndbn0 17923
[Lang] p. 3Definitiondf-mnd 17908
[Lang] p. 4Definition of a (finite) productgsumsplit1r 17893
[Lang] p. 4Property of composites. Second formulagsumccat 18002
[Lang] p. 5Equationgsumreidx 19033
[Lang] p. 5Definition of an (infinite) productgsumfsupp 44305
[Lang] p. 6Examplenn0mnd 44302
[Lang] p. 6Equationgsumxp2 19096
[Lang] p. 6Statementcycsubm 18341
[Lang] p. 6Definitionmulgnn0gsum 18230
[Lang] p. 6Observationmndlsmidm 18792
[Lang] p. 7Definitiondfgrp2e 18125
[Lang] p. 30Definitiondf-tocyc 30774
[Lang] p. 32Property (a)cyc3genpm 30819
[Lang] p. 32Property (b)cyc3conja 30824  cycpmconjv 30809
[Lang] p. 53Definitiondf-cat 16935
[Lang] p. 54Definitiondf-iso 17015
[Lang] p. 57Definitiondf-inito 17247  df-termo 17248
[Lang] p. 58Exampleirinitoringc 44556
[Lang] p. 58Statementinitoeu1 17267  termoeu1 17274
[Lang] p. 62Definitiondf-func 17124
[Lang] p. 65Definitiondf-nat 17209
[Lang] p. 91Notedf-ringc 44492
[Lang] p. 92Statementmxidlprm 31005
[Lang] p. 92Definitionisprmidlc 30991
[Lang] p. 128Remarkdsmmlmod 20882
[Lang] p. 129Prooflincscm 44701  lincscmcl 44703  lincsum 44700  lincsumcl 44702
[Lang] p. 129Statementlincolss 44705
[Lang] p. 129Observationdsmmfi 20875
[Lang] p. 141Theorem 5.3dimkerim 31051  qusdimsum 31052
[Lang] p. 141Corollary 5.4lssdimle 31034
[Lang] p. 147Definitionsnlindsntor 44742
[Lang] p. 504Statementmat1 21049  matring 21045
[Lang] p. 504Definitiondf-mamu 20988
[Lang] p. 505Statementmamuass 21004  mamutpos 21060  matassa 21046  mattposvs 21057  tposmap 21059
[Lang] p. 513Definitionmdet1 21203  mdetf 21197
[Lang] p. 513Theorem 4.4cramer 21293
[Lang] p. 514Proposition 4.6mdetleib 21189
[Lang] p. 514Proposition 4.8mdettpos 21213
[Lang] p. 515Corollary 4.9mdetero 21212  mdetralt 21210
[Lang] p. 517Proposition 4.15mdetmul 21225
[Lang] p. 561Theorem 3.1cayleyhamilton 21491
[Lang], p. 224Proposition 1.2extdgmul 31079  fedgmul 31055
[Lang], p. 561Remarkchpmatply1 21433
[Lang], p. 561Definitiondf-chpmat 21428
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 40895
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 40890
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 40896
[LeBlanc] p. 277Rule R2axnul 5195
[Levy] p. 12Axiom 4.3.1df-clab 2803
[Levy] p. 338Axiomdf-clel 2896  df-cleq 2817
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2896  df-cleq 2817
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2803
[Levy] p. 358Axiomdf-clab 2803
[Levy58] p. 2Definition Iisfin1-3 9800
[Levy58] p. 2Definition IIdf-fin2 9700
[Levy58] p. 2Definition IIIdf-fin3 9702
[Levy58] p. 3Definition Vdf-fin5 9703
[Levy58] p. 3Definition IVdf-fin4 9701
[Levy58] p. 4Definition VIdf-fin6 9704
[Levy58] p. 4Definition VIIdf-fin7 9705
[Levy58], p. 3Theorem 1fin1a2 9829
[Lipparini] p. 3Lemma 2.1.1nosepssdm 33215
[Lipparini] p. 3Lemma 2.1.4noresle 33225
[Lipparini] p. 6Proposition 4.2nosupbnd1 33239
[Lipparini] p. 6Proposition 4.3nosupbnd2 33241
[Lipparini] p. 7Theorem 5.1noetalem2 33243  noetalem3 33244
[Lopez-Astorga] p. 12Rule 1mptnan 1770
[Lopez-Astorga] p. 12Rule 2mptxor 1771
[Lopez-Astorga] p. 12Rule 3mtpxor 1773
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 30187
[Maeda] p. 168Lemma 5mdsym 30191  mdsymi 30190
[Maeda] p. 168Lemma 4(i)mdsymlem4 30185  mdsymlem6 30187  mdsymlem7 30188
[Maeda] p. 168Lemma 4(ii)mdsymlem8 30189
[MaedaMaeda] p. 1Remarkssdmd1 30092  ssdmd2 30093  ssmd1 30090  ssmd2 30091
[MaedaMaeda] p. 1Lemma 1.2mddmd2 30088
[MaedaMaeda] p. 1Definition 1.1df-dmd 30060  df-md 30059  mdbr 30073
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 30110  mdslj1i 30098  mdslj2i 30099  mdslle1i 30096  mdslle2i 30097  mdslmd1i 30108  mdslmd2i 30109
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 30100  mdsl2bi 30102  mdsl2i 30101
[MaedaMaeda] p. 2Lemma 1.6mdexchi 30114
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 30111
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 30112
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 30089
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 30094  mdsl3 30095
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 30113
[MaedaMaeda] p. 4Theorem 1.14mdcompli 30208
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 36527  hlrelat1 36606
[MaedaMaeda] p. 31Lemma 7.5lcvexch 36245
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 30115  cvmdi 30103  cvnbtwn4 30068  cvrnbtwn4 36485
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 30116
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 36546  cvp 30154  cvrp 36622  lcvp 36246
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 30178
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 30177
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 36539  hlexch4N 36598
[MaedaMaeda] p. 34Exercise 7.1atabsi 30180
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 36649
[MaedaMaeda] p. 61Definition 15.10psubN 36955  atpsubN 36959  df-pointsN 36708  pointpsubN 36957
[MaedaMaeda] p. 62Theorem 15.5df-pmap 36710  pmap11 36968  pmaple 36967  pmapsub 36974  pmapval 36963
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 36971  pmap1N 36973
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 36976  pmapglb2N 36977  pmapglb2xN 36978  pmapglbx 36975
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 37058
[MaedaMaeda] p. 67Postulate PS1ps-1 36683
[MaedaMaeda] p. 68Condition PS2ps-2 36684
[MaedaMaeda] p. 69Lemma 16.4ps-1 36683
[MaedaMaeda] p. 69Theorem 16.4ps-2 36684
[MaedaMaeda] p. 70Theorem 16.9lsmmod 18797  lsmmod2 18798  lssats 36218  shatomici 30137  shatomistici 30140  shmodi 29169  shmodsi 29168
[MaedaMaeda] p. 130Remark 29.6dmdmd 30079  mdsymlem7 30188
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 29368
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 29272
[MaedaMaeda] p. 139Remarksumdmdii 30194
[Margaris] p. 40Rule Cexlimiv 1932
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 400  df-ex 1782  df-or 845  dfbi2 478
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 28181
[Margaris] p. 59Section 14notnotrALTVD 41478
[Margaris] p. 60Theorem 8jcn 165
[Margaris] p. 60Section 14con3ALTVD 41479
[Margaris] p. 79Rule Cexinst01 41188  exinst11 41189
[Margaris] p. 89Theorem 19.219.2 1982  19.2g 2189  r19.2z 4422
[Margaris] p. 89Theorem 19.319.3 2204  rr19.3v 3645
[Margaris] p. 89Theorem 19.5alcom 2164
[Margaris] p. 89Theorem 19.6alex 1827
[Margaris] p. 89Theorem 19.7alnex 1783
[Margaris] p. 89Theorem 19.819.8a 2182
[Margaris] p. 89Theorem 19.919.9 2207  19.9h 2296  exlimd 2220  exlimdh 2300
[Margaris] p. 89Theorem 19.11excom 2170  excomim 2171
[Margaris] p. 89Theorem 19.1219.12 2348
[Margaris] p. 90Section 19conventions-labels 28182  conventions-labels 28182  conventions-labels 28182  conventions-labels 28182
[Margaris] p. 90Theorem 19.14exnal 1828
[Margaris] p. 90Theorem 19.152albi 40939  albi 1820
[Margaris] p. 90Theorem 19.1619.16 2229
[Margaris] p. 90Theorem 19.1719.17 2230
[Margaris] p. 90Theorem 19.182exbi 40941  exbi 1848
[Margaris] p. 90Theorem 19.1919.19 2233
[Margaris] p. 90Theorem 19.202alim 40938  2alimdv 1920  alimd 2214  alimdh 1819  alimdv 1918  ax-4 1811  ralimdaa 3212  ralimdv 3173  ralimdva 3172  ralimdvva 3174  sbcimdv 3827
[Margaris] p. 90Theorem 19.2119.21 2209  19.21h 2297  19.21t 2208  19.21vv 40937  alrimd 2217  alrimdd 2216  alrimdh 1865  alrimdv 1931  alrimi 2215  alrimih 1825  alrimiv 1929  alrimivv 1930  hbralrimi 3175  r19.21be 3205  r19.21bi 3203  ralrimd 3213  ralrimdv 3183  ralrimdva 3184  ralrimdvv 3188  ralrimdvva 3189  ralrimi 3211  ralrimia 41626  ralrimiv 3176  ralrimiva 3177  ralrimivv 3185  ralrimivva 3186  ralrimivvva 3187  ralrimivw 3178
[Margaris] p. 90Theorem 19.222exim 40940  2eximdv 1921  exim 1835  eximd 2218  eximdh 1866  eximdv 1919  rexim 3236  reximd2a 3305  reximdai 3304  reximdd 41649  reximddv 3268  reximddv2 3271  reximddv3 41648  reximdv 3266  reximdv2 3264  reximdva 3267  reximdvai 3265  reximdvva 3270  reximi2 3239
[Margaris] p. 90Theorem 19.2319.23 2213  19.23bi 2192  19.23h 2298  19.23t 2212  exlimdv 1935  exlimdvv 1936  exlimexi 41087  exlimiv 1932  exlimivv 1934  rexlimd3 41641  rexlimdv 3276  rexlimdv3a 3279  rexlimdva 3277  rexlimdva2 3280  rexlimdvaa 3278  rexlimdvv 3286  rexlimdvva 3287  rexlimdvw 3283  rexlimiv 3273  rexlimiva 3274  rexlimivv 3285
[Margaris] p. 90Theorem 19.2419.24 1993
[Margaris] p. 90Theorem 19.2519.25 1882
[Margaris] p. 90Theorem 19.2619.26 1872
[Margaris] p. 90Theorem 19.2719.27 2231  r19.27z 4432  r19.27zv 4433
[Margaris] p. 90Theorem 19.2819.28 2232  19.28vv 40947  r19.28z 4425  r19.28zv 4428  rr19.28v 3646
[Margaris] p. 90Theorem 19.2919.29 1875  r19.29d2r 3327  r19.29imd 3252
[Margaris] p. 90Theorem 19.3019.30 1883
[Margaris] p. 90Theorem 19.3119.31 2238  19.31vv 40945
[Margaris] p. 90Theorem 19.3219.32 2237  r19.32 43516
[Margaris] p. 90Theorem 19.3319.33-2 40943  19.33 1886
[Margaris] p. 90Theorem 19.3419.34 1994
[Margaris] p. 90Theorem 19.3519.35 1879
[Margaris] p. 90Theorem 19.3619.36 2234  19.36vv 40944  r19.36zv 4434
[Margaris] p. 90Theorem 19.3719.37 2236  19.37vv 40946  r19.37zv 4429
[Margaris] p. 90Theorem 19.3819.38 1840
[Margaris] p. 90Theorem 19.3919.39 1992
[Margaris] p. 90Theorem 19.4019.40-2 1889  19.40 1888  r19.40 3338
[Margaris] p. 90Theorem 19.4119.41 2239  19.41rg 41113
[Margaris] p. 90Theorem 19.4219.42 2240
[Margaris] p. 90Theorem 19.4319.43 1884
[Margaris] p. 90Theorem 19.4419.44 2241  r19.44zv 4431
[Margaris] p. 90Theorem 19.4519.45 2242  r19.45zv 4430
[Margaris] p. 110Exercise 2(b)eu1 2697
[Mayet] p. 370Remarkjpi 30049  largei 30046  stri 30036
[Mayet3] p. 9Definition of CH-statesdf-hst 29991  ishst 29993
[Mayet3] p. 10Theoremhstrbi 30045  hstri 30044
[Mayet3] p. 1223Theorem 4.1mayete3i 29507
[Mayet3] p. 1240Theorem 7.1mayetes3i 29508
[MegPav2000] p. 2344Theorem 3.3stcltrthi 30057
[MegPav2000] p. 2345Definition 3.4-1chintcl 29111  chsupcl 29119
[MegPav2000] p. 2345Definition 3.4-2hatomic 30139
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 30133
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 30160
[MegPav2000] p. 2366Figure 7pl42N 37189
[MegPav2002] p. 362Lemma 2.2latj31 17705  latj32 17703  latjass 17701
[Megill] p. 444Axiom C5ax-5 1912  ax5ALT 36113
[Megill] p. 444Section 7conventions 28181
[Megill] p. 445Lemma L12aecom-o 36107  ax-c11n 36094  axc11n 2450
[Megill] p. 446Lemma L17equtrr 2030
[Megill] p. 446Lemma L18ax6fromc10 36102
[Megill] p. 446Lemma L19hbnae-o 36134  hbnae 2456
[Megill] p. 447Remark 9.1dfsb1 2512  sbid 2259  sbidd-misc 45096  sbidd 45095
[Megill] p. 448Remark 9.6axc14 2488
[Megill] p. 448Scheme C4'ax-c4 36090
[Megill] p. 448Scheme C5'ax-c5 36089  sp 2184
[Megill] p. 448Scheme C6'ax-11 2162
[Megill] p. 448Scheme C7'ax-c7 36091
[Megill] p. 448Scheme C8'ax-7 2016
[Megill] p. 448Scheme C9'ax-c9 36096
[Megill] p. 448Scheme C10'ax-6 1971  ax-c10 36092
[Megill] p. 448Scheme C11'ax-c11 36093
[Megill] p. 448Scheme C12'ax-8 2117
[Megill] p. 448Scheme C13'ax-9 2125
[Megill] p. 448Scheme C14'ax-c14 36097
[Megill] p. 448Scheme C15'ax-c15 36095
[Megill] p. 448Scheme C16'ax-c16 36098
[Megill] p. 448Theorem 9.4dral1-o 36110  dral1 2463  dral2-o 36136  dral2 2462  drex1 2465  drex2 2466  drsb1 2537  drsb2 2269
[Megill] p. 449Theorem 9.7sbcom2 2169  sbequ 2091  sbid2v 2553
[Megill] p. 450Example in Appendixhba1-o 36103  hba1 2303
[Mendelson] p. 35Axiom A3hirstL-ax3 43348
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3846  rspsbca 3847  stdpc4 2074
[Mendelson] p. 69Axiom 5ax-c4 36090  ra4 3853  stdpc5 2210
[Mendelson] p. 81Rule Cexlimiv 1932
[Mendelson] p. 95Axiom 6stdpc6 2036
[Mendelson] p. 95Axiom 7stdpc7 2254
[Mendelson] p. 225Axiom system NBGru 3757
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5391
[Mendelson] p. 231Exercise 4.10(k)inv1 4330
[Mendelson] p. 231Exercise 4.10(l)unv 4331
[Mendelson] p. 231Exercise 4.10(n)dfin3 4227
[Mendelson] p. 231Exercise 4.10(o)df-nul 4276
[Mendelson] p. 231Exercise 4.10(q)dfin4 4228
[Mendelson] p. 231Exercise 4.10(s)ddif 4098
[Mendelson] p. 231Definition of uniondfun3 4226
[Mendelson] p. 235Exercise 4.12(c)univ 5331
[Mendelson] p. 235Exercise 4.12(d)pwv 4821
[Mendelson] p. 235Exercise 4.12(j)pwin 5441
[Mendelson] p. 235Exercise 4.12(k)pwunss 4541
[Mendelson] p. 235Exercise 4.12(l)pwssun 5443
[Mendelson] p. 235Exercise 4.12(n)uniin 4848
[Mendelson] p. 235Exercise 4.12(p)reli 5685
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6108
[Mendelson] p. 244Proposition 4.8(g)epweon 7487
[Mendelson] p. 246Definition of successordf-suc 6184
[Mendelson] p. 250Exercise 4.36oelim2 8211
[Mendelson] p. 254Proposition 4.22(b)xpen 8671
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8591  xpsneng 8592
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8598  xpcomeng 8599
[Mendelson] p. 254Proposition 4.22(e)xpassen 8601
[Mendelson] p. 255Definitionbrsdom 8522
[Mendelson] p. 255Exercise 4.39endisj 8594
[Mendelson] p. 255Exercise 4.41mapprc 8400
[Mendelson] p. 255Exercise 4.43mapsnen 8579  mapsnend 8578
[Mendelson] p. 255Exercise 4.45mapunen 8677
[Mendelson] p. 255Exercise 4.47xpmapen 8676
[Mendelson] p. 255Exercise 4.42(a)map0e 8436
[Mendelson] p. 255Exercise 4.42(b)map1 8582
[Mendelson] p. 257Proposition 4.24(a)undom 8595
[Mendelson] p. 258Exercise 4.56(c)djuassen 9596  djucomen 9595
[Mendelson] p. 258Exercise 4.56(f)djudom1 9600
[Mendelson] p. 258Exercise 4.56(g)xp2dju 9594
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8146
[Mendelson] p. 266Proposition 4.34(f)oaordex 8174
[Mendelson] p. 275Proposition 4.42(d)entri3 9973
[Mendelson] p. 281Definitiondf-r1 9184
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9233
[Mendelson] p. 287Axiom system MKru 3757
[MertziosUnger] p. 152Definitiondf-frgr 28040
[MertziosUnger] p. 153Remark 1frgrconngr 28075
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 28077  vdgn1frgrv3 28078
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 28079
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 28072
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 28065  2pthfrgrrn 28063  2pthfrgrrn2 28064
[Mittelstaedt] p. 9Definitiondf-oc 29031
[Monk1] p. 22Remarkconventions 28181
[Monk1] p. 22Theorem 3.1conventions 28181
[Monk1] p. 26Theorem 2.8(vii)ssin 4191
[Monk1] p. 33Theorem 3.2(i)ssrel 5644  ssrelf 30370
[Monk1] p. 33Theorem 3.2(ii)eqrel 5645
[Monk1] p. 34Definition 3.3df-opab 5115
[Monk1] p. 36Theorem 3.7(i)coi1 6102  coi2 6103
[Monk1] p. 36Theorem 3.8(v)dm0 5777  rn0 5783
[Monk1] p. 36Theorem 3.7(ii)cnvi 5987
[Monk1] p. 37Theorem 3.13(i)relxp 5560
[Monk1] p. 37Theorem 3.13(x)dmxp 5786  rnxp 6014
[Monk1] p. 37Theorem 3.13(ii)0xp 5636  xp0 6002
[Monk1] p. 38Theorem 3.16(ii)ima0 5932
[Monk1] p. 38Theorem 3.16(viii)imai 5929
[Monk1] p. 39Theorem 3.17imaex 7611  imaexALTV 35657  imaexg 7610
[Monk1] p. 39Theorem 3.16(xi)imassrn 5927
[Monk1] p. 41Theorem 4.3(i)fnopfv 6831  funfvop 6808
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6709
[Monk1] p. 42Theorem 4.4(iii)fvelima 6719
[Monk1] p. 43Theorem 4.6funun 6388
[Monk1] p. 43Theorem 4.8(iv)dff13 7002  dff13f 7003
[Monk1] p. 46Theorem 4.15(v)funex 6970  funrnex 7645
[Monk1] p. 50Definition 5.4fniunfv 6995
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6071
[Monk1] p. 52Theorem 5.11(viii)ssint 4878
[Monk1] p. 52Definition 5.13 (i)1stval2 7696  df-1st 7679
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7697  df-2nd 7680
[Monk1] p. 112Theorem 15.17(v)ranksn 9274  ranksnb 9247
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9275
[Monk1] p. 112Theorem 15.17(iii)rankun 9276  rankunb 9270
[Monk1] p. 113Theorem 15.18r1val3 9258
[Monk1] p. 113Definition 15.19df-r1 9184  r1val2 9257
[Monk1] p. 117Lemmazorn2 9920  zorn2g 9917
[Monk1] p. 133Theorem 18.11cardom 9406
[Monk1] p. 133Theorem 18.12canth3 9975
[Monk1] p. 133Theorem 18.14carduni 9401
[Monk2] p. 105Axiom C4ax-4 1811
[Monk2] p. 105Axiom C7ax-7 2016
[Monk2] p. 105Axiom C8ax-12 2179  ax-c15 36095  ax12v2 2181
[Monk2] p. 108Lemma 5ax-c4 36090
[Monk2] p. 109Lemma 12ax-11 2162
[Monk2] p. 109Lemma 15equvini 2479  equvinv 2037  eqvinop 5365
[Monk2] p. 113Axiom C5-1ax-5 1912  ax5ALT 36113
[Monk2] p. 113Axiom C5-2ax-10 2146
[Monk2] p. 113Axiom C5-3ax-11 2162
[Monk2] p. 114Lemma 21sp 2184
[Monk2] p. 114Lemma 22axc4 2342  hba1-o 36103  hba1 2303
[Monk2] p. 114Lemma 23nfia1 2158
[Monk2] p. 114Lemma 24nfa2 2178  nfra2 3223  nfra2w 3222
[Moore] p. 53Part Idf-mre 16853
[Munkres] p. 77Example 2distop 21596  indistop 21603  indistopon 21602
[Munkres] p. 77Example 3fctop 21605  fctop2 21606
[Munkres] p. 77Example 4cctop 21607
[Munkres] p. 78Definition of basisdf-bases 21547  isbasis3g 21550
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 16713  tgval2 21557
[Munkres] p. 79Remarktgcl 21570
[Munkres] p. 80Lemma 2.1tgval3 21564
[Munkres] p. 80Lemma 2.2tgss2 21588  tgss3 21587
[Munkres] p. 81Lemma 2.3basgen 21589  basgen2 21590
[Munkres] p. 83Exercise 3topdifinf 34678  topdifinfeq 34679  topdifinffin 34677  topdifinfindis 34675
[Munkres] p. 89Definition of subspace topologyresttop 21761
[Munkres] p. 93Theorem 6.1(1)0cld 21639  topcld 21636
[Munkres] p. 93Theorem 6.1(2)iincld 21640
[Munkres] p. 93Theorem 6.1(3)uncld 21642
[Munkres] p. 94Definition of closureclsval 21638
[Munkres] p. 94Definition of interiorntrval 21637
[Munkres] p. 95Theorem 6.5(a)clsndisj 21676  elcls 21674
[Munkres] p. 95Theorem 6.5(b)elcls3 21684
[Munkres] p. 97Theorem 6.6clslp 21749  neindisj 21718
[Munkres] p. 97Corollary 6.7cldlp 21751
[Munkres] p. 97Definition of limit pointislp2 21746  lpval 21740
[Munkres] p. 98Definition of Hausdorff spacedf-haus 21916
[Munkres] p. 102Definition of continuous functiondf-cn 21828  iscn 21836  iscn2 21839
[Munkres] p. 107Theorem 7.2(g)cncnp 21881  cncnp2 21882  cncnpi 21879  df-cnp 21829  iscnp 21838  iscnp2 21840
[Munkres] p. 127Theorem 10.1metcn 23146
[Munkres] p. 128Theorem 10.3metcn4 23911
[Nathanson] p. 123Remarkreprgt 31917  reprinfz1 31918  reprlt 31915
[Nathanson] p. 123Definitiondf-repr 31905
[Nathanson] p. 123Chapter 5.1circlemethnat 31937
[Nathanson] p. 123Propositionbreprexp 31929  breprexpnat 31930  itgexpif 31902
[NielsenChuang] p. 195Equation 4.73unierri 29883
[OeSilva] p. 2042Section 2ax-bgbltosilva 44191
[Pfenning] p. 17Definition XMnatded 28184
[Pfenning] p. 17Definition NNCnatded 28184  notnotrd 135
[Pfenning] p. 17Definition ` `Cnatded 28184
[Pfenning] p. 18Rule"natded 28184
[Pfenning] p. 18Definition /\Inatded 28184
[Pfenning] p. 18Definition ` `Enatded 28184  natded 28184  natded 28184  natded 28184  natded 28184
[Pfenning] p. 18Definition ` `Inatded 28184  natded 28184  natded 28184  natded 28184  natded 28184
[Pfenning] p. 18Definition ` `ELnatded 28184
[Pfenning] p. 18Definition ` `ERnatded 28184
[Pfenning] p. 18Definition ` `Ea,unatded 28184
[Pfenning] p. 18Definition ` `IRnatded 28184
[Pfenning] p. 18Definition ` `Ianatded 28184
[Pfenning] p. 127Definition =Enatded 28184
[Pfenning] p. 127Definition =Inatded 28184
[Ponnusamy] p. 361Theorem 6.44cphip0l 23803  df-dip 28480  dip0l 28497  ip0l 20773
[Ponnusamy] p. 361Equation 6.45cphipval 23843  ipval 28482
[Ponnusamy] p. 362Equation I1dipcj 28493  ipcj 20771
[Ponnusamy] p. 362Equation I3cphdir 23806  dipdir 28621  ipdir 20776  ipdiri 28609
[Ponnusamy] p. 362Equation I4ipidsq 28489  nmsq 23795
[Ponnusamy] p. 362Equation 6.46ip0i 28604
[Ponnusamy] p. 362Equation 6.47ip1i 28606
[Ponnusamy] p. 362Equation 6.48ip2i 28607
[Ponnusamy] p. 363Equation I2cphass 23812  dipass 28624  ipass 20782  ipassi 28620
[Prugovecki] p. 186Definition of brabraval 29723  df-bra 29629
[Prugovecki] p. 376Equation 8.1df-kb 29630  kbval 29733
[PtakPulmannova] p. 66Proposition 3.2.17atomli 30161
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 37094
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 30175  atcvat4i 30176  cvrat3 36648  cvrat4 36649  lsatcvat3 36258
[PtakPulmannova] p. 68Definition 3.2.18cvbr 30061  cvrval 36475  df-cv 30058  df-lcv 36225  lspsncv0 19911
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 37106
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 37107
[Quine] p. 16Definition 2.1df-clab 2803  rabid 3370
[Quine] p. 17Definition 2.1''dfsb7 2287
[Quine] p. 18Definition 2.7df-cleq 2817
[Quine] p. 19Definition 2.9conventions 28181  df-v 3482
[Quine] p. 34Theorem 5.1abeq2 2948
[Quine] p. 35Theorem 5.2abid1 2957  abid2f 3011
[Quine] p. 40Theorem 6.1sb5 2278
[Quine] p. 40Theorem 6.2sb56 2279  sb6 2094
[Quine] p. 41Theorem 6.3df-clel 2896
[Quine] p. 41Theorem 6.4eqid 2824  eqid1 28248
[Quine] p. 41Theorem 6.5eqcom 2831
[Quine] p. 42Theorem 6.6df-sbc 3759
[Quine] p. 42Theorem 6.7dfsbcq 3760  dfsbcq2 3761
[Quine] p. 43Theorem 6.8vex 3483
[Quine] p. 43Theorem 6.9isset 3492
[Quine] p. 44Theorem 7.3spcgf 3576  spcgv 3581  spcimgf 3574
[Quine] p. 44Theorem 6.11spsbc 3771  spsbcd 3772
[Quine] p. 44Theorem 6.12elex 3498
[Quine] p. 44Theorem 6.13elab 3653  elabg 3652  elabgf 3648
[Quine] p. 44Theorem 6.14noel 4279
[Quine] p. 48Theorem 7.2snprc 4637
[Quine] p. 48Definition 7.1df-pr 4552  df-sn 4550
[Quine] p. 49Theorem 7.4snss 4702  snssg 4701
[Quine] p. 49Theorem 7.6prid1 4682  prid1g 4680  prid2 4683  prid2g 4681  snid 4585  snidg 4583
[Quine] p. 51Theorem 7.12snex 5319
[Quine] p. 51Theorem 7.13prex 5320
[Quine] p. 53Theorem 8.2unisn 4844  unisnALT 41489  unisng 4843
[Quine] p. 53Theorem 8.3uniun 4847
[Quine] p. 54Theorem 8.6elssuni 4854
[Quine] p. 54Theorem 8.7uni0 4852
[Quine] p. 56Theorem 8.17uniabio 6316
[Quine] p. 56Definition 8.18dfaiota2 43506  dfiota2 6303
[Quine] p. 57Theorem 8.19aiotaval 43513  iotaval 6317
[Quine] p. 57Theorem 8.22iotanul 6321
[Quine] p. 58Theorem 8.23iotaex 6323
[Quine] p. 58Definition 9.1df-op 4556
[Quine] p. 61Theorem 9.5opabid 5400  opabidw 5399  opelopab 5416  opelopaba 5410  opelopabaf 5418  opelopabf 5419  opelopabg 5412  opelopabga 5407  opelopabgf 5414  oprabid 7177  oprabidw 7176
[Quine] p. 64Definition 9.11df-xp 5548
[Quine] p. 64Definition 9.12df-cnv 5550
[Quine] p. 64Definition 9.15df-id 5447
[Quine] p. 65Theorem 10.3fun0 6407
[Quine] p. 65Theorem 10.4funi 6375
[Quine] p. 65Theorem 10.5funsn 6395  funsng 6393
[Quine] p. 65Definition 10.1df-fun 6345
[Quine] p. 65Definition 10.2args 5944  dffv4 6655
[Quine] p. 68Definition 10.11conventions 28181  df-fv 6351  fv2 6653
[Quine] p. 124Theorem 17.3nn0opth2 13633  nn0opth2i 13632  nn0opthi 13631  omopthi 8274
[Quine] p. 177Definition 25.2df-rdg 8036
[Quine] p. 232Equation icarddom 9968
[Quine] p. 284Axiom 39(vi)funimaex 6429  funimaexg 6428
[Quine] p. 331Axiom system NFru 3757
[ReedSimon] p. 36Definition (iii)ax-his3 28863
[ReedSimon] p. 63Exercise 4(a)df-dip 28480  polid 28938  polid2i 28936  polidi 28937
[ReedSimon] p. 63Exercise 4(b)df-ph 28592
[ReedSimon] p. 195Remarklnophm 29798  lnophmi 29797
[Retherford] p. 49Exercise 1(ii)leopmul 29913  leopmuli 29912
[Retherford] p. 49Exercise 1(iv)leoptr 29916
[Retherford] p. 49Definition VI.1df-leop 29631  leoppos 29905
[Retherford] p. 49Exercise 1(iii)leoptri 29915
[Retherford] p. 49Definition of operator orderingleop3 29904
[Roman] p. 4Definitiondf-dmat 21092  df-dmatalt 44669
[Roman] p. 18Part Preliminariesdf-rng0 44362
[Roman] p. 19Part Preliminariesdf-ring 19295
[Roman] p. 46Theorem 1.6isldepslvec2 44756
[Roman] p. 112Noteisldepslvec2 44756  ldepsnlinc 44779  zlmodzxznm 44768
[Roman] p. 112Examplezlmodzxzequa 44767  zlmodzxzequap 44770  zlmodzxzldep 44775
[Roman] p. 170Theorem 7.8cayleyhamilton 21491
[Rosenlicht] p. 80Theoremheicant 35002
[Rosser] p. 281Definitiondf-op 4556
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 31941
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 31942
[Rotman] p. 28Remarkpgrpgt2nabl 44630  pmtr3ncom 18599
[Rotman] p. 31Theorem 3.4symggen2 18595
[Rotman] p. 42Theorem 3.15cayley 18538  cayleyth 18539
[Rudin] p. 164Equation 27efcan 15445
[Rudin] p. 164Equation 30efzval 15451
[Rudin] p. 167Equation 48absefi 15545
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1773
[Sanford] p. 39Rule 4mptxor 1771
[Sanford] p. 40Rule 1mptnan 1770
[Schechter] p. 51Definition of antisymmetryintasym 5962
[Schechter] p. 51Definition of irreflexivityintirr 5965
[Schechter] p. 51Definition of symmetrycnvsym 5961
[Schechter] p. 51Definition of transitivitycotr 5959
[Schechter] p. 78Definition of Moore collection of setsdf-mre 16853
[Schechter] p. 79Definition of Moore closuredf-mrc 16854
[Schechter] p. 82Section 4.5df-mrc 16854
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 16856
[Schechter] p. 139Definition AC3dfac9 9554
[Schechter] p. 141Definition (MC)dfac11 39859
[Schechter] p. 149Axiom DC1ax-dc 9860  axdc3 9868
[Schechter] p. 187Definition of ring with unitisring 19297  isrngo 35245
[Schechter] p. 276Remark 11.6.espan0 29321
[Schechter] p. 276Definition of spandf-span 29088  spanval 29112
[Schechter] p. 428Definition 15.35bastop1 21594
[Schwabhauser] p. 10Axiom A1axcgrrflx 26704  axtgcgrrflx 26252
[Schwabhauser] p. 10Axiom A2axcgrtr 26705
[Schwabhauser] p. 10Axiom A3axcgrid 26706  axtgcgrid 26253
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 26238
[Schwabhauser] p. 11Axiom A4axsegcon 26717  axtgsegcon 26254  df-trkgcb 26240
[Schwabhauser] p. 11Axiom A5ax5seg 26728  axtg5seg 26255  df-trkgcb 26240
[Schwabhauser] p. 11Axiom A6axbtwnid 26729  axtgbtwnid 26256  df-trkgb 26239
[Schwabhauser] p. 12Axiom A7axpasch 26731  axtgpasch 26257  df-trkgb 26239
[Schwabhauser] p. 12Axiom A8axlowdim2 26750  df-trkg2d 31961
[Schwabhauser] p. 13Axiom A8axtglowdim2 26260
[Schwabhauser] p. 13Axiom A9axtgupdim2 26261  df-trkg2d 31961
[Schwabhauser] p. 13Axiom A10axeuclid 26753  axtgeucl 26262  df-trkge 26241
[Schwabhauser] p. 13Axiom A11axcont 26766  axtgcont 26259  axtgcont1 26258  df-trkgb 26239
[Schwabhauser] p. 27Theorem 2.1cgrrflx 33473
[Schwabhauser] p. 27Theorem 2.2cgrcomim 33475
[Schwabhauser] p. 27Theorem 2.3cgrtr 33478
[Schwabhauser] p. 27Theorem 2.4cgrcoml 33482
[Schwabhauser] p. 27Theorem 2.5cgrcomr 33483  tgcgrcomimp 26267  tgcgrcoml 26269  tgcgrcomr 26268
[Schwabhauser] p. 28Theorem 2.8cgrtriv 33488  tgcgrtriv 26274
[Schwabhauser] p. 28Theorem 2.105segofs 33492  tg5segofs 31969
[Schwabhauser] p. 28Definition 2.10df-afs 31966  df-ofs 33469
[Schwabhauser] p. 29Theorem 2.11cgrextend 33494  tgcgrextend 26275
[Schwabhauser] p. 29Theorem 2.12segconeq 33496  tgsegconeq 26276
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 33508  btwntriv2 33498  tgbtwntriv2 26277
[Schwabhauser] p. 30Theorem 3.2btwncomim 33499  tgbtwncom 26278
[Schwabhauser] p. 30Theorem 3.3btwntriv1 33502  tgbtwntriv1 26281
[Schwabhauser] p. 30Theorem 3.4btwnswapid 33503  tgbtwnswapid 26282
[Schwabhauser] p. 30Theorem 3.5btwnexch2 33509  btwnintr 33505  tgbtwnexch2 26286  tgbtwnintr 26283
[Schwabhauser] p. 30Theorem 3.6btwnexch 33511  btwnexch3 33506  tgbtwnexch 26288  tgbtwnexch3 26284
[Schwabhauser] p. 30Theorem 3.7btwnouttr 33510  tgbtwnouttr 26287  tgbtwnouttr2 26285
[Schwabhauser] p. 32Theorem 3.13axlowdim1 26749
[Schwabhauser] p. 32Theorem 3.14btwndiff 33513  tgbtwndiff 26296
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 26289  trisegint 33514
[Schwabhauser] p. 34Theorem 4.2ifscgr 33530  tgifscgr 26298
[Schwabhauser] p. 34Theorem 4.11colcom 26348  colrot1 26349  colrot2 26350  lncom 26412  lnrot1 26413  lnrot2 26414
[Schwabhauser] p. 34Definition 4.1df-ifs 33526
[Schwabhauser] p. 35Theorem 4.3cgrsub 33531  tgcgrsub 26299
[Schwabhauser] p. 35Theorem 4.5cgrxfr 33541  tgcgrxfr 26308
[Schwabhauser] p. 35Statement 4.4ercgrg 26307
[Schwabhauser] p. 35Definition 4.4df-cgr3 33527  df-cgrg 26301
[Schwabhauser] p. 35Definition instead (givendf-cgrg 26301
[Schwabhauser] p. 36Theorem 4.6btwnxfr 33542  tgbtwnxfr 26320
[Schwabhauser] p. 36Theorem 4.11colinearperm1 33548  colinearperm2 33550  colinearperm3 33549  colinearperm4 33551  colinearperm5 33552
[Schwabhauser] p. 36Definition 4.8df-ismt 26323
[Schwabhauser] p. 36Definition 4.10df-colinear 33525  tgellng 26343  tglng 26336
[Schwabhauser] p. 37Theorem 4.12colineartriv1 33553
[Schwabhauser] p. 37Theorem 4.13colinearxfr 33561  lnxfr 26356
[Schwabhauser] p. 37Theorem 4.14lineext 33562  lnext 26357
[Schwabhauser] p. 37Theorem 4.16fscgr 33566  tgfscgr 26358
[Schwabhauser] p. 37Theorem 4.17linecgr 33567  lncgr 26359
[Schwabhauser] p. 37Definition 4.15df-fs 33528
[Schwabhauser] p. 38Theorem 4.18lineid 33569  lnid 26360
[Schwabhauser] p. 38Theorem 4.19idinside 33570  tgidinside 26361
[Schwabhauser] p. 39Theorem 5.1btwnconn1 33587  tgbtwnconn1 26365
[Schwabhauser] p. 41Theorem 5.2btwnconn2 33588  tgbtwnconn2 26366
[Schwabhauser] p. 41Theorem 5.3btwnconn3 33589  tgbtwnconn3 26367
[Schwabhauser] p. 41Theorem 5.5brsegle2 33595
[Schwabhauser] p. 41Definition 5.4df-segle 33593  legov 26375
[Schwabhauser] p. 41Definition 5.5legov2 26376
[Schwabhauser] p. 42Remark 5.13legso 26389
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 33596
[Schwabhauser] p. 42Theorem 5.7seglerflx 33598
[Schwabhauser] p. 42Theorem 5.8segletr 33600
[Schwabhauser] p. 42Theorem 5.9segleantisym 33601
[Schwabhauser] p. 42Theorem 5.10seglelin 33602
[Schwabhauser] p. 42Theorem 5.11seglemin 33599
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 33604
[Schwabhauser] p. 42Proposition 5.7legid 26377
[Schwabhauser] p. 42Proposition 5.8legtrd 26379
[Schwabhauser] p. 42Proposition 5.9legtri3 26380
[Schwabhauser] p. 42Proposition 5.10legtrid 26381
[Schwabhauser] p. 42Proposition 5.11leg0 26382
[Schwabhauser] p. 43Theorem 6.2btwnoutside 33611
[Schwabhauser] p. 43Theorem 6.3broutsideof3 33612
[Schwabhauser] p. 43Theorem 6.4broutsideof 33607  df-outsideof 33606
[Schwabhauser] p. 43Definition 6.1broutsideof2 33608  ishlg 26392
[Schwabhauser] p. 44Theorem 6.4hlln 26397
[Schwabhauser] p. 44Theorem 6.5hlid 26399  outsideofrflx 33613
[Schwabhauser] p. 44Theorem 6.6hlcomb 26393  hlcomd 26394  outsideofcom 33614
[Schwabhauser] p. 44Theorem 6.7hltr 26400  outsideoftr 33615
[Schwabhauser] p. 44Theorem 6.11hlcgreu 26408  outsideofeu 33617
[Schwabhauser] p. 44Definition 6.8df-ray 33624
[Schwabhauser] p. 45Part 2df-lines2 33625
[Schwabhauser] p. 45Theorem 6.13outsidele 33618
[Schwabhauser] p. 45Theorem 6.15lineunray 33633
[Schwabhauser] p. 45Theorem 6.16lineelsb2 33634  tglineelsb2 26422
[Schwabhauser] p. 45Theorem 6.17linecom 33636  linerflx1 33635  linerflx2 33637  tglinecom 26425  tglinerflx1 26423  tglinerflx2 26424
[Schwabhauser] p. 45Theorem 6.18linethru 33639  tglinethru 26426
[Schwabhauser] p. 45Definition 6.14df-line2 33623  tglng 26336
[Schwabhauser] p. 45Proposition 6.13legbtwn 26384
[Schwabhauser] p. 46Theorem 6.19linethrueu 33642  tglinethrueu 26429
[Schwabhauser] p. 46Theorem 6.21lineintmo 33643  tglineineq 26433  tglineinteq 26435  tglineintmo 26432
[Schwabhauser] p. 46Theorem 6.23colline 26439
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 26440
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 26441
[Schwabhauser] p. 49Theorem 7.3mirinv 26456
[Schwabhauser] p. 49Theorem 7.7mirmir 26452
[Schwabhauser] p. 49Theorem 7.8mirreu3 26444
[Schwabhauser] p. 49Definition 7.5df-mir 26443  ismir 26449  mirbtwn 26448  mircgr 26447  mirfv 26446  mirval 26445
[Schwabhauser] p. 50Theorem 7.8mirreu 26454
[Schwabhauser] p. 50Theorem 7.9mireq 26455
[Schwabhauser] p. 50Theorem 7.10mirinv 26456
[Schwabhauser] p. 50Theorem 7.11mirf1o 26459
[Schwabhauser] p. 50Theorem 7.13miriso 26460
[Schwabhauser] p. 51Theorem 7.14mirmot 26465
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 26462  mirbtwni 26461
[Schwabhauser] p. 51Theorem 7.16mircgrs 26463
[Schwabhauser] p. 51Theorem 7.17miduniq 26475
[Schwabhauser] p. 52Theorem 7.18miduniq1 26476
[Schwabhauser] p. 52Theorem 7.19miduniq2 26477
[Schwabhauser] p. 52Theorem 7.20colmid 26478
[Schwabhauser] p. 53Lemma 7.22krippen 26481
[Schwabhauser] p. 55Lemma 7.25midexlem 26482
[Schwabhauser] p. 57Theorem 8.2ragcom 26488
[Schwabhauser] p. 57Definition 8.1df-rag 26484  israg 26487
[Schwabhauser] p. 58Theorem 8.3ragcol 26489
[Schwabhauser] p. 58Theorem 8.4ragmir 26490
[Schwabhauser] p. 58Theorem 8.5ragtrivb 26492
[Schwabhauser] p. 58Theorem 8.6ragflat2 26493
[Schwabhauser] p. 58Theorem 8.7ragflat 26494
[Schwabhauser] p. 58Theorem 8.8ragtriva 26495
[Schwabhauser] p. 58Theorem 8.9ragflat3 26496  ragncol 26499
[Schwabhauser] p. 58Theorem 8.10ragcgr 26497
[Schwabhauser] p. 59Theorem 8.12perpcom 26503
[Schwabhauser] p. 59Theorem 8.13ragperp 26507
[Schwabhauser] p. 59Theorem 8.14perpneq 26504
[Schwabhauser] p. 59Definition 8.11df-perpg 26486  isperp 26502
[Schwabhauser] p. 59Definition 8.13isperp2 26505
[Schwabhauser] p. 60Theorem 8.18foot 26512
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 26520  colperpexlem2 26521
[Schwabhauser] p. 63Theorem 8.21colperpex 26523  colperpexlem3 26522
[Schwabhauser] p. 64Theorem 8.22mideu 26528  midex 26527
[Schwabhauser] p. 66Lemma 8.24opphllem 26525
[Schwabhauser] p. 67Theorem 9.2oppcom 26534
[Schwabhauser] p. 67Definition 9.1islnopp 26529
[Schwabhauser] p. 68Lemma 9.3opphllem2 26538
[Schwabhauser] p. 68Lemma 9.4opphllem5 26541  opphllem6 26542
[Schwabhauser] p. 69Theorem 9.5opphl 26544
[Schwabhauser] p. 69Theorem 9.6axtgpasch 26257
[Schwabhauser] p. 70Theorem 9.6outpasch 26545
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 26553
[Schwabhauser] p. 71Definition 9.7df-hpg 26548  hpgbr 26550
[Schwabhauser] p. 72Lemma 9.10hpgerlem 26555
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 26554
[Schwabhauser] p. 72Theorem 9.11hpgid 26556
[Schwabhauser] p. 72Theorem 9.12hpgcom 26557
[Schwabhauser] p. 72Theorem 9.13hpgtr 26558
[Schwabhauser] p. 73Theorem 9.18colopp 26559
[Schwabhauser] p. 73Theorem 9.19colhp 26560
[Schwabhauser] p. 88Theorem 10.2lmieu 26574
[Schwabhauser] p. 88Definition 10.1df-mid 26564
[Schwabhauser] p. 89Theorem 10.4lmicom 26578
[Schwabhauser] p. 89Theorem 10.5lmilmi 26579
[Schwabhauser] p. 89Theorem 10.6lmireu 26580
[Schwabhauser] p. 89Theorem 10.7lmieq 26581
[Schwabhauser] p. 89Theorem 10.8lmiinv 26582
[Schwabhauser] p. 89Theorem 10.9lmif1o 26585
[Schwabhauser] p. 89Theorem 10.10lmiiso 26587
[Schwabhauser] p. 89Definition 10.3df-lmi 26565
[Schwabhauser] p. 90Theorem 10.11lmimot 26588
[Schwabhauser] p. 91Theorem 10.12hypcgr 26591
[Schwabhauser] p. 92Theorem 10.14lmiopp 26592
[Schwabhauser] p. 92Theorem 10.15lnperpex 26593
[Schwabhauser] p. 92Theorem 10.16trgcopy 26594  trgcopyeu 26596
[Schwabhauser] p. 95Definition 11.2dfcgra2 26620
[Schwabhauser] p. 95Definition 11.3iscgra 26599
[Schwabhauser] p. 95Proposition 11.4cgracgr 26608
[Schwabhauser] p. 95Proposition 11.10cgrahl1 26606  cgrahl2 26607
[Schwabhauser] p. 96Theorem 11.6cgraid 26609
[Schwabhauser] p. 96Theorem 11.9cgraswap 26610
[Schwabhauser] p. 97Theorem 11.7cgracom 26612
[Schwabhauser] p. 97Theorem 11.8cgratr 26613
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 26616  cgrahl 26617
[Schwabhauser] p. 98Theorem 11.13sacgr 26621
[Schwabhauser] p. 98Theorem 11.14oacgr 26622
[Schwabhauser] p. 98Theorem 11.15acopy 26623  acopyeu 26624
[Schwabhauser] p. 101Theorem 11.24inagswap 26631
[Schwabhauser] p. 101Theorem 11.25inaghl 26635
[Schwabhauser] p. 101Definition 11.23isinag 26628
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 26643
[Schwabhauser] p. 102Definition 11.27df-leag 26636  isleag 26637
[Schwabhauser] p. 107Theorem 11.49tgsas 26645  tgsas1 26644  tgsas2 26646  tgsas3 26647
[Schwabhauser] p. 108Theorem 11.50tgasa 26649  tgasa1 26648
[Schwabhauser] p. 109Theorem 11.51tgsss1 26650  tgsss2 26651  tgsss3 26652
[Shapiro] p. 230Theorem 6.5.1dchrhash 25851  dchrsum 25849  dchrsum2 25848  sumdchr 25852
[Shapiro] p. 232Theorem 6.5.2dchr2sum 25853  sum2dchr 25854
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19184  ablfacrp2 19185
[Shapiro], p. 328Equation 9.2.4vmasum 25796
[Shapiro], p. 329Equation 9.2.7logfac2 25797
[Shapiro], p. 329Equation 9.2.9logfacrlim 25804
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 26065
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 26119  vmalogdivsum2 26118
[Shapiro], p. 375Theorem 9.4.1dirith 26109  dirith2 26108
[Shapiro], p. 375Equation 9.4.3rplogsum 26107  rpvmasum 26106  rpvmasum2 26092
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 26067
[Shapiro], p. 376Equation 9.4.8dchrvmasum 26105
[Shapiro], p. 377Lemma 9.4.1dchrisum 26072  dchrisumlem1 26069  dchrisumlem2 26070  dchrisumlem3 26071  dchrisumlema 26068
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 26075
[Shapiro], p. 379Equation 9.4.16dchrmusum 26104  dchrmusumlem 26102  dchrvmasumlem 26103
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 26074
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 26076
[Shapiro], p. 382Lemma 9.4.4dchrisum0 26100  dchrisum0re 26093  dchrisumn0 26101
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 26086
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 26090
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 26091
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 26146  pntrsumbnd2 26147  pntrsumo1 26145
[Shapiro], p. 405Equation 10.2.1mudivsum 26110
[Shapiro], p. 406Equation 10.2.6mulogsum 26112
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 26114
[Shapiro], p. 407Equation 10.2.8mulog2sum 26117
[Shapiro], p. 418Equation 10.4.6logsqvma 26122
[Shapiro], p. 418Equation 10.4.8logsqvma2 26123
[Shapiro], p. 419Equation 10.4.10selberg 26128
[Shapiro], p. 420Equation 10.4.12selberg2lem 26130
[Shapiro], p. 420Equation 10.4.14selberg2 26131
[Shapiro], p. 422Equation 10.6.7selberg3 26139
[Shapiro], p. 422Equation 10.4.20selberg4lem1 26140
[Shapiro], p. 422Equation 10.4.21selberg3lem1 26137  selberg3lem2 26138
[Shapiro], p. 422Equation 10.4.23selberg4 26141
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 26135
[Shapiro], p. 428Equation 10.6.2selbergr 26148
[Shapiro], p. 429Equation 10.6.8selberg3r 26149
[Shapiro], p. 430Equation 10.6.11selberg4r 26150
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 26164
[Shapiro], p. 434Equation 10.6.27pntlema 26176  pntlemb 26177  pntlemc 26175  pntlemd 26174  pntlemg 26178
[Shapiro], p. 435Equation 10.6.29pntlema 26176
[Shapiro], p. 436Lemma 10.6.1pntpbnd 26168
[Shapiro], p. 436Lemma 10.6.2pntibnd 26173
[Shapiro], p. 436Equation 10.6.34pntlema 26176
[Shapiro], p. 436Equation 10.6.35pntlem3 26189  pntleml 26191
[Stoll] p. 13Definition corresponds to dfsymdif3 4253
[Stoll] p. 16Exercise 4.40dif 4337  dif0 4314
[Stoll] p. 16Exercise 4.8difdifdir 4419
[Stoll] p. 17Theorem 5.1(5)unvdif 4405
[Stoll] p. 19Theorem 5.2(13)undm 4246
[Stoll] p. 19Theorem 5.2(13')indm 4247
[Stoll] p. 20Remarkinvdif 4229
[Stoll] p. 25Definition of ordered tripledf-ot 4558
[Stoll] p. 43Definitionuniiun 4968
[Stoll] p. 44Definitionintiin 4969
[Stoll] p. 45Definitiondf-iin 4908
[Stoll] p. 45Definition indexed uniondf-iun 4907
[Stoll] p. 176Theorem 3.4(27)iman 405
[Stoll] p. 262Example 4.1dfsymdif3 4253
[Strang] p. 242Section 6.3expgrowth 40896
[Suppes] p. 22Theorem 2eq0 4290  eq0f 4287
[Suppes] p. 22Theorem 4eqss 3967  eqssd 3969  eqssi 3968
[Suppes] p. 23Theorem 5ss0 4334  ss0b 4333
[Suppes] p. 23Theorem 6sstr 3960  sstrALT2 41398
[Suppes] p. 23Theorem 7pssirr 4062
[Suppes] p. 23Theorem 8pssn2lp 4063
[Suppes] p. 23Theorem 9psstr 4066
[Suppes] p. 23Theorem 10pssss 4057
[Suppes] p. 25Theorem 12elin 3935  elun 4110
[Suppes] p. 26Theorem 15inidm 4179
[Suppes] p. 26Theorem 16in0 4327
[Suppes] p. 27Theorem 23unidm 4113
[Suppes] p. 27Theorem 24un0 4326
[Suppes] p. 27Theorem 25ssun1 4133
[Suppes] p. 27Theorem 26ssequn1 4141
[Suppes] p. 27Theorem 27unss 4145
[Suppes] p. 27Theorem 28indir 4236
[Suppes] p. 27Theorem 29undir 4237
[Suppes] p. 28Theorem 32difid 4312
[Suppes] p. 29Theorem 33difin 4222
[Suppes] p. 29Theorem 34indif 4230
[Suppes] p. 29Theorem 35undif1 4406
[Suppes] p. 29Theorem 36difun2 4411
[Suppes] p. 29Theorem 37difin0 4404
[Suppes] p. 29Theorem 38disjdif 4403
[Suppes] p. 29Theorem 39difundi 4240
[Suppes] p. 29Theorem 40difindi 4242
[Suppes] p. 30Theorem 41nalset 5203
[Suppes] p. 39Theorem 61uniss 4832
[Suppes] p. 39Theorem 65uniop 5392
[Suppes] p. 41Theorem 70intsn 4898
[Suppes] p. 42Theorem 71intpr 4895  intprg 4896
[Suppes] p. 42Theorem 73op1stb 5350
[Suppes] p. 42Theorem 78intun 4894
[Suppes] p. 44Definition 15(a)dfiun2 4944  dfiun2g 4941
[Suppes] p. 44Definition 15(b)dfiin2 4945
[Suppes] p. 47Theorem 86elpw 4525  elpw2 5234  elpw2g 5233  elpwg 4524  elpwgdedVD 41480
[Suppes] p. 47Theorem 87pwid 4545
[Suppes] p. 47Theorem 89pw0 4729
[Suppes] p. 48Theorem 90pwpw0 4730
[Suppes] p. 52Theorem 101xpss12 5557
[Suppes] p. 52Theorem 102xpindi 5691  xpindir 5692
[Suppes] p. 52Theorem 103xpundi 5607  xpundir 5608
[Suppes] p. 54Theorem 105elirrv 9051
[Suppes] p. 58Theorem 2relss 5643
[Suppes] p. 59Theorem 4eldm 5756  eldm2 5757  eldm2g 5755  eldmg 5754
[Suppes] p. 59Definition 3df-dm 5552
[Suppes] p. 60Theorem 6dmin 5767
[Suppes] p. 60Theorem 8rnun 5991
[Suppes] p. 60Theorem 9rnin 5992
[Suppes] p. 60Definition 4dfrn2 5746
[Suppes] p. 61Theorem 11brcnv 5740  brcnvg 5737
[Suppes] p. 62Equation 5elcnv 5734  elcnv2 5735
[Suppes] p. 62Theorem 12relcnv 5954
[Suppes] p. 62Theorem 15cnvin 5990
[Suppes] p. 62Theorem 16cnvun 5988
[Suppes] p. 63Definitiondftrrels2 35881
[Suppes] p. 63Theorem 20co02 6100
[Suppes] p. 63Theorem 21dmcoss 5829
[Suppes] p. 63Definition 7df-co 5551
[Suppes] p. 64Theorem 26cnvco 5743
[Suppes] p. 64Theorem 27coass 6105
[Suppes] p. 65Theorem 31resundi 5854
[Suppes] p. 65Theorem 34elima 5921  elima2 5922  elima3 5923  elimag 5920
[Suppes] p. 65Theorem 35imaundi 5995
[Suppes] p. 66Theorem 40dminss 5997
[Suppes] p. 66Theorem 41imainss 5998
[Suppes] p. 67Exercise 11cnvxp 6001
[Suppes] p. 81Definition 34dfec2 8282
[Suppes] p. 82Theorem 72elec 8323  elecALTV 35597  elecg 8322
[Suppes] p. 82Theorem 73eqvrelth 35916  erth 8328  erth2 8329
[Suppes] p. 83Theorem 74eqvreldisj 35919  erdisj 8331
[Suppes] p. 89Theorem 96map0b 8437
[Suppes] p. 89Theorem 97map0 8441  map0g 8438
[Suppes] p. 89Theorem 98mapsn 8442  mapsnd 8440
[Suppes] p. 89Theorem 99mapss 8443
[Suppes] p. 91Definition 12(ii)alephsuc 9486
[Suppes] p. 91Definition 12(iii)alephlim 9485
[Suppes] p. 92Theorem 1enref 8532  enrefg 8531
[Suppes] p. 92Theorem 2ensym 8548  ensymb 8547  ensymi 8549
[Suppes] p. 92Theorem 3entr 8551
[Suppes] p. 92Theorem 4unen 8586
[Suppes] p. 94Theorem 15endom 8526
[Suppes] p. 94Theorem 16ssdomg 8545
[Suppes] p. 94Theorem 17domtr 8552
[Suppes] p. 95Theorem 18sbth 8628
[Suppes] p. 97Theorem 23canth2 8661  canth2g 8662
[Suppes] p. 97Definition 3brsdom2 8632  df-sdom 8502  dfsdom2 8631
[Suppes] p. 97Theorem 21(i)sdomirr 8645
[Suppes] p. 97Theorem 22(i)domnsym 8634
[Suppes] p. 97Theorem 21(ii)sdomnsym 8633
[Suppes] p. 97Theorem 22(ii)domsdomtr 8643
[Suppes] p. 97Theorem 22(iv)brdom2 8529
[Suppes] p. 97Theorem 21(iii)sdomtr 8646
[Suppes] p. 97Theorem 22(iii)sdomdomtr 8641
[Suppes] p. 98Exercise 4fundmen 8573  fundmeng 8574
[Suppes] p. 98Exercise 6xpdom3 8605
[Suppes] p. 98Exercise 11sdomentr 8642
[Suppes] p. 104Theorem 37fofi 8801
[Suppes] p. 104Theorem 38pwfi 8810
[Suppes] p. 105Theorem 40pwfi 8810
[Suppes] p. 111Axiom for cardinal numberscarden 9965
[Suppes] p. 130Definition 3df-tr 5159
[Suppes] p. 132Theorem 9ssonuni 7491
[Suppes] p. 134Definition 6df-suc 6184
[Suppes] p. 136Theorem Schema 22findes 7602  finds 7598  finds1 7601  finds2 7600
[Suppes] p. 151Theorem 42isfinite 9106  isfinite2 8767  isfiniteg 8769  unbnn 8765
[Suppes] p. 162Definition 5df-ltnq 10332  df-ltpq 10324
[Suppes] p. 197Theorem Schema 4tfindes 7567  tfinds 7564  tfinds2 7568
[Suppes] p. 209Theorem 18oaord1 8167
[Suppes] p. 209Theorem 21oaword2 8169
[Suppes] p. 211Theorem 25oaass 8177
[Suppes] p. 225Definition 8iscard2 9396
[Suppes] p. 227Theorem 56ondomon 9977
[Suppes] p. 228Theorem 59harcard 9398
[Suppes] p. 228Definition 12(i)aleph0 9484
[Suppes] p. 228Theorem Schema 61onintss 6228
[Suppes] p. 228Theorem Schema 62onminesb 7503  onminsb 7504
[Suppes] p. 229Theorem 64alephval2 9986
[Suppes] p. 229Theorem 65alephcard 9488
[Suppes] p. 229Theorem 66alephord2i 9495
[Suppes] p. 229Theorem 67alephnbtwn 9489
[Suppes] p. 229Definition 12df-aleph 9360
[Suppes] p. 242Theorem 6weth 9909
[Suppes] p. 242Theorem 8entric 9971
[Suppes] p. 242Theorem 9carden 9965
[TakeutiZaring] p. 8Axiom 1ax-ext 2796
[TakeutiZaring] p. 13Definition 4.5df-cleq 2817
[TakeutiZaring] p. 13Proposition 4.6df-clel 2896
[TakeutiZaring] p. 13Proposition 4.9cvjust 2819
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2844
[TakeutiZaring] p. 14Definition 4.16df-oprab 7149
[TakeutiZaring] p. 14Proposition 4.14ru 3757
[TakeutiZaring] p. 15Axiom 2zfpair 5309
[TakeutiZaring] p. 15Exercise 1elpr 4572  elpr2 4574  elpr2g 4573  elprg 4570
[TakeutiZaring] p. 15Exercise 2elsn 4564  elsn2 4588  elsn2g 4587  elsng 4563  velsn 4565
[TakeutiZaring] p. 15Exercise 3elop 5346
[TakeutiZaring] p. 15Exercise 4sneq 4559  sneqr 4755
[TakeutiZaring] p. 15Definition 5.1dfpr2 4568  dfsn2 4562  dfsn2ALT 4569
[TakeutiZaring] p. 16Axiom 3uniex 7457
[TakeutiZaring] p. 16Exercise 6opth 5355
[TakeutiZaring] p. 16Exercise 7opex 5343
[TakeutiZaring] p. 16Exercise 8rext 5328
[TakeutiZaring] p. 16Corollary 5.8unex 7459  unexg 7462
[TakeutiZaring] p. 16Definition 5.3dftp2 4611
[TakeutiZaring] p. 16Definition 5.5df-uni 4825
[TakeutiZaring] p. 16Definition 5.6df-in 3926  df-un 3924
[TakeutiZaring] p. 16Proposition 5.7unipr 4841  uniprg 4842
[TakeutiZaring] p. 17Axiom 4vpwex 5265
[TakeutiZaring] p. 17Exercise 1eltp 4610
[TakeutiZaring] p. 17Exercise 5elsuc 6247  elsucg 6245  sstr2 3959
[TakeutiZaring] p. 17Exercise 6uncom 4114
[TakeutiZaring] p. 17Exercise 7incom 4162
[TakeutiZaring] p. 17Exercise 8unass 4127
[TakeutiZaring] p. 17Exercise 9inass 4180
[TakeutiZaring] p. 17Exercise 10indi 4234
[TakeutiZaring] p. 17Exercise 11undi 4235
[TakeutiZaring] p. 17Definition 5.9df-pss 3938  dfss2 3939
[TakeutiZaring] p. 17Definition 5.10df-pw 4523
[TakeutiZaring] p. 18Exercise 7unss2 4142
[TakeutiZaring] p. 18Exercise 9df-ss 3936  sseqin2 4176
[TakeutiZaring] p. 18Exercise 10ssid 3974
[TakeutiZaring] p. 18Exercise 12inss1 4189  inss2 4190
[TakeutiZaring] p. 18Exercise 13nss 4014
[TakeutiZaring] p. 18Exercise 15unieq 4835
[TakeutiZaring] p. 18Exercise 18sspwb 5329  sspwimp 41481  sspwimpALT 41488  sspwimpALT2 41491  sspwimpcf 41483
[TakeutiZaring] p. 18Exercise 19pweqb 5336
[TakeutiZaring] p. 19Axiom 5ax-rep 5176
[TakeutiZaring] p. 20Definitiondf-rab 3142  df-wl-rab 34935
[TakeutiZaring] p. 20Corollary 5.160ex 5197
[TakeutiZaring] p. 20Definition 5.12df-dif 3922
[TakeutiZaring] p. 20Definition 5.14dfnul2 4277
[TakeutiZaring] p. 20Proposition 5.15difid 4312
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4292  n0f 4289  neq0 4291  neq0f 4288
[TakeutiZaring] p. 21Axiom 6zfreg 9050
[TakeutiZaring] p. 21Axiom 6'zfregs 9165
[TakeutiZaring] p. 21Theorem 5.22setind 9167
[TakeutiZaring] p. 21Definition 5.20df-v 3482
[TakeutiZaring] p. 21Proposition 5.21vprc 5205
[TakeutiZaring] p. 22Exercise 10ss 4332
[TakeutiZaring] p. 22Exercise 3ssex 5211  ssexg 5213
[TakeutiZaring] p. 22Exercise 4inex1 5207
[TakeutiZaring] p. 22Exercise 5ruv 9057
[TakeutiZaring] p. 22Exercise 6elirr 9052
[TakeutiZaring] p. 22Exercise 7ssdif0 4305
[TakeutiZaring] p. 22Exercise 11difdif 4092
[TakeutiZaring] p. 22Exercise 13undif3 4249  undif3VD 41445
[TakeutiZaring] p. 22Exercise 14difss 4093
[TakeutiZaring] p. 22Exercise 15sscon 4100
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3138
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3139
[TakeutiZaring] p. 23Proposition 6.2xpex 7466  xpexg 7463
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5549
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6413
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6572  fun11 6416
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6355  svrelfun 6414
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5745
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5747
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5554
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5555
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5551
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6038  dfrel2 6033
[TakeutiZaring] p. 25Exercise 3xpss 5558
[TakeutiZaring] p. 25Exercise 5relun 5671
[TakeutiZaring] p. 25Exercise 6reluni 5678
[TakeutiZaring] p. 25Exercise 9inxp 5690
[TakeutiZaring] p. 25Exercise 12relres 5869
[TakeutiZaring] p. 25Exercise 13opelres 5846  opelresi 5848
[TakeutiZaring] p. 25Exercise 14dmres 5862
[TakeutiZaring] p. 25Exercise 15resss 5865
[TakeutiZaring] p. 25Exercise 17resabs1 5870
[TakeutiZaring] p. 25Exercise 18funres 6385
[TakeutiZaring] p. 25Exercise 24relco 6084
[TakeutiZaring] p. 25Exercise 29funco 6383
[TakeutiZaring] p. 25Exercise 30f1co 6573
[TakeutiZaring] p. 26Definition 6.10eu2 2696
[TakeutiZaring] p. 26Definition 6.11conventions 28181  df-fv 6351  fv3 6676
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7620  cnvexg 7619
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7606  dmexg 7603
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7607  rnexg 7604
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 41015
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7615
[TakeutiZaring] p. 27Corollary 6.13fvex 6671
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 43593  tz6.12-1-afv2 43660  tz6.12-1 6680  tz6.12-afv 43592  tz6.12-afv2 43659  tz6.12 6681  tz6.12c-afv2 43661  tz6.12c 6683
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 43656  tz6.12-2 6648  tz6.12i-afv2 43662  tz6.12i 6684
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6346
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6347
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6349  wfo 6341
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6348  wf1 6340
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6350  wf1o 6342
[TakeutiZaring] p. 28Exercise 4eqfnfv 6790  eqfnfv2 6791  eqfnfv2f 6794
[TakeutiZaring] p. 28Exercise 5fvco 6747
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 6968
[TakeutiZaring] p. 28Proposition 6.17resfunexg 6966
[TakeutiZaring] p. 29Exercise 9funimaex 6429  funimaexg 6428
[TakeutiZaring] p. 29Definition 6.18df-br 5053
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5462
[TakeutiZaring] p. 30Definition 6.21dffr2 5507  dffr3 5949  eliniseg 5945  iniseg 5947
[TakeutiZaring] p. 30Definition 6.22df-eprel 5452
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5520  fr3nr 7484  frirr 5519
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5501
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7486
[TakeutiZaring] p. 31Exercise 4wess 5529
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6166  tz6.26i 6167  wefrc 5536  wereu2 5539
[TakeutiZaring] p. 32Theorem 6.27wfi 6168  wfii 6169
[TakeutiZaring] p. 32Definition 6.28df-isom 6352
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7071
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7072
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7078
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7079
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7080
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7084
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7091
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7093
[TakeutiZaring] p. 35Notationwtr 5158
[TakeutiZaring] p. 35Theorem 7.2trelpss 41016  tz7.2 5526
[TakeutiZaring] p. 35Definition 7.1dftr3 5162
[TakeutiZaring] p. 36Proposition 7.4ordwe 6191
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6199
[TakeutiZaring] p. 36Proposition 7.6ordelord 6200  ordelordALT 41100  ordelordALTVD 41430
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6206  ordelssne 6205
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6204
[TakeutiZaring] p. 37Proposition 7.9ordin 6208
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7493
[TakeutiZaring] p. 38Corollary 7.15ordsson 7494
[TakeutiZaring] p. 38Definition 7.11df-on 6182
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6210
[TakeutiZaring] p. 38Proposition 7.12onfrALT 41112  ordon 7488
[TakeutiZaring] p. 38Proposition 7.13onprc 7489
[TakeutiZaring] p. 39Theorem 7.17tfi 7558
[TakeutiZaring] p. 40Exercise 3ontr2 6225
[TakeutiZaring] p. 40Exercise 7dftr2 5160
[TakeutiZaring] p. 40Exercise 9onssmin 7502
[TakeutiZaring] p. 40Exercise 11unon 7536
[TakeutiZaring] p. 40Exercise 12ordun 6279
[TakeutiZaring] p. 40Exercise 14ordequn 6278
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7490
[TakeutiZaring] p. 40Proposition 7.20elssuni 4854
[TakeutiZaring] p. 41Definition 7.22df-suc 6184
[TakeutiZaring] p. 41Proposition 7.23sssucid 6255  sucidg 6256
[TakeutiZaring] p. 41Proposition 7.24suceloni 7518
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6269  ordnbtwn 6268
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7533
[TakeutiZaring] p. 42Exercise 1df-lim 6183
[TakeutiZaring] p. 42Exercise 4omssnlim 7584
[TakeutiZaring] p. 42Exercise 7ssnlim 7589
[TakeutiZaring] p. 42Exercise 8onsucssi 7546  ordelsuc 7525
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7527
[TakeutiZaring] p. 42Definition 7.27nlimon 7556
[TakeutiZaring] p. 42Definition 7.28dfom2 7572
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7591
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7592
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7593
[TakeutiZaring] p. 43Remarkomon 7581
[TakeutiZaring] p. 43Axiom 7inf3 9089  omex 9097
[TakeutiZaring] p. 43Theorem 7.32ordom 7579
[TakeutiZaring] p. 43Corollary 7.31find 7597
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7594
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7595
[TakeutiZaring] p. 44Exercise 1limomss 7575
[TakeutiZaring] p. 44Exercise 2int0 4876
[TakeutiZaring] p. 44Exercise 3trintss 5175
[TakeutiZaring] p. 44Exercise 4intss1 4877
[TakeutiZaring] p. 44Exercise 5intex 5226
[TakeutiZaring] p. 44Exercise 6oninton 7505
[TakeutiZaring] p. 44Exercise 11ordintdif 6227
[TakeutiZaring] p. 44Definition 7.35df-int 4863
[TakeutiZaring] p. 44Proposition 7.34noinfep 9114
[TakeutiZaring] p. 45Exercise 4onint 7500
[TakeutiZaring] p. 47Lemma 1tfrlem1 8002
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8023
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8024
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8025
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8032  tz7.44-2 8033  tz7.44-3 8034
[TakeutiZaring] p. 50Exercise 1smogt 7994
[TakeutiZaring] p. 50Exercise 3smoiso 7989
[TakeutiZaring] p. 50Definition 7.46df-smo 7973
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8071  tz7.49c 8072
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8069
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8068
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8070
[TakeutiZaring] p. 53Proposition 7.532eu5 2743
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9429
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9430
[TakeutiZaring] p. 56Definition 8.1oalim 8147  oasuc 8139
[TakeutiZaring] p. 57Remarktfindsg 7565
[TakeutiZaring] p. 57Proposition 8.2oacl 8150
[TakeutiZaring] p. 57Proposition 8.3oa0 8131  oa0r 8153
[TakeutiZaring] p. 57Proposition 8.16omcl 8151
[TakeutiZaring] p. 58Corollary 8.5oacan 8164
[TakeutiZaring] p. 58Proposition 8.4nnaord 8235  nnaordi 8234  oaord 8163  oaordi 8162
[TakeutiZaring] p. 59Proposition 8.6iunss2 4959  uniss2 4857
[TakeutiZaring] p. 59Proposition 8.7oawordri 8166
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8171  oawordex 8173
[TakeutiZaring] p. 59Proposition 8.9nnacl 8227
[TakeutiZaring] p. 59Proposition 8.10oaabs 8261
[TakeutiZaring] p. 60Remarkoancom 9105
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8176
[TakeutiZaring] p. 62Exercise 1nnarcl 8232
[TakeutiZaring] p. 62Exercise 5oaword1 8168
[TakeutiZaring] p. 62Definition 8.15om0x 8134  omlim 8148  omsuc 8141
[TakeutiZaring] p. 62Definition 8.15(a)om0 8132
[TakeutiZaring] p. 63Proposition 8.17nnecl 8229  nnmcl 8228
[TakeutiZaring] p. 63Proposition 8.19nnmord 8248  nnmordi 8247  omord 8184  omordi 8182
[TakeutiZaring] p. 63Proposition 8.20omcan 8185
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8252  omwordri 8188
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8154
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8158  om1r 8159
[TakeutiZaring] p. 64Proposition 8.22om00 8191
[TakeutiZaring] p. 64Proposition 8.23omordlim 8193
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8194
[TakeutiZaring] p. 64Proposition 8.25odi 8195
[TakeutiZaring] p. 65Theorem 8.26omass 8196
[TakeutiZaring] p. 67Definition 8.30nnesuc 8224  oe0 8137  oelim 8149  oesuc 8142  onesuc 8145
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8135
[TakeutiZaring] p. 67Proposition 8.32oen0 8202
[TakeutiZaring] p. 67Proposition 8.33oeordi 8203
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8136
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8161
[TakeutiZaring] p. 68Corollary 8.34oeord 8204
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8210
[TakeutiZaring] p. 68Proposition 8.35oewordri 8208
[TakeutiZaring] p. 68Proposition 8.37oeworde 8209
[TakeutiZaring] p. 69Proposition 8.41oeoa 8213
[TakeutiZaring] p. 70Proposition 8.42oeoe 8215
[TakeutiZaring] p. 73Theorem 9.1trcl 9161  tz9.1 9162
[TakeutiZaring] p. 76Definition 9.9df-r1 9184  r10 9188  r1lim 9192  r1limg 9191  r1suc 9190  r1sucg 9189
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9200  r1ord2 9201  r1ordg 9198
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9210
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9235  tz9.13 9211  tz9.13g 9212
[TakeutiZaring] p. 79Definition 9.14df-rank 9185  rankval 9236  rankvalb 9217  rankvalg 9237
[TakeutiZaring] p. 79Proposition 9.16rankel 9259  rankelb 9244
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9273  rankval3 9260  rankval3b 9246
[TakeutiZaring] p. 79Proposition 9.18rankonid 9249
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9215
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9254  rankr1c 9241  rankr1g 9252
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9255
[TakeutiZaring] p. 80Exercise 1rankss 9269  rankssb 9268
[TakeutiZaring] p. 80Exercise 2unbndrank 9262
[TakeutiZaring] p. 80Proposition 9.19bndrank 9261
[TakeutiZaring] p. 83Axiom of Choiceac4 9889  dfac3 9539
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9448  numth 9886  numth2 9885
[TakeutiZaring] p. 85Definition 10.4cardval 9960
[TakeutiZaring] p. 85Proposition 10.5cardid 9961  cardid2 9373
[TakeutiZaring] p. 85Proposition 10.9oncard 9380
[TakeutiZaring] p. 85Proposition 10.10carden 9965
[TakeutiZaring] p. 85Proposition 10.11cardidm 9379
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9364
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9385
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9377
[TakeutiZaring] p. 87Proposition 10.15pwen 8681
[TakeutiZaring] p. 88Exercise 1en0 8562
[TakeutiZaring] p. 88Exercise 7infensuc 8686
[TakeutiZaring] p. 89Exercise 10omxpen 8609
[TakeutiZaring] p. 90Corollary 10.23cardnn 9383
[TakeutiZaring] p. 90Definition 10.27alephiso 9516
[TakeutiZaring] p. 90Proposition 10.20nneneq 8691
[TakeutiZaring] p. 90Proposition 10.22onomeneq 8700
[TakeutiZaring] p. 90Proposition 10.26alephprc 9517
[TakeutiZaring] p. 90Corollary 10.21(1)php5 8696
[TakeutiZaring] p. 91Exercise 2alephle 9506
[TakeutiZaring] p. 91Exercise 3aleph0 9484
[TakeutiZaring] p. 91Exercise 4cardlim 9392
[TakeutiZaring] p. 91Exercise 7infpss 9631
[TakeutiZaring] p. 91Exercise 8infcntss 8783
[TakeutiZaring] p. 91Definition 10.29df-fin 8503  isfi 8523
[TakeutiZaring] p. 92Proposition 10.32onfin 8701
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8602
[TakeutiZaring] p. 93Proposition 10.35fodomb 9940
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 9603  unxpdom 8716
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9394  cardsdomelir 9393
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 8718
[TakeutiZaring] p. 94Proposition 10.39infxpen 9432
[TakeutiZaring] p. 95Definition 10.42df-map 8398
[TakeutiZaring] p. 95Proposition 10.40infxpidm 9976  infxpidm2 9435
[TakeutiZaring] p. 95Proposition 10.41infdju 9622  infxp 9629
[TakeutiZaring] p. 96Proposition 10.44pw2en 8614  pw2f1o 8612
[TakeutiZaring] p. 96Proposition 10.45mapxpen 8674
[TakeutiZaring] p. 97Theorem 10.46ac6s3 9901
[TakeutiZaring] p. 98Theorem 10.46ac6c5 9896  ac6s5 9905
[TakeutiZaring] p. 98Theorem 10.47unidom 9957
[TakeutiZaring] p. 100Definition 11.1cfcof 9688
[TakeutiZaring] p. 101Proposition 11.7cofsmo 9683
[TakeutiZaring] p. 102Exercise 1cfle 9668
[TakeutiZaring] p. 102Exercise 2cf0 9665
[TakeutiZaring] p. 102Exercise 3cfsuc 9671
[TakeutiZaring] p. 102Exercise 4cfom 9678
[TakeutiZaring] p. 102Proposition 11.9coftr 9687
[TakeutiZaring] p. 103Theorem 11.15alephreg 9996
[TakeutiZaring] p. 103Proposition 11.11cardcf 9666
[TakeutiZaring] p. 103Proposition 11.13alephsing 9690
[TakeutiZaring] p. 104Corollary 11.17cardinfima 9515
[TakeutiZaring] p. 104Proposition 11.16carduniima 9514
[TakeutiZaring] p. 104Proposition 11.18alephfp 9526  alephfp2 9527
[TakeutiZaring] p. 106Theorem 11.20gchina 10113
[TakeutiZaring] p. 106Theorem 11.21mappwen 9530
[TakeutiZaring] p. 107Theorem 11.26konigth 9983
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 9997
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 9998
[Tarski] p. 67Axiom B5ax-c5 36089
[Tarski] p. 67Scheme B5sp 2184
[Tarski] p. 68Lemma 6avril1 28244  equid 2020
[Tarski] p. 69Lemma 7equcomi 2025
[Tarski] p. 70Lemma 14spim 2407  spime 2409  spimew 1975
[Tarski] p. 70Lemma 16ax-12 2179  ax-c15 36095  ax12i 1970
[Tarski] p. 70Lemmas 16 and 17sb6 2094
[Tarski] p. 75Axiom B7ax6v 1972
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1912  ax5ALT 36113
[Tarski], p. 75Scheme B8 of system S2ax-7 2016  ax-8 2117  ax-9 2125
[Tarski1999] p. 178Axiom 4axtgsegcon 26254
[Tarski1999] p. 178Axiom 5axtg5seg 26255
[Tarski1999] p. 179Axiom 7axtgpasch 26257
[Tarski1999] p. 180Axiom 7.1axtgpasch 26257
[Tarski1999] p. 185Axiom 11axtgcont1 26258
[Truss] p. 114Theorem 5.18ruc 15592
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 35006
[Viaclovsky8] p. 3Proposition 7ismblfin 35008
[Weierstrass] p. 272Definitiondf-mdet 21187  mdetuni 21224
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 917
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 965
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 34774
[WhiteheadRussell] p. 100Theorem *2.05frege5 40355  imim2 58  wl-luk-imim2 34769
[WhiteheadRussell] p. 101Theorem *2.06barbara 2751  syl 17
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 34772
[WhiteheadRussell] p. 102Theorem *2.14notnotr 132  notnotrALT2 41490  wl-luk-notnotr 34773
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 40385  axfrege28 40384  con3 156
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 34766
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 28182  pm2.27 42  wl-luk-pm2.27 34764
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 172  pm2.5g 171
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 889  pm2.67 890
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 179  pm2.521g 177  pm2.521g2 178
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 473  pm3.2im 163
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 452
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 453
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 486  simplim 170
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 488  simprim 169
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 764
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 765
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 807
[WhiteheadRussell] p. 113Theorem *3.44jao 958  pm3.44 957
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 477
[WhiteheadRussell] p. 117Theorem *4.22biantr 805  bitr 804
[WhiteheadRussell] p. 117Theorem *4.25oridm 902  pm4.25 903
[WhiteheadRussell] p. 119Theorem *4.45orabs 996  pm4.45 995  pm4.45im 826
[WhiteheadRussell] p. 120Theorem *4.56ioran 981  pm4.56 986
[WhiteheadRussell] p. 120Theorem *4.57oran 987  pm4.57 988
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 561  pm4.71d 565  pm4.71i 563  pm4.71r 562  pm4.71rd 566  pm4.71ri 564
[WhiteheadRussell] p. 121Theorem *4.76jcab 521  pm4.76 522
[WhiteheadRussell] p. 121Theorem *4.77jaob 959  pm4.77 960
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 392  impexp 454  pm4.87 840
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 942  pm5.11g 941
[WhiteheadRussell] p. 124Theorem *5.18nbbn 388  pm5.18 386
[WhiteheadRussell] p. 125Theorem *5.41imdi 394  pm5.41 395
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 40968  pm13.13b 40969
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 41115  pm13.193 40972
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 40983  pm14.122b 40984  pm14.122c 40985
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 40986  pm14.123b 40987  pm14.123c 40988