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 16410  invisoinvl 16431
[Adamek] p. 28Example 3.13idinv 16430  idiso 16429
[Adamek] p. 28Definition 3.8df-inv 16389  df-iso 16390  dfiso2 16413
[Adamek] p. 29Definition 3.15cic 16440  df-cic 16437
[Adamek] p. 29Proposition 3.14(2)invco 16412  isoco 16418
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 16788
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 16788
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 16773
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 16773
[Adamek] p. 101Example 7.2 (6)irinitoringc 41834
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 16643
[Adamek] p. 102Proposition 7.3 (2)initoeu2 16647
[Adamek] p. 103Example 7.9 (3)nzerooringczr 41837
[AhoHopUll] p. 2Section 1.1df-bigo 42107
[AhoHopUll] p. 12Section 1.3df-blen 42129
[AhoHopUll] p. 318Section 9.1df-concat 13284  df-pfx 41147  df-substr 13286  df-word 13282  lencl 13307  wrd0 13313
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 22493  df-nmoo 27570
[AkhiezerGlazman] p. 64Theoremhmopidmch 28982  hmopidmchi 28980
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 29030  pjcmul2i 29031
[AkhiezerGlazman] p. 72Theoremcnvunop 28747  unoplin 28749
[AkhiezerGlazman] p. 73Theoremelunop2 28842  lnopunii 28841
[Apostol] p. 18Theorem I.2negeu 10256
[Apostol] p. 18Theorem I.3negsub 10314  negsubd 10383  negsubi 10344
[Apostol] p. 18Theorem I.4negneg 10316  negnegd 10368  negnegi 10336
[Apostol] p. 18Theorem I.5subdi 10448  subdid 10471  subdii 10464  subdir 10449  subdird 10472  subdiri 10465
[Apostol] p. 18Theorem I.6mul01 10200  mul01d 10220  mul01i 10211  mul02 10199  mul02d 10219  mul02i 10210
[Apostol] p. 18Theorem I.7mulcan 10649  mulcan2d 10646  mulcand 10645  mulcani 10651
[Apostol] p. 18Theorem I.8receu 10657  xreceu 29604
[Apostol] p. 18Theorem I.9divrec 10686  divrecd 10789  divreci 10755  divreczi 10748
[Apostol] p. 18Theorem I.10recrec 10707  recreci 10742
[Apostol] p. 18Theorem I.11mul0or 10652  mul0ord 10662  mul0ori 10660
[Apostol] p. 18Theorem I.12mul2neg 10454  mul2negd 10470  mul2negi 10463  mulneg1 10451  mulneg1d 10468  mulneg1i 10461
[Apostol] p. 18Theorem I.14divmuldiv 10710  divmuldivd 10827  divmuldivi 10770  rdivmuldivd 29765
[Apostol] p. 18Theorem I.15divdivdiv 10711  divdivdivd 10833  divdivdivi 10773
[Apostol] p. 20Axiom 8rpneg 11848
[Apostol] p. 20Axiom 90nrp 11850
[Apostol] p. 20Theorem I.17lttri 10148
[Apostol] p. 20Theorem I.19ltmul1 10858  ltmul1a 10857  ltmul1i 10927  ltmul1ii 10937  ltmul2 10859  ltmul2d 11899  ltmul2dd 11913  ltmul2i 10930
[Apostol] p. 20Theorem I.20msqgt0 10533  msqgt0d 10580  msqgt0i 10550
[Apostol] p. 20Theorem I.210lt1 10535
[Apostol] p. 20Theorem I.23lt0neg1 10519  lt0neg1d 10582  ltneg 10513  ltnegd 10590  ltnegi 10557
[Apostol] p. 20Definition of positive numbersdf-rp 11818
[Apostol] p. 21Exercise 4recgt0 10852  recgt0d 10943  recgt0i 10913  recgt0ii 10914
[Apostol] p. 22Definition of integersdf-z 11363
[Apostol] p. 22Definition of positive integersdfnn3 11019
[Apostol] p. 22Definition of rationalsdf-q 11774
[Apostol] p. 24Theorem I.26supeu 8345
[Apostol] p. 26Theorem I.28nnunb 11273
[Apostol] p. 26Theorem I.29arch 11274
[Apostol] p. 28Exercise 2btwnz 11464
[Apostol] p. 28Exercise 3nnrecl 11275
[Apostol] p. 28Exercise 4rebtwnz 11772
[Apostol] p. 28Exercise 5zbtwnre 11771
[Apostol] p. 28Exercise 6qbtwnre 12015
[Apostol] p. 28Exercise 10(a)zeneo 15044  zneo 11445  zneoALTV 41345
[Apostol] p. 29Theorem I.35msqsqrtd 14160  resqrtth 13977  sqrtth 14085  sqrtthi 14091  sqsqrtd 14159
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 11008
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 11738
[Apostol] p. 361Remarkcrreczi 12972
[Apostol] p. 363Remarkabsgt0i 14119
[Apostol] p. 363Exampleabssubd 14173  abssubi 14123
[ApostolNT] p. 7Remarkfmtno0 41217  fmtno1 41218  fmtno2 41227  fmtno3 41228  fmtno4 41229  fmtno5fac 41259  fmtnofz04prm 41254
[ApostolNT] p. 7Definitiondf-fmtno 41205
[ApostolNT] p. 8Definitiondf-ppi 24807
[ApostolNT] p. 14Definitiondf-dvds 14965
[ApostolNT] p. 14Theorem 1.1(a)iddvds 14976
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 14999
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 14995
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 14989
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 14991
[ApostolNT] p. 14Theorem 1.1(f)1dvds 14977
[ApostolNT] p. 14Theorem 1.1(g)dvds0 14978
[ApostolNT] p. 14Theorem 1.1(h)0dvds 14983
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 15014
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 15016
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 15018
[ApostolNT] p. 15Definitiondf-gcd 15198  dfgcd2 15244
[ApostolNT] p. 16Definitionisprm2 15376
[ApostolNT] p. 16Theorem 1.5coprmdvds 15347
[ApostolNT] p. 16Theorem 1.7prminf 15600
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 15216
[ApostolNT] p. 16Theorem 1.4(b)gcdass 15245
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 15247
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 15230
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 15222
[ApostolNT] p. 17Theorem 1.8coprm 15404
[ApostolNT] p. 17Theorem 1.9euclemma 15406
[ApostolNT] p. 17Theorem 1.101arith2 15613
[ApostolNT] p. 18Theorem 1.13prmrec 15607
[ApostolNT] p. 19Theorem 1.14divalg 15107
[ApostolNT] p. 20Theorem 1.15eucalg 15281
[ApostolNT] p. 24Definitiondf-mu 24808
[ApostolNT] p. 25Definitiondf-phi 15452
[ApostolNT] p. 25Theorem 2.1musum 24898
[ApostolNT] p. 26Theorem 2.2phisum 15476
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 15462
[ApostolNT] p. 28Theorem 2.5(c)phimul 15466
[ApostolNT] p. 32Definitiondf-vma 24805
[ApostolNT] p. 32Theorem 2.9muinv 24900
[ApostolNT] p. 32Theorem 2.10vmasum 24922
[ApostolNT] p. 38Remarkdf-sgm 24809
[ApostolNT] p. 38Definitiondf-sgm 24809
[ApostolNT] p. 75Definitiondf-chp 24806  df-cht 24804
[ApostolNT] p. 104Definitioncongr 15359
[ApostolNT] p. 106Remarkdvdsval3 14968
[ApostolNT] p. 106Definitionmoddvds 14972
[ApostolNT] p. 107Example 2mod2eq0even 15051
[ApostolNT] p. 107Example 3mod2eq1n2dvds 15052
[ApostolNT] p. 107Example 4zmod1congr 12670
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 12707
[ApostolNT] p. 107Theorem 5.2(c)modexp 12982
[ApostolNT] p. 108Theorem 5.3modmulconst 14994
[ApostolNT] p. 109Theorem 5.4cncongr1 15362
[ApostolNT] p. 109Theorem 5.6gcdmodi 15759
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 15364
[ApostolNT] p. 113Theorem 5.17eulerth 15469
[ApostolNT] p. 113Theorem 5.18vfermltl 15487
[ApostolNT] p. 114Theorem 5.19fermltl 15470
[ApostolNT] p. 116Theorem 5.24wilthimp 24779
[ApostolNT] p. 179Definitiondf-lgs 25001  lgsprme0 25045
[ApostolNT] p. 180Example 11lgs 25046
[ApostolNT] p. 180Theorem 9.2lgsvalmod 25022
[ApostolNT] p. 180Theorem 9.3lgsdirprm 25037
[ApostolNT] p. 181Theorem 9.4m1lgs 25094
[ApostolNT] p. 181Theorem 9.52lgs 25113  2lgsoddprm 25122
[ApostolNT] p. 182Theorem 9.6gausslemma2d 25080
[ApostolNT] p. 188Definitiondf-lgs 25001  lgs1 25047
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 25038
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 25040
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 25048
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 25049
[Baer] p. 40Property (b)mapdord 36746
[Baer] p. 40Property (c)mapd11 36747
[Baer] p. 40Property (e)mapdin 36770  mapdlsm 36772
[Baer] p. 40Property (f)mapd0 36773
[Baer] p. 40Definition of projectivitydf-mapd 36733  mapd1o 36756
[Baer] p. 41Property (g)mapdat 36775
[Baer] p. 44Part (1)mapdpg 36814
[Baer] p. 45Part (2)hdmap1eq 36910  mapdheq 36836  mapdheq2 36837  mapdheq2biN 36838
[Baer] p. 45Part (3)baerlem3 36821
[Baer] p. 46Part (4)mapdheq4 36840  mapdheq4lem 36839
[Baer] p. 46Part (5)baerlem5a 36822  baerlem5abmN 36826  baerlem5amN 36824  baerlem5b 36823  baerlem5bmN 36825
[Baer] p. 47Part (6)hdmap1l6 36930  hdmap1l6a 36918  hdmap1l6e 36923  hdmap1l6f 36924  hdmap1l6g 36925  hdmap1l6lem1 36916  hdmap1l6lem2 36917  hdmap1p6N 36931  mapdh6N 36855  mapdh6aN 36843  mapdh6eN 36848  mapdh6fN 36849  mapdh6gN 36850  mapdh6lem1N 36841  mapdh6lem2N 36842
[Baer] p. 48Part 9hdmapval 36939
[Baer] p. 48Part 10hdmap10 36951
[Baer] p. 48Part (6)hdmap1l6h 36926  mapdh6hN 36851
[Baer] p. 48Part (7)mapdh75cN 36861  mapdh75d 36862  mapdh75e 36860  mapdh75fN 36863  mapdh7cN 36857  mapdh7dN 36858  mapdh7eN 36856  mapdh7fN 36859
[Baer] p. 48Part (8)mapdh8 36897  mapdh8a 36883  mapdh8aa 36884  mapdh8ab 36885  mapdh8ac 36886  mapdh8ad 36887  mapdh8b 36888  mapdh8c 36889  mapdh8d 36891  mapdh8d0N 36890  mapdh8e 36892  mapdh8fN 36893  mapdh8g 36894  mapdh8i 36895  mapdh8j 36896
[Baer] p. 48Part (9)mapdh9a 36898
[Baer] p. 48Equation 10mapdhvmap 36877
[Baer] p. 49Part 12hdmap11 36959  hdmapeq0 36955  hdmapf1oN 36976  hdmapneg 36957  hdmaprnN 36975  hdmaprnlem1N 36960  hdmaprnlem3N 36961  hdmaprnlem3uN 36962  hdmaprnlem4N 36964  hdmaprnlem6N 36965  hdmaprnlem7N 36966  hdmaprnlem8N 36967  hdmaprnlem9N 36968  hdmapsub 36958
[Baer] p. 49Part 14hdmap14lem1 36979  hdmap14lem10 36988  hdmap14lem1a 36977  hdmap14lem2N 36980  hdmap14lem2a 36978  hdmap14lem3 36981  hdmap14lem8 36986  hdmap14lem9 36987
[Baer] p. 50Part 14hdmap14lem11 36989  hdmap14lem12 36990  hdmap14lem13 36991  hdmap14lem14 36992  hdmap14lem15 36993  hgmapval 36998
[Baer] p. 50Part 15hgmapadd 37005  hgmapmul 37006  hgmaprnlem2N 37008  hgmapvs 37002
[Baer] p. 50Part 16hgmaprnN 37012
[Baer] p. 110Lemma 1hdmapip0com 37028
[Baer] p. 110Line 27hdmapinvlem1 37029
[Baer] p. 110Line 28hdmapinvlem2 37030
[Baer] p. 110Line 30hdmapinvlem3 37031
[Baer] p. 110Part 1.2hdmapglem5 37033  hgmapvv 37037
[Baer] p. 110Proposition 1hdmapinvlem4 37032
[Baer] p. 111Line 10hgmapvvlem1 37034
[Baer] p. 111Line 15hdmapg 37041  hdmapglem7 37040
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2472
[BellMachover] p. 460Notationdf-mo 2473
[BellMachover] p. 460Definitionmo3 2505
[BellMachover] p. 461Axiom Extax-ext 2600
[BellMachover] p. 462Theorem 1.1bm1.1 2605
[BellMachover] p. 463Axiom Repaxrep5 4767
[BellMachover] p. 463Scheme Sepaxsep 4771
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4775
[BellMachover] p. 466Problemaxpow2 4836
[BellMachover] p. 466Axiom Powaxpow3 4837
[BellMachover] p. 466Axiom Unionaxun2 6936
[BellMachover] p. 468Definitiondf-ord 5714
[BellMachover] p. 469Theorem 2.2(i)ordirr 5729
[BellMachover] p. 469Theorem 2.2(iii)onelon 5736
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 5731
[BellMachover] p. 471Definition of Ndf-om 7051
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 6991
[BellMachover] p. 471Definition of Limdf-lim 5716
[BellMachover] p. 472Axiom Infzfinf2 8524
[BellMachover] p. 473Theorem 2.8limom 7065
[BellMachover] p. 477Equation 3.1df-r1 8612
[BellMachover] p. 478Definitionrankval2 8666
[BellMachover] p. 478Theorem 3.3(i)r1ord3 8630  r1ord3g 8627
[BellMachover] p. 480Axiom Regzfreg 8485
[BellMachover] p. 488Axiom ACac5 9284  dfac4 8930
[BellMachover] p. 490Definition of alephalephval3 8918
[BeltramettiCassinelli] p. 98Remarkatlatmstc 34425
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 29182
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 29224  chirredi 29223
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 29212
[Beran] p. 3Definition of joinsshjval3 28183
[Beran] p. 39Theorem 2.3(i)cmcm2 28445  cmcm2i 28422  cmcm2ii 28427  cmt2N 34356
[Beran] p. 40Theorem 2.3(iii)lecm 28446  lecmi 28431  lecmii 28432
[Beran] p. 45Theorem 3.4cmcmlem 28420
[Beran] p. 49Theorem 4.2cm2j 28449  cm2ji 28454  cm2mi 28455
[Beran] p. 95Definitiondf-sh 28034  issh2 28036
[Beran] p. 95Lemma 3.1(S5)his5 27913
[Beran] p. 95Lemma 3.1(S6)his6 27926
[Beran] p. 95Lemma 3.1(S7)his7 27917
[Beran] p. 95Lemma 3.2(S8)ho01i 28657
[Beran] p. 95Lemma 3.2(S9)hoeq1 28659
[Beran] p. 95Lemma 3.2(S10)ho02i 28658
[Beran] p. 95Lemma 3.2(S11)hoeq2 28660
[Beran] p. 95Postulate (S1)ax-his1 27909  his1i 27927
[Beran] p. 95Postulate (S2)ax-his2 27910
[Beran] p. 95Postulate (S3)ax-his3 27911
[Beran] p. 95Postulate (S4)ax-his4 27912
[Beran] p. 96Definition of normdf-hnorm 27795  dfhnorm2 27949  normval 27951
[Beran] p. 96Definition for Cauchy sequencehcau 28011
[Beran] p. 96Definition of Cauchy sequencedf-hcau 27800
[Beran] p. 96Definition of complete subspaceisch3 28068
[Beran] p. 96Definition of convergedf-hlim 27799  hlimi 28015
[Beran] p. 97Theorem 3.3(i)norm-i-i 27960  norm-i 27956
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 27964  norm-ii 27965  normlem0 27936  normlem1 27937  normlem2 27938  normlem3 27939  normlem4 27940  normlem5 27941  normlem6 27942  normlem7 27943  normlem7tALT 27946
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 27966  norm-iii 27967
[Beran] p. 98Remark 3.4bcs 28008  bcsiALT 28006  bcsiHIL 28007
[Beran] p. 98Remark 3.4(B)normlem9at 27948  normpar 27982  normpari 27981
[Beran] p. 98Remark 3.4(C)normpyc 27973  normpyth 27972  normpythi 27969
[Beran] p. 99Remarklnfn0 28876  lnfn0i 28871  lnop0 28795  lnop0i 28799
[Beran] p. 99Theorem 3.5(i)nmcexi 28855  nmcfnex 28882  nmcfnexi 28880  nmcopex 28858  nmcopexi 28856
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 28883  nmcfnlbi 28881  nmcoplb 28859  nmcoplbi 28857
[Beran] p. 99Theorem 3.5(iii)lnfncon 28885  lnfnconi 28884  lnopcon 28864  lnopconi 28863
[Beran] p. 100Lemma 3.6normpar2i 27983
[Beran] p. 102Theorem 3.7(i)chocunii 28130  pjhth 28222  pjhtheu 28223  pjpjhth 28254  pjpjhthi 28255  pjth 23191
[Beran] p. 102Theorem 3.7(ii)ococ 28235  ococi 28234
[Beran] p. 103Remark 3.8nlelchi 28890
[Beran] p. 104Theorem 3.9riesz3i 28891  riesz4 28893  riesz4i 28892
[Beran] p. 107Definitiondf-ch 28048  isch2 28050
[Beran] p. 107Remark 3.12choccl 28135  isch3 28068  occl 28133  ocsh 28112  shoccl 28134  shocsh 28113
[Beran] p. 107Remark 3.12(B)ococin 28237
[Beran] p. 108Theorem 3.13chintcl 28161
[Beran] p. 109Property (ii)pjidmco 29010  pjidmcoi 29006  pjidmi 28502
[Beran] p. 110Definition of projector orderingpjordi 29002
[Beran] p. 111Remarkho0val 28579  pjch1 28499
[Beran] p. 111Definitiondf-hfmul 28563  df-hfsum 28562  df-hodif 28561  df-homul 28560  df-hosum 28559
[Beran] p. 111Lemma 4.4(i)pjo 28500
[Beran] p. 111Lemma 4.4(ii)pjch 28523  pjchi 28261
[Beran] p. 111Lemma 4.4(iii)pjoc2 28268  pjoc2i 28267
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 28509
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 28994  pjssmii 28510
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 28993
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 28992
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 28997
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 28995  pjssge0ii 28511
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 28996  pjdifnormii 28512
[Bobzien] p. 116Statement T3stoic3 1699
[Bobzien] p. 117Statement T2stoic2a 1697
[Bobzien] p. 117Statement T4stoic4a 1700
[Bobzien] p. 117Conclusion the contradictorystoic1a 1695
[Bogachev] p. 16Definition 1.5df-oms 30328
[Bogachev] p. 17Example 1.5.2omsmon 30334
[Bogachev] p. 41Definition 1.11.2df-carsg 30338
[Bogachev] p. 42Theorem 1.11.4carsgsiga 30358
[Bogachev] p. 116Definition 2.3.1df-itgm 30389  df-sitm 30367
[Bogachev] p. 118Chapter 2.4.4df-itgm 30389
[Bogachev] p. 118Definition 2.4.1df-sitg 30366
[Bollobas] p. 1Section I.1df-edg 25921  isuhgrop 25946  isusgrop 26038  isuspgrop 26037
[Bollobas] p. 2Section I.1df-subgr 26141  uhgrspan1 26176  uhgrspansubgr 26164
[Bollobas] p. 3Section I.1cusgrsize 26331  df-cusgr 26213  df-nbgr 26209  fusgrmaxsize 26341
[Bollobas] p. 4Definitiondf-upwlks 41480  df-wlks 26476
[Bollobas] p. 4Section I.1finsumvtxdg2size 26427  finsumvtxdgeven 26429  fusgr1th 26428  fusgrvtxdgonume 26431  vtxdgoddnumeven 26430
[Bollobas] p. 5Notationdf-pths 26593
[Bollobas] p. 5Definitiondf-crcts 26662  df-cycls 26663  df-trls 26570  df-wlkson 26477
[Bollobas] p. 7Section I.1df-ushgr 25935
[BourbakiAlg1] p. 1Definition 1df-clintop 41601  df-cllaw 41587  df-mgm 17223  df-mgm2 41620
[BourbakiAlg1] p. 4Definition 5df-assintop 41602  df-asslaw 41589  df-sgrp 17265  df-sgrp2 41622
[BourbakiAlg1] p. 7Definition 8df-cmgm2 41621  df-comlaw 41588
[BourbakiAlg1] p. 12Definition 2df-mnd 17276
[BourbakiAlg1] p. 92Definition 1df-ring 18530
[BourbakiAlg1] p. 93Section I.8.1df-rng0 41640
[BourbakiEns] p. Proposition 8fcof1 6527  fcofo 6528
[BourbakiTop1] p. Remarkxnegmnf 12026  xnegpnf 12025
[BourbakiTop1] p. Remark rexneg 12027
[BourbakiTop1] p. Theoremneiss 20894
[BourbakiTop1] p. Remark 3ust0 22004  ustfilxp 21997
[BourbakiTop1] p. Axiom GT'tgpsubcn 21875
[BourbakiTop1] p. Example 1cstucnd 22069  iducn 22068  snfil 21649
[BourbakiTop1] p. Example 2neifil 21665
[BourbakiTop1] p. Theorem 1cnextcn 21852
[BourbakiTop1] p. Theorem 2ucnextcn 22089
[BourbakiTop1] p. Theorem 3df-hcmp 29977
[BourbakiTop1] p. Definitionistgp 21862
[BourbakiTop1] p. Paragraph 3infil 21648
[BourbakiTop1] p. Propositioncnpco 21052  ishmeo 21543  neips 20898
[BourbakiTop1] p. Definition 1df-ucn 22061  df-ust 21985  filintn0 21646  ucnprima 22067
[BourbakiTop1] p. Definition 2df-cfilu 22072
[BourbakiTop1] p. Definition 3df-cusp 22083  df-usp 22042  df-utop 22016  trust 22014
[BourbakiTop1] p. Definition 6df-pcmp 29897
[BourbakiTop1] p. Condition F_Iustssel 21990
[BourbakiTop1] p. Condition U_Iustdiag 21993
[BourbakiTop1] p. Property V_ivneiptopreu 20918
[BourbakiTop1] p. Proposition 1ucncn 22070  ustund 22006  ustuqtop 22031
[BourbakiTop1] p. Proposition 2neiptopreu 20918  utop2nei 22035  utop3cls 22036
[BourbakiTop1] p. Proposition 3fmucnd 22077  uspreg 22059  utopreg 22037
[BourbakiTop1] p. Proposition 4imasncld 21475  imasncls 21476  imasnopn 21474
[BourbakiTop1] p. Proposition 9cnpflf2 21785
[BourbakiTop1] p. Theorem 1 (d)iscncl 21054
[BourbakiTop1] p. Condition F_IIustincl 21992
[BourbakiTop1] p. Condition U_IIustinvel 21994
[BourbakiTop1] p. Proposition 11cnextucn 22088
[BourbakiTop1] p. Proposition Vissnei2 20901
[BourbakiTop1] p. Condition F_IIbustbasel 21991
[BourbakiTop1] p. Condition U_IIIustexhalf 21995
[BourbakiTop1] p. Definition C'''df-cmp 21171
[BourbakiTop1] p. Proposition Viiinnei 20910
[BourbakiTop1] p. Proposition Vivneissex 20912
[BourbakiTop1] p. Proposition Viiielnei 20896  ssnei 20895
[BourbakiTop1] p. Remark below def. 1filn0 21647
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 21631
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 20680
[BourbakiTop2] p. 195Definition 1df-ldlf 29894
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 40042
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 40044  stoweid 40043
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 39981  stoweidlem10 39990  stoweidlem14 39994  stoweidlem15 39995  stoweidlem35 40015  stoweidlem36 40016  stoweidlem37 40017  stoweidlem38 40018  stoweidlem40 40020  stoweidlem41 40021  stoweidlem43 40023  stoweidlem44 40024  stoweidlem46 40026  stoweidlem5 39985  stoweidlem50 40030  stoweidlem52 40032  stoweidlem53 40033  stoweidlem55 40035  stoweidlem56 40036
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 40003  stoweidlem24 40004  stoweidlem27 40007  stoweidlem28 40008  stoweidlem30 40010
[BrosowskiDeutsh] p. 91Proofstoweidlem34 40014  stoweidlem59 40039  stoweidlem60 40040
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 40025  stoweidlem49 40029  stoweidlem7 39987
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 40011  stoweidlem39 40019  stoweidlem42 40022  stoweidlem48 40028  stoweidlem51 40031  stoweidlem54 40034  stoweidlem57 40037  stoweidlem58 40038
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 40005
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 39997
[BrosowskiDeutsh] p. 92Proofstoweidlem11 39991  stoweidlem13 39993  stoweidlem26 40006  stoweidlem61 40041
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 39998
[Bruck] p. 1Section I.1df-clintop 41601  df-mgm 17223  df-mgm2 41620
[Bruck] p. 23Section II.1df-sgrp 17265  df-sgrp2 41622
[Bruck] p. 28Theorem 3.2dfgrp3 17495
[ChoquetDD] p. 2Definition of mappingdf-mpt 4721
[Church] p. 129Section II.24df-ifp 1012  dfifp2 1013
[Clemente] p. 10Definition ITnatded 27230
[Clemente] p. 10Definition I` `m,nnatded 27230
[Clemente] p. 11Definition E=>m,nnatded 27230
[Clemente] p. 11Definition I=>m,nnatded 27230
[Clemente] p. 11Definition E` `(1)natded 27230
[Clemente] p. 11Definition E` `(2)natded 27230
[Clemente] p. 12Definition E` `m,n,pnatded 27230
[Clemente] p. 12Definition I` `n(1)natded 27230
[Clemente] p. 12Definition I` `n(2)natded 27230
[Clemente] p. 13Definition I` `m,n,pnatded 27230
[Clemente] p. 14Proof 5.11natded 27230
[Clemente] p. 14Definition E` `nnatded 27230
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 27232  ex-natded5.2 27231
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 27235  ex-natded5.3 27234
[Clemente] p. 18Theorem 5.5ex-natded5.5 27237
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 27239  ex-natded5.7 27238
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 27241  ex-natded5.8 27240
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 27243  ex-natded5.13 27242
[Clemente] p. 32Definition I` `nnatded 27230
[Clemente] p. 32Definition E` `m,n,p,anatded 27230
[Clemente] p. 32Definition E` `n,tnatded 27230
[Clemente] p. 32Definition I` `n,tnatded 27230
[Clemente] p. 43Theorem 9.20ex-natded9.20 27244
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 27245
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 27247  ex-natded9.26 27246
[Cohen] p. 301Remarkrelogoprlem 24318
[Cohen] p. 301Property 2relogmul 24319  relogmuld 24352
[Cohen] p. 301Property 3relogdiv 24320  relogdivd 24353
[Cohen] p. 301Property 4relogexp 24323
[Cohen] p. 301Property 1alog1 24313
[Cohen] p. 301Property 1bloge 24314
[Cohen4] p. 348Observationrelogbcxpb 24506
[Cohen4] p. 349Propertyrelogbf 24510
[Cohen4] p. 352Definitionelogb 24489
[Cohen4] p. 361Property 2relogbmul 24496
[Cohen4] p. 361Property 3logbrec 24501  relogbdiv 24498
[Cohen4] p. 361Property 4relogbreexp 24494
[Cohen4] p. 361Property 6relogbexp 24499
[Cohen4] p. 361Property 1(a)logbid1 24487
[Cohen4] p. 361Property 1(b)logb1 24488
[Cohen4] p. 367Propertylogbchbase 24490
[Cohen4] p. 377Property 2logblt 24503
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 30321  sxbrsigalem4 30323
[Cohn] p. 81Section II.5acsdomd 17162  acsinfd 17161  acsinfdimd 17163  acsmap2d 17160  acsmapd 17159
[Cohn] p. 143Example 5.1.1sxbrsiga 30326
[Connell] p. 57Definitiondf-scmat 20278  df-scmatalt 41953
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 12643
[Crawley] p. 1Definition of posetdf-poset 16927
[Crawley] p. 107Theorem 13.2hlsupr 34491
[Crawley] p. 110Theorem 13.3arglem1N 35296  dalaw 34991
[Crawley] p. 111Theorem 13.4hlathil 37072
[Crawley] p. 111Definition of set Wdf-watsN 35095
[Crawley] p. 111Definition of dilationdf-dilN 35211  df-ldil 35209  isldil 35215
[Crawley] p. 111Definition of translationdf-ltrn 35210  df-trnN 35212  isltrn 35224  ltrnu 35226
[Crawley] p. 112Lemma Acdlema1N 34896  cdlema2N 34897  exatleN 34509
[Crawley] p. 112Lemma B1cvrat 34581  cdlemb 34899  cdlemb2 35146  cdlemb3 35713  idltrn 35255  l1cvat 34161  lhpat 35148  lhpat2 35150  lshpat 34162  ltrnel 35244  ltrnmw 35256
[Crawley] p. 112Lemma Ccdlemc1 35297  cdlemc2 35298  ltrnnidn 35280  trlat 35275  trljat1 35272  trljat2 35273  trljat3 35274  trlne 35291  trlnidat 35279  trlnle 35292
[Crawley] p. 112Definition of automorphismdf-pautN 35096
[Crawley] p. 113Lemma Ccdlemc 35303  cdlemc3 35299  cdlemc4 35300
[Crawley] p. 113Lemma Dcdlemd 35313  cdlemd1 35304  cdlemd2 35305  cdlemd3 35306  cdlemd4 35307  cdlemd5 35308  cdlemd6 35309  cdlemd7 35310  cdlemd8 35311  cdlemd9 35312  cdleme31sde 35492  cdleme31se 35489  cdleme31se2 35490  cdleme31snd 35493  cdleme32a 35548  cdleme32b 35549  cdleme32c 35550  cdleme32d 35551  cdleme32e 35552  cdleme32f 35553  cdleme32fva 35544  cdleme32fva1 35545  cdleme32fvcl 35547  cdleme32le 35554  cdleme48fv 35606  cdleme4gfv 35614  cdleme50eq 35648  cdleme50f 35649  cdleme50f1 35650  cdleme50f1o 35653  cdleme50laut 35654  cdleme50ldil 35655  cdleme50lebi 35647  cdleme50rn 35652  cdleme50rnlem 35651  cdlemeg49le 35618  cdlemeg49lebilem 35646
[Crawley] p. 113Lemma Ecdleme 35667  cdleme00a 35315  cdleme01N 35327  cdleme02N 35328  cdleme0a 35317  cdleme0aa 35316  cdleme0b 35318  cdleme0c 35319  cdleme0cp 35320  cdleme0cq 35321  cdleme0dN 35322  cdleme0e 35323  cdleme0ex1N 35329  cdleme0ex2N 35330  cdleme0fN 35324  cdleme0gN 35325  cdleme0moN 35331  cdleme1 35333  cdleme10 35360  cdleme10tN 35364  cdleme11 35376  cdleme11a 35366  cdleme11c 35367  cdleme11dN 35368  cdleme11e 35369  cdleme11fN 35370  cdleme11g 35371  cdleme11h 35372  cdleme11j 35373  cdleme11k 35374  cdleme11l 35375  cdleme12 35377  cdleme13 35378  cdleme14 35379  cdleme15 35384  cdleme15a 35380  cdleme15b 35381  cdleme15c 35382  cdleme15d 35383  cdleme16 35391  cdleme16aN 35365  cdleme16b 35385  cdleme16c 35386  cdleme16d 35387  cdleme16e 35388  cdleme16f 35389  cdleme16g 35390  cdleme19a 35410  cdleme19b 35411  cdleme19c 35412  cdleme19d 35413  cdleme19e 35414  cdleme19f 35415  cdleme1b 35332  cdleme2 35334  cdleme20aN 35416  cdleme20bN 35417  cdleme20c 35418  cdleme20d 35419  cdleme20e 35420  cdleme20f 35421  cdleme20g 35422  cdleme20h 35423  cdleme20i 35424  cdleme20j 35425  cdleme20k 35426  cdleme20l 35429  cdleme20l1 35427  cdleme20l2 35428  cdleme20m 35430  cdleme20y 35408  cdleme20zN 35407  cdleme21 35444  cdleme21d 35437  cdleme21e 35438  cdleme22a 35447  cdleme22aa 35446  cdleme22b 35448  cdleme22cN 35449  cdleme22d 35450  cdleme22e 35451  cdleme22eALTN 35452  cdleme22f 35453  cdleme22f2 35454  cdleme22g 35455  cdleme23a 35456  cdleme23b 35457  cdleme23c 35458  cdleme26e 35466  cdleme26eALTN 35468  cdleme26ee 35467  cdleme26f 35470  cdleme26f2 35472  cdleme26f2ALTN 35471  cdleme26fALTN 35469  cdleme27N 35476  cdleme27a 35474  cdleme27cl 35473  cdleme28c 35479  cdleme3 35343  cdleme30a 35485  cdleme31fv 35497  cdleme31fv1 35498  cdleme31fv1s 35499  cdleme31fv2 35500  cdleme31id 35501  cdleme31sc 35491  cdleme31sdnN 35494  cdleme31sn 35487  cdleme31sn1 35488  cdleme31sn1c 35495  cdleme31sn2 35496  cdleme31so 35486  cdleme35a 35555  cdleme35b 35557  cdleme35c 35558  cdleme35d 35559  cdleme35e 35560  cdleme35f 35561  cdleme35fnpq 35556  cdleme35g 35562  cdleme35h 35563  cdleme35h2 35564  cdleme35sn2aw 35565  cdleme35sn3a 35566  cdleme36a 35567  cdleme36m 35568  cdleme37m 35569  cdleme38m 35570  cdleme38n 35571  cdleme39a 35572  cdleme39n 35573  cdleme3b 35335  cdleme3c 35336  cdleme3d 35337  cdleme3e 35338  cdleme3fN 35339  cdleme3fa 35342  cdleme3g 35340  cdleme3h 35341  cdleme4 35344  cdleme40m 35574  cdleme40n 35575  cdleme40v 35576  cdleme40w 35577  cdleme41fva11 35584  cdleme41sn3aw 35581  cdleme41sn4aw 35582  cdleme41snaw 35583  cdleme42a 35578  cdleme42b 35585  cdleme42c 35579  cdleme42d 35580  cdleme42e 35586  cdleme42f 35587  cdleme42g 35588  cdleme42h 35589  cdleme42i 35590  cdleme42k 35591  cdleme42ke 35592  cdleme42keg 35593  cdleme42mN 35594  cdleme42mgN 35595  cdleme43aN 35596  cdleme43bN 35597  cdleme43cN 35598  cdleme43dN 35599  cdleme5 35346  cdleme50ex 35666  cdleme50ltrn 35664  cdleme51finvN 35663  cdleme51finvfvN 35662  cdleme51finvtrN 35665  cdleme6 35347  cdleme7 35355  cdleme7a 35349  cdleme7aa 35348  cdleme7b 35350  cdleme7c 35351  cdleme7d 35352  cdleme7e 35353  cdleme7ga 35354  cdleme8 35356  cdleme8tN 35361  cdleme9 35359  cdleme9a 35357  cdleme9b 35358  cdleme9tN 35363  cdleme9taN 35362  cdlemeda 35404  cdlemedb 35403  cdlemednpq 35405  cdlemednuN 35406  cdlemefr27cl 35510  cdlemefr32fva1 35517  cdlemefr32fvaN 35516  cdlemefrs32fva 35507  cdlemefrs32fva1 35508  cdlemefs27cl 35520  cdlemefs32fva1 35530  cdlemefs32fvaN 35529  cdlemesner 35402  cdlemeulpq 35326
[Crawley] p. 114Lemma E4atex 35181  4atexlem7 35180  cdleme0nex 35396  cdleme17a 35392  cdleme17c 35394  cdleme17d 35605  cdleme17d1 35395  cdleme17d2 35602  cdleme18a 35397  cdleme18b 35398  cdleme18c 35399  cdleme18d 35401  cdleme4a 35345
[Crawley] p. 115Lemma Ecdleme21a 35432  cdleme21at 35435  cdleme21b 35433  cdleme21c 35434  cdleme21ct 35436  cdleme21f 35439  cdleme21g 35440  cdleme21h 35441  cdleme21i 35442  cdleme22gb 35400
[Crawley] p. 116Lemma Fcdlemf 35670  cdlemf1 35668  cdlemf2 35669
[Crawley] p. 116Lemma Gcdlemftr1 35674  cdlemg16 35764  cdlemg28 35811  cdlemg28a 35800  cdlemg28b 35810  cdlemg3a 35704  cdlemg42 35836  cdlemg43 35837  cdlemg44 35840  cdlemg44a 35838  cdlemg46 35842  cdlemg47 35843  cdlemg9 35741  ltrnco 35826  ltrncom 35845  tgrpabl 35858  trlco 35834
[Crawley] p. 116Definition of Gdf-tgrp 35850
[Crawley] p. 117Lemma Gcdlemg17 35784  cdlemg17b 35769
[Crawley] p. 117Definition of Edf-edring-rN 35863  df-edring 35864
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 35867
[Crawley] p. 118Remarktendopltp 35887
[Crawley] p. 118Lemma Hcdlemh 35924  cdlemh1 35922  cdlemh2 35923
[Crawley] p. 118Lemma Icdlemi 35927  cdlemi1 35925  cdlemi2 35926
[Crawley] p. 118Lemma Jcdlemj1 35928  cdlemj2 35929  cdlemj3 35930  tendocan 35931
[Crawley] p. 118Lemma Kcdlemk 36081  cdlemk1 35938  cdlemk10 35950  cdlemk11 35956  cdlemk11t 36053  cdlemk11ta 36036  cdlemk11tb 36038  cdlemk11tc 36052  cdlemk11u-2N 35996  cdlemk11u 35978  cdlemk12 35957  cdlemk12u-2N 35997  cdlemk12u 35979  cdlemk13-2N 35983  cdlemk13 35959  cdlemk14-2N 35985  cdlemk14 35961  cdlemk15-2N 35986  cdlemk15 35962  cdlemk16-2N 35987  cdlemk16 35964  cdlemk16a 35963  cdlemk17-2N 35988  cdlemk17 35965  cdlemk18-2N 35993  cdlemk18-3N 36007  cdlemk18 35975  cdlemk19-2N 35994  cdlemk19 35976  cdlemk19u 36077  cdlemk1u 35966  cdlemk2 35939  cdlemk20-2N 35999  cdlemk20 35981  cdlemk21-2N 35998  cdlemk21N 35980  cdlemk22-3 36008  cdlemk22 36000  cdlemk23-3 36009  cdlemk24-3 36010  cdlemk25-3 36011  cdlemk26-3 36013  cdlemk26b-3 36012  cdlemk27-3 36014  cdlemk28-3 36015  cdlemk29-3 36018  cdlemk3 35940  cdlemk30 36001  cdlemk31 36003  cdlemk32 36004  cdlemk33N 36016  cdlemk34 36017  cdlemk35 36019  cdlemk36 36020  cdlemk37 36021  cdlemk38 36022  cdlemk39 36023  cdlemk39u 36075  cdlemk4 35941  cdlemk41 36027  cdlemk42 36048  cdlemk42yN 36051  cdlemk43N 36070  cdlemk45 36054  cdlemk46 36055  cdlemk47 36056  cdlemk48 36057  cdlemk49 36058  cdlemk5 35943  cdlemk50 36059  cdlemk51 36060  cdlemk52 36061  cdlemk53 36064  cdlemk54 36065  cdlemk55 36068  cdlemk55u 36073  cdlemk56 36078  cdlemk5a 35942  cdlemk5auN 35967  cdlemk5u 35968  cdlemk6 35944  cdlemk6u 35969  cdlemk7 35955  cdlemk7u-2N 35995  cdlemk7u 35977  cdlemk8 35945  cdlemk9 35946  cdlemk9bN 35947  cdlemki 35948  cdlemkid 36043  cdlemkj-2N 35989  cdlemkj 35970  cdlemksat 35953  cdlemksel 35952  cdlemksv 35951  cdlemksv2 35954  cdlemkuat 35973  cdlemkuel-2N 35991  cdlemkuel-3 36005  cdlemkuel 35972  cdlemkuv-2N 35990  cdlemkuv2-2 35992  cdlemkuv2-3N 36006  cdlemkuv2 35974  cdlemkuvN 35971  cdlemkvcl 35949  cdlemky 36033  cdlemkyyN 36069  tendoex 36082
[Crawley] p. 120Remarkdva1dim 36092
[Crawley] p. 120Lemma Lcdleml1N 36083  cdleml2N 36084  cdleml3N 36085  cdleml4N 36086  cdleml5N 36087  cdleml6 36088  cdleml7 36089  cdleml8 36090  cdleml9 36091  dia1dim 36169
[Crawley] p. 120Lemma Mdia11N 36156  diaf11N 36157  dialss 36154  diaord 36155  dibf11N 36269  djajN 36245
[Crawley] p. 120Definition of isomorphism mapdiaval 36140
[Crawley] p. 121Lemma Mcdlemm10N 36226  dia2dimlem1 36172  dia2dimlem2 36173  dia2dimlem3 36174  dia2dimlem4 36175  dia2dimlem5 36176  diaf1oN 36238  diarnN 36237  dvheveccl 36220  dvhopN 36224
[Crawley] p. 121Lemma Ncdlemn 36320  cdlemn10 36314  cdlemn11 36319  cdlemn11a 36315  cdlemn11b 36316  cdlemn11c 36317  cdlemn11pre 36318  cdlemn2 36303  cdlemn2a 36304  cdlemn3 36305  cdlemn4 36306  cdlemn4a 36307  cdlemn5 36309  cdlemn5pre 36308  cdlemn6 36310  cdlemn7 36311  cdlemn8 36312  cdlemn9 36313  diclspsn 36302
[Crawley] p. 121Definition of phi(q)df-dic 36281
[Crawley] p. 122Lemma Ndih11 36373  dihf11 36375  dihjust 36325  dihjustlem 36324  dihord 36372  dihord1 36326  dihord10 36331  dihord11b 36330  dihord11c 36332  dihord2 36335  dihord2a 36327  dihord2b 36328  dihord2cN 36329  dihord2pre 36333  dihord2pre2 36334  dihordlem6 36321  dihordlem7 36322  dihordlem7b 36323
[Crawley] p. 122Definition of isomorphism mapdihffval 36338  dihfval 36339  dihval 36340
[Diestel] p. 3Section 1.1df-cusgr 26213  df-nbgr 26209
[Diestel] p. 4Section 1.1df-subgr 26141  uhgrspan1 26176  uhgrspansubgr 26164
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 26431  vtxdgoddnumeven 26430
[Diestel] p. 27Section 1.10df-ushgr 25935
[Eisenberg] p. 67Definition 5.3df-dif 3570
[Eisenberg] p. 82Definition 6.3dfom3 8529
[Eisenberg] p. 125Definition 8.21df-map 7844
[Eisenberg] p. 216Example 13.2(4)omenps 8537
[Eisenberg] p. 310Theorem 19.8cardprc 8791
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 9362
[Enderton] p. 18Axiom of Empty Setaxnul 4779
[Enderton] p. 19Definitiondf-tp 4173
[Enderton] p. 26Exercise 5unissb 4460
[Enderton] p. 26Exercise 10pwel 4911
[Enderton] p. 28Exercise 7(b)pwun 5012
[Enderton] p. 30Theorem "Distributive laws"iinin1 4582  iinin2 4581  iinun2 4577  iunin1 4576  iunin1f 29346  iunin2 4575  uniin1 29339  uniin2 29340
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4580  iundif2 4578
[Enderton] p. 32Exercise 20unineq 3869
[Enderton] p. 33Exercise 23iinuni 4600
[Enderton] p. 33Exercise 25iununi 4601
[Enderton] p. 33Exercise 24(a)iinpw 4608
[Enderton] p. 33Exercise 24(b)iunpw 6963  iunpwss 4609
[Enderton] p. 36Definitionopthwiener 4966
[Enderton] p. 38Exercise 6(a)unipw 4909
[Enderton] p. 38Exercise 6(b)pwuni 4465
[Enderton] p. 41Lemma 3Dopeluu 4930  rnex 7085  rnexg 7083
[Enderton] p. 41Exercise 8dmuni 5323  rnuni 5532
[Enderton] p. 42Definition of a functiondffun7 5903  dffun8 5904
[Enderton] p. 43Definition of function valuefunfv2 6253
[Enderton] p. 43Definition of single-rootedfuncnv 5946
[Enderton] p. 44Definition (d)dfima2 5456  dfima3 5457
[Enderton] p. 47Theorem 3Hfvco2 6260
[Enderton] p. 49Axiom of Choice (first form)ac7 9280  ac7g 9281  df-ac 8924  dfac2 8938  dfac2a 8937  dfac3 8929  dfac7 8939
[Enderton] p. 50Theorem 3K(a)imauni 6489
[Enderton] p. 52Definitiondf-map 7844
[Enderton] p. 53Exercise 21coass 5642
[Enderton] p. 53Exercise 27dmco 5631
[Enderton] p. 53Exercise 14(a)funin 5953
[Enderton] p. 53Exercise 22(a)imass2 5489
[Enderton] p. 54Remarkixpf 7915  ixpssmap 7927
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7894
[Enderton] p. 55Axiom of Choice (second form)ac9 9290  ac9s 9300
[Enderton] p. 56Theorem 3Merref 7747
[Enderton] p. 57Lemma 3Nerthi 7778
[Enderton] p. 57Definitiondf-ec 7729
[Enderton] p. 58Definitiondf-qs 7733
[Enderton] p. 61Exercise 35df-ec 7729
[Enderton] p. 65Exercise 56(a)dmun 5320
[Enderton] p. 68Definition of successordf-suc 5717
[Enderton] p. 71Definitiondf-tr 4744  dftr4 4748
[Enderton] p. 72Theorem 4Eunisuc 5789
[Enderton] p. 73Exercise 6unisuc 5789
[Enderton] p. 73Exercise 5(a)truni 4758
[Enderton] p. 73Exercise 5(b)trint 4759  trintALT 38937
[Enderton] p. 79Theorem 4I(A1)nna0 7669
[Enderton] p. 79Theorem 4I(A2)nnasuc 7671  onasuc 7593
[Enderton] p. 79Definition of operation valuedf-ov 6638
[Enderton] p. 80Theorem 4J(A1)nnm0 7670
[Enderton] p. 80Theorem 4J(A2)nnmsuc 7672  onmsuc 7594
[Enderton] p. 81Theorem 4K(1)nnaass 7687
[Enderton] p. 81Theorem 4K(2)nna0r 7674  nnacom 7682
[Enderton] p. 81Theorem 4K(3)nndi 7688
[Enderton] p. 81Theorem 4K(4)nnmass 7689
[Enderton] p. 81Theorem 4K(5)nnmcom 7691
[Enderton] p. 82Exercise 16nnm0r 7675  nnmsucr 7690
[Enderton] p. 88Exercise 23nnaordex 7703
[Enderton] p. 129Definitiondf-en 7941
[Enderton] p. 132Theorem 6B(b)canth 6593
[Enderton] p. 133Exercise 1xpomen 8823
[Enderton] p. 133Exercise 2qnnen 14923
[Enderton] p. 134Theorem (Pigeonhole Principle)php 8129
[Enderton] p. 135Corollary 6Cphp3 8131
[Enderton] p. 136Corollary 6Enneneq 8128
[Enderton] p. 136Corollary 6D(a)pssinf 8155
[Enderton] p. 136Corollary 6D(b)ominf 8157
[Enderton] p. 137Lemma 6Fpssnn 8163
[Enderton] p. 138Corollary 6Gssfi 8165
[Enderton] p. 139Theorem 6H(c)mapen 8109
[Enderton] p. 142Theorem 6I(3)xpcdaen 8990
[Enderton] p. 142Theorem 6I(4)mapcdaen 8991
[Enderton] p. 143Theorem 6Jcda0en 8986  cda1en 8982
[Enderton] p. 144Exercise 13iunfi 8239  unifi 8240  unifi2 8241
[Enderton] p. 144Corollary 6Kundif2 4035  unfi 8212  unfi2 8214
[Enderton] p. 145Figure 38ffoss 7112
[Enderton] p. 145Definitiondf-dom 7942
[Enderton] p. 146Example 1domen 7953  domeng 7954
[Enderton] p. 146Example 3nndomo 8139  nnsdom 8536  nnsdomg 8204
[Enderton] p. 149Theorem 6L(c)mapdom1 8110  xpdom1 8044  xpdom1g 8042  xpdom2g 8041
[Enderton] p. 149Theorem 6L(d)mapdom2 8116
[Enderton] p. 151Theorem 6Mzorn 9314  zorng 9311
[Enderton] p. 151Theorem 6M(4)ac8 9299  dfac5 8936
[Enderton] p. 159Theorem 6Qunictb 9382
[Enderton] p. 164Exampleinfdif 9016
[Enderton] p. 168Definitiondf-po 5025
[Enderton] p. 192Theorem 7M(a)oneli 5823
[Enderton] p. 192Theorem 7M(b)ontr1 5759
[Enderton] p. 192Theorem 7M(c)onirri 5822
[Enderton] p. 193Corollary 7N(b)0elon 5766
[Enderton] p. 193Corollary 7N(c)onsuci 7023
[Enderton] p. 193Corollary 7N(d)ssonunii 6972
[Enderton] p. 194Remarkonprc 6969
[Enderton] p. 194Exercise 16suc11 5819
[Enderton] p. 197Definitiondf-card 8750
[Enderton] p. 197Theorem 7Pcarden 9358
[Enderton] p. 200Exercise 25tfis 7039
[Enderton] p. 202Lemma 7Tr1tr 8624
[Enderton] p. 202Definitiondf-r1 8612
[Enderton] p. 202Theorem 7Qr1val1 8634
[Enderton] p. 204Theorem 7V(b)rankval4 8715
[Enderton] p. 206Theorem 7X(b)en2lp 8495
[Enderton] p. 207Exercise 30rankpr 8705  rankprb 8699  rankpw 8691  rankpwi 8671  rankuniss 8714
[Enderton] p. 207Exercise 34opthreg 8500
[Enderton] p. 208Exercise 35suc11reg 8501
[Enderton] p. 212Definition of alephalephval3 8918
[Enderton] p. 213Theorem 8A(a)alephord2 8884
[Enderton] p. 213Theorem 8A(b)cardalephex 8898
[Enderton] p. 218Theorem Schema 8Eonfununi 7423
[Enderton] p. 222Definition of kardkarden 8743  kardex 8742
[Enderton] p. 238Theorem 8Roeoa 7662
[Enderton] p. 238Theorem 8Soeoe 7664
[Enderton] p. 240Exercise 25oarec 7627
[Enderton] p. 257Definition of cofinalitycflm 9057
[FaureFrolicher] p. 57Definition 3.1.9mreexd 16283
[FaureFrolicher] p. 83Definition 4.1.1df-mri 16229
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 17158  mrieqv2d 16280  mrieqvd 16279
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 16284
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 16289  mreexexlem2d 16286
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 17164  mreexfidimd 16292
[Frege1879] p. 11Statementdf3or2 37879
[Frege1879] p. 12Statementdf3an2 37880  dfxor4 37877  dfxor5 37878
[Frege1879] p. 26Axiom 1ax-frege1 37904
[Frege1879] p. 26Axiom 2ax-frege2 37905
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 37909
[Frege1879] p. 31Proposition 4frege4 37913
[Frege1879] p. 32Proposition 5frege5 37914
[Frege1879] p. 33Proposition 6frege6 37920
[Frege1879] p. 34Proposition 7frege7 37922
[Frege1879] p. 35Axiom 8ax-frege8 37923  axfrege8 37921
[Frege1879] p. 35Proposition 8pm2.04 90  wl-pm2.04 33238
[Frege1879] p. 35Proposition 9frege9 37926
[Frege1879] p. 36Proposition 10frege10 37934
[Frege1879] p. 36Proposition 11frege11 37928
[Frege1879] p. 37Proposition 12frege12 37927
[Frege1879] p. 37Proposition 13frege13 37936
[Frege1879] p. 37Proposition 14frege14 37937
[Frege1879] p. 38Proposition 15frege15 37940
[Frege1879] p. 38Proposition 16frege16 37930
[Frege1879] p. 39Proposition 17frege17 37935
[Frege1879] p. 39Proposition 18frege18 37932
[Frege1879] p. 39Proposition 19frege19 37938
[Frege1879] p. 40Proposition 20frege20 37942
[Frege1879] p. 40Proposition 21frege21 37941
[Frege1879] p. 41Proposition 22frege22 37933
[Frege1879] p. 42Proposition 23frege23 37939
[Frege1879] p. 42Proposition 24frege24 37929
[Frege1879] p. 42Proposition 25frege25 37931  rp-frege25 37919
[Frege1879] p. 42Proposition 26frege26 37924
[Frege1879] p. 43Axiom 28ax-frege28 37944
[Frege1879] p. 43Proposition 27frege27 37925
[Frege1879] p. 43Proposition 28con3 149
[Frege1879] p. 43Proposition 29frege29 37945
[Frege1879] p. 44Axiom 31ax-frege31 37948  axfrege31 37947
[Frege1879] p. 44Proposition 30frege30 37946
[Frege1879] p. 44Proposition 31notnotr 125
[Frege1879] p. 44Proposition 32frege32 37949
[Frege1879] p. 44Proposition 33frege33 37950
[Frege1879] p. 45Proposition 34frege34 37951
[Frege1879] p. 45Proposition 35frege35 37952
[Frege1879] p. 45Proposition 36frege36 37953
[Frege1879] p. 46Proposition 37frege37 37954
[Frege1879] p. 46Proposition 38frege38 37955
[Frege1879] p. 46Proposition 39frege39 37956
[Frege1879] p. 46Proposition 40frege40 37957
[Frege1879] p. 47Axiom 41ax-frege41 37959  axfrege41 37958
[Frege1879] p. 47Proposition 41notnot 136
[Frege1879] p. 47Proposition 42frege42 37960
[Frege1879] p. 47Proposition 43frege43 37961
[Frege1879] p. 47Proposition 44frege44 37962
[Frege1879] p. 47Proposition 45frege45 37963
[Frege1879] p. 48Proposition 46frege46 37964
[Frege1879] p. 48Proposition 47frege47 37965
[Frege1879] p. 49Proposition 48frege48 37966
[Frege1879] p. 49Proposition 49frege49 37967
[Frege1879] p. 49Proposition 50frege50 37968
[Frege1879] p. 50Axiom 52ax-frege52a 37971  ax-frege52c 38002  frege52aid 37972  frege52b 38003
[Frege1879] p. 50Axiom 54ax-frege54a 37976  ax-frege54c 38006  frege54b 38007
[Frege1879] p. 50Proposition 51frege51 37969
[Frege1879] p. 50Proposition 52dfsbcq 3431
[Frege1879] p. 50Proposition 53frege53a 37974  frege53aid 37973  frege53b 38004  frege53c 38028
[Frege1879] p. 50Proposition 54biid 251  eqid 2620
[Frege1879] p. 50Proposition 55frege55a 37982  frege55aid 37979  frege55b 38011  frege55c 38032  frege55cor1a 37983  frege55lem2a 37981  frege55lem2b 38010  frege55lem2c 38031
[Frege1879] p. 50Proposition 56frege56a 37985  frege56aid 37984  frege56b 38012  frege56c 38033
[Frege1879] p. 51Axiom 58ax-frege58a 37989  ax-frege58b 38015  frege58bid 38016  frege58c 38035
[Frege1879] p. 51Proposition 57frege57a 37987  frege57aid 37986  frege57b 38013  frege57c 38034
[Frege1879] p. 51Proposition 58spsbc 3442
[Frege1879] p. 51Proposition 59frege59a 37991  frege59b 38018  frege59c 38036
[Frege1879] p. 52Proposition 60frege60a 37992  frege60b 38019  frege60c 38037
[Frege1879] p. 52Proposition 61frege61a 37993  frege61b 38020  frege61c 38038
[Frege1879] p. 52Proposition 62frege62a 37994  frege62b 38021  frege62c 38039
[Frege1879] p. 52Proposition 63frege63a 37995  frege63b 38022  frege63c 38040
[Frege1879] p. 53Proposition 64frege64a 37996  frege64b 38023  frege64c 38041
[Frege1879] p. 53Proposition 65frege65a 37997  frege65b 38024  frege65c 38042
[Frege1879] p. 54Proposition 66frege66a 37998  frege66b 38025  frege66c 38043
[Frege1879] p. 54Proposition 67frege67a 37999  frege67b 38026  frege67c 38044
[Frege1879] p. 54Proposition 68frege68a 38000  frege68b 38027  frege68c 38045
[Frege1879] p. 55Definition 69dffrege69 38046
[Frege1879] p. 58Proposition 70frege70 38047
[Frege1879] p. 59Proposition 71frege71 38048
[Frege1879] p. 59Proposition 72frege72 38049
[Frege1879] p. 59Proposition 73frege73 38050
[Frege1879] p. 60Definition 76dffrege76 38053
[Frege1879] p. 60Proposition 74frege74 38051
[Frege1879] p. 60Proposition 75frege75 38052
[Frege1879] p. 62Proposition 77frege77 38054  frege77d 37857
[Frege1879] p. 63Proposition 78frege78 38055
[Frege1879] p. 63Proposition 79frege79 38056
[Frege1879] p. 63Proposition 80frege80 38057
[Frege1879] p. 63Proposition 81frege81 38058  frege81d 37858
[Frege1879] p. 64Proposition 82frege82 38059
[Frege1879] p. 65Proposition 83frege83 38060  frege83d 37859
[Frege1879] p. 65Proposition 84frege84 38061
[Frege1879] p. 66Proposition 85frege85 38062
[Frege1879] p. 66Proposition 86frege86 38063
[Frege1879] p. 66Proposition 87frege87 38064  frege87d 37861
[Frege1879] p. 67Proposition 88frege88 38065
[Frege1879] p. 68Proposition 89frege89 38066
[Frege1879] p. 68Proposition 90frege90 38067
[Frege1879] p. 68Proposition 91frege91 38068  frege91d 37862
[Frege1879] p. 69Proposition 92frege92 38069
[Frege1879] p. 70Proposition 93frege93 38070
[Frege1879] p. 70Proposition 94frege94 38071
[Frege1879] p. 70Proposition 95frege95 38072
[Frege1879] p. 71Definition 99dffrege99 38076
[Frege1879] p. 71Proposition 96frege96 38073  frege96d 37860
[Frege1879] p. 71Proposition 97frege97 38074  frege97d 37863
[Frege1879] p. 71Proposition 98frege98 38075  frege98d 37864
[Frege1879] p. 72Proposition 100frege100 38077
[Frege1879] p. 72Proposition 101frege101 38078
[Frege1879] p. 72Proposition 102frege102 38079  frege102d 37865
[Frege1879] p. 73Proposition 103frege103 38080
[Frege1879] p. 73Proposition 104frege104 38081
[Frege1879] p. 73Proposition 105frege105 38082
[Frege1879] p. 73Proposition 106frege106 38083  frege106d 37866
[Frege1879] p. 74Proposition 107frege107 38084
[Frege1879] p. 74Proposition 108frege108 38085  frege108d 37867
[Frege1879] p. 74Proposition 109frege109 38086  frege109d 37868
[Frege1879] p. 75Proposition 110frege110 38087
[Frege1879] p. 75Proposition 111frege111 38088  frege111d 37870
[Frege1879] p. 76Proposition 112frege112 38089
[Frege1879] p. 76Proposition 113frege113 38090
[Frege1879] p. 76Proposition 114frege114 38091  frege114d 37869
[Frege1879] p. 77Definition 115dffrege115 38092
[Frege1879] p. 77Proposition 116frege116 38093
[Frege1879] p. 78Proposition 117frege117 38094
[Frege1879] p. 78Proposition 118frege118 38095
[Frege1879] p. 78Proposition 119frege119 38096
[Frege1879] p. 78Proposition 120frege120 38097
[Frege1879] p. 79Proposition 121frege121 38098
[Frege1879] p. 79Proposition 122frege122 38099  frege122d 37871
[Frege1879] p. 79Proposition 123frege123 38100
[Frege1879] p. 80Proposition 124frege124 38101  frege124d 37872
[Frege1879] p. 81Proposition 125frege125 38102
[Frege1879] p. 81Proposition 126frege126 38103  frege126d 37873
[Frege1879] p. 82Proposition 127frege127 38104
[Frege1879] p. 83Proposition 128frege128 38105
[Frege1879] p. 83Proposition 129frege129 38106  frege129d 37874
[Frege1879] p. 84Proposition 130frege130 38107
[Frege1879] p. 85Proposition 131frege131 38108  frege131d 37875
[Frege1879] p. 86Proposition 132frege132 38109
[Frege1879] p. 86Proposition 133frege133 38110  frege133d 37876
[Fremlin1] p. 13Definition 111G (b)df-salgen 40296
[Fremlin1] p. 13Definition 111G (d)borelmbl 40613
[Fremlin1] p. 13Proposition 111G (b)salgenss 40317
[Fremlin1] p. 14Definition 112Aismea 40431
[Fremlin1] p. 15Remark 112B (d)psmeasure 40451
[Fremlin1] p. 15Property 112C (b)meassle 40443
[Fremlin1] p. 15Property 112C (c)meaunle 40444
[Fremlin1] p. 16Property 112C (d)iundjiun 40440  meaiunle 40449  meaiunlelem 40448
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 40461  meaiuninc2 40462  meaiuninclem 40460
[Fremlin1] p. 16Proposition 112C (f)meaiininc 40464  meaiininc2 40465  meaiininclem 40463
[Fremlin1] p. 19Theorem 113Ccaragen0 40483  caragendifcl 40491  caratheodory 40505  omelesplit 40495
[Fremlin1] p. 19Definition 113Aisome 40471  isomennd 40508  isomenndlem 40507
[Fremlin1] p. 19Remark 113B (c)omeunle 40493
[Fremlin1] p. 19Definition 112Dfcaragencmpl 40512  voncmpl 40598
[Fremlin1] p. 19Definition 113A (ii)omessle 40475
[Fremlin1] p. 20Theorem 113Ccarageniuncl 40500  carageniuncllem1 40498  carageniuncllem2 40499  caragenuncl 40490  caragenuncllem 40489  caragenunicl 40501
[Fremlin1] p. 21Remark 113Dcaragenel2d 40509
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 40503  caratheodorylem2 40504
[Fremlin1] p. 21Exercise 113Xacaragencmpl 40512
[Fremlin1] p. 23Lemma 114Bhoidmv1le 40571  hoidmv1lelem1 40568  hoidmv1lelem2 40569  hoidmv1lelem3 40570
[Fremlin1] p. 25Definition 114Eisvonmbl 40615
[Fremlin1] p. 29Lemma 115Bhoidmv1le 40571  hoidmvle 40577  hoidmvlelem1 40572  hoidmvlelem2 40573  hoidmvlelem3 40574  hoidmvlelem4 40575  hoidmvlelem5 40576  hsphoidmvle2 40562  hsphoif 40553  hsphoival 40556
[Fremlin1] p. 29Definition 1135 (b)hoicvr 40525
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 40533
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 40560  hoidmvn0val 40561  hoidmvval 40554  hoidmvval0 40564  hoidmvval0b 40567
[Fremlin1] p. 30Lemma 115Bhoiprodp1 40565  hsphoidmvle 40563
[Fremlin1] p. 30Definition 115Cdf-ovoln 40514  df-voln 40516
[Fremlin1] p. 30Proposition 115D (a)dmovn 40581  ovn0 40543  ovn0lem 40542  ovnf 40540  ovnome 40550  ovnssle 40538  ovnsslelem 40537  ovnsupge0 40534
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 40580  ovnhoilem1 40578  ovnhoilem2 40579  vonhoi 40644
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 40597  hoidifhspf 40595  hoidifhspval 40585  hoidifhspval2 40592  hoidifhspval3 40596  hspmbl 40606  hspmbllem1 40603  hspmbllem2 40604  hspmbllem3 40605
[Fremlin1] p. 31Definition 115Evoncmpl 40598  vonmea 40551
[Fremlin1] p. 32Proposition 115G (a)hoimbl 40608  hoimbl2 40642  hoimbllem 40607  hspdifhsp 40593  opnvonmbl 40611  opnvonmbllem2 40610
[Fremlin1] p. 32Proposition 115G (b)borelmbl 40613
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 40656  iccvonmbllem 40655  ioovonmbl 40654
[Fremlin1] p. 32Proposition 115G (d)vonicc 40662  vonicclem2 40661  vonioo 40659  vonioolem2 40658  vonn0icc 40665  vonn0icc2 40669  vonn0ioo 40664  vonn0ioo2 40667
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 40666  snvonmbl 40663  vonct 40670  vonsn 40668
[Fremlin1] p. 35Lemma 121Asubsalsal 40340
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 40339  subsaliuncllem 40338
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 40697  salpreimalegt 40683  salpreimaltle 40698
[Fremlin1] p. 35Proposition 121B (i)issmf 40700  issmff 40706  issmflem 40699
[Fremlin1] p. 35Proposition 121B (ii)issmfle 40717  issmflelem 40716  smfpreimale 40726
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 40728  issmfgtlem 40727
[Fremlin1] p. 36Definition 121Cdf-smblfn 40673  issmf 40700  issmff 40706  issmfge 40741  issmfgelem 40740  issmfgt 40728  issmfgtlem 40727  issmfle 40717  issmflelem 40716  issmflem 40699
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 40681  salpreimagtlt 40702  salpreimalelt 40701
[Fremlin1] p. 36Proposition 121B (iv)issmfge 40741  issmfgelem 40740
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 40725
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 40723  cnfsmf 40712
[Fremlin1] p. 36Proposition 121D (c)decsmf 40738  decsmflem 40737  incsmf 40714  incsmflem 40713
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 40677  pimconstlt1 40678  smfconst 40721
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 40766
[Fremlin1] p. 37Proposition 121E (d)smfmul 40765  smfmullem1 40761  smfmullem2 40762  smfmullem3 40763  smfmullem4 40764
[Fremlin1] p. 37Proposition 121E (e)smfdiv 40767
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 40770  smfpimbor1lem2 40769
[Fremlin1] p. 37Proposition 121E (g)smfco 40772
[Fremlin1] p. 37Proposition 121E (h)smfres 40760
[Fremlin1] p. 38Proposition 121E (e)smfrec 40759
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 40768  smfresal 40758
[Fremlin1] p. 38Proposition 121F (a)smflim 40748  smflim2 40775  smflimlem1 40742  smflimlem2 40743  smflimlem3 40744  smflimlem4 40745  smflimlem5 40746  smflimlem6 40747  smflimmpt 40779
[Fremlin1] p. 38Proposition 121F (b)smfsup 40783  smfsuplem1 40780  smfsuplem2 40781  smfsuplem3 40782  smfsupmpt 40784  smfsupxr 40785
[Fremlin1] p. 38Proposition 121F (c)smfinf 40787  smfinflem 40786  smfinfmpt 40788
[Fremlin1] p. 39Remark 121Gsmflim 40748  smflim2 40775  smflimmpt 40779
[Fremlin1] p. 39Proposition 121Fsmfpimcc 40777
[Fremlin1] p. 39Proposition 121F (d)smflimsup 40797  smflimsuplem2 40790  smflimsuplem6 40794  smflimsuplem7 40795  smflimsuplem8 40796  smflimsupmpt 40798
[Fremlin1] p. 39Proposition 121F (e)smfliminf 40800  smfliminflem 40799  smfliminfmpt 40801
[Fremlin1] p. 80Definition 135E (b)df-smblfn 40673
[Fremlin5] p. 193Proposition 563Gbnulmbl2 23285
[Fremlin5] p. 213Lemma 565Cauniioovol 23328
[Fremlin5] p. 214Lemma 565Cauniioombl 23338
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 33461
[Fremlin5] p. 220Theorem 565Maftc1anc 33464
[FreydScedrov] p. 283Axiom of Infinityax-inf 8520  inf1 8504  inf2 8505
[Gleason] p. 117Proposition 9-2.1df-enq 9718  enqer 9728
[Gleason] p. 117Proposition 9-2.2df-1nq 9723  df-nq 9719
[Gleason] p. 117Proposition 9-2.3df-plpq 9715  df-plq 9721
[Gleason] p. 119Proposition 9-2.4caovmo 6856  df-mpq 9716  df-mq 9722
[Gleason] p. 119Proposition 9-2.5df-rq 9724
[Gleason] p. 119Proposition 9-2.6ltexnq 9782
[Gleason] p. 120Proposition 9-2.6(i)halfnq 9783  ltbtwnnq 9785
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 9778
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 9779
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 9786
[Gleason] p. 121Definition 9-3.1df-np 9788
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 9800
[Gleason] p. 121Definition 9-3.1(iii)prnmax 9802
[Gleason] p. 122Definitiondf-1p 9789
[Gleason] p. 122Remark (1)prub 9801
[Gleason] p. 122Lemma 9-3.4prlem934 9840
[Gleason] p. 122Proposition 9-3.2df-ltp 9792
[Gleason] p. 122Proposition 9-3.3ltsopr 9839  psslinpr 9838  supexpr 9861  suplem1pr 9859  suplem2pr 9860
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 9850  ltexprlem1 9843  ltexprlem2 9844  ltexprlem3 9845  ltexprlem4 9846  ltexprlem5 9847  ltexprlem6 9848  ltexprlem7 9849
[Gleason] p. 123Proposition 9-3.5(v)ltapr 9852  ltaprlem 9851
[Gleason] p. 124Lemma 9-3.6prlem936 9854
[Gleason] p. 124Proposition 9-3.7df-mp 9791  mulclpr 9827  mulclprlem 9826  reclem2pr 9855
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 9836
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 9831
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 9830
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 9835
[Gleason] p. 124Proposition 9-3.7(v)recexpr 9858  reclem3pr 9856  reclem4pr 9857
[Gleason] p. 126Proposition 9-4.1df-enr 9862  enrer 9871
[Gleason] p. 126Proposition 9-4.2df-0r 9867  df-1r 9868  df-nr 9863
[Gleason] p. 126Proposition 9-4.3df-mr 9865  df-plr 9864  negexsr 9908  recexsr 9913  recexsrlem 9909
[Gleason] p. 127Proposition 9-4.4df-ltr 9866
[Gleason] p. 130Proposition 10-1.3creui 11000  creur 10999  cru 10997
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 9994  axcnre 9970
[Gleason] p. 132Definition 10-3.1crim 13836  crimd 13953  crimi 13914  crre 13835  crred 13952  crrei 13913
[Gleason] p. 132Definition 10-3.2remim 13838  remimd 13919
[Gleason] p. 133Definition 10.36absval2 14005  absval2d 14165  absval2i 14117
[Gleason] p. 133Proposition 10-3.4(c)cjmul 13863  cjmuld 13942  cjmuli 13910
[Gleason] p. 133Proposition 10-3.4(e)cjcj 13861  cjcjd 13920  cjcji 13892
[Gleason] p. 133Proposition 10-3.4(f)cjre 13860  cjreb 13844  cjrebd 13923  cjrebi 13895  cjred 13947  rere 13843  rereb 13841  rerebd 13922  rerebi 13894  rered 13945
[Gleason] p. 133Proposition 10-3.7(a)absval 13959
[Gleason] p. 133Proposition 10-3.7(b)abscj 14000  abscjd 14170  abscji 14121
[Gleason] p. 133Proposition 10-3.7(c)abs00 14010  abs00d 14166  abs00i 14118  absne0d 14167
[Gleason] p. 133Proposition 10-3.7(d)releabs 14042  releabsd 14171  releabsi 14122
[Gleason] p. 133Proposition 10-3.7(f)absmul 14015  absmuld 14174  absmuli 14124
[Gleason] p. 133Proposition 10-3.7(h)abstri 14051  abstrid 14176  abstrii 14128
[Gleason] p. 134Definition 10-4.10exp0e1 12848  df-exp 12844  exp0 12847  expp1 12850  expp1d 12992
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 24415  cxpmuld 24461  expmul 12888  expmuld 12994  expmulz 12889
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 24412  mulcxpd 24455  mulexp 12882  mulexpd 13006  mulexpz 12883
[Gleason] p. 140Exercise 1znnen 14922
[Gleason] p. 141Definition 11-2.1fzval 12313
[Gleason] p. 168Proposition 12-2.1(b)climsub 14345  rlimsub 14355
[Gleason] p. 168Proposition 12-2.1(c)climmul 14344  rlimmul 14356
[Gleason] p. 171Corollary 12-2.2climmulc2 14348
[Gleason] p. 172Corollary 12-2.5climrecl 14295
[Gleason] p. 172Proposition 12-2.4(c)climabs 14315  climcj 14316  climim 14318  climre 14317  rlimabs 14320  rlimcj 14321  rlimim 14323  rlimre 14322
[Gleason] p. 173Definition 12-3.1df-ltxr 10064  df-xr 10063  ltxr 11934
[Gleason] p. 175Definition 12-4.1df-limsup 14183  limsupval 14186
[Gleason] p. 180Theorem 12-5.1climsup 14381
[Gleason] p. 180Theorem 12-5.3caucvg 14390  caucvgb 14391  caucvgr 14387  climcau 14382
[Gleason] p. 182Exercise 3cvgcmp 14529
[Gleason] p. 182Exercise 4cvgrat 14596
[Gleason] p. 195Theorem 13-2.12abs1m 14056
[Gleason] p. 217Lemma 13-4.1btwnzge0 12612
[Gleason] p. 223Definition 14-1.1df-met 19721
[Gleason] p. 223Definition 14-1.1(a)met0 22129  xmet0 22128
[Gleason] p. 223Definition 14-1.1(b)metgt0 22145
[Gleason] p. 223Definition 14-1.1(c)metsym 22136
[Gleason] p. 223Definition 14-1.1(d)mettri 22138  mstri 22255  xmettri 22137  xmstri 22254
[Gleason] p. 225Definition 14-1.5xpsmet 22168
[Gleason] p. 230Proposition 14-2.6txlm 21432
[Gleason] p. 240Theorem 14-4.3metcnp4 23089
[Gleason] p. 240Proposition 14-4.2metcnp3 22326
[Gleason] p. 243Proposition 14-4.16addcn 22649  addcn2 14305  mulcn 22651  mulcn2 14307  subcn 22650  subcn2 14306
[Gleason] p. 295Remarkbcval3 13076  bcval4 13077
[Gleason] p. 295Equation 2bcpasc 13091
[Gleason] p. 295Definition of binomial coefficientbcval 13074  df-bc 13073
[Gleason] p. 296Remarkbcn0 13080  bcnn 13082
[Gleason] p. 296Theorem 15-2.8binom 14543
[Gleason] p. 308Equation 2ef0 14802
[Gleason] p. 308Equation 3efcj 14803
[Gleason] p. 309Corollary 15-4.3efne0 14808
[Gleason] p. 309Corollary 15-4.4efexp 14812
[Gleason] p. 311Equation 17sincossq 14887
[Gleason] p. 311Equation 18cosbnd 14892  sinbnd 14891
[Gleason] p. 311Lemma 15-4.7sqeqor 12961  sqeqori 12959
[Gleason] p. 311Definition of pidf-pi 14784
[Godowski] p. 730Equation SFgoeqi 29102
[GodowskiGreechie] p. 249Equation IV3oai 28497
[Golan] p. 1Remarksrgisid 18509
[Golan] p. 1Definitiondf-srg 18487
[Golan] p. 149Definitiondf-slmd 29728
[GramKnuthPat], p. 47Definition 2.42df-fwddif 32241
[Gratzer] p. 23Section 0.6df-mre 16227
[Gratzer] p. 27Section 0.6df-mri 16229
[Hall] p. 1Section 1.1df-asslaw 41589  df-cllaw 41587  df-comlaw 41588
[Hall] p. 2Section 1.2df-clintop 41601
[Hall] p. 7Section 1.3df-sgrp2 41622
[Halmos] p. 31Theorem 17.3riesz1 28894  riesz2 28895
[Halmos] p. 41Definition of Hermitianhmopadj2 28770
[Halmos] p. 42Definition of projector orderingpjordi 29002
[Halmos] p. 43Theorem 26.1elpjhmop 29014  elpjidm 29013  pjnmopi 28977
[Halmos] p. 44Remarkpjinormi 28516  pjinormii 28505
[Halmos] p. 44Theorem 26.2elpjch 29018  pjrn 28536  pjrni 28531  pjvec 28525
[Halmos] p. 44Theorem 26.3pjnorm2 28556
[Halmos] p. 44Theorem 26.4hmopidmpj 28983  hmopidmpji 28981
[Halmos] p. 45Theorem 27.1pjinvari 29020
[Halmos] p. 45Theorem 27.3pjoci 29009  pjocvec 28526
[Halmos] p. 45Theorem 27.4pjorthcoi 28998
[Halmos] p. 48Theorem 29.2pjssposi 29001
[Halmos] p. 48Theorem 29.3pjssdif1i 29004  pjssdif2i 29003
[Halmos] p. 50Definition of spectrumdf-spec 28684
[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 1720
[Hatcher] p. 25Definitiondf-phtpc 22772  df-phtpy 22751
[Hatcher] p. 26Definitiondf-pco 22786  df-pi1 22789
[Hatcher] p. 26Proposition 1.2phtpcer 22775
[Hatcher] p. 26Proposition 1.3pi1grp 22831
[Hefferon] p. 240Definition 3.12df-dmat 20277  df-dmatalt 41952
[Helfgott] p. 2Theoremtgoldbach 41470
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 41455
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 41467  bgoldbtbnd 41462  bgoldbtbnd 41462  tgblthelfgott 41468
[Helfgott] p. 5Proposition 1.1circlevma 30694
[Helfgott] p. 69Statement 7.49circlemethhgt 30695
[Helfgott] p. 69Statement 7.50hgt750lema 30709  hgt750lemb 30708  hgt750leme 30710  hgt750lemf 30705  hgt750lemg 30706
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 41464  tgoldbachgt 30715  tgoldbachgtALTV 41465  tgoldbachgtd 30714
[Helfgott] p. 70Statement 7.49ax-hgt749 30696
[Herstein] p. 54Exercise 28df-grpo 27317
[Herstein] p. 55Lemma 2.2.1(a)grpideu 17414  grpoideu 27333  mndideu 17285
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 17437  grpoinveu 27343
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 17463  grpo2inv 27355
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 17474  grpoinvop 27357
[Herstein] p. 57Exercise 1dfgrp3e 17496
[Hitchcock] p. 5Rule A3mptnan 1691
[Hitchcock] p. 5Rule A4mptxor 1692
[Hitchcock] p. 5Rule A5mtpxor 1694
[Holland] p. 1519Theorem 2sumdmdi 29249
[Holland] p. 1520Lemma 5cdj1i 29262  cdj3i 29270  cdj3lem1 29263  cdjreui 29261
[Holland] p. 1524Lemma 7mddmdin0i 29260
[Holland95] p. 13Theorem 3.6hlathil 37072
[Holland95] p. 14Line 15hgmapvs 37002
[Holland95] p. 14Line 16hdmaplkr 37024
[Holland95] p. 14Line 17hdmapellkr 37025
[Holland95] p. 14Line 19hdmapglnm2 37022
[Holland95] p. 14Line 20hdmapip0com 37028
[Holland95] p. 14Theorem 3.6hdmapevec2 36947
[Holland95] p. 14Lines 24 and 25hdmapoc 37042
[Holland95] p. 204Definition of involutiondf-srng 18827
[Holland95] p. 212Definition of subspacedf-psubsp 34608
[Holland95] p. 214Lemma 3.3lclkrlem2v 36636
[Holland95] p. 214Definition 3.2df-lpolN 36589
[Holland95] p. 214Definition of nonsingularpnonsingN 35038
[Holland95] p. 215Lemma 3.3(1)dihoml4 36485  poml4N 35058
[Holland95] p. 215Lemma 3.3(2)dochexmid 36576  pexmidALTN 35083  pexmidN 35074
[Holland95] p. 218Theorem 3.6lclkr 36641
[Holland95] p. 218Definition of dual vector spacedf-ldual 34230  ldualset 34231
[Holland95] p. 222Item 1df-lines 34606  df-pointsN 34607
[Holland95] p. 222Item 2df-polarityN 35008
[Holland95] p. 223Remarkispsubcl2N 35052  omllaw4 34352  pol1N 35015  polcon3N 35022
[Holland95] p. 223Definitiondf-psubclN 35040
[Holland95] p. 223Equation for polaritypolval2N 35011
[Hughes] p. 44Equation 1.21bax-his3 27911
[Hughes] p. 47Definition of projection operatordfpjop 29011
[Hughes] p. 49Equation 1.30eighmre 28792  eigre 28664  eigrei 28663
[Hughes] p. 49Equation 1.31eighmorth 28793  eigorth 28667  eigorthi 28666
[Hughes] p. 137Remark (ii)eigposi 28665
[Huneke] p. 1Claim 1frgrncvvdeq 27153
[Huneke] p. 1Statement 1frgrncvvdeqlem7 27149
[Huneke] p. 1Statement 2frgrncvvdeqlem8 27150
[Huneke] p. 1Statement 3frgrncvvdeqlem9 27151
[Huneke] p. 2Claim 2frgrregorufr 27163  frgrregorufr0 27162  frgrregorufrg 27164
[Huneke] p. 2Claim 3frgrhash2wsp 27170  frrusgrord 27179  frrusgrord0 27178
[Huneke] p. 2Statement 4frgrwopreglem4 27157
[Huneke] p. 2Statement 5frgrwopreg1 27160  frgrwopreg2 27161
[Huneke] p. 2Statement 6frgrwopreglem5 27158
[Huneke] p. 2Statement 7fusgreghash2wspv 27173
[Huneke] p. 2Statement 8fusgreghash2wsp 27176
[Huneke] p. 2Statement 9clwlksndivn 26952  numclwwlk1 27202  numclwwlk8 27220
[Huneke] p. 2Definition 3frgrwopreglem1 27154
[Huneke] p. 2Definition 4df-clwlks 26648
[Huneke] p. 2Definition 5numclwwlkovf 27185
[Huneke] p. 2Definition 6numclwwlkovg 27192
[Huneke] p. 2Definition 7numclwwlkovh 27205
[Huneke] p. 2Statement 10numclwwlk2 27211
[Huneke] p. 2Statement 11rusgrnumwlkg 26853
[Huneke] p. 2Statement 12numclwwlk3 27213
[Huneke] p. 2Statement 13numclwwlk5 27216
[Huneke] p. 2Statement 14numclwwlk7 27219
[Indrzejczak] p. 33Definition ` `Enatded 27230  natded 27230
[Indrzejczak] p. 33Definition ` `Inatded 27230
[Indrzejczak] p. 34Definition ` `Enatded 27230  natded 27230
[Indrzejczak] p. 34Definition ` `Inatded 27230
[Jech] p. 4Definition of classcv 1480  cvjust 2615
[Jech] p. 42Lemma 6.1alephexp1 9386
[Jech] p. 42Equation 6.1alephadd 9384  alephmul 9385
[Jech] p. 43Lemma 6.2infmap 9383  infmap2 9025
[Jech] p. 71Lemma 9.3jech9.3 8662
[Jech] p. 72Equation 9.3scott0 8734  scottex 8733
[Jech] p. 72Exercise 9.1rankval4 8715
[Jech] p. 72Scheme "Collection Principle"cp 8739
[Jech] p. 78Noteopthprc 5157
[JonesMatijasevic] p. 694Definition 2.3rmxyval 37299
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 37389
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 37390
[JonesMatijasevic] p. 695Equation 2.9rmxp1 37316  rmyp1 37317
[JonesMatijasevic] p. 695Equation 2.10rmxm1 37318  rmym1 37319
[JonesMatijasevic] p. 695Equation 2.11rmx0 37309  rmx1 37310  rmxluc 37320
[JonesMatijasevic] p. 695Equation 2.12rmy0 37313  rmy1 37314  rmyluc 37321
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 37323
[JonesMatijasevic] p. 695Equation 2.14rmydbl 37324
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 37346  jm2.17b 37347  jm2.17c 37348
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 37379
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 37383
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 37374
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 37349  jm2.24nn 37345
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 37388
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 37394  rmygeid 37350
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 37406
[Juillerat] p. 11Section *5etransc 40263  etransclem47 40261  etransclem48 40262
[Juillerat] p. 12Equation (7)etransclem44 40258
[Juillerat] p. 12Equation *(7)etransclem46 40260
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 40246
[Juillerat] p. 13Proofetransclem35 40249
[Juillerat] p. 13Part of case 2 proven inetransclem38 40252
[Juillerat] p. 13Part of case 2 provenetransclem24 40238
[Juillerat] p. 13Part of case 2: proven inetransclem41 40255
[Juillerat] p. 14Proofetransclem23 40237
[KalishMontague] p. 81Note 1ax-6 1886
[KalishMontague] p. 85Lemma 2equid 1937
[KalishMontague] p. 85Lemma 3equcomi 1942
[KalishMontague] p. 86Lemma 7cbvalivw 1932  cbvaliw 1931
[KalishMontague] p. 87Lemma 8spimvw 1925  spimw 1924
[KalishMontague] p. 87Lemma 9spfw 1963  spw 1965
[Kalmbach] p. 14Definition of latticechabs1 28345  chabs1i 28347  chabs2 28346  chabs2i 28348  chjass 28362  chjassi 28315  latabs1 17068  latabs2 17069
[Kalmbach] p. 15Definition of atomdf-at 29167  ela 29168
[Kalmbach] p. 15Definition of coverscvbr2 29112  cvrval2 34380
[Kalmbach] p. 16Definitiondf-ol 34284  df-oml 34285
[Kalmbach] p. 20Definition of commutescmbr 28413  cmbri 28419  cmtvalN 34317  df-cm 28412  df-cmtN 34283
[Kalmbach] p. 22Remarkomllaw5N 34353  pjoml5 28442  pjoml5i 28417
[Kalmbach] p. 22Definitionpjoml2 28440  pjoml2i 28414
[Kalmbach] p. 22Theorem 2(v)cmcm 28443  cmcmi 28421  cmcmii 28426  cmtcomN 34355
[Kalmbach] p. 22Theorem 2(ii)omllaw3 34351  omlsi 28233  pjoml 28265  pjomli 28264
[Kalmbach] p. 22Definition of OML lawomllaw2N 34350
[Kalmbach] p. 23Remarkcmbr2i 28425  cmcm3 28444  cmcm3i 28423  cmcm3ii 28428  cmcm4i 28424  cmt3N 34357  cmt4N 34358  cmtbr2N 34359
[Kalmbach] p. 23Lemma 3cmbr3 28437  cmbr3i 28429  cmtbr3N 34360
[Kalmbach] p. 25Theorem 5fh1 28447  fh1i 28450  fh2 28448  fh2i 28451  omlfh1N 34364
[Kalmbach] p. 65Remarkchjatom 29186  chslej 28327  chsleji 28287  shslej 28209  shsleji 28199
[Kalmbach] p. 65Proposition 1chocin 28324  chocini 28283  chsupcl 28169  chsupval2 28239  h0elch 28082  helch 28070  hsupval2 28238  ocin 28125  ococss 28122  shococss 28123
[Kalmbach] p. 65Definition of subspace sumshsval 28141
[Kalmbach] p. 66Remarkdf-pjh 28224  pjssmi 28994  pjssmii 28510
[Kalmbach] p. 67Lemma 3osum 28474  osumi 28471
[Kalmbach] p. 67Lemma 4pjci 29029
[Kalmbach] p. 103Exercise 6atmd2 29229
[Kalmbach] p. 103Exercise 12mdsl0 29139
[Kalmbach] p. 140Remarkhatomic 29189  hatomici 29188  hatomistici 29191
[Kalmbach] p. 140Proposition 1atlatmstc 34425
[Kalmbach] p. 140Proposition 1(i)atexch 29210  lsatexch 34149
[Kalmbach] p. 140Proposition 1(ii)chcv1 29184  cvlcvr1 34445  cvr1 34515
[Kalmbach] p. 140Proposition 1(iii)cvexch 29203  cvexchi 29198  cvrexch 34525
[Kalmbach] p. 149Remark 2chrelati 29193  hlrelat 34507  hlrelat5N 34506  lrelat 34120
[Kalmbach] p. 153Exercise 5lsmcv 19122  lsmsatcv 34116  spansncv 28482  spansncvi 28481
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 34135  spansncv2 29122
[Kalmbach] p. 266Definitiondf-st 29040
[KanamoriPincus] p. 415Theorem 1.1fpwwe 9453  fpwwe2 9450
[KanamoriPincus] p. 416Corollary 1.3canth4 9454
[KanamoriPincus] p. 417Corollary 1.6canthp1 9461
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 9456
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 9458
[KanamoriPincus] p. 418Proposition 1.7pwfseq 9471
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 9475  gchxpidm 9476
[KanamoriPincus] p. 419Theorem 2.1gchacg 9487  gchhar 9486
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 9023  unxpwdom 8479
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 9477
[Kreyszig] p. 3Property M1metcl 22118  xmetcl 22117
[Kreyszig] p. 4Property M2meteq0 22125
[Kreyszig] p. 8Definition 1.1-8dscmet 22358
[Kreyszig] p. 12Equation 5conjmul 10727  muleqadd 10656
[Kreyszig] p. 18Definition 1.3-2mopnval 22224
[Kreyszig] p. 19Remarkmopntopon 22225
[Kreyszig] p. 19Theorem T1mopn0 22284  mopnm 22230
[Kreyszig] p. 19Theorem T2unimopn 22282
[Kreyszig] p. 19Definition of neighborhoodneibl 22287
[Kreyszig] p. 20Definition 1.3-3metcnp2 22328
[Kreyszig] p. 25Definition 1.4-1lmbr 21043  lmmbr 23037  lmmbr2 23038
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 21165
[Kreyszig] p. 28Theorem 1.4-5lmcau 23092
[Kreyszig] p. 28Definition 1.4-3iscau 23055  iscmet2 23073
[Kreyszig] p. 30Theorem 1.4-7cmetss 23094
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 21245  metelcls 23084
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 23085  metcld2 23086
[Kreyszig] p. 51Equation 2clmvneg1 22880  lmodvneg1 18887  nvinv 27464  vcm 27401
[Kreyszig] p. 51Equation 1aclm0vs 22876  lmod0vs 18877  slmd0vs 29751  vc0 27399
[Kreyszig] p. 51Equation 1blmodvs0 18878  slmdvs0 29752  vcz 27400
[Kreyszig] p. 58Definition 2.2-1imsmet 27516  ngpmet 22388  nrmmetd 22360
[Kreyszig] p. 59Equation 1imsdval 27511  imsdval2 27512  ncvspds 22942  ngpds 22389
[Kreyszig] p. 63Problem 1nmval 22375  nvnd 27513
[Kreyszig] p. 64Problem 2nmeq0 22403  nmge0 22402  nvge0 27498  nvz 27494
[Kreyszig] p. 64Problem 3nmrtri 22409  nvabs 27497
[Kreyszig] p. 91Definition 2.7-1isblo3i 27626
[Kreyszig] p. 92Equation 2df-nmoo 27570
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 27632  blocni 27630
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 27631
[Kreyszig] p. 129Definition 3.1-1cphipeq0 22985  ipeq0 19964  ipz 27544
[Kreyszig] p. 135Problem 2pythi 27675
[Kreyszig] p. 137Lemma 3-2.1(a)sii 27679
[Kreyszig] p. 144Equation 4supcvg 14569
[Kreyszig] p. 144Theorem 3.3-1minvec 23188  minveco 27710
[Kreyszig] p. 196Definition 3.9-1df-aj 27575
[Kreyszig] p. 247Theorem 4.7-2bcth 23107
[Kreyszig] p. 249Theorem 4.7-3ubth 27699
[Kreyszig] p. 470Definition of positive operator orderingleop 28952  leopg 28951
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 28970
[Kreyszig] p. 525Theorem 10.1-1htth 27745
[Kulpa] p. 547Theorempoimir 33413
[Kulpa] p. 547Equation (1)poimirlem32 33412
[Kulpa] p. 547Equation (2)poimirlem31 33411
[Kulpa] p. 548Theorembroucube 33414
[Kulpa] p. 548Equation (6)poimirlem26 33406
[Kulpa] p. 548Equation (7)poimirlem27 33407
[Kunen] p. 10Axiom 0ax6e 2248  axnul 4779
[Kunen] p. 11Axiom 3axnul 4779
[Kunen] p. 12Axiom 6zfrep6 7119
[Kunen] p. 24Definition 10.24mapval 7854  mapvalg 7852
[Kunen] p. 30Lemma 10.20fodom 9329
[Kunen] p. 31Definition 10.24mapex 7848
[Kunen] p. 95Definition 2.1df-r1 8612
[Kunen] p. 97Lemma 2.10r1elss 8654  r1elssi 8653
[Kunen] p. 107Exercise 4rankop 8706  rankopb 8700  rankuni 8711  rankxplim 8727  rankxpsuc 8730
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4522
[Lang] p. 3Definitiondf-mnd 17276
[Lang] p. 7Definitiondfgrp2e 17429
[Lang] p. 53Definitiondf-cat 16310
[Lang] p. 54Definitiondf-iso 16390
[Lang] p. 57Definitiondf-inito 16622  df-termo 16623
[Lang] p. 58Exampleirinitoringc 41834
[Lang] p. 58Statementinitoeu1 16642  termoeu1 16649
[Lang] p. 62Definitiondf-func 16499
[Lang] p. 65Definitiondf-nat 16584
[Lang] p. 91Notedf-ringc 41770
[Lang] p. 128Remarkdsmmlmod 20070
[Lang] p. 129Prooflincscm 41984  lincscmcl 41986  lincsum 41983  lincsumcl 41985
[Lang] p. 129Statementlincolss 41988
[Lang] p. 129Observationdsmmfi 20063
[Lang] p. 147Definitionsnlindsntor 42025
[Lang] p. 504Statementmat1 20234  matring 20230
[Lang] p. 504Definitiondf-mamu 20171
[Lang] p. 505Statementmamuass 20189  mamutpos 20245  matassa 20231  mattposvs 20242  tposmap 20244
[Lang] p. 513Definitionmdet1 20388  mdetf 20382
[Lang] p. 513Theorem 4.4cramer 20478
[Lang] p. 514Proposition 4.6mdetleib 20374
[Lang] p. 514Proposition 4.8mdettpos 20398
[Lang] p. 515Corollary 4.9mdetero 20397  mdetralt 20395
[Lang] p. 517Proposition 4.15mdetmul 20410
[Lang] p. 561Theorem 3.1cayleyhamilton 20676
[Lang], p. 561Remarkchpmatply1 20618
[Lang], p. 561Definitiondf-chpmat 20613
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 38353
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 38348
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 38354
[LeBlanc] p. 277Rule R2axnul 4779
[Levy] p. 338Axiomdf-clab 2607  df-clel 2616  df-cleq 2613
[Levy58] p. 2Definition Iisfin1-3 9193
[Levy58] p. 2Definition IIdf-fin2 9093
[Levy58] p. 2Definition IIIdf-fin3 9095
[Levy58] p. 3Definition Vdf-fin5 9096
[Levy58] p. 3Definition IVdf-fin4 9094
[Levy58] p. 4Definition VIdf-fin6 9097
[Levy58] p. 4Definition VIIdf-fin7 9098
[Levy58], p. 3Theorem 1fin1a2 9222
[Lipparini] p. 3Lemma 2.1.1nosepssdm 31810
[Lipparini] p. 3Lemma 2.1.4noresle 31820
[Lipparini] p. 6Proposition 4.2nosupbnd1 31834
[Lipparini] p. 6Proposition 4.3nosupbnd2 31836
[Lipparini] p. 7Theorem 5.1noetalem2 31838  noetalem3 31839
[Lopez-Astorga] p. 12Rule 1mptnan 1691
[Lopez-Astorga] p. 12Rule 2mptxor 1692
[Lopez-Astorga] p. 12Rule 3mtpxor 1694
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 29237
[Maeda] p. 168Lemma 5mdsym 29241  mdsymi 29240
[Maeda] p. 168Lemma 4(i)mdsymlem4 29235  mdsymlem6 29237  mdsymlem7 29238
[Maeda] p. 168Lemma 4(ii)mdsymlem8 29239
[MaedaMaeda] p. 1Remarkssdmd1 29142  ssdmd2 29143  ssmd1 29140  ssmd2 29141
[MaedaMaeda] p. 1Lemma 1.2mddmd2 29138
[MaedaMaeda] p. 1Definition 1.1df-dmd 29110  df-md 29109  mdbr 29123
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 29160  mdslj1i 29148  mdslj2i 29149  mdslle1i 29146  mdslle2i 29147  mdslmd1i 29158  mdslmd2i 29159
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 29150  mdsl2bi 29152  mdsl2i 29151
[MaedaMaeda] p. 2Lemma 1.6mdexchi 29164
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 29161
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 29162
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 29139
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 29144  mdsl3 29145
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 29163
[MaedaMaeda] p. 4Theorem 1.14mdcompli 29258
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 34427  hlrelat1 34505
[MaedaMaeda] p. 31Lemma 7.5lcvexch 34145
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 29165  cvmdi 29153  cvnbtwn4 29118  cvrnbtwn4 34385
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 29166
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 34446  cvp 29204  cvrp 34521  lcvp 34146
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 29228
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 29227
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 34439  hlexch4N 34497
[MaedaMaeda] p. 34Exercise 7.1atabsi 29230
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 34548
[MaedaMaeda] p. 61Definition 15.10psubN 34854  atpsubN 34858  df-pointsN 34607  pointpsubN 34856
[MaedaMaeda] p. 62Theorem 15.5df-pmap 34609  pmap11 34867  pmaple 34866  pmapsub 34873  pmapval 34862
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 34870  pmap1N 34872
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 34875  pmapglb2N 34876  pmapglb2xN 34877  pmapglbx 34874
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 34957
[MaedaMaeda] p. 67Postulate PS1ps-1 34582
[MaedaMaeda] p. 68Condition PS2ps-2 34583
[MaedaMaeda] p. 69Lemma 16.4ps-1 34582
[MaedaMaeda] p. 69Theorem 16.4ps-2 34583
[MaedaMaeda] p. 70Theorem 16.9lsmmod 18069  lsmmod2 18070  lssats 34118  shatomici 29187  shatomistici 29190  shmodi 28219  shmodsi 28218
[MaedaMaeda] p. 130Remark 29.6dmdmd 29129  mdsymlem7 29238
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 28418
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 28322
[MaedaMaeda] p. 139Remarksumdmdii 29244
[Margaris] p. 40Rule Cexlimiv 1856
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 386  df-ex 1703  df-or 385  dfbi2 659
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 27228
[Margaris] p. 59Section 14notnotrALTVD 38971
[Margaris] p. 60Theorem 8mth8 158
[Margaris] p. 60Section 14con3ALTVD 38972
[Margaris] p. 79Rule Cexinst01 38670  exinst11 38671
[Margaris] p. 89Theorem 19.219.2 1890  19.2g 2056  r19.2z 4051
[Margaris] p. 89Theorem 19.319.3 2067  rr19.3v 3339
[Margaris] p. 89Theorem 19.5alcom 2035
[Margaris] p. 89Theorem 19.6alex 1751
[Margaris] p. 89Theorem 19.7alnex 1704
[Margaris] p. 89Theorem 19.819.8a 2050
[Margaris] p. 89Theorem 19.919.9 2070  19.9h 2118  exlimd 2085  exlimdh 2147
[Margaris] p. 89Theorem 19.11excom 2040  excomim 2041
[Margaris] p. 89Theorem 19.1219.12 2162
[Margaris] p. 90Section 19conventions-label 27229  conventions-label 27229  conventions-label 27229  conventions-label 27229
[Margaris] p. 90Theorem 19.14exnal 1752
[Margaris] p. 90Theorem 19.152albi 38397  albi 1744
[Margaris] p. 90Theorem 19.1619.16 2091
[Margaris] p. 90Theorem 19.1719.17 2092
[Margaris] p. 90Theorem 19.182exbi 38399  exbi 1771
[Margaris] p. 90Theorem 19.1919.19 2095
[Margaris] p. 90Theorem 19.202alim 38396  2alimdv 1845  alimd 2079  alimdh 1743  alimdv 1843  ax-4 1735  ralimdaa 2955  ralimdv 2960  ralimdva 2959  ralimdvva 2961  sbcimdv 3492
[Margaris] p. 90Theorem 19.2119.21 2073  19.21h 2119  19.21t 2071  19.21vv 38395  alrimd 2082  alrimdd 2081  alrimdh 1788  alrimdv 1855  alrimi 2080  alrimih 1749  alrimiv 1853  alrimivv 1854  hbralrimi 2951  r19.21be 2930  r19.21bi 2929  ralrimd 2956  ralrimdv 2965  ralrimdva 2966  ralrimdvv 2970  ralrimdvva 2971  ralrimi 2954  ralrimia 39135  ralrimiv 2962  ralrimiva 2963  ralrimivv 2967  ralrimivva 2968  ralrimivvva 2969  ralrimivw 2964
[Margaris] p. 90Theorem 19.222exim 38398  2eximdv 1846  exim 1759  eximd 2083  eximdh 1789  eximdv 1844  rexim 3005  reximd2a 3010  reximdai 3009  reximddv 3015  reximddv2 3016  reximdv 3013  reximdv2 3011  reximdva 3014  reximdvai 3012  reximi2 3007
[Margaris] p. 90Theorem 19.2319.23 2078  19.23bi 2059  19.23h 2120  exlimdv 1859  exlimdvv 1860  exlimexi 38550  exlimiv 1856  exlimivv 1858  rexlimd3 39155  rexlimdv 3026  rexlimdv3a 3029  rexlimdva 3027  rexlimdva2 39159  rexlimdvaa 3028  rexlimdvv 3033  rexlimdvva 3034  rexlimdvw 3030  rexlimiv 3023  rexlimiva 3024  rexlimivv 3032
[Margaris] p. 90Theorem 19.2419.24 1898
[Margaris] p. 90Theorem 19.2519.25 1806
[Margaris] p. 90Theorem 19.2619.26 1796
[Margaris] p. 90Theorem 19.2719.27 2093  r19.27z 4061  r19.27zv 4062
[Margaris] p. 90Theorem 19.2819.28 2094  19.28vv 38405  r19.28z 4054  r19.28zv 4057  rr19.28v 3340
[Margaris] p. 90Theorem 19.2919.29 1799  r19.29d2r 3075  r19.29imd 3070
[Margaris] p. 90Theorem 19.3019.30 1807
[Margaris] p. 90Theorem 19.3119.31 2100  19.31vv 38403
[Margaris] p. 90Theorem 19.3219.32 2099  r19.32 40930
[Margaris] p. 90Theorem 19.3319.33-2 38401  19.33 1810
[Margaris] p. 90Theorem 19.3419.34 1899
[Margaris] p. 90Theorem 19.3519.35 1803
[Margaris] p. 90Theorem 19.3619.36 2096  19.36vv 38402  r19.36zv 4063
[Margaris] p. 90Theorem 19.3719.37 2098  19.37vv 38404  r19.37zv 4058
[Margaris] p. 90Theorem 19.3819.38 1764
[Margaris] p. 90Theorem 19.3919.39 1897
[Margaris] p. 90Theorem 19.4019.40-2 1812  19.40 1795  r19.40 3083
[Margaris] p. 90Theorem 19.4119.41 2101  19.41rg 38586
[Margaris] p. 90Theorem 19.4219.42 2103
[Margaris] p. 90Theorem 19.4319.43 1808
[Margaris] p. 90Theorem 19.4419.44 2104  r19.44zv 4060
[Margaris] p. 90Theorem 19.4519.45 2105  r19.45zv 4059
[Margaris] p. 90Theorem 1977.2319.23t 2077
[Margaris] p. 110Exercise 2(b)eu1 2508
[Mayet] p. 370Remarkjpi 29099  largei 29096  stri 29086
[Mayet3] p. 9Definition of CH-statesdf-hst 29041  ishst 29043
[Mayet3] p. 10Theoremhstrbi 29095  hstri 29094
[Mayet3] p. 1223Theorem 4.1mayete3i 28557
[Mayet3] p. 1240Theorem 7.1mayetes3i 28558
[MegPav2000] p. 2344Theorem 3.3stcltrthi 29107
[MegPav2000] p. 2345Definition 3.4-1chintcl 28161  chsupcl 28169
[MegPav2000] p. 2345Definition 3.4-2hatomic 29189
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 29183
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 29210
[MegPav2000] p. 2366Figure 7pl42N 35088
[MegPav2002] p. 362Lemma 2.2latj31 17080  latj32 17078  latjass 17076
[Megill] p. 444Axiom C5ax-5 1837  ax5ALT 34011
[Megill] p. 444Section 7conventions 27228
[Megill] p. 445Lemma L12aecom-o 34005  ax-c11n 33992  axc11n 2305
[Megill] p. 446Lemma L17equtrr 1947
[Megill] p. 446Lemma L18ax6fromc10 34000
[Megill] p. 446Lemma L19hbnae-o 34032  hbnae 2315
[Megill] p. 447Remark 9.1df-sb 1879  sbid 2112  sbidd-misc 42225  sbidd 42224
[Megill] p. 448Remark 9.6axc14 2370
[Megill] p. 448Scheme C4'ax-c4 33988
[Megill] p. 448Scheme C5'ax-c5 33987  sp 2051
[Megill] p. 448Scheme C6'ax-11 2032
[Megill] p. 448Scheme C7'ax-c7 33989
[Megill] p. 448Scheme C8'ax-7 1933
[Megill] p. 448Scheme C9'ax-c9 33994
[Megill] p. 448Scheme C10'ax-6 1886  ax-c10 33990
[Megill] p. 448Scheme C11'ax-c11 33991
[Megill] p. 448Scheme C12'ax-8 1990
[Megill] p. 448Scheme C13'ax-9 1997
[Megill] p. 448Scheme C14'ax-c14 33995
[Megill] p. 448Scheme C15'ax-c15 33993
[Megill] p. 448Scheme C16'ax-c16 33996
[Megill] p. 448Theorem 9.4dral1-o 34008  dral1 2323  dral2-o 34034  dral2 2322  drex1 2325  drex2 2326  drsb1 2375  drsb2 2376
[Megill] p. 449Theorem 9.7sbcom2 2443  sbequ 2374  sbid2v 2455
[Megill] p. 450Example in Appendixhba1-o 34001  hba1 2149
[Mendelson] p. 35Axiom A3hirstL-ax3 40822
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3511  rspsbca 3512  stdpc4 2351
[Mendelson] p. 69Axiom 5ax-c4 33988  ra4 3518  stdpc5 2074
[Mendelson] p. 81Rule Cexlimiv 1856
[Mendelson] p. 95Axiom 6stdpc6 1955
[Mendelson] p. 95Axiom 7stdpc7 1956
[Mendelson] p. 225Axiom system NBGru 3428
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4966
[Mendelson] p. 231Exercise 4.10(k)inv1 3961
[Mendelson] p. 231Exercise 4.10(l)unv 3962
[Mendelson] p. 231Exercise 4.10(n)dfin3 3858
[Mendelson] p. 231Exercise 4.10(o)df-nul 3908
[Mendelson] p. 231Exercise 4.10(q)dfin4 3859
[Mendelson] p. 231Exercise 4.10(s)ddif 3734
[Mendelson] p. 231Definition of uniondfun3 3857
[Mendelson] p. 235Exercise 4.12(c)univ 4910
[Mendelson] p. 235Exercise 4.12(d)pwv 4424
[Mendelson] p. 235Exercise 4.12(j)pwin 5008
[Mendelson] p. 235Exercise 4.12(k)pwunss 5009
[Mendelson] p. 235Exercise 4.12(l)pwssun 5010
[Mendelson] p. 235Exercise 4.12(n)uniin 4448
[Mendelson] p. 235Exercise 4.12(p)reli 5238
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5644
[Mendelson] p. 244Proposition 4.8(g)epweon 6968
[Mendelson] p. 246Definition of successordf-suc 5717
[Mendelson] p. 250Exercise 4.36oelim2 7660
[Mendelson] p. 254Proposition 4.22(b)xpen 8108
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8029  xpsneng 8030
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8036  xpcomeng 8037
[Mendelson] p. 254Proposition 4.22(e)xpassen 8039
[Mendelson] p. 255Definitionbrsdom 7963
[Mendelson] p. 255Exercise 4.39endisj 8032
[Mendelson] p. 255Exercise 4.41mapprc 7846
[Mendelson] p. 255Exercise 4.43mapsnen 8020
[Mendelson] p. 255Exercise 4.45mapunen 8114
[Mendelson] p. 255Exercise 4.47xpmapen 8113
[Mendelson] p. 255Exercise 4.42(a)map0e 7880
[Mendelson] p. 255Exercise 4.42(b)map1 8021
[Mendelson] p. 257Proposition 4.24(a)undom 8033
[Mendelson] p. 258Exercise 4.56(b)cdaen 8980
[Mendelson] p. 258Exercise 4.56(c)cdaassen 8989  cdacomen 8988
[Mendelson] p. 258Exercise 4.56(g)xp2cda 8987
[Mendelson] p. 258Definition of cardinal sumcdaval 8977  df-cda 8975
[Mendelson] p. 266Proposition 4.34(a)oa1suc 7596
[Mendelson] p. 266Proposition 4.34(f)oaordex 7623
[Mendelson] p. 275Proposition 4.42(d)entri3 9366
[Mendelson] p. 281Definitiondf-r1 8612
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 8661
[Mendelson] p. 287Axiom system MKru 3428
[MertziosUnger] p. 152Definitiondf-frgr 27101
[MertziosUnger] p. 153Remark 1frgrconngr 27138
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 27140  vdgn1frgrv3 27141
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 27142
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 27135
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 27128  2pthfrgrrn 27126  2pthfrgrrn2 27127
[Mittelstaedt] p. 9Definitiondf-oc 28079
[Monk1] p. 22Remarkconventions 27228
[Monk1] p. 22Theorem 3.1conventions 27228
[Monk1] p. 26Theorem 2.8(vii)ssin 3827
[Monk1] p. 33Theorem 3.2(i)ssrel 5197  ssrelf 29397
[Monk1] p. 33Theorem 3.2(ii)eqrel 5199
[Monk1] p. 34Definition 3.3df-opab 4704
[Monk1] p. 36Theorem 3.7(i)coi1 5639  coi2 5640
[Monk1] p. 36Theorem 3.8(v)dm0 5328  rn0 5366
[Monk1] p. 36Theorem 3.7(ii)cnvi 5525
[Monk1] p. 37Theorem 3.13(i)relxp 5217
[Monk1] p. 37Theorem 3.13(x)dmxp 5333  rnxp 5552
[Monk1] p. 37Theorem 3.13(ii)0xp 5189  xp0 5540
[Monk1] p. 38Theorem 3.16(ii)ima0 5469
[Monk1] p. 38Theorem 3.16(viii)imai 5466
[Monk1] p. 39Theorem 3.17imaex 7089  imaexg 7088
[Monk1] p. 39Theorem 3.16(xi)imassrn 5465
[Monk1] p. 41Theorem 4.3(i)fnopfv 6337  funfvop 6315
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6226
[Monk1] p. 42Theorem 4.4(iii)fvelima 6235
[Monk1] p. 43Theorem 4.6funun 5920
[Monk1] p. 43Theorem 4.8(iv)dff13 6497  dff13f 6498
[Monk1] p. 46Theorem 4.15(v)funex 6467  funrnex 7118
[Monk1] p. 50Definition 5.4fniunfv 6490
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5607
[Monk1] p. 52Theorem 5.11(viii)ssint 4484
[Monk1] p. 52Definition 5.13 (i)1stval2 7170  df-1st 7153
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7171  df-2nd 7154
[Monk1] p. 112Theorem 15.17(v)ranksn 8702  ranksnb 8675
[Monk1] p. 112Theorem 15.17(iv)rankuni2 8703
[Monk1] p. 112Theorem 15.17(iii)rankun 8704  rankunb 8698
[Monk1] p. 113Theorem 15.18r1val3 8686
[Monk1] p. 113Definition 15.19df-r1 8612  r1val2 8685
[Monk1] p. 117Lemmazorn2 9313  zorn2g 9310
[Monk1] p. 133Theorem 18.11cardom 8797
[Monk1] p. 133Theorem 18.12canth3 9368
[Monk1] p. 133Theorem 18.14carduni 8792
[Monk2] p. 105Axiom C4ax-4 1735
[Monk2] p. 105Axiom C7ax-7 1933
[Monk2] p. 105Axiom C8ax-12 2045  ax-c15 33993  ax12v2 2047
[Monk2] p. 108Lemma 5ax-c4 33988
[Monk2] p. 109Lemma 12ax-11 2032
[Monk2] p. 109Lemma 15equvini 2344  equvinv 1957  eqvinop 4945
[Monk2] p. 113Axiom C5-1ax-5 1837  ax5ALT 34011
[Monk2] p. 113Axiom C5-2ax-10 2017
[Monk2] p. 113Axiom C5-3ax-11 2032
[Monk2] p. 114Lemma 21sp 2051
[Monk2] p. 114Lemma 22axc4 2128  hba1-o 34001  hba1 2149
[Monk2] p. 114Lemma 23nfia1 2028
[Monk2] p. 114Lemma 24nfa2 2038  nfra2 2943
[Moore] p. 53Part Idf-mre 16227
[Munkres] p. 77Example 2distop 20780  indistop 20787  indistopon 20786
[Munkres] p. 77Example 3fctop 20789  fctop2 20790
[Munkres] p. 77Example 4cctop 20791
[Munkres] p. 78Definition of basisdf-bases 20731  isbasis3g 20734
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 16085  tgval2 20741
[Munkres] p. 79Remarktgcl 20754
[Munkres] p. 80Lemma 2.1tgval3 20748
[Munkres] p. 80Lemma 2.2tgss2 20772  tgss3 20771
[Munkres] p. 81Lemma 2.3basgen 20773  basgen2 20774
[Munkres] p. 83Exercise 3topdifinf 33168  topdifinfeq 33169  topdifinffin 33167  topdifinfindis 33165
[Munkres] p. 89Definition of subspace topologyresttop 20945
[Munkres] p. 93Theorem 6.1(1)0cld 20823  topcld 20820
[Munkres] p. 93Theorem 6.1(2)iincld 20824
[Munkres] p. 93Theorem 6.1(3)uncld 20826
[Munkres] p. 94Definition of closureclsval 20822
[Munkres] p. 94Definition of interiorntrval 20821
[Munkres] p. 95Theorem 6.5(a)clsndisj 20860  elcls 20858
[Munkres] p. 95Theorem 6.5(b)elcls3 20868
[Munkres] p. 97Theorem 6.6clslp 20933  neindisj 20902
[Munkres] p. 97Corollary 6.7cldlp 20935
[Munkres] p. 97Definition of limit pointislp2 20930  lpval 20924
[Munkres] p. 98Definition of Hausdorff spacedf-haus 21100
[Munkres] p. 102Definition of continuous functiondf-cn 21012  iscn 21020  iscn2 21023
[Munkres] p. 107Theorem 7.2(g)cncnp 21065  cncnp2 21066  cncnpi 21063  df-cnp 21013  iscnp 21022  iscnp2 21024
[Munkres] p. 127Theorem 10.1metcn 22329
[Munkres] p. 128Theorem 10.3metcn4 23090
[Nathanson] p. 123Remarkreprgt 30673  reprinfz1 30674  reprlt 30671
[Nathanson] p. 123Definitiondf-repr 30661
[Nathanson] p. 123Chapter 5.1circlemethnat 30693
[Nathanson] p. 123Propositionbreprexp 30685  breprexpnat 30686  itgexpif 30658
[NielsenChuang] p. 195Equation 4.73unierri 28933
[OeSilva] p. 2042Section 2ax-bgbltosilva 41463
[Pfenning] p. 17Definition XMnatded 27230
[Pfenning] p. 17Definition NNCnatded 27230  notnotrd 128
[Pfenning] p. 17Definition ` `Cnatded 27230
[Pfenning] p. 18Rule"natded 27230
[Pfenning] p. 18Definition /\Inatded 27230
[Pfenning] p. 18Definition ` `Enatded 27230  natded 27230  natded 27230  natded 27230  natded 27230
[Pfenning] p. 18Definition ` `Inatded 27230  natded 27230  natded 27230  natded 27230  natded 27230
[Pfenning] p. 18Definition ` `ELnatded 27230
[Pfenning] p. 18Definition ` `ERnatded 27230
[Pfenning] p. 18Definition ` `Ea,unatded 27230
[Pfenning] p. 18Definition ` `IRnatded 27230
[Pfenning] p. 18Definition ` `Ianatded 27230
[Pfenning] p. 127Definition =Enatded 27230
[Pfenning] p. 127Definition =Inatded 27230
[Ponnusamy] p. 361Theorem 6.44cphip0l 22983  df-dip 27526  dip0l 27543  ip0l 19962
[Ponnusamy] p. 361Equation 6.45cphipval 23023  ipval 27528
[Ponnusamy] p. 362Equation I1dipcj 27539  ipcj 19960
[Ponnusamy] p. 362Equation I3cphdir 22986  dipdir 27667  ipdir 19965  ipdiri 27655
[Ponnusamy] p. 362Equation I4ipidsq 27535  nmsq 22975
[Ponnusamy] p. 362Equation 6.46ip0i 27650
[Ponnusamy] p. 362Equation 6.47ip1i 27652
[Ponnusamy] p. 362Equation 6.48ip2i 27653
[Ponnusamy] p. 363Equation I2cphass 22992  dipass 27670  ipass 19971  ipassi 27666
[Prugovecki] p. 186Definition of brabraval 28773  df-bra 28679
[Prugovecki] p. 376Equation 8.1df-kb 28680  kbval 28783
[PtakPulmannova] p. 66Proposition 3.2.17atomli 29211
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 34993
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 29225  atcvat4i 29226  cvrat3 34547  cvrat4 34548  lsatcvat3 34158
[PtakPulmannova] p. 68Definition 3.2.18cvbr 29111  cvrval 34375  df-cv 29108  df-lcv 34125  lspsncv0 19127
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 35005
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 35006
[Quine] p. 16Definition 2.1df-clab 2607  rabid 3111
[Quine] p. 17Definition 2.1''dfsb7 2453
[Quine] p. 18Definition 2.7df-cleq 2613
[Quine] p. 19Definition 2.9conventions 27228  df-v 3197
[Quine] p. 34Theorem 5.1abeq2 2730
[Quine] p. 35Theorem 5.2abid1 2742  abid2f 2788
[Quine] p. 40Theorem 6.1sb5 2428
[Quine] p. 40Theorem 6.2sb56 2148  sb6 2427
[Quine] p. 41Theorem 6.3df-clel 2616
[Quine] p. 41Theorem 6.4eqid 2620  eqid1 27293
[Quine] p. 41Theorem 6.5eqcom 2627
[Quine] p. 42Theorem 6.6df-sbc 3430
[Quine] p. 42Theorem 6.7dfsbcq 3431  dfsbcq2 3432
[Quine] p. 43Theorem 6.8vex 3198
[Quine] p. 43Theorem 6.9isset 3202
[Quine] p. 44Theorem 7.3spcgf 3283  spcgv 3288  spcimgf 3281
[Quine] p. 44Theorem 6.11spsbc 3442  spsbcd 3443
[Quine] p. 44Theorem 6.12elex 3207
[Quine] p. 44Theorem 6.13elab 3344  elabg 3345  elabgf 3342
[Quine] p. 44Theorem 6.14noel 3911
[Quine] p. 48Theorem 7.2snprc 4244
[Quine] p. 48Definition 7.1df-pr 4171  df-sn 4169
[Quine] p. 49Theorem 7.4snss 4307  snssg 4318
[Quine] p. 49Theorem 7.6prid1 4288  prid1g 4286  prid2 4289  prid2g 4287  snid 4199  snidg 4197
[Quine] p. 51Theorem 7.12snex 4899
[Quine] p. 51Theorem 7.13prex 4900
[Quine] p. 53Theorem 8.2unisn 4442  unisnALT 38982  unisng 4443
[Quine] p. 53Theorem 8.3uniun 4447
[Quine] p. 54Theorem 8.6elssuni 4458
[Quine] p. 54Theorem 8.7uni0 4456
[Quine] p. 56Theorem 8.17uniabio 5849
[Quine] p. 56Definition 8.18dfiota2 5840
[Quine] p. 57Theorem 8.19iotaval 5850
[Quine] p. 57Theorem 8.22iotanul 5854
[Quine] p. 58Theorem 8.23iotaex 5856
[Quine] p. 58Definition 9.1df-op 4175
[Quine] p. 61Theorem 9.5opabid 4972  opelopab 4987  opelopaba 4981  opelopabaf 4989  opelopabf 4990  opelopabg 4983  opelopabga 4978  opelopabgf 4985  oprabid 6662
[Quine] p. 64Definition 9.11df-xp 5110
[Quine] p. 64Definition 9.12df-cnv 5112
[Quine] p. 64Definition 9.15df-id 5014
[Quine] p. 65Theorem 10.3fun0 5942
[Quine] p. 65Theorem 10.4funi 5908
[Quine] p. 65Theorem 10.5funsn 5927  funsng 5925
[Quine] p. 65Definition 10.1df-fun 5878
[Quine] p. 65Definition 10.2args 5481  dffv4 6175
[Quine] p. 68Definition 10.11conventions 27228  df-fv 5884  fv2 6173
[Quine] p. 124Theorem 17.3nn0opth2 13042  nn0opth2i 13041  nn0opthi 13040  omopthi 7722
[Quine] p. 177Definition 25.2df-rdg 7491
[Quine] p. 232Equation icarddom 9361
[Quine] p. 284Axiom 39(vi)funimaex 5964  funimaexg 5963
[Quine] p. 331Axiom system NFru 3428
[ReedSimon] p. 36Definition (iii)ax-his3 27911
[ReedSimon] p. 63Exercise 4(a)df-dip 27526  polid 27986  polid2i 27984  polidi 27985
[ReedSimon] p. 63Exercise 4(b)df-ph 27638
[ReedSimon] p. 195Remarklnophm 28848  lnophmi 28847
[Retherford] p. 49Exercise 1(ii)leopmul 28963  leopmuli 28962
[Retherford] p. 49Exercise 1(iv)leoptr 28966
[Retherford] p. 49Definition VI.1df-leop 28681  leoppos 28955
[Retherford] p. 49Exercise 1(iii)leoptri 28965
[Retherford] p. 49Definition of operator orderingleop3 28954
[Roman] p. 4Definitiondf-dmat 20277  df-dmatalt 41952
[Roman] p. 18Part Preliminariesdf-rng0 41640
[Roman] p. 19Part Preliminariesdf-ring 18530
[Roman] p. 46Theorem 1.6isldepslvec2 42039
[Roman] p. 112Noteisldepslvec2 42039  ldepsnlinc 42062  zlmodzxznm 42051
[Roman] p. 112Examplezlmodzxzequa 42050  zlmodzxzequap 42053  zlmodzxzldep 42058
[Roman] p. 170Theorem 7.8cayleyhamilton 20676
[Rosenlicht] p. 80Theoremheicant 33415
[Rosser] p. 281Definitiondf-op 4175
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 30697
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 30698
[Rotman] p. 28Remarkpgrpgt2nabl 41912  pmtr3ncom 17876
[Rotman] p. 31Theorem 3.4symggen2 17872
[Rotman] p. 42Theorem 3.15cayley 17815  cayleyth 17816
[Rudin] p. 164Equation 27efcan 14807
[Rudin] p. 164Equation 30efzval 14813
[Rudin] p. 167Equation 48absefi 14907
[Sanford] p. 39Remarkax-mp 5  mto 188
[Sanford] p. 39Rule 3mtpxor 1694
[Sanford] p. 39Rule 4mptxor 1692
[Sanford] p. 40Rule 1mptnan 1691
[Schechter] p. 51Definition of antisymmetryintasym 5499
[Schechter] p. 51Definition of irreflexivityintirr 5502
[Schechter] p. 51Definition of symmetrycnvsym 5498
[Schechter] p. 51Definition of transitivitycotr 5496
[Schechter] p. 78Definition of Moore collection of setsdf-mre 16227
[Schechter] p. 79Definition of Moore closuredf-mrc 16228
[Schechter] p. 82Section 4.5df-mrc 16228
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 16230
[Schechter] p. 139Definition AC3dfac9 8943
[Schechter] p. 141Definition (MC)dfac11 37451
[Schechter] p. 149Axiom DC1ax-dc 9253  axdc3 9261
[Schechter] p. 187Definition of ring with unitisring 18532  isrngo 33667
[Schechter] p. 276Remark 11.6.espan0 28371
[Schechter] p. 276Definition of spandf-span 28138  spanval 28162
[Schechter] p. 428Definition 15.35bastop1 20778
[Schwabhauser] p. 10Axiom A1axcgrrflx 25775  axtgcgrrflx 25342
[Schwabhauser] p. 10Axiom A2axcgrtr 25776
[Schwabhauser] p. 10Axiom A3axcgrid 25777  axtgcgrid 25343
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 25328
[Schwabhauser] p. 11Axiom A4axsegcon 25788  axtgsegcon 25344  df-trkgcb 25330
[Schwabhauser] p. 11Axiom A5ax5seg 25799  axtg5seg 25345  df-trkgcb 25330
[Schwabhauser] p. 11Axiom A6axbtwnid 25800  axtgbtwnid 25346  df-trkgb 25329
[Schwabhauser] p. 12Axiom A7axpasch 25802  axtgpasch 25347  df-trkgb 25329
[Schwabhauser] p. 12Axiom A8axlowdim2 25821  df-trkg2d 30717
[Schwabhauser] p. 13Axiom A8axtglowdim2 25350
[Schwabhauser] p. 13Axiom A9axtgupdim2 25351  df-trkg2d 30717
[Schwabhauser] p. 13Axiom A10axeuclid 25824  axtgeucl 25352  df-trkge 25331
[Schwabhauser] p. 13Axiom A11axcont 25837  axtgcont 25349  axtgcont1 25348  df-trkgb 25329
[Schwabhauser] p. 27Theorem 2.1cgrrflx 32069
[Schwabhauser] p. 27Theorem 2.2cgrcomim 32071
[Schwabhauser] p. 27Theorem 2.3cgrtr 32074
[Schwabhauser] p. 27Theorem 2.4cgrcoml 32078
[Schwabhauser] p. 27Theorem 2.5cgrcomr 32079  tgcgrcomimp 25353  tgcgrcoml 25355  tgcgrcomr 25354
[Schwabhauser] p. 28Theorem 2.8cgrtriv 32084  tgcgrtriv 25360
[Schwabhauser] p. 28Theorem 2.105segofs 32088  tg5segofs 30725
[Schwabhauser] p. 28Definition 2.10df-afs 30722  df-ofs 32065
[Schwabhauser] p. 29Theorem 2.11cgrextend 32090  tgcgrextend 25361
[Schwabhauser] p. 29Theorem 2.12segconeq 32092  tgsegconeq 25362
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 32104  btwntriv2 32094  tgbtwntriv2 25363
[Schwabhauser] p. 30Theorem 3.2btwncomim 32095  tgbtwncom 25364
[Schwabhauser] p. 30Theorem 3.3btwntriv1 32098  tgbtwntriv1 25367
[Schwabhauser] p. 30Theorem 3.4btwnswapid 32099  tgbtwnswapid 25368
[Schwabhauser] p. 30Theorem 3.5btwnexch2 32105  btwnintr 32101  tgbtwnexch2 25372  tgbtwnintr 25369
[Schwabhauser] p. 30Theorem 3.6btwnexch 32107  btwnexch3 32102  tgbtwnexch 25374  tgbtwnexch3 25370
[Schwabhauser] p. 30Theorem 3.7btwnouttr 32106  tgbtwnouttr 25373  tgbtwnouttr2 25371
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25820
[Schwabhauser] p. 32Theorem 3.14btwndiff 32109  tgbtwndiff 25382
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 25375  trisegint 32110
[Schwabhauser] p. 34Theorem 4.2ifscgr 32126  tgifscgr 25384
[Schwabhauser] p. 34Theorem 4.11colcom 25434  colrot1 25435  colrot2 25436  lncom 25498  lnrot1 25499  lnrot2 25500
[Schwabhauser] p. 34Definition 4.1df-ifs 32122
[Schwabhauser] p. 35Theorem 4.3cgrsub 32127  tgcgrsub 25385
[Schwabhauser] p. 35Theorem 4.5cgrxfr 32137  tgcgrxfr 25394
[Schwabhauser] p. 35Statement 4.4ercgrg 25393
[Schwabhauser] p. 35Definition 4.4df-cgr3 32123  df-cgrg 25387
[Schwabhauser] p. 36Theorem 4.6btwnxfr 32138  tgbtwnxfr 25406
[Schwabhauser] p. 36Theorem 4.11colinearperm1 32144  colinearperm2 32146  colinearperm3 32145  colinearperm4 32147  colinearperm5 32148
[Schwabhauser] p. 36Definition 4.8df-ismt 25409
[Schwabhauser] p. 36Definition 4.10df-colinear 32121  tgellng 25429  tglng 25422
[Schwabhauser] p. 37Theorem 4.12colineartriv1 32149
[Schwabhauser] p. 37Theorem 4.13colinearxfr 32157  lnxfr 25442
[Schwabhauser] p. 37Theorem 4.14lineext 32158  lnext 25443
[Schwabhauser] p. 37Theorem 4.16fscgr 32162  tgfscgr 25444
[Schwabhauser] p. 37Theorem 4.17linecgr 32163  lncgr 25445
[Schwabhauser] p. 37Definition 4.15df-fs 32124
[Schwabhauser] p. 38Theorem 4.18lineid 32165  lnid 25446
[Schwabhauser] p. 38Theorem 4.19idinside 32166  tgidinside 25447
[Schwabhauser] p. 39Theorem 5.1btwnconn1 32183  tgbtwnconn1 25451
[Schwabhauser] p. 41Theorem 5.2btwnconn2 32184  tgbtwnconn2 25452
[Schwabhauser] p. 41Theorem 5.3btwnconn3 32185  tgbtwnconn3 25453
[Schwabhauser] p. 41Theorem 5.5brsegle2 32191
[Schwabhauser] p. 41Definition 5.4df-segle 32189  legov 25461
[Schwabhauser] p. 41Definition 5.5legov2 25462
[Schwabhauser] p. 42Remark 5.13legso 25475
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 32192
[Schwabhauser] p. 42Theorem 5.7seglerflx 32194
[Schwabhauser] p. 42Theorem 5.8segletr 32196
[Schwabhauser] p. 42Theorem 5.9segleantisym 32197
[Schwabhauser] p. 42Theorem 5.10seglelin 32198
[Schwabhauser] p. 42Theorem 5.11seglemin 32195
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 32200
[Schwabhauser] p. 42Proposition 5.7legid 25463
[Schwabhauser] p. 42Proposition 5.8legtrd 25465
[Schwabhauser] p. 42Proposition 5.9legtri3 25466
[Schwabhauser] p. 42Proposition 5.10legtrid 25467
[Schwabhauser] p. 42Proposition 5.11leg0 25468
[Schwabhauser] p. 43Theorem 6.2btwnoutside 32207
[Schwabhauser] p. 43Theorem 6.3broutsideof3 32208
[Schwabhauser] p. 43Theorem 6.4broutsideof 32203  df-outsideof 32202
[Schwabhauser] p. 43Definition 6.1broutsideof2 32204  ishlg 25478
[Schwabhauser] p. 44Theorem 6.4hlln 25483
[Schwabhauser] p. 44Theorem 6.5hlid 25485  outsideofrflx 32209
[Schwabhauser] p. 44Theorem 6.6hlcomb 25479  hlcomd 25480  outsideofcom 32210
[Schwabhauser] p. 44Theorem 6.7hltr 25486  outsideoftr 32211
[Schwabhauser] p. 44Theorem 6.11hlcgreu 25494  outsideofeu 32213
[Schwabhauser] p. 44Definition 6.8df-ray 32220
[Schwabhauser] p. 45Part 2df-lines2 32221
[Schwabhauser] p. 45Theorem 6.13outsidele 32214
[Schwabhauser] p. 45Theorem 6.15lineunray 32229
[Schwabhauser] p. 45Theorem 6.16lineelsb2 32230  tglineelsb2 25508
[Schwabhauser] p. 45Theorem 6.17linecom 32232  linerflx1 32231  linerflx2 32233  tglinecom 25511  tglinerflx1 25509  tglinerflx2 25510
[Schwabhauser] p. 45Theorem 6.18linethru 32235  tglinethru 25512
[Schwabhauser] p. 45Definition 6.14df-line2 32219  tglng 25422
[Schwabhauser] p. 45Proposition 6.13legbtwn 25470
[Schwabhauser] p. 46Theorem 6.19linethrueu 32238  tglinethrueu 25515
[Schwabhauser] p. 46Theorem 6.21lineintmo 32239  tglineineq 25519  tglineinteq 25521  tglineintmo 25518
[Schwabhauser] p. 46Theorem 6.23colline 25525
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 25526
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 25527
[Schwabhauser] p. 49Theorem 7.3mirinv 25542
[Schwabhauser] p. 49Theorem 7.7mirmir 25538
[Schwabhauser] p. 49Theorem 7.8mirreu3 25530
[Schwabhauser] p. 49Definition 7.5df-mir 25529  ismir 25535  mirbtwn 25534  mircgr 25533  mirfv 25532  mirval 25531
[Schwabhauser] p. 50Theorem 7.8mirreu 25540
[Schwabhauser] p. 50Theorem 7.9mireq 25541
[Schwabhauser] p. 50Theorem 7.10mirinv 25542
[Schwabhauser] p. 50Theorem 7.11mirf1o 25545
[Schwabhauser] p. 50Theorem 7.13miriso 25546
[Schwabhauser] p. 51Theorem 7.14mirmot 25551
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 25548  mirbtwni 25547
[Schwabhauser] p. 51Theorem 7.16mircgrs 25549
[Schwabhauser] p. 51Theorem 7.17miduniq 25561
[Schwabhauser] p. 52Theorem 7.18miduniq1 25562
[Schwabhauser] p. 52Theorem 7.19miduniq2 25563
[Schwabhauser] p. 52Theorem 7.20colmid 25564
[Schwabhauser] p. 53Lemma 7.22krippen 25567
[Schwabhauser] p. 55Lemma 7.25midexlem 25568
[Schwabhauser] p. 57Theorem 8.2ragcom 25574
[Schwabhauser] p. 57Definition 8.1df-rag 25570  israg 25573
[Schwabhauser] p. 58Theorem 8.3ragcol 25575
[Schwabhauser] p. 58Theorem 8.4ragmir 25576
[Schwabhauser] p. 58Theorem 8.5ragtrivb 25578
[Schwabhauser] p. 58Theorem 8.6ragflat2 25579
[Schwabhauser] p. 58Theorem 8.7ragflat 25580
[Schwabhauser] p. 58Theorem 8.8ragtriva 25581
[Schwabhauser] p. 58Theorem 8.9ragflat3 25582  ragncol 25585
[Schwabhauser] p. 58Theorem 8.10ragcgr 25583
[Schwabhauser] p. 59Theorem 8.12perpcom 25589
[Schwabhauser] p. 59Theorem 8.13ragperp 25593
[Schwabhauser] p. 59Theorem 8.14perpneq 25590
[Schwabhauser] p. 59Definition 8.11df-perpg 25572  isperp 25588
[Schwabhauser] p. 59Definition 8.13isperp2 25591
[Schwabhauser] p. 60Theorem 8.18foot 25595
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 25603  colperpexlem2 25604
[Schwabhauser] p. 63Theorem 8.21colperpex 25606  colperpexlem3 25605
[Schwabhauser] p. 64Theorem 8.22mideu 25611  midex 25610
[Schwabhauser] p. 66Lemma 8.24opphllem 25608
[Schwabhauser] p. 67Theorem 9.2oppcom 25617
[Schwabhauser] p. 67Definition 9.1islnopp 25612
[Schwabhauser] p. 68Lemma 9.3opphllem2 25621
[Schwabhauser] p. 68Lemma 9.4opphllem5 25624  opphllem6 25625
[Schwabhauser] p. 69Theorem 9.5opphl 25627
[Schwabhauser] p. 69Theorem 9.6axtgpasch 25347
[Schwabhauser] p. 70Theorem 9.6outpasch 25628
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 25636
[Schwabhauser] p. 71Definition 9.7df-hpg 25631  hpgbr 25633
[Schwabhauser] p. 72Lemma 9.10hpgerlem 25638
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 25637
[Schwabhauser] p. 72Theorem 9.11hpgid 25639
[Schwabhauser] p. 72Theorem 9.12hpgcom 25640
[Schwabhauser] p. 72Theorem 9.13hpgtr 25641
[Schwabhauser] p. 73Theorem 9.18colopp 25642
[Schwabhauser] p. 73Theorem 9.19colhp 25643
[Schwabhauser] p. 88Theorem 10.2lmieu 25657
[Schwabhauser] p. 88Definition 10.1df-mid 25647
[Schwabhauser] p. 89Theorem 10.4lmicom 25661
[Schwabhauser] p. 89Theorem 10.5lmilmi 25662
[Schwabhauser] p. 89Theorem 10.6lmireu 25663
[Schwabhauser] p. 89Theorem 10.7lmieq 25664
[Schwabhauser] p. 89Theorem 10.8lmiinv 25665
[Schwabhauser] p. 89Theorem 10.9lmif1o 25668
[Schwabhauser] p. 89Theorem 10.10lmiiso 25670
[Schwabhauser] p. 89Definition 10.3df-lmi 25648
[Schwabhauser] p. 90Theorem 10.11lmimot 25671
[Schwabhauser] p. 91Theorem 10.12hypcgr 25674
[Schwabhauser] p. 92Theorem 10.14lmiopp 25675
[Schwabhauser] p. 92Theorem 10.15lnperpex 25676
[Schwabhauser] p. 92Theorem 10.16trgcopy 25677  trgcopyeu 25679
[Schwabhauser] p. 95Definition 11.2dfcgra2 25702
[Schwabhauser] p. 95Definition 11.3iscgra 25682
[Schwabhauser] p. 95Proposition 11.4cgracgr 25691
[Schwabhauser] p. 95Proposition 11.10cgrahl1 25689  cgrahl2 25690
[Schwabhauser] p. 96Theorem 11.6cgraid 25692
[Schwabhauser] p. 96Theorem 11.9cgraswap 25693
[Schwabhauser] p. 97Theorem 11.7cgracom 25695
[Schwabhauser] p. 97Theorem 11.8cgratr 25696
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 25698  cgrahl 25699
[Schwabhauser] p. 98Theorem 11.13sacgr 25703
[Schwabhauser] p. 98Theorem 11.14oacgr 25704
[Schwabhauser] p. 98Theorem 11.15acopy 25705  acopyeu 25706
[Schwabhauser] p. 101Theorem 11.24inagswap 25711
[Schwabhauser] p. 101Theorem 11.25inaghl 25712
[Schwabhauser] p. 101Property for point ` ` to lie in the angle ` ` Defnition 11.23isinag 25710
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 25715
[Schwabhauser] p. 102Definition 11.27df-leag 25713  isleag 25714
[Schwabhauser] p. 107Theorem 11.49tgsas 25717  tgsas1 25716  tgsas2 25718  tgsas3 25719
[Schwabhauser] p. 108Theorem 11.50tgasa 25721  tgasa1 25720
[Schwabhauser] p. 109Theorem 11.51tgsss1 25722  tgsss2 25723  tgsss3 25724
[Shapiro] p. 230Theorem 6.5.1dchrhash 24977  dchrsum 24975  dchrsum2 24974  sumdchr 24978
[Shapiro] p. 232Theorem 6.5.2dchr2sum 24979  sum2dchr 24980
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 18446  ablfacrp2 18447
[Shapiro], p. 328Equation 9.2.4vmasum 24922
[Shapiro], p. 329Equation 9.2.7logfac2 24923
[Shapiro], p. 329Equation 9.2.9logfacrlim 24930
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 25155
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 25209  vmalogdivsum2 25208
[Shapiro], p. 375Theorem 9.4.1dirith 25199  dirith2 25198
[Shapiro], p. 375Equation 9.4.3rplogsum 25197  rpvmasum 25196  rpvmasum2 25182
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 25157
[Shapiro], p. 376Equation 9.4.8dchrvmasum 25195
[Shapiro], p. 377Lemma 9.4.1dchrisum 25162  dchrisumlem1 25159  dchrisumlem2 25160  dchrisumlem3 25161  dchrisumlema 25158
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 25165
[Shapiro], p. 379Equation 9.4.16dchrmusum 25194  dchrmusumlem 25192  dchrvmasumlem 25193
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 25164
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 25166
[Shapiro], p. 382Lemma 9.4.4dchrisum0 25190  dchrisum0re 25183  dchrisumn0 25191
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 25176
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 25180
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 25181
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 25236  pntrsumbnd2 25237  pntrsumo1 25235
[Shapiro], p. 405Equation 10.2.1mudivsum 25200
[Shapiro], p. 406Equation 10.2.6mulogsum 25202
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 25204
[Shapiro], p. 407Equation 10.2.8mulog2sum 25207
[Shapiro], p. 418Equation 10.4.6logsqvma 25212
[Shapiro], p. 418Equation 10.4.8logsqvma2 25213
[Shapiro], p. 419Equation 10.4.10selberg 25218
[Shapiro], p. 420Equation 10.4.12selberg2lem 25220
[Shapiro], p. 420Equation 10.4.14selberg2 25221
[Shapiro], p. 422Equation 10.6.7selberg3 25229
[Shapiro], p. 422Equation 10.4.20selberg4lem1 25230
[Shapiro], p. 422Equation 10.4.21selberg3lem1 25227  selberg3lem2 25228
[Shapiro], p. 422Equation 10.4.23selberg4 25231
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 25225
[Shapiro], p. 428Equation 10.6.2selbergr 25238
[Shapiro], p. 429Equation 10.6.8selberg3r 25239
[Shapiro], p. 430Equation 10.6.11selberg4r 25240
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 25254
[Shapiro], p. 434Equation 10.6.27pntlema 25266  pntlemb 25267  pntlemc 25265  pntlemd 25264  pntlemg 25268
[Shapiro], p. 435Equation 10.6.29pntlema 25266
[Shapiro], p. 436Lemma 10.6.1pntpbnd 25258
[Shapiro], p. 436Lemma 10.6.2pntibnd 25263
[Shapiro], p. 436Equation 10.6.34pntlema 25266
[Shapiro], p. 436Equation 10.6.35pntlem3 25279  pntleml 25281
[Stoll] p. 13Definition corresponds to dfsymdif3 3885
[Stoll] p. 16Exercise 4.40dif 3968  dif0 3941
[Stoll] p. 16Exercise 4.8difdifdir 4047
[Stoll] p. 17Theorem 5.1(5)unvdif 4033
[Stoll] p. 19Theorem 5.2(13)undm 3877
[Stoll] p. 19Theorem 5.2(13')indm 3878
[Stoll] p. 20Remarkinvdif 3860
[Stoll] p. 25Definition of ordered tripledf-ot 4177
[Stoll] p. 43Definitionuniiun 4564
[Stoll] p. 44Definitionintiin 4565
[Stoll] p. 45Definitiondf-iin 4514
[Stoll] p. 45Definition indexed uniondf-iun 4513
[Stoll] p. 176Theorem 3.4(27)iman 440
[Stoll] p. 262Example 4.1dfsymdif3 3885
[Strang] p. 242Section 6.3expgrowth 38354
[Suppes] p. 22Theorem 2eq0 3921  eq0f 3917
[Suppes] p. 22Theorem 4eqss 3610  eqssd 3612  eqssi 3611
[Suppes] p. 23Theorem 5ss0 3965  ss0b 3964
[Suppes] p. 23Theorem 6sstr 3603  sstrALT2 38890
[Suppes] p. 23Theorem 7pssirr 3699
[Suppes] p. 23Theorem 8pssn2lp 3700
[Suppes] p. 23Theorem 9psstr 3703
[Suppes] p. 23Theorem 10pssss 3694
[Suppes] p. 25Theorem 12elin 3788  elun 3745
[Suppes] p. 26Theorem 15inidm 3814
[Suppes] p. 26Theorem 16in0 3959
[Suppes] p. 27Theorem 23unidm 3748
[Suppes] p. 27Theorem 24un0 3958
[Suppes] p. 27Theorem 25ssun1 3768
[Suppes] p. 27Theorem 26ssequn1 3775
[Suppes] p. 27Theorem 27unss 3779
[Suppes] p. 27Theorem 28indir 3867
[Suppes] p. 27Theorem 29undir 3868
[Suppes] p. 28Theorem 32difid 3939
[Suppes] p. 29Theorem 33difin 3853
[Suppes] p. 29Theorem 34indif 3861
[Suppes] p. 29Theorem 35undif1 4034
[Suppes] p. 29Theorem 36difun2 4039
[Suppes] p. 29Theorem 37difin0 4032
[Suppes] p. 29Theorem 38disjdif 4031
[Suppes] p. 29Theorem 39difundi 3871
[Suppes] p. 29Theorem 40difindi 3873
[Suppes] p. 30Theorem 41nalset 4786
[Suppes] p. 39Theorem 61uniss 4449
[Suppes] p. 39Theorem 65uniop 4967
[Suppes] p. 41Theorem 70intsn 4504
[Suppes] p. 42Theorem 71intpr 4501  intprg 4502
[Suppes] p. 42Theorem 73op1stb 4931
[Suppes] p. 42Theorem 78intun 4500
[Suppes] p. 44Definition 15(a)dfiun2 4545  dfiun2g 4543
[Suppes] p. 44Definition 15(b)dfiin2 4546
[Suppes] p. 47Theorem 86elpw 4155  elpw2 4819  elpw2g 4818  elpwg 4157  elpwgdedVD 38973
[Suppes] p. 47Theorem 87pwid 4165
[Suppes] p. 47Theorem 89pw0 4334
[Suppes] p. 48Theorem 90pwpw0 4335
[Suppes] p. 52Theorem 101xpss12 5215
[Suppes] p. 52Theorem 102xpindi 5244  xpindir 5245
[Suppes] p. 52Theorem 103xpundi 5161  xpundir 5162
[Suppes] p. 54Theorem 105elirrv 8489
[Suppes] p. 58Theorem 2relss 5196
[Suppes] p. 59Theorem 4eldm 5310  eldm2 5311  eldm2g 5309  eldmg 5308
[Suppes] p. 59Definition 3df-dm 5114
[Suppes] p. 60Theorem 6dmin 5321
[Suppes] p. 60Theorem 8rnun 5529
[Suppes] p. 60Theorem 9rnin 5530
[Suppes] p. 60Definition 4dfrn2 5300
[Suppes] p. 61Theorem 11brcnv 5294  brcnvg 5292
[Suppes] p. 62Equation 5elcnv 5288  elcnv2 5289
[Suppes] p. 62Theorem 12relcnv 5491
[Suppes] p. 62Theorem 15cnvin 5528
[Suppes] p. 62Theorem 16cnvun 5526
[Suppes] p. 63Theorem 20co02 5637
[Suppes] p. 63Theorem 21dmcoss 5374
[Suppes] p. 63Definition 7df-co 5113
[Suppes] p. 64Theorem 26cnvco 5297
[Suppes] p. 64Theorem 27coass 5642
[Suppes] p. 65Theorem 31resundi 5398
[Suppes] p. 65Theorem 34elima 5459  elima2 5460  elima3 5461  elimag 5458
[Suppes] p. 65Theorem 35imaundi 5533
[Suppes] p. 66Theorem 40dminss 5535
[Suppes] p. 66Theorem 41imainss 5536
[Suppes] p. 67Exercise 11cnvxp 5539
[Suppes] p. 81Definition 34dfec2 7730
[Suppes] p. 82Theorem 72elec 7771  elecg 7770
[Suppes] p. 82Theorem 73erth 7776  erth2 7777
[Suppes] p. 83Theorem 74erdisj 7779
[Suppes] p. 89Theorem 96map0b 7881
[Suppes] p. 89Theorem 97map0 7883  map0g 7882
[Suppes] p. 89Theorem 98mapsn 7884
[Suppes] p. 89Theorem 99mapss 7885
[Suppes] p. 91Definition 12(ii)alephsuc 8876
[Suppes] p. 91Definition 12(iii)alephlim 8875
[Suppes] p. 92Theorem 1enref 7973  enrefg 7972
[Suppes] p. 92Theorem 2ensym 7990  ensymb 7989  ensymi 7991
[Suppes] p. 92Theorem 3entr 7993
[Suppes] p. 92Theorem 4unen 8025
[Suppes] p. 94Theorem 15endom 7967
[Suppes] p. 94Theorem 16ssdomg 7986
[Suppes] p. 94Theorem 17domtr 7994
[Suppes] p. 95Theorem 18sbth 8065
[Suppes] p. 97Theorem 23canth2 8098  canth2g 8099
[Suppes] p. 97Definition 3brsdom2 8069  df-sdom 7943  dfsdom2 8068
[Suppes] p. 97Theorem 21(i)sdomirr 8082
[Suppes] p. 97Theorem 22(i)domnsym 8071
[Suppes] p. 97Theorem 21(ii)sdomnsym 8070
[Suppes] p. 97Theorem 22(ii)domsdomtr 8080
[Suppes] p. 97Theorem 22(iv)brdom2 7970
[Suppes] p. 97Theorem 21(iii)sdomtr 8083
[Suppes] p. 97Theorem 22(iii)sdomdomtr 8078
[Suppes] p. 98Exercise 4fundmen 8015  fundmeng 8016
[Suppes] p. 98Exercise 6xpdom3 8043
[Suppes] p. 98Exercise 11sdomentr 8079
[Suppes] p. 104Theorem 37fofi 8237
[Suppes] p. 104Theorem 38pwfi 8246
[Suppes] p. 105Theorem 40pwfi 8246
[Suppes] p. 111Axiom for cardinal numberscarden 9358
[Suppes] p. 130Definition 3df-tr 4744
[Suppes] p. 132Theorem 9ssonuni 6971
[Suppes] p. 134Definition 6df-suc 5717
[Suppes] p. 136Theorem Schema 22findes 7081  finds 7077  finds1 7080  finds2 7079
[Suppes] p. 151Theorem 42isfinite 8534  isfinite2 8203  isfiniteg 8205  unbnn 8201
[Suppes] p. 162Definition 5df-ltnq 9725  df-ltpq 9717
[Suppes] p. 197Theorem Schema 4tfindes 7047  tfinds 7044  tfinds2 7048
[Suppes] p. 209Theorem 18oaord1 7616
[Suppes] p. 209Theorem 21oaword2 7618
[Suppes] p. 211Theorem 25oaass 7626
[Suppes] p. 225Definition 8iscard2 8787
[Suppes] p. 227Theorem 56ondomon 9370
[Suppes] p. 228Theorem 59harcard 8789
[Suppes] p. 228Definition 12(i)aleph0 8874
[Suppes] p. 228Theorem Schema 61onintss 5763
[Suppes] p. 228Theorem Schema 62onminesb 6983  onminsb 6984
[Suppes] p. 229Theorem 64alephval2 9379
[Suppes] p. 229Theorem 65alephcard 8878
[Suppes] p. 229Theorem 66alephord2i 8885
[Suppes] p. 229Theorem 67alephnbtwn 8879
[Suppes] p. 229Definition 12df-aleph 8751
[Suppes] p. 242Theorem 6weth 9302
[Suppes] p. 242Theorem 8entric 9364
[Suppes] p. 242Theorem 9carden 9358
[TakeutiZaring] p. 8Axiom 1ax-ext 2600
[TakeutiZaring] p. 13Definition 4.5df-cleq 2613
[TakeutiZaring] p. 13Proposition 4.6df-clel 2616
[TakeutiZaring] p. 13Proposition 4.9cvjust 2615
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2639
[TakeutiZaring] p. 14Definition 4.16df-oprab 6639
[TakeutiZaring] p. 14Proposition 4.14ru 3428
[TakeutiZaring] p. 15Axiom 2zfpair 4895
[TakeutiZaring] p. 15Exercise 1elpr 4189  elpr2 4190  elprg 4187
[TakeutiZaring] p. 15Exercise 2elsn 4183  elsn2 4202  elsn2g 4201  elsng 4182  velsn 4184
[TakeutiZaring] p. 15Exercise 3elop 4926
[TakeutiZaring] p. 15Exercise 4sneq 4178  sneqr 4362
[TakeutiZaring] p. 15Definition 5.1dfpr2 4186  dfsn2 4181
[TakeutiZaring] p. 16Axiom 3uniex 6938
[TakeutiZaring] p. 16Exercise 6opth 4935
[TakeutiZaring] p. 16Exercise 7opex 4923
[TakeutiZaring] p. 16Exercise 8rext 4907
[TakeutiZaring] p. 16Corollary 5.8unex 6941  unexg 6944
[TakeutiZaring] p. 16Definition 5.3dftp2 4222
[TakeutiZaring] p. 16Definition 5.5df-uni 4428
[TakeutiZaring] p. 16Definition 5.6df-in 3574  df-un 3572
[TakeutiZaring] p. 16Proposition 5.7unipr 4440  uniprg 4441
[TakeutiZaring] p. 17Axiom 4pwex 4839  pwexg 4841
[TakeutiZaring] p. 17Exercise 1eltp 4221
[TakeutiZaring] p. 17Exercise 5elsuc 5782  elsucg 5780  sstr2 3602
[TakeutiZaring] p. 17Exercise 6uncom 3749
[TakeutiZaring] p. 17Exercise 7incom 3797
[TakeutiZaring] p. 17Exercise 8unass 3762
[TakeutiZaring] p. 17Exercise 9inass 3815
[TakeutiZaring] p. 17Exercise 10indi 3865
[TakeutiZaring] p. 17Exercise 11undi 3866
[TakeutiZaring] p. 17Definition 5.9df-pss 3583  dfss2 3584
[TakeutiZaring] p. 17Definition 5.10df-pw 4151
[TakeutiZaring] p. 18Exercise 7unss2 3776
[TakeutiZaring] p. 18Exercise 9df-ss 3581  sseqin2 3809
[TakeutiZaring] p. 18Exercise 10ssid 3616
[TakeutiZaring] p. 18Exercise 12inss1 3825  inss2 3826
[TakeutiZaring] p. 18Exercise 13nss 3655
[TakeutiZaring] p. 18Exercise 15unieq 4435
[TakeutiZaring] p. 18Exercise 18sspwb 4908  sspwimp 38974  sspwimpALT 38981  sspwimpALT2 38984  sspwimpcf 38976
[TakeutiZaring] p. 18Exercise 19pweqb 4916
[TakeutiZaring] p. 19Axiom 5ax-rep 4762
[TakeutiZaring] p. 20Definitiondf-rab 2918
[TakeutiZaring] p. 20Corollary 5.160ex 4781
[TakeutiZaring] p. 20Definition 5.12df-dif 3570
[TakeutiZaring] p. 20Definition 5.14dfnul2 3909
[TakeutiZaring] p. 20Proposition 5.15difid 3939
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3923  n0f 3919  neq0 3922  neq0f 3918
[TakeutiZaring] p. 21Axiom 6zfreg 8485
[TakeutiZaring] p. 21Axiom 6'zfregs 8593
[TakeutiZaring] p. 21Theorem 5.22setind 8595
[TakeutiZaring] p. 21Definition 5.20df-v 3197
[TakeutiZaring] p. 21Proposition 5.21vprc 4787
[TakeutiZaring] p. 22Exercise 10ss 3963
[TakeutiZaring] p. 22Exercise 3ssex 4793  ssexg 4795
[TakeutiZaring] p. 22Exercise 4inex1 4790
[TakeutiZaring] p. 22Exercise 5ruv 8492
[TakeutiZaring] p. 22Exercise 6elirr 8490
[TakeutiZaring] p. 22Exercise 7ssdif0 3933
[TakeutiZaring] p. 22Exercise 11difdif 3728
[TakeutiZaring] p. 22Exercise 13undif3 3880  undif3VD 38938
[TakeutiZaring] p. 22Exercise 14difss 3729
[TakeutiZaring] p. 22Exercise 15sscon 3736
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2914
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2915
[TakeutiZaring] p. 23Proposition 6.2xpex 6947  xpexg 6945
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5111
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5948
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6096  fun11 5951
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5888  svrelfun 5949
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5299
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5301
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5116
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5117
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5113
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5577  dfrel2 5571
[TakeutiZaring] p. 25Exercise 3xpss 5216
[TakeutiZaring] p. 25Exercise 5relun 5225
[TakeutiZaring] p. 25Exercise 6reluni 5231
[TakeutiZaring] p. 25Exercise 9inxp 5243
[TakeutiZaring] p. 25Exercise 12relres 5414
[TakeutiZaring] p. 25Exercise 13opelres 5390  opelresg 5392
[TakeutiZaring] p. 25Exercise 14dmres 5407
[TakeutiZaring] p. 25Exercise 15resss 5410
[TakeutiZaring] p. 25Exercise 17resabs1 5415
[TakeutiZaring] p. 25Exercise 18funres 5917
[TakeutiZaring] p. 25Exercise 24relco 5621
[TakeutiZaring] p. 25Exercise 29funco 5916
[TakeutiZaring] p. 25Exercise 30f1co 6097
[TakeutiZaring] p. 26Definition 6.10eu2 2507
[TakeutiZaring] p. 26Definition 6.11conventions 27228  df-fv 5884  fv3 6193
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7098  cnvexg 7097
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7084  dmexg 7082
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7085  rnexg 7083
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 38478
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7093
[TakeutiZaring] p. 27Corollary 6.13fvex 6188
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 41017  tz6.12-1 6197  tz6.12-afv 41016  tz6.12 6198  tz6.12c 6200
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 6169  tz6.12i 6201
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5879
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5880
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5882  wfo 5874
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5881  wf1 5873
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5883  wf1o 5875
[TakeutiZaring] p. 28Exercise 4eqfnfv 6297  eqfnfv2 6298  eqfnfv2f 6301
[TakeutiZaring] p. 28Exercise 5fvco 6261
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 6466
[TakeutiZaring] p. 28Proposition 6.17resfunexg 6464
[TakeutiZaring] p. 29Exercise 9funimaex 5964  funimaexg 5963
[TakeutiZaring] p. 29Definition 6.18df-br 4645
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5026
[TakeutiZaring] p. 30Definition 6.21dffr2 5069  dffr3 5486  eliniseg 5482  iniseg 5484
[TakeutiZaring] p. 30Definition 6.22df-eprel 5019
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5082  fr3nr 6964  frirr 5081
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5063
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 6966
[TakeutiZaring] p. 31Exercise 4wess 5091
[TakeutiZaring] p. 31Proposition 6.26tz6.26 5699  tz6.26i 5700  wefrc 5098  wereu2 5101
[TakeutiZaring] p. 32Theorem 6.27wfi 5701  wfii 5702
[TakeutiZaring] p. 32Definition 6.28df-isom 5885
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6564
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6565
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6571
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6572
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6573
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6577
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6584
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6586
[TakeutiZaring] p. 35Notationwtr 4743
[TakeutiZaring] p. 35Theorem 7.2trelpss 38479  tz7.2 5088
[TakeutiZaring] p. 35Definition 7.1dftr3 4747
[TakeutiZaring] p. 36Proposition 7.4ordwe 5724
[TakeutiZaring] p. 36Proposition 7.5tz7.5 5732
[TakeutiZaring] p. 36Proposition 7.6ordelord 5733  ordelordALT 38567  ordelordALTVD 38923
[TakeutiZaring] p. 37Corollary 7.8ordelpss 5739  ordelssne 5738
[TakeutiZaring] p. 37Proposition 7.7tz7.7 5737
[TakeutiZaring] p. 37Proposition 7.9ordin 5741
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 6973
[TakeutiZaring] p. 38Corollary 7.15ordsson 6974
[TakeutiZaring] p. 38Definition 7.11df-on 5715
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 5743
[TakeutiZaring] p. 38Proposition 7.12onfrALT 38584  ordon 6967
[TakeutiZaring] p. 38Proposition 7.13onprc 6969
[TakeutiZaring] p. 39Theorem 7.17tfi 7038
[TakeutiZaring] p. 40Exercise 3ontr2 5760
[TakeutiZaring] p. 40Exercise 7dftr2 4745
[TakeutiZaring] p. 40Exercise 9onssmin 6982
[TakeutiZaring] p. 40Exercise 11unon 7016
[TakeutiZaring] p. 40Exercise 12ordun 5817
[TakeutiZaring] p. 40Exercise 14ordequn 5816
[TakeutiZaring] p. 40Proposition 7.19ssorduni 6970
[TakeutiZaring] p. 40Proposition 7.20elssuni 4458
[TakeutiZaring] p. 41Definition 7.22df-suc 5717
[TakeutiZaring] p. 41Proposition 7.23sssucid 5790  sucidg 5791
[TakeutiZaring] p. 41Proposition 7.24suceloni 6998
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 5806  ordnbtwn 5804
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7013
[TakeutiZaring] p. 42Exercise 1df-lim 5716
[TakeutiZaring] p. 42Exercise 4omssnlim 7064
[TakeutiZaring] p. 42Exercise 7ssnlim 7068
[TakeutiZaring] p. 42Exercise 8onsucssi 7026  ordelsuc 7005
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7007
[TakeutiZaring] p. 42Definition 7.27nlimon 7036
[TakeutiZaring] p. 42Definition 7.28dfom2 7052
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7070
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7071
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7072
[TakeutiZaring] p. 43Remarkomon 7061
[TakeutiZaring] p. 43Axiom 7inf3 8517  omex 8525
[TakeutiZaring] p. 43Theorem 7.32ordom 7059
[TakeutiZaring] p. 43Corollary 7.31find 7076
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7073
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7074
[TakeutiZaring] p. 44Exercise 1limomss 7055
[TakeutiZaring] p. 44Exercise 2int0 4481
[TakeutiZaring] p. 44Exercise 3trintss 4760
[TakeutiZaring] p. 44Exercise 4intss1 4483
[TakeutiZaring] p. 44Exercise 5intex 4811
[TakeutiZaring] p. 44Exercise 6oninton 6985
[TakeutiZaring] p. 44Exercise 11ordintdif 5762
[TakeutiZaring] p. 44Definition 7.35df-int 4467
[TakeutiZaring] p. 44Proposition 7.34noinfep 8542
[TakeutiZaring] p. 45Exercise 4onint 6980
[TakeutiZaring] p. 47Lemma 1tfrlem1 7457
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 7478
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 7479
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 7480
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 7487  tz7.44-2 7488  tz7.44-3 7489
[TakeutiZaring] p. 50Exercise 1smogt 7449
[TakeutiZaring] p. 50Exercise 3smoiso 7444
[TakeutiZaring] p. 50Definition 7.46df-smo 7428
[TakeutiZaring] p. 51Proposition 7.49tz7.49 7525  tz7.49c 7526
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 7523
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 7522
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 7524
[TakeutiZaring] p. 53Proposition 7.532eu5 2555
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 8819
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 8820
[TakeutiZaring] p. 56Definition 8.1oalim 7597  oasuc 7589
[TakeutiZaring] p. 57Remarktfindsg 7045
[TakeutiZaring] p. 57Proposition 8.2oacl 7600
[TakeutiZaring] p. 57Proposition 8.3oa0 7581  oa0r 7603
[TakeutiZaring] p. 57Proposition 8.16omcl 7601
[TakeutiZaring] p. 58Corollary 8.5oacan 7613
[TakeutiZaring] p. 58Proposition 8.4nnaord 7684  nnaordi 7683  oaord 7612  oaordi 7611
[TakeutiZaring] p. 59Proposition 8.6iunss2 4556  uniss2 4461
[TakeutiZaring] p. 59Proposition 8.7oawordri 7615
[TakeutiZaring] p. 59Proposition 8.8oawordeu 7620  oawordex 7622
[TakeutiZaring] p. 59Proposition 8.9nnacl 7676
[TakeutiZaring] p. 59Proposition 8.10oaabs 7709
[TakeutiZaring] p. 60Remarkoancom 8533
[TakeutiZaring] p. 60Proposition 8.11oalimcl 7625
[TakeutiZaring] p. 62Exercise 1nnarcl 7681
[TakeutiZaring] p. 62Exercise 5oaword1 7617
[TakeutiZaring] p. 62Definition 8.15om0 7582  om0x 7584  omlim 7598  omsuc 7591
[TakeutiZaring] p. 63Proposition 8.17nnecl 7678  nnmcl 7677
[TakeutiZaring] p. 63Proposition 8.19nnmord 7697  nnmordi 7696  omord 7633  omordi 7631
[TakeutiZaring] p. 63Proposition 8.20omcan 7634
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 7701  omwordri 7637
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 7604
[TakeutiZaring] p. 63Proposition 8.18(2)om1 7607  om1r 7608
[TakeutiZaring] p. 64Proposition 8.22om00 7640
[TakeutiZaring] p. 64Proposition 8.23omordlim 7642
[TakeutiZaring] p. 64Proposition 8.24omlimcl 7643
[TakeutiZaring] p. 64Proposition 8.25odi 7644
[TakeutiZaring] p. 65Theorem 8.26omass 7645
[TakeutiZaring] p. 67Definition 8.30nnesuc 7673  oe0 7587  oelim 7599  oesuc 7592  onesuc 7595
[TakeutiZaring] p. 67Proposition 8.31oe0m0 7585
[TakeutiZaring] p. 67Proposition 8.32oen0 7651
[TakeutiZaring] p. 67Proposition 8.33oeordi 7652
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 7586
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 7610
[TakeutiZaring] p. 68Corollary 8.34oeord 7653
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 7659
[TakeutiZaring] p. 68Proposition 8.35oewordri 7657
[TakeutiZaring] p. 68Proposition 8.37oeworde 7658
[TakeutiZaring] p. 69Proposition 8.41oeoa 7662
[TakeutiZaring] p. 70Proposition 8.42oeoe 7664
[TakeutiZaring] p. 73Theorem 9.1trcl 8589  tz9.1 8590
[TakeutiZaring] p. 76Definition 9.9df-r1 8612  r10 8616  r1lim 8620  r1limg 8619  r1suc 8618  r1sucg 8617
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 8628  r1ord2 8629  r1ordg 8626
[TakeutiZaring] p. 78Proposition 9.12tz9.12 8638
[TakeutiZaring] p. 78Proposition 9.13rankwflem 8663  tz9.13 8639  tz9.13g 8640
[TakeutiZaring] p. 79Definition 9.14df-rank 8613  rankval 8664  rankvalb 8645  rankvalg 8665
[TakeutiZaring] p. 79Proposition 9.16rankel 8687  rankelb 8672
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 8701  rankval3 8688  rankval3b 8674
[TakeutiZaring] p. 79Proposition 9.18rankonid 8677
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 8643
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 8682  rankr1c 8669  rankr1g 8680
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 8683
[TakeutiZaring] p. 80Exercise 1rankss 8697  rankssb 8696
[TakeutiZaring] p. 80Exercise 2unbndrank 8690
[TakeutiZaring] p. 80Proposition 9.19bndrank 8689
[TakeutiZaring] p. 83Axiom of Choiceac4 9282  dfac3 8929
[TakeutiZaring] p. 84Theorem 10.3dfac8a 8838  numth 9279  numth2 9278
[TakeutiZaring] p. 85Definition 10.4cardval 9353
[TakeutiZaring] p. 85Proposition 10.5cardid 9354  cardid2 8764
[TakeutiZaring] p. 85Proposition 10.9oncard 8771
[TakeutiZaring] p. 85Proposition 10.10carden 9358
[TakeutiZaring] p. 85Proposition 10.11cardidm 8770
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 8755
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 8776
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 8768
[TakeutiZaring] p. 87Proposition 10.15pwen 8118
[TakeutiZaring] p. 88Exercise 1en0 8004
[TakeutiZaring] p. 88Exercise 7infensuc 8123
[TakeutiZaring] p. 89Exercise 10omxpen 8047
[TakeutiZaring] p. 90Corollary 10.23cardnn 8774
[TakeutiZaring] p. 90Definition 10.27alephiso 8906
[TakeutiZaring] p. 90Proposition 10.20nneneq 8128
[TakeutiZaring] p. 90Proposition 10.22onomeneq 8135
[TakeutiZaring] p. 90Proposition 10.26alephprc 8907
[TakeutiZaring] p. 90Corollary 10.21(1)php5 8133
[TakeutiZaring] p. 91Exercise 2alephle 8896
[TakeutiZaring] p. 91Exercise 3aleph0 8874
[TakeutiZaring] p. 91Exercise 4cardlim 8783
[TakeutiZaring] p. 91Exercise 7infpss 9024
[TakeutiZaring] p. 91Exercise 8infcntss 8219
[TakeutiZaring] p. 91Definition 10.29df-fin 7944  isfi 7964
[TakeutiZaring] p. 92Proposition 10.32onfin 8136
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8040
[TakeutiZaring] p. 93Proposition 10.35fodomb 9333
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8996  unxpdom 8152
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 8785  cardsdomelir 8784
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 8154
[TakeutiZaring] p. 94Proposition 10.39infxpen 8822
[TakeutiZaring] p. 95Definition 10.42df-map 7844
[TakeutiZaring] p. 95Proposition 10.40infxpidm 9369  infxpidm2 8825
[TakeutiZaring] p. 95Proposition 10.41infcda 9015  infxp 9022
[TakeutiZaring] p. 96Proposition 10.44pw2en 8052  pw2f1o 8050
[TakeutiZaring] p. 96Proposition 10.45mapxpen 8111
[TakeutiZaring] p. 97Theorem 10.46ac6s3 9294
[TakeutiZaring] p. 98Theorem 10.46ac6c5 9289  ac6s5 9298
[TakeutiZaring] p. 98Theorem 10.47unidom 9350
[TakeutiZaring] p. 100Definition 11.1cfcof 9081
[TakeutiZaring] p. 101Proposition 11.7cofsmo 9076
[TakeutiZaring] p. 102Exercise 1cfle 9061
[TakeutiZaring] p. 102Exercise 2cf0 9058
[TakeutiZaring] p. 102Exercise 3cfsuc 9064
[TakeutiZaring] p. 102Exercise 4cfom 9071
[TakeutiZaring] p. 102Proposition 11.9coftr 9080
[TakeutiZaring] p. 103Theorem 11.15alephreg 9389
[TakeutiZaring] p. 103Proposition 11.11cardcf 9059
[TakeutiZaring] p. 103Proposition 11.13alephsing 9083
[TakeutiZaring] p. 104Corollary 11.17cardinfima 8905
[TakeutiZaring] p. 104Proposition 11.16carduniima 8904
[TakeutiZaring] p. 104Proposition 11.18alephfp 8916  alephfp2 8917
[TakeutiZaring] p. 106Theorem 11.20gchina 9506
[TakeutiZaring] p. 106Theorem 11.21mappwen 8920
[TakeutiZaring] p. 107Theorem 11.26konigth 9376
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 9390
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 9391
[Tarski] p. 67Axiom B5ax-c5 33987
[Tarski] p. 67Scheme B5sp 2051
[Tarski] p. 68Lemma 6avril1 27289  equid 1937
[Tarski] p. 69Lemma 7equcomi 1942
[Tarski] p. 70Lemma 14spim 2252  spime 2254  spimeh 1923
[Tarski] p. 70Lemma 16ax-12 2045  ax-c15 33993  ax12i 1877
[Tarski] p. 70Lemmas 16 and 17sb6 2427
[Tarski] p. 75Axiom B7ax6v 1887
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1837  ax5ALT 34011
[Tarski], p. 75Scheme B8 of system S2ax-7 1933  ax-8 1990  ax-9 1997
[Tarski1999] p. 178Axiom 4axtgsegcon 25344
[Tarski1999] p. 178Axiom 5axtg5seg 25345
[Tarski1999] p. 179Axiom 7axtgpasch 25347
[Tarski1999] p. 180Axiom 7.1axtgpasch 25347
[Tarski1999] p. 185Axiom 11axtgcont1 25348
[Truss] p. 114Theorem 5.18ruc 14953
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 33419
[Viaclovsky8] p. 3Proposition 7ismblfin 33421
[Weierstrass] p. 272Definitiondf-mdet 20372  mdetuni 20409
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 544
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 885
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-pm2.04 33238
[WhiteheadRussell] p. 100Theorem *2.05frege5 37914  imim2 58  wl-imim2 33233
[WhiteheadRussell] p. 101Theorem *2.06barbara 2561  syl 17
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-id 33236
[WhiteheadRussell] p. 102Theorem *2.14notnotr 125  notnotrALT2 38983  wl-notnotr 33237
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 37944  axfrege28 37943  con3 149
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 120  wl-pm2.21 33230
[WhiteheadRussell] p. 104Theorem *2.27conventions-label 27229  pm2.27 42  wl-pm2.27 33228
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 417  pm2.67 418
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 463  pm3.2im 157
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 460
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 461
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 473  simplim 163
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 477  simprim 162
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 608
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 609
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 602
[WhiteheadRussell] p. 113Theorem *3.44jao 534  pm3.44 533
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 905
[WhiteheadRussell] p. 117Theorem *4.22biantr 971  bitr 744
[WhiteheadRussell] p. 117Theorem *4.25oridm 536  pm4.25 537
[WhiteheadRussell] p. 119Theorem *4.45orabs 899  pm4.45 723  pm4.45im 584
[WhiteheadRussell] p. 120Theorem *4.56ioran 511  pm4.56 516
[WhiteheadRussell] p. 120Theorem *4.57oran 517  pm4.57 518
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 661  pm4.71d 665  pm4.71i 663  pm4.71r 662  pm4.71rd 666  pm4.71ri 664
[WhiteheadRussell] p. 121Theorem *4.76jcab 906  pm4.76 909
[WhiteheadRussell] p. 121Theorem *4.77jaob 821  pm4.77 827
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 376  impexp 462  pm4.87 607
[WhiteheadRussell] p. 124Theorem *5.18nbbn 373  pm5.18 371
[WhiteheadRussell] p. 125Theorem *5.41imdi 378  pm5.41 379
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 38428  pm13.13b 38429
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 38588  pm13.193 38432
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 38443  pm14.122b 38444  pm14.122c 38445
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 38446  pm14.123b 38447  pm14.123c 38448