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 17635
[Adamek] p. 21Condition 3.1(b)df-cat 17635
[Adamek] p. 22Example 3.3(1)df-setc 18044
[Adamek] p. 24Example 3.3(4.c)0cat 17656  0funcg 49002  df-termc 49351
[Adamek] p. 24Example 3.3(4.d)df-prstc 49428  prsthinc 49342
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49456  df-mndtc 49456
[Adamek] p. 24Example 3.3(4)(c)discsnterm 49452
[Adamek] p. 25Definition 3.5df-oppc 17679
[Adamek] p. 25Example 3.6(1)oduoppcciso 49444
[Adamek] p. 25Example 3.6(2)oppgoppcco 49469  oppgoppchom 49468  oppgoppcid 49470
[Adamek] p. 28Remark 3.9oppciso 17749
[Adamek] p. 28Remark 3.12invf1o 17737  invisoinvl 17758
[Adamek] p. 28Example 3.13idinv 17757  idiso 17756
[Adamek] p. 28Corollary 3.11inveq 17742
[Adamek] p. 28Definition 3.8df-inv 17716  df-iso 17717  dfiso2 17740
[Adamek] p. 28Proposition 3.10sectcan 17723
[Adamek] p. 29Remark 3.16cicer 17774  cicerALT 48963
[Adamek] p. 29Definition 3.15cic 17767  df-cic 17764
[Adamek] p. 29Definition 3.17df-func 17826
[Adamek] p. 29Proposition 3.14(1)invinv 17738
[Adamek] p. 29Proposition 3.14(2)invco 17739  isoco 17745
[Adamek] p. 30Remark 3.19df-func 17826
[Adamek] p. 30Example 3.20(1)idfucl 17849
[Adamek] p. 30Example 3.20(2)diag1 49199
[Adamek] p. 32Proposition 3.21funciso 17842
[Adamek] p. 33Example 3.26(1)discsnterm 49452  discthing 49339
[Adamek] p. 33Example 3.26(2)df-thinc 49296  prsthinc 49342  thincciso 49331  thincciso2 49333  thincciso3 49334  thinccisod 49332
[Adamek] p. 33Example 3.26(3)df-mndtc 49456
[Adamek] p. 33Proposition 3.23cofucl 17856  cofucla 49013
[Adamek] p. 34Remark 3.28(1)cofidfth 49073
[Adamek] p. 34Remark 3.28(2)catciso 18079  catcisoi 49292
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18134
[Adamek] p. 34Definition 3.27(2)df-fth 17875
[Adamek] p. 34Definition 3.27(3)df-full 17874
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18134
[Adamek] p. 35Corollary 3.32ffthiso 17899
[Adamek] p. 35Proposition 3.30(c)cofth 17905
[Adamek] p. 35Proposition 3.30(d)cofull 17904
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18119
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18119
[Adamek] p. 39Definition 3.41df-oppf 49040  funcoppc 17843
[Adamek] p. 39Definition 3.44.df-catc 18067  elcatchom 49289
[Adamek] p. 39Proposition 3.43(c)fthoppc 17893
[Adamek] p. 39Proposition 3.43(d)fulloppc 17892
[Adamek] p. 40Remark 3.48catccat 18076
[Adamek] p. 40Definition 3.470funcg 49002  df-catc 18067
[Adamek] p. 45Exercise 3Gincat 49479
[Adamek] p. 48Remark 4.2(2)cnelsubc 49482  nelsubc3 48988
[Adamek] p. 48Remark 4.2(3)imasubc 49062  imasubc2 49063  imasubc3 49067
[Adamek] p. 48Example 4.3(1.a)0subcat 17806
[Adamek] p. 48Example 4.3(1.b)catsubcat 17807
[Adamek] p. 48Definition 4.1(1)nelsubc3 48988
[Adamek] p. 48Definition 4.1(2)fullsubc 17818
[Adamek] p. 48Definition 4.1(a)df-subc 17780
[Adamek] p. 49Remark 4.4idsubc 49071
[Adamek] p. 49Remark 4.4(1)idemb 49070
[Adamek] p. 49Remark 4.4(2)idfullsubc 49072  ressffth 17908
[Adamek] p. 58Exercise 4Asetc1onsubc 49480
[Adamek] p. 83Definition 6.1df-nat 17914
[Adamek] p. 87Remark 6.14(a)fuccocl 17935
[Adamek] p. 87Remark 6.14(b)fucass 17939
[Adamek] p. 87Definition 6.15df-fuc 17915
[Adamek] p. 88Remark 6.16fuccat 17941
[Adamek] p. 101Definition 7.10funcg 49002  df-inito 17952
[Adamek] p. 101Example 7.2(3)0funcg 49002  df-termc 49351  initc 49008
[Adamek] p. 101Example 7.2 (6)irinitoringc 21395
[Adamek] p. 102Definition 7.4df-termo 17953  oppctermo 49137
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17980
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17984
[Adamek] p. 103Remark 7.8oppczeroo 49138
[Adamek] p. 103Definition 7.7df-zeroo 17954
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21396
[Adamek] p. 103Proposition 7.6termoeu1w 17987
[Adamek] p. 106Definition 7.19df-sect 17715
[Adamek] p. 185Section 10.67updjud 9905
[Adamek] p. 193Definition 11.1(1)df-lmd 49520
[Adamek] p. 193Definition 11.3(1)df-lmd 49520
[Adamek] p. 194Definition 11.3(2)df-lmd 49520
[Adamek] p. 202Definition 11.27(1)df-cmd 49521
[Adamek] p. 202Definition 11.27(2)df-cmd 49521
[Adamek] p. 478Item Rngdf-ringc 20561
[AhoHopUll] p. 2Section 1.1df-bigo 48470
[AhoHopUll] p. 12Section 1.3df-blen 48492
[AhoHopUll] p. 318Section 9.1df-concat 14546  df-pfx 14646  df-substr 14616  df-word 14489  lencl 14508  wrd0 14514
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24602  df-nmoo 30681
[AkhiezerGlazman] p. 64Theoremhmopidmch 32089  hmopidmchi 32087
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32137  pjcmul2i 32138
[AkhiezerGlazman] p. 72Theoremcnvunop 31854  unoplin 31856
[AkhiezerGlazman] p. 72Equation 2unopadj 31855  unopadj2 31874
[AkhiezerGlazman] p. 73Theoremelunop2 31949  lnopunii 31948
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32022
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27842
[Alling] p. 184Axiom Bbdayfo 27596
[Alling] p. 184Axiom Osltso 27595
[Alling] p. 184Axiom SDnodense 27611
[Alling] p. 185Lemma 0nocvxmin 27697
[Alling] p. 185Theoremconway 27718
[Alling] p. 185Axiom FEnoeta 27662
[Alling] p. 186Theorem 4slerec 27738
[Alling], p. 2Definitionrp-brsslt 43384
[Alling], p. 3Notenla0001 43387  nla0002 43385  nla0003 43386
[Apostol] p. 18Theorem I.1addcan 11376  addcan2d 11396  addcan2i 11386  addcand 11395  addcani 11385
[Apostol] p. 18Theorem I.2negeu 11429
[Apostol] p. 18Theorem I.3negsub 11488  negsubd 11557  negsubi 11518
[Apostol] p. 18Theorem I.4negneg 11490  negnegd 11542  negnegi 11510
[Apostol] p. 18Theorem I.5subdi 11627  subdid 11650  subdii 11643  subdir 11628  subdird 11651  subdiri 11644
[Apostol] p. 18Theorem I.6mul01 11371  mul01d 11391  mul01i 11382  mul02 11370  mul02d 11390  mul02i 11381
[Apostol] p. 18Theorem I.7mulcan 11831  mulcan2d 11828  mulcand 11827  mulcani 11833
[Apostol] p. 18Theorem I.8receu 11839  xreceu 32850
[Apostol] p. 18Theorem I.9divrec 11869  divrecd 11977  divreci 11943  divreczi 11936
[Apostol] p. 18Theorem I.10recrec 11895  recreci 11930
[Apostol] p. 18Theorem I.11mul0or 11834  mul0ord 11844  mul0ori 11842
[Apostol] p. 18Theorem I.12mul2neg 11633  mul2negd 11649  mul2negi 11642  mulneg1 11630  mulneg1d 11647  mulneg1i 11640
[Apostol] p. 18Theorem I.13divadddiv 11913  divadddivd 12018  divadddivi 11960
[Apostol] p. 18Theorem I.14divmuldiv 11898  divmuldivd 12015  divmuldivi 11958  rdivmuldivd 20328
[Apostol] p. 18Theorem I.15divdivdiv 11899  divdivdivd 12021  divdivdivi 11961
[Apostol] p. 20Axiom 7rpaddcl 12988  rpaddcld 13023  rpmulcl 12989  rpmulcld 13024
[Apostol] p. 20Axiom 8rpneg 12998
[Apostol] p. 20Axiom 90nrp 13001
[Apostol] p. 20Theorem I.17lttri 11318
[Apostol] p. 20Theorem I.18ltadd1d 11787  ltadd1dd 11805  ltadd1i 11748
[Apostol] p. 20Theorem I.19ltmul1 12048  ltmul1a 12047  ltmul1i 12117  ltmul1ii 12127  ltmul2 12049  ltmul2d 13050  ltmul2dd 13064  ltmul2i 12120
[Apostol] p. 20Theorem I.20msqgt0 11714  msqgt0d 11761  msqgt0i 11731
[Apostol] p. 20Theorem I.210lt1 11716
[Apostol] p. 20Theorem I.23lt0neg1 11700  lt0neg1d 11763  ltneg 11694  ltnegd 11772  ltnegi 11738
[Apostol] p. 20Theorem I.25lt2add 11679  lt2addd 11817  lt2addi 11756
[Apostol] p. 20Definition of positive numbersdf-rp 12966
[Apostol] p. 21Exercise 4recgt0 12044  recgt0d 12133  recgt0i 12104  recgt0ii 12105
[Apostol] p. 22Definition of integersdf-z 12546
[Apostol] p. 22Definition of positive integersdfnn3 12211
[Apostol] p. 22Definition of rationalsdf-q 12922
[Apostol] p. 24Theorem I.26supeu 9423
[Apostol] p. 26Theorem I.28nnunb 12454
[Apostol] p. 26Theorem I.29arch 12455  archd 45128
[Apostol] p. 28Exercise 2btwnz 12653
[Apostol] p. 28Exercise 3nnrecl 12456
[Apostol] p. 28Exercise 4rebtwnz 12920
[Apostol] p. 28Exercise 5zbtwnre 12919
[Apostol] p. 28Exercise 6qbtwnre 13172
[Apostol] p. 28Exercise 10(a)zeneo 16315  zneo 12633  zneoALTV 47625
[Apostol] p. 29Theorem I.35cxpsqrtth 26646  msqsqrtd 15416  resqrtth 15231  sqrtth 15340  sqrtthi 15346  sqsqrtd 15415
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12200
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12886
[Apostol] p. 361Remarkcrreczi 14203
[Apostol] p. 363Remarkabsgt0i 15375
[Apostol] p. 363Exampleabssubd 15429  abssubi 15379
[ApostolNT] p. 7Remarkfmtno0 47496  fmtno1 47497  fmtno2 47506  fmtno3 47507  fmtno4 47508  fmtno5fac 47538  fmtnofz04prm 47533
[ApostolNT] p. 7Definitiondf-fmtno 47484
[ApostolNT] p. 8Definitiondf-ppi 27017
[ApostolNT] p. 14Definitiondf-dvds 16230
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16246
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16270
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16265
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16259
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16261
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16247
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16248
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16253
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16287
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16289
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16291
[ApostolNT] p. 15Definitiondf-gcd 16471  dfgcd2 16522
[ApostolNT] p. 16Definitionisprm2 16658
[ApostolNT] p. 16Theorem 1.5coprmdvds 16629
[ApostolNT] p. 16Theorem 1.7prminf 16892
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16489
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16523
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16525
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16504
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16496
[ApostolNT] p. 17Theorem 1.8coprm 16687
[ApostolNT] p. 17Theorem 1.9euclemma 16689
[ApostolNT] p. 17Theorem 1.101arith2 16905
[ApostolNT] p. 18Theorem 1.13prmrec 16899
[ApostolNT] p. 19Theorem 1.14divalg 16379
[ApostolNT] p. 20Theorem 1.15eucalg 16563
[ApostolNT] p. 24Definitiondf-mu 27018
[ApostolNT] p. 25Definitiondf-phi 16742
[ApostolNT] p. 25Theorem 2.1musum 27108
[ApostolNT] p. 26Theorem 2.2phisum 16767
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16752
[ApostolNT] p. 28Theorem 2.5(c)phimul 16756
[ApostolNT] p. 32Definitiondf-vma 27015
[ApostolNT] p. 32Theorem 2.9muinv 27110
[ApostolNT] p. 32Theorem 2.10vmasum 27134
[ApostolNT] p. 38Remarkdf-sgm 27019
[ApostolNT] p. 38Definitiondf-sgm 27019
[ApostolNT] p. 75Definitiondf-chp 27016  df-cht 27014
[ApostolNT] p. 104Definitioncongr 16640
[ApostolNT] p. 106Remarkdvdsval3 16233
[ApostolNT] p. 106Definitionmoddvds 16240
[ApostolNT] p. 107Example 2mod2eq0even 16322
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16323
[ApostolNT] p. 107Example 4zmod1congr 13862
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13900
[ApostolNT] p. 107Theorem 5.2(c)modexp 14213
[ApostolNT] p. 108Theorem 5.3modmulconst 16264
[ApostolNT] p. 109Theorem 5.4cncongr1 16643
[ApostolNT] p. 109Theorem 5.6gcdmodi 17051
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16645
[ApostolNT] p. 113Theorem 5.17eulerth 16759
[ApostolNT] p. 113Theorem 5.18vfermltl 16778
[ApostolNT] p. 114Theorem 5.19fermltl 16760
[ApostolNT] p. 116Theorem 5.24wilthimp 26989
[ApostolNT] p. 179Definitiondf-lgs 27213  lgsprme0 27257
[ApostolNT] p. 180Example 11lgs 27258
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27234
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27249
[ApostolNT] p. 181Theorem 9.4m1lgs 27306
[ApostolNT] p. 181Theorem 9.52lgs 27325  2lgsoddprm 27334
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27292
[ApostolNT] p. 185Theorem 9.8lgsquad 27301
[ApostolNT] p. 188Definitiondf-lgs 27213  lgs1 27259
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27250
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27252
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27260
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27261
[Baer] p. 40Property (b)mapdord 41624
[Baer] p. 40Property (c)mapd11 41625
[Baer] p. 40Property (e)mapdin 41648  mapdlsm 41650
[Baer] p. 40Property (f)mapd0 41651
[Baer] p. 40Definition of projectivitydf-mapd 41611  mapd1o 41634
[Baer] p. 41Property (g)mapdat 41653
[Baer] p. 44Part (1)mapdpg 41692
[Baer] p. 45Part (2)hdmap1eq 41787  mapdheq 41714  mapdheq2 41715  mapdheq2biN 41716
[Baer] p. 45Part (3)baerlem3 41699
[Baer] p. 46Part (4)mapdheq4 41718  mapdheq4lem 41717
[Baer] p. 46Part (5)baerlem5a 41700  baerlem5abmN 41704  baerlem5amN 41702  baerlem5b 41701  baerlem5bmN 41703
[Baer] p. 47Part (6)hdmap1l6 41807  hdmap1l6a 41795  hdmap1l6e 41800  hdmap1l6f 41801  hdmap1l6g 41802  hdmap1l6lem1 41793  hdmap1l6lem2 41794  mapdh6N 41733  mapdh6aN 41721  mapdh6eN 41726  mapdh6fN 41727  mapdh6gN 41728  mapdh6lem1N 41719  mapdh6lem2N 41720
[Baer] p. 48Part 9hdmapval 41814
[Baer] p. 48Part 10hdmap10 41826
[Baer] p. 48Part 11hdmapadd 41829
[Baer] p. 48Part (6)hdmap1l6h 41803  mapdh6hN 41729
[Baer] p. 48Part (7)mapdh75cN 41739  mapdh75d 41740  mapdh75e 41738  mapdh75fN 41741  mapdh7cN 41735  mapdh7dN 41736  mapdh7eN 41734  mapdh7fN 41737
[Baer] p. 48Part (8)mapdh8 41774  mapdh8a 41761  mapdh8aa 41762  mapdh8ab 41763  mapdh8ac 41764  mapdh8ad 41765  mapdh8b 41766  mapdh8c 41767  mapdh8d 41769  mapdh8d0N 41768  mapdh8e 41770  mapdh8g 41771  mapdh8i 41772  mapdh8j 41773
[Baer] p. 48Part (9)mapdh9a 41775
[Baer] p. 48Equation 10mapdhvmap 41755
[Baer] p. 49Part 12hdmap11 41834  hdmapeq0 41830  hdmapf1oN 41851  hdmapneg 41832  hdmaprnN 41850  hdmaprnlem1N 41835  hdmaprnlem3N 41836  hdmaprnlem3uN 41837  hdmaprnlem4N 41839  hdmaprnlem6N 41840  hdmaprnlem7N 41841  hdmaprnlem8N 41842  hdmaprnlem9N 41843  hdmapsub 41833
[Baer] p. 49Part 14hdmap14lem1 41854  hdmap14lem10 41863  hdmap14lem1a 41852  hdmap14lem2N 41855  hdmap14lem2a 41853  hdmap14lem3 41856  hdmap14lem8 41861  hdmap14lem9 41862
[Baer] p. 50Part 14hdmap14lem11 41864  hdmap14lem12 41865  hdmap14lem13 41866  hdmap14lem14 41867  hdmap14lem15 41868  hgmapval 41873
[Baer] p. 50Part 15hgmapadd 41880  hgmapmul 41881  hgmaprnlem2N 41883  hgmapvs 41877
[Baer] p. 50Part 16hgmaprnN 41887
[Baer] p. 110Lemma 1hdmapip0com 41903
[Baer] p. 110Line 27hdmapinvlem1 41904
[Baer] p. 110Line 28hdmapinvlem2 41905
[Baer] p. 110Line 30hdmapinvlem3 41906
[Baer] p. 110Part 1.2hdmapglem5 41908  hgmapvv 41912
[Baer] p. 110Proposition 1hdmapinvlem4 41907
[Baer] p. 111Line 10hgmapvvlem1 41909
[Baer] p. 111Line 15hdmapg 41916  hdmapglem7 41915
[Bauer], p. 483Theorem 1.22irrexpq 26647  2irrexpqALT 26717
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2563
[BellMachover] p. 460Notationdf-mo 2534
[BellMachover] p. 460Definitionmo3 2558
[BellMachover] p. 461Axiom Extax-ext 2702
[BellMachover] p. 462Theorem 1.1axextmo 2706
[BellMachover] p. 463Axiom Repaxrep5 5250
[BellMachover] p. 463Scheme Sepax-sep 5259
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37049  sepex 5263
[BellMachover] p. 466Problemaxpow2 5330
[BellMachover] p. 466Axiom Powaxpow3 5331
[BellMachover] p. 466Axiom Unionaxun2 7720
[BellMachover] p. 468Definitiondf-ord 6343
[BellMachover] p. 469Theorem 2.2(i)ordirr 6358
[BellMachover] p. 469Theorem 2.2(iii)onelon 6365
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6360
[BellMachover] p. 471Definition of Ndf-om 7851
[BellMachover] p. 471Problem 2.5(ii)uniordint 7784
[BellMachover] p. 471Definition of Limdf-lim 6345
[BellMachover] p. 472Axiom Infzfinf2 9613
[BellMachover] p. 473Theorem 2.8limom 7866
[BellMachover] p. 477Equation 3.1df-r1 9735
[BellMachover] p. 478Definitionrankval2 9789
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9753  r1ord3g 9750
[BellMachover] p. 480Axiom Regzfreg 9566
[BellMachover] p. 488Axiom ACac5 10448  dfac4 10093
[BellMachover] p. 490Definition of alephalephval3 10081
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39304
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32289
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32331  chirredi 32330
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32319
[Beran] p. 3Definition of joinsshjval3 31290
[Beran] p. 39Theorem 2.3(i)cmcm2 31552  cmcm2i 31529  cmcm2ii 31534  cmt2N 39235
[Beran] p. 40Theorem 2.3(iii)lecm 31553  lecmi 31538  lecmii 31539
[Beran] p. 45Theorem 3.4cmcmlem 31527
[Beran] p. 49Theorem 4.2cm2j 31556  cm2ji 31561  cm2mi 31562
[Beran] p. 95Definitiondf-sh 31143  issh2 31145
[Beran] p. 95Lemma 3.1(S5)his5 31022
[Beran] p. 95Lemma 3.1(S6)his6 31035
[Beran] p. 95Lemma 3.1(S7)his7 31026
[Beran] p. 95Lemma 3.2(S8)ho01i 31764
[Beran] p. 95Lemma 3.2(S9)hoeq1 31766
[Beran] p. 95Lemma 3.2(S10)ho02i 31765
[Beran] p. 95Lemma 3.2(S11)hoeq2 31767
[Beran] p. 95Postulate (S1)ax-his1 31018  his1i 31036
[Beran] p. 95Postulate (S2)ax-his2 31019
[Beran] p. 95Postulate (S3)ax-his3 31020
[Beran] p. 95Postulate (S4)ax-his4 31021
[Beran] p. 96Definition of normdf-hnorm 30904  dfhnorm2 31058  normval 31060
[Beran] p. 96Definition for Cauchy sequencehcau 31120
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30909
[Beran] p. 96Definition of complete subspaceisch3 31177
[Beran] p. 96Definition of convergedf-hlim 30908  hlimi 31124
[Beran] p. 97Theorem 3.3(i)norm-i-i 31069  norm-i 31065
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31073  norm-ii 31074  normlem0 31045  normlem1 31046  normlem2 31047  normlem3 31048  normlem4 31049  normlem5 31050  normlem6 31051  normlem7 31052  normlem7tALT 31055
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31075  norm-iii 31076
[Beran] p. 98Remark 3.4bcs 31117  bcsiALT 31115  bcsiHIL 31116
[Beran] p. 98Remark 3.4(B)normlem9at 31057  normpar 31091  normpari 31090
[Beran] p. 98Remark 3.4(C)normpyc 31082  normpyth 31081  normpythi 31078
[Beran] p. 99Remarklnfn0 31983  lnfn0i 31978  lnop0 31902  lnop0i 31906
[Beran] p. 99Theorem 3.5(i)nmcexi 31962  nmcfnex 31989  nmcfnexi 31987  nmcopex 31965  nmcopexi 31963
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 31990  nmcfnlbi 31988  nmcoplb 31966  nmcoplbi 31964
[Beran] p. 99Theorem 3.5(iii)lnfncon 31992  lnfnconi 31991  lnopcon 31971  lnopconi 31970
[Beran] p. 100Lemma 3.6normpar2i 31092
[Beran] p. 101Lemma 3.6norm3adifi 31089  norm3adifii 31084  norm3dif 31086  norm3difi 31083
[Beran] p. 102Theorem 3.7(i)chocunii 31237  pjhth 31329  pjhtheu 31330  pjpjhth 31361  pjpjhthi 31362  pjth 25346
[Beran] p. 102Theorem 3.7(ii)ococ 31342  ococi 31341
[Beran] p. 103Remark 3.8nlelchi 31997
[Beran] p. 104Theorem 3.9riesz3i 31998  riesz4 32000  riesz4i 31999
[Beran] p. 104Theorem 3.10cnlnadj 32015  cnlnadjeu 32014  cnlnadjeui 32013  cnlnadji 32012  cnlnadjlem1 32003  nmopadjlei 32024
[Beran] p. 106Theorem 3.11(i)adjeq0 32027
[Beran] p. 106Theorem 3.11(v)nmopadji 32026
[Beran] p. 106Theorem 3.11(ii)adjmul 32028
[Beran] p. 106Theorem 3.11(iv)adjadj 31872
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32038  nmopcoadji 32037
[Beran] p. 106Theorem 3.11(iii)adjadd 32029
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32039
[Beran] p. 106Theorem 3.11(viii)adjcoi 32036  pjadj2coi 32140  pjadjcoi 32097
[Beran] p. 107Definitiondf-ch 31157  isch2 31159
[Beran] p. 107Remark 3.12choccl 31242  isch3 31177  occl 31240  ocsh 31219  shoccl 31241  shocsh 31220
[Beran] p. 107Remark 3.12(B)ococin 31344
[Beran] p. 108Theorem 3.13chintcl 31268
[Beran] p. 109Property (i)pjadj2 32123  pjadj3 32124  pjadji 31621  pjadjii 31610
[Beran] p. 109Property (ii)pjidmco 32117  pjidmcoi 32113  pjidmi 31609
[Beran] p. 110Definition of projector orderingpjordi 32109
[Beran] p. 111Remarkho0val 31686  pjch1 31606
[Beran] p. 111Definitiondf-hfmul 31670  df-hfsum 31669  df-hodif 31668  df-homul 31667  df-hosum 31666
[Beran] p. 111Lemma 4.4(i)pjo 31607
[Beran] p. 111Lemma 4.4(ii)pjch 31630  pjchi 31368
[Beran] p. 111Lemma 4.4(iii)pjoc2 31375  pjoc2i 31374
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31616
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32101  pjssmii 31617
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32100
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32099
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32104
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32102  pjssge0ii 31618
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32103  pjdifnormii 31619
[Bobzien] p. 116Statement T3stoic3 1776
[Bobzien] p. 117Statement T2stoic2a 1774
[Bobzien] p. 117Statement T4stoic4a 1777
[Bobzien] p. 117Conclusion the contradictorystoic1a 1772
[Bogachev] p. 16Definition 1.5df-oms 34291
[Bogachev] p. 17Lemma 1.5.4omssubadd 34299
[Bogachev] p. 17Example 1.5.2omsmon 34297
[Bogachev] p. 41Definition 1.11.2df-carsg 34301
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34321
[Bogachev] p. 116Definition 2.3.1df-itgm 34352  df-sitm 34330
[Bogachev] p. 118Chapter 2.4.4df-itgm 34352
[Bogachev] p. 118Definition 2.4.1df-sitg 34329
[Bollobas] p. 1Section I.1df-edg 28982  isuhgrop 29004  isusgrop 29096  isuspgrop 29095
[Bollobas] p. 2Section I.1df-isubgr 47816  df-subgr 29202  uhgrspan1 29237  uhgrspansubgr 29225
[Bollobas] p. 3Definitiondf-gric 47836  gricuspgr 47873  isuspgrim 47851
[Bollobas] p. 3Section I.1cusgrsize 29389  df-clnbgr 47775  df-cusgr 29346  df-nbgr 29267  fusgrmaxsize 29399
[Bollobas] p. 4Definitiondf-upwlks 48051  df-wlks 29534
[Bollobas] p. 4Section I.1finsumvtxdg2size 29485  finsumvtxdgeven 29487  fusgr1th 29486  fusgrvtxdgonume 29489  vtxdgoddnumeven 29488
[Bollobas] p. 5Notationdf-pths 29651
[Bollobas] p. 5Definitiondf-crcts 29723  df-cycls 29724  df-trls 29627  df-wlkson 29535
[Bollobas] p. 7Section I.1df-ushgr 28993
[BourbakiAlg1] p. 1Definition 1df-clintop 48117  df-cllaw 48103  df-mgm 18573  df-mgm2 48136
[BourbakiAlg1] p. 4Definition 5df-assintop 48118  df-asslaw 48105  df-sgrp 18652  df-sgrp2 48138
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48137  df-comlaw 48104
[BourbakiAlg1] p. 12Definition 2df-mnd 18668
[BourbakiAlg1] p. 17Chapter I.mndlactf1 32975  mndlactf1o 32979  mndractf1 32977  mndractf1o 32980
[BourbakiAlg1] p. 92Definition 1df-ring 20150
[BourbakiAlg1] p. 93Section I.8.1df-rng 20068
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33637
[BourbakiAlg2] p. 113Chapter 5.assafld 33641  assarrginv 33640
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33681  fldextrspunfld 33679  fldextrspunlem1 33678  fldextrspunlem2 33680  fldextrspunlsp 33677  fldextrspunlsplem 33676
[BourbakiCAlg2], p. 228Proposition 21arithidom 33516  dfufd2 33529
[BourbakiEns] p. Proposition 8fcof1 7269  fcofo 7270
[BourbakiTop1] p. Remarkxnegmnf 13183  xnegpnf 13182
[BourbakiTop1] p. Remark rexneg 13184
[BourbakiTop1] p. Remark 3ust0 24113  ustfilxp 24106
[BourbakiTop1] p. Axiom GT'tgpsubcn 23983
[BourbakiTop1] p. Criterionishmeo 23652
[BourbakiTop1] p. Example 1cstucnd 24177  iducn 24176  snfil 23757
[BourbakiTop1] p. Example 2neifil 23773
[BourbakiTop1] p. Theorem 1cnextcn 23960
[BourbakiTop1] p. Theorem 2ucnextcn 24197
[BourbakiTop1] p. Theorem 3df-hcmp 33955
[BourbakiTop1] p. Paragraph 3infil 23756
[BourbakiTop1] p. Definition 1df-ucn 24169  df-ust 24094  filintn0 23754  filn0 23755  istgp 23970  ucnprima 24175
[BourbakiTop1] p. Definition 2df-cfilu 24180
[BourbakiTop1] p. Definition 3df-cusp 24191  df-usp 24151  df-utop 24125  trust 24123
[BourbakiTop1] p. Definition 6df-pcmp 33854
[BourbakiTop1] p. Property V_issnei2 23009
[BourbakiTop1] p. Theorem 1(d)iscncl 23162
[BourbakiTop1] p. Condition F_Iustssel 24099
[BourbakiTop1] p. Condition U_Iustdiag 24102
[BourbakiTop1] p. Property V_iiinnei 23018
[BourbakiTop1] p. Property V_ivneiptopreu 23026  neissex 23020
[BourbakiTop1] p. Proposition 1neips 23006  neiss 23002  ucncn 24178  ustund 24115  ustuqtop 24140
[BourbakiTop1] p. Proposition 2cnpco 23160  neiptopreu 23026  utop2nei 24144  utop3cls 24145
[BourbakiTop1] p. Proposition 3fmucnd 24185  uspreg 24167  utopreg 24146
[BourbakiTop1] p. Proposition 4imasncld 23584  imasncls 23585  imasnopn 23583
[BourbakiTop1] p. Proposition 9cnpflf2 23893
[BourbakiTop1] p. Condition F_IIustincl 24101
[BourbakiTop1] p. Condition U_IIustinvel 24103
[BourbakiTop1] p. Property V_iiielnei 23004
[BourbakiTop1] p. Proposition 11cnextucn 24196
[BourbakiTop1] p. Condition F_IIbustbasel 24100
[BourbakiTop1] p. Condition U_IIIustexhalf 24104
[BourbakiTop1] p. Definition C'''df-cmp 23280
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23739
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22787
[BourbakiTop2] p. 195Definition 1df-ldlf 33851
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46033
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46035  stoweid 46034
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 45972  stoweidlem10 45981  stoweidlem14 45985  stoweidlem15 45986  stoweidlem35 46006  stoweidlem36 46007  stoweidlem37 46008  stoweidlem38 46009  stoweidlem40 46011  stoweidlem41 46012  stoweidlem43 46014  stoweidlem44 46015  stoweidlem46 46017  stoweidlem5 45976  stoweidlem50 46021  stoweidlem52 46023  stoweidlem53 46024  stoweidlem55 46026  stoweidlem56 46027
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 45994  stoweidlem24 45995  stoweidlem27 45998  stoweidlem28 45999  stoweidlem30 46001
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46005  stoweidlem59 46030  stoweidlem60 46031
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46016  stoweidlem49 46020  stoweidlem7 45978
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46002  stoweidlem39 46010  stoweidlem42 46013  stoweidlem48 46019  stoweidlem51 46022  stoweidlem54 46025  stoweidlem57 46028  stoweidlem58 46029
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 45996
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 45988
[BrosowskiDeutsh] p. 92Proofstoweidlem11 45982  stoweidlem13 45984  stoweidlem26 45997  stoweidlem61 46032
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 45989
[Bruck] p. 1Section I.1df-clintop 48117  df-mgm 18573  df-mgm2 48136
[Bruck] p. 23Section II.1df-sgrp 18652  df-sgrp2 48138
[Bruck] p. 28Theorem 3.2dfgrp3 18977
[ChoquetDD] p. 2Definition of mappingdf-mpt 5197
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 30339
[Clemente] p. 10Definition I` `m,nnatded 30339
[Clemente] p. 11Definition E=>m,nnatded 30339
[Clemente] p. 11Definition I=>m,nnatded 30339
[Clemente] p. 11Definition E` `(1)natded 30339
[Clemente] p. 11Definition E` `(2)natded 30339
[Clemente] p. 12Definition E` `m,n,pnatded 30339
[Clemente] p. 12Definition I` `n(1)natded 30339
[Clemente] p. 12Definition I` `n(2)natded 30339
[Clemente] p. 13Definition I` `m,n,pnatded 30339
[Clemente] p. 14Proof 5.11natded 30339
[Clemente] p. 14Definition E` `nnatded 30339
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30341  ex-natded5.2 30340
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30344  ex-natded5.3 30343
[Clemente] p. 18Theorem 5.5ex-natded5.5 30346
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30348  ex-natded5.7 30347
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30350  ex-natded5.8 30349
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30352  ex-natded5.13 30351
[Clemente] p. 32Definition I` `nnatded 30339
[Clemente] p. 32Definition E` `m,n,p,anatded 30339
[Clemente] p. 32Definition E` `n,tnatded 30339
[Clemente] p. 32Definition I` `n,tnatded 30339
[Clemente] p. 43Theorem 9.20ex-natded9.20 30353
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30354
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30356  ex-natded9.26 30355
[Cohen] p. 301Remarkrelogoprlem 26507
[Cohen] p. 301Property 2relogmul 26508  relogmuld 26541
[Cohen] p. 301Property 3relogdiv 26509  relogdivd 26542
[Cohen] p. 301Property 4relogexp 26512
[Cohen] p. 301Property 1alog1 26501
[Cohen] p. 301Property 1bloge 26502
[Cohen4] p. 348Observationrelogbcxpb 26704
[Cohen4] p. 349Propertyrelogbf 26708
[Cohen4] p. 352Definitionelogb 26687
[Cohen4] p. 361Property 2relogbmul 26694
[Cohen4] p. 361Property 3logbrec 26699  relogbdiv 26696
[Cohen4] p. 361Property 4relogbreexp 26692
[Cohen4] p. 361Property 6relogbexp 26697
[Cohen4] p. 361Property 1(a)logbid1 26685
[Cohen4] p. 361Property 1(b)logb1 26686
[Cohen4] p. 367Propertylogbchbase 26688
[Cohen4] p. 377Property 2logblt 26701
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34284  sxbrsigalem4 34286
[Cohn] p. 81Section II.5acsdomd 18522  acsinfd 18521  acsinfdimd 18523  acsmap2d 18520  acsmapd 18519
[Cohn] p. 143Example 5.1.1sxbrsiga 34289
[Connell] p. 57Definitiondf-scmat 22384  df-scmatalt 48317
[Conway] p. 4Definitionslerec 27738
[Conway] p. 5Definitionaddsval 27876  addsval2 27877  df-adds 27874  df-muls 28017  df-negs 27934
[Conway] p. 7Theorem0slt1s 27748
[Conway] p. 16Theorem 0(i)ssltright 27790
[Conway] p. 16Theorem 0(ii)ssltleft 27789
[Conway] p. 16Theorem 0(iii)slerflex 27682
[Conway] p. 17Theorem 3addsass 27919  addsassd 27920  addscom 27880  addscomd 27881  addsrid 27878  addsridd 27879
[Conway] p. 17Definitiondf-0s 27743
[Conway] p. 17Theorem 4(ii)negnegs 27957
[Conway] p. 17Theorem 4(iii)negsid 27954  negsidd 27955
[Conway] p. 18Theorem 5sleadd1 27903  sleadd1d 27909
[Conway] p. 18Definitiondf-1s 27744
[Conway] p. 18Theorem 6(ii)negscl 27949  negscld 27950
[Conway] p. 18Theorem 6(iii)addscld 27894
[Conway] p. 19Notemulsunif2 28080
[Conway] p. 19Theorem 7addsdi 28065  addsdid 28066  addsdird 28067  mulnegs1d 28070  mulnegs2d 28071  mulsass 28076  mulsassd 28077  mulscom 28049  mulscomd 28050
[Conway] p. 19Theorem 8(i)mulscl 28044  mulscld 28045
[Conway] p. 19Theorem 8(iii)slemuld 28048  sltmul 28046  sltmuld 28047
[Conway] p. 20Theorem 9mulsgt0 28054  mulsgt0d 28055
[Conway] p. 21Theorem 10(iv)precsex 28127
[Conway] p. 24Definitiondf-reno 28352
[Conway] p. 24Theorem 13(ii)readdscl 28357  remulscl 28360  renegscl 28356
[Conway] p. 27Definitiondf-ons 28160  elons2 28166
[Conway] p. 27Theorem 14sltonex 28170
[Conway] p. 28Theorem 15onscutlt 28172  onswe 28177
[Conway] p. 29Remarkmadebday 27818  newbday 27820  oldbday 27819
[Conway] p. 29Definitiondf-made 27762  df-new 27764  df-old 27763
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13835
[Crawley] p. 1Definition of posetdf-poset 18280
[Crawley] p. 107Theorem 13.2hlsupr 39372
[Crawley] p. 110Theorem 13.3arglem1N 40176  dalaw 39872
[Crawley] p. 111Theorem 13.4hlathil 41947
[Crawley] p. 111Definition of set Wdf-watsN 39976
[Crawley] p. 111Definition of dilationdf-dilN 40092  df-ldil 40090  isldil 40096
[Crawley] p. 111Definition of translationdf-ltrn 40091  df-trnN 40093  isltrn 40105  ltrnu 40107
[Crawley] p. 112Lemma Acdlema1N 39777  cdlema2N 39778  exatleN 39390
[Crawley] p. 112Lemma B1cvrat 39462  cdlemb 39780  cdlemb2 40027  cdlemb3 40592  idltrn 40136  l1cvat 39040  lhpat 40029  lhpat2 40031  lshpat 39041  ltrnel 40125  ltrnmw 40137
[Crawley] p. 112Lemma Ccdlemc1 40177  cdlemc2 40178  ltrnnidn 40160  trlat 40155  trljat1 40152  trljat2 40153  trljat3 40154  trlne 40171  trlnidat 40159  trlnle 40172
[Crawley] p. 112Definition of automorphismdf-pautN 39977
[Crawley] p. 113Lemma Ccdlemc 40183  cdlemc3 40179  cdlemc4 40180
[Crawley] p. 113Lemma Dcdlemd 40193  cdlemd1 40184  cdlemd2 40185  cdlemd3 40186  cdlemd4 40187  cdlemd5 40188  cdlemd6 40189  cdlemd7 40190  cdlemd8 40191  cdlemd9 40192  cdleme31sde 40371  cdleme31se 40368  cdleme31se2 40369  cdleme31snd 40372  cdleme32a 40427  cdleme32b 40428  cdleme32c 40429  cdleme32d 40430  cdleme32e 40431  cdleme32f 40432  cdleme32fva 40423  cdleme32fva1 40424  cdleme32fvcl 40426  cdleme32le 40433  cdleme48fv 40485  cdleme4gfv 40493  cdleme50eq 40527  cdleme50f 40528  cdleme50f1 40529  cdleme50f1o 40532  cdleme50laut 40533  cdleme50ldil 40534  cdleme50lebi 40526  cdleme50rn 40531  cdleme50rnlem 40530  cdlemeg49le 40497  cdlemeg49lebilem 40525
[Crawley] p. 113Lemma Ecdleme 40546  cdleme00a 40195  cdleme01N 40207  cdleme02N 40208  cdleme0a 40197  cdleme0aa 40196  cdleme0b 40198  cdleme0c 40199  cdleme0cp 40200  cdleme0cq 40201  cdleme0dN 40202  cdleme0e 40203  cdleme0ex1N 40209  cdleme0ex2N 40210  cdleme0fN 40204  cdleme0gN 40205  cdleme0moN 40211  cdleme1 40213  cdleme10 40240  cdleme10tN 40244  cdleme11 40256  cdleme11a 40246  cdleme11c 40247  cdleme11dN 40248  cdleme11e 40249  cdleme11fN 40250  cdleme11g 40251  cdleme11h 40252  cdleme11j 40253  cdleme11k 40254  cdleme11l 40255  cdleme12 40257  cdleme13 40258  cdleme14 40259  cdleme15 40264  cdleme15a 40260  cdleme15b 40261  cdleme15c 40262  cdleme15d 40263  cdleme16 40271  cdleme16aN 40245  cdleme16b 40265  cdleme16c 40266  cdleme16d 40267  cdleme16e 40268  cdleme16f 40269  cdleme16g 40270  cdleme19a 40289  cdleme19b 40290  cdleme19c 40291  cdleme19d 40292  cdleme19e 40293  cdleme19f 40294  cdleme1b 40212  cdleme2 40214  cdleme20aN 40295  cdleme20bN 40296  cdleme20c 40297  cdleme20d 40298  cdleme20e 40299  cdleme20f 40300  cdleme20g 40301  cdleme20h 40302  cdleme20i 40303  cdleme20j 40304  cdleme20k 40305  cdleme20l 40308  cdleme20l1 40306  cdleme20l2 40307  cdleme20m 40309  cdleme20y 40288  cdleme20zN 40287  cdleme21 40323  cdleme21d 40316  cdleme21e 40317  cdleme22a 40326  cdleme22aa 40325  cdleme22b 40327  cdleme22cN 40328  cdleme22d 40329  cdleme22e 40330  cdleme22eALTN 40331  cdleme22f 40332  cdleme22f2 40333  cdleme22g 40334  cdleme23a 40335  cdleme23b 40336  cdleme23c 40337  cdleme26e 40345  cdleme26eALTN 40347  cdleme26ee 40346  cdleme26f 40349  cdleme26f2 40351  cdleme26f2ALTN 40350  cdleme26fALTN 40348  cdleme27N 40355  cdleme27a 40353  cdleme27cl 40352  cdleme28c 40358  cdleme3 40223  cdleme30a 40364  cdleme31fv 40376  cdleme31fv1 40377  cdleme31fv1s 40378  cdleme31fv2 40379  cdleme31id 40380  cdleme31sc 40370  cdleme31sdnN 40373  cdleme31sn 40366  cdleme31sn1 40367  cdleme31sn1c 40374  cdleme31sn2 40375  cdleme31so 40365  cdleme35a 40434  cdleme35b 40436  cdleme35c 40437  cdleme35d 40438  cdleme35e 40439  cdleme35f 40440  cdleme35fnpq 40435  cdleme35g 40441  cdleme35h 40442  cdleme35h2 40443  cdleme35sn2aw 40444  cdleme35sn3a 40445  cdleme36a 40446  cdleme36m 40447  cdleme37m 40448  cdleme38m 40449  cdleme38n 40450  cdleme39a 40451  cdleme39n 40452  cdleme3b 40215  cdleme3c 40216  cdleme3d 40217  cdleme3e 40218  cdleme3fN 40219  cdleme3fa 40222  cdleme3g 40220  cdleme3h 40221  cdleme4 40224  cdleme40m 40453  cdleme40n 40454  cdleme40v 40455  cdleme40w 40456  cdleme41fva11 40463  cdleme41sn3aw 40460  cdleme41sn4aw 40461  cdleme41snaw 40462  cdleme42a 40457  cdleme42b 40464  cdleme42c 40458  cdleme42d 40459  cdleme42e 40465  cdleme42f 40466  cdleme42g 40467  cdleme42h 40468  cdleme42i 40469  cdleme42k 40470  cdleme42ke 40471  cdleme42keg 40472  cdleme42mN 40473  cdleme42mgN 40474  cdleme43aN 40475  cdleme43bN 40476  cdleme43cN 40477  cdleme43dN 40478  cdleme5 40226  cdleme50ex 40545  cdleme50ltrn 40543  cdleme51finvN 40542  cdleme51finvfvN 40541  cdleme51finvtrN 40544  cdleme6 40227  cdleme7 40235  cdleme7a 40229  cdleme7aa 40228  cdleme7b 40230  cdleme7c 40231  cdleme7d 40232  cdleme7e 40233  cdleme7ga 40234  cdleme8 40236  cdleme8tN 40241  cdleme9 40239  cdleme9a 40237  cdleme9b 40238  cdleme9tN 40243  cdleme9taN 40242  cdlemeda 40284  cdlemedb 40283  cdlemednpq 40285  cdlemednuN 40286  cdlemefr27cl 40389  cdlemefr32fva1 40396  cdlemefr32fvaN 40395  cdlemefrs32fva 40386  cdlemefrs32fva1 40387  cdlemefs27cl 40399  cdlemefs32fva1 40409  cdlemefs32fvaN 40408  cdlemesner 40282  cdlemeulpq 40206
[Crawley] p. 114Lemma E4atex 40062  4atexlem7 40061  cdleme0nex 40276  cdleme17a 40272  cdleme17c 40274  cdleme17d 40484  cdleme17d1 40275  cdleme17d2 40481  cdleme18a 40277  cdleme18b 40278  cdleme18c 40279  cdleme18d 40281  cdleme4a 40225
[Crawley] p. 115Lemma Ecdleme21a 40311  cdleme21at 40314  cdleme21b 40312  cdleme21c 40313  cdleme21ct 40315  cdleme21f 40318  cdleme21g 40319  cdleme21h 40320  cdleme21i 40321  cdleme22gb 40280
[Crawley] p. 116Lemma Fcdlemf 40549  cdlemf1 40547  cdlemf2 40548
[Crawley] p. 116Lemma Gcdlemftr1 40553  cdlemg16 40643  cdlemg28 40690  cdlemg28a 40679  cdlemg28b 40689  cdlemg3a 40583  cdlemg42 40715  cdlemg43 40716  cdlemg44 40719  cdlemg44a 40717  cdlemg46 40721  cdlemg47 40722  cdlemg9 40620  ltrnco 40705  ltrncom 40724  tgrpabl 40737  trlco 40713
[Crawley] p. 116Definition of Gdf-tgrp 40729
[Crawley] p. 117Lemma Gcdlemg17 40663  cdlemg17b 40648
[Crawley] p. 117Definition of Edf-edring-rN 40742  df-edring 40743
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40746
[Crawley] p. 118Remarktendopltp 40766
[Crawley] p. 118Lemma Hcdlemh 40803  cdlemh1 40801  cdlemh2 40802
[Crawley] p. 118Lemma Icdlemi 40806  cdlemi1 40804  cdlemi2 40805
[Crawley] p. 118Lemma Jcdlemj1 40807  cdlemj2 40808  cdlemj3 40809  tendocan 40810
[Crawley] p. 118Lemma Kcdlemk 40960  cdlemk1 40817  cdlemk10 40829  cdlemk11 40835  cdlemk11t 40932  cdlemk11ta 40915  cdlemk11tb 40917  cdlemk11tc 40931  cdlemk11u-2N 40875  cdlemk11u 40857  cdlemk12 40836  cdlemk12u-2N 40876  cdlemk12u 40858  cdlemk13-2N 40862  cdlemk13 40838  cdlemk14-2N 40864  cdlemk14 40840  cdlemk15-2N 40865  cdlemk15 40841  cdlemk16-2N 40866  cdlemk16 40843  cdlemk16a 40842  cdlemk17-2N 40867  cdlemk17 40844  cdlemk18-2N 40872  cdlemk18-3N 40886  cdlemk18 40854  cdlemk19-2N 40873  cdlemk19 40855  cdlemk19u 40956  cdlemk1u 40845  cdlemk2 40818  cdlemk20-2N 40878  cdlemk20 40860  cdlemk21-2N 40877  cdlemk21N 40859  cdlemk22-3 40887  cdlemk22 40879  cdlemk23-3 40888  cdlemk24-3 40889  cdlemk25-3 40890  cdlemk26-3 40892  cdlemk26b-3 40891  cdlemk27-3 40893  cdlemk28-3 40894  cdlemk29-3 40897  cdlemk3 40819  cdlemk30 40880  cdlemk31 40882  cdlemk32 40883  cdlemk33N 40895  cdlemk34 40896  cdlemk35 40898  cdlemk36 40899  cdlemk37 40900  cdlemk38 40901  cdlemk39 40902  cdlemk39u 40954  cdlemk4 40820  cdlemk41 40906  cdlemk42 40927  cdlemk42yN 40930  cdlemk43N 40949  cdlemk45 40933  cdlemk46 40934  cdlemk47 40935  cdlemk48 40936  cdlemk49 40937  cdlemk5 40822  cdlemk50 40938  cdlemk51 40939  cdlemk52 40940  cdlemk53 40943  cdlemk54 40944  cdlemk55 40947  cdlemk55u 40952  cdlemk56 40957  cdlemk5a 40821  cdlemk5auN 40846  cdlemk5u 40847  cdlemk6 40823  cdlemk6u 40848  cdlemk7 40834  cdlemk7u-2N 40874  cdlemk7u 40856  cdlemk8 40824  cdlemk9 40825  cdlemk9bN 40826  cdlemki 40827  cdlemkid 40922  cdlemkj-2N 40868  cdlemkj 40849  cdlemksat 40832  cdlemksel 40831  cdlemksv 40830  cdlemksv2 40833  cdlemkuat 40852  cdlemkuel-2N 40870  cdlemkuel-3 40884  cdlemkuel 40851  cdlemkuv-2N 40869  cdlemkuv2-2 40871  cdlemkuv2-3N 40885  cdlemkuv2 40853  cdlemkuvN 40850  cdlemkvcl 40828  cdlemky 40912  cdlemkyyN 40948  tendoex 40961
[Crawley] p. 120Remarkdva1dim 40971
[Crawley] p. 120Lemma Lcdleml1N 40962  cdleml2N 40963  cdleml3N 40964  cdleml4N 40965  cdleml5N 40966  cdleml6 40967  cdleml7 40968  cdleml8 40969  cdleml9 40970  dia1dim 41047
[Crawley] p. 120Lemma Mdia11N 41034  diaf11N 41035  dialss 41032  diaord 41033  dibf11N 41147  djajN 41123
[Crawley] p. 120Definition of isomorphism mapdiaval 41018
[Crawley] p. 121Lemma Mcdlemm10N 41104  dia2dimlem1 41050  dia2dimlem2 41051  dia2dimlem3 41052  dia2dimlem4 41053  dia2dimlem5 41054  diaf1oN 41116  diarnN 41115  dvheveccl 41098  dvhopN 41102
[Crawley] p. 121Lemma Ncdlemn 41198  cdlemn10 41192  cdlemn11 41197  cdlemn11a 41193  cdlemn11b 41194  cdlemn11c 41195  cdlemn11pre 41196  cdlemn2 41181  cdlemn2a 41182  cdlemn3 41183  cdlemn4 41184  cdlemn4a 41185  cdlemn5 41187  cdlemn5pre 41186  cdlemn6 41188  cdlemn7 41189  cdlemn8 41190  cdlemn9 41191  diclspsn 41180
[Crawley] p. 121Definition of phi(q)df-dic 41159
[Crawley] p. 122Lemma Ndih11 41251  dihf11 41253  dihjust 41203  dihjustlem 41202  dihord 41250  dihord1 41204  dihord10 41209  dihord11b 41208  dihord11c 41210  dihord2 41213  dihord2a 41205  dihord2b 41206  dihord2cN 41207  dihord2pre 41211  dihord2pre2 41212  dihordlem6 41199  dihordlem7 41200  dihordlem7b 41201
[Crawley] p. 122Definition of isomorphism mapdihffval 41216  dihfval 41217  dihval 41218
[Diestel] p. 3Definitiondf-gric 47836  df-grim 47833  isuspgrim 47851
[Diestel] p. 3Section 1.1df-cusgr 29346  df-nbgr 29267
[Diestel] p. 3Definition by df-grisom 47832
[Diestel] p. 4Section 1.1df-isubgr 47816  df-subgr 29202  uhgrspan1 29237  uhgrspansubgr 29225
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29489  vtxdgoddnumeven 29488
[Diestel] p. 27Section 1.10df-ushgr 28993
[EGA] p. 80Notation 1.1.1rspecval 33862
[EGA] p. 80Proposition 1.1.2zartop 33874
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33866  zarcls1 33867
[EGA] p. 81Corollary 1.1.8zart0 33877
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33880
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33883
[Eisenberg] p. 67Definition 5.3df-dif 3925
[Eisenberg] p. 82Definition 6.3dfom3 9618
[Eisenberg] p. 125Definition 8.21df-map 8805
[Eisenberg] p. 216Example 13.2(4)omenps 9626
[Eisenberg] p. 310Theorem 19.8cardprc 9951
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10526
[Enderton] p. 18Axiom of Empty Setaxnul 5268
[Enderton] p. 19Definitiondf-tp 4602
[Enderton] p. 26Exercise 5unissb 4911
[Enderton] p. 26Exercise 10pwel 5344
[Enderton] p. 28Exercise 7(b)pwun 5539
[Enderton] p. 30Theorem "Distributive laws"iinin1 5051  iinin2 5050  iinun2 5045  iunin1 5044  iunin1f 32493  iunin2 5043  uniin1 32487  uniin2 32488
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5049  iundif2 5046
[Enderton] p. 32Exercise 20unineq 4259
[Enderton] p. 33Exercise 23iinuni 5070
[Enderton] p. 33Exercise 25iununi 5071
[Enderton] p. 33Exercise 24(a)iinpw 5078
[Enderton] p. 33Exercise 24(b)iunpw 7754  iunpwss 5079
[Enderton] p. 36Definitionopthwiener 5482
[Enderton] p. 38Exercise 6(a)unipw 5418
[Enderton] p. 38Exercise 6(b)pwuni 4917
[Enderton] p. 41Lemma 3Dopeluu 5438  rnex 7895  rnexg 7887
[Enderton] p. 41Exercise 8dmuni 5886  rnuni 6129
[Enderton] p. 42Definition of a functiondffun7 6551  dffun8 6552
[Enderton] p. 43Definition of function valuefunfv2 6956
[Enderton] p. 43Definition of single-rootedfuncnv 6593
[Enderton] p. 44Definition (d)dfima2 6041  dfima3 6042
[Enderton] p. 47Theorem 3Hfvco2 6965
[Enderton] p. 49Axiom of Choice (first form)ac7 10444  ac7g 10445  df-ac 10087  dfac2 10103  dfac2a 10101  dfac2b 10102  dfac3 10092  dfac7 10104
[Enderton] p. 50Theorem 3K(a)imauni 7227
[Enderton] p. 52Definitiondf-map 8805
[Enderton] p. 53Exercise 21coass 6246
[Enderton] p. 53Exercise 27dmco 6235
[Enderton] p. 53Exercise 14(a)funin 6600
[Enderton] p. 53Exercise 22(a)imass2 6081
[Enderton] p. 54Remarkixpf 8897  ixpssmap 8909
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8875
[Enderton] p. 55Axiom of Choice (second form)ac9 10454  ac9s 10464
[Enderton] p. 56Theorem 3Meqvrelref 38595  erref 8702
[Enderton] p. 57Lemma 3Neqvrelthi 38598  erthi 8735
[Enderton] p. 57Definitiondf-ec 8684
[Enderton] p. 58Definitiondf-qs 8688
[Enderton] p. 61Exercise 35df-ec 8684
[Enderton] p. 65Exercise 56(a)dmun 5882
[Enderton] p. 68Definition of successordf-suc 6346
[Enderton] p. 71Definitiondf-tr 5223  dftr4 5229
[Enderton] p. 72Theorem 4Eunisuc 6421  unisucg 6420
[Enderton] p. 73Exercise 6unisuc 6421  unisucg 6420
[Enderton] p. 73Exercise 5(a)truni 5238
[Enderton] p. 73Exercise 5(b)trint 5240  trintALT 44842
[Enderton] p. 79Theorem 4I(A1)nna0 8579
[Enderton] p. 79Theorem 4I(A2)nnasuc 8581  onasuc 8503
[Enderton] p. 79Definition of operation valuedf-ov 7397
[Enderton] p. 80Theorem 4J(A1)nnm0 8580
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8582  onmsuc 8504
[Enderton] p. 81Theorem 4K(1)nnaass 8597
[Enderton] p. 81Theorem 4K(2)nna0r 8584  nnacom 8592
[Enderton] p. 81Theorem 4K(3)nndi 8598
[Enderton] p. 81Theorem 4K(4)nnmass 8599
[Enderton] p. 81Theorem 4K(5)nnmcom 8601
[Enderton] p. 82Exercise 16nnm0r 8585  nnmsucr 8600
[Enderton] p. 88Exercise 23nnaordex 8613
[Enderton] p. 129Definitiondf-en 8923
[Enderton] p. 132Theorem 6B(b)canth 7348
[Enderton] p. 133Exercise 1xpomen 9986
[Enderton] p. 133Exercise 2qnnen 16188
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9184
[Enderton] p. 135Corollary 6Cphp3 9186
[Enderton] p. 136Corollary 6Enneneq 9183
[Enderton] p. 136Corollary 6D(a)pssinf 9221
[Enderton] p. 136Corollary 6D(b)ominf 9223
[Enderton] p. 137Lemma 6Fpssnn 9145
[Enderton] p. 138Corollary 6Gssfi 9150
[Enderton] p. 139Theorem 6H(c)mapen 9118
[Enderton] p. 142Theorem 6I(3)xpdjuen 10151
[Enderton] p. 142Theorem 6I(4)mapdjuen 10152
[Enderton] p. 143Theorem 6Jdju0en 10147  dju1en 10143
[Enderton] p. 144Exercise 13iunfi 9312  unifi 9313  unifi2 9314
[Enderton] p. 144Corollary 6Kundif2 4448  unfi 9148  unfi2 9277
[Enderton] p. 145Figure 38ffoss 7933
[Enderton] p. 145Definitiondf-dom 8924
[Enderton] p. 146Example 1domen 8939  domeng 8940
[Enderton] p. 146Example 3nndomo 9198  nnsdom 9625  nnsdomg 9264
[Enderton] p. 149Theorem 6L(a)djudom2 10155
[Enderton] p. 149Theorem 6L(c)mapdom1 9119  xpdom1 9048  xpdom1g 9046  xpdom2g 9045
[Enderton] p. 149Theorem 6L(d)mapdom2 9125
[Enderton] p. 151Theorem 6Mzorn 10478  zorng 10475
[Enderton] p. 151Theorem 6M(4)ac8 10463  dfac5 10100
[Enderton] p. 159Theorem 6Qunictb 10546
[Enderton] p. 164Exampleinfdif 10179
[Enderton] p. 168Definitiondf-po 5554
[Enderton] p. 192Theorem 7M(a)oneli 6456
[Enderton] p. 192Theorem 7M(b)ontr1 6387
[Enderton] p. 192Theorem 7M(c)onirri 6455
[Enderton] p. 193Corollary 7N(b)0elon 6395
[Enderton] p. 193Corollary 7N(c)onsuci 7822
[Enderton] p. 193Corollary 7N(d)ssonunii 7764
[Enderton] p. 194Remarkonprc 7761
[Enderton] p. 194Exercise 16suc11 6449
[Enderton] p. 197Definitiondf-card 9910
[Enderton] p. 197Theorem 7Pcarden 10522
[Enderton] p. 200Exercise 25tfis 7839
[Enderton] p. 202Lemma 7Tr1tr 9747
[Enderton] p. 202Definitiondf-r1 9735
[Enderton] p. 202Theorem 7Qr1val1 9757
[Enderton] p. 204Theorem 7V(b)rankval4 9838
[Enderton] p. 206Theorem 7X(b)en2lp 9577
[Enderton] p. 207Exercise 30rankpr 9828  rankprb 9822  rankpw 9814  rankpwi 9794  rankuniss 9837
[Enderton] p. 207Exercise 34opthreg 9589
[Enderton] p. 208Exercise 35suc11reg 9590
[Enderton] p. 212Definition of alephalephval3 10081
[Enderton] p. 213Theorem 8A(a)alephord2 10047
[Enderton] p. 213Theorem 8A(b)cardalephex 10061
[Enderton] p. 218Theorem Schema 8Eonfununi 8319
[Enderton] p. 222Definition of kardkarden 9866  kardex 9865
[Enderton] p. 238Theorem 8Roeoa 8572
[Enderton] p. 238Theorem 8Soeoe 8574
[Enderton] p. 240Exercise 25oarec 8537
[Enderton] p. 257Definition of cofinalitycflm 10221
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17609
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17555
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18518  mrieqv2d 17606  mrieqvd 17605
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17610
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17615  mreexexlem2d 17612
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18524  mreexfidimd 17617
[Frege1879] p. 11Statementdf3or2 43729
[Frege1879] p. 12Statementdf3an2 43730  dfxor4 43727  dfxor5 43728
[Frege1879] p. 26Axiom 1ax-frege1 43751
[Frege1879] p. 26Axiom 2ax-frege2 43752
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43756
[Frege1879] p. 31Proposition 4frege4 43760
[Frege1879] p. 32Proposition 5frege5 43761
[Frege1879] p. 33Proposition 6frege6 43767
[Frege1879] p. 34Proposition 7frege7 43769
[Frege1879] p. 35Axiom 8ax-frege8 43770  axfrege8 43768
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37430
[Frege1879] p. 35Proposition 9frege9 43773
[Frege1879] p. 36Proposition 10frege10 43781
[Frege1879] p. 36Proposition 11frege11 43775
[Frege1879] p. 37Proposition 12frege12 43774
[Frege1879] p. 37Proposition 13frege13 43783
[Frege1879] p. 37Proposition 14frege14 43784
[Frege1879] p. 38Proposition 15frege15 43787
[Frege1879] p. 38Proposition 16frege16 43777
[Frege1879] p. 39Proposition 17frege17 43782
[Frege1879] p. 39Proposition 18frege18 43779
[Frege1879] p. 39Proposition 19frege19 43785
[Frege1879] p. 40Proposition 20frege20 43789
[Frege1879] p. 40Proposition 21frege21 43788
[Frege1879] p. 41Proposition 22frege22 43780
[Frege1879] p. 42Proposition 23frege23 43786
[Frege1879] p. 42Proposition 24frege24 43776
[Frege1879] p. 42Proposition 25frege25 43778  rp-frege25 43766
[Frege1879] p. 42Proposition 26frege26 43771
[Frege1879] p. 43Axiom 28ax-frege28 43791
[Frege1879] p. 43Proposition 27frege27 43772
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43792
[Frege1879] p. 44Axiom 31ax-frege31 43795  axfrege31 43794
[Frege1879] p. 44Proposition 30frege30 43793
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43796
[Frege1879] p. 44Proposition 33frege33 43797
[Frege1879] p. 45Proposition 34frege34 43798
[Frege1879] p. 45Proposition 35frege35 43799
[Frege1879] p. 45Proposition 36frege36 43800
[Frege1879] p. 46Proposition 37frege37 43801
[Frege1879] p. 46Proposition 38frege38 43802
[Frege1879] p. 46Proposition 39frege39 43803
[Frege1879] p. 46Proposition 40frege40 43804
[Frege1879] p. 47Axiom 41ax-frege41 43806  axfrege41 43805
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43807
[Frege1879] p. 47Proposition 43frege43 43808
[Frege1879] p. 47Proposition 44frege44 43809
[Frege1879] p. 47Proposition 45frege45 43810
[Frege1879] p. 48Proposition 46frege46 43811
[Frege1879] p. 48Proposition 47frege47 43812
[Frege1879] p. 49Proposition 48frege48 43813
[Frege1879] p. 49Proposition 49frege49 43814
[Frege1879] p. 49Proposition 50frege50 43815
[Frege1879] p. 50Axiom 52ax-frege52a 43818  ax-frege52c 43849  frege52aid 43819  frege52b 43850
[Frege1879] p. 50Axiom 54ax-frege54a 43823  ax-frege54c 43853  frege54b 43854
[Frege1879] p. 50Proposition 51frege51 43816
[Frege1879] p. 50Proposition 52dfsbcq 3763
[Frege1879] p. 50Proposition 53frege53a 43821  frege53aid 43820  frege53b 43851  frege53c 43875
[Frege1879] p. 50Proposition 54biid 261  eqid 2730
[Frege1879] p. 50Proposition 55frege55a 43829  frege55aid 43826  frege55b 43858  frege55c 43879  frege55cor1a 43830  frege55lem2a 43828  frege55lem2b 43857  frege55lem2c 43878
[Frege1879] p. 50Proposition 56frege56a 43832  frege56aid 43831  frege56b 43859  frege56c 43880
[Frege1879] p. 51Axiom 58ax-frege58a 43836  ax-frege58b 43862  frege58bid 43863  frege58c 43882
[Frege1879] p. 51Proposition 57frege57a 43834  frege57aid 43833  frege57b 43860  frege57c 43881
[Frege1879] p. 51Proposition 58spsbc 3774
[Frege1879] p. 51Proposition 59frege59a 43838  frege59b 43865  frege59c 43883
[Frege1879] p. 52Proposition 60frege60a 43839  frege60b 43866  frege60c 43884
[Frege1879] p. 52Proposition 61frege61a 43840  frege61b 43867  frege61c 43885
[Frege1879] p. 52Proposition 62frege62a 43841  frege62b 43868  frege62c 43886
[Frege1879] p. 52Proposition 63frege63a 43842  frege63b 43869  frege63c 43887
[Frege1879] p. 53Proposition 64frege64a 43843  frege64b 43870  frege64c 43888
[Frege1879] p. 53Proposition 65frege65a 43844  frege65b 43871  frege65c 43889
[Frege1879] p. 54Proposition 66frege66a 43845  frege66b 43872  frege66c 43890
[Frege1879] p. 54Proposition 67frege67a 43846  frege67b 43873  frege67c 43891
[Frege1879] p. 54Proposition 68frege68a 43847  frege68b 43874  frege68c 43892
[Frege1879] p. 55Definition 69dffrege69 43893
[Frege1879] p. 58Proposition 70frege70 43894
[Frege1879] p. 59Proposition 71frege71 43895
[Frege1879] p. 59Proposition 72frege72 43896
[Frege1879] p. 59Proposition 73frege73 43897
[Frege1879] p. 60Definition 76dffrege76 43900
[Frege1879] p. 60Proposition 74frege74 43898
[Frege1879] p. 60Proposition 75frege75 43899
[Frege1879] p. 62Proposition 77frege77 43901  frege77d 43707
[Frege1879] p. 63Proposition 78frege78 43902
[Frege1879] p. 63Proposition 79frege79 43903
[Frege1879] p. 63Proposition 80frege80 43904
[Frege1879] p. 63Proposition 81frege81 43905  frege81d 43708
[Frege1879] p. 64Proposition 82frege82 43906
[Frege1879] p. 65Proposition 83frege83 43907  frege83d 43709
[Frege1879] p. 65Proposition 84frege84 43908
[Frege1879] p. 66Proposition 85frege85 43909
[Frege1879] p. 66Proposition 86frege86 43910
[Frege1879] p. 66Proposition 87frege87 43911  frege87d 43711
[Frege1879] p. 67Proposition 88frege88 43912
[Frege1879] p. 68Proposition 89frege89 43913
[Frege1879] p. 68Proposition 90frege90 43914
[Frege1879] p. 68Proposition 91frege91 43915  frege91d 43712
[Frege1879] p. 69Proposition 92frege92 43916
[Frege1879] p. 70Proposition 93frege93 43917
[Frege1879] p. 70Proposition 94frege94 43918
[Frege1879] p. 70Proposition 95frege95 43919
[Frege1879] p. 71Definition 99dffrege99 43923
[Frege1879] p. 71Proposition 96frege96 43920  frege96d 43710
[Frege1879] p. 71Proposition 97frege97 43921  frege97d 43713
[Frege1879] p. 71Proposition 98frege98 43922  frege98d 43714
[Frege1879] p. 72Proposition 100frege100 43924
[Frege1879] p. 72Proposition 101frege101 43925
[Frege1879] p. 72Proposition 102frege102 43926  frege102d 43715
[Frege1879] p. 73Proposition 103frege103 43927
[Frege1879] p. 73Proposition 104frege104 43928
[Frege1879] p. 73Proposition 105frege105 43929
[Frege1879] p. 73Proposition 106frege106 43930  frege106d 43716
[Frege1879] p. 74Proposition 107frege107 43931
[Frege1879] p. 74Proposition 108frege108 43932  frege108d 43717
[Frege1879] p. 74Proposition 109frege109 43933  frege109d 43718
[Frege1879] p. 75Proposition 110frege110 43934
[Frege1879] p. 75Proposition 111frege111 43935  frege111d 43720
[Frege1879] p. 76Proposition 112frege112 43936
[Frege1879] p. 76Proposition 113frege113 43937
[Frege1879] p. 76Proposition 114frege114 43938  frege114d 43719
[Frege1879] p. 77Definition 115dffrege115 43939
[Frege1879] p. 77Proposition 116frege116 43940
[Frege1879] p. 78Proposition 117frege117 43941
[Frege1879] p. 78Proposition 118frege118 43942
[Frege1879] p. 78Proposition 119frege119 43943
[Frege1879] p. 78Proposition 120frege120 43944
[Frege1879] p. 79Proposition 121frege121 43945
[Frege1879] p. 79Proposition 122frege122 43946  frege122d 43721
[Frege1879] p. 79Proposition 123frege123 43947
[Frege1879] p. 80Proposition 124frege124 43948  frege124d 43722
[Frege1879] p. 81Proposition 125frege125 43949
[Frege1879] p. 81Proposition 126frege126 43950  frege126d 43723
[Frege1879] p. 82Proposition 127frege127 43951
[Frege1879] p. 83Proposition 128frege128 43952
[Frege1879] p. 83Proposition 129frege129 43953  frege129d 43724
[Frege1879] p. 84Proposition 130frege130 43954
[Frege1879] p. 85Proposition 131frege131 43955  frege131d 43725
[Frege1879] p. 86Proposition 132frege132 43956
[Frege1879] p. 86Proposition 133frege133 43957  frege133d 43726
[Fremlin1] p. 13Definition 111G (b)df-salgen 46284
[Fremlin1] p. 13Definition 111G (d)borelmbl 46607
[Fremlin1] p. 13Proposition 111G (b)salgenss 46307
[Fremlin1] p. 14Definition 112Aismea 46422
[Fremlin1] p. 15Remark 112B (d)psmeasure 46442
[Fremlin1] p. 15Property 112C (a)meadjun 46433  meadjunre 46447
[Fremlin1] p. 15Property 112C (b)meassle 46434
[Fremlin1] p. 15Property 112C (c)meaunle 46435
[Fremlin1] p. 16Property 112C (d)iundjiun 46431  meaiunle 46440  meaiunlelem 46439
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46452  meaiuninc2 46453  meaiuninc3 46456  meaiuninc3v 46455  meaiunincf 46454  meaiuninclem 46451
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46458  meaiininc2 46459  meaiininclem 46457
[Fremlin1] p. 19Theorem 113Ccaragen0 46477  caragendifcl 46485  caratheodory 46499  omelesplit 46489
[Fremlin1] p. 19Definition 113Aisome 46465  isomennd 46502  isomenndlem 46501
[Fremlin1] p. 19Remark 113B (c)omeunle 46487
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46506  voncmpl 46592
[Fremlin1] p. 19Definition 113A (ii)omessle 46469
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46494  carageniuncllem1 46492  carageniuncllem2 46493  caragenuncl 46484  caragenuncllem 46483  caragenunicl 46495
[Fremlin1] p. 21Remark 113Dcaragenel2d 46503
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46497  caratheodorylem2 46498
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46506
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46565  hoidmv1lelem1 46562  hoidmv1lelem2 46563  hoidmv1lelem3 46564
[Fremlin1] p. 25Definition 114Eisvonmbl 46609
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46565  hoidmvle 46571  hoidmvlelem1 46566  hoidmvlelem2 46567  hoidmvlelem3 46568  hoidmvlelem4 46569  hoidmvlelem5 46570  hsphoidmvle2 46556  hsphoif 46547  hsphoival 46550
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46519
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46527
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46554  hoidmvn0val 46555  hoidmvval 46548  hoidmvval0 46558  hoidmvval0b 46561
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46559  hsphoidmvle 46557
[Fremlin1] p. 30Definition 115Cdf-ovoln 46508  df-voln 46510
[Fremlin1] p. 30Proposition 115D (a)dmovn 46575  ovn0 46537  ovn0lem 46536  ovnf 46534  ovnome 46544  ovnssle 46532  ovnsslelem 46531  ovnsupge0 46528
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46574  ovnhoilem1 46572  ovnhoilem2 46573  vonhoi 46638
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46591  hoidifhspf 46589  hoidifhspval 46579  hoidifhspval2 46586  hoidifhspval3 46590  hspmbl 46600  hspmbllem1 46597  hspmbllem2 46598  hspmbllem3 46599
[Fremlin1] p. 31Definition 115Evoncmpl 46592  vonmea 46545
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46543  ovnsubadd2 46617  ovnsubadd2lem 46616  ovnsubaddlem1 46541  ovnsubaddlem2 46542
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46602  hoimbl2 46636  hoimbllem 46601  hspdifhsp 46587  opnvonmbl 46605  opnvonmbllem2 46604
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46607
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46650  iccvonmbllem 46649  ioovonmbl 46648
[Fremlin1] p. 32Proposition 115G (d)vonicc 46656  vonicclem2 46655  vonioo 46653  vonioolem2 46652  vonn0icc 46659  vonn0icc2 46663  vonn0ioo 46658  vonn0ioo2 46661
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46660  snvonmbl 46657  vonct 46664  vonsn 46662
[Fremlin1] p. 35Lemma 121Asubsalsal 46330
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46329  subsaliuncllem 46328
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46696  salpreimalegt 46680  salpreimaltle 46697
[Fremlin1] p. 35Proposition 121B (i)issmf 46699  issmff 46705  issmflem 46698
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46716  issmflelem 46715  smfpreimale 46725
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46727  issmfgtlem 46726
[Fremlin1] p. 36Definition 121Cdf-smblfn 46667  issmf 46699  issmff 46705  issmfge 46741  issmfgelem 46740  issmfgt 46727  issmfgtlem 46726  issmfle 46716  issmflelem 46715  issmflem 46698
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46678  salpreimagtlt 46701  salpreimalelt 46700
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46741  issmfgelem 46740
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46724
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46722  cnfsmf 46711
[Fremlin1] p. 36Proposition 121D (c)decsmf 46738  decsmflem 46737  incsmf 46713  incsmflem 46712
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46672  pimconstlt1 46673  smfconst 46720
[Fremlin1] p. 37Proposition 121E (b)smfadd 46736  smfaddlem1 46734  smfaddlem2 46735
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46767
[Fremlin1] p. 37Proposition 121E (d)smfmul 46766  smfmullem1 46762  smfmullem2 46763  smfmullem3 46764  smfmullem4 46765
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46768
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46771  smfpimbor1lem2 46770
[Fremlin1] p. 37Proposition 121E (g)smfco 46773
[Fremlin1] p. 37Proposition 121E (h)smfres 46761
[Fremlin1] p. 38Proposition 121E (e)smfrec 46760
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46769  smfresal 46759
[Fremlin1] p. 38Proposition 121F (a)smflim 46748  smflim2 46777  smflimlem1 46742  smflimlem2 46743  smflimlem3 46744  smflimlem4 46745  smflimlem5 46746  smflimlem6 46747  smflimmpt 46781
[Fremlin1] p. 38Proposition 121F (b)smfsup 46785  smfsuplem1 46782  smfsuplem2 46783  smfsuplem3 46784  smfsupmpt 46786  smfsupxr 46787
[Fremlin1] p. 38Proposition 121F (c)smfinf 46789  smfinflem 46788  smfinfmpt 46790
[Fremlin1] p. 39Remark 121Gsmflim 46748  smflim2 46777  smflimmpt 46781
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46779
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46809  smfdivdmmbl2 46812  smfinfdmmbl 46820  smfinfdmmbllem 46819  smfsupdmmbl 46816  smfsupdmmbllem 46815
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46799  smflimsuplem2 46792  smflimsuplem6 46796  smflimsuplem7 46797  smflimsuplem8 46798  smflimsupmpt 46800
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46802  smfliminflem 46801  smfliminfmpt 46803
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46667
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46813  fsupdm2 46814
[Fremlin1], p. 39Proposition 121Hadddmmbl 46804  adddmmbl2 46805  finfdm 46817  finfdm2 46818  fsupdm 46813  fsupdm2 46814  muldmmbl 46806  muldmmbl2 46807
[Fremlin1], p. 39Proposition 121F (c)finfdm 46817  finfdm2 46818
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25444
[Fremlin5] p. 213Lemma 565Cauniioovol 25487
[Fremlin5] p. 214Lemma 565Cauniioombl 25497
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37689
[Fremlin5] p. 220Theorem 565Maftc1anc 37692
[FreydScedrov] p. 283Axiom of Infinityax-inf 9609  inf1 9593  inf2 9594
[Gleason] p. 117Proposition 9-2.1df-enq 10882  enqer 10892
[Gleason] p. 117Proposition 9-2.2df-1nq 10887  df-nq 10883
[Gleason] p. 117Proposition 9-2.3df-plpq 10879  df-plq 10885
[Gleason] p. 119Proposition 9-2.4caovmo 7633  df-mpq 10880  df-mq 10886
[Gleason] p. 119Proposition 9-2.5df-rq 10888
[Gleason] p. 119Proposition 9-2.6ltexnq 10946
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10947  ltbtwnnq 10949
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10942
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10943
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10950
[Gleason] p. 121Definition 9-3.1df-np 10952
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10964
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10966
[Gleason] p. 122Definitiondf-1p 10953
[Gleason] p. 122Remark (1)prub 10965
[Gleason] p. 122Lemma 9-3.4prlem934 11004
[Gleason] p. 122Proposition 9-3.2df-ltp 10956
[Gleason] p. 122Proposition 9-3.3ltsopr 11003  psslinpr 11002  supexpr 11025  suplem1pr 11023  suplem2pr 11024
[Gleason] p. 123Proposition 9-3.5addclpr 10989  addclprlem1 10987  addclprlem2 10988  df-plp 10954
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10993
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10992
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11005
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11014  ltexprlem1 11007  ltexprlem2 11008  ltexprlem3 11009  ltexprlem4 11010  ltexprlem5 11011  ltexprlem6 11012  ltexprlem7 11013
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11016  ltaprlem 11015
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11017
[Gleason] p. 124Lemma 9-3.6prlem936 11018
[Gleason] p. 124Proposition 9-3.7df-mp 10955  mulclpr 10991  mulclprlem 10990  reclem2pr 11019
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11000
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10995
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10994
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10999
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11022  reclem3pr 11020  reclem4pr 11021
[Gleason] p. 126Proposition 9-4.1df-enr 11026  enrer 11034
[Gleason] p. 126Proposition 9-4.2df-0r 11031  df-1r 11032  df-nr 11027
[Gleason] p. 126Proposition 9-4.3df-mr 11029  df-plr 11028  negexsr 11073  recexsr 11078  recexsrlem 11074
[Gleason] p. 127Proposition 9-4.4df-ltr 11030
[Gleason] p. 130Proposition 10-1.3creui 12192  creur 12191  cru 12189
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11159  axcnre 11135
[Gleason] p. 132Definition 10-3.1crim 15091  crimd 15208  crimi 15169  crre 15090  crred 15207  crrei 15168
[Gleason] p. 132Definition 10-3.2remim 15093  remimd 15174
[Gleason] p. 133Definition 10.36absval2 15260  absval2d 15421  absval2i 15373
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15117  cjaddd 15196  cjaddi 15164
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15118  cjmuld 15197  cjmuli 15165
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15116  cjcjd 15175  cjcji 15147
[Gleason] p. 133Proposition 10-3.4(f)cjre 15115  cjreb 15099  cjrebd 15178  cjrebi 15150  cjred 15202  rere 15098  rereb 15096  rerebd 15177  rerebi 15149  rered 15200
[Gleason] p. 133Proposition 10-3.4(h)addcj 15124  addcjd 15188  addcji 15159
[Gleason] p. 133Proposition 10-3.7(a)absval 15214
[Gleason] p. 133Proposition 10-3.7(b)abscj 15255  abscjd 15426  abscji 15377
[Gleason] p. 133Proposition 10-3.7(c)abs00 15265  abs00d 15422  abs00i 15374  absne0d 15423
[Gleason] p. 133Proposition 10-3.7(d)releabs 15297  releabsd 15427  releabsi 15378
[Gleason] p. 133Proposition 10-3.7(f)absmul 15270  absmuld 15430  absmuli 15380
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15258  sqabsaddi 15381
[Gleason] p. 133Proposition 10-3.7(h)abstri 15306  abstrid 15432  abstrii 15384
[Gleason] p. 134Definition 10-4.1df-exp 14037  exp0 14040  expp1 14043  expp1d 14122
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26595  cxpaddd 26633  expadd 14079  expaddd 14123  expaddz 14081
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26604  cxpmuld 26653  expmul 14082  expmuld 14124  expmulz 14083
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26601  mulcxpd 26644  mulexp 14076  mulexpd 14136  mulexpz 14077
[Gleason] p. 140Exercise 1znnen 16187
[Gleason] p. 141Definition 11-2.1fzval 13483
[Gleason] p. 168Proposition 12-2.1(a)climadd 15605  rlimadd 15616  rlimdiv 15619
[Gleason] p. 168Proposition 12-2.1(b)climsub 15607  rlimsub 15617
[Gleason] p. 168Proposition 12-2.1(c)climmul 15606  rlimmul 15618
[Gleason] p. 171Corollary 12-2.2climmulc2 15610
[Gleason] p. 172Corollary 12-2.5climrecl 15556
[Gleason] p. 172Proposition 12-2.4(c)climabs 15577  climcj 15578  climim 15580  climre 15579  rlimabs 15582  rlimcj 15583  rlimim 15585  rlimre 15584
[Gleason] p. 173Definition 12-3.1df-ltxr 11231  df-xr 11230  ltxr 13088
[Gleason] p. 175Definition 12-4.1df-limsup 15444  limsupval 15447
[Gleason] p. 180Theorem 12-5.1climsup 15643
[Gleason] p. 180Theorem 12-5.3caucvg 15652  caucvgb 15653  caucvgbf 45458  caucvgr 15649  climcau 15644
[Gleason] p. 182Exercise 3cvgcmp 15789
[Gleason] p. 182Exercise 4cvgrat 15856
[Gleason] p. 195Theorem 13-2.12abs1m 15311
[Gleason] p. 217Lemma 13-4.1btwnzge0 13802
[Gleason] p. 223Definition 14-1.1df-met 21264
[Gleason] p. 223Definition 14-1.1(a)met0 24237  xmet0 24236
[Gleason] p. 223Definition 14-1.1(b)metgt0 24253
[Gleason] p. 223Definition 14-1.1(c)metsym 24244
[Gleason] p. 223Definition 14-1.1(d)mettri 24246  mstri 24363  xmettri 24245  xmstri 24362
[Gleason] p. 225Definition 14-1.5xpsmet 24276
[Gleason] p. 230Proposition 14-2.6txlm 23541
[Gleason] p. 240Theorem 14-4.3metcnp4 25217
[Gleason] p. 240Proposition 14-4.2metcnp3 24434
[Gleason] p. 243Proposition 14-4.16addcn 24760  addcn2 15567  mulcn 24762  mulcn2 15569  subcn 24761  subcn2 15568
[Gleason] p. 295Remarkbcval3 14281  bcval4 14282
[Gleason] p. 295Equation 2bcpasc 14296
[Gleason] p. 295Definition of binomial coefficientbcval 14279  df-bc 14278
[Gleason] p. 296Remarkbcn0 14285  bcnn 14287
[Gleason] p. 296Theorem 15-2.8binom 15803
[Gleason] p. 308Equation 2ef0 16064
[Gleason] p. 308Equation 3efcj 16065
[Gleason] p. 309Corollary 15-4.3efne0 16071
[Gleason] p. 309Corollary 15-4.4efexp 16076
[Gleason] p. 310Equation 14sinadd 16139
[Gleason] p. 310Equation 15cosadd 16140
[Gleason] p. 311Equation 17sincossq 16151
[Gleason] p. 311Equation 18cosbnd 16156  sinbnd 16155
[Gleason] p. 311Lemma 15-4.7sqeqor 14191  sqeqori 14189
[Gleason] p. 311Definition of ` `df-pi 16045
[Godowski] p. 730Equation SFgoeqi 32209
[GodowskiGreechie] p. 249Equation IV3oai 31604
[Golan] p. 1Remarksrgisid 20124
[Golan] p. 1Definitiondf-srg 20102
[Golan] p. 149Definitiondf-slmd 33162
[Gonshor] p. 7Definitiondf-scut 27702
[Gonshor] p. 9Theorem 2.5slerec 27738
[Gonshor] p. 10Theorem 2.6cofcut1 27835  cofcut1d 27836
[Gonshor] p. 10Theorem 2.7cofcut2 27837  cofcut2d 27838
[Gonshor] p. 12Theorem 2.9cofcutr 27839  cofcutr1d 27840  cofcutr2d 27841
[Gonshor] p. 13Definitiondf-adds 27874
[Gonshor] p. 14Theorem 3.1addsprop 27890
[Gonshor] p. 15Theorem 3.2addsunif 27916
[Gonshor] p. 17Theorem 3.4mulsprop 28040
[Gonshor] p. 18Theorem 3.5mulsunif 28060
[Gonshor] p. 28Lemma 4.2halfcut 28340
[Gonshor] p. 28Theorem 4.2pw2cut 28342
[Gonshor] p. 30Theorem 4.2addhalfcut 28341
[Gonshor] p. 95Theorem 6.1addsbday 27931
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36144
[Gratzer] p. 23Section 0.6df-mre 17553
[Gratzer] p. 27Section 0.6df-mri 17555
[Hall] p. 1Section 1.1df-asslaw 48105  df-cllaw 48103  df-comlaw 48104
[Hall] p. 2Section 1.2df-clintop 48117
[Hall] p. 7Section 1.3df-sgrp2 48138
[Halmos] p. 28Partition ` `df-parts 38750  dfmembpart2 38755
[Halmos] p. 31Theorem 17.3riesz1 32001  riesz2 32002
[Halmos] p. 41Definition of Hermitianhmopadj2 31877
[Halmos] p. 42Definition of projector orderingpjordi 32109
[Halmos] p. 43Theorem 26.1elpjhmop 32121  elpjidm 32120  pjnmopi 32084
[Halmos] p. 44Remarkpjinormi 31623  pjinormii 31612
[Halmos] p. 44Theorem 26.2elpjch 32125  pjrn 31643  pjrni 31638  pjvec 31632
[Halmos] p. 44Theorem 26.3pjnorm2 31663
[Halmos] p. 44Theorem 26.4hmopidmpj 32090  hmopidmpji 32088
[Halmos] p. 45Theorem 27.1pjinvari 32127
[Halmos] p. 45Theorem 27.3pjoci 32116  pjocvec 31633
[Halmos] p. 45Theorem 27.4pjorthcoi 32105
[Halmos] p. 48Theorem 29.2pjssposi 32108
[Halmos] p. 48Theorem 29.3pjssdif1i 32111  pjssdif2i 32110
[Halmos] p. 50Definition of spectrumdf-spec 31791
[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 1795
[Hatcher] p. 25Definitiondf-phtpc 24897  df-phtpy 24876
[Hatcher] p. 26Definitiondf-pco 24911  df-pi1 24914
[Hatcher] p. 26Proposition 1.2phtpcer 24900
[Hatcher] p. 26Proposition 1.3pi1grp 24956
[Hefferon] p. 240Definition 3.12df-dmat 22383  df-dmatalt 48316
[Helfgott] p. 2Theoremtgoldbach 47773
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47758
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47770  bgoldbtbnd 47765  bgoldbtbnd 47765  tgblthelfgott 47771
[Helfgott] p. 5Proposition 1.1circlevma 34641
[Helfgott] p. 69Statement 7.49circlemethhgt 34642
[Helfgott] p. 69Statement 7.50hgt750lema 34656  hgt750lemb 34655  hgt750leme 34657  hgt750lemf 34652  hgt750lemg 34653
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47767  tgoldbachgt 34662  tgoldbachgtALTV 47768  tgoldbachgtd 34661
[Helfgott] p. 70Statement 7.49ax-hgt749 34643
[Herstein] p. 54Exercise 28df-grpo 30429
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18882  grpoideu 30445  mndideu 18678
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18912  grpoinveu 30455
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18943  grpo2inv 30467
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18956  grpoinvop 30469
[Herstein] p. 57Exercise 1dfgrp3e 18978
[Hitchcock] p. 5Rule A3mptnan 1768
[Hitchcock] p. 5Rule A4mptxor 1769
[Hitchcock] p. 5Rule A5mtpxor 1771
[Holland] p. 1519Theorem 2sumdmdi 32356
[Holland] p. 1520Lemma 5cdj1i 32369  cdj3i 32377  cdj3lem1 32370  cdjreui 32368
[Holland] p. 1524Lemma 7mddmdin0i 32367
[Holland95] p. 13Theorem 3.6hlathil 41947
[Holland95] p. 14Line 15hgmapvs 41877
[Holland95] p. 14Line 16hdmaplkr 41899
[Holland95] p. 14Line 17hdmapellkr 41900
[Holland95] p. 14Line 19hdmapglnm2 41897
[Holland95] p. 14Line 20hdmapip0com 41903
[Holland95] p. 14Theorem 3.6hdmapevec2 41822
[Holland95] p. 14Lines 24 and 25hdmapoc 41917
[Holland95] p. 204Definition of involutiondf-srng 20755
[Holland95] p. 212Definition of subspacedf-psubsp 39489
[Holland95] p. 214Lemma 3.3lclkrlem2v 41514
[Holland95] p. 214Definition 3.2df-lpolN 41467
[Holland95] p. 214Definition of nonsingularpnonsingN 39919
[Holland95] p. 215Lemma 3.3(1)dihoml4 41363  poml4N 39939
[Holland95] p. 215Lemma 3.3(2)dochexmid 41454  pexmidALTN 39964  pexmidN 39955
[Holland95] p. 218Theorem 3.6lclkr 41519
[Holland95] p. 218Definition of dual vector spacedf-ldual 39109  ldualset 39110
[Holland95] p. 222Item 1df-lines 39487  df-pointsN 39488
[Holland95] p. 222Item 2df-polarityN 39889
[Holland95] p. 223Remarkispsubcl2N 39933  omllaw4 39231  pol1N 39896  polcon3N 39903
[Holland95] p. 223Definitiondf-psubclN 39921
[Holland95] p. 223Equation for polaritypolval2N 39892
[Holmes] p. 40Definitiondf-xrn 38356
[Hughes] p. 44Equation 1.21bax-his3 31020
[Hughes] p. 47Definition of projection operatordfpjop 32118
[Hughes] p. 49Equation 1.30eighmre 31899  eigre 31771  eigrei 31770
[Hughes] p. 49Equation 1.31eighmorth 31900  eigorth 31774  eigorthi 31773
[Hughes] p. 137Remark (ii)eigposi 31772
[Huneke] p. 1Claim 1frgrncvvdeq 30245
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30241
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30242
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30243
[Huneke] p. 2Claim 2frgrregorufr 30261  frgrregorufr0 30260  frgrregorufrg 30262
[Huneke] p. 2Claim 3frgrhash2wsp 30268  frrusgrord 30277  frrusgrord0 30276
[Huneke] p. 2Statementdf-clwwlknon 30024
[Huneke] p. 2Statement 4frgrwopreglem4 30251
[Huneke] p. 2Statement 5frgrwopreg1 30254  frgrwopreg2 30255  frgrwopregasn 30252  frgrwopregbsn 30253
[Huneke] p. 2Statement 6frgrwopreglem5 30257
[Huneke] p. 2Statement 7fusgreghash2wspv 30271
[Huneke] p. 2Statement 8fusgreghash2wsp 30274
[Huneke] p. 2Statement 9clwlksndivn 30022  numclwlk1 30307  numclwlk1lem1 30305  numclwlk1lem2 30306  numclwwlk1 30297  numclwwlk8 30328
[Huneke] p. 2Definition 3frgrwopreglem1 30248
[Huneke] p. 2Definition 4df-clwlks 29708
[Huneke] p. 2Definition 62clwwlk 30283
[Huneke] p. 2Definition 7numclwwlkovh 30309  numclwwlkovh0 30308
[Huneke] p. 2Statement 10numclwwlk2 30317
[Huneke] p. 2Statement 11rusgrnumwlkg 29914
[Huneke] p. 2Statement 12numclwwlk3 30321
[Huneke] p. 2Statement 13numclwwlk5 30324
[Huneke] p. 2Statement 14numclwwlk7 30327
[Indrzejczak] p. 33Definition ` `Enatded 30339  natded 30339
[Indrzejczak] p. 33Definition ` `Inatded 30339
[Indrzejczak] p. 34Definition ` `Enatded 30339  natded 30339
[Indrzejczak] p. 34Definition ` `Inatded 30339
[Jech] p. 4Definition of classcv 1539  cvjust 2724
[Jech] p. 42Lemma 6.1alephexp1 10550
[Jech] p. 42Equation 6.1alephadd 10548  alephmul 10549
[Jech] p. 43Lemma 6.2infmap 10547  infmap2 10188
[Jech] p. 71Lemma 9.3jech9.3 9785
[Jech] p. 72Equation 9.3scott0 9857  scottex 9856
[Jech] p. 72Exercise 9.1rankval4 9838
[Jech] p. 72Scheme "Collection Principle"cp 9862
[Jech] p. 78Noteopthprc 5710
[JonesMatijasevic] p. 694Definition 2.3rmxyval 42876
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 42964
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 42965
[JonesMatijasevic] p. 695Equation 2.7rmxadd 42888
[JonesMatijasevic] p. 695Equation 2.8rmyadd 42892
[JonesMatijasevic] p. 695Equation 2.9rmxp1 42893  rmyp1 42894
[JonesMatijasevic] p. 695Equation 2.10rmxm1 42895  rmym1 42896
[JonesMatijasevic] p. 695Equation 2.11rmx0 42886  rmx1 42887  rmxluc 42897
[JonesMatijasevic] p. 695Equation 2.12rmy0 42890  rmy1 42891  rmyluc 42898
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 42900
[JonesMatijasevic] p. 695Equation 2.14rmydbl 42901
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42921  jm2.17b 42922  jm2.17c 42923
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 42954
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 42958
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 42949
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42924  jm2.24nn 42920
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 42963
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 42969  rmygeid 42925
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 42981
[Juillerat] p. 11Section *5etransc 46254  etransclem47 46252  etransclem48 46253
[Juillerat] p. 12Equation (7)etransclem44 46249
[Juillerat] p. 12Equation *(7)etransclem46 46251
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46237
[Juillerat] p. 13Proofetransclem35 46240
[Juillerat] p. 13Part of case 2 proven inetransclem38 46243
[Juillerat] p. 13Part of case 2 provenetransclem24 46229
[Juillerat] p. 13Part of case 2: proven inetransclem41 46246
[Juillerat] p. 14Proofetransclem23 46228
[KalishMontague] p. 81Note 1ax-6 1967
[KalishMontague] p. 85Lemma 2equid 2012
[KalishMontague] p. 85Lemma 3equcomi 2017
[KalishMontague] p. 86Lemma 7cbvalivw 2007  cbvaliw 2006  wl-cbvmotv 37498  wl-motae 37500  wl-moteq 37499
[KalishMontague] p. 87Lemma 8spimvw 1986  spimw 1970
[KalishMontague] p. 87Lemma 9spfw 2033  spw 2034
[Kalmbach] p. 14Definition of latticechabs1 31452  chabs1i 31454  chabs2 31453  chabs2i 31455  chjass 31469  chjassi 31422  latabs1 18440  latabs2 18441
[Kalmbach] p. 15Definition of atomdf-at 32274  ela 32275
[Kalmbach] p. 15Definition of coverscvbr2 32219  cvrval2 39259
[Kalmbach] p. 16Definitiondf-ol 39163  df-oml 39164
[Kalmbach] p. 20Definition of commutescmbr 31520  cmbri 31526  cmtvalN 39196  df-cm 31519  df-cmtN 39162
[Kalmbach] p. 22Remarkomllaw5N 39232  pjoml5 31549  pjoml5i 31524
[Kalmbach] p. 22Definitionpjoml2 31547  pjoml2i 31521
[Kalmbach] p. 22Theorem 2(v)cmcm 31550  cmcmi 31528  cmcmii 31533  cmtcomN 39234
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39230  omlsi 31340  pjoml 31372  pjomli 31371
[Kalmbach] p. 22Definition of OML lawomllaw2N 39229
[Kalmbach] p. 23Remarkcmbr2i 31532  cmcm3 31551  cmcm3i 31530  cmcm3ii 31535  cmcm4i 31531  cmt3N 39236  cmt4N 39237  cmtbr2N 39238
[Kalmbach] p. 23Lemma 3cmbr3 31544  cmbr3i 31536  cmtbr3N 39239
[Kalmbach] p. 25Theorem 5fh1 31554  fh1i 31557  fh2 31555  fh2i 31558  omlfh1N 39243
[Kalmbach] p. 65Remarkchjatom 32293  chslej 31434  chsleji 31394  shslej 31316  shsleji 31306
[Kalmbach] p. 65Proposition 1chocin 31431  chocini 31390  chsupcl 31276  chsupval2 31346  h0elch 31191  helch 31179  hsupval2 31345  ocin 31232  ococss 31229  shococss 31230
[Kalmbach] p. 65Definition of subspace sumshsval 31248
[Kalmbach] p. 66Remarkdf-pjh 31331  pjssmi 32101  pjssmii 31617
[Kalmbach] p. 67Lemma 3osum 31581  osumi 31578
[Kalmbach] p. 67Lemma 4pjci 32136
[Kalmbach] p. 103Exercise 6atmd2 32336
[Kalmbach] p. 103Exercise 12mdsl0 32246
[Kalmbach] p. 140Remarkhatomic 32296  hatomici 32295  hatomistici 32298
[Kalmbach] p. 140Proposition 1atlatmstc 39304
[Kalmbach] p. 140Proposition 1(i)atexch 32317  lsatexch 39028
[Kalmbach] p. 140Proposition 1(ii)chcv1 32291  cvlcvr1 39324  cvr1 39396
[Kalmbach] p. 140Proposition 1(iii)cvexch 32310  cvexchi 32305  cvrexch 39406
[Kalmbach] p. 149Remark 2chrelati 32300  hlrelat 39388  hlrelat5N 39387  lrelat 38999
[Kalmbach] p. 153Exercise 5lsmcv 21057  lsmsatcv 38995  spansncv 31589  spansncvi 31588
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39014  spansncv2 32229
[Kalmbach] p. 266Definitiondf-st 32147
[Kalmbach2] p. 8Definition of adjointdf-adjh 31785
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10617  fpwwe2 10614
[KanamoriPincus] p. 416Corollary 1.3canth4 10618
[KanamoriPincus] p. 417Corollary 1.6canthp1 10625
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10620
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10622
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10635
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10639  gchxpidm 10640
[KanamoriPincus] p. 419Theorem 2.1gchacg 10651  gchhar 10650
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10186  unxpwdom 9560
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10641
[Kreyszig] p. 3Property M1metcl 24226  xmetcl 24225
[Kreyszig] p. 4Property M2meteq0 24233
[Kreyszig] p. 8Definition 1.1-8dscmet 24466
[Kreyszig] p. 12Equation 5conjmul 11915  muleqadd 11838
[Kreyszig] p. 18Definition 1.3-2mopnval 24332
[Kreyszig] p. 19Remarkmopntopon 24333
[Kreyszig] p. 19Theorem T1mopn0 24392  mopnm 24338
[Kreyszig] p. 19Theorem T2unimopn 24390
[Kreyszig] p. 19Definition of neighborhoodneibl 24395
[Kreyszig] p. 20Definition 1.3-3metcnp2 24436
[Kreyszig] p. 25Definition 1.4-1lmbr 23151  lmmbr 25165  lmmbr2 25166
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23273
[Kreyszig] p. 28Theorem 1.4-5lmcau 25220
[Kreyszig] p. 28Definition 1.4-3iscau 25183  iscmet2 25201
[Kreyszig] p. 30Theorem 1.4-7cmetss 25223
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23354  metelcls 25212
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25213  metcld2 25214
[Kreyszig] p. 51Equation 2clmvneg1 25005  lmodvneg1 20817  nvinv 30575  vcm 30512
[Kreyszig] p. 51Equation 1aclm0vs 25001  lmod0vs 20807  slmd0vs 33185  vc0 30510
[Kreyszig] p. 51Equation 1blmodvs0 20808  slmdvs0 33186  vcz 30511
[Kreyszig] p. 58Definition 2.2-1imsmet 30627  ngpmet 24497  nrmmetd 24468
[Kreyszig] p. 59Equation 1imsdval 30622  imsdval2 30623  ncvspds 25068  ngpds 24498
[Kreyszig] p. 63Problem 1nmval 24483  nvnd 30624
[Kreyszig] p. 64Problem 2nmeq0 24512  nmge0 24511  nvge0 30609  nvz 30605
[Kreyszig] p. 64Problem 3nmrtri 24518  nvabs 30608
[Kreyszig] p. 91Definition 2.7-1isblo3i 30737
[Kreyszig] p. 92Equation 2df-nmoo 30681
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30743  blocni 30741
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30742
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25111  ipeq0 21553  ipz 30655
[Kreyszig] p. 135Problem 2cphpyth 25123  pythi 30786
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30790
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25145
[Kreyszig] p. 144Equation 4supcvg 15829
[Kreyszig] p. 144Theorem 3.3-1minvec 25343  minveco 30820
[Kreyszig] p. 196Definition 3.9-1df-aj 30686
[Kreyszig] p. 247Theorem 4.7-2bcth 25236
[Kreyszig] p. 249Theorem 4.7-3ubth 30809
[Kreyszig] p. 470Definition of positive operator orderingleop 32059  leopg 32058
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32077
[Kreyszig] p. 525Theorem 10.1-1htth 30854
[Kulpa] p. 547Theorempoimir 37644
[Kulpa] p. 547Equation (1)poimirlem32 37643
[Kulpa] p. 547Equation (2)poimirlem31 37642
[Kulpa] p. 548Theorembroucube 37645
[Kulpa] p. 548Equation (6)poimirlem26 37637
[Kulpa] p. 548Equation (7)poimirlem27 37638
[Kunen] p. 10Axiom 0ax6e 2382  axnul 5268
[Kunen] p. 11Axiom 3axnul 5268
[Kunen] p. 12Axiom 6zfrep6 7942
[Kunen] p. 24Definition 10.24mapval 8815  mapvalg 8813
[Kunen] p. 30Lemma 10.20fodomg 10493
[Kunen] p. 31Definition 10.24mapex 7926
[Kunen] p. 95Definition 2.1df-r1 9735
[Kunen] p. 97Lemma 2.10r1elss 9777  r1elssi 9776
[Kunen] p. 107Exercise 4rankop 9829  rankopb 9823  rankuni 9834  rankxplim 9850  rankxpsuc 9853
[Kunen2] p. 47Lemma I.9.9relpfr 44916
[Kunen2] p. 53Lemma I.9.21trfr 44924
[Kunen2] p. 53Lemma I.9.24(2)wffr 44923
[Kunen2] p. 53Definition I.9.20tcfr 44925
[Kunen2] p. 95Lemma I.16.2ralabso 44930  rexabso 44931
[Kunen2] p. 96Example I.16.3disjabso 44937  n0abso 44938  ssabso 44936
[Kunen2] p. 111Lemma II.2.4(1)traxext 44939
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 44949
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 44944
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 44947
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 44948
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 44943
[Kunen2] p. 112Corollary II.2.5wfaxext 44955  wfaxpr 44960  wfaxreg 44962  wfaxrep 44956  wfaxsep 44957  wfaxun 44961
[Kunen2] p. 113Lemma II.2.8pwclaxpow 44946
[Kunen2] p. 113Corollary II.2.9wfaxpow 44959
[Kunen2] p. 114Theorem II.2.13wfaxext 44955
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 44954  omelaxinf2 44951
[Kunen2] p. 114Corollary II.2.12wfac8prim 44964  wfaxinf2 44963
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 44977  permaxext 44967  permaxinf2 44975  permaxnul 44970  permaxpow 44971  permaxpr 44972  permaxrep 44968  permaxsep 44969  permaxun 44973
[Kunen2] p. 148Definition II.9.1brpermmodel 44965
[Kunen2] p. 149Exercise II.9.3permac8prim 44976
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4976
[Lang] , p. 225Corollary 1.3finexttrb 33668
[Lang] p. Definitiondf-rn 5657
[Lang] p. 3Statementlidrideqd 18602  mndbn0 18683
[Lang] p. 3Definitiondf-mnd 18668
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18620
[Lang] p. 4Property of composites. Second formulagsumccat 18774
[Lang] p. 5Equationgsumreidx 19853
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48099
[Lang] p. 6Examplenn0mnd 48096
[Lang] p. 6Equationgsumxp2 19916
[Lang] p. 6Statementcycsubm 19140
[Lang] p. 6Definitionmulgnn0gsum 19018
[Lang] p. 6Observationmndlsmidm 19606
[Lang] p. 7Definitiondfgrp2e 18901
[Lang] p. 30Definitiondf-tocyc 33072
[Lang] p. 32Property (a)cyc3genpm 33117
[Lang] p. 32Property (b)cyc3conja 33122  cycpmconjv 33107
[Lang] p. 53Definitiondf-cat 17635
[Lang] p. 53Axiom CAT 1cat1 18065  cat1lem 18064
[Lang] p. 54Definitiondf-iso 17717
[Lang] p. 57Definitiondf-inito 17952  df-termo 17953
[Lang] p. 58Exampleirinitoringc 21395
[Lang] p. 58Statementinitoeu1 17979  termoeu1 17986
[Lang] p. 62Definitiondf-func 17826
[Lang] p. 65Definitiondf-nat 17914
[Lang] p. 91Notedf-ringc 20561
[Lang] p. 92Statementmxidlprm 33449
[Lang] p. 92Definitionisprmidlc 33426
[Lang] p. 128Remarkdsmmlmod 21660
[Lang] p. 129Prooflincscm 48348  lincscmcl 48350  lincsum 48347  lincsumcl 48349
[Lang] p. 129Statementlincolss 48352
[Lang] p. 129Observationdsmmfi 21653
[Lang] p. 141Theorem 5.3dimkerim 33631  qusdimsum 33632
[Lang] p. 141Corollary 5.4lssdimle 33611
[Lang] p. 147Definitionsnlindsntor 48389
[Lang] p. 504Statementmat1 22340  matring 22336
[Lang] p. 504Definitiondf-mamu 22284
[Lang] p. 505Statementmamuass 22295  mamutpos 22351  matassa 22337  mattposvs 22348  tposmap 22350
[Lang] p. 513Definitionmdet1 22494  mdetf 22488
[Lang] p. 513Theorem 4.4cramer 22584
[Lang] p. 514Proposition 4.6mdetleib 22480
[Lang] p. 514Proposition 4.8mdettpos 22504
[Lang] p. 515Definitiondf-minmar1 22528  smadiadetr 22568
[Lang] p. 515Corollary 4.9mdetero 22503  mdetralt 22501
[Lang] p. 517Proposition 4.15mdetmul 22516
[Lang] p. 518Definitiondf-madu 22527
[Lang] p. 518Proposition 4.16madulid 22538  madurid 22537  matinv 22570
[Lang] p. 561Theorem 3.1cayleyhamilton 22783
[Lang], p. 224Proposition 1.2extdgmul 33667  fedgmul 33635
[Lang], p. 561Remarkchpmatply1 22725
[Lang], p. 561Definitiondf-chpmat 22720
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44295
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44290
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44296
[LeBlanc] p. 277Rule R2axnul 5268
[Levy] p. 12Axiom 4.3.1df-clab 2709
[Levy] p. 59Definitiondf-ttrcl 9679
[Levy] p. 64Theorem 5.6(ii)frinsg 9722
[Levy] p. 338Axiomdf-clel 2804  df-cleq 2722
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2804  df-cleq 2722
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2709
[Levy] p. 358Axiomdf-clab 2709
[Levy58] p. 2Definition Iisfin1-3 10357
[Levy58] p. 2Definition IIdf-fin2 10257
[Levy58] p. 2Definition Iadf-fin1a 10256
[Levy58] p. 2Definition IIIdf-fin3 10259
[Levy58] p. 3Definition Vdf-fin5 10260
[Levy58] p. 3Definition IVdf-fin4 10258
[Levy58] p. 4Definition VIdf-fin6 10261
[Levy58] p. 4Definition VIIdf-fin7 10262
[Levy58], p. 3Theorem 1fin1a2 10386
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27605
[Lipparini] p. 3Lemma 2.1.4noresle 27616
[Lipparini] p. 6Proposition 4.2noinfbnd1 27648  nosupbnd1 27633
[Lipparini] p. 6Proposition 4.3noinfbnd2 27650  nosupbnd2 27635
[Lipparini] p. 7Theorem 5.1noetasuplem3 27654  noetasuplem4 27655
[Lipparini] p. 7Corollary 4.4nosupinfsep 27651
[Lopez-Astorga] p. 12Rule 1mptnan 1768
[Lopez-Astorga] p. 12Rule 2mptxor 1769
[Lopez-Astorga] p. 12Rule 3mtpxor 1771
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32344
[Maeda] p. 168Lemma 5mdsym 32348  mdsymi 32347
[Maeda] p. 168Lemma 4(i)mdsymlem4 32342  mdsymlem6 32344  mdsymlem7 32345
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32346
[MaedaMaeda] p. 1Remarkssdmd1 32249  ssdmd2 32250  ssmd1 32247  ssmd2 32248
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32245
[MaedaMaeda] p. 1Definition 1.1df-dmd 32217  df-md 32216  mdbr 32230
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32267  mdslj1i 32255  mdslj2i 32256  mdslle1i 32253  mdslle2i 32254  mdslmd1i 32265  mdslmd2i 32266
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32257  mdsl2bi 32259  mdsl2i 32258
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32271
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32268
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32269
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32246
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32251  mdsl3 32252
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32270
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32365
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39306  hlrelat1 39386
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39024
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32272  cvmdi 32260  cvnbtwn4 32225  cvrnbtwn4 39264
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32273
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39325  cvp 32311  cvrp 39402  lcvp 39025
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32335
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32334
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39318  hlexch4N 39378
[MaedaMaeda] p. 34Exercise 7.1atabsi 32337
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39429
[MaedaMaeda] p. 61Definition 15.10psubN 39735  atpsubN 39739  df-pointsN 39488  pointpsubN 39737
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39490  pmap11 39748  pmaple 39747  pmapsub 39754  pmapval 39743
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39751  pmap1N 39753
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39756  pmapglb2N 39757  pmapglb2xN 39758  pmapglbx 39755
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39838
[MaedaMaeda] p. 67Postulate PS1ps-1 39463
[MaedaMaeda] p. 68Lemma 16.2df-padd 39782  paddclN 39828  paddidm 39827
[MaedaMaeda] p. 68Condition PS2ps-2 39464
[MaedaMaeda] p. 68Equation 16.2.1paddass 39824
[MaedaMaeda] p. 69Lemma 16.4ps-1 39463
[MaedaMaeda] p. 69Theorem 16.4ps-2 39464
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19611  lsmmod2 19612  lssats 38997  shatomici 32294  shatomistici 32297  shmodi 31326  shmodsi 31325
[MaedaMaeda] p. 130Remark 29.6dmdmd 32236  mdsymlem7 32345
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31525
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31429
[MaedaMaeda] p. 139Remarksumdmdii 32351
[Margaris] p. 40Rule Cexlimiv 1930
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 396  df-ex 1780  df-or 848  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30336
[Margaris] p. 59Section 14notnotrALTVD 44876
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 44877
[Margaris] p. 79Rule Cexinst01 44587  exinst11 44588
[Margaris] p. 89Theorem 19.219.2 1976  19.2g 2189  r19.2z 4466
[Margaris] p. 89Theorem 19.319.3 2203  rr19.3v 3642
[Margaris] p. 89Theorem 19.5alcom 2160
[Margaris] p. 89Theorem 19.6alex 1826
[Margaris] p. 89Theorem 19.7alnex 1781
[Margaris] p. 89Theorem 19.819.8a 2182
[Margaris] p. 89Theorem 19.919.9 2206  19.9h 2286  exlimd 2219  exlimdh 2290
[Margaris] p. 89Theorem 19.11excom 2163  excomim 2164
[Margaris] p. 89Theorem 19.1219.12 2326
[Margaris] p. 90Section 19conventions-labels 30337  conventions-labels 30337  conventions-labels 30337  conventions-labels 30337
[Margaris] p. 90Theorem 19.14exnal 1827
[Margaris] p. 90Theorem 19.152albi 44339  albi 1818
[Margaris] p. 90Theorem 19.1619.16 2226
[Margaris] p. 90Theorem 19.1719.17 2227
[Margaris] p. 90Theorem 19.182exbi 44341  exbi 1847
[Margaris] p. 90Theorem 19.1919.19 2230
[Margaris] p. 90Theorem 19.202alim 44338  2alimdv 1918  alimd 2213  alimdh 1817  alimdv 1916  ax-4 1809  ralimdaa 3240  ralimdv 3149  ralimdva 3147  ralimdvva 3186  sbcimdv 3830
[Margaris] p. 90Theorem 19.2119.21 2208  19.21h 2287  19.21t 2207  19.21vv 44337  alrimd 2216  alrimdd 2215  alrimdh 1863  alrimdv 1929  alrimi 2214  alrimih 1824  alrimiv 1927  alrimivv 1928  hbralrimi 3125  r19.21be 3232  r19.21bi 3231  ralrimd 3244  ralrimdv 3133  ralrimdva 3135  ralrimdvv 3183  ralrimdvva 3194  ralrimi 3237  ralrimia 3238  ralrimiv 3126  ralrimiva 3127  ralrimivv 3180  ralrimivva 3182  ralrimivvva 3185  ralrimivw 3131
[Margaris] p. 90Theorem 19.222exim 44340  2eximdv 1919  exim 1834  eximd 2217  eximdh 1864  eximdv 1917  rexim 3072  reximd2a 3249  reximdai 3241  reximdd 45114  reximddv 3151  reximddv2 3198  reximddv3 3152  reximdv 3150  reximdv2 3145  reximdva 3148  reximdvai 3146  reximdvva 3187  reximi2 3064
[Margaris] p. 90Theorem 19.2319.23 2212  19.23bi 2192  19.23h 2288  19.23t 2211  exlimdv 1933  exlimdvv 1934  exlimexi 44486  exlimiv 1930  exlimivv 1932  rexlimd3 45110  rexlimdv 3134  rexlimdv3a 3140  rexlimdva 3136  rexlimdva2 3138  rexlimdvaa 3137  rexlimdvv 3195  rexlimdvva 3196  rexlimdvvva 3197  rexlimdvw 3141  rexlimiv 3129  rexlimiva 3128  rexlimivv 3181
[Margaris] p. 90Theorem 19.2419.24 1991
[Margaris] p. 90Theorem 19.2519.25 1880
[Margaris] p. 90Theorem 19.2619.26 1870
[Margaris] p. 90Theorem 19.2719.27 2228  r19.27z 4476  r19.27zv 4477
[Margaris] p. 90Theorem 19.2819.28 2229  19.28vv 44347  r19.28z 4469  r19.28zf 45125  r19.28zv 4472  rr19.28v 3643
[Margaris] p. 90Theorem 19.2919.29 1873  r19.29d2r 3122  r19.29imd 3100
[Margaris] p. 90Theorem 19.3019.30 1881
[Margaris] p. 90Theorem 19.3119.31 2235  19.31vv 44345
[Margaris] p. 90Theorem 19.3219.32 2234  r19.32 47069
[Margaris] p. 90Theorem 19.3319.33-2 44343  19.33 1884
[Margaris] p. 90Theorem 19.3419.34 1992
[Margaris] p. 90Theorem 19.3519.35 1877
[Margaris] p. 90Theorem 19.3619.36 2231  19.36vv 44344  r19.36zv 4478
[Margaris] p. 90Theorem 19.3719.37 2233  19.37vv 44346  r19.37zv 4473
[Margaris] p. 90Theorem 19.3819.38 1839
[Margaris] p. 90Theorem 19.3919.39 1990
[Margaris] p. 90Theorem 19.4019.40-2 1887  19.40 1886  r19.40 3101
[Margaris] p. 90Theorem 19.4119.41 2236  19.41rg 44512
[Margaris] p. 90Theorem 19.4219.42 2237
[Margaris] p. 90Theorem 19.4319.43 1882
[Margaris] p. 90Theorem 19.4419.44 2238  r19.44zv 4475
[Margaris] p. 90Theorem 19.4519.45 2239  r19.45zv 4474
[Margaris] p. 110Exercise 2(b)eu1 2604
[Mayet] p. 370Remarkjpi 32206  largei 32203  stri 32193
[Mayet3] p. 9Definition of CH-statesdf-hst 32148  ishst 32150
[Mayet3] p. 10Theoremhstrbi 32202  hstri 32201
[Mayet3] p. 1223Theorem 4.1mayete3i 31664
[Mayet3] p. 1240Theorem 7.1mayetes3i 31665
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32214
[MegPav2000] p. 2345Definition 3.4-1chintcl 31268  chsupcl 31276
[MegPav2000] p. 2345Definition 3.4-2hatomic 32296
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32290
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32317
[MegPav2000] p. 2366Figure 7pl42N 39969
[MegPav2002] p. 362Lemma 2.2latj31 18452  latj32 18450  latjass 18448
[Megill] p. 444Axiom C5ax-5 1910  ax5ALT 38892
[Megill] p. 444Section 7conventions 30336
[Megill] p. 445Lemma L12aecom-o 38886  ax-c11n 38873  axc11n 2425
[Megill] p. 446Lemma L17equtrr 2022
[Megill] p. 446Lemma L18ax6fromc10 38881
[Megill] p. 446Lemma L19hbnae-o 38913  hbnae 2431
[Megill] p. 447Remark 9.1dfsb1 2480  sbid 2256  sbidd-misc 49585  sbidd 49584
[Megill] p. 448Remark 9.6axc14 2462
[Megill] p. 448Scheme C4'ax-c4 38869
[Megill] p. 448Scheme C5'ax-c5 38868  sp 2184
[Megill] p. 448Scheme C6'ax-11 2158
[Megill] p. 448Scheme C7'ax-c7 38870
[Megill] p. 448Scheme C8'ax-7 2008
[Megill] p. 448Scheme C9'ax-c9 38875
[Megill] p. 448Scheme C10'ax-6 1967  ax-c10 38871
[Megill] p. 448Scheme C11'ax-c11 38872
[Megill] p. 448Scheme C12'ax-8 2111
[Megill] p. 448Scheme C13'ax-9 2119
[Megill] p. 448Scheme C14'ax-c14 38876
[Megill] p. 448Scheme C15'ax-c15 38874
[Megill] p. 448Scheme C16'ax-c16 38877
[Megill] p. 448Theorem 9.4dral1-o 38889  dral1 2438  dral2-o 38915  dral2 2437  drex1 2440  drex2 2441  drsb1 2494  drsb2 2267
[Megill] p. 449Theorem 9.7sbcom2 2174  sbequ 2084  sbid2v 2508
[Megill] p. 450Example in Appendixhba1-o 38882  hba1 2293
[Mendelson] p. 35Axiom A3hirstL-ax3 46863
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3850  rspsbca 3851  stdpc4 2069
[Mendelson] p. 69Axiom 5ax-c4 38869  ra4 3857  stdpc5 2209
[Mendelson] p. 81Rule Cexlimiv 1930
[Mendelson] p. 95Axiom 6stdpc6 2028
[Mendelson] p. 95Axiom 7stdpc7 2251
[Mendelson] p. 225Axiom system NBGru 3759
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5482
[Mendelson] p. 231Exercise 4.10(k)inv1 4369
[Mendelson] p. 231Exercise 4.10(l)unv 4370
[Mendelson] p. 231Exercise 4.10(n)dfin3 4248
[Mendelson] p. 231Exercise 4.10(o)df-nul 4305
[Mendelson] p. 231Exercise 4.10(q)dfin4 4249
[Mendelson] p. 231Exercise 4.10(s)ddif 4112
[Mendelson] p. 231Definition of uniondfun3 4247
[Mendelson] p. 235Exercise 4.12(c)univ 5419
[Mendelson] p. 235Exercise 4.12(d)pwv 4876
[Mendelson] p. 235Exercise 4.12(j)pwin 5537
[Mendelson] p. 235Exercise 4.12(k)pwunss 4589
[Mendelson] p. 235Exercise 4.12(l)pwssun 5538
[Mendelson] p. 235Exercise 4.12(n)uniin 4903
[Mendelson] p. 235Exercise 4.12(p)reli 5797
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6249
[Mendelson] p. 244Proposition 4.8(g)epweon 7758
[Mendelson] p. 246Definition of successordf-suc 6346
[Mendelson] p. 250Exercise 4.36oelim2 8570
[Mendelson] p. 254Proposition 4.22(b)xpen 9117
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9032  xpsneng 9033
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9040  xpcomeng 9041
[Mendelson] p. 254Proposition 4.22(e)xpassen 9043
[Mendelson] p. 255Definitionbrsdom 8952
[Mendelson] p. 255Exercise 4.39endisj 9035
[Mendelson] p. 255Exercise 4.41mapprc 8807
[Mendelson] p. 255Exercise 4.43mapsnen 9014  mapsnend 9013
[Mendelson] p. 255Exercise 4.45mapunen 9123
[Mendelson] p. 255Exercise 4.47xpmapen 9122
[Mendelson] p. 255Exercise 4.42(a)map0e 8859
[Mendelson] p. 255Exercise 4.42(b)map1 9017
[Mendelson] p. 257Proposition 4.24(a)undom 9036
[Mendelson] p. 258Exercise 4.56(c)djuassen 10150  djucomen 10149
[Mendelson] p. 258Exercise 4.56(f)djudom1 10154
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10148
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8506
[Mendelson] p. 266Proposition 4.34(f)oaordex 8533
[Mendelson] p. 275Proposition 4.42(d)entri3 10530
[Mendelson] p. 281Definitiondf-r1 9735
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9784
[Mendelson] p. 287Axiom system MKru 3759
[MertziosUnger] p. 152Definitiondf-frgr 30195
[MertziosUnger] p. 153Remark 1frgrconngr 30230
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30232  vdgn1frgrv3 30233
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30234
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30227
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30220  2pthfrgrrn 30218  2pthfrgrrn2 30219
[Mittelstaedt] p. 9Definitiondf-oc 31188
[Monk1] p. 22Remarkconventions 30336
[Monk1] p. 22Theorem 3.1conventions 30336
[Monk1] p. 26Theorem 2.8(vii)ssin 4210
[Monk1] p. 33Theorem 3.2(i)ssrel 5753  ssrelf 32550
[Monk1] p. 33Theorem 3.2(ii)eqrel 5755
[Monk1] p. 34Definition 3.3df-opab 5178
[Monk1] p. 36Theorem 3.7(i)coi1 6243  coi2 6244
[Monk1] p. 36Theorem 3.8(v)dm0 5892  rn0 5897
[Monk1] p. 36Theorem 3.7(ii)cnvi 6122
[Monk1] p. 37Theorem 3.13(i)relxp 5664
[Monk1] p. 37Theorem 3.13(x)dmxp 5900  rnxp 6151
[Monk1] p. 37Theorem 3.13(ii)0xp 5745  xp0 6139
[Monk1] p. 38Theorem 3.16(ii)ima0 6056
[Monk1] p. 38Theorem 3.16(viii)imai 6053
[Monk1] p. 39Theorem 3.17imaex 7899  imaexALTV 38315  imaexg 7898
[Monk1] p. 39Theorem 3.16(xi)imassrn 6050
[Monk1] p. 41Theorem 4.3(i)fnopfv 7054  funfvop 7029
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6922
[Monk1] p. 42Theorem 4.4(iii)fvelima 6933
[Monk1] p. 43Theorem 4.6funun 6570
[Monk1] p. 43Theorem 4.8(iv)dff13 7236  dff13f 7237
[Monk1] p. 46Theorem 4.15(v)funex 7200  funrnex 7941
[Monk1] p. 50Definition 5.4fniunfv 7228
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6208
[Monk1] p. 52Theorem 5.11(viii)ssint 4936
[Monk1] p. 52Definition 5.13 (i)1stval2 7994  df-1st 7977
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7995  df-2nd 7978
[Monk1] p. 112Theorem 15.17(v)ranksn 9825  ranksnb 9798
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9826
[Monk1] p. 112Theorem 15.17(iii)rankun 9827  rankunb 9821
[Monk1] p. 113Theorem 15.18r1val3 9809
[Monk1] p. 113Definition 15.19df-r1 9735  r1val2 9808
[Monk1] p. 117Lemmazorn2 10477  zorn2g 10474
[Monk1] p. 133Theorem 18.11cardom 9957
[Monk1] p. 133Theorem 18.12canth3 10532
[Monk1] p. 133Theorem 18.14carduni 9952
[Monk2] p. 105Axiom C4ax-4 1809
[Monk2] p. 105Axiom C7ax-7 2008
[Monk2] p. 105Axiom C8ax-12 2178  ax-c15 38874  ax12v2 2180
[Monk2] p. 108Lemma 5ax-c4 38869
[Monk2] p. 109Lemma 12ax-11 2158
[Monk2] p. 109Lemma 15equvini 2454  equvinv 2029  eqvinop 5455
[Monk2] p. 113Axiom C5-1ax-5 1910  ax5ALT 38892
[Monk2] p. 113Axiom C5-2ax-10 2142
[Monk2] p. 113Axiom C5-3ax-11 2158
[Monk2] p. 114Lemma 21sp 2184
[Monk2] p. 114Lemma 22axc4 2320  hba1-o 38882  hba1 2293
[Monk2] p. 114Lemma 23nfia1 2154
[Monk2] p. 114Lemma 24nfa2 2177  nfra2 3353  nfra2w 3277
[Moore] p. 53Part Idf-mre 17553
[Munkres] p. 77Example 2distop 22888  indistop 22895  indistopon 22894
[Munkres] p. 77Example 3fctop 22897  fctop2 22898
[Munkres] p. 77Example 4cctop 22899
[Munkres] p. 78Definition of basisdf-bases 22839  isbasis3g 22842
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17412  tgval2 22849
[Munkres] p. 79Remarktgcl 22862
[Munkres] p. 80Lemma 2.1tgval3 22856
[Munkres] p. 80Lemma 2.2tgss2 22880  tgss3 22879
[Munkres] p. 81Lemma 2.3basgen 22881  basgen2 22882
[Munkres] p. 83Exercise 3topdifinf 37334  topdifinfeq 37335  topdifinffin 37333  topdifinfindis 37331
[Munkres] p. 89Definition of subspace topologyresttop 23053
[Munkres] p. 93Theorem 6.1(1)0cld 22931  topcld 22928
[Munkres] p. 93Theorem 6.1(2)iincld 22932
[Munkres] p. 93Theorem 6.1(3)uncld 22934
[Munkres] p. 94Definition of closureclsval 22930
[Munkres] p. 94Definition of interiorntrval 22929
[Munkres] p. 95Theorem 6.5(a)clsndisj 22968  elcls 22966
[Munkres] p. 95Theorem 6.5(b)elcls3 22976
[Munkres] p. 97Theorem 6.6clslp 23041  neindisj 23010
[Munkres] p. 97Corollary 6.7cldlp 23043
[Munkres] p. 97Definition of limit pointislp2 23038  lpval 23032
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23208
[Munkres] p. 102Definition of continuous functiondf-cn 23120  iscn 23128  iscn2 23131
[Munkres] p. 107Theorem 7.2(g)cncnp 23173  cncnp2 23174  cncnpi 23171  df-cnp 23121  iscnp 23130  iscnp2 23132
[Munkres] p. 127Theorem 10.1metcn 24437
[Munkres] p. 128Theorem 10.3metcn4 25218
[Nathanson] p. 123Remarkreprgt 34620  reprinfz1 34621  reprlt 34618
[Nathanson] p. 123Definitiondf-repr 34608
[Nathanson] p. 123Chapter 5.1circlemethnat 34640
[Nathanson] p. 123Propositionbreprexp 34632  breprexpnat 34633  itgexpif 34605
[NielsenChuang] p. 195Equation 4.73unierri 32040
[OeSilva] p. 2042Section 2ax-bgbltosilva 47766
[Pfenning] p. 17Definition XMnatded 30339
[Pfenning] p. 17Definition NNCnatded 30339  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30339
[Pfenning] p. 18Rule"natded 30339
[Pfenning] p. 18Definition /\Inatded 30339
[Pfenning] p. 18Definition ` `Enatded 30339  natded 30339  natded 30339  natded 30339  natded 30339
[Pfenning] p. 18Definition ` `Inatded 30339  natded 30339  natded 30339  natded 30339  natded 30339
[Pfenning] p. 18Definition ` `ELnatded 30339
[Pfenning] p. 18Definition ` `ERnatded 30339
[Pfenning] p. 18Definition ` `Ea,unatded 30339
[Pfenning] p. 18Definition ` `IRnatded 30339
[Pfenning] p. 18Definition ` `Ianatded 30339
[Pfenning] p. 127Definition =Enatded 30339
[Pfenning] p. 127Definition =Inatded 30339
[Ponnusamy] p. 361Theorem 6.44cphip0l 25109  df-dip 30637  dip0l 30654  ip0l 21551
[Ponnusamy] p. 361Equation 6.45cphipval 25150  ipval 30639
[Ponnusamy] p. 362Equation I1dipcj 30650  ipcj 21549
[Ponnusamy] p. 362Equation I3cphdir 25112  dipdir 30778  ipdir 21554  ipdiri 30766
[Ponnusamy] p. 362Equation I4ipidsq 30646  nmsq 25101
[Ponnusamy] p. 362Equation 6.46ip0i 30761
[Ponnusamy] p. 362Equation 6.47ip1i 30763
[Ponnusamy] p. 362Equation 6.48ip2i 30764
[Ponnusamy] p. 363Equation I2cphass 25118  dipass 30781  ipass 21560  ipassi 30777
[Prugovecki] p. 186Definition of brabraval 31880  df-bra 31786
[Prugovecki] p. 376Equation 8.1df-kb 31787  kbval 31890
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32318
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39874
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32332  atcvat4i 32333  cvrat3 39428  cvrat4 39429  lsatcvat3 39037
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32218  cvrval 39254  df-cv 32215  df-lcv 39004  lspsncv0 21062
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39886
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39887
[Quine] p. 16Definition 2.1df-clab 2709  rabid 3433  rabidd 45121
[Quine] p. 17Definition 2.1''dfsb7 2279
[Quine] p. 18Definition 2.7df-cleq 2722
[Quine] p. 19Definition 2.9conventions 30336  df-v 3457
[Quine] p. 34Theorem 5.1eqabb 2869
[Quine] p. 35Theorem 5.2abid1 2866  abid2f 2924
[Quine] p. 40Theorem 6.1sb5 2276
[Quine] p. 40Theorem 6.2sb6 2086  sbalex 2243
[Quine] p. 41Theorem 6.3df-clel 2804
[Quine] p. 41Theorem 6.4eqid 2730  eqid1 30403
[Quine] p. 41Theorem 6.5eqcom 2737
[Quine] p. 42Theorem 6.6df-sbc 3762
[Quine] p. 42Theorem 6.7dfsbcq 3763  dfsbcq2 3764
[Quine] p. 43Theorem 6.8vex 3459
[Quine] p. 43Theorem 6.9isset 3469
[Quine] p. 44Theorem 7.3spcgf 3566  spcgv 3571  spcimgf 3525
[Quine] p. 44Theorem 6.11spsbc 3774  spsbcd 3775
[Quine] p. 44Theorem 6.12elex 3476
[Quine] p. 44Theorem 6.13elab 3654  elabg 3651  elabgf 3649
[Quine] p. 44Theorem 6.14noel 4309
[Quine] p. 48Theorem 7.2snprc 4689
[Quine] p. 48Definition 7.1df-pr 4600  df-sn 4598
[Quine] p. 49Theorem 7.4snss 4757  snssg 4755
[Quine] p. 49Theorem 7.5prss 4792  prssg 4791
[Quine] p. 49Theorem 7.6prid1 4734  prid1g 4732  prid2 4735  prid2g 4733  snid 4634  snidg 4632
[Quine] p. 51Theorem 7.12snex 5399
[Quine] p. 51Theorem 7.13prex 5400
[Quine] p. 53Theorem 8.2unisn 4898  unisnALT 44887  unisng 4897
[Quine] p. 53Theorem 8.3uniun 4902
[Quine] p. 54Theorem 8.6elssuni 4909
[Quine] p. 54Theorem 8.7uni0 4907
[Quine] p. 56Theorem 8.17uniabio 6486
[Quine] p. 56Definition 8.18dfaiota2 47057  dfiota2 6473
[Quine] p. 57Theorem 8.19aiotaval 47066  iotaval 6490
[Quine] p. 57Theorem 8.22iotanul 6497
[Quine] p. 58Theorem 8.23iotaex 6492
[Quine] p. 58Definition 9.1df-op 4604
[Quine] p. 61Theorem 9.5opabid 5493  opabidw 5492  opelopab 5510  opelopaba 5504  opelopabaf 5512  opelopabf 5513  opelopabg 5506  opelopabga 5501  opelopabgf 5508  oprabid 7426  oprabidw 7425
[Quine] p. 64Definition 9.11df-xp 5652
[Quine] p. 64Definition 9.12df-cnv 5654
[Quine] p. 64Definition 9.15df-id 5541
[Quine] p. 65Theorem 10.3fun0 6589
[Quine] p. 65Theorem 10.4funi 6556
[Quine] p. 65Theorem 10.5funsn 6577  funsng 6575
[Quine] p. 65Definition 10.1df-fun 6521
[Quine] p. 65Definition 10.2args 6071  dffv4 6862
[Quine] p. 68Definition 10.11conventions 30336  df-fv 6527  fv2 6860
[Quine] p. 124Theorem 17.3nn0opth2 14247  nn0opth2i 14246  nn0opthi 14245  omopthi 8636
[Quine] p. 177Definition 25.2df-rdg 8387
[Quine] p. 232Equation icarddom 10525
[Quine] p. 284Axiom 39(vi)funimaex 6613  funimaexg 6611
[Quine] p. 331Axiom system NFru 3759
[ReedSimon] p. 36Definition (iii)ax-his3 31020
[ReedSimon] p. 63Exercise 4(a)df-dip 30637  polid 31095  polid2i 31093  polidi 31094
[ReedSimon] p. 63Exercise 4(b)df-ph 30749
[ReedSimon] p. 195Remarklnophm 31955  lnophmi 31954
[Retherford] p. 49Exercise 1(i)leopadd 32068
[Retherford] p. 49Exercise 1(ii)leopmul 32070  leopmuli 32069
[Retherford] p. 49Exercise 1(iv)leoptr 32073
[Retherford] p. 49Definition VI.1df-leop 31788  leoppos 32062
[Retherford] p. 49Exercise 1(iii)leoptri 32072
[Retherford] p. 49Definition of operator orderingleop3 32061
[Roman] p. 4Definitiondf-dmat 22383  df-dmatalt 48316
[Roman] p. 18Part Preliminariesdf-rng 20068
[Roman] p. 19Part Preliminariesdf-ring 20150
[Roman] p. 46Theorem 1.6isldepslvec2 48403
[Roman] p. 112Noteisldepslvec2 48403  ldepsnlinc 48426  zlmodzxznm 48415
[Roman] p. 112Examplezlmodzxzequa 48414  zlmodzxzequap 48417  zlmodzxzldep 48422
[Roman] p. 170Theorem 7.8cayleyhamilton 22783
[Rosenlicht] p. 80Theoremheicant 37646
[Rosser] p. 281Definitiondf-op 4604
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34644
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34645
[Rotman] p. 28Remarkpgrpgt2nabl 48283  pmtr3ncom 19411
[Rotman] p. 31Theorem 3.4symggen2 19407
[Rotman] p. 42Theorem 3.15cayley 19350  cayleyth 19351
[Rudin] p. 164Equation 27efcan 16069
[Rudin] p. 164Equation 30efzval 16077
[Rudin] p. 167Equation 48absefi 16171
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1771
[Sanford] p. 39Rule 4mptxor 1769
[Sanford] p. 40Rule 1mptnan 1768
[Schechter] p. 51Definition of antisymmetryintasym 6096
[Schechter] p. 51Definition of irreflexivityintirr 6099
[Schechter] p. 51Definition of symmetrycnvsym 6093
[Schechter] p. 51Definition of transitivitycotr 6091
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17553
[Schechter] p. 79Definition of Moore closuredf-mrc 17554
[Schechter] p. 82Section 4.5df-mrc 17554
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17556
[Schechter] p. 139Definition AC3dfac9 10108
[Schechter] p. 141Definition (MC)dfac11 43023
[Schechter] p. 149Axiom DC1ax-dc 10417  axdc3 10425
[Schechter] p. 187Definition of "ring with unit"isring 20152  isrngo 37888
[Schechter] p. 276Remark 11.6.espan0 31478
[Schechter] p. 276Definition of spandf-span 31245  spanval 31269
[Schechter] p. 428Definition 15.35bastop1 22886
[Schloeder] p. 1Lemma 1.3onelon 6365  onelord 43212  ordelon 6364  ordelord 6362
[Schloeder] p. 1Lemma 1.7onepsuc 43213  sucidg 6423
[Schloeder] p. 1Remark 1.50elon 6395  onsuc 7794  ord0 6394  ordsuci 7791
[Schloeder] p. 1Theorem 1.9epsoon 43214
[Schloeder] p. 1Definition 1.1dftr5 5226
[Schloeder] p. 1Definition 1.2dford3 42989  elon2 6351
[Schloeder] p. 1Definition 1.4df-suc 6346
[Schloeder] p. 1Definition 1.6epel 5549  epelg 5547
[Schloeder] p. 1Theorem 1.9(i)elirr 9568  epirron 43215  ordirr 6358
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43217  oneptr 43216  ontr1 6387
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6383  oneptri 43218  ordtri3or 6372
[Schloeder] p. 2Lemma 1.10ondif1 8476  ord0eln0 6396
[Schloeder] p. 2Lemma 1.13elsuci 6409  onsucss 43227  trsucss 6430
[Schloeder] p. 2Lemma 1.14ordsucss 7801
[Schloeder] p. 2Lemma 1.15onnbtwn 6436  ordnbtwn 6435
[Schloeder] p. 2Lemma 1.16orddif0suc 43229  ordnexbtwnsuc 43228
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10372  onsucf1lem 43230  onsucf1o 43233  onsucf1olem 43231  onsucrn 43232
[Schloeder] p. 2Lemma 1.18dflim7 43234
[Schloeder] p. 2Remark 1.12ordzsl 7829
[Schloeder] p. 2Theorem 1.10ondif1i 43223  ordne0gt0 43222
[Schloeder] p. 2Definition 1.11dflim6 43225  limnsuc 43226  onsucelab 43224
[Schloeder] p. 3Remark 1.21omex 9614
[Schloeder] p. 3Theorem 1.19tfinds 7844
[Schloeder] p. 3Theorem 1.22omelon 9617  ordom 7860
[Schloeder] p. 3Definition 1.20dfom3 9618
[Schloeder] p. 4Lemma 2.21onn 8615
[Schloeder] p. 4Lemma 2.7ssonuni 7763  ssorduni 7762
[Schloeder] p. 4Remark 2.4oa1suc 8506
[Schloeder] p. 4Theorem 1.23dfom5 9621  limom 7866
[Schloeder] p. 4Definition 2.1df-1o 8443  df1o2 8450
[Schloeder] p. 4Definition 2.3oa0 8491  oa0suclim 43236  oalim 8507  oasuc 8499
[Schloeder] p. 4Definition 2.5om0 8492  om0suclim 43237  omlim 8508  omsuc 8501
[Schloeder] p. 4Definition 2.6oe0 8497  oe0m1 8496  oe0suclim 43238  oelim 8509  oesuc 8502
[Schloeder] p. 5Lemma 2.10onsupuni 43190
[Schloeder] p. 5Lemma 2.11onsupsucismax 43240
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43241
[Schloeder] p. 5Lemma 2.13limexissup 43242  limexissupab 43244  limiun 43243  limuni 6402
[Schloeder] p. 5Lemma 2.14oa0r 8513
[Schloeder] p. 5Lemma 2.15om1 8517  om1om1r 43245  om1r 8518
[Schloeder] p. 5Remark 2.8oacl 8510  oaomoecl 43239  oecl 8512  omcl 8511
[Schloeder] p. 5Definition 2.9onsupintrab 43192
[Schloeder] p. 6Lemma 2.16oe1 8519
[Schloeder] p. 6Lemma 2.17oe1m 8520
[Schloeder] p. 6Lemma 2.18oe0rif 43246
[Schloeder] p. 6Theorem 2.19oasubex 43247
[Schloeder] p. 6Theorem 2.20nnacl 8586  nnamecl 43248  nnecl 8588  nnmcl 8587
[Schloeder] p. 7Lemma 3.1onsucwordi 43249
[Schloeder] p. 7Lemma 3.2oaword1 8527
[Schloeder] p. 7Lemma 3.3oaword2 8528
[Schloeder] p. 7Lemma 3.4oalimcl 8535
[Schloeder] p. 7Lemma 3.5oaltublim 43251
[Schloeder] p. 8Lemma 3.6oaordi3 43252
[Schloeder] p. 8Lemma 3.81oaomeqom 43254
[Schloeder] p. 8Lemma 3.10oa00 8534
[Schloeder] p. 8Lemma 3.11omge1 43258  omword1 8548
[Schloeder] p. 8Remark 3.9oaordnr 43257  oaordnrex 43256
[Schloeder] p. 8Theorem 3.7oaord3 43253
[Schloeder] p. 9Lemma 3.12omge2 43259  omword2 8549
[Schloeder] p. 9Lemma 3.13omlim2 43260
[Schloeder] p. 9Lemma 3.14omord2lim 43261
[Schloeder] p. 9Lemma 3.15omord2i 43262  omordi 8541
[Schloeder] p. 9Theorem 3.16omord 8543  omord2com 43263
[Schloeder] p. 10Lemma 3.172omomeqom 43264  df-2o 8444
[Schloeder] p. 10Lemma 3.19oege1 43267  oewordi 8566
[Schloeder] p. 10Lemma 3.20oege2 43268  oeworde 8568
[Schloeder] p. 10Lemma 3.21rp-oelim2 43269
[Schloeder] p. 10Lemma 3.22oeord2lim 43270
[Schloeder] p. 10Remark 3.18omnord1 43266  omnord1ex 43265
[Schloeder] p. 11Lemma 3.23oeord2i 43271
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43273
[Schloeder] p. 11Remark 3.26oenord1 43277  oenord1ex 43276
[Schloeder] p. 11Theorem 4.1oaomoencom 43278
[Schloeder] p. 11Theorem 4.2oaass 8536
[Schloeder] p. 11Theorem 3.24oeord2com 43272
[Schloeder] p. 12Theorem 4.3odi 8554
[Schloeder] p. 13Theorem 4.4omass 8555
[Schloeder] p. 14Remark 4.6oenass 43280
[Schloeder] p. 14Theorem 4.7oeoa 8572
[Schloeder] p. 15Lemma 5.1cantnftermord 43281
[Schloeder] p. 15Lemma 5.2cantnfub 43282  cantnfub2 43283
[Schloeder] p. 16Theorem 5.3cantnf2 43286
[Schwabhauser] p. 10Axiom A1axcgrrflx 28848  axtgcgrrflx 28396
[Schwabhauser] p. 10Axiom A2axcgrtr 28849
[Schwabhauser] p. 10Axiom A3axcgrid 28850  axtgcgrid 28397
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28382
[Schwabhauser] p. 11Axiom A4axsegcon 28861  axtgsegcon 28398  df-trkgcb 28384
[Schwabhauser] p. 11Axiom A5ax5seg 28872  axtg5seg 28399  df-trkgcb 28384
[Schwabhauser] p. 11Axiom A6axbtwnid 28873  axtgbtwnid 28400  df-trkgb 28383
[Schwabhauser] p. 12Axiom A7axpasch 28875  axtgpasch 28401  df-trkgb 28383
[Schwabhauser] p. 12Axiom A8axlowdim2 28894  df-trkg2d 34664
[Schwabhauser] p. 13Axiom A8axtglowdim2 28404
[Schwabhauser] p. 13Axiom A9axtgupdim2 28405  df-trkg2d 34664
[Schwabhauser] p. 13Axiom A10axeuclid 28897  axtgeucl 28406  df-trkge 28385
[Schwabhauser] p. 13Axiom A11axcont 28910  axtgcont 28403  axtgcont1 28402  df-trkgb 28383
[Schwabhauser] p. 27Theorem 2.1cgrrflx 35972
[Schwabhauser] p. 27Theorem 2.2cgrcomim 35974
[Schwabhauser] p. 27Theorem 2.3cgrtr 35977
[Schwabhauser] p. 27Theorem 2.4cgrcoml 35981
[Schwabhauser] p. 27Theorem 2.5cgrcomr 35982  tgcgrcomimp 28411  tgcgrcoml 28413  tgcgrcomr 28412
[Schwabhauser] p. 28Theorem 2.8cgrtriv 35987  tgcgrtriv 28418
[Schwabhauser] p. 28Theorem 2.105segofs 35991  tg5segofs 34672
[Schwabhauser] p. 28Definition 2.10df-afs 34669  df-ofs 35968
[Schwabhauser] p. 29Theorem 2.11cgrextend 35993  tgcgrextend 28419
[Schwabhauser] p. 29Theorem 2.12segconeq 35995  tgsegconeq 28420
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36007  btwntriv2 35997  tgbtwntriv2 28421
[Schwabhauser] p. 30Theorem 3.2btwncomim 35998  tgbtwncom 28422
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36001  tgbtwntriv1 28425
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36002  tgbtwnswapid 28426
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36008  btwnintr 36004  tgbtwnexch2 28430  tgbtwnintr 28427
[Schwabhauser] p. 30Theorem 3.6btwnexch 36010  btwnexch3 36005  tgbtwnexch 28432  tgbtwnexch3 28428
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36009  tgbtwnouttr 28431  tgbtwnouttr2 28429
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28893
[Schwabhauser] p. 32Theorem 3.14btwndiff 36012  tgbtwndiff 28440
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28433  trisegint 36013
[Schwabhauser] p. 34Theorem 4.2ifscgr 36029  tgifscgr 28442
[Schwabhauser] p. 34Theorem 4.11colcom 28492  colrot1 28493  colrot2 28494  lncom 28556  lnrot1 28557  lnrot2 28558
[Schwabhauser] p. 34Definition 4.1df-ifs 36025
[Schwabhauser] p. 35Theorem 4.3cgrsub 36030  tgcgrsub 28443
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36040  tgcgrxfr 28452
[Schwabhauser] p. 35Statement 4.4ercgrg 28451
[Schwabhauser] p. 35Definition 4.4df-cgr3 36026  df-cgrg 28445
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28445
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36041  tgbtwnxfr 28464
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36047  colinearperm2 36049  colinearperm3 36048  colinearperm4 36050  colinearperm5 36051
[Schwabhauser] p. 36Definition 4.8df-ismt 28467
[Schwabhauser] p. 36Definition 4.10df-colinear 36024  tgellng 28487  tglng 28480
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36052
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36060  lnxfr 28500
[Schwabhauser] p. 37Theorem 4.14lineext 36061  lnext 28501
[Schwabhauser] p. 37Theorem 4.16fscgr 36065  tgfscgr 28502
[Schwabhauser] p. 37Theorem 4.17linecgr 36066  lncgr 28503
[Schwabhauser] p. 37Definition 4.15df-fs 36027
[Schwabhauser] p. 38Theorem 4.18lineid 36068  lnid 28504
[Schwabhauser] p. 38Theorem 4.19idinside 36069  tgidinside 28505
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36086  tgbtwnconn1 28509
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36087  tgbtwnconn2 28510
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36088  tgbtwnconn3 28511
[Schwabhauser] p. 41Theorem 5.5brsegle2 36094
[Schwabhauser] p. 41Definition 5.4df-segle 36092  legov 28519
[Schwabhauser] p. 41Definition 5.5legov2 28520
[Schwabhauser] p. 42Remark 5.13legso 28533
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36095
[Schwabhauser] p. 42Theorem 5.7seglerflx 36097
[Schwabhauser] p. 42Theorem 5.8segletr 36099
[Schwabhauser] p. 42Theorem 5.9segleantisym 36100
[Schwabhauser] p. 42Theorem 5.10seglelin 36101
[Schwabhauser] p. 42Theorem 5.11seglemin 36098
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36103
[Schwabhauser] p. 42Proposition 5.7legid 28521
[Schwabhauser] p. 42Proposition 5.8legtrd 28523
[Schwabhauser] p. 42Proposition 5.9legtri3 28524
[Schwabhauser] p. 42Proposition 5.10legtrid 28525
[Schwabhauser] p. 42Proposition 5.11leg0 28526
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36110
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36111
[Schwabhauser] p. 43Theorem 6.4broutsideof 36106  df-outsideof 36105
[Schwabhauser] p. 43Definition 6.1broutsideof2 36107  ishlg 28536
[Schwabhauser] p. 44Theorem 6.4hlln 28541
[Schwabhauser] p. 44Theorem 6.5hlid 28543  outsideofrflx 36112
[Schwabhauser] p. 44Theorem 6.6hlcomb 28537  hlcomd 28538  outsideofcom 36113
[Schwabhauser] p. 44Theorem 6.7hltr 28544  outsideoftr 36114
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28552  outsideofeu 36116
[Schwabhauser] p. 44Definition 6.8df-ray 36123
[Schwabhauser] p. 45Part 2df-lines2 36124
[Schwabhauser] p. 45Theorem 6.13outsidele 36117
[Schwabhauser] p. 45Theorem 6.15lineunray 36132
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36133  tglineelsb2 28566
[Schwabhauser] p. 45Theorem 6.17linecom 36135  linerflx1 36134  linerflx2 36136  tglinecom 28569  tglinerflx1 28567  tglinerflx2 28568
[Schwabhauser] p. 45Theorem 6.18linethru 36138  tglinethru 28570
[Schwabhauser] p. 45Definition 6.14df-line2 36122  tglng 28480
[Schwabhauser] p. 45Proposition 6.13legbtwn 28528
[Schwabhauser] p. 46Theorem 6.19linethrueu 36141  tglinethrueu 28573
[Schwabhauser] p. 46Theorem 6.21lineintmo 36142  tglineineq 28577  tglineinteq 28579  tglineintmo 28576
[Schwabhauser] p. 46Theorem 6.23colline 28583
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28584
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28585
[Schwabhauser] p. 49Theorem 7.3mirinv 28600
[Schwabhauser] p. 49Theorem 7.7mirmir 28596
[Schwabhauser] p. 49Theorem 7.8mirreu3 28588
[Schwabhauser] p. 49Definition 7.5df-mir 28587  ismir 28593  mirbtwn 28592  mircgr 28591  mirfv 28590  mirval 28589
[Schwabhauser] p. 50Theorem 7.8mirreu 28598
[Schwabhauser] p. 50Theorem 7.9mireq 28599
[Schwabhauser] p. 50Theorem 7.10mirinv 28600
[Schwabhauser] p. 50Theorem 7.11mirf1o 28603
[Schwabhauser] p. 50Theorem 7.13miriso 28604
[Schwabhauser] p. 51Theorem 7.14mirmot 28609
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28606  mirbtwni 28605
[Schwabhauser] p. 51Theorem 7.16mircgrs 28607
[Schwabhauser] p. 51Theorem 7.17miduniq 28619
[Schwabhauser] p. 52Lemma 7.21symquadlem 28623
[Schwabhauser] p. 52Theorem 7.18miduniq1 28620
[Schwabhauser] p. 52Theorem 7.19miduniq2 28621
[Schwabhauser] p. 52Theorem 7.20colmid 28622
[Schwabhauser] p. 53Lemma 7.22krippen 28625
[Schwabhauser] p. 55Lemma 7.25midexlem 28626
[Schwabhauser] p. 57Theorem 8.2ragcom 28632
[Schwabhauser] p. 57Definition 8.1df-rag 28628  israg 28631
[Schwabhauser] p. 58Theorem 8.3ragcol 28633
[Schwabhauser] p. 58Theorem 8.4ragmir 28634
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28636
[Schwabhauser] p. 58Theorem 8.6ragflat2 28637
[Schwabhauser] p. 58Theorem 8.7ragflat 28638
[Schwabhauser] p. 58Theorem 8.8ragtriva 28639
[Schwabhauser] p. 58Theorem 8.9ragflat3 28640  ragncol 28643
[Schwabhauser] p. 58Theorem 8.10ragcgr 28641
[Schwabhauser] p. 59Theorem 8.12perpcom 28647
[Schwabhauser] p. 59Theorem 8.13ragperp 28651
[Schwabhauser] p. 59Theorem 8.14perpneq 28648
[Schwabhauser] p. 59Definition 8.11df-perpg 28630  isperp 28646
[Schwabhauser] p. 59Definition 8.13isperp2 28649
[Schwabhauser] p. 60Theorem 8.18foot 28656
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28664  colperpexlem2 28665
[Schwabhauser] p. 63Theorem 8.21colperpex 28667  colperpexlem3 28666
[Schwabhauser] p. 64Theorem 8.22mideu 28672  midex 28671
[Schwabhauser] p. 66Lemma 8.24opphllem 28669
[Schwabhauser] p. 67Theorem 9.2oppcom 28678
[Schwabhauser] p. 67Definition 9.1islnopp 28673
[Schwabhauser] p. 68Lemma 9.3opphllem2 28682
[Schwabhauser] p. 68Lemma 9.4opphllem5 28685  opphllem6 28686
[Schwabhauser] p. 69Theorem 9.5opphl 28688
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28401
[Schwabhauser] p. 70Theorem 9.6outpasch 28689
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28697
[Schwabhauser] p. 71Definition 9.7df-hpg 28692  hpgbr 28694
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28699
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28698
[Schwabhauser] p. 72Theorem 9.11hpgid 28700
[Schwabhauser] p. 72Theorem 9.12hpgcom 28701
[Schwabhauser] p. 72Theorem 9.13hpgtr 28702
[Schwabhauser] p. 73Theorem 9.18colopp 28703
[Schwabhauser] p. 73Theorem 9.19colhp 28704
[Schwabhauser] p. 88Theorem 10.2lmieu 28718
[Schwabhauser] p. 88Definition 10.1df-mid 28708
[Schwabhauser] p. 89Theorem 10.4lmicom 28722
[Schwabhauser] p. 89Theorem 10.5lmilmi 28723
[Schwabhauser] p. 89Theorem 10.6lmireu 28724
[Schwabhauser] p. 89Theorem 10.7lmieq 28725
[Schwabhauser] p. 89Theorem 10.8lmiinv 28726
[Schwabhauser] p. 89Theorem 10.9lmif1o 28729
[Schwabhauser] p. 89Theorem 10.10lmiiso 28731
[Schwabhauser] p. 89Definition 10.3df-lmi 28709
[Schwabhauser] p. 90Theorem 10.11lmimot 28732
[Schwabhauser] p. 91Theorem 10.12hypcgr 28735
[Schwabhauser] p. 92Theorem 10.14lmiopp 28736
[Schwabhauser] p. 92Theorem 10.15lnperpex 28737
[Schwabhauser] p. 92Theorem 10.16trgcopy 28738  trgcopyeu 28740
[Schwabhauser] p. 95Definition 11.2dfcgra2 28764
[Schwabhauser] p. 95Definition 11.3iscgra 28743
[Schwabhauser] p. 95Proposition 11.4cgracgr 28752
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28750  cgrahl2 28751
[Schwabhauser] p. 96Theorem 11.6cgraid 28753
[Schwabhauser] p. 96Theorem 11.9cgraswap 28754
[Schwabhauser] p. 97Theorem 11.7cgracom 28756
[Schwabhauser] p. 97Theorem 11.8cgratr 28757
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28760  cgrahl 28761
[Schwabhauser] p. 98Theorem 11.13sacgr 28765
[Schwabhauser] p. 98Theorem 11.14oacgr 28766
[Schwabhauser] p. 98Theorem 11.15acopy 28767  acopyeu 28768
[Schwabhauser] p. 101Theorem 11.24inagswap 28775
[Schwabhauser] p. 101Theorem 11.25inaghl 28779
[Schwabhauser] p. 101Definition 11.23isinag 28772
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28787
[Schwabhauser] p. 102Definition 11.27df-leag 28780  isleag 28781
[Schwabhauser] p. 107Theorem 11.49tgsas 28789  tgsas1 28788  tgsas2 28790  tgsas3 28791
[Schwabhauser] p. 108Theorem 11.50tgasa 28793  tgasa1 28792
[Schwabhauser] p. 109Theorem 11.51tgsss1 28794  tgsss2 28795  tgsss3 28796
[Shapiro] p. 230Theorem 6.5.1dchrhash 27189  dchrsum 27187  dchrsum2 27186  sumdchr 27190
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27191  sum2dchr 27192
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20004  ablfacrp2 20005
[Shapiro], p. 328Equation 9.2.4vmasum 27134
[Shapiro], p. 329Equation 9.2.7logfac2 27135
[Shapiro], p. 329Equation 9.2.9logfacrlim 27142
[Shapiro], p. 331Equation 9.2.13vmadivsum 27400
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27403
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27457  vmalogdivsum2 27456
[Shapiro], p. 375Theorem 9.4.1dirith 27447  dirith2 27446
[Shapiro], p. 375Equation 9.4.3rplogsum 27445  rpvmasum 27444  rpvmasum2 27430
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27405
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27443
[Shapiro], p. 377Lemma 9.4.1dchrisum 27410  dchrisumlem1 27407  dchrisumlem2 27408  dchrisumlem3 27409  dchrisumlema 27406
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27413
[Shapiro], p. 379Equation 9.4.16dchrmusum 27442  dchrmusumlem 27440  dchrvmasumlem 27441
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27412
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27414
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27438  dchrisum0re 27431  dchrisumn0 27439
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27424
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27428
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27429
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27484  pntrsumbnd2 27485  pntrsumo1 27483
[Shapiro], p. 405Equation 10.2.1mudivsum 27448
[Shapiro], p. 406Equation 10.2.6mulogsum 27450
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27452
[Shapiro], p. 407Equation 10.2.8mulog2sum 27455
[Shapiro], p. 418Equation 10.4.6logsqvma 27460
[Shapiro], p. 418Equation 10.4.8logsqvma2 27461
[Shapiro], p. 419Equation 10.4.10selberg 27466
[Shapiro], p. 420Equation 10.4.12selberg2lem 27468
[Shapiro], p. 420Equation 10.4.14selberg2 27469
[Shapiro], p. 422Equation 10.6.7selberg3 27477
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27478
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27475  selberg3lem2 27476
[Shapiro], p. 422Equation 10.4.23selberg4 27479
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27473
[Shapiro], p. 428Equation 10.6.2selbergr 27486
[Shapiro], p. 429Equation 10.6.8selberg3r 27487
[Shapiro], p. 430Equation 10.6.11selberg4r 27488
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27502
[Shapiro], p. 434Equation 10.6.27pntlema 27514  pntlemb 27515  pntlemc 27513  pntlemd 27512  pntlemg 27516
[Shapiro], p. 435Equation 10.6.29pntlema 27514
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27506
[Shapiro], p. 436Lemma 10.6.2pntibnd 27511
[Shapiro], p. 436Equation 10.6.34pntlema 27514
[Shapiro], p. 436Equation 10.6.35pntlem3 27527  pntleml 27529
[Stewart] p. 91Lemma 7.3constrss 33741
[Stewart] p. 92Definition 7.4.df-constr 33728
[Stewart] p. 96Theorem 7.10constraddcl 33760  constrinvcl 33771  constrmulcl 33769  constrnegcl 33761  constrsqrtcl 33777
[Stewart] p. 97Theorem 7.11constrextdg2 33747
[Stewart] p. 98Theorem 7.12constrext2chn 33757
[Stewart] p. 99Theorem 7.132sqr3nconstr 33779
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33789
[Stoll] p. 13Definition corresponds to dfsymdif3 4277
[Stoll] p. 16Exercise 4.40dif 4376  dif0 4349
[Stoll] p. 16Exercise 4.8difdifdir 4463
[Stoll] p. 17Theorem 5.1(5)unvdif 4446
[Stoll] p. 19Theorem 5.2(13)undm 4268
[Stoll] p. 19Theorem 5.2(13')indm 4269
[Stoll] p. 20Remarkinvdif 4250
[Stoll] p. 25Definition of ordered tripledf-ot 4606
[Stoll] p. 43Definitionuniiun 5030
[Stoll] p. 44Definitionintiin 5031
[Stoll] p. 45Definitiondf-iin 4966
[Stoll] p. 45Definition indexed uniondf-iun 4965
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4277
[Strang] p. 242Section 6.3expgrowth 44296
[Suppes] p. 22Theorem 2eq0 4321  eq0f 4318
[Suppes] p. 22Theorem 4eqss 3970  eqssd 3972  eqssi 3971
[Suppes] p. 23Theorem 5ss0 4373  ss0b 4372
[Suppes] p. 23Theorem 6sstr 3963  sstrALT2 44796
[Suppes] p. 23Theorem 7pssirr 4074
[Suppes] p. 23Theorem 8pssn2lp 4075
[Suppes] p. 23Theorem 9psstr 4078
[Suppes] p. 23Theorem 10pssss 4069
[Suppes] p. 25Theorem 12elin 3938  elun 4124
[Suppes] p. 26Theorem 15inidm 4198
[Suppes] p. 26Theorem 16in0 4366
[Suppes] p. 27Theorem 23unidm 4128
[Suppes] p. 27Theorem 24un0 4365
[Suppes] p. 27Theorem 25ssun1 4149
[Suppes] p. 27Theorem 26ssequn1 4157
[Suppes] p. 27Theorem 27unss 4161
[Suppes] p. 27Theorem 28indir 4257
[Suppes] p. 27Theorem 29undir 4258
[Suppes] p. 28Theorem 32difid 4347
[Suppes] p. 29Theorem 33difin 4243
[Suppes] p. 29Theorem 34indif 4251
[Suppes] p. 29Theorem 35undif1 4447
[Suppes] p. 29Theorem 36difun2 4452
[Suppes] p. 29Theorem 37difin0 4445
[Suppes] p. 29Theorem 38disjdif 4443
[Suppes] p. 29Theorem 39difundi 4261
[Suppes] p. 29Theorem 40difindi 4263
[Suppes] p. 30Theorem 41nalset 5276
[Suppes] p. 39Theorem 61uniss 4887
[Suppes] p. 39Theorem 65uniop 5483
[Suppes] p. 41Theorem 70intsn 4956
[Suppes] p. 42Theorem 71intpr 4954  intprg 4953
[Suppes] p. 42Theorem 73op1stb 5439
[Suppes] p. 42Theorem 78intun 4952
[Suppes] p. 44Definition 15(a)dfiun2 5005  dfiun2g 5002
[Suppes] p. 44Definition 15(b)dfiin2 5006
[Suppes] p. 47Theorem 86elpw 4575  elpw2 5297  elpw2g 5296  elpwg 4574  elpwgdedVD 44878
[Suppes] p. 47Theorem 87pwid 4593
[Suppes] p. 47Theorem 89pw0 4784
[Suppes] p. 48Theorem 90pwpw0 4785
[Suppes] p. 52Theorem 101xpss12 5661
[Suppes] p. 52Theorem 102xpindi 5805  xpindir 5806
[Suppes] p. 52Theorem 103xpundi 5715  xpundir 5716
[Suppes] p. 54Theorem 105elirrv 9567
[Suppes] p. 58Theorem 2relss 5752
[Suppes] p. 59Theorem 4eldm 5872  eldm2 5873  eldm2g 5871  eldmg 5870
[Suppes] p. 59Definition 3df-dm 5656
[Suppes] p. 60Theorem 6dmin 5883
[Suppes] p. 60Theorem 8rnun 6126
[Suppes] p. 60Theorem 9rnin 6127
[Suppes] p. 60Definition 4dfrn2 5860
[Suppes] p. 61Theorem 11brcnv 5854  brcnvg 5851
[Suppes] p. 62Equation 5elcnv 5848  elcnv2 5849
[Suppes] p. 62Theorem 12relcnv 6083
[Suppes] p. 62Theorem 15cnvin 6125
[Suppes] p. 62Theorem 16cnvun 6123
[Suppes] p. 63Definitiondftrrels2 38560
[Suppes] p. 63Theorem 20co02 6241
[Suppes] p. 63Theorem 21dmcoss 5946
[Suppes] p. 63Definition 7df-co 5655
[Suppes] p. 64Theorem 26cnvco 5857
[Suppes] p. 64Theorem 27coass 6246
[Suppes] p. 65Theorem 31resundi 5972
[Suppes] p. 65Theorem 34elima 6044  elima2 6045  elima3 6046  elimag 6043
[Suppes] p. 65Theorem 35imaundi 6130
[Suppes] p. 66Theorem 40dminss 6134
[Suppes] p. 66Theorem 41imainss 6135
[Suppes] p. 67Exercise 11cnvxp 6138
[Suppes] p. 81Definition 34dfec2 8685
[Suppes] p. 82Theorem 72elec 8728  elecALTV 38251  elecg 8726
[Suppes] p. 82Theorem 73eqvrelth 38596  erth 8733  erth2 8734
[Suppes] p. 83Theorem 74eqvreldisj 38599  erdisj 8736
[Suppes] p. 83Definition 35, df-parts 38750  dfmembpart2 38755
[Suppes] p. 89Theorem 96map0b 8860
[Suppes] p. 89Theorem 97map0 8864  map0g 8861
[Suppes] p. 89Theorem 98mapsn 8865  mapsnd 8863
[Suppes] p. 89Theorem 99mapss 8866
[Suppes] p. 91Definition 12(ii)alephsuc 10039
[Suppes] p. 91Definition 12(iii)alephlim 10038
[Suppes] p. 92Theorem 1enref 8962  enrefg 8961
[Suppes] p. 92Theorem 2ensym 8980  ensymb 8979  ensymi 8981
[Suppes] p. 92Theorem 3entr 8983
[Suppes] p. 92Theorem 4unen 9023
[Suppes] p. 94Theorem 15endom 8956
[Suppes] p. 94Theorem 16ssdomg 8977
[Suppes] p. 94Theorem 17domtr 8984
[Suppes] p. 95Theorem 18sbth 9070
[Suppes] p. 97Theorem 23canth2 9107  canth2g 9108
[Suppes] p. 97Definition 3brsdom2 9074  df-sdom 8925  dfsdom2 9073
[Suppes] p. 97Theorem 21(i)sdomirr 9091
[Suppes] p. 97Theorem 22(i)domnsym 9076
[Suppes] p. 97Theorem 21(ii)sdomnsym 9075
[Suppes] p. 97Theorem 22(ii)domsdomtr 9089
[Suppes] p. 97Theorem 22(iv)brdom2 8959
[Suppes] p. 97Theorem 21(iii)sdomtr 9092
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9087
[Suppes] p. 98Exercise 4fundmen 9008  fundmeng 9009
[Suppes] p. 98Exercise 6xpdom3 9047
[Suppes] p. 98Exercise 11sdomentr 9088
[Suppes] p. 104Theorem 37fofi 9280
[Suppes] p. 104Theorem 38pwfi 9286
[Suppes] p. 105Theorem 40pwfi 9286
[Suppes] p. 111Axiom for cardinal numberscarden 10522
[Suppes] p. 130Definition 3df-tr 5223
[Suppes] p. 132Theorem 9ssonuni 7763
[Suppes] p. 134Definition 6df-suc 6346
[Suppes] p. 136Theorem Schema 22findes 7885  finds 7881  finds1 7884  finds2 7883
[Suppes] p. 151Theorem 42isfinite 9623  isfinite2 9263  isfiniteg 9266  unbnn 9261
[Suppes] p. 162Definition 5df-ltnq 10889  df-ltpq 10881
[Suppes] p. 197Theorem Schema 4tfindes 7847  tfinds 7844  tfinds2 7848
[Suppes] p. 209Theorem 18oaord1 8526
[Suppes] p. 209Theorem 21oaword2 8528
[Suppes] p. 211Theorem 25oaass 8536
[Suppes] p. 225Definition 8iscard2 9947
[Suppes] p. 227Theorem 56ondomon 10534
[Suppes] p. 228Theorem 59harcard 9949
[Suppes] p. 228Definition 12(i)aleph0 10037
[Suppes] p. 228Theorem Schema 61onintss 6392
[Suppes] p. 228Theorem Schema 62onminesb 7776  onminsb 7777
[Suppes] p. 229Theorem 64alephval2 10543
[Suppes] p. 229Theorem 65alephcard 10041
[Suppes] p. 229Theorem 66alephord2i 10048
[Suppes] p. 229Theorem 67alephnbtwn 10042
[Suppes] p. 229Definition 12df-aleph 9911
[Suppes] p. 242Theorem 6weth 10466
[Suppes] p. 242Theorem 8entric 10528
[Suppes] p. 242Theorem 9carden 10522
[Szendrei] p. 11Line 6df-cloneop 35680
[Szendrei] p. 11Paragraph 3df-suppos 35684
[TakeutiZaring] p. 8Axiom 1ax-ext 2702
[TakeutiZaring] p. 13Definition 4.5df-cleq 2722
[TakeutiZaring] p. 13Proposition 4.6df-clel 2804
[TakeutiZaring] p. 13Proposition 4.9cvjust 2724
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2750
[TakeutiZaring] p. 14Definition 4.16df-oprab 7398
[TakeutiZaring] p. 14Proposition 4.14ru 3759
[TakeutiZaring] p. 15Axiom 2zfpair 5384
[TakeutiZaring] p. 15Exercise 1elpr 4622  elpr2 4624  elpr2g 4623  elprg 4620
[TakeutiZaring] p. 15Exercise 2elsn 4612  elsn2 4637  elsn2g 4636  elsng 4611  velsn 4613
[TakeutiZaring] p. 15Exercise 3elop 5435
[TakeutiZaring] p. 15Exercise 4sneq 4607  sneqr 4812
[TakeutiZaring] p. 15Definition 5.1dfpr2 4618  dfsn2 4610  dfsn2ALT 4619
[TakeutiZaring] p. 16Axiom 3uniex 7724
[TakeutiZaring] p. 16Exercise 6opth 5444
[TakeutiZaring] p. 16Exercise 7opex 5432
[TakeutiZaring] p. 16Exercise 8rext 5416
[TakeutiZaring] p. 16Corollary 5.8unex 7727  unexg 7726
[TakeutiZaring] p. 16Definition 5.3dftp2 4663
[TakeutiZaring] p. 16Definition 5.5df-uni 4880
[TakeutiZaring] p. 16Definition 5.6df-in 3929  df-un 3927
[TakeutiZaring] p. 16Proposition 5.7unipr 4896  uniprg 4895
[TakeutiZaring] p. 17Axiom 4vpwex 5340
[TakeutiZaring] p. 17Exercise 1eltp 4661
[TakeutiZaring] p. 17Exercise 5elsuc 6412  elsucg 6410  sstr2 3961
[TakeutiZaring] p. 17Exercise 6uncom 4129
[TakeutiZaring] p. 17Exercise 7incom 4180
[TakeutiZaring] p. 17Exercise 8unass 4143
[TakeutiZaring] p. 17Exercise 9inass 4199
[TakeutiZaring] p. 17Exercise 10indi 4255
[TakeutiZaring] p. 17Exercise 11undi 4256
[TakeutiZaring] p. 17Definition 5.9df-pss 3942  df-ss 3939
[TakeutiZaring] p. 17Definition 5.10df-pw 4573
[TakeutiZaring] p. 18Exercise 7unss2 4158
[TakeutiZaring] p. 18Exercise 9dfss2 3940  sseqin2 4194
[TakeutiZaring] p. 18Exercise 10ssid 3977
[TakeutiZaring] p. 18Exercise 12inss1 4208  inss2 4209
[TakeutiZaring] p. 18Exercise 13nss 4019
[TakeutiZaring] p. 18Exercise 15unieq 4890
[TakeutiZaring] p. 18Exercise 18sspwb 5417  sspwimp 44879  sspwimpALT 44886  sspwimpALT2 44889  sspwimpcf 44881
[TakeutiZaring] p. 18Exercise 19pweqb 5424
[TakeutiZaring] p. 19Axiom 5ax-rep 5242
[TakeutiZaring] p. 20Definitiondf-rab 3412
[TakeutiZaring] p. 20Corollary 5.160ex 5270
[TakeutiZaring] p. 20Definition 5.12df-dif 3925
[TakeutiZaring] p. 20Definition 5.14dfnul2 4307
[TakeutiZaring] p. 20Proposition 5.15difid 4347
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4324  n0f 4320  neq0 4323  neq0f 4319
[TakeutiZaring] p. 21Axiom 6zfreg 9566
[TakeutiZaring] p. 21Axiom 6'zfregs 9703
[TakeutiZaring] p. 21Theorem 5.22setind 9705
[TakeutiZaring] p. 21Definition 5.20df-v 3457
[TakeutiZaring] p. 21Proposition 5.21vprc 5278
[TakeutiZaring] p. 22Exercise 10ss 4371
[TakeutiZaring] p. 22Exercise 3ssex 5284  ssexg 5286
[TakeutiZaring] p. 22Exercise 4inex1 5280
[TakeutiZaring] p. 22Exercise 5ruv 9573
[TakeutiZaring] p. 22Exercise 6elirr 9568
[TakeutiZaring] p. 22Exercise 7ssdif0 4337
[TakeutiZaring] p. 22Exercise 11difdif 4106
[TakeutiZaring] p. 22Exercise 13undif3 4271  undif3VD 44843
[TakeutiZaring] p. 22Exercise 14difss 4107
[TakeutiZaring] p. 22Exercise 15sscon 4114
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3047
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3056
[TakeutiZaring] p. 23Proposition 6.2xpex 7736  xpexg 7733
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5653
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6595
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6772  fun11 6598
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6535  svrelfun 6596
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5859
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5861
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5658
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5659
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5655
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6175  dfrel2 6170
[TakeutiZaring] p. 25Exercise 3xpss 5662
[TakeutiZaring] p. 25Exercise 5relun 5782
[TakeutiZaring] p. 25Exercise 6reluni 5789
[TakeutiZaring] p. 25Exercise 9inxp 5803
[TakeutiZaring] p. 25Exercise 12relres 5984
[TakeutiZaring] p. 25Exercise 13opelres 5964  opelresi 5966
[TakeutiZaring] p. 25Exercise 14dmres 5991
[TakeutiZaring] p. 25Exercise 15resss 5980
[TakeutiZaring] p. 25Exercise 17resabs1 5985
[TakeutiZaring] p. 25Exercise 18funres 6566
[TakeutiZaring] p. 25Exercise 24relco 6087
[TakeutiZaring] p. 25Exercise 29funco 6564
[TakeutiZaring] p. 25Exercise 30f1co 6774
[TakeutiZaring] p. 26Definition 6.10eu2 2603
[TakeutiZaring] p. 26Definition 6.11conventions 30336  df-fv 6527  fv3 6883
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7910  cnvexg 7909
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7894  dmexg 7886
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7895  rnexg 7887
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44415
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7905
[TakeutiZaring] p. 27Corollary 6.13fvex 6878
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47145  tz6.12-1-afv2 47212  tz6.12-1 6888  tz6.12-afv 47144  tz6.12-afv2 47211  tz6.12 6890  tz6.12c-afv2 47213  tz6.12c 6887
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47208  tz6.12-2 6853  tz6.12i-afv2 47214  tz6.12i 6893
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6522
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6523
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6525  wfo 6517
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6524  wf1 6516
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6526  wf1o 6518
[TakeutiZaring] p. 28Exercise 4eqfnfv 7010  eqfnfv2 7011  eqfnfv2f 7014
[TakeutiZaring] p. 28Exercise 5fvco 6966
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7198
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7196
[TakeutiZaring] p. 29Exercise 9funimaex 6613  funimaexg 6611
[TakeutiZaring] p. 29Definition 6.18df-br 5116
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5555
[TakeutiZaring] p. 30Definition 6.21dffr2 5607  dffr3 6078  eliniseg 6073  iniseg 6076
[TakeutiZaring] p. 30Definition 6.22df-eprel 5546
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5623  fr3nr 7755  frirr 5622
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5599
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7757
[TakeutiZaring] p. 31Exercise 1frss 5610
[TakeutiZaring] p. 31Exercise 4wess 5632
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6328  tz6.26i 6329  wefrc 5640  wereu2 5643
[TakeutiZaring] p. 32Theorem 6.27wfi 6330  wfii 6331
[TakeutiZaring] p. 32Definition 6.28df-isom 6528
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7311
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7312
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7318
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7319
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7320
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7324
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7331
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7333
[TakeutiZaring] p. 35Notationwtr 5222
[TakeutiZaring] p. 35Theorem 7.2trelpss 44416  tz7.2 5629
[TakeutiZaring] p. 35Definition 7.1dftr3 5228
[TakeutiZaring] p. 36Proposition 7.4ordwe 6353
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6361
[TakeutiZaring] p. 36Proposition 7.6ordelord 6362  ordelordALT 44499  ordelordALTVD 44828
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6368  ordelssne 6367
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6366
[TakeutiZaring] p. 37Proposition 7.9ordin 6370
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7765
[TakeutiZaring] p. 38Corollary 7.15ordsson 7766
[TakeutiZaring] p. 38Definition 7.11df-on 6344
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6372
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44511  ordon 7760
[TakeutiZaring] p. 38Proposition 7.13onprc 7761
[TakeutiZaring] p. 39Theorem 7.17tfi 7837
[TakeutiZaring] p. 40Exercise 3ontr2 6388
[TakeutiZaring] p. 40Exercise 7dftr2 5224
[TakeutiZaring] p. 40Exercise 9onssmin 7775
[TakeutiZaring] p. 40Exercise 11unon 7814
[TakeutiZaring] p. 40Exercise 12ordun 6446
[TakeutiZaring] p. 40Exercise 14ordequn 6445
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7762
[TakeutiZaring] p. 40Proposition 7.20elssuni 4909
[TakeutiZaring] p. 41Definition 7.22df-suc 6346
[TakeutiZaring] p. 41Proposition 7.23sssucid 6422  sucidg 6423
[TakeutiZaring] p. 41Proposition 7.24onsuc 7794
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6436  ordnbtwn 6435
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7811
[TakeutiZaring] p. 42Exercise 1df-lim 6345
[TakeutiZaring] p. 42Exercise 4omssnlim 7865
[TakeutiZaring] p. 42Exercise 7ssnlim 7870
[TakeutiZaring] p. 42Exercise 8onsucssi 7825  ordelsuc 7803
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7805
[TakeutiZaring] p. 42Definition 7.27nlimon 7835
[TakeutiZaring] p. 42Definition 7.28dfom2 7852
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7873
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7875
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7876
[TakeutiZaring] p. 43Remarkomon 7862
[TakeutiZaring] p. 43Axiom 7inf3 9606  omex 9614
[TakeutiZaring] p. 43Theorem 7.32ordom 7860
[TakeutiZaring] p. 43Corollary 7.31find 7880
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7877
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7878
[TakeutiZaring] p. 44Exercise 1limomss 7855
[TakeutiZaring] p. 44Exercise 2int0 4934
[TakeutiZaring] p. 44Exercise 3trintss 5241
[TakeutiZaring] p. 44Exercise 4intss1 4935
[TakeutiZaring] p. 44Exercise 5intex 5307
[TakeutiZaring] p. 44Exercise 6oninton 7778
[TakeutiZaring] p. 44Exercise 11ordintdif 6391
[TakeutiZaring] p. 44Definition 7.35df-int 4919
[TakeutiZaring] p. 44Proposition 7.34noinfep 9631
[TakeutiZaring] p. 45Exercise 4onint 7773
[TakeutiZaring] p. 47Lemma 1tfrlem1 8353
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8374
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8375
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8376
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8383  tz7.44-2 8384  tz7.44-3 8385
[TakeutiZaring] p. 50Exercise 1smogt 8345
[TakeutiZaring] p. 50Exercise 3smoiso 8340
[TakeutiZaring] p. 50Definition 7.46df-smo 8324
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8422  tz7.49c 8423
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8420
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8419
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8421
[TakeutiZaring] p. 53Proposition 7.532eu5 2650
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9982
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9983
[TakeutiZaring] p. 56Definition 8.1oalim 8507  oasuc 8499
[TakeutiZaring] p. 57Remarktfindsg 7845
[TakeutiZaring] p. 57Proposition 8.2oacl 8510
[TakeutiZaring] p. 57Proposition 8.3oa0 8491  oa0r 8513
[TakeutiZaring] p. 57Proposition 8.16omcl 8511
[TakeutiZaring] p. 58Corollary 8.5oacan 8523
[TakeutiZaring] p. 58Proposition 8.4nnaord 8594  nnaordi 8593  oaord 8522  oaordi 8521
[TakeutiZaring] p. 59Proposition 8.6iunss2 5021  uniss2 4913
[TakeutiZaring] p. 59Proposition 8.7oawordri 8525
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8530  oawordex 8532
[TakeutiZaring] p. 59Proposition 8.9nnacl 8586
[TakeutiZaring] p. 59Proposition 8.10oaabs 8623
[TakeutiZaring] p. 60Remarkoancom 9622
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8535
[TakeutiZaring] p. 62Exercise 1nnarcl 8591
[TakeutiZaring] p. 62Exercise 5oaword1 8527
[TakeutiZaring] p. 62Definition 8.15om0x 8494  omlim 8508  omsuc 8501
[TakeutiZaring] p. 62Definition 8.15(a)om0 8492
[TakeutiZaring] p. 63Proposition 8.17nnecl 8588  nnmcl 8587
[TakeutiZaring] p. 63Proposition 8.19nnmord 8607  nnmordi 8606  omord 8543  omordi 8541
[TakeutiZaring] p. 63Proposition 8.20omcan 8544
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8611  omwordri 8547
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8514
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8517  om1r 8518
[TakeutiZaring] p. 64Proposition 8.22om00 8550
[TakeutiZaring] p. 64Proposition 8.23omordlim 8552
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8553
[TakeutiZaring] p. 64Proposition 8.25odi 8554
[TakeutiZaring] p. 65Theorem 8.26omass 8555
[TakeutiZaring] p. 67Definition 8.30nnesuc 8583  oe0 8497  oelim 8509  oesuc 8502  onesuc 8505
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8495
[TakeutiZaring] p. 67Proposition 8.32oen0 8561
[TakeutiZaring] p. 67Proposition 8.33oeordi 8562
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8496
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8520
[TakeutiZaring] p. 68Corollary 8.34oeord 8563
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8569
[TakeutiZaring] p. 68Proposition 8.35oewordri 8567
[TakeutiZaring] p. 68Proposition 8.37oeworde 8568
[TakeutiZaring] p. 69Proposition 8.41oeoa 8572
[TakeutiZaring] p. 70Proposition 8.42oeoe 8574
[TakeutiZaring] p. 73Theorem 9.1trcl 9699  tz9.1 9700
[TakeutiZaring] p. 76Definition 9.9df-r1 9735  r10 9739  r1lim 9743  r1limg 9742  r1suc 9741  r1sucg 9740
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9751  r1ord2 9752  r1ordg 9749
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9761
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9786  tz9.13 9762  tz9.13g 9763
[TakeutiZaring] p. 79Definition 9.14df-rank 9736  rankval 9787  rankvalb 9768  rankvalg 9788
[TakeutiZaring] p. 79Proposition 9.16rankel 9810  rankelb 9795
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9824  rankval3 9811  rankval3b 9797
[TakeutiZaring] p. 79Proposition 9.18rankonid 9800
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9766
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9805  rankr1c 9792  rankr1g 9803
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9806
[TakeutiZaring] p. 80Exercise 1rankss 9820  rankssb 9819
[TakeutiZaring] p. 80Exercise 2unbndrank 9813
[TakeutiZaring] p. 80Proposition 9.19bndrank 9812
[TakeutiZaring] p. 83Axiom of Choiceac4 10446  dfac3 10092
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10001  numth 10443  numth2 10442
[TakeutiZaring] p. 85Definition 10.4cardval 10517
[TakeutiZaring] p. 85Proposition 10.5cardid 10518  cardid2 9924
[TakeutiZaring] p. 85Proposition 10.9oncard 9931
[TakeutiZaring] p. 85Proposition 10.10carden 10522
[TakeutiZaring] p. 85Proposition 10.11cardidm 9930
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9915
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9936
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9928
[TakeutiZaring] p. 87Proposition 10.15pwen 9127
[TakeutiZaring] p. 88Exercise 1en0 8995
[TakeutiZaring] p. 88Exercise 7infensuc 9132
[TakeutiZaring] p. 89Exercise 10omxpen 9051
[TakeutiZaring] p. 90Corollary 10.23cardnn 9934
[TakeutiZaring] p. 90Definition 10.27alephiso 10069
[TakeutiZaring] p. 90Proposition 10.20nneneq 9183
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9194
[TakeutiZaring] p. 90Proposition 10.26alephprc 10070
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9188
[TakeutiZaring] p. 91Exercise 2alephle 10059
[TakeutiZaring] p. 91Exercise 3aleph0 10037
[TakeutiZaring] p. 91Exercise 4cardlim 9943
[TakeutiZaring] p. 91Exercise 7infpss 10187
[TakeutiZaring] p. 91Exercise 8infcntss 9291
[TakeutiZaring] p. 91Definition 10.29df-fin 8926  isfi 8953
[TakeutiZaring] p. 92Proposition 10.32onfin 9196
[TakeutiZaring] p. 92Proposition 10.34imadomg 10505
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9044
[TakeutiZaring] p. 93Proposition 10.35fodomb 10497
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10157  unxpdom 9218
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9945  cardsdomelir 9944
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9220
[TakeutiZaring] p. 94Proposition 10.39infxpen 9985
[TakeutiZaring] p. 95Definition 10.42df-map 8805
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10533  infxpidm2 9988
[TakeutiZaring] p. 95Proposition 10.41infdju 10178  infxp 10185
[TakeutiZaring] p. 96Proposition 10.44pw2en 9056  pw2f1o 9054
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9120
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10458
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10453  ac6s5 10462
[TakeutiZaring] p. 98Theorem 10.47unidom 10514
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10515  uniimadomf 10516
[TakeutiZaring] p. 100Definition 11.1cfcof 10245
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10240
[TakeutiZaring] p. 102Exercise 1cfle 10225
[TakeutiZaring] p. 102Exercise 2cf0 10222
[TakeutiZaring] p. 102Exercise 3cfsuc 10228
[TakeutiZaring] p. 102Exercise 4cfom 10235
[TakeutiZaring] p. 102Proposition 11.9coftr 10244
[TakeutiZaring] p. 103Theorem 11.15alephreg 10553
[TakeutiZaring] p. 103Proposition 11.11cardcf 10223
[TakeutiZaring] p. 103Proposition 11.13alephsing 10247
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10068
[TakeutiZaring] p. 104Proposition 11.16carduniima 10067
[TakeutiZaring] p. 104Proposition 11.18alephfp 10079  alephfp2 10080
[TakeutiZaring] p. 106Theorem 11.20gchina 10670
[TakeutiZaring] p. 106Theorem 11.21mappwen 10083
[TakeutiZaring] p. 107Theorem 11.26konigth 10540
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10554
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10555
[Tarski] p. 67Axiom B5ax-c5 38868
[Tarski] p. 67Scheme B5sp 2184
[Tarski] p. 68Lemma 6avril1 30399  equid 2012
[Tarski] p. 69Lemma 7equcomi 2017
[Tarski] p. 70Lemma 14spim 2386  spime 2388  spimew 1971
[Tarski] p. 70Lemma 16ax-12 2178  ax-c15 38874  ax12i 1966
[Tarski] p. 70Lemmas 16 and 17sb6 2086
[Tarski] p. 75Axiom B7ax6v 1968
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1910  ax5ALT 38892
[Tarski], p. 75Scheme B8 of system S2ax-7 2008  ax-8 2111  ax-9 2119
[Tarski1999] p. 178Axiom 4axtgsegcon 28398
[Tarski1999] p. 178Axiom 5axtg5seg 28399
[Tarski1999] p. 179Axiom 7axtgpasch 28401
[Tarski1999] p. 180Axiom 7.1axtgpasch 28401
[Tarski1999] p. 185Axiom 11axtgcont1 28402
[Truss] p. 114Theorem 5.18ruc 16218
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37650
[Viaclovsky8] p. 3Proposition 7ismblfin 37652
[Weierstrass] p. 272Definitiondf-mdet 22478  mdetuni 22515
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 903
[WhiteheadRussell] p. 96Axiom *1.3olc 868
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 869
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 919
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 969
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 188
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 37430
[WhiteheadRussell] p. 100Theorem *2.05frege5 43761  imim2 58  wl-luk-imim2 37425
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 46990  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2657  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37428
[WhiteheadRussell] p. 101Theorem *2.11exmid 894
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 897
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 44888  wl-luk-notnotr 37429
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43791  axfrege28 43790  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 867
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 924
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37422
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 889
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 941
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30337  pm2.27 42  wl-luk-pm2.27 37420
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38348
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 923
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 971
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 972
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 970
[WhiteheadRussell] p. 105Definition *2.33df-3or 1087
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 906
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 907
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 944
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 881
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 882
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 191
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 883
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 884
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 885
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 851
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 852
[WhiteheadRussell] p. 107Theorem *2.55orel1 888
[WhiteheadRussell] p. 107Theorem *2.56orel2 890
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 899
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 942
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 943
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 891  pm2.67 892
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 898
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 974
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 900
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 975
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 976
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 933
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 931
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 973
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 977
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 932
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 993
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 994
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 995
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 996
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 997
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 471
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 459
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 402
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 802
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 448
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 449
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 482  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 484  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 764
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 765
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 807
[WhiteheadRussell] p. 113Fact)pm3.45 622
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 809
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 492
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 493
[WhiteheadRussell] p. 113Theorem *3.44jao 962  pm3.44 961
[WhiteheadRussell] p. 113Theorem *3.47anim12 808
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 965
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 261
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 353
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 806
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 832
[WhiteheadRussell] p. 117Theorem *4.21bicom 222
[WhiteheadRussell] p. 117Theorem *4.22biantr 805  bitr 804
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 563
[WhiteheadRussell] p. 117Theorem *4.25oridm 904  pm4.25 905
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1009
[WhiteheadRussell] p. 118Theorem *4.31orcom 870
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[WhiteheadRussell] p. 118Theorem *4.33orass 921
[WhiteheadRussell] p. 118Theorem *4.36anbi1 633
[WhiteheadRussell] p. 118Theorem *4.37orbi1 917
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 637
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 978
[WhiteheadRussell] p. 118Definition *4.34df-3an 1088
[WhiteheadRussell] p. 119Theorem *4.41ordi 1007
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1053
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1024
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 998
[WhiteheadRussell] p. 119Theorem *4.45orabs 1000  pm4.45 999  pm4.45im 827
[WhiteheadRussell] p. 120Theorem *4.5anor 984
[WhiteheadRussell] p. 120Theorem *4.6imor 853
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 983
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 986
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 987
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 988
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 989
[WhiteheadRussell] p. 120Theorem *4.56ioran 985  pm4.56 990
[WhiteheadRussell] p. 120Theorem *4.57oran 991  pm4.57 992
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 856
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 849
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 850
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 398
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 557  pm4.71d 561  pm4.71i 559  pm4.71r 558  pm4.71rd 562  pm4.71ri 560
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 951
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 936
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 963  pm4.77 964
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 934
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1005
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1025
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1026
[WhiteheadRussell] p. 122Theorem *4.84imbi1 347
[WhiteheadRussell] p. 122Theorem *4.85imbi2 348
[WhiteheadRussell] p. 122Theorem *4.86bibi1 351
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 387  impexp 450  pm4.87 843
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 823
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 946  pm5.11g 945
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 947
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 949
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 948
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1014
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1015
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1013
[WhiteheadRussell] p. 124Theorem *5.18nbbn 383  pm5.18 381
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 386
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 824
[WhiteheadRussell] p. 124Theorem *5.22xor 1016
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1049
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1050
[WhiteheadRussell] p. 124Theorem *5.25dfor2 901
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 572
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 388
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 361
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1003
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 955
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 830
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 573
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 835
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 825
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 833
[WhiteheadRussell] p. 125Theorem *5.41imdi 389  pm5.41 390
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 543
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 542
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1006
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1019
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 950
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1002
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1020
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1021
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1029
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1030
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44319
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44320
[WhiteheadRussell] p. 147Theorem *10.2219.26 1870
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44321
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44322
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44323
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1893
[WhiteheadRussell] p. 151Theorem *10.301albitr 44324
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44325
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44326
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44327
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44328
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44330
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44331
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44332
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44329
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2091
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44335
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44336
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2071
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2161
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1829
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1830
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44337
[WhiteheadRussell] p. 162Theorem *11.322alim 44338
[WhiteheadRussell] p. 162Theorem *11.332albi 44339
[WhiteheadRussell] p. 162Theorem *11.342exim 44340
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44342
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44341
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1887
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44344
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44345
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44343
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1828
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44346
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44347
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1846
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44348
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2344
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1860
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44353
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44349
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44350
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44351
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44352
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44357
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44354
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44355
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44356
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44358
[WhiteheadRussell] p. 175Definition *14.02df-eu 2563
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44368  pm13.13b 44369
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44370
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3008
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3009
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3641
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44376
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44377
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44371
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44514  pm13.193 44372
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44373
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44374
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44375
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44382
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44381
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44380
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3824
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44383  pm14.122b 44384  pm14.122c 44385
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44386  pm14.123b 44387  pm14.123c 44388
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44390
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44389
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44391
[WhiteheadRussell] p. 190Theorem *14.22iota4 6500
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44392
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6501
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44393
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44395
[WhiteheadRussell] p. 192Theorem *14.26eupick 2627  eupickbi 2630  sbaniota 44396
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44394
[WhiteheadRussell] p. 192Theorem *14.271eubi 2578
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44398
[WhiteheadRussell] p. 235Definition *30.01conventions 30336  df-fv 6527
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9972  pm54.43lem 9971
[Young] p. 141Definition of operator orderingleop2 32060
[Young] p. 142Example 12.2(i)0leop 32066  idleop 32067
[vandenDries] p. 42Lemma 61irrapx1 42788
[vandenDries] p. 43Theorem 62pellex 42795  pellexlem1 42789

This page was last updated on 26-Nov-2025.
Copyright terms: Public domain