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 17566
[Adamek] p. 21Condition 3.1(b)df-cat 17566
[Adamek] p. 22Example 3.3(1)df-setc 17975
[Adamek] p. 24Example 3.3(4.c)0cat 17587  0funcg 49096  df-termc 49484
[Adamek] p. 24Example 3.3(4.d)df-prstc 49561  prsthinc 49475
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49589  df-mndtc 49589
[Adamek] p. 24Example 3.3(4)(c)discsnterm 49585
[Adamek] p. 25Definition 3.5df-oppc 17610
[Adamek] p. 25Example 3.6(1)oduoppcciso 49577
[Adamek] p. 25Example 3.6(2)oppgoppcco 49602  oppgoppchom 49601  oppgoppcid 49603
[Adamek] p. 28Remark 3.9oppciso 17680
[Adamek] p. 28Remark 3.12invf1o 17668  invisoinvl 17689
[Adamek] p. 28Example 3.13idinv 17688  idiso 17687
[Adamek] p. 28Corollary 3.11inveq 17673
[Adamek] p. 28Definition 3.8df-inv 17647  df-iso 17648  dfiso2 17671
[Adamek] p. 28Proposition 3.10sectcan 17654
[Adamek] p. 29Remark 3.16cicer 17705  cicerALT 49057
[Adamek] p. 29Definition 3.15cic 17698  df-cic 17695
[Adamek] p. 29Definition 3.17df-func 17757
[Adamek] p. 29Proposition 3.14(1)invinv 17669
[Adamek] p. 29Proposition 3.14(2)invco 17670  isoco 17676
[Adamek] p. 30Remark 3.19df-func 17757
[Adamek] p. 30Example 3.20(1)idfucl 17780
[Adamek] p. 30Example 3.20(2)diag1 49315
[Adamek] p. 32Proposition 3.21funciso 17773
[Adamek] p. 33Example 3.26(1)discsnterm 49585  discthing 49472
[Adamek] p. 33Example 3.26(2)df-thinc 49429  prsthinc 49475  thincciso 49464  thincciso2 49466  thincciso3 49467  thinccisod 49465
[Adamek] p. 33Example 3.26(3)df-mndtc 49589
[Adamek] p. 33Proposition 3.23cofucl 17787  cofucla 49107
[Adamek] p. 34Remark 3.28(1)cofidfth 49173
[Adamek] p. 34Remark 3.28(2)catciso 18010  catcisoi 49411
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18065
[Adamek] p. 34Definition 3.27(2)df-fth 17806
[Adamek] p. 34Definition 3.27(3)df-full 17805
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18065
[Adamek] p. 35Corollary 3.32ffthiso 17830
[Adamek] p. 35Proposition 3.30(c)cofth 17836
[Adamek] p. 35Proposition 3.30(d)cofull 17835
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18050
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18050
[Adamek] p. 39Remark 3.422oppf 49143
[Adamek] p. 39Definition 3.41df-oppf 49134  funcoppc 17774
[Adamek] p. 39Definition 3.44.df-catc 17998  elcatchom 49408
[Adamek] p. 39Proposition 3.43(c)fthoppc 17824  fthoppf 49175
[Adamek] p. 39Proposition 3.43(d)fulloppc 17823  fulloppf 49174
[Adamek] p. 40Remark 3.48catccat 18007
[Adamek] p. 40Definition 3.470funcg 49096  df-catc 17998
[Adamek] p. 45Exercise 3Gincat 49612
[Adamek] p. 48Remark 4.2(2)cnelsubc 49615  nelsubc3 49082
[Adamek] p. 48Remark 4.2(3)imasubc 49162  imasubc2 49163  imasubc3 49167
[Adamek] p. 48Example 4.3(1.a)0subcat 17737
[Adamek] p. 48Example 4.3(1.b)catsubcat 17738
[Adamek] p. 48Definition 4.1(1)nelsubc3 49082
[Adamek] p. 48Definition 4.1(2)fullsubc 17749
[Adamek] p. 48Definition 4.1(a)df-subc 17711
[Adamek] p. 49Remark 4.4idsubc 49171
[Adamek] p. 49Remark 4.4(1)idemb 49170
[Adamek] p. 49Remark 4.4(2)idfullsubc 49172  ressffth 17839
[Adamek] p. 58Exercise 4Asetc1onsubc 49613
[Adamek] p. 83Definition 6.1df-nat 17845
[Adamek] p. 87Remark 6.14(a)fuccocl 17866
[Adamek] p. 87Remark 6.14(b)fucass 17870
[Adamek] p. 87Definition 6.15df-fuc 17846
[Adamek] p. 88Remark 6.16fuccat 17872
[Adamek] p. 101Definition 7.10funcg 49096  df-inito 17883
[Adamek] p. 101Example 7.2(3)0funcg 49096  df-termc 49484  initc 49102
[Adamek] p. 101Example 7.2 (6)irinitoringc 21409
[Adamek] p. 102Definition 7.4df-termo 17884  oppctermo 49247
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17911
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17915
[Adamek] p. 103Remark 7.8oppczeroo 49248
[Adamek] p. 103Definition 7.7df-zeroo 17885
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21410
[Adamek] p. 103Proposition 7.6termoeu1w 17918
[Adamek] p. 106Definition 7.19df-sect 17646
[Adamek] p. 107Example 7.20(7)thincinv 49480
[Adamek] p. 108Example 7.25(4)thincsect2 49479
[Adamek] p. 110Example 7.33(9)thincmon 49444
[Adamek] p. 110Proposition 7.35sectmon 17681
[Adamek] p. 112Proposition 7.42sectepi 17683
[Adamek] p. 185Section 10.67updjud 9819
[Adamek] p. 193Definition 11.1(1)df-lmd 49656
[Adamek] p. 193Definition 11.3(1)df-lmd 49656
[Adamek] p. 194Definition 11.3(2)df-lmd 49656
[Adamek] p. 202Definition 11.27(1)df-cmd 49657
[Adamek] p. 202Definition 11.27(2)df-cmd 49657
[Adamek] p. 478Item Rngdf-ringc 20554
[AhoHopUll] p. 2Section 1.1df-bigo 48559
[AhoHopUll] p. 12Section 1.3df-blen 48581
[AhoHopUll] p. 318Section 9.1df-concat 14470  df-pfx 14571  df-substr 14541  df-word 14413  lencl 14432  wrd0 14438
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24616  df-nmoo 30715
[AkhiezerGlazman] p. 64Theoremhmopidmch 32123  hmopidmchi 32121
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32171  pjcmul2i 32172
[AkhiezerGlazman] p. 72Theoremcnvunop 31888  unoplin 31890
[AkhiezerGlazman] p. 72Equation 2unopadj 31889  unopadj2 31908
[AkhiezerGlazman] p. 73Theoremelunop2 31983  lnopunii 31982
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32056
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27864
[Alling] p. 184Axiom Bbdayfo 27609
[Alling] p. 184Axiom Osltso 27608
[Alling] p. 184Axiom SDnodense 27624
[Alling] p. 185Lemma 0nocvxmin 27711
[Alling] p. 185Theoremconway 27733
[Alling] p. 185Axiom FEnoeta 27675
[Alling] p. 186Theorem 4slerec 27753  slerecd 27754
[Alling], p. 2Definitionrp-brsslt 43435
[Alling], p. 3Notenla0001 43438  nla0002 43436  nla0003 43437
[Apostol] p. 18Theorem I.1addcan 11289  addcan2d 11309  addcan2i 11299  addcand 11308  addcani 11298
[Apostol] p. 18Theorem I.2negeu 11342
[Apostol] p. 18Theorem I.3negsub 11401  negsubd 11470  negsubi 11431
[Apostol] p. 18Theorem I.4negneg 11403  negnegd 11455  negnegi 11423
[Apostol] p. 18Theorem I.5subdi 11542  subdid 11565  subdii 11558  subdir 11543  subdird 11566  subdiri 11559
[Apostol] p. 18Theorem I.6mul01 11284  mul01d 11304  mul01i 11295  mul02 11283  mul02d 11303  mul02i 11294
[Apostol] p. 18Theorem I.7mulcan 11746  mulcan2d 11743  mulcand 11742  mulcani 11748
[Apostol] p. 18Theorem I.8receu 11754  xreceu 32892
[Apostol] p. 18Theorem I.9divrec 11784  divrecd 11892  divreci 11858  divreczi 11851
[Apostol] p. 18Theorem I.10recrec 11810  recreci 11845
[Apostol] p. 18Theorem I.11mul0or 11749  mul0ord 11757  mul0ori 11756
[Apostol] p. 18Theorem I.12mul2neg 11548  mul2negd 11564  mul2negi 11557  mulneg1 11545  mulneg1d 11562  mulneg1i 11555
[Apostol] p. 18Theorem I.13divadddiv 11828  divadddivd 11933  divadddivi 11875
[Apostol] p. 18Theorem I.14divmuldiv 11813  divmuldivd 11930  divmuldivi 11873  rdivmuldivd 20324
[Apostol] p. 18Theorem I.15divdivdiv 11814  divdivdivd 11936  divdivdivi 11876
[Apostol] p. 20Axiom 7rpaddcl 12906  rpaddcld 12941  rpmulcl 12907  rpmulcld 12942
[Apostol] p. 20Axiom 8rpneg 12916
[Apostol] p. 20Axiom 90nrp 12919
[Apostol] p. 20Theorem I.17lttri 11231
[Apostol] p. 20Theorem I.18ltadd1d 11702  ltadd1dd 11720  ltadd1i 11663
[Apostol] p. 20Theorem I.19ltmul1 11963  ltmul1a 11962  ltmul1i 12032  ltmul1ii 12042  ltmul2 11964  ltmul2d 12968  ltmul2dd 12982  ltmul2i 12035
[Apostol] p. 20Theorem I.20msqgt0 11629  msqgt0d 11676  msqgt0i 11646
[Apostol] p. 20Theorem I.210lt1 11631
[Apostol] p. 20Theorem I.23lt0neg1 11615  lt0neg1d 11678  ltneg 11609  ltnegd 11687  ltnegi 11653
[Apostol] p. 20Theorem I.25lt2add 11594  lt2addd 11732  lt2addi 11671
[Apostol] p. 20Definition of positive numbersdf-rp 12883
[Apostol] p. 21Exercise 4recgt0 11959  recgt0d 12048  recgt0i 12019  recgt0ii 12020
[Apostol] p. 22Definition of integersdf-z 12461
[Apostol] p. 22Definition of positive integersdfnn3 12131
[Apostol] p. 22Definition of rationalsdf-q 12839
[Apostol] p. 24Theorem I.26supeu 9333
[Apostol] p. 26Theorem I.28nnunb 12369
[Apostol] p. 26Theorem I.29arch 12370  archd 45178
[Apostol] p. 28Exercise 2btwnz 12568
[Apostol] p. 28Exercise 3nnrecl 12371
[Apostol] p. 28Exercise 4rebtwnz 12837
[Apostol] p. 28Exercise 5zbtwnre 12836
[Apostol] p. 28Exercise 6qbtwnre 13090
[Apostol] p. 28Exercise 10(a)zeneo 16242  zneo 12548  zneoALTV 47679
[Apostol] p. 29Theorem I.35cxpsqrtth 26659  msqsqrtd 15342  resqrtth 15154  sqrtth 15264  sqrtthi 15270  sqsqrtd 15341
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12120
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12803
[Apostol] p. 361Remarkcrreczi 14127
[Apostol] p. 363Remarkabsgt0i 15299
[Apostol] p. 363Exampleabssubd 15355  abssubi 15303
[ApostolNT] p. 7Remarkfmtno0 47550  fmtno1 47551  fmtno2 47560  fmtno3 47561  fmtno4 47562  fmtno5fac 47592  fmtnofz04prm 47587
[ApostolNT] p. 7Definitiondf-fmtno 47538
[ApostolNT] p. 8Definitiondf-ppi 27030
[ApostolNT] p. 14Definitiondf-dvds 16156
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16172
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16197
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16192
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16185
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16187
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16173
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16174
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16179
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16214
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16216
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16218
[ApostolNT] p. 15Definitiondf-gcd 16398  dfgcd2 16449
[ApostolNT] p. 16Definitionisprm2 16585
[ApostolNT] p. 16Theorem 1.5coprmdvds 16556
[ApostolNT] p. 16Theorem 1.7prminf 16819
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16416
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16450
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16452
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16431
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16423
[ApostolNT] p. 17Theorem 1.8coprm 16614
[ApostolNT] p. 17Theorem 1.9euclemma 16616
[ApostolNT] p. 17Theorem 1.101arith2 16832
[ApostolNT] p. 18Theorem 1.13prmrec 16826
[ApostolNT] p. 19Theorem 1.14divalg 16306
[ApostolNT] p. 20Theorem 1.15eucalg 16490
[ApostolNT] p. 24Definitiondf-mu 27031
[ApostolNT] p. 25Definitiondf-phi 16669
[ApostolNT] p. 25Theorem 2.1musum 27121
[ApostolNT] p. 26Theorem 2.2phisum 16694
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16679
[ApostolNT] p. 28Theorem 2.5(c)phimul 16683
[ApostolNT] p. 32Definitiondf-vma 27028
[ApostolNT] p. 32Theorem 2.9muinv 27123
[ApostolNT] p. 32Theorem 2.10vmasum 27147
[ApostolNT] p. 38Remarkdf-sgm 27032
[ApostolNT] p. 38Definitiondf-sgm 27032
[ApostolNT] p. 75Definitiondf-chp 27029  df-cht 27027
[ApostolNT] p. 104Definitioncongr 16567
[ApostolNT] p. 106Remarkdvdsval3 16159
[ApostolNT] p. 106Definitionmoddvds 16166
[ApostolNT] p. 107Example 2mod2eq0even 16249
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16250
[ApostolNT] p. 107Example 4zmod1congr 13784
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13824
[ApostolNT] p. 107Theorem 5.2(c)modexp 14137
[ApostolNT] p. 108Theorem 5.3modmulconst 16191
[ApostolNT] p. 109Theorem 5.4cncongr1 16570
[ApostolNT] p. 109Theorem 5.6gcdmodi 16978
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16572
[ApostolNT] p. 113Theorem 5.17eulerth 16686
[ApostolNT] p. 113Theorem 5.18vfermltl 16705
[ApostolNT] p. 114Theorem 5.19fermltl 16687
[ApostolNT] p. 116Theorem 5.24wilthimp 27002
[ApostolNT] p. 179Definitiondf-lgs 27226  lgsprme0 27270
[ApostolNT] p. 180Example 11lgs 27271
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27247
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27262
[ApostolNT] p. 181Theorem 9.4m1lgs 27319
[ApostolNT] p. 181Theorem 9.52lgs 27338  2lgsoddprm 27347
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27305
[ApostolNT] p. 185Theorem 9.8lgsquad 27314
[ApostolNT] p. 188Definitiondf-lgs 27226  lgs1 27272
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27263
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27265
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27273
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27274
[Baer] p. 40Property (b)mapdord 41656
[Baer] p. 40Property (c)mapd11 41657
[Baer] p. 40Property (e)mapdin 41680  mapdlsm 41682
[Baer] p. 40Property (f)mapd0 41683
[Baer] p. 40Definition of projectivitydf-mapd 41643  mapd1o 41666
[Baer] p. 41Property (g)mapdat 41685
[Baer] p. 44Part (1)mapdpg 41724
[Baer] p. 45Part (2)hdmap1eq 41819  mapdheq 41746  mapdheq2 41747  mapdheq2biN 41748
[Baer] p. 45Part (3)baerlem3 41731
[Baer] p. 46Part (4)mapdheq4 41750  mapdheq4lem 41749
[Baer] p. 46Part (5)baerlem5a 41732  baerlem5abmN 41736  baerlem5amN 41734  baerlem5b 41733  baerlem5bmN 41735
[Baer] p. 47Part (6)hdmap1l6 41839  hdmap1l6a 41827  hdmap1l6e 41832  hdmap1l6f 41833  hdmap1l6g 41834  hdmap1l6lem1 41825  hdmap1l6lem2 41826  mapdh6N 41765  mapdh6aN 41753  mapdh6eN 41758  mapdh6fN 41759  mapdh6gN 41760  mapdh6lem1N 41751  mapdh6lem2N 41752
[Baer] p. 48Part 9hdmapval 41846
[Baer] p. 48Part 10hdmap10 41858
[Baer] p. 48Part 11hdmapadd 41861
[Baer] p. 48Part (6)hdmap1l6h 41835  mapdh6hN 41761
[Baer] p. 48Part (7)mapdh75cN 41771  mapdh75d 41772  mapdh75e 41770  mapdh75fN 41773  mapdh7cN 41767  mapdh7dN 41768  mapdh7eN 41766  mapdh7fN 41769
[Baer] p. 48Part (8)mapdh8 41806  mapdh8a 41793  mapdh8aa 41794  mapdh8ab 41795  mapdh8ac 41796  mapdh8ad 41797  mapdh8b 41798  mapdh8c 41799  mapdh8d 41801  mapdh8d0N 41800  mapdh8e 41802  mapdh8g 41803  mapdh8i 41804  mapdh8j 41805
[Baer] p. 48Part (9)mapdh9a 41807
[Baer] p. 48Equation 10mapdhvmap 41787
[Baer] p. 49Part 12hdmap11 41866  hdmapeq0 41862  hdmapf1oN 41883  hdmapneg 41864  hdmaprnN 41882  hdmaprnlem1N 41867  hdmaprnlem3N 41868  hdmaprnlem3uN 41869  hdmaprnlem4N 41871  hdmaprnlem6N 41872  hdmaprnlem7N 41873  hdmaprnlem8N 41874  hdmaprnlem9N 41875  hdmapsub 41865
[Baer] p. 49Part 14hdmap14lem1 41886  hdmap14lem10 41895  hdmap14lem1a 41884  hdmap14lem2N 41887  hdmap14lem2a 41885  hdmap14lem3 41888  hdmap14lem8 41893  hdmap14lem9 41894
[Baer] p. 50Part 14hdmap14lem11 41896  hdmap14lem12 41897  hdmap14lem13 41898  hdmap14lem14 41899  hdmap14lem15 41900  hgmapval 41905
[Baer] p. 50Part 15hgmapadd 41912  hgmapmul 41913  hgmaprnlem2N 41915  hgmapvs 41909
[Baer] p. 50Part 16hgmaprnN 41919
[Baer] p. 110Lemma 1hdmapip0com 41935
[Baer] p. 110Line 27hdmapinvlem1 41936
[Baer] p. 110Line 28hdmapinvlem2 41937
[Baer] p. 110Line 30hdmapinvlem3 41938
[Baer] p. 110Part 1.2hdmapglem5 41940  hgmapvv 41944
[Baer] p. 110Proposition 1hdmapinvlem4 41939
[Baer] p. 111Line 10hgmapvvlem1 41941
[Baer] p. 111Line 15hdmapg 41948  hdmapglem7 41947
[Bauer], p. 483Theorem 1.22irrexpq 26660  2irrexpqALT 26730
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2563
[BellMachover] p. 460Notationdf-mo 2534
[BellMachover] p. 460Definitionmo3 2558
[BellMachover] p. 461Axiom Extax-ext 2702
[BellMachover] p. 462Theorem 1.1axextmo 2706
[BellMachover] p. 463Axiom Repaxrep5 5223
[BellMachover] p. 463Scheme Sepax-sep 5232
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37077  sepex 5236
[BellMachover] p. 466Problemaxpow2 5303
[BellMachover] p. 466Axiom Powaxpow3 5304
[BellMachover] p. 466Axiom Unionaxun2 7665
[BellMachover] p. 468Definitiondf-ord 6305
[BellMachover] p. 469Theorem 2.2(i)ordirr 6320
[BellMachover] p. 469Theorem 2.2(iii)onelon 6327
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6322
[BellMachover] p. 471Definition of Ndf-om 7792
[BellMachover] p. 471Problem 2.5(ii)uniordint 7729
[BellMachover] p. 471Definition of Limdf-lim 6307
[BellMachover] p. 472Axiom Infzfinf2 9527
[BellMachover] p. 473Theorem 2.8limom 7807
[BellMachover] p. 477Equation 3.1df-r1 9649
[BellMachover] p. 478Definitionrankval2 9703
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9667  r1ord3g 9664
[BellMachover] p. 480Axiom Regzfreg 9477
[BellMachover] p. 488Axiom ACac5 10360  dfac4 10005
[BellMachover] p. 490Definition of alephalephval3 9993
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39337
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32323
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32365  chirredi 32364
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32353
[Beran] p. 3Definition of joinsshjval3 31324
[Beran] p. 39Theorem 2.3(i)cmcm2 31586  cmcm2i 31563  cmcm2ii 31568  cmt2N 39268
[Beran] p. 40Theorem 2.3(iii)lecm 31587  lecmi 31572  lecmii 31573
[Beran] p. 45Theorem 3.4cmcmlem 31561
[Beran] p. 49Theorem 4.2cm2j 31590  cm2ji 31595  cm2mi 31596
[Beran] p. 95Definitiondf-sh 31177  issh2 31179
[Beran] p. 95Lemma 3.1(S5)his5 31056
[Beran] p. 95Lemma 3.1(S6)his6 31069
[Beran] p. 95Lemma 3.1(S7)his7 31060
[Beran] p. 95Lemma 3.2(S8)ho01i 31798
[Beran] p. 95Lemma 3.2(S9)hoeq1 31800
[Beran] p. 95Lemma 3.2(S10)ho02i 31799
[Beran] p. 95Lemma 3.2(S11)hoeq2 31801
[Beran] p. 95Postulate (S1)ax-his1 31052  his1i 31070
[Beran] p. 95Postulate (S2)ax-his2 31053
[Beran] p. 95Postulate (S3)ax-his3 31054
[Beran] p. 95Postulate (S4)ax-his4 31055
[Beran] p. 96Definition of normdf-hnorm 30938  dfhnorm2 31092  normval 31094
[Beran] p. 96Definition for Cauchy sequencehcau 31154
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30943
[Beran] p. 96Definition of complete subspaceisch3 31211
[Beran] p. 96Definition of convergedf-hlim 30942  hlimi 31158
[Beran] p. 97Theorem 3.3(i)norm-i-i 31103  norm-i 31099
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31107  norm-ii 31108  normlem0 31079  normlem1 31080  normlem2 31081  normlem3 31082  normlem4 31083  normlem5 31084  normlem6 31085  normlem7 31086  normlem7tALT 31089
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31109  norm-iii 31110
[Beran] p. 98Remark 3.4bcs 31151  bcsiALT 31149  bcsiHIL 31150
[Beran] p. 98Remark 3.4(B)normlem9at 31091  normpar 31125  normpari 31124
[Beran] p. 98Remark 3.4(C)normpyc 31116  normpyth 31115  normpythi 31112
[Beran] p. 99Remarklnfn0 32017  lnfn0i 32012  lnop0 31936  lnop0i 31940
[Beran] p. 99Theorem 3.5(i)nmcexi 31996  nmcfnex 32023  nmcfnexi 32021  nmcopex 31999  nmcopexi 31997
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32024  nmcfnlbi 32022  nmcoplb 32000  nmcoplbi 31998
[Beran] p. 99Theorem 3.5(iii)lnfncon 32026  lnfnconi 32025  lnopcon 32005  lnopconi 32004
[Beran] p. 100Lemma 3.6normpar2i 31126
[Beran] p. 101Lemma 3.6norm3adifi 31123  norm3adifii 31118  norm3dif 31120  norm3difi 31117
[Beran] p. 102Theorem 3.7(i)chocunii 31271  pjhth 31363  pjhtheu 31364  pjpjhth 31395  pjpjhthi 31396  pjth 25359
[Beran] p. 102Theorem 3.7(ii)ococ 31376  ococi 31375
[Beran] p. 103Remark 3.8nlelchi 32031
[Beran] p. 104Theorem 3.9riesz3i 32032  riesz4 32034  riesz4i 32033
[Beran] p. 104Theorem 3.10cnlnadj 32049  cnlnadjeu 32048  cnlnadjeui 32047  cnlnadji 32046  cnlnadjlem1 32037  nmopadjlei 32058
[Beran] p. 106Theorem 3.11(i)adjeq0 32061
[Beran] p. 106Theorem 3.11(v)nmopadji 32060
[Beran] p. 106Theorem 3.11(ii)adjmul 32062
[Beran] p. 106Theorem 3.11(iv)adjadj 31906
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32072  nmopcoadji 32071
[Beran] p. 106Theorem 3.11(iii)adjadd 32063
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32073
[Beran] p. 106Theorem 3.11(viii)adjcoi 32070  pjadj2coi 32174  pjadjcoi 32131
[Beran] p. 107Definitiondf-ch 31191  isch2 31193
[Beran] p. 107Remark 3.12choccl 31276  isch3 31211  occl 31274  ocsh 31253  shoccl 31275  shocsh 31254
[Beran] p. 107Remark 3.12(B)ococin 31378
[Beran] p. 108Theorem 3.13chintcl 31302
[Beran] p. 109Property (i)pjadj2 32157  pjadj3 32158  pjadji 31655  pjadjii 31644
[Beran] p. 109Property (ii)pjidmco 32151  pjidmcoi 32147  pjidmi 31643
[Beran] p. 110Definition of projector orderingpjordi 32143
[Beran] p. 111Remarkho0val 31720  pjch1 31640
[Beran] p. 111Definitiondf-hfmul 31704  df-hfsum 31703  df-hodif 31702  df-homul 31701  df-hosum 31700
[Beran] p. 111Lemma 4.4(i)pjo 31641
[Beran] p. 111Lemma 4.4(ii)pjch 31664  pjchi 31402
[Beran] p. 111Lemma 4.4(iii)pjoc2 31409  pjoc2i 31408
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31650
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32135  pjssmii 31651
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32134
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32133
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32138
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32136  pjssge0ii 31652
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32137  pjdifnormii 31653
[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 34295
[Bogachev] p. 17Lemma 1.5.4omssubadd 34303
[Bogachev] p. 17Example 1.5.2omsmon 34301
[Bogachev] p. 41Definition 1.11.2df-carsg 34305
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34325
[Bogachev] p. 116Definition 2.3.1df-itgm 34356  df-sitm 34334
[Bogachev] p. 118Chapter 2.4.4df-itgm 34356
[Bogachev] p. 118Definition 2.4.1df-sitg 34333
[Bollobas] p. 1Section I.1df-edg 29019  isuhgrop 29041  isusgrop 29133  isuspgrop 29132
[Bollobas] p. 2Section I.1df-isubgr 47871  df-subgr 29239  uhgrspan1 29274  uhgrspansubgr 29262
[Bollobas] p. 3Definitiondf-gric 47891  gricuspgr 47928  isuspgrim 47906
[Bollobas] p. 3Section I.1cusgrsize 29426  df-clnbgr 47829  df-cusgr 29383  df-nbgr 29304  fusgrmaxsize 29436
[Bollobas] p. 4Definitiondf-upwlks 48144  df-wlks 29571
[Bollobas] p. 4Section I.1finsumvtxdg2size 29522  finsumvtxdgeven 29524  fusgr1th 29523  fusgrvtxdgonume 29526  vtxdgoddnumeven 29525
[Bollobas] p. 5Notationdf-pths 29685
[Bollobas] p. 5Definitiondf-crcts 29757  df-cycls 29758  df-trls 29662  df-wlkson 29572
[Bollobas] p. 7Section I.1df-ushgr 29030
[BourbakiAlg1] p. 1Definition 1df-clintop 48210  df-cllaw 48196  df-mgm 18540  df-mgm2 48229
[BourbakiAlg1] p. 4Definition 5df-assintop 48211  df-asslaw 48198  df-sgrp 18619  df-sgrp2 48231
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48230  df-comlaw 48197
[BourbakiAlg1] p. 12Definition 2df-mnd 18635
[BourbakiAlg1] p. 17Chapter I.mndlactf1 32997  mndlactf1o 33001  mndractf1 32999  mndractf1o 33002
[BourbakiAlg1] p. 92Definition 1df-ring 20146
[BourbakiAlg1] p. 93Section I.8.1df-rng 20064
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33636
[BourbakiAlg2] p. 113Chapter 5.assafld 33640  assarrginv 33639
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33681  fldextrspunfld 33679  fldextrspunlem1 33678  fldextrspunlem2 33680  fldextrspunlsp 33677  fldextrspunlsplem 33676
[BourbakiCAlg2], p. 228Proposition 21arithidom 33492  dfufd2 33505
[BourbakiEns] p. Proposition 8fcof1 7216  fcofo 7217
[BourbakiTop1] p. Remarkxnegmnf 13101  xnegpnf 13100
[BourbakiTop1] p. Remark rexneg 13102
[BourbakiTop1] p. Remark 3ust0 24128  ustfilxp 24121
[BourbakiTop1] p. Axiom GT'tgpsubcn 23998
[BourbakiTop1] p. Criterionishmeo 23667
[BourbakiTop1] p. Example 1cstucnd 24191  iducn 24190  snfil 23772
[BourbakiTop1] p. Example 2neifil 23788
[BourbakiTop1] p. Theorem 1cnextcn 23975
[BourbakiTop1] p. Theorem 2ucnextcn 24211
[BourbakiTop1] p. Theorem 3df-hcmp 33960
[BourbakiTop1] p. Paragraph 3infil 23771
[BourbakiTop1] p. Definition 1df-ucn 24183  df-ust 24109  filintn0 23769  filn0 23770  istgp 23985  ucnprima 24189
[BourbakiTop1] p. Definition 2df-cfilu 24194
[BourbakiTop1] p. Definition 3df-cusp 24205  df-usp 24165  df-utop 24139  trust 24137
[BourbakiTop1] p. Definition 6df-pcmp 33859
[BourbakiTop1] p. Property V_issnei2 23024
[BourbakiTop1] p. Theorem 1(d)iscncl 23177
[BourbakiTop1] p. Condition F_Iustssel 24114
[BourbakiTop1] p. Condition U_Iustdiag 24117
[BourbakiTop1] p. Property V_iiinnei 23033
[BourbakiTop1] p. Property V_ivneiptopreu 23041  neissex 23035
[BourbakiTop1] p. Proposition 1neips 23021  neiss 23017  ucncn 24192  ustund 24130  ustuqtop 24154
[BourbakiTop1] p. Proposition 2cnpco 23175  neiptopreu 23041  utop2nei 24158  utop3cls 24159
[BourbakiTop1] p. Proposition 3fmucnd 24199  uspreg 24181  utopreg 24160
[BourbakiTop1] p. Proposition 4imasncld 23599  imasncls 23600  imasnopn 23598
[BourbakiTop1] p. Proposition 9cnpflf2 23908
[BourbakiTop1] p. Condition F_IIustincl 24116
[BourbakiTop1] p. Condition U_IIustinvel 24118
[BourbakiTop1] p. Property V_iiielnei 23019
[BourbakiTop1] p. Proposition 11cnextucn 24210
[BourbakiTop1] p. Condition F_IIbustbasel 24115
[BourbakiTop1] p. Condition U_IIIustexhalf 24119
[BourbakiTop1] p. Definition C'''df-cmp 23295
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23754
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22802
[BourbakiTop2] p. 195Definition 1df-ldlf 33856
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46079
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46081  stoweid 46080
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46018  stoweidlem10 46027  stoweidlem14 46031  stoweidlem15 46032  stoweidlem35 46052  stoweidlem36 46053  stoweidlem37 46054  stoweidlem38 46055  stoweidlem40 46057  stoweidlem41 46058  stoweidlem43 46060  stoweidlem44 46061  stoweidlem46 46063  stoweidlem5 46022  stoweidlem50 46067  stoweidlem52 46069  stoweidlem53 46070  stoweidlem55 46072  stoweidlem56 46073
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46040  stoweidlem24 46041  stoweidlem27 46044  stoweidlem28 46045  stoweidlem30 46047
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46051  stoweidlem59 46076  stoweidlem60 46077
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46062  stoweidlem49 46066  stoweidlem7 46024
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46048  stoweidlem39 46056  stoweidlem42 46059  stoweidlem48 46065  stoweidlem51 46068  stoweidlem54 46071  stoweidlem57 46074  stoweidlem58 46075
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46042
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46034
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46028  stoweidlem13 46030  stoweidlem26 46043  stoweidlem61 46078
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46035
[Bruck] p. 1Section I.1df-clintop 48210  df-mgm 18540  df-mgm2 48229
[Bruck] p. 23Section II.1df-sgrp 18619  df-sgrp2 48231
[Bruck] p. 28Theorem 3.2dfgrp3 18944
[ChoquetDD] p. 2Definition of mappingdf-mpt 5171
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 30373
[Clemente] p. 10Definition I` `m,nnatded 30373
[Clemente] p. 11Definition E=>m,nnatded 30373
[Clemente] p. 11Definition I=>m,nnatded 30373
[Clemente] p. 11Definition E` `(1)natded 30373
[Clemente] p. 11Definition E` `(2)natded 30373
[Clemente] p. 12Definition E` `m,n,pnatded 30373
[Clemente] p. 12Definition I` `n(1)natded 30373
[Clemente] p. 12Definition I` `n(2)natded 30373
[Clemente] p. 13Definition I` `m,n,pnatded 30373
[Clemente] p. 14Proof 5.11natded 30373
[Clemente] p. 14Definition E` `nnatded 30373
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30375  ex-natded5.2 30374
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30378  ex-natded5.3 30377
[Clemente] p. 18Theorem 5.5ex-natded5.5 30380
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30382  ex-natded5.7 30381
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30384  ex-natded5.8 30383
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30386  ex-natded5.13 30385
[Clemente] p. 32Definition I` `nnatded 30373
[Clemente] p. 32Definition E` `m,n,p,anatded 30373
[Clemente] p. 32Definition E` `n,tnatded 30373
[Clemente] p. 32Definition I` `n,tnatded 30373
[Clemente] p. 43Theorem 9.20ex-natded9.20 30387
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30388
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30390  ex-natded9.26 30389
[Cohen] p. 301Remarkrelogoprlem 26520
[Cohen] p. 301Property 2relogmul 26521  relogmuld 26554
[Cohen] p. 301Property 3relogdiv 26522  relogdivd 26555
[Cohen] p. 301Property 4relogexp 26525
[Cohen] p. 301Property 1alog1 26514
[Cohen] p. 301Property 1bloge 26515
[Cohen4] p. 348Observationrelogbcxpb 26717
[Cohen4] p. 349Propertyrelogbf 26721
[Cohen4] p. 352Definitionelogb 26700
[Cohen4] p. 361Property 2relogbmul 26707
[Cohen4] p. 361Property 3logbrec 26712  relogbdiv 26709
[Cohen4] p. 361Property 4relogbreexp 26705
[Cohen4] p. 361Property 6relogbexp 26710
[Cohen4] p. 361Property 1(a)logbid1 26698
[Cohen4] p. 361Property 1(b)logb1 26699
[Cohen4] p. 367Propertylogbchbase 26701
[Cohen4] p. 377Property 2logblt 26714
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34288  sxbrsigalem4 34290
[Cohn] p. 81Section II.5acsdomd 18455  acsinfd 18454  acsinfdimd 18456  acsmap2d 18453  acsmapd 18452
[Cohn] p. 143Example 5.1.1sxbrsiga 34293
[Connell] p. 57Definitiondf-scmat 22399  df-scmatalt 48410
[Conway] p. 4Definitionslerec 27753  slerecd 27754
[Conway] p. 5Definitionaddsval 27898  addsval2 27899  df-adds 27896  df-muls 28039  df-negs 27956
[Conway] p. 7Theorem0slt1s 27766
[Conway] p. 12Theorem 12pw2cut2 28375
[Conway] p. 16Theorem 0(i)ssltright 27809
[Conway] p. 16Theorem 0(ii)ssltleft 27808
[Conway] p. 16Theorem 0(iii)slerflex 27695
[Conway] p. 17Theorem 3addsass 27941  addsassd 27942  addscom 27902  addscomd 27903  addsrid 27900  addsridd 27901
[Conway] p. 17Definitiondf-0s 27761
[Conway] p. 17Theorem 4(ii)negnegs 27979
[Conway] p. 17Theorem 4(iii)negsid 27976  negsidd 27977
[Conway] p. 18Theorem 5sleadd1 27925  sleadd1d 27931
[Conway] p. 18Definitiondf-1s 27762
[Conway] p. 18Theorem 6(ii)negscl 27971  negscld 27972
[Conway] p. 18Theorem 6(iii)addscld 27916
[Conway] p. 19Notemulsunif2 28102
[Conway] p. 19Theorem 7addsdi 28087  addsdid 28088  addsdird 28089  mulnegs1d 28092  mulnegs2d 28093  mulsass 28098  mulsassd 28099  mulscom 28071  mulscomd 28072
[Conway] p. 19Theorem 8(i)mulscl 28066  mulscld 28067
[Conway] p. 19Theorem 8(iii)slemuld 28070  sltmul 28068  sltmuld 28069
[Conway] p. 20Theorem 9mulsgt0 28076  mulsgt0d 28077
[Conway] p. 21Theorem 10(iv)precsex 28149
[Conway] p. 23Theorem 11eqscut3 27758
[Conway] p. 24Definitiondf-reno 28389
[Conway] p. 24Theorem 13(ii)readdscl 28394  remulscl 28397  renegscl 28393
[Conway] p. 27Definitiondf-ons 28182  elons2 28188
[Conway] p. 27Theorem 14sltonex 28192
[Conway] p. 28Theorem 15onscutlt 28194  onswe 28199
[Conway] p. 29Remarkmadebday 27838  newbday 27840  oldbday 27839
[Conway] p. 29Definitiondf-made 27781  df-new 27783  df-old 27782
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13757
[Crawley] p. 1Definition of posetdf-poset 18211
[Crawley] p. 107Theorem 13.2hlsupr 39404
[Crawley] p. 110Theorem 13.3arglem1N 40208  dalaw 39904
[Crawley] p. 111Theorem 13.4hlathil 41979
[Crawley] p. 111Definition of set Wdf-watsN 40008
[Crawley] p. 111Definition of dilationdf-dilN 40124  df-ldil 40122  isldil 40128
[Crawley] p. 111Definition of translationdf-ltrn 40123  df-trnN 40125  isltrn 40137  ltrnu 40139
[Crawley] p. 112Lemma Acdlema1N 39809  cdlema2N 39810  exatleN 39422
[Crawley] p. 112Lemma B1cvrat 39494  cdlemb 39812  cdlemb2 40059  cdlemb3 40624  idltrn 40168  l1cvat 39073  lhpat 40061  lhpat2 40063  lshpat 39074  ltrnel 40157  ltrnmw 40169
[Crawley] p. 112Lemma Ccdlemc1 40209  cdlemc2 40210  ltrnnidn 40192  trlat 40187  trljat1 40184  trljat2 40185  trljat3 40186  trlne 40203  trlnidat 40191  trlnle 40204
[Crawley] p. 112Definition of automorphismdf-pautN 40009
[Crawley] p. 113Lemma Ccdlemc 40215  cdlemc3 40211  cdlemc4 40212
[Crawley] p. 113Lemma Dcdlemd 40225  cdlemd1 40216  cdlemd2 40217  cdlemd3 40218  cdlemd4 40219  cdlemd5 40220  cdlemd6 40221  cdlemd7 40222  cdlemd8 40223  cdlemd9 40224  cdleme31sde 40403  cdleme31se 40400  cdleme31se2 40401  cdleme31snd 40404  cdleme32a 40459  cdleme32b 40460  cdleme32c 40461  cdleme32d 40462  cdleme32e 40463  cdleme32f 40464  cdleme32fva 40455  cdleme32fva1 40456  cdleme32fvcl 40458  cdleme32le 40465  cdleme48fv 40517  cdleme4gfv 40525  cdleme50eq 40559  cdleme50f 40560  cdleme50f1 40561  cdleme50f1o 40564  cdleme50laut 40565  cdleme50ldil 40566  cdleme50lebi 40558  cdleme50rn 40563  cdleme50rnlem 40562  cdlemeg49le 40529  cdlemeg49lebilem 40557
[Crawley] p. 113Lemma Ecdleme 40578  cdleme00a 40227  cdleme01N 40239  cdleme02N 40240  cdleme0a 40229  cdleme0aa 40228  cdleme0b 40230  cdleme0c 40231  cdleme0cp 40232  cdleme0cq 40233  cdleme0dN 40234  cdleme0e 40235  cdleme0ex1N 40241  cdleme0ex2N 40242  cdleme0fN 40236  cdleme0gN 40237  cdleme0moN 40243  cdleme1 40245  cdleme10 40272  cdleme10tN 40276  cdleme11 40288  cdleme11a 40278  cdleme11c 40279  cdleme11dN 40280  cdleme11e 40281  cdleme11fN 40282  cdleme11g 40283  cdleme11h 40284  cdleme11j 40285  cdleme11k 40286  cdleme11l 40287  cdleme12 40289  cdleme13 40290  cdleme14 40291  cdleme15 40296  cdleme15a 40292  cdleme15b 40293  cdleme15c 40294  cdleme15d 40295  cdleme16 40303  cdleme16aN 40277  cdleme16b 40297  cdleme16c 40298  cdleme16d 40299  cdleme16e 40300  cdleme16f 40301  cdleme16g 40302  cdleme19a 40321  cdleme19b 40322  cdleme19c 40323  cdleme19d 40324  cdleme19e 40325  cdleme19f 40326  cdleme1b 40244  cdleme2 40246  cdleme20aN 40327  cdleme20bN 40328  cdleme20c 40329  cdleme20d 40330  cdleme20e 40331  cdleme20f 40332  cdleme20g 40333  cdleme20h 40334  cdleme20i 40335  cdleme20j 40336  cdleme20k 40337  cdleme20l 40340  cdleme20l1 40338  cdleme20l2 40339  cdleme20m 40341  cdleme20y 40320  cdleme20zN 40319  cdleme21 40355  cdleme21d 40348  cdleme21e 40349  cdleme22a 40358  cdleme22aa 40357  cdleme22b 40359  cdleme22cN 40360  cdleme22d 40361  cdleme22e 40362  cdleme22eALTN 40363  cdleme22f 40364  cdleme22f2 40365  cdleme22g 40366  cdleme23a 40367  cdleme23b 40368  cdleme23c 40369  cdleme26e 40377  cdleme26eALTN 40379  cdleme26ee 40378  cdleme26f 40381  cdleme26f2 40383  cdleme26f2ALTN 40382  cdleme26fALTN 40380  cdleme27N 40387  cdleme27a 40385  cdleme27cl 40384  cdleme28c 40390  cdleme3 40255  cdleme30a 40396  cdleme31fv 40408  cdleme31fv1 40409  cdleme31fv1s 40410  cdleme31fv2 40411  cdleme31id 40412  cdleme31sc 40402  cdleme31sdnN 40405  cdleme31sn 40398  cdleme31sn1 40399  cdleme31sn1c 40406  cdleme31sn2 40407  cdleme31so 40397  cdleme35a 40466  cdleme35b 40468  cdleme35c 40469  cdleme35d 40470  cdleme35e 40471  cdleme35f 40472  cdleme35fnpq 40467  cdleme35g 40473  cdleme35h 40474  cdleme35h2 40475  cdleme35sn2aw 40476  cdleme35sn3a 40477  cdleme36a 40478  cdleme36m 40479  cdleme37m 40480  cdleme38m 40481  cdleme38n 40482  cdleme39a 40483  cdleme39n 40484  cdleme3b 40247  cdleme3c 40248  cdleme3d 40249  cdleme3e 40250  cdleme3fN 40251  cdleme3fa 40254  cdleme3g 40252  cdleme3h 40253  cdleme4 40256  cdleme40m 40485  cdleme40n 40486  cdleme40v 40487  cdleme40w 40488  cdleme41fva11 40495  cdleme41sn3aw 40492  cdleme41sn4aw 40493  cdleme41snaw 40494  cdleme42a 40489  cdleme42b 40496  cdleme42c 40490  cdleme42d 40491  cdleme42e 40497  cdleme42f 40498  cdleme42g 40499  cdleme42h 40500  cdleme42i 40501  cdleme42k 40502  cdleme42ke 40503  cdleme42keg 40504  cdleme42mN 40505  cdleme42mgN 40506  cdleme43aN 40507  cdleme43bN 40508  cdleme43cN 40509  cdleme43dN 40510  cdleme5 40258  cdleme50ex 40577  cdleme50ltrn 40575  cdleme51finvN 40574  cdleme51finvfvN 40573  cdleme51finvtrN 40576  cdleme6 40259  cdleme7 40267  cdleme7a 40261  cdleme7aa 40260  cdleme7b 40262  cdleme7c 40263  cdleme7d 40264  cdleme7e 40265  cdleme7ga 40266  cdleme8 40268  cdleme8tN 40273  cdleme9 40271  cdleme9a 40269  cdleme9b 40270  cdleme9tN 40275  cdleme9taN 40274  cdlemeda 40316  cdlemedb 40315  cdlemednpq 40317  cdlemednuN 40318  cdlemefr27cl 40421  cdlemefr32fva1 40428  cdlemefr32fvaN 40427  cdlemefrs32fva 40418  cdlemefrs32fva1 40419  cdlemefs27cl 40431  cdlemefs32fva1 40441  cdlemefs32fvaN 40440  cdlemesner 40314  cdlemeulpq 40238
[Crawley] p. 114Lemma E4atex 40094  4atexlem7 40093  cdleme0nex 40308  cdleme17a 40304  cdleme17c 40306  cdleme17d 40516  cdleme17d1 40307  cdleme17d2 40513  cdleme18a 40309  cdleme18b 40310  cdleme18c 40311  cdleme18d 40313  cdleme4a 40257
[Crawley] p. 115Lemma Ecdleme21a 40343  cdleme21at 40346  cdleme21b 40344  cdleme21c 40345  cdleme21ct 40347  cdleme21f 40350  cdleme21g 40351  cdleme21h 40352  cdleme21i 40353  cdleme22gb 40312
[Crawley] p. 116Lemma Fcdlemf 40581  cdlemf1 40579  cdlemf2 40580
[Crawley] p. 116Lemma Gcdlemftr1 40585  cdlemg16 40675  cdlemg28 40722  cdlemg28a 40711  cdlemg28b 40721  cdlemg3a 40615  cdlemg42 40747  cdlemg43 40748  cdlemg44 40751  cdlemg44a 40749  cdlemg46 40753  cdlemg47 40754  cdlemg9 40652  ltrnco 40737  ltrncom 40756  tgrpabl 40769  trlco 40745
[Crawley] p. 116Definition of Gdf-tgrp 40761
[Crawley] p. 117Lemma Gcdlemg17 40695  cdlemg17b 40680
[Crawley] p. 117Definition of Edf-edring-rN 40774  df-edring 40775
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40778
[Crawley] p. 118Remarktendopltp 40798
[Crawley] p. 118Lemma Hcdlemh 40835  cdlemh1 40833  cdlemh2 40834
[Crawley] p. 118Lemma Icdlemi 40838  cdlemi1 40836  cdlemi2 40837
[Crawley] p. 118Lemma Jcdlemj1 40839  cdlemj2 40840  cdlemj3 40841  tendocan 40842
[Crawley] p. 118Lemma Kcdlemk 40992  cdlemk1 40849  cdlemk10 40861  cdlemk11 40867  cdlemk11t 40964  cdlemk11ta 40947  cdlemk11tb 40949  cdlemk11tc 40963  cdlemk11u-2N 40907  cdlemk11u 40889  cdlemk12 40868  cdlemk12u-2N 40908  cdlemk12u 40890  cdlemk13-2N 40894  cdlemk13 40870  cdlemk14-2N 40896  cdlemk14 40872  cdlemk15-2N 40897  cdlemk15 40873  cdlemk16-2N 40898  cdlemk16 40875  cdlemk16a 40874  cdlemk17-2N 40899  cdlemk17 40876  cdlemk18-2N 40904  cdlemk18-3N 40918  cdlemk18 40886  cdlemk19-2N 40905  cdlemk19 40887  cdlemk19u 40988  cdlemk1u 40877  cdlemk2 40850  cdlemk20-2N 40910  cdlemk20 40892  cdlemk21-2N 40909  cdlemk21N 40891  cdlemk22-3 40919  cdlemk22 40911  cdlemk23-3 40920  cdlemk24-3 40921  cdlemk25-3 40922  cdlemk26-3 40924  cdlemk26b-3 40923  cdlemk27-3 40925  cdlemk28-3 40926  cdlemk29-3 40929  cdlemk3 40851  cdlemk30 40912  cdlemk31 40914  cdlemk32 40915  cdlemk33N 40927  cdlemk34 40928  cdlemk35 40930  cdlemk36 40931  cdlemk37 40932  cdlemk38 40933  cdlemk39 40934  cdlemk39u 40986  cdlemk4 40852  cdlemk41 40938  cdlemk42 40959  cdlemk42yN 40962  cdlemk43N 40981  cdlemk45 40965  cdlemk46 40966  cdlemk47 40967  cdlemk48 40968  cdlemk49 40969  cdlemk5 40854  cdlemk50 40970  cdlemk51 40971  cdlemk52 40972  cdlemk53 40975  cdlemk54 40976  cdlemk55 40979  cdlemk55u 40984  cdlemk56 40989  cdlemk5a 40853  cdlemk5auN 40878  cdlemk5u 40879  cdlemk6 40855  cdlemk6u 40880  cdlemk7 40866  cdlemk7u-2N 40906  cdlemk7u 40888  cdlemk8 40856  cdlemk9 40857  cdlemk9bN 40858  cdlemki 40859  cdlemkid 40954  cdlemkj-2N 40900  cdlemkj 40881  cdlemksat 40864  cdlemksel 40863  cdlemksv 40862  cdlemksv2 40865  cdlemkuat 40884  cdlemkuel-2N 40902  cdlemkuel-3 40916  cdlemkuel 40883  cdlemkuv-2N 40901  cdlemkuv2-2 40903  cdlemkuv2-3N 40917  cdlemkuv2 40885  cdlemkuvN 40882  cdlemkvcl 40860  cdlemky 40944  cdlemkyyN 40980  tendoex 40993
[Crawley] p. 120Remarkdva1dim 41003
[Crawley] p. 120Lemma Lcdleml1N 40994  cdleml2N 40995  cdleml3N 40996  cdleml4N 40997  cdleml5N 40998  cdleml6 40999  cdleml7 41000  cdleml8 41001  cdleml9 41002  dia1dim 41079
[Crawley] p. 120Lemma Mdia11N 41066  diaf11N 41067  dialss 41064  diaord 41065  dibf11N 41179  djajN 41155
[Crawley] p. 120Definition of isomorphism mapdiaval 41050
[Crawley] p. 121Lemma Mcdlemm10N 41136  dia2dimlem1 41082  dia2dimlem2 41083  dia2dimlem3 41084  dia2dimlem4 41085  dia2dimlem5 41086  diaf1oN 41148  diarnN 41147  dvheveccl 41130  dvhopN 41134
[Crawley] p. 121Lemma Ncdlemn 41230  cdlemn10 41224  cdlemn11 41229  cdlemn11a 41225  cdlemn11b 41226  cdlemn11c 41227  cdlemn11pre 41228  cdlemn2 41213  cdlemn2a 41214  cdlemn3 41215  cdlemn4 41216  cdlemn4a 41217  cdlemn5 41219  cdlemn5pre 41218  cdlemn6 41220  cdlemn7 41221  cdlemn8 41222  cdlemn9 41223  diclspsn 41212
[Crawley] p. 121Definition of phi(q)df-dic 41191
[Crawley] p. 122Lemma Ndih11 41283  dihf11 41285  dihjust 41235  dihjustlem 41234  dihord 41282  dihord1 41236  dihord10 41241  dihord11b 41240  dihord11c 41242  dihord2 41245  dihord2a 41237  dihord2b 41238  dihord2cN 41239  dihord2pre 41243  dihord2pre2 41244  dihordlem6 41231  dihordlem7 41232  dihordlem7b 41233
[Crawley] p. 122Definition of isomorphism mapdihffval 41248  dihfval 41249  dihval 41250
[Diestel] p. 3Definitiondf-gric 47891  df-grim 47888  isuspgrim 47906
[Diestel] p. 3Section 1.1df-cusgr 29383  df-nbgr 29304
[Diestel] p. 3Definition by df-grisom 47887
[Diestel] p. 4Section 1.1df-isubgr 47871  df-subgr 29239  uhgrspan1 29274  uhgrspansubgr 29262
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29526  vtxdgoddnumeven 29525
[Diestel] p. 27Section 1.10df-ushgr 29030
[EGA] p. 80Notation 1.1.1rspecval 33867
[EGA] p. 80Proposition 1.1.2zartop 33879
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33871  zarcls1 33872
[EGA] p. 81Corollary 1.1.8zart0 33882
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33885
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33888
[Eisenberg] p. 67Definition 5.3df-dif 3903
[Eisenberg] p. 82Definition 6.3dfom3 9532
[Eisenberg] p. 125Definition 8.21df-map 8747
[Eisenberg] p. 216Example 13.2(4)omenps 9540
[Eisenberg] p. 310Theorem 19.8cardprc 9865
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10438
[Enderton] p. 18Axiom of Empty Setaxnul 5241
[Enderton] p. 19Definitiondf-tp 4579
[Enderton] p. 26Exercise 5unissb 4889
[Enderton] p. 26Exercise 10pwel 5317
[Enderton] p. 28Exercise 7(b)pwun 5507
[Enderton] p. 30Theorem "Distributive laws"iinin1 5025  iinin2 5024  iinun2 5019  iunin1 5018  iunin1f 32527  iunin2 5017  uniin1 32521  uniin2 32522
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5023  iundif2 5020
[Enderton] p. 32Exercise 20unineq 4236
[Enderton] p. 33Exercise 23iinuni 5044
[Enderton] p. 33Exercise 25iununi 5045
[Enderton] p. 33Exercise 24(a)iinpw 5052
[Enderton] p. 33Exercise 24(b)iunpw 7699  iunpwss 5053
[Enderton] p. 36Definitionopthwiener 5452
[Enderton] p. 38Exercise 6(a)unipw 5389
[Enderton] p. 38Exercise 6(b)pwuni 4894
[Enderton] p. 41Lemma 3Dopeluu 5408  rnex 7835  rnexg 7827
[Enderton] p. 41Exercise 8dmuni 5852  rnuni 6092
[Enderton] p. 42Definition of a functiondffun7 6504  dffun8 6505
[Enderton] p. 43Definition of function valuefunfv2 6905
[Enderton] p. 43Definition of single-rootedfuncnv 6546
[Enderton] p. 44Definition (d)dfima2 6008  dfima3 6009
[Enderton] p. 47Theorem 3Hfvco2 6914
[Enderton] p. 49Axiom of Choice (first form)ac7 10356  ac7g 10357  df-ac 9999  dfac2 10015  dfac2a 10013  dfac2b 10014  dfac3 10004  dfac7 10016
[Enderton] p. 50Theorem 3K(a)imauni 7175
[Enderton] p. 52Definitiondf-map 8747
[Enderton] p. 53Exercise 21coass 6209
[Enderton] p. 53Exercise 27dmco 6198
[Enderton] p. 53Exercise 14(a)funin 6553
[Enderton] p. 53Exercise 22(a)imass2 6048
[Enderton] p. 54Remarkixpf 8839  ixpssmap 8851
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8817
[Enderton] p. 55Axiom of Choice (second form)ac9 10366  ac9s 10376
[Enderton] p. 56Theorem 3Meqvrelref 38626  erref 8637
[Enderton] p. 57Lemma 3Neqvrelthi 38629  erthi 8673
[Enderton] p. 57Definitiondf-ec 8619
[Enderton] p. 58Definitiondf-qs 8623
[Enderton] p. 61Exercise 35df-ec 8619
[Enderton] p. 65Exercise 56(a)dmun 5848
[Enderton] p. 68Definition of successordf-suc 6308
[Enderton] p. 71Definitiondf-tr 5197  dftr4 5202
[Enderton] p. 72Theorem 4Eunisuc 6383  unisucg 6382
[Enderton] p. 73Exercise 6unisuc 6383  unisucg 6382
[Enderton] p. 73Exercise 5(a)truni 5211
[Enderton] p. 73Exercise 5(b)trint 5213  trintALT 44892
[Enderton] p. 79Theorem 4I(A1)nna0 8514
[Enderton] p. 79Theorem 4I(A2)nnasuc 8516  onasuc 8438
[Enderton] p. 79Definition of operation valuedf-ov 7344
[Enderton] p. 80Theorem 4J(A1)nnm0 8515
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8517  onmsuc 8439
[Enderton] p. 81Theorem 4K(1)nnaass 8532
[Enderton] p. 81Theorem 4K(2)nna0r 8519  nnacom 8527
[Enderton] p. 81Theorem 4K(3)nndi 8533
[Enderton] p. 81Theorem 4K(4)nnmass 8534
[Enderton] p. 81Theorem 4K(5)nnmcom 8536
[Enderton] p. 82Exercise 16nnm0r 8520  nnmsucr 8535
[Enderton] p. 88Exercise 23nnaordex 8548
[Enderton] p. 129Definitiondf-en 8865
[Enderton] p. 132Theorem 6B(b)canth 7295
[Enderton] p. 133Exercise 1xpomen 9898
[Enderton] p. 133Exercise 2qnnen 16114
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9111
[Enderton] p. 135Corollary 6Cphp3 9113
[Enderton] p. 136Corollary 6Enneneq 9110
[Enderton] p. 136Corollary 6D(a)pssinf 9141
[Enderton] p. 136Corollary 6D(b)ominf 9143
[Enderton] p. 137Lemma 6Fpssnn 9073
[Enderton] p. 138Corollary 6Gssfi 9077
[Enderton] p. 139Theorem 6H(c)mapen 9049
[Enderton] p. 142Theorem 6I(3)xpdjuen 10063
[Enderton] p. 142Theorem 6I(4)mapdjuen 10064
[Enderton] p. 143Theorem 6Jdju0en 10059  dju1en 10055
[Enderton] p. 144Exercise 13iunfi 9222  unifi 9223  unifi2 9224
[Enderton] p. 144Corollary 6Kundif2 4425  unfi 9075  unfi2 9189
[Enderton] p. 145Figure 38ffoss 7873
[Enderton] p. 145Definitiondf-dom 8866
[Enderton] p. 146Example 1domen 8879  domeng 8880
[Enderton] p. 146Example 3nndomo 9121  nnsdom 9539  nnsdomg 9178
[Enderton] p. 149Theorem 6L(a)djudom2 10067
[Enderton] p. 149Theorem 6L(c)mapdom1 9050  xpdom1 8984  xpdom1g 8982  xpdom2g 8981
[Enderton] p. 149Theorem 6L(d)mapdom2 9056
[Enderton] p. 151Theorem 6Mzorn 10390  zorng 10387
[Enderton] p. 151Theorem 6M(4)ac8 10375  dfac5 10012
[Enderton] p. 159Theorem 6Qunictb 10458
[Enderton] p. 164Exampleinfdif 10091
[Enderton] p. 168Definitiondf-po 5522
[Enderton] p. 192Theorem 7M(a)oneli 6417
[Enderton] p. 192Theorem 7M(b)ontr1 6349
[Enderton] p. 192Theorem 7M(c)onirri 6416
[Enderton] p. 193Corollary 7N(b)0elon 6357
[Enderton] p. 193Corollary 7N(c)onsuci 7764
[Enderton] p. 193Corollary 7N(d)ssonunii 7709
[Enderton] p. 194Remarkonprc 7706
[Enderton] p. 194Exercise 16suc11 6411
[Enderton] p. 197Definitiondf-card 9824
[Enderton] p. 197Theorem 7Pcarden 10434
[Enderton] p. 200Exercise 25tfis 7780
[Enderton] p. 202Lemma 7Tr1tr 9661
[Enderton] p. 202Definitiondf-r1 9649
[Enderton] p. 202Theorem 7Qr1val1 9671
[Enderton] p. 204Theorem 7V(b)rankval4 9752
[Enderton] p. 206Theorem 7X(b)en2lp 9491
[Enderton] p. 207Exercise 30rankpr 9742  rankprb 9736  rankpw 9728  rankpwi 9708  rankuniss 9751
[Enderton] p. 207Exercise 34opthreg 9503
[Enderton] p. 208Exercise 35suc11reg 9504
[Enderton] p. 212Definition of alephalephval3 9993
[Enderton] p. 213Theorem 8A(a)alephord2 9959
[Enderton] p. 213Theorem 8A(b)cardalephex 9973
[Enderton] p. 218Theorem Schema 8Eonfununi 8256
[Enderton] p. 222Definition of kardkarden 9780  kardex 9779
[Enderton] p. 238Theorem 8Roeoa 8507
[Enderton] p. 238Theorem 8Soeoe 8509
[Enderton] p. 240Exercise 25oarec 8472
[Enderton] p. 257Definition of cofinalitycflm 10133
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17540
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17482
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18451  mrieqv2d 17537  mrieqvd 17536
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17541
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17546  mreexexlem2d 17543
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18457  mreexfidimd 17548
[Frege1879] p. 11Statementdf3or2 43780
[Frege1879] p. 12Statementdf3an2 43781  dfxor4 43778  dfxor5 43779
[Frege1879] p. 26Axiom 1ax-frege1 43802
[Frege1879] p. 26Axiom 2ax-frege2 43803
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43807
[Frege1879] p. 31Proposition 4frege4 43811
[Frege1879] p. 32Proposition 5frege5 43812
[Frege1879] p. 33Proposition 6frege6 43818
[Frege1879] p. 34Proposition 7frege7 43820
[Frege1879] p. 35Axiom 8ax-frege8 43821  axfrege8 43819
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37458
[Frege1879] p. 35Proposition 9frege9 43824
[Frege1879] p. 36Proposition 10frege10 43832
[Frege1879] p. 36Proposition 11frege11 43826
[Frege1879] p. 37Proposition 12frege12 43825
[Frege1879] p. 37Proposition 13frege13 43834
[Frege1879] p. 37Proposition 14frege14 43835
[Frege1879] p. 38Proposition 15frege15 43838
[Frege1879] p. 38Proposition 16frege16 43828
[Frege1879] p. 39Proposition 17frege17 43833
[Frege1879] p. 39Proposition 18frege18 43830
[Frege1879] p. 39Proposition 19frege19 43836
[Frege1879] p. 40Proposition 20frege20 43840
[Frege1879] p. 40Proposition 21frege21 43839
[Frege1879] p. 41Proposition 22frege22 43831
[Frege1879] p. 42Proposition 23frege23 43837
[Frege1879] p. 42Proposition 24frege24 43827
[Frege1879] p. 42Proposition 25frege25 43829  rp-frege25 43817
[Frege1879] p. 42Proposition 26frege26 43822
[Frege1879] p. 43Axiom 28ax-frege28 43842
[Frege1879] p. 43Proposition 27frege27 43823
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43843
[Frege1879] p. 44Axiom 31ax-frege31 43846  axfrege31 43845
[Frege1879] p. 44Proposition 30frege30 43844
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43847
[Frege1879] p. 44Proposition 33frege33 43848
[Frege1879] p. 45Proposition 34frege34 43849
[Frege1879] p. 45Proposition 35frege35 43850
[Frege1879] p. 45Proposition 36frege36 43851
[Frege1879] p. 46Proposition 37frege37 43852
[Frege1879] p. 46Proposition 38frege38 43853
[Frege1879] p. 46Proposition 39frege39 43854
[Frege1879] p. 46Proposition 40frege40 43855
[Frege1879] p. 47Axiom 41ax-frege41 43857  axfrege41 43856
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43858
[Frege1879] p. 47Proposition 43frege43 43859
[Frege1879] p. 47Proposition 44frege44 43860
[Frege1879] p. 47Proposition 45frege45 43861
[Frege1879] p. 48Proposition 46frege46 43862
[Frege1879] p. 48Proposition 47frege47 43863
[Frege1879] p. 49Proposition 48frege48 43864
[Frege1879] p. 49Proposition 49frege49 43865
[Frege1879] p. 49Proposition 50frege50 43866
[Frege1879] p. 50Axiom 52ax-frege52a 43869  ax-frege52c 43900  frege52aid 43870  frege52b 43901
[Frege1879] p. 50Axiom 54ax-frege54a 43874  ax-frege54c 43904  frege54b 43905
[Frege1879] p. 50Proposition 51frege51 43867
[Frege1879] p. 50Proposition 52dfsbcq 3741
[Frege1879] p. 50Proposition 53frege53a 43872  frege53aid 43871  frege53b 43902  frege53c 43926
[Frege1879] p. 50Proposition 54biid 261  eqid 2730
[Frege1879] p. 50Proposition 55frege55a 43880  frege55aid 43877  frege55b 43909  frege55c 43930  frege55cor1a 43881  frege55lem2a 43879  frege55lem2b 43908  frege55lem2c 43929
[Frege1879] p. 50Proposition 56frege56a 43883  frege56aid 43882  frege56b 43910  frege56c 43931
[Frege1879] p. 51Axiom 58ax-frege58a 43887  ax-frege58b 43913  frege58bid 43914  frege58c 43933
[Frege1879] p. 51Proposition 57frege57a 43885  frege57aid 43884  frege57b 43911  frege57c 43932
[Frege1879] p. 51Proposition 58spsbc 3752
[Frege1879] p. 51Proposition 59frege59a 43889  frege59b 43916  frege59c 43934
[Frege1879] p. 52Proposition 60frege60a 43890  frege60b 43917  frege60c 43935
[Frege1879] p. 52Proposition 61frege61a 43891  frege61b 43918  frege61c 43936
[Frege1879] p. 52Proposition 62frege62a 43892  frege62b 43919  frege62c 43937
[Frege1879] p. 52Proposition 63frege63a 43893  frege63b 43920  frege63c 43938
[Frege1879] p. 53Proposition 64frege64a 43894  frege64b 43921  frege64c 43939
[Frege1879] p. 53Proposition 65frege65a 43895  frege65b 43922  frege65c 43940
[Frege1879] p. 54Proposition 66frege66a 43896  frege66b 43923  frege66c 43941
[Frege1879] p. 54Proposition 67frege67a 43897  frege67b 43924  frege67c 43942
[Frege1879] p. 54Proposition 68frege68a 43898  frege68b 43925  frege68c 43943
[Frege1879] p. 55Definition 69dffrege69 43944
[Frege1879] p. 58Proposition 70frege70 43945
[Frege1879] p. 59Proposition 71frege71 43946
[Frege1879] p. 59Proposition 72frege72 43947
[Frege1879] p. 59Proposition 73frege73 43948
[Frege1879] p. 60Definition 76dffrege76 43951
[Frege1879] p. 60Proposition 74frege74 43949
[Frege1879] p. 60Proposition 75frege75 43950
[Frege1879] p. 62Proposition 77frege77 43952  frege77d 43758
[Frege1879] p. 63Proposition 78frege78 43953
[Frege1879] p. 63Proposition 79frege79 43954
[Frege1879] p. 63Proposition 80frege80 43955
[Frege1879] p. 63Proposition 81frege81 43956  frege81d 43759
[Frege1879] p. 64Proposition 82frege82 43957
[Frege1879] p. 65Proposition 83frege83 43958  frege83d 43760
[Frege1879] p. 65Proposition 84frege84 43959
[Frege1879] p. 66Proposition 85frege85 43960
[Frege1879] p. 66Proposition 86frege86 43961
[Frege1879] p. 66Proposition 87frege87 43962  frege87d 43762
[Frege1879] p. 67Proposition 88frege88 43963
[Frege1879] p. 68Proposition 89frege89 43964
[Frege1879] p. 68Proposition 90frege90 43965
[Frege1879] p. 68Proposition 91frege91 43966  frege91d 43763
[Frege1879] p. 69Proposition 92frege92 43967
[Frege1879] p. 70Proposition 93frege93 43968
[Frege1879] p. 70Proposition 94frege94 43969
[Frege1879] p. 70Proposition 95frege95 43970
[Frege1879] p. 71Definition 99dffrege99 43974
[Frege1879] p. 71Proposition 96frege96 43971  frege96d 43761
[Frege1879] p. 71Proposition 97frege97 43972  frege97d 43764
[Frege1879] p. 71Proposition 98frege98 43973  frege98d 43765
[Frege1879] p. 72Proposition 100frege100 43975
[Frege1879] p. 72Proposition 101frege101 43976
[Frege1879] p. 72Proposition 102frege102 43977  frege102d 43766
[Frege1879] p. 73Proposition 103frege103 43978
[Frege1879] p. 73Proposition 104frege104 43979
[Frege1879] p. 73Proposition 105frege105 43980
[Frege1879] p. 73Proposition 106frege106 43981  frege106d 43767
[Frege1879] p. 74Proposition 107frege107 43982
[Frege1879] p. 74Proposition 108frege108 43983  frege108d 43768
[Frege1879] p. 74Proposition 109frege109 43984  frege109d 43769
[Frege1879] p. 75Proposition 110frege110 43985
[Frege1879] p. 75Proposition 111frege111 43986  frege111d 43771
[Frege1879] p. 76Proposition 112frege112 43987
[Frege1879] p. 76Proposition 113frege113 43988
[Frege1879] p. 76Proposition 114frege114 43989  frege114d 43770
[Frege1879] p. 77Definition 115dffrege115 43990
[Frege1879] p. 77Proposition 116frege116 43991
[Frege1879] p. 78Proposition 117frege117 43992
[Frege1879] p. 78Proposition 118frege118 43993
[Frege1879] p. 78Proposition 119frege119 43994
[Frege1879] p. 78Proposition 120frege120 43995
[Frege1879] p. 79Proposition 121frege121 43996
[Frege1879] p. 79Proposition 122frege122 43997  frege122d 43772
[Frege1879] p. 79Proposition 123frege123 43998
[Frege1879] p. 80Proposition 124frege124 43999  frege124d 43773
[Frege1879] p. 81Proposition 125frege125 44000
[Frege1879] p. 81Proposition 126frege126 44001  frege126d 43774
[Frege1879] p. 82Proposition 127frege127 44002
[Frege1879] p. 83Proposition 128frege128 44003
[Frege1879] p. 83Proposition 129frege129 44004  frege129d 43775
[Frege1879] p. 84Proposition 130frege130 44005
[Frege1879] p. 85Proposition 131frege131 44006  frege131d 43776
[Frege1879] p. 86Proposition 132frege132 44007
[Frege1879] p. 86Proposition 133frege133 44008  frege133d 43777
[Fremlin1] p. 13Definition 111G (b)df-salgen 46330
[Fremlin1] p. 13Definition 111G (d)borelmbl 46653
[Fremlin1] p. 13Proposition 111G (b)salgenss 46353
[Fremlin1] p. 14Definition 112Aismea 46468
[Fremlin1] p. 15Remark 112B (d)psmeasure 46488
[Fremlin1] p. 15Property 112C (a)meadjun 46479  meadjunre 46493
[Fremlin1] p. 15Property 112C (b)meassle 46480
[Fremlin1] p. 15Property 112C (c)meaunle 46481
[Fremlin1] p. 16Property 112C (d)iundjiun 46477  meaiunle 46486  meaiunlelem 46485
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46498  meaiuninc2 46499  meaiuninc3 46502  meaiuninc3v 46501  meaiunincf 46500  meaiuninclem 46497
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46504  meaiininc2 46505  meaiininclem 46503
[Fremlin1] p. 19Theorem 113Ccaragen0 46523  caragendifcl 46531  caratheodory 46545  omelesplit 46535
[Fremlin1] p. 19Definition 113Aisome 46511  isomennd 46548  isomenndlem 46547
[Fremlin1] p. 19Remark 113B (c)omeunle 46533
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46552  voncmpl 46638
[Fremlin1] p. 19Definition 113A (ii)omessle 46515
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46540  carageniuncllem1 46538  carageniuncllem2 46539  caragenuncl 46530  caragenuncllem 46529  caragenunicl 46541
[Fremlin1] p. 21Remark 113Dcaragenel2d 46549
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46543  caratheodorylem2 46544
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46552
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46611  hoidmv1lelem1 46608  hoidmv1lelem2 46609  hoidmv1lelem3 46610
[Fremlin1] p. 25Definition 114Eisvonmbl 46655
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46611  hoidmvle 46617  hoidmvlelem1 46612  hoidmvlelem2 46613  hoidmvlelem3 46614  hoidmvlelem4 46615  hoidmvlelem5 46616  hsphoidmvle2 46602  hsphoif 46593  hsphoival 46596
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46565
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46573
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46600  hoidmvn0val 46601  hoidmvval 46594  hoidmvval0 46604  hoidmvval0b 46607
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46605  hsphoidmvle 46603
[Fremlin1] p. 30Definition 115Cdf-ovoln 46554  df-voln 46556
[Fremlin1] p. 30Proposition 115D (a)dmovn 46621  ovn0 46583  ovn0lem 46582  ovnf 46580  ovnome 46590  ovnssle 46578  ovnsslelem 46577  ovnsupge0 46574
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46620  ovnhoilem1 46618  ovnhoilem2 46619  vonhoi 46684
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46637  hoidifhspf 46635  hoidifhspval 46625  hoidifhspval2 46632  hoidifhspval3 46636  hspmbl 46646  hspmbllem1 46643  hspmbllem2 46644  hspmbllem3 46645
[Fremlin1] p. 31Definition 115Evoncmpl 46638  vonmea 46591
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46589  ovnsubadd2 46663  ovnsubadd2lem 46662  ovnsubaddlem1 46587  ovnsubaddlem2 46588
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46648  hoimbl2 46682  hoimbllem 46647  hspdifhsp 46633  opnvonmbl 46651  opnvonmbllem2 46650
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46653
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46696  iccvonmbllem 46695  ioovonmbl 46694
[Fremlin1] p. 32Proposition 115G (d)vonicc 46702  vonicclem2 46701  vonioo 46699  vonioolem2 46698  vonn0icc 46705  vonn0icc2 46709  vonn0ioo 46704  vonn0ioo2 46707
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46706  snvonmbl 46703  vonct 46710  vonsn 46708
[Fremlin1] p. 35Lemma 121Asubsalsal 46376
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46375  subsaliuncllem 46374
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46742  salpreimalegt 46726  salpreimaltle 46743
[Fremlin1] p. 35Proposition 121B (i)issmf 46745  issmff 46751  issmflem 46744
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46762  issmflelem 46761  smfpreimale 46771
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46773  issmfgtlem 46772
[Fremlin1] p. 36Definition 121Cdf-smblfn 46713  issmf 46745  issmff 46751  issmfge 46787  issmfgelem 46786  issmfgt 46773  issmfgtlem 46772  issmfle 46762  issmflelem 46761  issmflem 46744
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46724  salpreimagtlt 46747  salpreimalelt 46746
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46787  issmfgelem 46786
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46770
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46768  cnfsmf 46757
[Fremlin1] p. 36Proposition 121D (c)decsmf 46784  decsmflem 46783  incsmf 46759  incsmflem 46758
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46718  pimconstlt1 46719  smfconst 46766
[Fremlin1] p. 37Proposition 121E (b)smfadd 46782  smfaddlem1 46780  smfaddlem2 46781
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46813
[Fremlin1] p. 37Proposition 121E (d)smfmul 46812  smfmullem1 46808  smfmullem2 46809  smfmullem3 46810  smfmullem4 46811
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46814
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46817  smfpimbor1lem2 46816
[Fremlin1] p. 37Proposition 121E (g)smfco 46819
[Fremlin1] p. 37Proposition 121E (h)smfres 46807
[Fremlin1] p. 38Proposition 121E (e)smfrec 46806
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46815  smfresal 46805
[Fremlin1] p. 38Proposition 121F (a)smflim 46794  smflim2 46823  smflimlem1 46788  smflimlem2 46789  smflimlem3 46790  smflimlem4 46791  smflimlem5 46792  smflimlem6 46793  smflimmpt 46827
[Fremlin1] p. 38Proposition 121F (b)smfsup 46831  smfsuplem1 46828  smfsuplem2 46829  smfsuplem3 46830  smfsupmpt 46832  smfsupxr 46833
[Fremlin1] p. 38Proposition 121F (c)smfinf 46835  smfinflem 46834  smfinfmpt 46836
[Fremlin1] p. 39Remark 121Gsmflim 46794  smflim2 46823  smflimmpt 46827
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46825
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46855  smfdivdmmbl2 46858  smfinfdmmbl 46866  smfinfdmmbllem 46865  smfsupdmmbl 46862  smfsupdmmbllem 46861
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46845  smflimsuplem2 46838  smflimsuplem6 46842  smflimsuplem7 46843  smflimsuplem8 46844  smflimsupmpt 46846
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46848  smfliminflem 46847  smfliminfmpt 46849
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46713
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46859  fsupdm2 46860
[Fremlin1], p. 39Proposition 121Hadddmmbl 46850  adddmmbl2 46851  finfdm 46863  finfdm2 46864  fsupdm 46859  fsupdm2 46860  muldmmbl 46852  muldmmbl2 46853
[Fremlin1], p. 39Proposition 121F (c)finfdm 46863  finfdm2 46864
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25457
[Fremlin5] p. 213Lemma 565Cauniioovol 25500
[Fremlin5] p. 214Lemma 565Cauniioombl 25510
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37717
[Fremlin5] p. 220Theorem 565Maftc1anc 37720
[FreydScedrov] p. 283Axiom of Infinityax-inf 9523  inf1 9507  inf2 9508
[Gleason] p. 117Proposition 9-2.1df-enq 10794  enqer 10804
[Gleason] p. 117Proposition 9-2.2df-1nq 10799  df-nq 10795
[Gleason] p. 117Proposition 9-2.3df-plpq 10791  df-plq 10797
[Gleason] p. 119Proposition 9-2.4caovmo 7578  df-mpq 10792  df-mq 10798
[Gleason] p. 119Proposition 9-2.5df-rq 10800
[Gleason] p. 119Proposition 9-2.6ltexnq 10858
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10859  ltbtwnnq 10861
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10854
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10855
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10862
[Gleason] p. 121Definition 9-3.1df-np 10864
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10876
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10878
[Gleason] p. 122Definitiondf-1p 10865
[Gleason] p. 122Remark (1)prub 10877
[Gleason] p. 122Lemma 9-3.4prlem934 10916
[Gleason] p. 122Proposition 9-3.2df-ltp 10868
[Gleason] p. 122Proposition 9-3.3ltsopr 10915  psslinpr 10914  supexpr 10937  suplem1pr 10935  suplem2pr 10936
[Gleason] p. 123Proposition 9-3.5addclpr 10901  addclprlem1 10899  addclprlem2 10900  df-plp 10866
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10905
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10904
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10917
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10926  ltexprlem1 10919  ltexprlem2 10920  ltexprlem3 10921  ltexprlem4 10922  ltexprlem5 10923  ltexprlem6 10924  ltexprlem7 10925
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10928  ltaprlem 10927
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10929
[Gleason] p. 124Lemma 9-3.6prlem936 10930
[Gleason] p. 124Proposition 9-3.7df-mp 10867  mulclpr 10903  mulclprlem 10902  reclem2pr 10931
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10912
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10907
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10906
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10911
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10934  reclem3pr 10932  reclem4pr 10933
[Gleason] p. 126Proposition 9-4.1df-enr 10938  enrer 10946
[Gleason] p. 126Proposition 9-4.2df-0r 10943  df-1r 10944  df-nr 10939
[Gleason] p. 126Proposition 9-4.3df-mr 10941  df-plr 10940  negexsr 10985  recexsr 10990  recexsrlem 10986
[Gleason] p. 127Proposition 9-4.4df-ltr 10942
[Gleason] p. 130Proposition 10-1.3creui 12112  creur 12111  cru 12109
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11071  axcnre 11047
[Gleason] p. 132Definition 10-3.1crim 15014  crimd 15131  crimi 15092  crre 15013  crred 15130  crrei 15091
[Gleason] p. 132Definition 10-3.2remim 15016  remimd 15097
[Gleason] p. 133Definition 10.36absval2 15183  absval2d 15347  absval2i 15297
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15040  cjaddd 15119  cjaddi 15087
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15041  cjmuld 15120  cjmuli 15088
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15039  cjcjd 15098  cjcji 15070
[Gleason] p. 133Proposition 10-3.4(f)cjre 15038  cjreb 15022  cjrebd 15101  cjrebi 15073  cjred 15125  rere 15021  rereb 15019  rerebd 15100  rerebi 15072  rered 15123
[Gleason] p. 133Proposition 10-3.4(h)addcj 15047  addcjd 15111  addcji 15082
[Gleason] p. 133Proposition 10-3.7(a)absval 15137
[Gleason] p. 133Proposition 10-3.7(b)abscj 15178  abscjd 15352  abscji 15301
[Gleason] p. 133Proposition 10-3.7(c)abs00 15188  abs00d 15348  abs00i 15298  absne0d 15349
[Gleason] p. 133Proposition 10-3.7(d)releabs 15221  releabsd 15353  releabsi 15302
[Gleason] p. 133Proposition 10-3.7(f)absmul 15193  absmuld 15356  absmuli 15304
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15181  sqabsaddi 15305
[Gleason] p. 133Proposition 10-3.7(h)abstri 15230  abstrid 15358  abstrii 15308
[Gleason] p. 134Definition 10-4.1df-exp 13961  exp0 13964  expp1 13967  expp1d 14046
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26608  cxpaddd 26646  expadd 14003  expaddd 14047  expaddz 14005
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26617  cxpmuld 26666  expmul 14006  expmuld 14048  expmulz 14007
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26614  mulcxpd 26657  mulexp 14000  mulexpd 14060  mulexpz 14001
[Gleason] p. 140Exercise 1znnen 16113
[Gleason] p. 141Definition 11-2.1fzval 13401
[Gleason] p. 168Proposition 12-2.1(a)climadd 15531  rlimadd 15542  rlimdiv 15545
[Gleason] p. 168Proposition 12-2.1(b)climsub 15533  rlimsub 15543
[Gleason] p. 168Proposition 12-2.1(c)climmul 15532  rlimmul 15544
[Gleason] p. 171Corollary 12-2.2climmulc2 15536
[Gleason] p. 172Corollary 12-2.5climrecl 15482
[Gleason] p. 172Proposition 12-2.4(c)climabs 15503  climcj 15504  climim 15506  climre 15505  rlimabs 15508  rlimcj 15509  rlimim 15511  rlimre 15510
[Gleason] p. 173Definition 12-3.1df-ltxr 11143  df-xr 11142  ltxr 13006
[Gleason] p. 175Definition 12-4.1df-limsup 15370  limsupval 15373
[Gleason] p. 180Theorem 12-5.1climsup 15569
[Gleason] p. 180Theorem 12-5.3caucvg 15578  caucvgb 15579  caucvgbf 45506  caucvgr 15575  climcau 15570
[Gleason] p. 182Exercise 3cvgcmp 15715
[Gleason] p. 182Exercise 4cvgrat 15782
[Gleason] p. 195Theorem 13-2.12abs1m 15235
[Gleason] p. 217Lemma 13-4.1btwnzge0 13724
[Gleason] p. 223Definition 14-1.1df-met 21278
[Gleason] p. 223Definition 14-1.1(a)met0 24251  xmet0 24250
[Gleason] p. 223Definition 14-1.1(b)metgt0 24267
[Gleason] p. 223Definition 14-1.1(c)metsym 24258
[Gleason] p. 223Definition 14-1.1(d)mettri 24260  mstri 24377  xmettri 24259  xmstri 24376
[Gleason] p. 225Definition 14-1.5xpsmet 24290
[Gleason] p. 230Proposition 14-2.6txlm 23556
[Gleason] p. 240Theorem 14-4.3metcnp4 25230
[Gleason] p. 240Proposition 14-4.2metcnp3 24448
[Gleason] p. 243Proposition 14-4.16addcn 24774  addcn2 15493  mulcn 24776  mulcn2 15495  subcn 24775  subcn2 15494
[Gleason] p. 295Remarkbcval3 14205  bcval4 14206
[Gleason] p. 295Equation 2bcpasc 14220
[Gleason] p. 295Definition of binomial coefficientbcval 14203  df-bc 14202
[Gleason] p. 296Remarkbcn0 14209  bcnn 14211
[Gleason] p. 296Theorem 15-2.8binom 15729
[Gleason] p. 308Equation 2ef0 15990
[Gleason] p. 308Equation 3efcj 15991
[Gleason] p. 309Corollary 15-4.3efne0 15997
[Gleason] p. 309Corollary 15-4.4efexp 16002
[Gleason] p. 310Equation 14sinadd 16065
[Gleason] p. 310Equation 15cosadd 16066
[Gleason] p. 311Equation 17sincossq 16077
[Gleason] p. 311Equation 18cosbnd 16082  sinbnd 16081
[Gleason] p. 311Lemma 15-4.7sqeqor 14115  sqeqori 14113
[Gleason] p. 311Definition of ` `df-pi 15971
[Godowski] p. 730Equation SFgoeqi 32243
[GodowskiGreechie] p. 249Equation IV3oai 31638
[Golan] p. 1Remarksrgisid 20120
[Golan] p. 1Definitiondf-srg 20098
[Golan] p. 149Definitiondf-slmd 33160
[Gonshor] p. 7Definitiondf-scut 27716
[Gonshor] p. 9Theorem 2.5slerec 27753  slerecd 27754
[Gonshor] p. 10Theorem 2.6cofcut1 27857  cofcut1d 27858
[Gonshor] p. 10Theorem 2.7cofcut2 27859  cofcut2d 27860
[Gonshor] p. 12Theorem 2.9cofcutr 27861  cofcutr1d 27862  cofcutr2d 27863
[Gonshor] p. 13Definitiondf-adds 27896
[Gonshor] p. 14Theorem 3.1addsprop 27912
[Gonshor] p. 15Theorem 3.2addsunif 27938
[Gonshor] p. 17Theorem 3.4mulsprop 28062
[Gonshor] p. 18Theorem 3.5mulsunif 28082
[Gonshor] p. 28Lemma 4.2halfcut 28371
[Gonshor] p. 28Theorem 4.2pw2cut 28373
[Gonshor] p. 30Theorem 4.2addhalfcut 28372
[Gonshor] p. 95Theorem 6.1addsbday 27953
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36172
[Gratzer] p. 23Section 0.6df-mre 17480
[Gratzer] p. 27Section 0.6df-mri 17482
[Hall] p. 1Section 1.1df-asslaw 48198  df-cllaw 48196  df-comlaw 48197
[Hall] p. 2Section 1.2df-clintop 48210
[Hall] p. 7Section 1.3df-sgrp2 48231
[Halmos] p. 28Partition ` `df-parts 38782  dfmembpart2 38787
[Halmos] p. 31Theorem 17.3riesz1 32035  riesz2 32036
[Halmos] p. 41Definition of Hermitianhmopadj2 31911
[Halmos] p. 42Definition of projector orderingpjordi 32143
[Halmos] p. 43Theorem 26.1elpjhmop 32155  elpjidm 32154  pjnmopi 32118
[Halmos] p. 44Remarkpjinormi 31657  pjinormii 31646
[Halmos] p. 44Theorem 26.2elpjch 32159  pjrn 31677  pjrni 31672  pjvec 31666
[Halmos] p. 44Theorem 26.3pjnorm2 31697
[Halmos] p. 44Theorem 26.4hmopidmpj 32124  hmopidmpji 32122
[Halmos] p. 45Theorem 27.1pjinvari 32161
[Halmos] p. 45Theorem 27.3pjoci 32150  pjocvec 31667
[Halmos] p. 45Theorem 27.4pjorthcoi 32139
[Halmos] p. 48Theorem 29.2pjssposi 32142
[Halmos] p. 48Theorem 29.3pjssdif1i 32145  pjssdif2i 32144
[Halmos] p. 50Definition of spectrumdf-spec 31825
[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 24911  df-phtpy 24890
[Hatcher] p. 26Definitiondf-pco 24925  df-pi1 24928
[Hatcher] p. 26Proposition 1.2phtpcer 24914
[Hatcher] p. 26Proposition 1.3pi1grp 24970
[Hefferon] p. 240Definition 3.12df-dmat 22398  df-dmatalt 48409
[Helfgott] p. 2Theoremtgoldbach 47827
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47812
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47824  bgoldbtbnd 47819  bgoldbtbnd 47819  tgblthelfgott 47825
[Helfgott] p. 5Proposition 1.1circlevma 34645
[Helfgott] p. 69Statement 7.49circlemethhgt 34646
[Helfgott] p. 69Statement 7.50hgt750lema 34660  hgt750lemb 34659  hgt750leme 34661  hgt750lemf 34656  hgt750lemg 34657
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47821  tgoldbachgt 34666  tgoldbachgtALTV 47822  tgoldbachgtd 34665
[Helfgott] p. 70Statement 7.49ax-hgt749 34647
[Herstein] p. 54Exercise 28df-grpo 30463
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18849  grpoideu 30479  mndideu 18645
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18879  grpoinveu 30489
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18910  grpo2inv 30501
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18923  grpoinvop 30503
[Herstein] p. 57Exercise 1dfgrp3e 18945
[Hitchcock] p. 5Rule A3mptnan 1769
[Hitchcock] p. 5Rule A4mptxor 1770
[Hitchcock] p. 5Rule A5mtpxor 1772
[Holland] p. 1519Theorem 2sumdmdi 32390
[Holland] p. 1520Lemma 5cdj1i 32403  cdj3i 32411  cdj3lem1 32404  cdjreui 32402
[Holland] p. 1524Lemma 7mddmdin0i 32401
[Holland95] p. 13Theorem 3.6hlathil 41979
[Holland95] p. 14Line 15hgmapvs 41909
[Holland95] p. 14Line 16hdmaplkr 41931
[Holland95] p. 14Line 17hdmapellkr 41932
[Holland95] p. 14Line 19hdmapglnm2 41929
[Holland95] p. 14Line 20hdmapip0com 41935
[Holland95] p. 14Theorem 3.6hdmapevec2 41854
[Holland95] p. 14Lines 24 and 25hdmapoc 41949
[Holland95] p. 204Definition of involutiondf-srng 20748
[Holland95] p. 212Definition of subspacedf-psubsp 39521
[Holland95] p. 214Lemma 3.3lclkrlem2v 41546
[Holland95] p. 214Definition 3.2df-lpolN 41499
[Holland95] p. 214Definition of nonsingularpnonsingN 39951
[Holland95] p. 215Lemma 3.3(1)dihoml4 41395  poml4N 39971
[Holland95] p. 215Lemma 3.3(2)dochexmid 41486  pexmidALTN 39996  pexmidN 39987
[Holland95] p. 218Theorem 3.6lclkr 41551
[Holland95] p. 218Definition of dual vector spacedf-ldual 39142  ldualset 39143
[Holland95] p. 222Item 1df-lines 39519  df-pointsN 39520
[Holland95] p. 222Item 2df-polarityN 39921
[Holland95] p. 223Remarkispsubcl2N 39965  omllaw4 39264  pol1N 39928  polcon3N 39935
[Holland95] p. 223Definitiondf-psubclN 39953
[Holland95] p. 223Equation for polaritypolval2N 39924
[Holmes] p. 40Definitiondf-xrn 38378
[Hughes] p. 44Equation 1.21bax-his3 31054
[Hughes] p. 47Definition of projection operatordfpjop 32152
[Hughes] p. 49Equation 1.30eighmre 31933  eigre 31805  eigrei 31804
[Hughes] p. 49Equation 1.31eighmorth 31934  eigorth 31808  eigorthi 31807
[Hughes] p. 137Remark (ii)eigposi 31806
[Huneke] p. 1Claim 1frgrncvvdeq 30279
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30275
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30276
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30277
[Huneke] p. 2Claim 2frgrregorufr 30295  frgrregorufr0 30294  frgrregorufrg 30296
[Huneke] p. 2Claim 3frgrhash2wsp 30302  frrusgrord 30311  frrusgrord0 30310
[Huneke] p. 2Statementdf-clwwlknon 30058
[Huneke] p. 2Statement 4frgrwopreglem4 30285
[Huneke] p. 2Statement 5frgrwopreg1 30288  frgrwopreg2 30289  frgrwopregasn 30286  frgrwopregbsn 30287
[Huneke] p. 2Statement 6frgrwopreglem5 30291
[Huneke] p. 2Statement 7fusgreghash2wspv 30305
[Huneke] p. 2Statement 8fusgreghash2wsp 30308
[Huneke] p. 2Statement 9clwlksndivn 30056  numclwlk1 30341  numclwlk1lem1 30339  numclwlk1lem2 30340  numclwwlk1 30331  numclwwlk8 30362
[Huneke] p. 2Definition 3frgrwopreglem1 30282
[Huneke] p. 2Definition 4df-clwlks 29742
[Huneke] p. 2Definition 62clwwlk 30317
[Huneke] p. 2Definition 7numclwwlkovh 30343  numclwwlkovh0 30342
[Huneke] p. 2Statement 10numclwwlk2 30351
[Huneke] p. 2Statement 11rusgrnumwlkg 29948
[Huneke] p. 2Statement 12numclwwlk3 30355
[Huneke] p. 2Statement 13numclwwlk5 30358
[Huneke] p. 2Statement 14numclwwlk7 30361
[Indrzejczak] p. 33Definition ` `Enatded 30373  natded 30373
[Indrzejczak] p. 33Definition ` `Inatded 30373
[Indrzejczak] p. 34Definition ` `Enatded 30373  natded 30373
[Indrzejczak] p. 34Definition ` `Inatded 30373
[Jech] p. 4Definition of classcv 1540  cvjust 2724
[Jech] p. 42Lemma 6.1alephexp1 10462
[Jech] p. 42Equation 6.1alephadd 10460  alephmul 10461
[Jech] p. 43Lemma 6.2infmap 10459  infmap2 10100
[Jech] p. 71Lemma 9.3jech9.3 9699
[Jech] p. 72Equation 9.3scott0 9771  scottex 9770
[Jech] p. 72Exercise 9.1rankval4 9752
[Jech] p. 72Scheme "Collection Principle"cp 9776
[Jech] p. 78Noteopthprc 5678
[JonesMatijasevic] p. 694Definition 2.3rmxyval 42927
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43015
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43016
[JonesMatijasevic] p. 695Equation 2.7rmxadd 42939
[JonesMatijasevic] p. 695Equation 2.8rmyadd 42943
[JonesMatijasevic] p. 695Equation 2.9rmxp1 42944  rmyp1 42945
[JonesMatijasevic] p. 695Equation 2.10rmxm1 42946  rmym1 42947
[JonesMatijasevic] p. 695Equation 2.11rmx0 42937  rmx1 42938  rmxluc 42948
[JonesMatijasevic] p. 695Equation 2.12rmy0 42941  rmy1 42942  rmyluc 42949
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 42951
[JonesMatijasevic] p. 695Equation 2.14rmydbl 42952
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42972  jm2.17b 42973  jm2.17c 42974
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43005
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43009
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43000
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42975  jm2.24nn 42971
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43014
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43020  rmygeid 42976
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43032
[Juillerat] p. 11Section *5etransc 46300  etransclem47 46298  etransclem48 46299
[Juillerat] p. 12Equation (7)etransclem44 46295
[Juillerat] p. 12Equation *(7)etransclem46 46297
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46283
[Juillerat] p. 13Proofetransclem35 46286
[Juillerat] p. 13Part of case 2 proven inetransclem38 46289
[Juillerat] p. 13Part of case 2 provenetransclem24 46275
[Juillerat] p. 13Part of case 2: proven inetransclem41 46292
[Juillerat] p. 14Proofetransclem23 46274
[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 37526  wl-motae 37528  wl-moteq 37527
[KalishMontague] p. 87Lemma 8spimvw 1987  spimw 1971
[KalishMontague] p. 87Lemma 9spfw 2034  spw 2035
[Kalmbach] p. 14Definition of latticechabs1 31486  chabs1i 31488  chabs2 31487  chabs2i 31489  chjass 31503  chjassi 31456  latabs1 18373  latabs2 18374
[Kalmbach] p. 15Definition of atomdf-at 32308  ela 32309
[Kalmbach] p. 15Definition of coverscvbr2 32253  cvrval2 39292
[Kalmbach] p. 16Definitiondf-ol 39196  df-oml 39197
[Kalmbach] p. 20Definition of commutescmbr 31554  cmbri 31560  cmtvalN 39229  df-cm 31553  df-cmtN 39195
[Kalmbach] p. 22Remarkomllaw5N 39265  pjoml5 31583  pjoml5i 31558
[Kalmbach] p. 22Definitionpjoml2 31581  pjoml2i 31555
[Kalmbach] p. 22Theorem 2(v)cmcm 31584  cmcmi 31562  cmcmii 31567  cmtcomN 39267
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39263  omlsi 31374  pjoml 31406  pjomli 31405
[Kalmbach] p. 22Definition of OML lawomllaw2N 39262
[Kalmbach] p. 23Remarkcmbr2i 31566  cmcm3 31585  cmcm3i 31564  cmcm3ii 31569  cmcm4i 31565  cmt3N 39269  cmt4N 39270  cmtbr2N 39271
[Kalmbach] p. 23Lemma 3cmbr3 31578  cmbr3i 31570  cmtbr3N 39272
[Kalmbach] p. 25Theorem 5fh1 31588  fh1i 31591  fh2 31589  fh2i 31592  omlfh1N 39276
[Kalmbach] p. 65Remarkchjatom 32327  chslej 31468  chsleji 31428  shslej 31350  shsleji 31340
[Kalmbach] p. 65Proposition 1chocin 31465  chocini 31424  chsupcl 31310  chsupval2 31380  h0elch 31225  helch 31213  hsupval2 31379  ocin 31266  ococss 31263  shococss 31264
[Kalmbach] p. 65Definition of subspace sumshsval 31282
[Kalmbach] p. 66Remarkdf-pjh 31365  pjssmi 32135  pjssmii 31651
[Kalmbach] p. 67Lemma 3osum 31615  osumi 31612
[Kalmbach] p. 67Lemma 4pjci 32170
[Kalmbach] p. 103Exercise 6atmd2 32370
[Kalmbach] p. 103Exercise 12mdsl0 32280
[Kalmbach] p. 140Remarkhatomic 32330  hatomici 32329  hatomistici 32332
[Kalmbach] p. 140Proposition 1atlatmstc 39337
[Kalmbach] p. 140Proposition 1(i)atexch 32351  lsatexch 39061
[Kalmbach] p. 140Proposition 1(ii)chcv1 32325  cvlcvr1 39357  cvr1 39428
[Kalmbach] p. 140Proposition 1(iii)cvexch 32344  cvexchi 32339  cvrexch 39438
[Kalmbach] p. 149Remark 2chrelati 32334  hlrelat 39420  hlrelat5N 39419  lrelat 39032
[Kalmbach] p. 153Exercise 5lsmcv 21071  lsmsatcv 39028  spansncv 31623  spansncvi 31622
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39047  spansncv2 32263
[Kalmbach] p. 266Definitiondf-st 32181
[Kalmbach2] p. 8Definition of adjointdf-adjh 31819
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10529  fpwwe2 10526
[KanamoriPincus] p. 416Corollary 1.3canth4 10530
[KanamoriPincus] p. 417Corollary 1.6canthp1 10537
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10532
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10534
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10547
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10551  gchxpidm 10552
[KanamoriPincus] p. 419Theorem 2.1gchacg 10563  gchhar 10562
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10098  unxpwdom 9470
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10553
[Kreyszig] p. 3Property M1metcl 24240  xmetcl 24239
[Kreyszig] p. 4Property M2meteq0 24247
[Kreyszig] p. 8Definition 1.1-8dscmet 24480
[Kreyszig] p. 12Equation 5conjmul 11830  muleqadd 11753
[Kreyszig] p. 18Definition 1.3-2mopnval 24346
[Kreyszig] p. 19Remarkmopntopon 24347
[Kreyszig] p. 19Theorem T1mopn0 24406  mopnm 24352
[Kreyszig] p. 19Theorem T2unimopn 24404
[Kreyszig] p. 19Definition of neighborhoodneibl 24409
[Kreyszig] p. 20Definition 1.3-3metcnp2 24450
[Kreyszig] p. 25Definition 1.4-1lmbr 23166  lmmbr 25178  lmmbr2 25179
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23288
[Kreyszig] p. 28Theorem 1.4-5lmcau 25233
[Kreyszig] p. 28Definition 1.4-3iscau 25196  iscmet2 25214
[Kreyszig] p. 30Theorem 1.4-7cmetss 25236
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23369  metelcls 25225
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25226  metcld2 25227
[Kreyszig] p. 51Equation 2clmvneg1 25019  lmodvneg1 20831  nvinv 30609  vcm 30546
[Kreyszig] p. 51Equation 1aclm0vs 25015  lmod0vs 20821  slmd0vs 33183  vc0 30544
[Kreyszig] p. 51Equation 1blmodvs0 20822  slmdvs0 33184  vcz 30545
[Kreyszig] p. 58Definition 2.2-1imsmet 30661  ngpmet 24511  nrmmetd 24482
[Kreyszig] p. 59Equation 1imsdval 30656  imsdval2 30657  ncvspds 25081  ngpds 24512
[Kreyszig] p. 63Problem 1nmval 24497  nvnd 30658
[Kreyszig] p. 64Problem 2nmeq0 24526  nmge0 24525  nvge0 30643  nvz 30639
[Kreyszig] p. 64Problem 3nmrtri 24532  nvabs 30642
[Kreyszig] p. 91Definition 2.7-1isblo3i 30771
[Kreyszig] p. 92Equation 2df-nmoo 30715
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30777  blocni 30775
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30776
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25124  ipeq0 21568  ipz 30689
[Kreyszig] p. 135Problem 2cphpyth 25136  pythi 30820
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30824
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25158
[Kreyszig] p. 144Equation 4supcvg 15755
[Kreyszig] p. 144Theorem 3.3-1minvec 25356  minveco 30854
[Kreyszig] p. 196Definition 3.9-1df-aj 30720
[Kreyszig] p. 247Theorem 4.7-2bcth 25249
[Kreyszig] p. 249Theorem 4.7-3ubth 30843
[Kreyszig] p. 470Definition of positive operator orderingleop 32093  leopg 32092
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32111
[Kreyszig] p. 525Theorem 10.1-1htth 30888
[Kulpa] p. 547Theorempoimir 37672
[Kulpa] p. 547Equation (1)poimirlem32 37671
[Kulpa] p. 547Equation (2)poimirlem31 37670
[Kulpa] p. 548Theorembroucube 37673
[Kulpa] p. 548Equation (6)poimirlem26 37665
[Kulpa] p. 548Equation (7)poimirlem27 37666
[Kunen] p. 10Axiom 0ax6e 2382  axnul 5241
[Kunen] p. 11Axiom 3axnul 5241
[Kunen] p. 12Axiom 6zfrep6 7882
[Kunen] p. 24Definition 10.24mapval 8757  mapvalg 8755
[Kunen] p. 30Lemma 10.20fodomg 10405
[Kunen] p. 31Definition 10.24mapex 7866
[Kunen] p. 95Definition 2.1df-r1 9649
[Kunen] p. 97Lemma 2.10r1elss 9691  r1elssi 9690
[Kunen] p. 107Exercise 4rankop 9743  rankopb 9737  rankuni 9748  rankxplim 9764  rankxpsuc 9767
[Kunen2] p. 47Lemma I.9.9relpfr 44966
[Kunen2] p. 53Lemma I.9.21trfr 44974
[Kunen2] p. 53Lemma I.9.24(2)wffr 44973
[Kunen2] p. 53Definition I.9.20tcfr 44975
[Kunen2] p. 95Lemma I.16.2ralabso 44980  rexabso 44981
[Kunen2] p. 96Example I.16.3disjabso 44987  n0abso 44988  ssabso 44986
[Kunen2] p. 111Lemma II.2.4(1)traxext 44989
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 44999
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 44994
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 44997
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 44998
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 44993
[Kunen2] p. 112Corollary II.2.5wfaxext 45005  wfaxpr 45010  wfaxreg 45012  wfaxrep 45006  wfaxsep 45007  wfaxun 45011
[Kunen2] p. 113Lemma II.2.8pwclaxpow 44996
[Kunen2] p. 113Corollary II.2.9wfaxpow 45009
[Kunen2] p. 114Theorem II.2.13wfaxext 45005
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45004  omelaxinf2 45001
[Kunen2] p. 114Corollary II.2.12wfac8prim 45014  wfaxinf2 45013
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45027  permaxext 45017  permaxinf2 45025  permaxnul 45020  permaxpow 45021  permaxpr 45022  permaxrep 45018  permaxsep 45019  permaxun 45023
[Kunen2] p. 148Definition II.9.1brpermmodel 45015
[Kunen2] p. 149Exercise II.9.3permac8prim 45026
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4952
[Lang] , p. 225Corollary 1.3finexttrb 33668
[Lang] p. Definitiondf-rn 5625
[Lang] p. 3Statementlidrideqd 18569  mndbn0 18650
[Lang] p. 3Definitiondf-mnd 18635
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18587
[Lang] p. 4Property of composites. Second formulagsumccat 18741
[Lang] p. 5Equationgsumreidx 19822
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48192
[Lang] p. 6Examplenn0mnd 48189
[Lang] p. 6Equationgsumxp2 19885
[Lang] p. 6Statementcycsubm 19107
[Lang] p. 6Definitionmulgnn0gsum 18985
[Lang] p. 6Observationmndlsmidm 19575
[Lang] p. 7Definitiondfgrp2e 18868
[Lang] p. 30Definitiondf-tocyc 33066
[Lang] p. 32Property (a)cyc3genpm 33111
[Lang] p. 32Property (b)cyc3conja 33116  cycpmconjv 33101
[Lang] p. 53Definitiondf-cat 17566
[Lang] p. 53Axiom CAT 1cat1 17996  cat1lem 17995
[Lang] p. 54Definitiondf-iso 17648
[Lang] p. 57Definitiondf-inito 17883  df-termo 17884
[Lang] p. 58Exampleirinitoringc 21409
[Lang] p. 58Statementinitoeu1 17910  termoeu1 17917
[Lang] p. 62Definitiondf-func 17757
[Lang] p. 65Definitiondf-nat 17845
[Lang] p. 91Notedf-ringc 20554
[Lang] p. 92Statementmxidlprm 33425
[Lang] p. 92Definitionisprmidlc 33402
[Lang] p. 128Remarkdsmmlmod 21675
[Lang] p. 129Prooflincscm 48441  lincscmcl 48443  lincsum 48440  lincsumcl 48442
[Lang] p. 129Statementlincolss 48445
[Lang] p. 129Observationdsmmfi 21668
[Lang] p. 141Theorem 5.3dimkerim 33630  qusdimsum 33631
[Lang] p. 141Corollary 5.4lssdimle 33610
[Lang] p. 147Definitionsnlindsntor 48482
[Lang] p. 504Statementmat1 22355  matring 22351
[Lang] p. 504Definitiondf-mamu 22299
[Lang] p. 505Statementmamuass 22310  mamutpos 22366  matassa 22352  mattposvs 22363  tposmap 22365
[Lang] p. 513Definitionmdet1 22509  mdetf 22503
[Lang] p. 513Theorem 4.4cramer 22599
[Lang] p. 514Proposition 4.6mdetleib 22495
[Lang] p. 514Proposition 4.8mdettpos 22519
[Lang] p. 515Definitiondf-minmar1 22543  smadiadetr 22583
[Lang] p. 515Corollary 4.9mdetero 22518  mdetralt 22516
[Lang] p. 517Proposition 4.15mdetmul 22531
[Lang] p. 518Definitiondf-madu 22542
[Lang] p. 518Proposition 4.16madulid 22553  madurid 22552  matinv 22585
[Lang] p. 561Theorem 3.1cayleyhamilton 22798
[Lang], p. 224Proposition 1.1extdgfialg 33697  finextalg 33701
[Lang], p. 224Proposition 1.2extdgmul 33666  fedgmul 33634
[Lang], p. 225Proposition 1.4algextdeg 33728
[Lang], p. 561Remarkchpmatply1 22740
[Lang], p. 561Definitiondf-chpmat 22735
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44346
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44341
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44347
[LeBlanc] p. 277Rule R2axnul 5241
[Levy] p. 12Axiom 4.3.1df-clab 2709
[Levy] p. 59Definitiondf-ttrcl 9593
[Levy] p. 64Theorem 5.6(ii)frinsg 9636
[Levy] p. 338Axiomdf-clel 2804  df-cleq 2722
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2804  df-cleq 2722
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2709
[Levy] p. 358Axiomdf-clab 2709
[Levy58] p. 2Definition Iisfin1-3 10269
[Levy58] p. 2Definition IIdf-fin2 10169
[Levy58] p. 2Definition Iadf-fin1a 10168
[Levy58] p. 2Definition IIIdf-fin3 10171
[Levy58] p. 3Definition Vdf-fin5 10172
[Levy58] p. 3Definition IVdf-fin4 10170
[Levy58] p. 4Definition VIdf-fin6 10173
[Levy58] p. 4Definition VIIdf-fin7 10174
[Levy58], p. 3Theorem 1fin1a2 10298
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27618
[Lipparini] p. 3Lemma 2.1.4noresle 27629
[Lipparini] p. 6Proposition 4.2noinfbnd1 27661  nosupbnd1 27646
[Lipparini] p. 6Proposition 4.3noinfbnd2 27663  nosupbnd2 27648
[Lipparini] p. 7Theorem 5.1noetasuplem3 27667  noetasuplem4 27668
[Lipparini] p. 7Corollary 4.4nosupinfsep 27664
[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 32378
[Maeda] p. 168Lemma 5mdsym 32382  mdsymi 32381
[Maeda] p. 168Lemma 4(i)mdsymlem4 32376  mdsymlem6 32378  mdsymlem7 32379
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32380
[MaedaMaeda] p. 1Remarkssdmd1 32283  ssdmd2 32284  ssmd1 32281  ssmd2 32282
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32279
[MaedaMaeda] p. 1Definition 1.1df-dmd 32251  df-md 32250  mdbr 32264
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32301  mdslj1i 32289  mdslj2i 32290  mdslle1i 32287  mdslle2i 32288  mdslmd1i 32299  mdslmd2i 32300
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32291  mdsl2bi 32293  mdsl2i 32292
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32305
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32302
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32303
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32280
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32285  mdsl3 32286
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32304
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32399
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39339  hlrelat1 39418
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39057
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32306  cvmdi 32294  cvnbtwn4 32259  cvrnbtwn4 39297
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32307
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39358  cvp 32345  cvrp 39434  lcvp 39058
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32369
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32368
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39351  hlexch4N 39410
[MaedaMaeda] p. 34Exercise 7.1atabsi 32371
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39461
[MaedaMaeda] p. 61Definition 15.10psubN 39767  atpsubN 39771  df-pointsN 39520  pointpsubN 39769
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39522  pmap11 39780  pmaple 39779  pmapsub 39786  pmapval 39775
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39783  pmap1N 39785
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39788  pmapglb2N 39789  pmapglb2xN 39790  pmapglbx 39787
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39870
[MaedaMaeda] p. 67Postulate PS1ps-1 39495
[MaedaMaeda] p. 68Lemma 16.2df-padd 39814  paddclN 39860  paddidm 39859
[MaedaMaeda] p. 68Condition PS2ps-2 39496
[MaedaMaeda] p. 68Equation 16.2.1paddass 39856
[MaedaMaeda] p. 69Lemma 16.4ps-1 39495
[MaedaMaeda] p. 69Theorem 16.4ps-2 39496
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19580  lsmmod2 19581  lssats 39030  shatomici 32328  shatomistici 32331  shmodi 31360  shmodsi 31359
[MaedaMaeda] p. 130Remark 29.6dmdmd 32270  mdsymlem7 32379
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31559
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31463
[MaedaMaeda] p. 139Remarksumdmdii 32385
[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 30370
[Margaris] p. 59Section 14notnotrALTVD 44926
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 44927
[Margaris] p. 79Rule Cexinst01 44637  exinst11 44638
[Margaris] p. 89Theorem 19.219.2 1977  19.2g 2190  r19.2z 4443
[Margaris] p. 89Theorem 19.319.3 2204  rr19.3v 3620
[Margaris] p. 89Theorem 19.5alcom 2161
[Margaris] p. 89Theorem 19.6alex 1827
[Margaris] p. 89Theorem 19.7alnex 1782
[Margaris] p. 89Theorem 19.819.8a 2183
[Margaris] p. 89Theorem 19.919.9 2207  19.9h 2287  exlimd 2220  exlimdh 2291
[Margaris] p. 89Theorem 19.11excom 2164  excomim 2165
[Margaris] p. 89Theorem 19.1219.12 2327
[Margaris] p. 90Section 19conventions-labels 30371  conventions-labels 30371  conventions-labels 30371  conventions-labels 30371
[Margaris] p. 90Theorem 19.14exnal 1828
[Margaris] p. 90Theorem 19.152albi 44390  albi 1819
[Margaris] p. 90Theorem 19.1619.16 2227
[Margaris] p. 90Theorem 19.1719.17 2228
[Margaris] p. 90Theorem 19.182exbi 44392  exbi 1848
[Margaris] p. 90Theorem 19.1919.19 2231
[Margaris] p. 90Theorem 19.202alim 44389  2alimdv 1919  alimd 2214  alimdh 1818  alimdv 1917  ax-4 1810  ralimdaa 3231  ralimdv 3144  ralimdva 3142  ralimdvva 3177  sbcimdv 3808
[Margaris] p. 90Theorem 19.2119.21 2209  19.21h 2288  19.21t 2208  19.21vv 44388  alrimd 2217  alrimdd 2216  alrimdh 1864  alrimdv 1930  alrimi 2215  alrimih 1825  alrimiv 1928  alrimivv 1929  hbralrimi 3120  r19.21be 3223  r19.21bi 3222  ralrimd 3235  ralrimdv 3128  ralrimdva 3130  ralrimdvv 3174  ralrimdvva 3185  ralrimi 3228  ralrimia 3229  ralrimiv 3121  ralrimiva 3122  ralrimivv 3171  ralrimivva 3173  ralrimivvva 3176  ralrimivw 3126
[Margaris] p. 90Theorem 19.222exim 44391  2eximdv 1920  exim 1835  eximd 2218  eximdh 1865  eximdv 1918  rexim 3071  reximd2a 3240  reximdai 3232  reximdd 45164  reximddv 3146  reximddv2 3189  reximddv3 3147  reximdv 3145  reximdv2 3140  reximdva 3143  reximdvai 3141  reximdvva 3178  reximi2 3063
[Margaris] p. 90Theorem 19.2319.23 2213  19.23bi 2193  19.23h 2289  19.23t 2212  exlimdv 1934  exlimdvv 1935  exlimexi 44536  exlimiv 1931  exlimivv 1933  rexlimd3 45160  rexlimdv 3129  rexlimdv3a 3135  rexlimdva 3131  rexlimdva2 3133  rexlimdvaa 3132  rexlimdvv 3186  rexlimdvva 3187  rexlimdvvva 3188  rexlimdvw 3136  rexlimiv 3124  rexlimiva 3123  rexlimivv 3172
[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 2229  r19.27z 4453  r19.27zv 4454
[Margaris] p. 90Theorem 19.2819.28 2230  19.28vv 44398  r19.28z 4446  r19.28zf 45175  r19.28zv 4449  rr19.28v 3621
[Margaris] p. 90Theorem 19.2919.29 1874  r19.29d2r 3117  r19.29imd 3095
[Margaris] p. 90Theorem 19.3019.30 1882
[Margaris] p. 90Theorem 19.3119.31 2236  19.31vv 44396
[Margaris] p. 90Theorem 19.3219.32 2235  r19.32 47108
[Margaris] p. 90Theorem 19.3319.33-2 44394  19.33 1885
[Margaris] p. 90Theorem 19.3419.34 1993
[Margaris] p. 90Theorem 19.3519.35 1878
[Margaris] p. 90Theorem 19.3619.36 2232  19.36vv 44395  r19.36zv 4455
[Margaris] p. 90Theorem 19.3719.37 2234  19.37vv 44397  r19.37zv 4450
[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 3096
[Margaris] p. 90Theorem 19.4119.41 2237  19.41rg 44562
[Margaris] p. 90Theorem 19.4219.42 2238
[Margaris] p. 90Theorem 19.4319.43 1883
[Margaris] p. 90Theorem 19.4419.44 2239  r19.44zv 4452
[Margaris] p. 90Theorem 19.4519.45 2240  r19.45zv 4451
[Margaris] p. 110Exercise 2(b)eu1 2604
[Mayet] p. 370Remarkjpi 32240  largei 32237  stri 32227
[Mayet3] p. 9Definition of CH-statesdf-hst 32182  ishst 32184
[Mayet3] p. 10Theoremhstrbi 32236  hstri 32235
[Mayet3] p. 1223Theorem 4.1mayete3i 31698
[Mayet3] p. 1240Theorem 7.1mayetes3i 31699
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32248
[MegPav2000] p. 2345Definition 3.4-1chintcl 31302  chsupcl 31310
[MegPav2000] p. 2345Definition 3.4-2hatomic 32330
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32324
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32351
[MegPav2000] p. 2366Figure 7pl42N 40001
[MegPav2002] p. 362Lemma 2.2latj31 18385  latj32 18383  latjass 18381
[Megill] p. 444Axiom C5ax-5 1911  ax5ALT 38925
[Megill] p. 444Section 7conventions 30370
[Megill] p. 445Lemma L12aecom-o 38919  ax-c11n 38906  axc11n 2425
[Megill] p. 446Lemma L17equtrr 2023
[Megill] p. 446Lemma L18ax6fromc10 38914
[Megill] p. 446Lemma L19hbnae-o 38946  hbnae 2431
[Megill] p. 447Remark 9.1dfsb1 2480  sbid 2257  sbidd-misc 49730  sbidd 49729
[Megill] p. 448Remark 9.6axc14 2462
[Megill] p. 448Scheme C4'ax-c4 38902
[Megill] p. 448Scheme C5'ax-c5 38901  sp 2185
[Megill] p. 448Scheme C6'ax-11 2159
[Megill] p. 448Scheme C7'ax-c7 38903
[Megill] p. 448Scheme C8'ax-7 2009
[Megill] p. 448Scheme C9'ax-c9 38908
[Megill] p. 448Scheme C10'ax-6 1968  ax-c10 38904
[Megill] p. 448Scheme C11'ax-c11 38905
[Megill] p. 448Scheme C12'ax-8 2112
[Megill] p. 448Scheme C13'ax-9 2120
[Megill] p. 448Scheme C14'ax-c14 38909
[Megill] p. 448Scheme C15'ax-c15 38907
[Megill] p. 448Scheme C16'ax-c16 38910
[Megill] p. 448Theorem 9.4dral1-o 38922  dral1 2438  dral2-o 38948  dral2 2437  drex1 2440  drex2 2441  drsb1 2494  drsb2 2268
[Megill] p. 449Theorem 9.7sbcom2 2175  sbequ 2085  sbid2v 2508
[Megill] p. 450Example in Appendixhba1-o 38915  hba1 2294
[Mendelson] p. 35Axiom A3hirstL-ax3 46902
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3828  rspsbca 3829  stdpc4 2070
[Mendelson] p. 69Axiom 5ax-c4 38902  ra4 3835  stdpc5 2210
[Mendelson] p. 81Rule Cexlimiv 1931
[Mendelson] p. 95Axiom 6stdpc6 2029
[Mendelson] p. 95Axiom 7stdpc7 2252
[Mendelson] p. 225Axiom system NBGru 3737
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5452
[Mendelson] p. 231Exercise 4.10(k)inv1 4346
[Mendelson] p. 231Exercise 4.10(l)unv 4347
[Mendelson] p. 231Exercise 4.10(n)dfin3 4225
[Mendelson] p. 231Exercise 4.10(o)df-nul 4282
[Mendelson] p. 231Exercise 4.10(q)dfin4 4226
[Mendelson] p. 231Exercise 4.10(s)ddif 4089
[Mendelson] p. 231Definition of uniondfun3 4224
[Mendelson] p. 235Exercise 4.12(c)univ 5390
[Mendelson] p. 235Exercise 4.12(d)pwv 4854
[Mendelson] p. 235Exercise 4.12(j)pwin 5505
[Mendelson] p. 235Exercise 4.12(k)pwunss 4566
[Mendelson] p. 235Exercise 4.12(l)pwssun 5506
[Mendelson] p. 235Exercise 4.12(n)uniin 4881
[Mendelson] p. 235Exercise 4.12(p)reli 5764
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6212
[Mendelson] p. 244Proposition 4.8(g)epweon 7703
[Mendelson] p. 246Definition of successordf-suc 6308
[Mendelson] p. 250Exercise 4.36oelim2 8505
[Mendelson] p. 254Proposition 4.22(b)xpen 9048
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8969  xpsneng 8970
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8976  xpcomeng 8977
[Mendelson] p. 254Proposition 4.22(e)xpassen 8979
[Mendelson] p. 255Definitionbrsdom 8892
[Mendelson] p. 255Exercise 4.39endisj 8972
[Mendelson] p. 255Exercise 4.41mapprc 8749
[Mendelson] p. 255Exercise 4.43mapsnen 8954  mapsnend 8953
[Mendelson] p. 255Exercise 4.45mapunen 9054
[Mendelson] p. 255Exercise 4.47xpmapen 9053
[Mendelson] p. 255Exercise 4.42(a)map0e 8801
[Mendelson] p. 255Exercise 4.42(b)map1 8957
[Mendelson] p. 257Proposition 4.24(a)undom 8973
[Mendelson] p. 258Exercise 4.56(c)djuassen 10062  djucomen 10061
[Mendelson] p. 258Exercise 4.56(f)djudom1 10066
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10060
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8441
[Mendelson] p. 266Proposition 4.34(f)oaordex 8468
[Mendelson] p. 275Proposition 4.42(d)entri3 10442
[Mendelson] p. 281Definitiondf-r1 9649
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9698
[Mendelson] p. 287Axiom system MKru 3737
[MertziosUnger] p. 152Definitiondf-frgr 30229
[MertziosUnger] p. 153Remark 1frgrconngr 30264
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30266  vdgn1frgrv3 30267
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30268
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30261
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30254  2pthfrgrrn 30252  2pthfrgrrn2 30253
[Mittelstaedt] p. 9Definitiondf-oc 31222
[Monk1] p. 22Remarkconventions 30370
[Monk1] p. 22Theorem 3.1conventions 30370
[Monk1] p. 26Theorem 2.8(vii)ssin 4187
[Monk1] p. 33Theorem 3.2(i)ssrel 5721  ssrelf 32588
[Monk1] p. 33Theorem 3.2(ii)eqrel 5722
[Monk1] p. 34Definition 3.3df-opab 5152
[Monk1] p. 36Theorem 3.7(i)coi1 6206  coi2 6207
[Monk1] p. 36Theorem 3.8(v)dm0 5858  rn0 5863
[Monk1] p. 36Theorem 3.7(ii)cnvi 6085
[Monk1] p. 37Theorem 3.13(i)relxp 5632
[Monk1] p. 37Theorem 3.13(x)dmxp 5866  rnxp 6114
[Monk1] p. 37Theorem 3.13(ii)0xp 5713  xp0 6102
[Monk1] p. 38Theorem 3.16(ii)ima0 6023
[Monk1] p. 38Theorem 3.16(viii)imai 6020
[Monk1] p. 39Theorem 3.17imaex 7839  imaexg 7838
[Monk1] p. 39Theorem 3.16(xi)imassrn 6017
[Monk1] p. 41Theorem 4.3(i)fnopfv 7003  funfvop 6978
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6871
[Monk1] p. 42Theorem 4.4(iii)fvelima 6882
[Monk1] p. 43Theorem 4.6funun 6523
[Monk1] p. 43Theorem 4.8(iv)dff13 7183  dff13f 7184
[Monk1] p. 46Theorem 4.15(v)funex 7148  funrnex 7881
[Monk1] p. 50Definition 5.4fniunfv 7176
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6171
[Monk1] p. 52Theorem 5.11(viii)ssint 4912
[Monk1] p. 52Definition 5.13 (i)1stval2 7933  df-1st 7916
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7934  df-2nd 7917
[Monk1] p. 112Theorem 15.17(v)ranksn 9739  ranksnb 9712
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9740
[Monk1] p. 112Theorem 15.17(iii)rankun 9741  rankunb 9735
[Monk1] p. 113Theorem 15.18r1val3 9723
[Monk1] p. 113Definition 15.19df-r1 9649  r1val2 9722
[Monk1] p. 117Lemmazorn2 10389  zorn2g 10386
[Monk1] p. 133Theorem 18.11cardom 9871
[Monk1] p. 133Theorem 18.12canth3 10444
[Monk1] p. 133Theorem 18.14carduni 9866
[Monk2] p. 105Axiom C4ax-4 1810
[Monk2] p. 105Axiom C7ax-7 2009
[Monk2] p. 105Axiom C8ax-12 2179  ax-c15 38907  ax12v2 2181
[Monk2] p. 108Lemma 5ax-c4 38902
[Monk2] p. 109Lemma 12ax-11 2159
[Monk2] p. 109Lemma 15equvini 2454  equvinv 2030  eqvinop 5425
[Monk2] p. 113Axiom C5-1ax-5 1911  ax5ALT 38925
[Monk2] p. 113Axiom C5-2ax-10 2143
[Monk2] p. 113Axiom C5-3ax-11 2159
[Monk2] p. 114Lemma 21sp 2185
[Monk2] p. 114Lemma 22axc4 2321  hba1-o 38915  hba1 2294
[Monk2] p. 114Lemma 23nfia1 2155
[Monk2] p. 114Lemma 24nfa2 2178  nfra2 3340  nfra2w 3266
[Moore] p. 53Part Idf-mre 17480
[Munkres] p. 77Example 2distop 22903  indistop 22910  indistopon 22909
[Munkres] p. 77Example 3fctop 22912  fctop2 22913
[Munkres] p. 77Example 4cctop 22914
[Munkres] p. 78Definition of basisdf-bases 22854  isbasis3g 22857
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17339  tgval2 22864
[Munkres] p. 79Remarktgcl 22877
[Munkres] p. 80Lemma 2.1tgval3 22871
[Munkres] p. 80Lemma 2.2tgss2 22895  tgss3 22894
[Munkres] p. 81Lemma 2.3basgen 22896  basgen2 22897
[Munkres] p. 83Exercise 3topdifinf 37362  topdifinfeq 37363  topdifinffin 37361  topdifinfindis 37359
[Munkres] p. 89Definition of subspace topologyresttop 23068
[Munkres] p. 93Theorem 6.1(1)0cld 22946  topcld 22943
[Munkres] p. 93Theorem 6.1(2)iincld 22947
[Munkres] p. 93Theorem 6.1(3)uncld 22949
[Munkres] p. 94Definition of closureclsval 22945
[Munkres] p. 94Definition of interiorntrval 22944
[Munkres] p. 95Theorem 6.5(a)clsndisj 22983  elcls 22981
[Munkres] p. 95Theorem 6.5(b)elcls3 22991
[Munkres] p. 97Theorem 6.6clslp 23056  neindisj 23025
[Munkres] p. 97Corollary 6.7cldlp 23058
[Munkres] p. 97Definition of limit pointislp2 23053  lpval 23047
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23223
[Munkres] p. 102Definition of continuous functiondf-cn 23135  iscn 23143  iscn2 23146
[Munkres] p. 107Theorem 7.2(g)cncnp 23188  cncnp2 23189  cncnpi 23186  df-cnp 23136  iscnp 23145  iscnp2 23147
[Munkres] p. 127Theorem 10.1metcn 24451
[Munkres] p. 128Theorem 10.3metcn4 25231
[Nathanson] p. 123Remarkreprgt 34624  reprinfz1 34625  reprlt 34622
[Nathanson] p. 123Definitiondf-repr 34612
[Nathanson] p. 123Chapter 5.1circlemethnat 34644
[Nathanson] p. 123Propositionbreprexp 34636  breprexpnat 34637  itgexpif 34609
[NielsenChuang] p. 195Equation 4.73unierri 32074
[OeSilva] p. 2042Section 2ax-bgbltosilva 47820
[Pfenning] p. 17Definition XMnatded 30373
[Pfenning] p. 17Definition NNCnatded 30373  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30373
[Pfenning] p. 18Rule"natded 30373
[Pfenning] p. 18Definition /\Inatded 30373
[Pfenning] p. 18Definition ` `Enatded 30373  natded 30373  natded 30373  natded 30373  natded 30373
[Pfenning] p. 18Definition ` `Inatded 30373  natded 30373  natded 30373  natded 30373  natded 30373
[Pfenning] p. 18Definition ` `ELnatded 30373
[Pfenning] p. 18Definition ` `ERnatded 30373
[Pfenning] p. 18Definition ` `Ea,unatded 30373
[Pfenning] p. 18Definition ` `IRnatded 30373
[Pfenning] p. 18Definition ` `Ianatded 30373
[Pfenning] p. 127Definition =Enatded 30373
[Pfenning] p. 127Definition =Inatded 30373
[Ponnusamy] p. 361Theorem 6.44cphip0l 25122  df-dip 30671  dip0l 30688  ip0l 21566
[Ponnusamy] p. 361Equation 6.45cphipval 25163  ipval 30673
[Ponnusamy] p. 362Equation I1dipcj 30684  ipcj 21564
[Ponnusamy] p. 362Equation I3cphdir 25125  dipdir 30812  ipdir 21569  ipdiri 30800
[Ponnusamy] p. 362Equation I4ipidsq 30680  nmsq 25114
[Ponnusamy] p. 362Equation 6.46ip0i 30795
[Ponnusamy] p. 362Equation 6.47ip1i 30797
[Ponnusamy] p. 362Equation 6.48ip2i 30798
[Ponnusamy] p. 363Equation I2cphass 25131  dipass 30815  ipass 21575  ipassi 30811
[Prugovecki] p. 186Definition of brabraval 31914  df-bra 31820
[Prugovecki] p. 376Equation 8.1df-kb 31821  kbval 31924
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32352
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39906
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32366  atcvat4i 32367  cvrat3 39460  cvrat4 39461  lsatcvat3 39070
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32252  cvrval 39287  df-cv 32249  df-lcv 39037  lspsncv0 21076
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39918
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39919
[Quine] p. 16Definition 2.1df-clab 2709  rabid 3414  rabidd 45171
[Quine] p. 17Definition 2.1''dfsb7 2280
[Quine] p. 18Definition 2.7df-cleq 2722
[Quine] p. 19Definition 2.9conventions 30370  df-v 3436
[Quine] p. 34Theorem 5.1eqabb 2868
[Quine] p. 35Theorem 5.2abid1 2865  abid2f 2923
[Quine] p. 40Theorem 6.1sb5 2277
[Quine] p. 40Theorem 6.2sb6 2087  sbalex 2244
[Quine] p. 41Theorem 6.3df-clel 2804
[Quine] p. 41Theorem 6.4eqid 2730  eqid1 30437
[Quine] p. 41Theorem 6.5eqcom 2737
[Quine] p. 42Theorem 6.6df-sbc 3740
[Quine] p. 42Theorem 6.7dfsbcq 3741  dfsbcq2 3742
[Quine] p. 43Theorem 6.8vex 3438
[Quine] p. 43Theorem 6.9isset 3448
[Quine] p. 44Theorem 7.3spcgf 3544  spcgv 3549  spcimgf 3503
[Quine] p. 44Theorem 6.11spsbc 3752  spsbcd 3753
[Quine] p. 44Theorem 6.12elex 3455
[Quine] p. 44Theorem 6.13elab 3633  elabg 3630  elabgf 3628
[Quine] p. 44Theorem 6.14noel 4286
[Quine] p. 48Theorem 7.2snprc 4668
[Quine] p. 48Definition 7.1df-pr 4577  df-sn 4575
[Quine] p. 49Theorem 7.4snss 4735  snssg 4734
[Quine] p. 49Theorem 7.5prss 4770  prssg 4769
[Quine] p. 49Theorem 7.6prid1 4713  prid1g 4711  prid2 4714  prid2g 4712  snid 4613  snidg 4611
[Quine] p. 51Theorem 7.12snex 5372
[Quine] p. 51Theorem 7.13prex 5373
[Quine] p. 53Theorem 8.2unisn 4876  unisnALT 44937  unisng 4875
[Quine] p. 53Theorem 8.3uniun 4880
[Quine] p. 54Theorem 8.6elssuni 4887
[Quine] p. 54Theorem 8.7uni0 4885
[Quine] p. 56Theorem 8.17uniabio 6447
[Quine] p. 56Definition 8.18dfaiota2 47096  dfiota2 6434
[Quine] p. 57Theorem 8.19aiotaval 47105  iotaval 6451
[Quine] p. 57Theorem 8.22iotanul 6457
[Quine] p. 58Theorem 8.23iotaex 6453
[Quine] p. 58Definition 9.1df-op 4581
[Quine] p. 61Theorem 9.5opabid 5463  opabidw 5462  opelopab 5480  opelopaba 5474  opelopabaf 5482  opelopabf 5483  opelopabg 5476  opelopabga 5471  opelopabgf 5478  oprabid 7373  oprabidw 7372
[Quine] p. 64Definition 9.11df-xp 5620
[Quine] p. 64Definition 9.12df-cnv 5622
[Quine] p. 64Definition 9.15df-id 5509
[Quine] p. 65Theorem 10.3fun0 6542
[Quine] p. 65Theorem 10.4funi 6509
[Quine] p. 65Theorem 10.5funsn 6530  funsng 6528
[Quine] p. 65Definition 10.1df-fun 6479
[Quine] p. 65Definition 10.2args 6038  dffv4 6814
[Quine] p. 68Definition 10.11conventions 30370  df-fv 6485  fv2 6812
[Quine] p. 124Theorem 17.3nn0opth2 14171  nn0opth2i 14170  nn0opthi 14169  omopthi 8571
[Quine] p. 177Definition 25.2df-rdg 8324
[Quine] p. 232Equation icarddom 10437
[Quine] p. 284Axiom 39(vi)funimaex 6565  funimaexg 6564
[Quine] p. 331Axiom system NFru 3737
[ReedSimon] p. 36Definition (iii)ax-his3 31054
[ReedSimon] p. 63Exercise 4(a)df-dip 30671  polid 31129  polid2i 31127  polidi 31128
[ReedSimon] p. 63Exercise 4(b)df-ph 30783
[ReedSimon] p. 195Remarklnophm 31989  lnophmi 31988
[Retherford] p. 49Exercise 1(i)leopadd 32102
[Retherford] p. 49Exercise 1(ii)leopmul 32104  leopmuli 32103
[Retherford] p. 49Exercise 1(iv)leoptr 32107
[Retherford] p. 49Definition VI.1df-leop 31822  leoppos 32096
[Retherford] p. 49Exercise 1(iii)leoptri 32106
[Retherford] p. 49Definition of operator orderingleop3 32095
[Roman] p. 4Definitiondf-dmat 22398  df-dmatalt 48409
[Roman] p. 18Part Preliminariesdf-rng 20064
[Roman] p. 19Part Preliminariesdf-ring 20146
[Roman] p. 46Theorem 1.6isldepslvec2 48496
[Roman] p. 112Noteisldepslvec2 48496  ldepsnlinc 48519  zlmodzxznm 48508
[Roman] p. 112Examplezlmodzxzequa 48507  zlmodzxzequap 48510  zlmodzxzldep 48515
[Roman] p. 170Theorem 7.8cayleyhamilton 22798
[Rosenlicht] p. 80Theoremheicant 37674
[Rosser] p. 281Definitiondf-op 4581
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34648
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34649
[Rotman] p. 28Remarkpgrpgt2nabl 48376  pmtr3ncom 19380
[Rotman] p. 31Theorem 3.4symggen2 19376
[Rotman] p. 42Theorem 3.15cayley 19319  cayleyth 19320
[Rudin] p. 164Equation 27efcan 15995
[Rudin] p. 164Equation 30efzval 16003
[Rudin] p. 167Equation 48absefi 16097
[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 6059
[Schechter] p. 51Definition of irreflexivityintirr 6062
[Schechter] p. 51Definition of symmetrycnvsym 6058
[Schechter] p. 51Definition of transitivitycotr 6056
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17480
[Schechter] p. 79Definition of Moore closuredf-mrc 17481
[Schechter] p. 82Section 4.5df-mrc 17481
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17483
[Schechter] p. 139Definition AC3dfac9 10020
[Schechter] p. 141Definition (MC)dfac11 43074
[Schechter] p. 149Axiom DC1ax-dc 10329  axdc3 10337
[Schechter] p. 187Definition of "ring with unit"isring 20148  isrngo 37916
[Schechter] p. 276Remark 11.6.espan0 31512
[Schechter] p. 276Definition of spandf-span 31279  spanval 31303
[Schechter] p. 428Definition 15.35bastop1 22901
[Schloeder] p. 1Lemma 1.3onelon 6327  onelord 43263  ordelon 6326  ordelord 6324
[Schloeder] p. 1Lemma 1.7onepsuc 43264  sucidg 6385
[Schloeder] p. 1Remark 1.50elon 6357  onsuc 7738  ord0 6356  ordsuci 7736
[Schloeder] p. 1Theorem 1.9epsoon 43265
[Schloeder] p. 1Definition 1.1dftr5 5200
[Schloeder] p. 1Definition 1.2dford3 43040  elon2 6313
[Schloeder] p. 1Definition 1.4df-suc 6308
[Schloeder] p. 1Definition 1.6epel 5517  epelg 5515
[Schloeder] p. 1Theorem 1.9(i)elirr 9480  epirron 43266  ordirr 6320
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43268  oneptr 43267  ontr1 6349
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6345  oneptri 43269  ordtri3or 6334
[Schloeder] p. 2Lemma 1.10ondif1 8411  ord0eln0 6358
[Schloeder] p. 2Lemma 1.13elsuci 6371  onsucss 43278  trsucss 6392
[Schloeder] p. 2Lemma 1.14ordsucss 7743
[Schloeder] p. 2Lemma 1.15onnbtwn 6398  ordnbtwn 6397
[Schloeder] p. 2Lemma 1.16orddif0suc 43280  ordnexbtwnsuc 43279
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10284  onsucf1lem 43281  onsucf1o 43284  onsucf1olem 43282  onsucrn 43283
[Schloeder] p. 2Lemma 1.18dflim7 43285
[Schloeder] p. 2Remark 1.12ordzsl 7770
[Schloeder] p. 2Theorem 1.10ondif1i 43274  ordne0gt0 43273
[Schloeder] p. 2Definition 1.11dflim6 43276  limnsuc 43277  onsucelab 43275
[Schloeder] p. 3Remark 1.21omex 9528
[Schloeder] p. 3Theorem 1.19tfinds 7785
[Schloeder] p. 3Theorem 1.22omelon 9531  ordom 7801
[Schloeder] p. 3Definition 1.20dfom3 9532
[Schloeder] p. 4Lemma 2.21onn 8550
[Schloeder] p. 4Lemma 2.7ssonuni 7708  ssorduni 7707
[Schloeder] p. 4Remark 2.4oa1suc 8441
[Schloeder] p. 4Theorem 1.23dfom5 9535  limom 7807
[Schloeder] p. 4Definition 2.1df-1o 8380  df1o2 8387
[Schloeder] p. 4Definition 2.3oa0 8426  oa0suclim 43287  oalim 8442  oasuc 8434
[Schloeder] p. 4Definition 2.5om0 8427  om0suclim 43288  omlim 8443  omsuc 8436
[Schloeder] p. 4Definition 2.6oe0 8432  oe0m1 8431  oe0suclim 43289  oelim 8444  oesuc 8437
[Schloeder] p. 5Lemma 2.10onsupuni 43241
[Schloeder] p. 5Lemma 2.11onsupsucismax 43291
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43292
[Schloeder] p. 5Lemma 2.13limexissup 43293  limexissupab 43295  limiun 43294  limuni 6364
[Schloeder] p. 5Lemma 2.14oa0r 8448
[Schloeder] p. 5Lemma 2.15om1 8452  om1om1r 43296  om1r 8453
[Schloeder] p. 5Remark 2.8oacl 8445  oaomoecl 43290  oecl 8447  omcl 8446
[Schloeder] p. 5Definition 2.9onsupintrab 43243
[Schloeder] p. 6Lemma 2.16oe1 8454
[Schloeder] p. 6Lemma 2.17oe1m 8455
[Schloeder] p. 6Lemma 2.18oe0rif 43297
[Schloeder] p. 6Theorem 2.19oasubex 43298
[Schloeder] p. 6Theorem 2.20nnacl 8521  nnamecl 43299  nnecl 8523  nnmcl 8522
[Schloeder] p. 7Lemma 3.1onsucwordi 43300
[Schloeder] p. 7Lemma 3.2oaword1 8462
[Schloeder] p. 7Lemma 3.3oaword2 8463
[Schloeder] p. 7Lemma 3.4oalimcl 8470
[Schloeder] p. 7Lemma 3.5oaltublim 43302
[Schloeder] p. 8Lemma 3.6oaordi3 43303
[Schloeder] p. 8Lemma 3.81oaomeqom 43305
[Schloeder] p. 8Lemma 3.10oa00 8469
[Schloeder] p. 8Lemma 3.11omge1 43309  omword1 8483
[Schloeder] p. 8Remark 3.9oaordnr 43308  oaordnrex 43307
[Schloeder] p. 8Theorem 3.7oaord3 43304
[Schloeder] p. 9Lemma 3.12omge2 43310  omword2 8484
[Schloeder] p. 9Lemma 3.13omlim2 43311
[Schloeder] p. 9Lemma 3.14omord2lim 43312
[Schloeder] p. 9Lemma 3.15omord2i 43313  omordi 8476
[Schloeder] p. 9Theorem 3.16omord 8478  omord2com 43314
[Schloeder] p. 10Lemma 3.172omomeqom 43315  df-2o 8381
[Schloeder] p. 10Lemma 3.19oege1 43318  oewordi 8501
[Schloeder] p. 10Lemma 3.20oege2 43319  oeworde 8503
[Schloeder] p. 10Lemma 3.21rp-oelim2 43320
[Schloeder] p. 10Lemma 3.22oeord2lim 43321
[Schloeder] p. 10Remark 3.18omnord1 43317  omnord1ex 43316
[Schloeder] p. 11Lemma 3.23oeord2i 43322
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43324
[Schloeder] p. 11Remark 3.26oenord1 43328  oenord1ex 43327
[Schloeder] p. 11Theorem 4.1oaomoencom 43329
[Schloeder] p. 11Theorem 4.2oaass 8471
[Schloeder] p. 11Theorem 3.24oeord2com 43323
[Schloeder] p. 12Theorem 4.3odi 8489
[Schloeder] p. 13Theorem 4.4omass 8490
[Schloeder] p. 14Remark 4.6oenass 43331
[Schloeder] p. 14Theorem 4.7oeoa 8507
[Schloeder] p. 15Lemma 5.1cantnftermord 43332
[Schloeder] p. 15Lemma 5.2cantnfub 43333  cantnfub2 43334
[Schloeder] p. 16Theorem 5.3cantnf2 43337
[Schwabhauser] p. 10Axiom A1axcgrrflx 28885  axtgcgrrflx 28433
[Schwabhauser] p. 10Axiom A2axcgrtr 28886
[Schwabhauser] p. 10Axiom A3axcgrid 28887  axtgcgrid 28434
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28419
[Schwabhauser] p. 11Axiom A4axsegcon 28898  axtgsegcon 28435  df-trkgcb 28421
[Schwabhauser] p. 11Axiom A5ax5seg 28909  axtg5seg 28436  df-trkgcb 28421
[Schwabhauser] p. 11Axiom A6axbtwnid 28910  axtgbtwnid 28437  df-trkgb 28420
[Schwabhauser] p. 12Axiom A7axpasch 28912  axtgpasch 28438  df-trkgb 28420
[Schwabhauser] p. 12Axiom A8axlowdim2 28931  df-trkg2d 34668
[Schwabhauser] p. 13Axiom A8axtglowdim2 28441
[Schwabhauser] p. 13Axiom A9axtgupdim2 28442  df-trkg2d 34668
[Schwabhauser] p. 13Axiom A10axeuclid 28934  axtgeucl 28443  df-trkge 28422
[Schwabhauser] p. 13Axiom A11axcont 28947  axtgcont 28440  axtgcont1 28439  df-trkgb 28420
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36000
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36002
[Schwabhauser] p. 27Theorem 2.3cgrtr 36005
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36009
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36010  tgcgrcomimp 28448  tgcgrcoml 28450  tgcgrcomr 28449
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36015  tgcgrtriv 28455
[Schwabhauser] p. 28Theorem 2.105segofs 36019  tg5segofs 34676
[Schwabhauser] p. 28Definition 2.10df-afs 34673  df-ofs 35996
[Schwabhauser] p. 29Theorem 2.11cgrextend 36021  tgcgrextend 28456
[Schwabhauser] p. 29Theorem 2.12segconeq 36023  tgsegconeq 28457
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36035  btwntriv2 36025  tgbtwntriv2 28458
[Schwabhauser] p. 30Theorem 3.2btwncomim 36026  tgbtwncom 28459
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36029  tgbtwntriv1 28462
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36030  tgbtwnswapid 28463
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36036  btwnintr 36032  tgbtwnexch2 28467  tgbtwnintr 28464
[Schwabhauser] p. 30Theorem 3.6btwnexch 36038  btwnexch3 36033  tgbtwnexch 28469  tgbtwnexch3 28465
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36037  tgbtwnouttr 28468  tgbtwnouttr2 28466
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28930
[Schwabhauser] p. 32Theorem 3.14btwndiff 36040  tgbtwndiff 28477
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28470  trisegint 36041
[Schwabhauser] p. 34Theorem 4.2ifscgr 36057  tgifscgr 28479
[Schwabhauser] p. 34Theorem 4.11colcom 28529  colrot1 28530  colrot2 28531  lncom 28593  lnrot1 28594  lnrot2 28595
[Schwabhauser] p. 34Definition 4.1df-ifs 36053
[Schwabhauser] p. 35Theorem 4.3cgrsub 36058  tgcgrsub 28480
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36068  tgcgrxfr 28489
[Schwabhauser] p. 35Statement 4.4ercgrg 28488
[Schwabhauser] p. 35Definition 4.4df-cgr3 36054  df-cgrg 28482
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28482
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36069  tgbtwnxfr 28501
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36075  colinearperm2 36077  colinearperm3 36076  colinearperm4 36078  colinearperm5 36079
[Schwabhauser] p. 36Definition 4.8df-ismt 28504
[Schwabhauser] p. 36Definition 4.10df-colinear 36052  tgellng 28524  tglng 28517
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36080
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36088  lnxfr 28537
[Schwabhauser] p. 37Theorem 4.14lineext 36089  lnext 28538
[Schwabhauser] p. 37Theorem 4.16fscgr 36093  tgfscgr 28539
[Schwabhauser] p. 37Theorem 4.17linecgr 36094  lncgr 28540
[Schwabhauser] p. 37Definition 4.15df-fs 36055
[Schwabhauser] p. 38Theorem 4.18lineid 36096  lnid 28541
[Schwabhauser] p. 38Theorem 4.19idinside 36097  tgidinside 28542
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36114  tgbtwnconn1 28546
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36115  tgbtwnconn2 28547
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36116  tgbtwnconn3 28548
[Schwabhauser] p. 41Theorem 5.5brsegle2 36122
[Schwabhauser] p. 41Definition 5.4df-segle 36120  legov 28556
[Schwabhauser] p. 41Definition 5.5legov2 28557
[Schwabhauser] p. 42Remark 5.13legso 28570
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36123
[Schwabhauser] p. 42Theorem 5.7seglerflx 36125
[Schwabhauser] p. 42Theorem 5.8segletr 36127
[Schwabhauser] p. 42Theorem 5.9segleantisym 36128
[Schwabhauser] p. 42Theorem 5.10seglelin 36129
[Schwabhauser] p. 42Theorem 5.11seglemin 36126
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36131
[Schwabhauser] p. 42Proposition 5.7legid 28558
[Schwabhauser] p. 42Proposition 5.8legtrd 28560
[Schwabhauser] p. 42Proposition 5.9legtri3 28561
[Schwabhauser] p. 42Proposition 5.10legtrid 28562
[Schwabhauser] p. 42Proposition 5.11leg0 28563
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36138
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36139
[Schwabhauser] p. 43Theorem 6.4broutsideof 36134  df-outsideof 36133
[Schwabhauser] p. 43Definition 6.1broutsideof2 36135  ishlg 28573
[Schwabhauser] p. 44Theorem 6.4hlln 28578
[Schwabhauser] p. 44Theorem 6.5hlid 28580  outsideofrflx 36140
[Schwabhauser] p. 44Theorem 6.6hlcomb 28574  hlcomd 28575  outsideofcom 36141
[Schwabhauser] p. 44Theorem 6.7hltr 28581  outsideoftr 36142
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28589  outsideofeu 36144
[Schwabhauser] p. 44Definition 6.8df-ray 36151
[Schwabhauser] p. 45Part 2df-lines2 36152
[Schwabhauser] p. 45Theorem 6.13outsidele 36145
[Schwabhauser] p. 45Theorem 6.15lineunray 36160
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36161  tglineelsb2 28603
[Schwabhauser] p. 45Theorem 6.17linecom 36163  linerflx1 36162  linerflx2 36164  tglinecom 28606  tglinerflx1 28604  tglinerflx2 28605
[Schwabhauser] p. 45Theorem 6.18linethru 36166  tglinethru 28607
[Schwabhauser] p. 45Definition 6.14df-line2 36150  tglng 28517
[Schwabhauser] p. 45Proposition 6.13legbtwn 28565
[Schwabhauser] p. 46Theorem 6.19linethrueu 36169  tglinethrueu 28610
[Schwabhauser] p. 46Theorem 6.21lineintmo 36170  tglineineq 28614  tglineinteq 28616  tglineintmo 28613
[Schwabhauser] p. 46Theorem 6.23colline 28620
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28621
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28622
[Schwabhauser] p. 49Theorem 7.3mirinv 28637
[Schwabhauser] p. 49Theorem 7.7mirmir 28633
[Schwabhauser] p. 49Theorem 7.8mirreu3 28625
[Schwabhauser] p. 49Definition 7.5df-mir 28624  ismir 28630  mirbtwn 28629  mircgr 28628  mirfv 28627  mirval 28626
[Schwabhauser] p. 50Theorem 7.8mirreu 28635
[Schwabhauser] p. 50Theorem 7.9mireq 28636
[Schwabhauser] p. 50Theorem 7.10mirinv 28637
[Schwabhauser] p. 50Theorem 7.11mirf1o 28640
[Schwabhauser] p. 50Theorem 7.13miriso 28641
[Schwabhauser] p. 51Theorem 7.14mirmot 28646
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28643  mirbtwni 28642
[Schwabhauser] p. 51Theorem 7.16mircgrs 28644
[Schwabhauser] p. 51Theorem 7.17miduniq 28656
[Schwabhauser] p. 52Lemma 7.21symquadlem 28660
[Schwabhauser] p. 52Theorem 7.18miduniq1 28657
[Schwabhauser] p. 52Theorem 7.19miduniq2 28658
[Schwabhauser] p. 52Theorem 7.20colmid 28659
[Schwabhauser] p. 53Lemma 7.22krippen 28662
[Schwabhauser] p. 55Lemma 7.25midexlem 28663
[Schwabhauser] p. 57Theorem 8.2ragcom 28669
[Schwabhauser] p. 57Definition 8.1df-rag 28665  israg 28668
[Schwabhauser] p. 58Theorem 8.3ragcol 28670
[Schwabhauser] p. 58Theorem 8.4ragmir 28671
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28673
[Schwabhauser] p. 58Theorem 8.6ragflat2 28674
[Schwabhauser] p. 58Theorem 8.7ragflat 28675
[Schwabhauser] p. 58Theorem 8.8ragtriva 28676
[Schwabhauser] p. 58Theorem 8.9ragflat3 28677  ragncol 28680
[Schwabhauser] p. 58Theorem 8.10ragcgr 28678
[Schwabhauser] p. 59Theorem 8.12perpcom 28684
[Schwabhauser] p. 59Theorem 8.13ragperp 28688
[Schwabhauser] p. 59Theorem 8.14perpneq 28685
[Schwabhauser] p. 59Definition 8.11df-perpg 28667  isperp 28683
[Schwabhauser] p. 59Definition 8.13isperp2 28686
[Schwabhauser] p. 60Theorem 8.18foot 28693
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28701  colperpexlem2 28702
[Schwabhauser] p. 63Theorem 8.21colperpex 28704  colperpexlem3 28703
[Schwabhauser] p. 64Theorem 8.22mideu 28709  midex 28708
[Schwabhauser] p. 66Lemma 8.24opphllem 28706
[Schwabhauser] p. 67Theorem 9.2oppcom 28715
[Schwabhauser] p. 67Definition 9.1islnopp 28710
[Schwabhauser] p. 68Lemma 9.3opphllem2 28719
[Schwabhauser] p. 68Lemma 9.4opphllem5 28722  opphllem6 28723
[Schwabhauser] p. 69Theorem 9.5opphl 28725
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28438
[Schwabhauser] p. 70Theorem 9.6outpasch 28726
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28734
[Schwabhauser] p. 71Definition 9.7df-hpg 28729  hpgbr 28731
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28736
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28735
[Schwabhauser] p. 72Theorem 9.11hpgid 28737
[Schwabhauser] p. 72Theorem 9.12hpgcom 28738
[Schwabhauser] p. 72Theorem 9.13hpgtr 28739
[Schwabhauser] p. 73Theorem 9.18colopp 28740
[Schwabhauser] p. 73Theorem 9.19colhp 28741
[Schwabhauser] p. 88Theorem 10.2lmieu 28755
[Schwabhauser] p. 88Definition 10.1df-mid 28745
[Schwabhauser] p. 89Theorem 10.4lmicom 28759
[Schwabhauser] p. 89Theorem 10.5lmilmi 28760
[Schwabhauser] p. 89Theorem 10.6lmireu 28761
[Schwabhauser] p. 89Theorem 10.7lmieq 28762
[Schwabhauser] p. 89Theorem 10.8lmiinv 28763
[Schwabhauser] p. 89Theorem 10.9lmif1o 28766
[Schwabhauser] p. 89Theorem 10.10lmiiso 28768
[Schwabhauser] p. 89Definition 10.3df-lmi 28746
[Schwabhauser] p. 90Theorem 10.11lmimot 28769
[Schwabhauser] p. 91Theorem 10.12hypcgr 28772
[Schwabhauser] p. 92Theorem 10.14lmiopp 28773
[Schwabhauser] p. 92Theorem 10.15lnperpex 28774
[Schwabhauser] p. 92Theorem 10.16trgcopy 28775  trgcopyeu 28777
[Schwabhauser] p. 95Definition 11.2dfcgra2 28801
[Schwabhauser] p. 95Definition 11.3iscgra 28780
[Schwabhauser] p. 95Proposition 11.4cgracgr 28789
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28787  cgrahl2 28788
[Schwabhauser] p. 96Theorem 11.6cgraid 28790
[Schwabhauser] p. 96Theorem 11.9cgraswap 28791
[Schwabhauser] p. 97Theorem 11.7cgracom 28793
[Schwabhauser] p. 97Theorem 11.8cgratr 28794
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28797  cgrahl 28798
[Schwabhauser] p. 98Theorem 11.13sacgr 28802
[Schwabhauser] p. 98Theorem 11.14oacgr 28803
[Schwabhauser] p. 98Theorem 11.15acopy 28804  acopyeu 28805
[Schwabhauser] p. 101Theorem 11.24inagswap 28812
[Schwabhauser] p. 101Theorem 11.25inaghl 28816
[Schwabhauser] p. 101Definition 11.23isinag 28809
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28824
[Schwabhauser] p. 102Definition 11.27df-leag 28817  isleag 28818
[Schwabhauser] p. 107Theorem 11.49tgsas 28826  tgsas1 28825  tgsas2 28827  tgsas3 28828
[Schwabhauser] p. 108Theorem 11.50tgasa 28830  tgasa1 28829
[Schwabhauser] p. 109Theorem 11.51tgsss1 28831  tgsss2 28832  tgsss3 28833
[Shapiro] p. 230Theorem 6.5.1dchrhash 27202  dchrsum 27200  dchrsum2 27199  sumdchr 27203
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27204  sum2dchr 27205
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19973  ablfacrp2 19974
[Shapiro], p. 328Equation 9.2.4vmasum 27147
[Shapiro], p. 329Equation 9.2.7logfac2 27148
[Shapiro], p. 329Equation 9.2.9logfacrlim 27155
[Shapiro], p. 331Equation 9.2.13vmadivsum 27413
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27416
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27470  vmalogdivsum2 27469
[Shapiro], p. 375Theorem 9.4.1dirith 27460  dirith2 27459
[Shapiro], p. 375Equation 9.4.3rplogsum 27458  rpvmasum 27457  rpvmasum2 27443
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27418
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27456
[Shapiro], p. 377Lemma 9.4.1dchrisum 27423  dchrisumlem1 27420  dchrisumlem2 27421  dchrisumlem3 27422  dchrisumlema 27419
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27426
[Shapiro], p. 379Equation 9.4.16dchrmusum 27455  dchrmusumlem 27453  dchrvmasumlem 27454
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27425
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27427
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27451  dchrisum0re 27444  dchrisumn0 27452
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27437
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27441
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27442
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27497  pntrsumbnd2 27498  pntrsumo1 27496
[Shapiro], p. 405Equation 10.2.1mudivsum 27461
[Shapiro], p. 406Equation 10.2.6mulogsum 27463
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27465
[Shapiro], p. 407Equation 10.2.8mulog2sum 27468
[Shapiro], p. 418Equation 10.4.6logsqvma 27473
[Shapiro], p. 418Equation 10.4.8logsqvma2 27474
[Shapiro], p. 419Equation 10.4.10selberg 27479
[Shapiro], p. 420Equation 10.4.12selberg2lem 27481
[Shapiro], p. 420Equation 10.4.14selberg2 27482
[Shapiro], p. 422Equation 10.6.7selberg3 27490
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27491
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27488  selberg3lem2 27489
[Shapiro], p. 422Equation 10.4.23selberg4 27492
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27486
[Shapiro], p. 428Equation 10.6.2selbergr 27499
[Shapiro], p. 429Equation 10.6.8selberg3r 27500
[Shapiro], p. 430Equation 10.6.11selberg4r 27501
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27515
[Shapiro], p. 434Equation 10.6.27pntlema 27527  pntlemb 27528  pntlemc 27526  pntlemd 27525  pntlemg 27529
[Shapiro], p. 435Equation 10.6.29pntlema 27527
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27519
[Shapiro], p. 436Lemma 10.6.2pntibnd 27524
[Shapiro], p. 436Equation 10.6.34pntlema 27527
[Shapiro], p. 436Equation 10.6.35pntlem3 27540  pntleml 27542
[Stewart] p. 91Lemma 7.3constrss 33746
[Stewart] p. 92Definition 7.4.df-constr 33733
[Stewart] p. 96Theorem 7.10constraddcl 33765  constrinvcl 33776  constrmulcl 33774  constrnegcl 33766  constrsqrtcl 33782
[Stewart] p. 97Theorem 7.11constrextdg2 33752
[Stewart] p. 98Theorem 7.12constrext2chn 33762
[Stewart] p. 99Theorem 7.132sqr3nconstr 33784
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33794
[Stoll] p. 13Definition corresponds to dfsymdif3 4254
[Stoll] p. 16Exercise 4.40dif 4353  dif0 4326
[Stoll] p. 16Exercise 4.8difdifdir 4440
[Stoll] p. 17Theorem 5.1(5)unvdif 4423
[Stoll] p. 19Theorem 5.2(13)undm 4245
[Stoll] p. 19Theorem 5.2(13')indm 4246
[Stoll] p. 20Remarkinvdif 4227
[Stoll] p. 25Definition of ordered tripledf-ot 4583
[Stoll] p. 43Definitionuniiun 5005
[Stoll] p. 44Definitionintiin 5006
[Stoll] p. 45Definitiondf-iin 4942
[Stoll] p. 45Definition indexed uniondf-iun 4941
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4254
[Strang] p. 242Section 6.3expgrowth 44347
[Suppes] p. 22Theorem 2eq0 4298  eq0f 4295
[Suppes] p. 22Theorem 4eqss 3948  eqssd 3950  eqssi 3949
[Suppes] p. 23Theorem 5ss0 4350  ss0b 4349
[Suppes] p. 23Theorem 6sstr 3941  sstrALT2 44846
[Suppes] p. 23Theorem 7pssirr 4051
[Suppes] p. 23Theorem 8pssn2lp 4052
[Suppes] p. 23Theorem 9psstr 4055
[Suppes] p. 23Theorem 10pssss 4046
[Suppes] p. 25Theorem 12elin 3916  elun 4101
[Suppes] p. 26Theorem 15inidm 4175
[Suppes] p. 26Theorem 16in0 4343
[Suppes] p. 27Theorem 23unidm 4105
[Suppes] p. 27Theorem 24un0 4342
[Suppes] p. 27Theorem 25ssun1 4126
[Suppes] p. 27Theorem 26ssequn1 4134
[Suppes] p. 27Theorem 27unss 4138
[Suppes] p. 27Theorem 28indir 4234
[Suppes] p. 27Theorem 29undir 4235
[Suppes] p. 28Theorem 32difid 4324
[Suppes] p. 29Theorem 33difin 4220
[Suppes] p. 29Theorem 34indif 4228
[Suppes] p. 29Theorem 35undif1 4424
[Suppes] p. 29Theorem 36difun2 4429
[Suppes] p. 29Theorem 37difin0 4422
[Suppes] p. 29Theorem 38disjdif 4420
[Suppes] p. 29Theorem 39difundi 4238
[Suppes] p. 29Theorem 40difindi 4240
[Suppes] p. 30Theorem 41nalset 5249
[Suppes] p. 39Theorem 61uniss 4865
[Suppes] p. 39Theorem 65uniop 5453
[Suppes] p. 41Theorem 70intsn 4932
[Suppes] p. 42Theorem 71intpr 4930  intprg 4929
[Suppes] p. 42Theorem 73op1stb 5409
[Suppes] p. 42Theorem 78intun 4928
[Suppes] p. 44Definition 15(a)dfiun2 4980  dfiun2g 4978
[Suppes] p. 44Definition 15(b)dfiin2 4981
[Suppes] p. 47Theorem 86elpw 4552  elpw2 5270  elpw2g 5269  elpwg 4551  elpwgdedVD 44928
[Suppes] p. 47Theorem 87pwid 4570
[Suppes] p. 47Theorem 89pw0 4762
[Suppes] p. 48Theorem 90pwpw0 4763
[Suppes] p. 52Theorem 101xpss12 5629
[Suppes] p. 52Theorem 102xpindi 5771  xpindir 5772
[Suppes] p. 52Theorem 103xpundi 5683  xpundir 5684
[Suppes] p. 54Theorem 105elirrv 9478
[Suppes] p. 58Theorem 2relss 5720
[Suppes] p. 59Theorem 4eldm 5838  eldm2 5839  eldm2g 5837  eldmg 5836
[Suppes] p. 59Definition 3df-dm 5624
[Suppes] p. 60Theorem 6dmin 5849
[Suppes] p. 60Theorem 8rnun 6089
[Suppes] p. 60Theorem 9rnin 6090
[Suppes] p. 60Definition 4dfrn2 5826
[Suppes] p. 61Theorem 11brcnv 5820  brcnvg 5817
[Suppes] p. 62Equation 5elcnv 5814  elcnv2 5815
[Suppes] p. 62Theorem 12relcnv 6050
[Suppes] p. 62Theorem 15cnvin 6088
[Suppes] p. 62Theorem 16cnvun 6086
[Suppes] p. 63Definitiondftrrels2 38591
[Suppes] p. 63Theorem 20co02 6204
[Suppes] p. 63Theorem 21dmcoss 5911
[Suppes] p. 63Definition 7df-co 5623
[Suppes] p. 64Theorem 26cnvco 5823
[Suppes] p. 64Theorem 27coass 6209
[Suppes] p. 65Theorem 31resundi 5939
[Suppes] p. 65Theorem 34elima 6011  elima2 6012  elima3 6013  elimag 6010
[Suppes] p. 65Theorem 35imaundi 6093
[Suppes] p. 66Theorem 40dminss 6097
[Suppes] p. 66Theorem 41imainss 6098
[Suppes] p. 67Exercise 11cnvxp 6101
[Suppes] p. 81Definition 34dfec2 8620
[Suppes] p. 82Theorem 72elec 8663  elecALTV 38280  elecg 8661
[Suppes] p. 82Theorem 73eqvrelth 38627  erth 8671  erth2 8672
[Suppes] p. 83Theorem 74eqvreldisj 38630  erdisj 8674
[Suppes] p. 83Definition 35, df-parts 38782  dfmembpart2 38787
[Suppes] p. 89Theorem 96map0b 8802
[Suppes] p. 89Theorem 97map0 8806  map0g 8803
[Suppes] p. 89Theorem 98mapsn 8807  mapsnd 8805
[Suppes] p. 89Theorem 99mapss 8808
[Suppes] p. 91Definition 12(ii)alephsuc 9951
[Suppes] p. 91Definition 12(iii)alephlim 9950
[Suppes] p. 92Theorem 1enref 8902  enrefg 8901
[Suppes] p. 92Theorem 2ensym 8920  ensymb 8919  ensymi 8921
[Suppes] p. 92Theorem 3entr 8923
[Suppes] p. 92Theorem 4unen 8962
[Suppes] p. 94Theorem 15endom 8896
[Suppes] p. 94Theorem 16ssdomg 8917
[Suppes] p. 94Theorem 17domtr 8924
[Suppes] p. 95Theorem 18sbth 9005
[Suppes] p. 97Theorem 23canth2 9038  canth2g 9039
[Suppes] p. 97Definition 3brsdom2 9009  df-sdom 8867  dfsdom2 9008
[Suppes] p. 97Theorem 21(i)sdomirr 9022
[Suppes] p. 97Theorem 22(i)domnsym 9011
[Suppes] p. 97Theorem 21(ii)sdomnsym 9010
[Suppes] p. 97Theorem 22(ii)domsdomtr 9020
[Suppes] p. 97Theorem 22(iv)brdom2 8899
[Suppes] p. 97Theorem 21(iii)sdomtr 9023
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9018
[Suppes] p. 98Exercise 4fundmen 8948  fundmeng 8949
[Suppes] p. 98Exercise 6xpdom3 8983
[Suppes] p. 98Exercise 11sdomentr 9019
[Suppes] p. 104Theorem 37fofi 9192
[Suppes] p. 104Theorem 38pwfi 9198
[Suppes] p. 105Theorem 40pwfi 9198
[Suppes] p. 111Axiom for cardinal numberscarden 10434
[Suppes] p. 130Definition 3df-tr 5197
[Suppes] p. 132Theorem 9ssonuni 7708
[Suppes] p. 134Definition 6df-suc 6308
[Suppes] p. 136Theorem Schema 22findes 7825  finds 7821  finds1 7824  finds2 7823
[Suppes] p. 151Theorem 42isfinite 9537  isfinite2 9177  isfiniteg 9179  unbnn 9175
[Suppes] p. 162Definition 5df-ltnq 10801  df-ltpq 10793
[Suppes] p. 197Theorem Schema 4tfindes 7788  tfinds 7785  tfinds2 7789
[Suppes] p. 209Theorem 18oaord1 8461
[Suppes] p. 209Theorem 21oaword2 8463
[Suppes] p. 211Theorem 25oaass 8471
[Suppes] p. 225Definition 8iscard2 9861
[Suppes] p. 227Theorem 56ondomon 10446
[Suppes] p. 228Theorem 59harcard 9863
[Suppes] p. 228Definition 12(i)aleph0 9949
[Suppes] p. 228Theorem Schema 61onintss 6354
[Suppes] p. 228Theorem Schema 62onminesb 7721  onminsb 7722
[Suppes] p. 229Theorem 64alephval2 10455
[Suppes] p. 229Theorem 65alephcard 9953
[Suppes] p. 229Theorem 66alephord2i 9960
[Suppes] p. 229Theorem 67alephnbtwn 9954
[Suppes] p. 229Definition 12df-aleph 9825
[Suppes] p. 242Theorem 6weth 10378
[Suppes] p. 242Theorem 8entric 10440
[Suppes] p. 242Theorem 9carden 10434
[Szendrei] p. 11Line 6df-cloneop 35708
[Szendrei] p. 11Paragraph 3df-suppos 35712
[TakeutiZaring] p. 8Axiom 1ax-ext 2702
[TakeutiZaring] p. 13Definition 4.5df-cleq 2722
[TakeutiZaring] p. 13Proposition 4.6df-clel 2804
[TakeutiZaring] p. 13Proposition 4.9cvjust 2724
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2750
[TakeutiZaring] p. 14Definition 4.16df-oprab 7345
[TakeutiZaring] p. 14Proposition 4.14ru 3737
[TakeutiZaring] p. 15Axiom 2zfpair 5357
[TakeutiZaring] p. 15Exercise 1elpr 4599  elpr2 4601  elpr2g 4600  elprg 4597
[TakeutiZaring] p. 15Exercise 2elsn 4589  elsn2 4616  elsn2g 4615  elsng 4588  velsn 4590
[TakeutiZaring] p. 15Exercise 3elop 5405
[TakeutiZaring] p. 15Exercise 4sneq 4584  sneqr 4790
[TakeutiZaring] p. 15Definition 5.1dfpr2 4595  dfsn2 4587  dfsn2ALT 4596
[TakeutiZaring] p. 16Axiom 3uniex 7669
[TakeutiZaring] p. 16Exercise 6opth 5414
[TakeutiZaring] p. 16Exercise 7opex 5402
[TakeutiZaring] p. 16Exercise 8rext 5387
[TakeutiZaring] p. 16Corollary 5.8unex 7672  unexg 7671
[TakeutiZaring] p. 16Definition 5.3dftp2 4642
[TakeutiZaring] p. 16Definition 5.5df-uni 4858
[TakeutiZaring] p. 16Definition 5.6df-in 3907  df-un 3905
[TakeutiZaring] p. 16Proposition 5.7unipr 4874  uniprg 4873
[TakeutiZaring] p. 17Axiom 4vpwex 5313
[TakeutiZaring] p. 17Exercise 1eltp 4640
[TakeutiZaring] p. 17Exercise 5elsuc 6374  elsucg 6372  sstr2 3939
[TakeutiZaring] p. 17Exercise 6uncom 4106
[TakeutiZaring] p. 17Exercise 7incom 4157
[TakeutiZaring] p. 17Exercise 8unass 4120
[TakeutiZaring] p. 17Exercise 9inass 4176
[TakeutiZaring] p. 17Exercise 10indi 4232
[TakeutiZaring] p. 17Exercise 11undi 4233
[TakeutiZaring] p. 17Definition 5.9df-pss 3920  df-ss 3917
[TakeutiZaring] p. 17Definition 5.10df-pw 4550
[TakeutiZaring] p. 18Exercise 7unss2 4135
[TakeutiZaring] p. 18Exercise 9dfss2 3918  sseqin2 4171
[TakeutiZaring] p. 18Exercise 10ssid 3955
[TakeutiZaring] p. 18Exercise 12inss1 4185  inss2 4186
[TakeutiZaring] p. 18Exercise 13nss 3997
[TakeutiZaring] p. 18Exercise 15unieq 4868
[TakeutiZaring] p. 18Exercise 18sspwb 5388  sspwimp 44929  sspwimpALT 44936  sspwimpALT2 44939  sspwimpcf 44931
[TakeutiZaring] p. 18Exercise 19pweqb 5395
[TakeutiZaring] p. 19Axiom 5ax-rep 5215
[TakeutiZaring] p. 20Definitiondf-rab 3394
[TakeutiZaring] p. 20Corollary 5.160ex 5243
[TakeutiZaring] p. 20Definition 5.12df-dif 3903
[TakeutiZaring] p. 20Definition 5.14dfnul2 4284
[TakeutiZaring] p. 20Proposition 5.15difid 4324
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4301  n0f 4297  neq0 4300  neq0f 4296
[TakeutiZaring] p. 21Axiom 6zfreg 9477
[TakeutiZaring] p. 21Axiom 6'zfregs 9617
[TakeutiZaring] p. 21Theorem 5.22setind 9619
[TakeutiZaring] p. 21Definition 5.20df-v 3436
[TakeutiZaring] p. 21Proposition 5.21vprc 5251
[TakeutiZaring] p. 22Exercise 10ss 4348
[TakeutiZaring] p. 22Exercise 3ssex 5257  ssexg 5259
[TakeutiZaring] p. 22Exercise 4inex1 5253
[TakeutiZaring] p. 22Exercise 5ruv 9486
[TakeutiZaring] p. 22Exercise 6elirr 9480
[TakeutiZaring] p. 22Exercise 7ssdif0 4314
[TakeutiZaring] p. 22Exercise 11difdif 4083
[TakeutiZaring] p. 22Exercise 13undif3 4248  undif3VD 44893
[TakeutiZaring] p. 22Exercise 14difss 4084
[TakeutiZaring] p. 22Exercise 15sscon 4091
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3046
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3055
[TakeutiZaring] p. 23Proposition 6.2xpex 7681  xpexg 7678
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5621
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6548
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6724  fun11 6551
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6490  svrelfun 6549
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5825
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5827
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5626
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5627
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5623
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6138  dfrel2 6133
[TakeutiZaring] p. 25Exercise 3xpss 5630
[TakeutiZaring] p. 25Exercise 5relun 5749
[TakeutiZaring] p. 25Exercise 6reluni 5756
[TakeutiZaring] p. 25Exercise 9inxp 5769
[TakeutiZaring] p. 25Exercise 12relres 5951
[TakeutiZaring] p. 25Exercise 13opelres 5931  opelresi 5933
[TakeutiZaring] p. 25Exercise 14dmres 5958
[TakeutiZaring] p. 25Exercise 15resss 5947
[TakeutiZaring] p. 25Exercise 17resabs1 5952
[TakeutiZaring] p. 25Exercise 18funres 6519
[TakeutiZaring] p. 25Exercise 24relco 6054
[TakeutiZaring] p. 25Exercise 29funco 6517
[TakeutiZaring] p. 25Exercise 30f1co 6726
[TakeutiZaring] p. 26Definition 6.10eu2 2603
[TakeutiZaring] p. 26Definition 6.11conventions 30370  df-fv 6485  fv3 6835
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7850  cnvexg 7849
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7834  dmexg 7826
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7835  rnexg 7827
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44465
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7845
[TakeutiZaring] p. 27Corollary 6.13fvex 6830
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47184  tz6.12-1-afv2 47251  tz6.12-1 6840  tz6.12-afv 47183  tz6.12-afv2 47250  tz6.12 6841  tz6.12c-afv2 47252  tz6.12c 6839
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47247  tz6.12-2 6805  tz6.12i-afv2 47253  tz6.12i 6843
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6480
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6481
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6483  wfo 6475
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6482  wf1 6474
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6484  wf1o 6476
[TakeutiZaring] p. 28Exercise 4eqfnfv 6959  eqfnfv2 6960  eqfnfv2f 6963
[TakeutiZaring] p. 28Exercise 5fvco 6915
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7146
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7144
[TakeutiZaring] p. 29Exercise 9funimaex 6565  funimaexg 6564
[TakeutiZaring] p. 29Definition 6.18df-br 5090
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5523
[TakeutiZaring] p. 30Definition 6.21dffr2 5575  dffr3 6045  eliniseg 6040  iniseg 6043
[TakeutiZaring] p. 30Definition 6.22df-eprel 5514
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5591  fr3nr 7700  frirr 5590
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5567
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7702
[TakeutiZaring] p. 31Exercise 1frss 5578
[TakeutiZaring] p. 31Exercise 4wess 5600
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6290  tz6.26i 6291  wefrc 5608  wereu2 5611
[TakeutiZaring] p. 32Theorem 6.27wfi 6292  wfii 6293
[TakeutiZaring] p. 32Definition 6.28df-isom 6486
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7258
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7259
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7265
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7266
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7267
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7271
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7278
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7280
[TakeutiZaring] p. 35Notationwtr 5196
[TakeutiZaring] p. 35Theorem 7.2trelpss 44466  tz7.2 5597
[TakeutiZaring] p. 35Definition 7.1dftr3 5201
[TakeutiZaring] p. 36Proposition 7.4ordwe 6315
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6323
[TakeutiZaring] p. 36Proposition 7.6ordelord 6324  ordelordALT 44549  ordelordALTVD 44878
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6330  ordelssne 6329
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6328
[TakeutiZaring] p. 37Proposition 7.9ordin 6332
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7710
[TakeutiZaring] p. 38Corollary 7.15ordsson 7711
[TakeutiZaring] p. 38Definition 7.11df-on 6306
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6334
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44561  ordon 7705
[TakeutiZaring] p. 38Proposition 7.13onprc 7706
[TakeutiZaring] p. 39Theorem 7.17tfi 7778
[TakeutiZaring] p. 40Exercise 3ontr2 6350
[TakeutiZaring] p. 40Exercise 7dftr2 5198
[TakeutiZaring] p. 40Exercise 9onssmin 7720
[TakeutiZaring] p. 40Exercise 11unon 7756
[TakeutiZaring] p. 40Exercise 12ordun 6408
[TakeutiZaring] p. 40Exercise 14ordequn 6407
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7707
[TakeutiZaring] p. 40Proposition 7.20elssuni 4887
[TakeutiZaring] p. 41Definition 7.22df-suc 6308
[TakeutiZaring] p. 41Proposition 7.23sssucid 6384  sucidg 6385
[TakeutiZaring] p. 41Proposition 7.24onsuc 7738
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6398  ordnbtwn 6397
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7753
[TakeutiZaring] p. 42Exercise 1df-lim 6307
[TakeutiZaring] p. 42Exercise 4omssnlim 7806
[TakeutiZaring] p. 42Exercise 7ssnlim 7811
[TakeutiZaring] p. 42Exercise 8onsucssi 7766  ordelsuc 7745
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7747
[TakeutiZaring] p. 42Definition 7.27nlimon 7776
[TakeutiZaring] p. 42Definition 7.28dfom2 7793
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7814
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7815
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7816
[TakeutiZaring] p. 43Remarkomon 7803
[TakeutiZaring] p. 43Axiom 7inf3 9520  omex 9528
[TakeutiZaring] p. 43Theorem 7.32ordom 7801
[TakeutiZaring] p. 43Corollary 7.31find 7820
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7817
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7818
[TakeutiZaring] p. 44Exercise 1limomss 7796
[TakeutiZaring] p. 44Exercise 2int0 4910
[TakeutiZaring] p. 44Exercise 3trintss 5214
[TakeutiZaring] p. 44Exercise 4intss1 4911
[TakeutiZaring] p. 44Exercise 5intex 5280
[TakeutiZaring] p. 44Exercise 6oninton 7723
[TakeutiZaring] p. 44Exercise 11ordintdif 6353
[TakeutiZaring] p. 44Definition 7.35df-int 4896
[TakeutiZaring] p. 44Proposition 7.34noinfep 9545
[TakeutiZaring] p. 45Exercise 4onint 7718
[TakeutiZaring] p. 47Lemma 1tfrlem1 8290
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8311
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8312
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8313
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8320  tz7.44-2 8321  tz7.44-3 8322
[TakeutiZaring] p. 50Exercise 1smogt 8282
[TakeutiZaring] p. 50Exercise 3smoiso 8277
[TakeutiZaring] p. 50Definition 7.46df-smo 8261
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8359  tz7.49c 8360
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8357
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8356
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8358
[TakeutiZaring] p. 53Proposition 7.532eu5 2650
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9894
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9895
[TakeutiZaring] p. 56Definition 8.1oalim 8442  oasuc 8434
[TakeutiZaring] p. 57Remarktfindsg 7786
[TakeutiZaring] p. 57Proposition 8.2oacl 8445
[TakeutiZaring] p. 57Proposition 8.3oa0 8426  oa0r 8448
[TakeutiZaring] p. 57Proposition 8.16omcl 8446
[TakeutiZaring] p. 58Corollary 8.5oacan 8458
[TakeutiZaring] p. 58Proposition 8.4nnaord 8529  nnaordi 8528  oaord 8457  oaordi 8456
[TakeutiZaring] p. 59Proposition 8.6iunss2 4996  uniss2 4890
[TakeutiZaring] p. 59Proposition 8.7oawordri 8460
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8465  oawordex 8467
[TakeutiZaring] p. 59Proposition 8.9nnacl 8521
[TakeutiZaring] p. 59Proposition 8.10oaabs 8558
[TakeutiZaring] p. 60Remarkoancom 9536
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8470
[TakeutiZaring] p. 62Exercise 1nnarcl 8526
[TakeutiZaring] p. 62Exercise 5oaword1 8462
[TakeutiZaring] p. 62Definition 8.15om0x 8429  omlim 8443  omsuc 8436
[TakeutiZaring] p. 62Definition 8.15(a)om0 8427
[TakeutiZaring] p. 63Proposition 8.17nnecl 8523  nnmcl 8522
[TakeutiZaring] p. 63Proposition 8.19nnmord 8542  nnmordi 8541  omord 8478  omordi 8476
[TakeutiZaring] p. 63Proposition 8.20omcan 8479
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8546  omwordri 8482
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8449
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8452  om1r 8453
[TakeutiZaring] p. 64Proposition 8.22om00 8485
[TakeutiZaring] p. 64Proposition 8.23omordlim 8487
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8488
[TakeutiZaring] p. 64Proposition 8.25odi 8489
[TakeutiZaring] p. 65Theorem 8.26omass 8490
[TakeutiZaring] p. 67Definition 8.30nnesuc 8518  oe0 8432  oelim 8444  oesuc 8437  onesuc 8440
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8430
[TakeutiZaring] p. 67Proposition 8.32oen0 8496
[TakeutiZaring] p. 67Proposition 8.33oeordi 8497
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8431
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8455
[TakeutiZaring] p. 68Corollary 8.34oeord 8498
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8504
[TakeutiZaring] p. 68Proposition 8.35oewordri 8502
[TakeutiZaring] p. 68Proposition 8.37oeworde 8503
[TakeutiZaring] p. 69Proposition 8.41oeoa 8507
[TakeutiZaring] p. 70Proposition 8.42oeoe 8509
[TakeutiZaring] p. 73Theorem 9.1trcl 9613  tz9.1 9614
[TakeutiZaring] p. 76Definition 9.9df-r1 9649  r10 9653  r1lim 9657  r1limg 9656  r1suc 9655  r1sucg 9654
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9665  r1ord2 9666  r1ordg 9663
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9675
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9700  tz9.13 9676  tz9.13g 9677
[TakeutiZaring] p. 79Definition 9.14df-rank 9650  rankval 9701  rankvalb 9682  rankvalg 9702
[TakeutiZaring] p. 79Proposition 9.16rankel 9724  rankelb 9709
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9738  rankval3 9725  rankval3b 9711
[TakeutiZaring] p. 79Proposition 9.18rankonid 9714
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9680
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9719  rankr1c 9706  rankr1g 9717
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9720
[TakeutiZaring] p. 80Exercise 1rankss 9734  rankssb 9733
[TakeutiZaring] p. 80Exercise 2unbndrank 9727
[TakeutiZaring] p. 80Proposition 9.19bndrank 9726
[TakeutiZaring] p. 83Axiom of Choiceac4 10358  dfac3 10004
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9913  numth 10355  numth2 10354
[TakeutiZaring] p. 85Definition 10.4cardval 10429
[TakeutiZaring] p. 85Proposition 10.5cardid 10430  cardid2 9838
[TakeutiZaring] p. 85Proposition 10.9oncard 9845
[TakeutiZaring] p. 85Proposition 10.10carden 10434
[TakeutiZaring] p. 85Proposition 10.11cardidm 9844
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9829
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9850
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9842
[TakeutiZaring] p. 87Proposition 10.15pwen 9058
[TakeutiZaring] p. 88Exercise 1en0 8935
[TakeutiZaring] p. 88Exercise 7infensuc 9063
[TakeutiZaring] p. 89Exercise 10omxpen 8987
[TakeutiZaring] p. 90Corollary 10.23cardnn 9848
[TakeutiZaring] p. 90Definition 10.27alephiso 9981
[TakeutiZaring] p. 90Proposition 10.20nneneq 9110
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9118
[TakeutiZaring] p. 90Proposition 10.26alephprc 9982
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9115
[TakeutiZaring] p. 91Exercise 2alephle 9971
[TakeutiZaring] p. 91Exercise 3aleph0 9949
[TakeutiZaring] p. 91Exercise 4cardlim 9857
[TakeutiZaring] p. 91Exercise 7infpss 10099
[TakeutiZaring] p. 91Exercise 8infcntss 9202
[TakeutiZaring] p. 91Definition 10.29df-fin 8868  isfi 8893
[TakeutiZaring] p. 92Proposition 10.32onfin 9119
[TakeutiZaring] p. 92Proposition 10.34imadomg 10417
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8980
[TakeutiZaring] p. 93Proposition 10.35fodomb 10409
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10069  unxpdom 9138
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9859  cardsdomelir 9858
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9140
[TakeutiZaring] p. 94Proposition 10.39infxpen 9897
[TakeutiZaring] p. 95Definition 10.42df-map 8747
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10445  infxpidm2 9900
[TakeutiZaring] p. 95Proposition 10.41infdju 10090  infxp 10097
[TakeutiZaring] p. 96Proposition 10.44pw2en 8992  pw2f1o 8990
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9051
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10370
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10365  ac6s5 10374
[TakeutiZaring] p. 98Theorem 10.47unidom 10426
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10427  uniimadomf 10428
[TakeutiZaring] p. 100Definition 11.1cfcof 10157
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10152
[TakeutiZaring] p. 102Exercise 1cfle 10137
[TakeutiZaring] p. 102Exercise 2cf0 10134
[TakeutiZaring] p. 102Exercise 3cfsuc 10140
[TakeutiZaring] p. 102Exercise 4cfom 10147
[TakeutiZaring] p. 102Proposition 11.9coftr 10156
[TakeutiZaring] p. 103Theorem 11.15alephreg 10465
[TakeutiZaring] p. 103Proposition 11.11cardcf 10135
[TakeutiZaring] p. 103Proposition 11.13alephsing 10159
[TakeutiZaring] p. 104Corollary 11.17cardinfima 9980
[TakeutiZaring] p. 104Proposition 11.16carduniima 9979
[TakeutiZaring] p. 104Proposition 11.18alephfp 9991  alephfp2 9992
[TakeutiZaring] p. 106Theorem 11.20gchina 10582
[TakeutiZaring] p. 106Theorem 11.21mappwen 9995
[TakeutiZaring] p. 107Theorem 11.26konigth 10452
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10466
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10467
[Tarski] p. 67Axiom B5ax-c5 38901
[Tarski] p. 67Scheme B5sp 2185
[Tarski] p. 68Lemma 6avril1 30433  equid 2013
[Tarski] p. 69Lemma 7equcomi 2018
[Tarski] p. 70Lemma 14spim 2386  spime 2388  spimew 1972
[Tarski] p. 70Lemma 16ax-12 2179  ax-c15 38907  ax12i 1967
[Tarski] p. 70Lemmas 16 and 17sb6 2087
[Tarski] p. 75Axiom B7ax6v 1969
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1911  ax5ALT 38925
[Tarski], p. 75Scheme B8 of system S2ax-7 2009  ax-8 2112  ax-9 2120
[Tarski1999] p. 178Axiom 4axtgsegcon 28435
[Tarski1999] p. 178Axiom 5axtg5seg 28436
[Tarski1999] p. 179Axiom 7axtgpasch 28438
[Tarski1999] p. 180Axiom 7.1axtgpasch 28438
[Tarski1999] p. 185Axiom 11axtgcont1 28439
[Truss] p. 114Theorem 5.18ruc 16144
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37678
[Viaclovsky8] p. 3Proposition 7ismblfin 37680
[Weierstrass] p. 272Definitiondf-mdet 22493  mdetuni 22530
[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 37458
[WhiteheadRussell] p. 100Theorem *2.05frege5 43812  imim2 58  wl-luk-imim2 37453
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47029  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2657  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37456
[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 44938  wl-luk-notnotr 37457
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43842  axfrege28 43841  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 37450
[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 30371  pm2.27 42  wl-luk-pm2.27 37448
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38370
[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 44370
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44371
[WhiteheadRussell] p. 147Theorem *10.2219.26 1871
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44372
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44373
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44374
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1894
[WhiteheadRussell] p. 151Theorem *10.301albitr 44375
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44376
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44377
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44378
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44379
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44381
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44382
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44383
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44380
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2092
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44386
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44387
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2072
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2162
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1830
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1831
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44388
[WhiteheadRussell] p. 162Theorem *11.322alim 44389
[WhiteheadRussell] p. 162Theorem *11.332albi 44390
[WhiteheadRussell] p. 162Theorem *11.342exim 44391
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44393
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44392
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1888
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44395
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44396
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44394
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1829
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44397
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44398
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1847
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44399
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2345
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1861
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44404
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44400
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44401
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44402
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44403
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44408
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44405
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44406
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44407
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44409
[WhiteheadRussell] p. 175Definition *14.02df-eu 2563
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44419  pm13.13b 44420
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44421
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3007
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3008
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3619
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44427
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44428
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44422
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44564  pm13.193 44423
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44424
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44425
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44426
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44433
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44432
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44431
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3802
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44434  pm14.122b 44435  pm14.122c 44436
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44437  pm14.123b 44438  pm14.123c 44439
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44441
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44440
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44442
[WhiteheadRussell] p. 190Theorem *14.22iota4 6458
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44443
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6459
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44444
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44446
[WhiteheadRussell] p. 192Theorem *14.26eupick 2627  eupickbi 2630  sbaniota 44447
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44445
[WhiteheadRussell] p. 192Theorem *14.271eubi 2578
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44448
[WhiteheadRussell] p. 235Definition *30.01conventions 30370  df-fv 6485
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9886  pm54.43lem 9885
[Young] p. 141Definition of operator orderingleop2 32094
[Young] p. 142Example 12.2(i)0leop 32100  idleop 32101
[vandenDries] p. 42Lemma 61irrapx1 42840
[vandenDries] p. 43Theorem 62pellex 42847  pellexlem1 42841

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