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 17571
[Adamek] p. 21Condition 3.1(b)df-cat 17571
[Adamek] p. 22Example 3.3(1)df-setc 17980
[Adamek] p. 24Example 3.3(4.c)0cat 17592  0funcg 49116  df-termc 49504
[Adamek] p. 24Example 3.3(4.d)df-prstc 49581  prsthinc 49495
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49609  df-mndtc 49609
[Adamek] p. 24Example 3.3(4)(c)discsnterm 49605
[Adamek] p. 25Definition 3.5df-oppc 17615
[Adamek] p. 25Example 3.6(1)oduoppcciso 49597
[Adamek] p. 25Example 3.6(2)oppgoppcco 49622  oppgoppchom 49621  oppgoppcid 49623
[Adamek] p. 28Remark 3.9oppciso 17685
[Adamek] p. 28Remark 3.12invf1o 17673  invisoinvl 17694
[Adamek] p. 28Example 3.13idinv 17693  idiso 17692
[Adamek] p. 28Corollary 3.11inveq 17678
[Adamek] p. 28Definition 3.8df-inv 17652  df-iso 17653  dfiso2 17676
[Adamek] p. 28Proposition 3.10sectcan 17659
[Adamek] p. 29Remark 3.16cicer 17710  cicerALT 49077
[Adamek] p. 29Definition 3.15cic 17703  df-cic 17700
[Adamek] p. 29Definition 3.17df-func 17762
[Adamek] p. 29Proposition 3.14(1)invinv 17674
[Adamek] p. 29Proposition 3.14(2)invco 17675  isoco 17681
[Adamek] p. 30Remark 3.19df-func 17762
[Adamek] p. 30Example 3.20(1)idfucl 17785
[Adamek] p. 30Example 3.20(2)diag1 49335
[Adamek] p. 32Proposition 3.21funciso 17778
[Adamek] p. 33Example 3.26(1)discsnterm 49605  discthing 49492
[Adamek] p. 33Example 3.26(2)df-thinc 49449  prsthinc 49495  thincciso 49484  thincciso2 49486  thincciso3 49487  thinccisod 49485
[Adamek] p. 33Example 3.26(3)df-mndtc 49609
[Adamek] p. 33Proposition 3.23cofucl 17792  cofucla 49127
[Adamek] p. 34Remark 3.28(1)cofidfth 49193
[Adamek] p. 34Remark 3.28(2)catciso 18015  catcisoi 49431
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18070
[Adamek] p. 34Definition 3.27(2)df-fth 17811
[Adamek] p. 34Definition 3.27(3)df-full 17810
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18070
[Adamek] p. 35Corollary 3.32ffthiso 17835
[Adamek] p. 35Proposition 3.30(c)cofth 17841
[Adamek] p. 35Proposition 3.30(d)cofull 17840
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18055
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18055
[Adamek] p. 39Remark 3.422oppf 49163
[Adamek] p. 39Definition 3.41df-oppf 49154  funcoppc 17779
[Adamek] p. 39Definition 3.44.df-catc 18003  elcatchom 49428
[Adamek] p. 39Proposition 3.43(c)fthoppc 17829  fthoppf 49195
[Adamek] p. 39Proposition 3.43(d)fulloppc 17828  fulloppf 49194
[Adamek] p. 40Remark 3.48catccat 18012
[Adamek] p. 40Definition 3.470funcg 49116  df-catc 18003
[Adamek] p. 45Exercise 3Gincat 49632
[Adamek] p. 48Remark 4.2(2)cnelsubc 49635  nelsubc3 49102
[Adamek] p. 48Remark 4.2(3)imasubc 49182  imasubc2 49183  imasubc3 49187
[Adamek] p. 48Example 4.3(1.a)0subcat 17742
[Adamek] p. 48Example 4.3(1.b)catsubcat 17743
[Adamek] p. 48Definition 4.1(1)nelsubc3 49102
[Adamek] p. 48Definition 4.1(2)fullsubc 17754
[Adamek] p. 48Definition 4.1(a)df-subc 17716
[Adamek] p. 49Remark 4.4idsubc 49191
[Adamek] p. 49Remark 4.4(1)idemb 49190
[Adamek] p. 49Remark 4.4(2)idfullsubc 49192  ressffth 17844
[Adamek] p. 58Exercise 4Asetc1onsubc 49633
[Adamek] p. 83Definition 6.1df-nat 17850
[Adamek] p. 87Remark 6.14(a)fuccocl 17871
[Adamek] p. 87Remark 6.14(b)fucass 17875
[Adamek] p. 87Definition 6.15df-fuc 17851
[Adamek] p. 88Remark 6.16fuccat 17877
[Adamek] p. 101Definition 7.10funcg 49116  df-inito 17888
[Adamek] p. 101Example 7.2(3)0funcg 49116  df-termc 49504  initc 49122
[Adamek] p. 101Example 7.2 (6)irinitoringc 21414
[Adamek] p. 102Definition 7.4df-termo 17889  oppctermo 49267
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17916
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17920
[Adamek] p. 103Remark 7.8oppczeroo 49268
[Adamek] p. 103Definition 7.7df-zeroo 17890
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21415
[Adamek] p. 103Proposition 7.6termoeu1w 17923
[Adamek] p. 106Definition 7.19df-sect 17651
[Adamek] p. 107Example 7.20(7)thincinv 49500
[Adamek] p. 108Example 7.25(4)thincsect2 49499
[Adamek] p. 110Example 7.33(9)thincmon 49464
[Adamek] p. 110Proposition 7.35sectmon 17686
[Adamek] p. 112Proposition 7.42sectepi 17688
[Adamek] p. 185Section 10.67updjud 9824
[Adamek] p. 193Definition 11.1(1)df-lmd 49676
[Adamek] p. 193Definition 11.3(1)df-lmd 49676
[Adamek] p. 194Definition 11.3(2)df-lmd 49676
[Adamek] p. 202Definition 11.27(1)df-cmd 49677
[Adamek] p. 202Definition 11.27(2)df-cmd 49677
[Adamek] p. 478Item Rngdf-ringc 20559
[AhoHopUll] p. 2Section 1.1df-bigo 48579
[AhoHopUll] p. 12Section 1.3df-blen 48601
[AhoHopUll] p. 318Section 9.1df-concat 14475  df-pfx 14576  df-substr 14546  df-word 14418  lencl 14437  wrd0 14443
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24621  df-nmoo 30720
[AkhiezerGlazman] p. 64Theoremhmopidmch 32128  hmopidmchi 32126
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32176  pjcmul2i 32177
[AkhiezerGlazman] p. 72Theoremcnvunop 31893  unoplin 31895
[AkhiezerGlazman] p. 72Equation 2unopadj 31894  unopadj2 31913
[AkhiezerGlazman] p. 73Theoremelunop2 31988  lnopunii 31987
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32061
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27869
[Alling] p. 184Axiom Bbdayfo 27614
[Alling] p. 184Axiom Osltso 27613
[Alling] p. 184Axiom SDnodense 27629
[Alling] p. 185Lemma 0nocvxmin 27716
[Alling] p. 185Theoremconway 27738
[Alling] p. 185Axiom FEnoeta 27680
[Alling] p. 186Theorem 4slerec 27758  slerecd 27759
[Alling], p. 2Definitionrp-brsslt 43455
[Alling], p. 3Notenla0001 43458  nla0002 43456  nla0003 43457
[Apostol] p. 18Theorem I.1addcan 11294  addcan2d 11314  addcan2i 11304  addcand 11313  addcani 11303
[Apostol] p. 18Theorem I.2negeu 11347
[Apostol] p. 18Theorem I.3negsub 11406  negsubd 11475  negsubi 11436
[Apostol] p. 18Theorem I.4negneg 11408  negnegd 11460  negnegi 11428
[Apostol] p. 18Theorem I.5subdi 11547  subdid 11570  subdii 11563  subdir 11548  subdird 11571  subdiri 11564
[Apostol] p. 18Theorem I.6mul01 11289  mul01d 11309  mul01i 11300  mul02 11288  mul02d 11308  mul02i 11299
[Apostol] p. 18Theorem I.7mulcan 11751  mulcan2d 11748  mulcand 11747  mulcani 11753
[Apostol] p. 18Theorem I.8receu 11759  xreceu 32897
[Apostol] p. 18Theorem I.9divrec 11789  divrecd 11897  divreci 11863  divreczi 11856
[Apostol] p. 18Theorem I.10recrec 11815  recreci 11850
[Apostol] p. 18Theorem I.11mul0or 11754  mul0ord 11762  mul0ori 11761
[Apostol] p. 18Theorem I.12mul2neg 11553  mul2negd 11569  mul2negi 11562  mulneg1 11550  mulneg1d 11567  mulneg1i 11560
[Apostol] p. 18Theorem I.13divadddiv 11833  divadddivd 11938  divadddivi 11880
[Apostol] p. 18Theorem I.14divmuldiv 11818  divmuldivd 11935  divmuldivi 11878  rdivmuldivd 20329
[Apostol] p. 18Theorem I.15divdivdiv 11819  divdivdivd 11941  divdivdivi 11881
[Apostol] p. 20Axiom 7rpaddcl 12911  rpaddcld 12946  rpmulcl 12912  rpmulcld 12947
[Apostol] p. 20Axiom 8rpneg 12921
[Apostol] p. 20Axiom 90nrp 12924
[Apostol] p. 20Theorem I.17lttri 11236
[Apostol] p. 20Theorem I.18ltadd1d 11707  ltadd1dd 11725  ltadd1i 11668
[Apostol] p. 20Theorem I.19ltmul1 11968  ltmul1a 11967  ltmul1i 12037  ltmul1ii 12047  ltmul2 11969  ltmul2d 12973  ltmul2dd 12987  ltmul2i 12040
[Apostol] p. 20Theorem I.20msqgt0 11634  msqgt0d 11681  msqgt0i 11651
[Apostol] p. 20Theorem I.210lt1 11636
[Apostol] p. 20Theorem I.23lt0neg1 11620  lt0neg1d 11683  ltneg 11614  ltnegd 11692  ltnegi 11658
[Apostol] p. 20Theorem I.25lt2add 11599  lt2addd 11737  lt2addi 11676
[Apostol] p. 20Definition of positive numbersdf-rp 12888
[Apostol] p. 21Exercise 4recgt0 11964  recgt0d 12053  recgt0i 12024  recgt0ii 12025
[Apostol] p. 22Definition of integersdf-z 12466
[Apostol] p. 22Definition of positive integersdfnn3 12136
[Apostol] p. 22Definition of rationalsdf-q 12844
[Apostol] p. 24Theorem I.26supeu 9338
[Apostol] p. 26Theorem I.28nnunb 12374
[Apostol] p. 26Theorem I.29arch 12375  archd 45198
[Apostol] p. 28Exercise 2btwnz 12573
[Apostol] p. 28Exercise 3nnrecl 12376
[Apostol] p. 28Exercise 4rebtwnz 12842
[Apostol] p. 28Exercise 5zbtwnre 12841
[Apostol] p. 28Exercise 6qbtwnre 13095
[Apostol] p. 28Exercise 10(a)zeneo 16247  zneo 12553  zneoALTV 47699
[Apostol] p. 29Theorem I.35cxpsqrtth 26664  msqsqrtd 15347  resqrtth 15159  sqrtth 15269  sqrtthi 15275  sqsqrtd 15346
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12125
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12808
[Apostol] p. 361Remarkcrreczi 14132
[Apostol] p. 363Remarkabsgt0i 15304
[Apostol] p. 363Exampleabssubd 15360  abssubi 15308
[ApostolNT] p. 7Remarkfmtno0 47570  fmtno1 47571  fmtno2 47580  fmtno3 47581  fmtno4 47582  fmtno5fac 47612  fmtnofz04prm 47607
[ApostolNT] p. 7Definitiondf-fmtno 47558
[ApostolNT] p. 8Definitiondf-ppi 27035
[ApostolNT] p. 14Definitiondf-dvds 16161
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16177
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16202
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16197
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16190
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16192
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16178
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16179
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16184
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16219
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16221
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16223
[ApostolNT] p. 15Definitiondf-gcd 16403  dfgcd2 16454
[ApostolNT] p. 16Definitionisprm2 16590
[ApostolNT] p. 16Theorem 1.5coprmdvds 16561
[ApostolNT] p. 16Theorem 1.7prminf 16824
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16421
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16455
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16457
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16436
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16428
[ApostolNT] p. 17Theorem 1.8coprm 16619
[ApostolNT] p. 17Theorem 1.9euclemma 16621
[ApostolNT] p. 17Theorem 1.101arith2 16837
[ApostolNT] p. 18Theorem 1.13prmrec 16831
[ApostolNT] p. 19Theorem 1.14divalg 16311
[ApostolNT] p. 20Theorem 1.15eucalg 16495
[ApostolNT] p. 24Definitiondf-mu 27036
[ApostolNT] p. 25Definitiondf-phi 16674
[ApostolNT] p. 25Theorem 2.1musum 27126
[ApostolNT] p. 26Theorem 2.2phisum 16699
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16684
[ApostolNT] p. 28Theorem 2.5(c)phimul 16688
[ApostolNT] p. 32Definitiondf-vma 27033
[ApostolNT] p. 32Theorem 2.9muinv 27128
[ApostolNT] p. 32Theorem 2.10vmasum 27152
[ApostolNT] p. 38Remarkdf-sgm 27037
[ApostolNT] p. 38Definitiondf-sgm 27037
[ApostolNT] p. 75Definitiondf-chp 27034  df-cht 27032
[ApostolNT] p. 104Definitioncongr 16572
[ApostolNT] p. 106Remarkdvdsval3 16164
[ApostolNT] p. 106Definitionmoddvds 16171
[ApostolNT] p. 107Example 2mod2eq0even 16254
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16255
[ApostolNT] p. 107Example 4zmod1congr 13789
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13829
[ApostolNT] p. 107Theorem 5.2(c)modexp 14142
[ApostolNT] p. 108Theorem 5.3modmulconst 16196
[ApostolNT] p. 109Theorem 5.4cncongr1 16575
[ApostolNT] p. 109Theorem 5.6gcdmodi 16983
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16577
[ApostolNT] p. 113Theorem 5.17eulerth 16691
[ApostolNT] p. 113Theorem 5.18vfermltl 16710
[ApostolNT] p. 114Theorem 5.19fermltl 16692
[ApostolNT] p. 116Theorem 5.24wilthimp 27007
[ApostolNT] p. 179Definitiondf-lgs 27231  lgsprme0 27275
[ApostolNT] p. 180Example 11lgs 27276
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27252
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27267
[ApostolNT] p. 181Theorem 9.4m1lgs 27324
[ApostolNT] p. 181Theorem 9.52lgs 27343  2lgsoddprm 27352
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27310
[ApostolNT] p. 185Theorem 9.8lgsquad 27319
[ApostolNT] p. 188Definitiondf-lgs 27231  lgs1 27277
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27268
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27270
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27278
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27279
[Baer] p. 40Property (b)mapdord 41676
[Baer] p. 40Property (c)mapd11 41677
[Baer] p. 40Property (e)mapdin 41700  mapdlsm 41702
[Baer] p. 40Property (f)mapd0 41703
[Baer] p. 40Definition of projectivitydf-mapd 41663  mapd1o 41686
[Baer] p. 41Property (g)mapdat 41705
[Baer] p. 44Part (1)mapdpg 41744
[Baer] p. 45Part (2)hdmap1eq 41839  mapdheq 41766  mapdheq2 41767  mapdheq2biN 41768
[Baer] p. 45Part (3)baerlem3 41751
[Baer] p. 46Part (4)mapdheq4 41770  mapdheq4lem 41769
[Baer] p. 46Part (5)baerlem5a 41752  baerlem5abmN 41756  baerlem5amN 41754  baerlem5b 41753  baerlem5bmN 41755
[Baer] p. 47Part (6)hdmap1l6 41859  hdmap1l6a 41847  hdmap1l6e 41852  hdmap1l6f 41853  hdmap1l6g 41854  hdmap1l6lem1 41845  hdmap1l6lem2 41846  mapdh6N 41785  mapdh6aN 41773  mapdh6eN 41778  mapdh6fN 41779  mapdh6gN 41780  mapdh6lem1N 41771  mapdh6lem2N 41772
[Baer] p. 48Part 9hdmapval 41866
[Baer] p. 48Part 10hdmap10 41878
[Baer] p. 48Part 11hdmapadd 41881
[Baer] p. 48Part (6)hdmap1l6h 41855  mapdh6hN 41781
[Baer] p. 48Part (7)mapdh75cN 41791  mapdh75d 41792  mapdh75e 41790  mapdh75fN 41793  mapdh7cN 41787  mapdh7dN 41788  mapdh7eN 41786  mapdh7fN 41789
[Baer] p. 48Part (8)mapdh8 41826  mapdh8a 41813  mapdh8aa 41814  mapdh8ab 41815  mapdh8ac 41816  mapdh8ad 41817  mapdh8b 41818  mapdh8c 41819  mapdh8d 41821  mapdh8d0N 41820  mapdh8e 41822  mapdh8g 41823  mapdh8i 41824  mapdh8j 41825
[Baer] p. 48Part (9)mapdh9a 41827
[Baer] p. 48Equation 10mapdhvmap 41807
[Baer] p. 49Part 12hdmap11 41886  hdmapeq0 41882  hdmapf1oN 41903  hdmapneg 41884  hdmaprnN 41902  hdmaprnlem1N 41887  hdmaprnlem3N 41888  hdmaprnlem3uN 41889  hdmaprnlem4N 41891  hdmaprnlem6N 41892  hdmaprnlem7N 41893  hdmaprnlem8N 41894  hdmaprnlem9N 41895  hdmapsub 41885
[Baer] p. 49Part 14hdmap14lem1 41906  hdmap14lem10 41915  hdmap14lem1a 41904  hdmap14lem2N 41907  hdmap14lem2a 41905  hdmap14lem3 41908  hdmap14lem8 41913  hdmap14lem9 41914
[Baer] p. 50Part 14hdmap14lem11 41916  hdmap14lem12 41917  hdmap14lem13 41918  hdmap14lem14 41919  hdmap14lem15 41920  hgmapval 41925
[Baer] p. 50Part 15hgmapadd 41932  hgmapmul 41933  hgmaprnlem2N 41935  hgmapvs 41929
[Baer] p. 50Part 16hgmaprnN 41939
[Baer] p. 110Lemma 1hdmapip0com 41955
[Baer] p. 110Line 27hdmapinvlem1 41956
[Baer] p. 110Line 28hdmapinvlem2 41957
[Baer] p. 110Line 30hdmapinvlem3 41958
[Baer] p. 110Part 1.2hdmapglem5 41960  hgmapvv 41964
[Baer] p. 110Proposition 1hdmapinvlem4 41959
[Baer] p. 111Line 10hgmapvvlem1 41961
[Baer] p. 111Line 15hdmapg 41968  hdmapglem7 41967
[Bauer], p. 483Theorem 1.22irrexpq 26665  2irrexpqALT 26735
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2564
[BellMachover] p. 460Notationdf-mo 2535
[BellMachover] p. 460Definitionmo3 2559
[BellMachover] p. 461Axiom Extax-ext 2703
[BellMachover] p. 462Theorem 1.1axextmo 2707
[BellMachover] p. 463Axiom Repaxrep5 5225
[BellMachover] p. 463Scheme Sepax-sep 5234
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37097  sepex 5238
[BellMachover] p. 466Problemaxpow2 5305
[BellMachover] p. 466Axiom Powaxpow3 5306
[BellMachover] p. 466Axiom Unionaxun2 7670
[BellMachover] p. 468Definitiondf-ord 6309
[BellMachover] p. 469Theorem 2.2(i)ordirr 6324
[BellMachover] p. 469Theorem 2.2(iii)onelon 6331
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6326
[BellMachover] p. 471Definition of Ndf-om 7797
[BellMachover] p. 471Problem 2.5(ii)uniordint 7734
[BellMachover] p. 471Definition of Limdf-lim 6311
[BellMachover] p. 472Axiom Infzfinf2 9532
[BellMachover] p. 473Theorem 2.8limom 7812
[BellMachover] p. 477Equation 3.1df-r1 9654
[BellMachover] p. 478Definitionrankval2 9708  rankval2b 35103
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9672  r1ord3g 9669
[BellMachover] p. 480Axiom Regzfreg 9482
[BellMachover] p. 488Axiom ACac5 10365  dfac4 10010
[BellMachover] p. 490Definition of alephalephval3 9998
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39357
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32328
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32370  chirredi 32369
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32358
[Beran] p. 3Definition of joinsshjval3 31329
[Beran] p. 39Theorem 2.3(i)cmcm2 31591  cmcm2i 31568  cmcm2ii 31573  cmt2N 39288
[Beran] p. 40Theorem 2.3(iii)lecm 31592  lecmi 31577  lecmii 31578
[Beran] p. 45Theorem 3.4cmcmlem 31566
[Beran] p. 49Theorem 4.2cm2j 31595  cm2ji 31600  cm2mi 31601
[Beran] p. 95Definitiondf-sh 31182  issh2 31184
[Beran] p. 95Lemma 3.1(S5)his5 31061
[Beran] p. 95Lemma 3.1(S6)his6 31074
[Beran] p. 95Lemma 3.1(S7)his7 31065
[Beran] p. 95Lemma 3.2(S8)ho01i 31803
[Beran] p. 95Lemma 3.2(S9)hoeq1 31805
[Beran] p. 95Lemma 3.2(S10)ho02i 31804
[Beran] p. 95Lemma 3.2(S11)hoeq2 31806
[Beran] p. 95Postulate (S1)ax-his1 31057  his1i 31075
[Beran] p. 95Postulate (S2)ax-his2 31058
[Beran] p. 95Postulate (S3)ax-his3 31059
[Beran] p. 95Postulate (S4)ax-his4 31060
[Beran] p. 96Definition of normdf-hnorm 30943  dfhnorm2 31097  normval 31099
[Beran] p. 96Definition for Cauchy sequencehcau 31159
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30948
[Beran] p. 96Definition of complete subspaceisch3 31216
[Beran] p. 96Definition of convergedf-hlim 30947  hlimi 31163
[Beran] p. 97Theorem 3.3(i)norm-i-i 31108  norm-i 31104
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31112  norm-ii 31113  normlem0 31084  normlem1 31085  normlem2 31086  normlem3 31087  normlem4 31088  normlem5 31089  normlem6 31090  normlem7 31091  normlem7tALT 31094
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31114  norm-iii 31115
[Beran] p. 98Remark 3.4bcs 31156  bcsiALT 31154  bcsiHIL 31155
[Beran] p. 98Remark 3.4(B)normlem9at 31096  normpar 31130  normpari 31129
[Beran] p. 98Remark 3.4(C)normpyc 31121  normpyth 31120  normpythi 31117
[Beran] p. 99Remarklnfn0 32022  lnfn0i 32017  lnop0 31941  lnop0i 31945
[Beran] p. 99Theorem 3.5(i)nmcexi 32001  nmcfnex 32028  nmcfnexi 32026  nmcopex 32004  nmcopexi 32002
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32029  nmcfnlbi 32027  nmcoplb 32005  nmcoplbi 32003
[Beran] p. 99Theorem 3.5(iii)lnfncon 32031  lnfnconi 32030  lnopcon 32010  lnopconi 32009
[Beran] p. 100Lemma 3.6normpar2i 31131
[Beran] p. 101Lemma 3.6norm3adifi 31128  norm3adifii 31123  norm3dif 31125  norm3difi 31122
[Beran] p. 102Theorem 3.7(i)chocunii 31276  pjhth 31368  pjhtheu 31369  pjpjhth 31400  pjpjhthi 31401  pjth 25364
[Beran] p. 102Theorem 3.7(ii)ococ 31381  ococi 31380
[Beran] p. 103Remark 3.8nlelchi 32036
[Beran] p. 104Theorem 3.9riesz3i 32037  riesz4 32039  riesz4i 32038
[Beran] p. 104Theorem 3.10cnlnadj 32054  cnlnadjeu 32053  cnlnadjeui 32052  cnlnadji 32051  cnlnadjlem1 32042  nmopadjlei 32063
[Beran] p. 106Theorem 3.11(i)adjeq0 32066
[Beran] p. 106Theorem 3.11(v)nmopadji 32065
[Beran] p. 106Theorem 3.11(ii)adjmul 32067
[Beran] p. 106Theorem 3.11(iv)adjadj 31911
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32077  nmopcoadji 32076
[Beran] p. 106Theorem 3.11(iii)adjadd 32068
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32078
[Beran] p. 106Theorem 3.11(viii)adjcoi 32075  pjadj2coi 32179  pjadjcoi 32136
[Beran] p. 107Definitiondf-ch 31196  isch2 31198
[Beran] p. 107Remark 3.12choccl 31281  isch3 31216  occl 31279  ocsh 31258  shoccl 31280  shocsh 31259
[Beran] p. 107Remark 3.12(B)ococin 31383
[Beran] p. 108Theorem 3.13chintcl 31307
[Beran] p. 109Property (i)pjadj2 32162  pjadj3 32163  pjadji 31660  pjadjii 31649
[Beran] p. 109Property (ii)pjidmco 32156  pjidmcoi 32152  pjidmi 31648
[Beran] p. 110Definition of projector orderingpjordi 32148
[Beran] p. 111Remarkho0val 31725  pjch1 31645
[Beran] p. 111Definitiondf-hfmul 31709  df-hfsum 31708  df-hodif 31707  df-homul 31706  df-hosum 31705
[Beran] p. 111Lemma 4.4(i)pjo 31646
[Beran] p. 111Lemma 4.4(ii)pjch 31669  pjchi 31407
[Beran] p. 111Lemma 4.4(iii)pjoc2 31414  pjoc2i 31413
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31655
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32140  pjssmii 31656
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32139
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32138
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32143
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32141  pjssge0ii 31657
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32142  pjdifnormii 31658
[Bobzien] p. 116Statement T3stoic3 1777
[Bobzien] p. 117Statement T2stoic2a 1775
[Bobzien] p. 117Statement T4stoic4a 1778
[Bobzien] p. 117Conclusion the contradictorystoic1a 1773
[Bogachev] p. 16Definition 1.5df-oms 34300
[Bogachev] p. 17Lemma 1.5.4omssubadd 34308
[Bogachev] p. 17Example 1.5.2omsmon 34306
[Bogachev] p. 41Definition 1.11.2df-carsg 34310
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34330
[Bogachev] p. 116Definition 2.3.1df-itgm 34361  df-sitm 34339
[Bogachev] p. 118Chapter 2.4.4df-itgm 34361
[Bogachev] p. 118Definition 2.4.1df-sitg 34338
[Bollobas] p. 1Section I.1df-edg 29024  isuhgrop 29046  isusgrop 29138  isuspgrop 29137
[Bollobas] p. 2Section I.1df-isubgr 47891  df-subgr 29244  uhgrspan1 29279  uhgrspansubgr 29267
[Bollobas] p. 3Definitiondf-gric 47911  gricuspgr 47948  isuspgrim 47926
[Bollobas] p. 3Section I.1cusgrsize 29431  df-clnbgr 47849  df-cusgr 29388  df-nbgr 29309  fusgrmaxsize 29441
[Bollobas] p. 4Definitiondf-upwlks 48164  df-wlks 29576
[Bollobas] p. 4Section I.1finsumvtxdg2size 29527  finsumvtxdgeven 29529  fusgr1th 29528  fusgrvtxdgonume 29531  vtxdgoddnumeven 29530
[Bollobas] p. 5Notationdf-pths 29690
[Bollobas] p. 5Definitiondf-crcts 29762  df-cycls 29763  df-trls 29667  df-wlkson 29577
[Bollobas] p. 7Section I.1df-ushgr 29035
[BourbakiAlg1] p. 1Definition 1df-clintop 48230  df-cllaw 48216  df-mgm 18545  df-mgm2 48249
[BourbakiAlg1] p. 4Definition 5df-assintop 48231  df-asslaw 48218  df-sgrp 18624  df-sgrp2 48251
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48250  df-comlaw 48217
[BourbakiAlg1] p. 12Definition 2df-mnd 18640
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33002  mndlactf1o 33006  mndractf1 33004  mndractf1o 33007
[BourbakiAlg1] p. 92Definition 1df-ring 20151
[BourbakiAlg1] p. 93Section I.8.1df-rng 20069
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33641
[BourbakiAlg2] p. 113Chapter 5.assafld 33645  assarrginv 33644
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33686  fldextrspunfld 33684  fldextrspunlem1 33683  fldextrspunlem2 33685  fldextrspunlsp 33682  fldextrspunlsplem 33681
[BourbakiCAlg2], p. 228Proposition 21arithidom 33497  dfufd2 33510
[BourbakiEns] p. Proposition 8fcof1 7221  fcofo 7222
[BourbakiTop1] p. Remarkxnegmnf 13106  xnegpnf 13105
[BourbakiTop1] p. Remark rexneg 13107
[BourbakiTop1] p. Remark 3ust0 24133  ustfilxp 24126
[BourbakiTop1] p. Axiom GT'tgpsubcn 24003
[BourbakiTop1] p. Criterionishmeo 23672
[BourbakiTop1] p. Example 1cstucnd 24196  iducn 24195  snfil 23777
[BourbakiTop1] p. Example 2neifil 23793
[BourbakiTop1] p. Theorem 1cnextcn 23980
[BourbakiTop1] p. Theorem 2ucnextcn 24216
[BourbakiTop1] p. Theorem 3df-hcmp 33965
[BourbakiTop1] p. Paragraph 3infil 23776
[BourbakiTop1] p. Definition 1df-ucn 24188  df-ust 24114  filintn0 23774  filn0 23775  istgp 23990  ucnprima 24194
[BourbakiTop1] p. Definition 2df-cfilu 24199
[BourbakiTop1] p. Definition 3df-cusp 24210  df-usp 24170  df-utop 24144  trust 24142
[BourbakiTop1] p. Definition 6df-pcmp 33864
[BourbakiTop1] p. Property V_issnei2 23029
[BourbakiTop1] p. Theorem 1(d)iscncl 23182
[BourbakiTop1] p. Condition F_Iustssel 24119
[BourbakiTop1] p. Condition U_Iustdiag 24122
[BourbakiTop1] p. Property V_iiinnei 23038
[BourbakiTop1] p. Property V_ivneiptopreu 23046  neissex 23040
[BourbakiTop1] p. Proposition 1neips 23026  neiss 23022  ucncn 24197  ustund 24135  ustuqtop 24159
[BourbakiTop1] p. Proposition 2cnpco 23180  neiptopreu 23046  utop2nei 24163  utop3cls 24164
[BourbakiTop1] p. Proposition 3fmucnd 24204  uspreg 24186  utopreg 24165
[BourbakiTop1] p. Proposition 4imasncld 23604  imasncls 23605  imasnopn 23603
[BourbakiTop1] p. Proposition 9cnpflf2 23913
[BourbakiTop1] p. Condition F_IIustincl 24121
[BourbakiTop1] p. Condition U_IIustinvel 24123
[BourbakiTop1] p. Property V_iiielnei 23024
[BourbakiTop1] p. Proposition 11cnextucn 24215
[BourbakiTop1] p. Condition F_IIbustbasel 24120
[BourbakiTop1] p. Condition U_IIIustexhalf 24124
[BourbakiTop1] p. Definition C'''df-cmp 23300
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23759
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22807
[BourbakiTop2] p. 195Definition 1df-ldlf 33861
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46099
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46101  stoweid 46100
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46038  stoweidlem10 46047  stoweidlem14 46051  stoweidlem15 46052  stoweidlem35 46072  stoweidlem36 46073  stoweidlem37 46074  stoweidlem38 46075  stoweidlem40 46077  stoweidlem41 46078  stoweidlem43 46080  stoweidlem44 46081  stoweidlem46 46083  stoweidlem5 46042  stoweidlem50 46087  stoweidlem52 46089  stoweidlem53 46090  stoweidlem55 46092  stoweidlem56 46093
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46060  stoweidlem24 46061  stoweidlem27 46064  stoweidlem28 46065  stoweidlem30 46067
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46071  stoweidlem59 46096  stoweidlem60 46097
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46082  stoweidlem49 46086  stoweidlem7 46044
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46068  stoweidlem39 46076  stoweidlem42 46079  stoweidlem48 46085  stoweidlem51 46088  stoweidlem54 46091  stoweidlem57 46094  stoweidlem58 46095
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46062
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46054
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46048  stoweidlem13 46050  stoweidlem26 46063  stoweidlem61 46098
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46055
[Bruck] p. 1Section I.1df-clintop 48230  df-mgm 18545  df-mgm2 48249
[Bruck] p. 23Section II.1df-sgrp 18624  df-sgrp2 48251
[Bruck] p. 28Theorem 3.2dfgrp3 18949
[ChoquetDD] p. 2Definition of mappingdf-mpt 5173
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 30378
[Clemente] p. 10Definition I` `m,nnatded 30378
[Clemente] p. 11Definition E=>m,nnatded 30378
[Clemente] p. 11Definition I=>m,nnatded 30378
[Clemente] p. 11Definition E` `(1)natded 30378
[Clemente] p. 11Definition E` `(2)natded 30378
[Clemente] p. 12Definition E` `m,n,pnatded 30378
[Clemente] p. 12Definition I` `n(1)natded 30378
[Clemente] p. 12Definition I` `n(2)natded 30378
[Clemente] p. 13Definition I` `m,n,pnatded 30378
[Clemente] p. 14Proof 5.11natded 30378
[Clemente] p. 14Definition E` `nnatded 30378
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30380  ex-natded5.2 30379
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30383  ex-natded5.3 30382
[Clemente] p. 18Theorem 5.5ex-natded5.5 30385
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30387  ex-natded5.7 30386
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30389  ex-natded5.8 30388
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30391  ex-natded5.13 30390
[Clemente] p. 32Definition I` `nnatded 30378
[Clemente] p. 32Definition E` `m,n,p,anatded 30378
[Clemente] p. 32Definition E` `n,tnatded 30378
[Clemente] p. 32Definition I` `n,tnatded 30378
[Clemente] p. 43Theorem 9.20ex-natded9.20 30392
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30393
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30395  ex-natded9.26 30394
[Cohen] p. 301Remarkrelogoprlem 26525
[Cohen] p. 301Property 2relogmul 26526  relogmuld 26559
[Cohen] p. 301Property 3relogdiv 26527  relogdivd 26560
[Cohen] p. 301Property 4relogexp 26530
[Cohen] p. 301Property 1alog1 26519
[Cohen] p. 301Property 1bloge 26520
[Cohen4] p. 348Observationrelogbcxpb 26722
[Cohen4] p. 349Propertyrelogbf 26726
[Cohen4] p. 352Definitionelogb 26705
[Cohen4] p. 361Property 2relogbmul 26712
[Cohen4] p. 361Property 3logbrec 26717  relogbdiv 26714
[Cohen4] p. 361Property 4relogbreexp 26710
[Cohen4] p. 361Property 6relogbexp 26715
[Cohen4] p. 361Property 1(a)logbid1 26703
[Cohen4] p. 361Property 1(b)logb1 26704
[Cohen4] p. 367Propertylogbchbase 26706
[Cohen4] p. 377Property 2logblt 26719
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34293  sxbrsigalem4 34295
[Cohn] p. 81Section II.5acsdomd 18460  acsinfd 18459  acsinfdimd 18461  acsmap2d 18458  acsmapd 18457
[Cohn] p. 143Example 5.1.1sxbrsiga 34298
[Connell] p. 57Definitiondf-scmat 22404  df-scmatalt 48430
[Conway] p. 4Definitionslerec 27758  slerecd 27759
[Conway] p. 5Definitionaddsval 27903  addsval2 27904  df-adds 27901  df-muls 28044  df-negs 27961
[Conway] p. 7Theorem0slt1s 27771
[Conway] p. 12Theorem 12pw2cut2 28380
[Conway] p. 16Theorem 0(i)ssltright 27814
[Conway] p. 16Theorem 0(ii)ssltleft 27813
[Conway] p. 16Theorem 0(iii)slerflex 27700
[Conway] p. 17Theorem 3addsass 27946  addsassd 27947  addscom 27907  addscomd 27908  addsrid 27905  addsridd 27906
[Conway] p. 17Definitiondf-0s 27766
[Conway] p. 17Theorem 4(ii)negnegs 27984
[Conway] p. 17Theorem 4(iii)negsid 27981  negsidd 27982
[Conway] p. 18Theorem 5sleadd1 27930  sleadd1d 27936
[Conway] p. 18Definitiondf-1s 27767
[Conway] p. 18Theorem 6(ii)negscl 27976  negscld 27977
[Conway] p. 18Theorem 6(iii)addscld 27921
[Conway] p. 19Notemulsunif2 28107
[Conway] p. 19Theorem 7addsdi 28092  addsdid 28093  addsdird 28094  mulnegs1d 28097  mulnegs2d 28098  mulsass 28103  mulsassd 28104  mulscom 28076  mulscomd 28077
[Conway] p. 19Theorem 8(i)mulscl 28071  mulscld 28072
[Conway] p. 19Theorem 8(iii)slemuld 28075  sltmul 28073  sltmuld 28074
[Conway] p. 20Theorem 9mulsgt0 28081  mulsgt0d 28082
[Conway] p. 21Theorem 10(iv)precsex 28154
[Conway] p. 23Theorem 11eqscut3 27763
[Conway] p. 24Definitiondf-reno 28394
[Conway] p. 24Theorem 13(ii)readdscl 28399  remulscl 28402  renegscl 28398
[Conway] p. 27Definitiondf-ons 28187  elons2 28193
[Conway] p. 27Theorem 14sltonex 28197
[Conway] p. 28Theorem 15onscutlt 28199  onswe 28204
[Conway] p. 29Remarkmadebday 27843  newbday 27845  oldbday 27844
[Conway] p. 29Definitiondf-made 27786  df-new 27788  df-old 27787
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13762
[Crawley] p. 1Definition of posetdf-poset 18216
[Crawley] p. 107Theorem 13.2hlsupr 39424
[Crawley] p. 110Theorem 13.3arglem1N 40228  dalaw 39924
[Crawley] p. 111Theorem 13.4hlathil 41999
[Crawley] p. 111Definition of set Wdf-watsN 40028
[Crawley] p. 111Definition of dilationdf-dilN 40144  df-ldil 40142  isldil 40148
[Crawley] p. 111Definition of translationdf-ltrn 40143  df-trnN 40145  isltrn 40157  ltrnu 40159
[Crawley] p. 112Lemma Acdlema1N 39829  cdlema2N 39830  exatleN 39442
[Crawley] p. 112Lemma B1cvrat 39514  cdlemb 39832  cdlemb2 40079  cdlemb3 40644  idltrn 40188  l1cvat 39093  lhpat 40081  lhpat2 40083  lshpat 39094  ltrnel 40177  ltrnmw 40189
[Crawley] p. 112Lemma Ccdlemc1 40229  cdlemc2 40230  ltrnnidn 40212  trlat 40207  trljat1 40204  trljat2 40205  trljat3 40206  trlne 40223  trlnidat 40211  trlnle 40224
[Crawley] p. 112Definition of automorphismdf-pautN 40029
[Crawley] p. 113Lemma Ccdlemc 40235  cdlemc3 40231  cdlemc4 40232
[Crawley] p. 113Lemma Dcdlemd 40245  cdlemd1 40236  cdlemd2 40237  cdlemd3 40238  cdlemd4 40239  cdlemd5 40240  cdlemd6 40241  cdlemd7 40242  cdlemd8 40243  cdlemd9 40244  cdleme31sde 40423  cdleme31se 40420  cdleme31se2 40421  cdleme31snd 40424  cdleme32a 40479  cdleme32b 40480  cdleme32c 40481  cdleme32d 40482  cdleme32e 40483  cdleme32f 40484  cdleme32fva 40475  cdleme32fva1 40476  cdleme32fvcl 40478  cdleme32le 40485  cdleme48fv 40537  cdleme4gfv 40545  cdleme50eq 40579  cdleme50f 40580  cdleme50f1 40581  cdleme50f1o 40584  cdleme50laut 40585  cdleme50ldil 40586  cdleme50lebi 40578  cdleme50rn 40583  cdleme50rnlem 40582  cdlemeg49le 40549  cdlemeg49lebilem 40577
[Crawley] p. 113Lemma Ecdleme 40598  cdleme00a 40247  cdleme01N 40259  cdleme02N 40260  cdleme0a 40249  cdleme0aa 40248  cdleme0b 40250  cdleme0c 40251  cdleme0cp 40252  cdleme0cq 40253  cdleme0dN 40254  cdleme0e 40255  cdleme0ex1N 40261  cdleme0ex2N 40262  cdleme0fN 40256  cdleme0gN 40257  cdleme0moN 40263  cdleme1 40265  cdleme10 40292  cdleme10tN 40296  cdleme11 40308  cdleme11a 40298  cdleme11c 40299  cdleme11dN 40300  cdleme11e 40301  cdleme11fN 40302  cdleme11g 40303  cdleme11h 40304  cdleme11j 40305  cdleme11k 40306  cdleme11l 40307  cdleme12 40309  cdleme13 40310  cdleme14 40311  cdleme15 40316  cdleme15a 40312  cdleme15b 40313  cdleme15c 40314  cdleme15d 40315  cdleme16 40323  cdleme16aN 40297  cdleme16b 40317  cdleme16c 40318  cdleme16d 40319  cdleme16e 40320  cdleme16f 40321  cdleme16g 40322  cdleme19a 40341  cdleme19b 40342  cdleme19c 40343  cdleme19d 40344  cdleme19e 40345  cdleme19f 40346  cdleme1b 40264  cdleme2 40266  cdleme20aN 40347  cdleme20bN 40348  cdleme20c 40349  cdleme20d 40350  cdleme20e 40351  cdleme20f 40352  cdleme20g 40353  cdleme20h 40354  cdleme20i 40355  cdleme20j 40356  cdleme20k 40357  cdleme20l 40360  cdleme20l1 40358  cdleme20l2 40359  cdleme20m 40361  cdleme20y 40340  cdleme20zN 40339  cdleme21 40375  cdleme21d 40368  cdleme21e 40369  cdleme22a 40378  cdleme22aa 40377  cdleme22b 40379  cdleme22cN 40380  cdleme22d 40381  cdleme22e 40382  cdleme22eALTN 40383  cdleme22f 40384  cdleme22f2 40385  cdleme22g 40386  cdleme23a 40387  cdleme23b 40388  cdleme23c 40389  cdleme26e 40397  cdleme26eALTN 40399  cdleme26ee 40398  cdleme26f 40401  cdleme26f2 40403  cdleme26f2ALTN 40402  cdleme26fALTN 40400  cdleme27N 40407  cdleme27a 40405  cdleme27cl 40404  cdleme28c 40410  cdleme3 40275  cdleme30a 40416  cdleme31fv 40428  cdleme31fv1 40429  cdleme31fv1s 40430  cdleme31fv2 40431  cdleme31id 40432  cdleme31sc 40422  cdleme31sdnN 40425  cdleme31sn 40418  cdleme31sn1 40419  cdleme31sn1c 40426  cdleme31sn2 40427  cdleme31so 40417  cdleme35a 40486  cdleme35b 40488  cdleme35c 40489  cdleme35d 40490  cdleme35e 40491  cdleme35f 40492  cdleme35fnpq 40487  cdleme35g 40493  cdleme35h 40494  cdleme35h2 40495  cdleme35sn2aw 40496  cdleme35sn3a 40497  cdleme36a 40498  cdleme36m 40499  cdleme37m 40500  cdleme38m 40501  cdleme38n 40502  cdleme39a 40503  cdleme39n 40504  cdleme3b 40267  cdleme3c 40268  cdleme3d 40269  cdleme3e 40270  cdleme3fN 40271  cdleme3fa 40274  cdleme3g 40272  cdleme3h 40273  cdleme4 40276  cdleme40m 40505  cdleme40n 40506  cdleme40v 40507  cdleme40w 40508  cdleme41fva11 40515  cdleme41sn3aw 40512  cdleme41sn4aw 40513  cdleme41snaw 40514  cdleme42a 40509  cdleme42b 40516  cdleme42c 40510  cdleme42d 40511  cdleme42e 40517  cdleme42f 40518  cdleme42g 40519  cdleme42h 40520  cdleme42i 40521  cdleme42k 40522  cdleme42ke 40523  cdleme42keg 40524  cdleme42mN 40525  cdleme42mgN 40526  cdleme43aN 40527  cdleme43bN 40528  cdleme43cN 40529  cdleme43dN 40530  cdleme5 40278  cdleme50ex 40597  cdleme50ltrn 40595  cdleme51finvN 40594  cdleme51finvfvN 40593  cdleme51finvtrN 40596  cdleme6 40279  cdleme7 40287  cdleme7a 40281  cdleme7aa 40280  cdleme7b 40282  cdleme7c 40283  cdleme7d 40284  cdleme7e 40285  cdleme7ga 40286  cdleme8 40288  cdleme8tN 40293  cdleme9 40291  cdleme9a 40289  cdleme9b 40290  cdleme9tN 40295  cdleme9taN 40294  cdlemeda 40336  cdlemedb 40335  cdlemednpq 40337  cdlemednuN 40338  cdlemefr27cl 40441  cdlemefr32fva1 40448  cdlemefr32fvaN 40447  cdlemefrs32fva 40438  cdlemefrs32fva1 40439  cdlemefs27cl 40451  cdlemefs32fva1 40461  cdlemefs32fvaN 40460  cdlemesner 40334  cdlemeulpq 40258
[Crawley] p. 114Lemma E4atex 40114  4atexlem7 40113  cdleme0nex 40328  cdleme17a 40324  cdleme17c 40326  cdleme17d 40536  cdleme17d1 40327  cdleme17d2 40533  cdleme18a 40329  cdleme18b 40330  cdleme18c 40331  cdleme18d 40333  cdleme4a 40277
[Crawley] p. 115Lemma Ecdleme21a 40363  cdleme21at 40366  cdleme21b 40364  cdleme21c 40365  cdleme21ct 40367  cdleme21f 40370  cdleme21g 40371  cdleme21h 40372  cdleme21i 40373  cdleme22gb 40332
[Crawley] p. 116Lemma Fcdlemf 40601  cdlemf1 40599  cdlemf2 40600
[Crawley] p. 116Lemma Gcdlemftr1 40605  cdlemg16 40695  cdlemg28 40742  cdlemg28a 40731  cdlemg28b 40741  cdlemg3a 40635  cdlemg42 40767  cdlemg43 40768  cdlemg44 40771  cdlemg44a 40769  cdlemg46 40773  cdlemg47 40774  cdlemg9 40672  ltrnco 40757  ltrncom 40776  tgrpabl 40789  trlco 40765
[Crawley] p. 116Definition of Gdf-tgrp 40781
[Crawley] p. 117Lemma Gcdlemg17 40715  cdlemg17b 40700
[Crawley] p. 117Definition of Edf-edring-rN 40794  df-edring 40795
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40798
[Crawley] p. 118Remarktendopltp 40818
[Crawley] p. 118Lemma Hcdlemh 40855  cdlemh1 40853  cdlemh2 40854
[Crawley] p. 118Lemma Icdlemi 40858  cdlemi1 40856  cdlemi2 40857
[Crawley] p. 118Lemma Jcdlemj1 40859  cdlemj2 40860  cdlemj3 40861  tendocan 40862
[Crawley] p. 118Lemma Kcdlemk 41012  cdlemk1 40869  cdlemk10 40881  cdlemk11 40887  cdlemk11t 40984  cdlemk11ta 40967  cdlemk11tb 40969  cdlemk11tc 40983  cdlemk11u-2N 40927  cdlemk11u 40909  cdlemk12 40888  cdlemk12u-2N 40928  cdlemk12u 40910  cdlemk13-2N 40914  cdlemk13 40890  cdlemk14-2N 40916  cdlemk14 40892  cdlemk15-2N 40917  cdlemk15 40893  cdlemk16-2N 40918  cdlemk16 40895  cdlemk16a 40894  cdlemk17-2N 40919  cdlemk17 40896  cdlemk18-2N 40924  cdlemk18-3N 40938  cdlemk18 40906  cdlemk19-2N 40925  cdlemk19 40907  cdlemk19u 41008  cdlemk1u 40897  cdlemk2 40870  cdlemk20-2N 40930  cdlemk20 40912  cdlemk21-2N 40929  cdlemk21N 40911  cdlemk22-3 40939  cdlemk22 40931  cdlemk23-3 40940  cdlemk24-3 40941  cdlemk25-3 40942  cdlemk26-3 40944  cdlemk26b-3 40943  cdlemk27-3 40945  cdlemk28-3 40946  cdlemk29-3 40949  cdlemk3 40871  cdlemk30 40932  cdlemk31 40934  cdlemk32 40935  cdlemk33N 40947  cdlemk34 40948  cdlemk35 40950  cdlemk36 40951  cdlemk37 40952  cdlemk38 40953  cdlemk39 40954  cdlemk39u 41006  cdlemk4 40872  cdlemk41 40958  cdlemk42 40979  cdlemk42yN 40982  cdlemk43N 41001  cdlemk45 40985  cdlemk46 40986  cdlemk47 40987  cdlemk48 40988  cdlemk49 40989  cdlemk5 40874  cdlemk50 40990  cdlemk51 40991  cdlemk52 40992  cdlemk53 40995  cdlemk54 40996  cdlemk55 40999  cdlemk55u 41004  cdlemk56 41009  cdlemk5a 40873  cdlemk5auN 40898  cdlemk5u 40899  cdlemk6 40875  cdlemk6u 40900  cdlemk7 40886  cdlemk7u-2N 40926  cdlemk7u 40908  cdlemk8 40876  cdlemk9 40877  cdlemk9bN 40878  cdlemki 40879  cdlemkid 40974  cdlemkj-2N 40920  cdlemkj 40901  cdlemksat 40884  cdlemksel 40883  cdlemksv 40882  cdlemksv2 40885  cdlemkuat 40904  cdlemkuel-2N 40922  cdlemkuel-3 40936  cdlemkuel 40903  cdlemkuv-2N 40921  cdlemkuv2-2 40923  cdlemkuv2-3N 40937  cdlemkuv2 40905  cdlemkuvN 40902  cdlemkvcl 40880  cdlemky 40964  cdlemkyyN 41000  tendoex 41013
[Crawley] p. 120Remarkdva1dim 41023
[Crawley] p. 120Lemma Lcdleml1N 41014  cdleml2N 41015  cdleml3N 41016  cdleml4N 41017  cdleml5N 41018  cdleml6 41019  cdleml7 41020  cdleml8 41021  cdleml9 41022  dia1dim 41099
[Crawley] p. 120Lemma Mdia11N 41086  diaf11N 41087  dialss 41084  diaord 41085  dibf11N 41199  djajN 41175
[Crawley] p. 120Definition of isomorphism mapdiaval 41070
[Crawley] p. 121Lemma Mcdlemm10N 41156  dia2dimlem1 41102  dia2dimlem2 41103  dia2dimlem3 41104  dia2dimlem4 41105  dia2dimlem5 41106  diaf1oN 41168  diarnN 41167  dvheveccl 41150  dvhopN 41154
[Crawley] p. 121Lemma Ncdlemn 41250  cdlemn10 41244  cdlemn11 41249  cdlemn11a 41245  cdlemn11b 41246  cdlemn11c 41247  cdlemn11pre 41248  cdlemn2 41233  cdlemn2a 41234  cdlemn3 41235  cdlemn4 41236  cdlemn4a 41237  cdlemn5 41239  cdlemn5pre 41238  cdlemn6 41240  cdlemn7 41241  cdlemn8 41242  cdlemn9 41243  diclspsn 41232
[Crawley] p. 121Definition of phi(q)df-dic 41211
[Crawley] p. 122Lemma Ndih11 41303  dihf11 41305  dihjust 41255  dihjustlem 41254  dihord 41302  dihord1 41256  dihord10 41261  dihord11b 41260  dihord11c 41262  dihord2 41265  dihord2a 41257  dihord2b 41258  dihord2cN 41259  dihord2pre 41263  dihord2pre2 41264  dihordlem6 41251  dihordlem7 41252  dihordlem7b 41253
[Crawley] p. 122Definition of isomorphism mapdihffval 41268  dihfval 41269  dihval 41270
[Diestel] p. 3Definitiondf-gric 47911  df-grim 47908  isuspgrim 47926
[Diestel] p. 3Section 1.1df-cusgr 29388  df-nbgr 29309
[Diestel] p. 3Definition by df-grisom 47907
[Diestel] p. 4Section 1.1df-isubgr 47891  df-subgr 29244  uhgrspan1 29279  uhgrspansubgr 29267
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29531  vtxdgoddnumeven 29530
[Diestel] p. 27Section 1.10df-ushgr 29035
[EGA] p. 80Notation 1.1.1rspecval 33872
[EGA] p. 80Proposition 1.1.2zartop 33884
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33876  zarcls1 33877
[EGA] p. 81Corollary 1.1.8zart0 33887
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33890
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33893
[Eisenberg] p. 67Definition 5.3df-dif 3905
[Eisenberg] p. 82Definition 6.3dfom3 9537
[Eisenberg] p. 125Definition 8.21df-map 8752
[Eisenberg] p. 216Example 13.2(4)omenps 9545
[Eisenberg] p. 310Theorem 19.8cardprc 9870
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10443
[Enderton] p. 18Axiom of Empty Setaxnul 5243
[Enderton] p. 19Definitiondf-tp 4581
[Enderton] p. 26Exercise 5unissb 4891
[Enderton] p. 26Exercise 10pwel 5319
[Enderton] p. 28Exercise 7(b)pwun 5509
[Enderton] p. 30Theorem "Distributive laws"iinin1 5027  iinin2 5026  iinun2 5021  iunin1 5020  iunin1f 32532  iunin2 5019  uniin1 32526  uniin2 32527
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5025  iundif2 5022
[Enderton] p. 32Exercise 20unineq 4238
[Enderton] p. 33Exercise 23iinuni 5046
[Enderton] p. 33Exercise 25iununi 5047
[Enderton] p. 33Exercise 24(a)iinpw 5054
[Enderton] p. 33Exercise 24(b)iunpw 7704  iunpwss 5055
[Enderton] p. 36Definitionopthwiener 5454
[Enderton] p. 38Exercise 6(a)unipw 5391
[Enderton] p. 38Exercise 6(b)pwuni 4896
[Enderton] p. 41Lemma 3Dopeluu 5410  rnex 7840  rnexg 7832
[Enderton] p. 41Exercise 8dmuni 5854  rnuni 6095
[Enderton] p. 42Definition of a functiondffun7 6508  dffun8 6509
[Enderton] p. 43Definition of function valuefunfv2 6910
[Enderton] p. 43Definition of single-rootedfuncnv 6550
[Enderton] p. 44Definition (d)dfima2 6011  dfima3 6012
[Enderton] p. 47Theorem 3Hfvco2 6919
[Enderton] p. 49Axiom of Choice (first form)ac7 10361  ac7g 10362  df-ac 10004  dfac2 10020  dfac2a 10018  dfac2b 10019  dfac3 10009  dfac7 10021
[Enderton] p. 50Theorem 3K(a)imauni 7180
[Enderton] p. 52Definitiondf-map 8752
[Enderton] p. 53Exercise 21coass 6213
[Enderton] p. 53Exercise 27dmco 6202
[Enderton] p. 53Exercise 14(a)funin 6557
[Enderton] p. 53Exercise 22(a)imass2 6051
[Enderton] p. 54Remarkixpf 8844  ixpssmap 8856
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8822
[Enderton] p. 55Axiom of Choice (second form)ac9 10371  ac9s 10381
[Enderton] p. 56Theorem 3Meqvrelref 38646  erref 8642
[Enderton] p. 57Lemma 3Neqvrelthi 38649  erthi 8678
[Enderton] p. 57Definitiondf-ec 8624
[Enderton] p. 58Definitiondf-qs 8628
[Enderton] p. 61Exercise 35df-ec 8624
[Enderton] p. 65Exercise 56(a)dmun 5850
[Enderton] p. 68Definition of successordf-suc 6312
[Enderton] p. 71Definitiondf-tr 5199  dftr4 5204
[Enderton] p. 72Theorem 4Eunisuc 6387  unisucg 6386
[Enderton] p. 73Exercise 6unisuc 6387  unisucg 6386
[Enderton] p. 73Exercise 5(a)truni 5213
[Enderton] p. 73Exercise 5(b)trint 5215  trintALT 44912
[Enderton] p. 79Theorem 4I(A1)nna0 8519
[Enderton] p. 79Theorem 4I(A2)nnasuc 8521  onasuc 8443
[Enderton] p. 79Definition of operation valuedf-ov 7349
[Enderton] p. 80Theorem 4J(A1)nnm0 8520
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8522  onmsuc 8444
[Enderton] p. 81Theorem 4K(1)nnaass 8537
[Enderton] p. 81Theorem 4K(2)nna0r 8524  nnacom 8532
[Enderton] p. 81Theorem 4K(3)nndi 8538
[Enderton] p. 81Theorem 4K(4)nnmass 8539
[Enderton] p. 81Theorem 4K(5)nnmcom 8541
[Enderton] p. 82Exercise 16nnm0r 8525  nnmsucr 8540
[Enderton] p. 88Exercise 23nnaordex 8553
[Enderton] p. 129Definitiondf-en 8870
[Enderton] p. 132Theorem 6B(b)canth 7300
[Enderton] p. 133Exercise 1xpomen 9903
[Enderton] p. 133Exercise 2qnnen 16119
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9116
[Enderton] p. 135Corollary 6Cphp3 9118
[Enderton] p. 136Corollary 6Enneneq 9115
[Enderton] p. 136Corollary 6D(a)pssinf 9146
[Enderton] p. 136Corollary 6D(b)ominf 9148
[Enderton] p. 137Lemma 6Fpssnn 9078
[Enderton] p. 138Corollary 6Gssfi 9082
[Enderton] p. 139Theorem 6H(c)mapen 9054
[Enderton] p. 142Theorem 6I(3)xpdjuen 10068
[Enderton] p. 142Theorem 6I(4)mapdjuen 10069
[Enderton] p. 143Theorem 6Jdju0en 10064  dju1en 10060
[Enderton] p. 144Exercise 13iunfi 9227  unifi 9228  unifi2 9229
[Enderton] p. 144Corollary 6Kundif2 4427  unfi 9080  unfi2 9194
[Enderton] p. 145Figure 38ffoss 7878
[Enderton] p. 145Definitiondf-dom 8871
[Enderton] p. 146Example 1domen 8884  domeng 8885
[Enderton] p. 146Example 3nndomo 9126  nnsdom 9544  nnsdomg 9183
[Enderton] p. 149Theorem 6L(a)djudom2 10072
[Enderton] p. 149Theorem 6L(c)mapdom1 9055  xpdom1 8989  xpdom1g 8987  xpdom2g 8986
[Enderton] p. 149Theorem 6L(d)mapdom2 9061
[Enderton] p. 151Theorem 6Mzorn 10395  zorng 10392
[Enderton] p. 151Theorem 6M(4)ac8 10380  dfac5 10017
[Enderton] p. 159Theorem 6Qunictb 10463
[Enderton] p. 164Exampleinfdif 10096
[Enderton] p. 168Definitiondf-po 5524
[Enderton] p. 192Theorem 7M(a)oneli 6421
[Enderton] p. 192Theorem 7M(b)ontr1 6353
[Enderton] p. 192Theorem 7M(c)onirri 6420
[Enderton] p. 193Corollary 7N(b)0elon 6361
[Enderton] p. 193Corollary 7N(c)onsuci 7769
[Enderton] p. 193Corollary 7N(d)ssonunii 7714
[Enderton] p. 194Remarkonprc 7711
[Enderton] p. 194Exercise 16suc11 6415
[Enderton] p. 197Definitiondf-card 9829
[Enderton] p. 197Theorem 7Pcarden 10439
[Enderton] p. 200Exercise 25tfis 7785
[Enderton] p. 202Lemma 7Tr1tr 9666
[Enderton] p. 202Definitiondf-r1 9654
[Enderton] p. 202Theorem 7Qr1val1 9676
[Enderton] p. 204Theorem 7V(b)rankval4 9757  rankval4b 35104
[Enderton] p. 206Theorem 7X(b)en2lp 9496
[Enderton] p. 207Exercise 30rankpr 9747  rankprb 9741  rankpw 9733  rankpwi 9713  rankuniss 9756
[Enderton] p. 207Exercise 34opthreg 9508
[Enderton] p. 208Exercise 35suc11reg 9509
[Enderton] p. 212Definition of alephalephval3 9998
[Enderton] p. 213Theorem 8A(a)alephord2 9964
[Enderton] p. 213Theorem 8A(b)cardalephex 9978
[Enderton] p. 218Theorem Schema 8Eonfununi 8261
[Enderton] p. 222Definition of kardkarden 9785  kardex 9784
[Enderton] p. 238Theorem 8Roeoa 8512
[Enderton] p. 238Theorem 8Soeoe 8514
[Enderton] p. 240Exercise 25oarec 8477
[Enderton] p. 257Definition of cofinalitycflm 10138
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17545
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17487
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18456  mrieqv2d 17542  mrieqvd 17541
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17546
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17551  mreexexlem2d 17548
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18462  mreexfidimd 17553
[Frege1879] p. 11Statementdf3or2 43800
[Frege1879] p. 12Statementdf3an2 43801  dfxor4 43798  dfxor5 43799
[Frege1879] p. 26Axiom 1ax-frege1 43822
[Frege1879] p. 26Axiom 2ax-frege2 43823
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43827
[Frege1879] p. 31Proposition 4frege4 43831
[Frege1879] p. 32Proposition 5frege5 43832
[Frege1879] p. 33Proposition 6frege6 43838
[Frege1879] p. 34Proposition 7frege7 43840
[Frege1879] p. 35Axiom 8ax-frege8 43841  axfrege8 43839
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37478
[Frege1879] p. 35Proposition 9frege9 43844
[Frege1879] p. 36Proposition 10frege10 43852
[Frege1879] p. 36Proposition 11frege11 43846
[Frege1879] p. 37Proposition 12frege12 43845
[Frege1879] p. 37Proposition 13frege13 43854
[Frege1879] p. 37Proposition 14frege14 43855
[Frege1879] p. 38Proposition 15frege15 43858
[Frege1879] p. 38Proposition 16frege16 43848
[Frege1879] p. 39Proposition 17frege17 43853
[Frege1879] p. 39Proposition 18frege18 43850
[Frege1879] p. 39Proposition 19frege19 43856
[Frege1879] p. 40Proposition 20frege20 43860
[Frege1879] p. 40Proposition 21frege21 43859
[Frege1879] p. 41Proposition 22frege22 43851
[Frege1879] p. 42Proposition 23frege23 43857
[Frege1879] p. 42Proposition 24frege24 43847
[Frege1879] p. 42Proposition 25frege25 43849  rp-frege25 43837
[Frege1879] p. 42Proposition 26frege26 43842
[Frege1879] p. 43Axiom 28ax-frege28 43862
[Frege1879] p. 43Proposition 27frege27 43843
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43863
[Frege1879] p. 44Axiom 31ax-frege31 43866  axfrege31 43865
[Frege1879] p. 44Proposition 30frege30 43864
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43867
[Frege1879] p. 44Proposition 33frege33 43868
[Frege1879] p. 45Proposition 34frege34 43869
[Frege1879] p. 45Proposition 35frege35 43870
[Frege1879] p. 45Proposition 36frege36 43871
[Frege1879] p. 46Proposition 37frege37 43872
[Frege1879] p. 46Proposition 38frege38 43873
[Frege1879] p. 46Proposition 39frege39 43874
[Frege1879] p. 46Proposition 40frege40 43875
[Frege1879] p. 47Axiom 41ax-frege41 43877  axfrege41 43876
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43878
[Frege1879] p. 47Proposition 43frege43 43879
[Frege1879] p. 47Proposition 44frege44 43880
[Frege1879] p. 47Proposition 45frege45 43881
[Frege1879] p. 48Proposition 46frege46 43882
[Frege1879] p. 48Proposition 47frege47 43883
[Frege1879] p. 49Proposition 48frege48 43884
[Frege1879] p. 49Proposition 49frege49 43885
[Frege1879] p. 49Proposition 50frege50 43886
[Frege1879] p. 50Axiom 52ax-frege52a 43889  ax-frege52c 43920  frege52aid 43890  frege52b 43921
[Frege1879] p. 50Axiom 54ax-frege54a 43894  ax-frege54c 43924  frege54b 43925
[Frege1879] p. 50Proposition 51frege51 43887
[Frege1879] p. 50Proposition 52dfsbcq 3743
[Frege1879] p. 50Proposition 53frege53a 43892  frege53aid 43891  frege53b 43922  frege53c 43946
[Frege1879] p. 50Proposition 54biid 261  eqid 2731
[Frege1879] p. 50Proposition 55frege55a 43900  frege55aid 43897  frege55b 43929  frege55c 43950  frege55cor1a 43901  frege55lem2a 43899  frege55lem2b 43928  frege55lem2c 43949
[Frege1879] p. 50Proposition 56frege56a 43903  frege56aid 43902  frege56b 43930  frege56c 43951
[Frege1879] p. 51Axiom 58ax-frege58a 43907  ax-frege58b 43933  frege58bid 43934  frege58c 43953
[Frege1879] p. 51Proposition 57frege57a 43905  frege57aid 43904  frege57b 43931  frege57c 43952
[Frege1879] p. 51Proposition 58spsbc 3754
[Frege1879] p. 51Proposition 59frege59a 43909  frege59b 43936  frege59c 43954
[Frege1879] p. 52Proposition 60frege60a 43910  frege60b 43937  frege60c 43955
[Frege1879] p. 52Proposition 61frege61a 43911  frege61b 43938  frege61c 43956
[Frege1879] p. 52Proposition 62frege62a 43912  frege62b 43939  frege62c 43957
[Frege1879] p. 52Proposition 63frege63a 43913  frege63b 43940  frege63c 43958
[Frege1879] p. 53Proposition 64frege64a 43914  frege64b 43941  frege64c 43959
[Frege1879] p. 53Proposition 65frege65a 43915  frege65b 43942  frege65c 43960
[Frege1879] p. 54Proposition 66frege66a 43916  frege66b 43943  frege66c 43961
[Frege1879] p. 54Proposition 67frege67a 43917  frege67b 43944  frege67c 43962
[Frege1879] p. 54Proposition 68frege68a 43918  frege68b 43945  frege68c 43963
[Frege1879] p. 55Definition 69dffrege69 43964
[Frege1879] p. 58Proposition 70frege70 43965
[Frege1879] p. 59Proposition 71frege71 43966
[Frege1879] p. 59Proposition 72frege72 43967
[Frege1879] p. 59Proposition 73frege73 43968
[Frege1879] p. 60Definition 76dffrege76 43971
[Frege1879] p. 60Proposition 74frege74 43969
[Frege1879] p. 60Proposition 75frege75 43970
[Frege1879] p. 62Proposition 77frege77 43972  frege77d 43778
[Frege1879] p. 63Proposition 78frege78 43973
[Frege1879] p. 63Proposition 79frege79 43974
[Frege1879] p. 63Proposition 80frege80 43975
[Frege1879] p. 63Proposition 81frege81 43976  frege81d 43779
[Frege1879] p. 64Proposition 82frege82 43977
[Frege1879] p. 65Proposition 83frege83 43978  frege83d 43780
[Frege1879] p. 65Proposition 84frege84 43979
[Frege1879] p. 66Proposition 85frege85 43980
[Frege1879] p. 66Proposition 86frege86 43981
[Frege1879] p. 66Proposition 87frege87 43982  frege87d 43782
[Frege1879] p. 67Proposition 88frege88 43983
[Frege1879] p. 68Proposition 89frege89 43984
[Frege1879] p. 68Proposition 90frege90 43985
[Frege1879] p. 68Proposition 91frege91 43986  frege91d 43783
[Frege1879] p. 69Proposition 92frege92 43987
[Frege1879] p. 70Proposition 93frege93 43988
[Frege1879] p. 70Proposition 94frege94 43989
[Frege1879] p. 70Proposition 95frege95 43990
[Frege1879] p. 71Definition 99dffrege99 43994
[Frege1879] p. 71Proposition 96frege96 43991  frege96d 43781
[Frege1879] p. 71Proposition 97frege97 43992  frege97d 43784
[Frege1879] p. 71Proposition 98frege98 43993  frege98d 43785
[Frege1879] p. 72Proposition 100frege100 43995
[Frege1879] p. 72Proposition 101frege101 43996
[Frege1879] p. 72Proposition 102frege102 43997  frege102d 43786
[Frege1879] p. 73Proposition 103frege103 43998
[Frege1879] p. 73Proposition 104frege104 43999
[Frege1879] p. 73Proposition 105frege105 44000
[Frege1879] p. 73Proposition 106frege106 44001  frege106d 43787
[Frege1879] p. 74Proposition 107frege107 44002
[Frege1879] p. 74Proposition 108frege108 44003  frege108d 43788
[Frege1879] p. 74Proposition 109frege109 44004  frege109d 43789
[Frege1879] p. 75Proposition 110frege110 44005
[Frege1879] p. 75Proposition 111frege111 44006  frege111d 43791
[Frege1879] p. 76Proposition 112frege112 44007
[Frege1879] p. 76Proposition 113frege113 44008
[Frege1879] p. 76Proposition 114frege114 44009  frege114d 43790
[Frege1879] p. 77Definition 115dffrege115 44010
[Frege1879] p. 77Proposition 116frege116 44011
[Frege1879] p. 78Proposition 117frege117 44012
[Frege1879] p. 78Proposition 118frege118 44013
[Frege1879] p. 78Proposition 119frege119 44014
[Frege1879] p. 78Proposition 120frege120 44015
[Frege1879] p. 79Proposition 121frege121 44016
[Frege1879] p. 79Proposition 122frege122 44017  frege122d 43792
[Frege1879] p. 79Proposition 123frege123 44018
[Frege1879] p. 80Proposition 124frege124 44019  frege124d 43793
[Frege1879] p. 81Proposition 125frege125 44020
[Frege1879] p. 81Proposition 126frege126 44021  frege126d 43794
[Frege1879] p. 82Proposition 127frege127 44022
[Frege1879] p. 83Proposition 128frege128 44023
[Frege1879] p. 83Proposition 129frege129 44024  frege129d 43795
[Frege1879] p. 84Proposition 130frege130 44025
[Frege1879] p. 85Proposition 131frege131 44026  frege131d 43796
[Frege1879] p. 86Proposition 132frege132 44027
[Frege1879] p. 86Proposition 133frege133 44028  frege133d 43797
[Fremlin1] p. 13Definition 111G (b)df-salgen 46350
[Fremlin1] p. 13Definition 111G (d)borelmbl 46673
[Fremlin1] p. 13Proposition 111G (b)salgenss 46373
[Fremlin1] p. 14Definition 112Aismea 46488
[Fremlin1] p. 15Remark 112B (d)psmeasure 46508
[Fremlin1] p. 15Property 112C (a)meadjun 46499  meadjunre 46513
[Fremlin1] p. 15Property 112C (b)meassle 46500
[Fremlin1] p. 15Property 112C (c)meaunle 46501
[Fremlin1] p. 16Property 112C (d)iundjiun 46497  meaiunle 46506  meaiunlelem 46505
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46518  meaiuninc2 46519  meaiuninc3 46522  meaiuninc3v 46521  meaiunincf 46520  meaiuninclem 46517
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46524  meaiininc2 46525  meaiininclem 46523
[Fremlin1] p. 19Theorem 113Ccaragen0 46543  caragendifcl 46551  caratheodory 46565  omelesplit 46555
[Fremlin1] p. 19Definition 113Aisome 46531  isomennd 46568  isomenndlem 46567
[Fremlin1] p. 19Remark 113B (c)omeunle 46553
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46572  voncmpl 46658
[Fremlin1] p. 19Definition 113A (ii)omessle 46535
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46560  carageniuncllem1 46558  carageniuncllem2 46559  caragenuncl 46550  caragenuncllem 46549  caragenunicl 46561
[Fremlin1] p. 21Remark 113Dcaragenel2d 46569
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46563  caratheodorylem2 46564
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46572
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46631  hoidmv1lelem1 46628  hoidmv1lelem2 46629  hoidmv1lelem3 46630
[Fremlin1] p. 25Definition 114Eisvonmbl 46675
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46631  hoidmvle 46637  hoidmvlelem1 46632  hoidmvlelem2 46633  hoidmvlelem3 46634  hoidmvlelem4 46635  hoidmvlelem5 46636  hsphoidmvle2 46622  hsphoif 46613  hsphoival 46616
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46585
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46593
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46620  hoidmvn0val 46621  hoidmvval 46614  hoidmvval0 46624  hoidmvval0b 46627
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46625  hsphoidmvle 46623
[Fremlin1] p. 30Definition 115Cdf-ovoln 46574  df-voln 46576
[Fremlin1] p. 30Proposition 115D (a)dmovn 46641  ovn0 46603  ovn0lem 46602  ovnf 46600  ovnome 46610  ovnssle 46598  ovnsslelem 46597  ovnsupge0 46594
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46640  ovnhoilem1 46638  ovnhoilem2 46639  vonhoi 46704
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46657  hoidifhspf 46655  hoidifhspval 46645  hoidifhspval2 46652  hoidifhspval3 46656  hspmbl 46666  hspmbllem1 46663  hspmbllem2 46664  hspmbllem3 46665
[Fremlin1] p. 31Definition 115Evoncmpl 46658  vonmea 46611
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46609  ovnsubadd2 46683  ovnsubadd2lem 46682  ovnsubaddlem1 46607  ovnsubaddlem2 46608
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46668  hoimbl2 46702  hoimbllem 46667  hspdifhsp 46653  opnvonmbl 46671  opnvonmbllem2 46670
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46673
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46716  iccvonmbllem 46715  ioovonmbl 46714
[Fremlin1] p. 32Proposition 115G (d)vonicc 46722  vonicclem2 46721  vonioo 46719  vonioolem2 46718  vonn0icc 46725  vonn0icc2 46729  vonn0ioo 46724  vonn0ioo2 46727
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46726  snvonmbl 46723  vonct 46730  vonsn 46728
[Fremlin1] p. 35Lemma 121Asubsalsal 46396
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46395  subsaliuncllem 46394
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46762  salpreimalegt 46746  salpreimaltle 46763
[Fremlin1] p. 35Proposition 121B (i)issmf 46765  issmff 46771  issmflem 46764
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46782  issmflelem 46781  smfpreimale 46791
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46793  issmfgtlem 46792
[Fremlin1] p. 36Definition 121Cdf-smblfn 46733  issmf 46765  issmff 46771  issmfge 46807  issmfgelem 46806  issmfgt 46793  issmfgtlem 46792  issmfle 46782  issmflelem 46781  issmflem 46764
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46744  salpreimagtlt 46767  salpreimalelt 46766
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46807  issmfgelem 46806
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46790
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46788  cnfsmf 46777
[Fremlin1] p. 36Proposition 121D (c)decsmf 46804  decsmflem 46803  incsmf 46779  incsmflem 46778
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46738  pimconstlt1 46739  smfconst 46786
[Fremlin1] p. 37Proposition 121E (b)smfadd 46802  smfaddlem1 46800  smfaddlem2 46801
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46833
[Fremlin1] p. 37Proposition 121E (d)smfmul 46832  smfmullem1 46828  smfmullem2 46829  smfmullem3 46830  smfmullem4 46831
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46834
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46837  smfpimbor1lem2 46836
[Fremlin1] p. 37Proposition 121E (g)smfco 46839
[Fremlin1] p. 37Proposition 121E (h)smfres 46827
[Fremlin1] p. 38Proposition 121E (e)smfrec 46826
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46835  smfresal 46825
[Fremlin1] p. 38Proposition 121F (a)smflim 46814  smflim2 46843  smflimlem1 46808  smflimlem2 46809  smflimlem3 46810  smflimlem4 46811  smflimlem5 46812  smflimlem6 46813  smflimmpt 46847
[Fremlin1] p. 38Proposition 121F (b)smfsup 46851  smfsuplem1 46848  smfsuplem2 46849  smfsuplem3 46850  smfsupmpt 46852  smfsupxr 46853
[Fremlin1] p. 38Proposition 121F (c)smfinf 46855  smfinflem 46854  smfinfmpt 46856
[Fremlin1] p. 39Remark 121Gsmflim 46814  smflim2 46843  smflimmpt 46847
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46845
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46875  smfdivdmmbl2 46878  smfinfdmmbl 46886  smfinfdmmbllem 46885  smfsupdmmbl 46882  smfsupdmmbllem 46881
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46865  smflimsuplem2 46858  smflimsuplem6 46862  smflimsuplem7 46863  smflimsuplem8 46864  smflimsupmpt 46866
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46868  smfliminflem 46867  smfliminfmpt 46869
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46733
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46879  fsupdm2 46880
[Fremlin1], p. 39Proposition 121Hadddmmbl 46870  adddmmbl2 46871  finfdm 46883  finfdm2 46884  fsupdm 46879  fsupdm2 46880  muldmmbl 46872  muldmmbl2 46873
[Fremlin1], p. 39Proposition 121F (c)finfdm 46883  finfdm2 46884
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25462
[Fremlin5] p. 213Lemma 565Cauniioovol 25505
[Fremlin5] p. 214Lemma 565Cauniioombl 25515
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37737
[Fremlin5] p. 220Theorem 565Maftc1anc 37740
[FreydScedrov] p. 283Axiom of Infinityax-inf 9528  inf1 9512  inf2 9513
[Gleason] p. 117Proposition 9-2.1df-enq 10799  enqer 10809
[Gleason] p. 117Proposition 9-2.2df-1nq 10804  df-nq 10800
[Gleason] p. 117Proposition 9-2.3df-plpq 10796  df-plq 10802
[Gleason] p. 119Proposition 9-2.4caovmo 7583  df-mpq 10797  df-mq 10803
[Gleason] p. 119Proposition 9-2.5df-rq 10805
[Gleason] p. 119Proposition 9-2.6ltexnq 10863
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10864  ltbtwnnq 10866
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10859
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10860
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10867
[Gleason] p. 121Definition 9-3.1df-np 10869
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10881
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10883
[Gleason] p. 122Definitiondf-1p 10870
[Gleason] p. 122Remark (1)prub 10882
[Gleason] p. 122Lemma 9-3.4prlem934 10921
[Gleason] p. 122Proposition 9-3.2df-ltp 10873
[Gleason] p. 122Proposition 9-3.3ltsopr 10920  psslinpr 10919  supexpr 10942  suplem1pr 10940  suplem2pr 10941
[Gleason] p. 123Proposition 9-3.5addclpr 10906  addclprlem1 10904  addclprlem2 10905  df-plp 10871
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10910
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10909
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10922
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10931  ltexprlem1 10924  ltexprlem2 10925  ltexprlem3 10926  ltexprlem4 10927  ltexprlem5 10928  ltexprlem6 10929  ltexprlem7 10930
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10933  ltaprlem 10932
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10934
[Gleason] p. 124Lemma 9-3.6prlem936 10935
[Gleason] p. 124Proposition 9-3.7df-mp 10872  mulclpr 10908  mulclprlem 10907  reclem2pr 10936
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10917
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10912
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10911
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10916
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10939  reclem3pr 10937  reclem4pr 10938
[Gleason] p. 126Proposition 9-4.1df-enr 10943  enrer 10951
[Gleason] p. 126Proposition 9-4.2df-0r 10948  df-1r 10949  df-nr 10944
[Gleason] p. 126Proposition 9-4.3df-mr 10946  df-plr 10945  negexsr 10990  recexsr 10995  recexsrlem 10991
[Gleason] p. 127Proposition 9-4.4df-ltr 10947
[Gleason] p. 130Proposition 10-1.3creui 12117  creur 12116  cru 12114
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11076  axcnre 11052
[Gleason] p. 132Definition 10-3.1crim 15019  crimd 15136  crimi 15097  crre 15018  crred 15135  crrei 15096
[Gleason] p. 132Definition 10-3.2remim 15021  remimd 15102
[Gleason] p. 133Definition 10.36absval2 15188  absval2d 15352  absval2i 15302
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15045  cjaddd 15124  cjaddi 15092
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15046  cjmuld 15125  cjmuli 15093
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15044  cjcjd 15103  cjcji 15075
[Gleason] p. 133Proposition 10-3.4(f)cjre 15043  cjreb 15027  cjrebd 15106  cjrebi 15078  cjred 15130  rere 15026  rereb 15024  rerebd 15105  rerebi 15077  rered 15128
[Gleason] p. 133Proposition 10-3.4(h)addcj 15052  addcjd 15116  addcji 15087
[Gleason] p. 133Proposition 10-3.7(a)absval 15142
[Gleason] p. 133Proposition 10-3.7(b)abscj 15183  abscjd 15357  abscji 15306
[Gleason] p. 133Proposition 10-3.7(c)abs00 15193  abs00d 15353  abs00i 15303  absne0d 15354
[Gleason] p. 133Proposition 10-3.7(d)releabs 15226  releabsd 15358  releabsi 15307
[Gleason] p. 133Proposition 10-3.7(f)absmul 15198  absmuld 15361  absmuli 15309
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15186  sqabsaddi 15310
[Gleason] p. 133Proposition 10-3.7(h)abstri 15235  abstrid 15363  abstrii 15313
[Gleason] p. 134Definition 10-4.1df-exp 13966  exp0 13969  expp1 13972  expp1d 14051
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26613  cxpaddd 26651  expadd 14008  expaddd 14052  expaddz 14010
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26622  cxpmuld 26671  expmul 14011  expmuld 14053  expmulz 14012
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26619  mulcxpd 26662  mulexp 14005  mulexpd 14065  mulexpz 14006
[Gleason] p. 140Exercise 1znnen 16118
[Gleason] p. 141Definition 11-2.1fzval 13406
[Gleason] p. 168Proposition 12-2.1(a)climadd 15536  rlimadd 15547  rlimdiv 15550
[Gleason] p. 168Proposition 12-2.1(b)climsub 15538  rlimsub 15548
[Gleason] p. 168Proposition 12-2.1(c)climmul 15537  rlimmul 15549
[Gleason] p. 171Corollary 12-2.2climmulc2 15541
[Gleason] p. 172Corollary 12-2.5climrecl 15487
[Gleason] p. 172Proposition 12-2.4(c)climabs 15508  climcj 15509  climim 15511  climre 15510  rlimabs 15513  rlimcj 15514  rlimim 15516  rlimre 15515
[Gleason] p. 173Definition 12-3.1df-ltxr 11148  df-xr 11147  ltxr 13011
[Gleason] p. 175Definition 12-4.1df-limsup 15375  limsupval 15378
[Gleason] p. 180Theorem 12-5.1climsup 15574
[Gleason] p. 180Theorem 12-5.3caucvg 15583  caucvgb 15584  caucvgbf 45526  caucvgr 15580  climcau 15575
[Gleason] p. 182Exercise 3cvgcmp 15720
[Gleason] p. 182Exercise 4cvgrat 15787
[Gleason] p. 195Theorem 13-2.12abs1m 15240
[Gleason] p. 217Lemma 13-4.1btwnzge0 13729
[Gleason] p. 223Definition 14-1.1df-met 21283
[Gleason] p. 223Definition 14-1.1(a)met0 24256  xmet0 24255
[Gleason] p. 223Definition 14-1.1(b)metgt0 24272
[Gleason] p. 223Definition 14-1.1(c)metsym 24263
[Gleason] p. 223Definition 14-1.1(d)mettri 24265  mstri 24382  xmettri 24264  xmstri 24381
[Gleason] p. 225Definition 14-1.5xpsmet 24295
[Gleason] p. 230Proposition 14-2.6txlm 23561
[Gleason] p. 240Theorem 14-4.3metcnp4 25235
[Gleason] p. 240Proposition 14-4.2metcnp3 24453
[Gleason] p. 243Proposition 14-4.16addcn 24779  addcn2 15498  mulcn 24781  mulcn2 15500  subcn 24780  subcn2 15499
[Gleason] p. 295Remarkbcval3 14210  bcval4 14211
[Gleason] p. 295Equation 2bcpasc 14225
[Gleason] p. 295Definition of binomial coefficientbcval 14208  df-bc 14207
[Gleason] p. 296Remarkbcn0 14214  bcnn 14216
[Gleason] p. 296Theorem 15-2.8binom 15734
[Gleason] p. 308Equation 2ef0 15995
[Gleason] p. 308Equation 3efcj 15996
[Gleason] p. 309Corollary 15-4.3efne0 16002
[Gleason] p. 309Corollary 15-4.4efexp 16007
[Gleason] p. 310Equation 14sinadd 16070
[Gleason] p. 310Equation 15cosadd 16071
[Gleason] p. 311Equation 17sincossq 16082
[Gleason] p. 311Equation 18cosbnd 16087  sinbnd 16086
[Gleason] p. 311Lemma 15-4.7sqeqor 14120  sqeqori 14118
[Gleason] p. 311Definition of ` `df-pi 15976
[Godowski] p. 730Equation SFgoeqi 32248
[GodowskiGreechie] p. 249Equation IV3oai 31643
[Golan] p. 1Remarksrgisid 20125
[Golan] p. 1Definitiondf-srg 20103
[Golan] p. 149Definitiondf-slmd 33165
[Gonshor] p. 7Definitiondf-scut 27721
[Gonshor] p. 9Theorem 2.5slerec 27758  slerecd 27759
[Gonshor] p. 10Theorem 2.6cofcut1 27862  cofcut1d 27863
[Gonshor] p. 10Theorem 2.7cofcut2 27864  cofcut2d 27865
[Gonshor] p. 12Theorem 2.9cofcutr 27866  cofcutr1d 27867  cofcutr2d 27868
[Gonshor] p. 13Definitiondf-adds 27901
[Gonshor] p. 14Theorem 3.1addsprop 27917
[Gonshor] p. 15Theorem 3.2addsunif 27943
[Gonshor] p. 17Theorem 3.4mulsprop 28067
[Gonshor] p. 18Theorem 3.5mulsunif 28087
[Gonshor] p. 28Lemma 4.2halfcut 28376
[Gonshor] p. 28Theorem 4.2pw2cut 28378
[Gonshor] p. 30Theorem 4.2addhalfcut 28377
[Gonshor] p. 95Theorem 6.1addsbday 27958
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36192
[Gratzer] p. 23Section 0.6df-mre 17485
[Gratzer] p. 27Section 0.6df-mri 17487
[Hall] p. 1Section 1.1df-asslaw 48218  df-cllaw 48216  df-comlaw 48217
[Hall] p. 2Section 1.2df-clintop 48230
[Hall] p. 7Section 1.3df-sgrp2 48251
[Halmos] p. 28Partition ` `df-parts 38802  dfmembpart2 38807
[Halmos] p. 31Theorem 17.3riesz1 32040  riesz2 32041
[Halmos] p. 41Definition of Hermitianhmopadj2 31916
[Halmos] p. 42Definition of projector orderingpjordi 32148
[Halmos] p. 43Theorem 26.1elpjhmop 32160  elpjidm 32159  pjnmopi 32123
[Halmos] p. 44Remarkpjinormi 31662  pjinormii 31651
[Halmos] p. 44Theorem 26.2elpjch 32164  pjrn 31682  pjrni 31677  pjvec 31671
[Halmos] p. 44Theorem 26.3pjnorm2 31702
[Halmos] p. 44Theorem 26.4hmopidmpj 32129  hmopidmpji 32127
[Halmos] p. 45Theorem 27.1pjinvari 32166
[Halmos] p. 45Theorem 27.3pjoci 32155  pjocvec 31672
[Halmos] p. 45Theorem 27.4pjorthcoi 32144
[Halmos] p. 48Theorem 29.2pjssposi 32147
[Halmos] p. 48Theorem 29.3pjssdif1i 32150  pjssdif2i 32149
[Halmos] p. 50Definition of spectrumdf-spec 31830
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1796
[Hatcher] p. 25Definitiondf-phtpc 24916  df-phtpy 24895
[Hatcher] p. 26Definitiondf-pco 24930  df-pi1 24933
[Hatcher] p. 26Proposition 1.2phtpcer 24919
[Hatcher] p. 26Proposition 1.3pi1grp 24975
[Hefferon] p. 240Definition 3.12df-dmat 22403  df-dmatalt 48429
[Helfgott] p. 2Theoremtgoldbach 47847
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47832
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47844  bgoldbtbnd 47839  bgoldbtbnd 47839  tgblthelfgott 47845
[Helfgott] p. 5Proposition 1.1circlevma 34650
[Helfgott] p. 69Statement 7.49circlemethhgt 34651
[Helfgott] p. 69Statement 7.50hgt750lema 34665  hgt750lemb 34664  hgt750leme 34666  hgt750lemf 34661  hgt750lemg 34662
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47841  tgoldbachgt 34671  tgoldbachgtALTV 47842  tgoldbachgtd 34670
[Helfgott] p. 70Statement 7.49ax-hgt749 34652
[Herstein] p. 54Exercise 28df-grpo 30468
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18854  grpoideu 30484  mndideu 18650
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18884  grpoinveu 30494
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18915  grpo2inv 30506
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18928  grpoinvop 30508
[Herstein] p. 57Exercise 1dfgrp3e 18950
[Hitchcock] p. 5Rule A3mptnan 1769
[Hitchcock] p. 5Rule A4mptxor 1770
[Hitchcock] p. 5Rule A5mtpxor 1772
[Holland] p. 1519Theorem 2sumdmdi 32395
[Holland] p. 1520Lemma 5cdj1i 32408  cdj3i 32416  cdj3lem1 32409  cdjreui 32407
[Holland] p. 1524Lemma 7mddmdin0i 32406
[Holland95] p. 13Theorem 3.6hlathil 41999
[Holland95] p. 14Line 15hgmapvs 41929
[Holland95] p. 14Line 16hdmaplkr 41951
[Holland95] p. 14Line 17hdmapellkr 41952
[Holland95] p. 14Line 19hdmapglnm2 41949
[Holland95] p. 14Line 20hdmapip0com 41955
[Holland95] p. 14Theorem 3.6hdmapevec2 41874
[Holland95] p. 14Lines 24 and 25hdmapoc 41969
[Holland95] p. 204Definition of involutiondf-srng 20753
[Holland95] p. 212Definition of subspacedf-psubsp 39541
[Holland95] p. 214Lemma 3.3lclkrlem2v 41566
[Holland95] p. 214Definition 3.2df-lpolN 41519
[Holland95] p. 214Definition of nonsingularpnonsingN 39971
[Holland95] p. 215Lemma 3.3(1)dihoml4 41415  poml4N 39991
[Holland95] p. 215Lemma 3.3(2)dochexmid 41506  pexmidALTN 40016  pexmidN 40007
[Holland95] p. 218Theorem 3.6lclkr 41571
[Holland95] p. 218Definition of dual vector spacedf-ldual 39162  ldualset 39163
[Holland95] p. 222Item 1df-lines 39539  df-pointsN 39540
[Holland95] p. 222Item 2df-polarityN 39941
[Holland95] p. 223Remarkispsubcl2N 39985  omllaw4 39284  pol1N 39948  polcon3N 39955
[Holland95] p. 223Definitiondf-psubclN 39973
[Holland95] p. 223Equation for polaritypolval2N 39944
[Holmes] p. 40Definitiondf-xrn 38398
[Hughes] p. 44Equation 1.21bax-his3 31059
[Hughes] p. 47Definition of projection operatordfpjop 32157
[Hughes] p. 49Equation 1.30eighmre 31938  eigre 31810  eigrei 31809
[Hughes] p. 49Equation 1.31eighmorth 31939  eigorth 31813  eigorthi 31812
[Hughes] p. 137Remark (ii)eigposi 31811
[Huneke] p. 1Claim 1frgrncvvdeq 30284
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30280
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30281
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30282
[Huneke] p. 2Claim 2frgrregorufr 30300  frgrregorufr0 30299  frgrregorufrg 30301
[Huneke] p. 2Claim 3frgrhash2wsp 30307  frrusgrord 30316  frrusgrord0 30315
[Huneke] p. 2Statementdf-clwwlknon 30063
[Huneke] p. 2Statement 4frgrwopreglem4 30290
[Huneke] p. 2Statement 5frgrwopreg1 30293  frgrwopreg2 30294  frgrwopregasn 30291  frgrwopregbsn 30292
[Huneke] p. 2Statement 6frgrwopreglem5 30296
[Huneke] p. 2Statement 7fusgreghash2wspv 30310
[Huneke] p. 2Statement 8fusgreghash2wsp 30313
[Huneke] p. 2Statement 9clwlksndivn 30061  numclwlk1 30346  numclwlk1lem1 30344  numclwlk1lem2 30345  numclwwlk1 30336  numclwwlk8 30367
[Huneke] p. 2Definition 3frgrwopreglem1 30287
[Huneke] p. 2Definition 4df-clwlks 29747
[Huneke] p. 2Definition 62clwwlk 30322
[Huneke] p. 2Definition 7numclwwlkovh 30348  numclwwlkovh0 30347
[Huneke] p. 2Statement 10numclwwlk2 30356
[Huneke] p. 2Statement 11rusgrnumwlkg 29953
[Huneke] p. 2Statement 12numclwwlk3 30360
[Huneke] p. 2Statement 13numclwwlk5 30363
[Huneke] p. 2Statement 14numclwwlk7 30366
[Indrzejczak] p. 33Definition ` `Enatded 30378  natded 30378
[Indrzejczak] p. 33Definition ` `Inatded 30378
[Indrzejczak] p. 34Definition ` `Enatded 30378  natded 30378
[Indrzejczak] p. 34Definition ` `Inatded 30378
[Jech] p. 4Definition of classcv 1540  cvjust 2725
[Jech] p. 42Lemma 6.1alephexp1 10467
[Jech] p. 42Equation 6.1alephadd 10465  alephmul 10466
[Jech] p. 43Lemma 6.2infmap 10464  infmap2 10105
[Jech] p. 71Lemma 9.3jech9.3 9704
[Jech] p. 72Equation 9.3scott0 9776  scottex 9775
[Jech] p. 72Exercise 9.1rankval4 9757  rankval4b 35104
[Jech] p. 72Scheme "Collection Principle"cp 9781
[Jech] p. 78Noteopthprc 5680
[JonesMatijasevic] p. 694Definition 2.3rmxyval 42947
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43035
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43036
[JonesMatijasevic] p. 695Equation 2.7rmxadd 42959
[JonesMatijasevic] p. 695Equation 2.8rmyadd 42963
[JonesMatijasevic] p. 695Equation 2.9rmxp1 42964  rmyp1 42965
[JonesMatijasevic] p. 695Equation 2.10rmxm1 42966  rmym1 42967
[JonesMatijasevic] p. 695Equation 2.11rmx0 42957  rmx1 42958  rmxluc 42968
[JonesMatijasevic] p. 695Equation 2.12rmy0 42961  rmy1 42962  rmyluc 42969
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 42971
[JonesMatijasevic] p. 695Equation 2.14rmydbl 42972
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42992  jm2.17b 42993  jm2.17c 42994
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43025
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43029
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43020
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42995  jm2.24nn 42991
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43034
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43040  rmygeid 42996
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43052
[Juillerat] p. 11Section *5etransc 46320  etransclem47 46318  etransclem48 46319
[Juillerat] p. 12Equation (7)etransclem44 46315
[Juillerat] p. 12Equation *(7)etransclem46 46317
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46303
[Juillerat] p. 13Proofetransclem35 46306
[Juillerat] p. 13Part of case 2 proven inetransclem38 46309
[Juillerat] p. 13Part of case 2 provenetransclem24 46295
[Juillerat] p. 13Part of case 2: proven inetransclem41 46312
[Juillerat] p. 14Proofetransclem23 46294
[KalishMontague] p. 81Note 1ax-6 1968
[KalishMontague] p. 85Lemma 2equid 2013
[KalishMontague] p. 85Lemma 3equcomi 2018
[KalishMontague] p. 86Lemma 7cbvalivw 2008  cbvaliw 2007  wl-cbvmotv 37546  wl-motae 37548  wl-moteq 37547
[KalishMontague] p. 87Lemma 8spimvw 1987  spimw 1971
[KalishMontague] p. 87Lemma 9spfw 2034  spw 2035
[Kalmbach] p. 14Definition of latticechabs1 31491  chabs1i 31493  chabs2 31492  chabs2i 31494  chjass 31508  chjassi 31461  latabs1 18378  latabs2 18379
[Kalmbach] p. 15Definition of atomdf-at 32313  ela 32314
[Kalmbach] p. 15Definition of coverscvbr2 32258  cvrval2 39312
[Kalmbach] p. 16Definitiondf-ol 39216  df-oml 39217
[Kalmbach] p. 20Definition of commutescmbr 31559  cmbri 31565  cmtvalN 39249  df-cm 31558  df-cmtN 39215
[Kalmbach] p. 22Remarkomllaw5N 39285  pjoml5 31588  pjoml5i 31563
[Kalmbach] p. 22Definitionpjoml2 31586  pjoml2i 31560
[Kalmbach] p. 22Theorem 2(v)cmcm 31589  cmcmi 31567  cmcmii 31572  cmtcomN 39287
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39283  omlsi 31379  pjoml 31411  pjomli 31410
[Kalmbach] p. 22Definition of OML lawomllaw2N 39282
[Kalmbach] p. 23Remarkcmbr2i 31571  cmcm3 31590  cmcm3i 31569  cmcm3ii 31574  cmcm4i 31570  cmt3N 39289  cmt4N 39290  cmtbr2N 39291
[Kalmbach] p. 23Lemma 3cmbr3 31583  cmbr3i 31575  cmtbr3N 39292
[Kalmbach] p. 25Theorem 5fh1 31593  fh1i 31596  fh2 31594  fh2i 31597  omlfh1N 39296
[Kalmbach] p. 65Remarkchjatom 32332  chslej 31473  chsleji 31433  shslej 31355  shsleji 31345
[Kalmbach] p. 65Proposition 1chocin 31470  chocini 31429  chsupcl 31315  chsupval2 31385  h0elch 31230  helch 31218  hsupval2 31384  ocin 31271  ococss 31268  shococss 31269
[Kalmbach] p. 65Definition of subspace sumshsval 31287
[Kalmbach] p. 66Remarkdf-pjh 31370  pjssmi 32140  pjssmii 31656
[Kalmbach] p. 67Lemma 3osum 31620  osumi 31617
[Kalmbach] p. 67Lemma 4pjci 32175
[Kalmbach] p. 103Exercise 6atmd2 32375
[Kalmbach] p. 103Exercise 12mdsl0 32285
[Kalmbach] p. 140Remarkhatomic 32335  hatomici 32334  hatomistici 32337
[Kalmbach] p. 140Proposition 1atlatmstc 39357
[Kalmbach] p. 140Proposition 1(i)atexch 32356  lsatexch 39081
[Kalmbach] p. 140Proposition 1(ii)chcv1 32330  cvlcvr1 39377  cvr1 39448
[Kalmbach] p. 140Proposition 1(iii)cvexch 32349  cvexchi 32344  cvrexch 39458
[Kalmbach] p. 149Remark 2chrelati 32339  hlrelat 39440  hlrelat5N 39439  lrelat 39052
[Kalmbach] p. 153Exercise 5lsmcv 21076  lsmsatcv 39048  spansncv 31628  spansncvi 31627
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39067  spansncv2 32268
[Kalmbach] p. 266Definitiondf-st 32186
[Kalmbach2] p. 8Definition of adjointdf-adjh 31824
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10534  fpwwe2 10531
[KanamoriPincus] p. 416Corollary 1.3canth4 10535
[KanamoriPincus] p. 417Corollary 1.6canthp1 10542
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10537
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10539
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10552
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10556  gchxpidm 10557
[KanamoriPincus] p. 419Theorem 2.1gchacg 10568  gchhar 10567
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10103  unxpwdom 9475
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10558
[Kreyszig] p. 3Property M1metcl 24245  xmetcl 24244
[Kreyszig] p. 4Property M2meteq0 24252
[Kreyszig] p. 8Definition 1.1-8dscmet 24485
[Kreyszig] p. 12Equation 5conjmul 11835  muleqadd 11758
[Kreyszig] p. 18Definition 1.3-2mopnval 24351
[Kreyszig] p. 19Remarkmopntopon 24352
[Kreyszig] p. 19Theorem T1mopn0 24411  mopnm 24357
[Kreyszig] p. 19Theorem T2unimopn 24409
[Kreyszig] p. 19Definition of neighborhoodneibl 24414
[Kreyszig] p. 20Definition 1.3-3metcnp2 24455
[Kreyszig] p. 25Definition 1.4-1lmbr 23171  lmmbr 25183  lmmbr2 25184
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23293
[Kreyszig] p. 28Theorem 1.4-5lmcau 25238
[Kreyszig] p. 28Definition 1.4-3iscau 25201  iscmet2 25219
[Kreyszig] p. 30Theorem 1.4-7cmetss 25241
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23374  metelcls 25230
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25231  metcld2 25232
[Kreyszig] p. 51Equation 2clmvneg1 25024  lmodvneg1 20836  nvinv 30614  vcm 30551
[Kreyszig] p. 51Equation 1aclm0vs 25020  lmod0vs 20826  slmd0vs 33188  vc0 30549
[Kreyszig] p. 51Equation 1blmodvs0 20827  slmdvs0 33189  vcz 30550
[Kreyszig] p. 58Definition 2.2-1imsmet 30666  ngpmet 24516  nrmmetd 24487
[Kreyszig] p. 59Equation 1imsdval 30661  imsdval2 30662  ncvspds 25086  ngpds 24517
[Kreyszig] p. 63Problem 1nmval 24502  nvnd 30663
[Kreyszig] p. 64Problem 2nmeq0 24531  nmge0 24530  nvge0 30648  nvz 30644
[Kreyszig] p. 64Problem 3nmrtri 24537  nvabs 30647
[Kreyszig] p. 91Definition 2.7-1isblo3i 30776
[Kreyszig] p. 92Equation 2df-nmoo 30720
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30782  blocni 30780
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30781
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25129  ipeq0 21573  ipz 30694
[Kreyszig] p. 135Problem 2cphpyth 25141  pythi 30825
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30829
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25163
[Kreyszig] p. 144Equation 4supcvg 15760
[Kreyszig] p. 144Theorem 3.3-1minvec 25361  minveco 30859
[Kreyszig] p. 196Definition 3.9-1df-aj 30725
[Kreyszig] p. 247Theorem 4.7-2bcth 25254
[Kreyszig] p. 249Theorem 4.7-3ubth 30848
[Kreyszig] p. 470Definition of positive operator orderingleop 32098  leopg 32097
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32116
[Kreyszig] p. 525Theorem 10.1-1htth 30893
[Kulpa] p. 547Theorempoimir 37692
[Kulpa] p. 547Equation (1)poimirlem32 37691
[Kulpa] p. 547Equation (2)poimirlem31 37690
[Kulpa] p. 548Theorembroucube 37693
[Kulpa] p. 548Equation (6)poimirlem26 37685
[Kulpa] p. 548Equation (7)poimirlem27 37686
[Kunen] p. 10Axiom 0ax6e 2383  axnul 5243
[Kunen] p. 11Axiom 3axnul 5243
[Kunen] p. 12Axiom 6zfrep6 7887
[Kunen] p. 24Definition 10.24mapval 8762  mapvalg 8760
[Kunen] p. 30Lemma 10.20fodomg 10410
[Kunen] p. 31Definition 10.24mapex 7871
[Kunen] p. 95Definition 2.1df-r1 9654
[Kunen] p. 97Lemma 2.10r1elss 9696  r1elssi 9695
[Kunen] p. 107Exercise 4rankop 9748  rankopb 9742  rankuni 9753  rankxplim 9769  rankxpsuc 9772
[Kunen2] p. 47Lemma I.9.9relpfr 44986
[Kunen2] p. 53Lemma I.9.21trfr 44994
[Kunen2] p. 53Lemma I.9.24(2)wffr 44993
[Kunen2] p. 53Definition I.9.20tcfr 44995
[Kunen2] p. 95Lemma I.16.2ralabso 45000  rexabso 45001
[Kunen2] p. 96Example I.16.3disjabso 45007  n0abso 45008  ssabso 45006
[Kunen2] p. 111Lemma II.2.4(1)traxext 45009
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45019
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45014
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45017
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45018
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45013
[Kunen2] p. 112Corollary II.2.5wfaxext 45025  wfaxpr 45030  wfaxreg 45032  wfaxrep 45026  wfaxsep 45027  wfaxun 45031
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45016
[Kunen2] p. 113Corollary II.2.9wfaxpow 45029
[Kunen2] p. 114Theorem II.2.13wfaxext 45025
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45024  omelaxinf2 45021
[Kunen2] p. 114Corollary II.2.12wfac8prim 45034  wfaxinf2 45033
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45047  permaxext 45037  permaxinf2 45045  permaxnul 45040  permaxpow 45041  permaxpr 45042  permaxrep 45038  permaxsep 45039  permaxun 45043
[Kunen2] p. 148Definition II.9.1brpermmodel 45035
[Kunen2] p. 149Exercise II.9.3permac8prim 45046
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4954
[Lang] , p. 225Corollary 1.3finexttrb 33673
[Lang] p. Definitiondf-rn 5627
[Lang] p. 3Statementlidrideqd 18574  mndbn0 18655
[Lang] p. 3Definitiondf-mnd 18640
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18592
[Lang] p. 4Property of composites. Second formulagsumccat 18746
[Lang] p. 5Equationgsumreidx 19827
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48212
[Lang] p. 6Examplenn0mnd 48209
[Lang] p. 6Equationgsumxp2 19890
[Lang] p. 6Statementcycsubm 19112
[Lang] p. 6Definitionmulgnn0gsum 18990
[Lang] p. 6Observationmndlsmidm 19580
[Lang] p. 7Definitiondfgrp2e 18873
[Lang] p. 30Definitiondf-tocyc 33071
[Lang] p. 32Property (a)cyc3genpm 33116
[Lang] p. 32Property (b)cyc3conja 33121  cycpmconjv 33106
[Lang] p. 53Definitiondf-cat 17571
[Lang] p. 53Axiom CAT 1cat1 18001  cat1lem 18000
[Lang] p. 54Definitiondf-iso 17653
[Lang] p. 57Definitiondf-inito 17888  df-termo 17889
[Lang] p. 58Exampleirinitoringc 21414
[Lang] p. 58Statementinitoeu1 17915  termoeu1 17922
[Lang] p. 62Definitiondf-func 17762
[Lang] p. 65Definitiondf-nat 17850
[Lang] p. 91Notedf-ringc 20559
[Lang] p. 92Statementmxidlprm 33430
[Lang] p. 92Definitionisprmidlc 33407
[Lang] p. 128Remarkdsmmlmod 21680
[Lang] p. 129Prooflincscm 48461  lincscmcl 48463  lincsum 48460  lincsumcl 48462
[Lang] p. 129Statementlincolss 48465
[Lang] p. 129Observationdsmmfi 21673
[Lang] p. 141Theorem 5.3dimkerim 33635  qusdimsum 33636
[Lang] p. 141Corollary 5.4lssdimle 33615
[Lang] p. 147Definitionsnlindsntor 48502
[Lang] p. 504Statementmat1 22360  matring 22356
[Lang] p. 504Definitiondf-mamu 22304
[Lang] p. 505Statementmamuass 22315  mamutpos 22371  matassa 22357  mattposvs 22368  tposmap 22370
[Lang] p. 513Definitionmdet1 22514  mdetf 22508
[Lang] p. 513Theorem 4.4cramer 22604
[Lang] p. 514Proposition 4.6mdetleib 22500
[Lang] p. 514Proposition 4.8mdettpos 22524
[Lang] p. 515Definitiondf-minmar1 22548  smadiadetr 22588
[Lang] p. 515Corollary 4.9mdetero 22523  mdetralt 22521
[Lang] p. 517Proposition 4.15mdetmul 22536
[Lang] p. 518Definitiondf-madu 22547
[Lang] p. 518Proposition 4.16madulid 22558  madurid 22557  matinv 22590
[Lang] p. 561Theorem 3.1cayleyhamilton 22803
[Lang], p. 224Proposition 1.1extdgfialg 33702  finextalg 33706
[Lang], p. 224Proposition 1.2extdgmul 33671  fedgmul 33639
[Lang], p. 225Proposition 1.4algextdeg 33733
[Lang], p. 561Remarkchpmatply1 22745
[Lang], p. 561Definitiondf-chpmat 22740
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44366
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44361
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44367
[LeBlanc] p. 277Rule R2axnul 5243
[Levy] p. 12Axiom 4.3.1df-clab 2710
[Levy] p. 59Definitiondf-ttrcl 9598
[Levy] p. 64Theorem 5.6(ii)frinsg 9641
[Levy] p. 338Axiomdf-clel 2806  df-cleq 2723
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2806  df-cleq 2723
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2710
[Levy] p. 358Axiomdf-clab 2710
[Levy58] p. 2Definition Iisfin1-3 10274
[Levy58] p. 2Definition IIdf-fin2 10174
[Levy58] p. 2Definition Iadf-fin1a 10173
[Levy58] p. 2Definition IIIdf-fin3 10176
[Levy58] p. 3Definition Vdf-fin5 10177
[Levy58] p. 3Definition IVdf-fin4 10175
[Levy58] p. 4Definition VIdf-fin6 10178
[Levy58] p. 4Definition VIIdf-fin7 10179
[Levy58], p. 3Theorem 1fin1a2 10303
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27623
[Lipparini] p. 3Lemma 2.1.4noresle 27634
[Lipparini] p. 6Proposition 4.2noinfbnd1 27666  nosupbnd1 27651
[Lipparini] p. 6Proposition 4.3noinfbnd2 27668  nosupbnd2 27653
[Lipparini] p. 7Theorem 5.1noetasuplem3 27672  noetasuplem4 27673
[Lipparini] p. 7Corollary 4.4nosupinfsep 27669
[Lopez-Astorga] p. 12Rule 1mptnan 1769
[Lopez-Astorga] p. 12Rule 2mptxor 1770
[Lopez-Astorga] p. 12Rule 3mtpxor 1772
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32383
[Maeda] p. 168Lemma 5mdsym 32387  mdsymi 32386
[Maeda] p. 168Lemma 4(i)mdsymlem4 32381  mdsymlem6 32383  mdsymlem7 32384
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32385
[MaedaMaeda] p. 1Remarkssdmd1 32288  ssdmd2 32289  ssmd1 32286  ssmd2 32287
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32284
[MaedaMaeda] p. 1Definition 1.1df-dmd 32256  df-md 32255  mdbr 32269
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32306  mdslj1i 32294  mdslj2i 32295  mdslle1i 32292  mdslle2i 32293  mdslmd1i 32304  mdslmd2i 32305
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32296  mdsl2bi 32298  mdsl2i 32297
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32310
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32307
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32308
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32285
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32290  mdsl3 32291
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32309
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32404
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39359  hlrelat1 39438
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39077
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32311  cvmdi 32299  cvnbtwn4 32264  cvrnbtwn4 39317
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32312
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39378  cvp 32350  cvrp 39454  lcvp 39078
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32374
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32373
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39371  hlexch4N 39430
[MaedaMaeda] p. 34Exercise 7.1atabsi 32376
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39481
[MaedaMaeda] p. 61Definition 15.10psubN 39787  atpsubN 39791  df-pointsN 39540  pointpsubN 39789
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39542  pmap11 39800  pmaple 39799  pmapsub 39806  pmapval 39795
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39803  pmap1N 39805
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39808  pmapglb2N 39809  pmapglb2xN 39810  pmapglbx 39807
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39890
[MaedaMaeda] p. 67Postulate PS1ps-1 39515
[MaedaMaeda] p. 68Lemma 16.2df-padd 39834  paddclN 39880  paddidm 39879
[MaedaMaeda] p. 68Condition PS2ps-2 39516
[MaedaMaeda] p. 68Equation 16.2.1paddass 39876
[MaedaMaeda] p. 69Lemma 16.4ps-1 39515
[MaedaMaeda] p. 69Theorem 16.4ps-2 39516
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19585  lsmmod2 19586  lssats 39050  shatomici 32333  shatomistici 32336  shmodi 31365  shmodsi 31364
[MaedaMaeda] p. 130Remark 29.6dmdmd 32275  mdsymlem7 32384
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31564
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31468
[MaedaMaeda] p. 139Remarksumdmdii 32390
[Margaris] p. 40Rule Cexlimiv 1931
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 396  df-ex 1781  df-or 848  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30375
[Margaris] p. 59Section 14notnotrALTVD 44946
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 44947
[Margaris] p. 79Rule Cexinst01 44657  exinst11 44658
[Margaris] p. 89Theorem 19.219.2 1977  19.2g 2191  r19.2z 4445
[Margaris] p. 89Theorem 19.319.3 2205  rr19.3v 3622
[Margaris] p. 89Theorem 19.5alcom 2162
[Margaris] p. 89Theorem 19.6alex 1827
[Margaris] p. 89Theorem 19.7alnex 1782
[Margaris] p. 89Theorem 19.819.8a 2184
[Margaris] p. 89Theorem 19.919.9 2208  19.9h 2288  exlimd 2221  exlimdh 2292
[Margaris] p. 89Theorem 19.11excom 2165  excomim 2166
[Margaris] p. 89Theorem 19.1219.12 2328
[Margaris] p. 90Section 19conventions-labels 30376  conventions-labels 30376  conventions-labels 30376  conventions-labels 30376
[Margaris] p. 90Theorem 19.14exnal 1828
[Margaris] p. 90Theorem 19.152albi 44410  albi 1819
[Margaris] p. 90Theorem 19.1619.16 2228
[Margaris] p. 90Theorem 19.1719.17 2229
[Margaris] p. 90Theorem 19.182exbi 44412  exbi 1848
[Margaris] p. 90Theorem 19.1919.19 2232
[Margaris] p. 90Theorem 19.202alim 44409  2alimdv 1919  alimd 2215  alimdh 1818  alimdv 1917  ax-4 1810  ralimdaa 3233  ralimdv 3146  ralimdva 3144  ralimdvva 3179  sbcimdv 3810
[Margaris] p. 90Theorem 19.2119.21 2210  19.21h 2289  19.21t 2209  19.21vv 44408  alrimd 2218  alrimdd 2217  alrimdh 1864  alrimdv 1930  alrimi 2216  alrimih 1825  alrimiv 1928  alrimivv 1929  hbralrimi 3122  r19.21be 3225  r19.21bi 3224  ralrimd 3237  ralrimdv 3130  ralrimdva 3132  ralrimdvv 3176  ralrimdvva 3187  ralrimi 3230  ralrimia 3231  ralrimiv 3123  ralrimiva 3124  ralrimivv 3173  ralrimivva 3175  ralrimivvva 3178  ralrimivw 3128
[Margaris] p. 90Theorem 19.222exim 44411  2eximdv 1920  exim 1835  eximd 2219  eximdh 1865  eximdv 1918  rexim 3073  reximd2a 3242  reximdai 3234  reximdd 45184  reximddv 3148  reximddv2 3191  reximddv3 3149  reximdv 3147  reximdv2 3142  reximdva 3145  reximdvai 3143  reximdvva 3180  reximi2 3065
[Margaris] p. 90Theorem 19.2319.23 2214  19.23bi 2194  19.23h 2290  19.23t 2213  exlimdv 1934  exlimdvv 1935  exlimexi 44556  exlimiv 1931  exlimivv 1933  rexlimd3 45180  rexlimdv 3131  rexlimdv3a 3137  rexlimdva 3133  rexlimdva2 3135  rexlimdvaa 3134  rexlimdvv 3188  rexlimdvva 3189  rexlimdvvva 3190  rexlimdvw 3138  rexlimiv 3126  rexlimiva 3125  rexlimivv 3174
[Margaris] p. 90Theorem 19.2419.24 1992
[Margaris] p. 90Theorem 19.2519.25 1881
[Margaris] p. 90Theorem 19.2619.26 1871
[Margaris] p. 90Theorem 19.2719.27 2230  r19.27z 4455  r19.27zv 4456
[Margaris] p. 90Theorem 19.2819.28 2231  19.28vv 44418  r19.28z 4448  r19.28zf 45195  r19.28zv 4451  rr19.28v 3623
[Margaris] p. 90Theorem 19.2919.29 1874  r19.29d2r 3119  r19.29imd 3097
[Margaris] p. 90Theorem 19.3019.30 1882
[Margaris] p. 90Theorem 19.3119.31 2237  19.31vv 44416
[Margaris] p. 90Theorem 19.3219.32 2236  r19.32 47128
[Margaris] p. 90Theorem 19.3319.33-2 44414  19.33 1885
[Margaris] p. 90Theorem 19.3419.34 1993
[Margaris] p. 90Theorem 19.3519.35 1878
[Margaris] p. 90Theorem 19.3619.36 2233  19.36vv 44415  r19.36zv 4457
[Margaris] p. 90Theorem 19.3719.37 2235  19.37vv 44417  r19.37zv 4452
[Margaris] p. 90Theorem 19.3819.38 1840
[Margaris] p. 90Theorem 19.3919.39 1991
[Margaris] p. 90Theorem 19.4019.40-2 1888  19.40 1887  r19.40 3098
[Margaris] p. 90Theorem 19.4119.41 2238  19.41rg 44582
[Margaris] p. 90Theorem 19.4219.42 2239
[Margaris] p. 90Theorem 19.4319.43 1883
[Margaris] p. 90Theorem 19.4419.44 2240  r19.44zv 4454
[Margaris] p. 90Theorem 19.4519.45 2241  r19.45zv 4453
[Margaris] p. 110Exercise 2(b)eu1 2605
[Mayet] p. 370Remarkjpi 32245  largei 32242  stri 32232
[Mayet3] p. 9Definition of CH-statesdf-hst 32187  ishst 32189
[Mayet3] p. 10Theoremhstrbi 32241  hstri 32240
[Mayet3] p. 1223Theorem 4.1mayete3i 31703
[Mayet3] p. 1240Theorem 7.1mayetes3i 31704
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32253
[MegPav2000] p. 2345Definition 3.4-1chintcl 31307  chsupcl 31315
[MegPav2000] p. 2345Definition 3.4-2hatomic 32335
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32329
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32356
[MegPav2000] p. 2366Figure 7pl42N 40021
[MegPav2002] p. 362Lemma 2.2latj31 18390  latj32 18388  latjass 18386
[Megill] p. 444Axiom C5ax-5 1911  ax5ALT 38945
[Megill] p. 444Section 7conventions 30375
[Megill] p. 445Lemma L12aecom-o 38939  ax-c11n 38926  axc11n 2426
[Megill] p. 446Lemma L17equtrr 2023
[Megill] p. 446Lemma L18ax6fromc10 38934
[Megill] p. 446Lemma L19hbnae-o 38966  hbnae 2432
[Megill] p. 447Remark 9.1dfsb1 2481  sbid 2258  sbidd-misc 49750  sbidd 49749
[Megill] p. 448Remark 9.6axc14 2463
[Megill] p. 448Scheme C4'ax-c4 38922
[Megill] p. 448Scheme C5'ax-c5 38921  sp 2186
[Megill] p. 448Scheme C6'ax-11 2160
[Megill] p. 448Scheme C7'ax-c7 38923
[Megill] p. 448Scheme C8'ax-7 2009
[Megill] p. 448Scheme C9'ax-c9 38928
[Megill] p. 448Scheme C10'ax-6 1968  ax-c10 38924
[Megill] p. 448Scheme C11'ax-c11 38925
[Megill] p. 448Scheme C12'ax-8 2113
[Megill] p. 448Scheme C13'ax-9 2121
[Megill] p. 448Scheme C14'ax-c14 38929
[Megill] p. 448Scheme C15'ax-c15 38927
[Megill] p. 448Scheme C16'ax-c16 38930
[Megill] p. 448Theorem 9.4dral1-o 38942  dral1 2439  dral2-o 38968  dral2 2438  drex1 2441  drex2 2442  drsb1 2495  drsb2 2269
[Megill] p. 449Theorem 9.7sbcom2 2176  sbequ 2086  sbid2v 2509
[Megill] p. 450Example in Appendixhba1-o 38935  hba1 2295
[Mendelson] p. 35Axiom A3hirstL-ax3 46922
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3830  rspsbca 3831  stdpc4 2071
[Mendelson] p. 69Axiom 5ax-c4 38922  ra4 3837  stdpc5 2211
[Mendelson] p. 81Rule Cexlimiv 1931
[Mendelson] p. 95Axiom 6stdpc6 2029
[Mendelson] p. 95Axiom 7stdpc7 2253
[Mendelson] p. 225Axiom system NBGru 3739
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5454
[Mendelson] p. 231Exercise 4.10(k)inv1 4348
[Mendelson] p. 231Exercise 4.10(l)unv 4349
[Mendelson] p. 231Exercise 4.10(n)dfin3 4227
[Mendelson] p. 231Exercise 4.10(o)df-nul 4284
[Mendelson] p. 231Exercise 4.10(q)dfin4 4228
[Mendelson] p. 231Exercise 4.10(s)ddif 4091
[Mendelson] p. 231Definition of uniondfun3 4226
[Mendelson] p. 235Exercise 4.12(c)univ 5392
[Mendelson] p. 235Exercise 4.12(d)pwv 4856
[Mendelson] p. 235Exercise 4.12(j)pwin 5507
[Mendelson] p. 235Exercise 4.12(k)pwunss 4568
[Mendelson] p. 235Exercise 4.12(l)pwssun 5508
[Mendelson] p. 235Exercise 4.12(n)uniin 4883
[Mendelson] p. 235Exercise 4.12(p)reli 5766
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6216
[Mendelson] p. 244Proposition 4.8(g)epweon 7708
[Mendelson] p. 246Definition of successordf-suc 6312
[Mendelson] p. 250Exercise 4.36oelim2 8510
[Mendelson] p. 254Proposition 4.22(b)xpen 9053
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8974  xpsneng 8975
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8981  xpcomeng 8982
[Mendelson] p. 254Proposition 4.22(e)xpassen 8984
[Mendelson] p. 255Definitionbrsdom 8897
[Mendelson] p. 255Exercise 4.39endisj 8977
[Mendelson] p. 255Exercise 4.41mapprc 8754
[Mendelson] p. 255Exercise 4.43mapsnen 8959  mapsnend 8958
[Mendelson] p. 255Exercise 4.45mapunen 9059
[Mendelson] p. 255Exercise 4.47xpmapen 9058
[Mendelson] p. 255Exercise 4.42(a)map0e 8806
[Mendelson] p. 255Exercise 4.42(b)map1 8962
[Mendelson] p. 257Proposition 4.24(a)undom 8978
[Mendelson] p. 258Exercise 4.56(c)djuassen 10067  djucomen 10066
[Mendelson] p. 258Exercise 4.56(f)djudom1 10071
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10065
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8446
[Mendelson] p. 266Proposition 4.34(f)oaordex 8473
[Mendelson] p. 275Proposition 4.42(d)entri3 10447
[Mendelson] p. 281Definitiondf-r1 9654
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9703
[Mendelson] p. 287Axiom system MKru 3739
[MertziosUnger] p. 152Definitiondf-frgr 30234
[MertziosUnger] p. 153Remark 1frgrconngr 30269
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30271  vdgn1frgrv3 30272
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30273
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30266
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30259  2pthfrgrrn 30257  2pthfrgrrn2 30258
[Mittelstaedt] p. 9Definitiondf-oc 31227
[Monk1] p. 22Remarkconventions 30375
[Monk1] p. 22Theorem 3.1conventions 30375
[Monk1] p. 26Theorem 2.8(vii)ssin 4189
[Monk1] p. 33Theorem 3.2(i)ssrel 5723  ssrelf 32593
[Monk1] p. 33Theorem 3.2(ii)eqrel 5724
[Monk1] p. 34Definition 3.3df-opab 5154
[Monk1] p. 36Theorem 3.7(i)coi1 6210  coi2 6211
[Monk1] p. 36Theorem 3.8(v)dm0 5860  rn0 5866
[Monk1] p. 36Theorem 3.7(ii)cnvi 6088
[Monk1] p. 37Theorem 3.13(i)relxp 5634
[Monk1] p. 37Theorem 3.13(x)dmxp 5869  rnxp 6117
[Monk1] p. 37Theorem 3.13(ii)0xp 5715  xp0 6105
[Monk1] p. 38Theorem 3.16(ii)ima0 6026
[Monk1] p. 38Theorem 3.16(viii)imai 6023
[Monk1] p. 39Theorem 3.17imaex 7844  imaexg 7843
[Monk1] p. 39Theorem 3.16(xi)imassrn 6020
[Monk1] p. 41Theorem 4.3(i)fnopfv 7008  funfvop 6983
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6876
[Monk1] p. 42Theorem 4.4(iii)fvelima 6887
[Monk1] p. 43Theorem 4.6funun 6527
[Monk1] p. 43Theorem 4.8(iv)dff13 7188  dff13f 7189
[Monk1] p. 46Theorem 4.15(v)funex 7153  funrnex 7886
[Monk1] p. 50Definition 5.4fniunfv 7181
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6174
[Monk1] p. 52Theorem 5.11(viii)ssint 4914
[Monk1] p. 52Definition 5.13 (i)1stval2 7938  df-1st 7921
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7939  df-2nd 7922
[Monk1] p. 112Theorem 15.17(v)ranksn 9744  ranksnb 9717
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9745
[Monk1] p. 112Theorem 15.17(iii)rankun 9746  rankunb 9740
[Monk1] p. 113Theorem 15.18r1val3 9728
[Monk1] p. 113Definition 15.19df-r1 9654  r1val2 9727
[Monk1] p. 117Lemmazorn2 10394  zorn2g 10391
[Monk1] p. 133Theorem 18.11cardom 9876
[Monk1] p. 133Theorem 18.12canth3 10449
[Monk1] p. 133Theorem 18.14carduni 9871
[Monk2] p. 105Axiom C4ax-4 1810
[Monk2] p. 105Axiom C7ax-7 2009
[Monk2] p. 105Axiom C8ax-12 2180  ax-c15 38927  ax12v2 2182
[Monk2] p. 108Lemma 5ax-c4 38922
[Monk2] p. 109Lemma 12ax-11 2160
[Monk2] p. 109Lemma 15equvini 2455  equvinv 2030  eqvinop 5427
[Monk2] p. 113Axiom C5-1ax-5 1911  ax5ALT 38945
[Monk2] p. 113Axiom C5-2ax-10 2144
[Monk2] p. 113Axiom C5-3ax-11 2160
[Monk2] p. 114Lemma 21sp 2186
[Monk2] p. 114Lemma 22axc4 2322  hba1-o 38935  hba1 2295
[Monk2] p. 114Lemma 23nfia1 2156
[Monk2] p. 114Lemma 24nfa2 2179  nfra2 3342  nfra2w 3268
[Moore] p. 53Part Idf-mre 17485
[Munkres] p. 77Example 2distop 22908  indistop 22915  indistopon 22914
[Munkres] p. 77Example 3fctop 22917  fctop2 22918
[Munkres] p. 77Example 4cctop 22919
[Munkres] p. 78Definition of basisdf-bases 22859  isbasis3g 22862
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17344  tgval2 22869
[Munkres] p. 79Remarktgcl 22882
[Munkres] p. 80Lemma 2.1tgval3 22876
[Munkres] p. 80Lemma 2.2tgss2 22900  tgss3 22899
[Munkres] p. 81Lemma 2.3basgen 22901  basgen2 22902
[Munkres] p. 83Exercise 3topdifinf 37382  topdifinfeq 37383  topdifinffin 37381  topdifinfindis 37379
[Munkres] p. 89Definition of subspace topologyresttop 23073
[Munkres] p. 93Theorem 6.1(1)0cld 22951  topcld 22948
[Munkres] p. 93Theorem 6.1(2)iincld 22952
[Munkres] p. 93Theorem 6.1(3)uncld 22954
[Munkres] p. 94Definition of closureclsval 22950
[Munkres] p. 94Definition of interiorntrval 22949
[Munkres] p. 95Theorem 6.5(a)clsndisj 22988  elcls 22986
[Munkres] p. 95Theorem 6.5(b)elcls3 22996
[Munkres] p. 97Theorem 6.6clslp 23061  neindisj 23030
[Munkres] p. 97Corollary 6.7cldlp 23063
[Munkres] p. 97Definition of limit pointislp2 23058  lpval 23052
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23228
[Munkres] p. 102Definition of continuous functiondf-cn 23140  iscn 23148  iscn2 23151
[Munkres] p. 107Theorem 7.2(g)cncnp 23193  cncnp2 23194  cncnpi 23191  df-cnp 23141  iscnp 23150  iscnp2 23152
[Munkres] p. 127Theorem 10.1metcn 24456
[Munkres] p. 128Theorem 10.3metcn4 25236
[Nathanson] p. 123Remarkreprgt 34629  reprinfz1 34630  reprlt 34627
[Nathanson] p. 123Definitiondf-repr 34617
[Nathanson] p. 123Chapter 5.1circlemethnat 34649
[Nathanson] p. 123Propositionbreprexp 34641  breprexpnat 34642  itgexpif 34614
[NielsenChuang] p. 195Equation 4.73unierri 32079
[OeSilva] p. 2042Section 2ax-bgbltosilva 47840
[Pfenning] p. 17Definition XMnatded 30378
[Pfenning] p. 17Definition NNCnatded 30378  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30378
[Pfenning] p. 18Rule"natded 30378
[Pfenning] p. 18Definition /\Inatded 30378
[Pfenning] p. 18Definition ` `Enatded 30378  natded 30378  natded 30378  natded 30378  natded 30378
[Pfenning] p. 18Definition ` `Inatded 30378  natded 30378  natded 30378  natded 30378  natded 30378
[Pfenning] p. 18Definition ` `ELnatded 30378
[Pfenning] p. 18Definition ` `ERnatded 30378
[Pfenning] p. 18Definition ` `Ea,unatded 30378
[Pfenning] p. 18Definition ` `IRnatded 30378
[Pfenning] p. 18Definition ` `Ianatded 30378
[Pfenning] p. 127Definition =Enatded 30378
[Pfenning] p. 127Definition =Inatded 30378
[Ponnusamy] p. 361Theorem 6.44cphip0l 25127  df-dip 30676  dip0l 30693  ip0l 21571
[Ponnusamy] p. 361Equation 6.45cphipval 25168  ipval 30678
[Ponnusamy] p. 362Equation I1dipcj 30689  ipcj 21569
[Ponnusamy] p. 362Equation I3cphdir 25130  dipdir 30817  ipdir 21574  ipdiri 30805
[Ponnusamy] p. 362Equation I4ipidsq 30685  nmsq 25119
[Ponnusamy] p. 362Equation 6.46ip0i 30800
[Ponnusamy] p. 362Equation 6.47ip1i 30802
[Ponnusamy] p. 362Equation 6.48ip2i 30803
[Ponnusamy] p. 363Equation I2cphass 25136  dipass 30820  ipass 21580  ipassi 30816
[Prugovecki] p. 186Definition of brabraval 31919  df-bra 31825
[Prugovecki] p. 376Equation 8.1df-kb 31826  kbval 31929
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32357
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39926
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32371  atcvat4i 32372  cvrat3 39480  cvrat4 39481  lsatcvat3 39090
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32257  cvrval 39307  df-cv 32254  df-lcv 39057  lspsncv0 21081
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39938
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39939
[Quine] p. 16Definition 2.1df-clab 2710  rabid 3416  rabidd 45191
[Quine] p. 17Definition 2.1''dfsb7 2281
[Quine] p. 18Definition 2.7df-cleq 2723
[Quine] p. 19Definition 2.9conventions 30375  df-v 3438
[Quine] p. 34Theorem 5.1eqabb 2870
[Quine] p. 35Theorem 5.2abid1 2867  abid2f 2925
[Quine] p. 40Theorem 6.1sb5 2278
[Quine] p. 40Theorem 6.2sb6 2088  sbalex 2245
[Quine] p. 41Theorem 6.3df-clel 2806
[Quine] p. 41Theorem 6.4eqid 2731  eqid1 30442
[Quine] p. 41Theorem 6.5eqcom 2738
[Quine] p. 42Theorem 6.6df-sbc 3742
[Quine] p. 42Theorem 6.7dfsbcq 3743  dfsbcq2 3744
[Quine] p. 43Theorem 6.8vex 3440
[Quine] p. 43Theorem 6.9isset 3450
[Quine] p. 44Theorem 7.3spcgf 3546  spcgv 3551  spcimgf 3505
[Quine] p. 44Theorem 6.11spsbc 3754  spsbcd 3755
[Quine] p. 44Theorem 6.12elex 3457
[Quine] p. 44Theorem 6.13elab 3635  elabg 3632  elabgf 3630
[Quine] p. 44Theorem 6.14noel 4288
[Quine] p. 48Theorem 7.2snprc 4670
[Quine] p. 48Definition 7.1df-pr 4579  df-sn 4577
[Quine] p. 49Theorem 7.4snss 4737  snssg 4736
[Quine] p. 49Theorem 7.5prss 4772  prssg 4771
[Quine] p. 49Theorem 7.6prid1 4715  prid1g 4713  prid2 4716  prid2g 4714  snid 4615  snidg 4613
[Quine] p. 51Theorem 7.12snex 5374
[Quine] p. 51Theorem 7.13prex 5375
[Quine] p. 53Theorem 8.2unisn 4878  unisnALT 44957  unisng 4877
[Quine] p. 53Theorem 8.3uniun 4882
[Quine] p. 54Theorem 8.6elssuni 4889
[Quine] p. 54Theorem 8.7uni0 4887
[Quine] p. 56Theorem 8.17uniabio 6451
[Quine] p. 56Definition 8.18dfaiota2 47116  dfiota2 6438
[Quine] p. 57Theorem 8.19aiotaval 47125  iotaval 6455
[Quine] p. 57Theorem 8.22iotanul 6461
[Quine] p. 58Theorem 8.23iotaex 6457
[Quine] p. 58Definition 9.1df-op 4583
[Quine] p. 61Theorem 9.5opabid 5465  opabidw 5464  opelopab 5482  opelopaba 5476  opelopabaf 5484  opelopabf 5485  opelopabg 5478  opelopabga 5473  opelopabgf 5480  oprabid 7378  oprabidw 7377
[Quine] p. 64Definition 9.11df-xp 5622
[Quine] p. 64Definition 9.12df-cnv 5624
[Quine] p. 64Definition 9.15df-id 5511
[Quine] p. 65Theorem 10.3fun0 6546
[Quine] p. 65Theorem 10.4funi 6513
[Quine] p. 65Theorem 10.5funsn 6534  funsng 6532
[Quine] p. 65Definition 10.1df-fun 6483
[Quine] p. 65Definition 10.2args 6041  dffv4 6819
[Quine] p. 68Definition 10.11conventions 30375  df-fv 6489  fv2 6817
[Quine] p. 124Theorem 17.3nn0opth2 14176  nn0opth2i 14175  nn0opthi 14174  omopthi 8576
[Quine] p. 177Definition 25.2df-rdg 8329
[Quine] p. 232Equation icarddom 10442
[Quine] p. 284Axiom 39(vi)funimaex 6569  funimaexg 6568
[Quine] p. 331Axiom system NFru 3739
[ReedSimon] p. 36Definition (iii)ax-his3 31059
[ReedSimon] p. 63Exercise 4(a)df-dip 30676  polid 31134  polid2i 31132  polidi 31133
[ReedSimon] p. 63Exercise 4(b)df-ph 30788
[ReedSimon] p. 195Remarklnophm 31994  lnophmi 31993
[Retherford] p. 49Exercise 1(i)leopadd 32107
[Retherford] p. 49Exercise 1(ii)leopmul 32109  leopmuli 32108
[Retherford] p. 49Exercise 1(iv)leoptr 32112
[Retherford] p. 49Definition VI.1df-leop 31827  leoppos 32101
[Retherford] p. 49Exercise 1(iii)leoptri 32111
[Retherford] p. 49Definition of operator orderingleop3 32100
[Roman] p. 4Definitiondf-dmat 22403  df-dmatalt 48429
[Roman] p. 18Part Preliminariesdf-rng 20069
[Roman] p. 19Part Preliminariesdf-ring 20151
[Roman] p. 46Theorem 1.6isldepslvec2 48516
[Roman] p. 112Noteisldepslvec2 48516  ldepsnlinc 48539  zlmodzxznm 48528
[Roman] p. 112Examplezlmodzxzequa 48527  zlmodzxzequap 48530  zlmodzxzldep 48535
[Roman] p. 170Theorem 7.8cayleyhamilton 22803
[Rosenlicht] p. 80Theoremheicant 37694
[Rosser] p. 281Definitiondf-op 4583
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34653
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34654
[Rotman] p. 28Remarkpgrpgt2nabl 48396  pmtr3ncom 19385
[Rotman] p. 31Theorem 3.4symggen2 19381
[Rotman] p. 42Theorem 3.15cayley 19324  cayleyth 19325
[Rudin] p. 164Equation 27efcan 16000
[Rudin] p. 164Equation 30efzval 16008
[Rudin] p. 167Equation 48absefi 16102
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1772
[Sanford] p. 39Rule 4mptxor 1770
[Sanford] p. 40Rule 1mptnan 1769
[Schechter] p. 51Definition of antisymmetryintasym 6062
[Schechter] p. 51Definition of irreflexivityintirr 6065
[Schechter] p. 51Definition of symmetrycnvsym 6061
[Schechter] p. 51Definition of transitivitycotr 6059
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17485
[Schechter] p. 79Definition of Moore closuredf-mrc 17486
[Schechter] p. 82Section 4.5df-mrc 17486
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17488
[Schechter] p. 139Definition AC3dfac9 10025
[Schechter] p. 141Definition (MC)dfac11 43094
[Schechter] p. 149Axiom DC1ax-dc 10334  axdc3 10342
[Schechter] p. 187Definition of "ring with unit"isring 20153  isrngo 37936
[Schechter] p. 276Remark 11.6.espan0 31517
[Schechter] p. 276Definition of spandf-span 31284  spanval 31308
[Schechter] p. 428Definition 15.35bastop1 22906
[Schloeder] p. 1Lemma 1.3onelon 6331  onelord 43283  ordelon 6330  ordelord 6328
[Schloeder] p. 1Lemma 1.7onepsuc 43284  sucidg 6389
[Schloeder] p. 1Remark 1.50elon 6361  onsuc 7743  ord0 6360  ordsuci 7741
[Schloeder] p. 1Theorem 1.9epsoon 43285
[Schloeder] p. 1Definition 1.1dftr5 5202
[Schloeder] p. 1Definition 1.2dford3 43060  elon2 6317
[Schloeder] p. 1Definition 1.4df-suc 6312
[Schloeder] p. 1Definition 1.6epel 5519  epelg 5517
[Schloeder] p. 1Theorem 1.9(i)elirr 9485  epirron 43286  ordirr 6324
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43288  oneptr 43287  ontr1 6353
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6349  oneptri 43289  ordtri3or 6338
[Schloeder] p. 2Lemma 1.10ondif1 8416  ord0eln0 6362
[Schloeder] p. 2Lemma 1.13elsuci 6375  onsucss 43298  trsucss 6396
[Schloeder] p. 2Lemma 1.14ordsucss 7748
[Schloeder] p. 2Lemma 1.15onnbtwn 6402  ordnbtwn 6401
[Schloeder] p. 2Lemma 1.16orddif0suc 43300  ordnexbtwnsuc 43299
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10289  onsucf1lem 43301  onsucf1o 43304  onsucf1olem 43302  onsucrn 43303
[Schloeder] p. 2Lemma 1.18dflim7 43305
[Schloeder] p. 2Remark 1.12ordzsl 7775
[Schloeder] p. 2Theorem 1.10ondif1i 43294  ordne0gt0 43293
[Schloeder] p. 2Definition 1.11dflim6 43296  limnsuc 43297  onsucelab 43295
[Schloeder] p. 3Remark 1.21omex 9533
[Schloeder] p. 3Theorem 1.19tfinds 7790
[Schloeder] p. 3Theorem 1.22omelon 9536  ordom 7806
[Schloeder] p. 3Definition 1.20dfom3 9537
[Schloeder] p. 4Lemma 2.21onn 8555
[Schloeder] p. 4Lemma 2.7ssonuni 7713  ssorduni 7712
[Schloeder] p. 4Remark 2.4oa1suc 8446
[Schloeder] p. 4Theorem 1.23dfom5 9540  limom 7812
[Schloeder] p. 4Definition 2.1df-1o 8385  df1o2 8392
[Schloeder] p. 4Definition 2.3oa0 8431  oa0suclim 43307  oalim 8447  oasuc 8439
[Schloeder] p. 4Definition 2.5om0 8432  om0suclim 43308  omlim 8448  omsuc 8441
[Schloeder] p. 4Definition 2.6oe0 8437  oe0m1 8436  oe0suclim 43309  oelim 8449  oesuc 8442
[Schloeder] p. 5Lemma 2.10onsupuni 43261
[Schloeder] p. 5Lemma 2.11onsupsucismax 43311
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43312
[Schloeder] p. 5Lemma 2.13limexissup 43313  limexissupab 43315  limiun 43314  limuni 6368
[Schloeder] p. 5Lemma 2.14oa0r 8453
[Schloeder] p. 5Lemma 2.15om1 8457  om1om1r 43316  om1r 8458
[Schloeder] p. 5Remark 2.8oacl 8450  oaomoecl 43310  oecl 8452  omcl 8451
[Schloeder] p. 5Definition 2.9onsupintrab 43263
[Schloeder] p. 6Lemma 2.16oe1 8459
[Schloeder] p. 6Lemma 2.17oe1m 8460
[Schloeder] p. 6Lemma 2.18oe0rif 43317
[Schloeder] p. 6Theorem 2.19oasubex 43318
[Schloeder] p. 6Theorem 2.20nnacl 8526  nnamecl 43319  nnecl 8528  nnmcl 8527
[Schloeder] p. 7Lemma 3.1onsucwordi 43320
[Schloeder] p. 7Lemma 3.2oaword1 8467
[Schloeder] p. 7Lemma 3.3oaword2 8468
[Schloeder] p. 7Lemma 3.4oalimcl 8475
[Schloeder] p. 7Lemma 3.5oaltublim 43322
[Schloeder] p. 8Lemma 3.6oaordi3 43323
[Schloeder] p. 8Lemma 3.81oaomeqom 43325
[Schloeder] p. 8Lemma 3.10oa00 8474
[Schloeder] p. 8Lemma 3.11omge1 43329  omword1 8488
[Schloeder] p. 8Remark 3.9oaordnr 43328  oaordnrex 43327
[Schloeder] p. 8Theorem 3.7oaord3 43324
[Schloeder] p. 9Lemma 3.12omge2 43330  omword2 8489
[Schloeder] p. 9Lemma 3.13omlim2 43331
[Schloeder] p. 9Lemma 3.14omord2lim 43332
[Schloeder] p. 9Lemma 3.15omord2i 43333  omordi 8481
[Schloeder] p. 9Theorem 3.16omord 8483  omord2com 43334
[Schloeder] p. 10Lemma 3.172omomeqom 43335  df-2o 8386
[Schloeder] p. 10Lemma 3.19oege1 43338  oewordi 8506
[Schloeder] p. 10Lemma 3.20oege2 43339  oeworde 8508
[Schloeder] p. 10Lemma 3.21rp-oelim2 43340
[Schloeder] p. 10Lemma 3.22oeord2lim 43341
[Schloeder] p. 10Remark 3.18omnord1 43337  omnord1ex 43336
[Schloeder] p. 11Lemma 3.23oeord2i 43342
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43344
[Schloeder] p. 11Remark 3.26oenord1 43348  oenord1ex 43347
[Schloeder] p. 11Theorem 4.1oaomoencom 43349
[Schloeder] p. 11Theorem 4.2oaass 8476
[Schloeder] p. 11Theorem 3.24oeord2com 43343
[Schloeder] p. 12Theorem 4.3odi 8494
[Schloeder] p. 13Theorem 4.4omass 8495
[Schloeder] p. 14Remark 4.6oenass 43351
[Schloeder] p. 14Theorem 4.7oeoa 8512
[Schloeder] p. 15Lemma 5.1cantnftermord 43352
[Schloeder] p. 15Lemma 5.2cantnfub 43353  cantnfub2 43354
[Schloeder] p. 16Theorem 5.3cantnf2 43357
[Schwabhauser] p. 10Axiom A1axcgrrflx 28890  axtgcgrrflx 28438
[Schwabhauser] p. 10Axiom A2axcgrtr 28891
[Schwabhauser] p. 10Axiom A3axcgrid 28892  axtgcgrid 28439
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28424
[Schwabhauser] p. 11Axiom A4axsegcon 28903  axtgsegcon 28440  df-trkgcb 28426
[Schwabhauser] p. 11Axiom A5ax5seg 28914  axtg5seg 28441  df-trkgcb 28426
[Schwabhauser] p. 11Axiom A6axbtwnid 28915  axtgbtwnid 28442  df-trkgb 28425
[Schwabhauser] p. 12Axiom A7axpasch 28917  axtgpasch 28443  df-trkgb 28425
[Schwabhauser] p. 12Axiom A8axlowdim2 28936  df-trkg2d 34673
[Schwabhauser] p. 13Axiom A8axtglowdim2 28446
[Schwabhauser] p. 13Axiom A9axtgupdim2 28447  df-trkg2d 34673
[Schwabhauser] p. 13Axiom A10axeuclid 28939  axtgeucl 28448  df-trkge 28427
[Schwabhauser] p. 13Axiom A11axcont 28952  axtgcont 28445  axtgcont1 28444  df-trkgb 28425
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36020
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36022
[Schwabhauser] p. 27Theorem 2.3cgrtr 36025
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36029
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36030  tgcgrcomimp 28453  tgcgrcoml 28455  tgcgrcomr 28454
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36035  tgcgrtriv 28460
[Schwabhauser] p. 28Theorem 2.105segofs 36039  tg5segofs 34681
[Schwabhauser] p. 28Definition 2.10df-afs 34678  df-ofs 36016
[Schwabhauser] p. 29Theorem 2.11cgrextend 36041  tgcgrextend 28461
[Schwabhauser] p. 29Theorem 2.12segconeq 36043  tgsegconeq 28462
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36055  btwntriv2 36045  tgbtwntriv2 28463
[Schwabhauser] p. 30Theorem 3.2btwncomim 36046  tgbtwncom 28464
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36049  tgbtwntriv1 28467
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36050  tgbtwnswapid 28468
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36056  btwnintr 36052  tgbtwnexch2 28472  tgbtwnintr 28469
[Schwabhauser] p. 30Theorem 3.6btwnexch 36058  btwnexch3 36053  tgbtwnexch 28474  tgbtwnexch3 28470
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36057  tgbtwnouttr 28473  tgbtwnouttr2 28471
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28935
[Schwabhauser] p. 32Theorem 3.14btwndiff 36060  tgbtwndiff 28482
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28475  trisegint 36061
[Schwabhauser] p. 34Theorem 4.2ifscgr 36077  tgifscgr 28484
[Schwabhauser] p. 34Theorem 4.11colcom 28534  colrot1 28535  colrot2 28536  lncom 28598  lnrot1 28599  lnrot2 28600
[Schwabhauser] p. 34Definition 4.1df-ifs 36073
[Schwabhauser] p. 35Theorem 4.3cgrsub 36078  tgcgrsub 28485
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36088  tgcgrxfr 28494
[Schwabhauser] p. 35Statement 4.4ercgrg 28493
[Schwabhauser] p. 35Definition 4.4df-cgr3 36074  df-cgrg 28487
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28487
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36089  tgbtwnxfr 28506
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36095  colinearperm2 36097  colinearperm3 36096  colinearperm4 36098  colinearperm5 36099
[Schwabhauser] p. 36Definition 4.8df-ismt 28509
[Schwabhauser] p. 36Definition 4.10df-colinear 36072  tgellng 28529  tglng 28522
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36100
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36108  lnxfr 28542
[Schwabhauser] p. 37Theorem 4.14lineext 36109  lnext 28543
[Schwabhauser] p. 37Theorem 4.16fscgr 36113  tgfscgr 28544
[Schwabhauser] p. 37Theorem 4.17linecgr 36114  lncgr 28545
[Schwabhauser] p. 37Definition 4.15df-fs 36075
[Schwabhauser] p. 38Theorem 4.18lineid 36116  lnid 28546
[Schwabhauser] p. 38Theorem 4.19idinside 36117  tgidinside 28547
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36134  tgbtwnconn1 28551
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36135  tgbtwnconn2 28552
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36136  tgbtwnconn3 28553
[Schwabhauser] p. 41Theorem 5.5brsegle2 36142
[Schwabhauser] p. 41Definition 5.4df-segle 36140  legov 28561
[Schwabhauser] p. 41Definition 5.5legov2 28562
[Schwabhauser] p. 42Remark 5.13legso 28575
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36143
[Schwabhauser] p. 42Theorem 5.7seglerflx 36145
[Schwabhauser] p. 42Theorem 5.8segletr 36147
[Schwabhauser] p. 42Theorem 5.9segleantisym 36148
[Schwabhauser] p. 42Theorem 5.10seglelin 36149
[Schwabhauser] p. 42Theorem 5.11seglemin 36146
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36151
[Schwabhauser] p. 42Proposition 5.7legid 28563
[Schwabhauser] p. 42Proposition 5.8legtrd 28565
[Schwabhauser] p. 42Proposition 5.9legtri3 28566
[Schwabhauser] p. 42Proposition 5.10legtrid 28567
[Schwabhauser] p. 42Proposition 5.11leg0 28568
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36158
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36159
[Schwabhauser] p. 43Theorem 6.4broutsideof 36154  df-outsideof 36153
[Schwabhauser] p. 43Definition 6.1broutsideof2 36155  ishlg 28578
[Schwabhauser] p. 44Theorem 6.4hlln 28583
[Schwabhauser] p. 44Theorem 6.5hlid 28585  outsideofrflx 36160
[Schwabhauser] p. 44Theorem 6.6hlcomb 28579  hlcomd 28580  outsideofcom 36161
[Schwabhauser] p. 44Theorem 6.7hltr 28586  outsideoftr 36162
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28594  outsideofeu 36164
[Schwabhauser] p. 44Definition 6.8df-ray 36171
[Schwabhauser] p. 45Part 2df-lines2 36172
[Schwabhauser] p. 45Theorem 6.13outsidele 36165
[Schwabhauser] p. 45Theorem 6.15lineunray 36180
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36181  tglineelsb2 28608
[Schwabhauser] p. 45Theorem 6.17linecom 36183  linerflx1 36182  linerflx2 36184  tglinecom 28611  tglinerflx1 28609  tglinerflx2 28610
[Schwabhauser] p. 45Theorem 6.18linethru 36186  tglinethru 28612
[Schwabhauser] p. 45Definition 6.14df-line2 36170  tglng 28522
[Schwabhauser] p. 45Proposition 6.13legbtwn 28570
[Schwabhauser] p. 46Theorem 6.19linethrueu 36189  tglinethrueu 28615
[Schwabhauser] p. 46Theorem 6.21lineintmo 36190  tglineineq 28619  tglineinteq 28621  tglineintmo 28618
[Schwabhauser] p. 46Theorem 6.23colline 28625
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28626
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28627
[Schwabhauser] p. 49Theorem 7.3mirinv 28642
[Schwabhauser] p. 49Theorem 7.7mirmir 28638
[Schwabhauser] p. 49Theorem 7.8mirreu3 28630
[Schwabhauser] p. 49Definition 7.5df-mir 28629  ismir 28635  mirbtwn 28634  mircgr 28633  mirfv 28632  mirval 28631
[Schwabhauser] p. 50Theorem 7.8mirreu 28640
[Schwabhauser] p. 50Theorem 7.9mireq 28641
[Schwabhauser] p. 50Theorem 7.10mirinv 28642
[Schwabhauser] p. 50Theorem 7.11mirf1o 28645
[Schwabhauser] p. 50Theorem 7.13miriso 28646
[Schwabhauser] p. 51Theorem 7.14mirmot 28651
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28648  mirbtwni 28647
[Schwabhauser] p. 51Theorem 7.16mircgrs 28649
[Schwabhauser] p. 51Theorem 7.17miduniq 28661
[Schwabhauser] p. 52Lemma 7.21symquadlem 28665
[Schwabhauser] p. 52Theorem 7.18miduniq1 28662
[Schwabhauser] p. 52Theorem 7.19miduniq2 28663
[Schwabhauser] p. 52Theorem 7.20colmid 28664
[Schwabhauser] p. 53Lemma 7.22krippen 28667
[Schwabhauser] p. 55Lemma 7.25midexlem 28668
[Schwabhauser] p. 57Theorem 8.2ragcom 28674
[Schwabhauser] p. 57Definition 8.1df-rag 28670  israg 28673
[Schwabhauser] p. 58Theorem 8.3ragcol 28675
[Schwabhauser] p. 58Theorem 8.4ragmir 28676
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28678
[Schwabhauser] p. 58Theorem 8.6ragflat2 28679
[Schwabhauser] p. 58Theorem 8.7ragflat 28680
[Schwabhauser] p. 58Theorem 8.8ragtriva 28681
[Schwabhauser] p. 58Theorem 8.9ragflat3 28682  ragncol 28685
[Schwabhauser] p. 58Theorem 8.10ragcgr 28683
[Schwabhauser] p. 59Theorem 8.12perpcom 28689
[Schwabhauser] p. 59Theorem 8.13ragperp 28693
[Schwabhauser] p. 59Theorem 8.14perpneq 28690
[Schwabhauser] p. 59Definition 8.11df-perpg 28672  isperp 28688
[Schwabhauser] p. 59Definition 8.13isperp2 28691
[Schwabhauser] p. 60Theorem 8.18foot 28698
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28706  colperpexlem2 28707
[Schwabhauser] p. 63Theorem 8.21colperpex 28709  colperpexlem3 28708
[Schwabhauser] p. 64Theorem 8.22mideu 28714  midex 28713
[Schwabhauser] p. 66Lemma 8.24opphllem 28711
[Schwabhauser] p. 67Theorem 9.2oppcom 28720
[Schwabhauser] p. 67Definition 9.1islnopp 28715
[Schwabhauser] p. 68Lemma 9.3opphllem2 28724
[Schwabhauser] p. 68Lemma 9.4opphllem5 28727  opphllem6 28728
[Schwabhauser] p. 69Theorem 9.5opphl 28730
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28443
[Schwabhauser] p. 70Theorem 9.6outpasch 28731
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28739
[Schwabhauser] p. 71Definition 9.7df-hpg 28734  hpgbr 28736
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28741
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28740
[Schwabhauser] p. 72Theorem 9.11hpgid 28742
[Schwabhauser] p. 72Theorem 9.12hpgcom 28743
[Schwabhauser] p. 72Theorem 9.13hpgtr 28744
[Schwabhauser] p. 73Theorem 9.18colopp 28745
[Schwabhauser] p. 73Theorem 9.19colhp 28746
[Schwabhauser] p. 88Theorem 10.2lmieu 28760
[Schwabhauser] p. 88Definition 10.1df-mid 28750
[Schwabhauser] p. 89Theorem 10.4lmicom 28764
[Schwabhauser] p. 89Theorem 10.5lmilmi 28765
[Schwabhauser] p. 89Theorem 10.6lmireu 28766
[Schwabhauser] p. 89Theorem 10.7lmieq 28767
[Schwabhauser] p. 89Theorem 10.8lmiinv 28768
[Schwabhauser] p. 89Theorem 10.9lmif1o 28771
[Schwabhauser] p. 89Theorem 10.10lmiiso 28773
[Schwabhauser] p. 89Definition 10.3df-lmi 28751
[Schwabhauser] p. 90Theorem 10.11lmimot 28774
[Schwabhauser] p. 91Theorem 10.12hypcgr 28777
[Schwabhauser] p. 92Theorem 10.14lmiopp 28778
[Schwabhauser] p. 92Theorem 10.15lnperpex 28779
[Schwabhauser] p. 92Theorem 10.16trgcopy 28780  trgcopyeu 28782
[Schwabhauser] p. 95Definition 11.2dfcgra2 28806
[Schwabhauser] p. 95Definition 11.3iscgra 28785
[Schwabhauser] p. 95Proposition 11.4cgracgr 28794
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28792  cgrahl2 28793
[Schwabhauser] p. 96Theorem 11.6cgraid 28795
[Schwabhauser] p. 96Theorem 11.9cgraswap 28796
[Schwabhauser] p. 97Theorem 11.7cgracom 28798
[Schwabhauser] p. 97Theorem 11.8cgratr 28799
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28802  cgrahl 28803
[Schwabhauser] p. 98Theorem 11.13sacgr 28807
[Schwabhauser] p. 98Theorem 11.14oacgr 28808
[Schwabhauser] p. 98Theorem 11.15acopy 28809  acopyeu 28810
[Schwabhauser] p. 101Theorem 11.24inagswap 28817
[Schwabhauser] p. 101Theorem 11.25inaghl 28821
[Schwabhauser] p. 101Definition 11.23isinag 28814
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28829
[Schwabhauser] p. 102Definition 11.27df-leag 28822  isleag 28823
[Schwabhauser] p. 107Theorem 11.49tgsas 28831  tgsas1 28830  tgsas2 28832  tgsas3 28833
[Schwabhauser] p. 108Theorem 11.50tgasa 28835  tgasa1 28834
[Schwabhauser] p. 109Theorem 11.51tgsss1 28836  tgsss2 28837  tgsss3 28838
[Shapiro] p. 230Theorem 6.5.1dchrhash 27207  dchrsum 27205  dchrsum2 27204  sumdchr 27208
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27209  sum2dchr 27210
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19978  ablfacrp2 19979
[Shapiro], p. 328Equation 9.2.4vmasum 27152
[Shapiro], p. 329Equation 9.2.7logfac2 27153
[Shapiro], p. 329Equation 9.2.9logfacrlim 27160
[Shapiro], p. 331Equation 9.2.13vmadivsum 27418
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27421
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27475  vmalogdivsum2 27474
[Shapiro], p. 375Theorem 9.4.1dirith 27465  dirith2 27464
[Shapiro], p. 375Equation 9.4.3rplogsum 27463  rpvmasum 27462  rpvmasum2 27448
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27423
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27461
[Shapiro], p. 377Lemma 9.4.1dchrisum 27428  dchrisumlem1 27425  dchrisumlem2 27426  dchrisumlem3 27427  dchrisumlema 27424
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27431
[Shapiro], p. 379Equation 9.4.16dchrmusum 27460  dchrmusumlem 27458  dchrvmasumlem 27459
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27430
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27432
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27456  dchrisum0re 27449  dchrisumn0 27457
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27442
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27446
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27447
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27502  pntrsumbnd2 27503  pntrsumo1 27501
[Shapiro], p. 405Equation 10.2.1mudivsum 27466
[Shapiro], p. 406Equation 10.2.6mulogsum 27468
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27470
[Shapiro], p. 407Equation 10.2.8mulog2sum 27473
[Shapiro], p. 418Equation 10.4.6logsqvma 27478
[Shapiro], p. 418Equation 10.4.8logsqvma2 27479
[Shapiro], p. 419Equation 10.4.10selberg 27484
[Shapiro], p. 420Equation 10.4.12selberg2lem 27486
[Shapiro], p. 420Equation 10.4.14selberg2 27487
[Shapiro], p. 422Equation 10.6.7selberg3 27495
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27496
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27493  selberg3lem2 27494
[Shapiro], p. 422Equation 10.4.23selberg4 27497
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27491
[Shapiro], p. 428Equation 10.6.2selbergr 27504
[Shapiro], p. 429Equation 10.6.8selberg3r 27505
[Shapiro], p. 430Equation 10.6.11selberg4r 27506
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27520
[Shapiro], p. 434Equation 10.6.27pntlema 27532  pntlemb 27533  pntlemc 27531  pntlemd 27530  pntlemg 27534
[Shapiro], p. 435Equation 10.6.29pntlema 27532
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27524
[Shapiro], p. 436Lemma 10.6.2pntibnd 27529
[Shapiro], p. 436Equation 10.6.34pntlema 27532
[Shapiro], p. 436Equation 10.6.35pntlem3 27545  pntleml 27547
[Stewart] p. 91Lemma 7.3constrss 33751
[Stewart] p. 92Definition 7.4.df-constr 33738
[Stewart] p. 96Theorem 7.10constraddcl 33770  constrinvcl 33781  constrmulcl 33779  constrnegcl 33771  constrsqrtcl 33787
[Stewart] p. 97Theorem 7.11constrextdg2 33757
[Stewart] p. 98Theorem 7.12constrext2chn 33767
[Stewart] p. 99Theorem 7.132sqr3nconstr 33789
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33799
[Stoll] p. 13Definition corresponds to dfsymdif3 4256
[Stoll] p. 16Exercise 4.40dif 4355  dif0 4328
[Stoll] p. 16Exercise 4.8difdifdir 4442
[Stoll] p. 17Theorem 5.1(5)unvdif 4425
[Stoll] p. 19Theorem 5.2(13)undm 4247
[Stoll] p. 19Theorem 5.2(13')indm 4248
[Stoll] p. 20Remarkinvdif 4229
[Stoll] p. 25Definition of ordered tripledf-ot 4585
[Stoll] p. 43Definitionuniiun 5007
[Stoll] p. 44Definitionintiin 5008
[Stoll] p. 45Definitiondf-iin 4944
[Stoll] p. 45Definition indexed uniondf-iun 4943
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4256
[Strang] p. 242Section 6.3expgrowth 44367
[Suppes] p. 22Theorem 2eq0 4300  eq0f 4297
[Suppes] p. 22Theorem 4eqss 3950  eqssd 3952  eqssi 3951
[Suppes] p. 23Theorem 5ss0 4352  ss0b 4351
[Suppes] p. 23Theorem 6sstr 3943  sstrALT2 44866
[Suppes] p. 23Theorem 7pssirr 4053
[Suppes] p. 23Theorem 8pssn2lp 4054
[Suppes] p. 23Theorem 9psstr 4057
[Suppes] p. 23Theorem 10pssss 4048
[Suppes] p. 25Theorem 12elin 3918  elun 4103
[Suppes] p. 26Theorem 15inidm 4177
[Suppes] p. 26Theorem 16in0 4345
[Suppes] p. 27Theorem 23unidm 4107
[Suppes] p. 27Theorem 24un0 4344
[Suppes] p. 27Theorem 25ssun1 4128
[Suppes] p. 27Theorem 26ssequn1 4136
[Suppes] p. 27Theorem 27unss 4140
[Suppes] p. 27Theorem 28indir 4236
[Suppes] p. 27Theorem 29undir 4237
[Suppes] p. 28Theorem 32difid 4326
[Suppes] p. 29Theorem 33difin 4222
[Suppes] p. 29Theorem 34indif 4230
[Suppes] p. 29Theorem 35undif1 4426
[Suppes] p. 29Theorem 36difun2 4431
[Suppes] p. 29Theorem 37difin0 4424
[Suppes] p. 29Theorem 38disjdif 4422
[Suppes] p. 29Theorem 39difundi 4240
[Suppes] p. 29Theorem 40difindi 4242
[Suppes] p. 30Theorem 41nalset 5251
[Suppes] p. 39Theorem 61uniss 4867
[Suppes] p. 39Theorem 65uniop 5455
[Suppes] p. 41Theorem 70intsn 4934
[Suppes] p. 42Theorem 71intpr 4932  intprg 4931
[Suppes] p. 42Theorem 73op1stb 5411
[Suppes] p. 42Theorem 78intun 4930
[Suppes] p. 44Definition 15(a)dfiun2 4982  dfiun2g 4980
[Suppes] p. 44Definition 15(b)dfiin2 4983
[Suppes] p. 47Theorem 86elpw 4554  elpw2 5272  elpw2g 5271  elpwg 4553  elpwgdedVD 44948
[Suppes] p. 47Theorem 87pwid 4572
[Suppes] p. 47Theorem 89pw0 4764
[Suppes] p. 48Theorem 90pwpw0 4765
[Suppes] p. 52Theorem 101xpss12 5631
[Suppes] p. 52Theorem 102xpindi 5773  xpindir 5774
[Suppes] p. 52Theorem 103xpundi 5685  xpundir 5686
[Suppes] p. 54Theorem 105elirrv 9483
[Suppes] p. 58Theorem 2relss 5722
[Suppes] p. 59Theorem 4eldm 5840  eldm2 5841  eldm2g 5839  eldmg 5838
[Suppes] p. 59Definition 3df-dm 5626
[Suppes] p. 60Theorem 6dmin 5851
[Suppes] p. 60Theorem 8rnun 6092
[Suppes] p. 60Theorem 9rnin 6093
[Suppes] p. 60Definition 4dfrn2 5828
[Suppes] p. 61Theorem 11brcnv 5822  brcnvg 5819
[Suppes] p. 62Equation 5elcnv 5816  elcnv2 5817
[Suppes] p. 62Theorem 12relcnv 6053
[Suppes] p. 62Theorem 15cnvin 6091
[Suppes] p. 62Theorem 16cnvun 6089
[Suppes] p. 63Definitiondftrrels2 38611
[Suppes] p. 63Theorem 20co02 6208
[Suppes] p. 63Theorem 21dmcoss 5914
[Suppes] p. 63Definition 7df-co 5625
[Suppes] p. 64Theorem 26cnvco 5825
[Suppes] p. 64Theorem 27coass 6213
[Suppes] p. 65Theorem 31resundi 5942
[Suppes] p. 65Theorem 34elima 6014  elima2 6015  elima3 6016  elimag 6013
[Suppes] p. 65Theorem 35imaundi 6096
[Suppes] p. 66Theorem 40dminss 6100
[Suppes] p. 66Theorem 41imainss 6101
[Suppes] p. 67Exercise 11cnvxp 6104
[Suppes] p. 81Definition 34dfec2 8625
[Suppes] p. 82Theorem 72elec 8668  elecALTV 38300  elecg 8666
[Suppes] p. 82Theorem 73eqvrelth 38647  erth 8676  erth2 8677
[Suppes] p. 83Theorem 74eqvreldisj 38650  erdisj 8679
[Suppes] p. 83Definition 35, df-parts 38802  dfmembpart2 38807
[Suppes] p. 89Theorem 96map0b 8807
[Suppes] p. 89Theorem 97map0 8811  map0g 8808
[Suppes] p. 89Theorem 98mapsn 8812  mapsnd 8810
[Suppes] p. 89Theorem 99mapss 8813
[Suppes] p. 91Definition 12(ii)alephsuc 9956
[Suppes] p. 91Definition 12(iii)alephlim 9955
[Suppes] p. 92Theorem 1enref 8907  enrefg 8906
[Suppes] p. 92Theorem 2ensym 8925  ensymb 8924  ensymi 8926
[Suppes] p. 92Theorem 3entr 8928
[Suppes] p. 92Theorem 4unen 8967
[Suppes] p. 94Theorem 15endom 8901
[Suppes] p. 94Theorem 16ssdomg 8922
[Suppes] p. 94Theorem 17domtr 8929
[Suppes] p. 95Theorem 18sbth 9010
[Suppes] p. 97Theorem 23canth2 9043  canth2g 9044
[Suppes] p. 97Definition 3brsdom2 9014  df-sdom 8872  dfsdom2 9013
[Suppes] p. 97Theorem 21(i)sdomirr 9027
[Suppes] p. 97Theorem 22(i)domnsym 9016
[Suppes] p. 97Theorem 21(ii)sdomnsym 9015
[Suppes] p. 97Theorem 22(ii)domsdomtr 9025
[Suppes] p. 97Theorem 22(iv)brdom2 8904
[Suppes] p. 97Theorem 21(iii)sdomtr 9028
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9023
[Suppes] p. 98Exercise 4fundmen 8953  fundmeng 8954
[Suppes] p. 98Exercise 6xpdom3 8988
[Suppes] p. 98Exercise 11sdomentr 9024
[Suppes] p. 104Theorem 37fofi 9197
[Suppes] p. 104Theorem 38pwfi 9203
[Suppes] p. 105Theorem 40pwfi 9203
[Suppes] p. 111Axiom for cardinal numberscarden 10439
[Suppes] p. 130Definition 3df-tr 5199
[Suppes] p. 132Theorem 9ssonuni 7713
[Suppes] p. 134Definition 6df-suc 6312
[Suppes] p. 136Theorem Schema 22findes 7830  finds 7826  finds1 7829  finds2 7828
[Suppes] p. 151Theorem 42isfinite 9542  isfinite2 9182  isfiniteg 9184  unbnn 9180
[Suppes] p. 162Definition 5df-ltnq 10806  df-ltpq 10798
[Suppes] p. 197Theorem Schema 4tfindes 7793  tfinds 7790  tfinds2 7794
[Suppes] p. 209Theorem 18oaord1 8466
[Suppes] p. 209Theorem 21oaword2 8468
[Suppes] p. 211Theorem 25oaass 8476
[Suppes] p. 225Definition 8iscard2 9866
[Suppes] p. 227Theorem 56ondomon 10451
[Suppes] p. 228Theorem 59harcard 9868
[Suppes] p. 228Definition 12(i)aleph0 9954
[Suppes] p. 228Theorem Schema 61onintss 6358
[Suppes] p. 228Theorem Schema 62onminesb 7726  onminsb 7727
[Suppes] p. 229Theorem 64alephval2 10460
[Suppes] p. 229Theorem 65alephcard 9958
[Suppes] p. 229Theorem 66alephord2i 9965
[Suppes] p. 229Theorem 67alephnbtwn 9959
[Suppes] p. 229Definition 12df-aleph 9830
[Suppes] p. 242Theorem 6weth 10383
[Suppes] p. 242Theorem 8entric 10445
[Suppes] p. 242Theorem 9carden 10439
[Szendrei] p. 11Line 6df-cloneop 35728
[Szendrei] p. 11Paragraph 3df-suppos 35732
[TakeutiZaring] p. 8Axiom 1ax-ext 2703
[TakeutiZaring] p. 13Definition 4.5df-cleq 2723
[TakeutiZaring] p. 13Proposition 4.6df-clel 2806
[TakeutiZaring] p. 13Proposition 4.9cvjust 2725
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2751
[TakeutiZaring] p. 14Definition 4.16df-oprab 7350
[TakeutiZaring] p. 14Proposition 4.14ru 3739
[TakeutiZaring] p. 15Axiom 2zfpair 5359
[TakeutiZaring] p. 15Exercise 1elpr 4601  elpr2 4603  elpr2g 4602  elprg 4599
[TakeutiZaring] p. 15Exercise 2elsn 4591  elsn2 4618  elsn2g 4617  elsng 4590  velsn 4592
[TakeutiZaring] p. 15Exercise 3elop 5407
[TakeutiZaring] p. 15Exercise 4sneq 4586  sneqr 4792
[TakeutiZaring] p. 15Definition 5.1dfpr2 4597  dfsn2 4589  dfsn2ALT 4598
[TakeutiZaring] p. 16Axiom 3uniex 7674
[TakeutiZaring] p. 16Exercise 6opth 5416
[TakeutiZaring] p. 16Exercise 7opex 5404
[TakeutiZaring] p. 16Exercise 8rext 5389
[TakeutiZaring] p. 16Corollary 5.8unex 7677  unexg 7676
[TakeutiZaring] p. 16Definition 5.3dftp2 4644
[TakeutiZaring] p. 16Definition 5.5df-uni 4860
[TakeutiZaring] p. 16Definition 5.6df-in 3909  df-un 3907
[TakeutiZaring] p. 16Proposition 5.7unipr 4876  uniprg 4875
[TakeutiZaring] p. 17Axiom 4vpwex 5315
[TakeutiZaring] p. 17Exercise 1eltp 4642
[TakeutiZaring] p. 17Exercise 5elsuc 6378  elsucg 6376  sstr2 3941
[TakeutiZaring] p. 17Exercise 6uncom 4108
[TakeutiZaring] p. 17Exercise 7incom 4159
[TakeutiZaring] p. 17Exercise 8unass 4122
[TakeutiZaring] p. 17Exercise 9inass 4178
[TakeutiZaring] p. 17Exercise 10indi 4234
[TakeutiZaring] p. 17Exercise 11undi 4235
[TakeutiZaring] p. 17Definition 5.9df-pss 3922  df-ss 3919
[TakeutiZaring] p. 17Definition 5.10df-pw 4552
[TakeutiZaring] p. 18Exercise 7unss2 4137
[TakeutiZaring] p. 18Exercise 9dfss2 3920  sseqin2 4173
[TakeutiZaring] p. 18Exercise 10ssid 3957
[TakeutiZaring] p. 18Exercise 12inss1 4187  inss2 4188
[TakeutiZaring] p. 18Exercise 13nss 3999
[TakeutiZaring] p. 18Exercise 15unieq 4870
[TakeutiZaring] p. 18Exercise 18sspwb 5390  sspwimp 44949  sspwimpALT 44956  sspwimpALT2 44959  sspwimpcf 44951
[TakeutiZaring] p. 18Exercise 19pweqb 5397
[TakeutiZaring] p. 19Axiom 5ax-rep 5217
[TakeutiZaring] p. 20Definitiondf-rab 3396
[TakeutiZaring] p. 20Corollary 5.160ex 5245
[TakeutiZaring] p. 20Definition 5.12df-dif 3905
[TakeutiZaring] p. 20Definition 5.14dfnul2 4286
[TakeutiZaring] p. 20Proposition 5.15difid 4326
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4303  n0f 4299  neq0 4302  neq0f 4298
[TakeutiZaring] p. 21Axiom 6zfreg 9482
[TakeutiZaring] p. 21Axiom 6'zfregs 9622
[TakeutiZaring] p. 21Theorem 5.22setind 9624
[TakeutiZaring] p. 21Definition 5.20df-v 3438
[TakeutiZaring] p. 21Proposition 5.21vprc 5253
[TakeutiZaring] p. 22Exercise 10ss 4350
[TakeutiZaring] p. 22Exercise 3ssex 5259  ssexg 5261
[TakeutiZaring] p. 22Exercise 4inex1 5255
[TakeutiZaring] p. 22Exercise 5ruv 9491
[TakeutiZaring] p. 22Exercise 6elirr 9485
[TakeutiZaring] p. 22Exercise 7ssdif0 4316
[TakeutiZaring] p. 22Exercise 11difdif 4085
[TakeutiZaring] p. 22Exercise 13undif3 4250  undif3VD 44913
[TakeutiZaring] p. 22Exercise 14difss 4086
[TakeutiZaring] p. 22Exercise 15sscon 4093
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3048
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3057
[TakeutiZaring] p. 23Proposition 6.2xpex 7686  xpexg 7683
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5623
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6552
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6728  fun11 6555
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6494  svrelfun 6553
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5827
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5829
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5628
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5629
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5625
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6141  dfrel2 6136
[TakeutiZaring] p. 25Exercise 3xpss 5632
[TakeutiZaring] p. 25Exercise 5relun 5751
[TakeutiZaring] p. 25Exercise 6reluni 5758
[TakeutiZaring] p. 25Exercise 9inxp 5771
[TakeutiZaring] p. 25Exercise 12relres 5954
[TakeutiZaring] p. 25Exercise 13opelres 5934  opelresi 5936
[TakeutiZaring] p. 25Exercise 14dmres 5961
[TakeutiZaring] p. 25Exercise 15resss 5950
[TakeutiZaring] p. 25Exercise 17resabs1 5955
[TakeutiZaring] p. 25Exercise 18funres 6523
[TakeutiZaring] p. 25Exercise 24relco 6057
[TakeutiZaring] p. 25Exercise 29funco 6521
[TakeutiZaring] p. 25Exercise 30f1co 6730
[TakeutiZaring] p. 26Definition 6.10eu2 2604
[TakeutiZaring] p. 26Definition 6.11conventions 30375  df-fv 6489  fv3 6840
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7855  cnvexg 7854
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7839  dmexg 7831
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7840  rnexg 7832
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44485
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7850
[TakeutiZaring] p. 27Corollary 6.13fvex 6835
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47204  tz6.12-1-afv2 47271  tz6.12-1 6845  tz6.12-afv 47203  tz6.12-afv2 47270  tz6.12 6846  tz6.12c-afv2 47272  tz6.12c 6844
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47267  tz6.12-2 6809  tz6.12i-afv2 47273  tz6.12i 6848
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6484
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6485
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6487  wfo 6479
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6486  wf1 6478
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6488  wf1o 6480
[TakeutiZaring] p. 28Exercise 4eqfnfv 6964  eqfnfv2 6965  eqfnfv2f 6968
[TakeutiZaring] p. 28Exercise 5fvco 6920
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7151
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7149
[TakeutiZaring] p. 29Exercise 9funimaex 6569  funimaexg 6568
[TakeutiZaring] p. 29Definition 6.18df-br 5092
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5525
[TakeutiZaring] p. 30Definition 6.21dffr2 5577  dffr3 6048  eliniseg 6043  iniseg 6046
[TakeutiZaring] p. 30Definition 6.22df-eprel 5516
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5593  fr3nr 7705  frirr 5592
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5569
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7707
[TakeutiZaring] p. 31Exercise 1frss 5580
[TakeutiZaring] p. 31Exercise 4wess 5602
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6294  tz6.26i 6295  wefrc 5610  wereu2 5613
[TakeutiZaring] p. 32Theorem 6.27wfi 6296  wfii 6297
[TakeutiZaring] p. 32Definition 6.28df-isom 6490
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7263
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7264
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7270
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7271
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7272
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7276
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7283
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7285
[TakeutiZaring] p. 35Notationwtr 5198
[TakeutiZaring] p. 35Theorem 7.2trelpss 44486  tz7.2 5599
[TakeutiZaring] p. 35Definition 7.1dftr3 5203
[TakeutiZaring] p. 36Proposition 7.4ordwe 6319
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6327
[TakeutiZaring] p. 36Proposition 7.6ordelord 6328  ordelordALT 44569  ordelordALTVD 44898
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6334  ordelssne 6333
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6332
[TakeutiZaring] p. 37Proposition 7.9ordin 6336
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7715
[TakeutiZaring] p. 38Corollary 7.15ordsson 7716
[TakeutiZaring] p. 38Definition 7.11df-on 6310
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6338
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44581  ordon 7710
[TakeutiZaring] p. 38Proposition 7.13onprc 7711
[TakeutiZaring] p. 39Theorem 7.17tfi 7783
[TakeutiZaring] p. 40Exercise 3ontr2 6354
[TakeutiZaring] p. 40Exercise 7dftr2 5200
[TakeutiZaring] p. 40Exercise 9onssmin 7725
[TakeutiZaring] p. 40Exercise 11unon 7761
[TakeutiZaring] p. 40Exercise 12ordun 6412
[TakeutiZaring] p. 40Exercise 14ordequn 6411
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7712
[TakeutiZaring] p. 40Proposition 7.20elssuni 4889
[TakeutiZaring] p. 41Definition 7.22df-suc 6312
[TakeutiZaring] p. 41Proposition 7.23sssucid 6388  sucidg 6389
[TakeutiZaring] p. 41Proposition 7.24onsuc 7743
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6402  ordnbtwn 6401
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7758
[TakeutiZaring] p. 42Exercise 1df-lim 6311
[TakeutiZaring] p. 42Exercise 4omssnlim 7811
[TakeutiZaring] p. 42Exercise 7ssnlim 7816
[TakeutiZaring] p. 42Exercise 8onsucssi 7771  ordelsuc 7750
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7752
[TakeutiZaring] p. 42Definition 7.27nlimon 7781
[TakeutiZaring] p. 42Definition 7.28dfom2 7798
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7819
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7820
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7821
[TakeutiZaring] p. 43Remarkomon 7808
[TakeutiZaring] p. 43Axiom 7inf3 9525  omex 9533
[TakeutiZaring] p. 43Theorem 7.32ordom 7806
[TakeutiZaring] p. 43Corollary 7.31find 7825
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7822
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7823
[TakeutiZaring] p. 44Exercise 1limomss 7801
[TakeutiZaring] p. 44Exercise 2int0 4912
[TakeutiZaring] p. 44Exercise 3trintss 5216
[TakeutiZaring] p. 44Exercise 4intss1 4913
[TakeutiZaring] p. 44Exercise 5intex 5282
[TakeutiZaring] p. 44Exercise 6oninton 7728
[TakeutiZaring] p. 44Exercise 11ordintdif 6357
[TakeutiZaring] p. 44Definition 7.35df-int 4898
[TakeutiZaring] p. 44Proposition 7.34noinfep 9550
[TakeutiZaring] p. 45Exercise 4onint 7723
[TakeutiZaring] p. 47Lemma 1tfrlem1 8295
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8316
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8317
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8318
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8325  tz7.44-2 8326  tz7.44-3 8327
[TakeutiZaring] p. 50Exercise 1smogt 8287
[TakeutiZaring] p. 50Exercise 3smoiso 8282
[TakeutiZaring] p. 50Definition 7.46df-smo 8266
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8364  tz7.49c 8365
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8362
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8361
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8363
[TakeutiZaring] p. 53Proposition 7.532eu5 2651
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9899
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9900
[TakeutiZaring] p. 56Definition 8.1oalim 8447  oasuc 8439
[TakeutiZaring] p. 57Remarktfindsg 7791
[TakeutiZaring] p. 57Proposition 8.2oacl 8450
[TakeutiZaring] p. 57Proposition 8.3oa0 8431  oa0r 8453
[TakeutiZaring] p. 57Proposition 8.16omcl 8451
[TakeutiZaring] p. 58Corollary 8.5oacan 8463
[TakeutiZaring] p. 58Proposition 8.4nnaord 8534  nnaordi 8533  oaord 8462  oaordi 8461
[TakeutiZaring] p. 59Proposition 8.6iunss2 4998  uniss2 4892
[TakeutiZaring] p. 59Proposition 8.7oawordri 8465
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8470  oawordex 8472
[TakeutiZaring] p. 59Proposition 8.9nnacl 8526
[TakeutiZaring] p. 59Proposition 8.10oaabs 8563
[TakeutiZaring] p. 60Remarkoancom 9541
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8475
[TakeutiZaring] p. 62Exercise 1nnarcl 8531
[TakeutiZaring] p. 62Exercise 5oaword1 8467
[TakeutiZaring] p. 62Definition 8.15om0x 8434  omlim 8448  omsuc 8441
[TakeutiZaring] p. 62Definition 8.15(a)om0 8432
[TakeutiZaring] p. 63Proposition 8.17nnecl 8528  nnmcl 8527
[TakeutiZaring] p. 63Proposition 8.19nnmord 8547  nnmordi 8546  omord 8483  omordi 8481
[TakeutiZaring] p. 63Proposition 8.20omcan 8484
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8551  omwordri 8487
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8454
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8457  om1r 8458
[TakeutiZaring] p. 64Proposition 8.22om00 8490
[TakeutiZaring] p. 64Proposition 8.23omordlim 8492
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8493
[TakeutiZaring] p. 64Proposition 8.25odi 8494
[TakeutiZaring] p. 65Theorem 8.26omass 8495
[TakeutiZaring] p. 67Definition 8.30nnesuc 8523  oe0 8437  oelim 8449  oesuc 8442  onesuc 8445
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8435
[TakeutiZaring] p. 67Proposition 8.32oen0 8501
[TakeutiZaring] p. 67Proposition 8.33oeordi 8502
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8436
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8460
[TakeutiZaring] p. 68Corollary 8.34oeord 8503
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8509
[TakeutiZaring] p. 68Proposition 8.35oewordri 8507
[TakeutiZaring] p. 68Proposition 8.37oeworde 8508
[TakeutiZaring] p. 69Proposition 8.41oeoa 8512
[TakeutiZaring] p. 70Proposition 8.42oeoe 8514
[TakeutiZaring] p. 73Theorem 9.1trcl 9618  tz9.1 9619
[TakeutiZaring] p. 76Definition 9.9df-r1 9654  r10 9658  r1lim 9662  r1limg 9661  r1suc 9660  r1sucg 9659
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9670  r1ord2 9671  r1ordg 9668
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9680
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9705  tz9.13 9681  tz9.13g 9682
[TakeutiZaring] p. 79Definition 9.14df-rank 9655  rankval 9706  rankvalb 9687  rankvalg 9707
[TakeutiZaring] p. 79Proposition 9.16rankel 9729  rankelb 9714
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9743  rankval3 9730  rankval3b 9716
[TakeutiZaring] p. 79Proposition 9.18rankonid 9719
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9685
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9724  rankr1c 9711  rankr1g 9722
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9725
[TakeutiZaring] p. 80Exercise 1rankss 9739  rankssb 9738
[TakeutiZaring] p. 80Exercise 2unbndrank 9732
[TakeutiZaring] p. 80Proposition 9.19bndrank 9731
[TakeutiZaring] p. 83Axiom of Choiceac4 10363  dfac3 10009
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9918  numth 10360  numth2 10359
[TakeutiZaring] p. 85Definition 10.4cardval 10434
[TakeutiZaring] p. 85Proposition 10.5cardid 10435  cardid2 9843
[TakeutiZaring] p. 85Proposition 10.9oncard 9850
[TakeutiZaring] p. 85Proposition 10.10carden 10439
[TakeutiZaring] p. 85Proposition 10.11cardidm 9849
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9834
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9855
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9847
[TakeutiZaring] p. 87Proposition 10.15pwen 9063
[TakeutiZaring] p. 88Exercise 1en0 8940
[TakeutiZaring] p. 88Exercise 7infensuc 9068
[TakeutiZaring] p. 89Exercise 10omxpen 8992
[TakeutiZaring] p. 90Corollary 10.23cardnn 9853
[TakeutiZaring] p. 90Definition 10.27alephiso 9986
[TakeutiZaring] p. 90Proposition 10.20nneneq 9115
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9123
[TakeutiZaring] p. 90Proposition 10.26alephprc 9987
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9120
[TakeutiZaring] p. 91Exercise 2alephle 9976
[TakeutiZaring] p. 91Exercise 3aleph0 9954
[TakeutiZaring] p. 91Exercise 4cardlim 9862
[TakeutiZaring] p. 91Exercise 7infpss 10104
[TakeutiZaring] p. 91Exercise 8infcntss 9207
[TakeutiZaring] p. 91Definition 10.29df-fin 8873  isfi 8898
[TakeutiZaring] p. 92Proposition 10.32onfin 9124
[TakeutiZaring] p. 92Proposition 10.34imadomg 10422
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8985
[TakeutiZaring] p. 93Proposition 10.35fodomb 10414
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10074  unxpdom 9143
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9864  cardsdomelir 9863
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9145
[TakeutiZaring] p. 94Proposition 10.39infxpen 9902
[TakeutiZaring] p. 95Definition 10.42df-map 8752
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10450  infxpidm2 9905
[TakeutiZaring] p. 95Proposition 10.41infdju 10095  infxp 10102
[TakeutiZaring] p. 96Proposition 10.44pw2en 8997  pw2f1o 8995
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9056
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10375
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10370  ac6s5 10379
[TakeutiZaring] p. 98Theorem 10.47unidom 10431
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10432  uniimadomf 10433
[TakeutiZaring] p. 100Definition 11.1cfcof 10162
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10157
[TakeutiZaring] p. 102Exercise 1cfle 10142
[TakeutiZaring] p. 102Exercise 2cf0 10139
[TakeutiZaring] p. 102Exercise 3cfsuc 10145
[TakeutiZaring] p. 102Exercise 4cfom 10152
[TakeutiZaring] p. 102Proposition 11.9coftr 10161
[TakeutiZaring] p. 103Theorem 11.15alephreg 10470
[TakeutiZaring] p. 103Proposition 11.11cardcf 10140
[TakeutiZaring] p. 103Proposition 11.13alephsing 10164
[TakeutiZaring] p. 104Corollary 11.17cardinfima 9985
[TakeutiZaring] p. 104Proposition 11.16carduniima 9984
[TakeutiZaring] p. 104Proposition 11.18alephfp 9996  alephfp2 9997
[TakeutiZaring] p. 106Theorem 11.20gchina 10587
[TakeutiZaring] p. 106Theorem 11.21mappwen 10000
[TakeutiZaring] p. 107Theorem 11.26konigth 10457
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10471
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10472
[Tarski] p. 67Axiom B5ax-c5 38921
[Tarski] p. 67Scheme B5sp 2186
[Tarski] p. 68Lemma 6avril1 30438  equid 2013
[Tarski] p. 69Lemma 7equcomi 2018
[Tarski] p. 70Lemma 14spim 2387  spime 2389  spimew 1972
[Tarski] p. 70Lemma 16ax-12 2180  ax-c15 38927  ax12i 1967
[Tarski] p. 70Lemmas 16 and 17sb6 2088
[Tarski] p. 75Axiom B7ax6v 1969
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1911  ax5ALT 38945
[Tarski], p. 75Scheme B8 of system S2ax-7 2009  ax-8 2113  ax-9 2121
[Tarski1999] p. 178Axiom 4axtgsegcon 28440
[Tarski1999] p. 178Axiom 5axtg5seg 28441
[Tarski1999] p. 179Axiom 7axtgpasch 28443
[Tarski1999] p. 180Axiom 7.1axtgpasch 28443
[Tarski1999] p. 185Axiom 11axtgcont1 28444
[Truss] p. 114Theorem 5.18ruc 16149
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37698
[Viaclovsky8] p. 3Proposition 7ismblfin 37700
[Weierstrass] p. 272Definitiondf-mdet 22498  mdetuni 22535
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 903
[WhiteheadRussell] p. 96Axiom *1.3olc 868
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 869
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 919
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 969
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 188
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 37478
[WhiteheadRussell] p. 100Theorem *2.05frege5 43832  imim2 58  wl-luk-imim2 37473
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47049  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2658  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37476
[WhiteheadRussell] p. 101Theorem *2.11exmid 894
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 897
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 44958  wl-luk-notnotr 37477
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43862  axfrege28 43861  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 867
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 924
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37470
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 889
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 941
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30376  pm2.27 42  wl-luk-pm2.27 37468
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38390
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 923
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 971
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 972
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 970
[WhiteheadRussell] p. 105Definition *2.33df-3or 1087
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 906
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 907
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 944
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 881
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 882
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 191
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 883
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 884
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 885
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 851
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 852
[WhiteheadRussell] p. 107Theorem *2.55orel1 888
[WhiteheadRussell] p. 107Theorem *2.56orel2 890
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 899
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 942
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 943
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 891  pm2.67 892
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 898
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 974
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 900
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 975
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 976
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 933
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 931
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 973
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 977
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 932
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 993
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 994
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 995
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 996
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 997
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 471
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 459
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 402
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 802
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 448
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 449
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 482  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 484  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 764
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 765
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 807
[WhiteheadRussell] p. 113Fact)pm3.45 622
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 809
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 492
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 493
[WhiteheadRussell] p. 113Theorem *3.44jao 962  pm3.44 961
[WhiteheadRussell] p. 113Theorem *3.47anim12 808
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 965
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 261
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 353
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 806
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 832
[WhiteheadRussell] p. 117Theorem *4.21bicom 222
[WhiteheadRussell] p. 117Theorem *4.22biantr 805  bitr 804
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 563
[WhiteheadRussell] p. 117Theorem *4.25oridm 904  pm4.25 905
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1009
[WhiteheadRussell] p. 118Theorem *4.31orcom 870
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[WhiteheadRussell] p. 118Theorem *4.33orass 921
[WhiteheadRussell] p. 118Theorem *4.36anbi1 633
[WhiteheadRussell] p. 118Theorem *4.37orbi1 917
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 637
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 978
[WhiteheadRussell] p. 118Definition *4.34df-3an 1088
[WhiteheadRussell] p. 119Theorem *4.41ordi 1007
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1053
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1024
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 998
[WhiteheadRussell] p. 119Theorem *4.45orabs 1000  pm4.45 999  pm4.45im 827
[WhiteheadRussell] p. 120Theorem *4.5anor 984
[WhiteheadRussell] p. 120Theorem *4.6imor 853
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 983
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 986
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 987
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 988
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 989
[WhiteheadRussell] p. 120Theorem *4.56ioran 985  pm4.56 990
[WhiteheadRussell] p. 120Theorem *4.57oran 991  pm4.57 992
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 856
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 849
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 850
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 398
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 557  pm4.71d 561  pm4.71i 559  pm4.71r 558  pm4.71rd 562  pm4.71ri 560
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 951
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 936
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 963  pm4.77 964
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 934
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1005
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1025
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1026
[WhiteheadRussell] p. 122Theorem *4.84imbi1 347
[WhiteheadRussell] p. 122Theorem *4.85imbi2 348
[WhiteheadRussell] p. 122Theorem *4.86bibi1 351
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 387  impexp 450  pm4.87 843
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 823
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 946  pm5.11g 945
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 947
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 949
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 948
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1014
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1015
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1013
[WhiteheadRussell] p. 124Theorem *5.18nbbn 383  pm5.18 381
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 386
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 824
[WhiteheadRussell] p. 124Theorem *5.22xor 1016
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1049
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1050
[WhiteheadRussell] p. 124Theorem *5.25dfor2 901
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 572
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 388
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 361
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1003
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 955
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 830
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 573
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 835
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 825
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 833
[WhiteheadRussell] p. 125Theorem *5.41imdi 389  pm5.41 390
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 543
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 542
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1006
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1019
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 950
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1002
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1020
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1021
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1029
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1030
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44390
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44391
[WhiteheadRussell] p. 147Theorem *10.2219.26 1871
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44392
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44393
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44394
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1894
[WhiteheadRussell] p. 151Theorem *10.301albitr 44395
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44396
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44397
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44398
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44399
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44401
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44402
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44403
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44400
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2093
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44406
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44407
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2073
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2163
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1830
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1831
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44408
[WhiteheadRussell] p. 162Theorem *11.322alim 44409
[WhiteheadRussell] p. 162Theorem *11.332albi 44410
[WhiteheadRussell] p. 162Theorem *11.342exim 44411
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44413
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44412
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1888
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44415
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44416
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44414
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1829
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44417
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44418
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1847
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44419
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2346
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1861
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44424
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44420
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44421
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44422
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44423
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44428
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44425
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44426
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44427
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44429
[WhiteheadRussell] p. 175Definition *14.02df-eu 2564
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44439  pm13.13b 44440
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44441
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3009
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3010
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3621
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44447
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44448
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44442
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44584  pm13.193 44443
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44444
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44445
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44446
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44453
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44452
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44451
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3804
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44454  pm14.122b 44455  pm14.122c 44456
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44457  pm14.123b 44458  pm14.123c 44459
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44461
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44460
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44462
[WhiteheadRussell] p. 190Theorem *14.22iota4 6462
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44463
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6463
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44464
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44466
[WhiteheadRussell] p. 192Theorem *14.26eupick 2628  eupickbi 2631  sbaniota 44467
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44465
[WhiteheadRussell] p. 192Theorem *14.271eubi 2579
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44468
[WhiteheadRussell] p. 235Definition *30.01conventions 30375  df-fv 6489
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9891  pm54.43lem 9890
[Young] p. 141Definition of operator orderingleop2 32099
[Young] p. 142Example 12.2(i)0leop 32105  idleop 32106
[vandenDries] p. 42Lemma 61irrapx1 42860
[vandenDries] p. 43Theorem 62pellex 42867  pellexlem1 42861

This page was last updated on 28-Jan-2026.
Copyright terms: Public domain