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 17726
[Adamek] p. 21Condition 3.1(b)df-cat 17726
[Adamek] p. 22Example 3.3(1)df-setc 18143
[Adamek] p. 24Example 3.3(4.c)0cat 17747
[Adamek] p. 24Example 3.3(4.d)df-prstc 48730  prsthinc 48721
[Adamek] p. 24Example 3.3(4.e)df-mndtc 48751  df-mndtc 48751
[Adamek] p. 25Definition 3.5df-oppc 17770
[Adamek] p. 28Remark 3.9oppciso 17842
[Adamek] p. 28Remark 3.12invf1o 17830  invisoinvl 17851
[Adamek] p. 28Example 3.13idinv 17850  idiso 17849
[Adamek] p. 28Corollary 3.11inveq 17835
[Adamek] p. 28Definition 3.8df-inv 17809  df-iso 17810  dfiso2 17833
[Adamek] p. 28Proposition 3.10sectcan 17816
[Adamek] p. 29Remark 3.16cicer 17867
[Adamek] p. 29Definition 3.15cic 17860  df-cic 17857
[Adamek] p. 29Definition 3.17df-func 17922
[Adamek] p. 29Proposition 3.14(1)invinv 17831
[Adamek] p. 29Proposition 3.14(2)invco 17832  isoco 17838
[Adamek] p. 30Remark 3.19df-func 17922
[Adamek] p. 30Example 3.20(1)idfucl 17945
[Adamek] p. 32Proposition 3.21funciso 17938
[Adamek] p. 33Example 3.26(2)df-thinc 48687  prsthinc 48721  thincciso 48716
[Adamek] p. 33Example 3.26(3)df-mndtc 48751
[Adamek] p. 33Proposition 3.23cofucl 17952
[Adamek] p. 34Remark 3.28(2)catciso 18178
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18236
[Adamek] p. 34Definition 3.27(2)df-fth 17972
[Adamek] p. 34Definition 3.27(3)df-full 17971
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18236
[Adamek] p. 35Corollary 3.32ffthiso 17996
[Adamek] p. 35Proposition 3.30(c)cofth 18002
[Adamek] p. 35Proposition 3.30(d)cofull 18001
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18221
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18221
[Adamek] p. 39Definition 3.41funcoppc 17939
[Adamek] p. 39Definition 3.44.df-catc 18166
[Adamek] p. 39Proposition 3.43(c)fthoppc 17990
[Adamek] p. 39Proposition 3.43(d)fulloppc 17989
[Adamek] p. 40Remark 3.48catccat 18175
[Adamek] p. 40Definition 3.47df-catc 18166
[Adamek] p. 48Example 4.3(1.a)0subcat 17902
[Adamek] p. 48Example 4.3(1.b)catsubcat 17903
[Adamek] p. 48Definition 4.1(2)fullsubc 17914
[Adamek] p. 48Definition 4.1(a)df-subc 17873
[Adamek] p. 49Remark 4.4(2)ressffth 18005
[Adamek] p. 83Definition 6.1df-nat 18011
[Adamek] p. 87Remark 6.14(a)fuccocl 18034
[Adamek] p. 87Remark 6.14(b)fucass 18038
[Adamek] p. 87Definition 6.15df-fuc 18012
[Adamek] p. 88Remark 6.16fuccat 18040
[Adamek] p. 101Definition 7.1df-inito 18051
[Adamek] p. 101Example 7.2 (6)irinitoringc 21513
[Adamek] p. 102Definition 7.4df-termo 18052
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18079
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18083
[Adamek] p. 103Definition 7.7df-zeroo 18053
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21514
[Adamek] p. 103Proposition 7.6termoeu1w 18086
[Adamek] p. 106Definition 7.19df-sect 17808
[Adamek] p. 185Section 10.67updjud 10003
[Adamek] p. 478Item Rngdf-ringc 20668
[AhoHopUll] p. 2Section 1.1df-bigo 48282
[AhoHopUll] p. 12Section 1.3df-blen 48304
[AhoHopUll] p. 318Section 9.1df-concat 14619  df-pfx 14719  df-substr 14689  df-word 14563  lencl 14581  wrd0 14587
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24750  df-nmoo 30777
[AkhiezerGlazman] p. 64Theoremhmopidmch 32185  hmopidmchi 32183
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32233  pjcmul2i 32234
[AkhiezerGlazman] p. 72Theoremcnvunop 31950  unoplin 31952
[AkhiezerGlazman] p. 72Equation 2unopadj 31951  unopadj2 31970
[AkhiezerGlazman] p. 73Theoremelunop2 32045  lnopunii 32044
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32118
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27979
[Alling] p. 184Axiom Bbdayfo 27740
[Alling] p. 184Axiom Osltso 27739
[Alling] p. 184Axiom SDnodense 27755
[Alling] p. 185Lemma 0nocvxmin 27841
[Alling] p. 185Theoremconway 27862
[Alling] p. 185Axiom FEnoeta 27806
[Alling] p. 186Theorem 4slerec 27882
[Alling], p. 2Definitionrp-brsslt 43385
[Alling], p. 3Notenla0001 43388  nla0002 43386  nla0003 43387
[Apostol] p. 18Theorem I.1addcan 11474  addcan2d 11494  addcan2i 11484  addcand 11493  addcani 11483
[Apostol] p. 18Theorem I.2negeu 11526
[Apostol] p. 18Theorem I.3negsub 11584  negsubd 11653  negsubi 11614
[Apostol] p. 18Theorem I.4negneg 11586  negnegd 11638  negnegi 11606
[Apostol] p. 18Theorem I.5subdi 11723  subdid 11746  subdii 11739  subdir 11724  subdird 11747  subdiri 11740
[Apostol] p. 18Theorem I.6mul01 11469  mul01d 11489  mul01i 11480  mul02 11468  mul02d 11488  mul02i 11479
[Apostol] p. 18Theorem I.7mulcan 11927  mulcan2d 11924  mulcand 11923  mulcani 11929
[Apostol] p. 18Theorem I.8receu 11935  xreceu 32886
[Apostol] p. 18Theorem I.9divrec 11965  divrecd 12073  divreci 12039  divreczi 12032
[Apostol] p. 18Theorem I.10recrec 11991  recreci 12026
[Apostol] p. 18Theorem I.11mul0or 11930  mul0ord 11940  mul0ori 11938
[Apostol] p. 18Theorem I.12mul2neg 11729  mul2negd 11745  mul2negi 11738  mulneg1 11726  mulneg1d 11743  mulneg1i 11736
[Apostol] p. 18Theorem I.13divadddiv 12009  divadddivd 12114  divadddivi 12056
[Apostol] p. 18Theorem I.14divmuldiv 11994  divmuldivd 12111  divmuldivi 12054  rdivmuldivd 20439
[Apostol] p. 18Theorem I.15divdivdiv 11995  divdivdivd 12117  divdivdivi 12057
[Apostol] p. 20Axiom 7rpaddcl 13079  rpaddcld 13114  rpmulcl 13080  rpmulcld 13115
[Apostol] p. 20Axiom 8rpneg 13089
[Apostol] p. 20Axiom 90nrp 13092
[Apostol] p. 20Theorem I.17lttri 11416
[Apostol] p. 20Theorem I.18ltadd1d 11883  ltadd1dd 11901  ltadd1i 11844
[Apostol] p. 20Theorem I.19ltmul1 12144  ltmul1a 12143  ltmul1i 12213  ltmul1ii 12223  ltmul2 12145  ltmul2d 13141  ltmul2dd 13155  ltmul2i 12216
[Apostol] p. 20Theorem I.20msqgt0 11810  msqgt0d 11857  msqgt0i 11827
[Apostol] p. 20Theorem I.210lt1 11812
[Apostol] p. 20Theorem I.23lt0neg1 11796  lt0neg1d 11859  ltneg 11790  ltnegd 11868  ltnegi 11834
[Apostol] p. 20Theorem I.25lt2add 11775  lt2addd 11913  lt2addi 11852
[Apostol] p. 20Definition of positive numbersdf-rp 13058
[Apostol] p. 21Exercise 4recgt0 12140  recgt0d 12229  recgt0i 12200  recgt0ii 12201
[Apostol] p. 22Definition of integersdf-z 12640
[Apostol] p. 22Definition of positive integersdfnn3 12307
[Apostol] p. 22Definition of rationalsdf-q 13014
[Apostol] p. 24Theorem I.26supeu 9523
[Apostol] p. 26Theorem I.28nnunb 12549
[Apostol] p. 26Theorem I.29arch 12550  archd 45067
[Apostol] p. 28Exercise 2btwnz 12746
[Apostol] p. 28Exercise 3nnrecl 12551
[Apostol] p. 28Exercise 4rebtwnz 13012
[Apostol] p. 28Exercise 5zbtwnre 13011
[Apostol] p. 28Exercise 6qbtwnre 13261
[Apostol] p. 28Exercise 10(a)zeneo 16387  zneo 12726  zneoALTV 47543
[Apostol] p. 29Theorem I.35cxpsqrtth 26790  msqsqrtd 15489  resqrtth 15304  sqrtth 15413  sqrtthi 15419  sqsqrtd 15488
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12296
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12978
[Apostol] p. 361Remarkcrreczi 14277
[Apostol] p. 363Remarkabsgt0i 15448
[Apostol] p. 363Exampleabssubd 15502  abssubi 15452
[ApostolNT] p. 7Remarkfmtno0 47414  fmtno1 47415  fmtno2 47424  fmtno3 47425  fmtno4 47426  fmtno5fac 47456  fmtnofz04prm 47451
[ApostolNT] p. 7Definitiondf-fmtno 47402
[ApostolNT] p. 8Definitiondf-ppi 27161
[ApostolNT] p. 14Definitiondf-dvds 16303
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16318
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16342
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16337
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16331
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16333
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16319
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16320
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16325
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16359
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16361
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16363
[ApostolNT] p. 15Definitiondf-gcd 16541  dfgcd2 16593
[ApostolNT] p. 16Definitionisprm2 16729
[ApostolNT] p. 16Theorem 1.5coprmdvds 16700
[ApostolNT] p. 16Theorem 1.7prminf 16962
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16559
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16594
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16596
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16574
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16566
[ApostolNT] p. 17Theorem 1.8coprm 16758
[ApostolNT] p. 17Theorem 1.9euclemma 16760
[ApostolNT] p. 17Theorem 1.101arith2 16975
[ApostolNT] p. 18Theorem 1.13prmrec 16969
[ApostolNT] p. 19Theorem 1.14divalg 16451
[ApostolNT] p. 20Theorem 1.15eucalg 16634
[ApostolNT] p. 24Definitiondf-mu 27162
[ApostolNT] p. 25Definitiondf-phi 16813
[ApostolNT] p. 25Theorem 2.1musum 27252
[ApostolNT] p. 26Theorem 2.2phisum 16837
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16823
[ApostolNT] p. 28Theorem 2.5(c)phimul 16827
[ApostolNT] p. 32Definitiondf-vma 27159
[ApostolNT] p. 32Theorem 2.9muinv 27254
[ApostolNT] p. 32Theorem 2.10vmasum 27278
[ApostolNT] p. 38Remarkdf-sgm 27163
[ApostolNT] p. 38Definitiondf-sgm 27163
[ApostolNT] p. 75Definitiondf-chp 27160  df-cht 27158
[ApostolNT] p. 104Definitioncongr 16711
[ApostolNT] p. 106Remarkdvdsval3 16306
[ApostolNT] p. 106Definitionmoddvds 16313
[ApostolNT] p. 107Example 2mod2eq0even 16394
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16395
[ApostolNT] p. 107Example 4zmod1congr 13939
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13976
[ApostolNT] p. 107Theorem 5.2(c)modexp 14287
[ApostolNT] p. 108Theorem 5.3modmulconst 16336
[ApostolNT] p. 109Theorem 5.4cncongr1 16714
[ApostolNT] p. 109Theorem 5.6gcdmodi 17121
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16716
[ApostolNT] p. 113Theorem 5.17eulerth 16830
[ApostolNT] p. 113Theorem 5.18vfermltl 16848
[ApostolNT] p. 114Theorem 5.19fermltl 16831
[ApostolNT] p. 116Theorem 5.24wilthimp 27133
[ApostolNT] p. 179Definitiondf-lgs 27357  lgsprme0 27401
[ApostolNT] p. 180Example 11lgs 27402
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27378
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27393
[ApostolNT] p. 181Theorem 9.4m1lgs 27450
[ApostolNT] p. 181Theorem 9.52lgs 27469  2lgsoddprm 27478
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27436
[ApostolNT] p. 185Theorem 9.8lgsquad 27445
[ApostolNT] p. 188Definitiondf-lgs 27357  lgs1 27403
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27394
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27396
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27404
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27405
[Baer] p. 40Property (b)mapdord 41595
[Baer] p. 40Property (c)mapd11 41596
[Baer] p. 40Property (e)mapdin 41619  mapdlsm 41621
[Baer] p. 40Property (f)mapd0 41622
[Baer] p. 40Definition of projectivitydf-mapd 41582  mapd1o 41605
[Baer] p. 41Property (g)mapdat 41624
[Baer] p. 44Part (1)mapdpg 41663
[Baer] p. 45Part (2)hdmap1eq 41758  mapdheq 41685  mapdheq2 41686  mapdheq2biN 41687
[Baer] p. 45Part (3)baerlem3 41670
[Baer] p. 46Part (4)mapdheq4 41689  mapdheq4lem 41688
[Baer] p. 46Part (5)baerlem5a 41671  baerlem5abmN 41675  baerlem5amN 41673  baerlem5b 41672  baerlem5bmN 41674
[Baer] p. 47Part (6)hdmap1l6 41778  hdmap1l6a 41766  hdmap1l6e 41771  hdmap1l6f 41772  hdmap1l6g 41773  hdmap1l6lem1 41764  hdmap1l6lem2 41765  mapdh6N 41704  mapdh6aN 41692  mapdh6eN 41697  mapdh6fN 41698  mapdh6gN 41699  mapdh6lem1N 41690  mapdh6lem2N 41691
[Baer] p. 48Part 9hdmapval 41785
[Baer] p. 48Part 10hdmap10 41797
[Baer] p. 48Part 11hdmapadd 41800
[Baer] p. 48Part (6)hdmap1l6h 41774  mapdh6hN 41700
[Baer] p. 48Part (7)mapdh75cN 41710  mapdh75d 41711  mapdh75e 41709  mapdh75fN 41712  mapdh7cN 41706  mapdh7dN 41707  mapdh7eN 41705  mapdh7fN 41708
[Baer] p. 48Part (8)mapdh8 41745  mapdh8a 41732  mapdh8aa 41733  mapdh8ab 41734  mapdh8ac 41735  mapdh8ad 41736  mapdh8b 41737  mapdh8c 41738  mapdh8d 41740  mapdh8d0N 41739  mapdh8e 41741  mapdh8g 41742  mapdh8i 41743  mapdh8j 41744
[Baer] p. 48Part (9)mapdh9a 41746
[Baer] p. 48Equation 10mapdhvmap 41726
[Baer] p. 49Part 12hdmap11 41805  hdmapeq0 41801  hdmapf1oN 41822  hdmapneg 41803  hdmaprnN 41821  hdmaprnlem1N 41806  hdmaprnlem3N 41807  hdmaprnlem3uN 41808  hdmaprnlem4N 41810  hdmaprnlem6N 41811  hdmaprnlem7N 41812  hdmaprnlem8N 41813  hdmaprnlem9N 41814  hdmapsub 41804
[Baer] p. 49Part 14hdmap14lem1 41825  hdmap14lem10 41834  hdmap14lem1a 41823  hdmap14lem2N 41826  hdmap14lem2a 41824  hdmap14lem3 41827  hdmap14lem8 41832  hdmap14lem9 41833
[Baer] p. 50Part 14hdmap14lem11 41835  hdmap14lem12 41836  hdmap14lem13 41837  hdmap14lem14 41838  hdmap14lem15 41839  hgmapval 41844
[Baer] p. 50Part 15hgmapadd 41851  hgmapmul 41852  hgmaprnlem2N 41854  hgmapvs 41848
[Baer] p. 50Part 16hgmaprnN 41858
[Baer] p. 110Lemma 1hdmapip0com 41874
[Baer] p. 110Line 27hdmapinvlem1 41875
[Baer] p. 110Line 28hdmapinvlem2 41876
[Baer] p. 110Line 30hdmapinvlem3 41877
[Baer] p. 110Part 1.2hdmapglem5 41879  hgmapvv 41883
[Baer] p. 110Proposition 1hdmapinvlem4 41878
[Baer] p. 111Line 10hgmapvvlem1 41880
[Baer] p. 111Line 15hdmapg 41887  hdmapglem7 41886
[Bauer], p. 483Theorem 1.22irrexpq 26791  2irrexpqALT 26861
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2572
[BellMachover] p. 460Notationdf-mo 2543
[BellMachover] p. 460Definitionmo3 2567
[BellMachover] p. 461Axiom Extax-ext 2711
[BellMachover] p. 462Theorem 1.1axextmo 2715
[BellMachover] p. 463Axiom Repaxrep5 5309
[BellMachover] p. 463Scheme Sepax-sep 5317
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37030  bm1.3ii 5320
[BellMachover] p. 466Problemaxpow2 5385
[BellMachover] p. 466Axiom Powaxpow3 5386
[BellMachover] p. 466Axiom Unionaxun2 7772
[BellMachover] p. 468Definitiondf-ord 6398
[BellMachover] p. 469Theorem 2.2(i)ordirr 6413
[BellMachover] p. 469Theorem 2.2(iii)onelon 6420
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6415
[BellMachover] p. 471Definition of Ndf-om 7904
[BellMachover] p. 471Problem 2.5(ii)uniordint 7837
[BellMachover] p. 471Definition of Limdf-lim 6400
[BellMachover] p. 472Axiom Infzfinf2 9711
[BellMachover] p. 473Theorem 2.8limom 7919
[BellMachover] p. 477Equation 3.1df-r1 9833
[BellMachover] p. 478Definitionrankval2 9887
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9851  r1ord3g 9848
[BellMachover] p. 480Axiom Regzfreg 9664
[BellMachover] p. 488Axiom ACac5 10546  dfac4 10191
[BellMachover] p. 490Definition of alephalephval3 10179
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39275
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32385
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32427  chirredi 32426
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32415
[Beran] p. 3Definition of joinsshjval3 31386
[Beran] p. 39Theorem 2.3(i)cmcm2 31648  cmcm2i 31625  cmcm2ii 31630  cmt2N 39206
[Beran] p. 40Theorem 2.3(iii)lecm 31649  lecmi 31634  lecmii 31635
[Beran] p. 45Theorem 3.4cmcmlem 31623
[Beran] p. 49Theorem 4.2cm2j 31652  cm2ji 31657  cm2mi 31658
[Beran] p. 95Definitiondf-sh 31239  issh2 31241
[Beran] p. 95Lemma 3.1(S5)his5 31118
[Beran] p. 95Lemma 3.1(S6)his6 31131
[Beran] p. 95Lemma 3.1(S7)his7 31122
[Beran] p. 95Lemma 3.2(S8)ho01i 31860
[Beran] p. 95Lemma 3.2(S9)hoeq1 31862
[Beran] p. 95Lemma 3.2(S10)ho02i 31861
[Beran] p. 95Lemma 3.2(S11)hoeq2 31863
[Beran] p. 95Postulate (S1)ax-his1 31114  his1i 31132
[Beran] p. 95Postulate (S2)ax-his2 31115
[Beran] p. 95Postulate (S3)ax-his3 31116
[Beran] p. 95Postulate (S4)ax-his4 31117
[Beran] p. 96Definition of normdf-hnorm 31000  dfhnorm2 31154  normval 31156
[Beran] p. 96Definition for Cauchy sequencehcau 31216
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31005
[Beran] p. 96Definition of complete subspaceisch3 31273
[Beran] p. 96Definition of convergedf-hlim 31004  hlimi 31220
[Beran] p. 97Theorem 3.3(i)norm-i-i 31165  norm-i 31161
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31169  norm-ii 31170  normlem0 31141  normlem1 31142  normlem2 31143  normlem3 31144  normlem4 31145  normlem5 31146  normlem6 31147  normlem7 31148  normlem7tALT 31151
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31171  norm-iii 31172
[Beran] p. 98Remark 3.4bcs 31213  bcsiALT 31211  bcsiHIL 31212
[Beran] p. 98Remark 3.4(B)normlem9at 31153  normpar 31187  normpari 31186
[Beran] p. 98Remark 3.4(C)normpyc 31178  normpyth 31177  normpythi 31174
[Beran] p. 99Remarklnfn0 32079  lnfn0i 32074  lnop0 31998  lnop0i 32002
[Beran] p. 99Theorem 3.5(i)nmcexi 32058  nmcfnex 32085  nmcfnexi 32083  nmcopex 32061  nmcopexi 32059
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32086  nmcfnlbi 32084  nmcoplb 32062  nmcoplbi 32060
[Beran] p. 99Theorem 3.5(iii)lnfncon 32088  lnfnconi 32087  lnopcon 32067  lnopconi 32066
[Beran] p. 100Lemma 3.6normpar2i 31188
[Beran] p. 101Lemma 3.6norm3adifi 31185  norm3adifii 31180  norm3dif 31182  norm3difi 31179
[Beran] p. 102Theorem 3.7(i)chocunii 31333  pjhth 31425  pjhtheu 31426  pjpjhth 31457  pjpjhthi 31458  pjth 25492
[Beran] p. 102Theorem 3.7(ii)ococ 31438  ococi 31437
[Beran] p. 103Remark 3.8nlelchi 32093
[Beran] p. 104Theorem 3.9riesz3i 32094  riesz4 32096  riesz4i 32095
[Beran] p. 104Theorem 3.10cnlnadj 32111  cnlnadjeu 32110  cnlnadjeui 32109  cnlnadji 32108  cnlnadjlem1 32099  nmopadjlei 32120
[Beran] p. 106Theorem 3.11(i)adjeq0 32123
[Beran] p. 106Theorem 3.11(v)nmopadji 32122
[Beran] p. 106Theorem 3.11(ii)adjmul 32124
[Beran] p. 106Theorem 3.11(iv)adjadj 31968
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32134  nmopcoadji 32133
[Beran] p. 106Theorem 3.11(iii)adjadd 32125
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32135
[Beran] p. 106Theorem 3.11(viii)adjcoi 32132  pjadj2coi 32236  pjadjcoi 32193
[Beran] p. 107Definitiondf-ch 31253  isch2 31255
[Beran] p. 107Remark 3.12choccl 31338  isch3 31273  occl 31336  ocsh 31315  shoccl 31337  shocsh 31316
[Beran] p. 107Remark 3.12(B)ococin 31440
[Beran] p. 108Theorem 3.13chintcl 31364
[Beran] p. 109Property (i)pjadj2 32219  pjadj3 32220  pjadji 31717  pjadjii 31706
[Beran] p. 109Property (ii)pjidmco 32213  pjidmcoi 32209  pjidmi 31705
[Beran] p. 110Definition of projector orderingpjordi 32205
[Beran] p. 111Remarkho0val 31782  pjch1 31702
[Beran] p. 111Definitiondf-hfmul 31766  df-hfsum 31765  df-hodif 31764  df-homul 31763  df-hosum 31762
[Beran] p. 111Lemma 4.4(i)pjo 31703
[Beran] p. 111Lemma 4.4(ii)pjch 31726  pjchi 31464
[Beran] p. 111Lemma 4.4(iii)pjoc2 31471  pjoc2i 31470
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31712
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32197  pjssmii 31713
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32196
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32195
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32200
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32198  pjssge0ii 31714
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32199  pjdifnormii 31715
[Bobzien] p. 116Statement T3stoic3 1774
[Bobzien] p. 117Statement T2stoic2a 1772
[Bobzien] p. 117Statement T4stoic4a 1775
[Bobzien] p. 117Conclusion the contradictorystoic1a 1770
[Bogachev] p. 16Definition 1.5df-oms 34257
[Bogachev] p. 17Lemma 1.5.4omssubadd 34265
[Bogachev] p. 17Example 1.5.2omsmon 34263
[Bogachev] p. 41Definition 1.11.2df-carsg 34267
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34287
[Bogachev] p. 116Definition 2.3.1df-itgm 34318  df-sitm 34296
[Bogachev] p. 118Chapter 2.4.4df-itgm 34318
[Bogachev] p. 118Definition 2.4.1df-sitg 34295
[Bollobas] p. 1Section I.1df-edg 29083  isuhgrop 29105  isusgrop 29197  isuspgrop 29196
[Bollobas] p. 2Section I.1df-isubgr 47733  df-subgr 29303  uhgrspan1 29338  uhgrspansubgr 29326
[Bollobas] p. 3Definitiondf-gric 47751  gricuspgr 47771  isuspgrim 47759
[Bollobas] p. 3Section I.1cusgrsize 29490  df-clnbgr 47693  df-cusgr 29447  df-nbgr 29368  fusgrmaxsize 29500
[Bollobas] p. 4Definitiondf-upwlks 47857  df-wlks 29635
[Bollobas] p. 4Section I.1finsumvtxdg2size 29586  finsumvtxdgeven 29588  fusgr1th 29587  fusgrvtxdgonume 29590  vtxdgoddnumeven 29589
[Bollobas] p. 5Notationdf-pths 29752
[Bollobas] p. 5Definitiondf-crcts 29822  df-cycls 29823  df-trls 29728  df-wlkson 29636
[Bollobas] p. 7Section I.1df-ushgr 29094
[BourbakiAlg1] p. 1Definition 1df-clintop 47923  df-cllaw 47909  df-mgm 18678  df-mgm2 47942
[BourbakiAlg1] p. 4Definition 5df-assintop 47924  df-asslaw 47911  df-sgrp 18757  df-sgrp2 47944
[BourbakiAlg1] p. 7Definition 8df-cmgm2 47943  df-comlaw 47910
[BourbakiAlg1] p. 12Definition 2df-mnd 18773
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33012  mndlactf1o 33016  mndractf1 33014  mndractf1o 33017
[BourbakiAlg1] p. 92Definition 1df-ring 20262
[BourbakiAlg1] p. 93Section I.8.1df-rng 20180
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33646
[BourbakiAlg2] p. 113Chapter 5.assafld 33650  assarrginv 33649
[BourbakiCAlg2], p. 228Proposition 21arithidom 33530  dfufd2 33543
[BourbakiEns] p. Proposition 8fcof1 7323  fcofo 7324
[BourbakiTop1] p. Remarkxnegmnf 13272  xnegpnf 13271
[BourbakiTop1] p. Remark rexneg 13273
[BourbakiTop1] p. Remark 3ust0 24249  ustfilxp 24242
[BourbakiTop1] p. Axiom GT'tgpsubcn 24119
[BourbakiTop1] p. Criterionishmeo 23788
[BourbakiTop1] p. Example 1cstucnd 24314  iducn 24313  snfil 23893
[BourbakiTop1] p. Example 2neifil 23909
[BourbakiTop1] p. Theorem 1cnextcn 24096
[BourbakiTop1] p. Theorem 2ucnextcn 24334
[BourbakiTop1] p. Theorem 3df-hcmp 33903
[BourbakiTop1] p. Paragraph 3infil 23892
[BourbakiTop1] p. Definition 1df-ucn 24306  df-ust 24230  filintn0 23890  filn0 23891  istgp 24106  ucnprima 24312
[BourbakiTop1] p. Definition 2df-cfilu 24317
[BourbakiTop1] p. Definition 3df-cusp 24328  df-usp 24287  df-utop 24261  trust 24259
[BourbakiTop1] p. Definition 6df-pcmp 33802
[BourbakiTop1] p. Property V_issnei2 23145
[BourbakiTop1] p. Theorem 1(d)iscncl 23298
[BourbakiTop1] p. Condition F_Iustssel 24235
[BourbakiTop1] p. Condition U_Iustdiag 24238
[BourbakiTop1] p. Property V_iiinnei 23154
[BourbakiTop1] p. Property V_ivneiptopreu 23162  neissex 23156
[BourbakiTop1] p. Proposition 1neips 23142  neiss 23138  ucncn 24315  ustund 24251  ustuqtop 24276
[BourbakiTop1] p. Proposition 2cnpco 23296  neiptopreu 23162  utop2nei 24280  utop3cls 24281
[BourbakiTop1] p. Proposition 3fmucnd 24322  uspreg 24304  utopreg 24282
[BourbakiTop1] p. Proposition 4imasncld 23720  imasncls 23721  imasnopn 23719
[BourbakiTop1] p. Proposition 9cnpflf2 24029
[BourbakiTop1] p. Condition F_IIustincl 24237
[BourbakiTop1] p. Condition U_IIustinvel 24239
[BourbakiTop1] p. Property V_iiielnei 23140
[BourbakiTop1] p. Proposition 11cnextucn 24333
[BourbakiTop1] p. Condition F_IIbustbasel 24236
[BourbakiTop1] p. Condition U_IIIustexhalf 24240
[BourbakiTop1] p. Definition C'''df-cmp 23416
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23875
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22921
[BourbakiTop2] p. 195Definition 1df-ldlf 33799
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 45983
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 45985  stoweid 45984
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 45922  stoweidlem10 45931  stoweidlem14 45935  stoweidlem15 45936  stoweidlem35 45956  stoweidlem36 45957  stoweidlem37 45958  stoweidlem38 45959  stoweidlem40 45961  stoweidlem41 45962  stoweidlem43 45964  stoweidlem44 45965  stoweidlem46 45967  stoweidlem5 45926  stoweidlem50 45971  stoweidlem52 45973  stoweidlem53 45974  stoweidlem55 45976  stoweidlem56 45977
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 45944  stoweidlem24 45945  stoweidlem27 45948  stoweidlem28 45949  stoweidlem30 45951
[BrosowskiDeutsh] p. 91Proofstoweidlem34 45955  stoweidlem59 45980  stoweidlem60 45981
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 45966  stoweidlem49 45970  stoweidlem7 45928
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 45952  stoweidlem39 45960  stoweidlem42 45963  stoweidlem48 45969  stoweidlem51 45972  stoweidlem54 45975  stoweidlem57 45978  stoweidlem58 45979
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 45946
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 45938
[BrosowskiDeutsh] p. 92Proofstoweidlem11 45932  stoweidlem13 45934  stoweidlem26 45947  stoweidlem61 45982
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 45939
[Bruck] p. 1Section I.1df-clintop 47923  df-mgm 18678  df-mgm2 47942
[Bruck] p. 23Section II.1df-sgrp 18757  df-sgrp2 47944
[Bruck] p. 28Theorem 3.2dfgrp3 19079
[ChoquetDD] p. 2Definition of mappingdf-mpt 5250
[Church] p. 129Section II.24df-ifp 1064  dfifp2 1065
[Clemente] p. 10Definition ITnatded 30435
[Clemente] p. 10Definition I` `m,nnatded 30435
[Clemente] p. 11Definition E=>m,nnatded 30435
[Clemente] p. 11Definition I=>m,nnatded 30435
[Clemente] p. 11Definition E` `(1)natded 30435
[Clemente] p. 11Definition E` `(2)natded 30435
[Clemente] p. 12Definition E` `m,n,pnatded 30435
[Clemente] p. 12Definition I` `n(1)natded 30435
[Clemente] p. 12Definition I` `n(2)natded 30435
[Clemente] p. 13Definition I` `m,n,pnatded 30435
[Clemente] p. 14Proof 5.11natded 30435
[Clemente] p. 14Definition E` `nnatded 30435
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30437  ex-natded5.2 30436
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30440  ex-natded5.3 30439
[Clemente] p. 18Theorem 5.5ex-natded5.5 30442
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30444  ex-natded5.7 30443
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30446  ex-natded5.8 30445
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30448  ex-natded5.13 30447
[Clemente] p. 32Definition I` `nnatded 30435
[Clemente] p. 32Definition E` `m,n,p,anatded 30435
[Clemente] p. 32Definition E` `n,tnatded 30435
[Clemente] p. 32Definition I` `n,tnatded 30435
[Clemente] p. 43Theorem 9.20ex-natded9.20 30449
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30450
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30452  ex-natded9.26 30451
[Cohen] p. 301Remarkrelogoprlem 26651
[Cohen] p. 301Property 2relogmul 26652  relogmuld 26685
[Cohen] p. 301Property 3relogdiv 26653  relogdivd 26686
[Cohen] p. 301Property 4relogexp 26656
[Cohen] p. 301Property 1alog1 26645
[Cohen] p. 301Property 1bloge 26646
[Cohen4] p. 348Observationrelogbcxpb 26848
[Cohen4] p. 349Propertyrelogbf 26852
[Cohen4] p. 352Definitionelogb 26831
[Cohen4] p. 361Property 2relogbmul 26838
[Cohen4] p. 361Property 3logbrec 26843  relogbdiv 26840
[Cohen4] p. 361Property 4relogbreexp 26836
[Cohen4] p. 361Property 6relogbexp 26841
[Cohen4] p. 361Property 1(a)logbid1 26829
[Cohen4] p. 361Property 1(b)logb1 26830
[Cohen4] p. 367Propertylogbchbase 26832
[Cohen4] p. 377Property 2logblt 26845
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34250  sxbrsigalem4 34252
[Cohn] p. 81Section II.5acsdomd 18627  acsinfd 18626  acsinfdimd 18628  acsmap2d 18625  acsmapd 18624
[Cohn] p. 143Example 5.1.1sxbrsiga 34255
[Connell] p. 57Definitiondf-scmat 22518  df-scmatalt 48128
[Conway] p. 4Definitionslerec 27882
[Conway] p. 5Definitionaddsval 28013  addsval2 28014  df-adds 28011  df-muls 28151  df-negs 28071
[Conway] p. 7Theorem0slt1s 27892
[Conway] p. 16Theorem 0(i)ssltright 27928
[Conway] p. 16Theorem 0(ii)ssltleft 27927
[Conway] p. 16Theorem 0(iii)slerflex 27826
[Conway] p. 17Theorem 3addsass 28056  addsassd 28057  addscom 28017  addscomd 28018  addsrid 28015  addsridd 28016
[Conway] p. 17Definitiondf-0s 27887
[Conway] p. 17Theorem 4(ii)negnegs 28094
[Conway] p. 17Theorem 4(iii)negsid 28091  negsidd 28092
[Conway] p. 18Theorem 5sleadd1 28040  sleadd1d 28046
[Conway] p. 18Definitiondf-1s 27888
[Conway] p. 18Theorem 6(ii)negscl 28086  negscld 28087
[Conway] p. 18Theorem 6(iii)addscld 28031
[Conway] p. 19Notemulsunif2 28214
[Conway] p. 19Theorem 7addsdi 28199  addsdid 28200  addsdird 28201  mulnegs1d 28204  mulnegs2d 28205  mulsass 28210  mulsassd 28211  mulscom 28183  mulscomd 28184
[Conway] p. 19Theorem 8(i)mulscl 28178  mulscld 28179
[Conway] p. 19Theorem 8(iii)slemuld 28182  sltmul 28180  sltmuld 28181
[Conway] p. 20Theorem 9mulsgt0 28188  mulsgt0d 28189
[Conway] p. 21Theorem 10(iv)precsex 28260
[Conway] p. 24Definitiondf-reno 28444
[Conway] p. 24Theorem 13(ii)readdscl 28449  remulscl 28452  renegscl 28448
[Conway] p. 27Definitiondf-ons 28293  elons2 28299
[Conway] p. 27Theorem 14sltonex 28302
[Conway] p. 29Remarkmadebday 27956  newbday 27958  oldbday 27957
[Conway] p. 29Definitiondf-made 27904  df-new 27906  df-old 27905
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13912
[Crawley] p. 1Definition of posetdf-poset 18383
[Crawley] p. 107Theorem 13.2hlsupr 39343
[Crawley] p. 110Theorem 13.3arglem1N 40147  dalaw 39843
[Crawley] p. 111Theorem 13.4hlathil 41922
[Crawley] p. 111Definition of set Wdf-watsN 39947
[Crawley] p. 111Definition of dilationdf-dilN 40063  df-ldil 40061  isldil 40067
[Crawley] p. 111Definition of translationdf-ltrn 40062  df-trnN 40064  isltrn 40076  ltrnu 40078
[Crawley] p. 112Lemma Acdlema1N 39748  cdlema2N 39749  exatleN 39361
[Crawley] p. 112Lemma B1cvrat 39433  cdlemb 39751  cdlemb2 39998  cdlemb3 40563  idltrn 40107  l1cvat 39011  lhpat 40000  lhpat2 40002  lshpat 39012  ltrnel 40096  ltrnmw 40108
[Crawley] p. 112Lemma Ccdlemc1 40148  cdlemc2 40149  ltrnnidn 40131  trlat 40126  trljat1 40123  trljat2 40124  trljat3 40125  trlne 40142  trlnidat 40130  trlnle 40143
[Crawley] p. 112Definition of automorphismdf-pautN 39948
[Crawley] p. 113Lemma Ccdlemc 40154  cdlemc3 40150  cdlemc4 40151
[Crawley] p. 113Lemma Dcdlemd 40164  cdlemd1 40155  cdlemd2 40156  cdlemd3 40157  cdlemd4 40158  cdlemd5 40159  cdlemd6 40160  cdlemd7 40161  cdlemd8 40162  cdlemd9 40163  cdleme31sde 40342  cdleme31se 40339  cdleme31se2 40340  cdleme31snd 40343  cdleme32a 40398  cdleme32b 40399  cdleme32c 40400  cdleme32d 40401  cdleme32e 40402  cdleme32f 40403  cdleme32fva 40394  cdleme32fva1 40395  cdleme32fvcl 40397  cdleme32le 40404  cdleme48fv 40456  cdleme4gfv 40464  cdleme50eq 40498  cdleme50f 40499  cdleme50f1 40500  cdleme50f1o 40503  cdleme50laut 40504  cdleme50ldil 40505  cdleme50lebi 40497  cdleme50rn 40502  cdleme50rnlem 40501  cdlemeg49le 40468  cdlemeg49lebilem 40496
[Crawley] p. 113Lemma Ecdleme 40517  cdleme00a 40166  cdleme01N 40178  cdleme02N 40179  cdleme0a 40168  cdleme0aa 40167  cdleme0b 40169  cdleme0c 40170  cdleme0cp 40171  cdleme0cq 40172  cdleme0dN 40173  cdleme0e 40174  cdleme0ex1N 40180  cdleme0ex2N 40181  cdleme0fN 40175  cdleme0gN 40176  cdleme0moN 40182  cdleme1 40184  cdleme10 40211  cdleme10tN 40215  cdleme11 40227  cdleme11a 40217  cdleme11c 40218  cdleme11dN 40219  cdleme11e 40220  cdleme11fN 40221  cdleme11g 40222  cdleme11h 40223  cdleme11j 40224  cdleme11k 40225  cdleme11l 40226  cdleme12 40228  cdleme13 40229  cdleme14 40230  cdleme15 40235  cdleme15a 40231  cdleme15b 40232  cdleme15c 40233  cdleme15d 40234  cdleme16 40242  cdleme16aN 40216  cdleme16b 40236  cdleme16c 40237  cdleme16d 40238  cdleme16e 40239  cdleme16f 40240  cdleme16g 40241  cdleme19a 40260  cdleme19b 40261  cdleme19c 40262  cdleme19d 40263  cdleme19e 40264  cdleme19f 40265  cdleme1b 40183  cdleme2 40185  cdleme20aN 40266  cdleme20bN 40267  cdleme20c 40268  cdleme20d 40269  cdleme20e 40270  cdleme20f 40271  cdleme20g 40272  cdleme20h 40273  cdleme20i 40274  cdleme20j 40275  cdleme20k 40276  cdleme20l 40279  cdleme20l1 40277  cdleme20l2 40278  cdleme20m 40280  cdleme20y 40259  cdleme20zN 40258  cdleme21 40294  cdleme21d 40287  cdleme21e 40288  cdleme22a 40297  cdleme22aa 40296  cdleme22b 40298  cdleme22cN 40299  cdleme22d 40300  cdleme22e 40301  cdleme22eALTN 40302  cdleme22f 40303  cdleme22f2 40304  cdleme22g 40305  cdleme23a 40306  cdleme23b 40307  cdleme23c 40308  cdleme26e 40316  cdleme26eALTN 40318  cdleme26ee 40317  cdleme26f 40320  cdleme26f2 40322  cdleme26f2ALTN 40321  cdleme26fALTN 40319  cdleme27N 40326  cdleme27a 40324  cdleme27cl 40323  cdleme28c 40329  cdleme3 40194  cdleme30a 40335  cdleme31fv 40347  cdleme31fv1 40348  cdleme31fv1s 40349  cdleme31fv2 40350  cdleme31id 40351  cdleme31sc 40341  cdleme31sdnN 40344  cdleme31sn 40337  cdleme31sn1 40338  cdleme31sn1c 40345  cdleme31sn2 40346  cdleme31so 40336  cdleme35a 40405  cdleme35b 40407  cdleme35c 40408  cdleme35d 40409  cdleme35e 40410  cdleme35f 40411  cdleme35fnpq 40406  cdleme35g 40412  cdleme35h 40413  cdleme35h2 40414  cdleme35sn2aw 40415  cdleme35sn3a 40416  cdleme36a 40417  cdleme36m 40418  cdleme37m 40419  cdleme38m 40420  cdleme38n 40421  cdleme39a 40422  cdleme39n 40423  cdleme3b 40186  cdleme3c 40187  cdleme3d 40188  cdleme3e 40189  cdleme3fN 40190  cdleme3fa 40193  cdleme3g 40191  cdleme3h 40192  cdleme4 40195  cdleme40m 40424  cdleme40n 40425  cdleme40v 40426  cdleme40w 40427  cdleme41fva11 40434  cdleme41sn3aw 40431  cdleme41sn4aw 40432  cdleme41snaw 40433  cdleme42a 40428  cdleme42b 40435  cdleme42c 40429  cdleme42d 40430  cdleme42e 40436  cdleme42f 40437  cdleme42g 40438  cdleme42h 40439  cdleme42i 40440  cdleme42k 40441  cdleme42ke 40442  cdleme42keg 40443  cdleme42mN 40444  cdleme42mgN 40445  cdleme43aN 40446  cdleme43bN 40447  cdleme43cN 40448  cdleme43dN 40449  cdleme5 40197  cdleme50ex 40516  cdleme50ltrn 40514  cdleme51finvN 40513  cdleme51finvfvN 40512  cdleme51finvtrN 40515  cdleme6 40198  cdleme7 40206  cdleme7a 40200  cdleme7aa 40199  cdleme7b 40201  cdleme7c 40202  cdleme7d 40203  cdleme7e 40204  cdleme7ga 40205  cdleme8 40207  cdleme8tN 40212  cdleme9 40210  cdleme9a 40208  cdleme9b 40209  cdleme9tN 40214  cdleme9taN 40213  cdlemeda 40255  cdlemedb 40254  cdlemednpq 40256  cdlemednuN 40257  cdlemefr27cl 40360  cdlemefr32fva1 40367  cdlemefr32fvaN 40366  cdlemefrs32fva 40357  cdlemefrs32fva1 40358  cdlemefs27cl 40370  cdlemefs32fva1 40380  cdlemefs32fvaN 40379  cdlemesner 40253  cdlemeulpq 40177
[Crawley] p. 114Lemma E4atex 40033  4atexlem7 40032  cdleme0nex 40247  cdleme17a 40243  cdleme17c 40245  cdleme17d 40455  cdleme17d1 40246  cdleme17d2 40452  cdleme18a 40248  cdleme18b 40249  cdleme18c 40250  cdleme18d 40252  cdleme4a 40196
[Crawley] p. 115Lemma Ecdleme21a 40282  cdleme21at 40285  cdleme21b 40283  cdleme21c 40284  cdleme21ct 40286  cdleme21f 40289  cdleme21g 40290  cdleme21h 40291  cdleme21i 40292  cdleme22gb 40251
[Crawley] p. 116Lemma Fcdlemf 40520  cdlemf1 40518  cdlemf2 40519
[Crawley] p. 116Lemma Gcdlemftr1 40524  cdlemg16 40614  cdlemg28 40661  cdlemg28a 40650  cdlemg28b 40660  cdlemg3a 40554  cdlemg42 40686  cdlemg43 40687  cdlemg44 40690  cdlemg44a 40688  cdlemg46 40692  cdlemg47 40693  cdlemg9 40591  ltrnco 40676  ltrncom 40695  tgrpabl 40708  trlco 40684
[Crawley] p. 116Definition of Gdf-tgrp 40700
[Crawley] p. 117Lemma Gcdlemg17 40634  cdlemg17b 40619
[Crawley] p. 117Definition of Edf-edring-rN 40713  df-edring 40714
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40717
[Crawley] p. 118Remarktendopltp 40737
[Crawley] p. 118Lemma Hcdlemh 40774  cdlemh1 40772  cdlemh2 40773
[Crawley] p. 118Lemma Icdlemi 40777  cdlemi1 40775  cdlemi2 40776
[Crawley] p. 118Lemma Jcdlemj1 40778  cdlemj2 40779  cdlemj3 40780  tendocan 40781
[Crawley] p. 118Lemma Kcdlemk 40931  cdlemk1 40788  cdlemk10 40800  cdlemk11 40806  cdlemk11t 40903  cdlemk11ta 40886  cdlemk11tb 40888  cdlemk11tc 40902  cdlemk11u-2N 40846  cdlemk11u 40828  cdlemk12 40807  cdlemk12u-2N 40847  cdlemk12u 40829  cdlemk13-2N 40833  cdlemk13 40809  cdlemk14-2N 40835  cdlemk14 40811  cdlemk15-2N 40836  cdlemk15 40812  cdlemk16-2N 40837  cdlemk16 40814  cdlemk16a 40813  cdlemk17-2N 40838  cdlemk17 40815  cdlemk18-2N 40843  cdlemk18-3N 40857  cdlemk18 40825  cdlemk19-2N 40844  cdlemk19 40826  cdlemk19u 40927  cdlemk1u 40816  cdlemk2 40789  cdlemk20-2N 40849  cdlemk20 40831  cdlemk21-2N 40848  cdlemk21N 40830  cdlemk22-3 40858  cdlemk22 40850  cdlemk23-3 40859  cdlemk24-3 40860  cdlemk25-3 40861  cdlemk26-3 40863  cdlemk26b-3 40862  cdlemk27-3 40864  cdlemk28-3 40865  cdlemk29-3 40868  cdlemk3 40790  cdlemk30 40851  cdlemk31 40853  cdlemk32 40854  cdlemk33N 40866  cdlemk34 40867  cdlemk35 40869  cdlemk36 40870  cdlemk37 40871  cdlemk38 40872  cdlemk39 40873  cdlemk39u 40925  cdlemk4 40791  cdlemk41 40877  cdlemk42 40898  cdlemk42yN 40901  cdlemk43N 40920  cdlemk45 40904  cdlemk46 40905  cdlemk47 40906  cdlemk48 40907  cdlemk49 40908  cdlemk5 40793  cdlemk50 40909  cdlemk51 40910  cdlemk52 40911  cdlemk53 40914  cdlemk54 40915  cdlemk55 40918  cdlemk55u 40923  cdlemk56 40928  cdlemk5a 40792  cdlemk5auN 40817  cdlemk5u 40818  cdlemk6 40794  cdlemk6u 40819  cdlemk7 40805  cdlemk7u-2N 40845  cdlemk7u 40827  cdlemk8 40795  cdlemk9 40796  cdlemk9bN 40797  cdlemki 40798  cdlemkid 40893  cdlemkj-2N 40839  cdlemkj 40820  cdlemksat 40803  cdlemksel 40802  cdlemksv 40801  cdlemksv2 40804  cdlemkuat 40823  cdlemkuel-2N 40841  cdlemkuel-3 40855  cdlemkuel 40822  cdlemkuv-2N 40840  cdlemkuv2-2 40842  cdlemkuv2-3N 40856  cdlemkuv2 40824  cdlemkuvN 40821  cdlemkvcl 40799  cdlemky 40883  cdlemkyyN 40919  tendoex 40932
[Crawley] p. 120Remarkdva1dim 40942
[Crawley] p. 120Lemma Lcdleml1N 40933  cdleml2N 40934  cdleml3N 40935  cdleml4N 40936  cdleml5N 40937  cdleml6 40938  cdleml7 40939  cdleml8 40940  cdleml9 40941  dia1dim 41018
[Crawley] p. 120Lemma Mdia11N 41005  diaf11N 41006  dialss 41003  diaord 41004  dibf11N 41118  djajN 41094
[Crawley] p. 120Definition of isomorphism mapdiaval 40989
[Crawley] p. 121Lemma Mcdlemm10N 41075  dia2dimlem1 41021  dia2dimlem2 41022  dia2dimlem3 41023  dia2dimlem4 41024  dia2dimlem5 41025  diaf1oN 41087  diarnN 41086  dvheveccl 41069  dvhopN 41073
[Crawley] p. 121Lemma Ncdlemn 41169  cdlemn10 41163  cdlemn11 41168  cdlemn11a 41164  cdlemn11b 41165  cdlemn11c 41166  cdlemn11pre 41167  cdlemn2 41152  cdlemn2a 41153  cdlemn3 41154  cdlemn4 41155  cdlemn4a 41156  cdlemn5 41158  cdlemn5pre 41157  cdlemn6 41159  cdlemn7 41160  cdlemn8 41161  cdlemn9 41162  diclspsn 41151
[Crawley] p. 121Definition of phi(q)df-dic 41130
[Crawley] p. 122Lemma Ndih11 41222  dihf11 41224  dihjust 41174  dihjustlem 41173  dihord 41221  dihord1 41175  dihord10 41180  dihord11b 41179  dihord11c 41181  dihord2 41184  dihord2a 41176  dihord2b 41177  dihord2cN 41178  dihord2pre 41182  dihord2pre2 41183  dihordlem6 41170  dihordlem7 41171  dihordlem7b 41172
[Crawley] p. 122Definition of isomorphism mapdihffval 41187  dihfval 41188  dihval 41189
[Diestel] p. 3Definitiondf-gric 47751  df-grim 47748  isuspgrim 47759
[Diestel] p. 3Section 1.1df-cusgr 29447  df-nbgr 29368
[Diestel] p. 3Definition by df-grisom 47747
[Diestel] p. 4Section 1.1df-isubgr 47733  df-subgr 29303  uhgrspan1 29338  uhgrspansubgr 29326
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29590  vtxdgoddnumeven 29589
[Diestel] p. 27Section 1.10df-ushgr 29094
[EGA] p. 80Notation 1.1.1rspecval 33810
[EGA] p. 80Proposition 1.1.2zartop 33822
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33814  zarcls1 33815
[EGA] p. 81Corollary 1.1.8zart0 33825
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33828
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33831
[Eisenberg] p. 67Definition 5.3df-dif 3979
[Eisenberg] p. 82Definition 6.3dfom3 9716
[Eisenberg] p. 125Definition 8.21df-map 8886
[Eisenberg] p. 216Example 13.2(4)omenps 9724
[Eisenberg] p. 310Theorem 19.8cardprc 10049
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10624
[Enderton] p. 18Axiom of Empty Setaxnul 5323
[Enderton] p. 19Definitiondf-tp 4653
[Enderton] p. 26Exercise 5unissb 4963
[Enderton] p. 26Exercise 10pwel 5399
[Enderton] p. 28Exercise 7(b)pwun 5591
[Enderton] p. 30Theorem "Distributive laws"iinin1 5102  iinin2 5101  iinun2 5096  iunin1 5095  iunin1f 32580  iunin2 5094  uniin1 32574  uniin2 32575
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5100  iundif2 5097
[Enderton] p. 32Exercise 20unineq 4307
[Enderton] p. 33Exercise 23iinuni 5121
[Enderton] p. 33Exercise 25iununi 5122
[Enderton] p. 33Exercise 24(a)iinpw 5129
[Enderton] p. 33Exercise 24(b)iunpw 7806  iunpwss 5130
[Enderton] p. 36Definitionopthwiener 5533
[Enderton] p. 38Exercise 6(a)unipw 5470
[Enderton] p. 38Exercise 6(b)pwuni 4969
[Enderton] p. 41Lemma 3Dopeluu 5490  rnex 7950  rnexg 7942
[Enderton] p. 41Exercise 8dmuni 5939  rnuni 6180
[Enderton] p. 42Definition of a functiondffun7 6605  dffun8 6606
[Enderton] p. 43Definition of function valuefunfv2 7010
[Enderton] p. 43Definition of single-rootedfuncnv 6647
[Enderton] p. 44Definition (d)dfima2 6091  dfima3 6092
[Enderton] p. 47Theorem 3Hfvco2 7019
[Enderton] p. 49Axiom of Choice (first form)ac7 10542  ac7g 10543  df-ac 10185  dfac2 10201  dfac2a 10199  dfac2b 10200  dfac3 10190  dfac7 10202
[Enderton] p. 50Theorem 3K(a)imauni 7283
[Enderton] p. 52Definitiondf-map 8886
[Enderton] p. 53Exercise 21coass 6296
[Enderton] p. 53Exercise 27dmco 6285
[Enderton] p. 53Exercise 14(a)funin 6654
[Enderton] p. 53Exercise 22(a)imass2 6132
[Enderton] p. 54Remarkixpf 8978  ixpssmap 8990
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8956
[Enderton] p. 55Axiom of Choice (second form)ac9 10552  ac9s 10562
[Enderton] p. 56Theorem 3Meqvrelref 38566  erref 8783
[Enderton] p. 57Lemma 3Neqvrelthi 38569  erthi 8816
[Enderton] p. 57Definitiondf-ec 8765
[Enderton] p. 58Definitiondf-qs 8769
[Enderton] p. 61Exercise 35df-ec 8765
[Enderton] p. 65Exercise 56(a)dmun 5935
[Enderton] p. 68Definition of successordf-suc 6401
[Enderton] p. 71Definitiondf-tr 5284  dftr4 5290
[Enderton] p. 72Theorem 4Eunisuc 6474  unisucg 6473
[Enderton] p. 73Exercise 6unisuc 6474  unisucg 6473
[Enderton] p. 73Exercise 5(a)truni 5299
[Enderton] p. 73Exercise 5(b)trint 5301  trintALT 44852
[Enderton] p. 79Theorem 4I(A1)nna0 8660
[Enderton] p. 79Theorem 4I(A2)nnasuc 8662  onasuc 8584
[Enderton] p. 79Definition of operation valuedf-ov 7451
[Enderton] p. 80Theorem 4J(A1)nnm0 8661
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8663  onmsuc 8585
[Enderton] p. 81Theorem 4K(1)nnaass 8678
[Enderton] p. 81Theorem 4K(2)nna0r 8665  nnacom 8673
[Enderton] p. 81Theorem 4K(3)nndi 8679
[Enderton] p. 81Theorem 4K(4)nnmass 8680
[Enderton] p. 81Theorem 4K(5)nnmcom 8682
[Enderton] p. 82Exercise 16nnm0r 8666  nnmsucr 8681
[Enderton] p. 88Exercise 23nnaordex 8694
[Enderton] p. 129Definitiondf-en 9004
[Enderton] p. 132Theorem 6B(b)canth 7401
[Enderton] p. 133Exercise 1xpomen 10084
[Enderton] p. 133Exercise 2qnnen 16261
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9273
[Enderton] p. 135Corollary 6Cphp3 9275
[Enderton] p. 136Corollary 6Enneneq 9272
[Enderton] p. 136Corollary 6D(a)pssinf 9319
[Enderton] p. 136Corollary 6D(b)ominf 9321
[Enderton] p. 137Lemma 6Fpssnn 9234
[Enderton] p. 138Corollary 6Gssfi 9240
[Enderton] p. 139Theorem 6H(c)mapen 9207
[Enderton] p. 142Theorem 6I(3)xpdjuen 10249
[Enderton] p. 142Theorem 6I(4)mapdjuen 10250
[Enderton] p. 143Theorem 6Jdju0en 10245  dju1en 10241
[Enderton] p. 144Exercise 13iunfi 9411  unifi 9412  unifi2 9413
[Enderton] p. 144Corollary 6Kundif2 4500  unfi 9238  unfi2 9376
[Enderton] p. 145Figure 38ffoss 7986
[Enderton] p. 145Definitiondf-dom 9005
[Enderton] p. 146Example 1domen 9021  domeng 9022
[Enderton] p. 146Example 3nndomo 9296  nnsdom 9723  nnsdomg 9363
[Enderton] p. 149Theorem 6L(a)djudom2 10253
[Enderton] p. 149Theorem 6L(c)mapdom1 9208  xpdom1 9137  xpdom1g 9135  xpdom2g 9134
[Enderton] p. 149Theorem 6L(d)mapdom2 9214
[Enderton] p. 151Theorem 6Mzorn 10576  zorng 10573
[Enderton] p. 151Theorem 6M(4)ac8 10561  dfac5 10198
[Enderton] p. 159Theorem 6Qunictb 10644
[Enderton] p. 164Exampleinfdif 10277
[Enderton] p. 168Definitiondf-po 5607
[Enderton] p. 192Theorem 7M(a)oneli 6509
[Enderton] p. 192Theorem 7M(b)ontr1 6441
[Enderton] p. 192Theorem 7M(c)onirri 6508
[Enderton] p. 193Corollary 7N(b)0elon 6449
[Enderton] p. 193Corollary 7N(c)onsuci 7875
[Enderton] p. 193Corollary 7N(d)ssonunii 7816
[Enderton] p. 194Remarkonprc 7813
[Enderton] p. 194Exercise 16suc11 6502
[Enderton] p. 197Definitiondf-card 10008
[Enderton] p. 197Theorem 7Pcarden 10620
[Enderton] p. 200Exercise 25tfis 7892
[Enderton] p. 202Lemma 7Tr1tr 9845
[Enderton] p. 202Definitiondf-r1 9833
[Enderton] p. 202Theorem 7Qr1val1 9855
[Enderton] p. 204Theorem 7V(b)rankval4 9936
[Enderton] p. 206Theorem 7X(b)en2lp 9675
[Enderton] p. 207Exercise 30rankpr 9926  rankprb 9920  rankpw 9912  rankpwi 9892  rankuniss 9935
[Enderton] p. 207Exercise 34opthreg 9687
[Enderton] p. 208Exercise 35suc11reg 9688
[Enderton] p. 212Definition of alephalephval3 10179
[Enderton] p. 213Theorem 8A(a)alephord2 10145
[Enderton] p. 213Theorem 8A(b)cardalephex 10159
[Enderton] p. 218Theorem Schema 8Eonfununi 8397
[Enderton] p. 222Definition of kardkarden 9964  kardex 9963
[Enderton] p. 238Theorem 8Roeoa 8653
[Enderton] p. 238Theorem 8Soeoe 8655
[Enderton] p. 240Exercise 25oarec 8618
[Enderton] p. 257Definition of cofinalitycflm 10319
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17700
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17646
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18623  mrieqv2d 17697  mrieqvd 17696
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17701
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17706  mreexexlem2d 17703
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18629  mreexfidimd 17708
[Frege1879] p. 11Statementdf3or2 43730
[Frege1879] p. 12Statementdf3an2 43731  dfxor4 43728  dfxor5 43729
[Frege1879] p. 26Axiom 1ax-frege1 43752
[Frege1879] p. 26Axiom 2ax-frege2 43753
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43757
[Frege1879] p. 31Proposition 4frege4 43761
[Frege1879] p. 32Proposition 5frege5 43762
[Frege1879] p. 33Proposition 6frege6 43768
[Frege1879] p. 34Proposition 7frege7 43770
[Frege1879] p. 35Axiom 8ax-frege8 43771  axfrege8 43769
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37411
[Frege1879] p. 35Proposition 9frege9 43774
[Frege1879] p. 36Proposition 10frege10 43782
[Frege1879] p. 36Proposition 11frege11 43776
[Frege1879] p. 37Proposition 12frege12 43775
[Frege1879] p. 37Proposition 13frege13 43784
[Frege1879] p. 37Proposition 14frege14 43785
[Frege1879] p. 38Proposition 15frege15 43788
[Frege1879] p. 38Proposition 16frege16 43778
[Frege1879] p. 39Proposition 17frege17 43783
[Frege1879] p. 39Proposition 18frege18 43780
[Frege1879] p. 39Proposition 19frege19 43786
[Frege1879] p. 40Proposition 20frege20 43790
[Frege1879] p. 40Proposition 21frege21 43789
[Frege1879] p. 41Proposition 22frege22 43781
[Frege1879] p. 42Proposition 23frege23 43787
[Frege1879] p. 42Proposition 24frege24 43777
[Frege1879] p. 42Proposition 25frege25 43779  rp-frege25 43767
[Frege1879] p. 42Proposition 26frege26 43772
[Frege1879] p. 43Axiom 28ax-frege28 43792
[Frege1879] p. 43Proposition 27frege27 43773
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43793
[Frege1879] p. 44Axiom 31ax-frege31 43796  axfrege31 43795
[Frege1879] p. 44Proposition 30frege30 43794
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43797
[Frege1879] p. 44Proposition 33frege33 43798
[Frege1879] p. 45Proposition 34frege34 43799
[Frege1879] p. 45Proposition 35frege35 43800
[Frege1879] p. 45Proposition 36frege36 43801
[Frege1879] p. 46Proposition 37frege37 43802
[Frege1879] p. 46Proposition 38frege38 43803
[Frege1879] p. 46Proposition 39frege39 43804
[Frege1879] p. 46Proposition 40frege40 43805
[Frege1879] p. 47Axiom 41ax-frege41 43807  axfrege41 43806
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43808
[Frege1879] p. 47Proposition 43frege43 43809
[Frege1879] p. 47Proposition 44frege44 43810
[Frege1879] p. 47Proposition 45frege45 43811
[Frege1879] p. 48Proposition 46frege46 43812
[Frege1879] p. 48Proposition 47frege47 43813
[Frege1879] p. 49Proposition 48frege48 43814
[Frege1879] p. 49Proposition 49frege49 43815
[Frege1879] p. 49Proposition 50frege50 43816
[Frege1879] p. 50Axiom 52ax-frege52a 43819  ax-frege52c 43850  frege52aid 43820  frege52b 43851
[Frege1879] p. 50Axiom 54ax-frege54a 43824  ax-frege54c 43854  frege54b 43855
[Frege1879] p. 50Proposition 51frege51 43817
[Frege1879] p. 50Proposition 52dfsbcq 3806
[Frege1879] p. 50Proposition 53frege53a 43822  frege53aid 43821  frege53b 43852  frege53c 43876
[Frege1879] p. 50Proposition 54biid 261  eqid 2740
[Frege1879] p. 50Proposition 55frege55a 43830  frege55aid 43827  frege55b 43859  frege55c 43880  frege55cor1a 43831  frege55lem2a 43829  frege55lem2b 43858  frege55lem2c 43879
[Frege1879] p. 50Proposition 56frege56a 43833  frege56aid 43832  frege56b 43860  frege56c 43881
[Frege1879] p. 51Axiom 58ax-frege58a 43837  ax-frege58b 43863  frege58bid 43864  frege58c 43883
[Frege1879] p. 51Proposition 57frege57a 43835  frege57aid 43834  frege57b 43861  frege57c 43882
[Frege1879] p. 51Proposition 58spsbc 3817
[Frege1879] p. 51Proposition 59frege59a 43839  frege59b 43866  frege59c 43884
[Frege1879] p. 52Proposition 60frege60a 43840  frege60b 43867  frege60c 43885
[Frege1879] p. 52Proposition 61frege61a 43841  frege61b 43868  frege61c 43886
[Frege1879] p. 52Proposition 62frege62a 43842  frege62b 43869  frege62c 43887
[Frege1879] p. 52Proposition 63frege63a 43843  frege63b 43870  frege63c 43888
[Frege1879] p. 53Proposition 64frege64a 43844  frege64b 43871  frege64c 43889
[Frege1879] p. 53Proposition 65frege65a 43845  frege65b 43872  frege65c 43890
[Frege1879] p. 54Proposition 66frege66a 43846  frege66b 43873  frege66c 43891
[Frege1879] p. 54Proposition 67frege67a 43847  frege67b 43874  frege67c 43892
[Frege1879] p. 54Proposition 68frege68a 43848  frege68b 43875  frege68c 43893
[Frege1879] p. 55Definition 69dffrege69 43894
[Frege1879] p. 58Proposition 70frege70 43895
[Frege1879] p. 59Proposition 71frege71 43896
[Frege1879] p. 59Proposition 72frege72 43897
[Frege1879] p. 59Proposition 73frege73 43898
[Frege1879] p. 60Definition 76dffrege76 43901
[Frege1879] p. 60Proposition 74frege74 43899
[Frege1879] p. 60Proposition 75frege75 43900
[Frege1879] p. 62Proposition 77frege77 43902  frege77d 43708
[Frege1879] p. 63Proposition 78frege78 43903
[Frege1879] p. 63Proposition 79frege79 43904
[Frege1879] p. 63Proposition 80frege80 43905
[Frege1879] p. 63Proposition 81frege81 43906  frege81d 43709
[Frege1879] p. 64Proposition 82frege82 43907
[Frege1879] p. 65Proposition 83frege83 43908  frege83d 43710
[Frege1879] p. 65Proposition 84frege84 43909
[Frege1879] p. 66Proposition 85frege85 43910
[Frege1879] p. 66Proposition 86frege86 43911
[Frege1879] p. 66Proposition 87frege87 43912  frege87d 43712
[Frege1879] p. 67Proposition 88frege88 43913
[Frege1879] p. 68Proposition 89frege89 43914
[Frege1879] p. 68Proposition 90frege90 43915
[Frege1879] p. 68Proposition 91frege91 43916  frege91d 43713
[Frege1879] p. 69Proposition 92frege92 43917
[Frege1879] p. 70Proposition 93frege93 43918
[Frege1879] p. 70Proposition 94frege94 43919
[Frege1879] p. 70Proposition 95frege95 43920
[Frege1879] p. 71Definition 99dffrege99 43924
[Frege1879] p. 71Proposition 96frege96 43921  frege96d 43711
[Frege1879] p. 71Proposition 97frege97 43922  frege97d 43714
[Frege1879] p. 71Proposition 98frege98 43923  frege98d 43715
[Frege1879] p. 72Proposition 100frege100 43925
[Frege1879] p. 72Proposition 101frege101 43926
[Frege1879] p. 72Proposition 102frege102 43927  frege102d 43716
[Frege1879] p. 73Proposition 103frege103 43928
[Frege1879] p. 73Proposition 104frege104 43929
[Frege1879] p. 73Proposition 105frege105 43930
[Frege1879] p. 73Proposition 106frege106 43931  frege106d 43717
[Frege1879] p. 74Proposition 107frege107 43932
[Frege1879] p. 74Proposition 108frege108 43933  frege108d 43718
[Frege1879] p. 74Proposition 109frege109 43934  frege109d 43719
[Frege1879] p. 75Proposition 110frege110 43935
[Frege1879] p. 75Proposition 111frege111 43936  frege111d 43721
[Frege1879] p. 76Proposition 112frege112 43937
[Frege1879] p. 76Proposition 113frege113 43938
[Frege1879] p. 76Proposition 114frege114 43939  frege114d 43720
[Frege1879] p. 77Definition 115dffrege115 43940
[Frege1879] p. 77Proposition 116frege116 43941
[Frege1879] p. 78Proposition 117frege117 43942
[Frege1879] p. 78Proposition 118frege118 43943
[Frege1879] p. 78Proposition 119frege119 43944
[Frege1879] p. 78Proposition 120frege120 43945
[Frege1879] p. 79Proposition 121frege121 43946
[Frege1879] p. 79Proposition 122frege122 43947  frege122d 43722
[Frege1879] p. 79Proposition 123frege123 43948
[Frege1879] p. 80Proposition 124frege124 43949  frege124d 43723
[Frege1879] p. 81Proposition 125frege125 43950
[Frege1879] p. 81Proposition 126frege126 43951  frege126d 43724
[Frege1879] p. 82Proposition 127frege127 43952
[Frege1879] p. 83Proposition 128frege128 43953
[Frege1879] p. 83Proposition 129frege129 43954  frege129d 43725
[Frege1879] p. 84Proposition 130frege130 43955
[Frege1879] p. 85Proposition 131frege131 43956  frege131d 43726
[Frege1879] p. 86Proposition 132frege132 43957
[Frege1879] p. 86Proposition 133frege133 43958  frege133d 43727
[Fremlin1] p. 13Definition 111G (b)df-salgen 46234
[Fremlin1] p. 13Definition 111G (d)borelmbl 46557
[Fremlin1] p. 13Proposition 111G (b)salgenss 46257
[Fremlin1] p. 14Definition 112Aismea 46372
[Fremlin1] p. 15Remark 112B (d)psmeasure 46392
[Fremlin1] p. 15Property 112C (a)meadjun 46383  meadjunre 46397
[Fremlin1] p. 15Property 112C (b)meassle 46384
[Fremlin1] p. 15Property 112C (c)meaunle 46385
[Fremlin1] p. 16Property 112C (d)iundjiun 46381  meaiunle 46390  meaiunlelem 46389
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46402  meaiuninc2 46403  meaiuninc3 46406  meaiuninc3v 46405  meaiunincf 46404  meaiuninclem 46401
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46408  meaiininc2 46409  meaiininclem 46407
[Fremlin1] p. 19Theorem 113Ccaragen0 46427  caragendifcl 46435  caratheodory 46449  omelesplit 46439
[Fremlin1] p. 19Definition 113Aisome 46415  isomennd 46452  isomenndlem 46451
[Fremlin1] p. 19Remark 113B (c)omeunle 46437
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46456  voncmpl 46542
[Fremlin1] p. 19Definition 113A (ii)omessle 46419
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46444  carageniuncllem1 46442  carageniuncllem2 46443  caragenuncl 46434  caragenuncllem 46433  caragenunicl 46445
[Fremlin1] p. 21Remark 113Dcaragenel2d 46453
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46447  caratheodorylem2 46448
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46456
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46515  hoidmv1lelem1 46512  hoidmv1lelem2 46513  hoidmv1lelem3 46514
[Fremlin1] p. 25Definition 114Eisvonmbl 46559
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46515  hoidmvle 46521  hoidmvlelem1 46516  hoidmvlelem2 46517  hoidmvlelem3 46518  hoidmvlelem4 46519  hoidmvlelem5 46520  hsphoidmvle2 46506  hsphoif 46497  hsphoival 46500
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46469
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46477
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46504  hoidmvn0val 46505  hoidmvval 46498  hoidmvval0 46508  hoidmvval0b 46511
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46509  hsphoidmvle 46507
[Fremlin1] p. 30Definition 115Cdf-ovoln 46458  df-voln 46460
[Fremlin1] p. 30Proposition 115D (a)dmovn 46525  ovn0 46487  ovn0lem 46486  ovnf 46484  ovnome 46494  ovnssle 46482  ovnsslelem 46481  ovnsupge0 46478
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46524  ovnhoilem1 46522  ovnhoilem2 46523  vonhoi 46588
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46541  hoidifhspf 46539  hoidifhspval 46529  hoidifhspval2 46536  hoidifhspval3 46540  hspmbl 46550  hspmbllem1 46547  hspmbllem2 46548  hspmbllem3 46549
[Fremlin1] p. 31Definition 115Evoncmpl 46542  vonmea 46495
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46493  ovnsubadd2 46567  ovnsubadd2lem 46566  ovnsubaddlem1 46491  ovnsubaddlem2 46492
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46552  hoimbl2 46586  hoimbllem 46551  hspdifhsp 46537  opnvonmbl 46555  opnvonmbllem2 46554
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46557
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46600  iccvonmbllem 46599  ioovonmbl 46598
[Fremlin1] p. 32Proposition 115G (d)vonicc 46606  vonicclem2 46605  vonioo 46603  vonioolem2 46602  vonn0icc 46609  vonn0icc2 46613  vonn0ioo 46608  vonn0ioo2 46611
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46610  snvonmbl 46607  vonct 46614  vonsn 46612
[Fremlin1] p. 35Lemma 121Asubsalsal 46280
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46279  subsaliuncllem 46278
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46646  salpreimalegt 46630  salpreimaltle 46647
[Fremlin1] p. 35Proposition 121B (i)issmf 46649  issmff 46655  issmflem 46648
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46666  issmflelem 46665  smfpreimale 46675
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46677  issmfgtlem 46676
[Fremlin1] p. 36Definition 121Cdf-smblfn 46617  issmf 46649  issmff 46655  issmfge 46691  issmfgelem 46690  issmfgt 46677  issmfgtlem 46676  issmfle 46666  issmflelem 46665  issmflem 46648
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46628  salpreimagtlt 46651  salpreimalelt 46650
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46691  issmfgelem 46690
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46674
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46672  cnfsmf 46661
[Fremlin1] p. 36Proposition 121D (c)decsmf 46688  decsmflem 46687  incsmf 46663  incsmflem 46662
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46622  pimconstlt1 46623  smfconst 46670
[Fremlin1] p. 37Proposition 121E (b)smfadd 46686  smfaddlem1 46684  smfaddlem2 46685
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46717
[Fremlin1] p. 37Proposition 121E (d)smfmul 46716  smfmullem1 46712  smfmullem2 46713  smfmullem3 46714  smfmullem4 46715
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46718
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46721  smfpimbor1lem2 46720
[Fremlin1] p. 37Proposition 121E (g)smfco 46723
[Fremlin1] p. 37Proposition 121E (h)smfres 46711
[Fremlin1] p. 38Proposition 121E (e)smfrec 46710
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46719  smfresal 46709
[Fremlin1] p. 38Proposition 121F (a)smflim 46698  smflim2 46727  smflimlem1 46692  smflimlem2 46693  smflimlem3 46694  smflimlem4 46695  smflimlem5 46696  smflimlem6 46697  smflimmpt 46731
[Fremlin1] p. 38Proposition 121F (b)smfsup 46735  smfsuplem1 46732  smfsuplem2 46733  smfsuplem3 46734  smfsupmpt 46736  smfsupxr 46737
[Fremlin1] p. 38Proposition 121F (c)smfinf 46739  smfinflem 46738  smfinfmpt 46740
[Fremlin1] p. 39Remark 121Gsmflim 46698  smflim2 46727  smflimmpt 46731
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46729
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46759  smfdivdmmbl2 46762  smfinfdmmbl 46770  smfinfdmmbllem 46769  smfsupdmmbl 46766  smfsupdmmbllem 46765
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46749  smflimsuplem2 46742  smflimsuplem6 46746  smflimsuplem7 46747  smflimsuplem8 46748  smflimsupmpt 46750
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46752  smfliminflem 46751  smfliminfmpt 46753
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46617
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46763  fsupdm2 46764
[Fremlin1], p. 39Proposition 121Hadddmmbl 46754  adddmmbl2 46755  finfdm 46767  finfdm2 46768  fsupdm 46763  fsupdm2 46764  muldmmbl 46756  muldmmbl2 46757
[Fremlin1], p. 39Proposition 121F (c)finfdm 46767  finfdm2 46768
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25590
[Fremlin5] p. 213Lemma 565Cauniioovol 25633
[Fremlin5] p. 214Lemma 565Cauniioombl 25643
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37658
[Fremlin5] p. 220Theorem 565Maftc1anc 37661
[FreydScedrov] p. 283Axiom of Infinityax-inf 9707  inf1 9691  inf2 9692
[Gleason] p. 117Proposition 9-2.1df-enq 10980  enqer 10990
[Gleason] p. 117Proposition 9-2.2df-1nq 10985  df-nq 10981
[Gleason] p. 117Proposition 9-2.3df-plpq 10977  df-plq 10983
[Gleason] p. 119Proposition 9-2.4caovmo 7687  df-mpq 10978  df-mq 10984
[Gleason] p. 119Proposition 9-2.5df-rq 10986
[Gleason] p. 119Proposition 9-2.6ltexnq 11044
[Gleason] p. 120Proposition 9-2.6(i)halfnq 11045  ltbtwnnq 11047
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 11040
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 11041
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 11048
[Gleason] p. 121Definition 9-3.1df-np 11050
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 11062
[Gleason] p. 121Definition 9-3.1(iii)prnmax 11064
[Gleason] p. 122Definitiondf-1p 11051
[Gleason] p. 122Remark (1)prub 11063
[Gleason] p. 122Lemma 9-3.4prlem934 11102
[Gleason] p. 122Proposition 9-3.2df-ltp 11054
[Gleason] p. 122Proposition 9-3.3ltsopr 11101  psslinpr 11100  supexpr 11123  suplem1pr 11121  suplem2pr 11122
[Gleason] p. 123Proposition 9-3.5addclpr 11087  addclprlem1 11085  addclprlem2 11086  df-plp 11052
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11091
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11090
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11103
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11112  ltexprlem1 11105  ltexprlem2 11106  ltexprlem3 11107  ltexprlem4 11108  ltexprlem5 11109  ltexprlem6 11110  ltexprlem7 11111
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11114  ltaprlem 11113
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11115
[Gleason] p. 124Lemma 9-3.6prlem936 11116
[Gleason] p. 124Proposition 9-3.7df-mp 11053  mulclpr 11089  mulclprlem 11088  reclem2pr 11117
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11098
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11093
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11092
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11097
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11120  reclem3pr 11118  reclem4pr 11119
[Gleason] p. 126Proposition 9-4.1df-enr 11124  enrer 11132
[Gleason] p. 126Proposition 9-4.2df-0r 11129  df-1r 11130  df-nr 11125
[Gleason] p. 126Proposition 9-4.3df-mr 11127  df-plr 11126  negexsr 11171  recexsr 11176  recexsrlem 11172
[Gleason] p. 127Proposition 9-4.4df-ltr 11128
[Gleason] p. 130Proposition 10-1.3creui 12288  creur 12287  cru 12285
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11257  axcnre 11233
[Gleason] p. 132Definition 10-3.1crim 15164  crimd 15281  crimi 15242  crre 15163  crred 15280  crrei 15241
[Gleason] p. 132Definition 10-3.2remim 15166  remimd 15247
[Gleason] p. 133Definition 10.36absval2 15333  absval2d 15494  absval2i 15446
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15190  cjaddd 15269  cjaddi 15237
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15191  cjmuld 15270  cjmuli 15238
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15189  cjcjd 15248  cjcji 15220
[Gleason] p. 133Proposition 10-3.4(f)cjre 15188  cjreb 15172  cjrebd 15251  cjrebi 15223  cjred 15275  rere 15171  rereb 15169  rerebd 15250  rerebi 15222  rered 15273
[Gleason] p. 133Proposition 10-3.4(h)addcj 15197  addcjd 15261  addcji 15232
[Gleason] p. 133Proposition 10-3.7(a)absval 15287
[Gleason] p. 133Proposition 10-3.7(b)abscj 15328  abscjd 15499  abscji 15450
[Gleason] p. 133Proposition 10-3.7(c)abs00 15338  abs00d 15495  abs00i 15447  absne0d 15496
[Gleason] p. 133Proposition 10-3.7(d)releabs 15370  releabsd 15500  releabsi 15451
[Gleason] p. 133Proposition 10-3.7(f)absmul 15343  absmuld 15503  absmuli 15453
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15331  sqabsaddi 15454
[Gleason] p. 133Proposition 10-3.7(h)abstri 15379  abstrid 15505  abstrii 15457
[Gleason] p. 134Definition 10-4.1df-exp 14113  exp0 14116  expp1 14119  expp1d 14197
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26739  cxpaddd 26777  expadd 14155  expaddd 14198  expaddz 14157
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26748  cxpmuld 26797  expmul 14158  expmuld 14199  expmulz 14159
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26745  mulcxpd 26788  mulexp 14152  mulexpd 14211  mulexpz 14153
[Gleason] p. 140Exercise 1znnen 16260
[Gleason] p. 141Definition 11-2.1fzval 13569
[Gleason] p. 168Proposition 12-2.1(a)climadd 15678  rlimadd 15689  rlimdiv 15694
[Gleason] p. 168Proposition 12-2.1(b)climsub 15680  rlimsub 15691
[Gleason] p. 168Proposition 12-2.1(c)climmul 15679  rlimmul 15692
[Gleason] p. 171Corollary 12-2.2climmulc2 15683
[Gleason] p. 172Corollary 12-2.5climrecl 15629
[Gleason] p. 172Proposition 12-2.4(c)climabs 15650  climcj 15651  climim 15653  climre 15652  rlimabs 15655  rlimcj 15656  rlimim 15658  rlimre 15657
[Gleason] p. 173Definition 12-3.1df-ltxr 11329  df-xr 11328  ltxr 13178
[Gleason] p. 175Definition 12-4.1df-limsup 15517  limsupval 15520
[Gleason] p. 180Theorem 12-5.1climsup 15718
[Gleason] p. 180Theorem 12-5.3caucvg 15727  caucvgb 15728  caucvgbf 45405  caucvgr 15724  climcau 15719
[Gleason] p. 182Exercise 3cvgcmp 15864
[Gleason] p. 182Exercise 4cvgrat 15931
[Gleason] p. 195Theorem 13-2.12abs1m 15384
[Gleason] p. 217Lemma 13-4.1btwnzge0 13879
[Gleason] p. 223Definition 14-1.1df-met 21381
[Gleason] p. 223Definition 14-1.1(a)met0 24374  xmet0 24373
[Gleason] p. 223Definition 14-1.1(b)metgt0 24390
[Gleason] p. 223Definition 14-1.1(c)metsym 24381
[Gleason] p. 223Definition 14-1.1(d)mettri 24383  mstri 24500  xmettri 24382  xmstri 24499
[Gleason] p. 225Definition 14-1.5xpsmet 24413
[Gleason] p. 230Proposition 14-2.6txlm 23677
[Gleason] p. 240Theorem 14-4.3metcnp4 25363
[Gleason] p. 240Proposition 14-4.2metcnp3 24574
[Gleason] p. 243Proposition 14-4.16addcn 24906  addcn2 15640  mulcn 24908  mulcn2 15642  subcn 24907  subcn2 15641
[Gleason] p. 295Remarkbcval3 14355  bcval4 14356
[Gleason] p. 295Equation 2bcpasc 14370
[Gleason] p. 295Definition of binomial coefficientbcval 14353  df-bc 14352
[Gleason] p. 296Remarkbcn0 14359  bcnn 14361
[Gleason] p. 296Theorem 15-2.8binom 15878
[Gleason] p. 308Equation 2ef0 16139
[Gleason] p. 308Equation 3efcj 16140
[Gleason] p. 309Corollary 15-4.3efne0 16145
[Gleason] p. 309Corollary 15-4.4efexp 16149
[Gleason] p. 310Equation 14sinadd 16212
[Gleason] p. 310Equation 15cosadd 16213
[Gleason] p. 311Equation 17sincossq 16224
[Gleason] p. 311Equation 18cosbnd 16229  sinbnd 16228
[Gleason] p. 311Lemma 15-4.7sqeqor 14265  sqeqori 14263
[Gleason] p. 311Definition of ` `df-pi 16120
[Godowski] p. 730Equation SFgoeqi 32305
[GodowskiGreechie] p. 249Equation IV3oai 31700
[Golan] p. 1Remarksrgisid 20236
[Golan] p. 1Definitiondf-srg 20214
[Golan] p. 149Definitiondf-slmd 33180
[Gonshor] p. 7Definitiondf-scut 27846
[Gonshor] p. 9Theorem 2.5slerec 27882
[Gonshor] p. 10Theorem 2.6cofcut1 27972  cofcut1d 27973
[Gonshor] p. 10Theorem 2.7cofcut2 27974  cofcut2d 27975
[Gonshor] p. 12Theorem 2.9cofcutr 27976  cofcutr1d 27977  cofcutr2d 27978
[Gonshor] p. 13Definitiondf-adds 28011
[Gonshor] p. 14Theorem 3.1addsprop 28027
[Gonshor] p. 15Theorem 3.2addsunif 28053
[Gonshor] p. 17Theorem 3.4mulsprop 28174
[Gonshor] p. 18Theorem 3.5mulsunif 28194
[Gonshor] p. 28Lemma 4.2halfcut 28434
[Gonshor] p. 28Theorem 4.2pw2cut 28438
[Gonshor] p. 30Theorem 4.2addhalfcut 28437
[Gonshor] p. 95Theorem 6.1addsbday 28068
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36123
[Gratzer] p. 23Section 0.6df-mre 17644
[Gratzer] p. 27Section 0.6df-mri 17646
[Hall] p. 1Section 1.1df-asslaw 47911  df-cllaw 47909  df-comlaw 47910
[Hall] p. 2Section 1.2df-clintop 47923
[Hall] p. 7Section 1.3df-sgrp2 47944
[Halmos] p. 28Partition ` `df-parts 38721  dfmembpart2 38726
[Halmos] p. 31Theorem 17.3riesz1 32097  riesz2 32098
[Halmos] p. 41Definition of Hermitianhmopadj2 31973
[Halmos] p. 42Definition of projector orderingpjordi 32205
[Halmos] p. 43Theorem 26.1elpjhmop 32217  elpjidm 32216  pjnmopi 32180
[Halmos] p. 44Remarkpjinormi 31719  pjinormii 31708
[Halmos] p. 44Theorem 26.2elpjch 32221  pjrn 31739  pjrni 31734  pjvec 31728
[Halmos] p. 44Theorem 26.3pjnorm2 31759
[Halmos] p. 44Theorem 26.4hmopidmpj 32186  hmopidmpji 32184
[Halmos] p. 45Theorem 27.1pjinvari 32223
[Halmos] p. 45Theorem 27.3pjoci 32212  pjocvec 31729
[Halmos] p. 45Theorem 27.4pjorthcoi 32201
[Halmos] p. 48Theorem 29.2pjssposi 32204
[Halmos] p. 48Theorem 29.3pjssdif1i 32207  pjssdif2i 32206
[Halmos] p. 50Definition of spectrumdf-spec 31887
[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 1793
[Hatcher] p. 25Definitiondf-phtpc 25043  df-phtpy 25022
[Hatcher] p. 26Definitiondf-pco 25057  df-pi1 25060
[Hatcher] p. 26Proposition 1.2phtpcer 25046
[Hatcher] p. 26Proposition 1.3pi1grp 25102
[Hefferon] p. 240Definition 3.12df-dmat 22517  df-dmatalt 48127
[Helfgott] p. 2Theoremtgoldbach 47691
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47676
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47688  bgoldbtbnd 47683  bgoldbtbnd 47683  tgblthelfgott 47689
[Helfgott] p. 5Proposition 1.1circlevma 34619
[Helfgott] p. 69Statement 7.49circlemethhgt 34620
[Helfgott] p. 69Statement 7.50hgt750lema 34634  hgt750lemb 34633  hgt750leme 34635  hgt750lemf 34630  hgt750lemg 34631
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47685  tgoldbachgt 34640  tgoldbachgtALTV 47686  tgoldbachgtd 34639
[Helfgott] p. 70Statement 7.49ax-hgt749 34621
[Herstein] p. 54Exercise 28df-grpo 30525
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18984  grpoideu 30541  mndideu 18783
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19014  grpoinveu 30551
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19045  grpo2inv 30563
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19058  grpoinvop 30565
[Herstein] p. 57Exercise 1dfgrp3e 19080
[Hitchcock] p. 5Rule A3mptnan 1766
[Hitchcock] p. 5Rule A4mptxor 1767
[Hitchcock] p. 5Rule A5mtpxor 1769
[Holland] p. 1519Theorem 2sumdmdi 32452
[Holland] p. 1520Lemma 5cdj1i 32465  cdj3i 32473  cdj3lem1 32466  cdjreui 32464
[Holland] p. 1524Lemma 7mddmdin0i 32463
[Holland95] p. 13Theorem 3.6hlathil 41922
[Holland95] p. 14Line 15hgmapvs 41848
[Holland95] p. 14Line 16hdmaplkr 41870
[Holland95] p. 14Line 17hdmapellkr 41871
[Holland95] p. 14Line 19hdmapglnm2 41868
[Holland95] p. 14Line 20hdmapip0com 41874
[Holland95] p. 14Theorem 3.6hdmapevec2 41793
[Holland95] p. 14Lines 24 and 25hdmapoc 41888
[Holland95] p. 204Definition of involutiondf-srng 20863
[Holland95] p. 212Definition of subspacedf-psubsp 39460
[Holland95] p. 214Lemma 3.3lclkrlem2v 41485
[Holland95] p. 214Definition 3.2df-lpolN 41438
[Holland95] p. 214Definition of nonsingularpnonsingN 39890
[Holland95] p. 215Lemma 3.3(1)dihoml4 41334  poml4N 39910
[Holland95] p. 215Lemma 3.3(2)dochexmid 41425  pexmidALTN 39935  pexmidN 39926
[Holland95] p. 218Theorem 3.6lclkr 41490
[Holland95] p. 218Definition of dual vector spacedf-ldual 39080  ldualset 39081
[Holland95] p. 222Item 1df-lines 39458  df-pointsN 39459
[Holland95] p. 222Item 2df-polarityN 39860
[Holland95] p. 223Remarkispsubcl2N 39904  omllaw4 39202  pol1N 39867  polcon3N 39874
[Holland95] p. 223Definitiondf-psubclN 39892
[Holland95] p. 223Equation for polaritypolval2N 39863
[Holmes] p. 40Definitiondf-xrn 38327
[Hughes] p. 44Equation 1.21bax-his3 31116
[Hughes] p. 47Definition of projection operatordfpjop 32214
[Hughes] p. 49Equation 1.30eighmre 31995  eigre 31867  eigrei 31866
[Hughes] p. 49Equation 1.31eighmorth 31996  eigorth 31870  eigorthi 31869
[Hughes] p. 137Remark (ii)eigposi 31868
[Huneke] p. 1Claim 1frgrncvvdeq 30341
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30337
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30338
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30339
[Huneke] p. 2Claim 2frgrregorufr 30357  frgrregorufr0 30356  frgrregorufrg 30358
[Huneke] p. 2Claim 3frgrhash2wsp 30364  frrusgrord 30373  frrusgrord0 30372
[Huneke] p. 2Statementdf-clwwlknon 30120
[Huneke] p. 2Statement 4frgrwopreglem4 30347
[Huneke] p. 2Statement 5frgrwopreg1 30350  frgrwopreg2 30351  frgrwopregasn 30348  frgrwopregbsn 30349
[Huneke] p. 2Statement 6frgrwopreglem5 30353
[Huneke] p. 2Statement 7fusgreghash2wspv 30367
[Huneke] p. 2Statement 8fusgreghash2wsp 30370
[Huneke] p. 2Statement 9clwlksndivn 30118  numclwlk1 30403  numclwlk1lem1 30401  numclwlk1lem2 30402  numclwwlk1 30393  numclwwlk8 30424
[Huneke] p. 2Definition 3frgrwopreglem1 30344
[Huneke] p. 2Definition 4df-clwlks 29807
[Huneke] p. 2Definition 62clwwlk 30379
[Huneke] p. 2Definition 7numclwwlkovh 30405  numclwwlkovh0 30404
[Huneke] p. 2Statement 10numclwwlk2 30413
[Huneke] p. 2Statement 11rusgrnumwlkg 30010
[Huneke] p. 2Statement 12numclwwlk3 30417
[Huneke] p. 2Statement 13numclwwlk5 30420
[Huneke] p. 2Statement 14numclwwlk7 30423
[Indrzejczak] p. 33Definition ` `Enatded 30435  natded 30435
[Indrzejczak] p. 33Definition ` `Inatded 30435
[Indrzejczak] p. 34Definition ` `Enatded 30435  natded 30435
[Indrzejczak] p. 34Definition ` `Inatded 30435
[Jech] p. 4Definition of classcv 1536  cvjust 2734
[Jech] p. 42Lemma 6.1alephexp1 10648
[Jech] p. 42Equation 6.1alephadd 10646  alephmul 10647
[Jech] p. 43Lemma 6.2infmap 10645  infmap2 10286
[Jech] p. 71Lemma 9.3jech9.3 9883
[Jech] p. 72Equation 9.3scott0 9955  scottex 9954
[Jech] p. 72Exercise 9.1rankval4 9936
[Jech] p. 72Scheme "Collection Principle"cp 9960
[Jech] p. 78Noteopthprc 5764
[JonesMatijasevic] p. 694Definition 2.3rmxyval 42872
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 42960
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 42961
[JonesMatijasevic] p. 695Equation 2.7rmxadd 42884
[JonesMatijasevic] p. 695Equation 2.8rmyadd 42888
[JonesMatijasevic] p. 695Equation 2.9rmxp1 42889  rmyp1 42890
[JonesMatijasevic] p. 695Equation 2.10rmxm1 42891  rmym1 42892
[JonesMatijasevic] p. 695Equation 2.11rmx0 42882  rmx1 42883  rmxluc 42893
[JonesMatijasevic] p. 695Equation 2.12rmy0 42886  rmy1 42887  rmyluc 42894
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 42896
[JonesMatijasevic] p. 695Equation 2.14rmydbl 42897
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42917  jm2.17b 42918  jm2.17c 42919
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 42950
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 42954
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 42945
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42920  jm2.24nn 42916
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 42959
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 42965  rmygeid 42921
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 42977
[Juillerat] p. 11Section *5etransc 46204  etransclem47 46202  etransclem48 46203
[Juillerat] p. 12Equation (7)etransclem44 46199
[Juillerat] p. 12Equation *(7)etransclem46 46201
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46187
[Juillerat] p. 13Proofetransclem35 46190
[Juillerat] p. 13Part of case 2 proven inetransclem38 46193
[Juillerat] p. 13Part of case 2 provenetransclem24 46179
[Juillerat] p. 13Part of case 2: proven inetransclem41 46196
[Juillerat] p. 14Proofetransclem23 46178
[KalishMontague] p. 81Note 1ax-6 1967
[KalishMontague] p. 85Lemma 2equid 2011
[KalishMontague] p. 85Lemma 3equcomi 2016
[KalishMontague] p. 86Lemma 7cbvalivw 2006  cbvaliw 2005  wl-cbvmotv 37467  wl-motae 37469  wl-moteq 37468
[KalishMontague] p. 87Lemma 8spimvw 1995  spimw 1970
[KalishMontague] p. 87Lemma 9spfw 2032  spw 2033
[Kalmbach] p. 14Definition of latticechabs1 31548  chabs1i 31550  chabs2 31549  chabs2i 31551  chjass 31565  chjassi 31518  latabs1 18545  latabs2 18546
[Kalmbach] p. 15Definition of atomdf-at 32370  ela 32371
[Kalmbach] p. 15Definition of coverscvbr2 32315  cvrval2 39230
[Kalmbach] p. 16Definitiondf-ol 39134  df-oml 39135
[Kalmbach] p. 20Definition of commutescmbr 31616  cmbri 31622  cmtvalN 39167  df-cm 31615  df-cmtN 39133
[Kalmbach] p. 22Remarkomllaw5N 39203  pjoml5 31645  pjoml5i 31620
[Kalmbach] p. 22Definitionpjoml2 31643  pjoml2i 31617
[Kalmbach] p. 22Theorem 2(v)cmcm 31646  cmcmi 31624  cmcmii 31629  cmtcomN 39205
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39201  omlsi 31436  pjoml 31468  pjomli 31467
[Kalmbach] p. 22Definition of OML lawomllaw2N 39200
[Kalmbach] p. 23Remarkcmbr2i 31628  cmcm3 31647  cmcm3i 31626  cmcm3ii 31631  cmcm4i 31627  cmt3N 39207  cmt4N 39208  cmtbr2N 39209
[Kalmbach] p. 23Lemma 3cmbr3 31640  cmbr3i 31632  cmtbr3N 39210
[Kalmbach] p. 25Theorem 5fh1 31650  fh1i 31653  fh2 31651  fh2i 31654  omlfh1N 39214
[Kalmbach] p. 65Remarkchjatom 32389  chslej 31530  chsleji 31490  shslej 31412  shsleji 31402
[Kalmbach] p. 65Proposition 1chocin 31527  chocini 31486  chsupcl 31372  chsupval2 31442  h0elch 31287  helch 31275  hsupval2 31441  ocin 31328  ococss 31325  shococss 31326
[Kalmbach] p. 65Definition of subspace sumshsval 31344
[Kalmbach] p. 66Remarkdf-pjh 31427  pjssmi 32197  pjssmii 31713
[Kalmbach] p. 67Lemma 3osum 31677  osumi 31674
[Kalmbach] p. 67Lemma 4pjci 32232
[Kalmbach] p. 103Exercise 6atmd2 32432
[Kalmbach] p. 103Exercise 12mdsl0 32342
[Kalmbach] p. 140Remarkhatomic 32392  hatomici 32391  hatomistici 32394
[Kalmbach] p. 140Proposition 1atlatmstc 39275
[Kalmbach] p. 140Proposition 1(i)atexch 32413  lsatexch 38999
[Kalmbach] p. 140Proposition 1(ii)chcv1 32387  cvlcvr1 39295  cvr1 39367
[Kalmbach] p. 140Proposition 1(iii)cvexch 32406  cvexchi 32401  cvrexch 39377
[Kalmbach] p. 149Remark 2chrelati 32396  hlrelat 39359  hlrelat5N 39358  lrelat 38970
[Kalmbach] p. 153Exercise 5lsmcv 21166  lsmsatcv 38966  spansncv 31685  spansncvi 31684
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 38985  spansncv2 32325
[Kalmbach] p. 266Definitiondf-st 32243
[Kalmbach2] p. 8Definition of adjointdf-adjh 31881
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10715  fpwwe2 10712
[KanamoriPincus] p. 416Corollary 1.3canth4 10716
[KanamoriPincus] p. 417Corollary 1.6canthp1 10723
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10718
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10720
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10733
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10737  gchxpidm 10738
[KanamoriPincus] p. 419Theorem 2.1gchacg 10749  gchhar 10748
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10284  unxpwdom 9658
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10739
[Kreyszig] p. 3Property M1metcl 24363  xmetcl 24362
[Kreyszig] p. 4Property M2meteq0 24370
[Kreyszig] p. 8Definition 1.1-8dscmet 24606
[Kreyszig] p. 12Equation 5conjmul 12011  muleqadd 11934
[Kreyszig] p. 18Definition 1.3-2mopnval 24469
[Kreyszig] p. 19Remarkmopntopon 24470
[Kreyszig] p. 19Theorem T1mopn0 24532  mopnm 24475
[Kreyszig] p. 19Theorem T2unimopn 24530
[Kreyszig] p. 19Definition of neighborhoodneibl 24535
[Kreyszig] p. 20Definition 1.3-3metcnp2 24576
[Kreyszig] p. 25Definition 1.4-1lmbr 23287  lmmbr 25311  lmmbr2 25312
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23409
[Kreyszig] p. 28Theorem 1.4-5lmcau 25366
[Kreyszig] p. 28Definition 1.4-3iscau 25329  iscmet2 25347
[Kreyszig] p. 30Theorem 1.4-7cmetss 25369
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23490  metelcls 25358
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25359  metcld2 25360
[Kreyszig] p. 51Equation 2clmvneg1 25151  lmodvneg1 20925  nvinv 30671  vcm 30608
[Kreyszig] p. 51Equation 1aclm0vs 25147  lmod0vs 20915  slmd0vs 33203  vc0 30606
[Kreyszig] p. 51Equation 1blmodvs0 20916  slmdvs0 33204  vcz 30607
[Kreyszig] p. 58Definition 2.2-1imsmet 30723  ngpmet 24637  nrmmetd 24608
[Kreyszig] p. 59Equation 1imsdval 30718  imsdval2 30719  ncvspds 25214  ngpds 24638
[Kreyszig] p. 63Problem 1nmval 24623  nvnd 30720
[Kreyszig] p. 64Problem 2nmeq0 24652  nmge0 24651  nvge0 30705  nvz 30701
[Kreyszig] p. 64Problem 3nmrtri 24658  nvabs 30704
[Kreyszig] p. 91Definition 2.7-1isblo3i 30833
[Kreyszig] p. 92Equation 2df-nmoo 30777
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30839  blocni 30837
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30838
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25257  ipeq0 21679  ipz 30751
[Kreyszig] p. 135Problem 2cphpyth 25269  pythi 30882
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30886
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25291
[Kreyszig] p. 144Equation 4supcvg 15904
[Kreyszig] p. 144Theorem 3.3-1minvec 25489  minveco 30916
[Kreyszig] p. 196Definition 3.9-1df-aj 30782
[Kreyszig] p. 247Theorem 4.7-2bcth 25382
[Kreyszig] p. 249Theorem 4.7-3ubth 30905
[Kreyszig] p. 470Definition of positive operator orderingleop 32155  leopg 32154
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32173
[Kreyszig] p. 525Theorem 10.1-1htth 30950
[Kulpa] p. 547Theorempoimir 37613
[Kulpa] p. 547Equation (1)poimirlem32 37612
[Kulpa] p. 547Equation (2)poimirlem31 37611
[Kulpa] p. 548Theorembroucube 37614
[Kulpa] p. 548Equation (6)poimirlem26 37606
[Kulpa] p. 548Equation (7)poimirlem27 37607
[Kunen] p. 10Axiom 0ax6e 2391  axnul 5323
[Kunen] p. 11Axiom 3axnul 5323
[Kunen] p. 12Axiom 6zfrep6 7995
[Kunen] p. 24Definition 10.24mapval 8896  mapvalg 8894
[Kunen] p. 30Lemma 10.20fodomg 10591
[Kunen] p. 31Definition 10.24mapex 7979
[Kunen] p. 95Definition 2.1df-r1 9833
[Kunen] p. 97Lemma 2.10r1elss 9875  r1elssi 9874
[Kunen] p. 107Exercise 4rankop 9927  rankopb 9921  rankuni 9932  rankxplim 9948  rankxpsuc 9951
[Kunen2] p. 111Lemma II.2.4(1)traxext 44910
[Kunen2] p. 112Part of Corollaray II.2.5wfaxext 44911
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 5027
[Lang] , p. 225Corollary 1.3finexttrb 33675
[Lang] p. Definitiondf-rn 5711
[Lang] p. 3Statementlidrideqd 18707  mndbn0 18788
[Lang] p. 3Definitiondf-mnd 18773
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18725
[Lang] p. 4Property of composites. Second formulagsumccat 18876
[Lang] p. 5Equationgsumreidx 19959
[Lang] p. 5Definition of an (infinite) productgsumfsupp 47905
[Lang] p. 6Examplenn0mnd 47902
[Lang] p. 6Equationgsumxp2 20022
[Lang] p. 6Statementcycsubm 19242
[Lang] p. 6Definitionmulgnn0gsum 19120
[Lang] p. 6Observationmndlsmidm 19712
[Lang] p. 7Definitiondfgrp2e 19003
[Lang] p. 30Definitiondf-tocyc 33100
[Lang] p. 32Property (a)cyc3genpm 33145
[Lang] p. 32Property (b)cyc3conja 33150  cycpmconjv 33135
[Lang] p. 53Definitiondf-cat 17726
[Lang] p. 53Axiom CAT 1cat1 18164  cat1lem 18163
[Lang] p. 54Definitiondf-iso 17810
[Lang] p. 57Definitiondf-inito 18051  df-termo 18052
[Lang] p. 58Exampleirinitoringc 21513
[Lang] p. 58Statementinitoeu1 18078  termoeu1 18085
[Lang] p. 62Definitiondf-func 17922
[Lang] p. 65Definitiondf-nat 18011
[Lang] p. 91Notedf-ringc 20668
[Lang] p. 92Statementmxidlprm 33463
[Lang] p. 92Definitionisprmidlc 33440
[Lang] p. 128Remarkdsmmlmod 21788
[Lang] p. 129Prooflincscm 48159  lincscmcl 48161  lincsum 48158  lincsumcl 48160
[Lang] p. 129Statementlincolss 48163
[Lang] p. 129Observationdsmmfi 21781
[Lang] p. 141Theorem 5.3dimkerim 33640  qusdimsum 33641
[Lang] p. 141Corollary 5.4lssdimle 33620
[Lang] p. 147Definitionsnlindsntor 48200
[Lang] p. 504Statementmat1 22474  matring 22470
[Lang] p. 504Definitiondf-mamu 22416
[Lang] p. 505Statementmamuass 22427  mamutpos 22485  matassa 22471  mattposvs 22482  tposmap 22484
[Lang] p. 513Definitionmdet1 22628  mdetf 22622
[Lang] p. 513Theorem 4.4cramer 22718
[Lang] p. 514Proposition 4.6mdetleib 22614
[Lang] p. 514Proposition 4.8mdettpos 22638
[Lang] p. 515Definitiondf-minmar1 22662  smadiadetr 22702
[Lang] p. 515Corollary 4.9mdetero 22637  mdetralt 22635
[Lang] p. 517Proposition 4.15mdetmul 22650
[Lang] p. 518Definitiondf-madu 22661
[Lang] p. 518Proposition 4.16madulid 22672  madurid 22671  matinv 22704
[Lang] p. 561Theorem 3.1cayleyhamilton 22917
[Lang], p. 224Proposition 1.2extdgmul 33674  fedgmul 33644
[Lang], p. 561Remarkchpmatply1 22859
[Lang], p. 561Definitiondf-chpmat 22854
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44303
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44298
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44304
[LeBlanc] p. 277Rule R2axnul 5323
[Levy] p. 12Axiom 4.3.1df-clab 2718
[Levy] p. 59Definitiondf-ttrcl 9777
[Levy] p. 64Theorem 5.6(ii)frinsg 9820
[Levy] p. 338Axiomdf-clel 2819  df-cleq 2732
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2819  df-cleq 2732
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2718
[Levy] p. 358Axiomdf-clab 2718
[Levy58] p. 2Definition Iisfin1-3 10455
[Levy58] p. 2Definition IIdf-fin2 10355
[Levy58] p. 2Definition Iadf-fin1a 10354
[Levy58] p. 2Definition IIIdf-fin3 10357
[Levy58] p. 3Definition Vdf-fin5 10358
[Levy58] p. 3Definition IVdf-fin4 10356
[Levy58] p. 4Definition VIdf-fin6 10359
[Levy58] p. 4Definition VIIdf-fin7 10360
[Levy58], p. 3Theorem 1fin1a2 10484
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27749
[Lipparini] p. 3Lemma 2.1.4noresle 27760
[Lipparini] p. 6Proposition 4.2noinfbnd1 27792  nosupbnd1 27777
[Lipparini] p. 6Proposition 4.3noinfbnd2 27794  nosupbnd2 27779
[Lipparini] p. 7Theorem 5.1noetasuplem3 27798  noetasuplem4 27799
[Lipparini] p. 7Corollary 4.4nosupinfsep 27795
[Lopez-Astorga] p. 12Rule 1mptnan 1766
[Lopez-Astorga] p. 12Rule 2mptxor 1767
[Lopez-Astorga] p. 12Rule 3mtpxor 1769
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32440
[Maeda] p. 168Lemma 5mdsym 32444  mdsymi 32443
[Maeda] p. 168Lemma 4(i)mdsymlem4 32438  mdsymlem6 32440  mdsymlem7 32441
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32442
[MaedaMaeda] p. 1Remarkssdmd1 32345  ssdmd2 32346  ssmd1 32343  ssmd2 32344
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32341
[MaedaMaeda] p. 1Definition 1.1df-dmd 32313  df-md 32312  mdbr 32326
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32363  mdslj1i 32351  mdslj2i 32352  mdslle1i 32349  mdslle2i 32350  mdslmd1i 32361  mdslmd2i 32362
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32353  mdsl2bi 32355  mdsl2i 32354
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32367
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32364
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32365
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32342
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32347  mdsl3 32348
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32366
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32461
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39277  hlrelat1 39357
[MaedaMaeda] p. 31Lemma 7.5lcvexch 38995
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32368  cvmdi 32356  cvnbtwn4 32321  cvrnbtwn4 39235
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32369
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39296  cvp 32407  cvrp 39373  lcvp 38996
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32431
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32430
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39289  hlexch4N 39349
[MaedaMaeda] p. 34Exercise 7.1atabsi 32433
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39400
[MaedaMaeda] p. 61Definition 15.10psubN 39706  atpsubN 39710  df-pointsN 39459  pointpsubN 39708
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39461  pmap11 39719  pmaple 39718  pmapsub 39725  pmapval 39714
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39722  pmap1N 39724
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39727  pmapglb2N 39728  pmapglb2xN 39729  pmapglbx 39726
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39809
[MaedaMaeda] p. 67Postulate PS1ps-1 39434
[MaedaMaeda] p. 68Lemma 16.2df-padd 39753  paddclN 39799  paddidm 39798
[MaedaMaeda] p. 68Condition PS2ps-2 39435
[MaedaMaeda] p. 68Equation 16.2.1paddass 39795
[MaedaMaeda] p. 69Lemma 16.4ps-1 39434
[MaedaMaeda] p. 69Theorem 16.4ps-2 39435
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19717  lsmmod2 19718  lssats 38968  shatomici 32390  shatomistici 32393  shmodi 31422  shmodsi 31421
[MaedaMaeda] p. 130Remark 29.6dmdmd 32332  mdsymlem7 32441
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31621
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31525
[MaedaMaeda] p. 139Remarksumdmdii 32447
[Margaris] p. 40Rule Cexlimiv 1929
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 396  df-ex 1778  df-or 847  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30432
[Margaris] p. 59Section 14notnotrALTVD 44886
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 44887
[Margaris] p. 79Rule Cexinst01 44596  exinst11 44597
[Margaris] p. 89Theorem 19.219.2 1976  19.2g 2189  r19.2z 4518
[Margaris] p. 89Theorem 19.319.3 2203  rr19.3v 3680
[Margaris] p. 89Theorem 19.5alcom 2160
[Margaris] p. 89Theorem 19.6alex 1824
[Margaris] p. 89Theorem 19.7alnex 1779
[Margaris] p. 89Theorem 19.819.8a 2182
[Margaris] p. 89Theorem 19.919.9 2206  19.9h 2290  exlimd 2219  exlimdh 2294
[Margaris] p. 89Theorem 19.11excom 2163  excomim 2164
[Margaris] p. 89Theorem 19.1219.12 2331
[Margaris] p. 90Section 19conventions-labels 30433  conventions-labels 30433  conventions-labels 30433  conventions-labels 30433
[Margaris] p. 90Theorem 19.14exnal 1825
[Margaris] p. 90Theorem 19.152albi 44347  albi 1816
[Margaris] p. 90Theorem 19.1619.16 2226
[Margaris] p. 90Theorem 19.1719.17 2227
[Margaris] p. 90Theorem 19.182exbi 44349  exbi 1845
[Margaris] p. 90Theorem 19.1919.19 2230
[Margaris] p. 90Theorem 19.202alim 44346  2alimdv 1917  alimd 2213  alimdh 1815  alimdv 1915  ax-4 1807  ralimdaa 3266  ralimdv 3175  ralimdva 3173  ralimdvva 3212  sbcimdv 3878
[Margaris] p. 90Theorem 19.2119.21 2208  19.21h 2291  19.21t 2207  19.21vv 44345  alrimd 2216  alrimdd 2215  alrimdh 1862  alrimdv 1928  alrimi 2214  alrimih 1822  alrimiv 1926  alrimivv 1927  hbralrimi 3150  r19.21be 3258  r19.21bi 3257  ralrimd 3270  ralrimdv 3158  ralrimdva 3160  ralrimdvv 3209  ralrimdvva 3217  ralrimi 3263  ralrimia 3264  ralrimiv 3151  ralrimiva 3152  ralrimivv 3206  ralrimivva 3208  ralrimivvva 3211  ralrimivw 3156
[Margaris] p. 90Theorem 19.222exim 44348  2eximdv 1918  exim 1832  eximd 2217  eximdh 1863  eximdv 1916  rexim 3093  reximd2a 3275  reximdai 3267  reximdd 45053  reximddv 3177  reximddv2 3221  reximddv3 3178  reximdv 3176  reximdv2 3170  reximdva 3174  reximdvai 3171  reximdvva 3213  reximi2 3085
[Margaris] p. 90Theorem 19.2319.23 2212  19.23bi 2192  19.23h 2292  19.23t 2211  exlimdv 1932  exlimdvv 1933  exlimexi 44495  exlimiv 1929  exlimivv 1931  rexlimd3 45046  rexlimdv 3159  rexlimdv3a 3165  rexlimdva 3161  rexlimdva2 3163  rexlimdvaa 3162  rexlimdvv 3218  rexlimdvva 3219  rexlimdvvva 3220  rexlimdvw 3166  rexlimiv 3154  rexlimiva 3153  rexlimivv 3207
[Margaris] p. 90Theorem 19.2419.24 1985
[Margaris] p. 90Theorem 19.2519.25 1879
[Margaris] p. 90Theorem 19.2619.26 1869
[Margaris] p. 90Theorem 19.2719.27 2228  r19.27z 4528  r19.27zv 4529
[Margaris] p. 90Theorem 19.2819.28 2229  19.28vv 44355  r19.28z 4521  r19.28zf 45064  r19.28zv 4524  rr19.28v 3681
[Margaris] p. 90Theorem 19.2919.29 1872  r19.29d2r 3146  r19.29imd 3124
[Margaris] p. 90Theorem 19.3019.30 1880
[Margaris] p. 90Theorem 19.3119.31 2235  19.31vv 44353
[Margaris] p. 90Theorem 19.3219.32 2234  r19.32 47013
[Margaris] p. 90Theorem 19.3319.33-2 44351  19.33 1883
[Margaris] p. 90Theorem 19.3419.34 1986
[Margaris] p. 90Theorem 19.3519.35 1876
[Margaris] p. 90Theorem 19.3619.36 2231  19.36vv 44352  r19.36zv 4530
[Margaris] p. 90Theorem 19.3719.37 2233  19.37vv 44354  r19.37zv 4525
[Margaris] p. 90Theorem 19.3819.38 1837
[Margaris] p. 90Theorem 19.3919.39 1984
[Margaris] p. 90Theorem 19.4019.40-2 1886  19.40 1885  r19.40 3125
[Margaris] p. 90Theorem 19.4119.41 2236  19.41rg 44521
[Margaris] p. 90Theorem 19.4219.42 2237
[Margaris] p. 90Theorem 19.4319.43 1881
[Margaris] p. 90Theorem 19.4419.44 2238  r19.44zv 4527
[Margaris] p. 90Theorem 19.4519.45 2239  r19.45zv 4526
[Margaris] p. 110Exercise 2(b)eu1 2613
[Mayet] p. 370Remarkjpi 32302  largei 32299  stri 32289
[Mayet3] p. 9Definition of CH-statesdf-hst 32244  ishst 32246
[Mayet3] p. 10Theoremhstrbi 32298  hstri 32297
[Mayet3] p. 1223Theorem 4.1mayete3i 31760
[Mayet3] p. 1240Theorem 7.1mayetes3i 31761
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32310
[MegPav2000] p. 2345Definition 3.4-1chintcl 31364  chsupcl 31372
[MegPav2000] p. 2345Definition 3.4-2hatomic 32392
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32386
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32413
[MegPav2000] p. 2366Figure 7pl42N 39940
[MegPav2002] p. 362Lemma 2.2latj31 18557  latj32 18555  latjass 18553
[Megill] p. 444Axiom C5ax-5 1909  ax5ALT 38863
[Megill] p. 444Section 7conventions 30432
[Megill] p. 445Lemma L12aecom-o 38857  ax-c11n 38844  axc11n 2434
[Megill] p. 446Lemma L17equtrr 2021
[Megill] p. 446Lemma L18ax6fromc10 38852
[Megill] p. 446Lemma L19hbnae-o 38884  hbnae 2440
[Megill] p. 447Remark 9.1dfsb1 2489  sbid 2256  sbidd-misc 48811  sbidd 48810
[Megill] p. 448Remark 9.6axc14 2471
[Megill] p. 448Scheme C4'ax-c4 38840
[Megill] p. 448Scheme C5'ax-c5 38839  sp 2184
[Megill] p. 448Scheme C6'ax-11 2158
[Megill] p. 448Scheme C7'ax-c7 38841
[Megill] p. 448Scheme C8'ax-7 2007
[Megill] p. 448Scheme C9'ax-c9 38846
[Megill] p. 448Scheme C10'ax-6 1967  ax-c10 38842
[Megill] p. 448Scheme C11'ax-c11 38843
[Megill] p. 448Scheme C12'ax-8 2110
[Megill] p. 448Scheme C13'ax-9 2118
[Megill] p. 448Scheme C14'ax-c14 38847
[Megill] p. 448Scheme C15'ax-c15 38845
[Megill] p. 448Scheme C16'ax-c16 38848
[Megill] p. 448Theorem 9.4dral1-o 38860  dral1 2447  dral2-o 38886  dral2 2446  drex1 2449  drex2 2450  drsb1 2503  drsb2 2267
[Megill] p. 449Theorem 9.7sbcom2 2174  sbequ 2083  sbid2v 2517
[Megill] p. 450Example in Appendixhba1-o 38853  hba1 2297
[Mendelson] p. 35Axiom A3hirstL-ax3 46807
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3901  rspsbca 3902  stdpc4 2068
[Mendelson] p. 69Axiom 5ax-c4 38840  ra4 3908  stdpc5 2209
[Mendelson] p. 81Rule Cexlimiv 1929
[Mendelson] p. 95Axiom 6stdpc6 2027
[Mendelson] p. 95Axiom 7stdpc7 2251
[Mendelson] p. 225Axiom system NBGru 3802
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5533
[Mendelson] p. 231Exercise 4.10(k)inv1 4421
[Mendelson] p. 231Exercise 4.10(l)unv 4422
[Mendelson] p. 231Exercise 4.10(n)dfin3 4296
[Mendelson] p. 231Exercise 4.10(o)df-nul 4353
[Mendelson] p. 231Exercise 4.10(q)dfin4 4297
[Mendelson] p. 231Exercise 4.10(s)ddif 4164
[Mendelson] p. 231Definition of uniondfun3 4295
[Mendelson] p. 235Exercise 4.12(c)univ 5471
[Mendelson] p. 235Exercise 4.12(d)pwv 4928
[Mendelson] p. 235Exercise 4.12(j)pwin 5589
[Mendelson] p. 235Exercise 4.12(k)pwunss 4640
[Mendelson] p. 235Exercise 4.12(l)pwssun 5590
[Mendelson] p. 235Exercise 4.12(n)uniin 4955
[Mendelson] p. 235Exercise 4.12(p)reli 5850
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6299
[Mendelson] p. 244Proposition 4.8(g)epweon 7810
[Mendelson] p. 246Definition of successordf-suc 6401
[Mendelson] p. 250Exercise 4.36oelim2 8651
[Mendelson] p. 254Proposition 4.22(b)xpen 9206
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9121  xpsneng 9122
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9129  xpcomeng 9130
[Mendelson] p. 254Proposition 4.22(e)xpassen 9132
[Mendelson] p. 255Definitionbrsdom 9035
[Mendelson] p. 255Exercise 4.39endisj 9124
[Mendelson] p. 255Exercise 4.41mapprc 8888
[Mendelson] p. 255Exercise 4.43mapsnen 9102  mapsnend 9101
[Mendelson] p. 255Exercise 4.45mapunen 9212
[Mendelson] p. 255Exercise 4.47xpmapen 9211
[Mendelson] p. 255Exercise 4.42(a)map0e 8940
[Mendelson] p. 255Exercise 4.42(b)map1 9105
[Mendelson] p. 257Proposition 4.24(a)undom 9125
[Mendelson] p. 258Exercise 4.56(c)djuassen 10248  djucomen 10247
[Mendelson] p. 258Exercise 4.56(f)djudom1 10252
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10246
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8587
[Mendelson] p. 266Proposition 4.34(f)oaordex 8614
[Mendelson] p. 275Proposition 4.42(d)entri3 10628
[Mendelson] p. 281Definitiondf-r1 9833
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9882
[Mendelson] p. 287Axiom system MKru 3802
[MertziosUnger] p. 152Definitiondf-frgr 30291
[MertziosUnger] p. 153Remark 1frgrconngr 30326
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30328  vdgn1frgrv3 30329
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30330
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30323
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30316  2pthfrgrrn 30314  2pthfrgrrn2 30315
[Mittelstaedt] p. 9Definitiondf-oc 31284
[Monk1] p. 22Remarkconventions 30432
[Monk1] p. 22Theorem 3.1conventions 30432
[Monk1] p. 26Theorem 2.8(vii)ssin 4260
[Monk1] p. 33Theorem 3.2(i)ssrel 5806  ssrelf 32637
[Monk1] p. 33Theorem 3.2(ii)eqrel 5808
[Monk1] p. 34Definition 3.3df-opab 5229
[Monk1] p. 36Theorem 3.7(i)coi1 6293  coi2 6294
[Monk1] p. 36Theorem 3.8(v)dm0 5945  rn0 5950
[Monk1] p. 36Theorem 3.7(ii)cnvi 6173
[Monk1] p. 37Theorem 3.13(i)relxp 5718
[Monk1] p. 37Theorem 3.13(x)dmxp 5953  rnxp 6201
[Monk1] p. 37Theorem 3.13(ii)0xp 5798  xp0 6189
[Monk1] p. 38Theorem 3.16(ii)ima0 6106
[Monk1] p. 38Theorem 3.16(viii)imai 6103
[Monk1] p. 39Theorem 3.17imaex 7954  imaexALTV 38286  imaexg 7953
[Monk1] p. 39Theorem 3.16(xi)imassrn 6100
[Monk1] p. 41Theorem 4.3(i)fnopfv 7109  funfvop 7083
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6976
[Monk1] p. 42Theorem 4.4(iii)fvelima 6987
[Monk1] p. 43Theorem 4.6funun 6624
[Monk1] p. 43Theorem 4.8(iv)dff13 7292  dff13f 7293
[Monk1] p. 46Theorem 4.15(v)funex 7256  funrnex 7994
[Monk1] p. 50Definition 5.4fniunfv 7284
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6258
[Monk1] p. 52Theorem 5.11(viii)ssint 4988
[Monk1] p. 52Definition 5.13 (i)1stval2 8047  df-1st 8030
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8048  df-2nd 8031
[Monk1] p. 112Theorem 15.17(v)ranksn 9923  ranksnb 9896
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9924
[Monk1] p. 112Theorem 15.17(iii)rankun 9925  rankunb 9919
[Monk1] p. 113Theorem 15.18r1val3 9907
[Monk1] p. 113Definition 15.19df-r1 9833  r1val2 9906
[Monk1] p. 117Lemmazorn2 10575  zorn2g 10572
[Monk1] p. 133Theorem 18.11cardom 10055
[Monk1] p. 133Theorem 18.12canth3 10630
[Monk1] p. 133Theorem 18.14carduni 10050
[Monk2] p. 105Axiom C4ax-4 1807
[Monk2] p. 105Axiom C7ax-7 2007
[Monk2] p. 105Axiom C8ax-12 2178  ax-c15 38845  ax12v2 2180
[Monk2] p. 108Lemma 5ax-c4 38840
[Monk2] p. 109Lemma 12ax-11 2158
[Monk2] p. 109Lemma 15equvini 2463  equvinv 2028  eqvinop 5507
[Monk2] p. 113Axiom C5-1ax-5 1909  ax5ALT 38863
[Monk2] p. 113Axiom C5-2ax-10 2141
[Monk2] p. 113Axiom C5-3ax-11 2158
[Monk2] p. 114Lemma 21sp 2184
[Monk2] p. 114Lemma 22axc4 2325  hba1-o 38853  hba1 2297
[Monk2] p. 114Lemma 23nfia1 2154
[Monk2] p. 114Lemma 24nfa2 2177  nfra2 3384  nfra2w 3305
[Moore] p. 53Part Idf-mre 17644
[Munkres] p. 77Example 2distop 23023  indistop 23030  indistopon 23029
[Munkres] p. 77Example 3fctop 23032  fctop2 23033
[Munkres] p. 77Example 4cctop 23034
[Munkres] p. 78Definition of basisdf-bases 22974  isbasis3g 22977
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17503  tgval2 22984
[Munkres] p. 79Remarktgcl 22997
[Munkres] p. 80Lemma 2.1tgval3 22991
[Munkres] p. 80Lemma 2.2tgss2 23015  tgss3 23014
[Munkres] p. 81Lemma 2.3basgen 23016  basgen2 23017
[Munkres] p. 83Exercise 3topdifinf 37315  topdifinfeq 37316  topdifinffin 37314  topdifinfindis 37312
[Munkres] p. 89Definition of subspace topologyresttop 23189
[Munkres] p. 93Theorem 6.1(1)0cld 23067  topcld 23064
[Munkres] p. 93Theorem 6.1(2)iincld 23068
[Munkres] p. 93Theorem 6.1(3)uncld 23070
[Munkres] p. 94Definition of closureclsval 23066
[Munkres] p. 94Definition of interiorntrval 23065
[Munkres] p. 95Theorem 6.5(a)clsndisj 23104  elcls 23102
[Munkres] p. 95Theorem 6.5(b)elcls3 23112
[Munkres] p. 97Theorem 6.6clslp 23177  neindisj 23146
[Munkres] p. 97Corollary 6.7cldlp 23179
[Munkres] p. 97Definition of limit pointislp2 23174  lpval 23168
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23344
[Munkres] p. 102Definition of continuous functiondf-cn 23256  iscn 23264  iscn2 23267
[Munkres] p. 107Theorem 7.2(g)cncnp 23309  cncnp2 23310  cncnpi 23307  df-cnp 23257  iscnp 23266  iscnp2 23268
[Munkres] p. 127Theorem 10.1metcn 24577
[Munkres] p. 128Theorem 10.3metcn4 25364
[Nathanson] p. 123Remarkreprgt 34598  reprinfz1 34599  reprlt 34596
[Nathanson] p. 123Definitiondf-repr 34586
[Nathanson] p. 123Chapter 5.1circlemethnat 34618
[Nathanson] p. 123Propositionbreprexp 34610  breprexpnat 34611  itgexpif 34583
[NielsenChuang] p. 195Equation 4.73unierri 32136
[OeSilva] p. 2042Section 2ax-bgbltosilva 47684
[Pfenning] p. 17Definition XMnatded 30435
[Pfenning] p. 17Definition NNCnatded 30435  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30435
[Pfenning] p. 18Rule"natded 30435
[Pfenning] p. 18Definition /\Inatded 30435
[Pfenning] p. 18Definition ` `Enatded 30435  natded 30435  natded 30435  natded 30435  natded 30435
[Pfenning] p. 18Definition ` `Inatded 30435  natded 30435  natded 30435  natded 30435  natded 30435
[Pfenning] p. 18Definition ` `ELnatded 30435
[Pfenning] p. 18Definition ` `ERnatded 30435
[Pfenning] p. 18Definition ` `Ea,unatded 30435
[Pfenning] p. 18Definition ` `IRnatded 30435
[Pfenning] p. 18Definition ` `Ianatded 30435
[Pfenning] p. 127Definition =Enatded 30435
[Pfenning] p. 127Definition =Inatded 30435
[Ponnusamy] p. 361Theorem 6.44cphip0l 25255  df-dip 30733  dip0l 30750  ip0l 21677
[Ponnusamy] p. 361Equation 6.45cphipval 25296  ipval 30735
[Ponnusamy] p. 362Equation I1dipcj 30746  ipcj 21675
[Ponnusamy] p. 362Equation I3cphdir 25258  dipdir 30874  ipdir 21680  ipdiri 30862
[Ponnusamy] p. 362Equation I4ipidsq 30742  nmsq 25247
[Ponnusamy] p. 362Equation 6.46ip0i 30857
[Ponnusamy] p. 362Equation 6.47ip1i 30859
[Ponnusamy] p. 362Equation 6.48ip2i 30860
[Ponnusamy] p. 363Equation I2cphass 25264  dipass 30877  ipass 21686  ipassi 30873
[Prugovecki] p. 186Definition of brabraval 31976  df-bra 31882
[Prugovecki] p. 376Equation 8.1df-kb 31883  kbval 31986
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32414
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39845
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32428  atcvat4i 32429  cvrat3 39399  cvrat4 39400  lsatcvat3 39008
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32314  cvrval 39225  df-cv 32311  df-lcv 38975  lspsncv0 21171
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39857
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39858
[Quine] p. 16Definition 2.1df-clab 2718  rabid 3465  rabidd 45060
[Quine] p. 17Definition 2.1''dfsb7 2283
[Quine] p. 18Definition 2.7df-cleq 2732
[Quine] p. 19Definition 2.9conventions 30432  df-v 3490
[Quine] p. 34Theorem 5.1eqabb 2884
[Quine] p. 35Theorem 5.2abid1 2881  abid2f 2942
[Quine] p. 40Theorem 6.1sb5 2277
[Quine] p. 40Theorem 6.2sb6 2085  sbalex 2243
[Quine] p. 41Theorem 6.3df-clel 2819
[Quine] p. 41Theorem 6.4eqid 2740  eqid1 30499
[Quine] p. 41Theorem 6.5eqcom 2747
[Quine] p. 42Theorem 6.6df-sbc 3805
[Quine] p. 42Theorem 6.7dfsbcq 3806  dfsbcq2 3807
[Quine] p. 43Theorem 6.8vex 3492
[Quine] p. 43Theorem 6.9isset 3502
[Quine] p. 44Theorem 7.3spcgf 3604  spcgv 3609  spcimgf 3562
[Quine] p. 44Theorem 6.11spsbc 3817  spsbcd 3818
[Quine] p. 44Theorem 6.12elex 3509
[Quine] p. 44Theorem 6.13elab 3694  elabg 3690  elabgf 3688
[Quine] p. 44Theorem 6.14noel 4360
[Quine] p. 48Theorem 7.2snprc 4742
[Quine] p. 48Definition 7.1df-pr 4651  df-sn 4649
[Quine] p. 49Theorem 7.4snss 4810  snssg 4808
[Quine] p. 49Theorem 7.5prss 4845  prssg 4844
[Quine] p. 49Theorem 7.6prid1 4787  prid1g 4785  prid2 4788  prid2g 4786  snid 4684  snidg 4682
[Quine] p. 51Theorem 7.12snex 5451
[Quine] p. 51Theorem 7.13prex 5452
[Quine] p. 53Theorem 8.2unisn 4950  unisnALT 44897  unisng 4949
[Quine] p. 53Theorem 8.3uniun 4954
[Quine] p. 54Theorem 8.6elssuni 4961
[Quine] p. 54Theorem 8.7uni0 4959
[Quine] p. 56Theorem 8.17uniabio 6540
[Quine] p. 56Definition 8.18dfaiota2 47001  dfiota2 6526
[Quine] p. 57Theorem 8.19aiotaval 47010  iotaval 6544
[Quine] p. 57Theorem 8.22iotanul 6551
[Quine] p. 58Theorem 8.23iotaex 6546
[Quine] p. 58Definition 9.1df-op 4655
[Quine] p. 61Theorem 9.5opabid 5544  opabidw 5543  opelopab 5561  opelopaba 5555  opelopabaf 5563  opelopabf 5564  opelopabg 5557  opelopabga 5552  opelopabgf 5559  oprabid 7480  oprabidw 7479
[Quine] p. 64Definition 9.11df-xp 5706
[Quine] p. 64Definition 9.12df-cnv 5708
[Quine] p. 64Definition 9.15df-id 5593
[Quine] p. 65Theorem 10.3fun0 6643
[Quine] p. 65Theorem 10.4funi 6610
[Quine] p. 65Theorem 10.5funsn 6631  funsng 6629
[Quine] p. 65Definition 10.1df-fun 6575
[Quine] p. 65Definition 10.2args 6122  dffv4 6917
[Quine] p. 68Definition 10.11conventions 30432  df-fv 6581  fv2 6915
[Quine] p. 124Theorem 17.3nn0opth2 14321  nn0opth2i 14320  nn0opthi 14319  omopthi 8717
[Quine] p. 177Definition 25.2df-rdg 8466
[Quine] p. 232Equation icarddom 10623
[Quine] p. 284Axiom 39(vi)funimaex 6666  funimaexg 6664
[Quine] p. 331Axiom system NFru 3802
[ReedSimon] p. 36Definition (iii)ax-his3 31116
[ReedSimon] p. 63Exercise 4(a)df-dip 30733  polid 31191  polid2i 31189  polidi 31190
[ReedSimon] p. 63Exercise 4(b)df-ph 30845
[ReedSimon] p. 195Remarklnophm 32051  lnophmi 32050
[Retherford] p. 49Exercise 1(i)leopadd 32164
[Retherford] p. 49Exercise 1(ii)leopmul 32166  leopmuli 32165
[Retherford] p. 49Exercise 1(iv)leoptr 32169
[Retherford] p. 49Definition VI.1df-leop 31884  leoppos 32158
[Retherford] p. 49Exercise 1(iii)leoptri 32168
[Retherford] p. 49Definition of operator orderingleop3 32157
[Roman] p. 4Definitiondf-dmat 22517  df-dmatalt 48127
[Roman] p. 18Part Preliminariesdf-rng 20180
[Roman] p. 19Part Preliminariesdf-ring 20262
[Roman] p. 46Theorem 1.6isldepslvec2 48214
[Roman] p. 112Noteisldepslvec2 48214  ldepsnlinc 48237  zlmodzxznm 48226
[Roman] p. 112Examplezlmodzxzequa 48225  zlmodzxzequap 48228  zlmodzxzldep 48233
[Roman] p. 170Theorem 7.8cayleyhamilton 22917
[Rosenlicht] p. 80Theoremheicant 37615
[Rosser] p. 281Definitiondf-op 4655
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34622
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34623
[Rotman] p. 28Remarkpgrpgt2nabl 48091  pmtr3ncom 19517
[Rotman] p. 31Theorem 3.4symggen2 19513
[Rotman] p. 42Theorem 3.15cayley 19456  cayleyth 19457
[Rudin] p. 164Equation 27efcan 16144
[Rudin] p. 164Equation 30efzval 16150
[Rudin] p. 167Equation 48absefi 16244
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1769
[Sanford] p. 39Rule 4mptxor 1767
[Sanford] p. 40Rule 1mptnan 1766
[Schechter] p. 51Definition of antisymmetryintasym 6147
[Schechter] p. 51Definition of irreflexivityintirr 6150
[Schechter] p. 51Definition of symmetrycnvsym 6144
[Schechter] p. 51Definition of transitivitycotr 6142
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17644
[Schechter] p. 79Definition of Moore closuredf-mrc 17645
[Schechter] p. 82Section 4.5df-mrc 17645
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17647
[Schechter] p. 139Definition AC3dfac9 10206
[Schechter] p. 141Definition (MC)dfac11 43019
[Schechter] p. 149Axiom DC1ax-dc 10515  axdc3 10523
[Schechter] p. 187Definition of "ring with unit"isring 20264  isrngo 37857
[Schechter] p. 276Remark 11.6.espan0 31574
[Schechter] p. 276Definition of spandf-span 31341  spanval 31365
[Schechter] p. 428Definition 15.35bastop1 23021
[Schloeder] p. 1Lemma 1.3onelon 6420  onelord 43212  ordelon 6419  ordelord 6417
[Schloeder] p. 1Lemma 1.7onepsuc 43213  sucidg 6476
[Schloeder] p. 1Remark 1.50elon 6449  onsuc 7847  ord0 6448  ordsuci 7844
[Schloeder] p. 1Theorem 1.9epsoon 43214
[Schloeder] p. 1Definition 1.1dftr5 5287
[Schloeder] p. 1Definition 1.2dford3 42985  elon2 6406
[Schloeder] p. 1Definition 1.4df-suc 6401
[Schloeder] p. 1Definition 1.6epel 5602  epelg 5600
[Schloeder] p. 1Theorem 1.9(i)elirr 9666  epirron 43215  ordirr 6413
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43217  oneptr 43216  ontr1 6441
[Schloeder] p. 1Theorem 1.9(iii)oneltri 43219  oneptri 43218  ordtri3or 6427
[Schloeder] p. 2Lemma 1.10ondif1 8557  ord0eln0 6450
[Schloeder] p. 2Lemma 1.13elsuci 6462  onsucss 43228  trsucss 6483
[Schloeder] p. 2Lemma 1.14ordsucss 7854
[Schloeder] p. 2Lemma 1.15onnbtwn 6489  ordnbtwn 6488
[Schloeder] p. 2Lemma 1.16orddif0suc 43230  ordnexbtwnsuc 43229
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10470  onsucf1lem 43231  onsucf1o 43234  onsucf1olem 43232  onsucrn 43233
[Schloeder] p. 2Lemma 1.18dflim7 43235
[Schloeder] p. 2Remark 1.12ordzsl 7882
[Schloeder] p. 2Theorem 1.10ondif1i 43224  ordne0gt0 43223
[Schloeder] p. 2Definition 1.11dflim6 43226  limnsuc 43227  onsucelab 43225
[Schloeder] p. 3Remark 1.21omex 9712
[Schloeder] p. 3Theorem 1.19tfinds 7897
[Schloeder] p. 3Theorem 1.22omelon 9715  ordom 7913
[Schloeder] p. 3Definition 1.20dfom3 9716
[Schloeder] p. 4Lemma 2.21onn 8696
[Schloeder] p. 4Lemma 2.7ssonuni 7815  ssorduni 7814
[Schloeder] p. 4Remark 2.4oa1suc 8587
[Schloeder] p. 4Theorem 1.23dfom5 9719  limom 7919
[Schloeder] p. 4Definition 2.1df-1o 8522  df1o2 8529
[Schloeder] p. 4Definition 2.3oa0 8572  oa0suclim 43237  oalim 8588  oasuc 8580
[Schloeder] p. 4Definition 2.5om0 8573  om0suclim 43238  omlim 8589  omsuc 8582
[Schloeder] p. 4Definition 2.6oe0 8578  oe0m1 8577  oe0suclim 43239  oelim 8590  oesuc 8583
[Schloeder] p. 5Lemma 2.10onsupuni 43190
[Schloeder] p. 5Lemma 2.11onsupsucismax 43241
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43242
[Schloeder] p. 5Lemma 2.13limexissup 43243  limexissupab 43245  limiun 43244  limuni 6456
[Schloeder] p. 5Lemma 2.14oa0r 8594
[Schloeder] p. 5Lemma 2.15om1 8598  om1om1r 43246  om1r 8599
[Schloeder] p. 5Remark 2.8oacl 8591  oaomoecl 43240  oecl 8593  omcl 8592
[Schloeder] p. 5Definition 2.9onsupintrab 43192
[Schloeder] p. 6Lemma 2.16oe1 8600
[Schloeder] p. 6Lemma 2.17oe1m 8601
[Schloeder] p. 6Lemma 2.18oe0rif 43247
[Schloeder] p. 6Theorem 2.19oasubex 43248
[Schloeder] p. 6Theorem 2.20nnacl 8667  nnamecl 43249  nnecl 8669  nnmcl 8668
[Schloeder] p. 7Lemma 3.1onsucwordi 43250
[Schloeder] p. 7Lemma 3.2oaword1 8608
[Schloeder] p. 7Lemma 3.3oaword2 8609
[Schloeder] p. 7Lemma 3.4oalimcl 8616
[Schloeder] p. 7Lemma 3.5oaltublim 43252
[Schloeder] p. 8Lemma 3.6oaordi3 43253
[Schloeder] p. 8Lemma 3.81oaomeqom 43255
[Schloeder] p. 8Lemma 3.10oa00 8615
[Schloeder] p. 8Lemma 3.11omge1 43259  omword1 8629
[Schloeder] p. 8Remark 3.9oaordnr 43258  oaordnrex 43257
[Schloeder] p. 8Theorem 3.7oaord3 43254
[Schloeder] p. 9Lemma 3.12omge2 43260  omword2 8630
[Schloeder] p. 9Lemma 3.13omlim2 43261
[Schloeder] p. 9Lemma 3.14omord2lim 43262
[Schloeder] p. 9Lemma 3.15omord2i 43263  omordi 8622
[Schloeder] p. 9Theorem 3.16omord 8624  omord2com 43264
[Schloeder] p. 10Lemma 3.172omomeqom 43265  df-2o 8523
[Schloeder] p. 10Lemma 3.19oege1 43268  oewordi 8647
[Schloeder] p. 10Lemma 3.20oege2 43269  oeworde 8649
[Schloeder] p. 10Lemma 3.21rp-oelim2 43270
[Schloeder] p. 10Lemma 3.22oeord2lim 43271
[Schloeder] p. 10Remark 3.18omnord1 43267  omnord1ex 43266
[Schloeder] p. 11Lemma 3.23oeord2i 43272
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43274
[Schloeder] p. 11Remark 3.26oenord1 43278  oenord1ex 43277
[Schloeder] p. 11Theorem 4.1oaomoencom 43279
[Schloeder] p. 11Theorem 4.2oaass 8617
[Schloeder] p. 11Theorem 3.24oeord2com 43273
[Schloeder] p. 12Theorem 4.3odi 8635
[Schloeder] p. 13Theorem 4.4omass 8636
[Schloeder] p. 14Remark 4.6oenass 43281
[Schloeder] p. 14Theorem 4.7oeoa 8653
[Schloeder] p. 15Lemma 5.1cantnftermord 43282
[Schloeder] p. 15Lemma 5.2cantnfub 43283  cantnfub2 43284
[Schloeder] p. 16Theorem 5.3cantnf2 43287
[Schwabhauser] p. 10Axiom A1axcgrrflx 28947  axtgcgrrflx 28488
[Schwabhauser] p. 10Axiom A2axcgrtr 28948
[Schwabhauser] p. 10Axiom A3axcgrid 28949  axtgcgrid 28489
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28474
[Schwabhauser] p. 11Axiom A4axsegcon 28960  axtgsegcon 28490  df-trkgcb 28476
[Schwabhauser] p. 11Axiom A5ax5seg 28971  axtg5seg 28491  df-trkgcb 28476
[Schwabhauser] p. 11Axiom A6axbtwnid 28972  axtgbtwnid 28492  df-trkgb 28475
[Schwabhauser] p. 12Axiom A7axpasch 28974  axtgpasch 28493  df-trkgb 28475
[Schwabhauser] p. 12Axiom A8axlowdim2 28993  df-trkg2d 34642
[Schwabhauser] p. 13Axiom A8axtglowdim2 28496
[Schwabhauser] p. 13Axiom A9axtgupdim2 28497  df-trkg2d 34642
[Schwabhauser] p. 13Axiom A10axeuclid 28996  axtgeucl 28498  df-trkge 28477
[Schwabhauser] p. 13Axiom A11axcont 29009  axtgcont 28495  axtgcont1 28494  df-trkgb 28475
[Schwabhauser] p. 27Theorem 2.1cgrrflx 35951
[Schwabhauser] p. 27Theorem 2.2cgrcomim 35953
[Schwabhauser] p. 27Theorem 2.3cgrtr 35956
[Schwabhauser] p. 27Theorem 2.4cgrcoml 35960
[Schwabhauser] p. 27Theorem 2.5cgrcomr 35961  tgcgrcomimp 28503  tgcgrcoml 28505  tgcgrcomr 28504
[Schwabhauser] p. 28Theorem 2.8cgrtriv 35966  tgcgrtriv 28510
[Schwabhauser] p. 28Theorem 2.105segofs 35970  tg5segofs 34650
[Schwabhauser] p. 28Definition 2.10df-afs 34647  df-ofs 35947
[Schwabhauser] p. 29Theorem 2.11cgrextend 35972  tgcgrextend 28511
[Schwabhauser] p. 29Theorem 2.12segconeq 35974  tgsegconeq 28512
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 35986  btwntriv2 35976  tgbtwntriv2 28513
[Schwabhauser] p. 30Theorem 3.2btwncomim 35977  tgbtwncom 28514
[Schwabhauser] p. 30Theorem 3.3btwntriv1 35980  tgbtwntriv1 28517
[Schwabhauser] p. 30Theorem 3.4btwnswapid 35981  tgbtwnswapid 28518
[Schwabhauser] p. 30Theorem 3.5btwnexch2 35987  btwnintr 35983  tgbtwnexch2 28522  tgbtwnintr 28519
[Schwabhauser] p. 30Theorem 3.6btwnexch 35989  btwnexch3 35984  tgbtwnexch 28524  tgbtwnexch3 28520
[Schwabhauser] p. 30Theorem 3.7btwnouttr 35988  tgbtwnouttr 28523  tgbtwnouttr2 28521
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28992
[Schwabhauser] p. 32Theorem 3.14btwndiff 35991  tgbtwndiff 28532
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28525  trisegint 35992
[Schwabhauser] p. 34Theorem 4.2ifscgr 36008  tgifscgr 28534
[Schwabhauser] p. 34Theorem 4.11colcom 28584  colrot1 28585  colrot2 28586  lncom 28648  lnrot1 28649  lnrot2 28650
[Schwabhauser] p. 34Definition 4.1df-ifs 36004
[Schwabhauser] p. 35Theorem 4.3cgrsub 36009  tgcgrsub 28535
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36019  tgcgrxfr 28544
[Schwabhauser] p. 35Statement 4.4ercgrg 28543
[Schwabhauser] p. 35Definition 4.4df-cgr3 36005  df-cgrg 28537
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28537
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36020  tgbtwnxfr 28556
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36026  colinearperm2 36028  colinearperm3 36027  colinearperm4 36029  colinearperm5 36030
[Schwabhauser] p. 36Definition 4.8df-ismt 28559
[Schwabhauser] p. 36Definition 4.10df-colinear 36003  tgellng 28579  tglng 28572
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36031
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36039  lnxfr 28592
[Schwabhauser] p. 37Theorem 4.14lineext 36040  lnext 28593
[Schwabhauser] p. 37Theorem 4.16fscgr 36044  tgfscgr 28594
[Schwabhauser] p. 37Theorem 4.17linecgr 36045  lncgr 28595
[Schwabhauser] p. 37Definition 4.15df-fs 36006
[Schwabhauser] p. 38Theorem 4.18lineid 36047  lnid 28596
[Schwabhauser] p. 38Theorem 4.19idinside 36048  tgidinside 28597
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36065  tgbtwnconn1 28601
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36066  tgbtwnconn2 28602
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36067  tgbtwnconn3 28603
[Schwabhauser] p. 41Theorem 5.5brsegle2 36073
[Schwabhauser] p. 41Definition 5.4df-segle 36071  legov 28611
[Schwabhauser] p. 41Definition 5.5legov2 28612
[Schwabhauser] p. 42Remark 5.13legso 28625
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36074
[Schwabhauser] p. 42Theorem 5.7seglerflx 36076
[Schwabhauser] p. 42Theorem 5.8segletr 36078
[Schwabhauser] p. 42Theorem 5.9segleantisym 36079
[Schwabhauser] p. 42Theorem 5.10seglelin 36080
[Schwabhauser] p. 42Theorem 5.11seglemin 36077
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36082
[Schwabhauser] p. 42Proposition 5.7legid 28613
[Schwabhauser] p. 42Proposition 5.8legtrd 28615
[Schwabhauser] p. 42Proposition 5.9legtri3 28616
[Schwabhauser] p. 42Proposition 5.10legtrid 28617
[Schwabhauser] p. 42Proposition 5.11leg0 28618
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36089
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36090
[Schwabhauser] p. 43Theorem 6.4broutsideof 36085  df-outsideof 36084
[Schwabhauser] p. 43Definition 6.1broutsideof2 36086  ishlg 28628
[Schwabhauser] p. 44Theorem 6.4hlln 28633
[Schwabhauser] p. 44Theorem 6.5hlid 28635  outsideofrflx 36091
[Schwabhauser] p. 44Theorem 6.6hlcomb 28629  hlcomd 28630  outsideofcom 36092
[Schwabhauser] p. 44Theorem 6.7hltr 28636  outsideoftr 36093
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28644  outsideofeu 36095
[Schwabhauser] p. 44Definition 6.8df-ray 36102
[Schwabhauser] p. 45Part 2df-lines2 36103
[Schwabhauser] p. 45Theorem 6.13outsidele 36096
[Schwabhauser] p. 45Theorem 6.15lineunray 36111
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36112  tglineelsb2 28658
[Schwabhauser] p. 45Theorem 6.17linecom 36114  linerflx1 36113  linerflx2 36115  tglinecom 28661  tglinerflx1 28659  tglinerflx2 28660
[Schwabhauser] p. 45Theorem 6.18linethru 36117  tglinethru 28662
[Schwabhauser] p. 45Definition 6.14df-line2 36101  tglng 28572
[Schwabhauser] p. 45Proposition 6.13legbtwn 28620
[Schwabhauser] p. 46Theorem 6.19linethrueu 36120  tglinethrueu 28665
[Schwabhauser] p. 46Theorem 6.21lineintmo 36121  tglineineq 28669  tglineinteq 28671  tglineintmo 28668
[Schwabhauser] p. 46Theorem 6.23colline 28675
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28676
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28677
[Schwabhauser] p. 49Theorem 7.3mirinv 28692
[Schwabhauser] p. 49Theorem 7.7mirmir 28688
[Schwabhauser] p. 49Theorem 7.8mirreu3 28680
[Schwabhauser] p. 49Definition 7.5df-mir 28679  ismir 28685  mirbtwn 28684  mircgr 28683  mirfv 28682  mirval 28681
[Schwabhauser] p. 50Theorem 7.8mirreu 28690
[Schwabhauser] p. 50Theorem 7.9mireq 28691
[Schwabhauser] p. 50Theorem 7.10mirinv 28692
[Schwabhauser] p. 50Theorem 7.11mirf1o 28695
[Schwabhauser] p. 50Theorem 7.13miriso 28696
[Schwabhauser] p. 51Theorem 7.14mirmot 28701
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28698  mirbtwni 28697
[Schwabhauser] p. 51Theorem 7.16mircgrs 28699
[Schwabhauser] p. 51Theorem 7.17miduniq 28711
[Schwabhauser] p. 52Lemma 7.21symquadlem 28715
[Schwabhauser] p. 52Theorem 7.18miduniq1 28712
[Schwabhauser] p. 52Theorem 7.19miduniq2 28713
[Schwabhauser] p. 52Theorem 7.20colmid 28714
[Schwabhauser] p. 53Lemma 7.22krippen 28717
[Schwabhauser] p. 55Lemma 7.25midexlem 28718
[Schwabhauser] p. 57Theorem 8.2ragcom 28724
[Schwabhauser] p. 57Definition 8.1df-rag 28720  israg 28723
[Schwabhauser] p. 58Theorem 8.3ragcol 28725
[Schwabhauser] p. 58Theorem 8.4ragmir 28726
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28728
[Schwabhauser] p. 58Theorem 8.6ragflat2 28729
[Schwabhauser] p. 58Theorem 8.7ragflat 28730
[Schwabhauser] p. 58Theorem 8.8ragtriva 28731
[Schwabhauser] p. 58Theorem 8.9ragflat3 28732  ragncol 28735
[Schwabhauser] p. 58Theorem 8.10ragcgr 28733
[Schwabhauser] p. 59Theorem 8.12perpcom 28739
[Schwabhauser] p. 59Theorem 8.13ragperp 28743
[Schwabhauser] p. 59Theorem 8.14perpneq 28740
[Schwabhauser] p. 59Definition 8.11df-perpg 28722  isperp 28738
[Schwabhauser] p. 59Definition 8.13isperp2 28741
[Schwabhauser] p. 60Theorem 8.18foot 28748
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28756  colperpexlem2 28757
[Schwabhauser] p. 63Theorem 8.21colperpex 28759  colperpexlem3 28758
[Schwabhauser] p. 64Theorem 8.22mideu 28764  midex 28763
[Schwabhauser] p. 66Lemma 8.24opphllem 28761
[Schwabhauser] p. 67Theorem 9.2oppcom 28770
[Schwabhauser] p. 67Definition 9.1islnopp 28765
[Schwabhauser] p. 68Lemma 9.3opphllem2 28774
[Schwabhauser] p. 68Lemma 9.4opphllem5 28777  opphllem6 28778
[Schwabhauser] p. 69Theorem 9.5opphl 28780
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28493
[Schwabhauser] p. 70Theorem 9.6outpasch 28781
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28789
[Schwabhauser] p. 71Definition 9.7df-hpg 28784  hpgbr 28786
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28791
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28790
[Schwabhauser] p. 72Theorem 9.11hpgid 28792
[Schwabhauser] p. 72Theorem 9.12hpgcom 28793
[Schwabhauser] p. 72Theorem 9.13hpgtr 28794
[Schwabhauser] p. 73Theorem 9.18colopp 28795
[Schwabhauser] p. 73Theorem 9.19colhp 28796
[Schwabhauser] p. 88Theorem 10.2lmieu 28810
[Schwabhauser] p. 88Definition 10.1df-mid 28800
[Schwabhauser] p. 89Theorem 10.4lmicom 28814
[Schwabhauser] p. 89Theorem 10.5lmilmi 28815
[Schwabhauser] p. 89Theorem 10.6lmireu 28816
[Schwabhauser] p. 89Theorem 10.7lmieq 28817
[Schwabhauser] p. 89Theorem 10.8lmiinv 28818
[Schwabhauser] p. 89Theorem 10.9lmif1o 28821
[Schwabhauser] p. 89Theorem 10.10lmiiso 28823
[Schwabhauser] p. 89Definition 10.3df-lmi 28801
[Schwabhauser] p. 90Theorem 10.11lmimot 28824
[Schwabhauser] p. 91Theorem 10.12hypcgr 28827
[Schwabhauser] p. 92Theorem 10.14lmiopp 28828
[Schwabhauser] p. 92Theorem 10.15lnperpex 28829
[Schwabhauser] p. 92Theorem 10.16trgcopy 28830  trgcopyeu 28832
[Schwabhauser] p. 95Definition 11.2dfcgra2 28856
[Schwabhauser] p. 95Definition 11.3iscgra 28835
[Schwabhauser] p. 95Proposition 11.4cgracgr 28844
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28842  cgrahl2 28843
[Schwabhauser] p. 96Theorem 11.6cgraid 28845
[Schwabhauser] p. 96Theorem 11.9cgraswap 28846
[Schwabhauser] p. 97Theorem 11.7cgracom 28848
[Schwabhauser] p. 97Theorem 11.8cgratr 28849
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28852  cgrahl 28853
[Schwabhauser] p. 98Theorem 11.13sacgr 28857
[Schwabhauser] p. 98Theorem 11.14oacgr 28858
[Schwabhauser] p. 98Theorem 11.15acopy 28859  acopyeu 28860
[Schwabhauser] p. 101Theorem 11.24inagswap 28867
[Schwabhauser] p. 101Theorem 11.25inaghl 28871
[Schwabhauser] p. 101Definition 11.23isinag 28864
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28879
[Schwabhauser] p. 102Definition 11.27df-leag 28872  isleag 28873
[Schwabhauser] p. 107Theorem 11.49tgsas 28881  tgsas1 28880  tgsas2 28882  tgsas3 28883
[Schwabhauser] p. 108Theorem 11.50tgasa 28885  tgasa1 28884
[Schwabhauser] p. 109Theorem 11.51tgsss1 28886  tgsss2 28887  tgsss3 28888
[Shapiro] p. 230Theorem 6.5.1dchrhash 27333  dchrsum 27331  dchrsum2 27330  sumdchr 27334
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27335  sum2dchr 27336
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20110  ablfacrp2 20111
[Shapiro], p. 328Equation 9.2.4vmasum 27278
[Shapiro], p. 329Equation 9.2.7logfac2 27279
[Shapiro], p. 329Equation 9.2.9logfacrlim 27286
[Shapiro], p. 331Equation 9.2.13vmadivsum 27544
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27547
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27601  vmalogdivsum2 27600
[Shapiro], p. 375Theorem 9.4.1dirith 27591  dirith2 27590
[Shapiro], p. 375Equation 9.4.3rplogsum 27589  rpvmasum 27588  rpvmasum2 27574
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27549
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27587
[Shapiro], p. 377Lemma 9.4.1dchrisum 27554  dchrisumlem1 27551  dchrisumlem2 27552  dchrisumlem3 27553  dchrisumlema 27550
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27557
[Shapiro], p. 379Equation 9.4.16dchrmusum 27586  dchrmusumlem 27584  dchrvmasumlem 27585
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27556
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27558
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27582  dchrisum0re 27575  dchrisumn0 27583
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27568
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27572
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27573
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27628  pntrsumbnd2 27629  pntrsumo1 27627
[Shapiro], p. 405Equation 10.2.1mudivsum 27592
[Shapiro], p. 406Equation 10.2.6mulogsum 27594
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27596
[Shapiro], p. 407Equation 10.2.8mulog2sum 27599
[Shapiro], p. 418Equation 10.4.6logsqvma 27604
[Shapiro], p. 418Equation 10.4.8logsqvma2 27605
[Shapiro], p. 419Equation 10.4.10selberg 27610
[Shapiro], p. 420Equation 10.4.12selberg2lem 27612
[Shapiro], p. 420Equation 10.4.14selberg2 27613
[Shapiro], p. 422Equation 10.6.7selberg3 27621
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27622
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27619  selberg3lem2 27620
[Shapiro], p. 422Equation 10.4.23selberg4 27623
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27617
[Shapiro], p. 428Equation 10.6.2selbergr 27630
[Shapiro], p. 429Equation 10.6.8selberg3r 27631
[Shapiro], p. 430Equation 10.6.11selberg4r 27632
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27646
[Shapiro], p. 434Equation 10.6.27pntlema 27658  pntlemb 27659  pntlemc 27657  pntlemd 27656  pntlemg 27660
[Shapiro], p. 435Equation 10.6.29pntlema 27658
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27650
[Shapiro], p. 436Lemma 10.6.2pntibnd 27655
[Shapiro], p. 436Equation 10.6.34pntlema 27658
[Shapiro], p. 436Equation 10.6.35pntlem3 27671  pntleml 27673
[Stoll] p. 13Definition corresponds to dfsymdif3 4325
[Stoll] p. 16Exercise 4.40dif 4428  dif0 4400
[Stoll] p. 16Exercise 4.8difdifdir 4515
[Stoll] p. 17Theorem 5.1(5)unvdif 4498
[Stoll] p. 19Theorem 5.2(13)undm 4316
[Stoll] p. 19Theorem 5.2(13')indm 4317
[Stoll] p. 20Remarkinvdif 4298
[Stoll] p. 25Definition of ordered tripledf-ot 4657
[Stoll] p. 43Definitionuniiun 5081
[Stoll] p. 44Definitionintiin 5082
[Stoll] p. 45Definitiondf-iin 5018
[Stoll] p. 45Definition indexed uniondf-iun 5017
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4325
[Strang] p. 242Section 6.3expgrowth 44304
[Suppes] p. 22Theorem 2eq0 4373  eq0f 4370
[Suppes] p. 22Theorem 4eqss 4024  eqssd 4026  eqssi 4025
[Suppes] p. 23Theorem 5ss0 4425  ss0b 4424
[Suppes] p. 23Theorem 6sstr 4017  sstrALT2 44806
[Suppes] p. 23Theorem 7pssirr 4126
[Suppes] p. 23Theorem 8pssn2lp 4127
[Suppes] p. 23Theorem 9psstr 4130
[Suppes] p. 23Theorem 10pssss 4121
[Suppes] p. 25Theorem 12elin 3992  elun 4176
[Suppes] p. 26Theorem 15inidm 4248
[Suppes] p. 26Theorem 16in0 4418
[Suppes] p. 27Theorem 23unidm 4180
[Suppes] p. 27Theorem 24un0 4417
[Suppes] p. 27Theorem 25ssun1 4201
[Suppes] p. 27Theorem 26ssequn1 4209
[Suppes] p. 27Theorem 27unss 4213
[Suppes] p. 27Theorem 28indir 4305
[Suppes] p. 27Theorem 29undir 4306
[Suppes] p. 28Theorem 32difid 4398
[Suppes] p. 29Theorem 33difin 4291
[Suppes] p. 29Theorem 34indif 4299
[Suppes] p. 29Theorem 35undif1 4499
[Suppes] p. 29Theorem 36difun2 4504
[Suppes] p. 29Theorem 37difin0 4497
[Suppes] p. 29Theorem 38disjdif 4495
[Suppes] p. 29Theorem 39difundi 4309
[Suppes] p. 29Theorem 40difindi 4311
[Suppes] p. 30Theorem 41nalset 5331
[Suppes] p. 39Theorem 61uniss 4939
[Suppes] p. 39Theorem 65uniop 5534
[Suppes] p. 41Theorem 70intsn 5008
[Suppes] p. 42Theorem 71intpr 5006  intprg 5005
[Suppes] p. 42Theorem 73op1stb 5491
[Suppes] p. 42Theorem 78intun 5004
[Suppes] p. 44Definition 15(a)dfiun2 5056  dfiun2g 5053
[Suppes] p. 44Definition 15(b)dfiin2 5057
[Suppes] p. 47Theorem 86elpw 4626  elpw2 5352  elpw2g 5351  elpwg 4625  elpwgdedVD 44888
[Suppes] p. 47Theorem 87pwid 4644
[Suppes] p. 47Theorem 89pw0 4837
[Suppes] p. 48Theorem 90pwpw0 4838
[Suppes] p. 52Theorem 101xpss12 5715
[Suppes] p. 52Theorem 102xpindi 5858  xpindir 5859
[Suppes] p. 52Theorem 103xpundi 5768  xpundir 5769
[Suppes] p. 54Theorem 105elirrv 9665
[Suppes] p. 58Theorem 2relss 5805
[Suppes] p. 59Theorem 4eldm 5925  eldm2 5926  eldm2g 5924  eldmg 5923
[Suppes] p. 59Definition 3df-dm 5710
[Suppes] p. 60Theorem 6dmin 5936
[Suppes] p. 60Theorem 8rnun 6177
[Suppes] p. 60Theorem 9rnin 6178
[Suppes] p. 60Definition 4dfrn2 5913
[Suppes] p. 61Theorem 11brcnv 5907  brcnvg 5904
[Suppes] p. 62Equation 5elcnv 5901  elcnv2 5902
[Suppes] p. 62Theorem 12relcnv 6134
[Suppes] p. 62Theorem 15cnvin 6176
[Suppes] p. 62Theorem 16cnvun 6174
[Suppes] p. 63Definitiondftrrels2 38531
[Suppes] p. 63Theorem 20co02 6291
[Suppes] p. 63Theorem 21dmcoss 5997
[Suppes] p. 63Definition 7df-co 5709
[Suppes] p. 64Theorem 26cnvco 5910
[Suppes] p. 64Theorem 27coass 6296
[Suppes] p. 65Theorem 31resundi 6023
[Suppes] p. 65Theorem 34elima 6094  elima2 6095  elima3 6096  elimag 6093
[Suppes] p. 65Theorem 35imaundi 6181
[Suppes] p. 66Theorem 40dminss 6184
[Suppes] p. 66Theorem 41imainss 6185
[Suppes] p. 67Exercise 11cnvxp 6188
[Suppes] p. 81Definition 34dfec2 8766
[Suppes] p. 82Theorem 72elec 8809  elecALTV 38222  elecg 8807
[Suppes] p. 82Theorem 73eqvrelth 38567  erth 8814  erth2 8815
[Suppes] p. 83Theorem 74eqvreldisj 38570  erdisj 8817
[Suppes] p. 83Definition 35, df-parts 38721  dfmembpart2 38726
[Suppes] p. 89Theorem 96map0b 8941
[Suppes] p. 89Theorem 97map0 8945  map0g 8942
[Suppes] p. 89Theorem 98mapsn 8946  mapsnd 8944
[Suppes] p. 89Theorem 99mapss 8947
[Suppes] p. 91Definition 12(ii)alephsuc 10137
[Suppes] p. 91Definition 12(iii)alephlim 10136
[Suppes] p. 92Theorem 1enref 9045  enrefg 9044
[Suppes] p. 92Theorem 2ensym 9063  ensymb 9062  ensymi 9064
[Suppes] p. 92Theorem 3entr 9066
[Suppes] p. 92Theorem 4unen 9112
[Suppes] p. 94Theorem 15endom 9039
[Suppes] p. 94Theorem 16ssdomg 9060
[Suppes] p. 94Theorem 17domtr 9067
[Suppes] p. 95Theorem 18sbth 9159
[Suppes] p. 97Theorem 23canth2 9196  canth2g 9197
[Suppes] p. 97Definition 3brsdom2 9163  df-sdom 9006  dfsdom2 9162
[Suppes] p. 97Theorem 21(i)sdomirr 9180
[Suppes] p. 97Theorem 22(i)domnsym 9165
[Suppes] p. 97Theorem 21(ii)sdomnsym 9164
[Suppes] p. 97Theorem 22(ii)domsdomtr 9178
[Suppes] p. 97Theorem 22(iv)brdom2 9042
[Suppes] p. 97Theorem 21(iii)sdomtr 9181
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9176
[Suppes] p. 98Exercise 4fundmen 9096  fundmeng 9097
[Suppes] p. 98Exercise 6xpdom3 9136
[Suppes] p. 98Exercise 11sdomentr 9177
[Suppes] p. 104Theorem 37fofi 9379
[Suppes] p. 104Theorem 38pwfi 9385
[Suppes] p. 105Theorem 40pwfi 9385
[Suppes] p. 111Axiom for cardinal numberscarden 10620
[Suppes] p. 130Definition 3df-tr 5284
[Suppes] p. 132Theorem 9ssonuni 7815
[Suppes] p. 134Definition 6df-suc 6401
[Suppes] p. 136Theorem Schema 22findes 7940  finds 7936  finds1 7939  finds2 7938
[Suppes] p. 151Theorem 42isfinite 9721  isfinite2 9362  isfiniteg 9365  unbnn 9360
[Suppes] p. 162Definition 5df-ltnq 10987  df-ltpq 10979
[Suppes] p. 197Theorem Schema 4tfindes 7900  tfinds 7897  tfinds2 7901
[Suppes] p. 209Theorem 18oaord1 8607
[Suppes] p. 209Theorem 21oaword2 8609
[Suppes] p. 211Theorem 25oaass 8617
[Suppes] p. 225Definition 8iscard2 10045
[Suppes] p. 227Theorem 56ondomon 10632
[Suppes] p. 228Theorem 59harcard 10047
[Suppes] p. 228Definition 12(i)aleph0 10135
[Suppes] p. 228Theorem Schema 61onintss 6446
[Suppes] p. 228Theorem Schema 62onminesb 7829  onminsb 7830
[Suppes] p. 229Theorem 64alephval2 10641
[Suppes] p. 229Theorem 65alephcard 10139
[Suppes] p. 229Theorem 66alephord2i 10146
[Suppes] p. 229Theorem 67alephnbtwn 10140
[Suppes] p. 229Definition 12df-aleph 10009
[Suppes] p. 242Theorem 6weth 10564
[Suppes] p. 242Theorem 8entric 10626
[Suppes] p. 242Theorem 9carden 10620
[Szendrei] p. 11Line 6df-cloneop 35658
[Szendrei] p. 11Paragraph 3df-suppos 35662
[TakeutiZaring] p. 8Axiom 1ax-ext 2711
[TakeutiZaring] p. 13Definition 4.5df-cleq 2732
[TakeutiZaring] p. 13Proposition 4.6df-clel 2819
[TakeutiZaring] p. 13Proposition 4.9cvjust 2734
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2763
[TakeutiZaring] p. 14Definition 4.16df-oprab 7452
[TakeutiZaring] p. 14Proposition 4.14ru 3802
[TakeutiZaring] p. 15Axiom 2zfpair 5439
[TakeutiZaring] p. 15Exercise 1elpr 4672  elpr2 4674  elpr2g 4673  elprg 4670
[TakeutiZaring] p. 15Exercise 2elsn 4663  elsn2 4687  elsn2g 4686  elsng 4662  velsn 4664
[TakeutiZaring] p. 15Exercise 3elop 5487
[TakeutiZaring] p. 15Exercise 4sneq 4658  sneqr 4865
[TakeutiZaring] p. 15Definition 5.1dfpr2 4668  dfsn2 4661  dfsn2ALT 4669
[TakeutiZaring] p. 16Axiom 3uniex 7776
[TakeutiZaring] p. 16Exercise 6opth 5496
[TakeutiZaring] p. 16Exercise 7opex 5484
[TakeutiZaring] p. 16Exercise 8rext 5468
[TakeutiZaring] p. 16Corollary 5.8unex 7779  unexg 7778
[TakeutiZaring] p. 16Definition 5.3dftp2 4714
[TakeutiZaring] p. 16Definition 5.5df-uni 4932
[TakeutiZaring] p. 16Definition 5.6df-in 3983  df-un 3981
[TakeutiZaring] p. 16Proposition 5.7unipr 4948  uniprg 4947
[TakeutiZaring] p. 17Axiom 4vpwex 5395
[TakeutiZaring] p. 17Exercise 1eltp 4712
[TakeutiZaring] p. 17Exercise 5elsuc 6465  elsucg 6463  sstr2 4015
[TakeutiZaring] p. 17Exercise 6uncom 4181
[TakeutiZaring] p. 17Exercise 7incom 4230
[TakeutiZaring] p. 17Exercise 8unass 4195
[TakeutiZaring] p. 17Exercise 9inass 4249
[TakeutiZaring] p. 17Exercise 10indi 4303
[TakeutiZaring] p. 17Exercise 11undi 4304
[TakeutiZaring] p. 17Definition 5.9df-pss 3996  df-ss 3993
[TakeutiZaring] p. 17Definition 5.10df-pw 4624
[TakeutiZaring] p. 18Exercise 7unss2 4210
[TakeutiZaring] p. 18Exercise 9dfss2 3994  sseqin2 4244
[TakeutiZaring] p. 18Exercise 10ssid 4031
[TakeutiZaring] p. 18Exercise 12inss1 4258  inss2 4259
[TakeutiZaring] p. 18Exercise 13nss 4073
[TakeutiZaring] p. 18Exercise 15unieq 4942
[TakeutiZaring] p. 18Exercise 18sspwb 5469  sspwimp 44889  sspwimpALT 44896  sspwimpALT2 44899  sspwimpcf 44891
[TakeutiZaring] p. 18Exercise 19pweqb 5476
[TakeutiZaring] p. 19Axiom 5ax-rep 5303
[TakeutiZaring] p. 20Definitiondf-rab 3444
[TakeutiZaring] p. 20Corollary 5.160ex 5325
[TakeutiZaring] p. 20Definition 5.12df-dif 3979
[TakeutiZaring] p. 20Definition 5.14dfnul2 4355
[TakeutiZaring] p. 20Proposition 5.15difid 4398
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4376  n0f 4372  neq0 4375  neq0f 4371
[TakeutiZaring] p. 21Axiom 6zfreg 9664
[TakeutiZaring] p. 21Axiom 6'zfregs 9801
[TakeutiZaring] p. 21Theorem 5.22setind 9803
[TakeutiZaring] p. 21Definition 5.20df-v 3490
[TakeutiZaring] p. 21Proposition 5.21vprc 5333
[TakeutiZaring] p. 22Exercise 10ss 4423
[TakeutiZaring] p. 22Exercise 3ssex 5339  ssexg 5341
[TakeutiZaring] p. 22Exercise 4inex1 5335
[TakeutiZaring] p. 22Exercise 5ruv 9671
[TakeutiZaring] p. 22Exercise 6elirr 9666
[TakeutiZaring] p. 22Exercise 7ssdif0 4389
[TakeutiZaring] p. 22Exercise 11difdif 4158
[TakeutiZaring] p. 22Exercise 13undif3 4319  undif3VD 44853
[TakeutiZaring] p. 22Exercise 14difss 4159
[TakeutiZaring] p. 22Exercise 15sscon 4166
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3068
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3077
[TakeutiZaring] p. 23Proposition 6.2xpex 7788  xpexg 7785
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5707
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6649
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6826  fun11 6652
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6589  svrelfun 6650
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5912
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5914
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5712
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5713
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5709
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6225  dfrel2 6220
[TakeutiZaring] p. 25Exercise 3xpss 5716
[TakeutiZaring] p. 25Exercise 5relun 5835
[TakeutiZaring] p. 25Exercise 6reluni 5842
[TakeutiZaring] p. 25Exercise 9inxp 5856
[TakeutiZaring] p. 25Exercise 12relres 6035
[TakeutiZaring] p. 25Exercise 13opelres 6015  opelresi 6017
[TakeutiZaring] p. 25Exercise 14dmres 6041
[TakeutiZaring] p. 25Exercise 15resss 6031
[TakeutiZaring] p. 25Exercise 17resabs1 6036
[TakeutiZaring] p. 25Exercise 18funres 6620
[TakeutiZaring] p. 25Exercise 24relco 6138
[TakeutiZaring] p. 25Exercise 29funco 6618
[TakeutiZaring] p. 25Exercise 30f1co 6828
[TakeutiZaring] p. 26Definition 6.10eu2 2612
[TakeutiZaring] p. 26Definition 6.11conventions 30432  df-fv 6581  fv3 6938
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7965  cnvexg 7964
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7949  dmexg 7941
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7950  rnexg 7942
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44423
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7960
[TakeutiZaring] p. 27Corollary 6.13fvex 6933
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47089  tz6.12-1-afv2 47156  tz6.12-1 6943  tz6.12-afv 47088  tz6.12-afv2 47155  tz6.12 6945  tz6.12c-afv2 47157  tz6.12c 6942
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47152  tz6.12-2 6908  tz6.12i-afv2 47158  tz6.12i 6948
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6576
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6577
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6579  wfo 6571
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6578  wf1 6570
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6580  wf1o 6572
[TakeutiZaring] p. 28Exercise 4eqfnfv 7064  eqfnfv2 7065  eqfnfv2f 7068
[TakeutiZaring] p. 28Exercise 5fvco 7020
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7254
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7252
[TakeutiZaring] p. 29Exercise 9funimaex 6666  funimaexg 6664
[TakeutiZaring] p. 29Definition 6.18df-br 5167
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5608
[TakeutiZaring] p. 30Definition 6.21dffr2 5661  dffr3 6129  eliniseg 6124  iniseg 6127
[TakeutiZaring] p. 30Definition 6.22df-eprel 5599
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5677  fr3nr 7807  frirr 5676
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5652
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7809
[TakeutiZaring] p. 31Exercise 1frss 5664
[TakeutiZaring] p. 31Exercise 4wess 5686
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6379  tz6.26i 6381  wefrc 5694  wereu2 5697
[TakeutiZaring] p. 32Theorem 6.27wfi 6382  wfii 6384
[TakeutiZaring] p. 32Definition 6.28df-isom 6582
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7365
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7366
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7372
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7373
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7374
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7378
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7385
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7387
[TakeutiZaring] p. 35Notationwtr 5283
[TakeutiZaring] p. 35Theorem 7.2trelpss 44424  tz7.2 5683
[TakeutiZaring] p. 35Definition 7.1dftr3 5289
[TakeutiZaring] p. 36Proposition 7.4ordwe 6408
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6416
[TakeutiZaring] p. 36Proposition 7.6ordelord 6417  ordelordALT 44508  ordelordALTVD 44838
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6423  ordelssne 6422
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6421
[TakeutiZaring] p. 37Proposition 7.9ordin 6425
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7817
[TakeutiZaring] p. 38Corollary 7.15ordsson 7818
[TakeutiZaring] p. 38Definition 7.11df-on 6399
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6427
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44520  ordon 7812
[TakeutiZaring] p. 38Proposition 7.13onprc 7813
[TakeutiZaring] p. 39Theorem 7.17tfi 7890
[TakeutiZaring] p. 40Exercise 3ontr2 6442
[TakeutiZaring] p. 40Exercise 7dftr2 5285
[TakeutiZaring] p. 40Exercise 9onssmin 7828
[TakeutiZaring] p. 40Exercise 11unon 7867
[TakeutiZaring] p. 40Exercise 12ordun 6499
[TakeutiZaring] p. 40Exercise 14ordequn 6498
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7814
[TakeutiZaring] p. 40Proposition 7.20elssuni 4961
[TakeutiZaring] p. 41Definition 7.22df-suc 6401
[TakeutiZaring] p. 41Proposition 7.23sssucid 6475  sucidg 6476
[TakeutiZaring] p. 41Proposition 7.24onsuc 7847
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6489  ordnbtwn 6488
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7864
[TakeutiZaring] p. 42Exercise 1df-lim 6400
[TakeutiZaring] p. 42Exercise 4omssnlim 7918
[TakeutiZaring] p. 42Exercise 7ssnlim 7923
[TakeutiZaring] p. 42Exercise 8onsucssi 7878  ordelsuc 7856
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7858
[TakeutiZaring] p. 42Definition 7.27nlimon 7888
[TakeutiZaring] p. 42Definition 7.28dfom2 7905
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7927
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7929
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7930
[TakeutiZaring] p. 43Remarkomon 7915
[TakeutiZaring] p. 43Axiom 7inf3 9704  omex 9712
[TakeutiZaring] p. 43Theorem 7.32ordom 7913
[TakeutiZaring] p. 43Corollary 7.31find 7935
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7931
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7932
[TakeutiZaring] p. 44Exercise 1limomss 7908
[TakeutiZaring] p. 44Exercise 2int0 4986
[TakeutiZaring] p. 44Exercise 3trintss 5302
[TakeutiZaring] p. 44Exercise 4intss1 4987
[TakeutiZaring] p. 44Exercise 5intex 5362
[TakeutiZaring] p. 44Exercise 6oninton 7831
[TakeutiZaring] p. 44Exercise 11ordintdif 6445
[TakeutiZaring] p. 44Definition 7.35df-int 4971
[TakeutiZaring] p. 44Proposition 7.34noinfep 9729
[TakeutiZaring] p. 45Exercise 4onint 7826
[TakeutiZaring] p. 47Lemma 1tfrlem1 8432
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8453
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8454
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8455
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8462  tz7.44-2 8463  tz7.44-3 8464
[TakeutiZaring] p. 50Exercise 1smogt 8423
[TakeutiZaring] p. 50Exercise 3smoiso 8418
[TakeutiZaring] p. 50Definition 7.46df-smo 8402
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8501  tz7.49c 8502
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8499
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8498
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8500
[TakeutiZaring] p. 53Proposition 7.532eu5 2659
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10080
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10081
[TakeutiZaring] p. 56Definition 8.1oalim 8588  oasuc 8580
[TakeutiZaring] p. 57Remarktfindsg 7898
[TakeutiZaring] p. 57Proposition 8.2oacl 8591
[TakeutiZaring] p. 57Proposition 8.3oa0 8572  oa0r 8594
[TakeutiZaring] p. 57Proposition 8.16omcl 8592
[TakeutiZaring] p. 58Corollary 8.5oacan 8604
[TakeutiZaring] p. 58Proposition 8.4nnaord 8675  nnaordi 8674  oaord 8603  oaordi 8602
[TakeutiZaring] p. 59Proposition 8.6iunss2 5072  uniss2 4965
[TakeutiZaring] p. 59Proposition 8.7oawordri 8606
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8611  oawordex 8613
[TakeutiZaring] p. 59Proposition 8.9nnacl 8667
[TakeutiZaring] p. 59Proposition 8.10oaabs 8704
[TakeutiZaring] p. 60Remarkoancom 9720
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8616
[TakeutiZaring] p. 62Exercise 1nnarcl 8672
[TakeutiZaring] p. 62Exercise 5oaword1 8608
[TakeutiZaring] p. 62Definition 8.15om0x 8575  omlim 8589  omsuc 8582
[TakeutiZaring] p. 62Definition 8.15(a)om0 8573
[TakeutiZaring] p. 63Proposition 8.17nnecl 8669  nnmcl 8668
[TakeutiZaring] p. 63Proposition 8.19nnmord 8688  nnmordi 8687  omord 8624  omordi 8622
[TakeutiZaring] p. 63Proposition 8.20omcan 8625
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8692  omwordri 8628
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8595
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8598  om1r 8599
[TakeutiZaring] p. 64Proposition 8.22om00 8631
[TakeutiZaring] p. 64Proposition 8.23omordlim 8633
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8634
[TakeutiZaring] p. 64Proposition 8.25odi 8635
[TakeutiZaring] p. 65Theorem 8.26omass 8636
[TakeutiZaring] p. 67Definition 8.30nnesuc 8664  oe0 8578  oelim 8590  oesuc 8583  onesuc 8586
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8576
[TakeutiZaring] p. 67Proposition 8.32oen0 8642
[TakeutiZaring] p. 67Proposition 8.33oeordi 8643
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8577
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8601
[TakeutiZaring] p. 68Corollary 8.34oeord 8644
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8650
[TakeutiZaring] p. 68Proposition 8.35oewordri 8648
[TakeutiZaring] p. 68Proposition 8.37oeworde 8649
[TakeutiZaring] p. 69Proposition 8.41oeoa 8653
[TakeutiZaring] p. 70Proposition 8.42oeoe 8655
[TakeutiZaring] p. 73Theorem 9.1trcl 9797  tz9.1 9798
[TakeutiZaring] p. 76Definition 9.9df-r1 9833  r10 9837  r1lim 9841  r1limg 9840  r1suc 9839  r1sucg 9838
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9849  r1ord2 9850  r1ordg 9847
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9859
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9884  tz9.13 9860  tz9.13g 9861
[TakeutiZaring] p. 79Definition 9.14df-rank 9834  rankval 9885  rankvalb 9866  rankvalg 9886
[TakeutiZaring] p. 79Proposition 9.16rankel 9908  rankelb 9893
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9922  rankval3 9909  rankval3b 9895
[TakeutiZaring] p. 79Proposition 9.18rankonid 9898
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9864
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9903  rankr1c 9890  rankr1g 9901
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9904
[TakeutiZaring] p. 80Exercise 1rankss 9918  rankssb 9917
[TakeutiZaring] p. 80Exercise 2unbndrank 9911
[TakeutiZaring] p. 80Proposition 9.19bndrank 9910
[TakeutiZaring] p. 83Axiom of Choiceac4 10544  dfac3 10190
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10099  numth 10541  numth2 10540
[TakeutiZaring] p. 85Definition 10.4cardval 10615
[TakeutiZaring] p. 85Proposition 10.5cardid 10616  cardid2 10022
[TakeutiZaring] p. 85Proposition 10.9oncard 10029
[TakeutiZaring] p. 85Proposition 10.10carden 10620
[TakeutiZaring] p. 85Proposition 10.11cardidm 10028
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 10013
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 10034
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 10026
[TakeutiZaring] p. 87Proposition 10.15pwen 9216
[TakeutiZaring] p. 88Exercise 1en0 9078
[TakeutiZaring] p. 88Exercise 7infensuc 9221
[TakeutiZaring] p. 89Exercise 10omxpen 9140
[TakeutiZaring] p. 90Corollary 10.23cardnn 10032
[TakeutiZaring] p. 90Definition 10.27alephiso 10167
[TakeutiZaring] p. 90Proposition 10.20nneneq 9272
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9291
[TakeutiZaring] p. 90Proposition 10.26alephprc 10168
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9277
[TakeutiZaring] p. 91Exercise 2alephle 10157
[TakeutiZaring] p. 91Exercise 3aleph0 10135
[TakeutiZaring] p. 91Exercise 4cardlim 10041
[TakeutiZaring] p. 91Exercise 7infpss 10285
[TakeutiZaring] p. 91Exercise 8infcntss 9390
[TakeutiZaring] p. 91Definition 10.29df-fin 9007  isfi 9036
[TakeutiZaring] p. 92Proposition 10.32onfin 9293
[TakeutiZaring] p. 92Proposition 10.34imadomg 10603
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9133
[TakeutiZaring] p. 93Proposition 10.35fodomb 10595
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10255  unxpdom 9316
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 10043  cardsdomelir 10042
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9318
[TakeutiZaring] p. 94Proposition 10.39infxpen 10083
[TakeutiZaring] p. 95Definition 10.42df-map 8886
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10631  infxpidm2 10086
[TakeutiZaring] p. 95Proposition 10.41infdju 10276  infxp 10283
[TakeutiZaring] p. 96Proposition 10.44pw2en 9145  pw2f1o 9143
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9209
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10556
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10551  ac6s5 10560
[TakeutiZaring] p. 98Theorem 10.47unidom 10612
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10613  uniimadomf 10614
[TakeutiZaring] p. 100Definition 11.1cfcof 10343
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10338
[TakeutiZaring] p. 102Exercise 1cfle 10323
[TakeutiZaring] p. 102Exercise 2cf0 10320
[TakeutiZaring] p. 102Exercise 3cfsuc 10326
[TakeutiZaring] p. 102Exercise 4cfom 10333
[TakeutiZaring] p. 102Proposition 11.9coftr 10342
[TakeutiZaring] p. 103Theorem 11.15alephreg 10651
[TakeutiZaring] p. 103Proposition 11.11cardcf 10321
[TakeutiZaring] p. 103Proposition 11.13alephsing 10345
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10166
[TakeutiZaring] p. 104Proposition 11.16carduniima 10165
[TakeutiZaring] p. 104Proposition 11.18alephfp 10177  alephfp2 10178
[TakeutiZaring] p. 106Theorem 11.20gchina 10768
[TakeutiZaring] p. 106Theorem 11.21mappwen 10181
[TakeutiZaring] p. 107Theorem 11.26konigth 10638
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10652
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10653
[Tarski] p. 67Axiom B5ax-c5 38839
[Tarski] p. 67Scheme B5sp 2184
[Tarski] p. 68Lemma 6avril1 30495  equid 2011
[Tarski] p. 69Lemma 7equcomi 2016
[Tarski] p. 70Lemma 14spim 2395  spime 2397  spimew 1971
[Tarski] p. 70Lemma 16ax-12 2178  ax-c15 38845  ax12i 1966
[Tarski] p. 70Lemmas 16 and 17sb6 2085
[Tarski] p. 75Axiom B7ax6v 1968
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1909  ax5ALT 38863
[Tarski], p. 75Scheme B8 of system S2ax-7 2007  ax-8 2110  ax-9 2118
[Tarski1999] p. 178Axiom 4axtgsegcon 28490
[Tarski1999] p. 178Axiom 5axtg5seg 28491
[Tarski1999] p. 179Axiom 7axtgpasch 28493
[Tarski1999] p. 180Axiom 7.1axtgpasch 28493
[Tarski1999] p. 185Axiom 11axtgcont1 28494
[Truss] p. 114Theorem 5.18ruc 16291
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37619
[Viaclovsky8] p. 3Proposition 7ismblfin 37621
[Weierstrass] p. 272Definitiondf-mdet 22612  mdetuni 22649
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 902
[WhiteheadRussell] p. 96Axiom *1.3olc 867
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 868
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 918
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 968
[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 37411
[WhiteheadRussell] p. 100Theorem *2.05frege5 43762  imim2 58  wl-luk-imim2 37406
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 46934  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 895
[WhiteheadRussell] p. 101Theorem *2.06barbara 2666  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 901
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37409
[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 44898  wl-luk-notnotr 37410
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43792  axfrege28 43791  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 866
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 923
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37403
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 888
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 940
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30433  pm2.27 42  wl-luk-pm2.27 37401
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 921
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38319
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 922
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 970
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 971
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 969
[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 943
[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 191
[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 850
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 851
[WhiteheadRussell] p. 107Theorem *2.55orel1 887
[WhiteheadRussell] p. 107Theorem *2.56orel2 889
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 898
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 941
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 942
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[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 973
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 899
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 974
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 975
[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 972
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 976
[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 992
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 993
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 994
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 995
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 996
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 471
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 459
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 402
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 802
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 448
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 449
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 482  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 484  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 764
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 765
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 807
[WhiteheadRussell] p. 113Fact)pm3.45 621
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 809
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 492
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 493
[WhiteheadRussell] p. 113Theorem *3.44jao 961  pm3.44 960
[WhiteheadRussell] p. 113Theorem *3.47anim12 808
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 964
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 261
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 353
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 806
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 832
[WhiteheadRussell] p. 117Theorem *4.21bicom 222
[WhiteheadRussell] p. 117Theorem *4.22biantr 805  bitr 804
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 563
[WhiteheadRussell] p. 117Theorem *4.25oridm 903  pm4.25 904
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1008
[WhiteheadRussell] p. 118Theorem *4.31orcom 869
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[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 977
[WhiteheadRussell] p. 118Definition *4.34df-3an 1089
[WhiteheadRussell] p. 119Theorem *4.41ordi 1006
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1054
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1023
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 997
[WhiteheadRussell] p. 119Theorem *4.45orabs 999  pm4.45 998  pm4.45im 827
[WhiteheadRussell] p. 120Theorem *4.5anor 983
[WhiteheadRussell] p. 120Theorem *4.6imor 852
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 982
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 985
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 986
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 987
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 988
[WhiteheadRussell] p. 120Theorem *4.56ioran 984  pm4.56 989
[WhiteheadRussell] p. 120Theorem *4.57oran 990  pm4.57 991
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 855
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 848
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 849
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 398
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 557  pm4.71d 561  pm4.71i 559  pm4.71r 558  pm4.71rd 562  pm4.71ri 560
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 950
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 935
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 962  pm4.77 963
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 933
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1004
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1024
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1025
[WhiteheadRussell] p. 122Theorem *4.84imbi1 347
[WhiteheadRussell] p. 122Theorem *4.85imbi2 348
[WhiteheadRussell] p. 122Theorem *4.86bibi1 351
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 387  impexp 450  pm4.87 842
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 823
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 945  pm5.11g 944
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 946
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 948
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 947
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1013
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1014
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1012
[WhiteheadRussell] p. 124Theorem *5.18nbbn 383  pm5.18 381
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 386
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 824
[WhiteheadRussell] p. 124Theorem *5.22xor 1015
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1050
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1051
[WhiteheadRussell] p. 124Theorem *5.25dfor2 900
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 572
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 388
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 361
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1002
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 954
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 830
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 573
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 835
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 825
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 833
[WhiteheadRussell] p. 125Theorem *5.41imdi 389  pm5.41 390
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 543
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 542
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1005
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1018
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 949
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1001
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1019
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1020
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1028
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1029
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44327
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44328
[WhiteheadRussell] p. 147Theorem *10.2219.26 1869
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44329
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44330
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44331
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1892
[WhiteheadRussell] p. 151Theorem *10.301albitr 44332
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44333
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44334
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44335
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44336
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44338
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44339
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44340
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44337
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2090
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44343
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44344
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2070
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2161
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1827
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1828
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44345
[WhiteheadRussell] p. 162Theorem *11.322alim 44346
[WhiteheadRussell] p. 162Theorem *11.332albi 44347
[WhiteheadRussell] p. 162Theorem *11.342exim 44348
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44350
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44349
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1886
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44352
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44353
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44351
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1826
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44354
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44355
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1844
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44356
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2352
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1859
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44361
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44357
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44358
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44359
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44360
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44365
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44362
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44363
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44364
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44366
[WhiteheadRussell] p. 175Definition *14.02df-eu 2572
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44376  pm13.13b 44377
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44378
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3028
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3029
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3679
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44384
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44385
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44379
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44523  pm13.193 44380
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44381
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44382
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44383
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44390
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44389
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44388
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3872
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44391  pm14.122b 44392  pm14.122c 44393
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44394  pm14.123b 44395  pm14.123c 44396
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44398
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44397
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44399
[WhiteheadRussell] p. 190Theorem *14.22iota4 6554
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44400
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6555
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44401
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44403
[WhiteheadRussell] p. 192Theorem *14.26eupick 2636  eupickbi 2639  sbaniota 44404
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44402
[WhiteheadRussell] p. 192Theorem *14.271eubi 2587
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44406
[WhiteheadRussell] p. 235Definition *30.01conventions 30432  df-fv 6581
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 10070  pm54.43lem 10069
[Young] p. 141Definition of operator orderingleop2 32156
[Young] p. 142Example 12.2(i)0leop 32162  idleop 32163
[vandenDries] p. 42Lemma 61irrapx1 42784
[vandenDries] p. 43Theorem 62pellex 42791  pellexlem1 42785

This page was last updated on 17-Sep-2025.
Copyright terms: Public domain