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 17804
[Adamek] p. 21Condition 3.1(b)df-cat 17804
[Adamek] p. 22Example 3.3(1)df-setc 18213
[Adamek] p. 24Example 3.3(4.c)0cat 17825  0funcg 50115  df-termc 50503
[Adamek] p. 24Example 3.3(4.d)df-prstc 50580  prsthinc 50494
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50608  df-mndtc 50608
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50604
[Adamek] p. 25Definition 3.5df-oppc 17848
[Adamek] p. 25Example 3.6(1)oduoppcciso 50596
[Adamek] p. 25Example 3.6(2)oppgoppcco 50621  oppgoppchom 50620  oppgoppcid 50622
[Adamek] p. 28Remark 3.9oppciso 17918
[Adamek] p. 28Remark 3.12invf1o 17906  invisoinvl 17927
[Adamek] p. 28Example 3.13idinv 17926  idiso 17925
[Adamek] p. 28Corollary 3.11inveq 17911
[Adamek] p. 28Definition 3.8df-inv 17885  df-iso 17886  dfiso2 17909
[Adamek] p. 28Proposition 3.10sectcan 17892
[Adamek] p. 29Remark 3.16cicer 17943  cicerALT 50076
[Adamek] p. 29Definition 3.15cic 17936  df-cic 17933
[Adamek] p. 29Definition 3.17df-func 17995
[Adamek] p. 29Proposition 3.14(1)invinv 17907
[Adamek] p. 29Proposition 3.14(2)invco 17908  isoco 17914
[Adamek] p. 30Remark 3.19df-func 17995
[Adamek] p. 30Example 3.20(1)idfucl 18018
[Adamek] p. 30Example 3.20(2)diag1 50334
[Adamek] p. 32Proposition 3.21funciso 18011
[Adamek] p. 33Example 3.26(1)discsnterm 50604  discthing 50491
[Adamek] p. 33Example 3.26(2)df-thinc 50448  prsthinc 50494  thincciso 50483  thincciso2 50485  thincciso3 50486  thinccisod 50484
[Adamek] p. 33Example 3.26(3)df-mndtc 50608
[Adamek] p. 33Proposition 3.23cofucl 18025  cofucla 50126
[Adamek] p. 34Remark 3.28(1)cofidfth 50192
[Adamek] p. 34Remark 3.28(2)catciso 18248  catcisoi 50430
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18303
[Adamek] p. 34Definition 3.27(2)df-fth 18044
[Adamek] p. 34Definition 3.27(3)df-full 18043
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18303
[Adamek] p. 35Corollary 3.32ffthiso 18068
[Adamek] p. 35Proposition 3.30(c)cofth 18074
[Adamek] p. 35Proposition 3.30(d)cofull 18073
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18288
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18288
[Adamek] p. 39Remark 3.422oppf 50162
[Adamek] p. 39Definition 3.41df-oppf 50153  funcoppc 18012
[Adamek] p. 39Definition 3.44.df-catc 18236  elcatchom 50427
[Adamek] p. 39Proposition 3.43(c)fthoppc 18062  fthoppf 50194
[Adamek] p. 39Proposition 3.43(d)fulloppc 18061  fulloppf 50193
[Adamek] p. 40Remark 3.48catccat 18245
[Adamek] p. 40Definition 3.470funcg 50115  df-catc 18236
[Adamek] p. 45Exercise 3Gincat 50631
[Adamek] p. 48Remark 4.2(2)cnelsubc 50634  nelsubc3 50101
[Adamek] p. 48Remark 4.2(3)imasubc 50181  imasubc2 50182  imasubc3 50186
[Adamek] p. 48Example 4.3(1.a)0subcat 17975
[Adamek] p. 48Example 4.3(1.b)catsubcat 17976
[Adamek] p. 48Definition 4.1(1)nelsubc3 50101
[Adamek] p. 48Definition 4.1(2)fullsubc 17987
[Adamek] p. 48Definition 4.1(a)df-subc 17949
[Adamek] p. 49Remark 4.4idsubc 50190
[Adamek] p. 49Remark 4.4(1)idemb 50189
[Adamek] p. 49Remark 4.4(2)idfullsubc 50191  ressffth 18077
[Adamek] p. 58Exercise 4Asetc1onsubc 50632
[Adamek] p. 83Definition 6.1df-nat 18083
[Adamek] p. 87Remark 6.14(a)fuccocl 18104
[Adamek] p. 87Remark 6.14(b)fucass 18108
[Adamek] p. 87Definition 6.15df-fuc 18084
[Adamek] p. 88Remark 6.16fuccat 18110
[Adamek] p. 101Definition 7.10funcg 50115  df-inito 18121
[Adamek] p. 101Example 7.2(3)0funcg 50115  df-termc 50503  initc 50121
[Adamek] p. 101Example 7.2 (6)irinitoringc 21747
[Adamek] p. 102Definition 7.4df-termo 18122  oppctermo 50266
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18149
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18153
[Adamek] p. 103Remark 7.8oppczeroo 50267
[Adamek] p. 103Definition 7.7df-zeroo 18123
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21748
[Adamek] p. 103Proposition 7.6termoeu1w 18156
[Adamek] p. 106Definition 7.19df-sect 17884
[Adamek] p. 107Example 7.20(7)thincinv 50499
[Adamek] p. 108Example 7.25(4)thincsect2 50498
[Adamek] p. 110Example 7.33(9)thincmon 50463
[Adamek] p. 110Proposition 7.35sectmon 17919
[Adamek] p. 112Proposition 7.42sectepi 17921
[Adamek] p. 185Section 10.67updjud 9987
[Adamek] p. 193Definition 11.1(1)df-lmd 50675
[Adamek] p. 193Definition 11.3(1)df-lmd 50675
[Adamek] p. 194Definition 11.3(2)df-lmd 50675
[Adamek] p. 202Definition 11.27(1)df-cmd 50676
[Adamek] p. 202Definition 11.27(2)df-cmd 50676
[Adamek] p. 478Item Rngdf-ringc 20860
[AhoHopUll] p. 2Section 1.1df-bigo 49582
[AhoHopUll] p. 12Section 1.3df-blen 49604
[AhoHopUll] p. 318Section 9.1df-concat 14684  df-pfx 14789  df-substr 14757  df-word 14627  lencl 14646  wrd0 14652
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24989  df-nmoo 31281
[AkhiezerGlazman] p. 64Theoremhmopidmch 32689  hmopidmchi 32687
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32737  pjcmul2i 32738
[AkhiezerGlazman] p. 72Theoremcnvunop 32454  unoplin 32456
[AkhiezerGlazman] p. 72Equation 2unopadj 32455  unopadj2 32474
[AkhiezerGlazman] p. 73Theoremelunop2 32549  lnopunii 32548
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32622
[Alling] p. 125Theorem 4.02(12)cofcutrtime 28247
[Alling] p. 184Axiom Bbdayfo 27968
[Alling] p. 184Axiom Oltsso 27967
[Alling] p. 184Axiom SDnodense 27983
[Alling] p. 185Lemma 0nocvxmin 28075
[Alling] p. 185Theoremconway 28099
[Alling] p. 185Axiom FEnoeta 28034
[Alling] p. 186Theorem 4lesrec 28119  lesrecd 28120
[Alling], p. 2Definitionrp-brsslt 44367
[Alling], p. 3Notenla0001 44370  nla0002 44368  nla0003 44369
[Apostol] p. 18Theorem I.1addcan 11466  addcan2d 11486  addcan2i 11476  addcand 11485  addcani 11475
[Apostol] p. 18Theorem I.2negeu 11519
[Apostol] p. 18Theorem I.3negsub 11578  negsubd 11647  negsubi 11608
[Apostol] p. 18Theorem I.4negneg 11580  negnegd 11632  negnegi 11600
[Apostol] p. 18Theorem I.5subdi 11719  subdid 11742  subdii 11735  subdir 11720  subdird 11743  subdiri 11736
[Apostol] p. 18Theorem I.6mul01 11461  mul01d 11481  mul01i 11472  mul02 11460  mul02d 11480  mul02i 11471
[Apostol] p. 18Theorem I.7mulcan 11923  mulcan2d 11920  mulcand 11919  mulcani 11925
[Apostol] p. 18Theorem I.8receu 11931  xreceu 33422
[Apostol] p. 18Theorem I.9divrec 11960  divrecd 12066  divreci 12032  divreczi 12025
[Apostol] p. 18Theorem I.10recrec 11984  recreci 12019
[Apostol] p. 18Theorem I.11mul0or 11926  mul0ord 11934  mul0ori 11933
[Apostol] p. 18Theorem I.12mul2neg 11725  mul2negd 11741  mul2negi 11734  mulneg1 11722  mulneg1d 11739  mulneg1i 11732
[Apostol] p. 18Theorem I.13divadddiv 12002  divadddivd 12107  divadddivi 12049
[Apostol] p. 18Theorem I.14divmuldiv 11987  divmuldivd 12104  divmuldivi 12047  rdivmuldivd 20605
[Apostol] p. 18Theorem I.15divdivdiv 11988  divdivdivd 12110  divdivdivi 12050
[Apostol] p. 20Axiom 7rpaddcl 13114  rpaddcld 13149  rpmulcl 13115  rpmulcld 13150
[Apostol] p. 20Axiom 8rpneg 13124
[Apostol] p. 20Axiom 90nrp 13127
[Apostol] p. 20Theorem I.17lttri 11408
[Apostol] p. 20Theorem I.18ltadd1d 11879  ltadd1dd 11897  ltadd1i 11840
[Apostol] p. 20Theorem I.19ltmul1 12137  ltmul1a 12136  ltmul1i 12205  ltmul1ii 12215  ltmul2 12138  ltmul2d 13176  ltmul2dd 13190  ltmul2i 12208
[Apostol] p. 20Theorem I.20msqgt0 11806  msqgt0d 11853  msqgt0i 11823
[Apostol] p. 20Theorem I.210lt1 11808
[Apostol] p. 20Theorem I.23lt0neg1 11792  lt0neg1d 11855  ltneg 11786  ltnegd 11864  ltnegi 11830
[Apostol] p. 20Theorem I.25lt2add 11771  lt2addd 11909  lt2addi 11848
[Apostol] p. 20Definition of positive numbersdf-rp 13091
[Apostol] p. 21Exercise 4recgt0 12133  recgt0d 12221  recgt0i 12192  recgt0ii 12193
[Apostol] p. 22Definition of integersdf-z 12664
[Apostol] p. 22Definition of positive integersdfnn3 12319
[Apostol] p. 22Definition of rationalsdf-q 13046
[Apostol] p. 24Theorem I.26supeu 9424
[Apostol] p. 26Theorem I.28nnunb 12572
[Apostol] p. 26Theorem I.29arch 12573  archd 46098
[Apostol] p. 28Exercise 2btwnz 12772
[Apostol] p. 28Exercise 3nnrecl 12574
[Apostol] p. 28Exercise 4rebtwnz 13044
[Apostol] p. 28Exercise 5zbtwnre 13043
[Apostol] p. 28Exercise 6qbtwnre 13299
[Apostol] p. 28Exercise 10(a)zeneo 16477  zneo 12752  zneoALTV 48689
[Apostol] p. 29Theorem I.35cxpsqrtth 27022  msqsqrtd 15578  resqrtth 15390  sqrtth 15500  sqrtthi 15506  sqsqrtd 15577
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12308
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 13010
[Apostol] p. 361Remarkcrreczi 14340
[Apostol] p. 363Remarkabsgt0i 15535
[Apostol] p. 363Exampleabssubd 15591  abssubi 15539
[ApostolNT] p. 7Remarkfmtno0 48547  fmtno1 48548  fmtno2 48557  fmtno3 48558  fmtno4 48559  fmtno5fac 48589  fmtnofz04prm 48584
[ApostolNT] p. 7Definitiondf-fmtno 48535
[ApostolNT] p. 8Definitiondf-ppi 27391
[ApostolNT] p. 14Definitiondf-dvds 16391
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16407
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16432
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16427
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16420
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16422
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16408
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16409
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16414
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16449
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16451
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16453
[ApostolNT] p. 15Definitiondf-gcd 16633  dfgcd2 16684
[ApostolNT] p. 16Definitionisprm2 16820
[ApostolNT] p. 16Theorem 1.5coprmdvds 16791
[ApostolNT] p. 16Theorem 1.7prminf 17055
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16651
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16685
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16687
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16666
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16658
[ApostolNT] p. 17Theorem 1.8coprm 16850
[ApostolNT] p. 17Theorem 1.9euclemma 16852
[ApostolNT] p. 17Theorem 1.101arith2 17068
[ApostolNT] p. 18Theorem 1.13prmrec 17062
[ApostolNT] p. 19Theorem 1.14divalg 16541
[ApostolNT] p. 20Theorem 1.15eucalg 16725
[ApostolNT] p. 24Definitiondf-mu 27392
[ApostolNT] p. 25Definitiondf-phi 16905
[ApostolNT] p. 25Theorem 2.1musum 27482
[ApostolNT] p. 26Theorem 2.2phisum 16930
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16915
[ApostolNT] p. 28Theorem 2.5(c)phimul 16919
[ApostolNT] p. 32Definitiondf-vma 27389
[ApostolNT] p. 32Theorem 2.9muinv 27484
[ApostolNT] p. 32Theorem 2.10vmasum 27507
[ApostolNT] p. 38Remarkdf-sgm 27393
[ApostolNT] p. 38Definitiondf-sgm 27393
[ApostolNT] p. 75Definitiondf-chp 27390  df-cht 27388
[ApostolNT] p. 104Definitioncongr 16802
[ApostolNT] p. 106Remarkdvdsval3 16394
[ApostolNT] p. 106Definitionmoddvds 16401
[ApostolNT] p. 107Example 2mod2eq0even 16484
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16485
[ApostolNT] p. 107Example 4zmod1congr 13997
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 14037
[ApostolNT] p. 107Theorem 5.2(c)modexp 14350
[ApostolNT] p. 108Theorem 5.3modmulconst 16426
[ApostolNT] p. 109Theorem 5.4cncongr1 16805
[ApostolNT] p. 109Theorem 5.6gcdmodi 17214
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16807
[ApostolNT] p. 113Theorem 5.17eulerth 16922
[ApostolNT] p. 113Theorem 5.18vfermltl 16941
[ApostolNT] p. 114Theorem 5.19fermltl 16923
[ApostolNT] p. 116Theorem 5.24wilthimp 27363
[ApostolNT] p. 179Definitiondf-lgs 27586  lgsprme0 27630
[ApostolNT] p. 180Example 11lgs 27631
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27607
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27622
[ApostolNT] p. 181Theorem 9.4m1lgs 27679
[ApostolNT] p. 181Theorem 9.52lgs 27698  2lgsoddprm 27707
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27665
[ApostolNT] p. 185Theorem 9.8lgsquad 27674
[ApostolNT] p. 188Definitiondf-lgs 27586  lgs1 27632
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27623
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27625
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27633
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27634
[Baer] p. 40Property (b)mapdord 42615
[Baer] p. 40Property (c)mapd11 42616
[Baer] p. 40Property (e)mapdin 42639  mapdlsm 42641
[Baer] p. 40Property (f)mapd0 42642
[Baer] p. 40Definition of projectivitydf-mapd 42602  mapd1o 42625
[Baer] p. 41Property (g)mapdat 42644
[Baer] p. 44Part (1)mapdpg 42683
[Baer] p. 45Part (2)hdmap1eq 42778  mapdheq 42705  mapdheq2 42706  mapdheq2biN 42707
[Baer] p. 45Part (3)baerlem3 42690
[Baer] p. 46Part (4)mapdheq4 42709  mapdheq4lem 42708
[Baer] p. 46Part (5)baerlem5a 42691  baerlem5abmN 42695  baerlem5amN 42693  baerlem5b 42692  baerlem5bmN 42694
[Baer] p. 47Part (6)hdmap1l6 42798  hdmap1l6a 42786  hdmap1l6e 42791  hdmap1l6f 42792  hdmap1l6g 42793  hdmap1l6lem1 42784  hdmap1l6lem2 42785  mapdh6N 42724  mapdh6aN 42712  mapdh6eN 42717  mapdh6fN 42718  mapdh6gN 42719  mapdh6lem1N 42710  mapdh6lem2N 42711
[Baer] p. 48Part 9hdmapval 42805
[Baer] p. 48Part 10hdmap10 42817
[Baer] p. 48Part 11hdmapadd 42820
[Baer] p. 48Part (6)hdmap1l6h 42794  mapdh6hN 42720
[Baer] p. 48Part (7)mapdh75cN 42730  mapdh75d 42731  mapdh75e 42729  mapdh75fN 42732  mapdh7cN 42726  mapdh7dN 42727  mapdh7eN 42725  mapdh7fN 42728
[Baer] p. 48Part (8)mapdh8 42765  mapdh8a 42752  mapdh8aa 42753  mapdh8ab 42754  mapdh8ac 42755  mapdh8ad 42756  mapdh8b 42757  mapdh8c 42758  mapdh8d 42760  mapdh8d0N 42759  mapdh8e 42761  mapdh8g 42762  mapdh8i 42763  mapdh8j 42764
[Baer] p. 48Part (9)mapdh9a 42766
[Baer] p. 48Equation 10mapdhvmap 42746
[Baer] p. 49Part 12hdmap11 42825  hdmapeq0 42821  hdmapf1oN 42842  hdmapneg 42823  hdmaprnN 42841  hdmaprnlem1N 42826  hdmaprnlem3N 42827  hdmaprnlem3uN 42828  hdmaprnlem4N 42830  hdmaprnlem6N 42831  hdmaprnlem7N 42832  hdmaprnlem8N 42833  hdmaprnlem9N 42834  hdmapsub 42824
[Baer] p. 49Part 14hdmap14lem1 42845  hdmap14lem10 42854  hdmap14lem1a 42843  hdmap14lem2N 42846  hdmap14lem2a 42844  hdmap14lem3 42847  hdmap14lem8 42852  hdmap14lem9 42853
[Baer] p. 50Part 14hdmap14lem11 42855  hdmap14lem12 42856  hdmap14lem13 42857  hdmap14lem14 42858  hdmap14lem15 42859  hgmapval 42864
[Baer] p. 50Part 15hgmapadd 42871  hgmapmul 42872  hgmaprnlem2N 42874  hgmapvs 42868
[Baer] p. 50Part 16hgmaprnN 42878
[Baer] p. 110Lemma 1hdmapip0com 42894
[Baer] p. 110Line 27hdmapinvlem1 42895
[Baer] p. 110Line 28hdmapinvlem2 42896
[Baer] p. 110Line 30hdmapinvlem3 42897
[Baer] p. 110Part 1.2hdmapglem5 42899  hgmapvv 42903
[Baer] p. 110Proposition 1hdmapinvlem4 42898
[Baer] p. 111Line 10hgmapvvlem1 42900
[Baer] p. 111Line 15hdmapg 42907  hdmapglem7 42906
[Bauer], p. 483Theorem 1.22irrexpq 27023  2irrexpqALT 27092
[BellMachover] p. 36Lemma 10.3idALT 24
[BellMachover] p. 97Definition 10.1df-eu 2594
[BellMachover] p. 460Notationdf-mo 2564
[BellMachover] p. 460Definitionmo3 2589
[BellMachover] p. 461Axiom Extax-ext 2732
[BellMachover] p. 462Theorem 1.1axextmo 2736
[BellMachover] p. 463Axiom Repaxrep5 5238
[BellMachover] p. 463Scheme Sepax-sep 5248
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37899  sepex 5254
[BellMachover] p. 466Problemaxpow2 5328
[BellMachover] p. 466Axiom Powaxpow3 5329
[BellMachover] p. 466Axiom Unionaxun2 7736
[BellMachover] p. 468Definitiondf-ord 6354
[BellMachover] p. 469Theorem 2.2(i)ordirr 6369
[BellMachover] p. 469Theorem 2.2(iii)onelon 6376  onelond 36870
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6371
[BellMachover] p. 471Definition of Ndf-om 7861
[BellMachover] p. 471Problem 2.5(ii)uniordint 7798
[BellMachover] p. 471Definition of Limdf-lim 6356
[BellMachover] p. 472Axiom Infzfinf2 9621
[BellMachover] p. 473Theorem 2.8limom 7876
[BellMachover] p. 477Equation 3.1df-r1 9746
[BellMachover] p. 478Definitionrankval2 9800  rankval2b 9808
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9764  r1ord3g 9761
[BellMachover] p. 480Axiom Regzfreg 9568
[BellMachover] p. 488Axiom ACac5 10527  dfac4 10173
[BellMachover] p. 490Definition of alephalephval3 10161
[BeltramettiCassinelli] p. 98Remarkatlatmstc 40296
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32889
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32931  chirredi 32930
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32919
[Beran] p. 3Definition of joinsshjval3 31890
[Beran] p. 39Theorem 2.3(i)cmcm2 32152  cmcm2i 32129  cmcm2ii 32134  cmt2N 40227
[Beran] p. 40Theorem 2.3(iii)lecm 32153  lecmi 32138  lecmii 32139
[Beran] p. 45Theorem 3.4cmcmlem 32127
[Beran] p. 49Theorem 4.2cm2j 32156  cm2ji 32161  cm2mi 32162
[Beran] p. 95Definitiondf-sh 31743  issh2 31745
[Beran] p. 95Lemma 3.1(S5)his5 31622
[Beran] p. 95Lemma 3.1(S6)his6 31635
[Beran] p. 95Lemma 3.1(S7)his7 31626
[Beran] p. 95Lemma 3.2(S8)ho01i 32364
[Beran] p. 95Lemma 3.2(S9)hoeq1 32366
[Beran] p. 95Lemma 3.2(S10)ho02i 32365
[Beran] p. 95Lemma 3.2(S11)hoeq2 32367
[Beran] p. 95Postulate (S1)ax-his1 31618  his1i 31636
[Beran] p. 95Postulate (S2)ax-his2 31619
[Beran] p. 95Postulate (S3)ax-his3 31620
[Beran] p. 95Postulate (S4)ax-his4 31621
[Beran] p. 96Definition of normdf-hnorm 31504  dfhnorm2 31658  normval 31660
[Beran] p. 96Definition for Cauchy sequencehcau 31720
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31509
[Beran] p. 96Definition of complete subspaceisch3 31777
[Beran] p. 96Definition of convergedf-hlim 31508  hlimi 31724
[Beran] p. 97Theorem 3.3(i)norm-i-i 31669  norm-i 31665
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31673  norm-ii 31674  normlem0 31645  normlem1 31646  normlem2 31647  normlem3 31648  normlem4 31649  normlem5 31650  normlem6 31651  normlem7 31652  normlem7tALT 31655
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31675  norm-iii 31676
[Beran] p. 98Remark 3.4bcs 31717  bcsiALT 31715  bcsiHIL 31716
[Beran] p. 98Remark 3.4(B)normlem9at 31657  normpar 31691  normpari 31690
[Beran] p. 98Remark 3.4(C)normpyc 31682  normpyth 31681  normpythi 31678
[Beran] p. 99Remarklnfn0 32583  lnfn0i 32578  lnop0 32502  lnop0i 32506
[Beran] p. 99Theorem 3.5(i)nmcexi 32562  nmcfnex 32589  nmcfnexi 32587  nmcopex 32565  nmcopexi 32563
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32590  nmcfnlbi 32588  nmcoplb 32566  nmcoplbi 32564
[Beran] p. 99Theorem 3.5(iii)lnfncon 32592  lnfnconi 32591  lnopcon 32571  lnopconi 32570
[Beran] p. 100Lemma 3.6normpar2i 31692
[Beran] p. 101Lemma 3.6norm3adifi 31689  norm3adifii 31684  norm3dif 31686  norm3difi 31683
[Beran] p. 102Theorem 3.7(i)chocunii 31837  pjhth 31929  pjhtheu 31930  pjpjhth 31961  pjpjhthi 31962  pjth 25722
[Beran] p. 102Theorem 3.7(ii)ococ 31942  ococi 31941
[Beran] p. 103Remark 3.8nlelchi 32597
[Beran] p. 104Theorem 3.9riesz3i 32598  riesz4 32600  riesz4i 32599
[Beran] p. 104Theorem 3.10cnlnadj 32615  cnlnadjeu 32614  cnlnadjeui 32613  cnlnadji 32612  cnlnadjlem1 32603  nmopadjlei 32624
[Beran] p. 106Theorem 3.11(i)adjeq0 32627
[Beran] p. 106Theorem 3.11(v)nmopadji 32626
[Beran] p. 106Theorem 3.11(ii)adjmul 32628
[Beran] p. 106Theorem 3.11(iv)adjadj 32472
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32638  nmopcoadji 32637
[Beran] p. 106Theorem 3.11(iii)adjadd 32629
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32639
[Beran] p. 106Theorem 3.11(viii)adjcoi 32636  pjadj2coi 32740  pjadjcoi 32697
[Beran] p. 107Definitiondf-ch 31757  isch2 31759
[Beran] p. 107Remark 3.12choccl 31842  isch3 31777  occl 31840  ocsh 31819  shoccl 31841  shocsh 31820
[Beran] p. 107Remark 3.12(B)ococin 31944
[Beran] p. 108Theorem 3.13chintcl 31868
[Beran] p. 109Property (i)pjadj2 32723  pjadj3 32724  pjadji 32221  pjadjii 32210
[Beran] p. 109Property (ii)pjidmco 32717  pjidmcoi 32713  pjidmi 32209
[Beran] p. 110Definition of projector orderingpjordi 32709
[Beran] p. 111Remarkho0val 32286  pjch1 32206
[Beran] p. 111Definitiondf-hfmul 32270  df-hfsum 32269  df-hodif 32268  df-homul 32267  df-hosum 32266
[Beran] p. 111Lemma 4.4(i)pjo 32207
[Beran] p. 111Lemma 4.4(ii)pjch 32230  pjchi 31968
[Beran] p. 111Lemma 4.4(iii)pjoc2 31975  pjoc2i 31974
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 32216
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32701  pjssmii 32217
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32700
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32699
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32704
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32702  pjssge0ii 32218
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32703  pjdifnormii 32219
[Bobzien] p. 116Statement T3stoic3 1809
[Bobzien] p. 117Statement T2stoic2a 1807
[Bobzien] p. 117Statement T4stoic4a 1810
[Bobzien] p. 117Conclusion the contradictorystoic1a 1805
[Bogachev] p. 16Definition 1.5df-oms 34859
[Bogachev] p. 17Lemma 1.5.4omssubadd 34867
[Bogachev] p. 17Example 1.5.2omsmon 34865
[Bogachev] p. 41Definition 1.11.2df-carsg 34869
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34889
[Bogachev] p. 116Definition 2.3.1df-itgm 34920  df-sitm 34898
[Bogachev] p. 118Chapter 2.4.4df-itgm 34920
[Bogachev] p. 118Definition 2.4.1df-sitg 34897
[Bollobas] p. 1Section I.1df-edg 29560  isuhgrop 29582  isusgrop 29677  isuspgrop 29676
[Bollobas] p. 2Section I.1df-isubgr 48881  df-subgr 29783  uhgrspan1 29818  uhgrspansubgr 29806
[Bollobas] p. 3Definitiondf-gric 48901  gricuspgr 48938  isuspgrim 48916
[Bollobas] p. 3Section I.1cusgrsize 29969  df-clnbgr 48839  df-cusgr 29927  df-nbgr 29848  fusgrmaxsize 29979
[Bollobas] p. 4Definitiondf-upwlks 49154  df-wlks 30114
[Bollobas] p. 4Section I.1finsumvtxdg2size 30065  finsumvtxdgeven 30067  fusgr1th 30066  fusgrvtxdgonume 30069  vtxdgoddnumeven 30068
[Bollobas] p. 5Notationdf-pths 30233
[Bollobas] p. 5Definitiondf-crcts 30307  df-cycls 30308  df-trls 30209  df-wlkson 30115
[Bollobas] p. 7Section I.1df-ushgr 29571
[BourbakiAlg1] p. 1Definition 1df-clintop 49219  df-cllaw 49205  df-mgm 18778  df-mgm2 49238
[BourbakiAlg1] p. 4Definition 5df-assintop 49220  df-asslaw 49207  df-sgrp 18870  df-sgrp2 49240
[BourbakiAlg1] p. 7Definition 8df-cmgm2 49239  df-comlaw 49206
[BourbakiAlg1] p. 12Definition 2df-mnd 18886
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33521  mndlactf1o 33525  mndractf1 33523  mndractf1o 33526
[BourbakiAlg1] p. 92Definition 1df-ring 20423
[BourbakiAlg1] p. 93Section I.8.1df-rng 20337
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 34199
[BourbakiAlg2] p. 113Chapter 5.assafld 34203  assarrginv 34202
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 34244  fldextrspunfld 34242  fldextrspunlem1 34241  fldextrspunlem2 34243  fldextrspunlsp 34240  fldextrspunlsplem 34239
[BourbakiCAlg2], p. 228Proposition 21arithidom 34003  dfufd2 34016
[BourbakiEns] p. Proposition 8fcof1 7283  fcofo 7284
[BourbakiTop1] p. Remarkxnegmnf 13310  xnegpnf 13309
[BourbakiTop1] p. Remark rexneg 13311
[BourbakiTop1] p. Remark 3ust0 24501  ustfilxp 24494
[BourbakiTop1] p. Axiom GT'tgpsubcn 24371
[BourbakiTop1] p. Criterionishmeo 24040
[BourbakiTop1] p. Example 1cstucnd 24564  iducn 24563  snfil 24145
[BourbakiTop1] p. Example 2neifil 24161
[BourbakiTop1] p. Theorem 1cnextcn 24348
[BourbakiTop1] p. Theorem 2ucnextcn 24584
[BourbakiTop1] p. Theorem 3df-hcmp 34523
[BourbakiTop1] p. Paragraph 3infil 24144
[BourbakiTop1] p. Definition 1df-ucn 24556  df-ust 24482  filintn0 24142  filn0 24143  istgp 24358  ucnprima 24562
[BourbakiTop1] p. Definition 2df-cfilu 24567
[BourbakiTop1] p. Definition 3df-cusp 24578  df-usp 24538  df-utop 24512  trust 24510
[BourbakiTop1] p. Definition 6df-pcmp 34422
[BourbakiTop1] p. Property V_issnei2 23396
[BourbakiTop1] p. Theorem 1(d)iscncl 23549
[BourbakiTop1] p. Condition F_Iustssel 24487
[BourbakiTop1] p. Condition U_Iustdiag 24490
[BourbakiTop1] p. Property V_iiinnei 23405
[BourbakiTop1] p. Property V_ivneiptopreu 23413  neissex 23407
[BourbakiTop1] p. Proposition 1neips 23393  neiss 23389  ucncn 24565  ustund 24503  ustuqtop 24527
[BourbakiTop1] p. Proposition 2cnpco 23547  neiptopreu 23413  utop2nei 24531  utop3cls 24532
[BourbakiTop1] p. Proposition 3fmucnd 24572  uspreg 24554  utopreg 24533
[BourbakiTop1] p. Proposition 4imasncld 23972  imasncls 23973  imasnopn 23971
[BourbakiTop1] p. Proposition 9cnpflf2 24281
[BourbakiTop1] p. Condition F_IIustincl 24489
[BourbakiTop1] p. Condition U_IIustinvel 24491
[BourbakiTop1] p. Property V_iiielnei 23391
[BourbakiTop1] p. Proposition 11cnextucn 24583
[BourbakiTop1] p. Condition F_IIbustbasel 24488
[BourbakiTop1] p. Condition U_IIIustexhalf 24492
[BourbakiTop1] p. Definition C'''df-cmp 23667
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 24127
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 23174
[BourbakiTop2] p. 195Definition 1df-ldlf 34419
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46994
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46996  stoweid 46995
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46933  stoweidlem10 46942  stoweidlem14 46946  stoweidlem15 46947  stoweidlem35 46967  stoweidlem36 46968  stoweidlem37 46969  stoweidlem38 46970  stoweidlem40 46972  stoweidlem41 46973  stoweidlem43 46975  stoweidlem44 46976  stoweidlem46 46978  stoweidlem5 46937  stoweidlem50 46982  stoweidlem52 46984  stoweidlem53 46985  stoweidlem55 46987  stoweidlem56 46988
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46955  stoweidlem24 46956  stoweidlem27 46959  stoweidlem28 46960  stoweidlem30 46962
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46966  stoweidlem59 46991  stoweidlem60 46992
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46977  stoweidlem49 46981  stoweidlem7 46939
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46963  stoweidlem39 46971  stoweidlem42 46974  stoweidlem48 46980  stoweidlem51 46983  stoweidlem54 46986  stoweidlem57 46989  stoweidlem58 46990
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46957
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46949
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46943  stoweidlem13 46945  stoweidlem26 46958  stoweidlem61 46993
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46950
[Bruck] p. 1Section I.1df-clintop 49219  df-mgm 18778  df-mgm2 49238
[Bruck] p. 23Section II.1df-sgrp 18870  df-sgrp2 49240
[Bruck] p. 28Theorem 3.2dfgrp3 19211
[ChoquetDD] p. 2Definition of mappingdf-mpt 5186
[Church] p. 129Section II.24df-ifp 1079  dfifp2 1080
[Clemente] p. 10Definition ITnatded 30938
[Clemente] p. 10Definition I` `m,nnatded 30938
[Clemente] p. 11Definition E=>m,nnatded 30938
[Clemente] p. 11Definition I=>m,nnatded 30938
[Clemente] p. 11Definition E` `(1)natded 30938
[Clemente] p. 11Definition E` `(2)natded 30938
[Clemente] p. 12Definition E` `m,n,pnatded 30938
[Clemente] p. 12Definition I` `n(1)natded 30938
[Clemente] p. 12Definition I` `n(2)natded 30938
[Clemente] p. 13Definition I` `m,n,pnatded 30938
[Clemente] p. 14Proof 5.11natded 30938
[Clemente] p. 14Definition E` `nnatded 30938
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30940  ex-natded5.2 30939
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30943  ex-natded5.3 30942
[Clemente] p. 18Theorem 5.5ex-natded5.5 30945
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30947  ex-natded5.7 30946
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30949  ex-natded5.8 30948
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30951  ex-natded5.13 30950
[Clemente] p. 32Definition I` `nnatded 30938
[Clemente] p. 32Definition E` `m,n,p,anatded 30938
[Clemente] p. 32Definition E` `n,tnatded 30938
[Clemente] p. 32Definition I` `n,tnatded 30938
[Clemente] p. 43Theorem 9.20ex-natded9.20 30952
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30953
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30955  ex-natded9.26 30954
[Cohen] p. 301Remarkrelogoprlem 26883
[Cohen] p. 301Property 2relogmul 26884  relogmuld 26917
[Cohen] p. 301Property 3relogdiv 26885  relogdivd 26918
[Cohen] p. 301Property 4relogexp 26888
[Cohen] p. 301Property 1alog1 26877
[Cohen] p. 301Property 1bloge 26878
[Cohen4] p. 348Observationrelogbcxpb 27079
[Cohen4] p. 349Propertyrelogbf 27083
[Cohen4] p. 352Definitionelogb 27062
[Cohen4] p. 361Property 2relogbmul 27069
[Cohen4] p. 361Property 3logbrec 27074  relogbdiv 27071
[Cohen4] p. 361Property 4relogbreexp 27067
[Cohen4] p. 361Property 6relogbexp 27072
[Cohen4] p. 361Property 1(a)logbid1 27060
[Cohen4] p. 361Property 1(b)logb1 27061
[Cohen4] p. 367Propertylogbchbase 27063
[Cohen4] p. 377Property 2logblt 27076
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34852  sxbrsigalem4 34854
[Cohn] p. 81Section II.5acsdomd 18693  acsinfd 18692  acsinfdimd 18694  acsmap2d 18691  acsmapd 18690
[Cohn] p. 143Example 5.1.1sxbrsiga 34857
[Connell] p. 57Definitiondf-scmat 22768  df-scmatalt 49433
[Conway] p. 4Definitionlesrec 28119  lesrecd 28120
[Conway] p. 5Definitionaddsval 28282  addsval2 28283  df-adds 28280  df-muls 28427  df-negs 28341
[Conway] p. 7Theorem0lt1s 28132
[Conway] p. 12Theorem 12pw2cut2 28782
[Conway] p. 16Theorem 0(i)sltsright 28181
[Conway] p. 16Theorem 0(ii)sltsleft 28180
[Conway] p. 16Theorem 0(iii)lesid 28058
[Conway] p. 17Theorem 3addsass 28325  addsassd 28326  addscom 28286  addscomd 28287  addsrid 28284  addsridd 28285
[Conway] p. 17Definitiondf-0s 28127
[Conway] p. 17Theorem 4(ii)negnegs 28364
[Conway] p. 17Theorem 4(iii)negsid 28361  negsidd 28362
[Conway] p. 18Theorem 5leadds1 28309  leadds1d 28315
[Conway] p. 18Definitiondf-1s 28128
[Conway] p. 18Theorem 6(ii)negscl 28356  negscld 28357
[Conway] p. 18Theorem 6(iii)addscld 28300
[Conway] p. 19Notemulsunif2 28490
[Conway] p. 19Theorem 7addsdi 28475  addsdid 28476  addsdird 28477  mulnegs1d 28480  mulnegs2d 28481  mulsass 28486  mulsassd 28487  mulscom 28459  mulscomd 28460
[Conway] p. 19Theorem 8(i)mulscl 28454  mulscld 28455
[Conway] p. 19Theorem 8(iii)lemulsd 28458  ltmuls 28456  ltmulsd 28457
[Conway] p. 20Theorem 9mulsgt0 28464  mulsgt0d 28465
[Conway] p. 21Theorem 10(iv)precsex 28538
[Conway] p. 23Theorem 11eqcuts3 28124
[Conway] p. 24Definitiondf-reno 28810
[Conway] p. 24Theorem 13(ii)readdscl 28819  remulscl 28822  renegscl 28818
[Conway] p. 27Definitiondf-ons 28572  elons2 28578
[Conway] p. 27Theorem 14ltonsex 28582
[Conway] p. 28Theorem 15oncutlt 28584  onswe 28592
[Conway] p. 29Remarkmadebday 28220  newbday 28222  oldbday 28221
[Conway] p. 29Definitiondf-made 28147  df-new 28149  df-old 28148
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13970
[Crawley] p. 1Definition of posetdf-poset 18449
[Crawley] p. 107Theorem 13.2hlsupr 40363
[Crawley] p. 110Theorem 13.3arglem1N 41167  dalaw 40863
[Crawley] p. 111Theorem 13.4hlathil 42938
[Crawley] p. 111Definition of set Wdf-watsN 40967
[Crawley] p. 111Definition of dilationdf-dilN 41083  df-ldil 41081  isldil 41087
[Crawley] p. 111Definition of translationdf-ltrn 41082  df-trnN 41084  isltrn 41096  ltrnu 41098
[Crawley] p. 112Lemma Acdlema1N 40768  cdlema2N 40769  exatleN 40381
[Crawley] p. 112Lemma B1cvrat 40453  cdlemb 40771  cdlemb2 41018  cdlemb3 41583  idltrn 41127  l1cvat 40032  lhpat 41020  lhpat2 41022  lshpat 40033  ltrnel 41116  ltrnmw 41128
[Crawley] p. 112Lemma Ccdlemc1 41168  cdlemc2 41169  ltrnnidn 41151  trlat 41146  trljat1 41143  trljat2 41144  trljat3 41145  trlne 41162  trlnidat 41150  trlnle 41163
[Crawley] p. 112Definition of automorphismdf-pautN 40968
[Crawley] p. 113Lemma Ccdlemc 41174  cdlemc3 41170  cdlemc4 41171
[Crawley] p. 113Lemma Dcdlemd 41184  cdlemd1 41175  cdlemd2 41176  cdlemd3 41177  cdlemd4 41178  cdlemd5 41179  cdlemd6 41180  cdlemd7 41181  cdlemd8 41182  cdlemd9 41183  cdleme31sde 41362  cdleme31se 41359  cdleme31se2 41360  cdleme31snd 41363  cdleme32a 41418  cdleme32b 41419  cdleme32c 41420  cdleme32d 41421  cdleme32e 41422  cdleme32f 41423  cdleme32fva 41414  cdleme32fva1 41415  cdleme32fvcl 41417  cdleme32le 41424  cdleme48fv 41476  cdleme4gfv 41484  cdleme50eq 41518  cdleme50f 41519  cdleme50f1 41520  cdleme50f1o 41523  cdleme50laut 41524  cdleme50ldil 41525  cdleme50lebi 41517  cdleme50rn 41522  cdleme50rnlem 41521  cdlemeg49le 41488  cdlemeg49lebilem 41516
[Crawley] p. 113Lemma Ecdleme 41537  cdleme00a 41186  cdleme01N 41198  cdleme02N 41199  cdleme0a 41188  cdleme0aa 41187  cdleme0b 41189  cdleme0c 41190  cdleme0cp 41191  cdleme0cq 41192  cdleme0dN 41193  cdleme0e 41194  cdleme0ex1N 41200  cdleme0ex2N 41201  cdleme0fN 41195  cdleme0gN 41196  cdleme0moN 41202  cdleme1 41204  cdleme10 41231  cdleme10tN 41235  cdleme11 41247  cdleme11a 41237  cdleme11c 41238  cdleme11dN 41239  cdleme11e 41240  cdleme11fN 41241  cdleme11g 41242  cdleme11h 41243  cdleme11j 41244  cdleme11k 41245  cdleme11l 41246  cdleme12 41248  cdleme13 41249  cdleme14 41250  cdleme15 41255  cdleme15a 41251  cdleme15b 41252  cdleme15c 41253  cdleme15d 41254  cdleme16 41262  cdleme16aN 41236  cdleme16b 41256  cdleme16c 41257  cdleme16d 41258  cdleme16e 41259  cdleme16f 41260  cdleme16g 41261  cdleme19a 41280  cdleme19b 41281  cdleme19c 41282  cdleme19d 41283  cdleme19e 41284  cdleme19f 41285  cdleme1b 41203  cdleme2 41205  cdleme20aN 41286  cdleme20bN 41287  cdleme20c 41288  cdleme20d 41289  cdleme20e 41290  cdleme20f 41291  cdleme20g 41292  cdleme20h 41293  cdleme20i 41294  cdleme20j 41295  cdleme20k 41296  cdleme20l 41299  cdleme20l1 41297  cdleme20l2 41298  cdleme20m 41300  cdleme20y 41279  cdleme20zN 41278  cdleme21 41314  cdleme21d 41307  cdleme21e 41308  cdleme22a 41317  cdleme22aa 41316  cdleme22b 41318  cdleme22cN 41319  cdleme22d 41320  cdleme22e 41321  cdleme22eALTN 41322  cdleme22f 41323  cdleme22f2 41324  cdleme22g 41325  cdleme23a 41326  cdleme23b 41327  cdleme23c 41328  cdleme26e 41336  cdleme26eALTN 41338  cdleme26ee 41337  cdleme26f 41340  cdleme26f2 41342  cdleme26f2ALTN 41341  cdleme26fALTN 41339  cdleme27N 41346  cdleme27a 41344  cdleme27cl 41343  cdleme28c 41349  cdleme3 41214  cdleme30a 41355  cdleme31fv 41367  cdleme31fv1 41368  cdleme31fv1s 41369  cdleme31fv2 41370  cdleme31id 41371  cdleme31sc 41361  cdleme31sdnN 41364  cdleme31sn 41357  cdleme31sn1 41358  cdleme31sn1c 41365  cdleme31sn2 41366  cdleme31so 41356  cdleme35a 41425  cdleme35b 41427  cdleme35c 41428  cdleme35d 41429  cdleme35e 41430  cdleme35f 41431  cdleme35fnpq 41426  cdleme35g 41432  cdleme35h 41433  cdleme35h2 41434  cdleme35sn2aw 41435  cdleme35sn3a 41436  cdleme36a 41437  cdleme36m 41438  cdleme37m 41439  cdleme38m 41440  cdleme38n 41441  cdleme39a 41442  cdleme39n 41443  cdleme3b 41206  cdleme3c 41207  cdleme3d 41208  cdleme3e 41209  cdleme3fN 41210  cdleme3fa 41213  cdleme3g 41211  cdleme3h 41212  cdleme4 41215  cdleme40m 41444  cdleme40n 41445  cdleme40v 41446  cdleme40w 41447  cdleme41fva11 41454  cdleme41sn3aw 41451  cdleme41sn4aw 41452  cdleme41snaw 41453  cdleme42a 41448  cdleme42b 41455  cdleme42c 41449  cdleme42d 41450  cdleme42e 41456  cdleme42f 41457  cdleme42g 41458  cdleme42h 41459  cdleme42i 41460  cdleme42k 41461  cdleme42ke 41462  cdleme42keg 41463  cdleme42mN 41464  cdleme42mgN 41465  cdleme43aN 41466  cdleme43bN 41467  cdleme43cN 41468  cdleme43dN 41469  cdleme5 41217  cdleme50ex 41536  cdleme50ltrn 41534  cdleme51finvN 41533  cdleme51finvfvN 41532  cdleme51finvtrN 41535  cdleme6 41218  cdleme7 41226  cdleme7a 41220  cdleme7aa 41219  cdleme7b 41221  cdleme7c 41222  cdleme7d 41223  cdleme7e 41224  cdleme7ga 41225  cdleme8 41227  cdleme8tN 41232  cdleme9 41230  cdleme9a 41228  cdleme9b 41229  cdleme9tN 41234  cdleme9taN 41233  cdlemeda 41275  cdlemedb 41274  cdlemednpq 41276  cdlemednuN 41277  cdlemefr27cl 41380  cdlemefr32fva1 41387  cdlemefr32fvaN 41386  cdlemefrs32fva 41377  cdlemefrs32fva1 41378  cdlemefs27cl 41390  cdlemefs32fva1 41400  cdlemefs32fvaN 41399  cdlemesner 41273  cdlemeulpq 41197
[Crawley] p. 114Lemma E4atex 41053  4atexlem7 41052  cdleme0nex 41267  cdleme17a 41263  cdleme17c 41265  cdleme17d 41475  cdleme17d1 41266  cdleme17d2 41472  cdleme18a 41268  cdleme18b 41269  cdleme18c 41270  cdleme18d 41272  cdleme4a 41216
[Crawley] p. 115Lemma Ecdleme21a 41302  cdleme21at 41305  cdleme21b 41303  cdleme21c 41304  cdleme21ct 41306  cdleme21f 41309  cdleme21g 41310  cdleme21h 41311  cdleme21i 41312  cdleme22gb 41271
[Crawley] p. 116Lemma Fcdlemf 41540  cdlemf1 41538  cdlemf2 41539
[Crawley] p. 116Lemma Gcdlemftr1 41544  cdlemg16 41634  cdlemg28 41681  cdlemg28a 41670  cdlemg28b 41680  cdlemg3a 41574  cdlemg42 41706  cdlemg43 41707  cdlemg44 41710  cdlemg44a 41708  cdlemg46 41712  cdlemg47 41713  cdlemg9 41611  ltrnco 41696  ltrncom 41715  tgrpabl 41728  trlco 41704
[Crawley] p. 116Definition of Gdf-tgrp 41720
[Crawley] p. 117Lemma Gcdlemg17 41654  cdlemg17b 41639
[Crawley] p. 117Definition of Edf-edring-rN 41733  df-edring 41734
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41737
[Crawley] p. 118Remarktendopltp 41757
[Crawley] p. 118Lemma Hcdlemh 41794  cdlemh1 41792  cdlemh2 41793
[Crawley] p. 118Lemma Icdlemi 41797  cdlemi1 41795  cdlemi2 41796
[Crawley] p. 118Lemma Jcdlemj1 41798  cdlemj2 41799  cdlemj3 41800  tendocan 41801
[Crawley] p. 118Lemma Kcdlemk 41951  cdlemk1 41808  cdlemk10 41820  cdlemk11 41826  cdlemk11t 41923  cdlemk11ta 41906  cdlemk11tb 41908  cdlemk11tc 41922  cdlemk11u-2N 41866  cdlemk11u 41848  cdlemk12 41827  cdlemk12u-2N 41867  cdlemk12u 41849  cdlemk13-2N 41853  cdlemk13 41829  cdlemk14-2N 41855  cdlemk14 41831  cdlemk15-2N 41856  cdlemk15 41832  cdlemk16-2N 41857  cdlemk16 41834  cdlemk16a 41833  cdlemk17-2N 41858  cdlemk17 41835  cdlemk18-2N 41863  cdlemk18-3N 41877  cdlemk18 41845  cdlemk19-2N 41864  cdlemk19 41846  cdlemk19u 41947  cdlemk1u 41836  cdlemk2 41809  cdlemk20-2N 41869  cdlemk20 41851  cdlemk21-2N 41868  cdlemk21N 41850  cdlemk22-3 41878  cdlemk22 41870  cdlemk23-3 41879  cdlemk24-3 41880  cdlemk25-3 41881  cdlemk26-3 41883  cdlemk26b-3 41882  cdlemk27-3 41884  cdlemk28-3 41885  cdlemk29-3 41888  cdlemk3 41810  cdlemk30 41871  cdlemk31 41873  cdlemk32 41874  cdlemk33N 41886  cdlemk34 41887  cdlemk35 41889  cdlemk36 41890  cdlemk37 41891  cdlemk38 41892  cdlemk39 41893  cdlemk39u 41945  cdlemk4 41811  cdlemk41 41897  cdlemk42 41918  cdlemk42yN 41921  cdlemk43N 41940  cdlemk45 41924  cdlemk46 41925  cdlemk47 41926  cdlemk48 41927  cdlemk49 41928  cdlemk5 41813  cdlemk50 41929  cdlemk51 41930  cdlemk52 41931  cdlemk53 41934  cdlemk54 41935  cdlemk55 41938  cdlemk55u 41943  cdlemk56 41948  cdlemk5a 41812  cdlemk5auN 41837  cdlemk5u 41838  cdlemk6 41814  cdlemk6u 41839  cdlemk7 41825  cdlemk7u-2N 41865  cdlemk7u 41847  cdlemk8 41815  cdlemk9 41816  cdlemk9bN 41817  cdlemki 41818  cdlemkid 41913  cdlemkj-2N 41859  cdlemkj 41840  cdlemksat 41823  cdlemksel 41822  cdlemksv 41821  cdlemksv2 41824  cdlemkuat 41843  cdlemkuel-2N 41861  cdlemkuel-3 41875  cdlemkuel 41842  cdlemkuv-2N 41860  cdlemkuv2-2 41862  cdlemkuv2-3N 41876  cdlemkuv2 41844  cdlemkuvN 41841  cdlemkvcl 41819  cdlemky 41903  cdlemkyyN 41939  tendoex 41952
[Crawley] p. 120Remarkdva1dim 41962
[Crawley] p. 120Lemma Lcdleml1N 41953  cdleml2N 41954  cdleml3N 41955  cdleml4N 41956  cdleml5N 41957  cdleml6 41958  cdleml7 41959  cdleml8 41960  cdleml9 41961  dia1dim 42038
[Crawley] p. 120Lemma Mdia11N 42025  diaf11N 42026  dialss 42023  diaord 42024  dibf11N 42138  djajN 42114
[Crawley] p. 120Definition of isomorphism mapdiaval 42009
[Crawley] p. 121Lemma Mcdlemm10N 42095  dia2dimlem1 42041  dia2dimlem2 42042  dia2dimlem3 42043  dia2dimlem4 42044  dia2dimlem5 42045  diaf1oN 42107  diarnN 42106  dvheveccl 42089  dvhopN 42093
[Crawley] p. 121Lemma Ncdlemn 42189  cdlemn10 42183  cdlemn11 42188  cdlemn11a 42184  cdlemn11b 42185  cdlemn11c 42186  cdlemn11pre 42187  cdlemn2 42172  cdlemn2a 42173  cdlemn3 42174  cdlemn4 42175  cdlemn4a 42176  cdlemn5 42178  cdlemn5pre 42177  cdlemn6 42179  cdlemn7 42180  cdlemn8 42181  cdlemn9 42182  diclspsn 42171
[Crawley] p. 121Definition of phi(q)df-dic 42150
[Crawley] p. 122Lemma Ndih11 42242  dihf11 42244  dihjust 42194  dihjustlem 42193  dihord 42241  dihord1 42195  dihord10 42200  dihord11b 42199  dihord11c 42201  dihord2 42204  dihord2a 42196  dihord2b 42197  dihord2cN 42198  dihord2pre 42202  dihord2pre2 42203  dihordlem6 42190  dihordlem7 42191  dihordlem7b 42192
[Crawley] p. 122Definition of isomorphism mapdihffval 42207  dihfval 42208  dihval 42209
[Diestel] p. 3Definitiondf-gric 48901  df-grim 48898  isuspgrim 48916
[Diestel] p. 3Section 1.1df-cusgr 29927  df-nbgr 29848
[Diestel] p. 3Definition by df-grisom 48897
[Diestel] p. 4Section 1.1df-isubgr 48881  df-subgr 29783  uhgrspan1 29818  uhgrspansubgr 29806
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 30069  vtxdgoddnumeven 30068
[Diestel] p. 27Section 1.10df-ushgr 29571
[EGA] p. 80Notation 1.1.1rspecval 34430
[EGA] p. 80Proposition 1.1.2zartop 34442
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34434  zarcls1 34435
[EGA] p. 81Corollary 1.1.8zart0 34445
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34448
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34451
[Eisenberg] p. 67Definition 5.3df-dif 3901
[Eisenberg] p. 82Definition 6.3dfom3 9626
[Eisenberg] p. 125Definition 8.21df-map 8827
[Eisenberg] p. 216Example 13.2(4)omenps 9634
[Eisenberg] p. 310Theorem 19.8cardprc 10033
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10611
[Enderton] p. 18Axiom of Empty Setaxnul 5258
[Enderton] p. 19Definitiondf-tp 4588
[Enderton] p. 26Exercise 5unissb 4900
[Enderton] p. 26Exercise 10pwel 5342
[Enderton] p. 28Exercise 7(b)pwun 5540
[Enderton] p. 30Theorem "Distributive laws"iinin1 5038  iinin2 5037  iinun2 5030  iunin1 5029  iunin1f 33086  iunin2 5028  uniin1 5032  uniin2 5033
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5036  iundif2 5031
[Enderton] p. 32Exercise 20unineq 4233
[Enderton] p. 33Exercise 23iinuni 5057
[Enderton] p. 33Exercise 25iununi 5058
[Enderton] p. 33Exercise 24(a)iinpw 5065
[Enderton] p. 33Exercise 24(b)iunpw 7768  iunpwss 5066
[Enderton] p. 36Definitionopthwiener 5483
[Enderton] p. 38Exercise 6(a)unipw 5417
[Enderton] p. 38Exercise 6(b)pwuni 4905
[Enderton] p. 41Lemma 3Dopeluu 5438  rnex 7905  rnexg 7897
[Enderton] p. 41Exercise 8dmuni 5892  rnuni 6134
[Enderton] p. 42Definition of a functiondffun7 6555  dffun8 6556
[Enderton] p. 43Definition of function valuefunfv2 6961
[Enderton] p. 43Definition of single-rootedfuncnv 6597
[Enderton] p. 44Definition (d)dfima2 6052  dfima3 6053
[Enderton] p. 47Theorem 3Hfvco2 6970
[Enderton] p. 49Axiom of Choice (first form)ac7 10523  ac7g 10524  df-ac 10167  dfac2 10182  dfac2a 10180  dfac2b 10181  dfac3 10172  dfac7 10183
[Enderton] p. 50Theorem 3K(a)imauni 7238
[Enderton] p. 52Definitiondf-map 8827
[Enderton] p. 53Exercise 21coass 6256
[Enderton] p. 53Exercise 27dmco 6245
[Enderton] p. 53Exercise 14(a)funin 6604
[Enderton] p. 53Exercise 22(a)imass2 6092
[Enderton] p. 54Remarkixpf 8926  ixpssmap 8938
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8904
[Enderton] p. 55Axiom of Choice (second form)ac9 10533  ac9s 10543
[Enderton] p. 56Theorem 3Meqvrelref 39546  erref 8716
[Enderton] p. 57Lemma 3Neqvrelthi 39549  erthi 8752
[Enderton] p. 57Definitiondf-ec 8697
[Enderton] p. 58Definitiondf-qs 8701
[Enderton] p. 61Exercise 35df-ec 8697
[Enderton] p. 65Exercise 56(a)dmun 5888
[Enderton] p. 68Definition of successordf-suc 6357
[Enderton] p. 71Definitiondf-tr 5212  dftr4 5217
[Enderton] p. 72Theorem 4Eunisuc 6433  unisucg 6432
[Enderton] p. 73Exercise 6unisuc 6433  unisucg 6432
[Enderton] p. 73Exercise 5(a)truni 5227
[Enderton] p. 73Exercise 5(b)trint 5229  trintALT 45807
[Enderton] p. 79Theorem 4I(A1)nna0 8591
[Enderton] p. 79Theorem 4I(A2)nnasuc 8593  onasuc 8514
[Enderton] p. 79Definition of operation valuedf-ov 7411
[Enderton] p. 80Theorem 4J(A1)nnm0 8592
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8594  onmsuc 8515
[Enderton] p. 81Theorem 4K(1)nnaass 8609
[Enderton] p. 81Theorem 4K(2)nna0r 8596  nnacom 8604
[Enderton] p. 81Theorem 4K(3)nndi 8610
[Enderton] p. 81Theorem 4K(4)nnmass 8611
[Enderton] p. 81Theorem 4K(5)nnmcom 8613
[Enderton] p. 82Exercise 16nnm0r 8597  nnmsucr 8612
[Enderton] p. 88Exercise 23nnaordex 8625
[Enderton] p. 129Definitiondf-en 8952
[Enderton] p. 132Theorem 6B(b)canth 7362
[Enderton] p. 133Exercise 1xpomen 10066
[Enderton] p. 133Exercise 2qnnen 16349
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9200
[Enderton] p. 135Corollary 6Cphp3 9202
[Enderton] p. 136Corollary 6Enneneq 9199
[Enderton] p. 136Corollary 6D(a)pssinf 9231
[Enderton] p. 136Corollary 6D(b)ominf 9233
[Enderton] p. 137Lemma 6Fpssnn 9162
[Enderton] p. 138Corollary 6Gssfi 9166
[Enderton] p. 139Theorem 6H(c)mapen 9138
[Enderton] p. 142Theorem 6I(3)xpdjuen 10230
[Enderton] p. 142Theorem 6I(4)mapdjuen 10231
[Enderton] p. 143Theorem 6Jdju0en 10226  dju1en 10222
[Enderton] p. 144Exercise 13iunfi 9310  unifi 9311  unifi2 9312
[Enderton] p. 144Corollary 6Kundif2 4430  unfi 9164  unfi2 9280
[Enderton] p. 145Figure 38ffoss 7941
[Enderton] p. 145Definitiondf-dom 8953
[Enderton] p. 146Example 1domen 8966  domeng 8967
[Enderton] p. 146Example 3nndomo 9211  nnsdom 9633  nnsdomg 9269
[Enderton] p. 149Theorem 6L(a)djudom2 10234
[Enderton] p. 149Theorem 6L(c)mapdom1 9139  xpdom1 9073  xpdom1g 9071  xpdom2g 9070
[Enderton] p. 149Theorem 6L(d)mapdom2 9145
[Enderton] p. 151Theorem 6Mzorn 10557  zorng 10554
[Enderton] p. 151Theorem 6M(4)ac8 10542  dfac5 10179
[Enderton] p. 159Theorem 6Qunictb 10632
[Enderton] p. 164Exampleinfdif 10258
[Enderton] p. 168Definitiondf-po 5555
[Enderton] p. 192Theorem 7M(a)oneli 6467
[Enderton] p. 192Theorem 7M(b)ontr1 6399
[Enderton] p. 192Theorem 7M(c)onirri 6466
[Enderton] p. 193Corollary 7N(b)0elon 6407
[Enderton] p. 193Corollary 7N(c)onsuci 7833
[Enderton] p. 193Corollary 7N(d)ssonunii 7778
[Enderton] p. 194Remarkonprc 7775
[Enderton] p. 194Exercise 16suc11 6461
[Enderton] p. 197Definitiondf-card 9992
[Enderton] p. 197Theorem 7Pcarden 10607
[Enderton] p. 200Exercise 25tfis 7849
[Enderton] p. 202Lemma 7Tr1tr 9758
[Enderton] p. 202Definitiondf-r1 9746
[Enderton] p. 202Theorem 7Qr1val1 9768
[Enderton] p. 204Theorem 7V(b)rankval4 9857  rankval4b 9853
[Enderton] p. 206Theorem 7X(b)en2lp 9585
[Enderton] p. 207Exercise 30rankpr 9844  rankprb 9838  rankpw 9829  rankpwi 9805  rankuniss 9856
[Enderton] p. 207Exercise 34opthreg 9597
[Enderton] p. 208Exercise 35suc11reg 9598
[Enderton] p. 212Definition of alephalephval3 10161
[Enderton] p. 213Theorem 8A(a)alephord2 10127
[Enderton] p. 213Theorem 8A(b)cardalephex 10141
[Enderton] p. 218Theorem Schema 8Eonfununi 8327
[Enderton] p. 222Definitiondf-kard 35743
[Enderton] p. 222Definition of kardkarden 9931  kardex 9929
[Enderton] p. 238Theorem 8Roeoa 8584
[Enderton] p. 238Theorem 8Soeoe 8586
[Enderton] p. 240Exercise 25oarec 8548
[Enderton] p. 257Definition of cofinalitycflm 10299
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17778
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17720
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18689  mrieqv2d 17775  mrieqvd 17774
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17779
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17784  mreexexlem2d 17781
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18695  mreexfidimd 17786
[Frege1879] p. 11Statementdf3or2 44712
[Frege1879] p. 12Statementdf3an2 44713  dfxor4 44710  dfxor5 44711
[Frege1879] p. 26Axiom 1ax-frege1 44734
[Frege1879] p. 26Axiom 2ax-frege2 44735
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44739
[Frege1879] p. 31Proposition 4frege4 44743
[Frege1879] p. 32Proposition 5frege5 44744
[Frege1879] p. 33Proposition 6frege6 44750
[Frege1879] p. 34Proposition 7frege7 44752
[Frege1879] p. 35Axiom 8ax-frege8 44753  axfrege8 44751
[Frege1879] p. 35Proposition 8pm2.04 91  wl-luk-pm2.04 38288
[Frege1879] p. 35Proposition 9frege9 44756
[Frege1879] p. 36Proposition 10frege10 44764
[Frege1879] p. 36Proposition 11frege11 44758
[Frege1879] p. 37Proposition 12frege12 44757
[Frege1879] p. 37Proposition 13frege13 44766
[Frege1879] p. 37Proposition 14frege14 44767
[Frege1879] p. 38Proposition 15frege15 44770
[Frege1879] p. 38Proposition 16frege16 44760
[Frege1879] p. 39Proposition 17frege17 44765
[Frege1879] p. 39Proposition 18frege18 44762
[Frege1879] p. 39Proposition 19frege19 44768
[Frege1879] p. 40Proposition 20frege20 44772
[Frege1879] p. 40Proposition 21frege21 44771
[Frege1879] p. 41Proposition 22frege22 44763
[Frege1879] p. 42Proposition 23frege23 44769
[Frege1879] p. 42Proposition 24frege24 44759
[Frege1879] p. 42Proposition 25frege25 44761  rp-frege25 44749
[Frege1879] p. 42Proposition 26frege26 44754
[Frege1879] p. 43Axiom 28ax-frege28 44774
[Frege1879] p. 43Proposition 27frege27 44755
[Frege1879] p. 43Proposition 28con3 154
[Frege1879] p. 43Proposition 29frege29 44775
[Frege1879] p. 44Axiom 31ax-frege31 44778  axfrege31 44777
[Frege1879] p. 44Proposition 30frege30 44776
[Frege1879] p. 44Proposition 31notnotr 131
[Frege1879] p. 44Proposition 32frege32 44779
[Frege1879] p. 44Proposition 33frege33 44780
[Frege1879] p. 45Proposition 34frege34 44781
[Frege1879] p. 45Proposition 35frege35 44782
[Frege1879] p. 45Proposition 36frege36 44783
[Frege1879] p. 46Proposition 37frege37 44784
[Frege1879] p. 46Proposition 38frege38 44785
[Frege1879] p. 46Proposition 39frege39 44786
[Frege1879] p. 46Proposition 40frege40 44787
[Frege1879] p. 47Axiom 41ax-frege41 44789  axfrege41 44788
[Frege1879] p. 47Proposition 41notnot 143
[Frege1879] p. 47Proposition 42frege42 44790
[Frege1879] p. 47Proposition 43frege43 44791
[Frege1879] p. 47Proposition 44frege44 44792
[Frege1879] p. 47Proposition 45frege45 44793
[Frege1879] p. 48Proposition 46frege46 44794
[Frege1879] p. 48Proposition 47frege47 44795
[Frege1879] p. 49Proposition 48frege48 44796
[Frege1879] p. 49Proposition 49frege49 44797
[Frege1879] p. 49Proposition 50frege50 44798
[Frege1879] p. 50Axiom 52ax-frege52a 44801  ax-frege52c 44832  frege52aid 44802  frege52b 44833
[Frege1879] p. 50Axiom 54ax-frege54a 44806  ax-frege54c 44836  frege54b 44837
[Frege1879] p. 50Proposition 51frege51 44799
[Frege1879] p. 50Proposition 52dfsbcq 3740
[Frege1879] p. 50Proposition 53frege53a 44804  frege53aid 44803  frege53b 44834  frege53c 44858
[Frege1879] p. 50Proposition 54biid 264  eqid 2760
[Frege1879] p. 50Proposition 55frege55a 44812  frege55aid 44809  frege55b 44841  frege55c 44862  frege55cor1a 44813  frege55lem2a 44811  frege55lem2b 44840  frege55lem2c 44861
[Frege1879] p. 50Proposition 56frege56a 44815  frege56aid 44814  frege56b 44842  frege56c 44863
[Frege1879] p. 51Axiom 58ax-frege58a 44819  ax-frege58b 44845  frege58bid 44846  frege58c 44865
[Frege1879] p. 51Proposition 57frege57a 44817  frege57aid 44816  frege57b 44843  frege57c 44864
[Frege1879] p. 51Proposition 58spsbc 3751
[Frege1879] p. 51Proposition 59frege59a 44821  frege59b 44848  frege59c 44866
[Frege1879] p. 52Proposition 60frege60a 44822  frege60b 44849  frege60c 44867
[Frege1879] p. 52Proposition 61frege61a 44823  frege61b 44850  frege61c 44868
[Frege1879] p. 52Proposition 62frege62a 44824  frege62b 44851  frege62c 44869
[Frege1879] p. 52Proposition 63frege63a 44825  frege63b 44852  frege63c 44870
[Frege1879] p. 53Proposition 64frege64a 44826  frege64b 44853  frege64c 44871
[Frege1879] p. 53Proposition 65frege65a 44827  frege65b 44854  frege65c 44872
[Frege1879] p. 54Proposition 66frege66a 44828  frege66b 44855  frege66c 44873
[Frege1879] p. 54Proposition 67frege67a 44829  frege67b 44856  frege67c 44874
[Frege1879] p. 54Proposition 68frege68a 44830  frege68b 44857  frege68c 44875
[Frege1879] p. 55Definition 69dffrege69 44876
[Frege1879] p. 58Proposition 70frege70 44877
[Frege1879] p. 59Proposition 71frege71 44878
[Frege1879] p. 59Proposition 72frege72 44879
[Frege1879] p. 59Proposition 73frege73 44880
[Frege1879] p. 60Definition 76dffrege76 44883
[Frege1879] p. 60Proposition 74frege74 44881
[Frege1879] p. 60Proposition 75frege75 44882
[Frege1879] p. 62Proposition 77frege77 44884  frege77d 44690
[Frege1879] p. 63Proposition 78frege78 44885
[Frege1879] p. 63Proposition 79frege79 44886
[Frege1879] p. 63Proposition 80frege80 44887
[Frege1879] p. 63Proposition 81frege81 44888  frege81d 44691
[Frege1879] p. 64Proposition 82frege82 44889
[Frege1879] p. 65Proposition 83frege83 44890  frege83d 44692
[Frege1879] p. 65Proposition 84frege84 44891
[Frege1879] p. 66Proposition 85frege85 44892
[Frege1879] p. 66Proposition 86frege86 44893
[Frege1879] p. 66Proposition 87frege87 44894  frege87d 44694
[Frege1879] p. 67Proposition 88frege88 44895
[Frege1879] p. 68Proposition 89frege89 44896
[Frege1879] p. 68Proposition 90frege90 44897
[Frege1879] p. 68Proposition 91frege91 44898  frege91d 44695
[Frege1879] p. 69Proposition 92frege92 44899
[Frege1879] p. 70Proposition 93frege93 44900
[Frege1879] p. 70Proposition 94frege94 44901
[Frege1879] p. 70Proposition 95frege95 44902
[Frege1879] p. 71Definition 99dffrege99 44906
[Frege1879] p. 71Proposition 96frege96 44903  frege96d 44693
[Frege1879] p. 71Proposition 97frege97 44904  frege97d 44696
[Frege1879] p. 71Proposition 98frege98 44905  frege98d 44697
[Frege1879] p. 72Proposition 100frege100 44907
[Frege1879] p. 72Proposition 101frege101 44908
[Frege1879] p. 72Proposition 102frege102 44909  frege102d 44698
[Frege1879] p. 73Proposition 103frege103 44910
[Frege1879] p. 73Proposition 104frege104 44911
[Frege1879] p. 73Proposition 105frege105 44912
[Frege1879] p. 73Proposition 106frege106 44913  frege106d 44699
[Frege1879] p. 74Proposition 107frege107 44914
[Frege1879] p. 74Proposition 108frege108 44915  frege108d 44700
[Frege1879] p. 74Proposition 109frege109 44916  frege109d 44701
[Frege1879] p. 75Proposition 110frege110 44917
[Frege1879] p. 75Proposition 111frege111 44918  frege111d 44703
[Frege1879] p. 76Proposition 112frege112 44919
[Frege1879] p. 76Proposition 113frege113 44920
[Frege1879] p. 76Proposition 114frege114 44921  frege114d 44702
[Frege1879] p. 77Definition 115dffrege115 44922
[Frege1879] p. 77Proposition 116frege116 44923
[Frege1879] p. 78Proposition 117frege117 44924
[Frege1879] p. 78Proposition 118frege118 44925
[Frege1879] p. 78Proposition 119frege119 44926
[Frege1879] p. 78Proposition 120frege120 44927
[Frege1879] p. 79Proposition 121frege121 44928
[Frege1879] p. 79Proposition 122frege122 44929  frege122d 44704
[Frege1879] p. 79Proposition 123frege123 44930
[Frege1879] p. 80Proposition 124frege124 44931  frege124d 44705
[Frege1879] p. 81Proposition 125frege125 44932
[Frege1879] p. 81Proposition 126frege126 44933  frege126d 44706
[Frege1879] p. 82Proposition 127frege127 44934
[Frege1879] p. 83Proposition 128frege128 44935
[Frege1879] p. 83Proposition 129frege129 44936  frege129d 44707
[Frege1879] p. 84Proposition 130frege130 44937
[Frege1879] p. 85Proposition 131frege131 44938  frege131d 44708
[Frege1879] p. 86Proposition 132frege132 44939
[Frege1879] p. 86Proposition 133frege133 44940  frege133d 44709
[Fremlin1] p. 13Definition 111G (b)df-salgen 47245
[Fremlin1] p. 13Definition 111G (d)borelmbl 47568
[Fremlin1] p. 13Proposition 111G (b)salgenss 47268
[Fremlin1] p. 14Definition 112Aismea 47383
[Fremlin1] p. 15Remark 112B (d)psmeasure 47403
[Fremlin1] p. 15Property 112C (a)meadjun 47394  meadjunre 47408
[Fremlin1] p. 15Property 112C (b)meassle 47395
[Fremlin1] p. 15Property 112C (c)meaunle 47396
[Fremlin1] p. 16Property 112C (d)iundjiun 47392  meaiunle 47401  meaiunlelem 47400
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47413  meaiuninc2 47414  meaiuninc3 47417  meaiuninc3v 47416  meaiunincf 47415  meaiuninclem 47412
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47419  meaiininc2 47420  meaiininclem 47418
[Fremlin1] p. 19Theorem 113Ccaragen0 47438  caragendifcl 47446  caratheodory 47460  omelesplit 47450
[Fremlin1] p. 19Definition 113Aisome 47426  isomennd 47463  isomenndlem 47462
[Fremlin1] p. 19Remark 113B (c)omeunle 47448
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47467  voncmpl 47553
[Fremlin1] p. 19Definition 113A (ii)omessle 47430
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47455  carageniuncllem1 47453  carageniuncllem2 47454  caragenuncl 47445  caragenuncllem 47444  caragenunicl 47456
[Fremlin1] p. 21Remark 113Dcaragenel2d 47464
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47458  caratheodorylem2 47459
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47467
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47526  hoidmv1lelem1 47523  hoidmv1lelem2 47524  hoidmv1lelem3 47525
[Fremlin1] p. 25Definition 114Eisvonmbl 47570
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47526  hoidmvle 47532  hoidmvlelem1 47527  hoidmvlelem2 47528  hoidmvlelem3 47529  hoidmvlelem4 47530  hoidmvlelem5 47531  hsphoidmvle2 47517  hsphoif 47508  hsphoival 47511
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47480
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47488
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47515  hoidmvn0val 47516  hoidmvval 47509  hoidmvval0 47519  hoidmvval0b 47522
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47520  hsphoidmvle 47518
[Fremlin1] p. 30Definition 115Cdf-ovoln 47469  df-voln 47471
[Fremlin1] p. 30Proposition 115D (a)dmovn 47536  ovn0 47498  ovn0lem 47497  ovnf 47495  ovnome 47505  ovnssle 47493  ovnsslelem 47492  ovnsupge0 47489
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47535  ovnhoilem1 47533  ovnhoilem2 47534  vonhoi 47599
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47552  hoidifhspf 47550  hoidifhspval 47540  hoidifhspval2 47547  hoidifhspval3 47551  hspmbl 47561  hspmbllem1 47558  hspmbllem2 47559  hspmbllem3 47560
[Fremlin1] p. 31Definition 115Evoncmpl 47553  vonmea 47506
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47504  ovnsubadd2 47578  ovnsubadd2lem 47577  ovnsubaddlem1 47502  ovnsubaddlem2 47503
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47563  hoimbl2 47597  hoimbllem 47562  hspdifhsp 47548  opnvonmbl 47566  opnvonmbllem2 47565
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47568
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47611  iccvonmbllem 47610  ioovonmbl 47609
[Fremlin1] p. 32Proposition 115G (d)vonicc 47617  vonicclem2 47616  vonioo 47614  vonioolem2 47613  vonn0icc 47620  vonn0icc2 47624  vonn0ioo 47619  vonn0ioo2 47622
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47621  snvonmbl 47618  vonct 47625  vonsn 47623
[Fremlin1] p. 35Lemma 121Asubsalsal 47291
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 47290  subsaliuncllem 47289
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47657  salpreimalegt 47641  salpreimaltle 47658
[Fremlin1] p. 35Proposition 121B (i)issmf 47660  issmff 47666  issmflem 47659
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47677  issmflelem 47676  smfpreimale 47686
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47688  issmfgtlem 47687
[Fremlin1] p. 36Definition 121Cdf-smblfn 47628  issmf 47660  issmff 47666  issmfge 47702  issmfgelem 47701  issmfgt 47688  issmfgtlem 47687  issmfle 47677  issmflelem 47676  issmflem 47659
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47639  salpreimagtlt 47662  salpreimalelt 47661
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47702  issmfgelem 47701
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47685
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47683  cnfsmf 47672
[Fremlin1] p. 36Proposition 121D (c)decsmf 47699  decsmflem 47698  incsmf 47674  incsmflem 47673
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47633  pimconstlt1 47634  smfconst 47681
[Fremlin1] p. 37Proposition 121E (b)smfadd 47697  smfaddlem1 47695  smfaddlem2 47696
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47728
[Fremlin1] p. 37Proposition 121E (d)smfmul 47727  smfmullem1 47723  smfmullem2 47724  smfmullem3 47725  smfmullem4 47726
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47729
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47732  smfpimbor1lem2 47731
[Fremlin1] p. 37Proposition 121E (g)smfco 47734
[Fremlin1] p. 37Proposition 121E (h)smfres 47722
[Fremlin1] p. 38Proposition 121E (e)smfrec 47721
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47730  smfresal 47720
[Fremlin1] p. 38Proposition 121F (a)smflim 47709  smflim2 47738  smflimlem1 47703  smflimlem2 47704  smflimlem3 47705  smflimlem4 47706  smflimlem5 47707  smflimlem6 47708  smflimmpt 47742
[Fremlin1] p. 38Proposition 121F (b)smfsup 47746  smfsuplem1 47743  smfsuplem2 47744  smfsuplem3 47745  smfsupmpt 47747  smfsupxr 47748
[Fremlin1] p. 38Proposition 121F (c)smfinf 47750  smfinflem 47749  smfinfmpt 47751
[Fremlin1] p. 39Remark 121Gsmflim 47709  smflim2 47738  smflimmpt 47742
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47740
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47770  smfdivdmmbl2 47773  smfinfdmmbl 47781  smfinfdmmbllem 47780  smfsupdmmbl 47777  smfsupdmmbllem 47776
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47760  smflimsuplem2 47753  smflimsuplem6 47757  smflimsuplem7 47758  smflimsuplem8 47759  smflimsupmpt 47761
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47763  smfliminflem 47762  smfliminfmpt 47764
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47628
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47774  fsupdm2 47775
[Fremlin1], p. 39Proposition 121Hadddmmbl 47765  adddmmbl2 47766  finfdm 47778  finfdm2 47779  fsupdm 47774  fsupdm2 47775  muldmmbl 47767  muldmmbl2 47768
[Fremlin1], p. 39Proposition 121F (c)finfdm 47778  finfdm2 47779
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25819
[Fremlin5] p. 213Lemma 565Cauniioovol 25862
[Fremlin5] p. 214Lemma 565Cauniioombl 25872
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38536
[Fremlin5] p. 220Theorem 565Maftc1anc 38539
[FreydScedrov] p. 283Axiom of Infinityax-inf 9617  inf1 9601  inf2 9602
[Gleason] p. 117Proposition 9-2.1df-enq 10968  enqer 10978
[Gleason] p. 117Proposition 9-2.2df-1nq 10973  df-nq 10969
[Gleason] p. 117Proposition 9-2.3df-plpq 10965  df-plq 10971
[Gleason] p. 119Proposition 9-2.4caovmo 7646  df-mpq 10966  df-mq 10972
[Gleason] p. 119Proposition 9-2.5df-rq 10974
[Gleason] p. 119Proposition 9-2.6ltexnq 11032
[Gleason] p. 120Proposition 9-2.6(i)halfnq 11033  ltbtwnnq 11035
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 11028
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 11029
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 11036
[Gleason] p. 121Definition 9-3.1df-np 11038
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 11050
[Gleason] p. 121Definition 9-3.1(iii)prnmax 11052
[Gleason] p. 122Definitiondf-1p 11039
[Gleason] p. 122Remark (1)prub 11051
[Gleason] p. 122Lemma 9-3.4prlem934 11090
[Gleason] p. 122Proposition 9-3.2df-ltp 11042
[Gleason] p. 122Proposition 9-3.3ltsopr 11089  psslinpr 11088  supexpr 11111  suplem1pr 11109  suplem2pr 11110
[Gleason] p. 123Proposition 9-3.5addclpr 11075  addclprlem1 11073  addclprlem2 11074  df-plp 11040
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11079
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11078
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11091
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11100  ltexprlem1 11093  ltexprlem2 11094  ltexprlem3 11095  ltexprlem4 11096  ltexprlem5 11097  ltexprlem6 11098  ltexprlem7 11099
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11102  ltaprlem 11101
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11103
[Gleason] p. 124Lemma 9-3.6prlem936 11104
[Gleason] p. 124Proposition 9-3.7df-mp 11041  mulclpr 11077  mulclprlem 11076  reclem2pr 11105
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11086
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11081
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11080
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11085
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11108  reclem3pr 11106  reclem4pr 11107
[Gleason] p. 126Proposition 9-4.1df-enr 11112  enrer 11120
[Gleason] p. 126Proposition 9-4.2df-0r 11117  df-1r 11118  df-nr 11113
[Gleason] p. 126Proposition 9-4.3df-mr 11115  df-plr 11114  negexsr 11159  recexsr 11164  recexsrlem 11160
[Gleason] p. 127Proposition 9-4.4df-ltr 11116
[Gleason] p. 130Proposition 10-1.3creui 12285  creur 12284  cru 12282
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11245  axcnre 11221
[Gleason] p. 132Definition 10-3.1crim 15250  crimd 15367  crimi 15328  crre 15249  crred 15366  crrei 15327
[Gleason] p. 132Definition 10-3.2remim 15252  remimd 15333
[Gleason] p. 133Definition 10.36absval2 15419  absval2d 15583  absval2i 15533
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15276  cjaddd 15355  cjaddi 15323
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15277  cjmuld 15356  cjmuli 15324
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15275  cjcjd 15334  cjcji 15306
[Gleason] p. 133Proposition 10-3.4(f)cjre 15274  cjreb 15258  cjrebd 15337  cjrebi 15309  cjred 15361  rere 15257  rereb 15255  rerebd 15336  rerebi 15308  rered 15359
[Gleason] p. 133Proposition 10-3.4(h)addcj 15283  addcjd 15347  addcji 15318
[Gleason] p. 133Proposition 10-3.7(a)absval 15373
[Gleason] p. 133Proposition 10-3.7(b)abscj 15414  abscjd 15588  abscji 15537
[Gleason] p. 133Proposition 10-3.7(c)abs00 15424  abs00d 15584  abs00i 15534  absne0d 15585
[Gleason] p. 133Proposition 10-3.7(d)releabs 15457  releabsd 15589  releabsi 15538
[Gleason] p. 133Proposition 10-3.7(f)absmul 15429  absmuld 15592  absmuli 15540
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15417  sqabsaddi 15541
[Gleason] p. 133Proposition 10-3.7(h)abstri 15466  abstrid 15594  abstrii 15544
[Gleason] p. 134Definition 10-4.1df-exp 14174  exp0 14177  expp1 14180  expp1d 14259
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26971  cxpaddd 27009  expadd 14216  expaddd 14260  expaddz 14218
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26980  cxpmuld 27029  expmul 14219  expmuld 14261  expmulz 14220
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26977  mulcxpd 27020  mulexp 14213  mulexpd 14273  mulexpz 14214
[Gleason] p. 140Exercise 1znnen 16348
[Gleason] p. 141Definition 11-2.1fzval 13611
[Gleason] p. 168Proposition 12-2.1(a)climadd 15767  rlimadd 15778  rlimdiv 15781
[Gleason] p. 168Proposition 12-2.1(b)climsub 15769  rlimsub 15779
[Gleason] p. 168Proposition 12-2.1(c)climmul 15768  rlimmul 15780
[Gleason] p. 171Corollary 12-2.2climmulc2 15772
[Gleason] p. 172Corollary 12-2.5climrecl 15718
[Gleason] p. 172Proposition 12-2.4(c)climabs 15739  climcj 15740  climim 15742  climre 15741  rlimabs 15744  rlimcj 15745  rlimim 15747  rlimre 15746
[Gleason] p. 173Definition 12-3.1df-ltxr 11320  df-xr 11319  ltxr 13214
[Gleason] p. 175Definition 12-4.1df-limsup 15606  limsupval 15609
[Gleason] p. 180Theorem 12-5.1climsup 15805
[Gleason] p. 180Theorem 12-5.3caucvg 15814  caucvgb 15815  caucvgbf 46421  caucvgr 15811  climcau 15806
[Gleason] p. 182Exercise 3cvgcmp 15951
[Gleason] p. 182Exercise 4cvgrat 16020
[Gleason] p. 195Theorem 13-2.12abs1m 15471
[Gleason] p. 217Lemma 13-4.1btwnzge0 13937
[Gleason] p. 223Definition 14-1.1df-met 21634
[Gleason] p. 223Definition 14-1.1(a)met0 24624  xmet0 24623
[Gleason] p. 223Definition 14-1.1(b)metgt0 24640
[Gleason] p. 223Definition 14-1.1(c)metsym 24631
[Gleason] p. 223Definition 14-1.1(d)mettri 24633  mstri 24750  xmettri 24632  xmstri 24749
[Gleason] p. 225Definition 14-1.5xpsmet 24663
[Gleason] p. 230Proposition 14-2.6txlm 23929
[Gleason] p. 240Theorem 14-4.3metcnp4 25593
[Gleason] p. 240Proposition 14-4.2metcnp3 24821
[Gleason] p. 243Proposition 14-4.16addcn 25147  addcn2 15729  mulcn 25149  mulcn2 15731  subcn 25148  subcn2 15730
[Gleason] p. 295Remarkbcval3 14418  bcval4 14419
[Gleason] p. 295Equation 2bcpasc 14433
[Gleason] p. 295Definition of binomial coefficientbcval 14416  df-bc 14415
[Gleason] p. 296Remarkbcn0 14422  bcnn 14424
[Gleason] p. 296Theorem 15-2.8binom 15967
[Gleason] p. 308Equation 2ef0 16225
[Gleason] p. 308Equation 3efcj 16226
[Gleason] p. 309Corollary 15-4.3efne0 16232
[Gleason] p. 309Corollary 15-4.4efexp 16237
[Gleason] p. 310Equation 14sinadd 16300
[Gleason] p. 310Equation 15cosadd 16301
[Gleason] p. 311Equation 17sincossq 16312
[Gleason] p. 311Equation 18cosbnd 16317  sinbnd 16316
[Gleason] p. 311Lemma 15-4.7sqeqor 14328  sqeqori 14326
[Gleason] p. 311Definition of ` `df-pi 16206
[Godowski] p. 730Equation SFgoeqi 32809
[GodowskiGreechie] p. 249Equation IV3oai 32204
[Golan] p. 1Remarksrgisid 20397
[Golan] p. 1Definitiondf-srg 20375
[Golan] p. 149Definitiondf-slmd 33696
[Gonshor] p. 7Definitiondf-cuts 28080
[Gonshor] p. 9Theorem 2.5lesrec 28119  lesrecd 28120
[Gonshor] p. 10Theorem 2.6cofcut1 28240  cofcut1d 28241
[Gonshor] p. 10Theorem 2.7cofcut2 28242  cofcut2d 28243
[Gonshor] p. 12Theorem 2.9cofcutr 28244  cofcutr1d 28245  cofcutr2d 28246
[Gonshor] p. 13Definitiondf-adds 28280
[Gonshor] p. 14Theorem 3.1addsprop 28296
[Gonshor] p. 15Theorem 3.2addsunif 28322
[Gonshor] p. 17Theorem 3.4mulsprop 28450
[Gonshor] p. 18Theorem 3.5mulsunif 28470
[Gonshor] p. 28Lemma 4.2halfcut 28778
[Gonshor] p. 28Theorem 4.2pw2cut 28780
[Gonshor] p. 30Theorem 4.2addhalfcut 28779
[Gonshor] p. 39Theorem 4.4(b)elreno2 28815
[Gonshor] p. 95Theorem 6.1addbday 28338
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36846
[Gratzer] p. 23Section 0.6df-mre 17718
[Gratzer] p. 27Section 0.6df-mri 17720
[Hall] p. 1Section 1.1df-asslaw 49207  df-cllaw 49205  df-comlaw 49206
[Hall] p. 2Section 1.2df-clintop 49219
[Hall] p. 7Section 1.3df-sgrp2 49240
[Halmos] p. 28Partition ` `df-parts 39720  dfmembpart2 39725
[Halmos] p. 31Theorem 17.3riesz1 32601  riesz2 32602
[Halmos] p. 41Definition of Hermitianhmopadj2 32477
[Halmos] p. 42Definition of projector orderingpjordi 32709
[Halmos] p. 43Theorem 26.1elpjhmop 32721  elpjidm 32720  pjnmopi 32684
[Halmos] p. 44Remarkpjinormi 32223  pjinormii 32212
[Halmos] p. 44Theorem 26.2elpjch 32725  pjrn 32243  pjrni 32238  pjvec 32232
[Halmos] p. 44Theorem 26.3pjnorm2 32263
[Halmos] p. 44Theorem 26.4hmopidmpj 32690  hmopidmpji 32688
[Halmos] p. 45Theorem 27.1pjinvari 32727
[Halmos] p. 45Theorem 27.3pjoci 32716  pjocvec 32233
[Halmos] p. 45Theorem 27.4pjorthcoi 32705
[Halmos] p. 48Theorem 29.2pjssposi 32708
[Halmos] p. 48Theorem 29.3pjssdif1i 32711  pjssdif2i 32710
[Halmos] p. 50Definition of spectrumdf-spec 32391
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 24
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1828
[Hatcher] p. 25Definitiondf-phtpc 25275  df-phtpy 25254
[Hatcher] p. 26Definitiondf-pco 25288  df-pi1 25291
[Hatcher] p. 26Proposition 1.2phtpcer 25278
[Hatcher] p. 26Proposition 1.3pi1grp 25333
[Hefferon] p. 240Definition 3.12df-dmat 22767  df-dmatalt 49432
[Helfgott] p. 2Theoremtgoldbach 48837
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48822
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48834  bgoldbtbnd 48829  bgoldbtbnd 48829  tgblthelfgott 48835
[Helfgott] p. 5Proposition 1.1circlevma 35206
[Helfgott] p. 69Statement 7.49circlemethhgt 35207
[Helfgott] p. 69Statement 7.50hgt750lema 35221  hgt750lemb 35220  hgt750leme 35222  hgt750lemf 35217  hgt750lemg 35218
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48831  tgoldbachgt 35227  tgoldbachgtALTV 48832  tgoldbachgtd 35226
[Helfgott] p. 70Statement 7.49ax-hgt749 35208
[Herstein] p. 54Exercise 28df-grpo 31029
[Herstein] p. 55Lemma 2.2.1(a)grpideu 19117  grpoideu 31045  mndideu 18896
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19147  grpoinveu 31055
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19178  grpo2inv 31067
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19190  grpoinvop 31069
[Herstein] p. 57Exercise 1dfgrp3e 19212
[Hitchcock] p. 5Rule A3mptnan 1801
[Hitchcock] p. 5Rule A4mptxor 1802
[Hitchcock] p. 5Rule A5mtpxor 1804
[Holland] p. 1519Theorem 2sumdmdi 32956
[Holland] p. 1520Lemma 5cdj1i 32969  cdj3i 32977  cdj3lem1 32970  cdjreui 32968
[Holland] p. 1524Lemma 7mddmdin0i 32967
[Holland95] p. 13Theorem 3.6hlathil 42938
[Holland95] p. 14Line 15hgmapvs 42868
[Holland95] p. 14Line 16hdmaplkr 42890
[Holland95] p. 14Line 17hdmapellkr 42891
[Holland95] p. 14Line 19hdmapglnm2 42888
[Holland95] p. 14Line 20hdmapip0com 42894
[Holland95] p. 14Theorem 3.6hdmapevec2 42813
[Holland95] p. 14Lines 24 and 25hdmapoc 42908
[Holland95] p. 204Definition of involutiondf-srng 21059
[Holland95] p. 212Definition of subspacedf-psubsp 40480
[Holland95] p. 214Lemma 3.3lclkrlem2v 42505
[Holland95] p. 214Definition 3.2df-lpolN 42458
[Holland95] p. 214Definition of nonsingularpnonsingN 40910
[Holland95] p. 215Lemma 3.3(1)dihoml4 42354  poml4N 40930
[Holland95] p. 215Lemma 3.3(2)dochexmid 42445  pexmidALTN 40955  pexmidN 40946
[Holland95] p. 218Theorem 3.6lclkr 42510
[Holland95] p. 218Definition of dual vector spacedf-ldual 40101  ldualset 40102
[Holland95] p. 222Item 1df-lines 40478  df-pointsN 40479
[Holland95] p. 222Item 2df-polarityN 40880
[Holland95] p. 223Remarkispsubcl2N 40924  omllaw4 40223  pol1N 40887  polcon3N 40894
[Holland95] p. 223Definitiondf-psubclN 40912
[Holland95] p. 223Equation for polaritypolval2N 40883
[Holmes] p. 40Definitiondf-xrn 39232
[Hughes] p. 44Equation 1.21bax-his3 31620
[Hughes] p. 47Definition of projection operatordfpjop 32718
[Hughes] p. 49Equation 1.30eighmre 32499  eigre 32371  eigrei 32370
[Hughes] p. 49Equation 1.31eighmorth 32500  eigorth 32374  eigorthi 32373
[Hughes] p. 137Remark (ii)eigposi 32372
[Huneke] p. 1Claim 1frgrncvvdeq 30844
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30840
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30841
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30842
[Huneke] p. 2Claim 2frgrregorufr 30860  frgrregorufr0 30859  frgrregorufrg 30861
[Huneke] p. 2Claim 3frgrhash2wsp 30867  frrusgrord 30876  frrusgrord0 30875
[Huneke] p. 2Statementdf-clwwlknon 30613
[Huneke] p. 2Statement 4frgrwopreglem4 30850
[Huneke] p. 2Statement 5frgrwopreg1 30853  frgrwopreg2 30854  frgrwopregasn 30851  frgrwopregbsn 30852
[Huneke] p. 2Statement 6frgrwopreglem5 30856
[Huneke] p. 2Statement 7fusgreghash2wspv 30870
[Huneke] p. 2Statement 8fusgreghash2wsp 30873
[Huneke] p. 2Statement 9clwlksndivn 30611  numclwlk1 30906  numclwlk1lem1 30904  numclwlk1lem2 30905  numclwwlk1 30896  numclwwlk8 30927
[Huneke] p. 2Definition 3frgrwopreglem1 30847
[Huneke] p. 2Definition 4df-clwlks 30292
[Huneke] p. 2Definition 62clwwlk 30882
[Huneke] p. 2Definition 7numclwwlkovh 30908  numclwwlkovh0 30907
[Huneke] p. 2Statement 10numclwwlk2 30916
[Huneke] p. 2Statement 11rusgrnumwlkg 30503
[Huneke] p. 2Statement 12numclwwlk3 30920
[Huneke] p. 2Statement 13numclwwlk5 30923
[Huneke] p. 2Statement 14numclwwlk7 30926
[Indrzejczak] p. 33Definition ` `Enatded 30938  natded 30938
[Indrzejczak] p. 33Definition ` `Inatded 30938
[Indrzejczak] p. 34Definition ` `Enatded 30938  natded 30938
[Indrzejczak] p. 34Definition ` `Inatded 30938
[Jech] p. 4Definition of classcv 1569  cvjust 2754
[Jech] p. 42Lemma 6.1alephexp1 10636
[Jech] p. 42Equation 6.1alephadd 10634  alephmul 10635
[Jech] p. 43Lemma 6.2infmap 10633  infmap2 10267
[Jech] p. 71Lemma 9.3jech9.3 9796
[Jech] p. 72Equation 9.3df-scott 9901
[Jech] p. 72Exercise 9.1rankval4 9857  rankval4b 9853
[Jech] p. 72Scheme "Collection Principle"cp 9926
[Jech] p. 78Noteopthprc 5711
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43860
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43948
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43949
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43872
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43876
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43877  rmyp1 43878
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43879  rmym1 43880
[JonesMatijasevic] p. 695Equation 2.11rmx0 43870  rmx1 43871  rmxluc 43881
[JonesMatijasevic] p. 695Equation 2.12rmy0 43874  rmy1 43875  rmyluc 43882
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43884
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43885
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43905  jm2.17b 43906  jm2.17c 43907
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43938
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43942
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43933
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43908  jm2.24nn 43904
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43947
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43953  rmygeid 43909
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43965
[Juillerat] p. 11Section *5etransc 47215  etransclem47 47213  etransclem48 47214
[Juillerat] p. 12Equation (7)etransclem44 47210
[Juillerat] p. 12Equation *(7)etransclem46 47212
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 47198
[Juillerat] p. 13Proofetransclem35 47201
[Juillerat] p. 13Part of case 2 proven inetransclem38 47204
[Juillerat] p. 13Part of case 2 provenetransclem24 47190
[Juillerat] p. 13Part of case 2: proven inetransclem41 47207
[Juillerat] p. 14Proofetransclem23 47189
[KalishMontague] p. 81Note 1ax-6 2000
[KalishMontague] p. 85Lemma 2equid 2045
[KalishMontague] p. 85Lemma 3equcomi 2050
[KalishMontague] p. 86Lemma 7cbvalivw 2040  cbvaliw 2039  wl-cbvmotv 38365  wl-motae 38367  wl-moteq 38366
[KalishMontague] p. 87Lemma 8spimvw 2019  spimw 2003
[KalishMontague] p. 87Lemma 9spfw 2066  spw 2067
[Kalmbach] p. 14Definition of latticechabs1 32052  chabs1i 32054  chabs2 32053  chabs2i 32055  chjass 32069  chjassi 32022  latabs1 18611  latabs2 18612
[Kalmbach] p. 15Definition of atomdf-at 32874  ela 32875
[Kalmbach] p. 15Definition of coverscvbr2 32819  cvrval2 40251
[Kalmbach] p. 16Definitiondf-ol 40155  df-oml 40156
[Kalmbach] p. 20Definition of commutescmbr 32120  cmbri 32126  cmtvalN 40188  df-cm 32119  df-cmtN 40154
[Kalmbach] p. 22Remarkomllaw5N 40224  pjoml5 32149  pjoml5i 32124
[Kalmbach] p. 22Definitionpjoml2 32147  pjoml2i 32121
[Kalmbach] p. 22Theorem 2(v)cmcm 32150  cmcmi 32128  cmcmii 32133  cmtcomN 40226
[Kalmbach] p. 22Theorem 2(ii)omllaw3 40222  omlsi 31940  pjoml 31972  pjomli 31971
[Kalmbach] p. 22Definition of OML lawomllaw2N 40221
[Kalmbach] p. 23Remarkcmbr2i 32132  cmcm3 32151  cmcm3i 32130  cmcm3ii 32135  cmcm4i 32131  cmt3N 40228  cmt4N 40229  cmtbr2N 40230
[Kalmbach] p. 23Lemma 3cmbr3 32144  cmbr3i 32136  cmtbr3N 40231
[Kalmbach] p. 25Theorem 5fh1 32154  fh1i 32157  fh2 32155  fh2i 32158  omlfh1N 40235
[Kalmbach] p. 65Remarkchjatom 32893  chslej 32034  chsleji 31994  shslej 31916  shsleji 31906
[Kalmbach] p. 65Proposition 1chocin 32031  chocini 31990  chsupcl 31876  chsupval2 31946  h0elch 31791  helch 31779  hsupval2 31945  ocin 31832  ococss 31829  shococss 31830
[Kalmbach] p. 65Definition of subspace sumshsval 31848
[Kalmbach] p. 66Remarkdf-pjh 31931  pjssmi 32701  pjssmii 32217
[Kalmbach] p. 67Lemma 3osum 32181  osumi 32178
[Kalmbach] p. 67Lemma 4pjci 32736
[Kalmbach] p. 103Exercise 6atmd2 32936
[Kalmbach] p. 103Exercise 12mdsl0 32846
[Kalmbach] p. 140Remarkhatomic 32896  hatomici 32895  hatomistici 32898
[Kalmbach] p. 140Proposition 1atlatmstc 40296
[Kalmbach] p. 140Proposition 1(i)atexch 32917  lsatexch 40020
[Kalmbach] p. 140Proposition 1(ii)chcv1 32891  cvlcvr1 40316  cvr1 40387
[Kalmbach] p. 140Proposition 1(iii)cvexch 32910  cvexchi 32905  cvrexch 40397
[Kalmbach] p. 149Remark 2chrelati 32900  hlrelat 40379  hlrelat5N 40378  lrelat 39991
[Kalmbach] p. 153Exercise 5lsmcv 21381  lsmsatcv 39987  spansncv 32189  spansncvi 32188
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 40006  spansncv2 32829
[Kalmbach] p. 266Definitiondf-st 32747
[Kalmbach2] p. 8Definition of adjointdf-adjh 32385
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10703  fpwwe2 10700
[KanamoriPincus] p. 416Corollary 1.3canth4 10704
[KanamoriPincus] p. 417Corollary 1.6canthp1 10711
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10706
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10708
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10721
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10725  gchxpidm 10726
[KanamoriPincus] p. 419Theorem 2.1gchacg 10737  gchhar 10736
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10265  unxpwdom 9561
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10727
[Kreyszig] p. 3Property M1metcl 24613  xmetcl 24612
[Kreyszig] p. 4Property M2meteq0 24620
[Kreyszig] p. 8Definition 1.1-8dscmet 24853
[Kreyszig] p. 12Equation 5conjmul 12004  muleqadd 11930
[Kreyszig] p. 18Definition 1.3-2mopnval 24719
[Kreyszig] p. 19Remarkmopntopon 24720
[Kreyszig] p. 19Theorem T1mopn0 24779  mopnm 24725
[Kreyszig] p. 19Theorem T2unimopn 24777
[Kreyszig] p. 19Definition of neighborhoodneibl 24782
[Kreyszig] p. 20Definition 1.3-3metcnp2 24823
[Kreyszig] p. 25Definition 1.4-1lmbr 23538  lmmbr 25541  lmmbr2 25542
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23660
[Kreyszig] p. 28Theorem 1.4-5lmcau 25596
[Kreyszig] p. 28Definition 1.4-3iscau 25559  iscmet2 25577
[Kreyszig] p. 30Theorem 1.4-7cmetss 25599
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23742  metelcls 25588
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25589  metcld2 25590
[Kreyszig] p. 51Equation 2clmvneg1 25382  lmodvneg1 21142  nvinv 31175  vcm 31112
[Kreyszig] p. 51Equation 1aclm0vs 25378  lmod0vs 21132  slmd0vs 33719  vc0 31110
[Kreyszig] p. 51Equation 1blmodvs0 21133  slmdvs0 33720  vcz 31111
[Kreyszig] p. 58Definition 2.2-1imsmet 31227  ngpmet 24884  nrmmetd 24855
[Kreyszig] p. 59Equation 1imsdval 31222  imsdval2 31223  ncvspds 25444  ngpds 24885
[Kreyszig] p. 63Problem 1nmval 24870  nvnd 31224
[Kreyszig] p. 64Problem 2nmeq0 24899  nmge0 24898  nvge0 31209  nvz 31205
[Kreyszig] p. 64Problem 3nmrtri 24905  nvabs 31208
[Kreyszig] p. 91Definition 2.7-1isblo3i 31337
[Kreyszig] p. 92Equation 2df-nmoo 31281
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 31343  blocni 31341
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 31342
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25487  ipeq0 21906  ipz 31255
[Kreyszig] p. 135Problem 2cphpyth 25499  pythi 31386
[Kreyszig] p. 137Lemma 3-2.1(a)sii 31390
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25521
[Kreyszig] p. 144Equation 4supcvg 15993
[Kreyszig] p. 144Theorem 3.3-1minvec 25719  minveco 31420
[Kreyszig] p. 196Definition 3.9-1df-aj 31286
[Kreyszig] p. 247Theorem 4.7-2bcth 25612
[Kreyszig] p. 249Theorem 4.7-3ubth 31409
[Kreyszig] p. 470Definition of positive operator orderingleop 32659  leopg 32658
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32677
[Kreyszig] p. 525Theorem 10.1-1htth 31454
[Kulpa] p. 547Theorempoimir 38491
[Kulpa] p. 547Equation (1)poimirlem32 38490
[Kulpa] p. 547Equation (2)poimirlem31 38489
[Kulpa] p. 548Theorembroucube 38492
[Kulpa] p. 548Equation (6)poimirlem26 38484
[Kulpa] p. 548Equation (7)poimirlem27 38485
[Kunen] p. 10Axiom 0ax6e 2412  axnul 5258
[Kunen] p. 11Axiom 3axnul 5258
[Kunen] p. 12Axiom 6zfrep6 5241
[Kunen] p. 24Definition 10.24mapval 8836  mapvalg 8834
[Kunen] p. 30Lemma 10.20fodomg 10572
[Kunen] p. 31Definition 10.24mapex 7935
[Kunen] p. 95Definition 2.1df-r1 9746
[Kunen] p. 97Lemma 2.10r1elss 9788  r1elssi 9787
[Kunen] p. 107Exercise 4rankop 9845  rankopb 9839  rankuni 9852  rankxplim 9869  rankxpsuc 9872
[Kunen2] p. 47Lemma I.9.9relpfr 45881
[Kunen2] p. 53Lemma I.9.21trfr 45889
[Kunen2] p. 53Lemma I.9.24(2)wffr 45888
[Kunen2] p. 53Definition I.9.20tcfr 45890
[Kunen2] p. 95Lemma I.16.2ralabso 45895  rexabso 45896
[Kunen2] p. 96Example I.16.3disjabso 45902  n0abso 45903  ssabso 45901
[Kunen2] p. 111Lemma II.2.4(1)traxext 45904
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45914
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45909
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45912
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45913
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45908
[Kunen2] p. 112Corollary II.2.5wfaxext 45920  wfaxpr 45925  wfaxreg 45927  wfaxrep 45921  wfaxsep 45922  wfaxun 45926
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45911
[Kunen2] p. 113Corollary II.2.9wfaxpow 45924
[Kunen2] p. 114Theorem II.2.13wfaxext 45920
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45919  omelaxinf2 45916
[Kunen2] p. 114Corollary II.2.12wfac8prim 45929  wfaxinf2 45928
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45942  permaxext 45932  permaxinf2 45940  permaxnul 45935  permaxpow 45936  permaxpr 45937  permaxrep 45933  permaxsep 45934  permaxun 45938
[Kunen2] p. 148Definition II.9.1brpermmodel 45930
[Kunen2] p. 149Exercise II.9.3permac8prim 45941
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4963
[Lang] , p. 225Corollary 1.3finexttrb 34231
[Lang] p. Definitiondf-rn 5658
[Lang] p. 3Statementlidrideqd 18812  mndbn0 18902
[Lang] p. 3Definitiondf-mnd 18886
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18838
[Lang] p. 4Property of composites. Second formulagsumccat 18999
[Lang] p. 5Equationgsumreidx 20093
[Lang] p. 5Definition of an (infinite) productgsumfsupp 49201
[Lang] p. 6Examplenn0mnd 49198
[Lang] p. 6Equationgsumxp2 20156
[Lang] p. 6Statementcycsubm 19379
[Lang] p. 6Definitionmulgnn0gsum 19252
[Lang] p. 6Observationmndlsmidm 19846
[Lang] p. 7Definitiondfgrp2e 19136
[Lang] p. 30Definitiondf-tocyc 33602
[Lang] p. 32Property (a)cyc3genpm 33647
[Lang] p. 32Property (b)cyc3conja 33652  cycpmconjv 33637
[Lang] p. 53Definitiondf-cat 17804
[Lang] p. 53Axiom CAT 1cat1 18234  cat1lem 18233
[Lang] p. 54Definitiondf-iso 17886
[Lang] p. 57Definitiondf-inito 18121  df-termo 18122
[Lang] p. 58Exampleirinitoringc 21747
[Lang] p. 58Statementinitoeu1 18148  termoeu1 18155
[Lang] p. 62Definitiondf-func 17995
[Lang] p. 65Definitiondf-nat 18083
[Lang] p. 83Definition of "ring with unit"dfring2 20479
[Lang] p. 91Notedf-ringc 20860
[Lang] p. 92Statementmxidlprm 33929
[Lang] p. 92Definitionisprmidlc 21590
[Lang] p. 128Remarkdsmmlmod 22013
[Lang] p. 129Prooflincscm 49464  lincscmcl 49466  lincsum 49463  lincsumcl 49465
[Lang] p. 129Statementlincolss 49468
[Lang] p. 129Observationdsmmfi 22006
[Lang] p. 141Theorem 5.3dimkerim 34193  qusdimsum 34194
[Lang] p. 141Corollary 5.4lssdimle 34174
[Lang] p. 147Definitionsnlindsntor 49505
[Lang] p. 504Statementmat1 22724  matring 22720
[Lang] p. 504Definitiondf-mamu 22668
[Lang] p. 505Statementmamuass 22679  mamutpos 22735  matassa 22721  mattposvs 22732  tposmap 22734
[Lang] p. 513Definitionmdet1 22878  mdetf 22872
[Lang] p. 513Theorem 4.4cramer 22971
[Lang] p. 514Proposition 4.6mdetleib 22864
[Lang] p. 514Proposition 4.8mdettpos 22888
[Lang] p. 515Definitiondf-minmar1 22912  smadiadetr 22952
[Lang] p. 515Corollary 4.9mdetero 22887  mdetralt 22885
[Lang] p. 517Proposition 4.15mdetmul 22900
[Lang] p. 518Definitiondf-madu 22911
[Lang] p. 518Proposition 4.16madulid 22922  madurid 22921  matinv 22954
[Lang] p. 561Theorem 3.1cayleyhamilton 23170
[Lang], p. 190Chapter 6vieta 34146
[Lang], p. 224Proposition 1.1extdgfialg 34260  finextalg 34264
[Lang], p. 224Proposition 1.2extdgmul 34229  fedgmul 34197
[Lang], p. 225Proposition 1.4algextdeg 34291
[Lang], p. 561Remarkchpmatply1 23112
[Lang], p. 561Definitiondf-chpmat 23107
[Lang2] p. 3Notationsdf-ind 12291
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 45262
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 45257
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 45263
[LeBlanc] p. 277Rule R2axnul 5258
[Levy] p. 12Axiom 4.3.1df-clab 2739  wl-df.clab 38350
[Levy] p. 59Definitiondf-ttrcl 9687
[Levy] p. 64Theorem 5.6(ii)frinsg 9733
[Levy] p. 338Axiomdf-clel 2835  df-cleq 2752  wl-df.cleq 38351
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 38354
[Levy] p. 357Definition extends to class variables a relation already valid for set variables, and is therefore conservative. This only sketches the conservativity arguement; for details see Appendixwl-df.clel 38354
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2835  df-cleq 2752  wl-df.cleq 38351
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2739  wl-df.clab 38350
[Levy] p. 358Axiomdf-clab 2739  wl-df.clab 38350
[Levy58] p. 2Definition Iisfin1-3 10436
[Levy58] p. 2Definition IIdf-fin2 10336
[Levy58] p. 2Definition Iadf-fin1a 10335
[Levy58] p. 2Definition IIIdf-fin3 10338
[Levy58] p. 3Definition Vdf-fin5 10339
[Levy58] p. 3Definition IVdf-fin4 10337
[Levy58] p. 4Definition VIdf-fin6 10340
[Levy58] p. 4Definition VIIdf-fin7 10341
[Levy58], p. 3Theorem 1fin1a2 10465
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27977
[Lipparini] p. 3Lemma 2.1.4noresle 27988
[Lipparini] p. 6Proposition 4.2noinfbnd1 28020  nosupbnd1 28005
[Lipparini] p. 6Proposition 4.3noinfbnd2 28022  nosupbnd2 28007
[Lipparini] p. 7Theorem 5.1noetasuplem3 28026  noetasuplem4 28027
[Lipparini] p. 7Corollary 4.4nosupinfsep 28023
[Lopez-Astorga] p. 12Rule 1mptnan 1801
[Lopez-Astorga] p. 12Rule 2mptxor 1802
[Lopez-Astorga] p. 12Rule 3mtpxor 1804
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32944
[Maeda] p. 168Lemma 5mdsym 32948  mdsymi 32947
[Maeda] p. 168Lemma 4(i)mdsymlem4 32942  mdsymlem6 32944  mdsymlem7 32945
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32946
[MaedaMaeda] p. 1Remarkssdmd1 32849  ssdmd2 32850  ssmd1 32847  ssmd2 32848
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32845
[MaedaMaeda] p. 1Definition 1.1df-dmd 32817  df-md 32816  mdbr 32830
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32867  mdslj1i 32855  mdslj2i 32856  mdslle1i 32853  mdslle2i 32854  mdslmd1i 32865  mdslmd2i 32866
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32857  mdsl2bi 32859  mdsl2i 32858
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32871
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32868
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32869
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32846
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32851  mdsl3 32852
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32870
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32965
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 40298  hlrelat1 40377
[MaedaMaeda] p. 31Lemma 7.5lcvexch 40016
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32872  cvmdi 32860  cvnbtwn4 32825  cvrnbtwn4 40256
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32873
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 40317  cvp 32911  cvrp 40393  lcvp 40017
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32935
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32934
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 40310  hlexch4N 40369
[MaedaMaeda] p. 34Exercise 7.1atabsi 32937
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40420
[MaedaMaeda] p. 61Definition 15.10psubN 40726  atpsubN 40730  df-pointsN 40479  pointpsubN 40728
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40481  pmap11 40739  pmaple 40738  pmapsub 40745  pmapval 40734
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40742  pmap1N 40744
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40747  pmapglb2N 40748  pmapglb2xN 40749  pmapglbx 40746
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40829
[MaedaMaeda] p. 67Postulate PS1ps-1 40454
[MaedaMaeda] p. 68Lemma 16.2df-padd 40773  paddclN 40819  paddidm 40818
[MaedaMaeda] p. 68Condition PS2ps-2 40455
[MaedaMaeda] p. 68Equation 16.2.1paddass 40815
[MaedaMaeda] p. 69Lemma 16.4ps-1 40454
[MaedaMaeda] p. 69Theorem 16.4ps-2 40455
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19851  lsmmod2 19852  lssats 39989  shatomici 32894  shatomistici 32897  shmodi 31926  shmodsi 31925
[MaedaMaeda] p. 130Remark 29.6dmdmd 32836  mdsymlem7 32945
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 32125
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 32029
[MaedaMaeda] p. 139Remarksumdmdii 32951
[Margaris] p. 40Rule Cexlimiv 1963
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 402  df-ex 1813  df-or 862  dfbi2 480
[Margaris] p. 51Theorem 1idALT 24
[Margaris] p. 56Theorem 3conventions 30935
[Margaris] p. 59Section 14notnotrALTVD 45841
[Margaris] p. 60Theorem 8jcn 163
[Margaris] p. 60Section 14con3ALTVD 45842
[Margaris] p. 79Rule Cexinst01 45552  exinst11 45553
[Margaris] p. 89Theorem 19.219.2 2009  19.2g 2224  r19.2z 4454
[Margaris] p. 89Theorem 19.319.3 2238  rr19.3v 3620
[Margaris] p. 89Theorem 19.5alcom 2196
[Margaris] p. 89Theorem 19.6alex 1859
[Margaris] p. 89Theorem 19.7alnex 1814
[Margaris] p. 89Theorem 19.819.8a 2217
[Margaris] p. 89Theorem 19.919.9 2241  19.9h 2319  exlimd 2254  exlimdh 2323
[Margaris] p. 89Theorem 19.11excom 2199  excomim 2200
[Margaris] p. 89Theorem 19.1219.12 2357
[Margaris] p. 90Section 19conventions-labels 30936  conventions-labels 30936  conventions-labels 30936  conventions-labels 30936
[Margaris] p. 90Theorem 19.14exnal 1860
[Margaris] p. 90Theorem 19.152albi 45306  albi 1851
[Margaris] p. 90Theorem 19.1619.16 2261
[Margaris] p. 90Theorem 19.1719.17 2262
[Margaris] p. 90Theorem 19.182exbi 45308  exbi 1880
[Margaris] p. 90Theorem 19.1919.19 2265
[Margaris] p. 90Theorem 19.202alim 45305  2alimdv 1951  alimd 2248  alimdh 1850  alimdv 1949  ax-4 1842  ralimdaa 3263  ralimdv 3176  ralimdva 3174  ralimdvva 3209  sbcimdv 3806
[Margaris] p. 90Theorem 19.2119.21 2243  19.21h 2320  19.21t 2242  19.21vv 45304  alrimd 2251  alrimdd 2250  alrimdh 1896  alrimdv 1962  alrimi 2249  alrimih 1857  alrimiv 1960  alrimivv 1961  bj-alrimdh 37416  hbralrimi 3152  r19.21be 3255  r19.21bi 3254  ralrimd 3267  ralrimdv 3160  ralrimdva 3162  ralrimdvv 3206  ralrimdvva 3217  ralrimi 3260  ralrimia 3261  ralrimiv 3153  ralrimiva 3154  ralrimivv 3203  ralrimivva 3205  ralrimivvva 3208  ralrimivw 3158
[Margaris] p. 90Theorem 19.222exim 45307  2eximdv 1952  bj-exim 37431  exim 1867  eximd 2252  eximdh 1897  eximdv 1950  rexim 3103  reximd2a 3272  reximdai 3264  reximdd 46084  reximddv 3178  reximddv2 3221  reximddv3 3179  reximdv 3177  reximdv2 3172  reximdva 3175  reximdvai 3173  reximdvva 3210  reximi2 3095
[Margaris] p. 90Theorem 19.2319.23 2247  19.23bi 2227  19.23h 2321  19.23t 2246  exlimdv 1966  exlimdvv 1967  exlimexi 45451  exlimiv 1963  exlimivv 1965  rexlimd3 46080  rexlimdv 3161  rexlimdv3a 3167  rexlimdva 3163  rexlimdva2 3165  rexlimdvaa 3164  rexlimdvv 3218  rexlimdvva 3219  rexlimdvvva 3220  rexlimdvw 3168  rexlimiv 3156  rexlimiva 3155  rexlimivv 3204
[Margaris] p. 90Theorem 19.2419.24 2024
[Margaris] p. 90Theorem 19.2519.25 1913
[Margaris] p. 90Theorem 19.2619.26 1903
[Margaris] p. 90Theorem 19.2719.27 2263  r19.27z 4465  r19.27zv 4466
[Margaris] p. 90Theorem 19.2819.28 2264  19.28vv 45314  r19.28z 4457  r19.28zf 46095  r19.28zv 4461  rr19.28v 3621
[Margaris] p. 90Theorem 19.2919.29 1906  r19.29d2r 3149  r19.29imd 3127
[Margaris] p. 90Theorem 19.3019.30 1914
[Margaris] p. 90Theorem 19.3119.31 2270  19.31vv 45312
[Margaris] p. 90Theorem 19.3219.32 2269  r19.32 48090
[Margaris] p. 90Theorem 19.3319.33-2 45310  19.33 1917
[Margaris] p. 90Theorem 19.3419.34 2025
[Margaris] p. 90Theorem 19.3519.35 1910
[Margaris] p. 90Theorem 19.3619.36 2266  19.36vv 45311  r19.36zv 4467
[Margaris] p. 90Theorem 19.3719.37 2268  19.37vv 45313  r19.37zv 4462
[Margaris] p. 90Theorem 19.3819.38 1872
[Margaris] p. 90Theorem 19.3919.39 2023
[Margaris] p. 90Theorem 19.4019.40-2 1920  19.40 1919  r19.40 3128
[Margaris] p. 90Theorem 19.4119.41 2271  19.41rg 45477
[Margaris] p. 90Theorem 19.4219.42 2272
[Margaris] p. 90Theorem 19.4319.43 1915
[Margaris] p. 90Theorem 19.4419.44 2273  r19.44zv 4464
[Margaris] p. 90Theorem 19.4519.45 2274  r19.45zv 4463
[Margaris] p. 110Exercise 2(b)eu1 2635
[Mayet] p. 370Remarkjpi 32806  largei 32803  stri 32793
[Mayet3] p. 9Definition of CH-statesdf-hst 32748  ishst 32750
[Mayet3] p. 10Theoremhstrbi 32802  hstri 32801
[Mayet3] p. 1223Theorem 4.1mayete3i 32264
[Mayet3] p. 1240Theorem 7.1mayetes3i 32265
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32814
[MegPav2000] p. 2345Definition 3.4-1chintcl 31868  chsupcl 31876
[MegPav2000] p. 2345Definition 3.4-2hatomic 32896
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32890
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32917
[MegPav2000] p. 2366Figure 7pl42N 40960
[MegPav2002] p. 362Lemma 2.2latj31 18623  latj32 18621  latjass 18619
[Megill] p. 444Axiom C5ax-5 1943  ax5ALT 39884
[Megill] p. 444Section 7conventions 30935
[Megill] p. 445Lemma L12aecom-o 39878  ax-c11n 39865  axc11n 2455
[Megill] p. 446Lemma L17equtrr 2055
[Megill] p. 446Lemma L18ax6fromc10 39873
[Megill] p. 446Lemma L19hbnae-o 39905  hbnae 2461
[Megill] p. 447Remark 9.1dfsb1 2510  sbid 2290  sbidd-misc 50734  sbidd 50733
[Megill] p. 448Remark 9.6axc14 2492
[Megill] p. 448Scheme C4'ax-c4 39861
[Megill] p. 448Scheme C5'ax-c5 39860  sp 2219
[Megill] p. 448Scheme C6'ax-11 2194
[Megill] p. 448Scheme C7'ax-c7 39862
[Megill] p. 448Scheme C8'ax-7 2041
[Megill] p. 448Scheme C9'ax-c9 39867
[Megill] p. 448Scheme C10'ax-6 2000  ax-c10 39863
[Megill] p. 448Scheme C11'ax-c11 39864
[Megill] p. 448Scheme C12'ax-8 2147
[Megill] p. 448Scheme C13'ax-9 2155
[Megill] p. 448Scheme C14'ax-c14 39868
[Megill] p. 448Scheme C15'ax-c15 39866
[Megill] p. 448Scheme C16'ax-c16 39869
[Megill] p. 448Theorem 9.4dral1-o 39881  dral1 2468  dral2-o 39907  dral2 2467  drex1 2470  drex2 2471  drsb1 2524  drsb2 2300
[Megill] p. 449Theorem 9.7sbcom2 2209  sbequ 2120  sbid2v 2538
[Megill] p. 450Example in Appendixhba1-o 39874  hba1 2326
[Mendelson] p. 35Axiom A3hirstL-ax3 47884
[Mendelson] p. 36Lemma 1.8idALT 24
[Mendelson] p. 69Axiom 4rspsbc 3825  rspsbca 3826  stdpc4 2105
[Mendelson] p. 69Axiom 5ax-c4 39861  ra4 3832  stdpc5 2244
[Mendelson] p. 81Rule Cexlimiv 1963
[Mendelson] p. 95Axiom 6stdpc6 2061
[Mendelson] p. 95Axiom 7stdpc7 2285
[Mendelson] p. 225Axiom system NBGru 3737
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5483
[Mendelson] p. 231Exercise 4.10(k)inv1 4347
[Mendelson] p. 231Exercise 4.10(l)unv 4348
[Mendelson] p. 231Exercise 4.10(n)dfin3 4222
[Mendelson] p. 231Exercise 4.10(o)df-nul 4279
[Mendelson] p. 231Exercise 4.10(q)dfin4 4223
[Mendelson] p. 231Exercise 4.10(s)ddif 4087
[Mendelson] p. 231Definition of uniondfun3 4221
[Mendelson] p. 235Exercise 4.12(c)univ 5418
[Mendelson] p. 235Exercise 4.12(d)pwv 4863
[Mendelson] p. 235Exercise 4.12(j)pwin 5538
[Mendelson] p. 235Exercise 4.12(k)pwunss 4574
[Mendelson] p. 235Exercise 4.12(l)pwssun 5539
[Mendelson] p. 235Exercise 4.12(n)uniin 4890
[Mendelson] p. 235Exercise 4.12(p)reli 5800
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6260
[Mendelson] p. 244Proposition 4.8(g)epweon 7772
[Mendelson] p. 246Definition of successordf-suc 6357
[Mendelson] p. 250Exercise 4.36oelim2 8582
[Mendelson] p. 254Proposition 4.22(b)xpen 9137
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9058  xpsneng 9059
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9065  xpcomeng 9066
[Mendelson] p. 254Proposition 4.22(e)xpassen 9068
[Mendelson] p. 255Definitionbrsdom 8979
[Mendelson] p. 255Exercise 4.39endisj 9061
[Mendelson] p. 255Exercise 4.41mapprc 8829
[Mendelson] p. 255Exercise 4.43mapsnen 9043  mapsnend 9042
[Mendelson] p. 255Exercise 4.45mapunen 9143
[Mendelson] p. 255Exercise 4.47xpmapen 9142
[Mendelson] p. 255Exercise 4.42(a)map0e 8888
[Mendelson] p. 255Exercise 4.42(b)map1 9046
[Mendelson] p. 257Proposition 4.24(a)undom 9062
[Mendelson] p. 258Exercise 4.56(c)djuassen 10229  djucomen 10228
[Mendelson] p. 258Exercise 4.56(f)djudom1 10233
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10227
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8517
[Mendelson] p. 266Proposition 4.34(f)oaordex 8544
[Mendelson] p. 275Proposition 4.42(d)entri3 10615
[Mendelson] p. 281Definitiondf-r1 9746
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9795
[Mendelson] p. 287Axiom system MKru 3737
[MertziosUnger] p. 152Definitiondf-frgr 30794
[MertziosUnger] p. 153Remark 1frgrconngr 30829
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30831  vdgn1frgrv3 30832
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30833
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30826
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30819  2pthfrgrrn 30817  2pthfrgrrn2 30818
[Mittelstaedt] p. 9Definitiondf-oc 31788
[Monk1] p. 22Remarkconventions 30935
[Monk1] p. 22Theorem 3.1conventions 30935
[Monk1] p. 26Theorem 2.8(vii)ssin 4183
[Monk1] p. 33Theorem 3.2(i)ssrel 5755  ssrelf 33143
[Monk1] p. 33Theorem 3.2(ii)eqrel 5756
[Monk1] p. 34Definition 3.3df-opab 5167
[Monk1] p. 36Theorem 3.7(i)coi1 6253  coi2 6254
[Monk1] p. 36Theorem 3.8(v)dm0 5898  rn0 5904
[Monk1] p. 36Theorem 3.7(ii)cnvi 5859
[Monk1] p. 37Theorem 3.13(i)relxp 5665
[Monk1] p. 37Theorem 3.13(x)dmxp 5907  rnxp 6157
[Monk1] p. 37Theorem 3.13(ii)0xp 5746  xp0 5747
[Monk1] p. 38Theorem 3.16(ii)ima0 6067
[Monk1] p. 38Theorem 3.16(viii)imai 6064
[Monk1] p. 39Theorem 3.17imaex 7909  imaexg 7908
[Monk1] p. 39Theorem 3.16(xi)imassrn 6061
[Monk1] p. 41Theorem 4.3(i)fnopfv 7063  funfvop 7037
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6927
[Monk1] p. 42Theorem 4.4(iii)fvelima 6938
[Monk1] p. 43Theorem 4.6funun 6574
[Monk1] p. 43Theorem 4.8(iv)dff13 7246  dff13f 7247
[Monk1] p. 46Theorem 4.15(v)funex 7213  funrnex 7949
[Monk1] p. 50Definition 5.4fniunfv 7239
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6217
[Monk1] p. 52Theorem 5.11(viii)ssint 4923
[Monk1] p. 52Definition 5.13 (i)1stval2 8001  df-1st 7984
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8002  df-2nd 7985
[Monk1] p. 112Theorem 15.17(v)ranksn 9841  ranksnb 9810
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9842
[Monk1] p. 112Theorem 15.17(iii)rankun 9843  rankunb 9837
[Monk1] p. 113Theorem 15.18r1val3 9823
[Monk1] p. 113Definition 15.19df-r1 9746  r1val2 9822
[Monk1] p. 117Lemmazorn2 10556  zorn2g 10553
[Monk1] p. 133Theorem 18.11cardom 10039
[Monk1] p. 133Theorem 18.12canth3 10617
[Monk1] p. 133Theorem 18.14carduni 10034
[Monk2] p. 105Axiom C4ax-4 1842
[Monk2] p. 105Axiom C7ax-7 2041
[Monk2] p. 105Axiom C8ax-12 2213  ax-c15 39866  ax12v2 2215
[Monk2] p. 108Lemma 5ax-c4 39861
[Monk2] p. 109Lemma 12ax-11 2194
[Monk2] p. 109Lemma 15equvini 2484  equvinv 2062  eqvinop 5455
[Monk2] p. 113Axiom C5-1ax-5 1943  ax5ALT 39884
[Monk2] p. 113Axiom C5-2ax-10 2178
[Monk2] p. 113Axiom C5-3ax-11 2194
[Monk2] p. 114Lemma 21sp 2219
[Monk2] p. 114Lemma 22axc4 2351  hba1-o 39874  hba1 2326
[Monk2] p. 114Lemma 23nfia1 2190
[Monk2] p. 114Lemma 24nfa2 2210  nfra2 3361  nfra2w 3298
[Moore] p. 53Part Idf-mre 17718
[Munkres] p. 77Example 2distop 23275  indistop 23282  indistopon 23281
[Munkres] p. 77Example 3fctop 23284  fctop2 23285
[Munkres] p. 77Example 4cctop 23286
[Munkres] p. 78Definition of basisdf-bases 23226  isbasis3g 23229
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17576  tgval2 23236
[Munkres] p. 79Remarktgcl 23249
[Munkres] p. 80Lemma 2.1tgval3 23243
[Munkres] p. 80Lemma 2.2tgss2 23267  tgss3 23266
[Munkres] p. 81Lemma 2.3basgen 23268  basgen2 23269
[Munkres] p. 83Exercise 3topdifinf 38192  topdifinfeq 38193  topdifinffin 38191  topdifinfindis 38189
[Munkres] p. 89Definition of subspace topologyresttop 23440
[Munkres] p. 93Theorem 6.1(1)0cld 23318  topcld 23315
[Munkres] p. 93Theorem 6.1(2)iincld 23319
[Munkres] p. 93Theorem 6.1(3)uncld 23321
[Munkres] p. 94Definition of closureclsval 23317
[Munkres] p. 94Definition of interiorntrval 23316
[Munkres] p. 95Theorem 6.5(a)clsndisj 23355  elcls 23353
[Munkres] p. 95Theorem 6.5(b)elcls3 23363
[Munkres] p. 97Theorem 6.6clslp 23428  neindisj 23397
[Munkres] p. 97Corollary 6.7cldlp 23430
[Munkres] p. 97Definition of limit pointislp2 23425  lpval 23419
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23595
[Munkres] p. 102Definition of continuous functiondf-cn 23507  iscn 23515  iscn2 23518
[Munkres] p. 107Theorem 7.2(g)cncnp 23560  cncnp2 23561  cncnpi 23558  df-cnp 23508  iscnp 23517  iscnp2 23519
[Munkres] p. 127Theorem 10.1metcn 24824
[Munkres] p. 128Theorem 10.3metcn4 25594
[Nathanson] p. 123Remarkreprgt 35185  reprinfz1 35186  reprlt 35183
[Nathanson] p. 123Definitiondf-repr 35173
[Nathanson] p. 123Chapter 5.1circlemethnat 35205
[Nathanson] p. 123Propositionbreprexp 35197  breprexpnat 35198  itgexpif 35170
[NielsenChuang] p. 195Equation 4.73unierri 32640
[OeSilva] p. 2042Section 2ax-bgbltosilva 48830
[Pfenning] p. 17Definition XMnatded 30938
[Pfenning] p. 17Definition NNCnatded 30938  notnotrd 134
[Pfenning] p. 17Definition ` `Cnatded 30938
[Pfenning] p. 18Rule"natded 30938
[Pfenning] p. 18Definition /\Inatded 30938
[Pfenning] p. 18Definition ` `Enatded 30938  natded 30938  natded 30938  natded 30938  natded 30938
[Pfenning] p. 18Definition ` `Inatded 30938  natded 30938  natded 30938  natded 30938  natded 30938
[Pfenning] p. 18Definition ` `ELnatded 30938
[Pfenning] p. 18Definition ` `ERnatded 30938
[Pfenning] p. 18Definition ` `Ea,unatded 30938
[Pfenning] p. 18Definition ` `IRnatded 30938
[Pfenning] p. 18Definition ` `Ianatded 30938
[Pfenning] p. 127Definition =Enatded 30938
[Pfenning] p. 127Definition =Inatded 30938
[Ponnusamy] p. 361Theorem 6.44cphip0l 25485  df-dip 31237  dip0l 31254  ip0l 21904
[Ponnusamy] p. 361Equation 6.45cphipval 25526  ipval 31239
[Ponnusamy] p. 362Equation I1dipcj 31250  ipcj 21902
[Ponnusamy] p. 362Equation I3cphdir 25488  dipdir 31378  ipdir 21907  ipdiri 31366
[Ponnusamy] p. 362Equation I4ipidsq 31246  nmsq 25477
[Ponnusamy] p. 362Equation 6.46ip0i 31361
[Ponnusamy] p. 362Equation 6.47ip1i 31363
[Ponnusamy] p. 362Equation 6.48ip2i 31364
[Ponnusamy] p. 363Equation I2cphass 25494  dipass 31381  ipass 21913  ipassi 31377
[Prugovecki] p. 186Definition of brabraval 32480  df-bra 32386
[Prugovecki] p. 376Equation 8.1df-kb 32387  kbval 32490
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32918
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40865
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32932  atcvat4i 32933  cvrat3 40419  cvrat4 40420  lsatcvat3 40029
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32818  cvrval 40246  df-cv 32815  df-lcv 39996  lspsncv0 21386
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40877
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40878
[Quine] p. 16Definition 2.1df-clab 2739  rabid 3432  rabidd 46091  wl-df.clab 38350
[Quine] p. 17Definition 2.1''dfsb7 2312
[Quine] p. 18Definition 2.7df-cleq 2752  wl-df.cleq 38351
[Quine] p. 19Definition 2.9conventions 30935  df-v 3452
[Quine] p. 34Theorem 5.1eqabb 2899
[Quine] p. 35Theorem 5.2abid1 2896  abid2f 2952
[Quine] p. 40Theorem 6.1sb5 2309
[Quine] p. 40Theorem 6.2sb6 2122  sbalex 2278
[Quine] p. 41Theorem 6.3df-clel 2835  wl-df.clel 38354
[Quine] p. 41Theorem 6.4eqid 2760  eqid1 31002
[Quine] p. 41Theorem 6.5eqcom 2767
[Quine] p. 42Theorem 6.6df-sbc 3739
[Quine] p. 42Theorem 6.7dfsbcq 3740  dfsbcq2 3741
[Quine] p. 43Theorem 6.8vex 3454
[Quine] p. 43Theorem 6.9isset 3464
[Quine] p. 44Theorem 7.3spcgf 3545  spcgv 3550  spcimgf 3513
[Quine] p. 44Theorem 6.11spsbc 3751  spsbcd 3752
[Quine] p. 44Theorem 6.12elex 3471
[Quine] p. 44Theorem 6.13elab 3632  elabg 3629  elabgf 3627
[Quine] p. 44Theorem 6.14noel 4283
[Quine] p. 48Theorem 7.2snprc 4677
[Quine] p. 48Definition 7.1df-pr 4586  df-sn 4584
[Quine] p. 49Theorem 7.4snss 4744  snssg 4743
[Quine] p. 49Theorem 7.5prss 4780  prssg 4779
[Quine] p. 49Theorem 7.6prid1 4722  prid1g 4720  prid2 4723  prid2g 4721  snid 4622  snidg 4620
[Quine] p. 51Theorem 7.12snex 5396
[Quine] p. 51Theorem 7.13prex 5395
[Quine] p. 53Theorem 8.2unisn 4885  unisnALT 45852  unisng 4884
[Quine] p. 53Theorem 8.3uniun 4889
[Quine] p. 54Theorem 8.6elssuni 4898
[Quine] p. 54Theorem 8.7uni0 4895
[Quine] p. 56Theorem 8.17uniabio 6497
[Quine] p. 56Definition 8.18dfaiota2 48078  dfiota2 6484
[Quine] p. 57Theorem 8.19aiotaval 48087  iotaval 6501
[Quine] p. 57Theorem 8.22iotanul 6507
[Quine] p. 58Theorem 8.23iotaex 6503
[Quine] p. 58Definition 9.1df-op 4590
[Quine] p. 61Theorem 9.5opabid 5495  opabidw 5494  opelopab 5513  opelopaba 5506  opelopabaf 5515  opelopabf 5516  opelopabg 5509  opelopabga 5503  opelopabgf 5511  oprabid 7440  oprabidw 7439
[Quine] p. 64Definition 9.11df-xp 5653
[Quine] p. 64Definition 9.12df-cnv 5655
[Quine] p. 64Definition 9.15df-id 5542
[Quine] p. 65Theorem 10.3fun0 6593
[Quine] p. 65Theorem 10.4funi 6560
[Quine] p. 65Theorem 10.5funsn 6581  funsng 6579
[Quine] p. 65Definition 10.1df-fun 6529
[Quine] p. 65Definition 10.2args 6082  dffv4 6870
[Quine] p. 68Definition 10.11conventions 30935  df-fv 6535  fv2 6868
[Quine] p. 124Theorem 17.3nn0opth2 14384  nn0opth2i 14383  nn0opthi 14382  omopthi 8648
[Quine] p. 177Definition 25.2df-rdg 8396
[Quine] p. 232Equation icarddom 10610
[Quine] p. 284Axiom 39(vi)funimaex 6615  funimaexg 6614
[Quine] p. 331Axiom system NFru 3737
[ReedSimon] p. 36Definition (iii)ax-his3 31620
[ReedSimon] p. 63Exercise 4(a)df-dip 31237  polid 31695  polid2i 31693  polidi 31694
[ReedSimon] p. 63Exercise 4(b)df-ph 31349
[ReedSimon] p. 195Remarklnophm 32555  lnophmi 32554
[Retherford] p. 49Exercise 1(i)leopadd 32668
[Retherford] p. 49Exercise 1(ii)leopmul 32670  leopmuli 32669
[Retherford] p. 49Exercise 1(iv)leoptr 32673
[Retherford] p. 49Definition VI.1df-leop 32388  leoppos 32662
[Retherford] p. 49Exercise 1(iii)leoptri 32672
[Retherford] p. 49Definition of operator orderingleop3 32661
[Ribenboim] p. 181Remarknprmdvdsfacm1 48631
[Ribenboim], p. 181Statementppivalnn 48639
[Roman] p. 4Definitiondf-dmat 22767  df-dmatalt 49432
[Roman] p. 18Part Preliminariesdf-rng 20337
[Roman] p. 19Part Preliminariesdf-ring 20423
[Roman] p. 46Theorem 1.6isldepslvec2 49519
[Roman] p. 112Noteisldepslvec2 49519  ldepsnlinc 49542  zlmodzxznm 49531
[Roman] p. 112Examplezlmodzxzequa 49530  zlmodzxzequap 49533  zlmodzxzldep 49538
[Roman] p. 170Theorem 7.8cayleyhamilton 23170
[Rosenlicht] p. 80Theoremheicant 38493
[Rosser] p. 281Definitiondf-op 4590
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 35209
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 35210
[Rotman] p. 28Remarkpgrpgt2nabl 49400  pmtr3ncom 19651
[Rotman] p. 31Theorem 3.4symggen2 19647
[Rotman] p. 42Theorem 3.15cayley 19590  cayleyth 19591
[Rudin] p. 164Equation 27efcan 16230
[Rudin] p. 164Equation 30efzval 16238
[Rudin] p. 167Equation 48absefi 16332
[Russell1905] p. 482Example of "the fatherdfalseu2 50854
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1804
[Sanford] p. 39Rule 4mptxor 1802
[Sanford] p. 40Rule 1mptnan 1801
[Schechter] p. 51Definition of antisymmetryintasym 6103
[Schechter] p. 51Definition of irreflexivityintirr 6106
[Schechter] p. 51Definition of symmetrycnvsym 6102
[Schechter] p. 51Definition of transitivitycotr 6100
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17718
[Schechter] p. 79Definition of Moore closuredf-mrc 17719
[Schechter] p. 82Section 4.5df-mrc 17719
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17721
[Schechter] p. 139Definition AC3dfac9 10187
[Schechter] p. 141Definition (MC)dfac11 44007
[Schechter] p. 149Axiom DC1ax-dc 10496  axdc3 10504
[Schechter] p. 187Definition of "ring with unit"isring 20425  isrngo 38751
[Schechter] p. 276Remark 11.6.espan0 32078
[Schechter] p. 276Definition of spandf-span 31845  spanval 31869
[Schechter] p. 428Definition 15.35bastop1 23273
[Schloeder] p. 1Lemma 1.3onelon 6376  onelond 36870  onelord 44196  ordelon 6375  ordelord 6373
[Schloeder] p. 1Lemma 1.7onepsuc 44197  sucidg 6435
[Schloeder] p. 1Remark 1.50elon 6407  onsuc 7807  ord0 6406  ordsuci 7805
[Schloeder] p. 1Theorem 1.9epsoon 44198
[Schloeder] p. 1Definition 1.1dftr5 5215
[Schloeder] p. 1Definition 1.2dford3 43973  elon2 6362
[Schloeder] p. 1Definition 1.4df-suc 6357
[Schloeder] p. 1Definition 1.6epel 5550  epelg 5548
[Schloeder] p. 1Theorem 1.9(i)elirr 9572  epirron 44199  ordirr 6369
[Schloeder] p. 1Theorem 1.9(ii)oneltr 44201  oneptr 44200  ontr1 6399
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6395  oneptri 44202  ordtri3or 6384
[Schloeder] p. 2Lemma 1.10ondif1 8487  ord0eln0 6408
[Schloeder] p. 2Lemma 1.13elsuci 6421  onsucss 44211  trsucss 6442
[Schloeder] p. 2Lemma 1.14ordsucss 7812
[Schloeder] p. 2Lemma 1.15onnbtwn 6448  ordnbtwn 6447
[Schloeder] p. 2Lemma 1.16orddif0suc 44213  ordnexbtwnsuc 44212
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10451  onsucf1lem 44214  onsucf1o 44217  onsucf1olem 44215  onsucrn 44216
[Schloeder] p. 2Lemma 1.18dflim7 44218
[Schloeder] p. 2Remark 1.12ordzsl 7839
[Schloeder] p. 2Theorem 1.10ondif1i 44207  ordne0gt0 44206
[Schloeder] p. 2Definition 1.11dflim6 44209  limnsuc 44210  onsucelab 44208
[Schloeder] p. 3Remark 1.21omex 9622
[Schloeder] p. 3Theorem 1.19tfinds 7854
[Schloeder] p. 3Theorem 1.22omelon 9625  ordom 7870
[Schloeder] p. 3Definition 1.20dfom3 9626
[Schloeder] p. 4Lemma 2.21onn 8627
[Schloeder] p. 4Lemma 2.7ssonuni 7777  ssorduni 7776
[Schloeder] p. 4Remark 2.4oa1suc 8517
[Schloeder] p. 4Theorem 1.23dfom5 9629  limom 7876
[Schloeder] p. 4Definition 2.1df-1o 8454  df1o2 8461
[Schloeder] p. 4Definition 2.3oa0 8502  oa0suclim 44220  oalim 8518  oasuc 8510
[Schloeder] p. 4Definition 2.5om0 8503  om0suclim 44221  omlim 8519  omsuc 8512
[Schloeder] p. 4Definition 2.6oe0 8508  oe0m1 8507  oe0suclim 44222  oelim 8520  oesuc 8513
[Schloeder] p. 5Lemma 2.10onsupuni 44174
[Schloeder] p. 5Lemma 2.11onsupsucismax 44224
[Schloeder] p. 5Lemma 2.12onsssupeqcond 44225
[Schloeder] p. 5Lemma 2.13limexissup 44226  limexissupab 44228  limiun 44227  limuni 6414
[Schloeder] p. 5Lemma 2.14oa0r 8524
[Schloeder] p. 5Lemma 2.15om1 8528  om1om1r 44229  om1r 8529
[Schloeder] p. 5Remark 2.8oacl 8521  oaomoecl 44223  oecl 8523  omcl 8522
[Schloeder] p. 5Definition 2.9onsupintrab 44176
[Schloeder] p. 6Lemma 2.16oe1 8530
[Schloeder] p. 6Lemma 2.17oe1m 8531
[Schloeder] p. 6Lemma 2.18oe0rif 44230
[Schloeder] p. 6Theorem 2.19oasubex 44231
[Schloeder] p. 6Theorem 2.20nnacl 8598  nnamecl 44232  nnecl 8600  nnmcl 8599
[Schloeder] p. 7Lemma 3.1onsucwordi 44233
[Schloeder] p. 7Lemma 3.2oaword1 8538
[Schloeder] p. 7Lemma 3.3oaword2 8539
[Schloeder] p. 7Lemma 3.4oalimcl 8546
[Schloeder] p. 7Lemma 3.5oaltublim 44235
[Schloeder] p. 8Lemma 3.6oaordi3 44236
[Schloeder] p. 8Lemma 3.81oaomeqom 44238
[Schloeder] p. 8Lemma 3.10oa00 8545
[Schloeder] p. 8Lemma 3.11omge1 44242  omword1 8559
[Schloeder] p. 8Remark 3.9oaordnr 44241  oaordnrex 44240
[Schloeder] p. 8Theorem 3.7oaord3 44237
[Schloeder] p. 9Lemma 3.12omge2 44243  omword2 8560
[Schloeder] p. 9Lemma 3.13omlim2 44244
[Schloeder] p. 9Lemma 3.14omord2lim 44245
[Schloeder] p. 9Lemma 3.15omord2i 44246  omordi 8552
[Schloeder] p. 9Theorem 3.16omord 8554  omord2com 44247
[Schloeder] p. 10Lemma 3.172omomeqom 44248  df-2o 8455
[Schloeder] p. 10Lemma 3.19oege1 44251  oewordi 8578
[Schloeder] p. 10Lemma 3.20oege2 44252  oeworde 8580
[Schloeder] p. 10Lemma 3.21rp-oelim2 44253
[Schloeder] p. 10Lemma 3.22oeord2lim 44254
[Schloeder] p. 10Remark 3.18omnord1 44250  omnord1ex 44249
[Schloeder] p. 11Lemma 3.23oeord2i 44255
[Schloeder] p. 11Lemma 3.25nnoeomeqom 44257
[Schloeder] p. 11Remark 3.26oenord1 44261  oenord1ex 44260
[Schloeder] p. 11Theorem 4.1oaomoencom 44262
[Schloeder] p. 11Theorem 4.2oaass 8547
[Schloeder] p. 11Theorem 3.24oeord2com 44256
[Schloeder] p. 12Theorem 4.3odi 8565
[Schloeder] p. 13Theorem 4.4omass 8566
[Schloeder] p. 14Remark 4.6oenass 44264
[Schloeder] p. 14Theorem 4.7oeoa 8584
[Schloeder] p. 15Lemma 5.1cantnftermord 44265
[Schloeder] p. 15Lemma 5.2cantnfub 44266  cantnfub2 44267
[Schloeder] p. 16Theorem 5.3cantnf2 44270
[Schwabhauser] p. 10Axiom A1axcgrrflx 29426  axtgcgrrflx 28858
[Schwabhauser] p. 10Axiom A2axcgrtr 29427
[Schwabhauser] p. 10Axiom A3axcgrid 29428  axtgcgrid 28859
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28844
[Schwabhauser] p. 11Axiom A4axsegcon 29439  axtgsegcon 28860  df-trkgcb 28846
[Schwabhauser] p. 11Axiom A5ax5seg 29450  axtg5seg 28861  df-trkgcb 28846
[Schwabhauser] p. 11Axiom A6axbtwnid 29451  axtgbtwnid 28862  df-trkgb 28845
[Schwabhauser] p. 12Axiom A7axpasch 29453  axtgpasch 28863  df-trkgb 28845
[Schwabhauser] p. 12Axiom A8axlowdim2 29472  df-trkg2d 35229
[Schwabhauser] p. 13Axiom A8axtglowdim2 28866
[Schwabhauser] p. 13Axiom A9axtgupdim2 28867  df-trkg2d 35229
[Schwabhauser] p. 13Axiom A10axeuclid 29475  axtgeucl 28868  df-trkge 28847
[Schwabhauser] p. 13Axiom A11axcont 29488  axtgcont 28865  axtgcont1 28864  df-trkgb 28845
[Schwabhauser] p. 24Theorem A10prlngmo 29366
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36674
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36676
[Schwabhauser] p. 27Theorem 2.3cgrtr 36679
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36683
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36684  tgcgrcomimp 28873  tgcgrcoml 28875  tgcgrcomr 28874
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36689  tgcgrtriv 28880
[Schwabhauser] p. 28Theorem 2.105segofs 36693  tg5segofs 35240
[Schwabhauser] p. 28Definition 2.10df-afs 35237  df-ofs 36670
[Schwabhauser] p. 29Theorem 2.11cgrextend 36695  tgcgrextend 28881
[Schwabhauser] p. 29Theorem 2.12segconeq 36697  tgsegconeq 28882
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36709  btwntriv2 36699  tgbtwntriv2 28884
[Schwabhauser] p. 30Theorem 3.2btwncomim 36700  tgbtwncom 28885
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36703  tgbtwntriv1 28888
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36704  tgbtwnswapid 28889
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36710  btwnintr 36706  tgbtwnexch2 28893  tgbtwnintr 28890
[Schwabhauser] p. 30Theorem 3.6btwnexch 36712  btwnexch3 36707  tgbtwnexch 28895  tgbtwnexch3 28891
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36711  tgbtwnouttr 28894  tgbtwnouttr2 28892
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29471
[Schwabhauser] p. 32Theorem 3.14btwndiff 36714  tgbtwndiff 28903
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28896  trisegint 36715
[Schwabhauser] p. 34Theorem 4.2ifscgr 36731  tgifscgr 28905
[Schwabhauser] p. 34Theorem 4.11colcom 28955  colrot1 28956  colrot2 28957  lncom 29024  lnrot1 29025  lnrot2 29026
[Schwabhauser] p. 34Definition 4.1df-ifs 36727
[Schwabhauser] p. 35Theorem 4.3cgrsub 36732  tgcgrsub 28906
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36742  tgcgrxfr 28915
[Schwabhauser] p. 35Statement 4.4ercgrg 28914
[Schwabhauser] p. 35Definition 4.4df-cgr3 36728  df-cgrg 28908
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28908
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36743  tgbtwnxfr 28927
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36749  colinearperm2 36751  colinearperm3 36750  colinearperm4 36752  colinearperm5 36753
[Schwabhauser] p. 36Definition 4.8df-ismt 28930
[Schwabhauser] p. 36Definition 4.10df-colinear 36726  tgellng 28950  tglng 28943
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36754
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36762  lnxfr 28963
[Schwabhauser] p. 37Theorem 4.14lineext 36763  lnext 28964
[Schwabhauser] p. 37Theorem 4.16fscgr 36767  tgfscgr 28965
[Schwabhauser] p. 37Theorem 4.17linecgr 36768  lncgr 28966
[Schwabhauser] p. 37Definition 4.15df-fs 36729
[Schwabhauser] p. 38Theorem 4.18lineid 36770  lnid 28967
[Schwabhauser] p. 38Theorem 4.19idinside 36771  tgidinside 28968
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36788  tgbtwnconn1 28972
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36789  tgbtwnconn2 28973
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36790  tgbtwnconn3 28974
[Schwabhauser] p. 41Theorem 5.5brsegle2 36796
[Schwabhauser] p. 41Definition 5.4df-segle 36794  legov 28982
[Schwabhauser] p. 41Definition 5.5legov2 28983
[Schwabhauser] p. 42Remark 5.13legso 28996
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36797
[Schwabhauser] p. 42Theorem 5.7seglerflx 36799
[Schwabhauser] p. 42Theorem 5.8segletr 36801
[Schwabhauser] p. 42Theorem 5.9segleantisym 36802
[Schwabhauser] p. 42Theorem 5.10seglelin 36803
[Schwabhauser] p. 42Theorem 5.11seglemin 36800
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36805
[Schwabhauser] p. 42Proposition 5.7legid 28984
[Schwabhauser] p. 42Proposition 5.8legtrd 28986
[Schwabhauser] p. 42Proposition 5.9legtri3 28987
[Schwabhauser] p. 42Proposition 5.10legtrid 28988
[Schwabhauser] p. 42Proposition 5.11leg0 28989
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36812
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36813
[Schwabhauser] p. 43Theorem 6.4broutsideof 36808  df-outsideof 36807
[Schwabhauser] p. 43Definition 6.1broutsideof2 36809  ishlg 29002
[Schwabhauser] p. 44Theorem 6.4hlln 29007
[Schwabhauser] p. 44Theorem 6.5hlid 29009  outsideofrflx 36814
[Schwabhauser] p. 44Theorem 6.6hlcomb 29003  hlcomd 29004  outsideofcom 36815
[Schwabhauser] p. 44Theorem 6.7hltr 29010  outsideoftr 36816
[Schwabhauser] p. 44Theorem 6.11hlcgreq 29019  hlcgreu 29018  outsideofeu 36818
[Schwabhauser] p. 44Definition 6.8df-ray 36825
[Schwabhauser] p. 45Part 2df-lines2 36826
[Schwabhauser] p. 45Theorem 6.13outsidele 36819
[Schwabhauser] p. 45Theorem 6.15lineunray 36834
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36835  tglineelsb2 29034
[Schwabhauser] p. 45Theorem 6.17linecom 36837  linerflx1 36836  linerflx2 36838  tglinecom 29037  tglinerflx1 29035  tglinerflx2 29036
[Schwabhauser] p. 45Theorem 6.18linethru 36840  tglinethru 29038
[Schwabhauser] p. 45Definition 6.14df-line2 36824  tglng 28943
[Schwabhauser] p. 45Proposition 6.13legbtwn 28991
[Schwabhauser] p. 46Theorem 6.19linethrueu 36843  tglinethrueu 29041
[Schwabhauser] p. 46Theorem 6.21lineintmo 36844  tglineineq 29045  tglineinsn 29046  tglineinteq 29048  tglineintmo 29044
[Schwabhauser] p. 46Theorem 6.23colline 29052
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 29053
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 29054
[Schwabhauser] p. 49Theorem 7.3mirinv 29072
[Schwabhauser] p. 49Theorem 7.7mirmir 29068
[Schwabhauser] p. 49Theorem 7.8mirreu3 29060
[Schwabhauser] p. 49Definition 7.5df-mir 29059  ismir 29065  mirbtwn 29064  mircgr 29063  mirfv 29062  mirval 29061
[Schwabhauser] p. 50Theorem 7.8mirreu 29070
[Schwabhauser] p. 50Theorem 7.9mireq 29071
[Schwabhauser] p. 50Theorem 7.10mirinv 29072
[Schwabhauser] p. 50Theorem 7.11mirf1o 29075
[Schwabhauser] p. 50Theorem 7.13miriso 29076
[Schwabhauser] p. 51Theorem 7.14mirmot 29081
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 29078  mirbtwni 29077
[Schwabhauser] p. 51Theorem 7.16mircgrs 29079
[Schwabhauser] p. 51Theorem 7.17miduniq 29091
[Schwabhauser] p. 52Lemma 7.21symquadlem 29095  symquadmid 29238
[Schwabhauser] p. 52Theorem 7.18miduniq1 29092
[Schwabhauser] p. 52Theorem 7.19miduniq2 29093
[Schwabhauser] p. 52Theorem 7.20colmid 29094
[Schwabhauser] p. 53Lemma 7.22krippen 29097
[Schwabhauser] p. 55Lemma 7.25midexlem 29098
[Schwabhauser] p. 57Theorem 8.2ragcom 29107
[Schwabhauser] p. 57Definition 8.1df-rag 29103  israg 29106
[Schwabhauser] p. 58Theorem 8.3ragcol 29108
[Schwabhauser] p. 58Theorem 8.4ragmir 29109
[Schwabhauser] p. 58Theorem 8.5ragtrivb 29111
[Schwabhauser] p. 58Theorem 8.6ragflat2 29112
[Schwabhauser] p. 58Theorem 8.7ragflat 29113
[Schwabhauser] p. 58Theorem 8.8ragtriva 29114
[Schwabhauser] p. 58Theorem 8.9ragflat3 29115  ragncol 29118
[Schwabhauser] p. 58Theorem 8.10ragcgr 29116
[Schwabhauser] p. 59Theorem 8.12perpcom 29122
[Schwabhauser] p. 59Theorem 8.13ragperp 29126
[Schwabhauser] p. 59Theorem 8.14perpneq 29123
[Schwabhauser] p. 59Definition 8.11df-perpg 29105  isperp 29121
[Schwabhauser] p. 59Definition 8.13isperp2 29124
[Schwabhauser] p. 60Theorem 8.18foot 29131
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 29140  colperpexlem2 29141
[Schwabhauser] p. 63Theorem 8.21colperpex 29143  colperpexlem3 29142
[Schwabhauser] p. 64Theorem 8.22mideu 29148  midex 29147
[Schwabhauser] p. 66Lemma 8.24opphllem 29145
[Schwabhauser] p. 67Theorem 9.2oppcom 29154
[Schwabhauser] p. 67Definition 9.1islnopp 29149
[Schwabhauser] p. 68Lemma 9.3opphllem2 29158
[Schwabhauser] p. 68Lemma 9.4opphllem5 29161  opphllem6 29162
[Schwabhauser] p. 69Theorem 9.5opphl 29164
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28863
[Schwabhauser] p. 70Theorem 9.6outpasch 29167
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 29175
[Schwabhauser] p. 71Definition 9.7df-hpg 29170  hpgbr 29172
[Schwabhauser] p. 72Lemma 9.10hpgerlem 29177
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 29176
[Schwabhauser] p. 72Theorem 9.11hpgid 29178
[Schwabhauser] p. 72Theorem 9.12hpgcom 29179
[Schwabhauser] p. 72Theorem 9.13hpgtr 29180
[Schwabhauser] p. 73Theorem 9.18colopp 29181
[Schwabhauser] p. 73Theorem 9.19colhp 29182
[Schwabhauser] p. 74Lemma 9.22lnincplng 29196
[Schwabhauser] p. 74Theorem 9.21plngcp 29198
[Schwabhauser] p. 74Theorem 9.24plngrot 29202
[Schwabhauser] p. 74Definition 9.20df-plng 29186  elplng 29192
[Schwabhauser] p. 75Theorem 9.25lnssplng 29204  lnssplng1 29205
[Schwabhauser] p. 76Theorem 9.26plng3p 29209
[Schwabhauser] p. 88Theorem 10.2lmieu 29223
[Schwabhauser] p. 88Definition 10.1df-mid 29213
[Schwabhauser] p. 89Theorem 10.4lmicom 29227
[Schwabhauser] p. 89Theorem 10.5lmilmi 29228
[Schwabhauser] p. 89Theorem 10.6lmireu 29229
[Schwabhauser] p. 89Theorem 10.7lmieq 29230
[Schwabhauser] p. 89Theorem 10.8lmiinv 29231
[Schwabhauser] p. 89Theorem 10.9lmif1o 29234
[Schwabhauser] p. 89Theorem 10.10lmiiso 29236
[Schwabhauser] p. 89Definition 10.3df-lmi 29214
[Schwabhauser] p. 90Theorem 10.11lmimot 29237
[Schwabhauser] p. 91Theorem 10.12hypcgr 29241
[Schwabhauser] p. 92Theorem 10.14lmiopp 29242
[Schwabhauser] p. 92Theorem 10.15lnperpex 29243  lnperpexs 29244
[Schwabhauser] p. 92Theorem 10.16trgcopy 29245  trgcopyeu 29247
[Schwabhauser] p. 95Definition 11.2dfcgra2 29272
[Schwabhauser] p. 95Definition 11.3iscgra 29250
[Schwabhauser] p. 95Proposition 11.4cgracgr 29259
[Schwabhauser] p. 95Proposition 11.10cgrahl1 29257  cgrahl2 29258
[Schwabhauser] p. 96Theorem 11.6cgraid 29260
[Schwabhauser] p. 96Theorem 11.9cgraswap 29261
[Schwabhauser] p. 97Theorem 11.7cgracom 29263
[Schwabhauser] p. 97Theorem 11.8cgratr 29264
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 29268  cgrahl 29269
[Schwabhauser] p. 98Theorem 11.13sacgr 29273
[Schwabhauser] p. 98Theorem 11.14oacgr 29274
[Schwabhauser] p. 98Theorem 11.15acopy 29275  acopyeu 29276
[Schwabhauser] p. 98Theorem 11.16ragcgra 29277
[Schwabhauser] p. 98Theorem 11.17cgrarag 29278
[Schwabhauser] p. 98Theorem 11.18ragsupplcgra 29279
[Schwabhauser] p. 99Theorem 11.19ragraghl 29280
[Schwabhauser] p. 99Theorem 11.20perpeq 29282
[Schwabhauser] p. 99Theorem 11.22tgaaddcpbl 29286
[Schwabhauser] p. 101Theorem 11.24inagswap 29294
[Schwabhauser] p. 101Theorem 11.25inaghl 29298
[Schwabhauser] p. 101Definition 11.23isinag 29291
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 29306
[Schwabhauser] p. 102Definition 11.27df-leag 29299  isleag 29300
[Schwabhauser] p. 107Theorem 11.49tgsas 29334  tgsas1 29333  tgsas2 29335  tgsas3 29336
[Schwabhauser] p. 108Theorem 11.50tgasa 29338  tgasa1 29337
[Schwabhauser] p. 109Theorem 11.51tgsss1 29339  tgsss2 29340  tgsss3 29341
[Schwabhauser] p. 121Definition 12.2df-prlng 29349
[Schwabhauser] p. 122Theorem 12.4prlngref 29352
[Schwabhauser] p. 122Theorem 12.5prlngsym 29353
[Schwabhauser] p. 122Theorem 12.6prlnghpg 29358
[Schwabhauser] p. 122Theorem 12.7dfprlng2 29359  dfprlng3 29360
[Schwabhauser] p. 122Theorem 12.9perpprlng 29362
[Schwabhauser] p. 122Theorem 12.10prlngex 29363
[Schwabhauser] p. 123Theorem 12.11prlngmo 29366  prlngmo2 29368
[Schwabhauser] p. 124Theorem 12.13prlngeu 29367
[Schwabhauser] p. 124Theorem 12.14prlngpln4 29370
[Schwabhauser] p. 124Theorem 12.15prlngplngtr 29371
[Schwabhauser] p. 125Theorem 12.16prlnginn0 29372
[Schwabhauser] p. 125Theorem 12.17prlngmid2 29373
[Schwabhauser] p. 126Theorem 12.18symquadprlng 29374
[Schwabhauser] p. 126Theorem 12.19prlngsymquad 29376  prlngsymquadopp 29377
[Schwabhauser] p. 126Theorem 12.20quadcgrprlng 29378
[Schwabhauser] p. 126Theorem 12.21tgaltai 29379
[Shapiro] p. 230Theorem 6.5.1dchrhash 27562  dchrsum 27560  dchrsum2 27559  sumdchr 27563
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27564  sum2dchr 27565
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20244  ablfacrp2 20245
[Shapiro], p. 328Equation 9.2.4vmasum 27507
[Shapiro], p. 329Equation 9.2.7logfac2 27508
[Shapiro], p. 329Equation 9.2.9logfacrlim 27515
[Shapiro], p. 331Equation 9.2.13vmadivsum 27773
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27776
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27830  vmalogdivsum2 27829
[Shapiro], p. 375Theorem 9.4.1dirith 27820  dirith2 27819
[Shapiro], p. 375Equation 9.4.3rplogsum 27818  rpvmasum 27817  rpvmasum2 27803
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27778
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27816
[Shapiro], p. 377Lemma 9.4.1dchrisum 27783  dchrisumlem1 27780  dchrisumlem2 27781  dchrisumlem3 27782  dchrisumlema 27779
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27786
[Shapiro], p. 379Equation 9.4.16dchrmusum 27815  dchrmusumlem 27813  dchrvmasumlem 27814
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27785
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27787
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27811  dchrisum0re 27804  dchrisumn0 27812
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27797
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27801
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27802
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27857  pntrsumbnd2 27858  pntrsumo1 27856
[Shapiro], p. 405Equation 10.2.1mudivsum 27821
[Shapiro], p. 406Equation 10.2.6mulogsum 27823
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27825
[Shapiro], p. 407Equation 10.2.8mulog2sum 27828
[Shapiro], p. 418Equation 10.4.6logsqvma 27833
[Shapiro], p. 418Equation 10.4.8logsqvma2 27834
[Shapiro], p. 419Equation 10.4.10selberg 27839
[Shapiro], p. 420Equation 10.4.12selberg2lem 27841
[Shapiro], p. 420Equation 10.4.14selberg2 27842
[Shapiro], p. 422Equation 10.6.7selberg3 27850
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27851
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27848  selberg3lem2 27849
[Shapiro], p. 422Equation 10.4.23selberg4 27852
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27846
[Shapiro], p. 428Equation 10.6.2selbergr 27859
[Shapiro], p. 429Equation 10.6.8selberg3r 27860
[Shapiro], p. 430Equation 10.6.11selberg4r 27861
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27875
[Shapiro], p. 434Equation 10.6.27pntlema 27887  pntlemb 27888  pntlemc 27886  pntlemd 27885  pntlemg 27889
[Shapiro], p. 435Equation 10.6.29pntlema 27887
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27879
[Shapiro], p. 436Lemma 10.6.2pntibnd 27884
[Shapiro], p. 436Equation 10.6.34pntlema 27887
[Shapiro], p. 436Equation 10.6.35pntlem3 27900  pntleml 27902
[Stewart] p. 91Lemma 7.3constrss 34309
[Stewart] p. 92Definition 7.4.df-constr 34296
[Stewart] p. 96Theorem 7.10constraddcl 34328  constrinvcl 34339  constrmulcl 34337  constrnegcl 34329  constrsqrtcl 34345
[Stewart] p. 97Theorem 7.11constrextdg2 34315
[Stewart] p. 98Theorem 7.12constrext2chn 34325
[Stewart] p. 99Theorem 7.132sqr3nconstr 34347
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34357
[Stoll] p. 13Definition corresponds to dfsymdif3 4251
[Stoll] p. 16Exercise 4.40dif 4355  dif0 4326
[Stoll] p. 16Exercise 4.8difdifdir 4446
[Stoll] p. 17Theorem 5.1(5)unvdif 4428
[Stoll] p. 19Theorem 5.2(13)undm 4242
[Stoll] p. 19Theorem 5.2(13')indm 4243
[Stoll] p. 20Remarkinvdif 4224
[Stoll] p. 25Definition of ordered tripledf-ot 4592
[Stoll] p. 43Definitionuniiun 5016
[Stoll] p. 44Definitionintiin 5017
[Stoll] p. 45Definitiondf-iin 4953
[Stoll] p. 45Definition indexed uniondf-iun 4952
[Stoll] p. 176Theorem 3.4(27)iman 407
[Stoll] p. 262Example 4.1dfsymdif3 4251
[Strang] p. 242Section 6.3expgrowth 45263
[Suppes] p. 22Theorem 2eq0 4296  eq0f 4293
[Suppes] p. 22Theorem 4eqss 3945  eqssd 3947  eqssi 3946
[Suppes] p. 23Theorem 5ss0 4351  ss0b 4350
[Suppes] p. 23Theorem 6sstr 3938  sstrALT2 45761
[Suppes] p. 23Theorem 7pssirr 4050
[Suppes] p. 23Theorem 8pssn2lp 4052
[Suppes] p. 23Theorem 9psstr 4055
[Suppes] p. 23Theorem 10pssss 4045
[Suppes] p. 25Theorem 12elin 3914  elun 4099
[Suppes] p. 26Theorem 15inidm 4171
[Suppes] p. 26Theorem 16in0 4344
[Suppes] p. 27Theorem 23unidm 4103
[Suppes] p. 27Theorem 24un0 4343
[Suppes] p. 27Theorem 25ssun1 4123
[Suppes] p. 27Theorem 26ssequn1 4131
[Suppes] p. 27Theorem 27unss 4135
[Suppes] p. 27Theorem 28indir 4231
[Suppes] p. 27Theorem 29undir 4232
[Suppes] p. 28Theorem 32difid 4324
[Suppes] p. 29Theorem 33difin 4217
[Suppes] p. 29Theorem 34indif 4225
[Suppes] p. 29Theorem 35undif1 4429
[Suppes] p. 29Theorem 36difun2 4436
[Suppes] p. 29Theorem 37difin0 4427
[Suppes] p. 29Theorem 38disjdif 4425
[Suppes] p. 29Theorem 39difundi 4235
[Suppes] p. 29Theorem 40difindi 4237
[Suppes] p. 30Theorem 41nalset 5267
[Suppes] p. 39Theorem 61uniss 4874
[Suppes] p. 39Theorem 65uniop 5484
[Suppes] p. 41Theorem 70intsn 4943
[Suppes] p. 42Theorem 71intpr 4941  intprg 4940
[Suppes] p. 42Theorem 73op1stb 5439
[Suppes] p. 42Theorem 78intun 4939
[Suppes] p. 44Definition 15(a)dfiun2 4989  dfiun2g 4987
[Suppes] p. 44Definition 15(b)dfiin2 4990
[Suppes] p. 47Theorem 86elpw 4560  elpw2 5295  elpw2g 5294  elpwg 4559  elpwgdedVD 45843
[Suppes] p. 47Theorem 87pwid 4579
[Suppes] p. 47Theorem 89pw0 4772
[Suppes] p. 48Theorem 90pwpw0 4773
[Suppes] p. 52Theorem 101xpss12 5662
[Suppes] p. 52Theorem 102xpindi 5806  xpindir 5807
[Suppes] p. 52Theorem 103xpundi 5716  xpundir 5717
[Suppes] p. 54Theorem 105elirrv 9569
[Suppes] p. 58Theorem 2relss 5754
[Suppes] p. 59Theorem 4eldm 5878  eldm2 5879  eldm2g 5877  eldmg 5876
[Suppes] p. 59Definition 3df-dm 5657
[Suppes] p. 60Theorem 6dmin 5889
[Suppes] p. 60Theorem 8rnun 6130
[Suppes] p. 60Theorem 9rnin 6131
[Suppes] p. 60Definition 4dfrn2 5866
[Suppes] p. 61Theorem 11brcnv 5856  brcnvg 5853
[Suppes] p. 62Equation 5elcnv 5850  elcnv2 5851
[Suppes] p. 62Theorem 12relcnv 6094
[Suppes] p. 62Theorem 15cnvin 6129
[Suppes] p. 62Theorem 16cnvun 6127
[Suppes] p. 63Definitiondftrrels2 39511
[Suppes] p. 63Theorem 20co02 6251
[Suppes] p. 63Theorem 21dmcoss 5953
[Suppes] p. 63Definition 7df-co 5656
[Suppes] p. 64Theorem 26cnvco 5863
[Suppes] p. 64Theorem 27coass 6256
[Suppes] p. 65Theorem 31resundi 5980
[Suppes] p. 65Theorem 34elima 6055  elima2 6056  elima3 6057  elimag 6054
[Suppes] p. 65Theorem 35imaundi 6135
[Suppes] p. 66Theorem 40dminss 6138
[Suppes] p. 66Theorem 41imainss 6139
[Suppes] p. 67Exercise 11cnvxp 6142
[Suppes] p. 81Definition 34dfec2 8698
[Suppes] p. 82Theorem 72elec 8742  elecALTV 39123  elecg 8740
[Suppes] p. 82Theorem 73eqvrelth 39547  erth 8750  erth2 8751
[Suppes] p. 83Theorem 74eqvreldisj 39550  erdisj 8753
[Suppes] p. 83Definition 35, df-parts 39720  dfmembpart2 39725
[Suppes] p. 89Theorem 96map0b 8889
[Suppes] p. 89Theorem 97map0 8893  map0g 8890
[Suppes] p. 89Theorem 98mapsn 8894  mapsnd 8892
[Suppes] p. 89Theorem 99mapss 8895
[Suppes] p. 91Definition 12(ii)alephsuc 10119
[Suppes] p. 91Definition 12(iii)alephlim 10118
[Suppes] p. 92Theorem 1enref 8990  enrefg 8989
[Suppes] p. 92Theorem 2ensym 9008  ensymb 9007  ensymi 9009
[Suppes] p. 92Theorem 3entr 9011
[Suppes] p. 92Theorem 4unen 9051
[Suppes] p. 94Theorem 15endom 8984
[Suppes] p. 94Theorem 16ssdomg 9005
[Suppes] p. 94Theorem 17domtr 9012
[Suppes] p. 95Theorem 18sbth 9094
[Suppes] p. 97Theorem 23canth2 9127  canth2g 9128
[Suppes] p. 97Definition 3brsdom2 9098  df-sdom 8954  dfsdom2 9097
[Suppes] p. 97Theorem 21(i)sdomirr 9111
[Suppes] p. 97Theorem 22(i)domnsym 9100
[Suppes] p. 97Theorem 21(ii)sdomnsym 9099
[Suppes] p. 97Theorem 22(ii)domsdomtr 9109
[Suppes] p. 97Theorem 22(iv)brdom2 8987
[Suppes] p. 97Theorem 21(iii)sdomtr 9112
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9107
[Suppes] p. 98Exercise 4fundmen 9037  fundmeng 9038
[Suppes] p. 98Exercise 6xpdom3 9072
[Suppes] p. 98Exercise 11sdomentr 9108
[Suppes] p. 104Theorem 37fofi 9283
[Suppes] p. 104Theorem 38pwfi 9288
[Suppes] p. 105Theorem 40pwfi 9288
[Suppes] p. 111Axiom for cardinal numberscarden 10607
[Suppes] p. 130Definition 3df-tr 5212
[Suppes] p. 132Theorem 9ssonuni 7777
[Suppes] p. 134Definition 6df-suc 6357
[Suppes] p. 136Theorem Schema 22findes 7895  finds 7891  finds1 7894  finds2 7893
[Suppes] p. 151Theorem 42isfinite 9631  isfinite2 9268  isfiniteg 9270  unbnn 9266
[Suppes] p. 162Definition 5df-ltnq 10975  df-ltpq 10967
[Suppes] p. 197Theorem Schema 4tfindes 7857  tfinds 7854  tfinds2 7858
[Suppes] p. 209Theorem 18oaord1 8537
[Suppes] p. 209Theorem 21oaword2 8539
[Suppes] p. 211Theorem 25oaass 8547
[Suppes] p. 225Definition 8iscard2 10029
[Suppes] p. 227Theorem 56ondomon 10619
[Suppes] p. 228Theorem 59harcard 10031
[Suppes] p. 228Definition 12(i)aleph0 10117
[Suppes] p. 228Theorem Schema 61onintss 6404
[Suppes] p. 228Theorem Schema 62onminesb 7790  onminsb 7791
[Suppes] p. 229Theorem 64alephval2 10629
[Suppes] p. 229Theorem 65alephcard 10121
[Suppes] p. 229Theorem 66alephord2i 10128
[Suppes] p. 229Theorem 67alephnbtwn 10122
[Suppes] p. 229Definition 12df-aleph 9993
[Suppes] p. 242Theorem 6weth 10545
[Suppes] p. 242Theorem 8entric 10613
[Suppes] p. 242Theorem 9carden 10607
[Szendrei] p. 11Line 6df-cloneop 36382
[Szendrei] p. 11Paragraph 3df-suppos 36386
[TakeutiZaring] p. 8Axiom 1ax-ext 2732
[TakeutiZaring] p. 13Definition 4.5df-cleq 2752  wl-df.cleq 38351
[TakeutiZaring] p. 13Proposition 4.6df-clel 2835  wl-df.clel 38354
[TakeutiZaring] p. 13Proposition 4.9cvjust 2754
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2780
[TakeutiZaring] p. 14Definition 4.16df-oprab 7412
[TakeutiZaring] p. 14Proposition 4.14ru 3737
[TakeutiZaring] p. 15Axiom 2zfpair 5382
[TakeutiZaring] p. 15Exercise 1elpr 4608  elpr2 4610  elpr2g 4609  elprg 4606
[TakeutiZaring] p. 15Exercise 2elsn 4598  elsn2 4625  elsn2g 4624  elsng 4597  velsn 4599
[TakeutiZaring] p. 15Exercise 3elop 5435
[TakeutiZaring] p. 15Exercise 4sneq 4593  sneqr 4799
[TakeutiZaring] p. 15Definition 5.1dfpr2 4604  dfsn2 4596  dfsn2ALT 4605
[TakeutiZaring] p. 16Axiom 3uniex 7741
[TakeutiZaring] p. 16Exercise 6opth 5444
[TakeutiZaring] p. 16Exercise 7opex 5431
[TakeutiZaring] p. 16Exercise 8rext 5415
[TakeutiZaring] p. 16Corollary 5.8unex 7744  unexg 7743
[TakeutiZaring] p. 16Definition 5.3dftp2 4651
[TakeutiZaring] p. 16Definition 5.5df-uni 4867
[TakeutiZaring] p. 16Definition 5.6df-in 3905  df-un 3903
[TakeutiZaring] p. 16Proposition 5.7unipr 4883  uniprg 4882
[TakeutiZaring] p. 17Axiom 4vpwex 5338
[TakeutiZaring] p. 17Exercise 1eltp 4649
[TakeutiZaring] p. 17Exercise 5elsuc 6424  elsucg 6422  sstr2 3937
[TakeutiZaring] p. 17Exercise 6uncom 4104
[TakeutiZaring] p. 17Exercise 7incom 4154
[TakeutiZaring] p. 17Exercise 8unass 4117
[TakeutiZaring] p. 17Exercise 9inass 4172
[TakeutiZaring] p. 17Exercise 10indi 4229
[TakeutiZaring] p. 17Exercise 11undi 4230
[TakeutiZaring] p. 17Definition 5.9df-pss 3918  df-ss 3915
[TakeutiZaring] p. 17Definition 5.10df-pw 4558
[TakeutiZaring] p. 18Exercise 7unss2 4132
[TakeutiZaring] p. 18Exercise 9dfss2 3916  sseqin2 4168
[TakeutiZaring] p. 18Exercise 10ssid 3952
[TakeutiZaring] p. 18Exercise 12inss1 4181  inss2 4182
[TakeutiZaring] p. 18Exercise 13nss 3994
[TakeutiZaring] p. 18Exercise 15unieq 4877
[TakeutiZaring] p. 18Exercise 18sspwb 5416  sspwimp 45844  sspwimpALT 45851  sspwimpALT2 45854  sspwimpcf 45846
[TakeutiZaring] p. 18Exercise 19pweqb 5423
[TakeutiZaring] p. 19Axiom 5ax-rep 5231
[TakeutiZaring] p. 20Definitiondf-rab 3413
[TakeutiZaring] p. 20Corollary 5.160ex 5260
[TakeutiZaring] p. 20Definition 5.12df-dif 3901
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 37362  dfnul2 4281
[TakeutiZaring] p. 20Proposition 5.15difid 4324
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4299  n0f 4295  neq0 4298  neq0f 4294
[TakeutiZaring] p. 21Axiom 6zfreg 9568
[TakeutiZaring] p. 21Axiom 6'zfregs 9711
[TakeutiZaring] p. 21Theorem 5.22setind 9726
[TakeutiZaring] p. 21Definition 5.20df-v 3452
[TakeutiZaring] p. 21Proposition 5.21vprc 5273
[TakeutiZaring] p. 22Exercise 10ss 4349
[TakeutiZaring] p. 22Exercise 3ssex 5281  ssexg 5280
[TakeutiZaring] p. 22Exercise 4inex1 5276
[TakeutiZaring] p. 22Exercise 5ruv 9580
[TakeutiZaring] p. 22Exercise 6elirr 9572
[TakeutiZaring] p. 22Exercise 7ssdif0 4313
[TakeutiZaring] p. 22Exercise 11difdif 4081
[TakeutiZaring] p. 22Exercise 13undif3 4245  undif3VD 45808
[TakeutiZaring] p. 22Exercise 14difss 4082
[TakeutiZaring] p. 22Exercise 15sscon 4089
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3077
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3087
[TakeutiZaring] p. 23Proposition 6.2xpex 7750  xpexg 7747
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5654
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6599
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6777  fun11 6602
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6540  svrelfun 6600
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5865
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5867
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5659
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5660
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5656
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6181  dfrel2 6176
[TakeutiZaring] p. 25Exercise 3xpss 5663
[TakeutiZaring] p. 25Exercise 5relun 5785
[TakeutiZaring] p. 25Exercise 6reluni 5792
[TakeutiZaring] p. 25Exercise 9inxp 5805
[TakeutiZaring] p. 25Exercise 12relres 5992
[TakeutiZaring] p. 25Exercise 13opelres 5972  opelresi 5974
[TakeutiZaring] p. 25Exercise 14dmres 5999
[TakeutiZaring] p. 25Exercise 15resss 5988
[TakeutiZaring] p. 25Exercise 17resabs1 5993
[TakeutiZaring] p. 25Exercise 18funres 6570
[TakeutiZaring] p. 25Exercise 24relco 6098
[TakeutiZaring] p. 25Exercise 29funco 6568
[TakeutiZaring] p. 25Exercise 30f1co 6779
[TakeutiZaring] p. 26Definition 6.10eu2 2634
[TakeutiZaring] p. 26Definition 6.11conventions 30935  df-fv 6535  fv3 6891
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7920  cnvexg 7919
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7904  dmexg 7896
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7905  rnexg 7897
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 45380
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7915
[TakeutiZaring] p. 27Corollary 6.13fvex 6886
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 48166  tz6.12-1-afv2 48233  tz6.12-1 6896  tz6.12-afv 48165  tz6.12-afv2 48232  tz6.12 6897  tz6.12c-afv2 48234  tz6.12c 6895
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 48229  tz6.12-2 6860  tz6.12i-afv2 48235  tz6.12i 6899
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6530
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6531
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6533  wfo 6525
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6532  wf1 6524
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6534  wf1o 6526
[TakeutiZaring] p. 28Exercise 4eqfnfv 7017  eqfnfv2 7018  eqfnfv2f 7021
[TakeutiZaring] p. 28Exercise 5fvco 6971
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7211
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7209
[TakeutiZaring] p. 29Exercise 9funimaex 6615  funimaexg 6614
[TakeutiZaring] p. 29Definition 6.18df-br 5103
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5556
[TakeutiZaring] p. 30Definition 6.21dffr2 5608  dffr3 6089  eliniseg 6084  iniseg 6087
[TakeutiZaring] p. 30Definition 6.22df-eprel 5547
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5624  fr3nr 7769  frirr 5623
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5600
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7771
[TakeutiZaring] p. 31Exercise 1frss 5611
[TakeutiZaring] p. 31Exercise 4wess 5633
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6339  tz6.26i 6340  wefrc 5641  wereu2 5644
[TakeutiZaring] p. 32Theorem 6.27wfi 6341  wfii 6342
[TakeutiZaring] p. 32Definition 6.28df-isom 6536
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7325
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7326
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7332
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7333
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7334
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7338
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7345
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7347
[TakeutiZaring] p. 35Notationwtr 5211
[TakeutiZaring] p. 35Theorem 7.2trelpss 45381  tz7.2 5630
[TakeutiZaring] p. 35Definition 7.1dftr3 5216
[TakeutiZaring] p. 36Proposition 7.4ordwe 6364
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6372
[TakeutiZaring] p. 36Proposition 7.6ordelord 6373  ordelordALT 45464  ordelordALTVD 45793
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6379  ordelssne 6378
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6377
[TakeutiZaring] p. 37Proposition 7.9ordin 6382
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7779
[TakeutiZaring] p. 38Corollary 7.15ordsson 7780
[TakeutiZaring] p. 38Definition 7.11df-on 6355
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6384
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45476  ordon 7774
[TakeutiZaring] p. 38Proposition 7.13onprc 7775
[TakeutiZaring] p. 39Theorem 7.17tfi 7847
[TakeutiZaring] p. 40Exercise 3ontr2 6400  ontr2d 36871
[TakeutiZaring] p. 40Exercise 7dftr2 5213
[TakeutiZaring] p. 40Exercise 9onssmin 7789
[TakeutiZaring] p. 40Exercise 11unon 7825
[TakeutiZaring] p. 40Exercise 12ordun 6458
[TakeutiZaring] p. 40Exercise 14ordequn 6457
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7776
[TakeutiZaring] p. 40Proposition 7.20elssuni 4898
[TakeutiZaring] p. 41Definition 7.22df-suc 6357
[TakeutiZaring] p. 41Proposition 7.23sssucid 6434  sucidg 6435
[TakeutiZaring] p. 41Proposition 7.24onsuc 7807
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6448  ordnbtwn 6447
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7822
[TakeutiZaring] p. 42Exercise 1df-lim 6356
[TakeutiZaring] p. 42Exercise 4omssnlim 7875
[TakeutiZaring] p. 42Exercise 7ssnlim 7880
[TakeutiZaring] p. 42Exercise 8onsucssi 7835  ordelsuc 7814
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7816
[TakeutiZaring] p. 42Definition 7.27nlimon 7845
[TakeutiZaring] p. 42Definition 7.28dfom2 7862
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7883
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7884
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7885
[TakeutiZaring] p. 43Remarkomon 7872
[TakeutiZaring] p. 43Axiom 7inf3 9614  omex 9622
[TakeutiZaring] p. 43Theorem 7.32ordom 7870
[TakeutiZaring] p. 43Corollary 7.31find 7890
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7887
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7888
[TakeutiZaring] p. 44Exercise 1limomss 7865
[TakeutiZaring] p. 44Exercise 2int0 4921
[TakeutiZaring] p. 44Exercise 3trintss 5230
[TakeutiZaring] p. 44Exercise 4intss1 4922
[TakeutiZaring] p. 44Exercise 5intex 5304
[TakeutiZaring] p. 44Exercise 6oninton 7792
[TakeutiZaring] p. 44Exercise 11ordintdif 6403
[TakeutiZaring] p. 44Definition 7.35df-int 4907
[TakeutiZaring] p. 44Proposition 7.34noinfep 9639
[TakeutiZaring] p. 45Exercise 4onint 7787
[TakeutiZaring] p. 47Lemma 1tfrlem1 8361
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8383
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8384
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8385
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8392  tz7.44-2 8393  tz7.44-3 8394
[TakeutiZaring] p. 50Exercise 1smogt 8353
[TakeutiZaring] p. 50Exercise 3smoiso 8348
[TakeutiZaring] p. 50Definition 7.46df-smo 8332
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8433  tz7.49c 8434
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8431
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8430
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8432
[TakeutiZaring] p. 53Proposition 7.532eu5 2680
[TakeutiZaring] p. 54Definition 7.55df-lexo 35797
[TakeutiZaring] p. 54Definition 7.57df-r0 35798
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10062
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10063
[TakeutiZaring] p. 55Definition 7.59df-j0 35799
[TakeutiZaring] p. 56Definition 8.1oalim 8518  oasuc 8510
[TakeutiZaring] p. 57Remarktfindsg 7855
[TakeutiZaring] p. 57Proposition 8.2oacl 8521
[TakeutiZaring] p. 57Proposition 8.3oa0 8502  oa0r 8524
[TakeutiZaring] p. 57Proposition 8.16omcl 8522
[TakeutiZaring] p. 58Corollary 8.5oacan 8534
[TakeutiZaring] p. 58Proposition 8.4nnaord 8606  nnaordi 8605  oaord 8533  oaordi 8532
[TakeutiZaring] p. 59Proposition 8.6iunss2 5007  uniss2 4901
[TakeutiZaring] p. 59Proposition 8.7oawordri 8536
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8541  oawordex 8543
[TakeutiZaring] p. 59Proposition 8.9nnacl 8598
[TakeutiZaring] p. 59Proposition 8.10oaabs 8635
[TakeutiZaring] p. 60Remarkoancom 9630
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8546
[TakeutiZaring] p. 62Exercise 1nnarcl 8603
[TakeutiZaring] p. 62Exercise 5oaword1 8538
[TakeutiZaring] p. 62Definition 8.15om0x 8505  omlim 8519  omsuc 8512
[TakeutiZaring] p. 62Definition 8.15(a)om0 8503
[TakeutiZaring] p. 63Proposition 8.17nnecl 8600  nnmcl 8599
[TakeutiZaring] p. 63Proposition 8.19nnmord 8619  nnmordi 8618  omord 8554  omordi 8552
[TakeutiZaring] p. 63Proposition 8.20omcan 8555
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8623  omwordri 8558
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8525
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8528  om1r 8529
[TakeutiZaring] p. 64Proposition 8.22om00 8561
[TakeutiZaring] p. 64Proposition 8.23omordlim 8563
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8564
[TakeutiZaring] p. 64Proposition 8.25odi 8565
[TakeutiZaring] p. 65Theorem 8.26omass 8566
[TakeutiZaring] p. 67Definition 8.30nnesuc 8595  oe0 8508  oelim 8520  oesuc 8513  onesuc 8516
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8506
[TakeutiZaring] p. 67Proposition 8.32oen0 8573
[TakeutiZaring] p. 67Proposition 8.33oeordi 8574
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8507
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8531
[TakeutiZaring] p. 68Corollary 8.34oeord 8575
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8581
[TakeutiZaring] p. 68Proposition 8.35oewordri 8579
[TakeutiZaring] p. 68Proposition 8.37oeworde 8580
[TakeutiZaring] p. 69Proposition 8.41oeoa 8584
[TakeutiZaring] p. 70Proposition 8.42oeoe 8586
[TakeutiZaring] p. 73Theorem 9.1trcl 9707  tz9.1 9708
[TakeutiZaring] p. 76Definition 9.9df-r1 9746  r10 9750  r1lim 9754  r1limg 9753  r1suc 9752  r1sucg 9751
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9762  r1ord2 9763  r1ordg 9760
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9772
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9797  tz9.13 9773  tz9.13g 9774
[TakeutiZaring] p. 79Definition 9.14df-rank 9747  rankval 9798  rankvalb 9779  rankvalg 9799
[TakeutiZaring] p. 79Proposition 9.16rankel 9824  rankelb 9806
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9840  rankval3 9826  rankval3b 9809
[TakeutiZaring] p. 79Proposition 9.18rankonid 9812
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9777
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9819  rankr1c 9803  rankr1g 9817
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9820
[TakeutiZaring] p. 80Exercise 1rankss 9836  rankssb 9835
[TakeutiZaring] p. 80Exercise 2unbndrank 9828
[TakeutiZaring] p. 80Proposition 9.19bndrank 9827
[TakeutiZaring] p. 83Axiom of Choiceac4 10525  dfac3 10172
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10081  numth 10522  numth2 10521
[TakeutiZaring] p. 85Definition 10.4cardval 10602
[TakeutiZaring] p. 85Proposition 10.5cardid 10603  cardid2 10006
[TakeutiZaring] p. 85Proposition 10.9oncard 10013
[TakeutiZaring] p. 85Proposition 10.10carden 10607
[TakeutiZaring] p. 85Proposition 10.11cardidm 10012
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9997
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 10018
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 10010
[TakeutiZaring] p. 87Proposition 10.15pwen 9147
[TakeutiZaring] p. 88Exercise 1en0 9023
[TakeutiZaring] p. 88Exercise 7infensuc 9152
[TakeutiZaring] p. 89Exercise 10omxpen 9076
[TakeutiZaring] p. 90Corollary 10.23cardnn 10016
[TakeutiZaring] p. 90Definition 10.27alephiso 10149
[TakeutiZaring] p. 90Proposition 10.20nneneq 9199
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9207
[TakeutiZaring] p. 90Proposition 10.26alephprc 10150
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9204
[TakeutiZaring] p. 91Exercise 2alephle 10139
[TakeutiZaring] p. 91Exercise 3aleph0 10117
[TakeutiZaring] p. 91Exercise 4cardlim 10025
[TakeutiZaring] p. 91Exercise 7infpss 10266
[TakeutiZaring] p. 91Exercise 8infcntss 9292
[TakeutiZaring] p. 91Definition 10.29df-fin 8955  isfi 8980
[TakeutiZaring] p. 92Proposition 10.32onfin 9208
[TakeutiZaring] p. 92Proposition 10.34imadomg 10585
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9069
[TakeutiZaring] p. 93Proposition 10.35fodomb 10577
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10236  unxpdom 9228
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 10027  cardsdomelir 10026
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9230
[TakeutiZaring] p. 94Proposition 10.39infxpen 10065
[TakeutiZaring] p. 95Definition 10.42df-map 8827
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10618  infxpidm2 10068
[TakeutiZaring] p. 95Proposition 10.41infdju 10257  infxp 10264
[TakeutiZaring] p. 96Proposition 10.44pw2en 9081  pw2f1o 9079
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9140
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10537
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10532  ac6s5 10541
[TakeutiZaring] p. 98Theorem 10.47unidom 10599
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10600  uniimadomf 10601
[TakeutiZaring] p. 100Definition 11.1cfcof 10324
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10319
[TakeutiZaring] p. 102Exercise 1cfle 10303
[TakeutiZaring] p. 102Exercise 2cf0 10300
[TakeutiZaring] p. 102Exercise 3cfsuc 10307
[TakeutiZaring] p. 102Exercise 4cfom 10314
[TakeutiZaring] p. 102Proposition 11.9coftr 10323
[TakeutiZaring] p. 103Theorem 11.15alephreg 10639
[TakeutiZaring] p. 103Proposition 11.11cardcf 10301
[TakeutiZaring] p. 103Proposition 11.13alephsing 10326
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10148
[TakeutiZaring] p. 104Proposition 11.16carduniima 10147
[TakeutiZaring] p. 104Proposition 11.18alephfp 10159  alephfp2 10160
[TakeutiZaring] p. 106Theorem 11.20gchina 10756
[TakeutiZaring] p. 106Theorem 11.21mappwen 10163
[TakeutiZaring] p. 107Theorem 11.26konigth 10626
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10640
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10641
[TakeutiZaring] p. 143Definition 14.1(1)df-cnv2 35777
[TakeutiZaring] p. 143Definition 14.1(2)df-cnv3 35778
[TakeutiZaring] p. 144Definition 14.2df-gdlop1 35779  df-gdlop2 35780  df-gdlop3 35781  df-gdlop4 35782  df-gdlop5 35783  df-gdlop6 35784  df-gdlop7 35785  df-gdlop8 35786  df-gdlopc 35787
[TakeutiZaring] p. 155Definition 15.2df-j 35800
[TakeutiZaring] p. 156Definition 15.7df-k1 35801  df-k2 35802  df-k3 35803
[TakeutiZaring] p. 158Definition 15.13df-fnl 35804
[TakeutiZaring] p. 158Definition 15.15df-l 35805
[Tarski] p. 67Axiom B5ax-c5 39860
[Tarski] p. 67Scheme B5sp 2219
[Tarski] p. 68Lemma 6avril1 30998  equid 2045
[Tarski] p. 69Lemma 7equcomi 2050
[Tarski] p. 70Lemma 14spim 2416  spime 2418  spimew 2004
[Tarski] p. 70Lemma 16ax-12 2213  ax-c15 39866  ax12i 1999
[Tarski] p. 70Lemmas 16 and 17sb6 2122
[Tarski] p. 75Axiom B7ax6v 2001
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1943  ax5ALT 39884
[Tarski], p. 75Scheme B8 of system S2ax-7 2041  ax-8 2147  ax-9 2155
[Tarski1999] p. 178Axiom 4axtgsegcon 28860
[Tarski1999] p. 178Axiom 5axtg5seg 28861
[Tarski1999] p. 179Axiom 7axtgpasch 28863
[Tarski1999] p. 180Axiom 7.1axtgpasch 28863
[Tarski1999] p. 185Axiom 11axtgcont1 28864
[Truss] p. 114Theorem 5.18ruc 16379
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38497
[Viaclovsky8] p. 3Proposition 7ismblfin 38499
[Weierstrass] p. 272Definitiondf-mdet 22862  mdetuni 22899
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 917
[WhiteheadRussell] p. 96Axiom *1.3olc 882
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 883
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 933
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 983
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 190
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 136
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 91  wl-luk-pm2.04 38288
[WhiteheadRussell] p. 100Theorem *2.05frege5 44744  imim2 59  wl-luk-imim2 38283
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 48011  imim1 84
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 910
[WhiteheadRussell] p. 101Theorem *2.06barbara 2687  syl 18
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 916
[WhiteheadRussell] p. 101Theorem *2.08id 23  wl-luk-id 38286
[WhiteheadRussell] p. 101Theorem *2.11exmid 908
[WhiteheadRussell] p. 101Theorem *2.12notnot 143
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 911
[WhiteheadRussell] p. 102Theorem *2.14notnotr 131  notnotrALT2 45853  wl-luk-notnotr 38287
[WhiteheadRussell] p. 102Theorem *2.15con1 147
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44774  axfrege28 44773  con3 154
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 129
[WhiteheadRussell] p. 104Theorem *2.2orc 881
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 938
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 124  wl-luk-pm2.21 38280
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 125
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 903
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 954
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30936  pm2.27 43  wl-luk-pm2.27 38278
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 936
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 39223
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 937
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 985
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 986
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 984
[WhiteheadRussell] p. 105Definition *2.33df-3or 1104
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 920
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 921
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 957
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 57
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 895
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 896
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 170  pm2.5g 169
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 193
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 897
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 898
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 899
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 173
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 174
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 865
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 866
[WhiteheadRussell] p. 107Theorem *2.55orel1 902
[WhiteheadRussell] p. 107Theorem *2.56orel2 904
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 194
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 913
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 955
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 956
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 195
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 905  pm2.67 906
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 177  pm2.521g 175  pm2.521g2 176
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 912
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 988
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 914
[WhiteheadRussell] p. 108Theorem *2.69looinv 206
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 989
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 990
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 947
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 945
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 987
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 991
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 85
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 946
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 110
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1007
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 475  pm3.2im 161
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1008
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1009
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1010
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1011
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 477
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 465
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 408
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 815
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 454
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 455
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 488  simplim 168
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 490  simprim 167
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 777
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 778
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 820
[WhiteheadRussell] p. 113Fact)pm3.45 634
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 822
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 498
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 499
[WhiteheadRussell] p. 113Theorem *3.44jao 975  pm3.44 974
[WhiteheadRussell] p. 113Theorem *3.47anim12 821
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 479
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 978
[WhiteheadRussell] p. 116Theorem *4.1con34b 319
[WhiteheadRussell] p. 117Theorem *4.2biid 264
[WhiteheadRussell] p. 117Theorem *4.11notbi 322
[WhiteheadRussell] p. 117Theorem *4.12con2bi 356
[WhiteheadRussell] p. 117Theorem *4.13notnotb 318
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 819
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 846
[WhiteheadRussell] p. 117Theorem *4.21bicom 225
[WhiteheadRussell] p. 117Theorem *4.22biantr 818  bitr 817
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 574
[WhiteheadRussell] p. 117Theorem *4.25oridm 918  pm4.25 919
[WhiteheadRussell] p. 118Theorem *4.3ancom 466
[WhiteheadRussell] p. 118Theorem *4.4andi 1025
[WhiteheadRussell] p. 118Theorem *4.31orcom 884
[WhiteheadRussell] p. 118Theorem *4.32anass 474
[WhiteheadRussell] p. 118Theorem *4.33orass 935
[WhiteheadRussell] p. 118Theorem *4.36anbi1 645
[WhiteheadRussell] p. 118Theorem *4.37orbi1 931
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 649
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 992
[WhiteheadRussell] p. 118Definition *4.34df-3an 1105
[WhiteheadRussell] p. 119Theorem *4.41ordi 1023
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1069
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1040
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1012
[WhiteheadRussell] p. 119Theorem *4.45orabs 1014  pm4.45 1013  pm4.45im 841
[WhiteheadRussell] p. 120Theorem *4.5anor 998
[WhiteheadRussell] p. 120Theorem *4.6imor 867
[WhiteheadRussell] p. 120Theorem *4.7anclb 555
[WhiteheadRussell] p. 120Theorem *4.51ianor 997
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 1000
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 1001
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 1002
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 1003
[WhiteheadRussell] p. 120Theorem *4.56ioran 999  pm4.56 1004
[WhiteheadRussell] p. 120Theorem *4.57oran 1005  pm4.57 1006
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 410
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 870
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 403
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 863
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 411
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 864
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 404
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 567  pm4.71d 571  pm4.71i 569  pm4.71r 568  pm4.71rd 572  pm4.71ri 570
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 964
[WhiteheadRussell] p. 121Theorem *4.73iba 537
[WhiteheadRussell] p. 121Theorem *4.74biorf 950
[WhiteheadRussell] p. 121Theorem *4.76jcab 527  pm4.76 528
[WhiteheadRussell] p. 121Theorem *4.77jaob 976  pm4.77 977
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 948
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1021
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 398
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 399
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1041
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1042
[WhiteheadRussell] p. 122Theorem *4.84imbi1 350
[WhiteheadRussell] p. 122Theorem *4.85imbi2 351
[WhiteheadRussell] p. 122Theorem *4.86bibi1 354
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 392  impexp 456  pm4.87 857
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 836
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 959  pm5.11g 958
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 960
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 962
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 961
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1030
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1031
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1029
[WhiteheadRussell] p. 124Theorem *5.18nbbn 386  pm5.18 384
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 391
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 837
[WhiteheadRussell] p. 124Theorem *5.22xor 1032
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1065
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1066
[WhiteheadRussell] p. 124Theorem *5.25dfor2 915
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 583
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 393
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 364
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1017
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 968
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 844
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 584
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 849
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 838
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 847
[WhiteheadRussell] p. 125Theorem *5.41imdi 394  pm5.41 395
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 553
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 552
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1022
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1035
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 963
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1016
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1036
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1037
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1045
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 369
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 273
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1046
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 37413
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 45286
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 45287
[WhiteheadRussell] p. 147Theorem *10.2219.26 1903
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 45288
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 45289
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 45290
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1926
[WhiteheadRussell] p. 151Theorem *10.301albitr 45291
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 45292
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 45293
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 45294
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 45295
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 45297
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 45298
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 45299
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 45296
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2127
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 45302
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 45303
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2107
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2197
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1862
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1863
[WhiteheadRussell] p. 161Theorem *11.319.21vv 45304
[WhiteheadRussell] p. 162Theorem *11.322alim 45305
[WhiteheadRussell] p. 162Theorem *11.332albi 45306
[WhiteheadRussell] p. 162Theorem *11.342exim 45307
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 45309
[WhiteheadRussell] p. 162Theorem *11.3412exbi 45308
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1920
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 45311
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 45312
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 45310
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1861
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 45313
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 45314
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1879
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 45315
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2375
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1893
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 45320
[WhiteheadRussell] p. 165Theorem *11.56aaanv 45316
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 45317
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 45318
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 45319
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 45324
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 45321
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 45322
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 45323
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 45325
[WhiteheadRussell] p. 175Definition *14.02df-eu 2594
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 45335  pm13.13b 45336
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 45337
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3036
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3037
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3619
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 45343
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 45344
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 45338
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45479  pm13.193 45339
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 45340
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 45341
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 45342
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 45349
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 45348
[WhiteheadRussell] p. 184Definition *14.01iotasbc 45347
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3800
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 45350  pm14.122b 45351  pm14.122c 45352
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 45353  pm14.123b 45354  pm14.123c 45355
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 45357
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 45356
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 45358
[WhiteheadRussell] p. 190Theorem *14.22iota4 6508
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 45359
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6509
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 45360
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 45362
[WhiteheadRussell] p. 192Theorem *14.26eupick 2658  eupickbi 2661  sbaniota 45363
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 45361
[WhiteheadRussell] p. 192Theorem *14.271eubi 2609
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 45364
[WhiteheadRussell] p. 235Definition *30.01conventions 30935  df-fv 6535
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 10054  pm54.43lem 10053
[Young] p. 141Definition of operator orderingleop2 32660
[Young] p. 142Example 12.2(i)0leop 32666  idleop 32667
[vandenDries] p. 42Lemma 61irrapx1 43773
[vandenDries] p. 43Theorem 62pellex 43780  pellexlem1 43774

This page was last updated on 26-Sep-2026.
Copyright terms: Public domain