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 17760
[Adamek] p. 21Condition 3.1(b)df-cat 17760
[Adamek] p. 22Example 3.3(1)df-setc 18169
[Adamek] p. 24Example 3.3(4.c)0cat 17781  0funcg 50013  df-termc 50401
[Adamek] p. 24Example 3.3(4.d)df-prstc 50478  prsthinc 50392
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50506  df-mndtc 50506
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50502
[Adamek] p. 25Definition 3.5df-oppc 17804
[Adamek] p. 25Example 3.6(1)oduoppcciso 50494
[Adamek] p. 25Example 3.6(2)oppgoppcco 50519  oppgoppchom 50518  oppgoppcid 50520
[Adamek] p. 28Remark 3.9oppciso 17874
[Adamek] p. 28Remark 3.12invf1o 17862  invisoinvl 17883
[Adamek] p. 28Example 3.13idinv 17882  idiso 17881
[Adamek] p. 28Corollary 3.11inveq 17867
[Adamek] p. 28Definition 3.8df-inv 17841  df-iso 17842  dfiso2 17865
[Adamek] p. 28Proposition 3.10sectcan 17848
[Adamek] p. 29Remark 3.16cicer 17899  cicerALT 49974
[Adamek] p. 29Definition 3.15cic 17892  df-cic 17889
[Adamek] p. 29Definition 3.17df-func 17951
[Adamek] p. 29Proposition 3.14(1)invinv 17863
[Adamek] p. 29Proposition 3.14(2)invco 17864  isoco 17870
[Adamek] p. 30Remark 3.19df-func 17951
[Adamek] p. 30Example 3.20(1)idfucl 17974
[Adamek] p. 30Example 3.20(2)diag1 50232
[Adamek] p. 32Proposition 3.21funciso 17967
[Adamek] p. 33Example 3.26(1)discsnterm 50502  discthing 50389
[Adamek] p. 33Example 3.26(2)df-thinc 50346  prsthinc 50392  thincciso 50381  thincciso2 50383  thincciso3 50384  thinccisod 50382
[Adamek] p. 33Example 3.26(3)df-mndtc 50506
[Adamek] p. 33Proposition 3.23cofucl 17981  cofucla 50024
[Adamek] p. 34Remark 3.28(1)cofidfth 50090
[Adamek] p. 34Remark 3.28(2)catciso 18204  catcisoi 50328
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18259
[Adamek] p. 34Definition 3.27(2)df-fth 18000
[Adamek] p. 34Definition 3.27(3)df-full 17999
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18259
[Adamek] p. 35Corollary 3.32ffthiso 18024
[Adamek] p. 35Proposition 3.30(c)cofth 18030
[Adamek] p. 35Proposition 3.30(d)cofull 18029
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18244
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18244
[Adamek] p. 39Remark 3.422oppf 50060
[Adamek] p. 39Definition 3.41df-oppf 50051  funcoppc 17968
[Adamek] p. 39Definition 3.44.df-catc 18192  elcatchom 50325
[Adamek] p. 39Proposition 3.43(c)fthoppc 18018  fthoppf 50092
[Adamek] p. 39Proposition 3.43(d)fulloppc 18017  fulloppf 50091
[Adamek] p. 40Remark 3.48catccat 18201
[Adamek] p. 40Definition 3.470funcg 50013  df-catc 18192
[Adamek] p. 45Exercise 3Gincat 50529
[Adamek] p. 48Remark 4.2(2)cnelsubc 50532  nelsubc3 49999
[Adamek] p. 48Remark 4.2(3)imasubc 50079  imasubc2 50080  imasubc3 50084
[Adamek] p. 48Example 4.3(1.a)0subcat 17931
[Adamek] p. 48Example 4.3(1.b)catsubcat 17932
[Adamek] p. 48Definition 4.1(1)nelsubc3 49999
[Adamek] p. 48Definition 4.1(2)fullsubc 17943
[Adamek] p. 48Definition 4.1(a)df-subc 17905
[Adamek] p. 49Remark 4.4idsubc 50088
[Adamek] p. 49Remark 4.4(1)idemb 50087
[Adamek] p. 49Remark 4.4(2)idfullsubc 50089  ressffth 18033
[Adamek] p. 58Exercise 4Asetc1onsubc 50530
[Adamek] p. 83Definition 6.1df-nat 18039
[Adamek] p. 87Remark 6.14(a)fuccocl 18060
[Adamek] p. 87Remark 6.14(b)fucass 18064
[Adamek] p. 87Definition 6.15df-fuc 18040
[Adamek] p. 88Remark 6.16fuccat 18066
[Adamek] p. 101Definition 7.10funcg 50013  df-inito 18077
[Adamek] p. 101Example 7.2(3)0funcg 50013  df-termc 50401  initc 50019
[Adamek] p. 101Example 7.2 (6)irinitoringc 21696
[Adamek] p. 102Definition 7.4df-termo 18078  oppctermo 50164
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18105
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18109
[Adamek] p. 103Remark 7.8oppczeroo 50165
[Adamek] p. 103Definition 7.7df-zeroo 18079
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21697
[Adamek] p. 103Proposition 7.6termoeu1w 18112
[Adamek] p. 106Definition 7.19df-sect 17840
[Adamek] p. 107Example 7.20(7)thincinv 50397
[Adamek] p. 108Example 7.25(4)thincsect2 50396
[Adamek] p. 110Example 7.33(9)thincmon 50361
[Adamek] p. 110Proposition 7.35sectmon 17875
[Adamek] p. 112Proposition 7.42sectepi 17877
[Adamek] p. 185Section 10.67updjud 9942
[Adamek] p. 193Definition 11.1(1)df-lmd 50573
[Adamek] p. 193Definition 11.3(1)df-lmd 50573
[Adamek] p. 194Definition 11.3(2)df-lmd 50573
[Adamek] p. 202Definition 11.27(1)df-cmd 50574
[Adamek] p. 202Definition 11.27(2)df-cmd 50574
[Adamek] p. 478Item Rngdf-ringc 20812
[AhoHopUll] p. 2Section 1.1df-bigo 49480
[AhoHopUll] p. 12Section 1.3df-blen 49502
[AhoHopUll] p. 318Section 9.1df-concat 14638  df-pfx 14743  df-substr 14711  df-word 14581  lencl 14600  wrd0 14606
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24938  df-nmoo 31227
[AkhiezerGlazman] p. 64Theoremhmopidmch 32635  hmopidmchi 32633
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32683  pjcmul2i 32684
[AkhiezerGlazman] p. 72Theoremcnvunop 32400  unoplin 32402
[AkhiezerGlazman] p. 72Equation 2unopadj 32401  unopadj2 32420
[AkhiezerGlazman] p. 73Theoremelunop2 32495  lnopunii 32494
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32568
[Alling] p. 125Theorem 4.02(12)cofcutrtime 28193
[Alling] p. 184Axiom Bbdayfo 27914
[Alling] p. 184Axiom Oltsso 27913
[Alling] p. 184Axiom SDnodense 27929
[Alling] p. 185Lemma 0nocvxmin 28021
[Alling] p. 185Theoremconway 28045
[Alling] p. 185Axiom FEnoeta 27980
[Alling] p. 186Theorem 4lesrec 28065  lesrecd 28066
[Alling], p. 2Definitionrp-brsslt 44265
[Alling], p. 3Notenla0001 44268  nla0002 44266  nla0003 44267
[Apostol] p. 18Theorem I.1addcan 11421  addcan2d 11441  addcan2i 11431  addcand 11440  addcani 11430
[Apostol] p. 18Theorem I.2negeu 11474
[Apostol] p. 18Theorem I.3negsub 11533  negsubd 11602  negsubi 11563
[Apostol] p. 18Theorem I.4negneg 11535  negnegd 11587  negnegi 11555
[Apostol] p. 18Theorem I.5subdi 11674  subdid 11697  subdii 11690  subdir 11675  subdird 11698  subdiri 11691
[Apostol] p. 18Theorem I.6mul01 11416  mul01d 11436  mul01i 11427  mul02 11415  mul02d 11435  mul02i 11426
[Apostol] p. 18Theorem I.7mulcan 11878  mulcan2d 11875  mulcand 11874  mulcani 11880
[Apostol] p. 18Theorem I.8receu 11886  xreceu 33369
[Apostol] p. 18Theorem I.9divrec 11915  divrecd 12021  divreci 11987  divreczi 11980
[Apostol] p. 18Theorem I.10recrec 11939  recreci 11974
[Apostol] p. 18Theorem I.11mul0or 11881  mul0ord 11889  mul0ori 11888
[Apostol] p. 18Theorem I.12mul2neg 11680  mul2negd 11696  mul2negi 11689  mulneg1 11677  mulneg1d 11694  mulneg1i 11687
[Apostol] p. 18Theorem I.13divadddiv 11957  divadddivd 12062  divadddivi 12004
[Apostol] p. 18Theorem I.14divmuldiv 11942  divmuldivd 12059  divmuldivi 12002  rdivmuldivd 20558
[Apostol] p. 18Theorem I.15divdivdiv 11943  divdivdivd 12065  divdivdivi 12005
[Apostol] p. 20Axiom 7rpaddcl 13068  rpaddcld 13103  rpmulcl 13069  rpmulcld 13104
[Apostol] p. 20Axiom 8rpneg 13078
[Apostol] p. 20Axiom 90nrp 13081
[Apostol] p. 20Theorem I.17lttri 11363
[Apostol] p. 20Theorem I.18ltadd1d 11834  ltadd1dd 11852  ltadd1i 11795
[Apostol] p. 20Theorem I.19ltmul1 12092  ltmul1a 12091  ltmul1i 12160  ltmul1ii 12170  ltmul2 12093  ltmul2d 13130  ltmul2dd 13144  ltmul2i 12163
[Apostol] p. 20Theorem I.20msqgt0 11761  msqgt0d 11808  msqgt0i 11778
[Apostol] p. 20Theorem I.210lt1 11763
[Apostol] p. 20Theorem I.23lt0neg1 11747  lt0neg1d 11810  ltneg 11741  ltnegd 11819  ltnegi 11785
[Apostol] p. 20Theorem I.25lt2add 11726  lt2addd 11864  lt2addi 11803
[Apostol] p. 20Definition of positive numbersdf-rp 13045
[Apostol] p. 21Exercise 4recgt0 12088  recgt0d 12176  recgt0i 12147  recgt0ii 12148
[Apostol] p. 22Definition of integersdf-z 12619
[Apostol] p. 22Definition of positive integersdfnn3 12274
[Apostol] p. 22Definition of rationalsdf-q 13001
[Apostol] p. 24Theorem I.26supeu 9427
[Apostol] p. 26Theorem I.28nnunb 12527
[Apostol] p. 26Theorem I.29arch 12528  archd 45996
[Apostol] p. 28Exercise 2btwnz 12727
[Apostol] p. 28Exercise 3nnrecl 12529
[Apostol] p. 28Exercise 4rebtwnz 12999
[Apostol] p. 28Exercise 5zbtwnre 12998
[Apostol] p. 28Exercise 6qbtwnre 13253
[Apostol] p. 28Exercise 10(a)zeneo 16433  zneo 12707  zneoALTV 48587
[Apostol] p. 29Theorem I.35cxpsqrtth 26968  msqsqrtd 15532  resqrtth 15344  sqrtth 15454  sqrtthi 15460  sqsqrtd 15531
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12263
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12965
[Apostol] p. 361Remarkcrreczi 14294
[Apostol] p. 363Remarkabsgt0i 15489
[Apostol] p. 363Exampleabssubd 15545  abssubi 15493
[ApostolNT] p. 7Remarkfmtno0 48445  fmtno1 48446  fmtno2 48455  fmtno3 48456  fmtno4 48457  fmtno5fac 48487  fmtnofz04prm 48482
[ApostolNT] p. 7Definitiondf-fmtno 48433
[ApostolNT] p. 8Definitiondf-ppi 27337
[ApostolNT] p. 14Definitiondf-dvds 16347
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16363
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16388
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16383
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16376
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16378
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16364
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16365
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16370
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16405
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16407
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16409
[ApostolNT] p. 15Definitiondf-gcd 16589  dfgcd2 16640
[ApostolNT] p. 16Definitionisprm2 16776
[ApostolNT] p. 16Theorem 1.5coprmdvds 16747
[ApostolNT] p. 16Theorem 1.7prminf 17011
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16607
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16641
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16643
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16622
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16614
[ApostolNT] p. 17Theorem 1.8coprm 16806
[ApostolNT] p. 17Theorem 1.9euclemma 16808
[ApostolNT] p. 17Theorem 1.101arith2 17024
[ApostolNT] p. 18Theorem 1.13prmrec 17018
[ApostolNT] p. 19Theorem 1.14divalg 16497
[ApostolNT] p. 20Theorem 1.15eucalg 16681
[ApostolNT] p. 24Definitiondf-mu 27338
[ApostolNT] p. 25Definitiondf-phi 16861
[ApostolNT] p. 25Theorem 2.1musum 27428
[ApostolNT] p. 26Theorem 2.2phisum 16886
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16871
[ApostolNT] p. 28Theorem 2.5(c)phimul 16875
[ApostolNT] p. 32Definitiondf-vma 27335
[ApostolNT] p. 32Theorem 2.9muinv 27430
[ApostolNT] p. 32Theorem 2.10vmasum 27453
[ApostolNT] p. 38Remarkdf-sgm 27339
[ApostolNT] p. 38Definitiondf-sgm 27339
[ApostolNT] p. 75Definitiondf-chp 27336  df-cht 27334
[ApostolNT] p. 104Definitioncongr 16758
[ApostolNT] p. 106Remarkdvdsval3 16350
[ApostolNT] p. 106Definitionmoddvds 16357
[ApostolNT] p. 107Example 2mod2eq0even 16440
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16441
[ApostolNT] p. 107Example 4zmod1congr 13951
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13991
[ApostolNT] p. 107Theorem 5.2(c)modexp 14304
[ApostolNT] p. 108Theorem 5.3modmulconst 16382
[ApostolNT] p. 109Theorem 5.4cncongr1 16761
[ApostolNT] p. 109Theorem 5.6gcdmodi 17170
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16763
[ApostolNT] p. 113Theorem 5.17eulerth 16878
[ApostolNT] p. 113Theorem 5.18vfermltl 16897
[ApostolNT] p. 114Theorem 5.19fermltl 16879
[ApostolNT] p. 116Theorem 5.24wilthimp 27309
[ApostolNT] p. 179Definitiondf-lgs 27532  lgsprme0 27576
[ApostolNT] p. 180Example 11lgs 27577
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27553
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27568
[ApostolNT] p. 181Theorem 9.4m1lgs 27625
[ApostolNT] p. 181Theorem 9.52lgs 27644  2lgsoddprm 27653
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27611
[ApostolNT] p. 185Theorem 9.8lgsquad 27620
[ApostolNT] p. 188Definitiondf-lgs 27532  lgs1 27578
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27569
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27571
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27579
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27580
[Baer] p. 40Property (b)mapdord 42513
[Baer] p. 40Property (c)mapd11 42514
[Baer] p. 40Property (e)mapdin 42537  mapdlsm 42539
[Baer] p. 40Property (f)mapd0 42540
[Baer] p. 40Definition of projectivitydf-mapd 42500  mapd1o 42523
[Baer] p. 41Property (g)mapdat 42542
[Baer] p. 44Part (1)mapdpg 42581
[Baer] p. 45Part (2)hdmap1eq 42676  mapdheq 42603  mapdheq2 42604  mapdheq2biN 42605
[Baer] p. 45Part (3)baerlem3 42588
[Baer] p. 46Part (4)mapdheq4 42607  mapdheq4lem 42606
[Baer] p. 46Part (5)baerlem5a 42589  baerlem5abmN 42593  baerlem5amN 42591  baerlem5b 42590  baerlem5bmN 42592
[Baer] p. 47Part (6)hdmap1l6 42696  hdmap1l6a 42684  hdmap1l6e 42689  hdmap1l6f 42690  hdmap1l6g 42691  hdmap1l6lem1 42682  hdmap1l6lem2 42683  mapdh6N 42622  mapdh6aN 42610  mapdh6eN 42615  mapdh6fN 42616  mapdh6gN 42617  mapdh6lem1N 42608  mapdh6lem2N 42609
[Baer] p. 48Part 9hdmapval 42703
[Baer] p. 48Part 10hdmap10 42715
[Baer] p. 48Part 11hdmapadd 42718
[Baer] p. 48Part (6)hdmap1l6h 42692  mapdh6hN 42618
[Baer] p. 48Part (7)mapdh75cN 42628  mapdh75d 42629  mapdh75e 42627  mapdh75fN 42630  mapdh7cN 42624  mapdh7dN 42625  mapdh7eN 42623  mapdh7fN 42626
[Baer] p. 48Part (8)mapdh8 42663  mapdh8a 42650  mapdh8aa 42651  mapdh8ab 42652  mapdh8ac 42653  mapdh8ad 42654  mapdh8b 42655  mapdh8c 42656  mapdh8d 42658  mapdh8d0N 42657  mapdh8e 42659  mapdh8g 42660  mapdh8i 42661  mapdh8j 42662
[Baer] p. 48Part (9)mapdh9a 42664
[Baer] p. 48Equation 10mapdhvmap 42644
[Baer] p. 49Part 12hdmap11 42723  hdmapeq0 42719  hdmapf1oN 42740  hdmapneg 42721  hdmaprnN 42739  hdmaprnlem1N 42724  hdmaprnlem3N 42725  hdmaprnlem3uN 42726  hdmaprnlem4N 42728  hdmaprnlem6N 42729  hdmaprnlem7N 42730  hdmaprnlem8N 42731  hdmaprnlem9N 42732  hdmapsub 42722
[Baer] p. 49Part 14hdmap14lem1 42743  hdmap14lem10 42752  hdmap14lem1a 42741  hdmap14lem2N 42744  hdmap14lem2a 42742  hdmap14lem3 42745  hdmap14lem8 42750  hdmap14lem9 42751
[Baer] p. 50Part 14hdmap14lem11 42753  hdmap14lem12 42754  hdmap14lem13 42755  hdmap14lem14 42756  hdmap14lem15 42757  hgmapval 42762
[Baer] p. 50Part 15hgmapadd 42769  hgmapmul 42770  hgmaprnlem2N 42772  hgmapvs 42766
[Baer] p. 50Part 16hgmaprnN 42776
[Baer] p. 110Lemma 1hdmapip0com 42792
[Baer] p. 110Line 27hdmapinvlem1 42793
[Baer] p. 110Line 28hdmapinvlem2 42794
[Baer] p. 110Line 30hdmapinvlem3 42795
[Baer] p. 110Part 1.2hdmapglem5 42797  hgmapvv 42801
[Baer] p. 110Proposition 1hdmapinvlem4 42796
[Baer] p. 111Line 10hgmapvvlem1 42798
[Baer] p. 111Line 15hdmapg 42805  hdmapglem7 42804
[Bauer], p. 483Theorem 1.22irrexpq 26969  2irrexpqALT 27038
[BellMachover] p. 36Lemma 10.3idALT 24
[BellMachover] p. 97Definition 10.1df-eu 2596
[BellMachover] p. 460Notationdf-mo 2566
[BellMachover] p. 460Definitionmo3 2591
[BellMachover] p. 461Axiom Extax-ext 2734
[BellMachover] p. 462Theorem 1.1axextmo 2738
[BellMachover] p. 463Axiom Repaxrep5 5244
[BellMachover] p. 463Scheme Sepax-sep 5255
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37810  sepex 5261
[BellMachover] p. 466Problemaxpow2 5336
[BellMachover] p. 466Axiom Powaxpow3 5337
[BellMachover] p. 466Axiom Unionaxun2 7741
[BellMachover] p. 468Definitiondf-ord 6364
[BellMachover] p. 469Theorem 2.2(i)ordirr 6379
[BellMachover] p. 469Theorem 2.2(iii)onelon 6386  onelond 36781
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6381
[BellMachover] p. 471Definition of Ndf-om 7866
[BellMachover] p. 471Problem 2.5(ii)uniordint 7803
[BellMachover] p. 471Definition of Limdf-lim 6366
[BellMachover] p. 472Axiom Infzfinf2 9624
[BellMachover] p. 473Theorem 2.8limom 7881
[BellMachover] p. 477Equation 3.1df-r1 9749
[BellMachover] p. 478Definitionrankval2 9803  rankval2b 35608
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9767  r1ord3g 9764
[BellMachover] p. 480Axiom Regzfreg 9571
[BellMachover] p. 488Axiom ACac5 10482  dfac4 10128
[BellMachover] p. 490Definition of alephalephval3 10116
[BeltramettiCassinelli] p. 98Remarkatlatmstc 40194
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32835
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32877  chirredi 32876
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32865
[Beran] p. 3Definition of joinsshjval3 31836
[Beran] p. 39Theorem 2.3(i)cmcm2 32098  cmcm2i 32075  cmcm2ii 32080  cmt2N 40125
[Beran] p. 40Theorem 2.3(iii)lecm 32099  lecmi 32084  lecmii 32085
[Beran] p. 45Theorem 3.4cmcmlem 32073
[Beran] p. 49Theorem 4.2cm2j 32102  cm2ji 32107  cm2mi 32108
[Beran] p. 95Definitiondf-sh 31689  issh2 31691
[Beran] p. 95Lemma 3.1(S5)his5 31568
[Beran] p. 95Lemma 3.1(S6)his6 31581
[Beran] p. 95Lemma 3.1(S7)his7 31572
[Beran] p. 95Lemma 3.2(S8)ho01i 32310
[Beran] p. 95Lemma 3.2(S9)hoeq1 32312
[Beran] p. 95Lemma 3.2(S10)ho02i 32311
[Beran] p. 95Lemma 3.2(S11)hoeq2 32313
[Beran] p. 95Postulate (S1)ax-his1 31564  his1i 31582
[Beran] p. 95Postulate (S2)ax-his2 31565
[Beran] p. 95Postulate (S3)ax-his3 31566
[Beran] p. 95Postulate (S4)ax-his4 31567
[Beran] p. 96Definition of normdf-hnorm 31450  dfhnorm2 31604  normval 31606
[Beran] p. 96Definition for Cauchy sequencehcau 31666
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31455
[Beran] p. 96Definition of complete subspaceisch3 31723
[Beran] p. 96Definition of convergedf-hlim 31454  hlimi 31670
[Beran] p. 97Theorem 3.3(i)norm-i-i 31615  norm-i 31611
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31619  norm-ii 31620  normlem0 31591  normlem1 31592  normlem2 31593  normlem3 31594  normlem4 31595  normlem5 31596  normlem6 31597  normlem7 31598  normlem7tALT 31601
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31621  norm-iii 31622
[Beran] p. 98Remark 3.4bcs 31663  bcsiALT 31661  bcsiHIL 31662
[Beran] p. 98Remark 3.4(B)normlem9at 31603  normpar 31637  normpari 31636
[Beran] p. 98Remark 3.4(C)normpyc 31628  normpyth 31627  normpythi 31624
[Beran] p. 99Remarklnfn0 32529  lnfn0i 32524  lnop0 32448  lnop0i 32452
[Beran] p. 99Theorem 3.5(i)nmcexi 32508  nmcfnex 32535  nmcfnexi 32533  nmcopex 32511  nmcopexi 32509
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32536  nmcfnlbi 32534  nmcoplb 32512  nmcoplbi 32510
[Beran] p. 99Theorem 3.5(iii)lnfncon 32538  lnfnconi 32537  lnopcon 32517  lnopconi 32516
[Beran] p. 100Lemma 3.6normpar2i 31638
[Beran] p. 101Lemma 3.6norm3adifi 31635  norm3adifii 31630  norm3dif 31632  norm3difi 31629
[Beran] p. 102Theorem 3.7(i)chocunii 31783  pjhth 31875  pjhtheu 31876  pjpjhth 31907  pjpjhthi 31908  pjth 25671
[Beran] p. 102Theorem 3.7(ii)ococ 31888  ococi 31887
[Beran] p. 103Remark 3.8nlelchi 32543
[Beran] p. 104Theorem 3.9riesz3i 32544  riesz4 32546  riesz4i 32545
[Beran] p. 104Theorem 3.10cnlnadj 32561  cnlnadjeu 32560  cnlnadjeui 32559  cnlnadji 32558  cnlnadjlem1 32549  nmopadjlei 32570
[Beran] p. 106Theorem 3.11(i)adjeq0 32573
[Beran] p. 106Theorem 3.11(v)nmopadji 32572
[Beran] p. 106Theorem 3.11(ii)adjmul 32574
[Beran] p. 106Theorem 3.11(iv)adjadj 32418
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32584  nmopcoadji 32583
[Beran] p. 106Theorem 3.11(iii)adjadd 32575
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32585
[Beran] p. 106Theorem 3.11(viii)adjcoi 32582  pjadj2coi 32686  pjadjcoi 32643
[Beran] p. 107Definitiondf-ch 31703  isch2 31705
[Beran] p. 107Remark 3.12choccl 31788  isch3 31723  occl 31786  ocsh 31765  shoccl 31787  shocsh 31766
[Beran] p. 107Remark 3.12(B)ococin 31890
[Beran] p. 108Theorem 3.13chintcl 31814
[Beran] p. 109Property (i)pjadj2 32669  pjadj3 32670  pjadji 32167  pjadjii 32156
[Beran] p. 109Property (ii)pjidmco 32663  pjidmcoi 32659  pjidmi 32155
[Beran] p. 110Definition of projector orderingpjordi 32655
[Beran] p. 111Remarkho0val 32232  pjch1 32152
[Beran] p. 111Definitiondf-hfmul 32216  df-hfsum 32215  df-hodif 32214  df-homul 32213  df-hosum 32212
[Beran] p. 111Lemma 4.4(i)pjo 32153
[Beran] p. 111Lemma 4.4(ii)pjch 32176  pjchi 31914
[Beran] p. 111Lemma 4.4(iii)pjoc2 31921  pjoc2i 31920
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 32162
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32647  pjssmii 32163
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32646
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32645
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32650
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32648  pjssge0ii 32164
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32649  pjdifnormii 32165
[Bobzien] p. 116Statement T3stoic3 1809
[Bobzien] p. 117Statement T2stoic2a 1807
[Bobzien] p. 117Statement T4stoic4a 1810
[Bobzien] p. 117Conclusion the contradictorystoic1a 1805
[Bogachev] p. 16Definition 1.5df-oms 34805
[Bogachev] p. 17Lemma 1.5.4omssubadd 34813
[Bogachev] p. 17Example 1.5.2omsmon 34811
[Bogachev] p. 41Definition 1.11.2df-carsg 34815
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34835
[Bogachev] p. 116Definition 2.3.1df-itgm 34866  df-sitm 34844
[Bogachev] p. 118Chapter 2.4.4df-itgm 34866
[Bogachev] p. 118Definition 2.4.1df-sitg 34843
[Bollobas] p. 1Section I.1df-edg 29506  isuhgrop 29528  isusgrop 29623  isuspgrop 29622
[Bollobas] p. 2Section I.1df-isubgr 48779  df-subgr 29729  uhgrspan1 29764  uhgrspansubgr 29752
[Bollobas] p. 3Definitiondf-gric 48799  gricuspgr 48836  isuspgrim 48814
[Bollobas] p. 3Section I.1cusgrsize 29915  df-clnbgr 48737  df-cusgr 29873  df-nbgr 29794  fusgrmaxsize 29925
[Bollobas] p. 4Definitiondf-upwlks 49052  df-wlks 30060
[Bollobas] p. 4Section I.1finsumvtxdg2size 30011  finsumvtxdgeven 30013  fusgr1th 30012  fusgrvtxdgonume 30015  vtxdgoddnumeven 30014
[Bollobas] p. 5Notationdf-pths 30179
[Bollobas] p. 5Definitiondf-crcts 30253  df-cycls 30254  df-trls 30155  df-wlkson 30061
[Bollobas] p. 7Section I.1df-ushgr 29517
[BourbakiAlg1] p. 1Definition 1df-clintop 49117  df-cllaw 49103  df-mgm 18734  df-mgm2 49136
[BourbakiAlg1] p. 4Definition 5df-assintop 49118  df-asslaw 49105  df-sgrp 18825  df-sgrp2 49138
[BourbakiAlg1] p. 7Definition 8df-cmgm2 49137  df-comlaw 49104
[BourbakiAlg1] p. 12Definition 2df-mnd 18841
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33468  mndlactf1o 33472  mndractf1 33470  mndractf1o 33473
[BourbakiAlg1] p. 92Definition 1df-ring 20378
[BourbakiAlg1] p. 93Section I.8.1df-rng 20292
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 34145
[BourbakiAlg2] p. 113Chapter 5.assafld 34149  assarrginv 34148
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 34190  fldextrspunfld 34188  fldextrspunlem1 34187  fldextrspunlem2 34189  fldextrspunlsp 34186  fldextrspunlsplem 34185
[BourbakiCAlg2], p. 228Proposition 21arithidom 33949  dfufd2 33962
[BourbakiEns] p. Proposition 8fcof1 7291  fcofo 7292
[BourbakiTop1] p. Remarkxnegmnf 13264  xnegpnf 13263
[BourbakiTop1] p. Remark rexneg 13265
[BourbakiTop1] p. Remark 3ust0 24450  ustfilxp 24443
[BourbakiTop1] p. Axiom GT'tgpsubcn 24320
[BourbakiTop1] p. Criterionishmeo 23989
[BourbakiTop1] p. Example 1cstucnd 24513  iducn 24512  snfil 24094
[BourbakiTop1] p. Example 2neifil 24110
[BourbakiTop1] p. Theorem 1cnextcn 24297
[BourbakiTop1] p. Theorem 2ucnextcn 24533
[BourbakiTop1] p. Theorem 3df-hcmp 34469
[BourbakiTop1] p. Paragraph 3infil 24093
[BourbakiTop1] p. Definition 1df-ucn 24505  df-ust 24431  filintn0 24091  filn0 24092  istgp 24307  ucnprima 24511
[BourbakiTop1] p. Definition 2df-cfilu 24516
[BourbakiTop1] p. Definition 3df-cusp 24527  df-usp 24487  df-utop 24461  trust 24459
[BourbakiTop1] p. Definition 6df-pcmp 34368
[BourbakiTop1] p. Property V_issnei2 23345
[BourbakiTop1] p. Theorem 1(d)iscncl 23498
[BourbakiTop1] p. Condition F_Iustssel 24436
[BourbakiTop1] p. Condition U_Iustdiag 24439
[BourbakiTop1] p. Property V_iiinnei 23354
[BourbakiTop1] p. Property V_ivneiptopreu 23362  neissex 23356
[BourbakiTop1] p. Proposition 1neips 23342  neiss 23338  ucncn 24514  ustund 24452  ustuqtop 24476
[BourbakiTop1] p. Proposition 2cnpco 23496  neiptopreu 23362  utop2nei 24480  utop3cls 24481
[BourbakiTop1] p. Proposition 3fmucnd 24521  uspreg 24503  utopreg 24482
[BourbakiTop1] p. Proposition 4imasncld 23921  imasncls 23922  imasnopn 23920
[BourbakiTop1] p. Proposition 9cnpflf2 24230
[BourbakiTop1] p. Condition F_IIustincl 24438
[BourbakiTop1] p. Condition U_IIustinvel 24440
[BourbakiTop1] p. Property V_iiielnei 23340
[BourbakiTop1] p. Proposition 11cnextucn 24532
[BourbakiTop1] p. Condition F_IIbustbasel 24437
[BourbakiTop1] p. Condition U_IIIustexhalf 24441
[BourbakiTop1] p. Definition C'''df-cmp 23616
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 24076
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 23123
[BourbakiTop2] p. 195Definition 1df-ldlf 34365
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46892
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46894  stoweid 46893
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46831  stoweidlem10 46840  stoweidlem14 46844  stoweidlem15 46845  stoweidlem35 46865  stoweidlem36 46866  stoweidlem37 46867  stoweidlem38 46868  stoweidlem40 46870  stoweidlem41 46871  stoweidlem43 46873  stoweidlem44 46874  stoweidlem46 46876  stoweidlem5 46835  stoweidlem50 46880  stoweidlem52 46882  stoweidlem53 46883  stoweidlem55 46885  stoweidlem56 46886
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46853  stoweidlem24 46854  stoweidlem27 46857  stoweidlem28 46858  stoweidlem30 46860
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46864  stoweidlem59 46889  stoweidlem60 46890
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46875  stoweidlem49 46879  stoweidlem7 46837
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46861  stoweidlem39 46869  stoweidlem42 46872  stoweidlem48 46878  stoweidlem51 46881  stoweidlem54 46884  stoweidlem57 46887  stoweidlem58 46888
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46855
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46847
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46841  stoweidlem13 46843  stoweidlem26 46856  stoweidlem61 46891
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46848
[Bruck] p. 1Section I.1df-clintop 49117  df-mgm 18734  df-mgm2 49136
[Bruck] p. 23Section II.1df-sgrp 18825  df-sgrp2 49138
[Bruck] p. 28Theorem 3.2dfgrp3 19166
[ChoquetDD] p. 2Definition of mappingdf-mpt 5191
[Church] p. 129Section II.24df-ifp 1079  dfifp2 1080
[Clemente] p. 10Definition ITnatded 30884
[Clemente] p. 10Definition I` `m,nnatded 30884
[Clemente] p. 11Definition E=>m,nnatded 30884
[Clemente] p. 11Definition I=>m,nnatded 30884
[Clemente] p. 11Definition E` `(1)natded 30884
[Clemente] p. 11Definition E` `(2)natded 30884
[Clemente] p. 12Definition E` `m,n,pnatded 30884
[Clemente] p. 12Definition I` `n(1)natded 30884
[Clemente] p. 12Definition I` `n(2)natded 30884
[Clemente] p. 13Definition I` `m,n,pnatded 30884
[Clemente] p. 14Proof 5.11natded 30884
[Clemente] p. 14Definition E` `nnatded 30884
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30886  ex-natded5.2 30885
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30889  ex-natded5.3 30888
[Clemente] p. 18Theorem 5.5ex-natded5.5 30891
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30893  ex-natded5.7 30892
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30895  ex-natded5.8 30894
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30897  ex-natded5.13 30896
[Clemente] p. 32Definition I` `nnatded 30884
[Clemente] p. 32Definition E` `m,n,p,anatded 30884
[Clemente] p. 32Definition E` `n,tnatded 30884
[Clemente] p. 32Definition I` `n,tnatded 30884
[Clemente] p. 43Theorem 9.20ex-natded9.20 30898
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30899
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30901  ex-natded9.26 30900
[Cohen] p. 301Remarkrelogoprlem 26829
[Cohen] p. 301Property 2relogmul 26830  relogmuld 26863
[Cohen] p. 301Property 3relogdiv 26831  relogdivd 26864
[Cohen] p. 301Property 4relogexp 26834
[Cohen] p. 301Property 1alog1 26823
[Cohen] p. 301Property 1bloge 26824
[Cohen4] p. 348Observationrelogbcxpb 27025
[Cohen4] p. 349Propertyrelogbf 27029
[Cohen4] p. 352Definitionelogb 27008
[Cohen4] p. 361Property 2relogbmul 27015
[Cohen4] p. 361Property 3logbrec 27020  relogbdiv 27017
[Cohen4] p. 361Property 4relogbreexp 27013
[Cohen4] p. 361Property 6relogbexp 27018
[Cohen4] p. 361Property 1(a)logbid1 27006
[Cohen4] p. 361Property 1(b)logb1 27007
[Cohen4] p. 367Propertylogbchbase 27009
[Cohen4] p. 377Property 2logblt 27022
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34798  sxbrsigalem4 34800
[Cohn] p. 81Section II.5acsdomd 18649  acsinfd 18648  acsinfdimd 18650  acsmap2d 18647  acsmapd 18646
[Cohn] p. 143Example 5.1.1sxbrsiga 34803
[Connell] p. 57Definitiondf-scmat 22717  df-scmatalt 49331
[Conway] p. 4Definitionlesrec 28065  lesrecd 28066
[Conway] p. 5Definitionaddsval 28228  addsval2 28229  df-adds 28226  df-muls 28373  df-negs 28287
[Conway] p. 7Theorem0lt1s 28078
[Conway] p. 12Theorem 12pw2cut2 28728
[Conway] p. 16Theorem 0(i)sltsright 28127
[Conway] p. 16Theorem 0(ii)sltsleft 28126
[Conway] p. 16Theorem 0(iii)lesid 28004
[Conway] p. 17Theorem 3addsass 28271  addsassd 28272  addscom 28232  addscomd 28233  addsrid 28230  addsridd 28231
[Conway] p. 17Definitiondf-0s 28073
[Conway] p. 17Theorem 4(ii)negnegs 28310
[Conway] p. 17Theorem 4(iii)negsid 28307  negsidd 28308
[Conway] p. 18Theorem 5leadds1 28255  leadds1d 28261
[Conway] p. 18Definitiondf-1s 28074
[Conway] p. 18Theorem 6(ii)negscl 28302  negscld 28303
[Conway] p. 18Theorem 6(iii)addscld 28246
[Conway] p. 19Notemulsunif2 28436
[Conway] p. 19Theorem 7addsdi 28421  addsdid 28422  addsdird 28423  mulnegs1d 28426  mulnegs2d 28427  mulsass 28432  mulsassd 28433  mulscom 28405  mulscomd 28406
[Conway] p. 19Theorem 8(i)mulscl 28400  mulscld 28401
[Conway] p. 19Theorem 8(iii)lemulsd 28404  ltmuls 28402  ltmulsd 28403
[Conway] p. 20Theorem 9mulsgt0 28410  mulsgt0d 28411
[Conway] p. 21Theorem 10(iv)precsex 28484
[Conway] p. 23Theorem 11eqcuts3 28070
[Conway] p. 24Definitiondf-reno 28756
[Conway] p. 24Theorem 13(ii)readdscl 28765  remulscl 28768  renegscl 28764
[Conway] p. 27Definitiondf-ons 28518  elons2 28524
[Conway] p. 27Theorem 14ltonsex 28528
[Conway] p. 28Theorem 15oncutlt 28530  onswe 28538
[Conway] p. 29Remarkmadebday 28166  newbday 28168  oldbday 28167
[Conway] p. 29Definitiondf-made 28093  df-new 28095  df-old 28094
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13924
[Crawley] p. 1Definition of posetdf-poset 18405
[Crawley] p. 107Theorem 13.2hlsupr 40261
[Crawley] p. 110Theorem 13.3arglem1N 41065  dalaw 40761
[Crawley] p. 111Theorem 13.4hlathil 42836
[Crawley] p. 111Definition of set Wdf-watsN 40865
[Crawley] p. 111Definition of dilationdf-dilN 40981  df-ldil 40979  isldil 40985
[Crawley] p. 111Definition of translationdf-ltrn 40980  df-trnN 40982  isltrn 40994  ltrnu 40996
[Crawley] p. 112Lemma Acdlema1N 40666  cdlema2N 40667  exatleN 40279
[Crawley] p. 112Lemma B1cvrat 40351  cdlemb 40669  cdlemb2 40916  cdlemb3 41481  idltrn 41025  l1cvat 39930  lhpat 40918  lhpat2 40920  lshpat 39931  ltrnel 41014  ltrnmw 41026
[Crawley] p. 112Lemma Ccdlemc1 41066  cdlemc2 41067  ltrnnidn 41049  trlat 41044  trljat1 41041  trljat2 41042  trljat3 41043  trlne 41060  trlnidat 41048  trlnle 41061
[Crawley] p. 112Definition of automorphismdf-pautN 40866
[Crawley] p. 113Lemma Ccdlemc 41072  cdlemc3 41068  cdlemc4 41069
[Crawley] p. 113Lemma Dcdlemd 41082  cdlemd1 41073  cdlemd2 41074  cdlemd3 41075  cdlemd4 41076  cdlemd5 41077  cdlemd6 41078  cdlemd7 41079  cdlemd8 41080  cdlemd9 41081  cdleme31sde 41260  cdleme31se 41257  cdleme31se2 41258  cdleme31snd 41261  cdleme32a 41316  cdleme32b 41317  cdleme32c 41318  cdleme32d 41319  cdleme32e 41320  cdleme32f 41321  cdleme32fva 41312  cdleme32fva1 41313  cdleme32fvcl 41315  cdleme32le 41322  cdleme48fv 41374  cdleme4gfv 41382  cdleme50eq 41416  cdleme50f 41417  cdleme50f1 41418  cdleme50f1o 41421  cdleme50laut 41422  cdleme50ldil 41423  cdleme50lebi 41415  cdleme50rn 41420  cdleme50rnlem 41419  cdlemeg49le 41386  cdlemeg49lebilem 41414
[Crawley] p. 113Lemma Ecdleme 41435  cdleme00a 41084  cdleme01N 41096  cdleme02N 41097  cdleme0a 41086  cdleme0aa 41085  cdleme0b 41087  cdleme0c 41088  cdleme0cp 41089  cdleme0cq 41090  cdleme0dN 41091  cdleme0e 41092  cdleme0ex1N 41098  cdleme0ex2N 41099  cdleme0fN 41093  cdleme0gN 41094  cdleme0moN 41100  cdleme1 41102  cdleme10 41129  cdleme10tN 41133  cdleme11 41145  cdleme11a 41135  cdleme11c 41136  cdleme11dN 41137  cdleme11e 41138  cdleme11fN 41139  cdleme11g 41140  cdleme11h 41141  cdleme11j 41142  cdleme11k 41143  cdleme11l 41144  cdleme12 41146  cdleme13 41147  cdleme14 41148  cdleme15 41153  cdleme15a 41149  cdleme15b 41150  cdleme15c 41151  cdleme15d 41152  cdleme16 41160  cdleme16aN 41134  cdleme16b 41154  cdleme16c 41155  cdleme16d 41156  cdleme16e 41157  cdleme16f 41158  cdleme16g 41159  cdleme19a 41178  cdleme19b 41179  cdleme19c 41180  cdleme19d 41181  cdleme19e 41182  cdleme19f 41183  cdleme1b 41101  cdleme2 41103  cdleme20aN 41184  cdleme20bN 41185  cdleme20c 41186  cdleme20d 41187  cdleme20e 41188  cdleme20f 41189  cdleme20g 41190  cdleme20h 41191  cdleme20i 41192  cdleme20j 41193  cdleme20k 41194  cdleme20l 41197  cdleme20l1 41195  cdleme20l2 41196  cdleme20m 41198  cdleme20y 41177  cdleme20zN 41176  cdleme21 41212  cdleme21d 41205  cdleme21e 41206  cdleme22a 41215  cdleme22aa 41214  cdleme22b 41216  cdleme22cN 41217  cdleme22d 41218  cdleme22e 41219  cdleme22eALTN 41220  cdleme22f 41221  cdleme22f2 41222  cdleme22g 41223  cdleme23a 41224  cdleme23b 41225  cdleme23c 41226  cdleme26e 41234  cdleme26eALTN 41236  cdleme26ee 41235  cdleme26f 41238  cdleme26f2 41240  cdleme26f2ALTN 41239  cdleme26fALTN 41237  cdleme27N 41244  cdleme27a 41242  cdleme27cl 41241  cdleme28c 41247  cdleme3 41112  cdleme30a 41253  cdleme31fv 41265  cdleme31fv1 41266  cdleme31fv1s 41267  cdleme31fv2 41268  cdleme31id 41269  cdleme31sc 41259  cdleme31sdnN 41262  cdleme31sn 41255  cdleme31sn1 41256  cdleme31sn1c 41263  cdleme31sn2 41264  cdleme31so 41254  cdleme35a 41323  cdleme35b 41325  cdleme35c 41326  cdleme35d 41327  cdleme35e 41328  cdleme35f 41329  cdleme35fnpq 41324  cdleme35g 41330  cdleme35h 41331  cdleme35h2 41332  cdleme35sn2aw 41333  cdleme35sn3a 41334  cdleme36a 41335  cdleme36m 41336  cdleme37m 41337  cdleme38m 41338  cdleme38n 41339  cdleme39a 41340  cdleme39n 41341  cdleme3b 41104  cdleme3c 41105  cdleme3d 41106  cdleme3e 41107  cdleme3fN 41108  cdleme3fa 41111  cdleme3g 41109  cdleme3h 41110  cdleme4 41113  cdleme40m 41342  cdleme40n 41343  cdleme40v 41344  cdleme40w 41345  cdleme41fva11 41352  cdleme41sn3aw 41349  cdleme41sn4aw 41350  cdleme41snaw 41351  cdleme42a 41346  cdleme42b 41353  cdleme42c 41347  cdleme42d 41348  cdleme42e 41354  cdleme42f 41355  cdleme42g 41356  cdleme42h 41357  cdleme42i 41358  cdleme42k 41359  cdleme42ke 41360  cdleme42keg 41361  cdleme42mN 41362  cdleme42mgN 41363  cdleme43aN 41364  cdleme43bN 41365  cdleme43cN 41366  cdleme43dN 41367  cdleme5 41115  cdleme50ex 41434  cdleme50ltrn 41432  cdleme51finvN 41431  cdleme51finvfvN 41430  cdleme51finvtrN 41433  cdleme6 41116  cdleme7 41124  cdleme7a 41118  cdleme7aa 41117  cdleme7b 41119  cdleme7c 41120  cdleme7d 41121  cdleme7e 41122  cdleme7ga 41123  cdleme8 41125  cdleme8tN 41130  cdleme9 41128  cdleme9a 41126  cdleme9b 41127  cdleme9tN 41132  cdleme9taN 41131  cdlemeda 41173  cdlemedb 41172  cdlemednpq 41174  cdlemednuN 41175  cdlemefr27cl 41278  cdlemefr32fva1 41285  cdlemefr32fvaN 41284  cdlemefrs32fva 41275  cdlemefrs32fva1 41276  cdlemefs27cl 41288  cdlemefs32fva1 41298  cdlemefs32fvaN 41297  cdlemesner 41171  cdlemeulpq 41095
[Crawley] p. 114Lemma E4atex 40951  4atexlem7 40950  cdleme0nex 41165  cdleme17a 41161  cdleme17c 41163  cdleme17d 41373  cdleme17d1 41164  cdleme17d2 41370  cdleme18a 41166  cdleme18b 41167  cdleme18c 41168  cdleme18d 41170  cdleme4a 41114
[Crawley] p. 115Lemma Ecdleme21a 41200  cdleme21at 41203  cdleme21b 41201  cdleme21c 41202  cdleme21ct 41204  cdleme21f 41207  cdleme21g 41208  cdleme21h 41209  cdleme21i 41210  cdleme22gb 41169
[Crawley] p. 116Lemma Fcdlemf 41438  cdlemf1 41436  cdlemf2 41437
[Crawley] p. 116Lemma Gcdlemftr1 41442  cdlemg16 41532  cdlemg28 41579  cdlemg28a 41568  cdlemg28b 41578  cdlemg3a 41472  cdlemg42 41604  cdlemg43 41605  cdlemg44 41608  cdlemg44a 41606  cdlemg46 41610  cdlemg47 41611  cdlemg9 41509  ltrnco 41594  ltrncom 41613  tgrpabl 41626  trlco 41602
[Crawley] p. 116Definition of Gdf-tgrp 41618
[Crawley] p. 117Lemma Gcdlemg17 41552  cdlemg17b 41537
[Crawley] p. 117Definition of Edf-edring-rN 41631  df-edring 41632
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41635
[Crawley] p. 118Remarktendopltp 41655
[Crawley] p. 118Lemma Hcdlemh 41692  cdlemh1 41690  cdlemh2 41691
[Crawley] p. 118Lemma Icdlemi 41695  cdlemi1 41693  cdlemi2 41694
[Crawley] p. 118Lemma Jcdlemj1 41696  cdlemj2 41697  cdlemj3 41698  tendocan 41699
[Crawley] p. 118Lemma Kcdlemk 41849  cdlemk1 41706  cdlemk10 41718  cdlemk11 41724  cdlemk11t 41821  cdlemk11ta 41804  cdlemk11tb 41806  cdlemk11tc 41820  cdlemk11u-2N 41764  cdlemk11u 41746  cdlemk12 41725  cdlemk12u-2N 41765  cdlemk12u 41747  cdlemk13-2N 41751  cdlemk13 41727  cdlemk14-2N 41753  cdlemk14 41729  cdlemk15-2N 41754  cdlemk15 41730  cdlemk16-2N 41755  cdlemk16 41732  cdlemk16a 41731  cdlemk17-2N 41756  cdlemk17 41733  cdlemk18-2N 41761  cdlemk18-3N 41775  cdlemk18 41743  cdlemk19-2N 41762  cdlemk19 41744  cdlemk19u 41845  cdlemk1u 41734  cdlemk2 41707  cdlemk20-2N 41767  cdlemk20 41749  cdlemk21-2N 41766  cdlemk21N 41748  cdlemk22-3 41776  cdlemk22 41768  cdlemk23-3 41777  cdlemk24-3 41778  cdlemk25-3 41779  cdlemk26-3 41781  cdlemk26b-3 41780  cdlemk27-3 41782  cdlemk28-3 41783  cdlemk29-3 41786  cdlemk3 41708  cdlemk30 41769  cdlemk31 41771  cdlemk32 41772  cdlemk33N 41784  cdlemk34 41785  cdlemk35 41787  cdlemk36 41788  cdlemk37 41789  cdlemk38 41790  cdlemk39 41791  cdlemk39u 41843  cdlemk4 41709  cdlemk41 41795  cdlemk42 41816  cdlemk42yN 41819  cdlemk43N 41838  cdlemk45 41822  cdlemk46 41823  cdlemk47 41824  cdlemk48 41825  cdlemk49 41826  cdlemk5 41711  cdlemk50 41827  cdlemk51 41828  cdlemk52 41829  cdlemk53 41832  cdlemk54 41833  cdlemk55 41836  cdlemk55u 41841  cdlemk56 41846  cdlemk5a 41710  cdlemk5auN 41735  cdlemk5u 41736  cdlemk6 41712  cdlemk6u 41737  cdlemk7 41723  cdlemk7u-2N 41763  cdlemk7u 41745  cdlemk8 41713  cdlemk9 41714  cdlemk9bN 41715  cdlemki 41716  cdlemkid 41811  cdlemkj-2N 41757  cdlemkj 41738  cdlemksat 41721  cdlemksel 41720  cdlemksv 41719  cdlemksv2 41722  cdlemkuat 41741  cdlemkuel-2N 41759  cdlemkuel-3 41773  cdlemkuel 41740  cdlemkuv-2N 41758  cdlemkuv2-2 41760  cdlemkuv2-3N 41774  cdlemkuv2 41742  cdlemkuvN 41739  cdlemkvcl 41717  cdlemky 41801  cdlemkyyN 41837  tendoex 41850
[Crawley] p. 120Remarkdva1dim 41860
[Crawley] p. 120Lemma Lcdleml1N 41851  cdleml2N 41852  cdleml3N 41853  cdleml4N 41854  cdleml5N 41855  cdleml6 41856  cdleml7 41857  cdleml8 41858  cdleml9 41859  dia1dim 41936
[Crawley] p. 120Lemma Mdia11N 41923  diaf11N 41924  dialss 41921  diaord 41922  dibf11N 42036  djajN 42012
[Crawley] p. 120Definition of isomorphism mapdiaval 41907
[Crawley] p. 121Lemma Mcdlemm10N 41993  dia2dimlem1 41939  dia2dimlem2 41940  dia2dimlem3 41941  dia2dimlem4 41942  dia2dimlem5 41943  diaf1oN 42005  diarnN 42004  dvheveccl 41987  dvhopN 41991
[Crawley] p. 121Lemma Ncdlemn 42087  cdlemn10 42081  cdlemn11 42086  cdlemn11a 42082  cdlemn11b 42083  cdlemn11c 42084  cdlemn11pre 42085  cdlemn2 42070  cdlemn2a 42071  cdlemn3 42072  cdlemn4 42073  cdlemn4a 42074  cdlemn5 42076  cdlemn5pre 42075  cdlemn6 42077  cdlemn7 42078  cdlemn8 42079  cdlemn9 42080  diclspsn 42069
[Crawley] p. 121Definition of phi(q)df-dic 42048
[Crawley] p. 122Lemma Ndih11 42140  dihf11 42142  dihjust 42092  dihjustlem 42091  dihord 42139  dihord1 42093  dihord10 42098  dihord11b 42097  dihord11c 42099  dihord2 42102  dihord2a 42094  dihord2b 42095  dihord2cN 42096  dihord2pre 42100  dihord2pre2 42101  dihordlem6 42088  dihordlem7 42089  dihordlem7b 42090
[Crawley] p. 122Definition of isomorphism mapdihffval 42105  dihfval 42106  dihval 42107
[Diestel] p. 3Definitiondf-gric 48799  df-grim 48796  isuspgrim 48814
[Diestel] p. 3Section 1.1df-cusgr 29873  df-nbgr 29794
[Diestel] p. 3Definition by df-grisom 48795
[Diestel] p. 4Section 1.1df-isubgr 48779  df-subgr 29729  uhgrspan1 29764  uhgrspansubgr 29752
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 30015  vtxdgoddnumeven 30014
[Diestel] p. 27Section 1.10df-ushgr 29517
[EGA] p. 80Notation 1.1.1rspecval 34376
[EGA] p. 80Proposition 1.1.2zartop 34388
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34380  zarcls1 34381
[EGA] p. 81Corollary 1.1.8zart0 34391
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34394
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34397
[Eisenberg] p. 67Definition 5.3df-dif 3905
[Eisenberg] p. 82Definition 6.3dfom3 9629
[Eisenberg] p. 125Definition 8.21df-map 8831
[Eisenberg] p. 216Example 13.2(4)omenps 9637
[Eisenberg] p. 310Theorem 19.8cardprc 9988
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10566
[Enderton] p. 18Axiom of Empty Setaxnul 5266
[Enderton] p. 19Definitiondf-tp 4592
[Enderton] p. 26Exercise 5unissb 4904
[Enderton] p. 26Exercise 10pwel 5350
[Enderton] p. 28Exercise 7(b)pwun 5552
[Enderton] p. 30Theorem "Distributive laws"iinin1 5043  iinin2 5042  iinun2 5035  iunin1 5034  iunin1f 33032  iunin2 5033  uniin1 5037  uniin2 5038
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5041  iundif2 5036
[Enderton] p. 32Exercise 20unineq 4237
[Enderton] p. 33Exercise 23iinuni 5062
[Enderton] p. 33Exercise 25iununi 5063
[Enderton] p. 33Exercise 24(a)iinpw 5070
[Enderton] p. 33Exercise 24(b)iunpw 7773  iunpwss 5071
[Enderton] p. 36Definitionopthwiener 5495
[Enderton] p. 38Exercise 6(a)unipw 5429
[Enderton] p. 38Exercise 6(b)pwuni 4909
[Enderton] p. 41Lemma 3Dopeluu 5450  rnex 7910  rnexg 7902
[Enderton] p. 41Exercise 8dmuni 5902  rnuni 6144
[Enderton] p. 42Definition of a functiondffun7 6564  dffun8 6565
[Enderton] p. 43Definition of function valuefunfv2 6970
[Enderton] p. 43Definition of single-rootedfuncnv 6606
[Enderton] p. 44Definition (d)dfima2 6062  dfima3 6063
[Enderton] p. 47Theorem 3Hfvco2 6979
[Enderton] p. 49Axiom of Choice (first form)ac7 10478  ac7g 10479  df-ac 10122  dfac2 10137  dfac2a 10135  dfac2b 10136  dfac3 10127  dfac7 10138
[Enderton] p. 50Theorem 3K(a)imauni 7246
[Enderton] p. 52Definitiondf-map 8831
[Enderton] p. 53Exercise 21coass 6266
[Enderton] p. 53Exercise 27dmco 6255
[Enderton] p. 53Exercise 14(a)funin 6613
[Enderton] p. 53Exercise 22(a)imass2 6102
[Enderton] p. 54Remarkixpf 8930  ixpssmap 8942
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8908
[Enderton] p. 55Axiom of Choice (second form)ac9 10488  ac9s 10498
[Enderton] p. 56Theorem 3Meqvrelref 39444  erref 8720
[Enderton] p. 57Lemma 3Neqvrelthi 39447  erthi 8756
[Enderton] p. 57Definitiondf-ec 8701
[Enderton] p. 58Definitiondf-qs 8705
[Enderton] p. 61Exercise 35df-ec 8701
[Enderton] p. 65Exercise 56(a)dmun 5898
[Enderton] p. 68Definition of successordf-suc 6367
[Enderton] p. 71Definitiondf-tr 5217  dftr4 5222
[Enderton] p. 72Theorem 4Eunisuc 6443  unisucg 6442
[Enderton] p. 73Exercise 6unisuc 6443  unisucg 6442
[Enderton] p. 73Exercise 5(a)truni 5232
[Enderton] p. 73Exercise 5(b)trint 5234  trintALT 45705
[Enderton] p. 79Theorem 4I(A1)nna0 8595
[Enderton] p. 79Theorem 4I(A2)nnasuc 8597  onasuc 8518
[Enderton] p. 79Definition of operation valuedf-ov 7419
[Enderton] p. 80Theorem 4J(A1)nnm0 8596
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8598  onmsuc 8519
[Enderton] p. 81Theorem 4K(1)nnaass 8613
[Enderton] p. 81Theorem 4K(2)nna0r 8600  nnacom 8608
[Enderton] p. 81Theorem 4K(3)nndi 8614
[Enderton] p. 81Theorem 4K(4)nnmass 8615
[Enderton] p. 81Theorem 4K(5)nnmcom 8617
[Enderton] p. 82Exercise 16nnm0r 8601  nnmsucr 8616
[Enderton] p. 88Exercise 23nnaordex 8629
[Enderton] p. 129Definitiondf-en 8956
[Enderton] p. 132Theorem 6B(b)canth 7370
[Enderton] p. 133Exercise 1xpomen 10021
[Enderton] p. 133Exercise 2qnnen 16305
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9204
[Enderton] p. 135Corollary 6Cphp3 9206
[Enderton] p. 136Corollary 6Enneneq 9203
[Enderton] p. 136Corollary 6D(a)pssinf 9235
[Enderton] p. 136Corollary 6D(b)ominf 9237
[Enderton] p. 137Lemma 6Fpssnn 9166
[Enderton] p. 138Corollary 6Gssfi 9170
[Enderton] p. 139Theorem 6H(c)mapen 9142
[Enderton] p. 142Theorem 6I(3)xpdjuen 10185
[Enderton] p. 142Theorem 6I(4)mapdjuen 10186
[Enderton] p. 143Theorem 6Jdju0en 10181  dju1en 10177
[Enderton] p. 144Exercise 13iunfi 9313  unifi 9314  unifi2 9315
[Enderton] p. 144Corollary 6Kundif2 4434  unfi 9168  unfi2 9283
[Enderton] p. 145Figure 38ffoss 7946
[Enderton] p. 145Definitiondf-dom 8957
[Enderton] p. 146Example 1domen 8970  domeng 8971
[Enderton] p. 146Example 3nndomo 9215  nnsdom 9636  nnsdomg 9272
[Enderton] p. 149Theorem 6L(a)djudom2 10189
[Enderton] p. 149Theorem 6L(c)mapdom1 9143  xpdom1 9077  xpdom1g 9075  xpdom2g 9074
[Enderton] p. 149Theorem 6L(d)mapdom2 9149
[Enderton] p. 151Theorem 6Mzorn 10512  zorng 10509
[Enderton] p. 151Theorem 6M(4)ac8 10497  dfac5 10134
[Enderton] p. 159Theorem 6Qunictb 10587
[Enderton] p. 164Exampleinfdif 10213
[Enderton] p. 168Definitiondf-po 5567
[Enderton] p. 192Theorem 7M(a)oneli 6477
[Enderton] p. 192Theorem 7M(b)ontr1 6409
[Enderton] p. 192Theorem 7M(c)onirri 6476
[Enderton] p. 193Corollary 7N(b)0elon 6417
[Enderton] p. 193Corollary 7N(c)onsuci 7838
[Enderton] p. 193Corollary 7N(d)ssonunii 7783
[Enderton] p. 194Remarkonprc 7780
[Enderton] p. 194Exercise 16suc11 6471
[Enderton] p. 197Definitiondf-card 9947
[Enderton] p. 197Theorem 7Pcarden 10562
[Enderton] p. 200Exercise 25tfis 7854
[Enderton] p. 202Lemma 7Tr1tr 9761
[Enderton] p. 202Definitiondf-r1 9749
[Enderton] p. 202Theorem 7Qr1val1 9771
[Enderton] p. 204Theorem 7V(b)rankval4 9852  rankval4b 35609
[Enderton] p. 206Theorem 7X(b)en2lp 9588
[Enderton] p. 207Exercise 30rankpr 9842  rankprb 9836  rankpw 9828  rankpwi 9808  rankuniss 9851
[Enderton] p. 207Exercise 34opthreg 9600
[Enderton] p. 208Exercise 35suc11reg 9601
[Enderton] p. 212Definition of alephalephval3 10116
[Enderton] p. 213Theorem 8A(a)alephord2 10082
[Enderton] p. 213Theorem 8A(b)cardalephex 10096
[Enderton] p. 218Theorem Schema 8Eonfununi 8333
[Enderton] p. 222Definitiondf-kard 35678
[Enderton] p. 222Definition of kardkarden 9901  kardex 9899
[Enderton] p. 238Theorem 8Roeoa 8588
[Enderton] p. 238Theorem 8Soeoe 8590
[Enderton] p. 240Exercise 25oarec 8552
[Enderton] p. 257Definition of cofinalitycflm 10254
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17734
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17676
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18645  mrieqv2d 17731  mrieqvd 17730
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17735
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17740  mreexexlem2d 17737
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18651  mreexfidimd 17742
[Frege1879] p. 11Statementdf3or2 44610
[Frege1879] p. 12Statementdf3an2 44611  dfxor4 44608  dfxor5 44609
[Frege1879] p. 26Axiom 1ax-frege1 44632
[Frege1879] p. 26Axiom 2ax-frege2 44633
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44637
[Frege1879] p. 31Proposition 4frege4 44641
[Frege1879] p. 32Proposition 5frege5 44642
[Frege1879] p. 33Proposition 6frege6 44648
[Frege1879] p. 34Proposition 7frege7 44650
[Frege1879] p. 35Axiom 8ax-frege8 44651  axfrege8 44649
[Frege1879] p. 35Proposition 8pm2.04 91  wl-luk-pm2.04 38201
[Frege1879] p. 35Proposition 9frege9 44654
[Frege1879] p. 36Proposition 10frege10 44662
[Frege1879] p. 36Proposition 11frege11 44656
[Frege1879] p. 37Proposition 12frege12 44655
[Frege1879] p. 37Proposition 13frege13 44664
[Frege1879] p. 37Proposition 14frege14 44665
[Frege1879] p. 38Proposition 15frege15 44668
[Frege1879] p. 38Proposition 16frege16 44658
[Frege1879] p. 39Proposition 17frege17 44663
[Frege1879] p. 39Proposition 18frege18 44660
[Frege1879] p. 39Proposition 19frege19 44666
[Frege1879] p. 40Proposition 20frege20 44670
[Frege1879] p. 40Proposition 21frege21 44669
[Frege1879] p. 41Proposition 22frege22 44661
[Frege1879] p. 42Proposition 23frege23 44667
[Frege1879] p. 42Proposition 24frege24 44657
[Frege1879] p. 42Proposition 25frege25 44659  rp-frege25 44647
[Frege1879] p. 42Proposition 26frege26 44652
[Frege1879] p. 43Axiom 28ax-frege28 44672
[Frege1879] p. 43Proposition 27frege27 44653
[Frege1879] p. 43Proposition 28con3 154
[Frege1879] p. 43Proposition 29frege29 44673
[Frege1879] p. 44Axiom 31ax-frege31 44676  axfrege31 44675
[Frege1879] p. 44Proposition 30frege30 44674
[Frege1879] p. 44Proposition 31notnotr 131
[Frege1879] p. 44Proposition 32frege32 44677
[Frege1879] p. 44Proposition 33frege33 44678
[Frege1879] p. 45Proposition 34frege34 44679
[Frege1879] p. 45Proposition 35frege35 44680
[Frege1879] p. 45Proposition 36frege36 44681
[Frege1879] p. 46Proposition 37frege37 44682
[Frege1879] p. 46Proposition 38frege38 44683
[Frege1879] p. 46Proposition 39frege39 44684
[Frege1879] p. 46Proposition 40frege40 44685
[Frege1879] p. 47Axiom 41ax-frege41 44687  axfrege41 44686
[Frege1879] p. 47Proposition 41notnot 143
[Frege1879] p. 47Proposition 42frege42 44688
[Frege1879] p. 47Proposition 43frege43 44689
[Frege1879] p. 47Proposition 44frege44 44690
[Frege1879] p. 47Proposition 45frege45 44691
[Frege1879] p. 48Proposition 46frege46 44692
[Frege1879] p. 48Proposition 47frege47 44693
[Frege1879] p. 49Proposition 48frege48 44694
[Frege1879] p. 49Proposition 49frege49 44695
[Frege1879] p. 49Proposition 50frege50 44696
[Frege1879] p. 50Axiom 52ax-frege52a 44699  ax-frege52c 44730  frege52aid 44700  frege52b 44731
[Frege1879] p. 50Axiom 54ax-frege54a 44704  ax-frege54c 44734  frege54b 44735
[Frege1879] p. 50Proposition 51frege51 44697
[Frege1879] p. 50Proposition 52dfsbcq 3744
[Frege1879] p. 50Proposition 53frege53a 44702  frege53aid 44701  frege53b 44732  frege53c 44756
[Frege1879] p. 50Proposition 54biid 264  eqid 2762
[Frege1879] p. 50Proposition 55frege55a 44710  frege55aid 44707  frege55b 44739  frege55c 44760  frege55cor1a 44711  frege55lem2a 44709  frege55lem2b 44738  frege55lem2c 44759
[Frege1879] p. 50Proposition 56frege56a 44713  frege56aid 44712  frege56b 44740  frege56c 44761
[Frege1879] p. 51Axiom 58ax-frege58a 44717  ax-frege58b 44743  frege58bid 44744  frege58c 44763
[Frege1879] p. 51Proposition 57frege57a 44715  frege57aid 44714  frege57b 44741  frege57c 44762
[Frege1879] p. 51Proposition 58spsbc 3755
[Frege1879] p. 51Proposition 59frege59a 44719  frege59b 44746  frege59c 44764
[Frege1879] p. 52Proposition 60frege60a 44720  frege60b 44747  frege60c 44765
[Frege1879] p. 52Proposition 61frege61a 44721  frege61b 44748  frege61c 44766
[Frege1879] p. 52Proposition 62frege62a 44722  frege62b 44749  frege62c 44767
[Frege1879] p. 52Proposition 63frege63a 44723  frege63b 44750  frege63c 44768
[Frege1879] p. 53Proposition 64frege64a 44724  frege64b 44751  frege64c 44769
[Frege1879] p. 53Proposition 65frege65a 44725  frege65b 44752  frege65c 44770
[Frege1879] p. 54Proposition 66frege66a 44726  frege66b 44753  frege66c 44771
[Frege1879] p. 54Proposition 67frege67a 44727  frege67b 44754  frege67c 44772
[Frege1879] p. 54Proposition 68frege68a 44728  frege68b 44755  frege68c 44773
[Frege1879] p. 55Definition 69dffrege69 44774
[Frege1879] p. 58Proposition 70frege70 44775
[Frege1879] p. 59Proposition 71frege71 44776
[Frege1879] p. 59Proposition 72frege72 44777
[Frege1879] p. 59Proposition 73frege73 44778
[Frege1879] p. 60Definition 76dffrege76 44781
[Frege1879] p. 60Proposition 74frege74 44779
[Frege1879] p. 60Proposition 75frege75 44780
[Frege1879] p. 62Proposition 77frege77 44782  frege77d 44588
[Frege1879] p. 63Proposition 78frege78 44783
[Frege1879] p. 63Proposition 79frege79 44784
[Frege1879] p. 63Proposition 80frege80 44785
[Frege1879] p. 63Proposition 81frege81 44786  frege81d 44589
[Frege1879] p. 64Proposition 82frege82 44787
[Frege1879] p. 65Proposition 83frege83 44788  frege83d 44590
[Frege1879] p. 65Proposition 84frege84 44789
[Frege1879] p. 66Proposition 85frege85 44790
[Frege1879] p. 66Proposition 86frege86 44791
[Frege1879] p. 66Proposition 87frege87 44792  frege87d 44592
[Frege1879] p. 67Proposition 88frege88 44793
[Frege1879] p. 68Proposition 89frege89 44794
[Frege1879] p. 68Proposition 90frege90 44795
[Frege1879] p. 68Proposition 91frege91 44796  frege91d 44593
[Frege1879] p. 69Proposition 92frege92 44797
[Frege1879] p. 70Proposition 93frege93 44798
[Frege1879] p. 70Proposition 94frege94 44799
[Frege1879] p. 70Proposition 95frege95 44800
[Frege1879] p. 71Definition 99dffrege99 44804
[Frege1879] p. 71Proposition 96frege96 44801  frege96d 44591
[Frege1879] p. 71Proposition 97frege97 44802  frege97d 44594
[Frege1879] p. 71Proposition 98frege98 44803  frege98d 44595
[Frege1879] p. 72Proposition 100frege100 44805
[Frege1879] p. 72Proposition 101frege101 44806
[Frege1879] p. 72Proposition 102frege102 44807  frege102d 44596
[Frege1879] p. 73Proposition 103frege103 44808
[Frege1879] p. 73Proposition 104frege104 44809
[Frege1879] p. 73Proposition 105frege105 44810
[Frege1879] p. 73Proposition 106frege106 44811  frege106d 44597
[Frege1879] p. 74Proposition 107frege107 44812
[Frege1879] p. 74Proposition 108frege108 44813  frege108d 44598
[Frege1879] p. 74Proposition 109frege109 44814  frege109d 44599
[Frege1879] p. 75Proposition 110frege110 44815
[Frege1879] p. 75Proposition 111frege111 44816  frege111d 44601
[Frege1879] p. 76Proposition 112frege112 44817
[Frege1879] p. 76Proposition 113frege113 44818
[Frege1879] p. 76Proposition 114frege114 44819  frege114d 44600
[Frege1879] p. 77Definition 115dffrege115 44820
[Frege1879] p. 77Proposition 116frege116 44821
[Frege1879] p. 78Proposition 117frege117 44822
[Frege1879] p. 78Proposition 118frege118 44823
[Frege1879] p. 78Proposition 119frege119 44824
[Frege1879] p. 78Proposition 120frege120 44825
[Frege1879] p. 79Proposition 121frege121 44826
[Frege1879] p. 79Proposition 122frege122 44827  frege122d 44602
[Frege1879] p. 79Proposition 123frege123 44828
[Frege1879] p. 80Proposition 124frege124 44829  frege124d 44603
[Frege1879] p. 81Proposition 125frege125 44830
[Frege1879] p. 81Proposition 126frege126 44831  frege126d 44604
[Frege1879] p. 82Proposition 127frege127 44832
[Frege1879] p. 83Proposition 128frege128 44833
[Frege1879] p. 83Proposition 129frege129 44834  frege129d 44605
[Frege1879] p. 84Proposition 130frege130 44835
[Frege1879] p. 85Proposition 131frege131 44836  frege131d 44606
[Frege1879] p. 86Proposition 132frege132 44837
[Frege1879] p. 86Proposition 133frege133 44838  frege133d 44607
[Fremlin1] p. 13Definition 111G (b)df-salgen 47143
[Fremlin1] p. 13Definition 111G (d)borelmbl 47466
[Fremlin1] p. 13Proposition 111G (b)salgenss 47166
[Fremlin1] p. 14Definition 112Aismea 47281
[Fremlin1] p. 15Remark 112B (d)psmeasure 47301
[Fremlin1] p. 15Property 112C (a)meadjun 47292  meadjunre 47306
[Fremlin1] p. 15Property 112C (b)meassle 47293
[Fremlin1] p. 15Property 112C (c)meaunle 47294
[Fremlin1] p. 16Property 112C (d)iundjiun 47290  meaiunle 47299  meaiunlelem 47298
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47311  meaiuninc2 47312  meaiuninc3 47315  meaiuninc3v 47314  meaiunincf 47313  meaiuninclem 47310
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47317  meaiininc2 47318  meaiininclem 47316
[Fremlin1] p. 19Theorem 113Ccaragen0 47336  caragendifcl 47344  caratheodory 47358  omelesplit 47348
[Fremlin1] p. 19Definition 113Aisome 47324  isomennd 47361  isomenndlem 47360
[Fremlin1] p. 19Remark 113B (c)omeunle 47346
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47365  voncmpl 47451
[Fremlin1] p. 19Definition 113A (ii)omessle 47328
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47353  carageniuncllem1 47351  carageniuncllem2 47352  caragenuncl 47343  caragenuncllem 47342  caragenunicl 47354
[Fremlin1] p. 21Remark 113Dcaragenel2d 47362
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47356  caratheodorylem2 47357
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47365
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47424  hoidmv1lelem1 47421  hoidmv1lelem2 47422  hoidmv1lelem3 47423
[Fremlin1] p. 25Definition 114Eisvonmbl 47468
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47424  hoidmvle 47430  hoidmvlelem1 47425  hoidmvlelem2 47426  hoidmvlelem3 47427  hoidmvlelem4 47428  hoidmvlelem5 47429  hsphoidmvle2 47415  hsphoif 47406  hsphoival 47409
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47378
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47386
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47413  hoidmvn0val 47414  hoidmvval 47407  hoidmvval0 47417  hoidmvval0b 47420
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47418  hsphoidmvle 47416
[Fremlin1] p. 30Definition 115Cdf-ovoln 47367  df-voln 47369
[Fremlin1] p. 30Proposition 115D (a)dmovn 47434  ovn0 47396  ovn0lem 47395  ovnf 47393  ovnome 47403  ovnssle 47391  ovnsslelem 47390  ovnsupge0 47387
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47433  ovnhoilem1 47431  ovnhoilem2 47432  vonhoi 47497
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47450  hoidifhspf 47448  hoidifhspval 47438  hoidifhspval2 47445  hoidifhspval3 47449  hspmbl 47459  hspmbllem1 47456  hspmbllem2 47457  hspmbllem3 47458
[Fremlin1] p. 31Definition 115Evoncmpl 47451  vonmea 47404
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47402  ovnsubadd2 47476  ovnsubadd2lem 47475  ovnsubaddlem1 47400  ovnsubaddlem2 47401
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47461  hoimbl2 47495  hoimbllem 47460  hspdifhsp 47446  opnvonmbl 47464  opnvonmbllem2 47463
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47466
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47509  iccvonmbllem 47508  ioovonmbl 47507
[Fremlin1] p. 32Proposition 115G (d)vonicc 47515  vonicclem2 47514  vonioo 47512  vonioolem2 47511  vonn0icc 47518  vonn0icc2 47522  vonn0ioo 47517  vonn0ioo2 47520
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47519  snvonmbl 47516  vonct 47523  vonsn 47521
[Fremlin1] p. 35Lemma 121Asubsalsal 47189
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 47188  subsaliuncllem 47187
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47555  salpreimalegt 47539  salpreimaltle 47556
[Fremlin1] p. 35Proposition 121B (i)issmf 47558  issmff 47564  issmflem 47557
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47575  issmflelem 47574  smfpreimale 47584
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47586  issmfgtlem 47585
[Fremlin1] p. 36Definition 121Cdf-smblfn 47526  issmf 47558  issmff 47564  issmfge 47600  issmfgelem 47599  issmfgt 47586  issmfgtlem 47585  issmfle 47575  issmflelem 47574  issmflem 47557
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47537  salpreimagtlt 47560  salpreimalelt 47559
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47600  issmfgelem 47599
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47583
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47581  cnfsmf 47570
[Fremlin1] p. 36Proposition 121D (c)decsmf 47597  decsmflem 47596  incsmf 47572  incsmflem 47571
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47531  pimconstlt1 47532  smfconst 47579
[Fremlin1] p. 37Proposition 121E (b)smfadd 47595  smfaddlem1 47593  smfaddlem2 47594
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47626
[Fremlin1] p. 37Proposition 121E (d)smfmul 47625  smfmullem1 47621  smfmullem2 47622  smfmullem3 47623  smfmullem4 47624
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47627
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47630  smfpimbor1lem2 47629
[Fremlin1] p. 37Proposition 121E (g)smfco 47632
[Fremlin1] p. 37Proposition 121E (h)smfres 47620
[Fremlin1] p. 38Proposition 121E (e)smfrec 47619
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47628  smfresal 47618
[Fremlin1] p. 38Proposition 121F (a)smflim 47607  smflim2 47636  smflimlem1 47601  smflimlem2 47602  smflimlem3 47603  smflimlem4 47604  smflimlem5 47605  smflimlem6 47606  smflimmpt 47640
[Fremlin1] p. 38Proposition 121F (b)smfsup 47644  smfsuplem1 47641  smfsuplem2 47642  smfsuplem3 47643  smfsupmpt 47645  smfsupxr 47646
[Fremlin1] p. 38Proposition 121F (c)smfinf 47648  smfinflem 47647  smfinfmpt 47649
[Fremlin1] p. 39Remark 121Gsmflim 47607  smflim2 47636  smflimmpt 47640
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47638
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47668  smfdivdmmbl2 47671  smfinfdmmbl 47679  smfinfdmmbllem 47678  smfsupdmmbl 47675  smfsupdmmbllem 47674
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47658  smflimsuplem2 47651  smflimsuplem6 47655  smflimsuplem7 47656  smflimsuplem8 47657  smflimsupmpt 47659
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47661  smfliminflem 47660  smfliminfmpt 47662
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47526
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47672  fsupdm2 47673
[Fremlin1], p. 39Proposition 121Hadddmmbl 47663  adddmmbl2 47664  finfdm 47676  finfdm2 47677  fsupdm 47672  fsupdm2 47673  muldmmbl 47665  muldmmbl2 47666
[Fremlin1], p. 39Proposition 121F (c)finfdm 47676  finfdm2 47677
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25768
[Fremlin5] p. 213Lemma 565Cauniioovol 25811
[Fremlin5] p. 214Lemma 565Cauniioombl 25821
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38449
[Fremlin5] p. 220Theorem 565Maftc1anc 38452
[FreydScedrov] p. 283Axiom of Infinityax-inf 9620  inf1 9604  inf2 9605
[Gleason] p. 117Proposition 9-2.1df-enq 10923  enqer 10933
[Gleason] p. 117Proposition 9-2.2df-1nq 10928  df-nq 10924
[Gleason] p. 117Proposition 9-2.3df-plpq 10920  df-plq 10926
[Gleason] p. 119Proposition 9-2.4caovmo 7654  df-mpq 10921  df-mq 10927
[Gleason] p. 119Proposition 9-2.5df-rq 10929
[Gleason] p. 119Proposition 9-2.6ltexnq 10987
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10988  ltbtwnnq 10990
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10983
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10984
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10991
[Gleason] p. 121Definition 9-3.1df-np 10993
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 11005
[Gleason] p. 121Definition 9-3.1(iii)prnmax 11007
[Gleason] p. 122Definitiondf-1p 10994
[Gleason] p. 122Remark (1)prub 11006
[Gleason] p. 122Lemma 9-3.4prlem934 11045
[Gleason] p. 122Proposition 9-3.2df-ltp 10997
[Gleason] p. 122Proposition 9-3.3ltsopr 11044  psslinpr 11043  supexpr 11066  suplem1pr 11064  suplem2pr 11065
[Gleason] p. 123Proposition 9-3.5addclpr 11030  addclprlem1 11028  addclprlem2 11029  df-plp 10995
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11034
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11033
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11046
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11055  ltexprlem1 11048  ltexprlem2 11049  ltexprlem3 11050  ltexprlem4 11051  ltexprlem5 11052  ltexprlem6 11053  ltexprlem7 11054
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11057  ltaprlem 11056
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11058
[Gleason] p. 124Lemma 9-3.6prlem936 11059
[Gleason] p. 124Proposition 9-3.7df-mp 10996  mulclpr 11032  mulclprlem 11031  reclem2pr 11060
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11041
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11036
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11035
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11040
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11063  reclem3pr 11061  reclem4pr 11062
[Gleason] p. 126Proposition 9-4.1df-enr 11067  enrer 11075
[Gleason] p. 126Proposition 9-4.2df-0r 11072  df-1r 11073  df-nr 11068
[Gleason] p. 126Proposition 9-4.3df-mr 11070  df-plr 11069  negexsr 11114  recexsr 11119  recexsrlem 11115
[Gleason] p. 127Proposition 9-4.4df-ltr 11071
[Gleason] p. 130Proposition 10-1.3creui 12240  creur 12239  cru 12237
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11200  axcnre 11176
[Gleason] p. 132Definition 10-3.1crim 15204  crimd 15321  crimi 15282  crre 15203  crred 15320  crrei 15281
[Gleason] p. 132Definition 10-3.2remim 15206  remimd 15287
[Gleason] p. 133Definition 10.36absval2 15373  absval2d 15537  absval2i 15487
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15230  cjaddd 15309  cjaddi 15277
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15231  cjmuld 15310  cjmuli 15278
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15229  cjcjd 15288  cjcji 15260
[Gleason] p. 133Proposition 10-3.4(f)cjre 15228  cjreb 15212  cjrebd 15291  cjrebi 15263  cjred 15315  rere 15211  rereb 15209  rerebd 15290  rerebi 15262  rered 15313
[Gleason] p. 133Proposition 10-3.4(h)addcj 15237  addcjd 15301  addcji 15272
[Gleason] p. 133Proposition 10-3.7(a)absval 15327
[Gleason] p. 133Proposition 10-3.7(b)abscj 15368  abscjd 15542  abscji 15491
[Gleason] p. 133Proposition 10-3.7(c)abs00 15378  abs00d 15538  abs00i 15488  absne0d 15539
[Gleason] p. 133Proposition 10-3.7(d)releabs 15411  releabsd 15543  releabsi 15492
[Gleason] p. 133Proposition 10-3.7(f)absmul 15383  absmuld 15546  absmuli 15494
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15371  sqabsaddi 15495
[Gleason] p. 133Proposition 10-3.7(h)abstri 15420  abstrid 15548  abstrii 15498
[Gleason] p. 134Definition 10-4.1df-exp 14128  exp0 14131  expp1 14134  expp1d 14213
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26917  cxpaddd 26955  expadd 14170  expaddd 14214  expaddz 14172
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26926  cxpmuld 26975  expmul 14173  expmuld 14215  expmulz 14174
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26923  mulcxpd 26966  mulexp 14167  mulexpd 14227  mulexpz 14168
[Gleason] p. 140Exercise 1znnen 16304
[Gleason] p. 141Definition 11-2.1fzval 13565
[Gleason] p. 168Proposition 12-2.1(a)climadd 15721  rlimadd 15732  rlimdiv 15735
[Gleason] p. 168Proposition 12-2.1(b)climsub 15723  rlimsub 15733
[Gleason] p. 168Proposition 12-2.1(c)climmul 15722  rlimmul 15734
[Gleason] p. 171Corollary 12-2.2climmulc2 15726
[Gleason] p. 172Corollary 12-2.5climrecl 15672
[Gleason] p. 172Proposition 12-2.4(c)climabs 15693  climcj 15694  climim 15696  climre 15695  rlimabs 15698  rlimcj 15699  rlimim 15701  rlimre 15700
[Gleason] p. 173Definition 12-3.1df-ltxr 11275  df-xr 11274  ltxr 13168
[Gleason] p. 175Definition 12-4.1df-limsup 15560  limsupval 15563
[Gleason] p. 180Theorem 12-5.1climsup 15759
[Gleason] p. 180Theorem 12-5.3caucvg 15768  caucvgb 15769  caucvgbf 46319  caucvgr 15765  climcau 15760
[Gleason] p. 182Exercise 3cvgcmp 15905
[Gleason] p. 182Exercise 4cvgrat 15974
[Gleason] p. 195Theorem 13-2.12abs1m 15425
[Gleason] p. 217Lemma 13-4.1btwnzge0 13891
[Gleason] p. 223Definition 14-1.1df-met 21583
[Gleason] p. 223Definition 14-1.1(a)met0 24573  xmet0 24572
[Gleason] p. 223Definition 14-1.1(b)metgt0 24589
[Gleason] p. 223Definition 14-1.1(c)metsym 24580
[Gleason] p. 223Definition 14-1.1(d)mettri 24582  mstri 24699  xmettri 24581  xmstri 24698
[Gleason] p. 225Definition 14-1.5xpsmet 24612
[Gleason] p. 230Proposition 14-2.6txlm 23878
[Gleason] p. 240Theorem 14-4.3metcnp4 25542
[Gleason] p. 240Proposition 14-4.2metcnp3 24770
[Gleason] p. 243Proposition 14-4.16addcn 25096  addcn2 15683  mulcn 25098  mulcn2 15685  subcn 25097  subcn2 15684
[Gleason] p. 295Remarkbcval3 14372  bcval4 14373
[Gleason] p. 295Equation 2bcpasc 14387
[Gleason] p. 295Definition of binomial coefficientbcval 14370  df-bc 14369
[Gleason] p. 296Remarkbcn0 14376  bcnn 14378
[Gleason] p. 296Theorem 15-2.8binom 15921
[Gleason] p. 308Equation 2ef0 16181
[Gleason] p. 308Equation 3efcj 16182
[Gleason] p. 309Corollary 15-4.3efne0 16188
[Gleason] p. 309Corollary 15-4.4efexp 16193
[Gleason] p. 310Equation 14sinadd 16256
[Gleason] p. 310Equation 15cosadd 16257
[Gleason] p. 311Equation 17sincossq 16268
[Gleason] p. 311Equation 18cosbnd 16273  sinbnd 16272
[Gleason] p. 311Lemma 15-4.7sqeqor 14282  sqeqori 14280
[Gleason] p. 311Definition of ` `df-pi 16162
[Godowski] p. 730Equation SFgoeqi 32755
[GodowskiGreechie] p. 249Equation IV3oai 32150
[Golan] p. 1Remarksrgisid 20352
[Golan] p. 1Definitiondf-srg 20330
[Golan] p. 149Definitiondf-slmd 33643
[Gonshor] p. 7Definitiondf-cuts 28026
[Gonshor] p. 9Theorem 2.5lesrec 28065  lesrecd 28066
[Gonshor] p. 10Theorem 2.6cofcut1 28186  cofcut1d 28187
[Gonshor] p. 10Theorem 2.7cofcut2 28188  cofcut2d 28189
[Gonshor] p. 12Theorem 2.9cofcutr 28190  cofcutr1d 28191  cofcutr2d 28192
[Gonshor] p. 13Definitiondf-adds 28226
[Gonshor] p. 14Theorem 3.1addsprop 28242
[Gonshor] p. 15Theorem 3.2addsunif 28268
[Gonshor] p. 17Theorem 3.4mulsprop 28396
[Gonshor] p. 18Theorem 3.5mulsunif 28416
[Gonshor] p. 28Lemma 4.2halfcut 28724
[Gonshor] p. 28Theorem 4.2pw2cut 28726
[Gonshor] p. 30Theorem 4.2addhalfcut 28725
[Gonshor] p. 39Theorem 4.4(b)elreno2 28761
[Gonshor] p. 95Theorem 6.1addbday 28284
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36741
[Gratzer] p. 23Section 0.6df-mre 17674
[Gratzer] p. 27Section 0.6df-mri 17676
[Hall] p. 1Section 1.1df-asslaw 49105  df-cllaw 49103  df-comlaw 49104
[Hall] p. 2Section 1.2df-clintop 49117
[Hall] p. 7Section 1.3df-sgrp2 49138
[Halmos] p. 28Partition ` `df-parts 39618  dfmembpart2 39623
[Halmos] p. 31Theorem 17.3riesz1 32547  riesz2 32548
[Halmos] p. 41Definition of Hermitianhmopadj2 32423
[Halmos] p. 42Definition of projector orderingpjordi 32655
[Halmos] p. 43Theorem 26.1elpjhmop 32667  elpjidm 32666  pjnmopi 32630
[Halmos] p. 44Remarkpjinormi 32169  pjinormii 32158
[Halmos] p. 44Theorem 26.2elpjch 32671  pjrn 32189  pjrni 32184  pjvec 32178
[Halmos] p. 44Theorem 26.3pjnorm2 32209
[Halmos] p. 44Theorem 26.4hmopidmpj 32636  hmopidmpji 32634
[Halmos] p. 45Theorem 27.1pjinvari 32673
[Halmos] p. 45Theorem 27.3pjoci 32662  pjocvec 32179
[Halmos] p. 45Theorem 27.4pjorthcoi 32651
[Halmos] p. 48Theorem 29.2pjssposi 32654
[Halmos] p. 48Theorem 29.3pjssdif1i 32657  pjssdif2i 32656
[Halmos] p. 50Definition of spectrumdf-spec 32337
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 24
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1828
[Hatcher] p. 25Definitiondf-phtpc 25224  df-phtpy 25203
[Hatcher] p. 26Definitiondf-pco 25237  df-pi1 25240
[Hatcher] p. 26Proposition 1.2phtpcer 25227
[Hatcher] p. 26Proposition 1.3pi1grp 25282
[Hefferon] p. 240Definition 3.12df-dmat 22716  df-dmatalt 49330
[Helfgott] p. 2Theoremtgoldbach 48735
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48720
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48732  bgoldbtbnd 48727  bgoldbtbnd 48727  tgblthelfgott 48733
[Helfgott] p. 5Proposition 1.1circlevma 35152
[Helfgott] p. 69Statement 7.49circlemethhgt 35153
[Helfgott] p. 69Statement 7.50hgt750lema 35167  hgt750lemb 35166  hgt750leme 35168  hgt750lemf 35163  hgt750lemg 35164
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48729  tgoldbachgt 35173  tgoldbachgtALTV 48730  tgoldbachgtd 35172
[Helfgott] p. 70Statement 7.49ax-hgt749 35154
[Herstein] p. 54Exercise 28df-grpo 30975
[Herstein] p. 55Lemma 2.2.1(a)grpideu 19072  grpoideu 30991  mndideu 18851
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19102  grpoinveu 31001
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19133  grpo2inv 31013
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19145  grpoinvop 31015
[Herstein] p. 57Exercise 1dfgrp3e 19167
[Hitchcock] p. 5Rule A3mptnan 1801
[Hitchcock] p. 5Rule A4mptxor 1802
[Hitchcock] p. 5Rule A5mtpxor 1804
[Holland] p. 1519Theorem 2sumdmdi 32902
[Holland] p. 1520Lemma 5cdj1i 32915  cdj3i 32923  cdj3lem1 32916  cdjreui 32914
[Holland] p. 1524Lemma 7mddmdin0i 32913
[Holland95] p. 13Theorem 3.6hlathil 42836
[Holland95] p. 14Line 15hgmapvs 42766
[Holland95] p. 14Line 16hdmaplkr 42788
[Holland95] p. 14Line 17hdmapellkr 42789
[Holland95] p. 14Line 19hdmapglnm2 42786
[Holland95] p. 14Line 20hdmapip0com 42792
[Holland95] p. 14Theorem 3.6hdmapevec2 42711
[Holland95] p. 14Lines 24 and 25hdmapoc 42806
[Holland95] p. 204Definition of involutiondf-srng 21010
[Holland95] p. 212Definition of subspacedf-psubsp 40378
[Holland95] p. 214Lemma 3.3lclkrlem2v 42403
[Holland95] p. 214Definition 3.2df-lpolN 42356
[Holland95] p. 214Definition of nonsingularpnonsingN 40808
[Holland95] p. 215Lemma 3.3(1)dihoml4 42252  poml4N 40828
[Holland95] p. 215Lemma 3.3(2)dochexmid 42343  pexmidALTN 40853  pexmidN 40844
[Holland95] p. 218Theorem 3.6lclkr 42408
[Holland95] p. 218Definition of dual vector spacedf-ldual 39999  ldualset 40000
[Holland95] p. 222Item 1df-lines 40376  df-pointsN 40377
[Holland95] p. 222Item 2df-polarityN 40778
[Holland95] p. 223Remarkispsubcl2N 40822  omllaw4 40121  pol1N 40785  polcon3N 40792
[Holland95] p. 223Definitiondf-psubclN 40810
[Holland95] p. 223Equation for polaritypolval2N 40781
[Holmes] p. 40Definitiondf-xrn 39130
[Hughes] p. 44Equation 1.21bax-his3 31566
[Hughes] p. 47Definition of projection operatordfpjop 32664
[Hughes] p. 49Equation 1.30eighmre 32445  eigre 32317  eigrei 32316
[Hughes] p. 49Equation 1.31eighmorth 32446  eigorth 32320  eigorthi 32319
[Hughes] p. 137Remark (ii)eigposi 32318
[Huneke] p. 1Claim 1frgrncvvdeq 30790
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30786
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30787
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30788
[Huneke] p. 2Claim 2frgrregorufr 30806  frgrregorufr0 30805  frgrregorufrg 30807
[Huneke] p. 2Claim 3frgrhash2wsp 30813  frrusgrord 30822  frrusgrord0 30821
[Huneke] p. 2Statementdf-clwwlknon 30559
[Huneke] p. 2Statement 4frgrwopreglem4 30796
[Huneke] p. 2Statement 5frgrwopreg1 30799  frgrwopreg2 30800  frgrwopregasn 30797  frgrwopregbsn 30798
[Huneke] p. 2Statement 6frgrwopreglem5 30802
[Huneke] p. 2Statement 7fusgreghash2wspv 30816
[Huneke] p. 2Statement 8fusgreghash2wsp 30819
[Huneke] p. 2Statement 9clwlksndivn 30557  numclwlk1 30852  numclwlk1lem1 30850  numclwlk1lem2 30851  numclwwlk1 30842  numclwwlk8 30873
[Huneke] p. 2Definition 3frgrwopreglem1 30793
[Huneke] p. 2Definition 4df-clwlks 30238
[Huneke] p. 2Definition 62clwwlk 30828
[Huneke] p. 2Definition 7numclwwlkovh 30854  numclwwlkovh0 30853
[Huneke] p. 2Statement 10numclwwlk2 30862
[Huneke] p. 2Statement 11rusgrnumwlkg 30449
[Huneke] p. 2Statement 12numclwwlk3 30866
[Huneke] p. 2Statement 13numclwwlk5 30869
[Huneke] p. 2Statement 14numclwwlk7 30872
[Indrzejczak] p. 33Definition ` `Enatded 30884  natded 30884
[Indrzejczak] p. 33Definition ` `Inatded 30884
[Indrzejczak] p. 34Definition ` `Enatded 30884  natded 30884
[Indrzejczak] p. 34Definition ` `Inatded 30884
[Jech] p. 4Definition of classcv 1569  cvjust 2756
[Jech] p. 42Lemma 6.1alephexp1 10591
[Jech] p. 42Equation 6.1alephadd 10589  alephmul 10590
[Jech] p. 43Lemma 6.2infmap 10588  infmap2 10222
[Jech] p. 71Lemma 9.3jech9.3 9799
[Jech] p. 72Equation 9.3df-scott 9871
[Jech] p. 72Exercise 9.1rankval4 9852  rankval4b 35609
[Jech] p. 72Scheme "Collection Principle"cp 9896
[Jech] p. 78Noteopthprc 5723
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43758
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43846
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43847
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43770
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43774
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43775  rmyp1 43776
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43777  rmym1 43778
[JonesMatijasevic] p. 695Equation 2.11rmx0 43768  rmx1 43769  rmxluc 43779
[JonesMatijasevic] p. 695Equation 2.12rmy0 43772  rmy1 43773  rmyluc 43780
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43782
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43783
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43803  jm2.17b 43804  jm2.17c 43805
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43836
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43840
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43831
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43806  jm2.24nn 43802
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43845
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43851  rmygeid 43807
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43863
[Juillerat] p. 11Section *5etransc 47113  etransclem47 47111  etransclem48 47112
[Juillerat] p. 12Equation (7)etransclem44 47108
[Juillerat] p. 12Equation *(7)etransclem46 47110
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 47096
[Juillerat] p. 13Proofetransclem35 47099
[Juillerat] p. 13Part of case 2 proven inetransclem38 47102
[Juillerat] p. 13Part of case 2 provenetransclem24 47088
[Juillerat] p. 13Part of case 2: proven inetransclem41 47105
[Juillerat] p. 14Proofetransclem23 47087
[KalishMontague] p. 81Note 1ax-6 2000
[KalishMontague] p. 85Lemma 2equid 2045
[KalishMontague] p. 85Lemma 3equcomi 2050
[KalishMontague] p. 86Lemma 7cbvalivw 2040  cbvaliw 2039  wl-cbvmotv 38278  wl-motae 38280  wl-moteq 38279
[KalishMontague] p. 87Lemma 8spimvw 2019  spimw 2003
[KalishMontague] p. 87Lemma 9spfw 2066  spw 2067
[Kalmbach] p. 14Definition of latticechabs1 31998  chabs1i 32000  chabs2 31999  chabs2i 32001  chjass 32015  chjassi 31968  latabs1 18567  latabs2 18568
[Kalmbach] p. 15Definition of atomdf-at 32820  ela 32821
[Kalmbach] p. 15Definition of coverscvbr2 32765  cvrval2 40149
[Kalmbach] p. 16Definitiondf-ol 40053  df-oml 40054
[Kalmbach] p. 20Definition of commutescmbr 32066  cmbri 32072  cmtvalN 40086  df-cm 32065  df-cmtN 40052
[Kalmbach] p. 22Remarkomllaw5N 40122  pjoml5 32095  pjoml5i 32070
[Kalmbach] p. 22Definitionpjoml2 32093  pjoml2i 32067
[Kalmbach] p. 22Theorem 2(v)cmcm 32096  cmcmi 32074  cmcmii 32079  cmtcomN 40124
[Kalmbach] p. 22Theorem 2(ii)omllaw3 40120  omlsi 31886  pjoml 31918  pjomli 31917
[Kalmbach] p. 22Definition of OML lawomllaw2N 40119
[Kalmbach] p. 23Remarkcmbr2i 32078  cmcm3 32097  cmcm3i 32076  cmcm3ii 32081  cmcm4i 32077  cmt3N 40126  cmt4N 40127  cmtbr2N 40128
[Kalmbach] p. 23Lemma 3cmbr3 32090  cmbr3i 32082  cmtbr3N 40129
[Kalmbach] p. 25Theorem 5fh1 32100  fh1i 32103  fh2 32101  fh2i 32104  omlfh1N 40133
[Kalmbach] p. 65Remarkchjatom 32839  chslej 31980  chsleji 31940  shslej 31862  shsleji 31852
[Kalmbach] p. 65Proposition 1chocin 31977  chocini 31936  chsupcl 31822  chsupval2 31892  h0elch 31737  helch 31725  hsupval2 31891  ocin 31778  ococss 31775  shococss 31776
[Kalmbach] p. 65Definition of subspace sumshsval 31794
[Kalmbach] p. 66Remarkdf-pjh 31877  pjssmi 32647  pjssmii 32163
[Kalmbach] p. 67Lemma 3osum 32127  osumi 32124
[Kalmbach] p. 67Lemma 4pjci 32682
[Kalmbach] p. 103Exercise 6atmd2 32882
[Kalmbach] p. 103Exercise 12mdsl0 32792
[Kalmbach] p. 140Remarkhatomic 32842  hatomici 32841  hatomistici 32844
[Kalmbach] p. 140Proposition 1atlatmstc 40194
[Kalmbach] p. 140Proposition 1(i)atexch 32863  lsatexch 39918
[Kalmbach] p. 140Proposition 1(ii)chcv1 32837  cvlcvr1 40214  cvr1 40285
[Kalmbach] p. 140Proposition 1(iii)cvexch 32856  cvexchi 32851  cvrexch 40295
[Kalmbach] p. 149Remark 2chrelati 32846  hlrelat 40277  hlrelat5N 40276  lrelat 39889
[Kalmbach] p. 153Exercise 5lsmcv 21332  lsmsatcv 39885  spansncv 32135  spansncvi 32134
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39904  spansncv2 32775
[Kalmbach] p. 266Definitiondf-st 32693
[Kalmbach2] p. 8Definition of adjointdf-adjh 32331
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10658  fpwwe2 10655
[KanamoriPincus] p. 416Corollary 1.3canth4 10659
[KanamoriPincus] p. 417Corollary 1.6canthp1 10666
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10661
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10663
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10676
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10680  gchxpidm 10681
[KanamoriPincus] p. 419Theorem 2.1gchacg 10692  gchhar 10691
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10220  unxpwdom 9564
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10682
[Kreyszig] p. 3Property M1metcl 24562  xmetcl 24561
[Kreyszig] p. 4Property M2meteq0 24569
[Kreyszig] p. 8Definition 1.1-8dscmet 24802
[Kreyszig] p. 12Equation 5conjmul 11959  muleqadd 11885
[Kreyszig] p. 18Definition 1.3-2mopnval 24668
[Kreyszig] p. 19Remarkmopntopon 24669
[Kreyszig] p. 19Theorem T1mopn0 24728  mopnm 24674
[Kreyszig] p. 19Theorem T2unimopn 24726
[Kreyszig] p. 19Definition of neighborhoodneibl 24731
[Kreyszig] p. 20Definition 1.3-3metcnp2 24772
[Kreyszig] p. 25Definition 1.4-1lmbr 23487  lmmbr 25490  lmmbr2 25491
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23609
[Kreyszig] p. 28Theorem 1.4-5lmcau 25545
[Kreyszig] p. 28Definition 1.4-3iscau 25508  iscmet2 25526
[Kreyszig] p. 30Theorem 1.4-7cmetss 25548
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23691  metelcls 25537
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25538  metcld2 25539
[Kreyszig] p. 51Equation 2clmvneg1 25331  lmodvneg1 21093  nvinv 31121  vcm 31058
[Kreyszig] p. 51Equation 1aclm0vs 25327  lmod0vs 21083  slmd0vs 33666  vc0 31056
[Kreyszig] p. 51Equation 1blmodvs0 21084  slmdvs0 33667  vcz 31057
[Kreyszig] p. 58Definition 2.2-1imsmet 31173  ngpmet 24833  nrmmetd 24804
[Kreyszig] p. 59Equation 1imsdval 31168  imsdval2 31169  ncvspds 25393  ngpds 24834
[Kreyszig] p. 63Problem 1nmval 24819  nvnd 31170
[Kreyszig] p. 64Problem 2nmeq0 24848  nmge0 24847  nvge0 31155  nvz 31151
[Kreyszig] p. 64Problem 3nmrtri 24854  nvabs 31154
[Kreyszig] p. 91Definition 2.7-1isblo3i 31283
[Kreyszig] p. 92Equation 2df-nmoo 31227
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 31289  blocni 31287
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 31288
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25436  ipeq0 21855  ipz 31201
[Kreyszig] p. 135Problem 2cphpyth 25448  pythi 31332
[Kreyszig] p. 137Lemma 3-2.1(a)sii 31336
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25470
[Kreyszig] p. 144Equation 4supcvg 15947
[Kreyszig] p. 144Theorem 3.3-1minvec 25668  minveco 31366
[Kreyszig] p. 196Definition 3.9-1df-aj 31232
[Kreyszig] p. 247Theorem 4.7-2bcth 25561
[Kreyszig] p. 249Theorem 4.7-3ubth 31355
[Kreyszig] p. 470Definition of positive operator orderingleop 32605  leopg 32604
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32623
[Kreyszig] p. 525Theorem 10.1-1htth 31400
[Kulpa] p. 547Theorempoimir 38404
[Kulpa] p. 547Equation (1)poimirlem32 38403
[Kulpa] p. 547Equation (2)poimirlem31 38402
[Kulpa] p. 548Theorembroucube 38405
[Kulpa] p. 548Equation (6)poimirlem26 38397
[Kulpa] p. 548Equation (7)poimirlem27 38398
[Kunen] p. 10Axiom 0ax6e 2414  axnul 5266
[Kunen] p. 11Axiom 3axnul 5266
[Kunen] p. 12Axiom 6zfrep6 5248
[Kunen] p. 24Definition 10.24mapval 8840  mapvalg 8838
[Kunen] p. 30Lemma 10.20fodomg 10527
[Kunen] p. 31Definition 10.24mapex 7940
[Kunen] p. 95Definition 2.1df-r1 9749
[Kunen] p. 97Lemma 2.10r1elss 9791  r1elssi 9790
[Kunen] p. 107Exercise 4rankop 9843  rankopb 9837  rankuni 9848  rankxplim 9864  rankxpsuc 9867
[Kunen2] p. 47Lemma I.9.9relpfr 45779
[Kunen2] p. 53Lemma I.9.21trfr 45787
[Kunen2] p. 53Lemma I.9.24(2)wffr 45786
[Kunen2] p. 53Definition I.9.20tcfr 45788
[Kunen2] p. 95Lemma I.16.2ralabso 45793  rexabso 45794
[Kunen2] p. 96Example I.16.3disjabso 45800  n0abso 45801  ssabso 45799
[Kunen2] p. 111Lemma II.2.4(1)traxext 45802
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45812
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45807
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45810
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45811
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45806
[Kunen2] p. 112Corollary II.2.5wfaxext 45818  wfaxpr 45823  wfaxreg 45825  wfaxrep 45819  wfaxsep 45820  wfaxun 45824
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45809
[Kunen2] p. 113Corollary II.2.9wfaxpow 45822
[Kunen2] p. 114Theorem II.2.13wfaxext 45818
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45817  omelaxinf2 45814
[Kunen2] p. 114Corollary II.2.12wfac8prim 45827  wfaxinf2 45826
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45840  permaxext 45830  permaxinf2 45838  permaxnul 45833  permaxpow 45834  permaxpr 45835  permaxrep 45831  permaxsep 45832  permaxun 45836
[Kunen2] p. 148Definition II.9.1brpermmodel 45828
[Kunen2] p. 149Exercise II.9.3permac8prim 45839
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4967
[Lang] , p. 225Corollary 1.3finexttrb 34177
[Lang] p. Definitiondf-rn 5670
[Lang] p. 3Statementlidrideqd 18767  mndbn0 18857
[Lang] p. 3Definitiondf-mnd 18841
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18793
[Lang] p. 4Property of composites. Second formulagsumccat 18954
[Lang] p. 5Equationgsumreidx 20048
[Lang] p. 5Definition of an (infinite) productgsumfsupp 49099
[Lang] p. 6Examplenn0mnd 49096
[Lang] p. 6Equationgsumxp2 20111
[Lang] p. 6Statementcycsubm 19334
[Lang] p. 6Definitionmulgnn0gsum 19207
[Lang] p. 6Observationmndlsmidm 19801
[Lang] p. 7Definitiondfgrp2e 19091
[Lang] p. 30Definitiondf-tocyc 33549
[Lang] p. 32Property (a)cyc3genpm 33594
[Lang] p. 32Property (b)cyc3conja 33599  cycpmconjv 33584
[Lang] p. 53Definitiondf-cat 17760
[Lang] p. 53Axiom CAT 1cat1 18190  cat1lem 18189
[Lang] p. 54Definitiondf-iso 17842
[Lang] p. 57Definitiondf-inito 18077  df-termo 18078
[Lang] p. 58Exampleirinitoringc 21696
[Lang] p. 58Statementinitoeu1 18104  termoeu1 18111
[Lang] p. 62Definitiondf-func 17951
[Lang] p. 65Definitiondf-nat 18039
[Lang] p. 83Definition of "ring with unit"dfring2 20433
[Lang] p. 91Notedf-ringc 20812
[Lang] p. 92Statementmxidlprm 33875
[Lang] p. 92Definitionisprmidlc 21539
[Lang] p. 128Remarkdsmmlmod 21962
[Lang] p. 129Prooflincscm 49362  lincscmcl 49364  lincsum 49361  lincsumcl 49363
[Lang] p. 129Statementlincolss 49366
[Lang] p. 129Observationdsmmfi 21955
[Lang] p. 141Theorem 5.3dimkerim 34139  qusdimsum 34140
[Lang] p. 141Corollary 5.4lssdimle 34120
[Lang] p. 147Definitionsnlindsntor 49403
[Lang] p. 504Statementmat1 22673  matring 22669
[Lang] p. 504Definitiondf-mamu 22617
[Lang] p. 505Statementmamuass 22628  mamutpos 22684  matassa 22670  mattposvs 22681  tposmap 22683
[Lang] p. 513Definitionmdet1 22827  mdetf 22821
[Lang] p. 513Theorem 4.4cramer 22920
[Lang] p. 514Proposition 4.6mdetleib 22813
[Lang] p. 514Proposition 4.8mdettpos 22837
[Lang] p. 515Definitiondf-minmar1 22861  smadiadetr 22901
[Lang] p. 515Corollary 4.9mdetero 22836  mdetralt 22834
[Lang] p. 517Proposition 4.15mdetmul 22849
[Lang] p. 518Definitiondf-madu 22860
[Lang] p. 518Proposition 4.16madulid 22871  madurid 22870  matinv 22903
[Lang] p. 561Theorem 3.1cayleyhamilton 23119
[Lang], p. 190Chapter 6vieta 34092
[Lang], p. 224Proposition 1.1extdgfialg 34206  finextalg 34210
[Lang], p. 224Proposition 1.2extdgmul 34175  fedgmul 34143
[Lang], p. 225Proposition 1.4algextdeg 34237
[Lang], p. 561Remarkchpmatply1 23061
[Lang], p. 561Definitiondf-chpmat 23056
[Lang2] p. 3Notationsdf-ind 12246
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 45160
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 45155
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 45161
[LeBlanc] p. 277Rule R2axnul 5266
[Levy] p. 12Axiom 4.3.1df-clab 2741  wl-df.clab 38263
[Levy] p. 59Definitiondf-ttrcl 9690
[Levy] p. 64Theorem 5.6(ii)frinsg 9736
[Levy] p. 338Axiomdf-clel 2837  df-cleq 2754  wl-df.cleq 38264
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 38267
[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 38267
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2837  df-cleq 2754  wl-df.cleq 38264
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2741  wl-df.clab 38263
[Levy] p. 358Axiomdf-clab 2741  wl-df.clab 38263
[Levy58] p. 2Definition Iisfin1-3 10391
[Levy58] p. 2Definition IIdf-fin2 10291
[Levy58] p. 2Definition Iadf-fin1a 10290
[Levy58] p. 2Definition IIIdf-fin3 10293
[Levy58] p. 3Definition Vdf-fin5 10294
[Levy58] p. 3Definition IVdf-fin4 10292
[Levy58] p. 4Definition VIdf-fin6 10295
[Levy58] p. 4Definition VIIdf-fin7 10296
[Levy58], p. 3Theorem 1fin1a2 10420
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27923
[Lipparini] p. 3Lemma 2.1.4noresle 27934
[Lipparini] p. 6Proposition 4.2noinfbnd1 27966  nosupbnd1 27951
[Lipparini] p. 6Proposition 4.3noinfbnd2 27968  nosupbnd2 27953
[Lipparini] p. 7Theorem 5.1noetasuplem3 27972  noetasuplem4 27973
[Lipparini] p. 7Corollary 4.4nosupinfsep 27969
[Lopez-Astorga] p. 12Rule 1mptnan 1801
[Lopez-Astorga] p. 12Rule 2mptxor 1802
[Lopez-Astorga] p. 12Rule 3mtpxor 1804
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32890
[Maeda] p. 168Lemma 5mdsym 32894  mdsymi 32893
[Maeda] p. 168Lemma 4(i)mdsymlem4 32888  mdsymlem6 32890  mdsymlem7 32891
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32892
[MaedaMaeda] p. 1Remarkssdmd1 32795  ssdmd2 32796  ssmd1 32793  ssmd2 32794
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32791
[MaedaMaeda] p. 1Definition 1.1df-dmd 32763  df-md 32762  mdbr 32776
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32813  mdslj1i 32801  mdslj2i 32802  mdslle1i 32799  mdslle2i 32800  mdslmd1i 32811  mdslmd2i 32812
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32803  mdsl2bi 32805  mdsl2i 32804
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32817
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32814
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32815
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32792
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32797  mdsl3 32798
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32816
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32911
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 40196  hlrelat1 40275
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39914
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32818  cvmdi 32806  cvnbtwn4 32771  cvrnbtwn4 40154
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32819
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 40215  cvp 32857  cvrp 40291  lcvp 39915
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32881
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32880
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 40208  hlexch4N 40267
[MaedaMaeda] p. 34Exercise 7.1atabsi 32883
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40318
[MaedaMaeda] p. 61Definition 15.10psubN 40624  atpsubN 40628  df-pointsN 40377  pointpsubN 40626
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40379  pmap11 40637  pmaple 40636  pmapsub 40643  pmapval 40632
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40640  pmap1N 40642
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40645  pmapglb2N 40646  pmapglb2xN 40647  pmapglbx 40644
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40727
[MaedaMaeda] p. 67Postulate PS1ps-1 40352
[MaedaMaeda] p. 68Lemma 16.2df-padd 40671  paddclN 40717  paddidm 40716
[MaedaMaeda] p. 68Condition PS2ps-2 40353
[MaedaMaeda] p. 68Equation 16.2.1paddass 40713
[MaedaMaeda] p. 69Lemma 16.4ps-1 40352
[MaedaMaeda] p. 69Theorem 16.4ps-2 40353
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19806  lsmmod2 19807  lssats 39887  shatomici 32840  shatomistici 32843  shmodi 31872  shmodsi 31871
[MaedaMaeda] p. 130Remark 29.6dmdmd 32782  mdsymlem7 32891
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 32071
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31975
[MaedaMaeda] p. 139Remarksumdmdii 32897
[Margaris] p. 40Rule Cexlimiv 1963
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 402  df-ex 1813  df-or 862  dfbi2 480
[Margaris] p. 51Theorem 1idALT 24
[Margaris] p. 56Theorem 3conventions 30881
[Margaris] p. 59Section 14notnotrALTVD 45739
[Margaris] p. 60Theorem 8jcn 163
[Margaris] p. 60Section 14con3ALTVD 45740
[Margaris] p. 79Rule Cexinst01 45450  exinst11 45451
[Margaris] p. 89Theorem 19.219.2 2009  19.2g 2226  r19.2z 4458
[Margaris] p. 89Theorem 19.319.3 2240  rr19.3v 3624
[Margaris] p. 89Theorem 19.5alcom 2196
[Margaris] p. 89Theorem 19.6alex 1859
[Margaris] p. 89Theorem 19.7alnex 1814
[Margaris] p. 89Theorem 19.819.8a 2219
[Margaris] p. 89Theorem 19.919.9 2243  19.9h 2321  exlimd 2256  exlimdh 2325
[Margaris] p. 89Theorem 19.11excom 2199  excomim 2200
[Margaris] p. 89Theorem 19.1219.12 2359
[Margaris] p. 90Section 19conventions-labels 30882  conventions-labels 30882  conventions-labels 30882  conventions-labels 30882
[Margaris] p. 90Theorem 19.14exnal 1860
[Margaris] p. 90Theorem 19.152albi 45204  albi 1851
[Margaris] p. 90Theorem 19.1619.16 2263
[Margaris] p. 90Theorem 19.1719.17 2264
[Margaris] p. 90Theorem 19.182exbi 45206  exbi 1880
[Margaris] p. 90Theorem 19.1919.19 2267
[Margaris] p. 90Theorem 19.202alim 45203  2alimdv 1951  alimd 2250  alimdh 1850  alimdv 1949  ax-4 1842  ralimdaa 3265  ralimdv 3178  ralimdva 3176  ralimdvva 3211  sbcimdv 3810
[Margaris] p. 90Theorem 19.2119.21 2245  19.21h 2322  19.21t 2244  19.21vv 45202  alrimd 2253  alrimdd 2252  alrimdh 1896  alrimdv 1962  alrimi 2251  alrimih 1857  alrimiv 1960  alrimivv 1961  bj-alrimdh 37327  hbralrimi 3154  r19.21be 3257  r19.21bi 3256  ralrimd 3269  ralrimdv 3162  ralrimdva 3164  ralrimdvv 3208  ralrimdvva 3219  ralrimi 3262  ralrimia 3263  ralrimiv 3155  ralrimiva 3156  ralrimivv 3205  ralrimivva 3207  ralrimivvva 3210  ralrimivw 3160
[Margaris] p. 90Theorem 19.222exim 45205  2eximdv 1952  bj-exim 37342  exim 1867  eximd 2254  eximdh 1897  eximdv 1950  rexim 3105  reximd2a 3274  reximdai 3266  reximdd 45982  reximddv 3180  reximddv2 3223  reximddv3 3181  reximdv 3179  reximdv2 3174  reximdva 3177  reximdvai 3175  reximdvva 3212  reximi2 3097
[Margaris] p. 90Theorem 19.2319.23 2249  19.23bi 2229  19.23h 2323  19.23t 2248  exlimdv 1966  exlimdvv 1967  exlimexi 45349  exlimiv 1963  exlimivv 1965  rexlimd3 45978  rexlimdv 3163  rexlimdv3a 3169  rexlimdva 3165  rexlimdva2 3167  rexlimdvaa 3166  rexlimdvv 3220  rexlimdvva 3221  rexlimdvvva 3222  rexlimdvw 3170  rexlimiv 3158  rexlimiva 3157  rexlimivv 3206
[Margaris] p. 90Theorem 19.2419.24 2024
[Margaris] p. 90Theorem 19.2519.25 1913
[Margaris] p. 90Theorem 19.2619.26 1903
[Margaris] p. 90Theorem 19.2719.27 2265  r19.27z 4469  r19.27zv 4470
[Margaris] p. 90Theorem 19.2819.28 2266  19.28vv 45212  r19.28z 4461  r19.28zf 45993  r19.28zv 4465  rr19.28v 3625
[Margaris] p. 90Theorem 19.2919.29 1906  r19.29d2r 3151  r19.29imd 3129
[Margaris] p. 90Theorem 19.3019.30 1914
[Margaris] p. 90Theorem 19.3119.31 2272  19.31vv 45210
[Margaris] p. 90Theorem 19.3219.32 2271  r19.32 47988
[Margaris] p. 90Theorem 19.3319.33-2 45208  19.33 1917
[Margaris] p. 90Theorem 19.3419.34 2025
[Margaris] p. 90Theorem 19.3519.35 1910
[Margaris] p. 90Theorem 19.3619.36 2268  19.36vv 45209  r19.36zv 4471
[Margaris] p. 90Theorem 19.3719.37 2270  19.37vv 45211  r19.37zv 4466
[Margaris] p. 90Theorem 19.3819.38 1872
[Margaris] p. 90Theorem 19.3919.39 2023
[Margaris] p. 90Theorem 19.4019.40-2 1920  19.40 1919  r19.40 3130
[Margaris] p. 90Theorem 19.4119.41 2273  19.41rg 45375
[Margaris] p. 90Theorem 19.4219.42 2274
[Margaris] p. 90Theorem 19.4319.43 1915
[Margaris] p. 90Theorem 19.4419.44 2275  r19.44zv 4468
[Margaris] p. 90Theorem 19.4519.45 2276  r19.45zv 4467
[Margaris] p. 110Exercise 2(b)eu1 2637
[Mayet] p. 370Remarkjpi 32752  largei 32749  stri 32739
[Mayet3] p. 9Definition of CH-statesdf-hst 32694  ishst 32696
[Mayet3] p. 10Theoremhstrbi 32748  hstri 32747
[Mayet3] p. 1223Theorem 4.1mayete3i 32210
[Mayet3] p. 1240Theorem 7.1mayetes3i 32211
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32760
[MegPav2000] p. 2345Definition 3.4-1chintcl 31814  chsupcl 31822
[MegPav2000] p. 2345Definition 3.4-2hatomic 32842
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32836
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32863
[MegPav2000] p. 2366Figure 7pl42N 40858
[MegPav2002] p. 362Lemma 2.2latj31 18579  latj32 18577  latjass 18575
[Megill] p. 444Axiom C5ax-5 1943  ax5ALT 39782
[Megill] p. 444Section 7conventions 30881
[Megill] p. 445Lemma L12aecom-o 39776  ax-c11n 39763  axc11n 2457
[Megill] p. 446Lemma L17equtrr 2055
[Megill] p. 446Lemma L18ax6fromc10 39771
[Megill] p. 446Lemma L19hbnae-o 39803  hbnae 2463
[Megill] p. 447Remark 9.1dfsb1 2512  sbid 2292  sbidd-misc 50647  sbidd 50646
[Megill] p. 448Remark 9.6axc14 2494
[Megill] p. 448Scheme C4'ax-c4 39759
[Megill] p. 448Scheme C5'ax-c5 39758  sp 2221
[Megill] p. 448Scheme C6'ax-11 2194
[Megill] p. 448Scheme C7'ax-c7 39760
[Megill] p. 448Scheme C8'ax-7 2041
[Megill] p. 448Scheme C9'ax-c9 39765
[Megill] p. 448Scheme C10'ax-6 2000  ax-c10 39761
[Megill] p. 448Scheme C11'ax-c11 39762
[Megill] p. 448Scheme C12'ax-8 2147
[Megill] p. 448Scheme C13'ax-9 2155
[Megill] p. 448Scheme C14'ax-c14 39766
[Megill] p. 448Scheme C15'ax-c15 39764
[Megill] p. 448Scheme C16'ax-c16 39767
[Megill] p. 448Theorem 9.4dral1-o 39779  dral1 2470  dral2-o 39805  dral2 2469  drex1 2472  drex2 2473  drsb1 2526  drsb2 2302
[Megill] p. 449Theorem 9.7sbcom2 2209  sbequ 2120  sbid2v 2540
[Megill] p. 450Example in Appendixhba1-o 39772  hba1 2328
[Mendelson] p. 35Axiom A3hirstL-ax3 47782
[Mendelson] p. 36Lemma 1.8idALT 24
[Mendelson] p. 69Axiom 4rspsbc 3829  rspsbca 3830  stdpc4 2105
[Mendelson] p. 69Axiom 5ax-c4 39759  ra4 3836  stdpc5 2246
[Mendelson] p. 81Rule Cexlimiv 1963
[Mendelson] p. 95Axiom 6stdpc6 2061
[Mendelson] p. 95Axiom 7stdpc7 2287
[Mendelson] p. 225Axiom system NBGru 3741
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5495
[Mendelson] p. 231Exercise 4.10(k)inv1 4351
[Mendelson] p. 231Exercise 4.10(l)unv 4352
[Mendelson] p. 231Exercise 4.10(n)dfin3 4226
[Mendelson] p. 231Exercise 4.10(o)df-nul 4283
[Mendelson] p. 231Exercise 4.10(q)dfin4 4227
[Mendelson] p. 231Exercise 4.10(s)ddif 4091
[Mendelson] p. 231Definition of uniondfun3 4225
[Mendelson] p. 235Exercise 4.12(c)univ 5430
[Mendelson] p. 235Exercise 4.12(d)pwv 4867
[Mendelson] p. 235Exercise 4.12(j)pwin 5550
[Mendelson] p. 235Exercise 4.12(k)pwunss 4578
[Mendelson] p. 235Exercise 4.12(l)pwssun 5551
[Mendelson] p. 235Exercise 4.12(n)uniin 4894
[Mendelson] p. 235Exercise 4.12(p)reli 5811
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6270
[Mendelson] p. 244Proposition 4.8(g)epweon 7777
[Mendelson] p. 246Definition of successordf-suc 6367
[Mendelson] p. 250Exercise 4.36oelim2 8586
[Mendelson] p. 254Proposition 4.22(b)xpen 9141
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9062  xpsneng 9063
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9069  xpcomeng 9070
[Mendelson] p. 254Proposition 4.22(e)xpassen 9072
[Mendelson] p. 255Definitionbrsdom 8983
[Mendelson] p. 255Exercise 4.39endisj 9065
[Mendelson] p. 255Exercise 4.41mapprc 8833
[Mendelson] p. 255Exercise 4.43mapsnen 9047  mapsnend 9046
[Mendelson] p. 255Exercise 4.45mapunen 9147
[Mendelson] p. 255Exercise 4.47xpmapen 9146
[Mendelson] p. 255Exercise 4.42(a)map0e 8892
[Mendelson] p. 255Exercise 4.42(b)map1 9050
[Mendelson] p. 257Proposition 4.24(a)undom 9066
[Mendelson] p. 258Exercise 4.56(c)djuassen 10184  djucomen 10183
[Mendelson] p. 258Exercise 4.56(f)djudom1 10188
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10182
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8521
[Mendelson] p. 266Proposition 4.34(f)oaordex 8548
[Mendelson] p. 275Proposition 4.42(d)entri3 10570
[Mendelson] p. 281Definitiondf-r1 9749
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9798
[Mendelson] p. 287Axiom system MKru 3741
[MertziosUnger] p. 152Definitiondf-frgr 30740
[MertziosUnger] p. 153Remark 1frgrconngr 30775
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30777  vdgn1frgrv3 30778
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30779
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30772
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30765  2pthfrgrrn 30763  2pthfrgrrn2 30764
[Mittelstaedt] p. 9Definitiondf-oc 31734
[Monk1] p. 22Remarkconventions 30881
[Monk1] p. 22Theorem 3.1conventions 30881
[Monk1] p. 26Theorem 2.8(vii)ssin 4187
[Monk1] p. 33Theorem 3.2(i)ssrel 5767  ssrelf 33090
[Monk1] p. 33Theorem 3.2(ii)eqrel 5768
[Monk1] p. 34Definition 3.3df-opab 5172
[Monk1] p. 36Theorem 3.7(i)coi1 6263  coi2 6264
[Monk1] p. 36Theorem 3.8(v)dm0 5908  rn0 5914
[Monk1] p. 36Theorem 3.7(ii)cnvi 5869
[Monk1] p. 37Theorem 3.13(i)relxp 5677
[Monk1] p. 37Theorem 3.13(x)dmxp 5917  rnxp 6167
[Monk1] p. 37Theorem 3.13(ii)0xp 5758  xp0 5759
[Monk1] p. 38Theorem 3.16(ii)ima0 6077
[Monk1] p. 38Theorem 3.16(viii)imai 6074
[Monk1] p. 39Theorem 3.17imaex 7914  imaexg 7913
[Monk1] p. 39Theorem 3.16(xi)imassrn 6071
[Monk1] p. 41Theorem 4.3(i)fnopfv 7071  funfvop 7046
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6936
[Monk1] p. 42Theorem 4.4(iii)fvelima 6947
[Monk1] p. 43Theorem 4.6funun 6583
[Monk1] p. 43Theorem 4.8(iv)dff13 7254  dff13f 7255
[Monk1] p. 46Theorem 4.15(v)funex 7221  funrnex 7954
[Monk1] p. 50Definition 5.4fniunfv 7247
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6227
[Monk1] p. 52Theorem 5.11(viii)ssint 4927
[Monk1] p. 52Definition 5.13 (i)1stval2 8006  df-1st 7989
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8007  df-2nd 7990
[Monk1] p. 112Theorem 15.17(v)ranksn 9839  ranksnb 9812
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9840
[Monk1] p. 112Theorem 15.17(iii)rankun 9841  rankunb 9835
[Monk1] p. 113Theorem 15.18r1val3 9823
[Monk1] p. 113Definition 15.19df-r1 9749  r1val2 9822
[Monk1] p. 117Lemmazorn2 10511  zorn2g 10508
[Monk1] p. 133Theorem 18.11cardom 9994
[Monk1] p. 133Theorem 18.12canth3 10572
[Monk1] p. 133Theorem 18.14carduni 9989
[Monk2] p. 105Axiom C4ax-4 1842
[Monk2] p. 105Axiom C7ax-7 2041
[Monk2] p. 105Axiom C8ax-12 2215  ax-c15 39764  ax12v2 2217
[Monk2] p. 108Lemma 5ax-c4 39759
[Monk2] p. 109Lemma 12ax-11 2194
[Monk2] p. 109Lemma 15equvini 2486  equvinv 2062  eqvinop 5467
[Monk2] p. 113Axiom C5-1ax-5 1943  ax5ALT 39782
[Monk2] p. 113Axiom C5-2ax-10 2178
[Monk2] p. 113Axiom C5-3ax-11 2194
[Monk2] p. 114Lemma 21sp 2221
[Monk2] p. 114Lemma 22axc4 2353  hba1-o 39772  hba1 2328
[Monk2] p. 114Lemma 23nfia1 2190
[Monk2] p. 114Lemma 24nfa2 2212  nfra2 3363  nfra2w 3300
[Moore] p. 53Part Idf-mre 17674
[Munkres] p. 77Example 2distop 23224  indistop 23231  indistopon 23230
[Munkres] p. 77Example 3fctop 23233  fctop2 23234
[Munkres] p. 77Example 4cctop 23235
[Munkres] p. 78Definition of basisdf-bases 23175  isbasis3g 23178
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17532  tgval2 23185
[Munkres] p. 79Remarktgcl 23198
[Munkres] p. 80Lemma 2.1tgval3 23192
[Munkres] p. 80Lemma 2.2tgss2 23216  tgss3 23215
[Munkres] p. 81Lemma 2.3basgen 23217  basgen2 23218
[Munkres] p. 83Exercise 3topdifinf 38105  topdifinfeq 38106  topdifinffin 38104  topdifinfindis 38102
[Munkres] p. 89Definition of subspace topologyresttop 23389
[Munkres] p. 93Theorem 6.1(1)0cld 23267  topcld 23264
[Munkres] p. 93Theorem 6.1(2)iincld 23268
[Munkres] p. 93Theorem 6.1(3)uncld 23270
[Munkres] p. 94Definition of closureclsval 23266
[Munkres] p. 94Definition of interiorntrval 23265
[Munkres] p. 95Theorem 6.5(a)clsndisj 23304  elcls 23302
[Munkres] p. 95Theorem 6.5(b)elcls3 23312
[Munkres] p. 97Theorem 6.6clslp 23377  neindisj 23346
[Munkres] p. 97Corollary 6.7cldlp 23379
[Munkres] p. 97Definition of limit pointislp2 23374  lpval 23368
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23544
[Munkres] p. 102Definition of continuous functiondf-cn 23456  iscn 23464  iscn2 23467
[Munkres] p. 107Theorem 7.2(g)cncnp 23509  cncnp2 23510  cncnpi 23507  df-cnp 23457  iscnp 23466  iscnp2 23468
[Munkres] p. 127Theorem 10.1metcn 24773
[Munkres] p. 128Theorem 10.3metcn4 25543
[Nathanson] p. 123Remarkreprgt 35131  reprinfz1 35132  reprlt 35129
[Nathanson] p. 123Definitiondf-repr 35119
[Nathanson] p. 123Chapter 5.1circlemethnat 35151
[Nathanson] p. 123Propositionbreprexp 35143  breprexpnat 35144  itgexpif 35116
[NielsenChuang] p. 195Equation 4.73unierri 32586
[OeSilva] p. 2042Section 2ax-bgbltosilva 48728
[Pfenning] p. 17Definition XMnatded 30884
[Pfenning] p. 17Definition NNCnatded 30884  notnotrd 134
[Pfenning] p. 17Definition ` `Cnatded 30884
[Pfenning] p. 18Rule"natded 30884
[Pfenning] p. 18Definition /\Inatded 30884
[Pfenning] p. 18Definition ` `Enatded 30884  natded 30884  natded 30884  natded 30884  natded 30884
[Pfenning] p. 18Definition ` `Inatded 30884  natded 30884  natded 30884  natded 30884  natded 30884
[Pfenning] p. 18Definition ` `ELnatded 30884
[Pfenning] p. 18Definition ` `ERnatded 30884
[Pfenning] p. 18Definition ` `Ea,unatded 30884
[Pfenning] p. 18Definition ` `IRnatded 30884
[Pfenning] p. 18Definition ` `Ianatded 30884
[Pfenning] p. 127Definition =Enatded 30884
[Pfenning] p. 127Definition =Inatded 30884
[Ponnusamy] p. 361Theorem 6.44cphip0l 25434  df-dip 31183  dip0l 31200  ip0l 21853
[Ponnusamy] p. 361Equation 6.45cphipval 25475  ipval 31185
[Ponnusamy] p. 362Equation I1dipcj 31196  ipcj 21851
[Ponnusamy] p. 362Equation I3cphdir 25437  dipdir 31324  ipdir 21856  ipdiri 31312
[Ponnusamy] p. 362Equation I4ipidsq 31192  nmsq 25426
[Ponnusamy] p. 362Equation 6.46ip0i 31307
[Ponnusamy] p. 362Equation 6.47ip1i 31309
[Ponnusamy] p. 362Equation 6.48ip2i 31310
[Ponnusamy] p. 363Equation I2cphass 25443  dipass 31327  ipass 21862  ipassi 31323
[Prugovecki] p. 186Definition of brabraval 32426  df-bra 32332
[Prugovecki] p. 376Equation 8.1df-kb 32333  kbval 32436
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32864
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40763
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32878  atcvat4i 32879  cvrat3 40317  cvrat4 40318  lsatcvat3 39927
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32764  cvrval 40144  df-cv 32761  df-lcv 39894  lspsncv0 21337
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40775
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40776
[Quine] p. 16Definition 2.1df-clab 2741  rabid 3435  rabidd 45989  wl-df.clab 38263
[Quine] p. 17Definition 2.1''dfsb7 2314
[Quine] p. 18Definition 2.7df-cleq 2754  wl-df.cleq 38264
[Quine] p. 19Definition 2.9conventions 30881  df-v 3455
[Quine] p. 34Theorem 5.1eqabb 2901
[Quine] p. 35Theorem 5.2abid1 2898  abid2f 2954
[Quine] p. 40Theorem 6.1sb5 2311
[Quine] p. 40Theorem 6.2sb6 2122  sbalex 2280
[Quine] p. 41Theorem 6.3df-clel 2837  wl-df.clel 38267
[Quine] p. 41Theorem 6.4eqid 2762  eqid1 30948
[Quine] p. 41Theorem 6.5eqcom 2769
[Quine] p. 42Theorem 6.6df-sbc 3743
[Quine] p. 42Theorem 6.7dfsbcq 3744  dfsbcq2 3745
[Quine] p. 43Theorem 6.8vex 3457
[Quine] p. 43Theorem 6.9isset 3467
[Quine] p. 44Theorem 7.3spcgf 3548  spcgv 3553  spcimgf 3516
[Quine] p. 44Theorem 6.11spsbc 3755  spsbcd 3756
[Quine] p. 44Theorem 6.12elex 3474
[Quine] p. 44Theorem 6.13elab 3636  elabg 3633  elabgf 3631
[Quine] p. 44Theorem 6.14noel 4287
[Quine] p. 48Theorem 7.2snprc 4681
[Quine] p. 48Definition 7.1df-pr 4590  df-sn 4588
[Quine] p. 49Theorem 7.4snss 4748  snssg 4747
[Quine] p. 49Theorem 7.5prss 4784  prssg 4783
[Quine] p. 49Theorem 7.6prid1 4726  prid1g 4724  prid2 4727  prid2g 4725  snid 4626  snidg 4624
[Quine] p. 51Theorem 7.12snex 5408
[Quine] p. 51Theorem 7.13prex 5407
[Quine] p. 53Theorem 8.2unisn 4889  unisnALT 45750  unisng 4888
[Quine] p. 53Theorem 8.3uniun 4893
[Quine] p. 54Theorem 8.6elssuni 4902
[Quine] p. 54Theorem 8.7uni0 4899
[Quine] p. 56Theorem 8.17uniabio 6507
[Quine] p. 56Definition 8.18dfaiota2 47976  dfiota2 6494
[Quine] p. 57Theorem 8.19aiotaval 47985  iotaval 6511
[Quine] p. 57Theorem 8.22iotanul 6517
[Quine] p. 58Theorem 8.23iotaex 6513
[Quine] p. 58Definition 9.1df-op 4594
[Quine] p. 61Theorem 9.5opabid 5507  opabidw 5506  opelopab 5525  opelopaba 5518  opelopabaf 5527  opelopabf 5528  opelopabg 5521  opelopabga 5515  opelopabgf 5523  oprabid 7448  oprabidw 7447
[Quine] p. 64Definition 9.11df-xp 5665
[Quine] p. 64Definition 9.12df-cnv 5667
[Quine] p. 64Definition 9.15df-id 5554
[Quine] p. 65Theorem 10.3fun0 6602
[Quine] p. 65Theorem 10.4funi 6569
[Quine] p. 65Theorem 10.5funsn 6590  funsng 6588
[Quine] p. 65Definition 10.1df-fun 6539
[Quine] p. 65Definition 10.2args 6092  dffv4 6879
[Quine] p. 68Definition 10.11conventions 30881  df-fv 6545  fv2 6877
[Quine] p. 124Theorem 17.3nn0opth2 14338  nn0opth2i 14337  nn0opthi 14336  omopthi 8652
[Quine] p. 177Definition 25.2df-rdg 8402
[Quine] p. 232Equation icarddom 10565
[Quine] p. 284Axiom 39(vi)funimaex 6624  funimaexg 6623
[Quine] p. 331Axiom system NFru 3741
[ReedSimon] p. 36Definition (iii)ax-his3 31566
[ReedSimon] p. 63Exercise 4(a)df-dip 31183  polid 31641  polid2i 31639  polidi 31640
[ReedSimon] p. 63Exercise 4(b)df-ph 31295
[ReedSimon] p. 195Remarklnophm 32501  lnophmi 32500
[Retherford] p. 49Exercise 1(i)leopadd 32614
[Retherford] p. 49Exercise 1(ii)leopmul 32616  leopmuli 32615
[Retherford] p. 49Exercise 1(iv)leoptr 32619
[Retherford] p. 49Definition VI.1df-leop 32334  leoppos 32608
[Retherford] p. 49Exercise 1(iii)leoptri 32618
[Retherford] p. 49Definition of operator orderingleop3 32607
[Ribenboim] p. 181Remarknprmdvdsfacm1 48529
[Ribenboim], p. 181Statementppivalnn 48537
[Roman] p. 4Definitiondf-dmat 22716  df-dmatalt 49330
[Roman] p. 18Part Preliminariesdf-rng 20292
[Roman] p. 19Part Preliminariesdf-ring 20378
[Roman] p. 46Theorem 1.6isldepslvec2 49417
[Roman] p. 112Noteisldepslvec2 49417  ldepsnlinc 49440  zlmodzxznm 49429
[Roman] p. 112Examplezlmodzxzequa 49428  zlmodzxzequap 49431  zlmodzxzldep 49436
[Roman] p. 170Theorem 7.8cayleyhamilton 23119
[Rosenlicht] p. 80Theoremheicant 38406
[Rosser] p. 281Definitiondf-op 4594
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 35155
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 35156
[Rotman] p. 28Remarkpgrpgt2nabl 49298  pmtr3ncom 19606
[Rotman] p. 31Theorem 3.4symggen2 19602
[Rotman] p. 42Theorem 3.15cayley 19545  cayleyth 19546
[Rudin] p. 164Equation 27efcan 16186
[Rudin] p. 164Equation 30efzval 16194
[Rudin] p. 167Equation 48absefi 16288
[Russell1905] p. 482Example of "the fatherdfalseu2 50767
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1804
[Sanford] p. 39Rule 4mptxor 1802
[Sanford] p. 40Rule 1mptnan 1801
[Schechter] p. 51Definition of antisymmetryintasym 6113
[Schechter] p. 51Definition of irreflexivityintirr 6116
[Schechter] p. 51Definition of symmetrycnvsym 6112
[Schechter] p. 51Definition of transitivitycotr 6110
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17674
[Schechter] p. 79Definition of Moore closuredf-mrc 17675
[Schechter] p. 82Section 4.5df-mrc 17675
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17677
[Schechter] p. 139Definition AC3dfac9 10142
[Schechter] p. 141Definition (MC)dfac11 43905
[Schechter] p. 149Axiom DC1ax-dc 10451  axdc3 10459
[Schechter] p. 187Definition of "ring with unit"isring 20380  isrngo 38649
[Schechter] p. 276Remark 11.6.espan0 32024
[Schechter] p. 276Definition of spandf-span 31791  spanval 31815
[Schechter] p. 428Definition 15.35bastop1 23222
[Schloeder] p. 1Lemma 1.3onelon 6386  onelond 36781  onelord 44094  ordelon 6385  ordelord 6383
[Schloeder] p. 1Lemma 1.7onepsuc 44095  sucidg 6445
[Schloeder] p. 1Remark 1.50elon 6417  onsuc 7812  ord0 6416  ordsuci 7810
[Schloeder] p. 1Theorem 1.9epsoon 44096
[Schloeder] p. 1Definition 1.1dftr5 5220
[Schloeder] p. 1Definition 1.2dford3 43871  elon2 6372
[Schloeder] p. 1Definition 1.4df-suc 6367
[Schloeder] p. 1Definition 1.6epel 5562  epelg 5560
[Schloeder] p. 1Theorem 1.9(i)elirr 9575  epirron 44097  ordirr 6379
[Schloeder] p. 1Theorem 1.9(ii)oneltr 44099  oneptr 44098  ontr1 6409
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6405  oneptri 44100  ordtri3or 6394
[Schloeder] p. 2Lemma 1.10ondif1 8491  ord0eln0 6418
[Schloeder] p. 2Lemma 1.13elsuci 6431  onsucss 44109  trsucss 6452
[Schloeder] p. 2Lemma 1.14ordsucss 7817
[Schloeder] p. 2Lemma 1.15onnbtwn 6458  ordnbtwn 6457
[Schloeder] p. 2Lemma 1.16orddif0suc 44111  ordnexbtwnsuc 44110
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10406  onsucf1lem 44112  onsucf1o 44115  onsucf1olem 44113  onsucrn 44114
[Schloeder] p. 2Lemma 1.18dflim7 44116
[Schloeder] p. 2Remark 1.12ordzsl 7844
[Schloeder] p. 2Theorem 1.10ondif1i 44105  ordne0gt0 44104
[Schloeder] p. 2Definition 1.11dflim6 44107  limnsuc 44108  onsucelab 44106
[Schloeder] p. 3Remark 1.21omex 9625
[Schloeder] p. 3Theorem 1.19tfinds 7859
[Schloeder] p. 3Theorem 1.22omelon 9628  ordom 7875
[Schloeder] p. 3Definition 1.20dfom3 9629
[Schloeder] p. 4Lemma 2.21onn 8631
[Schloeder] p. 4Lemma 2.7ssonuni 7782  ssorduni 7781
[Schloeder] p. 4Remark 2.4oa1suc 8521
[Schloeder] p. 4Theorem 1.23dfom5 9632  limom 7881
[Schloeder] p. 4Definition 2.1df-1o 8458  df1o2 8465
[Schloeder] p. 4Definition 2.3oa0 8506  oa0suclim 44118  oalim 8522  oasuc 8514
[Schloeder] p. 4Definition 2.5om0 8507  om0suclim 44119  omlim 8523  omsuc 8516
[Schloeder] p. 4Definition 2.6oe0 8512  oe0m1 8511  oe0suclim 44120  oelim 8524  oesuc 8517
[Schloeder] p. 5Lemma 2.10onsupuni 44072
[Schloeder] p. 5Lemma 2.11onsupsucismax 44122
[Schloeder] p. 5Lemma 2.12onsssupeqcond 44123
[Schloeder] p. 5Lemma 2.13limexissup 44124  limexissupab 44126  limiun 44125  limuni 6424
[Schloeder] p. 5Lemma 2.14oa0r 8528
[Schloeder] p. 5Lemma 2.15om1 8532  om1om1r 44127  om1r 8533
[Schloeder] p. 5Remark 2.8oacl 8525  oaomoecl 44121  oecl 8527  omcl 8526
[Schloeder] p. 5Definition 2.9onsupintrab 44074
[Schloeder] p. 6Lemma 2.16oe1 8534
[Schloeder] p. 6Lemma 2.17oe1m 8535
[Schloeder] p. 6Lemma 2.18oe0rif 44128
[Schloeder] p. 6Theorem 2.19oasubex 44129
[Schloeder] p. 6Theorem 2.20nnacl 8602  nnamecl 44130  nnecl 8604  nnmcl 8603
[Schloeder] p. 7Lemma 3.1onsucwordi 44131
[Schloeder] p. 7Lemma 3.2oaword1 8542
[Schloeder] p. 7Lemma 3.3oaword2 8543
[Schloeder] p. 7Lemma 3.4oalimcl 8550
[Schloeder] p. 7Lemma 3.5oaltublim 44133
[Schloeder] p. 8Lemma 3.6oaordi3 44134
[Schloeder] p. 8Lemma 3.81oaomeqom 44136
[Schloeder] p. 8Lemma 3.10oa00 8549
[Schloeder] p. 8Lemma 3.11omge1 44140  omword1 8563
[Schloeder] p. 8Remark 3.9oaordnr 44139  oaordnrex 44138
[Schloeder] p. 8Theorem 3.7oaord3 44135
[Schloeder] p. 9Lemma 3.12omge2 44141  omword2 8564
[Schloeder] p. 9Lemma 3.13omlim2 44142
[Schloeder] p. 9Lemma 3.14omord2lim 44143
[Schloeder] p. 9Lemma 3.15omord2i 44144  omordi 8556
[Schloeder] p. 9Theorem 3.16omord 8558  omord2com 44145
[Schloeder] p. 10Lemma 3.172omomeqom 44146  df-2o 8459
[Schloeder] p. 10Lemma 3.19oege1 44149  oewordi 8582
[Schloeder] p. 10Lemma 3.20oege2 44150  oeworde 8584
[Schloeder] p. 10Lemma 3.21rp-oelim2 44151
[Schloeder] p. 10Lemma 3.22oeord2lim 44152
[Schloeder] p. 10Remark 3.18omnord1 44148  omnord1ex 44147
[Schloeder] p. 11Lemma 3.23oeord2i 44153
[Schloeder] p. 11Lemma 3.25nnoeomeqom 44155
[Schloeder] p. 11Remark 3.26oenord1 44159  oenord1ex 44158
[Schloeder] p. 11Theorem 4.1oaomoencom 44160
[Schloeder] p. 11Theorem 4.2oaass 8551
[Schloeder] p. 11Theorem 3.24oeord2com 44154
[Schloeder] p. 12Theorem 4.3odi 8569
[Schloeder] p. 13Theorem 4.4omass 8570
[Schloeder] p. 14Remark 4.6oenass 44162
[Schloeder] p. 14Theorem 4.7oeoa 8588
[Schloeder] p. 15Lemma 5.1cantnftermord 44163
[Schloeder] p. 15Lemma 5.2cantnfub 44164  cantnfub2 44165
[Schloeder] p. 16Theorem 5.3cantnf2 44168
[Schwabhauser] p. 10Axiom A1axcgrrflx 29372  axtgcgrrflx 28804
[Schwabhauser] p. 10Axiom A2axcgrtr 29373
[Schwabhauser] p. 10Axiom A3axcgrid 29374  axtgcgrid 28805
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28790
[Schwabhauser] p. 11Axiom A4axsegcon 29385  axtgsegcon 28806  df-trkgcb 28792
[Schwabhauser] p. 11Axiom A5ax5seg 29396  axtg5seg 28807  df-trkgcb 28792
[Schwabhauser] p. 11Axiom A6axbtwnid 29397  axtgbtwnid 28808  df-trkgb 28791
[Schwabhauser] p. 12Axiom A7axpasch 29399  axtgpasch 28809  df-trkgb 28791
[Schwabhauser] p. 12Axiom A8axlowdim2 29418  df-trkg2d 35175
[Schwabhauser] p. 13Axiom A8axtglowdim2 28812
[Schwabhauser] p. 13Axiom A9axtgupdim2 28813  df-trkg2d 35175
[Schwabhauser] p. 13Axiom A10axeuclid 29421  axtgeucl 28814  df-trkge 28793
[Schwabhauser] p. 13Axiom A11axcont 29434  axtgcont 28811  axtgcont1 28810  df-trkgb 28791
[Schwabhauser] p. 24Theorem A10prlngmo 29312
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36569
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36571
[Schwabhauser] p. 27Theorem 2.3cgrtr 36574
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36578
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36579  tgcgrcomimp 28819  tgcgrcoml 28821  tgcgrcomr 28820
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36584  tgcgrtriv 28826
[Schwabhauser] p. 28Theorem 2.105segofs 36588  tg5segofs 35186
[Schwabhauser] p. 28Definition 2.10df-afs 35183  df-ofs 36565
[Schwabhauser] p. 29Theorem 2.11cgrextend 36590  tgcgrextend 28827
[Schwabhauser] p. 29Theorem 2.12segconeq 36592  tgsegconeq 28828
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36604  btwntriv2 36594  tgbtwntriv2 28830
[Schwabhauser] p. 30Theorem 3.2btwncomim 36595  tgbtwncom 28831
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36598  tgbtwntriv1 28834
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36599  tgbtwnswapid 28835
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36605  btwnintr 36601  tgbtwnexch2 28839  tgbtwnintr 28836
[Schwabhauser] p. 30Theorem 3.6btwnexch 36607  btwnexch3 36602  tgbtwnexch 28841  tgbtwnexch3 28837
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36606  tgbtwnouttr 28840  tgbtwnouttr2 28838
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29417
[Schwabhauser] p. 32Theorem 3.14btwndiff 36609  tgbtwndiff 28849
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28842  trisegint 36610
[Schwabhauser] p. 34Theorem 4.2ifscgr 36626  tgifscgr 28851
[Schwabhauser] p. 34Theorem 4.11colcom 28901  colrot1 28902  colrot2 28903  lncom 28970  lnrot1 28971  lnrot2 28972
[Schwabhauser] p. 34Definition 4.1df-ifs 36622
[Schwabhauser] p. 35Theorem 4.3cgrsub 36627  tgcgrsub 28852
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36637  tgcgrxfr 28861
[Schwabhauser] p. 35Statement 4.4ercgrg 28860
[Schwabhauser] p. 35Definition 4.4df-cgr3 36623  df-cgrg 28854
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28854
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36638  tgbtwnxfr 28873
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36644  colinearperm2 36646  colinearperm3 36645  colinearperm4 36647  colinearperm5 36648
[Schwabhauser] p. 36Definition 4.8df-ismt 28876
[Schwabhauser] p. 36Definition 4.10df-colinear 36621  tgellng 28896  tglng 28889
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36649
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36657  lnxfr 28909
[Schwabhauser] p. 37Theorem 4.14lineext 36658  lnext 28910
[Schwabhauser] p. 37Theorem 4.16fscgr 36662  tgfscgr 28911
[Schwabhauser] p. 37Theorem 4.17linecgr 36663  lncgr 28912
[Schwabhauser] p. 37Definition 4.15df-fs 36624
[Schwabhauser] p. 38Theorem 4.18lineid 36665  lnid 28913
[Schwabhauser] p. 38Theorem 4.19idinside 36666  tgidinside 28914
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36683  tgbtwnconn1 28918
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36684  tgbtwnconn2 28919
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36685  tgbtwnconn3 28920
[Schwabhauser] p. 41Theorem 5.5brsegle2 36691
[Schwabhauser] p. 41Definition 5.4df-segle 36689  legov 28928
[Schwabhauser] p. 41Definition 5.5legov2 28929
[Schwabhauser] p. 42Remark 5.13legso 28942
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36692
[Schwabhauser] p. 42Theorem 5.7seglerflx 36694
[Schwabhauser] p. 42Theorem 5.8segletr 36696
[Schwabhauser] p. 42Theorem 5.9segleantisym 36697
[Schwabhauser] p. 42Theorem 5.10seglelin 36698
[Schwabhauser] p. 42Theorem 5.11seglemin 36695
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36700
[Schwabhauser] p. 42Proposition 5.7legid 28930
[Schwabhauser] p. 42Proposition 5.8legtrd 28932
[Schwabhauser] p. 42Proposition 5.9legtri3 28933
[Schwabhauser] p. 42Proposition 5.10legtrid 28934
[Schwabhauser] p. 42Proposition 5.11leg0 28935
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36707
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36708
[Schwabhauser] p. 43Theorem 6.4broutsideof 36703  df-outsideof 36702
[Schwabhauser] p. 43Definition 6.1broutsideof2 36704  ishlg 28948
[Schwabhauser] p. 44Theorem 6.4hlln 28953
[Schwabhauser] p. 44Theorem 6.5hlid 28955  outsideofrflx 36709
[Schwabhauser] p. 44Theorem 6.6hlcomb 28949  hlcomd 28950  outsideofcom 36710
[Schwabhauser] p. 44Theorem 6.7hltr 28956  outsideoftr 36711
[Schwabhauser] p. 44Theorem 6.11hlcgreq 28965  hlcgreu 28964  outsideofeu 36713
[Schwabhauser] p. 44Definition 6.8df-ray 36720
[Schwabhauser] p. 45Part 2df-lines2 36721
[Schwabhauser] p. 45Theorem 6.13outsidele 36714
[Schwabhauser] p. 45Theorem 6.15lineunray 36729
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36730  tglineelsb2 28980
[Schwabhauser] p. 45Theorem 6.17linecom 36732  linerflx1 36731  linerflx2 36733  tglinecom 28983  tglinerflx1 28981  tglinerflx2 28982
[Schwabhauser] p. 45Theorem 6.18linethru 36735  tglinethru 28984
[Schwabhauser] p. 45Definition 6.14df-line2 36719  tglng 28889
[Schwabhauser] p. 45Proposition 6.13legbtwn 28937
[Schwabhauser] p. 46Theorem 6.19linethrueu 36738  tglinethrueu 28987
[Schwabhauser] p. 46Theorem 6.21lineintmo 36739  tglineineq 28991  tglineinsn 28992  tglineinteq 28994  tglineintmo 28990
[Schwabhauser] p. 46Theorem 6.23colline 28998
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28999
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 29000
[Schwabhauser] p. 49Theorem 7.3mirinv 29018
[Schwabhauser] p. 49Theorem 7.7mirmir 29014
[Schwabhauser] p. 49Theorem 7.8mirreu3 29006
[Schwabhauser] p. 49Definition 7.5df-mir 29005  ismir 29011  mirbtwn 29010  mircgr 29009  mirfv 29008  mirval 29007
[Schwabhauser] p. 50Theorem 7.8mirreu 29016
[Schwabhauser] p. 50Theorem 7.9mireq 29017
[Schwabhauser] p. 50Theorem 7.10mirinv 29018
[Schwabhauser] p. 50Theorem 7.11mirf1o 29021
[Schwabhauser] p. 50Theorem 7.13miriso 29022
[Schwabhauser] p. 51Theorem 7.14mirmot 29027
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 29024  mirbtwni 29023
[Schwabhauser] p. 51Theorem 7.16mircgrs 29025
[Schwabhauser] p. 51Theorem 7.17miduniq 29037
[Schwabhauser] p. 52Lemma 7.21symquadlem 29041  symquadmid 29184
[Schwabhauser] p. 52Theorem 7.18miduniq1 29038
[Schwabhauser] p. 52Theorem 7.19miduniq2 29039
[Schwabhauser] p. 52Theorem 7.20colmid 29040
[Schwabhauser] p. 53Lemma 7.22krippen 29043
[Schwabhauser] p. 55Lemma 7.25midexlem 29044
[Schwabhauser] p. 57Theorem 8.2ragcom 29053
[Schwabhauser] p. 57Definition 8.1df-rag 29049  israg 29052
[Schwabhauser] p. 58Theorem 8.3ragcol 29054
[Schwabhauser] p. 58Theorem 8.4ragmir 29055
[Schwabhauser] p. 58Theorem 8.5ragtrivb 29057
[Schwabhauser] p. 58Theorem 8.6ragflat2 29058
[Schwabhauser] p. 58Theorem 8.7ragflat 29059
[Schwabhauser] p. 58Theorem 8.8ragtriva 29060
[Schwabhauser] p. 58Theorem 8.9ragflat3 29061  ragncol 29064
[Schwabhauser] p. 58Theorem 8.10ragcgr 29062
[Schwabhauser] p. 59Theorem 8.12perpcom 29068
[Schwabhauser] p. 59Theorem 8.13ragperp 29072
[Schwabhauser] p. 59Theorem 8.14perpneq 29069
[Schwabhauser] p. 59Definition 8.11df-perpg 29051  isperp 29067
[Schwabhauser] p. 59Definition 8.13isperp2 29070
[Schwabhauser] p. 60Theorem 8.18foot 29077
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 29086  colperpexlem2 29087
[Schwabhauser] p. 63Theorem 8.21colperpex 29089  colperpexlem3 29088
[Schwabhauser] p. 64Theorem 8.22mideu 29094  midex 29093
[Schwabhauser] p. 66Lemma 8.24opphllem 29091
[Schwabhauser] p. 67Theorem 9.2oppcom 29100
[Schwabhauser] p. 67Definition 9.1islnopp 29095
[Schwabhauser] p. 68Lemma 9.3opphllem2 29104
[Schwabhauser] p. 68Lemma 9.4opphllem5 29107  opphllem6 29108
[Schwabhauser] p. 69Theorem 9.5opphl 29110
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28809
[Schwabhauser] p. 70Theorem 9.6outpasch 29113
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 29121
[Schwabhauser] p. 71Definition 9.7df-hpg 29116  hpgbr 29118
[Schwabhauser] p. 72Lemma 9.10hpgerlem 29123
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 29122
[Schwabhauser] p. 72Theorem 9.11hpgid 29124
[Schwabhauser] p. 72Theorem 9.12hpgcom 29125
[Schwabhauser] p. 72Theorem 9.13hpgtr 29126
[Schwabhauser] p. 73Theorem 9.18colopp 29127
[Schwabhauser] p. 73Theorem 9.19colhp 29128
[Schwabhauser] p. 74Lemma 9.22lnincplng 29142
[Schwabhauser] p. 74Theorem 9.21plngcp 29144
[Schwabhauser] p. 74Theorem 9.24plngrot 29148
[Schwabhauser] p. 74Definition 9.20df-plng 29132  elplng 29138
[Schwabhauser] p. 75Theorem 9.25lnssplng 29150  lnssplng1 29151
[Schwabhauser] p. 76Theorem 9.26plng3p 29155
[Schwabhauser] p. 88Theorem 10.2lmieu 29169
[Schwabhauser] p. 88Definition 10.1df-mid 29159
[Schwabhauser] p. 89Theorem 10.4lmicom 29173
[Schwabhauser] p. 89Theorem 10.5lmilmi 29174
[Schwabhauser] p. 89Theorem 10.6lmireu 29175
[Schwabhauser] p. 89Theorem 10.7lmieq 29176
[Schwabhauser] p. 89Theorem 10.8lmiinv 29177
[Schwabhauser] p. 89Theorem 10.9lmif1o 29180
[Schwabhauser] p. 89Theorem 10.10lmiiso 29182
[Schwabhauser] p. 89Definition 10.3df-lmi 29160
[Schwabhauser] p. 90Theorem 10.11lmimot 29183
[Schwabhauser] p. 91Theorem 10.12hypcgr 29187
[Schwabhauser] p. 92Theorem 10.14lmiopp 29188
[Schwabhauser] p. 92Theorem 10.15lnperpex 29189  lnperpexs 29190
[Schwabhauser] p. 92Theorem 10.16trgcopy 29191  trgcopyeu 29193
[Schwabhauser] p. 95Definition 11.2dfcgra2 29218
[Schwabhauser] p. 95Definition 11.3iscgra 29196
[Schwabhauser] p. 95Proposition 11.4cgracgr 29205
[Schwabhauser] p. 95Proposition 11.10cgrahl1 29203  cgrahl2 29204
[Schwabhauser] p. 96Theorem 11.6cgraid 29206
[Schwabhauser] p. 96Theorem 11.9cgraswap 29207
[Schwabhauser] p. 97Theorem 11.7cgracom 29209
[Schwabhauser] p. 97Theorem 11.8cgratr 29210
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 29214  cgrahl 29215
[Schwabhauser] p. 98Theorem 11.13sacgr 29219
[Schwabhauser] p. 98Theorem 11.14oacgr 29220
[Schwabhauser] p. 98Theorem 11.15acopy 29221  acopyeu 29222
[Schwabhauser] p. 98Theorem 11.16ragcgra 29223
[Schwabhauser] p. 98Theorem 11.17cgrarag 29224
[Schwabhauser] p. 98Theorem 11.18ragsupplcgra 29225
[Schwabhauser] p. 99Theorem 11.19ragraghl 29226
[Schwabhauser] p. 99Theorem 11.20perpeq 29228
[Schwabhauser] p. 99Theorem 11.22tgaaddcpbl 29232
[Schwabhauser] p. 101Theorem 11.24inagswap 29240
[Schwabhauser] p. 101Theorem 11.25inaghl 29244
[Schwabhauser] p. 101Definition 11.23isinag 29237
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 29252
[Schwabhauser] p. 102Definition 11.27df-leag 29245  isleag 29246
[Schwabhauser] p. 107Theorem 11.49tgsas 29280  tgsas1 29279  tgsas2 29281  tgsas3 29282
[Schwabhauser] p. 108Theorem 11.50tgasa 29284  tgasa1 29283
[Schwabhauser] p. 109Theorem 11.51tgsss1 29285  tgsss2 29286  tgsss3 29287
[Schwabhauser] p. 121Definition 12.2df-prlng 29295
[Schwabhauser] p. 122Theorem 12.4prlngref 29298
[Schwabhauser] p. 122Theorem 12.5prlngsym 29299
[Schwabhauser] p. 122Theorem 12.6prlnghpg 29304
[Schwabhauser] p. 122Theorem 12.7dfprlng2 29305  dfprlng3 29306
[Schwabhauser] p. 122Theorem 12.9perpprlng 29308
[Schwabhauser] p. 122Theorem 12.10prlngex 29309
[Schwabhauser] p. 123Theorem 12.11prlngmo 29312  prlngmo2 29314
[Schwabhauser] p. 124Theorem 12.13prlngeu 29313
[Schwabhauser] p. 124Theorem 12.14prlngpln4 29316
[Schwabhauser] p. 124Theorem 12.15prlngplngtr 29317
[Schwabhauser] p. 125Theorem 12.16prlnginn0 29318
[Schwabhauser] p. 125Theorem 12.17prlngmid2 29319
[Schwabhauser] p. 126Theorem 12.18symquadprlng 29320
[Schwabhauser] p. 126Theorem 12.19prlngsymquad 29322  prlngsymquadopp 29323
[Schwabhauser] p. 126Theorem 12.20quadcgrprlng 29324
[Schwabhauser] p. 126Theorem 12.21tgaltai 29325
[Shapiro] p. 230Theorem 6.5.1dchrhash 27508  dchrsum 27506  dchrsum2 27505  sumdchr 27509
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27510  sum2dchr 27511
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20199  ablfacrp2 20200
[Shapiro], p. 328Equation 9.2.4vmasum 27453
[Shapiro], p. 329Equation 9.2.7logfac2 27454
[Shapiro], p. 329Equation 9.2.9logfacrlim 27461
[Shapiro], p. 331Equation 9.2.13vmadivsum 27719
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27722
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27776  vmalogdivsum2 27775
[Shapiro], p. 375Theorem 9.4.1dirith 27766  dirith2 27765
[Shapiro], p. 375Equation 9.4.3rplogsum 27764  rpvmasum 27763  rpvmasum2 27749
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27724
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27762
[Shapiro], p. 377Lemma 9.4.1dchrisum 27729  dchrisumlem1 27726  dchrisumlem2 27727  dchrisumlem3 27728  dchrisumlema 27725
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27732
[Shapiro], p. 379Equation 9.4.16dchrmusum 27761  dchrmusumlem 27759  dchrvmasumlem 27760
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27731
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27733
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27757  dchrisum0re 27750  dchrisumn0 27758
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27743
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27747
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27748
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27803  pntrsumbnd2 27804  pntrsumo1 27802
[Shapiro], p. 405Equation 10.2.1mudivsum 27767
[Shapiro], p. 406Equation 10.2.6mulogsum 27769
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27771
[Shapiro], p. 407Equation 10.2.8mulog2sum 27774
[Shapiro], p. 418Equation 10.4.6logsqvma 27779
[Shapiro], p. 418Equation 10.4.8logsqvma2 27780
[Shapiro], p. 419Equation 10.4.10selberg 27785
[Shapiro], p. 420Equation 10.4.12selberg2lem 27787
[Shapiro], p. 420Equation 10.4.14selberg2 27788
[Shapiro], p. 422Equation 10.6.7selberg3 27796
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27797
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27794  selberg3lem2 27795
[Shapiro], p. 422Equation 10.4.23selberg4 27798
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27792
[Shapiro], p. 428Equation 10.6.2selbergr 27805
[Shapiro], p. 429Equation 10.6.8selberg3r 27806
[Shapiro], p. 430Equation 10.6.11selberg4r 27807
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27821
[Shapiro], p. 434Equation 10.6.27pntlema 27833  pntlemb 27834  pntlemc 27832  pntlemd 27831  pntlemg 27835
[Shapiro], p. 435Equation 10.6.29pntlema 27833
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27825
[Shapiro], p. 436Lemma 10.6.2pntibnd 27830
[Shapiro], p. 436Equation 10.6.34pntlema 27833
[Shapiro], p. 436Equation 10.6.35pntlem3 27846  pntleml 27848
[Stewart] p. 91Lemma 7.3constrss 34255
[Stewart] p. 92Definition 7.4.df-constr 34242
[Stewart] p. 96Theorem 7.10constraddcl 34274  constrinvcl 34285  constrmulcl 34283  constrnegcl 34275  constrsqrtcl 34291
[Stewart] p. 97Theorem 7.11constrextdg2 34261
[Stewart] p. 98Theorem 7.12constrext2chn 34271
[Stewart] p. 99Theorem 7.132sqr3nconstr 34293
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34303
[Stoll] p. 13Definition corresponds to dfsymdif3 4255
[Stoll] p. 16Exercise 4.40dif 4359  dif0 4330
[Stoll] p. 16Exercise 4.8difdifdir 4450
[Stoll] p. 17Theorem 5.1(5)unvdif 4432
[Stoll] p. 19Theorem 5.2(13)undm 4246
[Stoll] p. 19Theorem 5.2(13')indm 4247
[Stoll] p. 20Remarkinvdif 4228
[Stoll] p. 25Definition of ordered tripledf-ot 4596
[Stoll] p. 43Definitionuniiun 5021
[Stoll] p. 44Definitionintiin 5022
[Stoll] p. 45Definitiondf-iin 4957
[Stoll] p. 45Definition indexed uniondf-iun 4956
[Stoll] p. 176Theorem 3.4(27)iman 407
[Stoll] p. 262Example 4.1dfsymdif3 4255
[Strang] p. 242Section 6.3expgrowth 45161
[Suppes] p. 22Theorem 2eq0 4300  eq0f 4297
[Suppes] p. 22Theorem 4eqss 3949  eqssd 3951  eqssi 3950
[Suppes] p. 23Theorem 5ss0 4355  ss0b 4354
[Suppes] p. 23Theorem 6sstr 3942  sstrALT2 45659
[Suppes] p. 23Theorem 7pssirr 4054
[Suppes] p. 23Theorem 8pssn2lp 4056
[Suppes] p. 23Theorem 9psstr 4059
[Suppes] p. 23Theorem 10pssss 4049
[Suppes] p. 25Theorem 12elin 3918  elun 4103
[Suppes] p. 26Theorem 15inidm 4175
[Suppes] p. 26Theorem 16in0 4348
[Suppes] p. 27Theorem 23unidm 4107
[Suppes] p. 27Theorem 24un0 4347
[Suppes] p. 27Theorem 25ssun1 4127
[Suppes] p. 27Theorem 26ssequn1 4135
[Suppes] p. 27Theorem 27unss 4139
[Suppes] p. 27Theorem 28indir 4235
[Suppes] p. 27Theorem 29undir 4236
[Suppes] p. 28Theorem 32difid 4328
[Suppes] p. 29Theorem 33difin 4221
[Suppes] p. 29Theorem 34indif 4229
[Suppes] p. 29Theorem 35undif1 4433
[Suppes] p. 29Theorem 36difun2 4440
[Suppes] p. 29Theorem 37difin0 4431
[Suppes] p. 29Theorem 38disjdif 4429
[Suppes] p. 29Theorem 39difundi 4239
[Suppes] p. 29Theorem 40difindi 4241
[Suppes] p. 30Theorem 41nalset 5275
[Suppes] p. 39Theorem 61uniss 4878
[Suppes] p. 39Theorem 65uniop 5496
[Suppes] p. 41Theorem 70intsn 4947
[Suppes] p. 42Theorem 71intpr 4945  intprg 4944
[Suppes] p. 42Theorem 73op1stb 5451
[Suppes] p. 42Theorem 78intun 4943
[Suppes] p. 44Definition 15(a)dfiun2 4994  dfiun2g 4992
[Suppes] p. 44Definition 15(b)dfiin2 4995
[Suppes] p. 47Theorem 86elpw 4564  elpw2 5303  elpw2g 5302  elpwg 4563  elpwgdedVD 45741
[Suppes] p. 47Theorem 87pwid 4583
[Suppes] p. 47Theorem 89pw0 4776
[Suppes] p. 48Theorem 90pwpw0 4777
[Suppes] p. 52Theorem 101xpss12 5674
[Suppes] p. 52Theorem 102xpindi 5817  xpindir 5818
[Suppes] p. 52Theorem 103xpundi 5728  xpundir 5729
[Suppes] p. 54Theorem 105elirrv 9572
[Suppes] p. 58Theorem 2relss 5766
[Suppes] p. 59Theorem 4eldm 5888  eldm2 5889  eldm2g 5887  eldmg 5886
[Suppes] p. 59Definition 3df-dm 5669
[Suppes] p. 60Theorem 6dmin 5899
[Suppes] p. 60Theorem 8rnun 6140
[Suppes] p. 60Theorem 9rnin 6141
[Suppes] p. 60Definition 4dfrn2 5876
[Suppes] p. 61Theorem 11brcnv 5866  brcnvg 5863
[Suppes] p. 62Equation 5elcnv 5860  elcnv2 5861
[Suppes] p. 62Theorem 12relcnv 6104
[Suppes] p. 62Theorem 15cnvin 6139
[Suppes] p. 62Theorem 16cnvun 6137
[Suppes] p. 63Definitiondftrrels2 39409
[Suppes] p. 63Theorem 20co02 6261
[Suppes] p. 63Theorem 21dmcoss 5963
[Suppes] p. 63Definition 7df-co 5668
[Suppes] p. 64Theorem 26cnvco 5873
[Suppes] p. 64Theorem 27coass 6266
[Suppes] p. 65Theorem 31resundi 5990
[Suppes] p. 65Theorem 34elima 6065  elima2 6066  elima3 6067  elimag 6064
[Suppes] p. 65Theorem 35imaundi 6145
[Suppes] p. 66Theorem 40dminss 6148
[Suppes] p. 66Theorem 41imainss 6149
[Suppes] p. 67Exercise 11cnvxp 6152
[Suppes] p. 81Definition 34dfec2 8702
[Suppes] p. 82Theorem 72elec 8746  elecALTV 39021  elecg 8744
[Suppes] p. 82Theorem 73eqvrelth 39445  erth 8754  erth2 8755
[Suppes] p. 83Theorem 74eqvreldisj 39448  erdisj 8757
[Suppes] p. 83Definition 35, df-parts 39618  dfmembpart2 39623
[Suppes] p. 89Theorem 96map0b 8893
[Suppes] p. 89Theorem 97map0 8897  map0g 8894
[Suppes] p. 89Theorem 98mapsn 8898  mapsnd 8896
[Suppes] p. 89Theorem 99mapss 8899
[Suppes] p. 91Definition 12(ii)alephsuc 10074
[Suppes] p. 91Definition 12(iii)alephlim 10073
[Suppes] p. 92Theorem 1enref 8994  enrefg 8993
[Suppes] p. 92Theorem 2ensym 9012  ensymb 9011  ensymi 9013
[Suppes] p. 92Theorem 3entr 9015
[Suppes] p. 92Theorem 4unen 9055
[Suppes] p. 94Theorem 15endom 8988
[Suppes] p. 94Theorem 16ssdomg 9009
[Suppes] p. 94Theorem 17domtr 9016
[Suppes] p. 95Theorem 18sbth 9098
[Suppes] p. 97Theorem 23canth2 9131  canth2g 9132
[Suppes] p. 97Definition 3brsdom2 9102  df-sdom 8958  dfsdom2 9101
[Suppes] p. 97Theorem 21(i)sdomirr 9115
[Suppes] p. 97Theorem 22(i)domnsym 9104
[Suppes] p. 97Theorem 21(ii)sdomnsym 9103
[Suppes] p. 97Theorem 22(ii)domsdomtr 9113
[Suppes] p. 97Theorem 22(iv)brdom2 8991
[Suppes] p. 97Theorem 21(iii)sdomtr 9116
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9111
[Suppes] p. 98Exercise 4fundmen 9041  fundmeng 9042
[Suppes] p. 98Exercise 6xpdom3 9076
[Suppes] p. 98Exercise 11sdomentr 9112
[Suppes] p. 104Theorem 37fofi 9286
[Suppes] p. 104Theorem 38pwfi 9291
[Suppes] p. 105Theorem 40pwfi 9291
[Suppes] p. 111Axiom for cardinal numberscarden 10562
[Suppes] p. 130Definition 3df-tr 5217
[Suppes] p. 132Theorem 9ssonuni 7782
[Suppes] p. 134Definition 6df-suc 6367
[Suppes] p. 136Theorem Schema 22findes 7900  finds 7896  finds1 7899  finds2 7898
[Suppes] p. 151Theorem 42isfinite 9634  isfinite2 9271  isfiniteg 9273  unbnn 9269
[Suppes] p. 162Definition 5df-ltnq 10930  df-ltpq 10922
[Suppes] p. 197Theorem Schema 4tfindes 7862  tfinds 7859  tfinds2 7863
[Suppes] p. 209Theorem 18oaord1 8541
[Suppes] p. 209Theorem 21oaword2 8543
[Suppes] p. 211Theorem 25oaass 8551
[Suppes] p. 225Definition 8iscard2 9984
[Suppes] p. 227Theorem 56ondomon 10574
[Suppes] p. 228Theorem 59harcard 9986
[Suppes] p. 228Definition 12(i)aleph0 10072
[Suppes] p. 228Theorem Schema 61onintss 6414
[Suppes] p. 228Theorem Schema 62onminesb 7795  onminsb 7796
[Suppes] p. 229Theorem 64alephval2 10584
[Suppes] p. 229Theorem 65alephcard 10076
[Suppes] p. 229Theorem 66alephord2i 10083
[Suppes] p. 229Theorem 67alephnbtwn 10077
[Suppes] p. 229Definition 12df-aleph 9948
[Suppes] p. 242Theorem 6weth 10500
[Suppes] p. 242Theorem 8entric 10568
[Suppes] p. 242Theorem 9carden 10562
[Szendrei] p. 11Line 6df-cloneop 36277
[Szendrei] p. 11Paragraph 3df-suppos 36281
[TakeutiZaring] p. 8Axiom 1ax-ext 2734
[TakeutiZaring] p. 13Definition 4.5df-cleq 2754  wl-df.cleq 38264
[TakeutiZaring] p. 13Proposition 4.6df-clel 2837  wl-df.clel 38267
[TakeutiZaring] p. 13Proposition 4.9cvjust 2756
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2782
[TakeutiZaring] p. 14Definition 4.16df-oprab 7420
[TakeutiZaring] p. 14Proposition 4.14ru 3741
[TakeutiZaring] p. 15Axiom 2zfpair 5390
[TakeutiZaring] p. 15Exercise 1elpr 4612  elpr2 4614  elpr2g 4613  elprg 4610
[TakeutiZaring] p. 15Exercise 2elsn 4602  elsn2 4629  elsn2g 4628  elsng 4601  velsn 4603
[TakeutiZaring] p. 15Exercise 3elop 5447
[TakeutiZaring] p. 15Exercise 4sneq 4597  sneqr 4803
[TakeutiZaring] p. 15Definition 5.1dfpr2 4608  dfsn2 4600  dfsn2ALT 4609
[TakeutiZaring] p. 16Axiom 3uniex 7746
[TakeutiZaring] p. 16Exercise 6opth 5456
[TakeutiZaring] p. 16Exercise 7opex 5443
[TakeutiZaring] p. 16Exercise 8rext 5427
[TakeutiZaring] p. 16Corollary 5.8unex 7749  unexg 7748
[TakeutiZaring] p. 16Definition 5.3dftp2 4655
[TakeutiZaring] p. 16Definition 5.5df-uni 4871
[TakeutiZaring] p. 16Definition 5.6df-in 3909  df-un 3907
[TakeutiZaring] p. 16Proposition 5.7unipr 4887  uniprg 4886
[TakeutiZaring] p. 17Axiom 4vpwex 5346
[TakeutiZaring] p. 17Exercise 1eltp 4653
[TakeutiZaring] p. 17Exercise 5elsuc 6434  elsucg 6432  sstr2 3941
[TakeutiZaring] p. 17Exercise 6uncom 4108
[TakeutiZaring] p. 17Exercise 7incom 4158
[TakeutiZaring] p. 17Exercise 8unass 4121
[TakeutiZaring] p. 17Exercise 9inass 4176
[TakeutiZaring] p. 17Exercise 10indi 4233
[TakeutiZaring] p. 17Exercise 11undi 4234
[TakeutiZaring] p. 17Definition 5.9df-pss 3922  df-ss 3919
[TakeutiZaring] p. 17Definition 5.10df-pw 4562
[TakeutiZaring] p. 18Exercise 7unss2 4136
[TakeutiZaring] p. 18Exercise 9dfss2 3920  sseqin2 4172
[TakeutiZaring] p. 18Exercise 10ssid 3956
[TakeutiZaring] p. 18Exercise 12inss1 4185  inss2 4186
[TakeutiZaring] p. 18Exercise 13nss 3998
[TakeutiZaring] p. 18Exercise 15unieq 4881
[TakeutiZaring] p. 18Exercise 18sspwb 5428  sspwimp 45742  sspwimpALT 45749  sspwimpALT2 45752  sspwimpcf 45744
[TakeutiZaring] p. 18Exercise 19pweqb 5435
[TakeutiZaring] p. 19Axiom 5ax-rep 5236
[TakeutiZaring] p. 20Definitiondf-rab 3415
[TakeutiZaring] p. 20Corollary 5.160ex 5268
[TakeutiZaring] p. 20Definition 5.12df-dif 3905
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 37273  dfnul2 4285
[TakeutiZaring] p. 20Proposition 5.15difid 4328
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4303  n0f 4299  neq0 4302  neq0f 4298
[TakeutiZaring] p. 21Axiom 6zfreg 9571
[TakeutiZaring] p. 21Axiom 6'zfregs 9714
[TakeutiZaring] p. 21Theorem 5.22setind 9729
[TakeutiZaring] p. 21Definition 5.20df-v 3455
[TakeutiZaring] p. 21Proposition 5.21vprc 5281
[TakeutiZaring] p. 22Exercise 10ss 4353
[TakeutiZaring] p. 22Exercise 3ssex 5289  ssexg 5288
[TakeutiZaring] p. 22Exercise 4inex1 5284
[TakeutiZaring] p. 22Exercise 5ruv 9583
[TakeutiZaring] p. 22Exercise 6elirr 9575
[TakeutiZaring] p. 22Exercise 7ssdif0 4317
[TakeutiZaring] p. 22Exercise 11difdif 4085
[TakeutiZaring] p. 22Exercise 13undif3 4249  undif3VD 45706
[TakeutiZaring] p. 22Exercise 14difss 4086
[TakeutiZaring] p. 22Exercise 15sscon 4093
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3079
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3089
[TakeutiZaring] p. 23Proposition 6.2xpex 7755  xpexg 7752
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5666
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6608
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6786  fun11 6611
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6550  svrelfun 6609
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5875
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5877
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5671
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5672
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5668
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6191  dfrel2 6186
[TakeutiZaring] p. 25Exercise 3xpss 5675
[TakeutiZaring] p. 25Exercise 5relun 5796
[TakeutiZaring] p. 25Exercise 6reluni 5803
[TakeutiZaring] p. 25Exercise 9inxp 5816
[TakeutiZaring] p. 25Exercise 12relres 6002
[TakeutiZaring] p. 25Exercise 13opelres 5982  opelresi 5984
[TakeutiZaring] p. 25Exercise 14dmres 6009
[TakeutiZaring] p. 25Exercise 15resss 5998
[TakeutiZaring] p. 25Exercise 17resabs1 6003
[TakeutiZaring] p. 25Exercise 18funres 6579
[TakeutiZaring] p. 25Exercise 24relco 6108
[TakeutiZaring] p. 25Exercise 29funco 6577
[TakeutiZaring] p. 25Exercise 30f1co 6788
[TakeutiZaring] p. 26Definition 6.10eu2 2636
[TakeutiZaring] p. 26Definition 6.11conventions 30881  df-fv 6545  fv3 6900
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7925  cnvexg 7924
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7909  dmexg 7901
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7910  rnexg 7902
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 45278
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7920
[TakeutiZaring] p. 27Corollary 6.13fvex 6895
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 48064  tz6.12-1-afv2 48131  tz6.12-1 6905  tz6.12-afv 48063  tz6.12-afv2 48130  tz6.12 6906  tz6.12c-afv2 48132  tz6.12c 6904
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 48127  tz6.12-2 6869  tz6.12i-afv2 48133  tz6.12i 6908
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6540
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6541
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6543  wfo 6535
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6542  wf1 6534
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6544  wf1o 6536
[TakeutiZaring] p. 28Exercise 4eqfnfv 7026  eqfnfv2 7027  eqfnfv2f 7030
[TakeutiZaring] p. 28Exercise 5fvco 6980
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7219
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7217
[TakeutiZaring] p. 29Exercise 9funimaex 6624  funimaexg 6623
[TakeutiZaring] p. 29Definition 6.18df-br 5108
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5568
[TakeutiZaring] p. 30Definition 6.21dffr2 5620  dffr3 6099  eliniseg 6094  iniseg 6097
[TakeutiZaring] p. 30Definition 6.22df-eprel 5559
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5636  fr3nr 7774  frirr 5635
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5612
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7776
[TakeutiZaring] p. 31Exercise 1frss 5623
[TakeutiZaring] p. 31Exercise 4wess 5645
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6349  tz6.26i 6350  wefrc 5653  wereu2 5656
[TakeutiZaring] p. 32Theorem 6.27wfi 6351  wfii 6352
[TakeutiZaring] p. 32Definition 6.28df-isom 6546
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7333
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7334
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7340
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7341
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7342
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7346
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7353
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7355
[TakeutiZaring] p. 35Notationwtr 5216
[TakeutiZaring] p. 35Theorem 7.2trelpss 45279  tz7.2 5642
[TakeutiZaring] p. 35Definition 7.1dftr3 5221
[TakeutiZaring] p. 36Proposition 7.4ordwe 6374
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6382
[TakeutiZaring] p. 36Proposition 7.6ordelord 6383  ordelordALT 45362  ordelordALTVD 45691
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6389  ordelssne 6388
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6387
[TakeutiZaring] p. 37Proposition 7.9ordin 6392
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7784
[TakeutiZaring] p. 38Corollary 7.15ordsson 7785
[TakeutiZaring] p. 38Definition 7.11df-on 6365
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6394
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45374  ordon 7779
[TakeutiZaring] p. 38Proposition 7.13onprc 7780
[TakeutiZaring] p. 39Theorem 7.17tfi 7852
[TakeutiZaring] p. 40Exercise 3ontr2 6410  ontr2d 36782
[TakeutiZaring] p. 40Exercise 7dftr2 5218
[TakeutiZaring] p. 40Exercise 9onssmin 7794
[TakeutiZaring] p. 40Exercise 11unon 7830
[TakeutiZaring] p. 40Exercise 12ordun 6468
[TakeutiZaring] p. 40Exercise 14ordequn 6467
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7781
[TakeutiZaring] p. 40Proposition 7.20elssuni 4902
[TakeutiZaring] p. 41Definition 7.22df-suc 6367
[TakeutiZaring] p. 41Proposition 7.23sssucid 6444  sucidg 6445
[TakeutiZaring] p. 41Proposition 7.24onsuc 7812
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6458  ordnbtwn 6457
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7827
[TakeutiZaring] p. 42Exercise 1df-lim 6366
[TakeutiZaring] p. 42Exercise 4omssnlim 7880
[TakeutiZaring] p. 42Exercise 7ssnlim 7885
[TakeutiZaring] p. 42Exercise 8onsucssi 7840  ordelsuc 7819
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7821
[TakeutiZaring] p. 42Definition 7.27nlimon 7850
[TakeutiZaring] p. 42Definition 7.28dfom2 7867
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7888
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7889
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7890
[TakeutiZaring] p. 43Remarkomon 7877
[TakeutiZaring] p. 43Axiom 7inf3 9617  omex 9625
[TakeutiZaring] p. 43Theorem 7.32ordom 7875
[TakeutiZaring] p. 43Corollary 7.31find 7895
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7892
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7893
[TakeutiZaring] p. 44Exercise 1limomss 7870
[TakeutiZaring] p. 44Exercise 2int0 4925
[TakeutiZaring] p. 44Exercise 3trintss 5235
[TakeutiZaring] p. 44Exercise 4intss1 4926
[TakeutiZaring] p. 44Exercise 5intex 5312
[TakeutiZaring] p. 44Exercise 6oninton 7797
[TakeutiZaring] p. 44Exercise 11ordintdif 6413
[TakeutiZaring] p. 44Definition 7.35df-int 4911
[TakeutiZaring] p. 44Proposition 7.34noinfep 9642
[TakeutiZaring] p. 45Exercise 4onint 7792
[TakeutiZaring] p. 47Lemma 1tfrlem1 8367
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8389
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8390
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8391
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8398  tz7.44-2 8399  tz7.44-3 8400
[TakeutiZaring] p. 50Exercise 1smogt 8359
[TakeutiZaring] p. 50Exercise 3smoiso 8354
[TakeutiZaring] p. 50Definition 7.46df-smo 8338
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8437  tz7.49c 8438
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8435
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8434
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8436
[TakeutiZaring] p. 53Proposition 7.532eu5 2682
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10017
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10018
[TakeutiZaring] p. 56Definition 8.1oalim 8522  oasuc 8514
[TakeutiZaring] p. 57Remarktfindsg 7860
[TakeutiZaring] p. 57Proposition 8.2oacl 8525
[TakeutiZaring] p. 57Proposition 8.3oa0 8506  oa0r 8528
[TakeutiZaring] p. 57Proposition 8.16omcl 8526
[TakeutiZaring] p. 58Corollary 8.5oacan 8538
[TakeutiZaring] p. 58Proposition 8.4nnaord 8610  nnaordi 8609  oaord 8537  oaordi 8536
[TakeutiZaring] p. 59Proposition 8.6iunss2 5012  uniss2 4905
[TakeutiZaring] p. 59Proposition 8.7oawordri 8540
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8545  oawordex 8547
[TakeutiZaring] p. 59Proposition 8.9nnacl 8602
[TakeutiZaring] p. 59Proposition 8.10oaabs 8639
[TakeutiZaring] p. 60Remarkoancom 9633
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8550
[TakeutiZaring] p. 62Exercise 1nnarcl 8607
[TakeutiZaring] p. 62Exercise 5oaword1 8542
[TakeutiZaring] p. 62Definition 8.15om0x 8509  omlim 8523  omsuc 8516
[TakeutiZaring] p. 62Definition 8.15(a)om0 8507
[TakeutiZaring] p. 63Proposition 8.17nnecl 8604  nnmcl 8603
[TakeutiZaring] p. 63Proposition 8.19nnmord 8623  nnmordi 8622  omord 8558  omordi 8556
[TakeutiZaring] p. 63Proposition 8.20omcan 8559
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8627  omwordri 8562
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8529
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8532  om1r 8533
[TakeutiZaring] p. 64Proposition 8.22om00 8565
[TakeutiZaring] p. 64Proposition 8.23omordlim 8567
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8568
[TakeutiZaring] p. 64Proposition 8.25odi 8569
[TakeutiZaring] p. 65Theorem 8.26omass 8570
[TakeutiZaring] p. 67Definition 8.30nnesuc 8599  oe0 8512  oelim 8524  oesuc 8517  onesuc 8520
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8510
[TakeutiZaring] p. 67Proposition 8.32oen0 8577
[TakeutiZaring] p. 67Proposition 8.33oeordi 8578
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8511
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8535
[TakeutiZaring] p. 68Corollary 8.34oeord 8579
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8585
[TakeutiZaring] p. 68Proposition 8.35oewordri 8583
[TakeutiZaring] p. 68Proposition 8.37oeworde 8584
[TakeutiZaring] p. 69Proposition 8.41oeoa 8588
[TakeutiZaring] p. 70Proposition 8.42oeoe 8590
[TakeutiZaring] p. 73Theorem 9.1trcl 9710  tz9.1 9711
[TakeutiZaring] p. 76Definition 9.9df-r1 9749  r10 9753  r1lim 9757  r1limg 9756  r1suc 9755  r1sucg 9754
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9765  r1ord2 9766  r1ordg 9763
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9775
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9800  tz9.13 9776  tz9.13g 9777
[TakeutiZaring] p. 79Definition 9.14df-rank 9750  rankval 9801  rankvalb 9782  rankvalg 9802
[TakeutiZaring] p. 79Proposition 9.16rankel 9824  rankelb 9809
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9838  rankval3 9825  rankval3b 9811
[TakeutiZaring] p. 79Proposition 9.18rankonid 9814
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9780
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9819  rankr1c 9806  rankr1g 9817
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9820
[TakeutiZaring] p. 80Exercise 1rankss 9834  rankssb 9833
[TakeutiZaring] p. 80Exercise 2unbndrank 9827
[TakeutiZaring] p. 80Proposition 9.19bndrank 9826
[TakeutiZaring] p. 83Axiom of Choiceac4 10480  dfac3 10127
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10036  numth 10477  numth2 10476
[TakeutiZaring] p. 85Definition 10.4cardval 10557
[TakeutiZaring] p. 85Proposition 10.5cardid 10558  cardid2 9961
[TakeutiZaring] p. 85Proposition 10.9oncard 9968
[TakeutiZaring] p. 85Proposition 10.10carden 10562
[TakeutiZaring] p. 85Proposition 10.11cardidm 9967
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9952
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9973
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9965
[TakeutiZaring] p. 87Proposition 10.15pwen 9151
[TakeutiZaring] p. 88Exercise 1en0 9027
[TakeutiZaring] p. 88Exercise 7infensuc 9156
[TakeutiZaring] p. 89Exercise 10omxpen 9080
[TakeutiZaring] p. 90Corollary 10.23cardnn 9971
[TakeutiZaring] p. 90Definition 10.27alephiso 10104
[TakeutiZaring] p. 90Proposition 10.20nneneq 9203
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9211
[TakeutiZaring] p. 90Proposition 10.26alephprc 10105
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9208
[TakeutiZaring] p. 91Exercise 2alephle 10094
[TakeutiZaring] p. 91Exercise 3aleph0 10072
[TakeutiZaring] p. 91Exercise 4cardlim 9980
[TakeutiZaring] p. 91Exercise 7infpss 10221
[TakeutiZaring] p. 91Exercise 8infcntss 9295
[TakeutiZaring] p. 91Definition 10.29df-fin 8959  isfi 8984
[TakeutiZaring] p. 92Proposition 10.32onfin 9212
[TakeutiZaring] p. 92Proposition 10.34imadomg 10540
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9073
[TakeutiZaring] p. 93Proposition 10.35fodomb 10532
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10191  unxpdom 9232
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9982  cardsdomelir 9981
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9234
[TakeutiZaring] p. 94Proposition 10.39infxpen 10020
[TakeutiZaring] p. 95Definition 10.42df-map 8831
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10573  infxpidm2 10023
[TakeutiZaring] p. 95Proposition 10.41infdju 10212  infxp 10219
[TakeutiZaring] p. 96Proposition 10.44pw2en 9085  pw2f1o 9083
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9144
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10492
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10487  ac6s5 10496
[TakeutiZaring] p. 98Theorem 10.47unidom 10554
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10555  uniimadomf 10556
[TakeutiZaring] p. 100Definition 11.1cfcof 10279
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10274
[TakeutiZaring] p. 102Exercise 1cfle 10258
[TakeutiZaring] p. 102Exercise 2cf0 10255
[TakeutiZaring] p. 102Exercise 3cfsuc 10262
[TakeutiZaring] p. 102Exercise 4cfom 10269
[TakeutiZaring] p. 102Proposition 11.9coftr 10278
[TakeutiZaring] p. 103Theorem 11.15alephreg 10594
[TakeutiZaring] p. 103Proposition 11.11cardcf 10256
[TakeutiZaring] p. 103Proposition 11.13alephsing 10281
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10103
[TakeutiZaring] p. 104Proposition 11.16carduniima 10102
[TakeutiZaring] p. 104Proposition 11.18alephfp 10114  alephfp2 10115
[TakeutiZaring] p. 106Theorem 11.20gchina 10711
[TakeutiZaring] p. 106Theorem 11.21mappwen 10118
[TakeutiZaring] p. 107Theorem 11.26konigth 10581
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10595
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10596
[Tarski] p. 67Axiom B5ax-c5 39758
[Tarski] p. 67Scheme B5sp 2221
[Tarski] p. 68Lemma 6avril1 30944  equid 2045
[Tarski] p. 69Lemma 7equcomi 2050
[Tarski] p. 70Lemma 14spim 2418  spime 2420  spimew 2004
[Tarski] p. 70Lemma 16ax-12 2215  ax-c15 39764  ax12i 1999
[Tarski] p. 70Lemmas 16 and 17sb6 2122
[Tarski] p. 75Axiom B7ax6v 2001
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1943  ax5ALT 39782
[Tarski], p. 75Scheme B8 of system S2ax-7 2041  ax-8 2147  ax-9 2155
[Tarski1999] p. 178Axiom 4axtgsegcon 28806
[Tarski1999] p. 178Axiom 5axtg5seg 28807
[Tarski1999] p. 179Axiom 7axtgpasch 28809
[Tarski1999] p. 180Axiom 7.1axtgpasch 28809
[Tarski1999] p. 185Axiom 11axtgcont1 28810
[Truss] p. 114Theorem 5.18ruc 16335
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38410
[Viaclovsky8] p. 3Proposition 7ismblfin 38412
[Weierstrass] p. 272Definitiondf-mdet 22811  mdetuni 22848
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 917
[WhiteheadRussell] p. 96Axiom *1.3olc 882
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 883
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 933
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 983
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 190
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 136
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 91  wl-luk-pm2.04 38201
[WhiteheadRussell] p. 100Theorem *2.05frege5 44642  imim2 59  wl-luk-imim2 38196
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47909  imim1 84
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 910
[WhiteheadRussell] p. 101Theorem *2.06barbara 2689  syl 18
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 916
[WhiteheadRussell] p. 101Theorem *2.08id 23  wl-luk-id 38199
[WhiteheadRussell] p. 101Theorem *2.11exmid 908
[WhiteheadRussell] p. 101Theorem *2.12notnot 143
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 911
[WhiteheadRussell] p. 102Theorem *2.14notnotr 131  notnotrALT2 45751  wl-luk-notnotr 38200
[WhiteheadRussell] p. 102Theorem *2.15con1 147
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44672  axfrege28 44671  con3 154
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 129
[WhiteheadRussell] p. 104Theorem *2.2orc 881
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 938
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 124  wl-luk-pm2.21 38193
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 125
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 903
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 954
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30882  pm2.27 43  wl-luk-pm2.27 38191
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 936
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 39121
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 937
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 985
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 986
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 984
[WhiteheadRussell] p. 105Definition *2.33df-3or 1104
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 920
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 921
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 957
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 57
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 895
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 896
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 170  pm2.5g 169
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 193
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 897
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 898
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 899
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 173
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 174
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 865
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 866
[WhiteheadRussell] p. 107Theorem *2.55orel1 902
[WhiteheadRussell] p. 107Theorem *2.56orel2 904
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 194
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 913
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 955
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 956
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 195
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 905  pm2.67 906
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 177  pm2.521g 175  pm2.521g2 176
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 912
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 988
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 914
[WhiteheadRussell] p. 108Theorem *2.69looinv 206
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 989
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 990
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 947
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 945
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 987
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 991
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 85
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 946
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 110
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1007
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 475  pm3.2im 161
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1008
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1009
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1010
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1011
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 477
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 465
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 408
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 815
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 454
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 455
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 488  simplim 168
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 490  simprim 167
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 777
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 778
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 820
[WhiteheadRussell] p. 113Fact)pm3.45 634
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 822
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 498
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 499
[WhiteheadRussell] p. 113Theorem *3.44jao 975  pm3.44 974
[WhiteheadRussell] p. 113Theorem *3.47anim12 821
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 479
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 978
[WhiteheadRussell] p. 116Theorem *4.1con34b 319
[WhiteheadRussell] p. 117Theorem *4.2biid 264
[WhiteheadRussell] p. 117Theorem *4.11notbi 322
[WhiteheadRussell] p. 117Theorem *4.12con2bi 356
[WhiteheadRussell] p. 117Theorem *4.13notnotb 318
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 819
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 846
[WhiteheadRussell] p. 117Theorem *4.21bicom 225
[WhiteheadRussell] p. 117Theorem *4.22biantr 818  bitr 817
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 574
[WhiteheadRussell] p. 117Theorem *4.25oridm 918  pm4.25 919
[WhiteheadRussell] p. 118Theorem *4.3ancom 466
[WhiteheadRussell] p. 118Theorem *4.4andi 1025
[WhiteheadRussell] p. 118Theorem *4.31orcom 884
[WhiteheadRussell] p. 118Theorem *4.32anass 474
[WhiteheadRussell] p. 118Theorem *4.33orass 935
[WhiteheadRussell] p. 118Theorem *4.36anbi1 645
[WhiteheadRussell] p. 118Theorem *4.37orbi1 931
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 649
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 992
[WhiteheadRussell] p. 118Definition *4.34df-3an 1105
[WhiteheadRussell] p. 119Theorem *4.41ordi 1023
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1069
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1040
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1012
[WhiteheadRussell] p. 119Theorem *4.45orabs 1014  pm4.45 1013  pm4.45im 841
[WhiteheadRussell] p. 120Theorem *4.5anor 998
[WhiteheadRussell] p. 120Theorem *4.6imor 867
[WhiteheadRussell] p. 120Theorem *4.7anclb 555
[WhiteheadRussell] p. 120Theorem *4.51ianor 997
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 1000
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 1001
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 1002
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 1003
[WhiteheadRussell] p. 120Theorem *4.56ioran 999  pm4.56 1004
[WhiteheadRussell] p. 120Theorem *4.57oran 1005  pm4.57 1006
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 410
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 870
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 403
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 863
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 411
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 864
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 404
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 567  pm4.71d 571  pm4.71i 569  pm4.71r 568  pm4.71rd 572  pm4.71ri 570
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 964
[WhiteheadRussell] p. 121Theorem *4.73iba 537
[WhiteheadRussell] p. 121Theorem *4.74biorf 950
[WhiteheadRussell] p. 121Theorem *4.76jcab 527  pm4.76 528
[WhiteheadRussell] p. 121Theorem *4.77jaob 976  pm4.77 977
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 948
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1021
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 398
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 399
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1041
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1042
[WhiteheadRussell] p. 122Theorem *4.84imbi1 350
[WhiteheadRussell] p. 122Theorem *4.85imbi2 351
[WhiteheadRussell] p. 122Theorem *4.86bibi1 354
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 392  impexp 456  pm4.87 857
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 836
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 959  pm5.11g 958
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 960
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 962
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 961
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1030
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1031
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1029
[WhiteheadRussell] p. 124Theorem *5.18nbbn 386  pm5.18 384
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 391
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 837
[WhiteheadRussell] p. 124Theorem *5.22xor 1032
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1065
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1066
[WhiteheadRussell] p. 124Theorem *5.25dfor2 915
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 583
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 393
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 364
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1017
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 968
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 844
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 584
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 849
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 838
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 847
[WhiteheadRussell] p. 125Theorem *5.41imdi 394  pm5.41 395
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 553
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 552
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1022
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1035
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 963
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1016
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1036
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1037
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1045
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 369
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 273
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1046
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 37324
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 45184
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 45185
[WhiteheadRussell] p. 147Theorem *10.2219.26 1903
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 45186
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 45187
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 45188
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1926
[WhiteheadRussell] p. 151Theorem *10.301albitr 45189
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 45190
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 45191
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 45192
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 45193
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 45195
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 45196
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 45197
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 45194
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2127
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 45200
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 45201
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2107
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2197
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1862
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1863
[WhiteheadRussell] p. 161Theorem *11.319.21vv 45202
[WhiteheadRussell] p. 162Theorem *11.322alim 45203
[WhiteheadRussell] p. 162Theorem *11.332albi 45204
[WhiteheadRussell] p. 162Theorem *11.342exim 45205
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 45207
[WhiteheadRussell] p. 162Theorem *11.3412exbi 45206
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1920
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 45209
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 45210
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 45208
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1861
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 45211
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 45212
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1879
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 45213
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2377
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1893
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 45218
[WhiteheadRussell] p. 165Theorem *11.56aaanv 45214
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 45215
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 45216
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 45217
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 45222
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 45219
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 45220
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 45221
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 45223
[WhiteheadRussell] p. 175Definition *14.02df-eu 2596
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 45233  pm13.13b 45234
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 45235
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3038
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3039
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3623
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 45241
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 45242
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 45236
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45377  pm13.193 45237
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 45238
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 45239
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 45240
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 45247
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 45246
[WhiteheadRussell] p. 184Definition *14.01iotasbc 45245
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3804
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 45248  pm14.122b 45249  pm14.122c 45250
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 45251  pm14.123b 45252  pm14.123c 45253
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 45255
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 45254
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 45256
[WhiteheadRussell] p. 190Theorem *14.22iota4 6518
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 45257
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6519
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 45258
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 45260
[WhiteheadRussell] p. 192Theorem *14.26eupick 2660  eupickbi 2663  sbaniota 45261
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 45259
[WhiteheadRussell] p. 192Theorem *14.271eubi 2611
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 45262
[WhiteheadRussell] p. 235Definition *30.01conventions 30881  df-fv 6545
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 10009  pm54.43lem 10008
[Young] p. 141Definition of operator orderingleop2 32606
[Young] p. 142Example 12.2(i)0leop 32612  idleop 32613
[vandenDries] p. 42Lemma 61irrapx1 43671
[vandenDries] p. 43Theorem 62pellex 43678  pellexlem1 43672

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