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

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

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

Bibliographic Cross-Reference for the Metamath Proof Explorer
Bibliographic ReferenceDescriptionMetamath Proof Explorer Page(s)
[Adamek] p. 21Definition 3.1df-cat 17612
[Adamek] p. 21Condition 3.1(b)df-cat 17612
[Adamek] p. 22Example 3.3(1)df-setc 18026
[Adamek] p. 24Example 3.3(4.c)0cat 17633
[Adamek] p. 24Example 3.3(4.d)df-prstc 47683  prsthinc 47674
[Adamek] p. 24Example 3.3(4.e)df-mndtc 47704  df-mndtc 47704
[Adamek] p. 25Definition 3.5df-oppc 17656
[Adamek] p. 28Remark 3.9oppciso 17728
[Adamek] p. 28Remark 3.12invf1o 17716  invisoinvl 17737
[Adamek] p. 28Example 3.13idinv 17736  idiso 17735
[Adamek] p. 28Corollary 3.11inveq 17721
[Adamek] p. 28Definition 3.8df-inv 17695  df-iso 17696  dfiso2 17719
[Adamek] p. 28Proposition 3.10sectcan 17702
[Adamek] p. 29Remark 3.16cicer 17753
[Adamek] p. 29Definition 3.15cic 17746  df-cic 17743
[Adamek] p. 29Definition 3.17df-func 17808
[Adamek] p. 29Proposition 3.14(1)invinv 17717
[Adamek] p. 29Proposition 3.14(2)invco 17718  isoco 17724
[Adamek] p. 30Remark 3.19df-func 17808
[Adamek] p. 30Example 3.20(1)idfucl 17831
[Adamek] p. 32Proposition 3.21funciso 17824
[Adamek] p. 33Example 3.26(2)df-thinc 47640  prsthinc 47674  thincciso 47669
[Adamek] p. 33Example 3.26(3)df-mndtc 47704
[Adamek] p. 33Proposition 3.23cofucl 17838
[Adamek] p. 34Remark 3.28(2)catciso 18061
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18119
[Adamek] p. 34Definition 3.27(2)df-fth 17856
[Adamek] p. 34Definition 3.27(3)df-full 17855
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18119
[Adamek] p. 35Corollary 3.32ffthiso 17880
[Adamek] p. 35Proposition 3.30(c)cofth 17886
[Adamek] p. 35Proposition 3.30(d)cofull 17885
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18104
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18104
[Adamek] p. 39Definition 3.41funcoppc 17825
[Adamek] p. 39Definition 3.44.df-catc 18049
[Adamek] p. 39Proposition 3.43(c)fthoppc 17874
[Adamek] p. 39Proposition 3.43(d)fulloppc 17873
[Adamek] p. 40Remark 3.48catccat 18058
[Adamek] p. 40Definition 3.47df-catc 18049
[Adamek] p. 48Example 4.3(1.a)0subcat 17788
[Adamek] p. 48Example 4.3(1.b)catsubcat 17789
[Adamek] p. 48Definition 4.1(2)fullsubc 17800
[Adamek] p. 48Definition 4.1(a)df-subc 17759
[Adamek] p. 49Remark 4.4(2)ressffth 17889
[Adamek] p. 83Definition 6.1df-nat 17894
[Adamek] p. 87Remark 6.14(a)fuccocl 17917
[Adamek] p. 87Remark 6.14(b)fucass 17921
[Adamek] p. 87Definition 6.15df-fuc 17895
[Adamek] p. 88Remark 6.16fuccat 17923
[Adamek] p. 101Definition 7.1df-inito 17934
[Adamek] p. 101Example 7.2 (6)irinitoringc 46967
[Adamek] p. 102Definition 7.4df-termo 17935
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17962
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17966
[Adamek] p. 103Definition 7.7df-zeroo 17936
[Adamek] p. 103Example 7.9 (3)nzerooringczr 46970
[Adamek] p. 103Proposition 7.6termoeu1w 17969
[Adamek] p. 106Definition 7.19df-sect 17694
[Adamek] p. 185Section 10.67updjud 9929
[Adamek] p. 478Item Rngdf-ringc 46903
[AhoHopUll] p. 2Section 1.1df-bigo 47234
[AhoHopUll] p. 12Section 1.3df-blen 47256
[AhoHopUll] p. 318Section 9.1df-concat 14521  df-pfx 14621  df-substr 14591  df-word 14465  lencl 14483  wrd0 14489
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24225  df-nmoo 29998
[AkhiezerGlazman] p. 64Theoremhmopidmch 31406  hmopidmchi 31404
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 31454  pjcmul2i 31455
[AkhiezerGlazman] p. 72Theoremcnvunop 31171  unoplin 31173
[AkhiezerGlazman] p. 72Equation 2unopadj 31172  unopadj2 31191
[AkhiezerGlazman] p. 73Theoremelunop2 31266  lnopunii 31265
[AkhiezerGlazman] p. 80Proposition 1adjlnop 31339
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27414
[Alling] p. 184Axiom Bbdayfo 27180
[Alling] p. 184Axiom Osltso 27179
[Alling] p. 184Axiom SDnodense 27195
[Alling] p. 185Lemma 0nocvxmin 27280
[Alling] p. 185Theoremconway 27300
[Alling] p. 185Axiom FEnoeta 27246
[Alling] p. 186Theorem 4slerec 27320
[Alling], p. 2Definitionrp-brsslt 42174
[Alling], p. 3Notenla0001 42177  nla0002 42175  nla0003 42176
[Apostol] p. 18Theorem I.1addcan 11398  addcan2d 11418  addcan2i 11408  addcand 11417  addcani 11407
[Apostol] p. 18Theorem I.2negeu 11450
[Apostol] p. 18Theorem I.3negsub 11508  negsubd 11577  negsubi 11538
[Apostol] p. 18Theorem I.4negneg 11510  negnegd 11562  negnegi 11530
[Apostol] p. 18Theorem I.5subdi 11647  subdid 11670  subdii 11663  subdir 11648  subdird 11671  subdiri 11664
[Apostol] p. 18Theorem I.6mul01 11393  mul01d 11413  mul01i 11404  mul02 11392  mul02d 11412  mul02i 11403
[Apostol] p. 18Theorem I.7mulcan 11851  mulcan2d 11848  mulcand 11847  mulcani 11853
[Apostol] p. 18Theorem I.8receu 11859  xreceu 32088
[Apostol] p. 18Theorem I.9divrec 11888  divrecd 11993  divreci 11959  divreczi 11952
[Apostol] p. 18Theorem I.10recrec 11911  recreci 11946
[Apostol] p. 18Theorem I.11mul0or 11854  mul0ord 11864  mul0ori 11862
[Apostol] p. 18Theorem I.12mul2neg 11653  mul2negd 11669  mul2negi 11662  mulneg1 11650  mulneg1d 11667  mulneg1i 11660
[Apostol] p. 18Theorem I.13divadddiv 11929  divadddivd 12034  divadddivi 11976
[Apostol] p. 18Theorem I.14divmuldiv 11914  divmuldivd 12031  divmuldivi 11974  rdivmuldivd 20227
[Apostol] p. 18Theorem I.15divdivdiv 11915  divdivdivd 12037  divdivdivi 11977
[Apostol] p. 20Axiom 7rpaddcl 12996  rpaddcld 13031  rpmulcl 12997  rpmulcld 13032
[Apostol] p. 20Axiom 8rpneg 13006
[Apostol] p. 20Axiom 90nrp 13009
[Apostol] p. 20Theorem I.17lttri 11340
[Apostol] p. 20Theorem I.18ltadd1d 11807  ltadd1dd 11825  ltadd1i 11768
[Apostol] p. 20Theorem I.19ltmul1 12064  ltmul1a 12063  ltmul1i 12132  ltmul1ii 12142  ltmul2 12065  ltmul2d 13058  ltmul2dd 13072  ltmul2i 12135
[Apostol] p. 20Theorem I.20msqgt0 11734  msqgt0d 11781  msqgt0i 11751
[Apostol] p. 20Theorem I.210lt1 11736
[Apostol] p. 20Theorem I.23lt0neg1 11720  lt0neg1d 11783  ltneg 11714  ltnegd 11792  ltnegi 11758
[Apostol] p. 20Theorem I.25lt2add 11699  lt2addd 11837  lt2addi 11776
[Apostol] p. 20Definition of positive numbersdf-rp 12975
[Apostol] p. 21Exercise 4recgt0 12060  recgt0d 12148  recgt0i 12119  recgt0ii 12120
[Apostol] p. 22Definition of integersdf-z 12559
[Apostol] p. 22Definition of positive integersdfnn3 12226
[Apostol] p. 22Definition of rationalsdf-q 12933
[Apostol] p. 24Theorem I.26supeu 9449
[Apostol] p. 26Theorem I.28nnunb 12468
[Apostol] p. 26Theorem I.29arch 12469  archd 43856
[Apostol] p. 28Exercise 2btwnz 12665
[Apostol] p. 28Exercise 3nnrecl 12470
[Apostol] p. 28Exercise 4rebtwnz 12931
[Apostol] p. 28Exercise 5zbtwnre 12930
[Apostol] p. 28Exercise 6qbtwnre 13178
[Apostol] p. 28Exercise 10(a)zeneo 16282  zneo 12645  zneoALTV 46337
[Apostol] p. 29Theorem I.35cxpsqrtth 26238  msqsqrtd 15387  resqrtth 15202  sqrtth 15311  sqrtthi 15317  sqsqrtd 15386
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12215
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12897
[Apostol] p. 361Remarkcrreczi 14191
[Apostol] p. 363Remarkabsgt0i 15346
[Apostol] p. 363Exampleabssubd 15400  abssubi 15350
[ApostolNT] p. 7Remarkfmtno0 46208  fmtno1 46209  fmtno2 46218  fmtno3 46219  fmtno4 46220  fmtno5fac 46250  fmtnofz04prm 46245
[ApostolNT] p. 7Definitiondf-fmtno 46196
[ApostolNT] p. 8Definitiondf-ppi 26604
[ApostolNT] p. 14Definitiondf-dvds 16198
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16213
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16237
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16232
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16226
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16228
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16214
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16215
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16220
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16254
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16256
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16258
[ApostolNT] p. 15Definitiondf-gcd 16436  dfgcd2 16488
[ApostolNT] p. 16Definitionisprm2 16619
[ApostolNT] p. 16Theorem 1.5coprmdvds 16590
[ApostolNT] p. 16Theorem 1.7prminf 16848
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16454
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16489
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16491
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16469
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16461
[ApostolNT] p. 17Theorem 1.8coprm 16648
[ApostolNT] p. 17Theorem 1.9euclemma 16650
[ApostolNT] p. 17Theorem 1.101arith2 16861
[ApostolNT] p. 18Theorem 1.13prmrec 16855
[ApostolNT] p. 19Theorem 1.14divalg 16346
[ApostolNT] p. 20Theorem 1.15eucalg 16524
[ApostolNT] p. 24Definitiondf-mu 26605
[ApostolNT] p. 25Definitiondf-phi 16699
[ApostolNT] p. 25Theorem 2.1musum 26695
[ApostolNT] p. 26Theorem 2.2phisum 16723
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16709
[ApostolNT] p. 28Theorem 2.5(c)phimul 16713
[ApostolNT] p. 32Definitiondf-vma 26602
[ApostolNT] p. 32Theorem 2.9muinv 26697
[ApostolNT] p. 32Theorem 2.10vmasum 26719
[ApostolNT] p. 38Remarkdf-sgm 26606
[ApostolNT] p. 38Definitiondf-sgm 26606
[ApostolNT] p. 75Definitiondf-chp 26603  df-cht 26601
[ApostolNT] p. 104Definitioncongr 16601
[ApostolNT] p. 106Remarkdvdsval3 16201
[ApostolNT] p. 106Definitionmoddvds 16208
[ApostolNT] p. 107Example 2mod2eq0even 16289
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16290
[ApostolNT] p. 107Example 4zmod1congr 13853
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13890
[ApostolNT] p. 107Theorem 5.2(c)modexp 14201
[ApostolNT] p. 108Theorem 5.3modmulconst 16231
[ApostolNT] p. 109Theorem 5.4cncongr1 16604
[ApostolNT] p. 109Theorem 5.6gcdmodi 17007
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16606
[ApostolNT] p. 113Theorem 5.17eulerth 16716
[ApostolNT] p. 113Theorem 5.18vfermltl 16734
[ApostolNT] p. 114Theorem 5.19fermltl 16717
[ApostolNT] p. 116Theorem 5.24wilthimp 26576
[ApostolNT] p. 179Definitiondf-lgs 26798  lgsprme0 26842
[ApostolNT] p. 180Example 11lgs 26843
[ApostolNT] p. 180Theorem 9.2lgsvalmod 26819
[ApostolNT] p. 180Theorem 9.3lgsdirprm 26834
[ApostolNT] p. 181Theorem 9.4m1lgs 26891
[ApostolNT] p. 181Theorem 9.52lgs 26910  2lgsoddprm 26919
[ApostolNT] p. 182Theorem 9.6gausslemma2d 26877
[ApostolNT] p. 185Theorem 9.8lgsquad 26886
[ApostolNT] p. 188Definitiondf-lgs 26798  lgs1 26844
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 26835
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 26837
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 26845
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 26846
[Baer] p. 40Property (b)mapdord 40509
[Baer] p. 40Property (c)mapd11 40510
[Baer] p. 40Property (e)mapdin 40533  mapdlsm 40535
[Baer] p. 40Property (f)mapd0 40536
[Baer] p. 40Definition of projectivitydf-mapd 40496  mapd1o 40519
[Baer] p. 41Property (g)mapdat 40538
[Baer] p. 44Part (1)mapdpg 40577
[Baer] p. 45Part (2)hdmap1eq 40672  mapdheq 40599  mapdheq2 40600  mapdheq2biN 40601
[Baer] p. 45Part (3)baerlem3 40584
[Baer] p. 46Part (4)mapdheq4 40603  mapdheq4lem 40602
[Baer] p. 46Part (5)baerlem5a 40585  baerlem5abmN 40589  baerlem5amN 40587  baerlem5b 40586  baerlem5bmN 40588
[Baer] p. 47Part (6)hdmap1l6 40692  hdmap1l6a 40680  hdmap1l6e 40685  hdmap1l6f 40686  hdmap1l6g 40687  hdmap1l6lem1 40678  hdmap1l6lem2 40679  mapdh6N 40618  mapdh6aN 40606  mapdh6eN 40611  mapdh6fN 40612  mapdh6gN 40613  mapdh6lem1N 40604  mapdh6lem2N 40605
[Baer] p. 48Part 9hdmapval 40699
[Baer] p. 48Part 10hdmap10 40711
[Baer] p. 48Part 11hdmapadd 40714
[Baer] p. 48Part (6)hdmap1l6h 40688  mapdh6hN 40614
[Baer] p. 48Part (7)mapdh75cN 40624  mapdh75d 40625  mapdh75e 40623  mapdh75fN 40626  mapdh7cN 40620  mapdh7dN 40621  mapdh7eN 40619  mapdh7fN 40622
[Baer] p. 48Part (8)mapdh8 40659  mapdh8a 40646  mapdh8aa 40647  mapdh8ab 40648  mapdh8ac 40649  mapdh8ad 40650  mapdh8b 40651  mapdh8c 40652  mapdh8d 40654  mapdh8d0N 40653  mapdh8e 40655  mapdh8g 40656  mapdh8i 40657  mapdh8j 40658
[Baer] p. 48Part (9)mapdh9a 40660
[Baer] p. 48Equation 10mapdhvmap 40640
[Baer] p. 49Part 12hdmap11 40719  hdmapeq0 40715  hdmapf1oN 40736  hdmapneg 40717  hdmaprnN 40735  hdmaprnlem1N 40720  hdmaprnlem3N 40721  hdmaprnlem3uN 40722  hdmaprnlem4N 40724  hdmaprnlem6N 40725  hdmaprnlem7N 40726  hdmaprnlem8N 40727  hdmaprnlem9N 40728  hdmapsub 40718
[Baer] p. 49Part 14hdmap14lem1 40739  hdmap14lem10 40748  hdmap14lem1a 40737  hdmap14lem2N 40740  hdmap14lem2a 40738  hdmap14lem3 40741  hdmap14lem8 40746  hdmap14lem9 40747
[Baer] p. 50Part 14hdmap14lem11 40749  hdmap14lem12 40750  hdmap14lem13 40751  hdmap14lem14 40752  hdmap14lem15 40753  hgmapval 40758
[Baer] p. 50Part 15hgmapadd 40765  hgmapmul 40766  hgmaprnlem2N 40768  hgmapvs 40762
[Baer] p. 50Part 16hgmaprnN 40772
[Baer] p. 110Lemma 1hdmapip0com 40788
[Baer] p. 110Line 27hdmapinvlem1 40789
[Baer] p. 110Line 28hdmapinvlem2 40790
[Baer] p. 110Line 30hdmapinvlem3 40791
[Baer] p. 110Part 1.2hdmapglem5 40793  hgmapvv 40797
[Baer] p. 110Proposition 1hdmapinvlem4 40792
[Baer] p. 111Line 10hgmapvvlem1 40794
[Baer] p. 111Line 15hdmapg 40801  hdmapglem7 40800
[Bauer], p. 483Theorem 1.22irrexpq 26239  2irrexpqALT 26305
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2564
[BellMachover] p. 460Notationdf-mo 2535
[BellMachover] p. 460Definitionmo3 2559
[BellMachover] p. 461Axiom Extax-ext 2704
[BellMachover] p. 462Theorem 1.1axextmo 2708
[BellMachover] p. 463Axiom Repaxrep5 5292
[BellMachover] p. 463Scheme Sepax-sep 5300
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 35945  bm1.3ii 5303
[BellMachover] p. 466Problemaxpow2 5366
[BellMachover] p. 466Axiom Powaxpow3 5367
[BellMachover] p. 466Axiom Unionaxun2 7727
[BellMachover] p. 468Definitiondf-ord 6368
[BellMachover] p. 469Theorem 2.2(i)ordirr 6383
[BellMachover] p. 469Theorem 2.2(iii)onelon 6390
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6385
[BellMachover] p. 471Definition of Ndf-om 7856
[BellMachover] p. 471Problem 2.5(ii)uniordint 7789
[BellMachover] p. 471Definition of Limdf-lim 6370
[BellMachover] p. 472Axiom Infzfinf2 9637
[BellMachover] p. 473Theorem 2.8limom 7871
[BellMachover] p. 477Equation 3.1df-r1 9759
[BellMachover] p. 478Definitionrankval2 9813
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9777  r1ord3g 9774
[BellMachover] p. 480Axiom Regzfreg 9590
[BellMachover] p. 488Axiom ACac5 10472  dfac4 10117
[BellMachover] p. 490Definition of alephalephval3 10105
[BeltramettiCassinelli] p. 98Remarkatlatmstc 38189
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 31606
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 31648  chirredi 31647
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 31636
[Beran] p. 3Definition of joinsshjval3 30607
[Beran] p. 39Theorem 2.3(i)cmcm2 30869  cmcm2i 30846  cmcm2ii 30851  cmt2N 38120
[Beran] p. 40Theorem 2.3(iii)lecm 30870  lecmi 30855  lecmii 30856
[Beran] p. 45Theorem 3.4cmcmlem 30844
[Beran] p. 49Theorem 4.2cm2j 30873  cm2ji 30878  cm2mi 30879
[Beran] p. 95Definitiondf-sh 30460  issh2 30462
[Beran] p. 95Lemma 3.1(S5)his5 30339
[Beran] p. 95Lemma 3.1(S6)his6 30352
[Beran] p. 95Lemma 3.1(S7)his7 30343
[Beran] p. 95Lemma 3.2(S8)ho01i 31081
[Beran] p. 95Lemma 3.2(S9)hoeq1 31083
[Beran] p. 95Lemma 3.2(S10)ho02i 31082
[Beran] p. 95Lemma 3.2(S11)hoeq2 31084
[Beran] p. 95Postulate (S1)ax-his1 30335  his1i 30353
[Beran] p. 95Postulate (S2)ax-his2 30336
[Beran] p. 95Postulate (S3)ax-his3 30337
[Beran] p. 95Postulate (S4)ax-his4 30338
[Beran] p. 96Definition of normdf-hnorm 30221  dfhnorm2 30375  normval 30377
[Beran] p. 96Definition for Cauchy sequencehcau 30437
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30226
[Beran] p. 96Definition of complete subspaceisch3 30494
[Beran] p. 96Definition of convergedf-hlim 30225  hlimi 30441
[Beran] p. 97Theorem 3.3(i)norm-i-i 30386  norm-i 30382
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 30390  norm-ii 30391  normlem0 30362  normlem1 30363  normlem2 30364  normlem3 30365  normlem4 30366  normlem5 30367  normlem6 30368  normlem7 30369  normlem7tALT 30372
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 30392  norm-iii 30393
[Beran] p. 98Remark 3.4bcs 30434  bcsiALT 30432  bcsiHIL 30433
[Beran] p. 98Remark 3.4(B)normlem9at 30374  normpar 30408  normpari 30407
[Beran] p. 98Remark 3.4(C)normpyc 30399  normpyth 30398  normpythi 30395
[Beran] p. 99Remarklnfn0 31300  lnfn0i 31295  lnop0 31219  lnop0i 31223
[Beran] p. 99Theorem 3.5(i)nmcexi 31279  nmcfnex 31306  nmcfnexi 31304  nmcopex 31282  nmcopexi 31280
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 31307  nmcfnlbi 31305  nmcoplb 31283  nmcoplbi 31281
[Beran] p. 99Theorem 3.5(iii)lnfncon 31309  lnfnconi 31308  lnopcon 31288  lnopconi 31287
[Beran] p. 100Lemma 3.6normpar2i 30409
[Beran] p. 101Lemma 3.6norm3adifi 30406  norm3adifii 30401  norm3dif 30403  norm3difi 30400
[Beran] p. 102Theorem 3.7(i)chocunii 30554  pjhth 30646  pjhtheu 30647  pjpjhth 30678  pjpjhthi 30679  pjth 24956
[Beran] p. 102Theorem 3.7(ii)ococ 30659  ococi 30658
[Beran] p. 103Remark 3.8nlelchi 31314
[Beran] p. 104Theorem 3.9riesz3i 31315  riesz4 31317  riesz4i 31316
[Beran] p. 104Theorem 3.10cnlnadj 31332  cnlnadjeu 31331  cnlnadjeui 31330  cnlnadji 31329  cnlnadjlem1 31320  nmopadjlei 31341
[Beran] p. 106Theorem 3.11(i)adjeq0 31344
[Beran] p. 106Theorem 3.11(v)nmopadji 31343
[Beran] p. 106Theorem 3.11(ii)adjmul 31345
[Beran] p. 106Theorem 3.11(iv)adjadj 31189
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 31355  nmopcoadji 31354
[Beran] p. 106Theorem 3.11(iii)adjadd 31346
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 31356
[Beran] p. 106Theorem 3.11(viii)adjcoi 31353  pjadj2coi 31457  pjadjcoi 31414
[Beran] p. 107Definitiondf-ch 30474  isch2 30476
[Beran] p. 107Remark 3.12choccl 30559  isch3 30494  occl 30557  ocsh 30536  shoccl 30558  shocsh 30537
[Beran] p. 107Remark 3.12(B)ococin 30661
[Beran] p. 108Theorem 3.13chintcl 30585
[Beran] p. 109Property (i)pjadj2 31440  pjadj3 31441  pjadji 30938  pjadjii 30927
[Beran] p. 109Property (ii)pjidmco 31434  pjidmcoi 31430  pjidmi 30926
[Beran] p. 110Definition of projector orderingpjordi 31426
[Beran] p. 111Remarkho0val 31003  pjch1 30923
[Beran] p. 111Definitiondf-hfmul 30987  df-hfsum 30986  df-hodif 30985  df-homul 30984  df-hosum 30983
[Beran] p. 111Lemma 4.4(i)pjo 30924
[Beran] p. 111Lemma 4.4(ii)pjch 30947  pjchi 30685
[Beran] p. 111Lemma 4.4(iii)pjoc2 30692  pjoc2i 30691
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 30933
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 31418  pjssmii 30934
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 31417
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 31416
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 31421
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 31419  pjssge0ii 30935
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 31420  pjdifnormii 30936
[Bobzien] p. 116Statement T3stoic3 1779
[Bobzien] p. 117Statement T2stoic2a 1777
[Bobzien] p. 117Statement T4stoic4a 1780
[Bobzien] p. 117Conclusion the contradictorystoic1a 1775
[Bogachev] p. 16Definition 1.5df-oms 33291
[Bogachev] p. 17Lemma 1.5.4omssubadd 33299
[Bogachev] p. 17Example 1.5.2omsmon 33297
[Bogachev] p. 41Definition 1.11.2df-carsg 33301
[Bogachev] p. 42Theorem 1.11.4carsgsiga 33321
[Bogachev] p. 116Definition 2.3.1df-itgm 33352  df-sitm 33330
[Bogachev] p. 118Chapter 2.4.4df-itgm 33352
[Bogachev] p. 118Definition 2.4.1df-sitg 33329
[Bollobas] p. 1Section I.1df-edg 28308  isuhgrop 28330  isusgrop 28422  isuspgrop 28421
[Bollobas] p. 2Section I.1df-subgr 28525  uhgrspan1 28560  uhgrspansubgr 28548
[Bollobas] p. 3Definitionisomuspgr 46502
[Bollobas] p. 3Section I.1cusgrsize 28711  df-cusgr 28669  df-nbgr 28590  fusgrmaxsize 28721
[Bollobas] p. 4Definitiondf-upwlks 46512  df-wlks 28856
[Bollobas] p. 4Section I.1finsumvtxdg2size 28807  finsumvtxdgeven 28809  fusgr1th 28808  fusgrvtxdgonume 28811  vtxdgoddnumeven 28810
[Bollobas] p. 5Notationdf-pths 28973
[Bollobas] p. 5Definitiondf-crcts 29043  df-cycls 29044  df-trls 28949  df-wlkson 28857
[Bollobas] p. 7Section I.1df-ushgr 28319
[BourbakiAlg1] p. 1Definition 1df-clintop 46610  df-cllaw 46596  df-mgm 18561  df-mgm2 46629
[BourbakiAlg1] p. 4Definition 5df-assintop 46611  df-asslaw 46598  df-sgrp 18610  df-sgrp2 46631
[BourbakiAlg1] p. 7Definition 8df-cmgm2 46630  df-comlaw 46597
[BourbakiAlg1] p. 12Definition 2df-mnd 18626
[BourbakiAlg1] p. 92Definition 1df-ring 20058
[BourbakiAlg1] p. 93Section I.8.1df-rng 46649
[BourbakiEns] p. Proposition 8fcof1 7285  fcofo 7286
[BourbakiTop1] p. Remarkxnegmnf 13189  xnegpnf 13188
[BourbakiTop1] p. Remark rexneg 13190
[BourbakiTop1] p. Remark 3ust0 23724  ustfilxp 23717
[BourbakiTop1] p. Axiom GT'tgpsubcn 23594
[BourbakiTop1] p. Criterionishmeo 23263
[BourbakiTop1] p. Example 1cstucnd 23789  iducn 23788  snfil 23368
[BourbakiTop1] p. Example 2neifil 23384
[BourbakiTop1] p. Theorem 1cnextcn 23571
[BourbakiTop1] p. Theorem 2ucnextcn 23809
[BourbakiTop1] p. Theorem 3df-hcmp 32937
[BourbakiTop1] p. Paragraph 3infil 23367
[BourbakiTop1] p. Definition 1df-ucn 23781  df-ust 23705  filintn0 23365  filn0 23366  istgp 23581  ucnprima 23787
[BourbakiTop1] p. Definition 2df-cfilu 23792
[BourbakiTop1] p. Definition 3df-cusp 23803  df-usp 23762  df-utop 23736  trust 23734
[BourbakiTop1] p. Definition 6df-pcmp 32836
[BourbakiTop1] p. Property V_issnei2 22620
[BourbakiTop1] p. Theorem 1(d)iscncl 22773
[BourbakiTop1] p. Condition F_Iustssel 23710
[BourbakiTop1] p. Condition U_Iustdiag 23713
[BourbakiTop1] p. Property V_iiinnei 22629
[BourbakiTop1] p. Property V_ivneiptopreu 22637  neissex 22631
[BourbakiTop1] p. Proposition 1neips 22617  neiss 22613  ucncn 23790  ustund 23726  ustuqtop 23751
[BourbakiTop1] p. Proposition 2cnpco 22771  neiptopreu 22637  utop2nei 23755  utop3cls 23756
[BourbakiTop1] p. Proposition 3fmucnd 23797  uspreg 23779  utopreg 23757
[BourbakiTop1] p. Proposition 4imasncld 23195  imasncls 23196  imasnopn 23194
[BourbakiTop1] p. Proposition 9cnpflf2 23504
[BourbakiTop1] p. Condition F_IIustincl 23712
[BourbakiTop1] p. Condition U_IIustinvel 23714
[BourbakiTop1] p. Property V_iiielnei 22615
[BourbakiTop1] p. Proposition 11cnextucn 23808
[BourbakiTop1] p. Condition F_IIbustbasel 23711
[BourbakiTop1] p. Condition U_IIIustexhalf 23715
[BourbakiTop1] p. Definition C'''df-cmp 22891
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23350
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22396
[BourbakiTop2] p. 195Definition 1df-ldlf 32833
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 44778
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 44780  stoweid 44779
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 44717  stoweidlem10 44726  stoweidlem14 44730  stoweidlem15 44731  stoweidlem35 44751  stoweidlem36 44752  stoweidlem37 44753  stoweidlem38 44754  stoweidlem40 44756  stoweidlem41 44757  stoweidlem43 44759  stoweidlem44 44760  stoweidlem46 44762  stoweidlem5 44721  stoweidlem50 44766  stoweidlem52 44768  stoweidlem53 44769  stoweidlem55 44771  stoweidlem56 44772
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 44739  stoweidlem24 44740  stoweidlem27 44743  stoweidlem28 44744  stoweidlem30 44746
[BrosowskiDeutsh] p. 91Proofstoweidlem34 44750  stoweidlem59 44775  stoweidlem60 44776
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 44761  stoweidlem49 44765  stoweidlem7 44723
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 44747  stoweidlem39 44755  stoweidlem42 44758  stoweidlem48 44764  stoweidlem51 44767  stoweidlem54 44770  stoweidlem57 44773  stoweidlem58 44774
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 44741
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 44733
[BrosowskiDeutsh] p. 92Proofstoweidlem11 44727  stoweidlem13 44729  stoweidlem26 44742  stoweidlem61 44777
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 44734
[Bruck] p. 1Section I.1df-clintop 46610  df-mgm 18561  df-mgm2 46629
[Bruck] p. 23Section II.1df-sgrp 18610  df-sgrp2 46631
[Bruck] p. 28Theorem 3.2dfgrp3 18922
[ChoquetDD] p. 2Definition of mappingdf-mpt 5233
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 29656
[Clemente] p. 10Definition I` `m,nnatded 29656
[Clemente] p. 11Definition E=>m,nnatded 29656
[Clemente] p. 11Definition I=>m,nnatded 29656
[Clemente] p. 11Definition E` `(1)natded 29656
[Clemente] p. 11Definition E` `(2)natded 29656
[Clemente] p. 12Definition E` `m,n,pnatded 29656
[Clemente] p. 12Definition I` `n(1)natded 29656
[Clemente] p. 12Definition I` `n(2)natded 29656
[Clemente] p. 13Definition I` `m,n,pnatded 29656
[Clemente] p. 14Proof 5.11natded 29656
[Clemente] p. 14Definition E` `nnatded 29656
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 29658  ex-natded5.2 29657
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 29661  ex-natded5.3 29660
[Clemente] p. 18Theorem 5.5ex-natded5.5 29663
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 29665  ex-natded5.7 29664
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 29667  ex-natded5.8 29666
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 29669  ex-natded5.13 29668
[Clemente] p. 32Definition I` `nnatded 29656
[Clemente] p. 32Definition E` `m,n,p,anatded 29656
[Clemente] p. 32Definition E` `n,tnatded 29656
[Clemente] p. 32Definition I` `n,tnatded 29656
[Clemente] p. 43Theorem 9.20ex-natded9.20 29670
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 29671
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 29673  ex-natded9.26 29672
[Cohen] p. 301Remarkrelogoprlem 26099
[Cohen] p. 301Property 2relogmul 26100  relogmuld 26133
[Cohen] p. 301Property 3relogdiv 26101  relogdivd 26134
[Cohen] p. 301Property 4relogexp 26104
[Cohen] p. 301Property 1alog1 26094
[Cohen] p. 301Property 1bloge 26095
[Cohen4] p. 348Observationrelogbcxpb 26292
[Cohen4] p. 349Propertyrelogbf 26296
[Cohen4] p. 352Definitionelogb 26275
[Cohen4] p. 361Property 2relogbmul 26282
[Cohen4] p. 361Property 3logbrec 26287  relogbdiv 26284
[Cohen4] p. 361Property 4relogbreexp 26280
[Cohen4] p. 361Property 6relogbexp 26285
[Cohen4] p. 361Property 1(a)logbid1 26273
[Cohen4] p. 361Property 1(b)logb1 26274
[Cohen4] p. 367Propertylogbchbase 26276
[Cohen4] p. 377Property 2logblt 26289
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 33284  sxbrsigalem4 33286
[Cohn] p. 81Section II.5acsdomd 18510  acsinfd 18509  acsinfdimd 18511  acsmap2d 18508  acsmapd 18507
[Cohn] p. 143Example 5.1.1sxbrsiga 33289
[Connell] p. 57Definitiondf-scmat 21993  df-scmatalt 47080
[Conway] p. 4Definitionslerec 27320
[Conway] p. 5Definitionaddsval 27446  addsval2 27447  df-adds 27444  df-muls 27563  df-negs 27496
[Conway] p. 7Theorem0slt1s 27330
[Conway] p. 16Theorem 0(i)ssltright 27366
[Conway] p. 16Theorem 0(ii)ssltleft 27365
[Conway] p. 16Theorem 0(iii)slerflex 27266
[Conway] p. 17Theorem 3addsass 27488  addsassd 27489  addscom 27450  addscomd 27451  addsrid 27448  addsridd 27449
[Conway] p. 17Definitiondf-0s 27325
[Conway] p. 17Theorem 4(ii)negnegs 27518
[Conway] p. 17Theorem 4(iii)negsid 27515  negsidd 27516
[Conway] p. 18Theorem 5sleadd1 27472  sleadd1d 27478
[Conway] p. 18Definitiondf-1s 27326
[Conway] p. 18Theorem 6(ii)negscl 27510  negscld 27511
[Conway] p. 18Theorem 6(iii)addscld 27464
[Conway] p. 19Theorem 7addsdi 27610  addsdid 27611  addsdird 27612  mulnegs1d 27615  mulnegs2d 27616  mulsass 27621  mulsassd 27622  mulscom 27595  mulscomd 27596
[Conway] p. 19Theorem 8(i)mulscl 27590  mulscld 27591
[Conway] p. 19Theorem 8(iii)slemuld 27594  sltmul 27592  sltmuld 27593
[Conway] p. 20Theorem 9mulsgt0 27600  mulsgt0d 27601
[Conway] p. 21Theorem 10(iv)precsex 27664
[Conway] p. 29Remarkmadebday 27394  newbday 27396  oldbday 27395
[Conway] p. 29Definitiondf-made 27342  df-new 27344  df-old 27343
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13826
[Crawley] p. 1Definition of posetdf-poset 18266
[Crawley] p. 107Theorem 13.2hlsupr 38257
[Crawley] p. 110Theorem 13.3arglem1N 39061  dalaw 38757
[Crawley] p. 111Theorem 13.4hlathil 40836
[Crawley] p. 111Definition of set Wdf-watsN 38861
[Crawley] p. 111Definition of dilationdf-dilN 38977  df-ldil 38975  isldil 38981
[Crawley] p. 111Definition of translationdf-ltrn 38976  df-trnN 38978  isltrn 38990  ltrnu 38992
[Crawley] p. 112Lemma Acdlema1N 38662  cdlema2N 38663  exatleN 38275
[Crawley] p. 112Lemma B1cvrat 38347  cdlemb 38665  cdlemb2 38912  cdlemb3 39477  idltrn 39021  l1cvat 37925  lhpat 38914  lhpat2 38916  lshpat 37926  ltrnel 39010  ltrnmw 39022
[Crawley] p. 112Lemma Ccdlemc1 39062  cdlemc2 39063  ltrnnidn 39045  trlat 39040  trljat1 39037  trljat2 39038  trljat3 39039  trlne 39056  trlnidat 39044  trlnle 39057
[Crawley] p. 112Definition of automorphismdf-pautN 38862
[Crawley] p. 113Lemma Ccdlemc 39068  cdlemc3 39064  cdlemc4 39065
[Crawley] p. 113Lemma Dcdlemd 39078  cdlemd1 39069  cdlemd2 39070  cdlemd3 39071  cdlemd4 39072  cdlemd5 39073  cdlemd6 39074  cdlemd7 39075  cdlemd8 39076  cdlemd9 39077  cdleme31sde 39256  cdleme31se 39253  cdleme31se2 39254  cdleme31snd 39257  cdleme32a 39312  cdleme32b 39313  cdleme32c 39314  cdleme32d 39315  cdleme32e 39316  cdleme32f 39317  cdleme32fva 39308  cdleme32fva1 39309  cdleme32fvcl 39311  cdleme32le 39318  cdleme48fv 39370  cdleme4gfv 39378  cdleme50eq 39412  cdleme50f 39413  cdleme50f1 39414  cdleme50f1o 39417  cdleme50laut 39418  cdleme50ldil 39419  cdleme50lebi 39411  cdleme50rn 39416  cdleme50rnlem 39415  cdlemeg49le 39382  cdlemeg49lebilem 39410
[Crawley] p. 113Lemma Ecdleme 39431  cdleme00a 39080  cdleme01N 39092  cdleme02N 39093  cdleme0a 39082  cdleme0aa 39081  cdleme0b 39083  cdleme0c 39084  cdleme0cp 39085  cdleme0cq 39086  cdleme0dN 39087  cdleme0e 39088  cdleme0ex1N 39094  cdleme0ex2N 39095  cdleme0fN 39089  cdleme0gN 39090  cdleme0moN 39096  cdleme1 39098  cdleme10 39125  cdleme10tN 39129  cdleme11 39141  cdleme11a 39131  cdleme11c 39132  cdleme11dN 39133  cdleme11e 39134  cdleme11fN 39135  cdleme11g 39136  cdleme11h 39137  cdleme11j 39138  cdleme11k 39139  cdleme11l 39140  cdleme12 39142  cdleme13 39143  cdleme14 39144  cdleme15 39149  cdleme15a 39145  cdleme15b 39146  cdleme15c 39147  cdleme15d 39148  cdleme16 39156  cdleme16aN 39130  cdleme16b 39150  cdleme16c 39151  cdleme16d 39152  cdleme16e 39153  cdleme16f 39154  cdleme16g 39155  cdleme19a 39174  cdleme19b 39175  cdleme19c 39176  cdleme19d 39177  cdleme19e 39178  cdleme19f 39179  cdleme1b 39097  cdleme2 39099  cdleme20aN 39180  cdleme20bN 39181  cdleme20c 39182  cdleme20d 39183  cdleme20e 39184  cdleme20f 39185  cdleme20g 39186  cdleme20h 39187  cdleme20i 39188  cdleme20j 39189  cdleme20k 39190  cdleme20l 39193  cdleme20l1 39191  cdleme20l2 39192  cdleme20m 39194  cdleme20y 39173  cdleme20zN 39172  cdleme21 39208  cdleme21d 39201  cdleme21e 39202  cdleme22a 39211  cdleme22aa 39210  cdleme22b 39212  cdleme22cN 39213  cdleme22d 39214  cdleme22e 39215  cdleme22eALTN 39216  cdleme22f 39217  cdleme22f2 39218  cdleme22g 39219  cdleme23a 39220  cdleme23b 39221  cdleme23c 39222  cdleme26e 39230  cdleme26eALTN 39232  cdleme26ee 39231  cdleme26f 39234  cdleme26f2 39236  cdleme26f2ALTN 39235  cdleme26fALTN 39233  cdleme27N 39240  cdleme27a 39238  cdleme27cl 39237  cdleme28c 39243  cdleme3 39108  cdleme30a 39249  cdleme31fv 39261  cdleme31fv1 39262  cdleme31fv1s 39263  cdleme31fv2 39264  cdleme31id 39265  cdleme31sc 39255  cdleme31sdnN 39258  cdleme31sn 39251  cdleme31sn1 39252  cdleme31sn1c 39259  cdleme31sn2 39260  cdleme31so 39250  cdleme35a 39319  cdleme35b 39321  cdleme35c 39322  cdleme35d 39323  cdleme35e 39324  cdleme35f 39325  cdleme35fnpq 39320  cdleme35g 39326  cdleme35h 39327  cdleme35h2 39328  cdleme35sn2aw 39329  cdleme35sn3a 39330  cdleme36a 39331  cdleme36m 39332  cdleme37m 39333  cdleme38m 39334  cdleme38n 39335  cdleme39a 39336  cdleme39n 39337  cdleme3b 39100  cdleme3c 39101  cdleme3d 39102  cdleme3e 39103  cdleme3fN 39104  cdleme3fa 39107  cdleme3g 39105  cdleme3h 39106  cdleme4 39109  cdleme40m 39338  cdleme40n 39339  cdleme40v 39340  cdleme40w 39341  cdleme41fva11 39348  cdleme41sn3aw 39345  cdleme41sn4aw 39346  cdleme41snaw 39347  cdleme42a 39342  cdleme42b 39349  cdleme42c 39343  cdleme42d 39344  cdleme42e 39350  cdleme42f 39351  cdleme42g 39352  cdleme42h 39353  cdleme42i 39354  cdleme42k 39355  cdleme42ke 39356  cdleme42keg 39357  cdleme42mN 39358  cdleme42mgN 39359  cdleme43aN 39360  cdleme43bN 39361  cdleme43cN 39362  cdleme43dN 39363  cdleme5 39111  cdleme50ex 39430  cdleme50ltrn 39428  cdleme51finvN 39427  cdleme51finvfvN 39426  cdleme51finvtrN 39429  cdleme6 39112  cdleme7 39120  cdleme7a 39114  cdleme7aa 39113  cdleme7b 39115  cdleme7c 39116  cdleme7d 39117  cdleme7e 39118  cdleme7ga 39119  cdleme8 39121  cdleme8tN 39126  cdleme9 39124  cdleme9a 39122  cdleme9b 39123  cdleme9tN 39128  cdleme9taN 39127  cdlemeda 39169  cdlemedb 39168  cdlemednpq 39170  cdlemednuN 39171  cdlemefr27cl 39274  cdlemefr32fva1 39281  cdlemefr32fvaN 39280  cdlemefrs32fva 39271  cdlemefrs32fva1 39272  cdlemefs27cl 39284  cdlemefs32fva1 39294  cdlemefs32fvaN 39293  cdlemesner 39167  cdlemeulpq 39091
[Crawley] p. 114Lemma E4atex 38947  4atexlem7 38946  cdleme0nex 39161  cdleme17a 39157  cdleme17c 39159  cdleme17d 39369  cdleme17d1 39160  cdleme17d2 39366  cdleme18a 39162  cdleme18b 39163  cdleme18c 39164  cdleme18d 39166  cdleme4a 39110
[Crawley] p. 115Lemma Ecdleme21a 39196  cdleme21at 39199  cdleme21b 39197  cdleme21c 39198  cdleme21ct 39200  cdleme21f 39203  cdleme21g 39204  cdleme21h 39205  cdleme21i 39206  cdleme22gb 39165
[Crawley] p. 116Lemma Fcdlemf 39434  cdlemf1 39432  cdlemf2 39433
[Crawley] p. 116Lemma Gcdlemftr1 39438  cdlemg16 39528  cdlemg28 39575  cdlemg28a 39564  cdlemg28b 39574  cdlemg3a 39468  cdlemg42 39600  cdlemg43 39601  cdlemg44 39604  cdlemg44a 39602  cdlemg46 39606  cdlemg47 39607  cdlemg9 39505  ltrnco 39590  ltrncom 39609  tgrpabl 39622  trlco 39598
[Crawley] p. 116Definition of Gdf-tgrp 39614
[Crawley] p. 117Lemma Gcdlemg17 39548  cdlemg17b 39533
[Crawley] p. 117Definition of Edf-edring-rN 39627  df-edring 39628
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 39631
[Crawley] p. 118Remarktendopltp 39651
[Crawley] p. 118Lemma Hcdlemh 39688  cdlemh1 39686  cdlemh2 39687
[Crawley] p. 118Lemma Icdlemi 39691  cdlemi1 39689  cdlemi2 39690
[Crawley] p. 118Lemma Jcdlemj1 39692  cdlemj2 39693  cdlemj3 39694  tendocan 39695
[Crawley] p. 118Lemma Kcdlemk 39845  cdlemk1 39702  cdlemk10 39714  cdlemk11 39720  cdlemk11t 39817  cdlemk11ta 39800  cdlemk11tb 39802  cdlemk11tc 39816  cdlemk11u-2N 39760  cdlemk11u 39742  cdlemk12 39721  cdlemk12u-2N 39761  cdlemk12u 39743  cdlemk13-2N 39747  cdlemk13 39723  cdlemk14-2N 39749  cdlemk14 39725  cdlemk15-2N 39750  cdlemk15 39726  cdlemk16-2N 39751  cdlemk16 39728  cdlemk16a 39727  cdlemk17-2N 39752  cdlemk17 39729  cdlemk18-2N 39757  cdlemk18-3N 39771  cdlemk18 39739  cdlemk19-2N 39758  cdlemk19 39740  cdlemk19u 39841  cdlemk1u 39730  cdlemk2 39703  cdlemk20-2N 39763  cdlemk20 39745  cdlemk21-2N 39762  cdlemk21N 39744  cdlemk22-3 39772  cdlemk22 39764  cdlemk23-3 39773  cdlemk24-3 39774  cdlemk25-3 39775  cdlemk26-3 39777  cdlemk26b-3 39776  cdlemk27-3 39778  cdlemk28-3 39779  cdlemk29-3 39782  cdlemk3 39704  cdlemk30 39765  cdlemk31 39767  cdlemk32 39768  cdlemk33N 39780  cdlemk34 39781  cdlemk35 39783  cdlemk36 39784  cdlemk37 39785  cdlemk38 39786  cdlemk39 39787  cdlemk39u 39839  cdlemk4 39705  cdlemk41 39791  cdlemk42 39812  cdlemk42yN 39815  cdlemk43N 39834  cdlemk45 39818  cdlemk46 39819  cdlemk47 39820  cdlemk48 39821  cdlemk49 39822  cdlemk5 39707  cdlemk50 39823  cdlemk51 39824  cdlemk52 39825  cdlemk53 39828  cdlemk54 39829  cdlemk55 39832  cdlemk55u 39837  cdlemk56 39842  cdlemk5a 39706  cdlemk5auN 39731  cdlemk5u 39732  cdlemk6 39708  cdlemk6u 39733  cdlemk7 39719  cdlemk7u-2N 39759  cdlemk7u 39741  cdlemk8 39709  cdlemk9 39710  cdlemk9bN 39711  cdlemki 39712  cdlemkid 39807  cdlemkj-2N 39753  cdlemkj 39734  cdlemksat 39717  cdlemksel 39716  cdlemksv 39715  cdlemksv2 39718  cdlemkuat 39737  cdlemkuel-2N 39755  cdlemkuel-3 39769  cdlemkuel 39736  cdlemkuv-2N 39754  cdlemkuv2-2 39756  cdlemkuv2-3N 39770  cdlemkuv2 39738  cdlemkuvN 39735  cdlemkvcl 39713  cdlemky 39797  cdlemkyyN 39833  tendoex 39846
[Crawley] p. 120Remarkdva1dim 39856
[Crawley] p. 120Lemma Lcdleml1N 39847  cdleml2N 39848  cdleml3N 39849  cdleml4N 39850  cdleml5N 39851  cdleml6 39852  cdleml7 39853  cdleml8 39854  cdleml9 39855  dia1dim 39932
[Crawley] p. 120Lemma Mdia11N 39919  diaf11N 39920  dialss 39917  diaord 39918  dibf11N 40032  djajN 40008
[Crawley] p. 120Definition of isomorphism mapdiaval 39903
[Crawley] p. 121Lemma Mcdlemm10N 39989  dia2dimlem1 39935  dia2dimlem2 39936  dia2dimlem3 39937  dia2dimlem4 39938  dia2dimlem5 39939  diaf1oN 40001  diarnN 40000  dvheveccl 39983  dvhopN 39987
[Crawley] p. 121Lemma Ncdlemn 40083  cdlemn10 40077  cdlemn11 40082  cdlemn11a 40078  cdlemn11b 40079  cdlemn11c 40080  cdlemn11pre 40081  cdlemn2 40066  cdlemn2a 40067  cdlemn3 40068  cdlemn4 40069  cdlemn4a 40070  cdlemn5 40072  cdlemn5pre 40071  cdlemn6 40073  cdlemn7 40074  cdlemn8 40075  cdlemn9 40076  diclspsn 40065
[Crawley] p. 121Definition of phi(q)df-dic 40044
[Crawley] p. 122Lemma Ndih11 40136  dihf11 40138  dihjust 40088  dihjustlem 40087  dihord 40135  dihord1 40089  dihord10 40094  dihord11b 40093  dihord11c 40095  dihord2 40098  dihord2a 40090  dihord2b 40091  dihord2cN 40092  dihord2pre 40096  dihord2pre2 40097  dihordlem6 40084  dihordlem7 40085  dihordlem7b 40086
[Crawley] p. 122Definition of isomorphism mapdihffval 40101  dihfval 40102  dihval 40103
[Diestel] p. 3Section 1.1df-cusgr 28669  df-nbgr 28590
[Diestel] p. 4Section 1.1df-subgr 28525  uhgrspan1 28560  uhgrspansubgr 28548
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 28811  vtxdgoddnumeven 28810
[Diestel] p. 27Section 1.10df-ushgr 28319
[EGA] p. 80Notation 1.1.1rspecval 32844
[EGA] p. 80Proposition 1.1.2zartop 32856
[EGA] p. 80Proposition 1.1.2(i)zarcls0 32848  zarcls1 32849
[EGA] p. 81Corollary 1.1.8zart0 32859
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 32862
[EGA], p. 83Corollary 1.2.3rhmpreimacn 32865
[Eisenberg] p. 67Definition 5.3df-dif 3952
[Eisenberg] p. 82Definition 6.3dfom3 9642
[Eisenberg] p. 125Definition 8.21df-map 8822
[Eisenberg] p. 216Example 13.2(4)omenps 9650
[Eisenberg] p. 310Theorem 19.8cardprc 9975
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10550
[Enderton] p. 18Axiom of Empty Setaxnul 5306
[Enderton] p. 19Definitiondf-tp 4634
[Enderton] p. 26Exercise 5unissb 4944
[Enderton] p. 26Exercise 10pwel 5380
[Enderton] p. 28Exercise 7(b)pwun 5573
[Enderton] p. 30Theorem "Distributive laws"iinin1 5083  iinin2 5082  iinun2 5077  iunin1 5076  iunin1f 31789  iunin2 5075  uniin1 31783  uniin2 31784
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5081  iundif2 5078
[Enderton] p. 32Exercise 20unineq 4278
[Enderton] p. 33Exercise 23iinuni 5102
[Enderton] p. 33Exercise 25iununi 5103
[Enderton] p. 33Exercise 24(a)iinpw 5110
[Enderton] p. 33Exercise 24(b)iunpw 7758  iunpwss 5111
[Enderton] p. 36Definitionopthwiener 5515
[Enderton] p. 38Exercise 6(a)unipw 5451
[Enderton] p. 38Exercise 6(b)pwuni 4950
[Enderton] p. 41Lemma 3Dopeluu 5471  rnex 7903  rnexg 7895
[Enderton] p. 41Exercise 8dmuni 5915  rnuni 6149
[Enderton] p. 42Definition of a functiondffun7 6576  dffun8 6577
[Enderton] p. 43Definition of function valuefunfv2 6980
[Enderton] p. 43Definition of single-rootedfuncnv 6618
[Enderton] p. 44Definition (d)dfima2 6062  dfima3 6063
[Enderton] p. 47Theorem 3Hfvco2 6989
[Enderton] p. 49Axiom of Choice (first form)ac7 10468  ac7g 10469  df-ac 10111  dfac2 10126  dfac2a 10124  dfac2b 10125  dfac3 10116  dfac7 10127
[Enderton] p. 50Theorem 3K(a)imauni 7245
[Enderton] p. 52Definitiondf-map 8822
[Enderton] p. 53Exercise 21coass 6265
[Enderton] p. 53Exercise 27dmco 6254
[Enderton] p. 53Exercise 14(a)funin 6625
[Enderton] p. 53Exercise 22(a)imass2 6102
[Enderton] p. 54Remarkixpf 8914  ixpssmap 8926
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8892
[Enderton] p. 55Axiom of Choice (second form)ac9 10478  ac9s 10488
[Enderton] p. 56Theorem 3Meqvrelref 37480  erref 8723
[Enderton] p. 57Lemma 3Neqvrelthi 37483  erthi 8754
[Enderton] p. 57Definitiondf-ec 8705
[Enderton] p. 58Definitiondf-qs 8709
[Enderton] p. 61Exercise 35df-ec 8705
[Enderton] p. 65Exercise 56(a)dmun 5911
[Enderton] p. 68Definition of successordf-suc 6371
[Enderton] p. 71Definitiondf-tr 5267  dftr4 5273
[Enderton] p. 72Theorem 4Eunisuc 6444  unisucg 6443
[Enderton] p. 73Exercise 6unisuc 6444  unisucg 6443
[Enderton] p. 73Exercise 5(a)truni 5282
[Enderton] p. 73Exercise 5(b)trint 5284  trintALT 43642
[Enderton] p. 79Theorem 4I(A1)nna0 8604
[Enderton] p. 79Theorem 4I(A2)nnasuc 8606  onasuc 8528
[Enderton] p. 79Definition of operation valuedf-ov 7412
[Enderton] p. 80Theorem 4J(A1)nnm0 8605
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8607  onmsuc 8529
[Enderton] p. 81Theorem 4K(1)nnaass 8622
[Enderton] p. 81Theorem 4K(2)nna0r 8609  nnacom 8617
[Enderton] p. 81Theorem 4K(3)nndi 8623
[Enderton] p. 81Theorem 4K(4)nnmass 8624
[Enderton] p. 81Theorem 4K(5)nnmcom 8626
[Enderton] p. 82Exercise 16nnm0r 8610  nnmsucr 8625
[Enderton] p. 88Exercise 23nnaordex 8638
[Enderton] p. 129Definitiondf-en 8940
[Enderton] p. 132Theorem 6B(b)canth 7362
[Enderton] p. 133Exercise 1xpomen 10010
[Enderton] p. 133Exercise 2qnnen 16156
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9210
[Enderton] p. 135Corollary 6Cphp3 9212
[Enderton] p. 136Corollary 6Enneneq 9209
[Enderton] p. 136Corollary 6D(a)pssinf 9256
[Enderton] p. 136Corollary 6D(b)ominf 9258
[Enderton] p. 137Lemma 6Fpssnn 9168
[Enderton] p. 138Corollary 6Gssfi 9173
[Enderton] p. 139Theorem 6H(c)mapen 9141
[Enderton] p. 142Theorem 6I(3)xpdjuen 10174
[Enderton] p. 142Theorem 6I(4)mapdjuen 10175
[Enderton] p. 143Theorem 6Jdju0en 10170  dju1en 10166
[Enderton] p. 144Exercise 13iunfi 9340  unifi 9341  unifi2 9342
[Enderton] p. 144Corollary 6Kundif2 4477  unfi 9172  unfi2 9315
[Enderton] p. 145Figure 38ffoss 7932
[Enderton] p. 145Definitiondf-dom 8941
[Enderton] p. 146Example 1domen 8957  domeng 8958
[Enderton] p. 146Example 3nndomo 9233  nnsdom 9649  nnsdomg 9302
[Enderton] p. 149Theorem 6L(a)djudom2 10178
[Enderton] p. 149Theorem 6L(c)mapdom1 9142  xpdom1 9071  xpdom1g 9069  xpdom2g 9068
[Enderton] p. 149Theorem 6L(d)mapdom2 9148
[Enderton] p. 151Theorem 6Mzorn 10502  zorng 10499
[Enderton] p. 151Theorem 6M(4)ac8 10487  dfac5 10123
[Enderton] p. 159Theorem 6Qunictb 10570
[Enderton] p. 164Exampleinfdif 10204
[Enderton] p. 168Definitiondf-po 5589
[Enderton] p. 192Theorem 7M(a)oneli 6479
[Enderton] p. 192Theorem 7M(b)ontr1 6411
[Enderton] p. 192Theorem 7M(c)onirri 6478
[Enderton] p. 193Corollary 7N(b)0elon 6419
[Enderton] p. 193Corollary 7N(c)onsuci 7827
[Enderton] p. 193Corollary 7N(d)ssonunii 7768
[Enderton] p. 194Remarkonprc 7765
[Enderton] p. 194Exercise 16suc11 6472
[Enderton] p. 197Definitiondf-card 9934
[Enderton] p. 197Theorem 7Pcarden 10546
[Enderton] p. 200Exercise 25tfis 7844
[Enderton] p. 202Lemma 7Tr1tr 9771
[Enderton] p. 202Definitiondf-r1 9759
[Enderton] p. 202Theorem 7Qr1val1 9781
[Enderton] p. 204Theorem 7V(b)rankval4 9862
[Enderton] p. 206Theorem 7X(b)en2lp 9601
[Enderton] p. 207Exercise 30rankpr 9852  rankprb 9846  rankpw 9838  rankpwi 9818  rankuniss 9861
[Enderton] p. 207Exercise 34opthreg 9613
[Enderton] p. 208Exercise 35suc11reg 9614
[Enderton] p. 212Definition of alephalephval3 10105
[Enderton] p. 213Theorem 8A(a)alephord2 10071
[Enderton] p. 213Theorem 8A(b)cardalephex 10085
[Enderton] p. 218Theorem Schema 8Eonfununi 8341
[Enderton] p. 222Definition of kardkarden 9890  kardex 9889
[Enderton] p. 238Theorem 8Roeoa 8597
[Enderton] p. 238Theorem 8Soeoe 8599
[Enderton] p. 240Exercise 25oarec 8562
[Enderton] p. 257Definition of cofinalitycflm 10245
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17586
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17532
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18506  mrieqv2d 17583  mrieqvd 17582
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17587
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17592  mreexexlem2d 17589
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18512  mreexfidimd 17594
[Frege1879] p. 11Statementdf3or2 42519
[Frege1879] p. 12Statementdf3an2 42520  dfxor4 42517  dfxor5 42518
[Frege1879] p. 26Axiom 1ax-frege1 42541
[Frege1879] p. 26Axiom 2ax-frege2 42542
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 42546
[Frege1879] p. 31Proposition 4frege4 42550
[Frege1879] p. 32Proposition 5frege5 42551
[Frege1879] p. 33Proposition 6frege6 42557
[Frege1879] p. 34Proposition 7frege7 42559
[Frege1879] p. 35Axiom 8ax-frege8 42560  axfrege8 42558
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 36326
[Frege1879] p. 35Proposition 9frege9 42563
[Frege1879] p. 36Proposition 10frege10 42571
[Frege1879] p. 36Proposition 11frege11 42565
[Frege1879] p. 37Proposition 12frege12 42564
[Frege1879] p. 37Proposition 13frege13 42573
[Frege1879] p. 37Proposition 14frege14 42574
[Frege1879] p. 38Proposition 15frege15 42577
[Frege1879] p. 38Proposition 16frege16 42567
[Frege1879] p. 39Proposition 17frege17 42572
[Frege1879] p. 39Proposition 18frege18 42569
[Frege1879] p. 39Proposition 19frege19 42575
[Frege1879] p. 40Proposition 20frege20 42579
[Frege1879] p. 40Proposition 21frege21 42578
[Frege1879] p. 41Proposition 22frege22 42570
[Frege1879] p. 42Proposition 23frege23 42576
[Frege1879] p. 42Proposition 24frege24 42566
[Frege1879] p. 42Proposition 25frege25 42568  rp-frege25 42556
[Frege1879] p. 42Proposition 26frege26 42561
[Frege1879] p. 43Axiom 28ax-frege28 42581
[Frege1879] p. 43Proposition 27frege27 42562
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 42582
[Frege1879] p. 44Axiom 31ax-frege31 42585  axfrege31 42584
[Frege1879] p. 44Proposition 30frege30 42583
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 42586
[Frege1879] p. 44Proposition 33frege33 42587
[Frege1879] p. 45Proposition 34frege34 42588
[Frege1879] p. 45Proposition 35frege35 42589
[Frege1879] p. 45Proposition 36frege36 42590
[Frege1879] p. 46Proposition 37frege37 42591
[Frege1879] p. 46Proposition 38frege38 42592
[Frege1879] p. 46Proposition 39frege39 42593
[Frege1879] p. 46Proposition 40frege40 42594
[Frege1879] p. 47Axiom 41ax-frege41 42596  axfrege41 42595
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 42597
[Frege1879] p. 47Proposition 43frege43 42598
[Frege1879] p. 47Proposition 44frege44 42599
[Frege1879] p. 47Proposition 45frege45 42600
[Frege1879] p. 48Proposition 46frege46 42601
[Frege1879] p. 48Proposition 47frege47 42602
[Frege1879] p. 49Proposition 48frege48 42603
[Frege1879] p. 49Proposition 49frege49 42604
[Frege1879] p. 49Proposition 50frege50 42605
[Frege1879] p. 50Axiom 52ax-frege52a 42608  ax-frege52c 42639  frege52aid 42609  frege52b 42640
[Frege1879] p. 50Axiom 54ax-frege54a 42613  ax-frege54c 42643  frege54b 42644
[Frege1879] p. 50Proposition 51frege51 42606
[Frege1879] p. 50Proposition 52dfsbcq 3780
[Frege1879] p. 50Proposition 53frege53a 42611  frege53aid 42610  frege53b 42641  frege53c 42665
[Frege1879] p. 50Proposition 54biid 261  eqid 2733
[Frege1879] p. 50Proposition 55frege55a 42619  frege55aid 42616  frege55b 42648  frege55c 42669  frege55cor1a 42620  frege55lem2a 42618  frege55lem2b 42647  frege55lem2c 42668
[Frege1879] p. 50Proposition 56frege56a 42622  frege56aid 42621  frege56b 42649  frege56c 42670
[Frege1879] p. 51Axiom 58ax-frege58a 42626  ax-frege58b 42652  frege58bid 42653  frege58c 42672
[Frege1879] p. 51Proposition 57frege57a 42624  frege57aid 42623  frege57b 42650  frege57c 42671
[Frege1879] p. 51Proposition 58spsbc 3791
[Frege1879] p. 51Proposition 59frege59a 42628  frege59b 42655  frege59c 42673
[Frege1879] p. 52Proposition 60frege60a 42629  frege60b 42656  frege60c 42674
[Frege1879] p. 52Proposition 61frege61a 42630  frege61b 42657  frege61c 42675
[Frege1879] p. 52Proposition 62frege62a 42631  frege62b 42658  frege62c 42676
[Frege1879] p. 52Proposition 63frege63a 42632  frege63b 42659  frege63c 42677
[Frege1879] p. 53Proposition 64frege64a 42633  frege64b 42660  frege64c 42678
[Frege1879] p. 53Proposition 65frege65a 42634  frege65b 42661  frege65c 42679
[Frege1879] p. 54Proposition 66frege66a 42635  frege66b 42662  frege66c 42680
[Frege1879] p. 54Proposition 67frege67a 42636  frege67b 42663  frege67c 42681
[Frege1879] p. 54Proposition 68frege68a 42637  frege68b 42664  frege68c 42682
[Frege1879] p. 55Definition 69dffrege69 42683
[Frege1879] p. 58Proposition 70frege70 42684
[Frege1879] p. 59Proposition 71frege71 42685
[Frege1879] p. 59Proposition 72frege72 42686
[Frege1879] p. 59Proposition 73frege73 42687
[Frege1879] p. 60Definition 76dffrege76 42690
[Frege1879] p. 60Proposition 74frege74 42688
[Frege1879] p. 60Proposition 75frege75 42689
[Frege1879] p. 62Proposition 77frege77 42691  frege77d 42497
[Frege1879] p. 63Proposition 78frege78 42692
[Frege1879] p. 63Proposition 79frege79 42693
[Frege1879] p. 63Proposition 80frege80 42694
[Frege1879] p. 63Proposition 81frege81 42695  frege81d 42498
[Frege1879] p. 64Proposition 82frege82 42696
[Frege1879] p. 65Proposition 83frege83 42697  frege83d 42499
[Frege1879] p. 65Proposition 84frege84 42698
[Frege1879] p. 66Proposition 85frege85 42699
[Frege1879] p. 66Proposition 86frege86 42700
[Frege1879] p. 66Proposition 87frege87 42701  frege87d 42501
[Frege1879] p. 67Proposition 88frege88 42702
[Frege1879] p. 68Proposition 89frege89 42703
[Frege1879] p. 68Proposition 90frege90 42704
[Frege1879] p. 68Proposition 91frege91 42705  frege91d 42502
[Frege1879] p. 69Proposition 92frege92 42706
[Frege1879] p. 70Proposition 93frege93 42707
[Frege1879] p. 70Proposition 94frege94 42708
[Frege1879] p. 70Proposition 95frege95 42709
[Frege1879] p. 71Definition 99dffrege99 42713
[Frege1879] p. 71Proposition 96frege96 42710  frege96d 42500
[Frege1879] p. 71Proposition 97frege97 42711  frege97d 42503
[Frege1879] p. 71Proposition 98frege98 42712  frege98d 42504
[Frege1879] p. 72Proposition 100frege100 42714
[Frege1879] p. 72Proposition 101frege101 42715
[Frege1879] p. 72Proposition 102frege102 42716  frege102d 42505
[Frege1879] p. 73Proposition 103frege103 42717
[Frege1879] p. 73Proposition 104frege104 42718
[Frege1879] p. 73Proposition 105frege105 42719
[Frege1879] p. 73Proposition 106frege106 42720  frege106d 42506
[Frege1879] p. 74Proposition 107frege107 42721
[Frege1879] p. 74Proposition 108frege108 42722  frege108d 42507
[Frege1879] p. 74Proposition 109frege109 42723  frege109d 42508
[Frege1879] p. 75Proposition 110frege110 42724
[Frege1879] p. 75Proposition 111frege111 42725  frege111d 42510
[Frege1879] p. 76Proposition 112frege112 42726
[Frege1879] p. 76Proposition 113frege113 42727
[Frege1879] p. 76Proposition 114frege114 42728  frege114d 42509
[Frege1879] p. 77Definition 115dffrege115 42729
[Frege1879] p. 77Proposition 116frege116 42730
[Frege1879] p. 78Proposition 117frege117 42731
[Frege1879] p. 78Proposition 118frege118 42732
[Frege1879] p. 78Proposition 119frege119 42733
[Frege1879] p. 78Proposition 120frege120 42734
[Frege1879] p. 79Proposition 121frege121 42735
[Frege1879] p. 79Proposition 122frege122 42736  frege122d 42511
[Frege1879] p. 79Proposition 123frege123 42737
[Frege1879] p. 80Proposition 124frege124 42738  frege124d 42512
[Frege1879] p. 81Proposition 125frege125 42739
[Frege1879] p. 81Proposition 126frege126 42740  frege126d 42513
[Frege1879] p. 82Proposition 127frege127 42741
[Frege1879] p. 83Proposition 128frege128 42742
[Frege1879] p. 83Proposition 129frege129 42743  frege129d 42514
[Frege1879] p. 84Proposition 130frege130 42744
[Frege1879] p. 85Proposition 131frege131 42745  frege131d 42515
[Frege1879] p. 86Proposition 132frege132 42746
[Frege1879] p. 86Proposition 133frege133 42747  frege133d 42516
[Fremlin1] p. 13Definition 111G (b)df-salgen 45029
[Fremlin1] p. 13Definition 111G (d)borelmbl 45352
[Fremlin1] p. 13Proposition 111G (b)salgenss 45052
[Fremlin1] p. 14Definition 112Aismea 45167
[Fremlin1] p. 15Remark 112B (d)psmeasure 45187
[Fremlin1] p. 15Property 112C (a)meadjun 45178  meadjunre 45192
[Fremlin1] p. 15Property 112C (b)meassle 45179
[Fremlin1] p. 15Property 112C (c)meaunle 45180
[Fremlin1] p. 16Property 112C (d)iundjiun 45176  meaiunle 45185  meaiunlelem 45184
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 45197  meaiuninc2 45198  meaiuninc3 45201  meaiuninc3v 45200  meaiunincf 45199  meaiuninclem 45196
[Fremlin1] p. 16Proposition 112C (f)meaiininc 45203  meaiininc2 45204  meaiininclem 45202
[Fremlin1] p. 19Theorem 113Ccaragen0 45222  caragendifcl 45230  caratheodory 45244  omelesplit 45234
[Fremlin1] p. 19Definition 113Aisome 45210  isomennd 45247  isomenndlem 45246
[Fremlin1] p. 19Remark 113B (c)omeunle 45232
[Fremlin1] p. 19Definition 112Dfcaragencmpl 45251  voncmpl 45337
[Fremlin1] p. 19Definition 113A (ii)omessle 45214
[Fremlin1] p. 20Theorem 113Ccarageniuncl 45239  carageniuncllem1 45237  carageniuncllem2 45238  caragenuncl 45229  caragenuncllem 45228  caragenunicl 45240
[Fremlin1] p. 21Remark 113Dcaragenel2d 45248
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 45242  caratheodorylem2 45243
[Fremlin1] p. 21Exercise 113Xacaragencmpl 45251
[Fremlin1] p. 23Lemma 114Bhoidmv1le 45310  hoidmv1lelem1 45307  hoidmv1lelem2 45308  hoidmv1lelem3 45309
[Fremlin1] p. 25Definition 114Eisvonmbl 45354
[Fremlin1] p. 29Lemma 115Bhoidmv1le 45310  hoidmvle 45316  hoidmvlelem1 45311  hoidmvlelem2 45312  hoidmvlelem3 45313  hoidmvlelem4 45314  hoidmvlelem5 45315  hsphoidmvle2 45301  hsphoif 45292  hsphoival 45295
[Fremlin1] p. 29Definition 1135 (b)hoicvr 45264
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 45272
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 45299  hoidmvn0val 45300  hoidmvval 45293  hoidmvval0 45303  hoidmvval0b 45306
[Fremlin1] p. 30Lemma 115Bhoiprodp1 45304  hsphoidmvle 45302
[Fremlin1] p. 30Definition 115Cdf-ovoln 45253  df-voln 45255
[Fremlin1] p. 30Proposition 115D (a)dmovn 45320  ovn0 45282  ovn0lem 45281  ovnf 45279  ovnome 45289  ovnssle 45277  ovnsslelem 45276  ovnsupge0 45273
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 45319  ovnhoilem1 45317  ovnhoilem2 45318  vonhoi 45383
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 45336  hoidifhspf 45334  hoidifhspval 45324  hoidifhspval2 45331  hoidifhspval3 45335  hspmbl 45345  hspmbllem1 45342  hspmbllem2 45343  hspmbllem3 45344
[Fremlin1] p. 31Definition 115Evoncmpl 45337  vonmea 45290
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 45288  ovnsubadd2 45362  ovnsubadd2lem 45361  ovnsubaddlem1 45286  ovnsubaddlem2 45287
[Fremlin1] p. 32Proposition 115G (a)hoimbl 45347  hoimbl2 45381  hoimbllem 45346  hspdifhsp 45332  opnvonmbl 45350  opnvonmbllem2 45349
[Fremlin1] p. 32Proposition 115G (b)borelmbl 45352
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 45395  iccvonmbllem 45394  ioovonmbl 45393
[Fremlin1] p. 32Proposition 115G (d)vonicc 45401  vonicclem2 45400  vonioo 45398  vonioolem2 45397  vonn0icc 45404  vonn0icc2 45408  vonn0ioo 45403  vonn0ioo2 45406
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 45405  snvonmbl 45402  vonct 45409  vonsn 45407
[Fremlin1] p. 35Lemma 121Asubsalsal 45075
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 45074  subsaliuncllem 45073
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 45441  salpreimalegt 45425  salpreimaltle 45442
[Fremlin1] p. 35Proposition 121B (i)issmf 45444  issmff 45450  issmflem 45443
[Fremlin1] p. 35Proposition 121B (ii)issmfle 45461  issmflelem 45460  smfpreimale 45470
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 45472  issmfgtlem 45471
[Fremlin1] p. 36Definition 121Cdf-smblfn 45412  issmf 45444  issmff 45450  issmfge 45486  issmfgelem 45485  issmfgt 45472  issmfgtlem 45471  issmfle 45461  issmflelem 45460  issmflem 45443
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 45423  salpreimagtlt 45446  salpreimalelt 45445
[Fremlin1] p. 36Proposition 121B (iv)issmfge 45486  issmfgelem 45485
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 45469
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 45467  cnfsmf 45456
[Fremlin1] p. 36Proposition 121D (c)decsmf 45483  decsmflem 45482  incsmf 45458  incsmflem 45457
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 45417  pimconstlt1 45418  smfconst 45465
[Fremlin1] p. 37Proposition 121E (b)smfadd 45481  smfaddlem1 45479  smfaddlem2 45480
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 45512
[Fremlin1] p. 37Proposition 121E (d)smfmul 45511  smfmullem1 45507  smfmullem2 45508  smfmullem3 45509  smfmullem4 45510
[Fremlin1] p. 37Proposition 121E (e)smfdiv 45513
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 45516  smfpimbor1lem2 45515
[Fremlin1] p. 37Proposition 121E (g)smfco 45518
[Fremlin1] p. 37Proposition 121E (h)smfres 45506
[Fremlin1] p. 38Proposition 121E (e)smfrec 45505
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 45514  smfresal 45504
[Fremlin1] p. 38Proposition 121F (a)smflim 45493  smflim2 45522  smflimlem1 45487  smflimlem2 45488  smflimlem3 45489  smflimlem4 45490  smflimlem5 45491  smflimlem6 45492  smflimmpt 45526
[Fremlin1] p. 38Proposition 121F (b)smfsup 45530  smfsuplem1 45527  smfsuplem2 45528  smfsuplem3 45529  smfsupmpt 45531  smfsupxr 45532
[Fremlin1] p. 38Proposition 121F (c)smfinf 45534  smfinflem 45533  smfinfmpt 45535
[Fremlin1] p. 39Remark 121Gsmflim 45493  smflim2 45522  smflimmpt 45526
[Fremlin1] p. 39Proposition 121Fsmfpimcc 45524
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 45554  smfdivdmmbl2 45557  smfinfdmmbl 45565  smfinfdmmbllem 45564  smfsupdmmbl 45561  smfsupdmmbllem 45560
[Fremlin1] p. 39Proposition 121F (d)smflimsup 45544  smflimsuplem2 45537  smflimsuplem6 45541  smflimsuplem7 45542  smflimsuplem8 45543  smflimsupmpt 45545
[Fremlin1] p. 39Proposition 121F (e)smfliminf 45547  smfliminflem 45546  smfliminfmpt 45548
[Fremlin1] p. 80Definition 135E (b)df-smblfn 45412
[Fremlin1], p. 38Proposition 121F (b)fsupdm 45558  fsupdm2 45559
[Fremlin1], p. 39Proposition 121Hadddmmbl 45549  adddmmbl2 45550  finfdm 45562  finfdm2 45563  fsupdm 45558  fsupdm2 45559  muldmmbl 45551  muldmmbl2 45552
[Fremlin1], p. 39Proposition 121F (c)finfdm 45562  finfdm2 45563
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25053
[Fremlin5] p. 213Lemma 565Cauniioovol 25096
[Fremlin5] p. 214Lemma 565Cauniioombl 25106
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 36566
[Fremlin5] p. 220Theorem 565Maftc1anc 36569
[FreydScedrov] p. 283Axiom of Infinityax-inf 9633  inf1 9617  inf2 9618
[Gleason] p. 117Proposition 9-2.1df-enq 10906  enqer 10916
[Gleason] p. 117Proposition 9-2.2df-1nq 10911  df-nq 10907
[Gleason] p. 117Proposition 9-2.3df-plpq 10903  df-plq 10909
[Gleason] p. 119Proposition 9-2.4caovmo 7644  df-mpq 10904  df-mq 10910
[Gleason] p. 119Proposition 9-2.5df-rq 10912
[Gleason] p. 119Proposition 9-2.6ltexnq 10970
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10971  ltbtwnnq 10973
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10966
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10967
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10974
[Gleason] p. 121Definition 9-3.1df-np 10976
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10988
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10990
[Gleason] p. 122Definitiondf-1p 10977
[Gleason] p. 122Remark (1)prub 10989
[Gleason] p. 122Lemma 9-3.4prlem934 11028
[Gleason] p. 122Proposition 9-3.2df-ltp 10980
[Gleason] p. 122Proposition 9-3.3ltsopr 11027  psslinpr 11026  supexpr 11049  suplem1pr 11047  suplem2pr 11048
[Gleason] p. 123Proposition 9-3.5addclpr 11013  addclprlem1 11011  addclprlem2 11012  df-plp 10978
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11017
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11016
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11029
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11038  ltexprlem1 11031  ltexprlem2 11032  ltexprlem3 11033  ltexprlem4 11034  ltexprlem5 11035  ltexprlem6 11036  ltexprlem7 11037
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11040  ltaprlem 11039
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11041
[Gleason] p. 124Lemma 9-3.6prlem936 11042
[Gleason] p. 124Proposition 9-3.7df-mp 10979  mulclpr 11015  mulclprlem 11014  reclem2pr 11043
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11024
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11019
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11018
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11023
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11046  reclem3pr 11044  reclem4pr 11045
[Gleason] p. 126Proposition 9-4.1df-enr 11050  enrer 11058
[Gleason] p. 126Proposition 9-4.2df-0r 11055  df-1r 11056  df-nr 11051
[Gleason] p. 126Proposition 9-4.3df-mr 11053  df-plr 11052  negexsr 11097  recexsr 11102  recexsrlem 11098
[Gleason] p. 127Proposition 9-4.4df-ltr 11054
[Gleason] p. 130Proposition 10-1.3creui 12207  creur 12206  cru 12204
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11183  axcnre 11159
[Gleason] p. 132Definition 10-3.1crim 15062  crimd 15179  crimi 15140  crre 15061  crred 15178  crrei 15139
[Gleason] p. 132Definition 10-3.2remim 15064  remimd 15145
[Gleason] p. 133Definition 10.36absval2 15231  absval2d 15392  absval2i 15344
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15088  cjaddd 15167  cjaddi 15135
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15089  cjmuld 15168  cjmuli 15136
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15087  cjcjd 15146  cjcji 15118
[Gleason] p. 133Proposition 10-3.4(f)cjre 15086  cjreb 15070  cjrebd 15149  cjrebi 15121  cjred 15173  rere 15069  rereb 15067  rerebd 15148  rerebi 15120  rered 15171
[Gleason] p. 133Proposition 10-3.4(h)addcj 15095  addcjd 15159  addcji 15130
[Gleason] p. 133Proposition 10-3.7(a)absval 15185
[Gleason] p. 133Proposition 10-3.7(b)abscj 15226  abscjd 15397  abscji 15348
[Gleason] p. 133Proposition 10-3.7(c)abs00 15236  abs00d 15393  abs00i 15345  absne0d 15394
[Gleason] p. 133Proposition 10-3.7(d)releabs 15268  releabsd 15398  releabsi 15349
[Gleason] p. 133Proposition 10-3.7(f)absmul 15241  absmuld 15401  absmuli 15351
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15229  sqabsaddi 15352
[Gleason] p. 133Proposition 10-3.7(h)abstri 15277  abstrid 15403  abstrii 15355
[Gleason] p. 134Definition 10-4.1df-exp 14028  exp0 14031  expp1 14034  expp1d 14112
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26187  cxpaddd 26225  expadd 14070  expaddd 14113  expaddz 14072
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26196  cxpmuld 26245  expmul 14073  expmuld 14114  expmulz 14074
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26193  mulcxpd 26236  mulexp 14067  mulexpd 14126  mulexpz 14068
[Gleason] p. 140Exercise 1znnen 16155
[Gleason] p. 141Definition 11-2.1fzval 13486
[Gleason] p. 168Proposition 12-2.1(a)climadd 15576  rlimadd 15587  rlimdiv 15592
[Gleason] p. 168Proposition 12-2.1(b)climsub 15578  rlimsub 15589
[Gleason] p. 168Proposition 12-2.1(c)climmul 15577  rlimmul 15590
[Gleason] p. 171Corollary 12-2.2climmulc2 15581
[Gleason] p. 172Corollary 12-2.5climrecl 15527
[Gleason] p. 172Proposition 12-2.4(c)climabs 15548  climcj 15549  climim 15551  climre 15550  rlimabs 15553  rlimcj 15554  rlimim 15556  rlimre 15555
[Gleason] p. 173Definition 12-3.1df-ltxr 11253  df-xr 11252  ltxr 13095
[Gleason] p. 175Definition 12-4.1df-limsup 15415  limsupval 15418
[Gleason] p. 180Theorem 12-5.1climsup 15616
[Gleason] p. 180Theorem 12-5.3caucvg 15625  caucvgb 15626  caucvgbf 44200  caucvgr 15622  climcau 15617
[Gleason] p. 182Exercise 3cvgcmp 15762
[Gleason] p. 182Exercise 4cvgrat 15829
[Gleason] p. 195Theorem 13-2.12abs1m 15282
[Gleason] p. 217Lemma 13-4.1btwnzge0 13793
[Gleason] p. 223Definition 14-1.1df-met 20938
[Gleason] p. 223Definition 14-1.1(a)met0 23849  xmet0 23848
[Gleason] p. 223Definition 14-1.1(b)metgt0 23865
[Gleason] p. 223Definition 14-1.1(c)metsym 23856
[Gleason] p. 223Definition 14-1.1(d)mettri 23858  mstri 23975  xmettri 23857  xmstri 23974
[Gleason] p. 225Definition 14-1.5xpsmet 23888
[Gleason] p. 230Proposition 14-2.6txlm 23152
[Gleason] p. 240Theorem 14-4.3metcnp4 24827
[Gleason] p. 240Proposition 14-4.2metcnp3 24049
[Gleason] p. 243Proposition 14-4.16addcn 24381  addcn2 15538  mulcn 24383  mulcn2 15540  subcn 24382  subcn2 15539
[Gleason] p. 295Remarkbcval3 14266  bcval4 14267
[Gleason] p. 295Equation 2bcpasc 14281
[Gleason] p. 295Definition of binomial coefficientbcval 14264  df-bc 14263
[Gleason] p. 296Remarkbcn0 14270  bcnn 14272
[Gleason] p. 296Theorem 15-2.8binom 15776
[Gleason] p. 308Equation 2ef0 16034
[Gleason] p. 308Equation 3efcj 16035
[Gleason] p. 309Corollary 15-4.3efne0 16040
[Gleason] p. 309Corollary 15-4.4efexp 16044
[Gleason] p. 310Equation 14sinadd 16107
[Gleason] p. 310Equation 15cosadd 16108
[Gleason] p. 311Equation 17sincossq 16119
[Gleason] p. 311Equation 18cosbnd 16124  sinbnd 16123
[Gleason] p. 311Lemma 15-4.7sqeqor 14180  sqeqori 14178
[Gleason] p. 311Definition of ` `df-pi 16016
[Godowski] p. 730Equation SFgoeqi 31526
[GodowskiGreechie] p. 249Equation IV3oai 30921
[Golan] p. 1Remarksrgisid 20032
[Golan] p. 1Definitiondf-srg 20010
[Golan] p. 149Definitiondf-slmd 32346
[Gonshor] p. 7Definitiondf-scut 27285
[Gonshor] p. 9Theorem 2.5slerec 27320
[Gonshor] p. 10Theorem 2.6cofcut1 27407  cofcut1d 27408
[Gonshor] p. 10Theorem 2.7cofcut2 27409  cofcut2d 27410
[Gonshor] p. 12Theorem 2.9cofcutr 27411  cofcutr1d 27412  cofcutr2d 27413
[Gonshor] p. 13Definitiondf-adds 27444
[Gonshor] p. 14Theorem 3.1addsprop 27460
[Gonshor] p. 15Theorem 3.2addsunif 27485
[Gonshor] p. 17Theorem 3.4mulsprop 27586
[Gonshor] p. 18Theorem 3.5mulsunif 27605
[GramKnuthPat], p. 47Definition 2.42df-fwddif 35131
[Gratzer] p. 23Section 0.6df-mre 17530
[Gratzer] p. 27Section 0.6df-mri 17532
[Hall] p. 1Section 1.1df-asslaw 46598  df-cllaw 46596  df-comlaw 46597
[Hall] p. 2Section 1.2df-clintop 46610
[Hall] p. 7Section 1.3df-sgrp2 46631
[Halmos] p. 28Partition ` `df-parts 37635  dfmembpart2 37640
[Halmos] p. 31Theorem 17.3riesz1 31318  riesz2 31319
[Halmos] p. 41Definition of Hermitianhmopadj2 31194
[Halmos] p. 42Definition of projector orderingpjordi 31426
[Halmos] p. 43Theorem 26.1elpjhmop 31438  elpjidm 31437  pjnmopi 31401
[Halmos] p. 44Remarkpjinormi 30940  pjinormii 30929
[Halmos] p. 44Theorem 26.2elpjch 31442  pjrn 30960  pjrni 30955  pjvec 30949
[Halmos] p. 44Theorem 26.3pjnorm2 30980
[Halmos] p. 44Theorem 26.4hmopidmpj 31407  hmopidmpji 31405
[Halmos] p. 45Theorem 27.1pjinvari 31444
[Halmos] p. 45Theorem 27.3pjoci 31433  pjocvec 30950
[Halmos] p. 45Theorem 27.4pjorthcoi 31422
[Halmos] p. 48Theorem 29.2pjssposi 31425
[Halmos] p. 48Theorem 29.3pjssdif1i 31428  pjssdif2i 31427
[Halmos] p. 50Definition of spectrumdf-spec 31108
[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 1798
[Hatcher] p. 25Definitiondf-phtpc 24508  df-phtpy 24487
[Hatcher] p. 26Definitiondf-pco 24521  df-pi1 24524
[Hatcher] p. 26Proposition 1.2phtpcer 24511
[Hatcher] p. 26Proposition 1.3pi1grp 24566
[Hefferon] p. 240Definition 3.12df-dmat 21992  df-dmatalt 47079
[Helfgott] p. 2Theoremtgoldbach 46485
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 46470
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 46482  bgoldbtbnd 46477  bgoldbtbnd 46477  tgblthelfgott 46483
[Helfgott] p. 5Proposition 1.1circlevma 33654
[Helfgott] p. 69Statement 7.49circlemethhgt 33655
[Helfgott] p. 69Statement 7.50hgt750lema 33669  hgt750lemb 33668  hgt750leme 33670  hgt750lemf 33665  hgt750lemg 33666
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 46479  tgoldbachgt 33675  tgoldbachgtALTV 46480  tgoldbachgtd 33674
[Helfgott] p. 70Statement 7.49ax-hgt749 33656
[Herstein] p. 54Exercise 28df-grpo 29746
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18830  grpoideu 29762  mndideu 18636
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18859  grpoinveu 29772
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18890  grpo2inv 29784
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18901  grpoinvop 29786
[Herstein] p. 57Exercise 1dfgrp3e 18923
[Hitchcock] p. 5Rule A3mptnan 1771
[Hitchcock] p. 5Rule A4mptxor 1772
[Hitchcock] p. 5Rule A5mtpxor 1774
[Holland] p. 1519Theorem 2sumdmdi 31673
[Holland] p. 1520Lemma 5cdj1i 31686  cdj3i 31694  cdj3lem1 31687  cdjreui 31685
[Holland] p. 1524Lemma 7mddmdin0i 31684
[Holland95] p. 13Theorem 3.6hlathil 40836
[Holland95] p. 14Line 15hgmapvs 40762
[Holland95] p. 14Line 16hdmaplkr 40784
[Holland95] p. 14Line 17hdmapellkr 40785
[Holland95] p. 14Line 19hdmapglnm2 40782
[Holland95] p. 14Line 20hdmapip0com 40788
[Holland95] p. 14Theorem 3.6hdmapevec2 40707
[Holland95] p. 14Lines 24 and 25hdmapoc 40802
[Holland95] p. 204Definition of involutiondf-srng 20454
[Holland95] p. 212Definition of subspacedf-psubsp 38374
[Holland95] p. 214Lemma 3.3lclkrlem2v 40399
[Holland95] p. 214Definition 3.2df-lpolN 40352
[Holland95] p. 214Definition of nonsingularpnonsingN 38804
[Holland95] p. 215Lemma 3.3(1)dihoml4 40248  poml4N 38824
[Holland95] p. 215Lemma 3.3(2)dochexmid 40339  pexmidALTN 38849  pexmidN 38840
[Holland95] p. 218Theorem 3.6lclkr 40404
[Holland95] p. 218Definition of dual vector spacedf-ldual 37994  ldualset 37995
[Holland95] p. 222Item 1df-lines 38372  df-pointsN 38373
[Holland95] p. 222Item 2df-polarityN 38774
[Holland95] p. 223Remarkispsubcl2N 38818  omllaw4 38116  pol1N 38781  polcon3N 38788
[Holland95] p. 223Definitiondf-psubclN 38806
[Holland95] p. 223Equation for polaritypolval2N 38777
[Holmes] p. 40Definitiondf-xrn 37241
[Hughes] p. 44Equation 1.21bax-his3 30337
[Hughes] p. 47Definition of projection operatordfpjop 31435
[Hughes] p. 49Equation 1.30eighmre 31216  eigre 31088  eigrei 31087
[Hughes] p. 49Equation 1.31eighmorth 31217  eigorth 31091  eigorthi 31090
[Hughes] p. 137Remark (ii)eigposi 31089
[Huneke] p. 1Claim 1frgrncvvdeq 29562
[Huneke] p. 1Statement 1frgrncvvdeqlem7 29558
[Huneke] p. 1Statement 2frgrncvvdeqlem8 29559
[Huneke] p. 1Statement 3frgrncvvdeqlem9 29560
[Huneke] p. 2Claim 2frgrregorufr 29578  frgrregorufr0 29577  frgrregorufrg 29579
[Huneke] p. 2Claim 3frgrhash2wsp 29585  frrusgrord 29594  frrusgrord0 29593
[Huneke] p. 2Statementdf-clwwlknon 29341
[Huneke] p. 2Statement 4frgrwopreglem4 29568
[Huneke] p. 2Statement 5frgrwopreg1 29571  frgrwopreg2 29572  frgrwopregasn 29569  frgrwopregbsn 29570
[Huneke] p. 2Statement 6frgrwopreglem5 29574
[Huneke] p. 2Statement 7fusgreghash2wspv 29588
[Huneke] p. 2Statement 8fusgreghash2wsp 29591
[Huneke] p. 2Statement 9clwlksndivn 29339  numclwlk1 29624  numclwlk1lem1 29622  numclwlk1lem2 29623  numclwwlk1 29614  numclwwlk8 29645
[Huneke] p. 2Definition 3frgrwopreglem1 29565
[Huneke] p. 2Definition 4df-clwlks 29028
[Huneke] p. 2Definition 62clwwlk 29600
[Huneke] p. 2Definition 7numclwwlkovh 29626  numclwwlkovh0 29625
[Huneke] p. 2Statement 10numclwwlk2 29634
[Huneke] p. 2Statement 11rusgrnumwlkg 29231
[Huneke] p. 2Statement 12numclwwlk3 29638
[Huneke] p. 2Statement 13numclwwlk5 29641
[Huneke] p. 2Statement 14numclwwlk7 29644
[Indrzejczak] p. 33Definition ` `Enatded 29656  natded 29656
[Indrzejczak] p. 33Definition ` `Inatded 29656
[Indrzejczak] p. 34Definition ` `Enatded 29656  natded 29656
[Indrzejczak] p. 34Definition ` `Inatded 29656
[Jech] p. 4Definition of classcv 1541  cvjust 2727
[Jech] p. 42Lemma 6.1alephexp1 10574
[Jech] p. 42Equation 6.1alephadd 10572  alephmul 10573
[Jech] p. 43Lemma 6.2infmap 10571  infmap2 10213
[Jech] p. 71Lemma 9.3jech9.3 9809
[Jech] p. 72Equation 9.3scott0 9881  scottex 9880
[Jech] p. 72Exercise 9.1rankval4 9862
[Jech] p. 72Scheme "Collection Principle"cp 9886
[Jech] p. 78Noteopthprc 5741
[JonesMatijasevic] p. 694Definition 2.3rmxyval 41654
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 41742
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 41743
[JonesMatijasevic] p. 695Equation 2.7rmxadd 41666
[JonesMatijasevic] p. 695Equation 2.8rmyadd 41670
[JonesMatijasevic] p. 695Equation 2.9rmxp1 41671  rmyp1 41672
[JonesMatijasevic] p. 695Equation 2.10rmxm1 41673  rmym1 41674
[JonesMatijasevic] p. 695Equation 2.11rmx0 41664  rmx1 41665  rmxluc 41675
[JonesMatijasevic] p. 695Equation 2.12rmy0 41668  rmy1 41669  rmyluc 41676
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 41678
[JonesMatijasevic] p. 695Equation 2.14rmydbl 41679
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 41699  jm2.17b 41700  jm2.17c 41701
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 41732
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 41736
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 41727
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 41702  jm2.24nn 41698
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 41741
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 41747  rmygeid 41703
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 41759
[Juillerat] p. 11Section *5etransc 44999  etransclem47 44997  etransclem48 44998
[Juillerat] p. 12Equation (7)etransclem44 44994
[Juillerat] p. 12Equation *(7)etransclem46 44996
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 44982
[Juillerat] p. 13Proofetransclem35 44985
[Juillerat] p. 13Part of case 2 proven inetransclem38 44988
[Juillerat] p. 13Part of case 2 provenetransclem24 44974
[Juillerat] p. 13Part of case 2: proven inetransclem41 44991
[Juillerat] p. 14Proofetransclem23 44973
[KalishMontague] p. 81Note 1ax-6 1972
[KalishMontague] p. 85Lemma 2equid 2016
[KalishMontague] p. 85Lemma 3equcomi 2021
[KalishMontague] p. 86Lemma 7cbvalivw 2011  cbvaliw 2010  wl-cbvmotv 36382  wl-motae 36384  wl-moteq 36383
[KalishMontague] p. 87Lemma 8spimvw 2000  spimw 1975
[KalishMontague] p. 87Lemma 9spfw 2037  spw 2038
[Kalmbach] p. 14Definition of latticechabs1 30769  chabs1i 30771  chabs2 30770  chabs2i 30772  chjass 30786  chjassi 30739  latabs1 18428  latabs2 18429
[Kalmbach] p. 15Definition of atomdf-at 31591  ela 31592
[Kalmbach] p. 15Definition of coverscvbr2 31536  cvrval2 38144
[Kalmbach] p. 16Definitiondf-ol 38048  df-oml 38049
[Kalmbach] p. 20Definition of commutescmbr 30837  cmbri 30843  cmtvalN 38081  df-cm 30836  df-cmtN 38047
[Kalmbach] p. 22Remarkomllaw5N 38117  pjoml5 30866  pjoml5i 30841
[Kalmbach] p. 22Definitionpjoml2 30864  pjoml2i 30838
[Kalmbach] p. 22Theorem 2(v)cmcm 30867  cmcmi 30845  cmcmii 30850  cmtcomN 38119
[Kalmbach] p. 22Theorem 2(ii)omllaw3 38115  omlsi 30657  pjoml 30689  pjomli 30688
[Kalmbach] p. 22Definition of OML lawomllaw2N 38114
[Kalmbach] p. 23Remarkcmbr2i 30849  cmcm3 30868  cmcm3i 30847  cmcm3ii 30852  cmcm4i 30848  cmt3N 38121  cmt4N 38122  cmtbr2N 38123
[Kalmbach] p. 23Lemma 3cmbr3 30861  cmbr3i 30853  cmtbr3N 38124
[Kalmbach] p. 25Theorem 5fh1 30871  fh1i 30874  fh2 30872  fh2i 30875  omlfh1N 38128
[Kalmbach] p. 65Remarkchjatom 31610  chslej 30751  chsleji 30711  shslej 30633  shsleji 30623
[Kalmbach] p. 65Proposition 1chocin 30748  chocini 30707  chsupcl 30593  chsupval2 30663  h0elch 30508  helch 30496  hsupval2 30662  ocin 30549  ococss 30546  shococss 30547
[Kalmbach] p. 65Definition of subspace sumshsval 30565
[Kalmbach] p. 66Remarkdf-pjh 30648  pjssmi 31418  pjssmii 30934
[Kalmbach] p. 67Lemma 3osum 30898  osumi 30895
[Kalmbach] p. 67Lemma 4pjci 31453
[Kalmbach] p. 103Exercise 6atmd2 31653
[Kalmbach] p. 103Exercise 12mdsl0 31563
[Kalmbach] p. 140Remarkhatomic 31613  hatomici 31612  hatomistici 31615
[Kalmbach] p. 140Proposition 1atlatmstc 38189
[Kalmbach] p. 140Proposition 1(i)atexch 31634  lsatexch 37913
[Kalmbach] p. 140Proposition 1(ii)chcv1 31608  cvlcvr1 38209  cvr1 38281
[Kalmbach] p. 140Proposition 1(iii)cvexch 31627  cvexchi 31622  cvrexch 38291
[Kalmbach] p. 149Remark 2chrelati 31617  hlrelat 38273  hlrelat5N 38272  lrelat 37884
[Kalmbach] p. 153Exercise 5lsmcv 20754  lsmsatcv 37880  spansncv 30906  spansncvi 30905
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 37899  spansncv2 31546
[Kalmbach] p. 266Definitiondf-st 31464
[Kalmbach2] p. 8Definition of adjointdf-adjh 31102
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10641  fpwwe2 10638
[KanamoriPincus] p. 416Corollary 1.3canth4 10642
[KanamoriPincus] p. 417Corollary 1.6canthp1 10649
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10644
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10646
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10659
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10663  gchxpidm 10664
[KanamoriPincus] p. 419Theorem 2.1gchacg 10675  gchhar 10674
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10211  unxpwdom 9584
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10665
[Kreyszig] p. 3Property M1metcl 23838  xmetcl 23837
[Kreyszig] p. 4Property M2meteq0 23845
[Kreyszig] p. 8Definition 1.1-8dscmet 24081
[Kreyszig] p. 12Equation 5conjmul 11931  muleqadd 11858
[Kreyszig] p. 18Definition 1.3-2mopnval 23944
[Kreyszig] p. 19Remarkmopntopon 23945
[Kreyszig] p. 19Theorem T1mopn0 24007  mopnm 23950
[Kreyszig] p. 19Theorem T2unimopn 24005
[Kreyszig] p. 19Definition of neighborhoodneibl 24010
[Kreyszig] p. 20Definition 1.3-3metcnp2 24051
[Kreyszig] p. 25Definition 1.4-1lmbr 22762  lmmbr 24775  lmmbr2 24776
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 22884
[Kreyszig] p. 28Theorem 1.4-5lmcau 24830
[Kreyszig] p. 28Definition 1.4-3iscau 24793  iscmet2 24811
[Kreyszig] p. 30Theorem 1.4-7cmetss 24833
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 22965  metelcls 24822
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 24823  metcld2 24824
[Kreyszig] p. 51Equation 2clmvneg1 24615  lmodvneg1 20515  nvinv 29892  vcm 29829
[Kreyszig] p. 51Equation 1aclm0vs 24611  lmod0vs 20505  slmd0vs 32369  vc0 29827
[Kreyszig] p. 51Equation 1blmodvs0 20506  slmdvs0 32370  vcz 29828
[Kreyszig] p. 58Definition 2.2-1imsmet 29944  ngpmet 24112  nrmmetd 24083
[Kreyszig] p. 59Equation 1imsdval 29939  imsdval2 29940  ncvspds 24678  ngpds 24113
[Kreyszig] p. 63Problem 1nmval 24098  nvnd 29941
[Kreyszig] p. 64Problem 2nmeq0 24127  nmge0 24126  nvge0 29926  nvz 29922
[Kreyszig] p. 64Problem 3nmrtri 24133  nvabs 29925
[Kreyszig] p. 91Definition 2.7-1isblo3i 30054
[Kreyszig] p. 92Equation 2df-nmoo 29998
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30060  blocni 30058
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30059
[Kreyszig] p. 129Definition 3.1-1cphipeq0 24721  ipeq0 21191  ipz 29972
[Kreyszig] p. 135Problem 2cphpyth 24733  pythi 30103
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30107
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 24755
[Kreyszig] p. 144Equation 4supcvg 15802
[Kreyszig] p. 144Theorem 3.3-1minvec 24953  minveco 30137
[Kreyszig] p. 196Definition 3.9-1df-aj 30003
[Kreyszig] p. 247Theorem 4.7-2bcth 24846
[Kreyszig] p. 249Theorem 4.7-3ubth 30126
[Kreyszig] p. 470Definition of positive operator orderingleop 31376  leopg 31375
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 31394
[Kreyszig] p. 525Theorem 10.1-1htth 30171
[Kulpa] p. 547Theorempoimir 36521
[Kulpa] p. 547Equation (1)poimirlem32 36520
[Kulpa] p. 547Equation (2)poimirlem31 36519
[Kulpa] p. 548Theorembroucube 36522
[Kulpa] p. 548Equation (6)poimirlem26 36514
[Kulpa] p. 548Equation (7)poimirlem27 36515
[Kunen] p. 10Axiom 0ax6e 2383  axnul 5306
[Kunen] p. 11Axiom 3axnul 5306
[Kunen] p. 12Axiom 6zfrep6 7941
[Kunen] p. 24Definition 10.24mapval 8832  mapvalg 8830
[Kunen] p. 30Lemma 10.20fodomg 10517
[Kunen] p. 31Definition 10.24mapex 8826
[Kunen] p. 95Definition 2.1df-r1 9759
[Kunen] p. 97Lemma 2.10r1elss 9801  r1elssi 9800
[Kunen] p. 107Exercise 4rankop 9853  rankopb 9847  rankuni 9858  rankxplim 9874  rankxpsuc 9877
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 5010
[Lang] , p. 225Corollary 1.3finexttrb 32741
[Lang] p. Definitiondf-rn 5688
[Lang] p. 3Statementlidrideqd 18588  mndbn0 18641
[Lang] p. 3Definitiondf-mnd 18626
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18606
[Lang] p. 4Property of composites. Second formulagsumccat 18722
[Lang] p. 5Equationgsumreidx 19785
[Lang] p. 5Definition of an (infinite) productgsumfsupp 46592
[Lang] p. 6Examplenn0mnd 46589
[Lang] p. 6Equationgsumxp2 19848
[Lang] p. 6Statementcycsubm 19079
[Lang] p. 6Definitionmulgnn0gsum 18960
[Lang] p. 6Observationmndlsmidm 19538
[Lang] p. 7Definitiondfgrp2e 18848
[Lang] p. 30Definitiondf-tocyc 32266
[Lang] p. 32Property (a)cyc3genpm 32311
[Lang] p. 32Property (b)cyc3conja 32316  cycpmconjv 32301
[Lang] p. 53Definitiondf-cat 17612
[Lang] p. 53Axiom CAT 1cat1 18047  cat1lem 18046
[Lang] p. 54Definitiondf-iso 17696
[Lang] p. 57Definitiondf-inito 17934  df-termo 17935
[Lang] p. 58Exampleirinitoringc 46967
[Lang] p. 58Statementinitoeu1 17961  termoeu1 17968
[Lang] p. 62Definitiondf-func 17808
[Lang] p. 65Definitiondf-nat 17894
[Lang] p. 91Notedf-ringc 46903
[Lang] p. 92Statementmxidlprm 32586
[Lang] p. 92Definitionisprmidlc 32566
[Lang] p. 128Remarkdsmmlmod 21300
[Lang] p. 129Prooflincscm 47111  lincscmcl 47113  lincsum 47110  lincsumcl 47112
[Lang] p. 129Statementlincolss 47115
[Lang] p. 129Observationdsmmfi 21293
[Lang] p. 141Theorem 5.3dimkerim 32712  qusdimsum 32713
[Lang] p. 141Corollary 5.4lssdimle 32692
[Lang] p. 147Definitionsnlindsntor 47152
[Lang] p. 504Statementmat1 21949  matring 21945
[Lang] p. 504Definitiondf-mamu 21886
[Lang] p. 505Statementmamuass 21902  mamutpos 21960  matassa 21946  mattposvs 21957  tposmap 21959
[Lang] p. 513Definitionmdet1 22103  mdetf 22097
[Lang] p. 513Theorem 4.4cramer 22193
[Lang] p. 514Proposition 4.6mdetleib 22089
[Lang] p. 514Proposition 4.8mdettpos 22113
[Lang] p. 515Definitiondf-minmar1 22137  smadiadetr 22177
[Lang] p. 515Corollary 4.9mdetero 22112  mdetralt 22110
[Lang] p. 517Proposition 4.15mdetmul 22125
[Lang] p. 518Definitiondf-madu 22136
[Lang] p. 518Proposition 4.16madulid 22147  madurid 22146  matinv 22179
[Lang] p. 561Theorem 3.1cayleyhamilton 22392
[Lang], p. 224Proposition 1.2extdgmul 32740  fedgmul 32716
[Lang], p. 561Remarkchpmatply1 22334
[Lang], p. 561Definitiondf-chpmat 22329
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 43093
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 43088
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 43094
[LeBlanc] p. 277Rule R2axnul 5306
[Levy] p. 12Axiom 4.3.1df-clab 2711
[Levy] p. 59Definitiondf-ttrcl 9703
[Levy] p. 64Theorem 5.6(ii)frinsg 9746
[Levy] p. 338Axiomdf-clel 2811  df-cleq 2725
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2811  df-cleq 2725
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2711
[Levy] p. 358Axiomdf-clab 2711
[Levy58] p. 2Definition Iisfin1-3 10381
[Levy58] p. 2Definition IIdf-fin2 10281
[Levy58] p. 2Definition Iadf-fin1a 10280
[Levy58] p. 2Definition IIIdf-fin3 10283
[Levy58] p. 3Definition Vdf-fin5 10284
[Levy58] p. 3Definition IVdf-fin4 10282
[Levy58] p. 4Definition VIdf-fin6 10285
[Levy58] p. 4Definition VIIdf-fin7 10286
[Levy58], p. 3Theorem 1fin1a2 10410
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27189
[Lipparini] p. 3Lemma 2.1.4noresle 27200
[Lipparini] p. 6Proposition 4.2noinfbnd1 27232  nosupbnd1 27217
[Lipparini] p. 6Proposition 4.3noinfbnd2 27234  nosupbnd2 27219
[Lipparini] p. 7Theorem 5.1noetasuplem3 27238  noetasuplem4 27239
[Lipparini] p. 7Corollary 4.4nosupinfsep 27235
[Lopez-Astorga] p. 12Rule 1mptnan 1771
[Lopez-Astorga] p. 12Rule 2mptxor 1772
[Lopez-Astorga] p. 12Rule 3mtpxor 1774
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 31661
[Maeda] p. 168Lemma 5mdsym 31665  mdsymi 31664
[Maeda] p. 168Lemma 4(i)mdsymlem4 31659  mdsymlem6 31661  mdsymlem7 31662
[Maeda] p. 168Lemma 4(ii)mdsymlem8 31663
[MaedaMaeda] p. 1Remarkssdmd1 31566  ssdmd2 31567  ssmd1 31564  ssmd2 31565
[MaedaMaeda] p. 1Lemma 1.2mddmd2 31562
[MaedaMaeda] p. 1Definition 1.1df-dmd 31534  df-md 31533  mdbr 31547
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 31584  mdslj1i 31572  mdslj2i 31573  mdslle1i 31570  mdslle2i 31571  mdslmd1i 31582  mdslmd2i 31583
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 31574  mdsl2bi 31576  mdsl2i 31575
[MaedaMaeda] p. 2Lemma 1.6mdexchi 31588
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 31585
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 31586
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 31563
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 31568  mdsl3 31569
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 31587
[MaedaMaeda] p. 4Theorem 1.14mdcompli 31682
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 38191  hlrelat1 38271
[MaedaMaeda] p. 31Lemma 7.5lcvexch 37909
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 31589  cvmdi 31577  cvnbtwn4 31542  cvrnbtwn4 38149
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 31590
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 38210  cvp 31628  cvrp 38287  lcvp 37910
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 31652
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 31651
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 38203  hlexch4N 38263
[MaedaMaeda] p. 34Exercise 7.1atabsi 31654
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 38314
[MaedaMaeda] p. 61Definition 15.10psubN 38620  atpsubN 38624  df-pointsN 38373  pointpsubN 38622
[MaedaMaeda] p. 62Theorem 15.5df-pmap 38375  pmap11 38633  pmaple 38632  pmapsub 38639  pmapval 38628
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 38636  pmap1N 38638
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 38641  pmapglb2N 38642  pmapglb2xN 38643  pmapglbx 38640
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 38723
[MaedaMaeda] p. 67Postulate PS1ps-1 38348
[MaedaMaeda] p. 68Lemma 16.2df-padd 38667  paddclN 38713  paddidm 38712
[MaedaMaeda] p. 68Condition PS2ps-2 38349
[MaedaMaeda] p. 68Equation 16.2.1paddass 38709
[MaedaMaeda] p. 69Lemma 16.4ps-1 38348
[MaedaMaeda] p. 69Theorem 16.4ps-2 38349
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19543  lsmmod2 19544  lssats 37882  shatomici 31611  shatomistici 31614  shmodi 30643  shmodsi 30642
[MaedaMaeda] p. 130Remark 29.6dmdmd 31553  mdsymlem7 31662
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 30842
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 30746
[MaedaMaeda] p. 139Remarksumdmdii 31668
[Margaris] p. 40Rule Cexlimiv 1934
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 398  df-ex 1783  df-or 847  dfbi2 476
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 29653
[Margaris] p. 59Section 14notnotrALTVD 43676
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 43677
[Margaris] p. 79Rule Cexinst01 43386  exinst11 43387
[Margaris] p. 89Theorem 19.219.2 1981  19.2g 2182  r19.2z 4495
[Margaris] p. 89Theorem 19.319.3 2196  rr19.3v 3658
[Margaris] p. 89Theorem 19.5alcom 2157
[Margaris] p. 89Theorem 19.6alex 1829
[Margaris] p. 89Theorem 19.7alnex 1784
[Margaris] p. 89Theorem 19.819.8a 2175
[Margaris] p. 89Theorem 19.919.9 2199  19.9h 2283  exlimd 2212  exlimdh 2287
[Margaris] p. 89Theorem 19.11excom 2163  excomim 2164
[Margaris] p. 89Theorem 19.1219.12 2321
[Margaris] p. 90Section 19conventions-labels 29654  conventions-labels 29654  conventions-labels 29654  conventions-labels 29654
[Margaris] p. 90Theorem 19.14exnal 1830
[Margaris] p. 90Theorem 19.152albi 43137  albi 1821
[Margaris] p. 90Theorem 19.1619.16 2219
[Margaris] p. 90Theorem 19.1719.17 2220
[Margaris] p. 90Theorem 19.182exbi 43139  exbi 1850
[Margaris] p. 90Theorem 19.1919.19 2223
[Margaris] p. 90Theorem 19.202alim 43136  2alimdv 1922  alimd 2206  alimdh 1820  alimdv 1920  ax-4 1812  ralimdaa 3258  ralimdv 3170  ralimdva 3168  ralimdvva 3205  sbcimdv 3852
[Margaris] p. 90Theorem 19.2119.21 2201  19.21h 2284  19.21t 2200  19.21vv 43135  alrimd 2209  alrimdd 2208  alrimdh 1867  alrimdv 1933  alrimi 2207  alrimih 1827  alrimiv 1931  alrimivv 1932  hbralrimi 3145  r19.21be 3250  r19.21bi 3249  ralrimd 3262  ralrimdv 3153  ralrimdva 3155  ralrimdvv 3202  ralrimdvva 3210  ralrimi 3255  ralrimia 3256  ralrimiv 3146  ralrimiva 3147  ralrimivv 3199  ralrimivva 3201  ralrimivvva 3204  ralrimivw 3151
[Margaris] p. 90Theorem 19.222exim 43138  2eximdv 1923  exim 1837  eximd 2210  eximdh 1868  eximdv 1921  rexim 3088  reximd2a 3267  reximdai 3259  reximdd 43841  reximddv 3172  reximddv2 3213  reximddv3 43840  reximdv 3171  reximdv2 3165  reximdva 3169  reximdvai 3166  reximdvva 3206  reximi2 3080
[Margaris] p. 90Theorem 19.2319.23 2205  19.23bi 2185  19.23h 2285  19.23t 2204  exlimdv 1937  exlimdvv 1938  exlimexi 43285  exlimiv 1934  exlimivv 1936  rexlimd3 43833  rexlimdv 3154  rexlimdv3a 3160  rexlimdva 3156  rexlimdva2 3158  rexlimdvaa 3157  rexlimdvv 3211  rexlimdvva 3212  rexlimdvw 3161  rexlimiv 3149  rexlimiva 3148  rexlimivv 3200
[Margaris] p. 90Theorem 19.2419.24 1990
[Margaris] p. 90Theorem 19.2519.25 1884
[Margaris] p. 90Theorem 19.2619.26 1874
[Margaris] p. 90Theorem 19.2719.27 2221  r19.27z 4505  r19.27zv 4506
[Margaris] p. 90Theorem 19.2819.28 2222  19.28vv 43145  r19.28z 4498  r19.28zf 43853  r19.28zv 4501  rr19.28v 3659
[Margaris] p. 90Theorem 19.2919.29 1877  r19.29d2r 3141  r19.29imd 3119
[Margaris] p. 90Theorem 19.3019.30 1885
[Margaris] p. 90Theorem 19.3119.31 2228  19.31vv 43143
[Margaris] p. 90Theorem 19.3219.32 2227  r19.32 45806
[Margaris] p. 90Theorem 19.3319.33-2 43141  19.33 1888
[Margaris] p. 90Theorem 19.3419.34 1991
[Margaris] p. 90Theorem 19.3519.35 1881
[Margaris] p. 90Theorem 19.3619.36 2224  19.36vv 43142  r19.36zv 4507
[Margaris] p. 90Theorem 19.3719.37 2226  19.37vv 43144  r19.37zv 4502
[Margaris] p. 90Theorem 19.3819.38 1842
[Margaris] p. 90Theorem 19.3919.39 1989
[Margaris] p. 90Theorem 19.4019.40-2 1891  19.40 1890  r19.40 3120
[Margaris] p. 90Theorem 19.4119.41 2229  19.41rg 43311
[Margaris] p. 90Theorem 19.4219.42 2230
[Margaris] p. 90Theorem 19.4319.43 1886
[Margaris] p. 90Theorem 19.4419.44 2231  r19.44zv 4504
[Margaris] p. 90Theorem 19.4519.45 2232  r19.45zv 4503
[Margaris] p. 110Exercise 2(b)eu1 2607
[Mayet] p. 370Remarkjpi 31523  largei 31520  stri 31510
[Mayet3] p. 9Definition of CH-statesdf-hst 31465  ishst 31467
[Mayet3] p. 10Theoremhstrbi 31519  hstri 31518
[Mayet3] p. 1223Theorem 4.1mayete3i 30981
[Mayet3] p. 1240Theorem 7.1mayetes3i 30982
[MegPav2000] p. 2344Theorem 3.3stcltrthi 31531
[MegPav2000] p. 2345Definition 3.4-1chintcl 30585  chsupcl 30593
[MegPav2000] p. 2345Definition 3.4-2hatomic 31613
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 31607
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 31634
[MegPav2000] p. 2366Figure 7pl42N 38854
[MegPav2002] p. 362Lemma 2.2latj31 18440  latj32 18438  latjass 18436
[Megill] p. 444Axiom C5ax-5 1914  ax5ALT 37777
[Megill] p. 444Section 7conventions 29653
[Megill] p. 445Lemma L12aecom-o 37771  ax-c11n 37758  axc11n 2426
[Megill] p. 446Lemma L17equtrr 2026
[Megill] p. 446Lemma L18ax6fromc10 37766
[Megill] p. 446Lemma L19hbnae-o 37798  hbnae 2432
[Megill] p. 447Remark 9.1dfsb1 2481  sbid 2248  sbidd-misc 47764  sbidd 47763
[Megill] p. 448Remark 9.6axc14 2463
[Megill] p. 448Scheme C4'ax-c4 37754
[Megill] p. 448Scheme C5'ax-c5 37753  sp 2177
[Megill] p. 448Scheme C6'ax-11 2155
[Megill] p. 448Scheme C7'ax-c7 37755
[Megill] p. 448Scheme C8'ax-7 2012
[Megill] p. 448Scheme C9'ax-c9 37760
[Megill] p. 448Scheme C10'ax-6 1972  ax-c10 37756
[Megill] p. 448Scheme C11'ax-c11 37757
[Megill] p. 448Scheme C12'ax-8 2109
[Megill] p. 448Scheme C13'ax-9 2117
[Megill] p. 448Scheme C14'ax-c14 37761
[Megill] p. 448Scheme C15'ax-c15 37759
[Megill] p. 448Scheme C16'ax-c16 37762
[Megill] p. 448Theorem 9.4dral1-o 37774  dral1 2439  dral2-o 37800  dral2 2438  drex1 2441  drex2 2442  drsb1 2495  drsb2 2258
[Megill] p. 449Theorem 9.7sbcom2 2162  sbequ 2087  sbid2v 2509
[Megill] p. 450Example in Appendixhba1-o 37767  hba1 2290
[Mendelson] p. 35Axiom A3hirstL-ax3 45602
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3874  rspsbca 3875  stdpc4 2072
[Mendelson] p. 69Axiom 5ax-c4 37754  ra4 3881  stdpc5 2202
[Mendelson] p. 81Rule Cexlimiv 1934
[Mendelson] p. 95Axiom 6stdpc6 2032
[Mendelson] p. 95Axiom 7stdpc7 2243
[Mendelson] p. 225Axiom system NBGru 3777
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5515
[Mendelson] p. 231Exercise 4.10(k)inv1 4395
[Mendelson] p. 231Exercise 4.10(l)unv 4396
[Mendelson] p. 231Exercise 4.10(n)dfin3 4267
[Mendelson] p. 231Exercise 4.10(o)df-nul 4324
[Mendelson] p. 231Exercise 4.10(q)dfin4 4268
[Mendelson] p. 231Exercise 4.10(s)ddif 4137
[Mendelson] p. 231Definition of uniondfun3 4266
[Mendelson] p. 235Exercise 4.12(c)univ 5452
[Mendelson] p. 235Exercise 4.12(d)pwv 4906
[Mendelson] p. 235Exercise 4.12(j)pwin 5571
[Mendelson] p. 235Exercise 4.12(k)pwunss 4621
[Mendelson] p. 235Exercise 4.12(l)pwssun 5572
[Mendelson] p. 235Exercise 4.12(n)uniin 4936
[Mendelson] p. 235Exercise 4.12(p)reli 5827
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6268
[Mendelson] p. 244Proposition 4.8(g)epweon 7762
[Mendelson] p. 246Definition of successordf-suc 6371
[Mendelson] p. 250Exercise 4.36oelim2 8595
[Mendelson] p. 254Proposition 4.22(b)xpen 9140
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9055  xpsneng 9056
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9063  xpcomeng 9064
[Mendelson] p. 254Proposition 4.22(e)xpassen 9066
[Mendelson] p. 255Definitionbrsdom 8971
[Mendelson] p. 255Exercise 4.39endisj 9058
[Mendelson] p. 255Exercise 4.41mapprc 8824
[Mendelson] p. 255Exercise 4.43mapsnen 9037  mapsnend 9036
[Mendelson] p. 255Exercise 4.45mapunen 9146
[Mendelson] p. 255Exercise 4.47xpmapen 9145
[Mendelson] p. 255Exercise 4.42(a)map0e 8876
[Mendelson] p. 255Exercise 4.42(b)map1 9040
[Mendelson] p. 257Proposition 4.24(a)undom 9059
[Mendelson] p. 258Exercise 4.56(c)djuassen 10173  djucomen 10172
[Mendelson] p. 258Exercise 4.56(f)djudom1 10177
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10171
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8531
[Mendelson] p. 266Proposition 4.34(f)oaordex 8558
[Mendelson] p. 275Proposition 4.42(d)entri3 10554
[Mendelson] p. 281Definitiondf-r1 9759
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9808
[Mendelson] p. 287Axiom system MKru 3777
[MertziosUnger] p. 152Definitiondf-frgr 29512
[MertziosUnger] p. 153Remark 1frgrconngr 29547
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 29549  vdgn1frgrv3 29550
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 29551
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 29544
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 29537  2pthfrgrrn 29535  2pthfrgrrn2 29536
[Mittelstaedt] p. 9Definitiondf-oc 30505
[Monk1] p. 22Remarkconventions 29653
[Monk1] p. 22Theorem 3.1conventions 29653
[Monk1] p. 26Theorem 2.8(vii)ssin 4231
[Monk1] p. 33Theorem 3.2(i)ssrel 5783  ssrelf 31844
[Monk1] p. 33Theorem 3.2(ii)eqrel 5785
[Monk1] p. 34Definition 3.3df-opab 5212
[Monk1] p. 36Theorem 3.7(i)coi1 6262  coi2 6263
[Monk1] p. 36Theorem 3.8(v)dm0 5921  rn0 5926
[Monk1] p. 36Theorem 3.7(ii)cnvi 6142
[Monk1] p. 37Theorem 3.13(i)relxp 5695
[Monk1] p. 37Theorem 3.13(x)dmxp 5929  rnxp 6170
[Monk1] p. 37Theorem 3.13(ii)0xp 5775  xp0 6158
[Monk1] p. 38Theorem 3.16(ii)ima0 6077
[Monk1] p. 38Theorem 3.16(viii)imai 6074
[Monk1] p. 39Theorem 3.17imaex 7907  imaexALTV 37199  imaexg 7906
[Monk1] p. 39Theorem 3.16(xi)imassrn 6071
[Monk1] p. 41Theorem 4.3(i)fnopfv 7078  funfvop 7052
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6948
[Monk1] p. 42Theorem 4.4(iii)fvelima 6958
[Monk1] p. 43Theorem 4.6funun 6595
[Monk1] p. 43Theorem 4.8(iv)dff13 7254  dff13f 7255
[Monk1] p. 46Theorem 4.15(v)funex 7221  funrnex 7940
[Monk1] p. 50Definition 5.4fniunfv 7246
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6227
[Monk1] p. 52Theorem 5.11(viii)ssint 4969
[Monk1] p. 52Definition 5.13 (i)1stval2 7992  df-1st 7975
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7993  df-2nd 7976
[Monk1] p. 112Theorem 15.17(v)ranksn 9849  ranksnb 9822
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9850
[Monk1] p. 112Theorem 15.17(iii)rankun 9851  rankunb 9845
[Monk1] p. 113Theorem 15.18r1val3 9833
[Monk1] p. 113Definition 15.19df-r1 9759  r1val2 9832
[Monk1] p. 117Lemmazorn2 10501  zorn2g 10498
[Monk1] p. 133Theorem 18.11cardom 9981
[Monk1] p. 133Theorem 18.12canth3 10556
[Monk1] p. 133Theorem 18.14carduni 9976
[Monk2] p. 105Axiom C4ax-4 1812
[Monk2] p. 105Axiom C7ax-7 2012
[Monk2] p. 105Axiom C8ax-12 2172  ax-c15 37759  ax12v2 2174
[Monk2] p. 108Lemma 5ax-c4 37754
[Monk2] p. 109Lemma 12ax-11 2155
[Monk2] p. 109Lemma 15equvini 2455  equvinv 2033  eqvinop 5488
[Monk2] p. 113Axiom C5-1ax-5 1914  ax5ALT 37777
[Monk2] p. 113Axiom C5-2ax-10 2138
[Monk2] p. 113Axiom C5-3ax-11 2155
[Monk2] p. 114Lemma 21sp 2177
[Monk2] p. 114Lemma 22axc4 2315  hba1-o 37767  hba1 2290
[Monk2] p. 114Lemma 23nfia1 2151
[Monk2] p. 114Lemma 24nfa2 2171  nfra2 3373  nfra2w 3297
[Moore] p. 53Part Idf-mre 17530
[Munkres] p. 77Example 2distop 22498  indistop 22505  indistopon 22504
[Munkres] p. 77Example 3fctop 22507  fctop2 22508
[Munkres] p. 77Example 4cctop 22509
[Munkres] p. 78Definition of basisdf-bases 22449  isbasis3g 22452
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17389  tgval2 22459
[Munkres] p. 79Remarktgcl 22472
[Munkres] p. 80Lemma 2.1tgval3 22466
[Munkres] p. 80Lemma 2.2tgss2 22490  tgss3 22489
[Munkres] p. 81Lemma 2.3basgen 22491  basgen2 22492
[Munkres] p. 83Exercise 3topdifinf 36230  topdifinfeq 36231  topdifinffin 36229  topdifinfindis 36227
[Munkres] p. 89Definition of subspace topologyresttop 22664
[Munkres] p. 93Theorem 6.1(1)0cld 22542  topcld 22539
[Munkres] p. 93Theorem 6.1(2)iincld 22543
[Munkres] p. 93Theorem 6.1(3)uncld 22545
[Munkres] p. 94Definition of closureclsval 22541
[Munkres] p. 94Definition of interiorntrval 22540
[Munkres] p. 95Theorem 6.5(a)clsndisj 22579  elcls 22577
[Munkres] p. 95Theorem 6.5(b)elcls3 22587
[Munkres] p. 97Theorem 6.6clslp 22652  neindisj 22621
[Munkres] p. 97Corollary 6.7cldlp 22654
[Munkres] p. 97Definition of limit pointislp2 22649  lpval 22643
[Munkres] p. 98Definition of Hausdorff spacedf-haus 22819
[Munkres] p. 102Definition of continuous functiondf-cn 22731  iscn 22739  iscn2 22742
[Munkres] p. 107Theorem 7.2(g)cncnp 22784  cncnp2 22785  cncnpi 22782  df-cnp 22732  iscnp 22741  iscnp2 22743
[Munkres] p. 127Theorem 10.1metcn 24052
[Munkres] p. 128Theorem 10.3metcn4 24828
[Nathanson] p. 123Remarkreprgt 33633  reprinfz1 33634  reprlt 33631
[Nathanson] p. 123Definitiondf-repr 33621
[Nathanson] p. 123Chapter 5.1circlemethnat 33653
[Nathanson] p. 123Propositionbreprexp 33645  breprexpnat 33646  itgexpif 33618
[NielsenChuang] p. 195Equation 4.73unierri 31357
[OeSilva] p. 2042Section 2ax-bgbltosilva 46478
[Pfenning] p. 17Definition XMnatded 29656
[Pfenning] p. 17Definition NNCnatded 29656  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 29656
[Pfenning] p. 18Rule"natded 29656
[Pfenning] p. 18Definition /\Inatded 29656
[Pfenning] p. 18Definition ` `Enatded 29656  natded 29656  natded 29656  natded 29656  natded 29656
[Pfenning] p. 18Definition ` `Inatded 29656  natded 29656  natded 29656  natded 29656  natded 29656
[Pfenning] p. 18Definition ` `ELnatded 29656
[Pfenning] p. 18Definition ` `ERnatded 29656
[Pfenning] p. 18Definition ` `Ea,unatded 29656
[Pfenning] p. 18Definition ` `IRnatded 29656
[Pfenning] p. 18Definition ` `Ianatded 29656
[Pfenning] p. 127Definition =Enatded 29656
[Pfenning] p. 127Definition =Inatded 29656
[Ponnusamy] p. 361Theorem 6.44cphip0l 24719  df-dip 29954  dip0l 29971  ip0l 21189
[Ponnusamy] p. 361Equation 6.45cphipval 24760  ipval 29956
[Ponnusamy] p. 362Equation I1dipcj 29967  ipcj 21187
[Ponnusamy] p. 362Equation I3cphdir 24722  dipdir 30095  ipdir 21192  ipdiri 30083
[Ponnusamy] p. 362Equation I4ipidsq 29963  nmsq 24711
[Ponnusamy] p. 362Equation 6.46ip0i 30078
[Ponnusamy] p. 362Equation 6.47ip1i 30080
[Ponnusamy] p. 362Equation 6.48ip2i 30081
[Ponnusamy] p. 363Equation I2cphass 24728  dipass 30098  ipass 21198  ipassi 30094
[Prugovecki] p. 186Definition of brabraval 31197  df-bra 31103
[Prugovecki] p. 376Equation 8.1df-kb 31104  kbval 31207
[PtakPulmannova] p. 66Proposition 3.2.17atomli 31635
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 38759
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 31649  atcvat4i 31650  cvrat3 38313  cvrat4 38314  lsatcvat3 37922
[PtakPulmannova] p. 68Definition 3.2.18cvbr 31535  cvrval 38139  df-cv 31532  df-lcv 37889  lspsncv0 20759
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 38771
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 38772
[Quine] p. 16Definition 2.1df-clab 2711  rabid 3453  rabidd 43849
[Quine] p. 17Definition 2.1''dfsb7 2276
[Quine] p. 18Definition 2.7df-cleq 2725
[Quine] p. 19Definition 2.9conventions 29653  df-v 3477
[Quine] p. 34Theorem 5.1eqabb 2874
[Quine] p. 35Theorem 5.2abid1 2871  abid2f 2937
[Quine] p. 40Theorem 6.1sb5 2268
[Quine] p. 40Theorem 6.2sb6 2089  sbalex 2236
[Quine] p. 41Theorem 6.3df-clel 2811
[Quine] p. 41Theorem 6.4eqid 2733  eqid1 29720
[Quine] p. 41Theorem 6.5eqcom 2740
[Quine] p. 42Theorem 6.6df-sbc 3779
[Quine] p. 42Theorem 6.7dfsbcq 3780  dfsbcq2 3781
[Quine] p. 43Theorem 6.8vex 3479
[Quine] p. 43Theorem 6.9isset 3488
[Quine] p. 44Theorem 7.3spcgf 3582  spcgv 3587  spcimgf 3580
[Quine] p. 44Theorem 6.11spsbc 3791  spsbcd 3792
[Quine] p. 44Theorem 6.12elex 3493
[Quine] p. 44Theorem 6.13elab 3669  elabg 3667  elabgf 3665
[Quine] p. 44Theorem 6.14noel 4331
[Quine] p. 48Theorem 7.2snprc 4722
[Quine] p. 48Definition 7.1df-pr 4632  df-sn 4630
[Quine] p. 49Theorem 7.4snss 4790  snssg 4788
[Quine] p. 49Theorem 7.5prss 4824  prssg 4823
[Quine] p. 49Theorem 7.6prid1 4767  prid1g 4765  prid2 4768  prid2g 4766  snid 4665  snidg 4663
[Quine] p. 51Theorem 7.12snex 5432
[Quine] p. 51Theorem 7.13prex 5433
[Quine] p. 53Theorem 8.2unisn 4931  unisnALT 43687  unisng 4930
[Quine] p. 53Theorem 8.3uniun 4935
[Quine] p. 54Theorem 8.6elssuni 4942
[Quine] p. 54Theorem 8.7uni0 4940
[Quine] p. 56Theorem 8.17uniabio 6511
[Quine] p. 56Definition 8.18dfaiota2 45794  dfiota2 6497
[Quine] p. 57Theorem 8.19aiotaval 45803  iotaval 6515
[Quine] p. 57Theorem 8.22iotanul 6522
[Quine] p. 58Theorem 8.23iotaex 6517
[Quine] p. 58Definition 9.1df-op 4636
[Quine] p. 61Theorem 9.5opabid 5526  opabidw 5525  opelopab 5543  opelopaba 5537  opelopabaf 5545  opelopabf 5546  opelopabg 5539  opelopabga 5534  opelopabgf 5541  oprabid 7441  oprabidw 7440
[Quine] p. 64Definition 9.11df-xp 5683
[Quine] p. 64Definition 9.12df-cnv 5685
[Quine] p. 64Definition 9.15df-id 5575
[Quine] p. 65Theorem 10.3fun0 6614
[Quine] p. 65Theorem 10.4funi 6581
[Quine] p. 65Theorem 10.5funsn 6602  funsng 6600
[Quine] p. 65Definition 10.1df-fun 6546
[Quine] p. 65Definition 10.2args 6092  dffv4 6889
[Quine] p. 68Definition 10.11conventions 29653  df-fv 6552  fv2 6887
[Quine] p. 124Theorem 17.3nn0opth2 14232  nn0opth2i 14231  nn0opthi 14230  omopthi 8660
[Quine] p. 177Definition 25.2df-rdg 8410
[Quine] p. 232Equation icarddom 10549
[Quine] p. 284Axiom 39(vi)funimaex 6637  funimaexg 6635
[Quine] p. 331Axiom system NFru 3777
[ReedSimon] p. 36Definition (iii)ax-his3 30337
[ReedSimon] p. 63Exercise 4(a)df-dip 29954  polid 30412  polid2i 30410  polidi 30411
[ReedSimon] p. 63Exercise 4(b)df-ph 30066
[ReedSimon] p. 195Remarklnophm 31272  lnophmi 31271
[Retherford] p. 49Exercise 1(i)leopadd 31385
[Retherford] p. 49Exercise 1(ii)leopmul 31387  leopmuli 31386
[Retherford] p. 49Exercise 1(iv)leoptr 31390
[Retherford] p. 49Definition VI.1df-leop 31105  leoppos 31379
[Retherford] p. 49Exercise 1(iii)leoptri 31389
[Retherford] p. 49Definition of operator orderingleop3 31378
[Roman] p. 4Definitiondf-dmat 21992  df-dmatalt 47079
[Roman] p. 18Part Preliminariesdf-rng 46649
[Roman] p. 19Part Preliminariesdf-ring 20058
[Roman] p. 46Theorem 1.6isldepslvec2 47166
[Roman] p. 112Noteisldepslvec2 47166  ldepsnlinc 47189  zlmodzxznm 47178
[Roman] p. 112Examplezlmodzxzequa 47177  zlmodzxzequap 47180  zlmodzxzldep 47185
[Roman] p. 170Theorem 7.8cayleyhamilton 22392
[Rosenlicht] p. 80Theoremheicant 36523
[Rosser] p. 281Definitiondf-op 4636
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 33657
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 33658
[Rotman] p. 28Remarkpgrpgt2nabl 47042  pmtr3ncom 19343
[Rotman] p. 31Theorem 3.4symggen2 19339
[Rotman] p. 42Theorem 3.15cayley 19282  cayleyth 19283
[Rudin] p. 164Equation 27efcan 16039
[Rudin] p. 164Equation 30efzval 16045
[Rudin] p. 167Equation 48absefi 16139
[Sanford] p. 39Remarkax-mp 5  mto 196
[Sanford] p. 39Rule 3mtpxor 1774
[Sanford] p. 39Rule 4mptxor 1772
[Sanford] p. 40Rule 1mptnan 1771
[Schechter] p. 51Definition of antisymmetryintasym 6117
[Schechter] p. 51Definition of irreflexivityintirr 6120
[Schechter] p. 51Definition of symmetrycnvsym 6114
[Schechter] p. 51Definition of transitivitycotr 6112
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17530
[Schechter] p. 79Definition of Moore closuredf-mrc 17531
[Schechter] p. 82Section 4.5df-mrc 17531
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17533
[Schechter] p. 139Definition AC3dfac9 10131
[Schechter] p. 141Definition (MC)dfac11 41804
[Schechter] p. 149Axiom DC1ax-dc 10441  axdc3 10449
[Schechter] p. 187Definition of "ring with unit"isring 20060  isrngo 36765
[Schechter] p. 276Remark 11.6.espan0 30795
[Schechter] p. 276Definition of spandf-span 30562  spanval 30586
[Schechter] p. 428Definition 15.35bastop1 22496
[Schloeder] p. 1Lemma 1.3onelon 6390  onelord 42000  ordelon 6389  ordelord 6387
[Schloeder] p. 1Lemma 1.7onepsuc 42001  sucidg 6446
[Schloeder] p. 1Remark 1.50elon 6419  onsuc 7799  ord0 6418  ordsuci 7796
[Schloeder] p. 1Theorem 1.9epsoon 42002
[Schloeder] p. 1Definition 1.1dftr5 5270
[Schloeder] p. 1Definition 1.2dford3 41767  elon2 6376
[Schloeder] p. 1Definition 1.4df-suc 6371
[Schloeder] p. 1Definition 1.6epel 5584  epelg 5582
[Schloeder] p. 1Theorem 1.9(i)elirr 9592  epirron 42003  ordirr 6383
[Schloeder] p. 1Theorem 1.9(ii)oneltr 42005  oneptr 42004  ontr1 6411
[Schloeder] p. 1Theorem 1.9(iii)oneltri 42007  oneptri 42006  ordtri3or 6397
[Schloeder] p. 2Lemma 1.10ondif1 8501  ord0eln0 6420
[Schloeder] p. 2Lemma 1.13elsuci 6432  onsucss 42016  trsucss 6453
[Schloeder] p. 2Lemma 1.14ordsucss 7806
[Schloeder] p. 2Lemma 1.15onnbtwn 6459  ordnbtwn 6458
[Schloeder] p. 2Lemma 1.16orddif0suc 42018  ordnexbtwnsuc 42017
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10396  onsucf1lem 42019  onsucf1o 42022  onsucf1olem 42020  onsucrn 42021
[Schloeder] p. 2Lemma 1.18dflim7 42023
[Schloeder] p. 2Remark 1.12ordzsl 7834
[Schloeder] p. 2Theorem 1.10ondif1i 42012  ordne0gt0 42011
[Schloeder] p. 2Definition 1.11dflim6 42014  limnsuc 42015  onsucelab 42013
[Schloeder] p. 3Remark 1.21omex 9638
[Schloeder] p. 3Theorem 1.19tfinds 7849
[Schloeder] p. 3Theorem 1.22omelon 9641  ordom 7865
[Schloeder] p. 3Definition 1.20dfom3 9642
[Schloeder] p. 4Lemma 2.21onn 8639
[Schloeder] p. 4Lemma 2.7ssonuni 7767  ssorduni 7766
[Schloeder] p. 4Remark 2.4oa1suc 8531
[Schloeder] p. 4Theorem 1.23dfom5 9645  limom 7871
[Schloeder] p. 4Definition 2.1df-1o 8466  df1o2 8473
[Schloeder] p. 4Definition 2.3oa0 8516  oa0suclim 42025  oalim 8532  oasuc 8524
[Schloeder] p. 4Definition 2.5om0 8517  om0suclim 42026  omlim 8533  omsuc 8526
[Schloeder] p. 4Definition 2.6oe0 8522  oe0m1 8521  oe0suclim 42027  oelim 8534  oesuc 8527
[Schloeder] p. 5Lemma 2.10onsupuni 41978
[Schloeder] p. 5Lemma 2.11onsupsucismax 42029
[Schloeder] p. 5Lemma 2.12onsssupeqcond 42030
[Schloeder] p. 5Lemma 2.13limexissup 42031  limexissupab 42033  limiun 42032  limuni 6426
[Schloeder] p. 5Lemma 2.14oa0r 8538
[Schloeder] p. 5Lemma 2.15om1 8542  om1om1r 42034  om1r 8543
[Schloeder] p. 5Remark 2.8oacl 8535  oaomoecl 42028  oecl 8537  omcl 8536
[Schloeder] p. 5Definition 2.9onsupintrab 41980
[Schloeder] p. 6Lemma 2.16oe1 8544
[Schloeder] p. 6Lemma 2.17oe1m 8545
[Schloeder] p. 6Lemma 2.18oe0rif 42035
[Schloeder] p. 6Theorem 2.19oasubex 42036
[Schloeder] p. 6Theorem 2.20nnacl 8611  nnamecl 42037  nnecl 8613  nnmcl 8612
[Schloeder] p. 7Lemma 3.1onsucwordi 42038
[Schloeder] p. 7Lemma 3.2oaword1 8552
[Schloeder] p. 7Lemma 3.3oaword2 8553
[Schloeder] p. 7Lemma 3.4oalimcl 8560
[Schloeder] p. 7Lemma 3.5oaltublim 42040
[Schloeder] p. 8Lemma 3.6oaordi3 42041
[Schloeder] p. 8Lemma 3.81oaomeqom 42043
[Schloeder] p. 8Lemma 3.10oa00 8559
[Schloeder] p. 8Lemma 3.11omge1 42047  omword1 8573
[Schloeder] p. 8Remark 3.9oaordnr 42046  oaordnrex 42045
[Schloeder] p. 8Theorem 3.7oaord3 42042
[Schloeder] p. 9Lemma 3.12omge2 42048  omword2 8574
[Schloeder] p. 9Lemma 3.13omlim2 42049
[Schloeder] p. 9Lemma 3.14omord2lim 42050
[Schloeder] p. 9Lemma 3.15omord2i 42051  omordi 8566
[Schloeder] p. 9Theorem 3.16omord 8568  omord2com 42052
[Schloeder] p. 10Lemma 3.172omomeqom 42053  df-2o 8467
[Schloeder] p. 10Lemma 3.19oege1 42056  oewordi 8591
[Schloeder] p. 10Lemma 3.20oege2 42057  oeworde 8593
[Schloeder] p. 10Lemma 3.21rp-oelim2 42058
[Schloeder] p. 10Lemma 3.22oeord2lim 42059
[Schloeder] p. 10Remark 3.18omnord1 42055  omnord1ex 42054
[Schloeder] p. 11Lemma 3.23oeord2i 42060
[Schloeder] p. 11Lemma 3.25nnoeomeqom 42062
[Schloeder] p. 11Remark 3.26oenord1 42066  oenord1ex 42065
[Schloeder] p. 11Theorem 4.1oaomoencom 42067
[Schloeder] p. 11Theorem 4.2oaass 8561
[Schloeder] p. 11Theorem 3.24oeord2com 42061
[Schloeder] p. 12Theorem 4.3odi 8579
[Schloeder] p. 13Theorem 4.4omass 8580
[Schloeder] p. 14Remark 4.6oenass 42069
[Schloeder] p. 14Theorem 4.7oeoa 8597
[Schloeder] p. 15Lemma 5.1cantnftermord 42070
[Schloeder] p. 15Lemma 5.2cantnfub 42071  cantnfub2 42072
[Schloeder] p. 16Theorem 5.3cantnf2 42075
[Schwabhauser] p. 10Axiom A1axcgrrflx 28172  axtgcgrrflx 27713
[Schwabhauser] p. 10Axiom A2axcgrtr 28173
[Schwabhauser] p. 10Axiom A3axcgrid 28174  axtgcgrid 27714
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 27699
[Schwabhauser] p. 11Axiom A4axsegcon 28185  axtgsegcon 27715  df-trkgcb 27701
[Schwabhauser] p. 11Axiom A5ax5seg 28196  axtg5seg 27716  df-trkgcb 27701
[Schwabhauser] p. 11Axiom A6axbtwnid 28197  axtgbtwnid 27717  df-trkgb 27700
[Schwabhauser] p. 12Axiom A7axpasch 28199  axtgpasch 27718  df-trkgb 27700
[Schwabhauser] p. 12Axiom A8axlowdim2 28218  df-trkg2d 33677
[Schwabhauser] p. 13Axiom A8axtglowdim2 27721
[Schwabhauser] p. 13Axiom A9axtgupdim2 27722  df-trkg2d 33677
[Schwabhauser] p. 13Axiom A10axeuclid 28221  axtgeucl 27723  df-trkge 27702
[Schwabhauser] p. 13Axiom A11axcont 28234  axtgcont 27720  axtgcont1 27719  df-trkgb 27700
[Schwabhauser] p. 27Theorem 2.1cgrrflx 34959
[Schwabhauser] p. 27Theorem 2.2cgrcomim 34961
[Schwabhauser] p. 27Theorem 2.3cgrtr 34964
[Schwabhauser] p. 27Theorem 2.4cgrcoml 34968
[Schwabhauser] p. 27Theorem 2.5cgrcomr 34969  tgcgrcomimp 27728  tgcgrcoml 27730  tgcgrcomr 27729
[Schwabhauser] p. 28Theorem 2.8cgrtriv 34974  tgcgrtriv 27735
[Schwabhauser] p. 28Theorem 2.105segofs 34978  tg5segofs 33685
[Schwabhauser] p. 28Definition 2.10df-afs 33682  df-ofs 34955
[Schwabhauser] p. 29Theorem 2.11cgrextend 34980  tgcgrextend 27736
[Schwabhauser] p. 29Theorem 2.12segconeq 34982  tgsegconeq 27737
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 34994  btwntriv2 34984  tgbtwntriv2 27738
[Schwabhauser] p. 30Theorem 3.2btwncomim 34985  tgbtwncom 27739
[Schwabhauser] p. 30Theorem 3.3btwntriv1 34988  tgbtwntriv1 27742
[Schwabhauser] p. 30Theorem 3.4btwnswapid 34989  tgbtwnswapid 27743
[Schwabhauser] p. 30Theorem 3.5btwnexch2 34995  btwnintr 34991  tgbtwnexch2 27747  tgbtwnintr 27744
[Schwabhauser] p. 30Theorem 3.6btwnexch 34997  btwnexch3 34992  tgbtwnexch 27749  tgbtwnexch3 27745
[Schwabhauser] p. 30Theorem 3.7btwnouttr 34996  tgbtwnouttr 27748  tgbtwnouttr2 27746
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28217
[Schwabhauser] p. 32Theorem 3.14btwndiff 34999  tgbtwndiff 27757
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 27750  trisegint 35000
[Schwabhauser] p. 34Theorem 4.2ifscgr 35016  tgifscgr 27759
[Schwabhauser] p. 34Theorem 4.11colcom 27809  colrot1 27810  colrot2 27811  lncom 27873  lnrot1 27874  lnrot2 27875
[Schwabhauser] p. 34Definition 4.1df-ifs 35012
[Schwabhauser] p. 35Theorem 4.3cgrsub 35017  tgcgrsub 27760
[Schwabhauser] p. 35Theorem 4.5cgrxfr 35027  tgcgrxfr 27769
[Schwabhauser] p. 35Statement 4.4ercgrg 27768
[Schwabhauser] p. 35Definition 4.4df-cgr3 35013  df-cgrg 27762
[Schwabhauser] p. 35Definition instead (givendf-cgrg 27762
[Schwabhauser] p. 36Theorem 4.6btwnxfr 35028  tgbtwnxfr 27781
[Schwabhauser] p. 36Theorem 4.11colinearperm1 35034  colinearperm2 35036  colinearperm3 35035  colinearperm4 35037  colinearperm5 35038
[Schwabhauser] p. 36Definition 4.8df-ismt 27784
[Schwabhauser] p. 36Definition 4.10df-colinear 35011  tgellng 27804  tglng 27797
[Schwabhauser] p. 37Theorem 4.12colineartriv1 35039
[Schwabhauser] p. 37Theorem 4.13colinearxfr 35047  lnxfr 27817
[Schwabhauser] p. 37Theorem 4.14lineext 35048  lnext 27818
[Schwabhauser] p. 37Theorem 4.16fscgr 35052  tgfscgr 27819
[Schwabhauser] p. 37Theorem 4.17linecgr 35053  lncgr 27820
[Schwabhauser] p. 37Definition 4.15df-fs 35014
[Schwabhauser] p. 38Theorem 4.18lineid 35055  lnid 27821
[Schwabhauser] p. 38Theorem 4.19idinside 35056  tgidinside 27822
[Schwabhauser] p. 39Theorem 5.1btwnconn1 35073  tgbtwnconn1 27826
[Schwabhauser] p. 41Theorem 5.2btwnconn2 35074  tgbtwnconn2 27827
[Schwabhauser] p. 41Theorem 5.3btwnconn3 35075  tgbtwnconn3 27828
[Schwabhauser] p. 41Theorem 5.5brsegle2 35081
[Schwabhauser] p. 41Definition 5.4df-segle 35079  legov 27836
[Schwabhauser] p. 41Definition 5.5legov2 27837
[Schwabhauser] p. 42Remark 5.13legso 27850
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 35082
[Schwabhauser] p. 42Theorem 5.7seglerflx 35084
[Schwabhauser] p. 42Theorem 5.8segletr 35086
[Schwabhauser] p. 42Theorem 5.9segleantisym 35087
[Schwabhauser] p. 42Theorem 5.10seglelin 35088
[Schwabhauser] p. 42Theorem 5.11seglemin 35085
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 35090
[Schwabhauser] p. 42Proposition 5.7legid 27838
[Schwabhauser] p. 42Proposition 5.8legtrd 27840
[Schwabhauser] p. 42Proposition 5.9legtri3 27841
[Schwabhauser] p. 42Proposition 5.10legtrid 27842
[Schwabhauser] p. 42Proposition 5.11leg0 27843
[Schwabhauser] p. 43Theorem 6.2btwnoutside 35097
[Schwabhauser] p. 43Theorem 6.3broutsideof3 35098
[Schwabhauser] p. 43Theorem 6.4broutsideof 35093  df-outsideof 35092
[Schwabhauser] p. 43Definition 6.1broutsideof2 35094  ishlg 27853
[Schwabhauser] p. 44Theorem 6.4hlln 27858
[Schwabhauser] p. 44Theorem 6.5hlid 27860  outsideofrflx 35099
[Schwabhauser] p. 44Theorem 6.6hlcomb 27854  hlcomd 27855  outsideofcom 35100
[Schwabhauser] p. 44Theorem 6.7hltr 27861  outsideoftr 35101
[Schwabhauser] p. 44Theorem 6.11hlcgreu 27869  outsideofeu 35103
[Schwabhauser] p. 44Definition 6.8df-ray 35110
[Schwabhauser] p. 45Part 2df-lines2 35111
[Schwabhauser] p. 45Theorem 6.13outsidele 35104
[Schwabhauser] p. 45Theorem 6.15lineunray 35119
[Schwabhauser] p. 45Theorem 6.16lineelsb2 35120  tglineelsb2 27883
[Schwabhauser] p. 45Theorem 6.17linecom 35122  linerflx1 35121  linerflx2 35123  tglinecom 27886  tglinerflx1 27884  tglinerflx2 27885
[Schwabhauser] p. 45Theorem 6.18linethru 35125  tglinethru 27887
[Schwabhauser] p. 45Definition 6.14df-line2 35109  tglng 27797
[Schwabhauser] p. 45Proposition 6.13legbtwn 27845
[Schwabhauser] p. 46Theorem 6.19linethrueu 35128  tglinethrueu 27890
[Schwabhauser] p. 46Theorem 6.21lineintmo 35129  tglineineq 27894  tglineinteq 27896  tglineintmo 27893
[Schwabhauser] p. 46Theorem 6.23colline 27900
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 27901
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 27902
[Schwabhauser] p. 49Theorem 7.3mirinv 27917
[Schwabhauser] p. 49Theorem 7.7mirmir 27913
[Schwabhauser] p. 49Theorem 7.8mirreu3 27905
[Schwabhauser] p. 49Definition 7.5df-mir 27904  ismir 27910  mirbtwn 27909  mircgr 27908  mirfv 27907  mirval 27906
[Schwabhauser] p. 50Theorem 7.8mirreu 27915
[Schwabhauser] p. 50Theorem 7.9mireq 27916
[Schwabhauser] p. 50Theorem 7.10mirinv 27917
[Schwabhauser] p. 50Theorem 7.11mirf1o 27920
[Schwabhauser] p. 50Theorem 7.13miriso 27921
[Schwabhauser] p. 51Theorem 7.14mirmot 27926
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 27923  mirbtwni 27922
[Schwabhauser] p. 51Theorem 7.16mircgrs 27924
[Schwabhauser] p. 51Theorem 7.17miduniq 27936
[Schwabhauser] p. 52Lemma 7.21symquadlem 27940
[Schwabhauser] p. 52Theorem 7.18miduniq1 27937
[Schwabhauser] p. 52Theorem 7.19miduniq2 27938
[Schwabhauser] p. 52Theorem 7.20colmid 27939
[Schwabhauser] p. 53Lemma 7.22krippen 27942
[Schwabhauser] p. 55Lemma 7.25midexlem 27943
[Schwabhauser] p. 57Theorem 8.2ragcom 27949
[Schwabhauser] p. 57Definition 8.1df-rag 27945  israg 27948
[Schwabhauser] p. 58Theorem 8.3ragcol 27950
[Schwabhauser] p. 58Theorem 8.4ragmir 27951
[Schwabhauser] p. 58Theorem 8.5ragtrivb 27953
[Schwabhauser] p. 58Theorem 8.6ragflat2 27954
[Schwabhauser] p. 58Theorem 8.7ragflat 27955
[Schwabhauser] p. 58Theorem 8.8ragtriva 27956
[Schwabhauser] p. 58Theorem 8.9ragflat3 27957  ragncol 27960
[Schwabhauser] p. 58Theorem 8.10ragcgr 27958
[Schwabhauser] p. 59Theorem 8.12perpcom 27964
[Schwabhauser] p. 59Theorem 8.13ragperp 27968
[Schwabhauser] p. 59Theorem 8.14perpneq 27965
[Schwabhauser] p. 59Definition 8.11df-perpg 27947  isperp 27963
[Schwabhauser] p. 59Definition 8.13isperp2 27966
[Schwabhauser] p. 60Theorem 8.18foot 27973
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 27981  colperpexlem2 27982
[Schwabhauser] p. 63Theorem 8.21colperpex 27984  colperpexlem3 27983
[Schwabhauser] p. 64Theorem 8.22mideu 27989  midex 27988
[Schwabhauser] p. 66Lemma 8.24opphllem 27986
[Schwabhauser] p. 67Theorem 9.2oppcom 27995
[Schwabhauser] p. 67Definition 9.1islnopp 27990
[Schwabhauser] p. 68Lemma 9.3opphllem2 27999
[Schwabhauser] p. 68Lemma 9.4opphllem5 28002  opphllem6 28003
[Schwabhauser] p. 69Theorem 9.5opphl 28005
[Schwabhauser] p. 69Theorem 9.6axtgpasch 27718
[Schwabhauser] p. 70Theorem 9.6outpasch 28006
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28014
[Schwabhauser] p. 71Definition 9.7df-hpg 28009  hpgbr 28011
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28016
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28015
[Schwabhauser] p. 72Theorem 9.11hpgid 28017
[Schwabhauser] p. 72Theorem 9.12hpgcom 28018
[Schwabhauser] p. 72Theorem 9.13hpgtr 28019
[Schwabhauser] p. 73Theorem 9.18colopp 28020
[Schwabhauser] p. 73Theorem 9.19colhp 28021
[Schwabhauser] p. 88Theorem 10.2lmieu 28035
[Schwabhauser] p. 88Definition 10.1df-mid 28025
[Schwabhauser] p. 89Theorem 10.4lmicom 28039
[Schwabhauser] p. 89Theorem 10.5lmilmi 28040
[Schwabhauser] p. 89Theorem 10.6lmireu 28041
[Schwabhauser] p. 89Theorem 10.7lmieq 28042
[Schwabhauser] p. 89Theorem 10.8lmiinv 28043
[Schwabhauser] p. 89Theorem 10.9lmif1o 28046
[Schwabhauser] p. 89Theorem 10.10lmiiso 28048
[Schwabhauser] p. 89Definition 10.3df-lmi 28026
[Schwabhauser] p. 90Theorem 10.11lmimot 28049
[Schwabhauser] p. 91Theorem 10.12hypcgr 28052
[Schwabhauser] p. 92Theorem 10.14lmiopp 28053
[Schwabhauser] p. 92Theorem 10.15lnperpex 28054
[Schwabhauser] p. 92Theorem 10.16trgcopy 28055  trgcopyeu 28057
[Schwabhauser] p. 95Definition 11.2dfcgra2 28081
[Schwabhauser] p. 95Definition 11.3iscgra 28060
[Schwabhauser] p. 95Proposition 11.4cgracgr 28069
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28067  cgrahl2 28068
[Schwabhauser] p. 96Theorem 11.6cgraid 28070
[Schwabhauser] p. 96Theorem 11.9cgraswap 28071
[Schwabhauser] p. 97Theorem 11.7cgracom 28073
[Schwabhauser] p. 97Theorem 11.8cgratr 28074
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28077  cgrahl 28078
[Schwabhauser] p. 98Theorem 11.13sacgr 28082
[Schwabhauser] p. 98Theorem 11.14oacgr 28083
[Schwabhauser] p. 98Theorem 11.15acopy 28084  acopyeu 28085
[Schwabhauser] p. 101Theorem 11.24inagswap 28092
[Schwabhauser] p. 101Theorem 11.25inaghl 28096
[Schwabhauser] p. 101Definition 11.23isinag 28089
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28104
[Schwabhauser] p. 102Definition 11.27df-leag 28097  isleag 28098
[Schwabhauser] p. 107Theorem 11.49tgsas 28106  tgsas1 28105  tgsas2 28107  tgsas3 28108
[Schwabhauser] p. 108Theorem 11.50tgasa 28110  tgasa1 28109
[Schwabhauser] p. 109Theorem 11.51tgsss1 28111  tgsss2 28112  tgsss3 28113
[Shapiro] p. 230Theorem 6.5.1dchrhash 26774  dchrsum 26772  dchrsum2 26771  sumdchr 26775
[Shapiro] p. 232Theorem 6.5.2dchr2sum 26776  sum2dchr 26777
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19936  ablfacrp2 19937
[Shapiro], p. 328Equation 9.2.4vmasum 26719
[Shapiro], p. 329Equation 9.2.7logfac2 26720
[Shapiro], p. 329Equation 9.2.9logfacrlim 26727
[Shapiro], p. 331Equation 9.2.13vmadivsum 26985
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 26988
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27042  vmalogdivsum2 27041
[Shapiro], p. 375Theorem 9.4.1dirith 27032  dirith2 27031
[Shapiro], p. 375Equation 9.4.3rplogsum 27030  rpvmasum 27029  rpvmasum2 27015
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 26990
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27028
[Shapiro], p. 377Lemma 9.4.1dchrisum 26995  dchrisumlem1 26992  dchrisumlem2 26993  dchrisumlem3 26994  dchrisumlema 26991
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 26998
[Shapiro], p. 379Equation 9.4.16dchrmusum 27027  dchrmusumlem 27025  dchrvmasumlem 27026
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 26997
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 26999
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27023  dchrisum0re 27016  dchrisumn0 27024
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27009
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27013
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27014
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27069  pntrsumbnd2 27070  pntrsumo1 27068
[Shapiro], p. 405Equation 10.2.1mudivsum 27033
[Shapiro], p. 406Equation 10.2.6mulogsum 27035
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27037
[Shapiro], p. 407Equation 10.2.8mulog2sum 27040
[Shapiro], p. 418Equation 10.4.6logsqvma 27045
[Shapiro], p. 418Equation 10.4.8logsqvma2 27046
[Shapiro], p. 419Equation 10.4.10selberg 27051
[Shapiro], p. 420Equation 10.4.12selberg2lem 27053
[Shapiro], p. 420Equation 10.4.14selberg2 27054
[Shapiro], p. 422Equation 10.6.7selberg3 27062
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27063
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27060  selberg3lem2 27061
[Shapiro], p. 422Equation 10.4.23selberg4 27064
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27058
[Shapiro], p. 428Equation 10.6.2selbergr 27071
[Shapiro], p. 429Equation 10.6.8selberg3r 27072
[Shapiro], p. 430Equation 10.6.11selberg4r 27073
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27087
[Shapiro], p. 434Equation 10.6.27pntlema 27099  pntlemb 27100  pntlemc 27098  pntlemd 27097  pntlemg 27101
[Shapiro], p. 435Equation 10.6.29pntlema 27099
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27091
[Shapiro], p. 436Lemma 10.6.2pntibnd 27096
[Shapiro], p. 436Equation 10.6.34pntlema 27099
[Shapiro], p. 436Equation 10.6.35pntlem3 27112  pntleml 27114
[Stoll] p. 13Definition corresponds to dfsymdif3 4297
[Stoll] p. 16Exercise 4.40dif 4402  dif0 4373
[Stoll] p. 16Exercise 4.8difdifdir 4492
[Stoll] p. 17Theorem 5.1(5)unvdif 4475
[Stoll] p. 19Theorem 5.2(13)undm 4288
[Stoll] p. 19Theorem 5.2(13')indm 4289
[Stoll] p. 20Remarkinvdif 4269
[Stoll] p. 25Definition of ordered tripledf-ot 4638
[Stoll] p. 43Definitionuniiun 5062
[Stoll] p. 44Definitionintiin 5063
[Stoll] p. 45Definitiondf-iin 5001
[Stoll] p. 45Definition indexed uniondf-iun 5000
[Stoll] p. 176Theorem 3.4(27)iman 403
[Stoll] p. 262Example 4.1dfsymdif3 4297
[Strang] p. 242Section 6.3expgrowth 43094
[Suppes] p. 22Theorem 2eq0 4344  eq0f 4341
[Suppes] p. 22Theorem 4eqss 3998  eqssd 4000  eqssi 3999
[Suppes] p. 23Theorem 5ss0 4399  ss0b 4398
[Suppes] p. 23Theorem 6sstr 3991  sstrALT2 43596
[Suppes] p. 23Theorem 7pssirr 4101
[Suppes] p. 23Theorem 8pssn2lp 4102
[Suppes] p. 23Theorem 9psstr 4105
[Suppes] p. 23Theorem 10pssss 4096
[Suppes] p. 25Theorem 12elin 3965  elun 4149
[Suppes] p. 26Theorem 15inidm 4219
[Suppes] p. 26Theorem 16in0 4392
[Suppes] p. 27Theorem 23unidm 4153
[Suppes] p. 27Theorem 24un0 4391
[Suppes] p. 27Theorem 25ssun1 4173
[Suppes] p. 27Theorem 26ssequn1 4181
[Suppes] p. 27Theorem 27unss 4185
[Suppes] p. 27Theorem 28indir 4276
[Suppes] p. 27Theorem 29undir 4277
[Suppes] p. 28Theorem 32difid 4371
[Suppes] p. 29Theorem 33difin 4262
[Suppes] p. 29Theorem 34indif 4270
[Suppes] p. 29Theorem 35undif1 4476
[Suppes] p. 29Theorem 36difun2 4481
[Suppes] p. 29Theorem 37difin0 4474
[Suppes] p. 29Theorem 38disjdif 4472
[Suppes] p. 29Theorem 39difundi 4280
[Suppes] p. 29Theorem 40difindi 4282
[Suppes] p. 30Theorem 41nalset 5314
[Suppes] p. 39Theorem 61uniss 4917
[Suppes] p. 39Theorem 65uniop 5516
[Suppes] p. 41Theorem 70intsn 4991
[Suppes] p. 42Theorem 71intpr 4987  intprg 4986
[Suppes] p. 42Theorem 73op1stb 5472
[Suppes] p. 42Theorem 78intun 4985
[Suppes] p. 44Definition 15(a)dfiun2 5037  dfiun2g 5034
[Suppes] p. 44Definition 15(b)dfiin2 5038
[Suppes] p. 47Theorem 86elpw 4607  elpw2 5346  elpw2g 5345  elpwg 4606  elpwgdedVD 43678
[Suppes] p. 47Theorem 87pwid 4625
[Suppes] p. 47Theorem 89pw0 4816
[Suppes] p. 48Theorem 90pwpw0 4817
[Suppes] p. 52Theorem 101xpss12 5692
[Suppes] p. 52Theorem 102xpindi 5834  xpindir 5835
[Suppes] p. 52Theorem 103xpundi 5745  xpundir 5746
[Suppes] p. 54Theorem 105elirrv 9591
[Suppes] p. 58Theorem 2relss 5782
[Suppes] p. 59Theorem 4eldm 5901  eldm2 5902  eldm2g 5900  eldmg 5899
[Suppes] p. 59Definition 3df-dm 5687
[Suppes] p. 60Theorem 6dmin 5912
[Suppes] p. 60Theorem 8rnun 6146
[Suppes] p. 60Theorem 9rnin 6147
[Suppes] p. 60Definition 4dfrn2 5889
[Suppes] p. 61Theorem 11brcnv 5883  brcnvg 5880
[Suppes] p. 62Equation 5elcnv 5877  elcnv2 5878
[Suppes] p. 62Theorem 12relcnv 6104
[Suppes] p. 62Theorem 15cnvin 6145
[Suppes] p. 62Theorem 16cnvun 6143
[Suppes] p. 63Definitiondftrrels2 37445
[Suppes] p. 63Theorem 20co02 6260
[Suppes] p. 63Theorem 21dmcoss 5971
[Suppes] p. 63Definition 7df-co 5686
[Suppes] p. 64Theorem 26cnvco 5886
[Suppes] p. 64Theorem 27coass 6265
[Suppes] p. 65Theorem 31resundi 5996
[Suppes] p. 65Theorem 34elima 6065  elima2 6066  elima3 6067  elimag 6064
[Suppes] p. 65Theorem 35imaundi 6150
[Suppes] p. 66Theorem 40dminss 6153
[Suppes] p. 66Theorem 41imainss 6154
[Suppes] p. 67Exercise 11cnvxp 6157
[Suppes] p. 81Definition 34dfec2 8706
[Suppes] p. 82Theorem 72elec 8747  elecALTV 37134  elecg 8746
[Suppes] p. 82Theorem 73eqvrelth 37481  erth 8752  erth2 8753
[Suppes] p. 83Theorem 74eqvreldisj 37484  erdisj 8755
[Suppes] p. 83Definition 35, df-parts 37635  dfmembpart2 37640
[Suppes] p. 89Theorem 96map0b 8877
[Suppes] p. 89Theorem 97map0 8881  map0g 8878
[Suppes] p. 89Theorem 98mapsn 8882  mapsnd 8880
[Suppes] p. 89Theorem 99mapss 8883
[Suppes] p. 91Definition 12(ii)alephsuc 10063
[Suppes] p. 91Definition 12(iii)alephlim 10062
[Suppes] p. 92Theorem 1enref 8981  enrefg 8980
[Suppes] p. 92Theorem 2ensym 8999  ensymb 8998  ensymi 9000
[Suppes] p. 92Theorem 3entr 9002
[Suppes] p. 92Theorem 4unen 9046
[Suppes] p. 94Theorem 15endom 8975
[Suppes] p. 94Theorem 16ssdomg 8996
[Suppes] p. 94Theorem 17domtr 9003
[Suppes] p. 95Theorem 18sbth 9093
[Suppes] p. 97Theorem 23canth2 9130  canth2g 9131
[Suppes] p. 97Definition 3brsdom2 9097  df-sdom 8942  dfsdom2 9096
[Suppes] p. 97Theorem 21(i)sdomirr 9114
[Suppes] p. 97Theorem 22(i)domnsym 9099
[Suppes] p. 97Theorem 21(ii)sdomnsym 9098
[Suppes] p. 97Theorem 22(ii)domsdomtr 9112
[Suppes] p. 97Theorem 22(iv)brdom2 8978
[Suppes] p. 97Theorem 21(iii)sdomtr 9115
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9110
[Suppes] p. 98Exercise 4fundmen 9031  fundmeng 9032
[Suppes] p. 98Exercise 6xpdom3 9070
[Suppes] p. 98Exercise 11sdomentr 9111
[Suppes] p. 104Theorem 37fofi 9338
[Suppes] p. 104Theorem 38pwfi 9178
[Suppes] p. 105Theorem 40pwfi 9178
[Suppes] p. 111Axiom for cardinal numberscarden 10546
[Suppes] p. 130Definition 3df-tr 5267
[Suppes] p. 132Theorem 9ssonuni 7767
[Suppes] p. 134Definition 6df-suc 6371
[Suppes] p. 136Theorem Schema 22findes 7893  finds 7889  finds1 7892  finds2 7891
[Suppes] p. 151Theorem 42isfinite 9647  isfinite2 9301  isfiniteg 9304  unbnn 9299
[Suppes] p. 162Definition 5df-ltnq 10913  df-ltpq 10905
[Suppes] p. 197Theorem Schema 4tfindes 7852  tfinds 7849  tfinds2 7853
[Suppes] p. 209Theorem 18oaord1 8551
[Suppes] p. 209Theorem 21oaword2 8553
[Suppes] p. 211Theorem 25oaass 8561
[Suppes] p. 225Definition 8iscard2 9971
[Suppes] p. 227Theorem 56ondomon 10558
[Suppes] p. 228Theorem 59harcard 9973
[Suppes] p. 228Definition 12(i)aleph0 10061
[Suppes] p. 228Theorem Schema 61onintss 6416
[Suppes] p. 228Theorem Schema 62onminesb 7781  onminsb 7782
[Suppes] p. 229Theorem 64alephval2 10567
[Suppes] p. 229Theorem 65alephcard 10065
[Suppes] p. 229Theorem 66alephord2i 10072
[Suppes] p. 229Theorem 67alephnbtwn 10066
[Suppes] p. 229Definition 12df-aleph 9935
[Suppes] p. 242Theorem 6weth 10490
[Suppes] p. 242Theorem 8entric 10552
[Suppes] p. 242Theorem 9carden 10546
[TakeutiZaring] p. 8Axiom 1ax-ext 2704
[TakeutiZaring] p. 13Definition 4.5df-cleq 2725
[TakeutiZaring] p. 13Proposition 4.6df-clel 2811
[TakeutiZaring] p. 13Proposition 4.9cvjust 2727
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2756
[TakeutiZaring] p. 14Definition 4.16df-oprab 7413
[TakeutiZaring] p. 14Proposition 4.14ru 3777
[TakeutiZaring] p. 15Axiom 2zfpair 5420
[TakeutiZaring] p. 15Exercise 1elpr 4652  elpr2 4654  elpr2g 4653  elprg 4650
[TakeutiZaring] p. 15Exercise 2elsn 4644  elsn2 4668  elsn2g 4667  elsng 4643  velsn 4645
[TakeutiZaring] p. 15Exercise 3elop 5468
[TakeutiZaring] p. 15Exercise 4sneq 4639  sneqr 4842
[TakeutiZaring] p. 15Definition 5.1dfpr2 4648  dfsn2 4642  dfsn2ALT 4649
[TakeutiZaring] p. 16Axiom 3uniex 7731
[TakeutiZaring] p. 16Exercise 6opth 5477
[TakeutiZaring] p. 16Exercise 7opex 5465
[TakeutiZaring] p. 16Exercise 8rext 5449
[TakeutiZaring] p. 16Corollary 5.8unex 7733  unexg 7736
[TakeutiZaring] p. 16Definition 5.3dftp2 4694
[TakeutiZaring] p. 16Definition 5.5df-uni 4910
[TakeutiZaring] p. 16Definition 5.6df-in 3956  df-un 3954
[TakeutiZaring] p. 16Proposition 5.7unipr 4927  uniprg 4926
[TakeutiZaring] p. 17Axiom 4vpwex 5376
[TakeutiZaring] p. 17Exercise 1eltp 4693
[TakeutiZaring] p. 17Exercise 5elsuc 6435  elsucg 6433  sstr2 3990
[TakeutiZaring] p. 17Exercise 6uncom 4154
[TakeutiZaring] p. 17Exercise 7incom 4202
[TakeutiZaring] p. 17Exercise 8unass 4167
[TakeutiZaring] p. 17Exercise 9inass 4220
[TakeutiZaring] p. 17Exercise 10indi 4274
[TakeutiZaring] p. 17Exercise 11undi 4275
[TakeutiZaring] p. 17Definition 5.9df-pss 3968  dfss2 3969
[TakeutiZaring] p. 17Definition 5.10df-pw 4605
[TakeutiZaring] p. 18Exercise 7unss2 4182
[TakeutiZaring] p. 18Exercise 9df-ss 3966  sseqin2 4216
[TakeutiZaring] p. 18Exercise 10ssid 4005
[TakeutiZaring] p. 18Exercise 12inss1 4229  inss2 4230
[TakeutiZaring] p. 18Exercise 13nss 4047
[TakeutiZaring] p. 18Exercise 15unieq 4920
[TakeutiZaring] p. 18Exercise 18sspwb 5450  sspwimp 43679  sspwimpALT 43686  sspwimpALT2 43689  sspwimpcf 43681
[TakeutiZaring] p. 18Exercise 19pweqb 5457
[TakeutiZaring] p. 19Axiom 5ax-rep 5286
[TakeutiZaring] p. 20Definitiondf-rab 3434
[TakeutiZaring] p. 20Corollary 5.160ex 5308
[TakeutiZaring] p. 20Definition 5.12df-dif 3952
[TakeutiZaring] p. 20Definition 5.14dfnul2 4326
[TakeutiZaring] p. 20Proposition 5.15difid 4371
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4347  n0f 4343  neq0 4346  neq0f 4342
[TakeutiZaring] p. 21Axiom 6zfreg 9590
[TakeutiZaring] p. 21Axiom 6'zfregs 9727
[TakeutiZaring] p. 21Theorem 5.22setind 9729
[TakeutiZaring] p. 21Definition 5.20df-v 3477
[TakeutiZaring] p. 21Proposition 5.21vprc 5316
[TakeutiZaring] p. 22Exercise 10ss 4397
[TakeutiZaring] p. 22Exercise 3ssex 5322  ssexg 5324
[TakeutiZaring] p. 22Exercise 4inex1 5318
[TakeutiZaring] p. 22Exercise 5ruv 9597
[TakeutiZaring] p. 22Exercise 6elirr 9592
[TakeutiZaring] p. 22Exercise 7ssdif0 4364
[TakeutiZaring] p. 22Exercise 11difdif 4131
[TakeutiZaring] p. 22Exercise 13undif3 4291  undif3VD 43643
[TakeutiZaring] p. 22Exercise 14difss 4132
[TakeutiZaring] p. 22Exercise 15sscon 4139
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3063
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3072
[TakeutiZaring] p. 23Proposition 6.2xpex 7740  xpexg 7737
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5684
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6620
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6798  fun11 6623
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6560  svrelfun 6621
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5888
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5890
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5689
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5690
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5686
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6194  dfrel2 6189
[TakeutiZaring] p. 25Exercise 3xpss 5693
[TakeutiZaring] p. 25Exercise 5relun 5812
[TakeutiZaring] p. 25Exercise 6reluni 5819
[TakeutiZaring] p. 25Exercise 9inxp 5833
[TakeutiZaring] p. 25Exercise 12relres 6011
[TakeutiZaring] p. 25Exercise 13opelres 5988  opelresi 5990
[TakeutiZaring] p. 25Exercise 14dmres 6004
[TakeutiZaring] p. 25Exercise 15resss 6007
[TakeutiZaring] p. 25Exercise 17resabs1 6012
[TakeutiZaring] p. 25Exercise 18funres 6591
[TakeutiZaring] p. 25Exercise 24relco 6108
[TakeutiZaring] p. 25Exercise 29funco 6589
[TakeutiZaring] p. 25Exercise 30f1co 6800
[TakeutiZaring] p. 26Definition 6.10eu2 2606
[TakeutiZaring] p. 26Definition 6.11conventions 29653  df-fv 6552  fv3 6910
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7916  cnvexg 7915
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7902  dmexg 7894
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7903  rnexg 7895
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 43213
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7911
[TakeutiZaring] p. 27Corollary 6.13fvex 6905
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 45882  tz6.12-1-afv2 45949  tz6.12-1 6915  tz6.12-afv 45881  tz6.12-afv2 45948  tz6.12 6917  tz6.12c-afv2 45950  tz6.12c 6914
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 45945  tz6.12-2 6880  tz6.12i-afv2 45951  tz6.12i 6920
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6547
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6548
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6550  wfo 6542
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6549  wf1 6541
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6551  wf1o 6543
[TakeutiZaring] p. 28Exercise 4eqfnfv 7033  eqfnfv2 7034  eqfnfv2f 7037
[TakeutiZaring] p. 28Exercise 5fvco 6990
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7219
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7217
[TakeutiZaring] p. 29Exercise 9funimaex 6637  funimaexg 6635
[TakeutiZaring] p. 29Definition 6.18df-br 5150
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5590
[TakeutiZaring] p. 30Definition 6.21dffr2 5641  dffr3 6099  eliniseg 6094  iniseg 6097
[TakeutiZaring] p. 30Definition 6.22df-eprel 5581
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5655  fr3nr 7759  frirr 5654
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5632
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7761
[TakeutiZaring] p. 31Exercise 1frss 5644
[TakeutiZaring] p. 31Exercise 4wess 5664
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6349  tz6.26i 6351  wefrc 5671  wereu2 5674
[TakeutiZaring] p. 32Theorem 6.27wfi 6352  wfii 6354
[TakeutiZaring] p. 32Definition 6.28df-isom 6553
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7326
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7327
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7333
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7334
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7335
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7339
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7346
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7348
[TakeutiZaring] p. 35Notationwtr 5266
[TakeutiZaring] p. 35Theorem 7.2trelpss 43214  tz7.2 5661
[TakeutiZaring] p. 35Definition 7.1dftr3 5272
[TakeutiZaring] p. 36Proposition 7.4ordwe 6378
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6386
[TakeutiZaring] p. 36Proposition 7.6ordelord 6387  ordelordALT 43298  ordelordALTVD 43628
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6393  ordelssne 6392
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6391
[TakeutiZaring] p. 37Proposition 7.9ordin 6395
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7769
[TakeutiZaring] p. 38Corollary 7.15ordsson 7770
[TakeutiZaring] p. 38Definition 7.11df-on 6369
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6397
[TakeutiZaring] p. 38Proposition 7.12onfrALT 43310  ordon 7764
[TakeutiZaring] p. 38Proposition 7.13onprc 7765
[TakeutiZaring] p. 39Theorem 7.17tfi 7842
[TakeutiZaring] p. 40Exercise 3ontr2 6412
[TakeutiZaring] p. 40Exercise 7dftr2 5268
[TakeutiZaring] p. 40Exercise 9onssmin 7780
[TakeutiZaring] p. 40Exercise 11unon 7819
[TakeutiZaring] p. 40Exercise 12ordun 6469
[TakeutiZaring] p. 40Exercise 14ordequn 6468
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7766
[TakeutiZaring] p. 40Proposition 7.20elssuni 4942
[TakeutiZaring] p. 41Definition 7.22df-suc 6371
[TakeutiZaring] p. 41Proposition 7.23sssucid 6445  sucidg 6446
[TakeutiZaring] p. 41Proposition 7.24onsuc 7799
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6459  ordnbtwn 6458
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7816
[TakeutiZaring] p. 42Exercise 1df-lim 6370
[TakeutiZaring] p. 42Exercise 4omssnlim 7870
[TakeutiZaring] p. 42Exercise 7ssnlim 7875
[TakeutiZaring] p. 42Exercise 8onsucssi 7830  ordelsuc 7808
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7810
[TakeutiZaring] p. 42Definition 7.27nlimon 7840
[TakeutiZaring] p. 42Definition 7.28dfom2 7857
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7879
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7881
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7882
[TakeutiZaring] p. 43Remarkomon 7867
[TakeutiZaring] p. 43Axiom 7inf3 9630  omex 9638
[TakeutiZaring] p. 43Theorem 7.32ordom 7865
[TakeutiZaring] p. 43Corollary 7.31find 7887
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7883
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7884
[TakeutiZaring] p. 44Exercise 1limomss 7860
[TakeutiZaring] p. 44Exercise 2int0 4967
[TakeutiZaring] p. 44Exercise 3trintss 5285
[TakeutiZaring] p. 44Exercise 4intss1 4968
[TakeutiZaring] p. 44Exercise 5intex 5338
[TakeutiZaring] p. 44Exercise 6oninton 7783
[TakeutiZaring] p. 44Exercise 11ordintdif 6415
[TakeutiZaring] p. 44Definition 7.35df-int 4952
[TakeutiZaring] p. 44Proposition 7.34noinfep 9655
[TakeutiZaring] p. 45Exercise 4onint 7778
[TakeutiZaring] p. 47Lemma 1tfrlem1 8376
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8397
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8398
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8399
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8406  tz7.44-2 8407  tz7.44-3 8408
[TakeutiZaring] p. 50Exercise 1smogt 8367
[TakeutiZaring] p. 50Exercise 3smoiso 8362
[TakeutiZaring] p. 50Definition 7.46df-smo 8346
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8445  tz7.49c 8446
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8443
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8442
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8444
[TakeutiZaring] p. 53Proposition 7.532eu5 2652
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10006
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10007
[TakeutiZaring] p. 56Definition 8.1oalim 8532  oasuc 8524
[TakeutiZaring] p. 57Remarktfindsg 7850
[TakeutiZaring] p. 57Proposition 8.2oacl 8535
[TakeutiZaring] p. 57Proposition 8.3oa0 8516  oa0r 8538
[TakeutiZaring] p. 57Proposition 8.16omcl 8536
[TakeutiZaring] p. 58Corollary 8.5oacan 8548
[TakeutiZaring] p. 58Proposition 8.4nnaord 8619  nnaordi 8618  oaord 8547  oaordi 8546
[TakeutiZaring] p. 59Proposition 8.6iunss2 5053  uniss2 4946
[TakeutiZaring] p. 59Proposition 8.7oawordri 8550
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8555  oawordex 8557
[TakeutiZaring] p. 59Proposition 8.9nnacl 8611
[TakeutiZaring] p. 59Proposition 8.10oaabs 8647
[TakeutiZaring] p. 60Remarkoancom 9646
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8560
[TakeutiZaring] p. 62Exercise 1nnarcl 8616
[TakeutiZaring] p. 62Exercise 5oaword1 8552
[TakeutiZaring] p. 62Definition 8.15om0x 8519  omlim 8533  omsuc 8526
[TakeutiZaring] p. 62Definition 8.15(a)om0 8517
[TakeutiZaring] p. 63Proposition 8.17nnecl 8613  nnmcl 8612
[TakeutiZaring] p. 63Proposition 8.19nnmord 8632  nnmordi 8631  omord 8568  omordi 8566
[TakeutiZaring] p. 63Proposition 8.20omcan 8569
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8636  omwordri 8572
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8539
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8542  om1r 8543
[TakeutiZaring] p. 64Proposition 8.22om00 8575
[TakeutiZaring] p. 64Proposition 8.23omordlim 8577
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8578
[TakeutiZaring] p. 64Proposition 8.25odi 8579
[TakeutiZaring] p. 65Theorem 8.26omass 8580
[TakeutiZaring] p. 67Definition 8.30nnesuc 8608  oe0 8522  oelim 8534  oesuc 8527  onesuc 8530
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8520
[TakeutiZaring] p. 67Proposition 8.32oen0 8586
[TakeutiZaring] p. 67Proposition 8.33oeordi 8587
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8521
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8545
[TakeutiZaring] p. 68Corollary 8.34oeord 8588
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8594
[TakeutiZaring] p. 68Proposition 8.35oewordri 8592
[TakeutiZaring] p. 68Proposition 8.37oeworde 8593
[TakeutiZaring] p. 69Proposition 8.41oeoa 8597
[TakeutiZaring] p. 70Proposition 8.42oeoe 8599
[TakeutiZaring] p. 73Theorem 9.1trcl 9723  tz9.1 9724
[TakeutiZaring] p. 76Definition 9.9df-r1 9759  r10 9763  r1lim 9767  r1limg 9766  r1suc 9765  r1sucg 9764
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9775  r1ord2 9776  r1ordg 9773
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9785
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9810  tz9.13 9786  tz9.13g 9787
[TakeutiZaring] p. 79Definition 9.14df-rank 9760  rankval 9811  rankvalb 9792  rankvalg 9812
[TakeutiZaring] p. 79Proposition 9.16rankel 9834  rankelb 9819
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9848  rankval3 9835  rankval3b 9821
[TakeutiZaring] p. 79Proposition 9.18rankonid 9824
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9790
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9829  rankr1c 9816  rankr1g 9827
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9830
[TakeutiZaring] p. 80Exercise 1rankss 9844  rankssb 9843
[TakeutiZaring] p. 80Exercise 2unbndrank 9837
[TakeutiZaring] p. 80Proposition 9.19bndrank 9836
[TakeutiZaring] p. 83Axiom of Choiceac4 10470  dfac3 10116
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10025  numth 10467  numth2 10466
[TakeutiZaring] p. 85Definition 10.4cardval 10541
[TakeutiZaring] p. 85Proposition 10.5cardid 10542  cardid2 9948
[TakeutiZaring] p. 85Proposition 10.9oncard 9955
[TakeutiZaring] p. 85Proposition 10.10carden 10546
[TakeutiZaring] p. 85Proposition 10.11cardidm 9954
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9939
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9960
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9952
[TakeutiZaring] p. 87Proposition 10.15pwen 9150
[TakeutiZaring] p. 88Exercise 1en0 9013
[TakeutiZaring] p. 88Exercise 7infensuc 9155
[TakeutiZaring] p. 89Exercise 10omxpen 9074
[TakeutiZaring] p. 90Corollary 10.23cardnn 9958
[TakeutiZaring] p. 90Definition 10.27alephiso 10093
[TakeutiZaring] p. 90Proposition 10.20nneneq 9209
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9228
[TakeutiZaring] p. 90Proposition 10.26alephprc 10094
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9214
[TakeutiZaring] p. 91Exercise 2alephle 10083
[TakeutiZaring] p. 91Exercise 3aleph0 10061
[TakeutiZaring] p. 91Exercise 4cardlim 9967
[TakeutiZaring] p. 91Exercise 7infpss 10212
[TakeutiZaring] p. 91Exercise 8infcntss 9321
[TakeutiZaring] p. 91Definition 10.29df-fin 8943  isfi 8972
[TakeutiZaring] p. 92Proposition 10.32onfin 9230
[TakeutiZaring] p. 92Proposition 10.34imadomg 10529
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9067
[TakeutiZaring] p. 93Proposition 10.35fodomb 10521
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10180  unxpdom 9253
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9969  cardsdomelir 9968
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9255
[TakeutiZaring] p. 94Proposition 10.39infxpen 10009
[TakeutiZaring] p. 95Definition 10.42df-map 8822
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10557  infxpidm2 10012
[TakeutiZaring] p. 95Proposition 10.41infdju 10203  infxp 10210
[TakeutiZaring] p. 96Proposition 10.44pw2en 9079  pw2f1o 9077
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9143
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10482
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10477  ac6s5 10486
[TakeutiZaring] p. 98Theorem 10.47unidom 10538
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10539  uniimadomf 10540
[TakeutiZaring] p. 100Definition 11.1cfcof 10269
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10264
[TakeutiZaring] p. 102Exercise 1cfle 10249
[TakeutiZaring] p. 102Exercise 2cf0 10246
[TakeutiZaring] p. 102Exercise 3cfsuc 10252
[TakeutiZaring] p. 102Exercise 4cfom 10259
[TakeutiZaring] p. 102Proposition 11.9coftr 10268
[TakeutiZaring] p. 103Theorem 11.15alephreg 10577
[TakeutiZaring] p. 103Proposition 11.11cardcf 10247
[TakeutiZaring] p. 103Proposition 11.13alephsing 10271
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10092
[TakeutiZaring] p. 104Proposition 11.16carduniima 10091
[TakeutiZaring] p. 104Proposition 11.18alephfp 10103  alephfp2 10104
[TakeutiZaring] p. 106Theorem 11.20gchina 10694
[TakeutiZaring] p. 106Theorem 11.21mappwen 10107
[TakeutiZaring] p. 107Theorem 11.26konigth 10564
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10578
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10579
[Tarski] p. 67Axiom B5ax-c5 37753
[Tarski] p. 67Scheme B5sp 2177
[Tarski] p. 68Lemma 6avril1 29716  equid 2016
[Tarski] p. 69Lemma 7equcomi 2021
[Tarski] p. 70Lemma 14spim 2387  spime 2389  spimew 1976
[Tarski] p. 70Lemma 16ax-12 2172  ax-c15 37759  ax12i 1971
[Tarski] p. 70Lemmas 16 and 17sb6 2089
[Tarski] p. 75Axiom B7ax6v 1973
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1914  ax5ALT 37777
[Tarski], p. 75Scheme B8 of system S2ax-7 2012  ax-8 2109  ax-9 2117
[Tarski1999] p. 178Axiom 4axtgsegcon 27715
[Tarski1999] p. 178Axiom 5axtg5seg 27716
[Tarski1999] p. 179Axiom 7axtgpasch 27718
[Tarski1999] p. 180Axiom 7.1axtgpasch 27718
[Tarski1999] p. 185Axiom 11axtgcont1 27719
[Truss] p. 114Theorem 5.18ruc 16186
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 36527
[Viaclovsky8] p. 3Proposition 7ismblfin 36529
[Weierstrass] p. 272Definitiondf-mdet 22087  mdetuni 22124
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 903
[WhiteheadRussell] p. 96Axiom *1.3olc 867
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 868
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 919
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 967
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 188
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 36326
[WhiteheadRussell] p. 100Theorem *2.05frege5 42551  imim2 58  wl-luk-imim2 36321
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 45729  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2659  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 36324
[WhiteheadRussell] p. 101Theorem *2.11exmid 894
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 897
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 43688  wl-luk-notnotr 36325
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 42581  axfrege28 42580  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 866
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 924
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 36318
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 889
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 939
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 29654  pm2.27 42  wl-luk-pm2.27 36316
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 37232
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 923
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 969
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 970
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 968
[WhiteheadRussell] p. 105Definition *2.33df-3or 1089
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 906
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 907
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 942
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 881
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 882
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 190
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 883
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 884
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 885
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 850
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 851
[WhiteheadRussell] p. 107Theorem *2.55orel1 888
[WhiteheadRussell] p. 107Theorem *2.56orel2 890
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 191
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 899
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 940
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 941
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 192
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 891  pm2.67 892
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 898
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 972
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 900
[WhiteheadRussell] p. 108Theorem *2.69looinv 202
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 973
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 974
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 933
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 931
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 971
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 975
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 932
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 991
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 471  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 992
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 993
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 994
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 995
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 473
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 461
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 404
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 802
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 450
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 451
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 484  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 486  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 764
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 765
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 807
[WhiteheadRussell] p. 113Fact)pm3.45 623
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 809
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 494
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 495
[WhiteheadRussell] p. 113Theorem *3.44jao 960  pm3.44 959
[WhiteheadRussell] p. 113Theorem *3.47anim12 808
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 475
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 963
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 261
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 354
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 806
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 832
[WhiteheadRussell] p. 117Theorem *4.21bicom 221
[WhiteheadRussell] p. 117Theorem *4.22biantr 805  bitr 804
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 565
[WhiteheadRussell] p. 117Theorem *4.25oridm 904  pm4.25 905
[WhiteheadRussell] p. 118Theorem *4.3ancom 462
[WhiteheadRussell] p. 118Theorem *4.4andi 1007
[WhiteheadRussell] p. 118Theorem *4.31orcom 869
[WhiteheadRussell] p. 118Theorem *4.32anass 470
[WhiteheadRussell] p. 118Theorem *4.33orass 921
[WhiteheadRussell] p. 118Theorem *4.36anbi1 633
[WhiteheadRussell] p. 118Theorem *4.37orbi1 917
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 637
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 976
[WhiteheadRussell] p. 118Definition *4.34df-3an 1090
[WhiteheadRussell] p. 119Theorem *4.41ordi 1005
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1053
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1022
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 996
[WhiteheadRussell] p. 119Theorem *4.45orabs 998  pm4.45 997  pm4.45im 827
[WhiteheadRussell] p. 120Theorem *4.5anor 982
[WhiteheadRussell] p. 120Theorem *4.6imor 852
[WhiteheadRussell] p. 120Theorem *4.7anclb 547
[WhiteheadRussell] p. 120Theorem *4.51ianor 981
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 984
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 985
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 986
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 987
[WhiteheadRussell] p. 120Theorem *4.56ioran 983  pm4.56 988
[WhiteheadRussell] p. 120Theorem *4.57oran 989  pm4.57 990
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 406
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 855
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 399
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 848
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 407
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 849
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 400
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 559  pm4.71d 563  pm4.71i 561  pm4.71r 560  pm4.71rd 564  pm4.71ri 562
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 949
[WhiteheadRussell] p. 121Theorem *4.73iba 529
[WhiteheadRussell] p. 121Theorem *4.74biorf 936
[WhiteheadRussell] p. 121Theorem *4.76jcab 519  pm4.76 520
[WhiteheadRussell] p. 121Theorem *4.77jaob 961  pm4.77 962
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 934
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1003
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 394
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 395
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1023
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1024
[WhiteheadRussell] p. 122Theorem *4.84imbi1 348
[WhiteheadRussell] p. 122Theorem *4.85imbi2 349
[WhiteheadRussell] p. 122Theorem *4.86bibi1 352
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 389  impexp 452  pm4.87 842
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 823
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 944  pm5.11g 943
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 945
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 947
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 946
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1012
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1013
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1011
[WhiteheadRussell] p. 124Theorem *5.18nbbn 385  pm5.18 383
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 388
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 824
[WhiteheadRussell] p. 124Theorem *5.22xor 1014
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1049
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1050
[WhiteheadRussell] p. 124Theorem *5.25dfor2 901
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 574
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 390
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 362
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1001
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 953
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 830
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 575
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 835
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 825
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 833
[WhiteheadRussell] p. 125Theorem *5.41imdi 391  pm5.41 392
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 545
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 544
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1004
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1017
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 948
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1000
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1018
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1019
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1027
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 367
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1028
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 43117
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 43118
[WhiteheadRussell] p. 147Theorem *10.2219.26 1874
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 43119
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 43120
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 43121
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1897
[WhiteheadRussell] p. 151Theorem *10.301albitr 43122
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 43123
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 43124
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 43125
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 43126
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 43128
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 43129
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 43130
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 43127
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2094
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 43133
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 43134
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2074
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2158
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1832
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1833
[WhiteheadRussell] p. 161Theorem *11.319.21vv 43135
[WhiteheadRussell] p. 162Theorem *11.322alim 43136
[WhiteheadRussell] p. 162Theorem *11.332albi 43137
[WhiteheadRussell] p. 162Theorem *11.342exim 43138
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 43140
[WhiteheadRussell] p. 162Theorem *11.3412exbi 43139
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1891
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 43142
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 43143
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 43141
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1831
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 43144
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 43145
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1849
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 43146
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2343
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1864
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 43151
[WhiteheadRussell] p. 165Theorem *11.56aaanv 43147
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 43148
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 43149
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 43150
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 43155
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 43152
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 43153
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 43154
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 43156
[WhiteheadRussell] p. 175Definition *14.02df-eu 2564
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 43166  pm13.13b 43167
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 43168
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3023
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3024
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3657
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 43174
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 43175
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 43169
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 43313  pm13.193 43170
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 43171
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 43172
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 43173
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 43180
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 43179
[WhiteheadRussell] p. 184Definition *14.01iotasbc 43178
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3846
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 43181  pm14.122b 43182  pm14.122c 43183
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 43184  pm14.123b 43185  pm14.123c 43186
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 43188
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 43187
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 43189
[WhiteheadRussell] p. 190Theorem *14.22iota4 6525
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 43190
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6526
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 43191
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 43193
[WhiteheadRussell] p. 192Theorem *14.26eupick 2630  eupickbi 2633  sbaniota 43194
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 43192
[WhiteheadRussell] p. 192Theorem *14.271eubi 2579
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 43196
[WhiteheadRussell] p. 235Definition *30.01conventions 29653  df-fv 6552
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9996  pm54.43lem 9995
[Young] p. 141Definition of operator orderingleop2 31377
[Young] p. 142Example 12.2(i)0leop 31383  idleop 31384
[vandenDries] p. 42Lemma 61irrapx1 41566
[vandenDries] p. 43Theorem 62pellex 41573  pellexlem1 41567

This page was last updated on 4-Apr-2025.
Copyright terms: Public domain