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 17042
[Adamek] p. 21Condition 3.1(b)df-cat 17042
[Adamek] p. 22Example 3.3(1)df-setc 17448
[Adamek] p. 24Example 3.3(4.c)0cat 17063
[Adamek] p. 24Example 3.3(4.d)df-prstc 45803  prsthinc 45799
[Adamek] p. 24Example 3.3(4.e)df-mndtc 45819  df-mndtc 45819
[Adamek] p. 25Definition 3.5df-oppc 17086
[Adamek] p. 28Remark 3.9oppciso 17156
[Adamek] p. 28Remark 3.12invf1o 17144  invisoinvl 17165
[Adamek] p. 28Example 3.13idinv 17164  idiso 17163
[Adamek] p. 28Corollary 3.11inveq 17149
[Adamek] p. 28Definition 3.8df-inv 17123  df-iso 17124  dfiso2 17147
[Adamek] p. 28Proposition 3.10sectcan 17130
[Adamek] p. 29Remark 3.16cicer 17181
[Adamek] p. 29Definition 3.15cic 17174  df-cic 17171
[Adamek] p. 29Definition 3.17df-func 17233
[Adamek] p. 29Proposition 3.14(1)invinv 17145
[Adamek] p. 29Proposition 3.14(2)invco 17146  isoco 17152
[Adamek] p. 30Remark 3.19df-func 17233
[Adamek] p. 30Example 3.20(1)idfucl 17256
[Adamek] p. 32Proposition 3.21funciso 17249
[Adamek] p. 33Example 3.26(2)df-thinc 45780  prsthinc 45799
[Adamek] p. 33Example 3.26(3)df-mndtc 45819
[Adamek] p. 33Proposition 3.23cofucl 17263
[Adamek] p. 34Remark 3.28(2)catciso 17483
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 17533
[Adamek] p. 34Definition 3.27(2)df-fth 17280
[Adamek] p. 34Definition 3.27(3)df-full 17279
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 17533
[Adamek] p. 35Corollary 3.32ffthiso 17304
[Adamek] p. 35Proposition 3.30(c)cofth 17310
[Adamek] p. 35Proposition 3.30(d)cofull 17309
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 17518
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 17518
[Adamek] p. 39Definition 3.41funcoppc 17250
[Adamek] p. 39Definition 3.44.df-catc 17471
[Adamek] p. 39Proposition 3.43(c)fthoppc 17298
[Adamek] p. 39Proposition 3.43(d)fulloppc 17297
[Adamek] p. 40Remark 3.48catccat 17480
[Adamek] p. 40Definition 3.47df-catc 17471
[Adamek] p. 48Example 4.3(1.a)0subcat 17213
[Adamek] p. 48Example 4.3(1.b)catsubcat 17214
[Adamek] p. 48Definition 4.1(2)fullsubc 17225
[Adamek] p. 48Definition 4.1(a)df-subc 17187
[Adamek] p. 49Remark 4.4(2)ressffth 17313
[Adamek] p. 83Definition 6.1df-nat 17318
[Adamek] p. 87Remark 6.14(a)fuccocl 17339
[Adamek] p. 87Remark 6.14(b)fucass 17343
[Adamek] p. 87Definition 6.15df-fuc 17319
[Adamek] p. 88Remark 6.16fuccat 17345
[Adamek] p. 101Definition 7.1df-inito 17356
[Adamek] p. 101Example 7.2 (6)irinitoringc 45161
[Adamek] p. 102Definition 7.4df-termo 17357
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17384
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17388
[Adamek] p. 103Definition 7.7df-zeroo 17358
[Adamek] p. 103Example 7.9 (3)nzerooringczr 45164
[Adamek] p. 103Proposition 7.6termoeu1w 17391
[Adamek] p. 106Definition 7.19df-sect 17122
[Adamek] p. 185Section 10.67updjud 9436
[Adamek] p. 478Item Rngdf-ringc 45097
[AhoHopUll] p. 2Section 1.1df-bigo 45428
[AhoHopUll] p. 12Section 1.3df-blen 45450
[AhoHopUll] p. 318Section 9.1df-concat 14012  df-pfx 14122  df-substr 14092  df-word 13956  lencl 13974  wrd0 13980
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 23461  df-nmoo 28680
[AkhiezerGlazman] p. 64Theoremhmopidmch 30088  hmopidmchi 30086
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 30136  pjcmul2i 30137
[AkhiezerGlazman] p. 72Theoremcnvunop 29853  unoplin 29855
[AkhiezerGlazman] p. 72Equation 2unopadj 29854  unopadj2 29873
[AkhiezerGlazman] p. 73Theoremelunop2 29948  lnopunii 29947
[AkhiezerGlazman] p. 80Proposition 1adjlnop 30021
[Alling] p. 184Axiom Bbdayfo 33521
[Alling] p. 184Axiom Osltso 33520
[Alling] p. 184Axiom SDnodense 33536
[Alling] p. 185Lemma 0nocvxmin 33614
[Alling] p. 185Theoremconway 33634
[Alling] p. 185Axiom FEnoeta 33587
[Alling] p. 186Theorem 4slerec 33654
[Apostol] p. 18Theorem I.1addcan 10902  addcan2d 10922  addcan2i 10912  addcand 10921  addcani 10911
[Apostol] p. 18Theorem I.2negeu 10954
[Apostol] p. 18Theorem I.3negsub 11012  negsubd 11081  negsubi 11042
[Apostol] p. 18Theorem I.4negneg 11014  negnegd 11066  negnegi 11034
[Apostol] p. 18Theorem I.5subdi 11151  subdid 11174  subdii 11167  subdir 11152  subdird 11175  subdiri 11168
[Apostol] p. 18Theorem I.6mul01 10897  mul01d 10917  mul01i 10908  mul02 10896  mul02d 10916  mul02i 10907
[Apostol] p. 18Theorem I.7mulcan 11355  mulcan2d 11352  mulcand 11351  mulcani 11357
[Apostol] p. 18Theorem I.8receu 11363  xreceu 30771
[Apostol] p. 18Theorem I.9divrec 11392  divrecd 11497  divreci 11463  divreczi 11456
[Apostol] p. 18Theorem I.10recrec 11415  recreci 11450
[Apostol] p. 18Theorem I.11mul0or 11358  mul0ord 11368  mul0ori 11366
[Apostol] p. 18Theorem I.12mul2neg 11157  mul2negd 11173  mul2negi 11166  mulneg1 11154  mulneg1d 11171  mulneg1i 11164
[Apostol] p. 18Theorem I.13divadddiv 11433  divadddivd 11538  divadddivi 11480
[Apostol] p. 18Theorem I.14divmuldiv 11418  divmuldivd 11535  divmuldivi 11478  rdivmuldivd 31065
[Apostol] p. 18Theorem I.15divdivdiv 11419  divdivdivd 11541  divdivdivi 11481
[Apostol] p. 20Axiom 7rpaddcl 12494  rpaddcld 12529  rpmulcl 12495  rpmulcld 12530
[Apostol] p. 20Axiom 8rpneg 12504
[Apostol] p. 20Axiom 90nrp 12507
[Apostol] p. 20Theorem I.17lttri 10844
[Apostol] p. 20Theorem I.18ltadd1d 11311  ltadd1dd 11329  ltadd1i 11272
[Apostol] p. 20Theorem I.19ltmul1 11568  ltmul1a 11567  ltmul1i 11636  ltmul1ii 11646  ltmul2 11569  ltmul2d 12556  ltmul2dd 12570  ltmul2i 11639
[Apostol] p. 20Theorem I.20msqgt0 11238  msqgt0d 11285  msqgt0i 11255
[Apostol] p. 20Theorem I.210lt1 11240
[Apostol] p. 20Theorem I.23lt0neg1 11224  lt0neg1d 11287  ltneg 11218  ltnegd 11296  ltnegi 11262
[Apostol] p. 20Theorem I.25lt2add 11203  lt2addd 11341  lt2addi 11280
[Apostol] p. 20Definition of positive numbersdf-rp 12473
[Apostol] p. 21Exercise 4recgt0 11564  recgt0d 11652  recgt0i 11623  recgt0ii 11624
[Apostol] p. 22Definition of integersdf-z 12063
[Apostol] p. 22Definition of positive integersdfnn3 11730
[Apostol] p. 22Definition of rationalsdf-q 12431
[Apostol] p. 24Theorem I.26supeu 8991
[Apostol] p. 26Theorem I.28nnunb 11972
[Apostol] p. 26Theorem I.29arch 11973
[Apostol] p. 28Exercise 2btwnz 12165
[Apostol] p. 28Exercise 3nnrecl 11974
[Apostol] p. 28Exercise 4rebtwnz 12429
[Apostol] p. 28Exercise 5zbtwnre 12428
[Apostol] p. 28Exercise 6qbtwnre 12675
[Apostol] p. 28Exercise 10(a)zeneo 15784  zneo 12146  zneoALTV 44655
[Apostol] p. 29Theorem I.35cxpsqrtth 25472  msqsqrtd 14890  resqrtth 14705  sqrtth 14814  sqrtthi 14820  sqsqrtd 14889
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 11719
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12395
[Apostol] p. 361Remarkcrreczi 13681
[Apostol] p. 363Remarkabsgt0i 14849
[Apostol] p. 363Exampleabssubd 14903  abssubi 14853
[ApostolNT] p. 7Remarkfmtno0 44526  fmtno1 44527  fmtno2 44536  fmtno3 44537  fmtno4 44538  fmtno5fac 44568  fmtnofz04prm 44563
[ApostolNT] p. 7Definitiondf-fmtno 44514
[ApostolNT] p. 8Definitiondf-ppi 25837
[ApostolNT] p. 14Definitiondf-dvds 15700
[ApostolNT] p. 14Theorem 1.1(a)iddvds 15715
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 15739
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 15734
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 15728
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 15730
[ApostolNT] p. 14Theorem 1.1(f)1dvds 15716
[ApostolNT] p. 14Theorem 1.1(g)dvds0 15717
[ApostolNT] p. 14Theorem 1.1(h)0dvds 15722
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 15756
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 15758
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 15760
[ApostolNT] p. 15Definitiondf-gcd 15938  dfgcd2 15990
[ApostolNT] p. 16Definitionisprm2 16123
[ApostolNT] p. 16Theorem 1.5coprmdvds 16094
[ApostolNT] p. 16Theorem 1.7prminf 16351
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 15956
[ApostolNT] p. 16Theorem 1.4(b)gcdass 15991
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 15993
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 15971
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 15963
[ApostolNT] p. 17Theorem 1.8coprm 16152
[ApostolNT] p. 17Theorem 1.9euclemma 16154
[ApostolNT] p. 17Theorem 1.101arith2 16364
[ApostolNT] p. 18Theorem 1.13prmrec 16358
[ApostolNT] p. 19Theorem 1.14divalg 15848
[ApostolNT] p. 20Theorem 1.15eucalg 16028
[ApostolNT] p. 24Definitiondf-mu 25838
[ApostolNT] p. 25Definitiondf-phi 16203
[ApostolNT] p. 25Theorem 2.1musum 25928
[ApostolNT] p. 26Theorem 2.2phisum 16227
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16213
[ApostolNT] p. 28Theorem 2.5(c)phimul 16217
[ApostolNT] p. 32Definitiondf-vma 25835
[ApostolNT] p. 32Theorem 2.9muinv 25930
[ApostolNT] p. 32Theorem 2.10vmasum 25952
[ApostolNT] p. 38Remarkdf-sgm 25839
[ApostolNT] p. 38Definitiondf-sgm 25839
[ApostolNT] p. 75Definitiondf-chp 25836  df-cht 25834
[ApostolNT] p. 104Definitioncongr 16105
[ApostolNT] p. 106Remarkdvdsval3 15703
[ApostolNT] p. 106Definitionmoddvds 15710
[ApostolNT] p. 107Example 2mod2eq0even 15791
[ApostolNT] p. 107Example 3mod2eq1n2dvds 15792
[ApostolNT] p. 107Example 4zmod1congr 13347
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13384
[ApostolNT] p. 107Theorem 5.2(c)modexp 13691
[ApostolNT] p. 108Theorem 5.3modmulconst 15733
[ApostolNT] p. 109Theorem 5.4cncongr1 16108
[ApostolNT] p. 109Theorem 5.6gcdmodi 16510
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16110
[ApostolNT] p. 113Theorem 5.17eulerth 16220
[ApostolNT] p. 113Theorem 5.18vfermltl 16238
[ApostolNT] p. 114Theorem 5.19fermltl 16221
[ApostolNT] p. 116Theorem 5.24wilthimp 25809
[ApostolNT] p. 179Definitiondf-lgs 26031  lgsprme0 26075
[ApostolNT] p. 180Example 11lgs 26076
[ApostolNT] p. 180Theorem 9.2lgsvalmod 26052
[ApostolNT] p. 180Theorem 9.3lgsdirprm 26067
[ApostolNT] p. 181Theorem 9.4m1lgs 26124
[ApostolNT] p. 181Theorem 9.52lgs 26143  2lgsoddprm 26152
[ApostolNT] p. 182Theorem 9.6gausslemma2d 26110
[ApostolNT] p. 185Theorem 9.8lgsquad 26119
[ApostolNT] p. 188Definitiondf-lgs 26031  lgs1 26077
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 26068
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 26070
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 26078
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 26079
[Baer] p. 40Property (b)mapdord 39275
[Baer] p. 40Property (c)mapd11 39276
[Baer] p. 40Property (e)mapdin 39299  mapdlsm 39301
[Baer] p. 40Property (f)mapd0 39302
[Baer] p. 40Definition of projectivitydf-mapd 39262  mapd1o 39285
[Baer] p. 41Property (g)mapdat 39304
[Baer] p. 44Part (1)mapdpg 39343
[Baer] p. 45Part (2)hdmap1eq 39438  mapdheq 39365  mapdheq2 39366  mapdheq2biN 39367
[Baer] p. 45Part (3)baerlem3 39350
[Baer] p. 46Part (4)mapdheq4 39369  mapdheq4lem 39368
[Baer] p. 46Part (5)baerlem5a 39351  baerlem5abmN 39355  baerlem5amN 39353  baerlem5b 39352  baerlem5bmN 39354
[Baer] p. 47Part (6)hdmap1l6 39458  hdmap1l6a 39446  hdmap1l6e 39451  hdmap1l6f 39452  hdmap1l6g 39453  hdmap1l6lem1 39444  hdmap1l6lem2 39445  mapdh6N 39384  mapdh6aN 39372  mapdh6eN 39377  mapdh6fN 39378  mapdh6gN 39379  mapdh6lem1N 39370  mapdh6lem2N 39371
[Baer] p. 48Part 9hdmapval 39465
[Baer] p. 48Part 10hdmap10 39477
[Baer] p. 48Part 11hdmapadd 39480
[Baer] p. 48Part (6)hdmap1l6h 39454  mapdh6hN 39380
[Baer] p. 48Part (7)mapdh75cN 39390  mapdh75d 39391  mapdh75e 39389  mapdh75fN 39392  mapdh7cN 39386  mapdh7dN 39387  mapdh7eN 39385  mapdh7fN 39388
[Baer] p. 48Part (8)mapdh8 39425  mapdh8a 39412  mapdh8aa 39413  mapdh8ab 39414  mapdh8ac 39415  mapdh8ad 39416  mapdh8b 39417  mapdh8c 39418  mapdh8d 39420  mapdh8d0N 39419  mapdh8e 39421  mapdh8g 39422  mapdh8i 39423  mapdh8j 39424
[Baer] p. 48Part (9)mapdh9a 39426
[Baer] p. 48Equation 10mapdhvmap 39406
[Baer] p. 49Part 12hdmap11 39485  hdmapeq0 39481  hdmapf1oN 39502  hdmapneg 39483  hdmaprnN 39501  hdmaprnlem1N 39486  hdmaprnlem3N 39487  hdmaprnlem3uN 39488  hdmaprnlem4N 39490  hdmaprnlem6N 39491  hdmaprnlem7N 39492  hdmaprnlem8N 39493  hdmaprnlem9N 39494  hdmapsub 39484
[Baer] p. 49Part 14hdmap14lem1 39505  hdmap14lem10 39514  hdmap14lem1a 39503  hdmap14lem2N 39506  hdmap14lem2a 39504  hdmap14lem3 39507  hdmap14lem8 39512  hdmap14lem9 39513
[Baer] p. 50Part 14hdmap14lem11 39515  hdmap14lem12 39516  hdmap14lem13 39517  hdmap14lem14 39518  hdmap14lem15 39519  hgmapval 39524
[Baer] p. 50Part 15hgmapadd 39531  hgmapmul 39532  hgmaprnlem2N 39534  hgmapvs 39528
[Baer] p. 50Part 16hgmaprnN 39538
[Baer] p. 110Lemma 1hdmapip0com 39554
[Baer] p. 110Line 27hdmapinvlem1 39555
[Baer] p. 110Line 28hdmapinvlem2 39556
[Baer] p. 110Line 30hdmapinvlem3 39557
[Baer] p. 110Part 1.2hdmapglem5 39559  hgmapvv 39563
[Baer] p. 110Proposition 1hdmapinvlem4 39558
[Baer] p. 111Line 10hgmapvvlem1 39560
[Baer] p. 111Line 15hdmapg 39567  hdmapglem7 39566
[Bauer], p. 483Theorem 1.22irrexpq 25473  2irrexpqALT 25538
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2570
[BellMachover] p. 460Notationdf-mo 2540
[BellMachover] p. 460Definitionmo3 2564
[BellMachover] p. 461Axiom Extax-ext 2710
[BellMachover] p. 462Theorem 1.1axextmo 2714
[BellMachover] p. 463Axiom Repaxrep5 5160
[BellMachover] p. 463Scheme Sepax-sep 5167
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 34858  bm1.3ii 5170
[BellMachover] p. 466Problemaxpow2 5234
[BellMachover] p. 466Axiom Powaxpow3 5235
[BellMachover] p. 466Axiom Unionaxun2 7481
[BellMachover] p. 468Definitiondf-ord 6175
[BellMachover] p. 469Theorem 2.2(i)ordirr 6190
[BellMachover] p. 469Theorem 2.2(iii)onelon 6197
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6192
[BellMachover] p. 471Definition of Ndf-om 7600
[BellMachover] p. 471Problem 2.5(ii)uniordint 7540
[BellMachover] p. 471Definition of Limdf-lim 6177
[BellMachover] p. 472Axiom Infzfinf2 9178
[BellMachover] p. 473Theorem 2.8limom 7614
[BellMachover] p. 477Equation 3.1df-r1 9266
[BellMachover] p. 478Definitionrankval2 9320
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9284  r1ord3g 9281
[BellMachover] p. 480Axiom Regzfreg 9132
[BellMachover] p. 488Axiom ACac5 9977  dfac4 9622
[BellMachover] p. 490Definition of alephalephval3 9610
[BeltramettiCassinelli] p. 98Remarkatlatmstc 36956
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 30288
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 30330  chirredi 30329
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 30318
[Beran] p. 3Definition of joinsshjval3 29289
[Beran] p. 39Theorem 2.3(i)cmcm2 29551  cmcm2i 29528  cmcm2ii 29533  cmt2N 36887
[Beran] p. 40Theorem 2.3(iii)lecm 29552  lecmi 29537  lecmii 29538
[Beran] p. 45Theorem 3.4cmcmlem 29526
[Beran] p. 49Theorem 4.2cm2j 29555  cm2ji 29560  cm2mi 29561
[Beran] p. 95Definitiondf-sh 29142  issh2 29144
[Beran] p. 95Lemma 3.1(S5)his5 29021
[Beran] p. 95Lemma 3.1(S6)his6 29034
[Beran] p. 95Lemma 3.1(S7)his7 29025
[Beran] p. 95Lemma 3.2(S8)ho01i 29763
[Beran] p. 95Lemma 3.2(S9)hoeq1 29765
[Beran] p. 95Lemma 3.2(S10)ho02i 29764
[Beran] p. 95Lemma 3.2(S11)hoeq2 29766
[Beran] p. 95Postulate (S1)ax-his1 29017  his1i 29035
[Beran] p. 95Postulate (S2)ax-his2 29018
[Beran] p. 95Postulate (S3)ax-his3 29019
[Beran] p. 95Postulate (S4)ax-his4 29020
[Beran] p. 96Definition of normdf-hnorm 28903  dfhnorm2 29057  normval 29059
[Beran] p. 96Definition for Cauchy sequencehcau 29119
[Beran] p. 96Definition of Cauchy sequencedf-hcau 28908
[Beran] p. 96Definition of complete subspaceisch3 29176
[Beran] p. 96Definition of convergedf-hlim 28907  hlimi 29123
[Beran] p. 97Theorem 3.3(i)norm-i-i 29068  norm-i 29064
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 29072  norm-ii 29073  normlem0 29044  normlem1 29045  normlem2 29046  normlem3 29047  normlem4 29048  normlem5 29049  normlem6 29050  normlem7 29051  normlem7tALT 29054
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 29074  norm-iii 29075
[Beran] p. 98Remark 3.4bcs 29116  bcsiALT 29114  bcsiHIL 29115
[Beran] p. 98Remark 3.4(B)normlem9at 29056  normpar 29090  normpari 29089
[Beran] p. 98Remark 3.4(C)normpyc 29081  normpyth 29080  normpythi 29077
[Beran] p. 99Remarklnfn0 29982  lnfn0i 29977  lnop0 29901  lnop0i 29905
[Beran] p. 99Theorem 3.5(i)nmcexi 29961  nmcfnex 29988  nmcfnexi 29986  nmcopex 29964  nmcopexi 29962
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 29989  nmcfnlbi 29987  nmcoplb 29965  nmcoplbi 29963
[Beran] p. 99Theorem 3.5(iii)lnfncon 29991  lnfnconi 29990  lnopcon 29970  lnopconi 29969
[Beran] p. 100Lemma 3.6normpar2i 29091
[Beran] p. 101Lemma 3.6norm3adifi 29088  norm3adifii 29083  norm3dif 29085  norm3difi 29082
[Beran] p. 102Theorem 3.7(i)chocunii 29236  pjhth 29328  pjhtheu 29329  pjpjhth 29360  pjpjhthi 29361  pjth 24191
[Beran] p. 102Theorem 3.7(ii)ococ 29341  ococi 29340
[Beran] p. 103Remark 3.8nlelchi 29996
[Beran] p. 104Theorem 3.9riesz3i 29997  riesz4 29999  riesz4i 29998
[Beran] p. 104Theorem 3.10cnlnadj 30014  cnlnadjeu 30013  cnlnadjeui 30012  cnlnadji 30011  cnlnadjlem1 30002  nmopadjlei 30023
[Beran] p. 106Theorem 3.11(i)adjeq0 30026
[Beran] p. 106Theorem 3.11(v)nmopadji 30025
[Beran] p. 106Theorem 3.11(ii)adjmul 30027
[Beran] p. 106Theorem 3.11(iv)adjadj 29871
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 30037  nmopcoadji 30036
[Beran] p. 106Theorem 3.11(iii)adjadd 30028
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 30038
[Beran] p. 106Theorem 3.11(viii)adjcoi 30035  pjadj2coi 30139  pjadjcoi 30096
[Beran] p. 107Definitiondf-ch 29156  isch2 29158
[Beran] p. 107Remark 3.12choccl 29241  isch3 29176  occl 29239  ocsh 29218  shoccl 29240  shocsh 29219
[Beran] p. 107Remark 3.12(B)ococin 29343
[Beran] p. 108Theorem 3.13chintcl 29267
[Beran] p. 109Property (i)pjadj2 30122  pjadj3 30123  pjadji 29620  pjadjii 29609
[Beran] p. 109Property (ii)pjidmco 30116  pjidmcoi 30112  pjidmi 29608
[Beran] p. 110Definition of projector orderingpjordi 30108
[Beran] p. 111Remarkho0val 29685  pjch1 29605
[Beran] p. 111Definitiondf-hfmul 29669  df-hfsum 29668  df-hodif 29667  df-homul 29666  df-hosum 29665
[Beran] p. 111Lemma 4.4(i)pjo 29606
[Beran] p. 111Lemma 4.4(ii)pjch 29629  pjchi 29367
[Beran] p. 111Lemma 4.4(iii)pjoc2 29374  pjoc2i 29373
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 29615
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 30100  pjssmii 29616
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 30099
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 30098
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 30103
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 30101  pjssge0ii 29617
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 30102  pjdifnormii 29618
[Bobzien] p. 116Statement T3stoic3 1783
[Bobzien] p. 117Statement T2stoic2a 1781
[Bobzien] p. 117Statement T4stoic4a 1784
[Bobzien] p. 117Conclusion the contradictorystoic1a 1779
[Bogachev] p. 16Definition 1.5df-oms 31829
[Bogachev] p. 17Lemma 1.5.4omssubadd 31837
[Bogachev] p. 17Example 1.5.2omsmon 31835
[Bogachev] p. 41Definition 1.11.2df-carsg 31839
[Bogachev] p. 42Theorem 1.11.4carsgsiga 31859
[Bogachev] p. 116Definition 2.3.1df-itgm 31890  df-sitm 31868
[Bogachev] p. 118Chapter 2.4.4df-itgm 31890
[Bogachev] p. 118Definition 2.4.1df-sitg 31867
[Bollobas] p. 1Section I.1df-edg 26993  isuhgrop 27015  isusgrop 27107  isuspgrop 27106
[Bollobas] p. 2Section I.1df-subgr 27210  uhgrspan1 27245  uhgrspansubgr 27233
[Bollobas] p. 3Definitionisomuspgr 44820
[Bollobas] p. 3Section I.1cusgrsize 27396  df-cusgr 27354  df-nbgr 27275  fusgrmaxsize 27406
[Bollobas] p. 4Definitiondf-upwlks 44830  df-wlks 27541
[Bollobas] p. 4Section I.1finsumvtxdg2size 27492  finsumvtxdgeven 27494  fusgr1th 27493  fusgrvtxdgonume 27496  vtxdgoddnumeven 27495
[Bollobas] p. 5Notationdf-pths 27657
[Bollobas] p. 5Definitiondf-crcts 27727  df-cycls 27728  df-trls 27634  df-wlkson 27542
[Bollobas] p. 7Section I.1df-ushgr 27004
[BourbakiAlg1] p. 1Definition 1df-clintop 44928  df-cllaw 44914  df-mgm 17968  df-mgm2 44947
[BourbakiAlg1] p. 4Definition 5df-assintop 44929  df-asslaw 44916  df-sgrp 18017  df-sgrp2 44949
[BourbakiAlg1] p. 7Definition 8df-cmgm2 44948  df-comlaw 44915
[BourbakiAlg1] p. 12Definition 2df-mnd 18028
[BourbakiAlg1] p. 92Definition 1df-ring 19418
[BourbakiAlg1] p. 93Section I.8.1df-rng0 44967
[BourbakiEns] p. Proposition 8fcof1 7054  fcofo 7055
[BourbakiTop1] p. Remarkxnegmnf 12686  xnegpnf 12685
[BourbakiTop1] p. Remark rexneg 12687
[BourbakiTop1] p. Remark 3ust0 22971  ustfilxp 22964
[BourbakiTop1] p. Axiom GT'tgpsubcn 22841
[BourbakiTop1] p. Criterionishmeo 22510
[BourbakiTop1] p. Example 1cstucnd 23036  iducn 23035  snfil 22615
[BourbakiTop1] p. Example 2neifil 22631
[BourbakiTop1] p. Theorem 1cnextcn 22818
[BourbakiTop1] p. Theorem 2ucnextcn 23056
[BourbakiTop1] p. Theorem 3df-hcmp 31479
[BourbakiTop1] p. Paragraph 3infil 22614
[BourbakiTop1] p. Definition 1df-ucn 23028  df-ust 22952  filintn0 22612  filn0 22613  istgp 22828  ucnprima 23034
[BourbakiTop1] p. Definition 2df-cfilu 23039
[BourbakiTop1] p. Definition 3df-cusp 23050  df-usp 23009  df-utop 22983  trust 22981
[BourbakiTop1] p. Definition 6df-pcmp 31378
[BourbakiTop1] p. Property V_issnei2 21867
[BourbakiTop1] p. Theorem 1(d)iscncl 22020
[BourbakiTop1] p. Condition F_Iustssel 22957
[BourbakiTop1] p. Condition U_Iustdiag 22960
[BourbakiTop1] p. Property V_iiinnei 21876
[BourbakiTop1] p. Property V_ivneiptopreu 21884  neissex 21878
[BourbakiTop1] p. Proposition 1neips 21864  neiss 21860  ucncn 23037  ustund 22973  ustuqtop 22998
[BourbakiTop1] p. Proposition 2cnpco 22018  neiptopreu 21884  utop2nei 23002  utop3cls 23003
[BourbakiTop1] p. Proposition 3fmucnd 23044  uspreg 23026  utopreg 23004
[BourbakiTop1] p. Proposition 4imasncld 22442  imasncls 22443  imasnopn 22441
[BourbakiTop1] p. Proposition 9cnpflf2 22751
[BourbakiTop1] p. Condition F_IIustincl 22959
[BourbakiTop1] p. Condition U_IIustinvel 22961
[BourbakiTop1] p. Property V_iiielnei 21862
[BourbakiTop1] p. Proposition 11cnextucn 23055
[BourbakiTop1] p. Condition F_IIbustbasel 22958
[BourbakiTop1] p. Condition U_IIIustexhalf 22962
[BourbakiTop1] p. Definition C'''df-cmp 22138
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 22597
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 21645
[BourbakiTop2] p. 195Definition 1df-ldlf 31375
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 43145
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 43147  stoweid 43146
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 43084  stoweidlem10 43093  stoweidlem14 43097  stoweidlem15 43098  stoweidlem35 43118  stoweidlem36 43119  stoweidlem37 43120  stoweidlem38 43121  stoweidlem40 43123  stoweidlem41 43124  stoweidlem43 43126  stoweidlem44 43127  stoweidlem46 43129  stoweidlem5 43088  stoweidlem50 43133  stoweidlem52 43135  stoweidlem53 43136  stoweidlem55 43138  stoweidlem56 43139
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 43106  stoweidlem24 43107  stoweidlem27 43110  stoweidlem28 43111  stoweidlem30 43113
[BrosowskiDeutsh] p. 91Proofstoweidlem34 43117  stoweidlem59 43142  stoweidlem60 43143
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 43128  stoweidlem49 43132  stoweidlem7 43090
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 43114  stoweidlem39 43122  stoweidlem42 43125  stoweidlem48 43131  stoweidlem51 43134  stoweidlem54 43137  stoweidlem57 43140  stoweidlem58 43141
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 43108
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 43100
[BrosowskiDeutsh] p. 92Proofstoweidlem11 43094  stoweidlem13 43096  stoweidlem26 43109  stoweidlem61 43144
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 43101
[Bruck] p. 1Section I.1df-clintop 44928  df-mgm 17968  df-mgm2 44947
[Bruck] p. 23Section II.1df-sgrp 18017  df-sgrp2 44949
[Bruck] p. 28Theorem 3.2dfgrp3 18316
[ChoquetDD] p. 2Definition of mappingdf-mpt 5111
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 28340
[Clemente] p. 10Definition I` `m,nnatded 28340
[Clemente] p. 11Definition E=>m,nnatded 28340
[Clemente] p. 11Definition I=>m,nnatded 28340
[Clemente] p. 11Definition E` `(1)natded 28340
[Clemente] p. 11Definition E` `(2)natded 28340
[Clemente] p. 12Definition E` `m,n,pnatded 28340
[Clemente] p. 12Definition I` `n(1)natded 28340
[Clemente] p. 12Definition I` `n(2)natded 28340
[Clemente] p. 13Definition I` `m,n,pnatded 28340
[Clemente] p. 14Proof 5.11natded 28340
[Clemente] p. 14Definition E` `nnatded 28340
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 28342  ex-natded5.2 28341
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 28345  ex-natded5.3 28344
[Clemente] p. 18Theorem 5.5ex-natded5.5 28347
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 28349  ex-natded5.7 28348
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 28351  ex-natded5.8 28350
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 28353  ex-natded5.13 28352
[Clemente] p. 32Definition I` `nnatded 28340
[Clemente] p. 32Definition E` `m,n,p,anatded 28340
[Clemente] p. 32Definition E` `n,tnatded 28340
[Clemente] p. 32Definition I` `n,tnatded 28340
[Clemente] p. 43Theorem 9.20ex-natded9.20 28354
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 28355
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 28357  ex-natded9.26 28356
[Cohen] p. 301Remarkrelogoprlem 25334
[Cohen] p. 301Property 2relogmul 25335  relogmuld 25368
[Cohen] p. 301Property 3relogdiv 25336  relogdivd 25369
[Cohen] p. 301Property 4relogexp 25339
[Cohen] p. 301Property 1alog1 25329
[Cohen] p. 301Property 1bloge 25330
[Cohen4] p. 348Observationrelogbcxpb 25525
[Cohen4] p. 349Propertyrelogbf 25529
[Cohen4] p. 352Definitionelogb 25508
[Cohen4] p. 361Property 2relogbmul 25515
[Cohen4] p. 361Property 3logbrec 25520  relogbdiv 25517
[Cohen4] p. 361Property 4relogbreexp 25513
[Cohen4] p. 361Property 6relogbexp 25518
[Cohen4] p. 361Property 1(a)logbid1 25506
[Cohen4] p. 361Property 1(b)logb1 25507
[Cohen4] p. 367Propertylogbchbase 25509
[Cohen4] p. 377Property 2logblt 25522
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 31822  sxbrsigalem4 31824
[Cohn] p. 81Section II.5acsdomd 17907  acsinfd 17906  acsinfdimd 17908  acsmap2d 17905  acsmapd 17904
[Cohn] p. 143Example 5.1.1sxbrsiga 31827
[Connell] p. 57Definitiondf-scmat 21242  df-scmatalt 45274
[Conway] p. 4Definitionslerec 33654
[Conway] p. 5Definitionaddsov 33764  df-adds 33757  df-negs 33758
[Conway] p. 7Theorem0slt1s 33664
[Conway] p. 16Theorem 0(i)ssltright 33692
[Conway] p. 16Theorem 0(ii)ssltleft 33691
[Conway] p. 16Theorem 0(iii)slerflex 33607
[Conway] p. 17Theorem 3addscom 33767  addscomd 33768  addsid1 33765  addsid1d 33766
[Conway] p. 17Definitiondf-0s 33659
[Conway] p. 18Definitiondf-1s 33660
[Conway] p. 29Remarkmadebday 33718  newbday 33720  oldbday 33719
[Conway] p. 29Definitiondf-made 33672  df-new 33674  df-old 33673
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13320
[Crawley] p. 1Definition of posetdf-poset 17672
[Crawley] p. 107Theorem 13.2hlsupr 37023
[Crawley] p. 110Theorem 13.3arglem1N 37827  dalaw 37523
[Crawley] p. 111Theorem 13.4hlathil 39598
[Crawley] p. 111Definition of set Wdf-watsN 37627
[Crawley] p. 111Definition of dilationdf-dilN 37743  df-ldil 37741  isldil 37747
[Crawley] p. 111Definition of translationdf-ltrn 37742  df-trnN 37744  isltrn 37756  ltrnu 37758
[Crawley] p. 112Lemma Acdlema1N 37428  cdlema2N 37429  exatleN 37041
[Crawley] p. 112Lemma B1cvrat 37113  cdlemb 37431  cdlemb2 37678  cdlemb3 38243  idltrn 37787  l1cvat 36692  lhpat 37680  lhpat2 37682  lshpat 36693  ltrnel 37776  ltrnmw 37788
[Crawley] p. 112Lemma Ccdlemc1 37828  cdlemc2 37829  ltrnnidn 37811  trlat 37806  trljat1 37803  trljat2 37804  trljat3 37805  trlne 37822  trlnidat 37810  trlnle 37823
[Crawley] p. 112Definition of automorphismdf-pautN 37628
[Crawley] p. 113Lemma Ccdlemc 37834  cdlemc3 37830  cdlemc4 37831
[Crawley] p. 113Lemma Dcdlemd 37844  cdlemd1 37835  cdlemd2 37836  cdlemd3 37837  cdlemd4 37838  cdlemd5 37839  cdlemd6 37840  cdlemd7 37841  cdlemd8 37842  cdlemd9 37843  cdleme31sde 38022  cdleme31se 38019  cdleme31se2 38020  cdleme31snd 38023  cdleme32a 38078  cdleme32b 38079  cdleme32c 38080  cdleme32d 38081  cdleme32e 38082  cdleme32f 38083  cdleme32fva 38074  cdleme32fva1 38075  cdleme32fvcl 38077  cdleme32le 38084  cdleme48fv 38136  cdleme4gfv 38144  cdleme50eq 38178  cdleme50f 38179  cdleme50f1 38180  cdleme50f1o 38183  cdleme50laut 38184  cdleme50ldil 38185  cdleme50lebi 38177  cdleme50rn 38182  cdleme50rnlem 38181  cdlemeg49le 38148  cdlemeg49lebilem 38176
[Crawley] p. 113Lemma Ecdleme 38197  cdleme00a 37846  cdleme01N 37858  cdleme02N 37859  cdleme0a 37848  cdleme0aa 37847  cdleme0b 37849  cdleme0c 37850  cdleme0cp 37851  cdleme0cq 37852  cdleme0dN 37853  cdleme0e 37854  cdleme0ex1N 37860  cdleme0ex2N 37861  cdleme0fN 37855  cdleme0gN 37856  cdleme0moN 37862  cdleme1 37864  cdleme10 37891  cdleme10tN 37895  cdleme11 37907  cdleme11a 37897  cdleme11c 37898  cdleme11dN 37899  cdleme11e 37900  cdleme11fN 37901  cdleme11g 37902  cdleme11h 37903  cdleme11j 37904  cdleme11k 37905  cdleme11l 37906  cdleme12 37908  cdleme13 37909  cdleme14 37910  cdleme15 37915  cdleme15a 37911  cdleme15b 37912  cdleme15c 37913  cdleme15d 37914  cdleme16 37922  cdleme16aN 37896  cdleme16b 37916  cdleme16c 37917  cdleme16d 37918  cdleme16e 37919  cdleme16f 37920  cdleme16g 37921  cdleme19a 37940  cdleme19b 37941  cdleme19c 37942  cdleme19d 37943  cdleme19e 37944  cdleme19f 37945  cdleme1b 37863  cdleme2 37865  cdleme20aN 37946  cdleme20bN 37947  cdleme20c 37948  cdleme20d 37949  cdleme20e 37950  cdleme20f 37951  cdleme20g 37952  cdleme20h 37953  cdleme20i 37954  cdleme20j 37955  cdleme20k 37956  cdleme20l 37959  cdleme20l1 37957  cdleme20l2 37958  cdleme20m 37960  cdleme20y 37939  cdleme20zN 37938  cdleme21 37974  cdleme21d 37967  cdleme21e 37968  cdleme22a 37977  cdleme22aa 37976  cdleme22b 37978  cdleme22cN 37979  cdleme22d 37980  cdleme22e 37981  cdleme22eALTN 37982  cdleme22f 37983  cdleme22f2 37984  cdleme22g 37985  cdleme23a 37986  cdleme23b 37987  cdleme23c 37988  cdleme26e 37996  cdleme26eALTN 37998  cdleme26ee 37997  cdleme26f 38000  cdleme26f2 38002  cdleme26f2ALTN 38001  cdleme26fALTN 37999  cdleme27N 38006  cdleme27a 38004  cdleme27cl 38003  cdleme28c 38009  cdleme3 37874  cdleme30a 38015  cdleme31fv 38027  cdleme31fv1 38028  cdleme31fv1s 38029  cdleme31fv2 38030  cdleme31id 38031  cdleme31sc 38021  cdleme31sdnN 38024  cdleme31sn 38017  cdleme31sn1 38018  cdleme31sn1c 38025  cdleme31sn2 38026  cdleme31so 38016  cdleme35a 38085  cdleme35b 38087  cdleme35c 38088  cdleme35d 38089  cdleme35e 38090  cdleme35f 38091  cdleme35fnpq 38086  cdleme35g 38092  cdleme35h 38093  cdleme35h2 38094  cdleme35sn2aw 38095  cdleme35sn3a 38096  cdleme36a 38097  cdleme36m 38098  cdleme37m 38099  cdleme38m 38100  cdleme38n 38101  cdleme39a 38102  cdleme39n 38103  cdleme3b 37866  cdleme3c 37867  cdleme3d 37868  cdleme3e 37869  cdleme3fN 37870  cdleme3fa 37873  cdleme3g 37871  cdleme3h 37872  cdleme4 37875  cdleme40m 38104  cdleme40n 38105  cdleme40v 38106  cdleme40w 38107  cdleme41fva11 38114  cdleme41sn3aw 38111  cdleme41sn4aw 38112  cdleme41snaw 38113  cdleme42a 38108  cdleme42b 38115  cdleme42c 38109  cdleme42d 38110  cdleme42e 38116  cdleme42f 38117  cdleme42g 38118  cdleme42h 38119  cdleme42i 38120  cdleme42k 38121  cdleme42ke 38122  cdleme42keg 38123  cdleme42mN 38124  cdleme42mgN 38125  cdleme43aN 38126  cdleme43bN 38127  cdleme43cN 38128  cdleme43dN 38129  cdleme5 37877  cdleme50ex 38196  cdleme50ltrn 38194  cdleme51finvN 38193  cdleme51finvfvN 38192  cdleme51finvtrN 38195  cdleme6 37878  cdleme7 37886  cdleme7a 37880  cdleme7aa 37879  cdleme7b 37881  cdleme7c 37882  cdleme7d 37883  cdleme7e 37884  cdleme7ga 37885  cdleme8 37887  cdleme8tN 37892  cdleme9 37890  cdleme9a 37888  cdleme9b 37889  cdleme9tN 37894  cdleme9taN 37893  cdlemeda 37935  cdlemedb 37934  cdlemednpq 37936  cdlemednuN 37937  cdlemefr27cl 38040  cdlemefr32fva1 38047  cdlemefr32fvaN 38046  cdlemefrs32fva 38037  cdlemefrs32fva1 38038  cdlemefs27cl 38050  cdlemefs32fva1 38060  cdlemefs32fvaN 38059  cdlemesner 37933  cdlemeulpq 37857
[Crawley] p. 114Lemma E4atex 37713  4atexlem7 37712  cdleme0nex 37927  cdleme17a 37923  cdleme17c 37925  cdleme17d 38135  cdleme17d1 37926  cdleme17d2 38132  cdleme18a 37928  cdleme18b 37929  cdleme18c 37930  cdleme18d 37932  cdleme4a 37876
[Crawley] p. 115Lemma Ecdleme21a 37962  cdleme21at 37965  cdleme21b 37963  cdleme21c 37964  cdleme21ct 37966  cdleme21f 37969  cdleme21g 37970  cdleme21h 37971  cdleme21i 37972  cdleme22gb 37931
[Crawley] p. 116Lemma Fcdlemf 38200  cdlemf1 38198  cdlemf2 38199
[Crawley] p. 116Lemma Gcdlemftr1 38204  cdlemg16 38294  cdlemg28 38341  cdlemg28a 38330  cdlemg28b 38340  cdlemg3a 38234  cdlemg42 38366  cdlemg43 38367  cdlemg44 38370  cdlemg44a 38368  cdlemg46 38372  cdlemg47 38373  cdlemg9 38271  ltrnco 38356  ltrncom 38375  tgrpabl 38388  trlco 38364
[Crawley] p. 116Definition of Gdf-tgrp 38380
[Crawley] p. 117Lemma Gcdlemg17 38314  cdlemg17b 38299
[Crawley] p. 117Definition of Edf-edring-rN 38393  df-edring 38394
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 38397
[Crawley] p. 118Remarktendopltp 38417
[Crawley] p. 118Lemma Hcdlemh 38454  cdlemh1 38452  cdlemh2 38453
[Crawley] p. 118Lemma Icdlemi 38457  cdlemi1 38455  cdlemi2 38456
[Crawley] p. 118Lemma Jcdlemj1 38458  cdlemj2 38459  cdlemj3 38460  tendocan 38461
[Crawley] p. 118Lemma Kcdlemk 38611  cdlemk1 38468  cdlemk10 38480  cdlemk11 38486  cdlemk11t 38583  cdlemk11ta 38566  cdlemk11tb 38568  cdlemk11tc 38582  cdlemk11u-2N 38526  cdlemk11u 38508  cdlemk12 38487  cdlemk12u-2N 38527  cdlemk12u 38509  cdlemk13-2N 38513  cdlemk13 38489  cdlemk14-2N 38515  cdlemk14 38491  cdlemk15-2N 38516  cdlemk15 38492  cdlemk16-2N 38517  cdlemk16 38494  cdlemk16a 38493  cdlemk17-2N 38518  cdlemk17 38495  cdlemk18-2N 38523  cdlemk18-3N 38537  cdlemk18 38505  cdlemk19-2N 38524  cdlemk19 38506  cdlemk19u 38607  cdlemk1u 38496  cdlemk2 38469  cdlemk20-2N 38529  cdlemk20 38511  cdlemk21-2N 38528  cdlemk21N 38510  cdlemk22-3 38538  cdlemk22 38530  cdlemk23-3 38539  cdlemk24-3 38540  cdlemk25-3 38541  cdlemk26-3 38543  cdlemk26b-3 38542  cdlemk27-3 38544  cdlemk28-3 38545  cdlemk29-3 38548  cdlemk3 38470  cdlemk30 38531  cdlemk31 38533  cdlemk32 38534  cdlemk33N 38546  cdlemk34 38547  cdlemk35 38549  cdlemk36 38550  cdlemk37 38551  cdlemk38 38552  cdlemk39 38553  cdlemk39u 38605  cdlemk4 38471  cdlemk41 38557  cdlemk42 38578  cdlemk42yN 38581  cdlemk43N 38600  cdlemk45 38584  cdlemk46 38585  cdlemk47 38586  cdlemk48 38587  cdlemk49 38588  cdlemk5 38473  cdlemk50 38589  cdlemk51 38590  cdlemk52 38591  cdlemk53 38594  cdlemk54 38595  cdlemk55 38598  cdlemk55u 38603  cdlemk56 38608  cdlemk5a 38472  cdlemk5auN 38497  cdlemk5u 38498  cdlemk6 38474  cdlemk6u 38499  cdlemk7 38485  cdlemk7u-2N 38525  cdlemk7u 38507  cdlemk8 38475  cdlemk9 38476  cdlemk9bN 38477  cdlemki 38478  cdlemkid 38573  cdlemkj-2N 38519  cdlemkj 38500  cdlemksat 38483  cdlemksel 38482  cdlemksv 38481  cdlemksv2 38484  cdlemkuat 38503  cdlemkuel-2N 38521  cdlemkuel-3 38535  cdlemkuel 38502  cdlemkuv-2N 38520  cdlemkuv2-2 38522  cdlemkuv2-3N 38536  cdlemkuv2 38504  cdlemkuvN 38501  cdlemkvcl 38479  cdlemky 38563  cdlemkyyN 38599  tendoex 38612
[Crawley] p. 120Remarkdva1dim 38622
[Crawley] p. 120Lemma Lcdleml1N 38613  cdleml2N 38614  cdleml3N 38615  cdleml4N 38616  cdleml5N 38617  cdleml6 38618  cdleml7 38619  cdleml8 38620  cdleml9 38621  dia1dim 38698
[Crawley] p. 120Lemma Mdia11N 38685  diaf11N 38686  dialss 38683  diaord 38684  dibf11N 38798  djajN 38774
[Crawley] p. 120Definition of isomorphism mapdiaval 38669
[Crawley] p. 121Lemma Mcdlemm10N 38755  dia2dimlem1 38701  dia2dimlem2 38702  dia2dimlem3 38703  dia2dimlem4 38704  dia2dimlem5 38705  diaf1oN 38767  diarnN 38766  dvheveccl 38749  dvhopN 38753
[Crawley] p. 121Lemma Ncdlemn 38849  cdlemn10 38843  cdlemn11 38848  cdlemn11a 38844  cdlemn11b 38845  cdlemn11c 38846  cdlemn11pre 38847  cdlemn2 38832  cdlemn2a 38833  cdlemn3 38834  cdlemn4 38835  cdlemn4a 38836  cdlemn5 38838  cdlemn5pre 38837  cdlemn6 38839  cdlemn7 38840  cdlemn8 38841  cdlemn9 38842  diclspsn 38831
[Crawley] p. 121Definition of phi(q)df-dic 38810
[Crawley] p. 122Lemma Ndih11 38902  dihf11 38904  dihjust 38854  dihjustlem 38853  dihord 38901  dihord1 38855  dihord10 38860  dihord11b 38859  dihord11c 38861  dihord2 38864  dihord2a 38856  dihord2b 38857  dihord2cN 38858  dihord2pre 38862  dihord2pre2 38863  dihordlem6 38850  dihordlem7 38851  dihordlem7b 38852
[Crawley] p. 122Definition of isomorphism mapdihffval 38867  dihfval 38868  dihval 38869
[Diestel] p. 3Section 1.1df-cusgr 27354  df-nbgr 27275
[Diestel] p. 4Section 1.1df-subgr 27210  uhgrspan1 27245  uhgrspansubgr 27233
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 27496  vtxdgoddnumeven 27495
[Diestel] p. 27Section 1.10df-ushgr 27004
[EGA] p. 80Notation 1.1.1rspecval 31386
[EGA] p. 80Proposition 1.1.2zartop 31398
[EGA] p. 80Proposition 1.1.2(i)zarcls0 31390  zarcls1 31391
[EGA] p. 81Corollary 1.1.8zart0 31401
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 31404
[EGA], p. 83Corollary 1.2.3rhmpreimacn 31407
[Eisenberg] p. 67Definition 5.3df-dif 3846
[Eisenberg] p. 82Definition 6.3dfom3 9183
[Eisenberg] p. 125Definition 8.21df-map 8439
[Eisenberg] p. 216Example 13.2(4)omenps 9191
[Eisenberg] p. 310Theorem 19.8cardprc 9482
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10055
[Enderton] p. 18Axiom of Empty Setaxnul 5173
[Enderton] p. 19Definitiondf-tp 4521
[Enderton] p. 26Exercise 5unissb 4830
[Enderton] p. 26Exercise 10pwel 5248
[Enderton] p. 28Exercise 7(b)pwun 5427
[Enderton] p. 30Theorem "Distributive laws"iinin1 4964  iinin2 4963  iinun2 4958  iunin1 4957  iunin1f 30471  iunin2 4956  uniin1 30465  uniin2 30466
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4962  iundif2 4959
[Enderton] p. 32Exercise 20unineq 4168
[Enderton] p. 33Exercise 23iinuni 4983
[Enderton] p. 33Exercise 25iununi 4984
[Enderton] p. 33Exercise 24(a)iinpw 4991
[Enderton] p. 33Exercise 24(b)iunpw 7512  iunpwss 4992
[Enderton] p. 36Definitionopthwiener 5371
[Enderton] p. 38Exercise 6(a)unipw 5309
[Enderton] p. 38Exercise 6(b)pwuni 4835
[Enderton] p. 41Lemma 3Dopeluu 5328  rnex 7643  rnexg 7635
[Enderton] p. 41Exercise 8dmuni 5757  rnuni 5981
[Enderton] p. 42Definition of a functiondffun7 6366  dffun8 6367
[Enderton] p. 43Definition of function valuefunfv2 6756
[Enderton] p. 43Definition of single-rootedfuncnv 6408
[Enderton] p. 44Definition (d)dfima2 5905  dfima3 5906
[Enderton] p. 47Theorem 3Hfvco2 6765
[Enderton] p. 49Axiom of Choice (first form)ac7 9973  ac7g 9974  df-ac 9616  dfac2 9631  dfac2a 9629  dfac2b 9630  dfac3 9621  dfac7 9632
[Enderton] p. 50Theorem 3K(a)imauni 7016
[Enderton] p. 52Definitiondf-map 8439
[Enderton] p. 53Exercise 21coass 6098
[Enderton] p. 53Exercise 27dmco 6087
[Enderton] p. 53Exercise 14(a)funin 6415
[Enderton] p. 53Exercise 22(a)imass2 5939
[Enderton] p. 54Remarkixpf 8530  ixpssmap 8542
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8508
[Enderton] p. 55Axiom of Choice (second form)ac9 9983  ac9s 9993
[Enderton] p. 56Theorem 3Meqvrelref 36346  erref 8340
[Enderton] p. 57Lemma 3Neqvrelthi 36349  erthi 8371
[Enderton] p. 57Definitiondf-ec 8322
[Enderton] p. 58Definitiondf-qs 8326
[Enderton] p. 61Exercise 35df-ec 8322
[Enderton] p. 65Exercise 56(a)dmun 5753
[Enderton] p. 68Definition of successordf-suc 6178
[Enderton] p. 71Definitiondf-tr 5137  dftr4 5141
[Enderton] p. 72Theorem 4Eunisuc 6248
[Enderton] p. 73Exercise 6unisuc 6248
[Enderton] p. 73Exercise 5(a)truni 5150
[Enderton] p. 73Exercise 5(b)trint 5152  trintALT 42039
[Enderton] p. 79Theorem 4I(A1)nna0 8261
[Enderton] p. 79Theorem 4I(A2)nnasuc 8263  onasuc 8184
[Enderton] p. 79Definition of operation valuedf-ov 7173
[Enderton] p. 80Theorem 4J(A1)nnm0 8262
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8264  onmsuc 8185
[Enderton] p. 81Theorem 4K(1)nnaass 8279
[Enderton] p. 81Theorem 4K(2)nna0r 8266  nnacom 8274
[Enderton] p. 81Theorem 4K(3)nndi 8280
[Enderton] p. 81Theorem 4K(4)nnmass 8281
[Enderton] p. 81Theorem 4K(5)nnmcom 8283
[Enderton] p. 82Exercise 16nnm0r 8267  nnmsucr 8282
[Enderton] p. 88Exercise 23nnaordex 8295
[Enderton] p. 129Definitiondf-en 8556
[Enderton] p. 132Theorem 6B(b)canth 7124
[Enderton] p. 133Exercise 1xpomen 9515
[Enderton] p. 133Exercise 2qnnen 15658
[Enderton] p. 134Theorem (Pigeonhole Principle)php 8751
[Enderton] p. 135Corollary 6Cphp3 8753
[Enderton] p. 136Corollary 6Enneneq 8750
[Enderton] p. 136Corollary 6D(a)pssinf 8807
[Enderton] p. 136Corollary 6D(b)ominf 8809
[Enderton] p. 137Lemma 6Fpssnn 8767
[Enderton] p. 138Corollary 6Gssfi 8772
[Enderton] p. 139Theorem 6H(c)mapen 8731
[Enderton] p. 142Theorem 6I(3)xpdjuen 9679
[Enderton] p. 142Theorem 6I(4)mapdjuen 9680
[Enderton] p. 143Theorem 6Jdju0en 9675  dju1en 9671
[Enderton] p. 144Exercise 13iunfi 8885  unifi 8886  unifi2 8887
[Enderton] p. 144Corollary 6Kundif2 4366  unfi 8771  unfi2 8861
[Enderton] p. 145Figure 38ffoss 7672
[Enderton] p. 145Definitiondf-dom 8557
[Enderton] p. 146Example 1domen 8568  domeng 8569
[Enderton] p. 146Example 3nndomo 8792  nnsdom 9190  nnsdomg 8851
[Enderton] p. 149Theorem 6L(a)djudom2 9683
[Enderton] p. 149Theorem 6L(c)mapdom1 8732  xpdom1 8665  xpdom1g 8663  xpdom2g 8662
[Enderton] p. 149Theorem 6L(d)mapdom2 8738
[Enderton] p. 151Theorem 6Mzorn 10007  zorng 10004
[Enderton] p. 151Theorem 6M(4)ac8 9992  dfac5 9628
[Enderton] p. 159Theorem 6Qunictb 10075
[Enderton] p. 164Exampleinfdif 9709
[Enderton] p. 168Definitiondf-po 5442
[Enderton] p. 192Theorem 7M(a)oneli 6280
[Enderton] p. 192Theorem 7M(b)ontr1 6218
[Enderton] p. 192Theorem 7M(c)onirri 6279
[Enderton] p. 193Corollary 7N(b)0elon 6225
[Enderton] p. 193Corollary 7N(c)onsuci 7572
[Enderton] p. 193Corollary 7N(d)ssonunii 7521
[Enderton] p. 194Remarkonprc 7518
[Enderton] p. 194Exercise 16suc11 6275
[Enderton] p. 197Definitiondf-card 9441
[Enderton] p. 197Theorem 7Pcarden 10051
[Enderton] p. 200Exercise 25tfis 7588
[Enderton] p. 202Lemma 7Tr1tr 9278
[Enderton] p. 202Definitiondf-r1 9266
[Enderton] p. 202Theorem 7Qr1val1 9288
[Enderton] p. 204Theorem 7V(b)rankval4 9369
[Enderton] p. 206Theorem 7X(b)en2lp 9142
[Enderton] p. 207Exercise 30rankpr 9359  rankprb 9353  rankpw 9345  rankpwi 9325  rankuniss 9368
[Enderton] p. 207Exercise 34opthreg 9154
[Enderton] p. 208Exercise 35suc11reg 9155
[Enderton] p. 212Definition of alephalephval3 9610
[Enderton] p. 213Theorem 8A(a)alephord2 9576
[Enderton] p. 213Theorem 8A(b)cardalephex 9590
[Enderton] p. 218Theorem Schema 8Eonfununi 8007
[Enderton] p. 222Definition of kardkarden 9397  kardex 9396
[Enderton] p. 238Theorem 8Roeoa 8254
[Enderton] p. 238Theorem 8Soeoe 8256
[Enderton] p. 240Exercise 25oarec 8219
[Enderton] p. 257Definition of cofinalitycflm 9750
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17016
[FaureFrolicher] p. 83Definition 4.1.1df-mri 16962
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 17903  mrieqv2d 17013  mrieqvd 17012
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17017
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17022  mreexexlem2d 17019
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 17909  mreexfidimd 17024
[Frege1879] p. 11Statementdf3or2 40922
[Frege1879] p. 12Statementdf3an2 40923  dfxor4 40920  dfxor5 40921
[Frege1879] p. 26Axiom 1ax-frege1 40944
[Frege1879] p. 26Axiom 2ax-frege2 40945
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 40949
[Frege1879] p. 31Proposition 4frege4 40953
[Frege1879] p. 32Proposition 5frege5 40954
[Frege1879] p. 33Proposition 6frege6 40960
[Frege1879] p. 34Proposition 7frege7 40962
[Frege1879] p. 35Axiom 8ax-frege8 40963  axfrege8 40961
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 35239
[Frege1879] p. 35Proposition 9frege9 40966
[Frege1879] p. 36Proposition 10frege10 40974
[Frege1879] p. 36Proposition 11frege11 40968
[Frege1879] p. 37Proposition 12frege12 40967
[Frege1879] p. 37Proposition 13frege13 40976
[Frege1879] p. 37Proposition 14frege14 40977
[Frege1879] p. 38Proposition 15frege15 40980
[Frege1879] p. 38Proposition 16frege16 40970
[Frege1879] p. 39Proposition 17frege17 40975
[Frege1879] p. 39Proposition 18frege18 40972
[Frege1879] p. 39Proposition 19frege19 40978
[Frege1879] p. 40Proposition 20frege20 40982
[Frege1879] p. 40Proposition 21frege21 40981
[Frege1879] p. 41Proposition 22frege22 40973
[Frege1879] p. 42Proposition 23frege23 40979
[Frege1879] p. 42Proposition 24frege24 40969
[Frege1879] p. 42Proposition 25frege25 40971  rp-frege25 40959
[Frege1879] p. 42Proposition 26frege26 40964
[Frege1879] p. 43Axiom 28ax-frege28 40984
[Frege1879] p. 43Proposition 27frege27 40965
[Frege1879] p. 43Proposition 28con3 156
[Frege1879] p. 43Proposition 29frege29 40985
[Frege1879] p. 44Axiom 31ax-frege31 40988  axfrege31 40987
[Frege1879] p. 44Proposition 30frege30 40986
[Frege1879] p. 44Proposition 31notnotr 132
[Frege1879] p. 44Proposition 32frege32 40989
[Frege1879] p. 44Proposition 33frege33 40990
[Frege1879] p. 45Proposition 34frege34 40991
[Frege1879] p. 45Proposition 35frege35 40992
[Frege1879] p. 45Proposition 36frege36 40993
[Frege1879] p. 46Proposition 37frege37 40994
[Frege1879] p. 46Proposition 38frege38 40995
[Frege1879] p. 46Proposition 39frege39 40996
[Frege1879] p. 46Proposition 40frege40 40997
[Frege1879] p. 47Axiom 41ax-frege41 40999  axfrege41 40998
[Frege1879] p. 47Proposition 41notnot 144
[Frege1879] p. 47Proposition 42frege42 41000
[Frege1879] p. 47Proposition 43frege43 41001
[Frege1879] p. 47Proposition 44frege44 41002
[Frege1879] p. 47Proposition 45frege45 41003
[Frege1879] p. 48Proposition 46frege46 41004
[Frege1879] p. 48Proposition 47frege47 41005
[Frege1879] p. 49Proposition 48frege48 41006
[Frege1879] p. 49Proposition 49frege49 41007
[Frege1879] p. 49Proposition 50frege50 41008
[Frege1879] p. 50Axiom 52ax-frege52a 41011  ax-frege52c 41042  frege52aid 41012  frege52b 41043
[Frege1879] p. 50Axiom 54ax-frege54a 41016  ax-frege54c 41046  frege54b 41047
[Frege1879] p. 50Proposition 51frege51 41009
[Frege1879] p. 50Proposition 52dfsbcq 3682
[Frege1879] p. 50Proposition 53frege53a 41014  frege53aid 41013  frege53b 41044  frege53c 41068
[Frege1879] p. 50Proposition 54biid 264  eqid 2738
[Frege1879] p. 50Proposition 55frege55a 41022  frege55aid 41019  frege55b 41051  frege55c 41072  frege55cor1a 41023  frege55lem2a 41021  frege55lem2b 41050  frege55lem2c 41071
[Frege1879] p. 50Proposition 56frege56a 41025  frege56aid 41024  frege56b 41052  frege56c 41073
[Frege1879] p. 51Axiom 58ax-frege58a 41029  ax-frege58b 41055  frege58bid 41056  frege58c 41075
[Frege1879] p. 51Proposition 57frege57a 41027  frege57aid 41026  frege57b 41053  frege57c 41074
[Frege1879] p. 51Proposition 58spsbc 3693
[Frege1879] p. 51Proposition 59frege59a 41031  frege59b 41058  frege59c 41076
[Frege1879] p. 52Proposition 60frege60a 41032  frege60b 41059  frege60c 41077
[Frege1879] p. 52Proposition 61frege61a 41033  frege61b 41060  frege61c 41078
[Frege1879] p. 52Proposition 62frege62a 41034  frege62b 41061  frege62c 41079
[Frege1879] p. 52Proposition 63frege63a 41035  frege63b 41062  frege63c 41080
[Frege1879] p. 53Proposition 64frege64a 41036  frege64b 41063  frege64c 41081
[Frege1879] p. 53Proposition 65frege65a 41037  frege65b 41064  frege65c 41082
[Frege1879] p. 54Proposition 66frege66a 41038  frege66b 41065  frege66c 41083
[Frege1879] p. 54Proposition 67frege67a 41039  frege67b 41066  frege67c 41084
[Frege1879] p. 54Proposition 68frege68a 41040  frege68b 41067  frege68c 41085
[Frege1879] p. 55Definition 69dffrege69 41086
[Frege1879] p. 58Proposition 70frege70 41087
[Frege1879] p. 59Proposition 71frege71 41088
[Frege1879] p. 59Proposition 72frege72 41089
[Frege1879] p. 59Proposition 73frege73 41090
[Frege1879] p. 60Definition 76dffrege76 41093
[Frege1879] p. 60Proposition 74frege74 41091
[Frege1879] p. 60Proposition 75frege75 41092
[Frege1879] p. 62Proposition 77frege77 41094  frege77d 40900
[Frege1879] p. 63Proposition 78frege78 41095
[Frege1879] p. 63Proposition 79frege79 41096
[Frege1879] p. 63Proposition 80frege80 41097
[Frege1879] p. 63Proposition 81frege81 41098  frege81d 40901
[Frege1879] p. 64Proposition 82frege82 41099
[Frege1879] p. 65Proposition 83frege83 41100  frege83d 40902
[Frege1879] p. 65Proposition 84frege84 41101
[Frege1879] p. 66Proposition 85frege85 41102
[Frege1879] p. 66Proposition 86frege86 41103
[Frege1879] p. 66Proposition 87frege87 41104  frege87d 40904
[Frege1879] p. 67Proposition 88frege88 41105
[Frege1879] p. 68Proposition 89frege89 41106
[Frege1879] p. 68Proposition 90frege90 41107
[Frege1879] p. 68Proposition 91frege91 41108  frege91d 40905
[Frege1879] p. 69Proposition 92frege92 41109
[Frege1879] p. 70Proposition 93frege93 41110
[Frege1879] p. 70Proposition 94frege94 41111
[Frege1879] p. 70Proposition 95frege95 41112
[Frege1879] p. 71Definition 99dffrege99 41116
[Frege1879] p. 71Proposition 96frege96 41113  frege96d 40903
[Frege1879] p. 71Proposition 97frege97 41114  frege97d 40906
[Frege1879] p. 71Proposition 98frege98 41115  frege98d 40907
[Frege1879] p. 72Proposition 100frege100 41117
[Frege1879] p. 72Proposition 101frege101 41118
[Frege1879] p. 72Proposition 102frege102 41119  frege102d 40908
[Frege1879] p. 73Proposition 103frege103 41120
[Frege1879] p. 73Proposition 104frege104 41121
[Frege1879] p. 73Proposition 105frege105 41122
[Frege1879] p. 73Proposition 106frege106 41123  frege106d 40909
[Frege1879] p. 74Proposition 107frege107 41124
[Frege1879] p. 74Proposition 108frege108 41125  frege108d 40910
[Frege1879] p. 74Proposition 109frege109 41126  frege109d 40911
[Frege1879] p. 75Proposition 110frege110 41127
[Frege1879] p. 75Proposition 111frege111 41128  frege111d 40913
[Frege1879] p. 76Proposition 112frege112 41129
[Frege1879] p. 76Proposition 113frege113 41130
[Frege1879] p. 76Proposition 114frege114 41131  frege114d 40912
[Frege1879] p. 77Definition 115dffrege115 41132
[Frege1879] p. 77Proposition 116frege116 41133
[Frege1879] p. 78Proposition 117frege117 41134
[Frege1879] p. 78Proposition 118frege118 41135
[Frege1879] p. 78Proposition 119frege119 41136
[Frege1879] p. 78Proposition 120frege120 41137
[Frege1879] p. 79Proposition 121frege121 41138
[Frege1879] p. 79Proposition 122frege122 41139  frege122d 40914
[Frege1879] p. 79Proposition 123frege123 41140
[Frege1879] p. 80Proposition 124frege124 41141  frege124d 40915
[Frege1879] p. 81Proposition 125frege125 41142
[Frege1879] p. 81Proposition 126frege126 41143  frege126d 40916
[Frege1879] p. 82Proposition 127frege127 41144
[Frege1879] p. 83Proposition 128frege128 41145
[Frege1879] p. 83Proposition 129frege129 41146  frege129d 40917
[Frege1879] p. 84Proposition 130frege130 41147
[Frege1879] p. 85Proposition 131frege131 41148  frege131d 40918
[Frege1879] p. 86Proposition 132frege132 41149
[Frege1879] p. 86Proposition 133frege133 41150  frege133d 40919
[Fremlin1] p. 13Definition 111G (b)df-salgen 43396
[Fremlin1] p. 13Definition 111G (d)borelmbl 43716
[Fremlin1] p. 13Proposition 111G (b)salgenss 43417
[Fremlin1] p. 14Definition 112Aismea 43531
[Fremlin1] p. 15Remark 112B (d)psmeasure 43551
[Fremlin1] p. 15Property 112C (a)meadjun 43542  meadjunre 43556
[Fremlin1] p. 15Property 112C (b)meassle 43543
[Fremlin1] p. 15Property 112C (c)meaunle 43544
[Fremlin1] p. 16Property 112C (d)iundjiun 43540  meaiunle 43549  meaiunlelem 43548
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 43561  meaiuninc2 43562  meaiuninc3 43565  meaiuninc3v 43564  meaiunincf 43563  meaiuninclem 43560
[Fremlin1] p. 16Proposition 112C (f)meaiininc 43567  meaiininc2 43568  meaiininclem 43566
[Fremlin1] p. 19Theorem 113Ccaragen0 43586  caragendifcl 43594  caratheodory 43608  omelesplit 43598
[Fremlin1] p. 19Definition 113Aisome 43574  isomennd 43611  isomenndlem 43610
[Fremlin1] p. 19Remark 113B (c)omeunle 43596
[Fremlin1] p. 19Definition 112Dfcaragencmpl 43615  voncmpl 43701
[Fremlin1] p. 19Definition 113A (ii)omessle 43578
[Fremlin1] p. 20Theorem 113Ccarageniuncl 43603  carageniuncllem1 43601  carageniuncllem2 43602  caragenuncl 43593  caragenuncllem 43592  caragenunicl 43604
[Fremlin1] p. 21Remark 113Dcaragenel2d 43612
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 43606  caratheodorylem2 43607
[Fremlin1] p. 21Exercise 113Xacaragencmpl 43615
[Fremlin1] p. 23Lemma 114Bhoidmv1le 43674  hoidmv1lelem1 43671  hoidmv1lelem2 43672  hoidmv1lelem3 43673
[Fremlin1] p. 25Definition 114Eisvonmbl 43718
[Fremlin1] p. 29Lemma 115Bhoidmv1le 43674  hoidmvle 43680  hoidmvlelem1 43675  hoidmvlelem2 43676  hoidmvlelem3 43677  hoidmvlelem4 43678  hoidmvlelem5 43679  hsphoidmvle2 43665  hsphoif 43656  hsphoival 43659
[Fremlin1] p. 29Definition 1135 (b)hoicvr 43628
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 43636
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 43663  hoidmvn0val 43664  hoidmvval 43657  hoidmvval0 43667  hoidmvval0b 43670
[Fremlin1] p. 30Lemma 115Bhoiprodp1 43668  hsphoidmvle 43666
[Fremlin1] p. 30Definition 115Cdf-ovoln 43617  df-voln 43619
[Fremlin1] p. 30Proposition 115D (a)dmovn 43684  ovn0 43646  ovn0lem 43645  ovnf 43643  ovnome 43653  ovnssle 43641  ovnsslelem 43640  ovnsupge0 43637
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 43683  ovnhoilem1 43681  ovnhoilem2 43682  vonhoi 43747
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 43700  hoidifhspf 43698  hoidifhspval 43688  hoidifhspval2 43695  hoidifhspval3 43699  hspmbl 43709  hspmbllem1 43706  hspmbllem2 43707  hspmbllem3 43708
[Fremlin1] p. 31Definition 115Evoncmpl 43701  vonmea 43654
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 43652  ovnsubadd2 43726  ovnsubadd2lem 43725  ovnsubaddlem1 43650  ovnsubaddlem2 43651
[Fremlin1] p. 32Proposition 115G (a)hoimbl 43711  hoimbl2 43745  hoimbllem 43710  hspdifhsp 43696  opnvonmbl 43714  opnvonmbllem2 43713
[Fremlin1] p. 32Proposition 115G (b)borelmbl 43716
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 43759  iccvonmbllem 43758  ioovonmbl 43757
[Fremlin1] p. 32Proposition 115G (d)vonicc 43765  vonicclem2 43764  vonioo 43762  vonioolem2 43761  vonn0icc 43768  vonn0icc2 43772  vonn0ioo 43767  vonn0ioo2 43770
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 43769  snvonmbl 43766  vonct 43773  vonsn 43771
[Fremlin1] p. 35Lemma 121Asubsalsal 43440
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 43439  subsaliuncllem 43438
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 43800  salpreimalegt 43786  salpreimaltle 43801
[Fremlin1] p. 35Proposition 121B (i)issmf 43803  issmff 43809  issmflem 43802
[Fremlin1] p. 35Proposition 121B (ii)issmfle 43820  issmflelem 43819  smfpreimale 43829
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 43831  issmfgtlem 43830
[Fremlin1] p. 36Definition 121Cdf-smblfn 43776  issmf 43803  issmff 43809  issmfge 43844  issmfgelem 43843  issmfgt 43831  issmfgtlem 43830  issmfle 43820  issmflelem 43819  issmflem 43802
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 43784  salpreimagtlt 43805  salpreimalelt 43804
[Fremlin1] p. 36Proposition 121B (iv)issmfge 43844  issmfgelem 43843
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 43828
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 43826  cnfsmf 43815
[Fremlin1] p. 36Proposition 121D (c)decsmf 43841  decsmflem 43840  incsmf 43817  incsmflem 43816
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 43780  pimconstlt1 43781  smfconst 43824
[Fremlin1] p. 37Proposition 121E (b)smfadd 43839  smfaddlem1 43837  smfaddlem2 43838
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 43869
[Fremlin1] p. 37Proposition 121E (d)smfmul 43868  smfmullem1 43864  smfmullem2 43865  smfmullem3 43866  smfmullem4 43867
[Fremlin1] p. 37Proposition 121E (e)smfdiv 43870
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 43873  smfpimbor1lem2 43872
[Fremlin1] p. 37Proposition 121E (g)smfco 43875
[Fremlin1] p. 37Proposition 121E (h)smfres 43863
[Fremlin1] p. 38Proposition 121E (e)smfrec 43862
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 43871  smfresal 43861
[Fremlin1] p. 38Proposition 121F (a)smflim 43851  smflim2 43878  smflimlem1 43845  smflimlem2 43846  smflimlem3 43847  smflimlem4 43848  smflimlem5 43849  smflimlem6 43850  smflimmpt 43882
[Fremlin1] p. 38Proposition 121F (b)smfsup 43886  smfsuplem1 43883  smfsuplem2 43884  smfsuplem3 43885  smfsupmpt 43887  smfsupxr 43888
[Fremlin1] p. 38Proposition 121F (c)smfinf 43890  smfinflem 43889  smfinfmpt 43891
[Fremlin1] p. 39Remark 121Gsmflim 43851  smflim2 43878  smflimmpt 43882
[Fremlin1] p. 39Proposition 121Fsmfpimcc 43880
[Fremlin1] p. 39Proposition 121F (d)smflimsup 43900  smflimsuplem2 43893  smflimsuplem6 43897  smflimsuplem7 43898  smflimsuplem8 43899  smflimsupmpt 43901
[Fremlin1] p. 39Proposition 121F (e)smfliminf 43903  smfliminflem 43902  smfliminfmpt 43904
[Fremlin1] p. 80Definition 135E (b)df-smblfn 43776
[Fremlin5] p. 193Proposition 563Gbnulmbl2 24288
[Fremlin5] p. 213Lemma 565Cauniioovol 24331
[Fremlin5] p. 214Lemma 565Cauniioombl 24341
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 35478
[Fremlin5] p. 220Theorem 565Maftc1anc 35481
[FreydScedrov] p. 283Axiom of Infinityax-inf 9174  inf1 9158  inf2 9159
[Gleason] p. 117Proposition 9-2.1df-enq 10411  enqer 10421
[Gleason] p. 117Proposition 9-2.2df-1nq 10416  df-nq 10412
[Gleason] p. 117Proposition 9-2.3df-plpq 10408  df-plq 10414
[Gleason] p. 119Proposition 9-2.4caovmo 7401  df-mpq 10409  df-mq 10415
[Gleason] p. 119Proposition 9-2.5df-rq 10417
[Gleason] p. 119Proposition 9-2.6ltexnq 10475
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10476  ltbtwnnq 10478
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10471
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10472
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10479
[Gleason] p. 121Definition 9-3.1df-np 10481
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10493
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10495
[Gleason] p. 122Definitiondf-1p 10482
[Gleason] p. 122Remark (1)prub 10494
[Gleason] p. 122Lemma 9-3.4prlem934 10533
[Gleason] p. 122Proposition 9-3.2df-ltp 10485
[Gleason] p. 122Proposition 9-3.3ltsopr 10532  psslinpr 10531  supexpr 10554  suplem1pr 10552  suplem2pr 10553
[Gleason] p. 123Proposition 9-3.5addclpr 10518  addclprlem1 10516  addclprlem2 10517  df-plp 10483
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10522
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10521
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10534
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10543  ltexprlem1 10536  ltexprlem2 10537  ltexprlem3 10538  ltexprlem4 10539  ltexprlem5 10540  ltexprlem6 10541  ltexprlem7 10542
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10545  ltaprlem 10544
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10546
[Gleason] p. 124Lemma 9-3.6prlem936 10547
[Gleason] p. 124Proposition 9-3.7df-mp 10484  mulclpr 10520  mulclprlem 10519  reclem2pr 10548
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10529
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10524
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10523
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10528
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10551  reclem3pr 10549  reclem4pr 10550
[Gleason] p. 126Proposition 9-4.1df-enr 10555  enrer 10563
[Gleason] p. 126Proposition 9-4.2df-0r 10560  df-1r 10561  df-nr 10556
[Gleason] p. 126Proposition 9-4.3df-mr 10558  df-plr 10557  negexsr 10602  recexsr 10607  recexsrlem 10603
[Gleason] p. 127Proposition 9-4.4df-ltr 10559
[Gleason] p. 130Proposition 10-1.3creui 11711  creur 11710  cru 11708
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 10688  axcnre 10664
[Gleason] p. 132Definition 10-3.1crim 14564  crimd 14681  crimi 14642  crre 14563  crred 14680  crrei 14641
[Gleason] p. 132Definition 10-3.2remim 14566  remimd 14647
[Gleason] p. 133Definition 10.36absval2 14734  absval2d 14895  absval2i 14847
[Gleason] p. 133Proposition 10-3.4(a)cjadd 14590  cjaddd 14669  cjaddi 14637
[Gleason] p. 133Proposition 10-3.4(c)cjmul 14591  cjmuld 14670  cjmuli 14638
[Gleason] p. 133Proposition 10-3.4(e)cjcj 14589  cjcjd 14648  cjcji 14620
[Gleason] p. 133Proposition 10-3.4(f)cjre 14588  cjreb 14572  cjrebd 14651  cjrebi 14623  cjred 14675  rere 14571  rereb 14569  rerebd 14650  rerebi 14622  rered 14673
[Gleason] p. 133Proposition 10-3.4(h)addcj 14597  addcjd 14661  addcji 14632
[Gleason] p. 133Proposition 10-3.7(a)absval 14687
[Gleason] p. 133Proposition 10-3.7(b)abscj 14729  abscjd 14900  abscji 14851
[Gleason] p. 133Proposition 10-3.7(c)abs00 14739  abs00d 14896  abs00i 14848  absne0d 14897
[Gleason] p. 133Proposition 10-3.7(d)releabs 14771  releabsd 14901  releabsi 14852
[Gleason] p. 133Proposition 10-3.7(f)absmul 14744  absmuld 14904  absmuli 14854
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 14732  sqabsaddi 14855
[Gleason] p. 133Proposition 10-3.7(h)abstri 14780  abstrid 14906  abstrii 14858
[Gleason] p. 134Definition 10-4.1df-exp 13522  exp0 13525  expp1 13528  expp1d 13603
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 25422  cxpaddd 25460  expadd 13563  expaddd 13604  expaddz 13565
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 25431  cxpmuld 25479  expmul 13566  expmuld 13605  expmulz 13567
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 25428  mulcxpd 25471  mulexp 13560  mulexpd 13617  mulexpz 13561
[Gleason] p. 140Exercise 1znnen 15657
[Gleason] p. 141Definition 11-2.1fzval 12983
[Gleason] p. 168Proposition 12-2.1(a)climadd 15079  rlimadd 15090  rlimdiv 15095
[Gleason] p. 168Proposition 12-2.1(b)climsub 15081  rlimsub 15092
[Gleason] p. 168Proposition 12-2.1(c)climmul 15080  rlimmul 15093
[Gleason] p. 171Corollary 12-2.2climmulc2 15084
[Gleason] p. 172Corollary 12-2.5climrecl 15030
[Gleason] p. 172Proposition 12-2.4(c)climabs 15051  climcj 15052  climim 15054  climre 15053  rlimabs 15056  rlimcj 15057  rlimim 15059  rlimre 15058
[Gleason] p. 173Definition 12-3.1df-ltxr 10758  df-xr 10757  ltxr 12593
[Gleason] p. 175Definition 12-4.1df-limsup 14918  limsupval 14921
[Gleason] p. 180Theorem 12-5.1climsup 15119
[Gleason] p. 180Theorem 12-5.3caucvg 15128  caucvgb 15129  caucvgr 15125  climcau 15120
[Gleason] p. 182Exercise 3cvgcmp 15264
[Gleason] p. 182Exercise 4cvgrat 15331
[Gleason] p. 195Theorem 13-2.12abs1m 14785
[Gleason] p. 217Lemma 13-4.1btwnzge0 13289
[Gleason] p. 223Definition 14-1.1df-met 20211
[Gleason] p. 223Definition 14-1.1(a)met0 23096  xmet0 23095
[Gleason] p. 223Definition 14-1.1(b)metgt0 23112
[Gleason] p. 223Definition 14-1.1(c)metsym 23103
[Gleason] p. 223Definition 14-1.1(d)mettri 23105  mstri 23222  xmettri 23104  xmstri 23221
[Gleason] p. 225Definition 14-1.5xpsmet 23135
[Gleason] p. 230Proposition 14-2.6txlm 22399
[Gleason] p. 240Theorem 14-4.3metcnp4 24062
[Gleason] p. 240Proposition 14-4.2metcnp3 23293
[Gleason] p. 243Proposition 14-4.16addcn 23617  addcn2 15041  mulcn 23619  mulcn2 15043  subcn 23618  subcn2 15042
[Gleason] p. 295Remarkbcval3 13758  bcval4 13759
[Gleason] p. 295Equation 2bcpasc 13773
[Gleason] p. 295Definition of binomial coefficientbcval 13756  df-bc 13755
[Gleason] p. 296Remarkbcn0 13762  bcnn 13764
[Gleason] p. 296Theorem 15-2.8binom 15278
[Gleason] p. 308Equation 2ef0 15536
[Gleason] p. 308Equation 3efcj 15537
[Gleason] p. 309Corollary 15-4.3efne0 15542
[Gleason] p. 309Corollary 15-4.4efexp 15546
[Gleason] p. 310Equation 14sinadd 15609
[Gleason] p. 310Equation 15cosadd 15610
[Gleason] p. 311Equation 17sincossq 15621
[Gleason] p. 311Equation 18cosbnd 15626  sinbnd 15625
[Gleason] p. 311Lemma 15-4.7sqeqor 13670  sqeqori 13668
[Gleason] p. 311Definition of ` `df-pi 15518
[Godowski] p. 730Equation SFgoeqi 30208
[GodowskiGreechie] p. 249Equation IV3oai 29603
[Golan] p. 1Remarksrgisid 19397
[Golan] p. 1Definitiondf-srg 19375
[Golan] p. 149Definitiondf-slmd 31031
[Gonshor] p. 7Definitiondf-scut 33619
[Gonshor] p. 9Theorem 2.5slerec 33654
[Gonshor] p. 10Theorem 2.6cofcut1 33728
[Gonshor] p. 10Theorem 2.7cofcut2 33729
[Gonshor] p. 12Theorem 2.9cofcutr 33730
[Gonshor] p. 13Definitiondf-adds 33757
[GramKnuthPat], p. 47Definition 2.42df-fwddif 34099
[Gratzer] p. 23Section 0.6df-mre 16960
[Gratzer] p. 27Section 0.6df-mri 16962
[Hall] p. 1Section 1.1df-asslaw 44916  df-cllaw 44914  df-comlaw 44915
[Hall] p. 2Section 1.2df-clintop 44928
[Hall] p. 7Section 1.3df-sgrp2 44949
[Halmos] p. 31Theorem 17.3riesz1 30000  riesz2 30001
[Halmos] p. 41Definition of Hermitianhmopadj2 29876
[Halmos] p. 42Definition of projector orderingpjordi 30108
[Halmos] p. 43Theorem 26.1elpjhmop 30120  elpjidm 30119  pjnmopi 30083
[Halmos] p. 44Remarkpjinormi 29622  pjinormii 29611
[Halmos] p. 44Theorem 26.2elpjch 30124  pjrn 29642  pjrni 29637  pjvec 29631
[Halmos] p. 44Theorem 26.3pjnorm2 29662
[Halmos] p. 44Theorem 26.4hmopidmpj 30089  hmopidmpji 30087
[Halmos] p. 45Theorem 27.1pjinvari 30126
[Halmos] p. 45Theorem 27.3pjoci 30115  pjocvec 29632
[Halmos] p. 45Theorem 27.4pjorthcoi 30104
[Halmos] p. 48Theorem 29.2pjssposi 30107
[Halmos] p. 48Theorem 29.3pjssdif1i 30110  pjssdif2i 30109
[Halmos] p. 50Definition of spectrumdf-spec 29790
[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 1802
[Hatcher] p. 25Definitiondf-phtpc 23744  df-phtpy 23723
[Hatcher] p. 26Definitiondf-pco 23757  df-pi1 23760
[Hatcher] p. 26Proposition 1.2phtpcer 23747
[Hatcher] p. 26Proposition 1.3pi1grp 23802
[Hefferon] p. 240Definition 3.12df-dmat 21241  df-dmatalt 45273
[Helfgott] p. 2Theoremtgoldbach 44803
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 44788
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 44800  bgoldbtbnd 44795  bgoldbtbnd 44795  tgblthelfgott 44801
[Helfgott] p. 5Proposition 1.1circlevma 32192
[Helfgott] p. 69Statement 7.49circlemethhgt 32193
[Helfgott] p. 69Statement 7.50hgt750lema 32207  hgt750lemb 32206  hgt750leme 32208  hgt750lemf 32203  hgt750lemg 32204
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 44797  tgoldbachgt 32213  tgoldbachgtALTV 44798  tgoldbachgtd 32212
[Helfgott] p. 70Statement 7.49ax-hgt749 32194
[Herstein] p. 54Exercise 28df-grpo 28428
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18230  grpoideu 28444  mndideu 18038
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18256  grpoinveu 28454
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18284  grpo2inv 28466
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18295  grpoinvop 28468
[Herstein] p. 57Exercise 1dfgrp3e 18317
[Hitchcock] p. 5Rule A3mptnan 1775
[Hitchcock] p. 5Rule A4mptxor 1776
[Hitchcock] p. 5Rule A5mtpxor 1778
[Holland] p. 1519Theorem 2sumdmdi 30355
[Holland] p. 1520Lemma 5cdj1i 30368  cdj3i 30376  cdj3lem1 30369  cdjreui 30367
[Holland] p. 1524Lemma 7mddmdin0i 30366
[Holland95] p. 13Theorem 3.6hlathil 39598
[Holland95] p. 14Line 15hgmapvs 39528
[Holland95] p. 14Line 16hdmaplkr 39550
[Holland95] p. 14Line 17hdmapellkr 39551
[Holland95] p. 14Line 19hdmapglnm2 39548
[Holland95] p. 14Line 20hdmapip0com 39554
[Holland95] p. 14Theorem 3.6hdmapevec2 39473
[Holland95] p. 14Lines 24 and 25hdmapoc 39568
[Holland95] p. 204Definition of involutiondf-srng 19736
[Holland95] p. 212Definition of subspacedf-psubsp 37140
[Holland95] p. 214Lemma 3.3lclkrlem2v 39165
[Holland95] p. 214Definition 3.2df-lpolN 39118
[Holland95] p. 214Definition of nonsingularpnonsingN 37570
[Holland95] p. 215Lemma 3.3(1)dihoml4 39014  poml4N 37590
[Holland95] p. 215Lemma 3.3(2)dochexmid 39105  pexmidALTN 37615  pexmidN 37606
[Holland95] p. 218Theorem 3.6lclkr 39170
[Holland95] p. 218Definition of dual vector spacedf-ldual 36761  ldualset 36762
[Holland95] p. 222Item 1df-lines 37138  df-pointsN 37139
[Holland95] p. 222Item 2df-polarityN 37540
[Holland95] p. 223Remarkispsubcl2N 37584  omllaw4 36883  pol1N 37547  polcon3N 37554
[Holland95] p. 223Definitiondf-psubclN 37572
[Holland95] p. 223Equation for polaritypolval2N 37543
[Holmes] p. 40Definitiondf-xrn 36124
[Hughes] p. 44Equation 1.21bax-his3 29019
[Hughes] p. 47Definition of projection operatordfpjop 30117
[Hughes] p. 49Equation 1.30eighmre 29898  eigre 29770  eigrei 29769
[Hughes] p. 49Equation 1.31eighmorth 29899  eigorth 29773  eigorthi 29772
[Hughes] p. 137Remark (ii)eigposi 29771
[Huneke] p. 1Claim 1frgrncvvdeq 28246
[Huneke] p. 1Statement 1frgrncvvdeqlem7 28242
[Huneke] p. 1Statement 2frgrncvvdeqlem8 28243
[Huneke] p. 1Statement 3frgrncvvdeqlem9 28244
[Huneke] p. 2Claim 2frgrregorufr 28262  frgrregorufr0 28261  frgrregorufrg 28263
[Huneke] p. 2Claim 3frgrhash2wsp 28269  frrusgrord 28278  frrusgrord0 28277
[Huneke] p. 2Statementdf-clwwlknon 28025
[Huneke] p. 2Statement 4frgrwopreglem4 28252
[Huneke] p. 2Statement 5frgrwopreg1 28255  frgrwopreg2 28256  frgrwopregasn 28253  frgrwopregbsn 28254
[Huneke] p. 2Statement 6frgrwopreglem5 28258
[Huneke] p. 2Statement 7fusgreghash2wspv 28272
[Huneke] p. 2Statement 8fusgreghash2wsp 28275
[Huneke] p. 2Statement 9clwlksndivn 28023  numclwlk1 28308  numclwlk1lem1 28306  numclwlk1lem2 28307  numclwwlk1 28298  numclwwlk8 28329
[Huneke] p. 2Definition 3frgrwopreglem1 28249
[Huneke] p. 2Definition 4df-clwlks 27712
[Huneke] p. 2Definition 62clwwlk 28284
[Huneke] p. 2Definition 7numclwwlkovh 28310  numclwwlkovh0 28309
[Huneke] p. 2Statement 10numclwwlk2 28318
[Huneke] p. 2Statement 11rusgrnumwlkg 27915
[Huneke] p. 2Statement 12numclwwlk3 28322
[Huneke] p. 2Statement 13numclwwlk5 28325
[Huneke] p. 2Statement 14numclwwlk7 28328
[Indrzejczak] p. 33Definition ` `Enatded 28340  natded 28340
[Indrzejczak] p. 33Definition ` `Inatded 28340
[Indrzejczak] p. 34Definition ` `Enatded 28340  natded 28340
[Indrzejczak] p. 34Definition ` `Inatded 28340
[Jech] p. 4Definition of classcv 1541  cvjust 2732
[Jech] p. 42Lemma 6.1alephexp1 10079
[Jech] p. 42Equation 6.1alephadd 10077  alephmul 10078
[Jech] p. 43Lemma 6.2infmap 10076  infmap2 9718
[Jech] p. 71Lemma 9.3jech9.3 9316
[Jech] p. 72Equation 9.3scott0 9388  scottex 9387
[Jech] p. 72Exercise 9.1rankval4 9369
[Jech] p. 72Scheme "Collection Principle"cp 9393
[Jech] p. 78Noteopthprc 5587
[JonesMatijasevic] p. 694Definition 2.3rmxyval 40309
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 40397
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 40398
[JonesMatijasevic] p. 695Equation 2.7rmxadd 40321
[JonesMatijasevic] p. 695Equation 2.8rmyadd 40325
[JonesMatijasevic] p. 695Equation 2.9rmxp1 40326  rmyp1 40327
[JonesMatijasevic] p. 695Equation 2.10rmxm1 40328  rmym1 40329
[JonesMatijasevic] p. 695Equation 2.11rmx0 40319  rmx1 40320  rmxluc 40330
[JonesMatijasevic] p. 695Equation 2.12rmy0 40323  rmy1 40324  rmyluc 40331
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 40333
[JonesMatijasevic] p. 695Equation 2.14rmydbl 40334
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 40354  jm2.17b 40355  jm2.17c 40356
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 40387
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 40391
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 40382
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 40357  jm2.24nn 40353
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 40396
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 40402  rmygeid 40358
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 40414
[Juillerat] p. 11Section *5etransc 43366  etransclem47 43364  etransclem48 43365
[Juillerat] p. 12Equation (7)etransclem44 43361
[Juillerat] p. 12Equation *(7)etransclem46 43363
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 43349
[Juillerat] p. 13Proofetransclem35 43352
[Juillerat] p. 13Part of case 2 proven inetransclem38 43355
[Juillerat] p. 13Part of case 2 provenetransclem24 43341
[Juillerat] p. 13Part of case 2: proven inetransclem41 43358
[Juillerat] p. 14Proofetransclem23 43340
[KalishMontague] p. 81Note 1ax-6 1975
[KalishMontague] p. 85Lemma 2equid 2024
[KalishMontague] p. 85Lemma 3equcomi 2029
[KalishMontague] p. 86Lemma 7cbvalivw 2019  cbvaliw 2018  wl-cbvmotv 35295  wl-motae 35297  wl-moteq 35296
[KalishMontague] p. 87Lemma 8spimvw 2007  spimw 1978
[KalishMontague] p. 87Lemma 9spfw 2045  spw 2046
[Kalmbach] p. 14Definition of latticechabs1 29451  chabs1i 29453  chabs2 29452  chabs2i 29454  chjass 29468  chjassi 29421  latabs1 17813  latabs2 17814
[Kalmbach] p. 15Definition of atomdf-at 30273  ela 30274
[Kalmbach] p. 15Definition of coverscvbr2 30218  cvrval2 36911
[Kalmbach] p. 16Definitiondf-ol 36815  df-oml 36816
[Kalmbach] p. 20Definition of commutescmbr 29519  cmbri 29525  cmtvalN 36848  df-cm 29518  df-cmtN 36814
[Kalmbach] p. 22Remarkomllaw5N 36884  pjoml5 29548  pjoml5i 29523
[Kalmbach] p. 22Definitionpjoml2 29546  pjoml2i 29520
[Kalmbach] p. 22Theorem 2(v)cmcm 29549  cmcmi 29527  cmcmii 29532  cmtcomN 36886
[Kalmbach] p. 22Theorem 2(ii)omllaw3 36882  omlsi 29339  pjoml 29371  pjomli 29370
[Kalmbach] p. 22Definition of OML lawomllaw2N 36881
[Kalmbach] p. 23Remarkcmbr2i 29531  cmcm3 29550  cmcm3i 29529  cmcm3ii 29534  cmcm4i 29530  cmt3N 36888  cmt4N 36889  cmtbr2N 36890
[Kalmbach] p. 23Lemma 3cmbr3 29543  cmbr3i 29535  cmtbr3N 36891
[Kalmbach] p. 25Theorem 5fh1 29553  fh1i 29556  fh2 29554  fh2i 29557  omlfh1N 36895
[Kalmbach] p. 65Remarkchjatom 30292  chslej 29433  chsleji 29393  shslej 29315  shsleji 29305
[Kalmbach] p. 65Proposition 1chocin 29430  chocini 29389  chsupcl 29275  chsupval2 29345  h0elch 29190  helch 29178  hsupval2 29344  ocin 29231  ococss 29228  shococss 29229
[Kalmbach] p. 65Definition of subspace sumshsval 29247
[Kalmbach] p. 66Remarkdf-pjh 29330  pjssmi 30100  pjssmii 29616
[Kalmbach] p. 67Lemma 3osum 29580  osumi 29577
[Kalmbach] p. 67Lemma 4pjci 30135
[Kalmbach] p. 103Exercise 6atmd2 30335
[Kalmbach] p. 103Exercise 12mdsl0 30245
[Kalmbach] p. 140Remarkhatomic 30295  hatomici 30294  hatomistici 30297
[Kalmbach] p. 140Proposition 1atlatmstc 36956
[Kalmbach] p. 140Proposition 1(i)atexch 30316  lsatexch 36680
[Kalmbach] p. 140Proposition 1(ii)chcv1 30290  cvlcvr1 36976  cvr1 37047
[Kalmbach] p. 140Proposition 1(iii)cvexch 30309  cvexchi 30304  cvrexch 37057
[Kalmbach] p. 149Remark 2chrelati 30299  hlrelat 37039  hlrelat5N 37038  lrelat 36651
[Kalmbach] p. 153Exercise 5lsmcv 20032  lsmsatcv 36647  spansncv 29588  spansncvi 29587
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 36666  spansncv2 30228
[Kalmbach] p. 266Definitiondf-st 30146
[Kalmbach2] p. 8Definition of adjointdf-adjh 29784
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10146  fpwwe2 10143
[KanamoriPincus] p. 416Corollary 1.3canth4 10147
[KanamoriPincus] p. 417Corollary 1.6canthp1 10154
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10149
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10151
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10164
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10168  gchxpidm 10169
[KanamoriPincus] p. 419Theorem 2.1gchacg 10180  gchhar 10179
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 9716  unxpwdom 9126
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10170
[Kreyszig] p. 3Property M1metcl 23085  xmetcl 23084
[Kreyszig] p. 4Property M2meteq0 23092
[Kreyszig] p. 8Definition 1.1-8dscmet 23325
[Kreyszig] p. 12Equation 5conjmul 11435  muleqadd 11362
[Kreyszig] p. 18Definition 1.3-2mopnval 23191
[Kreyszig] p. 19Remarkmopntopon 23192
[Kreyszig] p. 19Theorem T1mopn0 23251  mopnm 23197
[Kreyszig] p. 19Theorem T2unimopn 23249
[Kreyszig] p. 19Definition of neighborhoodneibl 23254
[Kreyszig] p. 20Definition 1.3-3metcnp2 23295
[Kreyszig] p. 25Definition 1.4-1lmbr 22009  lmmbr 24010  lmmbr2 24011
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 22131
[Kreyszig] p. 28Theorem 1.4-5lmcau 24065
[Kreyszig] p. 28Definition 1.4-3iscau 24028  iscmet2 24046
[Kreyszig] p. 30Theorem 1.4-7cmetss 24068
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 22212  metelcls 24057
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 24058  metcld2 24059
[Kreyszig] p. 51Equation 2clmvneg1 23851  lmodvneg1 19796  nvinv 28574  vcm 28511
[Kreyszig] p. 51Equation 1aclm0vs 23847  lmod0vs 19786  slmd0vs 31054  vc0 28509
[Kreyszig] p. 51Equation 1blmodvs0 19787  slmdvs0 31055  vcz 28510
[Kreyszig] p. 58Definition 2.2-1imsmet 28626  ngpmet 23356  nrmmetd 23327
[Kreyszig] p. 59Equation 1imsdval 28621  imsdval2 28622  ncvspds 23913  ngpds 23357
[Kreyszig] p. 63Problem 1nmval 23342  nvnd 28623
[Kreyszig] p. 64Problem 2nmeq0 23371  nmge0 23370  nvge0 28608  nvz 28604
[Kreyszig] p. 64Problem 3nmrtri 23377  nvabs 28607
[Kreyszig] p. 91Definition 2.7-1isblo3i 28736
[Kreyszig] p. 92Equation 2df-nmoo 28680
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 28742  blocni 28740
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 28741
[Kreyszig] p. 129Definition 3.1-1cphipeq0 23956  ipeq0 20454  ipz 28654
[Kreyszig] p. 135Problem 2cphpyth 23968  pythi 28785
[Kreyszig] p. 137Lemma 3-2.1(a)sii 28789
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 23990
[Kreyszig] p. 144Equation 4supcvg 15304
[Kreyszig] p. 144Theorem 3.3-1minvec 24188  minveco 28819
[Kreyszig] p. 196Definition 3.9-1df-aj 28685
[Kreyszig] p. 247Theorem 4.7-2bcth 24081
[Kreyszig] p. 249Theorem 4.7-3ubth 28808
[Kreyszig] p. 470Definition of positive operator orderingleop 30058  leopg 30057
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 30076
[Kreyszig] p. 525Theorem 10.1-1htth 28853
[Kulpa] p. 547Theorempoimir 35433
[Kulpa] p. 547Equation (1)poimirlem32 35432
[Kulpa] p. 547Equation (2)poimirlem31 35431
[Kulpa] p. 548Theorembroucube 35434
[Kulpa] p. 548Equation (6)poimirlem26 35426
[Kulpa] p. 548Equation (7)poimirlem27 35427
[Kunen] p. 10Axiom 0ax6e 2383  axnul 5173
[Kunen] p. 11Axiom 3axnul 5173
[Kunen] p. 12Axiom 6zfrep6 7681
[Kunen] p. 24Definition 10.24mapval 8449  mapvalg 8447
[Kunen] p. 30Lemma 10.20fodomg 10022
[Kunen] p. 31Definition 10.24mapex 8443
[Kunen] p. 95Definition 2.1df-r1 9266
[Kunen] p. 97Lemma 2.10r1elss 9308  r1elssi 9307
[Kunen] p. 107Exercise 4rankop 9360  rankopb 9354  rankuni 9365  rankxplim 9381  rankxpsuc 9384
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4893
[Lang] , p. 225Corollary 1.3finexttrb 31309
[Lang] p. Definitiondf-rn 5536
[Lang] p. 3Statementlidrideqd 17995  mndbn0 18043
[Lang] p. 3Definitiondf-mnd 18028
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18013
[Lang] p. 4Property of composites. Second formulagsumccat 18122
[Lang] p. 5Equationgsumreidx 19156
[Lang] p. 5Definition of an (infinite) productgsumfsupp 44910
[Lang] p. 6Examplenn0mnd 44907
[Lang] p. 6Equationgsumxp2 19219
[Lang] p. 6Statementcycsubm 18463
[Lang] p. 6Definitionmulgnn0gsum 18352
[Lang] p. 6Observationmndlsmidm 18914
[Lang] p. 7Definitiondfgrp2e 18247
[Lang] p. 30Definitiondf-tocyc 30951
[Lang] p. 32Property (a)cyc3genpm 30996
[Lang] p. 32Property (b)cyc3conja 31001  cycpmconjv 30986
[Lang] p. 53Definitiondf-cat 17042
[Lang] p. 53Axiom CAT 1cat1 17469  cat1lem 17468
[Lang] p. 54Definitiondf-iso 17124
[Lang] p. 57Definitiondf-inito 17356  df-termo 17357
[Lang] p. 58Exampleirinitoringc 45161
[Lang] p. 58Statementinitoeu1 17383  termoeu1 17390
[Lang] p. 62Definitiondf-func 17233
[Lang] p. 65Definitiondf-nat 17318
[Lang] p. 91Notedf-ringc 45097
[Lang] p. 92Statementmxidlprm 31212
[Lang] p. 92Definitionisprmidlc 31195
[Lang] p. 128Remarkdsmmlmod 20561
[Lang] p. 129Prooflincscm 45305  lincscmcl 45307  lincsum 45304  lincsumcl 45306
[Lang] p. 129Statementlincolss 45309
[Lang] p. 129Observationdsmmfi 20554
[Lang] p. 141Theorem 5.3dimkerim 31280  qusdimsum 31281
[Lang] p. 141Corollary 5.4lssdimle 31263
[Lang] p. 147Definitionsnlindsntor 45346
[Lang] p. 504Statementmat1 21198  matring 21194
[Lang] p. 504Definitiondf-mamu 21137
[Lang] p. 505Statementmamuass 21153  mamutpos 21209  matassa 21195  mattposvs 21206  tposmap 21208
[Lang] p. 513Definitionmdet1 21352  mdetf 21346
[Lang] p. 513Theorem 4.4cramer 21442
[Lang] p. 514Proposition 4.6mdetleib 21338
[Lang] p. 514Proposition 4.8mdettpos 21362
[Lang] p. 515Definitiondf-minmar1 21386  smadiadetr 21426
[Lang] p. 515Corollary 4.9mdetero 21361  mdetralt 21359
[Lang] p. 517Proposition 4.15mdetmul 21374
[Lang] p. 518Definitiondf-madu 21385
[Lang] p. 518Proposition 4.16madulid 21396  madurid 21395  matinv 21428
[Lang] p. 561Theorem 3.1cayleyhamilton 21641
[Lang], p. 224Proposition 1.2extdgmul 31308  fedgmul 31284
[Lang], p. 561Remarkchpmatply1 21583
[Lang], p. 561Definitiondf-chpmat 21578
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 41490
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 41485
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 41491
[LeBlanc] p. 277Rule R2axnul 5173
[Levy] p. 12Axiom 4.3.1df-clab 2717
[Levy] p. 338Axiomdf-clel 2811  df-cleq 2730
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2811  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 2717
[Levy] p. 358Axiomdf-clab 2717
[Levy58] p. 2Definition Iisfin1-3 9886
[Levy58] p. 2Definition IIdf-fin2 9786
[Levy58] p. 2Definition Iadf-fin1a 9785
[Levy58] p. 2Definition IIIdf-fin3 9788
[Levy58] p. 3Definition Vdf-fin5 9789
[Levy58] p. 3Definition IVdf-fin4 9787
[Levy58] p. 4Definition VIdf-fin6 9790
[Levy58] p. 4Definition VIIdf-fin7 9791
[Levy58], p. 3Theorem 1fin1a2 9915
[Lipparini] p. 3Lemma 2.1.1nosepssdm 33530
[Lipparini] p. 3Lemma 2.1.4noresle 33541
[Lipparini] p. 6Proposition 4.2noinfbnd1 33573  nosupbnd1 33558
[Lipparini] p. 6Proposition 4.3noinfbnd2 33575  nosupbnd2 33560
[Lipparini] p. 7Theorem 5.1noetasuplem3 33579  noetasuplem4 33580
[Lipparini] p. 7Corollary 4.4nosupinfsep 33576
[Lopez-Astorga] p. 12Rule 1mptnan 1775
[Lopez-Astorga] p. 12Rule 2mptxor 1776
[Lopez-Astorga] p. 12Rule 3mtpxor 1778
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 30343
[Maeda] p. 168Lemma 5mdsym 30347  mdsymi 30346
[Maeda] p. 168Lemma 4(i)mdsymlem4 30341  mdsymlem6 30343  mdsymlem7 30344
[Maeda] p. 168Lemma 4(ii)mdsymlem8 30345
[MaedaMaeda] p. 1Remarkssdmd1 30248  ssdmd2 30249  ssmd1 30246  ssmd2 30247
[MaedaMaeda] p. 1Lemma 1.2mddmd2 30244
[MaedaMaeda] p. 1Definition 1.1df-dmd 30216  df-md 30215  mdbr 30229
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 30266  mdslj1i 30254  mdslj2i 30255  mdslle1i 30252  mdslle2i 30253  mdslmd1i 30264  mdslmd2i 30265
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 30256  mdsl2bi 30258  mdsl2i 30257
[MaedaMaeda] p. 2Lemma 1.6mdexchi 30270
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 30267
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 30268
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 30245
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 30250  mdsl3 30251
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 30269
[MaedaMaeda] p. 4Theorem 1.14mdcompli 30364
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 36958  hlrelat1 37037
[MaedaMaeda] p. 31Lemma 7.5lcvexch 36676
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 30271  cvmdi 30259  cvnbtwn4 30224  cvrnbtwn4 36916
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 30272
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 36977  cvp 30310  cvrp 37053  lcvp 36677
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 30334
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 30333
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 36970  hlexch4N 37029
[MaedaMaeda] p. 34Exercise 7.1atabsi 30336
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 37080
[MaedaMaeda] p. 61Definition 15.10psubN 37386  atpsubN 37390  df-pointsN 37139  pointpsubN 37388
[MaedaMaeda] p. 62Theorem 15.5df-pmap 37141  pmap11 37399  pmaple 37398  pmapsub 37405  pmapval 37394
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 37402  pmap1N 37404
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 37407  pmapglb2N 37408  pmapglb2xN 37409  pmapglbx 37406
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 37489
[MaedaMaeda] p. 67Postulate PS1ps-1 37114
[MaedaMaeda] p. 68Lemma 16.2df-padd 37433  paddclN 37479  paddidm 37478
[MaedaMaeda] p. 68Condition PS2ps-2 37115
[MaedaMaeda] p. 68Equation 16.2.1paddass 37475
[MaedaMaeda] p. 69Lemma 16.4ps-1 37114
[MaedaMaeda] p. 69Theorem 16.4ps-2 37115
[MaedaMaeda] p. 70Theorem 16.9lsmmod 18919  lsmmod2 18920  lssats 36649  shatomici 30293  shatomistici 30296  shmodi 29325  shmodsi 29324
[MaedaMaeda] p. 130Remark 29.6dmdmd 30235  mdsymlem7 30344
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 29524
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 29428
[MaedaMaeda] p. 139Remarksumdmdii 30350
[Margaris] p. 40Rule Cexlimiv 1937
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 400  df-ex 1787  df-or 847  dfbi2 478
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 28337
[Margaris] p. 59Section 14notnotrALTVD 42073
[Margaris] p. 60Theorem 8jcn 165
[Margaris] p. 60Section 14con3ALTVD 42074
[Margaris] p. 79Rule Cexinst01 41783  exinst11 41784
[Margaris] p. 89Theorem 19.219.2 1986  19.2g 2189  r19.2z 4381
[Margaris] p. 89Theorem 19.319.3 2204  rr19.3v 3565
[Margaris] p. 89Theorem 19.5alcom 2164
[Margaris] p. 89Theorem 19.6alex 1832
[Margaris] p. 89Theorem 19.7alnex 1788
[Margaris] p. 89Theorem 19.819.8a 2182
[Margaris] p. 89Theorem 19.919.9 2207  19.9h 2290  exlimd 2220  exlimdh 2294
[Margaris] p. 89Theorem 19.11excom 2170  excomim 2171
[Margaris] p. 89Theorem 19.1219.12 2329
[Margaris] p. 90Section 19conventions-labels 28338  conventions-labels 28338  conventions-labels 28338  conventions-labels 28338
[Margaris] p. 90Theorem 19.14exnal 1833
[Margaris] p. 90Theorem 19.152albi 41534  albi 1825
[Margaris] p. 90Theorem 19.1619.16 2227
[Margaris] p. 90Theorem 19.1719.17 2228
[Margaris] p. 90Theorem 19.182exbi 41536  exbi 1853
[Margaris] p. 90Theorem 19.1919.19 2231
[Margaris] p. 90Theorem 19.202alim 41533  2alimdv 1925  alimd 2214  alimdh 1824  alimdv 1923  ax-4 1816  ralimdaa 3129  ralimdv 3092  ralimdva 3091  ralimdvva 3093  sbcimdv 3751
[Margaris] p. 90Theorem 19.2119.21 2209  19.21h 2291  19.21t 2208  19.21vv 41532  alrimd 2217  alrimdd 2216  alrimdh 1870  alrimdv 1936  alrimi 2215  alrimih 1830  alrimiv 1934  alrimivv 1935  hbralrimi 3094  r19.21be 3122  r19.21bi 3121  ralrimd 3130  ralrimdv 3100  ralrimdva 3101  ralrimdvv 3105  ralrimdvva 3106  ralrimi 3128  ralrimia 3396  ralrimiv 3095  ralrimiva 3096  ralrimivv 3102  ralrimivva 3103  ralrimivvva 3104  ralrimivw 3097
[Margaris] p. 90Theorem 19.222exim 41535  2eximdv 1926  exim 1840  eximd 2218  eximdh 1871  eximdv 1924  rexim 3154  reximd2a 3222  reximdai 3221  reximdd 42239  reximddv 3185  reximddv2 3188  reximddv3 42238  reximdv 3183  reximdv2 3181  reximdva 3184  reximdvai 3182  reximdvva 3187  reximi2 3158
[Margaris] p. 90Theorem 19.2319.23 2213  19.23bi 2192  19.23h 2292  19.23t 2212  exlimdv 1940  exlimdvv 1941  exlimexi 41682  exlimiv 1937  exlimivv 1939  rexlimd3 42231  rexlimdv 3193  rexlimdv3a 3196  rexlimdva 3194  rexlimdva2 3197  rexlimdvaa 3195  rexlimdvv 3203  rexlimdvva 3204  rexlimdvw 3200  rexlimiv 3190  rexlimiva 3191  rexlimivv 3202
[Margaris] p. 90Theorem 19.2419.24 1997
[Margaris] p. 90Theorem 19.2519.25 1887
[Margaris] p. 90Theorem 19.2619.26 1877
[Margaris] p. 90Theorem 19.2719.27 2229  r19.27z 4391  r19.27zv 4392
[Margaris] p. 90Theorem 19.2819.28 2230  19.28vv 41542  r19.28z 4384  r19.28zv 4387  rr19.28v 3566
[Margaris] p. 90Theorem 19.2919.29 1880  r19.29d2r 3242  r19.29imd 3169
[Margaris] p. 90Theorem 19.3019.30 1888
[Margaris] p. 90Theorem 19.3119.31 2236  19.31vv 41540
[Margaris] p. 90Theorem 19.3219.32 2235  r19.32 44122
[Margaris] p. 90Theorem 19.3319.33-2 41538  19.33 1891
[Margaris] p. 90Theorem 19.3419.34 1998
[Margaris] p. 90Theorem 19.3519.35 1884
[Margaris] p. 90Theorem 19.3619.36 2232  19.36vv 41539  r19.36zv 4393
[Margaris] p. 90Theorem 19.3719.37 2234  19.37vv 41541  r19.37zv 4388
[Margaris] p. 90Theorem 19.3819.38 1845
[Margaris] p. 90Theorem 19.3919.39 1996
[Margaris] p. 90Theorem 19.4019.40-2 1894  19.40 1893  r19.40 3250
[Margaris] p. 90Theorem 19.4119.41 2237  19.41rg 41708
[Margaris] p. 90Theorem 19.4219.42 2238
[Margaris] p. 90Theorem 19.4319.43 1889
[Margaris] p. 90Theorem 19.4419.44 2239  r19.44zv 4390
[Margaris] p. 90Theorem 19.4519.45 2240  r19.45zv 4389
[Margaris] p. 110Exercise 2(b)eu1 2613
[Mayet] p. 370Remarkjpi 30205  largei 30202  stri 30192
[Mayet3] p. 9Definition of CH-statesdf-hst 30147  ishst 30149
[Mayet3] p. 10Theoremhstrbi 30201  hstri 30200
[Mayet3] p. 1223Theorem 4.1mayete3i 29663
[Mayet3] p. 1240Theorem 7.1mayetes3i 29664
[MegPav2000] p. 2344Theorem 3.3stcltrthi 30213
[MegPav2000] p. 2345Definition 3.4-1chintcl 29267  chsupcl 29275
[MegPav2000] p. 2345Definition 3.4-2hatomic 30295
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 30289
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 30316
[MegPav2000] p. 2366Figure 7pl42N 37620
[MegPav2002] p. 362Lemma 2.2latj31 17825  latj32 17823  latjass 17821
[Megill] p. 444Axiom C5ax-5 1917  ax5ALT 36544
[Megill] p. 444Section 7conventions 28337
[Megill] p. 445Lemma L12aecom-o 36538  ax-c11n 36525  axc11n 2426
[Megill] p. 446Lemma L17equtrr 2034
[Megill] p. 446Lemma L18ax6fromc10 36533
[Megill] p. 446Lemma L19hbnae-o 36565  hbnae 2432
[Megill] p. 447Remark 9.1dfsb1 2485  sbid 2257  sbidd-misc 45874  sbidd 45873
[Megill] p. 448Remark 9.6axc14 2463
[Megill] p. 448Scheme C4'ax-c4 36521
[Megill] p. 448Scheme C5'ax-c5 36520  sp 2184
[Megill] p. 448Scheme C6'ax-11 2162
[Megill] p. 448Scheme C7'ax-c7 36522
[Megill] p. 448Scheme C8'ax-7 2020
[Megill] p. 448Scheme C9'ax-c9 36527
[Megill] p. 448Scheme C10'ax-6 1975  ax-c10 36523
[Megill] p. 448Scheme C11'ax-c11 36524
[Megill] p. 448Scheme C12'ax-8 2116
[Megill] p. 448Scheme C13'ax-9 2124
[Megill] p. 448Scheme C14'ax-c14 36528
[Megill] p. 448Scheme C15'ax-c15 36526
[Megill] p. 448Scheme C16'ax-c16 36529
[Megill] p. 448Theorem 9.4dral1-o 36541  dral1 2439  dral2-o 36567  dral2 2438  drex1 2441  drex2 2442  drsb1 2499  drsb2 2267
[Megill] p. 449Theorem 9.7sbcom2 2169  sbequ 2093  sbid2v 2513
[Megill] p. 450Example in Appendixhba1-o 36534  hba1 2297
[Mendelson] p. 35Axiom A3hirstL-ax3 43926
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3770  rspsbca 3771  stdpc4 2078
[Mendelson] p. 69Axiom 5ax-c4 36521  ra4 3777  stdpc5 2210
[Mendelson] p. 81Rule Cexlimiv 1937
[Mendelson] p. 95Axiom 6stdpc6 2040
[Mendelson] p. 95Axiom 7stdpc7 2252
[Mendelson] p. 225Axiom system NBGru 3679
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5371
[Mendelson] p. 231Exercise 4.10(k)inv1 4283
[Mendelson] p. 231Exercise 4.10(l)unv 4284
[Mendelson] p. 231Exercise 4.10(n)dfin3 4157
[Mendelson] p. 231Exercise 4.10(o)df-nul 4212
[Mendelson] p. 231Exercise 4.10(q)dfin4 4158
[Mendelson] p. 231Exercise 4.10(s)ddif 4027
[Mendelson] p. 231Definition of uniondfun3 4156
[Mendelson] p. 235Exercise 4.12(c)univ 5310
[Mendelson] p. 235Exercise 4.12(d)pwv 4793
[Mendelson] p. 235Exercise 4.12(j)pwin 5423
[Mendelson] p. 235Exercise 4.12(k)pwunss 4508
[Mendelson] p. 235Exercise 4.12(l)pwssun 5425
[Mendelson] p. 235Exercise 4.12(n)uniin 4822
[Mendelson] p. 235Exercise 4.12(p)reli 5670
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6101
[Mendelson] p. 244Proposition 4.8(g)epweon 7516
[Mendelson] p. 246Definition of successordf-suc 6178
[Mendelson] p. 250Exercise 4.36oelim2 8252
[Mendelson] p. 254Proposition 4.22(b)xpen 8730
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8650  xpsneng 8651
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8657  xpcomeng 8658
[Mendelson] p. 254Proposition 4.22(e)xpassen 8660
[Mendelson] p. 255Definitionbrsdom 8578
[Mendelson] p. 255Exercise 4.39endisj 8653
[Mendelson] p. 255Exercise 4.41mapprc 8441
[Mendelson] p. 255Exercise 4.43mapsnen 8636  mapsnend 8635
[Mendelson] p. 255Exercise 4.45mapunen 8736
[Mendelson] p. 255Exercise 4.47xpmapen 8735
[Mendelson] p. 255Exercise 4.42(a)map0e 8492
[Mendelson] p. 255Exercise 4.42(b)map1 8639
[Mendelson] p. 257Proposition 4.24(a)undom 8654
[Mendelson] p. 258Exercise 4.56(c)djuassen 9678  djucomen 9677
[Mendelson] p. 258Exercise 4.56(f)djudom1 9682
[Mendelson] p. 258Exercise 4.56(g)xp2dju 9676
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8187
[Mendelson] p. 266Proposition 4.34(f)oaordex 8215
[Mendelson] p. 275Proposition 4.42(d)entri3 10059
[Mendelson] p. 281Definitiondf-r1 9266
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9315
[Mendelson] p. 287Axiom system MKru 3679
[MertziosUnger] p. 152Definitiondf-frgr 28196
[MertziosUnger] p. 153Remark 1frgrconngr 28231
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 28233  vdgn1frgrv3 28234
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 28235
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 28228
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 28221  2pthfrgrrn 28219  2pthfrgrrn2 28220
[Mittelstaedt] p. 9Definitiondf-oc 29187
[Monk1] p. 22Remarkconventions 28337
[Monk1] p. 22Theorem 3.1conventions 28337
[Monk1] p. 26Theorem 2.8(vii)ssin 4121
[Monk1] p. 33Theorem 3.2(i)ssrel 5628  ssrelf 30529
[Monk1] p. 33Theorem 3.2(ii)eqrel 5629
[Monk1] p. 34Definition 3.3df-opab 5093
[Monk1] p. 36Theorem 3.7(i)coi1 6095  coi2 6096
[Monk1] p. 36Theorem 3.8(v)dm0 5763  rn0 5769
[Monk1] p. 36Theorem 3.7(ii)cnvi 5974
[Monk1] p. 37Theorem 3.13(i)relxp 5543
[Monk1] p. 37Theorem 3.13(x)dmxp 5772  rnxp 6002
[Monk1] p. 37Theorem 3.13(ii)0xp 5620  xp0 5990
[Monk1] p. 38Theorem 3.16(ii)ima0 5919
[Monk1] p. 38Theorem 3.16(viii)imai 5916
[Monk1] p. 39Theorem 3.17imaex 7647  imaexALTV 36088  imaexg 7646
[Monk1] p. 39Theorem 3.16(xi)imassrn 5914
[Monk1] p. 41Theorem 4.3(i)fnopfv 6853  funfvop 6827
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6725
[Monk1] p. 42Theorem 4.4(iii)fvelima 6735
[Monk1] p. 43Theorem 4.6funun 6385
[Monk1] p. 43Theorem 4.8(iv)dff13 7024  dff13f 7025
[Monk1] p. 46Theorem 4.15(v)funex 6992  funrnex 7680
[Monk1] p. 50Definition 5.4fniunfv 7017
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6059
[Monk1] p. 52Theorem 5.11(viii)ssint 4852
[Monk1] p. 52Definition 5.13 (i)1stval2 7731  df-1st 7714
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7732  df-2nd 7715
[Monk1] p. 112Theorem 15.17(v)ranksn 9356  ranksnb 9329
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9357
[Monk1] p. 112Theorem 15.17(iii)rankun 9358  rankunb 9352
[Monk1] p. 113Theorem 15.18r1val3 9340
[Monk1] p. 113Definition 15.19df-r1 9266  r1val2 9339
[Monk1] p. 117Lemmazorn2 10006  zorn2g 10003
[Monk1] p. 133Theorem 18.11cardom 9488
[Monk1] p. 133Theorem 18.12canth3 10061
[Monk1] p. 133Theorem 18.14carduni 9483
[Monk2] p. 105Axiom C4ax-4 1816
[Monk2] p. 105Axiom C7ax-7 2020
[Monk2] p. 105Axiom C8ax-12 2179  ax-c15 36526  ax12v2 2181
[Monk2] p. 108Lemma 5ax-c4 36521
[Monk2] p. 109Lemma 12ax-11 2162
[Monk2] p. 109Lemma 15equvini 2455  equvinv 2041  eqvinop 5344
[Monk2] p. 113Axiom C5-1ax-5 1917  ax5ALT 36544
[Monk2] p. 113Axiom C5-2ax-10 2145
[Monk2] p. 113Axiom C5-3ax-11 2162
[Monk2] p. 114Lemma 21sp 2184
[Monk2] p. 114Lemma 22axc4 2323  hba1-o 36534  hba1 2297
[Monk2] p. 114Lemma 23nfia1 2158
[Monk2] p. 114Lemma 24nfa2 2178  nfra2 3142  nfra2w 3140
[Moore] p. 53Part Idf-mre 16960
[Munkres] p. 77Example 2distop 21746  indistop 21753  indistopon 21752
[Munkres] p. 77Example 3fctop 21755  fctop2 21756
[Munkres] p. 77Example 4cctop 21757
[Munkres] p. 78Definition of basisdf-bases 21697  isbasis3g 21700
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 16820  tgval2 21707
[Munkres] p. 79Remarktgcl 21720
[Munkres] p. 80Lemma 2.1tgval3 21714
[Munkres] p. 80Lemma 2.2tgss2 21738  tgss3 21737
[Munkres] p. 81Lemma 2.3basgen 21739  basgen2 21740
[Munkres] p. 83Exercise 3topdifinf 35143  topdifinfeq 35144  topdifinffin 35142  topdifinfindis 35140
[Munkres] p. 89Definition of subspace topologyresttop 21911
[Munkres] p. 93Theorem 6.1(1)0cld 21789  topcld 21786
[Munkres] p. 93Theorem 6.1(2)iincld 21790
[Munkres] p. 93Theorem 6.1(3)uncld 21792
[Munkres] p. 94Definition of closureclsval 21788
[Munkres] p. 94Definition of interiorntrval 21787
[Munkres] p. 95Theorem 6.5(a)clsndisj 21826  elcls 21824
[Munkres] p. 95Theorem 6.5(b)elcls3 21834
[Munkres] p. 97Theorem 6.6clslp 21899  neindisj 21868
[Munkres] p. 97Corollary 6.7cldlp 21901
[Munkres] p. 97Definition of limit pointislp2 21896  lpval 21890
[Munkres] p. 98Definition of Hausdorff spacedf-haus 22066
[Munkres] p. 102Definition of continuous functiondf-cn 21978  iscn 21986  iscn2 21989
[Munkres] p. 107Theorem 7.2(g)cncnp 22031  cncnp2 22032  cncnpi 22029  df-cnp 21979  iscnp 21988  iscnp2 21990
[Munkres] p. 127Theorem 10.1metcn 23296
[Munkres] p. 128Theorem 10.3metcn4 24063
[Nathanson] p. 123Remarkreprgt 32171  reprinfz1 32172  reprlt 32169
[Nathanson] p. 123Definitiondf-repr 32159
[Nathanson] p. 123Chapter 5.1circlemethnat 32191
[Nathanson] p. 123Propositionbreprexp 32183  breprexpnat 32184  itgexpif 32156
[NielsenChuang] p. 195Equation 4.73unierri 30039
[OeSilva] p. 2042Section 2ax-bgbltosilva 44796
[Pfenning] p. 17Definition XMnatded 28340
[Pfenning] p. 17Definition NNCnatded 28340  notnotrd 135
[Pfenning] p. 17Definition ` `Cnatded 28340
[Pfenning] p. 18Rule"natded 28340
[Pfenning] p. 18Definition /\Inatded 28340
[Pfenning] p. 18Definition ` `Enatded 28340  natded 28340  natded 28340  natded 28340  natded 28340
[Pfenning] p. 18Definition ` `Inatded 28340  natded 28340  natded 28340  natded 28340  natded 28340
[Pfenning] p. 18Definition ` `ELnatded 28340
[Pfenning] p. 18Definition ` `ERnatded 28340
[Pfenning] p. 18Definition ` `Ea,unatded 28340
[Pfenning] p. 18Definition ` `IRnatded 28340
[Pfenning] p. 18Definition ` `Ianatded 28340
[Pfenning] p. 127Definition =Enatded 28340
[Pfenning] p. 127Definition =Inatded 28340
[Ponnusamy] p. 361Theorem 6.44cphip0l 23954  df-dip 28636  dip0l 28653  ip0l 20452
[Ponnusamy] p. 361Equation 6.45cphipval 23995  ipval 28638
[Ponnusamy] p. 362Equation I1dipcj 28649  ipcj 20450
[Ponnusamy] p. 362Equation I3cphdir 23957  dipdir 28777  ipdir 20455  ipdiri 28765
[Ponnusamy] p. 362Equation I4ipidsq 28645  nmsq 23946
[Ponnusamy] p. 362Equation 6.46ip0i 28760
[Ponnusamy] p. 362Equation 6.47ip1i 28762
[Ponnusamy] p. 362Equation 6.48ip2i 28763
[Ponnusamy] p. 363Equation I2cphass 23963  dipass 28780  ipass 20461  ipassi 28776
[Prugovecki] p. 186Definition of brabraval 29879  df-bra 29785
[Prugovecki] p. 376Equation 8.1df-kb 29786  kbval 29889
[PtakPulmannova] p. 66Proposition 3.2.17atomli 30317
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 37525
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 30331  atcvat4i 30332  cvrat3 37079  cvrat4 37080  lsatcvat3 36689
[PtakPulmannova] p. 68Definition 3.2.18cvbr 30217  cvrval 36906  df-cv 30214  df-lcv 36656  lspsncv0 20037
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 37537
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 37538
[Quine] p. 16Definition 2.1df-clab 2717  rabid 3281
[Quine] p. 17Definition 2.1''dfsb7 2283
[Quine] p. 18Definition 2.7df-cleq 2730
[Quine] p. 19Definition 2.9conventions 28337  df-v 3400
[Quine] p. 34Theorem 5.1abeq2 2864
[Quine] p. 35Theorem 5.2abid1 2873  abid2f 2931
[Quine] p. 40Theorem 6.1sb5 2276
[Quine] p. 40Theorem 6.2sb6 2095  sbalex 2244
[Quine] p. 41Theorem 6.3df-clel 2811
[Quine] p. 41Theorem 6.4eqid 2738  eqid1 28404
[Quine] p. 41Theorem 6.5eqcom 2745
[Quine] p. 42Theorem 6.6df-sbc 3681
[Quine] p. 42Theorem 6.7dfsbcq 3682  dfsbcq2 3683
[Quine] p. 43Theorem 6.8vex 3402
[Quine] p. 43Theorem 6.9isset 3411
[Quine] p. 44Theorem 7.3spcgf 3495  spcgv 3500  spcimgf 3493
[Quine] p. 44Theorem 6.11spsbc 3693  spsbcd 3694
[Quine] p. 44Theorem 6.12elex 3416
[Quine] p. 44Theorem 6.13elab 3573  elabg 3571  elabgf 3568
[Quine] p. 44Theorem 6.14noel 4219
[Quine] p. 48Theorem 7.2snprc 4608
[Quine] p. 48Definition 7.1df-pr 4519  df-sn 4517
[Quine] p. 49Theorem 7.4snss 4674  snssg 4673
[Quine] p. 49Theorem 7.5prss 4708  prssg 4707
[Quine] p. 49Theorem 7.6prid1 4653  prid1g 4651  prid2 4654  prid2g 4652  snid 4552  snidg 4550
[Quine] p. 51Theorem 7.12snex 5298
[Quine] p. 51Theorem 7.13prex 5299
[Quine] p. 53Theorem 8.2unisn 4818  unisnALT 42084  unisng 4817
[Quine] p. 53Theorem 8.3uniun 4821
[Quine] p. 54Theorem 8.6elssuni 4828
[Quine] p. 54Theorem 8.7uni0 4826
[Quine] p. 56Theorem 8.17uniabio 6312
[Quine] p. 56Definition 8.18dfaiota2 44110  dfiota2 6298
[Quine] p. 57Theorem 8.19aiotaval 44119  iotaval 6313
[Quine] p. 57Theorem 8.22iotanul 6317
[Quine] p. 58Theorem 8.23iotaex 6319
[Quine] p. 58Definition 9.1df-op 4523
[Quine] p. 61Theorem 9.5opabid 5381  opabidw 5380  opelopab 5397  opelopaba 5391  opelopabaf 5399  opelopabf 5400  opelopabg 5393  opelopabga 5388  opelopabgf 5395  oprabid 7202  oprabidw 7201
[Quine] p. 64Definition 9.11df-xp 5531
[Quine] p. 64Definition 9.12df-cnv 5533
[Quine] p. 64Definition 9.15df-id 5429
[Quine] p. 65Theorem 10.3fun0 6404
[Quine] p. 65Theorem 10.4funi 6371
[Quine] p. 65Theorem 10.5funsn 6392  funsng 6390
[Quine] p. 65Definition 10.1df-fun 6341
[Quine] p. 65Definition 10.2args 5931  dffv4 6671
[Quine] p. 68Definition 10.11conventions 28337  df-fv 6347  fv2 6669
[Quine] p. 124Theorem 17.3nn0opth2 13724  nn0opth2i 13723  nn0opthi 13722  omopthi 8315
[Quine] p. 177Definition 25.2df-rdg 8075
[Quine] p. 232Equation icarddom 10054
[Quine] p. 284Axiom 39(vi)funimaex 6426  funimaexg 6425
[Quine] p. 331Axiom system NFru 3679
[ReedSimon] p. 36Definition (iii)ax-his3 29019
[ReedSimon] p. 63Exercise 4(a)df-dip 28636  polid 29094  polid2i 29092  polidi 29093
[ReedSimon] p. 63Exercise 4(b)df-ph 28748
[ReedSimon] p. 195Remarklnophm 29954  lnophmi 29953
[Retherford] p. 49Exercise 1(i)leopadd 30067
[Retherford] p. 49Exercise 1(ii)leopmul 30069  leopmuli 30068
[Retherford] p. 49Exercise 1(iv)leoptr 30072
[Retherford] p. 49Definition VI.1df-leop 29787  leoppos 30061
[Retherford] p. 49Exercise 1(iii)leoptri 30071
[Retherford] p. 49Definition of operator orderingleop3 30060
[Roman] p. 4Definitiondf-dmat 21241  df-dmatalt 45273
[Roman] p. 18Part Preliminariesdf-rng0 44967
[Roman] p. 19Part Preliminariesdf-ring 19418
[Roman] p. 46Theorem 1.6isldepslvec2 45360
[Roman] p. 112Noteisldepslvec2 45360  ldepsnlinc 45383  zlmodzxznm 45372
[Roman] p. 112Examplezlmodzxzequa 45371  zlmodzxzequap 45374  zlmodzxzldep 45379
[Roman] p. 170Theorem 7.8cayleyhamilton 21641
[Rosenlicht] p. 80Theoremheicant 35435
[Rosser] p. 281Definitiondf-op 4523
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 32195
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 32196
[Rotman] p. 28Remarkpgrpgt2nabl 45236  pmtr3ncom 18721
[Rotman] p. 31Theorem 3.4symggen2 18717
[Rotman] p. 42Theorem 3.15cayley 18660  cayleyth 18661
[Rudin] p. 164Equation 27efcan 15541
[Rudin] p. 164Equation 30efzval 15547
[Rudin] p. 167Equation 48absefi 15641
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1778
[Sanford] p. 39Rule 4mptxor 1776
[Sanford] p. 40Rule 1mptnan 1775
[Schechter] p. 51Definition of antisymmetryintasym 5949
[Schechter] p. 51Definition of irreflexivityintirr 5952
[Schechter] p. 51Definition of symmetrycnvsym 5948
[Schechter] p. 51Definition of transitivitycotr 5946
[Schechter] p. 78Definition of Moore collection of setsdf-mre 16960
[Schechter] p. 79Definition of Moore closuredf-mrc 16961
[Schechter] p. 82Section 4.5df-mrc 16961
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 16963
[Schechter] p. 139Definition AC3dfac9 9636
[Schechter] p. 141Definition (MC)dfac11 40459
[Schechter] p. 149Axiom DC1ax-dc 9946  axdc3 9954
[Schechter] p. 187Definition of ring with unitisring 19420  isrngo 35678
[Schechter] p. 276Remark 11.6.espan0 29477
[Schechter] p. 276Definition of spandf-span 29244  spanval 29268
[Schechter] p. 428Definition 15.35bastop1 21744
[Schwabhauser] p. 10Axiom A1axcgrrflx 26860  axtgcgrrflx 26408
[Schwabhauser] p. 10Axiom A2axcgrtr 26861
[Schwabhauser] p. 10Axiom A3axcgrid 26862  axtgcgrid 26409
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 26394
[Schwabhauser] p. 11Axiom A4axsegcon 26873  axtgsegcon 26410  df-trkgcb 26396
[Schwabhauser] p. 11Axiom A5ax5seg 26884  axtg5seg 26411  df-trkgcb 26396
[Schwabhauser] p. 11Axiom A6axbtwnid 26885  axtgbtwnid 26412  df-trkgb 26395
[Schwabhauser] p. 12Axiom A7axpasch 26887  axtgpasch 26413  df-trkgb 26395
[Schwabhauser] p. 12Axiom A8axlowdim2 26906  df-trkg2d 32215
[Schwabhauser] p. 13Axiom A8axtglowdim2 26416
[Schwabhauser] p. 13Axiom A9axtgupdim2 26417  df-trkg2d 32215
[Schwabhauser] p. 13Axiom A10axeuclid 26909  axtgeucl 26418  df-trkge 26397
[Schwabhauser] p. 13Axiom A11axcont 26922  axtgcont 26415  axtgcont1 26414  df-trkgb 26395
[Schwabhauser] p. 27Theorem 2.1cgrrflx 33927
[Schwabhauser] p. 27Theorem 2.2cgrcomim 33929
[Schwabhauser] p. 27Theorem 2.3cgrtr 33932
[Schwabhauser] p. 27Theorem 2.4cgrcoml 33936
[Schwabhauser] p. 27Theorem 2.5cgrcomr 33937  tgcgrcomimp 26423  tgcgrcoml 26425  tgcgrcomr 26424
[Schwabhauser] p. 28Theorem 2.8cgrtriv 33942  tgcgrtriv 26430
[Schwabhauser] p. 28Theorem 2.105segofs 33946  tg5segofs 32223
[Schwabhauser] p. 28Definition 2.10df-afs 32220  df-ofs 33923
[Schwabhauser] p. 29Theorem 2.11cgrextend 33948  tgcgrextend 26431
[Schwabhauser] p. 29Theorem 2.12segconeq 33950  tgsegconeq 26432
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 33962  btwntriv2 33952  tgbtwntriv2 26433
[Schwabhauser] p. 30Theorem 3.2btwncomim 33953  tgbtwncom 26434
[Schwabhauser] p. 30Theorem 3.3btwntriv1 33956  tgbtwntriv1 26437
[Schwabhauser] p. 30Theorem 3.4btwnswapid 33957  tgbtwnswapid 26438
[Schwabhauser] p. 30Theorem 3.5btwnexch2 33963  btwnintr 33959  tgbtwnexch2 26442  tgbtwnintr 26439
[Schwabhauser] p. 30Theorem 3.6btwnexch 33965  btwnexch3 33960  tgbtwnexch 26444  tgbtwnexch3 26440
[Schwabhauser] p. 30Theorem 3.7btwnouttr 33964  tgbtwnouttr 26443  tgbtwnouttr2 26441
[Schwabhauser] p. 32Theorem 3.13axlowdim1 26905
[Schwabhauser] p. 32Theorem 3.14btwndiff 33967  tgbtwndiff 26452
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 26445  trisegint 33968
[Schwabhauser] p. 34Theorem 4.2ifscgr 33984  tgifscgr 26454
[Schwabhauser] p. 34Theorem 4.11colcom 26504  colrot1 26505  colrot2 26506  lncom 26568  lnrot1 26569  lnrot2 26570
[Schwabhauser] p. 34Definition 4.1df-ifs 33980
[Schwabhauser] p. 35Theorem 4.3cgrsub 33985  tgcgrsub 26455
[Schwabhauser] p. 35Theorem 4.5cgrxfr 33995  tgcgrxfr 26464
[Schwabhauser] p. 35Statement 4.4ercgrg 26463
[Schwabhauser] p. 35Definition 4.4df-cgr3 33981  df-cgrg 26457
[Schwabhauser] p. 35Definition instead (givendf-cgrg 26457
[Schwabhauser] p. 36Theorem 4.6btwnxfr 33996  tgbtwnxfr 26476
[Schwabhauser] p. 36Theorem 4.11colinearperm1 34002  colinearperm2 34004  colinearperm3 34003  colinearperm4 34005  colinearperm5 34006
[Schwabhauser] p. 36Definition 4.8df-ismt 26479
[Schwabhauser] p. 36Definition 4.10df-colinear 33979  tgellng 26499  tglng 26492
[Schwabhauser] p. 37Theorem 4.12colineartriv1 34007
[Schwabhauser] p. 37Theorem 4.13colinearxfr 34015  lnxfr 26512
[Schwabhauser] p. 37Theorem 4.14lineext 34016  lnext 26513
[Schwabhauser] p. 37Theorem 4.16fscgr 34020  tgfscgr 26514
[Schwabhauser] p. 37Theorem 4.17linecgr 34021  lncgr 26515
[Schwabhauser] p. 37Definition 4.15df-fs 33982
[Schwabhauser] p. 38Theorem 4.18lineid 34023  lnid 26516
[Schwabhauser] p. 38Theorem 4.19idinside 34024  tgidinside 26517
[Schwabhauser] p. 39Theorem 5.1btwnconn1 34041  tgbtwnconn1 26521
[Schwabhauser] p. 41Theorem 5.2btwnconn2 34042  tgbtwnconn2 26522
[Schwabhauser] p. 41Theorem 5.3btwnconn3 34043  tgbtwnconn3 26523
[Schwabhauser] p. 41Theorem 5.5brsegle2 34049
[Schwabhauser] p. 41Definition 5.4df-segle 34047  legov 26531
[Schwabhauser] p. 41Definition 5.5legov2 26532
[Schwabhauser] p. 42Remark 5.13legso 26545
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 34050
[Schwabhauser] p. 42Theorem 5.7seglerflx 34052
[Schwabhauser] p. 42Theorem 5.8segletr 34054
[Schwabhauser] p. 42Theorem 5.9segleantisym 34055
[Schwabhauser] p. 42Theorem 5.10seglelin 34056
[Schwabhauser] p. 42Theorem 5.11seglemin 34053
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 34058
[Schwabhauser] p. 42Proposition 5.7legid 26533
[Schwabhauser] p. 42Proposition 5.8legtrd 26535
[Schwabhauser] p. 42Proposition 5.9legtri3 26536
[Schwabhauser] p. 42Proposition 5.10legtrid 26537
[Schwabhauser] p. 42Proposition 5.11leg0 26538
[Schwabhauser] p. 43Theorem 6.2btwnoutside 34065
[Schwabhauser] p. 43Theorem 6.3broutsideof3 34066
[Schwabhauser] p. 43Theorem 6.4broutsideof 34061  df-outsideof 34060
[Schwabhauser] p. 43Definition 6.1broutsideof2 34062  ishlg 26548
[Schwabhauser] p. 44Theorem 6.4hlln 26553
[Schwabhauser] p. 44Theorem 6.5hlid 26555  outsideofrflx 34067
[Schwabhauser] p. 44Theorem 6.6hlcomb 26549  hlcomd 26550  outsideofcom 34068
[Schwabhauser] p. 44Theorem 6.7hltr 26556  outsideoftr 34069
[Schwabhauser] p. 44Theorem 6.11hlcgreu 26564  outsideofeu 34071
[Schwabhauser] p. 44Definition 6.8df-ray 34078
[Schwabhauser] p. 45Part 2df-lines2 34079
[Schwabhauser] p. 45Theorem 6.13outsidele 34072
[Schwabhauser] p. 45Theorem 6.15lineunray 34087
[Schwabhauser] p. 45Theorem 6.16lineelsb2 34088  tglineelsb2 26578
[Schwabhauser] p. 45Theorem 6.17linecom 34090  linerflx1 34089  linerflx2 34091  tglinecom 26581  tglinerflx1 26579  tglinerflx2 26580
[Schwabhauser] p. 45Theorem 6.18linethru 34093  tglinethru 26582
[Schwabhauser] p. 45Definition 6.14df-line2 34077  tglng 26492
[Schwabhauser] p. 45Proposition 6.13legbtwn 26540
[Schwabhauser] p. 46Theorem 6.19linethrueu 34096  tglinethrueu 26585
[Schwabhauser] p. 46Theorem 6.21lineintmo 34097  tglineineq 26589  tglineinteq 26591  tglineintmo 26588
[Schwabhauser] p. 46Theorem 6.23colline 26595
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 26596
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 26597
[Schwabhauser] p. 49Theorem 7.3mirinv 26612
[Schwabhauser] p. 49Theorem 7.7mirmir 26608
[Schwabhauser] p. 49Theorem 7.8mirreu3 26600
[Schwabhauser] p. 49Definition 7.5df-mir 26599  ismir 26605  mirbtwn 26604  mircgr 26603  mirfv 26602  mirval 26601
[Schwabhauser] p. 50Theorem 7.8mirreu 26610
[Schwabhauser] p. 50Theorem 7.9mireq 26611
[Schwabhauser] p. 50Theorem 7.10mirinv 26612
[Schwabhauser] p. 50Theorem 7.11mirf1o 26615
[Schwabhauser] p. 50Theorem 7.13miriso 26616
[Schwabhauser] p. 51Theorem 7.14mirmot 26621
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 26618  mirbtwni 26617
[Schwabhauser] p. 51Theorem 7.16mircgrs 26619
[Schwabhauser] p. 51Theorem 7.17miduniq 26631
[Schwabhauser] p. 52Lemma 7.21symquadlem 26635
[Schwabhauser] p. 52Theorem 7.18miduniq1 26632
[Schwabhauser] p. 52Theorem 7.19miduniq2 26633
[Schwabhauser] p. 52Theorem 7.20colmid 26634
[Schwabhauser] p. 53Lemma 7.22krippen 26637
[Schwabhauser] p. 55Lemma 7.25midexlem 26638
[Schwabhauser] p. 57Theorem 8.2ragcom 26644
[Schwabhauser] p. 57Definition 8.1df-rag 26640  israg 26643
[Schwabhauser] p. 58Theorem 8.3ragcol 26645
[Schwabhauser] p. 58Theorem 8.4ragmir 26646
[Schwabhauser] p. 58Theorem 8.5ragtrivb 26648
[Schwabhauser] p. 58Theorem 8.6ragflat2 26649
[Schwabhauser] p. 58Theorem 8.7ragflat 26650
[Schwabhauser] p. 58Theorem 8.8ragtriva 26651
[Schwabhauser] p. 58Theorem 8.9ragflat3 26652  ragncol 26655
[Schwabhauser] p. 58Theorem 8.10ragcgr 26653
[Schwabhauser] p. 59Theorem 8.12perpcom 26659
[Schwabhauser] p. 59Theorem 8.13ragperp 26663
[Schwabhauser] p. 59Theorem 8.14perpneq 26660
[Schwabhauser] p. 59Definition 8.11df-perpg 26642  isperp 26658
[Schwabhauser] p. 59Definition 8.13isperp2 26661
[Schwabhauser] p. 60Theorem 8.18foot 26668
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 26676  colperpexlem2 26677
[Schwabhauser] p. 63Theorem 8.21colperpex 26679  colperpexlem3 26678
[Schwabhauser] p. 64Theorem 8.22mideu 26684  midex 26683
[Schwabhauser] p. 66Lemma 8.24opphllem 26681
[Schwabhauser] p. 67Theorem 9.2oppcom 26690
[Schwabhauser] p. 67Definition 9.1islnopp 26685
[Schwabhauser] p. 68Lemma 9.3opphllem2 26694
[Schwabhauser] p. 68Lemma 9.4opphllem5 26697  opphllem6 26698
[Schwabhauser] p. 69Theorem 9.5opphl 26700
[Schwabhauser] p. 69Theorem 9.6axtgpasch 26413
[Schwabhauser] p. 70Theorem 9.6outpasch 26701
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 26709
[Schwabhauser] p. 71Definition 9.7df-hpg 26704  hpgbr 26706
[Schwabhauser] p. 72Lemma 9.10hpgerlem 26711
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 26710
[Schwabhauser] p. 72Theorem 9.11hpgid 26712
[Schwabhauser] p. 72Theorem 9.12hpgcom 26713
[Schwabhauser] p. 72Theorem 9.13hpgtr 26714
[Schwabhauser] p. 73Theorem 9.18colopp 26715
[Schwabhauser] p. 73Theorem 9.19colhp 26716
[Schwabhauser] p. 88Theorem 10.2lmieu 26730
[Schwabhauser] p. 88Definition 10.1df-mid 26720
[Schwabhauser] p. 89Theorem 10.4lmicom 26734
[Schwabhauser] p. 89Theorem 10.5lmilmi 26735
[Schwabhauser] p. 89Theorem 10.6lmireu 26736
[Schwabhauser] p. 89Theorem 10.7lmieq 26737
[Schwabhauser] p. 89Theorem 10.8lmiinv 26738
[Schwabhauser] p. 89Theorem 10.9lmif1o 26741
[Schwabhauser] p. 89Theorem 10.10lmiiso 26743
[Schwabhauser] p. 89Definition 10.3df-lmi 26721
[Schwabhauser] p. 90Theorem 10.11lmimot 26744
[Schwabhauser] p. 91Theorem 10.12hypcgr 26747
[Schwabhauser] p. 92Theorem 10.14lmiopp 26748
[Schwabhauser] p. 92Theorem 10.15lnperpex 26749
[Schwabhauser] p. 92Theorem 10.16trgcopy 26750  trgcopyeu 26752
[Schwabhauser] p. 95Definition 11.2dfcgra2 26776
[Schwabhauser] p. 95Definition 11.3iscgra 26755
[Schwabhauser] p. 95Proposition 11.4cgracgr 26764
[Schwabhauser] p. 95Proposition 11.10cgrahl1 26762  cgrahl2 26763
[Schwabhauser] p. 96Theorem 11.6cgraid 26765
[Schwabhauser] p. 96Theorem 11.9cgraswap 26766
[Schwabhauser] p. 97Theorem 11.7cgracom 26768
[Schwabhauser] p. 97Theorem 11.8cgratr 26769
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 26772  cgrahl 26773
[Schwabhauser] p. 98Theorem 11.13sacgr 26777
[Schwabhauser] p. 98Theorem 11.14oacgr 26778
[Schwabhauser] p. 98Theorem 11.15acopy 26779  acopyeu 26780
[Schwabhauser] p. 101Theorem 11.24inagswap 26787
[Schwabhauser] p. 101Theorem 11.25inaghl 26791
[Schwabhauser] p. 101Definition 11.23isinag 26784
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 26799
[Schwabhauser] p. 102Definition 11.27df-leag 26792  isleag 26793
[Schwabhauser] p. 107Theorem 11.49tgsas 26801  tgsas1 26800  tgsas2 26802  tgsas3 26803
[Schwabhauser] p. 108Theorem 11.50tgasa 26805  tgasa1 26804
[Schwabhauser] p. 109Theorem 11.51tgsss1 26806  tgsss2 26807  tgsss3 26808
[Shapiro] p. 230Theorem 6.5.1dchrhash 26007  dchrsum 26005  dchrsum2 26004  sumdchr 26008
[Shapiro] p. 232Theorem 6.5.2dchr2sum 26009  sum2dchr 26010
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19307  ablfacrp2 19308
[Shapiro], p. 328Equation 9.2.4vmasum 25952
[Shapiro], p. 329Equation 9.2.7logfac2 25953
[Shapiro], p. 329Equation 9.2.9logfacrlim 25960
[Shapiro], p. 331Equation 9.2.13vmadivsum 26218
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 26221
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 26275  vmalogdivsum2 26274
[Shapiro], p. 375Theorem 9.4.1dirith 26265  dirith2 26264
[Shapiro], p. 375Equation 9.4.3rplogsum 26263  rpvmasum 26262  rpvmasum2 26248
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 26223
[Shapiro], p. 376Equation 9.4.8dchrvmasum 26261
[Shapiro], p. 377Lemma 9.4.1dchrisum 26228  dchrisumlem1 26225  dchrisumlem2 26226  dchrisumlem3 26227  dchrisumlema 26224
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 26231
[Shapiro], p. 379Equation 9.4.16dchrmusum 26260  dchrmusumlem 26258  dchrvmasumlem 26259
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 26230
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 26232
[Shapiro], p. 382Lemma 9.4.4dchrisum0 26256  dchrisum0re 26249  dchrisumn0 26257
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 26242
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 26246
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 26247
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 26302  pntrsumbnd2 26303  pntrsumo1 26301
[Shapiro], p. 405Equation 10.2.1mudivsum 26266
[Shapiro], p. 406Equation 10.2.6mulogsum 26268
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 26270
[Shapiro], p. 407Equation 10.2.8mulog2sum 26273
[Shapiro], p. 418Equation 10.4.6logsqvma 26278
[Shapiro], p. 418Equation 10.4.8logsqvma2 26279
[Shapiro], p. 419Equation 10.4.10selberg 26284
[Shapiro], p. 420Equation 10.4.12selberg2lem 26286
[Shapiro], p. 420Equation 10.4.14selberg2 26287
[Shapiro], p. 422Equation 10.6.7selberg3 26295
[Shapiro], p. 422Equation 10.4.20selberg4lem1 26296
[Shapiro], p. 422Equation 10.4.21selberg3lem1 26293  selberg3lem2 26294
[Shapiro], p. 422Equation 10.4.23selberg4 26297
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 26291
[Shapiro], p. 428Equation 10.6.2selbergr 26304
[Shapiro], p. 429Equation 10.6.8selberg3r 26305
[Shapiro], p. 430Equation 10.6.11selberg4r 26306
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 26320
[Shapiro], p. 434Equation 10.6.27pntlema 26332  pntlemb 26333  pntlemc 26331  pntlemd 26330  pntlemg 26334
[Shapiro], p. 435Equation 10.6.29pntlema 26332
[Shapiro], p. 436Lemma 10.6.1pntpbnd 26324
[Shapiro], p. 436Lemma 10.6.2pntibnd 26329
[Shapiro], p. 436Equation 10.6.34pntlema 26332
[Shapiro], p. 436Equation 10.6.35pntlem3 26345  pntleml 26347
[Stoll] p. 13Definition corresponds to dfsymdif3 4187
[Stoll] p. 16Exercise 4.40dif 4290  dif0 4261
[Stoll] p. 16Exercise 4.8difdifdir 4378
[Stoll] p. 17Theorem 5.1(5)unvdif 4364
[Stoll] p. 19Theorem 5.2(13)undm 4178
[Stoll] p. 19Theorem 5.2(13')indm 4179
[Stoll] p. 20Remarkinvdif 4159
[Stoll] p. 25Definition of ordered tripledf-ot 4525
[Stoll] p. 43Definitionuniiun 4944
[Stoll] p. 44Definitionintiin 4945
[Stoll] p. 45Definitiondf-iin 4884
[Stoll] p. 45Definition indexed uniondf-iun 4883
[Stoll] p. 176Theorem 3.4(27)iman 405
[Stoll] p. 262Example 4.1dfsymdif3 4187
[Strang] p. 242Section 6.3expgrowth 41491
[Suppes] p. 22Theorem 2eq0 4232  eq0f 4229
[Suppes] p. 22Theorem 4eqss 3892  eqssd 3894  eqssi 3893
[Suppes] p. 23Theorem 5ss0 4287  ss0b 4286
[Suppes] p. 23Theorem 6sstr 3885  sstrALT2 41993
[Suppes] p. 23Theorem 7pssirr 3991
[Suppes] p. 23Theorem 8pssn2lp 3992
[Suppes] p. 23Theorem 9psstr 3995
[Suppes] p. 23Theorem 10pssss 3986
[Suppes] p. 25Theorem 12elin 3859  elun 4039
[Suppes] p. 26Theorem 15inidm 4109
[Suppes] p. 26Theorem 16in0 4280
[Suppes] p. 27Theorem 23unidm 4042
[Suppes] p. 27Theorem 24un0 4279
[Suppes] p. 27Theorem 25ssun1 4062
[Suppes] p. 27Theorem 26ssequn1 4070
[Suppes] p. 27Theorem 27unss 4074
[Suppes] p. 27Theorem 28indir 4166
[Suppes] p. 27Theorem 29undir 4167
[Suppes] p. 28Theorem 32difid 4259
[Suppes] p. 29Theorem 33difin 4152
[Suppes] p. 29Theorem 34indif 4160
[Suppes] p. 29Theorem 35undif1 4365
[Suppes] p. 29Theorem 36difun2 4370
[Suppes] p. 29Theorem 37difin0 4363
[Suppes] p. 29Theorem 38disjdif 4361
[Suppes] p. 29Theorem 39difundi 4170
[Suppes] p. 29Theorem 40difindi 4172
[Suppes] p. 30Theorem 41nalset 5181
[Suppes] p. 39Theorem 61uniss 4804
[Suppes] p. 39Theorem 65uniop 5372
[Suppes] p. 41Theorem 70intsn 4874
[Suppes] p. 42Theorem 71intpr 4870  intprg 4869
[Suppes] p. 42Theorem 73op1stb 5329
[Suppes] p. 42Theorem 78intun 4868
[Suppes] p. 44Definition 15(a)dfiun2 4919  dfiun2g 4917
[Suppes] p. 44Definition 15(b)dfiin2 4920
[Suppes] p. 47Theorem 86elpw 4492  elpw2 5213  elpw2g 5212  elpwg 4491  elpwgdedVD 42075
[Suppes] p. 47Theorem 87pwid 4512
[Suppes] p. 47Theorem 89pw0 4700
[Suppes] p. 48Theorem 90pwpw0 4701
[Suppes] p. 52Theorem 101xpss12 5540
[Suppes] p. 52Theorem 102xpindi 5676  xpindir 5677
[Suppes] p. 52Theorem 103xpundi 5591  xpundir 5592
[Suppes] p. 54Theorem 105elirrv 9133
[Suppes] p. 58Theorem 2relss 5627
[Suppes] p. 59Theorem 4eldm 5743  eldm2 5744  eldm2g 5742  eldmg 5741
[Suppes] p. 59Definition 3df-dm 5535
[Suppes] p. 60Theorem 6dmin 5754
[Suppes] p. 60Theorem 8rnun 5978
[Suppes] p. 60Theorem 9rnin 5979
[Suppes] p. 60Definition 4dfrn2 5731
[Suppes] p. 61Theorem 11brcnv 5725  brcnvg 5722
[Suppes] p. 62Equation 5elcnv 5719  elcnv2 5720
[Suppes] p. 62Theorem 12relcnv 5941
[Suppes] p. 62Theorem 15cnvin 5977
[Suppes] p. 62Theorem 16cnvun 5975
[Suppes] p. 63Definitiondftrrels2 36312
[Suppes] p. 63Theorem 20co02 6093
[Suppes] p. 63Theorem 21dmcoss 5814
[Suppes] p. 63Definition 7df-co 5534
[Suppes] p. 64Theorem 26cnvco 5728
[Suppes] p. 64Theorem 27coass 6098
[Suppes] p. 65Theorem 31resundi 5839
[Suppes] p. 65Theorem 34elima 5908  elima2 5909  elima3 5910  elimag 5907
[Suppes] p. 65Theorem 35imaundi 5982
[Suppes] p. 66Theorem 40dminss 5985
[Suppes] p. 66Theorem 41imainss 5986
[Suppes] p. 67Exercise 11cnvxp 5989
[Suppes] p. 81Definition 34dfec2 8323
[Suppes] p. 82Theorem 72elec 8364  elecALTV 36028  elecg 8363
[Suppes] p. 82Theorem 73eqvrelth 36347  erth 8369  erth2 8370
[Suppes] p. 83Theorem 74eqvreldisj 36350  erdisj 8372
[Suppes] p. 89Theorem 96map0b 8493
[Suppes] p. 89Theorem 97map0 8497  map0g 8494
[Suppes] p. 89Theorem 98mapsn 8498  mapsnd 8496
[Suppes] p. 89Theorem 99mapss 8499
[Suppes] p. 91Definition 12(ii)alephsuc 9568
[Suppes] p. 91Definition 12(iii)alephlim 9567
[Suppes] p. 92Theorem 1enref 8588  enrefg 8587
[Suppes] p. 92Theorem 2ensym 8604  ensymb 8603  ensymi 8605
[Suppes] p. 92Theorem 3entr 8607
[Suppes] p. 92Theorem 4unen 8644
[Suppes] p. 94Theorem 15endom 8582
[Suppes] p. 94Theorem 16ssdomg 8601
[Suppes] p. 94Theorem 17domtr 8608
[Suppes] p. 95Theorem 18sbth 8687
[Suppes] p. 97Theorem 23canth2 8720  canth2g 8721
[Suppes] p. 97Definition 3brsdom2 8691  df-sdom 8558  dfsdom2 8690
[Suppes] p. 97Theorem 21(i)sdomirr 8704
[Suppes] p. 97Theorem 22(i)domnsym 8693
[Suppes] p. 97Theorem 21(ii)sdomnsym 8692
[Suppes] p. 97Theorem 22(ii)domsdomtr 8702
[Suppes] p. 97Theorem 22(iv)brdom2 8585
[Suppes] p. 97Theorem 21(iii)sdomtr 8705
[Suppes] p. 97Theorem 22(iii)sdomdomtr 8700
[Suppes] p. 98Exercise 4fundmen 8630  fundmeng 8631
[Suppes] p. 98Exercise 6xpdom3 8664
[Suppes] p. 98Exercise 11sdomentr 8701
[Suppes] p. 104Theorem 37fofi 8883
[Suppes] p. 104Theorem 38pwfi 8776
[Suppes] p. 105Theorem 40pwfi 8776
[Suppes] p. 111Axiom for cardinal numberscarden 10051
[Suppes] p. 130Definition 3df-tr 5137
[Suppes] p. 132Theorem 9ssonuni 7520
[Suppes] p. 134Definition 6df-suc 6178
[Suppes] p. 136Theorem Schema 22findes 7633  finds 7629  finds1 7632  finds2 7631
[Suppes] p. 151Theorem 42isfinite 9188  isfinite2 8850  isfiniteg 8852  unbnn 8848
[Suppes] p. 162Definition 5df-ltnq 10418  df-ltpq 10410
[Suppes] p. 197Theorem Schema 4tfindes 7596  tfinds 7593  tfinds2 7597
[Suppes] p. 209Theorem 18oaord1 8208
[Suppes] p. 209Theorem 21oaword2 8210
[Suppes] p. 211Theorem 25oaass 8218
[Suppes] p. 225Definition 8iscard2 9478
[Suppes] p. 227Theorem 56ondomon 10063
[Suppes] p. 228Theorem 59harcard 9480
[Suppes] p. 228Definition 12(i)aleph0 9566
[Suppes] p. 228Theorem Schema 61onintss 6222
[Suppes] p. 228Theorem Schema 62onminesb 7532  onminsb 7533
[Suppes] p. 229Theorem 64alephval2 10072
[Suppes] p. 229Theorem 65alephcard 9570
[Suppes] p. 229Theorem 66alephord2i 9577
[Suppes] p. 229Theorem 67alephnbtwn 9571
[Suppes] p. 229Definition 12df-aleph 9442
[Suppes] p. 242Theorem 6weth 9995
[Suppes] p. 242Theorem 8entric 10057
[Suppes] p. 242Theorem 9carden 10051
[TakeutiZaring] p. 8Axiom 1ax-ext 2710
[TakeutiZaring] p. 13Definition 4.5df-cleq 2730
[TakeutiZaring] p. 13Proposition 4.6df-clel 2811
[TakeutiZaring] p. 13Proposition 4.9cvjust 2732
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2758
[TakeutiZaring] p. 14Definition 4.16df-oprab 7174
[TakeutiZaring] p. 14Proposition 4.14ru 3679
[TakeutiZaring] p. 15Axiom 2zfpair 5288
[TakeutiZaring] p. 15Exercise 1elpr 4539  elpr2 4541  elpr2g 4540  elprg 4537
[TakeutiZaring] p. 15Exercise 2elsn 4531  elsn2 4555  elsn2g 4554  elsng 4530  velsn 4532
[TakeutiZaring] p. 15Exercise 3elop 5325
[TakeutiZaring] p. 15Exercise 4sneq 4526  sneqr 4726
[TakeutiZaring] p. 15Definition 5.1dfpr2 4535  dfsn2 4529  dfsn2ALT 4536
[TakeutiZaring] p. 16Axiom 3uniex 7485
[TakeutiZaring] p. 16Exercise 6opth 5334
[TakeutiZaring] p. 16Exercise 7opex 5322
[TakeutiZaring] p. 16Exercise 8rext 5307
[TakeutiZaring] p. 16Corollary 5.8unex 7487  unexg 7490
[TakeutiZaring] p. 16Definition 5.3dftp2 4580
[TakeutiZaring] p. 16Definition 5.5df-uni 4797
[TakeutiZaring] p. 16Definition 5.6df-in 3850  df-un 3848
[TakeutiZaring] p. 16Proposition 5.7unipr 4814  uniprg 4813
[TakeutiZaring] p. 17Axiom 4vpwex 5244
[TakeutiZaring] p. 17Exercise 1eltp 4579
[TakeutiZaring] p. 17Exercise 5elsuc 6241  elsucg 6239  sstr2 3884
[TakeutiZaring] p. 17Exercise 6uncom 4043
[TakeutiZaring] p. 17Exercise 7incom 4091
[TakeutiZaring] p. 17Exercise 8unass 4056
[TakeutiZaring] p. 17Exercise 9inass 4110
[TakeutiZaring] p. 17Exercise 10indi 4164
[TakeutiZaring] p. 17Exercise 11undi 4165
[TakeutiZaring] p. 17Definition 5.9df-pss 3862  dfss2 3863
[TakeutiZaring] p. 17Definition 5.10df-pw 4490
[TakeutiZaring] p. 18Exercise 7unss2 4071
[TakeutiZaring] p. 18Exercise 9df-ss 3860  sseqin2 4106
[TakeutiZaring] p. 18Exercise 10ssid 3899
[TakeutiZaring] p. 18Exercise 12inss1 4119  inss2 4120
[TakeutiZaring] p. 18Exercise 13nss 3939
[TakeutiZaring] p. 18Exercise 15unieq 4807
[TakeutiZaring] p. 18Exercise 18sspwb 5308  sspwimp 42076  sspwimpALT 42083  sspwimpALT2 42086  sspwimpcf 42078
[TakeutiZaring] p. 18Exercise 19pweqb 5315
[TakeutiZaring] p. 19Axiom 5ax-rep 5154
[TakeutiZaring] p. 20Definitiondf-rab 3062
[TakeutiZaring] p. 20Corollary 5.160ex 5175
[TakeutiZaring] p. 20Definition 5.12df-dif 3846
[TakeutiZaring] p. 20Definition 5.14dfnul2 4214
[TakeutiZaring] p. 20Proposition 5.15difid 4259
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4235  n0f 4231  neq0 4234  neq0f 4230
[TakeutiZaring] p. 21Axiom 6zfreg 9132
[TakeutiZaring] p. 21Axiom 6'zfregs 9247
[TakeutiZaring] p. 21Theorem 5.22setind 9249
[TakeutiZaring] p. 21Definition 5.20df-v 3400
[TakeutiZaring] p. 21Proposition 5.21vprc 5183
[TakeutiZaring] p. 22Exercise 10ss 4285
[TakeutiZaring] p. 22Exercise 3ssex 5189  ssexg 5191
[TakeutiZaring] p. 22Exercise 4inex1 5185
[TakeutiZaring] p. 22Exercise 5ruv 9139
[TakeutiZaring] p. 22Exercise 6elirr 9134
[TakeutiZaring] p. 22Exercise 7ssdif0 4252
[TakeutiZaring] p. 22Exercise 11difdif 4021
[TakeutiZaring] p. 22Exercise 13undif3 4181  undif3VD 42040
[TakeutiZaring] p. 22Exercise 14difss 4022
[TakeutiZaring] p. 22Exercise 15sscon 4029
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3058
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3059
[TakeutiZaring] p. 23Proposition 6.2xpex 7494  xpexg 7491
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5532
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6410
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6584  fun11 6413
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6351  svrelfun 6411
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5730
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5732
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5537
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5538
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5534
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6026  dfrel2 6021
[TakeutiZaring] p. 25Exercise 3xpss 5541
[TakeutiZaring] p. 25Exercise 5relun 5655
[TakeutiZaring] p. 25Exercise 6reluni 5662
[TakeutiZaring] p. 25Exercise 9inxp 5675
[TakeutiZaring] p. 25Exercise 12relres 5854
[TakeutiZaring] p. 25Exercise 13opelres 5831  opelresi 5833
[TakeutiZaring] p. 25Exercise 14dmres 5847
[TakeutiZaring] p. 25Exercise 15resss 5850
[TakeutiZaring] p. 25Exercise 17resabs1 5855
[TakeutiZaring] p. 25Exercise 18funres 6381
[TakeutiZaring] p. 25Exercise 24relco 6077
[TakeutiZaring] p. 25Exercise 29funco 6379
[TakeutiZaring] p. 25Exercise 30f1co 6586
[TakeutiZaring] p. 26Definition 6.10eu2 2612
[TakeutiZaring] p. 26Definition 6.11conventions 28337  df-fv 6347  fv3 6692
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7656  cnvexg 7655
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7642  dmexg 7634
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7643  rnexg 7635
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 41610
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7651
[TakeutiZaring] p. 27Corollary 6.13fvex 6687
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 44199  tz6.12-1-afv2 44266  tz6.12-1 6696  tz6.12-afv 44198  tz6.12-afv2 44265  tz6.12 6697  tz6.12c-afv2 44267  tz6.12c 6699
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 44262  tz6.12-2 6663  tz6.12i-afv2 44268  tz6.12i 6700
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6342
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6343
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6345  wfo 6337
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6344  wf1 6336
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6346  wf1o 6338
[TakeutiZaring] p. 28Exercise 4eqfnfv 6809  eqfnfv2 6810  eqfnfv2f 6813
[TakeutiZaring] p. 28Exercise 5fvco 6766
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 6990
[TakeutiZaring] p. 28Proposition 6.17resfunexg 6988
[TakeutiZaring] p. 29Exercise 9funimaex 6426  funimaexg 6425
[TakeutiZaring] p. 29Definition 6.18df-br 5031
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5443
[TakeutiZaring] p. 30Definition 6.21dffr2 5489  dffr3 5936  eliniseg 5932  iniseg 5934
[TakeutiZaring] p. 30Definition 6.22df-eprel 5434
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5503  fr3nr 7513  frirr 5502
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5483
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7515
[TakeutiZaring] p. 31Exercise 1frss 5492
[TakeutiZaring] p. 31Exercise 4wess 5512
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6160  tz6.26i 6161  wefrc 5519  wereu2 5522
[TakeutiZaring] p. 32Theorem 6.27wfi 6162  wfii 6163
[TakeutiZaring] p. 32Definition 6.28df-isom 6348
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7095
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7096
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7102
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7103
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7104
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7108
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7115
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7117
[TakeutiZaring] p. 35Notationwtr 5136
[TakeutiZaring] p. 35Theorem 7.2trelpss 41611  tz7.2 5509
[TakeutiZaring] p. 35Definition 7.1dftr3 5140
[TakeutiZaring] p. 36Proposition 7.4ordwe 6185
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6193
[TakeutiZaring] p. 36Proposition 7.6ordelord 6194  ordelordALT 41695  ordelordALTVD 42025
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6200  ordelssne 6199
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6198
[TakeutiZaring] p. 37Proposition 7.9ordin 6202
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7522
[TakeutiZaring] p. 38Corollary 7.15ordsson 7523
[TakeutiZaring] p. 38Definition 7.11df-on 6176
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6204
[TakeutiZaring] p. 38Proposition 7.12onfrALT 41707  ordon 7517
[TakeutiZaring] p. 38Proposition 7.13onprc 7518
[TakeutiZaring] p. 39Theorem 7.17tfi 7587
[TakeutiZaring] p. 40Exercise 3ontr2 6219
[TakeutiZaring] p. 40Exercise 7dftr2 5138
[TakeutiZaring] p. 40Exercise 9onssmin 7531
[TakeutiZaring] p. 40Exercise 11unon 7565
[TakeutiZaring] p. 40Exercise 12ordun 6273
[TakeutiZaring] p. 40Exercise 14ordequn 6272
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7519
[TakeutiZaring] p. 40Proposition 7.20elssuni 4828
[TakeutiZaring] p. 41Definition 7.22df-suc 6178
[TakeutiZaring] p. 41Proposition 7.23sssucid 6249  sucidg 6250
[TakeutiZaring] p. 41Proposition 7.24suceloni 7547
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6263  ordnbtwn 6262
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7562
[TakeutiZaring] p. 42Exercise 1df-lim 6177
[TakeutiZaring] p. 42Exercise 4omssnlim 7613
[TakeutiZaring] p. 42Exercise 7ssnlim 7618
[TakeutiZaring] p. 42Exercise 8onsucssi 7575  ordelsuc 7554
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7556
[TakeutiZaring] p. 42Definition 7.27nlimon 7585
[TakeutiZaring] p. 42Definition 7.28dfom2 7601
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7620
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7621
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7622
[TakeutiZaring] p. 43Remarkomon 7610
[TakeutiZaring] p. 43Axiom 7inf3 9171  omex 9179
[TakeutiZaring] p. 43Theorem 7.32ordom 7608
[TakeutiZaring] p. 43Corollary 7.31find 7627
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7623
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7624
[TakeutiZaring] p. 44Exercise 1limomss 7604
[TakeutiZaring] p. 44Exercise 2int0 4850
[TakeutiZaring] p. 44Exercise 3trintss 5153
[TakeutiZaring] p. 44Exercise 4intss1 4851
[TakeutiZaring] p. 44Exercise 5intex 5205
[TakeutiZaring] p. 44Exercise 6oninton 7534
[TakeutiZaring] p. 44Exercise 11ordintdif 6221
[TakeutiZaring] p. 44Definition 7.35df-int 4837
[TakeutiZaring] p. 44Proposition 7.34noinfep 9196
[TakeutiZaring] p. 45Exercise 4onint 7529
[TakeutiZaring] p. 47Lemma 1tfrlem1 8041
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8062
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8063
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8064
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8071  tz7.44-2 8072  tz7.44-3 8073
[TakeutiZaring] p. 50Exercise 1smogt 8033
[TakeutiZaring] p. 50Exercise 3smoiso 8028
[TakeutiZaring] p. 50Definition 7.46df-smo 8012
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8110  tz7.49c 8111
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8108
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8107
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8109
[TakeutiZaring] p. 53Proposition 7.532eu5 2658
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9511
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9512
[TakeutiZaring] p. 56Definition 8.1oalim 8188  oasuc 8180
[TakeutiZaring] p. 57Remarktfindsg 7594
[TakeutiZaring] p. 57Proposition 8.2oacl 8191
[TakeutiZaring] p. 57Proposition 8.3oa0 8172  oa0r 8194
[TakeutiZaring] p. 57Proposition 8.16omcl 8192
[TakeutiZaring] p. 58Corollary 8.5oacan 8205
[TakeutiZaring] p. 58Proposition 8.4nnaord 8276  nnaordi 8275  oaord 8204  oaordi 8203
[TakeutiZaring] p. 59Proposition 8.6iunss2 4935  uniss2 4831
[TakeutiZaring] p. 59Proposition 8.7oawordri 8207
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8212  oawordex 8214
[TakeutiZaring] p. 59Proposition 8.9nnacl 8268
[TakeutiZaring] p. 59Proposition 8.10oaabs 8302
[TakeutiZaring] p. 60Remarkoancom 9187
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8217
[TakeutiZaring] p. 62Exercise 1nnarcl 8273
[TakeutiZaring] p. 62Exercise 5oaword1 8209
[TakeutiZaring] p. 62Definition 8.15om0x 8175  omlim 8189  omsuc 8182
[TakeutiZaring] p. 62Definition 8.15(a)om0 8173
[TakeutiZaring] p. 63Proposition 8.17nnecl 8270  nnmcl 8269
[TakeutiZaring] p. 63Proposition 8.19nnmord 8289  nnmordi 8288  omord 8225  omordi 8223
[TakeutiZaring] p. 63Proposition 8.20omcan 8226
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8293  omwordri 8229
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8195
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8199  om1r 8200
[TakeutiZaring] p. 64Proposition 8.22om00 8232
[TakeutiZaring] p. 64Proposition 8.23omordlim 8234
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8235
[TakeutiZaring] p. 64Proposition 8.25odi 8236
[TakeutiZaring] p. 65Theorem 8.26omass 8237
[TakeutiZaring] p. 67Definition 8.30nnesuc 8265  oe0 8178  oelim 8190  oesuc 8183  onesuc 8186
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8176
[TakeutiZaring] p. 67Proposition 8.32oen0 8243
[TakeutiZaring] p. 67Proposition 8.33oeordi 8244
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8177
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8202
[TakeutiZaring] p. 68Corollary 8.34oeord 8245
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8251
[TakeutiZaring] p. 68Proposition 8.35oewordri 8249
[TakeutiZaring] p. 68Proposition 8.37oeworde 8250
[TakeutiZaring] p. 69Proposition 8.41oeoa 8254
[TakeutiZaring] p. 70Proposition 8.42oeoe 8256
[TakeutiZaring] p. 73Theorem 9.1trcl 9243  tz9.1 9244
[TakeutiZaring] p. 76Definition 9.9df-r1 9266  r10 9270  r1lim 9274  r1limg 9273  r1suc 9272  r1sucg 9271
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9282  r1ord2 9283  r1ordg 9280
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9292
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9317  tz9.13 9293  tz9.13g 9294
[TakeutiZaring] p. 79Definition 9.14df-rank 9267  rankval 9318  rankvalb 9299  rankvalg 9319
[TakeutiZaring] p. 79Proposition 9.16rankel 9341  rankelb 9326
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9355  rankval3 9342  rankval3b 9328
[TakeutiZaring] p. 79Proposition 9.18rankonid 9331
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9297
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9336  rankr1c 9323  rankr1g 9334
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9337
[TakeutiZaring] p. 80Exercise 1rankss 9351  rankssb 9350
[TakeutiZaring] p. 80Exercise 2unbndrank 9344
[TakeutiZaring] p. 80Proposition 9.19bndrank 9343
[TakeutiZaring] p. 83Axiom of Choiceac4 9975  dfac3 9621
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9530  numth 9972  numth2 9971
[TakeutiZaring] p. 85Definition 10.4cardval 10046
[TakeutiZaring] p. 85Proposition 10.5cardid 10047  cardid2 9455
[TakeutiZaring] p. 85Proposition 10.9oncard 9462
[TakeutiZaring] p. 85Proposition 10.10carden 10051
[TakeutiZaring] p. 85Proposition 10.11cardidm 9461
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9446
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9467
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9459
[TakeutiZaring] p. 87Proposition 10.15pwen 8740
[TakeutiZaring] p. 88Exercise 1en0 8618
[TakeutiZaring] p. 88Exercise 7infensuc 8745
[TakeutiZaring] p. 89Exercise 10omxpen 8668
[TakeutiZaring] p. 90Corollary 10.23cardnn 9465
[TakeutiZaring] p. 90Definition 10.27alephiso 9598
[TakeutiZaring] p. 90Proposition 10.20nneneq 8750
[TakeutiZaring] p. 90Proposition 10.22onomeneq 8788
[TakeutiZaring] p. 90Proposition 10.26alephprc 9599
[TakeutiZaring] p. 90Corollary 10.21(1)php5 8755
[TakeutiZaring] p. 91Exercise 2alephle 9588
[TakeutiZaring] p. 91Exercise 3aleph0 9566
[TakeutiZaring] p. 91Exercise 4cardlim 9474
[TakeutiZaring] p. 91Exercise 7infpss 9717
[TakeutiZaring] p. 91Exercise 8infcntss 8866
[TakeutiZaring] p. 91Definition 10.29df-fin 8559  isfi 8579
[TakeutiZaring] p. 92Proposition 10.32onfin 8789
[TakeutiZaring] p. 92Proposition 10.34imadomg 10034
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8661
[TakeutiZaring] p. 93Proposition 10.35fodomb 10026
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 9685  unxpdom 8804
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9476  cardsdomelir 9475
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 8806
[TakeutiZaring] p. 94Proposition 10.39infxpen 9514
[TakeutiZaring] p. 95Definition 10.42df-map 8439
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10062  infxpidm2 9517
[TakeutiZaring] p. 95Proposition 10.41infdju 9708  infxp 9715
[TakeutiZaring] p. 96Proposition 10.44pw2en 8673  pw2f1o 8671
[TakeutiZaring] p. 96Proposition 10.45mapxpen 8733
[TakeutiZaring] p. 97Theorem 10.46ac6s3 9987
[TakeutiZaring] p. 98Theorem 10.46ac6c5 9982  ac6s5 9991
[TakeutiZaring] p. 98Theorem 10.47unidom 10043
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10044  uniimadomf 10045
[TakeutiZaring] p. 100Definition 11.1cfcof 9774
[TakeutiZaring] p. 101Proposition 11.7cofsmo 9769
[TakeutiZaring] p. 102Exercise 1cfle 9754
[TakeutiZaring] p. 102Exercise 2cf0 9751
[TakeutiZaring] p. 102Exercise 3cfsuc 9757
[TakeutiZaring] p. 102Exercise 4cfom 9764
[TakeutiZaring] p. 102Proposition 11.9coftr 9773
[TakeutiZaring] p. 103Theorem 11.15alephreg 10082
[TakeutiZaring] p. 103Proposition 11.11cardcf 9752
[TakeutiZaring] p. 103Proposition 11.13alephsing 9776
[TakeutiZaring] p. 104Corollary 11.17cardinfima 9597
[TakeutiZaring] p. 104Proposition 11.16carduniima 9596
[TakeutiZaring] p. 104Proposition 11.18alephfp 9608  alephfp2 9609
[TakeutiZaring] p. 106Theorem 11.20gchina 10199
[TakeutiZaring] p. 106Theorem 11.21mappwen 9612
[TakeutiZaring] p. 107Theorem 11.26konigth 10069
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10083
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10084
[Tarski] p. 67Axiom B5ax-c5 36520
[Tarski] p. 67Scheme B5sp 2184
[Tarski] p. 68Lemma 6avril1 28400  equid 2024
[Tarski] p. 69Lemma 7equcomi 2029
[Tarski] p. 70Lemma 14spim 2387  spime 2389  spimew 1979
[Tarski] p. 70Lemma 16ax-12 2179  ax-c15 36526  ax12i 1974
[Tarski] p. 70Lemmas 16 and 17sb6 2095
[Tarski] p. 75Axiom B7ax6v 1976
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1917  ax5ALT 36544
[Tarski], p. 75Scheme B8 of system S2ax-7 2020  ax-8 2116  ax-9 2124
[Tarski1999] p. 178Axiom 4axtgsegcon 26410
[Tarski1999] p. 178Axiom 5axtg5seg 26411
[Tarski1999] p. 179Axiom 7axtgpasch 26413
[Tarski1999] p. 180Axiom 7.1axtgpasch 26413
[Tarski1999] p. 185Axiom 11axtgcont1 26414
[Truss] p. 114Theorem 5.18ruc 15688
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 35439
[Viaclovsky8] p. 3Proposition 7ismblfin 35441
[Weierstrass] p. 272Definitiondf-mdet 21336  mdetuni 21373
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 903
[WhiteheadRussell] p. 96Axiom *1.3olc 867
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 868
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 919
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 967
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 192
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 137
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 35239
[WhiteheadRussell] p. 100Theorem *2.05frege5 40954  imim2 58  wl-luk-imim2 35234
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 44053  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2665  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 35237
[WhiteheadRussell] p. 101Theorem *2.11exmid 894
[WhiteheadRussell] p. 101Theorem *2.12notnot 144
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 897
[WhiteheadRussell] p. 102Theorem *2.14notnotr 132  notnotrALT2 42085  wl-luk-notnotr 35238
[WhiteheadRussell] p. 102Theorem *2.15con1 148
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 40984  axfrege28 40983  con3 156
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 866
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 924
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 35231
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 889
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 939
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 28338  pm2.27 42  wl-luk-pm2.27 35229
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 923
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 969
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 970
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 968
[WhiteheadRussell] p. 105Definition *2.33df-3or 1089
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 906
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 907
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 942
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 881
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 882
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 172  pm2.5g 171
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 194
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 883
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 884
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 885
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 175
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 176
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 850
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 851
[WhiteheadRussell] p. 107Theorem *2.55orel1 888
[WhiteheadRussell] p. 107Theorem *2.56orel2 890
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 195
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 899
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 940
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 941
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 196
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 891  pm2.67 892
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 179  pm2.521g 177  pm2.521g2 178
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 898
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 972
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 900
[WhiteheadRussell] p. 108Theorem *2.69looinv 206
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 973
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 974
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 933
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 931
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 971
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 975
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 932
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 991
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 473  pm3.2im 163
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 992
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 993
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 994
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 995
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 475
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 463
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 406
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 803
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 452
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 453
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 486  simplim 170
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 488  simprim 169
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 765
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 766
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 808
[WhiteheadRussell] p. 113Fact)pm3.45 625
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 810
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 496
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 497
[WhiteheadRussell] p. 113Theorem *3.44jao 960  pm3.44 959
[WhiteheadRussell] p. 113Theorem *3.47anim12 809
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 477
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 963
[WhiteheadRussell] p. 116Theorem *4.1con34b 319
[WhiteheadRussell] p. 117Theorem *4.2biid 264
[WhiteheadRussell] p. 117Theorem *4.11notbi 322
[WhiteheadRussell] p. 117Theorem *4.12con2bi 357
[WhiteheadRussell] p. 117Theorem *4.13notnotb 318
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 807
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 832
[WhiteheadRussell] p. 117Theorem *4.21bicom 225
[WhiteheadRussell] p. 117Theorem *4.22biantr 806  bitr 805
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 567
[WhiteheadRussell] p. 117Theorem *4.25oridm 904  pm4.25 905
[WhiteheadRussell] p. 118Theorem *4.3ancom 464
[WhiteheadRussell] p. 118Theorem *4.4andi 1007
[WhiteheadRussell] p. 118Theorem *4.31orcom 869
[WhiteheadRussell] p. 118Theorem *4.32anass 472
[WhiteheadRussell] p. 118Theorem *4.33orass 921
[WhiteheadRussell] p. 118Theorem *4.36anbi1 635
[WhiteheadRussell] p. 118Theorem *4.37orbi1 917
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 638
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 976
[WhiteheadRussell] p. 118Definition *4.34df-3an 1090
[WhiteheadRussell] p. 119Theorem *4.41ordi 1005
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1053
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1022
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 996
[WhiteheadRussell] p. 119Theorem *4.45orabs 998  pm4.45 997  pm4.45im 827
[WhiteheadRussell] p. 120Theorem *4.5anor 982
[WhiteheadRussell] p. 120Theorem *4.6imor 852
[WhiteheadRussell] p. 120Theorem *4.7anclb 549
[WhiteheadRussell] p. 120Theorem *4.51ianor 981
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 984
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 985
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 986
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 987
[WhiteheadRussell] p. 120Theorem *4.56ioran 983  pm4.56 988
[WhiteheadRussell] p. 120Theorem *4.57oran 989  pm4.57 990
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 408
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 855
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 401
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 848
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 409
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 849
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 402
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 561  pm4.71d 565  pm4.71i 563  pm4.71r 562  pm4.71rd 566  pm4.71ri 564
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 949
[WhiteheadRussell] p. 121Theorem *4.73iba 531
[WhiteheadRussell] p. 121Theorem *4.74biorf 936
[WhiteheadRussell] p. 121Theorem *4.76jcab 521  pm4.76 522
[WhiteheadRussell] p. 121Theorem *4.77jaob 961  pm4.77 962
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 934
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1003
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 396
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 397
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1023
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1024
[WhiteheadRussell] p. 122Theorem *4.84imbi1 351
[WhiteheadRussell] p. 122Theorem *4.85imbi2 352
[WhiteheadRussell] p. 122Theorem *4.86bibi1 355
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 392  impexp 454  pm4.87 842
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 823
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 944  pm5.11g 943
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 945
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 947
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 946
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1012
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1013
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1011
[WhiteheadRussell] p. 124Theorem *5.18nbbn 388  pm5.18 386
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 391
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 824
[WhiteheadRussell] p. 124Theorem *5.22xor 1014
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1049
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1050
[WhiteheadRussell] p. 124Theorem *5.25dfor2 901
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 576
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 393
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 365
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1001
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 953
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 830
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 577
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 835
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 825
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 833
[WhiteheadRussell] p. 125Theorem *5.41imdi 394  pm5.41 395
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 547
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 546
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1004
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1017
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 948
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1000
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1018
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1019
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1027
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 370
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 273
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1028
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 41514
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 41515
[WhiteheadRussell] p. 147Theorem *10.2219.26 1877
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 41516
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 41517
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 41518
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1900
[WhiteheadRussell] p. 151Theorem *10.301albitr 41519
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 41520
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 41521
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 41522
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 41523
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 41525
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 41526
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 41527
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 41524
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2100
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 41530
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 41531
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2080
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2165
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1835
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1836
[WhiteheadRussell] p. 161Theorem *11.319.21vv 41532
[WhiteheadRussell] p. 162Theorem *11.322alim 41533
[WhiteheadRussell] p. 162Theorem *11.332albi 41534
[WhiteheadRussell] p. 162Theorem *11.342exim 41535
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 41537
[WhiteheadRussell] p. 162Theorem *11.3412exbi 41536
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1894
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 41539
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 41540
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 41538
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1834
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 41541
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 41542
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1852
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 41543
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2349
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1867
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 41548
[WhiteheadRussell] p. 165Theorem *11.56aaanv 41544
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 41545
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 41546
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 41547
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 41552
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 41549
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 41550
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 41551
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 41553
[WhiteheadRussell] p. 175Definition *14.02df-eu 2570
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 41563  pm13.13b 41564
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 41565
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3015
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3016
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3564
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 41571
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 41572
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 41566
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 41710  pm13.193 41567
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 41568
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 41569
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 41570
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 41577
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 41576
[WhiteheadRussell] p. 184Definition *14.01iotasbc 41575
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3745
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 41578  pm14.122b 41579  pm14.122c 41580
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 41581  pm14.123b 41582  pm14.123c 41583
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 41585
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 41584
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 41586
[WhiteheadRussell] p. 190Theorem *14.22iota4 6320
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 41587
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6321
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 41588
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 41590
[WhiteheadRussell] p. 192Theorem *14.26eupick 2636  eupickbi 2639  sbaniota 41591
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 41589
[WhiteheadRussell] p. 192Theorem *14.271eubi 2585
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 41593
[WhiteheadRussell] p. 235Definition *30.01conventions 28337  df-fv 6347
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9503  pm54.43lem 9502
[Young] p. 141Definition of operator orderingleop2 30059
[Young] p. 142Example 12.2(i)0leop 30065  idleop 30066
[vandenDries] p. 42Lemma 61irrapx1 40222
[vandenDries] p. 43Theorem 62pellex 40229  pellexlem1 40223

This page was last updated on 9-Oct-2024.
Copyright terms: Public domain