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 16688
[Adamek] p. 21Condition 3.1(b)df-cat 16688
[Adamek] p. 22Example 3.3(1)df-setc 17085
[Adamek] p. 24Example 3.3(4.c)0cat 16708
[Adamek] p. 25Definition 3.5df-oppc 16731
[Adamek] p. 28Remark 3.9oppciso 16800
[Adamek] p. 28Remark 3.12invf1o 16788  invisoinvl 16809
[Adamek] p. 28Example 3.13idinv 16808  idiso 16807
[Adamek] p. 28Corollary 3.11inveq 16793
[Adamek] p. 28Definition 3.8df-inv 16767  df-iso 16768  dfiso2 16791
[Adamek] p. 28Proposition 3.10sectcan 16774
[Adamek] p. 29Remark 3.16cicer 16825
[Adamek] p. 29Definition 3.15cic 16818  df-cic 16815
[Adamek] p. 29Definition 3.17df-func 16877
[Adamek] p. 29Proposition 3.14(1)invinv 16789
[Adamek] p. 29Proposition 3.14(2)invco 16790  isoco 16796
[Adamek] p. 30Remark 3.19df-func 16877
[Adamek] p. 30Example 3.20(1)idfucl 16900
[Adamek] p. 32Proposition 3.21funciso 16893
[Adamek] p. 33Proposition 3.23cofucl 16907
[Adamek] p. 34Remark 3.28(2)catciso 17116
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 17167
[Adamek] p. 34Definition 3.27(2)df-fth 16924
[Adamek] p. 34Definition 3.27(3)df-full 16923
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 17167
[Adamek] p. 35Corollary 3.32ffthiso 16948
[Adamek] p. 35Proposition 3.30(c)cofth 16954
[Adamek] p. 35Proposition 3.30(d)cofull 16953
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 17152
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 17152
[Adamek] p. 39Definition 3.41funcoppc 16894
[Adamek] p. 39Definition 3.44.df-catc 17104
[Adamek] p. 39Proposition 3.43(c)fthoppc 16942
[Adamek] p. 39Proposition 3.43(d)fulloppc 16941
[Adamek] p. 40Remark 3.48catccat 17113
[Adamek] p. 40Definition 3.47df-catc 17104
[Adamek] p. 48Example 4.3(1.a)0subcat 16857
[Adamek] p. 48Example 4.3(1.b)catsubcat 16858
[Adamek] p. 48Definition 4.1(2)fullsubc 16869
[Adamek] p. 48Definition 4.1(a)df-subc 16831
[Adamek] p. 49Remark 4.4(2)ressffth 16957
[Adamek] p. 83Definition 6.1df-nat 16962
[Adamek] p. 87Remark 6.14(a)fuccocl 16983
[Adamek] p. 87Remark 6.14(b)fucass 16987
[Adamek] p. 87Definition 6.15df-fuc 16963
[Adamek] p. 88Remark 6.16fuccat 16989
[Adamek] p. 101Definition 7.1df-inito 17000
[Adamek] p. 101Example 7.2 (6)irinitoringc 42930
[Adamek] p. 102Definition 7.4df-termo 17001
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17021
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17025
[Adamek] p. 103Definition 7.7df-zeroo 17002
[Adamek] p. 103Example 7.9 (3)nzerooringczr 42933
[Adamek] p. 103Proposition 7.6termoeu1w 17028
[Adamek] p. 106Definition 7.19df-sect 16766
[Adamek] p. 478Item Rngdf-ringc 42866
[AhoHopUll] p. 2Section 1.1df-bigo 43203
[AhoHopUll] p. 12Section 1.3df-blen 43225
[AhoHopUll] p. 318Section 9.1df-concat 13638  df-pfx 13757  df-substr 13708  df-word 13582  lencl 13600  wrd0 13606
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 22889  df-nmoo 28151
[AkhiezerGlazman] p. 64Theoremhmopidmch 29563  hmopidmchi 29561
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 29611  pjcmul2i 29612
[AkhiezerGlazman] p. 72Theoremcnvunop 29328  unoplin 29330
[AkhiezerGlazman] p. 72Equation 2unopadj 29329  unopadj2 29348
[AkhiezerGlazman] p. 73Theoremelunop2 29423  lnopunii 29422
[AkhiezerGlazman] p. 80Proposition 1adjlnop 29496
[Apostol] p. 18Theorem I.1addcan 10546  addcan2d 10566  addcan2i 10556  addcand 10565  addcani 10555
[Apostol] p. 18Theorem I.2negeu 10598
[Apostol] p. 18Theorem I.3negsub 10657  negsubd 10726  negsubi 10687
[Apostol] p. 18Theorem I.4negneg 10659  negnegd 10711  negnegi 10679
[Apostol] p. 18Theorem I.5subdi 10794  subdid 10817  subdii 10810  subdir 10795  subdird 10818  subdiri 10811
[Apostol] p. 18Theorem I.6mul01 10541  mul01d 10561  mul01i 10552  mul02 10540  mul02d 10560  mul02i 10551
[Apostol] p. 18Theorem I.7mulcan 10996  mulcan2d 10993  mulcand 10992  mulcani 10998
[Apostol] p. 18Theorem I.8receu 11004  xreceu 30171
[Apostol] p. 18Theorem I.9divrec 11033  divrecd 11137  divreci 11103  divreczi 11096
[Apostol] p. 18Theorem I.10recrec 11055  recreci 11090
[Apostol] p. 18Theorem I.11mul0or 10999  mul0ord 11009  mul0ori 11007
[Apostol] p. 18Theorem I.12mul2neg 10800  mul2negd 10816  mul2negi 10809  mulneg1 10797  mulneg1d 10814  mulneg1i 10807
[Apostol] p. 18Theorem I.13divadddiv 11073  divadddivd 11178  divadddivi 11120
[Apostol] p. 18Theorem I.14divmuldiv 11058  divmuldivd 11175  divmuldivi 11118  rdivmuldivd 30332
[Apostol] p. 18Theorem I.15divdivdiv 11059  divdivdivd 11181  divdivdivi 11121
[Apostol] p. 20Axiom 7rpaddcl 12143  rpaddcld 12178  rpmulcl 12144  rpmulcld 12179
[Apostol] p. 20Axiom 8rpneg 12153
[Apostol] p. 20Axiom 90nrp 12156
[Apostol] p. 20Theorem I.17lttri 10489
[Apostol] p. 20Theorem I.18ltadd1d 10952  ltadd1dd 10970  ltadd1i 10913
[Apostol] p. 20Theorem I.19ltmul1 11210  ltmul1a 11209  ltmul1i 11279  ltmul1ii 11289  ltmul2 11211  ltmul2d 12205  ltmul2dd 12219  ltmul2i 11282
[Apostol] p. 20Theorem I.20msqgt0 10879  msqgt0d 10926  msqgt0i 10896
[Apostol] p. 20Theorem I.210lt1 10881
[Apostol] p. 20Theorem I.23lt0neg1 10865  lt0neg1d 10928  ltneg 10859  ltnegd 10937  ltnegi 10903
[Apostol] p. 20Theorem I.25lt2add 10844  lt2addd 10982  lt2addi 10921
[Apostol] p. 20Definition of positive numbersdf-rp 12120
[Apostol] p. 21Exercise 4recgt0 11204  recgt0d 11295  recgt0i 11265  recgt0ii 11266
[Apostol] p. 22Definition of integersdf-z 11712
[Apostol] p. 22Definition of positive integersdfnn3 11373
[Apostol] p. 22Definition of rationalsdf-q 12079
[Apostol] p. 24Theorem I.26supeu 8635
[Apostol] p. 26Theorem I.28nnunb 11621
[Apostol] p. 26Theorem I.29arch 11622
[Apostol] p. 28Exercise 2btwnz 11814
[Apostol] p. 28Exercise 3nnrecl 11623
[Apostol] p. 28Exercise 4rebtwnz 12077
[Apostol] p. 28Exercise 5zbtwnre 12076
[Apostol] p. 28Exercise 6qbtwnre 12325
[Apostol] p. 28Exercise 10(a)zeneo 15444  zneo 11795  zneoALTV 42424
[Apostol] p. 29Theorem I.35cxpsqrtth 24881  msqsqrtd 14563  resqrtth 14380  sqrtth 14488  sqrtthi 14494  sqsqrtd 14562
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 11360
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12043
[Apostol] p. 361Remarkcrreczi 13290
[Apostol] p. 363Remarkabsgt0i 14522
[Apostol] p. 363Exampleabssubd 14576  abssubi 14526
[ApostolNT] p. 7Remarkfmtno0 42296  fmtno1 42297  fmtno2 42306  fmtno3 42307  fmtno4 42308  fmtno5fac 42338  fmtnofz04prm 42333
[ApostolNT] p. 7Definitiondf-fmtno 42284
[ApostolNT] p. 8Definitiondf-ppi 25246
[ApostolNT] p. 14Definitiondf-dvds 15365
[ApostolNT] p. 14Theorem 1.1(a)iddvds 15379
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 15402
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 15398
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 15392
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 15394
[ApostolNT] p. 14Theorem 1.1(f)1dvds 15380
[ApostolNT] p. 14Theorem 1.1(g)dvds0 15381
[ApostolNT] p. 14Theorem 1.1(h)0dvds 15386
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 15417
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 15419
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 15421
[ApostolNT] p. 15Definitiondf-gcd 15597  dfgcd2 15643
[ApostolNT] p. 16Definitionisprm2 15774
[ApostolNT] p. 16Theorem 1.5coprmdvds 15746
[ApostolNT] p. 16Theorem 1.7prminf 15997
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 15615
[ApostolNT] p. 16Theorem 1.4(b)gcdass 15644
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 15646
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 15629
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 15621
[ApostolNT] p. 17Theorem 1.8coprm 15801
[ApostolNT] p. 17Theorem 1.9euclemma 15803
[ApostolNT] p. 17Theorem 1.101arith2 16010
[ApostolNT] p. 18Theorem 1.13prmrec 16004
[ApostolNT] p. 19Theorem 1.14divalg 15507
[ApostolNT] p. 20Theorem 1.15eucalg 15680
[ApostolNT] p. 24Definitiondf-mu 25247
[ApostolNT] p. 25Definitiondf-phi 15849
[ApostolNT] p. 25Theorem 2.1musum 25337
[ApostolNT] p. 26Theorem 2.2phisum 15873
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 15859
[ApostolNT] p. 28Theorem 2.5(c)phimul 15863
[ApostolNT] p. 32Definitiondf-vma 25244
[ApostolNT] p. 32Theorem 2.9muinv 25339
[ApostolNT] p. 32Theorem 2.10vmasum 25361
[ApostolNT] p. 38Remarkdf-sgm 25248
[ApostolNT] p. 38Definitiondf-sgm 25248
[ApostolNT] p. 75Definitiondf-chp 25245  df-cht 25243
[ApostolNT] p. 104Definitioncongr 15757
[ApostolNT] p. 106Remarkdvdsval3 15368
[ApostolNT] p. 106Definitionmoddvds 15375
[ApostolNT] p. 107Example 2mod2eq0even 15451
[ApostolNT] p. 107Example 3mod2eq1n2dvds 15452
[ApostolNT] p. 107Example 4zmod1congr 12989
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13026
[ApostolNT] p. 107Theorem 5.2(c)modexp 13300
[ApostolNT] p. 108Theorem 5.3modmulconst 15397
[ApostolNT] p. 109Theorem 5.4cncongr1 15760
[ApostolNT] p. 109Theorem 5.6gcdmodi 16156
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 15762
[ApostolNT] p. 113Theorem 5.17eulerth 15866
[ApostolNT] p. 113Theorem 5.18vfermltl 15884
[ApostolNT] p. 114Theorem 5.19fermltl 15867
[ApostolNT] p. 116Theorem 5.24wilthimp 25218
[ApostolNT] p. 179Definitiondf-lgs 25440  lgsprme0 25484
[ApostolNT] p. 180Example 11lgs 25485
[ApostolNT] p. 180Theorem 9.2lgsvalmod 25461
[ApostolNT] p. 180Theorem 9.3lgsdirprm 25476
[ApostolNT] p. 181Theorem 9.4m1lgs 25533
[ApostolNT] p. 181Theorem 9.52lgs 25552  2lgsoddprm 25561
[ApostolNT] p. 182Theorem 9.6gausslemma2d 25519
[ApostolNT] p. 185Theorem 9.8lgsquad 25528
[ApostolNT] p. 188Definitiondf-lgs 25440  lgs1 25486
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 25477
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 25479
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 25487
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 25488
[Baer] p. 40Property (b)mapdord 37708
[Baer] p. 40Property (c)mapd11 37709
[Baer] p. 40Property (e)mapdin 37732  mapdlsm 37734
[Baer] p. 40Property (f)mapd0 37735
[Baer] p. 40Definition of projectivitydf-mapd 37695  mapd1o 37718
[Baer] p. 41Property (g)mapdat 37737
[Baer] p. 44Part (1)mapdpg 37776
[Baer] p. 45Part (2)hdmap1eq 37871  mapdheq 37798  mapdheq2 37799  mapdheq2biN 37800
[Baer] p. 45Part (3)baerlem3 37783
[Baer] p. 46Part (4)mapdheq4 37802  mapdheq4lem 37801
[Baer] p. 46Part (5)baerlem5a 37784  baerlem5abmN 37788  baerlem5amN 37786  baerlem5b 37785  baerlem5bmN 37787
[Baer] p. 47Part (6)hdmap1l6 37891  hdmap1l6a 37879  hdmap1l6e 37884  hdmap1l6f 37885  hdmap1l6g 37886  hdmap1l6lem1 37877  hdmap1l6lem2 37878  mapdh6N 37817  mapdh6aN 37805  mapdh6eN 37810  mapdh6fN 37811  mapdh6gN 37812  mapdh6lem1N 37803  mapdh6lem2N 37804
[Baer] p. 48Part 9hdmapval 37898
[Baer] p. 48Part 10hdmap10 37910
[Baer] p. 48Part 11hdmapadd 37913
[Baer] p. 48Part (6)hdmap1l6h 37887  mapdh6hN 37813
[Baer] p. 48Part (7)mapdh75cN 37823  mapdh75d 37824  mapdh75e 37822  mapdh75fN 37825  mapdh7cN 37819  mapdh7dN 37820  mapdh7eN 37818  mapdh7fN 37821
[Baer] p. 48Part (8)mapdh8 37858  mapdh8a 37845  mapdh8aa 37846  mapdh8ab 37847  mapdh8ac 37848  mapdh8ad 37849  mapdh8b 37850  mapdh8c 37851  mapdh8d 37853  mapdh8d0N 37852  mapdh8e 37854  mapdh8g 37855  mapdh8i 37856  mapdh8j 37857
[Baer] p. 48Part (9)mapdh9a 37859
[Baer] p. 48Equation 10mapdhvmap 37839
[Baer] p. 49Part 12hdmap11 37918  hdmapeq0 37914  hdmapf1oN 37935  hdmapneg 37916  hdmaprnN 37934  hdmaprnlem1N 37919  hdmaprnlem3N 37920  hdmaprnlem3uN 37921  hdmaprnlem4N 37923  hdmaprnlem6N 37924  hdmaprnlem7N 37925  hdmaprnlem8N 37926  hdmaprnlem9N 37927  hdmapsub 37917
[Baer] p. 49Part 14hdmap14lem1 37938  hdmap14lem10 37947  hdmap14lem1a 37936  hdmap14lem2N 37939  hdmap14lem2a 37937  hdmap14lem3 37940  hdmap14lem8 37945  hdmap14lem9 37946
[Baer] p. 50Part 14hdmap14lem11 37948  hdmap14lem12 37949  hdmap14lem13 37950  hdmap14lem14 37951  hdmap14lem15 37952  hgmapval 37957
[Baer] p. 50Part 15hgmapadd 37964  hgmapmul 37965  hgmaprnlem2N 37967  hgmapvs 37961
[Baer] p. 50Part 16hgmaprnN 37971
[Baer] p. 110Lemma 1hdmapip0com 37987
[Baer] p. 110Line 27hdmapinvlem1 37988
[Baer] p. 110Line 28hdmapinvlem2 37989
[Baer] p. 110Line 30hdmapinvlem3 37990
[Baer] p. 110Part 1.2hdmapglem5 37992  hgmapvv 37996
[Baer] p. 110Proposition 1hdmapinvlem4 37991
[Baer] p. 111Line 10hgmapvvlem1 37993
[Baer] p. 111Line 15hdmapg 38000  hdmapglem7 37999
[Bauer], p. 483Theorem 1.22irrexpq 24882  2irrexpqALT 24947
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2640
[BellMachover] p. 460Notationdf-mo 2605
[BellMachover] p. 460Definitionmo3 2633
[BellMachover] p. 461Axiom Extax-ext 2803
[BellMachover] p. 462Theorem 1.1axextmo 2808
[BellMachover] p. 463Axiom Repaxrep5 5002
[BellMachover] p. 463Scheme Sepaxsep 5006
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 33541  bm1.3ii 5010
[BellMachover] p. 466Problemaxpow2 5069
[BellMachover] p. 466Axiom Powaxpow3 5070
[BellMachover] p. 466Axiom Unionaxun2 7216
[BellMachover] p. 468Definitiondf-ord 5970
[BellMachover] p. 469Theorem 2.2(i)ordirr 5985
[BellMachover] p. 469Theorem 2.2(iii)onelon 5992
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 5987
[BellMachover] p. 471Definition of Ndf-om 7332
[BellMachover] p. 471Problem 2.5(ii)uniordint 7272
[BellMachover] p. 471Definition of Limdf-lim 5972
[BellMachover] p. 472Axiom Infzfinf2 8823
[BellMachover] p. 473Theorem 2.8limom 7346
[BellMachover] p. 477Equation 3.1df-r1 8911
[BellMachover] p. 478Definitionrankval2 8965
[BellMachover] p. 478Theorem 3.3(i)r1ord3 8929  r1ord3g 8926
[BellMachover] p. 480Axiom Regzfreg 8776
[BellMachover] p. 488Axiom ACac5 9621  dfac4 9265
[BellMachover] p. 490Definition of alephalephval3 9253
[BeltramettiCassinelli] p. 98Remarkatlatmstc 35389
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 29763
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 29805  chirredi 29804
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 29793
[Beran] p. 3Definition of joinsshjval3 28764
[Beran] p. 39Theorem 2.3(i)cmcm2 29026  cmcm2i 29003  cmcm2ii 29008  cmt2N 35320
[Beran] p. 40Theorem 2.3(iii)lecm 29027  lecmi 29012  lecmii 29013
[Beran] p. 45Theorem 3.4cmcmlem 29001
[Beran] p. 49Theorem 4.2cm2j 29030  cm2ji 29035  cm2mi 29036
[Beran] p. 95Definitiondf-sh 28615  issh2 28617
[Beran] p. 95Lemma 3.1(S5)his5 28494
[Beran] p. 95Lemma 3.1(S6)his6 28507
[Beran] p. 95Lemma 3.1(S7)his7 28498
[Beran] p. 95Lemma 3.2(S8)ho01i 29238
[Beran] p. 95Lemma 3.2(S9)hoeq1 29240
[Beran] p. 95Lemma 3.2(S10)ho02i 29239
[Beran] p. 95Lemma 3.2(S11)hoeq2 29241
[Beran] p. 95Postulate (S1)ax-his1 28490  his1i 28508
[Beran] p. 95Postulate (S2)ax-his2 28491
[Beran] p. 95Postulate (S3)ax-his3 28492
[Beran] p. 95Postulate (S4)ax-his4 28493
[Beran] p. 96Definition of normdf-hnorm 28376  dfhnorm2 28530  normval 28532
[Beran] p. 96Definition for Cauchy sequencehcau 28592
[Beran] p. 96Definition of Cauchy sequencedf-hcau 28381
[Beran] p. 96Definition of complete subspaceisch3 28649
[Beran] p. 96Definition of convergedf-hlim 28380  hlimi 28596
[Beran] p. 97Theorem 3.3(i)norm-i-i 28541  norm-i 28537
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 28545  norm-ii 28546  normlem0 28517  normlem1 28518  normlem2 28519  normlem3 28520  normlem4 28521  normlem5 28522  normlem6 28523  normlem7 28524  normlem7tALT 28527
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 28547  norm-iii 28548
[Beran] p. 98Remark 3.4bcs 28589  bcsiALT 28587  bcsiHIL 28588
[Beran] p. 98Remark 3.4(B)normlem9at 28529  normpar 28563  normpari 28562
[Beran] p. 98Remark 3.4(C)normpyc 28554  normpyth 28553  normpythi 28550
[Beran] p. 99Remarklnfn0 29457  lnfn0i 29452  lnop0 29376  lnop0i 29380
[Beran] p. 99Theorem 3.5(i)nmcexi 29436  nmcfnex 29463  nmcfnexi 29461  nmcopex 29439  nmcopexi 29437
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 29464  nmcfnlbi 29462  nmcoplb 29440  nmcoplbi 29438
[Beran] p. 99Theorem 3.5(iii)lnfncon 29466  lnfnconi 29465  lnopcon 29445  lnopconi 29444
[Beran] p. 100Lemma 3.6normpar2i 28564
[Beran] p. 101Lemma 3.6norm3adifi 28561  norm3adifii 28556  norm3dif 28558  norm3difi 28555
[Beran] p. 102Theorem 3.7(i)chocunii 28711  pjhth 28803  pjhtheu 28804  pjpjhth 28835  pjpjhthi 28836  pjth 23614
[Beran] p. 102Theorem 3.7(ii)ococ 28816  ococi 28815
[Beran] p. 103Remark 3.8nlelchi 29471
[Beran] p. 104Theorem 3.9riesz3i 29472  riesz4 29474  riesz4i 29473
[Beran] p. 104Theorem 3.10cnlnadj 29489  cnlnadjeu 29488  cnlnadjeui 29487  cnlnadji 29486  cnlnadjlem1 29477  nmopadjlei 29498
[Beran] p. 106Theorem 3.11(i)adjeq0 29501
[Beran] p. 106Theorem 3.11(v)nmopadji 29500
[Beran] p. 106Theorem 3.11(ii)adjmul 29502
[Beran] p. 106Theorem 3.11(iv)adjadj 29346
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 29512  nmopcoadji 29511
[Beran] p. 106Theorem 3.11(iii)adjadd 29503
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 29513
[Beran] p. 106Theorem 3.11(viii)adjcoi 29510  pjadj2coi 29614  pjadjcoi 29571
[Beran] p. 107Definitiondf-ch 28629  isch2 28631
[Beran] p. 107Remark 3.12choccl 28716  isch3 28649  occl 28714  ocsh 28693  shoccl 28715  shocsh 28694
[Beran] p. 107Remark 3.12(B)ococin 28818
[Beran] p. 108Theorem 3.13chintcl 28742
[Beran] p. 109Property (i)pjadj2 29597  pjadj3 29598  pjadji 29095  pjadjii 29084
[Beran] p. 109Property (ii)pjidmco 29591  pjidmcoi 29587  pjidmi 29083
[Beran] p. 110Definition of projector orderingpjordi 29583
[Beran] p. 111Remarkho0val 29160  pjch1 29080
[Beran] p. 111Definitiondf-hfmul 29144  df-hfsum 29143  df-hodif 29142  df-homul 29141  df-hosum 29140
[Beran] p. 111Lemma 4.4(i)pjo 29081
[Beran] p. 111Lemma 4.4(ii)pjch 29104  pjchi 28842
[Beran] p. 111Lemma 4.4(iii)pjoc2 28849  pjoc2i 28848
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 29090
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 29575  pjssmii 29091
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 29574
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 29573
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 29578
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 29576  pjssge0ii 29092
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 29577  pjdifnormii 29093
[Bobzien] p. 116Statement T3stoic3 1875
[Bobzien] p. 117Statement T2stoic2a 1873
[Bobzien] p. 117Statement T4stoic4a 1876
[Bobzien] p. 117Conclusion the contradictorystoic1a 1871
[Bogachev] p. 16Definition 1.5df-oms 30895
[Bogachev] p. 17Lemma 1.5.4omssubadd 30903
[Bogachev] p. 17Example 1.5.2omsmon 30901
[Bogachev] p. 41Definition 1.11.2df-carsg 30905
[Bogachev] p. 42Theorem 1.11.4carsgsiga 30925
[Bogachev] p. 116Definition 2.3.1df-itgm 30956  df-sitm 30934
[Bogachev] p. 118Chapter 2.4.4df-itgm 30956
[Bogachev] p. 118Definition 2.4.1df-sitg 30933
[Bollobas] p. 1Section I.1df-edg 26353  isuhgrop 26375  isusgrop 26468  isuspgrop 26467
[Bollobas] p. 2Section I.1df-subgr 26572  uhgrspan1 26607  uhgrspansubgr 26595
[Bollobas] p. 3Definitionisomuspgr 42566
[Bollobas] p. 3Section I.1cusgrsize 26759  df-cusgr 26717  df-nbgr 26637  fusgrmaxsize 26769
[Bollobas] p. 4Definitiondf-upwlks 42576  df-wlks 26904
[Bollobas] p. 4Section I.1finsumvtxdg2size 26855  finsumvtxdgeven 26857  fusgr1th 26856  fusgrvtxdgonume 26859  vtxdgoddnumeven 26858
[Bollobas] p. 5Notationdf-pths 27025
[Bollobas] p. 5Definitiondf-crcts 27095  df-cycls 27096  df-trls 27000  df-wlkson 26905
[Bollobas] p. 7Section I.1df-ushgr 26364
[BourbakiAlg1] p. 1Definition 1df-clintop 42697  df-cllaw 42683  df-mgm 17602  df-mgm2 42716
[BourbakiAlg1] p. 4Definition 5df-assintop 42698  df-asslaw 42685  df-sgrp 17644  df-sgrp2 42718
[BourbakiAlg1] p. 7Definition 8df-cmgm2 42717  df-comlaw 42684
[BourbakiAlg1] p. 12Definition 2df-mnd 17655
[BourbakiAlg1] p. 92Definition 1df-ring 18910
[BourbakiAlg1] p. 93Section I.8.1df-rng0 42736
[BourbakiEns] p. Proposition 8fcof1 6802  fcofo 6803
[BourbakiTop1] p. Remarkxnegmnf 12336  xnegpnf 12335
[BourbakiTop1] p. Remark rexneg 12337
[BourbakiTop1] p. Remark 3ust0 22400  ustfilxp 22393
[BourbakiTop1] p. Axiom GT'tgpsubcn 22271
[BourbakiTop1] p. Example 1cstucnd 22465  iducn 22464  snfil 22045
[BourbakiTop1] p. Example 2neifil 22061
[BourbakiTop1] p. Theorem 1cnextcn 22248
[BourbakiTop1] p. Theorem 2ucnextcn 22485
[BourbakiTop1] p. Theorem 3df-hcmp 30544
[BourbakiTop1] p. Paragraph 3infil 22044
[BourbakiTop1] p. Propositionishmeo 21940
[BourbakiTop1] p. Definition 1df-ucn 22457  df-ust 22381  filintn0 22042  filn0 22043  istgp 22258  ucnprima 22463
[BourbakiTop1] p. Definition 2df-cfilu 22468
[BourbakiTop1] p. Definition 3df-cusp 22479  df-usp 22438  df-utop 22412  trust 22410
[BourbakiTop1] p. Definition 6df-pcmp 30464
[BourbakiTop1] p. Property V_issnei2 21298
[BourbakiTop1] p. Theorem 1(d)iscncl 21451
[BourbakiTop1] p. Condition F_Iustssel 22386
[BourbakiTop1] p. Condition U_Iustdiag 22389
[BourbakiTop1] p. Property V_iiinnei 21307
[BourbakiTop1] p. Property V_ivneiptopreu 21315  neissex 21309
[BourbakiTop1] p. Proposition 1neips 21295  neiss 21291  ucncn 22466  ustund 22402  ustuqtop 22427
[BourbakiTop1] p. Proposition 2cnpco 21449  neiptopreu 21315  utop2nei 22431  utop3cls 22432
[BourbakiTop1] p. Proposition 3fmucnd 22473  uspreg 22455  utopreg 22433
[BourbakiTop1] p. Proposition 4imasncld 21872  imasncls 21873  imasnopn 21871
[BourbakiTop1] p. Proposition 9cnpflf2 22181
[BourbakiTop1] p. Condition F_IIustincl 22388
[BourbakiTop1] p. Condition U_IIustinvel 22390
[BourbakiTop1] p. Property V_iiielnei 21293
[BourbakiTop1] p. Proposition 11cnextucn 22484
[BourbakiTop1] p. Condition F_IIbustbasel 22387
[BourbakiTop1] p. Condition U_IIIustexhalf 22391
[BourbakiTop1] p. Definition C'''df-cmp 21568
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 22027
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 21076
[BourbakiTop2] p. 195Definition 1df-ldlf 30461
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 41067
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 41069  stoweid 41068
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 41006  stoweidlem10 41015  stoweidlem14 41019  stoweidlem15 41020  stoweidlem35 41040  stoweidlem36 41041  stoweidlem37 41042  stoweidlem38 41043  stoweidlem40 41045  stoweidlem41 41046  stoweidlem43 41048  stoweidlem44 41049  stoweidlem46 41051  stoweidlem5 41010  stoweidlem50 41055  stoweidlem52 41057  stoweidlem53 41058  stoweidlem55 41060  stoweidlem56 41061
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 41028  stoweidlem24 41029  stoweidlem27 41032  stoweidlem28 41033  stoweidlem30 41035
[BrosowskiDeutsh] p. 91Proofstoweidlem34 41039  stoweidlem59 41064  stoweidlem60 41065
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 41050  stoweidlem49 41054  stoweidlem7 41012
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 41036  stoweidlem39 41044  stoweidlem42 41047  stoweidlem48 41053  stoweidlem51 41056  stoweidlem54 41059  stoweidlem57 41062  stoweidlem58 41063
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 41030
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 41022
[BrosowskiDeutsh] p. 92Proofstoweidlem11 41016  stoweidlem13 41018  stoweidlem26 41031  stoweidlem61 41066
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 41023
[Bruck] p. 1Section I.1df-clintop 42697  df-mgm 17602  df-mgm2 42716
[Bruck] p. 23Section II.1df-sgrp 17644  df-sgrp2 42718
[Bruck] p. 28Theorem 3.2dfgrp3 17875
[ChoquetDD] p. 2Definition of mappingdf-mpt 4955
[Church] p. 129Section II.24df-ifp 1090  dfifp2 1091
[Clemente] p. 10Definition ITnatded 27814
[Clemente] p. 10Definition I` `m,nnatded 27814
[Clemente] p. 11Definition E=>m,nnatded 27814
[Clemente] p. 11Definition I=>m,nnatded 27814
[Clemente] p. 11Definition E` `(1)natded 27814
[Clemente] p. 11Definition E` `(2)natded 27814
[Clemente] p. 12Definition E` `m,n,pnatded 27814
[Clemente] p. 12Definition I` `n(1)natded 27814
[Clemente] p. 12Definition I` `n(2)natded 27814
[Clemente] p. 13Definition I` `m,n,pnatded 27814
[Clemente] p. 14Proof 5.11natded 27814
[Clemente] p. 14Definition E` `nnatded 27814
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 27816  ex-natded5.2 27815
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 27819  ex-natded5.3 27818
[Clemente] p. 18Theorem 5.5ex-natded5.5 27821
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 27823  ex-natded5.7 27822
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 27825  ex-natded5.8 27824
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 27827  ex-natded5.13 27826
[Clemente] p. 32Definition I` `nnatded 27814
[Clemente] p. 32Definition E` `m,n,p,anatded 27814
[Clemente] p. 32Definition E` `n,tnatded 27814
[Clemente] p. 32Definition I` `n,tnatded 27814
[Clemente] p. 43Theorem 9.20ex-natded9.20 27828
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 27829
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 27831  ex-natded9.26 27830
[Cohen] p. 301Remarkrelogoprlem 24743
[Cohen] p. 301Property 2relogmul 24744  relogmuld 24777
[Cohen] p. 301Property 3relogdiv 24745  relogdivd 24778
[Cohen] p. 301Property 4relogexp 24748
[Cohen] p. 301Property 1alog1 24738
[Cohen] p. 301Property 1bloge 24739
[Cohen4] p. 348Observationrelogbcxpb 24934
[Cohen4] p. 349Propertyrelogbf 24938
[Cohen4] p. 352Definitionelogb 24917
[Cohen4] p. 361Property 2relogbmul 24924
[Cohen4] p. 361Property 3logbrec 24929  relogbdiv 24926
[Cohen4] p. 361Property 4relogbreexp 24922
[Cohen4] p. 361Property 6relogbexp 24927
[Cohen4] p. 361Property 1(a)logbid1 24915
[Cohen4] p. 361Property 1(b)logb1 24916
[Cohen4] p. 367Propertylogbchbase 24918
[Cohen4] p. 377Property 2logblt 24931
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 30888  sxbrsigalem4 30890
[Cohn] p. 81Section II.5acsdomd 17541  acsinfd 17540  acsinfdimd 17542  acsmap2d 17539  acsmapd 17538
[Cohn] p. 143Example 5.1.1sxbrsiga 30893
[Connell] p. 57Definitiondf-scmat 20672  df-scmatalt 43049
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 12962
[Crawley] p. 1Definition of posetdf-poset 17306
[Crawley] p. 107Theorem 13.2hlsupr 35456
[Crawley] p. 110Theorem 13.3arglem1N 36260  dalaw 35956
[Crawley] p. 111Theorem 13.4hlathil 38031
[Crawley] p. 111Definition of set Wdf-watsN 36060
[Crawley] p. 111Definition of dilationdf-dilN 36176  df-ldil 36174  isldil 36180
[Crawley] p. 111Definition of translationdf-ltrn 36175  df-trnN 36177  isltrn 36189  ltrnu 36191
[Crawley] p. 112Lemma Acdlema1N 35861  cdlema2N 35862  exatleN 35474
[Crawley] p. 112Lemma B1cvrat 35546  cdlemb 35864  cdlemb2 36111  cdlemb3 36676  idltrn 36220  l1cvat 35125  lhpat 36113  lhpat2 36115  lshpat 35126  ltrnel 36209  ltrnmw 36221
[Crawley] p. 112Lemma Ccdlemc1 36261  cdlemc2 36262  ltrnnidn 36244  trlat 36239  trljat1 36236  trljat2 36237  trljat3 36238  trlne 36255  trlnidat 36243  trlnle 36256
[Crawley] p. 112Definition of automorphismdf-pautN 36061
[Crawley] p. 113Lemma Ccdlemc 36267  cdlemc3 36263  cdlemc4 36264
[Crawley] p. 113Lemma Dcdlemd 36277  cdlemd1 36268  cdlemd2 36269  cdlemd3 36270  cdlemd4 36271  cdlemd5 36272  cdlemd6 36273  cdlemd7 36274  cdlemd8 36275  cdlemd9 36276  cdleme31sde 36455  cdleme31se 36452  cdleme31se2 36453  cdleme31snd 36456  cdleme32a 36511  cdleme32b 36512  cdleme32c 36513  cdleme32d 36514  cdleme32e 36515  cdleme32f 36516  cdleme32fva 36507  cdleme32fva1 36508  cdleme32fvcl 36510  cdleme32le 36517  cdleme48fv 36569  cdleme4gfv 36577  cdleme50eq 36611  cdleme50f 36612  cdleme50f1 36613  cdleme50f1o 36616  cdleme50laut 36617  cdleme50ldil 36618  cdleme50lebi 36610  cdleme50rn 36615  cdleme50rnlem 36614  cdlemeg49le 36581  cdlemeg49lebilem 36609
[Crawley] p. 113Lemma Ecdleme 36630  cdleme00a 36279  cdleme01N 36291  cdleme02N 36292  cdleme0a 36281  cdleme0aa 36280  cdleme0b 36282  cdleme0c 36283  cdleme0cp 36284  cdleme0cq 36285  cdleme0dN 36286  cdleme0e 36287  cdleme0ex1N 36293  cdleme0ex2N 36294  cdleme0fN 36288  cdleme0gN 36289  cdleme0moN 36295  cdleme1 36297  cdleme10 36324  cdleme10tN 36328  cdleme11 36340  cdleme11a 36330  cdleme11c 36331  cdleme11dN 36332  cdleme11e 36333  cdleme11fN 36334  cdleme11g 36335  cdleme11h 36336  cdleme11j 36337  cdleme11k 36338  cdleme11l 36339  cdleme12 36341  cdleme13 36342  cdleme14 36343  cdleme15 36348  cdleme15a 36344  cdleme15b 36345  cdleme15c 36346  cdleme15d 36347  cdleme16 36355  cdleme16aN 36329  cdleme16b 36349  cdleme16c 36350  cdleme16d 36351  cdleme16e 36352  cdleme16f 36353  cdleme16g 36354  cdleme19a 36373  cdleme19b 36374  cdleme19c 36375  cdleme19d 36376  cdleme19e 36377  cdleme19f 36378  cdleme1b 36296  cdleme2 36298  cdleme20aN 36379  cdleme20bN 36380  cdleme20c 36381  cdleme20d 36382  cdleme20e 36383  cdleme20f 36384  cdleme20g 36385  cdleme20h 36386  cdleme20i 36387  cdleme20j 36388  cdleme20k 36389  cdleme20l 36392  cdleme20l1 36390  cdleme20l2 36391  cdleme20m 36393  cdleme20y 36372  cdleme20zN 36371  cdleme21 36407  cdleme21d 36400  cdleme21e 36401  cdleme22a 36410  cdleme22aa 36409  cdleme22b 36411  cdleme22cN 36412  cdleme22d 36413  cdleme22e 36414  cdleme22eALTN 36415  cdleme22f 36416  cdleme22f2 36417  cdleme22g 36418  cdleme23a 36419  cdleme23b 36420  cdleme23c 36421  cdleme26e 36429  cdleme26eALTN 36431  cdleme26ee 36430  cdleme26f 36433  cdleme26f2 36435  cdleme26f2ALTN 36434  cdleme26fALTN 36432  cdleme27N 36439  cdleme27a 36437  cdleme27cl 36436  cdleme28c 36442  cdleme3 36307  cdleme30a 36448  cdleme31fv 36460  cdleme31fv1 36461  cdleme31fv1s 36462  cdleme31fv2 36463  cdleme31id 36464  cdleme31sc 36454  cdleme31sdnN 36457  cdleme31sn 36450  cdleme31sn1 36451  cdleme31sn1c 36458  cdleme31sn2 36459  cdleme31so 36449  cdleme35a 36518  cdleme35b 36520  cdleme35c 36521  cdleme35d 36522  cdleme35e 36523  cdleme35f 36524  cdleme35fnpq 36519  cdleme35g 36525  cdleme35h 36526  cdleme35h2 36527  cdleme35sn2aw 36528  cdleme35sn3a 36529  cdleme36a 36530  cdleme36m 36531  cdleme37m 36532  cdleme38m 36533  cdleme38n 36534  cdleme39a 36535  cdleme39n 36536  cdleme3b 36299  cdleme3c 36300  cdleme3d 36301  cdleme3e 36302  cdleme3fN 36303  cdleme3fa 36306  cdleme3g 36304  cdleme3h 36305  cdleme4 36308  cdleme40m 36537  cdleme40n 36538  cdleme40v 36539  cdleme40w 36540  cdleme41fva11 36547  cdleme41sn3aw 36544  cdleme41sn4aw 36545  cdleme41snaw 36546  cdleme42a 36541  cdleme42b 36548  cdleme42c 36542  cdleme42d 36543  cdleme42e 36549  cdleme42f 36550  cdleme42g 36551  cdleme42h 36552  cdleme42i 36553  cdleme42k 36554  cdleme42ke 36555  cdleme42keg 36556  cdleme42mN 36557  cdleme42mgN 36558  cdleme43aN 36559  cdleme43bN 36560  cdleme43cN 36561  cdleme43dN 36562  cdleme5 36310  cdleme50ex 36629  cdleme50ltrn 36627  cdleme51finvN 36626  cdleme51finvfvN 36625  cdleme51finvtrN 36628  cdleme6 36311  cdleme7 36319  cdleme7a 36313  cdleme7aa 36312  cdleme7b 36314  cdleme7c 36315  cdleme7d 36316  cdleme7e 36317  cdleme7ga 36318  cdleme8 36320  cdleme8tN 36325  cdleme9 36323  cdleme9a 36321  cdleme9b 36322  cdleme9tN 36327  cdleme9taN 36326  cdlemeda 36368  cdlemedb 36367  cdlemednpq 36369  cdlemednuN 36370  cdlemefr27cl 36473  cdlemefr32fva1 36480  cdlemefr32fvaN 36479  cdlemefrs32fva 36470  cdlemefrs32fva1 36471  cdlemefs27cl 36483  cdlemefs32fva1 36493  cdlemefs32fvaN 36492  cdlemesner 36366  cdlemeulpq 36290
[Crawley] p. 114Lemma E4atex 36146  4atexlem7 36145  cdleme0nex 36360  cdleme17a 36356  cdleme17c 36358  cdleme17d 36568  cdleme17d1 36359  cdleme17d2 36565  cdleme18a 36361  cdleme18b 36362  cdleme18c 36363  cdleme18d 36365  cdleme4a 36309
[Crawley] p. 115Lemma Ecdleme21a 36395  cdleme21at 36398  cdleme21b 36396  cdleme21c 36397  cdleme21ct 36399  cdleme21f 36402  cdleme21g 36403  cdleme21h 36404  cdleme21i 36405  cdleme22gb 36364
[Crawley] p. 116Lemma Fcdlemf 36633  cdlemf1 36631  cdlemf2 36632
[Crawley] p. 116Lemma Gcdlemftr1 36637  cdlemg16 36727  cdlemg28 36774  cdlemg28a 36763  cdlemg28b 36773  cdlemg3a 36667  cdlemg42 36799  cdlemg43 36800  cdlemg44 36803  cdlemg44a 36801  cdlemg46 36805  cdlemg47 36806  cdlemg9 36704  ltrnco 36789  ltrncom 36808  tgrpabl 36821  trlco 36797
[Crawley] p. 116Definition of Gdf-tgrp 36813
[Crawley] p. 117Lemma Gcdlemg17 36747  cdlemg17b 36732
[Crawley] p. 117Definition of Edf-edring-rN 36826  df-edring 36827
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 36830
[Crawley] p. 118Remarktendopltp 36850
[Crawley] p. 118Lemma Hcdlemh 36887  cdlemh1 36885  cdlemh2 36886
[Crawley] p. 118Lemma Icdlemi 36890  cdlemi1 36888  cdlemi2 36889
[Crawley] p. 118Lemma Jcdlemj1 36891  cdlemj2 36892  cdlemj3 36893  tendocan 36894
[Crawley] p. 118Lemma Kcdlemk 37044  cdlemk1 36901  cdlemk10 36913  cdlemk11 36919  cdlemk11t 37016  cdlemk11ta 36999  cdlemk11tb 37001  cdlemk11tc 37015  cdlemk11u-2N 36959  cdlemk11u 36941  cdlemk12 36920  cdlemk12u-2N 36960  cdlemk12u 36942  cdlemk13-2N 36946  cdlemk13 36922  cdlemk14-2N 36948  cdlemk14 36924  cdlemk15-2N 36949  cdlemk15 36925  cdlemk16-2N 36950  cdlemk16 36927  cdlemk16a 36926  cdlemk17-2N 36951  cdlemk17 36928  cdlemk18-2N 36956  cdlemk18-3N 36970  cdlemk18 36938  cdlemk19-2N 36957  cdlemk19 36939  cdlemk19u 37040  cdlemk1u 36929  cdlemk2 36902  cdlemk20-2N 36962  cdlemk20 36944  cdlemk21-2N 36961  cdlemk21N 36943  cdlemk22-3 36971  cdlemk22 36963  cdlemk23-3 36972  cdlemk24-3 36973  cdlemk25-3 36974  cdlemk26-3 36976  cdlemk26b-3 36975  cdlemk27-3 36977  cdlemk28-3 36978  cdlemk29-3 36981  cdlemk3 36903  cdlemk30 36964  cdlemk31 36966  cdlemk32 36967  cdlemk33N 36979  cdlemk34 36980  cdlemk35 36982  cdlemk36 36983  cdlemk37 36984  cdlemk38 36985  cdlemk39 36986  cdlemk39u 37038  cdlemk4 36904  cdlemk41 36990  cdlemk42 37011  cdlemk42yN 37014  cdlemk43N 37033  cdlemk45 37017  cdlemk46 37018  cdlemk47 37019  cdlemk48 37020  cdlemk49 37021  cdlemk5 36906  cdlemk50 37022  cdlemk51 37023  cdlemk52 37024  cdlemk53 37027  cdlemk54 37028  cdlemk55 37031  cdlemk55u 37036  cdlemk56 37041  cdlemk5a 36905  cdlemk5auN 36930  cdlemk5u 36931  cdlemk6 36907  cdlemk6u 36932  cdlemk7 36918  cdlemk7u-2N 36958  cdlemk7u 36940  cdlemk8 36908  cdlemk9 36909  cdlemk9bN 36910  cdlemki 36911  cdlemkid 37006  cdlemkj-2N 36952  cdlemkj 36933  cdlemksat 36916  cdlemksel 36915  cdlemksv 36914  cdlemksv2 36917  cdlemkuat 36936  cdlemkuel-2N 36954  cdlemkuel-3 36968  cdlemkuel 36935  cdlemkuv-2N 36953  cdlemkuv2-2 36955  cdlemkuv2-3N 36969  cdlemkuv2 36937  cdlemkuvN 36934  cdlemkvcl 36912  cdlemky 36996  cdlemkyyN 37032  tendoex 37045
[Crawley] p. 120Remarkdva1dim 37055
[Crawley] p. 120Lemma Lcdleml1N 37046  cdleml2N 37047  cdleml3N 37048  cdleml4N 37049  cdleml5N 37050  cdleml6 37051  cdleml7 37052  cdleml8 37053  cdleml9 37054  dia1dim 37131
[Crawley] p. 120Lemma Mdia11N 37118  diaf11N 37119  dialss 37116  diaord 37117  dibf11N 37231  djajN 37207
[Crawley] p. 120Definition of isomorphism mapdiaval 37102
[Crawley] p. 121Lemma Mcdlemm10N 37188  dia2dimlem1 37134  dia2dimlem2 37135  dia2dimlem3 37136  dia2dimlem4 37137  dia2dimlem5 37138  diaf1oN 37200  diarnN 37199  dvheveccl 37182  dvhopN 37186
[Crawley] p. 121Lemma Ncdlemn 37282  cdlemn10 37276  cdlemn11 37281  cdlemn11a 37277  cdlemn11b 37278  cdlemn11c 37279  cdlemn11pre 37280  cdlemn2 37265  cdlemn2a 37266  cdlemn3 37267  cdlemn4 37268  cdlemn4a 37269  cdlemn5 37271  cdlemn5pre 37270  cdlemn6 37272  cdlemn7 37273  cdlemn8 37274  cdlemn9 37275  diclspsn 37264
[Crawley] p. 121Definition of phi(q)df-dic 37243
[Crawley] p. 122Lemma Ndih11 37335  dihf11 37337  dihjust 37287  dihjustlem 37286  dihord 37334  dihord1 37288  dihord10 37293  dihord11b 37292  dihord11c 37294  dihord2 37297  dihord2a 37289  dihord2b 37290  dihord2cN 37291  dihord2pre 37295  dihord2pre2 37296  dihordlem6 37283  dihordlem7 37284  dihordlem7b 37285
[Crawley] p. 122Definition of isomorphism mapdihffval 37300  dihfval 37301  dihval 37302
[Diestel] p. 3Section 1.1df-cusgr 26717  df-nbgr 26637
[Diestel] p. 4Section 1.1df-subgr 26572  uhgrspan1 26607  uhgrspansubgr 26595
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 26859  vtxdgoddnumeven 26858
[Diestel] p. 27Section 1.10df-ushgr 26364
[Eisenberg] p. 67Definition 5.3df-dif 3801
[Eisenberg] p. 82Definition 6.3dfom3 8828
[Eisenberg] p. 125Definition 8.21df-map 8129
[Eisenberg] p. 216Example 13.2(4)omenps 8836
[Eisenberg] p. 310Theorem 19.8cardprc 9126
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 9699
[Enderton] p. 18Axiom of Empty Setaxnul 5014
[Enderton] p. 19Definitiondf-tp 4404
[Enderton] p. 26Exercise 5unissb 4693
[Enderton] p. 26Exercise 10pwel 5143
[Enderton] p. 28Exercise 7(b)pwun 5250
[Enderton] p. 30Theorem "Distributive laws"iinin1 4813  iinin2 4812  iinun2 4808  iunin1 4807  iunin1f 29918  iunin2 4806  uniin1 29911  uniin2 29912
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4811  iundif2 4809
[Enderton] p. 32Exercise 20unineq 4109
[Enderton] p. 33Exercise 23iinuni 4832
[Enderton] p. 33Exercise 25iununi 4833
[Enderton] p. 33Exercise 24(a)iinpw 4840
[Enderton] p. 33Exercise 24(b)iunpw 7244  iunpwss 4841
[Enderton] p. 36Definitionopthwiener 5202
[Enderton] p. 38Exercise 6(a)unipw 5141
[Enderton] p. 38Exercise 6(b)pwuni 4698
[Enderton] p. 41Lemma 3Dopeluu 5161  rnex 7367  rnexg 7364
[Enderton] p. 41Exercise 8dmuni 5570  rnuni 5789
[Enderton] p. 42Definition of a functiondffun7 6154  dffun8 6155
[Enderton] p. 43Definition of function valuefunfv2 6517
[Enderton] p. 43Definition of single-rootedfuncnv 6195
[Enderton] p. 44Definition (d)dfima2 5713  dfima3 5714
[Enderton] p. 47Theorem 3Hfvco2 6524
[Enderton] p. 49Axiom of Choice (first form)ac7 9617  ac7g 9618  df-ac 9259  dfac2 9274  dfac2a 9272  dfac2b 9273  dfac3 9264  dfac7 9276
[Enderton] p. 50Theorem 3K(a)imauni 6764
[Enderton] p. 52Definitiondf-map 8129
[Enderton] p. 53Exercise 21coass 5899
[Enderton] p. 53Exercise 27dmco 5888
[Enderton] p. 53Exercise 14(a)funin 6202
[Enderton] p. 53Exercise 22(a)imass2 5746
[Enderton] p. 54Remarkixpf 8203  ixpssmap 8215
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8182
[Enderton] p. 55Axiom of Choice (second form)ac9 9627  ac9s 9637
[Enderton] p. 56Theorem 3Meqvrelref 34895  erref 8034
[Enderton] p. 57Lemma 3Neqvrelthi 34898  erthi 8063
[Enderton] p. 57Definitiondf-ec 8016
[Enderton] p. 58Definitiondf-qs 8020
[Enderton] p. 61Exercise 35df-ec 8016
[Enderton] p. 65Exercise 56(a)dmun 5567
[Enderton] p. 68Definition of successordf-suc 5973
[Enderton] p. 71Definitiondf-tr 4978  dftr4 4982
[Enderton] p. 72Theorem 4Eunisuc 6043
[Enderton] p. 73Exercise 6unisuc 6043
[Enderton] p. 73Exercise 5(a)truni 4991
[Enderton] p. 73Exercise 5(b)trint 4993  trintALT 39930
[Enderton] p. 79Theorem 4I(A1)nna0 7956
[Enderton] p. 79Theorem 4I(A2)nnasuc 7958  onasuc 7880
[Enderton] p. 79Definition of operation valuedf-ov 6913
[Enderton] p. 80Theorem 4J(A1)nnm0 7957
[Enderton] p. 80Theorem 4J(A2)nnmsuc 7959  onmsuc 7881
[Enderton] p. 81Theorem 4K(1)nnaass 7974
[Enderton] p. 81Theorem 4K(2)nna0r 7961  nnacom 7969
[Enderton] p. 81Theorem 4K(3)nndi 7975
[Enderton] p. 81Theorem 4K(4)nnmass 7976
[Enderton] p. 81Theorem 4K(5)nnmcom 7978
[Enderton] p. 82Exercise 16nnm0r 7962  nnmsucr 7977
[Enderton] p. 88Exercise 23nnaordex 7990
[Enderton] p. 129Definitiondf-en 8229
[Enderton] p. 132Theorem 6B(b)canth 6868
[Enderton] p. 133Exercise 1xpomen 9158
[Enderton] p. 133Exercise 2qnnen 15323
[Enderton] p. 134Theorem (Pigeonhole Principle)php 8419
[Enderton] p. 135Corollary 6Cphp3 8421
[Enderton] p. 136Corollary 6Enneneq 8418
[Enderton] p. 136Corollary 6D(a)pssinf 8445
[Enderton] p. 136Corollary 6D(b)ominf 8447
[Enderton] p. 137Lemma 6Fpssnn 8453
[Enderton] p. 138Corollary 6Gssfi 8455
[Enderton] p. 139Theorem 6H(c)mapen 8399
[Enderton] p. 142Theorem 6I(3)xpcdaen 9327
[Enderton] p. 142Theorem 6I(4)mapcdaen 9328
[Enderton] p. 143Theorem 6Jcda0en 9323  cda1en 9319
[Enderton] p. 144Exercise 13iunfi 8529  unifi 8530  unifi2 8531
[Enderton] p. 144Corollary 6Kundif2 4269  unfi 8502  unfi2 8504
[Enderton] p. 145Figure 38ffoss 7394
[Enderton] p. 145Definitiondf-dom 8230
[Enderton] p. 146Example 1domen 8241  domeng 8242
[Enderton] p. 146Example 3nndomo 8429  nnsdom 8835  nnsdomg 8494
[Enderton] p. 149Theorem 6L(a)cdadom2 9331
[Enderton] p. 149Theorem 6L(c)mapdom1 8400  xpdom1 8334  xpdom1g 8332  xpdom2g 8331
[Enderton] p. 149Theorem 6L(d)mapdom2 8406
[Enderton] p. 151Theorem 6Mzorn 9651  zorng 9648
[Enderton] p. 151Theorem 6M(4)ac8 9636  dfac5 9271
[Enderton] p. 159Theorem 6Qunictb 9719
[Enderton] p. 164Exampleinfdif 9353
[Enderton] p. 168Definitiondf-po 5265
[Enderton] p. 192Theorem 7M(a)oneli 6074
[Enderton] p. 192Theorem 7M(b)ontr1 6013
[Enderton] p. 192Theorem 7M(c)onirri 6073
[Enderton] p. 193Corollary 7N(b)0elon 6020
[Enderton] p. 193Corollary 7N(c)onsuci 7304
[Enderton] p. 193Corollary 7N(d)ssonunii 7253
[Enderton] p. 194Remarkonprc 7250
[Enderton] p. 194Exercise 16suc11 6070
[Enderton] p. 197Definitiondf-card 9085
[Enderton] p. 197Theorem 7Pcarden 9695
[Enderton] p. 200Exercise 25tfis 7320
[Enderton] p. 202Lemma 7Tr1tr 8923
[Enderton] p. 202Definitiondf-r1 8911
[Enderton] p. 202Theorem 7Qr1val1 8933
[Enderton] p. 204Theorem 7V(b)rankval4 9014
[Enderton] p. 206Theorem 7X(b)en2lp 8786
[Enderton] p. 207Exercise 30rankpr 9004  rankprb 8998  rankpw 8990  rankpwi 8970  rankuniss 9013
[Enderton] p. 207Exercise 34opthreg 8797
[Enderton] p. 208Exercise 35suc11reg 8800
[Enderton] p. 212Definition of alephalephval3 9253
[Enderton] p. 213Theorem 8A(a)alephord2 9219
[Enderton] p. 213Theorem 8A(b)cardalephex 9233
[Enderton] p. 218Theorem Schema 8Eonfununi 7709
[Enderton] p. 222Definition of kardkarden 9042  kardex 9041
[Enderton] p. 238Theorem 8Roeoa 7949
[Enderton] p. 238Theorem 8Soeoe 7951
[Enderton] p. 240Exercise 25oarec 7914
[Enderton] p. 257Definition of cofinalitycflm 9394
[FaureFrolicher] p. 57Definition 3.1.9mreexd 16662
[FaureFrolicher] p. 83Definition 4.1.1df-mri 16608
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 17537  mrieqv2d 16659  mrieqvd 16658
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 16663
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 16668  mreexexlem2d 16665
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 17543  mreexfidimd 16670
[Frege1879] p. 11Statementdf3or2 38896
[Frege1879] p. 12Statementdf3an2 38897  dfxor4 38894  dfxor5 38895
[Frege1879] p. 26Axiom 1ax-frege1 38919
[Frege1879] p. 26Axiom 2ax-frege2 38920
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 38924
[Frege1879] p. 31Proposition 4frege4 38928
[Frege1879] p. 32Proposition 5frege5 38929
[Frege1879] p. 33Proposition 6frege6 38935
[Frege1879] p. 34Proposition 7frege7 38937
[Frege1879] p. 35Axiom 8ax-frege8 38938  axfrege8 38936
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 33809
[Frege1879] p. 35Proposition 9frege9 38941
[Frege1879] p. 36Proposition 10frege10 38949
[Frege1879] p. 36Proposition 11frege11 38943
[Frege1879] p. 37Proposition 12frege12 38942
[Frege1879] p. 37Proposition 13frege13 38951
[Frege1879] p. 37Proposition 14frege14 38952
[Frege1879] p. 38Proposition 15frege15 38955
[Frege1879] p. 38Proposition 16frege16 38945
[Frege1879] p. 39Proposition 17frege17 38950
[Frege1879] p. 39Proposition 18frege18 38947
[Frege1879] p. 39Proposition 19frege19 38953
[Frege1879] p. 40Proposition 20frege20 38957
[Frege1879] p. 40Proposition 21frege21 38956
[Frege1879] p. 41Proposition 22frege22 38948
[Frege1879] p. 42Proposition 23frege23 38954
[Frege1879] p. 42Proposition 24frege24 38944
[Frege1879] p. 42Proposition 25frege25 38946  rp-frege25 38934
[Frege1879] p. 42Proposition 26frege26 38939
[Frege1879] p. 43Axiom 28ax-frege28 38959
[Frege1879] p. 43Proposition 27frege27 38940
[Frege1879] p. 43Proposition 28con3 151
[Frege1879] p. 43Proposition 29frege29 38960
[Frege1879] p. 44Axiom 31ax-frege31 38963  axfrege31 38962
[Frege1879] p. 44Proposition 30frege30 38961
[Frege1879] p. 44Proposition 31notnotr 128
[Frege1879] p. 44Proposition 32frege32 38964
[Frege1879] p. 44Proposition 33frege33 38965
[Frege1879] p. 45Proposition 34frege34 38966
[Frege1879] p. 45Proposition 35frege35 38967
[Frege1879] p. 45Proposition 36frege36 38968
[Frege1879] p. 46Proposition 37frege37 38969
[Frege1879] p. 46Proposition 38frege38 38970
[Frege1879] p. 46Proposition 39frege39 38971
[Frege1879] p. 46Proposition 40frege40 38972
[Frege1879] p. 47Axiom 41ax-frege41 38974  axfrege41 38973
[Frege1879] p. 47Proposition 41notnot 139
[Frege1879] p. 47Proposition 42frege42 38975
[Frege1879] p. 47Proposition 43frege43 38976
[Frege1879] p. 47Proposition 44frege44 38977
[Frege1879] p. 47Proposition 45frege45 38978
[Frege1879] p. 48Proposition 46frege46 38979
[Frege1879] p. 48Proposition 47frege47 38980
[Frege1879] p. 49Proposition 48frege48 38981
[Frege1879] p. 49Proposition 49frege49 38982
[Frege1879] p. 49Proposition 50frege50 38983
[Frege1879] p. 50Axiom 52ax-frege52a 38986  ax-frege52c 39017  frege52aid 38987  frege52b 39018
[Frege1879] p. 50Axiom 54ax-frege54a 38991  ax-frege54c 39021  frege54b 39022
[Frege1879] p. 50Proposition 51frege51 38984
[Frege1879] p. 50Proposition 52dfsbcq 3664
[Frege1879] p. 50Proposition 53frege53a 38989  frege53aid 38988  frege53b 39019  frege53c 39043
[Frege1879] p. 50Proposition 54biid 253  eqid 2825
[Frege1879] p. 50Proposition 55frege55a 38997  frege55aid 38994  frege55b 39026  frege55c 39047  frege55cor1a 38998  frege55lem2a 38996  frege55lem2b 39025  frege55lem2c 39046
[Frege1879] p. 50Proposition 56frege56a 39000  frege56aid 38999  frege56b 39027  frege56c 39048
[Frege1879] p. 51Axiom 58ax-frege58a 39004  ax-frege58b 39030  frege58bid 39031  frege58c 39050
[Frege1879] p. 51Proposition 57frege57a 39002  frege57aid 39001  frege57b 39028  frege57c 39049
[Frege1879] p. 51Proposition 58spsbc 3675
[Frege1879] p. 51Proposition 59frege59a 39006  frege59b 39033  frege59c 39051
[Frege1879] p. 52Proposition 60frege60a 39007  frege60b 39034  frege60c 39052
[Frege1879] p. 52Proposition 61frege61a 39008  frege61b 39035  frege61c 39053
[Frege1879] p. 52Proposition 62frege62a 39009  frege62b 39036  frege62c 39054
[Frege1879] p. 52Proposition 63frege63a 39010  frege63b 39037  frege63c 39055
[Frege1879] p. 53Proposition 64frege64a 39011  frege64b 39038  frege64c 39056
[Frege1879] p. 53Proposition 65frege65a 39012  frege65b 39039  frege65c 39057
[Frege1879] p. 54Proposition 66frege66a 39013  frege66b 39040  frege66c 39058
[Frege1879] p. 54Proposition 67frege67a 39014  frege67b 39041  frege67c 39059
[Frege1879] p. 54Proposition 68frege68a 39015  frege68b 39042  frege68c 39060
[Frege1879] p. 55Definition 69dffrege69 39061
[Frege1879] p. 58Proposition 70frege70 39062
[Frege1879] p. 59Proposition 71frege71 39063
[Frege1879] p. 59Proposition 72frege72 39064
[Frege1879] p. 59Proposition 73frege73 39065
[Frege1879] p. 60Definition 76dffrege76 39068
[Frege1879] p. 60Proposition 74frege74 39066
[Frege1879] p. 60Proposition 75frege75 39067
[Frege1879] p. 62Proposition 77frege77 39069  frege77d 38874
[Frege1879] p. 63Proposition 78frege78 39070
[Frege1879] p. 63Proposition 79frege79 39071
[Frege1879] p. 63Proposition 80frege80 39072
[Frege1879] p. 63Proposition 81frege81 39073  frege81d 38875
[Frege1879] p. 64Proposition 82frege82 39074
[Frege1879] p. 65Proposition 83frege83 39075  frege83d 38876
[Frege1879] p. 65Proposition 84frege84 39076
[Frege1879] p. 66Proposition 85frege85 39077
[Frege1879] p. 66Proposition 86frege86 39078
[Frege1879] p. 66Proposition 87frege87 39079  frege87d 38878
[Frege1879] p. 67Proposition 88frege88 39080
[Frege1879] p. 68Proposition 89frege89 39081
[Frege1879] p. 68Proposition 90frege90 39082
[Frege1879] p. 68Proposition 91frege91 39083  frege91d 38879
[Frege1879] p. 69Proposition 92frege92 39084
[Frege1879] p. 70Proposition 93frege93 39085
[Frege1879] p. 70Proposition 94frege94 39086
[Frege1879] p. 70Proposition 95frege95 39087
[Frege1879] p. 71Definition 99dffrege99 39091
[Frege1879] p. 71Proposition 96frege96 39088  frege96d 38877
[Frege1879] p. 71Proposition 97frege97 39089  frege97d 38880
[Frege1879] p. 71Proposition 98frege98 39090  frege98d 38881
[Frege1879] p. 72Proposition 100frege100 39092
[Frege1879] p. 72Proposition 101frege101 39093
[Frege1879] p. 72Proposition 102frege102 39094  frege102d 38882
[Frege1879] p. 73Proposition 103frege103 39095
[Frege1879] p. 73Proposition 104frege104 39096
[Frege1879] p. 73Proposition 105frege105 39097
[Frege1879] p. 73Proposition 106frege106 39098  frege106d 38883
[Frege1879] p. 74Proposition 107frege107 39099
[Frege1879] p. 74Proposition 108frege108 39100  frege108d 38884
[Frege1879] p. 74Proposition 109frege109 39101  frege109d 38885
[Frege1879] p. 75Proposition 110frege110 39102
[Frege1879] p. 75Proposition 111frege111 39103  frege111d 38887
[Frege1879] p. 76Proposition 112frege112 39104
[Frege1879] p. 76Proposition 113frege113 39105
[Frege1879] p. 76Proposition 114frege114 39106  frege114d 38886
[Frege1879] p. 77Definition 115dffrege115 39107
[Frege1879] p. 77Proposition 116frege116 39108
[Frege1879] p. 78Proposition 117frege117 39109
[Frege1879] p. 78Proposition 118frege118 39110
[Frege1879] p. 78Proposition 119frege119 39111
[Frege1879] p. 78Proposition 120frege120 39112
[Frege1879] p. 79Proposition 121frege121 39113
[Frege1879] p. 79Proposition 122frege122 39114  frege122d 38888
[Frege1879] p. 79Proposition 123frege123 39115
[Frege1879] p. 80Proposition 124frege124 39116  frege124d 38889
[Frege1879] p. 81Proposition 125frege125 39117
[Frege1879] p. 81Proposition 126frege126 39118  frege126d 38890
[Frege1879] p. 82Proposition 127frege127 39119
[Frege1879] p. 83Proposition 128frege128 39120
[Frege1879] p. 83Proposition 129frege129 39121  frege129d 38891
[Frege1879] p. 84Proposition 130frege130 39122
[Frege1879] p. 85Proposition 131frege131 39123  frege131d 38892
[Frege1879] p. 86Proposition 132frege132 39124
[Frege1879] p. 86Proposition 133frege133 39125  frege133d 38893
[Fremlin1] p. 13Definition 111G (b)df-salgen 41318
[Fremlin1] p. 13Definition 111G (d)borelmbl 41638
[Fremlin1] p. 13Proposition 111G (b)salgenss 41339
[Fremlin1] p. 14Definition 112Aismea 41453
[Fremlin1] p. 15Remark 112B (d)psmeasure 41473
[Fremlin1] p. 15Property 112C (a)meadjun 41464  meadjunre 41478
[Fremlin1] p. 15Property 112C (b)meassle 41465
[Fremlin1] p. 15Property 112C (c)meaunle 41466
[Fremlin1] p. 16Property 112C (d)iundjiun 41462  meaiunle 41471  meaiunlelem 41470
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 41483  meaiuninc2 41484  meaiuninc3 41487  meaiuninc3v 41486  meaiunincf 41485  meaiuninclem 41482
[Fremlin1] p. 16Proposition 112C (f)meaiininc 41489  meaiininc2 41490  meaiininclem 41488
[Fremlin1] p. 19Theorem 113Ccaragen0 41508  caragendifcl 41516  caratheodory 41530  omelesplit 41520
[Fremlin1] p. 19Definition 113Aisome 41496  isomennd 41533  isomenndlem 41532
[Fremlin1] p. 19Remark 113B (c)omeunle 41518
[Fremlin1] p. 19Definition 112Dfcaragencmpl 41537  voncmpl 41623
[Fremlin1] p. 19Definition 113A (ii)omessle 41500
[Fremlin1] p. 20Theorem 113Ccarageniuncl 41525  carageniuncllem1 41523  carageniuncllem2 41524  caragenuncl 41515  caragenuncllem 41514  caragenunicl 41526
[Fremlin1] p. 21Remark 113Dcaragenel2d 41534
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 41528  caratheodorylem2 41529
[Fremlin1] p. 21Exercise 113Xacaragencmpl 41537
[Fremlin1] p. 23Lemma 114Bhoidmv1le 41596  hoidmv1lelem1 41593  hoidmv1lelem2 41594  hoidmv1lelem3 41595
[Fremlin1] p. 25Definition 114Eisvonmbl 41640
[Fremlin1] p. 29Lemma 115Bhoidmv1le 41596  hoidmvle 41602  hoidmvlelem1 41597  hoidmvlelem2 41598  hoidmvlelem3 41599  hoidmvlelem4 41600  hoidmvlelem5 41601  hsphoidmvle2 41587  hsphoif 41578  hsphoival 41581
[Fremlin1] p. 29Definition 1135 (b)hoicvr 41550
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 41558
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 41585  hoidmvn0val 41586  hoidmvval 41579  hoidmvval0 41589  hoidmvval0b 41592
[Fremlin1] p. 30Lemma 115Bhoiprodp1 41590  hsphoidmvle 41588
[Fremlin1] p. 30Definition 115Cdf-ovoln 41539  df-voln 41541
[Fremlin1] p. 30Proposition 115D (a)dmovn 41606  ovn0 41568  ovn0lem 41567  ovnf 41565  ovnome 41575  ovnssle 41563  ovnsslelem 41562  ovnsupge0 41559
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 41605  ovnhoilem1 41603  ovnhoilem2 41604  vonhoi 41669
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 41622  hoidifhspf 41620  hoidifhspval 41610  hoidifhspval2 41617  hoidifhspval3 41621  hspmbl 41631  hspmbllem1 41628  hspmbllem2 41629  hspmbllem3 41630
[Fremlin1] p. 31Definition 115Evoncmpl 41623  vonmea 41576
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 41574  ovnsubadd2 41648  ovnsubadd2lem 41647  ovnsubaddlem1 41572  ovnsubaddlem2 41573
[Fremlin1] p. 32Proposition 115G (a)hoimbl 41633  hoimbl2 41667  hoimbllem 41632  hspdifhsp 41618  opnvonmbl 41636  opnvonmbllem2 41635
[Fremlin1] p. 32Proposition 115G (b)borelmbl 41638
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 41681  iccvonmbllem 41680  ioovonmbl 41679
[Fremlin1] p. 32Proposition 115G (d)vonicc 41687  vonicclem2 41686  vonioo 41684  vonioolem2 41683  vonn0icc 41690  vonn0icc2 41694  vonn0ioo 41689  vonn0ioo2 41692
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 41691  snvonmbl 41688  vonct 41695  vonsn 41693
[Fremlin1] p. 35Lemma 121Asubsalsal 41362
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 41361  subsaliuncllem 41360
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 41722  salpreimalegt 41708  salpreimaltle 41723
[Fremlin1] p. 35Proposition 121B (i)issmf 41725  issmff 41731  issmflem 41724
[Fremlin1] p. 35Proposition 121B (ii)issmfle 41742  issmflelem 41741  smfpreimale 41751
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 41753  issmfgtlem 41752
[Fremlin1] p. 36Definition 121Cdf-smblfn 41698  issmf 41725  issmff 41731  issmfge 41766  issmfgelem 41765  issmfgt 41753  issmfgtlem 41752  issmfle 41742  issmflelem 41741  issmflem 41724
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 41706  salpreimagtlt 41727  salpreimalelt 41726
[Fremlin1] p. 36Proposition 121B (iv)issmfge 41766  issmfgelem 41765
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 41750
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 41748  cnfsmf 41737
[Fremlin1] p. 36Proposition 121D (c)decsmf 41763  decsmflem 41762  incsmf 41739  incsmflem 41738
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 41702  pimconstlt1 41703  smfconst 41746
[Fremlin1] p. 37Proposition 121E (b)smfadd 41761  smfaddlem1 41759  smfaddlem2 41760
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 41791
[Fremlin1] p. 37Proposition 121E (d)smfmul 41790  smfmullem1 41786  smfmullem2 41787  smfmullem3 41788  smfmullem4 41789
[Fremlin1] p. 37Proposition 121E (e)smfdiv 41792
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 41795  smfpimbor1lem2 41794
[Fremlin1] p. 37Proposition 121E (g)smfco 41797
[Fremlin1] p. 37Proposition 121E (h)smfres 41785
[Fremlin1] p. 38Proposition 121E (e)smfrec 41784
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 41793  smfresal 41783
[Fremlin1] p. 38Proposition 121F (a)smflim 41773  smflim2 41800  smflimlem1 41767  smflimlem2 41768  smflimlem3 41769  smflimlem4 41770  smflimlem5 41771  smflimlem6 41772  smflimmpt 41804
[Fremlin1] p. 38Proposition 121F (b)smfsup 41808  smfsuplem1 41805  smfsuplem2 41806  smfsuplem3 41807  smfsupmpt 41809  smfsupxr 41810
[Fremlin1] p. 38Proposition 121F (c)smfinf 41812  smfinflem 41811  smfinfmpt 41813
[Fremlin1] p. 39Remark 121Gsmflim 41773  smflim2 41800  smflimmpt 41804
[Fremlin1] p. 39Proposition 121Fsmfpimcc 41802
[Fremlin1] p. 39Proposition 121F (d)smflimsup 41822  smflimsuplem2 41815  smflimsuplem6 41819  smflimsuplem7 41820  smflimsuplem8 41821  smflimsupmpt 41823
[Fremlin1] p. 39Proposition 121F (e)smfliminf 41825  smfliminflem 41824  smfliminfmpt 41826
[Fremlin1] p. 80Definition 135E (b)df-smblfn 41698
[Fremlin5] p. 193Proposition 563Gbnulmbl2 23709
[Fremlin5] p. 213Lemma 565Cauniioovol 23752
[Fremlin5] p. 214Lemma 565Cauniioombl 23762
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 34028
[Fremlin5] p. 220Theorem 565Maftc1anc 34031
[FreydScedrov] p. 283Axiom of Infinityax-inf 8819  inf1 8803  inf2 8804
[Gleason] p. 117Proposition 9-2.1df-enq 10055  enqer 10065
[Gleason] p. 117Proposition 9-2.2df-1nq 10060  df-nq 10056
[Gleason] p. 117Proposition 9-2.3df-plpq 10052  df-plq 10058
[Gleason] p. 119Proposition 9-2.4caovmo 7136  df-mpq 10053  df-mq 10059
[Gleason] p. 119Proposition 9-2.5df-rq 10061
[Gleason] p. 119Proposition 9-2.6ltexnq 10119
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10120  ltbtwnnq 10122
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10115
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10116
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10123
[Gleason] p. 121Definition 9-3.1df-np 10125
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10137
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10139
[Gleason] p. 122Definitiondf-1p 10126
[Gleason] p. 122Remark (1)prub 10138
[Gleason] p. 122Lemma 9-3.4prlem934 10177
[Gleason] p. 122Proposition 9-3.2df-ltp 10129
[Gleason] p. 122Proposition 9-3.3ltsopr 10176  psslinpr 10175  supexpr 10198  suplem1pr 10196  suplem2pr 10197
[Gleason] p. 123Proposition 9-3.5addclpr 10162  addclprlem1 10160  addclprlem2 10161  df-plp 10127
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10166
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10165
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10178
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10187  ltexprlem1 10180  ltexprlem2 10181  ltexprlem3 10182  ltexprlem4 10183  ltexprlem5 10184  ltexprlem6 10185  ltexprlem7 10186
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10189  ltaprlem 10188
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10190
[Gleason] p. 124Lemma 9-3.6prlem936 10191
[Gleason] p. 124Proposition 9-3.7df-mp 10128  mulclpr 10164  mulclprlem 10163  reclem2pr 10192
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10173
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10168
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10167
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10172
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10195  reclem3pr 10193  reclem4pr 10194
[Gleason] p. 126Proposition 9-4.1df-enr 10199  enrer 10207
[Gleason] p. 126Proposition 9-4.2df-0r 10204  df-1r 10205  df-nr 10200
[Gleason] p. 126Proposition 9-4.3df-mr 10202  df-plr 10201  negexsr 10246  recexsr 10251  recexsrlem 10247
[Gleason] p. 127Proposition 9-4.4df-ltr 10203
[Gleason] p. 130Proposition 10-1.3creui 11352  creur 11351  cru 11349
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 10332  axcnre 10308
[Gleason] p. 132Definition 10-3.1crim 14239  crimd 14356  crimi 14317  crre 14238  crred 14355  crrei 14316
[Gleason] p. 132Definition 10-3.2remim 14241  remimd 14322
[Gleason] p. 133Definition 10.36absval2 14408  absval2d 14568  absval2i 14520
[Gleason] p. 133Proposition 10-3.4(a)cjadd 14265  cjaddd 14344  cjaddi 14312
[Gleason] p. 133Proposition 10-3.4(c)cjmul 14266  cjmuld 14345  cjmuli 14313
[Gleason] p. 133Proposition 10-3.4(e)cjcj 14264  cjcjd 14323  cjcji 14295
[Gleason] p. 133Proposition 10-3.4(f)cjre 14263  cjreb 14247  cjrebd 14326  cjrebi 14298  cjred 14350  rere 14246  rereb 14244  rerebd 14325  rerebi 14297  rered 14348
[Gleason] p. 133Proposition 10-3.4(h)addcj 14272  addcjd 14336  addcji 14307
[Gleason] p. 133Proposition 10-3.7(a)absval 14362
[Gleason] p. 133Proposition 10-3.7(b)abscj 14403  abscjd 14573  abscji 14524
[Gleason] p. 133Proposition 10-3.7(c)abs00 14413  abs00d 14569  abs00i 14521  absne0d 14570
[Gleason] p. 133Proposition 10-3.7(d)releabs 14445  releabsd 14574  releabsi 14525
[Gleason] p. 133Proposition 10-3.7(f)absmul 14418  absmuld 14577  absmuli 14527
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 14406  sqabsaddi 14528
[Gleason] p. 133Proposition 10-3.7(h)abstri 14454  abstrid 14579  abstrii 14531
[Gleason] p. 134Definition 10-4.10exp0e1 13166  df-exp 13162  exp0 13165  expp1 13168  expp1d 13310
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 24831  cxpaddd 24869  expadd 13203  expaddd 13311  expaddz 13205
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 24840  cxpmuld 24888  expmul 13206  expmuld 13312  expmulz 13207
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 24837  mulcxpd 24880  mulexp 13200  mulexpd 13324  mulexpz 13201
[Gleason] p. 140Exercise 1znnen 15322
[Gleason] p. 141Definition 11-2.1fzval 12628
[Gleason] p. 168Proposition 12-2.1(a)climadd 14746  rlimadd 14757  rlimdiv 14760
[Gleason] p. 168Proposition 12-2.1(b)climsub 14748  rlimsub 14758
[Gleason] p. 168Proposition 12-2.1(c)climmul 14747  rlimmul 14759
[Gleason] p. 171Corollary 12-2.2climmulc2 14751
[Gleason] p. 172Corollary 12-2.5climrecl 14698
[Gleason] p. 172Proposition 12-2.4(c)climabs 14718  climcj 14719  climim 14721  climre 14720  rlimabs 14723  rlimcj 14724  rlimim 14726  rlimre 14725
[Gleason] p. 173Definition 12-3.1df-ltxr 10403  df-xr 10402  ltxr 12242
[Gleason] p. 175Definition 12-4.1df-limsup 14586  limsupval 14589
[Gleason] p. 180Theorem 12-5.1climsup 14784
[Gleason] p. 180Theorem 12-5.3caucvg 14793  caucvgb 14794  caucvgr 14790  climcau 14785
[Gleason] p. 182Exercise 3cvgcmp 14929
[Gleason] p. 182Exercise 4cvgrat 14995
[Gleason] p. 195Theorem 13-2.12abs1m 14459
[Gleason] p. 217Lemma 13-4.1btwnzge0 12931
[Gleason] p. 223Definition 14-1.1df-met 20107
[Gleason] p. 223Definition 14-1.1(a)met0 22525  xmet0 22524
[Gleason] p. 223Definition 14-1.1(b)metgt0 22541
[Gleason] p. 223Definition 14-1.1(c)metsym 22532
[Gleason] p. 223Definition 14-1.1(d)mettri 22534  mstri 22651  xmettri 22533  xmstri 22650
[Gleason] p. 225Definition 14-1.5xpsmet 22564
[Gleason] p. 230Proposition 14-2.6txlm 21829
[Gleason] p. 240Theorem 14-4.3metcnp4 23485
[Gleason] p. 240Proposition 14-4.2metcnp3 22722
[Gleason] p. 243Proposition 14-4.16addcn 23045  addcn2 14708  mulcn 23047  mulcn2 14710  subcn 23046  subcn2 14709
[Gleason] p. 295Remarkbcval3 13393  bcval4 13394
[Gleason] p. 295Equation 2bcpasc 13408
[Gleason] p. 295Definition of binomial coefficientbcval 13391  df-bc 13390
[Gleason] p. 296Remarkbcn0 13397  bcnn 13399
[Gleason] p. 296Theorem 15-2.8binom 14943
[Gleason] p. 308Equation 2ef0 15200
[Gleason] p. 308Equation 3efcj 15201
[Gleason] p. 309Corollary 15-4.3efne0 15206
[Gleason] p. 309Corollary 15-4.4efexp 15210
[Gleason] p. 310Equation 14sinadd 15273
[Gleason] p. 310Equation 15cosadd 15274
[Gleason] p. 311Equation 17sincossq 15285
[Gleason] p. 311Equation 18cosbnd 15290  sinbnd 15289
[Gleason] p. 311Lemma 15-4.7sqeqor 13279  sqeqori 13277
[Gleason] p. 311Definition of ` `df-pi 15182
[Godowski] p. 730Equation SFgoeqi 29683
[GodowskiGreechie] p. 249Equation IV3oai 29078
[Golan] p. 1Remarksrgisid 18889
[Golan] p. 1Definitiondf-srg 18867
[Golan] p. 149Definitiondf-slmd 30295
[GramKnuthPat], p. 47Definition 2.42df-fwddif 32800
[Gratzer] p. 23Section 0.6df-mre 16606
[Gratzer] p. 27Section 0.6df-mri 16608
[Hall] p. 1Section 1.1df-asslaw 42685  df-cllaw 42683  df-comlaw 42684
[Hall] p. 2Section 1.2df-clintop 42697
[Hall] p. 7Section 1.3df-sgrp2 42718
[Halmos] p. 31Theorem 17.3riesz1 29475  riesz2 29476
[Halmos] p. 41Definition of Hermitianhmopadj2 29351
[Halmos] p. 42Definition of projector orderingpjordi 29583
[Halmos] p. 43Theorem 26.1elpjhmop 29595  elpjidm 29594  pjnmopi 29558
[Halmos] p. 44Remarkpjinormi 29097  pjinormii 29086
[Halmos] p. 44Theorem 26.2elpjch 29599  pjrn 29117  pjrni 29112  pjvec 29106
[Halmos] p. 44Theorem 26.3pjnorm2 29137
[Halmos] p. 44Theorem 26.4hmopidmpj 29564  hmopidmpji 29562
[Halmos] p. 45Theorem 27.1pjinvari 29601
[Halmos] p. 45Theorem 27.3pjoci 29590  pjocvec 29107
[Halmos] p. 45Theorem 27.4pjorthcoi 29579
[Halmos] p. 48Theorem 29.2pjssposi 29582
[Halmos] p. 48Theorem 29.3pjssdif1i 29585  pjssdif2i 29584
[Halmos] p. 50Definition of spectrumdf-spec 29265
[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 1894
[Hatcher] p. 25Definitiondf-phtpc 23168  df-phtpy 23147
[Hatcher] p. 26Definitiondf-pco 23181  df-pi1 23184
[Hatcher] p. 26Proposition 1.2phtpcer 23171
[Hatcher] p. 26Proposition 1.3pi1grp 23226
[Hefferon] p. 240Definition 3.12df-dmat 20671  df-dmatalt 43048
[Helfgott] p. 2Theoremtgoldbach 42549
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 42534
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 42546  bgoldbtbnd 42541  bgoldbtbnd 42541  tgblthelfgott 42547
[Helfgott] p. 5Proposition 1.1circlevma 31265
[Helfgott] p. 69Statement 7.49circlemethhgt 31266
[Helfgott] p. 69Statement 7.50hgt750lema 31280  hgt750lemb 31279  hgt750leme 31281  hgt750lemf 31276  hgt750lemg 31277
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 42543  tgoldbachgt 31286  tgoldbachgtALTV 42544  tgoldbachgtd 31285
[Helfgott] p. 70Statement 7.49ax-hgt749 31267
[Herstein] p. 54Exercise 28df-grpo 27899
[Herstein] p. 55Lemma 2.2.1(a)grpideu 17794  grpoideu 27915  mndideu 17664
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 17817  grpoinveu 27925
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 17843  grpo2inv 27937
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 17854  grpoinvop 27939
[Herstein] p. 57Exercise 1dfgrp3e 17876
[Hitchcock] p. 5Rule A3mptnan 1867
[Hitchcock] p. 5Rule A4mptxor 1868
[Hitchcock] p. 5Rule A5mtpxor 1870
[Holland] p. 1519Theorem 2sumdmdi 29830
[Holland] p. 1520Lemma 5cdj1i 29843  cdj3i 29851  cdj3lem1 29844  cdjreui 29842
[Holland] p. 1524Lemma 7mddmdin0i 29841
[Holland95] p. 13Theorem 3.6hlathil 38031
[Holland95] p. 14Line 15hgmapvs 37961
[Holland95] p. 14Line 16hdmaplkr 37983
[Holland95] p. 14Line 17hdmapellkr 37984
[Holland95] p. 14Line 19hdmapglnm2 37981
[Holland95] p. 14Line 20hdmapip0com 37987
[Holland95] p. 14Theorem 3.6hdmapevec2 37906
[Holland95] p. 14Lines 24 and 25hdmapoc 38001
[Holland95] p. 204Definition of involutiondf-srng 19209
[Holland95] p. 212Definition of subspacedf-psubsp 35573
[Holland95] p. 214Lemma 3.3lclkrlem2v 37598
[Holland95] p. 214Definition 3.2df-lpolN 37551
[Holland95] p. 214Definition of nonsingularpnonsingN 36003
[Holland95] p. 215Lemma 3.3(1)dihoml4 37447  poml4N 36023
[Holland95] p. 215Lemma 3.3(2)dochexmid 37538  pexmidALTN 36048  pexmidN 36039
[Holland95] p. 218Theorem 3.6lclkr 37603
[Holland95] p. 218Definition of dual vector spacedf-ldual 35194  ldualset 35195
[Holland95] p. 222Item 1df-lines 35571  df-pointsN 35572
[Holland95] p. 222Item 2df-polarityN 35973
[Holland95] p. 223Remarkispsubcl2N 36017  omllaw4 35316  pol1N 35980  polcon3N 35987
[Holland95] p. 223Definitiondf-psubclN 36005
[Holland95] p. 223Equation for polaritypolval2N 35976
[Holmes] p. 40Definitiondf-xrn 34676
[Hughes] p. 44Equation 1.21bax-his3 28492
[Hughes] p. 47Definition of projection operatordfpjop 29592
[Hughes] p. 49Equation 1.30eighmre 29373  eigre 29245  eigrei 29244
[Hughes] p. 49Equation 1.31eighmorth 29374  eigorth 29248  eigorthi 29247
[Hughes] p. 137Remark (ii)eigposi 29246
[Huneke] p. 1Claim 1frgrncvvdeq 27686
[Huneke] p. 1Statement 1frgrncvvdeqlem7 27682
[Huneke] p. 1Statement 2frgrncvvdeqlem8 27683
[Huneke] p. 1Statement 3frgrncvvdeqlem9 27684
[Huneke] p. 2Claim 2frgrregorufr 27702  frgrregorufr0 27701  frgrregorufrg 27703
[Huneke] p. 2Claim 3frgrhash2wsp 27709  frrusgrord 27718  frrusgrord0 27717
[Huneke] p. 2Statementdf-clwwlknon 27459
[Huneke] p. 2Statement 4frgrwopreglem4 27692
[Huneke] p. 2Statement 5frgrwopreg1 27695  frgrwopreg2 27696  frgrwopregasn 27693  frgrwopregbsn 27694
[Huneke] p. 2Statement 6frgrwopreglem5 27698
[Huneke] p. 2Statement 7fusgreghash2wspv 27712
[Huneke] p. 2Statement 8fusgreghash2wsp 27715
[Huneke] p. 2Statement 9clwlksndivn 27457  numclwlk1 27770  numclwlk1lem1 27768  numclwlk1lem2 27769  numclwwlk1 27755  numclwwlk8 27803
[Huneke] p. 2Definition 3frgrwopreglem1 27689
[Huneke] p. 2Definition 4df-clwlks 27080
[Huneke] p. 2Definition 62clwwlk 27727
[Huneke] p. 2Definition 7numclwwlkovh 27772  numclwwlkovh0 27771
[Huneke] p. 2Statement 10numclwwlk2 27784
[Huneke] p. 2Statement 11rusgrnumwlkg 27314
[Huneke] p. 2Statement 12numclwwlk3 27796
[Huneke] p. 2Statement 13numclwwlk5 27799
[Huneke] p. 2Statement 14numclwwlk7 27802
[Indrzejczak] p. 33Definition ` `Enatded 27814  natded 27814
[Indrzejczak] p. 33Definition ` `Inatded 27814
[Indrzejczak] p. 34Definition ` `Enatded 27814  natded 27814
[Indrzejczak] p. 34Definition ` `Inatded 27814
[Jech] p. 4Definition of classcv 1655  cvjust 2820
[Jech] p. 42Lemma 6.1alephexp1 9723
[Jech] p. 42Equation 6.1alephadd 9721  alephmul 9722
[Jech] p. 43Lemma 6.2infmap 9720  infmap2 9362
[Jech] p. 71Lemma 9.3jech9.3 8961
[Jech] p. 72Equation 9.3scott0 9033  scottex 9032
[Jech] p. 72Exercise 9.1rankval4 9014
[Jech] p. 72Scheme "Collection Principle"cp 9038
[Jech] p. 78Noteopthprc 5404
[JonesMatijasevic] p. 694Definition 2.3rmxyval 38318
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 38408
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 38409
[JonesMatijasevic] p. 695Equation 2.7rmxadd 38330
[JonesMatijasevic] p. 695Equation 2.8rmyadd 38334
[JonesMatijasevic] p. 695Equation 2.9rmxp1 38335  rmyp1 38336
[JonesMatijasevic] p. 695Equation 2.10rmxm1 38337  rmym1 38338
[JonesMatijasevic] p. 695Equation 2.11rmx0 38328  rmx1 38329  rmxluc 38339
[JonesMatijasevic] p. 695Equation 2.12rmy0 38332  rmy1 38333  rmyluc 38340
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 38342
[JonesMatijasevic] p. 695Equation 2.14rmydbl 38343
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 38365  jm2.17b 38366  jm2.17c 38367
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 38398
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 38402
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 38393
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 38368  jm2.24nn 38364
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 38407
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 38413  rmygeid 38369
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 38425
[Juillerat] p. 11Section *5etransc 41288  etransclem47 41286  etransclem48 41287
[Juillerat] p. 12Equation (7)etransclem44 41283
[Juillerat] p. 12Equation *(7)etransclem46 41285
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 41271
[Juillerat] p. 13Proofetransclem35 41274
[Juillerat] p. 13Part of case 2 proven inetransclem38 41277
[Juillerat] p. 13Part of case 2 provenetransclem24 41263
[Juillerat] p. 13Part of case 2: proven inetransclem41 41280
[Juillerat] p. 14Proofetransclem23 41262
[KalishMontague] p. 81Note 1ax-6 2075
[KalishMontague] p. 85Lemma 2equid 2116
[KalishMontague] p. 85Lemma 3equcomi 2121
[KalishMontague] p. 86Lemma 7cbvalivw 2111  cbvaliw 2110  wl-cbvmotv 33836  wl-motae 33838  wl-moteq 33837
[KalishMontague] p. 87Lemma 8spimvw 2103  spimw 2102
[KalishMontague] p. 87Lemma 9spfw 2140  spw 2141
[Kalmbach] p. 14Definition of latticechabs1 28926  chabs1i 28928  chabs2 28927  chabs2i 28929  chjass 28943  chjassi 28896  latabs1 17447  latabs2 17448
[Kalmbach] p. 15Definition of atomdf-at 29748  ela 29749
[Kalmbach] p. 15Definition of coverscvbr2 29693  cvrval2 35344
[Kalmbach] p. 16Definitiondf-ol 35248  df-oml 35249
[Kalmbach] p. 20Definition of commutescmbr 28994  cmbri 29000  cmtvalN 35281  df-cm 28993  df-cmtN 35247
[Kalmbach] p. 22Remarkomllaw5N 35317  pjoml5 29023  pjoml5i 28998
[Kalmbach] p. 22Definitionpjoml2 29021  pjoml2i 28995
[Kalmbach] p. 22Theorem 2(v)cmcm 29024  cmcmi 29002  cmcmii 29007  cmtcomN 35319
[Kalmbach] p. 22Theorem 2(ii)omllaw3 35315  omlsi 28814  pjoml 28846  pjomli 28845
[Kalmbach] p. 22Definition of OML lawomllaw2N 35314
[Kalmbach] p. 23Remarkcmbr2i 29006  cmcm3 29025  cmcm3i 29004  cmcm3ii 29009  cmcm4i 29005  cmt3N 35321  cmt4N 35322  cmtbr2N 35323
[Kalmbach] p. 23Lemma 3cmbr3 29018  cmbr3i 29010  cmtbr3N 35324
[Kalmbach] p. 25Theorem 5fh1 29028  fh1i 29031  fh2 29029  fh2i 29032  omlfh1N 35328
[Kalmbach] p. 65Remarkchjatom 29767  chslej 28908  chsleji 28868  shslej 28790  shsleji 28780
[Kalmbach] p. 65Proposition 1chocin 28905  chocini 28864  chsupcl 28750  chsupval2 28820  h0elch 28663  helch 28651  hsupval2 28819  ocin 28706  ococss 28703  shococss 28704
[Kalmbach] p. 65Definition of subspace sumshsval 28722
[Kalmbach] p. 66Remarkdf-pjh 28805  pjssmi 29575  pjssmii 29091
[Kalmbach] p. 67Lemma 3osum 29055  osumi 29052
[Kalmbach] p. 67Lemma 4pjci 29610
[Kalmbach] p. 103Exercise 6atmd2 29810
[Kalmbach] p. 103Exercise 12mdsl0 29720
[Kalmbach] p. 140Remarkhatomic 29770  hatomici 29769  hatomistici 29772
[Kalmbach] p. 140Proposition 1atlatmstc 35389
[Kalmbach] p. 140Proposition 1(i)atexch 29791  lsatexch 35113
[Kalmbach] p. 140Proposition 1(ii)chcv1 29765  cvlcvr1 35409  cvr1 35480
[Kalmbach] p. 140Proposition 1(iii)cvexch 29784  cvexchi 29779  cvrexch 35490
[Kalmbach] p. 149Remark 2chrelati 29774  hlrelat 35472  hlrelat5N 35471  lrelat 35084
[Kalmbach] p. 153Exercise 5lsmcv 19508  lsmsatcv 35080  spansncv 29063  spansncvi 29062
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 35099  spansncv2 29703
[Kalmbach] p. 266Definitiondf-st 29621
[Kalmbach2] p. 8Definition of adjointdf-adjh 29259
[KanamoriPincus] p. 415Theorem 1.1fpwwe 9790  fpwwe2 9787
[KanamoriPincus] p. 416Corollary 1.3canth4 9791
[KanamoriPincus] p. 417Corollary 1.6canthp1 9798
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 9793
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 9795
[KanamoriPincus] p. 418Proposition 1.7pwfseq 9808
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 9812  gchxpidm 9813
[KanamoriPincus] p. 419Theorem 2.1gchacg 9824  gchhar 9823
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 9360  unxpwdom 8770
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 9814
[Kreyszig] p. 3Property M1metcl 22514  xmetcl 22513
[Kreyszig] p. 4Property M2meteq0 22521
[Kreyszig] p. 8Definition 1.1-8dscmet 22754
[Kreyszig] p. 12Equation 5conjmul 11075  muleqadd 11003
[Kreyszig] p. 18Definition 1.3-2mopnval 22620
[Kreyszig] p. 19Remarkmopntopon 22621
[Kreyszig] p. 19Theorem T1mopn0 22680  mopnm 22626
[Kreyszig] p. 19Theorem T2unimopn 22678
[Kreyszig] p. 19Definition of neighborhoodneibl 22683
[Kreyszig] p. 20Definition 1.3-3metcnp2 22724
[Kreyszig] p. 25Definition 1.4-1lmbr 21440  lmmbr 23433  lmmbr2 23434
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 21562
[Kreyszig] p. 28Theorem 1.4-5lmcau 23488
[Kreyszig] p. 28Definition 1.4-3iscau 23451  iscmet2 23469
[Kreyszig] p. 30Theorem 1.4-7cmetss 23491
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 21642  metelcls 23480
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 23481  metcld2 23482
[Kreyszig] p. 51Equation 2clmvneg1 23275  lmodvneg1 19269  nvinv 28045  vcm 27982
[Kreyszig] p. 51Equation 1aclm0vs 23271  lmod0vs 19259  slmd0vs 30318  vc0 27980
[Kreyszig] p. 51Equation 1blmodvs0 19260  slmdvs0 30319  vcz 27981
[Kreyszig] p. 58Definition 2.2-1imsmet 28097  ngpmet 22784  nrmmetd 22756
[Kreyszig] p. 59Equation 1imsdval 28092  imsdval2 28093  ncvspds 23337  ngpds 22785
[Kreyszig] p. 63Problem 1nmval 22771  nvnd 28094
[Kreyszig] p. 64Problem 2nmeq0 22799  nmge0 22798  nvge0 28079  nvz 28075
[Kreyszig] p. 64Problem 3nmrtri 22805  nvabs 28078
[Kreyszig] p. 91Definition 2.7-1isblo3i 28207
[Kreyszig] p. 92Equation 2df-nmoo 28151
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 28213  blocni 28211
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 28212
[Kreyszig] p. 129Definition 3.1-1cphipeq0 23380  ipeq0 20352  ipz 28125
[Kreyszig] p. 135Problem 2pythi 28256
[Kreyszig] p. 137Lemma 3-2.1(a)sii 28260
[Kreyszig] p. 144Equation 4supcvg 14969
[Kreyszig] p. 144Theorem 3.3-1minvec 23611  minveco 28291
[Kreyszig] p. 196Definition 3.9-1df-aj 28156
[Kreyszig] p. 247Theorem 4.7-2bcth 23504
[Kreyszig] p. 249Theorem 4.7-3ubth 28280
[Kreyszig] p. 470Definition of positive operator orderingleop 29533  leopg 29532
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 29551
[Kreyszig] p. 525Theorem 10.1-1htth 28326
[Kulpa] p. 547Theorempoimir 33981
[Kulpa] p. 547Equation (1)poimirlem32 33980
[Kulpa] p. 547Equation (2)poimirlem31 33979
[Kulpa] p. 548Theorembroucube 33982
[Kulpa] p. 548Equation (6)poimirlem26 33974
[Kulpa] p. 548Equation (7)poimirlem27 33975
[Kunen] p. 10Axiom 0ax6e 2402  axnul 5014
[Kunen] p. 11Axiom 3axnul 5014
[Kunen] p. 12Axiom 6zfrep6 7401
[Kunen] p. 24Definition 10.24mapval 8139  mapvalg 8137
[Kunen] p. 30Lemma 10.20fodom 9666
[Kunen] p. 31Definition 10.24mapex 8133
[Kunen] p. 95Definition 2.1df-r1 8911
[Kunen] p. 97Lemma 2.10r1elss 8953  r1elssi 8952
[Kunen] p. 107Exercise 4rankop 9005  rankopb 8999  rankuni 9010  rankxplim 9026  rankxpsuc 9029
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4753
[Lang] p. 3Definitiondf-mnd 17655
[Lang] p. 7Definitiondfgrp2e 17809
[Lang] p. 53Definitiondf-cat 16688
[Lang] p. 54Definitiondf-iso 16768
[Lang] p. 57Definitiondf-inito 17000  df-termo 17001
[Lang] p. 58Exampleirinitoringc 42930
[Lang] p. 58Statementinitoeu1 17020  termoeu1 17027
[Lang] p. 62Definitiondf-func 16877
[Lang] p. 65Definitiondf-nat 16962
[Lang] p. 91Notedf-ringc 42866
[Lang] p. 128Remarkdsmmlmod 20459
[Lang] p. 129Prooflincscm 43080  lincscmcl 43082  lincsum 43079  lincsumcl 43081
[Lang] p. 129Statementlincolss 43084
[Lang] p. 129Observationdsmmfi 20452
[Lang] p. 147Definitionsnlindsntor 43121
[Lang] p. 504Statementmat1 20628  matring 20623
[Lang] p. 504Definitiondf-mamu 20564
[Lang] p. 505Statementmamuass 20582  mamutpos 20639  matassa 20624  mattposvs 20636  tposmap 20638
[Lang] p. 513Definitionmdet1 20782  mdetf 20776
[Lang] p. 513Theorem 4.4cramer 20874
[Lang] p. 514Proposition 4.6mdetleib 20768
[Lang] p. 514Proposition 4.8mdettpos 20792
[Lang] p. 515Definitiondf-minmar1 20816  smadiadetr 20857
[Lang] p. 515Corollary 4.9mdetero 20791  mdetralt 20789
[Lang] p. 517Proposition 4.15mdetmul 20804
[Lang] p. 518Definitiondf-madu 20815
[Lang] p. 518Proposition 4.16madulid 20826  madurid 20825  matinv 20859
[Lang] p. 561Theorem 3.1cayleyhamilton 21072
[Lang], p. 561Remarkchpmatply1 21014
[Lang], p. 561Definitiondf-chpmat 21009
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 39368
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 39363
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 39369
[LeBlanc] p. 277Rule R2axnul 5014
[Levy] p. 338Axiomdf-clab 2812  df-clel 2821  df-cleq 2818
[Levy58] p. 2Definition Iisfin1-3 9530
[Levy58] p. 2Definition IIdf-fin2 9430
[Levy58] p. 2Definition Iadf-fin1a 9429
[Levy58] p. 2Definition IIIdf-fin3 9432
[Levy58] p. 3Definition Vdf-fin5 9433
[Levy58] p. 3Definition IVdf-fin4 9431
[Levy58] p. 4Definition VIdf-fin6 9434
[Levy58] p. 4Definition VIIdf-fin7 9435
[Levy58], p. 3Theorem 1fin1a2 9559
[Lipparini] p. 3Lemma 2.1.1nosepssdm 32370
[Lipparini] p. 3Lemma 2.1.4noresle 32380
[Lipparini] p. 6Proposition 4.2nosupbnd1 32394
[Lipparini] p. 6Proposition 4.3nosupbnd2 32396
[Lipparini] p. 7Theorem 5.1noetalem2 32398  noetalem3 32399
[Lopez-Astorga] p. 12Rule 1mptnan 1867
[Lopez-Astorga] p. 12Rule 2mptxor 1868
[Lopez-Astorga] p. 12Rule 3mtpxor 1870
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 29818
[Maeda] p. 168Lemma 5mdsym 29822  mdsymi 29821
[Maeda] p. 168Lemma 4(i)mdsymlem4 29816  mdsymlem6 29818  mdsymlem7 29819
[Maeda] p. 168Lemma 4(ii)mdsymlem8 29820
[MaedaMaeda] p. 1Remarkssdmd1 29723  ssdmd2 29724  ssmd1 29721  ssmd2 29722
[MaedaMaeda] p. 1Lemma 1.2mddmd2 29719
[MaedaMaeda] p. 1Definition 1.1df-dmd 29691  df-md 29690  mdbr 29704
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 29741  mdslj1i 29729  mdslj2i 29730  mdslle1i 29727  mdslle2i 29728  mdslmd1i 29739  mdslmd2i 29740
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 29731  mdsl2bi 29733  mdsl2i 29732
[MaedaMaeda] p. 2Lemma 1.6mdexchi 29745
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 29742
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 29743
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 29720
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 29725  mdsl3 29726
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 29744
[MaedaMaeda] p. 4Theorem 1.14mdcompli 29839
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 35391  hlrelat1 35470
[MaedaMaeda] p. 31Lemma 7.5lcvexch 35109
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 29746  cvmdi 29734  cvnbtwn4 29699  cvrnbtwn4 35349
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 29747
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 35410  cvp 29785  cvrp 35486  lcvp 35110
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 29809
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 29808
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 35403  hlexch4N 35462
[MaedaMaeda] p. 34Exercise 7.1atabsi 29811
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 35513
[MaedaMaeda] p. 61Definition 15.10psubN 35819  atpsubN 35823  df-pointsN 35572  pointpsubN 35821
[MaedaMaeda] p. 62Theorem 15.5df-pmap 35574  pmap11 35832  pmaple 35831  pmapsub 35838  pmapval 35827
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 35835  pmap1N 35837
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 35840  pmapglb2N 35841  pmapglb2xN 35842  pmapglbx 35839
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 35922
[MaedaMaeda] p. 67Postulate PS1ps-1 35547
[MaedaMaeda] p. 68Lemma 16.2df-padd 35866  paddclN 35912  paddidm 35911
[MaedaMaeda] p. 68Condition PS2ps-2 35548
[MaedaMaeda] p. 68Equation 16.2.1paddass 35908
[MaedaMaeda] p. 69Lemma 16.4ps-1 35547
[MaedaMaeda] p. 69Theorem 16.4ps-2 35548
[MaedaMaeda] p. 70Theorem 16.9lsmmod 18446  lsmmod2 18447  lssats 35082  shatomici 29768  shatomistici 29771  shmodi 28800  shmodsi 28799
[MaedaMaeda] p. 130Remark 29.6dmdmd 29710  mdsymlem7 29819
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 28999
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 28903
[MaedaMaeda] p. 139Remarksumdmdii 29825
[Margaris] p. 40Rule Cexlimiv 2029
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 387  df-ex 1879  df-or 879  dfbi2 468
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 27811
[Margaris] p. 59Section 14notnotrALTVD 39964
[Margaris] p. 60Theorem 8mth8 160
[Margaris] p. 60Section 14con3ALTVD 39965
[Margaris] p. 79Rule Cexinst01 39673  exinst11 39674
[Margaris] p. 89Theorem 19.219.2 2080  19.2g 2229  r19.2z 4284
[Margaris] p. 89Theorem 19.319.3 2243  rr19.3v 3564
[Margaris] p. 89Theorem 19.5alcom 2209
[Margaris] p. 89Theorem 19.6alex 1924
[Margaris] p. 89Theorem 19.7alnex 1880
[Margaris] p. 89Theorem 19.819.8a 2223
[Margaris] p. 89Theorem 19.919.9 2247  19.9h 2317  exlimd 2261  exlimdh 2321
[Margaris] p. 89Theorem 19.11excom 2212  excomim 2213
[Margaris] p. 89Theorem 19.1219.12 2359
[Margaris] p. 90Section 19conventions-labels 27812  conventions-labels 27812  conventions-labels 27812  conventions-labels 27812
[Margaris] p. 90Theorem 19.14exnal 1925
[Margaris] p. 90Theorem 19.152albi 39412  albi 1917
[Margaris] p. 90Theorem 19.1619.16 2268
[Margaris] p. 90Theorem 19.1719.17 2269
[Margaris] p. 90Theorem 19.182exbi 39414  exbi 1946
[Margaris] p. 90Theorem 19.1919.19 2272
[Margaris] p. 90Theorem 19.202alim 39411  2alimdv 2017  alimd 2255  alimdh 1916  alimdv 2015  ax-4 1908  ralimdaa 3167  ralimdv 3172  ralimdva 3171  ralimdvva 3173  sbcimdv 3724
[Margaris] p. 90Theorem 19.2119.21 2249  19.21h 2318  19.21t 2248  19.21vv 39410  alrimd 2258  alrimdd 2257  alrimdh 1964  alrimdv 2028  alrimi 2256  alrimih 1922  alrimiv 2026  alrimivv 2027  hbralrimi 3163  r19.21be 3142  r19.21bi 3141  ralrimd 3168  ralrimdv 3177  ralrimdva 3178  ralrimdvv 3182  ralrimdvva 3183  ralrimi 3166  ralrimia 40124  ralrimiv 3174  ralrimiva 3175  ralrimivv 3179  ralrimivva 3180  ralrimivvva 3181  ralrimivw 3176
[Margaris] p. 90Theorem 19.222exim 39413  2eximdv 2018  exim 1932  eximd 2259  eximdh 1965  eximdv 2016  rexim 3216  reximd2a 3221  reximdai 3220  reximdd 40148  reximddv 3226  reximddv2 3229  reximddv3 40147  reximdv 3224  reximdv2 3222  reximdva 3225  reximdvai 3223  reximdvva 3228  reximi2 3218
[Margaris] p. 90Theorem 19.2319.23 2254  19.23bi 2232  19.23h 2319  19.23t 2252  exlimdv 2032  exlimdvv 2033  exlimexi 39563  exlimiv 2029  exlimivv 2031  rexlimd3 40140  rexlimdv 3239  rexlimdv3a 3242  rexlimdva 3240  rexlimdva2 3243  rexlimdvaa 3241  rexlimdvv 3247  rexlimdvva 3248  rexlimdvw 3244  rexlimiv 3236  rexlimiva 3237  rexlimivv 3246
[Margaris] p. 90Theorem 19.2419.24 2088
[Margaris] p. 90Theorem 19.2519.25 1983
[Margaris] p. 90Theorem 19.2619.26 1972
[Margaris] p. 90Theorem 19.2719.27 2270  r19.27z 4294  r19.27zv 4295
[Margaris] p. 90Theorem 19.2819.28 2271  19.28vv 39420  r19.28z 4287  r19.28zv 4290  rr19.28v 3565
[Margaris] p. 90Theorem 19.2919.29 1976  r19.29d2r 3290  r19.29imd 3284
[Margaris] p. 90Theorem 19.3019.30 1984
[Margaris] p. 90Theorem 19.3119.31 2277  19.31vv 39418
[Margaris] p. 90Theorem 19.3219.32 2276  r19.32 41987
[Margaris] p. 90Theorem 19.3319.33-2 39416  19.33 1987
[Margaris] p. 90Theorem 19.3419.34 2089
[Margaris] p. 90Theorem 19.3519.35 1980
[Margaris] p. 90Theorem 19.3619.36 2273  19.36vv 39417  r19.36zv 4296
[Margaris] p. 90Theorem 19.3719.37 2275  19.37vv 39419  r19.37zv 4291
[Margaris] p. 90Theorem 19.3819.38 1937
[Margaris] p. 90Theorem 19.3919.39 2087
[Margaris] p. 90Theorem 19.4019.40-2 1989  19.40 1971  r19.40 3298
[Margaris] p. 90Theorem 19.4119.41 2278  19.41rg 39589
[Margaris] p. 90Theorem 19.4219.42 2280
[Margaris] p. 90Theorem 19.4319.43 1985
[Margaris] p. 90Theorem 19.4419.44 2281  r19.44zv 4293
[Margaris] p. 90Theorem 19.4519.45 2282  r19.45zv 4292
[Margaris] p. 110Exercise 2(b)eu1 2695
[Mayet] p. 370Remarkjpi 29680  largei 29677  stri 29667
[Mayet3] p. 9Definition of CH-statesdf-hst 29622  ishst 29624
[Mayet3] p. 10Theoremhstrbi 29676  hstri 29675
[Mayet3] p. 1223Theorem 4.1mayete3i 29138
[Mayet3] p. 1240Theorem 7.1mayetes3i 29139
[MegPav2000] p. 2344Theorem 3.3stcltrthi 29688
[MegPav2000] p. 2345Definition 3.4-1chintcl 28742  chsupcl 28750
[MegPav2000] p. 2345Definition 3.4-2hatomic 29770
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 29764
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 29791
[MegPav2000] p. 2366Figure 7pl42N 36053
[MegPav2002] p. 362Lemma 2.2latj31 17459  latj32 17457  latjass 17455
[Megill] p. 444Axiom C5ax-5 2009  ax5ALT 34977
[Megill] p. 444Section 7conventions 27811
[Megill] p. 445Lemma L12aecom-o 34971  ax-c11n 34958  axc11n 2447
[Megill] p. 446Lemma L17equtrr 2126
[Megill] p. 446Lemma L18ax6fromc10 34966
[Megill] p. 446Lemma L19hbnae-o 34998  hbnae 2454
[Megill] p. 447Remark 9.1df-sb 2068  sbid 2289  sbidd-misc 43368  sbidd 43367
[Megill] p. 448Remark 9.6axc14 2503
[Megill] p. 448Scheme C4'ax-c4 34954
[Megill] p. 448Scheme C5'ax-c5 34953  sp 2224
[Megill] p. 448Scheme C6'ax-11 2207
[Megill] p. 448Scheme C7'ax-c7 34955
[Megill] p. 448Scheme C8'ax-7 2112
[Megill] p. 448Scheme C9'ax-c9 34960
[Megill] p. 448Scheme C10'ax-6 2075  ax-c10 34956
[Megill] p. 448Scheme C11'ax-c11 34957
[Megill] p. 448Scheme C12'ax-8 2166
[Megill] p. 448Scheme C13'ax-9 2173
[Megill] p. 448Scheme C14'ax-c14 34961
[Megill] p. 448Scheme C15'ax-c15 34959
[Megill] p. 448Scheme C16'ax-c16 34962
[Megill] p. 448Theorem 9.4dral1-o 34974  dral1 2460  dral2-o 35000  dral2 2459  drex1 2462  drex2 2463  drsb1 2508  drsb2 2509
[Megill] p. 449Theorem 9.7sbcom2 2578  sbequ 2507  sbid2v 2545
[Megill] p. 450Example in Appendixhba1-o 34967  hba1 2325
[Mendelson] p. 35Axiom A3hirstL-ax3 41847
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3742  rspsbca 3743  stdpc4 2483
[Mendelson] p. 69Axiom 5ax-c4 34954  ra4 3749  stdpc5 2250
[Mendelson] p. 81Rule Cexlimiv 2029
[Mendelson] p. 95Axiom 6stdpc6 2132
[Mendelson] p. 95Axiom 7stdpc7 2133
[Mendelson] p. 225Axiom system NBGru 3661
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5202
[Mendelson] p. 231Exercise 4.10(k)inv1 4197
[Mendelson] p. 231Exercise 4.10(l)unv 4198
[Mendelson] p. 231Exercise 4.10(n)dfin3 4098
[Mendelson] p. 231Exercise 4.10(o)df-nul 4147
[Mendelson] p. 231Exercise 4.10(q)dfin4 4099
[Mendelson] p. 231Exercise 4.10(s)ddif 3971
[Mendelson] p. 231Definition of uniondfun3 4097
[Mendelson] p. 235Exercise 4.12(c)univ 5142
[Mendelson] p. 235Exercise 4.12(d)pwv 4657
[Mendelson] p. 235Exercise 4.12(j)pwin 5246
[Mendelson] p. 235Exercise 4.12(k)pwunss 5247
[Mendelson] p. 235Exercise 4.12(l)pwssun 5248
[Mendelson] p. 235Exercise 4.12(n)uniin 4682
[Mendelson] p. 235Exercise 4.12(p)reli 5486
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5901
[Mendelson] p. 244Proposition 4.8(g)epweon 7248
[Mendelson] p. 246Definition of successordf-suc 5973
[Mendelson] p. 250Exercise 4.36oelim2 7947
[Mendelson] p. 254Proposition 4.22(b)xpen 8398
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8319  xpsneng 8320
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8326  xpcomeng 8327
[Mendelson] p. 254Proposition 4.22(e)xpassen 8329
[Mendelson] p. 255Definitionbrsdom 8251
[Mendelson] p. 255Exercise 4.39endisj 8322
[Mendelson] p. 255Exercise 4.41mapprc 8131
[Mendelson] p. 255Exercise 4.43mapsnen 8308  mapsnend 8307
[Mendelson] p. 255Exercise 4.45mapunen 8404
[Mendelson] p. 255Exercise 4.47xpmapen 8403
[Mendelson] p. 255Exercise 4.42(a)map0e 8166
[Mendelson] p. 255Exercise 4.42(b)map1 8311
[Mendelson] p. 257Proposition 4.24(a)undom 8323
[Mendelson] p. 258Exercise 4.56(b)cdaen 9317
[Mendelson] p. 258Exercise 4.56(c)cdaassen 9326  cdacomen 9325
[Mendelson] p. 258Exercise 4.56(f)cdadom1 9330
[Mendelson] p. 258Exercise 4.56(g)xp2cda 9324
[Mendelson] p. 258Definition of cardinal sumcdaval 9314  df-cda 9312
[Mendelson] p. 266Proposition 4.34(a)oa1suc 7883
[Mendelson] p. 266Proposition 4.34(f)oaordex 7910
[Mendelson] p. 275Proposition 4.42(d)entri3 9703
[Mendelson] p. 281Definitiondf-r1 8911
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 8960
[Mendelson] p. 287Axiom system MKru 3661
[MertziosUnger] p. 152Definitiondf-frgr 27634
[MertziosUnger] p. 153Remark 1frgrconngr 27671
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 27673  vdgn1frgrv3 27674
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 27675
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 27668
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 27661  2pthfrgrrn 27659  2pthfrgrrn2 27660
[Mittelstaedt] p. 9Definitiondf-oc 28660
[Monk1] p. 22Remarkconventions 27811
[Monk1] p. 22Theorem 3.1conventions 27811
[Monk1] p. 26Theorem 2.8(vii)ssin 4061
[Monk1] p. 33Theorem 3.2(i)ssrel 5446  ssrelf 29970
[Monk1] p. 33Theorem 3.2(ii)eqrel 5447
[Monk1] p. 34Definition 3.3df-opab 4938
[Monk1] p. 36Theorem 3.7(i)coi1 5896  coi2 5897
[Monk1] p. 36Theorem 3.8(v)dm0 5575  rn0 5614
[Monk1] p. 36Theorem 3.7(ii)cnvi 5782
[Monk1] p. 37Theorem 3.13(i)relxp 5364
[Monk1] p. 37Theorem 3.13(x)dmxp 5580  rnxp 5809
[Monk1] p. 37Theorem 3.13(ii)0xp 5438  xp0 5797
[Monk1] p. 38Theorem 3.16(ii)ima0 5726
[Monk1] p. 38Theorem 3.16(viii)imai 5723
[Monk1] p. 39Theorem 3.17imaex 7371  imaexg 7370
[Monk1] p. 39Theorem 3.16(xi)imassrn 5722
[Monk1] p. 41Theorem 4.3(i)fnopfv 6605  funfvop 6583
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6489
[Monk1] p. 42Theorem 4.4(iii)fvelima 6499
[Monk1] p. 43Theorem 4.6funun 6172
[Monk1] p. 43Theorem 4.8(iv)dff13 6772  dff13f 6773
[Monk1] p. 46Theorem 4.15(v)funex 6743  funrnex 7400
[Monk1] p. 50Definition 5.4fniunfv 6765
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5865
[Monk1] p. 52Theorem 5.11(viii)ssint 4715
[Monk1] p. 52Definition 5.13 (i)1stval2 7450  df-1st 7433
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7451  df-2nd 7434
[Monk1] p. 112Theorem 15.17(v)ranksn 9001  ranksnb 8974
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9002
[Monk1] p. 112Theorem 15.17(iii)rankun 9003  rankunb 8997
[Monk1] p. 113Theorem 15.18r1val3 8985
[Monk1] p. 113Definition 15.19df-r1 8911  r1val2 8984
[Monk1] p. 117Lemmazorn2 9650  zorn2g 9647
[Monk1] p. 133Theorem 18.11cardom 9132
[Monk1] p. 133Theorem 18.12canth3 9705
[Monk1] p. 133Theorem 18.14carduni 9127
[Monk2] p. 105Axiom C4ax-4 1908
[Monk2] p. 105Axiom C7ax-7 2112
[Monk2] p. 105Axiom C8ax-12 2220  ax-c15 34959  ax12v2 2222
[Monk2] p. 108Lemma 5ax-c4 34954
[Monk2] p. 109Lemma 12ax-11 2207
[Monk2] p. 109Lemma 15equvini 2476  equvinv 2134  eqvinop 5177
[Monk2] p. 113Axiom C5-1ax-5 2009  ax5ALT 34977
[Monk2] p. 113Axiom C5-2ax-10 2192
[Monk2] p. 113Axiom C5-3ax-11 2207
[Monk2] p. 114Lemma 21sp 2224
[Monk2] p. 114Lemma 22axc4 2352  hba1-o 34967  hba1 2325
[Monk2] p. 114Lemma 23nfia1 2204
[Monk2] p. 114Lemma 24nfa2 2219  nfra2 3155
[Moore] p. 53Part Idf-mre 16606
[Munkres] p. 77Example 2distop 21177  indistop 21184  indistopon 21183
[Munkres] p. 77Example 3fctop 21186  fctop2 21187
[Munkres] p. 77Example 4cctop 21188
[Munkres] p. 78Definition of basisdf-bases 21128  isbasis3g 21131
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 16464  tgval2 21138
[Munkres] p. 79Remarktgcl 21151
[Munkres] p. 80Lemma 2.1tgval3 21145
[Munkres] p. 80Lemma 2.2tgss2 21169  tgss3 21168
[Munkres] p. 81Lemma 2.3basgen 21170  basgen2 21171
[Munkres] p. 83Exercise 3topdifinf 33737  topdifinfeq 33738  topdifinffin 33736  topdifinfindis 33734
[Munkres] p. 89Definition of subspace topologyresttop 21342
[Munkres] p. 93Theorem 6.1(1)0cld 21220  topcld 21217
[Munkres] p. 93Theorem 6.1(2)iincld 21221
[Munkres] p. 93Theorem 6.1(3)uncld 21223
[Munkres] p. 94Definition of closureclsval 21219
[Munkres] p. 94Definition of interiorntrval 21218
[Munkres] p. 95Theorem 6.5(a)clsndisj 21257  elcls 21255
[Munkres] p. 95Theorem 6.5(b)elcls3 21265
[Munkres] p. 97Theorem 6.6clslp 21330  neindisj 21299
[Munkres] p. 97Corollary 6.7cldlp 21332
[Munkres] p. 97Definition of limit pointislp2 21327  lpval 21321
[Munkres] p. 98Definition of Hausdorff spacedf-haus 21497
[Munkres] p. 102Definition of continuous functiondf-cn 21409  iscn 21417  iscn2 21420
[Munkres] p. 107Theorem 7.2(g)cncnp 21462  cncnp2 21463  cncnpi 21460  df-cnp 21410  iscnp 21419  iscnp2 21421
[Munkres] p. 127Theorem 10.1metcn 22725
[Munkres] p. 128Theorem 10.3metcn4 23486
[Nathanson] p. 123Remarkreprgt 31244  reprinfz1 31245  reprlt 31242
[Nathanson] p. 123Definitiondf-repr 31232
[Nathanson] p. 123Chapter 5.1circlemethnat 31264
[Nathanson] p. 123Propositionbreprexp 31256  breprexpnat 31257  itgexpif 31229
[NielsenChuang] p. 195Equation 4.73unierri 29514
[OeSilva] p. 2042Section 2ax-bgbltosilva 42542
[Pfenning] p. 17Definition XMnatded 27814
[Pfenning] p. 17Definition NNCnatded 27814  notnotrd 131
[Pfenning] p. 17Definition ` `Cnatded 27814
[Pfenning] p. 18Rule"natded 27814
[Pfenning] p. 18Definition /\Inatded 27814
[Pfenning] p. 18Definition ` `Enatded 27814  natded 27814  natded 27814  natded 27814  natded 27814
[Pfenning] p. 18Definition ` `Inatded 27814  natded 27814  natded 27814  natded 27814  natded 27814
[Pfenning] p. 18Definition ` `ELnatded 27814
[Pfenning] p. 18Definition ` `ERnatded 27814
[Pfenning] p. 18Definition ` `Ea,unatded 27814
[Pfenning] p. 18Definition ` `IRnatded 27814
[Pfenning] p. 18Definition ` `Ianatded 27814
[Pfenning] p. 127Definition =Enatded 27814
[Pfenning] p. 127Definition =Inatded 27814
[Ponnusamy] p. 361Theorem 6.44cphip0l 23378  df-dip 28107  dip0l 28124  ip0l 20350
[Ponnusamy] p. 361Equation 6.45cphipval 23418  ipval 28109
[Ponnusamy] p. 362Equation I1dipcj 28120  ipcj 20348
[Ponnusamy] p. 362Equation I3cphdir 23381  dipdir 28248  ipdir 20353  ipdiri 28236
[Ponnusamy] p. 362Equation I4ipidsq 28116  nmsq 23370
[Ponnusamy] p. 362Equation 6.46ip0i 28231
[Ponnusamy] p. 362Equation 6.47ip1i 28233
[Ponnusamy] p. 362Equation 6.48ip2i 28234
[Ponnusamy] p. 363Equation I2cphass 23387  dipass 28251  ipass 20359  ipassi 28247
[Prugovecki] p. 186Definition of brabraval 29354  df-bra 29260
[Prugovecki] p. 376Equation 8.1df-kb 29261  kbval 29364
[PtakPulmannova] p. 66Proposition 3.2.17atomli 29792
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 35958
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 29806  atcvat4i 29807  cvrat3 35512  cvrat4 35513  lsatcvat3 35122
[PtakPulmannova] p. 68Definition 3.2.18cvbr 29692  cvrval 35339  df-cv 29689  df-lcv 35089  lspsncv0 19513
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 35970
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 35971
[Quine] p. 16Definition 2.1df-clab 2812  rabid 3326
[Quine] p. 17Definition 2.1''dfsb7 2589
[Quine] p. 18Definition 2.7df-cleq 2818
[Quine] p. 19Definition 2.9conventions 27811  df-v 3416
[Quine] p. 34Theorem 5.1abeq2 2937
[Quine] p. 35Theorem 5.2abid1 2949  abid2f 2996
[Quine] p. 40Theorem 6.1sb5 2308
[Quine] p. 40Theorem 6.2sb56 2305  sb6 2307
[Quine] p. 41Theorem 6.3df-clel 2821
[Quine] p. 41Theorem 6.4eqid 2825  eqid1 27877
[Quine] p. 41Theorem 6.5eqcom 2832
[Quine] p. 42Theorem 6.6df-sbc 3663
[Quine] p. 42Theorem 6.7dfsbcq 3664  dfsbcq2 3665
[Quine] p. 43Theorem 6.8vex 3417
[Quine] p. 43Theorem 6.9isset 3424
[Quine] p. 44Theorem 7.3spcgf 3505  spcgv 3510  spcimgf 3503
[Quine] p. 44Theorem 6.11spsbc 3675  spsbcd 3676
[Quine] p. 44Theorem 6.12elex 3429
[Quine] p. 44Theorem 6.13elab 3571  elabg 3569  elabgf 3567
[Quine] p. 44Theorem 6.14noel 4150
[Quine] p. 48Theorem 7.2snprc 4473
[Quine] p. 48Definition 7.1df-pr 4402  df-sn 4400
[Quine] p. 49Theorem 7.4snss 4537  snssg 4536
[Quine] p. 49Theorem 7.5prss 4571  prssg 4570
[Quine] p. 49Theorem 7.6prid1 4517  prid1g 4515  prid2 4518  prid2g 4516  snid 4431  snidg 4429
[Quine] p. 51Theorem 7.12snex 5131
[Quine] p. 51Theorem 7.13prex 5132
[Quine] p. 53Theorem 8.2unisn 4676  unisnALT 39975  unisng 4675
[Quine] p. 53Theorem 8.3uniun 4681
[Quine] p. 54Theorem 8.6elssuni 4691
[Quine] p. 54Theorem 8.7uni0 4689
[Quine] p. 56Theorem 8.17uniabio 6100
[Quine] p. 56Definition 8.18dfaiota2 41977  dfiota2 6091
[Quine] p. 57Theorem 8.19aiotaval 41984  iotaval 6101
[Quine] p. 57Theorem 8.22iotanul 6105
[Quine] p. 58Theorem 8.23iotaex 6107
[Quine] p. 58Definition 9.1df-op 4406
[Quine] p. 61Theorem 9.5opabid 5210  opelopab 5225  opelopaba 5219  opelopabaf 5227  opelopabf 5228  opelopabg 5221  opelopabga 5216  opelopabgf 5223  oprabid 6941
[Quine] p. 64Definition 9.11df-xp 5352
[Quine] p. 64Definition 9.12df-cnv 5354
[Quine] p. 64Definition 9.15df-id 5252
[Quine] p. 65Theorem 10.3fun0 6191
[Quine] p. 65Theorem 10.4funi 6159
[Quine] p. 65Theorem 10.5funsn 6179  funsng 6177
[Quine] p. 65Definition 10.1df-fun 6129
[Quine] p. 65Definition 10.2args 5738  dffv4 6434
[Quine] p. 68Definition 10.11conventions 27811  df-fv 6135  fv2 6432
[Quine] p. 124Theorem 17.3nn0opth2 13359  nn0opth2i 13358  nn0opthi 13357  omopthi 8009
[Quine] p. 177Definition 25.2df-rdg 7777
[Quine] p. 232Equation icarddom 9698
[Quine] p. 284Axiom 39(vi)funimaex 6213  funimaexg 6212
[Quine] p. 331Axiom system NFru 3661
[ReedSimon] p. 36Definition (iii)ax-his3 28492
[ReedSimon] p. 63Exercise 4(a)df-dip 28107  polid 28567  polid2i 28565  polidi 28566
[ReedSimon] p. 63Exercise 4(b)df-ph 28219
[ReedSimon] p. 195Remarklnophm 29429  lnophmi 29428
[Retherford] p. 49Exercise 1(i)leopadd 29542
[Retherford] p. 49Exercise 1(ii)leopmul 29544  leopmuli 29543
[Retherford] p. 49Exercise 1(iv)leoptr 29547
[Retherford] p. 49Definition VI.1df-leop 29262  leoppos 29536
[Retherford] p. 49Exercise 1(iii)leoptri 29546
[Retherford] p. 49Definition of operator orderingleop3 29535
[Roman] p. 4Definitiondf-dmat 20671  df-dmatalt 43048
[Roman] p. 18Part Preliminariesdf-rng0 42736
[Roman] p. 19Part Preliminariesdf-ring 18910
[Roman] p. 46Theorem 1.6isldepslvec2 43135
[Roman] p. 112Noteisldepslvec2 43135  ldepsnlinc 43158  zlmodzxznm 43147
[Roman] p. 112Examplezlmodzxzequa 43146  zlmodzxzequap 43149  zlmodzxzldep 43154
[Roman] p. 170Theorem 7.8cayleyhamilton 21072
[Rosenlicht] p. 80Theoremheicant 33983
[Rosser] p. 281Definitiondf-op 4406
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 31268
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 31269
[Rotman] p. 28Remarkpgrpgt2nabl 43008  pmtr3ncom 18252
[Rotman] p. 31Theorem 3.4symggen2 18248
[Rotman] p. 42Theorem 3.15cayley 18191  cayleyth 18192
[Rudin] p. 164Equation 27efcan 15205
[Rudin] p. 164Equation 30efzval 15211
[Rudin] p. 167Equation 48absefi 15305
[Sanford] p. 39Remarkax-mp 5  mto 189
[Sanford] p. 39Rule 3mtpxor 1870
[Sanford] p. 39Rule 4mptxor 1868
[Sanford] p. 40Rule 1mptnan 1867
[Schechter] p. 51Definition of antisymmetryintasym 5757
[Schechter] p. 51Definition of irreflexivityintirr 5760
[Schechter] p. 51Definition of symmetrycnvsym 5756
[Schechter] p. 51Definition of transitivitycotr 5753
[Schechter] p. 78Definition of Moore collection of setsdf-mre 16606
[Schechter] p. 79Definition of Moore closuredf-mrc 16607
[Schechter] p. 82Section 4.5df-mrc 16607
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 16609
[Schechter] p. 139Definition AC3dfac9 9280
[Schechter] p. 141Definition (MC)dfac11 38470
[Schechter] p. 149Axiom DC1ax-dc 9590  axdc3 9598
[Schechter] p. 187Definition of ring with unitisring 18912  isrngo 34233
[Schechter] p. 276Remark 11.6.espan0 28952
[Schechter] p. 276Definition of spandf-span 28719  spanval 28743
[Schechter] p. 428Definition 15.35bastop1 21175
[Schwabhauser] p. 10Axiom A1axcgrrflx 26220  axtgcgrrflx 25781
[Schwabhauser] p. 10Axiom A2axcgrtr 26221
[Schwabhauser] p. 10Axiom A3axcgrid 26222  axtgcgrid 25782
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 25767
[Schwabhauser] p. 11Axiom A4axsegcon 26233  axtgsegcon 25783  df-trkgcb 25769
[Schwabhauser] p. 11Axiom A5ax5seg 26244  axtg5seg 25784  df-trkgcb 25769
[Schwabhauser] p. 11Axiom A6axbtwnid 26245  axtgbtwnid 25785  df-trkgb 25768
[Schwabhauser] p. 12Axiom A7axpasch 26247  axtgpasch 25786  df-trkgb 25768
[Schwabhauser] p. 12Axiom A8axlowdim2 26266  df-trkg2d 31288
[Schwabhauser] p. 13Axiom A8axtglowdim2 25789
[Schwabhauser] p. 13Axiom A9axtgupdim2 25790  df-trkg2d 31288
[Schwabhauser] p. 13Axiom A10axeuclid 26269  axtgeucl 25791  df-trkge 25770
[Schwabhauser] p. 13Axiom A11axcont 26282  axtgcont 25788  axtgcont1 25787  df-trkgb 25768
[Schwabhauser] p. 27Theorem 2.1cgrrflx 32628
[Schwabhauser] p. 27Theorem 2.2cgrcomim 32630
[Schwabhauser] p. 27Theorem 2.3cgrtr 32633
[Schwabhauser] p. 27Theorem 2.4cgrcoml 32637
[Schwabhauser] p. 27Theorem 2.5cgrcomr 32638  tgcgrcomimp 25796  tgcgrcoml 25798  tgcgrcomr 25797
[Schwabhauser] p. 28Theorem 2.8cgrtriv 32643  tgcgrtriv 25803
[Schwabhauser] p. 28Theorem 2.105segofs 32647  tg5segofs 31296
[Schwabhauser] p. 28Definition 2.10df-afs 31293  df-ofs 32624
[Schwabhauser] p. 29Theorem 2.11cgrextend 32649  tgcgrextend 25804
[Schwabhauser] p. 29Theorem 2.12segconeq 32651  tgsegconeq 25805
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 32663  btwntriv2 32653  tgbtwntriv2 25806
[Schwabhauser] p. 30Theorem 3.2btwncomim 32654  tgbtwncom 25807
[Schwabhauser] p. 30Theorem 3.3btwntriv1 32657  tgbtwntriv1 25810
[Schwabhauser] p. 30Theorem 3.4btwnswapid 32658  tgbtwnswapid 25811
[Schwabhauser] p. 30Theorem 3.5btwnexch2 32664  btwnintr 32660  tgbtwnexch2 25815  tgbtwnintr 25812
[Schwabhauser] p. 30Theorem 3.6btwnexch 32666  btwnexch3 32661  tgbtwnexch 25817  tgbtwnexch3 25813
[Schwabhauser] p. 30Theorem 3.7btwnouttr 32665  tgbtwnouttr 25816  tgbtwnouttr2 25814
[Schwabhauser] p. 32Theorem 3.13axlowdim1 26265
[Schwabhauser] p. 32Theorem 3.14btwndiff 32668  tgbtwndiff 25825
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 25818  trisegint 32669
[Schwabhauser] p. 34Theorem 4.2ifscgr 32685  tgifscgr 25827
[Schwabhauser] p. 34Theorem 4.11colcom 25877  colrot1 25878  colrot2 25879  lncom 25941  lnrot1 25942  lnrot2 25943
[Schwabhauser] p. 34Definition 4.1df-ifs 32681
[Schwabhauser] p. 35Theorem 4.3cgrsub 32686  tgcgrsub 25828
[Schwabhauser] p. 35Theorem 4.5cgrxfr 32696  tgcgrxfr 25837
[Schwabhauser] p. 35Statement 4.4ercgrg 25836
[Schwabhauser] p. 35Definition 4.4df-cgr3 32682  df-cgrg 25830
[Schwabhauser] p. 35Definition instead (givendf-cgrg 25830
[Schwabhauser] p. 36Theorem 4.6btwnxfr 32697  tgbtwnxfr 25849
[Schwabhauser] p. 36Theorem 4.11colinearperm1 32703  colinearperm2 32705  colinearperm3 32704  colinearperm4 32706  colinearperm5 32707
[Schwabhauser] p. 36Definition 4.8df-ismt 25852
[Schwabhauser] p. 36Definition 4.10df-colinear 32680  tgellng 25872  tglng 25865
[Schwabhauser] p. 37Theorem 4.12colineartriv1 32708
[Schwabhauser] p. 37Theorem 4.13colinearxfr 32716  lnxfr 25885
[Schwabhauser] p. 37Theorem 4.14lineext 32717  lnext 25886
[Schwabhauser] p. 37Theorem 4.16fscgr 32721  tgfscgr 25887
[Schwabhauser] p. 37Theorem 4.17linecgr 32722  lncgr 25888
[Schwabhauser] p. 37Definition 4.15df-fs 32683
[Schwabhauser] p. 38Theorem 4.18lineid 32724  lnid 25889
[Schwabhauser] p. 38Theorem 4.19idinside 32725  tgidinside 25890
[Schwabhauser] p. 39Theorem 5.1btwnconn1 32742  tgbtwnconn1 25894
[Schwabhauser] p. 41Theorem 5.2btwnconn2 32743  tgbtwnconn2 25895
[Schwabhauser] p. 41Theorem 5.3btwnconn3 32744  tgbtwnconn3 25896
[Schwabhauser] p. 41Theorem 5.5brsegle2 32750
[Schwabhauser] p. 41Definition 5.4df-segle 32748  legov 25904
[Schwabhauser] p. 41Definition 5.5legov2 25905
[Schwabhauser] p. 42Remark 5.13legso 25918
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 32751
[Schwabhauser] p. 42Theorem 5.7seglerflx 32753
[Schwabhauser] p. 42Theorem 5.8segletr 32755
[Schwabhauser] p. 42Theorem 5.9segleantisym 32756
[Schwabhauser] p. 42Theorem 5.10seglelin 32757
[Schwabhauser] p. 42Theorem 5.11seglemin 32754
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 32759
[Schwabhauser] p. 42Proposition 5.7legid 25906
[Schwabhauser] p. 42Proposition 5.8legtrd 25908
[Schwabhauser] p. 42Proposition 5.9legtri3 25909
[Schwabhauser] p. 42Proposition 5.10legtrid 25910
[Schwabhauser] p. 42Proposition 5.11leg0 25911
[Schwabhauser] p. 43Theorem 6.2btwnoutside 32766
[Schwabhauser] p. 43Theorem 6.3broutsideof3 32767
[Schwabhauser] p. 43Theorem 6.4broutsideof 32762  df-outsideof 32761
[Schwabhauser] p. 43Definition 6.1broutsideof2 32763  ishlg 25921
[Schwabhauser] p. 44Theorem 6.4hlln 25926
[Schwabhauser] p. 44Theorem 6.5hlid 25928  outsideofrflx 32768
[Schwabhauser] p. 44Theorem 6.6hlcomb 25922  hlcomd 25923  outsideofcom 32769
[Schwabhauser] p. 44Theorem 6.7hltr 25929  outsideoftr 32770
[Schwabhauser] p. 44Theorem 6.11hlcgreu 25937  outsideofeu 32772
[Schwabhauser] p. 44Definition 6.8df-ray 32779
[Schwabhauser] p. 45Part 2df-lines2 32780
[Schwabhauser] p. 45Theorem 6.13outsidele 32773
[Schwabhauser] p. 45Theorem 6.15lineunray 32788
[Schwabhauser] p. 45Theorem 6.16lineelsb2 32789  tglineelsb2 25951
[Schwabhauser] p. 45Theorem 6.17linecom 32791  linerflx1 32790  linerflx2 32792  tglinecom 25954  tglinerflx1 25952  tglinerflx2 25953
[Schwabhauser] p. 45Theorem 6.18linethru 32794  tglinethru 25955
[Schwabhauser] p. 45Definition 6.14df-line2 32778  tglng 25865
[Schwabhauser] p. 45Proposition 6.13legbtwn 25913
[Schwabhauser] p. 46Theorem 6.19linethrueu 32797  tglinethrueu 25958
[Schwabhauser] p. 46Theorem 6.21lineintmo 32798  tglineineq 25962  tglineinteq 25964  tglineintmo 25961
[Schwabhauser] p. 46Theorem 6.23colline 25968
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 25969
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 25970
[Schwabhauser] p. 49Theorem 7.3mirinv 25985
[Schwabhauser] p. 49Theorem 7.7mirmir 25981
[Schwabhauser] p. 49Theorem 7.8mirreu3 25973
[Schwabhauser] p. 49Definition 7.5df-mir 25972  ismir 25978  mirbtwn 25977  mircgr 25976  mirfv 25975  mirval 25974
[Schwabhauser] p. 50Theorem 7.8mirreu 25983
[Schwabhauser] p. 50Theorem 7.9mireq 25984
[Schwabhauser] p. 50Theorem 7.10mirinv 25985
[Schwabhauser] p. 50Theorem 7.11mirf1o 25988
[Schwabhauser] p. 50Theorem 7.13miriso 25989
[Schwabhauser] p. 51Theorem 7.14mirmot 25994
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 25991  mirbtwni 25990
[Schwabhauser] p. 51Theorem 7.16mircgrs 25992
[Schwabhauser] p. 51Theorem 7.17miduniq 26004
[Schwabhauser] p. 52Lemma 7.21symquadlem 26008
[Schwabhauser] p. 52Theorem 7.18miduniq1 26005
[Schwabhauser] p. 52Theorem 7.19miduniq2 26006
[Schwabhauser] p. 52Theorem 7.20colmid 26007
[Schwabhauser] p. 53Lemma 7.22krippen 26010
[Schwabhauser] p. 55Lemma 7.25midexlem 26011
[Schwabhauser] p. 57Theorem 8.2ragcom 26017
[Schwabhauser] p. 57Definition 8.1df-rag 26013  israg 26016
[Schwabhauser] p. 58Theorem 8.3ragcol 26018
[Schwabhauser] p. 58Theorem 8.4ragmir 26019
[Schwabhauser] p. 58Theorem 8.5ragtrivb 26021
[Schwabhauser] p. 58Theorem 8.6ragflat2 26022
[Schwabhauser] p. 58Theorem 8.7ragflat 26023
[Schwabhauser] p. 58Theorem 8.8ragtriva 26024
[Schwabhauser] p. 58Theorem 8.9ragflat3 26025  ragncol 26028
[Schwabhauser] p. 58Theorem 8.10ragcgr 26026
[Schwabhauser] p. 59Theorem 8.12perpcom 26032
[Schwabhauser] p. 59Theorem 8.13ragperp 26036
[Schwabhauser] p. 59Theorem 8.14perpneq 26033
[Schwabhauser] p. 59Definition 8.11df-perpg 26015  isperp 26031
[Schwabhauser] p. 59Definition 8.13isperp2 26034
[Schwabhauser] p. 60Theorem 8.18foot 26038
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 26046  colperpexlem2 26047
[Schwabhauser] p. 63Theorem 8.21colperpex 26049  colperpexlem3 26048
[Schwabhauser] p. 64Theorem 8.22mideu 26054  midex 26053
[Schwabhauser] p. 66Lemma 8.24opphllem 26051
[Schwabhauser] p. 67Theorem 9.2oppcom 26060
[Schwabhauser] p. 67Definition 9.1islnopp 26055
[Schwabhauser] p. 68Lemma 9.3opphllem2 26064
[Schwabhauser] p. 68Lemma 9.4opphllem5 26067  opphllem6 26068
[Schwabhauser] p. 69Theorem 9.5opphl 26070
[Schwabhauser] p. 69Theorem 9.6axtgpasch 25786
[Schwabhauser] p. 70Theorem 9.6outpasch 26071
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 26079
[Schwabhauser] p. 71Definition 9.7df-hpg 26074  hpgbr 26076
[Schwabhauser] p. 72Lemma 9.10hpgerlem 26081
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 26080
[Schwabhauser] p. 72Theorem 9.11hpgid 26082
[Schwabhauser] p. 72Theorem 9.12hpgcom 26083
[Schwabhauser] p. 72Theorem 9.13hpgtr 26084
[Schwabhauser] p. 73Theorem 9.18colopp 26085
[Schwabhauser] p. 73Theorem 9.19colhp 26086
[Schwabhauser] p. 88Theorem 10.2lmieu 26100
[Schwabhauser] p. 88Definition 10.1df-mid 26090
[Schwabhauser] p. 89Theorem 10.4lmicom 26104
[Schwabhauser] p. 89Theorem 10.5lmilmi 26105
[Schwabhauser] p. 89Theorem 10.6lmireu 26106
[Schwabhauser] p. 89Theorem 10.7lmieq 26107
[Schwabhauser] p. 89Theorem 10.8lmiinv 26108
[Schwabhauser] p. 89Theorem 10.9lmif1o 26111
[Schwabhauser] p. 89Theorem 10.10lmiiso 26113
[Schwabhauser] p. 89Definition 10.3df-lmi 26091
[Schwabhauser] p. 90Theorem 10.11lmimot 26114
[Schwabhauser] p. 91Theorem 10.12hypcgr 26117
[Schwabhauser] p. 92Theorem 10.14lmiopp 26118
[Schwabhauser] p. 92Theorem 10.15lnperpex 26119
[Schwabhauser] p. 92Theorem 10.16trgcopy 26120  trgcopyeu 26122
[Schwabhauser] p. 95Definition 11.2dfcgra2 26145
[Schwabhauser] p. 95Definition 11.3iscgra 26125
[Schwabhauser] p. 95Proposition 11.4cgracgr 26134
[Schwabhauser] p. 95Proposition 11.10cgrahl1 26132  cgrahl2 26133
[Schwabhauser] p. 96Theorem 11.6cgraid 26135
[Schwabhauser] p. 96Theorem 11.9cgraswap 26136
[Schwabhauser] p. 97Theorem 11.7cgracom 26138
[Schwabhauser] p. 97Theorem 11.8cgratr 26139
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 26141  cgrahl 26142
[Schwabhauser] p. 98Theorem 11.13sacgr 26146
[Schwabhauser] p. 98Theorem 11.14oacgr 26148
[Schwabhauser] p. 98Theorem 11.15acopy 26149  acopyeu 26150
[Schwabhauser] p. 101Theorem 11.24inagswap 26155
[Schwabhauser] p. 101Theorem 11.25inaghl 26156
[Schwabhauser] p. 101Property for point ` ` to lie in the angle ` ` Defnition 11.23isinag 26154
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 26159
[Schwabhauser] p. 102Definition 11.27df-leag 26157  isleag 26158
[Schwabhauser] p. 107Theorem 11.49tgsas 26161  tgsas1 26160  tgsas2 26162  tgsas3 26163
[Schwabhauser] p. 108Theorem 11.50tgasa 26165  tgasa1 26164
[Schwabhauser] p. 109Theorem 11.51tgsss1 26166  tgsss2 26167  tgsss3 26168
[Shapiro] p. 230Theorem 6.5.1dchrhash 25416  dchrsum 25414  dchrsum2 25413  sumdchr 25417
[Shapiro] p. 232Theorem 6.5.2dchr2sum 25418  sum2dchr 25419
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 18826  ablfacrp2 18827
[Shapiro], p. 328Equation 9.2.4vmasum 25361
[Shapiro], p. 329Equation 9.2.7logfac2 25362
[Shapiro], p. 329Equation 9.2.9logfacrlim 25369
[Shapiro], p. 331Equation 9.2.13vmadivsum 25591
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 25594
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 25648  vmalogdivsum2 25647
[Shapiro], p. 375Theorem 9.4.1dirith 25638  dirith2 25637
[Shapiro], p. 375Equation 9.4.3rplogsum 25636  rpvmasum 25635  rpvmasum2 25621
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 25596
[Shapiro], p. 376Equation 9.4.8dchrvmasum 25634
[Shapiro], p. 377Lemma 9.4.1dchrisum 25601  dchrisumlem1 25598  dchrisumlem2 25599  dchrisumlem3 25600  dchrisumlema 25597
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 25604
[Shapiro], p. 379Equation 9.4.16dchrmusum 25633  dchrmusumlem 25631  dchrvmasumlem 25632
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 25603
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 25605
[Shapiro], p. 382Lemma 9.4.4dchrisum0 25629  dchrisum0re 25622  dchrisumn0 25630
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 25615
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 25619
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 25620
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 25675  pntrsumbnd2 25676  pntrsumo1 25674
[Shapiro], p. 405Equation 10.2.1mudivsum 25639
[Shapiro], p. 406Equation 10.2.6mulogsum 25641
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 25643
[Shapiro], p. 407Equation 10.2.8mulog2sum 25646
[Shapiro], p. 418Equation 10.4.6logsqvma 25651
[Shapiro], p. 418Equation 10.4.8logsqvma2 25652
[Shapiro], p. 419Equation 10.4.10selberg 25657
[Shapiro], p. 420Equation 10.4.12selberg2lem 25659
[Shapiro], p. 420Equation 10.4.14selberg2 25660
[Shapiro], p. 422Equation 10.6.7selberg3 25668
[Shapiro], p. 422Equation 10.4.20selberg4lem1 25669
[Shapiro], p. 422Equation 10.4.21selberg3lem1 25666  selberg3lem2 25667
[Shapiro], p. 422Equation 10.4.23selberg4 25670
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 25664
[Shapiro], p. 428Equation 10.6.2selbergr 25677
[Shapiro], p. 429Equation 10.6.8selberg3r 25678
[Shapiro], p. 430Equation 10.6.11selberg4r 25679
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 25693
[Shapiro], p. 434Equation 10.6.27pntlema 25705  pntlemb 25706  pntlemc 25704  pntlemd 25703  pntlemg 25707
[Shapiro], p. 435Equation 10.6.29pntlema 25705
[Shapiro], p. 436Lemma 10.6.1pntpbnd 25697
[Shapiro], p. 436Lemma 10.6.2pntibnd 25702
[Shapiro], p. 436Equation 10.6.34pntlema 25705
[Shapiro], p. 436Equation 10.6.35pntlem3 25718  pntleml 25720
[Stoll] p. 13Definition corresponds to dfsymdif3 4124
[Stoll] p. 16Exercise 4.40dif 4204  dif0 4182
[Stoll] p. 16Exercise 4.8difdifdir 4281
[Stoll] p. 17Theorem 5.1(5)unvdif 4267
[Stoll] p. 19Theorem 5.2(13)undm 4117
[Stoll] p. 19Theorem 5.2(13')indm 4118
[Stoll] p. 20Remarkinvdif 4100
[Stoll] p. 25Definition of ordered tripledf-ot 4408
[Stoll] p. 43Definitionuniiun 4795
[Stoll] p. 44Definitionintiin 4796
[Stoll] p. 45Definitiondf-iin 4745
[Stoll] p. 45Definition indexed uniondf-iun 4744
[Stoll] p. 176Theorem 3.4(27)iman 392
[Stoll] p. 262Example 4.1dfsymdif3 4124
[Strang] p. 242Section 6.3expgrowth 39369
[Suppes] p. 22Theorem 2eq0 4160  eq0f 4157
[Suppes] p. 22Theorem 4eqss 3842  eqssd 3844  eqssi 3843
[Suppes] p. 23Theorem 5ss0 4201  ss0b 4200
[Suppes] p. 23Theorem 6sstr 3835  sstrALT2 39884
[Suppes] p. 23Theorem 7pssirr 3935
[Suppes] p. 23Theorem 8pssn2lp 3936
[Suppes] p. 23Theorem 9psstr 3939
[Suppes] p. 23Theorem 10pssss 3930
[Suppes] p. 25Theorem 12elin 4025  elun 3982
[Suppes] p. 26Theorem 15inidm 4049
[Suppes] p. 26Theorem 16in0 4195
[Suppes] p. 27Theorem 23unidm 3985
[Suppes] p. 27Theorem 24un0 4194
[Suppes] p. 27Theorem 25ssun1 4005
[Suppes] p. 27Theorem 26ssequn1 4012
[Suppes] p. 27Theorem 27unss 4016
[Suppes] p. 27Theorem 28indir 4107
[Suppes] p. 27Theorem 29undir 4108
[Suppes] p. 28Theorem 32difid 4180
[Suppes] p. 29Theorem 33difin 4093
[Suppes] p. 29Theorem 34indif 4101
[Suppes] p. 29Theorem 35undif1 4268
[Suppes] p. 29Theorem 36difun2 4273
[Suppes] p. 29Theorem 37difin0 4266
[Suppes] p. 29Theorem 38disjdif 4265
[Suppes] p. 29Theorem 39difundi 4111
[Suppes] p. 29Theorem 40difindi 4113
[Suppes] p. 30Theorem 41nalset 5022
[Suppes] p. 39Theorem 61uniss 4683
[Suppes] p. 39Theorem 65uniop 5203
[Suppes] p. 41Theorem 70intsn 4735
[Suppes] p. 42Theorem 71intpr 4732  intprg 4733
[Suppes] p. 42Theorem 73op1stb 5162
[Suppes] p. 42Theorem 78intun 4731
[Suppes] p. 44Definition 15(a)dfiun2 4776  dfiun2g 4774
[Suppes] p. 44Definition 15(b)dfiin2 4777
[Suppes] p. 47Theorem 86elpw 4386  elpw2 5052  elpw2g 5051  elpwg 4388  elpwgdedVD 39966
[Suppes] p. 47Theorem 87pwid 4396
[Suppes] p. 47Theorem 89pw0 4563
[Suppes] p. 48Theorem 90pwpw0 4564
[Suppes] p. 52Theorem 101xpss12 5361
[Suppes] p. 52Theorem 102xpindi 5492  xpindir 5493
[Suppes] p. 52Theorem 103xpundi 5408  xpundir 5409
[Suppes] p. 54Theorem 105elirrv 8777
[Suppes] p. 58Theorem 2relss 5445
[Suppes] p. 59Theorem 4eldm 5557  eldm2 5558  eldm2g 5556  eldmg 5555
[Suppes] p. 59Definition 3df-dm 5356
[Suppes] p. 60Theorem 6dmin 5568
[Suppes] p. 60Theorem 8rnun 5786
[Suppes] p. 60Theorem 9rnin 5787
[Suppes] p. 60Definition 4dfrn2 5547
[Suppes] p. 61Theorem 11brcnv 5541  brcnvg 5538
[Suppes] p. 62Equation 5elcnv 5535  elcnv2 5536
[Suppes] p. 62Theorem 12relcnv 5748
[Suppes] p. 62Theorem 15cnvin 5785
[Suppes] p. 62Theorem 16cnvun 5783
[Suppes] p. 63Definitiondftrrels2 34864
[Suppes] p. 63Theorem 20co02 5894
[Suppes] p. 63Theorem 21dmcoss 5622
[Suppes] p. 63Definition 7df-co 5355
[Suppes] p. 64Theorem 26cnvco 5544
[Suppes] p. 64Theorem 27coass 5899
[Suppes] p. 65Theorem 31resundi 5651
[Suppes] p. 65Theorem 34elima 5716  elima2 5717  elima3 5718  elimag 5715
[Suppes] p. 65Theorem 35imaundi 5790
[Suppes] p. 66Theorem 40dminss 5792
[Suppes] p. 66Theorem 41imainss 5793
[Suppes] p. 67Exercise 11cnvxp 5796
[Suppes] p. 81Definition 34dfec2 8017
[Suppes] p. 82Theorem 72elec 8056  elecALTV 34579  elecg 8055
[Suppes] p. 82Theorem 73eqvrelth 34896  erth 8061  erth2 8062
[Suppes] p. 83Theorem 74eqvreldisj 34899  erdisj 8064
[Suppes] p. 89Theorem 96map0b 8168
[Suppes] p. 89Theorem 97map0 8171  map0g 8169
[Suppes] p. 89Theorem 98mapsn 8172  mapsnd 8170
[Suppes] p. 89Theorem 99mapss 8173
[Suppes] p. 91Definition 12(ii)alephsuc 9211
[Suppes] p. 91Definition 12(iii)alephlim 9210
[Suppes] p. 92Theorem 1enref 8261  enrefg 8260
[Suppes] p. 92Theorem 2ensym 8277  ensymb 8276  ensymi 8278
[Suppes] p. 92Theorem 3entr 8280
[Suppes] p. 92Theorem 4unen 8315
[Suppes] p. 94Theorem 15endom 8255
[Suppes] p. 94Theorem 16ssdomg 8274
[Suppes] p. 94Theorem 17domtr 8281
[Suppes] p. 95Theorem 18sbth 8355
[Suppes] p. 97Theorem 23canth2 8388  canth2g 8389
[Suppes] p. 97Definition 3brsdom2 8359  df-sdom 8231  dfsdom2 8358
[Suppes] p. 97Theorem 21(i)sdomirr 8372
[Suppes] p. 97Theorem 22(i)domnsym 8361
[Suppes] p. 97Theorem 21(ii)sdomnsym 8360
[Suppes] p. 97Theorem 22(ii)domsdomtr 8370
[Suppes] p. 97Theorem 22(iv)brdom2 8258
[Suppes] p. 97Theorem 21(iii)sdomtr 8373
[Suppes] p. 97Theorem 22(iii)sdomdomtr 8368
[Suppes] p. 98Exercise 4fundmen 8302  fundmeng 8303
[Suppes] p. 98Exercise 6xpdom3 8333
[Suppes] p. 98Exercise 11sdomentr 8369
[Suppes] p. 104Theorem 37fofi 8527
[Suppes] p. 104Theorem 38pwfi 8536
[Suppes] p. 105Theorem 40pwfi 8536
[Suppes] p. 111Axiom for cardinal numberscarden 9695
[Suppes] p. 130Definition 3df-tr 4978
[Suppes] p. 132Theorem 9ssonuni 7252
[Suppes] p. 134Definition 6df-suc 5973
[Suppes] p. 136Theorem Schema 22findes 7362  finds 7358  finds1 7361  finds2 7360
[Suppes] p. 151Theorem 42isfinite 8833  isfinite2 8493  isfiniteg 8495  unbnn 8491
[Suppes] p. 162Definition 5df-ltnq 10062  df-ltpq 10054
[Suppes] p. 197Theorem Schema 4tfindes 7328  tfinds 7325  tfinds2 7329
[Suppes] p. 209Theorem 18oaord1 7903
[Suppes] p. 209Theorem 21oaword2 7905
[Suppes] p. 211Theorem 25oaass 7913
[Suppes] p. 225Definition 8iscard2 9122
[Suppes] p. 227Theorem 56ondomon 9707
[Suppes] p. 228Theorem 59harcard 9124
[Suppes] p. 228Definition 12(i)aleph0 9209
[Suppes] p. 228Theorem Schema 61onintss 6017
[Suppes] p. 228Theorem Schema 62onminesb 7264  onminsb 7265
[Suppes] p. 229Theorem 64alephval2 9716
[Suppes] p. 229Theorem 65alephcard 9213
[Suppes] p. 229Theorem 66alephord2i 9220
[Suppes] p. 229Theorem 67alephnbtwn 9214
[Suppes] p. 229Definition 12df-aleph 9086
[Suppes] p. 242Theorem 6weth 9639
[Suppes] p. 242Theorem 8entric 9701
[Suppes] p. 242Theorem 9carden 9695
[TakeutiZaring] p. 8Axiom 1ax-ext 2803
[TakeutiZaring] p. 13Definition 4.5df-cleq 2818
[TakeutiZaring] p. 13Proposition 4.6df-clel 2821
[TakeutiZaring] p. 13Proposition 4.9cvjust 2820
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2846
[TakeutiZaring] p. 14Definition 4.16df-oprab 6914
[TakeutiZaring] p. 14Proposition 4.14ru 3661
[TakeutiZaring] p. 15Axiom 2zfpair 5127
[TakeutiZaring] p. 15Exercise 1elpr 4422  elpr2 4423  elprg 4420
[TakeutiZaring] p. 15Exercise 2elsn 4414  elsn2 4434  elsn2g 4433  elsng 4413  velsn 4415
[TakeutiZaring] p. 15Exercise 3elop 5158
[TakeutiZaring] p. 15Exercise 4sneq 4409  sneqr 4589
[TakeutiZaring] p. 15Definition 5.1dfpr2 4418  dfsn2 4412  dfsn2ALT 4419
[TakeutiZaring] p. 16Axiom 3uniex 7218
[TakeutiZaring] p. 16Exercise 6opth 5167
[TakeutiZaring] p. 16Exercise 7opex 5155
[TakeutiZaring] p. 16Exercise 8rext 5139
[TakeutiZaring] p. 16Corollary 5.8unex 7221  unexg 7224
[TakeutiZaring] p. 16Definition 5.3dftp2 4452
[TakeutiZaring] p. 16Definition 5.5df-uni 4661
[TakeutiZaring] p. 16Definition 5.6df-in 3805  df-un 3803
[TakeutiZaring] p. 16Proposition 5.7unipr 4673  uniprg 4674
[TakeutiZaring] p. 17Axiom 4vpwex 5079
[TakeutiZaring] p. 17Exercise 1eltp 4451
[TakeutiZaring] p. 17Exercise 5elsuc 6036  elsucg 6034  sstr2 3834
[TakeutiZaring] p. 17Exercise 6uncom 3986
[TakeutiZaring] p. 17Exercise 7incom 4034
[TakeutiZaring] p. 17Exercise 8unass 3999
[TakeutiZaring] p. 17Exercise 9inass 4050
[TakeutiZaring] p. 17Exercise 10indi 4105
[TakeutiZaring] p. 17Exercise 11undi 4106
[TakeutiZaring] p. 17Definition 5.9df-pss 3814  dfss2 3815
[TakeutiZaring] p. 17Definition 5.10df-pw 4382
[TakeutiZaring] p. 18Exercise 7unss2 4013
[TakeutiZaring] p. 18Exercise 9df-ss 3812  sseqin2 4046
[TakeutiZaring] p. 18Exercise 10ssid 3848
[TakeutiZaring] p. 18Exercise 12inss1 4059  inss2 4060
[TakeutiZaring] p. 18Exercise 13nss 3888
[TakeutiZaring] p. 18Exercise 15unieq 4668
[TakeutiZaring] p. 18Exercise 18sspwb 5140  sspwimp 39967  sspwimpALT 39974  sspwimpALT2 39977  sspwimpcf 39969
[TakeutiZaring] p. 18Exercise 19pweqb 5148
[TakeutiZaring] p. 19Axiom 5ax-rep 4996
[TakeutiZaring] p. 20Definitiondf-rab 3126
[TakeutiZaring] p. 20Corollary 5.160ex 5016
[TakeutiZaring] p. 20Definition 5.12df-dif 3801
[TakeutiZaring] p. 20Definition 5.14dfnul2 4148
[TakeutiZaring] p. 20Proposition 5.15difid 4180
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4162  n0f 4159  neq0 4161  neq0f 4158
[TakeutiZaring] p. 21Axiom 6zfreg 8776
[TakeutiZaring] p. 21Axiom 6'zfregs 8892
[TakeutiZaring] p. 21Theorem 5.22setind 8894
[TakeutiZaring] p. 21Definition 5.20df-v 3416
[TakeutiZaring] p. 21Proposition 5.21vprc 5024
[TakeutiZaring] p. 22Exercise 10ss 4199
[TakeutiZaring] p. 22Exercise 3ssex 5029  ssexg 5031
[TakeutiZaring] p. 22Exercise 4inex1 5026
[TakeutiZaring] p. 22Exercise 5ruv 8783
[TakeutiZaring] p. 22Exercise 6elirr 8778
[TakeutiZaring] p. 22Exercise 7ssdif0 4173
[TakeutiZaring] p. 22Exercise 11difdif 3965
[TakeutiZaring] p. 22Exercise 13undif3 4120  undif3VD 39931
[TakeutiZaring] p. 22Exercise 14difss 3966
[TakeutiZaring] p. 22Exercise 15sscon 3973
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3122
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3123
[TakeutiZaring] p. 23Proposition 6.2xpex 7228  xpexg 7225
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5353
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6197
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6351  fun11 6200
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6139  svrelfun 6198
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5546
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5548
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5358
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5359
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5355
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5833  dfrel2 5828
[TakeutiZaring] p. 25Exercise 3xpss 5362
[TakeutiZaring] p. 25Exercise 5relun 5473
[TakeutiZaring] p. 25Exercise 6reluni 5480
[TakeutiZaring] p. 25Exercise 9inxp 5491
[TakeutiZaring] p. 25Exercise 12relres 5666
[TakeutiZaring] p. 25Exercise 13opelres 5639  opelresi 5641
[TakeutiZaring] p. 25Exercise 14dmres 5659
[TakeutiZaring] p. 25Exercise 15resss 5662
[TakeutiZaring] p. 25Exercise 17resabs1 5667
[TakeutiZaring] p. 25Exercise 18funres 6169
[TakeutiZaring] p. 25Exercise 24relco 5878
[TakeutiZaring] p. 25Exercise 29funco 6167
[TakeutiZaring] p. 25Exercise 30f1co 6352
[TakeutiZaring] p. 26Definition 6.10eu2 2694
[TakeutiZaring] p. 26Definition 6.11conventions 27811  df-fv 6135  fv3 6455
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7380  cnvexg 7379
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7366  dmexg 7363
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7367  rnexg 7364
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 39491
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7375
[TakeutiZaring] p. 27Corollary 6.13fvex 6450
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 42070  tz6.12-1-afv2 42137  tz6.12-1 6459  tz6.12-afv 42069  tz6.12-afv2 42136  tz6.12 6460  tz6.12c-afv2 42138  tz6.12c 6462
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 42133  tz6.12-2 6427  tz6.12i-afv2 42139  tz6.12i 6463
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6130
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6131
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6133  wfo 6125
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6132  wf1 6124
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6134  wf1o 6126
[TakeutiZaring] p. 28Exercise 4eqfnfv 6565  eqfnfv2 6566  eqfnfv2f 6569
[TakeutiZaring] p. 28Exercise 5fvco 6525
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 6742
[TakeutiZaring] p. 28Proposition 6.17resfunexg 6740
[TakeutiZaring] p. 29Exercise 9funimaex 6213  funimaexg 6212
[TakeutiZaring] p. 29Definition 6.18df-br 4876
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5266
[TakeutiZaring] p. 30Definition 6.21dffr2 5311  dffr3 5743  eliniseg 5739  iniseg 5741
[TakeutiZaring] p. 30Definition 6.22df-eprel 5257
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5324  fr3nr 7245  frirr 5323
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5305
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7247
[TakeutiZaring] p. 31Exercise 1frss 5313
[TakeutiZaring] p. 31Exercise 4wess 5333
[TakeutiZaring] p. 31Proposition 6.26tz6.26 5955  tz6.26i 5956  wefrc 5340  wereu2 5343
[TakeutiZaring] p. 32Theorem 6.27wfi 5957  wfii 5958
[TakeutiZaring] p. 32Definition 6.28df-isom 6136
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6839
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6840
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6846
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6847
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6848
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6852
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6859
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6861
[TakeutiZaring] p. 35Notationwtr 4977
[TakeutiZaring] p. 35Theorem 7.2trelpss 39492  tz7.2 5330
[TakeutiZaring] p. 35Definition 7.1dftr3 4981
[TakeutiZaring] p. 36Proposition 7.4ordwe 5980
[TakeutiZaring] p. 36Proposition 7.5tz7.5 5988
[TakeutiZaring] p. 36Proposition 7.6ordelord 5989  ordelordALT 39576  ordelordALTVD 39916
[TakeutiZaring] p. 37Corollary 7.8ordelpss 5995  ordelssne 5994
[TakeutiZaring] p. 37Proposition 7.7tz7.7 5993
[TakeutiZaring] p. 37Proposition 7.9ordin 5997
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7254
[TakeutiZaring] p. 38Corollary 7.15ordsson 7255
[TakeutiZaring] p. 38Definition 7.11df-on 5971
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 5999
[TakeutiZaring] p. 38Proposition 7.12onfrALT 39588  ordon 7249
[TakeutiZaring] p. 38Proposition 7.13onprc 7250
[TakeutiZaring] p. 39Theorem 7.17tfi 7319
[TakeutiZaring] p. 40Exercise 3ontr2 6014
[TakeutiZaring] p. 40Exercise 7dftr2 4979
[TakeutiZaring] p. 40Exercise 9onssmin 7263
[TakeutiZaring] p. 40Exercise 11unon 7297
[TakeutiZaring] p. 40Exercise 12ordun 6068
[TakeutiZaring] p. 40Exercise 14ordequn 6067
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7251
[TakeutiZaring] p. 40Proposition 7.20elssuni 4691
[TakeutiZaring] p. 41Definition 7.22df-suc 5973
[TakeutiZaring] p. 41Proposition 7.23sssucid 6044  sucidg 6045
[TakeutiZaring] p. 41Proposition 7.24suceloni 7279
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6058  ordnbtwn 6057
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7294
[TakeutiZaring] p. 42Exercise 1df-lim 5972
[TakeutiZaring] p. 42Exercise 4omssnlim 7345
[TakeutiZaring] p. 42Exercise 7ssnlim 7349
[TakeutiZaring] p. 42Exercise 8onsucssi 7307  ordelsuc 7286
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7288
[TakeutiZaring] p. 42Definition 7.27nlimon 7317
[TakeutiZaring] p. 42Definition 7.28dfom2 7333
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7351
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7352
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7353
[TakeutiZaring] p. 43Remarkomon 7342
[TakeutiZaring] p. 43Axiom 7inf3 8816  omex 8824
[TakeutiZaring] p. 43Theorem 7.32ordom 7340
[TakeutiZaring] p. 43Corollary 7.31find 7357
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7354
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7355
[TakeutiZaring] p. 44Exercise 1limomss 7336
[TakeutiZaring] p. 44Exercise 2int0 4713
[TakeutiZaring] p. 44Exercise 3trintss 4995
[TakeutiZaring] p. 44Exercise 4intss1 4714
[TakeutiZaring] p. 44Exercise 5intex 5044
[TakeutiZaring] p. 44Exercise 6oninton 7266
[TakeutiZaring] p. 44Exercise 11ordintdif 6016
[TakeutiZaring] p. 44Definition 7.35df-int 4700
[TakeutiZaring] p. 44Proposition 7.34noinfep 8841
[TakeutiZaring] p. 45Exercise 4onint 7261
[TakeutiZaring] p. 47Lemma 1tfrlem1 7743
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 7764
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 7765
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 7766
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 7773  tz7.44-2 7774  tz7.44-3 7775
[TakeutiZaring] p. 50Exercise 1smogt 7735
[TakeutiZaring] p. 50Exercise 3smoiso 7730
[TakeutiZaring] p. 50Definition 7.46df-smo 7714
[TakeutiZaring] p. 51Proposition 7.49tz7.49 7811  tz7.49c 7812
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 7809
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 7808
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 7810
[TakeutiZaring] p. 53Proposition 7.532eu5 2737
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9154
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9155
[TakeutiZaring] p. 56Definition 8.1oalim 7884  oasuc 7876
[TakeutiZaring] p. 57Remarktfindsg 7326
[TakeutiZaring] p. 57Proposition 8.2oacl 7887
[TakeutiZaring] p. 57Proposition 8.3oa0 7868  oa0r 7890
[TakeutiZaring] p. 57Proposition 8.16omcl 7888
[TakeutiZaring] p. 58Corollary 8.5oacan 7900
[TakeutiZaring] p. 58Proposition 8.4nnaord 7971  nnaordi 7970  oaord 7899  oaordi 7898
[TakeutiZaring] p. 59Proposition 8.6iunss2 4787  uniss2 4694
[TakeutiZaring] p. 59Proposition 8.7oawordri 7902
[TakeutiZaring] p. 59Proposition 8.8oawordeu 7907  oawordex 7909
[TakeutiZaring] p. 59Proposition 8.9nnacl 7963
[TakeutiZaring] p. 59Proposition 8.10oaabs 7996
[TakeutiZaring] p. 60Remarkoancom 8832
[TakeutiZaring] p. 60Proposition 8.11oalimcl 7912
[TakeutiZaring] p. 62Exercise 1nnarcl 7968
[TakeutiZaring] p. 62Exercise 5oaword1 7904
[TakeutiZaring] p. 62Definition 8.15om0x 7871  omlim 7885  omsuc 7878
[TakeutiZaring] p. 62Definition 8.15(a)om0 7869
[TakeutiZaring] p. 63Proposition 8.17nnecl 7965  nnmcl 7964
[TakeutiZaring] p. 63Proposition 8.19nnmord 7984  nnmordi 7983  omord 7920  omordi 7918
[TakeutiZaring] p. 63Proposition 8.20omcan 7921
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 7988  omwordri 7924
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 7891
[TakeutiZaring] p. 63Proposition 8.18(2)om1 7894  om1r 7895
[TakeutiZaring] p. 64Proposition 8.22om00 7927
[TakeutiZaring] p. 64Proposition 8.23omordlim 7929
[TakeutiZaring] p. 64Proposition 8.24omlimcl 7930
[TakeutiZaring] p. 64Proposition 8.25odi 7931
[TakeutiZaring] p. 65Theorem 8.26omass 7932
[TakeutiZaring] p. 67Definition 8.30nnesuc 7960  oe0 7874  oelim 7886  oesuc 7879  onesuc 7882
[TakeutiZaring] p. 67Proposition 8.31oe0m0 7872
[TakeutiZaring] p. 67Proposition 8.32oen0 7938
[TakeutiZaring] p. 67Proposition 8.33oeordi 7939
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 7873
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 7897
[TakeutiZaring] p. 68Corollary 8.34oeord 7940
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 7946
[TakeutiZaring] p. 68Proposition 8.35oewordri 7944
[TakeutiZaring] p. 68Proposition 8.37oeworde 7945
[TakeutiZaring] p. 69Proposition 8.41oeoa 7949
[TakeutiZaring] p. 70Proposition 8.42oeoe 7951
[TakeutiZaring] p. 73Theorem 9.1trcl 8888  tz9.1 8889
[TakeutiZaring] p. 76Definition 9.9df-r1 8911  r10 8915  r1lim 8919  r1limg 8918  r1suc 8917  r1sucg 8916
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 8927  r1ord2 8928  r1ordg 8925
[TakeutiZaring] p. 78Proposition 9.12tz9.12 8937
[TakeutiZaring] p. 78Proposition 9.13rankwflem 8962  tz9.13 8938  tz9.13g 8939
[TakeutiZaring] p. 79Definition 9.14df-rank 8912  rankval 8963  rankvalb 8944  rankvalg 8964
[TakeutiZaring] p. 79Proposition 9.16rankel 8986  rankelb 8971
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9000  rankval3 8987  rankval3b 8973
[TakeutiZaring] p. 79Proposition 9.18rankonid 8976
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 8942
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 8981  rankr1c 8968  rankr1g 8979
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 8982
[TakeutiZaring] p. 80Exercise 1rankss 8996  rankssb 8995
[TakeutiZaring] p. 80Exercise 2unbndrank 8989
[TakeutiZaring] p. 80Proposition 9.19bndrank 8988
[TakeutiZaring] p. 83Axiom of Choiceac4 9619  dfac3 9264
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9173  numth 9616  numth2 9615
[TakeutiZaring] p. 85Definition 10.4cardval 9690
[TakeutiZaring] p. 85Proposition 10.5cardid 9691  cardid2 9099
[TakeutiZaring] p. 85Proposition 10.9oncard 9106
[TakeutiZaring] p. 85Proposition 10.10carden 9695
[TakeutiZaring] p. 85Proposition 10.11cardidm 9105
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9090
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9111
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9103
[TakeutiZaring] p. 87Proposition 10.15pwen 8408
[TakeutiZaring] p. 88Exercise 1en0 8291
[TakeutiZaring] p. 88Exercise 7infensuc 8413
[TakeutiZaring] p. 89Exercise 10omxpen 8337
[TakeutiZaring] p. 90Corollary 10.23cardnn 9109
[TakeutiZaring] p. 90Definition 10.27alephiso 9241
[TakeutiZaring] p. 90Proposition 10.20nneneq 8418
[TakeutiZaring] p. 90Proposition 10.22onomeneq 8425
[TakeutiZaring] p. 90Proposition 10.26alephprc 9242
[TakeutiZaring] p. 90Corollary 10.21(1)php5 8423
[TakeutiZaring] p. 91Exercise 2alephle 9231
[TakeutiZaring] p. 91Exercise 3aleph0 9209
[TakeutiZaring] p. 91Exercise 4cardlim 9118
[TakeutiZaring] p. 91Exercise 7infpss 9361
[TakeutiZaring] p. 91Exercise 8infcntss 8509
[TakeutiZaring] p. 91Definition 10.29df-fin 8232  isfi 8252
[TakeutiZaring] p. 92Proposition 10.32onfin 8426
[TakeutiZaring] p. 92Proposition 10.34imadomg 9678
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8330
[TakeutiZaring] p. 93Proposition 10.35fodomb 9670
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 9333  unxpdom 8442
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9120  cardsdomelir 9119
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 8444
[TakeutiZaring] p. 94Proposition 10.39infxpen 9157
[TakeutiZaring] p. 95Definition 10.42df-map 8129
[TakeutiZaring] p. 95Proposition 10.40infxpidm 9706  infxpidm2 9160
[TakeutiZaring] p. 95Proposition 10.41infcda 9352  infxp 9359
[TakeutiZaring] p. 96Proposition 10.44pw2en 8342  pw2f1o 8340
[TakeutiZaring] p. 96Proposition 10.45mapxpen 8401
[TakeutiZaring] p. 97Theorem 10.46ac6s3 9631
[TakeutiZaring] p. 98Theorem 10.46ac6c5 9626  ac6s5 9635
[TakeutiZaring] p. 98Theorem 10.47unidom 9687
[TakeutiZaring] p. 99Theorem 10.48uniimadom 9688  uniimadomf 9689
[TakeutiZaring] p. 100Definition 11.1cfcof 9418
[TakeutiZaring] p. 101Proposition 11.7cofsmo 9413
[TakeutiZaring] p. 102Exercise 1cfle 9398
[TakeutiZaring] p. 102Exercise 2cf0 9395
[TakeutiZaring] p. 102Exercise 3cfsuc 9401
[TakeutiZaring] p. 102Exercise 4cfom 9408
[TakeutiZaring] p. 102Proposition 11.9coftr 9417
[TakeutiZaring] p. 103Theorem 11.15alephreg 9726
[TakeutiZaring] p. 103Proposition 11.11cardcf 9396
[TakeutiZaring] p. 103Proposition 11.13alephsing 9420
[TakeutiZaring] p. 104Corollary 11.17cardinfima 9240
[TakeutiZaring] p. 104Proposition 11.16carduniima 9239
[TakeutiZaring] p. 104Proposition 11.18alephfp 9251  alephfp2 9252
[TakeutiZaring] p. 106Theorem 11.20gchina 9843
[TakeutiZaring] p. 106Theorem 11.21mappwen 9255
[TakeutiZaring] p. 107Theorem 11.26konigth 9713
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 9727
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 9728
[Tarski] p. 67Axiom B5ax-c5 34953
[Tarski] p. 67Scheme B5sp 2224
[Tarski] p. 68Lemma 6avril1 27873  equid 2116
[Tarski] p. 69Lemma 7equcomi 2121
[Tarski] p. 70Lemma 14spim 2407  spime 2409  spimeh 2101
[Tarski] p. 70Lemma 16ax-12 2220  ax-c15 34959  ax12i 2066
[Tarski] p. 70Lemmas 16 and 17sb6 2307
[Tarski] p. 75Axiom B7ax6v 2076
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 2009  ax5ALT 34977
[Tarski], p. 75Scheme B8 of system S2ax-7 2112  ax-8 2166  ax-9 2173
[Tarski1999] p. 178Axiom 4axtgsegcon 25783
[Tarski1999] p. 178Axiom 5axtg5seg 25784
[Tarski1999] p. 179Axiom 7axtgpasch 25786
[Tarski1999] p. 180Axiom 7.1axtgpasch 25786
[Tarski1999] p. 185Axiom 11axtgcont1 25787
[Truss] p. 114Theorem 5.18ruc 15353
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 33987
[Viaclovsky8] p. 3Proposition 7ismblfin 33989
[Weierstrass] p. 272Definitiondf-mdet 20766  mdetuni 20803
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 932
[WhiteheadRussell] p. 96Axiom *1.3olc 899
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 900
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 948
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 995
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 181
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 133
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 33809
[WhiteheadRussell] p. 100Theorem *2.05frege5 38929  imim2 58  wl-luk-imim2 33804
[WhiteheadRussell] p. 100Theorem *2.06imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 925
[WhiteheadRussell] p. 101Theorem *2.06barbara 2746  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 931
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 33807
[WhiteheadRussell] p. 101Theorem *2.11exmid 923
[WhiteheadRussell] p. 101Theorem *2.12notnot 139
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 926
[WhiteheadRussell] p. 102Theorem *2.14notnotr 128  notnotrALT2 39976  wl-luk-notnotr 33808
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 38959  axfrege28 38958  con3 151
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 125
[WhiteheadRussell] p. 104Theorem *2.2orc 898
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 953
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 121  wl-luk-pm2.21 33801
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 122
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 918
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 968
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 27812  pm2.27 42  wl-luk-pm2.27 33799
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 951
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 952
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 997
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 998
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 996
[WhiteheadRussell] p. 105Definition *2.33df-3or 1112
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 935
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 936
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 971
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 910
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 911
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 166
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 183
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 912
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 913
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 914
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 167
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 169
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 882
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 883
[WhiteheadRussell] p. 107Theorem *2.55orel1 917
[WhiteheadRussell] p. 107Theorem *2.56orel2 919
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 184
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 928
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 969
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 970
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 185
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 920  pm2.67 921
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 168
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 927
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 1000
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 929
[WhiteheadRussell] p. 108Theorem *2.69looinv 195
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 1001
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 1002
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 962
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 960
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 999
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 1003
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 961
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1019
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 463  pm3.2im 159
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1020
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1021
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1022
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1023
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 465
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 453
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 393
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 837
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 441
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 442
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 476  simplim 165
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 479  simprim 164
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 781
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 782
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 842
[WhiteheadRussell] p. 113Fact)pm3.45 615
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 844
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 488
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 489
[WhiteheadRussell] p. 113Theorem *3.44jao 988  pm3.44 987
[WhiteheadRussell] p. 113Theorem *3.47prth 843
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 467
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 991
[WhiteheadRussell] p. 116Theorem *4.1con34b 308
[WhiteheadRussell] p. 117Theorem *4.2biid 253
[WhiteheadRussell] p. 117Theorem *4.11notbi 311
[WhiteheadRussell] p. 117Theorem *4.12con2bi 345
[WhiteheadRussell] p. 117Theorem *4.13notnotb 307
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 841
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 866
[WhiteheadRussell] p. 117Theorem *4.21bicom 214
[WhiteheadRussell] p. 117Theorem *4.22biantr 840  bitr 839
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 559
[WhiteheadRussell] p. 117Theorem *4.25oridm 933  pm4.25 934
[WhiteheadRussell] p. 118Theorem *4.3ancom 454
[WhiteheadRussell] p. 118Theorem *4.4andi 1035
[WhiteheadRussell] p. 118Theorem *4.31orcom 901
[WhiteheadRussell] p. 118Theorem *4.32anass 462
[WhiteheadRussell] p. 118Theorem *4.33orass 950
[WhiteheadRussell] p. 118Theorem *4.36anbi1 625
[WhiteheadRussell] p. 118Theorem *4.37orbi1 946
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 628
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 1004
[WhiteheadRussell] p. 118Definition *4.34df-3an 1113
[WhiteheadRussell] p. 119Theorem *4.41ordi 1033
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1080
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1051
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1024
[WhiteheadRussell] p. 119Theorem *4.45orabs 1026  pm4.45 1025  pm4.45im 863
[WhiteheadRussell] p. 120Theorem *4.5anor 1010
[WhiteheadRussell] p. 120Theorem *4.6imor 884
[WhiteheadRussell] p. 120Theorem *4.7anclb 541
[WhiteheadRussell] p. 120Theorem *4.51ianor 1009
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 1012
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 1013
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 1014
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 1015
[WhiteheadRussell] p. 120Theorem *4.56ioran 1011  pm4.56 1016
[WhiteheadRussell] p. 120Theorem *4.57oran 1017  pm4.57 1018
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 395
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 887
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 388
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 880
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 396
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 881
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 389
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 553  pm4.71d 557  pm4.71i 555  pm4.71r 554  pm4.71rd 558  pm4.71ri 556
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 977
[WhiteheadRussell] p. 121Theorem *4.73iba 523
[WhiteheadRussell] p. 121Theorem *4.74biorf 965
[WhiteheadRussell] p. 121Theorem *4.76jcab 513  pm4.76 514
[WhiteheadRussell] p. 121Theorem *4.77jaob 989  pm4.77 990
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 963
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1031
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 383
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 384
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1052
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1053
[WhiteheadRussell] p. 122Theorem *4.84imbi1 339
[WhiteheadRussell] p. 122Theorem *4.85imbi2 340
[WhiteheadRussell] p. 122Theorem *4.86bibi1 343
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 379  impexp 443  pm4.87 874
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 859
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 972
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 973
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 975
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 974
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1041
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1042
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1040
[WhiteheadRussell] p. 124Theorem *5.18nbbn 375  pm5.18 373
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 378
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 860
[WhiteheadRussell] p. 124Theorem *5.22xor 1043
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1076
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1077
[WhiteheadRussell] p. 124Theorem *5.25dfor2 930
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 568
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 380
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 353
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1029
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 981
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 865
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 569
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 869
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 861
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 867
[WhiteheadRussell] p. 125Theorem *5.41imdi 381  pm5.41 382
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 539
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 538
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1032
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1046
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 976
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1028
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1047
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1048
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1056
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 358
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 262
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1057
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 39392
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 39393
[WhiteheadRussell] p. 147Theorem *10.2219.26 1972
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 39394
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 39395
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 39396
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1995
[WhiteheadRussell] p. 151Theorem *10.301albitr 39397
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 39398
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 39399
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 39400
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 39401
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 39403
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 39404
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 39405
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 39402
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2581
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 39408
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 39409
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2484
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2210
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1927
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1928
[WhiteheadRussell] p. 161Theorem *11.319.21vv 39410
[WhiteheadRussell] p. 162Theorem *11.322alim 39411
[WhiteheadRussell] p. 162Theorem *11.332albi 39412
[WhiteheadRussell] p. 162Theorem *11.342exim 39413
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 39415
[WhiteheadRussell] p. 162Theorem *11.3412exbi 39414
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1989
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 39417
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 39418
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 39416
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1926
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 39419
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 39420
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1945
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 39421
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2370
[WhiteheadRussell] p. 164Theorem *11.5212exanali 39422
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 39427
[WhiteheadRussell] p. 165Theorem *11.56aaanv 39423
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 39424
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 39425
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 39426
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 39431
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 39428
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 39429
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 39430
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 39432
[WhiteheadRussell] p. 175Definition *14.02df-eu 2640
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 39442  pm13.13b 39443
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 39444
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3080
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3081
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3563
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 39450
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 39451
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 39445
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 39591  pm13.193 39446
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 39447
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 39448
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 39449
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 39456
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 39455
[WhiteheadRussell] p. 184Definition *14.01iotasbc 39454
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3715
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 39457  pm14.122b 39458  pm14.122c 39459
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 39460  pm14.123b 39461  pm14.123c 39462
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 39464
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 39463
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 39465
[WhiteheadRussell] p. 190Theorem *14.22iota4 6108
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 39466
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6109
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 39467
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 39469
[WhiteheadRussell] p. 192Theorem *14.26eupick 2716  eupickbi 2719  sbaniota 39470
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 39468
[WhiteheadRussell] p. 192Theorem *14.271eubi 2657
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 39472
[WhiteheadRussell] p. 235Definition *30.01conventions 27811  df-fv 6135
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9146  pm54.43lem 9145
[Young] p. 141Definition of operator orderingleop2 29534
[Young] p. 142Example 12.2(i)0leop 29540  idleop 29541
[vandenDries] p. 42Lemma 61irrapx1 38231
[vandenDries] p. 43Theorem 62pellex 38238  pellexlem1 38232

This page was last updated on 1-Apr-2023.
Copyright terms: Public domain