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 17632
[Adamek] p. 21Condition 3.1(b)df-cat 17632
[Adamek] p. 22Example 3.3(1)df-setc 18041
[Adamek] p. 24Example 3.3(4.c)0cat 17653  0funcg 49576  df-termc 49964
[Adamek] p. 24Example 3.3(4.d)df-prstc 50041  prsthinc 49955
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50069  df-mndtc 50069
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50065
[Adamek] p. 25Definition 3.5df-oppc 17676
[Adamek] p. 25Example 3.6(1)oduoppcciso 50057
[Adamek] p. 25Example 3.6(2)oppgoppcco 50082  oppgoppchom 50081  oppgoppcid 50083
[Adamek] p. 28Remark 3.9oppciso 17746
[Adamek] p. 28Remark 3.12invf1o 17734  invisoinvl 17755
[Adamek] p. 28Example 3.13idinv 17754  idiso 17753
[Adamek] p. 28Corollary 3.11inveq 17739
[Adamek] p. 28Definition 3.8df-inv 17713  df-iso 17714  dfiso2 17737
[Adamek] p. 28Proposition 3.10sectcan 17720
[Adamek] p. 29Remark 3.16cicer 17771  cicerALT 49537
[Adamek] p. 29Definition 3.15cic 17764  df-cic 17761
[Adamek] p. 29Definition 3.17df-func 17823
[Adamek] p. 29Proposition 3.14(1)invinv 17735
[Adamek] p. 29Proposition 3.14(2)invco 17736  isoco 17742
[Adamek] p. 30Remark 3.19df-func 17823
[Adamek] p. 30Example 3.20(1)idfucl 17846
[Adamek] p. 30Example 3.20(2)diag1 49795
[Adamek] p. 32Proposition 3.21funciso 17839
[Adamek] p. 33Example 3.26(1)discsnterm 50065  discthing 49952
[Adamek] p. 33Example 3.26(2)df-thinc 49909  prsthinc 49955  thincciso 49944  thincciso2 49946  thincciso3 49947  thinccisod 49945
[Adamek] p. 33Example 3.26(3)df-mndtc 50069
[Adamek] p. 33Proposition 3.23cofucl 17853  cofucla 49587
[Adamek] p. 34Remark 3.28(1)cofidfth 49653
[Adamek] p. 34Remark 3.28(2)catciso 18076  catcisoi 49891
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18131
[Adamek] p. 34Definition 3.27(2)df-fth 17872
[Adamek] p. 34Definition 3.27(3)df-full 17871
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18131
[Adamek] p. 35Corollary 3.32ffthiso 17896
[Adamek] p. 35Proposition 3.30(c)cofth 17902
[Adamek] p. 35Proposition 3.30(d)cofull 17901
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18116
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18116
[Adamek] p. 39Remark 3.422oppf 49623
[Adamek] p. 39Definition 3.41df-oppf 49614  funcoppc 17840
[Adamek] p. 39Definition 3.44.df-catc 18064  elcatchom 49888
[Adamek] p. 39Proposition 3.43(c)fthoppc 17890  fthoppf 49655
[Adamek] p. 39Proposition 3.43(d)fulloppc 17889  fulloppf 49654
[Adamek] p. 40Remark 3.48catccat 18073
[Adamek] p. 40Definition 3.470funcg 49576  df-catc 18064
[Adamek] p. 45Exercise 3Gincat 50092
[Adamek] p. 48Remark 4.2(2)cnelsubc 50095  nelsubc3 49562
[Adamek] p. 48Remark 4.2(3)imasubc 49642  imasubc2 49643  imasubc3 49647
[Adamek] p. 48Example 4.3(1.a)0subcat 17803
[Adamek] p. 48Example 4.3(1.b)catsubcat 17804
[Adamek] p. 48Definition 4.1(1)nelsubc3 49562
[Adamek] p. 48Definition 4.1(2)fullsubc 17815
[Adamek] p. 48Definition 4.1(a)df-subc 17777
[Adamek] p. 49Remark 4.4idsubc 49651
[Adamek] p. 49Remark 4.4(1)idemb 49650
[Adamek] p. 49Remark 4.4(2)idfullsubc 49652  ressffth 17905
[Adamek] p. 58Exercise 4Asetc1onsubc 50093
[Adamek] p. 83Definition 6.1df-nat 17911
[Adamek] p. 87Remark 6.14(a)fuccocl 17932
[Adamek] p. 87Remark 6.14(b)fucass 17936
[Adamek] p. 87Definition 6.15df-fuc 17912
[Adamek] p. 88Remark 6.16fuccat 17938
[Adamek] p. 101Definition 7.10funcg 49576  df-inito 17949
[Adamek] p. 101Example 7.2(3)0funcg 49576  df-termc 49964  initc 49582
[Adamek] p. 101Example 7.2 (6)irinitoringc 21461
[Adamek] p. 102Definition 7.4df-termo 17950  oppctermo 49727
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17977
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17981
[Adamek] p. 103Remark 7.8oppczeroo 49728
[Adamek] p. 103Definition 7.7df-zeroo 17951
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21462
[Adamek] p. 103Proposition 7.6termoeu1w 17984
[Adamek] p. 106Definition 7.19df-sect 17712
[Adamek] p. 107Example 7.20(7)thincinv 49960
[Adamek] p. 108Example 7.25(4)thincsect2 49959
[Adamek] p. 110Example 7.33(9)thincmon 49924
[Adamek] p. 110Proposition 7.35sectmon 17747
[Adamek] p. 112Proposition 7.42sectepi 17749
[Adamek] p. 185Section 10.67updjud 9856
[Adamek] p. 193Definition 11.1(1)df-lmd 50136
[Adamek] p. 193Definition 11.3(1)df-lmd 50136
[Adamek] p. 194Definition 11.3(2)df-lmd 50136
[Adamek] p. 202Definition 11.27(1)df-cmd 50137
[Adamek] p. 202Definition 11.27(2)df-cmd 50137
[Adamek] p. 478Item Rngdf-ringc 20625
[AhoHopUll] p. 2Section 1.1df-bigo 49040
[AhoHopUll] p. 12Section 1.3df-blen 49062
[AhoHopUll] p. 318Section 9.1df-concat 14531  df-pfx 14632  df-substr 14602  df-word 14474  lencl 14493  wrd0 14499
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24698  df-nmoo 30841
[AkhiezerGlazman] p. 64Theoremhmopidmch 32249  hmopidmchi 32247
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32297  pjcmul2i 32298
[AkhiezerGlazman] p. 72Theoremcnvunop 32014  unoplin 32016
[AkhiezerGlazman] p. 72Equation 2unopadj 32015  unopadj2 32034
[AkhiezerGlazman] p. 73Theoremelunop2 32109  lnopunii 32108
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32182
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27944
[Alling] p. 184Axiom Bbdayfo 27666
[Alling] p. 184Axiom Oltsso 27665
[Alling] p. 184Axiom SDnodense 27681
[Alling] p. 185Lemma 0nocvxmin 27772
[Alling] p. 185Theoremconway 27796
[Alling] p. 185Axiom FEnoeta 27732
[Alling] p. 186Theorem 4lesrec 27816  lesrecd 27817
[Alling], p. 2Definitionrp-brsslt 43868
[Alling], p. 3Notenla0001 43871  nla0002 43869  nla0003 43870
[Apostol] p. 18Theorem I.1addcan 11328  addcan2d 11348  addcan2i 11338  addcand 11347  addcani 11337
[Apostol] p. 18Theorem I.2negeu 11381
[Apostol] p. 18Theorem I.3negsub 11440  negsubd 11509  negsubi 11470
[Apostol] p. 18Theorem I.4negneg 11442  negnegd 11494  negnegi 11462
[Apostol] p. 18Theorem I.5subdi 11581  subdid 11604  subdii 11597  subdir 11582  subdird 11605  subdiri 11598
[Apostol] p. 18Theorem I.6mul01 11323  mul01d 11343  mul01i 11334  mul02 11322  mul02d 11342  mul02i 11333
[Apostol] p. 18Theorem I.7mulcan 11785  mulcan2d 11782  mulcand 11781  mulcani 11787
[Apostol] p. 18Theorem I.8receu 11793  xreceu 33007
[Apostol] p. 18Theorem I.9divrec 11823  divrecd 11932  divreci 11898  divreczi 11891
[Apostol] p. 18Theorem I.10recrec 11850  recreci 11885
[Apostol] p. 18Theorem I.11mul0or 11788  mul0ord 11796  mul0ori 11795
[Apostol] p. 18Theorem I.12mul2neg 11587  mul2negd 11603  mul2negi 11596  mulneg1 11584  mulneg1d 11601  mulneg1i 11594
[Apostol] p. 18Theorem I.13divadddiv 11868  divadddivd 11973  divadddivi 11915
[Apostol] p. 18Theorem I.14divmuldiv 11853  divmuldivd 11970  divmuldivi 11913  rdivmuldivd 20391
[Apostol] p. 18Theorem I.15divdivdiv 11854  divdivdivd 11976  divdivdivi 11916
[Apostol] p. 20Axiom 7rpaddcl 12964  rpaddcld 12999  rpmulcl 12965  rpmulcld 13000
[Apostol] p. 20Axiom 8rpneg 12974
[Apostol] p. 20Axiom 90nrp 12977
[Apostol] p. 20Theorem I.17lttri 11270
[Apostol] p. 20Theorem I.18ltadd1d 11741  ltadd1dd 11759  ltadd1i 11702
[Apostol] p. 20Theorem I.19ltmul1 12003  ltmul1a 12002  ltmul1i 12072  ltmul1ii 12082  ltmul2 12004  ltmul2d 13026  ltmul2dd 13040  ltmul2i 12075
[Apostol] p. 20Theorem I.20msqgt0 11668  msqgt0d 11715  msqgt0i 11685
[Apostol] p. 20Theorem I.210lt1 11670
[Apostol] p. 20Theorem I.23lt0neg1 11654  lt0neg1d 11717  ltneg 11648  ltnegd 11726  ltnegi 11692
[Apostol] p. 20Theorem I.25lt2add 11633  lt2addd 11771  lt2addi 11710
[Apostol] p. 20Definition of positive numbersdf-rp 12941
[Apostol] p. 21Exercise 4recgt0 11999  recgt0d 12088  recgt0i 12059  recgt0ii 12060
[Apostol] p. 22Definition of integersdf-z 12523
[Apostol] p. 22Definition of positive integersdfnn3 12186
[Apostol] p. 22Definition of rationalsdf-q 12897
[Apostol] p. 24Theorem I.26supeu 9364
[Apostol] p. 26Theorem I.28nnunb 12431
[Apostol] p. 26Theorem I.29arch 12432  archd 45610
[Apostol] p. 28Exercise 2btwnz 12630
[Apostol] p. 28Exercise 3nnrecl 12433
[Apostol] p. 28Exercise 4rebtwnz 12895
[Apostol] p. 28Exercise 5zbtwnre 12894
[Apostol] p. 28Exercise 6qbtwnre 13149
[Apostol] p. 28Exercise 10(a)zeneo 16306  zneo 12610  zneoALTV 48161
[Apostol] p. 29Theorem I.35cxpsqrtth 26719  msqsqrtd 15403  resqrtth 15215  sqrtth 15325  sqrtthi 15331  sqsqrtd 15402
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12175
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12861
[Apostol] p. 361Remarkcrreczi 14188
[Apostol] p. 363Remarkabsgt0i 15360
[Apostol] p. 363Exampleabssubd 15416  abssubi 15364
[ApostolNT] p. 7Remarkfmtno0 48019  fmtno1 48020  fmtno2 48029  fmtno3 48030  fmtno4 48031  fmtno5fac 48061  fmtnofz04prm 48056
[ApostolNT] p. 7Definitiondf-fmtno 48007
[ApostolNT] p. 8Definitiondf-ppi 27088
[ApostolNT] p. 14Definitiondf-dvds 16220
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16236
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16261
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16256
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16249
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16251
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16237
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16238
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16243
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16278
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16280
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16282
[ApostolNT] p. 15Definitiondf-gcd 16462  dfgcd2 16513
[ApostolNT] p. 16Definitionisprm2 16649
[ApostolNT] p. 16Theorem 1.5coprmdvds 16620
[ApostolNT] p. 16Theorem 1.7prminf 16884
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16480
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16514
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16516
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16495
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16487
[ApostolNT] p. 17Theorem 1.8coprm 16679
[ApostolNT] p. 17Theorem 1.9euclemma 16681
[ApostolNT] p. 17Theorem 1.101arith2 16897
[ApostolNT] p. 18Theorem 1.13prmrec 16891
[ApostolNT] p. 19Theorem 1.14divalg 16370
[ApostolNT] p. 20Theorem 1.15eucalg 16554
[ApostolNT] p. 24Definitiondf-mu 27089
[ApostolNT] p. 25Definitiondf-phi 16734
[ApostolNT] p. 25Theorem 2.1musum 27179
[ApostolNT] p. 26Theorem 2.2phisum 16759
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16744
[ApostolNT] p. 28Theorem 2.5(c)phimul 16748
[ApostolNT] p. 32Definitiondf-vma 27086
[ApostolNT] p. 32Theorem 2.9muinv 27181
[ApostolNT] p. 32Theorem 2.10vmasum 27204
[ApostolNT] p. 38Remarkdf-sgm 27090
[ApostolNT] p. 38Definitiondf-sgm 27090
[ApostolNT] p. 75Definitiondf-chp 27087  df-cht 27085
[ApostolNT] p. 104Definitioncongr 16631
[ApostolNT] p. 106Remarkdvdsval3 16223
[ApostolNT] p. 106Definitionmoddvds 16230
[ApostolNT] p. 107Example 2mod2eq0even 16313
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16314
[ApostolNT] p. 107Example 4zmod1congr 13845
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13885
[ApostolNT] p. 107Theorem 5.2(c)modexp 14198
[ApostolNT] p. 108Theorem 5.3modmulconst 16255
[ApostolNT] p. 109Theorem 5.4cncongr1 16634
[ApostolNT] p. 109Theorem 5.6gcdmodi 17043
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16636
[ApostolNT] p. 113Theorem 5.17eulerth 16751
[ApostolNT] p. 113Theorem 5.18vfermltl 16770
[ApostolNT] p. 114Theorem 5.19fermltl 16752
[ApostolNT] p. 116Theorem 5.24wilthimp 27060
[ApostolNT] p. 179Definitiondf-lgs 27283  lgsprme0 27327
[ApostolNT] p. 180Example 11lgs 27328
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27304
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27319
[ApostolNT] p. 181Theorem 9.4m1lgs 27376
[ApostolNT] p. 181Theorem 9.52lgs 27395  2lgsoddprm 27404
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27362
[ApostolNT] p. 185Theorem 9.8lgsquad 27371
[ApostolNT] p. 188Definitiondf-lgs 27283  lgs1 27329
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27320
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27322
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27330
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27331
[Baer] p. 40Property (b)mapdord 42131
[Baer] p. 40Property (c)mapd11 42132
[Baer] p. 40Property (e)mapdin 42155  mapdlsm 42157
[Baer] p. 40Property (f)mapd0 42158
[Baer] p. 40Definition of projectivitydf-mapd 42118  mapd1o 42141
[Baer] p. 41Property (g)mapdat 42160
[Baer] p. 44Part (1)mapdpg 42199
[Baer] p. 45Part (2)hdmap1eq 42294  mapdheq 42221  mapdheq2 42222  mapdheq2biN 42223
[Baer] p. 45Part (3)baerlem3 42206
[Baer] p. 46Part (4)mapdheq4 42225  mapdheq4lem 42224
[Baer] p. 46Part (5)baerlem5a 42207  baerlem5abmN 42211  baerlem5amN 42209  baerlem5b 42208  baerlem5bmN 42210
[Baer] p. 47Part (6)hdmap1l6 42314  hdmap1l6a 42302  hdmap1l6e 42307  hdmap1l6f 42308  hdmap1l6g 42309  hdmap1l6lem1 42300  hdmap1l6lem2 42301  mapdh6N 42240  mapdh6aN 42228  mapdh6eN 42233  mapdh6fN 42234  mapdh6gN 42235  mapdh6lem1N 42226  mapdh6lem2N 42227
[Baer] p. 48Part 9hdmapval 42321
[Baer] p. 48Part 10hdmap10 42333
[Baer] p. 48Part 11hdmapadd 42336
[Baer] p. 48Part (6)hdmap1l6h 42310  mapdh6hN 42236
[Baer] p. 48Part (7)mapdh75cN 42246  mapdh75d 42247  mapdh75e 42245  mapdh75fN 42248  mapdh7cN 42242  mapdh7dN 42243  mapdh7eN 42241  mapdh7fN 42244
[Baer] p. 48Part (8)mapdh8 42281  mapdh8a 42268  mapdh8aa 42269  mapdh8ab 42270  mapdh8ac 42271  mapdh8ad 42272  mapdh8b 42273  mapdh8c 42274  mapdh8d 42276  mapdh8d0N 42275  mapdh8e 42277  mapdh8g 42278  mapdh8i 42279  mapdh8j 42280
[Baer] p. 48Part (9)mapdh9a 42282
[Baer] p. 48Equation 10mapdhvmap 42262
[Baer] p. 49Part 12hdmap11 42341  hdmapeq0 42337  hdmapf1oN 42358  hdmapneg 42339  hdmaprnN 42357  hdmaprnlem1N 42342  hdmaprnlem3N 42343  hdmaprnlem3uN 42344  hdmaprnlem4N 42346  hdmaprnlem6N 42347  hdmaprnlem7N 42348  hdmaprnlem8N 42349  hdmaprnlem9N 42350  hdmapsub 42340
[Baer] p. 49Part 14hdmap14lem1 42361  hdmap14lem10 42370  hdmap14lem1a 42359  hdmap14lem2N 42362  hdmap14lem2a 42360  hdmap14lem3 42363  hdmap14lem8 42368  hdmap14lem9 42369
[Baer] p. 50Part 14hdmap14lem11 42371  hdmap14lem12 42372  hdmap14lem13 42373  hdmap14lem14 42374  hdmap14lem15 42375  hgmapval 42380
[Baer] p. 50Part 15hgmapadd 42387  hgmapmul 42388  hgmaprnlem2N 42390  hgmapvs 42384
[Baer] p. 50Part 16hgmaprnN 42394
[Baer] p. 110Lemma 1hdmapip0com 42410
[Baer] p. 110Line 27hdmapinvlem1 42411
[Baer] p. 110Line 28hdmapinvlem2 42412
[Baer] p. 110Line 30hdmapinvlem3 42413
[Baer] p. 110Part 1.2hdmapglem5 42415  hgmapvv 42419
[Baer] p. 110Proposition 1hdmapinvlem4 42414
[Baer] p. 111Line 10hgmapvvlem1 42416
[Baer] p. 111Line 15hdmapg 42423  hdmapglem7 42422
[Bauer], p. 483Theorem 1.22irrexpq 26720  2irrexpqALT 26789
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2573
[BellMachover] p. 460Notationdf-mo 2543
[BellMachover] p. 460Definitionmo3 2568
[BellMachover] p. 461Axiom Extax-ext 2712
[BellMachover] p. 462Theorem 1.1axextmo 2716
[BellMachover] p. 463Axiom Repaxrep5 5214
[BellMachover] p. 463Scheme Sepax-sep 5225
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37418  sepex 5229
[BellMachover] p. 466Problemaxpow2 5303
[BellMachover] p. 466Axiom Powaxpow3 5304
[BellMachover] p. 466Axiom Unionaxun2 7687
[BellMachover] p. 468Definitiondf-ord 6320
[BellMachover] p. 469Theorem 2.2(i)ordirr 6335
[BellMachover] p. 469Theorem 2.2(iii)onelon 6342
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6337
[BellMachover] p. 471Definition of Ndf-om 7814
[BellMachover] p. 471Problem 2.5(ii)uniordint 7751
[BellMachover] p. 471Definition of Limdf-lim 6322
[BellMachover] p. 472Axiom Infzfinf2 9561
[BellMachover] p. 473Theorem 2.8limom 7829
[BellMachover] p. 477Equation 3.1df-r1 9686
[BellMachover] p. 478Definitionrankval2 9740  rankval2b 35289
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9704  r1ord3g 9701
[BellMachover] p. 480Axiom Regzfreg 9508
[BellMachover] p. 488Axiom ACac5 10397  dfac4 10042
[BellMachover] p. 490Definition of alephalephval3 10030
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39812
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32449
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32491  chirredi 32490
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32479
[Beran] p. 3Definition of joinsshjval3 31450
[Beran] p. 39Theorem 2.3(i)cmcm2 31712  cmcm2i 31689  cmcm2ii 31694  cmt2N 39743
[Beran] p. 40Theorem 2.3(iii)lecm 31713  lecmi 31698  lecmii 31699
[Beran] p. 45Theorem 3.4cmcmlem 31687
[Beran] p. 49Theorem 4.2cm2j 31716  cm2ji 31721  cm2mi 31722
[Beran] p. 95Definitiondf-sh 31303  issh2 31305
[Beran] p. 95Lemma 3.1(S5)his5 31182
[Beran] p. 95Lemma 3.1(S6)his6 31195
[Beran] p. 95Lemma 3.1(S7)his7 31186
[Beran] p. 95Lemma 3.2(S8)ho01i 31924
[Beran] p. 95Lemma 3.2(S9)hoeq1 31926
[Beran] p. 95Lemma 3.2(S10)ho02i 31925
[Beran] p. 95Lemma 3.2(S11)hoeq2 31927
[Beran] p. 95Postulate (S1)ax-his1 31178  his1i 31196
[Beran] p. 95Postulate (S2)ax-his2 31179
[Beran] p. 95Postulate (S3)ax-his3 31180
[Beran] p. 95Postulate (S4)ax-his4 31181
[Beran] p. 96Definition of normdf-hnorm 31064  dfhnorm2 31218  normval 31220
[Beran] p. 96Definition for Cauchy sequencehcau 31280
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31069
[Beran] p. 96Definition of complete subspaceisch3 31337
[Beran] p. 96Definition of convergedf-hlim 31068  hlimi 31284
[Beran] p. 97Theorem 3.3(i)norm-i-i 31229  norm-i 31225
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31233  norm-ii 31234  normlem0 31205  normlem1 31206  normlem2 31207  normlem3 31208  normlem4 31209  normlem5 31210  normlem6 31211  normlem7 31212  normlem7tALT 31215
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31235  norm-iii 31236
[Beran] p. 98Remark 3.4bcs 31277  bcsiALT 31275  bcsiHIL 31276
[Beran] p. 98Remark 3.4(B)normlem9at 31217  normpar 31251  normpari 31250
[Beran] p. 98Remark 3.4(C)normpyc 31242  normpyth 31241  normpythi 31238
[Beran] p. 99Remarklnfn0 32143  lnfn0i 32138  lnop0 32062  lnop0i 32066
[Beran] p. 99Theorem 3.5(i)nmcexi 32122  nmcfnex 32149  nmcfnexi 32147  nmcopex 32125  nmcopexi 32123
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32150  nmcfnlbi 32148  nmcoplb 32126  nmcoplbi 32124
[Beran] p. 99Theorem 3.5(iii)lnfncon 32152  lnfnconi 32151  lnopcon 32131  lnopconi 32130
[Beran] p. 100Lemma 3.6normpar2i 31252
[Beran] p. 101Lemma 3.6norm3adifi 31249  norm3adifii 31244  norm3dif 31246  norm3difi 31243
[Beran] p. 102Theorem 3.7(i)chocunii 31397  pjhth 31489  pjhtheu 31490  pjpjhth 31521  pjpjhthi 31522  pjth 25431
[Beran] p. 102Theorem 3.7(ii)ococ 31502  ococi 31501
[Beran] p. 103Remark 3.8nlelchi 32157
[Beran] p. 104Theorem 3.9riesz3i 32158  riesz4 32160  riesz4i 32159
[Beran] p. 104Theorem 3.10cnlnadj 32175  cnlnadjeu 32174  cnlnadjeui 32173  cnlnadji 32172  cnlnadjlem1 32163  nmopadjlei 32184
[Beran] p. 106Theorem 3.11(i)adjeq0 32187
[Beran] p. 106Theorem 3.11(v)nmopadji 32186
[Beran] p. 106Theorem 3.11(ii)adjmul 32188
[Beran] p. 106Theorem 3.11(iv)adjadj 32032
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32198  nmopcoadji 32197
[Beran] p. 106Theorem 3.11(iii)adjadd 32189
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32199
[Beran] p. 106Theorem 3.11(viii)adjcoi 32196  pjadj2coi 32300  pjadjcoi 32257
[Beran] p. 107Definitiondf-ch 31317  isch2 31319
[Beran] p. 107Remark 3.12choccl 31402  isch3 31337  occl 31400  ocsh 31379  shoccl 31401  shocsh 31380
[Beran] p. 107Remark 3.12(B)ococin 31504
[Beran] p. 108Theorem 3.13chintcl 31428
[Beran] p. 109Property (i)pjadj2 32283  pjadj3 32284  pjadji 31781  pjadjii 31770
[Beran] p. 109Property (ii)pjidmco 32277  pjidmcoi 32273  pjidmi 31769
[Beran] p. 110Definition of projector orderingpjordi 32269
[Beran] p. 111Remarkho0val 31846  pjch1 31766
[Beran] p. 111Definitiondf-hfmul 31830  df-hfsum 31829  df-hodif 31828  df-homul 31827  df-hosum 31826
[Beran] p. 111Lemma 4.4(i)pjo 31767
[Beran] p. 111Lemma 4.4(ii)pjch 31790  pjchi 31528
[Beran] p. 111Lemma 4.4(iii)pjoc2 31535  pjoc2i 31534
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31776
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32261  pjssmii 31777
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32260
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32259
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32264
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32262  pjssge0ii 31778
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32263  pjdifnormii 31779
[Bobzien] p. 116Statement T3stoic3 1783
[Bobzien] p. 117Statement T2stoic2a 1781
[Bobzien] p. 117Statement T4stoic4a 1784
[Bobzien] p. 117Conclusion the contradictorystoic1a 1779
[Bogachev] p. 16Definition 1.5df-oms 34483
[Bogachev] p. 17Lemma 1.5.4omssubadd 34491
[Bogachev] p. 17Example 1.5.2omsmon 34489
[Bogachev] p. 41Definition 1.11.2df-carsg 34493
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34513
[Bogachev] p. 116Definition 2.3.1df-itgm 34544  df-sitm 34522
[Bogachev] p. 118Chapter 2.4.4df-itgm 34544
[Bogachev] p. 118Definition 2.4.1df-sitg 34521
[Bollobas] p. 1Section I.1df-edg 29142  isuhgrop 29164  isusgrop 29256  isuspgrop 29255
[Bollobas] p. 2Section I.1df-isubgr 48353  df-subgr 29362  uhgrspan1 29397  uhgrspansubgr 29385
[Bollobas] p. 3Definitiondf-gric 48373  gricuspgr 48410  isuspgrim 48388
[Bollobas] p. 3Section I.1cusgrsize 29548  df-clnbgr 48311  df-cusgr 29506  df-nbgr 29427  fusgrmaxsize 29558
[Bollobas] p. 4Definitiondf-upwlks 48626  df-wlks 29693
[Bollobas] p. 4Section I.1finsumvtxdg2size 29644  finsumvtxdgeven 29646  fusgr1th 29645  fusgrvtxdgonume 29648  vtxdgoddnumeven 29647
[Bollobas] p. 5Notationdf-pths 29807
[Bollobas] p. 5Definitiondf-crcts 29879  df-cycls 29880  df-trls 29784  df-wlkson 29694
[Bollobas] p. 7Section I.1df-ushgr 29153
[BourbakiAlg1] p. 1Definition 1df-clintop 48692  df-cllaw 48678  df-mgm 18606  df-mgm2 48711
[BourbakiAlg1] p. 4Definition 5df-assintop 48693  df-asslaw 48680  df-sgrp 18685  df-sgrp2 48713
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48712  df-comlaw 48679
[BourbakiAlg1] p. 12Definition 2df-mnd 18701
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33112  mndlactf1o 33116  mndractf1 33114  mndractf1o 33117
[BourbakiAlg1] p. 92Definition 1df-ring 20214
[BourbakiAlg1] p. 93Section I.8.1df-rng 20132
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33824
[BourbakiAlg2] p. 113Chapter 5.assafld 33828  assarrginv 33827
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33869  fldextrspunfld 33867  fldextrspunlem1 33866  fldextrspunlem2 33868  fldextrspunlsp 33865  fldextrspunlsplem 33864
[BourbakiCAlg2], p. 228Proposition 21arithidom 33627  dfufd2 33640
[BourbakiEns] p. Proposition 8fcof1 7238  fcofo 7239
[BourbakiTop1] p. Remarkxnegmnf 13160  xnegpnf 13159
[BourbakiTop1] p. Remark rexneg 13161
[BourbakiTop1] p. Remark 3ust0 24210  ustfilxp 24203
[BourbakiTop1] p. Axiom GT'tgpsubcn 24080
[BourbakiTop1] p. Criterionishmeo 23749
[BourbakiTop1] p. Example 1cstucnd 24273  iducn 24272  snfil 23854
[BourbakiTop1] p. Example 2neifil 23870
[BourbakiTop1] p. Theorem 1cnextcn 24057
[BourbakiTop1] p. Theorem 2ucnextcn 24293
[BourbakiTop1] p. Theorem 3df-hcmp 34148
[BourbakiTop1] p. Paragraph 3infil 23853
[BourbakiTop1] p. Definition 1df-ucn 24265  df-ust 24191  filintn0 23851  filn0 23852  istgp 24067  ucnprima 24271
[BourbakiTop1] p. Definition 2df-cfilu 24276
[BourbakiTop1] p. Definition 3df-cusp 24287  df-usp 24247  df-utop 24221  trust 24219
[BourbakiTop1] p. Definition 6df-pcmp 34047
[BourbakiTop1] p. Property V_issnei2 23106
[BourbakiTop1] p. Theorem 1(d)iscncl 23259
[BourbakiTop1] p. Condition F_Iustssel 24196
[BourbakiTop1] p. Condition U_Iustdiag 24199
[BourbakiTop1] p. Property V_iiinnei 23115
[BourbakiTop1] p. Property V_ivneiptopreu 23123  neissex 23117
[BourbakiTop1] p. Proposition 1neips 23103  neiss 23099  ucncn 24274  ustund 24212  ustuqtop 24236
[BourbakiTop1] p. Proposition 2cnpco 23257  neiptopreu 23123  utop2nei 24240  utop3cls 24241
[BourbakiTop1] p. Proposition 3fmucnd 24281  uspreg 24263  utopreg 24242
[BourbakiTop1] p. Proposition 4imasncld 23681  imasncls 23682  imasnopn 23680
[BourbakiTop1] p. Proposition 9cnpflf2 23990
[BourbakiTop1] p. Condition F_IIustincl 24198
[BourbakiTop1] p. Condition U_IIustinvel 24200
[BourbakiTop1] p. Property V_iiielnei 23101
[BourbakiTop1] p. Proposition 11cnextucn 24292
[BourbakiTop1] p. Condition F_IIbustbasel 24197
[BourbakiTop1] p. Condition U_IIIustexhalf 24201
[BourbakiTop1] p. Definition C'''df-cmp 23377
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23836
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22884
[BourbakiTop2] p. 195Definition 1df-ldlf 34044
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46506
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46508  stoweid 46507
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46445  stoweidlem10 46454  stoweidlem14 46458  stoweidlem15 46459  stoweidlem35 46479  stoweidlem36 46480  stoweidlem37 46481  stoweidlem38 46482  stoweidlem40 46484  stoweidlem41 46485  stoweidlem43 46487  stoweidlem44 46488  stoweidlem46 46490  stoweidlem5 46449  stoweidlem50 46494  stoweidlem52 46496  stoweidlem53 46497  stoweidlem55 46499  stoweidlem56 46500
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46467  stoweidlem24 46468  stoweidlem27 46471  stoweidlem28 46472  stoweidlem30 46474
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46478  stoweidlem59 46503  stoweidlem60 46504
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46489  stoweidlem49 46493  stoweidlem7 46451
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46475  stoweidlem39 46483  stoweidlem42 46486  stoweidlem48 46492  stoweidlem51 46495  stoweidlem54 46498  stoweidlem57 46501  stoweidlem58 46502
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46469
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46461
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46455  stoweidlem13 46457  stoweidlem26 46470  stoweidlem61 46505
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46462
[Bruck] p. 1Section I.1df-clintop 48692  df-mgm 18606  df-mgm2 48711
[Bruck] p. 23Section II.1df-sgrp 18685  df-sgrp2 48713
[Bruck] p. 28Theorem 3.2dfgrp3 19013
[ChoquetDD] p. 2Definition of mappingdf-mpt 5161
[Church] p. 129Section II.24df-ifp 1069  dfifp2 1070
[Clemente] p. 10Definition ITnatded 30498
[Clemente] p. 10Definition I` `m,nnatded 30498
[Clemente] p. 11Definition E=>m,nnatded 30498
[Clemente] p. 11Definition I=>m,nnatded 30498
[Clemente] p. 11Definition E` `(1)natded 30498
[Clemente] p. 11Definition E` `(2)natded 30498
[Clemente] p. 12Definition E` `m,n,pnatded 30498
[Clemente] p. 12Definition I` `n(1)natded 30498
[Clemente] p. 12Definition I` `n(2)natded 30498
[Clemente] p. 13Definition I` `m,n,pnatded 30498
[Clemente] p. 14Proof 5.11natded 30498
[Clemente] p. 14Definition E` `nnatded 30498
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30500  ex-natded5.2 30499
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30503  ex-natded5.3 30502
[Clemente] p. 18Theorem 5.5ex-natded5.5 30505
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30507  ex-natded5.7 30506
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30509  ex-natded5.8 30508
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30511  ex-natded5.13 30510
[Clemente] p. 32Definition I` `nnatded 30498
[Clemente] p. 32Definition E` `m,n,p,anatded 30498
[Clemente] p. 32Definition E` `n,tnatded 30498
[Clemente] p. 32Definition I` `n,tnatded 30498
[Clemente] p. 43Theorem 9.20ex-natded9.20 30512
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30513
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30515  ex-natded9.26 30514
[Cohen] p. 301Remarkrelogoprlem 26580
[Cohen] p. 301Property 2relogmul 26581  relogmuld 26614
[Cohen] p. 301Property 3relogdiv 26582  relogdivd 26615
[Cohen] p. 301Property 4relogexp 26585
[Cohen] p. 301Property 1alog1 26574
[Cohen] p. 301Property 1bloge 26575
[Cohen4] p. 348Observationrelogbcxpb 26776
[Cohen4] p. 349Propertyrelogbf 26780
[Cohen4] p. 352Definitionelogb 26759
[Cohen4] p. 361Property 2relogbmul 26766
[Cohen4] p. 361Property 3logbrec 26771  relogbdiv 26768
[Cohen4] p. 361Property 4relogbreexp 26764
[Cohen4] p. 361Property 6relogbexp 26769
[Cohen4] p. 361Property 1(a)logbid1 26757
[Cohen4] p. 361Property 1(b)logb1 26758
[Cohen4] p. 367Propertylogbchbase 26760
[Cohen4] p. 377Property 2logblt 26773
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34476  sxbrsigalem4 34478
[Cohn] p. 81Section II.5acsdomd 18521  acsinfd 18520  acsinfdimd 18522  acsmap2d 18519  acsmapd 18518
[Cohn] p. 143Example 5.1.1sxbrsiga 34481
[Connell] p. 57Definitiondf-scmat 22481  df-scmatalt 48891
[Conway] p. 4Definitionlesrec 27816  lesrecd 27817
[Conway] p. 5Definitionaddsval 27979  addsval2 27980  df-adds 27977  df-muls 28124  df-negs 28038
[Conway] p. 7Theorem0lt1s 27829
[Conway] p. 12Theorem 12pw2cut2 28479
[Conway] p. 16Theorem 0(i)sltsright 27878
[Conway] p. 16Theorem 0(ii)sltsleft 27877
[Conway] p. 16Theorem 0(iii)lesid 27756
[Conway] p. 17Theorem 3addsass 28022  addsassd 28023  addscom 27983  addscomd 27984  addsrid 27981  addsridd 27982
[Conway] p. 17Definitiondf-0s 27824
[Conway] p. 17Theorem 4(ii)negnegs 28061
[Conway] p. 17Theorem 4(iii)negsid 28058  negsidd 28059
[Conway] p. 18Theorem 5leadds1 28006  leadds1d 28012
[Conway] p. 18Definitiondf-1s 27825
[Conway] p. 18Theorem 6(ii)negscl 28053  negscld 28054
[Conway] p. 18Theorem 6(iii)addscld 27997
[Conway] p. 19Notemulsunif2 28187
[Conway] p. 19Theorem 7addsdi 28172  addsdid 28173  addsdird 28174  mulnegs1d 28177  mulnegs2d 28178  mulsass 28183  mulsassd 28184  mulscom 28156  mulscomd 28157
[Conway] p. 19Theorem 8(i)mulscl 28151  mulscld 28152
[Conway] p. 19Theorem 8(iii)lemulsd 28155  ltmuls 28153  ltmulsd 28154
[Conway] p. 20Theorem 9mulsgt0 28161  mulsgt0d 28162
[Conway] p. 21Theorem 10(iv)precsex 28235
[Conway] p. 23Theorem 11eqcuts3 27821
[Conway] p. 24Definitiondf-reno 28507
[Conway] p. 24Theorem 13(ii)readdscl 28516  remulscl 28519  renegscl 28515
[Conway] p. 27Definitiondf-ons 28269  elons2 28275
[Conway] p. 27Theorem 14ltonsex 28279
[Conway] p. 28Theorem 15oncutlt 28281  onswe 28289
[Conway] p. 29Remarkmadebday 27917  newbday 27919  oldbday 27918
[Conway] p. 29Definitiondf-made 27844  df-new 27846  df-old 27845
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13818
[Crawley] p. 1Definition of posetdf-poset 18277
[Crawley] p. 107Theorem 13.2hlsupr 39879
[Crawley] p. 110Theorem 13.3arglem1N 40683  dalaw 40379
[Crawley] p. 111Theorem 13.4hlathil 42454
[Crawley] p. 111Definition of set Wdf-watsN 40483
[Crawley] p. 111Definition of dilationdf-dilN 40599  df-ldil 40597  isldil 40603
[Crawley] p. 111Definition of translationdf-ltrn 40598  df-trnN 40600  isltrn 40612  ltrnu 40614
[Crawley] p. 112Lemma Acdlema1N 40284  cdlema2N 40285  exatleN 39897
[Crawley] p. 112Lemma B1cvrat 39969  cdlemb 40287  cdlemb2 40534  cdlemb3 41099  idltrn 40643  l1cvat 39548  lhpat 40536  lhpat2 40538  lshpat 39549  ltrnel 40632  ltrnmw 40644
[Crawley] p. 112Lemma Ccdlemc1 40684  cdlemc2 40685  ltrnnidn 40667  trlat 40662  trljat1 40659  trljat2 40660  trljat3 40661  trlne 40678  trlnidat 40666  trlnle 40679
[Crawley] p. 112Definition of automorphismdf-pautN 40484
[Crawley] p. 113Lemma Ccdlemc 40690  cdlemc3 40686  cdlemc4 40687
[Crawley] p. 113Lemma Dcdlemd 40700  cdlemd1 40691  cdlemd2 40692  cdlemd3 40693  cdlemd4 40694  cdlemd5 40695  cdlemd6 40696  cdlemd7 40697  cdlemd8 40698  cdlemd9 40699  cdleme31sde 40878  cdleme31se 40875  cdleme31se2 40876  cdleme31snd 40879  cdleme32a 40934  cdleme32b 40935  cdleme32c 40936  cdleme32d 40937  cdleme32e 40938  cdleme32f 40939  cdleme32fva 40930  cdleme32fva1 40931  cdleme32fvcl 40933  cdleme32le 40940  cdleme48fv 40992  cdleme4gfv 41000  cdleme50eq 41034  cdleme50f 41035  cdleme50f1 41036  cdleme50f1o 41039  cdleme50laut 41040  cdleme50ldil 41041  cdleme50lebi 41033  cdleme50rn 41038  cdleme50rnlem 41037  cdlemeg49le 41004  cdlemeg49lebilem 41032
[Crawley] p. 113Lemma Ecdleme 41053  cdleme00a 40702  cdleme01N 40714  cdleme02N 40715  cdleme0a 40704  cdleme0aa 40703  cdleme0b 40705  cdleme0c 40706  cdleme0cp 40707  cdleme0cq 40708  cdleme0dN 40709  cdleme0e 40710  cdleme0ex1N 40716  cdleme0ex2N 40717  cdleme0fN 40711  cdleme0gN 40712  cdleme0moN 40718  cdleme1 40720  cdleme10 40747  cdleme10tN 40751  cdleme11 40763  cdleme11a 40753  cdleme11c 40754  cdleme11dN 40755  cdleme11e 40756  cdleme11fN 40757  cdleme11g 40758  cdleme11h 40759  cdleme11j 40760  cdleme11k 40761  cdleme11l 40762  cdleme12 40764  cdleme13 40765  cdleme14 40766  cdleme15 40771  cdleme15a 40767  cdleme15b 40768  cdleme15c 40769  cdleme15d 40770  cdleme16 40778  cdleme16aN 40752  cdleme16b 40772  cdleme16c 40773  cdleme16d 40774  cdleme16e 40775  cdleme16f 40776  cdleme16g 40777  cdleme19a 40796  cdleme19b 40797  cdleme19c 40798  cdleme19d 40799  cdleme19e 40800  cdleme19f 40801  cdleme1b 40719  cdleme2 40721  cdleme20aN 40802  cdleme20bN 40803  cdleme20c 40804  cdleme20d 40805  cdleme20e 40806  cdleme20f 40807  cdleme20g 40808  cdleme20h 40809  cdleme20i 40810  cdleme20j 40811  cdleme20k 40812  cdleme20l 40815  cdleme20l1 40813  cdleme20l2 40814  cdleme20m 40816  cdleme20y 40795  cdleme20zN 40794  cdleme21 40830  cdleme21d 40823  cdleme21e 40824  cdleme22a 40833  cdleme22aa 40832  cdleme22b 40834  cdleme22cN 40835  cdleme22d 40836  cdleme22e 40837  cdleme22eALTN 40838  cdleme22f 40839  cdleme22f2 40840  cdleme22g 40841  cdleme23a 40842  cdleme23b 40843  cdleme23c 40844  cdleme26e 40852  cdleme26eALTN 40854  cdleme26ee 40853  cdleme26f 40856  cdleme26f2 40858  cdleme26f2ALTN 40857  cdleme26fALTN 40855  cdleme27N 40862  cdleme27a 40860  cdleme27cl 40859  cdleme28c 40865  cdleme3 40730  cdleme30a 40871  cdleme31fv 40883  cdleme31fv1 40884  cdleme31fv1s 40885  cdleme31fv2 40886  cdleme31id 40887  cdleme31sc 40877  cdleme31sdnN 40880  cdleme31sn 40873  cdleme31sn1 40874  cdleme31sn1c 40881  cdleme31sn2 40882  cdleme31so 40872  cdleme35a 40941  cdleme35b 40943  cdleme35c 40944  cdleme35d 40945  cdleme35e 40946  cdleme35f 40947  cdleme35fnpq 40942  cdleme35g 40948  cdleme35h 40949  cdleme35h2 40950  cdleme35sn2aw 40951  cdleme35sn3a 40952  cdleme36a 40953  cdleme36m 40954  cdleme37m 40955  cdleme38m 40956  cdleme38n 40957  cdleme39a 40958  cdleme39n 40959  cdleme3b 40722  cdleme3c 40723  cdleme3d 40724  cdleme3e 40725  cdleme3fN 40726  cdleme3fa 40729  cdleme3g 40727  cdleme3h 40728  cdleme4 40731  cdleme40m 40960  cdleme40n 40961  cdleme40v 40962  cdleme40w 40963  cdleme41fva11 40970  cdleme41sn3aw 40967  cdleme41sn4aw 40968  cdleme41snaw 40969  cdleme42a 40964  cdleme42b 40971  cdleme42c 40965  cdleme42d 40966  cdleme42e 40972  cdleme42f 40973  cdleme42g 40974  cdleme42h 40975  cdleme42i 40976  cdleme42k 40977  cdleme42ke 40978  cdleme42keg 40979  cdleme42mN 40980  cdleme42mgN 40981  cdleme43aN 40982  cdleme43bN 40983  cdleme43cN 40984  cdleme43dN 40985  cdleme5 40733  cdleme50ex 41052  cdleme50ltrn 41050  cdleme51finvN 41049  cdleme51finvfvN 41048  cdleme51finvtrN 41051  cdleme6 40734  cdleme7 40742  cdleme7a 40736  cdleme7aa 40735  cdleme7b 40737  cdleme7c 40738  cdleme7d 40739  cdleme7e 40740  cdleme7ga 40741  cdleme8 40743  cdleme8tN 40748  cdleme9 40746  cdleme9a 40744  cdleme9b 40745  cdleme9tN 40750  cdleme9taN 40749  cdlemeda 40791  cdlemedb 40790  cdlemednpq 40792  cdlemednuN 40793  cdlemefr27cl 40896  cdlemefr32fva1 40903  cdlemefr32fvaN 40902  cdlemefrs32fva 40893  cdlemefrs32fva1 40894  cdlemefs27cl 40906  cdlemefs32fva1 40916  cdlemefs32fvaN 40915  cdlemesner 40789  cdlemeulpq 40713
[Crawley] p. 114Lemma E4atex 40569  4atexlem7 40568  cdleme0nex 40783  cdleme17a 40779  cdleme17c 40781  cdleme17d 40991  cdleme17d1 40782  cdleme17d2 40988  cdleme18a 40784  cdleme18b 40785  cdleme18c 40786  cdleme18d 40788  cdleme4a 40732
[Crawley] p. 115Lemma Ecdleme21a 40818  cdleme21at 40821  cdleme21b 40819  cdleme21c 40820  cdleme21ct 40822  cdleme21f 40825  cdleme21g 40826  cdleme21h 40827  cdleme21i 40828  cdleme22gb 40787
[Crawley] p. 116Lemma Fcdlemf 41056  cdlemf1 41054  cdlemf2 41055
[Crawley] p. 116Lemma Gcdlemftr1 41060  cdlemg16 41150  cdlemg28 41197  cdlemg28a 41186  cdlemg28b 41196  cdlemg3a 41090  cdlemg42 41222  cdlemg43 41223  cdlemg44 41226  cdlemg44a 41224  cdlemg46 41228  cdlemg47 41229  cdlemg9 41127  ltrnco 41212  ltrncom 41231  tgrpabl 41244  trlco 41220
[Crawley] p. 116Definition of Gdf-tgrp 41236
[Crawley] p. 117Lemma Gcdlemg17 41170  cdlemg17b 41155
[Crawley] p. 117Definition of Edf-edring-rN 41249  df-edring 41250
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41253
[Crawley] p. 118Remarktendopltp 41273
[Crawley] p. 118Lemma Hcdlemh 41310  cdlemh1 41308  cdlemh2 41309
[Crawley] p. 118Lemma Icdlemi 41313  cdlemi1 41311  cdlemi2 41312
[Crawley] p. 118Lemma Jcdlemj1 41314  cdlemj2 41315  cdlemj3 41316  tendocan 41317
[Crawley] p. 118Lemma Kcdlemk 41467  cdlemk1 41324  cdlemk10 41336  cdlemk11 41342  cdlemk11t 41439  cdlemk11ta 41422  cdlemk11tb 41424  cdlemk11tc 41438  cdlemk11u-2N 41382  cdlemk11u 41364  cdlemk12 41343  cdlemk12u-2N 41383  cdlemk12u 41365  cdlemk13-2N 41369  cdlemk13 41345  cdlemk14-2N 41371  cdlemk14 41347  cdlemk15-2N 41372  cdlemk15 41348  cdlemk16-2N 41373  cdlemk16 41350  cdlemk16a 41349  cdlemk17-2N 41374  cdlemk17 41351  cdlemk18-2N 41379  cdlemk18-3N 41393  cdlemk18 41361  cdlemk19-2N 41380  cdlemk19 41362  cdlemk19u 41463  cdlemk1u 41352  cdlemk2 41325  cdlemk20-2N 41385  cdlemk20 41367  cdlemk21-2N 41384  cdlemk21N 41366  cdlemk22-3 41394  cdlemk22 41386  cdlemk23-3 41395  cdlemk24-3 41396  cdlemk25-3 41397  cdlemk26-3 41399  cdlemk26b-3 41398  cdlemk27-3 41400  cdlemk28-3 41401  cdlemk29-3 41404  cdlemk3 41326  cdlemk30 41387  cdlemk31 41389  cdlemk32 41390  cdlemk33N 41402  cdlemk34 41403  cdlemk35 41405  cdlemk36 41406  cdlemk37 41407  cdlemk38 41408  cdlemk39 41409  cdlemk39u 41461  cdlemk4 41327  cdlemk41 41413  cdlemk42 41434  cdlemk42yN 41437  cdlemk43N 41456  cdlemk45 41440  cdlemk46 41441  cdlemk47 41442  cdlemk48 41443  cdlemk49 41444  cdlemk5 41329  cdlemk50 41445  cdlemk51 41446  cdlemk52 41447  cdlemk53 41450  cdlemk54 41451  cdlemk55 41454  cdlemk55u 41459  cdlemk56 41464  cdlemk5a 41328  cdlemk5auN 41353  cdlemk5u 41354  cdlemk6 41330  cdlemk6u 41355  cdlemk7 41341  cdlemk7u-2N 41381  cdlemk7u 41363  cdlemk8 41331  cdlemk9 41332  cdlemk9bN 41333  cdlemki 41334  cdlemkid 41429  cdlemkj-2N 41375  cdlemkj 41356  cdlemksat 41339  cdlemksel 41338  cdlemksv 41337  cdlemksv2 41340  cdlemkuat 41359  cdlemkuel-2N 41377  cdlemkuel-3 41391  cdlemkuel 41358  cdlemkuv-2N 41376  cdlemkuv2-2 41378  cdlemkuv2-3N 41392  cdlemkuv2 41360  cdlemkuvN 41357  cdlemkvcl 41335  cdlemky 41419  cdlemkyyN 41455  tendoex 41468
[Crawley] p. 120Remarkdva1dim 41478
[Crawley] p. 120Lemma Lcdleml1N 41469  cdleml2N 41470  cdleml3N 41471  cdleml4N 41472  cdleml5N 41473  cdleml6 41474  cdleml7 41475  cdleml8 41476  cdleml9 41477  dia1dim 41554
[Crawley] p. 120Lemma Mdia11N 41541  diaf11N 41542  dialss 41539  diaord 41540  dibf11N 41654  djajN 41630
[Crawley] p. 120Definition of isomorphism mapdiaval 41525
[Crawley] p. 121Lemma Mcdlemm10N 41611  dia2dimlem1 41557  dia2dimlem2 41558  dia2dimlem3 41559  dia2dimlem4 41560  dia2dimlem5 41561  diaf1oN 41623  diarnN 41622  dvheveccl 41605  dvhopN 41609
[Crawley] p. 121Lemma Ncdlemn 41705  cdlemn10 41699  cdlemn11 41704  cdlemn11a 41700  cdlemn11b 41701  cdlemn11c 41702  cdlemn11pre 41703  cdlemn2 41688  cdlemn2a 41689  cdlemn3 41690  cdlemn4 41691  cdlemn4a 41692  cdlemn5 41694  cdlemn5pre 41693  cdlemn6 41695  cdlemn7 41696  cdlemn8 41697  cdlemn9 41698  diclspsn 41687
[Crawley] p. 121Definition of phi(q)df-dic 41666
[Crawley] p. 122Lemma Ndih11 41758  dihf11 41760  dihjust 41710  dihjustlem 41709  dihord 41757  dihord1 41711  dihord10 41716  dihord11b 41715  dihord11c 41717  dihord2 41720  dihord2a 41712  dihord2b 41713  dihord2cN 41714  dihord2pre 41718  dihord2pre2 41719  dihordlem6 41706  dihordlem7 41707  dihordlem7b 41708
[Crawley] p. 122Definition of isomorphism mapdihffval 41723  dihfval 41724  dihval 41725
[Diestel] p. 3Definitiondf-gric 48373  df-grim 48370  isuspgrim 48388
[Diestel] p. 3Section 1.1df-cusgr 29506  df-nbgr 29427
[Diestel] p. 3Definition by df-grisom 48369
[Diestel] p. 4Section 1.1df-isubgr 48353  df-subgr 29362  uhgrspan1 29397  uhgrspansubgr 29385
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29648  vtxdgoddnumeven 29647
[Diestel] p. 27Section 1.10df-ushgr 29153
[EGA] p. 80Notation 1.1.1rspecval 34055
[EGA] p. 80Proposition 1.1.2zartop 34067
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34059  zarcls1 34060
[EGA] p. 81Corollary 1.1.8zart0 34070
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34073
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34076
[Eisenberg] p. 67Definition 5.3df-dif 3893
[Eisenberg] p. 82Definition 6.3dfom3 9566
[Eisenberg] p. 125Definition 8.21df-map 8772
[Eisenberg] p. 216Example 13.2(4)omenps 9574
[Eisenberg] p. 310Theorem 19.8cardprc 9902
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10475
[Enderton] p. 18Axiom of Empty Setaxnul 5234
[Enderton] p. 19Definitiondf-tp 4567
[Enderton] p. 26Exercise 5unissb 4878
[Enderton] p. 26Exercise 10pwel 5317
[Enderton] p. 28Exercise 7(b)pwun 5518
[Enderton] p. 30Theorem "Distributive laws"iinin1 5015  iinin2 5014  iinun2 5009  iunin1 5008  iunin1f 32653  iunin2 5007  uniin1 32647  uniin2 32648
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5013  iundif2 5010
[Enderton] p. 32Exercise 20unineq 4223
[Enderton] p. 33Exercise 23iinuni 5034
[Enderton] p. 33Exercise 25iununi 5035
[Enderton] p. 33Exercise 24(a)iinpw 5042
[Enderton] p. 33Exercise 24(b)iunpw 7721  iunpwss 5043
[Enderton] p. 36Definitionopthwiener 5462
[Enderton] p. 38Exercise 6(a)unipw 5396
[Enderton] p. 38Exercise 6(b)pwuni 4883
[Enderton] p. 41Lemma 3Dopeluu 5417  rnex 7857  rnexg 7849
[Enderton] p. 41Exercise 8dmuni 5863  rnuni 6106
[Enderton] p. 42Definition of a functiondffun7 6519  dffun8 6520
[Enderton] p. 43Definition of function valuefunfv2 6922
[Enderton] p. 43Definition of single-rootedfuncnv 6561
[Enderton] p. 44Definition (d)dfima2 6021  dfima3 6022
[Enderton] p. 47Theorem 3Hfvco2 6931
[Enderton] p. 49Axiom of Choice (first form)ac7 10393  ac7g 10394  df-ac 10036  dfac2 10052  dfac2a 10050  dfac2b 10051  dfac3 10041  dfac7 10053
[Enderton] p. 50Theorem 3K(a)imauni 7197
[Enderton] p. 52Definitiondf-map 8772
[Enderton] p. 53Exercise 21coass 6224
[Enderton] p. 53Exercise 27dmco 6213
[Enderton] p. 53Exercise 14(a)funin 6568
[Enderton] p. 53Exercise 22(a)imass2 6061
[Enderton] p. 54Remarkixpf 8865  ixpssmap 8877
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8843
[Enderton] p. 55Axiom of Choice (second form)ac9 10403  ac9s 10413
[Enderton] p. 56Theorem 3Meqvrelref 39062  erref 8661
[Enderton] p. 57Lemma 3Neqvrelthi 39065  erthi 8697
[Enderton] p. 57Definitiondf-ec 8642
[Enderton] p. 58Definitiondf-qs 8646
[Enderton] p. 61Exercise 35df-ec 8642
[Enderton] p. 65Exercise 56(a)dmun 5859
[Enderton] p. 68Definition of successordf-suc 6323
[Enderton] p. 71Definitiondf-tr 5187  dftr4 5192
[Enderton] p. 72Theorem 4Eunisuc 6398  unisucg 6397
[Enderton] p. 73Exercise 6unisuc 6398  unisucg 6397
[Enderton] p. 73Exercise 5(a)truni 5202
[Enderton] p. 73Exercise 5(b)trint 5204  trintALT 45325
[Enderton] p. 79Theorem 4I(A1)nna0 8537
[Enderton] p. 79Theorem 4I(A2)nnasuc 8539  onasuc 8460
[Enderton] p. 79Definition of operation valuedf-ov 7366
[Enderton] p. 80Theorem 4J(A1)nnm0 8538
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8540  onmsuc 8461
[Enderton] p. 81Theorem 4K(1)nnaass 8555
[Enderton] p. 81Theorem 4K(2)nna0r 8542  nnacom 8550
[Enderton] p. 81Theorem 4K(3)nndi 8556
[Enderton] p. 81Theorem 4K(4)nnmass 8557
[Enderton] p. 81Theorem 4K(5)nnmcom 8559
[Enderton] p. 82Exercise 16nnm0r 8543  nnmsucr 8558
[Enderton] p. 88Exercise 23nnaordex 8571
[Enderton] p. 129Definitiondf-en 8891
[Enderton] p. 132Theorem 6B(b)canth 7317
[Enderton] p. 133Exercise 1xpomen 9935
[Enderton] p. 133Exercise 2qnnen 16178
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9138
[Enderton] p. 135Corollary 6Cphp3 9140
[Enderton] p. 136Corollary 6Enneneq 9137
[Enderton] p. 136Corollary 6D(a)pssinf 9169
[Enderton] p. 136Corollary 6D(b)ominf 9171
[Enderton] p. 137Lemma 6Fpssnn 9100
[Enderton] p. 138Corollary 6Gssfi 9104
[Enderton] p. 139Theorem 6H(c)mapen 9076
[Enderton] p. 142Theorem 6I(3)xpdjuen 10100
[Enderton] p. 142Theorem 6I(4)mapdjuen 10101
[Enderton] p. 143Theorem 6Jdju0en 10096  dju1en 10092
[Enderton] p. 144Exercise 13iunfi 9250  unifi 9251  unifi2 9252
[Enderton] p. 144Corollary 6Kundif2 4412  unfi 9102  unfi2 9217
[Enderton] p. 145Figure 38ffoss 7895
[Enderton] p. 145Definitiondf-dom 8892
[Enderton] p. 146Example 1domen 8905  domeng 8906
[Enderton] p. 146Example 3nndomo 9149  nnsdom 9573  nnsdomg 9206
[Enderton] p. 149Theorem 6L(a)djudom2 10104
[Enderton] p. 149Theorem 6L(c)mapdom1 9077  xpdom1 9011  xpdom1g 9009  xpdom2g 9008
[Enderton] p. 149Theorem 6L(d)mapdom2 9083
[Enderton] p. 151Theorem 6Mzorn 10427  zorng 10424
[Enderton] p. 151Theorem 6M(4)ac8 10412  dfac5 10049
[Enderton] p. 159Theorem 6Qunictb 10496
[Enderton] p. 164Exampleinfdif 10128
[Enderton] p. 168Definitiondf-po 5533
[Enderton] p. 192Theorem 7M(a)oneli 6432
[Enderton] p. 192Theorem 7M(b)ontr1 6364
[Enderton] p. 192Theorem 7M(c)onirri 6431
[Enderton] p. 193Corollary 7N(b)0elon 6372
[Enderton] p. 193Corollary 7N(c)onsuci 7786
[Enderton] p. 193Corollary 7N(d)ssonunii 7731
[Enderton] p. 194Remarkonprc 7728
[Enderton] p. 194Exercise 16suc11 6426
[Enderton] p. 197Definitiondf-card 9861
[Enderton] p. 197Theorem 7Pcarden 10471
[Enderton] p. 200Exercise 25tfis 7802
[Enderton] p. 202Lemma 7Tr1tr 9698
[Enderton] p. 202Definitiondf-r1 9686
[Enderton] p. 202Theorem 7Qr1val1 9708
[Enderton] p. 204Theorem 7V(b)rankval4 9789  rankval4b 35290
[Enderton] p. 206Theorem 7X(b)en2lp 9525
[Enderton] p. 207Exercise 30rankpr 9779  rankprb 9773  rankpw 9765  rankpwi 9745  rankuniss 9788
[Enderton] p. 207Exercise 34opthreg 9537
[Enderton] p. 208Exercise 35suc11reg 9538
[Enderton] p. 212Definition of alephalephval3 10030
[Enderton] p. 213Theorem 8A(a)alephord2 9996
[Enderton] p. 213Theorem 8A(b)cardalephex 10010
[Enderton] p. 218Theorem Schema 8Eonfununi 8278
[Enderton] p. 222Definition of kardkarden 9817  kardex 9816
[Enderton] p. 238Theorem 8Roeoa 8530
[Enderton] p. 238Theorem 8Soeoe 8532
[Enderton] p. 240Exercise 25oarec 8494
[Enderton] p. 257Definition of cofinalitycflm 10170
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17606
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17548
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18517  mrieqv2d 17603  mrieqvd 17602
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17607
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17612  mreexexlem2d 17609
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18523  mreexfidimd 17614
[Frege1879] p. 11Statementdf3or2 44213
[Frege1879] p. 12Statementdf3an2 44214  dfxor4 44211  dfxor5 44212
[Frege1879] p. 26Axiom 1ax-frege1 44235
[Frege1879] p. 26Axiom 2ax-frege2 44236
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44240
[Frege1879] p. 31Proposition 4frege4 44244
[Frege1879] p. 32Proposition 5frege5 44245
[Frege1879] p. 33Proposition 6frege6 44251
[Frege1879] p. 34Proposition 7frege7 44253
[Frege1879] p. 35Axiom 8ax-frege8 44254  axfrege8 44252
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37808
[Frege1879] p. 35Proposition 9frege9 44257
[Frege1879] p. 36Proposition 10frege10 44265
[Frege1879] p. 36Proposition 11frege11 44259
[Frege1879] p. 37Proposition 12frege12 44258
[Frege1879] p. 37Proposition 13frege13 44267
[Frege1879] p. 37Proposition 14frege14 44268
[Frege1879] p. 38Proposition 15frege15 44271
[Frege1879] p. 38Proposition 16frege16 44261
[Frege1879] p. 39Proposition 17frege17 44266
[Frege1879] p. 39Proposition 18frege18 44263
[Frege1879] p. 39Proposition 19frege19 44269
[Frege1879] p. 40Proposition 20frege20 44273
[Frege1879] p. 40Proposition 21frege21 44272
[Frege1879] p. 41Proposition 22frege22 44264
[Frege1879] p. 42Proposition 23frege23 44270
[Frege1879] p. 42Proposition 24frege24 44260
[Frege1879] p. 42Proposition 25frege25 44262  rp-frege25 44250
[Frege1879] p. 42Proposition 26frege26 44255
[Frege1879] p. 43Axiom 28ax-frege28 44275
[Frege1879] p. 43Proposition 27frege27 44256
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 44276
[Frege1879] p. 44Axiom 31ax-frege31 44279  axfrege31 44278
[Frege1879] p. 44Proposition 30frege30 44277
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 44280
[Frege1879] p. 44Proposition 33frege33 44281
[Frege1879] p. 45Proposition 34frege34 44282
[Frege1879] p. 45Proposition 35frege35 44283
[Frege1879] p. 45Proposition 36frege36 44284
[Frege1879] p. 46Proposition 37frege37 44285
[Frege1879] p. 46Proposition 38frege38 44286
[Frege1879] p. 46Proposition 39frege39 44287
[Frege1879] p. 46Proposition 40frege40 44288
[Frege1879] p. 47Axiom 41ax-frege41 44290  axfrege41 44289
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 44291
[Frege1879] p. 47Proposition 43frege43 44292
[Frege1879] p. 47Proposition 44frege44 44293
[Frege1879] p. 47Proposition 45frege45 44294
[Frege1879] p. 48Proposition 46frege46 44295
[Frege1879] p. 48Proposition 47frege47 44296
[Frege1879] p. 49Proposition 48frege48 44297
[Frege1879] p. 49Proposition 49frege49 44298
[Frege1879] p. 49Proposition 50frege50 44299
[Frege1879] p. 50Axiom 52ax-frege52a 44302  ax-frege52c 44333  frege52aid 44303  frege52b 44334
[Frege1879] p. 50Axiom 54ax-frege54a 44307  ax-frege54c 44337  frege54b 44338
[Frege1879] p. 50Proposition 51frege51 44300
[Frege1879] p. 50Proposition 52dfsbcq 3732
[Frege1879] p. 50Proposition 53frege53a 44305  frege53aid 44304  frege53b 44335  frege53c 44359
[Frege1879] p. 50Proposition 54biid 262  eqid 2740
[Frege1879] p. 50Proposition 55frege55a 44313  frege55aid 44310  frege55b 44342  frege55c 44363  frege55cor1a 44314  frege55lem2a 44312  frege55lem2b 44341  frege55lem2c 44362
[Frege1879] p. 50Proposition 56frege56a 44316  frege56aid 44315  frege56b 44343  frege56c 44364
[Frege1879] p. 51Axiom 58ax-frege58a 44320  ax-frege58b 44346  frege58bid 44347  frege58c 44366
[Frege1879] p. 51Proposition 57frege57a 44318  frege57aid 44317  frege57b 44344  frege57c 44365
[Frege1879] p. 51Proposition 58spsbc 3743
[Frege1879] p. 51Proposition 59frege59a 44322  frege59b 44349  frege59c 44367
[Frege1879] p. 52Proposition 60frege60a 44323  frege60b 44350  frege60c 44368
[Frege1879] p. 52Proposition 61frege61a 44324  frege61b 44351  frege61c 44369
[Frege1879] p. 52Proposition 62frege62a 44325  frege62b 44352  frege62c 44370
[Frege1879] p. 52Proposition 63frege63a 44326  frege63b 44353  frege63c 44371
[Frege1879] p. 53Proposition 64frege64a 44327  frege64b 44354  frege64c 44372
[Frege1879] p. 53Proposition 65frege65a 44328  frege65b 44355  frege65c 44373
[Frege1879] p. 54Proposition 66frege66a 44329  frege66b 44356  frege66c 44374
[Frege1879] p. 54Proposition 67frege67a 44330  frege67b 44357  frege67c 44375
[Frege1879] p. 54Proposition 68frege68a 44331  frege68b 44358  frege68c 44376
[Frege1879] p. 55Definition 69dffrege69 44377
[Frege1879] p. 58Proposition 70frege70 44378
[Frege1879] p. 59Proposition 71frege71 44379
[Frege1879] p. 59Proposition 72frege72 44380
[Frege1879] p. 59Proposition 73frege73 44381
[Frege1879] p. 60Definition 76dffrege76 44384
[Frege1879] p. 60Proposition 74frege74 44382
[Frege1879] p. 60Proposition 75frege75 44383
[Frege1879] p. 62Proposition 77frege77 44385  frege77d 44191
[Frege1879] p. 63Proposition 78frege78 44386
[Frege1879] p. 63Proposition 79frege79 44387
[Frege1879] p. 63Proposition 80frege80 44388
[Frege1879] p. 63Proposition 81frege81 44389  frege81d 44192
[Frege1879] p. 64Proposition 82frege82 44390
[Frege1879] p. 65Proposition 83frege83 44391  frege83d 44193
[Frege1879] p. 65Proposition 84frege84 44392
[Frege1879] p. 66Proposition 85frege85 44393
[Frege1879] p. 66Proposition 86frege86 44394
[Frege1879] p. 66Proposition 87frege87 44395  frege87d 44195
[Frege1879] p. 67Proposition 88frege88 44396
[Frege1879] p. 68Proposition 89frege89 44397
[Frege1879] p. 68Proposition 90frege90 44398
[Frege1879] p. 68Proposition 91frege91 44399  frege91d 44196
[Frege1879] p. 69Proposition 92frege92 44400
[Frege1879] p. 70Proposition 93frege93 44401
[Frege1879] p. 70Proposition 94frege94 44402
[Frege1879] p. 70Proposition 95frege95 44403
[Frege1879] p. 71Definition 99dffrege99 44407
[Frege1879] p. 71Proposition 96frege96 44404  frege96d 44194
[Frege1879] p. 71Proposition 97frege97 44405  frege97d 44197
[Frege1879] p. 71Proposition 98frege98 44406  frege98d 44198
[Frege1879] p. 72Proposition 100frege100 44408
[Frege1879] p. 72Proposition 101frege101 44409
[Frege1879] p. 72Proposition 102frege102 44410  frege102d 44199
[Frege1879] p. 73Proposition 103frege103 44411
[Frege1879] p. 73Proposition 104frege104 44412
[Frege1879] p. 73Proposition 105frege105 44413
[Frege1879] p. 73Proposition 106frege106 44414  frege106d 44200
[Frege1879] p. 74Proposition 107frege107 44415
[Frege1879] p. 74Proposition 108frege108 44416  frege108d 44201
[Frege1879] p. 74Proposition 109frege109 44417  frege109d 44202
[Frege1879] p. 75Proposition 110frege110 44418
[Frege1879] p. 75Proposition 111frege111 44419  frege111d 44204
[Frege1879] p. 76Proposition 112frege112 44420
[Frege1879] p. 76Proposition 113frege113 44421
[Frege1879] p. 76Proposition 114frege114 44422  frege114d 44203
[Frege1879] p. 77Definition 115dffrege115 44423
[Frege1879] p. 77Proposition 116frege116 44424
[Frege1879] p. 78Proposition 117frege117 44425
[Frege1879] p. 78Proposition 118frege118 44426
[Frege1879] p. 78Proposition 119frege119 44427
[Frege1879] p. 78Proposition 120frege120 44428
[Frege1879] p. 79Proposition 121frege121 44429
[Frege1879] p. 79Proposition 122frege122 44430  frege122d 44205
[Frege1879] p. 79Proposition 123frege123 44431
[Frege1879] p. 80Proposition 124frege124 44432  frege124d 44206
[Frege1879] p. 81Proposition 125frege125 44433
[Frege1879] p. 81Proposition 126frege126 44434  frege126d 44207
[Frege1879] p. 82Proposition 127frege127 44435
[Frege1879] p. 83Proposition 128frege128 44436
[Frege1879] p. 83Proposition 129frege129 44437  frege129d 44208
[Frege1879] p. 84Proposition 130frege130 44438
[Frege1879] p. 85Proposition 131frege131 44439  frege131d 44209
[Frege1879] p. 86Proposition 132frege132 44440
[Frege1879] p. 86Proposition 133frege133 44441  frege133d 44210
[Fremlin1] p. 13Definition 111G (b)df-salgen 46757
[Fremlin1] p. 13Definition 111G (d)borelmbl 47080
[Fremlin1] p. 13Proposition 111G (b)salgenss 46780
[Fremlin1] p. 14Definition 112Aismea 46895
[Fremlin1] p. 15Remark 112B (d)psmeasure 46915
[Fremlin1] p. 15Property 112C (a)meadjun 46906  meadjunre 46920
[Fremlin1] p. 15Property 112C (b)meassle 46907
[Fremlin1] p. 15Property 112C (c)meaunle 46908
[Fremlin1] p. 16Property 112C (d)iundjiun 46904  meaiunle 46913  meaiunlelem 46912
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46925  meaiuninc2 46926  meaiuninc3 46929  meaiuninc3v 46928  meaiunincf 46927  meaiuninclem 46924
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46931  meaiininc2 46932  meaiininclem 46930
[Fremlin1] p. 19Theorem 113Ccaragen0 46950  caragendifcl 46958  caratheodory 46972  omelesplit 46962
[Fremlin1] p. 19Definition 113Aisome 46938  isomennd 46975  isomenndlem 46974
[Fremlin1] p. 19Remark 113B (c)omeunle 46960
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46979  voncmpl 47065
[Fremlin1] p. 19Definition 113A (ii)omessle 46942
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46967  carageniuncllem1 46965  carageniuncllem2 46966  caragenuncl 46957  caragenuncllem 46956  caragenunicl 46968
[Fremlin1] p. 21Remark 113Dcaragenel2d 46976
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46970  caratheodorylem2 46971
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46979
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47038  hoidmv1lelem1 47035  hoidmv1lelem2 47036  hoidmv1lelem3 47037
[Fremlin1] p. 25Definition 114Eisvonmbl 47082
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47038  hoidmvle 47044  hoidmvlelem1 47039  hoidmvlelem2 47040  hoidmvlelem3 47041  hoidmvlelem4 47042  hoidmvlelem5 47043  hsphoidmvle2 47029  hsphoif 47020  hsphoival 47023
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46992
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47000
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47027  hoidmvn0val 47028  hoidmvval 47021  hoidmvval0 47031  hoidmvval0b 47034
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47032  hsphoidmvle 47030
[Fremlin1] p. 30Definition 115Cdf-ovoln 46981  df-voln 46983
[Fremlin1] p. 30Proposition 115D (a)dmovn 47048  ovn0 47010  ovn0lem 47009  ovnf 47007  ovnome 47017  ovnssle 47005  ovnsslelem 47004  ovnsupge0 47001
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47047  ovnhoilem1 47045  ovnhoilem2 47046  vonhoi 47111
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47064  hoidifhspf 47062  hoidifhspval 47052  hoidifhspval2 47059  hoidifhspval3 47063  hspmbl 47073  hspmbllem1 47070  hspmbllem2 47071  hspmbllem3 47072
[Fremlin1] p. 31Definition 115Evoncmpl 47065  vonmea 47018
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47016  ovnsubadd2 47090  ovnsubadd2lem 47089  ovnsubaddlem1 47014  ovnsubaddlem2 47015
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47075  hoimbl2 47109  hoimbllem 47074  hspdifhsp 47060  opnvonmbl 47078  opnvonmbllem2 47077
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47080
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47123  iccvonmbllem 47122  ioovonmbl 47121
[Fremlin1] p. 32Proposition 115G (d)vonicc 47129  vonicclem2 47128  vonioo 47126  vonioolem2 47125  vonn0icc 47132  vonn0icc2 47136  vonn0ioo 47131  vonn0ioo2 47134
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47133  snvonmbl 47130  vonct 47137  vonsn 47135
[Fremlin1] p. 35Lemma 121Asubsalsal 46803
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46802  subsaliuncllem 46801
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47169  salpreimalegt 47153  salpreimaltle 47170
[Fremlin1] p. 35Proposition 121B (i)issmf 47172  issmff 47178  issmflem 47171
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47189  issmflelem 47188  smfpreimale 47198
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47200  issmfgtlem 47199
[Fremlin1] p. 36Definition 121Cdf-smblfn 47140  issmf 47172  issmff 47178  issmfge 47214  issmfgelem 47213  issmfgt 47200  issmfgtlem 47199  issmfle 47189  issmflelem 47188  issmflem 47171
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47151  salpreimagtlt 47174  salpreimalelt 47173
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47214  issmfgelem 47213
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47197
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47195  cnfsmf 47184
[Fremlin1] p. 36Proposition 121D (c)decsmf 47211  decsmflem 47210  incsmf 47186  incsmflem 47185
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47145  pimconstlt1 47146  smfconst 47193
[Fremlin1] p. 37Proposition 121E (b)smfadd 47209  smfaddlem1 47207  smfaddlem2 47208
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47240
[Fremlin1] p. 37Proposition 121E (d)smfmul 47239  smfmullem1 47235  smfmullem2 47236  smfmullem3 47237  smfmullem4 47238
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47241
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47244  smfpimbor1lem2 47243
[Fremlin1] p. 37Proposition 121E (g)smfco 47246
[Fremlin1] p. 37Proposition 121E (h)smfres 47234
[Fremlin1] p. 38Proposition 121E (e)smfrec 47233
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47242  smfresal 47232
[Fremlin1] p. 38Proposition 121F (a)smflim 47221  smflim2 47250  smflimlem1 47215  smflimlem2 47216  smflimlem3 47217  smflimlem4 47218  smflimlem5 47219  smflimlem6 47220  smflimmpt 47254
[Fremlin1] p. 38Proposition 121F (b)smfsup 47258  smfsuplem1 47255  smfsuplem2 47256  smfsuplem3 47257  smfsupmpt 47259  smfsupxr 47260
[Fremlin1] p. 38Proposition 121F (c)smfinf 47262  smfinflem 47261  smfinfmpt 47263
[Fremlin1] p. 39Remark 121Gsmflim 47221  smflim2 47250  smflimmpt 47254
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47252
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47282  smfdivdmmbl2 47285  smfinfdmmbl 47293  smfinfdmmbllem 47292  smfsupdmmbl 47289  smfsupdmmbllem 47288
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47272  smflimsuplem2 47265  smflimsuplem6 47269  smflimsuplem7 47270  smflimsuplem8 47271  smflimsupmpt 47273
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47275  smfliminflem 47274  smfliminfmpt 47276
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47140
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47286  fsupdm2 47287
[Fremlin1], p. 39Proposition 121Hadddmmbl 47277  adddmmbl2 47278  finfdm 47290  finfdm2 47291  fsupdm 47286  fsupdm2 47287  muldmmbl 47279  muldmmbl2 47280
[Fremlin1], p. 39Proposition 121F (c)finfdm 47290  finfdm2 47291
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25528
[Fremlin5] p. 213Lemma 565Cauniioovol 25571
[Fremlin5] p. 214Lemma 565Cauniioombl 25581
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38066
[Fremlin5] p. 220Theorem 565Maftc1anc 38069
[FreydScedrov] p. 283Axiom of Infinityax-inf 9557  inf1 9541  inf2 9542
[Gleason] p. 117Proposition 9-2.1df-enq 10832  enqer 10842
[Gleason] p. 117Proposition 9-2.2df-1nq 10837  df-nq 10833
[Gleason] p. 117Proposition 9-2.3df-plpq 10829  df-plq 10835
[Gleason] p. 119Proposition 9-2.4caovmo 7600  df-mpq 10830  df-mq 10836
[Gleason] p. 119Proposition 9-2.5df-rq 10838
[Gleason] p. 119Proposition 9-2.6ltexnq 10896
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10897  ltbtwnnq 10899
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10892
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10893
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10900
[Gleason] p. 121Definition 9-3.1df-np 10902
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10914
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10916
[Gleason] p. 122Definitiondf-1p 10903
[Gleason] p. 122Remark (1)prub 10915
[Gleason] p. 122Lemma 9-3.4prlem934 10954
[Gleason] p. 122Proposition 9-3.2df-ltp 10906
[Gleason] p. 122Proposition 9-3.3ltsopr 10953  psslinpr 10952  supexpr 10975  suplem1pr 10973  suplem2pr 10974
[Gleason] p. 123Proposition 9-3.5addclpr 10939  addclprlem1 10937  addclprlem2 10938  df-plp 10904
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10943
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10942
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10955
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10964  ltexprlem1 10957  ltexprlem2 10958  ltexprlem3 10959  ltexprlem4 10960  ltexprlem5 10961  ltexprlem6 10962  ltexprlem7 10963
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10966  ltaprlem 10965
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10967
[Gleason] p. 124Lemma 9-3.6prlem936 10968
[Gleason] p. 124Proposition 9-3.7df-mp 10905  mulclpr 10941  mulclprlem 10940  reclem2pr 10969
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10950
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10945
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10944
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10949
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10972  reclem3pr 10970  reclem4pr 10971
[Gleason] p. 126Proposition 9-4.1df-enr 10976  enrer 10984
[Gleason] p. 126Proposition 9-4.2df-0r 10981  df-1r 10982  df-nr 10977
[Gleason] p. 126Proposition 9-4.3df-mr 10979  df-plr 10978  negexsr 11023  recexsr 11028  recexsrlem 11024
[Gleason] p. 127Proposition 9-4.4df-ltr 10980
[Gleason] p. 130Proposition 10-1.3creui 12152  creur 12151  cru 12149
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11109  axcnre 11085
[Gleason] p. 132Definition 10-3.1crim 15075  crimd 15192  crimi 15153  crre 15074  crred 15191  crrei 15152
[Gleason] p. 132Definition 10-3.2remim 15077  remimd 15158
[Gleason] p. 133Definition 10.36absval2 15244  absval2d 15408  absval2i 15358
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15101  cjaddd 15180  cjaddi 15148
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15102  cjmuld 15181  cjmuli 15149
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15100  cjcjd 15159  cjcji 15131
[Gleason] p. 133Proposition 10-3.4(f)cjre 15099  cjreb 15083  cjrebd 15162  cjrebi 15134  cjred 15186  rere 15082  rereb 15080  rerebd 15161  rerebi 15133  rered 15184
[Gleason] p. 133Proposition 10-3.4(h)addcj 15108  addcjd 15172  addcji 15143
[Gleason] p. 133Proposition 10-3.7(a)absval 15198
[Gleason] p. 133Proposition 10-3.7(b)abscj 15239  abscjd 15413  abscji 15362
[Gleason] p. 133Proposition 10-3.7(c)abs00 15249  abs00d 15409  abs00i 15359  absne0d 15410
[Gleason] p. 133Proposition 10-3.7(d)releabs 15282  releabsd 15414  releabsi 15363
[Gleason] p. 133Proposition 10-3.7(f)absmul 15254  absmuld 15417  absmuli 15365
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15242  sqabsaddi 15366
[Gleason] p. 133Proposition 10-3.7(h)abstri 15291  abstrid 15419  abstrii 15369
[Gleason] p. 134Definition 10-4.1df-exp 14022  exp0 14025  expp1 14028  expp1d 14107
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26668  cxpaddd 26706  expadd 14064  expaddd 14108  expaddz 14066
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26677  cxpmuld 26726  expmul 14067  expmuld 14109  expmulz 14068
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26674  mulcxpd 26717  mulexp 14061  mulexpd 14121  mulexpz 14062
[Gleason] p. 140Exercise 1znnen 16177
[Gleason] p. 141Definition 11-2.1fzval 13461
[Gleason] p. 168Proposition 12-2.1(a)climadd 15592  rlimadd 15603  rlimdiv 15606
[Gleason] p. 168Proposition 12-2.1(b)climsub 15594  rlimsub 15604
[Gleason] p. 168Proposition 12-2.1(c)climmul 15593  rlimmul 15605
[Gleason] p. 171Corollary 12-2.2climmulc2 15597
[Gleason] p. 172Corollary 12-2.5climrecl 15543
[Gleason] p. 172Proposition 12-2.4(c)climabs 15564  climcj 15565  climim 15567  climre 15566  rlimabs 15569  rlimcj 15570  rlimim 15572  rlimre 15571
[Gleason] p. 173Definition 12-3.1df-ltxr 11182  df-xr 11181  ltxr 13064
[Gleason] p. 175Definition 12-4.1df-limsup 15431  limsupval 15434
[Gleason] p. 180Theorem 12-5.1climsup 15630
[Gleason] p. 180Theorem 12-5.3caucvg 15639  caucvgb 15640  caucvgbf 45933  caucvgr 15636  climcau 15631
[Gleason] p. 182Exercise 3cvgcmp 15777
[Gleason] p. 182Exercise 4cvgrat 15846
[Gleason] p. 195Theorem 13-2.12abs1m 15296
[Gleason] p. 217Lemma 13-4.1btwnzge0 13785
[Gleason] p. 223Definition 14-1.1df-met 21348
[Gleason] p. 223Definition 14-1.1(a)met0 24333  xmet0 24332
[Gleason] p. 223Definition 14-1.1(b)metgt0 24349
[Gleason] p. 223Definition 14-1.1(c)metsym 24340
[Gleason] p. 223Definition 14-1.1(d)mettri 24342  mstri 24459  xmettri 24341  xmstri 24458
[Gleason] p. 225Definition 14-1.5xpsmet 24372
[Gleason] p. 230Proposition 14-2.6txlm 23638
[Gleason] p. 240Theorem 14-4.3metcnp4 25302
[Gleason] p. 240Proposition 14-4.2metcnp3 24530
[Gleason] p. 243Proposition 14-4.16addcn 24856  addcn2 15554  mulcn 24858  mulcn2 15556  subcn 24857  subcn2 15555
[Gleason] p. 295Remarkbcval3 14266  bcval4 14267
[Gleason] p. 295Equation 2bcpasc 14281
[Gleason] p. 295Definition of binomial coefficientbcval 14264  df-bc 14263
[Gleason] p. 296Remarkbcn0 14270  bcnn 14272
[Gleason] p. 296Theorem 15-2.8binom 15793
[Gleason] p. 308Equation 2ef0 16054
[Gleason] p. 308Equation 3efcj 16055
[Gleason] p. 309Corollary 15-4.3efne0 16061
[Gleason] p. 309Corollary 15-4.4efexp 16066
[Gleason] p. 310Equation 14sinadd 16129
[Gleason] p. 310Equation 15cosadd 16130
[Gleason] p. 311Equation 17sincossq 16141
[Gleason] p. 311Equation 18cosbnd 16146  sinbnd 16145
[Gleason] p. 311Lemma 15-4.7sqeqor 14176  sqeqori 14174
[Gleason] p. 311Definition of ` `df-pi 16035
[Godowski] p. 730Equation SFgoeqi 32369
[GodowskiGreechie] p. 249Equation IV3oai 31764
[Golan] p. 1Remarksrgisid 20188
[Golan] p. 1Definitiondf-srg 20166
[Golan] p. 149Definitiondf-slmd 33289
[Gonshor] p. 7Definitiondf-cuts 27777
[Gonshor] p. 9Theorem 2.5lesrec 27816  lesrecd 27817
[Gonshor] p. 10Theorem 2.6cofcut1 27937  cofcut1d 27938
[Gonshor] p. 10Theorem 2.7cofcut2 27939  cofcut2d 27940
[Gonshor] p. 12Theorem 2.9cofcutr 27941  cofcutr1d 27942  cofcutr2d 27943
[Gonshor] p. 13Definitiondf-adds 27977
[Gonshor] p. 14Theorem 3.1addsprop 27993
[Gonshor] p. 15Theorem 3.2addsunif 28019
[Gonshor] p. 17Theorem 3.4mulsprop 28147
[Gonshor] p. 18Theorem 3.5mulsunif 28167
[Gonshor] p. 28Lemma 4.2halfcut 28475
[Gonshor] p. 28Theorem 4.2pw2cut 28477
[Gonshor] p. 30Theorem 4.2addhalfcut 28476
[Gonshor] p. 39Theorem 4.4(b)elreno2 28512
[Gonshor] p. 95Theorem 6.1addbday 28035
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36388
[Gratzer] p. 23Section 0.6df-mre 17546
[Gratzer] p. 27Section 0.6df-mri 17548
[Hall] p. 1Section 1.1df-asslaw 48680  df-cllaw 48678  df-comlaw 48679
[Hall] p. 2Section 1.2df-clintop 48692
[Hall] p. 7Section 1.3df-sgrp2 48713
[Halmos] p. 28Partition ` `df-parts 39236  dfmembpart2 39241
[Halmos] p. 31Theorem 17.3riesz1 32161  riesz2 32162
[Halmos] p. 41Definition of Hermitianhmopadj2 32037
[Halmos] p. 42Definition of projector orderingpjordi 32269
[Halmos] p. 43Theorem 26.1elpjhmop 32281  elpjidm 32280  pjnmopi 32244
[Halmos] p. 44Remarkpjinormi 31783  pjinormii 31772
[Halmos] p. 44Theorem 26.2elpjch 32285  pjrn 31803  pjrni 31798  pjvec 31792
[Halmos] p. 44Theorem 26.3pjnorm2 31823
[Halmos] p. 44Theorem 26.4hmopidmpj 32250  hmopidmpji 32248
[Halmos] p. 45Theorem 27.1pjinvari 32287
[Halmos] p. 45Theorem 27.3pjoci 32276  pjocvec 31793
[Halmos] p. 45Theorem 27.4pjorthcoi 32265
[Halmos] p. 48Theorem 29.2pjssposi 32268
[Halmos] p. 48Theorem 29.3pjssdif1i 32271  pjssdif2i 32270
[Halmos] p. 50Definition of spectrumdf-spec 31951
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1802
[Hatcher] p. 25Definitiondf-phtpc 24984  df-phtpy 24963
[Hatcher] p. 26Definitiondf-pco 24997  df-pi1 25000
[Hatcher] p. 26Proposition 1.2phtpcer 24987
[Hatcher] p. 26Proposition 1.3pi1grp 25042
[Hefferon] p. 240Definition 3.12df-dmat 22480  df-dmatalt 48890
[Helfgott] p. 2Theoremtgoldbach 48309
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48294
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48306  bgoldbtbnd 48301  bgoldbtbnd 48301  tgblthelfgott 48307
[Helfgott] p. 5Proposition 1.1circlevma 34833
[Helfgott] p. 69Statement 7.49circlemethhgt 34834
[Helfgott] p. 69Statement 7.50hgt750lema 34848  hgt750lemb 34847  hgt750leme 34849  hgt750lemf 34844  hgt750lemg 34845
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48303  tgoldbachgt 34854  tgoldbachgtALTV 48304  tgoldbachgtd 34853
[Helfgott] p. 70Statement 7.49ax-hgt749 34835
[Herstein] p. 54Exercise 28df-grpo 30589
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18918  grpoideu 30605  mndideu 18711
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18948  grpoinveu 30615
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18979  grpo2inv 30627
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18992  grpoinvop 30629
[Herstein] p. 57Exercise 1dfgrp3e 19014
[Hitchcock] p. 5Rule A3mptnan 1775
[Hitchcock] p. 5Rule A4mptxor 1776
[Hitchcock] p. 5Rule A5mtpxor 1778
[Holland] p. 1519Theorem 2sumdmdi 32516
[Holland] p. 1520Lemma 5cdj1i 32529  cdj3i 32537  cdj3lem1 32530  cdjreui 32528
[Holland] p. 1524Lemma 7mddmdin0i 32527
[Holland95] p. 13Theorem 3.6hlathil 42454
[Holland95] p. 14Line 15hgmapvs 42384
[Holland95] p. 14Line 16hdmaplkr 42406
[Holland95] p. 14Line 17hdmapellkr 42407
[Holland95] p. 14Line 19hdmapglnm2 42404
[Holland95] p. 14Line 20hdmapip0com 42410
[Holland95] p. 14Theorem 3.6hdmapevec2 42329
[Holland95] p. 14Lines 24 and 25hdmapoc 42424
[Holland95] p. 204Definition of involutiondf-srng 20819
[Holland95] p. 212Definition of subspacedf-psubsp 39996
[Holland95] p. 214Lemma 3.3lclkrlem2v 42021
[Holland95] p. 214Definition 3.2df-lpolN 41974
[Holland95] p. 214Definition of nonsingularpnonsingN 40426
[Holland95] p. 215Lemma 3.3(1)dihoml4 41870  poml4N 40446
[Holland95] p. 215Lemma 3.3(2)dochexmid 41961  pexmidALTN 40471  pexmidN 40462
[Holland95] p. 218Theorem 3.6lclkr 42026
[Holland95] p. 218Definition of dual vector spacedf-ldual 39617  ldualset 39618
[Holland95] p. 222Item 1df-lines 39994  df-pointsN 39995
[Holland95] p. 222Item 2df-polarityN 40396
[Holland95] p. 223Remarkispsubcl2N 40440  omllaw4 39739  pol1N 40403  polcon3N 40410
[Holland95] p. 223Definitiondf-psubclN 40428
[Holland95] p. 223Equation for polaritypolval2N 40399
[Holmes] p. 40Definitiondf-xrn 38748
[Hughes] p. 44Equation 1.21bax-his3 31180
[Hughes] p. 47Definition of projection operatordfpjop 32278
[Hughes] p. 49Equation 1.30eighmre 32059  eigre 31931  eigrei 31930
[Hughes] p. 49Equation 1.31eighmorth 32060  eigorth 31934  eigorthi 31933
[Hughes] p. 137Remark (ii)eigposi 31932
[Huneke] p. 1Claim 1frgrncvvdeq 30404
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30400
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30401
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30402
[Huneke] p. 2Claim 2frgrregorufr 30420  frgrregorufr0 30419  frgrregorufrg 30421
[Huneke] p. 2Claim 3frgrhash2wsp 30427  frrusgrord 30436  frrusgrord0 30435
[Huneke] p. 2Statementdf-clwwlknon 30183
[Huneke] p. 2Statement 4frgrwopreglem4 30410
[Huneke] p. 2Statement 5frgrwopreg1 30413  frgrwopreg2 30414  frgrwopregasn 30411  frgrwopregbsn 30412
[Huneke] p. 2Statement 6frgrwopreglem5 30416
[Huneke] p. 2Statement 7fusgreghash2wspv 30430
[Huneke] p. 2Statement 8fusgreghash2wsp 30433
[Huneke] p. 2Statement 9clwlksndivn 30181  numclwlk1 30466  numclwlk1lem1 30464  numclwlk1lem2 30465  numclwwlk1 30456  numclwwlk8 30487
[Huneke] p. 2Definition 3frgrwopreglem1 30407
[Huneke] p. 2Definition 4df-clwlks 29864
[Huneke] p. 2Definition 62clwwlk 30442
[Huneke] p. 2Definition 7numclwwlkovh 30468  numclwwlkovh0 30467
[Huneke] p. 2Statement 10numclwwlk2 30476
[Huneke] p. 2Statement 11rusgrnumwlkg 30073
[Huneke] p. 2Statement 12numclwwlk3 30480
[Huneke] p. 2Statement 13numclwwlk5 30483
[Huneke] p. 2Statement 14numclwwlk7 30486
[Indrzejczak] p. 33Definition ` `Enatded 30498  natded 30498
[Indrzejczak] p. 33Definition ` `Inatded 30498
[Indrzejczak] p. 34Definition ` `Enatded 30498  natded 30498
[Indrzejczak] p. 34Definition ` `Inatded 30498
[Jech] p. 4Definition of classcv 1546  cvjust 2734
[Jech] p. 42Lemma 6.1alephexp1 10500
[Jech] p. 42Equation 6.1alephadd 10498  alephmul 10499
[Jech] p. 43Lemma 6.2infmap 10497  infmap2 10137
[Jech] p. 71Lemma 9.3jech9.3 9736
[Jech] p. 72Equation 9.3scott0 9808  scottex 9807
[Jech] p. 72Exercise 9.1rankval4 9789  rankval4b 35290
[Jech] p. 72Scheme "Collection Principle"cp 9813
[Jech] p. 78Noteopthprc 5689
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43361
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43449
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43450
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43373
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43377
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43378  rmyp1 43379
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43380  rmym1 43381
[JonesMatijasevic] p. 695Equation 2.11rmx0 43371  rmx1 43372  rmxluc 43382
[JonesMatijasevic] p. 695Equation 2.12rmy0 43375  rmy1 43376  rmyluc 43383
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43385
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43386
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43406  jm2.17b 43407  jm2.17c 43408
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43439
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43443
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43434
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43409  jm2.24nn 43405
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43448
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43454  rmygeid 43410
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43466
[Juillerat] p. 11Section *5etransc 46727  etransclem47 46725  etransclem48 46726
[Juillerat] p. 12Equation (7)etransclem44 46722
[Juillerat] p. 12Equation *(7)etransclem46 46724
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46710
[Juillerat] p. 13Proofetransclem35 46713
[Juillerat] p. 13Part of case 2 proven inetransclem38 46716
[Juillerat] p. 13Part of case 2 provenetransclem24 46702
[Juillerat] p. 13Part of case 2: proven inetransclem41 46719
[Juillerat] p. 14Proofetransclem23 46701
[KalishMontague] p. 81Note 1ax-6 1974
[KalishMontague] p. 85Lemma 2equid 2019
[KalishMontague] p. 85Lemma 3equcomi 2024
[KalishMontague] p. 86Lemma 7cbvalivw 2014  cbvaliw 2013  wl-cbvmotv 37885  wl-motae 37887  wl-moteq 37886
[KalishMontague] p. 87Lemma 8spimvw 1993  spimw 1977
[KalishMontague] p. 87Lemma 9spfw 2040  spw 2041
[Kalmbach] p. 14Definition of latticechabs1 31612  chabs1i 31614  chabs2 31613  chabs2i 31615  chjass 31629  chjassi 31582  latabs1 18439  latabs2 18440
[Kalmbach] p. 15Definition of atomdf-at 32434  ela 32435
[Kalmbach] p. 15Definition of coverscvbr2 32379  cvrval2 39767
[Kalmbach] p. 16Definitiondf-ol 39671  df-oml 39672
[Kalmbach] p. 20Definition of commutescmbr 31680  cmbri 31686  cmtvalN 39704  df-cm 31679  df-cmtN 39670
[Kalmbach] p. 22Remarkomllaw5N 39740  pjoml5 31709  pjoml5i 31684
[Kalmbach] p. 22Definitionpjoml2 31707  pjoml2i 31681
[Kalmbach] p. 22Theorem 2(v)cmcm 31710  cmcmi 31688  cmcmii 31693  cmtcomN 39742
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39738  omlsi 31500  pjoml 31532  pjomli 31531
[Kalmbach] p. 22Definition of OML lawomllaw2N 39737
[Kalmbach] p. 23Remarkcmbr2i 31692  cmcm3 31711  cmcm3i 31690  cmcm3ii 31695  cmcm4i 31691  cmt3N 39744  cmt4N 39745  cmtbr2N 39746
[Kalmbach] p. 23Lemma 3cmbr3 31704  cmbr3i 31696  cmtbr3N 39747
[Kalmbach] p. 25Theorem 5fh1 31714  fh1i 31717  fh2 31715  fh2i 31718  omlfh1N 39751
[Kalmbach] p. 65Remarkchjatom 32453  chslej 31594  chsleji 31554  shslej 31476  shsleji 31466
[Kalmbach] p. 65Proposition 1chocin 31591  chocini 31550  chsupcl 31436  chsupval2 31506  h0elch 31351  helch 31339  hsupval2 31505  ocin 31392  ococss 31389  shococss 31390
[Kalmbach] p. 65Definition of subspace sumshsval 31408
[Kalmbach] p. 66Remarkdf-pjh 31491  pjssmi 32261  pjssmii 31777
[Kalmbach] p. 67Lemma 3osum 31741  osumi 31738
[Kalmbach] p. 67Lemma 4pjci 32296
[Kalmbach] p. 103Exercise 6atmd2 32496
[Kalmbach] p. 103Exercise 12mdsl0 32406
[Kalmbach] p. 140Remarkhatomic 32456  hatomici 32455  hatomistici 32458
[Kalmbach] p. 140Proposition 1atlatmstc 39812
[Kalmbach] p. 140Proposition 1(i)atexch 32477  lsatexch 39536
[Kalmbach] p. 140Proposition 1(ii)chcv1 32451  cvlcvr1 39832  cvr1 39903
[Kalmbach] p. 140Proposition 1(iii)cvexch 32470  cvexchi 32465  cvrexch 39913
[Kalmbach] p. 149Remark 2chrelati 32460  hlrelat 39895  hlrelat5N 39894  lrelat 39507
[Kalmbach] p. 153Exercise 5lsmcv 21141  lsmsatcv 39503  spansncv 31749  spansncvi 31748
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39522  spansncv2 32389
[Kalmbach] p. 266Definitiondf-st 32307
[Kalmbach2] p. 8Definition of adjointdf-adjh 31945
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10567  fpwwe2 10564
[KanamoriPincus] p. 416Corollary 1.3canth4 10568
[KanamoriPincus] p. 417Corollary 1.6canthp1 10575
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10570
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10572
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10585
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10589  gchxpidm 10590
[KanamoriPincus] p. 419Theorem 2.1gchacg 10601  gchhar 10600
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10135  unxpwdom 9501
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10591
[Kreyszig] p. 3Property M1metcl 24322  xmetcl 24321
[Kreyszig] p. 4Property M2meteq0 24329
[Kreyszig] p. 8Definition 1.1-8dscmet 24562
[Kreyszig] p. 12Equation 5conjmul 11870  muleqadd 11792
[Kreyszig] p. 18Definition 1.3-2mopnval 24428
[Kreyszig] p. 19Remarkmopntopon 24429
[Kreyszig] p. 19Theorem T1mopn0 24488  mopnm 24434
[Kreyszig] p. 19Theorem T2unimopn 24486
[Kreyszig] p. 19Definition of neighborhoodneibl 24491
[Kreyszig] p. 20Definition 1.3-3metcnp2 24532
[Kreyszig] p. 25Definition 1.4-1lmbr 23248  lmmbr 25250  lmmbr2 25251
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23370
[Kreyszig] p. 28Theorem 1.4-5lmcau 25305
[Kreyszig] p. 28Definition 1.4-3iscau 25268  iscmet2 25286
[Kreyszig] p. 30Theorem 1.4-7cmetss 25308
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23451  metelcls 25297
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25298  metcld2 25299
[Kreyszig] p. 51Equation 2clmvneg1 25091  lmodvneg1 20902  nvinv 30735  vcm 30672
[Kreyszig] p. 51Equation 1aclm0vs 25087  lmod0vs 20892  slmd0vs 33312  vc0 30670
[Kreyszig] p. 51Equation 1blmodvs0 20893  slmdvs0 33313  vcz 30671
[Kreyszig] p. 58Definition 2.2-1imsmet 30787  ngpmet 24593  nrmmetd 24564
[Kreyszig] p. 59Equation 1imsdval 30782  imsdval2 30783  ncvspds 25153  ngpds 24594
[Kreyszig] p. 63Problem 1nmval 24579  nvnd 30784
[Kreyszig] p. 64Problem 2nmeq0 24608  nmge0 24607  nvge0 30769  nvz 30765
[Kreyszig] p. 64Problem 3nmrtri 24614  nvabs 30768
[Kreyszig] p. 91Definition 2.7-1isblo3i 30897
[Kreyszig] p. 92Equation 2df-nmoo 30841
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30903  blocni 30901
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30902
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25196  ipeq0 21620  ipz 30815
[Kreyszig] p. 135Problem 2cphpyth 25208  pythi 30946
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30950
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25230
[Kreyszig] p. 144Equation 4supcvg 15819
[Kreyszig] p. 144Theorem 3.3-1minvec 25428  minveco 30980
[Kreyszig] p. 196Definition 3.9-1df-aj 30846
[Kreyszig] p. 247Theorem 4.7-2bcth 25321
[Kreyszig] p. 249Theorem 4.7-3ubth 30969
[Kreyszig] p. 470Definition of positive operator orderingleop 32219  leopg 32218
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32237
[Kreyszig] p. 525Theorem 10.1-1htth 31014
[Kulpa] p. 547Theorempoimir 38021
[Kulpa] p. 547Equation (1)poimirlem32 38020
[Kulpa] p. 547Equation (2)poimirlem31 38019
[Kulpa] p. 548Theorembroucube 38022
[Kulpa] p. 548Equation (6)poimirlem26 38014
[Kulpa] p. 548Equation (7)poimirlem27 38015
[Kunen] p. 10Axiom 0ax6e 2391  axnul 5234
[Kunen] p. 11Axiom 3axnul 5234
[Kunen] p. 12Axiom 6zfrep6 5218
[Kunen] p. 24Definition 10.24mapval 8782  mapvalg 8780
[Kunen] p. 30Lemma 10.20fodomg 10442
[Kunen] p. 31Definition 10.24mapex 7888
[Kunen] p. 95Definition 2.1df-r1 9686
[Kunen] p. 97Lemma 2.10r1elss 9728  r1elssi 9727
[Kunen] p. 107Exercise 4rankop 9780  rankopb 9774  rankuni 9785  rankxplim 9801  rankxpsuc 9804
[Kunen2] p. 47Lemma I.9.9relpfr 45399
[Kunen2] p. 53Lemma I.9.21trfr 45407
[Kunen2] p. 53Lemma I.9.24(2)wffr 45406
[Kunen2] p. 53Definition I.9.20tcfr 45408
[Kunen2] p. 95Lemma I.16.2ralabso 45413  rexabso 45414
[Kunen2] p. 96Example I.16.3disjabso 45420  n0abso 45421  ssabso 45419
[Kunen2] p. 111Lemma II.2.4(1)traxext 45422
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45432
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45427
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45430
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45431
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45426
[Kunen2] p. 112Corollary II.2.5wfaxext 45438  wfaxpr 45443  wfaxreg 45445  wfaxrep 45439  wfaxsep 45440  wfaxun 45444
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45429
[Kunen2] p. 113Corollary II.2.9wfaxpow 45442
[Kunen2] p. 114Theorem II.2.13wfaxext 45438
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45437  omelaxinf2 45434
[Kunen2] p. 114Corollary II.2.12wfac8prim 45447  wfaxinf2 45446
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45460  permaxext 45450  permaxinf2 45458  permaxnul 45453  permaxpow 45454  permaxpr 45455  permaxrep 45451  permaxsep 45452  permaxun 45456
[Kunen2] p. 148Definition II.9.1brpermmodel 45448
[Kunen2] p. 149Exercise II.9.3permac8prim 45459
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4941
[Lang] , p. 225Corollary 1.3finexttrb 33856
[Lang] p. Definitiondf-rn 5636
[Lang] p. 3Statementlidrideqd 18635  mndbn0 18716
[Lang] p. 3Definitiondf-mnd 18701
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18653
[Lang] p. 4Property of composites. Second formulagsumccat 18807
[Lang] p. 5Equationgsumreidx 19890
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48674
[Lang] p. 6Examplenn0mnd 48671
[Lang] p. 6Equationgsumxp2 19953
[Lang] p. 6Statementcycsubm 19175
[Lang] p. 6Definitionmulgnn0gsum 19054
[Lang] p. 6Observationmndlsmidm 19643
[Lang] p. 7Definitiondfgrp2e 18937
[Lang] p. 30Definitiondf-tocyc 33195
[Lang] p. 32Property (a)cyc3genpm 33240
[Lang] p. 32Property (b)cyc3conja 33245  cycpmconjv 33230
[Lang] p. 53Definitiondf-cat 17632
[Lang] p. 53Axiom CAT 1cat1 18062  cat1lem 18061
[Lang] p. 54Definitiondf-iso 17714
[Lang] p. 57Definitiondf-inito 17949  df-termo 17950
[Lang] p. 58Exampleirinitoringc 21461
[Lang] p. 58Statementinitoeu1 17976  termoeu1 17983
[Lang] p. 62Definitiondf-func 17823
[Lang] p. 65Definitiondf-nat 17911
[Lang] p. 91Notedf-ringc 20625
[Lang] p. 92Statementmxidlprm 33560
[Lang] p. 92Definitionisprmidlc 33537
[Lang] p. 128Remarkdsmmlmod 21727
[Lang] p. 129Prooflincscm 48922  lincscmcl 48924  lincsum 48921  lincsumcl 48923
[Lang] p. 129Statementlincolss 48926
[Lang] p. 129Observationdsmmfi 21720
[Lang] p. 141Theorem 5.3dimkerim 33818  qusdimsum 33819
[Lang] p. 141Corollary 5.4lssdimle 33799
[Lang] p. 147Definitionsnlindsntor 48963
[Lang] p. 504Statementmat1 22437  matring 22433
[Lang] p. 504Definitiondf-mamu 22381
[Lang] p. 505Statementmamuass 22392  mamutpos 22448  matassa 22434  mattposvs 22445  tposmap 22447
[Lang] p. 513Definitionmdet1 22591  mdetf 22585
[Lang] p. 513Theorem 4.4cramer 22681
[Lang] p. 514Proposition 4.6mdetleib 22577
[Lang] p. 514Proposition 4.8mdettpos 22601
[Lang] p. 515Definitiondf-minmar1 22625  smadiadetr 22665
[Lang] p. 515Corollary 4.9mdetero 22600  mdetralt 22598
[Lang] p. 517Proposition 4.15mdetmul 22613
[Lang] p. 518Definitiondf-madu 22624
[Lang] p. 518Proposition 4.16madulid 22635  madurid 22634  matinv 22667
[Lang] p. 561Theorem 3.1cayleyhamilton 22880
[Lang], p. 190Chapter 6vieta 33771
[Lang], p. 224Proposition 1.1extdgfialg 33885  finextalg 33889
[Lang], p. 224Proposition 1.2extdgmul 33854  fedgmul 33822
[Lang], p. 225Proposition 1.4algextdeg 33916
[Lang], p. 561Remarkchpmatply1 22822
[Lang], p. 561Definitiondf-chpmat 22817
[Lang2] p. 3Notationsdf-ind 12158
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44779
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44774
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44780
[LeBlanc] p. 277Rule R2axnul 5234
[Levy] p. 12Axiom 4.3.1df-clab 2719  wl-df.clab 37870
[Levy] p. 59Definitiondf-ttrcl 9627
[Levy] p. 64Theorem 5.6(ii)frinsg 9673
[Levy] p. 338Axiomdf-clel 2815  df-cleq 2732  wl-df.cleq 37871
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 37874
[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 37874
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2815  df-cleq 2732  wl-df.cleq 37871
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2719  wl-df.clab 37870
[Levy] p. 358Axiomdf-clab 2719  wl-df.clab 37870
[Levy58] p. 2Definition Iisfin1-3 10306
[Levy58] p. 2Definition IIdf-fin2 10206
[Levy58] p. 2Definition Iadf-fin1a 10205
[Levy58] p. 2Definition IIIdf-fin3 10208
[Levy58] p. 3Definition Vdf-fin5 10209
[Levy58] p. 3Definition IVdf-fin4 10207
[Levy58] p. 4Definition VIdf-fin6 10210
[Levy58] p. 4Definition VIIdf-fin7 10211
[Levy58], p. 3Theorem 1fin1a2 10335
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27675
[Lipparini] p. 3Lemma 2.1.4noresle 27686
[Lipparini] p. 6Proposition 4.2noinfbnd1 27718  nosupbnd1 27703
[Lipparini] p. 6Proposition 4.3noinfbnd2 27720  nosupbnd2 27705
[Lipparini] p. 7Theorem 5.1noetasuplem3 27724  noetasuplem4 27725
[Lipparini] p. 7Corollary 4.4nosupinfsep 27721
[Lopez-Astorga] p. 12Rule 1mptnan 1775
[Lopez-Astorga] p. 12Rule 2mptxor 1776
[Lopez-Astorga] p. 12Rule 3mtpxor 1778
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32504
[Maeda] p. 168Lemma 5mdsym 32508  mdsymi 32507
[Maeda] p. 168Lemma 4(i)mdsymlem4 32502  mdsymlem6 32504  mdsymlem7 32505
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32506
[MaedaMaeda] p. 1Remarkssdmd1 32409  ssdmd2 32410  ssmd1 32407  ssmd2 32408
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32405
[MaedaMaeda] p. 1Definition 1.1df-dmd 32377  df-md 32376  mdbr 32390
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32427  mdslj1i 32415  mdslj2i 32416  mdslle1i 32413  mdslle2i 32414  mdslmd1i 32425  mdslmd2i 32426
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32417  mdsl2bi 32419  mdsl2i 32418
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32431
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32428
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32429
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32406
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32411  mdsl3 32412
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32430
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32525
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39814  hlrelat1 39893
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39532
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32432  cvmdi 32420  cvnbtwn4 32385  cvrnbtwn4 39772
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32433
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39833  cvp 32471  cvrp 39909  lcvp 39533
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32495
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32494
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39826  hlexch4N 39885
[MaedaMaeda] p. 34Exercise 7.1atabsi 32497
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39936
[MaedaMaeda] p. 61Definition 15.10psubN 40242  atpsubN 40246  df-pointsN 39995  pointpsubN 40244
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39997  pmap11 40255  pmaple 40254  pmapsub 40261  pmapval 40250
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40258  pmap1N 40260
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40263  pmapglb2N 40264  pmapglb2xN 40265  pmapglbx 40262
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40345
[MaedaMaeda] p. 67Postulate PS1ps-1 39970
[MaedaMaeda] p. 68Lemma 16.2df-padd 40289  paddclN 40335  paddidm 40334
[MaedaMaeda] p. 68Condition PS2ps-2 39971
[MaedaMaeda] p. 68Equation 16.2.1paddass 40331
[MaedaMaeda] p. 69Lemma 16.4ps-1 39970
[MaedaMaeda] p. 69Theorem 16.4ps-2 39971
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19648  lsmmod2 19649  lssats 39505  shatomici 32454  shatomistici 32457  shmodi 31486  shmodsi 31485
[MaedaMaeda] p. 130Remark 29.6dmdmd 32396  mdsymlem7 32505
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31685
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31589
[MaedaMaeda] p. 139Remarksumdmdii 32511
[Margaris] p. 40Rule Cexlimiv 1937
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 397  df-ex 1787  df-or 854  dfbi2 475
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30495
[Margaris] p. 59Section 14notnotrALTVD 45359
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 45360
[Margaris] p. 79Rule Cexinst01 45070  exinst11 45071
[Margaris] p. 89Theorem 19.219.2 1983  19.2g 2200  r19.2z 4434
[Margaris] p. 89Theorem 19.319.3 2214  rr19.3v 3612
[Margaris] p. 89Theorem 19.5alcom 2170
[Margaris] p. 89Theorem 19.6alex 1833
[Margaris] p. 89Theorem 19.7alnex 1788
[Margaris] p. 89Theorem 19.819.8a 2193
[Margaris] p. 89Theorem 19.919.9 2217  19.9h 2297  exlimd 2230  exlimdh 2301
[Margaris] p. 89Theorem 19.11excom 2173  excomim 2174
[Margaris] p. 89Theorem 19.1219.12 2336
[Margaris] p. 90Section 19conventions-labels 30496  conventions-labels 30496  conventions-labels 30496  conventions-labels 30496
[Margaris] p. 90Theorem 19.14exnal 1834
[Margaris] p. 90Theorem 19.152albi 44823  albi 1825
[Margaris] p. 90Theorem 19.1619.16 2237
[Margaris] p. 90Theorem 19.1719.17 2238
[Margaris] p. 90Theorem 19.182exbi 44825  exbi 1854
[Margaris] p. 90Theorem 19.1919.19 2241
[Margaris] p. 90Theorem 19.202alim 44822  2alimdv 1925  alimd 2224  alimdh 1824  alimdv 1923  ax-4 1816  ralimdaa 3241  ralimdv 3154  ralimdva 3152  ralimdvva 3187  sbcimdv 3798
[Margaris] p. 90Theorem 19.2119.21 2219  19.21h 2298  19.21t 2218  19.21vv 44821  alrimd 2227  alrimdd 2226  alrimdh 1870  alrimdv 1936  alrimi 2225  alrimih 1831  alrimiv 1934  alrimivv 1935  bj-alrimdh 36936  hbralrimi 3130  r19.21be 3233  r19.21bi 3232  ralrimd 3245  ralrimdv 3138  ralrimdva 3140  ralrimdvv 3184  ralrimdvva 3195  ralrimi 3238  ralrimia 3239  ralrimiv 3131  ralrimiva 3132  ralrimivv 3181  ralrimivva 3183  ralrimivvva 3186  ralrimivw 3136
[Margaris] p. 90Theorem 19.222exim 44824  2eximdv 1926  bj-exim 36951  exim 1841  eximd 2228  eximdh 1871  eximdv 1924  rexim 3081  reximd2a 3250  reximdai 3242  reximdd 45596  reximddv 3156  reximddv2 3199  reximddv3 3157  reximdv 3155  reximdv2 3150  reximdva 3153  reximdvai 3151  reximdvva 3188  reximi2 3073
[Margaris] p. 90Theorem 19.2319.23 2223  19.23bi 2203  19.23h 2299  19.23t 2222  exlimdv 1940  exlimdvv 1941  exlimexi 44969  exlimiv 1937  exlimivv 1939  rexlimd3 45592  rexlimdv 3139  rexlimdv3a 3145  rexlimdva 3141  rexlimdva2 3143  rexlimdvaa 3142  rexlimdvv 3196  rexlimdvva 3197  rexlimdvvva 3198  rexlimdvw 3146  rexlimiv 3134  rexlimiva 3133  rexlimivv 3182
[Margaris] p. 90Theorem 19.2419.24 1998
[Margaris] p. 90Theorem 19.2519.25 1887
[Margaris] p. 90Theorem 19.2619.26 1877
[Margaris] p. 90Theorem 19.2719.27 2239  r19.27z 4445  r19.27zv 4446
[Margaris] p. 90Theorem 19.2819.28 2240  19.28vv 44831  r19.28z 4437  r19.28zf 45607  r19.28zv 4441  rr19.28v 3613
[Margaris] p. 90Theorem 19.2919.29 1880  r19.29d2r 3127  r19.29imd 3105
[Margaris] p. 90Theorem 19.3019.30 1888
[Margaris] p. 90Theorem 19.3119.31 2246  19.31vv 44829
[Margaris] p. 90Theorem 19.3219.32 2245  r19.32 47562
[Margaris] p. 90Theorem 19.3319.33-2 44827  19.33 1891
[Margaris] p. 90Theorem 19.3419.34 1999
[Margaris] p. 90Theorem 19.3519.35 1884
[Margaris] p. 90Theorem 19.3619.36 2242  19.36vv 44828  r19.36zv 4447
[Margaris] p. 90Theorem 19.3719.37 2244  19.37vv 44830  r19.37zv 4442
[Margaris] p. 90Theorem 19.3819.38 1846
[Margaris] p. 90Theorem 19.3919.39 1997
[Margaris] p. 90Theorem 19.4019.40-2 1894  19.40 1893  r19.40 3106
[Margaris] p. 90Theorem 19.4119.41 2247  19.41rg 44995
[Margaris] p. 90Theorem 19.4219.42 2248
[Margaris] p. 90Theorem 19.4319.43 1889
[Margaris] p. 90Theorem 19.4419.44 2249  r19.44zv 4444
[Margaris] p. 90Theorem 19.4519.45 2250  r19.45zv 4443
[Margaris] p. 110Exercise 2(b)eu1 2614
[Mayet] p. 370Remarkjpi 32366  largei 32363  stri 32353
[Mayet3] p. 9Definition of CH-statesdf-hst 32308  ishst 32310
[Mayet3] p. 10Theoremhstrbi 32362  hstri 32361
[Mayet3] p. 1223Theorem 4.1mayete3i 31824
[Mayet3] p. 1240Theorem 7.1mayetes3i 31825
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32374
[MegPav2000] p. 2345Definition 3.4-1chintcl 31428  chsupcl 31436
[MegPav2000] p. 2345Definition 3.4-2hatomic 32456
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32450
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32477
[MegPav2000] p. 2366Figure 7pl42N 40476
[MegPav2002] p. 362Lemma 2.2latj31 18451  latj32 18449  latjass 18447
[Megill] p. 444Axiom C5ax-5 1917  ax5ALT 39400
[Megill] p. 444Section 7conventions 30495
[Megill] p. 445Lemma L12aecom-o 39394  ax-c11n 39381  axc11n 2434
[Megill] p. 446Lemma L17equtrr 2029
[Megill] p. 446Lemma L18ax6fromc10 39389
[Megill] p. 446Lemma L19hbnae-o 39421  hbnae 2440
[Megill] p. 447Remark 9.1dfsb1 2489  sbid 2267  sbidd-misc 50210  sbidd 50209
[Megill] p. 448Remark 9.6axc14 2471
[Megill] p. 448Scheme C4'ax-c4 39377
[Megill] p. 448Scheme C5'ax-c5 39376  sp 2195
[Megill] p. 448Scheme C6'ax-11 2168
[Megill] p. 448Scheme C7'ax-c7 39378
[Megill] p. 448Scheme C8'ax-7 2015
[Megill] p. 448Scheme C9'ax-c9 39383
[Megill] p. 448Scheme C10'ax-6 1974  ax-c10 39379
[Megill] p. 448Scheme C11'ax-c11 39380
[Megill] p. 448Scheme C12'ax-8 2121
[Megill] p. 448Scheme C13'ax-9 2129
[Megill] p. 448Scheme C14'ax-c14 39384
[Megill] p. 448Scheme C15'ax-c15 39382
[Megill] p. 448Scheme C16'ax-c16 39385
[Megill] p. 448Theorem 9.4dral1-o 39397  dral1 2447  dral2-o 39423  dral2 2446  drex1 2449  drex2 2450  drsb1 2503  drsb2 2278
[Megill] p. 449Theorem 9.7sbcom2 2183  sbequ 2094  sbid2v 2517
[Megill] p. 450Example in Appendixhba1-o 39390  hba1 2304
[Mendelson] p. 35Axiom A3hirstL-ax3 47356
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3818  rspsbca 3819  stdpc4 2079
[Mendelson] p. 69Axiom 5ax-c4 39377  ra4 3825  stdpc5 2220
[Mendelson] p. 81Rule Cexlimiv 1937
[Mendelson] p. 95Axiom 6stdpc6 2035
[Mendelson] p. 95Axiom 7stdpc7 2262
[Mendelson] p. 225Axiom system NBGru 3728
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5462
[Mendelson] p. 231Exercise 4.10(k)inv1 4333
[Mendelson] p. 231Exercise 4.10(l)unv 4334
[Mendelson] p. 231Exercise 4.10(n)dfin3 4212
[Mendelson] p. 231Exercise 4.10(o)df-nul 4269
[Mendelson] p. 231Exercise 4.10(q)dfin4 4213
[Mendelson] p. 231Exercise 4.10(s)ddif 4078
[Mendelson] p. 231Definition of uniondfun3 4211
[Mendelson] p. 235Exercise 4.12(c)univ 5397
[Mendelson] p. 235Exercise 4.12(d)pwv 4842
[Mendelson] p. 235Exercise 4.12(j)pwin 5516
[Mendelson] p. 235Exercise 4.12(k)pwunss 4554
[Mendelson] p. 235Exercise 4.12(l)pwssun 5517
[Mendelson] p. 235Exercise 4.12(n)uniin 4869
[Mendelson] p. 235Exercise 4.12(p)reli 5776
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6227
[Mendelson] p. 244Proposition 4.8(g)epweon 7725
[Mendelson] p. 246Definition of successordf-suc 6323
[Mendelson] p. 250Exercise 4.36oelim2 8528
[Mendelson] p. 254Proposition 4.22(b)xpen 9075
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8996  xpsneng 8997
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9003  xpcomeng 9004
[Mendelson] p. 254Proposition 4.22(e)xpassen 9006
[Mendelson] p. 255Definitionbrsdom 8918
[Mendelson] p. 255Exercise 4.39endisj 8999
[Mendelson] p. 255Exercise 4.41mapprc 8774
[Mendelson] p. 255Exercise 4.43mapsnen 8981  mapsnend 8980
[Mendelson] p. 255Exercise 4.45mapunen 9081
[Mendelson] p. 255Exercise 4.47xpmapen 9080
[Mendelson] p. 255Exercise 4.42(a)map0e 8827
[Mendelson] p. 255Exercise 4.42(b)map1 8984
[Mendelson] p. 257Proposition 4.24(a)undom 9000
[Mendelson] p. 258Exercise 4.56(c)djuassen 10099  djucomen 10098
[Mendelson] p. 258Exercise 4.56(f)djudom1 10103
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10097
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8463
[Mendelson] p. 266Proposition 4.34(f)oaordex 8490
[Mendelson] p. 275Proposition 4.42(d)entri3 10479
[Mendelson] p. 281Definitiondf-r1 9686
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9735
[Mendelson] p. 287Axiom system MKru 3728
[MertziosUnger] p. 152Definitiondf-frgr 30354
[MertziosUnger] p. 153Remark 1frgrconngr 30389
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30391  vdgn1frgrv3 30392
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30393
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30386
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30379  2pthfrgrrn 30377  2pthfrgrrn2 30378
[Mittelstaedt] p. 9Definitiondf-oc 31348
[Monk1] p. 22Remarkconventions 30495
[Monk1] p. 22Theorem 3.1conventions 30495
[Monk1] p. 26Theorem 2.8(vii)ssin 4174
[Monk1] p. 33Theorem 3.2(i)ssrel 5733  ssrelf 32714
[Monk1] p. 33Theorem 3.2(ii)eqrel 5734
[Monk1] p. 34Definition 3.3df-opab 5142
[Monk1] p. 36Theorem 3.7(i)coi1 6221  coi2 6222
[Monk1] p. 36Theorem 3.8(v)dm0 5869  rn0 5875
[Monk1] p. 36Theorem 3.7(ii)cnvi 6099
[Monk1] p. 37Theorem 3.13(i)relxp 5643
[Monk1] p. 37Theorem 3.13(x)dmxp 5878  rnxp 6128
[Monk1] p. 37Theorem 3.13(ii)0xp 5724  xp0 5725
[Monk1] p. 38Theorem 3.16(ii)ima0 6036
[Monk1] p. 38Theorem 3.16(viii)imai 6033
[Monk1] p. 39Theorem 3.17imaex 7861  imaexg 7860
[Monk1] p. 39Theorem 3.16(xi)imassrn 6030
[Monk1] p. 41Theorem 4.3(i)fnopfv 7023  funfvop 6998
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6888
[Monk1] p. 42Theorem 4.4(iii)fvelima 6899
[Monk1] p. 43Theorem 4.6funun 6538
[Monk1] p. 43Theorem 4.8(iv)dff13 7205  dff13f 7206
[Monk1] p. 46Theorem 4.15(v)funex 7170  funrnex 7903
[Monk1] p. 50Definition 5.4fniunfv 7198
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6185
[Monk1] p. 52Theorem 5.11(viii)ssint 4901
[Monk1] p. 52Definition 5.13 (i)1stval2 7955  df-1st 7938
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7956  df-2nd 7939
[Monk1] p. 112Theorem 15.17(v)ranksn 9776  ranksnb 9749
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9777
[Monk1] p. 112Theorem 15.17(iii)rankun 9778  rankunb 9772
[Monk1] p. 113Theorem 15.18r1val3 9760
[Monk1] p. 113Definition 15.19df-r1 9686  r1val2 9759
[Monk1] p. 117Lemmazorn2 10426  zorn2g 10423
[Monk1] p. 133Theorem 18.11cardom 9908
[Monk1] p. 133Theorem 18.12canth3 10481
[Monk1] p. 133Theorem 18.14carduni 9903
[Monk2] p. 105Axiom C4ax-4 1816
[Monk2] p. 105Axiom C7ax-7 2015
[Monk2] p. 105Axiom C8ax-12 2189  ax-c15 39382  ax12v2 2191
[Monk2] p. 108Lemma 5ax-c4 39377
[Monk2] p. 109Lemma 12ax-11 2168
[Monk2] p. 109Lemma 15equvini 2463  equvinv 2036  eqvinop 5434
[Monk2] p. 113Axiom C5-1ax-5 1917  ax5ALT 39400
[Monk2] p. 113Axiom C5-2ax-10 2152
[Monk2] p. 113Axiom C5-3ax-11 2168
[Monk2] p. 114Lemma 21sp 2195
[Monk2] p. 114Lemma 22axc4 2330  hba1-o 39390  hba1 2304
[Monk2] p. 114Lemma 23nfia1 2164
[Monk2] p. 114Lemma 24nfa2 2186  nfra2 3341  nfra2w 3276
[Moore] p. 53Part Idf-mre 17546
[Munkres] p. 77Example 2distop 22985  indistop 22992  indistopon 22991
[Munkres] p. 77Example 3fctop 22994  fctop2 22995
[Munkres] p. 77Example 4cctop 22996
[Munkres] p. 78Definition of basisdf-bases 22936  isbasis3g 22939
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17404  tgval2 22946
[Munkres] p. 79Remarktgcl 22959
[Munkres] p. 80Lemma 2.1tgval3 22953
[Munkres] p. 80Lemma 2.2tgss2 22977  tgss3 22976
[Munkres] p. 81Lemma 2.3basgen 22978  basgen2 22979
[Munkres] p. 83Exercise 3topdifinf 37712  topdifinfeq 37713  topdifinffin 37711  topdifinfindis 37709
[Munkres] p. 89Definition of subspace topologyresttop 23150
[Munkres] p. 93Theorem 6.1(1)0cld 23028  topcld 23025
[Munkres] p. 93Theorem 6.1(2)iincld 23029
[Munkres] p. 93Theorem 6.1(3)uncld 23031
[Munkres] p. 94Definition of closureclsval 23027
[Munkres] p. 94Definition of interiorntrval 23026
[Munkres] p. 95Theorem 6.5(a)clsndisj 23065  elcls 23063
[Munkres] p. 95Theorem 6.5(b)elcls3 23073
[Munkres] p. 97Theorem 6.6clslp 23138  neindisj 23107
[Munkres] p. 97Corollary 6.7cldlp 23140
[Munkres] p. 97Definition of limit pointislp2 23135  lpval 23129
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23305
[Munkres] p. 102Definition of continuous functiondf-cn 23217  iscn 23225  iscn2 23228
[Munkres] p. 107Theorem 7.2(g)cncnp 23270  cncnp2 23271  cncnpi 23268  df-cnp 23218  iscnp 23227  iscnp2 23229
[Munkres] p. 127Theorem 10.1metcn 24533
[Munkres] p. 128Theorem 10.3metcn4 25303
[Nathanson] p. 123Remarkreprgt 34812  reprinfz1 34813  reprlt 34810
[Nathanson] p. 123Definitiondf-repr 34800
[Nathanson] p. 123Chapter 5.1circlemethnat 34832
[Nathanson] p. 123Propositionbreprexp 34824  breprexpnat 34825  itgexpif 34797
[NielsenChuang] p. 195Equation 4.73unierri 32200
[OeSilva] p. 2042Section 2ax-bgbltosilva 48302
[Pfenning] p. 17Definition XMnatded 30498
[Pfenning] p. 17Definition NNCnatded 30498  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30498
[Pfenning] p. 18Rule"natded 30498
[Pfenning] p. 18Definition /\Inatded 30498
[Pfenning] p. 18Definition ` `Enatded 30498  natded 30498  natded 30498  natded 30498  natded 30498
[Pfenning] p. 18Definition ` `Inatded 30498  natded 30498  natded 30498  natded 30498  natded 30498
[Pfenning] p. 18Definition ` `ELnatded 30498
[Pfenning] p. 18Definition ` `ERnatded 30498
[Pfenning] p. 18Definition ` `Ea,unatded 30498
[Pfenning] p. 18Definition ` `IRnatded 30498
[Pfenning] p. 18Definition ` `Ianatded 30498
[Pfenning] p. 127Definition =Enatded 30498
[Pfenning] p. 127Definition =Inatded 30498
[Ponnusamy] p. 361Theorem 6.44cphip0l 25194  df-dip 30797  dip0l 30814  ip0l 21618
[Ponnusamy] p. 361Equation 6.45cphipval 25235  ipval 30799
[Ponnusamy] p. 362Equation I1dipcj 30810  ipcj 21616
[Ponnusamy] p. 362Equation I3cphdir 25197  dipdir 30938  ipdir 21621  ipdiri 30926
[Ponnusamy] p. 362Equation I4ipidsq 30806  nmsq 25186
[Ponnusamy] p. 362Equation 6.46ip0i 30921
[Ponnusamy] p. 362Equation 6.47ip1i 30923
[Ponnusamy] p. 362Equation 6.48ip2i 30924
[Ponnusamy] p. 363Equation I2cphass 25203  dipass 30941  ipass 21627  ipassi 30937
[Prugovecki] p. 186Definition of brabraval 32040  df-bra 31946
[Prugovecki] p. 376Equation 8.1df-kb 31947  kbval 32050
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32478
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40381
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32492  atcvat4i 32493  cvrat3 39935  cvrat4 39936  lsatcvat3 39545
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32378  cvrval 39762  df-cv 32375  df-lcv 39512  lspsncv0 21146
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40393
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40394
[Quine] p. 16Definition 2.1df-clab 2719  rabid 3413  rabidd 45603  wl-df.clab 37870
[Quine] p. 17Definition 2.1''dfsb7 2290
[Quine] p. 18Definition 2.7df-cleq 2732  wl-df.cleq 37871
[Quine] p. 19Definition 2.9conventions 30495  df-v 3434
[Quine] p. 34Theorem 5.1eqabb 2879
[Quine] p. 35Theorem 5.2abid1 2876  abid2f 2932
[Quine] p. 40Theorem 6.1sb5 2287
[Quine] p. 40Theorem 6.2sb6 2096  sbalex 2254
[Quine] p. 41Theorem 6.3df-clel 2815  wl-df.clel 37874
[Quine] p. 41Theorem 6.4eqid 2740  eqid1 30562
[Quine] p. 41Theorem 6.5eqcom 2747
[Quine] p. 42Theorem 6.6df-sbc 3731
[Quine] p. 42Theorem 6.7dfsbcq 3732  dfsbcq2 3733
[Quine] p. 43Theorem 6.8vex 3436
[Quine] p. 43Theorem 6.9isset 3446
[Quine] p. 44Theorem 7.3spcgf 3536  spcgv 3541  spcimgf 3498
[Quine] p. 44Theorem 6.11spsbc 3743  spsbcd 3744
[Quine] p. 44Theorem 6.12elex 3453
[Quine] p. 44Theorem 6.13elab 3624  elabg 3621  elabgf 3619
[Quine] p. 44Theorem 6.14noel 4273
[Quine] p. 48Theorem 7.2snprc 4656
[Quine] p. 48Definition 7.1df-pr 4565  df-sn 4563
[Quine] p. 49Theorem 7.4snss 4723  snssg 4722
[Quine] p. 49Theorem 7.5prss 4758  prssg 4757
[Quine] p. 49Theorem 7.6prid1 4701  prid1g 4699  prid2 4702  prid2g 4700  snid 4601  snidg 4599
[Quine] p. 51Theorem 7.12snex 5375
[Quine] p. 51Theorem 7.13prex 5374
[Quine] p. 53Theorem 8.2unisn 4864  unisnALT 45370  unisng 4863
[Quine] p. 53Theorem 8.3uniun 4868
[Quine] p. 54Theorem 8.6elssuni 4876
[Quine] p. 54Theorem 8.7uni0 4873
[Quine] p. 56Theorem 8.17uniabio 6462
[Quine] p. 56Definition 8.18dfaiota2 47550  dfiota2 6449
[Quine] p. 57Theorem 8.19aiotaval 47559  iotaval 6466
[Quine] p. 57Theorem 8.22iotanul 6472
[Quine] p. 58Theorem 8.23iotaex 6468
[Quine] p. 58Definition 9.1df-op 4569
[Quine] p. 61Theorem 9.5opabid 5474  opabidw 5473  opelopab 5491  opelopaba 5485  opelopabaf 5493  opelopabf 5494  opelopabg 5487  opelopabga 5482  opelopabgf 5489  oprabid 7395  oprabidw 7394
[Quine] p. 64Definition 9.11df-xp 5631
[Quine] p. 64Definition 9.12df-cnv 5633
[Quine] p. 64Definition 9.15df-id 5520
[Quine] p. 65Theorem 10.3fun0 6557
[Quine] p. 65Theorem 10.4funi 6524
[Quine] p. 65Theorem 10.5funsn 6545  funsng 6543
[Quine] p. 65Definition 10.1df-fun 6494
[Quine] p. 65Definition 10.2args 6051  dffv4 6831
[Quine] p. 68Definition 10.11conventions 30495  df-fv 6500  fv2 6829
[Quine] p. 124Theorem 17.3nn0opth2 14232  nn0opth2i 14231  nn0opthi 14230  omopthi 8594
[Quine] p. 177Definition 25.2df-rdg 8346
[Quine] p. 232Equation icarddom 10474
[Quine] p. 284Axiom 39(vi)funimaex 6580  funimaexg 6579
[Quine] p. 331Axiom system NFru 3728
[ReedSimon] p. 36Definition (iii)ax-his3 31180
[ReedSimon] p. 63Exercise 4(a)df-dip 30797  polid 31255  polid2i 31253  polidi 31254
[ReedSimon] p. 63Exercise 4(b)df-ph 30909
[ReedSimon] p. 195Remarklnophm 32115  lnophmi 32114
[Retherford] p. 49Exercise 1(i)leopadd 32228
[Retherford] p. 49Exercise 1(ii)leopmul 32230  leopmuli 32229
[Retherford] p. 49Exercise 1(iv)leoptr 32233
[Retherford] p. 49Definition VI.1df-leop 31948  leoppos 32222
[Retherford] p. 49Exercise 1(iii)leoptri 32232
[Retherford] p. 49Definition of operator orderingleop3 32221
[Ribenboim] p. 181Remarknprmdvdsfacm1 48103
[Ribenboim], p. 181Statementppivalnn 48111
[Roman] p. 4Definitiondf-dmat 22480  df-dmatalt 48890
[Roman] p. 18Part Preliminariesdf-rng 20132
[Roman] p. 19Part Preliminariesdf-ring 20214
[Roman] p. 46Theorem 1.6isldepslvec2 48977
[Roman] p. 112Noteisldepslvec2 48977  ldepsnlinc 49000  zlmodzxznm 48989
[Roman] p. 112Examplezlmodzxzequa 48988  zlmodzxzequap 48991  zlmodzxzldep 48996
[Roman] p. 170Theorem 7.8cayleyhamilton 22880
[Rosenlicht] p. 80Theoremheicant 38023
[Rosser] p. 281Definitiondf-op 4569
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34836
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34837
[Rotman] p. 28Remarkpgrpgt2nabl 48858  pmtr3ncom 19448
[Rotman] p. 31Theorem 3.4symggen2 19444
[Rotman] p. 42Theorem 3.15cayley 19387  cayleyth 19388
[Rudin] p. 164Equation 27efcan 16059
[Rudin] p. 164Equation 30efzval 16067
[Rudin] p. 167Equation 48absefi 16161
[Sanford] p. 39Remarkax-mp 5  mto 198
[Sanford] p. 39Rule 3mtpxor 1778
[Sanford] p. 39Rule 4mptxor 1776
[Sanford] p. 40Rule 1mptnan 1775
[Schechter] p. 51Definition of antisymmetryintasym 6072
[Schechter] p. 51Definition of irreflexivityintirr 6075
[Schechter] p. 51Definition of symmetrycnvsym 6071
[Schechter] p. 51Definition of transitivitycotr 6069
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17546
[Schechter] p. 79Definition of Moore closuredf-mrc 17547
[Schechter] p. 82Section 4.5df-mrc 17547
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17549
[Schechter] p. 139Definition AC3dfac9 10057
[Schechter] p. 141Definition (MC)dfac11 43508
[Schechter] p. 149Axiom DC1ax-dc 10366  axdc3 10374
[Schechter] p. 187Definition of "ring with unit"isring 20216  isrngo 38265
[Schechter] p. 276Remark 11.6.espan0 31638
[Schechter] p. 276Definition of spandf-span 31405  spanval 31429
[Schechter] p. 428Definition 15.35bastop1 22983
[Schloeder] p. 1Lemma 1.3onelon 6342  onelord 43697  ordelon 6341  ordelord 6339
[Schloeder] p. 1Lemma 1.7onepsuc 43698  sucidg 6400
[Schloeder] p. 1Remark 1.50elon 6372  onsuc 7760  ord0 6371  ordsuci 7758
[Schloeder] p. 1Theorem 1.9epsoon 43699
[Schloeder] p. 1Definition 1.1dftr5 5190
[Schloeder] p. 1Definition 1.2dford3 43474  elon2 6328
[Schloeder] p. 1Definition 1.4df-suc 6323
[Schloeder] p. 1Definition 1.6epel 5528  epelg 5526
[Schloeder] p. 1Theorem 1.9(i)elirr 9512  epirron 43700  ordirr 6335
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43702  oneptr 43701  ontr1 6364
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6360  oneptri 43703  ordtri3or 6349
[Schloeder] p. 2Lemma 1.10ondif1 8433  ord0eln0 6373
[Schloeder] p. 2Lemma 1.13elsuci 6386  onsucss 43712  trsucss 6407
[Schloeder] p. 2Lemma 1.14ordsucss 7765
[Schloeder] p. 2Lemma 1.15onnbtwn 6413  ordnbtwn 6412
[Schloeder] p. 2Lemma 1.16orddif0suc 43714  ordnexbtwnsuc 43713
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10321  onsucf1lem 43715  onsucf1o 43718  onsucf1olem 43716  onsucrn 43717
[Schloeder] p. 2Lemma 1.18dflim7 43719
[Schloeder] p. 2Remark 1.12ordzsl 7792
[Schloeder] p. 2Theorem 1.10ondif1i 43708  ordne0gt0 43707
[Schloeder] p. 2Definition 1.11dflim6 43710  limnsuc 43711  onsucelab 43709
[Schloeder] p. 3Remark 1.21omex 9562
[Schloeder] p. 3Theorem 1.19tfinds 7807
[Schloeder] p. 3Theorem 1.22omelon 9565  ordom 7823
[Schloeder] p. 3Definition 1.20dfom3 9566
[Schloeder] p. 4Lemma 2.21onn 8573
[Schloeder] p. 4Lemma 2.7ssonuni 7730  ssorduni 7729
[Schloeder] p. 4Remark 2.4oa1suc 8463
[Schloeder] p. 4Theorem 1.23dfom5 9569  limom 7829
[Schloeder] p. 4Definition 2.1df-1o 8402  df1o2 8409
[Schloeder] p. 4Definition 2.3oa0 8448  oa0suclim 43721  oalim 8464  oasuc 8456
[Schloeder] p. 4Definition 2.5om0 8449  om0suclim 43722  omlim 8465  omsuc 8458
[Schloeder] p. 4Definition 2.6oe0 8454  oe0m1 8453  oe0suclim 43723  oelim 8466  oesuc 8459
[Schloeder] p. 5Lemma 2.10onsupuni 43675
[Schloeder] p. 5Lemma 2.11onsupsucismax 43725
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43726
[Schloeder] p. 5Lemma 2.13limexissup 43727  limexissupab 43729  limiun 43728  limuni 6379
[Schloeder] p. 5Lemma 2.14oa0r 8470
[Schloeder] p. 5Lemma 2.15om1 8474  om1om1r 43730  om1r 8475
[Schloeder] p. 5Remark 2.8oacl 8467  oaomoecl 43724  oecl 8469  omcl 8468
[Schloeder] p. 5Definition 2.9onsupintrab 43677
[Schloeder] p. 6Lemma 2.16oe1 8476
[Schloeder] p. 6Lemma 2.17oe1m 8477
[Schloeder] p. 6Lemma 2.18oe0rif 43731
[Schloeder] p. 6Theorem 2.19oasubex 43732
[Schloeder] p. 6Theorem 2.20nnacl 8544  nnamecl 43733  nnecl 8546  nnmcl 8545
[Schloeder] p. 7Lemma 3.1onsucwordi 43734
[Schloeder] p. 7Lemma 3.2oaword1 8484
[Schloeder] p. 7Lemma 3.3oaword2 8485
[Schloeder] p. 7Lemma 3.4oalimcl 8492
[Schloeder] p. 7Lemma 3.5oaltublim 43736
[Schloeder] p. 8Lemma 3.6oaordi3 43737
[Schloeder] p. 8Lemma 3.81oaomeqom 43739
[Schloeder] p. 8Lemma 3.10oa00 8491
[Schloeder] p. 8Lemma 3.11omge1 43743  omword1 8505
[Schloeder] p. 8Remark 3.9oaordnr 43742  oaordnrex 43741
[Schloeder] p. 8Theorem 3.7oaord3 43738
[Schloeder] p. 9Lemma 3.12omge2 43744  omword2 8506
[Schloeder] p. 9Lemma 3.13omlim2 43745
[Schloeder] p. 9Lemma 3.14omord2lim 43746
[Schloeder] p. 9Lemma 3.15omord2i 43747  omordi 8498
[Schloeder] p. 9Theorem 3.16omord 8500  omord2com 43748
[Schloeder] p. 10Lemma 3.172omomeqom 43749  df-2o 8403
[Schloeder] p. 10Lemma 3.19oege1 43752  oewordi 8524
[Schloeder] p. 10Lemma 3.20oege2 43753  oeworde 8526
[Schloeder] p. 10Lemma 3.21rp-oelim2 43754
[Schloeder] p. 10Lemma 3.22oeord2lim 43755
[Schloeder] p. 10Remark 3.18omnord1 43751  omnord1ex 43750
[Schloeder] p. 11Lemma 3.23oeord2i 43756
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43758
[Schloeder] p. 11Remark 3.26oenord1 43762  oenord1ex 43761
[Schloeder] p. 11Theorem 4.1oaomoencom 43763
[Schloeder] p. 11Theorem 4.2oaass 8493
[Schloeder] p. 11Theorem 3.24oeord2com 43757
[Schloeder] p. 12Theorem 4.3odi 8511
[Schloeder] p. 13Theorem 4.4omass 8512
[Schloeder] p. 14Remark 4.6oenass 43765
[Schloeder] p. 14Theorem 4.7oeoa 8530
[Schloeder] p. 15Lemma 5.1cantnftermord 43766
[Schloeder] p. 15Lemma 5.2cantnfub 43767  cantnfub2 43768
[Schloeder] p. 16Theorem 5.3cantnf2 43771
[Schwabhauser] p. 10Axiom A1axcgrrflx 29008  axtgcgrrflx 28555
[Schwabhauser] p. 10Axiom A2axcgrtr 29009
[Schwabhauser] p. 10Axiom A3axcgrid 29010  axtgcgrid 28556
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28541
[Schwabhauser] p. 11Axiom A4axsegcon 29021  axtgsegcon 28557  df-trkgcb 28543
[Schwabhauser] p. 11Axiom A5ax5seg 29032  axtg5seg 28558  df-trkgcb 28543
[Schwabhauser] p. 11Axiom A6axbtwnid 29033  axtgbtwnid 28559  df-trkgb 28542
[Schwabhauser] p. 12Axiom A7axpasch 29035  axtgpasch 28560  df-trkgb 28542
[Schwabhauser] p. 12Axiom A8axlowdim2 29054  df-trkg2d 34856
[Schwabhauser] p. 13Axiom A8axtglowdim2 28563
[Schwabhauser] p. 13Axiom A9axtgupdim2 28564  df-trkg2d 34856
[Schwabhauser] p. 13Axiom A10axeuclid 29057  axtgeucl 28565  df-trkge 28544
[Schwabhauser] p. 13Axiom A11axcont 29070  axtgcont 28562  axtgcont1 28561  df-trkgb 28542
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36216
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36218
[Schwabhauser] p. 27Theorem 2.3cgrtr 36221
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36225
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36226  tgcgrcomimp 28570  tgcgrcoml 28572  tgcgrcomr 28571
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36231  tgcgrtriv 28577
[Schwabhauser] p. 28Theorem 2.105segofs 36235  tg5segofs 34864
[Schwabhauser] p. 28Definition 2.10df-afs 34861  df-ofs 36212
[Schwabhauser] p. 29Theorem 2.11cgrextend 36237  tgcgrextend 28578
[Schwabhauser] p. 29Theorem 2.12segconeq 36239  tgsegconeq 28579
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36251  btwntriv2 36241  tgbtwntriv2 28580
[Schwabhauser] p. 30Theorem 3.2btwncomim 36242  tgbtwncom 28581
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36245  tgbtwntriv1 28584
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36246  tgbtwnswapid 28585
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36252  btwnintr 36248  tgbtwnexch2 28589  tgbtwnintr 28586
[Schwabhauser] p. 30Theorem 3.6btwnexch 36254  btwnexch3 36249  tgbtwnexch 28591  tgbtwnexch3 28587
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36253  tgbtwnouttr 28590  tgbtwnouttr2 28588
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29053
[Schwabhauser] p. 32Theorem 3.14btwndiff 36256  tgbtwndiff 28599
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28592  trisegint 36257
[Schwabhauser] p. 34Theorem 4.2ifscgr 36273  tgifscgr 28601
[Schwabhauser] p. 34Theorem 4.11colcom 28651  colrot1 28652  colrot2 28653  lncom 28715  lnrot1 28716  lnrot2 28717
[Schwabhauser] p. 34Definition 4.1df-ifs 36269
[Schwabhauser] p. 35Theorem 4.3cgrsub 36274  tgcgrsub 28602
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36284  tgcgrxfr 28611
[Schwabhauser] p. 35Statement 4.4ercgrg 28610
[Schwabhauser] p. 35Definition 4.4df-cgr3 36270  df-cgrg 28604
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28604
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36285  tgbtwnxfr 28623
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36291  colinearperm2 36293  colinearperm3 36292  colinearperm4 36294  colinearperm5 36295
[Schwabhauser] p. 36Definition 4.8df-ismt 28626
[Schwabhauser] p. 36Definition 4.10df-colinear 36268  tgellng 28646  tglng 28639
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36296
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36304  lnxfr 28659
[Schwabhauser] p. 37Theorem 4.14lineext 36305  lnext 28660
[Schwabhauser] p. 37Theorem 4.16fscgr 36309  tgfscgr 28661
[Schwabhauser] p. 37Theorem 4.17linecgr 36310  lncgr 28662
[Schwabhauser] p. 37Definition 4.15df-fs 36271
[Schwabhauser] p. 38Theorem 4.18lineid 36312  lnid 28663
[Schwabhauser] p. 38Theorem 4.19idinside 36313  tgidinside 28664
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36330  tgbtwnconn1 28668
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36331  tgbtwnconn2 28669
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36332  tgbtwnconn3 28670
[Schwabhauser] p. 41Theorem 5.5brsegle2 36338
[Schwabhauser] p. 41Definition 5.4df-segle 36336  legov 28678
[Schwabhauser] p. 41Definition 5.5legov2 28679
[Schwabhauser] p. 42Remark 5.13legso 28692
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36339
[Schwabhauser] p. 42Theorem 5.7seglerflx 36341
[Schwabhauser] p. 42Theorem 5.8segletr 36343
[Schwabhauser] p. 42Theorem 5.9segleantisym 36344
[Schwabhauser] p. 42Theorem 5.10seglelin 36345
[Schwabhauser] p. 42Theorem 5.11seglemin 36342
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36347
[Schwabhauser] p. 42Proposition 5.7legid 28680
[Schwabhauser] p. 42Proposition 5.8legtrd 28682
[Schwabhauser] p. 42Proposition 5.9legtri3 28683
[Schwabhauser] p. 42Proposition 5.10legtrid 28684
[Schwabhauser] p. 42Proposition 5.11leg0 28685
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36354
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36355
[Schwabhauser] p. 43Theorem 6.4broutsideof 36350  df-outsideof 36349
[Schwabhauser] p. 43Definition 6.1broutsideof2 36351  ishlg 28695
[Schwabhauser] p. 44Theorem 6.4hlln 28700
[Schwabhauser] p. 44Theorem 6.5hlid 28702  outsideofrflx 36356
[Schwabhauser] p. 44Theorem 6.6hlcomb 28696  hlcomd 28697  outsideofcom 36357
[Schwabhauser] p. 44Theorem 6.7hltr 28703  outsideoftr 36358
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28711  outsideofeu 36360
[Schwabhauser] p. 44Definition 6.8df-ray 36367
[Schwabhauser] p. 45Part 2df-lines2 36368
[Schwabhauser] p. 45Theorem 6.13outsidele 36361
[Schwabhauser] p. 45Theorem 6.15lineunray 36376
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36377  tglineelsb2 28725
[Schwabhauser] p. 45Theorem 6.17linecom 36379  linerflx1 36378  linerflx2 36380  tglinecom 28728  tglinerflx1 28726  tglinerflx2 28727
[Schwabhauser] p. 45Theorem 6.18linethru 36382  tglinethru 28729
[Schwabhauser] p. 45Definition 6.14df-line2 36366  tglng 28639
[Schwabhauser] p. 45Proposition 6.13legbtwn 28687
[Schwabhauser] p. 46Theorem 6.19linethrueu 36385  tglinethrueu 28732
[Schwabhauser] p. 46Theorem 6.21lineintmo 36386  tglineineq 28736  tglineinteq 28738  tglineintmo 28735
[Schwabhauser] p. 46Theorem 6.23colline 28742
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28743
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28744
[Schwabhauser] p. 49Theorem 7.3mirinv 28759
[Schwabhauser] p. 49Theorem 7.7mirmir 28755
[Schwabhauser] p. 49Theorem 7.8mirreu3 28747
[Schwabhauser] p. 49Definition 7.5df-mir 28746  ismir 28752  mirbtwn 28751  mircgr 28750  mirfv 28749  mirval 28748
[Schwabhauser] p. 50Theorem 7.8mirreu 28757
[Schwabhauser] p. 50Theorem 7.9mireq 28758
[Schwabhauser] p. 50Theorem 7.10mirinv 28759
[Schwabhauser] p. 50Theorem 7.11mirf1o 28762
[Schwabhauser] p. 50Theorem 7.13miriso 28763
[Schwabhauser] p. 51Theorem 7.14mirmot 28768
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28765  mirbtwni 28764
[Schwabhauser] p. 51Theorem 7.16mircgrs 28766
[Schwabhauser] p. 51Theorem 7.17miduniq 28778
[Schwabhauser] p. 52Lemma 7.21symquadlem 28782
[Schwabhauser] p. 52Theorem 7.18miduniq1 28779
[Schwabhauser] p. 52Theorem 7.19miduniq2 28780
[Schwabhauser] p. 52Theorem 7.20colmid 28781
[Schwabhauser] p. 53Lemma 7.22krippen 28784
[Schwabhauser] p. 55Lemma 7.25midexlem 28785
[Schwabhauser] p. 57Theorem 8.2ragcom 28791
[Schwabhauser] p. 57Definition 8.1df-rag 28787  israg 28790
[Schwabhauser] p. 58Theorem 8.3ragcol 28792
[Schwabhauser] p. 58Theorem 8.4ragmir 28793
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28795
[Schwabhauser] p. 58Theorem 8.6ragflat2 28796
[Schwabhauser] p. 58Theorem 8.7ragflat 28797
[Schwabhauser] p. 58Theorem 8.8ragtriva 28798
[Schwabhauser] p. 58Theorem 8.9ragflat3 28799  ragncol 28802
[Schwabhauser] p. 58Theorem 8.10ragcgr 28800
[Schwabhauser] p. 59Theorem 8.12perpcom 28806
[Schwabhauser] p. 59Theorem 8.13ragperp 28810
[Schwabhauser] p. 59Theorem 8.14perpneq 28807
[Schwabhauser] p. 59Definition 8.11df-perpg 28789  isperp 28805
[Schwabhauser] p. 59Definition 8.13isperp2 28808
[Schwabhauser] p. 60Theorem 8.18foot 28815
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28823  colperpexlem2 28824
[Schwabhauser] p. 63Theorem 8.21colperpex 28826  colperpexlem3 28825
[Schwabhauser] p. 64Theorem 8.22mideu 28831  midex 28830
[Schwabhauser] p. 66Lemma 8.24opphllem 28828
[Schwabhauser] p. 67Theorem 9.2oppcom 28837
[Schwabhauser] p. 67Definition 9.1islnopp 28832
[Schwabhauser] p. 68Lemma 9.3opphllem2 28841
[Schwabhauser] p. 68Lemma 9.4opphllem5 28844  opphllem6 28845
[Schwabhauser] p. 69Theorem 9.5opphl 28847
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28560
[Schwabhauser] p. 70Theorem 9.6outpasch 28848
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28856
[Schwabhauser] p. 71Definition 9.7df-hpg 28851  hpgbr 28853
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28858
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28857
[Schwabhauser] p. 72Theorem 9.11hpgid 28859
[Schwabhauser] p. 72Theorem 9.12hpgcom 28860
[Schwabhauser] p. 72Theorem 9.13hpgtr 28861
[Schwabhauser] p. 73Theorem 9.18colopp 28862
[Schwabhauser] p. 73Theorem 9.19colhp 28863
[Schwabhauser] p. 88Theorem 10.2lmieu 28877
[Schwabhauser] p. 88Definition 10.1df-mid 28867
[Schwabhauser] p. 89Theorem 10.4lmicom 28881
[Schwabhauser] p. 89Theorem 10.5lmilmi 28882
[Schwabhauser] p. 89Theorem 10.6lmireu 28883
[Schwabhauser] p. 89Theorem 10.7lmieq 28884
[Schwabhauser] p. 89Theorem 10.8lmiinv 28885
[Schwabhauser] p. 89Theorem 10.9lmif1o 28888
[Schwabhauser] p. 89Theorem 10.10lmiiso 28890
[Schwabhauser] p. 89Definition 10.3df-lmi 28868
[Schwabhauser] p. 90Theorem 10.11lmimot 28891
[Schwabhauser] p. 91Theorem 10.12hypcgr 28894
[Schwabhauser] p. 92Theorem 10.14lmiopp 28895
[Schwabhauser] p. 92Theorem 10.15lnperpex 28896
[Schwabhauser] p. 92Theorem 10.16trgcopy 28897  trgcopyeu 28899
[Schwabhauser] p. 95Definition 11.2dfcgra2 28923
[Schwabhauser] p. 95Definition 11.3iscgra 28902
[Schwabhauser] p. 95Proposition 11.4cgracgr 28911
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28909  cgrahl2 28910
[Schwabhauser] p. 96Theorem 11.6cgraid 28912
[Schwabhauser] p. 96Theorem 11.9cgraswap 28913
[Schwabhauser] p. 97Theorem 11.7cgracom 28915
[Schwabhauser] p. 97Theorem 11.8cgratr 28916
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28919  cgrahl 28920
[Schwabhauser] p. 98Theorem 11.13sacgr 28924
[Schwabhauser] p. 98Theorem 11.14oacgr 28925
[Schwabhauser] p. 98Theorem 11.15acopy 28926  acopyeu 28927
[Schwabhauser] p. 101Theorem 11.24inagswap 28934
[Schwabhauser] p. 101Theorem 11.25inaghl 28938
[Schwabhauser] p. 101Definition 11.23isinag 28931
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28946
[Schwabhauser] p. 102Definition 11.27df-leag 28939  isleag 28940
[Schwabhauser] p. 107Theorem 11.49tgsas 28948  tgsas1 28947  tgsas2 28949  tgsas3 28950
[Schwabhauser] p. 108Theorem 11.50tgasa 28952  tgasa1 28951
[Schwabhauser] p. 109Theorem 11.51tgsss1 28953  tgsss2 28954  tgsss3 28955
[Shapiro] p. 230Theorem 6.5.1dchrhash 27259  dchrsum 27257  dchrsum2 27256  sumdchr 27260
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27261  sum2dchr 27262
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20041  ablfacrp2 20042
[Shapiro], p. 328Equation 9.2.4vmasum 27204
[Shapiro], p. 329Equation 9.2.7logfac2 27205
[Shapiro], p. 329Equation 9.2.9logfacrlim 27212
[Shapiro], p. 331Equation 9.2.13vmadivsum 27470
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27473
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27527  vmalogdivsum2 27526
[Shapiro], p. 375Theorem 9.4.1dirith 27517  dirith2 27516
[Shapiro], p. 375Equation 9.4.3rplogsum 27515  rpvmasum 27514  rpvmasum2 27500
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27475
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27513
[Shapiro], p. 377Lemma 9.4.1dchrisum 27480  dchrisumlem1 27477  dchrisumlem2 27478  dchrisumlem3 27479  dchrisumlema 27476
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27483
[Shapiro], p. 379Equation 9.4.16dchrmusum 27512  dchrmusumlem 27510  dchrvmasumlem 27511
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27482
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27484
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27508  dchrisum0re 27501  dchrisumn0 27509
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27494
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27498
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27499
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27554  pntrsumbnd2 27555  pntrsumo1 27553
[Shapiro], p. 405Equation 10.2.1mudivsum 27518
[Shapiro], p. 406Equation 10.2.6mulogsum 27520
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27522
[Shapiro], p. 407Equation 10.2.8mulog2sum 27525
[Shapiro], p. 418Equation 10.4.6logsqvma 27530
[Shapiro], p. 418Equation 10.4.8logsqvma2 27531
[Shapiro], p. 419Equation 10.4.10selberg 27536
[Shapiro], p. 420Equation 10.4.12selberg2lem 27538
[Shapiro], p. 420Equation 10.4.14selberg2 27539
[Shapiro], p. 422Equation 10.6.7selberg3 27547
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27548
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27545  selberg3lem2 27546
[Shapiro], p. 422Equation 10.4.23selberg4 27549
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27543
[Shapiro], p. 428Equation 10.6.2selbergr 27556
[Shapiro], p. 429Equation 10.6.8selberg3r 27557
[Shapiro], p. 430Equation 10.6.11selberg4r 27558
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27572
[Shapiro], p. 434Equation 10.6.27pntlema 27584  pntlemb 27585  pntlemc 27583  pntlemd 27582  pntlemg 27586
[Shapiro], p. 435Equation 10.6.29pntlema 27584
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27576
[Shapiro], p. 436Lemma 10.6.2pntibnd 27581
[Shapiro], p. 436Equation 10.6.34pntlema 27584
[Shapiro], p. 436Equation 10.6.35pntlem3 27597  pntleml 27599
[Stewart] p. 91Lemma 7.3constrss 33934
[Stewart] p. 92Definition 7.4.df-constr 33921
[Stewart] p. 96Theorem 7.10constraddcl 33953  constrinvcl 33964  constrmulcl 33962  constrnegcl 33954  constrsqrtcl 33970
[Stewart] p. 97Theorem 7.11constrextdg2 33940
[Stewart] p. 98Theorem 7.12constrext2chn 33950
[Stewart] p. 99Theorem 7.132sqr3nconstr 33972
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33982
[Stoll] p. 13Definition corresponds to dfsymdif3 4241
[Stoll] p. 16Exercise 4.40dif 4340  dif0 4313
[Stoll] p. 16Exercise 4.8difdifdir 4426
[Stoll] p. 17Theorem 5.1(5)unvdif 4410
[Stoll] p. 19Theorem 5.2(13)undm 4232
[Stoll] p. 19Theorem 5.2(13')indm 4233
[Stoll] p. 20Remarkinvdif 4214
[Stoll] p. 25Definition of ordered tripledf-ot 4571
[Stoll] p. 43Definitionuniiun 4995
[Stoll] p. 44Definitionintiin 4996
[Stoll] p. 45Definitiondf-iin 4931
[Stoll] p. 45Definition indexed uniondf-iun 4930
[Stoll] p. 176Theorem 3.4(27)iman 402
[Stoll] p. 262Example 4.1dfsymdif3 4241
[Strang] p. 242Section 6.3expgrowth 44780
[Suppes] p. 22Theorem 2eq0 4285  eq0f 4282
[Suppes] p. 22Theorem 4eqss 3937  eqssd 3939  eqssi 3938
[Suppes] p. 23Theorem 5ss0 4337  ss0b 4336
[Suppes] p. 23Theorem 6sstr 3930  sstrALT2 45279
[Suppes] p. 23Theorem 7pssirr 4041
[Suppes] p. 23Theorem 8pssn2lp 4042
[Suppes] p. 23Theorem 9psstr 4045
[Suppes] p. 23Theorem 10pssss 4036
[Suppes] p. 25Theorem 12elin 3906  elun 4090
[Suppes] p. 26Theorem 15inidm 4162
[Suppes] p. 26Theorem 16in0 4330
[Suppes] p. 27Theorem 23unidm 4094
[Suppes] p. 27Theorem 24un0 4329
[Suppes] p. 27Theorem 25ssun1 4114
[Suppes] p. 27Theorem 26ssequn1 4122
[Suppes] p. 27Theorem 27unss 4126
[Suppes] p. 27Theorem 28indir 4221
[Suppes] p. 27Theorem 29undir 4222
[Suppes] p. 28Theorem 32difid 4311
[Suppes] p. 29Theorem 33difin 4207
[Suppes] p. 29Theorem 34indif 4215
[Suppes] p. 29Theorem 35undif1 4411
[Suppes] p. 29Theorem 36difun2 4416
[Suppes] p. 29Theorem 37difin0 4409
[Suppes] p. 29Theorem 38disjdif 4407
[Suppes] p. 29Theorem 39difundi 4225
[Suppes] p. 29Theorem 40difindi 4227
[Suppes] p. 30Theorem 41nalset 5243
[Suppes] p. 39Theorem 61uniss 4853
[Suppes] p. 39Theorem 65uniop 5463
[Suppes] p. 41Theorem 70intsn 4921
[Suppes] p. 42Theorem 71intpr 4919  intprg 4918
[Suppes] p. 42Theorem 73op1stb 5418
[Suppes] p. 42Theorem 78intun 4917
[Suppes] p. 44Definition 15(a)dfiun2 4968  dfiun2g 4966
[Suppes] p. 44Definition 15(b)dfiin2 4969
[Suppes] p. 47Theorem 86elpw 4540  elpw2 5269  elpw2g 5268  elpwg 4539  elpwgdedVD 45361
[Suppes] p. 47Theorem 87pwid 4558
[Suppes] p. 47Theorem 89pw0 4750
[Suppes] p. 48Theorem 90pwpw0 4751
[Suppes] p. 52Theorem 101xpss12 5640
[Suppes] p. 52Theorem 102xpindi 5782  xpindir 5783
[Suppes] p. 52Theorem 103xpundi 5694  xpundir 5695
[Suppes] p. 54Theorem 105elirrv 9509
[Suppes] p. 58Theorem 2relss 5732
[Suppes] p. 59Theorem 4eldm 5849  eldm2 5850  eldm2g 5848  eldmg 5847
[Suppes] p. 59Definition 3df-dm 5635
[Suppes] p. 60Theorem 6dmin 5860
[Suppes] p. 60Theorem 8rnun 6103
[Suppes] p. 60Theorem 9rnin 6104
[Suppes] p. 60Definition 4dfrn2 5837
[Suppes] p. 61Theorem 11brcnv 5831  brcnvg 5828
[Suppes] p. 62Equation 5elcnv 5825  elcnv2 5826
[Suppes] p. 62Theorem 12relcnv 6063
[Suppes] p. 62Theorem 15cnvin 6102
[Suppes] p. 62Theorem 16cnvun 6100
[Suppes] p. 63Definitiondftrrels2 39027
[Suppes] p. 63Theorem 20co02 6219
[Suppes] p. 63Theorem 21dmcoss 5924
[Suppes] p. 63Definition 7df-co 5634
[Suppes] p. 64Theorem 26cnvco 5834
[Suppes] p. 64Theorem 27coass 6224
[Suppes] p. 65Theorem 31resundi 5952
[Suppes] p. 65Theorem 34elima 6024  elima2 6025  elima3 6026  elimag 6023
[Suppes] p. 65Theorem 35imaundi 6107
[Suppes] p. 66Theorem 40dminss 6111
[Suppes] p. 66Theorem 41imainss 6112
[Suppes] p. 67Exercise 11cnvxp 6115
[Suppes] p. 81Definition 34dfec2 8643
[Suppes] p. 82Theorem 72elec 8687  elecALTV 38639  elecg 8685
[Suppes] p. 82Theorem 73eqvrelth 39063  erth 8695  erth2 8696
[Suppes] p. 83Theorem 74eqvreldisj 39066  erdisj 8698
[Suppes] p. 83Definition 35, df-parts 39236  dfmembpart2 39241
[Suppes] p. 89Theorem 96map0b 8828
[Suppes] p. 89Theorem 97map0 8832  map0g 8829
[Suppes] p. 89Theorem 98mapsn 8833  mapsnd 8831
[Suppes] p. 89Theorem 99mapss 8834
[Suppes] p. 91Definition 12(ii)alephsuc 9988
[Suppes] p. 91Definition 12(iii)alephlim 9987
[Suppes] p. 92Theorem 1enref 8929  enrefg 8928
[Suppes] p. 92Theorem 2ensym 8947  ensymb 8946  ensymi 8948
[Suppes] p. 92Theorem 3entr 8950
[Suppes] p. 92Theorem 4unen 8989
[Suppes] p. 94Theorem 15endom 8923
[Suppes] p. 94Theorem 16ssdomg 8944
[Suppes] p. 94Theorem 17domtr 8951
[Suppes] p. 95Theorem 18sbth 9032
[Suppes] p. 97Theorem 23canth2 9065  canth2g 9066
[Suppes] p. 97Definition 3brsdom2 9036  df-sdom 8893  dfsdom2 9035
[Suppes] p. 97Theorem 21(i)sdomirr 9049
[Suppes] p. 97Theorem 22(i)domnsym 9038
[Suppes] p. 97Theorem 21(ii)sdomnsym 9037
[Suppes] p. 97Theorem 22(ii)domsdomtr 9047
[Suppes] p. 97Theorem 22(iv)brdom2 8926
[Suppes] p. 97Theorem 21(iii)sdomtr 9050
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9045
[Suppes] p. 98Exercise 4fundmen 8975  fundmeng 8976
[Suppes] p. 98Exercise 6xpdom3 9010
[Suppes] p. 98Exercise 11sdomentr 9046
[Suppes] p. 104Theorem 37fofi 9220
[Suppes] p. 104Theorem 38pwfi 9226
[Suppes] p. 105Theorem 40pwfi 9226
[Suppes] p. 111Axiom for cardinal numberscarden 10471
[Suppes] p. 130Definition 3df-tr 5187
[Suppes] p. 132Theorem 9ssonuni 7730
[Suppes] p. 134Definition 6df-suc 6323
[Suppes] p. 136Theorem Schema 22findes 7847  finds 7843  finds1 7846  finds2 7845
[Suppes] p. 151Theorem 42isfinite 9571  isfinite2 9205  isfiniteg 9207  unbnn 9203
[Suppes] p. 162Definition 5df-ltnq 10839  df-ltpq 10831
[Suppes] p. 197Theorem Schema 4tfindes 7810  tfinds 7807  tfinds2 7811
[Suppes] p. 209Theorem 18oaord1 8483
[Suppes] p. 209Theorem 21oaword2 8485
[Suppes] p. 211Theorem 25oaass 8493
[Suppes] p. 225Definition 8iscard2 9898
[Suppes] p. 227Theorem 56ondomon 10483
[Suppes] p. 228Theorem 59harcard 9900
[Suppes] p. 228Definition 12(i)aleph0 9986
[Suppes] p. 228Theorem Schema 61onintss 6369
[Suppes] p. 228Theorem Schema 62onminesb 7743  onminsb 7744
[Suppes] p. 229Theorem 64alephval2 10493
[Suppes] p. 229Theorem 65alephcard 9990
[Suppes] p. 229Theorem 66alephord2i 9997
[Suppes] p. 229Theorem 67alephnbtwn 9991
[Suppes] p. 229Definition 12df-aleph 9862
[Suppes] p. 242Theorem 6weth 10415
[Suppes] p. 242Theorem 8entric 10477
[Suppes] p. 242Theorem 9carden 10471
[Szendrei] p. 11Line 6df-cloneop 35925
[Szendrei] p. 11Paragraph 3df-suppos 35929
[TakeutiZaring] p. 8Axiom 1ax-ext 2712
[TakeutiZaring] p. 13Definition 4.5df-cleq 2732  wl-df.cleq 37871
[TakeutiZaring] p. 13Proposition 4.6df-clel 2815  wl-df.clel 37874
[TakeutiZaring] p. 13Proposition 4.9cvjust 2734
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2760
[TakeutiZaring] p. 14Definition 4.16df-oprab 7367
[TakeutiZaring] p. 14Proposition 4.14ru 3728
[TakeutiZaring] p. 15Axiom 2zfpair 5357
[TakeutiZaring] p. 15Exercise 1elpr 4587  elpr2 4589  elpr2g 4588  elprg 4585
[TakeutiZaring] p. 15Exercise 2elsn 4577  elsn2 4604  elsn2g 4603  elsng 4576  velsn 4578
[TakeutiZaring] p. 15Exercise 3elop 5414
[TakeutiZaring] p. 15Exercise 4sneq 4572  sneqr 4778
[TakeutiZaring] p. 15Definition 5.1dfpr2 4583  dfsn2 4575  dfsn2ALT 4584
[TakeutiZaring] p. 16Axiom 3uniex 7691
[TakeutiZaring] p. 16Exercise 6opth 5423
[TakeutiZaring] p. 16Exercise 7opex 5410
[TakeutiZaring] p. 16Exercise 8rext 5394
[TakeutiZaring] p. 16Corollary 5.8unex 7694  unexg 7693
[TakeutiZaring] p. 16Definition 5.3dftp2 4630
[TakeutiZaring] p. 16Definition 5.5df-uni 4846
[TakeutiZaring] p. 16Definition 5.6df-in 3897  df-un 3895
[TakeutiZaring] p. 16Proposition 5.7unipr 4862  uniprg 4861
[TakeutiZaring] p. 17Axiom 4vpwex 5313
[TakeutiZaring] p. 17Exercise 1eltp 4628
[TakeutiZaring] p. 17Exercise 5elsuc 6389  elsucg 6387  sstr2 3929
[TakeutiZaring] p. 17Exercise 6uncom 4095
[TakeutiZaring] p. 17Exercise 7incom 4145
[TakeutiZaring] p. 17Exercise 8unass 4108
[TakeutiZaring] p. 17Exercise 9inass 4163
[TakeutiZaring] p. 17Exercise 10indi 4219
[TakeutiZaring] p. 17Exercise 11undi 4220
[TakeutiZaring] p. 17Definition 5.9df-pss 3910  df-ss 3907
[TakeutiZaring] p. 17Definition 5.10df-pw 4538
[TakeutiZaring] p. 18Exercise 7unss2 4123
[TakeutiZaring] p. 18Exercise 9dfss2 3908  sseqin2 4159
[TakeutiZaring] p. 18Exercise 10ssid 3944
[TakeutiZaring] p. 18Exercise 12inss1 4172  inss2 4173
[TakeutiZaring] p. 18Exercise 13nss 3986
[TakeutiZaring] p. 18Exercise 15unieq 4856
[TakeutiZaring] p. 18Exercise 18sspwb 5395  sspwimp 45362  sspwimpALT 45369  sspwimpALT2 45372  sspwimpcf 45364
[TakeutiZaring] p. 18Exercise 19pweqb 5402
[TakeutiZaring] p. 19Axiom 5ax-rep 5206
[TakeutiZaring] p. 20Definitiondf-rab 3393
[TakeutiZaring] p. 20Corollary 5.160ex 5236
[TakeutiZaring] p. 20Definition 5.12df-dif 3893
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 36882  dfnul2 4271
[TakeutiZaring] p. 20Proposition 5.15difid 4311
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4288  n0f 4284  neq0 4287  neq0f 4283
[TakeutiZaring] p. 21Axiom 6zfreg 9508
[TakeutiZaring] p. 21Axiom 6'zfregs 9651
[TakeutiZaring] p. 21Theorem 5.22setind 9666
[TakeutiZaring] p. 21Definition 5.20df-v 3434
[TakeutiZaring] p. 21Proposition 5.21vprc 5249
[TakeutiZaring] p. 22Exercise 10ss 4335
[TakeutiZaring] p. 22Exercise 3ssex 5256  ssexg 5258
[TakeutiZaring] p. 22Exercise 4inex1 5252
[TakeutiZaring] p. 22Exercise 5ruv 9520
[TakeutiZaring] p. 22Exercise 6elirr 9512
[TakeutiZaring] p. 22Exercise 7ssdif0 4301
[TakeutiZaring] p. 22Exercise 11difdif 4072
[TakeutiZaring] p. 22Exercise 13undif3 4235  undif3VD 45326
[TakeutiZaring] p. 22Exercise 14difss 4073
[TakeutiZaring] p. 22Exercise 15sscon 4080
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3055
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3065
[TakeutiZaring] p. 23Proposition 6.2xpex 7703  xpexg 7700
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5632
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6563
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6739  fun11 6566
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6505  svrelfun 6564
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5836
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5838
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5637
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5638
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5634
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6152  dfrel2 6147
[TakeutiZaring] p. 25Exercise 3xpss 5641
[TakeutiZaring] p. 25Exercise 5relun 5761
[TakeutiZaring] p. 25Exercise 6reluni 5768
[TakeutiZaring] p. 25Exercise 9inxp 5781
[TakeutiZaring] p. 25Exercise 12relres 5964
[TakeutiZaring] p. 25Exercise 13opelres 5944  opelresi 5946
[TakeutiZaring] p. 25Exercise 14dmres 5971
[TakeutiZaring] p. 25Exercise 15resss 5960
[TakeutiZaring] p. 25Exercise 17resabs1 5965
[TakeutiZaring] p. 25Exercise 18funres 6534
[TakeutiZaring] p. 25Exercise 24relco 6067
[TakeutiZaring] p. 25Exercise 29funco 6532
[TakeutiZaring] p. 25Exercise 30f1co 6741
[TakeutiZaring] p. 26Definition 6.10eu2 2613
[TakeutiZaring] p. 26Definition 6.11conventions 30495  df-fv 6500  fv3 6852
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7872  cnvexg 7871
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7856  dmexg 7848
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7857  rnexg 7849
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44898
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7867
[TakeutiZaring] p. 27Corollary 6.13fvex 6847
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47638  tz6.12-1-afv2 47705  tz6.12-1 6857  tz6.12-afv 47637  tz6.12-afv2 47704  tz6.12 6858  tz6.12c-afv2 47706  tz6.12c 6856
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47701  tz6.12-2 6821  tz6.12i-afv2 47707  tz6.12i 6860
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6495
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6496
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6498  wfo 6490
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6497  wf1 6489
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6499  wf1o 6491
[TakeutiZaring] p. 28Exercise 4eqfnfv 6978  eqfnfv2 6979  eqfnfv2f 6982
[TakeutiZaring] p. 28Exercise 5fvco 6932
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7168
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7166
[TakeutiZaring] p. 29Exercise 9funimaex 6580  funimaexg 6579
[TakeutiZaring] p. 29Definition 6.18df-br 5080
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5534
[TakeutiZaring] p. 30Definition 6.21dffr2 5586  dffr3 6058  eliniseg 6053  iniseg 6056
[TakeutiZaring] p. 30Definition 6.22df-eprel 5525
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5602  fr3nr 7722  frirr 5601
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5578
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7724
[TakeutiZaring] p. 31Exercise 1frss 5589
[TakeutiZaring] p. 31Exercise 4wess 5611
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6305  tz6.26i 6306  wefrc 5619  wereu2 5622
[TakeutiZaring] p. 32Theorem 6.27wfi 6307  wfii 6308
[TakeutiZaring] p. 32Definition 6.28df-isom 6501
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7280
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7281
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7287
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7288
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7289
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7293
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7300
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7302
[TakeutiZaring] p. 35Notationwtr 5186
[TakeutiZaring] p. 35Theorem 7.2trelpss 44899  tz7.2 5608
[TakeutiZaring] p. 35Definition 7.1dftr3 5191
[TakeutiZaring] p. 36Proposition 7.4ordwe 6330
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6338
[TakeutiZaring] p. 36Proposition 7.6ordelord 6339  ordelordALT 44982  ordelordALTVD 45311
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6345  ordelssne 6344
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6343
[TakeutiZaring] p. 37Proposition 7.9ordin 6347
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7732
[TakeutiZaring] p. 38Corollary 7.15ordsson 7733
[TakeutiZaring] p. 38Definition 7.11df-on 6321
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6349
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44994  ordon 7727
[TakeutiZaring] p. 38Proposition 7.13onprc 7728
[TakeutiZaring] p. 39Theorem 7.17tfi 7800
[TakeutiZaring] p. 40Exercise 3ontr2 6365
[TakeutiZaring] p. 40Exercise 7dftr2 5188
[TakeutiZaring] p. 40Exercise 9onssmin 7742
[TakeutiZaring] p. 40Exercise 11unon 7778
[TakeutiZaring] p. 40Exercise 12ordun 6423
[TakeutiZaring] p. 40Exercise 14ordequn 6422
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7729
[TakeutiZaring] p. 40Proposition 7.20elssuni 4876
[TakeutiZaring] p. 41Definition 7.22df-suc 6323
[TakeutiZaring] p. 41Proposition 7.23sssucid 6399  sucidg 6400
[TakeutiZaring] p. 41Proposition 7.24onsuc 7760
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6413  ordnbtwn 6412
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7775
[TakeutiZaring] p. 42Exercise 1df-lim 6322
[TakeutiZaring] p. 42Exercise 4omssnlim 7828
[TakeutiZaring] p. 42Exercise 7ssnlim 7833
[TakeutiZaring] p. 42Exercise 8onsucssi 7788  ordelsuc 7767
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7769
[TakeutiZaring] p. 42Definition 7.27nlimon 7798
[TakeutiZaring] p. 42Definition 7.28dfom2 7815
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7836
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7837
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7838
[TakeutiZaring] p. 43Remarkomon 7825
[TakeutiZaring] p. 43Axiom 7inf3 9554  omex 9562
[TakeutiZaring] p. 43Theorem 7.32ordom 7823
[TakeutiZaring] p. 43Corollary 7.31find 7842
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7839
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7840
[TakeutiZaring] p. 44Exercise 1limomss 7818
[TakeutiZaring] p. 44Exercise 2int0 4899
[TakeutiZaring] p. 44Exercise 3trintss 5205
[TakeutiZaring] p. 44Exercise 4intss1 4900
[TakeutiZaring] p. 44Exercise 5intex 5279
[TakeutiZaring] p. 44Exercise 6oninton 7745
[TakeutiZaring] p. 44Exercise 11ordintdif 6368
[TakeutiZaring] p. 44Definition 7.35df-int 4885
[TakeutiZaring] p. 44Proposition 7.34noinfep 9579
[TakeutiZaring] p. 45Exercise 4onint 7740
[TakeutiZaring] p. 47Lemma 1tfrlem1 8312
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8333
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8334
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8335
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8342  tz7.44-2 8343  tz7.44-3 8344
[TakeutiZaring] p. 50Exercise 1smogt 8304
[TakeutiZaring] p. 50Exercise 3smoiso 8299
[TakeutiZaring] p. 50Definition 7.46df-smo 8283
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8381  tz7.49c 8382
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8379
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8378
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8380
[TakeutiZaring] p. 53Proposition 7.532eu5 2660
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9931
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9932
[TakeutiZaring] p. 56Definition 8.1oalim 8464  oasuc 8456
[TakeutiZaring] p. 57Remarktfindsg 7808
[TakeutiZaring] p. 57Proposition 8.2oacl 8467
[TakeutiZaring] p. 57Proposition 8.3oa0 8448  oa0r 8470
[TakeutiZaring] p. 57Proposition 8.16omcl 8468
[TakeutiZaring] p. 58Corollary 8.5oacan 8480
[TakeutiZaring] p. 58Proposition 8.4nnaord 8552  nnaordi 8551  oaord 8479  oaordi 8478
[TakeutiZaring] p. 59Proposition 8.6iunss2 4986  uniss2 4879
[TakeutiZaring] p. 59Proposition 8.7oawordri 8482
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8487  oawordex 8489
[TakeutiZaring] p. 59Proposition 8.9nnacl 8544
[TakeutiZaring] p. 59Proposition 8.10oaabs 8581
[TakeutiZaring] p. 60Remarkoancom 9570
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8492
[TakeutiZaring] p. 62Exercise 1nnarcl 8549
[TakeutiZaring] p. 62Exercise 5oaword1 8484
[TakeutiZaring] p. 62Definition 8.15om0x 8451  omlim 8465  omsuc 8458
[TakeutiZaring] p. 62Definition 8.15(a)om0 8449
[TakeutiZaring] p. 63Proposition 8.17nnecl 8546  nnmcl 8545
[TakeutiZaring] p. 63Proposition 8.19nnmord 8565  nnmordi 8564  omord 8500  omordi 8498
[TakeutiZaring] p. 63Proposition 8.20omcan 8501
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8569  omwordri 8504
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8471
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8474  om1r 8475
[TakeutiZaring] p. 64Proposition 8.22om00 8507
[TakeutiZaring] p. 64Proposition 8.23omordlim 8509
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8510
[TakeutiZaring] p. 64Proposition 8.25odi 8511
[TakeutiZaring] p. 65Theorem 8.26omass 8512
[TakeutiZaring] p. 67Definition 8.30nnesuc 8541  oe0 8454  oelim 8466  oesuc 8459  onesuc 8462
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8452
[TakeutiZaring] p. 67Proposition 8.32oen0 8519
[TakeutiZaring] p. 67Proposition 8.33oeordi 8520
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8453
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8477
[TakeutiZaring] p. 68Corollary 8.34oeord 8521
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8527
[TakeutiZaring] p. 68Proposition 8.35oewordri 8525
[TakeutiZaring] p. 68Proposition 8.37oeworde 8526
[TakeutiZaring] p. 69Proposition 8.41oeoa 8530
[TakeutiZaring] p. 70Proposition 8.42oeoe 8532
[TakeutiZaring] p. 73Theorem 9.1trcl 9647  tz9.1 9648
[TakeutiZaring] p. 76Definition 9.9df-r1 9686  r10 9690  r1lim 9694  r1limg 9693  r1suc 9692  r1sucg 9691
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9702  r1ord2 9703  r1ordg 9700
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9712
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9737  tz9.13 9713  tz9.13g 9714
[TakeutiZaring] p. 79Definition 9.14df-rank 9687  rankval 9738  rankvalb 9719  rankvalg 9739
[TakeutiZaring] p. 79Proposition 9.16rankel 9761  rankelb 9746
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9775  rankval3 9762  rankval3b 9748
[TakeutiZaring] p. 79Proposition 9.18rankonid 9751
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9717
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9756  rankr1c 9743  rankr1g 9754
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9757
[TakeutiZaring] p. 80Exercise 1rankss 9771  rankssb 9770
[TakeutiZaring] p. 80Exercise 2unbndrank 9764
[TakeutiZaring] p. 80Proposition 9.19bndrank 9763
[TakeutiZaring] p. 83Axiom of Choiceac4 10395  dfac3 10041
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9950  numth 10392  numth2 10391
[TakeutiZaring] p. 85Definition 10.4cardval 10466
[TakeutiZaring] p. 85Proposition 10.5cardid 10467  cardid2 9875
[TakeutiZaring] p. 85Proposition 10.9oncard 9882
[TakeutiZaring] p. 85Proposition 10.10carden 10471
[TakeutiZaring] p. 85Proposition 10.11cardidm 9881
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9866
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9887
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9879
[TakeutiZaring] p. 87Proposition 10.15pwen 9085
[TakeutiZaring] p. 88Exercise 1en0 8962
[TakeutiZaring] p. 88Exercise 7infensuc 9090
[TakeutiZaring] p. 89Exercise 10omxpen 9014
[TakeutiZaring] p. 90Corollary 10.23cardnn 9885
[TakeutiZaring] p. 90Definition 10.27alephiso 10018
[TakeutiZaring] p. 90Proposition 10.20nneneq 9137
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9145
[TakeutiZaring] p. 90Proposition 10.26alephprc 10019
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9142
[TakeutiZaring] p. 91Exercise 2alephle 10008
[TakeutiZaring] p. 91Exercise 3aleph0 9986
[TakeutiZaring] p. 91Exercise 4cardlim 9894
[TakeutiZaring] p. 91Exercise 7infpss 10136
[TakeutiZaring] p. 91Exercise 8infcntss 9230
[TakeutiZaring] p. 91Definition 10.29df-fin 8894  isfi 8919
[TakeutiZaring] p. 92Proposition 10.32onfin 9146
[TakeutiZaring] p. 92Proposition 10.34imadomg 10454
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9007
[TakeutiZaring] p. 93Proposition 10.35fodomb 10446
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10106  unxpdom 9166
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9896  cardsdomelir 9895
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9168
[TakeutiZaring] p. 94Proposition 10.39infxpen 9934
[TakeutiZaring] p. 95Definition 10.42df-map 8772
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10482  infxpidm2 9937
[TakeutiZaring] p. 95Proposition 10.41infdju 10127  infxp 10134
[TakeutiZaring] p. 96Proposition 10.44pw2en 9019  pw2f1o 9017
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9078
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10407
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10402  ac6s5 10411
[TakeutiZaring] p. 98Theorem 10.47unidom 10463
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10464  uniimadomf 10465
[TakeutiZaring] p. 100Definition 11.1cfcof 10194
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10189
[TakeutiZaring] p. 102Exercise 1cfle 10174
[TakeutiZaring] p. 102Exercise 2cf0 10171
[TakeutiZaring] p. 102Exercise 3cfsuc 10177
[TakeutiZaring] p. 102Exercise 4cfom 10184
[TakeutiZaring] p. 102Proposition 11.9coftr 10193
[TakeutiZaring] p. 103Theorem 11.15alephreg 10503
[TakeutiZaring] p. 103Proposition 11.11cardcf 10172
[TakeutiZaring] p. 103Proposition 11.13alephsing 10196
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10017
[TakeutiZaring] p. 104Proposition 11.16carduniima 10016
[TakeutiZaring] p. 104Proposition 11.18alephfp 10028  alephfp2 10029
[TakeutiZaring] p. 106Theorem 11.20gchina 10620
[TakeutiZaring] p. 106Theorem 11.21mappwen 10032
[TakeutiZaring] p. 107Theorem 11.26konigth 10490
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10504
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10505
[Tarski] p. 67Axiom B5ax-c5 39376
[Tarski] p. 67Scheme B5sp 2195
[Tarski] p. 68Lemma 6avril1 30558  equid 2019
[Tarski] p. 69Lemma 7equcomi 2024
[Tarski] p. 70Lemma 14spim 2395  spime 2397  spimew 1978
[Tarski] p. 70Lemma 16ax-12 2189  ax-c15 39382  ax12i 1973
[Tarski] p. 70Lemmas 16 and 17sb6 2096
[Tarski] p. 75Axiom B7ax6v 1975
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1917  ax5ALT 39400
[Tarski], p. 75Scheme B8 of system S2ax-7 2015  ax-8 2121  ax-9 2129
[Tarski1999] p. 178Axiom 4axtgsegcon 28557
[Tarski1999] p. 178Axiom 5axtg5seg 28558
[Tarski1999] p. 179Axiom 7axtgpasch 28560
[Tarski1999] p. 180Axiom 7.1axtgpasch 28560
[Tarski1999] p. 185Axiom 11axtgcont1 28561
[Truss] p. 114Theorem 5.18ruc 16208
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38027
[Viaclovsky8] p. 3Proposition 7ismblfin 38029
[Weierstrass] p. 272Definitiondf-mdet 22575  mdetuni 22612
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 909
[WhiteheadRussell] p. 96Axiom *1.3olc 874
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 875
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 925
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 975
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 189
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 37808
[WhiteheadRussell] p. 100Theorem *2.05frege5 44245  imim2 58  wl-luk-imim2 37803
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47483  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 902
[WhiteheadRussell] p. 101Theorem *2.06barbara 2667  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 908
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37806
[WhiteheadRussell] p. 101Theorem *2.11exmid 900
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 903
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 45371  wl-luk-notnotr 37807
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44275  axfrege28 44274  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 873
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 930
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37800
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 895
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 947
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30496  pm2.27 42  wl-luk-pm2.27 37798
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 928
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38739
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 929
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 977
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 978
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 976
[WhiteheadRussell] p. 105Definition *2.33df-3or 1093
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 912
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 913
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 950
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 887
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 888
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 192
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 889
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 890
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 891
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 857
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 858
[WhiteheadRussell] p. 107Theorem *2.55orel1 894
[WhiteheadRussell] p. 107Theorem *2.56orel2 896
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 193
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 905
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 948
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 949
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 194
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 897  pm2.67 898
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 904
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 980
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 906
[WhiteheadRussell] p. 108Theorem *2.69looinv 204
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 981
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 982
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 939
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 937
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 979
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 983
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 938
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 999
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 470  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1000
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1001
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1002
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1003
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 472
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 460
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 403
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 808
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 449
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 450
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 483  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 485  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 770
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 771
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 813
[WhiteheadRussell] p. 113Fact)pm3.45 628
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 815
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 493
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 494
[WhiteheadRussell] p. 113Theorem *3.44jao 968  pm3.44 967
[WhiteheadRussell] p. 113Theorem *3.47anim12 814
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 474
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 971
[WhiteheadRussell] p. 116Theorem *4.1con34b 317
[WhiteheadRussell] p. 117Theorem *4.2biid 262
[WhiteheadRussell] p. 117Theorem *4.11notbi 320
[WhiteheadRussell] p. 117Theorem *4.12con2bi 354
[WhiteheadRussell] p. 117Theorem *4.13notnotb 316
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 812
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 838
[WhiteheadRussell] p. 117Theorem *4.21bicom 223
[WhiteheadRussell] p. 117Theorem *4.22biantr 811  bitr 810
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 568
[WhiteheadRussell] p. 117Theorem *4.25oridm 910  pm4.25 911
[WhiteheadRussell] p. 118Theorem *4.3ancom 461
[WhiteheadRussell] p. 118Theorem *4.4andi 1015
[WhiteheadRussell] p. 118Theorem *4.31orcom 876
[WhiteheadRussell] p. 118Theorem *4.32anass 469
[WhiteheadRussell] p. 118Theorem *4.33orass 927
[WhiteheadRussell] p. 118Theorem *4.36anbi1 639
[WhiteheadRussell] p. 118Theorem *4.37orbi1 923
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 643
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 984
[WhiteheadRussell] p. 118Definition *4.34df-3an 1094
[WhiteheadRussell] p. 119Theorem *4.41ordi 1013
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1059
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1030
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1004
[WhiteheadRussell] p. 119Theorem *4.45orabs 1006  pm4.45 1005  pm4.45im 833
[WhiteheadRussell] p. 120Theorem *4.5anor 990
[WhiteheadRussell] p. 120Theorem *4.6imor 859
[WhiteheadRussell] p. 120Theorem *4.7anclb 550
[WhiteheadRussell] p. 120Theorem *4.51ianor 989
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 992
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 993
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 994
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 995
[WhiteheadRussell] p. 120Theorem *4.56ioran 991  pm4.56 996
[WhiteheadRussell] p. 120Theorem *4.57oran 997  pm4.57 998
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 405
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 862
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 398
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 855
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 406
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 856
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 399
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 562  pm4.71d 566  pm4.71i 564  pm4.71r 563  pm4.71rd 567  pm4.71ri 565
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 957
[WhiteheadRussell] p. 121Theorem *4.73iba 532
[WhiteheadRussell] p. 121Theorem *4.74biorf 942
[WhiteheadRussell] p. 121Theorem *4.76jcab 522  pm4.76 523
[WhiteheadRussell] p. 121Theorem *4.77jaob 969  pm4.77 970
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 940
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1011
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 393
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 394
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1031
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1032
[WhiteheadRussell] p. 122Theorem *4.84imbi1 348
[WhiteheadRussell] p. 122Theorem *4.85imbi2 349
[WhiteheadRussell] p. 122Theorem *4.86bibi1 352
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 388  impexp 451  pm4.87 849
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 829
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 952  pm5.11g 951
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 953
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 955
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 954
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1020
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1021
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1019
[WhiteheadRussell] p. 124Theorem *5.18nbbn 384  pm5.18 382
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 387
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 830
[WhiteheadRussell] p. 124Theorem *5.22xor 1022
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1055
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1056
[WhiteheadRussell] p. 124Theorem *5.25dfor2 907
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 577
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 389
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 362
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1009
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 961
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 836
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 578
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 841
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 831
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 839
[WhiteheadRussell] p. 125Theorem *5.41imdi 390  pm5.41 391
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 548
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 547
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1012
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1025
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 956
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1008
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1026
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1027
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1035
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 367
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 271
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1036
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 36933
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44803
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44804
[WhiteheadRussell] p. 147Theorem *10.2219.26 1877
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44805
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44806
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44807
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1900
[WhiteheadRussell] p. 151Theorem *10.301albitr 44808
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44809
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44810
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44811
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44812
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44814
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44815
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44816
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44813
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2101
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44819
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44820
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2081
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2171
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1836
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1837
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44821
[WhiteheadRussell] p. 162Theorem *11.322alim 44822
[WhiteheadRussell] p. 162Theorem *11.332albi 44823
[WhiteheadRussell] p. 162Theorem *11.342exim 44824
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44826
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44825
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1894
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44828
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44829
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44827
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1835
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44830
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44831
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1853
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44832
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2354
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1867
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44837
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44833
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44834
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44835
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44836
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44841
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44838
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44839
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44840
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44842
[WhiteheadRussell] p. 175Definition *14.02df-eu 2573
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44852  pm13.13b 44853
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44854
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3016
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3017
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3611
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44860
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44861
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44855
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44997  pm13.193 44856
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44857
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44858
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44859
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44866
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44865
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44864
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3792
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44867  pm14.122b 44868  pm14.122c 44869
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44870  pm14.123b 44871  pm14.123c 44872
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44874
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44873
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44875
[WhiteheadRussell] p. 190Theorem *14.22iota4 6473
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44876
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6474
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44877
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44879
[WhiteheadRussell] p. 192Theorem *14.26eupick 2637  eupickbi 2640  sbaniota 44880
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44878
[WhiteheadRussell] p. 192Theorem *14.271eubi 2588
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44881
[WhiteheadRussell] p. 235Definition *30.01conventions 30495  df-fv 6500
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9923  pm54.43lem 9922
[Young] p. 141Definition of operator orderingleop2 32220
[Young] p. 142Example 12.2(i)0leop 32226  idleop 32227
[vandenDries] p. 42Lemma 61irrapx1 43274
[vandenDries] p. 43Theorem 62pellex 43281  pellexlem1 43275

This page was last updated on 27-May-2026.
Copyright terms: Public domain