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 17730
[Adamek] p. 21Condition 3.1(b)df-cat 17730
[Adamek] p. 22Example 3.3(1)df-setc 18139
[Adamek] p. 24Example 3.3(4.c)0cat 17751  0funcg 49891  df-termc 50279
[Adamek] p. 24Example 3.3(4.d)df-prstc 50356  prsthinc 50270
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50384  df-mndtc 50384
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50380
[Adamek] p. 25Definition 3.5df-oppc 17774
[Adamek] p. 25Example 3.6(1)oduoppcciso 50372
[Adamek] p. 25Example 3.6(2)oppgoppcco 50397  oppgoppchom 50396  oppgoppcid 50398
[Adamek] p. 28Remark 3.9oppciso 17844
[Adamek] p. 28Remark 3.12invf1o 17832  invisoinvl 17853
[Adamek] p. 28Example 3.13idinv 17852  idiso 17851
[Adamek] p. 28Corollary 3.11inveq 17837
[Adamek] p. 28Definition 3.8df-inv 17811  df-iso 17812  dfiso2 17835
[Adamek] p. 28Proposition 3.10sectcan 17818
[Adamek] p. 29Remark 3.16cicer 17869  cicerALT 49852
[Adamek] p. 29Definition 3.15cic 17862  df-cic 17859
[Adamek] p. 29Definition 3.17df-func 17921
[Adamek] p. 29Proposition 3.14(1)invinv 17833
[Adamek] p. 29Proposition 3.14(2)invco 17834  isoco 17840
[Adamek] p. 30Remark 3.19df-func 17921
[Adamek] p. 30Example 3.20(1)idfucl 17944
[Adamek] p. 30Example 3.20(2)diag1 50110
[Adamek] p. 32Proposition 3.21funciso 17937
[Adamek] p. 33Example 3.26(1)discsnterm 50380  discthing 50267
[Adamek] p. 33Example 3.26(2)df-thinc 50224  prsthinc 50270  thincciso 50259  thincciso2 50261  thincciso3 50262  thinccisod 50260
[Adamek] p. 33Example 3.26(3)df-mndtc 50384
[Adamek] p. 33Proposition 3.23cofucl 17951  cofucla 49902
[Adamek] p. 34Remark 3.28(1)cofidfth 49968
[Adamek] p. 34Remark 3.28(2)catciso 18174  catcisoi 50206
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18229
[Adamek] p. 34Definition 3.27(2)df-fth 17970
[Adamek] p. 34Definition 3.27(3)df-full 17969
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18229
[Adamek] p. 35Corollary 3.32ffthiso 17994
[Adamek] p. 35Proposition 3.30(c)cofth 18000
[Adamek] p. 35Proposition 3.30(d)cofull 17999
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18214
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18214
[Adamek] p. 39Remark 3.422oppf 49938
[Adamek] p. 39Definition 3.41df-oppf 49929  funcoppc 17938
[Adamek] p. 39Definition 3.44.df-catc 18162  elcatchom 50203
[Adamek] p. 39Proposition 3.43(c)fthoppc 17988  fthoppf 49970
[Adamek] p. 39Proposition 3.43(d)fulloppc 17987  fulloppf 49969
[Adamek] p. 40Remark 3.48catccat 18171
[Adamek] p. 40Definition 3.470funcg 49891  df-catc 18162
[Adamek] p. 45Exercise 3Gincat 50407
[Adamek] p. 48Remark 4.2(2)cnelsubc 50410  nelsubc3 49877
[Adamek] p. 48Remark 4.2(3)imasubc 49957  imasubc2 49958  imasubc3 49962
[Adamek] p. 48Example 4.3(1.a)0subcat 17901
[Adamek] p. 48Example 4.3(1.b)catsubcat 17902
[Adamek] p. 48Definition 4.1(1)nelsubc3 49877
[Adamek] p. 48Definition 4.1(2)fullsubc 17913
[Adamek] p. 48Definition 4.1(a)df-subc 17875
[Adamek] p. 49Remark 4.4idsubc 49966
[Adamek] p. 49Remark 4.4(1)idemb 49965
[Adamek] p. 49Remark 4.4(2)idfullsubc 49967  ressffth 18003
[Adamek] p. 58Exercise 4Asetc1onsubc 50408
[Adamek] p. 83Definition 6.1df-nat 18009
[Adamek] p. 87Remark 6.14(a)fuccocl 18030
[Adamek] p. 87Remark 6.14(b)fucass 18034
[Adamek] p. 87Definition 6.15df-fuc 18010
[Adamek] p. 88Remark 6.16fuccat 18036
[Adamek] p. 101Definition 7.10funcg 49891  df-inito 18047
[Adamek] p. 101Example 7.2(3)0funcg 49891  df-termc 50279  initc 49897
[Adamek] p. 101Example 7.2 (6)irinitoringc 21640
[Adamek] p. 102Definition 7.4df-termo 18048  oppctermo 50042
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18075
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18079
[Adamek] p. 103Remark 7.8oppczeroo 50043
[Adamek] p. 103Definition 7.7df-zeroo 18049
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21641
[Adamek] p. 103Proposition 7.6termoeu1w 18082
[Adamek] p. 106Definition 7.19df-sect 17810
[Adamek] p. 107Example 7.20(7)thincinv 50275
[Adamek] p. 108Example 7.25(4)thincsect2 50274
[Adamek] p. 110Example 7.33(9)thincmon 50239
[Adamek] p. 110Proposition 7.35sectmon 17845
[Adamek] p. 112Proposition 7.42sectepi 17847
[Adamek] p. 185Section 10.67updjud 9927
[Adamek] p. 193Definition 11.1(1)df-lmd 50451
[Adamek] p. 193Definition 11.3(1)df-lmd 50451
[Adamek] p. 194Definition 11.3(2)df-lmd 50451
[Adamek] p. 202Definition 11.27(1)df-cmd 50452
[Adamek] p. 202Definition 11.27(2)df-cmd 50452
[Adamek] p. 478Item Rngdf-ringc 20756
[AhoHopUll] p. 2Section 1.1df-bigo 49356
[AhoHopUll] p. 12Section 1.3df-blen 49378
[AhoHopUll] p. 318Section 9.1df-concat 14615  df-pfx 14716  df-substr 14686  df-word 14558  lencl 14577  wrd0 14583
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24876  df-nmoo 31108
[AkhiezerGlazman] p. 64Theoremhmopidmch 32516  hmopidmchi 32514
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32564  pjcmul2i 32565
[AkhiezerGlazman] p. 72Theoremcnvunop 32281  unoplin 32283
[AkhiezerGlazman] p. 72Equation 2unopadj 32282  unopadj2 32301
[AkhiezerGlazman] p. 73Theoremelunop2 32376  lnopunii 32375
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32449
[Alling] p. 125Theorem 4.02(12)cofcutrtime 28131
[Alling] p. 184Axiom Bbdayfo 27852
[Alling] p. 184Axiom Oltsso 27851
[Alling] p. 184Axiom SDnodense 27867
[Alling] p. 185Lemma 0nocvxmin 27959
[Alling] p. 185Theoremconway 27983
[Alling] p. 185Axiom FEnoeta 27918
[Alling] p. 186Theorem 4lesrec 28003  lesrecd 28004
[Alling], p. 2Definitionrp-brsslt 44177
[Alling], p. 3Notenla0001 44180  nla0002 44178  nla0003 44179
[Apostol] p. 18Theorem I.1addcan 11400  addcan2d 11420  addcan2i 11410  addcand 11419  addcani 11409
[Apostol] p. 18Theorem I.2negeu 11453
[Apostol] p. 18Theorem I.3negsub 11512  negsubd 11581  negsubi 11542
[Apostol] p. 18Theorem I.4negneg 11514  negnegd 11566  negnegi 11534
[Apostol] p. 18Theorem I.5subdi 11653  subdid 11676  subdii 11669  subdir 11654  subdird 11677  subdiri 11670
[Apostol] p. 18Theorem I.6mul01 11395  mul01d 11415  mul01i 11406  mul02 11394  mul02d 11414  mul02i 11405
[Apostol] p. 18Theorem I.7mulcan 11857  mulcan2d 11854  mulcand 11853  mulcani 11859
[Apostol] p. 18Theorem I.8receu 11865  xreceu 33252
[Apostol] p. 18Theorem I.9divrec 11894  divrecd 12000  divreci 11966  divreczi 11959
[Apostol] p. 18Theorem I.10recrec 11918  recreci 11953
[Apostol] p. 18Theorem I.11mul0or 11860  mul0ord 11868  mul0ori 11867
[Apostol] p. 18Theorem I.12mul2neg 11659  mul2negd 11675  mul2negi 11668  mulneg1 11656  mulneg1d 11673  mulneg1i 11666
[Apostol] p. 18Theorem I.13divadddiv 11936  divadddivd 12041  divadddivi 11983
[Apostol] p. 18Theorem I.14divmuldiv 11921  divmuldivd 12038  divmuldivi 11981  rdivmuldivd 20502
[Apostol] p. 18Theorem I.15divdivdiv 11922  divdivdivd 12044  divdivdivi 11984
[Apostol] p. 20Axiom 7rpaddcl 13046  rpaddcld 13081  rpmulcl 13047  rpmulcld 13082
[Apostol] p. 20Axiom 8rpneg 13056
[Apostol] p. 20Axiom 90nrp 13059
[Apostol] p. 20Theorem I.17lttri 11342
[Apostol] p. 20Theorem I.18ltadd1d 11813  ltadd1dd 11831  ltadd1i 11774
[Apostol] p. 20Theorem I.19ltmul1 12071  ltmul1a 12070  ltmul1i 12139  ltmul1ii 12149  ltmul2 12072  ltmul2d 13108  ltmul2dd 13122  ltmul2i 12142
[Apostol] p. 20Theorem I.20msqgt0 11740  msqgt0d 11787  msqgt0i 11757
[Apostol] p. 20Theorem I.210lt1 11742
[Apostol] p. 20Theorem I.23lt0neg1 11726  lt0neg1d 11789  ltneg 11720  ltnegd 11798  ltnegi 11764
[Apostol] p. 20Theorem I.25lt2add 11705  lt2addd 11843  lt2addi 11782
[Apostol] p. 20Definition of positive numbersdf-rp 13023
[Apostol] p. 21Exercise 4recgt0 12067  recgt0d 12155  recgt0i 12126  recgt0ii 12127
[Apostol] p. 22Definition of integersdf-z 12598
[Apostol] p. 22Definition of positive integersdfnn3 12253
[Apostol] p. 22Definition of rationalsdf-q 12979
[Apostol] p. 24Theorem I.26supeu 9412
[Apostol] p. 26Theorem I.28nnunb 12506
[Apostol] p. 26Theorem I.29arch 12507  archd 45908
[Apostol] p. 28Exercise 2btwnz 12705
[Apostol] p. 28Exercise 3nnrecl 12508
[Apostol] p. 28Exercise 4rebtwnz 12977
[Apostol] p. 28Exercise 5zbtwnre 12976
[Apostol] p. 28Exercise 6qbtwnre 13231
[Apostol] p. 28Exercise 10(a)zeneo 16403  zneo 12685  zneoALTV 48462
[Apostol] p. 29Theorem I.35cxpsqrtth 26906  msqsqrtd 15501  resqrtth 15313  sqrtth 15423  sqrtthi 15429  sqsqrtd 15500
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12242
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12943
[Apostol] p. 361Remarkcrreczi 14271
[Apostol] p. 363Remarkabsgt0i 15458
[Apostol] p. 363Exampleabssubd 15514  abssubi 15462
[ApostolNT] p. 7Remarkfmtno0 48320  fmtno1 48321  fmtno2 48330  fmtno3 48331  fmtno4 48332  fmtno5fac 48362  fmtnofz04prm 48357
[ApostolNT] p. 7Definitiondf-fmtno 48308
[ApostolNT] p. 8Definitiondf-ppi 27275
[ApostolNT] p. 14Definitiondf-dvds 16317
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16333
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16358
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16353
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16346
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16348
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16334
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16335
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16340
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16375
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16377
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16379
[ApostolNT] p. 15Definitiondf-gcd 16559  dfgcd2 16610
[ApostolNT] p. 16Definitionisprm2 16746
[ApostolNT] p. 16Theorem 1.5coprmdvds 16717
[ApostolNT] p. 16Theorem 1.7prminf 16981
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16577
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16611
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16613
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16592
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16584
[ApostolNT] p. 17Theorem 1.8coprm 16776
[ApostolNT] p. 17Theorem 1.9euclemma 16778
[ApostolNT] p. 17Theorem 1.101arith2 16994
[ApostolNT] p. 18Theorem 1.13prmrec 16988
[ApostolNT] p. 19Theorem 1.14divalg 16467
[ApostolNT] p. 20Theorem 1.15eucalg 16651
[ApostolNT] p. 24Definitiondf-mu 27276
[ApostolNT] p. 25Definitiondf-phi 16831
[ApostolNT] p. 25Theorem 2.1musum 27366
[ApostolNT] p. 26Theorem 2.2phisum 16856
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16841
[ApostolNT] p. 28Theorem 2.5(c)phimul 16845
[ApostolNT] p. 32Definitiondf-vma 27273
[ApostolNT] p. 32Theorem 2.9muinv 27368
[ApostolNT] p. 32Theorem 2.10vmasum 27391
[ApostolNT] p. 38Remarkdf-sgm 27277
[ApostolNT] p. 38Definitiondf-sgm 27277
[ApostolNT] p. 75Definitiondf-chp 27274  df-cht 27272
[ApostolNT] p. 104Definitioncongr 16728
[ApostolNT] p. 106Remarkdvdsval3 16320
[ApostolNT] p. 106Definitionmoddvds 16327
[ApostolNT] p. 107Example 2mod2eq0even 16410
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16411
[ApostolNT] p. 107Example 4zmod1congr 13928
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13968
[ApostolNT] p. 107Theorem 5.2(c)modexp 14281
[ApostolNT] p. 108Theorem 5.3modmulconst 16352
[ApostolNT] p. 109Theorem 5.4cncongr1 16731
[ApostolNT] p. 109Theorem 5.6gcdmodi 17140
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16733
[ApostolNT] p. 113Theorem 5.17eulerth 16848
[ApostolNT] p. 113Theorem 5.18vfermltl 16867
[ApostolNT] p. 114Theorem 5.19fermltl 16849
[ApostolNT] p. 116Theorem 5.24wilthimp 27247
[ApostolNT] p. 179Definitiondf-lgs 27470  lgsprme0 27514
[ApostolNT] p. 180Example 11lgs 27515
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27491
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27506
[ApostolNT] p. 181Theorem 9.4m1lgs 27563
[ApostolNT] p. 181Theorem 9.52lgs 27582  2lgsoddprm 27591
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27549
[ApostolNT] p. 185Theorem 9.8lgsquad 27558
[ApostolNT] p. 188Definitiondf-lgs 27470  lgs1 27516
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27507
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27509
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27517
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27518
[Baer] p. 40Property (b)mapdord 42440
[Baer] p. 40Property (c)mapd11 42441
[Baer] p. 40Property (e)mapdin 42464  mapdlsm 42466
[Baer] p. 40Property (f)mapd0 42467
[Baer] p. 40Definition of projectivitydf-mapd 42427  mapd1o 42450
[Baer] p. 41Property (g)mapdat 42469
[Baer] p. 44Part (1)mapdpg 42508
[Baer] p. 45Part (2)hdmap1eq 42603  mapdheq 42530  mapdheq2 42531  mapdheq2biN 42532
[Baer] p. 45Part (3)baerlem3 42515
[Baer] p. 46Part (4)mapdheq4 42534  mapdheq4lem 42533
[Baer] p. 46Part (5)baerlem5a 42516  baerlem5abmN 42520  baerlem5amN 42518  baerlem5b 42517  baerlem5bmN 42519
[Baer] p. 47Part (6)hdmap1l6 42623  hdmap1l6a 42611  hdmap1l6e 42616  hdmap1l6f 42617  hdmap1l6g 42618  hdmap1l6lem1 42609  hdmap1l6lem2 42610  mapdh6N 42549  mapdh6aN 42537  mapdh6eN 42542  mapdh6fN 42543  mapdh6gN 42544  mapdh6lem1N 42535  mapdh6lem2N 42536
[Baer] p. 48Part 9hdmapval 42630
[Baer] p. 48Part 10hdmap10 42642
[Baer] p. 48Part 11hdmapadd 42645
[Baer] p. 48Part (6)hdmap1l6h 42619  mapdh6hN 42545
[Baer] p. 48Part (7)mapdh75cN 42555  mapdh75d 42556  mapdh75e 42554  mapdh75fN 42557  mapdh7cN 42551  mapdh7dN 42552  mapdh7eN 42550  mapdh7fN 42553
[Baer] p. 48Part (8)mapdh8 42590  mapdh8a 42577  mapdh8aa 42578  mapdh8ab 42579  mapdh8ac 42580  mapdh8ad 42581  mapdh8b 42582  mapdh8c 42583  mapdh8d 42585  mapdh8d0N 42584  mapdh8e 42586  mapdh8g 42587  mapdh8i 42588  mapdh8j 42589
[Baer] p. 48Part (9)mapdh9a 42591
[Baer] p. 48Equation 10mapdhvmap 42571
[Baer] p. 49Part 12hdmap11 42650  hdmapeq0 42646  hdmapf1oN 42667  hdmapneg 42648  hdmaprnN 42666  hdmaprnlem1N 42651  hdmaprnlem3N 42652  hdmaprnlem3uN 42653  hdmaprnlem4N 42655  hdmaprnlem6N 42656  hdmaprnlem7N 42657  hdmaprnlem8N 42658  hdmaprnlem9N 42659  hdmapsub 42649
[Baer] p. 49Part 14hdmap14lem1 42670  hdmap14lem10 42679  hdmap14lem1a 42668  hdmap14lem2N 42671  hdmap14lem2a 42669  hdmap14lem3 42672  hdmap14lem8 42677  hdmap14lem9 42678
[Baer] p. 50Part 14hdmap14lem11 42680  hdmap14lem12 42681  hdmap14lem13 42682  hdmap14lem14 42683  hdmap14lem15 42684  hgmapval 42689
[Baer] p. 50Part 15hgmapadd 42696  hgmapmul 42697  hgmaprnlem2N 42699  hgmapvs 42693
[Baer] p. 50Part 16hgmaprnN 42703
[Baer] p. 110Lemma 1hdmapip0com 42719
[Baer] p. 110Line 27hdmapinvlem1 42720
[Baer] p. 110Line 28hdmapinvlem2 42721
[Baer] p. 110Line 30hdmapinvlem3 42722
[Baer] p. 110Part 1.2hdmapglem5 42724  hgmapvv 42728
[Baer] p. 110Proposition 1hdmapinvlem4 42723
[Baer] p. 111Line 10hgmapvvlem1 42725
[Baer] p. 111Line 15hdmapg 42732  hdmapglem7 42731
[Bauer], p. 483Theorem 1.22irrexpq 26907  2irrexpqALT 26976
[BellMachover] p. 36Lemma 10.3idALT 24
[BellMachover] p. 97Definition 10.1df-eu 2596
[BellMachover] p. 460Notationdf-mo 2566
[BellMachover] p. 460Definitionmo3 2591
[BellMachover] p. 461Axiom Extax-ext 2734
[BellMachover] p. 462Theorem 1.1axextmo 2738
[BellMachover] p. 463Axiom Repaxrep5 5245
[BellMachover] p. 463Scheme Sepax-sep 5256
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37728  sepex 5262
[BellMachover] p. 466Problemaxpow2 5337
[BellMachover] p. 466Axiom Powaxpow3 5338
[BellMachover] p. 466Axiom Unionaxun2 7736
[BellMachover] p. 468Definitiondf-ord 6363
[BellMachover] p. 469Theorem 2.2(i)ordirr 6378
[BellMachover] p. 469Theorem 2.2(iii)onelon 6385  onelond 36699
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6380
[BellMachover] p. 471Definition of Ndf-om 7861
[BellMachover] p. 471Problem 2.5(ii)uniordint 7798
[BellMachover] p. 471Definition of Limdf-lim 6365
[BellMachover] p. 472Axiom Infzfinf2 9609
[BellMachover] p. 473Theorem 2.8limom 7876
[BellMachover] p. 477Equation 3.1df-r1 9734
[BellMachover] p. 478Definitionrankval2 9788  rankval2b 35501
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9752  r1ord3g 9749
[BellMachover] p. 480Axiom Regzfreg 9556
[BellMachover] p. 488Axiom ACac5 10467  dfac4 10113
[BellMachover] p. 490Definition of alephalephval3 10101
[BeltramettiCassinelli] p. 98Remarkatlatmstc 40121
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32716
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32758  chirredi 32757
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32746
[Beran] p. 3Definition of joinsshjval3 31717
[Beran] p. 39Theorem 2.3(i)cmcm2 31979  cmcm2i 31956  cmcm2ii 31961  cmt2N 40052
[Beran] p. 40Theorem 2.3(iii)lecm 31980  lecmi 31965  lecmii 31966
[Beran] p. 45Theorem 3.4cmcmlem 31954
[Beran] p. 49Theorem 4.2cm2j 31983  cm2ji 31988  cm2mi 31989
[Beran] p. 95Definitiondf-sh 31570  issh2 31572
[Beran] p. 95Lemma 3.1(S5)his5 31449
[Beran] p. 95Lemma 3.1(S6)his6 31462
[Beran] p. 95Lemma 3.1(S7)his7 31453
[Beran] p. 95Lemma 3.2(S8)ho01i 32191
[Beran] p. 95Lemma 3.2(S9)hoeq1 32193
[Beran] p. 95Lemma 3.2(S10)ho02i 32192
[Beran] p. 95Lemma 3.2(S11)hoeq2 32194
[Beran] p. 95Postulate (S1)ax-his1 31445  his1i 31463
[Beran] p. 95Postulate (S2)ax-his2 31446
[Beran] p. 95Postulate (S3)ax-his3 31447
[Beran] p. 95Postulate (S4)ax-his4 31448
[Beran] p. 96Definition of normdf-hnorm 31331  dfhnorm2 31485  normval 31487
[Beran] p. 96Definition for Cauchy sequencehcau 31547
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31336
[Beran] p. 96Definition of complete subspaceisch3 31604
[Beran] p. 96Definition of convergedf-hlim 31335  hlimi 31551
[Beran] p. 97Theorem 3.3(i)norm-i-i 31496  norm-i 31492
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31500  norm-ii 31501  normlem0 31472  normlem1 31473  normlem2 31474  normlem3 31475  normlem4 31476  normlem5 31477  normlem6 31478  normlem7 31479  normlem7tALT 31482
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31502  norm-iii 31503
[Beran] p. 98Remark 3.4bcs 31544  bcsiALT 31542  bcsiHIL 31543
[Beran] p. 98Remark 3.4(B)normlem9at 31484  normpar 31518  normpari 31517
[Beran] p. 98Remark 3.4(C)normpyc 31509  normpyth 31508  normpythi 31505
[Beran] p. 99Remarklnfn0 32410  lnfn0i 32405  lnop0 32329  lnop0i 32333
[Beran] p. 99Theorem 3.5(i)nmcexi 32389  nmcfnex 32416  nmcfnexi 32414  nmcopex 32392  nmcopexi 32390
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32417  nmcfnlbi 32415  nmcoplb 32393  nmcoplbi 32391
[Beran] p. 99Theorem 3.5(iii)lnfncon 32419  lnfnconi 32418  lnopcon 32398  lnopconi 32397
[Beran] p. 100Lemma 3.6normpar2i 31519
[Beran] p. 101Lemma 3.6norm3adifi 31516  norm3adifii 31511  norm3dif 31513  norm3difi 31510
[Beran] p. 102Theorem 3.7(i)chocunii 31664  pjhth 31756  pjhtheu 31757  pjpjhth 31788  pjpjhthi 31789  pjth 25609
[Beran] p. 102Theorem 3.7(ii)ococ 31769  ococi 31768
[Beran] p. 103Remark 3.8nlelchi 32424
[Beran] p. 104Theorem 3.9riesz3i 32425  riesz4 32427  riesz4i 32426
[Beran] p. 104Theorem 3.10cnlnadj 32442  cnlnadjeu 32441  cnlnadjeui 32440  cnlnadji 32439  cnlnadjlem1 32430  nmopadjlei 32451
[Beran] p. 106Theorem 3.11(i)adjeq0 32454
[Beran] p. 106Theorem 3.11(v)nmopadji 32453
[Beran] p. 106Theorem 3.11(ii)adjmul 32455
[Beran] p. 106Theorem 3.11(iv)adjadj 32299
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32465  nmopcoadji 32464
[Beran] p. 106Theorem 3.11(iii)adjadd 32456
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32466
[Beran] p. 106Theorem 3.11(viii)adjcoi 32463  pjadj2coi 32567  pjadjcoi 32524
[Beran] p. 107Definitiondf-ch 31584  isch2 31586
[Beran] p. 107Remark 3.12choccl 31669  isch3 31604  occl 31667  ocsh 31646  shoccl 31668  shocsh 31647
[Beran] p. 107Remark 3.12(B)ococin 31771
[Beran] p. 108Theorem 3.13chintcl 31695
[Beran] p. 109Property (i)pjadj2 32550  pjadj3 32551  pjadji 32048  pjadjii 32037
[Beran] p. 109Property (ii)pjidmco 32544  pjidmcoi 32540  pjidmi 32036
[Beran] p. 110Definition of projector orderingpjordi 32536
[Beran] p. 111Remarkho0val 32113  pjch1 32033
[Beran] p. 111Definitiondf-hfmul 32097  df-hfsum 32096  df-hodif 32095  df-homul 32094  df-hosum 32093
[Beran] p. 111Lemma 4.4(i)pjo 32034
[Beran] p. 111Lemma 4.4(ii)pjch 32057  pjchi 31795
[Beran] p. 111Lemma 4.4(iii)pjoc2 31802  pjoc2i 31801
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 32043
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32528  pjssmii 32044
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32527
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32526
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32531
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32529  pjssge0ii 32045
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32530  pjdifnormii 32046
[Bobzien] p. 116Statement T3stoic3 1805
[Bobzien] p. 117Statement T2stoic2a 1803
[Bobzien] p. 117Statement T4stoic4a 1806
[Bobzien] p. 117Conclusion the contradictorystoic1a 1801
[Bogachev] p. 16Definition 1.5df-oms 34691
[Bogachev] p. 17Lemma 1.5.4omssubadd 34699
[Bogachev] p. 17Example 1.5.2omsmon 34697
[Bogachev] p. 41Definition 1.11.2df-carsg 34701
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34721
[Bogachev] p. 116Definition 2.3.1df-itgm 34752  df-sitm 34730
[Bogachev] p. 118Chapter 2.4.4df-itgm 34752
[Bogachev] p. 118Definition 2.4.1df-sitg 34729
[Bollobas] p. 1Section I.1df-edg 29409  isuhgrop 29431  isusgrop 29523  isuspgrop 29522
[Bollobas] p. 2Section I.1df-isubgr 48654  df-subgr 29629  uhgrspan1 29664  uhgrspansubgr 29652
[Bollobas] p. 3Definitiondf-gric 48674  gricuspgr 48711  isuspgrim 48689
[Bollobas] p. 3Section I.1cusgrsize 29815  df-clnbgr 48612  df-cusgr 29773  df-nbgr 29694  fusgrmaxsize 29825
[Bollobas] p. 4Definitiondf-upwlks 48927  df-wlks 29960
[Bollobas] p. 4Section I.1finsumvtxdg2size 29911  finsumvtxdgeven 29913  fusgr1th 29912  fusgrvtxdgonume 29915  vtxdgoddnumeven 29914
[Bollobas] p. 5Notationdf-pths 30074
[Bollobas] p. 5Definitiondf-crcts 30146  df-cycls 30147  df-trls 30051  df-wlkson 29961
[Bollobas] p. 7Section I.1df-ushgr 29420
[BourbakiAlg1] p. 1Definition 1df-clintop 48993  df-cllaw 48979  df-mgm 18704  df-mgm2 49012
[BourbakiAlg1] p. 4Definition 5df-assintop 48994  df-asslaw 48981  df-sgrp 18783  df-sgrp2 49014
[BourbakiAlg1] p. 7Definition 8df-cmgm2 49013  df-comlaw 48980
[BourbakiAlg1] p. 12Definition 2df-mnd 18799
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33355  mndlactf1o 33359  mndractf1 33357  mndractf1o 33360
[BourbakiAlg1] p. 92Definition 1df-ring 20323
[BourbakiAlg1] p. 93Section I.8.1df-rng 20237
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 34032
[BourbakiAlg2] p. 113Chapter 5.assafld 34036  assarrginv 34035
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 34077  fldextrspunfld 34075  fldextrspunlem1 34074  fldextrspunlem2 34076  fldextrspunlsp 34073  fldextrspunlsplem 34072
[BourbakiCAlg2], p. 228Proposition 21arithidom 33836  dfufd2 33849
[BourbakiEns] p. Proposition 8fcof1 7285  fcofo 7286
[BourbakiTop1] p. Remarkxnegmnf 13242  xnegpnf 13241
[BourbakiTop1] p. Remark rexneg 13243
[BourbakiTop1] p. Remark 3ust0 24388  ustfilxp 24381
[BourbakiTop1] p. Axiom GT'tgpsubcn 24258
[BourbakiTop1] p. Criterionishmeo 23927
[BourbakiTop1] p. Example 1cstucnd 24451  iducn 24450  snfil 24032
[BourbakiTop1] p. Example 2neifil 24048
[BourbakiTop1] p. Theorem 1cnextcn 24235
[BourbakiTop1] p. Theorem 2ucnextcn 24471
[BourbakiTop1] p. Theorem 3df-hcmp 34356
[BourbakiTop1] p. Paragraph 3infil 24031
[BourbakiTop1] p. Definition 1df-ucn 24443  df-ust 24369  filintn0 24029  filn0 24030  istgp 24245  ucnprima 24449
[BourbakiTop1] p. Definition 2df-cfilu 24454
[BourbakiTop1] p. Definition 3df-cusp 24465  df-usp 24425  df-utop 24399  trust 24397
[BourbakiTop1] p. Definition 6df-pcmp 34255
[BourbakiTop1] p. Property V_issnei2 23284
[BourbakiTop1] p. Theorem 1(d)iscncl 23437
[BourbakiTop1] p. Condition F_Iustssel 24374
[BourbakiTop1] p. Condition U_Iustdiag 24377
[BourbakiTop1] p. Property V_iiinnei 23293
[BourbakiTop1] p. Property V_ivneiptopreu 23301  neissex 23295
[BourbakiTop1] p. Proposition 1neips 23281  neiss 23277  ucncn 24452  ustund 24390  ustuqtop 24414
[BourbakiTop1] p. Proposition 2cnpco 23435  neiptopreu 23301  utop2nei 24418  utop3cls 24419
[BourbakiTop1] p. Proposition 3fmucnd 24459  uspreg 24441  utopreg 24420
[BourbakiTop1] p. Proposition 4imasncld 23859  imasncls 23860  imasnopn 23858
[BourbakiTop1] p. Proposition 9cnpflf2 24168
[BourbakiTop1] p. Condition F_IIustincl 24376
[BourbakiTop1] p. Condition U_IIustinvel 24378
[BourbakiTop1] p. Property V_iiielnei 23279
[BourbakiTop1] p. Proposition 11cnextucn 24470
[BourbakiTop1] p. Condition F_IIbustbasel 24375
[BourbakiTop1] p. Condition U_IIIustexhalf 24379
[BourbakiTop1] p. Definition C'''df-cmp 23555
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 24014
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 23062
[BourbakiTop2] p. 195Definition 1df-ldlf 34252
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46804
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46806  stoweid 46805
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46743  stoweidlem10 46752  stoweidlem14 46756  stoweidlem15 46757  stoweidlem35 46777  stoweidlem36 46778  stoweidlem37 46779  stoweidlem38 46780  stoweidlem40 46782  stoweidlem41 46783  stoweidlem43 46785  stoweidlem44 46786  stoweidlem46 46788  stoweidlem5 46747  stoweidlem50 46792  stoweidlem52 46794  stoweidlem53 46795  stoweidlem55 46797  stoweidlem56 46798
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46765  stoweidlem24 46766  stoweidlem27 46769  stoweidlem28 46770  stoweidlem30 46772
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46776  stoweidlem59 46801  stoweidlem60 46802
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46787  stoweidlem49 46791  stoweidlem7 46749
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46773  stoweidlem39 46781  stoweidlem42 46784  stoweidlem48 46790  stoweidlem51 46793  stoweidlem54 46796  stoweidlem57 46799  stoweidlem58 46800
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46767
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46759
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46753  stoweidlem13 46755  stoweidlem26 46768  stoweidlem61 46803
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46760
[Bruck] p. 1Section I.1df-clintop 48993  df-mgm 18704  df-mgm2 49012
[Bruck] p. 23Section II.1df-sgrp 18783  df-sgrp2 49014
[Bruck] p. 28Theorem 3.2dfgrp3 19111
[ChoquetDD] p. 2Definition of mappingdf-mpt 5192
[Church] p. 129Section II.24df-ifp 1078  dfifp2 1079
[Clemente] p. 10Definition ITnatded 30765
[Clemente] p. 10Definition I` `m,nnatded 30765
[Clemente] p. 11Definition E=>m,nnatded 30765
[Clemente] p. 11Definition I=>m,nnatded 30765
[Clemente] p. 11Definition E` `(1)natded 30765
[Clemente] p. 11Definition E` `(2)natded 30765
[Clemente] p. 12Definition E` `m,n,pnatded 30765
[Clemente] p. 12Definition I` `n(1)natded 30765
[Clemente] p. 12Definition I` `n(2)natded 30765
[Clemente] p. 13Definition I` `m,n,pnatded 30765
[Clemente] p. 14Proof 5.11natded 30765
[Clemente] p. 14Definition E` `nnatded 30765
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30767  ex-natded5.2 30766
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30770  ex-natded5.3 30769
[Clemente] p. 18Theorem 5.5ex-natded5.5 30772
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30774  ex-natded5.7 30773
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30776  ex-natded5.8 30775
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30778  ex-natded5.13 30777
[Clemente] p. 32Definition I` `nnatded 30765
[Clemente] p. 32Definition E` `m,n,p,anatded 30765
[Clemente] p. 32Definition E` `n,tnatded 30765
[Clemente] p. 32Definition I` `n,tnatded 30765
[Clemente] p. 43Theorem 9.20ex-natded9.20 30779
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30780
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30782  ex-natded9.26 30781
[Cohen] p. 301Remarkrelogoprlem 26767
[Cohen] p. 301Property 2relogmul 26768  relogmuld 26801
[Cohen] p. 301Property 3relogdiv 26769  relogdivd 26802
[Cohen] p. 301Property 4relogexp 26772
[Cohen] p. 301Property 1alog1 26761
[Cohen] p. 301Property 1bloge 26762
[Cohen4] p. 348Observationrelogbcxpb 26963
[Cohen4] p. 349Propertyrelogbf 26967
[Cohen4] p. 352Definitionelogb 26946
[Cohen4] p. 361Property 2relogbmul 26953
[Cohen4] p. 361Property 3logbrec 26958  relogbdiv 26955
[Cohen4] p. 361Property 4relogbreexp 26951
[Cohen4] p. 361Property 6relogbexp 26956
[Cohen4] p. 361Property 1(a)logbid1 26944
[Cohen4] p. 361Property 1(b)logb1 26945
[Cohen4] p. 367Propertylogbchbase 26947
[Cohen4] p. 377Property 2logblt 26960
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34684  sxbrsigalem4 34686
[Cohn] p. 81Section II.5acsdomd 18619  acsinfd 18618  acsinfdimd 18620  acsmap2d 18617  acsmapd 18616
[Cohn] p. 143Example 5.1.1sxbrsiga 34689
[Connell] p. 57Definitiondf-scmat 22659  df-scmatalt 49207
[Conway] p. 4Definitionlesrec 28003  lesrecd 28004
[Conway] p. 5Definitionaddsval 28166  addsval2 28167  df-adds 28164  df-muls 28311  df-negs 28225
[Conway] p. 7Theorem0lt1s 28016
[Conway] p. 12Theorem 12pw2cut2 28666
[Conway] p. 16Theorem 0(i)sltsright 28065
[Conway] p. 16Theorem 0(ii)sltsleft 28064
[Conway] p. 16Theorem 0(iii)lesid 27942
[Conway] p. 17Theorem 3addsass 28209  addsassd 28210  addscom 28170  addscomd 28171  addsrid 28168  addsridd 28169
[Conway] p. 17Definitiondf-0s 28011
[Conway] p. 17Theorem 4(ii)negnegs 28248
[Conway] p. 17Theorem 4(iii)negsid 28245  negsidd 28246
[Conway] p. 18Theorem 5leadds1 28193  leadds1d 28199
[Conway] p. 18Definitiondf-1s 28012
[Conway] p. 18Theorem 6(ii)negscl 28240  negscld 28241
[Conway] p. 18Theorem 6(iii)addscld 28184
[Conway] p. 19Notemulsunif2 28374
[Conway] p. 19Theorem 7addsdi 28359  addsdid 28360  addsdird 28361  mulnegs1d 28364  mulnegs2d 28365  mulsass 28370  mulsassd 28371  mulscom 28343  mulscomd 28344
[Conway] p. 19Theorem 8(i)mulscl 28338  mulscld 28339
[Conway] p. 19Theorem 8(iii)lemulsd 28342  ltmuls 28340  ltmulsd 28341
[Conway] p. 20Theorem 9mulsgt0 28348  mulsgt0d 28349
[Conway] p. 21Theorem 10(iv)precsex 28422
[Conway] p. 23Theorem 11eqcuts3 28008
[Conway] p. 24Definitiondf-reno 28694
[Conway] p. 24Theorem 13(ii)readdscl 28703  remulscl 28706  renegscl 28702
[Conway] p. 27Definitiondf-ons 28456  elons2 28462
[Conway] p. 27Theorem 14ltonsex 28466
[Conway] p. 28Theorem 15oncutlt 28468  onswe 28476
[Conway] p. 29Remarkmadebday 28104  newbday 28106  oldbday 28105
[Conway] p. 29Definitiondf-made 28031  df-new 28033  df-old 28032
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13901
[Crawley] p. 1Definition of posetdf-poset 18375
[Crawley] p. 107Theorem 13.2hlsupr 40188
[Crawley] p. 110Theorem 13.3arglem1N 40992  dalaw 40688
[Crawley] p. 111Theorem 13.4hlathil 42763
[Crawley] p. 111Definition of set Wdf-watsN 40792
[Crawley] p. 111Definition of dilationdf-dilN 40908  df-ldil 40906  isldil 40912
[Crawley] p. 111Definition of translationdf-ltrn 40907  df-trnN 40909  isltrn 40921  ltrnu 40923
[Crawley] p. 112Lemma Acdlema1N 40593  cdlema2N 40594  exatleN 40206
[Crawley] p. 112Lemma B1cvrat 40278  cdlemb 40596  cdlemb2 40843  cdlemb3 41408  idltrn 40952  l1cvat 39857  lhpat 40845  lhpat2 40847  lshpat 39858  ltrnel 40941  ltrnmw 40953
[Crawley] p. 112Lemma Ccdlemc1 40993  cdlemc2 40994  ltrnnidn 40976  trlat 40971  trljat1 40968  trljat2 40969  trljat3 40970  trlne 40987  trlnidat 40975  trlnle 40988
[Crawley] p. 112Definition of automorphismdf-pautN 40793
[Crawley] p. 113Lemma Ccdlemc 40999  cdlemc3 40995  cdlemc4 40996
[Crawley] p. 113Lemma Dcdlemd 41009  cdlemd1 41000  cdlemd2 41001  cdlemd3 41002  cdlemd4 41003  cdlemd5 41004  cdlemd6 41005  cdlemd7 41006  cdlemd8 41007  cdlemd9 41008  cdleme31sde 41187  cdleme31se 41184  cdleme31se2 41185  cdleme31snd 41188  cdleme32a 41243  cdleme32b 41244  cdleme32c 41245  cdleme32d 41246  cdleme32e 41247  cdleme32f 41248  cdleme32fva 41239  cdleme32fva1 41240  cdleme32fvcl 41242  cdleme32le 41249  cdleme48fv 41301  cdleme4gfv 41309  cdleme50eq 41343  cdleme50f 41344  cdleme50f1 41345  cdleme50f1o 41348  cdleme50laut 41349  cdleme50ldil 41350  cdleme50lebi 41342  cdleme50rn 41347  cdleme50rnlem 41346  cdlemeg49le 41313  cdlemeg49lebilem 41341
[Crawley] p. 113Lemma Ecdleme 41362  cdleme00a 41011  cdleme01N 41023  cdleme02N 41024  cdleme0a 41013  cdleme0aa 41012  cdleme0b 41014  cdleme0c 41015  cdleme0cp 41016  cdleme0cq 41017  cdleme0dN 41018  cdleme0e 41019  cdleme0ex1N 41025  cdleme0ex2N 41026  cdleme0fN 41020  cdleme0gN 41021  cdleme0moN 41027  cdleme1 41029  cdleme10 41056  cdleme10tN 41060  cdleme11 41072  cdleme11a 41062  cdleme11c 41063  cdleme11dN 41064  cdleme11e 41065  cdleme11fN 41066  cdleme11g 41067  cdleme11h 41068  cdleme11j 41069  cdleme11k 41070  cdleme11l 41071  cdleme12 41073  cdleme13 41074  cdleme14 41075  cdleme15 41080  cdleme15a 41076  cdleme15b 41077  cdleme15c 41078  cdleme15d 41079  cdleme16 41087  cdleme16aN 41061  cdleme16b 41081  cdleme16c 41082  cdleme16d 41083  cdleme16e 41084  cdleme16f 41085  cdleme16g 41086  cdleme19a 41105  cdleme19b 41106  cdleme19c 41107  cdleme19d 41108  cdleme19e 41109  cdleme19f 41110  cdleme1b 41028  cdleme2 41030  cdleme20aN 41111  cdleme20bN 41112  cdleme20c 41113  cdleme20d 41114  cdleme20e 41115  cdleme20f 41116  cdleme20g 41117  cdleme20h 41118  cdleme20i 41119  cdleme20j 41120  cdleme20k 41121  cdleme20l 41124  cdleme20l1 41122  cdleme20l2 41123  cdleme20m 41125  cdleme20y 41104  cdleme20zN 41103  cdleme21 41139  cdleme21d 41132  cdleme21e 41133  cdleme22a 41142  cdleme22aa 41141  cdleme22b 41143  cdleme22cN 41144  cdleme22d 41145  cdleme22e 41146  cdleme22eALTN 41147  cdleme22f 41148  cdleme22f2 41149  cdleme22g 41150  cdleme23a 41151  cdleme23b 41152  cdleme23c 41153  cdleme26e 41161  cdleme26eALTN 41163  cdleme26ee 41162  cdleme26f 41165  cdleme26f2 41167  cdleme26f2ALTN 41166  cdleme26fALTN 41164  cdleme27N 41171  cdleme27a 41169  cdleme27cl 41168  cdleme28c 41174  cdleme3 41039  cdleme30a 41180  cdleme31fv 41192  cdleme31fv1 41193  cdleme31fv1s 41194  cdleme31fv2 41195  cdleme31id 41196  cdleme31sc 41186  cdleme31sdnN 41189  cdleme31sn 41182  cdleme31sn1 41183  cdleme31sn1c 41190  cdleme31sn2 41191  cdleme31so 41181  cdleme35a 41250  cdleme35b 41252  cdleme35c 41253  cdleme35d 41254  cdleme35e 41255  cdleme35f 41256  cdleme35fnpq 41251  cdleme35g 41257  cdleme35h 41258  cdleme35h2 41259  cdleme35sn2aw 41260  cdleme35sn3a 41261  cdleme36a 41262  cdleme36m 41263  cdleme37m 41264  cdleme38m 41265  cdleme38n 41266  cdleme39a 41267  cdleme39n 41268  cdleme3b 41031  cdleme3c 41032  cdleme3d 41033  cdleme3e 41034  cdleme3fN 41035  cdleme3fa 41038  cdleme3g 41036  cdleme3h 41037  cdleme4 41040  cdleme40m 41269  cdleme40n 41270  cdleme40v 41271  cdleme40w 41272  cdleme41fva11 41279  cdleme41sn3aw 41276  cdleme41sn4aw 41277  cdleme41snaw 41278  cdleme42a 41273  cdleme42b 41280  cdleme42c 41274  cdleme42d 41275  cdleme42e 41281  cdleme42f 41282  cdleme42g 41283  cdleme42h 41284  cdleme42i 41285  cdleme42k 41286  cdleme42ke 41287  cdleme42keg 41288  cdleme42mN 41289  cdleme42mgN 41290  cdleme43aN 41291  cdleme43bN 41292  cdleme43cN 41293  cdleme43dN 41294  cdleme5 41042  cdleme50ex 41361  cdleme50ltrn 41359  cdleme51finvN 41358  cdleme51finvfvN 41357  cdleme51finvtrN 41360  cdleme6 41043  cdleme7 41051  cdleme7a 41045  cdleme7aa 41044  cdleme7b 41046  cdleme7c 41047  cdleme7d 41048  cdleme7e 41049  cdleme7ga 41050  cdleme8 41052  cdleme8tN 41057  cdleme9 41055  cdleme9a 41053  cdleme9b 41054  cdleme9tN 41059  cdleme9taN 41058  cdlemeda 41100  cdlemedb 41099  cdlemednpq 41101  cdlemednuN 41102  cdlemefr27cl 41205  cdlemefr32fva1 41212  cdlemefr32fvaN 41211  cdlemefrs32fva 41202  cdlemefrs32fva1 41203  cdlemefs27cl 41215  cdlemefs32fva1 41225  cdlemefs32fvaN 41224  cdlemesner 41098  cdlemeulpq 41022
[Crawley] p. 114Lemma E4atex 40878  4atexlem7 40877  cdleme0nex 41092  cdleme17a 41088  cdleme17c 41090  cdleme17d 41300  cdleme17d1 41091  cdleme17d2 41297  cdleme18a 41093  cdleme18b 41094  cdleme18c 41095  cdleme18d 41097  cdleme4a 41041
[Crawley] p. 115Lemma Ecdleme21a 41127  cdleme21at 41130  cdleme21b 41128  cdleme21c 41129  cdleme21ct 41131  cdleme21f 41134  cdleme21g 41135  cdleme21h 41136  cdleme21i 41137  cdleme22gb 41096
[Crawley] p. 116Lemma Fcdlemf 41365  cdlemf1 41363  cdlemf2 41364
[Crawley] p. 116Lemma Gcdlemftr1 41369  cdlemg16 41459  cdlemg28 41506  cdlemg28a 41495  cdlemg28b 41505  cdlemg3a 41399  cdlemg42 41531  cdlemg43 41532  cdlemg44 41535  cdlemg44a 41533  cdlemg46 41537  cdlemg47 41538  cdlemg9 41436  ltrnco 41521  ltrncom 41540  tgrpabl 41553  trlco 41529
[Crawley] p. 116Definition of Gdf-tgrp 41545
[Crawley] p. 117Lemma Gcdlemg17 41479  cdlemg17b 41464
[Crawley] p. 117Definition of Edf-edring-rN 41558  df-edring 41559
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41562
[Crawley] p. 118Remarktendopltp 41582
[Crawley] p. 118Lemma Hcdlemh 41619  cdlemh1 41617  cdlemh2 41618
[Crawley] p. 118Lemma Icdlemi 41622  cdlemi1 41620  cdlemi2 41621
[Crawley] p. 118Lemma Jcdlemj1 41623  cdlemj2 41624  cdlemj3 41625  tendocan 41626
[Crawley] p. 118Lemma Kcdlemk 41776  cdlemk1 41633  cdlemk10 41645  cdlemk11 41651  cdlemk11t 41748  cdlemk11ta 41731  cdlemk11tb 41733  cdlemk11tc 41747  cdlemk11u-2N 41691  cdlemk11u 41673  cdlemk12 41652  cdlemk12u-2N 41692  cdlemk12u 41674  cdlemk13-2N 41678  cdlemk13 41654  cdlemk14-2N 41680  cdlemk14 41656  cdlemk15-2N 41681  cdlemk15 41657  cdlemk16-2N 41682  cdlemk16 41659  cdlemk16a 41658  cdlemk17-2N 41683  cdlemk17 41660  cdlemk18-2N 41688  cdlemk18-3N 41702  cdlemk18 41670  cdlemk19-2N 41689  cdlemk19 41671  cdlemk19u 41772  cdlemk1u 41661  cdlemk2 41634  cdlemk20-2N 41694  cdlemk20 41676  cdlemk21-2N 41693  cdlemk21N 41675  cdlemk22-3 41703  cdlemk22 41695  cdlemk23-3 41704  cdlemk24-3 41705  cdlemk25-3 41706  cdlemk26-3 41708  cdlemk26b-3 41707  cdlemk27-3 41709  cdlemk28-3 41710  cdlemk29-3 41713  cdlemk3 41635  cdlemk30 41696  cdlemk31 41698  cdlemk32 41699  cdlemk33N 41711  cdlemk34 41712  cdlemk35 41714  cdlemk36 41715  cdlemk37 41716  cdlemk38 41717  cdlemk39 41718  cdlemk39u 41770  cdlemk4 41636  cdlemk41 41722  cdlemk42 41743  cdlemk42yN 41746  cdlemk43N 41765  cdlemk45 41749  cdlemk46 41750  cdlemk47 41751  cdlemk48 41752  cdlemk49 41753  cdlemk5 41638  cdlemk50 41754  cdlemk51 41755  cdlemk52 41756  cdlemk53 41759  cdlemk54 41760  cdlemk55 41763  cdlemk55u 41768  cdlemk56 41773  cdlemk5a 41637  cdlemk5auN 41662  cdlemk5u 41663  cdlemk6 41639  cdlemk6u 41664  cdlemk7 41650  cdlemk7u-2N 41690  cdlemk7u 41672  cdlemk8 41640  cdlemk9 41641  cdlemk9bN 41642  cdlemki 41643  cdlemkid 41738  cdlemkj-2N 41684  cdlemkj 41665  cdlemksat 41648  cdlemksel 41647  cdlemksv 41646  cdlemksv2 41649  cdlemkuat 41668  cdlemkuel-2N 41686  cdlemkuel-3 41700  cdlemkuel 41667  cdlemkuv-2N 41685  cdlemkuv2-2 41687  cdlemkuv2-3N 41701  cdlemkuv2 41669  cdlemkuvN 41666  cdlemkvcl 41644  cdlemky 41728  cdlemkyyN 41764  tendoex 41777
[Crawley] p. 120Remarkdva1dim 41787
[Crawley] p. 120Lemma Lcdleml1N 41778  cdleml2N 41779  cdleml3N 41780  cdleml4N 41781  cdleml5N 41782  cdleml6 41783  cdleml7 41784  cdleml8 41785  cdleml9 41786  dia1dim 41863
[Crawley] p. 120Lemma Mdia11N 41850  diaf11N 41851  dialss 41848  diaord 41849  dibf11N 41963  djajN 41939
[Crawley] p. 120Definition of isomorphism mapdiaval 41834
[Crawley] p. 121Lemma Mcdlemm10N 41920  dia2dimlem1 41866  dia2dimlem2 41867  dia2dimlem3 41868  dia2dimlem4 41869  dia2dimlem5 41870  diaf1oN 41932  diarnN 41931  dvheveccl 41914  dvhopN 41918
[Crawley] p. 121Lemma Ncdlemn 42014  cdlemn10 42008  cdlemn11 42013  cdlemn11a 42009  cdlemn11b 42010  cdlemn11c 42011  cdlemn11pre 42012  cdlemn2 41997  cdlemn2a 41998  cdlemn3 41999  cdlemn4 42000  cdlemn4a 42001  cdlemn5 42003  cdlemn5pre 42002  cdlemn6 42004  cdlemn7 42005  cdlemn8 42006  cdlemn9 42007  diclspsn 41996
[Crawley] p. 121Definition of phi(q)df-dic 41975
[Crawley] p. 122Lemma Ndih11 42067  dihf11 42069  dihjust 42019  dihjustlem 42018  dihord 42066  dihord1 42020  dihord10 42025  dihord11b 42024  dihord11c 42026  dihord2 42029  dihord2a 42021  dihord2b 42022  dihord2cN 42023  dihord2pre 42027  dihord2pre2 42028  dihordlem6 42015  dihordlem7 42016  dihordlem7b 42017
[Crawley] p. 122Definition of isomorphism mapdihffval 42032  dihfval 42033  dihval 42034
[Diestel] p. 3Definitiondf-gric 48674  df-grim 48671  isuspgrim 48689
[Diestel] p. 3Section 1.1df-cusgr 29773  df-nbgr 29694
[Diestel] p. 3Definition by df-grisom 48670
[Diestel] p. 4Section 1.1df-isubgr 48654  df-subgr 29629  uhgrspan1 29664  uhgrspansubgr 29652
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29915  vtxdgoddnumeven 29914
[Diestel] p. 27Section 1.10df-ushgr 29420
[EGA] p. 80Notation 1.1.1rspecval 34263
[EGA] p. 80Proposition 1.1.2zartop 34275
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34267  zarcls1 34268
[EGA] p. 81Corollary 1.1.8zart0 34278
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34281
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34284
[Eisenberg] p. 67Definition 5.3df-dif 3907
[Eisenberg] p. 82Definition 6.3dfom3 9614
[Eisenberg] p. 125Definition 8.21df-map 8824
[Eisenberg] p. 216Example 13.2(4)omenps 9622
[Eisenberg] p. 310Theorem 19.8cardprc 9973
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10545
[Enderton] p. 18Axiom of Empty Setaxnul 5267
[Enderton] p. 19Definitiondf-tp 4593
[Enderton] p. 26Exercise 5unissb 4905
[Enderton] p. 26Exercise 10pwel 5351
[Enderton] p. 28Exercise 7(b)pwun 5553
[Enderton] p. 30Theorem "Distributive laws"iinin1 5044  iinin2 5043  iinun2 5036  iunin1 5035  iunin1f 32913  iunin2 5034  uniin1 5038  uniin2 5039
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5042  iundif2 5037
[Enderton] p. 32Exercise 20unineq 4240
[Enderton] p. 33Exercise 23iinuni 5063
[Enderton] p. 33Exercise 25iununi 5064
[Enderton] p. 33Exercise 24(a)iinpw 5071
[Enderton] p. 33Exercise 24(b)iunpw 7768  iunpwss 5072
[Enderton] p. 36Definitionopthwiener 5496
[Enderton] p. 38Exercise 6(a)unipw 5430
[Enderton] p. 38Exercise 6(b)pwuni 4910
[Enderton] p. 41Lemma 3Dopeluu 5451  rnex 7905  rnexg 7897
[Enderton] p. 41Exercise 8dmuni 5903  rnuni 6145
[Enderton] p. 42Definition of a functiondffun7 6563  dffun8 6564
[Enderton] p. 43Definition of function valuefunfv2 6969
[Enderton] p. 43Definition of single-rootedfuncnv 6605
[Enderton] p. 44Definition (d)dfima2 6063  dfima3 6064
[Enderton] p. 47Theorem 3Hfvco2 6978
[Enderton] p. 49Axiom of Choice (first form)ac7 10463  ac7g 10464  df-ac 10107  dfac2 10122  dfac2a 10120  dfac2b 10121  dfac3 10112  dfac7 10123
[Enderton] p. 50Theorem 3K(a)imauni 7244
[Enderton] p. 52Definitiondf-map 8824
[Enderton] p. 53Exercise 21coass 6266
[Enderton] p. 53Exercise 27dmco 6255
[Enderton] p. 53Exercise 14(a)funin 6612
[Enderton] p. 53Exercise 22(a)imass2 6103
[Enderton] p. 54Remarkixpf 8916  ixpssmap 8928
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8894
[Enderton] p. 55Axiom of Choice (second form)ac9 10473  ac9s 10483
[Enderton] p. 56Theorem 3Meqvrelref 39371  erref 8713
[Enderton] p. 57Lemma 3Neqvrelthi 39374  erthi 8749
[Enderton] p. 57Definitiondf-ec 8694
[Enderton] p. 58Definitiondf-qs 8698
[Enderton] p. 61Exercise 35df-ec 8694
[Enderton] p. 65Exercise 56(a)dmun 5899
[Enderton] p. 68Definition of successordf-suc 6366
[Enderton] p. 71Definitiondf-tr 5218  dftr4 5223
[Enderton] p. 72Theorem 4Eunisuc 6442  unisucg 6441
[Enderton] p. 73Exercise 6unisuc 6442  unisucg 6441
[Enderton] p. 73Exercise 5(a)truni 5233
[Enderton] p. 73Exercise 5(b)trint 5235  trintALT 45617
[Enderton] p. 79Theorem 4I(A1)nna0 8588
[Enderton] p. 79Theorem 4I(A2)nnasuc 8590  onasuc 8511
[Enderton] p. 79Definition of operation valuedf-ov 7415
[Enderton] p. 80Theorem 4J(A1)nnm0 8589
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8591  onmsuc 8512
[Enderton] p. 81Theorem 4K(1)nnaass 8606
[Enderton] p. 81Theorem 4K(2)nna0r 8593  nnacom 8601
[Enderton] p. 81Theorem 4K(3)nndi 8607
[Enderton] p. 81Theorem 4K(4)nnmass 8608
[Enderton] p. 81Theorem 4K(5)nnmcom 8610
[Enderton] p. 82Exercise 16nnm0r 8594  nnmsucr 8609
[Enderton] p. 88Exercise 23nnaordex 8622
[Enderton] p. 129Definitiondf-en 8942
[Enderton] p. 132Theorem 6B(b)canth 7366
[Enderton] p. 133Exercise 1xpomen 10006
[Enderton] p. 133Exercise 2qnnen 16275
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9189
[Enderton] p. 135Corollary 6Cphp3 9191
[Enderton] p. 136Corollary 6Enneneq 9188
[Enderton] p. 136Corollary 6D(a)pssinf 9220
[Enderton] p. 136Corollary 6D(b)ominf 9222
[Enderton] p. 137Lemma 6Fpssnn 9151
[Enderton] p. 138Corollary 6Gssfi 9155
[Enderton] p. 139Theorem 6H(c)mapen 9127
[Enderton] p. 142Theorem 6I(3)xpdjuen 10170
[Enderton] p. 142Theorem 6I(4)mapdjuen 10171
[Enderton] p. 143Theorem 6Jdju0en 10166  dju1en 10162
[Enderton] p. 144Exercise 13iunfi 9298  unifi 9299  unifi2 9300
[Enderton] p. 144Corollary 6Kundif2 4437  unfi 9153  unfi2 9268
[Enderton] p. 145Figure 38ffoss 7941
[Enderton] p. 145Definitiondf-dom 8943
[Enderton] p. 146Example 1domen 8956  domeng 8957
[Enderton] p. 146Example 3nndomo 9200  nnsdom 9621  nnsdomg 9257
[Enderton] p. 149Theorem 6L(a)djudom2 10174
[Enderton] p. 149Theorem 6L(c)mapdom1 9128  xpdom1 9062  xpdom1g 9060  xpdom2g 9059
[Enderton] p. 149Theorem 6L(d)mapdom2 9134
[Enderton] p. 151Theorem 6Mzorn 10497  zorng 10494
[Enderton] p. 151Theorem 6M(4)ac8 10482  dfac5 10119
[Enderton] p. 159Theorem 6Qunictb 10566
[Enderton] p. 164Exampleinfdif 10198
[Enderton] p. 168Definitiondf-po 5568
[Enderton] p. 192Theorem 7M(a)oneli 6476
[Enderton] p. 192Theorem 7M(b)ontr1 6408
[Enderton] p. 192Theorem 7M(c)onirri 6475
[Enderton] p. 193Corollary 7N(b)0elon 6416
[Enderton] p. 193Corollary 7N(c)onsuci 7833
[Enderton] p. 193Corollary 7N(d)ssonunii 7778
[Enderton] p. 194Remarkonprc 7775
[Enderton] p. 194Exercise 16suc11 6470
[Enderton] p. 197Definitiondf-card 9932
[Enderton] p. 197Theorem 7Pcarden 10541
[Enderton] p. 200Exercise 25tfis 7849
[Enderton] p. 202Lemma 7Tr1tr 9746
[Enderton] p. 202Definitiondf-r1 9734
[Enderton] p. 202Theorem 7Qr1val1 9756
[Enderton] p. 204Theorem 7V(b)rankval4 9837  rankval4b 35502
[Enderton] p. 206Theorem 7X(b)en2lp 9573
[Enderton] p. 207Exercise 30rankpr 9827  rankprb 9821  rankpw 9813  rankpwi 9793  rankuniss 9836
[Enderton] p. 207Exercise 34opthreg 9585
[Enderton] p. 208Exercise 35suc11reg 9586
[Enderton] p. 212Definition of alephalephval3 10101
[Enderton] p. 213Theorem 8A(a)alephord2 10067
[Enderton] p. 213Theorem 8A(b)cardalephex 10081
[Enderton] p. 218Theorem Schema 8Eonfununi 8326
[Enderton] p. 222Definitiondf-kard 35571
[Enderton] p. 222Definition of kardkarden 9886  kardex 9884
[Enderton] p. 238Theorem 8Roeoa 8581
[Enderton] p. 238Theorem 8Soeoe 8583
[Enderton] p. 240Exercise 25oarec 8545
[Enderton] p. 257Definition of cofinalitycflm 10239
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17704
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17646
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18615  mrieqv2d 17701  mrieqvd 17700
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17705
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17710  mreexexlem2d 17707
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18621  mreexfidimd 17712
[Frege1879] p. 11Statementdf3or2 44522
[Frege1879] p. 12Statementdf3an2 44523  dfxor4 44520  dfxor5 44521
[Frege1879] p. 26Axiom 1ax-frege1 44544
[Frege1879] p. 26Axiom 2ax-frege2 44545
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44549
[Frege1879] p. 31Proposition 4frege4 44553
[Frege1879] p. 32Proposition 5frege5 44554
[Frege1879] p. 33Proposition 6frege6 44560
[Frege1879] p. 34Proposition 7frege7 44562
[Frege1879] p. 35Axiom 8ax-frege8 44563  axfrege8 44561
[Frege1879] p. 35Proposition 8pm2.04 91  wl-luk-pm2.04 38119
[Frege1879] p. 35Proposition 9frege9 44566
[Frege1879] p. 36Proposition 10frege10 44574
[Frege1879] p. 36Proposition 11frege11 44568
[Frege1879] p. 37Proposition 12frege12 44567
[Frege1879] p. 37Proposition 13frege13 44576
[Frege1879] p. 37Proposition 14frege14 44577
[Frege1879] p. 38Proposition 15frege15 44580
[Frege1879] p. 38Proposition 16frege16 44570
[Frege1879] p. 39Proposition 17frege17 44575
[Frege1879] p. 39Proposition 18frege18 44572
[Frege1879] p. 39Proposition 19frege19 44578
[Frege1879] p. 40Proposition 20frege20 44582
[Frege1879] p. 40Proposition 21frege21 44581
[Frege1879] p. 41Proposition 22frege22 44573
[Frege1879] p. 42Proposition 23frege23 44579
[Frege1879] p. 42Proposition 24frege24 44569
[Frege1879] p. 42Proposition 25frege25 44571  rp-frege25 44559
[Frege1879] p. 42Proposition 26frege26 44564
[Frege1879] p. 43Axiom 28ax-frege28 44584
[Frege1879] p. 43Proposition 27frege27 44565
[Frege1879] p. 43Proposition 28con3 154
[Frege1879] p. 43Proposition 29frege29 44585
[Frege1879] p. 44Axiom 31ax-frege31 44588  axfrege31 44587
[Frege1879] p. 44Proposition 30frege30 44586
[Frege1879] p. 44Proposition 31notnotr 131
[Frege1879] p. 44Proposition 32frege32 44589
[Frege1879] p. 44Proposition 33frege33 44590
[Frege1879] p. 45Proposition 34frege34 44591
[Frege1879] p. 45Proposition 35frege35 44592
[Frege1879] p. 45Proposition 36frege36 44593
[Frege1879] p. 46Proposition 37frege37 44594
[Frege1879] p. 46Proposition 38frege38 44595
[Frege1879] p. 46Proposition 39frege39 44596
[Frege1879] p. 46Proposition 40frege40 44597
[Frege1879] p. 47Axiom 41ax-frege41 44599  axfrege41 44598
[Frege1879] p. 47Proposition 41notnot 143
[Frege1879] p. 47Proposition 42frege42 44600
[Frege1879] p. 47Proposition 43frege43 44601
[Frege1879] p. 47Proposition 44frege44 44602
[Frege1879] p. 47Proposition 45frege45 44603
[Frege1879] p. 48Proposition 46frege46 44604
[Frege1879] p. 48Proposition 47frege47 44605
[Frege1879] p. 49Proposition 48frege48 44606
[Frege1879] p. 49Proposition 49frege49 44607
[Frege1879] p. 49Proposition 50frege50 44608
[Frege1879] p. 50Axiom 52ax-frege52a 44611  ax-frege52c 44642  frege52aid 44612  frege52b 44643
[Frege1879] p. 50Axiom 54ax-frege54a 44616  ax-frege54c 44646  frege54b 44647
[Frege1879] p. 50Proposition 51frege51 44609
[Frege1879] p. 50Proposition 52dfsbcq 3745
[Frege1879] p. 50Proposition 53frege53a 44614  frege53aid 44613  frege53b 44644  frege53c 44668
[Frege1879] p. 50Proposition 54biid 264  eqid 2762
[Frege1879] p. 50Proposition 55frege55a 44622  frege55aid 44619  frege55b 44651  frege55c 44672  frege55cor1a 44623  frege55lem2a 44621  frege55lem2b 44650  frege55lem2c 44671
[Frege1879] p. 50Proposition 56frege56a 44625  frege56aid 44624  frege56b 44652  frege56c 44673
[Frege1879] p. 51Axiom 58ax-frege58a 44629  ax-frege58b 44655  frege58bid 44656  frege58c 44675
[Frege1879] p. 51Proposition 57frege57a 44627  frege57aid 44626  frege57b 44653  frege57c 44674
[Frege1879] p. 51Proposition 58spsbc 3756
[Frege1879] p. 51Proposition 59frege59a 44631  frege59b 44658  frege59c 44676
[Frege1879] p. 52Proposition 60frege60a 44632  frege60b 44659  frege60c 44677
[Frege1879] p. 52Proposition 61frege61a 44633  frege61b 44660  frege61c 44678
[Frege1879] p. 52Proposition 62frege62a 44634  frege62b 44661  frege62c 44679
[Frege1879] p. 52Proposition 63frege63a 44635  frege63b 44662  frege63c 44680
[Frege1879] p. 53Proposition 64frege64a 44636  frege64b 44663  frege64c 44681
[Frege1879] p. 53Proposition 65frege65a 44637  frege65b 44664  frege65c 44682
[Frege1879] p. 54Proposition 66frege66a 44638  frege66b 44665  frege66c 44683
[Frege1879] p. 54Proposition 67frege67a 44639  frege67b 44666  frege67c 44684
[Frege1879] p. 54Proposition 68frege68a 44640  frege68b 44667  frege68c 44685
[Frege1879] p. 55Definition 69dffrege69 44686
[Frege1879] p. 58Proposition 70frege70 44687
[Frege1879] p. 59Proposition 71frege71 44688
[Frege1879] p. 59Proposition 72frege72 44689
[Frege1879] p. 59Proposition 73frege73 44690
[Frege1879] p. 60Definition 76dffrege76 44693
[Frege1879] p. 60Proposition 74frege74 44691
[Frege1879] p. 60Proposition 75frege75 44692
[Frege1879] p. 62Proposition 77frege77 44694  frege77d 44500
[Frege1879] p. 63Proposition 78frege78 44695
[Frege1879] p. 63Proposition 79frege79 44696
[Frege1879] p. 63Proposition 80frege80 44697
[Frege1879] p. 63Proposition 81frege81 44698  frege81d 44501
[Frege1879] p. 64Proposition 82frege82 44699
[Frege1879] p. 65Proposition 83frege83 44700  frege83d 44502
[Frege1879] p. 65Proposition 84frege84 44701
[Frege1879] p. 66Proposition 85frege85 44702
[Frege1879] p. 66Proposition 86frege86 44703
[Frege1879] p. 66Proposition 87frege87 44704  frege87d 44504
[Frege1879] p. 67Proposition 88frege88 44705
[Frege1879] p. 68Proposition 89frege89 44706
[Frege1879] p. 68Proposition 90frege90 44707
[Frege1879] p. 68Proposition 91frege91 44708  frege91d 44505
[Frege1879] p. 69Proposition 92frege92 44709
[Frege1879] p. 70Proposition 93frege93 44710
[Frege1879] p. 70Proposition 94frege94 44711
[Frege1879] p. 70Proposition 95frege95 44712
[Frege1879] p. 71Definition 99dffrege99 44716
[Frege1879] p. 71Proposition 96frege96 44713  frege96d 44503
[Frege1879] p. 71Proposition 97frege97 44714  frege97d 44506
[Frege1879] p. 71Proposition 98frege98 44715  frege98d 44507
[Frege1879] p. 72Proposition 100frege100 44717
[Frege1879] p. 72Proposition 101frege101 44718
[Frege1879] p. 72Proposition 102frege102 44719  frege102d 44508
[Frege1879] p. 73Proposition 103frege103 44720
[Frege1879] p. 73Proposition 104frege104 44721
[Frege1879] p. 73Proposition 105frege105 44722
[Frege1879] p. 73Proposition 106frege106 44723  frege106d 44509
[Frege1879] p. 74Proposition 107frege107 44724
[Frege1879] p. 74Proposition 108frege108 44725  frege108d 44510
[Frege1879] p. 74Proposition 109frege109 44726  frege109d 44511
[Frege1879] p. 75Proposition 110frege110 44727
[Frege1879] p. 75Proposition 111frege111 44728  frege111d 44513
[Frege1879] p. 76Proposition 112frege112 44729
[Frege1879] p. 76Proposition 113frege113 44730
[Frege1879] p. 76Proposition 114frege114 44731  frege114d 44512
[Frege1879] p. 77Definition 115dffrege115 44732
[Frege1879] p. 77Proposition 116frege116 44733
[Frege1879] p. 78Proposition 117frege117 44734
[Frege1879] p. 78Proposition 118frege118 44735
[Frege1879] p. 78Proposition 119frege119 44736
[Frege1879] p. 78Proposition 120frege120 44737
[Frege1879] p. 79Proposition 121frege121 44738
[Frege1879] p. 79Proposition 122frege122 44739  frege122d 44514
[Frege1879] p. 79Proposition 123frege123 44740
[Frege1879] p. 80Proposition 124frege124 44741  frege124d 44515
[Frege1879] p. 81Proposition 125frege125 44742
[Frege1879] p. 81Proposition 126frege126 44743  frege126d 44516
[Frege1879] p. 82Proposition 127frege127 44744
[Frege1879] p. 83Proposition 128frege128 44745
[Frege1879] p. 83Proposition 129frege129 44746  frege129d 44517
[Frege1879] p. 84Proposition 130frege130 44747
[Frege1879] p. 85Proposition 131frege131 44748  frege131d 44518
[Frege1879] p. 86Proposition 132frege132 44749
[Frege1879] p. 86Proposition 133frege133 44750  frege133d 44519
[Fremlin1] p. 13Definition 111G (b)df-salgen 47055
[Fremlin1] p. 13Definition 111G (d)borelmbl 47378
[Fremlin1] p. 13Proposition 111G (b)salgenss 47078
[Fremlin1] p. 14Definition 112Aismea 47193
[Fremlin1] p. 15Remark 112B (d)psmeasure 47213
[Fremlin1] p. 15Property 112C (a)meadjun 47204  meadjunre 47218
[Fremlin1] p. 15Property 112C (b)meassle 47205
[Fremlin1] p. 15Property 112C (c)meaunle 47206
[Fremlin1] p. 16Property 112C (d)iundjiun 47202  meaiunle 47211  meaiunlelem 47210
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47223  meaiuninc2 47224  meaiuninc3 47227  meaiuninc3v 47226  meaiunincf 47225  meaiuninclem 47222
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47229  meaiininc2 47230  meaiininclem 47228
[Fremlin1] p. 19Theorem 113Ccaragen0 47248  caragendifcl 47256  caratheodory 47270  omelesplit 47260
[Fremlin1] p. 19Definition 113Aisome 47236  isomennd 47273  isomenndlem 47272
[Fremlin1] p. 19Remark 113B (c)omeunle 47258
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47277  voncmpl 47363
[Fremlin1] p. 19Definition 113A (ii)omessle 47240
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47265  carageniuncllem1 47263  carageniuncllem2 47264  caragenuncl 47255  caragenuncllem 47254  caragenunicl 47266
[Fremlin1] p. 21Remark 113Dcaragenel2d 47274
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47268  caratheodorylem2 47269
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47277
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47336  hoidmv1lelem1 47333  hoidmv1lelem2 47334  hoidmv1lelem3 47335
[Fremlin1] p. 25Definition 114Eisvonmbl 47380
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47336  hoidmvle 47342  hoidmvlelem1 47337  hoidmvlelem2 47338  hoidmvlelem3 47339  hoidmvlelem4 47340  hoidmvlelem5 47341  hsphoidmvle2 47327  hsphoif 47318  hsphoival 47321
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47290
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47298
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47325  hoidmvn0val 47326  hoidmvval 47319  hoidmvval0 47329  hoidmvval0b 47332
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47330  hsphoidmvle 47328
[Fremlin1] p. 30Definition 115Cdf-ovoln 47279  df-voln 47281
[Fremlin1] p. 30Proposition 115D (a)dmovn 47346  ovn0 47308  ovn0lem 47307  ovnf 47305  ovnome 47315  ovnssle 47303  ovnsslelem 47302  ovnsupge0 47299
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47345  ovnhoilem1 47343  ovnhoilem2 47344  vonhoi 47409
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47362  hoidifhspf 47360  hoidifhspval 47350  hoidifhspval2 47357  hoidifhspval3 47361  hspmbl 47371  hspmbllem1 47368  hspmbllem2 47369  hspmbllem3 47370
[Fremlin1] p. 31Definition 115Evoncmpl 47363  vonmea 47316
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47314  ovnsubadd2 47388  ovnsubadd2lem 47387  ovnsubaddlem1 47312  ovnsubaddlem2 47313
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47373  hoimbl2 47407  hoimbllem 47372  hspdifhsp 47358  opnvonmbl 47376  opnvonmbllem2 47375
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47378
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47421  iccvonmbllem 47420  ioovonmbl 47419
[Fremlin1] p. 32Proposition 115G (d)vonicc 47427  vonicclem2 47426  vonioo 47424  vonioolem2 47423  vonn0icc 47430  vonn0icc2 47434  vonn0ioo 47429  vonn0ioo2 47432
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47431  snvonmbl 47428  vonct 47435  vonsn 47433
[Fremlin1] p. 35Lemma 121Asubsalsal 47101
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 47100  subsaliuncllem 47099
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47467  salpreimalegt 47451  salpreimaltle 47468
[Fremlin1] p. 35Proposition 121B (i)issmf 47470  issmff 47476  issmflem 47469
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47487  issmflelem 47486  smfpreimale 47496
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47498  issmfgtlem 47497
[Fremlin1] p. 36Definition 121Cdf-smblfn 47438  issmf 47470  issmff 47476  issmfge 47512  issmfgelem 47511  issmfgt 47498  issmfgtlem 47497  issmfle 47487  issmflelem 47486  issmflem 47469
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47449  salpreimagtlt 47472  salpreimalelt 47471
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47512  issmfgelem 47511
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47495
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47493  cnfsmf 47482
[Fremlin1] p. 36Proposition 121D (c)decsmf 47509  decsmflem 47508  incsmf 47484  incsmflem 47483
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47443  pimconstlt1 47444  smfconst 47491
[Fremlin1] p. 37Proposition 121E (b)smfadd 47507  smfaddlem1 47505  smfaddlem2 47506
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47538
[Fremlin1] p. 37Proposition 121E (d)smfmul 47537  smfmullem1 47533  smfmullem2 47534  smfmullem3 47535  smfmullem4 47536
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47539
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47542  smfpimbor1lem2 47541
[Fremlin1] p. 37Proposition 121E (g)smfco 47544
[Fremlin1] p. 37Proposition 121E (h)smfres 47532
[Fremlin1] p. 38Proposition 121E (e)smfrec 47531
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47540  smfresal 47530
[Fremlin1] p. 38Proposition 121F (a)smflim 47519  smflim2 47548  smflimlem1 47513  smflimlem2 47514  smflimlem3 47515  smflimlem4 47516  smflimlem5 47517  smflimlem6 47518  smflimmpt 47552
[Fremlin1] p. 38Proposition 121F (b)smfsup 47556  smfsuplem1 47553  smfsuplem2 47554  smfsuplem3 47555  smfsupmpt 47557  smfsupxr 47558
[Fremlin1] p. 38Proposition 121F (c)smfinf 47560  smfinflem 47559  smfinfmpt 47561
[Fremlin1] p. 39Remark 121Gsmflim 47519  smflim2 47548  smflimmpt 47552
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47550
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47580  smfdivdmmbl2 47583  smfinfdmmbl 47591  smfinfdmmbllem 47590  smfsupdmmbl 47587  smfsupdmmbllem 47586
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47570  smflimsuplem2 47563  smflimsuplem6 47567  smflimsuplem7 47568  smflimsuplem8 47569  smflimsupmpt 47571
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47573  smfliminflem 47572  smfliminfmpt 47574
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47438
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47584  fsupdm2 47585
[Fremlin1], p. 39Proposition 121Hadddmmbl 47575  adddmmbl2 47576  finfdm 47588  finfdm2 47589  fsupdm 47584  fsupdm2 47585  muldmmbl 47577  muldmmbl2 47578
[Fremlin1], p. 39Proposition 121F (c)finfdm 47588  finfdm2 47589
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25706
[Fremlin5] p. 213Lemma 565Cauniioovol 25749
[Fremlin5] p. 214Lemma 565Cauniioombl 25759
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38377
[Fremlin5] p. 220Theorem 565Maftc1anc 38380
[FreydScedrov] p. 283Axiom of Infinityax-inf 9605  inf1 9589  inf2 9590
[Gleason] p. 117Proposition 9-2.1df-enq 10902  enqer 10912
[Gleason] p. 117Proposition 9-2.2df-1nq 10907  df-nq 10903
[Gleason] p. 117Proposition 9-2.3df-plpq 10899  df-plq 10905
[Gleason] p. 119Proposition 9-2.4caovmo 7649  df-mpq 10900  df-mq 10906
[Gleason] p. 119Proposition 9-2.5df-rq 10908
[Gleason] p. 119Proposition 9-2.6ltexnq 10966
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10967  ltbtwnnq 10969
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10962
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10963
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10970
[Gleason] p. 121Definition 9-3.1df-np 10972
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10984
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10986
[Gleason] p. 122Definitiondf-1p 10973
[Gleason] p. 122Remark (1)prub 10985
[Gleason] p. 122Lemma 9-3.4prlem934 11024
[Gleason] p. 122Proposition 9-3.2df-ltp 10976
[Gleason] p. 122Proposition 9-3.3ltsopr 11023  psslinpr 11022  supexpr 11045  suplem1pr 11043  suplem2pr 11044
[Gleason] p. 123Proposition 9-3.5addclpr 11009  addclprlem1 11007  addclprlem2 11008  df-plp 10974
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11013
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11012
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11025
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11034  ltexprlem1 11027  ltexprlem2 11028  ltexprlem3 11029  ltexprlem4 11030  ltexprlem5 11031  ltexprlem6 11032  ltexprlem7 11033
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11036  ltaprlem 11035
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11037
[Gleason] p. 124Lemma 9-3.6prlem936 11038
[Gleason] p. 124Proposition 9-3.7df-mp 10975  mulclpr 11011  mulclprlem 11010  reclem2pr 11039
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11020
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11015
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11014
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11019
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11042  reclem3pr 11040  reclem4pr 11041
[Gleason] p. 126Proposition 9-4.1df-enr 11046  enrer 11054
[Gleason] p. 126Proposition 9-4.2df-0r 11051  df-1r 11052  df-nr 11047
[Gleason] p. 126Proposition 9-4.3df-mr 11049  df-plr 11048  negexsr 11093  recexsr 11098  recexsrlem 11094
[Gleason] p. 127Proposition 9-4.4df-ltr 11050
[Gleason] p. 130Proposition 10-1.3creui 12219  creur 12218  cru 12216
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11179  axcnre 11155
[Gleason] p. 132Definition 10-3.1crim 15173  crimd 15290  crimi 15251  crre 15172  crred 15289  crrei 15250
[Gleason] p. 132Definition 10-3.2remim 15175  remimd 15256
[Gleason] p. 133Definition 10.36absval2 15342  absval2d 15506  absval2i 15456
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15199  cjaddd 15278  cjaddi 15246
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15200  cjmuld 15279  cjmuli 15247
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15198  cjcjd 15257  cjcji 15229
[Gleason] p. 133Proposition 10-3.4(f)cjre 15197  cjreb 15181  cjrebd 15260  cjrebi 15232  cjred 15284  rere 15180  rereb 15178  rerebd 15259  rerebi 15231  rered 15282
[Gleason] p. 133Proposition 10-3.4(h)addcj 15206  addcjd 15270  addcji 15241
[Gleason] p. 133Proposition 10-3.7(a)absval 15296
[Gleason] p. 133Proposition 10-3.7(b)abscj 15337  abscjd 15511  abscji 15460
[Gleason] p. 133Proposition 10-3.7(c)abs00 15347  abs00d 15507  abs00i 15457  absne0d 15508
[Gleason] p. 133Proposition 10-3.7(d)releabs 15380  releabsd 15512  releabsi 15461
[Gleason] p. 133Proposition 10-3.7(f)absmul 15352  absmuld 15515  absmuli 15463
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15340  sqabsaddi 15464
[Gleason] p. 133Proposition 10-3.7(h)abstri 15389  abstrid 15517  abstrii 15467
[Gleason] p. 134Definition 10-4.1df-exp 14105  exp0 14108  expp1 14111  expp1d 14190
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26855  cxpaddd 26893  expadd 14147  expaddd 14191  expaddz 14149
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26864  cxpmuld 26913  expmul 14150  expmuld 14192  expmulz 14151
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26861  mulcxpd 26904  mulexp 14144  mulexpd 14204  mulexpz 14145
[Gleason] p. 140Exercise 1znnen 16274
[Gleason] p. 141Definition 11-2.1fzval 13543
[Gleason] p. 168Proposition 12-2.1(a)climadd 15690  rlimadd 15701  rlimdiv 15704
[Gleason] p. 168Proposition 12-2.1(b)climsub 15692  rlimsub 15702
[Gleason] p. 168Proposition 12-2.1(c)climmul 15691  rlimmul 15703
[Gleason] p. 171Corollary 12-2.2climmulc2 15695
[Gleason] p. 172Corollary 12-2.5climrecl 15641
[Gleason] p. 172Proposition 12-2.4(c)climabs 15662  climcj 15663  climim 15665  climre 15664  rlimabs 15667  rlimcj 15668  rlimim 15670  rlimre 15669
[Gleason] p. 173Definition 12-3.1df-ltxr 11254  df-xr 11253  ltxr 13146
[Gleason] p. 175Definition 12-4.1df-limsup 15529  limsupval 15532
[Gleason] p. 180Theorem 12-5.1climsup 15728
[Gleason] p. 180Theorem 12-5.3caucvg 15737  caucvgb 15738  caucvgbf 46231  caucvgr 15734  climcau 15729
[Gleason] p. 182Exercise 3cvgcmp 15875
[Gleason] p. 182Exercise 4cvgrat 15944
[Gleason] p. 195Theorem 13-2.12abs1m 15394
[Gleason] p. 217Lemma 13-4.1btwnzge0 13868
[Gleason] p. 223Definition 14-1.1df-met 21527
[Gleason] p. 223Definition 14-1.1(a)met0 24511  xmet0 24510
[Gleason] p. 223Definition 14-1.1(b)metgt0 24527
[Gleason] p. 223Definition 14-1.1(c)metsym 24518
[Gleason] p. 223Definition 14-1.1(d)mettri 24520  mstri 24637  xmettri 24519  xmstri 24636
[Gleason] p. 225Definition 14-1.5xpsmet 24550
[Gleason] p. 230Proposition 14-2.6txlm 23816
[Gleason] p. 240Theorem 14-4.3metcnp4 25480
[Gleason] p. 240Proposition 14-4.2metcnp3 24708
[Gleason] p. 243Proposition 14-4.16addcn 25034  addcn2 15652  mulcn 25036  mulcn2 15654  subcn 25035  subcn2 15653
[Gleason] p. 295Remarkbcval3 14349  bcval4 14350
[Gleason] p. 295Equation 2bcpasc 14364
[Gleason] p. 295Definition of binomial coefficientbcval 14347  df-bc 14346
[Gleason] p. 296Remarkbcn0 14353  bcnn 14355
[Gleason] p. 296Theorem 15-2.8binom 15891
[Gleason] p. 308Equation 2ef0 16151
[Gleason] p. 308Equation 3efcj 16152
[Gleason] p. 309Corollary 15-4.3efne0 16158
[Gleason] p. 309Corollary 15-4.4efexp 16163
[Gleason] p. 310Equation 14sinadd 16226
[Gleason] p. 310Equation 15cosadd 16227
[Gleason] p. 311Equation 17sincossq 16238
[Gleason] p. 311Equation 18cosbnd 16243  sinbnd 16242
[Gleason] p. 311Lemma 15-4.7sqeqor 14259  sqeqori 14257
[Gleason] p. 311Definition of ` `df-pi 16132
[Godowski] p. 730Equation SFgoeqi 32636
[GodowskiGreechie] p. 249Equation IV3oai 32031
[Golan] p. 1Remarksrgisid 20297
[Golan] p. 1Definitiondf-srg 20275
[Golan] p. 149Definitiondf-slmd 33530
[Gonshor] p. 7Definitiondf-cuts 27964
[Gonshor] p. 9Theorem 2.5lesrec 28003  lesrecd 28004
[Gonshor] p. 10Theorem 2.6cofcut1 28124  cofcut1d 28125
[Gonshor] p. 10Theorem 2.7cofcut2 28126  cofcut2d 28127
[Gonshor] p. 12Theorem 2.9cofcutr 28128  cofcutr1d 28129  cofcutr2d 28130
[Gonshor] p. 13Definitiondf-adds 28164
[Gonshor] p. 14Theorem 3.1addsprop 28180
[Gonshor] p. 15Theorem 3.2addsunif 28206
[Gonshor] p. 17Theorem 3.4mulsprop 28334
[Gonshor] p. 18Theorem 3.5mulsunif 28354
[Gonshor] p. 28Lemma 4.2halfcut 28662
[Gonshor] p. 28Theorem 4.2pw2cut 28664
[Gonshor] p. 30Theorem 4.2addhalfcut 28663
[Gonshor] p. 39Theorem 4.4(b)elreno2 28699
[Gonshor] p. 95Theorem 6.1addbday 28222
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36659
[Gratzer] p. 23Section 0.6df-mre 17644
[Gratzer] p. 27Section 0.6df-mri 17646
[Hall] p. 1Section 1.1df-asslaw 48981  df-cllaw 48979  df-comlaw 48980
[Hall] p. 2Section 1.2df-clintop 48993
[Hall] p. 7Section 1.3df-sgrp2 49014
[Halmos] p. 28Partition ` `df-parts 39545  dfmembpart2 39550
[Halmos] p. 31Theorem 17.3riesz1 32428  riesz2 32429
[Halmos] p. 41Definition of Hermitianhmopadj2 32304
[Halmos] p. 42Definition of projector orderingpjordi 32536
[Halmos] p. 43Theorem 26.1elpjhmop 32548  elpjidm 32547  pjnmopi 32511
[Halmos] p. 44Remarkpjinormi 32050  pjinormii 32039
[Halmos] p. 44Theorem 26.2elpjch 32552  pjrn 32070  pjrni 32065  pjvec 32059
[Halmos] p. 44Theorem 26.3pjnorm2 32090
[Halmos] p. 44Theorem 26.4hmopidmpj 32517  hmopidmpji 32515
[Halmos] p. 45Theorem 27.1pjinvari 32554
[Halmos] p. 45Theorem 27.3pjoci 32543  pjocvec 32060
[Halmos] p. 45Theorem 27.4pjorthcoi 32532
[Halmos] p. 48Theorem 29.2pjssposi 32535
[Halmos] p. 48Theorem 29.3pjssdif1i 32538  pjssdif2i 32537
[Halmos] p. 50Definition of spectrumdf-spec 32218
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 24
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1824
[Hatcher] p. 25Definitiondf-phtpc 25162  df-phtpy 25141
[Hatcher] p. 26Definitiondf-pco 25175  df-pi1 25178
[Hatcher] p. 26Proposition 1.2phtpcer 25165
[Hatcher] p. 26Proposition 1.3pi1grp 25220
[Hefferon] p. 240Definition 3.12df-dmat 22658  df-dmatalt 49206
[Helfgott] p. 2Theoremtgoldbach 48610
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48595
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48607  bgoldbtbnd 48602  bgoldbtbnd 48602  tgblthelfgott 48608
[Helfgott] p. 5Proposition 1.1circlevma 35038
[Helfgott] p. 69Statement 7.49circlemethhgt 35039
[Helfgott] p. 69Statement 7.50hgt750lema 35053  hgt750lemb 35052  hgt750leme 35054  hgt750lemf 35049  hgt750lemg 35050
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48604  tgoldbachgt 35059  tgoldbachgtALTV 48605  tgoldbachgtd 35058
[Helfgott] p. 70Statement 7.49ax-hgt749 35040
[Herstein] p. 54Exercise 28df-grpo 30856
[Herstein] p. 55Lemma 2.2.1(a)grpideu 19017  grpoideu 30872  mndideu 18809
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19047  grpoinveu 30882
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19078  grpo2inv 30894
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19090  grpoinvop 30896
[Herstein] p. 57Exercise 1dfgrp3e 19112
[Hitchcock] p. 5Rule A3mptnan 1797
[Hitchcock] p. 5Rule A4mptxor 1798
[Hitchcock] p. 5Rule A5mtpxor 1800
[Holland] p. 1519Theorem 2sumdmdi 32783
[Holland] p. 1520Lemma 5cdj1i 32796  cdj3i 32804  cdj3lem1 32797  cdjreui 32795
[Holland] p. 1524Lemma 7mddmdin0i 32794
[Holland95] p. 13Theorem 3.6hlathil 42763
[Holland95] p. 14Line 15hgmapvs 42693
[Holland95] p. 14Line 16hdmaplkr 42715
[Holland95] p. 14Line 17hdmapellkr 42716
[Holland95] p. 14Line 19hdmapglnm2 42713
[Holland95] p. 14Line 20hdmapip0com 42719
[Holland95] p. 14Theorem 3.6hdmapevec2 42638
[Holland95] p. 14Lines 24 and 25hdmapoc 42733
[Holland95] p. 204Definition of involutiondf-srng 20954
[Holland95] p. 212Definition of subspacedf-psubsp 40305
[Holland95] p. 214Lemma 3.3lclkrlem2v 42330
[Holland95] p. 214Definition 3.2df-lpolN 42283
[Holland95] p. 214Definition of nonsingularpnonsingN 40735
[Holland95] p. 215Lemma 3.3(1)dihoml4 42179  poml4N 40755
[Holland95] p. 215Lemma 3.3(2)dochexmid 42270  pexmidALTN 40780  pexmidN 40771
[Holland95] p. 218Theorem 3.6lclkr 42335
[Holland95] p. 218Definition of dual vector spacedf-ldual 39926  ldualset 39927
[Holland95] p. 222Item 1df-lines 40303  df-pointsN 40304
[Holland95] p. 222Item 2df-polarityN 40705
[Holland95] p. 223Remarkispsubcl2N 40749  omllaw4 40048  pol1N 40712  polcon3N 40719
[Holland95] p. 223Definitiondf-psubclN 40737
[Holland95] p. 223Equation for polaritypolval2N 40708
[Holmes] p. 40Definitiondf-xrn 39057
[Hughes] p. 44Equation 1.21bax-his3 31447
[Hughes] p. 47Definition of projection operatordfpjop 32545
[Hughes] p. 49Equation 1.30eighmre 32326  eigre 32198  eigrei 32197
[Hughes] p. 49Equation 1.31eighmorth 32327  eigorth 32201  eigorthi 32200
[Hughes] p. 137Remark (ii)eigposi 32199
[Huneke] p. 1Claim 1frgrncvvdeq 30671
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30667
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30668
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30669
[Huneke] p. 2Claim 2frgrregorufr 30687  frgrregorufr0 30686  frgrregorufrg 30688
[Huneke] p. 2Claim 3frgrhash2wsp 30694  frrusgrord 30703  frrusgrord0 30702
[Huneke] p. 2Statementdf-clwwlknon 30450
[Huneke] p. 2Statement 4frgrwopreglem4 30677
[Huneke] p. 2Statement 5frgrwopreg1 30680  frgrwopreg2 30681  frgrwopregasn 30678  frgrwopregbsn 30679
[Huneke] p. 2Statement 6frgrwopreglem5 30683
[Huneke] p. 2Statement 7fusgreghash2wspv 30697
[Huneke] p. 2Statement 8fusgreghash2wsp 30700
[Huneke] p. 2Statement 9clwlksndivn 30448  numclwlk1 30733  numclwlk1lem1 30731  numclwlk1lem2 30732  numclwwlk1 30723  numclwwlk8 30754
[Huneke] p. 2Definition 3frgrwopreglem1 30674
[Huneke] p. 2Definition 4df-clwlks 30131
[Huneke] p. 2Definition 62clwwlk 30709
[Huneke] p. 2Definition 7numclwwlkovh 30735  numclwwlkovh0 30734
[Huneke] p. 2Statement 10numclwwlk2 30743
[Huneke] p. 2Statement 11rusgrnumwlkg 30340
[Huneke] p. 2Statement 12numclwwlk3 30747
[Huneke] p. 2Statement 13numclwwlk5 30750
[Huneke] p. 2Statement 14numclwwlk7 30753
[Indrzejczak] p. 33Definition ` `Enatded 30765  natded 30765
[Indrzejczak] p. 33Definition ` `Inatded 30765
[Indrzejczak] p. 34Definition ` `Enatded 30765  natded 30765
[Indrzejczak] p. 34Definition ` `Inatded 30765
[Jech] p. 4Definition of classcv 1568  cvjust 2756
[Jech] p. 42Lemma 6.1alephexp1 10570
[Jech] p. 42Equation 6.1alephadd 10568  alephmul 10569
[Jech] p. 43Lemma 6.2infmap 10567  infmap2 10207
[Jech] p. 71Lemma 9.3jech9.3 9784
[Jech] p. 72Equation 9.3df-scott 9856
[Jech] p. 72Exercise 9.1rankval4 9837  rankval4b 35502
[Jech] p. 72Scheme "Collection Principle"cp 9881
[Jech] p. 78Noteopthprc 5724
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43670
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43758
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43759
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43682
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43686
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43687  rmyp1 43688
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43689  rmym1 43690
[JonesMatijasevic] p. 695Equation 2.11rmx0 43680  rmx1 43681  rmxluc 43691
[JonesMatijasevic] p. 695Equation 2.12rmy0 43684  rmy1 43685  rmyluc 43692
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43694
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43695
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43715  jm2.17b 43716  jm2.17c 43717
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43748
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43752
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43743
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43718  jm2.24nn 43714
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43757
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43763  rmygeid 43719
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43775
[Juillerat] p. 11Section *5etransc 47025  etransclem47 47023  etransclem48 47024
[Juillerat] p. 12Equation (7)etransclem44 47020
[Juillerat] p. 12Equation *(7)etransclem46 47022
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 47008
[Juillerat] p. 13Proofetransclem35 47011
[Juillerat] p. 13Part of case 2 proven inetransclem38 47014
[Juillerat] p. 13Part of case 2 provenetransclem24 47000
[Juillerat] p. 13Part of case 2: proven inetransclem41 47017
[Juillerat] p. 14Proofetransclem23 46999
[KalishMontague] p. 81Note 1ax-6 1996
[KalishMontague] p. 85Lemma 2equid 2041
[KalishMontague] p. 85Lemma 3equcomi 2046
[KalishMontague] p. 86Lemma 7cbvalivw 2036  cbvaliw 2035  wl-cbvmotv 38196  wl-motae 38198  wl-moteq 38197
[KalishMontague] p. 87Lemma 8spimvw 2015  spimw 1999
[KalishMontague] p. 87Lemma 9spfw 2062  spw 2063
[Kalmbach] p. 14Definition of latticechabs1 31879  chabs1i 31881  chabs2 31880  chabs2i 31882  chjass 31896  chjassi 31849  latabs1 18537  latabs2 18538
[Kalmbach] p. 15Definition of atomdf-at 32701  ela 32702
[Kalmbach] p. 15Definition of coverscvbr2 32646  cvrval2 40076
[Kalmbach] p. 16Definitiondf-ol 39980  df-oml 39981
[Kalmbach] p. 20Definition of commutescmbr 31947  cmbri 31953  cmtvalN 40013  df-cm 31946  df-cmtN 39979
[Kalmbach] p. 22Remarkomllaw5N 40049  pjoml5 31976  pjoml5i 31951
[Kalmbach] p. 22Definitionpjoml2 31974  pjoml2i 31948
[Kalmbach] p. 22Theorem 2(v)cmcm 31977  cmcmi 31955  cmcmii 31960  cmtcomN 40051
[Kalmbach] p. 22Theorem 2(ii)omllaw3 40047  omlsi 31767  pjoml 31799  pjomli 31798
[Kalmbach] p. 22Definition of OML lawomllaw2N 40046
[Kalmbach] p. 23Remarkcmbr2i 31959  cmcm3 31978  cmcm3i 31957  cmcm3ii 31962  cmcm4i 31958  cmt3N 40053  cmt4N 40054  cmtbr2N 40055
[Kalmbach] p. 23Lemma 3cmbr3 31971  cmbr3i 31963  cmtbr3N 40056
[Kalmbach] p. 25Theorem 5fh1 31981  fh1i 31984  fh2 31982  fh2i 31985  omlfh1N 40060
[Kalmbach] p. 65Remarkchjatom 32720  chslej 31861  chsleji 31821  shslej 31743  shsleji 31733
[Kalmbach] p. 65Proposition 1chocin 31858  chocini 31817  chsupcl 31703  chsupval2 31773  h0elch 31618  helch 31606  hsupval2 31772  ocin 31659  ococss 31656  shococss 31657
[Kalmbach] p. 65Definition of subspace sumshsval 31675
[Kalmbach] p. 66Remarkdf-pjh 31758  pjssmi 32528  pjssmii 32044
[Kalmbach] p. 67Lemma 3osum 32008  osumi 32005
[Kalmbach] p. 67Lemma 4pjci 32563
[Kalmbach] p. 103Exercise 6atmd2 32763
[Kalmbach] p. 103Exercise 12mdsl0 32673
[Kalmbach] p. 140Remarkhatomic 32723  hatomici 32722  hatomistici 32725
[Kalmbach] p. 140Proposition 1atlatmstc 40121
[Kalmbach] p. 140Proposition 1(i)atexch 32744  lsatexch 39845
[Kalmbach] p. 140Proposition 1(ii)chcv1 32718  cvlcvr1 40141  cvr1 40212
[Kalmbach] p. 140Proposition 1(iii)cvexch 32737  cvexchi 32732  cvrexch 40222
[Kalmbach] p. 149Remark 2chrelati 32727  hlrelat 40204  hlrelat5N 40203  lrelat 39816
[Kalmbach] p. 153Exercise 5lsmcv 21276  lsmsatcv 39812  spansncv 32016  spansncvi 32015
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39831  spansncv2 32656
[Kalmbach] p. 266Definitiondf-st 32574
[Kalmbach2] p. 8Definition of adjointdf-adjh 32212
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10637  fpwwe2 10634
[KanamoriPincus] p. 416Corollary 1.3canth4 10638
[KanamoriPincus] p. 417Corollary 1.6canthp1 10645
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10640
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10642
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10655
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10659  gchxpidm 10660
[KanamoriPincus] p. 419Theorem 2.1gchacg 10671  gchhar 10670
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10205  unxpwdom 9549
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10661
[Kreyszig] p. 3Property M1metcl 24500  xmetcl 24499
[Kreyszig] p. 4Property M2meteq0 24507
[Kreyszig] p. 8Definition 1.1-8dscmet 24740
[Kreyszig] p. 12Equation 5conjmul 11938  muleqadd 11864
[Kreyszig] p. 18Definition 1.3-2mopnval 24606
[Kreyszig] p. 19Remarkmopntopon 24607
[Kreyszig] p. 19Theorem T1mopn0 24666  mopnm 24612
[Kreyszig] p. 19Theorem T2unimopn 24664
[Kreyszig] p. 19Definition of neighborhoodneibl 24669
[Kreyszig] p. 20Definition 1.3-3metcnp2 24710
[Kreyszig] p. 25Definition 1.4-1lmbr 23426  lmmbr 25428  lmmbr2 25429
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23548
[Kreyszig] p. 28Theorem 1.4-5lmcau 25483
[Kreyszig] p. 28Definition 1.4-3iscau 25446  iscmet2 25464
[Kreyszig] p. 30Theorem 1.4-7cmetss 25486
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23629  metelcls 25475
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25476  metcld2 25477
[Kreyszig] p. 51Equation 2clmvneg1 25269  lmodvneg1 21037  nvinv 31002  vcm 30939
[Kreyszig] p. 51Equation 1aclm0vs 25265  lmod0vs 21027  slmd0vs 33553  vc0 30937
[Kreyszig] p. 51Equation 1blmodvs0 21028  slmdvs0 33554  vcz 30938
[Kreyszig] p. 58Definition 2.2-1imsmet 31054  ngpmet 24771  nrmmetd 24742
[Kreyszig] p. 59Equation 1imsdval 31049  imsdval2 31050  ncvspds 25331  ngpds 24772
[Kreyszig] p. 63Problem 1nmval 24757  nvnd 31051
[Kreyszig] p. 64Problem 2nmeq0 24786  nmge0 24785  nvge0 31036  nvz 31032
[Kreyszig] p. 64Problem 3nmrtri 24792  nvabs 31035
[Kreyszig] p. 91Definition 2.7-1isblo3i 31164
[Kreyszig] p. 92Equation 2df-nmoo 31108
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 31170  blocni 31168
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 31169
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25374  ipeq0 21799  ipz 31082
[Kreyszig] p. 135Problem 2cphpyth 25386  pythi 31213
[Kreyszig] p. 137Lemma 3-2.1(a)sii 31217
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25408
[Kreyszig] p. 144Equation 4supcvg 15917
[Kreyszig] p. 144Theorem 3.3-1minvec 25606  minveco 31247
[Kreyszig] p. 196Definition 3.9-1df-aj 31113
[Kreyszig] p. 247Theorem 4.7-2bcth 25499
[Kreyszig] p. 249Theorem 4.7-3ubth 31236
[Kreyszig] p. 470Definition of positive operator orderingleop 32486  leopg 32485
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32504
[Kreyszig] p. 525Theorem 10.1-1htth 31281
[Kulpa] p. 547Theorempoimir 38332
[Kulpa] p. 547Equation (1)poimirlem32 38331
[Kulpa] p. 547Equation (2)poimirlem31 38330
[Kulpa] p. 548Theorembroucube 38333
[Kulpa] p. 548Equation (6)poimirlem26 38325
[Kulpa] p. 548Equation (7)poimirlem27 38326
[Kunen] p. 10Axiom 0ax6e 2414  axnul 5267
[Kunen] p. 11Axiom 3axnul 5267
[Kunen] p. 12Axiom 6zfrep6 5249
[Kunen] p. 24Definition 10.24mapval 8833  mapvalg 8831
[Kunen] p. 30Lemma 10.20fodomg 10512
[Kunen] p. 31Definition 10.24mapex 7935
[Kunen] p. 95Definition 2.1df-r1 9734
[Kunen] p. 97Lemma 2.10r1elss 9776  r1elssi 9775
[Kunen] p. 107Exercise 4rankop 9828  rankopb 9822  rankuni 9833  rankxplim 9849  rankxpsuc 9852
[Kunen2] p. 47Lemma I.9.9relpfr 45691
[Kunen2] p. 53Lemma I.9.21trfr 45699
[Kunen2] p. 53Lemma I.9.24(2)wffr 45698
[Kunen2] p. 53Definition I.9.20tcfr 45700
[Kunen2] p. 95Lemma I.16.2ralabso 45705  rexabso 45706
[Kunen2] p. 96Example I.16.3disjabso 45712  n0abso 45713  ssabso 45711
[Kunen2] p. 111Lemma II.2.4(1)traxext 45714
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45724
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45719
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45722
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45723
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45718
[Kunen2] p. 112Corollary II.2.5wfaxext 45730  wfaxpr 45735  wfaxreg 45737  wfaxrep 45731  wfaxsep 45732  wfaxun 45736
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45721
[Kunen2] p. 113Corollary II.2.9wfaxpow 45734
[Kunen2] p. 114Theorem II.2.13wfaxext 45730
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45729  omelaxinf2 45726
[Kunen2] p. 114Corollary II.2.12wfac8prim 45739  wfaxinf2 45738
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45752  permaxext 45742  permaxinf2 45750  permaxnul 45745  permaxpow 45746  permaxpr 45747  permaxrep 45743  permaxsep 45744  permaxun 45748
[Kunen2] p. 148Definition II.9.1brpermmodel 45740
[Kunen2] p. 149Exercise II.9.3permac8prim 45751
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4968
[Lang] , p. 225Corollary 1.3finexttrb 34064
[Lang] p. Definitiondf-rn 5671
[Lang] p. 3Statementlidrideqd 18733  mndbn0 18814
[Lang] p. 3Definitiondf-mnd 18799
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18751
[Lang] p. 4Property of composites. Second formulagsumccat 18906
[Lang] p. 5Equationgsumreidx 19993
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48975
[Lang] p. 6Examplenn0mnd 48972
[Lang] p. 6Equationgsumxp2 20056
[Lang] p. 6Statementcycsubm 19279
[Lang] p. 6Definitionmulgnn0gsum 19152
[Lang] p. 6Observationmndlsmidm 19746
[Lang] p. 7Definitiondfgrp2e 19036
[Lang] p. 30Definitiondf-tocyc 33436
[Lang] p. 32Property (a)cyc3genpm 33481
[Lang] p. 32Property (b)cyc3conja 33486  cycpmconjv 33471
[Lang] p. 53Definitiondf-cat 17730
[Lang] p. 53Axiom CAT 1cat1 18160  cat1lem 18159
[Lang] p. 54Definitiondf-iso 17812
[Lang] p. 57Definitiondf-inito 18047  df-termo 18048
[Lang] p. 58Exampleirinitoringc 21640
[Lang] p. 58Statementinitoeu1 18074  termoeu1 18081
[Lang] p. 62Definitiondf-func 17921
[Lang] p. 65Definitiondf-nat 18009
[Lang] p. 91Notedf-ringc 20756
[Lang] p. 92Statementmxidlprm 33762
[Lang] p. 92Definitionisprmidlc 21483
[Lang] p. 128Remarkdsmmlmod 21906
[Lang] p. 129Prooflincscm 49238  lincscmcl 49240  lincsum 49237  lincsumcl 49239
[Lang] p. 129Statementlincolss 49242
[Lang] p. 129Observationdsmmfi 21899
[Lang] p. 141Theorem 5.3dimkerim 34026  qusdimsum 34027
[Lang] p. 141Corollary 5.4lssdimle 34007
[Lang] p. 147Definitionsnlindsntor 49279
[Lang] p. 504Statementmat1 22615  matring 22611
[Lang] p. 504Definitiondf-mamu 22559
[Lang] p. 505Statementmamuass 22570  mamutpos 22626  matassa 22612  mattposvs 22623  tposmap 22625
[Lang] p. 513Definitionmdet1 22769  mdetf 22763
[Lang] p. 513Theorem 4.4cramer 22859
[Lang] p. 514Proposition 4.6mdetleib 22755
[Lang] p. 514Proposition 4.8mdettpos 22779
[Lang] p. 515Definitiondf-minmar1 22803  smadiadetr 22843
[Lang] p. 515Corollary 4.9mdetero 22778  mdetralt 22776
[Lang] p. 517Proposition 4.15mdetmul 22791
[Lang] p. 518Definitiondf-madu 22802
[Lang] p. 518Proposition 4.16madulid 22813  madurid 22812  matinv 22845
[Lang] p. 561Theorem 3.1cayleyhamilton 23058
[Lang], p. 190Chapter 6vieta 33979
[Lang], p. 224Proposition 1.1extdgfialg 34093  finextalg 34097
[Lang], p. 224Proposition 1.2extdgmul 34062  fedgmul 34030
[Lang], p. 225Proposition 1.4algextdeg 34124
[Lang], p. 561Remarkchpmatply1 23000
[Lang], p. 561Definitiondf-chpmat 22995
[Lang2] p. 3Notationsdf-ind 12225
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 45072
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 45067
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 45073
[LeBlanc] p. 277Rule R2axnul 5267
[Levy] p. 12Axiom 4.3.1df-clab 2741  wl-df.clab 38181
[Levy] p. 59Definitiondf-ttrcl 9675
[Levy] p. 64Theorem 5.6(ii)frinsg 9721
[Levy] p. 338Axiomdf-clel 2837  df-cleq 2754  wl-df.cleq 38182
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 38185
[Levy] p. 357Definition extends to class variables a relation already valid for set variables, and is therefore conservative. This only sketches the conservativity arguement; for details see Appendixwl-df.clel 38185
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2837  df-cleq 2754  wl-df.cleq 38182
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2741  wl-df.clab 38181
[Levy] p. 358Axiomdf-clab 2741  wl-df.clab 38181
[Levy58] p. 2Definition Iisfin1-3 10376
[Levy58] p. 2Definition IIdf-fin2 10276
[Levy58] p. 2Definition Iadf-fin1a 10275
[Levy58] p. 2Definition IIIdf-fin3 10278
[Levy58] p. 3Definition Vdf-fin5 10279
[Levy58] p. 3Definition IVdf-fin4 10277
[Levy58] p. 4Definition VIdf-fin6 10280
[Levy58] p. 4Definition VIIdf-fin7 10281
[Levy58], p. 3Theorem 1fin1a2 10405
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27861
[Lipparini] p. 3Lemma 2.1.4noresle 27872
[Lipparini] p. 6Proposition 4.2noinfbnd1 27904  nosupbnd1 27889
[Lipparini] p. 6Proposition 4.3noinfbnd2 27906  nosupbnd2 27891
[Lipparini] p. 7Theorem 5.1noetasuplem3 27910  noetasuplem4 27911
[Lipparini] p. 7Corollary 4.4nosupinfsep 27907
[Lopez-Astorga] p. 12Rule 1mptnan 1797
[Lopez-Astorga] p. 12Rule 2mptxor 1798
[Lopez-Astorga] p. 12Rule 3mtpxor 1800
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32771
[Maeda] p. 168Lemma 5mdsym 32775  mdsymi 32774
[Maeda] p. 168Lemma 4(i)mdsymlem4 32769  mdsymlem6 32771  mdsymlem7 32772
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32773
[MaedaMaeda] p. 1Remarkssdmd1 32676  ssdmd2 32677  ssmd1 32674  ssmd2 32675
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32672
[MaedaMaeda] p. 1Definition 1.1df-dmd 32644  df-md 32643  mdbr 32657
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32694  mdslj1i 32682  mdslj2i 32683  mdslle1i 32680  mdslle2i 32681  mdslmd1i 32692  mdslmd2i 32693
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32684  mdsl2bi 32686  mdsl2i 32685
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32698
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32695
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32696
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32673
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32678  mdsl3 32679
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32697
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32792
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 40123  hlrelat1 40202
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39841
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32699  cvmdi 32687  cvnbtwn4 32652  cvrnbtwn4 40081
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32700
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 40142  cvp 32738  cvrp 40218  lcvp 39842
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32762
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32761
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 40135  hlexch4N 40194
[MaedaMaeda] p. 34Exercise 7.1atabsi 32764
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40245
[MaedaMaeda] p. 61Definition 15.10psubN 40551  atpsubN 40555  df-pointsN 40304  pointpsubN 40553
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40306  pmap11 40564  pmaple 40563  pmapsub 40570  pmapval 40559
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40567  pmap1N 40569
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40572  pmapglb2N 40573  pmapglb2xN 40574  pmapglbx 40571
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40654
[MaedaMaeda] p. 67Postulate PS1ps-1 40279
[MaedaMaeda] p. 68Lemma 16.2df-padd 40598  paddclN 40644  paddidm 40643
[MaedaMaeda] p. 68Condition PS2ps-2 40280
[MaedaMaeda] p. 68Equation 16.2.1paddass 40640
[MaedaMaeda] p. 69Lemma 16.4ps-1 40279
[MaedaMaeda] p. 69Theorem 16.4ps-2 40280
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19751  lsmmod2 19752  lssats 39814  shatomici 32721  shatomistici 32724  shmodi 31753  shmodsi 31752
[MaedaMaeda] p. 130Remark 29.6dmdmd 32663  mdsymlem7 32772
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31952
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31856
[MaedaMaeda] p. 139Remarksumdmdii 32778
[Margaris] p. 40Rule Cexlimiv 1959
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 401  df-ex 1809  df-or 861  dfbi2 479
[Margaris] p. 51Theorem 1idALT 24
[Margaris] p. 56Theorem 3conventions 30762
[Margaris] p. 59Section 14notnotrALTVD 45651
[Margaris] p. 60Theorem 8jcn 163
[Margaris] p. 60Section 14con3ALTVD 45652
[Margaris] p. 79Rule Cexinst01 45362  exinst11 45363
[Margaris] p. 89Theorem 19.219.2 2005  19.2g 2223  r19.2z 4459
[Margaris] p. 89Theorem 19.319.3 2237  rr19.3v 3625
[Margaris] p. 89Theorem 19.5alcom 2193
[Margaris] p. 89Theorem 19.6alex 1855
[Margaris] p. 89Theorem 19.7alnex 1810
[Margaris] p. 89Theorem 19.819.8a 2216
[Margaris] p. 89Theorem 19.919.9 2240  19.9h 2320  exlimd 2253  exlimdh 2324
[Margaris] p. 89Theorem 19.11excom 2196  excomim 2197
[Margaris] p. 89Theorem 19.1219.12 2359
[Margaris] p. 90Section 19conventions-labels 30763  conventions-labels 30763  conventions-labels 30763  conventions-labels 30763
[Margaris] p. 90Theorem 19.14exnal 1856
[Margaris] p. 90Theorem 19.152albi 45116  albi 1847
[Margaris] p. 90Theorem 19.1619.16 2260
[Margaris] p. 90Theorem 19.1719.17 2261
[Margaris] p. 90Theorem 19.182exbi 45118  exbi 1876
[Margaris] p. 90Theorem 19.1919.19 2264
[Margaris] p. 90Theorem 19.202alim 45115  2alimdv 1947  alimd 2247  alimdh 1846  alimdv 1945  ax-4 1838  ralimdaa 3265  ralimdv 3178  ralimdva 3176  ralimdvva 3211  sbcimdv 3811
[Margaris] p. 90Theorem 19.2119.21 2242  19.21h 2321  19.21t 2241  19.21vv 45114  alrimd 2250  alrimdd 2249  alrimdh 1892  alrimdv 1958  alrimi 2248  alrimih 1853  alrimiv 1956  alrimivv 1957  bj-alrimdh 37245  hbralrimi 3154  r19.21be 3257  r19.21bi 3256  ralrimd 3269  ralrimdv 3162  ralrimdva 3164  ralrimdvv 3208  ralrimdvva 3219  ralrimi 3262  ralrimia 3263  ralrimiv 3155  ralrimiva 3156  ralrimivv 3205  ralrimivva 3207  ralrimivvva 3210  ralrimivw 3160
[Margaris] p. 90Theorem 19.222exim 45117  2eximdv 1948  bj-exim 37260  exim 1863  eximd 2251  eximdh 1893  eximdv 1946  rexim 3105  reximd2a 3274  reximdai 3266  reximdd 45894  reximddv 3180  reximddv2 3223  reximddv3 3181  reximdv 3179  reximdv2 3174  reximdva 3177  reximdvai 3175  reximdvva 3212  reximi2 3097
[Margaris] p. 90Theorem 19.2319.23 2246  19.23bi 2226  19.23h 2322  19.23t 2245  exlimdv 1962  exlimdvv 1963  exlimexi 45261  exlimiv 1959  exlimivv 1961  rexlimd3 45890  rexlimdv 3163  rexlimdv3a 3169  rexlimdva 3165  rexlimdva2 3167  rexlimdvaa 3166  rexlimdvv 3220  rexlimdvva 3221  rexlimdvvva 3222  rexlimdvw 3170  rexlimiv 3158  rexlimiva 3157  rexlimivv 3206
[Margaris] p. 90Theorem 19.2419.24 2020
[Margaris] p. 90Theorem 19.2519.25 1909
[Margaris] p. 90Theorem 19.2619.26 1899
[Margaris] p. 90Theorem 19.2719.27 2262  r19.27z 4470  r19.27zv 4471
[Margaris] p. 90Theorem 19.2819.28 2263  19.28vv 45124  r19.28z 4462  r19.28zf 45905  r19.28zv 4466  rr19.28v 3626
[Margaris] p. 90Theorem 19.2919.29 1902  r19.29d2r 3151  r19.29imd 3129
[Margaris] p. 90Theorem 19.3019.30 1910
[Margaris] p. 90Theorem 19.3119.31 2269  19.31vv 45122
[Margaris] p. 90Theorem 19.3219.32 2268  r19.32 47863
[Margaris] p. 90Theorem 19.3319.33-2 45120  19.33 1913
[Margaris] p. 90Theorem 19.3419.34 2021
[Margaris] p. 90Theorem 19.3519.35 1906
[Margaris] p. 90Theorem 19.3619.36 2265  19.36vv 45121  r19.36zv 4472
[Margaris] p. 90Theorem 19.3719.37 2267  19.37vv 45123  r19.37zv 4467
[Margaris] p. 90Theorem 19.3819.38 1868
[Margaris] p. 90Theorem 19.3919.39 2019
[Margaris] p. 90Theorem 19.4019.40-2 1916  19.40 1915  r19.40 3130
[Margaris] p. 90Theorem 19.4119.41 2270  19.41rg 45287
[Margaris] p. 90Theorem 19.4219.42 2271
[Margaris] p. 90Theorem 19.4319.43 1911
[Margaris] p. 90Theorem 19.4419.44 2272  r19.44zv 4469
[Margaris] p. 90Theorem 19.4519.45 2273  r19.45zv 4468
[Margaris] p. 110Exercise 2(b)eu1 2637
[Mayet] p. 370Remarkjpi 32633  largei 32630  stri 32620
[Mayet3] p. 9Definition of CH-statesdf-hst 32575  ishst 32577
[Mayet3] p. 10Theoremhstrbi 32629  hstri 32628
[Mayet3] p. 1223Theorem 4.1mayete3i 32091
[Mayet3] p. 1240Theorem 7.1mayetes3i 32092
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32641
[MegPav2000] p. 2345Definition 3.4-1chintcl 31695  chsupcl 31703
[MegPav2000] p. 2345Definition 3.4-2hatomic 32723
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32717
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32744
[MegPav2000] p. 2366Figure 7pl42N 40785
[MegPav2002] p. 362Lemma 2.2latj31 18549  latj32 18547  latjass 18545
[Megill] p. 444Axiom C5ax-5 1939  ax5ALT 39709
[Megill] p. 444Section 7conventions 30762
[Megill] p. 445Lemma L12aecom-o 39703  ax-c11n 39690  axc11n 2457
[Megill] p. 446Lemma L17equtrr 2051
[Megill] p. 446Lemma L18ax6fromc10 39698
[Megill] p. 446Lemma L19hbnae-o 39730  hbnae 2463
[Megill] p. 447Remark 9.1dfsb1 2512  sbid 2290  sbidd-misc 50525  sbidd 50524
[Megill] p. 448Remark 9.6axc14 2494
[Megill] p. 448Scheme C4'ax-c4 39686
[Megill] p. 448Scheme C5'ax-c5 39685  sp 2218
[Megill] p. 448Scheme C6'ax-11 2191
[Megill] p. 448Scheme C7'ax-c7 39687
[Megill] p. 448Scheme C8'ax-7 2037
[Megill] p. 448Scheme C9'ax-c9 39692
[Megill] p. 448Scheme C10'ax-6 1996  ax-c10 39688
[Megill] p. 448Scheme C11'ax-c11 39689
[Megill] p. 448Scheme C12'ax-8 2144
[Megill] p. 448Scheme C13'ax-9 2152
[Megill] p. 448Scheme C14'ax-c14 39693
[Megill] p. 448Scheme C15'ax-c15 39691
[Megill] p. 448Scheme C16'ax-c16 39694
[Megill] p. 448Theorem 9.4dral1-o 39706  dral1 2470  dral2-o 39732  dral2 2469  drex1 2472  drex2 2473  drsb1 2526  drsb2 2301
[Megill] p. 449Theorem 9.7sbcom2 2206  sbequ 2116  sbid2v 2540
[Megill] p. 450Example in Appendixhba1-o 39699  hba1 2327
[Mendelson] p. 35Axiom A3hirstL-ax3 47657
[Mendelson] p. 36Lemma 1.8idALT 24
[Mendelson] p. 69Axiom 4rspsbc 3831  rspsbca 3832  stdpc4 2101
[Mendelson] p. 69Axiom 5ax-c4 39686  ra4 3838  stdpc5 2243
[Mendelson] p. 81Rule Cexlimiv 1959
[Mendelson] p. 95Axiom 6stdpc6 2057
[Mendelson] p. 95Axiom 7stdpc7 2285
[Mendelson] p. 225Axiom system NBGru 3742
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5496
[Mendelson] p. 231Exercise 4.10(k)inv1 4354
[Mendelson] p. 231Exercise 4.10(l)unv 4355
[Mendelson] p. 231Exercise 4.10(n)dfin3 4229
[Mendelson] p. 231Exercise 4.10(o)df-nul 4286
[Mendelson] p. 231Exercise 4.10(q)dfin4 4230
[Mendelson] p. 231Exercise 4.10(s)ddif 4094
[Mendelson] p. 231Definition of uniondfun3 4228
[Mendelson] p. 235Exercise 4.12(c)univ 5431
[Mendelson] p. 235Exercise 4.12(d)pwv 4868
[Mendelson] p. 235Exercise 4.12(j)pwin 5551
[Mendelson] p. 235Exercise 4.12(k)pwunss 4579
[Mendelson] p. 235Exercise 4.12(l)pwssun 5552
[Mendelson] p. 235Exercise 4.12(n)uniin 4895
[Mendelson] p. 235Exercise 4.12(p)reli 5812
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6270
[Mendelson] p. 244Proposition 4.8(g)epweon 7772
[Mendelson] p. 246Definition of successordf-suc 6366
[Mendelson] p. 250Exercise 4.36oelim2 8579
[Mendelson] p. 254Proposition 4.22(b)xpen 9126
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9047  xpsneng 9048
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9054  xpcomeng 9055
[Mendelson] p. 254Proposition 4.22(e)xpassen 9057
[Mendelson] p. 255Definitionbrsdom 8969
[Mendelson] p. 255Exercise 4.39endisj 9050
[Mendelson] p. 255Exercise 4.41mapprc 8826
[Mendelson] p. 255Exercise 4.43mapsnen 9032  mapsnend 9031
[Mendelson] p. 255Exercise 4.45mapunen 9132
[Mendelson] p. 255Exercise 4.47xpmapen 9131
[Mendelson] p. 255Exercise 4.42(a)map0e 8878
[Mendelson] p. 255Exercise 4.42(b)map1 9035
[Mendelson] p. 257Proposition 4.24(a)undom 9051
[Mendelson] p. 258Exercise 4.56(c)djuassen 10169  djucomen 10168
[Mendelson] p. 258Exercise 4.56(f)djudom1 10173
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10167
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8514
[Mendelson] p. 266Proposition 4.34(f)oaordex 8541
[Mendelson] p. 275Proposition 4.42(d)entri3 10549
[Mendelson] p. 281Definitiondf-r1 9734
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9783
[Mendelson] p. 287Axiom system MKru 3742
[MertziosUnger] p. 152Definitiondf-frgr 30621
[MertziosUnger] p. 153Remark 1frgrconngr 30656
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30658  vdgn1frgrv3 30659
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30660
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30653
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30646  2pthfrgrrn 30644  2pthfrgrrn2 30645
[Mittelstaedt] p. 9Definitiondf-oc 31615
[Monk1] p. 22Remarkconventions 30762
[Monk1] p. 22Theorem 3.1conventions 30762
[Monk1] p. 26Theorem 2.8(vii)ssin 4190
[Monk1] p. 33Theorem 3.2(i)ssrel 5768  ssrelf 32971
[Monk1] p. 33Theorem 3.2(ii)eqrel 5769
[Monk1] p. 34Definition 3.3df-opab 5173
[Monk1] p. 36Theorem 3.7(i)coi1 6263  coi2 6264
[Monk1] p. 36Theorem 3.8(v)dm0 5909  rn0 5915
[Monk1] p. 36Theorem 3.7(ii)cnvi 5870
[Monk1] p. 37Theorem 3.13(i)relxp 5678
[Monk1] p. 37Theorem 3.13(x)dmxp 5918  rnxp 6167
[Monk1] p. 37Theorem 3.13(ii)0xp 5759  xp0 5760
[Monk1] p. 38Theorem 3.16(ii)ima0 6078
[Monk1] p. 38Theorem 3.16(viii)imai 6075
[Monk1] p. 39Theorem 3.17imaex 7909  imaexg 7908
[Monk1] p. 39Theorem 3.16(xi)imassrn 6072
[Monk1] p. 41Theorem 4.3(i)fnopfv 7070  funfvop 7045
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6935
[Monk1] p. 42Theorem 4.4(iii)fvelima 6946
[Monk1] p. 43Theorem 4.6funun 6582
[Monk1] p. 43Theorem 4.8(iv)dff13 7252  dff13f 7253
[Monk1] p. 46Theorem 4.15(v)funex 7217  funrnex 7949
[Monk1] p. 50Definition 5.4fniunfv 7245
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6227
[Monk1] p. 52Theorem 5.11(viii)ssint 4928
[Monk1] p. 52Definition 5.13 (i)1stval2 8001  df-1st 7984
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8002  df-2nd 7985
[Monk1] p. 112Theorem 15.17(v)ranksn 9824  ranksnb 9797
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9825
[Monk1] p. 112Theorem 15.17(iii)rankun 9826  rankunb 9820
[Monk1] p. 113Theorem 15.18r1val3 9808
[Monk1] p. 113Definition 15.19df-r1 9734  r1val2 9807
[Monk1] p. 117Lemmazorn2 10496  zorn2g 10493
[Monk1] p. 133Theorem 18.11cardom 9979
[Monk1] p. 133Theorem 18.12canth3 10551
[Monk1] p. 133Theorem 18.14carduni 9974
[Monk2] p. 105Axiom C4ax-4 1838
[Monk2] p. 105Axiom C7ax-7 2037
[Monk2] p. 105Axiom C8ax-12 2212  ax-c15 39691  ax12v2 2214
[Monk2] p. 108Lemma 5ax-c4 39686
[Monk2] p. 109Lemma 12ax-11 2191
[Monk2] p. 109Lemma 15equvini 2486  equvinv 2058  eqvinop 5468
[Monk2] p. 113Axiom C5-1ax-5 1939  ax5ALT 39709
[Monk2] p. 113Axiom C5-2ax-10 2175
[Monk2] p. 113Axiom C5-3ax-11 2191
[Monk2] p. 114Lemma 21sp 2218
[Monk2] p. 114Lemma 22axc4 2353  hba1-o 39699  hba1 2327
[Monk2] p. 114Lemma 23nfia1 2187
[Monk2] p. 114Lemma 24nfa2 2209  nfra2 3364  nfra2w 3300
[Moore] p. 53Part Idf-mre 17644
[Munkres] p. 77Example 2distop 23163  indistop 23170  indistopon 23169
[Munkres] p. 77Example 3fctop 23172  fctop2 23173
[Munkres] p. 77Example 4cctop 23174
[Munkres] p. 78Definition of basisdf-bases 23114  isbasis3g 23117
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17502  tgval2 23124
[Munkres] p. 79Remarktgcl 23137
[Munkres] p. 80Lemma 2.1tgval3 23131
[Munkres] p. 80Lemma 2.2tgss2 23155  tgss3 23154
[Munkres] p. 81Lemma 2.3basgen 23156  basgen2 23157
[Munkres] p. 83Exercise 3topdifinf 38023  topdifinfeq 38024  topdifinffin 38022  topdifinfindis 38020
[Munkres] p. 89Definition of subspace topologyresttop 23328
[Munkres] p. 93Theorem 6.1(1)0cld 23206  topcld 23203
[Munkres] p. 93Theorem 6.1(2)iincld 23207
[Munkres] p. 93Theorem 6.1(3)uncld 23209
[Munkres] p. 94Definition of closureclsval 23205
[Munkres] p. 94Definition of interiorntrval 23204
[Munkres] p. 95Theorem 6.5(a)clsndisj 23243  elcls 23241
[Munkres] p. 95Theorem 6.5(b)elcls3 23251
[Munkres] p. 97Theorem 6.6clslp 23316  neindisj 23285
[Munkres] p. 97Corollary 6.7cldlp 23318
[Munkres] p. 97Definition of limit pointislp2 23313  lpval 23307
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23483
[Munkres] p. 102Definition of continuous functiondf-cn 23395  iscn 23403  iscn2 23406
[Munkres] p. 107Theorem 7.2(g)cncnp 23448  cncnp2 23449  cncnpi 23446  df-cnp 23396  iscnp 23405  iscnp2 23407
[Munkres] p. 127Theorem 10.1metcn 24711
[Munkres] p. 128Theorem 10.3metcn4 25481
[Nathanson] p. 123Remarkreprgt 35017  reprinfz1 35018  reprlt 35015
[Nathanson] p. 123Definitiondf-repr 35005
[Nathanson] p. 123Chapter 5.1circlemethnat 35037
[Nathanson] p. 123Propositionbreprexp 35029  breprexpnat 35030  itgexpif 35002
[NielsenChuang] p. 195Equation 4.73unierri 32467
[OeSilva] p. 2042Section 2ax-bgbltosilva 48603
[Pfenning] p. 17Definition XMnatded 30765
[Pfenning] p. 17Definition NNCnatded 30765  notnotrd 134
[Pfenning] p. 17Definition ` `Cnatded 30765
[Pfenning] p. 18Rule"natded 30765
[Pfenning] p. 18Definition /\Inatded 30765
[Pfenning] p. 18Definition ` `Enatded 30765  natded 30765  natded 30765  natded 30765  natded 30765
[Pfenning] p. 18Definition ` `Inatded 30765  natded 30765  natded 30765  natded 30765  natded 30765
[Pfenning] p. 18Definition ` `ELnatded 30765
[Pfenning] p. 18Definition ` `ERnatded 30765
[Pfenning] p. 18Definition ` `Ea,unatded 30765
[Pfenning] p. 18Definition ` `IRnatded 30765
[Pfenning] p. 18Definition ` `Ianatded 30765
[Pfenning] p. 127Definition =Enatded 30765
[Pfenning] p. 127Definition =Inatded 30765
[Ponnusamy] p. 361Theorem 6.44cphip0l 25372  df-dip 31064  dip0l 31081  ip0l 21797
[Ponnusamy] p. 361Equation 6.45cphipval 25413  ipval 31066
[Ponnusamy] p. 362Equation I1dipcj 31077  ipcj 21795
[Ponnusamy] p. 362Equation I3cphdir 25375  dipdir 31205  ipdir 21800  ipdiri 31193
[Ponnusamy] p. 362Equation I4ipidsq 31073  nmsq 25364
[Ponnusamy] p. 362Equation 6.46ip0i 31188
[Ponnusamy] p. 362Equation 6.47ip1i 31190
[Ponnusamy] p. 362Equation 6.48ip2i 31191
[Ponnusamy] p. 363Equation I2cphass 25381  dipass 31208  ipass 21806  ipassi 31204
[Prugovecki] p. 186Definition of brabraval 32307  df-bra 32213
[Prugovecki] p. 376Equation 8.1df-kb 32214  kbval 32317
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32745
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40690
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32759  atcvat4i 32760  cvrat3 40244  cvrat4 40245  lsatcvat3 39854
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32645  cvrval 40071  df-cv 32642  df-lcv 39821  lspsncv0 21281
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40702
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40703
[Quine] p. 16Definition 2.1df-clab 2741  rabid 3436  rabidd 45901  wl-df.clab 38181
[Quine] p. 17Definition 2.1''dfsb7 2313
[Quine] p. 18Definition 2.7df-cleq 2754  wl-df.cleq 38182
[Quine] p. 19Definition 2.9conventions 30762  df-v 3456
[Quine] p. 34Theorem 5.1eqabb 2901
[Quine] p. 35Theorem 5.2abid1 2898  abid2f 2954
[Quine] p. 40Theorem 6.1sb5 2310
[Quine] p. 40Theorem 6.2sb6 2118  sbalex 2277
[Quine] p. 41Theorem 6.3df-clel 2837  wl-df.clel 38185
[Quine] p. 41Theorem 6.4eqid 2762  eqid1 30829
[Quine] p. 41Theorem 6.5eqcom 2769
[Quine] p. 42Theorem 6.6df-sbc 3744
[Quine] p. 42Theorem 6.7dfsbcq 3745  dfsbcq2 3746
[Quine] p. 43Theorem 6.8vex 3458
[Quine] p. 43Theorem 6.9isset 3468
[Quine] p. 44Theorem 7.3spcgf 3549  spcgv 3554  spcimgf 3517
[Quine] p. 44Theorem 6.11spsbc 3756  spsbcd 3757
[Quine] p. 44Theorem 6.12elex 3475
[Quine] p. 44Theorem 6.13elab 3637  elabg 3634  elabgf 3632
[Quine] p. 44Theorem 6.14noel 4290
[Quine] p. 48Theorem 7.2snprc 4682
[Quine] p. 48Definition 7.1df-pr 4591  df-sn 4589
[Quine] p. 49Theorem 7.4snss 4749  snssg 4748
[Quine] p. 49Theorem 7.5prss 4785  prssg 4784
[Quine] p. 49Theorem 7.6prid1 4727  prid1g 4725  prid2 4728  prid2g 4726  snid 4627  snidg 4625
[Quine] p. 51Theorem 7.12snex 5409
[Quine] p. 51Theorem 7.13prex 5408
[Quine] p. 53Theorem 8.2unisn 4890  unisnALT 45662  unisng 4889
[Quine] p. 53Theorem 8.3uniun 4894
[Quine] p. 54Theorem 8.6elssuni 4903
[Quine] p. 54Theorem 8.7uni0 4900
[Quine] p. 56Theorem 8.17uniabio 6506
[Quine] p. 56Definition 8.18dfaiota2 47851  dfiota2 6493
[Quine] p. 57Theorem 8.19aiotaval 47860  iotaval 6510
[Quine] p. 57Theorem 8.22iotanul 6516
[Quine] p. 58Theorem 8.23iotaex 6512
[Quine] p. 58Definition 9.1df-op 4595
[Quine] p. 61Theorem 9.5opabid 5508  opabidw 5507  opelopab 5526  opelopaba 5519  opelopabaf 5528  opelopabf 5529  opelopabg 5522  opelopabga 5516  opelopabgf 5524  oprabid 7444  oprabidw 7443
[Quine] p. 64Definition 9.11df-xp 5666
[Quine] p. 64Definition 9.12df-cnv 5668
[Quine] p. 64Definition 9.15df-id 5555
[Quine] p. 65Theorem 10.3fun0 6601
[Quine] p. 65Theorem 10.4funi 6568
[Quine] p. 65Theorem 10.5funsn 6589  funsng 6587
[Quine] p. 65Definition 10.1df-fun 6538
[Quine] p. 65Definition 10.2args 6093  dffv4 6878
[Quine] p. 68Definition 10.11conventions 30762  df-fv 6544  fv2 6876
[Quine] p. 124Theorem 17.3nn0opth2 14315  nn0opth2i 14314  nn0opthi 14313  omopthi 8645
[Quine] p. 177Definition 25.2df-rdg 8395
[Quine] p. 232Equation icarddom 10544
[Quine] p. 284Axiom 39(vi)funimaex 6623  funimaexg 6622
[Quine] p. 331Axiom system NFru 3742
[ReedSimon] p. 36Definition (iii)ax-his3 31447
[ReedSimon] p. 63Exercise 4(a)df-dip 31064  polid 31522  polid2i 31520  polidi 31521
[ReedSimon] p. 63Exercise 4(b)df-ph 31176
[ReedSimon] p. 195Remarklnophm 32382  lnophmi 32381
[Retherford] p. 49Exercise 1(i)leopadd 32495
[Retherford] p. 49Exercise 1(ii)leopmul 32497  leopmuli 32496
[Retherford] p. 49Exercise 1(iv)leoptr 32500
[Retherford] p. 49Definition VI.1df-leop 32215  leoppos 32489
[Retherford] p. 49Exercise 1(iii)leoptri 32499
[Retherford] p. 49Definition of operator orderingleop3 32488
[Ribenboim] p. 181Remarknprmdvdsfacm1 48404
[Ribenboim], p. 181Statementppivalnn 48412
[Roman] p. 4Definitiondf-dmat 22658  df-dmatalt 49206
[Roman] p. 18Part Preliminariesdf-rng 20237
[Roman] p. 19Part Preliminariesdf-ring 20323
[Roman] p. 46Theorem 1.6isldepslvec2 49293
[Roman] p. 112Noteisldepslvec2 49293  ldepsnlinc 49316  zlmodzxznm 49305
[Roman] p. 112Examplezlmodzxzequa 49304  zlmodzxzequap 49307  zlmodzxzldep 49312
[Roman] p. 170Theorem 7.8cayleyhamilton 23058
[Rosenlicht] p. 80Theoremheicant 38334
[Rosser] p. 281Definitiondf-op 4595
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 35041
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 35042
[Rotman] p. 28Remarkpgrpgt2nabl 49174  pmtr3ncom 19551
[Rotman] p. 31Theorem 3.4symggen2 19547
[Rotman] p. 42Theorem 3.15cayley 19490  cayleyth 19491
[Rudin] p. 164Equation 27efcan 16156
[Rudin] p. 164Equation 30efzval 16164
[Rudin] p. 167Equation 48absefi 16258
[Russell1905] p. 482Example of "the fatherdfalseu2 50642
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1800
[Sanford] p. 39Rule 4mptxor 1798
[Sanford] p. 40Rule 1mptnan 1797
[Schechter] p. 51Definition of antisymmetryintasym 6114
[Schechter] p. 51Definition of irreflexivityintirr 6117
[Schechter] p. 51Definition of symmetrycnvsym 6113
[Schechter] p. 51Definition of transitivitycotr 6111
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17644
[Schechter] p. 79Definition of Moore closuredf-mrc 17645
[Schechter] p. 82Section 4.5df-mrc 17645
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17647
[Schechter] p. 139Definition AC3dfac9 10127
[Schechter] p. 141Definition (MC)dfac11 43817
[Schechter] p. 149Axiom DC1ax-dc 10436  axdc3 10444
[Schechter] p. 187Definition of "ring with unit"isring 20325  isrngo 38576
[Schechter] p. 276Remark 11.6.espan0 31905
[Schechter] p. 276Definition of spandf-span 31672  spanval 31696
[Schechter] p. 428Definition 15.35bastop1 23161
[Schloeder] p. 1Lemma 1.3onelon 6385  onelond 36699  onelord 44006  ordelon 6384  ordelord 6382
[Schloeder] p. 1Lemma 1.7onepsuc 44007  sucidg 6444
[Schloeder] p. 1Remark 1.50elon 6416  onsuc 7807  ord0 6415  ordsuci 7805
[Schloeder] p. 1Theorem 1.9epsoon 44008
[Schloeder] p. 1Definition 1.1dftr5 5221
[Schloeder] p. 1Definition 1.2dford3 43783  elon2 6371
[Schloeder] p. 1Definition 1.4df-suc 6366
[Schloeder] p. 1Definition 1.6epel 5563  epelg 5561
[Schloeder] p. 1Theorem 1.9(i)elirr 9560  epirron 44009  ordirr 6378
[Schloeder] p. 1Theorem 1.9(ii)oneltr 44011  oneptr 44010  ontr1 6408
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6404  oneptri 44012  ordtri3or 6393
[Schloeder] p. 2Lemma 1.10ondif1 8484  ord0eln0 6417
[Schloeder] p. 2Lemma 1.13elsuci 6430  onsucss 44021  trsucss 6451
[Schloeder] p. 2Lemma 1.14ordsucss 7812
[Schloeder] p. 2Lemma 1.15onnbtwn 6457  ordnbtwn 6456
[Schloeder] p. 2Lemma 1.16orddif0suc 44023  ordnexbtwnsuc 44022
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10391  onsucf1lem 44024  onsucf1o 44027  onsucf1olem 44025  onsucrn 44026
[Schloeder] p. 2Lemma 1.18dflim7 44028
[Schloeder] p. 2Remark 1.12ordzsl 7839
[Schloeder] p. 2Theorem 1.10ondif1i 44017  ordne0gt0 44016
[Schloeder] p. 2Definition 1.11dflim6 44019  limnsuc 44020  onsucelab 44018
[Schloeder] p. 3Remark 1.21omex 9610
[Schloeder] p. 3Theorem 1.19tfinds 7854
[Schloeder] p. 3Theorem 1.22omelon 9613  ordom 7870
[Schloeder] p. 3Definition 1.20dfom3 9614
[Schloeder] p. 4Lemma 2.21onn 8624
[Schloeder] p. 4Lemma 2.7ssonuni 7777  ssorduni 7776
[Schloeder] p. 4Remark 2.4oa1suc 8514
[Schloeder] p. 4Theorem 1.23dfom5 9617  limom 7876
[Schloeder] p. 4Definition 2.1df-1o 8451  df1o2 8458
[Schloeder] p. 4Definition 2.3oa0 8499  oa0suclim 44030  oalim 8515  oasuc 8507
[Schloeder] p. 4Definition 2.5om0 8500  om0suclim 44031  omlim 8516  omsuc 8509
[Schloeder] p. 4Definition 2.6oe0 8505  oe0m1 8504  oe0suclim 44032  oelim 8517  oesuc 8510
[Schloeder] p. 5Lemma 2.10onsupuni 43984
[Schloeder] p. 5Lemma 2.11onsupsucismax 44034
[Schloeder] p. 5Lemma 2.12onsssupeqcond 44035
[Schloeder] p. 5Lemma 2.13limexissup 44036  limexissupab 44038  limiun 44037  limuni 6423
[Schloeder] p. 5Lemma 2.14oa0r 8521
[Schloeder] p. 5Lemma 2.15om1 8525  om1om1r 44039  om1r 8526
[Schloeder] p. 5Remark 2.8oacl 8518  oaomoecl 44033  oecl 8520  omcl 8519
[Schloeder] p. 5Definition 2.9onsupintrab 43986
[Schloeder] p. 6Lemma 2.16oe1 8527
[Schloeder] p. 6Lemma 2.17oe1m 8528
[Schloeder] p. 6Lemma 2.18oe0rif 44040
[Schloeder] p. 6Theorem 2.19oasubex 44041
[Schloeder] p. 6Theorem 2.20nnacl 8595  nnamecl 44042  nnecl 8597  nnmcl 8596
[Schloeder] p. 7Lemma 3.1onsucwordi 44043
[Schloeder] p. 7Lemma 3.2oaword1 8535
[Schloeder] p. 7Lemma 3.3oaword2 8536
[Schloeder] p. 7Lemma 3.4oalimcl 8543
[Schloeder] p. 7Lemma 3.5oaltublim 44045
[Schloeder] p. 8Lemma 3.6oaordi3 44046
[Schloeder] p. 8Lemma 3.81oaomeqom 44048
[Schloeder] p. 8Lemma 3.10oa00 8542
[Schloeder] p. 8Lemma 3.11omge1 44052  omword1 8556
[Schloeder] p. 8Remark 3.9oaordnr 44051  oaordnrex 44050
[Schloeder] p. 8Theorem 3.7oaord3 44047
[Schloeder] p. 9Lemma 3.12omge2 44053  omword2 8557
[Schloeder] p. 9Lemma 3.13omlim2 44054
[Schloeder] p. 9Lemma 3.14omord2lim 44055
[Schloeder] p. 9Lemma 3.15omord2i 44056  omordi 8549
[Schloeder] p. 9Theorem 3.16omord 8551  omord2com 44057
[Schloeder] p. 10Lemma 3.172omomeqom 44058  df-2o 8452
[Schloeder] p. 10Lemma 3.19oege1 44061  oewordi 8575
[Schloeder] p. 10Lemma 3.20oege2 44062  oeworde 8577
[Schloeder] p. 10Lemma 3.21rp-oelim2 44063
[Schloeder] p. 10Lemma 3.22oeord2lim 44064
[Schloeder] p. 10Remark 3.18omnord1 44060  omnord1ex 44059
[Schloeder] p. 11Lemma 3.23oeord2i 44065
[Schloeder] p. 11Lemma 3.25nnoeomeqom 44067
[Schloeder] p. 11Remark 3.26oenord1 44071  oenord1ex 44070
[Schloeder] p. 11Theorem 4.1oaomoencom 44072
[Schloeder] p. 11Theorem 4.2oaass 8544
[Schloeder] p. 11Theorem 3.24oeord2com 44066
[Schloeder] p. 12Theorem 4.3odi 8562
[Schloeder] p. 13Theorem 4.4omass 8563
[Schloeder] p. 14Remark 4.6oenass 44074
[Schloeder] p. 14Theorem 4.7oeoa 8581
[Schloeder] p. 15Lemma 5.1cantnftermord 44075
[Schloeder] p. 15Lemma 5.2cantnfub 44076  cantnfub2 44077
[Schloeder] p. 16Theorem 5.3cantnf2 44080
[Schwabhauser] p. 10Axiom A1axcgrrflx 29275  axtgcgrrflx 28742
[Schwabhauser] p. 10Axiom A2axcgrtr 29276
[Schwabhauser] p. 10Axiom A3axcgrid 29277  axtgcgrid 28743
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28728
[Schwabhauser] p. 11Axiom A4axsegcon 29288  axtgsegcon 28744  df-trkgcb 28730
[Schwabhauser] p. 11Axiom A5ax5seg 29299  axtg5seg 28745  df-trkgcb 28730
[Schwabhauser] p. 11Axiom A6axbtwnid 29300  axtgbtwnid 28746  df-trkgb 28729
[Schwabhauser] p. 12Axiom A7axpasch 29302  axtgpasch 28747  df-trkgb 28729
[Schwabhauser] p. 12Axiom A8axlowdim2 29321  df-trkg2d 35061
[Schwabhauser] p. 13Axiom A8axtglowdim2 28750
[Schwabhauser] p. 13Axiom A9axtgupdim2 28751  df-trkg2d 35061
[Schwabhauser] p. 13Axiom A10axeuclid 29324  axtgeucl 28752  df-trkge 28731
[Schwabhauser] p. 13Axiom A11axcont 29337  axtgcont 28749  axtgcont1 28748  df-trkgb 28729
[Schwabhauser] p. 24Theorem A10prlngmo 29215
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36487
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36489
[Schwabhauser] p. 27Theorem 2.3cgrtr 36492
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36496
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36497  tgcgrcomimp 28757  tgcgrcoml 28759  tgcgrcomr 28758
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36502  tgcgrtriv 28764
[Schwabhauser] p. 28Theorem 2.105segofs 36506  tg5segofs 35072
[Schwabhauser] p. 28Definition 2.10df-afs 35069  df-ofs 36483
[Schwabhauser] p. 29Theorem 2.11cgrextend 36508  tgcgrextend 28765
[Schwabhauser] p. 29Theorem 2.12segconeq 36510  tgsegconeq 28766
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36522  btwntriv2 36512  tgbtwntriv2 28767
[Schwabhauser] p. 30Theorem 3.2btwncomim 36513  tgbtwncom 28768
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36516  tgbtwntriv1 28771
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36517  tgbtwnswapid 28772
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36523  btwnintr 36519  tgbtwnexch2 28776  tgbtwnintr 28773
[Schwabhauser] p. 30Theorem 3.6btwnexch 36525  btwnexch3 36520  tgbtwnexch 28778  tgbtwnexch3 28774
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36524  tgbtwnouttr 28777  tgbtwnouttr2 28775
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29320
[Schwabhauser] p. 32Theorem 3.14btwndiff 36527  tgbtwndiff 28786
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28779  trisegint 36528
[Schwabhauser] p. 34Theorem 4.2ifscgr 36544  tgifscgr 28788
[Schwabhauser] p. 34Theorem 4.11colcom 28838  colrot1 28839  colrot2 28840  lncom 28906  lnrot1 28907  lnrot2 28908
[Schwabhauser] p. 34Definition 4.1df-ifs 36540
[Schwabhauser] p. 35Theorem 4.3cgrsub 36545  tgcgrsub 28789
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36555  tgcgrxfr 28798
[Schwabhauser] p. 35Statement 4.4ercgrg 28797
[Schwabhauser] p. 35Definition 4.4df-cgr3 36541  df-cgrg 28791
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28791
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36556  tgbtwnxfr 28810
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36562  colinearperm2 36564  colinearperm3 36563  colinearperm4 36565  colinearperm5 36566
[Schwabhauser] p. 36Definition 4.8df-ismt 28813
[Schwabhauser] p. 36Definition 4.10df-colinear 36539  tgellng 28833  tglng 28826
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36567
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36575  lnxfr 28846
[Schwabhauser] p. 37Theorem 4.14lineext 36576  lnext 28847
[Schwabhauser] p. 37Theorem 4.16fscgr 36580  tgfscgr 28848
[Schwabhauser] p. 37Theorem 4.17linecgr 36581  lncgr 28849
[Schwabhauser] p. 37Definition 4.15df-fs 36542
[Schwabhauser] p. 38Theorem 4.18lineid 36583  lnid 28850
[Schwabhauser] p. 38Theorem 4.19idinside 36584  tgidinside 28851
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36601  tgbtwnconn1 28855
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36602  tgbtwnconn2 28856
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36603  tgbtwnconn3 28857
[Schwabhauser] p. 41Theorem 5.5brsegle2 36609
[Schwabhauser] p. 41Definition 5.4df-segle 36607  legov 28865
[Schwabhauser] p. 41Definition 5.5legov2 28866
[Schwabhauser] p. 42Remark 5.13legso 28879
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36610
[Schwabhauser] p. 42Theorem 5.7seglerflx 36612
[Schwabhauser] p. 42Theorem 5.8segletr 36614
[Schwabhauser] p. 42Theorem 5.9segleantisym 36615
[Schwabhauser] p. 42Theorem 5.10seglelin 36616
[Schwabhauser] p. 42Theorem 5.11seglemin 36613
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36618
[Schwabhauser] p. 42Proposition 5.7legid 28867
[Schwabhauser] p. 42Proposition 5.8legtrd 28869
[Schwabhauser] p. 42Proposition 5.9legtri3 28870
[Schwabhauser] p. 42Proposition 5.10legtrid 28871
[Schwabhauser] p. 42Proposition 5.11leg0 28872
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36625
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36626
[Schwabhauser] p. 43Theorem 6.4broutsideof 36621  df-outsideof 36620
[Schwabhauser] p. 43Definition 6.1broutsideof2 36622  ishlg 28885
[Schwabhauser] p. 44Theorem 6.4hlln 28890
[Schwabhauser] p. 44Theorem 6.5hlid 28892  outsideofrflx 36627
[Schwabhauser] p. 44Theorem 6.6hlcomb 28886  hlcomd 28887  outsideofcom 36628
[Schwabhauser] p. 44Theorem 6.7hltr 28893  outsideoftr 36629
[Schwabhauser] p. 44Theorem 6.11hlcgreq 28902  hlcgreu 28901  outsideofeu 36631
[Schwabhauser] p. 44Definition 6.8df-ray 36638
[Schwabhauser] p. 45Part 2df-lines2 36639
[Schwabhauser] p. 45Theorem 6.13outsidele 36632
[Schwabhauser] p. 45Theorem 6.15lineunray 36647
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36648  tglineelsb2 28916
[Schwabhauser] p. 45Theorem 6.17linecom 36650  linerflx1 36649  linerflx2 36651  tglinecom 28919  tglinerflx1 28917  tglinerflx2 28918
[Schwabhauser] p. 45Theorem 6.18linethru 36653  tglinethru 28920
[Schwabhauser] p. 45Definition 6.14df-line2 36637  tglng 28826
[Schwabhauser] p. 45Proposition 6.13legbtwn 28874
[Schwabhauser] p. 46Theorem 6.19linethrueu 36656  tglinethrueu 28923
[Schwabhauser] p. 46Theorem 6.21lineintmo 36657  tglineineq 28927  tglineinsn 28928  tglineinteq 28930  tglineintmo 28926
[Schwabhauser] p. 46Theorem 6.23colline 28934
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28935
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28936
[Schwabhauser] p. 49Theorem 7.3mirinv 28954
[Schwabhauser] p. 49Theorem 7.7mirmir 28950
[Schwabhauser] p. 49Theorem 7.8mirreu3 28942
[Schwabhauser] p. 49Definition 7.5df-mir 28941  ismir 28947  mirbtwn 28946  mircgr 28945  mirfv 28944  mirval 28943
[Schwabhauser] p. 50Theorem 7.8mirreu 28952
[Schwabhauser] p. 50Theorem 7.9mireq 28953
[Schwabhauser] p. 50Theorem 7.10mirinv 28954
[Schwabhauser] p. 50Theorem 7.11mirf1o 28957
[Schwabhauser] p. 50Theorem 7.13miriso 28958
[Schwabhauser] p. 51Theorem 7.14mirmot 28963
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28960  mirbtwni 28959
[Schwabhauser] p. 51Theorem 7.16mircgrs 28961
[Schwabhauser] p. 51Theorem 7.17miduniq 28973
[Schwabhauser] p. 52Lemma 7.21symquadlem 28977  symquadmid 29119
[Schwabhauser] p. 52Theorem 7.18miduniq1 28974
[Schwabhauser] p. 52Theorem 7.19miduniq2 28975
[Schwabhauser] p. 52Theorem 7.20colmid 28976
[Schwabhauser] p. 53Lemma 7.22krippen 28979
[Schwabhauser] p. 55Lemma 7.25midexlem 28980
[Schwabhauser] p. 57Theorem 8.2ragcom 28989
[Schwabhauser] p. 57Definition 8.1df-rag 28985  israg 28988
[Schwabhauser] p. 58Theorem 8.3ragcol 28990
[Schwabhauser] p. 58Theorem 8.4ragmir 28991
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28993
[Schwabhauser] p. 58Theorem 8.6ragflat2 28994
[Schwabhauser] p. 58Theorem 8.7ragflat 28995
[Schwabhauser] p. 58Theorem 8.8ragtriva 28996
[Schwabhauser] p. 58Theorem 8.9ragflat3 28997  ragncol 29000
[Schwabhauser] p. 58Theorem 8.10ragcgr 28998
[Schwabhauser] p. 59Theorem 8.12perpcom 29004
[Schwabhauser] p. 59Theorem 8.13ragperp 29008
[Schwabhauser] p. 59Theorem 8.14perpneq 29005
[Schwabhauser] p. 59Definition 8.11df-perpg 28987  isperp 29003
[Schwabhauser] p. 59Definition 8.13isperp2 29006
[Schwabhauser] p. 60Theorem 8.18foot 29013
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 29022  colperpexlem2 29023
[Schwabhauser] p. 63Theorem 8.21colperpex 29025  colperpexlem3 29024
[Schwabhauser] p. 64Theorem 8.22mideu 29030  midex 29029
[Schwabhauser] p. 66Lemma 8.24opphllem 29027
[Schwabhauser] p. 67Theorem 9.2oppcom 29036
[Schwabhauser] p. 67Definition 9.1islnopp 29031
[Schwabhauser] p. 68Lemma 9.3opphllem2 29040
[Schwabhauser] p. 68Lemma 9.4opphllem5 29043  opphllem6 29044
[Schwabhauser] p. 69Theorem 9.5opphl 29046
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28747
[Schwabhauser] p. 70Theorem 9.6outpasch 29048
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 29056
[Schwabhauser] p. 71Definition 9.7df-hpg 29051  hpgbr 29053
[Schwabhauser] p. 72Lemma 9.10hpgerlem 29058
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 29057
[Schwabhauser] p. 72Theorem 9.11hpgid 29059
[Schwabhauser] p. 72Theorem 9.12hpgcom 29060
[Schwabhauser] p. 72Theorem 9.13hpgtr 29061
[Schwabhauser] p. 73Theorem 9.18colopp 29062
[Schwabhauser] p. 73Theorem 9.19colhp 29063
[Schwabhauser] p. 74Lemma 9.22lnincplng 29077
[Schwabhauser] p. 74Theorem 9.21plngcp 29079
[Schwabhauser] p. 74Theorem 9.24plngrot 29083
[Schwabhauser] p. 74Definition 9.20df-plng 29067  elplng 29073
[Schwabhauser] p. 75Theorem 9.25lnssplng 29085  lnssplng1 29086
[Schwabhauser] p. 76Theorem 9.26plng3p 29090
[Schwabhauser] p. 88Theorem 10.2lmieu 29104
[Schwabhauser] p. 88Definition 10.1df-mid 29094
[Schwabhauser] p. 89Theorem 10.4lmicom 29108
[Schwabhauser] p. 89Theorem 10.5lmilmi 29109
[Schwabhauser] p. 89Theorem 10.6lmireu 29110
[Schwabhauser] p. 89Theorem 10.7lmieq 29111
[Schwabhauser] p. 89Theorem 10.8lmiinv 29112
[Schwabhauser] p. 89Theorem 10.9lmif1o 29115
[Schwabhauser] p. 89Theorem 10.10lmiiso 29117
[Schwabhauser] p. 89Definition 10.3df-lmi 29095
[Schwabhauser] p. 90Theorem 10.11lmimot 29118
[Schwabhauser] p. 91Theorem 10.12hypcgr 29122
[Schwabhauser] p. 92Theorem 10.14lmiopp 29123
[Schwabhauser] p. 92Theorem 10.15lnperpex 29124  lnperpexs 29125
[Schwabhauser] p. 92Theorem 10.16trgcopy 29126  trgcopyeu 29128
[Schwabhauser] p. 95Definition 11.2dfcgra2 29152
[Schwabhauser] p. 95Definition 11.3iscgra 29131
[Schwabhauser] p. 95Proposition 11.4cgracgr 29140
[Schwabhauser] p. 95Proposition 11.10cgrahl1 29138  cgrahl2 29139
[Schwabhauser] p. 96Theorem 11.6cgraid 29141
[Schwabhauser] p. 96Theorem 11.9cgraswap 29142
[Schwabhauser] p. 97Theorem 11.7cgracom 29144
[Schwabhauser] p. 97Theorem 11.8cgratr 29145
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 29148  cgrahl 29149
[Schwabhauser] p. 98Theorem 11.13sacgr 29153
[Schwabhauser] p. 98Theorem 11.14oacgr 29154
[Schwabhauser] p. 98Theorem 11.15acopy 29155  acopyeu 29156
[Schwabhauser] p. 98Theorem 11.16ragcgra 29157
[Schwabhauser] p. 98Theorem 11.17cgrarag 29158
[Schwabhauser] p. 98Theorem 11.18ragsupplcgra 29159
[Schwabhauser] p. 99Theorem 11.19ragraghl 29160
[Schwabhauser] p. 99Theorem 11.20perpeq 29162
[Schwabhauser] p. 101Theorem 11.24inagswap 29169
[Schwabhauser] p. 101Theorem 11.25inaghl 29173
[Schwabhauser] p. 101Definition 11.23isinag 29166
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 29181
[Schwabhauser] p. 102Definition 11.27df-leag 29174  isleag 29175
[Schwabhauser] p. 107Theorem 11.49tgsas 29183  tgsas1 29182  tgsas2 29184  tgsas3 29185
[Schwabhauser] p. 108Theorem 11.50tgasa 29187  tgasa1 29186
[Schwabhauser] p. 109Theorem 11.51tgsss1 29188  tgsss2 29189  tgsss3 29190
[Schwabhauser] p. 121Definition 12.2df-prlng 29198
[Schwabhauser] p. 122Theorem 12.4prlngref 29201
[Schwabhauser] p. 122Theorem 12.5prlngsym 29202
[Schwabhauser] p. 122Theorem 12.6prlnghpg 29207
[Schwabhauser] p. 122Theorem 12.7dfprlng2 29208  dfprlng3 29209
[Schwabhauser] p. 122Theorem 12.9perpprlng 29211
[Schwabhauser] p. 122Theorem 12.10prlngex 29212
[Schwabhauser] p. 123Theorem 12.11prlngmo 29215  prlngmo2 29217
[Schwabhauser] p. 124Theorem 12.13prlngeu 29216
[Schwabhauser] p. 124Theorem 12.14prlngpln4 29219
[Schwabhauser] p. 124Theorem 12.15prlngplngtr 29220
[Schwabhauser] p. 125Theorem 12.16prlnginn0 29221
[Schwabhauser] p. 125Theorem 12.17prlngmid2 29222
[Schwabhauser] p. 126Theorem 12.18symquadprlng 29223
[Schwabhauser] p. 126Theorem 12.19prlngsymquad 29225  prlngsymquadopp 29226
[Schwabhauser] p. 126Theorem 12.20quadcgrprlng 29227
[Schwabhauser] p. 126Theorem 12.21tgaltai 29228
[Shapiro] p. 230Theorem 6.5.1dchrhash 27446  dchrsum 27444  dchrsum2 27443  sumdchr 27447
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27448  sum2dchr 27449
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20144  ablfacrp2 20145
[Shapiro], p. 328Equation 9.2.4vmasum 27391
[Shapiro], p. 329Equation 9.2.7logfac2 27392
[Shapiro], p. 329Equation 9.2.9logfacrlim 27399
[Shapiro], p. 331Equation 9.2.13vmadivsum 27657
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27660
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27714  vmalogdivsum2 27713
[Shapiro], p. 375Theorem 9.4.1dirith 27704  dirith2 27703
[Shapiro], p. 375Equation 9.4.3rplogsum 27702  rpvmasum 27701  rpvmasum2 27687
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27662
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27700
[Shapiro], p. 377Lemma 9.4.1dchrisum 27667  dchrisumlem1 27664  dchrisumlem2 27665  dchrisumlem3 27666  dchrisumlema 27663
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27670
[Shapiro], p. 379Equation 9.4.16dchrmusum 27699  dchrmusumlem 27697  dchrvmasumlem 27698
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27669
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27671
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27695  dchrisum0re 27688  dchrisumn0 27696
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27681
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27685
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27686
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27741  pntrsumbnd2 27742  pntrsumo1 27740
[Shapiro], p. 405Equation 10.2.1mudivsum 27705
[Shapiro], p. 406Equation 10.2.6mulogsum 27707
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27709
[Shapiro], p. 407Equation 10.2.8mulog2sum 27712
[Shapiro], p. 418Equation 10.4.6logsqvma 27717
[Shapiro], p. 418Equation 10.4.8logsqvma2 27718
[Shapiro], p. 419Equation 10.4.10selberg 27723
[Shapiro], p. 420Equation 10.4.12selberg2lem 27725
[Shapiro], p. 420Equation 10.4.14selberg2 27726
[Shapiro], p. 422Equation 10.6.7selberg3 27734
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27735
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27732  selberg3lem2 27733
[Shapiro], p. 422Equation 10.4.23selberg4 27736
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27730
[Shapiro], p. 428Equation 10.6.2selbergr 27743
[Shapiro], p. 429Equation 10.6.8selberg3r 27744
[Shapiro], p. 430Equation 10.6.11selberg4r 27745
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27759
[Shapiro], p. 434Equation 10.6.27pntlema 27771  pntlemb 27772  pntlemc 27770  pntlemd 27769  pntlemg 27773
[Shapiro], p. 435Equation 10.6.29pntlema 27771
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27763
[Shapiro], p. 436Lemma 10.6.2pntibnd 27768
[Shapiro], p. 436Equation 10.6.34pntlema 27771
[Shapiro], p. 436Equation 10.6.35pntlem3 27784  pntleml 27786
[Stewart] p. 91Lemma 7.3constrss 34142
[Stewart] p. 92Definition 7.4.df-constr 34129
[Stewart] p. 96Theorem 7.10constraddcl 34161  constrinvcl 34172  constrmulcl 34170  constrnegcl 34162  constrsqrtcl 34178
[Stewart] p. 97Theorem 7.11constrextdg2 34148
[Stewart] p. 98Theorem 7.12constrext2chn 34158
[Stewart] p. 99Theorem 7.132sqr3nconstr 34180
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34190
[Stoll] p. 13Definition corresponds to dfsymdif3 4258
[Stoll] p. 16Exercise 4.40dif 4362  dif0 4333
[Stoll] p. 16Exercise 4.8difdifdir 4451
[Stoll] p. 17Theorem 5.1(5)unvdif 4435
[Stoll] p. 19Theorem 5.2(13)undm 4249
[Stoll] p. 19Theorem 5.2(13')indm 4250
[Stoll] p. 20Remarkinvdif 4231
[Stoll] p. 25Definition of ordered tripledf-ot 4597
[Stoll] p. 43Definitionuniiun 5022
[Stoll] p. 44Definitionintiin 5023
[Stoll] p. 45Definitiondf-iin 4958
[Stoll] p. 45Definition indexed uniondf-iun 4957
[Stoll] p. 176Theorem 3.4(27)iman 406
[Stoll] p. 262Example 4.1dfsymdif3 4258
[Strang] p. 242Section 6.3expgrowth 45073
[Suppes] p. 22Theorem 2eq0 4303  eq0f 4300
[Suppes] p. 22Theorem 4eqss 3951  eqssd 3953  eqssi 3952
[Suppes] p. 23Theorem 5ss0 4358  ss0b 4357
[Suppes] p. 23Theorem 6sstr 3944  sstrALT2 45571
[Suppes] p. 23Theorem 7pssirr 4056
[Suppes] p. 23Theorem 8pssn2lp 4058
[Suppes] p. 23Theorem 9psstr 4061
[Suppes] p. 23Theorem 10pssss 4051
[Suppes] p. 25Theorem 12elin 3920  elun 4106
[Suppes] p. 26Theorem 15inidm 4178
[Suppes] p. 26Theorem 16in0 4351
[Suppes] p. 27Theorem 23unidm 4110
[Suppes] p. 27Theorem 24un0 4350
[Suppes] p. 27Theorem 25ssun1 4130
[Suppes] p. 27Theorem 26ssequn1 4138
[Suppes] p. 27Theorem 27unss 4142
[Suppes] p. 27Theorem 28indir 4238
[Suppes] p. 27Theorem 29undir 4239
[Suppes] p. 28Theorem 32difid 4331
[Suppes] p. 29Theorem 33difin 4224
[Suppes] p. 29Theorem 34indif 4232
[Suppes] p. 29Theorem 35undif1 4436
[Suppes] p. 29Theorem 36difun2 4441
[Suppes] p. 29Theorem 37difin0 4434
[Suppes] p. 29Theorem 38disjdif 4432
[Suppes] p. 29Theorem 39difundi 4242
[Suppes] p. 29Theorem 40difindi 4244
[Suppes] p. 30Theorem 41nalset 5276
[Suppes] p. 39Theorem 61uniss 4879
[Suppes] p. 39Theorem 65uniop 5497
[Suppes] p. 41Theorem 70intsn 4948
[Suppes] p. 42Theorem 71intpr 4946  intprg 4945
[Suppes] p. 42Theorem 73op1stb 5452
[Suppes] p. 42Theorem 78intun 4944
[Suppes] p. 44Definition 15(a)dfiun2 4995  dfiun2g 4993
[Suppes] p. 44Definition 15(b)dfiin2 4996
[Suppes] p. 47Theorem 86elpw 4565  elpw2 5304  elpw2g 5303  elpwg 4564  elpwgdedVD 45653
[Suppes] p. 47Theorem 87pwid 4584
[Suppes] p. 47Theorem 89pw0 4777
[Suppes] p. 48Theorem 90pwpw0 4778
[Suppes] p. 52Theorem 101xpss12 5675
[Suppes] p. 52Theorem 102xpindi 5818  xpindir 5819
[Suppes] p. 52Theorem 103xpundi 5729  xpundir 5730
[Suppes] p. 54Theorem 105elirrv 9557
[Suppes] p. 58Theorem 2relss 5767
[Suppes] p. 59Theorem 4eldm 5889  eldm2 5890  eldm2g 5888  eldmg 5887
[Suppes] p. 59Definition 3df-dm 5670
[Suppes] p. 60Theorem 6dmin 5900
[Suppes] p. 60Theorem 8rnun 6141
[Suppes] p. 60Theorem 9rnin 6142
[Suppes] p. 60Definition 4dfrn2 5877
[Suppes] p. 61Theorem 11brcnv 5867  brcnvg 5864
[Suppes] p. 62Equation 5elcnv 5861  elcnv2 5862
[Suppes] p. 62Theorem 12relcnv 6105
[Suppes] p. 62Theorem 15cnvin 6140
[Suppes] p. 62Theorem 16cnvun 6138
[Suppes] p. 63Definitiondftrrels2 39336
[Suppes] p. 63Theorem 20co02 6261
[Suppes] p. 63Theorem 21dmcoss 5964
[Suppes] p. 63Definition 7df-co 5669
[Suppes] p. 64Theorem 26cnvco 5874
[Suppes] p. 64Theorem 27coass 6266
[Suppes] p. 65Theorem 31resundi 5991
[Suppes] p. 65Theorem 34elima 6066  elima2 6067  elima3 6068  elimag 6065
[Suppes] p. 65Theorem 35imaundi 6146
[Suppes] p. 66Theorem 40dminss 6149
[Suppes] p. 66Theorem 41imainss 6150
[Suppes] p. 67Exercise 11cnvxp 6153
[Suppes] p. 81Definition 34dfec2 8695
[Suppes] p. 82Theorem 72elec 8739  elecALTV 38948  elecg 8737
[Suppes] p. 82Theorem 73eqvrelth 39372  erth 8747  erth2 8748
[Suppes] p. 83Theorem 74eqvreldisj 39375  erdisj 8750
[Suppes] p. 83Definition 35, df-parts 39545  dfmembpart2 39550
[Suppes] p. 89Theorem 96map0b 8879
[Suppes] p. 89Theorem 97map0 8883  map0g 8880
[Suppes] p. 89Theorem 98mapsn 8884  mapsnd 8882
[Suppes] p. 89Theorem 99mapss 8885
[Suppes] p. 91Definition 12(ii)alephsuc 10059
[Suppes] p. 91Definition 12(iii)alephlim 10058
[Suppes] p. 92Theorem 1enref 8980  enrefg 8979
[Suppes] p. 92Theorem 2ensym 8998  ensymb 8997  ensymi 8999
[Suppes] p. 92Theorem 3entr 9001
[Suppes] p. 92Theorem 4unen 9040
[Suppes] p. 94Theorem 15endom 8974
[Suppes] p. 94Theorem 16ssdomg 8995
[Suppes] p. 94Theorem 17domtr 9002
[Suppes] p. 95Theorem 18sbth 9083
[Suppes] p. 97Theorem 23canth2 9116  canth2g 9117
[Suppes] p. 97Definition 3brsdom2 9087  df-sdom 8944  dfsdom2 9086
[Suppes] p. 97Theorem 21(i)sdomirr 9100
[Suppes] p. 97Theorem 22(i)domnsym 9089
[Suppes] p. 97Theorem 21(ii)sdomnsym 9088
[Suppes] p. 97Theorem 22(ii)domsdomtr 9098
[Suppes] p. 97Theorem 22(iv)brdom2 8977
[Suppes] p. 97Theorem 21(iii)sdomtr 9101
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9096
[Suppes] p. 98Exercise 4fundmen 9026  fundmeng 9027
[Suppes] p. 98Exercise 6xpdom3 9061
[Suppes] p. 98Exercise 11sdomentr 9097
[Suppes] p. 104Theorem 37fofi 9271
[Suppes] p. 104Theorem 38pwfi 9276
[Suppes] p. 105Theorem 40pwfi 9276
[Suppes] p. 111Axiom for cardinal numberscarden 10541
[Suppes] p. 130Definition 3df-tr 5218
[Suppes] p. 132Theorem 9ssonuni 7777
[Suppes] p. 134Definition 6df-suc 6366
[Suppes] p. 136Theorem Schema 22findes 7895  finds 7891  finds1 7894  finds2 7893
[Suppes] p. 151Theorem 42isfinite 9619  isfinite2 9256  isfiniteg 9258  unbnn 9254
[Suppes] p. 162Definition 5df-ltnq 10909  df-ltpq 10901
[Suppes] p. 197Theorem Schema 4tfindes 7857  tfinds 7854  tfinds2 7858
[Suppes] p. 209Theorem 18oaord1 8534
[Suppes] p. 209Theorem 21oaword2 8536
[Suppes] p. 211Theorem 25oaass 8544
[Suppes] p. 225Definition 8iscard2 9969
[Suppes] p. 227Theorem 56ondomon 10553
[Suppes] p. 228Theorem 59harcard 9971
[Suppes] p. 228Definition 12(i)aleph0 10057
[Suppes] p. 228Theorem Schema 61onintss 6413
[Suppes] p. 228Theorem Schema 62onminesb 7790  onminsb 7791
[Suppes] p. 229Theorem 64alephval2 10563
[Suppes] p. 229Theorem 65alephcard 10061
[Suppes] p. 229Theorem 66alephord2i 10068
[Suppes] p. 229Theorem 67alephnbtwn 10062
[Suppes] p. 229Definition 12df-aleph 9933
[Suppes] p. 242Theorem 6weth 10485
[Suppes] p. 242Theorem 8entric 10547
[Suppes] p. 242Theorem 9carden 10541
[Szendrei] p. 11Line 6df-cloneop 36196
[Szendrei] p. 11Paragraph 3df-suppos 36200
[TakeutiZaring] p. 8Axiom 1ax-ext 2734
[TakeutiZaring] p. 13Definition 4.5df-cleq 2754  wl-df.cleq 38182
[TakeutiZaring] p. 13Proposition 4.6df-clel 2837  wl-df.clel 38185
[TakeutiZaring] p. 13Proposition 4.9cvjust 2756
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2782
[TakeutiZaring] p. 14Definition 4.16df-oprab 7416
[TakeutiZaring] p. 14Proposition 4.14ru 3742
[TakeutiZaring] p. 15Axiom 2zfpair 5391
[TakeutiZaring] p. 15Exercise 1elpr 4613  elpr2 4615  elpr2g 4614  elprg 4611
[TakeutiZaring] p. 15Exercise 2elsn 4603  elsn2 4630  elsn2g 4629  elsng 4602  velsn 4604
[TakeutiZaring] p. 15Exercise 3elop 5448
[TakeutiZaring] p. 15Exercise 4sneq 4598  sneqr 4804
[TakeutiZaring] p. 15Definition 5.1dfpr2 4609  dfsn2 4601  dfsn2ALT 4610
[TakeutiZaring] p. 16Axiom 3uniex 7741
[TakeutiZaring] p. 16Exercise 6opth 5457
[TakeutiZaring] p. 16Exercise 7opex 5444
[TakeutiZaring] p. 16Exercise 8rext 5428
[TakeutiZaring] p. 16Corollary 5.8unex 7744  unexg 7743
[TakeutiZaring] p. 16Definition 5.3dftp2 4656
[TakeutiZaring] p. 16Definition 5.5df-uni 4872
[TakeutiZaring] p. 16Definition 5.6df-in 3911  df-un 3909
[TakeutiZaring] p. 16Proposition 5.7unipr 4888  uniprg 4887
[TakeutiZaring] p. 17Axiom 4vpwex 5347
[TakeutiZaring] p. 17Exercise 1eltp 4654
[TakeutiZaring] p. 17Exercise 5elsuc 6433  elsucg 6431  sstr2 3943
[TakeutiZaring] p. 17Exercise 6uncom 4111
[TakeutiZaring] p. 17Exercise 7incom 4161
[TakeutiZaring] p. 17Exercise 8unass 4124
[TakeutiZaring] p. 17Exercise 9inass 4179
[TakeutiZaring] p. 17Exercise 10indi 4236
[TakeutiZaring] p. 17Exercise 11undi 4237
[TakeutiZaring] p. 17Definition 5.9df-pss 3924  df-ss 3921
[TakeutiZaring] p. 17Definition 5.10df-pw 4563
[TakeutiZaring] p. 18Exercise 7unss2 4139
[TakeutiZaring] p. 18Exercise 9dfss2 3922  sseqin2 4175
[TakeutiZaring] p. 18Exercise 10ssid 3958
[TakeutiZaring] p. 18Exercise 12inss1 4188  inss2 4189
[TakeutiZaring] p. 18Exercise 13nss 4000
[TakeutiZaring] p. 18Exercise 15unieq 4882
[TakeutiZaring] p. 18Exercise 18sspwb 5429  sspwimp 45654  sspwimpALT 45661  sspwimpALT2 45664  sspwimpcf 45656
[TakeutiZaring] p. 18Exercise 19pweqb 5436
[TakeutiZaring] p. 19Axiom 5ax-rep 5237
[TakeutiZaring] p. 20Definitiondf-rab 3416
[TakeutiZaring] p. 20Corollary 5.160ex 5269
[TakeutiZaring] p. 20Definition 5.12df-dif 3907
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 37191  dfnul2 4288
[TakeutiZaring] p. 20Proposition 5.15difid 4331
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4306  n0f 4302  neq0 4305  neq0f 4301
[TakeutiZaring] p. 21Axiom 6zfreg 9556
[TakeutiZaring] p. 21Axiom 6'zfregs 9699
[TakeutiZaring] p. 21Theorem 5.22setind 9714
[TakeutiZaring] p. 21Definition 5.20df-v 3456
[TakeutiZaring] p. 21Proposition 5.21vprc 5282
[TakeutiZaring] p. 22Exercise 10ss 4356
[TakeutiZaring] p. 22Exercise 3ssex 5290  ssexg 5289
[TakeutiZaring] p. 22Exercise 4inex1 5285
[TakeutiZaring] p. 22Exercise 5ruv 9568
[TakeutiZaring] p. 22Exercise 6elirr 9560
[TakeutiZaring] p. 22Exercise 7ssdif0 4320
[TakeutiZaring] p. 22Exercise 11difdif 4088
[TakeutiZaring] p. 22Exercise 13undif3 4252  undif3VD 45618
[TakeutiZaring] p. 22Exercise 14difss 4089
[TakeutiZaring] p. 22Exercise 15sscon 4096
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3079
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3089
[TakeutiZaring] p. 23Proposition 6.2xpex 7750  xpexg 7747
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5667
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6607
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6785  fun11 6610
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6549  svrelfun 6608
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5876
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5878
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5672
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5673
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5669
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6191  dfrel2 6186
[TakeutiZaring] p. 25Exercise 3xpss 5676
[TakeutiZaring] p. 25Exercise 5relun 5797
[TakeutiZaring] p. 25Exercise 6reluni 5804
[TakeutiZaring] p. 25Exercise 9inxp 5817
[TakeutiZaring] p. 25Exercise 12relres 6003
[TakeutiZaring] p. 25Exercise 13opelres 5983  opelresi 5985
[TakeutiZaring] p. 25Exercise 14dmres 6010
[TakeutiZaring] p. 25Exercise 15resss 5999
[TakeutiZaring] p. 25Exercise 17resabs1 6004
[TakeutiZaring] p. 25Exercise 18funres 6578
[TakeutiZaring] p. 25Exercise 24relco 6109
[TakeutiZaring] p. 25Exercise 29funco 6576
[TakeutiZaring] p. 25Exercise 30f1co 6787
[TakeutiZaring] p. 26Definition 6.10eu2 2636
[TakeutiZaring] p. 26Definition 6.11conventions 30762  df-fv 6544  fv3 6899
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7920  cnvexg 7919
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7904  dmexg 7896
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7905  rnexg 7897
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 45190
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7915
[TakeutiZaring] p. 27Corollary 6.13fvex 6894
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47939  tz6.12-1-afv2 48006  tz6.12-1 6904  tz6.12-afv 47938  tz6.12-afv2 48005  tz6.12 6905  tz6.12c-afv2 48007  tz6.12c 6903
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 48002  tz6.12-2 6868  tz6.12i-afv2 48008  tz6.12i 6907
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6539
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6540
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6542  wfo 6534
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6541  wf1 6533
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6543  wf1o 6535
[TakeutiZaring] p. 28Exercise 4eqfnfv 7025  eqfnfv2 7026  eqfnfv2f 7029
[TakeutiZaring] p. 28Exercise 5fvco 6979
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7215
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7213
[TakeutiZaring] p. 29Exercise 9funimaex 6623  funimaexg 6622
[TakeutiZaring] p. 29Definition 6.18df-br 5109
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5569
[TakeutiZaring] p. 30Definition 6.21dffr2 5621  dffr3 6100  eliniseg 6095  iniseg 6098
[TakeutiZaring] p. 30Definition 6.22df-eprel 5560
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5637  fr3nr 7769  frirr 5636
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5613
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7771
[TakeutiZaring] p. 31Exercise 1frss 5624
[TakeutiZaring] p. 31Exercise 4wess 5646
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6348  tz6.26i 6349  wefrc 5654  wereu2 5657
[TakeutiZaring] p. 32Theorem 6.27wfi 6350  wfii 6351
[TakeutiZaring] p. 32Definition 6.28df-isom 6545
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7327
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7328
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7334
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7335
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7336
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7340
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7347
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7349
[TakeutiZaring] p. 35Notationwtr 5217
[TakeutiZaring] p. 35Theorem 7.2trelpss 45191  tz7.2 5643
[TakeutiZaring] p. 35Definition 7.1dftr3 5222
[TakeutiZaring] p. 36Proposition 7.4ordwe 6373
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6381
[TakeutiZaring] p. 36Proposition 7.6ordelord 6382  ordelordALT 45274  ordelordALTVD 45603
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6388  ordelssne 6387
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6386
[TakeutiZaring] p. 37Proposition 7.9ordin 6391
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7779
[TakeutiZaring] p. 38Corollary 7.15ordsson 7780
[TakeutiZaring] p. 38Definition 7.11df-on 6364
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6393
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45286  ordon 7774
[TakeutiZaring] p. 38Proposition 7.13onprc 7775
[TakeutiZaring] p. 39Theorem 7.17tfi 7847
[TakeutiZaring] p. 40Exercise 3ontr2 6409  ontr2d 36700
[TakeutiZaring] p. 40Exercise 7dftr2 5219
[TakeutiZaring] p. 40Exercise 9onssmin 7789
[TakeutiZaring] p. 40Exercise 11unon 7825
[TakeutiZaring] p. 40Exercise 12ordun 6467
[TakeutiZaring] p. 40Exercise 14ordequn 6466
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7776
[TakeutiZaring] p. 40Proposition 7.20elssuni 4903
[TakeutiZaring] p. 41Definition 7.22df-suc 6366
[TakeutiZaring] p. 41Proposition 7.23sssucid 6443  sucidg 6444
[TakeutiZaring] p. 41Proposition 7.24onsuc 7807
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6457  ordnbtwn 6456
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7822
[TakeutiZaring] p. 42Exercise 1df-lim 6365
[TakeutiZaring] p. 42Exercise 4omssnlim 7875
[TakeutiZaring] p. 42Exercise 7ssnlim 7880
[TakeutiZaring] p. 42Exercise 8onsucssi 7835  ordelsuc 7814
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7816
[TakeutiZaring] p. 42Definition 7.27nlimon 7845
[TakeutiZaring] p. 42Definition 7.28dfom2 7862
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7883
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7884
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7885
[TakeutiZaring] p. 43Remarkomon 7872
[TakeutiZaring] p. 43Axiom 7inf3 9602  omex 9610
[TakeutiZaring] p. 43Theorem 7.32ordom 7870
[TakeutiZaring] p. 43Corollary 7.31find 7890
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7887
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7888
[TakeutiZaring] p. 44Exercise 1limomss 7865
[TakeutiZaring] p. 44Exercise 2int0 4926
[TakeutiZaring] p. 44Exercise 3trintss 5236
[TakeutiZaring] p. 44Exercise 4intss1 4927
[TakeutiZaring] p. 44Exercise 5intex 5313
[TakeutiZaring] p. 44Exercise 6oninton 7792
[TakeutiZaring] p. 44Exercise 11ordintdif 6412
[TakeutiZaring] p. 44Definition 7.35df-int 4912
[TakeutiZaring] p. 44Proposition 7.34noinfep 9627
[TakeutiZaring] p. 45Exercise 4onint 7787
[TakeutiZaring] p. 47Lemma 1tfrlem1 8360
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8382
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8383
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8384
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8391  tz7.44-2 8392  tz7.44-3 8393
[TakeutiZaring] p. 50Exercise 1smogt 8352
[TakeutiZaring] p. 50Exercise 3smoiso 8347
[TakeutiZaring] p. 50Definition 7.46df-smo 8331
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8430  tz7.49c 8431
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8428
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8427
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8429
[TakeutiZaring] p. 53Proposition 7.532eu5 2682
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10002
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10003
[TakeutiZaring] p. 56Definition 8.1oalim 8515  oasuc 8507
[TakeutiZaring] p. 57Remarktfindsg 7855
[TakeutiZaring] p. 57Proposition 8.2oacl 8518
[TakeutiZaring] p. 57Proposition 8.3oa0 8499  oa0r 8521
[TakeutiZaring] p. 57Proposition 8.16omcl 8519
[TakeutiZaring] p. 58Corollary 8.5oacan 8531
[TakeutiZaring] p. 58Proposition 8.4nnaord 8603  nnaordi 8602  oaord 8530  oaordi 8529
[TakeutiZaring] p. 59Proposition 8.6iunss2 5013  uniss2 4906
[TakeutiZaring] p. 59Proposition 8.7oawordri 8533
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8538  oawordex 8540
[TakeutiZaring] p. 59Proposition 8.9nnacl 8595
[TakeutiZaring] p. 59Proposition 8.10oaabs 8632
[TakeutiZaring] p. 60Remarkoancom 9618
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8543
[TakeutiZaring] p. 62Exercise 1nnarcl 8600
[TakeutiZaring] p. 62Exercise 5oaword1 8535
[TakeutiZaring] p. 62Definition 8.15om0x 8502  omlim 8516  omsuc 8509
[TakeutiZaring] p. 62Definition 8.15(a)om0 8500
[TakeutiZaring] p. 63Proposition 8.17nnecl 8597  nnmcl 8596
[TakeutiZaring] p. 63Proposition 8.19nnmord 8616  nnmordi 8615  omord 8551  omordi 8549
[TakeutiZaring] p. 63Proposition 8.20omcan 8552
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8620  omwordri 8555
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8522
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8525  om1r 8526
[TakeutiZaring] p. 64Proposition 8.22om00 8558
[TakeutiZaring] p. 64Proposition 8.23omordlim 8560
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8561
[TakeutiZaring] p. 64Proposition 8.25odi 8562
[TakeutiZaring] p. 65Theorem 8.26omass 8563
[TakeutiZaring] p. 67Definition 8.30nnesuc 8592  oe0 8505  oelim 8517  oesuc 8510  onesuc 8513
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8503
[TakeutiZaring] p. 67Proposition 8.32oen0 8570
[TakeutiZaring] p. 67Proposition 8.33oeordi 8571
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8504
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8528
[TakeutiZaring] p. 68Corollary 8.34oeord 8572
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8578
[TakeutiZaring] p. 68Proposition 8.35oewordri 8576
[TakeutiZaring] p. 68Proposition 8.37oeworde 8577
[TakeutiZaring] p. 69Proposition 8.41oeoa 8581
[TakeutiZaring] p. 70Proposition 8.42oeoe 8583
[TakeutiZaring] p. 73Theorem 9.1trcl 9695  tz9.1 9696
[TakeutiZaring] p. 76Definition 9.9df-r1 9734  r10 9738  r1lim 9742  r1limg 9741  r1suc 9740  r1sucg 9739
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9750  r1ord2 9751  r1ordg 9748
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9760
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9785  tz9.13 9761  tz9.13g 9762
[TakeutiZaring] p. 79Definition 9.14df-rank 9735  rankval 9786  rankvalb 9767  rankvalg 9787
[TakeutiZaring] p. 79Proposition 9.16rankel 9809  rankelb 9794
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9823  rankval3 9810  rankval3b 9796
[TakeutiZaring] p. 79Proposition 9.18rankonid 9799
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9765
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9804  rankr1c 9791  rankr1g 9802
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9805
[TakeutiZaring] p. 80Exercise 1rankss 9819  rankssb 9818
[TakeutiZaring] p. 80Exercise 2unbndrank 9812
[TakeutiZaring] p. 80Proposition 9.19bndrank 9811
[TakeutiZaring] p. 83Axiom of Choiceac4 10465  dfac3 10112
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10021  numth 10462  numth2 10461
[TakeutiZaring] p. 85Definition 10.4cardval 10536
[TakeutiZaring] p. 85Proposition 10.5cardid 10537  cardid2 9946
[TakeutiZaring] p. 85Proposition 10.9oncard 9953
[TakeutiZaring] p. 85Proposition 10.10carden 10541
[TakeutiZaring] p. 85Proposition 10.11cardidm 9952
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9937
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9958
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9950
[TakeutiZaring] p. 87Proposition 10.15pwen 9136
[TakeutiZaring] p. 88Exercise 1en0 9013
[TakeutiZaring] p. 88Exercise 7infensuc 9141
[TakeutiZaring] p. 89Exercise 10omxpen 9065
[TakeutiZaring] p. 90Corollary 10.23cardnn 9956
[TakeutiZaring] p. 90Definition 10.27alephiso 10089
[TakeutiZaring] p. 90Proposition 10.20nneneq 9188
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9196
[TakeutiZaring] p. 90Proposition 10.26alephprc 10090
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9193
[TakeutiZaring] p. 91Exercise 2alephle 10079
[TakeutiZaring] p. 91Exercise 3aleph0 10057
[TakeutiZaring] p. 91Exercise 4cardlim 9965
[TakeutiZaring] p. 91Exercise 7infpss 10206
[TakeutiZaring] p. 91Exercise 8infcntss 9280
[TakeutiZaring] p. 91Definition 10.29df-fin 8945  isfi 8970
[TakeutiZaring] p. 92Proposition 10.32onfin 9197
[TakeutiZaring] p. 92Proposition 10.34imadomg 10524
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9058
[TakeutiZaring] p. 93Proposition 10.35fodomb 10516
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10176  unxpdom 9217
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9967  cardsdomelir 9966
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9219
[TakeutiZaring] p. 94Proposition 10.39infxpen 10005
[TakeutiZaring] p. 95Definition 10.42df-map 8824
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10552  infxpidm2 10008
[TakeutiZaring] p. 95Proposition 10.41infdju 10197  infxp 10204
[TakeutiZaring] p. 96Proposition 10.44pw2en 9070  pw2f1o 9068
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9129
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10477
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10472  ac6s5 10481
[TakeutiZaring] p. 98Theorem 10.47unidom 10533
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10534  uniimadomf 10535
[TakeutiZaring] p. 100Definition 11.1cfcof 10264
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10259
[TakeutiZaring] p. 102Exercise 1cfle 10243
[TakeutiZaring] p. 102Exercise 2cf0 10240
[TakeutiZaring] p. 102Exercise 3cfsuc 10247
[TakeutiZaring] p. 102Exercise 4cfom 10254
[TakeutiZaring] p. 102Proposition 11.9coftr 10263
[TakeutiZaring] p. 103Theorem 11.15alephreg 10573
[TakeutiZaring] p. 103Proposition 11.11cardcf 10241
[TakeutiZaring] p. 103Proposition 11.13alephsing 10266
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10088
[TakeutiZaring] p. 104Proposition 11.16carduniima 10087
[TakeutiZaring] p. 104Proposition 11.18alephfp 10099  alephfp2 10100
[TakeutiZaring] p. 106Theorem 11.20gchina 10690
[TakeutiZaring] p. 106Theorem 11.21mappwen 10103
[TakeutiZaring] p. 107Theorem 11.26konigth 10560
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10574
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10575
[Tarski] p. 67Axiom B5ax-c5 39685
[Tarski] p. 67Scheme B5sp 2218
[Tarski] p. 68Lemma 6avril1 30825  equid 2041
[Tarski] p. 69Lemma 7equcomi 2046
[Tarski] p. 70Lemma 14spim 2418  spime 2420  spimew 2000
[Tarski] p. 70Lemma 16ax-12 2212  ax-c15 39691  ax12i 1995
[Tarski] p. 70Lemmas 16 and 17sb6 2118
[Tarski] p. 75Axiom B7ax6v 1997
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1939  ax5ALT 39709
[Tarski], p. 75Scheme B8 of system S2ax-7 2037  ax-8 2144  ax-9 2152
[Tarski1999] p. 178Axiom 4axtgsegcon 28744
[Tarski1999] p. 178Axiom 5axtg5seg 28745
[Tarski1999] p. 179Axiom 7axtgpasch 28747
[Tarski1999] p. 180Axiom 7.1axtgpasch 28747
[Tarski1999] p. 185Axiom 11axtgcont1 28748
[Truss] p. 114Theorem 5.18ruc 16305
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38338
[Viaclovsky8] p. 3Proposition 7ismblfin 38340
[Weierstrass] p. 272Definitiondf-mdet 22753  mdetuni 22790
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 916
[WhiteheadRussell] p. 96Axiom *1.3olc 881
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 882
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 932
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 982
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 190
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 136
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 91  wl-luk-pm2.04 38119
[WhiteheadRussell] p. 100Theorem *2.05frege5 44554  imim2 59  wl-luk-imim2 38114
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47784  imim1 84
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 909
[WhiteheadRussell] p. 101Theorem *2.06barbara 2689  syl 18
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 915
[WhiteheadRussell] p. 101Theorem *2.08id 23  wl-luk-id 38117
[WhiteheadRussell] p. 101Theorem *2.11exmid 907
[WhiteheadRussell] p. 101Theorem *2.12notnot 143
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 910
[WhiteheadRussell] p. 102Theorem *2.14notnotr 131  notnotrALT2 45663  wl-luk-notnotr 38118
[WhiteheadRussell] p. 102Theorem *2.15con1 147
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44584  axfrege28 44583  con3 154
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 129
[WhiteheadRussell] p. 104Theorem *2.2orc 880
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 937
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 124  wl-luk-pm2.21 38111
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 125
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 902
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 953
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30763  pm2.27 43  wl-luk-pm2.27 38109
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 935
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 39048
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 936
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 984
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 985
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 983
[WhiteheadRussell] p. 105Definition *2.33df-3or 1103
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 919
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 920
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 956
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 57
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 894
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 895
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 170  pm2.5g 169
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 193
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 896
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 897
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 898
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 173
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 174
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 864
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 865
[WhiteheadRussell] p. 107Theorem *2.55orel1 901
[WhiteheadRussell] p. 107Theorem *2.56orel2 903
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 194
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 912
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 954
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 955
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 195
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 904  pm2.67 905
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 177  pm2.521g 175  pm2.521g2 176
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 911
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 987
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 913
[WhiteheadRussell] p. 108Theorem *2.69looinv 206
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 988
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 989
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 946
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 944
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 986
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 990
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 85
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 945
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 110
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1006
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 474  pm3.2im 161
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1007
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1008
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1009
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1010
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 476
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 464
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 407
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 814
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 453
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 454
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 487  simplim 168
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 489  simprim 167
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 776
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 777
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 819
[WhiteheadRussell] p. 113Fact)pm3.45 633
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 821
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 497
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 498
[WhiteheadRussell] p. 113Theorem *3.44jao 974  pm3.44 973
[WhiteheadRussell] p. 113Theorem *3.47anim12 820
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 478
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 977
[WhiteheadRussell] p. 116Theorem *4.1con34b 319
[WhiteheadRussell] p. 117Theorem *4.2biid 264
[WhiteheadRussell] p. 117Theorem *4.11notbi 322
[WhiteheadRussell] p. 117Theorem *4.12con2bi 356
[WhiteheadRussell] p. 117Theorem *4.13notnotb 318
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 818
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 845
[WhiteheadRussell] p. 117Theorem *4.21bicom 225
[WhiteheadRussell] p. 117Theorem *4.22biantr 817  bitr 816
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 573
[WhiteheadRussell] p. 117Theorem *4.25oridm 917  pm4.25 918
[WhiteheadRussell] p. 118Theorem *4.3ancom 465
[WhiteheadRussell] p. 118Theorem *4.4andi 1024
[WhiteheadRussell] p. 118Theorem *4.31orcom 883
[WhiteheadRussell] p. 118Theorem *4.32anass 473
[WhiteheadRussell] p. 118Theorem *4.33orass 934
[WhiteheadRussell] p. 118Theorem *4.36anbi1 644
[WhiteheadRussell] p. 118Theorem *4.37orbi1 930
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 648
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 991
[WhiteheadRussell] p. 118Definition *4.34df-3an 1104
[WhiteheadRussell] p. 119Theorem *4.41ordi 1022
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1068
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1039
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1011
[WhiteheadRussell] p. 119Theorem *4.45orabs 1013  pm4.45 1012  pm4.45im 840
[WhiteheadRussell] p. 120Theorem *4.5anor 997
[WhiteheadRussell] p. 120Theorem *4.6imor 866
[WhiteheadRussell] p. 120Theorem *4.7anclb 554
[WhiteheadRussell] p. 120Theorem *4.51ianor 996
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 999
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 1000
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 1001
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 1002
[WhiteheadRussell] p. 120Theorem *4.56ioran 998  pm4.56 1003
[WhiteheadRussell] p. 120Theorem *4.57oran 1004  pm4.57 1005
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 409
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 869
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 402
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 862
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 410
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 863
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 403
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 566  pm4.71d 570  pm4.71i 568  pm4.71r 567  pm4.71rd 571  pm4.71ri 569
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 963
[WhiteheadRussell] p. 121Theorem *4.73iba 536
[WhiteheadRussell] p. 121Theorem *4.74biorf 949
[WhiteheadRussell] p. 121Theorem *4.76jcab 526  pm4.76 527
[WhiteheadRussell] p. 121Theorem *4.77jaob 975  pm4.77 976
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 947
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1020
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 397
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 398
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1040
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1041
[WhiteheadRussell] p. 122Theorem *4.84imbi1 350
[WhiteheadRussell] p. 122Theorem *4.85imbi2 351
[WhiteheadRussell] p. 122Theorem *4.86bibi1 354
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 391  impexp 455  pm4.87 856
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 835
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 958  pm5.11g 957
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 959
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 961
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 960
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1029
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1030
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1028
[WhiteheadRussell] p. 124Theorem *5.18nbbn 386  pm5.18 384
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 390
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 836
[WhiteheadRussell] p. 124Theorem *5.22xor 1031
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1064
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1065
[WhiteheadRussell] p. 124Theorem *5.25dfor2 914
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 582
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 392
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 364
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1016
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 967
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 843
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 583
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 848
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 837
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 846
[WhiteheadRussell] p. 125Theorem *5.41imdi 393  pm5.41 394
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 552
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 551
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1021
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1034
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 962
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1015
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1035
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1036
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1044
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 369
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 273
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1045
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 37242
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 45096
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 45097
[WhiteheadRussell] p. 147Theorem *10.2219.26 1899
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 45098
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 45099
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 45100
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1922
[WhiteheadRussell] p. 151Theorem *10.301albitr 45101
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 45102
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 45103
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 45104
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 45105
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 45107
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 45108
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 45109
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 45106
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2123
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 45112
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 45113
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2103
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2194
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1858
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1859
[WhiteheadRussell] p. 161Theorem *11.319.21vv 45114
[WhiteheadRussell] p. 162Theorem *11.322alim 45115
[WhiteheadRussell] p. 162Theorem *11.332albi 45116
[WhiteheadRussell] p. 162Theorem *11.342exim 45117
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 45119
[WhiteheadRussell] p. 162Theorem *11.3412exbi 45118
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1916
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 45121
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 45122
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 45120
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1857
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 45123
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 45124
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1875
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 45125
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2377
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1889
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 45130
[WhiteheadRussell] p. 165Theorem *11.56aaanv 45126
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 45127
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 45128
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 45129
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 45134
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 45131
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 45132
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 45133
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 45135
[WhiteheadRussell] p. 175Definition *14.02df-eu 2596
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 45145  pm13.13b 45146
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 45147
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3038
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3039
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3624
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 45153
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 45154
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 45148
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45289  pm13.193 45149
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 45150
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 45151
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 45152
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 45159
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 45158
[WhiteheadRussell] p. 184Definition *14.01iotasbc 45157
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3805
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 45160  pm14.122b 45161  pm14.122c 45162
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 45163  pm14.123b 45164  pm14.123c 45165
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 45167
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 45166
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 45168
[WhiteheadRussell] p. 190Theorem *14.22iota4 6517
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 45169
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6518
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 45170
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 45172
[WhiteheadRussell] p. 192Theorem *14.26eupick 2660  eupickbi 2663  sbaniota 45173
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 45171
[WhiteheadRussell] p. 192Theorem *14.271eubi 2611
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 45174
[WhiteheadRussell] p. 235Definition *30.01conventions 30762  df-fv 6544
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9994  pm54.43lem 9993
[Young] p. 141Definition of operator orderingleop2 32487
[Young] p. 142Example 12.2(i)0leop 32493  idleop 32494
[vandenDries] p. 42Lemma 61irrapx1 43583
[vandenDries] p. 43Theorem 62pellex 43590  pellexlem1 43584

This page was last updated on 16-Aug-2026.
Copyright terms: Public domain