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 17595
[Adamek] p. 21Condition 3.1(b)df-cat 17595
[Adamek] p. 22Example 3.3(1)df-setc 18004
[Adamek] p. 24Example 3.3(4.c)0cat 17616  0funcg 49366  df-termc 49754
[Adamek] p. 24Example 3.3(4.d)df-prstc 49831  prsthinc 49745
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49859  df-mndtc 49859
[Adamek] p. 24Example 3.3(4)(c)discsnterm 49855
[Adamek] p. 25Definition 3.5df-oppc 17639
[Adamek] p. 25Example 3.6(1)oduoppcciso 49847
[Adamek] p. 25Example 3.6(2)oppgoppcco 49872  oppgoppchom 49871  oppgoppcid 49873
[Adamek] p. 28Remark 3.9oppciso 17709
[Adamek] p. 28Remark 3.12invf1o 17697  invisoinvl 17718
[Adamek] p. 28Example 3.13idinv 17717  idiso 17716
[Adamek] p. 28Corollary 3.11inveq 17702
[Adamek] p. 28Definition 3.8df-inv 17676  df-iso 17677  dfiso2 17700
[Adamek] p. 28Proposition 3.10sectcan 17683
[Adamek] p. 29Remark 3.16cicer 17734  cicerALT 49327
[Adamek] p. 29Definition 3.15cic 17727  df-cic 17724
[Adamek] p. 29Definition 3.17df-func 17786
[Adamek] p. 29Proposition 3.14(1)invinv 17698
[Adamek] p. 29Proposition 3.14(2)invco 17699  isoco 17705
[Adamek] p. 30Remark 3.19df-func 17786
[Adamek] p. 30Example 3.20(1)idfucl 17809
[Adamek] p. 30Example 3.20(2)diag1 49585
[Adamek] p. 32Proposition 3.21funciso 17802
[Adamek] p. 33Example 3.26(1)discsnterm 49855  discthing 49742
[Adamek] p. 33Example 3.26(2)df-thinc 49699  prsthinc 49745  thincciso 49734  thincciso2 49736  thincciso3 49737  thinccisod 49735
[Adamek] p. 33Example 3.26(3)df-mndtc 49859
[Adamek] p. 33Proposition 3.23cofucl 17816  cofucla 49377
[Adamek] p. 34Remark 3.28(1)cofidfth 49443
[Adamek] p. 34Remark 3.28(2)catciso 18039  catcisoi 49681
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18094
[Adamek] p. 34Definition 3.27(2)df-fth 17835
[Adamek] p. 34Definition 3.27(3)df-full 17834
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18094
[Adamek] p. 35Corollary 3.32ffthiso 17859
[Adamek] p. 35Proposition 3.30(c)cofth 17865
[Adamek] p. 35Proposition 3.30(d)cofull 17864
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18079
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18079
[Adamek] p. 39Remark 3.422oppf 49413
[Adamek] p. 39Definition 3.41df-oppf 49404  funcoppc 17803
[Adamek] p. 39Definition 3.44.df-catc 18027  elcatchom 49678
[Adamek] p. 39Proposition 3.43(c)fthoppc 17853  fthoppf 49445
[Adamek] p. 39Proposition 3.43(d)fulloppc 17852  fulloppf 49444
[Adamek] p. 40Remark 3.48catccat 18036
[Adamek] p. 40Definition 3.470funcg 49366  df-catc 18027
[Adamek] p. 45Exercise 3Gincat 49882
[Adamek] p. 48Remark 4.2(2)cnelsubc 49885  nelsubc3 49352
[Adamek] p. 48Remark 4.2(3)imasubc 49432  imasubc2 49433  imasubc3 49437
[Adamek] p. 48Example 4.3(1.a)0subcat 17766
[Adamek] p. 48Example 4.3(1.b)catsubcat 17767
[Adamek] p. 48Definition 4.1(1)nelsubc3 49352
[Adamek] p. 48Definition 4.1(2)fullsubc 17778
[Adamek] p. 48Definition 4.1(a)df-subc 17740
[Adamek] p. 49Remark 4.4idsubc 49441
[Adamek] p. 49Remark 4.4(1)idemb 49440
[Adamek] p. 49Remark 4.4(2)idfullsubc 49442  ressffth 17868
[Adamek] p. 58Exercise 4Asetc1onsubc 49883
[Adamek] p. 83Definition 6.1df-nat 17874
[Adamek] p. 87Remark 6.14(a)fuccocl 17895
[Adamek] p. 87Remark 6.14(b)fucass 17899
[Adamek] p. 87Definition 6.15df-fuc 17875
[Adamek] p. 88Remark 6.16fuccat 17901
[Adamek] p. 101Definition 7.10funcg 49366  df-inito 17912
[Adamek] p. 101Example 7.2(3)0funcg 49366  df-termc 49754  initc 49372
[Adamek] p. 101Example 7.2 (6)irinitoringc 21438
[Adamek] p. 102Definition 7.4df-termo 17913  oppctermo 49517
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17940
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17944
[Adamek] p. 103Remark 7.8oppczeroo 49518
[Adamek] p. 103Definition 7.7df-zeroo 17914
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21439
[Adamek] p. 103Proposition 7.6termoeu1w 17947
[Adamek] p. 106Definition 7.19df-sect 17675
[Adamek] p. 107Example 7.20(7)thincinv 49750
[Adamek] p. 108Example 7.25(4)thincsect2 49749
[Adamek] p. 110Example 7.33(9)thincmon 49714
[Adamek] p. 110Proposition 7.35sectmon 17710
[Adamek] p. 112Proposition 7.42sectepi 17712
[Adamek] p. 185Section 10.67updjud 9850
[Adamek] p. 193Definition 11.1(1)df-lmd 49926
[Adamek] p. 193Definition 11.3(1)df-lmd 49926
[Adamek] p. 194Definition 11.3(2)df-lmd 49926
[Adamek] p. 202Definition 11.27(1)df-cmd 49927
[Adamek] p. 202Definition 11.27(2)df-cmd 49927
[Adamek] p. 478Item Rngdf-ringc 20583
[AhoHopUll] p. 2Section 1.1df-bigo 48830
[AhoHopUll] p. 12Section 1.3df-blen 48852
[AhoHopUll] p. 318Section 9.1df-concat 14498  df-pfx 14599  df-substr 14569  df-word 14441  lencl 14460  wrd0 14466
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24656  df-nmoo 30803
[AkhiezerGlazman] p. 64Theoremhmopidmch 32211  hmopidmchi 32209
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32259  pjcmul2i 32260
[AkhiezerGlazman] p. 72Theoremcnvunop 31976  unoplin 31978
[AkhiezerGlazman] p. 72Equation 2unopadj 31977  unopadj2 31996
[AkhiezerGlazman] p. 73Theoremelunop2 32071  lnopunii 32070
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32144
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27909
[Alling] p. 184Axiom Bbdayfo 27649
[Alling] p. 184Axiom Osltso 27648
[Alling] p. 184Axiom SDnodense 27664
[Alling] p. 185Lemma 0nocvxmin 27755
[Alling] p. 185Theoremconway 27777
[Alling] p. 185Axiom FEnoeta 27715
[Alling] p. 186Theorem 4slerec 27797  slerecd 27798
[Alling], p. 2Definitionrp-brsslt 43700
[Alling], p. 3Notenla0001 43703  nla0002 43701  nla0003 43702
[Apostol] p. 18Theorem I.1addcan 11321  addcan2d 11341  addcan2i 11331  addcand 11340  addcani 11330
[Apostol] p. 18Theorem I.2negeu 11374
[Apostol] p. 18Theorem I.3negsub 11433  negsubd 11502  negsubi 11463
[Apostol] p. 18Theorem I.4negneg 11435  negnegd 11487  negnegi 11455
[Apostol] p. 18Theorem I.5subdi 11574  subdid 11597  subdii 11590  subdir 11575  subdird 11598  subdiri 11591
[Apostol] p. 18Theorem I.6mul01 11316  mul01d 11336  mul01i 11327  mul02 11315  mul02d 11335  mul02i 11326
[Apostol] p. 18Theorem I.7mulcan 11778  mulcan2d 11775  mulcand 11774  mulcani 11780
[Apostol] p. 18Theorem I.8receu 11786  xreceu 32984
[Apostol] p. 18Theorem I.9divrec 11816  divrecd 11924  divreci 11890  divreczi 11883
[Apostol] p. 18Theorem I.10recrec 11842  recreci 11877
[Apostol] p. 18Theorem I.11mul0or 11781  mul0ord 11789  mul0ori 11788
[Apostol] p. 18Theorem I.12mul2neg 11580  mul2negd 11596  mul2negi 11589  mulneg1 11577  mulneg1d 11594  mulneg1i 11587
[Apostol] p. 18Theorem I.13divadddiv 11860  divadddivd 11965  divadddivi 11907
[Apostol] p. 18Theorem I.14divmuldiv 11845  divmuldivd 11962  divmuldivi 11905  rdivmuldivd 20353
[Apostol] p. 18Theorem I.15divdivdiv 11846  divdivdivd 11968  divdivdivi 11908
[Apostol] p. 20Axiom 7rpaddcl 12933  rpaddcld 12968  rpmulcl 12934  rpmulcld 12969
[Apostol] p. 20Axiom 8rpneg 12943
[Apostol] p. 20Axiom 90nrp 12946
[Apostol] p. 20Theorem I.17lttri 11263
[Apostol] p. 20Theorem I.18ltadd1d 11734  ltadd1dd 11752  ltadd1i 11695
[Apostol] p. 20Theorem I.19ltmul1 11995  ltmul1a 11994  ltmul1i 12064  ltmul1ii 12074  ltmul2 11996  ltmul2d 12995  ltmul2dd 13009  ltmul2i 12067
[Apostol] p. 20Theorem I.20msqgt0 11661  msqgt0d 11708  msqgt0i 11678
[Apostol] p. 20Theorem I.210lt1 11663
[Apostol] p. 20Theorem I.23lt0neg1 11647  lt0neg1d 11710  ltneg 11641  ltnegd 11719  ltnegi 11685
[Apostol] p. 20Theorem I.25lt2add 11626  lt2addd 11764  lt2addi 11703
[Apostol] p. 20Definition of positive numbersdf-rp 12910
[Apostol] p. 21Exercise 4recgt0 11991  recgt0d 12080  recgt0i 12051  recgt0ii 12052
[Apostol] p. 22Definition of integersdf-z 12493
[Apostol] p. 22Definition of positive integersdfnn3 12163
[Apostol] p. 22Definition of rationalsdf-q 12866
[Apostol] p. 24Theorem I.26supeu 9361
[Apostol] p. 26Theorem I.28nnunb 12401
[Apostol] p. 26Theorem I.29arch 12402  archd 45442
[Apostol] p. 28Exercise 2btwnz 12599
[Apostol] p. 28Exercise 3nnrecl 12403
[Apostol] p. 28Exercise 4rebtwnz 12864
[Apostol] p. 28Exercise 5zbtwnre 12863
[Apostol] p. 28Exercise 6qbtwnre 13118
[Apostol] p. 28Exercise 10(a)zeneo 16270  zneo 12579  zneoALTV 47951
[Apostol] p. 29Theorem I.35cxpsqrtth 26699  msqsqrtd 15370  resqrtth 15182  sqrtth 15292  sqrtthi 15298  sqsqrtd 15369
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12152
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12830
[Apostol] p. 361Remarkcrreczi 14155
[Apostol] p. 363Remarkabsgt0i 15327
[Apostol] p. 363Exampleabssubd 15383  abssubi 15331
[ApostolNT] p. 7Remarkfmtno0 47822  fmtno1 47823  fmtno2 47832  fmtno3 47833  fmtno4 47834  fmtno5fac 47864  fmtnofz04prm 47859
[ApostolNT] p. 7Definitiondf-fmtno 47810
[ApostolNT] p. 8Definitiondf-ppi 27070
[ApostolNT] p. 14Definitiondf-dvds 16184
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16200
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16225
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16220
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16213
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16215
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16201
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16202
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16207
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16242
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16244
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16246
[ApostolNT] p. 15Definitiondf-gcd 16426  dfgcd2 16477
[ApostolNT] p. 16Definitionisprm2 16613
[ApostolNT] p. 16Theorem 1.5coprmdvds 16584
[ApostolNT] p. 16Theorem 1.7prminf 16847
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16444
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16478
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16480
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16459
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16451
[ApostolNT] p. 17Theorem 1.8coprm 16642
[ApostolNT] p. 17Theorem 1.9euclemma 16644
[ApostolNT] p. 17Theorem 1.101arith2 16860
[ApostolNT] p. 18Theorem 1.13prmrec 16854
[ApostolNT] p. 19Theorem 1.14divalg 16334
[ApostolNT] p. 20Theorem 1.15eucalg 16518
[ApostolNT] p. 24Definitiondf-mu 27071
[ApostolNT] p. 25Definitiondf-phi 16697
[ApostolNT] p. 25Theorem 2.1musum 27161
[ApostolNT] p. 26Theorem 2.2phisum 16722
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16707
[ApostolNT] p. 28Theorem 2.5(c)phimul 16711
[ApostolNT] p. 32Definitiondf-vma 27068
[ApostolNT] p. 32Theorem 2.9muinv 27163
[ApostolNT] p. 32Theorem 2.10vmasum 27187
[ApostolNT] p. 38Remarkdf-sgm 27072
[ApostolNT] p. 38Definitiondf-sgm 27072
[ApostolNT] p. 75Definitiondf-chp 27069  df-cht 27067
[ApostolNT] p. 104Definitioncongr 16595
[ApostolNT] p. 106Remarkdvdsval3 16187
[ApostolNT] p. 106Definitionmoddvds 16194
[ApostolNT] p. 107Example 2mod2eq0even 16277
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16278
[ApostolNT] p. 107Example 4zmod1congr 13812
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13852
[ApostolNT] p. 107Theorem 5.2(c)modexp 14165
[ApostolNT] p. 108Theorem 5.3modmulconst 16219
[ApostolNT] p. 109Theorem 5.4cncongr1 16598
[ApostolNT] p. 109Theorem 5.6gcdmodi 17006
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16600
[ApostolNT] p. 113Theorem 5.17eulerth 16714
[ApostolNT] p. 113Theorem 5.18vfermltl 16733
[ApostolNT] p. 114Theorem 5.19fermltl 16715
[ApostolNT] p. 116Theorem 5.24wilthimp 27042
[ApostolNT] p. 179Definitiondf-lgs 27266  lgsprme0 27310
[ApostolNT] p. 180Example 11lgs 27311
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27287
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27302
[ApostolNT] p. 181Theorem 9.4m1lgs 27359
[ApostolNT] p. 181Theorem 9.52lgs 27378  2lgsoddprm 27387
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27345
[ApostolNT] p. 185Theorem 9.8lgsquad 27354
[ApostolNT] p. 188Definitiondf-lgs 27266  lgs1 27312
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27303
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27305
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27313
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27314
[Baer] p. 40Property (b)mapdord 41935
[Baer] p. 40Property (c)mapd11 41936
[Baer] p. 40Property (e)mapdin 41959  mapdlsm 41961
[Baer] p. 40Property (f)mapd0 41962
[Baer] p. 40Definition of projectivitydf-mapd 41922  mapd1o 41945
[Baer] p. 41Property (g)mapdat 41964
[Baer] p. 44Part (1)mapdpg 42003
[Baer] p. 45Part (2)hdmap1eq 42098  mapdheq 42025  mapdheq2 42026  mapdheq2biN 42027
[Baer] p. 45Part (3)baerlem3 42010
[Baer] p. 46Part (4)mapdheq4 42029  mapdheq4lem 42028
[Baer] p. 46Part (5)baerlem5a 42011  baerlem5abmN 42015  baerlem5amN 42013  baerlem5b 42012  baerlem5bmN 42014
[Baer] p. 47Part (6)hdmap1l6 42118  hdmap1l6a 42106  hdmap1l6e 42111  hdmap1l6f 42112  hdmap1l6g 42113  hdmap1l6lem1 42104  hdmap1l6lem2 42105  mapdh6N 42044  mapdh6aN 42032  mapdh6eN 42037  mapdh6fN 42038  mapdh6gN 42039  mapdh6lem1N 42030  mapdh6lem2N 42031
[Baer] p. 48Part 9hdmapval 42125
[Baer] p. 48Part 10hdmap10 42137
[Baer] p. 48Part 11hdmapadd 42140
[Baer] p. 48Part (6)hdmap1l6h 42114  mapdh6hN 42040
[Baer] p. 48Part (7)mapdh75cN 42050  mapdh75d 42051  mapdh75e 42049  mapdh75fN 42052  mapdh7cN 42046  mapdh7dN 42047  mapdh7eN 42045  mapdh7fN 42048
[Baer] p. 48Part (8)mapdh8 42085  mapdh8a 42072  mapdh8aa 42073  mapdh8ab 42074  mapdh8ac 42075  mapdh8ad 42076  mapdh8b 42077  mapdh8c 42078  mapdh8d 42080  mapdh8d0N 42079  mapdh8e 42081  mapdh8g 42082  mapdh8i 42083  mapdh8j 42084
[Baer] p. 48Part (9)mapdh9a 42086
[Baer] p. 48Equation 10mapdhvmap 42066
[Baer] p. 49Part 12hdmap11 42145  hdmapeq0 42141  hdmapf1oN 42162  hdmapneg 42143  hdmaprnN 42161  hdmaprnlem1N 42146  hdmaprnlem3N 42147  hdmaprnlem3uN 42148  hdmaprnlem4N 42150  hdmaprnlem6N 42151  hdmaprnlem7N 42152  hdmaprnlem8N 42153  hdmaprnlem9N 42154  hdmapsub 42144
[Baer] p. 49Part 14hdmap14lem1 42165  hdmap14lem10 42174  hdmap14lem1a 42163  hdmap14lem2N 42166  hdmap14lem2a 42164  hdmap14lem3 42167  hdmap14lem8 42172  hdmap14lem9 42173
[Baer] p. 50Part 14hdmap14lem11 42175  hdmap14lem12 42176  hdmap14lem13 42177  hdmap14lem14 42178  hdmap14lem15 42179  hgmapval 42184
[Baer] p. 50Part 15hgmapadd 42191  hgmapmul 42192  hgmaprnlem2N 42194  hgmapvs 42188
[Baer] p. 50Part 16hgmaprnN 42198
[Baer] p. 110Lemma 1hdmapip0com 42214
[Baer] p. 110Line 27hdmapinvlem1 42215
[Baer] p. 110Line 28hdmapinvlem2 42216
[Baer] p. 110Line 30hdmapinvlem3 42217
[Baer] p. 110Part 1.2hdmapglem5 42219  hgmapvv 42223
[Baer] p. 110Proposition 1hdmapinvlem4 42218
[Baer] p. 111Line 10hgmapvvlem1 42220
[Baer] p. 111Line 15hdmapg 42227  hdmapglem7 42226
[Bauer], p. 483Theorem 1.22irrexpq 26700  2irrexpqALT 26770
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2570
[BellMachover] p. 460Notationdf-mo 2540
[BellMachover] p. 460Definitionmo3 2565
[BellMachover] p. 461Axiom Extax-ext 2709
[BellMachover] p. 462Theorem 1.1axextmo 2713
[BellMachover] p. 463Axiom Repaxrep5 5233
[BellMachover] p. 463Scheme Sepax-sep 5242
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37240  sepex 5246
[BellMachover] p. 466Problemaxpow2 5313
[BellMachover] p. 466Axiom Powaxpow3 5314
[BellMachover] p. 466Axiom Unionaxun2 7684
[BellMachover] p. 468Definitiondf-ord 6321
[BellMachover] p. 469Theorem 2.2(i)ordirr 6336
[BellMachover] p. 469Theorem 2.2(iii)onelon 6343
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6338
[BellMachover] p. 471Definition of Ndf-om 7811
[BellMachover] p. 471Problem 2.5(ii)uniordint 7748
[BellMachover] p. 471Definition of Limdf-lim 6323
[BellMachover] p. 472Axiom Infzfinf2 9555
[BellMachover] p. 473Theorem 2.8limom 7826
[BellMachover] p. 477Equation 3.1df-r1 9680
[BellMachover] p. 478Definitionrankval2 9734  rankval2b 35236
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9698  r1ord3g 9695
[BellMachover] p. 480Axiom Regzfreg 9505
[BellMachover] p. 488Axiom ACac5 10391  dfac4 10036
[BellMachover] p. 490Definition of alephalephval3 10024
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39616
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32411
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32453  chirredi 32452
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32441
[Beran] p. 3Definition of joinsshjval3 31412
[Beran] p. 39Theorem 2.3(i)cmcm2 31674  cmcm2i 31651  cmcm2ii 31656  cmt2N 39547
[Beran] p. 40Theorem 2.3(iii)lecm 31675  lecmi 31660  lecmii 31661
[Beran] p. 45Theorem 3.4cmcmlem 31649
[Beran] p. 49Theorem 4.2cm2j 31678  cm2ji 31683  cm2mi 31684
[Beran] p. 95Definitiondf-sh 31265  issh2 31267
[Beran] p. 95Lemma 3.1(S5)his5 31144
[Beran] p. 95Lemma 3.1(S6)his6 31157
[Beran] p. 95Lemma 3.1(S7)his7 31148
[Beran] p. 95Lemma 3.2(S8)ho01i 31886
[Beran] p. 95Lemma 3.2(S9)hoeq1 31888
[Beran] p. 95Lemma 3.2(S10)ho02i 31887
[Beran] p. 95Lemma 3.2(S11)hoeq2 31889
[Beran] p. 95Postulate (S1)ax-his1 31140  his1i 31158
[Beran] p. 95Postulate (S2)ax-his2 31141
[Beran] p. 95Postulate (S3)ax-his3 31142
[Beran] p. 95Postulate (S4)ax-his4 31143
[Beran] p. 96Definition of normdf-hnorm 31026  dfhnorm2 31180  normval 31182
[Beran] p. 96Definition for Cauchy sequencehcau 31242
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31031
[Beran] p. 96Definition of complete subspaceisch3 31299
[Beran] p. 96Definition of convergedf-hlim 31030  hlimi 31246
[Beran] p. 97Theorem 3.3(i)norm-i-i 31191  norm-i 31187
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31195  norm-ii 31196  normlem0 31167  normlem1 31168  normlem2 31169  normlem3 31170  normlem4 31171  normlem5 31172  normlem6 31173  normlem7 31174  normlem7tALT 31177
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31197  norm-iii 31198
[Beran] p. 98Remark 3.4bcs 31239  bcsiALT 31237  bcsiHIL 31238
[Beran] p. 98Remark 3.4(B)normlem9at 31179  normpar 31213  normpari 31212
[Beran] p. 98Remark 3.4(C)normpyc 31204  normpyth 31203  normpythi 31200
[Beran] p. 99Remarklnfn0 32105  lnfn0i 32100  lnop0 32024  lnop0i 32028
[Beran] p. 99Theorem 3.5(i)nmcexi 32084  nmcfnex 32111  nmcfnexi 32109  nmcopex 32087  nmcopexi 32085
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32112  nmcfnlbi 32110  nmcoplb 32088  nmcoplbi 32086
[Beran] p. 99Theorem 3.5(iii)lnfncon 32114  lnfnconi 32113  lnopcon 32093  lnopconi 32092
[Beran] p. 100Lemma 3.6normpar2i 31214
[Beran] p. 101Lemma 3.6norm3adifi 31211  norm3adifii 31206  norm3dif 31208  norm3difi 31205
[Beran] p. 102Theorem 3.7(i)chocunii 31359  pjhth 31451  pjhtheu 31452  pjpjhth 31483  pjpjhthi 31484  pjth 25399
[Beran] p. 102Theorem 3.7(ii)ococ 31464  ococi 31463
[Beran] p. 103Remark 3.8nlelchi 32119
[Beran] p. 104Theorem 3.9riesz3i 32120  riesz4 32122  riesz4i 32121
[Beran] p. 104Theorem 3.10cnlnadj 32137  cnlnadjeu 32136  cnlnadjeui 32135  cnlnadji 32134  cnlnadjlem1 32125  nmopadjlei 32146
[Beran] p. 106Theorem 3.11(i)adjeq0 32149
[Beran] p. 106Theorem 3.11(v)nmopadji 32148
[Beran] p. 106Theorem 3.11(ii)adjmul 32150
[Beran] p. 106Theorem 3.11(iv)adjadj 31994
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32160  nmopcoadji 32159
[Beran] p. 106Theorem 3.11(iii)adjadd 32151
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32161
[Beran] p. 106Theorem 3.11(viii)adjcoi 32158  pjadj2coi 32262  pjadjcoi 32219
[Beran] p. 107Definitiondf-ch 31279  isch2 31281
[Beran] p. 107Remark 3.12choccl 31364  isch3 31299  occl 31362  ocsh 31341  shoccl 31363  shocsh 31342
[Beran] p. 107Remark 3.12(B)ococin 31466
[Beran] p. 108Theorem 3.13chintcl 31390
[Beran] p. 109Property (i)pjadj2 32245  pjadj3 32246  pjadji 31743  pjadjii 31732
[Beran] p. 109Property (ii)pjidmco 32239  pjidmcoi 32235  pjidmi 31731
[Beran] p. 110Definition of projector orderingpjordi 32231
[Beran] p. 111Remarkho0val 31808  pjch1 31728
[Beran] p. 111Definitiondf-hfmul 31792  df-hfsum 31791  df-hodif 31790  df-homul 31789  df-hosum 31788
[Beran] p. 111Lemma 4.4(i)pjo 31729
[Beran] p. 111Lemma 4.4(ii)pjch 31752  pjchi 31490
[Beran] p. 111Lemma 4.4(iii)pjoc2 31497  pjoc2i 31496
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31738
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32223  pjssmii 31739
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32222
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32221
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32226
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32224  pjssge0ii 31740
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32225  pjdifnormii 31741
[Bobzien] p. 116Statement T3stoic3 1778
[Bobzien] p. 117Statement T2stoic2a 1776
[Bobzien] p. 117Statement T4stoic4a 1779
[Bobzien] p. 117Conclusion the contradictorystoic1a 1774
[Bogachev] p. 16Definition 1.5df-oms 34430
[Bogachev] p. 17Lemma 1.5.4omssubadd 34438
[Bogachev] p. 17Example 1.5.2omsmon 34436
[Bogachev] p. 41Definition 1.11.2df-carsg 34440
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34460
[Bogachev] p. 116Definition 2.3.1df-itgm 34491  df-sitm 34469
[Bogachev] p. 118Chapter 2.4.4df-itgm 34491
[Bogachev] p. 118Definition 2.4.1df-sitg 34468
[Bollobas] p. 1Section I.1df-edg 29104  isuhgrop 29126  isusgrop 29218  isuspgrop 29217
[Bollobas] p. 2Section I.1df-isubgr 48143  df-subgr 29324  uhgrspan1 29359  uhgrspansubgr 29347
[Bollobas] p. 3Definitiondf-gric 48163  gricuspgr 48200  isuspgrim 48178
[Bollobas] p. 3Section I.1cusgrsize 29511  df-clnbgr 48101  df-cusgr 29468  df-nbgr 29389  fusgrmaxsize 29521
[Bollobas] p. 4Definitiondf-upwlks 48416  df-wlks 29656
[Bollobas] p. 4Section I.1finsumvtxdg2size 29607  finsumvtxdgeven 29609  fusgr1th 29608  fusgrvtxdgonume 29611  vtxdgoddnumeven 29610
[Bollobas] p. 5Notationdf-pths 29770
[Bollobas] p. 5Definitiondf-crcts 29842  df-cycls 29843  df-trls 29747  df-wlkson 29657
[Bollobas] p. 7Section I.1df-ushgr 29115
[BourbakiAlg1] p. 1Definition 1df-clintop 48482  df-cllaw 48468  df-mgm 18569  df-mgm2 48501
[BourbakiAlg1] p. 4Definition 5df-assintop 48483  df-asslaw 48470  df-sgrp 18648  df-sgrp2 48503
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48502  df-comlaw 48469
[BourbakiAlg1] p. 12Definition 2df-mnd 18664
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33089  mndlactf1o 33093  mndractf1 33091  mndractf1o 33094
[BourbakiAlg1] p. 92Definition 1df-ring 20174
[BourbakiAlg1] p. 93Section I.8.1df-rng 20092
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33771
[BourbakiAlg2] p. 113Chapter 5.assafld 33775  assarrginv 33774
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33816  fldextrspunfld 33814  fldextrspunlem1 33813  fldextrspunlem2 33815  fldextrspunlsp 33812  fldextrspunlsplem 33811
[BourbakiCAlg2], p. 228Proposition 21arithidom 33599  dfufd2 33612
[BourbakiEns] p. Proposition 8fcof1 7235  fcofo 7236
[BourbakiTop1] p. Remarkxnegmnf 13129  xnegpnf 13128
[BourbakiTop1] p. Remark rexneg 13130
[BourbakiTop1] p. Remark 3ust0 24168  ustfilxp 24161
[BourbakiTop1] p. Axiom GT'tgpsubcn 24038
[BourbakiTop1] p. Criterionishmeo 23707
[BourbakiTop1] p. Example 1cstucnd 24231  iducn 24230  snfil 23812
[BourbakiTop1] p. Example 2neifil 23828
[BourbakiTop1] p. Theorem 1cnextcn 24015
[BourbakiTop1] p. Theorem 2ucnextcn 24251
[BourbakiTop1] p. Theorem 3df-hcmp 34095
[BourbakiTop1] p. Paragraph 3infil 23811
[BourbakiTop1] p. Definition 1df-ucn 24223  df-ust 24149  filintn0 23809  filn0 23810  istgp 24025  ucnprima 24229
[BourbakiTop1] p. Definition 2df-cfilu 24234
[BourbakiTop1] p. Definition 3df-cusp 24245  df-usp 24205  df-utop 24179  trust 24177
[BourbakiTop1] p. Definition 6df-pcmp 33994
[BourbakiTop1] p. Property V_issnei2 23064
[BourbakiTop1] p. Theorem 1(d)iscncl 23217
[BourbakiTop1] p. Condition F_Iustssel 24154
[BourbakiTop1] p. Condition U_Iustdiag 24157
[BourbakiTop1] p. Property V_iiinnei 23073
[BourbakiTop1] p. Property V_ivneiptopreu 23081  neissex 23075
[BourbakiTop1] p. Proposition 1neips 23061  neiss 23057  ucncn 24232  ustund 24170  ustuqtop 24194
[BourbakiTop1] p. Proposition 2cnpco 23215  neiptopreu 23081  utop2nei 24198  utop3cls 24199
[BourbakiTop1] p. Proposition 3fmucnd 24239  uspreg 24221  utopreg 24200
[BourbakiTop1] p. Proposition 4imasncld 23639  imasncls 23640  imasnopn 23638
[BourbakiTop1] p. Proposition 9cnpflf2 23948
[BourbakiTop1] p. Condition F_IIustincl 24156
[BourbakiTop1] p. Condition U_IIustinvel 24158
[BourbakiTop1] p. Property V_iiielnei 23059
[BourbakiTop1] p. Proposition 11cnextucn 24250
[BourbakiTop1] p. Condition F_IIbustbasel 24155
[BourbakiTop1] p. Condition U_IIIustexhalf 24159
[BourbakiTop1] p. Definition C'''df-cmp 23335
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23794
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22842
[BourbakiTop2] p. 195Definition 1df-ldlf 33991
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46342
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46344  stoweid 46343
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46281  stoweidlem10 46290  stoweidlem14 46294  stoweidlem15 46295  stoweidlem35 46315  stoweidlem36 46316  stoweidlem37 46317  stoweidlem38 46318  stoweidlem40 46320  stoweidlem41 46321  stoweidlem43 46323  stoweidlem44 46324  stoweidlem46 46326  stoweidlem5 46285  stoweidlem50 46330  stoweidlem52 46332  stoweidlem53 46333  stoweidlem55 46335  stoweidlem56 46336
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46303  stoweidlem24 46304  stoweidlem27 46307  stoweidlem28 46308  stoweidlem30 46310
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46314  stoweidlem59 46339  stoweidlem60 46340
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46325  stoweidlem49 46329  stoweidlem7 46287
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46311  stoweidlem39 46319  stoweidlem42 46322  stoweidlem48 46328  stoweidlem51 46331  stoweidlem54 46334  stoweidlem57 46337  stoweidlem58 46338
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46305
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46297
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46291  stoweidlem13 46293  stoweidlem26 46306  stoweidlem61 46341
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46298
[Bruck] p. 1Section I.1df-clintop 48482  df-mgm 18569  df-mgm2 48501
[Bruck] p. 23Section II.1df-sgrp 18648  df-sgrp2 48503
[Bruck] p. 28Theorem 3.2dfgrp3 18973
[ChoquetDD] p. 2Definition of mappingdf-mpt 5181
[Church] p. 129Section II.24df-ifp 1064  dfifp2 1065
[Clemente] p. 10Definition ITnatded 30461
[Clemente] p. 10Definition I` `m,nnatded 30461
[Clemente] p. 11Definition E=>m,nnatded 30461
[Clemente] p. 11Definition I=>m,nnatded 30461
[Clemente] p. 11Definition E` `(1)natded 30461
[Clemente] p. 11Definition E` `(2)natded 30461
[Clemente] p. 12Definition E` `m,n,pnatded 30461
[Clemente] p. 12Definition I` `n(1)natded 30461
[Clemente] p. 12Definition I` `n(2)natded 30461
[Clemente] p. 13Definition I` `m,n,pnatded 30461
[Clemente] p. 14Proof 5.11natded 30461
[Clemente] p. 14Definition E` `nnatded 30461
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30463  ex-natded5.2 30462
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30466  ex-natded5.3 30465
[Clemente] p. 18Theorem 5.5ex-natded5.5 30468
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30470  ex-natded5.7 30469
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30472  ex-natded5.8 30471
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30474  ex-natded5.13 30473
[Clemente] p. 32Definition I` `nnatded 30461
[Clemente] p. 32Definition E` `m,n,p,anatded 30461
[Clemente] p. 32Definition E` `n,tnatded 30461
[Clemente] p. 32Definition I` `n,tnatded 30461
[Clemente] p. 43Theorem 9.20ex-natded9.20 30475
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30476
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30478  ex-natded9.26 30477
[Cohen] p. 301Remarkrelogoprlem 26560
[Cohen] p. 301Property 2relogmul 26561  relogmuld 26594
[Cohen] p. 301Property 3relogdiv 26562  relogdivd 26595
[Cohen] p. 301Property 4relogexp 26565
[Cohen] p. 301Property 1alog1 26554
[Cohen] p. 301Property 1bloge 26555
[Cohen4] p. 348Observationrelogbcxpb 26757
[Cohen4] p. 349Propertyrelogbf 26761
[Cohen4] p. 352Definitionelogb 26740
[Cohen4] p. 361Property 2relogbmul 26747
[Cohen4] p. 361Property 3logbrec 26752  relogbdiv 26749
[Cohen4] p. 361Property 4relogbreexp 26745
[Cohen4] p. 361Property 6relogbexp 26750
[Cohen4] p. 361Property 1(a)logbid1 26738
[Cohen4] p. 361Property 1(b)logb1 26739
[Cohen4] p. 367Propertylogbchbase 26741
[Cohen4] p. 377Property 2logblt 26754
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34423  sxbrsigalem4 34425
[Cohn] p. 81Section II.5acsdomd 18484  acsinfd 18483  acsinfdimd 18485  acsmap2d 18482  acsmapd 18481
[Cohn] p. 143Example 5.1.1sxbrsiga 34428
[Connell] p. 57Definitiondf-scmat 22439  df-scmatalt 48681
[Conway] p. 4Definitionslerec 27797  slerecd 27798
[Conway] p. 5Definitionaddsval 27944  addsval2 27945  df-adds 27942  df-muls 28089  df-negs 28003
[Conway] p. 7Theorem0slt1s 27810
[Conway] p. 12Theorem 12pw2cut2 28441
[Conway] p. 16Theorem 0(i)ssltright 27853
[Conway] p. 16Theorem 0(ii)ssltleft 27852
[Conway] p. 16Theorem 0(iii)slerflex 27739
[Conway] p. 17Theorem 3addsass 27987  addsassd 27988  addscom 27948  addscomd 27949  addsrid 27946  addsridd 27947
[Conway] p. 17Definitiondf-0s 27805
[Conway] p. 17Theorem 4(ii)negnegs 28026
[Conway] p. 17Theorem 4(iii)negsid 28023  negsidd 28024
[Conway] p. 18Theorem 5sleadd1 27971  sleadd1d 27977
[Conway] p. 18Definitiondf-1s 27806
[Conway] p. 18Theorem 6(ii)negscl 28018  negscld 28019
[Conway] p. 18Theorem 6(iii)addscld 27962
[Conway] p. 19Notemulsunif2 28152
[Conway] p. 19Theorem 7addsdi 28137  addsdid 28138  addsdird 28139  mulnegs1d 28142  mulnegs2d 28143  mulsass 28148  mulsassd 28149  mulscom 28121  mulscomd 28122
[Conway] p. 19Theorem 8(i)mulscl 28116  mulscld 28117
[Conway] p. 19Theorem 8(iii)slemuld 28120  sltmul 28118  sltmuld 28119
[Conway] p. 20Theorem 9mulsgt0 28126  mulsgt0d 28127
[Conway] p. 21Theorem 10(iv)precsex 28199
[Conway] p. 23Theorem 11eqscut3 27802
[Conway] p. 24Definitiondf-reno 28469
[Conway] p. 24Theorem 13(ii)readdscl 28478  remulscl 28481  renegscl 28477
[Conway] p. 27Definitiondf-ons 28233  elons2 28239
[Conway] p. 27Theorem 14sltonex 28243
[Conway] p. 28Theorem 15onscutlt 28245  onswe 28253
[Conway] p. 29Remarkmadebday 27882  newbday 27884  oldbday 27883
[Conway] p. 29Definitiondf-made 27825  df-new 27827  df-old 27826
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13785
[Crawley] p. 1Definition of posetdf-poset 18240
[Crawley] p. 107Theorem 13.2hlsupr 39683
[Crawley] p. 110Theorem 13.3arglem1N 40487  dalaw 40183
[Crawley] p. 111Theorem 13.4hlathil 42258
[Crawley] p. 111Definition of set Wdf-watsN 40287
[Crawley] p. 111Definition of dilationdf-dilN 40403  df-ldil 40401  isldil 40407
[Crawley] p. 111Definition of translationdf-ltrn 40402  df-trnN 40404  isltrn 40416  ltrnu 40418
[Crawley] p. 112Lemma Acdlema1N 40088  cdlema2N 40089  exatleN 39701
[Crawley] p. 112Lemma B1cvrat 39773  cdlemb 40091  cdlemb2 40338  cdlemb3 40903  idltrn 40447  l1cvat 39352  lhpat 40340  lhpat2 40342  lshpat 39353  ltrnel 40436  ltrnmw 40448
[Crawley] p. 112Lemma Ccdlemc1 40488  cdlemc2 40489  ltrnnidn 40471  trlat 40466  trljat1 40463  trljat2 40464  trljat3 40465  trlne 40482  trlnidat 40470  trlnle 40483
[Crawley] p. 112Definition of automorphismdf-pautN 40288
[Crawley] p. 113Lemma Ccdlemc 40494  cdlemc3 40490  cdlemc4 40491
[Crawley] p. 113Lemma Dcdlemd 40504  cdlemd1 40495  cdlemd2 40496  cdlemd3 40497  cdlemd4 40498  cdlemd5 40499  cdlemd6 40500  cdlemd7 40501  cdlemd8 40502  cdlemd9 40503  cdleme31sde 40682  cdleme31se 40679  cdleme31se2 40680  cdleme31snd 40683  cdleme32a 40738  cdleme32b 40739  cdleme32c 40740  cdleme32d 40741  cdleme32e 40742  cdleme32f 40743  cdleme32fva 40734  cdleme32fva1 40735  cdleme32fvcl 40737  cdleme32le 40744  cdleme48fv 40796  cdleme4gfv 40804  cdleme50eq 40838  cdleme50f 40839  cdleme50f1 40840  cdleme50f1o 40843  cdleme50laut 40844  cdleme50ldil 40845  cdleme50lebi 40837  cdleme50rn 40842  cdleme50rnlem 40841  cdlemeg49le 40808  cdlemeg49lebilem 40836
[Crawley] p. 113Lemma Ecdleme 40857  cdleme00a 40506  cdleme01N 40518  cdleme02N 40519  cdleme0a 40508  cdleme0aa 40507  cdleme0b 40509  cdleme0c 40510  cdleme0cp 40511  cdleme0cq 40512  cdleme0dN 40513  cdleme0e 40514  cdleme0ex1N 40520  cdleme0ex2N 40521  cdleme0fN 40515  cdleme0gN 40516  cdleme0moN 40522  cdleme1 40524  cdleme10 40551  cdleme10tN 40555  cdleme11 40567  cdleme11a 40557  cdleme11c 40558  cdleme11dN 40559  cdleme11e 40560  cdleme11fN 40561  cdleme11g 40562  cdleme11h 40563  cdleme11j 40564  cdleme11k 40565  cdleme11l 40566  cdleme12 40568  cdleme13 40569  cdleme14 40570  cdleme15 40575  cdleme15a 40571  cdleme15b 40572  cdleme15c 40573  cdleme15d 40574  cdleme16 40582  cdleme16aN 40556  cdleme16b 40576  cdleme16c 40577  cdleme16d 40578  cdleme16e 40579  cdleme16f 40580  cdleme16g 40581  cdleme19a 40600  cdleme19b 40601  cdleme19c 40602  cdleme19d 40603  cdleme19e 40604  cdleme19f 40605  cdleme1b 40523  cdleme2 40525  cdleme20aN 40606  cdleme20bN 40607  cdleme20c 40608  cdleme20d 40609  cdleme20e 40610  cdleme20f 40611  cdleme20g 40612  cdleme20h 40613  cdleme20i 40614  cdleme20j 40615  cdleme20k 40616  cdleme20l 40619  cdleme20l1 40617  cdleme20l2 40618  cdleme20m 40620  cdleme20y 40599  cdleme20zN 40598  cdleme21 40634  cdleme21d 40627  cdleme21e 40628  cdleme22a 40637  cdleme22aa 40636  cdleme22b 40638  cdleme22cN 40639  cdleme22d 40640  cdleme22e 40641  cdleme22eALTN 40642  cdleme22f 40643  cdleme22f2 40644  cdleme22g 40645  cdleme23a 40646  cdleme23b 40647  cdleme23c 40648  cdleme26e 40656  cdleme26eALTN 40658  cdleme26ee 40657  cdleme26f 40660  cdleme26f2 40662  cdleme26f2ALTN 40661  cdleme26fALTN 40659  cdleme27N 40666  cdleme27a 40664  cdleme27cl 40663  cdleme28c 40669  cdleme3 40534  cdleme30a 40675  cdleme31fv 40687  cdleme31fv1 40688  cdleme31fv1s 40689  cdleme31fv2 40690  cdleme31id 40691  cdleme31sc 40681  cdleme31sdnN 40684  cdleme31sn 40677  cdleme31sn1 40678  cdleme31sn1c 40685  cdleme31sn2 40686  cdleme31so 40676  cdleme35a 40745  cdleme35b 40747  cdleme35c 40748  cdleme35d 40749  cdleme35e 40750  cdleme35f 40751  cdleme35fnpq 40746  cdleme35g 40752  cdleme35h 40753  cdleme35h2 40754  cdleme35sn2aw 40755  cdleme35sn3a 40756  cdleme36a 40757  cdleme36m 40758  cdleme37m 40759  cdleme38m 40760  cdleme38n 40761  cdleme39a 40762  cdleme39n 40763  cdleme3b 40526  cdleme3c 40527  cdleme3d 40528  cdleme3e 40529  cdleme3fN 40530  cdleme3fa 40533  cdleme3g 40531  cdleme3h 40532  cdleme4 40535  cdleme40m 40764  cdleme40n 40765  cdleme40v 40766  cdleme40w 40767  cdleme41fva11 40774  cdleme41sn3aw 40771  cdleme41sn4aw 40772  cdleme41snaw 40773  cdleme42a 40768  cdleme42b 40775  cdleme42c 40769  cdleme42d 40770  cdleme42e 40776  cdleme42f 40777  cdleme42g 40778  cdleme42h 40779  cdleme42i 40780  cdleme42k 40781  cdleme42ke 40782  cdleme42keg 40783  cdleme42mN 40784  cdleme42mgN 40785  cdleme43aN 40786  cdleme43bN 40787  cdleme43cN 40788  cdleme43dN 40789  cdleme5 40537  cdleme50ex 40856  cdleme50ltrn 40854  cdleme51finvN 40853  cdleme51finvfvN 40852  cdleme51finvtrN 40855  cdleme6 40538  cdleme7 40546  cdleme7a 40540  cdleme7aa 40539  cdleme7b 40541  cdleme7c 40542  cdleme7d 40543  cdleme7e 40544  cdleme7ga 40545  cdleme8 40547  cdleme8tN 40552  cdleme9 40550  cdleme9a 40548  cdleme9b 40549  cdleme9tN 40554  cdleme9taN 40553  cdlemeda 40595  cdlemedb 40594  cdlemednpq 40596  cdlemednuN 40597  cdlemefr27cl 40700  cdlemefr32fva1 40707  cdlemefr32fvaN 40706  cdlemefrs32fva 40697  cdlemefrs32fva1 40698  cdlemefs27cl 40710  cdlemefs32fva1 40720  cdlemefs32fvaN 40719  cdlemesner 40593  cdlemeulpq 40517
[Crawley] p. 114Lemma E4atex 40373  4atexlem7 40372  cdleme0nex 40587  cdleme17a 40583  cdleme17c 40585  cdleme17d 40795  cdleme17d1 40586  cdleme17d2 40792  cdleme18a 40588  cdleme18b 40589  cdleme18c 40590  cdleme18d 40592  cdleme4a 40536
[Crawley] p. 115Lemma Ecdleme21a 40622  cdleme21at 40625  cdleme21b 40623  cdleme21c 40624  cdleme21ct 40626  cdleme21f 40629  cdleme21g 40630  cdleme21h 40631  cdleme21i 40632  cdleme22gb 40591
[Crawley] p. 116Lemma Fcdlemf 40860  cdlemf1 40858  cdlemf2 40859
[Crawley] p. 116Lemma Gcdlemftr1 40864  cdlemg16 40954  cdlemg28 41001  cdlemg28a 40990  cdlemg28b 41000  cdlemg3a 40894  cdlemg42 41026  cdlemg43 41027  cdlemg44 41030  cdlemg44a 41028  cdlemg46 41032  cdlemg47 41033  cdlemg9 40931  ltrnco 41016  ltrncom 41035  tgrpabl 41048  trlco 41024
[Crawley] p. 116Definition of Gdf-tgrp 41040
[Crawley] p. 117Lemma Gcdlemg17 40974  cdlemg17b 40959
[Crawley] p. 117Definition of Edf-edring-rN 41053  df-edring 41054
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41057
[Crawley] p. 118Remarktendopltp 41077
[Crawley] p. 118Lemma Hcdlemh 41114  cdlemh1 41112  cdlemh2 41113
[Crawley] p. 118Lemma Icdlemi 41117  cdlemi1 41115  cdlemi2 41116
[Crawley] p. 118Lemma Jcdlemj1 41118  cdlemj2 41119  cdlemj3 41120  tendocan 41121
[Crawley] p. 118Lemma Kcdlemk 41271  cdlemk1 41128  cdlemk10 41140  cdlemk11 41146  cdlemk11t 41243  cdlemk11ta 41226  cdlemk11tb 41228  cdlemk11tc 41242  cdlemk11u-2N 41186  cdlemk11u 41168  cdlemk12 41147  cdlemk12u-2N 41187  cdlemk12u 41169  cdlemk13-2N 41173  cdlemk13 41149  cdlemk14-2N 41175  cdlemk14 41151  cdlemk15-2N 41176  cdlemk15 41152  cdlemk16-2N 41177  cdlemk16 41154  cdlemk16a 41153  cdlemk17-2N 41178  cdlemk17 41155  cdlemk18-2N 41183  cdlemk18-3N 41197  cdlemk18 41165  cdlemk19-2N 41184  cdlemk19 41166  cdlemk19u 41267  cdlemk1u 41156  cdlemk2 41129  cdlemk20-2N 41189  cdlemk20 41171  cdlemk21-2N 41188  cdlemk21N 41170  cdlemk22-3 41198  cdlemk22 41190  cdlemk23-3 41199  cdlemk24-3 41200  cdlemk25-3 41201  cdlemk26-3 41203  cdlemk26b-3 41202  cdlemk27-3 41204  cdlemk28-3 41205  cdlemk29-3 41208  cdlemk3 41130  cdlemk30 41191  cdlemk31 41193  cdlemk32 41194  cdlemk33N 41206  cdlemk34 41207  cdlemk35 41209  cdlemk36 41210  cdlemk37 41211  cdlemk38 41212  cdlemk39 41213  cdlemk39u 41265  cdlemk4 41131  cdlemk41 41217  cdlemk42 41238  cdlemk42yN 41241  cdlemk43N 41260  cdlemk45 41244  cdlemk46 41245  cdlemk47 41246  cdlemk48 41247  cdlemk49 41248  cdlemk5 41133  cdlemk50 41249  cdlemk51 41250  cdlemk52 41251  cdlemk53 41254  cdlemk54 41255  cdlemk55 41258  cdlemk55u 41263  cdlemk56 41268  cdlemk5a 41132  cdlemk5auN 41157  cdlemk5u 41158  cdlemk6 41134  cdlemk6u 41159  cdlemk7 41145  cdlemk7u-2N 41185  cdlemk7u 41167  cdlemk8 41135  cdlemk9 41136  cdlemk9bN 41137  cdlemki 41138  cdlemkid 41233  cdlemkj-2N 41179  cdlemkj 41160  cdlemksat 41143  cdlemksel 41142  cdlemksv 41141  cdlemksv2 41144  cdlemkuat 41163  cdlemkuel-2N 41181  cdlemkuel-3 41195  cdlemkuel 41162  cdlemkuv-2N 41180  cdlemkuv2-2 41182  cdlemkuv2-3N 41196  cdlemkuv2 41164  cdlemkuvN 41161  cdlemkvcl 41139  cdlemky 41223  cdlemkyyN 41259  tendoex 41272
[Crawley] p. 120Remarkdva1dim 41282
[Crawley] p. 120Lemma Lcdleml1N 41273  cdleml2N 41274  cdleml3N 41275  cdleml4N 41276  cdleml5N 41277  cdleml6 41278  cdleml7 41279  cdleml8 41280  cdleml9 41281  dia1dim 41358
[Crawley] p. 120Lemma Mdia11N 41345  diaf11N 41346  dialss 41343  diaord 41344  dibf11N 41458  djajN 41434
[Crawley] p. 120Definition of isomorphism mapdiaval 41329
[Crawley] p. 121Lemma Mcdlemm10N 41415  dia2dimlem1 41361  dia2dimlem2 41362  dia2dimlem3 41363  dia2dimlem4 41364  dia2dimlem5 41365  diaf1oN 41427  diarnN 41426  dvheveccl 41409  dvhopN 41413
[Crawley] p. 121Lemma Ncdlemn 41509  cdlemn10 41503  cdlemn11 41508  cdlemn11a 41504  cdlemn11b 41505  cdlemn11c 41506  cdlemn11pre 41507  cdlemn2 41492  cdlemn2a 41493  cdlemn3 41494  cdlemn4 41495  cdlemn4a 41496  cdlemn5 41498  cdlemn5pre 41497  cdlemn6 41499  cdlemn7 41500  cdlemn8 41501  cdlemn9 41502  diclspsn 41491
[Crawley] p. 121Definition of phi(q)df-dic 41470
[Crawley] p. 122Lemma Ndih11 41562  dihf11 41564  dihjust 41514  dihjustlem 41513  dihord 41561  dihord1 41515  dihord10 41520  dihord11b 41519  dihord11c 41521  dihord2 41524  dihord2a 41516  dihord2b 41517  dihord2cN 41518  dihord2pre 41522  dihord2pre2 41523  dihordlem6 41510  dihordlem7 41511  dihordlem7b 41512
[Crawley] p. 122Definition of isomorphism mapdihffval 41527  dihfval 41528  dihval 41529
[Diestel] p. 3Definitiondf-gric 48163  df-grim 48160  isuspgrim 48178
[Diestel] p. 3Section 1.1df-cusgr 29468  df-nbgr 29389
[Diestel] p. 3Definition by df-grisom 48159
[Diestel] p. 4Section 1.1df-isubgr 48143  df-subgr 29324  uhgrspan1 29359  uhgrspansubgr 29347
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29611  vtxdgoddnumeven 29610
[Diestel] p. 27Section 1.10df-ushgr 29115
[EGA] p. 80Notation 1.1.1rspecval 34002
[EGA] p. 80Proposition 1.1.2zartop 34014
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34006  zarcls1 34007
[EGA] p. 81Corollary 1.1.8zart0 34017
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34020
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34023
[Eisenberg] p. 67Definition 5.3df-dif 3905
[Eisenberg] p. 82Definition 6.3dfom3 9560
[Eisenberg] p. 125Definition 8.21df-map 8769
[Eisenberg] p. 216Example 13.2(4)omenps 9568
[Eisenberg] p. 310Theorem 19.8cardprc 9896
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10469
[Enderton] p. 18Axiom of Empty Setaxnul 5251
[Enderton] p. 19Definitiondf-tp 4586
[Enderton] p. 26Exercise 5unissb 4897
[Enderton] p. 26Exercise 10pwel 5327
[Enderton] p. 28Exercise 7(b)pwun 5518
[Enderton] p. 30Theorem "Distributive laws"iinin1 5035  iinin2 5034  iinun2 5029  iunin1 5028  iunin1f 32614  iunin2 5027  uniin1 32608  uniin2 32609
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5033  iundif2 5030
[Enderton] p. 32Exercise 20unineq 4241
[Enderton] p. 33Exercise 23iinuni 5054
[Enderton] p. 33Exercise 25iununi 5055
[Enderton] p. 33Exercise 24(a)iinpw 5062
[Enderton] p. 33Exercise 24(b)iunpw 7718  iunpwss 5063
[Enderton] p. 36Definitionopthwiener 5463
[Enderton] p. 38Exercise 6(a)unipw 5399
[Enderton] p. 38Exercise 6(b)pwuni 4902
[Enderton] p. 41Lemma 3Dopeluu 5419  rnex 7854  rnexg 7846
[Enderton] p. 41Exercise 8dmuni 5864  rnuni 6107
[Enderton] p. 42Definition of a functiondffun7 6520  dffun8 6521
[Enderton] p. 43Definition of function valuefunfv2 6923
[Enderton] p. 43Definition of single-rootedfuncnv 6562
[Enderton] p. 44Definition (d)dfima2 6022  dfima3 6023
[Enderton] p. 47Theorem 3Hfvco2 6932
[Enderton] p. 49Axiom of Choice (first form)ac7 10387  ac7g 10388  df-ac 10030  dfac2 10046  dfac2a 10044  dfac2b 10045  dfac3 10035  dfac7 10047
[Enderton] p. 50Theorem 3K(a)imauni 7194
[Enderton] p. 52Definitiondf-map 8769
[Enderton] p. 53Exercise 21coass 6225
[Enderton] p. 53Exercise 27dmco 6214
[Enderton] p. 53Exercise 14(a)funin 6569
[Enderton] p. 53Exercise 22(a)imass2 6062
[Enderton] p. 54Remarkixpf 8862  ixpssmap 8874
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8840
[Enderton] p. 55Axiom of Choice (second form)ac9 10397  ac9s 10407
[Enderton] p. 56Theorem 3Meqvrelref 38866  erref 8658
[Enderton] p. 57Lemma 3Neqvrelthi 38869  erthi 8694
[Enderton] p. 57Definitiondf-ec 8639
[Enderton] p. 58Definitiondf-qs 8643
[Enderton] p. 61Exercise 35df-ec 8639
[Enderton] p. 65Exercise 56(a)dmun 5860
[Enderton] p. 68Definition of successordf-suc 6324
[Enderton] p. 71Definitiondf-tr 5207  dftr4 5212
[Enderton] p. 72Theorem 4Eunisuc 6399  unisucg 6398
[Enderton] p. 73Exercise 6unisuc 6399  unisucg 6398
[Enderton] p. 73Exercise 5(a)truni 5221
[Enderton] p. 73Exercise 5(b)trint 5223  trintALT 45157
[Enderton] p. 79Theorem 4I(A1)nna0 8534
[Enderton] p. 79Theorem 4I(A2)nnasuc 8536  onasuc 8457
[Enderton] p. 79Definition of operation valuedf-ov 7363
[Enderton] p. 80Theorem 4J(A1)nnm0 8535
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8537  onmsuc 8458
[Enderton] p. 81Theorem 4K(1)nnaass 8552
[Enderton] p. 81Theorem 4K(2)nna0r 8539  nnacom 8547
[Enderton] p. 81Theorem 4K(3)nndi 8553
[Enderton] p. 81Theorem 4K(4)nnmass 8554
[Enderton] p. 81Theorem 4K(5)nnmcom 8556
[Enderton] p. 82Exercise 16nnm0r 8540  nnmsucr 8555
[Enderton] p. 88Exercise 23nnaordex 8568
[Enderton] p. 129Definitiondf-en 8888
[Enderton] p. 132Theorem 6B(b)canth 7314
[Enderton] p. 133Exercise 1xpomen 9929
[Enderton] p. 133Exercise 2qnnen 16142
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9135
[Enderton] p. 135Corollary 6Cphp3 9137
[Enderton] p. 136Corollary 6Enneneq 9134
[Enderton] p. 136Corollary 6D(a)pssinf 9166
[Enderton] p. 136Corollary 6D(b)ominf 9168
[Enderton] p. 137Lemma 6Fpssnn 9097
[Enderton] p. 138Corollary 6Gssfi 9101
[Enderton] p. 139Theorem 6H(c)mapen 9073
[Enderton] p. 142Theorem 6I(3)xpdjuen 10094
[Enderton] p. 142Theorem 6I(4)mapdjuen 10095
[Enderton] p. 143Theorem 6Jdju0en 10090  dju1en 10086
[Enderton] p. 144Exercise 13iunfi 9247  unifi 9248  unifi2 9249
[Enderton] p. 144Corollary 6Kundif2 4430  unfi 9099  unfi2 9214
[Enderton] p. 145Figure 38ffoss 7892
[Enderton] p. 145Definitiondf-dom 8889
[Enderton] p. 146Example 1domen 8902  domeng 8903
[Enderton] p. 146Example 3nndomo 9146  nnsdom 9567  nnsdomg 9203
[Enderton] p. 149Theorem 6L(a)djudom2 10098
[Enderton] p. 149Theorem 6L(c)mapdom1 9074  xpdom1 9008  xpdom1g 9006  xpdom2g 9005
[Enderton] p. 149Theorem 6L(d)mapdom2 9080
[Enderton] p. 151Theorem 6Mzorn 10421  zorng 10418
[Enderton] p. 151Theorem 6M(4)ac8 10406  dfac5 10043
[Enderton] p. 159Theorem 6Qunictb 10490
[Enderton] p. 164Exampleinfdif 10122
[Enderton] p. 168Definitiondf-po 5533
[Enderton] p. 192Theorem 7M(a)oneli 6433
[Enderton] p. 192Theorem 7M(b)ontr1 6365
[Enderton] p. 192Theorem 7M(c)onirri 6432
[Enderton] p. 193Corollary 7N(b)0elon 6373
[Enderton] p. 193Corollary 7N(c)onsuci 7783
[Enderton] p. 193Corollary 7N(d)ssonunii 7728
[Enderton] p. 194Remarkonprc 7725
[Enderton] p. 194Exercise 16suc11 6427
[Enderton] p. 197Definitiondf-card 9855
[Enderton] p. 197Theorem 7Pcarden 10465
[Enderton] p. 200Exercise 25tfis 7799
[Enderton] p. 202Lemma 7Tr1tr 9692
[Enderton] p. 202Definitiondf-r1 9680
[Enderton] p. 202Theorem 7Qr1val1 9702
[Enderton] p. 204Theorem 7V(b)rankval4 9783  rankval4b 35237
[Enderton] p. 206Theorem 7X(b)en2lp 9519
[Enderton] p. 207Exercise 30rankpr 9773  rankprb 9767  rankpw 9759  rankpwi 9739  rankuniss 9782
[Enderton] p. 207Exercise 34opthreg 9531
[Enderton] p. 208Exercise 35suc11reg 9532
[Enderton] p. 212Definition of alephalephval3 10024
[Enderton] p. 213Theorem 8A(a)alephord2 9990
[Enderton] p. 213Theorem 8A(b)cardalephex 10004
[Enderton] p. 218Theorem Schema 8Eonfununi 8275
[Enderton] p. 222Definition of kardkarden 9811  kardex 9810
[Enderton] p. 238Theorem 8Roeoa 8527
[Enderton] p. 238Theorem 8Soeoe 8529
[Enderton] p. 240Exercise 25oarec 8491
[Enderton] p. 257Definition of cofinalitycflm 10164
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17569
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17511
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18480  mrieqv2d 17566  mrieqvd 17565
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17570
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17575  mreexexlem2d 17572
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18486  mreexfidimd 17577
[Frege1879] p. 11Statementdf3or2 44045
[Frege1879] p. 12Statementdf3an2 44046  dfxor4 44043  dfxor5 44044
[Frege1879] p. 26Axiom 1ax-frege1 44067
[Frege1879] p. 26Axiom 2ax-frege2 44068
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44072
[Frege1879] p. 31Proposition 4frege4 44076
[Frege1879] p. 32Proposition 5frege5 44077
[Frege1879] p. 33Proposition 6frege6 44083
[Frege1879] p. 34Proposition 7frege7 44085
[Frege1879] p. 35Axiom 8ax-frege8 44086  axfrege8 44084
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37621
[Frege1879] p. 35Proposition 9frege9 44089
[Frege1879] p. 36Proposition 10frege10 44097
[Frege1879] p. 36Proposition 11frege11 44091
[Frege1879] p. 37Proposition 12frege12 44090
[Frege1879] p. 37Proposition 13frege13 44099
[Frege1879] p. 37Proposition 14frege14 44100
[Frege1879] p. 38Proposition 15frege15 44103
[Frege1879] p. 38Proposition 16frege16 44093
[Frege1879] p. 39Proposition 17frege17 44098
[Frege1879] p. 39Proposition 18frege18 44095
[Frege1879] p. 39Proposition 19frege19 44101
[Frege1879] p. 40Proposition 20frege20 44105
[Frege1879] p. 40Proposition 21frege21 44104
[Frege1879] p. 41Proposition 22frege22 44096
[Frege1879] p. 42Proposition 23frege23 44102
[Frege1879] p. 42Proposition 24frege24 44092
[Frege1879] p. 42Proposition 25frege25 44094  rp-frege25 44082
[Frege1879] p. 42Proposition 26frege26 44087
[Frege1879] p. 43Axiom 28ax-frege28 44107
[Frege1879] p. 43Proposition 27frege27 44088
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 44108
[Frege1879] p. 44Axiom 31ax-frege31 44111  axfrege31 44110
[Frege1879] p. 44Proposition 30frege30 44109
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 44112
[Frege1879] p. 44Proposition 33frege33 44113
[Frege1879] p. 45Proposition 34frege34 44114
[Frege1879] p. 45Proposition 35frege35 44115
[Frege1879] p. 45Proposition 36frege36 44116
[Frege1879] p. 46Proposition 37frege37 44117
[Frege1879] p. 46Proposition 38frege38 44118
[Frege1879] p. 46Proposition 39frege39 44119
[Frege1879] p. 46Proposition 40frege40 44120
[Frege1879] p. 47Axiom 41ax-frege41 44122  axfrege41 44121
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 44123
[Frege1879] p. 47Proposition 43frege43 44124
[Frege1879] p. 47Proposition 44frege44 44125
[Frege1879] p. 47Proposition 45frege45 44126
[Frege1879] p. 48Proposition 46frege46 44127
[Frege1879] p. 48Proposition 47frege47 44128
[Frege1879] p. 49Proposition 48frege48 44129
[Frege1879] p. 49Proposition 49frege49 44130
[Frege1879] p. 49Proposition 50frege50 44131
[Frege1879] p. 50Axiom 52ax-frege52a 44134  ax-frege52c 44165  frege52aid 44135  frege52b 44166
[Frege1879] p. 50Axiom 54ax-frege54a 44139  ax-frege54c 44169  frege54b 44170
[Frege1879] p. 50Proposition 51frege51 44132
[Frege1879] p. 50Proposition 52dfsbcq 3743
[Frege1879] p. 50Proposition 53frege53a 44137  frege53aid 44136  frege53b 44167  frege53c 44191
[Frege1879] p. 50Proposition 54biid 261  eqid 2737
[Frege1879] p. 50Proposition 55frege55a 44145  frege55aid 44142  frege55b 44174  frege55c 44195  frege55cor1a 44146  frege55lem2a 44144  frege55lem2b 44173  frege55lem2c 44194
[Frege1879] p. 50Proposition 56frege56a 44148  frege56aid 44147  frege56b 44175  frege56c 44196
[Frege1879] p. 51Axiom 58ax-frege58a 44152  ax-frege58b 44178  frege58bid 44179  frege58c 44198
[Frege1879] p. 51Proposition 57frege57a 44150  frege57aid 44149  frege57b 44176  frege57c 44197
[Frege1879] p. 51Proposition 58spsbc 3754
[Frege1879] p. 51Proposition 59frege59a 44154  frege59b 44181  frege59c 44199
[Frege1879] p. 52Proposition 60frege60a 44155  frege60b 44182  frege60c 44200
[Frege1879] p. 52Proposition 61frege61a 44156  frege61b 44183  frege61c 44201
[Frege1879] p. 52Proposition 62frege62a 44157  frege62b 44184  frege62c 44202
[Frege1879] p. 52Proposition 63frege63a 44158  frege63b 44185  frege63c 44203
[Frege1879] p. 53Proposition 64frege64a 44159  frege64b 44186  frege64c 44204
[Frege1879] p. 53Proposition 65frege65a 44160  frege65b 44187  frege65c 44205
[Frege1879] p. 54Proposition 66frege66a 44161  frege66b 44188  frege66c 44206
[Frege1879] p. 54Proposition 67frege67a 44162  frege67b 44189  frege67c 44207
[Frege1879] p. 54Proposition 68frege68a 44163  frege68b 44190  frege68c 44208
[Frege1879] p. 55Definition 69dffrege69 44209
[Frege1879] p. 58Proposition 70frege70 44210
[Frege1879] p. 59Proposition 71frege71 44211
[Frege1879] p. 59Proposition 72frege72 44212
[Frege1879] p. 59Proposition 73frege73 44213
[Frege1879] p. 60Definition 76dffrege76 44216
[Frege1879] p. 60Proposition 74frege74 44214
[Frege1879] p. 60Proposition 75frege75 44215
[Frege1879] p. 62Proposition 77frege77 44217  frege77d 44023
[Frege1879] p. 63Proposition 78frege78 44218
[Frege1879] p. 63Proposition 79frege79 44219
[Frege1879] p. 63Proposition 80frege80 44220
[Frege1879] p. 63Proposition 81frege81 44221  frege81d 44024
[Frege1879] p. 64Proposition 82frege82 44222
[Frege1879] p. 65Proposition 83frege83 44223  frege83d 44025
[Frege1879] p. 65Proposition 84frege84 44224
[Frege1879] p. 66Proposition 85frege85 44225
[Frege1879] p. 66Proposition 86frege86 44226
[Frege1879] p. 66Proposition 87frege87 44227  frege87d 44027
[Frege1879] p. 67Proposition 88frege88 44228
[Frege1879] p. 68Proposition 89frege89 44229
[Frege1879] p. 68Proposition 90frege90 44230
[Frege1879] p. 68Proposition 91frege91 44231  frege91d 44028
[Frege1879] p. 69Proposition 92frege92 44232
[Frege1879] p. 70Proposition 93frege93 44233
[Frege1879] p. 70Proposition 94frege94 44234
[Frege1879] p. 70Proposition 95frege95 44235
[Frege1879] p. 71Definition 99dffrege99 44239
[Frege1879] p. 71Proposition 96frege96 44236  frege96d 44026
[Frege1879] p. 71Proposition 97frege97 44237  frege97d 44029
[Frege1879] p. 71Proposition 98frege98 44238  frege98d 44030
[Frege1879] p. 72Proposition 100frege100 44240
[Frege1879] p. 72Proposition 101frege101 44241
[Frege1879] p. 72Proposition 102frege102 44242  frege102d 44031
[Frege1879] p. 73Proposition 103frege103 44243
[Frege1879] p. 73Proposition 104frege104 44244
[Frege1879] p. 73Proposition 105frege105 44245
[Frege1879] p. 73Proposition 106frege106 44246  frege106d 44032
[Frege1879] p. 74Proposition 107frege107 44247
[Frege1879] p. 74Proposition 108frege108 44248  frege108d 44033
[Frege1879] p. 74Proposition 109frege109 44249  frege109d 44034
[Frege1879] p. 75Proposition 110frege110 44250
[Frege1879] p. 75Proposition 111frege111 44251  frege111d 44036
[Frege1879] p. 76Proposition 112frege112 44252
[Frege1879] p. 76Proposition 113frege113 44253
[Frege1879] p. 76Proposition 114frege114 44254  frege114d 44035
[Frege1879] p. 77Definition 115dffrege115 44255
[Frege1879] p. 77Proposition 116frege116 44256
[Frege1879] p. 78Proposition 117frege117 44257
[Frege1879] p. 78Proposition 118frege118 44258
[Frege1879] p. 78Proposition 119frege119 44259
[Frege1879] p. 78Proposition 120frege120 44260
[Frege1879] p. 79Proposition 121frege121 44261
[Frege1879] p. 79Proposition 122frege122 44262  frege122d 44037
[Frege1879] p. 79Proposition 123frege123 44263
[Frege1879] p. 80Proposition 124frege124 44264  frege124d 44038
[Frege1879] p. 81Proposition 125frege125 44265
[Frege1879] p. 81Proposition 126frege126 44266  frege126d 44039
[Frege1879] p. 82Proposition 127frege127 44267
[Frege1879] p. 83Proposition 128frege128 44268
[Frege1879] p. 83Proposition 129frege129 44269  frege129d 44040
[Frege1879] p. 84Proposition 130frege130 44270
[Frege1879] p. 85Proposition 131frege131 44271  frege131d 44041
[Frege1879] p. 86Proposition 132frege132 44272
[Frege1879] p. 86Proposition 133frege133 44273  frege133d 44042
[Fremlin1] p. 13Definition 111G (b)df-salgen 46593
[Fremlin1] p. 13Definition 111G (d)borelmbl 46916
[Fremlin1] p. 13Proposition 111G (b)salgenss 46616
[Fremlin1] p. 14Definition 112Aismea 46731
[Fremlin1] p. 15Remark 112B (d)psmeasure 46751
[Fremlin1] p. 15Property 112C (a)meadjun 46742  meadjunre 46756
[Fremlin1] p. 15Property 112C (b)meassle 46743
[Fremlin1] p. 15Property 112C (c)meaunle 46744
[Fremlin1] p. 16Property 112C (d)iundjiun 46740  meaiunle 46749  meaiunlelem 46748
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46761  meaiuninc2 46762  meaiuninc3 46765  meaiuninc3v 46764  meaiunincf 46763  meaiuninclem 46760
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46767  meaiininc2 46768  meaiininclem 46766
[Fremlin1] p. 19Theorem 113Ccaragen0 46786  caragendifcl 46794  caratheodory 46808  omelesplit 46798
[Fremlin1] p. 19Definition 113Aisome 46774  isomennd 46811  isomenndlem 46810
[Fremlin1] p. 19Remark 113B (c)omeunle 46796
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46815  voncmpl 46901
[Fremlin1] p. 19Definition 113A (ii)omessle 46778
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46803  carageniuncllem1 46801  carageniuncllem2 46802  caragenuncl 46793  caragenuncllem 46792  caragenunicl 46804
[Fremlin1] p. 21Remark 113Dcaragenel2d 46812
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46806  caratheodorylem2 46807
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46815
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46874  hoidmv1lelem1 46871  hoidmv1lelem2 46872  hoidmv1lelem3 46873
[Fremlin1] p. 25Definition 114Eisvonmbl 46918
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46874  hoidmvle 46880  hoidmvlelem1 46875  hoidmvlelem2 46876  hoidmvlelem3 46877  hoidmvlelem4 46878  hoidmvlelem5 46879  hsphoidmvle2 46865  hsphoif 46856  hsphoival 46859
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46828
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46836
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46863  hoidmvn0val 46864  hoidmvval 46857  hoidmvval0 46867  hoidmvval0b 46870
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46868  hsphoidmvle 46866
[Fremlin1] p. 30Definition 115Cdf-ovoln 46817  df-voln 46819
[Fremlin1] p. 30Proposition 115D (a)dmovn 46884  ovn0 46846  ovn0lem 46845  ovnf 46843  ovnome 46853  ovnssle 46841  ovnsslelem 46840  ovnsupge0 46837
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46883  ovnhoilem1 46881  ovnhoilem2 46882  vonhoi 46947
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46900  hoidifhspf 46898  hoidifhspval 46888  hoidifhspval2 46895  hoidifhspval3 46899  hspmbl 46909  hspmbllem1 46906  hspmbllem2 46907  hspmbllem3 46908
[Fremlin1] p. 31Definition 115Evoncmpl 46901  vonmea 46854
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46852  ovnsubadd2 46926  ovnsubadd2lem 46925  ovnsubaddlem1 46850  ovnsubaddlem2 46851
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46911  hoimbl2 46945  hoimbllem 46910  hspdifhsp 46896  opnvonmbl 46914  opnvonmbllem2 46913
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46916
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46959  iccvonmbllem 46958  ioovonmbl 46957
[Fremlin1] p. 32Proposition 115G (d)vonicc 46965  vonicclem2 46964  vonioo 46962  vonioolem2 46961  vonn0icc 46968  vonn0icc2 46972  vonn0ioo 46967  vonn0ioo2 46970
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46969  snvonmbl 46966  vonct 46973  vonsn 46971
[Fremlin1] p. 35Lemma 121Asubsalsal 46639
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46638  subsaliuncllem 46637
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47005  salpreimalegt 46989  salpreimaltle 47006
[Fremlin1] p. 35Proposition 121B (i)issmf 47008  issmff 47014  issmflem 47007
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47025  issmflelem 47024  smfpreimale 47034
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47036  issmfgtlem 47035
[Fremlin1] p. 36Definition 121Cdf-smblfn 46976  issmf 47008  issmff 47014  issmfge 47050  issmfgelem 47049  issmfgt 47036  issmfgtlem 47035  issmfle 47025  issmflelem 47024  issmflem 47007
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46987  salpreimagtlt 47010  salpreimalelt 47009
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47050  issmfgelem 47049
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47033
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47031  cnfsmf 47020
[Fremlin1] p. 36Proposition 121D (c)decsmf 47047  decsmflem 47046  incsmf 47022  incsmflem 47021
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46981  pimconstlt1 46982  smfconst 47029
[Fremlin1] p. 37Proposition 121E (b)smfadd 47045  smfaddlem1 47043  smfaddlem2 47044
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47076
[Fremlin1] p. 37Proposition 121E (d)smfmul 47075  smfmullem1 47071  smfmullem2 47072  smfmullem3 47073  smfmullem4 47074
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47077
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47080  smfpimbor1lem2 47079
[Fremlin1] p. 37Proposition 121E (g)smfco 47082
[Fremlin1] p. 37Proposition 121E (h)smfres 47070
[Fremlin1] p. 38Proposition 121E (e)smfrec 47069
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47078  smfresal 47068
[Fremlin1] p. 38Proposition 121F (a)smflim 47057  smflim2 47086  smflimlem1 47051  smflimlem2 47052  smflimlem3 47053  smflimlem4 47054  smflimlem5 47055  smflimlem6 47056  smflimmpt 47090
[Fremlin1] p. 38Proposition 121F (b)smfsup 47094  smfsuplem1 47091  smfsuplem2 47092  smfsuplem3 47093  smfsupmpt 47095  smfsupxr 47096
[Fremlin1] p. 38Proposition 121F (c)smfinf 47098  smfinflem 47097  smfinfmpt 47099
[Fremlin1] p. 39Remark 121Gsmflim 47057  smflim2 47086  smflimmpt 47090
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47088
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47118  smfdivdmmbl2 47121  smfinfdmmbl 47129  smfinfdmmbllem 47128  smfsupdmmbl 47125  smfsupdmmbllem 47124
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47108  smflimsuplem2 47101  smflimsuplem6 47105  smflimsuplem7 47106  smflimsuplem8 47107  smflimsupmpt 47109
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47111  smfliminflem 47110  smfliminfmpt 47112
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46976
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47122  fsupdm2 47123
[Fremlin1], p. 39Proposition 121Hadddmmbl 47113  adddmmbl2 47114  finfdm 47126  finfdm2 47127  fsupdm 47122  fsupdm2 47123  muldmmbl 47115  muldmmbl2 47116
[Fremlin1], p. 39Proposition 121F (c)finfdm 47126  finfdm2 47127
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25497
[Fremlin5] p. 213Lemma 565Cauniioovol 25540
[Fremlin5] p. 214Lemma 565Cauniioombl 25550
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37870
[Fremlin5] p. 220Theorem 565Maftc1anc 37873
[FreydScedrov] p. 283Axiom of Infinityax-inf 9551  inf1 9535  inf2 9536
[Gleason] p. 117Proposition 9-2.1df-enq 10826  enqer 10836
[Gleason] p. 117Proposition 9-2.2df-1nq 10831  df-nq 10827
[Gleason] p. 117Proposition 9-2.3df-plpq 10823  df-plq 10829
[Gleason] p. 119Proposition 9-2.4caovmo 7597  df-mpq 10824  df-mq 10830
[Gleason] p. 119Proposition 9-2.5df-rq 10832
[Gleason] p. 119Proposition 9-2.6ltexnq 10890
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10891  ltbtwnnq 10893
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10886
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10887
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10894
[Gleason] p. 121Definition 9-3.1df-np 10896
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10908
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10910
[Gleason] p. 122Definitiondf-1p 10897
[Gleason] p. 122Remark (1)prub 10909
[Gleason] p. 122Lemma 9-3.4prlem934 10948
[Gleason] p. 122Proposition 9-3.2df-ltp 10900
[Gleason] p. 122Proposition 9-3.3ltsopr 10947  psslinpr 10946  supexpr 10969  suplem1pr 10967  suplem2pr 10968
[Gleason] p. 123Proposition 9-3.5addclpr 10933  addclprlem1 10931  addclprlem2 10932  df-plp 10898
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10937
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10936
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10949
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10958  ltexprlem1 10951  ltexprlem2 10952  ltexprlem3 10953  ltexprlem4 10954  ltexprlem5 10955  ltexprlem6 10956  ltexprlem7 10957
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10960  ltaprlem 10959
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10961
[Gleason] p. 124Lemma 9-3.6prlem936 10962
[Gleason] p. 124Proposition 9-3.7df-mp 10899  mulclpr 10935  mulclprlem 10934  reclem2pr 10963
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10944
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10939
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10938
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10943
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10966  reclem3pr 10964  reclem4pr 10965
[Gleason] p. 126Proposition 9-4.1df-enr 10970  enrer 10978
[Gleason] p. 126Proposition 9-4.2df-0r 10975  df-1r 10976  df-nr 10971
[Gleason] p. 126Proposition 9-4.3df-mr 10973  df-plr 10972  negexsr 11017  recexsr 11022  recexsrlem 11018
[Gleason] p. 127Proposition 9-4.4df-ltr 10974
[Gleason] p. 130Proposition 10-1.3creui 12144  creur 12143  cru 12141
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11103  axcnre 11079
[Gleason] p. 132Definition 10-3.1crim 15042  crimd 15159  crimi 15120  crre 15041  crred 15158  crrei 15119
[Gleason] p. 132Definition 10-3.2remim 15044  remimd 15125
[Gleason] p. 133Definition 10.36absval2 15211  absval2d 15375  absval2i 15325
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15068  cjaddd 15147  cjaddi 15115
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15069  cjmuld 15148  cjmuli 15116
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15067  cjcjd 15126  cjcji 15098
[Gleason] p. 133Proposition 10-3.4(f)cjre 15066  cjreb 15050  cjrebd 15129  cjrebi 15101  cjred 15153  rere 15049  rereb 15047  rerebd 15128  rerebi 15100  rered 15151
[Gleason] p. 133Proposition 10-3.4(h)addcj 15075  addcjd 15139  addcji 15110
[Gleason] p. 133Proposition 10-3.7(a)absval 15165
[Gleason] p. 133Proposition 10-3.7(b)abscj 15206  abscjd 15380  abscji 15329
[Gleason] p. 133Proposition 10-3.7(c)abs00 15216  abs00d 15376  abs00i 15326  absne0d 15377
[Gleason] p. 133Proposition 10-3.7(d)releabs 15249  releabsd 15381  releabsi 15330
[Gleason] p. 133Proposition 10-3.7(f)absmul 15221  absmuld 15384  absmuli 15332
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15209  sqabsaddi 15333
[Gleason] p. 133Proposition 10-3.7(h)abstri 15258  abstrid 15386  abstrii 15336
[Gleason] p. 134Definition 10-4.1df-exp 13989  exp0 13992  expp1 13995  expp1d 14074
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26648  cxpaddd 26686  expadd 14031  expaddd 14075  expaddz 14033
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26657  cxpmuld 26706  expmul 14034  expmuld 14076  expmulz 14035
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26654  mulcxpd 26697  mulexp 14028  mulexpd 14088  mulexpz 14029
[Gleason] p. 140Exercise 1znnen 16141
[Gleason] p. 141Definition 11-2.1fzval 13429
[Gleason] p. 168Proposition 12-2.1(a)climadd 15559  rlimadd 15570  rlimdiv 15573
[Gleason] p. 168Proposition 12-2.1(b)climsub 15561  rlimsub 15571
[Gleason] p. 168Proposition 12-2.1(c)climmul 15560  rlimmul 15572
[Gleason] p. 171Corollary 12-2.2climmulc2 15564
[Gleason] p. 172Corollary 12-2.5climrecl 15510
[Gleason] p. 172Proposition 12-2.4(c)climabs 15531  climcj 15532  climim 15534  climre 15533  rlimabs 15536  rlimcj 15537  rlimim 15539  rlimre 15538
[Gleason] p. 173Definition 12-3.1df-ltxr 11175  df-xr 11174  ltxr 13033
[Gleason] p. 175Definition 12-4.1df-limsup 15398  limsupval 15401
[Gleason] p. 180Theorem 12-5.1climsup 15597
[Gleason] p. 180Theorem 12-5.3caucvg 15606  caucvgb 15607  caucvgbf 45769  caucvgr 15603  climcau 15598
[Gleason] p. 182Exercise 3cvgcmp 15743
[Gleason] p. 182Exercise 4cvgrat 15810
[Gleason] p. 195Theorem 13-2.12abs1m 15263
[Gleason] p. 217Lemma 13-4.1btwnzge0 13752
[Gleason] p. 223Definition 14-1.1df-met 21307
[Gleason] p. 223Definition 14-1.1(a)met0 24291  xmet0 24290
[Gleason] p. 223Definition 14-1.1(b)metgt0 24307
[Gleason] p. 223Definition 14-1.1(c)metsym 24298
[Gleason] p. 223Definition 14-1.1(d)mettri 24300  mstri 24417  xmettri 24299  xmstri 24416
[Gleason] p. 225Definition 14-1.5xpsmet 24330
[Gleason] p. 230Proposition 14-2.6txlm 23596
[Gleason] p. 240Theorem 14-4.3metcnp4 25270
[Gleason] p. 240Proposition 14-4.2metcnp3 24488
[Gleason] p. 243Proposition 14-4.16addcn 24814  addcn2 15521  mulcn 24816  mulcn2 15523  subcn 24815  subcn2 15522
[Gleason] p. 295Remarkbcval3 14233  bcval4 14234
[Gleason] p. 295Equation 2bcpasc 14248
[Gleason] p. 295Definition of binomial coefficientbcval 14231  df-bc 14230
[Gleason] p. 296Remarkbcn0 14237  bcnn 14239
[Gleason] p. 296Theorem 15-2.8binom 15757
[Gleason] p. 308Equation 2ef0 16018
[Gleason] p. 308Equation 3efcj 16019
[Gleason] p. 309Corollary 15-4.3efne0 16025
[Gleason] p. 309Corollary 15-4.4efexp 16030
[Gleason] p. 310Equation 14sinadd 16093
[Gleason] p. 310Equation 15cosadd 16094
[Gleason] p. 311Equation 17sincossq 16105
[Gleason] p. 311Equation 18cosbnd 16110  sinbnd 16109
[Gleason] p. 311Lemma 15-4.7sqeqor 14143  sqeqori 14141
[Gleason] p. 311Definition of ` `df-pi 15999
[Godowski] p. 730Equation SFgoeqi 32331
[GodowskiGreechie] p. 249Equation IV3oai 31726
[Golan] p. 1Remarksrgisid 20148
[Golan] p. 1Definitiondf-srg 20126
[Golan] p. 149Definitiondf-slmd 33264
[Gonshor] p. 7Definitiondf-scut 27760
[Gonshor] p. 9Theorem 2.5slerec 27797  slerecd 27798
[Gonshor] p. 10Theorem 2.6cofcut1 27902  cofcut1d 27903
[Gonshor] p. 10Theorem 2.7cofcut2 27904  cofcut2d 27905
[Gonshor] p. 12Theorem 2.9cofcutr 27906  cofcutr1d 27907  cofcutr2d 27908
[Gonshor] p. 13Definitiondf-adds 27942
[Gonshor] p. 14Theorem 3.1addsprop 27958
[Gonshor] p. 15Theorem 3.2addsunif 27984
[Gonshor] p. 17Theorem 3.4mulsprop 28112
[Gonshor] p. 18Theorem 3.5mulsunif 28132
[Gonshor] p. 28Lemma 4.2halfcut 28437
[Gonshor] p. 28Theorem 4.2pw2cut 28439
[Gonshor] p. 30Theorem 4.2addhalfcut 28438
[Gonshor] p. 39Theorem 4.4(b)elreno2 28474
[Gonshor] p. 95Theorem 6.1addsbday 28000
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36334
[Gratzer] p. 23Section 0.6df-mre 17509
[Gratzer] p. 27Section 0.6df-mri 17511
[Hall] p. 1Section 1.1df-asslaw 48470  df-cllaw 48468  df-comlaw 48469
[Hall] p. 2Section 1.2df-clintop 48482
[Hall] p. 7Section 1.3df-sgrp2 48503
[Halmos] p. 28Partition ` `df-parts 39040  dfmembpart2 39045
[Halmos] p. 31Theorem 17.3riesz1 32123  riesz2 32124
[Halmos] p. 41Definition of Hermitianhmopadj2 31999
[Halmos] p. 42Definition of projector orderingpjordi 32231
[Halmos] p. 43Theorem 26.1elpjhmop 32243  elpjidm 32242  pjnmopi 32206
[Halmos] p. 44Remarkpjinormi 31745  pjinormii 31734
[Halmos] p. 44Theorem 26.2elpjch 32247  pjrn 31765  pjrni 31760  pjvec 31754
[Halmos] p. 44Theorem 26.3pjnorm2 31785
[Halmos] p. 44Theorem 26.4hmopidmpj 32212  hmopidmpji 32210
[Halmos] p. 45Theorem 27.1pjinvari 32249
[Halmos] p. 45Theorem 27.3pjoci 32238  pjocvec 31755
[Halmos] p. 45Theorem 27.4pjorthcoi 32227
[Halmos] p. 48Theorem 29.2pjssposi 32230
[Halmos] p. 48Theorem 29.3pjssdif1i 32233  pjssdif2i 32232
[Halmos] p. 50Definition of spectrumdf-spec 31913
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1797
[Hatcher] p. 25Definitiondf-phtpc 24951  df-phtpy 24930
[Hatcher] p. 26Definitiondf-pco 24965  df-pi1 24968
[Hatcher] p. 26Proposition 1.2phtpcer 24954
[Hatcher] p. 26Proposition 1.3pi1grp 25010
[Hefferon] p. 240Definition 3.12df-dmat 22438  df-dmatalt 48680
[Helfgott] p. 2Theoremtgoldbach 48099
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48084
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48096  bgoldbtbnd 48091  bgoldbtbnd 48091  tgblthelfgott 48097
[Helfgott] p. 5Proposition 1.1circlevma 34780
[Helfgott] p. 69Statement 7.49circlemethhgt 34781
[Helfgott] p. 69Statement 7.50hgt750lema 34795  hgt750lemb 34794  hgt750leme 34796  hgt750lemf 34791  hgt750lemg 34792
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48093  tgoldbachgt 34801  tgoldbachgtALTV 48094  tgoldbachgtd 34800
[Helfgott] p. 70Statement 7.49ax-hgt749 34782
[Herstein] p. 54Exercise 28df-grpo 30551
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18878  grpoideu 30567  mndideu 18674
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18908  grpoinveu 30577
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18939  grpo2inv 30589
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18952  grpoinvop 30591
[Herstein] p. 57Exercise 1dfgrp3e 18974
[Hitchcock] p. 5Rule A3mptnan 1770
[Hitchcock] p. 5Rule A4mptxor 1771
[Hitchcock] p. 5Rule A5mtpxor 1773
[Holland] p. 1519Theorem 2sumdmdi 32478
[Holland] p. 1520Lemma 5cdj1i 32491  cdj3i 32499  cdj3lem1 32492  cdjreui 32490
[Holland] p. 1524Lemma 7mddmdin0i 32489
[Holland95] p. 13Theorem 3.6hlathil 42258
[Holland95] p. 14Line 15hgmapvs 42188
[Holland95] p. 14Line 16hdmaplkr 42210
[Holland95] p. 14Line 17hdmapellkr 42211
[Holland95] p. 14Line 19hdmapglnm2 42208
[Holland95] p. 14Line 20hdmapip0com 42214
[Holland95] p. 14Theorem 3.6hdmapevec2 42133
[Holland95] p. 14Lines 24 and 25hdmapoc 42228
[Holland95] p. 204Definition of involutiondf-srng 20777
[Holland95] p. 212Definition of subspacedf-psubsp 39800
[Holland95] p. 214Lemma 3.3lclkrlem2v 41825
[Holland95] p. 214Definition 3.2df-lpolN 41778
[Holland95] p. 214Definition of nonsingularpnonsingN 40230
[Holland95] p. 215Lemma 3.3(1)dihoml4 41674  poml4N 40250
[Holland95] p. 215Lemma 3.3(2)dochexmid 41765  pexmidALTN 40275  pexmidN 40266
[Holland95] p. 218Theorem 3.6lclkr 41830
[Holland95] p. 218Definition of dual vector spacedf-ldual 39421  ldualset 39422
[Holland95] p. 222Item 1df-lines 39798  df-pointsN 39799
[Holland95] p. 222Item 2df-polarityN 40200
[Holland95] p. 223Remarkispsubcl2N 40244  omllaw4 39543  pol1N 40207  polcon3N 40214
[Holland95] p. 223Definitiondf-psubclN 40232
[Holland95] p. 223Equation for polaritypolval2N 40203
[Holmes] p. 40Definitiondf-xrn 38552
[Hughes] p. 44Equation 1.21bax-his3 31142
[Hughes] p. 47Definition of projection operatordfpjop 32240
[Hughes] p. 49Equation 1.30eighmre 32021  eigre 31893  eigrei 31892
[Hughes] p. 49Equation 1.31eighmorth 32022  eigorth 31896  eigorthi 31895
[Hughes] p. 137Remark (ii)eigposi 31894
[Huneke] p. 1Claim 1frgrncvvdeq 30367
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30363
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30364
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30365
[Huneke] p. 2Claim 2frgrregorufr 30383  frgrregorufr0 30382  frgrregorufrg 30384
[Huneke] p. 2Claim 3frgrhash2wsp 30390  frrusgrord 30399  frrusgrord0 30398
[Huneke] p. 2Statementdf-clwwlknon 30146
[Huneke] p. 2Statement 4frgrwopreglem4 30373
[Huneke] p. 2Statement 5frgrwopreg1 30376  frgrwopreg2 30377  frgrwopregasn 30374  frgrwopregbsn 30375
[Huneke] p. 2Statement 6frgrwopreglem5 30379
[Huneke] p. 2Statement 7fusgreghash2wspv 30393
[Huneke] p. 2Statement 8fusgreghash2wsp 30396
[Huneke] p. 2Statement 9clwlksndivn 30144  numclwlk1 30429  numclwlk1lem1 30427  numclwlk1lem2 30428  numclwwlk1 30419  numclwwlk8 30450
[Huneke] p. 2Definition 3frgrwopreglem1 30370
[Huneke] p. 2Definition 4df-clwlks 29827
[Huneke] p. 2Definition 62clwwlk 30405
[Huneke] p. 2Definition 7numclwwlkovh 30431  numclwwlkovh0 30430
[Huneke] p. 2Statement 10numclwwlk2 30439
[Huneke] p. 2Statement 11rusgrnumwlkg 30036
[Huneke] p. 2Statement 12numclwwlk3 30443
[Huneke] p. 2Statement 13numclwwlk5 30446
[Huneke] p. 2Statement 14numclwwlk7 30449
[Indrzejczak] p. 33Definition ` `Enatded 30461  natded 30461
[Indrzejczak] p. 33Definition ` `Inatded 30461
[Indrzejczak] p. 34Definition ` `Enatded 30461  natded 30461
[Indrzejczak] p. 34Definition ` `Inatded 30461
[Jech] p. 4Definition of classcv 1541  cvjust 2731
[Jech] p. 42Lemma 6.1alephexp1 10494
[Jech] p. 42Equation 6.1alephadd 10492  alephmul 10493
[Jech] p. 43Lemma 6.2infmap 10491  infmap2 10131
[Jech] p. 71Lemma 9.3jech9.3 9730
[Jech] p. 72Equation 9.3scott0 9802  scottex 9801
[Jech] p. 72Exercise 9.1rankval4 9783  rankval4b 35237
[Jech] p. 72Scheme "Collection Principle"cp 9807
[Jech] p. 78Noteopthprc 5689
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43193
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43281
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43282
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43205
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43209
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43210  rmyp1 43211
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43212  rmym1 43213
[JonesMatijasevic] p. 695Equation 2.11rmx0 43203  rmx1 43204  rmxluc 43214
[JonesMatijasevic] p. 695Equation 2.12rmy0 43207  rmy1 43208  rmyluc 43215
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43217
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43218
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43238  jm2.17b 43239  jm2.17c 43240
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43271
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43275
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43266
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43241  jm2.24nn 43237
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43280
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43286  rmygeid 43242
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43298
[Juillerat] p. 11Section *5etransc 46563  etransclem47 46561  etransclem48 46562
[Juillerat] p. 12Equation (7)etransclem44 46558
[Juillerat] p. 12Equation *(7)etransclem46 46560
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46546
[Juillerat] p. 13Proofetransclem35 46549
[Juillerat] p. 13Part of case 2 proven inetransclem38 46552
[Juillerat] p. 13Part of case 2 provenetransclem24 46538
[Juillerat] p. 13Part of case 2: proven inetransclem41 46555
[Juillerat] p. 14Proofetransclem23 46537
[KalishMontague] p. 81Note 1ax-6 1969
[KalishMontague] p. 85Lemma 2equid 2014
[KalishMontague] p. 85Lemma 3equcomi 2019
[KalishMontague] p. 86Lemma 7cbvalivw 2009  cbvaliw 2008  wl-cbvmotv 37689  wl-motae 37691  wl-moteq 37690
[KalishMontague] p. 87Lemma 8spimvw 1988  spimw 1972
[KalishMontague] p. 87Lemma 9spfw 2035  spw 2036
[Kalmbach] p. 14Definition of latticechabs1 31574  chabs1i 31576  chabs2 31575  chabs2i 31577  chjass 31591  chjassi 31544  latabs1 18402  latabs2 18403
[Kalmbach] p. 15Definition of atomdf-at 32396  ela 32397
[Kalmbach] p. 15Definition of coverscvbr2 32341  cvrval2 39571
[Kalmbach] p. 16Definitiondf-ol 39475  df-oml 39476
[Kalmbach] p. 20Definition of commutescmbr 31642  cmbri 31648  cmtvalN 39508  df-cm 31641  df-cmtN 39474
[Kalmbach] p. 22Remarkomllaw5N 39544  pjoml5 31671  pjoml5i 31646
[Kalmbach] p. 22Definitionpjoml2 31669  pjoml2i 31643
[Kalmbach] p. 22Theorem 2(v)cmcm 31672  cmcmi 31650  cmcmii 31655  cmtcomN 39546
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39542  omlsi 31462  pjoml 31494  pjomli 31493
[Kalmbach] p. 22Definition of OML lawomllaw2N 39541
[Kalmbach] p. 23Remarkcmbr2i 31654  cmcm3 31673  cmcm3i 31652  cmcm3ii 31657  cmcm4i 31653  cmt3N 39548  cmt4N 39549  cmtbr2N 39550
[Kalmbach] p. 23Lemma 3cmbr3 31666  cmbr3i 31658  cmtbr3N 39551
[Kalmbach] p. 25Theorem 5fh1 31676  fh1i 31679  fh2 31677  fh2i 31680  omlfh1N 39555
[Kalmbach] p. 65Remarkchjatom 32415  chslej 31556  chsleji 31516  shslej 31438  shsleji 31428
[Kalmbach] p. 65Proposition 1chocin 31553  chocini 31512  chsupcl 31398  chsupval2 31468  h0elch 31313  helch 31301  hsupval2 31467  ocin 31354  ococss 31351  shococss 31352
[Kalmbach] p. 65Definition of subspace sumshsval 31370
[Kalmbach] p. 66Remarkdf-pjh 31453  pjssmi 32223  pjssmii 31739
[Kalmbach] p. 67Lemma 3osum 31703  osumi 31700
[Kalmbach] p. 67Lemma 4pjci 32258
[Kalmbach] p. 103Exercise 6atmd2 32458
[Kalmbach] p. 103Exercise 12mdsl0 32368
[Kalmbach] p. 140Remarkhatomic 32418  hatomici 32417  hatomistici 32420
[Kalmbach] p. 140Proposition 1atlatmstc 39616
[Kalmbach] p. 140Proposition 1(i)atexch 32439  lsatexch 39340
[Kalmbach] p. 140Proposition 1(ii)chcv1 32413  cvlcvr1 39636  cvr1 39707
[Kalmbach] p. 140Proposition 1(iii)cvexch 32432  cvexchi 32427  cvrexch 39717
[Kalmbach] p. 149Remark 2chrelati 32422  hlrelat 39699  hlrelat5N 39698  lrelat 39311
[Kalmbach] p. 153Exercise 5lsmcv 21100  lsmsatcv 39307  spansncv 31711  spansncvi 31710
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39326  spansncv2 32351
[Kalmbach] p. 266Definitiondf-st 32269
[Kalmbach2] p. 8Definition of adjointdf-adjh 31907
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10561  fpwwe2 10558
[KanamoriPincus] p. 416Corollary 1.3canth4 10562
[KanamoriPincus] p. 417Corollary 1.6canthp1 10569
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10564
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10566
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10579
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10583  gchxpidm 10584
[KanamoriPincus] p. 419Theorem 2.1gchacg 10595  gchhar 10594
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10129  unxpwdom 9498
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10585
[Kreyszig] p. 3Property M1metcl 24280  xmetcl 24279
[Kreyszig] p. 4Property M2meteq0 24287
[Kreyszig] p. 8Definition 1.1-8dscmet 24520
[Kreyszig] p. 12Equation 5conjmul 11862  muleqadd 11785
[Kreyszig] p. 18Definition 1.3-2mopnval 24386
[Kreyszig] p. 19Remarkmopntopon 24387
[Kreyszig] p. 19Theorem T1mopn0 24446  mopnm 24392
[Kreyszig] p. 19Theorem T2unimopn 24444
[Kreyszig] p. 19Definition of neighborhoodneibl 24449
[Kreyszig] p. 20Definition 1.3-3metcnp2 24490
[Kreyszig] p. 25Definition 1.4-1lmbr 23206  lmmbr 25218  lmmbr2 25219
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23328
[Kreyszig] p. 28Theorem 1.4-5lmcau 25273
[Kreyszig] p. 28Definition 1.4-3iscau 25236  iscmet2 25254
[Kreyszig] p. 30Theorem 1.4-7cmetss 25276
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23409  metelcls 25265
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25266  metcld2 25267
[Kreyszig] p. 51Equation 2clmvneg1 25059  lmodvneg1 20860  nvinv 30697  vcm 30634
[Kreyszig] p. 51Equation 1aclm0vs 25055  lmod0vs 20850  slmd0vs 33287  vc0 30632
[Kreyszig] p. 51Equation 1blmodvs0 20851  slmdvs0 33288  vcz 30633
[Kreyszig] p. 58Definition 2.2-1imsmet 30749  ngpmet 24551  nrmmetd 24522
[Kreyszig] p. 59Equation 1imsdval 30744  imsdval2 30745  ncvspds 25121  ngpds 24552
[Kreyszig] p. 63Problem 1nmval 24537  nvnd 30746
[Kreyszig] p. 64Problem 2nmeq0 24566  nmge0 24565  nvge0 30731  nvz 30727
[Kreyszig] p. 64Problem 3nmrtri 24572  nvabs 30730
[Kreyszig] p. 91Definition 2.7-1isblo3i 30859
[Kreyszig] p. 92Equation 2df-nmoo 30803
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30865  blocni 30863
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30864
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25164  ipeq0 21597  ipz 30777
[Kreyszig] p. 135Problem 2cphpyth 25176  pythi 30908
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30912
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25198
[Kreyszig] p. 144Equation 4supcvg 15783
[Kreyszig] p. 144Theorem 3.3-1minvec 25396  minveco 30942
[Kreyszig] p. 196Definition 3.9-1df-aj 30808
[Kreyszig] p. 247Theorem 4.7-2bcth 25289
[Kreyszig] p. 249Theorem 4.7-3ubth 30931
[Kreyszig] p. 470Definition of positive operator orderingleop 32181  leopg 32180
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32199
[Kreyszig] p. 525Theorem 10.1-1htth 30976
[Kulpa] p. 547Theorempoimir 37825
[Kulpa] p. 547Equation (1)poimirlem32 37824
[Kulpa] p. 547Equation (2)poimirlem31 37823
[Kulpa] p. 548Theorembroucube 37826
[Kulpa] p. 548Equation (6)poimirlem26 37818
[Kulpa] p. 548Equation (7)poimirlem27 37819
[Kunen] p. 10Axiom 0ax6e 2388  axnul 5251
[Kunen] p. 11Axiom 3axnul 5251
[Kunen] p. 12Axiom 6zfrep6 7901
[Kunen] p. 24Definition 10.24mapval 8779  mapvalg 8777
[Kunen] p. 30Lemma 10.20fodomg 10436
[Kunen] p. 31Definition 10.24mapex 7885
[Kunen] p. 95Definition 2.1df-r1 9680
[Kunen] p. 97Lemma 2.10r1elss 9722  r1elssi 9721
[Kunen] p. 107Exercise 4rankop 9774  rankopb 9768  rankuni 9779  rankxplim 9795  rankxpsuc 9798
[Kunen2] p. 47Lemma I.9.9relpfr 45231
[Kunen2] p. 53Lemma I.9.21trfr 45239
[Kunen2] p. 53Lemma I.9.24(2)wffr 45238
[Kunen2] p. 53Definition I.9.20tcfr 45240
[Kunen2] p. 95Lemma I.16.2ralabso 45245  rexabso 45246
[Kunen2] p. 96Example I.16.3disjabso 45252  n0abso 45253  ssabso 45251
[Kunen2] p. 111Lemma II.2.4(1)traxext 45254
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45264
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45259
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45262
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45263
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45258
[Kunen2] p. 112Corollary II.2.5wfaxext 45270  wfaxpr 45275  wfaxreg 45277  wfaxrep 45271  wfaxsep 45272  wfaxun 45276
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45261
[Kunen2] p. 113Corollary II.2.9wfaxpow 45274
[Kunen2] p. 114Theorem II.2.13wfaxext 45270
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45269  omelaxinf2 45266
[Kunen2] p. 114Corollary II.2.12wfac8prim 45279  wfaxinf2 45278
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45292  permaxext 45282  permaxinf2 45290  permaxnul 45285  permaxpow 45286  permaxpr 45287  permaxrep 45283  permaxsep 45284  permaxun 45288
[Kunen2] p. 148Definition II.9.1brpermmodel 45280
[Kunen2] p. 149Exercise II.9.3permac8prim 45291
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4960
[Lang] , p. 225Corollary 1.3finexttrb 33803
[Lang] p. Definitiondf-rn 5636
[Lang] p. 3Statementlidrideqd 18598  mndbn0 18679
[Lang] p. 3Definitiondf-mnd 18664
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18616
[Lang] p. 4Property of composites. Second formulagsumccat 18770
[Lang] p. 5Equationgsumreidx 19850
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48464
[Lang] p. 6Examplenn0mnd 48461
[Lang] p. 6Equationgsumxp2 19913
[Lang] p. 6Statementcycsubm 19135
[Lang] p. 6Definitionmulgnn0gsum 19014
[Lang] p. 6Observationmndlsmidm 19603
[Lang] p. 7Definitiondfgrp2e 18897
[Lang] p. 30Definitiondf-tocyc 33170
[Lang] p. 32Property (a)cyc3genpm 33215
[Lang] p. 32Property (b)cyc3conja 33220  cycpmconjv 33205
[Lang] p. 53Definitiondf-cat 17595
[Lang] p. 53Axiom CAT 1cat1 18025  cat1lem 18024
[Lang] p. 54Definitiondf-iso 17677
[Lang] p. 57Definitiondf-inito 17912  df-termo 17913
[Lang] p. 58Exampleirinitoringc 21438
[Lang] p. 58Statementinitoeu1 17939  termoeu1 17946
[Lang] p. 62Definitiondf-func 17786
[Lang] p. 65Definitiondf-nat 17874
[Lang] p. 91Notedf-ringc 20583
[Lang] p. 92Statementmxidlprm 33532
[Lang] p. 92Definitionisprmidlc 33509
[Lang] p. 128Remarkdsmmlmod 21704
[Lang] p. 129Prooflincscm 48712  lincscmcl 48714  lincsum 48711  lincsumcl 48713
[Lang] p. 129Statementlincolss 48716
[Lang] p. 129Observationdsmmfi 21697
[Lang] p. 141Theorem 5.3dimkerim 33765  qusdimsum 33766
[Lang] p. 141Corollary 5.4lssdimle 33745
[Lang] p. 147Definitionsnlindsntor 48753
[Lang] p. 504Statementmat1 22395  matring 22391
[Lang] p. 504Definitiondf-mamu 22339
[Lang] p. 505Statementmamuass 22350  mamutpos 22406  matassa 22392  mattposvs 22403  tposmap 22405
[Lang] p. 513Definitionmdet1 22549  mdetf 22543
[Lang] p. 513Theorem 4.4cramer 22639
[Lang] p. 514Proposition 4.6mdetleib 22535
[Lang] p. 514Proposition 4.8mdettpos 22559
[Lang] p. 515Definitiondf-minmar1 22583  smadiadetr 22623
[Lang] p. 515Corollary 4.9mdetero 22558  mdetralt 22556
[Lang] p. 517Proposition 4.15mdetmul 22571
[Lang] p. 518Definitiondf-madu 22582
[Lang] p. 518Proposition 4.16madulid 22593  madurid 22592  matinv 22625
[Lang] p. 561Theorem 3.1cayleyhamilton 22838
[Lang], p. 190Chapter 6vieta 33717
[Lang], p. 224Proposition 1.1extdgfialg 33832  finextalg 33836
[Lang], p. 224Proposition 1.2extdgmul 33801  fedgmul 33769
[Lang], p. 225Proposition 1.4algextdeg 33863
[Lang], p. 561Remarkchpmatply1 22780
[Lang], p. 561Definitiondf-chpmat 22775
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44611
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44606
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44612
[LeBlanc] p. 277Rule R2axnul 5251
[Levy] p. 12Axiom 4.3.1df-clab 2716
[Levy] p. 59Definitiondf-ttrcl 9621
[Levy] p. 64Theorem 5.6(ii)frinsg 9667
[Levy] p. 338Axiomdf-clel 2812  df-cleq 2729
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2812  df-cleq 2729
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2716
[Levy] p. 358Axiomdf-clab 2716
[Levy58] p. 2Definition Iisfin1-3 10300
[Levy58] p. 2Definition IIdf-fin2 10200
[Levy58] p. 2Definition Iadf-fin1a 10199
[Levy58] p. 2Definition IIIdf-fin3 10202
[Levy58] p. 3Definition Vdf-fin5 10203
[Levy58] p. 3Definition IVdf-fin4 10201
[Levy58] p. 4Definition VIdf-fin6 10204
[Levy58] p. 4Definition VIIdf-fin7 10205
[Levy58], p. 3Theorem 1fin1a2 10329
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27658
[Lipparini] p. 3Lemma 2.1.4noresle 27669
[Lipparini] p. 6Proposition 4.2noinfbnd1 27701  nosupbnd1 27686
[Lipparini] p. 6Proposition 4.3noinfbnd2 27703  nosupbnd2 27688
[Lipparini] p. 7Theorem 5.1noetasuplem3 27707  noetasuplem4 27708
[Lipparini] p. 7Corollary 4.4nosupinfsep 27704
[Lopez-Astorga] p. 12Rule 1mptnan 1770
[Lopez-Astorga] p. 12Rule 2mptxor 1771
[Lopez-Astorga] p. 12Rule 3mtpxor 1773
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32466
[Maeda] p. 168Lemma 5mdsym 32470  mdsymi 32469
[Maeda] p. 168Lemma 4(i)mdsymlem4 32464  mdsymlem6 32466  mdsymlem7 32467
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32468
[MaedaMaeda] p. 1Remarkssdmd1 32371  ssdmd2 32372  ssmd1 32369  ssmd2 32370
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32367
[MaedaMaeda] p. 1Definition 1.1df-dmd 32339  df-md 32338  mdbr 32352
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32389  mdslj1i 32377  mdslj2i 32378  mdslle1i 32375  mdslle2i 32376  mdslmd1i 32387  mdslmd2i 32388
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32379  mdsl2bi 32381  mdsl2i 32380
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32393
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32390
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32391
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32368
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32373  mdsl3 32374
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32392
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32487
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39618  hlrelat1 39697
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39336
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32394  cvmdi 32382  cvnbtwn4 32347  cvrnbtwn4 39576
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32395
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39637  cvp 32433  cvrp 39713  lcvp 39337
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32457
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32456
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39630  hlexch4N 39689
[MaedaMaeda] p. 34Exercise 7.1atabsi 32459
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39740
[MaedaMaeda] p. 61Definition 15.10psubN 40046  atpsubN 40050  df-pointsN 39799  pointpsubN 40048
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39801  pmap11 40059  pmaple 40058  pmapsub 40065  pmapval 40054
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40062  pmap1N 40064
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40067  pmapglb2N 40068  pmapglb2xN 40069  pmapglbx 40066
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40149
[MaedaMaeda] p. 67Postulate PS1ps-1 39774
[MaedaMaeda] p. 68Lemma 16.2df-padd 40093  paddclN 40139  paddidm 40138
[MaedaMaeda] p. 68Condition PS2ps-2 39775
[MaedaMaeda] p. 68Equation 16.2.1paddass 40135
[MaedaMaeda] p. 69Lemma 16.4ps-1 39774
[MaedaMaeda] p. 69Theorem 16.4ps-2 39775
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19608  lsmmod2 19609  lssats 39309  shatomici 32416  shatomistici 32419  shmodi 31448  shmodsi 31447
[MaedaMaeda] p. 130Remark 29.6dmdmd 32358  mdsymlem7 32467
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31647
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31551
[MaedaMaeda] p. 139Remarksumdmdii 32473
[Margaris] p. 40Rule Cexlimiv 1932
[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 1782  df-or 849  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30458
[Margaris] p. 59Section 14notnotrALTVD 45191
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 45192
[Margaris] p. 79Rule Cexinst01 44902  exinst11 44903
[Margaris] p. 89Theorem 19.219.2 1978  19.2g 2196  r19.2z 4453
[Margaris] p. 89Theorem 19.319.3 2210  rr19.3v 3622
[Margaris] p. 89Theorem 19.5alcom 2165
[Margaris] p. 89Theorem 19.6alex 1828
[Margaris] p. 89Theorem 19.7alnex 1783
[Margaris] p. 89Theorem 19.819.8a 2189
[Margaris] p. 89Theorem 19.919.9 2213  19.9h 2293  exlimd 2226  exlimdh 2297
[Margaris] p. 89Theorem 19.11excom 2168  excomim 2169
[Margaris] p. 89Theorem 19.1219.12 2333
[Margaris] p. 90Section 19conventions-labels 30459  conventions-labels 30459  conventions-labels 30459  conventions-labels 30459
[Margaris] p. 90Theorem 19.14exnal 1829
[Margaris] p. 90Theorem 19.152albi 44655  albi 1820
[Margaris] p. 90Theorem 19.1619.16 2233
[Margaris] p. 90Theorem 19.1719.17 2234
[Margaris] p. 90Theorem 19.182exbi 44657  exbi 1849
[Margaris] p. 90Theorem 19.1919.19 2237
[Margaris] p. 90Theorem 19.202alim 44654  2alimdv 1920  alimd 2220  alimdh 1819  alimdv 1918  ax-4 1811  ralimdaa 3238  ralimdv 3151  ralimdva 3149  ralimdvva 3184  sbcimdv 3810
[Margaris] p. 90Theorem 19.2119.21 2215  19.21h 2294  19.21t 2214  19.21vv 44653  alrimd 2223  alrimdd 2222  alrimdh 1865  alrimdv 1931  alrimi 2221  alrimih 1826  alrimiv 1929  alrimivv 1930  hbralrimi 3127  r19.21be 3230  r19.21bi 3229  ralrimd 3242  ralrimdv 3135  ralrimdva 3137  ralrimdvv 3181  ralrimdvva 3192  ralrimi 3235  ralrimia 3236  ralrimiv 3128  ralrimiva 3129  ralrimivv 3178  ralrimivva 3180  ralrimivvva 3183  ralrimivw 3133
[Margaris] p. 90Theorem 19.222exim 44656  2eximdv 1921  exim 1836  eximd 2224  eximdh 1866  eximdv 1919  rexim 3078  reximd2a 3247  reximdai 3239  reximdd 45428  reximddv 3153  reximddv2 3196  reximddv3 3154  reximdv 3152  reximdv2 3147  reximdva 3150  reximdvai 3148  reximdvva 3185  reximi2 3070
[Margaris] p. 90Theorem 19.2319.23 2219  19.23bi 2199  19.23h 2295  19.23t 2218  exlimdv 1935  exlimdvv 1936  exlimexi 44801  exlimiv 1932  exlimivv 1934  rexlimd3 45424  rexlimdv 3136  rexlimdv3a 3142  rexlimdva 3138  rexlimdva2 3140  rexlimdvaa 3139  rexlimdvv 3193  rexlimdvva 3194  rexlimdvvva 3195  rexlimdvw 3143  rexlimiv 3131  rexlimiva 3130  rexlimivv 3179
[Margaris] p. 90Theorem 19.2419.24 1993
[Margaris] p. 90Theorem 19.2519.25 1882
[Margaris] p. 90Theorem 19.2619.26 1872
[Margaris] p. 90Theorem 19.2719.27 2235  r19.27z 4464  r19.27zv 4465
[Margaris] p. 90Theorem 19.2819.28 2236  19.28vv 44663  r19.28z 4456  r19.28zf 45439  r19.28zv 4460  rr19.28v 3623
[Margaris] p. 90Theorem 19.2919.29 1875  r19.29d2r 3124  r19.29imd 3102
[Margaris] p. 90Theorem 19.3019.30 1883
[Margaris] p. 90Theorem 19.3119.31 2242  19.31vv 44661
[Margaris] p. 90Theorem 19.3219.32 2241  r19.32 47380
[Margaris] p. 90Theorem 19.3319.33-2 44659  19.33 1886
[Margaris] p. 90Theorem 19.3419.34 1994
[Margaris] p. 90Theorem 19.3519.35 1879
[Margaris] p. 90Theorem 19.3619.36 2238  19.36vv 44660  r19.36zv 4466
[Margaris] p. 90Theorem 19.3719.37 2240  19.37vv 44662  r19.37zv 4461
[Margaris] p. 90Theorem 19.3819.38 1841
[Margaris] p. 90Theorem 19.3919.39 1992
[Margaris] p. 90Theorem 19.4019.40-2 1889  19.40 1888  r19.40 3103
[Margaris] p. 90Theorem 19.4119.41 2243  19.41rg 44827
[Margaris] p. 90Theorem 19.4219.42 2244
[Margaris] p. 90Theorem 19.4319.43 1884
[Margaris] p. 90Theorem 19.4419.44 2245  r19.44zv 4463
[Margaris] p. 90Theorem 19.4519.45 2246  r19.45zv 4462
[Margaris] p. 110Exercise 2(b)eu1 2611
[Mayet] p. 370Remarkjpi 32328  largei 32325  stri 32315
[Mayet3] p. 9Definition of CH-statesdf-hst 32270  ishst 32272
[Mayet3] p. 10Theoremhstrbi 32324  hstri 32323
[Mayet3] p. 1223Theorem 4.1mayete3i 31786
[Mayet3] p. 1240Theorem 7.1mayetes3i 31787
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32336
[MegPav2000] p. 2345Definition 3.4-1chintcl 31390  chsupcl 31398
[MegPav2000] p. 2345Definition 3.4-2hatomic 32418
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32412
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32439
[MegPav2000] p. 2366Figure 7pl42N 40280
[MegPav2002] p. 362Lemma 2.2latj31 18414  latj32 18412  latjass 18410
[Megill] p. 444Axiom C5ax-5 1912  ax5ALT 39204
[Megill] p. 444Section 7conventions 30458
[Megill] p. 445Lemma L12aecom-o 39198  ax-c11n 39185  axc11n 2431
[Megill] p. 446Lemma L17equtrr 2024
[Megill] p. 446Lemma L18ax6fromc10 39193
[Megill] p. 446Lemma L19hbnae-o 39225  hbnae 2437
[Megill] p. 447Remark 9.1dfsb1 2486  sbid 2263  sbidd-misc 50000  sbidd 49999
[Megill] p. 448Remark 9.6axc14 2468
[Megill] p. 448Scheme C4'ax-c4 39181
[Megill] p. 448Scheme C5'ax-c5 39180  sp 2191
[Megill] p. 448Scheme C6'ax-11 2163
[Megill] p. 448Scheme C7'ax-c7 39182
[Megill] p. 448Scheme C8'ax-7 2010
[Megill] p. 448Scheme C9'ax-c9 39187
[Megill] p. 448Scheme C10'ax-6 1969  ax-c10 39183
[Megill] p. 448Scheme C11'ax-c11 39184
[Megill] p. 448Scheme C12'ax-8 2116
[Megill] p. 448Scheme C13'ax-9 2124
[Megill] p. 448Scheme C14'ax-c14 39188
[Megill] p. 448Scheme C15'ax-c15 39186
[Megill] p. 448Scheme C16'ax-c16 39189
[Megill] p. 448Theorem 9.4dral1-o 39201  dral1 2444  dral2-o 39227  dral2 2443  drex1 2446  drex2 2447  drsb1 2500  drsb2 2274
[Megill] p. 449Theorem 9.7sbcom2 2179  sbequ 2089  sbid2v 2514
[Megill] p. 450Example in Appendixhba1-o 39194  hba1 2300
[Mendelson] p. 35Axiom A3hirstL-ax3 47174
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3830  rspsbca 3831  stdpc4 2074
[Mendelson] p. 69Axiom 5ax-c4 39181  ra4 3837  stdpc5 2216
[Mendelson] p. 81Rule Cexlimiv 1932
[Mendelson] p. 95Axiom 6stdpc6 2030
[Mendelson] p. 95Axiom 7stdpc7 2258
[Mendelson] p. 225Axiom system NBGru 3739
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5463
[Mendelson] p. 231Exercise 4.10(k)inv1 4351
[Mendelson] p. 231Exercise 4.10(l)unv 4352
[Mendelson] p. 231Exercise 4.10(n)dfin3 4230
[Mendelson] p. 231Exercise 4.10(o)df-nul 4287
[Mendelson] p. 231Exercise 4.10(q)dfin4 4231
[Mendelson] p. 231Exercise 4.10(s)ddif 4094
[Mendelson] p. 231Definition of uniondfun3 4229
[Mendelson] p. 235Exercise 4.12(c)univ 5400
[Mendelson] p. 235Exercise 4.12(d)pwv 4861
[Mendelson] p. 235Exercise 4.12(j)pwin 5516
[Mendelson] p. 235Exercise 4.12(k)pwunss 4573
[Mendelson] p. 235Exercise 4.12(l)pwssun 5517
[Mendelson] p. 235Exercise 4.12(n)uniin 4888
[Mendelson] p. 235Exercise 4.12(p)reli 5776
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6228
[Mendelson] p. 244Proposition 4.8(g)epweon 7722
[Mendelson] p. 246Definition of successordf-suc 6324
[Mendelson] p. 250Exercise 4.36oelim2 8525
[Mendelson] p. 254Proposition 4.22(b)xpen 9072
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8993  xpsneng 8994
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9000  xpcomeng 9001
[Mendelson] p. 254Proposition 4.22(e)xpassen 9003
[Mendelson] p. 255Definitionbrsdom 8915
[Mendelson] p. 255Exercise 4.39endisj 8996
[Mendelson] p. 255Exercise 4.41mapprc 8771
[Mendelson] p. 255Exercise 4.43mapsnen 8978  mapsnend 8977
[Mendelson] p. 255Exercise 4.45mapunen 9078
[Mendelson] p. 255Exercise 4.47xpmapen 9077
[Mendelson] p. 255Exercise 4.42(a)map0e 8824
[Mendelson] p. 255Exercise 4.42(b)map1 8981
[Mendelson] p. 257Proposition 4.24(a)undom 8997
[Mendelson] p. 258Exercise 4.56(c)djuassen 10093  djucomen 10092
[Mendelson] p. 258Exercise 4.56(f)djudom1 10097
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10091
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8460
[Mendelson] p. 266Proposition 4.34(f)oaordex 8487
[Mendelson] p. 275Proposition 4.42(d)entri3 10473
[Mendelson] p. 281Definitiondf-r1 9680
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9729
[Mendelson] p. 287Axiom system MKru 3739
[MertziosUnger] p. 152Definitiondf-frgr 30317
[MertziosUnger] p. 153Remark 1frgrconngr 30352
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30354  vdgn1frgrv3 30355
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30356
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30349
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30342  2pthfrgrrn 30340  2pthfrgrrn2 30341
[Mittelstaedt] p. 9Definitiondf-oc 31310
[Monk1] p. 22Remarkconventions 30458
[Monk1] p. 22Theorem 3.1conventions 30458
[Monk1] p. 26Theorem 2.8(vii)ssin 4192
[Monk1] p. 33Theorem 3.2(i)ssrel 5733  ssrelf 32675
[Monk1] p. 33Theorem 3.2(ii)eqrel 5734
[Monk1] p. 34Definition 3.3df-opab 5162
[Monk1] p. 36Theorem 3.7(i)coi1 6222  coi2 6223
[Monk1] p. 36Theorem 3.8(v)dm0 5870  rn0 5876
[Monk1] p. 36Theorem 3.7(ii)cnvi 6100
[Monk1] p. 37Theorem 3.13(i)relxp 5643
[Monk1] p. 37Theorem 3.13(x)dmxp 5879  rnxp 6129
[Monk1] p. 37Theorem 3.13(ii)0xp 5724  xp0 5725
[Monk1] p. 38Theorem 3.16(ii)ima0 6037
[Monk1] p. 38Theorem 3.16(viii)imai 6034
[Monk1] p. 39Theorem 3.17imaex 7858  imaexg 7857
[Monk1] p. 39Theorem 3.16(xi)imassrn 6031
[Monk1] p. 41Theorem 4.3(i)fnopfv 7022  funfvop 6997
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6889
[Monk1] p. 42Theorem 4.4(iii)fvelima 6900
[Monk1] p. 43Theorem 4.6funun 6539
[Monk1] p. 43Theorem 4.8(iv)dff13 7202  dff13f 7203
[Monk1] p. 46Theorem 4.15(v)funex 7167  funrnex 7900
[Monk1] p. 50Definition 5.4fniunfv 7195
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6186
[Monk1] p. 52Theorem 5.11(viii)ssint 4920
[Monk1] p. 52Definition 5.13 (i)1stval2 7952  df-1st 7935
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7953  df-2nd 7936
[Monk1] p. 112Theorem 15.17(v)ranksn 9770  ranksnb 9743
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9771
[Monk1] p. 112Theorem 15.17(iii)rankun 9772  rankunb 9766
[Monk1] p. 113Theorem 15.18r1val3 9754
[Monk1] p. 113Definition 15.19df-r1 9680  r1val2 9753
[Monk1] p. 117Lemmazorn2 10420  zorn2g 10417
[Monk1] p. 133Theorem 18.11cardom 9902
[Monk1] p. 133Theorem 18.12canth3 10475
[Monk1] p. 133Theorem 18.14carduni 9897
[Monk2] p. 105Axiom C4ax-4 1811
[Monk2] p. 105Axiom C7ax-7 2010
[Monk2] p. 105Axiom C8ax-12 2185  ax-c15 39186  ax12v2 2187
[Monk2] p. 108Lemma 5ax-c4 39181
[Monk2] p. 109Lemma 12ax-11 2163
[Monk2] p. 109Lemma 15equvini 2460  equvinv 2031  eqvinop 5436
[Monk2] p. 113Axiom C5-1ax-5 1912  ax5ALT 39204
[Monk2] p. 113Axiom C5-2ax-10 2147
[Monk2] p. 113Axiom C5-3ax-11 2163
[Monk2] p. 114Lemma 21sp 2191
[Monk2] p. 114Lemma 22axc4 2327  hba1-o 39194  hba1 2300
[Monk2] p. 114Lemma 23nfia1 2159
[Monk2] p. 114Lemma 24nfa2 2182  nfra2 3347  nfra2w 3273
[Moore] p. 53Part Idf-mre 17509
[Munkres] p. 77Example 2distop 22943  indistop 22950  indistopon 22949
[Munkres] p. 77Example 3fctop 22952  fctop2 22953
[Munkres] p. 77Example 4cctop 22954
[Munkres] p. 78Definition of basisdf-bases 22894  isbasis3g 22897
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17367  tgval2 22904
[Munkres] p. 79Remarktgcl 22917
[Munkres] p. 80Lemma 2.1tgval3 22911
[Munkres] p. 80Lemma 2.2tgss2 22935  tgss3 22934
[Munkres] p. 81Lemma 2.3basgen 22936  basgen2 22937
[Munkres] p. 83Exercise 3topdifinf 37525  topdifinfeq 37526  topdifinffin 37524  topdifinfindis 37522
[Munkres] p. 89Definition of subspace topologyresttop 23108
[Munkres] p. 93Theorem 6.1(1)0cld 22986  topcld 22983
[Munkres] p. 93Theorem 6.1(2)iincld 22987
[Munkres] p. 93Theorem 6.1(3)uncld 22989
[Munkres] p. 94Definition of closureclsval 22985
[Munkres] p. 94Definition of interiorntrval 22984
[Munkres] p. 95Theorem 6.5(a)clsndisj 23023  elcls 23021
[Munkres] p. 95Theorem 6.5(b)elcls3 23031
[Munkres] p. 97Theorem 6.6clslp 23096  neindisj 23065
[Munkres] p. 97Corollary 6.7cldlp 23098
[Munkres] p. 97Definition of limit pointislp2 23093  lpval 23087
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23263
[Munkres] p. 102Definition of continuous functiondf-cn 23175  iscn 23183  iscn2 23186
[Munkres] p. 107Theorem 7.2(g)cncnp 23228  cncnp2 23229  cncnpi 23226  df-cnp 23176  iscnp 23185  iscnp2 23187
[Munkres] p. 127Theorem 10.1metcn 24491
[Munkres] p. 128Theorem 10.3metcn4 25271
[Nathanson] p. 123Remarkreprgt 34759  reprinfz1 34760  reprlt 34757
[Nathanson] p. 123Definitiondf-repr 34747
[Nathanson] p. 123Chapter 5.1circlemethnat 34779
[Nathanson] p. 123Propositionbreprexp 34771  breprexpnat 34772  itgexpif 34744
[NielsenChuang] p. 195Equation 4.73unierri 32162
[OeSilva] p. 2042Section 2ax-bgbltosilva 48092
[Pfenning] p. 17Definition XMnatded 30461
[Pfenning] p. 17Definition NNCnatded 30461  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30461
[Pfenning] p. 18Rule"natded 30461
[Pfenning] p. 18Definition /\Inatded 30461
[Pfenning] p. 18Definition ` `Enatded 30461  natded 30461  natded 30461  natded 30461  natded 30461
[Pfenning] p. 18Definition ` `Inatded 30461  natded 30461  natded 30461  natded 30461  natded 30461
[Pfenning] p. 18Definition ` `ELnatded 30461
[Pfenning] p. 18Definition ` `ERnatded 30461
[Pfenning] p. 18Definition ` `Ea,unatded 30461
[Pfenning] p. 18Definition ` `IRnatded 30461
[Pfenning] p. 18Definition ` `Ianatded 30461
[Pfenning] p. 127Definition =Enatded 30461
[Pfenning] p. 127Definition =Inatded 30461
[Ponnusamy] p. 361Theorem 6.44cphip0l 25162  df-dip 30759  dip0l 30776  ip0l 21595
[Ponnusamy] p. 361Equation 6.45cphipval 25203  ipval 30761
[Ponnusamy] p. 362Equation I1dipcj 30772  ipcj 21593
[Ponnusamy] p. 362Equation I3cphdir 25165  dipdir 30900  ipdir 21598  ipdiri 30888
[Ponnusamy] p. 362Equation I4ipidsq 30768  nmsq 25154
[Ponnusamy] p. 362Equation 6.46ip0i 30883
[Ponnusamy] p. 362Equation 6.47ip1i 30885
[Ponnusamy] p. 362Equation 6.48ip2i 30886
[Ponnusamy] p. 363Equation I2cphass 25171  dipass 30903  ipass 21604  ipassi 30899
[Prugovecki] p. 186Definition of brabraval 32002  df-bra 31908
[Prugovecki] p. 376Equation 8.1df-kb 31909  kbval 32012
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32440
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40185
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32454  atcvat4i 32455  cvrat3 39739  cvrat4 39740  lsatcvat3 39349
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32340  cvrval 39566  df-cv 32337  df-lcv 39316  lspsncv0 21105
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40197
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40198
[Quine] p. 16Definition 2.1df-clab 2716  rabid 3421  rabidd 45435
[Quine] p. 17Definition 2.1''dfsb7 2286
[Quine] p. 18Definition 2.7df-cleq 2729
[Quine] p. 19Definition 2.9conventions 30458  df-v 3443
[Quine] p. 34Theorem 5.1eqabb 2876
[Quine] p. 35Theorem 5.2abid1 2873  abid2f 2930
[Quine] p. 40Theorem 6.1sb5 2283
[Quine] p. 40Theorem 6.2sb6 2091  sbalex 2250
[Quine] p. 41Theorem 6.3df-clel 2812
[Quine] p. 41Theorem 6.4eqid 2737  eqid1 30525
[Quine] p. 41Theorem 6.5eqcom 2744
[Quine] p. 42Theorem 6.6df-sbc 3742
[Quine] p. 42Theorem 6.7dfsbcq 3743  dfsbcq2 3744
[Quine] p. 43Theorem 6.8vex 3445
[Quine] p. 43Theorem 6.9isset 3455
[Quine] p. 44Theorem 7.3spcgf 3546  spcgv 3551  spcimgf 3508
[Quine] p. 44Theorem 6.11spsbc 3754  spsbcd 3755
[Quine] p. 44Theorem 6.12elex 3462
[Quine] p. 44Theorem 6.13elab 3635  elabg 3632  elabgf 3630
[Quine] p. 44Theorem 6.14noel 4291
[Quine] p. 48Theorem 7.2snprc 4675
[Quine] p. 48Definition 7.1df-pr 4584  df-sn 4582
[Quine] p. 49Theorem 7.4snss 4742  snssg 4741
[Quine] p. 49Theorem 7.5prss 4777  prssg 4776
[Quine] p. 49Theorem 7.6prid1 4720  prid1g 4718  prid2 4721  prid2g 4719  snid 4620  snidg 4618
[Quine] p. 51Theorem 7.12snex 5382
[Quine] p. 51Theorem 7.13prex 5383
[Quine] p. 53Theorem 8.2unisn 4883  unisnALT 45202  unisng 4882
[Quine] p. 53Theorem 8.3uniun 4887
[Quine] p. 54Theorem 8.6elssuni 4895
[Quine] p. 54Theorem 8.7uni0 4892
[Quine] p. 56Theorem 8.17uniabio 6463
[Quine] p. 56Definition 8.18dfaiota2 47368  dfiota2 6450
[Quine] p. 57Theorem 8.19aiotaval 47377  iotaval 6467
[Quine] p. 57Theorem 8.22iotanul 6473
[Quine] p. 58Theorem 8.23iotaex 6469
[Quine] p. 58Definition 9.1df-op 4588
[Quine] p. 61Theorem 9.5opabid 5474  opabidw 5473  opelopab 5491  opelopaba 5485  opelopabaf 5493  opelopabf 5494  opelopabg 5487  opelopabga 5482  opelopabgf 5489  oprabid 7392  oprabidw 7391
[Quine] p. 64Definition 9.11df-xp 5631
[Quine] p. 64Definition 9.12df-cnv 5633
[Quine] p. 64Definition 9.15df-id 5520
[Quine] p. 65Theorem 10.3fun0 6558
[Quine] p. 65Theorem 10.4funi 6525
[Quine] p. 65Theorem 10.5funsn 6546  funsng 6544
[Quine] p. 65Definition 10.1df-fun 6495
[Quine] p. 65Definition 10.2args 6052  dffv4 6832
[Quine] p. 68Definition 10.11conventions 30458  df-fv 6501  fv2 6830
[Quine] p. 124Theorem 17.3nn0opth2 14199  nn0opth2i 14198  nn0opthi 14197  omopthi 8591
[Quine] p. 177Definition 25.2df-rdg 8343
[Quine] p. 232Equation icarddom 10468
[Quine] p. 284Axiom 39(vi)funimaex 6581  funimaexg 6580
[Quine] p. 331Axiom system NFru 3739
[ReedSimon] p. 36Definition (iii)ax-his3 31142
[ReedSimon] p. 63Exercise 4(a)df-dip 30759  polid 31217  polid2i 31215  polidi 31216
[ReedSimon] p. 63Exercise 4(b)df-ph 30871
[ReedSimon] p. 195Remarklnophm 32077  lnophmi 32076
[Retherford] p. 49Exercise 1(i)leopadd 32190
[Retherford] p. 49Exercise 1(ii)leopmul 32192  leopmuli 32191
[Retherford] p. 49Exercise 1(iv)leoptr 32195
[Retherford] p. 49Definition VI.1df-leop 31910  leoppos 32184
[Retherford] p. 49Exercise 1(iii)leoptri 32194
[Retherford] p. 49Definition of operator orderingleop3 32183
[Roman] p. 4Definitiondf-dmat 22438  df-dmatalt 48680
[Roman] p. 18Part Preliminariesdf-rng 20092
[Roman] p. 19Part Preliminariesdf-ring 20174
[Roman] p. 46Theorem 1.6isldepslvec2 48767
[Roman] p. 112Noteisldepslvec2 48767  ldepsnlinc 48790  zlmodzxznm 48779
[Roman] p. 112Examplezlmodzxzequa 48778  zlmodzxzequap 48781  zlmodzxzldep 48786
[Roman] p. 170Theorem 7.8cayleyhamilton 22838
[Rosenlicht] p. 80Theoremheicant 37827
[Rosser] p. 281Definitiondf-op 4588
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34783
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34784
[Rotman] p. 28Remarkpgrpgt2nabl 48648  pmtr3ncom 19408
[Rotman] p. 31Theorem 3.4symggen2 19404
[Rotman] p. 42Theorem 3.15cayley 19347  cayleyth 19348
[Rudin] p. 164Equation 27efcan 16023
[Rudin] p. 164Equation 30efzval 16031
[Rudin] p. 167Equation 48absefi 16125
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1773
[Sanford] p. 39Rule 4mptxor 1771
[Sanford] p. 40Rule 1mptnan 1770
[Schechter] p. 51Definition of antisymmetryintasym 6073
[Schechter] p. 51Definition of irreflexivityintirr 6076
[Schechter] p. 51Definition of symmetrycnvsym 6072
[Schechter] p. 51Definition of transitivitycotr 6070
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17509
[Schechter] p. 79Definition of Moore closuredf-mrc 17510
[Schechter] p. 82Section 4.5df-mrc 17510
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17512
[Schechter] p. 139Definition AC3dfac9 10051
[Schechter] p. 141Definition (MC)dfac11 43340
[Schechter] p. 149Axiom DC1ax-dc 10360  axdc3 10368
[Schechter] p. 187Definition of "ring with unit"isring 20176  isrngo 38069
[Schechter] p. 276Remark 11.6.espan0 31600
[Schechter] p. 276Definition of spandf-span 31367  spanval 31391
[Schechter] p. 428Definition 15.35bastop1 22941
[Schloeder] p. 1Lemma 1.3onelon 6343  onelord 43529  ordelon 6342  ordelord 6340
[Schloeder] p. 1Lemma 1.7onepsuc 43530  sucidg 6401
[Schloeder] p. 1Remark 1.50elon 6373  onsuc 7757  ord0 6372  ordsuci 7755
[Schloeder] p. 1Theorem 1.9epsoon 43531
[Schloeder] p. 1Definition 1.1dftr5 5210
[Schloeder] p. 1Definition 1.2dford3 43306  elon2 6329
[Schloeder] p. 1Definition 1.4df-suc 6324
[Schloeder] p. 1Definition 1.6epel 5528  epelg 5526
[Schloeder] p. 1Theorem 1.9(i)elirr 9508  epirron 43532  ordirr 6336
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43534  oneptr 43533  ontr1 6365
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6361  oneptri 43535  ordtri3or 6350
[Schloeder] p. 2Lemma 1.10ondif1 8430  ord0eln0 6374
[Schloeder] p. 2Lemma 1.13elsuci 6387  onsucss 43544  trsucss 6408
[Schloeder] p. 2Lemma 1.14ordsucss 7762
[Schloeder] p. 2Lemma 1.15onnbtwn 6414  ordnbtwn 6413
[Schloeder] p. 2Lemma 1.16orddif0suc 43546  ordnexbtwnsuc 43545
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10315  onsucf1lem 43547  onsucf1o 43550  onsucf1olem 43548  onsucrn 43549
[Schloeder] p. 2Lemma 1.18dflim7 43551
[Schloeder] p. 2Remark 1.12ordzsl 7789
[Schloeder] p. 2Theorem 1.10ondif1i 43540  ordne0gt0 43539
[Schloeder] p. 2Definition 1.11dflim6 43542  limnsuc 43543  onsucelab 43541
[Schloeder] p. 3Remark 1.21omex 9556
[Schloeder] p. 3Theorem 1.19tfinds 7804
[Schloeder] p. 3Theorem 1.22omelon 9559  ordom 7820
[Schloeder] p. 3Definition 1.20dfom3 9560
[Schloeder] p. 4Lemma 2.21onn 8570
[Schloeder] p. 4Lemma 2.7ssonuni 7727  ssorduni 7726
[Schloeder] p. 4Remark 2.4oa1suc 8460
[Schloeder] p. 4Theorem 1.23dfom5 9563  limom 7826
[Schloeder] p. 4Definition 2.1df-1o 8399  df1o2 8406
[Schloeder] p. 4Definition 2.3oa0 8445  oa0suclim 43553  oalim 8461  oasuc 8453
[Schloeder] p. 4Definition 2.5om0 8446  om0suclim 43554  omlim 8462  omsuc 8455
[Schloeder] p. 4Definition 2.6oe0 8451  oe0m1 8450  oe0suclim 43555  oelim 8463  oesuc 8456
[Schloeder] p. 5Lemma 2.10onsupuni 43507
[Schloeder] p. 5Lemma 2.11onsupsucismax 43557
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43558
[Schloeder] p. 5Lemma 2.13limexissup 43559  limexissupab 43561  limiun 43560  limuni 6380
[Schloeder] p. 5Lemma 2.14oa0r 8467
[Schloeder] p. 5Lemma 2.15om1 8471  om1om1r 43562  om1r 8472
[Schloeder] p. 5Remark 2.8oacl 8464  oaomoecl 43556  oecl 8466  omcl 8465
[Schloeder] p. 5Definition 2.9onsupintrab 43509
[Schloeder] p. 6Lemma 2.16oe1 8473
[Schloeder] p. 6Lemma 2.17oe1m 8474
[Schloeder] p. 6Lemma 2.18oe0rif 43563
[Schloeder] p. 6Theorem 2.19oasubex 43564
[Schloeder] p. 6Theorem 2.20nnacl 8541  nnamecl 43565  nnecl 8543  nnmcl 8542
[Schloeder] p. 7Lemma 3.1onsucwordi 43566
[Schloeder] p. 7Lemma 3.2oaword1 8481
[Schloeder] p. 7Lemma 3.3oaword2 8482
[Schloeder] p. 7Lemma 3.4oalimcl 8489
[Schloeder] p. 7Lemma 3.5oaltublim 43568
[Schloeder] p. 8Lemma 3.6oaordi3 43569
[Schloeder] p. 8Lemma 3.81oaomeqom 43571
[Schloeder] p. 8Lemma 3.10oa00 8488
[Schloeder] p. 8Lemma 3.11omge1 43575  omword1 8502
[Schloeder] p. 8Remark 3.9oaordnr 43574  oaordnrex 43573
[Schloeder] p. 8Theorem 3.7oaord3 43570
[Schloeder] p. 9Lemma 3.12omge2 43576  omword2 8503
[Schloeder] p. 9Lemma 3.13omlim2 43577
[Schloeder] p. 9Lemma 3.14omord2lim 43578
[Schloeder] p. 9Lemma 3.15omord2i 43579  omordi 8495
[Schloeder] p. 9Theorem 3.16omord 8497  omord2com 43580
[Schloeder] p. 10Lemma 3.172omomeqom 43581  df-2o 8400
[Schloeder] p. 10Lemma 3.19oege1 43584  oewordi 8521
[Schloeder] p. 10Lemma 3.20oege2 43585  oeworde 8523
[Schloeder] p. 10Lemma 3.21rp-oelim2 43586
[Schloeder] p. 10Lemma 3.22oeord2lim 43587
[Schloeder] p. 10Remark 3.18omnord1 43583  omnord1ex 43582
[Schloeder] p. 11Lemma 3.23oeord2i 43588
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43590
[Schloeder] p. 11Remark 3.26oenord1 43594  oenord1ex 43593
[Schloeder] p. 11Theorem 4.1oaomoencom 43595
[Schloeder] p. 11Theorem 4.2oaass 8490
[Schloeder] p. 11Theorem 3.24oeord2com 43589
[Schloeder] p. 12Theorem 4.3odi 8508
[Schloeder] p. 13Theorem 4.4omass 8509
[Schloeder] p. 14Remark 4.6oenass 43597
[Schloeder] p. 14Theorem 4.7oeoa 8527
[Schloeder] p. 15Lemma 5.1cantnftermord 43598
[Schloeder] p. 15Lemma 5.2cantnfub 43599  cantnfub2 43600
[Schloeder] p. 16Theorem 5.3cantnf2 43603
[Schwabhauser] p. 10Axiom A1axcgrrflx 28970  axtgcgrrflx 28517
[Schwabhauser] p. 10Axiom A2axcgrtr 28971
[Schwabhauser] p. 10Axiom A3axcgrid 28972  axtgcgrid 28518
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28503
[Schwabhauser] p. 11Axiom A4axsegcon 28983  axtgsegcon 28519  df-trkgcb 28505
[Schwabhauser] p. 11Axiom A5ax5seg 28994  axtg5seg 28520  df-trkgcb 28505
[Schwabhauser] p. 11Axiom A6axbtwnid 28995  axtgbtwnid 28521  df-trkgb 28504
[Schwabhauser] p. 12Axiom A7axpasch 28997  axtgpasch 28522  df-trkgb 28504
[Schwabhauser] p. 12Axiom A8axlowdim2 29016  df-trkg2d 34803
[Schwabhauser] p. 13Axiom A8axtglowdim2 28525
[Schwabhauser] p. 13Axiom A9axtgupdim2 28526  df-trkg2d 34803
[Schwabhauser] p. 13Axiom A10axeuclid 29019  axtgeucl 28527  df-trkge 28506
[Schwabhauser] p. 13Axiom A11axcont 29032  axtgcont 28524  axtgcont1 28523  df-trkgb 28504
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36162
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36164
[Schwabhauser] p. 27Theorem 2.3cgrtr 36167
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36171
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36172  tgcgrcomimp 28532  tgcgrcoml 28534  tgcgrcomr 28533
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36177  tgcgrtriv 28539
[Schwabhauser] p. 28Theorem 2.105segofs 36181  tg5segofs 34811
[Schwabhauser] p. 28Definition 2.10df-afs 34808  df-ofs 36158
[Schwabhauser] p. 29Theorem 2.11cgrextend 36183  tgcgrextend 28540
[Schwabhauser] p. 29Theorem 2.12segconeq 36185  tgsegconeq 28541
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36197  btwntriv2 36187  tgbtwntriv2 28542
[Schwabhauser] p. 30Theorem 3.2btwncomim 36188  tgbtwncom 28543
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36191  tgbtwntriv1 28546
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36192  tgbtwnswapid 28547
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36198  btwnintr 36194  tgbtwnexch2 28551  tgbtwnintr 28548
[Schwabhauser] p. 30Theorem 3.6btwnexch 36200  btwnexch3 36195  tgbtwnexch 28553  tgbtwnexch3 28549
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36199  tgbtwnouttr 28552  tgbtwnouttr2 28550
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29015
[Schwabhauser] p. 32Theorem 3.14btwndiff 36202  tgbtwndiff 28561
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28554  trisegint 36203
[Schwabhauser] p. 34Theorem 4.2ifscgr 36219  tgifscgr 28563
[Schwabhauser] p. 34Theorem 4.11colcom 28613  colrot1 28614  colrot2 28615  lncom 28677  lnrot1 28678  lnrot2 28679
[Schwabhauser] p. 34Definition 4.1df-ifs 36215
[Schwabhauser] p. 35Theorem 4.3cgrsub 36220  tgcgrsub 28564
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36230  tgcgrxfr 28573
[Schwabhauser] p. 35Statement 4.4ercgrg 28572
[Schwabhauser] p. 35Definition 4.4df-cgr3 36216  df-cgrg 28566
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28566
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36231  tgbtwnxfr 28585
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36237  colinearperm2 36239  colinearperm3 36238  colinearperm4 36240  colinearperm5 36241
[Schwabhauser] p. 36Definition 4.8df-ismt 28588
[Schwabhauser] p. 36Definition 4.10df-colinear 36214  tgellng 28608  tglng 28601
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36242
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36250  lnxfr 28621
[Schwabhauser] p. 37Theorem 4.14lineext 36251  lnext 28622
[Schwabhauser] p. 37Theorem 4.16fscgr 36255  tgfscgr 28623
[Schwabhauser] p. 37Theorem 4.17linecgr 36256  lncgr 28624
[Schwabhauser] p. 37Definition 4.15df-fs 36217
[Schwabhauser] p. 38Theorem 4.18lineid 36258  lnid 28625
[Schwabhauser] p. 38Theorem 4.19idinside 36259  tgidinside 28626
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36276  tgbtwnconn1 28630
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36277  tgbtwnconn2 28631
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36278  tgbtwnconn3 28632
[Schwabhauser] p. 41Theorem 5.5brsegle2 36284
[Schwabhauser] p. 41Definition 5.4df-segle 36282  legov 28640
[Schwabhauser] p. 41Definition 5.5legov2 28641
[Schwabhauser] p. 42Remark 5.13legso 28654
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36285
[Schwabhauser] p. 42Theorem 5.7seglerflx 36287
[Schwabhauser] p. 42Theorem 5.8segletr 36289
[Schwabhauser] p. 42Theorem 5.9segleantisym 36290
[Schwabhauser] p. 42Theorem 5.10seglelin 36291
[Schwabhauser] p. 42Theorem 5.11seglemin 36288
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36293
[Schwabhauser] p. 42Proposition 5.7legid 28642
[Schwabhauser] p. 42Proposition 5.8legtrd 28644
[Schwabhauser] p. 42Proposition 5.9legtri3 28645
[Schwabhauser] p. 42Proposition 5.10legtrid 28646
[Schwabhauser] p. 42Proposition 5.11leg0 28647
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36300
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36301
[Schwabhauser] p. 43Theorem 6.4broutsideof 36296  df-outsideof 36295
[Schwabhauser] p. 43Definition 6.1broutsideof2 36297  ishlg 28657
[Schwabhauser] p. 44Theorem 6.4hlln 28662
[Schwabhauser] p. 44Theorem 6.5hlid 28664  outsideofrflx 36302
[Schwabhauser] p. 44Theorem 6.6hlcomb 28658  hlcomd 28659  outsideofcom 36303
[Schwabhauser] p. 44Theorem 6.7hltr 28665  outsideoftr 36304
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28673  outsideofeu 36306
[Schwabhauser] p. 44Definition 6.8df-ray 36313
[Schwabhauser] p. 45Part 2df-lines2 36314
[Schwabhauser] p. 45Theorem 6.13outsidele 36307
[Schwabhauser] p. 45Theorem 6.15lineunray 36322
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36323  tglineelsb2 28687
[Schwabhauser] p. 45Theorem 6.17linecom 36325  linerflx1 36324  linerflx2 36326  tglinecom 28690  tglinerflx1 28688  tglinerflx2 28689
[Schwabhauser] p. 45Theorem 6.18linethru 36328  tglinethru 28691
[Schwabhauser] p. 45Definition 6.14df-line2 36312  tglng 28601
[Schwabhauser] p. 45Proposition 6.13legbtwn 28649
[Schwabhauser] p. 46Theorem 6.19linethrueu 36331  tglinethrueu 28694
[Schwabhauser] p. 46Theorem 6.21lineintmo 36332  tglineineq 28698  tglineinteq 28700  tglineintmo 28697
[Schwabhauser] p. 46Theorem 6.23colline 28704
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28705
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28706
[Schwabhauser] p. 49Theorem 7.3mirinv 28721
[Schwabhauser] p. 49Theorem 7.7mirmir 28717
[Schwabhauser] p. 49Theorem 7.8mirreu3 28709
[Schwabhauser] p. 49Definition 7.5df-mir 28708  ismir 28714  mirbtwn 28713  mircgr 28712  mirfv 28711  mirval 28710
[Schwabhauser] p. 50Theorem 7.8mirreu 28719
[Schwabhauser] p. 50Theorem 7.9mireq 28720
[Schwabhauser] p. 50Theorem 7.10mirinv 28721
[Schwabhauser] p. 50Theorem 7.11mirf1o 28724
[Schwabhauser] p. 50Theorem 7.13miriso 28725
[Schwabhauser] p. 51Theorem 7.14mirmot 28730
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28727  mirbtwni 28726
[Schwabhauser] p. 51Theorem 7.16mircgrs 28728
[Schwabhauser] p. 51Theorem 7.17miduniq 28740
[Schwabhauser] p. 52Lemma 7.21symquadlem 28744
[Schwabhauser] p. 52Theorem 7.18miduniq1 28741
[Schwabhauser] p. 52Theorem 7.19miduniq2 28742
[Schwabhauser] p. 52Theorem 7.20colmid 28743
[Schwabhauser] p. 53Lemma 7.22krippen 28746
[Schwabhauser] p. 55Lemma 7.25midexlem 28747
[Schwabhauser] p. 57Theorem 8.2ragcom 28753
[Schwabhauser] p. 57Definition 8.1df-rag 28749  israg 28752
[Schwabhauser] p. 58Theorem 8.3ragcol 28754
[Schwabhauser] p. 58Theorem 8.4ragmir 28755
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28757
[Schwabhauser] p. 58Theorem 8.6ragflat2 28758
[Schwabhauser] p. 58Theorem 8.7ragflat 28759
[Schwabhauser] p. 58Theorem 8.8ragtriva 28760
[Schwabhauser] p. 58Theorem 8.9ragflat3 28761  ragncol 28764
[Schwabhauser] p. 58Theorem 8.10ragcgr 28762
[Schwabhauser] p. 59Theorem 8.12perpcom 28768
[Schwabhauser] p. 59Theorem 8.13ragperp 28772
[Schwabhauser] p. 59Theorem 8.14perpneq 28769
[Schwabhauser] p. 59Definition 8.11df-perpg 28751  isperp 28767
[Schwabhauser] p. 59Definition 8.13isperp2 28770
[Schwabhauser] p. 60Theorem 8.18foot 28777
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28785  colperpexlem2 28786
[Schwabhauser] p. 63Theorem 8.21colperpex 28788  colperpexlem3 28787
[Schwabhauser] p. 64Theorem 8.22mideu 28793  midex 28792
[Schwabhauser] p. 66Lemma 8.24opphllem 28790
[Schwabhauser] p. 67Theorem 9.2oppcom 28799
[Schwabhauser] p. 67Definition 9.1islnopp 28794
[Schwabhauser] p. 68Lemma 9.3opphllem2 28803
[Schwabhauser] p. 68Lemma 9.4opphllem5 28806  opphllem6 28807
[Schwabhauser] p. 69Theorem 9.5opphl 28809
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28522
[Schwabhauser] p. 70Theorem 9.6outpasch 28810
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28818
[Schwabhauser] p. 71Definition 9.7df-hpg 28813  hpgbr 28815
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28820
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28819
[Schwabhauser] p. 72Theorem 9.11hpgid 28821
[Schwabhauser] p. 72Theorem 9.12hpgcom 28822
[Schwabhauser] p. 72Theorem 9.13hpgtr 28823
[Schwabhauser] p. 73Theorem 9.18colopp 28824
[Schwabhauser] p. 73Theorem 9.19colhp 28825
[Schwabhauser] p. 88Theorem 10.2lmieu 28839
[Schwabhauser] p. 88Definition 10.1df-mid 28829
[Schwabhauser] p. 89Theorem 10.4lmicom 28843
[Schwabhauser] p. 89Theorem 10.5lmilmi 28844
[Schwabhauser] p. 89Theorem 10.6lmireu 28845
[Schwabhauser] p. 89Theorem 10.7lmieq 28846
[Schwabhauser] p. 89Theorem 10.8lmiinv 28847
[Schwabhauser] p. 89Theorem 10.9lmif1o 28850
[Schwabhauser] p. 89Theorem 10.10lmiiso 28852
[Schwabhauser] p. 89Definition 10.3df-lmi 28830
[Schwabhauser] p. 90Theorem 10.11lmimot 28853
[Schwabhauser] p. 91Theorem 10.12hypcgr 28856
[Schwabhauser] p. 92Theorem 10.14lmiopp 28857
[Schwabhauser] p. 92Theorem 10.15lnperpex 28858
[Schwabhauser] p. 92Theorem 10.16trgcopy 28859  trgcopyeu 28861
[Schwabhauser] p. 95Definition 11.2dfcgra2 28885
[Schwabhauser] p. 95Definition 11.3iscgra 28864
[Schwabhauser] p. 95Proposition 11.4cgracgr 28873
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28871  cgrahl2 28872
[Schwabhauser] p. 96Theorem 11.6cgraid 28874
[Schwabhauser] p. 96Theorem 11.9cgraswap 28875
[Schwabhauser] p. 97Theorem 11.7cgracom 28877
[Schwabhauser] p. 97Theorem 11.8cgratr 28878
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28881  cgrahl 28882
[Schwabhauser] p. 98Theorem 11.13sacgr 28886
[Schwabhauser] p. 98Theorem 11.14oacgr 28887
[Schwabhauser] p. 98Theorem 11.15acopy 28888  acopyeu 28889
[Schwabhauser] p. 101Theorem 11.24inagswap 28896
[Schwabhauser] p. 101Theorem 11.25inaghl 28900
[Schwabhauser] p. 101Definition 11.23isinag 28893
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28908
[Schwabhauser] p. 102Definition 11.27df-leag 28901  isleag 28902
[Schwabhauser] p. 107Theorem 11.49tgsas 28910  tgsas1 28909  tgsas2 28911  tgsas3 28912
[Schwabhauser] p. 108Theorem 11.50tgasa 28914  tgasa1 28913
[Schwabhauser] p. 109Theorem 11.51tgsss1 28915  tgsss2 28916  tgsss3 28917
[Shapiro] p. 230Theorem 6.5.1dchrhash 27242  dchrsum 27240  dchrsum2 27239  sumdchr 27243
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27244  sum2dchr 27245
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20001  ablfacrp2 20002
[Shapiro], p. 328Equation 9.2.4vmasum 27187
[Shapiro], p. 329Equation 9.2.7logfac2 27188
[Shapiro], p. 329Equation 9.2.9logfacrlim 27195
[Shapiro], p. 331Equation 9.2.13vmadivsum 27453
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27456
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27510  vmalogdivsum2 27509
[Shapiro], p. 375Theorem 9.4.1dirith 27500  dirith2 27499
[Shapiro], p. 375Equation 9.4.3rplogsum 27498  rpvmasum 27497  rpvmasum2 27483
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27458
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27496
[Shapiro], p. 377Lemma 9.4.1dchrisum 27463  dchrisumlem1 27460  dchrisumlem2 27461  dchrisumlem3 27462  dchrisumlema 27459
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27466
[Shapiro], p. 379Equation 9.4.16dchrmusum 27495  dchrmusumlem 27493  dchrvmasumlem 27494
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27465
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27467
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27491  dchrisum0re 27484  dchrisumn0 27492
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27477
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27481
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27482
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27537  pntrsumbnd2 27538  pntrsumo1 27536
[Shapiro], p. 405Equation 10.2.1mudivsum 27501
[Shapiro], p. 406Equation 10.2.6mulogsum 27503
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27505
[Shapiro], p. 407Equation 10.2.8mulog2sum 27508
[Shapiro], p. 418Equation 10.4.6logsqvma 27513
[Shapiro], p. 418Equation 10.4.8logsqvma2 27514
[Shapiro], p. 419Equation 10.4.10selberg 27519
[Shapiro], p. 420Equation 10.4.12selberg2lem 27521
[Shapiro], p. 420Equation 10.4.14selberg2 27522
[Shapiro], p. 422Equation 10.6.7selberg3 27530
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27531
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27528  selberg3lem2 27529
[Shapiro], p. 422Equation 10.4.23selberg4 27532
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27526
[Shapiro], p. 428Equation 10.6.2selbergr 27539
[Shapiro], p. 429Equation 10.6.8selberg3r 27540
[Shapiro], p. 430Equation 10.6.11selberg4r 27541
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27555
[Shapiro], p. 434Equation 10.6.27pntlema 27567  pntlemb 27568  pntlemc 27566  pntlemd 27565  pntlemg 27569
[Shapiro], p. 435Equation 10.6.29pntlema 27567
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27559
[Shapiro], p. 436Lemma 10.6.2pntibnd 27564
[Shapiro], p. 436Equation 10.6.34pntlema 27567
[Shapiro], p. 436Equation 10.6.35pntlem3 27580  pntleml 27582
[Stewart] p. 91Lemma 7.3constrss 33881
[Stewart] p. 92Definition 7.4.df-constr 33868
[Stewart] p. 96Theorem 7.10constraddcl 33900  constrinvcl 33911  constrmulcl 33909  constrnegcl 33901  constrsqrtcl 33917
[Stewart] p. 97Theorem 7.11constrextdg2 33887
[Stewart] p. 98Theorem 7.12constrext2chn 33897
[Stewart] p. 99Theorem 7.132sqr3nconstr 33919
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33929
[Stoll] p. 13Definition corresponds to dfsymdif3 4259
[Stoll] p. 16Exercise 4.40dif 4358  dif0 4331
[Stoll] p. 16Exercise 4.8difdifdir 4445
[Stoll] p. 17Theorem 5.1(5)unvdif 4428
[Stoll] p. 19Theorem 5.2(13)undm 4250
[Stoll] p. 19Theorem 5.2(13')indm 4251
[Stoll] p. 20Remarkinvdif 4232
[Stoll] p. 25Definition of ordered tripledf-ot 4590
[Stoll] p. 43Definitionuniiun 5015
[Stoll] p. 44Definitionintiin 5016
[Stoll] p. 45Definitiondf-iin 4950
[Stoll] p. 45Definition indexed uniondf-iun 4949
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4259
[Strang] p. 242Section 6.3expgrowth 44612
[Suppes] p. 22Theorem 2eq0 4303  eq0f 4300
[Suppes] p. 22Theorem 4eqss 3950  eqssd 3952  eqssi 3951
[Suppes] p. 23Theorem 5ss0 4355  ss0b 4354
[Suppes] p. 23Theorem 6sstr 3943  sstrALT2 45111
[Suppes] p. 23Theorem 7pssirr 4056
[Suppes] p. 23Theorem 8pssn2lp 4057
[Suppes] p. 23Theorem 9psstr 4060
[Suppes] p. 23Theorem 10pssss 4051
[Suppes] p. 25Theorem 12elin 3918  elun 4106
[Suppes] p. 26Theorem 15inidm 4180
[Suppes] p. 26Theorem 16in0 4348
[Suppes] p. 27Theorem 23unidm 4110
[Suppes] p. 27Theorem 24un0 4347
[Suppes] p. 27Theorem 25ssun1 4131
[Suppes] p. 27Theorem 26ssequn1 4139
[Suppes] p. 27Theorem 27unss 4143
[Suppes] p. 27Theorem 28indir 4239
[Suppes] p. 27Theorem 29undir 4240
[Suppes] p. 28Theorem 32difid 4329
[Suppes] p. 29Theorem 33difin 4225
[Suppes] p. 29Theorem 34indif 4233
[Suppes] p. 29Theorem 35undif1 4429
[Suppes] p. 29Theorem 36difun2 4434
[Suppes] p. 29Theorem 37difin0 4427
[Suppes] p. 29Theorem 38disjdif 4425
[Suppes] p. 29Theorem 39difundi 4243
[Suppes] p. 29Theorem 40difindi 4245
[Suppes] p. 30Theorem 41nalset 5259
[Suppes] p. 39Theorem 61uniss 4872
[Suppes] p. 39Theorem 65uniop 5464
[Suppes] p. 41Theorem 70intsn 4940
[Suppes] p. 42Theorem 71intpr 4938  intprg 4937
[Suppes] p. 42Theorem 73op1stb 5420
[Suppes] p. 42Theorem 78intun 4936
[Suppes] p. 44Definition 15(a)dfiun2 4988  dfiun2g 4986
[Suppes] p. 44Definition 15(b)dfiin2 4989
[Suppes] p. 47Theorem 86elpw 4559  elpw2 5280  elpw2g 5279  elpwg 4558  elpwgdedVD 45193
[Suppes] p. 47Theorem 87pwid 4577
[Suppes] p. 47Theorem 89pw0 4769
[Suppes] p. 48Theorem 90pwpw0 4770
[Suppes] p. 52Theorem 101xpss12 5640
[Suppes] p. 52Theorem 102xpindi 5783  xpindir 5784
[Suppes] p. 52Theorem 103xpundi 5694  xpundir 5695
[Suppes] p. 54Theorem 105elirrv 9506
[Suppes] p. 58Theorem 2relss 5732
[Suppes] p. 59Theorem 4eldm 5850  eldm2 5851  eldm2g 5849  eldmg 5848
[Suppes] p. 59Definition 3df-dm 5635
[Suppes] p. 60Theorem 6dmin 5861
[Suppes] p. 60Theorem 8rnun 6104
[Suppes] p. 60Theorem 9rnin 6105
[Suppes] p. 60Definition 4dfrn2 5838
[Suppes] p. 61Theorem 11brcnv 5832  brcnvg 5829
[Suppes] p. 62Equation 5elcnv 5826  elcnv2 5827
[Suppes] p. 62Theorem 12relcnv 6064
[Suppes] p. 62Theorem 15cnvin 6103
[Suppes] p. 62Theorem 16cnvun 6101
[Suppes] p. 63Definitiondftrrels2 38831
[Suppes] p. 63Theorem 20co02 6220
[Suppes] p. 63Theorem 21dmcoss 5925
[Suppes] p. 63Definition 7df-co 5634
[Suppes] p. 64Theorem 26cnvco 5835
[Suppes] p. 64Theorem 27coass 6225
[Suppes] p. 65Theorem 31resundi 5953
[Suppes] p. 65Theorem 34elima 6025  elima2 6026  elima3 6027  elimag 6024
[Suppes] p. 65Theorem 35imaundi 6108
[Suppes] p. 66Theorem 40dminss 6112
[Suppes] p. 66Theorem 41imainss 6113
[Suppes] p. 67Exercise 11cnvxp 6116
[Suppes] p. 81Definition 34dfec2 8640
[Suppes] p. 82Theorem 72elec 8684  elecALTV 38443  elecg 8682
[Suppes] p. 82Theorem 73eqvrelth 38867  erth 8692  erth2 8693
[Suppes] p. 83Theorem 74eqvreldisj 38870  erdisj 8695
[Suppes] p. 83Definition 35, df-parts 39040  dfmembpart2 39045
[Suppes] p. 89Theorem 96map0b 8825
[Suppes] p. 89Theorem 97map0 8829  map0g 8826
[Suppes] p. 89Theorem 98mapsn 8830  mapsnd 8828
[Suppes] p. 89Theorem 99mapss 8831
[Suppes] p. 91Definition 12(ii)alephsuc 9982
[Suppes] p. 91Definition 12(iii)alephlim 9981
[Suppes] p. 92Theorem 1enref 8926  enrefg 8925
[Suppes] p. 92Theorem 2ensym 8944  ensymb 8943  ensymi 8945
[Suppes] p. 92Theorem 3entr 8947
[Suppes] p. 92Theorem 4unen 8986
[Suppes] p. 94Theorem 15endom 8920
[Suppes] p. 94Theorem 16ssdomg 8941
[Suppes] p. 94Theorem 17domtr 8948
[Suppes] p. 95Theorem 18sbth 9029
[Suppes] p. 97Theorem 23canth2 9062  canth2g 9063
[Suppes] p. 97Definition 3brsdom2 9033  df-sdom 8890  dfsdom2 9032
[Suppes] p. 97Theorem 21(i)sdomirr 9046
[Suppes] p. 97Theorem 22(i)domnsym 9035
[Suppes] p. 97Theorem 21(ii)sdomnsym 9034
[Suppes] p. 97Theorem 22(ii)domsdomtr 9044
[Suppes] p. 97Theorem 22(iv)brdom2 8923
[Suppes] p. 97Theorem 21(iii)sdomtr 9047
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9042
[Suppes] p. 98Exercise 4fundmen 8972  fundmeng 8973
[Suppes] p. 98Exercise 6xpdom3 9007
[Suppes] p. 98Exercise 11sdomentr 9043
[Suppes] p. 104Theorem 37fofi 9217
[Suppes] p. 104Theorem 38pwfi 9223
[Suppes] p. 105Theorem 40pwfi 9223
[Suppes] p. 111Axiom for cardinal numberscarden 10465
[Suppes] p. 130Definition 3df-tr 5207
[Suppes] p. 132Theorem 9ssonuni 7727
[Suppes] p. 134Definition 6df-suc 6324
[Suppes] p. 136Theorem Schema 22findes 7844  finds 7840  finds1 7843  finds2 7842
[Suppes] p. 151Theorem 42isfinite 9565  isfinite2 9202  isfiniteg 9204  unbnn 9200
[Suppes] p. 162Definition 5df-ltnq 10833  df-ltpq 10825
[Suppes] p. 197Theorem Schema 4tfindes 7807  tfinds 7804  tfinds2 7808
[Suppes] p. 209Theorem 18oaord1 8480
[Suppes] p. 209Theorem 21oaword2 8482
[Suppes] p. 211Theorem 25oaass 8490
[Suppes] p. 225Definition 8iscard2 9892
[Suppes] p. 227Theorem 56ondomon 10477
[Suppes] p. 228Theorem 59harcard 9894
[Suppes] p. 228Definition 12(i)aleph0 9980
[Suppes] p. 228Theorem Schema 61onintss 6370
[Suppes] p. 228Theorem Schema 62onminesb 7740  onminsb 7741
[Suppes] p. 229Theorem 64alephval2 10487
[Suppes] p. 229Theorem 65alephcard 9984
[Suppes] p. 229Theorem 66alephord2i 9991
[Suppes] p. 229Theorem 67alephnbtwn 9985
[Suppes] p. 229Definition 12df-aleph 9856
[Suppes] p. 242Theorem 6weth 10409
[Suppes] p. 242Theorem 8entric 10471
[Suppes] p. 242Theorem 9carden 10465
[Szendrei] p. 11Line 6df-cloneop 35871
[Szendrei] p. 11Paragraph 3df-suppos 35875
[TakeutiZaring] p. 8Axiom 1ax-ext 2709
[TakeutiZaring] p. 13Definition 4.5df-cleq 2729
[TakeutiZaring] p. 13Proposition 4.6df-clel 2812
[TakeutiZaring] p. 13Proposition 4.9cvjust 2731
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2757
[TakeutiZaring] p. 14Definition 4.16df-oprab 7364
[TakeutiZaring] p. 14Proposition 4.14ru 3739
[TakeutiZaring] p. 15Axiom 2zfpair 5367
[TakeutiZaring] p. 15Exercise 1elpr 4606  elpr2 4608  elpr2g 4607  elprg 4604
[TakeutiZaring] p. 15Exercise 2elsn 4596  elsn2 4623  elsn2g 4622  elsng 4595  velsn 4597
[TakeutiZaring] p. 15Exercise 3elop 5416
[TakeutiZaring] p. 15Exercise 4sneq 4591  sneqr 4797
[TakeutiZaring] p. 15Definition 5.1dfpr2 4602  dfsn2 4594  dfsn2ALT 4603
[TakeutiZaring] p. 16Axiom 3uniex 7688
[TakeutiZaring] p. 16Exercise 6opth 5425
[TakeutiZaring] p. 16Exercise 7opex 5413
[TakeutiZaring] p. 16Exercise 8rext 5397
[TakeutiZaring] p. 16Corollary 5.8unex 7691  unexg 7690
[TakeutiZaring] p. 16Definition 5.3dftp2 4649
[TakeutiZaring] p. 16Definition 5.5df-uni 4865
[TakeutiZaring] p. 16Definition 5.6df-in 3909  df-un 3907
[TakeutiZaring] p. 16Proposition 5.7unipr 4881  uniprg 4880
[TakeutiZaring] p. 17Axiom 4vpwex 5323
[TakeutiZaring] p. 17Exercise 1eltp 4647
[TakeutiZaring] p. 17Exercise 5elsuc 6390  elsucg 6388  sstr2 3941
[TakeutiZaring] p. 17Exercise 6uncom 4111
[TakeutiZaring] p. 17Exercise 7incom 4162
[TakeutiZaring] p. 17Exercise 8unass 4125
[TakeutiZaring] p. 17Exercise 9inass 4181
[TakeutiZaring] p. 17Exercise 10indi 4237
[TakeutiZaring] p. 17Exercise 11undi 4238
[TakeutiZaring] p. 17Definition 5.9df-pss 3922  df-ss 3919
[TakeutiZaring] p. 17Definition 5.10df-pw 4557
[TakeutiZaring] p. 18Exercise 7unss2 4140
[TakeutiZaring] p. 18Exercise 9dfss2 3920  sseqin2 4176
[TakeutiZaring] p. 18Exercise 10ssid 3957
[TakeutiZaring] p. 18Exercise 12inss1 4190  inss2 4191
[TakeutiZaring] p. 18Exercise 13nss 3999
[TakeutiZaring] p. 18Exercise 15unieq 4875
[TakeutiZaring] p. 18Exercise 18sspwb 5398  sspwimp 45194  sspwimpALT 45201  sspwimpALT2 45204  sspwimpcf 45196
[TakeutiZaring] p. 18Exercise 19pweqb 5405
[TakeutiZaring] p. 19Axiom 5ax-rep 5225
[TakeutiZaring] p. 20Definitiondf-rab 3401
[TakeutiZaring] p. 20Corollary 5.160ex 5253
[TakeutiZaring] p. 20Definition 5.12df-dif 3905
[TakeutiZaring] p. 20Definition 5.14dfnul2 4289
[TakeutiZaring] p. 20Proposition 5.15difid 4329
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4306  n0f 4302  neq0 4305  neq0f 4301
[TakeutiZaring] p. 21Axiom 6zfreg 9505
[TakeutiZaring] p. 21Axiom 6'zfregs 9645
[TakeutiZaring] p. 21Theorem 5.22setind 9660
[TakeutiZaring] p. 21Definition 5.20df-v 3443
[TakeutiZaring] p. 21Proposition 5.21vprc 5261
[TakeutiZaring] p. 22Exercise 10ss 4353
[TakeutiZaring] p. 22Exercise 3ssex 5267  ssexg 5269
[TakeutiZaring] p. 22Exercise 4inex1 5263
[TakeutiZaring] p. 22Exercise 5ruv 9514
[TakeutiZaring] p. 22Exercise 6elirr 9508
[TakeutiZaring] p. 22Exercise 7ssdif0 4319
[TakeutiZaring] p. 22Exercise 11difdif 4088
[TakeutiZaring] p. 22Exercise 13undif3 4253  undif3VD 45158
[TakeutiZaring] p. 22Exercise 14difss 4089
[TakeutiZaring] p. 22Exercise 15sscon 4096
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3053
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3062
[TakeutiZaring] p. 23Proposition 6.2xpex 7700  xpexg 7697
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5632
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6564
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6740  fun11 6567
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6506  svrelfun 6565
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5837
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5839
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5637
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5638
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5634
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6153  dfrel2 6148
[TakeutiZaring] p. 25Exercise 3xpss 5641
[TakeutiZaring] p. 25Exercise 5relun 5761
[TakeutiZaring] p. 25Exercise 6reluni 5768
[TakeutiZaring] p. 25Exercise 9inxp 5781
[TakeutiZaring] p. 25Exercise 12relres 5965
[TakeutiZaring] p. 25Exercise 13opelres 5945  opelresi 5947
[TakeutiZaring] p. 25Exercise 14dmres 5972
[TakeutiZaring] p. 25Exercise 15resss 5961
[TakeutiZaring] p. 25Exercise 17resabs1 5966
[TakeutiZaring] p. 25Exercise 18funres 6535
[TakeutiZaring] p. 25Exercise 24relco 6068
[TakeutiZaring] p. 25Exercise 29funco 6533
[TakeutiZaring] p. 25Exercise 30f1co 6742
[TakeutiZaring] p. 26Definition 6.10eu2 2610
[TakeutiZaring] p. 26Definition 6.11conventions 30458  df-fv 6501  fv3 6853
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7869  cnvexg 7868
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7853  dmexg 7845
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7854  rnexg 7846
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44730
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7864
[TakeutiZaring] p. 27Corollary 6.13fvex 6848
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47456  tz6.12-1-afv2 47523  tz6.12-1 6858  tz6.12-afv 47455  tz6.12-afv2 47522  tz6.12 6859  tz6.12c-afv2 47524  tz6.12c 6857
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47519  tz6.12-2 6822  tz6.12i-afv2 47525  tz6.12i 6861
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6496
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6497
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6499  wfo 6491
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6498  wf1 6490
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6500  wf1o 6492
[TakeutiZaring] p. 28Exercise 4eqfnfv 6978  eqfnfv2 6979  eqfnfv2f 6982
[TakeutiZaring] p. 28Exercise 5fvco 6933
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7165
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7163
[TakeutiZaring] p. 29Exercise 9funimaex 6581  funimaexg 6580
[TakeutiZaring] p. 29Definition 6.18df-br 5100
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5534
[TakeutiZaring] p. 30Definition 6.21dffr2 5586  dffr3 6059  eliniseg 6054  iniseg 6057
[TakeutiZaring] p. 30Definition 6.22df-eprel 5525
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5602  fr3nr 7719  frirr 5601
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5578
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7721
[TakeutiZaring] p. 31Exercise 1frss 5589
[TakeutiZaring] p. 31Exercise 4wess 5611
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6306  tz6.26i 6307  wefrc 5619  wereu2 5622
[TakeutiZaring] p. 32Theorem 6.27wfi 6308  wfii 6309
[TakeutiZaring] p. 32Definition 6.28df-isom 6502
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7277
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7278
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7284
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7285
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7286
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7290
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7297
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7299
[TakeutiZaring] p. 35Notationwtr 5206
[TakeutiZaring] p. 35Theorem 7.2trelpss 44731  tz7.2 5608
[TakeutiZaring] p. 35Definition 7.1dftr3 5211
[TakeutiZaring] p. 36Proposition 7.4ordwe 6331
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6339
[TakeutiZaring] p. 36Proposition 7.6ordelord 6340  ordelordALT 44814  ordelordALTVD 45143
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6346  ordelssne 6345
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6344
[TakeutiZaring] p. 37Proposition 7.9ordin 6348
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7729
[TakeutiZaring] p. 38Corollary 7.15ordsson 7730
[TakeutiZaring] p. 38Definition 7.11df-on 6322
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6350
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44826  ordon 7724
[TakeutiZaring] p. 38Proposition 7.13onprc 7725
[TakeutiZaring] p. 39Theorem 7.17tfi 7797
[TakeutiZaring] p. 40Exercise 3ontr2 6366
[TakeutiZaring] p. 40Exercise 7dftr2 5208
[TakeutiZaring] p. 40Exercise 9onssmin 7739
[TakeutiZaring] p. 40Exercise 11unon 7775
[TakeutiZaring] p. 40Exercise 12ordun 6424
[TakeutiZaring] p. 40Exercise 14ordequn 6423
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7726
[TakeutiZaring] p. 40Proposition 7.20elssuni 4895
[TakeutiZaring] p. 41Definition 7.22df-suc 6324
[TakeutiZaring] p. 41Proposition 7.23sssucid 6400  sucidg 6401
[TakeutiZaring] p. 41Proposition 7.24onsuc 7757
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6414  ordnbtwn 6413
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7772
[TakeutiZaring] p. 42Exercise 1df-lim 6323
[TakeutiZaring] p. 42Exercise 4omssnlim 7825
[TakeutiZaring] p. 42Exercise 7ssnlim 7830
[TakeutiZaring] p. 42Exercise 8onsucssi 7785  ordelsuc 7764
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7766
[TakeutiZaring] p. 42Definition 7.27nlimon 7795
[TakeutiZaring] p. 42Definition 7.28dfom2 7812
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7833
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7834
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7835
[TakeutiZaring] p. 43Remarkomon 7822
[TakeutiZaring] p. 43Axiom 7inf3 9548  omex 9556
[TakeutiZaring] p. 43Theorem 7.32ordom 7820
[TakeutiZaring] p. 43Corollary 7.31find 7839
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7836
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7837
[TakeutiZaring] p. 44Exercise 1limomss 7815
[TakeutiZaring] p. 44Exercise 2int0 4918
[TakeutiZaring] p. 44Exercise 3trintss 5224
[TakeutiZaring] p. 44Exercise 4intss1 4919
[TakeutiZaring] p. 44Exercise 5intex 5290
[TakeutiZaring] p. 44Exercise 6oninton 7742
[TakeutiZaring] p. 44Exercise 11ordintdif 6369
[TakeutiZaring] p. 44Definition 7.35df-int 4904
[TakeutiZaring] p. 44Proposition 7.34noinfep 9573
[TakeutiZaring] p. 45Exercise 4onint 7737
[TakeutiZaring] p. 47Lemma 1tfrlem1 8309
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8330
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8331
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8332
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8339  tz7.44-2 8340  tz7.44-3 8341
[TakeutiZaring] p. 50Exercise 1smogt 8301
[TakeutiZaring] p. 50Exercise 3smoiso 8296
[TakeutiZaring] p. 50Definition 7.46df-smo 8280
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8378  tz7.49c 8379
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8376
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8375
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8377
[TakeutiZaring] p. 53Proposition 7.532eu5 2657
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9925
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9926
[TakeutiZaring] p. 56Definition 8.1oalim 8461  oasuc 8453
[TakeutiZaring] p. 57Remarktfindsg 7805
[TakeutiZaring] p. 57Proposition 8.2oacl 8464
[TakeutiZaring] p. 57Proposition 8.3oa0 8445  oa0r 8467
[TakeutiZaring] p. 57Proposition 8.16omcl 8465
[TakeutiZaring] p. 58Corollary 8.5oacan 8477
[TakeutiZaring] p. 58Proposition 8.4nnaord 8549  nnaordi 8548  oaord 8476  oaordi 8475
[TakeutiZaring] p. 59Proposition 8.6iunss2 5006  uniss2 4898
[TakeutiZaring] p. 59Proposition 8.7oawordri 8479
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8484  oawordex 8486
[TakeutiZaring] p. 59Proposition 8.9nnacl 8541
[TakeutiZaring] p. 59Proposition 8.10oaabs 8578
[TakeutiZaring] p. 60Remarkoancom 9564
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8489
[TakeutiZaring] p. 62Exercise 1nnarcl 8546
[TakeutiZaring] p. 62Exercise 5oaword1 8481
[TakeutiZaring] p. 62Definition 8.15om0x 8448  omlim 8462  omsuc 8455
[TakeutiZaring] p. 62Definition 8.15(a)om0 8446
[TakeutiZaring] p. 63Proposition 8.17nnecl 8543  nnmcl 8542
[TakeutiZaring] p. 63Proposition 8.19nnmord 8562  nnmordi 8561  omord 8497  omordi 8495
[TakeutiZaring] p. 63Proposition 8.20omcan 8498
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8566  omwordri 8501
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8468
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8471  om1r 8472
[TakeutiZaring] p. 64Proposition 8.22om00 8504
[TakeutiZaring] p. 64Proposition 8.23omordlim 8506
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8507
[TakeutiZaring] p. 64Proposition 8.25odi 8508
[TakeutiZaring] p. 65Theorem 8.26omass 8509
[TakeutiZaring] p. 67Definition 8.30nnesuc 8538  oe0 8451  oelim 8463  oesuc 8456  onesuc 8459
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8449
[TakeutiZaring] p. 67Proposition 8.32oen0 8516
[TakeutiZaring] p. 67Proposition 8.33oeordi 8517
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8450
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8474
[TakeutiZaring] p. 68Corollary 8.34oeord 8518
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8524
[TakeutiZaring] p. 68Proposition 8.35oewordri 8522
[TakeutiZaring] p. 68Proposition 8.37oeworde 8523
[TakeutiZaring] p. 69Proposition 8.41oeoa 8527
[TakeutiZaring] p. 70Proposition 8.42oeoe 8529
[TakeutiZaring] p. 73Theorem 9.1trcl 9641  tz9.1 9642
[TakeutiZaring] p. 76Definition 9.9df-r1 9680  r10 9684  r1lim 9688  r1limg 9687  r1suc 9686  r1sucg 9685
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9696  r1ord2 9697  r1ordg 9694
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9706
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9731  tz9.13 9707  tz9.13g 9708
[TakeutiZaring] p. 79Definition 9.14df-rank 9681  rankval 9732  rankvalb 9713  rankvalg 9733
[TakeutiZaring] p. 79Proposition 9.16rankel 9755  rankelb 9740
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9769  rankval3 9756  rankval3b 9742
[TakeutiZaring] p. 79Proposition 9.18rankonid 9745
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9711
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9750  rankr1c 9737  rankr1g 9748
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9751
[TakeutiZaring] p. 80Exercise 1rankss 9765  rankssb 9764
[TakeutiZaring] p. 80Exercise 2unbndrank 9758
[TakeutiZaring] p. 80Proposition 9.19bndrank 9757
[TakeutiZaring] p. 83Axiom of Choiceac4 10389  dfac3 10035
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9944  numth 10386  numth2 10385
[TakeutiZaring] p. 85Definition 10.4cardval 10460
[TakeutiZaring] p. 85Proposition 10.5cardid 10461  cardid2 9869
[TakeutiZaring] p. 85Proposition 10.9oncard 9876
[TakeutiZaring] p. 85Proposition 10.10carden 10465
[TakeutiZaring] p. 85Proposition 10.11cardidm 9875
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9860
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9881
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9873
[TakeutiZaring] p. 87Proposition 10.15pwen 9082
[TakeutiZaring] p. 88Exercise 1en0 8959
[TakeutiZaring] p. 88Exercise 7infensuc 9087
[TakeutiZaring] p. 89Exercise 10omxpen 9011
[TakeutiZaring] p. 90Corollary 10.23cardnn 9879
[TakeutiZaring] p. 90Definition 10.27alephiso 10012
[TakeutiZaring] p. 90Proposition 10.20nneneq 9134
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9142
[TakeutiZaring] p. 90Proposition 10.26alephprc 10013
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9139
[TakeutiZaring] p. 91Exercise 2alephle 10002
[TakeutiZaring] p. 91Exercise 3aleph0 9980
[TakeutiZaring] p. 91Exercise 4cardlim 9888
[TakeutiZaring] p. 91Exercise 7infpss 10130
[TakeutiZaring] p. 91Exercise 8infcntss 9227
[TakeutiZaring] p. 91Definition 10.29df-fin 8891  isfi 8916
[TakeutiZaring] p. 92Proposition 10.32onfin 9143
[TakeutiZaring] p. 92Proposition 10.34imadomg 10448
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9004
[TakeutiZaring] p. 93Proposition 10.35fodomb 10440
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10100  unxpdom 9163
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9890  cardsdomelir 9889
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9165
[TakeutiZaring] p. 94Proposition 10.39infxpen 9928
[TakeutiZaring] p. 95Definition 10.42df-map 8769
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10476  infxpidm2 9931
[TakeutiZaring] p. 95Proposition 10.41infdju 10121  infxp 10128
[TakeutiZaring] p. 96Proposition 10.44pw2en 9016  pw2f1o 9014
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9075
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10401
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10396  ac6s5 10405
[TakeutiZaring] p. 98Theorem 10.47unidom 10457
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10458  uniimadomf 10459
[TakeutiZaring] p. 100Definition 11.1cfcof 10188
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10183
[TakeutiZaring] p. 102Exercise 1cfle 10168
[TakeutiZaring] p. 102Exercise 2cf0 10165
[TakeutiZaring] p. 102Exercise 3cfsuc 10171
[TakeutiZaring] p. 102Exercise 4cfom 10178
[TakeutiZaring] p. 102Proposition 11.9coftr 10187
[TakeutiZaring] p. 103Theorem 11.15alephreg 10497
[TakeutiZaring] p. 103Proposition 11.11cardcf 10166
[TakeutiZaring] p. 103Proposition 11.13alephsing 10190
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10011
[TakeutiZaring] p. 104Proposition 11.16carduniima 10010
[TakeutiZaring] p. 104Proposition 11.18alephfp 10022  alephfp2 10023
[TakeutiZaring] p. 106Theorem 11.20gchina 10614
[TakeutiZaring] p. 106Theorem 11.21mappwen 10026
[TakeutiZaring] p. 107Theorem 11.26konigth 10484
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10498
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10499
[Tarski] p. 67Axiom B5ax-c5 39180
[Tarski] p. 67Scheme B5sp 2191
[Tarski] p. 68Lemma 6avril1 30521  equid 2014
[Tarski] p. 69Lemma 7equcomi 2019
[Tarski] p. 70Lemma 14spim 2392  spime 2394  spimew 1973
[Tarski] p. 70Lemma 16ax-12 2185  ax-c15 39186  ax12i 1968
[Tarski] p. 70Lemmas 16 and 17sb6 2091
[Tarski] p. 75Axiom B7ax6v 1970
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1912  ax5ALT 39204
[Tarski], p. 75Scheme B8 of system S2ax-7 2010  ax-8 2116  ax-9 2124
[Tarski1999] p. 178Axiom 4axtgsegcon 28519
[Tarski1999] p. 178Axiom 5axtg5seg 28520
[Tarski1999] p. 179Axiom 7axtgpasch 28522
[Tarski1999] p. 180Axiom 7.1axtgpasch 28522
[Tarski1999] p. 185Axiom 11axtgcont1 28523
[Truss] p. 114Theorem 5.18ruc 16172
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37831
[Viaclovsky8] p. 3Proposition 7ismblfin 37833
[Weierstrass] p. 272Definitiondf-mdet 22533  mdetuni 22570
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 904
[WhiteheadRussell] p. 96Axiom *1.3olc 869
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 870
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 920
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 970
[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 37621
[WhiteheadRussell] p. 100Theorem *2.05frege5 44077  imim2 58  wl-luk-imim2 37616
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47301  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 897
[WhiteheadRussell] p. 101Theorem *2.06barbara 2664  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 903
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37619
[WhiteheadRussell] p. 101Theorem *2.11exmid 895
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 898
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 45203  wl-luk-notnotr 37620
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44107  axfrege28 44106  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 868
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 925
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37613
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 890
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 942
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30459  pm2.27 42  wl-luk-pm2.27 37611
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 923
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38543
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 924
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 972
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 973
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 971
[WhiteheadRussell] p. 105Definition *2.33df-3or 1088
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 907
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 908
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 945
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 882
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 883
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 191
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 884
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 885
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 886
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 852
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 853
[WhiteheadRussell] p. 107Theorem *2.55orel1 889
[WhiteheadRussell] p. 107Theorem *2.56orel2 891
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 900
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 943
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 944
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 892  pm2.67 893
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 899
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 975
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 901
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 976
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 977
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 934
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 932
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 974
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 978
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 933
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 994
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 995
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 996
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 997
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 998
[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 803
[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 765
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 766
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 808
[WhiteheadRussell] p. 113Fact)pm3.45 623
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 810
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 492
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 493
[WhiteheadRussell] p. 113Theorem *3.44jao 963  pm3.44 962
[WhiteheadRussell] p. 113Theorem *3.47anim12 809
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 966
[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 807
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 833
[WhiteheadRussell] p. 117Theorem *4.21bicom 222
[WhiteheadRussell] p. 117Theorem *4.22biantr 806  bitr 805
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 563
[WhiteheadRussell] p. 117Theorem *4.25oridm 905  pm4.25 906
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1010
[WhiteheadRussell] p. 118Theorem *4.31orcom 871
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[WhiteheadRussell] p. 118Theorem *4.33orass 922
[WhiteheadRussell] p. 118Theorem *4.36anbi1 634
[WhiteheadRussell] p. 118Theorem *4.37orbi1 918
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 638
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 979
[WhiteheadRussell] p. 118Definition *4.34df-3an 1089
[WhiteheadRussell] p. 119Theorem *4.41ordi 1008
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1054
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1025
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 999
[WhiteheadRussell] p. 119Theorem *4.45orabs 1001  pm4.45 1000  pm4.45im 828
[WhiteheadRussell] p. 120Theorem *4.5anor 985
[WhiteheadRussell] p. 120Theorem *4.6imor 854
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 984
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 987
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 988
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 989
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 990
[WhiteheadRussell] p. 120Theorem *4.56ioran 986  pm4.56 991
[WhiteheadRussell] p. 120Theorem *4.57oran 992  pm4.57 993
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 857
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 850
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 851
[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 952
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 937
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 964  pm4.77 965
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 935
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1006
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1026
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1027
[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 844
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 824
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 947  pm5.11g 946
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 948
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 950
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 949
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1015
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1016
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1014
[WhiteheadRussell] p. 124Theorem *5.18nbbn 383  pm5.18 381
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 386
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 825
[WhiteheadRussell] p. 124Theorem *5.22xor 1017
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1050
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1051
[WhiteheadRussell] p. 124Theorem *5.25dfor2 902
[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 1004
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 956
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 831
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 573
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 836
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 826
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 834
[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 1007
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1020
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 951
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1003
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1021
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1022
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1030
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1031
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44635
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44636
[WhiteheadRussell] p. 147Theorem *10.2219.26 1872
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44637
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44638
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44639
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1895
[WhiteheadRussell] p. 151Theorem *10.301albitr 44640
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44641
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44642
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44643
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44644
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44646
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44647
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44648
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44645
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2096
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44651
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44652
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2076
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2166
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1831
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1832
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44653
[WhiteheadRussell] p. 162Theorem *11.322alim 44654
[WhiteheadRussell] p. 162Theorem *11.332albi 44655
[WhiteheadRussell] p. 162Theorem *11.342exim 44656
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44658
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44657
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1889
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44660
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44661
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44659
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1830
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44662
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44663
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1848
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44664
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2351
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1862
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44669
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44665
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44666
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44667
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44668
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44673
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44670
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44671
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44672
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44674
[WhiteheadRussell] p. 175Definition *14.02df-eu 2570
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44684  pm13.13b 44685
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44686
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3014
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3015
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3621
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44692
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44693
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44687
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44829  pm13.193 44688
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44689
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44690
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44691
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44698
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44697
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44696
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3804
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44699  pm14.122b 44700  pm14.122c 44701
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44702  pm14.123b 44703  pm14.123c 44704
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44706
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44705
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44707
[WhiteheadRussell] p. 190Theorem *14.22iota4 6474
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44708
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6475
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44709
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44711
[WhiteheadRussell] p. 192Theorem *14.26eupick 2634  eupickbi 2637  sbaniota 44712
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44710
[WhiteheadRussell] p. 192Theorem *14.271eubi 2585
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44713
[WhiteheadRussell] p. 235Definition *30.01conventions 30458  df-fv 6501
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9917  pm54.43lem 9916
[Young] p. 141Definition of operator orderingleop2 32182
[Young] p. 142Example 12.2(i)0leop 32188  idleop 32189
[vandenDries] p. 42Lemma 61irrapx1 43106
[vandenDries] p. 43Theorem 62pellex 43113  pellexlem1 43107

This page was last updated on 5-Mar-2026.
Copyright terms: Public domain