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 17377
[Adamek] p. 21Condition 3.1(b)df-cat 17377
[Adamek] p. 22Example 3.3(1)df-setc 17791
[Adamek] p. 24Example 3.3(4.c)0cat 17398
[Adamek] p. 24Example 3.3(4.d)df-prstc 46344  prsthinc 46335
[Adamek] p. 24Example 3.3(4.e)df-mndtc 46365  df-mndtc 46365
[Adamek] p. 25Definition 3.5df-oppc 17421
[Adamek] p. 28Remark 3.9oppciso 17493
[Adamek] p. 28Remark 3.12invf1o 17481  invisoinvl 17502
[Adamek] p. 28Example 3.13idinv 17501  idiso 17500
[Adamek] p. 28Corollary 3.11inveq 17486
[Adamek] p. 28Definition 3.8df-inv 17460  df-iso 17461  dfiso2 17484
[Adamek] p. 28Proposition 3.10sectcan 17467
[Adamek] p. 29Remark 3.16cicer 17518
[Adamek] p. 29Definition 3.15cic 17511  df-cic 17508
[Adamek] p. 29Definition 3.17df-func 17573
[Adamek] p. 29Proposition 3.14(1)invinv 17482
[Adamek] p. 29Proposition 3.14(2)invco 17483  isoco 17489
[Adamek] p. 30Remark 3.19df-func 17573
[Adamek] p. 30Example 3.20(1)idfucl 17596
[Adamek] p. 32Proposition 3.21funciso 17589
[Adamek] p. 33Example 3.26(2)df-thinc 46301  prsthinc 46335  thincciso 46330
[Adamek] p. 33Example 3.26(3)df-mndtc 46365
[Adamek] p. 33Proposition 3.23cofucl 17603
[Adamek] p. 34Remark 3.28(2)catciso 17826
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 17884
[Adamek] p. 34Definition 3.27(2)df-fth 17621
[Adamek] p. 34Definition 3.27(3)df-full 17620
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 17884
[Adamek] p. 35Corollary 3.32ffthiso 17645
[Adamek] p. 35Proposition 3.30(c)cofth 17651
[Adamek] p. 35Proposition 3.30(d)cofull 17650
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 17869
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 17869
[Adamek] p. 39Definition 3.41funcoppc 17590
[Adamek] p. 39Definition 3.44.df-catc 17814
[Adamek] p. 39Proposition 3.43(c)fthoppc 17639
[Adamek] p. 39Proposition 3.43(d)fulloppc 17638
[Adamek] p. 40Remark 3.48catccat 17823
[Adamek] p. 40Definition 3.47df-catc 17814
[Adamek] p. 48Example 4.3(1.a)0subcat 17553
[Adamek] p. 48Example 4.3(1.b)catsubcat 17554
[Adamek] p. 48Definition 4.1(2)fullsubc 17565
[Adamek] p. 48Definition 4.1(a)df-subc 17524
[Adamek] p. 49Remark 4.4(2)ressffth 17654
[Adamek] p. 83Definition 6.1df-nat 17659
[Adamek] p. 87Remark 6.14(a)fuccocl 17682
[Adamek] p. 87Remark 6.14(b)fucass 17686
[Adamek] p. 87Definition 6.15df-fuc 17660
[Adamek] p. 88Remark 6.16fuccat 17688
[Adamek] p. 101Definition 7.1df-inito 17699
[Adamek] p. 101Example 7.2 (6)irinitoringc 45627
[Adamek] p. 102Definition 7.4df-termo 17700
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17727
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17731
[Adamek] p. 103Definition 7.7df-zeroo 17701
[Adamek] p. 103Example 7.9 (3)nzerooringczr 45630
[Adamek] p. 103Proposition 7.6termoeu1w 17734
[Adamek] p. 106Definition 7.19df-sect 17459
[Adamek] p. 185Section 10.67updjud 9692
[Adamek] p. 478Item Rngdf-ringc 45563
[AhoHopUll] p. 2Section 1.1df-bigo 45894
[AhoHopUll] p. 12Section 1.3df-blen 45916
[AhoHopUll] p. 318Section 9.1df-concat 14274  df-pfx 14384  df-substr 14354  df-word 14218  lencl 14236  wrd0 14242
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 23872  df-nmoo 29107
[AkhiezerGlazman] p. 64Theoremhmopidmch 30515  hmopidmchi 30513
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 30563  pjcmul2i 30564
[AkhiezerGlazman] p. 72Theoremcnvunop 30280  unoplin 30282
[AkhiezerGlazman] p. 72Equation 2unopadj 30281  unopadj2 30300
[AkhiezerGlazman] p. 73Theoremelunop2 30375  lnopunii 30374
[AkhiezerGlazman] p. 80Proposition 1adjlnop 30448
[Alling] p. 125Theorem 4.02(12)cofcutrtime 34093
[Alling] p. 184Axiom Bbdayfo 33880
[Alling] p. 184Axiom Osltso 33879
[Alling] p. 184Axiom SDnodense 33895
[Alling] p. 185Lemma 0nocvxmin 33973
[Alling] p. 185Theoremconway 33993
[Alling] p. 185Axiom FEnoeta 33946
[Alling] p. 186Theorem 4slerec 34013
[Apostol] p. 18Theorem I.1addcan 11159  addcan2d 11179  addcan2i 11169  addcand 11178  addcani 11168
[Apostol] p. 18Theorem I.2negeu 11211
[Apostol] p. 18Theorem I.3negsub 11269  negsubd 11338  negsubi 11299
[Apostol] p. 18Theorem I.4negneg 11271  negnegd 11323  negnegi 11291
[Apostol] p. 18Theorem I.5subdi 11408  subdid 11431  subdii 11424  subdir 11409  subdird 11432  subdiri 11425
[Apostol] p. 18Theorem I.6mul01 11154  mul01d 11174  mul01i 11165  mul02 11153  mul02d 11173  mul02i 11164
[Apostol] p. 18Theorem I.7mulcan 11612  mulcan2d 11609  mulcand 11608  mulcani 11614
[Apostol] p. 18Theorem I.8receu 11620  xreceu 31196
[Apostol] p. 18Theorem I.9divrec 11649  divrecd 11754  divreci 11720  divreczi 11713
[Apostol] p. 18Theorem I.10recrec 11672  recreci 11707
[Apostol] p. 18Theorem I.11mul0or 11615  mul0ord 11625  mul0ori 11623
[Apostol] p. 18Theorem I.12mul2neg 11414  mul2negd 11430  mul2negi 11423  mulneg1 11411  mulneg1d 11428  mulneg1i 11421
[Apostol] p. 18Theorem I.13divadddiv 11690  divadddivd 11795  divadddivi 11737
[Apostol] p. 18Theorem I.14divmuldiv 11675  divmuldivd 11792  divmuldivi 11735  rdivmuldivd 31488
[Apostol] p. 18Theorem I.15divdivdiv 11676  divdivdivd 11798  divdivdivi 11738
[Apostol] p. 20Axiom 7rpaddcl 12752  rpaddcld 12787  rpmulcl 12753  rpmulcld 12788
[Apostol] p. 20Axiom 8rpneg 12762
[Apostol] p. 20Axiom 90nrp 12765
[Apostol] p. 20Theorem I.17lttri 11101
[Apostol] p. 20Theorem I.18ltadd1d 11568  ltadd1dd 11586  ltadd1i 11529
[Apostol] p. 20Theorem I.19ltmul1 11825  ltmul1a 11824  ltmul1i 11893  ltmul1ii 11903  ltmul2 11826  ltmul2d 12814  ltmul2dd 12828  ltmul2i 11896
[Apostol] p. 20Theorem I.20msqgt0 11495  msqgt0d 11542  msqgt0i 11512
[Apostol] p. 20Theorem I.210lt1 11497
[Apostol] p. 20Theorem I.23lt0neg1 11481  lt0neg1d 11544  ltneg 11475  ltnegd 11553  ltnegi 11519
[Apostol] p. 20Theorem I.25lt2add 11460  lt2addd 11598  lt2addi 11537
[Apostol] p. 20Definition of positive numbersdf-rp 12731
[Apostol] p. 21Exercise 4recgt0 11821  recgt0d 11909  recgt0i 11880  recgt0ii 11881
[Apostol] p. 22Definition of integersdf-z 12320
[Apostol] p. 22Definition of positive integersdfnn3 11987
[Apostol] p. 22Definition of rationalsdf-q 12689
[Apostol] p. 24Theorem I.26supeu 9213
[Apostol] p. 26Theorem I.28nnunb 12229
[Apostol] p. 26Theorem I.29arch 12230
[Apostol] p. 28Exercise 2btwnz 12423
[Apostol] p. 28Exercise 3nnrecl 12231
[Apostol] p. 28Exercise 4rebtwnz 12687
[Apostol] p. 28Exercise 5zbtwnre 12686
[Apostol] p. 28Exercise 6qbtwnre 12933
[Apostol] p. 28Exercise 10(a)zeneo 16048  zneo 12403  zneoALTV 45121
[Apostol] p. 29Theorem I.35cxpsqrtth 25884  msqsqrtd 15152  resqrtth 14967  sqrtth 15076  sqrtthi 15082  sqsqrtd 15151
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 11976
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12653
[Apostol] p. 361Remarkcrreczi 13943
[Apostol] p. 363Remarkabsgt0i 15111
[Apostol] p. 363Exampleabssubd 15165  abssubi 15115
[ApostolNT] p. 7Remarkfmtno0 44992  fmtno1 44993  fmtno2 45002  fmtno3 45003  fmtno4 45004  fmtno5fac 45034  fmtnofz04prm 45029
[ApostolNT] p. 7Definitiondf-fmtno 44980
[ApostolNT] p. 8Definitiondf-ppi 26249
[ApostolNT] p. 14Definitiondf-dvds 15964
[ApostolNT] p. 14Theorem 1.1(a)iddvds 15979
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16003
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 15998
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 15992
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 15994
[ApostolNT] p. 14Theorem 1.1(f)1dvds 15980
[ApostolNT] p. 14Theorem 1.1(g)dvds0 15981
[ApostolNT] p. 14Theorem 1.1(h)0dvds 15986
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16020
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16022
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16024
[ApostolNT] p. 15Definitiondf-gcd 16202  dfgcd2 16254
[ApostolNT] p. 16Definitionisprm2 16387
[ApostolNT] p. 16Theorem 1.5coprmdvds 16358
[ApostolNT] p. 16Theorem 1.7prminf 16616
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16220
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16255
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16257
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16235
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16227
[ApostolNT] p. 17Theorem 1.8coprm 16416
[ApostolNT] p. 17Theorem 1.9euclemma 16418
[ApostolNT] p. 17Theorem 1.101arith2 16629
[ApostolNT] p. 18Theorem 1.13prmrec 16623
[ApostolNT] p. 19Theorem 1.14divalg 16112
[ApostolNT] p. 20Theorem 1.15eucalg 16292
[ApostolNT] p. 24Definitiondf-mu 26250
[ApostolNT] p. 25Definitiondf-phi 16467
[ApostolNT] p. 25Theorem 2.1musum 26340
[ApostolNT] p. 26Theorem 2.2phisum 16491
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16477
[ApostolNT] p. 28Theorem 2.5(c)phimul 16481
[ApostolNT] p. 32Definitiondf-vma 26247
[ApostolNT] p. 32Theorem 2.9muinv 26342
[ApostolNT] p. 32Theorem 2.10vmasum 26364
[ApostolNT] p. 38Remarkdf-sgm 26251
[ApostolNT] p. 38Definitiondf-sgm 26251
[ApostolNT] p. 75Definitiondf-chp 26248  df-cht 26246
[ApostolNT] p. 104Definitioncongr 16369
[ApostolNT] p. 106Remarkdvdsval3 15967
[ApostolNT] p. 106Definitionmoddvds 15974
[ApostolNT] p. 107Example 2mod2eq0even 16055
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16056
[ApostolNT] p. 107Example 4zmod1congr 13608
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13645
[ApostolNT] p. 107Theorem 5.2(c)modexp 13953
[ApostolNT] p. 108Theorem 5.3modmulconst 15997
[ApostolNT] p. 109Theorem 5.4cncongr1 16372
[ApostolNT] p. 109Theorem 5.6gcdmodi 16775
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16374
[ApostolNT] p. 113Theorem 5.17eulerth 16484
[ApostolNT] p. 113Theorem 5.18vfermltl 16502
[ApostolNT] p. 114Theorem 5.19fermltl 16485
[ApostolNT] p. 116Theorem 5.24wilthimp 26221
[ApostolNT] p. 179Definitiondf-lgs 26443  lgsprme0 26487
[ApostolNT] p. 180Example 11lgs 26488
[ApostolNT] p. 180Theorem 9.2lgsvalmod 26464
[ApostolNT] p. 180Theorem 9.3lgsdirprm 26479
[ApostolNT] p. 181Theorem 9.4m1lgs 26536
[ApostolNT] p. 181Theorem 9.52lgs 26555  2lgsoddprm 26564
[ApostolNT] p. 182Theorem 9.6gausslemma2d 26522
[ApostolNT] p. 185Theorem 9.8lgsquad 26531
[ApostolNT] p. 188Definitiondf-lgs 26443  lgs1 26489
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 26480
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 26482
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 26490
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 26491
[Baer] p. 40Property (b)mapdord 39652
[Baer] p. 40Property (c)mapd11 39653
[Baer] p. 40Property (e)mapdin 39676  mapdlsm 39678
[Baer] p. 40Property (f)mapd0 39679
[Baer] p. 40Definition of projectivitydf-mapd 39639  mapd1o 39662
[Baer] p. 41Property (g)mapdat 39681
[Baer] p. 44Part (1)mapdpg 39720
[Baer] p. 45Part (2)hdmap1eq 39815  mapdheq 39742  mapdheq2 39743  mapdheq2biN 39744
[Baer] p. 45Part (3)baerlem3 39727
[Baer] p. 46Part (4)mapdheq4 39746  mapdheq4lem 39745
[Baer] p. 46Part (5)baerlem5a 39728  baerlem5abmN 39732  baerlem5amN 39730  baerlem5b 39729  baerlem5bmN 39731
[Baer] p. 47Part (6)hdmap1l6 39835  hdmap1l6a 39823  hdmap1l6e 39828  hdmap1l6f 39829  hdmap1l6g 39830  hdmap1l6lem1 39821  hdmap1l6lem2 39822  mapdh6N 39761  mapdh6aN 39749  mapdh6eN 39754  mapdh6fN 39755  mapdh6gN 39756  mapdh6lem1N 39747  mapdh6lem2N 39748
[Baer] p. 48Part 9hdmapval 39842
[Baer] p. 48Part 10hdmap10 39854
[Baer] p. 48Part 11hdmapadd 39857
[Baer] p. 48Part (6)hdmap1l6h 39831  mapdh6hN 39757
[Baer] p. 48Part (7)mapdh75cN 39767  mapdh75d 39768  mapdh75e 39766  mapdh75fN 39769  mapdh7cN 39763  mapdh7dN 39764  mapdh7eN 39762  mapdh7fN 39765
[Baer] p. 48Part (8)mapdh8 39802  mapdh8a 39789  mapdh8aa 39790  mapdh8ab 39791  mapdh8ac 39792  mapdh8ad 39793  mapdh8b 39794  mapdh8c 39795  mapdh8d 39797  mapdh8d0N 39796  mapdh8e 39798  mapdh8g 39799  mapdh8i 39800  mapdh8j 39801
[Baer] p. 48Part (9)mapdh9a 39803
[Baer] p. 48Equation 10mapdhvmap 39783
[Baer] p. 49Part 12hdmap11 39862  hdmapeq0 39858  hdmapf1oN 39879  hdmapneg 39860  hdmaprnN 39878  hdmaprnlem1N 39863  hdmaprnlem3N 39864  hdmaprnlem3uN 39865  hdmaprnlem4N 39867  hdmaprnlem6N 39868  hdmaprnlem7N 39869  hdmaprnlem8N 39870  hdmaprnlem9N 39871  hdmapsub 39861
[Baer] p. 49Part 14hdmap14lem1 39882  hdmap14lem10 39891  hdmap14lem1a 39880  hdmap14lem2N 39883  hdmap14lem2a 39881  hdmap14lem3 39884  hdmap14lem8 39889  hdmap14lem9 39890
[Baer] p. 50Part 14hdmap14lem11 39892  hdmap14lem12 39893  hdmap14lem13 39894  hdmap14lem14 39895  hdmap14lem15 39896  hgmapval 39901
[Baer] p. 50Part 15hgmapadd 39908  hgmapmul 39909  hgmaprnlem2N 39911  hgmapvs 39905
[Baer] p. 50Part 16hgmaprnN 39915
[Baer] p. 110Lemma 1hdmapip0com 39931
[Baer] p. 110Line 27hdmapinvlem1 39932
[Baer] p. 110Line 28hdmapinvlem2 39933
[Baer] p. 110Line 30hdmapinvlem3 39934
[Baer] p. 110Part 1.2hdmapglem5 39936  hgmapvv 39940
[Baer] p. 110Proposition 1hdmapinvlem4 39935
[Baer] p. 111Line 10hgmapvvlem1 39937
[Baer] p. 111Line 15hdmapg 39944  hdmapglem7 39943
[Bauer], p. 483Theorem 1.22irrexpq 25885  2irrexpqALT 25950
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2569
[BellMachover] p. 460Notationdf-mo 2540
[BellMachover] p. 460Definitionmo3 2564
[BellMachover] p. 461Axiom Extax-ext 2709
[BellMachover] p. 462Theorem 1.1axextmo 2713
[BellMachover] p. 463Axiom Repaxrep5 5215
[BellMachover] p. 463Scheme Sepax-sep 5223
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 35235  bm1.3ii 5226
[BellMachover] p. 466Problemaxpow2 5290
[BellMachover] p. 466Axiom Powaxpow3 5291
[BellMachover] p. 466Axiom Unionaxun2 7590
[BellMachover] p. 468Definitiondf-ord 6269
[BellMachover] p. 469Theorem 2.2(i)ordirr 6284
[BellMachover] p. 469Theorem 2.2(iii)onelon 6291
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6286
[BellMachover] p. 471Definition of Ndf-om 7713
[BellMachover] p. 471Problem 2.5(ii)uniordint 7651
[BellMachover] p. 471Definition of Limdf-lim 6271
[BellMachover] p. 472Axiom Infzfinf2 9400
[BellMachover] p. 473Theorem 2.8limom 7728
[BellMachover] p. 477Equation 3.1df-r1 9522
[BellMachover] p. 478Definitionrankval2 9576
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9540  r1ord3g 9537
[BellMachover] p. 480Axiom Regzfreg 9354
[BellMachover] p. 488Axiom ACac5 10233  dfac4 9878
[BellMachover] p. 490Definition of alephalephval3 9866
[BeltramettiCassinelli] p. 98Remarkatlatmstc 37333
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 30715
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 30757  chirredi 30756
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 30745
[Beran] p. 3Definition of joinsshjval3 29716
[Beran] p. 39Theorem 2.3(i)cmcm2 29978  cmcm2i 29955  cmcm2ii 29960  cmt2N 37264
[Beran] p. 40Theorem 2.3(iii)lecm 29979  lecmi 29964  lecmii 29965
[Beran] p. 45Theorem 3.4cmcmlem 29953
[Beran] p. 49Theorem 4.2cm2j 29982  cm2ji 29987  cm2mi 29988
[Beran] p. 95Definitiondf-sh 29569  issh2 29571
[Beran] p. 95Lemma 3.1(S5)his5 29448
[Beran] p. 95Lemma 3.1(S6)his6 29461
[Beran] p. 95Lemma 3.1(S7)his7 29452
[Beran] p. 95Lemma 3.2(S8)ho01i 30190
[Beran] p. 95Lemma 3.2(S9)hoeq1 30192
[Beran] p. 95Lemma 3.2(S10)ho02i 30191
[Beran] p. 95Lemma 3.2(S11)hoeq2 30193
[Beran] p. 95Postulate (S1)ax-his1 29444  his1i 29462
[Beran] p. 95Postulate (S2)ax-his2 29445
[Beran] p. 95Postulate (S3)ax-his3 29446
[Beran] p. 95Postulate (S4)ax-his4 29447
[Beran] p. 96Definition of normdf-hnorm 29330  dfhnorm2 29484  normval 29486
[Beran] p. 96Definition for Cauchy sequencehcau 29546
[Beran] p. 96Definition of Cauchy sequencedf-hcau 29335
[Beran] p. 96Definition of complete subspaceisch3 29603
[Beran] p. 96Definition of convergedf-hlim 29334  hlimi 29550
[Beran] p. 97Theorem 3.3(i)norm-i-i 29495  norm-i 29491
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 29499  norm-ii 29500  normlem0 29471  normlem1 29472  normlem2 29473  normlem3 29474  normlem4 29475  normlem5 29476  normlem6 29477  normlem7 29478  normlem7tALT 29481
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 29501  norm-iii 29502
[Beran] p. 98Remark 3.4bcs 29543  bcsiALT 29541  bcsiHIL 29542
[Beran] p. 98Remark 3.4(B)normlem9at 29483  normpar 29517  normpari 29516
[Beran] p. 98Remark 3.4(C)normpyc 29508  normpyth 29507  normpythi 29504
[Beran] p. 99Remarklnfn0 30409  lnfn0i 30404  lnop0 30328  lnop0i 30332
[Beran] p. 99Theorem 3.5(i)nmcexi 30388  nmcfnex 30415  nmcfnexi 30413  nmcopex 30391  nmcopexi 30389
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 30416  nmcfnlbi 30414  nmcoplb 30392  nmcoplbi 30390
[Beran] p. 99Theorem 3.5(iii)lnfncon 30418  lnfnconi 30417  lnopcon 30397  lnopconi 30396
[Beran] p. 100Lemma 3.6normpar2i 29518
[Beran] p. 101Lemma 3.6norm3adifi 29515  norm3adifii 29510  norm3dif 29512  norm3difi 29509
[Beran] p. 102Theorem 3.7(i)chocunii 29663  pjhth 29755  pjhtheu 29756  pjpjhth 29787  pjpjhthi 29788  pjth 24603
[Beran] p. 102Theorem 3.7(ii)ococ 29768  ococi 29767
[Beran] p. 103Remark 3.8nlelchi 30423
[Beran] p. 104Theorem 3.9riesz3i 30424  riesz4 30426  riesz4i 30425
[Beran] p. 104Theorem 3.10cnlnadj 30441  cnlnadjeu 30440  cnlnadjeui 30439  cnlnadji 30438  cnlnadjlem1 30429  nmopadjlei 30450
[Beran] p. 106Theorem 3.11(i)adjeq0 30453
[Beran] p. 106Theorem 3.11(v)nmopadji 30452
[Beran] p. 106Theorem 3.11(ii)adjmul 30454
[Beran] p. 106Theorem 3.11(iv)adjadj 30298
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 30464  nmopcoadji 30463
[Beran] p. 106Theorem 3.11(iii)adjadd 30455
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 30465
[Beran] p. 106Theorem 3.11(viii)adjcoi 30462  pjadj2coi 30566  pjadjcoi 30523
[Beran] p. 107Definitiondf-ch 29583  isch2 29585
[Beran] p. 107Remark 3.12choccl 29668  isch3 29603  occl 29666  ocsh 29645  shoccl 29667  shocsh 29646
[Beran] p. 107Remark 3.12(B)ococin 29770
[Beran] p. 108Theorem 3.13chintcl 29694
[Beran] p. 109Property (i)pjadj2 30549  pjadj3 30550  pjadji 30047  pjadjii 30036
[Beran] p. 109Property (ii)pjidmco 30543  pjidmcoi 30539  pjidmi 30035
[Beran] p. 110Definition of projector orderingpjordi 30535
[Beran] p. 111Remarkho0val 30112  pjch1 30032
[Beran] p. 111Definitiondf-hfmul 30096  df-hfsum 30095  df-hodif 30094  df-homul 30093  df-hosum 30092
[Beran] p. 111Lemma 4.4(i)pjo 30033
[Beran] p. 111Lemma 4.4(ii)pjch 30056  pjchi 29794
[Beran] p. 111Lemma 4.4(iii)pjoc2 29801  pjoc2i 29800
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 30042
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 30527  pjssmii 30043
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 30526
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 30525
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 30530
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 30528  pjssge0ii 30044
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 30529  pjdifnormii 30045
[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 32259
[Bogachev] p. 17Lemma 1.5.4omssubadd 32267
[Bogachev] p. 17Example 1.5.2omsmon 32265
[Bogachev] p. 41Definition 1.11.2df-carsg 32269
[Bogachev] p. 42Theorem 1.11.4carsgsiga 32289
[Bogachev] p. 116Definition 2.3.1df-itgm 32320  df-sitm 32298
[Bogachev] p. 118Chapter 2.4.4df-itgm 32320
[Bogachev] p. 118Definition 2.4.1df-sitg 32297
[Bollobas] p. 1Section I.1df-edg 27418  isuhgrop 27440  isusgrop 27532  isuspgrop 27531
[Bollobas] p. 2Section I.1df-subgr 27635  uhgrspan1 27670  uhgrspansubgr 27658
[Bollobas] p. 3Definitionisomuspgr 45286
[Bollobas] p. 3Section I.1cusgrsize 27821  df-cusgr 27779  df-nbgr 27700  fusgrmaxsize 27831
[Bollobas] p. 4Definitiondf-upwlks 45296  df-wlks 27966
[Bollobas] p. 4Section I.1finsumvtxdg2size 27917  finsumvtxdgeven 27919  fusgr1th 27918  fusgrvtxdgonume 27921  vtxdgoddnumeven 27920
[Bollobas] p. 5Notationdf-pths 28084
[Bollobas] p. 5Definitiondf-crcts 28154  df-cycls 28155  df-trls 28060  df-wlkson 27967
[Bollobas] p. 7Section I.1df-ushgr 27429
[BourbakiAlg1] p. 1Definition 1df-clintop 45394  df-cllaw 45380  df-mgm 18326  df-mgm2 45413
[BourbakiAlg1] p. 4Definition 5df-assintop 45395  df-asslaw 45382  df-sgrp 18375  df-sgrp2 45415
[BourbakiAlg1] p. 7Definition 8df-cmgm2 45414  df-comlaw 45381
[BourbakiAlg1] p. 12Definition 2df-mnd 18386
[BourbakiAlg1] p. 92Definition 1df-ring 19785
[BourbakiAlg1] p. 93Section I.8.1df-rng0 45433
[BourbakiEns] p. Proposition 8fcof1 7159  fcofo 7160
[BourbakiTop1] p. Remarkxnegmnf 12944  xnegpnf 12943
[BourbakiTop1] p. Remark rexneg 12945
[BourbakiTop1] p. Remark 3ust0 23371  ustfilxp 23364
[BourbakiTop1] p. Axiom GT'tgpsubcn 23241
[BourbakiTop1] p. Criterionishmeo 22910
[BourbakiTop1] p. Example 1cstucnd 23436  iducn 23435  snfil 23015
[BourbakiTop1] p. Example 2neifil 23031
[BourbakiTop1] p. Theorem 1cnextcn 23218
[BourbakiTop1] p. Theorem 2ucnextcn 23456
[BourbakiTop1] p. Theorem 3df-hcmp 31907
[BourbakiTop1] p. Paragraph 3infil 23014
[BourbakiTop1] p. Definition 1df-ucn 23428  df-ust 23352  filintn0 23012  filn0 23013  istgp 23228  ucnprima 23434
[BourbakiTop1] p. Definition 2df-cfilu 23439
[BourbakiTop1] p. Definition 3df-cusp 23450  df-usp 23409  df-utop 23383  trust 23381
[BourbakiTop1] p. Definition 6df-pcmp 31806
[BourbakiTop1] p. Property V_issnei2 22267
[BourbakiTop1] p. Theorem 1(d)iscncl 22420
[BourbakiTop1] p. Condition F_Iustssel 23357
[BourbakiTop1] p. Condition U_Iustdiag 23360
[BourbakiTop1] p. Property V_iiinnei 22276
[BourbakiTop1] p. Property V_ivneiptopreu 22284  neissex 22278
[BourbakiTop1] p. Proposition 1neips 22264  neiss 22260  ucncn 23437  ustund 23373  ustuqtop 23398
[BourbakiTop1] p. Proposition 2cnpco 22418  neiptopreu 22284  utop2nei 23402  utop3cls 23403
[BourbakiTop1] p. Proposition 3fmucnd 23444  uspreg 23426  utopreg 23404
[BourbakiTop1] p. Proposition 4imasncld 22842  imasncls 22843  imasnopn 22841
[BourbakiTop1] p. Proposition 9cnpflf2 23151
[BourbakiTop1] p. Condition F_IIustincl 23359
[BourbakiTop1] p. Condition U_IIustinvel 23361
[BourbakiTop1] p. Property V_iiielnei 22262
[BourbakiTop1] p. Proposition 11cnextucn 23455
[BourbakiTop1] p. Condition F_IIbustbasel 23358
[BourbakiTop1] p. Condition U_IIIustexhalf 23362
[BourbakiTop1] p. Definition C'''df-cmp 22538
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 22997
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22043
[BourbakiTop2] p. 195Definition 1df-ldlf 31803
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 43603
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 43605  stoweid 43604
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 43542  stoweidlem10 43551  stoweidlem14 43555  stoweidlem15 43556  stoweidlem35 43576  stoweidlem36 43577  stoweidlem37 43578  stoweidlem38 43579  stoweidlem40 43581  stoweidlem41 43582  stoweidlem43 43584  stoweidlem44 43585  stoweidlem46 43587  stoweidlem5 43546  stoweidlem50 43591  stoweidlem52 43593  stoweidlem53 43594  stoweidlem55 43596  stoweidlem56 43597
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 43564  stoweidlem24 43565  stoweidlem27 43568  stoweidlem28 43569  stoweidlem30 43571
[BrosowskiDeutsh] p. 91Proofstoweidlem34 43575  stoweidlem59 43600  stoweidlem60 43601
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 43586  stoweidlem49 43590  stoweidlem7 43548
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 43572  stoweidlem39 43580  stoweidlem42 43583  stoweidlem48 43589  stoweidlem51 43592  stoweidlem54 43595  stoweidlem57 43598  stoweidlem58 43599
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 43566
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 43558
[BrosowskiDeutsh] p. 92Proofstoweidlem11 43552  stoweidlem13 43554  stoweidlem26 43567  stoweidlem61 43602
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 43559
[Bruck] p. 1Section I.1df-clintop 45394  df-mgm 18326  df-mgm2 45413
[Bruck] p. 23Section II.1df-sgrp 18375  df-sgrp2 45415
[Bruck] p. 28Theorem 3.2dfgrp3 18674
[ChoquetDD] p. 2Definition of mappingdf-mpt 5158
[Church] p. 129Section II.24df-ifp 1061  dfifp2 1062
[Clemente] p. 10Definition ITnatded 28767
[Clemente] p. 10Definition I` `m,nnatded 28767
[Clemente] p. 11Definition E=>m,nnatded 28767
[Clemente] p. 11Definition I=>m,nnatded 28767
[Clemente] p. 11Definition E` `(1)natded 28767
[Clemente] p. 11Definition E` `(2)natded 28767
[Clemente] p. 12Definition E` `m,n,pnatded 28767
[Clemente] p. 12Definition I` `n(1)natded 28767
[Clemente] p. 12Definition I` `n(2)natded 28767
[Clemente] p. 13Definition I` `m,n,pnatded 28767
[Clemente] p. 14Proof 5.11natded 28767
[Clemente] p. 14Definition E` `nnatded 28767
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 28769  ex-natded5.2 28768
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 28772  ex-natded5.3 28771
[Clemente] p. 18Theorem 5.5ex-natded5.5 28774
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 28776  ex-natded5.7 28775
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 28778  ex-natded5.8 28777
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 28780  ex-natded5.13 28779
[Clemente] p. 32Definition I` `nnatded 28767
[Clemente] p. 32Definition E` `m,n,p,anatded 28767
[Clemente] p. 32Definition E` `n,tnatded 28767
[Clemente] p. 32Definition I` `n,tnatded 28767
[Clemente] p. 43Theorem 9.20ex-natded9.20 28781
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 28782
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 28784  ex-natded9.26 28783
[Cohen] p. 301Remarkrelogoprlem 25746
[Cohen] p. 301Property 2relogmul 25747  relogmuld 25780
[Cohen] p. 301Property 3relogdiv 25748  relogdivd 25781
[Cohen] p. 301Property 4relogexp 25751
[Cohen] p. 301Property 1alog1 25741
[Cohen] p. 301Property 1bloge 25742
[Cohen4] p. 348Observationrelogbcxpb 25937
[Cohen4] p. 349Propertyrelogbf 25941
[Cohen4] p. 352Definitionelogb 25920
[Cohen4] p. 361Property 2relogbmul 25927
[Cohen4] p. 361Property 3logbrec 25932  relogbdiv 25929
[Cohen4] p. 361Property 4relogbreexp 25925
[Cohen4] p. 361Property 6relogbexp 25930
[Cohen4] p. 361Property 1(a)logbid1 25918
[Cohen4] p. 361Property 1(b)logb1 25919
[Cohen4] p. 367Propertylogbchbase 25921
[Cohen4] p. 377Property 2logblt 25934
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 32252  sxbrsigalem4 32254
[Cohn] p. 81Section II.5acsdomd 18275  acsinfd 18274  acsinfdimd 18276  acsmap2d 18273  acsmapd 18272
[Cohn] p. 143Example 5.1.1sxbrsiga 32257
[Connell] p. 57Definitiondf-scmat 21640  df-scmatalt 45740
[Conway] p. 4Definitionslerec 34013
[Conway] p. 5Definitionaddsval 34126  df-adds 34119  df-negs 34120
[Conway] p. 7Theorem0slt1s 34023
[Conway] p. 16Theorem 0(i)ssltright 34055
[Conway] p. 16Theorem 0(ii)ssltleft 34054
[Conway] p. 16Theorem 0(iii)slerflex 33966
[Conway] p. 17Theorem 3addscom 34129  addscomd 34130  addsid1 34127  addsid1d 34128
[Conway] p. 17Definitiondf-0s 34018
[Conway] p. 18Definitiondf-1s 34019
[Conway] p. 29Remarkmadebday 34080  newbday 34082  oldbday 34081
[Conway] p. 29Definitiondf-made 34031  df-new 34033  df-old 34032
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13581
[Crawley] p. 1Definition of posetdf-poset 18031
[Crawley] p. 107Theorem 13.2hlsupr 37400
[Crawley] p. 110Theorem 13.3arglem1N 38204  dalaw 37900
[Crawley] p. 111Theorem 13.4hlathil 39979
[Crawley] p. 111Definition of set Wdf-watsN 38004
[Crawley] p. 111Definition of dilationdf-dilN 38120  df-ldil 38118  isldil 38124
[Crawley] p. 111Definition of translationdf-ltrn 38119  df-trnN 38121  isltrn 38133  ltrnu 38135
[Crawley] p. 112Lemma Acdlema1N 37805  cdlema2N 37806  exatleN 37418
[Crawley] p. 112Lemma B1cvrat 37490  cdlemb 37808  cdlemb2 38055  cdlemb3 38620  idltrn 38164  l1cvat 37069  lhpat 38057  lhpat2 38059  lshpat 37070  ltrnel 38153  ltrnmw 38165
[Crawley] p. 112Lemma Ccdlemc1 38205  cdlemc2 38206  ltrnnidn 38188  trlat 38183  trljat1 38180  trljat2 38181  trljat3 38182  trlne 38199  trlnidat 38187  trlnle 38200
[Crawley] p. 112Definition of automorphismdf-pautN 38005
[Crawley] p. 113Lemma Ccdlemc 38211  cdlemc3 38207  cdlemc4 38208
[Crawley] p. 113Lemma Dcdlemd 38221  cdlemd1 38212  cdlemd2 38213  cdlemd3 38214  cdlemd4 38215  cdlemd5 38216  cdlemd6 38217  cdlemd7 38218  cdlemd8 38219  cdlemd9 38220  cdleme31sde 38399  cdleme31se 38396  cdleme31se2 38397  cdleme31snd 38400  cdleme32a 38455  cdleme32b 38456  cdleme32c 38457  cdleme32d 38458  cdleme32e 38459  cdleme32f 38460  cdleme32fva 38451  cdleme32fva1 38452  cdleme32fvcl 38454  cdleme32le 38461  cdleme48fv 38513  cdleme4gfv 38521  cdleme50eq 38555  cdleme50f 38556  cdleme50f1 38557  cdleme50f1o 38560  cdleme50laut 38561  cdleme50ldil 38562  cdleme50lebi 38554  cdleme50rn 38559  cdleme50rnlem 38558  cdlemeg49le 38525  cdlemeg49lebilem 38553
[Crawley] p. 113Lemma Ecdleme 38574  cdleme00a 38223  cdleme01N 38235  cdleme02N 38236  cdleme0a 38225  cdleme0aa 38224  cdleme0b 38226  cdleme0c 38227  cdleme0cp 38228  cdleme0cq 38229  cdleme0dN 38230  cdleme0e 38231  cdleme0ex1N 38237  cdleme0ex2N 38238  cdleme0fN 38232  cdleme0gN 38233  cdleme0moN 38239  cdleme1 38241  cdleme10 38268  cdleme10tN 38272  cdleme11 38284  cdleme11a 38274  cdleme11c 38275  cdleme11dN 38276  cdleme11e 38277  cdleme11fN 38278  cdleme11g 38279  cdleme11h 38280  cdleme11j 38281  cdleme11k 38282  cdleme11l 38283  cdleme12 38285  cdleme13 38286  cdleme14 38287  cdleme15 38292  cdleme15a 38288  cdleme15b 38289  cdleme15c 38290  cdleme15d 38291  cdleme16 38299  cdleme16aN 38273  cdleme16b 38293  cdleme16c 38294  cdleme16d 38295  cdleme16e 38296  cdleme16f 38297  cdleme16g 38298  cdleme19a 38317  cdleme19b 38318  cdleme19c 38319  cdleme19d 38320  cdleme19e 38321  cdleme19f 38322  cdleme1b 38240  cdleme2 38242  cdleme20aN 38323  cdleme20bN 38324  cdleme20c 38325  cdleme20d 38326  cdleme20e 38327  cdleme20f 38328  cdleme20g 38329  cdleme20h 38330  cdleme20i 38331  cdleme20j 38332  cdleme20k 38333  cdleme20l 38336  cdleme20l1 38334  cdleme20l2 38335  cdleme20m 38337  cdleme20y 38316  cdleme20zN 38315  cdleme21 38351  cdleme21d 38344  cdleme21e 38345  cdleme22a 38354  cdleme22aa 38353  cdleme22b 38355  cdleme22cN 38356  cdleme22d 38357  cdleme22e 38358  cdleme22eALTN 38359  cdleme22f 38360  cdleme22f2 38361  cdleme22g 38362  cdleme23a 38363  cdleme23b 38364  cdleme23c 38365  cdleme26e 38373  cdleme26eALTN 38375  cdleme26ee 38374  cdleme26f 38377  cdleme26f2 38379  cdleme26f2ALTN 38378  cdleme26fALTN 38376  cdleme27N 38383  cdleme27a 38381  cdleme27cl 38380  cdleme28c 38386  cdleme3 38251  cdleme30a 38392  cdleme31fv 38404  cdleme31fv1 38405  cdleme31fv1s 38406  cdleme31fv2 38407  cdleme31id 38408  cdleme31sc 38398  cdleme31sdnN 38401  cdleme31sn 38394  cdleme31sn1 38395  cdleme31sn1c 38402  cdleme31sn2 38403  cdleme31so 38393  cdleme35a 38462  cdleme35b 38464  cdleme35c 38465  cdleme35d 38466  cdleme35e 38467  cdleme35f 38468  cdleme35fnpq 38463  cdleme35g 38469  cdleme35h 38470  cdleme35h2 38471  cdleme35sn2aw 38472  cdleme35sn3a 38473  cdleme36a 38474  cdleme36m 38475  cdleme37m 38476  cdleme38m 38477  cdleme38n 38478  cdleme39a 38479  cdleme39n 38480  cdleme3b 38243  cdleme3c 38244  cdleme3d 38245  cdleme3e 38246  cdleme3fN 38247  cdleme3fa 38250  cdleme3g 38248  cdleme3h 38249  cdleme4 38252  cdleme40m 38481  cdleme40n 38482  cdleme40v 38483  cdleme40w 38484  cdleme41fva11 38491  cdleme41sn3aw 38488  cdleme41sn4aw 38489  cdleme41snaw 38490  cdleme42a 38485  cdleme42b 38492  cdleme42c 38486  cdleme42d 38487  cdleme42e 38493  cdleme42f 38494  cdleme42g 38495  cdleme42h 38496  cdleme42i 38497  cdleme42k 38498  cdleme42ke 38499  cdleme42keg 38500  cdleme42mN 38501  cdleme42mgN 38502  cdleme43aN 38503  cdleme43bN 38504  cdleme43cN 38505  cdleme43dN 38506  cdleme5 38254  cdleme50ex 38573  cdleme50ltrn 38571  cdleme51finvN 38570  cdleme51finvfvN 38569  cdleme51finvtrN 38572  cdleme6 38255  cdleme7 38263  cdleme7a 38257  cdleme7aa 38256  cdleme7b 38258  cdleme7c 38259  cdleme7d 38260  cdleme7e 38261  cdleme7ga 38262  cdleme8 38264  cdleme8tN 38269  cdleme9 38267  cdleme9a 38265  cdleme9b 38266  cdleme9tN 38271  cdleme9taN 38270  cdlemeda 38312  cdlemedb 38311  cdlemednpq 38313  cdlemednuN 38314  cdlemefr27cl 38417  cdlemefr32fva1 38424  cdlemefr32fvaN 38423  cdlemefrs32fva 38414  cdlemefrs32fva1 38415  cdlemefs27cl 38427  cdlemefs32fva1 38437  cdlemefs32fvaN 38436  cdlemesner 38310  cdlemeulpq 38234
[Crawley] p. 114Lemma E4atex 38090  4atexlem7 38089  cdleme0nex 38304  cdleme17a 38300  cdleme17c 38302  cdleme17d 38512  cdleme17d1 38303  cdleme17d2 38509  cdleme18a 38305  cdleme18b 38306  cdleme18c 38307  cdleme18d 38309  cdleme4a 38253
[Crawley] p. 115Lemma Ecdleme21a 38339  cdleme21at 38342  cdleme21b 38340  cdleme21c 38341  cdleme21ct 38343  cdleme21f 38346  cdleme21g 38347  cdleme21h 38348  cdleme21i 38349  cdleme22gb 38308
[Crawley] p. 116Lemma Fcdlemf 38577  cdlemf1 38575  cdlemf2 38576
[Crawley] p. 116Lemma Gcdlemftr1 38581  cdlemg16 38671  cdlemg28 38718  cdlemg28a 38707  cdlemg28b 38717  cdlemg3a 38611  cdlemg42 38743  cdlemg43 38744  cdlemg44 38747  cdlemg44a 38745  cdlemg46 38749  cdlemg47 38750  cdlemg9 38648  ltrnco 38733  ltrncom 38752  tgrpabl 38765  trlco 38741
[Crawley] p. 116Definition of Gdf-tgrp 38757
[Crawley] p. 117Lemma Gcdlemg17 38691  cdlemg17b 38676
[Crawley] p. 117Definition of Edf-edring-rN 38770  df-edring 38771
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 38774
[Crawley] p. 118Remarktendopltp 38794
[Crawley] p. 118Lemma Hcdlemh 38831  cdlemh1 38829  cdlemh2 38830
[Crawley] p. 118Lemma Icdlemi 38834  cdlemi1 38832  cdlemi2 38833
[Crawley] p. 118Lemma Jcdlemj1 38835  cdlemj2 38836  cdlemj3 38837  tendocan 38838
[Crawley] p. 118Lemma Kcdlemk 38988  cdlemk1 38845  cdlemk10 38857  cdlemk11 38863  cdlemk11t 38960  cdlemk11ta 38943  cdlemk11tb 38945  cdlemk11tc 38959  cdlemk11u-2N 38903  cdlemk11u 38885  cdlemk12 38864  cdlemk12u-2N 38904  cdlemk12u 38886  cdlemk13-2N 38890  cdlemk13 38866  cdlemk14-2N 38892  cdlemk14 38868  cdlemk15-2N 38893  cdlemk15 38869  cdlemk16-2N 38894  cdlemk16 38871  cdlemk16a 38870  cdlemk17-2N 38895  cdlemk17 38872  cdlemk18-2N 38900  cdlemk18-3N 38914  cdlemk18 38882  cdlemk19-2N 38901  cdlemk19 38883  cdlemk19u 38984  cdlemk1u 38873  cdlemk2 38846  cdlemk20-2N 38906  cdlemk20 38888  cdlemk21-2N 38905  cdlemk21N 38887  cdlemk22-3 38915  cdlemk22 38907  cdlemk23-3 38916  cdlemk24-3 38917  cdlemk25-3 38918  cdlemk26-3 38920  cdlemk26b-3 38919  cdlemk27-3 38921  cdlemk28-3 38922  cdlemk29-3 38925  cdlemk3 38847  cdlemk30 38908  cdlemk31 38910  cdlemk32 38911  cdlemk33N 38923  cdlemk34 38924  cdlemk35 38926  cdlemk36 38927  cdlemk37 38928  cdlemk38 38929  cdlemk39 38930  cdlemk39u 38982  cdlemk4 38848  cdlemk41 38934  cdlemk42 38955  cdlemk42yN 38958  cdlemk43N 38977  cdlemk45 38961  cdlemk46 38962  cdlemk47 38963  cdlemk48 38964  cdlemk49 38965  cdlemk5 38850  cdlemk50 38966  cdlemk51 38967  cdlemk52 38968  cdlemk53 38971  cdlemk54 38972  cdlemk55 38975  cdlemk55u 38980  cdlemk56 38985  cdlemk5a 38849  cdlemk5auN 38874  cdlemk5u 38875  cdlemk6 38851  cdlemk6u 38876  cdlemk7 38862  cdlemk7u-2N 38902  cdlemk7u 38884  cdlemk8 38852  cdlemk9 38853  cdlemk9bN 38854  cdlemki 38855  cdlemkid 38950  cdlemkj-2N 38896  cdlemkj 38877  cdlemksat 38860  cdlemksel 38859  cdlemksv 38858  cdlemksv2 38861  cdlemkuat 38880  cdlemkuel-2N 38898  cdlemkuel-3 38912  cdlemkuel 38879  cdlemkuv-2N 38897  cdlemkuv2-2 38899  cdlemkuv2-3N 38913  cdlemkuv2 38881  cdlemkuvN 38878  cdlemkvcl 38856  cdlemky 38940  cdlemkyyN 38976  tendoex 38989
[Crawley] p. 120Remarkdva1dim 38999
[Crawley] p. 120Lemma Lcdleml1N 38990  cdleml2N 38991  cdleml3N 38992  cdleml4N 38993  cdleml5N 38994  cdleml6 38995  cdleml7 38996  cdleml8 38997  cdleml9 38998  dia1dim 39075
[Crawley] p. 120Lemma Mdia11N 39062  diaf11N 39063  dialss 39060  diaord 39061  dibf11N 39175  djajN 39151
[Crawley] p. 120Definition of isomorphism mapdiaval 39046
[Crawley] p. 121Lemma Mcdlemm10N 39132  dia2dimlem1 39078  dia2dimlem2 39079  dia2dimlem3 39080  dia2dimlem4 39081  dia2dimlem5 39082  diaf1oN 39144  diarnN 39143  dvheveccl 39126  dvhopN 39130
[Crawley] p. 121Lemma Ncdlemn 39226  cdlemn10 39220  cdlemn11 39225  cdlemn11a 39221  cdlemn11b 39222  cdlemn11c 39223  cdlemn11pre 39224  cdlemn2 39209  cdlemn2a 39210  cdlemn3 39211  cdlemn4 39212  cdlemn4a 39213  cdlemn5 39215  cdlemn5pre 39214  cdlemn6 39216  cdlemn7 39217  cdlemn8 39218  cdlemn9 39219  diclspsn 39208
[Crawley] p. 121Definition of phi(q)df-dic 39187
[Crawley] p. 122Lemma Ndih11 39279  dihf11 39281  dihjust 39231  dihjustlem 39230  dihord 39278  dihord1 39232  dihord10 39237  dihord11b 39236  dihord11c 39238  dihord2 39241  dihord2a 39233  dihord2b 39234  dihord2cN 39235  dihord2pre 39239  dihord2pre2 39240  dihordlem6 39227  dihordlem7 39228  dihordlem7b 39229
[Crawley] p. 122Definition of isomorphism mapdihffval 39244  dihfval 39245  dihval 39246
[Diestel] p. 3Section 1.1df-cusgr 27779  df-nbgr 27700
[Diestel] p. 4Section 1.1df-subgr 27635  uhgrspan1 27670  uhgrspansubgr 27658
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 27921  vtxdgoddnumeven 27920
[Diestel] p. 27Section 1.10df-ushgr 27429
[EGA] p. 80Notation 1.1.1rspecval 31814
[EGA] p. 80Proposition 1.1.2zartop 31826
[EGA] p. 80Proposition 1.1.2(i)zarcls0 31818  zarcls1 31819
[EGA] p. 81Corollary 1.1.8zart0 31829
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 31832
[EGA], p. 83Corollary 1.2.3rhmpreimacn 31835
[Eisenberg] p. 67Definition 5.3df-dif 3890
[Eisenberg] p. 82Definition 6.3dfom3 9405
[Eisenberg] p. 125Definition 8.21df-map 8617
[Eisenberg] p. 216Example 13.2(4)omenps 9413
[Eisenberg] p. 310Theorem 19.8cardprc 9738
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10311
[Enderton] p. 18Axiom of Empty Setaxnul 5229
[Enderton] p. 19Definitiondf-tp 4566
[Enderton] p. 26Exercise 5unissb 4873
[Enderton] p. 26Exercise 10pwel 5304
[Enderton] p. 28Exercise 7(b)pwun 5487
[Enderton] p. 30Theorem "Distributive laws"iinin1 5008  iinin2 5007  iinun2 5002  iunin1 5001  iunin1f 30897  iunin2 5000  uniin1 30891  uniin2 30892
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5006  iundif2 5003
[Enderton] p. 32Exercise 20unineq 4211
[Enderton] p. 33Exercise 23iinuni 5027
[Enderton] p. 33Exercise 25iununi 5028
[Enderton] p. 33Exercise 24(a)iinpw 5035
[Enderton] p. 33Exercise 24(b)iunpw 7621  iunpwss 5036
[Enderton] p. 36Definitionopthwiener 5428
[Enderton] p. 38Exercise 6(a)unipw 5366
[Enderton] p. 38Exercise 6(b)pwuni 4878
[Enderton] p. 41Lemma 3Dopeluu 5385  rnex 7759  rnexg 7751
[Enderton] p. 41Exercise 8dmuni 5823  rnuni 6052
[Enderton] p. 42Definition of a functiondffun7 6461  dffun8 6462
[Enderton] p. 43Definition of function valuefunfv2 6856
[Enderton] p. 43Definition of single-rootedfuncnv 6503
[Enderton] p. 44Definition (d)dfima2 5971  dfima3 5972
[Enderton] p. 47Theorem 3Hfvco2 6865
[Enderton] p. 49Axiom of Choice (first form)ac7 10229  ac7g 10230  df-ac 9872  dfac2 9887  dfac2a 9885  dfac2b 9886  dfac3 9877  dfac7 9888
[Enderton] p. 50Theorem 3K(a)imauni 7119
[Enderton] p. 52Definitiondf-map 8617
[Enderton] p. 53Exercise 21coass 6169
[Enderton] p. 53Exercise 27dmco 6158
[Enderton] p. 53Exercise 14(a)funin 6510
[Enderton] p. 53Exercise 22(a)imass2 6010
[Enderton] p. 54Remarkixpf 8708  ixpssmap 8720
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8686
[Enderton] p. 55Axiom of Choice (second form)ac9 10239  ac9s 10249
[Enderton] p. 56Theorem 3Meqvrelref 36723  erref 8518
[Enderton] p. 57Lemma 3Neqvrelthi 36726  erthi 8549
[Enderton] p. 57Definitiondf-ec 8500
[Enderton] p. 58Definitiondf-qs 8504
[Enderton] p. 61Exercise 35df-ec 8500
[Enderton] p. 65Exercise 56(a)dmun 5819
[Enderton] p. 68Definition of successordf-suc 6272
[Enderton] p. 71Definitiondf-tr 5192  dftr4 5196
[Enderton] p. 72Theorem 4Eunisuc 6342
[Enderton] p. 73Exercise 6unisuc 6342
[Enderton] p. 73Exercise 5(a)truni 5205
[Enderton] p. 73Exercise 5(b)trint 5207  trintALT 42501
[Enderton] p. 79Theorem 4I(A1)nna0 8435
[Enderton] p. 79Theorem 4I(A2)nnasuc 8437  onasuc 8358
[Enderton] p. 79Definition of operation valuedf-ov 7278
[Enderton] p. 80Theorem 4J(A1)nnm0 8436
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8438  onmsuc 8359
[Enderton] p. 81Theorem 4K(1)nnaass 8453
[Enderton] p. 81Theorem 4K(2)nna0r 8440  nnacom 8448
[Enderton] p. 81Theorem 4K(3)nndi 8454
[Enderton] p. 81Theorem 4K(4)nnmass 8455
[Enderton] p. 81Theorem 4K(5)nnmcom 8457
[Enderton] p. 82Exercise 16nnm0r 8441  nnmsucr 8456
[Enderton] p. 88Exercise 23nnaordex 8469
[Enderton] p. 129Definitiondf-en 8734
[Enderton] p. 132Theorem 6B(b)canth 7229
[Enderton] p. 133Exercise 1xpomen 9771
[Enderton] p. 133Exercise 2qnnen 15922
[Enderton] p. 134Theorem (Pigeonhole Principle)php 8993
[Enderton] p. 135Corollary 6Cphp3 8995
[Enderton] p. 136Corollary 6Enneneq 8992
[Enderton] p. 136Corollary 6D(a)pssinf 9033
[Enderton] p. 136Corollary 6D(b)ominf 9035
[Enderton] p. 137Lemma 6Fpssnn 8951
[Enderton] p. 138Corollary 6Gssfi 8956
[Enderton] p. 139Theorem 6H(c)mapen 8928
[Enderton] p. 142Theorem 6I(3)xpdjuen 9935
[Enderton] p. 142Theorem 6I(4)mapdjuen 9936
[Enderton] p. 143Theorem 6Jdju0en 9931  dju1en 9927
[Enderton] p. 144Exercise 13iunfi 9107  unifi 9108  unifi2 9109
[Enderton] p. 144Corollary 6Kundif2 4410  unfi 8955  unfi2 9083
[Enderton] p. 145Figure 38ffoss 7788
[Enderton] p. 145Definitiondf-dom 8735
[Enderton] p. 146Example 1domen 8751  domeng 8752
[Enderton] p. 146Example 3nndomo 9016  nnsdom 9412  nnsdomg 9073
[Enderton] p. 149Theorem 6L(a)djudom2 9939
[Enderton] p. 149Theorem 6L(c)mapdom1 8929  xpdom1 8858  xpdom1g 8856  xpdom2g 8855
[Enderton] p. 149Theorem 6L(d)mapdom2 8935
[Enderton] p. 151Theorem 6Mzorn 10263  zorng 10260
[Enderton] p. 151Theorem 6M(4)ac8 10248  dfac5 9884
[Enderton] p. 159Theorem 6Qunictb 10331
[Enderton] p. 164Exampleinfdif 9965
[Enderton] p. 168Definitiondf-po 5503
[Enderton] p. 192Theorem 7M(a)oneli 6374
[Enderton] p. 192Theorem 7M(b)ontr1 6312
[Enderton] p. 192Theorem 7M(c)onirri 6373
[Enderton] p. 193Corollary 7N(b)0elon 6319
[Enderton] p. 193Corollary 7N(c)onsuci 7685
[Enderton] p. 193Corollary 7N(d)ssonunii 7631
[Enderton] p. 194Remarkonprc 7628
[Enderton] p. 194Exercise 16suc11 6369
[Enderton] p. 197Definitiondf-card 9697
[Enderton] p. 197Theorem 7Pcarden 10307
[Enderton] p. 200Exercise 25tfis 7701
[Enderton] p. 202Lemma 7Tr1tr 9534
[Enderton] p. 202Definitiondf-r1 9522
[Enderton] p. 202Theorem 7Qr1val1 9544
[Enderton] p. 204Theorem 7V(b)rankval4 9625
[Enderton] p. 206Theorem 7X(b)en2lp 9364
[Enderton] p. 207Exercise 30rankpr 9615  rankprb 9609  rankpw 9601  rankpwi 9581  rankuniss 9624
[Enderton] p. 207Exercise 34opthreg 9376
[Enderton] p. 208Exercise 35suc11reg 9377
[Enderton] p. 212Definition of alephalephval3 9866
[Enderton] p. 213Theorem 8A(a)alephord2 9832
[Enderton] p. 213Theorem 8A(b)cardalephex 9846
[Enderton] p. 218Theorem Schema 8Eonfununi 8172
[Enderton] p. 222Definition of kardkarden 9653  kardex 9652
[Enderton] p. 238Theorem 8Roeoa 8428
[Enderton] p. 238Theorem 8Soeoe 8430
[Enderton] p. 240Exercise 25oarec 8393
[Enderton] p. 257Definition of cofinalitycflm 10006
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17351
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17297
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18271  mrieqv2d 17348  mrieqvd 17347
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17352
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17357  mreexexlem2d 17354
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18277  mreexfidimd 17359
[Frege1879] p. 11Statementdf3or2 41376
[Frege1879] p. 12Statementdf3an2 41377  dfxor4 41374  dfxor5 41375
[Frege1879] p. 26Axiom 1ax-frege1 41398
[Frege1879] p. 26Axiom 2ax-frege2 41399
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 41403
[Frege1879] p. 31Proposition 4frege4 41407
[Frege1879] p. 32Proposition 5frege5 41408
[Frege1879] p. 33Proposition 6frege6 41414
[Frege1879] p. 34Proposition 7frege7 41416
[Frege1879] p. 35Axiom 8ax-frege8 41417  axfrege8 41415
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 35616
[Frege1879] p. 35Proposition 9frege9 41420
[Frege1879] p. 36Proposition 10frege10 41428
[Frege1879] p. 36Proposition 11frege11 41422
[Frege1879] p. 37Proposition 12frege12 41421
[Frege1879] p. 37Proposition 13frege13 41430
[Frege1879] p. 37Proposition 14frege14 41431
[Frege1879] p. 38Proposition 15frege15 41434
[Frege1879] p. 38Proposition 16frege16 41424
[Frege1879] p. 39Proposition 17frege17 41429
[Frege1879] p. 39Proposition 18frege18 41426
[Frege1879] p. 39Proposition 19frege19 41432
[Frege1879] p. 40Proposition 20frege20 41436
[Frege1879] p. 40Proposition 21frege21 41435
[Frege1879] p. 41Proposition 22frege22 41427
[Frege1879] p. 42Proposition 23frege23 41433
[Frege1879] p. 42Proposition 24frege24 41423
[Frege1879] p. 42Proposition 25frege25 41425  rp-frege25 41413
[Frege1879] p. 42Proposition 26frege26 41418
[Frege1879] p. 43Axiom 28ax-frege28 41438
[Frege1879] p. 43Proposition 27frege27 41419
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 41439
[Frege1879] p. 44Axiom 31ax-frege31 41442  axfrege31 41441
[Frege1879] p. 44Proposition 30frege30 41440
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 41443
[Frege1879] p. 44Proposition 33frege33 41444
[Frege1879] p. 45Proposition 34frege34 41445
[Frege1879] p. 45Proposition 35frege35 41446
[Frege1879] p. 45Proposition 36frege36 41447
[Frege1879] p. 46Proposition 37frege37 41448
[Frege1879] p. 46Proposition 38frege38 41449
[Frege1879] p. 46Proposition 39frege39 41450
[Frege1879] p. 46Proposition 40frege40 41451
[Frege1879] p. 47Axiom 41ax-frege41 41453  axfrege41 41452
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 41454
[Frege1879] p. 47Proposition 43frege43 41455
[Frege1879] p. 47Proposition 44frege44 41456
[Frege1879] p. 47Proposition 45frege45 41457
[Frege1879] p. 48Proposition 46frege46 41458
[Frege1879] p. 48Proposition 47frege47 41459
[Frege1879] p. 49Proposition 48frege48 41460
[Frege1879] p. 49Proposition 49frege49 41461
[Frege1879] p. 49Proposition 50frege50 41462
[Frege1879] p. 50Axiom 52ax-frege52a 41465  ax-frege52c 41496  frege52aid 41466  frege52b 41497
[Frege1879] p. 50Axiom 54ax-frege54a 41470  ax-frege54c 41500  frege54b 41501
[Frege1879] p. 50Proposition 51frege51 41463
[Frege1879] p. 50Proposition 52dfsbcq 3718
[Frege1879] p. 50Proposition 53frege53a 41468  frege53aid 41467  frege53b 41498  frege53c 41522
[Frege1879] p. 50Proposition 54biid 260  eqid 2738
[Frege1879] p. 50Proposition 55frege55a 41476  frege55aid 41473  frege55b 41505  frege55c 41526  frege55cor1a 41477  frege55lem2a 41475  frege55lem2b 41504  frege55lem2c 41525
[Frege1879] p. 50Proposition 56frege56a 41479  frege56aid 41478  frege56b 41506  frege56c 41527
[Frege1879] p. 51Axiom 58ax-frege58a 41483  ax-frege58b 41509  frege58bid 41510  frege58c 41529
[Frege1879] p. 51Proposition 57frege57a 41481  frege57aid 41480  frege57b 41507  frege57c 41528
[Frege1879] p. 51Proposition 58spsbc 3729
[Frege1879] p. 51Proposition 59frege59a 41485  frege59b 41512  frege59c 41530
[Frege1879] p. 52Proposition 60frege60a 41486  frege60b 41513  frege60c 41531
[Frege1879] p. 52Proposition 61frege61a 41487  frege61b 41514  frege61c 41532
[Frege1879] p. 52Proposition 62frege62a 41488  frege62b 41515  frege62c 41533
[Frege1879] p. 52Proposition 63frege63a 41489  frege63b 41516  frege63c 41534
[Frege1879] p. 53Proposition 64frege64a 41490  frege64b 41517  frege64c 41535
[Frege1879] p. 53Proposition 65frege65a 41491  frege65b 41518  frege65c 41536
[Frege1879] p. 54Proposition 66frege66a 41492  frege66b 41519  frege66c 41537
[Frege1879] p. 54Proposition 67frege67a 41493  frege67b 41520  frege67c 41538
[Frege1879] p. 54Proposition 68frege68a 41494  frege68b 41521  frege68c 41539
[Frege1879] p. 55Definition 69dffrege69 41540
[Frege1879] p. 58Proposition 70frege70 41541
[Frege1879] p. 59Proposition 71frege71 41542
[Frege1879] p. 59Proposition 72frege72 41543
[Frege1879] p. 59Proposition 73frege73 41544
[Frege1879] p. 60Definition 76dffrege76 41547
[Frege1879] p. 60Proposition 74frege74 41545
[Frege1879] p. 60Proposition 75frege75 41546
[Frege1879] p. 62Proposition 77frege77 41548  frege77d 41354
[Frege1879] p. 63Proposition 78frege78 41549
[Frege1879] p. 63Proposition 79frege79 41550
[Frege1879] p. 63Proposition 80frege80 41551
[Frege1879] p. 63Proposition 81frege81 41552  frege81d 41355
[Frege1879] p. 64Proposition 82frege82 41553
[Frege1879] p. 65Proposition 83frege83 41554  frege83d 41356
[Frege1879] p. 65Proposition 84frege84 41555
[Frege1879] p. 66Proposition 85frege85 41556
[Frege1879] p. 66Proposition 86frege86 41557
[Frege1879] p. 66Proposition 87frege87 41558  frege87d 41358
[Frege1879] p. 67Proposition 88frege88 41559
[Frege1879] p. 68Proposition 89frege89 41560
[Frege1879] p. 68Proposition 90frege90 41561
[Frege1879] p. 68Proposition 91frege91 41562  frege91d 41359
[Frege1879] p. 69Proposition 92frege92 41563
[Frege1879] p. 70Proposition 93frege93 41564
[Frege1879] p. 70Proposition 94frege94 41565
[Frege1879] p. 70Proposition 95frege95 41566
[Frege1879] p. 71Definition 99dffrege99 41570
[Frege1879] p. 71Proposition 96frege96 41567  frege96d 41357
[Frege1879] p. 71Proposition 97frege97 41568  frege97d 41360
[Frege1879] p. 71Proposition 98frege98 41569  frege98d 41361
[Frege1879] p. 72Proposition 100frege100 41571
[Frege1879] p. 72Proposition 101frege101 41572
[Frege1879] p. 72Proposition 102frege102 41573  frege102d 41362
[Frege1879] p. 73Proposition 103frege103 41574
[Frege1879] p. 73Proposition 104frege104 41575
[Frege1879] p. 73Proposition 105frege105 41576
[Frege1879] p. 73Proposition 106frege106 41577  frege106d 41363
[Frege1879] p. 74Proposition 107frege107 41578
[Frege1879] p. 74Proposition 108frege108 41579  frege108d 41364
[Frege1879] p. 74Proposition 109frege109 41580  frege109d 41365
[Frege1879] p. 75Proposition 110frege110 41581
[Frege1879] p. 75Proposition 111frege111 41582  frege111d 41367
[Frege1879] p. 76Proposition 112frege112 41583
[Frege1879] p. 76Proposition 113frege113 41584
[Frege1879] p. 76Proposition 114frege114 41585  frege114d 41366
[Frege1879] p. 77Definition 115dffrege115 41586
[Frege1879] p. 77Proposition 116frege116 41587
[Frege1879] p. 78Proposition 117frege117 41588
[Frege1879] p. 78Proposition 118frege118 41589
[Frege1879] p. 78Proposition 119frege119 41590
[Frege1879] p. 78Proposition 120frege120 41591
[Frege1879] p. 79Proposition 121frege121 41592
[Frege1879] p. 79Proposition 122frege122 41593  frege122d 41368
[Frege1879] p. 79Proposition 123frege123 41594
[Frege1879] p. 80Proposition 124frege124 41595  frege124d 41369
[Frege1879] p. 81Proposition 125frege125 41596
[Frege1879] p. 81Proposition 126frege126 41597  frege126d 41370
[Frege1879] p. 82Proposition 127frege127 41598
[Frege1879] p. 83Proposition 128frege128 41599
[Frege1879] p. 83Proposition 129frege129 41600  frege129d 41371
[Frege1879] p. 84Proposition 130frege130 41601
[Frege1879] p. 85Proposition 131frege131 41602  frege131d 41372
[Frege1879] p. 86Proposition 132frege132 41603
[Frege1879] p. 86Proposition 133frege133 41604  frege133d 41373
[Fremlin1] p. 13Definition 111G (b)df-salgen 43854
[Fremlin1] p. 13Definition 111G (d)borelmbl 44174
[Fremlin1] p. 13Proposition 111G (b)salgenss 43875
[Fremlin1] p. 14Definition 112Aismea 43989
[Fremlin1] p. 15Remark 112B (d)psmeasure 44009
[Fremlin1] p. 15Property 112C (a)meadjun 44000  meadjunre 44014
[Fremlin1] p. 15Property 112C (b)meassle 44001
[Fremlin1] p. 15Property 112C (c)meaunle 44002
[Fremlin1] p. 16Property 112C (d)iundjiun 43998  meaiunle 44007  meaiunlelem 44006
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 44019  meaiuninc2 44020  meaiuninc3 44023  meaiuninc3v 44022  meaiunincf 44021  meaiuninclem 44018
[Fremlin1] p. 16Proposition 112C (f)meaiininc 44025  meaiininc2 44026  meaiininclem 44024
[Fremlin1] p. 19Theorem 113Ccaragen0 44044  caragendifcl 44052  caratheodory 44066  omelesplit 44056
[Fremlin1] p. 19Definition 113Aisome 44032  isomennd 44069  isomenndlem 44068
[Fremlin1] p. 19Remark 113B (c)omeunle 44054
[Fremlin1] p. 19Definition 112Dfcaragencmpl 44073  voncmpl 44159
[Fremlin1] p. 19Definition 113A (ii)omessle 44036
[Fremlin1] p. 20Theorem 113Ccarageniuncl 44061  carageniuncllem1 44059  carageniuncllem2 44060  caragenuncl 44051  caragenuncllem 44050  caragenunicl 44062
[Fremlin1] p. 21Remark 113Dcaragenel2d 44070
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 44064  caratheodorylem2 44065
[Fremlin1] p. 21Exercise 113Xacaragencmpl 44073
[Fremlin1] p. 23Lemma 114Bhoidmv1le 44132  hoidmv1lelem1 44129  hoidmv1lelem2 44130  hoidmv1lelem3 44131
[Fremlin1] p. 25Definition 114Eisvonmbl 44176
[Fremlin1] p. 29Lemma 115Bhoidmv1le 44132  hoidmvle 44138  hoidmvlelem1 44133  hoidmvlelem2 44134  hoidmvlelem3 44135  hoidmvlelem4 44136  hoidmvlelem5 44137  hsphoidmvle2 44123  hsphoif 44114  hsphoival 44117
[Fremlin1] p. 29Definition 1135 (b)hoicvr 44086
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 44094
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 44121  hoidmvn0val 44122  hoidmvval 44115  hoidmvval0 44125  hoidmvval0b 44128
[Fremlin1] p. 30Lemma 115Bhoiprodp1 44126  hsphoidmvle 44124
[Fremlin1] p. 30Definition 115Cdf-ovoln 44075  df-voln 44077
[Fremlin1] p. 30Proposition 115D (a)dmovn 44142  ovn0 44104  ovn0lem 44103  ovnf 44101  ovnome 44111  ovnssle 44099  ovnsslelem 44098  ovnsupge0 44095
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 44141  ovnhoilem1 44139  ovnhoilem2 44140  vonhoi 44205
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 44158  hoidifhspf 44156  hoidifhspval 44146  hoidifhspval2 44153  hoidifhspval3 44157  hspmbl 44167  hspmbllem1 44164  hspmbllem2 44165  hspmbllem3 44166
[Fremlin1] p. 31Definition 115Evoncmpl 44159  vonmea 44112
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 44110  ovnsubadd2 44184  ovnsubadd2lem 44183  ovnsubaddlem1 44108  ovnsubaddlem2 44109
[Fremlin1] p. 32Proposition 115G (a)hoimbl 44169  hoimbl2 44203  hoimbllem 44168  hspdifhsp 44154  opnvonmbl 44172  opnvonmbllem2 44171
[Fremlin1] p. 32Proposition 115G (b)borelmbl 44174
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 44217  iccvonmbllem 44216  ioovonmbl 44215
[Fremlin1] p. 32Proposition 115G (d)vonicc 44223  vonicclem2 44222  vonioo 44220  vonioolem2 44219  vonn0icc 44226  vonn0icc2 44230  vonn0ioo 44225  vonn0ioo2 44228
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 44227  snvonmbl 44224  vonct 44231  vonsn 44229
[Fremlin1] p. 35Lemma 121Asubsalsal 43898
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 43897  subsaliuncllem 43896
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 44261  salpreimalegt 44246  salpreimaltle 44262
[Fremlin1] p. 35Proposition 121B (i)issmf 44264  issmff 44270  issmflem 44263
[Fremlin1] p. 35Proposition 121B (ii)issmfle 44281  issmflelem 44280  smfpreimale 44290
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 44292  issmfgtlem 44291
[Fremlin1] p. 36Definition 121Cdf-smblfn 44234  issmf 44264  issmff 44270  issmfge 44305  issmfgelem 44304  issmfgt 44292  issmfgtlem 44291  issmfle 44281  issmflelem 44280  issmflem 44263
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 44244  salpreimagtlt 44266  salpreimalelt 44265
[Fremlin1] p. 36Proposition 121B (iv)issmfge 44305  issmfgelem 44304
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 44289
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 44287  cnfsmf 44276
[Fremlin1] p. 36Proposition 121D (c)decsmf 44302  decsmflem 44301  incsmf 44278  incsmflem 44277
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 44239  pimconstlt1 44240  smfconst 44285
[Fremlin1] p. 37Proposition 121E (b)smfadd 44300  smfaddlem1 44298  smfaddlem2 44299
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 44330
[Fremlin1] p. 37Proposition 121E (d)smfmul 44329  smfmullem1 44325  smfmullem2 44326  smfmullem3 44327  smfmullem4 44328
[Fremlin1] p. 37Proposition 121E (e)smfdiv 44331
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 44334  smfpimbor1lem2 44333
[Fremlin1] p. 37Proposition 121E (g)smfco 44336
[Fremlin1] p. 37Proposition 121E (h)smfres 44324
[Fremlin1] p. 38Proposition 121E (e)smfrec 44323
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 44332  smfresal 44322
[Fremlin1] p. 38Proposition 121F (a)smflim 44312  smflim2 44339  smflimlem1 44306  smflimlem2 44307  smflimlem3 44308  smflimlem4 44309  smflimlem5 44310  smflimlem6 44311  smflimmpt 44343
[Fremlin1] p. 38Proposition 121F (b)smfsup 44347  smfsuplem1 44344  smfsuplem2 44345  smfsuplem3 44346  smfsupmpt 44348  smfsupxr 44349
[Fremlin1] p. 38Proposition 121F (c)smfinf 44351  smfinflem 44350  smfinfmpt 44352
[Fremlin1] p. 39Remark 121Gsmflim 44312  smflim2 44339  smflimmpt 44343
[Fremlin1] p. 39Proposition 121Fsmfpimcc 44341
[Fremlin1] p. 39Proposition 121F (d)smflimsup 44361  smflimsuplem2 44354  smflimsuplem6 44358  smflimsuplem7 44359  smflimsuplem8 44360  smflimsupmpt 44362
[Fremlin1] p. 39Proposition 121F (e)smfliminf 44364  smfliminflem 44363  smfliminfmpt 44365
[Fremlin1] p. 80Definition 135E (b)df-smblfn 44234
[Fremlin5] p. 193Proposition 563Gbnulmbl2 24700
[Fremlin5] p. 213Lemma 565Cauniioovol 24743
[Fremlin5] p. 214Lemma 565Cauniioombl 24753
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 35855
[Fremlin5] p. 220Theorem 565Maftc1anc 35858
[FreydScedrov] p. 283Axiom of Infinityax-inf 9396  inf1 9380  inf2 9381
[Gleason] p. 117Proposition 9-2.1df-enq 10667  enqer 10677
[Gleason] p. 117Proposition 9-2.2df-1nq 10672  df-nq 10668
[Gleason] p. 117Proposition 9-2.3df-plpq 10664  df-plq 10670
[Gleason] p. 119Proposition 9-2.4caovmo 7509  df-mpq 10665  df-mq 10671
[Gleason] p. 119Proposition 9-2.5df-rq 10673
[Gleason] p. 119Proposition 9-2.6ltexnq 10731
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10732  ltbtwnnq 10734
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10727
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10728
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10735
[Gleason] p. 121Definition 9-3.1df-np 10737
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10749
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10751
[Gleason] p. 122Definitiondf-1p 10738
[Gleason] p. 122Remark (1)prub 10750
[Gleason] p. 122Lemma 9-3.4prlem934 10789
[Gleason] p. 122Proposition 9-3.2df-ltp 10741
[Gleason] p. 122Proposition 9-3.3ltsopr 10788  psslinpr 10787  supexpr 10810  suplem1pr 10808  suplem2pr 10809
[Gleason] p. 123Proposition 9-3.5addclpr 10774  addclprlem1 10772  addclprlem2 10773  df-plp 10739
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10778
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10777
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10790
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10799  ltexprlem1 10792  ltexprlem2 10793  ltexprlem3 10794  ltexprlem4 10795  ltexprlem5 10796  ltexprlem6 10797  ltexprlem7 10798
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10801  ltaprlem 10800
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10802
[Gleason] p. 124Lemma 9-3.6prlem936 10803
[Gleason] p. 124Proposition 9-3.7df-mp 10740  mulclpr 10776  mulclprlem 10775  reclem2pr 10804
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10785
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10780
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10779
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10784
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10807  reclem3pr 10805  reclem4pr 10806
[Gleason] p. 126Proposition 9-4.1df-enr 10811  enrer 10819
[Gleason] p. 126Proposition 9-4.2df-0r 10816  df-1r 10817  df-nr 10812
[Gleason] p. 126Proposition 9-4.3df-mr 10814  df-plr 10813  negexsr 10858  recexsr 10863  recexsrlem 10859
[Gleason] p. 127Proposition 9-4.4df-ltr 10815
[Gleason] p. 130Proposition 10-1.3creui 11968  creur 11967  cru 11965
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 10944  axcnre 10920
[Gleason] p. 132Definition 10-3.1crim 14826  crimd 14943  crimi 14904  crre 14825  crred 14942  crrei 14903
[Gleason] p. 132Definition 10-3.2remim 14828  remimd 14909
[Gleason] p. 133Definition 10.36absval2 14996  absval2d 15157  absval2i 15109
[Gleason] p. 133Proposition 10-3.4(a)cjadd 14852  cjaddd 14931  cjaddi 14899
[Gleason] p. 133Proposition 10-3.4(c)cjmul 14853  cjmuld 14932  cjmuli 14900
[Gleason] p. 133Proposition 10-3.4(e)cjcj 14851  cjcjd 14910  cjcji 14882
[Gleason] p. 133Proposition 10-3.4(f)cjre 14850  cjreb 14834  cjrebd 14913  cjrebi 14885  cjred 14937  rere 14833  rereb 14831  rerebd 14912  rerebi 14884  rered 14935
[Gleason] p. 133Proposition 10-3.4(h)addcj 14859  addcjd 14923  addcji 14894
[Gleason] p. 133Proposition 10-3.7(a)absval 14949
[Gleason] p. 133Proposition 10-3.7(b)abscj 14991  abscjd 15162  abscji 15113
[Gleason] p. 133Proposition 10-3.7(c)abs00 15001  abs00d 15158  abs00i 15110  absne0d 15159
[Gleason] p. 133Proposition 10-3.7(d)releabs 15033  releabsd 15163  releabsi 15114
[Gleason] p. 133Proposition 10-3.7(f)absmul 15006  absmuld 15166  absmuli 15116
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 14994  sqabsaddi 15117
[Gleason] p. 133Proposition 10-3.7(h)abstri 15042  abstrid 15168  abstrii 15120
[Gleason] p. 134Definition 10-4.1df-exp 13783  exp0 13786  expp1 13789  expp1d 13865
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 25834  cxpaddd 25872  expadd 13825  expaddd 13866  expaddz 13827
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 25843  cxpmuld 25891  expmul 13828  expmuld 13867  expmulz 13829
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 25840  mulcxpd 25883  mulexp 13822  mulexpd 13879  mulexpz 13823
[Gleason] p. 140Exercise 1znnen 15921
[Gleason] p. 141Definition 11-2.1fzval 13241
[Gleason] p. 168Proposition 12-2.1(a)climadd 15341  rlimadd 15352  rlimdiv 15357
[Gleason] p. 168Proposition 12-2.1(b)climsub 15343  rlimsub 15354
[Gleason] p. 168Proposition 12-2.1(c)climmul 15342  rlimmul 15355
[Gleason] p. 171Corollary 12-2.2climmulc2 15346
[Gleason] p. 172Corollary 12-2.5climrecl 15292
[Gleason] p. 172Proposition 12-2.4(c)climabs 15313  climcj 15314  climim 15316  climre 15315  rlimabs 15318  rlimcj 15319  rlimim 15321  rlimre 15320
[Gleason] p. 173Definition 12-3.1df-ltxr 11014  df-xr 11013  ltxr 12851
[Gleason] p. 175Definition 12-4.1df-limsup 15180  limsupval 15183
[Gleason] p. 180Theorem 12-5.1climsup 15381
[Gleason] p. 180Theorem 12-5.3caucvg 15390  caucvgb 15391  caucvgr 15387  climcau 15382
[Gleason] p. 182Exercise 3cvgcmp 15528
[Gleason] p. 182Exercise 4cvgrat 15595
[Gleason] p. 195Theorem 13-2.12abs1m 15047
[Gleason] p. 217Lemma 13-4.1btwnzge0 13548
[Gleason] p. 223Definition 14-1.1df-met 20591
[Gleason] p. 223Definition 14-1.1(a)met0 23496  xmet0 23495
[Gleason] p. 223Definition 14-1.1(b)metgt0 23512
[Gleason] p. 223Definition 14-1.1(c)metsym 23503
[Gleason] p. 223Definition 14-1.1(d)mettri 23505  mstri 23622  xmettri 23504  xmstri 23621
[Gleason] p. 225Definition 14-1.5xpsmet 23535
[Gleason] p. 230Proposition 14-2.6txlm 22799
[Gleason] p. 240Theorem 14-4.3metcnp4 24474
[Gleason] p. 240Proposition 14-4.2metcnp3 23696
[Gleason] p. 243Proposition 14-4.16addcn 24028  addcn2 15303  mulcn 24030  mulcn2 15305  subcn 24029  subcn2 15304
[Gleason] p. 295Remarkbcval3 14020  bcval4 14021
[Gleason] p. 295Equation 2bcpasc 14035
[Gleason] p. 295Definition of binomial coefficientbcval 14018  df-bc 14017
[Gleason] p. 296Remarkbcn0 14024  bcnn 14026
[Gleason] p. 296Theorem 15-2.8binom 15542
[Gleason] p. 308Equation 2ef0 15800
[Gleason] p. 308Equation 3efcj 15801
[Gleason] p. 309Corollary 15-4.3efne0 15806
[Gleason] p. 309Corollary 15-4.4efexp 15810
[Gleason] p. 310Equation 14sinadd 15873
[Gleason] p. 310Equation 15cosadd 15874
[Gleason] p. 311Equation 17sincossq 15885
[Gleason] p. 311Equation 18cosbnd 15890  sinbnd 15889
[Gleason] p. 311Lemma 15-4.7sqeqor 13932  sqeqori 13930
[Gleason] p. 311Definition of ` `df-pi 15782
[Godowski] p. 730Equation SFgoeqi 30635
[GodowskiGreechie] p. 249Equation IV3oai 30030
[Golan] p. 1Remarksrgisid 19764
[Golan] p. 1Definitiondf-srg 19742
[Golan] p. 149Definitiondf-slmd 31454
[Gonshor] p. 7Definitiondf-scut 33978
[Gonshor] p. 9Theorem 2.5slerec 34013
[Gonshor] p. 10Theorem 2.6cofcut1 34090
[Gonshor] p. 10Theorem 2.7cofcut2 34091
[Gonshor] p. 12Theorem 2.9cofcutr 34092
[Gonshor] p. 13Definitiondf-adds 34119
[GramKnuthPat], p. 47Definition 2.42df-fwddif 34461
[Gratzer] p. 23Section 0.6df-mre 17295
[Gratzer] p. 27Section 0.6df-mri 17297
[Hall] p. 1Section 1.1df-asslaw 45382  df-cllaw 45380  df-comlaw 45381
[Hall] p. 2Section 1.2df-clintop 45394
[Hall] p. 7Section 1.3df-sgrp2 45415
[Halmos] p. 31Theorem 17.3riesz1 30427  riesz2 30428
[Halmos] p. 41Definition of Hermitianhmopadj2 30303
[Halmos] p. 42Definition of projector orderingpjordi 30535
[Halmos] p. 43Theorem 26.1elpjhmop 30547  elpjidm 30546  pjnmopi 30510
[Halmos] p. 44Remarkpjinormi 30049  pjinormii 30038
[Halmos] p. 44Theorem 26.2elpjch 30551  pjrn 30069  pjrni 30064  pjvec 30058
[Halmos] p. 44Theorem 26.3pjnorm2 30089
[Halmos] p. 44Theorem 26.4hmopidmpj 30516  hmopidmpji 30514
[Halmos] p. 45Theorem 27.1pjinvari 30553
[Halmos] p. 45Theorem 27.3pjoci 30542  pjocvec 30059
[Halmos] p. 45Theorem 27.4pjorthcoi 30531
[Halmos] p. 48Theorem 29.2pjssposi 30534
[Halmos] p. 48Theorem 29.3pjssdif1i 30537  pjssdif2i 30536
[Halmos] p. 50Definition of spectrumdf-spec 30217
[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 24155  df-phtpy 24134
[Hatcher] p. 26Definitiondf-pco 24168  df-pi1 24171
[Hatcher] p. 26Proposition 1.2phtpcer 24158
[Hatcher] p. 26Proposition 1.3pi1grp 24213
[Hefferon] p. 240Definition 3.12df-dmat 21639  df-dmatalt 45739
[Helfgott] p. 2Theoremtgoldbach 45269
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 45254
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 45266  bgoldbtbnd 45261  bgoldbtbnd 45261  tgblthelfgott 45267
[Helfgott] p. 5Proposition 1.1circlevma 32622
[Helfgott] p. 69Statement 7.49circlemethhgt 32623
[Helfgott] p. 69Statement 7.50hgt750lema 32637  hgt750lemb 32636  hgt750leme 32638  hgt750lemf 32633  hgt750lemg 32634
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 45263  tgoldbachgt 32643  tgoldbachgtALTV 45264  tgoldbachgtd 32642
[Helfgott] p. 70Statement 7.49ax-hgt749 32624
[Herstein] p. 54Exercise 28df-grpo 28855
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18588  grpoideu 28871  mndideu 18396
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18614  grpoinveu 28881
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18642  grpo2inv 28893
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18653  grpoinvop 28895
[Herstein] p. 57Exercise 1dfgrp3e 18675
[Hitchcock] p. 5Rule A3mptnan 1771
[Hitchcock] p. 5Rule A4mptxor 1772
[Hitchcock] p. 5Rule A5mtpxor 1774
[Holland] p. 1519Theorem 2sumdmdi 30782
[Holland] p. 1520Lemma 5cdj1i 30795  cdj3i 30803  cdj3lem1 30796  cdjreui 30794
[Holland] p. 1524Lemma 7mddmdin0i 30793
[Holland95] p. 13Theorem 3.6hlathil 39979
[Holland95] p. 14Line 15hgmapvs 39905
[Holland95] p. 14Line 16hdmaplkr 39927
[Holland95] p. 14Line 17hdmapellkr 39928
[Holland95] p. 14Line 19hdmapglnm2 39925
[Holland95] p. 14Line 20hdmapip0com 39931
[Holland95] p. 14Theorem 3.6hdmapevec2 39850
[Holland95] p. 14Lines 24 and 25hdmapoc 39945
[Holland95] p. 204Definition of involutiondf-srng 20106
[Holland95] p. 212Definition of subspacedf-psubsp 37517
[Holland95] p. 214Lemma 3.3lclkrlem2v 39542
[Holland95] p. 214Definition 3.2df-lpolN 39495
[Holland95] p. 214Definition of nonsingularpnonsingN 37947
[Holland95] p. 215Lemma 3.3(1)dihoml4 39391  poml4N 37967
[Holland95] p. 215Lemma 3.3(2)dochexmid 39482  pexmidALTN 37992  pexmidN 37983
[Holland95] p. 218Theorem 3.6lclkr 39547
[Holland95] p. 218Definition of dual vector spacedf-ldual 37138  ldualset 37139
[Holland95] p. 222Item 1df-lines 37515  df-pointsN 37516
[Holland95] p. 222Item 2df-polarityN 37917
[Holland95] p. 223Remarkispsubcl2N 37961  omllaw4 37260  pol1N 37924  polcon3N 37931
[Holland95] p. 223Definitiondf-psubclN 37949
[Holland95] p. 223Equation for polaritypolval2N 37920
[Holmes] p. 40Definitiondf-xrn 36501
[Hughes] p. 44Equation 1.21bax-his3 29446
[Hughes] p. 47Definition of projection operatordfpjop 30544
[Hughes] p. 49Equation 1.30eighmre 30325  eigre 30197  eigrei 30196
[Hughes] p. 49Equation 1.31eighmorth 30326  eigorth 30200  eigorthi 30199
[Hughes] p. 137Remark (ii)eigposi 30198
[Huneke] p. 1Claim 1frgrncvvdeq 28673
[Huneke] p. 1Statement 1frgrncvvdeqlem7 28669
[Huneke] p. 1Statement 2frgrncvvdeqlem8 28670
[Huneke] p. 1Statement 3frgrncvvdeqlem9 28671
[Huneke] p. 2Claim 2frgrregorufr 28689  frgrregorufr0 28688  frgrregorufrg 28690
[Huneke] p. 2Claim 3frgrhash2wsp 28696  frrusgrord 28705  frrusgrord0 28704
[Huneke] p. 2Statementdf-clwwlknon 28452
[Huneke] p. 2Statement 4frgrwopreglem4 28679
[Huneke] p. 2Statement 5frgrwopreg1 28682  frgrwopreg2 28683  frgrwopregasn 28680  frgrwopregbsn 28681
[Huneke] p. 2Statement 6frgrwopreglem5 28685
[Huneke] p. 2Statement 7fusgreghash2wspv 28699
[Huneke] p. 2Statement 8fusgreghash2wsp 28702
[Huneke] p. 2Statement 9clwlksndivn 28450  numclwlk1 28735  numclwlk1lem1 28733  numclwlk1lem2 28734  numclwwlk1 28725  numclwwlk8 28756
[Huneke] p. 2Definition 3frgrwopreglem1 28676
[Huneke] p. 2Definition 4df-clwlks 28139
[Huneke] p. 2Definition 62clwwlk 28711
[Huneke] p. 2Definition 7numclwwlkovh 28737  numclwwlkovh0 28736
[Huneke] p. 2Statement 10numclwwlk2 28745
[Huneke] p. 2Statement 11rusgrnumwlkg 28342
[Huneke] p. 2Statement 12numclwwlk3 28749
[Huneke] p. 2Statement 13numclwwlk5 28752
[Huneke] p. 2Statement 14numclwwlk7 28755
[Indrzejczak] p. 33Definition ` `Enatded 28767  natded 28767
[Indrzejczak] p. 33Definition ` `Inatded 28767
[Indrzejczak] p. 34Definition ` `Enatded 28767  natded 28767
[Indrzejczak] p. 34Definition ` `Inatded 28767
[Jech] p. 4Definition of classcv 1538  cvjust 2732
[Jech] p. 42Lemma 6.1alephexp1 10335
[Jech] p. 42Equation 6.1alephadd 10333  alephmul 10334
[Jech] p. 43Lemma 6.2infmap 10332  infmap2 9974
[Jech] p. 71Lemma 9.3jech9.3 9572
[Jech] p. 72Equation 9.3scott0 9644  scottex 9643
[Jech] p. 72Exercise 9.1rankval4 9625
[Jech] p. 72Scheme "Collection Principle"cp 9649
[Jech] p. 78Noteopthprc 5651
[JonesMatijasevic] p. 694Definition 2.3rmxyval 40737
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 40825
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 40826
[JonesMatijasevic] p. 695Equation 2.7rmxadd 40749
[JonesMatijasevic] p. 695Equation 2.8rmyadd 40753
[JonesMatijasevic] p. 695Equation 2.9rmxp1 40754  rmyp1 40755
[JonesMatijasevic] p. 695Equation 2.10rmxm1 40756  rmym1 40757
[JonesMatijasevic] p. 695Equation 2.11rmx0 40747  rmx1 40748  rmxluc 40758
[JonesMatijasevic] p. 695Equation 2.12rmy0 40751  rmy1 40752  rmyluc 40759
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 40761
[JonesMatijasevic] p. 695Equation 2.14rmydbl 40762
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 40782  jm2.17b 40783  jm2.17c 40784
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 40815
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 40819
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 40810
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 40785  jm2.24nn 40781
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 40824
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 40830  rmygeid 40786
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 40842
[Juillerat] p. 11Section *5etransc 43824  etransclem47 43822  etransclem48 43823
[Juillerat] p. 12Equation (7)etransclem44 43819
[Juillerat] p. 12Equation *(7)etransclem46 43821
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 43807
[Juillerat] p. 13Proofetransclem35 43810
[Juillerat] p. 13Part of case 2 proven inetransclem38 43813
[Juillerat] p. 13Part of case 2 provenetransclem24 43799
[Juillerat] p. 13Part of case 2: proven inetransclem41 43816
[Juillerat] p. 14Proofetransclem23 43798
[KalishMontague] p. 81Note 1ax-6 1971
[KalishMontague] p. 85Lemma 2equid 2015
[KalishMontague] p. 85Lemma 3equcomi 2020
[KalishMontague] p. 86Lemma 7cbvalivw 2010  cbvaliw 2009  wl-cbvmotv 35672  wl-motae 35674  wl-moteq 35673
[KalishMontague] p. 87Lemma 8spimvw 1999  spimw 1974
[KalishMontague] p. 87Lemma 9spfw 2036  spw 2037
[Kalmbach] p. 14Definition of latticechabs1 29878  chabs1i 29880  chabs2 29879  chabs2i 29881  chjass 29895  chjassi 29848  latabs1 18193  latabs2 18194
[Kalmbach] p. 15Definition of atomdf-at 30700  ela 30701
[Kalmbach] p. 15Definition of coverscvbr2 30645  cvrval2 37288
[Kalmbach] p. 16Definitiondf-ol 37192  df-oml 37193
[Kalmbach] p. 20Definition of commutescmbr 29946  cmbri 29952  cmtvalN 37225  df-cm 29945  df-cmtN 37191
[Kalmbach] p. 22Remarkomllaw5N 37261  pjoml5 29975  pjoml5i 29950
[Kalmbach] p. 22Definitionpjoml2 29973  pjoml2i 29947
[Kalmbach] p. 22Theorem 2(v)cmcm 29976  cmcmi 29954  cmcmii 29959  cmtcomN 37263
[Kalmbach] p. 22Theorem 2(ii)omllaw3 37259  omlsi 29766  pjoml 29798  pjomli 29797
[Kalmbach] p. 22Definition of OML lawomllaw2N 37258
[Kalmbach] p. 23Remarkcmbr2i 29958  cmcm3 29977  cmcm3i 29956  cmcm3ii 29961  cmcm4i 29957  cmt3N 37265  cmt4N 37266  cmtbr2N 37267
[Kalmbach] p. 23Lemma 3cmbr3 29970  cmbr3i 29962  cmtbr3N 37268
[Kalmbach] p. 25Theorem 5fh1 29980  fh1i 29983  fh2 29981  fh2i 29984  omlfh1N 37272
[Kalmbach] p. 65Remarkchjatom 30719  chslej 29860  chsleji 29820  shslej 29742  shsleji 29732
[Kalmbach] p. 65Proposition 1chocin 29857  chocini 29816  chsupcl 29702  chsupval2 29772  h0elch 29617  helch 29605  hsupval2 29771  ocin 29658  ococss 29655  shococss 29656
[Kalmbach] p. 65Definition of subspace sumshsval 29674
[Kalmbach] p. 66Remarkdf-pjh 29757  pjssmi 30527  pjssmii 30043
[Kalmbach] p. 67Lemma 3osum 30007  osumi 30004
[Kalmbach] p. 67Lemma 4pjci 30562
[Kalmbach] p. 103Exercise 6atmd2 30762
[Kalmbach] p. 103Exercise 12mdsl0 30672
[Kalmbach] p. 140Remarkhatomic 30722  hatomici 30721  hatomistici 30724
[Kalmbach] p. 140Proposition 1atlatmstc 37333
[Kalmbach] p. 140Proposition 1(i)atexch 30743  lsatexch 37057
[Kalmbach] p. 140Proposition 1(ii)chcv1 30717  cvlcvr1 37353  cvr1 37424
[Kalmbach] p. 140Proposition 1(iii)cvexch 30736  cvexchi 30731  cvrexch 37434
[Kalmbach] p. 149Remark 2chrelati 30726  hlrelat 37416  hlrelat5N 37415  lrelat 37028
[Kalmbach] p. 153Exercise 5lsmcv 20403  lsmsatcv 37024  spansncv 30015  spansncvi 30014
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 37043  spansncv2 30655
[Kalmbach] p. 266Definitiondf-st 30573
[Kalmbach2] p. 8Definition of adjointdf-adjh 30211
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10402  fpwwe2 10399
[KanamoriPincus] p. 416Corollary 1.3canth4 10403
[KanamoriPincus] p. 417Corollary 1.6canthp1 10410
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10405
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10407
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10420
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10424  gchxpidm 10425
[KanamoriPincus] p. 419Theorem 2.1gchacg 10436  gchhar 10435
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 9972  unxpwdom 9348
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10426
[Kreyszig] p. 3Property M1metcl 23485  xmetcl 23484
[Kreyszig] p. 4Property M2meteq0 23492
[Kreyszig] p. 8Definition 1.1-8dscmet 23728
[Kreyszig] p. 12Equation 5conjmul 11692  muleqadd 11619
[Kreyszig] p. 18Definition 1.3-2mopnval 23591
[Kreyszig] p. 19Remarkmopntopon 23592
[Kreyszig] p. 19Theorem T1mopn0 23654  mopnm 23597
[Kreyszig] p. 19Theorem T2unimopn 23652
[Kreyszig] p. 19Definition of neighborhoodneibl 23657
[Kreyszig] p. 20Definition 1.3-3metcnp2 23698
[Kreyszig] p. 25Definition 1.4-1lmbr 22409  lmmbr 24422  lmmbr2 24423
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 22531
[Kreyszig] p. 28Theorem 1.4-5lmcau 24477
[Kreyszig] p. 28Definition 1.4-3iscau 24440  iscmet2 24458
[Kreyszig] p. 30Theorem 1.4-7cmetss 24480
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 22612  metelcls 24469
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 24470  metcld2 24471
[Kreyszig] p. 51Equation 2clmvneg1 24262  lmodvneg1 20166  nvinv 29001  vcm 28938
[Kreyszig] p. 51Equation 1aclm0vs 24258  lmod0vs 20156  slmd0vs 31477  vc0 28936
[Kreyszig] p. 51Equation 1blmodvs0 20157  slmdvs0 31478  vcz 28937
[Kreyszig] p. 58Definition 2.2-1imsmet 29053  ngpmet 23759  nrmmetd 23730
[Kreyszig] p. 59Equation 1imsdval 29048  imsdval2 29049  ncvspds 24325  ngpds 23760
[Kreyszig] p. 63Problem 1nmval 23745  nvnd 29050
[Kreyszig] p. 64Problem 2nmeq0 23774  nmge0 23773  nvge0 29035  nvz 29031
[Kreyszig] p. 64Problem 3nmrtri 23780  nvabs 29034
[Kreyszig] p. 91Definition 2.7-1isblo3i 29163
[Kreyszig] p. 92Equation 2df-nmoo 29107
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 29169  blocni 29167
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 29168
[Kreyszig] p. 129Definition 3.1-1cphipeq0 24368  ipeq0 20843  ipz 29081
[Kreyszig] p. 135Problem 2cphpyth 24380  pythi 29212
[Kreyszig] p. 137Lemma 3-2.1(a)sii 29216
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 24402
[Kreyszig] p. 144Equation 4supcvg 15568
[Kreyszig] p. 144Theorem 3.3-1minvec 24600  minveco 29246
[Kreyszig] p. 196Definition 3.9-1df-aj 29112
[Kreyszig] p. 247Theorem 4.7-2bcth 24493
[Kreyszig] p. 249Theorem 4.7-3ubth 29235
[Kreyszig] p. 470Definition of positive operator orderingleop 30485  leopg 30484
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 30503
[Kreyszig] p. 525Theorem 10.1-1htth 29280
[Kulpa] p. 547Theorempoimir 35810
[Kulpa] p. 547Equation (1)poimirlem32 35809
[Kulpa] p. 547Equation (2)poimirlem31 35808
[Kulpa] p. 548Theorembroucube 35811
[Kulpa] p. 548Equation (6)poimirlem26 35803
[Kulpa] p. 548Equation (7)poimirlem27 35804
[Kunen] p. 10Axiom 0ax6e 2383  axnul 5229
[Kunen] p. 11Axiom 3axnul 5229
[Kunen] p. 12Axiom 6zfrep6 7797
[Kunen] p. 24Definition 10.24mapval 8627  mapvalg 8625
[Kunen] p. 30Lemma 10.20fodomg 10278
[Kunen] p. 31Definition 10.24mapex 8621
[Kunen] p. 95Definition 2.1df-r1 9522
[Kunen] p. 97Lemma 2.10r1elss 9564  r1elssi 9563
[Kunen] p. 107Exercise 4rankop 9616  rankopb 9610  rankuni 9621  rankxplim 9637  rankxpsuc 9640
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4936
[Lang] , p. 225Corollary 1.3finexttrb 31737
[Lang] p. Definitiondf-rn 5600
[Lang] p. 3Statementlidrideqd 18353  mndbn0 18401
[Lang] p. 3Definitiondf-mnd 18386
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18371
[Lang] p. 4Property of composites. Second formulagsumccat 18480
[Lang] p. 5Equationgsumreidx 19518
[Lang] p. 5Definition of an (infinite) productgsumfsupp 45376
[Lang] p. 6Examplenn0mnd 45373
[Lang] p. 6Equationgsumxp2 19581
[Lang] p. 6Statementcycsubm 18821
[Lang] p. 6Definitionmulgnn0gsum 18710
[Lang] p. 6Observationmndlsmidm 19276
[Lang] p. 7Definitiondfgrp2e 18605
[Lang] p. 30Definitiondf-tocyc 31374
[Lang] p. 32Property (a)cyc3genpm 31419
[Lang] p. 32Property (b)cyc3conja 31424  cycpmconjv 31409
[Lang] p. 53Definitiondf-cat 17377
[Lang] p. 53Axiom CAT 1cat1 17812  cat1lem 17811
[Lang] p. 54Definitiondf-iso 17461
[Lang] p. 57Definitiondf-inito 17699  df-termo 17700
[Lang] p. 58Exampleirinitoringc 45627
[Lang] p. 58Statementinitoeu1 17726  termoeu1 17733
[Lang] p. 62Definitiondf-func 17573
[Lang] p. 65Definitiondf-nat 17659
[Lang] p. 91Notedf-ringc 45563
[Lang] p. 92Statementmxidlprm 31640
[Lang] p. 92Definitionisprmidlc 31623
[Lang] p. 128Remarkdsmmlmod 20952
[Lang] p. 129Prooflincscm 45771  lincscmcl 45773  lincsum 45770  lincsumcl 45772
[Lang] p. 129Statementlincolss 45775
[Lang] p. 129Observationdsmmfi 20945
[Lang] p. 141Theorem 5.3dimkerim 31708  qusdimsum 31709
[Lang] p. 141Corollary 5.4lssdimle 31691
[Lang] p. 147Definitionsnlindsntor 45812
[Lang] p. 504Statementmat1 21596  matring 21592
[Lang] p. 504Definitiondf-mamu 21533
[Lang] p. 505Statementmamuass 21549  mamutpos 21607  matassa 21593  mattposvs 21604  tposmap 21606
[Lang] p. 513Definitionmdet1 21750  mdetf 21744
[Lang] p. 513Theorem 4.4cramer 21840
[Lang] p. 514Proposition 4.6mdetleib 21736
[Lang] p. 514Proposition 4.8mdettpos 21760
[Lang] p. 515Definitiondf-minmar1 21784  smadiadetr 21824
[Lang] p. 515Corollary 4.9mdetero 21759  mdetralt 21757
[Lang] p. 517Proposition 4.15mdetmul 21772
[Lang] p. 518Definitiondf-madu 21783
[Lang] p. 518Proposition 4.16madulid 21794  madurid 21793  matinv 21826
[Lang] p. 561Theorem 3.1cayleyhamilton 22039
[Lang], p. 224Proposition 1.2extdgmul 31736  fedgmul 31712
[Lang], p. 561Remarkchpmatply1 21981
[Lang], p. 561Definitiondf-chpmat 21976
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 41952
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 41947
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 41953
[LeBlanc] p. 277Rule R2axnul 5229
[Levy] p. 12Axiom 4.3.1df-clab 2716
[Levy] p. 59Definitiondf-ttrcl 9466
[Levy] p. 64Theorem 5.6(ii)frinsg 9509
[Levy] p. 338Axiomdf-clel 2816  df-cleq 2730
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2816  df-cleq 2730
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2716
[Levy] p. 358Axiomdf-clab 2716
[Levy58] p. 2Definition Iisfin1-3 10142
[Levy58] p. 2Definition IIdf-fin2 10042
[Levy58] p. 2Definition Iadf-fin1a 10041
[Levy58] p. 2Definition IIIdf-fin3 10044
[Levy58] p. 3Definition Vdf-fin5 10045
[Levy58] p. 3Definition IVdf-fin4 10043
[Levy58] p. 4Definition VIdf-fin6 10046
[Levy58] p. 4Definition VIIdf-fin7 10047
[Levy58], p. 3Theorem 1fin1a2 10171
[Lipparini] p. 3Lemma 2.1.1nosepssdm 33889
[Lipparini] p. 3Lemma 2.1.4noresle 33900
[Lipparini] p. 6Proposition 4.2noinfbnd1 33932  nosupbnd1 33917
[Lipparini] p. 6Proposition 4.3noinfbnd2 33934  nosupbnd2 33919
[Lipparini] p. 7Theorem 5.1noetasuplem3 33938  noetasuplem4 33939
[Lipparini] p. 7Corollary 4.4nosupinfsep 33935
[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 30770
[Maeda] p. 168Lemma 5mdsym 30774  mdsymi 30773
[Maeda] p. 168Lemma 4(i)mdsymlem4 30768  mdsymlem6 30770  mdsymlem7 30771
[Maeda] p. 168Lemma 4(ii)mdsymlem8 30772
[MaedaMaeda] p. 1Remarkssdmd1 30675  ssdmd2 30676  ssmd1 30673  ssmd2 30674
[MaedaMaeda] p. 1Lemma 1.2mddmd2 30671
[MaedaMaeda] p. 1Definition 1.1df-dmd 30643  df-md 30642  mdbr 30656
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 30693  mdslj1i 30681  mdslj2i 30682  mdslle1i 30679  mdslle2i 30680  mdslmd1i 30691  mdslmd2i 30692
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 30683  mdsl2bi 30685  mdsl2i 30684
[MaedaMaeda] p. 2Lemma 1.6mdexchi 30697
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 30694
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 30695
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 30672
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 30677  mdsl3 30678
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 30696
[MaedaMaeda] p. 4Theorem 1.14mdcompli 30791
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 37335  hlrelat1 37414
[MaedaMaeda] p. 31Lemma 7.5lcvexch 37053
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 30698  cvmdi 30686  cvnbtwn4 30651  cvrnbtwn4 37293
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 30699
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 37354  cvp 30737  cvrp 37430  lcvp 37054
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 30761
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 30760
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 37347  hlexch4N 37406
[MaedaMaeda] p. 34Exercise 7.1atabsi 30763
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 37457
[MaedaMaeda] p. 61Definition 15.10psubN 37763  atpsubN 37767  df-pointsN 37516  pointpsubN 37765
[MaedaMaeda] p. 62Theorem 15.5df-pmap 37518  pmap11 37776  pmaple 37775  pmapsub 37782  pmapval 37771
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 37779  pmap1N 37781
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 37784  pmapglb2N 37785  pmapglb2xN 37786  pmapglbx 37783
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 37866
[MaedaMaeda] p. 67Postulate PS1ps-1 37491
[MaedaMaeda] p. 68Lemma 16.2df-padd 37810  paddclN 37856  paddidm 37855
[MaedaMaeda] p. 68Condition PS2ps-2 37492
[MaedaMaeda] p. 68Equation 16.2.1paddass 37852
[MaedaMaeda] p. 69Lemma 16.4ps-1 37491
[MaedaMaeda] p. 69Theorem 16.4ps-2 37492
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19281  lsmmod2 19282  lssats 37026  shatomici 30720  shatomistici 30723  shmodi 29752  shmodsi 29751
[MaedaMaeda] p. 130Remark 29.6dmdmd 30662  mdsymlem7 30771
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 29951
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 29855
[MaedaMaeda] p. 139Remarksumdmdii 30777
[Margaris] p. 40Rule Cexlimiv 1933
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 397  df-ex 1783  df-or 845  dfbi2 475
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 28764
[Margaris] p. 59Section 14notnotrALTVD 42535
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 42536
[Margaris] p. 79Rule Cexinst01 42245  exinst11 42246
[Margaris] p. 89Theorem 19.219.2 1980  19.2g 2181  r19.2z 4425
[Margaris] p. 89Theorem 19.319.3 2195  rr19.3v 3598
[Margaris] p. 89Theorem 19.5alcom 2156
[Margaris] p. 89Theorem 19.6alex 1828
[Margaris] p. 89Theorem 19.7alnex 1784
[Margaris] p. 89Theorem 19.819.8a 2174
[Margaris] p. 89Theorem 19.919.9 2198  19.9h 2283  exlimd 2211  exlimdh 2287
[Margaris] p. 89Theorem 19.11excom 2162  excomim 2163
[Margaris] p. 89Theorem 19.1219.12 2321
[Margaris] p. 90Section 19conventions-labels 28765  conventions-labels 28765  conventions-labels 28765  conventions-labels 28765
[Margaris] p. 90Theorem 19.14exnal 1829
[Margaris] p. 90Theorem 19.152albi 41996  albi 1821
[Margaris] p. 90Theorem 19.1619.16 2218
[Margaris] p. 90Theorem 19.1719.17 2219
[Margaris] p. 90Theorem 19.182exbi 41998  exbi 1849
[Margaris] p. 90Theorem 19.1919.19 2222
[Margaris] p. 90Theorem 19.202alim 41995  2alimdv 1921  alimd 2205  alimdh 1820  alimdv 1919  ax-4 1812  ralimdaa 3142  ralimdv 3109  ralimdva 3108  ralimdvva 3126  sbcimdv 3790
[Margaris] p. 90Theorem 19.2119.21 2200  19.21h 2284  19.21t 2199  19.21vv 41994  alrimd 2208  alrimdd 2207  alrimdh 1866  alrimdv 1932  alrimi 2206  alrimih 1826  alrimiv 1930  alrimivv 1931  hbralrimi 3101  r19.21be 3135  r19.21bi 3134  ralrimd 3143  ralrimdv 3105  ralrimdva 3106  ralrimdvv 3124  ralrimdvva 3125  ralrimi 3141  ralrimia 3430  ralrimiv 3102  ralrimiva 3103  ralrimivv 3122  ralrimivva 3123  ralrimivvva 3127  ralrimivw 3104
[Margaris] p. 90Theorem 19.222exim 41997  2eximdv 1922  exim 1836  eximd 2209  eximdh 1867  eximdv 1920  rexim 3172  reximd2a 3245  reximdai 3244  reximdd 42701  reximddv 3204  reximddv2 3207  reximddv3 42700  reximdv 3202  reximdv2 3199  reximdva 3203  reximdvai 3200  reximdvva 3206  reximi2 3175
[Margaris] p. 90Theorem 19.2319.23 2204  19.23bi 2184  19.23h 2285  19.23t 2203  exlimdv 1936  exlimdvv 1937  exlimexi 42144  exlimiv 1933  exlimivv 1935  rexlimd3 42693  rexlimdv 3212  rexlimdv3a 3215  rexlimdva 3213  rexlimdva2 3216  rexlimdvaa 3214  rexlimdvv 3222  rexlimdvva 3223  rexlimdvw 3219  rexlimiv 3209  rexlimiva 3210  rexlimivv 3221
[Margaris] p. 90Theorem 19.2419.24 1989
[Margaris] p. 90Theorem 19.2519.25 1883
[Margaris] p. 90Theorem 19.2619.26 1873
[Margaris] p. 90Theorem 19.2719.27 2220  r19.27z 4435  r19.27zv 4436
[Margaris] p. 90Theorem 19.2819.28 2221  19.28vv 42004  r19.28z 4428  r19.28zv 4431  rr19.28v 3599
[Margaris] p. 90Theorem 19.2919.29 1876  r19.29d2r 3264  r19.29imd 3186
[Margaris] p. 90Theorem 19.3019.30 1884
[Margaris] p. 90Theorem 19.3119.31 2227  19.31vv 42002
[Margaris] p. 90Theorem 19.3219.32 2226  r19.32 44590
[Margaris] p. 90Theorem 19.3319.33-2 42000  19.33 1887
[Margaris] p. 90Theorem 19.3419.34 1990
[Margaris] p. 90Theorem 19.3519.35 1880
[Margaris] p. 90Theorem 19.3619.36 2223  19.36vv 42001  r19.36zv 4437
[Margaris] p. 90Theorem 19.3719.37 2225  19.37vv 42003  r19.37zv 4432
[Margaris] p. 90Theorem 19.3819.38 1841
[Margaris] p. 90Theorem 19.3919.39 1988
[Margaris] p. 90Theorem 19.4019.40-2 1890  19.40 1889  r19.40 3275
[Margaris] p. 90Theorem 19.4119.41 2228  19.41rg 42170
[Margaris] p. 90Theorem 19.4219.42 2229
[Margaris] p. 90Theorem 19.4319.43 1885
[Margaris] p. 90Theorem 19.4419.44 2230  r19.44zv 4434
[Margaris] p. 90Theorem 19.4519.45 2231  r19.45zv 4433
[Margaris] p. 110Exercise 2(b)eu1 2612
[Mayet] p. 370Remarkjpi 30632  largei 30629  stri 30619
[Mayet3] p. 9Definition of CH-statesdf-hst 30574  ishst 30576
[Mayet3] p. 10Theoremhstrbi 30628  hstri 30627
[Mayet3] p. 1223Theorem 4.1mayete3i 30090
[Mayet3] p. 1240Theorem 7.1mayetes3i 30091
[MegPav2000] p. 2344Theorem 3.3stcltrthi 30640
[MegPav2000] p. 2345Definition 3.4-1chintcl 29694  chsupcl 29702
[MegPav2000] p. 2345Definition 3.4-2hatomic 30722
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 30716
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 30743
[MegPav2000] p. 2366Figure 7pl42N 37997
[MegPav2002] p. 362Lemma 2.2latj31 18205  latj32 18203  latjass 18201
[Megill] p. 444Axiom C5ax-5 1913  ax5ALT 36921
[Megill] p. 444Section 7conventions 28764
[Megill] p. 445Lemma L12aecom-o 36915  ax-c11n 36902  axc11n 2426
[Megill] p. 446Lemma L17equtrr 2025
[Megill] p. 446Lemma L18ax6fromc10 36910
[Megill] p. 446Lemma L19hbnae-o 36942  hbnae 2432
[Megill] p. 447Remark 9.1dfsb1 2485  sbid 2248  sbidd-misc 46421  sbidd 46420
[Megill] p. 448Remark 9.6axc14 2463
[Megill] p. 448Scheme C4'ax-c4 36898
[Megill] p. 448Scheme C5'ax-c5 36897  sp 2176
[Megill] p. 448Scheme C6'ax-11 2154
[Megill] p. 448Scheme C7'ax-c7 36899
[Megill] p. 448Scheme C8'ax-7 2011
[Megill] p. 448Scheme C9'ax-c9 36904
[Megill] p. 448Scheme C10'ax-6 1971  ax-c10 36900
[Megill] p. 448Scheme C11'ax-c11 36901
[Megill] p. 448Scheme C12'ax-8 2108
[Megill] p. 448Scheme C13'ax-9 2116
[Megill] p. 448Scheme C14'ax-c14 36905
[Megill] p. 448Scheme C15'ax-c15 36903
[Megill] p. 448Scheme C16'ax-c16 36906
[Megill] p. 448Theorem 9.4dral1-o 36918  dral1 2439  dral2-o 36944  dral2 2438  drex1 2441  drex2 2442  drsb1 2499  drsb2 2258
[Megill] p. 449Theorem 9.7sbcom2 2161  sbequ 2086  sbid2v 2513
[Megill] p. 450Example in Appendixhba1-o 36911  hba1 2290
[Mendelson] p. 35Axiom A3hirstL-ax3 44387
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3812  rspsbca 3813  stdpc4 2071
[Mendelson] p. 69Axiom 5ax-c4 36898  ra4 3819  stdpc5 2201
[Mendelson] p. 81Rule Cexlimiv 1933
[Mendelson] p. 95Axiom 6stdpc6 2031
[Mendelson] p. 95Axiom 7stdpc7 2243
[Mendelson] p. 225Axiom system NBGru 3715
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5428
[Mendelson] p. 231Exercise 4.10(k)inv1 4328
[Mendelson] p. 231Exercise 4.10(l)unv 4329
[Mendelson] p. 231Exercise 4.10(n)dfin3 4200
[Mendelson] p. 231Exercise 4.10(o)df-nul 4257
[Mendelson] p. 231Exercise 4.10(q)dfin4 4201
[Mendelson] p. 231Exercise 4.10(s)ddif 4071
[Mendelson] p. 231Definition of uniondfun3 4199
[Mendelson] p. 235Exercise 4.12(c)univ 5367
[Mendelson] p. 235Exercise 4.12(d)pwv 4836
[Mendelson] p. 235Exercise 4.12(j)pwin 5483
[Mendelson] p. 235Exercise 4.12(k)pwunss 4553
[Mendelson] p. 235Exercise 4.12(l)pwssun 5485
[Mendelson] p. 235Exercise 4.12(n)uniin 4865
[Mendelson] p. 235Exercise 4.12(p)reli 5736
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6172
[Mendelson] p. 244Proposition 4.8(g)epweon 7625
[Mendelson] p. 246Definition of successordf-suc 6272
[Mendelson] p. 250Exercise 4.36oelim2 8426
[Mendelson] p. 254Proposition 4.22(b)xpen 8927
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8842  xpsneng 8843
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8850  xpcomeng 8851
[Mendelson] p. 254Proposition 4.22(e)xpassen 8853
[Mendelson] p. 255Definitionbrsdom 8763
[Mendelson] p. 255Exercise 4.39endisj 8845
[Mendelson] p. 255Exercise 4.41mapprc 8619
[Mendelson] p. 255Exercise 4.43mapsnen 8827  mapsnend 8826
[Mendelson] p. 255Exercise 4.45mapunen 8933
[Mendelson] p. 255Exercise 4.47xpmapen 8932
[Mendelson] p. 255Exercise 4.42(a)map0e 8670
[Mendelson] p. 255Exercise 4.42(b)map1 8830
[Mendelson] p. 257Proposition 4.24(a)undom 8846
[Mendelson] p. 258Exercise 4.56(c)djuassen 9934  djucomen 9933
[Mendelson] p. 258Exercise 4.56(f)djudom1 9938
[Mendelson] p. 258Exercise 4.56(g)xp2dju 9932
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8361
[Mendelson] p. 266Proposition 4.34(f)oaordex 8389
[Mendelson] p. 275Proposition 4.42(d)entri3 10315
[Mendelson] p. 281Definitiondf-r1 9522
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9571
[Mendelson] p. 287Axiom system MKru 3715
[MertziosUnger] p. 152Definitiondf-frgr 28623
[MertziosUnger] p. 153Remark 1frgrconngr 28658
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 28660  vdgn1frgrv3 28661
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 28662
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 28655
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 28648  2pthfrgrrn 28646  2pthfrgrrn2 28647
[Mittelstaedt] p. 9Definitiondf-oc 29614
[Monk1] p. 22Remarkconventions 28764
[Monk1] p. 22Theorem 3.1conventions 28764
[Monk1] p. 26Theorem 2.8(vii)ssin 4164
[Monk1] p. 33Theorem 3.2(i)ssrel 5693  ssrelf 30955
[Monk1] p. 33Theorem 3.2(ii)eqrel 5695
[Monk1] p. 34Definition 3.3df-opab 5137
[Monk1] p. 36Theorem 3.7(i)coi1 6166  coi2 6167
[Monk1] p. 36Theorem 3.8(v)dm0 5829  rn0 5835
[Monk1] p. 36Theorem 3.7(ii)cnvi 6045
[Monk1] p. 37Theorem 3.13(i)relxp 5607
[Monk1] p. 37Theorem 3.13(x)dmxp 5838  rnxp 6073
[Monk1] p. 37Theorem 3.13(ii)0xp 5685  xp0 6061
[Monk1] p. 38Theorem 3.16(ii)ima0 5985
[Monk1] p. 38Theorem 3.16(viii)imai 5982
[Monk1] p. 39Theorem 3.17imaex 7763  imaexALTV 36465  imaexg 7762
[Monk1] p. 39Theorem 3.16(xi)imassrn 5980
[Monk1] p. 41Theorem 4.3(i)fnopfv 6953  funfvop 6927
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6825
[Monk1] p. 42Theorem 4.4(iii)fvelima 6835
[Monk1] p. 43Theorem 4.6funun 6480
[Monk1] p. 43Theorem 4.8(iv)dff13 7128  dff13f 7129
[Monk1] p. 46Theorem 4.15(v)funex 7095  funrnex 7796
[Monk1] p. 50Definition 5.4fniunfv 7120
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6130
[Monk1] p. 52Theorem 5.11(viii)ssint 4895
[Monk1] p. 52Definition 5.13 (i)1stval2 7848  df-1st 7831
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7849  df-2nd 7832
[Monk1] p. 112Theorem 15.17(v)ranksn 9612  ranksnb 9585
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9613
[Monk1] p. 112Theorem 15.17(iii)rankun 9614  rankunb 9608
[Monk1] p. 113Theorem 15.18r1val3 9596
[Monk1] p. 113Definition 15.19df-r1 9522  r1val2 9595
[Monk1] p. 117Lemmazorn2 10262  zorn2g 10259
[Monk1] p. 133Theorem 18.11cardom 9744
[Monk1] p. 133Theorem 18.12canth3 10317
[Monk1] p. 133Theorem 18.14carduni 9739
[Monk2] p. 105Axiom C4ax-4 1812
[Monk2] p. 105Axiom C7ax-7 2011
[Monk2] p. 105Axiom C8ax-12 2171  ax-c15 36903  ax12v2 2173
[Monk2] p. 108Lemma 5ax-c4 36898
[Monk2] p. 109Lemma 12ax-11 2154
[Monk2] p. 109Lemma 15equvini 2455  equvinv 2032  eqvinop 5401
[Monk2] p. 113Axiom C5-1ax-5 1913  ax5ALT 36921
[Monk2] p. 113Axiom C5-2ax-10 2137
[Monk2] p. 113Axiom C5-3ax-11 2154
[Monk2] p. 114Lemma 21sp 2176
[Monk2] p. 114Lemma 22axc4 2315  hba1-o 36911  hba1 2290
[Monk2] p. 114Lemma 23nfia1 2150
[Monk2] p. 114Lemma 24nfa2 2170  nfra2 3157  nfra2w 3154
[Moore] p. 53Part Idf-mre 17295
[Munkres] p. 77Example 2distop 22145  indistop 22152  indistopon 22151
[Munkres] p. 77Example 3fctop 22154  fctop2 22155
[Munkres] p. 77Example 4cctop 22156
[Munkres] p. 78Definition of basisdf-bases 22096  isbasis3g 22099
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17154  tgval2 22106
[Munkres] p. 79Remarktgcl 22119
[Munkres] p. 80Lemma 2.1tgval3 22113
[Munkres] p. 80Lemma 2.2tgss2 22137  tgss3 22136
[Munkres] p. 81Lemma 2.3basgen 22138  basgen2 22139
[Munkres] p. 83Exercise 3topdifinf 35520  topdifinfeq 35521  topdifinffin 35519  topdifinfindis 35517
[Munkres] p. 89Definition of subspace topologyresttop 22311
[Munkres] p. 93Theorem 6.1(1)0cld 22189  topcld 22186
[Munkres] p. 93Theorem 6.1(2)iincld 22190
[Munkres] p. 93Theorem 6.1(3)uncld 22192
[Munkres] p. 94Definition of closureclsval 22188
[Munkres] p. 94Definition of interiorntrval 22187
[Munkres] p. 95Theorem 6.5(a)clsndisj 22226  elcls 22224
[Munkres] p. 95Theorem 6.5(b)elcls3 22234
[Munkres] p. 97Theorem 6.6clslp 22299  neindisj 22268
[Munkres] p. 97Corollary 6.7cldlp 22301
[Munkres] p. 97Definition of limit pointislp2 22296  lpval 22290
[Munkres] p. 98Definition of Hausdorff spacedf-haus 22466
[Munkres] p. 102Definition of continuous functiondf-cn 22378  iscn 22386  iscn2 22389
[Munkres] p. 107Theorem 7.2(g)cncnp 22431  cncnp2 22432  cncnpi 22429  df-cnp 22379  iscnp 22388  iscnp2 22390
[Munkres] p. 127Theorem 10.1metcn 23699
[Munkres] p. 128Theorem 10.3metcn4 24475
[Nathanson] p. 123Remarkreprgt 32601  reprinfz1 32602  reprlt 32599
[Nathanson] p. 123Definitiondf-repr 32589
[Nathanson] p. 123Chapter 5.1circlemethnat 32621
[Nathanson] p. 123Propositionbreprexp 32613  breprexpnat 32614  itgexpif 32586
[NielsenChuang] p. 195Equation 4.73unierri 30466
[OeSilva] p. 2042Section 2ax-bgbltosilva 45262
[Pfenning] p. 17Definition XMnatded 28767
[Pfenning] p. 17Definition NNCnatded 28767  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 28767
[Pfenning] p. 18Rule"natded 28767
[Pfenning] p. 18Definition /\Inatded 28767
[Pfenning] p. 18Definition ` `Enatded 28767  natded 28767  natded 28767  natded 28767  natded 28767
[Pfenning] p. 18Definition ` `Inatded 28767  natded 28767  natded 28767  natded 28767  natded 28767
[Pfenning] p. 18Definition ` `ELnatded 28767
[Pfenning] p. 18Definition ` `ERnatded 28767
[Pfenning] p. 18Definition ` `Ea,unatded 28767
[Pfenning] p. 18Definition ` `IRnatded 28767
[Pfenning] p. 18Definition ` `Ianatded 28767
[Pfenning] p. 127Definition =Enatded 28767
[Pfenning] p. 127Definition =Inatded 28767
[Ponnusamy] p. 361Theorem 6.44cphip0l 24366  df-dip 29063  dip0l 29080  ip0l 20841
[Ponnusamy] p. 361Equation 6.45cphipval 24407  ipval 29065
[Ponnusamy] p. 362Equation I1dipcj 29076  ipcj 20839
[Ponnusamy] p. 362Equation I3cphdir 24369  dipdir 29204  ipdir 20844  ipdiri 29192
[Ponnusamy] p. 362Equation I4ipidsq 29072  nmsq 24358
[Ponnusamy] p. 362Equation 6.46ip0i 29187
[Ponnusamy] p. 362Equation 6.47ip1i 29189
[Ponnusamy] p. 362Equation 6.48ip2i 29190
[Ponnusamy] p. 363Equation I2cphass 24375  dipass 29207  ipass 20850  ipassi 29203
[Prugovecki] p. 186Definition of brabraval 30306  df-bra 30212
[Prugovecki] p. 376Equation 8.1df-kb 30213  kbval 30316
[PtakPulmannova] p. 66Proposition 3.2.17atomli 30744
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 37902
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 30758  atcvat4i 30759  cvrat3 37456  cvrat4 37457  lsatcvat3 37066
[PtakPulmannova] p. 68Definition 3.2.18cvbr 30644  cvrval 37283  df-cv 30641  df-lcv 37033  lspsncv0 20408
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 37914
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 37915
[Quine] p. 16Definition 2.1df-clab 2716  rabid 3310
[Quine] p. 17Definition 2.1''dfsb7 2276
[Quine] p. 18Definition 2.7df-cleq 2730
[Quine] p. 19Definition 2.9conventions 28764  df-v 3434
[Quine] p. 34Theorem 5.1abeq2 2872
[Quine] p. 35Theorem 5.2abid1 2881  abid2f 2939
[Quine] p. 40Theorem 6.1sb5 2268
[Quine] p. 40Theorem 6.2sb6 2088  sbalex 2235
[Quine] p. 41Theorem 6.3df-clel 2816
[Quine] p. 41Theorem 6.4eqid 2738  eqid1 28831
[Quine] p. 41Theorem 6.5eqcom 2745
[Quine] p. 42Theorem 6.6df-sbc 3717
[Quine] p. 42Theorem 6.7dfsbcq 3718  dfsbcq2 3719
[Quine] p. 43Theorem 6.8vex 3436
[Quine] p. 43Theorem 6.9isset 3445
[Quine] p. 44Theorem 7.3spcgf 3530  spcgv 3535  spcimgf 3528
[Quine] p. 44Theorem 6.11spsbc 3729  spsbcd 3730
[Quine] p. 44Theorem 6.12elex 3450
[Quine] p. 44Theorem 6.13elab 3609  elabg 3607  elabgf 3605
[Quine] p. 44Theorem 6.14noel 4264
[Quine] p. 48Theorem 7.2snprc 4653
[Quine] p. 48Definition 7.1df-pr 4564  df-sn 4562
[Quine] p. 49Theorem 7.4snss 4719  snssg 4718
[Quine] p. 49Theorem 7.5prss 4753  prssg 4752
[Quine] p. 49Theorem 7.6prid1 4698  prid1g 4696  prid2 4699  prid2g 4697  snid 4597  snidg 4595
[Quine] p. 51Theorem 7.12snex 5354
[Quine] p. 51Theorem 7.13prex 5355
[Quine] p. 53Theorem 8.2unisn 4861  unisnALT 42546  unisng 4860
[Quine] p. 53Theorem 8.3uniun 4864
[Quine] p. 54Theorem 8.6elssuni 4871
[Quine] p. 54Theorem 8.7uni0 4869
[Quine] p. 56Theorem 8.17uniabio 6406
[Quine] p. 56Definition 8.18dfaiota2 44578  dfiota2 6392
[Quine] p. 57Theorem 8.19aiotaval 44587  iotaval 6407
[Quine] p. 57Theorem 8.22iotanul 6411
[Quine] p. 58Theorem 8.23iotaex 6413
[Quine] p. 58Definition 9.1df-op 4568
[Quine] p. 61Theorem 9.5opabid 5438  opabidw 5437  opelopab 5455  opelopaba 5449  opelopabaf 5457  opelopabf 5458  opelopabg 5451  opelopabga 5446  opelopabgf 5453  oprabid 7307  oprabidw 7306
[Quine] p. 64Definition 9.11df-xp 5595
[Quine] p. 64Definition 9.12df-cnv 5597
[Quine] p. 64Definition 9.15df-id 5489
[Quine] p. 65Theorem 10.3fun0 6499
[Quine] p. 65Theorem 10.4funi 6466
[Quine] p. 65Theorem 10.5funsn 6487  funsng 6485
[Quine] p. 65Definition 10.1df-fun 6435
[Quine] p. 65Definition 10.2args 6000  dffv4 6771
[Quine] p. 68Definition 10.11conventions 28764  df-fv 6441  fv2 6769
[Quine] p. 124Theorem 17.3nn0opth2 13986  nn0opth2i 13985  nn0opthi 13984  omopthi 8491
[Quine] p. 177Definition 25.2df-rdg 8241
[Quine] p. 232Equation icarddom 10310
[Quine] p. 284Axiom 39(vi)funimaex 6521  funimaexg 6520
[Quine] p. 331Axiom system NFru 3715
[ReedSimon] p. 36Definition (iii)ax-his3 29446
[ReedSimon] p. 63Exercise 4(a)df-dip 29063  polid 29521  polid2i 29519  polidi 29520
[ReedSimon] p. 63Exercise 4(b)df-ph 29175
[ReedSimon] p. 195Remarklnophm 30381  lnophmi 30380
[Retherford] p. 49Exercise 1(i)leopadd 30494
[Retherford] p. 49Exercise 1(ii)leopmul 30496  leopmuli 30495
[Retherford] p. 49Exercise 1(iv)leoptr 30499
[Retherford] p. 49Definition VI.1df-leop 30214  leoppos 30488
[Retherford] p. 49Exercise 1(iii)leoptri 30498
[Retherford] p. 49Definition of operator orderingleop3 30487
[Roman] p. 4Definitiondf-dmat 21639  df-dmatalt 45739
[Roman] p. 18Part Preliminariesdf-rng0 45433
[Roman] p. 19Part Preliminariesdf-ring 19785
[Roman] p. 46Theorem 1.6isldepslvec2 45826
[Roman] p. 112Noteisldepslvec2 45826  ldepsnlinc 45849  zlmodzxznm 45838
[Roman] p. 112Examplezlmodzxzequa 45837  zlmodzxzequap 45840  zlmodzxzldep 45845
[Roman] p. 170Theorem 7.8cayleyhamilton 22039
[Rosenlicht] p. 80Theoremheicant 35812
[Rosser] p. 281Definitiondf-op 4568
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 32625
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 32626
[Rotman] p. 28Remarkpgrpgt2nabl 45702  pmtr3ncom 19083
[Rotman] p. 31Theorem 3.4symggen2 19079
[Rotman] p. 42Theorem 3.15cayley 19022  cayleyth 19023
[Rudin] p. 164Equation 27efcan 15805
[Rudin] p. 164Equation 30efzval 15811
[Rudin] p. 167Equation 48absefi 15905
[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 6020
[Schechter] p. 51Definition of irreflexivityintirr 6023
[Schechter] p. 51Definition of symmetrycnvsym 6019
[Schechter] p. 51Definition of transitivitycotr 6017
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17295
[Schechter] p. 79Definition of Moore closuredf-mrc 17296
[Schechter] p. 82Section 4.5df-mrc 17296
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17298
[Schechter] p. 139Definition AC3dfac9 9892
[Schechter] p. 141Definition (MC)dfac11 40887
[Schechter] p. 149Axiom DC1ax-dc 10202  axdc3 10210
[Schechter] p. 187Definition of ring with unitisring 19787  isrngo 36055
[Schechter] p. 276Remark 11.6.espan0 29904
[Schechter] p. 276Definition of spandf-span 29671  spanval 29695
[Schechter] p. 428Definition 15.35bastop1 22143
[Schwabhauser] p. 10Axiom A1axcgrrflx 27282  axtgcgrrflx 26823
[Schwabhauser] p. 10Axiom A2axcgrtr 27283
[Schwabhauser] p. 10Axiom A3axcgrid 27284  axtgcgrid 26824
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 26809
[Schwabhauser] p. 11Axiom A4axsegcon 27295  axtgsegcon 26825  df-trkgcb 26811
[Schwabhauser] p. 11Axiom A5ax5seg 27306  axtg5seg 26826  df-trkgcb 26811
[Schwabhauser] p. 11Axiom A6axbtwnid 27307  axtgbtwnid 26827  df-trkgb 26810
[Schwabhauser] p. 12Axiom A7axpasch 27309  axtgpasch 26828  df-trkgb 26810
[Schwabhauser] p. 12Axiom A8axlowdim2 27328  df-trkg2d 32645
[Schwabhauser] p. 13Axiom A8axtglowdim2 26831
[Schwabhauser] p. 13Axiom A9axtgupdim2 26832  df-trkg2d 32645
[Schwabhauser] p. 13Axiom A10axeuclid 27331  axtgeucl 26833  df-trkge 26812
[Schwabhauser] p. 13Axiom A11axcont 27344  axtgcont 26830  axtgcont1 26829  df-trkgb 26810
[Schwabhauser] p. 27Theorem 2.1cgrrflx 34289
[Schwabhauser] p. 27Theorem 2.2cgrcomim 34291
[Schwabhauser] p. 27Theorem 2.3cgrtr 34294
[Schwabhauser] p. 27Theorem 2.4cgrcoml 34298
[Schwabhauser] p. 27Theorem 2.5cgrcomr 34299  tgcgrcomimp 26838  tgcgrcoml 26840  tgcgrcomr 26839
[Schwabhauser] p. 28Theorem 2.8cgrtriv 34304  tgcgrtriv 26845
[Schwabhauser] p. 28Theorem 2.105segofs 34308  tg5segofs 32653
[Schwabhauser] p. 28Definition 2.10df-afs 32650  df-ofs 34285
[Schwabhauser] p. 29Theorem 2.11cgrextend 34310  tgcgrextend 26846
[Schwabhauser] p. 29Theorem 2.12segconeq 34312  tgsegconeq 26847
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 34324  btwntriv2 34314  tgbtwntriv2 26848
[Schwabhauser] p. 30Theorem 3.2btwncomim 34315  tgbtwncom 26849
[Schwabhauser] p. 30Theorem 3.3btwntriv1 34318  tgbtwntriv1 26852
[Schwabhauser] p. 30Theorem 3.4btwnswapid 34319  tgbtwnswapid 26853
[Schwabhauser] p. 30Theorem 3.5btwnexch2 34325  btwnintr 34321  tgbtwnexch2 26857  tgbtwnintr 26854
[Schwabhauser] p. 30Theorem 3.6btwnexch 34327  btwnexch3 34322  tgbtwnexch 26859  tgbtwnexch3 26855
[Schwabhauser] p. 30Theorem 3.7btwnouttr 34326  tgbtwnouttr 26858  tgbtwnouttr2 26856
[Schwabhauser] p. 32Theorem 3.13axlowdim1 27327
[Schwabhauser] p. 32Theorem 3.14btwndiff 34329  tgbtwndiff 26867
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 26860  trisegint 34330
[Schwabhauser] p. 34Theorem 4.2ifscgr 34346  tgifscgr 26869
[Schwabhauser] p. 34Theorem 4.11colcom 26919  colrot1 26920  colrot2 26921  lncom 26983  lnrot1 26984  lnrot2 26985
[Schwabhauser] p. 34Definition 4.1df-ifs 34342
[Schwabhauser] p. 35Theorem 4.3cgrsub 34347  tgcgrsub 26870
[Schwabhauser] p. 35Theorem 4.5cgrxfr 34357  tgcgrxfr 26879
[Schwabhauser] p. 35Statement 4.4ercgrg 26878
[Schwabhauser] p. 35Definition 4.4df-cgr3 34343  df-cgrg 26872
[Schwabhauser] p. 35Definition instead (givendf-cgrg 26872
[Schwabhauser] p. 36Theorem 4.6btwnxfr 34358  tgbtwnxfr 26891
[Schwabhauser] p. 36Theorem 4.11colinearperm1 34364  colinearperm2 34366  colinearperm3 34365  colinearperm4 34367  colinearperm5 34368
[Schwabhauser] p. 36Definition 4.8df-ismt 26894
[Schwabhauser] p. 36Definition 4.10df-colinear 34341  tgellng 26914  tglng 26907
[Schwabhauser] p. 37Theorem 4.12colineartriv1 34369
[Schwabhauser] p. 37Theorem 4.13colinearxfr 34377  lnxfr 26927
[Schwabhauser] p. 37Theorem 4.14lineext 34378  lnext 26928
[Schwabhauser] p. 37Theorem 4.16fscgr 34382  tgfscgr 26929
[Schwabhauser] p. 37Theorem 4.17linecgr 34383  lncgr 26930
[Schwabhauser] p. 37Definition 4.15df-fs 34344
[Schwabhauser] p. 38Theorem 4.18lineid 34385  lnid 26931
[Schwabhauser] p. 38Theorem 4.19idinside 34386  tgidinside 26932
[Schwabhauser] p. 39Theorem 5.1btwnconn1 34403  tgbtwnconn1 26936
[Schwabhauser] p. 41Theorem 5.2btwnconn2 34404  tgbtwnconn2 26937
[Schwabhauser] p. 41Theorem 5.3btwnconn3 34405  tgbtwnconn3 26938
[Schwabhauser] p. 41Theorem 5.5brsegle2 34411
[Schwabhauser] p. 41Definition 5.4df-segle 34409  legov 26946
[Schwabhauser] p. 41Definition 5.5legov2 26947
[Schwabhauser] p. 42Remark 5.13legso 26960
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 34412
[Schwabhauser] p. 42Theorem 5.7seglerflx 34414
[Schwabhauser] p. 42Theorem 5.8segletr 34416
[Schwabhauser] p. 42Theorem 5.9segleantisym 34417
[Schwabhauser] p. 42Theorem 5.10seglelin 34418
[Schwabhauser] p. 42Theorem 5.11seglemin 34415
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 34420
[Schwabhauser] p. 42Proposition 5.7legid 26948
[Schwabhauser] p. 42Proposition 5.8legtrd 26950
[Schwabhauser] p. 42Proposition 5.9legtri3 26951
[Schwabhauser] p. 42Proposition 5.10legtrid 26952
[Schwabhauser] p. 42Proposition 5.11leg0 26953
[Schwabhauser] p. 43Theorem 6.2btwnoutside 34427
[Schwabhauser] p. 43Theorem 6.3broutsideof3 34428
[Schwabhauser] p. 43Theorem 6.4broutsideof 34423  df-outsideof 34422
[Schwabhauser] p. 43Definition 6.1broutsideof2 34424  ishlg 26963
[Schwabhauser] p. 44Theorem 6.4hlln 26968
[Schwabhauser] p. 44Theorem 6.5hlid 26970  outsideofrflx 34429
[Schwabhauser] p. 44Theorem 6.6hlcomb 26964  hlcomd 26965  outsideofcom 34430
[Schwabhauser] p. 44Theorem 6.7hltr 26971  outsideoftr 34431
[Schwabhauser] p. 44Theorem 6.11hlcgreu 26979  outsideofeu 34433
[Schwabhauser] p. 44Definition 6.8df-ray 34440
[Schwabhauser] p. 45Part 2df-lines2 34441
[Schwabhauser] p. 45Theorem 6.13outsidele 34434
[Schwabhauser] p. 45Theorem 6.15lineunray 34449
[Schwabhauser] p. 45Theorem 6.16lineelsb2 34450  tglineelsb2 26993
[Schwabhauser] p. 45Theorem 6.17linecom 34452  linerflx1 34451  linerflx2 34453  tglinecom 26996  tglinerflx1 26994  tglinerflx2 26995
[Schwabhauser] p. 45Theorem 6.18linethru 34455  tglinethru 26997
[Schwabhauser] p. 45Definition 6.14df-line2 34439  tglng 26907
[Schwabhauser] p. 45Proposition 6.13legbtwn 26955
[Schwabhauser] p. 46Theorem 6.19linethrueu 34458  tglinethrueu 27000
[Schwabhauser] p. 46Theorem 6.21lineintmo 34459  tglineineq 27004  tglineinteq 27006  tglineintmo 27003
[Schwabhauser] p. 46Theorem 6.23colline 27010
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 27011
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 27012
[Schwabhauser] p. 49Theorem 7.3mirinv 27027
[Schwabhauser] p. 49Theorem 7.7mirmir 27023
[Schwabhauser] p. 49Theorem 7.8mirreu3 27015
[Schwabhauser] p. 49Definition 7.5df-mir 27014  ismir 27020  mirbtwn 27019  mircgr 27018  mirfv 27017  mirval 27016
[Schwabhauser] p. 50Theorem 7.8mirreu 27025
[Schwabhauser] p. 50Theorem 7.9mireq 27026
[Schwabhauser] p. 50Theorem 7.10mirinv 27027
[Schwabhauser] p. 50Theorem 7.11mirf1o 27030
[Schwabhauser] p. 50Theorem 7.13miriso 27031
[Schwabhauser] p. 51Theorem 7.14mirmot 27036
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 27033  mirbtwni 27032
[Schwabhauser] p. 51Theorem 7.16mircgrs 27034
[Schwabhauser] p. 51Theorem 7.17miduniq 27046
[Schwabhauser] p. 52Lemma 7.21symquadlem 27050
[Schwabhauser] p. 52Theorem 7.18miduniq1 27047
[Schwabhauser] p. 52Theorem 7.19miduniq2 27048
[Schwabhauser] p. 52Theorem 7.20colmid 27049
[Schwabhauser] p. 53Lemma 7.22krippen 27052
[Schwabhauser] p. 55Lemma 7.25midexlem 27053
[Schwabhauser] p. 57Theorem 8.2ragcom 27059
[Schwabhauser] p. 57Definition 8.1df-rag 27055  israg 27058
[Schwabhauser] p. 58Theorem 8.3ragcol 27060
[Schwabhauser] p. 58Theorem 8.4ragmir 27061
[Schwabhauser] p. 58Theorem 8.5ragtrivb 27063
[Schwabhauser] p. 58Theorem 8.6ragflat2 27064
[Schwabhauser] p. 58Theorem 8.7ragflat 27065
[Schwabhauser] p. 58Theorem 8.8ragtriva 27066
[Schwabhauser] p. 58Theorem 8.9ragflat3 27067  ragncol 27070
[Schwabhauser] p. 58Theorem 8.10ragcgr 27068
[Schwabhauser] p. 59Theorem 8.12perpcom 27074
[Schwabhauser] p. 59Theorem 8.13ragperp 27078
[Schwabhauser] p. 59Theorem 8.14perpneq 27075
[Schwabhauser] p. 59Definition 8.11df-perpg 27057  isperp 27073
[Schwabhauser] p. 59Definition 8.13isperp2 27076
[Schwabhauser] p. 60Theorem 8.18foot 27083
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 27091  colperpexlem2 27092
[Schwabhauser] p. 63Theorem 8.21colperpex 27094  colperpexlem3 27093
[Schwabhauser] p. 64Theorem 8.22mideu 27099  midex 27098
[Schwabhauser] p. 66Lemma 8.24opphllem 27096
[Schwabhauser] p. 67Theorem 9.2oppcom 27105
[Schwabhauser] p. 67Definition 9.1islnopp 27100
[Schwabhauser] p. 68Lemma 9.3opphllem2 27109
[Schwabhauser] p. 68Lemma 9.4opphllem5 27112  opphllem6 27113
[Schwabhauser] p. 69Theorem 9.5opphl 27115
[Schwabhauser] p. 69Theorem 9.6axtgpasch 26828
[Schwabhauser] p. 70Theorem 9.6outpasch 27116
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 27124
[Schwabhauser] p. 71Definition 9.7df-hpg 27119  hpgbr 27121
[Schwabhauser] p. 72Lemma 9.10hpgerlem 27126
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 27125
[Schwabhauser] p. 72Theorem 9.11hpgid 27127
[Schwabhauser] p. 72Theorem 9.12hpgcom 27128
[Schwabhauser] p. 72Theorem 9.13hpgtr 27129
[Schwabhauser] p. 73Theorem 9.18colopp 27130
[Schwabhauser] p. 73Theorem 9.19colhp 27131
[Schwabhauser] p. 88Theorem 10.2lmieu 27145
[Schwabhauser] p. 88Definition 10.1df-mid 27135
[Schwabhauser] p. 89Theorem 10.4lmicom 27149
[Schwabhauser] p. 89Theorem 10.5lmilmi 27150
[Schwabhauser] p. 89Theorem 10.6lmireu 27151
[Schwabhauser] p. 89Theorem 10.7lmieq 27152
[Schwabhauser] p. 89Theorem 10.8lmiinv 27153
[Schwabhauser] p. 89Theorem 10.9lmif1o 27156
[Schwabhauser] p. 89Theorem 10.10lmiiso 27158
[Schwabhauser] p. 89Definition 10.3df-lmi 27136
[Schwabhauser] p. 90Theorem 10.11lmimot 27159
[Schwabhauser] p. 91Theorem 10.12hypcgr 27162
[Schwabhauser] p. 92Theorem 10.14lmiopp 27163
[Schwabhauser] p. 92Theorem 10.15lnperpex 27164
[Schwabhauser] p. 92Theorem 10.16trgcopy 27165  trgcopyeu 27167
[Schwabhauser] p. 95Definition 11.2dfcgra2 27191
[Schwabhauser] p. 95Definition 11.3iscgra 27170
[Schwabhauser] p. 95Proposition 11.4cgracgr 27179
[Schwabhauser] p. 95Proposition 11.10cgrahl1 27177  cgrahl2 27178
[Schwabhauser] p. 96Theorem 11.6cgraid 27180
[Schwabhauser] p. 96Theorem 11.9cgraswap 27181
[Schwabhauser] p. 97Theorem 11.7cgracom 27183
[Schwabhauser] p. 97Theorem 11.8cgratr 27184
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 27187  cgrahl 27188
[Schwabhauser] p. 98Theorem 11.13sacgr 27192
[Schwabhauser] p. 98Theorem 11.14oacgr 27193
[Schwabhauser] p. 98Theorem 11.15acopy 27194  acopyeu 27195
[Schwabhauser] p. 101Theorem 11.24inagswap 27202
[Schwabhauser] p. 101Theorem 11.25inaghl 27206
[Schwabhauser] p. 101Definition 11.23isinag 27199
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 27214
[Schwabhauser] p. 102Definition 11.27df-leag 27207  isleag 27208
[Schwabhauser] p. 107Theorem 11.49tgsas 27216  tgsas1 27215  tgsas2 27217  tgsas3 27218
[Schwabhauser] p. 108Theorem 11.50tgasa 27220  tgasa1 27219
[Schwabhauser] p. 109Theorem 11.51tgsss1 27221  tgsss2 27222  tgsss3 27223
[Shapiro] p. 230Theorem 6.5.1dchrhash 26419  dchrsum 26417  dchrsum2 26416  sumdchr 26420
[Shapiro] p. 232Theorem 6.5.2dchr2sum 26421  sum2dchr 26422
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19669  ablfacrp2 19670
[Shapiro], p. 328Equation 9.2.4vmasum 26364
[Shapiro], p. 329Equation 9.2.7logfac2 26365
[Shapiro], p. 329Equation 9.2.9logfacrlim 26372
[Shapiro], p. 331Equation 9.2.13vmadivsum 26630
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 26633
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 26687  vmalogdivsum2 26686
[Shapiro], p. 375Theorem 9.4.1dirith 26677  dirith2 26676
[Shapiro], p. 375Equation 9.4.3rplogsum 26675  rpvmasum 26674  rpvmasum2 26660
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 26635
[Shapiro], p. 376Equation 9.4.8dchrvmasum 26673
[Shapiro], p. 377Lemma 9.4.1dchrisum 26640  dchrisumlem1 26637  dchrisumlem2 26638  dchrisumlem3 26639  dchrisumlema 26636
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 26643
[Shapiro], p. 379Equation 9.4.16dchrmusum 26672  dchrmusumlem 26670  dchrvmasumlem 26671
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 26642
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 26644
[Shapiro], p. 382Lemma 9.4.4dchrisum0 26668  dchrisum0re 26661  dchrisumn0 26669
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 26654
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 26658
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 26659
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 26714  pntrsumbnd2 26715  pntrsumo1 26713
[Shapiro], p. 405Equation 10.2.1mudivsum 26678
[Shapiro], p. 406Equation 10.2.6mulogsum 26680
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 26682
[Shapiro], p. 407Equation 10.2.8mulog2sum 26685
[Shapiro], p. 418Equation 10.4.6logsqvma 26690
[Shapiro], p. 418Equation 10.4.8logsqvma2 26691
[Shapiro], p. 419Equation 10.4.10selberg 26696
[Shapiro], p. 420Equation 10.4.12selberg2lem 26698
[Shapiro], p. 420Equation 10.4.14selberg2 26699
[Shapiro], p. 422Equation 10.6.7selberg3 26707
[Shapiro], p. 422Equation 10.4.20selberg4lem1 26708
[Shapiro], p. 422Equation 10.4.21selberg3lem1 26705  selberg3lem2 26706
[Shapiro], p. 422Equation 10.4.23selberg4 26709
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 26703
[Shapiro], p. 428Equation 10.6.2selbergr 26716
[Shapiro], p. 429Equation 10.6.8selberg3r 26717
[Shapiro], p. 430Equation 10.6.11selberg4r 26718
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 26732
[Shapiro], p. 434Equation 10.6.27pntlema 26744  pntlemb 26745  pntlemc 26743  pntlemd 26742  pntlemg 26746
[Shapiro], p. 435Equation 10.6.29pntlema 26744
[Shapiro], p. 436Lemma 10.6.1pntpbnd 26736
[Shapiro], p. 436Lemma 10.6.2pntibnd 26741
[Shapiro], p. 436Equation 10.6.34pntlema 26744
[Shapiro], p. 436Equation 10.6.35pntlem3 26757  pntleml 26759
[Stoll] p. 13Definition corresponds to dfsymdif3 4230
[Stoll] p. 16Exercise 4.40dif 4335  dif0 4306
[Stoll] p. 16Exercise 4.8difdifdir 4422
[Stoll] p. 17Theorem 5.1(5)unvdif 4408
[Stoll] p. 19Theorem 5.2(13)undm 4221
[Stoll] p. 19Theorem 5.2(13')indm 4222
[Stoll] p. 20Remarkinvdif 4202
[Stoll] p. 25Definition of ordered tripledf-ot 4570
[Stoll] p. 43Definitionuniiun 4988
[Stoll] p. 44Definitionintiin 4989
[Stoll] p. 45Definitiondf-iin 4927
[Stoll] p. 45Definition indexed uniondf-iun 4926
[Stoll] p. 176Theorem 3.4(27)iman 402
[Stoll] p. 262Example 4.1dfsymdif3 4230
[Strang] p. 242Section 6.3expgrowth 41953
[Suppes] p. 22Theorem 2eq0 4277  eq0f 4274
[Suppes] p. 22Theorem 4eqss 3936  eqssd 3938  eqssi 3937
[Suppes] p. 23Theorem 5ss0 4332  ss0b 4331
[Suppes] p. 23Theorem 6sstr 3929  sstrALT2 42455
[Suppes] p. 23Theorem 7pssirr 4035
[Suppes] p. 23Theorem 8pssn2lp 4036
[Suppes] p. 23Theorem 9psstr 4039
[Suppes] p. 23Theorem 10pssss 4030
[Suppes] p. 25Theorem 12elin 3903  elun 4083
[Suppes] p. 26Theorem 15inidm 4152
[Suppes] p. 26Theorem 16in0 4325
[Suppes] p. 27Theorem 23unidm 4086
[Suppes] p. 27Theorem 24un0 4324
[Suppes] p. 27Theorem 25ssun1 4106
[Suppes] p. 27Theorem 26ssequn1 4114
[Suppes] p. 27Theorem 27unss 4118
[Suppes] p. 27Theorem 28indir 4209
[Suppes] p. 27Theorem 29undir 4210
[Suppes] p. 28Theorem 32difid 4304
[Suppes] p. 29Theorem 33difin 4195
[Suppes] p. 29Theorem 34indif 4203
[Suppes] p. 29Theorem 35undif1 4409
[Suppes] p. 29Theorem 36difun2 4414
[Suppes] p. 29Theorem 37difin0 4407
[Suppes] p. 29Theorem 38disjdif 4405
[Suppes] p. 29Theorem 39difundi 4213
[Suppes] p. 29Theorem 40difindi 4215
[Suppes] p. 30Theorem 41nalset 5237
[Suppes] p. 39Theorem 61uniss 4847
[Suppes] p. 39Theorem 65uniop 5429
[Suppes] p. 41Theorem 70intsn 4917
[Suppes] p. 42Theorem 71intpr 4913  intprg 4912
[Suppes] p. 42Theorem 73op1stb 5386
[Suppes] p. 42Theorem 78intun 4911
[Suppes] p. 44Definition 15(a)dfiun2 4963  dfiun2g 4960
[Suppes] p. 44Definition 15(b)dfiin2 4964
[Suppes] p. 47Theorem 86elpw 4537  elpw2 5269  elpw2g 5268  elpwg 4536  elpwgdedVD 42537
[Suppes] p. 47Theorem 87pwid 4557
[Suppes] p. 47Theorem 89pw0 4745
[Suppes] p. 48Theorem 90pwpw0 4746
[Suppes] p. 52Theorem 101xpss12 5604
[Suppes] p. 52Theorem 102xpindi 5742  xpindir 5743
[Suppes] p. 52Theorem 103xpundi 5655  xpundir 5656
[Suppes] p. 54Theorem 105elirrv 9355
[Suppes] p. 58Theorem 2relss 5692
[Suppes] p. 59Theorem 4eldm 5809  eldm2 5810  eldm2g 5808  eldmg 5807
[Suppes] p. 59Definition 3df-dm 5599
[Suppes] p. 60Theorem 6dmin 5820
[Suppes] p. 60Theorem 8rnun 6049
[Suppes] p. 60Theorem 9rnin 6050
[Suppes] p. 60Definition 4dfrn2 5797
[Suppes] p. 61Theorem 11brcnv 5791  brcnvg 5788
[Suppes] p. 62Equation 5elcnv 5785  elcnv2 5786
[Suppes] p. 62Theorem 12relcnv 6012
[Suppes] p. 62Theorem 15cnvin 6048
[Suppes] p. 62Theorem 16cnvun 6046
[Suppes] p. 63Definitiondftrrels2 36689
[Suppes] p. 63Theorem 20co02 6164
[Suppes] p. 63Theorem 21dmcoss 5880
[Suppes] p. 63Definition 7df-co 5598
[Suppes] p. 64Theorem 26cnvco 5794
[Suppes] p. 64Theorem 27coass 6169
[Suppes] p. 65Theorem 31resundi 5905
[Suppes] p. 65Theorem 34elima 5974  elima2 5975  elima3 5976  elimag 5973
[Suppes] p. 65Theorem 35imaundi 6053
[Suppes] p. 66Theorem 40dminss 6056
[Suppes] p. 66Theorem 41imainss 6057
[Suppes] p. 67Exercise 11cnvxp 6060
[Suppes] p. 81Definition 34dfec2 8501
[Suppes] p. 82Theorem 72elec 8542  elecALTV 36405  elecg 8541
[Suppes] p. 82Theorem 73eqvrelth 36724  erth 8547  erth2 8548
[Suppes] p. 83Theorem 74eqvreldisj 36727  erdisj 8550
[Suppes] p. 89Theorem 96map0b 8671
[Suppes] p. 89Theorem 97map0 8675  map0g 8672
[Suppes] p. 89Theorem 98mapsn 8676  mapsnd 8674
[Suppes] p. 89Theorem 99mapss 8677
[Suppes] p. 91Definition 12(ii)alephsuc 9824
[Suppes] p. 91Definition 12(iii)alephlim 9823
[Suppes] p. 92Theorem 1enref 8773  enrefg 8772
[Suppes] p. 92Theorem 2ensym 8789  ensymb 8788  ensymi 8790
[Suppes] p. 92Theorem 3entr 8792
[Suppes] p. 92Theorem 4unen 8836
[Suppes] p. 94Theorem 15endom 8767
[Suppes] p. 94Theorem 16ssdomg 8786
[Suppes] p. 94Theorem 17domtr 8793
[Suppes] p. 95Theorem 18sbth 8880
[Suppes] p. 97Theorem 23canth2 8917  canth2g 8918
[Suppes] p. 97Definition 3brsdom2 8884  df-sdom 8736  dfsdom2 8883
[Suppes] p. 97Theorem 21(i)sdomirr 8901
[Suppes] p. 97Theorem 22(i)domnsym 8886
[Suppes] p. 97Theorem 21(ii)sdomnsym 8885
[Suppes] p. 97Theorem 22(ii)domsdomtr 8899
[Suppes] p. 97Theorem 22(iv)brdom2 8770
[Suppes] p. 97Theorem 21(iii)sdomtr 8902
[Suppes] p. 97Theorem 22(iii)sdomdomtr 8897
[Suppes] p. 98Exercise 4fundmen 8821  fundmeng 8822
[Suppes] p. 98Exercise 6xpdom3 8857
[Suppes] p. 98Exercise 11sdomentr 8898
[Suppes] p. 104Theorem 37fofi 9105
[Suppes] p. 104Theorem 38pwfi 8961
[Suppes] p. 105Theorem 40pwfi 8961
[Suppes] p. 111Axiom for cardinal numberscarden 10307
[Suppes] p. 130Definition 3df-tr 5192
[Suppes] p. 132Theorem 9ssonuni 7630
[Suppes] p. 134Definition 6df-suc 6272
[Suppes] p. 136Theorem Schema 22findes 7749  finds 7745  finds1 7748  finds2 7747
[Suppes] p. 151Theorem 42isfinite 9410  isfinite2 9072  isfiniteg 9074  unbnn 9070
[Suppes] p. 162Definition 5df-ltnq 10674  df-ltpq 10666
[Suppes] p. 197Theorem Schema 4tfindes 7709  tfinds 7706  tfinds2 7710
[Suppes] p. 209Theorem 18oaord1 8382
[Suppes] p. 209Theorem 21oaword2 8384
[Suppes] p. 211Theorem 25oaass 8392
[Suppes] p. 225Definition 8iscard2 9734
[Suppes] p. 227Theorem 56ondomon 10319
[Suppes] p. 228Theorem 59harcard 9736
[Suppes] p. 228Definition 12(i)aleph0 9822
[Suppes] p. 228Theorem Schema 61onintss 6316
[Suppes] p. 228Theorem Schema 62onminesb 7643  onminsb 7644
[Suppes] p. 229Theorem 64alephval2 10328
[Suppes] p. 229Theorem 65alephcard 9826
[Suppes] p. 229Theorem 66alephord2i 9833
[Suppes] p. 229Theorem 67alephnbtwn 9827
[Suppes] p. 229Definition 12df-aleph 9698
[Suppes] p. 242Theorem 6weth 10251
[Suppes] p. 242Theorem 8entric 10313
[Suppes] p. 242Theorem 9carden 10307
[TakeutiZaring] p. 8Axiom 1ax-ext 2709
[TakeutiZaring] p. 13Definition 4.5df-cleq 2730
[TakeutiZaring] p. 13Proposition 4.6df-clel 2816
[TakeutiZaring] p. 13Proposition 4.9cvjust 2732
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2761
[TakeutiZaring] p. 14Definition 4.16df-oprab 7279
[TakeutiZaring] p. 14Proposition 4.14ru 3715
[TakeutiZaring] p. 15Axiom 2zfpair 5344
[TakeutiZaring] p. 15Exercise 1elpr 4584  elpr2 4586  elpr2g 4585  elprg 4582
[TakeutiZaring] p. 15Exercise 2elsn 4576  elsn2 4600  elsn2g 4599  elsng 4575  velsn 4577
[TakeutiZaring] p. 15Exercise 3elop 5382
[TakeutiZaring] p. 15Exercise 4sneq 4571  sneqr 4771
[TakeutiZaring] p. 15Definition 5.1dfpr2 4580  dfsn2 4574  dfsn2ALT 4581
[TakeutiZaring] p. 16Axiom 3uniex 7594
[TakeutiZaring] p. 16Exercise 6opth 5391
[TakeutiZaring] p. 16Exercise 7opex 5379
[TakeutiZaring] p. 16Exercise 8rext 5364
[TakeutiZaring] p. 16Corollary 5.8unex 7596  unexg 7599
[TakeutiZaring] p. 16Definition 5.3dftp2 4625
[TakeutiZaring] p. 16Definition 5.5df-uni 4840
[TakeutiZaring] p. 16Definition 5.6df-in 3894  df-un 3892
[TakeutiZaring] p. 16Proposition 5.7unipr 4857  uniprg 4856
[TakeutiZaring] p. 17Axiom 4vpwex 5300
[TakeutiZaring] p. 17Exercise 1eltp 4624
[TakeutiZaring] p. 17Exercise 5elsuc 6335  elsucg 6333  sstr2 3928
[TakeutiZaring] p. 17Exercise 6uncom 4087
[TakeutiZaring] p. 17Exercise 7incom 4135
[TakeutiZaring] p. 17Exercise 8unass 4100
[TakeutiZaring] p. 17Exercise 9inass 4153
[TakeutiZaring] p. 17Exercise 10indi 4207
[TakeutiZaring] p. 17Exercise 11undi 4208
[TakeutiZaring] p. 17Definition 5.9df-pss 3906  dfss2 3907
[TakeutiZaring] p. 17Definition 5.10df-pw 4535
[TakeutiZaring] p. 18Exercise 7unss2 4115
[TakeutiZaring] p. 18Exercise 9df-ss 3904  sseqin2 4149
[TakeutiZaring] p. 18Exercise 10ssid 3943
[TakeutiZaring] p. 18Exercise 12inss1 4162  inss2 4163
[TakeutiZaring] p. 18Exercise 13nss 3983
[TakeutiZaring] p. 18Exercise 15unieq 4850
[TakeutiZaring] p. 18Exercise 18sspwb 5365  sspwimp 42538  sspwimpALT 42545  sspwimpALT2 42548  sspwimpcf 42540
[TakeutiZaring] p. 18Exercise 19pweqb 5372
[TakeutiZaring] p. 19Axiom 5ax-rep 5209
[TakeutiZaring] p. 20Definitiondf-rab 3073
[TakeutiZaring] p. 20Corollary 5.160ex 5231
[TakeutiZaring] p. 20Definition 5.12df-dif 3890
[TakeutiZaring] p. 20Definition 5.14dfnul2 4259
[TakeutiZaring] p. 20Proposition 5.15difid 4304
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4280  n0f 4276  neq0 4279  neq0f 4275
[TakeutiZaring] p. 21Axiom 6zfreg 9354
[TakeutiZaring] p. 21Axiom 6'zfregs 9490
[TakeutiZaring] p. 21Theorem 5.22setind 9492
[TakeutiZaring] p. 21Definition 5.20df-v 3434
[TakeutiZaring] p. 21Proposition 5.21vprc 5239
[TakeutiZaring] p. 22Exercise 10ss 4330
[TakeutiZaring] p. 22Exercise 3ssex 5245  ssexg 5247
[TakeutiZaring] p. 22Exercise 4inex1 5241
[TakeutiZaring] p. 22Exercise 5ruv 9361
[TakeutiZaring] p. 22Exercise 6elirr 9356
[TakeutiZaring] p. 22Exercise 7ssdif0 4297
[TakeutiZaring] p. 22Exercise 11difdif 4065
[TakeutiZaring] p. 22Exercise 13undif3 4224  undif3VD 42502
[TakeutiZaring] p. 22Exercise 14difss 4066
[TakeutiZaring] p. 22Exercise 15sscon 4073
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3069
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3070
[TakeutiZaring] p. 23Proposition 6.2xpex 7603  xpexg 7600
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5596
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6505
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6680  fun11 6508
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6446  svrelfun 6506
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5796
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5798
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5601
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5602
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5598
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6097  dfrel2 6092
[TakeutiZaring] p. 25Exercise 3xpss 5605
[TakeutiZaring] p. 25Exercise 5relun 5721
[TakeutiZaring] p. 25Exercise 6reluni 5728
[TakeutiZaring] p. 25Exercise 9inxp 5741
[TakeutiZaring] p. 25Exercise 12relres 5920
[TakeutiZaring] p. 25Exercise 13opelres 5897  opelresi 5899
[TakeutiZaring] p. 25Exercise 14dmres 5913
[TakeutiZaring] p. 25Exercise 15resss 5916
[TakeutiZaring] p. 25Exercise 17resabs1 5921
[TakeutiZaring] p. 25Exercise 18funres 6476
[TakeutiZaring] p. 25Exercise 24relco 6148
[TakeutiZaring] p. 25Exercise 29funco 6474
[TakeutiZaring] p. 25Exercise 30f1co 6682
[TakeutiZaring] p. 26Definition 6.10eu2 2611
[TakeutiZaring] p. 26Definition 6.11conventions 28764  df-fv 6441  fv3 6792
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7772  cnvexg 7771
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7758  dmexg 7750
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7759  rnexg 7751
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 42072
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7767
[TakeutiZaring] p. 27Corollary 6.13fvex 6787
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 44666  tz6.12-1-afv2 44733  tz6.12-1 6796  tz6.12-afv 44665  tz6.12-afv2 44732  tz6.12 6797  tz6.12c-afv2 44734  tz6.12c 6799
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 44729  tz6.12-2 6762  tz6.12i-afv2 44735  tz6.12i 6800
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6436
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6437
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6439  wfo 6431
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6438  wf1 6430
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6440  wf1o 6432
[TakeutiZaring] p. 28Exercise 4eqfnfv 6909  eqfnfv2 6910  eqfnfv2f 6913
[TakeutiZaring] p. 28Exercise 5fvco 6866
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7093
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7091
[TakeutiZaring] p. 29Exercise 9funimaex 6521  funimaexg 6520
[TakeutiZaring] p. 29Definition 6.18df-br 5075
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5504
[TakeutiZaring] p. 30Definition 6.21dffr2 5553  dffr3 6007  eliniseg 6002  iniseg 6005
[TakeutiZaring] p. 30Definition 6.22df-eprel 5495
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5567  fr3nr 7622  frirr 5566
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5544
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7624
[TakeutiZaring] p. 31Exercise 1frss 5556
[TakeutiZaring] p. 31Exercise 4wess 5576
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6250  tz6.26i 6252  wefrc 5583  wereu2 5586
[TakeutiZaring] p. 32Theorem 6.27wfi 6253  wfii 6255
[TakeutiZaring] p. 32Definition 6.28df-isom 6442
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7200
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7201
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7207
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7208
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7209
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7213
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7220
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7222
[TakeutiZaring] p. 35Notationwtr 5191
[TakeutiZaring] p. 35Theorem 7.2trelpss 42073  tz7.2 5573
[TakeutiZaring] p. 35Definition 7.1dftr3 5195
[TakeutiZaring] p. 36Proposition 7.4ordwe 6279
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6287
[TakeutiZaring] p. 36Proposition 7.6ordelord 6288  ordelordALT 42157  ordelordALTVD 42487
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6294  ordelssne 6293
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6292
[TakeutiZaring] p. 37Proposition 7.9ordin 6296
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7632
[TakeutiZaring] p. 38Corollary 7.15ordsson 7633
[TakeutiZaring] p. 38Definition 7.11df-on 6270
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6298
[TakeutiZaring] p. 38Proposition 7.12onfrALT 42169  ordon 7627
[TakeutiZaring] p. 38Proposition 7.13onprc 7628
[TakeutiZaring] p. 39Theorem 7.17tfi 7700
[TakeutiZaring] p. 40Exercise 3ontr2 6313
[TakeutiZaring] p. 40Exercise 7dftr2 5193
[TakeutiZaring] p. 40Exercise 9onssmin 7642
[TakeutiZaring] p. 40Exercise 11unon 7678
[TakeutiZaring] p. 40Exercise 12ordun 6367
[TakeutiZaring] p. 40Exercise 14ordequn 6366
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7629
[TakeutiZaring] p. 40Proposition 7.20elssuni 4871
[TakeutiZaring] p. 41Definition 7.22df-suc 6272
[TakeutiZaring] p. 41Proposition 7.23sssucid 6343  sucidg 6344
[TakeutiZaring] p. 41Proposition 7.24suceloni 7659
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6357  ordnbtwn 6356
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7675
[TakeutiZaring] p. 42Exercise 1df-lim 6271
[TakeutiZaring] p. 42Exercise 4omssnlim 7727
[TakeutiZaring] p. 42Exercise 7ssnlim 7732
[TakeutiZaring] p. 42Exercise 8onsucssi 7688  ordelsuc 7667
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7669
[TakeutiZaring] p. 42Definition 7.27nlimon 7698
[TakeutiZaring] p. 42Definition 7.28dfom2 7714
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7735
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7737
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7738
[TakeutiZaring] p. 43Remarkomon 7724
[TakeutiZaring] p. 43Axiom 7inf3 9393  omex 9401
[TakeutiZaring] p. 43Theorem 7.32ordom 7722
[TakeutiZaring] p. 43Corollary 7.31find 7743
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7739
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7740
[TakeutiZaring] p. 44Exercise 1limomss 7717
[TakeutiZaring] p. 44Exercise 2int0 4893
[TakeutiZaring] p. 44Exercise 3trintss 5208
[TakeutiZaring] p. 44Exercise 4intss1 4894
[TakeutiZaring] p. 44Exercise 5intex 5261
[TakeutiZaring] p. 44Exercise 6oninton 7645
[TakeutiZaring] p. 44Exercise 11ordintdif 6315
[TakeutiZaring] p. 44Definition 7.35df-int 4880
[TakeutiZaring] p. 44Proposition 7.34noinfep 9418
[TakeutiZaring] p. 45Exercise 4onint 7640
[TakeutiZaring] p. 47Lemma 1tfrlem1 8207
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8228
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8229
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8230
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8237  tz7.44-2 8238  tz7.44-3 8239
[TakeutiZaring] p. 50Exercise 1smogt 8198
[TakeutiZaring] p. 50Exercise 3smoiso 8193
[TakeutiZaring] p. 50Definition 7.46df-smo 8177
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8276  tz7.49c 8277
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8274
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8273
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8275
[TakeutiZaring] p. 53Proposition 7.532eu5 2657
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9767
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9768
[TakeutiZaring] p. 56Definition 8.1oalim 8362  oasuc 8354
[TakeutiZaring] p. 57Remarktfindsg 7707
[TakeutiZaring] p. 57Proposition 8.2oacl 8365
[TakeutiZaring] p. 57Proposition 8.3oa0 8346  oa0r 8368
[TakeutiZaring] p. 57Proposition 8.16omcl 8366
[TakeutiZaring] p. 58Corollary 8.5oacan 8379
[TakeutiZaring] p. 58Proposition 8.4nnaord 8450  nnaordi 8449  oaord 8378  oaordi 8377
[TakeutiZaring] p. 59Proposition 8.6iunss2 4979  uniss2 4874
[TakeutiZaring] p. 59Proposition 8.7oawordri 8381
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8386  oawordex 8388
[TakeutiZaring] p. 59Proposition 8.9nnacl 8442
[TakeutiZaring] p. 59Proposition 8.10oaabs 8478
[TakeutiZaring] p. 60Remarkoancom 9409
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8391
[TakeutiZaring] p. 62Exercise 1nnarcl 8447
[TakeutiZaring] p. 62Exercise 5oaword1 8383
[TakeutiZaring] p. 62Definition 8.15om0x 8349  omlim 8363  omsuc 8356
[TakeutiZaring] p. 62Definition 8.15(a)om0 8347
[TakeutiZaring] p. 63Proposition 8.17nnecl 8444  nnmcl 8443
[TakeutiZaring] p. 63Proposition 8.19nnmord 8463  nnmordi 8462  omord 8399  omordi 8397
[TakeutiZaring] p. 63Proposition 8.20omcan 8400
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8467  omwordri 8403
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8369
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8373  om1r 8374
[TakeutiZaring] p. 64Proposition 8.22om00 8406
[TakeutiZaring] p. 64Proposition 8.23omordlim 8408
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8409
[TakeutiZaring] p. 64Proposition 8.25odi 8410
[TakeutiZaring] p. 65Theorem 8.26omass 8411
[TakeutiZaring] p. 67Definition 8.30nnesuc 8439  oe0 8352  oelim 8364  oesuc 8357  onesuc 8360
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8350
[TakeutiZaring] p. 67Proposition 8.32oen0 8417
[TakeutiZaring] p. 67Proposition 8.33oeordi 8418
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8351
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8376
[TakeutiZaring] p. 68Corollary 8.34oeord 8419
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8425
[TakeutiZaring] p. 68Proposition 8.35oewordri 8423
[TakeutiZaring] p. 68Proposition 8.37oeworde 8424
[TakeutiZaring] p. 69Proposition 8.41oeoa 8428
[TakeutiZaring] p. 70Proposition 8.42oeoe 8430
[TakeutiZaring] p. 73Theorem 9.1trcl 9486  tz9.1 9487
[TakeutiZaring] p. 76Definition 9.9df-r1 9522  r10 9526  r1lim 9530  r1limg 9529  r1suc 9528  r1sucg 9527
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9538  r1ord2 9539  r1ordg 9536
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9548
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9573  tz9.13 9549  tz9.13g 9550
[TakeutiZaring] p. 79Definition 9.14df-rank 9523  rankval 9574  rankvalb 9555  rankvalg 9575
[TakeutiZaring] p. 79Proposition 9.16rankel 9597  rankelb 9582
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9611  rankval3 9598  rankval3b 9584
[TakeutiZaring] p. 79Proposition 9.18rankonid 9587
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9553
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9592  rankr1c 9579  rankr1g 9590
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9593
[TakeutiZaring] p. 80Exercise 1rankss 9607  rankssb 9606
[TakeutiZaring] p. 80Exercise 2unbndrank 9600
[TakeutiZaring] p. 80Proposition 9.19bndrank 9599
[TakeutiZaring] p. 83Axiom of Choiceac4 10231  dfac3 9877
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9786  numth 10228  numth2 10227
[TakeutiZaring] p. 85Definition 10.4cardval 10302
[TakeutiZaring] p. 85Proposition 10.5cardid 10303  cardid2 9711
[TakeutiZaring] p. 85Proposition 10.9oncard 9718
[TakeutiZaring] p. 85Proposition 10.10carden 10307
[TakeutiZaring] p. 85Proposition 10.11cardidm 9717
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9702
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9723
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9715
[TakeutiZaring] p. 87Proposition 10.15pwen 8937
[TakeutiZaring] p. 88Exercise 1en0 8803
[TakeutiZaring] p. 88Exercise 7infensuc 8942
[TakeutiZaring] p. 89Exercise 10omxpen 8861
[TakeutiZaring] p. 90Corollary 10.23cardnn 9721
[TakeutiZaring] p. 90Definition 10.27alephiso 9854
[TakeutiZaring] p. 90Proposition 10.20nneneq 8992
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9011
[TakeutiZaring] p. 90Proposition 10.26alephprc 9855
[TakeutiZaring] p. 90Corollary 10.21(1)php5 8997
[TakeutiZaring] p. 91Exercise 2alephle 9844
[TakeutiZaring] p. 91Exercise 3aleph0 9822
[TakeutiZaring] p. 91Exercise 4cardlim 9730
[TakeutiZaring] p. 91Exercise 7infpss 9973
[TakeutiZaring] p. 91Exercise 8infcntss 9088
[TakeutiZaring] p. 91Definition 10.29df-fin 8737  isfi 8764
[TakeutiZaring] p. 92Proposition 10.32onfin 9013
[TakeutiZaring] p. 92Proposition 10.34imadomg 10290
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8854
[TakeutiZaring] p. 93Proposition 10.35fodomb 10282
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 9941  unxpdom 9030
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9732  cardsdomelir 9731
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9032
[TakeutiZaring] p. 94Proposition 10.39infxpen 9770
[TakeutiZaring] p. 95Definition 10.42df-map 8617
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10318  infxpidm2 9773
[TakeutiZaring] p. 95Proposition 10.41infdju 9964  infxp 9971
[TakeutiZaring] p. 96Proposition 10.44pw2en 8866  pw2f1o 8864
[TakeutiZaring] p. 96Proposition 10.45mapxpen 8930
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10243
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10238  ac6s5 10247
[TakeutiZaring] p. 98Theorem 10.47unidom 10299
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10300  uniimadomf 10301
[TakeutiZaring] p. 100Definition 11.1cfcof 10030
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10025
[TakeutiZaring] p. 102Exercise 1cfle 10010
[TakeutiZaring] p. 102Exercise 2cf0 10007
[TakeutiZaring] p. 102Exercise 3cfsuc 10013
[TakeutiZaring] p. 102Exercise 4cfom 10020
[TakeutiZaring] p. 102Proposition 11.9coftr 10029
[TakeutiZaring] p. 103Theorem 11.15alephreg 10338
[TakeutiZaring] p. 103Proposition 11.11cardcf 10008
[TakeutiZaring] p. 103Proposition 11.13alephsing 10032
[TakeutiZaring] p. 104Corollary 11.17cardinfima 9853
[TakeutiZaring] p. 104Proposition 11.16carduniima 9852
[TakeutiZaring] p. 104Proposition 11.18alephfp 9864  alephfp2 9865
[TakeutiZaring] p. 106Theorem 11.20gchina 10455
[TakeutiZaring] p. 106Theorem 11.21mappwen 9868
[TakeutiZaring] p. 107Theorem 11.26konigth 10325
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10339
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10340
[Tarski] p. 67Axiom B5ax-c5 36897
[Tarski] p. 67Scheme B5sp 2176
[Tarski] p. 68Lemma 6avril1 28827  equid 2015
[Tarski] p. 69Lemma 7equcomi 2020
[Tarski] p. 70Lemma 14spim 2387  spime 2389  spimew 1975
[Tarski] p. 70Lemma 16ax-12 2171  ax-c15 36903  ax12i 1970
[Tarski] p. 70Lemmas 16 and 17sb6 2088
[Tarski] p. 75Axiom B7ax6v 1972
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1913  ax5ALT 36921
[Tarski], p. 75Scheme B8 of system S2ax-7 2011  ax-8 2108  ax-9 2116
[Tarski1999] p. 178Axiom 4axtgsegcon 26825
[Tarski1999] p. 178Axiom 5axtg5seg 26826
[Tarski1999] p. 179Axiom 7axtgpasch 26828
[Tarski1999] p. 180Axiom 7.1axtgpasch 26828
[Tarski1999] p. 185Axiom 11axtgcont1 26829
[Truss] p. 114Theorem 5.18ruc 15952
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 35816
[Viaclovsky8] p. 3Proposition 7ismblfin 35818
[Weierstrass] p. 272Definitiondf-mdet 21734  mdetuni 21771
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 901
[WhiteheadRussell] p. 96Axiom *1.3olc 865
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 866
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 917
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 965
[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 35616
[WhiteheadRussell] p. 100Theorem *2.05frege5 41408  imim2 58  wl-luk-imim2 35611
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 44514  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 894
[WhiteheadRussell] p. 101Theorem *2.06barbara 2664  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 900
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 35614
[WhiteheadRussell] p. 101Theorem *2.11exmid 892
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 895
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 42547  wl-luk-notnotr 35615
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 41438  axfrege28 41437  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 864
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 922
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 35608
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 887
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 937
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 28765  pm2.27 42  wl-luk-pm2.27 35606
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 920
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 921
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 967
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 968
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 966
[WhiteheadRussell] p. 105Definition *2.33df-3or 1087
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 904
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 905
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 940
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 879
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 880
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 190
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 881
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 882
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 883
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 848
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 849
[WhiteheadRussell] p. 107Theorem *2.55orel1 886
[WhiteheadRussell] p. 107Theorem *2.56orel2 888
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 191
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 897
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 938
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 939
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 192
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 889  pm2.67 890
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 896
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 970
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 898
[WhiteheadRussell] p. 108Theorem *2.69looinv 202
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 971
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 972
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 931
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 929
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 969
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 973
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 930
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 989
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 470  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 990
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 991
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 992
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 993
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 472
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 460
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 403
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 800
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 449
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 450
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 483  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 485  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 762
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 763
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 805
[WhiteheadRussell] p. 113Fact)pm3.45 622
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 807
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 493
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 494
[WhiteheadRussell] p. 113Theorem *3.44jao 958  pm3.44 957
[WhiteheadRussell] p. 113Theorem *3.47anim12 806
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 474
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 961
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 260
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 354
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 804
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 830
[WhiteheadRussell] p. 117Theorem *4.21bicom 221
[WhiteheadRussell] p. 117Theorem *4.22biantr 803  bitr 802
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 564
[WhiteheadRussell] p. 117Theorem *4.25oridm 902  pm4.25 903
[WhiteheadRussell] p. 118Theorem *4.3ancom 461
[WhiteheadRussell] p. 118Theorem *4.4andi 1005
[WhiteheadRussell] p. 118Theorem *4.31orcom 867
[WhiteheadRussell] p. 118Theorem *4.32anass 469
[WhiteheadRussell] p. 118Theorem *4.33orass 919
[WhiteheadRussell] p. 118Theorem *4.36anbi1 632
[WhiteheadRussell] p. 118Theorem *4.37orbi1 915
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 635
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 974
[WhiteheadRussell] p. 118Definition *4.34df-3an 1088
[WhiteheadRussell] p. 119Theorem *4.41ordi 1003
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1051
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1020
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 994
[WhiteheadRussell] p. 119Theorem *4.45orabs 996  pm4.45 995  pm4.45im 825
[WhiteheadRussell] p. 120Theorem *4.5anor 980
[WhiteheadRussell] p. 120Theorem *4.6imor 850
[WhiteheadRussell] p. 120Theorem *4.7anclb 546
[WhiteheadRussell] p. 120Theorem *4.51ianor 979
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 982
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 983
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 984
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 985
[WhiteheadRussell] p. 120Theorem *4.56ioran 981  pm4.56 986
[WhiteheadRussell] p. 120Theorem *4.57oran 987  pm4.57 988
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 405
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 853
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 398
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 846
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 406
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 847
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 399
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 558  pm4.71d 562  pm4.71i 560  pm4.71r 559  pm4.71rd 563  pm4.71ri 561
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 947
[WhiteheadRussell] p. 121Theorem *4.73iba 528
[WhiteheadRussell] p. 121Theorem *4.74biorf 934
[WhiteheadRussell] p. 121Theorem *4.76jcab 518  pm4.76 519
[WhiteheadRussell] p. 121Theorem *4.77jaob 959  pm4.77 960
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 932
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1001
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 393
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 394
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1021
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1022
[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 451  pm4.87 840
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 821
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 942  pm5.11g 941
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 943
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 945
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 944
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1010
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1011
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1009
[WhiteheadRussell] p. 124Theorem *5.18nbbn 385  pm5.18 383
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 388
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 822
[WhiteheadRussell] p. 124Theorem *5.22xor 1012
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1047
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1048
[WhiteheadRussell] p. 124Theorem *5.25dfor2 899
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 573
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 390
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 362
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 999
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 951
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 828
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 574
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 833
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 823
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 831
[WhiteheadRussell] p. 125Theorem *5.41imdi 391  pm5.41 392
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 544
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 543
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1002
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1015
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 946
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 998
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1016
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1017
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1025
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 367
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 269
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1026
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 41976
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 41977
[WhiteheadRussell] p. 147Theorem *10.2219.26 1873
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 41978
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 41979
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 41980
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1896
[WhiteheadRussell] p. 151Theorem *10.301albitr 41981
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 41982
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 41983
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 41984
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 41985
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 41987
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 41988
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 41989
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 41986
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2093
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 41992
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 41993
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2073
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2157
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1831
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1832
[WhiteheadRussell] p. 161Theorem *11.319.21vv 41994
[WhiteheadRussell] p. 162Theorem *11.322alim 41995
[WhiteheadRussell] p. 162Theorem *11.332albi 41996
[WhiteheadRussell] p. 162Theorem *11.342exim 41997
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 41999
[WhiteheadRussell] p. 162Theorem *11.3412exbi 41998
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1890
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 42001
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 42002
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 42000
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1830
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 42003
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 42004
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1848
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 42005
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2344
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1863
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 42010
[WhiteheadRussell] p. 165Theorem *11.56aaanv 42006
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 42007
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 42008
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 42009
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 42014
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 42011
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 42012
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 42013
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 42015
[WhiteheadRussell] p. 175Definition *14.02df-eu 2569
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 42025  pm13.13b 42026
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 42027
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3025
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3026
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3597
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 42033
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 42034
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 42028
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 42172  pm13.193 42029
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 42030
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 42031
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 42032
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 42039
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 42038
[WhiteheadRussell] p. 184Definition *14.01iotasbc 42037
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3784
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 42040  pm14.122b 42041  pm14.122c 42042
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 42043  pm14.123b 42044  pm14.123c 42045
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 42047
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 42046
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 42048
[WhiteheadRussell] p. 190Theorem *14.22iota4 6414
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 42049
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6415
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 42050
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 42052
[WhiteheadRussell] p. 192Theorem *14.26eupick 2635  eupickbi 2638  sbaniota 42053
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 42051
[WhiteheadRussell] p. 192Theorem *14.271eubi 2584
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 42055
[WhiteheadRussell] p. 235Definition *30.01conventions 28764  df-fv 6441
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9759  pm54.43lem 9758
[Young] p. 141Definition of operator orderingleop2 30486
[Young] p. 142Example 12.2(i)0leop 30492  idleop 30493
[vandenDries] p. 42Lemma 61irrapx1 40650
[vandenDries] p. 43Theorem 62pellex 40657  pellexlem1 40651

This page was last updated on 21-Dec-2024.
Copyright terms: Public domain