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 17548
[Adamek] p. 21Condition 3.1(b)df-cat 17548
[Adamek] p. 22Example 3.3(1)df-setc 17962
[Adamek] p. 24Example 3.3(4.c)0cat 17569
[Adamek] p. 24Example 3.3(4.d)df-prstc 47073  prsthinc 47064
[Adamek] p. 24Example 3.3(4.e)df-mndtc 47094  df-mndtc 47094
[Adamek] p. 25Definition 3.5df-oppc 17592
[Adamek] p. 28Remark 3.9oppciso 17664
[Adamek] p. 28Remark 3.12invf1o 17652  invisoinvl 17673
[Adamek] p. 28Example 3.13idinv 17672  idiso 17671
[Adamek] p. 28Corollary 3.11inveq 17657
[Adamek] p. 28Definition 3.8df-inv 17631  df-iso 17632  dfiso2 17655
[Adamek] p. 28Proposition 3.10sectcan 17638
[Adamek] p. 29Remark 3.16cicer 17689
[Adamek] p. 29Definition 3.15cic 17682  df-cic 17679
[Adamek] p. 29Definition 3.17df-func 17744
[Adamek] p. 29Proposition 3.14(1)invinv 17653
[Adamek] p. 29Proposition 3.14(2)invco 17654  isoco 17660
[Adamek] p. 30Remark 3.19df-func 17744
[Adamek] p. 30Example 3.20(1)idfucl 17767
[Adamek] p. 32Proposition 3.21funciso 17760
[Adamek] p. 33Example 3.26(2)df-thinc 47030  prsthinc 47064  thincciso 47059
[Adamek] p. 33Example 3.26(3)df-mndtc 47094
[Adamek] p. 33Proposition 3.23cofucl 17774
[Adamek] p. 34Remark 3.28(2)catciso 17997
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18055
[Adamek] p. 34Definition 3.27(2)df-fth 17792
[Adamek] p. 34Definition 3.27(3)df-full 17791
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18055
[Adamek] p. 35Corollary 3.32ffthiso 17816
[Adamek] p. 35Proposition 3.30(c)cofth 17822
[Adamek] p. 35Proposition 3.30(d)cofull 17821
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18040
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18040
[Adamek] p. 39Definition 3.41funcoppc 17761
[Adamek] p. 39Definition 3.44.df-catc 17985
[Adamek] p. 39Proposition 3.43(c)fthoppc 17810
[Adamek] p. 39Proposition 3.43(d)fulloppc 17809
[Adamek] p. 40Remark 3.48catccat 17994
[Adamek] p. 40Definition 3.47df-catc 17985
[Adamek] p. 48Example 4.3(1.a)0subcat 17724
[Adamek] p. 48Example 4.3(1.b)catsubcat 17725
[Adamek] p. 48Definition 4.1(2)fullsubc 17736
[Adamek] p. 48Definition 4.1(a)df-subc 17695
[Adamek] p. 49Remark 4.4(2)ressffth 17825
[Adamek] p. 83Definition 6.1df-nat 17830
[Adamek] p. 87Remark 6.14(a)fuccocl 17853
[Adamek] p. 87Remark 6.14(b)fucass 17857
[Adamek] p. 87Definition 6.15df-fuc 17831
[Adamek] p. 88Remark 6.16fuccat 17859
[Adamek] p. 101Definition 7.1df-inito 17870
[Adamek] p. 101Example 7.2 (6)irinitoringc 46357
[Adamek] p. 102Definition 7.4df-termo 17871
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17898
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17902
[Adamek] p. 103Definition 7.7df-zeroo 17872
[Adamek] p. 103Example 7.9 (3)nzerooringczr 46360
[Adamek] p. 103Proposition 7.6termoeu1w 17905
[Adamek] p. 106Definition 7.19df-sect 17630
[Adamek] p. 185Section 10.67updjud 9870
[Adamek] p. 478Item Rngdf-ringc 46293
[AhoHopUll] p. 2Section 1.1df-bigo 46624
[AhoHopUll] p. 12Section 1.3df-blen 46646
[AhoHopUll] p. 318Section 9.1df-concat 14459  df-pfx 14559  df-substr 14529  df-word 14403  lencl 14421  wrd0 14427
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24072  df-nmoo 29687
[AkhiezerGlazman] p. 64Theoremhmopidmch 31095  hmopidmchi 31093
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 31143  pjcmul2i 31144
[AkhiezerGlazman] p. 72Theoremcnvunop 30860  unoplin 30862
[AkhiezerGlazman] p. 72Equation 2unopadj 30861  unopadj2 30880
[AkhiezerGlazman] p. 73Theoremelunop2 30955  lnopunii 30954
[AkhiezerGlazman] p. 80Proposition 1adjlnop 31028
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27246
[Alling] p. 184Axiom Bbdayfo 27025
[Alling] p. 184Axiom Osltso 27024
[Alling] p. 184Axiom SDnodense 27040
[Alling] p. 185Lemma 0nocvxmin 27118
[Alling] p. 185Theoremconway 27138
[Alling] p. 185Axiom FEnoeta 27091
[Alling] p. 186Theorem 4slerec 27158
[Alling], p. 2Definitionrp-brsslt 41685
[Alling], p. 3Notenla0001 41688  nla0002 41686  nla0003 41687
[Apostol] p. 18Theorem I.1addcan 11339  addcan2d 11359  addcan2i 11349  addcand 11358  addcani 11348
[Apostol] p. 18Theorem I.2negeu 11391
[Apostol] p. 18Theorem I.3negsub 11449  negsubd 11518  negsubi 11479
[Apostol] p. 18Theorem I.4negneg 11451  negnegd 11503  negnegi 11471
[Apostol] p. 18Theorem I.5subdi 11588  subdid 11611  subdii 11604  subdir 11589  subdird 11612  subdiri 11605
[Apostol] p. 18Theorem I.6mul01 11334  mul01d 11354  mul01i 11345  mul02 11333  mul02d 11353  mul02i 11344
[Apostol] p. 18Theorem I.7mulcan 11792  mulcan2d 11789  mulcand 11788  mulcani 11794
[Apostol] p. 18Theorem I.8receu 11800  xreceu 31778
[Apostol] p. 18Theorem I.9divrec 11829  divrecd 11934  divreci 11900  divreczi 11893
[Apostol] p. 18Theorem I.10recrec 11852  recreci 11887
[Apostol] p. 18Theorem I.11mul0or 11795  mul0ord 11805  mul0ori 11803
[Apostol] p. 18Theorem I.12mul2neg 11594  mul2negd 11610  mul2negi 11603  mulneg1 11591  mulneg1d 11608  mulneg1i 11601
[Apostol] p. 18Theorem I.13divadddiv 11870  divadddivd 11975  divadddivi 11917
[Apostol] p. 18Theorem I.14divmuldiv 11855  divmuldivd 11972  divmuldivi 11915  rdivmuldivd 32071
[Apostol] p. 18Theorem I.15divdivdiv 11856  divdivdivd 11978  divdivdivi 11918
[Apostol] p. 20Axiom 7rpaddcl 12937  rpaddcld 12972  rpmulcl 12938  rpmulcld 12973
[Apostol] p. 20Axiom 8rpneg 12947
[Apostol] p. 20Axiom 90nrp 12950
[Apostol] p. 20Theorem I.17lttri 11281
[Apostol] p. 20Theorem I.18ltadd1d 11748  ltadd1dd 11766  ltadd1i 11709
[Apostol] p. 20Theorem I.19ltmul1 12005  ltmul1a 12004  ltmul1i 12073  ltmul1ii 12083  ltmul2 12006  ltmul2d 12999  ltmul2dd 13013  ltmul2i 12076
[Apostol] p. 20Theorem I.20msqgt0 11675  msqgt0d 11722  msqgt0i 11692
[Apostol] p. 20Theorem I.210lt1 11677
[Apostol] p. 20Theorem I.23lt0neg1 11661  lt0neg1d 11724  ltneg 11655  ltnegd 11733  ltnegi 11699
[Apostol] p. 20Theorem I.25lt2add 11640  lt2addd 11778  lt2addi 11717
[Apostol] p. 20Definition of positive numbersdf-rp 12916
[Apostol] p. 21Exercise 4recgt0 12001  recgt0d 12089  recgt0i 12060  recgt0ii 12061
[Apostol] p. 22Definition of integersdf-z 12500
[Apostol] p. 22Definition of positive integersdfnn3 12167
[Apostol] p. 22Definition of rationalsdf-q 12874
[Apostol] p. 24Theorem I.26supeu 9390
[Apostol] p. 26Theorem I.28nnunb 12409
[Apostol] p. 26Theorem I.29arch 12410  archd 43367
[Apostol] p. 28Exercise 2btwnz 12606
[Apostol] p. 28Exercise 3nnrecl 12411
[Apostol] p. 28Exercise 4rebtwnz 12872
[Apostol] p. 28Exercise 5zbtwnre 12871
[Apostol] p. 28Exercise 6qbtwnre 13118
[Apostol] p. 28Exercise 10(a)zeneo 16221  zneo 12586  zneoALTV 45851
[Apostol] p. 29Theorem I.35cxpsqrtth 26084  msqsqrtd 15325  resqrtth 15140  sqrtth 15249  sqrtthi 15255  sqsqrtd 15324
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12156
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12838
[Apostol] p. 361Remarkcrreczi 14131
[Apostol] p. 363Remarkabsgt0i 15284
[Apostol] p. 363Exampleabssubd 15338  abssubi 15288
[ApostolNT] p. 7Remarkfmtno0 45722  fmtno1 45723  fmtno2 45732  fmtno3 45733  fmtno4 45734  fmtno5fac 45764  fmtnofz04prm 45759
[ApostolNT] p. 7Definitiondf-fmtno 45710
[ApostolNT] p. 8Definitiondf-ppi 26449
[ApostolNT] p. 14Definitiondf-dvds 16137
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16152
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16176
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16171
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16165
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16167
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16153
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16154
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16159
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16193
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16195
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16197
[ApostolNT] p. 15Definitiondf-gcd 16375  dfgcd2 16427
[ApostolNT] p. 16Definitionisprm2 16558
[ApostolNT] p. 16Theorem 1.5coprmdvds 16529
[ApostolNT] p. 16Theorem 1.7prminf 16787
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16393
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16428
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16430
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16408
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16400
[ApostolNT] p. 17Theorem 1.8coprm 16587
[ApostolNT] p. 17Theorem 1.9euclemma 16589
[ApostolNT] p. 17Theorem 1.101arith2 16800
[ApostolNT] p. 18Theorem 1.13prmrec 16794
[ApostolNT] p. 19Theorem 1.14divalg 16285
[ApostolNT] p. 20Theorem 1.15eucalg 16463
[ApostolNT] p. 24Definitiondf-mu 26450
[ApostolNT] p. 25Definitiondf-phi 16638
[ApostolNT] p. 25Theorem 2.1musum 26540
[ApostolNT] p. 26Theorem 2.2phisum 16662
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16648
[ApostolNT] p. 28Theorem 2.5(c)phimul 16652
[ApostolNT] p. 32Definitiondf-vma 26447
[ApostolNT] p. 32Theorem 2.9muinv 26542
[ApostolNT] p. 32Theorem 2.10vmasum 26564
[ApostolNT] p. 38Remarkdf-sgm 26451
[ApostolNT] p. 38Definitiondf-sgm 26451
[ApostolNT] p. 75Definitiondf-chp 26448  df-cht 26446
[ApostolNT] p. 104Definitioncongr 16540
[ApostolNT] p. 106Remarkdvdsval3 16140
[ApostolNT] p. 106Definitionmoddvds 16147
[ApostolNT] p. 107Example 2mod2eq0even 16228
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16229
[ApostolNT] p. 107Example 4zmod1congr 13793
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13830
[ApostolNT] p. 107Theorem 5.2(c)modexp 14141
[ApostolNT] p. 108Theorem 5.3modmulconst 16170
[ApostolNT] p. 109Theorem 5.4cncongr1 16543
[ApostolNT] p. 109Theorem 5.6gcdmodi 16946
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16545
[ApostolNT] p. 113Theorem 5.17eulerth 16655
[ApostolNT] p. 113Theorem 5.18vfermltl 16673
[ApostolNT] p. 114Theorem 5.19fermltl 16656
[ApostolNT] p. 116Theorem 5.24wilthimp 26421
[ApostolNT] p. 179Definitiondf-lgs 26643  lgsprme0 26687
[ApostolNT] p. 180Example 11lgs 26688
[ApostolNT] p. 180Theorem 9.2lgsvalmod 26664
[ApostolNT] p. 180Theorem 9.3lgsdirprm 26679
[ApostolNT] p. 181Theorem 9.4m1lgs 26736
[ApostolNT] p. 181Theorem 9.52lgs 26755  2lgsoddprm 26764
[ApostolNT] p. 182Theorem 9.6gausslemma2d 26722
[ApostolNT] p. 185Theorem 9.8lgsquad 26731
[ApostolNT] p. 188Definitiondf-lgs 26643  lgs1 26689
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 26680
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 26682
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 26690
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 26691
[Baer] p. 40Property (b)mapdord 40101
[Baer] p. 40Property (c)mapd11 40102
[Baer] p. 40Property (e)mapdin 40125  mapdlsm 40127
[Baer] p. 40Property (f)mapd0 40128
[Baer] p. 40Definition of projectivitydf-mapd 40088  mapd1o 40111
[Baer] p. 41Property (g)mapdat 40130
[Baer] p. 44Part (1)mapdpg 40169
[Baer] p. 45Part (2)hdmap1eq 40264  mapdheq 40191  mapdheq2 40192  mapdheq2biN 40193
[Baer] p. 45Part (3)baerlem3 40176
[Baer] p. 46Part (4)mapdheq4 40195  mapdheq4lem 40194
[Baer] p. 46Part (5)baerlem5a 40177  baerlem5abmN 40181  baerlem5amN 40179  baerlem5b 40178  baerlem5bmN 40180
[Baer] p. 47Part (6)hdmap1l6 40284  hdmap1l6a 40272  hdmap1l6e 40277  hdmap1l6f 40278  hdmap1l6g 40279  hdmap1l6lem1 40270  hdmap1l6lem2 40271  mapdh6N 40210  mapdh6aN 40198  mapdh6eN 40203  mapdh6fN 40204  mapdh6gN 40205  mapdh6lem1N 40196  mapdh6lem2N 40197
[Baer] p. 48Part 9hdmapval 40291
[Baer] p. 48Part 10hdmap10 40303
[Baer] p. 48Part 11hdmapadd 40306
[Baer] p. 48Part (6)hdmap1l6h 40280  mapdh6hN 40206
[Baer] p. 48Part (7)mapdh75cN 40216  mapdh75d 40217  mapdh75e 40215  mapdh75fN 40218  mapdh7cN 40212  mapdh7dN 40213  mapdh7eN 40211  mapdh7fN 40214
[Baer] p. 48Part (8)mapdh8 40251  mapdh8a 40238  mapdh8aa 40239  mapdh8ab 40240  mapdh8ac 40241  mapdh8ad 40242  mapdh8b 40243  mapdh8c 40244  mapdh8d 40246  mapdh8d0N 40245  mapdh8e 40247  mapdh8g 40248  mapdh8i 40249  mapdh8j 40250
[Baer] p. 48Part (9)mapdh9a 40252
[Baer] p. 48Equation 10mapdhvmap 40232
[Baer] p. 49Part 12hdmap11 40311  hdmapeq0 40307  hdmapf1oN 40328  hdmapneg 40309  hdmaprnN 40327  hdmaprnlem1N 40312  hdmaprnlem3N 40313  hdmaprnlem3uN 40314  hdmaprnlem4N 40316  hdmaprnlem6N 40317  hdmaprnlem7N 40318  hdmaprnlem8N 40319  hdmaprnlem9N 40320  hdmapsub 40310
[Baer] p. 49Part 14hdmap14lem1 40331  hdmap14lem10 40340  hdmap14lem1a 40329  hdmap14lem2N 40332  hdmap14lem2a 40330  hdmap14lem3 40333  hdmap14lem8 40338  hdmap14lem9 40339
[Baer] p. 50Part 14hdmap14lem11 40341  hdmap14lem12 40342  hdmap14lem13 40343  hdmap14lem14 40344  hdmap14lem15 40345  hgmapval 40350
[Baer] p. 50Part 15hgmapadd 40357  hgmapmul 40358  hgmaprnlem2N 40360  hgmapvs 40354
[Baer] p. 50Part 16hgmaprnN 40364
[Baer] p. 110Lemma 1hdmapip0com 40380
[Baer] p. 110Line 27hdmapinvlem1 40381
[Baer] p. 110Line 28hdmapinvlem2 40382
[Baer] p. 110Line 30hdmapinvlem3 40383
[Baer] p. 110Part 1.2hdmapglem5 40385  hgmapvv 40389
[Baer] p. 110Proposition 1hdmapinvlem4 40384
[Baer] p. 111Line 10hgmapvvlem1 40386
[Baer] p. 111Line 15hdmapg 40393  hdmapglem7 40392
[Bauer], p. 483Theorem 1.22irrexpq 26085  2irrexpqALT 26150
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2567
[BellMachover] p. 460Notationdf-mo 2538
[BellMachover] p. 460Definitionmo3 2562
[BellMachover] p. 461Axiom Extax-ext 2707
[BellMachover] p. 462Theorem 1.1axextmo 2711
[BellMachover] p. 463Axiom Repaxrep5 5248
[BellMachover] p. 463Scheme Sepax-sep 5256
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 35535  bm1.3ii 5259
[BellMachover] p. 466Problemaxpow2 5322
[BellMachover] p. 466Axiom Powaxpow3 5323
[BellMachover] p. 466Axiom Unionaxun2 7674
[BellMachover] p. 468Definitiondf-ord 6320
[BellMachover] p. 469Theorem 2.2(i)ordirr 6335
[BellMachover] p. 469Theorem 2.2(iii)onelon 6342
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6337
[BellMachover] p. 471Definition of Ndf-om 7803
[BellMachover] p. 471Problem 2.5(ii)uniordint 7736
[BellMachover] p. 471Definition of Limdf-lim 6322
[BellMachover] p. 472Axiom Infzfinf2 9578
[BellMachover] p. 473Theorem 2.8limom 7818
[BellMachover] p. 477Equation 3.1df-r1 9700
[BellMachover] p. 478Definitionrankval2 9754
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9718  r1ord3g 9715
[BellMachover] p. 480Axiom Regzfreg 9531
[BellMachover] p. 488Axiom ACac5 10413  dfac4 10058
[BellMachover] p. 490Definition of alephalephval3 10046
[BeltramettiCassinelli] p. 98Remarkatlatmstc 37781
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 31295
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 31337  chirredi 31336
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 31325
[Beran] p. 3Definition of joinsshjval3 30296
[Beran] p. 39Theorem 2.3(i)cmcm2 30558  cmcm2i 30535  cmcm2ii 30540  cmt2N 37712
[Beran] p. 40Theorem 2.3(iii)lecm 30559  lecmi 30544  lecmii 30545
[Beran] p. 45Theorem 3.4cmcmlem 30533
[Beran] p. 49Theorem 4.2cm2j 30562  cm2ji 30567  cm2mi 30568
[Beran] p. 95Definitiondf-sh 30149  issh2 30151
[Beran] p. 95Lemma 3.1(S5)his5 30028
[Beran] p. 95Lemma 3.1(S6)his6 30041
[Beran] p. 95Lemma 3.1(S7)his7 30032
[Beran] p. 95Lemma 3.2(S8)ho01i 30770
[Beran] p. 95Lemma 3.2(S9)hoeq1 30772
[Beran] p. 95Lemma 3.2(S10)ho02i 30771
[Beran] p. 95Lemma 3.2(S11)hoeq2 30773
[Beran] p. 95Postulate (S1)ax-his1 30024  his1i 30042
[Beran] p. 95Postulate (S2)ax-his2 30025
[Beran] p. 95Postulate (S3)ax-his3 30026
[Beran] p. 95Postulate (S4)ax-his4 30027
[Beran] p. 96Definition of normdf-hnorm 29910  dfhnorm2 30064  normval 30066
[Beran] p. 96Definition for Cauchy sequencehcau 30126
[Beran] p. 96Definition of Cauchy sequencedf-hcau 29915
[Beran] p. 96Definition of complete subspaceisch3 30183
[Beran] p. 96Definition of convergedf-hlim 29914  hlimi 30130
[Beran] p. 97Theorem 3.3(i)norm-i-i 30075  norm-i 30071
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 30079  norm-ii 30080  normlem0 30051  normlem1 30052  normlem2 30053  normlem3 30054  normlem4 30055  normlem5 30056  normlem6 30057  normlem7 30058  normlem7tALT 30061
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 30081  norm-iii 30082
[Beran] p. 98Remark 3.4bcs 30123  bcsiALT 30121  bcsiHIL 30122
[Beran] p. 98Remark 3.4(B)normlem9at 30063  normpar 30097  normpari 30096
[Beran] p. 98Remark 3.4(C)normpyc 30088  normpyth 30087  normpythi 30084
[Beran] p. 99Remarklnfn0 30989  lnfn0i 30984  lnop0 30908  lnop0i 30912
[Beran] p. 99Theorem 3.5(i)nmcexi 30968  nmcfnex 30995  nmcfnexi 30993  nmcopex 30971  nmcopexi 30969
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 30996  nmcfnlbi 30994  nmcoplb 30972  nmcoplbi 30970
[Beran] p. 99Theorem 3.5(iii)lnfncon 30998  lnfnconi 30997  lnopcon 30977  lnopconi 30976
[Beran] p. 100Lemma 3.6normpar2i 30098
[Beran] p. 101Lemma 3.6norm3adifi 30095  norm3adifii 30090  norm3dif 30092  norm3difi 30089
[Beran] p. 102Theorem 3.7(i)chocunii 30243  pjhth 30335  pjhtheu 30336  pjpjhth 30367  pjpjhthi 30368  pjth 24803
[Beran] p. 102Theorem 3.7(ii)ococ 30348  ococi 30347
[Beran] p. 103Remark 3.8nlelchi 31003
[Beran] p. 104Theorem 3.9riesz3i 31004  riesz4 31006  riesz4i 31005
[Beran] p. 104Theorem 3.10cnlnadj 31021  cnlnadjeu 31020  cnlnadjeui 31019  cnlnadji 31018  cnlnadjlem1 31009  nmopadjlei 31030
[Beran] p. 106Theorem 3.11(i)adjeq0 31033
[Beran] p. 106Theorem 3.11(v)nmopadji 31032
[Beran] p. 106Theorem 3.11(ii)adjmul 31034
[Beran] p. 106Theorem 3.11(iv)adjadj 30878
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 31044  nmopcoadji 31043
[Beran] p. 106Theorem 3.11(iii)adjadd 31035
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 31045
[Beran] p. 106Theorem 3.11(viii)adjcoi 31042  pjadj2coi 31146  pjadjcoi 31103
[Beran] p. 107Definitiondf-ch 30163  isch2 30165
[Beran] p. 107Remark 3.12choccl 30248  isch3 30183  occl 30246  ocsh 30225  shoccl 30247  shocsh 30226
[Beran] p. 107Remark 3.12(B)ococin 30350
[Beran] p. 108Theorem 3.13chintcl 30274
[Beran] p. 109Property (i)pjadj2 31129  pjadj3 31130  pjadji 30627  pjadjii 30616
[Beran] p. 109Property (ii)pjidmco 31123  pjidmcoi 31119  pjidmi 30615
[Beran] p. 110Definition of projector orderingpjordi 31115
[Beran] p. 111Remarkho0val 30692  pjch1 30612
[Beran] p. 111Definitiondf-hfmul 30676  df-hfsum 30675  df-hodif 30674  df-homul 30673  df-hosum 30672
[Beran] p. 111Lemma 4.4(i)pjo 30613
[Beran] p. 111Lemma 4.4(ii)pjch 30636  pjchi 30374
[Beran] p. 111Lemma 4.4(iii)pjoc2 30381  pjoc2i 30380
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 30622
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 31107  pjssmii 30623
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 31106
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 31105
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 31110
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 31108  pjssge0ii 30624
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 31109  pjdifnormii 30625
[Bobzien] p. 116Statement T3stoic3 1778
[Bobzien] p. 117Statement T2stoic2a 1776
[Bobzien] p. 117Statement T4stoic4a 1779
[Bobzien] p. 117Conclusion the contradictorystoic1a 1774
[Bogachev] p. 16Definition 1.5df-oms 32892
[Bogachev] p. 17Lemma 1.5.4omssubadd 32900
[Bogachev] p. 17Example 1.5.2omsmon 32898
[Bogachev] p. 41Definition 1.11.2df-carsg 32902
[Bogachev] p. 42Theorem 1.11.4carsgsiga 32922
[Bogachev] p. 116Definition 2.3.1df-itgm 32953  df-sitm 32931
[Bogachev] p. 118Chapter 2.4.4df-itgm 32953
[Bogachev] p. 118Definition 2.4.1df-sitg 32930
[Bollobas] p. 1Section I.1df-edg 27999  isuhgrop 28021  isusgrop 28113  isuspgrop 28112
[Bollobas] p. 2Section I.1df-subgr 28216  uhgrspan1 28251  uhgrspansubgr 28239
[Bollobas] p. 3Definitionisomuspgr 46016
[Bollobas] p. 3Section I.1cusgrsize 28402  df-cusgr 28360  df-nbgr 28281  fusgrmaxsize 28412
[Bollobas] p. 4Definitiondf-upwlks 46026  df-wlks 28547
[Bollobas] p. 4Section I.1finsumvtxdg2size 28498  finsumvtxdgeven 28500  fusgr1th 28499  fusgrvtxdgonume 28502  vtxdgoddnumeven 28501
[Bollobas] p. 5Notationdf-pths 28664
[Bollobas] p. 5Definitiondf-crcts 28734  df-cycls 28735  df-trls 28640  df-wlkson 28548
[Bollobas] p. 7Section I.1df-ushgr 28010
[BourbakiAlg1] p. 1Definition 1df-clintop 46124  df-cllaw 46110  df-mgm 18497  df-mgm2 46143
[BourbakiAlg1] p. 4Definition 5df-assintop 46125  df-asslaw 46112  df-sgrp 18546  df-sgrp2 46145
[BourbakiAlg1] p. 7Definition 8df-cmgm2 46144  df-comlaw 46111
[BourbakiAlg1] p. 12Definition 2df-mnd 18557
[BourbakiAlg1] p. 92Definition 1df-ring 19966
[BourbakiAlg1] p. 93Section I.8.1df-rng 46163
[BourbakiEns] p. Proposition 8fcof1 7233  fcofo 7234
[BourbakiTop1] p. Remarkxnegmnf 13129  xnegpnf 13128
[BourbakiTop1] p. Remark rexneg 13130
[BourbakiTop1] p. Remark 3ust0 23571  ustfilxp 23564
[BourbakiTop1] p. Axiom GT'tgpsubcn 23441
[BourbakiTop1] p. Criterionishmeo 23110
[BourbakiTop1] p. Example 1cstucnd 23636  iducn 23635  snfil 23215
[BourbakiTop1] p. Example 2neifil 23231
[BourbakiTop1] p. Theorem 1cnextcn 23418
[BourbakiTop1] p. Theorem 2ucnextcn 23656
[BourbakiTop1] p. Theorem 3df-hcmp 32538
[BourbakiTop1] p. Paragraph 3infil 23214
[BourbakiTop1] p. Definition 1df-ucn 23628  df-ust 23552  filintn0 23212  filn0 23213  istgp 23428  ucnprima 23634
[BourbakiTop1] p. Definition 2df-cfilu 23639
[BourbakiTop1] p. Definition 3df-cusp 23650  df-usp 23609  df-utop 23583  trust 23581
[BourbakiTop1] p. Definition 6df-pcmp 32437
[BourbakiTop1] p. Property V_issnei2 22467
[BourbakiTop1] p. Theorem 1(d)iscncl 22620
[BourbakiTop1] p. Condition F_Iustssel 23557
[BourbakiTop1] p. Condition U_Iustdiag 23560
[BourbakiTop1] p. Property V_iiinnei 22476
[BourbakiTop1] p. Property V_ivneiptopreu 22484  neissex 22478
[BourbakiTop1] p. Proposition 1neips 22464  neiss 22460  ucncn 23637  ustund 23573  ustuqtop 23598
[BourbakiTop1] p. Proposition 2cnpco 22618  neiptopreu 22484  utop2nei 23602  utop3cls 23603
[BourbakiTop1] p. Proposition 3fmucnd 23644  uspreg 23626  utopreg 23604
[BourbakiTop1] p. Proposition 4imasncld 23042  imasncls 23043  imasnopn 23041
[BourbakiTop1] p. Proposition 9cnpflf2 23351
[BourbakiTop1] p. Condition F_IIustincl 23559
[BourbakiTop1] p. Condition U_IIustinvel 23561
[BourbakiTop1] p. Property V_iiielnei 22462
[BourbakiTop1] p. Proposition 11cnextucn 23655
[BourbakiTop1] p. Condition F_IIbustbasel 23558
[BourbakiTop1] p. Condition U_IIIustexhalf 23562
[BourbakiTop1] p. Definition C'''df-cmp 22738
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23197
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22243
[BourbakiTop2] p. 195Definition 1df-ldlf 32434
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 44293
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 44295  stoweid 44294
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 44232  stoweidlem10 44241  stoweidlem14 44245  stoweidlem15 44246  stoweidlem35 44266  stoweidlem36 44267  stoweidlem37 44268  stoweidlem38 44269  stoweidlem40 44271  stoweidlem41 44272  stoweidlem43 44274  stoweidlem44 44275  stoweidlem46 44277  stoweidlem5 44236  stoweidlem50 44281  stoweidlem52 44283  stoweidlem53 44284  stoweidlem55 44286  stoweidlem56 44287
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 44254  stoweidlem24 44255  stoweidlem27 44258  stoweidlem28 44259  stoweidlem30 44261
[BrosowskiDeutsh] p. 91Proofstoweidlem34 44265  stoweidlem59 44290  stoweidlem60 44291
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 44276  stoweidlem49 44280  stoweidlem7 44238
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 44262  stoweidlem39 44270  stoweidlem42 44273  stoweidlem48 44279  stoweidlem51 44282  stoweidlem54 44285  stoweidlem57 44288  stoweidlem58 44289
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 44256
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 44248
[BrosowskiDeutsh] p. 92Proofstoweidlem11 44242  stoweidlem13 44244  stoweidlem26 44257  stoweidlem61 44292
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 44249
[Bruck] p. 1Section I.1df-clintop 46124  df-mgm 18497  df-mgm2 46143
[Bruck] p. 23Section II.1df-sgrp 18546  df-sgrp2 46145
[Bruck] p. 28Theorem 3.2dfgrp3 18846
[ChoquetDD] p. 2Definition of mappingdf-mpt 5189
[Church] p. 129Section II.24df-ifp 1062  dfifp2 1063
[Clemente] p. 10Definition ITnatded 29347
[Clemente] p. 10Definition I` `m,nnatded 29347
[Clemente] p. 11Definition E=>m,nnatded 29347
[Clemente] p. 11Definition I=>m,nnatded 29347
[Clemente] p. 11Definition E` `(1)natded 29347
[Clemente] p. 11Definition E` `(2)natded 29347
[Clemente] p. 12Definition E` `m,n,pnatded 29347
[Clemente] p. 12Definition I` `n(1)natded 29347
[Clemente] p. 12Definition I` `n(2)natded 29347
[Clemente] p. 13Definition I` `m,n,pnatded 29347
[Clemente] p. 14Proof 5.11natded 29347
[Clemente] p. 14Definition E` `nnatded 29347
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 29349  ex-natded5.2 29348
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 29352  ex-natded5.3 29351
[Clemente] p. 18Theorem 5.5ex-natded5.5 29354
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 29356  ex-natded5.7 29355
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 29358  ex-natded5.8 29357
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 29360  ex-natded5.13 29359
[Clemente] p. 32Definition I` `nnatded 29347
[Clemente] p. 32Definition E` `m,n,p,anatded 29347
[Clemente] p. 32Definition E` `n,tnatded 29347
[Clemente] p. 32Definition I` `n,tnatded 29347
[Clemente] p. 43Theorem 9.20ex-natded9.20 29361
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 29362
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 29364  ex-natded9.26 29363
[Cohen] p. 301Remarkrelogoprlem 25946
[Cohen] p. 301Property 2relogmul 25947  relogmuld 25980
[Cohen] p. 301Property 3relogdiv 25948  relogdivd 25981
[Cohen] p. 301Property 4relogexp 25951
[Cohen] p. 301Property 1alog1 25941
[Cohen] p. 301Property 1bloge 25942
[Cohen4] p. 348Observationrelogbcxpb 26137
[Cohen4] p. 349Propertyrelogbf 26141
[Cohen4] p. 352Definitionelogb 26120
[Cohen4] p. 361Property 2relogbmul 26127
[Cohen4] p. 361Property 3logbrec 26132  relogbdiv 26129
[Cohen4] p. 361Property 4relogbreexp 26125
[Cohen4] p. 361Property 6relogbexp 26130
[Cohen4] p. 361Property 1(a)logbid1 26118
[Cohen4] p. 361Property 1(b)logb1 26119
[Cohen4] p. 367Propertylogbchbase 26121
[Cohen4] p. 377Property 2logblt 26134
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 32885  sxbrsigalem4 32887
[Cohn] p. 81Section II.5acsdomd 18446  acsinfd 18445  acsinfdimd 18447  acsmap2d 18444  acsmapd 18443
[Cohn] p. 143Example 5.1.1sxbrsiga 32890
[Connell] p. 57Definitiondf-scmat 21840  df-scmatalt 46470
[Conway] p. 4Definitionslerec 27158
[Conway] p. 5Definitionaddsval 27274  addsval2 27275  df-adds 27272  df-muls 34406  df-negs 27320
[Conway] p. 7Theorem0slt1s 27168
[Conway] p. 16Theorem 0(i)ssltright 27201
[Conway] p. 16Theorem 0(ii)ssltleft 27200
[Conway] p. 16Theorem 0(iii)slerflex 27111
[Conway] p. 17Theorem 3addsass 27313  addsassd 27314  addscom 27278  addscomd 27279  addsid1 27276  addsid1d 27277
[Conway] p. 17Definitiondf-0s 27163
[Conway] p. 17Theorem 4(ii)negnegs 27342
[Conway] p. 17Theorem 4(iii)negsid 27339  negsidd 27340
[Conway] p. 18Theorem 5sleadd1 27298  sleadd1d 27304
[Conway] p. 18Definitiondf-1s 27164
[Conway] p. 18Theorem 6(ii)negscl 27334  negscld 27335
[Conway] p. 18Theorem 6(iii)addscld 27290
[Conway] p. 29Remarkmadebday 27229  newbday 27231  oldbday 27230
[Conway] p. 29Definitiondf-made 27177  df-new 27179  df-old 27178
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13766
[Crawley] p. 1Definition of posetdf-poset 18202
[Crawley] p. 107Theorem 13.2hlsupr 37849
[Crawley] p. 110Theorem 13.3arglem1N 38653  dalaw 38349
[Crawley] p. 111Theorem 13.4hlathil 40428
[Crawley] p. 111Definition of set Wdf-watsN 38453
[Crawley] p. 111Definition of dilationdf-dilN 38569  df-ldil 38567  isldil 38573
[Crawley] p. 111Definition of translationdf-ltrn 38568  df-trnN 38570  isltrn 38582  ltrnu 38584
[Crawley] p. 112Lemma Acdlema1N 38254  cdlema2N 38255  exatleN 37867
[Crawley] p. 112Lemma B1cvrat 37939  cdlemb 38257  cdlemb2 38504  cdlemb3 39069  idltrn 38613  l1cvat 37517  lhpat 38506  lhpat2 38508  lshpat 37518  ltrnel 38602  ltrnmw 38614
[Crawley] p. 112Lemma Ccdlemc1 38654  cdlemc2 38655  ltrnnidn 38637  trlat 38632  trljat1 38629  trljat2 38630  trljat3 38631  trlne 38648  trlnidat 38636  trlnle 38649
[Crawley] p. 112Definition of automorphismdf-pautN 38454
[Crawley] p. 113Lemma Ccdlemc 38660  cdlemc3 38656  cdlemc4 38657
[Crawley] p. 113Lemma Dcdlemd 38670  cdlemd1 38661  cdlemd2 38662  cdlemd3 38663  cdlemd4 38664  cdlemd5 38665  cdlemd6 38666  cdlemd7 38667  cdlemd8 38668  cdlemd9 38669  cdleme31sde 38848  cdleme31se 38845  cdleme31se2 38846  cdleme31snd 38849  cdleme32a 38904  cdleme32b 38905  cdleme32c 38906  cdleme32d 38907  cdleme32e 38908  cdleme32f 38909  cdleme32fva 38900  cdleme32fva1 38901  cdleme32fvcl 38903  cdleme32le 38910  cdleme48fv 38962  cdleme4gfv 38970  cdleme50eq 39004  cdleme50f 39005  cdleme50f1 39006  cdleme50f1o 39009  cdleme50laut 39010  cdleme50ldil 39011  cdleme50lebi 39003  cdleme50rn 39008  cdleme50rnlem 39007  cdlemeg49le 38974  cdlemeg49lebilem 39002
[Crawley] p. 113Lemma Ecdleme 39023  cdleme00a 38672  cdleme01N 38684  cdleme02N 38685  cdleme0a 38674  cdleme0aa 38673  cdleme0b 38675  cdleme0c 38676  cdleme0cp 38677  cdleme0cq 38678  cdleme0dN 38679  cdleme0e 38680  cdleme0ex1N 38686  cdleme0ex2N 38687  cdleme0fN 38681  cdleme0gN 38682  cdleme0moN 38688  cdleme1 38690  cdleme10 38717  cdleme10tN 38721  cdleme11 38733  cdleme11a 38723  cdleme11c 38724  cdleme11dN 38725  cdleme11e 38726  cdleme11fN 38727  cdleme11g 38728  cdleme11h 38729  cdleme11j 38730  cdleme11k 38731  cdleme11l 38732  cdleme12 38734  cdleme13 38735  cdleme14 38736  cdleme15 38741  cdleme15a 38737  cdleme15b 38738  cdleme15c 38739  cdleme15d 38740  cdleme16 38748  cdleme16aN 38722  cdleme16b 38742  cdleme16c 38743  cdleme16d 38744  cdleme16e 38745  cdleme16f 38746  cdleme16g 38747  cdleme19a 38766  cdleme19b 38767  cdleme19c 38768  cdleme19d 38769  cdleme19e 38770  cdleme19f 38771  cdleme1b 38689  cdleme2 38691  cdleme20aN 38772  cdleme20bN 38773  cdleme20c 38774  cdleme20d 38775  cdleme20e 38776  cdleme20f 38777  cdleme20g 38778  cdleme20h 38779  cdleme20i 38780  cdleme20j 38781  cdleme20k 38782  cdleme20l 38785  cdleme20l1 38783  cdleme20l2 38784  cdleme20m 38786  cdleme20y 38765  cdleme20zN 38764  cdleme21 38800  cdleme21d 38793  cdleme21e 38794  cdleme22a 38803  cdleme22aa 38802  cdleme22b 38804  cdleme22cN 38805  cdleme22d 38806  cdleme22e 38807  cdleme22eALTN 38808  cdleme22f 38809  cdleme22f2 38810  cdleme22g 38811  cdleme23a 38812  cdleme23b 38813  cdleme23c 38814  cdleme26e 38822  cdleme26eALTN 38824  cdleme26ee 38823  cdleme26f 38826  cdleme26f2 38828  cdleme26f2ALTN 38827  cdleme26fALTN 38825  cdleme27N 38832  cdleme27a 38830  cdleme27cl 38829  cdleme28c 38835  cdleme3 38700  cdleme30a 38841  cdleme31fv 38853  cdleme31fv1 38854  cdleme31fv1s 38855  cdleme31fv2 38856  cdleme31id 38857  cdleme31sc 38847  cdleme31sdnN 38850  cdleme31sn 38843  cdleme31sn1 38844  cdleme31sn1c 38851  cdleme31sn2 38852  cdleme31so 38842  cdleme35a 38911  cdleme35b 38913  cdleme35c 38914  cdleme35d 38915  cdleme35e 38916  cdleme35f 38917  cdleme35fnpq 38912  cdleme35g 38918  cdleme35h 38919  cdleme35h2 38920  cdleme35sn2aw 38921  cdleme35sn3a 38922  cdleme36a 38923  cdleme36m 38924  cdleme37m 38925  cdleme38m 38926  cdleme38n 38927  cdleme39a 38928  cdleme39n 38929  cdleme3b 38692  cdleme3c 38693  cdleme3d 38694  cdleme3e 38695  cdleme3fN 38696  cdleme3fa 38699  cdleme3g 38697  cdleme3h 38698  cdleme4 38701  cdleme40m 38930  cdleme40n 38931  cdleme40v 38932  cdleme40w 38933  cdleme41fva11 38940  cdleme41sn3aw 38937  cdleme41sn4aw 38938  cdleme41snaw 38939  cdleme42a 38934  cdleme42b 38941  cdleme42c 38935  cdleme42d 38936  cdleme42e 38942  cdleme42f 38943  cdleme42g 38944  cdleme42h 38945  cdleme42i 38946  cdleme42k 38947  cdleme42ke 38948  cdleme42keg 38949  cdleme42mN 38950  cdleme42mgN 38951  cdleme43aN 38952  cdleme43bN 38953  cdleme43cN 38954  cdleme43dN 38955  cdleme5 38703  cdleme50ex 39022  cdleme50ltrn 39020  cdleme51finvN 39019  cdleme51finvfvN 39018  cdleme51finvtrN 39021  cdleme6 38704  cdleme7 38712  cdleme7a 38706  cdleme7aa 38705  cdleme7b 38707  cdleme7c 38708  cdleme7d 38709  cdleme7e 38710  cdleme7ga 38711  cdleme8 38713  cdleme8tN 38718  cdleme9 38716  cdleme9a 38714  cdleme9b 38715  cdleme9tN 38720  cdleme9taN 38719  cdlemeda 38761  cdlemedb 38760  cdlemednpq 38762  cdlemednuN 38763  cdlemefr27cl 38866  cdlemefr32fva1 38873  cdlemefr32fvaN 38872  cdlemefrs32fva 38863  cdlemefrs32fva1 38864  cdlemefs27cl 38876  cdlemefs32fva1 38886  cdlemefs32fvaN 38885  cdlemesner 38759  cdlemeulpq 38683
[Crawley] p. 114Lemma E4atex 38539  4atexlem7 38538  cdleme0nex 38753  cdleme17a 38749  cdleme17c 38751  cdleme17d 38961  cdleme17d1 38752  cdleme17d2 38958  cdleme18a 38754  cdleme18b 38755  cdleme18c 38756  cdleme18d 38758  cdleme4a 38702
[Crawley] p. 115Lemma Ecdleme21a 38788  cdleme21at 38791  cdleme21b 38789  cdleme21c 38790  cdleme21ct 38792  cdleme21f 38795  cdleme21g 38796  cdleme21h 38797  cdleme21i 38798  cdleme22gb 38757
[Crawley] p. 116Lemma Fcdlemf 39026  cdlemf1 39024  cdlemf2 39025
[Crawley] p. 116Lemma Gcdlemftr1 39030  cdlemg16 39120  cdlemg28 39167  cdlemg28a 39156  cdlemg28b 39166  cdlemg3a 39060  cdlemg42 39192  cdlemg43 39193  cdlemg44 39196  cdlemg44a 39194  cdlemg46 39198  cdlemg47 39199  cdlemg9 39097  ltrnco 39182  ltrncom 39201  tgrpabl 39214  trlco 39190
[Crawley] p. 116Definition of Gdf-tgrp 39206
[Crawley] p. 117Lemma Gcdlemg17 39140  cdlemg17b 39125
[Crawley] p. 117Definition of Edf-edring-rN 39219  df-edring 39220
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 39223
[Crawley] p. 118Remarktendopltp 39243
[Crawley] p. 118Lemma Hcdlemh 39280  cdlemh1 39278  cdlemh2 39279
[Crawley] p. 118Lemma Icdlemi 39283  cdlemi1 39281  cdlemi2 39282
[Crawley] p. 118Lemma Jcdlemj1 39284  cdlemj2 39285  cdlemj3 39286  tendocan 39287
[Crawley] p. 118Lemma Kcdlemk 39437  cdlemk1 39294  cdlemk10 39306  cdlemk11 39312  cdlemk11t 39409  cdlemk11ta 39392  cdlemk11tb 39394  cdlemk11tc 39408  cdlemk11u-2N 39352  cdlemk11u 39334  cdlemk12 39313  cdlemk12u-2N 39353  cdlemk12u 39335  cdlemk13-2N 39339  cdlemk13 39315  cdlemk14-2N 39341  cdlemk14 39317  cdlemk15-2N 39342  cdlemk15 39318  cdlemk16-2N 39343  cdlemk16 39320  cdlemk16a 39319  cdlemk17-2N 39344  cdlemk17 39321  cdlemk18-2N 39349  cdlemk18-3N 39363  cdlemk18 39331  cdlemk19-2N 39350  cdlemk19 39332  cdlemk19u 39433  cdlemk1u 39322  cdlemk2 39295  cdlemk20-2N 39355  cdlemk20 39337  cdlemk21-2N 39354  cdlemk21N 39336  cdlemk22-3 39364  cdlemk22 39356  cdlemk23-3 39365  cdlemk24-3 39366  cdlemk25-3 39367  cdlemk26-3 39369  cdlemk26b-3 39368  cdlemk27-3 39370  cdlemk28-3 39371  cdlemk29-3 39374  cdlemk3 39296  cdlemk30 39357  cdlemk31 39359  cdlemk32 39360  cdlemk33N 39372  cdlemk34 39373  cdlemk35 39375  cdlemk36 39376  cdlemk37 39377  cdlemk38 39378  cdlemk39 39379  cdlemk39u 39431  cdlemk4 39297  cdlemk41 39383  cdlemk42 39404  cdlemk42yN 39407  cdlemk43N 39426  cdlemk45 39410  cdlemk46 39411  cdlemk47 39412  cdlemk48 39413  cdlemk49 39414  cdlemk5 39299  cdlemk50 39415  cdlemk51 39416  cdlemk52 39417  cdlemk53 39420  cdlemk54 39421  cdlemk55 39424  cdlemk55u 39429  cdlemk56 39434  cdlemk5a 39298  cdlemk5auN 39323  cdlemk5u 39324  cdlemk6 39300  cdlemk6u 39325  cdlemk7 39311  cdlemk7u-2N 39351  cdlemk7u 39333  cdlemk8 39301  cdlemk9 39302  cdlemk9bN 39303  cdlemki 39304  cdlemkid 39399  cdlemkj-2N 39345  cdlemkj 39326  cdlemksat 39309  cdlemksel 39308  cdlemksv 39307  cdlemksv2 39310  cdlemkuat 39329  cdlemkuel-2N 39347  cdlemkuel-3 39361  cdlemkuel 39328  cdlemkuv-2N 39346  cdlemkuv2-2 39348  cdlemkuv2-3N 39362  cdlemkuv2 39330  cdlemkuvN 39327  cdlemkvcl 39305  cdlemky 39389  cdlemkyyN 39425  tendoex 39438
[Crawley] p. 120Remarkdva1dim 39448
[Crawley] p. 120Lemma Lcdleml1N 39439  cdleml2N 39440  cdleml3N 39441  cdleml4N 39442  cdleml5N 39443  cdleml6 39444  cdleml7 39445  cdleml8 39446  cdleml9 39447  dia1dim 39524
[Crawley] p. 120Lemma Mdia11N 39511  diaf11N 39512  dialss 39509  diaord 39510  dibf11N 39624  djajN 39600
[Crawley] p. 120Definition of isomorphism mapdiaval 39495
[Crawley] p. 121Lemma Mcdlemm10N 39581  dia2dimlem1 39527  dia2dimlem2 39528  dia2dimlem3 39529  dia2dimlem4 39530  dia2dimlem5 39531  diaf1oN 39593  diarnN 39592  dvheveccl 39575  dvhopN 39579
[Crawley] p. 121Lemma Ncdlemn 39675  cdlemn10 39669  cdlemn11 39674  cdlemn11a 39670  cdlemn11b 39671  cdlemn11c 39672  cdlemn11pre 39673  cdlemn2 39658  cdlemn2a 39659  cdlemn3 39660  cdlemn4 39661  cdlemn4a 39662  cdlemn5 39664  cdlemn5pre 39663  cdlemn6 39665  cdlemn7 39666  cdlemn8 39667  cdlemn9 39668  diclspsn 39657
[Crawley] p. 121Definition of phi(q)df-dic 39636
[Crawley] p. 122Lemma Ndih11 39728  dihf11 39730  dihjust 39680  dihjustlem 39679  dihord 39727  dihord1 39681  dihord10 39686  dihord11b 39685  dihord11c 39687  dihord2 39690  dihord2a 39682  dihord2b 39683  dihord2cN 39684  dihord2pre 39688  dihord2pre2 39689  dihordlem6 39676  dihordlem7 39677  dihordlem7b 39678
[Crawley] p. 122Definition of isomorphism mapdihffval 39693  dihfval 39694  dihval 39695
[Diestel] p. 3Section 1.1df-cusgr 28360  df-nbgr 28281
[Diestel] p. 4Section 1.1df-subgr 28216  uhgrspan1 28251  uhgrspansubgr 28239
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 28502  vtxdgoddnumeven 28501
[Diestel] p. 27Section 1.10df-ushgr 28010
[EGA] p. 80Notation 1.1.1rspecval 32445
[EGA] p. 80Proposition 1.1.2zartop 32457
[EGA] p. 80Proposition 1.1.2(i)zarcls0 32449  zarcls1 32450
[EGA] p. 81Corollary 1.1.8zart0 32460
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 32463
[EGA], p. 83Corollary 1.2.3rhmpreimacn 32466
[Eisenberg] p. 67Definition 5.3df-dif 3913
[Eisenberg] p. 82Definition 6.3dfom3 9583
[Eisenberg] p. 125Definition 8.21df-map 8767
[Eisenberg] p. 216Example 13.2(4)omenps 9591
[Eisenberg] p. 310Theorem 19.8cardprc 9916
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10491
[Enderton] p. 18Axiom of Empty Setaxnul 5262
[Enderton] p. 19Definitiondf-tp 4591
[Enderton] p. 26Exercise 5unissb 4900
[Enderton] p. 26Exercise 10pwel 5336
[Enderton] p. 28Exercise 7(b)pwun 5529
[Enderton] p. 30Theorem "Distributive laws"iinin1 5039  iinin2 5038  iinun2 5033  iunin1 5032  iunin1f 31476  iunin2 5031  uniin1 31470  uniin2 31471
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5037  iundif2 5034
[Enderton] p. 32Exercise 20unineq 4237
[Enderton] p. 33Exercise 23iinuni 5058
[Enderton] p. 33Exercise 25iununi 5059
[Enderton] p. 33Exercise 24(a)iinpw 5066
[Enderton] p. 33Exercise 24(b)iunpw 7705  iunpwss 5067
[Enderton] p. 36Definitionopthwiener 5471
[Enderton] p. 38Exercise 6(a)unipw 5407
[Enderton] p. 38Exercise 6(b)pwuni 4906
[Enderton] p. 41Lemma 3Dopeluu 5427  rnex 7849  rnexg 7841
[Enderton] p. 41Exercise 8dmuni 5870  rnuni 6101
[Enderton] p. 42Definition of a functiondffun7 6528  dffun8 6529
[Enderton] p. 43Definition of function valuefunfv2 6929
[Enderton] p. 43Definition of single-rootedfuncnv 6570
[Enderton] p. 44Definition (d)dfima2 6015  dfima3 6016
[Enderton] p. 47Theorem 3Hfvco2 6938
[Enderton] p. 49Axiom of Choice (first form)ac7 10409  ac7g 10410  df-ac 10052  dfac2 10067  dfac2a 10065  dfac2b 10066  dfac3 10057  dfac7 10068
[Enderton] p. 50Theorem 3K(a)imauni 7193
[Enderton] p. 52Definitiondf-map 8767
[Enderton] p. 53Exercise 21coass 6217
[Enderton] p. 53Exercise 27dmco 6206
[Enderton] p. 53Exercise 14(a)funin 6577
[Enderton] p. 53Exercise 22(a)imass2 6054
[Enderton] p. 54Remarkixpf 8858  ixpssmap 8870
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8836
[Enderton] p. 55Axiom of Choice (second form)ac9 10419  ac9s 10429
[Enderton] p. 56Theorem 3Meqvrelref 37072  erref 8668
[Enderton] p. 57Lemma 3Neqvrelthi 37075  erthi 8699
[Enderton] p. 57Definitiondf-ec 8650
[Enderton] p. 58Definitiondf-qs 8654
[Enderton] p. 61Exercise 35df-ec 8650
[Enderton] p. 65Exercise 56(a)dmun 5866
[Enderton] p. 68Definition of successordf-suc 6323
[Enderton] p. 71Definitiondf-tr 5223  dftr4 5229
[Enderton] p. 72Theorem 4Eunisuc 6396  unisucg 6395
[Enderton] p. 73Exercise 6unisuc 6396  unisucg 6395
[Enderton] p. 73Exercise 5(a)truni 5238
[Enderton] p. 73Exercise 5(b)trint 5240  trintALT 43153
[Enderton] p. 79Theorem 4I(A1)nna0 8551
[Enderton] p. 79Theorem 4I(A2)nnasuc 8553  onasuc 8474
[Enderton] p. 79Definition of operation valuedf-ov 7360
[Enderton] p. 80Theorem 4J(A1)nnm0 8552
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8554  onmsuc 8475
[Enderton] p. 81Theorem 4K(1)nnaass 8569
[Enderton] p. 81Theorem 4K(2)nna0r 8556  nnacom 8564
[Enderton] p. 81Theorem 4K(3)nndi 8570
[Enderton] p. 81Theorem 4K(4)nnmass 8571
[Enderton] p. 81Theorem 4K(5)nnmcom 8573
[Enderton] p. 82Exercise 16nnm0r 8557  nnmsucr 8572
[Enderton] p. 88Exercise 23nnaordex 8585
[Enderton] p. 129Definitiondf-en 8884
[Enderton] p. 132Theorem 6B(b)canth 7310
[Enderton] p. 133Exercise 1xpomen 9951
[Enderton] p. 133Exercise 2qnnen 16095
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9154
[Enderton] p. 135Corollary 6Cphp3 9156
[Enderton] p. 136Corollary 6Enneneq 9153
[Enderton] p. 136Corollary 6D(a)pssinf 9200
[Enderton] p. 136Corollary 6D(b)ominf 9202
[Enderton] p. 137Lemma 6Fpssnn 9112
[Enderton] p. 138Corollary 6Gssfi 9117
[Enderton] p. 139Theorem 6H(c)mapen 9085
[Enderton] p. 142Theorem 6I(3)xpdjuen 10115
[Enderton] p. 142Theorem 6I(4)mapdjuen 10116
[Enderton] p. 143Theorem 6Jdju0en 10111  dju1en 10107
[Enderton] p. 144Exercise 13iunfi 9284  unifi 9285  unifi2 9286
[Enderton] p. 144Corollary 6Kundif2 4436  unfi 9116  unfi2 9259
[Enderton] p. 145Figure 38ffoss 7878
[Enderton] p. 145Definitiondf-dom 8885
[Enderton] p. 146Example 1domen 8901  domeng 8902
[Enderton] p. 146Example 3nndomo 9177  nnsdom 9590  nnsdomg 9246
[Enderton] p. 149Theorem 6L(a)djudom2 10119
[Enderton] p. 149Theorem 6L(c)mapdom1 9086  xpdom1 9015  xpdom1g 9013  xpdom2g 9012
[Enderton] p. 149Theorem 6L(d)mapdom2 9092
[Enderton] p. 151Theorem 6Mzorn 10443  zorng 10440
[Enderton] p. 151Theorem 6M(4)ac8 10428  dfac5 10064
[Enderton] p. 159Theorem 6Qunictb 10511
[Enderton] p. 164Exampleinfdif 10145
[Enderton] p. 168Definitiondf-po 5545
[Enderton] p. 192Theorem 7M(a)oneli 6431
[Enderton] p. 192Theorem 7M(b)ontr1 6363
[Enderton] p. 192Theorem 7M(c)onirri 6430
[Enderton] p. 193Corollary 7N(b)0elon 6371
[Enderton] p. 193Corollary 7N(c)onsuci 7774
[Enderton] p. 193Corollary 7N(d)ssonunii 7715
[Enderton] p. 194Remarkonprc 7712
[Enderton] p. 194Exercise 16suc11 6424
[Enderton] p. 197Definitiondf-card 9875
[Enderton] p. 197Theorem 7Pcarden 10487
[Enderton] p. 200Exercise 25tfis 7791
[Enderton] p. 202Lemma 7Tr1tr 9712
[Enderton] p. 202Definitiondf-r1 9700
[Enderton] p. 202Theorem 7Qr1val1 9722
[Enderton] p. 204Theorem 7V(b)rankval4 9803
[Enderton] p. 206Theorem 7X(b)en2lp 9542
[Enderton] p. 207Exercise 30rankpr 9793  rankprb 9787  rankpw 9779  rankpwi 9759  rankuniss 9802
[Enderton] p. 207Exercise 34opthreg 9554
[Enderton] p. 208Exercise 35suc11reg 9555
[Enderton] p. 212Definition of alephalephval3 10046
[Enderton] p. 213Theorem 8A(a)alephord2 10012
[Enderton] p. 213Theorem 8A(b)cardalephex 10026
[Enderton] p. 218Theorem Schema 8Eonfununi 8287
[Enderton] p. 222Definition of kardkarden 9831  kardex 9830
[Enderton] p. 238Theorem 8Roeoa 8544
[Enderton] p. 238Theorem 8Soeoe 8546
[Enderton] p. 240Exercise 25oarec 8509
[Enderton] p. 257Definition of cofinalitycflm 10186
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17522
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17468
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18442  mrieqv2d 17519  mrieqvd 17518
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17523
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17528  mreexexlem2d 17525
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18448  mreexfidimd 17530
[Frege1879] p. 11Statementdf3or2 42030
[Frege1879] p. 12Statementdf3an2 42031  dfxor4 42028  dfxor5 42029
[Frege1879] p. 26Axiom 1ax-frege1 42052
[Frege1879] p. 26Axiom 2ax-frege2 42053
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 42057
[Frege1879] p. 31Proposition 4frege4 42061
[Frege1879] p. 32Proposition 5frege5 42062
[Frege1879] p. 33Proposition 6frege6 42068
[Frege1879] p. 34Proposition 7frege7 42070
[Frege1879] p. 35Axiom 8ax-frege8 42071  axfrege8 42069
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 35916
[Frege1879] p. 35Proposition 9frege9 42074
[Frege1879] p. 36Proposition 10frege10 42082
[Frege1879] p. 36Proposition 11frege11 42076
[Frege1879] p. 37Proposition 12frege12 42075
[Frege1879] p. 37Proposition 13frege13 42084
[Frege1879] p. 37Proposition 14frege14 42085
[Frege1879] p. 38Proposition 15frege15 42088
[Frege1879] p. 38Proposition 16frege16 42078
[Frege1879] p. 39Proposition 17frege17 42083
[Frege1879] p. 39Proposition 18frege18 42080
[Frege1879] p. 39Proposition 19frege19 42086
[Frege1879] p. 40Proposition 20frege20 42090
[Frege1879] p. 40Proposition 21frege21 42089
[Frege1879] p. 41Proposition 22frege22 42081
[Frege1879] p. 42Proposition 23frege23 42087
[Frege1879] p. 42Proposition 24frege24 42077
[Frege1879] p. 42Proposition 25frege25 42079  rp-frege25 42067
[Frege1879] p. 42Proposition 26frege26 42072
[Frege1879] p. 43Axiom 28ax-frege28 42092
[Frege1879] p. 43Proposition 27frege27 42073
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 42093
[Frege1879] p. 44Axiom 31ax-frege31 42096  axfrege31 42095
[Frege1879] p. 44Proposition 30frege30 42094
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 42097
[Frege1879] p. 44Proposition 33frege33 42098
[Frege1879] p. 45Proposition 34frege34 42099
[Frege1879] p. 45Proposition 35frege35 42100
[Frege1879] p. 45Proposition 36frege36 42101
[Frege1879] p. 46Proposition 37frege37 42102
[Frege1879] p. 46Proposition 38frege38 42103
[Frege1879] p. 46Proposition 39frege39 42104
[Frege1879] p. 46Proposition 40frege40 42105
[Frege1879] p. 47Axiom 41ax-frege41 42107  axfrege41 42106
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 42108
[Frege1879] p. 47Proposition 43frege43 42109
[Frege1879] p. 47Proposition 44frege44 42110
[Frege1879] p. 47Proposition 45frege45 42111
[Frege1879] p. 48Proposition 46frege46 42112
[Frege1879] p. 48Proposition 47frege47 42113
[Frege1879] p. 49Proposition 48frege48 42114
[Frege1879] p. 49Proposition 49frege49 42115
[Frege1879] p. 49Proposition 50frege50 42116
[Frege1879] p. 50Axiom 52ax-frege52a 42119  ax-frege52c 42150  frege52aid 42120  frege52b 42151
[Frege1879] p. 50Axiom 54ax-frege54a 42124  ax-frege54c 42154  frege54b 42155
[Frege1879] p. 50Proposition 51frege51 42117
[Frege1879] p. 50Proposition 52dfsbcq 3741
[Frege1879] p. 50Proposition 53frege53a 42122  frege53aid 42121  frege53b 42152  frege53c 42176
[Frege1879] p. 50Proposition 54biid 260  eqid 2736
[Frege1879] p. 50Proposition 55frege55a 42130  frege55aid 42127  frege55b 42159  frege55c 42180  frege55cor1a 42131  frege55lem2a 42129  frege55lem2b 42158  frege55lem2c 42179
[Frege1879] p. 50Proposition 56frege56a 42133  frege56aid 42132  frege56b 42160  frege56c 42181
[Frege1879] p. 51Axiom 58ax-frege58a 42137  ax-frege58b 42163  frege58bid 42164  frege58c 42183
[Frege1879] p. 51Proposition 57frege57a 42135  frege57aid 42134  frege57b 42161  frege57c 42182
[Frege1879] p. 51Proposition 58spsbc 3752
[Frege1879] p. 51Proposition 59frege59a 42139  frege59b 42166  frege59c 42184
[Frege1879] p. 52Proposition 60frege60a 42140  frege60b 42167  frege60c 42185
[Frege1879] p. 52Proposition 61frege61a 42141  frege61b 42168  frege61c 42186
[Frege1879] p. 52Proposition 62frege62a 42142  frege62b 42169  frege62c 42187
[Frege1879] p. 52Proposition 63frege63a 42143  frege63b 42170  frege63c 42188
[Frege1879] p. 53Proposition 64frege64a 42144  frege64b 42171  frege64c 42189
[Frege1879] p. 53Proposition 65frege65a 42145  frege65b 42172  frege65c 42190
[Frege1879] p. 54Proposition 66frege66a 42146  frege66b 42173  frege66c 42191
[Frege1879] p. 54Proposition 67frege67a 42147  frege67b 42174  frege67c 42192
[Frege1879] p. 54Proposition 68frege68a 42148  frege68b 42175  frege68c 42193
[Frege1879] p. 55Definition 69dffrege69 42194
[Frege1879] p. 58Proposition 70frege70 42195
[Frege1879] p. 59Proposition 71frege71 42196
[Frege1879] p. 59Proposition 72frege72 42197
[Frege1879] p. 59Proposition 73frege73 42198
[Frege1879] p. 60Definition 76dffrege76 42201
[Frege1879] p. 60Proposition 74frege74 42199
[Frege1879] p. 60Proposition 75frege75 42200
[Frege1879] p. 62Proposition 77frege77 42202  frege77d 42008
[Frege1879] p. 63Proposition 78frege78 42203
[Frege1879] p. 63Proposition 79frege79 42204
[Frege1879] p. 63Proposition 80frege80 42205
[Frege1879] p. 63Proposition 81frege81 42206  frege81d 42009
[Frege1879] p. 64Proposition 82frege82 42207
[Frege1879] p. 65Proposition 83frege83 42208  frege83d 42010
[Frege1879] p. 65Proposition 84frege84 42209
[Frege1879] p. 66Proposition 85frege85 42210
[Frege1879] p. 66Proposition 86frege86 42211
[Frege1879] p. 66Proposition 87frege87 42212  frege87d 42012
[Frege1879] p. 67Proposition 88frege88 42213
[Frege1879] p. 68Proposition 89frege89 42214
[Frege1879] p. 68Proposition 90frege90 42215
[Frege1879] p. 68Proposition 91frege91 42216  frege91d 42013
[Frege1879] p. 69Proposition 92frege92 42217
[Frege1879] p. 70Proposition 93frege93 42218
[Frege1879] p. 70Proposition 94frege94 42219
[Frege1879] p. 70Proposition 95frege95 42220
[Frege1879] p. 71Definition 99dffrege99 42224
[Frege1879] p. 71Proposition 96frege96 42221  frege96d 42011
[Frege1879] p. 71Proposition 97frege97 42222  frege97d 42014
[Frege1879] p. 71Proposition 98frege98 42223  frege98d 42015
[Frege1879] p. 72Proposition 100frege100 42225
[Frege1879] p. 72Proposition 101frege101 42226
[Frege1879] p. 72Proposition 102frege102 42227  frege102d 42016
[Frege1879] p. 73Proposition 103frege103 42228
[Frege1879] p. 73Proposition 104frege104 42229
[Frege1879] p. 73Proposition 105frege105 42230
[Frege1879] p. 73Proposition 106frege106 42231  frege106d 42017
[Frege1879] p. 74Proposition 107frege107 42232
[Frege1879] p. 74Proposition 108frege108 42233  frege108d 42018
[Frege1879] p. 74Proposition 109frege109 42234  frege109d 42019
[Frege1879] p. 75Proposition 110frege110 42235
[Frege1879] p. 75Proposition 111frege111 42236  frege111d 42021
[Frege1879] p. 76Proposition 112frege112 42237
[Frege1879] p. 76Proposition 113frege113 42238
[Frege1879] p. 76Proposition 114frege114 42239  frege114d 42020
[Frege1879] p. 77Definition 115dffrege115 42240
[Frege1879] p. 77Proposition 116frege116 42241
[Frege1879] p. 78Proposition 117frege117 42242
[Frege1879] p. 78Proposition 118frege118 42243
[Frege1879] p. 78Proposition 119frege119 42244
[Frege1879] p. 78Proposition 120frege120 42245
[Frege1879] p. 79Proposition 121frege121 42246
[Frege1879] p. 79Proposition 122frege122 42247  frege122d 42022
[Frege1879] p. 79Proposition 123frege123 42248
[Frege1879] p. 80Proposition 124frege124 42249  frege124d 42023
[Frege1879] p. 81Proposition 125frege125 42250
[Frege1879] p. 81Proposition 126frege126 42251  frege126d 42024
[Frege1879] p. 82Proposition 127frege127 42252
[Frege1879] p. 83Proposition 128frege128 42253
[Frege1879] p. 83Proposition 129frege129 42254  frege129d 42025
[Frege1879] p. 84Proposition 130frege130 42255
[Frege1879] p. 85Proposition 131frege131 42256  frege131d 42026
[Frege1879] p. 86Proposition 132frege132 42257
[Frege1879] p. 86Proposition 133frege133 42258  frege133d 42027
[Fremlin1] p. 13Definition 111G (b)df-salgen 44544
[Fremlin1] p. 13Definition 111G (d)borelmbl 44867
[Fremlin1] p. 13Proposition 111G (b)salgenss 44567
[Fremlin1] p. 14Definition 112Aismea 44682
[Fremlin1] p. 15Remark 112B (d)psmeasure 44702
[Fremlin1] p. 15Property 112C (a)meadjun 44693  meadjunre 44707
[Fremlin1] p. 15Property 112C (b)meassle 44694
[Fremlin1] p. 15Property 112C (c)meaunle 44695
[Fremlin1] p. 16Property 112C (d)iundjiun 44691  meaiunle 44700  meaiunlelem 44699
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 44712  meaiuninc2 44713  meaiuninc3 44716  meaiuninc3v 44715  meaiunincf 44714  meaiuninclem 44711
[Fremlin1] p. 16Proposition 112C (f)meaiininc 44718  meaiininc2 44719  meaiininclem 44717
[Fremlin1] p. 19Theorem 113Ccaragen0 44737  caragendifcl 44745  caratheodory 44759  omelesplit 44749
[Fremlin1] p. 19Definition 113Aisome 44725  isomennd 44762  isomenndlem 44761
[Fremlin1] p. 19Remark 113B (c)omeunle 44747
[Fremlin1] p. 19Definition 112Dfcaragencmpl 44766  voncmpl 44852
[Fremlin1] p. 19Definition 113A (ii)omessle 44729
[Fremlin1] p. 20Theorem 113Ccarageniuncl 44754  carageniuncllem1 44752  carageniuncllem2 44753  caragenuncl 44744  caragenuncllem 44743  caragenunicl 44755
[Fremlin1] p. 21Remark 113Dcaragenel2d 44763
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 44757  caratheodorylem2 44758
[Fremlin1] p. 21Exercise 113Xacaragencmpl 44766
[Fremlin1] p. 23Lemma 114Bhoidmv1le 44825  hoidmv1lelem1 44822  hoidmv1lelem2 44823  hoidmv1lelem3 44824
[Fremlin1] p. 25Definition 114Eisvonmbl 44869
[Fremlin1] p. 29Lemma 115Bhoidmv1le 44825  hoidmvle 44831  hoidmvlelem1 44826  hoidmvlelem2 44827  hoidmvlelem3 44828  hoidmvlelem4 44829  hoidmvlelem5 44830  hsphoidmvle2 44816  hsphoif 44807  hsphoival 44810
[Fremlin1] p. 29Definition 1135 (b)hoicvr 44779
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 44787
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 44814  hoidmvn0val 44815  hoidmvval 44808  hoidmvval0 44818  hoidmvval0b 44821
[Fremlin1] p. 30Lemma 115Bhoiprodp1 44819  hsphoidmvle 44817
[Fremlin1] p. 30Definition 115Cdf-ovoln 44768  df-voln 44770
[Fremlin1] p. 30Proposition 115D (a)dmovn 44835  ovn0 44797  ovn0lem 44796  ovnf 44794  ovnome 44804  ovnssle 44792  ovnsslelem 44791  ovnsupge0 44788
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 44834  ovnhoilem1 44832  ovnhoilem2 44833  vonhoi 44898
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 44851  hoidifhspf 44849  hoidifhspval 44839  hoidifhspval2 44846  hoidifhspval3 44850  hspmbl 44860  hspmbllem1 44857  hspmbllem2 44858  hspmbllem3 44859
[Fremlin1] p. 31Definition 115Evoncmpl 44852  vonmea 44805
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 44803  ovnsubadd2 44877  ovnsubadd2lem 44876  ovnsubaddlem1 44801  ovnsubaddlem2 44802
[Fremlin1] p. 32Proposition 115G (a)hoimbl 44862  hoimbl2 44896  hoimbllem 44861  hspdifhsp 44847  opnvonmbl 44865  opnvonmbllem2 44864
[Fremlin1] p. 32Proposition 115G (b)borelmbl 44867
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 44910  iccvonmbllem 44909  ioovonmbl 44908
[Fremlin1] p. 32Proposition 115G (d)vonicc 44916  vonicclem2 44915  vonioo 44913  vonioolem2 44912  vonn0icc 44919  vonn0icc2 44923  vonn0ioo 44918  vonn0ioo2 44921
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 44920  snvonmbl 44917  vonct 44924  vonsn 44922
[Fremlin1] p. 35Lemma 121Asubsalsal 44590
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 44589  subsaliuncllem 44588
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 44956  salpreimalegt 44940  salpreimaltle 44957
[Fremlin1] p. 35Proposition 121B (i)issmf 44959  issmff 44965  issmflem 44958
[Fremlin1] p. 35Proposition 121B (ii)issmfle 44976  issmflelem 44975  smfpreimale 44985
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 44987  issmfgtlem 44986
[Fremlin1] p. 36Definition 121Cdf-smblfn 44927  issmf 44959  issmff 44965  issmfge 45001  issmfgelem 45000  issmfgt 44987  issmfgtlem 44986  issmfle 44976  issmflelem 44975  issmflem 44958
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 44938  salpreimagtlt 44961  salpreimalelt 44960
[Fremlin1] p. 36Proposition 121B (iv)issmfge 45001  issmfgelem 45000
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 44984
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 44982  cnfsmf 44971
[Fremlin1] p. 36Proposition 121D (c)decsmf 44998  decsmflem 44997  incsmf 44973  incsmflem 44972
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 44932  pimconstlt1 44933  smfconst 44980
[Fremlin1] p. 37Proposition 121E (b)smfadd 44996  smfaddlem1 44994  smfaddlem2 44995
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 45027
[Fremlin1] p. 37Proposition 121E (d)smfmul 45026  smfmullem1 45022  smfmullem2 45023  smfmullem3 45024  smfmullem4 45025
[Fremlin1] p. 37Proposition 121E (e)smfdiv 45028
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 45031  smfpimbor1lem2 45030
[Fremlin1] p. 37Proposition 121E (g)smfco 45033
[Fremlin1] p. 37Proposition 121E (h)smfres 45021
[Fremlin1] p. 38Proposition 121E (e)smfrec 45020
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 45029  smfresal 45019
[Fremlin1] p. 38Proposition 121F (a)smflim 45008  smflim2 45037  smflimlem1 45002  smflimlem2 45003  smflimlem3 45004  smflimlem4 45005  smflimlem5 45006  smflimlem6 45007  smflimmpt 45041
[Fremlin1] p. 38Proposition 121F (b)smfsup 45045  smfsuplem1 45042  smfsuplem2 45043  smfsuplem3 45044  smfsupmpt 45046  smfsupxr 45047
[Fremlin1] p. 38Proposition 121F (c)smfinf 45049  smfinflem 45048  smfinfmpt 45050
[Fremlin1] p. 39Remark 121Gsmflim 45008  smflim2 45037  smflimmpt 45041
[Fremlin1] p. 39Proposition 121Fsmfpimcc 45039
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 45069  smfdivdmmbl2 45072  smfinfdmmbl 45080  smfinfdmmbllem 45079  smfsupdmmbl 45076  smfsupdmmbllem 45075
[Fremlin1] p. 39Proposition 121F (d)smflimsup 45059  smflimsuplem2 45052  smflimsuplem6 45056  smflimsuplem7 45057  smflimsuplem8 45058  smflimsupmpt 45060
[Fremlin1] p. 39Proposition 121F (e)smfliminf 45062  smfliminflem 45061  smfliminfmpt 45063
[Fremlin1] p. 80Definition 135E (b)df-smblfn 44927
[Fremlin1], p. 38Proposition 121F (b)fsupdm 45073  fsupdm2 45074
[Fremlin1], p. 39Proposition 121Hadddmmbl 45064  adddmmbl2 45065  finfdm 45077  finfdm2 45078  fsupdm 45073  fsupdm2 45074  muldmmbl 45066  muldmmbl2 45067
[Fremlin1], p. 39Proposition 121F (c)finfdm 45077  finfdm2 45078
[Fremlin5] p. 193Proposition 563Gbnulmbl2 24900
[Fremlin5] p. 213Lemma 565Cauniioovol 24943
[Fremlin5] p. 214Lemma 565Cauniioombl 24953
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 36156
[Fremlin5] p. 220Theorem 565Maftc1anc 36159
[FreydScedrov] p. 283Axiom of Infinityax-inf 9574  inf1 9558  inf2 9559
[Gleason] p. 117Proposition 9-2.1df-enq 10847  enqer 10857
[Gleason] p. 117Proposition 9-2.2df-1nq 10852  df-nq 10848
[Gleason] p. 117Proposition 9-2.3df-plpq 10844  df-plq 10850
[Gleason] p. 119Proposition 9-2.4caovmo 7591  df-mpq 10845  df-mq 10851
[Gleason] p. 119Proposition 9-2.5df-rq 10853
[Gleason] p. 119Proposition 9-2.6ltexnq 10911
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10912  ltbtwnnq 10914
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10907
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10908
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10915
[Gleason] p. 121Definition 9-3.1df-np 10917
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10929
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10931
[Gleason] p. 122Definitiondf-1p 10918
[Gleason] p. 122Remark (1)prub 10930
[Gleason] p. 122Lemma 9-3.4prlem934 10969
[Gleason] p. 122Proposition 9-3.2df-ltp 10921
[Gleason] p. 122Proposition 9-3.3ltsopr 10968  psslinpr 10967  supexpr 10990  suplem1pr 10988  suplem2pr 10989
[Gleason] p. 123Proposition 9-3.5addclpr 10954  addclprlem1 10952  addclprlem2 10953  df-plp 10919
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10958
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10957
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10970
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10979  ltexprlem1 10972  ltexprlem2 10973  ltexprlem3 10974  ltexprlem4 10975  ltexprlem5 10976  ltexprlem6 10977  ltexprlem7 10978
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10981  ltaprlem 10980
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10982
[Gleason] p. 124Lemma 9-3.6prlem936 10983
[Gleason] p. 124Proposition 9-3.7df-mp 10920  mulclpr 10956  mulclprlem 10955  reclem2pr 10984
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10965
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10960
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10959
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10964
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10987  reclem3pr 10985  reclem4pr 10986
[Gleason] p. 126Proposition 9-4.1df-enr 10991  enrer 10999
[Gleason] p. 126Proposition 9-4.2df-0r 10996  df-1r 10997  df-nr 10992
[Gleason] p. 126Proposition 9-4.3df-mr 10994  df-plr 10993  negexsr 11038  recexsr 11043  recexsrlem 11039
[Gleason] p. 127Proposition 9-4.4df-ltr 10995
[Gleason] p. 130Proposition 10-1.3creui 12148  creur 12147  cru 12145
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11124  axcnre 11100
[Gleason] p. 132Definition 10-3.1crim 15000  crimd 15117  crimi 15078  crre 14999  crred 15116  crrei 15077
[Gleason] p. 132Definition 10-3.2remim 15002  remimd 15083
[Gleason] p. 133Definition 10.36absval2 15169  absval2d 15330  absval2i 15282
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15026  cjaddd 15105  cjaddi 15073
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15027  cjmuld 15106  cjmuli 15074
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15025  cjcjd 15084  cjcji 15056
[Gleason] p. 133Proposition 10-3.4(f)cjre 15024  cjreb 15008  cjrebd 15087  cjrebi 15059  cjred 15111  rere 15007  rereb 15005  rerebd 15086  rerebi 15058  rered 15109
[Gleason] p. 133Proposition 10-3.4(h)addcj 15033  addcjd 15097  addcji 15068
[Gleason] p. 133Proposition 10-3.7(a)absval 15123
[Gleason] p. 133Proposition 10-3.7(b)abscj 15164  abscjd 15335  abscji 15286
[Gleason] p. 133Proposition 10-3.7(c)abs00 15174  abs00d 15331  abs00i 15283  absne0d 15332
[Gleason] p. 133Proposition 10-3.7(d)releabs 15206  releabsd 15336  releabsi 15287
[Gleason] p. 133Proposition 10-3.7(f)absmul 15179  absmuld 15339  absmuli 15289
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15167  sqabsaddi 15290
[Gleason] p. 133Proposition 10-3.7(h)abstri 15215  abstrid 15341  abstrii 15293
[Gleason] p. 134Definition 10-4.1df-exp 13968  exp0 13971  expp1 13974  expp1d 14052
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26034  cxpaddd 26072  expadd 14010  expaddd 14053  expaddz 14012
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26043  cxpmuld 26091  expmul 14013  expmuld 14054  expmulz 14014
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26040  mulcxpd 26083  mulexp 14007  mulexpd 14066  mulexpz 14008
[Gleason] p. 140Exercise 1znnen 16094
[Gleason] p. 141Definition 11-2.1fzval 13426
[Gleason] p. 168Proposition 12-2.1(a)climadd 15514  rlimadd 15525  rlimdiv 15530
[Gleason] p. 168Proposition 12-2.1(b)climsub 15516  rlimsub 15527
[Gleason] p. 168Proposition 12-2.1(c)climmul 15515  rlimmul 15528
[Gleason] p. 171Corollary 12-2.2climmulc2 15519
[Gleason] p. 172Corollary 12-2.5climrecl 15465
[Gleason] p. 172Proposition 12-2.4(c)climabs 15486  climcj 15487  climim 15489  climre 15488  rlimabs 15491  rlimcj 15492  rlimim 15494  rlimre 15493
[Gleason] p. 173Definition 12-3.1df-ltxr 11194  df-xr 11193  ltxr 13036
[Gleason] p. 175Definition 12-4.1df-limsup 15353  limsupval 15356
[Gleason] p. 180Theorem 12-5.1climsup 15554
[Gleason] p. 180Theorem 12-5.3caucvg 15563  caucvgb 15564  caucvgbf 43715  caucvgr 15560  climcau 15555
[Gleason] p. 182Exercise 3cvgcmp 15701
[Gleason] p. 182Exercise 4cvgrat 15768
[Gleason] p. 195Theorem 13-2.12abs1m 15220
[Gleason] p. 217Lemma 13-4.1btwnzge0 13733
[Gleason] p. 223Definition 14-1.1df-met 20790
[Gleason] p. 223Definition 14-1.1(a)met0 23696  xmet0 23695
[Gleason] p. 223Definition 14-1.1(b)metgt0 23712
[Gleason] p. 223Definition 14-1.1(c)metsym 23703
[Gleason] p. 223Definition 14-1.1(d)mettri 23705  mstri 23822  xmettri 23704  xmstri 23821
[Gleason] p. 225Definition 14-1.5xpsmet 23735
[Gleason] p. 230Proposition 14-2.6txlm 22999
[Gleason] p. 240Theorem 14-4.3metcnp4 24674
[Gleason] p. 240Proposition 14-4.2metcnp3 23896
[Gleason] p. 243Proposition 14-4.16addcn 24228  addcn2 15476  mulcn 24230  mulcn2 15478  subcn 24229  subcn2 15477
[Gleason] p. 295Remarkbcval3 14206  bcval4 14207
[Gleason] p. 295Equation 2bcpasc 14221
[Gleason] p. 295Definition of binomial coefficientbcval 14204  df-bc 14203
[Gleason] p. 296Remarkbcn0 14210  bcnn 14212
[Gleason] p. 296Theorem 15-2.8binom 15715
[Gleason] p. 308Equation 2ef0 15973
[Gleason] p. 308Equation 3efcj 15974
[Gleason] p. 309Corollary 15-4.3efne0 15979
[Gleason] p. 309Corollary 15-4.4efexp 15983
[Gleason] p. 310Equation 14sinadd 16046
[Gleason] p. 310Equation 15cosadd 16047
[Gleason] p. 311Equation 17sincossq 16058
[Gleason] p. 311Equation 18cosbnd 16063  sinbnd 16062
[Gleason] p. 311Lemma 15-4.7sqeqor 14120  sqeqori 14118
[Gleason] p. 311Definition of ` `df-pi 15955
[Godowski] p. 730Equation SFgoeqi 31215
[GodowskiGreechie] p. 249Equation IV3oai 30610
[Golan] p. 1Remarksrgisid 19940
[Golan] p. 1Definitiondf-srg 19918
[Golan] p. 149Definitiondf-slmd 32036
[Gonshor] p. 7Definitiondf-scut 27123
[Gonshor] p. 9Theorem 2.5slerec 27158
[Gonshor] p. 10Theorem 2.6cofcut1 27239  cofcut1d 27240
[Gonshor] p. 10Theorem 2.7cofcut2 27241  cofcut2d 27242
[Gonshor] p. 12Theorem 2.9cofcutr 27243  cofcutr1d 27244  cofcutr2d 27245
[Gonshor] p. 13Definitiondf-adds 27272
[Gonshor] p. 14Theorem 3.1addsprop 27288
[Gonshor] p. 15Theorem 3.2addsunif 27310
[GramKnuthPat], p. 47Definition 2.42df-fwddif 34744
[Gratzer] p. 23Section 0.6df-mre 17466
[Gratzer] p. 27Section 0.6df-mri 17468
[Hall] p. 1Section 1.1df-asslaw 46112  df-cllaw 46110  df-comlaw 46111
[Hall] p. 2Section 1.2df-clintop 46124
[Hall] p. 7Section 1.3df-sgrp2 46145
[Halmos] p. 28Partition ` `df-parts 37227  dfmembpart2 37232
[Halmos] p. 31Theorem 17.3riesz1 31007  riesz2 31008
[Halmos] p. 41Definition of Hermitianhmopadj2 30883
[Halmos] p. 42Definition of projector orderingpjordi 31115
[Halmos] p. 43Theorem 26.1elpjhmop 31127  elpjidm 31126  pjnmopi 31090
[Halmos] p. 44Remarkpjinormi 30629  pjinormii 30618
[Halmos] p. 44Theorem 26.2elpjch 31131  pjrn 30649  pjrni 30644  pjvec 30638
[Halmos] p. 44Theorem 26.3pjnorm2 30669
[Halmos] p. 44Theorem 26.4hmopidmpj 31096  hmopidmpji 31094
[Halmos] p. 45Theorem 27.1pjinvari 31133
[Halmos] p. 45Theorem 27.3pjoci 31122  pjocvec 30639
[Halmos] p. 45Theorem 27.4pjorthcoi 31111
[Halmos] p. 48Theorem 29.2pjssposi 31114
[Halmos] p. 48Theorem 29.3pjssdif1i 31117  pjssdif2i 31116
[Halmos] p. 50Definition of spectrumdf-spec 30797
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1797
[Hatcher] p. 25Definitiondf-phtpc 24355  df-phtpy 24334
[Hatcher] p. 26Definitiondf-pco 24368  df-pi1 24371
[Hatcher] p. 26Proposition 1.2phtpcer 24358
[Hatcher] p. 26Proposition 1.3pi1grp 24413
[Hefferon] p. 240Definition 3.12df-dmat 21839  df-dmatalt 46469
[Helfgott] p. 2Theoremtgoldbach 45999
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 45984
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 45996  bgoldbtbnd 45991  bgoldbtbnd 45991  tgblthelfgott 45997
[Helfgott] p. 5Proposition 1.1circlevma 33255
[Helfgott] p. 69Statement 7.49circlemethhgt 33256
[Helfgott] p. 69Statement 7.50hgt750lema 33270  hgt750lemb 33269  hgt750leme 33271  hgt750lemf 33266  hgt750lemg 33267
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 45993  tgoldbachgt 33276  tgoldbachgtALTV 45994  tgoldbachgtd 33275
[Helfgott] p. 70Statement 7.49ax-hgt749 33257
[Herstein] p. 54Exercise 28df-grpo 29435
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18759  grpoideu 29451  mndideu 18567
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18785  grpoinveu 29461
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18814  grpo2inv 29473
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18825  grpoinvop 29475
[Herstein] p. 57Exercise 1dfgrp3e 18847
[Hitchcock] p. 5Rule A3mptnan 1770
[Hitchcock] p. 5Rule A4mptxor 1771
[Hitchcock] p. 5Rule A5mtpxor 1773
[Holland] p. 1519Theorem 2sumdmdi 31362
[Holland] p. 1520Lemma 5cdj1i 31375  cdj3i 31383  cdj3lem1 31376  cdjreui 31374
[Holland] p. 1524Lemma 7mddmdin0i 31373
[Holland95] p. 13Theorem 3.6hlathil 40428
[Holland95] p. 14Line 15hgmapvs 40354
[Holland95] p. 14Line 16hdmaplkr 40376
[Holland95] p. 14Line 17hdmapellkr 40377
[Holland95] p. 14Line 19hdmapglnm2 40374
[Holland95] p. 14Line 20hdmapip0com 40380
[Holland95] p. 14Theorem 3.6hdmapevec2 40299
[Holland95] p. 14Lines 24 and 25hdmapoc 40394
[Holland95] p. 204Definition of involutiondf-srng 20305
[Holland95] p. 212Definition of subspacedf-psubsp 37966
[Holland95] p. 214Lemma 3.3lclkrlem2v 39991
[Holland95] p. 214Definition 3.2df-lpolN 39944
[Holland95] p. 214Definition of nonsingularpnonsingN 38396
[Holland95] p. 215Lemma 3.3(1)dihoml4 39840  poml4N 38416
[Holland95] p. 215Lemma 3.3(2)dochexmid 39931  pexmidALTN 38441  pexmidN 38432
[Holland95] p. 218Theorem 3.6lclkr 39996
[Holland95] p. 218Definition of dual vector spacedf-ldual 37586  ldualset 37587
[Holland95] p. 222Item 1df-lines 37964  df-pointsN 37965
[Holland95] p. 222Item 2df-polarityN 38366
[Holland95] p. 223Remarkispsubcl2N 38410  omllaw4 37708  pol1N 38373  polcon3N 38380
[Holland95] p. 223Definitiondf-psubclN 38398
[Holland95] p. 223Equation for polaritypolval2N 38369
[Holmes] p. 40Definitiondf-xrn 36833
[Hughes] p. 44Equation 1.21bax-his3 30026
[Hughes] p. 47Definition of projection operatordfpjop 31124
[Hughes] p. 49Equation 1.30eighmre 30905  eigre 30777  eigrei 30776
[Hughes] p. 49Equation 1.31eighmorth 30906  eigorth 30780  eigorthi 30779
[Hughes] p. 137Remark (ii)eigposi 30778
[Huneke] p. 1Claim 1frgrncvvdeq 29253
[Huneke] p. 1Statement 1frgrncvvdeqlem7 29249
[Huneke] p. 1Statement 2frgrncvvdeqlem8 29250
[Huneke] p. 1Statement 3frgrncvvdeqlem9 29251
[Huneke] p. 2Claim 2frgrregorufr 29269  frgrregorufr0 29268  frgrregorufrg 29270
[Huneke] p. 2Claim 3frgrhash2wsp 29276  frrusgrord 29285  frrusgrord0 29284
[Huneke] p. 2Statementdf-clwwlknon 29032
[Huneke] p. 2Statement 4frgrwopreglem4 29259
[Huneke] p. 2Statement 5frgrwopreg1 29262  frgrwopreg2 29263  frgrwopregasn 29260  frgrwopregbsn 29261
[Huneke] p. 2Statement 6frgrwopreglem5 29265
[Huneke] p. 2Statement 7fusgreghash2wspv 29279
[Huneke] p. 2Statement 8fusgreghash2wsp 29282
[Huneke] p. 2Statement 9clwlksndivn 29030  numclwlk1 29315  numclwlk1lem1 29313  numclwlk1lem2 29314  numclwwlk1 29305  numclwwlk8 29336
[Huneke] p. 2Definition 3frgrwopreglem1 29256
[Huneke] p. 2Definition 4df-clwlks 28719
[Huneke] p. 2Definition 62clwwlk 29291
[Huneke] p. 2Definition 7numclwwlkovh 29317  numclwwlkovh0 29316
[Huneke] p. 2Statement 10numclwwlk2 29325
[Huneke] p. 2Statement 11rusgrnumwlkg 28922
[Huneke] p. 2Statement 12numclwwlk3 29329
[Huneke] p. 2Statement 13numclwwlk5 29332
[Huneke] p. 2Statement 14numclwwlk7 29335
[Indrzejczak] p. 33Definition ` `Enatded 29347  natded 29347
[Indrzejczak] p. 33Definition ` `Inatded 29347
[Indrzejczak] p. 34Definition ` `Enatded 29347  natded 29347
[Indrzejczak] p. 34Definition ` `Inatded 29347
[Jech] p. 4Definition of classcv 1540  cvjust 2730
[Jech] p. 42Lemma 6.1alephexp1 10515
[Jech] p. 42Equation 6.1alephadd 10513  alephmul 10514
[Jech] p. 43Lemma 6.2infmap 10512  infmap2 10154
[Jech] p. 71Lemma 9.3jech9.3 9750
[Jech] p. 72Equation 9.3scott0 9822  scottex 9821
[Jech] p. 72Exercise 9.1rankval4 9803
[Jech] p. 72Scheme "Collection Principle"cp 9827
[Jech] p. 78Noteopthprc 5696
[JonesMatijasevic] p. 694Definition 2.3rmxyval 41225
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 41313
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 41314
[JonesMatijasevic] p. 695Equation 2.7rmxadd 41237
[JonesMatijasevic] p. 695Equation 2.8rmyadd 41241
[JonesMatijasevic] p. 695Equation 2.9rmxp1 41242  rmyp1 41243
[JonesMatijasevic] p. 695Equation 2.10rmxm1 41244  rmym1 41245
[JonesMatijasevic] p. 695Equation 2.11rmx0 41235  rmx1 41236  rmxluc 41246
[JonesMatijasevic] p. 695Equation 2.12rmy0 41239  rmy1 41240  rmyluc 41247
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 41249
[JonesMatijasevic] p. 695Equation 2.14rmydbl 41250
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 41270  jm2.17b 41271  jm2.17c 41272
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 41303
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 41307
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 41298
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 41273  jm2.24nn 41269
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 41312
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 41318  rmygeid 41274
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 41330
[Juillerat] p. 11Section *5etransc 44514  etransclem47 44512  etransclem48 44513
[Juillerat] p. 12Equation (7)etransclem44 44509
[Juillerat] p. 12Equation *(7)etransclem46 44511
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 44497
[Juillerat] p. 13Proofetransclem35 44500
[Juillerat] p. 13Part of case 2 proven inetransclem38 44503
[Juillerat] p. 13Part of case 2 provenetransclem24 44489
[Juillerat] p. 13Part of case 2: proven inetransclem41 44506
[Juillerat] p. 14Proofetransclem23 44488
[KalishMontague] p. 81Note 1ax-6 1971
[KalishMontague] p. 85Lemma 2equid 2015
[KalishMontague] p. 85Lemma 3equcomi 2020
[KalishMontague] p. 86Lemma 7cbvalivw 2010  cbvaliw 2009  wl-cbvmotv 35972  wl-motae 35974  wl-moteq 35973
[KalishMontague] p. 87Lemma 8spimvw 1999  spimw 1974
[KalishMontague] p. 87Lemma 9spfw 2036  spw 2037
[Kalmbach] p. 14Definition of latticechabs1 30458  chabs1i 30460  chabs2 30459  chabs2i 30461  chjass 30475  chjassi 30428  latabs1 18364  latabs2 18365
[Kalmbach] p. 15Definition of atomdf-at 31280  ela 31281
[Kalmbach] p. 15Definition of coverscvbr2 31225  cvrval2 37736
[Kalmbach] p. 16Definitiondf-ol 37640  df-oml 37641
[Kalmbach] p. 20Definition of commutescmbr 30526  cmbri 30532  cmtvalN 37673  df-cm 30525  df-cmtN 37639
[Kalmbach] p. 22Remarkomllaw5N 37709  pjoml5 30555  pjoml5i 30530
[Kalmbach] p. 22Definitionpjoml2 30553  pjoml2i 30527
[Kalmbach] p. 22Theorem 2(v)cmcm 30556  cmcmi 30534  cmcmii 30539  cmtcomN 37711
[Kalmbach] p. 22Theorem 2(ii)omllaw3 37707  omlsi 30346  pjoml 30378  pjomli 30377
[Kalmbach] p. 22Definition of OML lawomllaw2N 37706
[Kalmbach] p. 23Remarkcmbr2i 30538  cmcm3 30557  cmcm3i 30536  cmcm3ii 30541  cmcm4i 30537  cmt3N 37713  cmt4N 37714  cmtbr2N 37715
[Kalmbach] p. 23Lemma 3cmbr3 30550  cmbr3i 30542  cmtbr3N 37716
[Kalmbach] p. 25Theorem 5fh1 30560  fh1i 30563  fh2 30561  fh2i 30564  omlfh1N 37720
[Kalmbach] p. 65Remarkchjatom 31299  chslej 30440  chsleji 30400  shslej 30322  shsleji 30312
[Kalmbach] p. 65Proposition 1chocin 30437  chocini 30396  chsupcl 30282  chsupval2 30352  h0elch 30197  helch 30185  hsupval2 30351  ocin 30238  ococss 30235  shococss 30236
[Kalmbach] p. 65Definition of subspace sumshsval 30254
[Kalmbach] p. 66Remarkdf-pjh 30337  pjssmi 31107  pjssmii 30623
[Kalmbach] p. 67Lemma 3osum 30587  osumi 30584
[Kalmbach] p. 67Lemma 4pjci 31142
[Kalmbach] p. 103Exercise 6atmd2 31342
[Kalmbach] p. 103Exercise 12mdsl0 31252
[Kalmbach] p. 140Remarkhatomic 31302  hatomici 31301  hatomistici 31304
[Kalmbach] p. 140Proposition 1atlatmstc 37781
[Kalmbach] p. 140Proposition 1(i)atexch 31323  lsatexch 37505
[Kalmbach] p. 140Proposition 1(ii)chcv1 31297  cvlcvr1 37801  cvr1 37873
[Kalmbach] p. 140Proposition 1(iii)cvexch 31316  cvexchi 31311  cvrexch 37883
[Kalmbach] p. 149Remark 2chrelati 31306  hlrelat 37865  hlrelat5N 37864  lrelat 37476
[Kalmbach] p. 153Exercise 5lsmcv 20602  lsmsatcv 37472  spansncv 30595  spansncvi 30594
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 37491  spansncv2 31235
[Kalmbach] p. 266Definitiondf-st 31153
[Kalmbach2] p. 8Definition of adjointdf-adjh 30791
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10582  fpwwe2 10579
[KanamoriPincus] p. 416Corollary 1.3canth4 10583
[KanamoriPincus] p. 417Corollary 1.6canthp1 10590
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10585
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10587
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10600
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10604  gchxpidm 10605
[KanamoriPincus] p. 419Theorem 2.1gchacg 10616  gchhar 10615
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10152  unxpwdom 9525
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10606
[Kreyszig] p. 3Property M1metcl 23685  xmetcl 23684
[Kreyszig] p. 4Property M2meteq0 23692
[Kreyszig] p. 8Definition 1.1-8dscmet 23928
[Kreyszig] p. 12Equation 5conjmul 11872  muleqadd 11799
[Kreyszig] p. 18Definition 1.3-2mopnval 23791
[Kreyszig] p. 19Remarkmopntopon 23792
[Kreyszig] p. 19Theorem T1mopn0 23854  mopnm 23797
[Kreyszig] p. 19Theorem T2unimopn 23852
[Kreyszig] p. 19Definition of neighborhoodneibl 23857
[Kreyszig] p. 20Definition 1.3-3metcnp2 23898
[Kreyszig] p. 25Definition 1.4-1lmbr 22609  lmmbr 24622  lmmbr2 24623
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 22731
[Kreyszig] p. 28Theorem 1.4-5lmcau 24677
[Kreyszig] p. 28Definition 1.4-3iscau 24640  iscmet2 24658
[Kreyszig] p. 30Theorem 1.4-7cmetss 24680
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 22812  metelcls 24669
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 24670  metcld2 24671
[Kreyszig] p. 51Equation 2clmvneg1 24462  lmodvneg1 20365  nvinv 29581  vcm 29518
[Kreyszig] p. 51Equation 1aclm0vs 24458  lmod0vs 20355  slmd0vs 32059  vc0 29516
[Kreyszig] p. 51Equation 1blmodvs0 20356  slmdvs0 32060  vcz 29517
[Kreyszig] p. 58Definition 2.2-1imsmet 29633  ngpmet 23959  nrmmetd 23930
[Kreyszig] p. 59Equation 1imsdval 29628  imsdval2 29629  ncvspds 24525  ngpds 23960
[Kreyszig] p. 63Problem 1nmval 23945  nvnd 29630
[Kreyszig] p. 64Problem 2nmeq0 23974  nmge0 23973  nvge0 29615  nvz 29611
[Kreyszig] p. 64Problem 3nmrtri 23980  nvabs 29614
[Kreyszig] p. 91Definition 2.7-1isblo3i 29743
[Kreyszig] p. 92Equation 2df-nmoo 29687
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 29749  blocni 29747
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 29748
[Kreyszig] p. 129Definition 3.1-1cphipeq0 24568  ipeq0 21042  ipz 29661
[Kreyszig] p. 135Problem 2cphpyth 24580  pythi 29792
[Kreyszig] p. 137Lemma 3-2.1(a)sii 29796
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 24602
[Kreyszig] p. 144Equation 4supcvg 15741
[Kreyszig] p. 144Theorem 3.3-1minvec 24800  minveco 29826
[Kreyszig] p. 196Definition 3.9-1df-aj 29692
[Kreyszig] p. 247Theorem 4.7-2bcth 24693
[Kreyszig] p. 249Theorem 4.7-3ubth 29815
[Kreyszig] p. 470Definition of positive operator orderingleop 31065  leopg 31064
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 31083
[Kreyszig] p. 525Theorem 10.1-1htth 29860
[Kulpa] p. 547Theorempoimir 36111
[Kulpa] p. 547Equation (1)poimirlem32 36110
[Kulpa] p. 547Equation (2)poimirlem31 36109
[Kulpa] p. 548Theorembroucube 36112
[Kulpa] p. 548Equation (6)poimirlem26 36104
[Kulpa] p. 548Equation (7)poimirlem27 36105
[Kunen] p. 10Axiom 0ax6e 2381  axnul 5262
[Kunen] p. 11Axiom 3axnul 5262
[Kunen] p. 12Axiom 6zfrep6 7887
[Kunen] p. 24Definition 10.24mapval 8777  mapvalg 8775
[Kunen] p. 30Lemma 10.20fodomg 10458
[Kunen] p. 31Definition 10.24mapex 8771
[Kunen] p. 95Definition 2.1df-r1 9700
[Kunen] p. 97Lemma 2.10r1elss 9742  r1elssi 9741
[Kunen] p. 107Exercise 4rankop 9794  rankopb 9788  rankuni 9799  rankxplim 9815  rankxpsuc 9818
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4966
[Lang] , p. 225Corollary 1.3finexttrb 32351
[Lang] p. Definitiondf-rn 5644
[Lang] p. 3Statementlidrideqd 18524  mndbn0 18572
[Lang] p. 3Definitiondf-mnd 18557
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18542
[Lang] p. 4Property of composites. Second formulagsumccat 18651
[Lang] p. 5Equationgsumreidx 19694
[Lang] p. 5Definition of an (infinite) productgsumfsupp 46106
[Lang] p. 6Examplenn0mnd 46103
[Lang] p. 6Equationgsumxp2 19757
[Lang] p. 6Statementcycsubm 18995
[Lang] p. 6Definitionmulgnn0gsum 18882
[Lang] p. 6Observationmndlsmidm 19452
[Lang] p. 7Definitiondfgrp2e 18776
[Lang] p. 30Definitiondf-tocyc 31956
[Lang] p. 32Property (a)cyc3genpm 32001
[Lang] p. 32Property (b)cyc3conja 32006  cycpmconjv 31991
[Lang] p. 53Definitiondf-cat 17548
[Lang] p. 53Axiom CAT 1cat1 17983  cat1lem 17982
[Lang] p. 54Definitiondf-iso 17632
[Lang] p. 57Definitiondf-inito 17870  df-termo 17871
[Lang] p. 58Exampleirinitoringc 46357
[Lang] p. 58Statementinitoeu1 17897  termoeu1 17904
[Lang] p. 62Definitiondf-func 17744
[Lang] p. 65Definitiondf-nat 17830
[Lang] p. 91Notedf-ringc 46293
[Lang] p. 92Statementmxidlprm 32237
[Lang] p. 92Definitionisprmidlc 32220
[Lang] p. 128Remarkdsmmlmod 21151
[Lang] p. 129Prooflincscm 46501  lincscmcl 46503  lincsum 46500  lincsumcl 46502
[Lang] p. 129Statementlincolss 46505
[Lang] p. 129Observationdsmmfi 21144
[Lang] p. 141Theorem 5.3dimkerim 32322  qusdimsum 32323
[Lang] p. 141Corollary 5.4lssdimle 32305
[Lang] p. 147Definitionsnlindsntor 46542
[Lang] p. 504Statementmat1 21796  matring 21792
[Lang] p. 504Definitiondf-mamu 21733
[Lang] p. 505Statementmamuass 21749  mamutpos 21807  matassa 21793  mattposvs 21804  tposmap 21806
[Lang] p. 513Definitionmdet1 21950  mdetf 21944
[Lang] p. 513Theorem 4.4cramer 22040
[Lang] p. 514Proposition 4.6mdetleib 21936
[Lang] p. 514Proposition 4.8mdettpos 21960
[Lang] p. 515Definitiondf-minmar1 21984  smadiadetr 22024
[Lang] p. 515Corollary 4.9mdetero 21959  mdetralt 21957
[Lang] p. 517Proposition 4.15mdetmul 21972
[Lang] p. 518Definitiondf-madu 21983
[Lang] p. 518Proposition 4.16madulid 21994  madurid 21993  matinv 22026
[Lang] p. 561Theorem 3.1cayleyhamilton 22239
[Lang], p. 224Proposition 1.2extdgmul 32350  fedgmul 32326
[Lang], p. 561Remarkchpmatply1 22181
[Lang], p. 561Definitiondf-chpmat 22176
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 42604
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 42599
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 42605
[LeBlanc] p. 277Rule R2axnul 5262
[Levy] p. 12Axiom 4.3.1df-clab 2714
[Levy] p. 59Definitiondf-ttrcl 9644
[Levy] p. 64Theorem 5.6(ii)frinsg 9687
[Levy] p. 338Axiomdf-clel 2814  df-cleq 2728
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2814  df-cleq 2728
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2714
[Levy] p. 358Axiomdf-clab 2714
[Levy58] p. 2Definition Iisfin1-3 10322
[Levy58] p. 2Definition IIdf-fin2 10222
[Levy58] p. 2Definition Iadf-fin1a 10221
[Levy58] p. 2Definition IIIdf-fin3 10224
[Levy58] p. 3Definition Vdf-fin5 10225
[Levy58] p. 3Definition IVdf-fin4 10223
[Levy58] p. 4Definition VIdf-fin6 10226
[Levy58] p. 4Definition VIIdf-fin7 10227
[Levy58], p. 3Theorem 1fin1a2 10351
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27034
[Lipparini] p. 3Lemma 2.1.4noresle 27045
[Lipparini] p. 6Proposition 4.2noinfbnd1 27077  nosupbnd1 27062
[Lipparini] p. 6Proposition 4.3noinfbnd2 27079  nosupbnd2 27064
[Lipparini] p. 7Theorem 5.1noetasuplem3 27083  noetasuplem4 27084
[Lipparini] p. 7Corollary 4.4nosupinfsep 27080
[Lopez-Astorga] p. 12Rule 1mptnan 1770
[Lopez-Astorga] p. 12Rule 2mptxor 1771
[Lopez-Astorga] p. 12Rule 3mtpxor 1773
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 31350
[Maeda] p. 168Lemma 5mdsym 31354  mdsymi 31353
[Maeda] p. 168Lemma 4(i)mdsymlem4 31348  mdsymlem6 31350  mdsymlem7 31351
[Maeda] p. 168Lemma 4(ii)mdsymlem8 31352
[MaedaMaeda] p. 1Remarkssdmd1 31255  ssdmd2 31256  ssmd1 31253  ssmd2 31254
[MaedaMaeda] p. 1Lemma 1.2mddmd2 31251
[MaedaMaeda] p. 1Definition 1.1df-dmd 31223  df-md 31222  mdbr 31236
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 31273  mdslj1i 31261  mdslj2i 31262  mdslle1i 31259  mdslle2i 31260  mdslmd1i 31271  mdslmd2i 31272
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 31263  mdsl2bi 31265  mdsl2i 31264
[MaedaMaeda] p. 2Lemma 1.6mdexchi 31277
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 31274
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 31275
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 31252
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 31257  mdsl3 31258
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 31276
[MaedaMaeda] p. 4Theorem 1.14mdcompli 31371
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 37783  hlrelat1 37863
[MaedaMaeda] p. 31Lemma 7.5lcvexch 37501
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 31278  cvmdi 31266  cvnbtwn4 31231  cvrnbtwn4 37741
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 31279
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 37802  cvp 31317  cvrp 37879  lcvp 37502
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 31341
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 31340
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 37795  hlexch4N 37855
[MaedaMaeda] p. 34Exercise 7.1atabsi 31343
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 37906
[MaedaMaeda] p. 61Definition 15.10psubN 38212  atpsubN 38216  df-pointsN 37965  pointpsubN 38214
[MaedaMaeda] p. 62Theorem 15.5df-pmap 37967  pmap11 38225  pmaple 38224  pmapsub 38231  pmapval 38220
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 38228  pmap1N 38230
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 38233  pmapglb2N 38234  pmapglb2xN 38235  pmapglbx 38232
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 38315
[MaedaMaeda] p. 67Postulate PS1ps-1 37940
[MaedaMaeda] p. 68Lemma 16.2df-padd 38259  paddclN 38305  paddidm 38304
[MaedaMaeda] p. 68Condition PS2ps-2 37941
[MaedaMaeda] p. 68Equation 16.2.1paddass 38301
[MaedaMaeda] p. 69Lemma 16.4ps-1 37940
[MaedaMaeda] p. 69Theorem 16.4ps-2 37941
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19457  lsmmod2 19458  lssats 37474  shatomici 31300  shatomistici 31303  shmodi 30332  shmodsi 30331
[MaedaMaeda] p. 130Remark 29.6dmdmd 31242  mdsymlem7 31351
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 30531
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 30435
[MaedaMaeda] p. 139Remarksumdmdii 31357
[Margaris] p. 40Rule Cexlimiv 1933
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 397  df-ex 1782  df-or 846  dfbi2 475
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 29344
[Margaris] p. 59Section 14notnotrALTVD 43187
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 43188
[Margaris] p. 79Rule Cexinst01 42897  exinst11 42898
[Margaris] p. 89Theorem 19.219.2 1980  19.2g 2181  r19.2z 4452
[Margaris] p. 89Theorem 19.319.3 2195  rr19.3v 3619
[Margaris] p. 89Theorem 19.5alcom 2156
[Margaris] p. 89Theorem 19.6alex 1828
[Margaris] p. 89Theorem 19.7alnex 1783
[Margaris] p. 89Theorem 19.819.8a 2174
[Margaris] p. 89Theorem 19.919.9 2198  19.9h 2282  exlimd 2211  exlimdh 2286
[Margaris] p. 89Theorem 19.11excom 2162  excomim 2163
[Margaris] p. 89Theorem 19.1219.12 2320
[Margaris] p. 90Section 19conventions-labels 29345  conventions-labels 29345  conventions-labels 29345  conventions-labels 29345
[Margaris] p. 90Theorem 19.14exnal 1829
[Margaris] p. 90Theorem 19.152albi 42648  albi 1820
[Margaris] p. 90Theorem 19.1619.16 2218
[Margaris] p. 90Theorem 19.1719.17 2219
[Margaris] p. 90Theorem 19.182exbi 42650  exbi 1849
[Margaris] p. 90Theorem 19.1919.19 2222
[Margaris] p. 90Theorem 19.202alim 42647  2alimdv 1921  alimd 2205  alimdh 1819  alimdv 1919  ax-4 1811  ralimdaa 3243  ralimdv 3166  ralimdva 3164  ralimdvva 3201  sbcimdv 3813
[Margaris] p. 90Theorem 19.2119.21 2200  19.21h 2283  19.21t 2199  19.21vv 42646  alrimd 2208  alrimdd 2207  alrimdh 1866  alrimdv 1932  alrimi 2206  alrimih 1826  alrimiv 1930  alrimivv 1931  hbralrimi 3141  r19.21be 3235  r19.21bi 3234  ralrimd 3247  ralrimdv 3149  ralrimdva 3151  ralrimdvv 3198  ralrimdvva 3203  ralrimi 3240  ralrimia 3241  ralrimiv 3142  ralrimiva 3143  ralrimivv 3195  ralrimivva 3197  ralrimivvva 3200  ralrimivw 3147
[Margaris] p. 90Theorem 19.222exim 42649  2eximdv 1922  exim 1836  eximd 2209  eximdh 1867  eximdv 1920  rexim 3090  reximd2a 3252  reximdai 3244  reximdd 43352  reximddv 3168  reximddv2 3206  reximddv3 43351  reximdv 3167  reximdv2 3161  reximdva 3165  reximdvai 3162  reximdvva 3202  reximi2 3082
[Margaris] p. 90Theorem 19.2319.23 2204  19.23bi 2184  19.23h 2284  19.23t 2203  exlimdv 1936  exlimdvv 1937  exlimexi 42796  exlimiv 1933  exlimivv 1935  rexlimd3 43344  rexlimdv 3150  rexlimdv3a 3156  rexlimdva 3152  rexlimdva2 3154  rexlimdvaa 3153  rexlimdvv 3204  rexlimdvva 3205  rexlimdvw 3157  rexlimiv 3145  rexlimiva 3144  rexlimivv 3196
[Margaris] p. 90Theorem 19.2419.24 1989
[Margaris] p. 90Theorem 19.2519.25 1883
[Margaris] p. 90Theorem 19.2619.26 1873
[Margaris] p. 90Theorem 19.2719.27 2220  r19.27z 4462  r19.27zv 4463
[Margaris] p. 90Theorem 19.2819.28 2221  19.28vv 42656  r19.28z 4455  r19.28zf 43364  r19.28zv 4458  rr19.28v 3620
[Margaris] p. 90Theorem 19.2919.29 1876  r19.29d2r 3137  r19.29imd 3121
[Margaris] p. 90Theorem 19.3019.30 1884
[Margaris] p. 90Theorem 19.3119.31 2227  19.31vv 42654
[Margaris] p. 90Theorem 19.3219.32 2226  r19.32 45320
[Margaris] p. 90Theorem 19.3319.33-2 42652  19.33 1887
[Margaris] p. 90Theorem 19.3419.34 1990
[Margaris] p. 90Theorem 19.3519.35 1880
[Margaris] p. 90Theorem 19.3619.36 2223  19.36vv 42653  r19.36zv 4464
[Margaris] p. 90Theorem 19.3719.37 2225  19.37vv 42655  r19.37zv 4459
[Margaris] p. 90Theorem 19.3819.38 1841
[Margaris] p. 90Theorem 19.3919.39 1988
[Margaris] p. 90Theorem 19.4019.40-2 1890  19.40 1889  r19.40 3122
[Margaris] p. 90Theorem 19.4119.41 2228  19.41rg 42822
[Margaris] p. 90Theorem 19.4219.42 2229
[Margaris] p. 90Theorem 19.4319.43 1885
[Margaris] p. 90Theorem 19.4419.44 2230  r19.44zv 4461
[Margaris] p. 90Theorem 19.4519.45 2231  r19.45zv 4460
[Margaris] p. 110Exercise 2(b)eu1 2610
[Mayet] p. 370Remarkjpi 31212  largei 31209  stri 31199
[Mayet3] p. 9Definition of CH-statesdf-hst 31154  ishst 31156
[Mayet3] p. 10Theoremhstrbi 31208  hstri 31207
[Mayet3] p. 1223Theorem 4.1mayete3i 30670
[Mayet3] p. 1240Theorem 7.1mayetes3i 30671
[MegPav2000] p. 2344Theorem 3.3stcltrthi 31220
[MegPav2000] p. 2345Definition 3.4-1chintcl 30274  chsupcl 30282
[MegPav2000] p. 2345Definition 3.4-2hatomic 31302
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 31296
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 31323
[MegPav2000] p. 2366Figure 7pl42N 38446
[MegPav2002] p. 362Lemma 2.2latj31 18376  latj32 18374  latjass 18372
[Megill] p. 444Axiom C5ax-5 1913  ax5ALT 37369
[Megill] p. 444Section 7conventions 29344
[Megill] p. 445Lemma L12aecom-o 37363  ax-c11n 37350  axc11n 2424
[Megill] p. 446Lemma L17equtrr 2025
[Megill] p. 446Lemma L18ax6fromc10 37358
[Megill] p. 446Lemma L19hbnae-o 37390  hbnae 2430
[Megill] p. 447Remark 9.1dfsb1 2483  sbid 2247  sbidd-misc 47154  sbidd 47153
[Megill] p. 448Remark 9.6axc14 2461
[Megill] p. 448Scheme C4'ax-c4 37346
[Megill] p. 448Scheme C5'ax-c5 37345  sp 2176
[Megill] p. 448Scheme C6'ax-11 2154
[Megill] p. 448Scheme C7'ax-c7 37347
[Megill] p. 448Scheme C8'ax-7 2011
[Megill] p. 448Scheme C9'ax-c9 37352
[Megill] p. 448Scheme C10'ax-6 1971  ax-c10 37348
[Megill] p. 448Scheme C11'ax-c11 37349
[Megill] p. 448Scheme C12'ax-8 2108
[Megill] p. 448Scheme C13'ax-9 2116
[Megill] p. 448Scheme C14'ax-c14 37353
[Megill] p. 448Scheme C15'ax-c15 37351
[Megill] p. 448Scheme C16'ax-c16 37354
[Megill] p. 448Theorem 9.4dral1-o 37366  dral1 2437  dral2-o 37392  dral2 2436  drex1 2439  drex2 2440  drsb1 2497  drsb2 2257
[Megill] p. 449Theorem 9.7sbcom2 2161  sbequ 2086  sbid2v 2511
[Megill] p. 450Example in Appendixhba1-o 37359  hba1 2289
[Mendelson] p. 35Axiom A3hirstL-ax3 45117
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3835  rspsbca 3836  stdpc4 2071
[Mendelson] p. 69Axiom 5ax-c4 37346  ra4 3842  stdpc5 2201
[Mendelson] p. 81Rule Cexlimiv 1933
[Mendelson] p. 95Axiom 6stdpc6 2031
[Mendelson] p. 95Axiom 7stdpc7 2242
[Mendelson] p. 225Axiom system NBGru 3738
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5471
[Mendelson] p. 231Exercise 4.10(k)inv1 4354
[Mendelson] p. 231Exercise 4.10(l)unv 4355
[Mendelson] p. 231Exercise 4.10(n)dfin3 4226
[Mendelson] p. 231Exercise 4.10(o)df-nul 4283
[Mendelson] p. 231Exercise 4.10(q)dfin4 4227
[Mendelson] p. 231Exercise 4.10(s)ddif 4096
[Mendelson] p. 231Definition of uniondfun3 4225
[Mendelson] p. 235Exercise 4.12(c)univ 5408
[Mendelson] p. 235Exercise 4.12(d)pwv 4862
[Mendelson] p. 235Exercise 4.12(j)pwin 5527
[Mendelson] p. 235Exercise 4.12(k)pwunss 4578
[Mendelson] p. 235Exercise 4.12(l)pwssun 5528
[Mendelson] p. 235Exercise 4.12(n)uniin 4892
[Mendelson] p. 235Exercise 4.12(p)reli 5782
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6220
[Mendelson] p. 244Proposition 4.8(g)epweon 7709
[Mendelson] p. 246Definition of successordf-suc 6323
[Mendelson] p. 250Exercise 4.36oelim2 8542
[Mendelson] p. 254Proposition 4.22(b)xpen 9084
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8999  xpsneng 9000
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9007  xpcomeng 9008
[Mendelson] p. 254Proposition 4.22(e)xpassen 9010
[Mendelson] p. 255Definitionbrsdom 8915
[Mendelson] p. 255Exercise 4.39endisj 9002
[Mendelson] p. 255Exercise 4.41mapprc 8769
[Mendelson] p. 255Exercise 4.43mapsnen 8981  mapsnend 8980
[Mendelson] p. 255Exercise 4.45mapunen 9090
[Mendelson] p. 255Exercise 4.47xpmapen 9089
[Mendelson] p. 255Exercise 4.42(a)map0e 8820
[Mendelson] p. 255Exercise 4.42(b)map1 8984
[Mendelson] p. 257Proposition 4.24(a)undom 9003
[Mendelson] p. 258Exercise 4.56(c)djuassen 10114  djucomen 10113
[Mendelson] p. 258Exercise 4.56(f)djudom1 10118
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10112
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8477
[Mendelson] p. 266Proposition 4.34(f)oaordex 8505
[Mendelson] p. 275Proposition 4.42(d)entri3 10495
[Mendelson] p. 281Definitiondf-r1 9700
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9749
[Mendelson] p. 287Axiom system MKru 3738
[MertziosUnger] p. 152Definitiondf-frgr 29203
[MertziosUnger] p. 153Remark 1frgrconngr 29238
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 29240  vdgn1frgrv3 29241
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 29242
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 29235
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 29228  2pthfrgrrn 29226  2pthfrgrrn2 29227
[Mittelstaedt] p. 9Definitiondf-oc 30194
[Monk1] p. 22Remarkconventions 29344
[Monk1] p. 22Theorem 3.1conventions 29344
[Monk1] p. 26Theorem 2.8(vii)ssin 4190
[Monk1] p. 33Theorem 3.2(i)ssrel 5738  ssrelf 31534
[Monk1] p. 33Theorem 3.2(ii)eqrel 5740
[Monk1] p. 34Definition 3.3df-opab 5168
[Monk1] p. 36Theorem 3.7(i)coi1 6214  coi2 6215
[Monk1] p. 36Theorem 3.8(v)dm0 5876  rn0 5881
[Monk1] p. 36Theorem 3.7(ii)cnvi 6094
[Monk1] p. 37Theorem 3.13(i)relxp 5651
[Monk1] p. 37Theorem 3.13(x)dmxp 5884  rnxp 6122
[Monk1] p. 37Theorem 3.13(ii)0xp 5730  xp0 6110
[Monk1] p. 38Theorem 3.16(ii)ima0 6029
[Monk1] p. 38Theorem 3.16(viii)imai 6026
[Monk1] p. 39Theorem 3.17imaex 7853  imaexALTV 36791  imaexg 7852
[Monk1] p. 39Theorem 3.16(xi)imassrn 6024
[Monk1] p. 41Theorem 4.3(i)fnopfv 7026  funfvop 7000
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6898
[Monk1] p. 42Theorem 4.4(iii)fvelima 6908
[Monk1] p. 43Theorem 4.6funun 6547
[Monk1] p. 43Theorem 4.8(iv)dff13 7202  dff13f 7203
[Monk1] p. 46Theorem 4.15(v)funex 7169  funrnex 7886
[Monk1] p. 50Definition 5.4fniunfv 7194
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6179
[Monk1] p. 52Theorem 5.11(viii)ssint 4925
[Monk1] p. 52Definition 5.13 (i)1stval2 7938  df-1st 7921
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7939  df-2nd 7922
[Monk1] p. 112Theorem 15.17(v)ranksn 9790  ranksnb 9763
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9791
[Monk1] p. 112Theorem 15.17(iii)rankun 9792  rankunb 9786
[Monk1] p. 113Theorem 15.18r1val3 9774
[Monk1] p. 113Definition 15.19df-r1 9700  r1val2 9773
[Monk1] p. 117Lemmazorn2 10442  zorn2g 10439
[Monk1] p. 133Theorem 18.11cardom 9922
[Monk1] p. 133Theorem 18.12canth3 10497
[Monk1] p. 133Theorem 18.14carduni 9917
[Monk2] p. 105Axiom C4ax-4 1811
[Monk2] p. 105Axiom C7ax-7 2011
[Monk2] p. 105Axiom C8ax-12 2171  ax-c15 37351  ax12v2 2173
[Monk2] p. 108Lemma 5ax-c4 37346
[Monk2] p. 109Lemma 12ax-11 2154
[Monk2] p. 109Lemma 15equvini 2453  equvinv 2032  eqvinop 5444
[Monk2] p. 113Axiom C5-1ax-5 1913  ax5ALT 37369
[Monk2] p. 113Axiom C5-2ax-10 2137
[Monk2] p. 113Axiom C5-3ax-11 2154
[Monk2] p. 114Lemma 21sp 2176
[Monk2] p. 114Lemma 22axc4 2314  hba1-o 37359  hba1 2289
[Monk2] p. 114Lemma 23nfia1 2150
[Monk2] p. 114Lemma 24nfa2 2170  nfra2 3349  nfra2w 3282
[Moore] p. 53Part Idf-mre 17466
[Munkres] p. 77Example 2distop 22345  indistop 22352  indistopon 22351
[Munkres] p. 77Example 3fctop 22354  fctop2 22355
[Munkres] p. 77Example 4cctop 22356
[Munkres] p. 78Definition of basisdf-bases 22296  isbasis3g 22299
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17325  tgval2 22306
[Munkres] p. 79Remarktgcl 22319
[Munkres] p. 80Lemma 2.1tgval3 22313
[Munkres] p. 80Lemma 2.2tgss2 22337  tgss3 22336
[Munkres] p. 81Lemma 2.3basgen 22338  basgen2 22339
[Munkres] p. 83Exercise 3topdifinf 35820  topdifinfeq 35821  topdifinffin 35819  topdifinfindis 35817
[Munkres] p. 89Definition of subspace topologyresttop 22511
[Munkres] p. 93Theorem 6.1(1)0cld 22389  topcld 22386
[Munkres] p. 93Theorem 6.1(2)iincld 22390
[Munkres] p. 93Theorem 6.1(3)uncld 22392
[Munkres] p. 94Definition of closureclsval 22388
[Munkres] p. 94Definition of interiorntrval 22387
[Munkres] p. 95Theorem 6.5(a)clsndisj 22426  elcls 22424
[Munkres] p. 95Theorem 6.5(b)elcls3 22434
[Munkres] p. 97Theorem 6.6clslp 22499  neindisj 22468
[Munkres] p. 97Corollary 6.7cldlp 22501
[Munkres] p. 97Definition of limit pointislp2 22496  lpval 22490
[Munkres] p. 98Definition of Hausdorff spacedf-haus 22666
[Munkres] p. 102Definition of continuous functiondf-cn 22578  iscn 22586  iscn2 22589
[Munkres] p. 107Theorem 7.2(g)cncnp 22631  cncnp2 22632  cncnpi 22629  df-cnp 22579  iscnp 22588  iscnp2 22590
[Munkres] p. 127Theorem 10.1metcn 23899
[Munkres] p. 128Theorem 10.3metcn4 24675
[Nathanson] p. 123Remarkreprgt 33234  reprinfz1 33235  reprlt 33232
[Nathanson] p. 123Definitiondf-repr 33222
[Nathanson] p. 123Chapter 5.1circlemethnat 33254
[Nathanson] p. 123Propositionbreprexp 33246  breprexpnat 33247  itgexpif 33219
[NielsenChuang] p. 195Equation 4.73unierri 31046
[OeSilva] p. 2042Section 2ax-bgbltosilva 45992
[Pfenning] p. 17Definition XMnatded 29347
[Pfenning] p. 17Definition NNCnatded 29347  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 29347
[Pfenning] p. 18Rule"natded 29347
[Pfenning] p. 18Definition /\Inatded 29347
[Pfenning] p. 18Definition ` `Enatded 29347  natded 29347  natded 29347  natded 29347  natded 29347
[Pfenning] p. 18Definition ` `Inatded 29347  natded 29347  natded 29347  natded 29347  natded 29347
[Pfenning] p. 18Definition ` `ELnatded 29347
[Pfenning] p. 18Definition ` `ERnatded 29347
[Pfenning] p. 18Definition ` `Ea,unatded 29347
[Pfenning] p. 18Definition ` `IRnatded 29347
[Pfenning] p. 18Definition ` `Ianatded 29347
[Pfenning] p. 127Definition =Enatded 29347
[Pfenning] p. 127Definition =Inatded 29347
[Ponnusamy] p. 361Theorem 6.44cphip0l 24566  df-dip 29643  dip0l 29660  ip0l 21040
[Ponnusamy] p. 361Equation 6.45cphipval 24607  ipval 29645
[Ponnusamy] p. 362Equation I1dipcj 29656  ipcj 21038
[Ponnusamy] p. 362Equation I3cphdir 24569  dipdir 29784  ipdir 21043  ipdiri 29772
[Ponnusamy] p. 362Equation I4ipidsq 29652  nmsq 24558
[Ponnusamy] p. 362Equation 6.46ip0i 29767
[Ponnusamy] p. 362Equation 6.47ip1i 29769
[Ponnusamy] p. 362Equation 6.48ip2i 29770
[Ponnusamy] p. 363Equation I2cphass 24575  dipass 29787  ipass 21049  ipassi 29783
[Prugovecki] p. 186Definition of brabraval 30886  df-bra 30792
[Prugovecki] p. 376Equation 8.1df-kb 30793  kbval 30896
[PtakPulmannova] p. 66Proposition 3.2.17atomli 31324
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 38351
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 31338  atcvat4i 31339  cvrat3 37905  cvrat4 37906  lsatcvat3 37514
[PtakPulmannova] p. 68Definition 3.2.18cvbr 31224  cvrval 37731  df-cv 31221  df-lcv 37481  lspsncv0 20607
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 38363
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 38364
[Quine] p. 16Definition 2.1df-clab 2714  rabid 3427  rabidd 43360
[Quine] p. 17Definition 2.1''dfsb7 2275
[Quine] p. 18Definition 2.7df-cleq 2728
[Quine] p. 19Definition 2.9conventions 29344  df-v 3447
[Quine] p. 34Theorem 5.1eqab 2877
[Quine] p. 35Theorem 5.2abid1 2874  abid2f 2939
[Quine] p. 40Theorem 6.1sb5 2267
[Quine] p. 40Theorem 6.2sb6 2088  sbalex 2235
[Quine] p. 41Theorem 6.3df-clel 2814
[Quine] p. 41Theorem 6.4eqid 2736  eqid1 29411
[Quine] p. 41Theorem 6.5eqcom 2743
[Quine] p. 42Theorem 6.6df-sbc 3740
[Quine] p. 42Theorem 6.7dfsbcq 3741  dfsbcq2 3742
[Quine] p. 43Theorem 6.8vex 3449
[Quine] p. 43Theorem 6.9isset 3458
[Quine] p. 44Theorem 7.3spcgf 3550  spcgv 3555  spcimgf 3548
[Quine] p. 44Theorem 6.11spsbc 3752  spsbcd 3753
[Quine] p. 44Theorem 6.12elex 3463
[Quine] p. 44Theorem 6.13elab 3630  elabg 3628  elabgf 3626
[Quine] p. 44Theorem 6.14noel 4290
[Quine] p. 48Theorem 7.2snprc 4678
[Quine] p. 48Definition 7.1df-pr 4589  df-sn 4587
[Quine] p. 49Theorem 7.4snss 4746  snssg 4744
[Quine] p. 49Theorem 7.5prss 4780  prssg 4779
[Quine] p. 49Theorem 7.6prid1 4723  prid1g 4721  prid2 4724  prid2g 4722  snid 4622  snidg 4620
[Quine] p. 51Theorem 7.12snex 5388
[Quine] p. 51Theorem 7.13prex 5389
[Quine] p. 53Theorem 8.2unisn 4887  unisnALT 43198  unisng 4886
[Quine] p. 53Theorem 8.3uniun 4891
[Quine] p. 54Theorem 8.6elssuni 4898
[Quine] p. 54Theorem 8.7uni0 4896
[Quine] p. 56Theorem 8.17uniabio 6463
[Quine] p. 56Definition 8.18dfaiota2 45308  dfiota2 6449
[Quine] p. 57Theorem 8.19aiotaval 45317  iotaval 6467
[Quine] p. 57Theorem 8.22iotanul 6474
[Quine] p. 58Theorem 8.23iotaex 6469
[Quine] p. 58Definition 9.1df-op 4593
[Quine] p. 61Theorem 9.5opabid 5482  opabidw 5481  opelopab 5499  opelopaba 5493  opelopabaf 5501  opelopabf 5502  opelopabg 5495  opelopabga 5490  opelopabgf 5497  oprabid 7389  oprabidw 7388
[Quine] p. 64Definition 9.11df-xp 5639
[Quine] p. 64Definition 9.12df-cnv 5641
[Quine] p. 64Definition 9.15df-id 5531
[Quine] p. 65Theorem 10.3fun0 6566
[Quine] p. 65Theorem 10.4funi 6533
[Quine] p. 65Theorem 10.5funsn 6554  funsng 6552
[Quine] p. 65Definition 10.1df-fun 6498
[Quine] p. 65Definition 10.2args 6044  dffv4 6839
[Quine] p. 68Definition 10.11conventions 29344  df-fv 6504  fv2 6837
[Quine] p. 124Theorem 17.3nn0opth2 14172  nn0opth2i 14171  nn0opthi 14170  omopthi 8607
[Quine] p. 177Definition 25.2df-rdg 8356
[Quine] p. 232Equation icarddom 10490
[Quine] p. 284Axiom 39(vi)funimaex 6589  funimaexg 6587
[Quine] p. 331Axiom system NFru 3738
[ReedSimon] p. 36Definition (iii)ax-his3 30026
[ReedSimon] p. 63Exercise 4(a)df-dip 29643  polid 30101  polid2i 30099  polidi 30100
[ReedSimon] p. 63Exercise 4(b)df-ph 29755
[ReedSimon] p. 195Remarklnophm 30961  lnophmi 30960
[Retherford] p. 49Exercise 1(i)leopadd 31074
[Retherford] p. 49Exercise 1(ii)leopmul 31076  leopmuli 31075
[Retherford] p. 49Exercise 1(iv)leoptr 31079
[Retherford] p. 49Definition VI.1df-leop 30794  leoppos 31068
[Retherford] p. 49Exercise 1(iii)leoptri 31078
[Retherford] p. 49Definition of operator orderingleop3 31067
[Roman] p. 4Definitiondf-dmat 21839  df-dmatalt 46469
[Roman] p. 18Part Preliminariesdf-rng 46163
[Roman] p. 19Part Preliminariesdf-ring 19966
[Roman] p. 46Theorem 1.6isldepslvec2 46556
[Roman] p. 112Noteisldepslvec2 46556  ldepsnlinc 46579  zlmodzxznm 46568
[Roman] p. 112Examplezlmodzxzequa 46567  zlmodzxzequap 46570  zlmodzxzldep 46575
[Roman] p. 170Theorem 7.8cayleyhamilton 22239
[Rosenlicht] p. 80Theoremheicant 36113
[Rosser] p. 281Definitiondf-op 4593
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 33258
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 33259
[Rotman] p. 28Remarkpgrpgt2nabl 46432  pmtr3ncom 19257
[Rotman] p. 31Theorem 3.4symggen2 19253
[Rotman] p. 42Theorem 3.15cayley 19196  cayleyth 19197
[Rudin] p. 164Equation 27efcan 15978
[Rudin] p. 164Equation 30efzval 15984
[Rudin] p. 167Equation 48absefi 16078
[Sanford] p. 39Remarkax-mp 5  mto 196
[Sanford] p. 39Rule 3mtpxor 1773
[Sanford] p. 39Rule 4mptxor 1771
[Sanford] p. 40Rule 1mptnan 1770
[Schechter] p. 51Definition of antisymmetryintasym 6069
[Schechter] p. 51Definition of irreflexivityintirr 6072
[Schechter] p. 51Definition of symmetrycnvsym 6066
[Schechter] p. 51Definition of transitivitycotr 6064
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17466
[Schechter] p. 79Definition of Moore closuredf-mrc 17467
[Schechter] p. 82Section 4.5df-mrc 17467
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17469
[Schechter] p. 139Definition AC3dfac9 10072
[Schechter] p. 141Definition (MC)dfac11 41375
[Schechter] p. 149Axiom DC1ax-dc 10382  axdc3 10390
[Schechter] p. 187Definition of "ring with unit"isring 19968  isrngo 36356
[Schechter] p. 276Remark 11.6.espan0 30484
[Schechter] p. 276Definition of spandf-span 30251  spanval 30275
[Schechter] p. 428Definition 15.35bastop1 22343
[Schloeder] p. 1Lemma 1.3onelon 6342  onelord 41571  ordelon 6341  ordelord 6339
[Schloeder] p. 1Lemma 1.7onepsuc 41572  sucidg 6398
[Schloeder] p. 1Remark 1.50elon 6371  onsuc 7746  ord0 6370  ordsuci 7743
[Schloeder] p. 1Theorem 1.9epsoon 41573
[Schloeder] p. 1Definition 1.1dftr5 5226
[Schloeder] p. 1Definition 1.2dford3 41338  elon2 6328
[Schloeder] p. 1Definition 1.4df-suc 6323
[Schloeder] p. 1Definition 1.6epel 5540  epelg 5538
[Schloeder] p. 1Theorem 1.9(i)elirr 9533  epirron 41574  ordirr 6335
[Schloeder] p. 1Theorem 1.9(ii)oneltr 41576  oneptr 41575  ontr1 6363
[Schloeder] p. 1Theorem 1.9(iii)oneltri 41578  oneptri 41577  ordtri3or 6349
[Schloeder] p. 2Lemma 1.10ondif1 8447  ord0eln0 6372
[Schloeder] p. 2Lemma 1.13elsuci 6384  onsucss 41587  trsucss 6405
[Schloeder] p. 2Lemma 1.14ordsucss 7753
[Schloeder] p. 2Lemma 1.15onnbtwn 6411  ordnbtwn 6410
[Schloeder] p. 2Lemma 1.16orddif0suc 41589  ordnexbtwnsuc 41588
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10337  onsucf1lem 41590  onsucf1o 41593  onsucf1olem 41591  onsucrn 41592
[Schloeder] p. 2Lemma 1.18dflim7 41594
[Schloeder] p. 2Remark 1.12ordzsl 7781
[Schloeder] p. 2Theorem 1.10ondif1i 41583  ordne0gt0 41582
[Schloeder] p. 2Definition 1.11dflim6 41585  limnsuc 41586  onsucelab 41584
[Schloeder] p. 3Remark 1.21omex 9579
[Schloeder] p. 3Theorem 1.19tfinds 7796
[Schloeder] p. 3Theorem 1.22omelon 9582  ordom 7812
[Schloeder] p. 3Definition 1.20dfom3 9583
[Schloeder] p. 4Lemma 2.21onn 8586
[Schloeder] p. 4Lemma 2.7ssonuni 7714  ssorduni 7713
[Schloeder] p. 4Remark 2.4oa1suc 8477
[Schloeder] p. 4Theorem 1.23dfom5 9586  limom 7818
[Schloeder] p. 4Definition 2.1df-1o 8412  df1o2 8419
[Schloeder] p. 4Definition 2.3oa0 8462  oa0suclim 41596  oalim 8478  oasuc 8470
[Schloeder] p. 4Definition 2.5om0 8463  om0suclim 41597  omlim 8479  omsuc 8472
[Schloeder] p. 4Definition 2.6oe0 8468  oe0m1 8467  oe0suclim 41598  oelim 8480  oesuc 8473
[Schloeder] p. 5Lemma 2.10onsupuni 41549
[Schloeder] p. 5Lemma 2.11onsupsucismax 41600
[Schloeder] p. 5Lemma 2.12onsssupeqcond 41601
[Schloeder] p. 5Lemma 2.13limexissup 41602  limexissupab 41604  limiun 41603  limuni 6378
[Schloeder] p. 5Lemma 2.14oa0r 8484
[Schloeder] p. 5Lemma 2.15om1 8489  om1om1r 41605  om1r 8490
[Schloeder] p. 5Remark 2.8oacl 8481  oaomoecl 41599  oecl 8483  omcl 8482
[Schloeder] p. 5Definition 2.9onsupintrab 41551
[Schloeder] p. 6Lemma 2.16oe1 8491
[Schloeder] p. 6Lemma 2.17oe1m 8492
[Schloeder] p. 6Lemma 2.18oe0rif 41606
[Schloeder] p. 6Theorem 2.19oasubex 41607
[Schloeder] p. 6Theorem 2.20nnacl 8558  nnamecl 41608  nnecl 8560  nnmcl 8559
[Schloeder] p. 7Lemma 3.1onsucwordi 41609
[Schloeder] p. 7Lemma 3.2oaword1 8499
[Schloeder] p. 7Lemma 3.3oaword2 8500
[Schloeder] p. 7Lemma 3.4oalimcl 8507
[Schloeder] p. 7Lemma 3.5oaltublim 41611
[Schloeder] p. 8Lemma 3.6oaordi3 41612
[Schloeder] p. 8Lemma 3.81oaomeqom 41614
[Schloeder] p. 8Lemma 3.10oa00 8506
[Schloeder] p. 8Lemma 3.11omge1 41617  omword1 8520
[Schloeder] p. 8Remark 3.9oaordnr 41616  oaordnrex 41615
[Schloeder] p. 8Theorem 3.7oaord3 41613
[Schloeder] p. 9Lemma 3.12omge2 41618  omword2 8521
[Schloeder] p. 9Lemma 3.13omlim2 41619
[Schloeder] p. 9Lemma 3.14omord2lim 41620
[Schloeder] p. 9Lemma 3.15omord2i 41621  omordi 8513
[Schloeder] p. 9Theorem 3.16omord 8515  omord2com 41622
[Schloeder] p. 10Lemma 3.172omomeqom 41623  df-2o 8413
[Schloeder] p. 10Lemma 3.19oege1 41626  oewordi 8538
[Schloeder] p. 10Lemma 3.20oege2 41627  oeworde 8540
[Schloeder] p. 10Lemma 3.21rp-oelim2 41628
[Schloeder] p. 10Lemma 3.22oeord2lim 41629
[Schloeder] p. 10Remark 3.18omnord1 41625  omnord1ex 41624
[Schloeder] p. 11Lemma 3.23oeord2i 41630
[Schloeder] p. 11Lemma 3.25nnoeomeqom 41632
[Schloeder] p. 11Remark 3.26oenord1 41636  oenord1ex 41635
[Schloeder] p. 11Theorem 4.1oaomoencom 41637
[Schloeder] p. 11Theorem 4.2oaass 8508
[Schloeder] p. 11Theorem 3.24oeord2com 41631
[Schloeder] p. 12Theorem 4.3odi 8526
[Schloeder] p. 13Theorem 4.4omass 8527
[Schloeder] p. 14Remark 4.6oenass 41639
[Schloeder] p. 14Theorem 4.7oeoa 8544
[Schloeder] p. 15Lemma 5.1cantnftermord 41640
[Schloeder] p. 15Lemma 5.2cantnfub 41641  cantnfub2 41642
[Schloeder] p. 16Theorem 5.3cantnf2 41645
[Schwabhauser] p. 10Axiom A1axcgrrflx 27863  axtgcgrrflx 27404
[Schwabhauser] p. 10Axiom A2axcgrtr 27864
[Schwabhauser] p. 10Axiom A3axcgrid 27865  axtgcgrid 27405
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 27390
[Schwabhauser] p. 11Axiom A4axsegcon 27876  axtgsegcon 27406  df-trkgcb 27392
[Schwabhauser] p. 11Axiom A5ax5seg 27887  axtg5seg 27407  df-trkgcb 27392
[Schwabhauser] p. 11Axiom A6axbtwnid 27888  axtgbtwnid 27408  df-trkgb 27391
[Schwabhauser] p. 12Axiom A7axpasch 27890  axtgpasch 27409  df-trkgb 27391
[Schwabhauser] p. 12Axiom A8axlowdim2 27909  df-trkg2d 33278
[Schwabhauser] p. 13Axiom A8axtglowdim2 27412
[Schwabhauser] p. 13Axiom A9axtgupdim2 27413  df-trkg2d 33278
[Schwabhauser] p. 13Axiom A10axeuclid 27912  axtgeucl 27414  df-trkge 27393
[Schwabhauser] p. 13Axiom A11axcont 27925  axtgcont 27411  axtgcont1 27410  df-trkgb 27391
[Schwabhauser] p. 27Theorem 2.1cgrrflx 34572
[Schwabhauser] p. 27Theorem 2.2cgrcomim 34574
[Schwabhauser] p. 27Theorem 2.3cgrtr 34577
[Schwabhauser] p. 27Theorem 2.4cgrcoml 34581
[Schwabhauser] p. 27Theorem 2.5cgrcomr 34582  tgcgrcomimp 27419  tgcgrcoml 27421  tgcgrcomr 27420
[Schwabhauser] p. 28Theorem 2.8cgrtriv 34587  tgcgrtriv 27426
[Schwabhauser] p. 28Theorem 2.105segofs 34591  tg5segofs 33286
[Schwabhauser] p. 28Definition 2.10df-afs 33283  df-ofs 34568
[Schwabhauser] p. 29Theorem 2.11cgrextend 34593  tgcgrextend 27427
[Schwabhauser] p. 29Theorem 2.12segconeq 34595  tgsegconeq 27428
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 34607  btwntriv2 34597  tgbtwntriv2 27429
[Schwabhauser] p. 30Theorem 3.2btwncomim 34598  tgbtwncom 27430
[Schwabhauser] p. 30Theorem 3.3btwntriv1 34601  tgbtwntriv1 27433
[Schwabhauser] p. 30Theorem 3.4btwnswapid 34602  tgbtwnswapid 27434
[Schwabhauser] p. 30Theorem 3.5btwnexch2 34608  btwnintr 34604  tgbtwnexch2 27438  tgbtwnintr 27435
[Schwabhauser] p. 30Theorem 3.6btwnexch 34610  btwnexch3 34605  tgbtwnexch 27440  tgbtwnexch3 27436
[Schwabhauser] p. 30Theorem 3.7btwnouttr 34609  tgbtwnouttr 27439  tgbtwnouttr2 27437
[Schwabhauser] p. 32Theorem 3.13axlowdim1 27908
[Schwabhauser] p. 32Theorem 3.14btwndiff 34612  tgbtwndiff 27448
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 27441  trisegint 34613
[Schwabhauser] p. 34Theorem 4.2ifscgr 34629  tgifscgr 27450
[Schwabhauser] p. 34Theorem 4.11colcom 27500  colrot1 27501  colrot2 27502  lncom 27564  lnrot1 27565  lnrot2 27566
[Schwabhauser] p. 34Definition 4.1df-ifs 34625
[Schwabhauser] p. 35Theorem 4.3cgrsub 34630  tgcgrsub 27451
[Schwabhauser] p. 35Theorem 4.5cgrxfr 34640  tgcgrxfr 27460
[Schwabhauser] p. 35Statement 4.4ercgrg 27459
[Schwabhauser] p. 35Definition 4.4df-cgr3 34626  df-cgrg 27453
[Schwabhauser] p. 35Definition instead (givendf-cgrg 27453
[Schwabhauser] p. 36Theorem 4.6btwnxfr 34641  tgbtwnxfr 27472
[Schwabhauser] p. 36Theorem 4.11colinearperm1 34647  colinearperm2 34649  colinearperm3 34648  colinearperm4 34650  colinearperm5 34651
[Schwabhauser] p. 36Definition 4.8df-ismt 27475
[Schwabhauser] p. 36Definition 4.10df-colinear 34624  tgellng 27495  tglng 27488
[Schwabhauser] p. 37Theorem 4.12colineartriv1 34652
[Schwabhauser] p. 37Theorem 4.13colinearxfr 34660  lnxfr 27508
[Schwabhauser] p. 37Theorem 4.14lineext 34661  lnext 27509
[Schwabhauser] p. 37Theorem 4.16fscgr 34665  tgfscgr 27510
[Schwabhauser] p. 37Theorem 4.17linecgr 34666  lncgr 27511
[Schwabhauser] p. 37Definition 4.15df-fs 34627
[Schwabhauser] p. 38Theorem 4.18lineid 34668  lnid 27512
[Schwabhauser] p. 38Theorem 4.19idinside 34669  tgidinside 27513
[Schwabhauser] p. 39Theorem 5.1btwnconn1 34686  tgbtwnconn1 27517
[Schwabhauser] p. 41Theorem 5.2btwnconn2 34687  tgbtwnconn2 27518
[Schwabhauser] p. 41Theorem 5.3btwnconn3 34688  tgbtwnconn3 27519
[Schwabhauser] p. 41Theorem 5.5brsegle2 34694
[Schwabhauser] p. 41Definition 5.4df-segle 34692  legov 27527
[Schwabhauser] p. 41Definition 5.5legov2 27528
[Schwabhauser] p. 42Remark 5.13legso 27541
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 34695
[Schwabhauser] p. 42Theorem 5.7seglerflx 34697
[Schwabhauser] p. 42Theorem 5.8segletr 34699
[Schwabhauser] p. 42Theorem 5.9segleantisym 34700
[Schwabhauser] p. 42Theorem 5.10seglelin 34701
[Schwabhauser] p. 42Theorem 5.11seglemin 34698
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 34703
[Schwabhauser] p. 42Proposition 5.7legid 27529
[Schwabhauser] p. 42Proposition 5.8legtrd 27531
[Schwabhauser] p. 42Proposition 5.9legtri3 27532
[Schwabhauser] p. 42Proposition 5.10legtrid 27533
[Schwabhauser] p. 42Proposition 5.11leg0 27534
[Schwabhauser] p. 43Theorem 6.2btwnoutside 34710
[Schwabhauser] p. 43Theorem 6.3broutsideof3 34711
[Schwabhauser] p. 43Theorem 6.4broutsideof 34706  df-outsideof 34705
[Schwabhauser] p. 43Definition 6.1broutsideof2 34707  ishlg 27544
[Schwabhauser] p. 44Theorem 6.4hlln 27549
[Schwabhauser] p. 44Theorem 6.5hlid 27551  outsideofrflx 34712
[Schwabhauser] p. 44Theorem 6.6hlcomb 27545  hlcomd 27546  outsideofcom 34713
[Schwabhauser] p. 44Theorem 6.7hltr 27552  outsideoftr 34714
[Schwabhauser] p. 44Theorem 6.11hlcgreu 27560  outsideofeu 34716
[Schwabhauser] p. 44Definition 6.8df-ray 34723
[Schwabhauser] p. 45Part 2df-lines2 34724
[Schwabhauser] p. 45Theorem 6.13outsidele 34717
[Schwabhauser] p. 45Theorem 6.15lineunray 34732
[Schwabhauser] p. 45Theorem 6.16lineelsb2 34733  tglineelsb2 27574
[Schwabhauser] p. 45Theorem 6.17linecom 34735  linerflx1 34734  linerflx2 34736  tglinecom 27577  tglinerflx1 27575  tglinerflx2 27576
[Schwabhauser] p. 45Theorem 6.18linethru 34738  tglinethru 27578
[Schwabhauser] p. 45Definition 6.14df-line2 34722  tglng 27488
[Schwabhauser] p. 45Proposition 6.13legbtwn 27536
[Schwabhauser] p. 46Theorem 6.19linethrueu 34741  tglinethrueu 27581
[Schwabhauser] p. 46Theorem 6.21lineintmo 34742  tglineineq 27585  tglineinteq 27587  tglineintmo 27584
[Schwabhauser] p. 46Theorem 6.23colline 27591
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 27592
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 27593
[Schwabhauser] p. 49Theorem 7.3mirinv 27608
[Schwabhauser] p. 49Theorem 7.7mirmir 27604
[Schwabhauser] p. 49Theorem 7.8mirreu3 27596
[Schwabhauser] p. 49Definition 7.5df-mir 27595  ismir 27601  mirbtwn 27600  mircgr 27599  mirfv 27598  mirval 27597
[Schwabhauser] p. 50Theorem 7.8mirreu 27606
[Schwabhauser] p. 50Theorem 7.9mireq 27607
[Schwabhauser] p. 50Theorem 7.10mirinv 27608
[Schwabhauser] p. 50Theorem 7.11mirf1o 27611
[Schwabhauser] p. 50Theorem 7.13miriso 27612
[Schwabhauser] p. 51Theorem 7.14mirmot 27617
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 27614  mirbtwni 27613
[Schwabhauser] p. 51Theorem 7.16mircgrs 27615
[Schwabhauser] p. 51Theorem 7.17miduniq 27627
[Schwabhauser] p. 52Lemma 7.21symquadlem 27631
[Schwabhauser] p. 52Theorem 7.18miduniq1 27628
[Schwabhauser] p. 52Theorem 7.19miduniq2 27629
[Schwabhauser] p. 52Theorem 7.20colmid 27630
[Schwabhauser] p. 53Lemma 7.22krippen 27633
[Schwabhauser] p. 55Lemma 7.25midexlem 27634
[Schwabhauser] p. 57Theorem 8.2ragcom 27640
[Schwabhauser] p. 57Definition 8.1df-rag 27636  israg 27639
[Schwabhauser] p. 58Theorem 8.3ragcol 27641
[Schwabhauser] p. 58Theorem 8.4ragmir 27642
[Schwabhauser] p. 58Theorem 8.5ragtrivb 27644
[Schwabhauser] p. 58Theorem 8.6ragflat2 27645
[Schwabhauser] p. 58Theorem 8.7ragflat 27646
[Schwabhauser] p. 58Theorem 8.8ragtriva 27647
[Schwabhauser] p. 58Theorem 8.9ragflat3 27648  ragncol 27651
[Schwabhauser] p. 58Theorem 8.10ragcgr 27649
[Schwabhauser] p. 59Theorem 8.12perpcom 27655
[Schwabhauser] p. 59Theorem 8.13ragperp 27659
[Schwabhauser] p. 59Theorem 8.14perpneq 27656
[Schwabhauser] p. 59Definition 8.11df-perpg 27638  isperp 27654
[Schwabhauser] p. 59Definition 8.13isperp2 27657
[Schwabhauser] p. 60Theorem 8.18foot 27664
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 27672  colperpexlem2 27673
[Schwabhauser] p. 63Theorem 8.21colperpex 27675  colperpexlem3 27674
[Schwabhauser] p. 64Theorem 8.22mideu 27680  midex 27679
[Schwabhauser] p. 66Lemma 8.24opphllem 27677
[Schwabhauser] p. 67Theorem 9.2oppcom 27686
[Schwabhauser] p. 67Definition 9.1islnopp 27681
[Schwabhauser] p. 68Lemma 9.3opphllem2 27690
[Schwabhauser] p. 68Lemma 9.4opphllem5 27693  opphllem6 27694
[Schwabhauser] p. 69Theorem 9.5opphl 27696
[Schwabhauser] p. 69Theorem 9.6axtgpasch 27409
[Schwabhauser] p. 70Theorem 9.6outpasch 27697
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 27705
[Schwabhauser] p. 71Definition 9.7df-hpg 27700  hpgbr 27702
[Schwabhauser] p. 72Lemma 9.10hpgerlem 27707
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 27706
[Schwabhauser] p. 72Theorem 9.11hpgid 27708
[Schwabhauser] p. 72Theorem 9.12hpgcom 27709
[Schwabhauser] p. 72Theorem 9.13hpgtr 27710
[Schwabhauser] p. 73Theorem 9.18colopp 27711
[Schwabhauser] p. 73Theorem 9.19colhp 27712
[Schwabhauser] p. 88Theorem 10.2lmieu 27726
[Schwabhauser] p. 88Definition 10.1df-mid 27716
[Schwabhauser] p. 89Theorem 10.4lmicom 27730
[Schwabhauser] p. 89Theorem 10.5lmilmi 27731
[Schwabhauser] p. 89Theorem 10.6lmireu 27732
[Schwabhauser] p. 89Theorem 10.7lmieq 27733
[Schwabhauser] p. 89Theorem 10.8lmiinv 27734
[Schwabhauser] p. 89Theorem 10.9lmif1o 27737
[Schwabhauser] p. 89Theorem 10.10lmiiso 27739
[Schwabhauser] p. 89Definition 10.3df-lmi 27717
[Schwabhauser] p. 90Theorem 10.11lmimot 27740
[Schwabhauser] p. 91Theorem 10.12hypcgr 27743
[Schwabhauser] p. 92Theorem 10.14lmiopp 27744
[Schwabhauser] p. 92Theorem 10.15lnperpex 27745
[Schwabhauser] p. 92Theorem 10.16trgcopy 27746  trgcopyeu 27748
[Schwabhauser] p. 95Definition 11.2dfcgra2 27772
[Schwabhauser] p. 95Definition 11.3iscgra 27751
[Schwabhauser] p. 95Proposition 11.4cgracgr 27760
[Schwabhauser] p. 95Proposition 11.10cgrahl1 27758  cgrahl2 27759
[Schwabhauser] p. 96Theorem 11.6cgraid 27761
[Schwabhauser] p. 96Theorem 11.9cgraswap 27762
[Schwabhauser] p. 97Theorem 11.7cgracom 27764
[Schwabhauser] p. 97Theorem 11.8cgratr 27765
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 27768  cgrahl 27769
[Schwabhauser] p. 98Theorem 11.13sacgr 27773
[Schwabhauser] p. 98Theorem 11.14oacgr 27774
[Schwabhauser] p. 98Theorem 11.15acopy 27775  acopyeu 27776
[Schwabhauser] p. 101Theorem 11.24inagswap 27783
[Schwabhauser] p. 101Theorem 11.25inaghl 27787
[Schwabhauser] p. 101Definition 11.23isinag 27780
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 27795
[Schwabhauser] p. 102Definition 11.27df-leag 27788  isleag 27789
[Schwabhauser] p. 107Theorem 11.49tgsas 27797  tgsas1 27796  tgsas2 27798  tgsas3 27799
[Schwabhauser] p. 108Theorem 11.50tgasa 27801  tgasa1 27800
[Schwabhauser] p. 109Theorem 11.51tgsss1 27802  tgsss2 27803  tgsss3 27804
[Shapiro] p. 230Theorem 6.5.1dchrhash 26619  dchrsum 26617  dchrsum2 26616  sumdchr 26620
[Shapiro] p. 232Theorem 6.5.2dchr2sum 26621  sum2dchr 26622
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19845  ablfacrp2 19846
[Shapiro], p. 328Equation 9.2.4vmasum 26564
[Shapiro], p. 329Equation 9.2.7logfac2 26565
[Shapiro], p. 329Equation 9.2.9logfacrlim 26572
[Shapiro], p. 331Equation 9.2.13vmadivsum 26830
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 26833
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 26887  vmalogdivsum2 26886
[Shapiro], p. 375Theorem 9.4.1dirith 26877  dirith2 26876
[Shapiro], p. 375Equation 9.4.3rplogsum 26875  rpvmasum 26874  rpvmasum2 26860
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 26835
[Shapiro], p. 376Equation 9.4.8dchrvmasum 26873
[Shapiro], p. 377Lemma 9.4.1dchrisum 26840  dchrisumlem1 26837  dchrisumlem2 26838  dchrisumlem3 26839  dchrisumlema 26836
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 26843
[Shapiro], p. 379Equation 9.4.16dchrmusum 26872  dchrmusumlem 26870  dchrvmasumlem 26871
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 26842
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 26844
[Shapiro], p. 382Lemma 9.4.4dchrisum0 26868  dchrisum0re 26861  dchrisumn0 26869
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 26854
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 26858
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 26859
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 26914  pntrsumbnd2 26915  pntrsumo1 26913
[Shapiro], p. 405Equation 10.2.1mudivsum 26878
[Shapiro], p. 406Equation 10.2.6mulogsum 26880
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 26882
[Shapiro], p. 407Equation 10.2.8mulog2sum 26885
[Shapiro], p. 418Equation 10.4.6logsqvma 26890
[Shapiro], p. 418Equation 10.4.8logsqvma2 26891
[Shapiro], p. 419Equation 10.4.10selberg 26896
[Shapiro], p. 420Equation 10.4.12selberg2lem 26898
[Shapiro], p. 420Equation 10.4.14selberg2 26899
[Shapiro], p. 422Equation 10.6.7selberg3 26907
[Shapiro], p. 422Equation 10.4.20selberg4lem1 26908
[Shapiro], p. 422Equation 10.4.21selberg3lem1 26905  selberg3lem2 26906
[Shapiro], p. 422Equation 10.4.23selberg4 26909
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 26903
[Shapiro], p. 428Equation 10.6.2selbergr 26916
[Shapiro], p. 429Equation 10.6.8selberg3r 26917
[Shapiro], p. 430Equation 10.6.11selberg4r 26918
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 26932
[Shapiro], p. 434Equation 10.6.27pntlema 26944  pntlemb 26945  pntlemc 26943  pntlemd 26942  pntlemg 26946
[Shapiro], p. 435Equation 10.6.29pntlema 26944
[Shapiro], p. 436Lemma 10.6.1pntpbnd 26936
[Shapiro], p. 436Lemma 10.6.2pntibnd 26941
[Shapiro], p. 436Equation 10.6.34pntlema 26944
[Shapiro], p. 436Equation 10.6.35pntlem3 26957  pntleml 26959
[Stoll] p. 13Definition corresponds to dfsymdif3 4256
[Stoll] p. 16Exercise 4.40dif 4361  dif0 4332
[Stoll] p. 16Exercise 4.8difdifdir 4449
[Stoll] p. 17Theorem 5.1(5)unvdif 4434
[Stoll] p. 19Theorem 5.2(13)undm 4247
[Stoll] p. 19Theorem 5.2(13')indm 4248
[Stoll] p. 20Remarkinvdif 4228
[Stoll] p. 25Definition of ordered tripledf-ot 4595
[Stoll] p. 43Definitionuniiun 5018
[Stoll] p. 44Definitionintiin 5019
[Stoll] p. 45Definitiondf-iin 4957
[Stoll] p. 45Definition indexed uniondf-iun 4956
[Stoll] p. 176Theorem 3.4(27)iman 402
[Stoll] p. 262Example 4.1dfsymdif3 4256
[Strang] p. 242Section 6.3expgrowth 42605
[Suppes] p. 22Theorem 2eq0 4303  eq0f 4300
[Suppes] p. 22Theorem 4eqss 3959  eqssd 3961  eqssi 3960
[Suppes] p. 23Theorem 5ss0 4358  ss0b 4357
[Suppes] p. 23Theorem 6sstr 3952  sstrALT2 43107
[Suppes] p. 23Theorem 7pssirr 4060
[Suppes] p. 23Theorem 8pssn2lp 4061
[Suppes] p. 23Theorem 9psstr 4064
[Suppes] p. 23Theorem 10pssss 4055
[Suppes] p. 25Theorem 12elin 3926  elun 4108
[Suppes] p. 26Theorem 15inidm 4178
[Suppes] p. 26Theorem 16in0 4351
[Suppes] p. 27Theorem 23unidm 4112
[Suppes] p. 27Theorem 24un0 4350
[Suppes] p. 27Theorem 25ssun1 4132
[Suppes] p. 27Theorem 26ssequn1 4140
[Suppes] p. 27Theorem 27unss 4144
[Suppes] p. 27Theorem 28indir 4235
[Suppes] p. 27Theorem 29undir 4236
[Suppes] p. 28Theorem 32difid 4330
[Suppes] p. 29Theorem 33difin 4221
[Suppes] p. 29Theorem 34indif 4229
[Suppes] p. 29Theorem 35undif1 4435
[Suppes] p. 29Theorem 36difun2 4440
[Suppes] p. 29Theorem 37difin0 4433
[Suppes] p. 29Theorem 38disjdif 4431
[Suppes] p. 29Theorem 39difundi 4239
[Suppes] p. 29Theorem 40difindi 4241
[Suppes] p. 30Theorem 41nalset 5270
[Suppes] p. 39Theorem 61uniss 4873
[Suppes] p. 39Theorem 65uniop 5472
[Suppes] p. 41Theorem 70intsn 4947
[Suppes] p. 42Theorem 71intpr 4943  intprg 4942
[Suppes] p. 42Theorem 73op1stb 5428
[Suppes] p. 42Theorem 78intun 4941
[Suppes] p. 44Definition 15(a)dfiun2 4993  dfiun2g 4990
[Suppes] p. 44Definition 15(b)dfiin2 4994
[Suppes] p. 47Theorem 86elpw 4564  elpw2 5302  elpw2g 5301  elpwg 4563  elpwgdedVD 43189
[Suppes] p. 47Theorem 87pwid 4582
[Suppes] p. 47Theorem 89pw0 4772
[Suppes] p. 48Theorem 90pwpw0 4773
[Suppes] p. 52Theorem 101xpss12 5648
[Suppes] p. 52Theorem 102xpindi 5789  xpindir 5790
[Suppes] p. 52Theorem 103xpundi 5700  xpundir 5701
[Suppes] p. 54Theorem 105elirrv 9532
[Suppes] p. 58Theorem 2relss 5737
[Suppes] p. 59Theorem 4eldm 5856  eldm2 5857  eldm2g 5855  eldmg 5854
[Suppes] p. 59Definition 3df-dm 5643
[Suppes] p. 60Theorem 6dmin 5867
[Suppes] p. 60Theorem 8rnun 6098
[Suppes] p. 60Theorem 9rnin 6099
[Suppes] p. 60Definition 4dfrn2 5844
[Suppes] p. 61Theorem 11brcnv 5838  brcnvg 5835
[Suppes] p. 62Equation 5elcnv 5832  elcnv2 5833
[Suppes] p. 62Theorem 12relcnv 6056
[Suppes] p. 62Theorem 15cnvin 6097
[Suppes] p. 62Theorem 16cnvun 6095
[Suppes] p. 63Definitiondftrrels2 37037
[Suppes] p. 63Theorem 20co02 6212
[Suppes] p. 63Theorem 21dmcoss 5926
[Suppes] p. 63Definition 7df-co 5642
[Suppes] p. 64Theorem 26cnvco 5841
[Suppes] p. 64Theorem 27coass 6217
[Suppes] p. 65Theorem 31resundi 5951
[Suppes] p. 65Theorem 34elima 6018  elima2 6019  elima3 6020  elimag 6017
[Suppes] p. 65Theorem 35imaundi 6102
[Suppes] p. 66Theorem 40dminss 6105
[Suppes] p. 66Theorem 41imainss 6106
[Suppes] p. 67Exercise 11cnvxp 6109
[Suppes] p. 81Definition 34dfec2 8651
[Suppes] p. 82Theorem 72elec 8692  elecALTV 36726  elecg 8691
[Suppes] p. 82Theorem 73eqvrelth 37073  erth 8697  erth2 8698
[Suppes] p. 83Theorem 74eqvreldisj 37076  erdisj 8700
[Suppes] p. 83Definition 35, df-parts 37227  dfmembpart2 37232
[Suppes] p. 89Theorem 96map0b 8821
[Suppes] p. 89Theorem 97map0 8825  map0g 8822
[Suppes] p. 89Theorem 98mapsn 8826  mapsnd 8824
[Suppes] p. 89Theorem 99mapss 8827
[Suppes] p. 91Definition 12(ii)alephsuc 10004
[Suppes] p. 91Definition 12(iii)alephlim 10003
[Suppes] p. 92Theorem 1enref 8925  enrefg 8924
[Suppes] p. 92Theorem 2ensym 8943  ensymb 8942  ensymi 8944
[Suppes] p. 92Theorem 3entr 8946
[Suppes] p. 92Theorem 4unen 8990
[Suppes] p. 94Theorem 15endom 8919
[Suppes] p. 94Theorem 16ssdomg 8940
[Suppes] p. 94Theorem 17domtr 8947
[Suppes] p. 95Theorem 18sbth 9037
[Suppes] p. 97Theorem 23canth2 9074  canth2g 9075
[Suppes] p. 97Definition 3brsdom2 9041  df-sdom 8886  dfsdom2 9040
[Suppes] p. 97Theorem 21(i)sdomirr 9058
[Suppes] p. 97Theorem 22(i)domnsym 9043
[Suppes] p. 97Theorem 21(ii)sdomnsym 9042
[Suppes] p. 97Theorem 22(ii)domsdomtr 9056
[Suppes] p. 97Theorem 22(iv)brdom2 8922
[Suppes] p. 97Theorem 21(iii)sdomtr 9059
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9054
[Suppes] p. 98Exercise 4fundmen 8975  fundmeng 8976
[Suppes] p. 98Exercise 6xpdom3 9014
[Suppes] p. 98Exercise 11sdomentr 9055
[Suppes] p. 104Theorem 37fofi 9282
[Suppes] p. 104Theorem 38pwfi 9122
[Suppes] p. 105Theorem 40pwfi 9122
[Suppes] p. 111Axiom for cardinal numberscarden 10487
[Suppes] p. 130Definition 3df-tr 5223
[Suppes] p. 132Theorem 9ssonuni 7714
[Suppes] p. 134Definition 6df-suc 6323
[Suppes] p. 136Theorem Schema 22findes 7839  finds 7835  finds1 7838  finds2 7837
[Suppes] p. 151Theorem 42isfinite 9588  isfinite2 9245  isfiniteg 9248  unbnn 9243
[Suppes] p. 162Definition 5df-ltnq 10854  df-ltpq 10846
[Suppes] p. 197Theorem Schema 4tfindes 7799  tfinds 7796  tfinds2 7800
[Suppes] p. 209Theorem 18oaord1 8498
[Suppes] p. 209Theorem 21oaword2 8500
[Suppes] p. 211Theorem 25oaass 8508
[Suppes] p. 225Definition 8iscard2 9912
[Suppes] p. 227Theorem 56ondomon 10499
[Suppes] p. 228Theorem 59harcard 9914
[Suppes] p. 228Definition 12(i)aleph0 10002
[Suppes] p. 228Theorem Schema 61onintss 6368
[Suppes] p. 228Theorem Schema 62onminesb 7728  onminsb 7729
[Suppes] p. 229Theorem 64alephval2 10508
[Suppes] p. 229Theorem 65alephcard 10006
[Suppes] p. 229Theorem 66alephord2i 10013
[Suppes] p. 229Theorem 67alephnbtwn 10007
[Suppes] p. 229Definition 12df-aleph 9876
[Suppes] p. 242Theorem 6weth 10431
[Suppes] p. 242Theorem 8entric 10493
[Suppes] p. 242Theorem 9carden 10487
[TakeutiZaring] p. 8Axiom 1ax-ext 2707
[TakeutiZaring] p. 13Definition 4.5df-cleq 2728
[TakeutiZaring] p. 13Proposition 4.6df-clel 2814
[TakeutiZaring] p. 13Proposition 4.9cvjust 2730
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2759
[TakeutiZaring] p. 14Definition 4.16df-oprab 7361
[TakeutiZaring] p. 14Proposition 4.14ru 3738
[TakeutiZaring] p. 15Axiom 2zfpair 5376
[TakeutiZaring] p. 15Exercise 1elpr 4609  elpr2 4611  elpr2g 4610  elprg 4607
[TakeutiZaring] p. 15Exercise 2elsn 4601  elsn2 4625  elsn2g 4624  elsng 4600  velsn 4602
[TakeutiZaring] p. 15Exercise 3elop 5424
[TakeutiZaring] p. 15Exercise 4sneq 4596  sneqr 4798
[TakeutiZaring] p. 15Definition 5.1dfpr2 4605  dfsn2 4599  dfsn2ALT 4606
[TakeutiZaring] p. 16Axiom 3uniex 7678
[TakeutiZaring] p. 16Exercise 6opth 5433
[TakeutiZaring] p. 16Exercise 7opex 5421
[TakeutiZaring] p. 16Exercise 8rext 5405
[TakeutiZaring] p. 16Corollary 5.8unex 7680  unexg 7683
[TakeutiZaring] p. 16Definition 5.3dftp2 4650
[TakeutiZaring] p. 16Definition 5.5df-uni 4866
[TakeutiZaring] p. 16Definition 5.6df-in 3917  df-un 3915
[TakeutiZaring] p. 16Proposition 5.7unipr 4883  uniprg 4882
[TakeutiZaring] p. 17Axiom 4vpwex 5332
[TakeutiZaring] p. 17Exercise 1eltp 4649
[TakeutiZaring] p. 17Exercise 5elsuc 6387  elsucg 6385  sstr2 3951
[TakeutiZaring] p. 17Exercise 6uncom 4113
[TakeutiZaring] p. 17Exercise 7incom 4161
[TakeutiZaring] p. 17Exercise 8unass 4126
[TakeutiZaring] p. 17Exercise 9inass 4179
[TakeutiZaring] p. 17Exercise 10indi 4233
[TakeutiZaring] p. 17Exercise 11undi 4234
[TakeutiZaring] p. 17Definition 5.9df-pss 3929  dfss2 3930
[TakeutiZaring] p. 17Definition 5.10df-pw 4562
[TakeutiZaring] p. 18Exercise 7unss2 4141
[TakeutiZaring] p. 18Exercise 9df-ss 3927  sseqin2 4175
[TakeutiZaring] p. 18Exercise 10ssid 3966
[TakeutiZaring] p. 18Exercise 12inss1 4188  inss2 4189
[TakeutiZaring] p. 18Exercise 13nss 4006
[TakeutiZaring] p. 18Exercise 15unieq 4876
[TakeutiZaring] p. 18Exercise 18sspwb 5406  sspwimp 43190  sspwimpALT 43197  sspwimpALT2 43200  sspwimpcf 43192
[TakeutiZaring] p. 18Exercise 19pweqb 5413
[TakeutiZaring] p. 19Axiom 5ax-rep 5242
[TakeutiZaring] p. 20Definitiondf-rab 3408
[TakeutiZaring] p. 20Corollary 5.160ex 5264
[TakeutiZaring] p. 20Definition 5.12df-dif 3913
[TakeutiZaring] p. 20Definition 5.14dfnul2 4285
[TakeutiZaring] p. 20Proposition 5.15difid 4330
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4306  n0f 4302  neq0 4305  neq0f 4301
[TakeutiZaring] p. 21Axiom 6zfreg 9531
[TakeutiZaring] p. 21Axiom 6'zfregs 9668
[TakeutiZaring] p. 21Theorem 5.22setind 9670
[TakeutiZaring] p. 21Definition 5.20df-v 3447
[TakeutiZaring] p. 21Proposition 5.21vprc 5272
[TakeutiZaring] p. 22Exercise 10ss 4356
[TakeutiZaring] p. 22Exercise 3ssex 5278  ssexg 5280
[TakeutiZaring] p. 22Exercise 4inex1 5274
[TakeutiZaring] p. 22Exercise 5ruv 9538
[TakeutiZaring] p. 22Exercise 6elirr 9533
[TakeutiZaring] p. 22Exercise 7ssdif0 4323
[TakeutiZaring] p. 22Exercise 11difdif 4090
[TakeutiZaring] p. 22Exercise 13undif3 4250  undif3VD 43154
[TakeutiZaring] p. 22Exercise 14difss 4091
[TakeutiZaring] p. 22Exercise 15sscon 4098
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3065
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3074
[TakeutiZaring] p. 23Proposition 6.2xpex 7687  xpexg 7684
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5640
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6572
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6748  fun11 6575
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6512  svrelfun 6573
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5843
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5845
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5645
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5646
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5642
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6146  dfrel2 6141
[TakeutiZaring] p. 25Exercise 3xpss 5649
[TakeutiZaring] p. 25Exercise 5relun 5767
[TakeutiZaring] p. 25Exercise 6reluni 5774
[TakeutiZaring] p. 25Exercise 9inxp 5788
[TakeutiZaring] p. 25Exercise 12relres 5966
[TakeutiZaring] p. 25Exercise 13opelres 5943  opelresi 5945
[TakeutiZaring] p. 25Exercise 14dmres 5959
[TakeutiZaring] p. 25Exercise 15resss 5962
[TakeutiZaring] p. 25Exercise 17resabs1 5967
[TakeutiZaring] p. 25Exercise 18funres 6543
[TakeutiZaring] p. 25Exercise 24relco 6060
[TakeutiZaring] p. 25Exercise 29funco 6541
[TakeutiZaring] p. 25Exercise 30f1co 6750
[TakeutiZaring] p. 26Definition 6.10eu2 2609
[TakeutiZaring] p. 26Definition 6.11conventions 29344  df-fv 6504  fv3 6860
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7862  cnvexg 7861
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7848  dmexg 7840
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7849  rnexg 7841
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 42724
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7857
[TakeutiZaring] p. 27Corollary 6.13fvex 6855
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 45396  tz6.12-1-afv2 45463  tz6.12-1 6865  tz6.12-afv 45395  tz6.12-afv2 45462  tz6.12 6867  tz6.12c-afv2 45464  tz6.12c 6864
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 45459  tz6.12-2 6830  tz6.12i-afv2 45465  tz6.12i 6870
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6499
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6500
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6502  wfo 6494
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6501  wf1 6493
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6503  wf1o 6495
[TakeutiZaring] p. 28Exercise 4eqfnfv 6982  eqfnfv2 6983  eqfnfv2f 6986
[TakeutiZaring] p. 28Exercise 5fvco 6939
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7167
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7165
[TakeutiZaring] p. 29Exercise 9funimaex 6589  funimaexg 6587
[TakeutiZaring] p. 29Definition 6.18df-br 5106
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5546
[TakeutiZaring] p. 30Definition 6.21dffr2 5597  dffr3 6051  eliniseg 6046  iniseg 6049
[TakeutiZaring] p. 30Definition 6.22df-eprel 5537
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5611  fr3nr 7706  frirr 5610
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5588
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7708
[TakeutiZaring] p. 31Exercise 1frss 5600
[TakeutiZaring] p. 31Exercise 4wess 5620
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6301  tz6.26i 6303  wefrc 5627  wereu2 5630
[TakeutiZaring] p. 32Theorem 6.27wfi 6304  wfii 6306
[TakeutiZaring] p. 32Definition 6.28df-isom 6505
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7274
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7275
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7281
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7282
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7283
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7287
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7294
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7296
[TakeutiZaring] p. 35Notationwtr 5222
[TakeutiZaring] p. 35Theorem 7.2trelpss 42725  tz7.2 5617
[TakeutiZaring] p. 35Definition 7.1dftr3 5228
[TakeutiZaring] p. 36Proposition 7.4ordwe 6330
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6338
[TakeutiZaring] p. 36Proposition 7.6ordelord 6339  ordelordALT 42809  ordelordALTVD 43139
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6345  ordelssne 6344
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6343
[TakeutiZaring] p. 37Proposition 7.9ordin 6347
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7716
[TakeutiZaring] p. 38Corollary 7.15ordsson 7717
[TakeutiZaring] p. 38Definition 7.11df-on 6321
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6349
[TakeutiZaring] p. 38Proposition 7.12onfrALT 42821  ordon 7711
[TakeutiZaring] p. 38Proposition 7.13onprc 7712
[TakeutiZaring] p. 39Theorem 7.17tfi 7789
[TakeutiZaring] p. 40Exercise 3ontr2 6364
[TakeutiZaring] p. 40Exercise 7dftr2 5224
[TakeutiZaring] p. 40Exercise 9onssmin 7727
[TakeutiZaring] p. 40Exercise 11unon 7766
[TakeutiZaring] p. 40Exercise 12ordun 6421
[TakeutiZaring] p. 40Exercise 14ordequn 6420
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7713
[TakeutiZaring] p. 40Proposition 7.20elssuni 4898
[TakeutiZaring] p. 41Definition 7.22df-suc 6323
[TakeutiZaring] p. 41Proposition 7.23sssucid 6397  sucidg 6398
[TakeutiZaring] p. 41Proposition 7.24onsuc 7746
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6411  ordnbtwn 6410
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7763
[TakeutiZaring] p. 42Exercise 1df-lim 6322
[TakeutiZaring] p. 42Exercise 4omssnlim 7817
[TakeutiZaring] p. 42Exercise 7ssnlim 7822
[TakeutiZaring] p. 42Exercise 8onsucssi 7777  ordelsuc 7755
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7757
[TakeutiZaring] p. 42Definition 7.27nlimon 7787
[TakeutiZaring] p. 42Definition 7.28dfom2 7804
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7825
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7827
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7828
[TakeutiZaring] p. 43Remarkomon 7814
[TakeutiZaring] p. 43Axiom 7inf3 9571  omex 9579
[TakeutiZaring] p. 43Theorem 7.32ordom 7812
[TakeutiZaring] p. 43Corollary 7.31find 7833
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7829
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7830
[TakeutiZaring] p. 44Exercise 1limomss 7807
[TakeutiZaring] p. 44Exercise 2int0 4923
[TakeutiZaring] p. 44Exercise 3trintss 5241
[TakeutiZaring] p. 44Exercise 4intss1 4924
[TakeutiZaring] p. 44Exercise 5intex 5294
[TakeutiZaring] p. 44Exercise 6oninton 7730
[TakeutiZaring] p. 44Exercise 11ordintdif 6367
[TakeutiZaring] p. 44Definition 7.35df-int 4908
[TakeutiZaring] p. 44Proposition 7.34noinfep 9596
[TakeutiZaring] p. 45Exercise 4onint 7725
[TakeutiZaring] p. 47Lemma 1tfrlem1 8322
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8343
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8344
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8345
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8352  tz7.44-2 8353  tz7.44-3 8354
[TakeutiZaring] p. 50Exercise 1smogt 8313
[TakeutiZaring] p. 50Exercise 3smoiso 8308
[TakeutiZaring] p. 50Definition 7.46df-smo 8292
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8391  tz7.49c 8392
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8389
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8388
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8390
[TakeutiZaring] p. 53Proposition 7.532eu5 2655
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9947
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9948
[TakeutiZaring] p. 56Definition 8.1oalim 8478  oasuc 8470
[TakeutiZaring] p. 57Remarktfindsg 7797
[TakeutiZaring] p. 57Proposition 8.2oacl 8481
[TakeutiZaring] p. 57Proposition 8.3oa0 8462  oa0r 8484
[TakeutiZaring] p. 57Proposition 8.16omcl 8482
[TakeutiZaring] p. 58Corollary 8.5oacan 8495
[TakeutiZaring] p. 58Proposition 8.4nnaord 8566  nnaordi 8565  oaord 8494  oaordi 8493
[TakeutiZaring] p. 59Proposition 8.6iunss2 5009  uniss2 4902
[TakeutiZaring] p. 59Proposition 8.7oawordri 8497
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8502  oawordex 8504
[TakeutiZaring] p. 59Proposition 8.9nnacl 8558
[TakeutiZaring] p. 59Proposition 8.10oaabs 8594
[TakeutiZaring] p. 60Remarkoancom 9587
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8507
[TakeutiZaring] p. 62Exercise 1nnarcl 8563
[TakeutiZaring] p. 62Exercise 5oaword1 8499
[TakeutiZaring] p. 62Definition 8.15om0x 8465  omlim 8479  omsuc 8472
[TakeutiZaring] p. 62Definition 8.15(a)om0 8463
[TakeutiZaring] p. 63Proposition 8.17nnecl 8560  nnmcl 8559
[TakeutiZaring] p. 63Proposition 8.19nnmord 8579  nnmordi 8578  omord 8515  omordi 8513
[TakeutiZaring] p. 63Proposition 8.20omcan 8516
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8583  omwordri 8519
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8485
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8489  om1r 8490
[TakeutiZaring] p. 64Proposition 8.22om00 8522
[TakeutiZaring] p. 64Proposition 8.23omordlim 8524
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8525
[TakeutiZaring] p. 64Proposition 8.25odi 8526
[TakeutiZaring] p. 65Theorem 8.26omass 8527
[TakeutiZaring] p. 67Definition 8.30nnesuc 8555  oe0 8468  oelim 8480  oesuc 8473  onesuc 8476
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8466
[TakeutiZaring] p. 67Proposition 8.32oen0 8533
[TakeutiZaring] p. 67Proposition 8.33oeordi 8534
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8467
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8492
[TakeutiZaring] p. 68Corollary 8.34oeord 8535
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8541
[TakeutiZaring] p. 68Proposition 8.35oewordri 8539
[TakeutiZaring] p. 68Proposition 8.37oeworde 8540
[TakeutiZaring] p. 69Proposition 8.41oeoa 8544
[TakeutiZaring] p. 70Proposition 8.42oeoe 8546
[TakeutiZaring] p. 73Theorem 9.1trcl 9664  tz9.1 9665
[TakeutiZaring] p. 76Definition 9.9df-r1 9700  r10 9704  r1lim 9708  r1limg 9707  r1suc 9706  r1sucg 9705
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9716  r1ord2 9717  r1ordg 9714
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9726
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9751  tz9.13 9727  tz9.13g 9728
[TakeutiZaring] p. 79Definition 9.14df-rank 9701  rankval 9752  rankvalb 9733  rankvalg 9753
[TakeutiZaring] p. 79Proposition 9.16rankel 9775  rankelb 9760
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9789  rankval3 9776  rankval3b 9762
[TakeutiZaring] p. 79Proposition 9.18rankonid 9765
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9731
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9770  rankr1c 9757  rankr1g 9768
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9771
[TakeutiZaring] p. 80Exercise 1rankss 9785  rankssb 9784
[TakeutiZaring] p. 80Exercise 2unbndrank 9778
[TakeutiZaring] p. 80Proposition 9.19bndrank 9777
[TakeutiZaring] p. 83Axiom of Choiceac4 10411  dfac3 10057
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9966  numth 10408  numth2 10407
[TakeutiZaring] p. 85Definition 10.4cardval 10482
[TakeutiZaring] p. 85Proposition 10.5cardid 10483  cardid2 9889
[TakeutiZaring] p. 85Proposition 10.9oncard 9896
[TakeutiZaring] p. 85Proposition 10.10carden 10487
[TakeutiZaring] p. 85Proposition 10.11cardidm 9895
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9880
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9901
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9893
[TakeutiZaring] p. 87Proposition 10.15pwen 9094
[TakeutiZaring] p. 88Exercise 1en0 8957
[TakeutiZaring] p. 88Exercise 7infensuc 9099
[TakeutiZaring] p. 89Exercise 10omxpen 9018
[TakeutiZaring] p. 90Corollary 10.23cardnn 9899
[TakeutiZaring] p. 90Definition 10.27alephiso 10034
[TakeutiZaring] p. 90Proposition 10.20nneneq 9153
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9172
[TakeutiZaring] p. 90Proposition 10.26alephprc 10035
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9158
[TakeutiZaring] p. 91Exercise 2alephle 10024
[TakeutiZaring] p. 91Exercise 3aleph0 10002
[TakeutiZaring] p. 91Exercise 4cardlim 9908
[TakeutiZaring] p. 91Exercise 7infpss 10153
[TakeutiZaring] p. 91Exercise 8infcntss 9265
[TakeutiZaring] p. 91Definition 10.29df-fin 8887  isfi 8916
[TakeutiZaring] p. 92Proposition 10.32onfin 9174
[TakeutiZaring] p. 92Proposition 10.34imadomg 10470
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9011
[TakeutiZaring] p. 93Proposition 10.35fodomb 10462
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10121  unxpdom 9197
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9910  cardsdomelir 9909
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9199
[TakeutiZaring] p. 94Proposition 10.39infxpen 9950
[TakeutiZaring] p. 95Definition 10.42df-map 8767
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10498  infxpidm2 9953
[TakeutiZaring] p. 95Proposition 10.41infdju 10144  infxp 10151
[TakeutiZaring] p. 96Proposition 10.44pw2en 9023  pw2f1o 9021
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9087
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10423
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10418  ac6s5 10427
[TakeutiZaring] p. 98Theorem 10.47unidom 10479
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10480  uniimadomf 10481
[TakeutiZaring] p. 100Definition 11.1cfcof 10210
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10205
[TakeutiZaring] p. 102Exercise 1cfle 10190
[TakeutiZaring] p. 102Exercise 2cf0 10187
[TakeutiZaring] p. 102Exercise 3cfsuc 10193
[TakeutiZaring] p. 102Exercise 4cfom 10200
[TakeutiZaring] p. 102Proposition 11.9coftr 10209
[TakeutiZaring] p. 103Theorem 11.15alephreg 10518
[TakeutiZaring] p. 103Proposition 11.11cardcf 10188
[TakeutiZaring] p. 103Proposition 11.13alephsing 10212
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10033
[TakeutiZaring] p. 104Proposition 11.16carduniima 10032
[TakeutiZaring] p. 104Proposition 11.18alephfp 10044  alephfp2 10045
[TakeutiZaring] p. 106Theorem 11.20gchina 10635
[TakeutiZaring] p. 106Theorem 11.21mappwen 10048
[TakeutiZaring] p. 107Theorem 11.26konigth 10505
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10519
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10520
[Tarski] p. 67Axiom B5ax-c5 37345
[Tarski] p. 67Scheme B5sp 2176
[Tarski] p. 68Lemma 6avril1 29407  equid 2015
[Tarski] p. 69Lemma 7equcomi 2020
[Tarski] p. 70Lemma 14spim 2385  spime 2387  spimew 1975
[Tarski] p. 70Lemma 16ax-12 2171  ax-c15 37351  ax12i 1970
[Tarski] p. 70Lemmas 16 and 17sb6 2088
[Tarski] p. 75Axiom B7ax6v 1972
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1913  ax5ALT 37369
[Tarski], p. 75Scheme B8 of system S2ax-7 2011  ax-8 2108  ax-9 2116
[Tarski1999] p. 178Axiom 4axtgsegcon 27406
[Tarski1999] p. 178Axiom 5axtg5seg 27407
[Tarski1999] p. 179Axiom 7axtgpasch 27409
[Tarski1999] p. 180Axiom 7.1axtgpasch 27409
[Tarski1999] p. 185Axiom 11axtgcont1 27410
[Truss] p. 114Theorem 5.18ruc 16125
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 36117
[Viaclovsky8] p. 3Proposition 7ismblfin 36119
[Weierstrass] p. 272Definitiondf-mdet 21934  mdetuni 21971
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 902
[WhiteheadRussell] p. 96Axiom *1.3olc 866
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 867
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 918
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 966
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 188
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 35916
[WhiteheadRussell] p. 100Theorem *2.05frege5 42062  imim2 58  wl-luk-imim2 35911
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 45244  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 895
[WhiteheadRussell] p. 101Theorem *2.06barbara 2662  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 901
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 35914
[WhiteheadRussell] p. 101Theorem *2.11exmid 893
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 896
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 43199  wl-luk-notnotr 35915
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 42092  axfrege28 42091  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 865
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 923
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 35908
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 888
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 938
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 29345  pm2.27 42  wl-luk-pm2.27 35906
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 921
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 36824
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 922
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 968
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 969
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 967
[WhiteheadRussell] p. 105Definition *2.33df-3or 1088
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 905
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 906
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 941
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 880
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 881
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 190
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 882
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 883
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 884
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 849
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 850
[WhiteheadRussell] p. 107Theorem *2.55orel1 887
[WhiteheadRussell] p. 107Theorem *2.56orel2 889
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 191
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 898
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 939
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 940
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 192
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 890  pm2.67 891
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 897
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 971
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 899
[WhiteheadRussell] p. 108Theorem *2.69looinv 202
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 972
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 973
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 932
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 930
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 970
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 974
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 931
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 990
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 470  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 991
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 992
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 993
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 994
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 472
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 460
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 403
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 801
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 449
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 450
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 483  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 485  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 763
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 764
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 806
[WhiteheadRussell] p. 113Fact)pm3.45 622
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 808
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 493
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 494
[WhiteheadRussell] p. 113Theorem *3.44jao 959  pm3.44 958
[WhiteheadRussell] p. 113Theorem *3.47anim12 807
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 474
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 962
[WhiteheadRussell] p. 116Theorem *4.1con34b 315
[WhiteheadRussell] p. 117Theorem *4.2biid 260
[WhiteheadRussell] p. 117Theorem *4.11notbi 318
[WhiteheadRussell] p. 117Theorem *4.12con2bi 353
[WhiteheadRussell] p. 117Theorem *4.13notnotb 314
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 805
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 831
[WhiteheadRussell] p. 117Theorem *4.21bicom 221
[WhiteheadRussell] p. 117Theorem *4.22biantr 804  bitr 803
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 564
[WhiteheadRussell] p. 117Theorem *4.25oridm 903  pm4.25 904
[WhiteheadRussell] p. 118Theorem *4.3ancom 461
[WhiteheadRussell] p. 118Theorem *4.4andi 1006
[WhiteheadRussell] p. 118Theorem *4.31orcom 868
[WhiteheadRussell] p. 118Theorem *4.32anass 469
[WhiteheadRussell] p. 118Theorem *4.33orass 920
[WhiteheadRussell] p. 118Theorem *4.36anbi1 632
[WhiteheadRussell] p. 118Theorem *4.37orbi1 916
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 636
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 975
[WhiteheadRussell] p. 118Definition *4.34df-3an 1089
[WhiteheadRussell] p. 119Theorem *4.41ordi 1004
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1052
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1021
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 995
[WhiteheadRussell] p. 119Theorem *4.45orabs 997  pm4.45 996  pm4.45im 826
[WhiteheadRussell] p. 120Theorem *4.5anor 981
[WhiteheadRussell] p. 120Theorem *4.6imor 851
[WhiteheadRussell] p. 120Theorem *4.7anclb 546
[WhiteheadRussell] p. 120Theorem *4.51ianor 980
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 983
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 984
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 985
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 986
[WhiteheadRussell] p. 120Theorem *4.56ioran 982  pm4.56 987
[WhiteheadRussell] p. 120Theorem *4.57oran 988  pm4.57 989
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 405
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 854
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 398
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 847
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 406
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 848
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 399
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 558  pm4.71d 562  pm4.71i 560  pm4.71r 559  pm4.71rd 563  pm4.71ri 561
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 948
[WhiteheadRussell] p. 121Theorem *4.73iba 528
[WhiteheadRussell] p. 121Theorem *4.74biorf 935
[WhiteheadRussell] p. 121Theorem *4.76jcab 518  pm4.76 519
[WhiteheadRussell] p. 121Theorem *4.77jaob 960  pm4.77 961
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 933
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1002
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 393
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 394
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1022
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1023
[WhiteheadRussell] p. 122Theorem *4.84imbi1 347
[WhiteheadRussell] p. 122Theorem *4.85imbi2 348
[WhiteheadRussell] p. 122Theorem *4.86bibi1 351
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 388  impexp 451  pm4.87 841
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 822
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 943  pm5.11g 942
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 944
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 946
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 945
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1011
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1012
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1010
[WhiteheadRussell] p. 124Theorem *5.18nbbn 384  pm5.18 382
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 387
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 823
[WhiteheadRussell] p. 124Theorem *5.22xor 1013
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1048
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1049
[WhiteheadRussell] p. 124Theorem *5.25dfor2 900
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 573
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 389
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 361
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1000
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 952
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 829
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 574
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 834
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 824
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 832
[WhiteheadRussell] p. 125Theorem *5.41imdi 390  pm5.41 391
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 544
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 543
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1003
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1016
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 947
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 999
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1017
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1018
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1026
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 269
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1027
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 42628
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 42629
[WhiteheadRussell] p. 147Theorem *10.2219.26 1873
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 42630
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 42631
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 42632
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1896
[WhiteheadRussell] p. 151Theorem *10.301albitr 42633
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 42634
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 42635
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 42636
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 42637
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 42639
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 42640
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 42641
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 42638
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2093
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 42644
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 42645
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2073
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2157
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1831
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1832
[WhiteheadRussell] p. 161Theorem *11.319.21vv 42646
[WhiteheadRussell] p. 162Theorem *11.322alim 42647
[WhiteheadRussell] p. 162Theorem *11.332albi 42648
[WhiteheadRussell] p. 162Theorem *11.342exim 42649
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 42651
[WhiteheadRussell] p. 162Theorem *11.3412exbi 42650
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1890
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 42653
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 42654
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 42652
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1830
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 42655
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 42656
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1848
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 42657
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2342
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1863
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 42662
[WhiteheadRussell] p. 165Theorem *11.56aaanv 42658
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 42659
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 42660
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 42661
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 42666
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 42663
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 42664
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 42665
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 42667
[WhiteheadRussell] p. 175Definition *14.02df-eu 2567
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 42677  pm13.13b 42678
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 42679
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3025
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3026
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3618
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 42685
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 42686
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 42680
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 42824  pm13.193 42681
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 42682
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 42683
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 42684
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 42691
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 42690
[WhiteheadRussell] p. 184Definition *14.01iotasbc 42689
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3807
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 42692  pm14.122b 42693  pm14.122c 42694
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 42695  pm14.123b 42696  pm14.123c 42697
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 42699
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 42698
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 42700
[WhiteheadRussell] p. 190Theorem *14.22iota4 6477
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 42701
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6478
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 42702
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 42704
[WhiteheadRussell] p. 192Theorem *14.26eupick 2633  eupickbi 2636  sbaniota 42705
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 42703
[WhiteheadRussell] p. 192Theorem *14.271eubi 2582
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 42707
[WhiteheadRussell] p. 235Definition *30.01conventions 29344  df-fv 6504
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9937  pm54.43lem 9936
[Young] p. 141Definition of operator orderingleop2 31066
[Young] p. 142Example 12.2(i)0leop 31072  idleop 31073
[vandenDries] p. 42Lemma 61irrapx1 41137
[vandenDries] p. 43Theorem 62pellex 41144  pellexlem1 41138

This page was last updated on 18-Feb-2025.
Copyright terms: Public domain