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 17629
[Adamek] p. 21Condition 3.1(b)df-cat 17629
[Adamek] p. 22Example 3.3(1)df-setc 18038
[Adamek] p. 24Example 3.3(4.c)0cat 17650  0funcg 49074  df-termc 49462
[Adamek] p. 24Example 3.3(4.d)df-prstc 49539  prsthinc 49453
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49567  df-mndtc 49567
[Adamek] p. 24Example 3.3(4)(c)discsnterm 49563
[Adamek] p. 25Definition 3.5df-oppc 17673
[Adamek] p. 25Example 3.6(1)oduoppcciso 49555
[Adamek] p. 25Example 3.6(2)oppgoppcco 49580  oppgoppchom 49579  oppgoppcid 49581
[Adamek] p. 28Remark 3.9oppciso 17743
[Adamek] p. 28Remark 3.12invf1o 17731  invisoinvl 17752
[Adamek] p. 28Example 3.13idinv 17751  idiso 17750
[Adamek] p. 28Corollary 3.11inveq 17736
[Adamek] p. 28Definition 3.8df-inv 17710  df-iso 17711  dfiso2 17734
[Adamek] p. 28Proposition 3.10sectcan 17717
[Adamek] p. 29Remark 3.16cicer 17768  cicerALT 49035
[Adamek] p. 29Definition 3.15cic 17761  df-cic 17758
[Adamek] p. 29Definition 3.17df-func 17820
[Adamek] p. 29Proposition 3.14(1)invinv 17732
[Adamek] p. 29Proposition 3.14(2)invco 17733  isoco 17739
[Adamek] p. 30Remark 3.19df-func 17820
[Adamek] p. 30Example 3.20(1)idfucl 17843
[Adamek] p. 30Example 3.20(2)diag1 49293
[Adamek] p. 32Proposition 3.21funciso 17836
[Adamek] p. 33Example 3.26(1)discsnterm 49563  discthing 49450
[Adamek] p. 33Example 3.26(2)df-thinc 49407  prsthinc 49453  thincciso 49442  thincciso2 49444  thincciso3 49445  thinccisod 49443
[Adamek] p. 33Example 3.26(3)df-mndtc 49567
[Adamek] p. 33Proposition 3.23cofucl 17850  cofucla 49085
[Adamek] p. 34Remark 3.28(1)cofidfth 49151
[Adamek] p. 34Remark 3.28(2)catciso 18073  catcisoi 49389
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18128
[Adamek] p. 34Definition 3.27(2)df-fth 17869
[Adamek] p. 34Definition 3.27(3)df-full 17868
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18128
[Adamek] p. 35Corollary 3.32ffthiso 17893
[Adamek] p. 35Proposition 3.30(c)cofth 17899
[Adamek] p. 35Proposition 3.30(d)cofull 17898
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18113
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18113
[Adamek] p. 39Remark 3.422oppf 49121
[Adamek] p. 39Definition 3.41df-oppf 49112  funcoppc 17837
[Adamek] p. 39Definition 3.44.df-catc 18061  elcatchom 49386
[Adamek] p. 39Proposition 3.43(c)fthoppc 17887  fthoppf 49153
[Adamek] p. 39Proposition 3.43(d)fulloppc 17886  fulloppf 49152
[Adamek] p. 40Remark 3.48catccat 18070
[Adamek] p. 40Definition 3.470funcg 49074  df-catc 18061
[Adamek] p. 45Exercise 3Gincat 49590
[Adamek] p. 48Remark 4.2(2)cnelsubc 49593  nelsubc3 49060
[Adamek] p. 48Remark 4.2(3)imasubc 49140  imasubc2 49141  imasubc3 49145
[Adamek] p. 48Example 4.3(1.a)0subcat 17800
[Adamek] p. 48Example 4.3(1.b)catsubcat 17801
[Adamek] p. 48Definition 4.1(1)nelsubc3 49060
[Adamek] p. 48Definition 4.1(2)fullsubc 17812
[Adamek] p. 48Definition 4.1(a)df-subc 17774
[Adamek] p. 49Remark 4.4idsubc 49149
[Adamek] p. 49Remark 4.4(1)idemb 49148
[Adamek] p. 49Remark 4.4(2)idfullsubc 49150  ressffth 17902
[Adamek] p. 58Exercise 4Asetc1onsubc 49591
[Adamek] p. 83Definition 6.1df-nat 17908
[Adamek] p. 87Remark 6.14(a)fuccocl 17929
[Adamek] p. 87Remark 6.14(b)fucass 17933
[Adamek] p. 87Definition 6.15df-fuc 17909
[Adamek] p. 88Remark 6.16fuccat 17935
[Adamek] p. 101Definition 7.10funcg 49074  df-inito 17946
[Adamek] p. 101Example 7.2(3)0funcg 49074  df-termc 49462  initc 49080
[Adamek] p. 101Example 7.2 (6)irinitoringc 21389
[Adamek] p. 102Definition 7.4df-termo 17947  oppctermo 49225
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17974
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17978
[Adamek] p. 103Remark 7.8oppczeroo 49226
[Adamek] p. 103Definition 7.7df-zeroo 17948
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21390
[Adamek] p. 103Proposition 7.6termoeu1w 17981
[Adamek] p. 106Definition 7.19df-sect 17709
[Adamek] p. 107Example 7.20(7)thincinv 49458
[Adamek] p. 108Example 7.25(4)thincsect2 49457
[Adamek] p. 110Example 7.33(9)thincmon 49422
[Adamek] p. 110Proposition 7.35sectmon 17744
[Adamek] p. 112Proposition 7.42sectepi 17746
[Adamek] p. 185Section 10.67updjud 9887
[Adamek] p. 193Definition 11.1(1)df-lmd 49634
[Adamek] p. 193Definition 11.3(1)df-lmd 49634
[Adamek] p. 194Definition 11.3(2)df-lmd 49634
[Adamek] p. 202Definition 11.27(1)df-cmd 49635
[Adamek] p. 202Definition 11.27(2)df-cmd 49635
[Adamek] p. 478Item Rngdf-ringc 20555
[AhoHopUll] p. 2Section 1.1df-bigo 48537
[AhoHopUll] p. 12Section 1.3df-blen 48559
[AhoHopUll] p. 318Section 9.1df-concat 14536  df-pfx 14636  df-substr 14606  df-word 14479  lencl 14498  wrd0 14504
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24596  df-nmoo 30674
[AkhiezerGlazman] p. 64Theoremhmopidmch 32082  hmopidmchi 32080
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32130  pjcmul2i 32131
[AkhiezerGlazman] p. 72Theoremcnvunop 31847  unoplin 31849
[AkhiezerGlazman] p. 72Equation 2unopadj 31848  unopadj2 31867
[AkhiezerGlazman] p. 73Theoremelunop2 31942  lnopunii 31941
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32015
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27835
[Alling] p. 184Axiom Bbdayfo 27589
[Alling] p. 184Axiom Osltso 27588
[Alling] p. 184Axiom SDnodense 27604
[Alling] p. 185Lemma 0nocvxmin 27690
[Alling] p. 185Theoremconway 27711
[Alling] p. 185Axiom FEnoeta 27655
[Alling] p. 186Theorem 4slerec 27731
[Alling], p. 2Definitionrp-brsslt 43412
[Alling], p. 3Notenla0001 43415  nla0002 43413  nla0003 43414
[Apostol] p. 18Theorem I.1addcan 11358  addcan2d 11378  addcan2i 11368  addcand 11377  addcani 11367
[Apostol] p. 18Theorem I.2negeu 11411
[Apostol] p. 18Theorem I.3negsub 11470  negsubd 11539  negsubi 11500
[Apostol] p. 18Theorem I.4negneg 11472  negnegd 11524  negnegi 11492
[Apostol] p. 18Theorem I.5subdi 11611  subdid 11634  subdii 11627  subdir 11612  subdird 11635  subdiri 11628
[Apostol] p. 18Theorem I.6mul01 11353  mul01d 11373  mul01i 11364  mul02 11352  mul02d 11372  mul02i 11363
[Apostol] p. 18Theorem I.7mulcan 11815  mulcan2d 11812  mulcand 11811  mulcani 11817
[Apostol] p. 18Theorem I.8receu 11823  xreceu 32842
[Apostol] p. 18Theorem I.9divrec 11853  divrecd 11961  divreci 11927  divreczi 11920
[Apostol] p. 18Theorem I.10recrec 11879  recreci 11914
[Apostol] p. 18Theorem I.11mul0or 11818  mul0ord 11826  mul0ori 11825
[Apostol] p. 18Theorem I.12mul2neg 11617  mul2negd 11633  mul2negi 11626  mulneg1 11614  mulneg1d 11631  mulneg1i 11624
[Apostol] p. 18Theorem I.13divadddiv 11897  divadddivd 12002  divadddivi 11944
[Apostol] p. 18Theorem I.14divmuldiv 11882  divmuldivd 11999  divmuldivi 11942  rdivmuldivd 20322
[Apostol] p. 18Theorem I.15divdivdiv 11883  divdivdivd 12005  divdivdivi 11945
[Apostol] p. 20Axiom 7rpaddcl 12975  rpaddcld 13010  rpmulcl 12976  rpmulcld 13011
[Apostol] p. 20Axiom 8rpneg 12985
[Apostol] p. 20Axiom 90nrp 12988
[Apostol] p. 20Theorem I.17lttri 11300
[Apostol] p. 20Theorem I.18ltadd1d 11771  ltadd1dd 11789  ltadd1i 11732
[Apostol] p. 20Theorem I.19ltmul1 12032  ltmul1a 12031  ltmul1i 12101  ltmul1ii 12111  ltmul2 12033  ltmul2d 13037  ltmul2dd 13051  ltmul2i 12104
[Apostol] p. 20Theorem I.20msqgt0 11698  msqgt0d 11745  msqgt0i 11715
[Apostol] p. 20Theorem I.210lt1 11700
[Apostol] p. 20Theorem I.23lt0neg1 11684  lt0neg1d 11747  ltneg 11678  ltnegd 11756  ltnegi 11722
[Apostol] p. 20Theorem I.25lt2add 11663  lt2addd 11801  lt2addi 11740
[Apostol] p. 20Definition of positive numbersdf-rp 12952
[Apostol] p. 21Exercise 4recgt0 12028  recgt0d 12117  recgt0i 12088  recgt0ii 12089
[Apostol] p. 22Definition of integersdf-z 12530
[Apostol] p. 22Definition of positive integersdfnn3 12200
[Apostol] p. 22Definition of rationalsdf-q 12908
[Apostol] p. 24Theorem I.26supeu 9405
[Apostol] p. 26Theorem I.28nnunb 12438
[Apostol] p. 26Theorem I.29arch 12439  archd 45156
[Apostol] p. 28Exercise 2btwnz 12637
[Apostol] p. 28Exercise 3nnrecl 12440
[Apostol] p. 28Exercise 4rebtwnz 12906
[Apostol] p. 28Exercise 5zbtwnre 12905
[Apostol] p. 28Exercise 6qbtwnre 13159
[Apostol] p. 28Exercise 10(a)zeneo 16309  zneo 12617  zneoALTV 47670
[Apostol] p. 29Theorem I.35cxpsqrtth 26639  msqsqrtd 15409  resqrtth 15221  sqrtth 15331  sqrtthi 15337  sqsqrtd 15408
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12189
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12872
[Apostol] p. 361Remarkcrreczi 14193
[Apostol] p. 363Remarkabsgt0i 15366
[Apostol] p. 363Exampleabssubd 15422  abssubi 15370
[ApostolNT] p. 7Remarkfmtno0 47541  fmtno1 47542  fmtno2 47551  fmtno3 47552  fmtno4 47553  fmtno5fac 47583  fmtnofz04prm 47578
[ApostolNT] p. 7Definitiondf-fmtno 47529
[ApostolNT] p. 8Definitiondf-ppi 27010
[ApostolNT] p. 14Definitiondf-dvds 16223
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16239
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16264
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16259
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16252
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16254
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16240
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16241
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16246
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16281
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16283
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16285
[ApostolNT] p. 15Definitiondf-gcd 16465  dfgcd2 16516
[ApostolNT] p. 16Definitionisprm2 16652
[ApostolNT] p. 16Theorem 1.5coprmdvds 16623
[ApostolNT] p. 16Theorem 1.7prminf 16886
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16483
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16517
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16519
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16498
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16490
[ApostolNT] p. 17Theorem 1.8coprm 16681
[ApostolNT] p. 17Theorem 1.9euclemma 16683
[ApostolNT] p. 17Theorem 1.101arith2 16899
[ApostolNT] p. 18Theorem 1.13prmrec 16893
[ApostolNT] p. 19Theorem 1.14divalg 16373
[ApostolNT] p. 20Theorem 1.15eucalg 16557
[ApostolNT] p. 24Definitiondf-mu 27011
[ApostolNT] p. 25Definitiondf-phi 16736
[ApostolNT] p. 25Theorem 2.1musum 27101
[ApostolNT] p. 26Theorem 2.2phisum 16761
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16746
[ApostolNT] p. 28Theorem 2.5(c)phimul 16750
[ApostolNT] p. 32Definitiondf-vma 27008
[ApostolNT] p. 32Theorem 2.9muinv 27103
[ApostolNT] p. 32Theorem 2.10vmasum 27127
[ApostolNT] p. 38Remarkdf-sgm 27012
[ApostolNT] p. 38Definitiondf-sgm 27012
[ApostolNT] p. 75Definitiondf-chp 27009  df-cht 27007
[ApostolNT] p. 104Definitioncongr 16634
[ApostolNT] p. 106Remarkdvdsval3 16226
[ApostolNT] p. 106Definitionmoddvds 16233
[ApostolNT] p. 107Example 2mod2eq0even 16316
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16317
[ApostolNT] p. 107Example 4zmod1congr 13850
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13890
[ApostolNT] p. 107Theorem 5.2(c)modexp 14203
[ApostolNT] p. 108Theorem 5.3modmulconst 16258
[ApostolNT] p. 109Theorem 5.4cncongr1 16637
[ApostolNT] p. 109Theorem 5.6gcdmodi 17045
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16639
[ApostolNT] p. 113Theorem 5.17eulerth 16753
[ApostolNT] p. 113Theorem 5.18vfermltl 16772
[ApostolNT] p. 114Theorem 5.19fermltl 16754
[ApostolNT] p. 116Theorem 5.24wilthimp 26982
[ApostolNT] p. 179Definitiondf-lgs 27206  lgsprme0 27250
[ApostolNT] p. 180Example 11lgs 27251
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27227
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27242
[ApostolNT] p. 181Theorem 9.4m1lgs 27299
[ApostolNT] p. 181Theorem 9.52lgs 27318  2lgsoddprm 27327
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27285
[ApostolNT] p. 185Theorem 9.8lgsquad 27294
[ApostolNT] p. 188Definitiondf-lgs 27206  lgs1 27252
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27243
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27245
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27253
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27254
[Baer] p. 40Property (b)mapdord 41632
[Baer] p. 40Property (c)mapd11 41633
[Baer] p. 40Property (e)mapdin 41656  mapdlsm 41658
[Baer] p. 40Property (f)mapd0 41659
[Baer] p. 40Definition of projectivitydf-mapd 41619  mapd1o 41642
[Baer] p. 41Property (g)mapdat 41661
[Baer] p. 44Part (1)mapdpg 41700
[Baer] p. 45Part (2)hdmap1eq 41795  mapdheq 41722  mapdheq2 41723  mapdheq2biN 41724
[Baer] p. 45Part (3)baerlem3 41707
[Baer] p. 46Part (4)mapdheq4 41726  mapdheq4lem 41725
[Baer] p. 46Part (5)baerlem5a 41708  baerlem5abmN 41712  baerlem5amN 41710  baerlem5b 41709  baerlem5bmN 41711
[Baer] p. 47Part (6)hdmap1l6 41815  hdmap1l6a 41803  hdmap1l6e 41808  hdmap1l6f 41809  hdmap1l6g 41810  hdmap1l6lem1 41801  hdmap1l6lem2 41802  mapdh6N 41741  mapdh6aN 41729  mapdh6eN 41734  mapdh6fN 41735  mapdh6gN 41736  mapdh6lem1N 41727  mapdh6lem2N 41728
[Baer] p. 48Part 9hdmapval 41822
[Baer] p. 48Part 10hdmap10 41834
[Baer] p. 48Part 11hdmapadd 41837
[Baer] p. 48Part (6)hdmap1l6h 41811  mapdh6hN 41737
[Baer] p. 48Part (7)mapdh75cN 41747  mapdh75d 41748  mapdh75e 41746  mapdh75fN 41749  mapdh7cN 41743  mapdh7dN 41744  mapdh7eN 41742  mapdh7fN 41745
[Baer] p. 48Part (8)mapdh8 41782  mapdh8a 41769  mapdh8aa 41770  mapdh8ab 41771  mapdh8ac 41772  mapdh8ad 41773  mapdh8b 41774  mapdh8c 41775  mapdh8d 41777  mapdh8d0N 41776  mapdh8e 41778  mapdh8g 41779  mapdh8i 41780  mapdh8j 41781
[Baer] p. 48Part (9)mapdh9a 41783
[Baer] p. 48Equation 10mapdhvmap 41763
[Baer] p. 49Part 12hdmap11 41842  hdmapeq0 41838  hdmapf1oN 41859  hdmapneg 41840  hdmaprnN 41858  hdmaprnlem1N 41843  hdmaprnlem3N 41844  hdmaprnlem3uN 41845  hdmaprnlem4N 41847  hdmaprnlem6N 41848  hdmaprnlem7N 41849  hdmaprnlem8N 41850  hdmaprnlem9N 41851  hdmapsub 41841
[Baer] p. 49Part 14hdmap14lem1 41862  hdmap14lem10 41871  hdmap14lem1a 41860  hdmap14lem2N 41863  hdmap14lem2a 41861  hdmap14lem3 41864  hdmap14lem8 41869  hdmap14lem9 41870
[Baer] p. 50Part 14hdmap14lem11 41872  hdmap14lem12 41873  hdmap14lem13 41874  hdmap14lem14 41875  hdmap14lem15 41876  hgmapval 41881
[Baer] p. 50Part 15hgmapadd 41888  hgmapmul 41889  hgmaprnlem2N 41891  hgmapvs 41885
[Baer] p. 50Part 16hgmaprnN 41895
[Baer] p. 110Lemma 1hdmapip0com 41911
[Baer] p. 110Line 27hdmapinvlem1 41912
[Baer] p. 110Line 28hdmapinvlem2 41913
[Baer] p. 110Line 30hdmapinvlem3 41914
[Baer] p. 110Part 1.2hdmapglem5 41916  hgmapvv 41920
[Baer] p. 110Proposition 1hdmapinvlem4 41915
[Baer] p. 111Line 10hgmapvvlem1 41917
[Baer] p. 111Line 15hdmapg 41924  hdmapglem7 41923
[Bauer], p. 483Theorem 1.22irrexpq 26640  2irrexpqALT 26710
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2562
[BellMachover] p. 460Notationdf-mo 2533
[BellMachover] p. 460Definitionmo3 2557
[BellMachover] p. 461Axiom Extax-ext 2701
[BellMachover] p. 462Theorem 1.1axextmo 2705
[BellMachover] p. 463Axiom Repaxrep5 5242
[BellMachover] p. 463Scheme Sepax-sep 5251
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37052  sepex 5255
[BellMachover] p. 466Problemaxpow2 5322
[BellMachover] p. 466Axiom Powaxpow3 5323
[BellMachover] p. 466Axiom Unionaxun2 7713
[BellMachover] p. 468Definitiondf-ord 6335
[BellMachover] p. 469Theorem 2.2(i)ordirr 6350
[BellMachover] p. 469Theorem 2.2(iii)onelon 6357
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6352
[BellMachover] p. 471Definition of Ndf-om 7843
[BellMachover] p. 471Problem 2.5(ii)uniordint 7777
[BellMachover] p. 471Definition of Limdf-lim 6337
[BellMachover] p. 472Axiom Infzfinf2 9595
[BellMachover] p. 473Theorem 2.8limom 7858
[BellMachover] p. 477Equation 3.1df-r1 9717
[BellMachover] p. 478Definitionrankval2 9771
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9735  r1ord3g 9732
[BellMachover] p. 480Axiom Regzfreg 9548
[BellMachover] p. 488Axiom ACac5 10430  dfac4 10075
[BellMachover] p. 490Definition of alephalephval3 10063
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39312
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32282
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32324  chirredi 32323
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32312
[Beran] p. 3Definition of joinsshjval3 31283
[Beran] p. 39Theorem 2.3(i)cmcm2 31545  cmcm2i 31522  cmcm2ii 31527  cmt2N 39243
[Beran] p. 40Theorem 2.3(iii)lecm 31546  lecmi 31531  lecmii 31532
[Beran] p. 45Theorem 3.4cmcmlem 31520
[Beran] p. 49Theorem 4.2cm2j 31549  cm2ji 31554  cm2mi 31555
[Beran] p. 95Definitiondf-sh 31136  issh2 31138
[Beran] p. 95Lemma 3.1(S5)his5 31015
[Beran] p. 95Lemma 3.1(S6)his6 31028
[Beran] p. 95Lemma 3.1(S7)his7 31019
[Beran] p. 95Lemma 3.2(S8)ho01i 31757
[Beran] p. 95Lemma 3.2(S9)hoeq1 31759
[Beran] p. 95Lemma 3.2(S10)ho02i 31758
[Beran] p. 95Lemma 3.2(S11)hoeq2 31760
[Beran] p. 95Postulate (S1)ax-his1 31011  his1i 31029
[Beran] p. 95Postulate (S2)ax-his2 31012
[Beran] p. 95Postulate (S3)ax-his3 31013
[Beran] p. 95Postulate (S4)ax-his4 31014
[Beran] p. 96Definition of normdf-hnorm 30897  dfhnorm2 31051  normval 31053
[Beran] p. 96Definition for Cauchy sequencehcau 31113
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30902
[Beran] p. 96Definition of complete subspaceisch3 31170
[Beran] p. 96Definition of convergedf-hlim 30901  hlimi 31117
[Beran] p. 97Theorem 3.3(i)norm-i-i 31062  norm-i 31058
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31066  norm-ii 31067  normlem0 31038  normlem1 31039  normlem2 31040  normlem3 31041  normlem4 31042  normlem5 31043  normlem6 31044  normlem7 31045  normlem7tALT 31048
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31068  norm-iii 31069
[Beran] p. 98Remark 3.4bcs 31110  bcsiALT 31108  bcsiHIL 31109
[Beran] p. 98Remark 3.4(B)normlem9at 31050  normpar 31084  normpari 31083
[Beran] p. 98Remark 3.4(C)normpyc 31075  normpyth 31074  normpythi 31071
[Beran] p. 99Remarklnfn0 31976  lnfn0i 31971  lnop0 31895  lnop0i 31899
[Beran] p. 99Theorem 3.5(i)nmcexi 31955  nmcfnex 31982  nmcfnexi 31980  nmcopex 31958  nmcopexi 31956
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 31983  nmcfnlbi 31981  nmcoplb 31959  nmcoplbi 31957
[Beran] p. 99Theorem 3.5(iii)lnfncon 31985  lnfnconi 31984  lnopcon 31964  lnopconi 31963
[Beran] p. 100Lemma 3.6normpar2i 31085
[Beran] p. 101Lemma 3.6norm3adifi 31082  norm3adifii 31077  norm3dif 31079  norm3difi 31076
[Beran] p. 102Theorem 3.7(i)chocunii 31230  pjhth 31322  pjhtheu 31323  pjpjhth 31354  pjpjhthi 31355  pjth 25339
[Beran] p. 102Theorem 3.7(ii)ococ 31335  ococi 31334
[Beran] p. 103Remark 3.8nlelchi 31990
[Beran] p. 104Theorem 3.9riesz3i 31991  riesz4 31993  riesz4i 31992
[Beran] p. 104Theorem 3.10cnlnadj 32008  cnlnadjeu 32007  cnlnadjeui 32006  cnlnadji 32005  cnlnadjlem1 31996  nmopadjlei 32017
[Beran] p. 106Theorem 3.11(i)adjeq0 32020
[Beran] p. 106Theorem 3.11(v)nmopadji 32019
[Beran] p. 106Theorem 3.11(ii)adjmul 32021
[Beran] p. 106Theorem 3.11(iv)adjadj 31865
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32031  nmopcoadji 32030
[Beran] p. 106Theorem 3.11(iii)adjadd 32022
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32032
[Beran] p. 106Theorem 3.11(viii)adjcoi 32029  pjadj2coi 32133  pjadjcoi 32090
[Beran] p. 107Definitiondf-ch 31150  isch2 31152
[Beran] p. 107Remark 3.12choccl 31235  isch3 31170  occl 31233  ocsh 31212  shoccl 31234  shocsh 31213
[Beran] p. 107Remark 3.12(B)ococin 31337
[Beran] p. 108Theorem 3.13chintcl 31261
[Beran] p. 109Property (i)pjadj2 32116  pjadj3 32117  pjadji 31614  pjadjii 31603
[Beran] p. 109Property (ii)pjidmco 32110  pjidmcoi 32106  pjidmi 31602
[Beran] p. 110Definition of projector orderingpjordi 32102
[Beran] p. 111Remarkho0val 31679  pjch1 31599
[Beran] p. 111Definitiondf-hfmul 31663  df-hfsum 31662  df-hodif 31661  df-homul 31660  df-hosum 31659
[Beran] p. 111Lemma 4.4(i)pjo 31600
[Beran] p. 111Lemma 4.4(ii)pjch 31623  pjchi 31361
[Beran] p. 111Lemma 4.4(iii)pjoc2 31368  pjoc2i 31367
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31609
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32094  pjssmii 31610
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32093
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32092
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32097
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32095  pjssge0ii 31611
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32096  pjdifnormii 31612
[Bobzien] p. 116Statement T3stoic3 1776
[Bobzien] p. 117Statement T2stoic2a 1774
[Bobzien] p. 117Statement T4stoic4a 1777
[Bobzien] p. 117Conclusion the contradictorystoic1a 1772
[Bogachev] p. 16Definition 1.5df-oms 34283
[Bogachev] p. 17Lemma 1.5.4omssubadd 34291
[Bogachev] p. 17Example 1.5.2omsmon 34289
[Bogachev] p. 41Definition 1.11.2df-carsg 34293
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34313
[Bogachev] p. 116Definition 2.3.1df-itgm 34344  df-sitm 34322
[Bogachev] p. 118Chapter 2.4.4df-itgm 34344
[Bogachev] p. 118Definition 2.4.1df-sitg 34321
[Bollobas] p. 1Section I.1df-edg 28975  isuhgrop 28997  isusgrop 29089  isuspgrop 29088
[Bollobas] p. 2Section I.1df-isubgr 47861  df-subgr 29195  uhgrspan1 29230  uhgrspansubgr 29218
[Bollobas] p. 3Definitiondf-gric 47881  gricuspgr 47918  isuspgrim 47896
[Bollobas] p. 3Section I.1cusgrsize 29382  df-clnbgr 47820  df-cusgr 29339  df-nbgr 29260  fusgrmaxsize 29392
[Bollobas] p. 4Definitiondf-upwlks 48122  df-wlks 29527
[Bollobas] p. 4Section I.1finsumvtxdg2size 29478  finsumvtxdgeven 29480  fusgr1th 29479  fusgrvtxdgonume 29482  vtxdgoddnumeven 29481
[Bollobas] p. 5Notationdf-pths 29644
[Bollobas] p. 5Definitiondf-crcts 29716  df-cycls 29717  df-trls 29620  df-wlkson 29528
[Bollobas] p. 7Section I.1df-ushgr 28986
[BourbakiAlg1] p. 1Definition 1df-clintop 48188  df-cllaw 48174  df-mgm 18567  df-mgm2 48207
[BourbakiAlg1] p. 4Definition 5df-assintop 48189  df-asslaw 48176  df-sgrp 18646  df-sgrp2 48209
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48208  df-comlaw 48175
[BourbakiAlg1] p. 12Definition 2df-mnd 18662
[BourbakiAlg1] p. 17Chapter I.mndlactf1 32967  mndlactf1o 32971  mndractf1 32969  mndractf1o 32972
[BourbakiAlg1] p. 92Definition 1df-ring 20144
[BourbakiAlg1] p. 93Section I.8.1df-rng 20062
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33629
[BourbakiAlg2] p. 113Chapter 5.assafld 33633  assarrginv 33632
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33673  fldextrspunfld 33671  fldextrspunlem1 33670  fldextrspunlem2 33672  fldextrspunlsp 33669  fldextrspunlsplem 33668
[BourbakiCAlg2], p. 228Proposition 21arithidom 33508  dfufd2 33521
[BourbakiEns] p. Proposition 8fcof1 7262  fcofo 7263
[BourbakiTop1] p. Remarkxnegmnf 13170  xnegpnf 13169
[BourbakiTop1] p. Remark rexneg 13171
[BourbakiTop1] p. Remark 3ust0 24107  ustfilxp 24100
[BourbakiTop1] p. Axiom GT'tgpsubcn 23977
[BourbakiTop1] p. Criterionishmeo 23646
[BourbakiTop1] p. Example 1cstucnd 24171  iducn 24170  snfil 23751
[BourbakiTop1] p. Example 2neifil 23767
[BourbakiTop1] p. Theorem 1cnextcn 23954
[BourbakiTop1] p. Theorem 2ucnextcn 24191
[BourbakiTop1] p. Theorem 3df-hcmp 33947
[BourbakiTop1] p. Paragraph 3infil 23750
[BourbakiTop1] p. Definition 1df-ucn 24163  df-ust 24088  filintn0 23748  filn0 23749  istgp 23964  ucnprima 24169
[BourbakiTop1] p. Definition 2df-cfilu 24174
[BourbakiTop1] p. Definition 3df-cusp 24185  df-usp 24145  df-utop 24119  trust 24117
[BourbakiTop1] p. Definition 6df-pcmp 33846
[BourbakiTop1] p. Property V_issnei2 23003
[BourbakiTop1] p. Theorem 1(d)iscncl 23156
[BourbakiTop1] p. Condition F_Iustssel 24093
[BourbakiTop1] p. Condition U_Iustdiag 24096
[BourbakiTop1] p. Property V_iiinnei 23012
[BourbakiTop1] p. Property V_ivneiptopreu 23020  neissex 23014
[BourbakiTop1] p. Proposition 1neips 23000  neiss 22996  ucncn 24172  ustund 24109  ustuqtop 24134
[BourbakiTop1] p. Proposition 2cnpco 23154  neiptopreu 23020  utop2nei 24138  utop3cls 24139
[BourbakiTop1] p. Proposition 3fmucnd 24179  uspreg 24161  utopreg 24140
[BourbakiTop1] p. Proposition 4imasncld 23578  imasncls 23579  imasnopn 23577
[BourbakiTop1] p. Proposition 9cnpflf2 23887
[BourbakiTop1] p. Condition F_IIustincl 24095
[BourbakiTop1] p. Condition U_IIustinvel 24097
[BourbakiTop1] p. Property V_iiielnei 22998
[BourbakiTop1] p. Proposition 11cnextucn 24190
[BourbakiTop1] p. Condition F_IIbustbasel 24094
[BourbakiTop1] p. Condition U_IIIustexhalf 24098
[BourbakiTop1] p. Definition C'''df-cmp 23274
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23733
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22781
[BourbakiTop2] p. 195Definition 1df-ldlf 33843
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46060
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46062  stoweid 46061
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 45999  stoweidlem10 46008  stoweidlem14 46012  stoweidlem15 46013  stoweidlem35 46033  stoweidlem36 46034  stoweidlem37 46035  stoweidlem38 46036  stoweidlem40 46038  stoweidlem41 46039  stoweidlem43 46041  stoweidlem44 46042  stoweidlem46 46044  stoweidlem5 46003  stoweidlem50 46048  stoweidlem52 46050  stoweidlem53 46051  stoweidlem55 46053  stoweidlem56 46054
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46021  stoweidlem24 46022  stoweidlem27 46025  stoweidlem28 46026  stoweidlem30 46028
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46032  stoweidlem59 46057  stoweidlem60 46058
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46043  stoweidlem49 46047  stoweidlem7 46005
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46029  stoweidlem39 46037  stoweidlem42 46040  stoweidlem48 46046  stoweidlem51 46049  stoweidlem54 46052  stoweidlem57 46055  stoweidlem58 46056
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46023
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46015
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46009  stoweidlem13 46011  stoweidlem26 46024  stoweidlem61 46059
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46016
[Bruck] p. 1Section I.1df-clintop 48188  df-mgm 18567  df-mgm2 48207
[Bruck] p. 23Section II.1df-sgrp 18646  df-sgrp2 48209
[Bruck] p. 28Theorem 3.2dfgrp3 18971
[ChoquetDD] p. 2Definition of mappingdf-mpt 5189
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 30332
[Clemente] p. 10Definition I` `m,nnatded 30332
[Clemente] p. 11Definition E=>m,nnatded 30332
[Clemente] p. 11Definition I=>m,nnatded 30332
[Clemente] p. 11Definition E` `(1)natded 30332
[Clemente] p. 11Definition E` `(2)natded 30332
[Clemente] p. 12Definition E` `m,n,pnatded 30332
[Clemente] p. 12Definition I` `n(1)natded 30332
[Clemente] p. 12Definition I` `n(2)natded 30332
[Clemente] p. 13Definition I` `m,n,pnatded 30332
[Clemente] p. 14Proof 5.11natded 30332
[Clemente] p. 14Definition E` `nnatded 30332
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30334  ex-natded5.2 30333
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30337  ex-natded5.3 30336
[Clemente] p. 18Theorem 5.5ex-natded5.5 30339
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30341  ex-natded5.7 30340
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30343  ex-natded5.8 30342
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30345  ex-natded5.13 30344
[Clemente] p. 32Definition I` `nnatded 30332
[Clemente] p. 32Definition E` `m,n,p,anatded 30332
[Clemente] p. 32Definition E` `n,tnatded 30332
[Clemente] p. 32Definition I` `n,tnatded 30332
[Clemente] p. 43Theorem 9.20ex-natded9.20 30346
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30347
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30349  ex-natded9.26 30348
[Cohen] p. 301Remarkrelogoprlem 26500
[Cohen] p. 301Property 2relogmul 26501  relogmuld 26534
[Cohen] p. 301Property 3relogdiv 26502  relogdivd 26535
[Cohen] p. 301Property 4relogexp 26505
[Cohen] p. 301Property 1alog1 26494
[Cohen] p. 301Property 1bloge 26495
[Cohen4] p. 348Observationrelogbcxpb 26697
[Cohen4] p. 349Propertyrelogbf 26701
[Cohen4] p. 352Definitionelogb 26680
[Cohen4] p. 361Property 2relogbmul 26687
[Cohen4] p. 361Property 3logbrec 26692  relogbdiv 26689
[Cohen4] p. 361Property 4relogbreexp 26685
[Cohen4] p. 361Property 6relogbexp 26690
[Cohen4] p. 361Property 1(a)logbid1 26678
[Cohen4] p. 361Property 1(b)logb1 26679
[Cohen4] p. 367Propertylogbchbase 26681
[Cohen4] p. 377Property 2logblt 26694
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34276  sxbrsigalem4 34278
[Cohn] p. 81Section II.5acsdomd 18516  acsinfd 18515  acsinfdimd 18517  acsmap2d 18514  acsmapd 18513
[Cohn] p. 143Example 5.1.1sxbrsiga 34281
[Connell] p. 57Definitiondf-scmat 22378  df-scmatalt 48388
[Conway] p. 4Definitionslerec 27731
[Conway] p. 5Definitionaddsval 27869  addsval2 27870  df-adds 27867  df-muls 28010  df-negs 27927
[Conway] p. 7Theorem0slt1s 27741
[Conway] p. 16Theorem 0(i)ssltright 27783
[Conway] p. 16Theorem 0(ii)ssltleft 27782
[Conway] p. 16Theorem 0(iii)slerflex 27675
[Conway] p. 17Theorem 3addsass 27912  addsassd 27913  addscom 27873  addscomd 27874  addsrid 27871  addsridd 27872
[Conway] p. 17Definitiondf-0s 27736
[Conway] p. 17Theorem 4(ii)negnegs 27950
[Conway] p. 17Theorem 4(iii)negsid 27947  negsidd 27948
[Conway] p. 18Theorem 5sleadd1 27896  sleadd1d 27902
[Conway] p. 18Definitiondf-1s 27737
[Conway] p. 18Theorem 6(ii)negscl 27942  negscld 27943
[Conway] p. 18Theorem 6(iii)addscld 27887
[Conway] p. 19Notemulsunif2 28073
[Conway] p. 19Theorem 7addsdi 28058  addsdid 28059  addsdird 28060  mulnegs1d 28063  mulnegs2d 28064  mulsass 28069  mulsassd 28070  mulscom 28042  mulscomd 28043
[Conway] p. 19Theorem 8(i)mulscl 28037  mulscld 28038
[Conway] p. 19Theorem 8(iii)slemuld 28041  sltmul 28039  sltmuld 28040
[Conway] p. 20Theorem 9mulsgt0 28047  mulsgt0d 28048
[Conway] p. 21Theorem 10(iv)precsex 28120
[Conway] p. 24Definitiondf-reno 28345
[Conway] p. 24Theorem 13(ii)readdscl 28350  remulscl 28353  renegscl 28349
[Conway] p. 27Definitiondf-ons 28153  elons2 28159
[Conway] p. 27Theorem 14sltonex 28163
[Conway] p. 28Theorem 15onscutlt 28165  onswe 28170
[Conway] p. 29Remarkmadebday 27811  newbday 27813  oldbday 27812
[Conway] p. 29Definitiondf-made 27755  df-new 27757  df-old 27756
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13823
[Crawley] p. 1Definition of posetdf-poset 18274
[Crawley] p. 107Theorem 13.2hlsupr 39380
[Crawley] p. 110Theorem 13.3arglem1N 40184  dalaw 39880
[Crawley] p. 111Theorem 13.4hlathil 41955
[Crawley] p. 111Definition of set Wdf-watsN 39984
[Crawley] p. 111Definition of dilationdf-dilN 40100  df-ldil 40098  isldil 40104
[Crawley] p. 111Definition of translationdf-ltrn 40099  df-trnN 40101  isltrn 40113  ltrnu 40115
[Crawley] p. 112Lemma Acdlema1N 39785  cdlema2N 39786  exatleN 39398
[Crawley] p. 112Lemma B1cvrat 39470  cdlemb 39788  cdlemb2 40035  cdlemb3 40600  idltrn 40144  l1cvat 39048  lhpat 40037  lhpat2 40039  lshpat 39049  ltrnel 40133  ltrnmw 40145
[Crawley] p. 112Lemma Ccdlemc1 40185  cdlemc2 40186  ltrnnidn 40168  trlat 40163  trljat1 40160  trljat2 40161  trljat3 40162  trlne 40179  trlnidat 40167  trlnle 40180
[Crawley] p. 112Definition of automorphismdf-pautN 39985
[Crawley] p. 113Lemma Ccdlemc 40191  cdlemc3 40187  cdlemc4 40188
[Crawley] p. 113Lemma Dcdlemd 40201  cdlemd1 40192  cdlemd2 40193  cdlemd3 40194  cdlemd4 40195  cdlemd5 40196  cdlemd6 40197  cdlemd7 40198  cdlemd8 40199  cdlemd9 40200  cdleme31sde 40379  cdleme31se 40376  cdleme31se2 40377  cdleme31snd 40380  cdleme32a 40435  cdleme32b 40436  cdleme32c 40437  cdleme32d 40438  cdleme32e 40439  cdleme32f 40440  cdleme32fva 40431  cdleme32fva1 40432  cdleme32fvcl 40434  cdleme32le 40441  cdleme48fv 40493  cdleme4gfv 40501  cdleme50eq 40535  cdleme50f 40536  cdleme50f1 40537  cdleme50f1o 40540  cdleme50laut 40541  cdleme50ldil 40542  cdleme50lebi 40534  cdleme50rn 40539  cdleme50rnlem 40538  cdlemeg49le 40505  cdlemeg49lebilem 40533
[Crawley] p. 113Lemma Ecdleme 40554  cdleme00a 40203  cdleme01N 40215  cdleme02N 40216  cdleme0a 40205  cdleme0aa 40204  cdleme0b 40206  cdleme0c 40207  cdleme0cp 40208  cdleme0cq 40209  cdleme0dN 40210  cdleme0e 40211  cdleme0ex1N 40217  cdleme0ex2N 40218  cdleme0fN 40212  cdleme0gN 40213  cdleme0moN 40219  cdleme1 40221  cdleme10 40248  cdleme10tN 40252  cdleme11 40264  cdleme11a 40254  cdleme11c 40255  cdleme11dN 40256  cdleme11e 40257  cdleme11fN 40258  cdleme11g 40259  cdleme11h 40260  cdleme11j 40261  cdleme11k 40262  cdleme11l 40263  cdleme12 40265  cdleme13 40266  cdleme14 40267  cdleme15 40272  cdleme15a 40268  cdleme15b 40269  cdleme15c 40270  cdleme15d 40271  cdleme16 40279  cdleme16aN 40253  cdleme16b 40273  cdleme16c 40274  cdleme16d 40275  cdleme16e 40276  cdleme16f 40277  cdleme16g 40278  cdleme19a 40297  cdleme19b 40298  cdleme19c 40299  cdleme19d 40300  cdleme19e 40301  cdleme19f 40302  cdleme1b 40220  cdleme2 40222  cdleme20aN 40303  cdleme20bN 40304  cdleme20c 40305  cdleme20d 40306  cdleme20e 40307  cdleme20f 40308  cdleme20g 40309  cdleme20h 40310  cdleme20i 40311  cdleme20j 40312  cdleme20k 40313  cdleme20l 40316  cdleme20l1 40314  cdleme20l2 40315  cdleme20m 40317  cdleme20y 40296  cdleme20zN 40295  cdleme21 40331  cdleme21d 40324  cdleme21e 40325  cdleme22a 40334  cdleme22aa 40333  cdleme22b 40335  cdleme22cN 40336  cdleme22d 40337  cdleme22e 40338  cdleme22eALTN 40339  cdleme22f 40340  cdleme22f2 40341  cdleme22g 40342  cdleme23a 40343  cdleme23b 40344  cdleme23c 40345  cdleme26e 40353  cdleme26eALTN 40355  cdleme26ee 40354  cdleme26f 40357  cdleme26f2 40359  cdleme26f2ALTN 40358  cdleme26fALTN 40356  cdleme27N 40363  cdleme27a 40361  cdleme27cl 40360  cdleme28c 40366  cdleme3 40231  cdleme30a 40372  cdleme31fv 40384  cdleme31fv1 40385  cdleme31fv1s 40386  cdleme31fv2 40387  cdleme31id 40388  cdleme31sc 40378  cdleme31sdnN 40381  cdleme31sn 40374  cdleme31sn1 40375  cdleme31sn1c 40382  cdleme31sn2 40383  cdleme31so 40373  cdleme35a 40442  cdleme35b 40444  cdleme35c 40445  cdleme35d 40446  cdleme35e 40447  cdleme35f 40448  cdleme35fnpq 40443  cdleme35g 40449  cdleme35h 40450  cdleme35h2 40451  cdleme35sn2aw 40452  cdleme35sn3a 40453  cdleme36a 40454  cdleme36m 40455  cdleme37m 40456  cdleme38m 40457  cdleme38n 40458  cdleme39a 40459  cdleme39n 40460  cdleme3b 40223  cdleme3c 40224  cdleme3d 40225  cdleme3e 40226  cdleme3fN 40227  cdleme3fa 40230  cdleme3g 40228  cdleme3h 40229  cdleme4 40232  cdleme40m 40461  cdleme40n 40462  cdleme40v 40463  cdleme40w 40464  cdleme41fva11 40471  cdleme41sn3aw 40468  cdleme41sn4aw 40469  cdleme41snaw 40470  cdleme42a 40465  cdleme42b 40472  cdleme42c 40466  cdleme42d 40467  cdleme42e 40473  cdleme42f 40474  cdleme42g 40475  cdleme42h 40476  cdleme42i 40477  cdleme42k 40478  cdleme42ke 40479  cdleme42keg 40480  cdleme42mN 40481  cdleme42mgN 40482  cdleme43aN 40483  cdleme43bN 40484  cdleme43cN 40485  cdleme43dN 40486  cdleme5 40234  cdleme50ex 40553  cdleme50ltrn 40551  cdleme51finvN 40550  cdleme51finvfvN 40549  cdleme51finvtrN 40552  cdleme6 40235  cdleme7 40243  cdleme7a 40237  cdleme7aa 40236  cdleme7b 40238  cdleme7c 40239  cdleme7d 40240  cdleme7e 40241  cdleme7ga 40242  cdleme8 40244  cdleme8tN 40249  cdleme9 40247  cdleme9a 40245  cdleme9b 40246  cdleme9tN 40251  cdleme9taN 40250  cdlemeda 40292  cdlemedb 40291  cdlemednpq 40293  cdlemednuN 40294  cdlemefr27cl 40397  cdlemefr32fva1 40404  cdlemefr32fvaN 40403  cdlemefrs32fva 40394  cdlemefrs32fva1 40395  cdlemefs27cl 40407  cdlemefs32fva1 40417  cdlemefs32fvaN 40416  cdlemesner 40290  cdlemeulpq 40214
[Crawley] p. 114Lemma E4atex 40070  4atexlem7 40069  cdleme0nex 40284  cdleme17a 40280  cdleme17c 40282  cdleme17d 40492  cdleme17d1 40283  cdleme17d2 40489  cdleme18a 40285  cdleme18b 40286  cdleme18c 40287  cdleme18d 40289  cdleme4a 40233
[Crawley] p. 115Lemma Ecdleme21a 40319  cdleme21at 40322  cdleme21b 40320  cdleme21c 40321  cdleme21ct 40323  cdleme21f 40326  cdleme21g 40327  cdleme21h 40328  cdleme21i 40329  cdleme22gb 40288
[Crawley] p. 116Lemma Fcdlemf 40557  cdlemf1 40555  cdlemf2 40556
[Crawley] p. 116Lemma Gcdlemftr1 40561  cdlemg16 40651  cdlemg28 40698  cdlemg28a 40687  cdlemg28b 40697  cdlemg3a 40591  cdlemg42 40723  cdlemg43 40724  cdlemg44 40727  cdlemg44a 40725  cdlemg46 40729  cdlemg47 40730  cdlemg9 40628  ltrnco 40713  ltrncom 40732  tgrpabl 40745  trlco 40721
[Crawley] p. 116Definition of Gdf-tgrp 40737
[Crawley] p. 117Lemma Gcdlemg17 40671  cdlemg17b 40656
[Crawley] p. 117Definition of Edf-edring-rN 40750  df-edring 40751
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 40754
[Crawley] p. 118Remarktendopltp 40774
[Crawley] p. 118Lemma Hcdlemh 40811  cdlemh1 40809  cdlemh2 40810
[Crawley] p. 118Lemma Icdlemi 40814  cdlemi1 40812  cdlemi2 40813
[Crawley] p. 118Lemma Jcdlemj1 40815  cdlemj2 40816  cdlemj3 40817  tendocan 40818
[Crawley] p. 118Lemma Kcdlemk 40968  cdlemk1 40825  cdlemk10 40837  cdlemk11 40843  cdlemk11t 40940  cdlemk11ta 40923  cdlemk11tb 40925  cdlemk11tc 40939  cdlemk11u-2N 40883  cdlemk11u 40865  cdlemk12 40844  cdlemk12u-2N 40884  cdlemk12u 40866  cdlemk13-2N 40870  cdlemk13 40846  cdlemk14-2N 40872  cdlemk14 40848  cdlemk15-2N 40873  cdlemk15 40849  cdlemk16-2N 40874  cdlemk16 40851  cdlemk16a 40850  cdlemk17-2N 40875  cdlemk17 40852  cdlemk18-2N 40880  cdlemk18-3N 40894  cdlemk18 40862  cdlemk19-2N 40881  cdlemk19 40863  cdlemk19u 40964  cdlemk1u 40853  cdlemk2 40826  cdlemk20-2N 40886  cdlemk20 40868  cdlemk21-2N 40885  cdlemk21N 40867  cdlemk22-3 40895  cdlemk22 40887  cdlemk23-3 40896  cdlemk24-3 40897  cdlemk25-3 40898  cdlemk26-3 40900  cdlemk26b-3 40899  cdlemk27-3 40901  cdlemk28-3 40902  cdlemk29-3 40905  cdlemk3 40827  cdlemk30 40888  cdlemk31 40890  cdlemk32 40891  cdlemk33N 40903  cdlemk34 40904  cdlemk35 40906  cdlemk36 40907  cdlemk37 40908  cdlemk38 40909  cdlemk39 40910  cdlemk39u 40962  cdlemk4 40828  cdlemk41 40914  cdlemk42 40935  cdlemk42yN 40938  cdlemk43N 40957  cdlemk45 40941  cdlemk46 40942  cdlemk47 40943  cdlemk48 40944  cdlemk49 40945  cdlemk5 40830  cdlemk50 40946  cdlemk51 40947  cdlemk52 40948  cdlemk53 40951  cdlemk54 40952  cdlemk55 40955  cdlemk55u 40960  cdlemk56 40965  cdlemk5a 40829  cdlemk5auN 40854  cdlemk5u 40855  cdlemk6 40831  cdlemk6u 40856  cdlemk7 40842  cdlemk7u-2N 40882  cdlemk7u 40864  cdlemk8 40832  cdlemk9 40833  cdlemk9bN 40834  cdlemki 40835  cdlemkid 40930  cdlemkj-2N 40876  cdlemkj 40857  cdlemksat 40840  cdlemksel 40839  cdlemksv 40838  cdlemksv2 40841  cdlemkuat 40860  cdlemkuel-2N 40878  cdlemkuel-3 40892  cdlemkuel 40859  cdlemkuv-2N 40877  cdlemkuv2-2 40879  cdlemkuv2-3N 40893  cdlemkuv2 40861  cdlemkuvN 40858  cdlemkvcl 40836  cdlemky 40920  cdlemkyyN 40956  tendoex 40969
[Crawley] p. 120Remarkdva1dim 40979
[Crawley] p. 120Lemma Lcdleml1N 40970  cdleml2N 40971  cdleml3N 40972  cdleml4N 40973  cdleml5N 40974  cdleml6 40975  cdleml7 40976  cdleml8 40977  cdleml9 40978  dia1dim 41055
[Crawley] p. 120Lemma Mdia11N 41042  diaf11N 41043  dialss 41040  diaord 41041  dibf11N 41155  djajN 41131
[Crawley] p. 120Definition of isomorphism mapdiaval 41026
[Crawley] p. 121Lemma Mcdlemm10N 41112  dia2dimlem1 41058  dia2dimlem2 41059  dia2dimlem3 41060  dia2dimlem4 41061  dia2dimlem5 41062  diaf1oN 41124  diarnN 41123  dvheveccl 41106  dvhopN 41110
[Crawley] p. 121Lemma Ncdlemn 41206  cdlemn10 41200  cdlemn11 41205  cdlemn11a 41201  cdlemn11b 41202  cdlemn11c 41203  cdlemn11pre 41204  cdlemn2 41189  cdlemn2a 41190  cdlemn3 41191  cdlemn4 41192  cdlemn4a 41193  cdlemn5 41195  cdlemn5pre 41194  cdlemn6 41196  cdlemn7 41197  cdlemn8 41198  cdlemn9 41199  diclspsn 41188
[Crawley] p. 121Definition of phi(q)df-dic 41167
[Crawley] p. 122Lemma Ndih11 41259  dihf11 41261  dihjust 41211  dihjustlem 41210  dihord 41258  dihord1 41212  dihord10 41217  dihord11b 41216  dihord11c 41218  dihord2 41221  dihord2a 41213  dihord2b 41214  dihord2cN 41215  dihord2pre 41219  dihord2pre2 41220  dihordlem6 41207  dihordlem7 41208  dihordlem7b 41209
[Crawley] p. 122Definition of isomorphism mapdihffval 41224  dihfval 41225  dihval 41226
[Diestel] p. 3Definitiondf-gric 47881  df-grim 47878  isuspgrim 47896
[Diestel] p. 3Section 1.1df-cusgr 29339  df-nbgr 29260
[Diestel] p. 3Definition by df-grisom 47877
[Diestel] p. 4Section 1.1df-isubgr 47861  df-subgr 29195  uhgrspan1 29230  uhgrspansubgr 29218
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29482  vtxdgoddnumeven 29481
[Diestel] p. 27Section 1.10df-ushgr 28986
[EGA] p. 80Notation 1.1.1rspecval 33854
[EGA] p. 80Proposition 1.1.2zartop 33866
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33858  zarcls1 33859
[EGA] p. 81Corollary 1.1.8zart0 33869
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33872
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33875
[Eisenberg] p. 67Definition 5.3df-dif 3917
[Eisenberg] p. 82Definition 6.3dfom3 9600
[Eisenberg] p. 125Definition 8.21df-map 8801
[Eisenberg] p. 216Example 13.2(4)omenps 9608
[Eisenberg] p. 310Theorem 19.8cardprc 9933
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10508
[Enderton] p. 18Axiom of Empty Setaxnul 5260
[Enderton] p. 19Definitiondf-tp 4594
[Enderton] p. 26Exercise 5unissb 4903
[Enderton] p. 26Exercise 10pwel 5336
[Enderton] p. 28Exercise 7(b)pwun 5531
[Enderton] p. 30Theorem "Distributive laws"iinin1 5043  iinin2 5042  iinun2 5037  iunin1 5036  iunin1f 32486  iunin2 5035  uniin1 32480  uniin2 32481
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5041  iundif2 5038
[Enderton] p. 32Exercise 20unineq 4251
[Enderton] p. 33Exercise 23iinuni 5062
[Enderton] p. 33Exercise 25iununi 5063
[Enderton] p. 33Exercise 24(a)iinpw 5070
[Enderton] p. 33Exercise 24(b)iunpw 7747  iunpwss 5071
[Enderton] p. 36Definitionopthwiener 5474
[Enderton] p. 38Exercise 6(a)unipw 5410
[Enderton] p. 38Exercise 6(b)pwuni 4909
[Enderton] p. 41Lemma 3Dopeluu 5430  rnex 7886  rnexg 7878
[Enderton] p. 41Exercise 8dmuni 5878  rnuni 6121
[Enderton] p. 42Definition of a functiondffun7 6543  dffun8 6544
[Enderton] p. 43Definition of function valuefunfv2 6949
[Enderton] p. 43Definition of single-rootedfuncnv 6585
[Enderton] p. 44Definition (d)dfima2 6033  dfima3 6034
[Enderton] p. 47Theorem 3Hfvco2 6958
[Enderton] p. 49Axiom of Choice (first form)ac7 10426  ac7g 10427  df-ac 10069  dfac2 10085  dfac2a 10083  dfac2b 10084  dfac3 10074  dfac7 10086
[Enderton] p. 50Theorem 3K(a)imauni 7220
[Enderton] p. 52Definitiondf-map 8801
[Enderton] p. 53Exercise 21coass 6238
[Enderton] p. 53Exercise 27dmco 6227
[Enderton] p. 53Exercise 14(a)funin 6592
[Enderton] p. 53Exercise 22(a)imass2 6073
[Enderton] p. 54Remarkixpf 8893  ixpssmap 8905
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8871
[Enderton] p. 55Axiom of Choice (second form)ac9 10436  ac9s 10446
[Enderton] p. 56Theorem 3Meqvrelref 38601  erref 8691
[Enderton] p. 57Lemma 3Neqvrelthi 38604  erthi 8727
[Enderton] p. 57Definitiondf-ec 8673
[Enderton] p. 58Definitiondf-qs 8677
[Enderton] p. 61Exercise 35df-ec 8673
[Enderton] p. 65Exercise 56(a)dmun 5874
[Enderton] p. 68Definition of successordf-suc 6338
[Enderton] p. 71Definitiondf-tr 5215  dftr4 5221
[Enderton] p. 72Theorem 4Eunisuc 6413  unisucg 6412
[Enderton] p. 73Exercise 6unisuc 6413  unisucg 6412
[Enderton] p. 73Exercise 5(a)truni 5230
[Enderton] p. 73Exercise 5(b)trint 5232  trintALT 44870
[Enderton] p. 79Theorem 4I(A1)nna0 8568
[Enderton] p. 79Theorem 4I(A2)nnasuc 8570  onasuc 8492
[Enderton] p. 79Definition of operation valuedf-ov 7390
[Enderton] p. 80Theorem 4J(A1)nnm0 8569
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8571  onmsuc 8493
[Enderton] p. 81Theorem 4K(1)nnaass 8586
[Enderton] p. 81Theorem 4K(2)nna0r 8573  nnacom 8581
[Enderton] p. 81Theorem 4K(3)nndi 8587
[Enderton] p. 81Theorem 4K(4)nnmass 8588
[Enderton] p. 81Theorem 4K(5)nnmcom 8590
[Enderton] p. 82Exercise 16nnm0r 8574  nnmsucr 8589
[Enderton] p. 88Exercise 23nnaordex 8602
[Enderton] p. 129Definitiondf-en 8919
[Enderton] p. 132Theorem 6B(b)canth 7341
[Enderton] p. 133Exercise 1xpomen 9968
[Enderton] p. 133Exercise 2qnnen 16181
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9171
[Enderton] p. 135Corollary 6Cphp3 9173
[Enderton] p. 136Corollary 6Enneneq 9170
[Enderton] p. 136Corollary 6D(a)pssinf 9203
[Enderton] p. 136Corollary 6D(b)ominf 9205
[Enderton] p. 137Lemma 6Fpssnn 9132
[Enderton] p. 138Corollary 6Gssfi 9137
[Enderton] p. 139Theorem 6H(c)mapen 9105
[Enderton] p. 142Theorem 6I(3)xpdjuen 10133
[Enderton] p. 142Theorem 6I(4)mapdjuen 10134
[Enderton] p. 143Theorem 6Jdju0en 10129  dju1en 10125
[Enderton] p. 144Exercise 13iunfi 9294  unifi 9295  unifi2 9296
[Enderton] p. 144Corollary 6Kundif2 4440  unfi 9135  unfi2 9259
[Enderton] p. 145Figure 38ffoss 7924
[Enderton] p. 145Definitiondf-dom 8920
[Enderton] p. 146Example 1domen 8933  domeng 8934
[Enderton] p. 146Example 3nndomo 9181  nnsdom 9607  nnsdomg 9246
[Enderton] p. 149Theorem 6L(a)djudom2 10137
[Enderton] p. 149Theorem 6L(c)mapdom1 9106  xpdom1 9040  xpdom1g 9038  xpdom2g 9037
[Enderton] p. 149Theorem 6L(d)mapdom2 9112
[Enderton] p. 151Theorem 6Mzorn 10460  zorng 10457
[Enderton] p. 151Theorem 6M(4)ac8 10445  dfac5 10082
[Enderton] p. 159Theorem 6Qunictb 10528
[Enderton] p. 164Exampleinfdif 10161
[Enderton] p. 168Definitiondf-po 5546
[Enderton] p. 192Theorem 7M(a)oneli 6448
[Enderton] p. 192Theorem 7M(b)ontr1 6379
[Enderton] p. 192Theorem 7M(c)onirri 6447
[Enderton] p. 193Corollary 7N(b)0elon 6387
[Enderton] p. 193Corollary 7N(c)onsuci 7814
[Enderton] p. 193Corollary 7N(d)ssonunii 7757
[Enderton] p. 194Remarkonprc 7754
[Enderton] p. 194Exercise 16suc11 6441
[Enderton] p. 197Definitiondf-card 9892
[Enderton] p. 197Theorem 7Pcarden 10504
[Enderton] p. 200Exercise 25tfis 7831
[Enderton] p. 202Lemma 7Tr1tr 9729
[Enderton] p. 202Definitiondf-r1 9717
[Enderton] p. 202Theorem 7Qr1val1 9739
[Enderton] p. 204Theorem 7V(b)rankval4 9820
[Enderton] p. 206Theorem 7X(b)en2lp 9559
[Enderton] p. 207Exercise 30rankpr 9810  rankprb 9804  rankpw 9796  rankpwi 9776  rankuniss 9819
[Enderton] p. 207Exercise 34opthreg 9571
[Enderton] p. 208Exercise 35suc11reg 9572
[Enderton] p. 212Definition of alephalephval3 10063
[Enderton] p. 213Theorem 8A(a)alephord2 10029
[Enderton] p. 213Theorem 8A(b)cardalephex 10043
[Enderton] p. 218Theorem Schema 8Eonfununi 8310
[Enderton] p. 222Definition of kardkarden 9848  kardex 9847
[Enderton] p. 238Theorem 8Roeoa 8561
[Enderton] p. 238Theorem 8Soeoe 8563
[Enderton] p. 240Exercise 25oarec 8526
[Enderton] p. 257Definition of cofinalitycflm 10203
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17603
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17549
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18512  mrieqv2d 17600  mrieqvd 17599
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17604
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17609  mreexexlem2d 17606
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18518  mreexfidimd 17611
[Frege1879] p. 11Statementdf3or2 43757
[Frege1879] p. 12Statementdf3an2 43758  dfxor4 43755  dfxor5 43756
[Frege1879] p. 26Axiom 1ax-frege1 43779
[Frege1879] p. 26Axiom 2ax-frege2 43780
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 43784
[Frege1879] p. 31Proposition 4frege4 43788
[Frege1879] p. 32Proposition 5frege5 43789
[Frege1879] p. 33Proposition 6frege6 43795
[Frege1879] p. 34Proposition 7frege7 43797
[Frege1879] p. 35Axiom 8ax-frege8 43798  axfrege8 43796
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37433
[Frege1879] p. 35Proposition 9frege9 43801
[Frege1879] p. 36Proposition 10frege10 43809
[Frege1879] p. 36Proposition 11frege11 43803
[Frege1879] p. 37Proposition 12frege12 43802
[Frege1879] p. 37Proposition 13frege13 43811
[Frege1879] p. 37Proposition 14frege14 43812
[Frege1879] p. 38Proposition 15frege15 43815
[Frege1879] p. 38Proposition 16frege16 43805
[Frege1879] p. 39Proposition 17frege17 43810
[Frege1879] p. 39Proposition 18frege18 43807
[Frege1879] p. 39Proposition 19frege19 43813
[Frege1879] p. 40Proposition 20frege20 43817
[Frege1879] p. 40Proposition 21frege21 43816
[Frege1879] p. 41Proposition 22frege22 43808
[Frege1879] p. 42Proposition 23frege23 43814
[Frege1879] p. 42Proposition 24frege24 43804
[Frege1879] p. 42Proposition 25frege25 43806  rp-frege25 43794
[Frege1879] p. 42Proposition 26frege26 43799
[Frege1879] p. 43Axiom 28ax-frege28 43819
[Frege1879] p. 43Proposition 27frege27 43800
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 43820
[Frege1879] p. 44Axiom 31ax-frege31 43823  axfrege31 43822
[Frege1879] p. 44Proposition 30frege30 43821
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 43824
[Frege1879] p. 44Proposition 33frege33 43825
[Frege1879] p. 45Proposition 34frege34 43826
[Frege1879] p. 45Proposition 35frege35 43827
[Frege1879] p. 45Proposition 36frege36 43828
[Frege1879] p. 46Proposition 37frege37 43829
[Frege1879] p. 46Proposition 38frege38 43830
[Frege1879] p. 46Proposition 39frege39 43831
[Frege1879] p. 46Proposition 40frege40 43832
[Frege1879] p. 47Axiom 41ax-frege41 43834  axfrege41 43833
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 43835
[Frege1879] p. 47Proposition 43frege43 43836
[Frege1879] p. 47Proposition 44frege44 43837
[Frege1879] p. 47Proposition 45frege45 43838
[Frege1879] p. 48Proposition 46frege46 43839
[Frege1879] p. 48Proposition 47frege47 43840
[Frege1879] p. 49Proposition 48frege48 43841
[Frege1879] p. 49Proposition 49frege49 43842
[Frege1879] p. 49Proposition 50frege50 43843
[Frege1879] p. 50Axiom 52ax-frege52a 43846  ax-frege52c 43877  frege52aid 43847  frege52b 43878
[Frege1879] p. 50Axiom 54ax-frege54a 43851  ax-frege54c 43881  frege54b 43882
[Frege1879] p. 50Proposition 51frege51 43844
[Frege1879] p. 50Proposition 52dfsbcq 3755
[Frege1879] p. 50Proposition 53frege53a 43849  frege53aid 43848  frege53b 43879  frege53c 43903
[Frege1879] p. 50Proposition 54biid 261  eqid 2729
[Frege1879] p. 50Proposition 55frege55a 43857  frege55aid 43854  frege55b 43886  frege55c 43907  frege55cor1a 43858  frege55lem2a 43856  frege55lem2b 43885  frege55lem2c 43906
[Frege1879] p. 50Proposition 56frege56a 43860  frege56aid 43859  frege56b 43887  frege56c 43908
[Frege1879] p. 51Axiom 58ax-frege58a 43864  ax-frege58b 43890  frege58bid 43891  frege58c 43910
[Frege1879] p. 51Proposition 57frege57a 43862  frege57aid 43861  frege57b 43888  frege57c 43909
[Frege1879] p. 51Proposition 58spsbc 3766
[Frege1879] p. 51Proposition 59frege59a 43866  frege59b 43893  frege59c 43911
[Frege1879] p. 52Proposition 60frege60a 43867  frege60b 43894  frege60c 43912
[Frege1879] p. 52Proposition 61frege61a 43868  frege61b 43895  frege61c 43913
[Frege1879] p. 52Proposition 62frege62a 43869  frege62b 43896  frege62c 43914
[Frege1879] p. 52Proposition 63frege63a 43870  frege63b 43897  frege63c 43915
[Frege1879] p. 53Proposition 64frege64a 43871  frege64b 43898  frege64c 43916
[Frege1879] p. 53Proposition 65frege65a 43872  frege65b 43899  frege65c 43917
[Frege1879] p. 54Proposition 66frege66a 43873  frege66b 43900  frege66c 43918
[Frege1879] p. 54Proposition 67frege67a 43874  frege67b 43901  frege67c 43919
[Frege1879] p. 54Proposition 68frege68a 43875  frege68b 43902  frege68c 43920
[Frege1879] p. 55Definition 69dffrege69 43921
[Frege1879] p. 58Proposition 70frege70 43922
[Frege1879] p. 59Proposition 71frege71 43923
[Frege1879] p. 59Proposition 72frege72 43924
[Frege1879] p. 59Proposition 73frege73 43925
[Frege1879] p. 60Definition 76dffrege76 43928
[Frege1879] p. 60Proposition 74frege74 43926
[Frege1879] p. 60Proposition 75frege75 43927
[Frege1879] p. 62Proposition 77frege77 43929  frege77d 43735
[Frege1879] p. 63Proposition 78frege78 43930
[Frege1879] p. 63Proposition 79frege79 43931
[Frege1879] p. 63Proposition 80frege80 43932
[Frege1879] p. 63Proposition 81frege81 43933  frege81d 43736
[Frege1879] p. 64Proposition 82frege82 43934
[Frege1879] p. 65Proposition 83frege83 43935  frege83d 43737
[Frege1879] p. 65Proposition 84frege84 43936
[Frege1879] p. 66Proposition 85frege85 43937
[Frege1879] p. 66Proposition 86frege86 43938
[Frege1879] p. 66Proposition 87frege87 43939  frege87d 43739
[Frege1879] p. 67Proposition 88frege88 43940
[Frege1879] p. 68Proposition 89frege89 43941
[Frege1879] p. 68Proposition 90frege90 43942
[Frege1879] p. 68Proposition 91frege91 43943  frege91d 43740
[Frege1879] p. 69Proposition 92frege92 43944
[Frege1879] p. 70Proposition 93frege93 43945
[Frege1879] p. 70Proposition 94frege94 43946
[Frege1879] p. 70Proposition 95frege95 43947
[Frege1879] p. 71Definition 99dffrege99 43951
[Frege1879] p. 71Proposition 96frege96 43948  frege96d 43738
[Frege1879] p. 71Proposition 97frege97 43949  frege97d 43741
[Frege1879] p. 71Proposition 98frege98 43950  frege98d 43742
[Frege1879] p. 72Proposition 100frege100 43952
[Frege1879] p. 72Proposition 101frege101 43953
[Frege1879] p. 72Proposition 102frege102 43954  frege102d 43743
[Frege1879] p. 73Proposition 103frege103 43955
[Frege1879] p. 73Proposition 104frege104 43956
[Frege1879] p. 73Proposition 105frege105 43957
[Frege1879] p. 73Proposition 106frege106 43958  frege106d 43744
[Frege1879] p. 74Proposition 107frege107 43959
[Frege1879] p. 74Proposition 108frege108 43960  frege108d 43745
[Frege1879] p. 74Proposition 109frege109 43961  frege109d 43746
[Frege1879] p. 75Proposition 110frege110 43962
[Frege1879] p. 75Proposition 111frege111 43963  frege111d 43748
[Frege1879] p. 76Proposition 112frege112 43964
[Frege1879] p. 76Proposition 113frege113 43965
[Frege1879] p. 76Proposition 114frege114 43966  frege114d 43747
[Frege1879] p. 77Definition 115dffrege115 43967
[Frege1879] p. 77Proposition 116frege116 43968
[Frege1879] p. 78Proposition 117frege117 43969
[Frege1879] p. 78Proposition 118frege118 43970
[Frege1879] p. 78Proposition 119frege119 43971
[Frege1879] p. 78Proposition 120frege120 43972
[Frege1879] p. 79Proposition 121frege121 43973
[Frege1879] p. 79Proposition 122frege122 43974  frege122d 43749
[Frege1879] p. 79Proposition 123frege123 43975
[Frege1879] p. 80Proposition 124frege124 43976  frege124d 43750
[Frege1879] p. 81Proposition 125frege125 43977
[Frege1879] p. 81Proposition 126frege126 43978  frege126d 43751
[Frege1879] p. 82Proposition 127frege127 43979
[Frege1879] p. 83Proposition 128frege128 43980
[Frege1879] p. 83Proposition 129frege129 43981  frege129d 43752
[Frege1879] p. 84Proposition 130frege130 43982
[Frege1879] p. 85Proposition 131frege131 43983  frege131d 43753
[Frege1879] p. 86Proposition 132frege132 43984
[Frege1879] p. 86Proposition 133frege133 43985  frege133d 43754
[Fremlin1] p. 13Definition 111G (b)df-salgen 46311
[Fremlin1] p. 13Definition 111G (d)borelmbl 46634
[Fremlin1] p. 13Proposition 111G (b)salgenss 46334
[Fremlin1] p. 14Definition 112Aismea 46449
[Fremlin1] p. 15Remark 112B (d)psmeasure 46469
[Fremlin1] p. 15Property 112C (a)meadjun 46460  meadjunre 46474
[Fremlin1] p. 15Property 112C (b)meassle 46461
[Fremlin1] p. 15Property 112C (c)meaunle 46462
[Fremlin1] p. 16Property 112C (d)iundjiun 46458  meaiunle 46467  meaiunlelem 46466
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46479  meaiuninc2 46480  meaiuninc3 46483  meaiuninc3v 46482  meaiunincf 46481  meaiuninclem 46478
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46485  meaiininc2 46486  meaiininclem 46484
[Fremlin1] p. 19Theorem 113Ccaragen0 46504  caragendifcl 46512  caratheodory 46526  omelesplit 46516
[Fremlin1] p. 19Definition 113Aisome 46492  isomennd 46529  isomenndlem 46528
[Fremlin1] p. 19Remark 113B (c)omeunle 46514
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46533  voncmpl 46619
[Fremlin1] p. 19Definition 113A (ii)omessle 46496
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46521  carageniuncllem1 46519  carageniuncllem2 46520  caragenuncl 46511  caragenuncllem 46510  caragenunicl 46522
[Fremlin1] p. 21Remark 113Dcaragenel2d 46530
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46524  caratheodorylem2 46525
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46533
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46592  hoidmv1lelem1 46589  hoidmv1lelem2 46590  hoidmv1lelem3 46591
[Fremlin1] p. 25Definition 114Eisvonmbl 46636
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46592  hoidmvle 46598  hoidmvlelem1 46593  hoidmvlelem2 46594  hoidmvlelem3 46595  hoidmvlelem4 46596  hoidmvlelem5 46597  hsphoidmvle2 46583  hsphoif 46574  hsphoival 46577
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46546
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46554
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46581  hoidmvn0val 46582  hoidmvval 46575  hoidmvval0 46585  hoidmvval0b 46588
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46586  hsphoidmvle 46584
[Fremlin1] p. 30Definition 115Cdf-ovoln 46535  df-voln 46537
[Fremlin1] p. 30Proposition 115D (a)dmovn 46602  ovn0 46564  ovn0lem 46563  ovnf 46561  ovnome 46571  ovnssle 46559  ovnsslelem 46558  ovnsupge0 46555
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46601  ovnhoilem1 46599  ovnhoilem2 46600  vonhoi 46665
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46618  hoidifhspf 46616  hoidifhspval 46606  hoidifhspval2 46613  hoidifhspval3 46617  hspmbl 46627  hspmbllem1 46624  hspmbllem2 46625  hspmbllem3 46626
[Fremlin1] p. 31Definition 115Evoncmpl 46619  vonmea 46572
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46570  ovnsubadd2 46644  ovnsubadd2lem 46643  ovnsubaddlem1 46568  ovnsubaddlem2 46569
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46629  hoimbl2 46663  hoimbllem 46628  hspdifhsp 46614  opnvonmbl 46632  opnvonmbllem2 46631
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46634
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 46677  iccvonmbllem 46676  ioovonmbl 46675
[Fremlin1] p. 32Proposition 115G (d)vonicc 46683  vonicclem2 46682  vonioo 46680  vonioolem2 46679  vonn0icc 46686  vonn0icc2 46690  vonn0ioo 46685  vonn0ioo2 46688
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 46687  snvonmbl 46684  vonct 46691  vonsn 46689
[Fremlin1] p. 35Lemma 121Asubsalsal 46357
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46356  subsaliuncllem 46355
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 46723  salpreimalegt 46707  salpreimaltle 46724
[Fremlin1] p. 35Proposition 121B (i)issmf 46726  issmff 46732  issmflem 46725
[Fremlin1] p. 35Proposition 121B (ii)issmfle 46743  issmflelem 46742  smfpreimale 46752
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 46754  issmfgtlem 46753
[Fremlin1] p. 36Definition 121Cdf-smblfn 46694  issmf 46726  issmff 46732  issmfge 46768  issmfgelem 46767  issmfgt 46754  issmfgtlem 46753  issmfle 46743  issmflelem 46742  issmflem 46725
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 46705  salpreimagtlt 46728  salpreimalelt 46727
[Fremlin1] p. 36Proposition 121B (iv)issmfge 46768  issmfgelem 46767
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 46751
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 46749  cnfsmf 46738
[Fremlin1] p. 36Proposition 121D (c)decsmf 46765  decsmflem 46764  incsmf 46740  incsmflem 46739
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 46699  pimconstlt1 46700  smfconst 46747
[Fremlin1] p. 37Proposition 121E (b)smfadd 46763  smfaddlem1 46761  smfaddlem2 46762
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 46794
[Fremlin1] p. 37Proposition 121E (d)smfmul 46793  smfmullem1 46789  smfmullem2 46790  smfmullem3 46791  smfmullem4 46792
[Fremlin1] p. 37Proposition 121E (e)smfdiv 46795
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 46798  smfpimbor1lem2 46797
[Fremlin1] p. 37Proposition 121E (g)smfco 46800
[Fremlin1] p. 37Proposition 121E (h)smfres 46788
[Fremlin1] p. 38Proposition 121E (e)smfrec 46787
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 46796  smfresal 46786
[Fremlin1] p. 38Proposition 121F (a)smflim 46775  smflim2 46804  smflimlem1 46769  smflimlem2 46770  smflimlem3 46771  smflimlem4 46772  smflimlem5 46773  smflimlem6 46774  smflimmpt 46808
[Fremlin1] p. 38Proposition 121F (b)smfsup 46812  smfsuplem1 46809  smfsuplem2 46810  smfsuplem3 46811  smfsupmpt 46813  smfsupxr 46814
[Fremlin1] p. 38Proposition 121F (c)smfinf 46816  smfinflem 46815  smfinfmpt 46817
[Fremlin1] p. 39Remark 121Gsmflim 46775  smflim2 46804  smflimmpt 46808
[Fremlin1] p. 39Proposition 121Fsmfpimcc 46806
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 46836  smfdivdmmbl2 46839  smfinfdmmbl 46847  smfinfdmmbllem 46846  smfsupdmmbl 46843  smfsupdmmbllem 46842
[Fremlin1] p. 39Proposition 121F (d)smflimsup 46826  smflimsuplem2 46819  smflimsuplem6 46823  smflimsuplem7 46824  smflimsuplem8 46825  smflimsupmpt 46827
[Fremlin1] p. 39Proposition 121F (e)smfliminf 46829  smfliminflem 46828  smfliminfmpt 46830
[Fremlin1] p. 80Definition 135E (b)df-smblfn 46694
[Fremlin1], p. 38Proposition 121F (b)fsupdm 46840  fsupdm2 46841
[Fremlin1], p. 39Proposition 121Hadddmmbl 46831  adddmmbl2 46832  finfdm 46844  finfdm2 46845  fsupdm 46840  fsupdm2 46841  muldmmbl 46833  muldmmbl2 46834
[Fremlin1], p. 39Proposition 121F (c)finfdm 46844  finfdm2 46845
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25437
[Fremlin5] p. 213Lemma 565Cauniioovol 25480
[Fremlin5] p. 214Lemma 565Cauniioombl 25490
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37692
[Fremlin5] p. 220Theorem 565Maftc1anc 37695
[FreydScedrov] p. 283Axiom of Infinityax-inf 9591  inf1 9575  inf2 9576
[Gleason] p. 117Proposition 9-2.1df-enq 10864  enqer 10874
[Gleason] p. 117Proposition 9-2.2df-1nq 10869  df-nq 10865
[Gleason] p. 117Proposition 9-2.3df-plpq 10861  df-plq 10867
[Gleason] p. 119Proposition 9-2.4caovmo 7626  df-mpq 10862  df-mq 10868
[Gleason] p. 119Proposition 9-2.5df-rq 10870
[Gleason] p. 119Proposition 9-2.6ltexnq 10928
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10929  ltbtwnnq 10931
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10924
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10925
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10932
[Gleason] p. 121Definition 9-3.1df-np 10934
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10946
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10948
[Gleason] p. 122Definitiondf-1p 10935
[Gleason] p. 122Remark (1)prub 10947
[Gleason] p. 122Lemma 9-3.4prlem934 10986
[Gleason] p. 122Proposition 9-3.2df-ltp 10938
[Gleason] p. 122Proposition 9-3.3ltsopr 10985  psslinpr 10984  supexpr 11007  suplem1pr 11005  suplem2pr 11006
[Gleason] p. 123Proposition 9-3.5addclpr 10971  addclprlem1 10969  addclprlem2 10970  df-plp 10936
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10975
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10974
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10987
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10996  ltexprlem1 10989  ltexprlem2 10990  ltexprlem3 10991  ltexprlem4 10992  ltexprlem5 10993  ltexprlem6 10994  ltexprlem7 10995
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10998  ltaprlem 10997
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10999
[Gleason] p. 124Lemma 9-3.6prlem936 11000
[Gleason] p. 124Proposition 9-3.7df-mp 10937  mulclpr 10973  mulclprlem 10972  reclem2pr 11001
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10982
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10977
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10976
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10981
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11004  reclem3pr 11002  reclem4pr 11003
[Gleason] p. 126Proposition 9-4.1df-enr 11008  enrer 11016
[Gleason] p. 126Proposition 9-4.2df-0r 11013  df-1r 11014  df-nr 11009
[Gleason] p. 126Proposition 9-4.3df-mr 11011  df-plr 11010  negexsr 11055  recexsr 11060  recexsrlem 11056
[Gleason] p. 127Proposition 9-4.4df-ltr 11012
[Gleason] p. 130Proposition 10-1.3creui 12181  creur 12180  cru 12178
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11141  axcnre 11117
[Gleason] p. 132Definition 10-3.1crim 15081  crimd 15198  crimi 15159  crre 15080  crred 15197  crrei 15158
[Gleason] p. 132Definition 10-3.2remim 15083  remimd 15164
[Gleason] p. 133Definition 10.36absval2 15250  absval2d 15414  absval2i 15364
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15107  cjaddd 15186  cjaddi 15154
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15108  cjmuld 15187  cjmuli 15155
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15106  cjcjd 15165  cjcji 15137
[Gleason] p. 133Proposition 10-3.4(f)cjre 15105  cjreb 15089  cjrebd 15168  cjrebi 15140  cjred 15192  rere 15088  rereb 15086  rerebd 15167  rerebi 15139  rered 15190
[Gleason] p. 133Proposition 10-3.4(h)addcj 15114  addcjd 15178  addcji 15149
[Gleason] p. 133Proposition 10-3.7(a)absval 15204
[Gleason] p. 133Proposition 10-3.7(b)abscj 15245  abscjd 15419  abscji 15368
[Gleason] p. 133Proposition 10-3.7(c)abs00 15255  abs00d 15415  abs00i 15365  absne0d 15416
[Gleason] p. 133Proposition 10-3.7(d)releabs 15288  releabsd 15420  releabsi 15369
[Gleason] p. 133Proposition 10-3.7(f)absmul 15260  absmuld 15423  absmuli 15371
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15248  sqabsaddi 15372
[Gleason] p. 133Proposition 10-3.7(h)abstri 15297  abstrid 15425  abstrii 15375
[Gleason] p. 134Definition 10-4.1df-exp 14027  exp0 14030  expp1 14033  expp1d 14112
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26588  cxpaddd 26626  expadd 14069  expaddd 14113  expaddz 14071
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26597  cxpmuld 26646  expmul 14072  expmuld 14114  expmulz 14073
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26594  mulcxpd 26637  mulexp 14066  mulexpd 14126  mulexpz 14067
[Gleason] p. 140Exercise 1znnen 16180
[Gleason] p. 141Definition 11-2.1fzval 13470
[Gleason] p. 168Proposition 12-2.1(a)climadd 15598  rlimadd 15609  rlimdiv 15612
[Gleason] p. 168Proposition 12-2.1(b)climsub 15600  rlimsub 15610
[Gleason] p. 168Proposition 12-2.1(c)climmul 15599  rlimmul 15611
[Gleason] p. 171Corollary 12-2.2climmulc2 15603
[Gleason] p. 172Corollary 12-2.5climrecl 15549
[Gleason] p. 172Proposition 12-2.4(c)climabs 15570  climcj 15571  climim 15573  climre 15572  rlimabs 15575  rlimcj 15576  rlimim 15578  rlimre 15577
[Gleason] p. 173Definition 12-3.1df-ltxr 11213  df-xr 11212  ltxr 13075
[Gleason] p. 175Definition 12-4.1df-limsup 15437  limsupval 15440
[Gleason] p. 180Theorem 12-5.1climsup 15636
[Gleason] p. 180Theorem 12-5.3caucvg 15645  caucvgb 15646  caucvgbf 45485  caucvgr 15642  climcau 15637
[Gleason] p. 182Exercise 3cvgcmp 15782
[Gleason] p. 182Exercise 4cvgrat 15849
[Gleason] p. 195Theorem 13-2.12abs1m 15302
[Gleason] p. 217Lemma 13-4.1btwnzge0 13790
[Gleason] p. 223Definition 14-1.1df-met 21258
[Gleason] p. 223Definition 14-1.1(a)met0 24231  xmet0 24230
[Gleason] p. 223Definition 14-1.1(b)metgt0 24247
[Gleason] p. 223Definition 14-1.1(c)metsym 24238
[Gleason] p. 223Definition 14-1.1(d)mettri 24240  mstri 24357  xmettri 24239  xmstri 24356
[Gleason] p. 225Definition 14-1.5xpsmet 24270
[Gleason] p. 230Proposition 14-2.6txlm 23535
[Gleason] p. 240Theorem 14-4.3metcnp4 25210
[Gleason] p. 240Proposition 14-4.2metcnp3 24428
[Gleason] p. 243Proposition 14-4.16addcn 24754  addcn2 15560  mulcn 24756  mulcn2 15562  subcn 24755  subcn2 15561
[Gleason] p. 295Remarkbcval3 14271  bcval4 14272
[Gleason] p. 295Equation 2bcpasc 14286
[Gleason] p. 295Definition of binomial coefficientbcval 14269  df-bc 14268
[Gleason] p. 296Remarkbcn0 14275  bcnn 14277
[Gleason] p. 296Theorem 15-2.8binom 15796
[Gleason] p. 308Equation 2ef0 16057
[Gleason] p. 308Equation 3efcj 16058
[Gleason] p. 309Corollary 15-4.3efne0 16064
[Gleason] p. 309Corollary 15-4.4efexp 16069
[Gleason] p. 310Equation 14sinadd 16132
[Gleason] p. 310Equation 15cosadd 16133
[Gleason] p. 311Equation 17sincossq 16144
[Gleason] p. 311Equation 18cosbnd 16149  sinbnd 16148
[Gleason] p. 311Lemma 15-4.7sqeqor 14181  sqeqori 14179
[Gleason] p. 311Definition of ` `df-pi 16038
[Godowski] p. 730Equation SFgoeqi 32202
[GodowskiGreechie] p. 249Equation IV3oai 31597
[Golan] p. 1Remarksrgisid 20118
[Golan] p. 1Definitiondf-srg 20096
[Golan] p. 149Definitiondf-slmd 33154
[Gonshor] p. 7Definitiondf-scut 27695
[Gonshor] p. 9Theorem 2.5slerec 27731
[Gonshor] p. 10Theorem 2.6cofcut1 27828  cofcut1d 27829
[Gonshor] p. 10Theorem 2.7cofcut2 27830  cofcut2d 27831
[Gonshor] p. 12Theorem 2.9cofcutr 27832  cofcutr1d 27833  cofcutr2d 27834
[Gonshor] p. 13Definitiondf-adds 27867
[Gonshor] p. 14Theorem 3.1addsprop 27883
[Gonshor] p. 15Theorem 3.2addsunif 27909
[Gonshor] p. 17Theorem 3.4mulsprop 28033
[Gonshor] p. 18Theorem 3.5mulsunif 28053
[Gonshor] p. 28Lemma 4.2halfcut 28333
[Gonshor] p. 28Theorem 4.2pw2cut 28335
[Gonshor] p. 30Theorem 4.2addhalfcut 28334
[Gonshor] p. 95Theorem 6.1addsbday 27924
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36147
[Gratzer] p. 23Section 0.6df-mre 17547
[Gratzer] p. 27Section 0.6df-mri 17549
[Hall] p. 1Section 1.1df-asslaw 48176  df-cllaw 48174  df-comlaw 48175
[Hall] p. 2Section 1.2df-clintop 48188
[Hall] p. 7Section 1.3df-sgrp2 48209
[Halmos] p. 28Partition ` `df-parts 38757  dfmembpart2 38762
[Halmos] p. 31Theorem 17.3riesz1 31994  riesz2 31995
[Halmos] p. 41Definition of Hermitianhmopadj2 31870
[Halmos] p. 42Definition of projector orderingpjordi 32102
[Halmos] p. 43Theorem 26.1elpjhmop 32114  elpjidm 32113  pjnmopi 32077
[Halmos] p. 44Remarkpjinormi 31616  pjinormii 31605
[Halmos] p. 44Theorem 26.2elpjch 32118  pjrn 31636  pjrni 31631  pjvec 31625
[Halmos] p. 44Theorem 26.3pjnorm2 31656
[Halmos] p. 44Theorem 26.4hmopidmpj 32083  hmopidmpji 32081
[Halmos] p. 45Theorem 27.1pjinvari 32120
[Halmos] p. 45Theorem 27.3pjoci 32109  pjocvec 31626
[Halmos] p. 45Theorem 27.4pjorthcoi 32098
[Halmos] p. 48Theorem 29.2pjssposi 32101
[Halmos] p. 48Theorem 29.3pjssdif1i 32104  pjssdif2i 32103
[Halmos] p. 50Definition of spectrumdf-spec 31784
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1795
[Hatcher] p. 25Definitiondf-phtpc 24891  df-phtpy 24870
[Hatcher] p. 26Definitiondf-pco 24905  df-pi1 24908
[Hatcher] p. 26Proposition 1.2phtpcer 24894
[Hatcher] p. 26Proposition 1.3pi1grp 24950
[Hefferon] p. 240Definition 3.12df-dmat 22377  df-dmatalt 48387
[Helfgott] p. 2Theoremtgoldbach 47818
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 47803
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 47815  bgoldbtbnd 47810  bgoldbtbnd 47810  tgblthelfgott 47816
[Helfgott] p. 5Proposition 1.1circlevma 34633
[Helfgott] p. 69Statement 7.49circlemethhgt 34634
[Helfgott] p. 69Statement 7.50hgt750lema 34648  hgt750lemb 34647  hgt750leme 34649  hgt750lemf 34644  hgt750lemg 34645
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 47812  tgoldbachgt 34654  tgoldbachgtALTV 47813  tgoldbachgtd 34653
[Helfgott] p. 70Statement 7.49ax-hgt749 34635
[Herstein] p. 54Exercise 28df-grpo 30422
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18876  grpoideu 30438  mndideu 18672
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18906  grpoinveu 30448
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18937  grpo2inv 30460
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18950  grpoinvop 30462
[Herstein] p. 57Exercise 1dfgrp3e 18972
[Hitchcock] p. 5Rule A3mptnan 1768
[Hitchcock] p. 5Rule A4mptxor 1769
[Hitchcock] p. 5Rule A5mtpxor 1771
[Holland] p. 1519Theorem 2sumdmdi 32349
[Holland] p. 1520Lemma 5cdj1i 32362  cdj3i 32370  cdj3lem1 32363  cdjreui 32361
[Holland] p. 1524Lemma 7mddmdin0i 32360
[Holland95] p. 13Theorem 3.6hlathil 41955
[Holland95] p. 14Line 15hgmapvs 41885
[Holland95] p. 14Line 16hdmaplkr 41907
[Holland95] p. 14Line 17hdmapellkr 41908
[Holland95] p. 14Line 19hdmapglnm2 41905
[Holland95] p. 14Line 20hdmapip0com 41911
[Holland95] p. 14Theorem 3.6hdmapevec2 41830
[Holland95] p. 14Lines 24 and 25hdmapoc 41925
[Holland95] p. 204Definition of involutiondf-srng 20749
[Holland95] p. 212Definition of subspacedf-psubsp 39497
[Holland95] p. 214Lemma 3.3lclkrlem2v 41522
[Holland95] p. 214Definition 3.2df-lpolN 41475
[Holland95] p. 214Definition of nonsingularpnonsingN 39927
[Holland95] p. 215Lemma 3.3(1)dihoml4 41371  poml4N 39947
[Holland95] p. 215Lemma 3.3(2)dochexmid 41462  pexmidALTN 39972  pexmidN 39963
[Holland95] p. 218Theorem 3.6lclkr 41527
[Holland95] p. 218Definition of dual vector spacedf-ldual 39117  ldualset 39118
[Holland95] p. 222Item 1df-lines 39495  df-pointsN 39496
[Holland95] p. 222Item 2df-polarityN 39897
[Holland95] p. 223Remarkispsubcl2N 39941  omllaw4 39239  pol1N 39904  polcon3N 39911
[Holland95] p. 223Definitiondf-psubclN 39929
[Holland95] p. 223Equation for polaritypolval2N 39900
[Holmes] p. 40Definitiondf-xrn 38353
[Hughes] p. 44Equation 1.21bax-his3 31013
[Hughes] p. 47Definition of projection operatordfpjop 32111
[Hughes] p. 49Equation 1.30eighmre 31892  eigre 31764  eigrei 31763
[Hughes] p. 49Equation 1.31eighmorth 31893  eigorth 31767  eigorthi 31766
[Hughes] p. 137Remark (ii)eigposi 31765
[Huneke] p. 1Claim 1frgrncvvdeq 30238
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30234
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30235
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30236
[Huneke] p. 2Claim 2frgrregorufr 30254  frgrregorufr0 30253  frgrregorufrg 30255
[Huneke] p. 2Claim 3frgrhash2wsp 30261  frrusgrord 30270  frrusgrord0 30269
[Huneke] p. 2Statementdf-clwwlknon 30017
[Huneke] p. 2Statement 4frgrwopreglem4 30244
[Huneke] p. 2Statement 5frgrwopreg1 30247  frgrwopreg2 30248  frgrwopregasn 30245  frgrwopregbsn 30246
[Huneke] p. 2Statement 6frgrwopreglem5 30250
[Huneke] p. 2Statement 7fusgreghash2wspv 30264
[Huneke] p. 2Statement 8fusgreghash2wsp 30267
[Huneke] p. 2Statement 9clwlksndivn 30015  numclwlk1 30300  numclwlk1lem1 30298  numclwlk1lem2 30299  numclwwlk1 30290  numclwwlk8 30321
[Huneke] p. 2Definition 3frgrwopreglem1 30241
[Huneke] p. 2Definition 4df-clwlks 29701
[Huneke] p. 2Definition 62clwwlk 30276
[Huneke] p. 2Definition 7numclwwlkovh 30302  numclwwlkovh0 30301
[Huneke] p. 2Statement 10numclwwlk2 30310
[Huneke] p. 2Statement 11rusgrnumwlkg 29907
[Huneke] p. 2Statement 12numclwwlk3 30314
[Huneke] p. 2Statement 13numclwwlk5 30317
[Huneke] p. 2Statement 14numclwwlk7 30320
[Indrzejczak] p. 33Definition ` `Enatded 30332  natded 30332
[Indrzejczak] p. 33Definition ` `Inatded 30332
[Indrzejczak] p. 34Definition ` `Enatded 30332  natded 30332
[Indrzejczak] p. 34Definition ` `Inatded 30332
[Jech] p. 4Definition of classcv 1539  cvjust 2723
[Jech] p. 42Lemma 6.1alephexp1 10532
[Jech] p. 42Equation 6.1alephadd 10530  alephmul 10531
[Jech] p. 43Lemma 6.2infmap 10529  infmap2 10170
[Jech] p. 71Lemma 9.3jech9.3 9767
[Jech] p. 72Equation 9.3scott0 9839  scottex 9838
[Jech] p. 72Exercise 9.1rankval4 9820
[Jech] p. 72Scheme "Collection Principle"cp 9844
[Jech] p. 78Noteopthprc 5702
[JonesMatijasevic] p. 694Definition 2.3rmxyval 42904
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 42992
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 42993
[JonesMatijasevic] p. 695Equation 2.7rmxadd 42916
[JonesMatijasevic] p. 695Equation 2.8rmyadd 42920
[JonesMatijasevic] p. 695Equation 2.9rmxp1 42921  rmyp1 42922
[JonesMatijasevic] p. 695Equation 2.10rmxm1 42923  rmym1 42924
[JonesMatijasevic] p. 695Equation 2.11rmx0 42914  rmx1 42915  rmxluc 42925
[JonesMatijasevic] p. 695Equation 2.12rmy0 42918  rmy1 42919  rmyluc 42926
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 42928
[JonesMatijasevic] p. 695Equation 2.14rmydbl 42929
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42949  jm2.17b 42950  jm2.17c 42951
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 42982
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 42986
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 42977
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42952  jm2.24nn 42948
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 42991
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 42997  rmygeid 42953
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43009
[Juillerat] p. 11Section *5etransc 46281  etransclem47 46279  etransclem48 46280
[Juillerat] p. 12Equation (7)etransclem44 46276
[Juillerat] p. 12Equation *(7)etransclem46 46278
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46264
[Juillerat] p. 13Proofetransclem35 46267
[Juillerat] p. 13Part of case 2 proven inetransclem38 46270
[Juillerat] p. 13Part of case 2 provenetransclem24 46256
[Juillerat] p. 13Part of case 2: proven inetransclem41 46273
[Juillerat] p. 14Proofetransclem23 46255
[KalishMontague] p. 81Note 1ax-6 1967
[KalishMontague] p. 85Lemma 2equid 2012
[KalishMontague] p. 85Lemma 3equcomi 2017
[KalishMontague] p. 86Lemma 7cbvalivw 2007  cbvaliw 2006  wl-cbvmotv 37501  wl-motae 37503  wl-moteq 37502
[KalishMontague] p. 87Lemma 8spimvw 1986  spimw 1970
[KalishMontague] p. 87Lemma 9spfw 2033  spw 2034
[Kalmbach] p. 14Definition of latticechabs1 31445  chabs1i 31447  chabs2 31446  chabs2i 31448  chjass 31462  chjassi 31415  latabs1 18434  latabs2 18435
[Kalmbach] p. 15Definition of atomdf-at 32267  ela 32268
[Kalmbach] p. 15Definition of coverscvbr2 32212  cvrval2 39267
[Kalmbach] p. 16Definitiondf-ol 39171  df-oml 39172
[Kalmbach] p. 20Definition of commutescmbr 31513  cmbri 31519  cmtvalN 39204  df-cm 31512  df-cmtN 39170
[Kalmbach] p. 22Remarkomllaw5N 39240  pjoml5 31542  pjoml5i 31517
[Kalmbach] p. 22Definitionpjoml2 31540  pjoml2i 31514
[Kalmbach] p. 22Theorem 2(v)cmcm 31543  cmcmi 31521  cmcmii 31526  cmtcomN 39242
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39238  omlsi 31333  pjoml 31365  pjomli 31364
[Kalmbach] p. 22Definition of OML lawomllaw2N 39237
[Kalmbach] p. 23Remarkcmbr2i 31525  cmcm3 31544  cmcm3i 31523  cmcm3ii 31528  cmcm4i 31524  cmt3N 39244  cmt4N 39245  cmtbr2N 39246
[Kalmbach] p. 23Lemma 3cmbr3 31537  cmbr3i 31529  cmtbr3N 39247
[Kalmbach] p. 25Theorem 5fh1 31547  fh1i 31550  fh2 31548  fh2i 31551  omlfh1N 39251
[Kalmbach] p. 65Remarkchjatom 32286  chslej 31427  chsleji 31387  shslej 31309  shsleji 31299
[Kalmbach] p. 65Proposition 1chocin 31424  chocini 31383  chsupcl 31269  chsupval2 31339  h0elch 31184  helch 31172  hsupval2 31338  ocin 31225  ococss 31222  shococss 31223
[Kalmbach] p. 65Definition of subspace sumshsval 31241
[Kalmbach] p. 66Remarkdf-pjh 31324  pjssmi 32094  pjssmii 31610
[Kalmbach] p. 67Lemma 3osum 31574  osumi 31571
[Kalmbach] p. 67Lemma 4pjci 32129
[Kalmbach] p. 103Exercise 6atmd2 32329
[Kalmbach] p. 103Exercise 12mdsl0 32239
[Kalmbach] p. 140Remarkhatomic 32289  hatomici 32288  hatomistici 32291
[Kalmbach] p. 140Proposition 1atlatmstc 39312
[Kalmbach] p. 140Proposition 1(i)atexch 32310  lsatexch 39036
[Kalmbach] p. 140Proposition 1(ii)chcv1 32284  cvlcvr1 39332  cvr1 39404
[Kalmbach] p. 140Proposition 1(iii)cvexch 32303  cvexchi 32298  cvrexch 39414
[Kalmbach] p. 149Remark 2chrelati 32293  hlrelat 39396  hlrelat5N 39395  lrelat 39007
[Kalmbach] p. 153Exercise 5lsmcv 21051  lsmsatcv 39003  spansncv 31582  spansncvi 31581
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39022  spansncv2 32222
[Kalmbach] p. 266Definitiondf-st 32140
[Kalmbach2] p. 8Definition of adjointdf-adjh 31778
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10599  fpwwe2 10596
[KanamoriPincus] p. 416Corollary 1.3canth4 10600
[KanamoriPincus] p. 417Corollary 1.6canthp1 10607
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10602
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10604
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10617
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10621  gchxpidm 10622
[KanamoriPincus] p. 419Theorem 2.1gchacg 10633  gchhar 10632
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10168  unxpwdom 9542
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10623
[Kreyszig] p. 3Property M1metcl 24220  xmetcl 24219
[Kreyszig] p. 4Property M2meteq0 24227
[Kreyszig] p. 8Definition 1.1-8dscmet 24460
[Kreyszig] p. 12Equation 5conjmul 11899  muleqadd 11822
[Kreyszig] p. 18Definition 1.3-2mopnval 24326
[Kreyszig] p. 19Remarkmopntopon 24327
[Kreyszig] p. 19Theorem T1mopn0 24386  mopnm 24332
[Kreyszig] p. 19Theorem T2unimopn 24384
[Kreyszig] p. 19Definition of neighborhoodneibl 24389
[Kreyszig] p. 20Definition 1.3-3metcnp2 24430
[Kreyszig] p. 25Definition 1.4-1lmbr 23145  lmmbr 25158  lmmbr2 25159
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23267
[Kreyszig] p. 28Theorem 1.4-5lmcau 25213
[Kreyszig] p. 28Definition 1.4-3iscau 25176  iscmet2 25194
[Kreyszig] p. 30Theorem 1.4-7cmetss 25216
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23348  metelcls 25205
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25206  metcld2 25207
[Kreyszig] p. 51Equation 2clmvneg1 24999  lmodvneg1 20811  nvinv 30568  vcm 30505
[Kreyszig] p. 51Equation 1aclm0vs 24995  lmod0vs 20801  slmd0vs 33177  vc0 30503
[Kreyszig] p. 51Equation 1blmodvs0 20802  slmdvs0 33178  vcz 30504
[Kreyszig] p. 58Definition 2.2-1imsmet 30620  ngpmet 24491  nrmmetd 24462
[Kreyszig] p. 59Equation 1imsdval 30615  imsdval2 30616  ncvspds 25061  ngpds 24492
[Kreyszig] p. 63Problem 1nmval 24477  nvnd 30617
[Kreyszig] p. 64Problem 2nmeq0 24506  nmge0 24505  nvge0 30602  nvz 30598
[Kreyszig] p. 64Problem 3nmrtri 24512  nvabs 30601
[Kreyszig] p. 91Definition 2.7-1isblo3i 30730
[Kreyszig] p. 92Equation 2df-nmoo 30674
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30736  blocni 30734
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30735
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25104  ipeq0 21547  ipz 30648
[Kreyszig] p. 135Problem 2cphpyth 25116  pythi 30779
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30783
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25138
[Kreyszig] p. 144Equation 4supcvg 15822
[Kreyszig] p. 144Theorem 3.3-1minvec 25336  minveco 30813
[Kreyszig] p. 196Definition 3.9-1df-aj 30679
[Kreyszig] p. 247Theorem 4.7-2bcth 25229
[Kreyszig] p. 249Theorem 4.7-3ubth 30802
[Kreyszig] p. 470Definition of positive operator orderingleop 32052  leopg 32051
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32070
[Kreyszig] p. 525Theorem 10.1-1htth 30847
[Kulpa] p. 547Theorempoimir 37647
[Kulpa] p. 547Equation (1)poimirlem32 37646
[Kulpa] p. 547Equation (2)poimirlem31 37645
[Kulpa] p. 548Theorembroucube 37648
[Kulpa] p. 548Equation (6)poimirlem26 37640
[Kulpa] p. 548Equation (7)poimirlem27 37641
[Kunen] p. 10Axiom 0ax6e 2381  axnul 5260
[Kunen] p. 11Axiom 3axnul 5260
[Kunen] p. 12Axiom 6zfrep6 7933
[Kunen] p. 24Definition 10.24mapval 8811  mapvalg 8809
[Kunen] p. 30Lemma 10.20fodomg 10475
[Kunen] p. 31Definition 10.24mapex 7917
[Kunen] p. 95Definition 2.1df-r1 9717
[Kunen] p. 97Lemma 2.10r1elss 9759  r1elssi 9758
[Kunen] p. 107Exercise 4rankop 9811  rankopb 9805  rankuni 9816  rankxplim 9832  rankxpsuc 9835
[Kunen2] p. 47Lemma I.9.9relpfr 44944
[Kunen2] p. 53Lemma I.9.21trfr 44952
[Kunen2] p. 53Lemma I.9.24(2)wffr 44951
[Kunen2] p. 53Definition I.9.20tcfr 44953
[Kunen2] p. 95Lemma I.16.2ralabso 44958  rexabso 44959
[Kunen2] p. 96Example I.16.3disjabso 44965  n0abso 44966  ssabso 44964
[Kunen2] p. 111Lemma II.2.4(1)traxext 44967
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 44977
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 44972
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 44975
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 44976
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 44971
[Kunen2] p. 112Corollary II.2.5wfaxext 44983  wfaxpr 44988  wfaxreg 44990  wfaxrep 44984  wfaxsep 44985  wfaxun 44989
[Kunen2] p. 113Lemma II.2.8pwclaxpow 44974
[Kunen2] p. 113Corollary II.2.9wfaxpow 44987
[Kunen2] p. 114Theorem II.2.13wfaxext 44983
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 44982  omelaxinf2 44979
[Kunen2] p. 114Corollary II.2.12wfac8prim 44992  wfaxinf2 44991
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45005  permaxext 44995  permaxinf2 45003  permaxnul 44998  permaxpow 44999  permaxpr 45000  permaxrep 44996  permaxsep 44997  permaxun 45001
[Kunen2] p. 148Definition II.9.1brpermmodel 44993
[Kunen2] p. 149Exercise II.9.3permac8prim 45004
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4968
[Lang] , p. 225Corollary 1.3finexttrb 33660
[Lang] p. Definitiondf-rn 5649
[Lang] p. 3Statementlidrideqd 18596  mndbn0 18677
[Lang] p. 3Definitiondf-mnd 18662
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18614
[Lang] p. 4Property of composites. Second formulagsumccat 18768
[Lang] p. 5Equationgsumreidx 19847
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48170
[Lang] p. 6Examplenn0mnd 48167
[Lang] p. 6Equationgsumxp2 19910
[Lang] p. 6Statementcycsubm 19134
[Lang] p. 6Definitionmulgnn0gsum 19012
[Lang] p. 6Observationmndlsmidm 19600
[Lang] p. 7Definitiondfgrp2e 18895
[Lang] p. 30Definitiondf-tocyc 33064
[Lang] p. 32Property (a)cyc3genpm 33109
[Lang] p. 32Property (b)cyc3conja 33114  cycpmconjv 33099
[Lang] p. 53Definitiondf-cat 17629
[Lang] p. 53Axiom CAT 1cat1 18059  cat1lem 18058
[Lang] p. 54Definitiondf-iso 17711
[Lang] p. 57Definitiondf-inito 17946  df-termo 17947
[Lang] p. 58Exampleirinitoringc 21389
[Lang] p. 58Statementinitoeu1 17973  termoeu1 17980
[Lang] p. 62Definitiondf-func 17820
[Lang] p. 65Definitiondf-nat 17908
[Lang] p. 91Notedf-ringc 20555
[Lang] p. 92Statementmxidlprm 33441
[Lang] p. 92Definitionisprmidlc 33418
[Lang] p. 128Remarkdsmmlmod 21654
[Lang] p. 129Prooflincscm 48419  lincscmcl 48421  lincsum 48418  lincsumcl 48420
[Lang] p. 129Statementlincolss 48423
[Lang] p. 129Observationdsmmfi 21647
[Lang] p. 141Theorem 5.3dimkerim 33623  qusdimsum 33624
[Lang] p. 141Corollary 5.4lssdimle 33603
[Lang] p. 147Definitionsnlindsntor 48460
[Lang] p. 504Statementmat1 22334  matring 22330
[Lang] p. 504Definitiondf-mamu 22278
[Lang] p. 505Statementmamuass 22289  mamutpos 22345  matassa 22331  mattposvs 22342  tposmap 22344
[Lang] p. 513Definitionmdet1 22488  mdetf 22482
[Lang] p. 513Theorem 4.4cramer 22578
[Lang] p. 514Proposition 4.6mdetleib 22474
[Lang] p. 514Proposition 4.8mdettpos 22498
[Lang] p. 515Definitiondf-minmar1 22522  smadiadetr 22562
[Lang] p. 515Corollary 4.9mdetero 22497  mdetralt 22495
[Lang] p. 517Proposition 4.15mdetmul 22510
[Lang] p. 518Definitiondf-madu 22521
[Lang] p. 518Proposition 4.16madulid 22532  madurid 22531  matinv 22564
[Lang] p. 561Theorem 3.1cayleyhamilton 22777
[Lang], p. 224Proposition 1.2extdgmul 33659  fedgmul 33627
[Lang], p. 561Remarkchpmatply1 22719
[Lang], p. 561Definitiondf-chpmat 22714
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44323
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44318
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44324
[LeBlanc] p. 277Rule R2axnul 5260
[Levy] p. 12Axiom 4.3.1df-clab 2708
[Levy] p. 59Definitiondf-ttrcl 9661
[Levy] p. 64Theorem 5.6(ii)frinsg 9704
[Levy] p. 338Axiomdf-clel 2803  df-cleq 2721
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2803  df-cleq 2721
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2708
[Levy] p. 358Axiomdf-clab 2708
[Levy58] p. 2Definition Iisfin1-3 10339
[Levy58] p. 2Definition IIdf-fin2 10239
[Levy58] p. 2Definition Iadf-fin1a 10238
[Levy58] p. 2Definition IIIdf-fin3 10241
[Levy58] p. 3Definition Vdf-fin5 10242
[Levy58] p. 3Definition IVdf-fin4 10240
[Levy58] p. 4Definition VIdf-fin6 10243
[Levy58] p. 4Definition VIIdf-fin7 10244
[Levy58], p. 3Theorem 1fin1a2 10368
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27598
[Lipparini] p. 3Lemma 2.1.4noresle 27609
[Lipparini] p. 6Proposition 4.2noinfbnd1 27641  nosupbnd1 27626
[Lipparini] p. 6Proposition 4.3noinfbnd2 27643  nosupbnd2 27628
[Lipparini] p. 7Theorem 5.1noetasuplem3 27647  noetasuplem4 27648
[Lipparini] p. 7Corollary 4.4nosupinfsep 27644
[Lopez-Astorga] p. 12Rule 1mptnan 1768
[Lopez-Astorga] p. 12Rule 2mptxor 1769
[Lopez-Astorga] p. 12Rule 3mtpxor 1771
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32337
[Maeda] p. 168Lemma 5mdsym 32341  mdsymi 32340
[Maeda] p. 168Lemma 4(i)mdsymlem4 32335  mdsymlem6 32337  mdsymlem7 32338
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32339
[MaedaMaeda] p. 1Remarkssdmd1 32242  ssdmd2 32243  ssmd1 32240  ssmd2 32241
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32238
[MaedaMaeda] p. 1Definition 1.1df-dmd 32210  df-md 32209  mdbr 32223
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32260  mdslj1i 32248  mdslj2i 32249  mdslle1i 32246  mdslle2i 32247  mdslmd1i 32258  mdslmd2i 32259
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32250  mdsl2bi 32252  mdsl2i 32251
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32264
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32261
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32262
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32239
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32244  mdsl3 32245
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32263
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32358
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39314  hlrelat1 39394
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39032
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32265  cvmdi 32253  cvnbtwn4 32218  cvrnbtwn4 39272
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32266
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39333  cvp 32304  cvrp 39410  lcvp 39033
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32328
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32327
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39326  hlexch4N 39386
[MaedaMaeda] p. 34Exercise 7.1atabsi 32330
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39437
[MaedaMaeda] p. 61Definition 15.10psubN 39743  atpsubN 39747  df-pointsN 39496  pointpsubN 39745
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39498  pmap11 39756  pmaple 39755  pmapsub 39762  pmapval 39751
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 39759  pmap1N 39761
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 39764  pmapglb2N 39765  pmapglb2xN 39766  pmapglbx 39763
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39846
[MaedaMaeda] p. 67Postulate PS1ps-1 39471
[MaedaMaeda] p. 68Lemma 16.2df-padd 39790  paddclN 39836  paddidm 39835
[MaedaMaeda] p. 68Condition PS2ps-2 39472
[MaedaMaeda] p. 68Equation 16.2.1paddass 39832
[MaedaMaeda] p. 69Lemma 16.4ps-1 39471
[MaedaMaeda] p. 69Theorem 16.4ps-2 39472
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19605  lsmmod2 19606  lssats 39005  shatomici 32287  shatomistici 32290  shmodi 31319  shmodsi 31318
[MaedaMaeda] p. 130Remark 29.6dmdmd 32229  mdsymlem7 32338
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31518
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31422
[MaedaMaeda] p. 139Remarksumdmdii 32344
[Margaris] p. 40Rule Cexlimiv 1930
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 396  df-ex 1780  df-or 848  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30329
[Margaris] p. 59Section 14notnotrALTVD 44904
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 44905
[Margaris] p. 79Rule Cexinst01 44615  exinst11 44616
[Margaris] p. 89Theorem 19.219.2 1976  19.2g 2189  r19.2z 4458
[Margaris] p. 89Theorem 19.319.3 2203  rr19.3v 3633
[Margaris] p. 89Theorem 19.5alcom 2160
[Margaris] p. 89Theorem 19.6alex 1826
[Margaris] p. 89Theorem 19.7alnex 1781
[Margaris] p. 89Theorem 19.819.8a 2182
[Margaris] p. 89Theorem 19.919.9 2206  19.9h 2286  exlimd 2219  exlimdh 2290
[Margaris] p. 89Theorem 19.11excom 2163  excomim 2164
[Margaris] p. 89Theorem 19.1219.12 2326
[Margaris] p. 90Section 19conventions-labels 30330  conventions-labels 30330  conventions-labels 30330  conventions-labels 30330
[Margaris] p. 90Theorem 19.14exnal 1827
[Margaris] p. 90Theorem 19.152albi 44367  albi 1818
[Margaris] p. 90Theorem 19.1619.16 2226
[Margaris] p. 90Theorem 19.1719.17 2227
[Margaris] p. 90Theorem 19.182exbi 44369  exbi 1847
[Margaris] p. 90Theorem 19.1919.19 2230
[Margaris] p. 90Theorem 19.202alim 44366  2alimdv 1918  alimd 2213  alimdh 1817  alimdv 1916  ax-4 1809  ralimdaa 3238  ralimdv 3147  ralimdva 3145  ralimdvva 3184  sbcimdv 3822
[Margaris] p. 90Theorem 19.2119.21 2208  19.21h 2287  19.21t 2207  19.21vv 44365  alrimd 2216  alrimdd 2215  alrimdh 1863  alrimdv 1929  alrimi 2214  alrimih 1824  alrimiv 1927  alrimivv 1928  hbralrimi 3123  r19.21be 3230  r19.21bi 3229  ralrimd 3242  ralrimdv 3131  ralrimdva 3133  ralrimdvv 3181  ralrimdvva 3192  ralrimi 3235  ralrimia 3236  ralrimiv 3124  ralrimiva 3125  ralrimivv 3178  ralrimivva 3180  ralrimivvva 3183  ralrimivw 3129
[Margaris] p. 90Theorem 19.222exim 44368  2eximdv 1919  exim 1834  eximd 2217  eximdh 1864  eximdv 1917  rexim 3070  reximd2a 3247  reximdai 3239  reximdd 45142  reximddv 3149  reximddv2 3196  reximddv3 3150  reximdv 3148  reximdv2 3143  reximdva 3146  reximdvai 3144  reximdvva 3185  reximi2 3062
[Margaris] p. 90Theorem 19.2319.23 2212  19.23bi 2192  19.23h 2288  19.23t 2211  exlimdv 1933  exlimdvv 1934  exlimexi 44514  exlimiv 1930  exlimivv 1932  rexlimd3 45138  rexlimdv 3132  rexlimdv3a 3138  rexlimdva 3134  rexlimdva2 3136  rexlimdvaa 3135  rexlimdvv 3193  rexlimdvva 3194  rexlimdvvva 3195  rexlimdvw 3139  rexlimiv 3127  rexlimiva 3126  rexlimivv 3179
[Margaris] p. 90Theorem 19.2419.24 1991
[Margaris] p. 90Theorem 19.2519.25 1880
[Margaris] p. 90Theorem 19.2619.26 1870
[Margaris] p. 90Theorem 19.2719.27 2228  r19.27z 4468  r19.27zv 4469
[Margaris] p. 90Theorem 19.2819.28 2229  19.28vv 44375  r19.28z 4461  r19.28zf 45153  r19.28zv 4464  rr19.28v 3634
[Margaris] p. 90Theorem 19.2919.29 1873  r19.29d2r 3120  r19.29imd 3098
[Margaris] p. 90Theorem 19.3019.30 1881
[Margaris] p. 90Theorem 19.3119.31 2235  19.31vv 44373
[Margaris] p. 90Theorem 19.3219.32 2234  r19.32 47099
[Margaris] p. 90Theorem 19.3319.33-2 44371  19.33 1884
[Margaris] p. 90Theorem 19.3419.34 1992
[Margaris] p. 90Theorem 19.3519.35 1877
[Margaris] p. 90Theorem 19.3619.36 2231  19.36vv 44372  r19.36zv 4470
[Margaris] p. 90Theorem 19.3719.37 2233  19.37vv 44374  r19.37zv 4465
[Margaris] p. 90Theorem 19.3819.38 1839
[Margaris] p. 90Theorem 19.3919.39 1990
[Margaris] p. 90Theorem 19.4019.40-2 1887  19.40 1886  r19.40 3099
[Margaris] p. 90Theorem 19.4119.41 2236  19.41rg 44540
[Margaris] p. 90Theorem 19.4219.42 2237
[Margaris] p. 90Theorem 19.4319.43 1882
[Margaris] p. 90Theorem 19.4419.44 2238  r19.44zv 4467
[Margaris] p. 90Theorem 19.4519.45 2239  r19.45zv 4466
[Margaris] p. 110Exercise 2(b)eu1 2603
[Mayet] p. 370Remarkjpi 32199  largei 32196  stri 32186
[Mayet3] p. 9Definition of CH-statesdf-hst 32141  ishst 32143
[Mayet3] p. 10Theoremhstrbi 32195  hstri 32194
[Mayet3] p. 1223Theorem 4.1mayete3i 31657
[Mayet3] p. 1240Theorem 7.1mayetes3i 31658
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32207
[MegPav2000] p. 2345Definition 3.4-1chintcl 31261  chsupcl 31269
[MegPav2000] p. 2345Definition 3.4-2hatomic 32289
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32283
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32310
[MegPav2000] p. 2366Figure 7pl42N 39977
[MegPav2002] p. 362Lemma 2.2latj31 18446  latj32 18444  latjass 18442
[Megill] p. 444Axiom C5ax-5 1910  ax5ALT 38900
[Megill] p. 444Section 7conventions 30329
[Megill] p. 445Lemma L12aecom-o 38894  ax-c11n 38881  axc11n 2424
[Megill] p. 446Lemma L17equtrr 2022
[Megill] p. 446Lemma L18ax6fromc10 38889
[Megill] p. 446Lemma L19hbnae-o 38921  hbnae 2430
[Megill] p. 447Remark 9.1dfsb1 2479  sbid 2256  sbidd-misc 49708  sbidd 49707
[Megill] p. 448Remark 9.6axc14 2461
[Megill] p. 448Scheme C4'ax-c4 38877
[Megill] p. 448Scheme C5'ax-c5 38876  sp 2184
[Megill] p. 448Scheme C6'ax-11 2158
[Megill] p. 448Scheme C7'ax-c7 38878
[Megill] p. 448Scheme C8'ax-7 2008
[Megill] p. 448Scheme C9'ax-c9 38883
[Megill] p. 448Scheme C10'ax-6 1967  ax-c10 38879
[Megill] p. 448Scheme C11'ax-c11 38880
[Megill] p. 448Scheme C12'ax-8 2111
[Megill] p. 448Scheme C13'ax-9 2119
[Megill] p. 448Scheme C14'ax-c14 38884
[Megill] p. 448Scheme C15'ax-c15 38882
[Megill] p. 448Scheme C16'ax-c16 38885
[Megill] p. 448Theorem 9.4dral1-o 38897  dral1 2437  dral2-o 38923  dral2 2436  drex1 2439  drex2 2440  drsb1 2493  drsb2 2267
[Megill] p. 449Theorem 9.7sbcom2 2174  sbequ 2084  sbid2v 2507
[Megill] p. 450Example in Appendixhba1-o 38890  hba1 2293
[Mendelson] p. 35Axiom A3hirstL-ax3 46893
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3842  rspsbca 3843  stdpc4 2069
[Mendelson] p. 69Axiom 5ax-c4 38877  ra4 3849  stdpc5 2209
[Mendelson] p. 81Rule Cexlimiv 1930
[Mendelson] p. 95Axiom 6stdpc6 2028
[Mendelson] p. 95Axiom 7stdpc7 2251
[Mendelson] p. 225Axiom system NBGru 3751
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5474
[Mendelson] p. 231Exercise 4.10(k)inv1 4361
[Mendelson] p. 231Exercise 4.10(l)unv 4362
[Mendelson] p. 231Exercise 4.10(n)dfin3 4240
[Mendelson] p. 231Exercise 4.10(o)df-nul 4297
[Mendelson] p. 231Exercise 4.10(q)dfin4 4241
[Mendelson] p. 231Exercise 4.10(s)ddif 4104
[Mendelson] p. 231Definition of uniondfun3 4239
[Mendelson] p. 235Exercise 4.12(c)univ 5411
[Mendelson] p. 235Exercise 4.12(d)pwv 4868
[Mendelson] p. 235Exercise 4.12(j)pwin 5529
[Mendelson] p. 235Exercise 4.12(k)pwunss 4581
[Mendelson] p. 235Exercise 4.12(l)pwssun 5530
[Mendelson] p. 235Exercise 4.12(n)uniin 4895
[Mendelson] p. 235Exercise 4.12(p)reli 5789
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6241
[Mendelson] p. 244Proposition 4.8(g)epweon 7751
[Mendelson] p. 246Definition of successordf-suc 6338
[Mendelson] p. 250Exercise 4.36oelim2 8559
[Mendelson] p. 254Proposition 4.22(b)xpen 9104
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9025  xpsneng 9026
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9032  xpcomeng 9033
[Mendelson] p. 254Proposition 4.22(e)xpassen 9035
[Mendelson] p. 255Definitionbrsdom 8946
[Mendelson] p. 255Exercise 4.39endisj 9028
[Mendelson] p. 255Exercise 4.41mapprc 8803
[Mendelson] p. 255Exercise 4.43mapsnen 9008  mapsnend 9007
[Mendelson] p. 255Exercise 4.45mapunen 9110
[Mendelson] p. 255Exercise 4.47xpmapen 9109
[Mendelson] p. 255Exercise 4.42(a)map0e 8855
[Mendelson] p. 255Exercise 4.42(b)map1 9011
[Mendelson] p. 257Proposition 4.24(a)undom 9029
[Mendelson] p. 258Exercise 4.56(c)djuassen 10132  djucomen 10131
[Mendelson] p. 258Exercise 4.56(f)djudom1 10136
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10130
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8495
[Mendelson] p. 266Proposition 4.34(f)oaordex 8522
[Mendelson] p. 275Proposition 4.42(d)entri3 10512
[Mendelson] p. 281Definitiondf-r1 9717
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9766
[Mendelson] p. 287Axiom system MKru 3751
[MertziosUnger] p. 152Definitiondf-frgr 30188
[MertziosUnger] p. 153Remark 1frgrconngr 30223
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30225  vdgn1frgrv3 30226
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30227
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30220
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30213  2pthfrgrrn 30211  2pthfrgrrn2 30212
[Mittelstaedt] p. 9Definitiondf-oc 31181
[Monk1] p. 22Remarkconventions 30329
[Monk1] p. 22Theorem 3.1conventions 30329
[Monk1] p. 26Theorem 2.8(vii)ssin 4202
[Monk1] p. 33Theorem 3.2(i)ssrel 5745  ssrelf 32543
[Monk1] p. 33Theorem 3.2(ii)eqrel 5747
[Monk1] p. 34Definition 3.3df-opab 5170
[Monk1] p. 36Theorem 3.7(i)coi1 6235  coi2 6236
[Monk1] p. 36Theorem 3.8(v)dm0 5884  rn0 5889
[Monk1] p. 36Theorem 3.7(ii)cnvi 6114
[Monk1] p. 37Theorem 3.13(i)relxp 5656
[Monk1] p. 37Theorem 3.13(x)dmxp 5892  rnxp 6143
[Monk1] p. 37Theorem 3.13(ii)0xp 5737  xp0 6131
[Monk1] p. 38Theorem 3.16(ii)ima0 6048
[Monk1] p. 38Theorem 3.16(viii)imai 6045
[Monk1] p. 39Theorem 3.17imaex 7890  imaexg 7889
[Monk1] p. 39Theorem 3.16(xi)imassrn 6042
[Monk1] p. 41Theorem 4.3(i)fnopfv 7047  funfvop 7022
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6915
[Monk1] p. 42Theorem 4.4(iii)fvelima 6926
[Monk1] p. 43Theorem 4.6funun 6562
[Monk1] p. 43Theorem 4.8(iv)dff13 7229  dff13f 7230
[Monk1] p. 46Theorem 4.15(v)funex 7193  funrnex 7932
[Monk1] p. 50Definition 5.4fniunfv 7221
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6200
[Monk1] p. 52Theorem 5.11(viii)ssint 4928
[Monk1] p. 52Definition 5.13 (i)1stval2 7985  df-1st 7968
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7986  df-2nd 7969
[Monk1] p. 112Theorem 15.17(v)ranksn 9807  ranksnb 9780
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9808
[Monk1] p. 112Theorem 15.17(iii)rankun 9809  rankunb 9803
[Monk1] p. 113Theorem 15.18r1val3 9791
[Monk1] p. 113Definition 15.19df-r1 9717  r1val2 9790
[Monk1] p. 117Lemmazorn2 10459  zorn2g 10456
[Monk1] p. 133Theorem 18.11cardom 9939
[Monk1] p. 133Theorem 18.12canth3 10514
[Monk1] p. 133Theorem 18.14carduni 9934
[Monk2] p. 105Axiom C4ax-4 1809
[Monk2] p. 105Axiom C7ax-7 2008
[Monk2] p. 105Axiom C8ax-12 2178  ax-c15 38882  ax12v2 2180
[Monk2] p. 108Lemma 5ax-c4 38877
[Monk2] p. 109Lemma 12ax-11 2158
[Monk2] p. 109Lemma 15equvini 2453  equvinv 2029  eqvinop 5447
[Monk2] p. 113Axiom C5-1ax-5 1910  ax5ALT 38900
[Monk2] p. 113Axiom C5-2ax-10 2142
[Monk2] p. 113Axiom C5-3ax-11 2158
[Monk2] p. 114Lemma 21sp 2184
[Monk2] p. 114Lemma 22axc4 2320  hba1-o 38890  hba1 2293
[Monk2] p. 114Lemma 23nfia1 2154
[Monk2] p. 114Lemma 24nfa2 2177  nfra2 3350  nfra2w 3274
[Moore] p. 53Part Idf-mre 17547
[Munkres] p. 77Example 2distop 22882  indistop 22889  indistopon 22888
[Munkres] p. 77Example 3fctop 22891  fctop2 22892
[Munkres] p. 77Example 4cctop 22893
[Munkres] p. 78Definition of basisdf-bases 22833  isbasis3g 22836
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17406  tgval2 22843
[Munkres] p. 79Remarktgcl 22856
[Munkres] p. 80Lemma 2.1tgval3 22850
[Munkres] p. 80Lemma 2.2tgss2 22874  tgss3 22873
[Munkres] p. 81Lemma 2.3basgen 22875  basgen2 22876
[Munkres] p. 83Exercise 3topdifinf 37337  topdifinfeq 37338  topdifinffin 37336  topdifinfindis 37334
[Munkres] p. 89Definition of subspace topologyresttop 23047
[Munkres] p. 93Theorem 6.1(1)0cld 22925  topcld 22922
[Munkres] p. 93Theorem 6.1(2)iincld 22926
[Munkres] p. 93Theorem 6.1(3)uncld 22928
[Munkres] p. 94Definition of closureclsval 22924
[Munkres] p. 94Definition of interiorntrval 22923
[Munkres] p. 95Theorem 6.5(a)clsndisj 22962  elcls 22960
[Munkres] p. 95Theorem 6.5(b)elcls3 22970
[Munkres] p. 97Theorem 6.6clslp 23035  neindisj 23004
[Munkres] p. 97Corollary 6.7cldlp 23037
[Munkres] p. 97Definition of limit pointislp2 23032  lpval 23026
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23202
[Munkres] p. 102Definition of continuous functiondf-cn 23114  iscn 23122  iscn2 23125
[Munkres] p. 107Theorem 7.2(g)cncnp 23167  cncnp2 23168  cncnpi 23165  df-cnp 23115  iscnp 23124  iscnp2 23126
[Munkres] p. 127Theorem 10.1metcn 24431
[Munkres] p. 128Theorem 10.3metcn4 25211
[Nathanson] p. 123Remarkreprgt 34612  reprinfz1 34613  reprlt 34610
[Nathanson] p. 123Definitiondf-repr 34600
[Nathanson] p. 123Chapter 5.1circlemethnat 34632
[Nathanson] p. 123Propositionbreprexp 34624  breprexpnat 34625  itgexpif 34597
[NielsenChuang] p. 195Equation 4.73unierri 32033
[OeSilva] p. 2042Section 2ax-bgbltosilva 47811
[Pfenning] p. 17Definition XMnatded 30332
[Pfenning] p. 17Definition NNCnatded 30332  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30332
[Pfenning] p. 18Rule"natded 30332
[Pfenning] p. 18Definition /\Inatded 30332
[Pfenning] p. 18Definition ` `Enatded 30332  natded 30332  natded 30332  natded 30332  natded 30332
[Pfenning] p. 18Definition ` `Inatded 30332  natded 30332  natded 30332  natded 30332  natded 30332
[Pfenning] p. 18Definition ` `ELnatded 30332
[Pfenning] p. 18Definition ` `ERnatded 30332
[Pfenning] p. 18Definition ` `Ea,unatded 30332
[Pfenning] p. 18Definition ` `IRnatded 30332
[Pfenning] p. 18Definition ` `Ianatded 30332
[Pfenning] p. 127Definition =Enatded 30332
[Pfenning] p. 127Definition =Inatded 30332
[Ponnusamy] p. 361Theorem 6.44cphip0l 25102  df-dip 30630  dip0l 30647  ip0l 21545
[Ponnusamy] p. 361Equation 6.45cphipval 25143  ipval 30632
[Ponnusamy] p. 362Equation I1dipcj 30643  ipcj 21543
[Ponnusamy] p. 362Equation I3cphdir 25105  dipdir 30771  ipdir 21548  ipdiri 30759
[Ponnusamy] p. 362Equation I4ipidsq 30639  nmsq 25094
[Ponnusamy] p. 362Equation 6.46ip0i 30754
[Ponnusamy] p. 362Equation 6.47ip1i 30756
[Ponnusamy] p. 362Equation 6.48ip2i 30757
[Ponnusamy] p. 363Equation I2cphass 25111  dipass 30774  ipass 21554  ipassi 30770
[Prugovecki] p. 186Definition of brabraval 31873  df-bra 31779
[Prugovecki] p. 376Equation 8.1df-kb 31780  kbval 31883
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32311
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39882
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32325  atcvat4i 32326  cvrat3 39436  cvrat4 39437  lsatcvat3 39045
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32211  cvrval 39262  df-cv 32208  df-lcv 39012  lspsncv0 21056
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39894
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39895
[Quine] p. 16Definition 2.1df-clab 2708  rabid 3427  rabidd 45149
[Quine] p. 17Definition 2.1''dfsb7 2279
[Quine] p. 18Definition 2.7df-cleq 2721
[Quine] p. 19Definition 2.9conventions 30329  df-v 3449
[Quine] p. 34Theorem 5.1eqabb 2867
[Quine] p. 35Theorem 5.2abid1 2864  abid2f 2922
[Quine] p. 40Theorem 6.1sb5 2276
[Quine] p. 40Theorem 6.2sb6 2086  sbalex 2243
[Quine] p. 41Theorem 6.3df-clel 2803
[Quine] p. 41Theorem 6.4eqid 2729  eqid1 30396
[Quine] p. 41Theorem 6.5eqcom 2736
[Quine] p. 42Theorem 6.6df-sbc 3754
[Quine] p. 42Theorem 6.7dfsbcq 3755  dfsbcq2 3756
[Quine] p. 43Theorem 6.8vex 3451
[Quine] p. 43Theorem 6.9isset 3461
[Quine] p. 44Theorem 7.3spcgf 3557  spcgv 3562  spcimgf 3516
[Quine] p. 44Theorem 6.11spsbc 3766  spsbcd 3767
[Quine] p. 44Theorem 6.12elex 3468
[Quine] p. 44Theorem 6.13elab 3646  elabg 3643  elabgf 3641
[Quine] p. 44Theorem 6.14noel 4301
[Quine] p. 48Theorem 7.2snprc 4681
[Quine] p. 48Definition 7.1df-pr 4592  df-sn 4590
[Quine] p. 49Theorem 7.4snss 4749  snssg 4747
[Quine] p. 49Theorem 7.5prss 4784  prssg 4783
[Quine] p. 49Theorem 7.6prid1 4726  prid1g 4724  prid2 4727  prid2g 4725  snid 4626  snidg 4624
[Quine] p. 51Theorem 7.12snex 5391
[Quine] p. 51Theorem 7.13prex 5392
[Quine] p. 53Theorem 8.2unisn 4890  unisnALT 44915  unisng 4889
[Quine] p. 53Theorem 8.3uniun 4894
[Quine] p. 54Theorem 8.6elssuni 4901
[Quine] p. 54Theorem 8.7uni0 4899
[Quine] p. 56Theorem 8.17uniabio 6478
[Quine] p. 56Definition 8.18dfaiota2 47087  dfiota2 6465
[Quine] p. 57Theorem 8.19aiotaval 47096  iotaval 6482
[Quine] p. 57Theorem 8.22iotanul 6489
[Quine] p. 58Theorem 8.23iotaex 6484
[Quine] p. 58Definition 9.1df-op 4596
[Quine] p. 61Theorem 9.5opabid 5485  opabidw 5484  opelopab 5502  opelopaba 5496  opelopabaf 5504  opelopabf 5505  opelopabg 5498  opelopabga 5493  opelopabgf 5500  oprabid 7419  oprabidw 7418
[Quine] p. 64Definition 9.11df-xp 5644
[Quine] p. 64Definition 9.12df-cnv 5646
[Quine] p. 64Definition 9.15df-id 5533
[Quine] p. 65Theorem 10.3fun0 6581
[Quine] p. 65Theorem 10.4funi 6548
[Quine] p. 65Theorem 10.5funsn 6569  funsng 6567
[Quine] p. 65Definition 10.1df-fun 6513
[Quine] p. 65Definition 10.2args 6063  dffv4 6855
[Quine] p. 68Definition 10.11conventions 30329  df-fv 6519  fv2 6853
[Quine] p. 124Theorem 17.3nn0opth2 14237  nn0opth2i 14236  nn0opthi 14235  omopthi 8625
[Quine] p. 177Definition 25.2df-rdg 8378
[Quine] p. 232Equation icarddom 10507
[Quine] p. 284Axiom 39(vi)funimaex 6605  funimaexg 6603
[Quine] p. 331Axiom system NFru 3751
[ReedSimon] p. 36Definition (iii)ax-his3 31013
[ReedSimon] p. 63Exercise 4(a)df-dip 30630  polid 31088  polid2i 31086  polidi 31087
[ReedSimon] p. 63Exercise 4(b)df-ph 30742
[ReedSimon] p. 195Remarklnophm 31948  lnophmi 31947
[Retherford] p. 49Exercise 1(i)leopadd 32061
[Retherford] p. 49Exercise 1(ii)leopmul 32063  leopmuli 32062
[Retherford] p. 49Exercise 1(iv)leoptr 32066
[Retherford] p. 49Definition VI.1df-leop 31781  leoppos 32055
[Retherford] p. 49Exercise 1(iii)leoptri 32065
[Retherford] p. 49Definition of operator orderingleop3 32054
[Roman] p. 4Definitiondf-dmat 22377  df-dmatalt 48387
[Roman] p. 18Part Preliminariesdf-rng 20062
[Roman] p. 19Part Preliminariesdf-ring 20144
[Roman] p. 46Theorem 1.6isldepslvec2 48474
[Roman] p. 112Noteisldepslvec2 48474  ldepsnlinc 48497  zlmodzxznm 48486
[Roman] p. 112Examplezlmodzxzequa 48485  zlmodzxzequap 48488  zlmodzxzldep 48493
[Roman] p. 170Theorem 7.8cayleyhamilton 22777
[Rosenlicht] p. 80Theoremheicant 37649
[Rosser] p. 281Definitiondf-op 4596
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34636
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34637
[Rotman] p. 28Remarkpgrpgt2nabl 48354  pmtr3ncom 19405
[Rotman] p. 31Theorem 3.4symggen2 19401
[Rotman] p. 42Theorem 3.15cayley 19344  cayleyth 19345
[Rudin] p. 164Equation 27efcan 16062
[Rudin] p. 164Equation 30efzval 16070
[Rudin] p. 167Equation 48absefi 16164
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1771
[Sanford] p. 39Rule 4mptxor 1769
[Sanford] p. 40Rule 1mptnan 1768
[Schechter] p. 51Definition of antisymmetryintasym 6088
[Schechter] p. 51Definition of irreflexivityintirr 6091
[Schechter] p. 51Definition of symmetrycnvsym 6085
[Schechter] p. 51Definition of transitivitycotr 6083
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17547
[Schechter] p. 79Definition of Moore closuredf-mrc 17548
[Schechter] p. 82Section 4.5df-mrc 17548
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17550
[Schechter] p. 139Definition AC3dfac9 10090
[Schechter] p. 141Definition (MC)dfac11 43051
[Schechter] p. 149Axiom DC1ax-dc 10399  axdc3 10407
[Schechter] p. 187Definition of "ring with unit"isring 20146  isrngo 37891
[Schechter] p. 276Remark 11.6.espan0 31471
[Schechter] p. 276Definition of spandf-span 31238  spanval 31262
[Schechter] p. 428Definition 15.35bastop1 22880
[Schloeder] p. 1Lemma 1.3onelon 6357  onelord 43240  ordelon 6356  ordelord 6354
[Schloeder] p. 1Lemma 1.7onepsuc 43241  sucidg 6415
[Schloeder] p. 1Remark 1.50elon 6387  onsuc 7787  ord0 6386  ordsuci 7784
[Schloeder] p. 1Theorem 1.9epsoon 43242
[Schloeder] p. 1Definition 1.1dftr5 5218
[Schloeder] p. 1Definition 1.2dford3 43017  elon2 6343
[Schloeder] p. 1Definition 1.4df-suc 6338
[Schloeder] p. 1Definition 1.6epel 5541  epelg 5539
[Schloeder] p. 1Theorem 1.9(i)elirr 9550  epirron 43243  ordirr 6350
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43245  oneptr 43244  ontr1 6379
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6375  oneptri 43246  ordtri3or 6364
[Schloeder] p. 2Lemma 1.10ondif1 8465  ord0eln0 6388
[Schloeder] p. 2Lemma 1.13elsuci 6401  onsucss 43255  trsucss 6422
[Schloeder] p. 2Lemma 1.14ordsucss 7793
[Schloeder] p. 2Lemma 1.15onnbtwn 6428  ordnbtwn 6427
[Schloeder] p. 2Lemma 1.16orddif0suc 43257  ordnexbtwnsuc 43256
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10354  onsucf1lem 43258  onsucf1o 43261  onsucf1olem 43259  onsucrn 43260
[Schloeder] p. 2Lemma 1.18dflim7 43262
[Schloeder] p. 2Remark 1.12ordzsl 7821
[Schloeder] p. 2Theorem 1.10ondif1i 43251  ordne0gt0 43250
[Schloeder] p. 2Definition 1.11dflim6 43253  limnsuc 43254  onsucelab 43252
[Schloeder] p. 3Remark 1.21omex 9596
[Schloeder] p. 3Theorem 1.19tfinds 7836
[Schloeder] p. 3Theorem 1.22omelon 9599  ordom 7852
[Schloeder] p. 3Definition 1.20dfom3 9600
[Schloeder] p. 4Lemma 2.21onn 8604
[Schloeder] p. 4Lemma 2.7ssonuni 7756  ssorduni 7755
[Schloeder] p. 4Remark 2.4oa1suc 8495
[Schloeder] p. 4Theorem 1.23dfom5 9603  limom 7858
[Schloeder] p. 4Definition 2.1df-1o 8434  df1o2 8441
[Schloeder] p. 4Definition 2.3oa0 8480  oa0suclim 43264  oalim 8496  oasuc 8488
[Schloeder] p. 4Definition 2.5om0 8481  om0suclim 43265  omlim 8497  omsuc 8490
[Schloeder] p. 4Definition 2.6oe0 8486  oe0m1 8485  oe0suclim 43266  oelim 8498  oesuc 8491
[Schloeder] p. 5Lemma 2.10onsupuni 43218
[Schloeder] p. 5Lemma 2.11onsupsucismax 43268
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43269
[Schloeder] p. 5Lemma 2.13limexissup 43270  limexissupab 43272  limiun 43271  limuni 6394
[Schloeder] p. 5Lemma 2.14oa0r 8502
[Schloeder] p. 5Lemma 2.15om1 8506  om1om1r 43273  om1r 8507
[Schloeder] p. 5Remark 2.8oacl 8499  oaomoecl 43267  oecl 8501  omcl 8500
[Schloeder] p. 5Definition 2.9onsupintrab 43220
[Schloeder] p. 6Lemma 2.16oe1 8508
[Schloeder] p. 6Lemma 2.17oe1m 8509
[Schloeder] p. 6Lemma 2.18oe0rif 43274
[Schloeder] p. 6Theorem 2.19oasubex 43275
[Schloeder] p. 6Theorem 2.20nnacl 8575  nnamecl 43276  nnecl 8577  nnmcl 8576
[Schloeder] p. 7Lemma 3.1onsucwordi 43277
[Schloeder] p. 7Lemma 3.2oaword1 8516
[Schloeder] p. 7Lemma 3.3oaword2 8517
[Schloeder] p. 7Lemma 3.4oalimcl 8524
[Schloeder] p. 7Lemma 3.5oaltublim 43279
[Schloeder] p. 8Lemma 3.6oaordi3 43280
[Schloeder] p. 8Lemma 3.81oaomeqom 43282
[Schloeder] p. 8Lemma 3.10oa00 8523
[Schloeder] p. 8Lemma 3.11omge1 43286  omword1 8537
[Schloeder] p. 8Remark 3.9oaordnr 43285  oaordnrex 43284
[Schloeder] p. 8Theorem 3.7oaord3 43281
[Schloeder] p. 9Lemma 3.12omge2 43287  omword2 8538
[Schloeder] p. 9Lemma 3.13omlim2 43288
[Schloeder] p. 9Lemma 3.14omord2lim 43289
[Schloeder] p. 9Lemma 3.15omord2i 43290  omordi 8530
[Schloeder] p. 9Theorem 3.16omord 8532  omord2com 43291
[Schloeder] p. 10Lemma 3.172omomeqom 43292  df-2o 8435
[Schloeder] p. 10Lemma 3.19oege1 43295  oewordi 8555
[Schloeder] p. 10Lemma 3.20oege2 43296  oeworde 8557
[Schloeder] p. 10Lemma 3.21rp-oelim2 43297
[Schloeder] p. 10Lemma 3.22oeord2lim 43298
[Schloeder] p. 10Remark 3.18omnord1 43294  omnord1ex 43293
[Schloeder] p. 11Lemma 3.23oeord2i 43299
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43301
[Schloeder] p. 11Remark 3.26oenord1 43305  oenord1ex 43304
[Schloeder] p. 11Theorem 4.1oaomoencom 43306
[Schloeder] p. 11Theorem 4.2oaass 8525
[Schloeder] p. 11Theorem 3.24oeord2com 43300
[Schloeder] p. 12Theorem 4.3odi 8543
[Schloeder] p. 13Theorem 4.4omass 8544
[Schloeder] p. 14Remark 4.6oenass 43308
[Schloeder] p. 14Theorem 4.7oeoa 8561
[Schloeder] p. 15Lemma 5.1cantnftermord 43309
[Schloeder] p. 15Lemma 5.2cantnfub 43310  cantnfub2 43311
[Schloeder] p. 16Theorem 5.3cantnf2 43314
[Schwabhauser] p. 10Axiom A1axcgrrflx 28841  axtgcgrrflx 28389
[Schwabhauser] p. 10Axiom A2axcgrtr 28842
[Schwabhauser] p. 10Axiom A3axcgrid 28843  axtgcgrid 28390
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28375
[Schwabhauser] p. 11Axiom A4axsegcon 28854  axtgsegcon 28391  df-trkgcb 28377
[Schwabhauser] p. 11Axiom A5ax5seg 28865  axtg5seg 28392  df-trkgcb 28377
[Schwabhauser] p. 11Axiom A6axbtwnid 28866  axtgbtwnid 28393  df-trkgb 28376
[Schwabhauser] p. 12Axiom A7axpasch 28868  axtgpasch 28394  df-trkgb 28376
[Schwabhauser] p. 12Axiom A8axlowdim2 28887  df-trkg2d 34656
[Schwabhauser] p. 13Axiom A8axtglowdim2 28397
[Schwabhauser] p. 13Axiom A9axtgupdim2 28398  df-trkg2d 34656
[Schwabhauser] p. 13Axiom A10axeuclid 28890  axtgeucl 28399  df-trkge 28378
[Schwabhauser] p. 13Axiom A11axcont 28903  axtgcont 28396  axtgcont1 28395  df-trkgb 28376
[Schwabhauser] p. 27Theorem 2.1cgrrflx 35975
[Schwabhauser] p. 27Theorem 2.2cgrcomim 35977
[Schwabhauser] p. 27Theorem 2.3cgrtr 35980
[Schwabhauser] p. 27Theorem 2.4cgrcoml 35984
[Schwabhauser] p. 27Theorem 2.5cgrcomr 35985  tgcgrcomimp 28404  tgcgrcoml 28406  tgcgrcomr 28405
[Schwabhauser] p. 28Theorem 2.8cgrtriv 35990  tgcgrtriv 28411
[Schwabhauser] p. 28Theorem 2.105segofs 35994  tg5segofs 34664
[Schwabhauser] p. 28Definition 2.10df-afs 34661  df-ofs 35971
[Schwabhauser] p. 29Theorem 2.11cgrextend 35996  tgcgrextend 28412
[Schwabhauser] p. 29Theorem 2.12segconeq 35998  tgsegconeq 28413
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36010  btwntriv2 36000  tgbtwntriv2 28414
[Schwabhauser] p. 30Theorem 3.2btwncomim 36001  tgbtwncom 28415
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36004  tgbtwntriv1 28418
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36005  tgbtwnswapid 28419
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36011  btwnintr 36007  tgbtwnexch2 28423  tgbtwnintr 28420
[Schwabhauser] p. 30Theorem 3.6btwnexch 36013  btwnexch3 36008  tgbtwnexch 28425  tgbtwnexch3 28421
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36012  tgbtwnouttr 28424  tgbtwnouttr2 28422
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28886
[Schwabhauser] p. 32Theorem 3.14btwndiff 36015  tgbtwndiff 28433
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28426  trisegint 36016
[Schwabhauser] p. 34Theorem 4.2ifscgr 36032  tgifscgr 28435
[Schwabhauser] p. 34Theorem 4.11colcom 28485  colrot1 28486  colrot2 28487  lncom 28549  lnrot1 28550  lnrot2 28551
[Schwabhauser] p. 34Definition 4.1df-ifs 36028
[Schwabhauser] p. 35Theorem 4.3cgrsub 36033  tgcgrsub 28436
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36043  tgcgrxfr 28445
[Schwabhauser] p. 35Statement 4.4ercgrg 28444
[Schwabhauser] p. 35Definition 4.4df-cgr3 36029  df-cgrg 28438
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28438
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36044  tgbtwnxfr 28457
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36050  colinearperm2 36052  colinearperm3 36051  colinearperm4 36053  colinearperm5 36054
[Schwabhauser] p. 36Definition 4.8df-ismt 28460
[Schwabhauser] p. 36Definition 4.10df-colinear 36027  tgellng 28480  tglng 28473
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36055
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36063  lnxfr 28493
[Schwabhauser] p. 37Theorem 4.14lineext 36064  lnext 28494
[Schwabhauser] p. 37Theorem 4.16fscgr 36068  tgfscgr 28495
[Schwabhauser] p. 37Theorem 4.17linecgr 36069  lncgr 28496
[Schwabhauser] p. 37Definition 4.15df-fs 36030
[Schwabhauser] p. 38Theorem 4.18lineid 36071  lnid 28497
[Schwabhauser] p. 38Theorem 4.19idinside 36072  tgidinside 28498
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36089  tgbtwnconn1 28502
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36090  tgbtwnconn2 28503
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36091  tgbtwnconn3 28504
[Schwabhauser] p. 41Theorem 5.5brsegle2 36097
[Schwabhauser] p. 41Definition 5.4df-segle 36095  legov 28512
[Schwabhauser] p. 41Definition 5.5legov2 28513
[Schwabhauser] p. 42Remark 5.13legso 28526
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36098
[Schwabhauser] p. 42Theorem 5.7seglerflx 36100
[Schwabhauser] p. 42Theorem 5.8segletr 36102
[Schwabhauser] p. 42Theorem 5.9segleantisym 36103
[Schwabhauser] p. 42Theorem 5.10seglelin 36104
[Schwabhauser] p. 42Theorem 5.11seglemin 36101
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36106
[Schwabhauser] p. 42Proposition 5.7legid 28514
[Schwabhauser] p. 42Proposition 5.8legtrd 28516
[Schwabhauser] p. 42Proposition 5.9legtri3 28517
[Schwabhauser] p. 42Proposition 5.10legtrid 28518
[Schwabhauser] p. 42Proposition 5.11leg0 28519
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36113
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36114
[Schwabhauser] p. 43Theorem 6.4broutsideof 36109  df-outsideof 36108
[Schwabhauser] p. 43Definition 6.1broutsideof2 36110  ishlg 28529
[Schwabhauser] p. 44Theorem 6.4hlln 28534
[Schwabhauser] p. 44Theorem 6.5hlid 28536  outsideofrflx 36115
[Schwabhauser] p. 44Theorem 6.6hlcomb 28530  hlcomd 28531  outsideofcom 36116
[Schwabhauser] p. 44Theorem 6.7hltr 28537  outsideoftr 36117
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28545  outsideofeu 36119
[Schwabhauser] p. 44Definition 6.8df-ray 36126
[Schwabhauser] p. 45Part 2df-lines2 36127
[Schwabhauser] p. 45Theorem 6.13outsidele 36120
[Schwabhauser] p. 45Theorem 6.15lineunray 36135
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36136  tglineelsb2 28559
[Schwabhauser] p. 45Theorem 6.17linecom 36138  linerflx1 36137  linerflx2 36139  tglinecom 28562  tglinerflx1 28560  tglinerflx2 28561
[Schwabhauser] p. 45Theorem 6.18linethru 36141  tglinethru 28563
[Schwabhauser] p. 45Definition 6.14df-line2 36125  tglng 28473
[Schwabhauser] p. 45Proposition 6.13legbtwn 28521
[Schwabhauser] p. 46Theorem 6.19linethrueu 36144  tglinethrueu 28566
[Schwabhauser] p. 46Theorem 6.21lineintmo 36145  tglineineq 28570  tglineinteq 28572  tglineintmo 28569
[Schwabhauser] p. 46Theorem 6.23colline 28576
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28577
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28578
[Schwabhauser] p. 49Theorem 7.3mirinv 28593
[Schwabhauser] p. 49Theorem 7.7mirmir 28589
[Schwabhauser] p. 49Theorem 7.8mirreu3 28581
[Schwabhauser] p. 49Definition 7.5df-mir 28580  ismir 28586  mirbtwn 28585  mircgr 28584  mirfv 28583  mirval 28582
[Schwabhauser] p. 50Theorem 7.8mirreu 28591
[Schwabhauser] p. 50Theorem 7.9mireq 28592
[Schwabhauser] p. 50Theorem 7.10mirinv 28593
[Schwabhauser] p. 50Theorem 7.11mirf1o 28596
[Schwabhauser] p. 50Theorem 7.13miriso 28597
[Schwabhauser] p. 51Theorem 7.14mirmot 28602
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28599  mirbtwni 28598
[Schwabhauser] p. 51Theorem 7.16mircgrs 28600
[Schwabhauser] p. 51Theorem 7.17miduniq 28612
[Schwabhauser] p. 52Lemma 7.21symquadlem 28616
[Schwabhauser] p. 52Theorem 7.18miduniq1 28613
[Schwabhauser] p. 52Theorem 7.19miduniq2 28614
[Schwabhauser] p. 52Theorem 7.20colmid 28615
[Schwabhauser] p. 53Lemma 7.22krippen 28618
[Schwabhauser] p. 55Lemma 7.25midexlem 28619
[Schwabhauser] p. 57Theorem 8.2ragcom 28625
[Schwabhauser] p. 57Definition 8.1df-rag 28621  israg 28624
[Schwabhauser] p. 58Theorem 8.3ragcol 28626
[Schwabhauser] p. 58Theorem 8.4ragmir 28627
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28629
[Schwabhauser] p. 58Theorem 8.6ragflat2 28630
[Schwabhauser] p. 58Theorem 8.7ragflat 28631
[Schwabhauser] p. 58Theorem 8.8ragtriva 28632
[Schwabhauser] p. 58Theorem 8.9ragflat3 28633  ragncol 28636
[Schwabhauser] p. 58Theorem 8.10ragcgr 28634
[Schwabhauser] p. 59Theorem 8.12perpcom 28640
[Schwabhauser] p. 59Theorem 8.13ragperp 28644
[Schwabhauser] p. 59Theorem 8.14perpneq 28641
[Schwabhauser] p. 59Definition 8.11df-perpg 28623  isperp 28639
[Schwabhauser] p. 59Definition 8.13isperp2 28642
[Schwabhauser] p. 60Theorem 8.18foot 28649
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28657  colperpexlem2 28658
[Schwabhauser] p. 63Theorem 8.21colperpex 28660  colperpexlem3 28659
[Schwabhauser] p. 64Theorem 8.22mideu 28665  midex 28664
[Schwabhauser] p. 66Lemma 8.24opphllem 28662
[Schwabhauser] p. 67Theorem 9.2oppcom 28671
[Schwabhauser] p. 67Definition 9.1islnopp 28666
[Schwabhauser] p. 68Lemma 9.3opphllem2 28675
[Schwabhauser] p. 68Lemma 9.4opphllem5 28678  opphllem6 28679
[Schwabhauser] p. 69Theorem 9.5opphl 28681
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28394
[Schwabhauser] p. 70Theorem 9.6outpasch 28682
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28690
[Schwabhauser] p. 71Definition 9.7df-hpg 28685  hpgbr 28687
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28692
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28691
[Schwabhauser] p. 72Theorem 9.11hpgid 28693
[Schwabhauser] p. 72Theorem 9.12hpgcom 28694
[Schwabhauser] p. 72Theorem 9.13hpgtr 28695
[Schwabhauser] p. 73Theorem 9.18colopp 28696
[Schwabhauser] p. 73Theorem 9.19colhp 28697
[Schwabhauser] p. 88Theorem 10.2lmieu 28711
[Schwabhauser] p. 88Definition 10.1df-mid 28701
[Schwabhauser] p. 89Theorem 10.4lmicom 28715
[Schwabhauser] p. 89Theorem 10.5lmilmi 28716
[Schwabhauser] p. 89Theorem 10.6lmireu 28717
[Schwabhauser] p. 89Theorem 10.7lmieq 28718
[Schwabhauser] p. 89Theorem 10.8lmiinv 28719
[Schwabhauser] p. 89Theorem 10.9lmif1o 28722
[Schwabhauser] p. 89Theorem 10.10lmiiso 28724
[Schwabhauser] p. 89Definition 10.3df-lmi 28702
[Schwabhauser] p. 90Theorem 10.11lmimot 28725
[Schwabhauser] p. 91Theorem 10.12hypcgr 28728
[Schwabhauser] p. 92Theorem 10.14lmiopp 28729
[Schwabhauser] p. 92Theorem 10.15lnperpex 28730
[Schwabhauser] p. 92Theorem 10.16trgcopy 28731  trgcopyeu 28733
[Schwabhauser] p. 95Definition 11.2dfcgra2 28757
[Schwabhauser] p. 95Definition 11.3iscgra 28736
[Schwabhauser] p. 95Proposition 11.4cgracgr 28745
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28743  cgrahl2 28744
[Schwabhauser] p. 96Theorem 11.6cgraid 28746
[Schwabhauser] p. 96Theorem 11.9cgraswap 28747
[Schwabhauser] p. 97Theorem 11.7cgracom 28749
[Schwabhauser] p. 97Theorem 11.8cgratr 28750
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28753  cgrahl 28754
[Schwabhauser] p. 98Theorem 11.13sacgr 28758
[Schwabhauser] p. 98Theorem 11.14oacgr 28759
[Schwabhauser] p. 98Theorem 11.15acopy 28760  acopyeu 28761
[Schwabhauser] p. 101Theorem 11.24inagswap 28768
[Schwabhauser] p. 101Theorem 11.25inaghl 28772
[Schwabhauser] p. 101Definition 11.23isinag 28765
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28780
[Schwabhauser] p. 102Definition 11.27df-leag 28773  isleag 28774
[Schwabhauser] p. 107Theorem 11.49tgsas 28782  tgsas1 28781  tgsas2 28783  tgsas3 28784
[Schwabhauser] p. 108Theorem 11.50tgasa 28786  tgasa1 28785
[Schwabhauser] p. 109Theorem 11.51tgsss1 28787  tgsss2 28788  tgsss3 28789
[Shapiro] p. 230Theorem 6.5.1dchrhash 27182  dchrsum 27180  dchrsum2 27179  sumdchr 27183
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27184  sum2dchr 27185
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19998  ablfacrp2 19999
[Shapiro], p. 328Equation 9.2.4vmasum 27127
[Shapiro], p. 329Equation 9.2.7logfac2 27128
[Shapiro], p. 329Equation 9.2.9logfacrlim 27135
[Shapiro], p. 331Equation 9.2.13vmadivsum 27393
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27396
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27450  vmalogdivsum2 27449
[Shapiro], p. 375Theorem 9.4.1dirith 27440  dirith2 27439
[Shapiro], p. 375Equation 9.4.3rplogsum 27438  rpvmasum 27437  rpvmasum2 27423
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27398
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27436
[Shapiro], p. 377Lemma 9.4.1dchrisum 27403  dchrisumlem1 27400  dchrisumlem2 27401  dchrisumlem3 27402  dchrisumlema 27399
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27406
[Shapiro], p. 379Equation 9.4.16dchrmusum 27435  dchrmusumlem 27433  dchrvmasumlem 27434
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27405
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27407
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27431  dchrisum0re 27424  dchrisumn0 27432
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27417
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27421
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27422
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27477  pntrsumbnd2 27478  pntrsumo1 27476
[Shapiro], p. 405Equation 10.2.1mudivsum 27441
[Shapiro], p. 406Equation 10.2.6mulogsum 27443
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27445
[Shapiro], p. 407Equation 10.2.8mulog2sum 27448
[Shapiro], p. 418Equation 10.4.6logsqvma 27453
[Shapiro], p. 418Equation 10.4.8logsqvma2 27454
[Shapiro], p. 419Equation 10.4.10selberg 27459
[Shapiro], p. 420Equation 10.4.12selberg2lem 27461
[Shapiro], p. 420Equation 10.4.14selberg2 27462
[Shapiro], p. 422Equation 10.6.7selberg3 27470
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27471
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27468  selberg3lem2 27469
[Shapiro], p. 422Equation 10.4.23selberg4 27472
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27466
[Shapiro], p. 428Equation 10.6.2selbergr 27479
[Shapiro], p. 429Equation 10.6.8selberg3r 27480
[Shapiro], p. 430Equation 10.6.11selberg4r 27481
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27495
[Shapiro], p. 434Equation 10.6.27pntlema 27507  pntlemb 27508  pntlemc 27506  pntlemd 27505  pntlemg 27509
[Shapiro], p. 435Equation 10.6.29pntlema 27507
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27499
[Shapiro], p. 436Lemma 10.6.2pntibnd 27504
[Shapiro], p. 436Equation 10.6.34pntlema 27507
[Shapiro], p. 436Equation 10.6.35pntlem3 27520  pntleml 27522
[Stewart] p. 91Lemma 7.3constrss 33733
[Stewart] p. 92Definition 7.4.df-constr 33720
[Stewart] p. 96Theorem 7.10constraddcl 33752  constrinvcl 33763  constrmulcl 33761  constrnegcl 33753  constrsqrtcl 33769
[Stewart] p. 97Theorem 7.11constrextdg2 33739
[Stewart] p. 98Theorem 7.12constrext2chn 33749
[Stewart] p. 99Theorem 7.132sqr3nconstr 33771
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33781
[Stoll] p. 13Definition corresponds to dfsymdif3 4269
[Stoll] p. 16Exercise 4.40dif 4368  dif0 4341
[Stoll] p. 16Exercise 4.8difdifdir 4455
[Stoll] p. 17Theorem 5.1(5)unvdif 4438
[Stoll] p. 19Theorem 5.2(13)undm 4260
[Stoll] p. 19Theorem 5.2(13')indm 4261
[Stoll] p. 20Remarkinvdif 4242
[Stoll] p. 25Definition of ordered tripledf-ot 4598
[Stoll] p. 43Definitionuniiun 5022
[Stoll] p. 44Definitionintiin 5023
[Stoll] p. 45Definitiondf-iin 4958
[Stoll] p. 45Definition indexed uniondf-iun 4957
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4269
[Strang] p. 242Section 6.3expgrowth 44324
[Suppes] p. 22Theorem 2eq0 4313  eq0f 4310
[Suppes] p. 22Theorem 4eqss 3962  eqssd 3964  eqssi 3963
[Suppes] p. 23Theorem 5ss0 4365  ss0b 4364
[Suppes] p. 23Theorem 6sstr 3955  sstrALT2 44824
[Suppes] p. 23Theorem 7pssirr 4066
[Suppes] p. 23Theorem 8pssn2lp 4067
[Suppes] p. 23Theorem 9psstr 4070
[Suppes] p. 23Theorem 10pssss 4061
[Suppes] p. 25Theorem 12elin 3930  elun 4116
[Suppes] p. 26Theorem 15inidm 4190
[Suppes] p. 26Theorem 16in0 4358
[Suppes] p. 27Theorem 23unidm 4120
[Suppes] p. 27Theorem 24un0 4357
[Suppes] p. 27Theorem 25ssun1 4141
[Suppes] p. 27Theorem 26ssequn1 4149
[Suppes] p. 27Theorem 27unss 4153
[Suppes] p. 27Theorem 28indir 4249
[Suppes] p. 27Theorem 29undir 4250
[Suppes] p. 28Theorem 32difid 4339
[Suppes] p. 29Theorem 33difin 4235
[Suppes] p. 29Theorem 34indif 4243
[Suppes] p. 29Theorem 35undif1 4439
[Suppes] p. 29Theorem 36difun2 4444
[Suppes] p. 29Theorem 37difin0 4437
[Suppes] p. 29Theorem 38disjdif 4435
[Suppes] p. 29Theorem 39difundi 4253
[Suppes] p. 29Theorem 40difindi 4255
[Suppes] p. 30Theorem 41nalset 5268
[Suppes] p. 39Theorem 61uniss 4879
[Suppes] p. 39Theorem 65uniop 5475
[Suppes] p. 41Theorem 70intsn 4948
[Suppes] p. 42Theorem 71intpr 4946  intprg 4945
[Suppes] p. 42Theorem 73op1stb 5431
[Suppes] p. 42Theorem 78intun 4944
[Suppes] p. 44Definition 15(a)dfiun2 4997  dfiun2g 4994
[Suppes] p. 44Definition 15(b)dfiin2 4998
[Suppes] p. 47Theorem 86elpw 4567  elpw2 5289  elpw2g 5288  elpwg 4566  elpwgdedVD 44906
[Suppes] p. 47Theorem 87pwid 4585
[Suppes] p. 47Theorem 89pw0 4776
[Suppes] p. 48Theorem 90pwpw0 4777
[Suppes] p. 52Theorem 101xpss12 5653
[Suppes] p. 52Theorem 102xpindi 5797  xpindir 5798
[Suppes] p. 52Theorem 103xpundi 5707  xpundir 5708
[Suppes] p. 54Theorem 105elirrv 9549
[Suppes] p. 58Theorem 2relss 5744
[Suppes] p. 59Theorem 4eldm 5864  eldm2 5865  eldm2g 5863  eldmg 5862
[Suppes] p. 59Definition 3df-dm 5648
[Suppes] p. 60Theorem 6dmin 5875
[Suppes] p. 60Theorem 8rnun 6118
[Suppes] p. 60Theorem 9rnin 6119
[Suppes] p. 60Definition 4dfrn2 5852
[Suppes] p. 61Theorem 11brcnv 5846  brcnvg 5843
[Suppes] p. 62Equation 5elcnv 5840  elcnv2 5841
[Suppes] p. 62Theorem 12relcnv 6075
[Suppes] p. 62Theorem 15cnvin 6117
[Suppes] p. 62Theorem 16cnvun 6115
[Suppes] p. 63Definitiondftrrels2 38566
[Suppes] p. 63Theorem 20co02 6233
[Suppes] p. 63Theorem 21dmcoss 5938
[Suppes] p. 63Definition 7df-co 5647
[Suppes] p. 64Theorem 26cnvco 5849
[Suppes] p. 64Theorem 27coass 6238
[Suppes] p. 65Theorem 31resundi 5964
[Suppes] p. 65Theorem 34elima 6036  elima2 6037  elima3 6038  elimag 6035
[Suppes] p. 65Theorem 35imaundi 6122
[Suppes] p. 66Theorem 40dminss 6126
[Suppes] p. 66Theorem 41imainss 6127
[Suppes] p. 67Exercise 11cnvxp 6130
[Suppes] p. 81Definition 34dfec2 8674
[Suppes] p. 82Theorem 72elec 8717  elecALTV 38255  elecg 8715
[Suppes] p. 82Theorem 73eqvrelth 38602  erth 8725  erth2 8726
[Suppes] p. 83Theorem 74eqvreldisj 38605  erdisj 8728
[Suppes] p. 83Definition 35, df-parts 38757  dfmembpart2 38762
[Suppes] p. 89Theorem 96map0b 8856
[Suppes] p. 89Theorem 97map0 8860  map0g 8857
[Suppes] p. 89Theorem 98mapsn 8861  mapsnd 8859
[Suppes] p. 89Theorem 99mapss 8862
[Suppes] p. 91Definition 12(ii)alephsuc 10021
[Suppes] p. 91Definition 12(iii)alephlim 10020
[Suppes] p. 92Theorem 1enref 8956  enrefg 8955
[Suppes] p. 92Theorem 2ensym 8974  ensymb 8973  ensymi 8975
[Suppes] p. 92Theorem 3entr 8977
[Suppes] p. 92Theorem 4unen 9017
[Suppes] p. 94Theorem 15endom 8950
[Suppes] p. 94Theorem 16ssdomg 8971
[Suppes] p. 94Theorem 17domtr 8978
[Suppes] p. 95Theorem 18sbth 9061
[Suppes] p. 97Theorem 23canth2 9094  canth2g 9095
[Suppes] p. 97Definition 3brsdom2 9065  df-sdom 8921  dfsdom2 9064
[Suppes] p. 97Theorem 21(i)sdomirr 9078
[Suppes] p. 97Theorem 22(i)domnsym 9067
[Suppes] p. 97Theorem 21(ii)sdomnsym 9066
[Suppes] p. 97Theorem 22(ii)domsdomtr 9076
[Suppes] p. 97Theorem 22(iv)brdom2 8953
[Suppes] p. 97Theorem 21(iii)sdomtr 9079
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9074
[Suppes] p. 98Exercise 4fundmen 9002  fundmeng 9003
[Suppes] p. 98Exercise 6xpdom3 9039
[Suppes] p. 98Exercise 11sdomentr 9075
[Suppes] p. 104Theorem 37fofi 9262
[Suppes] p. 104Theorem 38pwfi 9268
[Suppes] p. 105Theorem 40pwfi 9268
[Suppes] p. 111Axiom for cardinal numberscarden 10504
[Suppes] p. 130Definition 3df-tr 5215
[Suppes] p. 132Theorem 9ssonuni 7756
[Suppes] p. 134Definition 6df-suc 6338
[Suppes] p. 136Theorem Schema 22findes 7876  finds 7872  finds1 7875  finds2 7874
[Suppes] p. 151Theorem 42isfinite 9605  isfinite2 9245  isfiniteg 9248  unbnn 9243
[Suppes] p. 162Definition 5df-ltnq 10871  df-ltpq 10863
[Suppes] p. 197Theorem Schema 4tfindes 7839  tfinds 7836  tfinds2 7840
[Suppes] p. 209Theorem 18oaord1 8515
[Suppes] p. 209Theorem 21oaword2 8517
[Suppes] p. 211Theorem 25oaass 8525
[Suppes] p. 225Definition 8iscard2 9929
[Suppes] p. 227Theorem 56ondomon 10516
[Suppes] p. 228Theorem 59harcard 9931
[Suppes] p. 228Definition 12(i)aleph0 10019
[Suppes] p. 228Theorem Schema 61onintss 6384
[Suppes] p. 228Theorem Schema 62onminesb 7769  onminsb 7770
[Suppes] p. 229Theorem 64alephval2 10525
[Suppes] p. 229Theorem 65alephcard 10023
[Suppes] p. 229Theorem 66alephord2i 10030
[Suppes] p. 229Theorem 67alephnbtwn 10024
[Suppes] p. 229Definition 12df-aleph 9893
[Suppes] p. 242Theorem 6weth 10448
[Suppes] p. 242Theorem 8entric 10510
[Suppes] p. 242Theorem 9carden 10504
[Szendrei] p. 11Line 6df-cloneop 35683
[Szendrei] p. 11Paragraph 3df-suppos 35687
[TakeutiZaring] p. 8Axiom 1ax-ext 2701
[TakeutiZaring] p. 13Definition 4.5df-cleq 2721
[TakeutiZaring] p. 13Proposition 4.6df-clel 2803
[TakeutiZaring] p. 13Proposition 4.9cvjust 2723
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2749
[TakeutiZaring] p. 14Definition 4.16df-oprab 7391
[TakeutiZaring] p. 14Proposition 4.14ru 3751
[TakeutiZaring] p. 15Axiom 2zfpair 5376
[TakeutiZaring] p. 15Exercise 1elpr 4614  elpr2 4616  elpr2g 4615  elprg 4612
[TakeutiZaring] p. 15Exercise 2elsn 4604  elsn2 4629  elsn2g 4628  elsng 4603  velsn 4605
[TakeutiZaring] p. 15Exercise 3elop 5427
[TakeutiZaring] p. 15Exercise 4sneq 4599  sneqr 4804
[TakeutiZaring] p. 15Definition 5.1dfpr2 4610  dfsn2 4602  dfsn2ALT 4611
[TakeutiZaring] p. 16Axiom 3uniex 7717
[TakeutiZaring] p. 16Exercise 6opth 5436
[TakeutiZaring] p. 16Exercise 7opex 5424
[TakeutiZaring] p. 16Exercise 8rext 5408
[TakeutiZaring] p. 16Corollary 5.8unex 7720  unexg 7719
[TakeutiZaring] p. 16Definition 5.3dftp2 4655
[TakeutiZaring] p. 16Definition 5.5df-uni 4872
[TakeutiZaring] p. 16Definition 5.6df-in 3921  df-un 3919
[TakeutiZaring] p. 16Proposition 5.7unipr 4888  uniprg 4887
[TakeutiZaring] p. 17Axiom 4vpwex 5332
[TakeutiZaring] p. 17Exercise 1eltp 4653
[TakeutiZaring] p. 17Exercise 5elsuc 6404  elsucg 6402  sstr2 3953
[TakeutiZaring] p. 17Exercise 6uncom 4121
[TakeutiZaring] p. 17Exercise 7incom 4172
[TakeutiZaring] p. 17Exercise 8unass 4135
[TakeutiZaring] p. 17Exercise 9inass 4191
[TakeutiZaring] p. 17Exercise 10indi 4247
[TakeutiZaring] p. 17Exercise 11undi 4248
[TakeutiZaring] p. 17Definition 5.9df-pss 3934  df-ss 3931
[TakeutiZaring] p. 17Definition 5.10df-pw 4565
[TakeutiZaring] p. 18Exercise 7unss2 4150
[TakeutiZaring] p. 18Exercise 9dfss2 3932  sseqin2 4186
[TakeutiZaring] p. 18Exercise 10ssid 3969
[TakeutiZaring] p. 18Exercise 12inss1 4200  inss2 4201
[TakeutiZaring] p. 18Exercise 13nss 4011
[TakeutiZaring] p. 18Exercise 15unieq 4882
[TakeutiZaring] p. 18Exercise 18sspwb 5409  sspwimp 44907  sspwimpALT 44914  sspwimpALT2 44917  sspwimpcf 44909
[TakeutiZaring] p. 18Exercise 19pweqb 5416
[TakeutiZaring] p. 19Axiom 5ax-rep 5234
[TakeutiZaring] p. 20Definitiondf-rab 3406
[TakeutiZaring] p. 20Corollary 5.160ex 5262
[TakeutiZaring] p. 20Definition 5.12df-dif 3917
[TakeutiZaring] p. 20Definition 5.14dfnul2 4299
[TakeutiZaring] p. 20Proposition 5.15difid 4339
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4316  n0f 4312  neq0 4315  neq0f 4311
[TakeutiZaring] p. 21Axiom 6zfreg 9548
[TakeutiZaring] p. 21Axiom 6'zfregs 9685
[TakeutiZaring] p. 21Theorem 5.22setind 9687
[TakeutiZaring] p. 21Definition 5.20df-v 3449
[TakeutiZaring] p. 21Proposition 5.21vprc 5270
[TakeutiZaring] p. 22Exercise 10ss 4363
[TakeutiZaring] p. 22Exercise 3ssex 5276  ssexg 5278
[TakeutiZaring] p. 22Exercise 4inex1 5272
[TakeutiZaring] p. 22Exercise 5ruv 9555
[TakeutiZaring] p. 22Exercise 6elirr 9550
[TakeutiZaring] p. 22Exercise 7ssdif0 4329
[TakeutiZaring] p. 22Exercise 11difdif 4098
[TakeutiZaring] p. 22Exercise 13undif3 4263  undif3VD 44871
[TakeutiZaring] p. 22Exercise 14difss 4099
[TakeutiZaring] p. 22Exercise 15sscon 4106
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3045
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3054
[TakeutiZaring] p. 23Proposition 6.2xpex 7729  xpexg 7726
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5645
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6587
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6765  fun11 6590
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6527  svrelfun 6588
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5851
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5853
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5650
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5651
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5647
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6167  dfrel2 6162
[TakeutiZaring] p. 25Exercise 3xpss 5654
[TakeutiZaring] p. 25Exercise 5relun 5774
[TakeutiZaring] p. 25Exercise 6reluni 5781
[TakeutiZaring] p. 25Exercise 9inxp 5795
[TakeutiZaring] p. 25Exercise 12relres 5976
[TakeutiZaring] p. 25Exercise 13opelres 5956  opelresi 5958
[TakeutiZaring] p. 25Exercise 14dmres 5983
[TakeutiZaring] p. 25Exercise 15resss 5972
[TakeutiZaring] p. 25Exercise 17resabs1 5977
[TakeutiZaring] p. 25Exercise 18funres 6558
[TakeutiZaring] p. 25Exercise 24relco 6079
[TakeutiZaring] p. 25Exercise 29funco 6556
[TakeutiZaring] p. 25Exercise 30f1co 6767
[TakeutiZaring] p. 26Definition 6.10eu2 2602
[TakeutiZaring] p. 26Definition 6.11conventions 30329  df-fv 6519  fv3 6876
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7901  cnvexg 7900
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7885  dmexg 7877
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7886  rnexg 7878
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44443
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7896
[TakeutiZaring] p. 27Corollary 6.13fvex 6871
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47175  tz6.12-1-afv2 47242  tz6.12-1 6881  tz6.12-afv 47174  tz6.12-afv2 47241  tz6.12 6883  tz6.12c-afv2 47243  tz6.12c 6880
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47238  tz6.12-2 6846  tz6.12i-afv2 47244  tz6.12i 6886
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6514
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6515
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6517  wfo 6509
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6516  wf1 6508
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6518  wf1o 6510
[TakeutiZaring] p. 28Exercise 4eqfnfv 7003  eqfnfv2 7004  eqfnfv2f 7007
[TakeutiZaring] p. 28Exercise 5fvco 6959
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7191
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7189
[TakeutiZaring] p. 29Exercise 9funimaex 6605  funimaexg 6603
[TakeutiZaring] p. 29Definition 6.18df-br 5108
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5547
[TakeutiZaring] p. 30Definition 6.21dffr2 5599  dffr3 6070  eliniseg 6065  iniseg 6068
[TakeutiZaring] p. 30Definition 6.22df-eprel 5538
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5615  fr3nr 7748  frirr 5614
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5591
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7750
[TakeutiZaring] p. 31Exercise 1frss 5602
[TakeutiZaring] p. 31Exercise 4wess 5624
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6320  tz6.26i 6321  wefrc 5632  wereu2 5635
[TakeutiZaring] p. 32Theorem 6.27wfi 6322  wfii 6323
[TakeutiZaring] p. 32Definition 6.28df-isom 6520
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7304
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7305
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7311
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7312
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7313
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7317
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7324
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7326
[TakeutiZaring] p. 35Notationwtr 5214
[TakeutiZaring] p. 35Theorem 7.2trelpss 44444  tz7.2 5621
[TakeutiZaring] p. 35Definition 7.1dftr3 5220
[TakeutiZaring] p. 36Proposition 7.4ordwe 6345
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6353
[TakeutiZaring] p. 36Proposition 7.6ordelord 6354  ordelordALT 44527  ordelordALTVD 44856
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6360  ordelssne 6359
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6358
[TakeutiZaring] p. 37Proposition 7.9ordin 6362
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7758
[TakeutiZaring] p. 38Corollary 7.15ordsson 7759
[TakeutiZaring] p. 38Definition 7.11df-on 6336
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6364
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44539  ordon 7753
[TakeutiZaring] p. 38Proposition 7.13onprc 7754
[TakeutiZaring] p. 39Theorem 7.17tfi 7829
[TakeutiZaring] p. 40Exercise 3ontr2 6380
[TakeutiZaring] p. 40Exercise 7dftr2 5216
[TakeutiZaring] p. 40Exercise 9onssmin 7768
[TakeutiZaring] p. 40Exercise 11unon 7806
[TakeutiZaring] p. 40Exercise 12ordun 6438
[TakeutiZaring] p. 40Exercise 14ordequn 6437
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7755
[TakeutiZaring] p. 40Proposition 7.20elssuni 4901
[TakeutiZaring] p. 41Definition 7.22df-suc 6338
[TakeutiZaring] p. 41Proposition 7.23sssucid 6414  sucidg 6415
[TakeutiZaring] p. 41Proposition 7.24onsuc 7787
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6428  ordnbtwn 6427
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7803
[TakeutiZaring] p. 42Exercise 1df-lim 6337
[TakeutiZaring] p. 42Exercise 4omssnlim 7857
[TakeutiZaring] p. 42Exercise 7ssnlim 7862
[TakeutiZaring] p. 42Exercise 8onsucssi 7817  ordelsuc 7795
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7797
[TakeutiZaring] p. 42Definition 7.27nlimon 7827
[TakeutiZaring] p. 42Definition 7.28dfom2 7844
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7865
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7866
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7867
[TakeutiZaring] p. 43Remarkomon 7854
[TakeutiZaring] p. 43Axiom 7inf3 9588  omex 9596
[TakeutiZaring] p. 43Theorem 7.32ordom 7852
[TakeutiZaring] p. 43Corollary 7.31find 7871
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7868
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7869
[TakeutiZaring] p. 44Exercise 1limomss 7847
[TakeutiZaring] p. 44Exercise 2int0 4926
[TakeutiZaring] p. 44Exercise 3trintss 5233
[TakeutiZaring] p. 44Exercise 4intss1 4927
[TakeutiZaring] p. 44Exercise 5intex 5299
[TakeutiZaring] p. 44Exercise 6oninton 7771
[TakeutiZaring] p. 44Exercise 11ordintdif 6383
[TakeutiZaring] p. 44Definition 7.35df-int 4911
[TakeutiZaring] p. 44Proposition 7.34noinfep 9613
[TakeutiZaring] p. 45Exercise 4onint 7766
[TakeutiZaring] p. 47Lemma 1tfrlem1 8344
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8365
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8366
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8367
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8374  tz7.44-2 8375  tz7.44-3 8376
[TakeutiZaring] p. 50Exercise 1smogt 8336
[TakeutiZaring] p. 50Exercise 3smoiso 8331
[TakeutiZaring] p. 50Definition 7.46df-smo 8315
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8413  tz7.49c 8414
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8411
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8410
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8412
[TakeutiZaring] p. 53Proposition 7.532eu5 2649
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9964
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9965
[TakeutiZaring] p. 56Definition 8.1oalim 8496  oasuc 8488
[TakeutiZaring] p. 57Remarktfindsg 7837
[TakeutiZaring] p. 57Proposition 8.2oacl 8499
[TakeutiZaring] p. 57Proposition 8.3oa0 8480  oa0r 8502
[TakeutiZaring] p. 57Proposition 8.16omcl 8500
[TakeutiZaring] p. 58Corollary 8.5oacan 8512
[TakeutiZaring] p. 58Proposition 8.4nnaord 8583  nnaordi 8582  oaord 8511  oaordi 8510
[TakeutiZaring] p. 59Proposition 8.6iunss2 5013  uniss2 4905
[TakeutiZaring] p. 59Proposition 8.7oawordri 8514
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8519  oawordex 8521
[TakeutiZaring] p. 59Proposition 8.9nnacl 8575
[TakeutiZaring] p. 59Proposition 8.10oaabs 8612
[TakeutiZaring] p. 60Remarkoancom 9604
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8524
[TakeutiZaring] p. 62Exercise 1nnarcl 8580
[TakeutiZaring] p. 62Exercise 5oaword1 8516
[TakeutiZaring] p. 62Definition 8.15om0x 8483  omlim 8497  omsuc 8490
[TakeutiZaring] p. 62Definition 8.15(a)om0 8481
[TakeutiZaring] p. 63Proposition 8.17nnecl 8577  nnmcl 8576
[TakeutiZaring] p. 63Proposition 8.19nnmord 8596  nnmordi 8595  omord 8532  omordi 8530
[TakeutiZaring] p. 63Proposition 8.20omcan 8533
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8600  omwordri 8536
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8503
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8506  om1r 8507
[TakeutiZaring] p. 64Proposition 8.22om00 8539
[TakeutiZaring] p. 64Proposition 8.23omordlim 8541
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8542
[TakeutiZaring] p. 64Proposition 8.25odi 8543
[TakeutiZaring] p. 65Theorem 8.26omass 8544
[TakeutiZaring] p. 67Definition 8.30nnesuc 8572  oe0 8486  oelim 8498  oesuc 8491  onesuc 8494
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8484
[TakeutiZaring] p. 67Proposition 8.32oen0 8550
[TakeutiZaring] p. 67Proposition 8.33oeordi 8551
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8485
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8509
[TakeutiZaring] p. 68Corollary 8.34oeord 8552
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8558
[TakeutiZaring] p. 68Proposition 8.35oewordri 8556
[TakeutiZaring] p. 68Proposition 8.37oeworde 8557
[TakeutiZaring] p. 69Proposition 8.41oeoa 8561
[TakeutiZaring] p. 70Proposition 8.42oeoe 8563
[TakeutiZaring] p. 73Theorem 9.1trcl 9681  tz9.1 9682
[TakeutiZaring] p. 76Definition 9.9df-r1 9717  r10 9721  r1lim 9725  r1limg 9724  r1suc 9723  r1sucg 9722
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9733  r1ord2 9734  r1ordg 9731
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9743
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9768  tz9.13 9744  tz9.13g 9745
[TakeutiZaring] p. 79Definition 9.14df-rank 9718  rankval 9769  rankvalb 9750  rankvalg 9770
[TakeutiZaring] p. 79Proposition 9.16rankel 9792  rankelb 9777
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9806  rankval3 9793  rankval3b 9779
[TakeutiZaring] p. 79Proposition 9.18rankonid 9782
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9748
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9787  rankr1c 9774  rankr1g 9785
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9788
[TakeutiZaring] p. 80Exercise 1rankss 9802  rankssb 9801
[TakeutiZaring] p. 80Exercise 2unbndrank 9795
[TakeutiZaring] p. 80Proposition 9.19bndrank 9794
[TakeutiZaring] p. 83Axiom of Choiceac4 10428  dfac3 10074
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9983  numth 10425  numth2 10424
[TakeutiZaring] p. 85Definition 10.4cardval 10499
[TakeutiZaring] p. 85Proposition 10.5cardid 10500  cardid2 9906
[TakeutiZaring] p. 85Proposition 10.9oncard 9913
[TakeutiZaring] p. 85Proposition 10.10carden 10504
[TakeutiZaring] p. 85Proposition 10.11cardidm 9912
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9897
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9918
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9910
[TakeutiZaring] p. 87Proposition 10.15pwen 9114
[TakeutiZaring] p. 88Exercise 1en0 8989
[TakeutiZaring] p. 88Exercise 7infensuc 9119
[TakeutiZaring] p. 89Exercise 10omxpen 9043
[TakeutiZaring] p. 90Corollary 10.23cardnn 9916
[TakeutiZaring] p. 90Definition 10.27alephiso 10051
[TakeutiZaring] p. 90Proposition 10.20nneneq 9170
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9178
[TakeutiZaring] p. 90Proposition 10.26alephprc 10052
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9175
[TakeutiZaring] p. 91Exercise 2alephle 10041
[TakeutiZaring] p. 91Exercise 3aleph0 10019
[TakeutiZaring] p. 91Exercise 4cardlim 9925
[TakeutiZaring] p. 91Exercise 7infpss 10169
[TakeutiZaring] p. 91Exercise 8infcntss 9273
[TakeutiZaring] p. 91Definition 10.29df-fin 8922  isfi 8947
[TakeutiZaring] p. 92Proposition 10.32onfin 9179
[TakeutiZaring] p. 92Proposition 10.34imadomg 10487
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9036
[TakeutiZaring] p. 93Proposition 10.35fodomb 10479
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10139  unxpdom 9200
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9927  cardsdomelir 9926
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9202
[TakeutiZaring] p. 94Proposition 10.39infxpen 9967
[TakeutiZaring] p. 95Definition 10.42df-map 8801
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10515  infxpidm2 9970
[TakeutiZaring] p. 95Proposition 10.41infdju 10160  infxp 10167
[TakeutiZaring] p. 96Proposition 10.44pw2en 9048  pw2f1o 9046
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9107
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10440
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10435  ac6s5 10444
[TakeutiZaring] p. 98Theorem 10.47unidom 10496
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10497  uniimadomf 10498
[TakeutiZaring] p. 100Definition 11.1cfcof 10227
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10222
[TakeutiZaring] p. 102Exercise 1cfle 10207
[TakeutiZaring] p. 102Exercise 2cf0 10204
[TakeutiZaring] p. 102Exercise 3cfsuc 10210
[TakeutiZaring] p. 102Exercise 4cfom 10217
[TakeutiZaring] p. 102Proposition 11.9coftr 10226
[TakeutiZaring] p. 103Theorem 11.15alephreg 10535
[TakeutiZaring] p. 103Proposition 11.11cardcf 10205
[TakeutiZaring] p. 103Proposition 11.13alephsing 10229
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10050
[TakeutiZaring] p. 104Proposition 11.16carduniima 10049
[TakeutiZaring] p. 104Proposition 11.18alephfp 10061  alephfp2 10062
[TakeutiZaring] p. 106Theorem 11.20gchina 10652
[TakeutiZaring] p. 106Theorem 11.21mappwen 10065
[TakeutiZaring] p. 107Theorem 11.26konigth 10522
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10536
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10537
[Tarski] p. 67Axiom B5ax-c5 38876
[Tarski] p. 67Scheme B5sp 2184
[Tarski] p. 68Lemma 6avril1 30392  equid 2012
[Tarski] p. 69Lemma 7equcomi 2017
[Tarski] p. 70Lemma 14spim 2385  spime 2387  spimew 1971
[Tarski] p. 70Lemma 16ax-12 2178  ax-c15 38882  ax12i 1966
[Tarski] p. 70Lemmas 16 and 17sb6 2086
[Tarski] p. 75Axiom B7ax6v 1968
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1910  ax5ALT 38900
[Tarski], p. 75Scheme B8 of system S2ax-7 2008  ax-8 2111  ax-9 2119
[Tarski1999] p. 178Axiom 4axtgsegcon 28391
[Tarski1999] p. 178Axiom 5axtg5seg 28392
[Tarski1999] p. 179Axiom 7axtgpasch 28394
[Tarski1999] p. 180Axiom 7.1axtgpasch 28394
[Tarski1999] p. 185Axiom 11axtgcont1 28395
[Truss] p. 114Theorem 5.18ruc 16211
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37653
[Viaclovsky8] p. 3Proposition 7ismblfin 37655
[Weierstrass] p. 272Definitiondf-mdet 22472  mdetuni 22509
[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 37433
[WhiteheadRussell] p. 100Theorem *2.05frege5 43789  imim2 58  wl-luk-imim2 37428
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47020  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2656  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37431
[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 44916  wl-luk-notnotr 37432
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 43819  axfrege28 43818  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 37425
[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 30330  pm2.27 42  wl-luk-pm2.27 37423
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38345
[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 44347
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44348
[WhiteheadRussell] p. 147Theorem *10.2219.26 1870
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44349
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44350
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44351
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1893
[WhiteheadRussell] p. 151Theorem *10.301albitr 44352
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44353
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44354
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44355
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44356
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44358
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44359
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44360
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44357
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2091
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44363
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44364
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2071
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2161
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1829
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1830
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44365
[WhiteheadRussell] p. 162Theorem *11.322alim 44366
[WhiteheadRussell] p. 162Theorem *11.332albi 44367
[WhiteheadRussell] p. 162Theorem *11.342exim 44368
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44370
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44369
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1887
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44372
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44373
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44371
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1828
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44374
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44375
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1846
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44376
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2344
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1860
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44381
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44377
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44378
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44379
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44380
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44385
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44382
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44383
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44384
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44386
[WhiteheadRussell] p. 175Definition *14.02df-eu 2562
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44396  pm13.13b 44397
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44398
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3006
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3007
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3632
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44404
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44405
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44399
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44542  pm13.193 44400
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44401
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44402
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44403
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44410
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44409
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44408
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3816
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44411  pm14.122b 44412  pm14.122c 44413
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44414  pm14.123b 44415  pm14.123c 44416
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44418
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44417
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44419
[WhiteheadRussell] p. 190Theorem *14.22iota4 6492
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44420
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6493
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44421
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44423
[WhiteheadRussell] p. 192Theorem *14.26eupick 2626  eupickbi 2629  sbaniota 44424
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44422
[WhiteheadRussell] p. 192Theorem *14.271eubi 2577
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44426
[WhiteheadRussell] p. 235Definition *30.01conventions 30329  df-fv 6519
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9954  pm54.43lem 9953
[Young] p. 141Definition of operator orderingleop2 32053
[Young] p. 142Example 12.2(i)0leop 32059  idleop 32060
[vandenDries] p. 42Lemma 61irrapx1 42816
[vandenDries] p. 43Theorem 62pellex 42823  pellexlem1 42817

This page was last updated on 14-Dec-2025.
Copyright terms: Public domain