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 16536
[Adamek] p. 21Condition 3.1(b)df-cat 16536
[Adamek] p. 22Example 3.3(1)df-setc 16933
[Adamek] p. 24Example 3.3(4.c)0cat 16556
[Adamek] p. 25Definition 3.5df-oppc 16579
[Adamek] p. 28Remark 3.9oppciso 16648
[Adamek] p. 28Remark 3.12invf1o 16636  invisoinvl 16657
[Adamek] p. 28Example 3.13idinv 16656  idiso 16655
[Adamek] p. 28Corollary 3.11inveq 16641
[Adamek] p. 28Definition 3.8df-inv 16615  df-iso 16616  dfiso2 16639
[Adamek] p. 28Proposition 3.10sectcan 16622
[Adamek] p. 29Remark 3.16cicer 16673
[Adamek] p. 29Definition 3.15cic 16666  df-cic 16663
[Adamek] p. 29Definition 3.17df-func 16725
[Adamek] p. 29Proposition 3.14(1)invinv 16637
[Adamek] p. 29Proposition 3.14(2)invco 16638  isoco 16644
[Adamek] p. 30Remark 3.19df-func 16725
[Adamek] p. 30Example 3.20(1)idfucl 16748
[Adamek] p. 32Proposition 3.21funciso 16741
[Adamek] p. 33Proposition 3.23cofucl 16755
[Adamek] p. 34Remark 3.28(2)catciso 16964
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 17015
[Adamek] p. 34Definition 3.27(2)df-fth 16772
[Adamek] p. 34Definition 3.27(3)df-full 16771
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 17015
[Adamek] p. 35Corollary 3.32ffthiso 16796
[Adamek] p. 35Proposition 3.30(c)cofth 16802
[Adamek] p. 35Proposition 3.30(d)cofull 16801
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 17000
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 17000
[Adamek] p. 39Definition 3.41funcoppc 16742
[Adamek] p. 39Definition 3.44.df-catc 16952
[Adamek] p. 39Proposition 3.43(c)fthoppc 16790
[Adamek] p. 39Proposition 3.43(d)fulloppc 16789
[Adamek] p. 40Remark 3.48catccat 16961
[Adamek] p. 40Definition 3.47df-catc 16952
[Adamek] p. 48Example 4.3(1.a)0subcat 16705
[Adamek] p. 48Example 4.3(1.b)catsubcat 16706
[Adamek] p. 48Definition 4.1(2)fullsubc 16717
[Adamek] p. 48Definition 4.1(a)df-subc 16679
[Adamek] p. 49Remark 4.4(2)ressffth 16805
[Adamek] p. 83Definition 6.1df-nat 16810
[Adamek] p. 87Remark 6.14(a)fuccocl 16831
[Adamek] p. 87Remark 6.14(b)fucass 16835
[Adamek] p. 87Definition 6.15df-fuc 16811
[Adamek] p. 88Remark 6.16fuccat 16837
[Adamek] p. 101Definition 7.1df-inito 16848
[Adamek] p. 101Example 7.2 (6)irinitoringc 42592
[Adamek] p. 102Definition 7.4df-termo 16849
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 16869
[Adamek] p. 102Proposition 7.3 (2)initoeu2 16873
[Adamek] p. 103Definition 7.7df-zeroo 16850
[Adamek] p. 103Example 7.9 (3)nzerooringczr 42595
[Adamek] p. 103Proposition 7.6termoeu1w 16876
[Adamek] p. 106Definition 7.19df-sect 16614
[Adamek] p. 478Item Rngdf-ringc 42528
[AhoHopUll] p. 2Section 1.1df-bigo 42865
[AhoHopUll] p. 12Section 1.3df-blen 42887
[AhoHopUll] p. 318Section 9.1df-concat 13497  df-pfx 41905  df-substr 13499  df-word 13495  lencl 13520  wrd0 13526
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 22732  df-nmoo 27940
[AkhiezerGlazman] p. 64Theoremhmopidmch 29352  hmopidmchi 29350
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 29400  pjcmul2i 29401
[AkhiezerGlazman] p. 72Theoremcnvunop 29117  unoplin 29119
[AkhiezerGlazman] p. 72Equation 2unopadj 29118  unopadj2 29137
[AkhiezerGlazman] p. 73Theoremelunop2 29212  lnopunii 29211
[AkhiezerGlazman] p. 80Proposition 1adjlnop 29285
[Apostol] p. 18Theorem I.1addcan 10426  addcan2d 10446  addcan2i 10436  addcand 10445  addcani 10435
[Apostol] p. 18Theorem I.2negeu 10477
[Apostol] p. 18Theorem I.3negsub 10535  negsubd 10604  negsubi 10565
[Apostol] p. 18Theorem I.4negneg 10537  negnegd 10589  negnegi 10557
[Apostol] p. 18Theorem I.5subdi 10669  subdid 10692  subdii 10685  subdir 10670  subdird 10693  subdiri 10686
[Apostol] p. 18Theorem I.6mul01 10421  mul01d 10441  mul01i 10432  mul02 10420  mul02d 10440  mul02i 10431
[Apostol] p. 18Theorem I.7mulcan 10870  mulcan2d 10867  mulcand 10866  mulcani 10872
[Apostol] p. 18Theorem I.8receu 10878  xreceu 29970
[Apostol] p. 18Theorem I.9divrec 10907  divrecd 11010  divreci 10976  divreczi 10969
[Apostol] p. 18Theorem I.10recrec 10928  recreci 10963
[Apostol] p. 18Theorem I.11mul0or 10873  mul0ord 10883  mul0ori 10881
[Apostol] p. 18Theorem I.12mul2neg 10675  mul2negd 10691  mul2negi 10684  mulneg1 10672  mulneg1d 10689  mulneg1i 10682
[Apostol] p. 18Theorem I.13divadddiv 10946  divadddivd 11051  divadddivi 10993
[Apostol] p. 18Theorem I.14divmuldiv 10931  divmuldivd 11048  divmuldivi 10991  rdivmuldivd 30131
[Apostol] p. 18Theorem I.15divdivdiv 10932  divdivdivd 11054  divdivdivi 10994
[Apostol] p. 20Axiom 7rpaddcl 12057  rpaddcld 12090  rpmulcl 12058  rpmulcld 12091
[Apostol] p. 20Axiom 8rpneg 12066
[Apostol] p. 20Axiom 90nrp 12068
[Apostol] p. 20Theorem I.17lttri 10369
[Apostol] p. 20Theorem I.18ltadd1d 10826  ltadd1dd 10844  ltadd1i 10788
[Apostol] p. 20Theorem I.19ltmul1 11079  ltmul1a 11078  ltmul1i 11148  ltmul1ii 11158  ltmul2 11080  ltmul2d 12117  ltmul2dd 12131  ltmul2i 11151
[Apostol] p. 20Theorem I.20msqgt0 10754  msqgt0d 10801  msqgt0i 10771
[Apostol] p. 20Theorem I.210lt1 10756
[Apostol] p. 20Theorem I.23lt0neg1 10740  lt0neg1d 10803  ltneg 10734  ltnegd 10811  ltnegi 10778
[Apostol] p. 20Theorem I.25lt2add 10719  lt2addd 10856  lt2addi 10796
[Apostol] p. 20Definition of positive numbersdf-rp 12036
[Apostol] p. 21Exercise 4recgt0 11073  recgt0d 11164  recgt0i 11134  recgt0ii 11135
[Apostol] p. 22Definition of integersdf-z 11585
[Apostol] p. 22Definition of positive integersdfnn3 11240
[Apostol] p. 22Definition of rationalsdf-q 11997
[Apostol] p. 24Theorem I.26supeu 8520
[Apostol] p. 26Theorem I.28nnunb 11495
[Apostol] p. 26Theorem I.29arch 11496
[Apostol] p. 28Exercise 2btwnz 11686
[Apostol] p. 28Exercise 3nnrecl 11497
[Apostol] p. 28Exercise 4rebtwnz 11995
[Apostol] p. 28Exercise 5zbtwnre 11994
[Apostol] p. 28Exercise 6qbtwnre 12235
[Apostol] p. 28Exercise 10(a)zeneo 15271  zneo 11667  zneoALTV 42103
[Apostol] p. 29Theorem I.35msqsqrtd 14387  resqrtth 14204  sqrtth 14312  sqrtthi 14318  sqsqrtd 14386
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 11229
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 11961
[Apostol] p. 361Remarkcrreczi 13196
[Apostol] p. 363Remarkabsgt0i 14346
[Apostol] p. 363Exampleabssubd 14400  abssubi 14350
[ApostolNT] p. 7Remarkfmtno0 41975  fmtno1 41976  fmtno2 41985  fmtno3 41986  fmtno4 41987  fmtno5fac 42017  fmtnofz04prm 42012
[ApostolNT] p. 7Definitiondf-fmtno 41963
[ApostolNT] p. 8Definitiondf-ppi 25047
[ApostolNT] p. 14Definitiondf-dvds 15190
[ApostolNT] p. 14Theorem 1.1(a)iddvds 15204
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 15227
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 15223
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 15217
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 15219
[ApostolNT] p. 14Theorem 1.1(f)1dvds 15205
[ApostolNT] p. 14Theorem 1.1(g)dvds0 15206
[ApostolNT] p. 14Theorem 1.1(h)0dvds 15211
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 15242
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 15244
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 15246
[ApostolNT] p. 15Definitiondf-gcd 15425  dfgcd2 15471
[ApostolNT] p. 16Definitionisprm2 15602
[ApostolNT] p. 16Theorem 1.5coprmdvds 15574
[ApostolNT] p. 16Theorem 1.7prminf 15826
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 15443
[ApostolNT] p. 16Theorem 1.4(b)gcdass 15472
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 15474
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 15457
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 15449
[ApostolNT] p. 17Theorem 1.8coprm 15630
[ApostolNT] p. 17Theorem 1.9euclemma 15632
[ApostolNT] p. 17Theorem 1.101arith2 15839
[ApostolNT] p. 18Theorem 1.13prmrec 15833
[ApostolNT] p. 19Theorem 1.14divalg 15334
[ApostolNT] p. 20Theorem 1.15eucalg 15508
[ApostolNT] p. 24Definitiondf-mu 25048
[ApostolNT] p. 25Definitiondf-phi 15678
[ApostolNT] p. 25Theorem 2.1musum 25138
[ApostolNT] p. 26Theorem 2.2phisum 15702
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 15688
[ApostolNT] p. 28Theorem 2.5(c)phimul 15692
[ApostolNT] p. 32Definitiondf-vma 25045
[ApostolNT] p. 32Theorem 2.9muinv 25140
[ApostolNT] p. 32Theorem 2.10vmasum 25162
[ApostolNT] p. 38Remarkdf-sgm 25049
[ApostolNT] p. 38Definitiondf-sgm 25049
[ApostolNT] p. 75Definitiondf-chp 25046  df-cht 25044
[ApostolNT] p. 104Definitioncongr 15585
[ApostolNT] p. 106Remarkdvdsval3 15193
[ApostolNT] p. 106Definitionmoddvds 15200
[ApostolNT] p. 107Example 2mod2eq0even 15278
[ApostolNT] p. 107Example 3mod2eq1n2dvds 15279
[ApostolNT] p. 107Example 4zmod1congr 12895
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 12932
[ApostolNT] p. 107Theorem 5.2(c)modexp 13206
[ApostolNT] p. 108Theorem 5.3modmulconst 15222
[ApostolNT] p. 109Theorem 5.4cncongr1 15588
[ApostolNT] p. 109Theorem 5.6gcdmodi 15985
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 15590
[ApostolNT] p. 113Theorem 5.17eulerth 15695
[ApostolNT] p. 113Theorem 5.18vfermltl 15713
[ApostolNT] p. 114Theorem 5.19fermltl 15696
[ApostolNT] p. 116Theorem 5.24wilthimp 25019
[ApostolNT] p. 179Definitiondf-lgs 25241  lgsprme0 25285
[ApostolNT] p. 180Example 11lgs 25286
[ApostolNT] p. 180Theorem 9.2lgsvalmod 25262
[ApostolNT] p. 180Theorem 9.3lgsdirprm 25277
[ApostolNT] p. 181Theorem 9.4m1lgs 25334
[ApostolNT] p. 181Theorem 9.52lgs 25353  2lgsoddprm 25362
[ApostolNT] p. 182Theorem 9.6gausslemma2d 25320
[ApostolNT] p. 185Theorem 9.8lgsquad 25329
[ApostolNT] p. 188Definitiondf-lgs 25241  lgs1 25287
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 25278
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 25280
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 25288
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 25289
[Baer] p. 40Property (b)mapdord 37446
[Baer] p. 40Property (c)mapd11 37447
[Baer] p. 40Property (e)mapdin 37470  mapdlsm 37472
[Baer] p. 40Property (f)mapd0 37473
[Baer] p. 40Definition of projectivitydf-mapd 37433  mapd1o 37456
[Baer] p. 41Property (g)mapdat 37475
[Baer] p. 44Part (1)mapdpg 37514
[Baer] p. 45Part (2)hdmap1eq 37609  mapdheq 37536  mapdheq2 37537  mapdheq2biN 37538
[Baer] p. 45Part (3)baerlem3 37521
[Baer] p. 46Part (4)mapdheq4 37540  mapdheq4lem 37539
[Baer] p. 46Part (5)baerlem5a 37522  baerlem5abmN 37526  baerlem5amN 37524  baerlem5b 37523  baerlem5bmN 37525
[Baer] p. 47Part (6)hdmap1l6 37629  hdmap1l6a 37617  hdmap1l6e 37622  hdmap1l6f 37623  hdmap1l6g 37624  hdmap1l6lem1 37615  hdmap1l6lem2 37616  mapdh6N 37555  mapdh6aN 37543  mapdh6eN 37548  mapdh6fN 37549  mapdh6gN 37550  mapdh6lem1N 37541  mapdh6lem2N 37542
[Baer] p. 48Part 9hdmapval 37636
[Baer] p. 48Part 10hdmap10 37648
[Baer] p. 48Part 11hdmapadd 37651
[Baer] p. 48Part (6)hdmap1l6h 37625  mapdh6hN 37551
[Baer] p. 48Part (7)mapdh75cN 37561  mapdh75d 37562  mapdh75e 37560  mapdh75fN 37563  mapdh7cN 37557  mapdh7dN 37558  mapdh7eN 37556  mapdh7fN 37559
[Baer] p. 48Part (8)mapdh8 37596  mapdh8a 37583  mapdh8aa 37584  mapdh8ab 37585  mapdh8ac 37586  mapdh8ad 37587  mapdh8b 37588  mapdh8c 37589  mapdh8d 37591  mapdh8d0N 37590  mapdh8e 37592  mapdh8g 37593  mapdh8i 37594  mapdh8j 37595
[Baer] p. 48Part (9)mapdh9a 37597
[Baer] p. 48Equation 10mapdhvmap 37577
[Baer] p. 49Part 12hdmap11 37656  hdmapeq0 37652  hdmapf1oN 37673  hdmapneg 37654  hdmaprnN 37672  hdmaprnlem1N 37657  hdmaprnlem3N 37658  hdmaprnlem3uN 37659  hdmaprnlem4N 37661  hdmaprnlem6N 37662  hdmaprnlem7N 37663  hdmaprnlem8N 37664  hdmaprnlem9N 37665  hdmapsub 37655
[Baer] p. 49Part 14hdmap14lem1 37676  hdmap14lem10 37685  hdmap14lem1a 37674  hdmap14lem2N 37677  hdmap14lem2a 37675  hdmap14lem3 37678  hdmap14lem8 37683  hdmap14lem9 37684
[Baer] p. 50Part 14hdmap14lem11 37686  hdmap14lem12 37687  hdmap14lem13 37688  hdmap14lem14 37689  hdmap14lem15 37690  hgmapval 37695
[Baer] p. 50Part 15hgmapadd 37702  hgmapmul 37703  hgmaprnlem2N 37705  hgmapvs 37699
[Baer] p. 50Part 16hgmaprnN 37709
[Baer] p. 110Lemma 1hdmapip0com 37725
[Baer] p. 110Line 27hdmapinvlem1 37726
[Baer] p. 110Line 28hdmapinvlem2 37727
[Baer] p. 110Line 30hdmapinvlem3 37728
[Baer] p. 110Part 1.2hdmapglem5 37730  hgmapvv 37734
[Baer] p. 110Proposition 1hdmapinvlem4 37729
[Baer] p. 111Line 10hgmapvvlem1 37731
[Baer] p. 111Line 15hdmapg 37738  hdmapglem7 37737
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2622
[BellMachover] p. 460Notationdf-mo 2623
[BellMachover] p. 460Definitionmo3 2656
[BellMachover] p. 461Axiom Extax-ext 2751
[BellMachover] p. 462Theorem 1.1bm1.1 2756
[BellMachover] p. 463Axiom Repaxrep5 4911
[BellMachover] p. 463Scheme Sepaxsep 4915
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 33354  bm1.3ii 4919
[BellMachover] p. 466Problemaxpow2 4977
[BellMachover] p. 466Axiom Powaxpow3 4978
[BellMachover] p. 466Axiom Unionaxun2 7102
[BellMachover] p. 468Definitiondf-ord 5868
[BellMachover] p. 469Theorem 2.2(i)ordirr 5883
[BellMachover] p. 469Theorem 2.2(iii)onelon 5890
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 5885
[BellMachover] p. 471Definition of Ndf-om 7217
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 7157
[BellMachover] p. 471Definition of Limdf-lim 5870
[BellMachover] p. 472Axiom Infzfinf2 8707
[BellMachover] p. 473Theorem 2.8limom 7231
[BellMachover] p. 477Equation 3.1df-r1 8795
[BellMachover] p. 478Definitionrankval2 8849
[BellMachover] p. 478Theorem 3.3(i)r1ord3 8813  r1ord3g 8810
[BellMachover] p. 480Axiom Regzfreg 8660
[BellMachover] p. 488Axiom ACac5 9505  dfac4 9149
[BellMachover] p. 490Definition of alephalephval3 9137
[BeltramettiCassinelli] p. 98Remarkatlatmstc 35126
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 29552
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 29594  chirredi 29593
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 29582
[Beran] p. 3Definition of joinsshjval3 28553
[Beran] p. 39Theorem 2.3(i)cmcm2 28815  cmcm2i 28792  cmcm2ii 28797  cmt2N 35057
[Beran] p. 40Theorem 2.3(iii)lecm 28816  lecmi 28801  lecmii 28802
[Beran] p. 45Theorem 3.4cmcmlem 28790
[Beran] p. 49Theorem 4.2cm2j 28819  cm2ji 28824  cm2mi 28825
[Beran] p. 95Definitiondf-sh 28404  issh2 28406
[Beran] p. 95Lemma 3.1(S5)his5 28283
[Beran] p. 95Lemma 3.1(S6)his6 28296
[Beran] p. 95Lemma 3.1(S7)his7 28287
[Beran] p. 95Lemma 3.2(S8)ho01i 29027
[Beran] p. 95Lemma 3.2(S9)hoeq1 29029
[Beran] p. 95Lemma 3.2(S10)ho02i 29028
[Beran] p. 95Lemma 3.2(S11)hoeq2 29030
[Beran] p. 95Postulate (S1)ax-his1 28279  his1i 28297
[Beran] p. 95Postulate (S2)ax-his2 28280
[Beran] p. 95Postulate (S3)ax-his3 28281
[Beran] p. 95Postulate (S4)ax-his4 28282
[Beran] p. 96Definition of normdf-hnorm 28165  dfhnorm2 28319  normval 28321
[Beran] p. 96Definition for Cauchy sequencehcau 28381
[Beran] p. 96Definition of Cauchy sequencedf-hcau 28170
[Beran] p. 96Definition of complete subspaceisch3 28438
[Beran] p. 96Definition of convergedf-hlim 28169  hlimi 28385
[Beran] p. 97Theorem 3.3(i)norm-i-i 28330  norm-i 28326
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 28334  norm-ii 28335  normlem0 28306  normlem1 28307  normlem2 28308  normlem3 28309  normlem4 28310  normlem5 28311  normlem6 28312  normlem7 28313  normlem7tALT 28316
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 28336  norm-iii 28337
[Beran] p. 98Remark 3.4bcs 28378  bcsiALT 28376  bcsiHIL 28377
[Beran] p. 98Remark 3.4(B)normlem9at 28318  normpar 28352  normpari 28351
[Beran] p. 98Remark 3.4(C)normpyc 28343  normpyth 28342  normpythi 28339
[Beran] p. 99Remarklnfn0 29246  lnfn0i 29241  lnop0 29165  lnop0i 29169
[Beran] p. 99Theorem 3.5(i)nmcexi 29225  nmcfnex 29252  nmcfnexi 29250  nmcopex 29228  nmcopexi 29226
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 29253  nmcfnlbi 29251  nmcoplb 29229  nmcoplbi 29227
[Beran] p. 99Theorem 3.5(iii)lnfncon 29255  lnfnconi 29254  lnopcon 29234  lnopconi 29233
[Beran] p. 100Lemma 3.6normpar2i 28353
[Beran] p. 101Lemma 3.6norm3adifi 28350  norm3adifii 28345  norm3dif 28347  norm3difi 28344
[Beran] p. 102Theorem 3.7(i)chocunii 28500  pjhth 28592  pjhtheu 28593  pjpjhth 28624  pjpjhthi 28625  pjth 23429
[Beran] p. 102Theorem 3.7(ii)ococ 28605  ococi 28604
[Beran] p. 103Remark 3.8nlelchi 29260
[Beran] p. 104Theorem 3.9riesz3i 29261  riesz4 29263  riesz4i 29262
[Beran] p. 104Theorem 3.10cnlnadj 29278  cnlnadjeu 29277  cnlnadjeui 29276  cnlnadji 29275  cnlnadjlem1 29266  nmopadjlei 29287
[Beran] p. 106Theorem 3.11(i)adjeq0 29290
[Beran] p. 106Theorem 3.11(v)nmopadji 29289
[Beran] p. 106Theorem 3.11(ii)adjmul 29291
[Beran] p. 106Theorem 3.11(iv)adjadj 29135
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 29301  nmopcoadji 29300
[Beran] p. 106Theorem 3.11(iii)adjadd 29292
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 29302
[Beran] p. 106Theorem 3.11(viii)adjcoi 29299  pjadj2coi 29403  pjadjcoi 29360
[Beran] p. 107Definitiondf-ch 28418  isch2 28420
[Beran] p. 107Remark 3.12choccl 28505  isch3 28438  occl 28503  ocsh 28482  shoccl 28504  shocsh 28483
[Beran] p. 107Remark 3.12(B)ococin 28607
[Beran] p. 108Theorem 3.13chintcl 28531
[Beran] p. 109Property (i)pjadj2 29386  pjadj3 29387  pjadji 28884  pjadjii 28873
[Beran] p. 109Property (ii)pjidmco 29380  pjidmcoi 29376  pjidmi 28872
[Beran] p. 110Definition of projector orderingpjordi 29372
[Beran] p. 111Remarkho0val 28949  pjch1 28869
[Beran] p. 111Definitiondf-hfmul 28933  df-hfsum 28932  df-hodif 28931  df-homul 28930  df-hosum 28929
[Beran] p. 111Lemma 4.4(i)pjo 28870
[Beran] p. 111Lemma 4.4(ii)pjch 28893  pjchi 28631
[Beran] p. 111Lemma 4.4(iii)pjoc2 28638  pjoc2i 28637
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 28879
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 29364  pjssmii 28880
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 29363
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 29362
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 29367
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 29365  pjssge0ii 28881
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 29366  pjdifnormii 28882
[Bobzien] p. 116Statement T3stoic3 1849
[Bobzien] p. 117Statement T2stoic2a 1847
[Bobzien] p. 117Statement T4stoic4a 1850
[Bobzien] p. 117Conclusion the contradictorystoic1a 1845
[Bogachev] p. 16Definition 1.5df-oms 30694
[Bogachev] p. 17Lemma 1.5.4omssubadd 30702
[Bogachev] p. 17Example 1.5.2omsmon 30700
[Bogachev] p. 41Definition 1.11.2df-carsg 30704
[Bogachev] p. 42Theorem 1.11.4carsgsiga 30724
[Bogachev] p. 116Definition 2.3.1df-itgm 30755  df-sitm 30733
[Bogachev] p. 118Chapter 2.4.4df-itgm 30755
[Bogachev] p. 118Definition 2.4.1df-sitg 30732
[Bollobas] p. 1Section I.1df-edg 26161  isuhgrop 26186  isusgrop 26279  isuspgrop 26278
[Bollobas] p. 2Section I.1df-subgr 26383  uhgrspan1 26418  uhgrspansubgr 26406
[Bollobas] p. 3Section I.1cusgrsize 26585  df-cusgr 26542  df-nbgr 26448  fusgrmaxsize 26595
[Bollobas] p. 4Definitiondf-upwlks 42238  df-wlks 26730
[Bollobas] p. 4Section I.1finsumvtxdg2size 26681  finsumvtxdgeven 26683  fusgr1th 26682  fusgrvtxdgonume 26685  vtxdgoddnumeven 26684
[Bollobas] p. 5Notationdf-pths 26847
[Bollobas] p. 5Definitiondf-crcts 26917  df-cycls 26918  df-trls 26824  df-wlkson 26731
[Bollobas] p. 7Section I.1df-ushgr 26175
[BourbakiAlg1] p. 1Definition 1df-clintop 42359  df-cllaw 42345  df-mgm 17450  df-mgm2 42378
[BourbakiAlg1] p. 4Definition 5df-assintop 42360  df-asslaw 42347  df-sgrp 17492  df-sgrp2 42380
[BourbakiAlg1] p. 7Definition 8df-cmgm2 42379  df-comlaw 42346
[BourbakiAlg1] p. 12Definition 2df-mnd 17503
[BourbakiAlg1] p. 92Definition 1df-ring 18757
[BourbakiAlg1] p. 93Section I.8.1df-rng0 42398
[BourbakiEns] p. Proposition 8fcof1 6688  fcofo 6689
[BourbakiTop1] p. Remarkxnegmnf 12246  xnegpnf 12245
[BourbakiTop1] p. Remark rexneg 12247
[BourbakiTop1] p. Remark 3ust0 22243  ustfilxp 22236
[BourbakiTop1] p. Axiom GT'tgpsubcn 22114
[BourbakiTop1] p. Example 1cstucnd 22308  iducn 22307  snfil 21888
[BourbakiTop1] p. Example 2neifil 21904
[BourbakiTop1] p. Theorem 1cnextcn 22091
[BourbakiTop1] p. Theorem 2ucnextcn 22328
[BourbakiTop1] p. Theorem 3df-hcmp 30343
[BourbakiTop1] p. Paragraph 3infil 21887
[BourbakiTop1] p. Propositionishmeo 21783
[BourbakiTop1] p. Definition 1df-ucn 22300  df-ust 22224  filintn0 21885  filn0 21886  istgp 22101  ucnprima 22306
[BourbakiTop1] p. Definition 2df-cfilu 22311
[BourbakiTop1] p. Definition 3df-cusp 22322  df-usp 22281  df-utop 22255  trust 22253
[BourbakiTop1] p. Definition 6df-pcmp 30263
[BourbakiTop1] p. Property V_issnei2 21141
[BourbakiTop1] p. Theorem 1(d)iscncl 21294
[BourbakiTop1] p. Condition F_Iustssel 22229
[BourbakiTop1] p. Condition U_Iustdiag 22232
[BourbakiTop1] p. Property V_iiinnei 21150
[BourbakiTop1] p. Property V_ivneiptopreu 21158  neissex 21152
[BourbakiTop1] p. Proposition 1neips 21138  neiss 21134  ucncn 22309  ustund 22245  ustuqtop 22270
[BourbakiTop1] p. Proposition 2cnpco 21292  neiptopreu 21158  utop2nei 22274  utop3cls 22275
[BourbakiTop1] p. Proposition 3fmucnd 22316  uspreg 22298  utopreg 22276
[BourbakiTop1] p. Proposition 4imasncld 21715  imasncls 21716  imasnopn 21714
[BourbakiTop1] p. Proposition 9cnpflf2 22024
[BourbakiTop1] p. Condition F_IIustincl 22231
[BourbakiTop1] p. Condition U_IIustinvel 22233
[BourbakiTop1] p. Property V_iiielnei 21136
[BourbakiTop1] p. Proposition 11cnextucn 22327
[BourbakiTop1] p. Condition F_IIbustbasel 22230
[BourbakiTop1] p. Condition U_IIIustexhalf 22234
[BourbakiTop1] p. Definition C'''df-cmp 21411
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 21870
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 20919
[BourbakiTop2] p. 195Definition 1df-ldlf 30260
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 40791
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 40793  stoweid 40792
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 40730  stoweidlem10 40739  stoweidlem14 40743  stoweidlem15 40744  stoweidlem35 40764  stoweidlem36 40765  stoweidlem37 40766  stoweidlem38 40767  stoweidlem40 40769  stoweidlem41 40770  stoweidlem43 40772  stoweidlem44 40773  stoweidlem46 40775  stoweidlem5 40734  stoweidlem50 40779  stoweidlem52 40781  stoweidlem53 40782  stoweidlem55 40784  stoweidlem56 40785
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 40752  stoweidlem24 40753  stoweidlem27 40756  stoweidlem28 40757  stoweidlem30 40759
[BrosowskiDeutsh] p. 91Proofstoweidlem34 40763  stoweidlem59 40788  stoweidlem60 40789
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 40774  stoweidlem49 40778  stoweidlem7 40736
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 40760  stoweidlem39 40768  stoweidlem42 40771  stoweidlem48 40777  stoweidlem51 40780  stoweidlem54 40783  stoweidlem57 40786  stoweidlem58 40787
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 40754
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 40746
[BrosowskiDeutsh] p. 92Proofstoweidlem11 40740  stoweidlem13 40742  stoweidlem26 40755  stoweidlem61 40790
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 40747
[Bruck] p. 1Section I.1df-clintop 42359  df-mgm 17450  df-mgm2 42378
[Bruck] p. 23Section II.1df-sgrp 17492  df-sgrp2 42380
[Bruck] p. 28Theorem 3.2dfgrp3 17722
[ChoquetDD] p. 2Definition of mappingdf-mpt 4865
[Church] p. 129Section II.24df-ifp 1050  dfifp2 1051
[Clemente] p. 10Definition ITnatded 27602
[Clemente] p. 10Definition I` `m,nnatded 27602
[Clemente] p. 11Definition E=>m,nnatded 27602
[Clemente] p. 11Definition I=>m,nnatded 27602
[Clemente] p. 11Definition E` `(1)natded 27602
[Clemente] p. 11Definition E` `(2)natded 27602
[Clemente] p. 12Definition E` `m,n,pnatded 27602
[Clemente] p. 12Definition I` `n(1)natded 27602
[Clemente] p. 12Definition I` `n(2)natded 27602
[Clemente] p. 13Definition I` `m,n,pnatded 27602
[Clemente] p. 14Proof 5.11natded 27602
[Clemente] p. 14Definition E` `nnatded 27602
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 27604  ex-natded5.2 27603
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 27607  ex-natded5.3 27606
[Clemente] p. 18Theorem 5.5ex-natded5.5 27609
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 27611  ex-natded5.7 27610
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 27613  ex-natded5.8 27612
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 27615  ex-natded5.13 27614
[Clemente] p. 32Definition I` `nnatded 27602
[Clemente] p. 32Definition E` `m,n,p,anatded 27602
[Clemente] p. 32Definition E` `n,tnatded 27602
[Clemente] p. 32Definition I` `n,tnatded 27602
[Clemente] p. 43Theorem 9.20ex-natded9.20 27616
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 27617
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 27619  ex-natded9.26 27618
[Cohen] p. 301Remarkrelogoprlem 24558
[Cohen] p. 301Property 2relogmul 24559  relogmuld 24592
[Cohen] p. 301Property 3relogdiv 24560  relogdivd 24593
[Cohen] p. 301Property 4relogexp 24563
[Cohen] p. 301Property 1alog1 24553
[Cohen] p. 301Property 1bloge 24554
[Cohen4] p. 348Observationrelogbcxpb 24746
[Cohen4] p. 349Propertyrelogbf 24750
[Cohen4] p. 352Definitionelogb 24729
[Cohen4] p. 361Property 2relogbmul 24736
[Cohen4] p. 361Property 3logbrec 24741  relogbdiv 24738
[Cohen4] p. 361Property 4relogbreexp 24734
[Cohen4] p. 361Property 6relogbexp 24739
[Cohen4] p. 361Property 1(a)logbid1 24727
[Cohen4] p. 361Property 1(b)logb1 24728
[Cohen4] p. 367Propertylogbchbase 24730
[Cohen4] p. 377Property 2logblt 24743
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 30687  sxbrsigalem4 30689
[Cohn] p. 81Section II.5acsdomd 17389  acsinfd 17388  acsinfdimd 17390  acsmap2d 17387  acsmapd 17386
[Cohn] p. 143Example 5.1.1sxbrsiga 30692
[Connell] p. 57Definitiondf-scmat 20515  df-scmatalt 42711
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 12868
[Crawley] p. 1Definition of posetdf-poset 17154
[Crawley] p. 107Theorem 13.2hlsupr 35193
[Crawley] p. 110Theorem 13.3arglem1N 35998  dalaw 35693
[Crawley] p. 111Theorem 13.4hlathil 37769
[Crawley] p. 111Definition of set Wdf-watsN 35797
[Crawley] p. 111Definition of dilationdf-dilN 35913  df-ldil 35911  isldil 35917
[Crawley] p. 111Definition of translationdf-ltrn 35912  df-trnN 35914  isltrn 35926  ltrnu 35928
[Crawley] p. 112Lemma Acdlema1N 35598  cdlema2N 35599  exatleN 35211
[Crawley] p. 112Lemma B1cvrat 35283  cdlemb 35601  cdlemb2 35848  cdlemb3 36414  idltrn 35957  l1cvat 34862  lhpat 35850  lhpat2 35852  lshpat 34863  ltrnel 35946  ltrnmw 35958
[Crawley] p. 112Lemma Ccdlemc1 35999  cdlemc2 36000  ltrnnidn 35982  trlat 35977  trljat1 35974  trljat2 35975  trljat3 35976  trlne 35993  trlnidat 35981  trlnle 35994
[Crawley] p. 112Definition of automorphismdf-pautN 35798
[Crawley] p. 113Lemma Ccdlemc 36005  cdlemc3 36001  cdlemc4 36002
[Crawley] p. 113Lemma Dcdlemd 36015  cdlemd1 36006  cdlemd2 36007  cdlemd3 36008  cdlemd4 36009  cdlemd5 36010  cdlemd6 36011  cdlemd7 36012  cdlemd8 36013  cdlemd9 36014  cdleme31sde 36193  cdleme31se 36190  cdleme31se2 36191  cdleme31snd 36194  cdleme32a 36249  cdleme32b 36250  cdleme32c 36251  cdleme32d 36252  cdleme32e 36253  cdleme32f 36254  cdleme32fva 36245  cdleme32fva1 36246  cdleme32fvcl 36248  cdleme32le 36255  cdleme48fv 36307  cdleme4gfv 36315  cdleme50eq 36349  cdleme50f 36350  cdleme50f1 36351  cdleme50f1o 36354  cdleme50laut 36355  cdleme50ldil 36356  cdleme50lebi 36348  cdleme50rn 36353  cdleme50rnlem 36352  cdlemeg49le 36319  cdlemeg49lebilem 36347
[Crawley] p. 113Lemma Ecdleme 36368  cdleme00a 36017  cdleme01N 36029  cdleme02N 36030  cdleme0a 36019  cdleme0aa 36018  cdleme0b 36020  cdleme0c 36021  cdleme0cp 36022  cdleme0cq 36023  cdleme0dN 36024  cdleme0e 36025  cdleme0ex1N 36031  cdleme0ex2N 36032  cdleme0fN 36026  cdleme0gN 36027  cdleme0moN 36033  cdleme1 36035  cdleme10 36062  cdleme10tN 36066  cdleme11 36078  cdleme11a 36068  cdleme11c 36069  cdleme11dN 36070  cdleme11e 36071  cdleme11fN 36072  cdleme11g 36073  cdleme11h 36074  cdleme11j 36075  cdleme11k 36076  cdleme11l 36077  cdleme12 36079  cdleme13 36080  cdleme14 36081  cdleme15 36086  cdleme15a 36082  cdleme15b 36083  cdleme15c 36084  cdleme15d 36085  cdleme16 36093  cdleme16aN 36067  cdleme16b 36087  cdleme16c 36088  cdleme16d 36089  cdleme16e 36090  cdleme16f 36091  cdleme16g 36092  cdleme19a 36111  cdleme19b 36112  cdleme19c 36113  cdleme19d 36114  cdleme19e 36115  cdleme19f 36116  cdleme1b 36034  cdleme2 36036  cdleme20aN 36117  cdleme20bN 36118  cdleme20c 36119  cdleme20d 36120  cdleme20e 36121  cdleme20f 36122  cdleme20g 36123  cdleme20h 36124  cdleme20i 36125  cdleme20j 36126  cdleme20k 36127  cdleme20l 36130  cdleme20l1 36128  cdleme20l2 36129  cdleme20m 36131  cdleme20y 36110  cdleme20zN 36109  cdleme21 36145  cdleme21d 36138  cdleme21e 36139  cdleme22a 36148  cdleme22aa 36147  cdleme22b 36149  cdleme22cN 36150  cdleme22d 36151  cdleme22e 36152  cdleme22eALTN 36153  cdleme22f 36154  cdleme22f2 36155  cdleme22g 36156  cdleme23a 36157  cdleme23b 36158  cdleme23c 36159  cdleme26e 36167  cdleme26eALTN 36169  cdleme26ee 36168  cdleme26f 36171  cdleme26f2 36173  cdleme26f2ALTN 36172  cdleme26fALTN 36170  cdleme27N 36177  cdleme27a 36175  cdleme27cl 36174  cdleme28c 36180  cdleme3 36045  cdleme30a 36186  cdleme31fv 36198  cdleme31fv1 36199  cdleme31fv1s 36200  cdleme31fv2 36201  cdleme31id 36202  cdleme31sc 36192  cdleme31sdnN 36195  cdleme31sn 36188  cdleme31sn1 36189  cdleme31sn1c 36196  cdleme31sn2 36197  cdleme31so 36187  cdleme35a 36256  cdleme35b 36258  cdleme35c 36259  cdleme35d 36260  cdleme35e 36261  cdleme35f 36262  cdleme35fnpq 36257  cdleme35g 36263  cdleme35h 36264  cdleme35h2 36265  cdleme35sn2aw 36266  cdleme35sn3a 36267  cdleme36a 36268  cdleme36m 36269  cdleme37m 36270  cdleme38m 36271  cdleme38n 36272  cdleme39a 36273  cdleme39n 36274  cdleme3b 36037  cdleme3c 36038  cdleme3d 36039  cdleme3e 36040  cdleme3fN 36041  cdleme3fa 36044  cdleme3g 36042  cdleme3h 36043  cdleme4 36046  cdleme40m 36275  cdleme40n 36276  cdleme40v 36277  cdleme40w 36278  cdleme41fva11 36285  cdleme41sn3aw 36282  cdleme41sn4aw 36283  cdleme41snaw 36284  cdleme42a 36279  cdleme42b 36286  cdleme42c 36280  cdleme42d 36281  cdleme42e 36287  cdleme42f 36288  cdleme42g 36289  cdleme42h 36290  cdleme42i 36291  cdleme42k 36292  cdleme42ke 36293  cdleme42keg 36294  cdleme42mN 36295  cdleme42mgN 36296  cdleme43aN 36297  cdleme43bN 36298  cdleme43cN 36299  cdleme43dN 36300  cdleme5 36048  cdleme50ex 36367  cdleme50ltrn 36365  cdleme51finvN 36364  cdleme51finvfvN 36363  cdleme51finvtrN 36366  cdleme6 36049  cdleme7 36057  cdleme7a 36051  cdleme7aa 36050  cdleme7b 36052  cdleme7c 36053  cdleme7d 36054  cdleme7e 36055  cdleme7ga 36056  cdleme8 36058  cdleme8tN 36063  cdleme9 36061  cdleme9a 36059  cdleme9b 36060  cdleme9tN 36065  cdleme9taN 36064  cdlemeda 36106  cdlemedb 36105  cdlemednpq 36107  cdlemednuN 36108  cdlemefr27cl 36211  cdlemefr32fva1 36218  cdlemefr32fvaN 36217  cdlemefrs32fva 36208  cdlemefrs32fva1 36209  cdlemefs27cl 36221  cdlemefs32fva1 36231  cdlemefs32fvaN 36230  cdlemesner 36104  cdlemeulpq 36028
[Crawley] p. 114Lemma E4atex 35883  4atexlem7 35882  cdleme0nex 36098  cdleme17a 36094  cdleme17c 36096  cdleme17d 36306  cdleme17d1 36097  cdleme17d2 36303  cdleme18a 36099  cdleme18b 36100  cdleme18c 36101  cdleme18d 36103  cdleme4a 36047
[Crawley] p. 115Lemma Ecdleme21a 36133  cdleme21at 36136  cdleme21b 36134  cdleme21c 36135  cdleme21ct 36137  cdleme21f 36140  cdleme21g 36141  cdleme21h 36142  cdleme21i 36143  cdleme22gb 36102
[Crawley] p. 116Lemma Fcdlemf 36371  cdlemf1 36369  cdlemf2 36370
[Crawley] p. 116Lemma Gcdlemftr1 36375  cdlemg16 36465  cdlemg28 36512  cdlemg28a 36501  cdlemg28b 36511  cdlemg3a 36405  cdlemg42 36537  cdlemg43 36538  cdlemg44 36541  cdlemg44a 36539  cdlemg46 36543  cdlemg47 36544  cdlemg9 36442  ltrnco 36527  ltrncom 36546  tgrpabl 36559  trlco 36535
[Crawley] p. 116Definition of Gdf-tgrp 36551
[Crawley] p. 117Lemma Gcdlemg17 36485  cdlemg17b 36470
[Crawley] p. 117Definition of Edf-edring-rN 36564  df-edring 36565
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 36568
[Crawley] p. 118Remarktendopltp 36588
[Crawley] p. 118Lemma Hcdlemh 36625  cdlemh1 36623  cdlemh2 36624
[Crawley] p. 118Lemma Icdlemi 36628  cdlemi1 36626  cdlemi2 36627
[Crawley] p. 118Lemma Jcdlemj1 36629  cdlemj2 36630  cdlemj3 36631  tendocan 36632
[Crawley] p. 118Lemma Kcdlemk 36782  cdlemk1 36639  cdlemk10 36651  cdlemk11 36657  cdlemk11t 36754  cdlemk11ta 36737  cdlemk11tb 36739  cdlemk11tc 36753  cdlemk11u-2N 36697  cdlemk11u 36679  cdlemk12 36658  cdlemk12u-2N 36698  cdlemk12u 36680  cdlemk13-2N 36684  cdlemk13 36660  cdlemk14-2N 36686  cdlemk14 36662  cdlemk15-2N 36687  cdlemk15 36663  cdlemk16-2N 36688  cdlemk16 36665  cdlemk16a 36664  cdlemk17-2N 36689  cdlemk17 36666  cdlemk18-2N 36694  cdlemk18-3N 36708  cdlemk18 36676  cdlemk19-2N 36695  cdlemk19 36677  cdlemk19u 36778  cdlemk1u 36667  cdlemk2 36640  cdlemk20-2N 36700  cdlemk20 36682  cdlemk21-2N 36699  cdlemk21N 36681  cdlemk22-3 36709  cdlemk22 36701  cdlemk23-3 36710  cdlemk24-3 36711  cdlemk25-3 36712  cdlemk26-3 36714  cdlemk26b-3 36713  cdlemk27-3 36715  cdlemk28-3 36716  cdlemk29-3 36719  cdlemk3 36641  cdlemk30 36702  cdlemk31 36704  cdlemk32 36705  cdlemk33N 36717  cdlemk34 36718  cdlemk35 36720  cdlemk36 36721  cdlemk37 36722  cdlemk38 36723  cdlemk39 36724  cdlemk39u 36776  cdlemk4 36642  cdlemk41 36728  cdlemk42 36749  cdlemk42yN 36752  cdlemk43N 36771  cdlemk45 36755  cdlemk46 36756  cdlemk47 36757  cdlemk48 36758  cdlemk49 36759  cdlemk5 36644  cdlemk50 36760  cdlemk51 36761  cdlemk52 36762  cdlemk53 36765  cdlemk54 36766  cdlemk55 36769  cdlemk55u 36774  cdlemk56 36779  cdlemk5a 36643  cdlemk5auN 36668  cdlemk5u 36669  cdlemk6 36645  cdlemk6u 36670  cdlemk7 36656  cdlemk7u-2N 36696  cdlemk7u 36678  cdlemk8 36646  cdlemk9 36647  cdlemk9bN 36648  cdlemki 36649  cdlemkid 36744  cdlemkj-2N 36690  cdlemkj 36671  cdlemksat 36654  cdlemksel 36653  cdlemksv 36652  cdlemksv2 36655  cdlemkuat 36674  cdlemkuel-2N 36692  cdlemkuel-3 36706  cdlemkuel 36673  cdlemkuv-2N 36691  cdlemkuv2-2 36693  cdlemkuv2-3N 36707  cdlemkuv2 36675  cdlemkuvN 36672  cdlemkvcl 36650  cdlemky 36734  cdlemkyyN 36770  tendoex 36783
[Crawley] p. 120Remarkdva1dim 36793
[Crawley] p. 120Lemma Lcdleml1N 36784  cdleml2N 36785  cdleml3N 36786  cdleml4N 36787  cdleml5N 36788  cdleml6 36789  cdleml7 36790  cdleml8 36791  cdleml9 36792  dia1dim 36869
[Crawley] p. 120Lemma Mdia11N 36856  diaf11N 36857  dialss 36854  diaord 36855  dibf11N 36969  djajN 36945
[Crawley] p. 120Definition of isomorphism mapdiaval 36840
[Crawley] p. 121Lemma Mcdlemm10N 36926  dia2dimlem1 36872  dia2dimlem2 36873  dia2dimlem3 36874  dia2dimlem4 36875  dia2dimlem5 36876  diaf1oN 36938  diarnN 36937  dvheveccl 36920  dvhopN 36924
[Crawley] p. 121Lemma Ncdlemn 37020  cdlemn10 37014  cdlemn11 37019  cdlemn11a 37015  cdlemn11b 37016  cdlemn11c 37017  cdlemn11pre 37018  cdlemn2 37003  cdlemn2a 37004  cdlemn3 37005  cdlemn4 37006  cdlemn4a 37007  cdlemn5 37009  cdlemn5pre 37008  cdlemn6 37010  cdlemn7 37011  cdlemn8 37012  cdlemn9 37013  diclspsn 37002
[Crawley] p. 121Definition of phi(q)df-dic 36981
[Crawley] p. 122Lemma Ndih11 37073  dihf11 37075  dihjust 37025  dihjustlem 37024  dihord 37072  dihord1 37026  dihord10 37031  dihord11b 37030  dihord11c 37032  dihord2 37035  dihord2a 37027  dihord2b 37028  dihord2cN 37029  dihord2pre 37033  dihord2pre2 37034  dihordlem6 37021  dihordlem7 37022  dihordlem7b 37023
[Crawley] p. 122Definition of isomorphism mapdihffval 37038  dihfval 37039  dihval 37040
[Diestel] p. 3Section 1.1df-cusgr 26542  df-nbgr 26448
[Diestel] p. 4Section 1.1df-subgr 26383  uhgrspan1 26418  uhgrspansubgr 26406
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 26685  vtxdgoddnumeven 26684
[Diestel] p. 27Section 1.10df-ushgr 26175
[Eisenberg] p. 67Definition 5.3df-dif 3726
[Eisenberg] p. 82Definition 6.3dfom3 8712
[Eisenberg] p. 125Definition 8.21df-map 8015
[Eisenberg] p. 216Example 13.2(4)omenps 8720
[Eisenberg] p. 310Theorem 19.8cardprc 9010
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 9583
[Enderton] p. 18Axiom of Empty Setaxnul 4923
[Enderton] p. 19Definitiondf-tp 4322
[Enderton] p. 26Exercise 5unissb 4606
[Enderton] p. 26Exercise 10pwel 5049
[Enderton] p. 28Exercise 7(b)pwun 5156
[Enderton] p. 30Theorem "Distributive laws"iinin1 4726  iinin2 4725  iinun2 4721  iunin1 4720  iunin1f 29712  iunin2 4719  uniin1 29705  uniin2 29706
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4724  iundif2 4722
[Enderton] p. 32Exercise 20unineq 4026
[Enderton] p. 33Exercise 23iinuni 4744
[Enderton] p. 33Exercise 25iununi 4745
[Enderton] p. 33Exercise 24(a)iinpw 4752
[Enderton] p. 33Exercise 24(b)iunpw 7129  iunpwss 4753
[Enderton] p. 36Definitionopthwiener 5108
[Enderton] p. 38Exercise 6(a)unipw 5047
[Enderton] p. 38Exercise 6(b)pwuni 4611
[Enderton] p. 41Lemma 3Dopeluu 5067  rnex 7251  rnexg 7249
[Enderton] p. 41Exercise 8dmuni 5471  rnuni 5684
[Enderton] p. 42Definition of a functiondffun7 6057  dffun8 6058
[Enderton] p. 43Definition of function valuefunfv2 6410
[Enderton] p. 43Definition of single-rootedfuncnv 6097
[Enderton] p. 44Definition (d)dfima2 5608  dfima3 5609
[Enderton] p. 47Theorem 3Hfvco2 6417
[Enderton] p. 49Axiom of Choice (first form)ac7 9501  ac7g 9502  df-ac 9143  dfac2 9158  dfac2a 9156  dfac2b 9157  dfac3 9148  dfac7 9160
[Enderton] p. 50Theorem 3K(a)imauni 6650
[Enderton] p. 52Definitiondf-map 8015
[Enderton] p. 53Exercise 21coass 5797
[Enderton] p. 53Exercise 27dmco 5786
[Enderton] p. 53Exercise 14(a)funin 6104
[Enderton] p. 53Exercise 22(a)imass2 5641
[Enderton] p. 54Remarkixpf 8088  ixpssmap 8100
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8067
[Enderton] p. 55Axiom of Choice (second form)ac9 9511  ac9s 9521
[Enderton] p. 56Theorem 3Merref 7920
[Enderton] p. 57Lemma 3Nerthi 7949
[Enderton] p. 57Definitiondf-ec 7902
[Enderton] p. 58Definitiondf-qs 7906
[Enderton] p. 61Exercise 35df-ec 7902
[Enderton] p. 65Exercise 56(a)dmun 5468
[Enderton] p. 68Definition of successordf-suc 5871
[Enderton] p. 71Definitiondf-tr 4888  dftr4 4892
[Enderton] p. 72Theorem 4Eunisuc 5943
[Enderton] p. 73Exercise 6unisuc 5943
[Enderton] p. 73Exercise 5(a)truni 4901
[Enderton] p. 73Exercise 5(b)trint 4902  trintALT 39637
[Enderton] p. 79Theorem 4I(A1)nna0 7842
[Enderton] p. 79Theorem 4I(A2)nnasuc 7844  onasuc 7766
[Enderton] p. 79Definition of operation valuedf-ov 6799
[Enderton] p. 80Theorem 4J(A1)nnm0 7843
[Enderton] p. 80Theorem 4J(A2)nnmsuc 7845  onmsuc 7767
[Enderton] p. 81Theorem 4K(1)nnaass 7860
[Enderton] p. 81Theorem 4K(2)nna0r 7847  nnacom 7855
[Enderton] p. 81Theorem 4K(3)nndi 7861
[Enderton] p. 81Theorem 4K(4)nnmass 7862
[Enderton] p. 81Theorem 4K(5)nnmcom 7864
[Enderton] p. 82Exercise 16nnm0r 7848  nnmsucr 7863
[Enderton] p. 88Exercise 23nnaordex 7876
[Enderton] p. 129Definitiondf-en 8114
[Enderton] p. 132Theorem 6B(b)canth 6754
[Enderton] p. 133Exercise 1xpomen 9042
[Enderton] p. 133Exercise 2qnnen 15148
[Enderton] p. 134Theorem (Pigeonhole Principle)php 8304
[Enderton] p. 135Corollary 6Cphp3 8306
[Enderton] p. 136Corollary 6Enneneq 8303
[Enderton] p. 136Corollary 6D(a)pssinf 8330
[Enderton] p. 136Corollary 6D(b)ominf 8332
[Enderton] p. 137Lemma 6Fpssnn 8338
[Enderton] p. 138Corollary 6Gssfi 8340
[Enderton] p. 139Theorem 6H(c)mapen 8284
[Enderton] p. 142Theorem 6I(3)xpcdaen 9211
[Enderton] p. 142Theorem 6I(4)mapcdaen 9212
[Enderton] p. 143Theorem 6Jcda0en 9207  cda1en 9203
[Enderton] p. 144Exercise 13iunfi 8414  unifi 8415  unifi2 8416
[Enderton] p. 144Corollary 6Kundif2 4187  unfi 8387  unfi2 8389
[Enderton] p. 145Figure 38ffoss 7278
[Enderton] p. 145Definitiondf-dom 8115
[Enderton] p. 146Example 1domen 8126  domeng 8127
[Enderton] p. 146Example 3nndomo 8314  nnsdom 8719  nnsdomg 8379
[Enderton] p. 149Theorem 6L(a)cdadom2 9215
[Enderton] p. 149Theorem 6L(c)mapdom1 8285  xpdom1 8219  xpdom1g 8217  xpdom2g 8216
[Enderton] p. 149Theorem 6L(d)mapdom2 8291
[Enderton] p. 151Theorem 6Mzorn 9535  zorng 9532
[Enderton] p. 151Theorem 6M(4)ac8 9520  dfac5 9155
[Enderton] p. 159Theorem 6Qunictb 9603
[Enderton] p. 164Exampleinfdif 9237
[Enderton] p. 168Definitiondf-po 5171
[Enderton] p. 192Theorem 7M(a)oneli 5977
[Enderton] p. 192Theorem 7M(b)ontr1 5913
[Enderton] p. 192Theorem 7M(c)onirri 5976
[Enderton] p. 193Corollary 7N(b)0elon 5920
[Enderton] p. 193Corollary 7N(c)onsuci 7189
[Enderton] p. 193Corollary 7N(d)ssonunii 7138
[Enderton] p. 194Remarkonprc 7135
[Enderton] p. 194Exercise 16suc11 5973
[Enderton] p. 197Definitiondf-card 8969
[Enderton] p. 197Theorem 7Pcarden 9579
[Enderton] p. 200Exercise 25tfis 7205
[Enderton] p. 202Lemma 7Tr1tr 8807
[Enderton] p. 202Definitiondf-r1 8795
[Enderton] p. 202Theorem 7Qr1val1 8817
[Enderton] p. 204Theorem 7V(b)rankval4 8898
[Enderton] p. 206Theorem 7X(b)en2lp 8670
[Enderton] p. 207Exercise 30rankpr 8888  rankprb 8882  rankpw 8874  rankpwi 8854  rankuniss 8897
[Enderton] p. 207Exercise 34opthreg 8681
[Enderton] p. 208Exercise 35suc11reg 8684
[Enderton] p. 212Definition of alephalephval3 9137
[Enderton] p. 213Theorem 8A(a)alephord2 9103
[Enderton] p. 213Theorem 8A(b)cardalephex 9117
[Enderton] p. 218Theorem Schema 8Eonfununi 7595
[Enderton] p. 222Definition of kardkarden 8926  kardex 8925
[Enderton] p. 238Theorem 8Roeoa 7835
[Enderton] p. 238Theorem 8Soeoe 7837
[Enderton] p. 240Exercise 25oarec 7800
[Enderton] p. 257Definition of cofinalitycflm 9278
[FaureFrolicher] p. 57Definition 3.1.9mreexd 16510
[FaureFrolicher] p. 83Definition 4.1.1df-mri 16456
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 17385  mrieqv2d 16507  mrieqvd 16506
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 16511
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 16516  mreexexlem2d 16513
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 17391  mreexfidimd 16518
[Frege1879] p. 11Statementdf3or2 38584
[Frege1879] p. 12Statementdf3an2 38585  dfxor4 38582  dfxor5 38583
[Frege1879] p. 26Axiom 1ax-frege1 38608
[Frege1879] p. 26Axiom 2ax-frege2 38609
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 38613
[Frege1879] p. 31Proposition 4frege4 38617
[Frege1879] p. 32Proposition 5frege5 38618
[Frege1879] p. 33Proposition 6frege6 38624
[Frege1879] p. 34Proposition 7frege7 38626
[Frege1879] p. 35Axiom 8ax-frege8 38627  axfrege8 38625
[Frege1879] p. 35Proposition 8pm2.04 90  wl-pm2.04 33605
[Frege1879] p. 35Proposition 9frege9 38630
[Frege1879] p. 36Proposition 10frege10 38638
[Frege1879] p. 36Proposition 11frege11 38632
[Frege1879] p. 37Proposition 12frege12 38631
[Frege1879] p. 37Proposition 13frege13 38640
[Frege1879] p. 37Proposition 14frege14 38641
[Frege1879] p. 38Proposition 15frege15 38644
[Frege1879] p. 38Proposition 16frege16 38634
[Frege1879] p. 39Proposition 17frege17 38639
[Frege1879] p. 39Proposition 18frege18 38636
[Frege1879] p. 39Proposition 19frege19 38642
[Frege1879] p. 40Proposition 20frege20 38646
[Frege1879] p. 40Proposition 21frege21 38645
[Frege1879] p. 41Proposition 22frege22 38637
[Frege1879] p. 42Proposition 23frege23 38643
[Frege1879] p. 42Proposition 24frege24 38633
[Frege1879] p. 42Proposition 25frege25 38635  rp-frege25 38623
[Frege1879] p. 42Proposition 26frege26 38628
[Frege1879] p. 43Axiom 28ax-frege28 38648
[Frege1879] p. 43Proposition 27frege27 38629
[Frege1879] p. 43Proposition 28con3 150
[Frege1879] p. 43Proposition 29frege29 38649
[Frege1879] p. 44Axiom 31ax-frege31 38652  axfrege31 38651
[Frege1879] p. 44Proposition 30frege30 38650
[Frege1879] p. 44Proposition 31notnotr 128
[Frege1879] p. 44Proposition 32frege32 38653
[Frege1879] p. 44Proposition 33frege33 38654
[Frege1879] p. 45Proposition 34frege34 38655
[Frege1879] p. 45Proposition 35frege35 38656
[Frege1879] p. 45Proposition 36frege36 38657
[Frege1879] p. 46Proposition 37frege37 38658
[Frege1879] p. 46Proposition 38frege38 38659
[Frege1879] p. 46Proposition 39frege39 38660
[Frege1879] p. 46Proposition 40frege40 38661
[Frege1879] p. 47Axiom 41ax-frege41 38663  axfrege41 38662
[Frege1879] p. 47Proposition 41notnot 138
[Frege1879] p. 47Proposition 42frege42 38664
[Frege1879] p. 47Proposition 43frege43 38665
[Frege1879] p. 47Proposition 44frege44 38666
[Frege1879] p. 47Proposition 45frege45 38667
[Frege1879] p. 48Proposition 46frege46 38668
[Frege1879] p. 48Proposition 47frege47 38669
[Frege1879] p. 49Proposition 48frege48 38670
[Frege1879] p. 49Proposition 49frege49 38671
[Frege1879] p. 49Proposition 50frege50 38672
[Frege1879] p. 50Axiom 52ax-frege52a 38675  ax-frege52c 38706  frege52aid 38676  frege52b 38707
[Frege1879] p. 50Axiom 54ax-frege54a 38680  ax-frege54c 38710  frege54b 38711
[Frege1879] p. 50Proposition 51frege51 38673
[Frege1879] p. 50Proposition 52dfsbcq 3589
[Frege1879] p. 50Proposition 53frege53a 38678  frege53aid 38677  frege53b 38708  frege53c 38732
[Frege1879] p. 50Proposition 54biid 251  eqid 2771
[Frege1879] p. 50Proposition 55frege55a 38686  frege55aid 38683  frege55b 38715  frege55c 38736  frege55cor1a 38687  frege55lem2a 38685  frege55lem2b 38714  frege55lem2c 38735
[Frege1879] p. 50Proposition 56frege56a 38689  frege56aid 38688  frege56b 38716  frege56c 38737
[Frege1879] p. 51Axiom 58ax-frege58a 38693  ax-frege58b 38719  frege58bid 38720  frege58c 38739
[Frege1879] p. 51Proposition 57frege57a 38691  frege57aid 38690  frege57b 38717  frege57c 38738
[Frege1879] p. 51Proposition 58spsbc 3600
[Frege1879] p. 51Proposition 59frege59a 38695  frege59b 38722  frege59c 38740
[Frege1879] p. 52Proposition 60frege60a 38696  frege60b 38723  frege60c 38741
[Frege1879] p. 52Proposition 61frege61a 38697  frege61b 38724  frege61c 38742
[Frege1879] p. 52Proposition 62frege62a 38698  frege62b 38725  frege62c 38743
[Frege1879] p. 52Proposition 63frege63a 38699  frege63b 38726  frege63c 38744
[Frege1879] p. 53Proposition 64frege64a 38700  frege64b 38727  frege64c 38745
[Frege1879] p. 53Proposition 65frege65a 38701  frege65b 38728  frege65c 38746
[Frege1879] p. 54Proposition 66frege66a 38702  frege66b 38729  frege66c 38747
[Frege1879] p. 54Proposition 67frege67a 38703  frege67b 38730  frege67c 38748
[Frege1879] p. 54Proposition 68frege68a 38704  frege68b 38731  frege68c 38749
[Frege1879] p. 55Definition 69dffrege69 38750
[Frege1879] p. 58Proposition 70frege70 38751
[Frege1879] p. 59Proposition 71frege71 38752
[Frege1879] p. 59Proposition 72frege72 38753
[Frege1879] p. 59Proposition 73frege73 38754
[Frege1879] p. 60Definition 76dffrege76 38757
[Frege1879] p. 60Proposition 74frege74 38755
[Frege1879] p. 60Proposition 75frege75 38756
[Frege1879] p. 62Proposition 77frege77 38758  frege77d 38562
[Frege1879] p. 63Proposition 78frege78 38759
[Frege1879] p. 63Proposition 79frege79 38760
[Frege1879] p. 63Proposition 80frege80 38761
[Frege1879] p. 63Proposition 81frege81 38762  frege81d 38563
[Frege1879] p. 64Proposition 82frege82 38763
[Frege1879] p. 65Proposition 83frege83 38764  frege83d 38564
[Frege1879] p. 65Proposition 84frege84 38765
[Frege1879] p. 66Proposition 85frege85 38766
[Frege1879] p. 66Proposition 86frege86 38767
[Frege1879] p. 66Proposition 87frege87 38768  frege87d 38566
[Frege1879] p. 67Proposition 88frege88 38769
[Frege1879] p. 68Proposition 89frege89 38770
[Frege1879] p. 68Proposition 90frege90 38771
[Frege1879] p. 68Proposition 91frege91 38772  frege91d 38567
[Frege1879] p. 69Proposition 92frege92 38773
[Frege1879] p. 70Proposition 93frege93 38774
[Frege1879] p. 70Proposition 94frege94 38775
[Frege1879] p. 70Proposition 95frege95 38776
[Frege1879] p. 71Definition 99dffrege99 38780
[Frege1879] p. 71Proposition 96frege96 38777  frege96d 38565
[Frege1879] p. 71Proposition 97frege97 38778  frege97d 38568
[Frege1879] p. 71Proposition 98frege98 38779  frege98d 38569
[Frege1879] p. 72Proposition 100frege100 38781
[Frege1879] p. 72Proposition 101frege101 38782
[Frege1879] p. 72Proposition 102frege102 38783  frege102d 38570
[Frege1879] p. 73Proposition 103frege103 38784
[Frege1879] p. 73Proposition 104frege104 38785
[Frege1879] p. 73Proposition 105frege105 38786
[Frege1879] p. 73Proposition 106frege106 38787  frege106d 38571
[Frege1879] p. 74Proposition 107frege107 38788
[Frege1879] p. 74Proposition 108frege108 38789  frege108d 38572
[Frege1879] p. 74Proposition 109frege109 38790  frege109d 38573
[Frege1879] p. 75Proposition 110frege110 38791
[Frege1879] p. 75Proposition 111frege111 38792  frege111d 38575
[Frege1879] p. 76Proposition 112frege112 38793
[Frege1879] p. 76Proposition 113frege113 38794
[Frege1879] p. 76Proposition 114frege114 38795  frege114d 38574
[Frege1879] p. 77Definition 115dffrege115 38796
[Frege1879] p. 77Proposition 116frege116 38797
[Frege1879] p. 78Proposition 117frege117 38798
[Frege1879] p. 78Proposition 118frege118 38799
[Frege1879] p. 78Proposition 119frege119 38800
[Frege1879] p. 78Proposition 120frege120 38801
[Frege1879] p. 79Proposition 121frege121 38802
[Frege1879] p. 79Proposition 122frege122 38803  frege122d 38576
[Frege1879] p. 79Proposition 123frege123 38804
[Frege1879] p. 80Proposition 124frege124 38805  frege124d 38577
[Frege1879] p. 81Proposition 125frege125 38806
[Frege1879] p. 81Proposition 126frege126 38807  frege126d 38578
[Frege1879] p. 82Proposition 127frege127 38808
[Frege1879] p. 83Proposition 128frege128 38809
[Frege1879] p. 83Proposition 129frege129 38810  frege129d 38579
[Frege1879] p. 84Proposition 130frege130 38811
[Frege1879] p. 85Proposition 131frege131 38812  frege131d 38580
[Frege1879] p. 86Proposition 132frege132 38813
[Frege1879] p. 86Proposition 133frege133 38814  frege133d 38581
[Fremlin1] p. 13Definition 111G (b)df-salgen 41045
[Fremlin1] p. 13Definition 111G (d)borelmbl 41365
[Fremlin1] p. 13Proposition 111G (b)salgenss 41066
[Fremlin1] p. 14Definition 112Aismea 41180
[Fremlin1] p. 15Remark 112B (d)psmeasure 41200
[Fremlin1] p. 15Property 112C (a)meadjun 41191  meadjunre 41205
[Fremlin1] p. 15Property 112C (b)meassle 41192
[Fremlin1] p. 15Property 112C (c)meaunle 41193
[Fremlin1] p. 16Property 112C (d)iundjiun 41189  meaiunle 41198  meaiunlelem 41197
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 41210  meaiuninc2 41211  meaiuninc3 41214  meaiuninc3v 41213  meaiunincf 41212  meaiuninclem 41209
[Fremlin1] p. 16Proposition 112C (f)meaiininc 41216  meaiininc2 41217  meaiininclem 41215
[Fremlin1] p. 19Theorem 113Ccaragen0 41235  caragendifcl 41243  caratheodory 41257  omelesplit 41247
[Fremlin1] p. 19Definition 113Aisome 41223  isomennd 41260  isomenndlem 41259
[Fremlin1] p. 19Remark 113B (c)omeunle 41245
[Fremlin1] p. 19Definition 112Dfcaragencmpl 41264  voncmpl 41350
[Fremlin1] p. 19Definition 113A (ii)omessle 41227
[Fremlin1] p. 20Theorem 113Ccarageniuncl 41252  carageniuncllem1 41250  carageniuncllem2 41251  caragenuncl 41242  caragenuncllem 41241  caragenunicl 41253
[Fremlin1] p. 21Remark 113Dcaragenel2d 41261
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 41255  caratheodorylem2 41256
[Fremlin1] p. 21Exercise 113Xacaragencmpl 41264
[Fremlin1] p. 23Lemma 114Bhoidmv1le 41323  hoidmv1lelem1 41320  hoidmv1lelem2 41321  hoidmv1lelem3 41322
[Fremlin1] p. 25Definition 114Eisvonmbl 41367
[Fremlin1] p. 29Lemma 115Bhoidmv1le 41323  hoidmvle 41329  hoidmvlelem1 41324  hoidmvlelem2 41325  hoidmvlelem3 41326  hoidmvlelem4 41327  hoidmvlelem5 41328  hsphoidmvle2 41314  hsphoif 41305  hsphoival 41308
[Fremlin1] p. 29Definition 1135 (b)hoicvr 41277
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 41285
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 41312  hoidmvn0val 41313  hoidmvval 41306  hoidmvval0 41316  hoidmvval0b 41319
[Fremlin1] p. 30Lemma 115Bhoiprodp1 41317  hsphoidmvle 41315
[Fremlin1] p. 30Definition 115Cdf-ovoln 41266  df-voln 41268
[Fremlin1] p. 30Proposition 115D (a)dmovn 41333  ovn0 41295  ovn0lem 41294  ovnf 41292  ovnome 41302  ovnssle 41290  ovnsslelem 41289  ovnsupge0 41286
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 41332  ovnhoilem1 41330  ovnhoilem2 41331  vonhoi 41396
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 41349  hoidifhspf 41347  hoidifhspval 41337  hoidifhspval2 41344  hoidifhspval3 41348  hspmbl 41358  hspmbllem1 41355  hspmbllem2 41356  hspmbllem3 41357
[Fremlin1] p. 31Definition 115Evoncmpl 41350  vonmea 41303
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 41301  ovnsubadd2 41375  ovnsubadd2lem 41374  ovnsubaddlem1 41299  ovnsubaddlem2 41300
[Fremlin1] p. 32Proposition 115G (a)hoimbl 41360  hoimbl2 41394  hoimbllem 41359  hspdifhsp 41345  opnvonmbl 41363  opnvonmbllem2 41362
[Fremlin1] p. 32Proposition 115G (b)borelmbl 41365
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 41408  iccvonmbllem 41407  ioovonmbl 41406
[Fremlin1] p. 32Proposition 115G (d)vonicc 41414  vonicclem2 41413  vonioo 41411  vonioolem2 41410  vonn0icc 41417  vonn0icc2 41421  vonn0ioo 41416  vonn0ioo2 41419
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 41418  snvonmbl 41415  vonct 41422  vonsn 41420
[Fremlin1] p. 35Lemma 121Asubsalsal 41089
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 41088  subsaliuncllem 41087
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 41449  salpreimalegt 41435  salpreimaltle 41450
[Fremlin1] p. 35Proposition 121B (i)issmf 41452  issmff 41458  issmflem 41451
[Fremlin1] p. 35Proposition 121B (ii)issmfle 41469  issmflelem 41468  smfpreimale 41478
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 41480  issmfgtlem 41479
[Fremlin1] p. 36Definition 121Cdf-smblfn 41425  issmf 41452  issmff 41458  issmfge 41493  issmfgelem 41492  issmfgt 41480  issmfgtlem 41479  issmfle 41469  issmflelem 41468  issmflem 41451
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 41433  salpreimagtlt 41454  salpreimalelt 41453
[Fremlin1] p. 36Proposition 121B (iv)issmfge 41493  issmfgelem 41492
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 41477
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 41475  cnfsmf 41464
[Fremlin1] p. 36Proposition 121D (c)decsmf 41490  decsmflem 41489  incsmf 41466  incsmflem 41465
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 41429  pimconstlt1 41430  smfconst 41473
[Fremlin1] p. 37Proposition 121E (b)smfadd 41488  smfaddlem1 41486  smfaddlem2 41487
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 41518
[Fremlin1] p. 37Proposition 121E (d)smfmul 41517  smfmullem1 41513  smfmullem2 41514  smfmullem3 41515  smfmullem4 41516
[Fremlin1] p. 37Proposition 121E (e)smfdiv 41519
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 41522  smfpimbor1lem2 41521
[Fremlin1] p. 37Proposition 121E (g)smfco 41524
[Fremlin1] p. 37Proposition 121E (h)smfres 41512
[Fremlin1] p. 38Proposition 121E (e)smfrec 41511
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 41520  smfresal 41510
[Fremlin1] p. 38Proposition 121F (a)smflim 41500  smflim2 41527  smflimlem1 41494  smflimlem2 41495  smflimlem3 41496  smflimlem4 41497  smflimlem5 41498  smflimlem6 41499  smflimmpt 41531
[Fremlin1] p. 38Proposition 121F (b)smfsup 41535  smfsuplem1 41532  smfsuplem2 41533  smfsuplem3 41534  smfsupmpt 41536  smfsupxr 41537
[Fremlin1] p. 38Proposition 121F (c)smfinf 41539  smfinflem 41538  smfinfmpt 41540
[Fremlin1] p. 39Remark 121Gsmflim 41500  smflim2 41527  smflimmpt 41531
[Fremlin1] p. 39Proposition 121Fsmfpimcc 41529
[Fremlin1] p. 39Proposition 121F (d)smflimsup 41549  smflimsuplem2 41542  smflimsuplem6 41546  smflimsuplem7 41547  smflimsuplem8 41548  smflimsupmpt 41550
[Fremlin1] p. 39Proposition 121F (e)smfliminf 41552  smfliminflem 41551  smfliminfmpt 41553
[Fremlin1] p. 80Definition 135E (b)df-smblfn 41425
[Fremlin5] p. 193Proposition 563Gbnulmbl2 23524
[Fremlin5] p. 213Lemma 565Cauniioovol 23567
[Fremlin5] p. 214Lemma 565Cauniioombl 23577
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 33821
[Fremlin5] p. 220Theorem 565Maftc1anc 33824
[FreydScedrov] p. 283Axiom of Infinityax-inf 8703  inf1 8687  inf2 8688
[Gleason] p. 117Proposition 9-2.1df-enq 9939  enqer 9949
[Gleason] p. 117Proposition 9-2.2df-1nq 9944  df-nq 9940
[Gleason] p. 117Proposition 9-2.3df-plpq 9936  df-plq 9942
[Gleason] p. 119Proposition 9-2.4caovmo 7022  df-mpq 9937  df-mq 9943
[Gleason] p. 119Proposition 9-2.5df-rq 9945
[Gleason] p. 119Proposition 9-2.6ltexnq 10003
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10004  ltbtwnnq 10006
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 9999
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10000
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10007
[Gleason] p. 121Definition 9-3.1df-np 10009
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10021
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10023
[Gleason] p. 122Definitiondf-1p 10010
[Gleason] p. 122Remark (1)prub 10022
[Gleason] p. 122Lemma 9-3.4prlem934 10061
[Gleason] p. 122Proposition 9-3.2df-ltp 10013
[Gleason] p. 122Proposition 9-3.3ltsopr 10060  psslinpr 10059  supexpr 10082  suplem1pr 10080  suplem2pr 10081
[Gleason] p. 123Proposition 9-3.5addclpr 10046  addclprlem1 10044  addclprlem2 10045  df-plp 10011
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10050
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10049
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10062
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10071  ltexprlem1 10064  ltexprlem2 10065  ltexprlem3 10066  ltexprlem4 10067  ltexprlem5 10068  ltexprlem6 10069  ltexprlem7 10070
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10073  ltaprlem 10072
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10074
[Gleason] p. 124Lemma 9-3.6prlem936 10075
[Gleason] p. 124Proposition 9-3.7df-mp 10012  mulclpr 10048  mulclprlem 10047  reclem2pr 10076
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10057
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10052
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10051
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10056
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10079  reclem3pr 10077  reclem4pr 10078
[Gleason] p. 126Proposition 9-4.1df-enr 10083  enrer 10092
[Gleason] p. 126Proposition 9-4.2df-0r 10088  df-1r 10089  df-nr 10084
[Gleason] p. 126Proposition 9-4.3df-mr 10086  df-plr 10085  negexsr 10129  recexsr 10134  recexsrlem 10130
[Gleason] p. 127Proposition 9-4.4df-ltr 10087
[Gleason] p. 130Proposition 10-1.3creui 11221  creur 11220  cru 11218
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 10215  axcnre 10191
[Gleason] p. 132Definition 10-3.1crim 14063  crimd 14180  crimi 14141  crre 14062  crred 14179  crrei 14140
[Gleason] p. 132Definition 10-3.2remim 14065  remimd 14146
[Gleason] p. 133Definition 10.36absval2 14232  absval2d 14392  absval2i 14344
[Gleason] p. 133Proposition 10-3.4(a)cjadd 14089  cjaddd 14168  cjaddi 14136
[Gleason] p. 133Proposition 10-3.4(c)cjmul 14090  cjmuld 14169  cjmuli 14137
[Gleason] p. 133Proposition 10-3.4(e)cjcj 14088  cjcjd 14147  cjcji 14119
[Gleason] p. 133Proposition 10-3.4(f)cjre 14087  cjreb 14071  cjrebd 14150  cjrebi 14122  cjred 14174  rere 14070  rereb 14068  rerebd 14149  rerebi 14121  rered 14172
[Gleason] p. 133Proposition 10-3.4(h)addcj 14096  addcjd 14160  addcji 14131
[Gleason] p. 133Proposition 10-3.7(a)absval 14186
[Gleason] p. 133Proposition 10-3.7(b)abscj 14227  abscjd 14397  abscji 14348
[Gleason] p. 133Proposition 10-3.7(c)abs00 14237  abs00d 14393  abs00i 14345  absne0d 14394
[Gleason] p. 133Proposition 10-3.7(d)releabs 14269  releabsd 14398  releabsi 14349
[Gleason] p. 133Proposition 10-3.7(f)absmul 14242  absmuld 14401  absmuli 14351
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 14230  sqabsaddi 14352
[Gleason] p. 133Proposition 10-3.7(h)abstri 14278  abstrid 14403  abstrii 14355
[Gleason] p. 134Definition 10-4.10exp0e1 13072  df-exp 13068  exp0 13071  expp1 13074  expp1d 13216
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 24646  cxpaddd 24684  expadd 13109  expaddd 13217  expaddz 13111
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 24655  cxpmuld 24701  expmul 13112  expmuld 13218  expmulz 13113
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 24652  mulcxpd 24695  mulexp 13106  mulexpd 13230  mulexpz 13107
[Gleason] p. 140Exercise 1znnen 15147
[Gleason] p. 141Definition 11-2.1fzval 12535
[Gleason] p. 168Proposition 12-2.1(a)climadd 14570  rlimadd 14581  rlimdiv 14584
[Gleason] p. 168Proposition 12-2.1(b)climsub 14572  rlimsub 14582
[Gleason] p. 168Proposition 12-2.1(c)climmul 14571  rlimmul 14583
[Gleason] p. 171Corollary 12-2.2climmulc2 14575
[Gleason] p. 172Corollary 12-2.5climrecl 14522
[Gleason] p. 172Proposition 12-2.4(c)climabs 14542  climcj 14543  climim 14545  climre 14544  rlimabs 14547  rlimcj 14548  rlimim 14550  rlimre 14549
[Gleason] p. 173Definition 12-3.1df-ltxr 10285  df-xr 10284  ltxr 12154
[Gleason] p. 175Definition 12-4.1df-limsup 14410  limsupval 14413
[Gleason] p. 180Theorem 12-5.1climsup 14608
[Gleason] p. 180Theorem 12-5.3caucvg 14617  caucvgb 14618  caucvgr 14614  climcau 14609
[Gleason] p. 182Exercise 3cvgcmp 14755
[Gleason] p. 182Exercise 4cvgrat 14822
[Gleason] p. 195Theorem 13-2.12abs1m 14283
[Gleason] p. 217Lemma 13-4.1btwnzge0 12837
[Gleason] p. 223Definition 14-1.1df-met 19955
[Gleason] p. 223Definition 14-1.1(a)met0 22368  xmet0 22367
[Gleason] p. 223Definition 14-1.1(b)metgt0 22384
[Gleason] p. 223Definition 14-1.1(c)metsym 22375
[Gleason] p. 223Definition 14-1.1(d)mettri 22377  mstri 22494  xmettri 22376  xmstri 22493
[Gleason] p. 225Definition 14-1.5xpsmet 22407
[Gleason] p. 230Proposition 14-2.6txlm 21672
[Gleason] p. 240Theorem 14-4.3metcnp4 23327
[Gleason] p. 240Proposition 14-4.2metcnp3 22565
[Gleason] p. 243Proposition 14-4.16addcn 22888  addcn2 14532  mulcn 22890  mulcn2 14534  subcn 22889  subcn2 14533
[Gleason] p. 295Remarkbcval3 13297  bcval4 13298
[Gleason] p. 295Equation 2bcpasc 13312
[Gleason] p. 295Definition of binomial coefficientbcval 13295  df-bc 13294
[Gleason] p. 296Remarkbcn0 13301  bcnn 13303
[Gleason] p. 296Theorem 15-2.8binom 14769
[Gleason] p. 308Equation 2ef0 15027
[Gleason] p. 308Equation 3efcj 15028
[Gleason] p. 309Corollary 15-4.3efne0 15033
[Gleason] p. 309Corollary 15-4.4efexp 15037
[Gleason] p. 310Equation 14sinadd 15100
[Gleason] p. 310Equation 15cosadd 15101
[Gleason] p. 311Equation 17sincossq 15112
[Gleason] p. 311Equation 18cosbnd 15117  sinbnd 15116
[Gleason] p. 311Lemma 15-4.7sqeqor 13185  sqeqori 13183
[Gleason] p. 311Definition of pidf-pi 15009
[Godowski] p. 730Equation SFgoeqi 29472
[GodowskiGreechie] p. 249Equation IV3oai 28867
[Golan] p. 1Remarksrgisid 18736
[Golan] p. 1Definitiondf-srg 18714
[Golan] p. 149Definitiondf-slmd 30094
[GramKnuthPat], p. 47Definition 2.42df-fwddif 32603
[Gratzer] p. 23Section 0.6df-mre 16454
[Gratzer] p. 27Section 0.6df-mri 16456
[Hall] p. 1Section 1.1df-asslaw 42347  df-cllaw 42345  df-comlaw 42346
[Hall] p. 2Section 1.2df-clintop 42359
[Hall] p. 7Section 1.3df-sgrp2 42380
[Halmos] p. 31Theorem 17.3riesz1 29264  riesz2 29265
[Halmos] p. 41Definition of Hermitianhmopadj2 29140
[Halmos] p. 42Definition of projector orderingpjordi 29372
[Halmos] p. 43Theorem 26.1elpjhmop 29384  elpjidm 29383  pjnmopi 29347
[Halmos] p. 44Remarkpjinormi 28886  pjinormii 28875
[Halmos] p. 44Theorem 26.2elpjch 29388  pjrn 28906  pjrni 28901  pjvec 28895
[Halmos] p. 44Theorem 26.3pjnorm2 28926
[Halmos] p. 44Theorem 26.4hmopidmpj 29353  hmopidmpji 29351
[Halmos] p. 45Theorem 27.1pjinvari 29390
[Halmos] p. 45Theorem 27.3pjoci 29379  pjocvec 28896
[Halmos] p. 45Theorem 27.4pjorthcoi 29368
[Halmos] p. 48Theorem 29.2pjssposi 29371
[Halmos] p. 48Theorem 29.3pjssdif1i 29374  pjssdif2i 29373
[Halmos] p. 50Definition of spectrumdf-spec 29054
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1870
[Hatcher] p. 25Definitiondf-phtpc 23011  df-phtpy 22990
[Hatcher] p. 26Definitiondf-pco 23024  df-pi1 23027
[Hatcher] p. 26Proposition 1.2phtpcer 23014
[Hatcher] p. 26Proposition 1.3pi1grp 23069
[Hefferon] p. 240Definition 3.12df-dmat 20514  df-dmatalt 42710
[Helfgott] p. 2Theoremtgoldbach 42228
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 42213
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 42225  bgoldbtbnd 42220  bgoldbtbnd 42220  tgblthelfgott 42226
[Helfgott] p. 5Proposition 1.1circlevma 31060
[Helfgott] p. 69Statement 7.49circlemethhgt 31061
[Helfgott] p. 69Statement 7.50hgt750lema 31075  hgt750lemb 31074  hgt750leme 31076  hgt750lemf 31071  hgt750lemg 31072
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 42222  tgoldbachgt 31081  tgoldbachgtALTV 42223  tgoldbachgtd 31080
[Helfgott] p. 70Statement 7.49ax-hgt749 31062
[Herstein] p. 54Exercise 28df-grpo 27687
[Herstein] p. 55Lemma 2.2.1(a)grpideu 17641  grpoideu 27703  mndideu 17512
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 17664  grpoinveu 27713
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 17690  grpo2inv 27725
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 17701  grpoinvop 27727
[Herstein] p. 57Exercise 1dfgrp3e 17723
[Hitchcock] p. 5Rule A3mptnan 1841
[Hitchcock] p. 5Rule A4mptxor 1842
[Hitchcock] p. 5Rule A5mtpxor 1844
[Holland] p. 1519Theorem 2sumdmdi 29619
[Holland] p. 1520Lemma 5cdj1i 29632  cdj3i 29640  cdj3lem1 29633  cdjreui 29631
[Holland] p. 1524Lemma 7mddmdin0i 29630
[Holland95] p. 13Theorem 3.6hlathil 37769
[Holland95] p. 14Line 15hgmapvs 37699
[Holland95] p. 14Line 16hdmaplkr 37721
[Holland95] p. 14Line 17hdmapellkr 37722
[Holland95] p. 14Line 19hdmapglnm2 37719
[Holland95] p. 14Line 20hdmapip0com 37725
[Holland95] p. 14Theorem 3.6hdmapevec2 37644
[Holland95] p. 14Lines 24 and 25hdmapoc 37739
[Holland95] p. 204Definition of involutiondf-srng 19056
[Holland95] p. 212Definition of subspacedf-psubsp 35310
[Holland95] p. 214Lemma 3.3lclkrlem2v 37336
[Holland95] p. 214Definition 3.2df-lpolN 37289
[Holland95] p. 214Definition of nonsingularpnonsingN 35740
[Holland95] p. 215Lemma 3.3(1)dihoml4 37185  poml4N 35760
[Holland95] p. 215Lemma 3.3(2)dochexmid 37276  pexmidALTN 35785  pexmidN 35776
[Holland95] p. 218Theorem 3.6lclkr 37341
[Holland95] p. 218Definition of dual vector spacedf-ldual 34931  ldualset 34932
[Holland95] p. 222Item 1df-lines 35308  df-pointsN 35309
[Holland95] p. 222Item 2df-polarityN 35710
[Holland95] p. 223Remarkispsubcl2N 35754  omllaw4 35053  pol1N 35717  polcon3N 35724
[Holland95] p. 223Definitiondf-psubclN 35742
[Holland95] p. 223Equation for polaritypolval2N 35713
[Holmes] p. 40Definitiondf-xrn 34473
[Hughes] p. 44Equation 1.21bax-his3 28281
[Hughes] p. 47Definition of projection operatordfpjop 29381
[Hughes] p. 49Equation 1.30eighmre 29162  eigre 29034  eigrei 29033
[Hughes] p. 49Equation 1.31eighmorth 29163  eigorth 29037  eigorthi 29036
[Hughes] p. 137Remark (ii)eigposi 29035
[Huneke] p. 1Claim 1frgrncvvdeq 27491
[Huneke] p. 1Statement 1frgrncvvdeqlem7 27487
[Huneke] p. 1Statement 2frgrncvvdeqlem8 27488
[Huneke] p. 1Statement 3frgrncvvdeqlem9 27489
[Huneke] p. 2Claim 2frgrregorufr 27507  frgrregorufr0 27506  frgrregorufrg 27508
[Huneke] p. 2Claim 3frgrhash2wsp 27514  frrusgrord 27523  frrusgrord0 27522
[Huneke] p. 2Statementdf-clwwlknon 27260
[Huneke] p. 2Statement 4frgrwopreglem4 27497
[Huneke] p. 2Statement 5frgrwopreg1 27500  frgrwopreg2 27501  frgrwopregasn 27498  frgrwopregbsn 27499
[Huneke] p. 2Statement 6frgrwopreglem5 27503
[Huneke] p. 2Statement 7fusgreghash2wspv 27517
[Huneke] p. 2Statement 8fusgreghash2wsp 27520
[Huneke] p. 2Statement 9clwlksndivn 27258  numclwlk1 27562  numclwlk1lem1 27560  numclwlk1lem2 27561  numclwwlk1 27548  numclwwlk8 27591
[Huneke] p. 2Definition 3frgrwopreglem1 27494
[Huneke] p. 2Definition 4df-clwlks 26902
[Huneke] p. 2Definition 62clwwlk 27531
[Huneke] p. 2Definition 7numclwwlkovh 27564  numclwwlkovh0 27563
[Huneke] p. 2Statement 10numclwwlk2 27572
[Huneke] p. 2Statement 11rusgrnumwlkg 27126
[Huneke] p. 2Statement 12numclwwlk3 27584
[Huneke] p. 2Statement 13numclwwlk5 27587
[Huneke] p. 2Statement 14numclwwlk7 27590
[Indrzejczak] p. 33Definition ` `Enatded 27602  natded 27602
[Indrzejczak] p. 33Definition ` `Inatded 27602
[Indrzejczak] p. 34Definition ` `Enatded 27602  natded 27602
[Indrzejczak] p. 34Definition ` `Inatded 27602
[Jech] p. 4Definition of classcv 1630  cvjust 2766
[Jech] p. 42Lemma 6.1alephexp1 9607
[Jech] p. 42Equation 6.1alephadd 9605  alephmul 9606
[Jech] p. 43Lemma 6.2infmap 9604  infmap2 9246
[Jech] p. 71Lemma 9.3jech9.3 8845
[Jech] p. 72Equation 9.3scott0 8917  scottex 8916
[Jech] p. 72Exercise 9.1rankval4 8898
[Jech] p. 72Scheme "Collection Principle"cp 8922
[Jech] p. 78Noteopthprc 5306
[JonesMatijasevic] p. 694Definition 2.3rmxyval 38004
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 38094
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 38095
[JonesMatijasevic] p. 695Equation 2.7rmxadd 38016
[JonesMatijasevic] p. 695Equation 2.8rmyadd 38020
[JonesMatijasevic] p. 695Equation 2.9rmxp1 38021  rmyp1 38022
[JonesMatijasevic] p. 695Equation 2.10rmxm1 38023  rmym1 38024
[JonesMatijasevic] p. 695Equation 2.11rmx0 38014  rmx1 38015  rmxluc 38025
[JonesMatijasevic] p. 695Equation 2.12rmy0 38018  rmy1 38019  rmyluc 38026
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 38028
[JonesMatijasevic] p. 695Equation 2.14rmydbl 38029
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 38051  jm2.17b 38052  jm2.17c 38053
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 38084
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 38088
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 38079
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 38054  jm2.24nn 38050
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 38093
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 38099  rmygeid 38055
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 38111
[Juillerat] p. 11Section *5etransc 41012  etransclem47 41010  etransclem48 41011
[Juillerat] p. 12Equation (7)etransclem44 41007
[Juillerat] p. 12Equation *(7)etransclem46 41009
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 40995
[Juillerat] p. 13Proofetransclem35 40998
[Juillerat] p. 13Part of case 2 proven inetransclem38 41001
[Juillerat] p. 13Part of case 2 provenetransclem24 40987
[Juillerat] p. 13Part of case 2: proven inetransclem41 41004
[Juillerat] p. 14Proofetransclem23 40986
[KalishMontague] p. 81Note 1ax-6 2057
[KalishMontague] p. 85Lemma 2equid 2097
[KalishMontague] p. 85Lemma 3equcomi 2102
[KalishMontague] p. 86Lemma 7cbvalivw 2092  cbvaliw 2091
[KalishMontague] p. 87Lemma 8spimvw 2085  spimw 2084
[KalishMontague] p. 87Lemma 9spfw 2121  spw 2123
[Kalmbach] p. 14Definition of latticechabs1 28715  chabs1i 28717  chabs2 28716  chabs2i 28718  chjass 28732  chjassi 28685  latabs1 17295  latabs2 17296
[Kalmbach] p. 15Definition of atomdf-at 29537  ela 29538
[Kalmbach] p. 15Definition of coverscvbr2 29482  cvrval2 35081
[Kalmbach] p. 16Definitiondf-ol 34985  df-oml 34986
[Kalmbach] p. 20Definition of commutescmbr 28783  cmbri 28789  cmtvalN 35018  df-cm 28782  df-cmtN 34984
[Kalmbach] p. 22Remarkomllaw5N 35054  pjoml5 28812  pjoml5i 28787
[Kalmbach] p. 22Definitionpjoml2 28810  pjoml2i 28784
[Kalmbach] p. 22Theorem 2(v)cmcm 28813  cmcmi 28791  cmcmii 28796  cmtcomN 35056
[Kalmbach] p. 22Theorem 2(ii)omllaw3 35052  omlsi 28603  pjoml 28635  pjomli 28634
[Kalmbach] p. 22Definition of OML lawomllaw2N 35051
[Kalmbach] p. 23Remarkcmbr2i 28795  cmcm3 28814  cmcm3i 28793  cmcm3ii 28798  cmcm4i 28794  cmt3N 35058  cmt4N 35059  cmtbr2N 35060
[Kalmbach] p. 23Lemma 3cmbr3 28807  cmbr3i 28799  cmtbr3N 35061
[Kalmbach] p. 25Theorem 5fh1 28817  fh1i 28820  fh2 28818  fh2i 28821  omlfh1N 35065
[Kalmbach] p. 65Remarkchjatom 29556  chslej 28697  chsleji 28657  shslej 28579  shsleji 28569
[Kalmbach] p. 65Proposition 1chocin 28694  chocini 28653  chsupcl 28539  chsupval2 28609  h0elch 28452  helch 28440  hsupval2 28608  ocin 28495  ococss 28492  shococss 28493
[Kalmbach] p. 65Definition of subspace sumshsval 28511
[Kalmbach] p. 66Remarkdf-pjh 28594  pjssmi 29364  pjssmii 28880
[Kalmbach] p. 67Lemma 3osum 28844  osumi 28841
[Kalmbach] p. 67Lemma 4pjci 29399
[Kalmbach] p. 103Exercise 6atmd2 29599
[Kalmbach] p. 103Exercise 12mdsl0 29509
[Kalmbach] p. 140Remarkhatomic 29559  hatomici 29558  hatomistici 29561
[Kalmbach] p. 140Proposition 1atlatmstc 35126
[Kalmbach] p. 140Proposition 1(i)atexch 29580  lsatexch 34850
[Kalmbach] p. 140Proposition 1(ii)chcv1 29554  cvlcvr1 35146  cvr1 35217
[Kalmbach] p. 140Proposition 1(iii)cvexch 29573  cvexchi 29568  cvrexch 35227
[Kalmbach] p. 149Remark 2chrelati 29563  hlrelat 35209  hlrelat5N 35208  lrelat 34821
[Kalmbach] p. 153Exercise 5lsmcv 19355  lsmsatcv 34817  spansncv 28852  spansncvi 28851
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 34836  spansncv2 29492
[Kalmbach] p. 266Definitiondf-st 29410
[Kalmbach2] p. 8Definition of adjointdf-adjh 29048
[KanamoriPincus] p. 415Theorem 1.1fpwwe 9674  fpwwe2 9671
[KanamoriPincus] p. 416Corollary 1.3canth4 9675
[KanamoriPincus] p. 417Corollary 1.6canthp1 9682
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 9677
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 9679
[KanamoriPincus] p. 418Proposition 1.7pwfseq 9692
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 9696  gchxpidm 9697
[KanamoriPincus] p. 419Theorem 2.1gchacg 9708  gchhar 9707
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 9244  unxpwdom 8654
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 9698
[Kreyszig] p. 3Property M1metcl 22357  xmetcl 22356
[Kreyszig] p. 4Property M2meteq0 22364
[Kreyszig] p. 8Definition 1.1-8dscmet 22597
[Kreyszig] p. 12Equation 5conjmul 10948  muleqadd 10877
[Kreyszig] p. 18Definition 1.3-2mopnval 22463
[Kreyszig] p. 19Remarkmopntopon 22464
[Kreyszig] p. 19Theorem T1mopn0 22523  mopnm 22469
[Kreyszig] p. 19Theorem T2unimopn 22521
[Kreyszig] p. 19Definition of neighborhoodneibl 22526
[Kreyszig] p. 20Definition 1.3-3metcnp2 22567
[Kreyszig] p. 25Definition 1.4-1lmbr 21283  lmmbr 23275  lmmbr2 23276
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 21405
[Kreyszig] p. 28Theorem 1.4-5lmcau 23330
[Kreyszig] p. 28Definition 1.4-3iscau 23293  iscmet2 23311
[Kreyszig] p. 30Theorem 1.4-7cmetss 23332
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 21485  metelcls 23322
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 23323  metcld2 23324
[Kreyszig] p. 51Equation 2clmvneg1 23118  lmodvneg1 19116  nvinv 27834  vcm 27771
[Kreyszig] p. 51Equation 1aclm0vs 23114  lmod0vs 19106  slmd0vs 30117  vc0 27769
[Kreyszig] p. 51Equation 1blmodvs0 19107  slmdvs0 30118  vcz 27770
[Kreyszig] p. 58Definition 2.2-1imsmet 27886  ngpmet 22627  nrmmetd 22599
[Kreyszig] p. 59Equation 1imsdval 27881  imsdval2 27882  ncvspds 23180  ngpds 22628
[Kreyszig] p. 63Problem 1nmval 22614  nvnd 27883
[Kreyszig] p. 64Problem 2nmeq0 22642  nmge0 22641  nvge0 27868  nvz 27864
[Kreyszig] p. 64Problem 3nmrtri 22648  nvabs 27867
[Kreyszig] p. 91Definition 2.7-1isblo3i 27996
[Kreyszig] p. 92Equation 2df-nmoo 27940
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 28002  blocni 28000
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 28001
[Kreyszig] p. 129Definition 3.1-1cphipeq0 23223  ipeq0 20200  ipz 27914
[Kreyszig] p. 135Problem 2pythi 28045
[Kreyszig] p. 137Lemma 3-2.1(a)sii 28049
[Kreyszig] p. 144Equation 4supcvg 14795
[Kreyszig] p. 144Theorem 3.3-1minvec 23426  minveco 28080
[Kreyszig] p. 196Definition 3.9-1df-aj 27945
[Kreyszig] p. 247Theorem 4.7-2bcth 23345
[Kreyszig] p. 249Theorem 4.7-3ubth 28069
[Kreyszig] p. 470Definition of positive operator orderingleop 29322  leopg 29321
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 29340
[Kreyszig] p. 525Theorem 10.1-1htth 28115
[Kulpa] p. 547Theorempoimir 33774
[Kulpa] p. 547Equation (1)poimirlem32 33773
[Kulpa] p. 547Equation (2)poimirlem31 33772
[Kulpa] p. 548Theorembroucube 33775
[Kulpa] p. 548Equation (6)poimirlem26 33767
[Kulpa] p. 548Equation (7)poimirlem27 33768
[Kunen] p. 10Axiom 0ax6e 2412  axnul 4923
[Kunen] p. 11Axiom 3axnul 4923
[Kunen] p. 12Axiom 6zfrep6 7285
[Kunen] p. 24Definition 10.24mapval 8025  mapvalg 8023
[Kunen] p. 30Lemma 10.20fodom 9550
[Kunen] p. 31Definition 10.24mapex 8019
[Kunen] p. 95Definition 2.1df-r1 8795
[Kunen] p. 97Lemma 2.10r1elss 8837  r1elssi 8836
[Kunen] p. 107Exercise 4rankop 8889  rankopb 8883  rankuni 8894  rankxplim 8910  rankxpsuc 8913
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4666
[Lang] p. 3Definitiondf-mnd 17503
[Lang] p. 7Definitiondfgrp2e 17656
[Lang] p. 53Definitiondf-cat 16536
[Lang] p. 54Definitiondf-iso 16616
[Lang] p. 57Definitiondf-inito 16848  df-termo 16849
[Lang] p. 58Exampleirinitoringc 42592
[Lang] p. 58Statementinitoeu1 16868  termoeu1 16875
[Lang] p. 62Definitiondf-func 16725
[Lang] p. 65Definitiondf-nat 16810
[Lang] p. 91Notedf-ringc 42528
[Lang] p. 128Remarkdsmmlmod 20306
[Lang] p. 129Prooflincscm 42742  lincscmcl 42744  lincsum 42741  lincsumcl 42743
[Lang] p. 129Statementlincolss 42746
[Lang] p. 129Observationdsmmfi 20299
[Lang] p. 147Definitionsnlindsntor 42783
[Lang] p. 504Statementmat1 20471  matring 20466
[Lang] p. 504Definitiondf-mamu 20407
[Lang] p. 505Statementmamuass 20425  mamutpos 20482  matassa 20467  mattposvs 20479  tposmap 20481
[Lang] p. 513Definitionmdet1 20625  mdetf 20619
[Lang] p. 513Theorem 4.4cramer 20717
[Lang] p. 514Proposition 4.6mdetleib 20611
[Lang] p. 514Proposition 4.8mdettpos 20635
[Lang] p. 515Definitiondf-minmar1 20659  smadiadetr 20700
[Lang] p. 515Corollary 4.9mdetero 20634  mdetralt 20632
[Lang] p. 517Proposition 4.15mdetmul 20647
[Lang] p. 518Definitiondf-madu 20658
[Lang] p. 518Proposition 4.16madulid 20669  madurid 20668  matinv 20702
[Lang] p. 561Theorem 3.1cayleyhamilton 20915
[Lang], p. 561Remarkchpmatply1 20857
[Lang], p. 561Definitiondf-chpmat 20852
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 39057
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 39052
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 39058
[LeBlanc] p. 277Rule R2axnul 4923
[Levy] p. 338Axiomdf-clab 2758  df-clel 2767  df-cleq 2764
[Levy58] p. 2Definition Iisfin1-3 9414
[Levy58] p. 2Definition IIdf-fin2 9314
[Levy58] p. 2Definition Iadf-fin1a 9313
[Levy58] p. 2Definition IIIdf-fin3 9316
[Levy58] p. 3Definition Vdf-fin5 9317
[Levy58] p. 3Definition IVdf-fin4 9315
[Levy58] p. 4Definition VIdf-fin6 9318
[Levy58] p. 4Definition VIIdf-fin7 9319
[Levy58], p. 3Theorem 1fin1a2 9443
[Lipparini] p. 3Lemma 2.1.1nosepssdm 32173
[Lipparini] p. 3Lemma 2.1.4noresle 32183
[Lipparini] p. 6Proposition 4.2nosupbnd1 32197
[Lipparini] p. 6Proposition 4.3nosupbnd2 32199
[Lipparini] p. 7Theorem 5.1noetalem2 32201  noetalem3 32202
[Lopez-Astorga] p. 12Rule 1mptnan 1841
[Lopez-Astorga] p. 12Rule 2mptxor 1842
[Lopez-Astorga] p. 12Rule 3mtpxor 1844
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 29607
[Maeda] p. 168Lemma 5mdsym 29611  mdsymi 29610
[Maeda] p. 168Lemma 4(i)mdsymlem4 29605  mdsymlem6 29607  mdsymlem7 29608
[Maeda] p. 168Lemma 4(ii)mdsymlem8 29609
[MaedaMaeda] p. 1Remarkssdmd1 29512  ssdmd2 29513  ssmd1 29510  ssmd2 29511
[MaedaMaeda] p. 1Lemma 1.2mddmd2 29508
[MaedaMaeda] p. 1Definition 1.1df-dmd 29480  df-md 29479  mdbr 29493
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 29530  mdslj1i 29518  mdslj2i 29519  mdslle1i 29516  mdslle2i 29517  mdslmd1i 29528  mdslmd2i 29529
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 29520  mdsl2bi 29522  mdsl2i 29521
[MaedaMaeda] p. 2Lemma 1.6mdexchi 29534
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 29531
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 29532
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 29509
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 29514  mdsl3 29515
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 29533
[MaedaMaeda] p. 4Theorem 1.14mdcompli 29628
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 35128  hlrelat1 35207
[MaedaMaeda] p. 31Lemma 7.5lcvexch 34846
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 29535  cvmdi 29523  cvnbtwn4 29488  cvrnbtwn4 35086
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 29536
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 35147  cvp 29574  cvrp 35223  lcvp 34847
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 29598
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 29597
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 35140  hlexch4N 35199
[MaedaMaeda] p. 34Exercise 7.1atabsi 29600
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 35250
[MaedaMaeda] p. 61Definition 15.10psubN 35556  atpsubN 35560  df-pointsN 35309  pointpsubN 35558
[MaedaMaeda] p. 62Theorem 15.5df-pmap 35311  pmap11 35569  pmaple 35568  pmapsub 35575  pmapval 35564
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 35572  pmap1N 35574
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 35577  pmapglb2N 35578  pmapglb2xN 35579  pmapglbx 35576
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 35659
[MaedaMaeda] p. 67Postulate PS1ps-1 35284
[MaedaMaeda] p. 68Lemma 16.2df-padd 35603  paddclN 35649  paddidm 35648
[MaedaMaeda] p. 68Condition PS2ps-2 35285
[MaedaMaeda] p. 68Equation 16.2.1paddass 35645
[MaedaMaeda] p. 69Lemma 16.4ps-1 35284
[MaedaMaeda] p. 69Theorem 16.4ps-2 35285
[MaedaMaeda] p. 70Theorem 16.9lsmmod 18295  lsmmod2 18296  lssats 34819  shatomici 29557  shatomistici 29560  shmodi 28589  shmodsi 28588
[MaedaMaeda] p. 130Remark 29.6dmdmd 29499  mdsymlem7 29608
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 28788
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 28692
[MaedaMaeda] p. 139Remarksumdmdii 29614
[Margaris] p. 40Rule Cexlimiv 2010
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 383  df-ex 1853  df-or 837  dfbi2 460
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 27599
[Margaris] p. 59Section 14notnotrALTVD 39671
[Margaris] p. 60Theorem 8mth8 159
[Margaris] p. 60Section 14con3ALTVD 39672
[Margaris] p. 79Rule Cexinst01 39373  exinst11 39374
[Margaris] p. 89Theorem 19.219.2 2061  19.2g 2212  r19.2z 4202
[Margaris] p. 89Theorem 19.319.3 2224  rr19.3v 3496
[Margaris] p. 89Theorem 19.5alcom 2193
[Margaris] p. 89Theorem 19.6alex 1901
[Margaris] p. 89Theorem 19.7alnex 1854
[Margaris] p. 89Theorem 19.819.8a 2206
[Margaris] p. 89Theorem 19.919.9 2228  19.9h 2283  exlimd 2243  exlimdh 2314
[Margaris] p. 89Theorem 19.11excom 2198  excomim 2199
[Margaris] p. 89Theorem 19.1219.12 2326
[Margaris] p. 90Section 19conventions-label 27600  conventions-label 27600  conventions-label 27600  conventions-label 27600
[Margaris] p. 90Theorem 19.14exnal 1902
[Margaris] p. 90Theorem 19.152albi 39101  albi 1894
[Margaris] p. 90Theorem 19.1619.16 2249
[Margaris] p. 90Theorem 19.1719.17 2250
[Margaris] p. 90Theorem 19.182exbi 39103  exbi 1923
[Margaris] p. 90Theorem 19.1919.19 2253
[Margaris] p. 90Theorem 19.202alim 39100  2alimdv 1999  alimd 2237  alimdh 1893  alimdv 1997  ax-4 1885  ralimdaa 3107  ralimdv 3112  ralimdva 3111  ralimdvva 3113  sbcimdv 3649
[Margaris] p. 90Theorem 19.2119.21 2231  19.21h 2284  19.21t 2229  19.21vv 39099  alrimd 2240  alrimdd 2239  alrimdh 1941  alrimdv 2009  alrimi 2238  alrimih 1899  alrimiv 2007  alrimivv 2008  hbralrimi 3103  r19.21be 3082  r19.21bi 3081  ralrimd 3108  ralrimdv 3117  ralrimdva 3118  ralrimdvv 3122  ralrimdvva 3123  ralrimi 3106  ralrimia 39833  ralrimiv 3114  ralrimiva 3115  ralrimivv 3119  ralrimivva 3120  ralrimivvva 3121  ralrimivw 3116
[Margaris] p. 90Theorem 19.222exim 39102  2eximdv 2000  exim 1909  eximd 2241  eximdh 1942  eximdv 1998  rexim 3156  reximd2a 3161  reximdai 3160  reximdd 39861  reximddv 3166  reximddv2 3168  reximddv3 39860  reximdv 3164  reximdv2 3162  reximdva 3165  reximdvai 3163  reximdvva 3167  reximi2 3158
[Margaris] p. 90Theorem 19.2319.23 2236  19.23bi 2215  19.23h 2285  exlimdv 2013  exlimdvv 2014  exlimexi 39253  exlimiv 2010  exlimivv 2012  rexlimd3 39852  rexlimdv 3178  rexlimdv3a 3181  rexlimdva 3179  rexlimdva2 39856  rexlimdvaa 3180  rexlimdvv 3185  rexlimdvva 3186  rexlimdvw 3182  rexlimiv 3175  rexlimiva 3176  rexlimivv 3184
[Margaris] p. 90Theorem 19.2419.24 2069
[Margaris] p. 90Theorem 19.2519.25 1960
[Margaris] p. 90Theorem 19.2619.26 1949
[Margaris] p. 90Theorem 19.2719.27 2251  r19.27z 4212  r19.27zv 4213
[Margaris] p. 90Theorem 19.2819.28 2252  19.28vv 39109  r19.28z 4205  r19.28zv 4208  rr19.28v 3497
[Margaris] p. 90Theorem 19.2919.29 1953  r19.29d2r 3228  r19.29imd 3222
[Margaris] p. 90Theorem 19.3019.30 1961
[Margaris] p. 90Theorem 19.3119.31 2258  19.31vv 39107
[Margaris] p. 90Theorem 19.3219.32 2257  r19.32 41682
[Margaris] p. 90Theorem 19.3319.33-2 39105  19.33 1964
[Margaris] p. 90Theorem 19.3419.34 2070
[Margaris] p. 90Theorem 19.3519.35 1957
[Margaris] p. 90Theorem 19.3619.36 2254  19.36vv 39106  r19.36zv 4214
[Margaris] p. 90Theorem 19.3719.37 2256  19.37vv 39108  r19.37zv 4209
[Margaris] p. 90Theorem 19.3819.38 1914
[Margaris] p. 90Theorem 19.3919.39 2068
[Margaris] p. 90Theorem 19.4019.40-2 1966  19.40 1948  r19.40 3236
[Margaris] p. 90Theorem 19.4119.41 2259  19.41rg 39289
[Margaris] p. 90Theorem 19.4219.42 2261
[Margaris] p. 90Theorem 19.4319.43 1962
[Margaris] p. 90Theorem 19.4419.44 2262  r19.44zv 4211
[Margaris] p. 90Theorem 19.4519.45 2263  r19.45zv 4210
[Margaris] p. 90Theorem 1977.2319.23t 2235
[Margaris] p. 110Exercise 2(b)eu1 2659
[Mayet] p. 370Remarkjpi 29469  largei 29466  stri 29456
[Mayet3] p. 9Definition of CH-statesdf-hst 29411  ishst 29413
[Mayet3] p. 10Theoremhstrbi 29465  hstri 29464
[Mayet3] p. 1223Theorem 4.1mayete3i 28927
[Mayet3] p. 1240Theorem 7.1mayetes3i 28928
[MegPav2000] p. 2344Theorem 3.3stcltrthi 29477
[MegPav2000] p. 2345Definition 3.4-1chintcl 28531  chsupcl 28539
[MegPav2000] p. 2345Definition 3.4-2hatomic 29559
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 29553
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 29580
[MegPav2000] p. 2366Figure 7pl42N 35790
[MegPav2002] p. 362Lemma 2.2latj31 17307  latj32 17305  latjass 17303
[Megill] p. 444Axiom C5ax-5 1991  ax5ALT 34713
[Megill] p. 444Section 7conventions 27599
[Megill] p. 445Lemma L12aecom-o 34707  ax-c11n 34694  axc11n 2462
[Megill] p. 446Lemma L17equtrr 2107
[Megill] p. 446Lemma L18ax6fromc10 34702
[Megill] p. 446Lemma L19hbnae-o 34734  hbnae 2469
[Megill] p. 447Remark 9.1df-sb 2050  sbid 2270  sbidd-misc 42986  sbidd 42985
[Megill] p. 448Remark 9.6axc14 2519
[Megill] p. 448Scheme C4'ax-c4 34690
[Megill] p. 448Scheme C5'ax-c5 34689  sp 2207
[Megill] p. 448Scheme C6'ax-11 2190
[Megill] p. 448Scheme C7'ax-c7 34691
[Megill] p. 448Scheme C8'ax-7 2093
[Megill] p. 448Scheme C9'ax-c9 34696
[Megill] p. 448Scheme C10'ax-6 2057  ax-c10 34692
[Megill] p. 448Scheme C11'ax-c11 34693
[Megill] p. 448Scheme C12'ax-8 2147
[Megill] p. 448Scheme C13'ax-9 2154
[Megill] p. 448Scheme C14'ax-c14 34697
[Megill] p. 448Scheme C15'ax-c15 34695
[Megill] p. 448Scheme C16'ax-c16 34698
[Megill] p. 448Theorem 9.4dral1-o 34710  dral1 2475  dral2-o 34736  dral2 2474  drex1 2477  drex2 2478  drsb1 2524  drsb2 2525
[Megill] p. 449Theorem 9.7sbcom2 2593  sbequ 2523  sbid2v 2605
[Megill] p. 450Example in Appendixhba1-o 34703  hba1 2315
[Mendelson] p. 35Axiom A3hirstL-ax3 41574
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3667  rspsbca 3668  stdpc4 2499
[Mendelson] p. 69Axiom 5ax-c4 34690  ra4 3674  stdpc5 2232
[Mendelson] p. 81Rule Cexlimiv 2010
[Mendelson] p. 95Axiom 6stdpc6 2113
[Mendelson] p. 95Axiom 7stdpc7 2114
[Mendelson] p. 225Axiom system NBGru 3586
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5108
[Mendelson] p. 231Exercise 4.10(k)inv1 4115
[Mendelson] p. 231Exercise 4.10(l)unv 4116
[Mendelson] p. 231Exercise 4.10(n)dfin3 4015
[Mendelson] p. 231Exercise 4.10(o)df-nul 4064
[Mendelson] p. 231Exercise 4.10(q)dfin4 4016
[Mendelson] p. 231Exercise 4.10(s)ddif 3893
[Mendelson] p. 231Definition of uniondfun3 4014
[Mendelson] p. 235Exercise 4.12(c)univ 5048
[Mendelson] p. 235Exercise 4.12(d)pwv 4572
[Mendelson] p. 235Exercise 4.12(j)pwin 5152
[Mendelson] p. 235Exercise 4.12(k)pwunss 5153
[Mendelson] p. 235Exercise 4.12(l)pwssun 5154
[Mendelson] p. 235Exercise 4.12(n)uniin 4595
[Mendelson] p. 235Exercise 4.12(p)reli 5387
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5799
[Mendelson] p. 244Proposition 4.8(g)epweon 7134
[Mendelson] p. 246Definition of successordf-suc 5871
[Mendelson] p. 250Exercise 4.36oelim2 7833
[Mendelson] p. 254Proposition 4.22(b)xpen 8283
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8204  xpsneng 8205
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8211  xpcomeng 8212
[Mendelson] p. 254Proposition 4.22(e)xpassen 8214
[Mendelson] p. 255Definitionbrsdom 8136
[Mendelson] p. 255Exercise 4.39endisj 8207
[Mendelson] p. 255Exercise 4.41mapprc 8017
[Mendelson] p. 255Exercise 4.43mapsnen 8193  mapsnend 8192
[Mendelson] p. 255Exercise 4.45mapunen 8289
[Mendelson] p. 255Exercise 4.47xpmapen 8288
[Mendelson] p. 255Exercise 4.42(a)map0e 8051
[Mendelson] p. 255Exercise 4.42(b)map1 8196
[Mendelson] p. 257Proposition 4.24(a)undom 8208
[Mendelson] p. 258Exercise 4.56(b)cdaen 9201
[Mendelson] p. 258Exercise 4.56(c)cdaassen 9210  cdacomen 9209
[Mendelson] p. 258Exercise 4.56(f)cdadom1 9214
[Mendelson] p. 258Exercise 4.56(g)xp2cda 9208
[Mendelson] p. 258Definition of cardinal sumcdaval 9198  df-cda 9196
[Mendelson] p. 266Proposition 4.34(a)oa1suc 7769
[Mendelson] p. 266Proposition 4.34(f)oaordex 7796
[Mendelson] p. 275Proposition 4.42(d)entri3 9587
[Mendelson] p. 281Definitiondf-r1 8795
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 8844
[Mendelson] p. 287Axiom system MKru 3586
[MertziosUnger] p. 152Definitiondf-frgr 27439
[MertziosUnger] p. 153Remark 1frgrconngr 27476
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 27478  vdgn1frgrv3 27479
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 27480
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 27473
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 27466  2pthfrgrrn 27464  2pthfrgrrn2 27465
[Mittelstaedt] p. 9Definitiondf-oc 28449
[Monk1] p. 22Remarkconventions 27599
[Monk1] p. 22Theorem 3.1conventions 27599
[Monk1] p. 26Theorem 2.8(vii)ssin 3983
[Monk1] p. 33Theorem 3.2(i)ssrel 5346  ssrelf 29765
[Monk1] p. 33Theorem 3.2(ii)eqrel 5348
[Monk1] p. 34Definition 3.3df-opab 4848
[Monk1] p. 36Theorem 3.7(i)coi1 5794  coi2 5795
[Monk1] p. 36Theorem 3.8(v)dm0 5476  rn0 5514
[Monk1] p. 36Theorem 3.7(ii)cnvi 5677
[Monk1] p. 37Theorem 3.13(i)relxp 5267
[Monk1] p. 37Theorem 3.13(x)dmxp 5481  rnxp 5704
[Monk1] p. 37Theorem 3.13(ii)0xp 5338  xp0 5692
[Monk1] p. 38Theorem 3.16(ii)ima0 5621
[Monk1] p. 38Theorem 3.16(viii)imai 5618
[Monk1] p. 39Theorem 3.17imaex 7255  imaexg 7254
[Monk1] p. 39Theorem 3.16(xi)imassrn 5617
[Monk1] p. 41Theorem 4.3(i)fnopfv 6496  funfvop 6474
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6382
[Monk1] p. 42Theorem 4.4(iii)fvelima 6392
[Monk1] p. 43Theorem 4.6funun 6074
[Monk1] p. 43Theorem 4.8(iv)dff13 6658  dff13f 6659
[Monk1] p. 46Theorem 4.15(v)funex 6629  funrnex 7284
[Monk1] p. 50Definition 5.4fniunfv 6651
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5762
[Monk1] p. 52Theorem 5.11(viii)ssint 4628
[Monk1] p. 52Definition 5.13 (i)1stval2 7336  df-1st 7319
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7337  df-2nd 7320
[Monk1] p. 112Theorem 15.17(v)ranksn 8885  ranksnb 8858
[Monk1] p. 112Theorem 15.17(iv)rankuni2 8886
[Monk1] p. 112Theorem 15.17(iii)rankun 8887  rankunb 8881
[Monk1] p. 113Theorem 15.18r1val3 8869
[Monk1] p. 113Definition 15.19df-r1 8795  r1val2 8868
[Monk1] p. 117Lemmazorn2 9534  zorn2g 9531
[Monk1] p. 133Theorem 18.11cardom 9016
[Monk1] p. 133Theorem 18.12canth3 9589
[Monk1] p. 133Theorem 18.14carduni 9011
[Monk2] p. 105Axiom C4ax-4 1885
[Monk2] p. 105Axiom C7ax-7 2093
[Monk2] p. 105Axiom C8ax-12 2203  ax-c15 34695  ax12v2 2205
[Monk2] p. 108Lemma 5ax-c4 34690
[Monk2] p. 109Lemma 12ax-11 2190
[Monk2] p. 109Lemma 15equvini 2492  equvinv 2115  eqvinop 5083
[Monk2] p. 113Axiom C5-1ax-5 1991  ax5ALT 34713
[Monk2] p. 113Axiom C5-2ax-10 2174
[Monk2] p. 113Axiom C5-3ax-11 2190
[Monk2] p. 114Lemma 21sp 2207
[Monk2] p. 114Lemma 22axc4 2294  hba1-o 34703  hba1 2315
[Monk2] p. 114Lemma 23nfia1 2186
[Monk2] p. 114Lemma 24nfa2 2196  nfra2 3095
[Moore] p. 53Part Idf-mre 16454
[Munkres] p. 77Example 2distop 21020  indistop 21027  indistopon 21026
[Munkres] p. 77Example 3fctop 21029  fctop2 21030
[Munkres] p. 77Example 4cctop 21031
[Munkres] p. 78Definition of basisdf-bases 20971  isbasis3g 20974
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 16312  tgval2 20981
[Munkres] p. 79Remarktgcl 20994
[Munkres] p. 80Lemma 2.1tgval3 20988
[Munkres] p. 80Lemma 2.2tgss2 21012  tgss3 21011
[Munkres] p. 81Lemma 2.3basgen 21013  basgen2 21014
[Munkres] p. 83Exercise 3topdifinf 33533  topdifinfeq 33534  topdifinffin 33532  topdifinfindis 33530
[Munkres] p. 89Definition of subspace topologyresttop 21185
[Munkres] p. 93Theorem 6.1(1)0cld 21063  topcld 21060
[Munkres] p. 93Theorem 6.1(2)iincld 21064
[Munkres] p. 93Theorem 6.1(3)uncld 21066
[Munkres] p. 94Definition of closureclsval 21062
[Munkres] p. 94Definition of interiorntrval 21061
[Munkres] p. 95Theorem 6.5(a)clsndisj 21100  elcls 21098
[Munkres] p. 95Theorem 6.5(b)elcls3 21108
[Munkres] p. 97Theorem 6.6clslp 21173  neindisj 21142
[Munkres] p. 97Corollary 6.7cldlp 21175
[Munkres] p. 97Definition of limit pointislp2 21170  lpval 21164
[Munkres] p. 98Definition of Hausdorff spacedf-haus 21340
[Munkres] p. 102Definition of continuous functiondf-cn 21252  iscn 21260  iscn2 21263
[Munkres] p. 107Theorem 7.2(g)cncnp 21305  cncnp2 21306  cncnpi 21303  df-cnp 21253  iscnp 21262  iscnp2 21264
[Munkres] p. 127Theorem 10.1metcn 22568
[Munkres] p. 128Theorem 10.3metcn4 23328
[Nathanson] p. 123Remarkreprgt 31039  reprinfz1 31040  reprlt 31037
[Nathanson] p. 123Definitiondf-repr 31027
[Nathanson] p. 123Chapter 5.1circlemethnat 31059
[Nathanson] p. 123Propositionbreprexp 31051  breprexpnat 31052  itgexpif 31024
[NielsenChuang] p. 195Equation 4.73unierri 29303
[OeSilva] p. 2042Section 2ax-bgbltosilva 42221
[Pfenning] p. 17Definition XMnatded 27602
[Pfenning] p. 17Definition NNCnatded 27602  notnotrd 130
[Pfenning] p. 17Definition ` `Cnatded 27602
[Pfenning] p. 18Rule"natded 27602
[Pfenning] p. 18Definition /\Inatded 27602
[Pfenning] p. 18Definition ` `Enatded 27602  natded 27602  natded 27602  natded 27602  natded 27602
[Pfenning] p. 18Definition ` `Inatded 27602  natded 27602  natded 27602  natded 27602  natded 27602
[Pfenning] p. 18Definition ` `ELnatded 27602
[Pfenning] p. 18Definition ` `ERnatded 27602
[Pfenning] p. 18Definition ` `Ea,unatded 27602
[Pfenning] p. 18Definition ` `IRnatded 27602
[Pfenning] p. 18Definition ` `Ianatded 27602
[Pfenning] p. 127Definition =Enatded 27602
[Pfenning] p. 127Definition =Inatded 27602
[Ponnusamy] p. 361Theorem 6.44cphip0l 23221  df-dip 27896  dip0l 27913  ip0l 20198
[Ponnusamy] p. 361Equation 6.45cphipval 23261  ipval 27898
[Ponnusamy] p. 362Equation I1dipcj 27909  ipcj 20196
[Ponnusamy] p. 362Equation I3cphdir 23224  dipdir 28037  ipdir 20201  ipdiri 28025
[Ponnusamy] p. 362Equation I4ipidsq 27905  nmsq 23213
[Ponnusamy] p. 362Equation 6.46ip0i 28020
[Ponnusamy] p. 362Equation 6.47ip1i 28022
[Ponnusamy] p. 362Equation 6.48ip2i 28023
[Ponnusamy] p. 363Equation I2cphass 23230  dipass 28040  ipass 20207  ipassi 28036
[Prugovecki] p. 186Definition of brabraval 29143  df-bra 29049
[Prugovecki] p. 376Equation 8.1df-kb 29050  kbval 29153
[PtakPulmannova] p. 66Proposition 3.2.17atomli 29581
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 35695
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 29595  atcvat4i 29596  cvrat3 35249  cvrat4 35250  lsatcvat3 34859
[PtakPulmannova] p. 68Definition 3.2.18cvbr 29481  cvrval 35076  df-cv 29478  df-lcv 34826  lspsncv0 19360
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 35707
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 35708
[Quine] p. 16Definition 2.1df-clab 2758  rabid 3264
[Quine] p. 17Definition 2.1''dfsb7 2603
[Quine] p. 18Definition 2.7df-cleq 2764
[Quine] p. 19Definition 2.9conventions 27599  df-v 3353
[Quine] p. 34Theorem 5.1abeq2 2881
[Quine] p. 35Theorem 5.2abid1 2893  abid2f 2940
[Quine] p. 40Theorem 6.1sb5 2273
[Quine] p. 40Theorem 6.2sb56 2271  sb6 2272
[Quine] p. 41Theorem 6.3df-clel 2767
[Quine] p. 41Theorem 6.4eqid 2771  eqid1 27665
[Quine] p. 41Theorem 6.5eqcom 2778
[Quine] p. 42Theorem 6.6df-sbc 3588
[Quine] p. 42Theorem 6.7dfsbcq 3589  dfsbcq2 3590
[Quine] p. 43Theorem 6.8vex 3354
[Quine] p. 43Theorem 6.9isset 3359
[Quine] p. 44Theorem 7.3spcgf 3439  spcgv 3444  spcimgf 3437
[Quine] p. 44Theorem 6.11spsbc 3600  spsbcd 3601
[Quine] p. 44Theorem 6.12elex 3364
[Quine] p. 44Theorem 6.13elab 3501  elabg 3502  elabgf 3499
[Quine] p. 44Theorem 6.14noel 4067
[Quine] p. 48Theorem 7.2snprc 4390
[Quine] p. 48Definition 7.1df-pr 4320  df-sn 4318
[Quine] p. 49Theorem 7.4snss 4452  snssg 4451
[Quine] p. 49Theorem 7.5prss 4487  prssg 4486
[Quine] p. 49Theorem 7.6prid1 4434  prid1g 4432  prid2 4435  prid2g 4433  snid 4348  snidg 4346
[Quine] p. 51Theorem 7.12snex 5037
[Quine] p. 51Theorem 7.13prex 5038
[Quine] p. 53Theorem 8.2unisn 4590  unisnALT 39682  unisng 4591
[Quine] p. 53Theorem 8.3uniun 4594
[Quine] p. 54Theorem 8.6elssuni 4604
[Quine] p. 54Theorem 8.7uni0 4602
[Quine] p. 56Theorem 8.17uniabio 6003
[Quine] p. 56Definition 8.18dfiota2 5994
[Quine] p. 57Theorem 8.19iotaval 6004
[Quine] p. 57Theorem 8.22iotanul 6008
[Quine] p. 58Theorem 8.23iotaex 6010
[Quine] p. 58Definition 9.1df-op 4324
[Quine] p. 61Theorem 9.5opabid 5116  opelopab 5131  opelopaba 5125  opelopabaf 5133  opelopabf 5134  opelopabg 5127  opelopabga 5122  opelopabgf 5129  oprabid 6826
[Quine] p. 64Definition 9.11df-xp 5256
[Quine] p. 64Definition 9.12df-cnv 5258
[Quine] p. 64Definition 9.15df-id 5158
[Quine] p. 65Theorem 10.3fun0 6093
[Quine] p. 65Theorem 10.4funi 6062
[Quine] p. 65Theorem 10.5funsn 6081  funsng 6079
[Quine] p. 65Definition 10.1df-fun 6032
[Quine] p. 65Definition 10.2args 5633  dffv4 6330
[Quine] p. 68Definition 10.11conventions 27599  df-fv 6038  fv2 6328
[Quine] p. 124Theorem 17.3nn0opth2 13263  nn0opth2i 13262  nn0opthi 13261  omopthi 7895
[Quine] p. 177Definition 25.2df-rdg 7663
[Quine] p. 232Equation icarddom 9582
[Quine] p. 284Axiom 39(vi)funimaex 6115  funimaexg 6114
[Quine] p. 331Axiom system NFru 3586
[ReedSimon] p. 36Definition (iii)ax-his3 28281
[ReedSimon] p. 63Exercise 4(a)df-dip 27896  polid 28356  polid2i 28354  polidi 28355
[ReedSimon] p. 63Exercise 4(b)df-ph 28008
[ReedSimon] p. 195Remarklnophm 29218  lnophmi 29217
[Retherford] p. 49Exercise 1(i)leopadd 29331
[Retherford] p. 49Exercise 1(ii)leopmul 29333  leopmuli 29332
[Retherford] p. 49Exercise 1(iv)leoptr 29336
[Retherford] p. 49Definition VI.1df-leop 29051  leoppos 29325
[Retherford] p. 49Exercise 1(iii)leoptri 29335
[Retherford] p. 49Definition of operator orderingleop3 29324
[Roman] p. 4Definitiondf-dmat 20514  df-dmatalt 42710
[Roman] p. 18Part Preliminariesdf-rng0 42398
[Roman] p. 19Part Preliminariesdf-ring 18757
[Roman] p. 46Theorem 1.6isldepslvec2 42797
[Roman] p. 112Noteisldepslvec2 42797  ldepsnlinc 42820  zlmodzxznm 42809
[Roman] p. 112Examplezlmodzxzequa 42808  zlmodzxzequap 42811  zlmodzxzldep 42816
[Roman] p. 170Theorem 7.8cayleyhamilton 20915
[Rosenlicht] p. 80Theoremheicant 33776
[Rosser] p. 281Definitiondf-op 4324
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 31063
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 31064
[Rotman] p. 28Remarkpgrpgt2nabl 42670  pmtr3ncom 18102
[Rotman] p. 31Theorem 3.4symggen2 18098
[Rotman] p. 42Theorem 3.15cayley 18041  cayleyth 18042
[Rudin] p. 164Equation 27efcan 15032
[Rudin] p. 164Equation 30efzval 15038
[Rudin] p. 167Equation 48absefi 15132
[Sanford] p. 39Remarkax-mp 5  mto 188
[Sanford] p. 39Rule 3mtpxor 1844
[Sanford] p. 39Rule 4mptxor 1842
[Sanford] p. 40Rule 1mptnan 1841
[Schechter] p. 51Definition of antisymmetryintasym 5651
[Schechter] p. 51Definition of irreflexivityintirr 5654
[Schechter] p. 51Definition of symmetrycnvsym 5650
[Schechter] p. 51Definition of transitivitycotr 5648
[Schechter] p. 78Definition of Moore collection of setsdf-mre 16454
[Schechter] p. 79Definition of Moore closuredf-mrc 16455
[Schechter] p. 82Section 4.5df-mrc 16455
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 16457
[Schechter] p. 139Definition AC3dfac9 9164
[Schechter] p. 141Definition (MC)dfac11 38156
[Schechter] p. 149Axiom DC1ax-dc 9474  axdc3 9482
[Schechter] p. 187Definition of ring with unitisring 18759  isrngo 34026
[Schechter] p. 276Remark 11.6.espan0 28741
[Schechter] p. 276Definition of spandf-span 28508  spanval 28532
[Schechter] p. 428Definition 15.35bastop1 21018
[Schwabhauser] p. 10Axiom A1axcgrrflx 26015  axtgcgrrflx 25582
[Schwabhauser] p. 10Axiom A2axcgrtr 26016
[Schwabhauser] p. 10Axiom A3axcgrid 26017  axtgcgrid 25583
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 25568
[Schwabhauser] p. 11Axiom A4axsegcon 26028  axtgsegcon 25584  df-trkgcb 25570
[Schwabhauser] p. 11Axiom A5ax5seg 26039  axtg5seg 25585  df-trkgcb 25570
[Schwabhauser] p. 11Axiom A6axbtwnid 26040  axtgbtwnid 25586  df-trkgb 25569
[Schwabhauser] p. 12Axiom A7axpasch 26042  axtgpasch 25587  df-trkgb 25569
[Schwabhauser] p. 12Axiom A8axlowdim2 26061  df-trkg2d 31083
[Schwabhauser] p. 13Axiom A8axtglowdim2 25590
[Schwabhauser] p. 13Axiom A9axtgupdim2 25591  df-trkg2d 31083
[Schwabhauser] p. 13Axiom A10axeuclid 26064  axtgeucl 25592  df-trkge 25571
[Schwabhauser] p. 13Axiom A11axcont 26077  axtgcont 25589  axtgcont1 25588  df-trkgb 25569
[Schwabhauser] p. 27Theorem 2.1cgrrflx 32431
[Schwabhauser] p. 27Theorem 2.2cgrcomim 32433
[Schwabhauser] p. 27Theorem 2.3cgrtr 32436
[Schwabhauser] p. 27Theorem 2.4cgrcoml 32440
[Schwabhauser] p. 27Theorem 2.5cgrcomr 32441  tgcgrcomimp 25593  tgcgrcoml 25595  tgcgrcomr 25594
[Schwabhauser] p. 28Theorem 2.8cgrtriv 32446  tgcgrtriv 25600
[Schwabhauser] p. 28Theorem 2.105segofs 32450  tg5segofs 31091
[Schwabhauser] p. 28Definition 2.10df-afs 31088  df-ofs 32427
[Schwabhauser] p. 29Theorem 2.11cgrextend 32452  tgcgrextend 25601
[Schwabhauser] p. 29Theorem 2.12segconeq 32454  tgsegconeq 25602
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 32466  btwntriv2 32456  tgbtwntriv2 25603
[Schwabhauser] p. 30Theorem 3.2btwncomim 32457  tgbtwncom 25604
[Schwabhauser] p. 30Theorem 3.3btwntriv1 32460  tgbtwntriv1 25607
[Schwabhauser] p. 30Theorem 3.4btwnswapid 32461  tgbtwnswapid 25608
[Schwabhauser] p. 30Theorem 3.5btwnexch2 32467  btwnintr 32463  tgbtwnexch2 25612  tgbtwnintr 25609
[Schwabhauser] p. 30Theorem 3.6btwnexch 32469  btwnexch3 32464  tgbtwnexch 25614  tgbtwnexch3 25610
[Schwabhauser] p. 30Theorem 3.7btwnouttr 32468  tgbtwnouttr 25613  tgbtwnouttr2 25611
[Schwabhauser] p. 32Theorem 3.13axlowdim1 26060
[Schwabhauser] p. 32Theorem 3.14btwndiff 32471  tgbtwndiff 25622
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 25615  trisegint 32472
[Schwabhauser] p. 34Theorem 4.2ifscgr 32488  tgifscgr 25624
[Schwabhauser] p. 34Theorem 4.11colcom 25674  colrot1 25675  colrot2 25676  lncom 25738  lnrot1 25739  lnrot2 25740
[Schwabhauser] p. 34Definition 4.1df-ifs 32484
[Schwabhauser] p. 35Theorem 4.3cgrsub 32489  tgcgrsub 25625
[Schwabhauser] p. 35Theorem 4.5cgrxfr 32499  tgcgrxfr 25634
[Schwabhauser] p. 35Statement 4.4ercgrg 25633
[Schwabhauser] p. 35Definition 4.4df-cgr3 32485  df-cgrg 25627
[Schwabhauser] p. 36Theorem 4.6btwnxfr 32500  tgbtwnxfr 25646
[Schwabhauser] p. 36Theorem 4.11colinearperm1 32506  colinearperm2 32508  colinearperm3 32507  colinearperm4 32509  colinearperm5 32510
[Schwabhauser] p. 36Definition 4.8df-ismt 25649
[Schwabhauser] p. 36Definition 4.10df-colinear 32483  tgellng 25669  tglng 25662
[Schwabhauser] p. 37Theorem 4.12colineartriv1 32511
[Schwabhauser] p. 37Theorem 4.13colinearxfr 32519  lnxfr 25682
[Schwabhauser] p. 37Theorem 4.14lineext 32520  lnext 25683
[Schwabhauser] p. 37Theorem 4.16fscgr 32524  tgfscgr 25684
[Schwabhauser] p. 37Theorem 4.17linecgr 32525  lncgr 25685
[Schwabhauser] p. 37Definition 4.15df-fs 32486
[Schwabhauser] p. 38Theorem 4.18lineid 32527  lnid 25686
[Schwabhauser] p. 38Theorem 4.19idinside 32528  tgidinside 25687
[Schwabhauser] p. 39Theorem 5.1btwnconn1 32545  tgbtwnconn1 25691
[Schwabhauser] p. 41Theorem 5.2btwnconn2 32546  tgbtwnconn2 25692
[Schwabhauser] p. 41Theorem 5.3btwnconn3 32547  tgbtwnconn3 25693
[Schwabhauser] p. 41Theorem 5.5brsegle2 32553
[Schwabhauser] p. 41Definition 5.4df-segle 32551  legov 25701
[Schwabhauser] p. 41Definition 5.5legov2 25702
[Schwabhauser] p. 42Remark 5.13legso 25715
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 32554
[Schwabhauser] p. 42Theorem 5.7seglerflx 32556
[Schwabhauser] p. 42Theorem 5.8segletr 32558
[Schwabhauser] p. 42Theorem 5.9segleantisym 32559
[Schwabhauser] p. 42Theorem 5.10seglelin 32560
[Schwabhauser] p. 42Theorem 5.11seglemin 32557
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 32562
[Schwabhauser] p. 42Proposition 5.7legid 25703
[Schwabhauser] p. 42Proposition 5.8legtrd 25705
[Schwabhauser] p. 42Proposition 5.9legtri3 25706
[Schwabhauser] p. 42Proposition 5.10legtrid 25707
[Schwabhauser] p. 42Proposition 5.11leg0 25708
[Schwabhauser] p. 43Theorem 6.2btwnoutside 32569
[Schwabhauser] p. 43Theorem 6.3broutsideof3 32570
[Schwabhauser] p. 43Theorem 6.4broutsideof 32565  df-outsideof 32564
[Schwabhauser] p. 43Definition 6.1broutsideof2 32566  ishlg 25718
[Schwabhauser] p. 44Theorem 6.4hlln 25723
[Schwabhauser] p. 44Theorem 6.5hlid 25725  outsideofrflx 32571
[Schwabhauser] p. 44Theorem 6.6hlcomb 25719  hlcomd 25720  outsideofcom 32572
[Schwabhauser] p. 44Theorem 6.7hltr 25726  outsideoftr 32573
[Schwabhauser] p. 44Theorem 6.11hlcgreu 25734  outsideofeu 32575
[Schwabhauser] p. 44Definition 6.8df-ray 32582
[Schwabhauser] p. 45Part 2df-lines2 32583
[Schwabhauser] p. 45Theorem 6.13outsidele 32576
[Schwabhauser] p. 45Theorem 6.15lineunray 32591
[Schwabhauser] p. 45Theorem 6.16lineelsb2 32592  tglineelsb2 25748
[Schwabhauser] p. 45Theorem 6.17linecom 32594  linerflx1 32593  linerflx2 32595  tglinecom 25751  tglinerflx1 25749  tglinerflx2 25750
[Schwabhauser] p. 45Theorem 6.18linethru 32597  tglinethru 25752
[Schwabhauser] p. 45Definition 6.14df-line2 32581  tglng 25662
[Schwabhauser] p. 45Proposition 6.13legbtwn 25710
[Schwabhauser] p. 46Theorem 6.19linethrueu 32600  tglinethrueu 25755
[Schwabhauser] p. 46Theorem 6.21lineintmo 32601  tglineineq 25759  tglineinteq 25761  tglineintmo 25758
[Schwabhauser] p. 46Theorem 6.23colline 25765
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 25766
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 25767
[Schwabhauser] p. 49Theorem 7.3mirinv 25782
[Schwabhauser] p. 49Theorem 7.7mirmir 25778
[Schwabhauser] p. 49Theorem 7.8mirreu3 25770
[Schwabhauser] p. 49Definition 7.5df-mir 25769  ismir 25775  mirbtwn 25774  mircgr 25773  mirfv 25772  mirval 25771
[Schwabhauser] p. 50Theorem 7.8mirreu 25780
[Schwabhauser] p. 50Theorem 7.9mireq 25781
[Schwabhauser] p. 50Theorem 7.10mirinv 25782
[Schwabhauser] p. 50Theorem 7.11mirf1o 25785
[Schwabhauser] p. 50Theorem 7.13miriso 25786
[Schwabhauser] p. 51Theorem 7.14mirmot 25791
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 25788  mirbtwni 25787
[Schwabhauser] p. 51Theorem 7.16mircgrs 25789
[Schwabhauser] p. 51Theorem 7.17miduniq 25801
[Schwabhauser] p. 52Lemma 7.21symquadlem 25805
[Schwabhauser] p. 52Theorem 7.18miduniq1 25802
[Schwabhauser] p. 52Theorem 7.19miduniq2 25803
[Schwabhauser] p. 52Theorem 7.20colmid 25804
[Schwabhauser] p. 53Lemma 7.22krippen 25807
[Schwabhauser] p. 55Lemma 7.25midexlem 25808
[Schwabhauser] p. 57Theorem 8.2ragcom 25814
[Schwabhauser] p. 57Definition 8.1df-rag 25810  israg 25813
[Schwabhauser] p. 58Theorem 8.3ragcol 25815
[Schwabhauser] p. 58Theorem 8.4ragmir 25816
[Schwabhauser] p. 58Theorem 8.5ragtrivb 25818
[Schwabhauser] p. 58Theorem 8.6ragflat2 25819
[Schwabhauser] p. 58Theorem 8.7ragflat 25820
[Schwabhauser] p. 58Theorem 8.8ragtriva 25821
[Schwabhauser] p. 58Theorem 8.9ragflat3 25822  ragncol 25825
[Schwabhauser] p. 58Theorem 8.10ragcgr 25823
[Schwabhauser] p. 59Theorem 8.12perpcom 25829
[Schwabhauser] p. 59Theorem 8.13ragperp 25833
[Schwabhauser] p. 59Theorem 8.14perpneq 25830
[Schwabhauser] p. 59Definition 8.11df-perpg 25812  isperp 25828
[Schwabhauser] p. 59Definition 8.13isperp2 25831
[Schwabhauser] p. 60Theorem 8.18foot 25835
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 25843  colperpexlem2 25844
[Schwabhauser] p. 63Theorem 8.21colperpex 25846  colperpexlem3 25845
[Schwabhauser] p. 64Theorem 8.22mideu 25851  midex 25850
[Schwabhauser] p. 66Lemma 8.24opphllem 25848
[Schwabhauser] p. 67Theorem 9.2oppcom 25857
[Schwabhauser] p. 67Definition 9.1islnopp 25852
[Schwabhauser] p. 68Lemma 9.3opphllem2 25861
[Schwabhauser] p. 68Lemma 9.4opphllem5 25864  opphllem6 25865
[Schwabhauser] p. 69Theorem 9.5opphl 25867
[Schwabhauser] p. 69Theorem 9.6axtgpasch 25587
[Schwabhauser] p. 70Theorem 9.6outpasch 25868
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 25876
[Schwabhauser] p. 71Definition 9.7df-hpg 25871  hpgbr 25873
[Schwabhauser] p. 72Lemma 9.10hpgerlem 25878
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 25877
[Schwabhauser] p. 72Theorem 9.11hpgid 25879
[Schwabhauser] p. 72Theorem 9.12hpgcom 25880
[Schwabhauser] p. 72Theorem 9.13hpgtr 25881
[Schwabhauser] p. 73Theorem 9.18colopp 25882
[Schwabhauser] p. 73Theorem 9.19colhp 25883
[Schwabhauser] p. 88Theorem 10.2lmieu 25897
[Schwabhauser] p. 88Definition 10.1df-mid 25887
[Schwabhauser] p. 89Theorem 10.4lmicom 25901
[Schwabhauser] p. 89Theorem 10.5lmilmi 25902
[Schwabhauser] p. 89Theorem 10.6lmireu 25903
[Schwabhauser] p. 89Theorem 10.7lmieq 25904
[Schwabhauser] p. 89Theorem 10.8lmiinv 25905
[Schwabhauser] p. 89Theorem 10.9lmif1o 25908
[Schwabhauser] p. 89Theorem 10.10lmiiso 25910
[Schwabhauser] p. 89Definition 10.3df-lmi 25888
[Schwabhauser] p. 90Theorem 10.11lmimot 25911
[Schwabhauser] p. 91Theorem 10.12hypcgr 25914
[Schwabhauser] p. 92Theorem 10.14lmiopp 25915
[Schwabhauser] p. 92Theorem 10.15lnperpex 25916
[Schwabhauser] p. 92Theorem 10.16trgcopy 25917  trgcopyeu 25919
[Schwabhauser] p. 95Definition 11.2dfcgra2 25942
[Schwabhauser] p. 95Definition 11.3iscgra 25922
[Schwabhauser] p. 95Proposition 11.4cgracgr 25931
[Schwabhauser] p. 95Proposition 11.10cgrahl1 25929  cgrahl2 25930
[Schwabhauser] p. 96Theorem 11.6cgraid 25932
[Schwabhauser] p. 96Theorem 11.9cgraswap 25933
[Schwabhauser] p. 97Theorem 11.7cgracom 25935
[Schwabhauser] p. 97Theorem 11.8cgratr 25936
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 25938  cgrahl 25939
[Schwabhauser] p. 98Theorem 11.13sacgr 25943
[Schwabhauser] p. 98Theorem 11.14oacgr 25944
[Schwabhauser] p. 98Theorem 11.15acopy 25945  acopyeu 25946
[Schwabhauser] p. 101Theorem 11.24inagswap 25951
[Schwabhauser] p. 101Theorem 11.25inaghl 25952
[Schwabhauser] p. 101Property for point ` ` to lie in the angle ` ` Defnition 11.23isinag 25950
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 25955
[Schwabhauser] p. 102Definition 11.27df-leag 25953  isleag 25954
[Schwabhauser] p. 107Theorem 11.49tgsas 25957  tgsas1 25956  tgsas2 25958  tgsas3 25959
[Schwabhauser] p. 108Theorem 11.50tgasa 25961  tgasa1 25960
[Schwabhauser] p. 109Theorem 11.51tgsss1 25962  tgsss2 25963  tgsss3 25964
[Shapiro] p. 230Theorem 6.5.1dchrhash 25217  dchrsum 25215  dchrsum2 25214  sumdchr 25218
[Shapiro] p. 232Theorem 6.5.2dchr2sum 25219  sum2dchr 25220
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 18673  ablfacrp2 18674
[Shapiro], p. 328Equation 9.2.4vmasum 25162
[Shapiro], p. 329Equation 9.2.7logfac2 25163
[Shapiro], p. 329Equation 9.2.9logfacrlim 25170
[Shapiro], p. 331Equation 9.2.13vmadivsum 25392
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 25395
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 25449  vmalogdivsum2 25448
[Shapiro], p. 375Theorem 9.4.1dirith 25439  dirith2 25438
[Shapiro], p. 375Equation 9.4.3rplogsum 25437  rpvmasum 25436  rpvmasum2 25422
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 25397
[Shapiro], p. 376Equation 9.4.8dchrvmasum 25435
[Shapiro], p. 377Lemma 9.4.1dchrisum 25402  dchrisumlem1 25399  dchrisumlem2 25400  dchrisumlem3 25401  dchrisumlema 25398
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 25405
[Shapiro], p. 379Equation 9.4.16dchrmusum 25434  dchrmusumlem 25432  dchrvmasumlem 25433
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 25404
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 25406
[Shapiro], p. 382Lemma 9.4.4dchrisum0 25430  dchrisum0re 25423  dchrisumn0 25431
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 25416
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 25420
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 25421
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 25476  pntrsumbnd2 25477  pntrsumo1 25475
[Shapiro], p. 405Equation 10.2.1mudivsum 25440
[Shapiro], p. 406Equation 10.2.6mulogsum 25442
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 25444
[Shapiro], p. 407Equation 10.2.8mulog2sum 25447
[Shapiro], p. 418Equation 10.4.6logsqvma 25452
[Shapiro], p. 418Equation 10.4.8logsqvma2 25453
[Shapiro], p. 419Equation 10.4.10selberg 25458
[Shapiro], p. 420Equation 10.4.12selberg2lem 25460
[Shapiro], p. 420Equation 10.4.14selberg2 25461
[Shapiro], p. 422Equation 10.6.7selberg3 25469
[Shapiro], p. 422Equation 10.4.20selberg4lem1 25470
[Shapiro], p. 422Equation 10.4.21selberg3lem1 25467  selberg3lem2 25468
[Shapiro], p. 422Equation 10.4.23selberg4 25471
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 25465
[Shapiro], p. 428Equation 10.6.2selbergr 25478
[Shapiro], p. 429Equation 10.6.8selberg3r 25479
[Shapiro], p. 430Equation 10.6.11selberg4r 25480
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 25494
[Shapiro], p. 434Equation 10.6.27pntlema 25506  pntlemb 25507  pntlemc 25505  pntlemd 25504  pntlemg 25508
[Shapiro], p. 435Equation 10.6.29pntlema 25506
[Shapiro], p. 436Lemma 10.6.1pntpbnd 25498
[Shapiro], p. 436Lemma 10.6.2pntibnd 25503
[Shapiro], p. 436Equation 10.6.34pntlema 25506
[Shapiro], p. 436Equation 10.6.35pntlem3 25519  pntleml 25521
[Stoll] p. 13Definition corresponds to dfsymdif3 4041
[Stoll] p. 16Exercise 4.40dif 4122  dif0 4098
[Stoll] p. 16Exercise 4.8difdifdir 4199
[Stoll] p. 17Theorem 5.1(5)unvdif 4185
[Stoll] p. 19Theorem 5.2(13)undm 4034
[Stoll] p. 19Theorem 5.2(13')indm 4035
[Stoll] p. 20Remarkinvdif 4017
[Stoll] p. 25Definition of ordered tripledf-ot 4326
[Stoll] p. 43Definitionuniiun 4708
[Stoll] p. 44Definitionintiin 4709
[Stoll] p. 45Definitiondf-iin 4658
[Stoll] p. 45Definition indexed uniondf-iun 4657
[Stoll] p. 176Theorem 3.4(27)iman 388
[Stoll] p. 262Example 4.1dfsymdif3 4041
[Strang] p. 242Section 6.3expgrowth 39058
[Suppes] p. 22Theorem 2eq0 4077  eq0f 4074
[Suppes] p. 22Theorem 4eqss 3767  eqssd 3769  eqssi 3768
[Suppes] p. 23Theorem 5ss0 4119  ss0b 4118
[Suppes] p. 23Theorem 6sstr 3760  sstrALT2 39590
[Suppes] p. 23Theorem 7pssirr 3857
[Suppes] p. 23Theorem 8pssn2lp 3858
[Suppes] p. 23Theorem 9psstr 3861
[Suppes] p. 23Theorem 10pssss 3852
[Suppes] p. 25Theorem 12elin 3947  elun 3904
[Suppes] p. 26Theorem 15inidm 3971
[Suppes] p. 26Theorem 16in0 4113
[Suppes] p. 27Theorem 23unidm 3907
[Suppes] p. 27Theorem 24un0 4112
[Suppes] p. 27Theorem 25ssun1 3927
[Suppes] p. 27Theorem 26ssequn1 3934
[Suppes] p. 27Theorem 27unss 3938
[Suppes] p. 27Theorem 28indir 4024
[Suppes] p. 27Theorem 29undir 4025
[Suppes] p. 28Theorem 32difid 4096
[Suppes] p. 29Theorem 33difin 4010
[Suppes] p. 29Theorem 34indif 4018
[Suppes] p. 29Theorem 35undif1 4186
[Suppes] p. 29Theorem 36difun2 4191
[Suppes] p. 29Theorem 37difin0 4184
[Suppes] p. 29Theorem 38disjdif 4183
[Suppes] p. 29Theorem 39difundi 4028
[Suppes] p. 29Theorem 40difindi 4030
[Suppes] p. 30Theorem 41nalset 4930
[Suppes] p. 39Theorem 61uniss 4596
[Suppes] p. 39Theorem 65uniop 5109
[Suppes] p. 41Theorem 70intsn 4648
[Suppes] p. 42Theorem 71intpr 4645  intprg 4646
[Suppes] p. 42Theorem 73op1stb 5068
[Suppes] p. 42Theorem 78intun 4644
[Suppes] p. 44Definition 15(a)dfiun2 4689  dfiun2g 4687
[Suppes] p. 44Definition 15(b)dfiin2 4690
[Suppes] p. 47Theorem 86elpw 4304  elpw2 4960  elpw2g 4959  elpwg 4306  elpwgdedVD 39673
[Suppes] p. 47Theorem 87pwid 4314
[Suppes] p. 47Theorem 89pw0 4479
[Suppes] p. 48Theorem 90pwpw0 4480
[Suppes] p. 52Theorem 101xpss12 5265
[Suppes] p. 52Theorem 102xpindi 5393  xpindir 5394
[Suppes] p. 52Theorem 103xpundi 5310  xpundir 5311
[Suppes] p. 54Theorem 105elirrv 8661
[Suppes] p. 58Theorem 2relss 5345
[Suppes] p. 59Theorem 4eldm 5458  eldm2 5459  eldm2g 5457  eldmg 5456
[Suppes] p. 59Definition 3df-dm 5260
[Suppes] p. 60Theorem 6dmin 5469
[Suppes] p. 60Theorem 8rnun 5681
[Suppes] p. 60Theorem 9rnin 5682
[Suppes] p. 60Definition 4dfrn2 5448
[Suppes] p. 61Theorem 11brcnv 5442  brcnvg 5440
[Suppes] p. 62Equation 5elcnv 5436  elcnv2 5437
[Suppes] p. 62Theorem 12relcnv 5643
[Suppes] p. 62Theorem 15cnvin 5680
[Suppes] p. 62Theorem 16cnvun 5678
[Suppes] p. 63Theorem 20co02 5792
[Suppes] p. 63Theorem 21dmcoss 5522
[Suppes] p. 63Definition 7df-co 5259
[Suppes] p. 64Theorem 26cnvco 5445
[Suppes] p. 64Theorem 27coass 5797
[Suppes] p. 65Theorem 31resundi 5550
[Suppes] p. 65Theorem 34elima 5611  elima2 5612  elima3 5613  elimag 5610
[Suppes] p. 65Theorem 35imaundi 5685
[Suppes] p. 66Theorem 40dminss 5687
[Suppes] p. 66Theorem 41imainss 5688
[Suppes] p. 67Exercise 11cnvxp 5691
[Suppes] p. 81Definition 34dfec2 7903
[Suppes] p. 82Theorem 72elec 7942  elecALTV 34371  elecg 7941
[Suppes] p. 82Theorem 73erth 7947  erth2 7948
[Suppes] p. 83Theorem 74erdisj 7950
[Suppes] p. 89Theorem 96map0b 8053
[Suppes] p. 89Theorem 97map0 8056  map0g 8054
[Suppes] p. 89Theorem 98mapsn 8057  mapsnd 8055
[Suppes] p. 89Theorem 99mapss 8058
[Suppes] p. 91Definition 12(ii)alephsuc 9095
[Suppes] p. 91Definition 12(iii)alephlim 9094
[Suppes] p. 92Theorem 1enref 8146  enrefg 8145
[Suppes] p. 92Theorem 2ensym 8162  ensymb 8161  ensymi 8163
[Suppes] p. 92Theorem 3entr 8165
[Suppes] p. 92Theorem 4unen 8200
[Suppes] p. 94Theorem 15endom 8140
[Suppes] p. 94Theorem 16ssdomg 8159
[Suppes] p. 94Theorem 17domtr 8166
[Suppes] p. 95Theorem 18sbth 8240
[Suppes] p. 97Theorem 23canth2 8273  canth2g 8274
[Suppes] p. 97Definition 3brsdom2 8244  df-sdom 8116  dfsdom2 8243
[Suppes] p. 97Theorem 21(i)sdomirr 8257
[Suppes] p. 97Theorem 22(i)domnsym 8246
[Suppes] p. 97Theorem 21(ii)sdomnsym 8245
[Suppes] p. 97Theorem 22(ii)domsdomtr 8255
[Suppes] p. 97Theorem 22(iv)brdom2 8143
[Suppes] p. 97Theorem 21(iii)sdomtr 8258
[Suppes] p. 97Theorem 22(iii)sdomdomtr 8253
[Suppes] p. 98Exercise 4fundmen 8187  fundmeng 8188
[Suppes] p. 98Exercise 6xpdom3 8218
[Suppes] p. 98Exercise 11sdomentr 8254
[Suppes] p. 104Theorem 37fofi 8412
[Suppes] p. 104Theorem 38pwfi 8421
[Suppes] p. 105Theorem 40pwfi 8421
[Suppes] p. 111Axiom for cardinal numberscarden 9579
[Suppes] p. 130Definition 3df-tr 4888
[Suppes] p. 132Theorem 9ssonuni 7137
[Suppes] p. 134Definition 6df-suc 5871
[Suppes] p. 136Theorem Schema 22findes 7247  finds 7243  finds1 7246  finds2 7245
[Suppes] p. 151Theorem 42isfinite 8717  isfinite2 8378  isfiniteg 8380  unbnn 8376
[Suppes] p. 162Definition 5df-ltnq 9946  df-ltpq 9938
[Suppes] p. 197Theorem Schema 4tfindes 7213  tfinds 7210  tfinds2 7214
[Suppes] p. 209Theorem 18oaord1 7789
[Suppes] p. 209Theorem 21oaword2 7791
[Suppes] p. 211Theorem 25oaass 7799
[Suppes] p. 225Definition 8iscard2 9006
[Suppes] p. 227Theorem 56ondomon 9591
[Suppes] p. 228Theorem 59harcard 9008
[Suppes] p. 228Definition 12(i)aleph0 9093
[Suppes] p. 228Theorem Schema 61onintss 5917
[Suppes] p. 228Theorem Schema 62onminesb 7149  onminsb 7150
[Suppes] p. 229Theorem 64alephval2 9600
[Suppes] p. 229Theorem 65alephcard 9097
[Suppes] p. 229Theorem 66alephord2i 9104
[Suppes] p. 229Theorem 67alephnbtwn 9098
[Suppes] p. 229Definition 12df-aleph 8970
[Suppes] p. 242Theorem 6weth 9523
[Suppes] p. 242Theorem 8entric 9585
[Suppes] p. 242Theorem 9carden 9579
[TakeutiZaring] p. 8Axiom 1ax-ext 2751
[TakeutiZaring] p. 13Definition 4.5df-cleq 2764
[TakeutiZaring] p. 13Proposition 4.6df-clel 2767
[TakeutiZaring] p. 13Proposition 4.9cvjust 2766
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2790
[TakeutiZaring] p. 14Definition 4.16df-oprab 6800
[TakeutiZaring] p. 14Proposition 4.14ru 3586
[TakeutiZaring] p. 15Axiom 2zfpair 5033
[TakeutiZaring] p. 15Exercise 1elpr 4339  elpr2 4340  elprg 4337
[TakeutiZaring] p. 15Exercise 2elsn 4332  elsn2 4351  elsn2g 4350  elsng 4331  velsn 4333
[TakeutiZaring] p. 15Exercise 3elop 5064
[TakeutiZaring] p. 15Exercise 4sneq 4327  sneqr 4505
[TakeutiZaring] p. 15Definition 5.1dfpr2 4335  dfsn2 4330  dfsn2ALT 4336
[TakeutiZaring] p. 16Axiom 3uniex 7104
[TakeutiZaring] p. 16Exercise 6opth 5073
[TakeutiZaring] p. 16Exercise 7opex 5061
[TakeutiZaring] p. 16Exercise 8rext 5045
[TakeutiZaring] p. 16Corollary 5.8unex 7107  unexg 7110
[TakeutiZaring] p. 16Definition 5.3dftp2 4369
[TakeutiZaring] p. 16Definition 5.5df-uni 4576
[TakeutiZaring] p. 16Definition 5.6df-in 3730  df-un 3728
[TakeutiZaring] p. 16Proposition 5.7unipr 4588  uniprg 4589
[TakeutiZaring] p. 17Axiom 4vpwex 4980
[TakeutiZaring] p. 17Exercise 1eltp 4368
[TakeutiZaring] p. 17Exercise 5elsuc 5936  elsucg 5934  sstr2 3759
[TakeutiZaring] p. 17Exercise 6uncom 3908
[TakeutiZaring] p. 17Exercise 7incom 3956
[TakeutiZaring] p. 17Exercise 8unass 3921
[TakeutiZaring] p. 17Exercise 9inass 3972
[TakeutiZaring] p. 17Exercise 10indi 4022
[TakeutiZaring] p. 17Exercise 11undi 4023
[TakeutiZaring] p. 17Definition 5.9df-pss 3739  dfss2 3740
[TakeutiZaring] p. 17Definition 5.10df-pw 4300
[TakeutiZaring] p. 18Exercise 7unss2 3935
[TakeutiZaring] p. 18Exercise 9df-ss 3737  sseqin2 3968
[TakeutiZaring] p. 18Exercise 10ssid 3773
[TakeutiZaring] p. 18Exercise 12inss1 3981  inss2 3982
[TakeutiZaring] p. 18Exercise 13nss 3812
[TakeutiZaring] p. 18Exercise 15unieq 4583
[TakeutiZaring] p. 18Exercise 18sspwb 5046  sspwimp 39674  sspwimpALT 39681  sspwimpALT2 39684  sspwimpcf 39676
[TakeutiZaring] p. 18Exercise 19pweqb 5054
[TakeutiZaring] p. 19Axiom 5ax-rep 4905
[TakeutiZaring] p. 20Definitiondf-rab 3070
[TakeutiZaring] p. 20Corollary 5.160ex 4925
[TakeutiZaring] p. 20Definition 5.12df-dif 3726
[TakeutiZaring] p. 20Definition 5.14dfnul2 4065
[TakeutiZaring] p. 20Proposition 5.15difid 4096
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4079  n0f 4076  neq0 4078  neq0f 4075
[TakeutiZaring] p. 21Axiom 6zfreg 8660
[TakeutiZaring] p. 21Axiom 6'zfregs 8776
[TakeutiZaring] p. 21Theorem 5.22setind 8778
[TakeutiZaring] p. 21Definition 5.20df-v 3353
[TakeutiZaring] p. 21Proposition 5.21vprc 4932
[TakeutiZaring] p. 22Exercise 10ss 4117
[TakeutiZaring] p. 22Exercise 3ssex 4937  ssexg 4939
[TakeutiZaring] p. 22Exercise 4inex1 4934
[TakeutiZaring] p. 22Exercise 5ruv 8667
[TakeutiZaring] p. 22Exercise 6elirr 8662
[TakeutiZaring] p. 22Exercise 7ssdif0 4090
[TakeutiZaring] p. 22Exercise 11difdif 3887
[TakeutiZaring] p. 22Exercise 13undif3 4037  undif3VD 39638
[TakeutiZaring] p. 22Exercise 14difss 3888
[TakeutiZaring] p. 22Exercise 15sscon 3895
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3066
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3067
[TakeutiZaring] p. 23Proposition 6.2xpex 7113  xpexg 7111
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5257
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6099
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6251  fun11 6102
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6042  svrelfun 6100
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5447
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5449
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5262
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5263
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5259
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5729  dfrel2 5723
[TakeutiZaring] p. 25Exercise 3xpss 5266
[TakeutiZaring] p. 25Exercise 5relun 5373
[TakeutiZaring] p. 25Exercise 6reluni 5379
[TakeutiZaring] p. 25Exercise 9inxp 5392
[TakeutiZaring] p. 25Exercise 12relres 5566
[TakeutiZaring] p. 25Exercise 13opelres 5541  opelresALTV 34372  opelresg 5539
[TakeutiZaring] p. 25Exercise 14dmres 5559
[TakeutiZaring] p. 25Exercise 15resss 5562
[TakeutiZaring] p. 25Exercise 17resabs1 5567
[TakeutiZaring] p. 25Exercise 18funres 6071
[TakeutiZaring] p. 25Exercise 24relco 5776
[TakeutiZaring] p. 25Exercise 29funco 6070
[TakeutiZaring] p. 25Exercise 30f1co 6252
[TakeutiZaring] p. 26Definition 6.10eu2 2658
[TakeutiZaring] p. 26Definition 6.11conventions 27599  df-fv 6038  fv3 6349
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7264  cnvexg 7263
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7250  dmexg 7248
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7251  rnexg 7249
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 39181
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7259
[TakeutiZaring] p. 27Corollary 6.13fvex 6344
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 41769  tz6.12-1 6353  tz6.12-afv 41768  tz6.12 6354  tz6.12c 6356
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 6324  tz6.12i 6357
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6033
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6034
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6036  wfo 6028
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6035  wf1 6027
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6037  wf1o 6029
[TakeutiZaring] p. 28Exercise 4eqfnfv 6456  eqfnfv2 6457  eqfnfv2f 6460
[TakeutiZaring] p. 28Exercise 5fvco 6418
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 6628
[TakeutiZaring] p. 28Proposition 6.17resfunexg 6626
[TakeutiZaring] p. 29Exercise 9funimaex 6115  funimaexg 6114
[TakeutiZaring] p. 29Definition 6.18df-br 4788
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5172
[TakeutiZaring] p. 30Definition 6.21dffr2 5215  dffr3 5638  eliniseg 5634  iniseg 5636
[TakeutiZaring] p. 30Definition 6.22df-eprel 5163
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5228  fr3nr 7130  frirr 5227
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5209
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7132
[TakeutiZaring] p. 31Exercise 1frss 5217
[TakeutiZaring] p. 31Exercise 4wess 5237
[TakeutiZaring] p. 31Proposition 6.26tz6.26 5853  tz6.26i 5854  wefrc 5244  wereu2 5247
[TakeutiZaring] p. 32Theorem 6.27wfi 5855  wfii 5856
[TakeutiZaring] p. 32Definition 6.28df-isom 6039
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6725
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6726
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6732
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6733
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6734
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6738
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6745
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6747
[TakeutiZaring] p. 35Notationwtr 4887
[TakeutiZaring] p. 35Theorem 7.2trelpss 39182  tz7.2 5234
[TakeutiZaring] p. 35Definition 7.1dftr3 4891
[TakeutiZaring] p. 36Proposition 7.4ordwe 5878
[TakeutiZaring] p. 36Proposition 7.5tz7.5 5886
[TakeutiZaring] p. 36Proposition 7.6ordelord 5887  ordelordALT 39270  ordelordALTVD 39623
[TakeutiZaring] p. 37Corollary 7.8ordelpss 5893  ordelssne 5892
[TakeutiZaring] p. 37Proposition 7.7tz7.7 5891
[TakeutiZaring] p. 37Proposition 7.9ordin 5895
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7139
[TakeutiZaring] p. 38Corollary 7.15ordsson 7140
[TakeutiZaring] p. 38Definition 7.11df-on 5869
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 5897
[TakeutiZaring] p. 38Proposition 7.12onfrALT 39287  ordon 7133
[TakeutiZaring] p. 38Proposition 7.13onprc 7135
[TakeutiZaring] p. 39Theorem 7.17tfi 7204
[TakeutiZaring] p. 40Exercise 3ontr2 5914
[TakeutiZaring] p. 40Exercise 7dftr2 4889
[TakeutiZaring] p. 40Exercise 9onssmin 7148
[TakeutiZaring] p. 40Exercise 11unon 7182
[TakeutiZaring] p. 40Exercise 12ordun 5971
[TakeutiZaring] p. 40Exercise 14ordequn 5970
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7136
[TakeutiZaring] p. 40Proposition 7.20elssuni 4604
[TakeutiZaring] p. 41Definition 7.22df-suc 5871
[TakeutiZaring] p. 41Proposition 7.23sssucid 5944  sucidg 5945
[TakeutiZaring] p. 41Proposition 7.24suceloni 7164
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 5960  ordnbtwn 5958
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7179
[TakeutiZaring] p. 42Exercise 1df-lim 5870
[TakeutiZaring] p. 42Exercise 4omssnlim 7230
[TakeutiZaring] p. 42Exercise 7ssnlim 7234
[TakeutiZaring] p. 42Exercise 8onsucssi 7192  ordelsuc 7171
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7173
[TakeutiZaring] p. 42Definition 7.27nlimon 7202
[TakeutiZaring] p. 42Definition 7.28dfom2 7218
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7236
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7237
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7238
[TakeutiZaring] p. 43Remarkomon 7227
[TakeutiZaring] p. 43Axiom 7inf3 8700  omex 8708
[TakeutiZaring] p. 43Theorem 7.32ordom 7225
[TakeutiZaring] p. 43Corollary 7.31find 7242
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7239
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7240
[TakeutiZaring] p. 44Exercise 1limomss 7221
[TakeutiZaring] p. 44Exercise 2int0 4626
[TakeutiZaring] p. 44Exercise 3trintss 4903
[TakeutiZaring] p. 44Exercise 4intss1 4627
[TakeutiZaring] p. 44Exercise 5intex 4952
[TakeutiZaring] p. 44Exercise 6oninton 7151
[TakeutiZaring] p. 44Exercise 11ordintdif 5916
[TakeutiZaring] p. 44Definition 7.35df-int 4613
[TakeutiZaring] p. 44Proposition 7.34noinfep 8725
[TakeutiZaring] p. 45Exercise 4onint 7146
[TakeutiZaring] p. 47Lemma 1tfrlem1 7629
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 7650
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 7651
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 7652
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 7659  tz7.44-2 7660  tz7.44-3 7661
[TakeutiZaring] p. 50Exercise 1smogt 7621
[TakeutiZaring] p. 50Exercise 3smoiso 7616
[TakeutiZaring] p. 50Definition 7.46df-smo 7600
[TakeutiZaring] p. 51Proposition 7.49tz7.49 7697  tz7.49c 7698
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 7695
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 7694
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 7696
[TakeutiZaring] p. 53Proposition 7.532eu5 2706
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9038
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9039
[TakeutiZaring] p. 56Definition 8.1oalim 7770  oasuc 7762
[TakeutiZaring] p. 57Remarktfindsg 7211
[TakeutiZaring] p. 57Proposition 8.2oacl 7773
[TakeutiZaring] p. 57Proposition 8.3oa0 7754  oa0r 7776
[TakeutiZaring] p. 57Proposition 8.16omcl 7774
[TakeutiZaring] p. 58Corollary 8.5oacan 7786
[TakeutiZaring] p. 58Proposition 8.4nnaord 7857  nnaordi 7856  oaord 7785  oaordi 7784
[TakeutiZaring] p. 59Proposition 8.6iunss2 4700  uniss2 4607
[TakeutiZaring] p. 59Proposition 8.7oawordri 7788
[TakeutiZaring] p. 59Proposition 8.8oawordeu 7793  oawordex 7795
[TakeutiZaring] p. 59Proposition 8.9nnacl 7849
[TakeutiZaring] p. 59Proposition 8.10oaabs 7882
[TakeutiZaring] p. 60Remarkoancom 8716
[TakeutiZaring] p. 60Proposition 8.11oalimcl 7798
[TakeutiZaring] p. 62Exercise 1nnarcl 7854
[TakeutiZaring] p. 62Exercise 5oaword1 7790
[TakeutiZaring] p. 62Definition 8.15om0 7755  om0x 7757  omlim 7771  omsuc 7764
[TakeutiZaring] p. 63Proposition 8.17nnecl 7851  nnmcl 7850
[TakeutiZaring] p. 63Proposition 8.19nnmord 7870  nnmordi 7869  omord 7806  omordi 7804
[TakeutiZaring] p. 63Proposition 8.20omcan 7807
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 7874  omwordri 7810
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 7777
[TakeutiZaring] p. 63Proposition 8.18(2)om1 7780  om1r 7781
[TakeutiZaring] p. 64Proposition 8.22om00 7813
[TakeutiZaring] p. 64Proposition 8.23omordlim 7815
[TakeutiZaring] p. 64Proposition 8.24omlimcl 7816
[TakeutiZaring] p. 64Proposition 8.25odi 7817
[TakeutiZaring] p. 65Theorem 8.26omass 7818
[TakeutiZaring] p. 67Definition 8.30nnesuc 7846  oe0 7760  oelim 7772  oesuc 7765  onesuc 7768
[TakeutiZaring] p. 67Proposition 8.31oe0m0 7758
[TakeutiZaring] p. 67Proposition 8.32oen0 7824
[TakeutiZaring] p. 67Proposition 8.33oeordi 7825
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 7759
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 7783
[TakeutiZaring] p. 68Corollary 8.34oeord 7826
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 7832
[TakeutiZaring] p. 68Proposition 8.35oewordri 7830
[TakeutiZaring] p. 68Proposition 8.37oeworde 7831
[TakeutiZaring] p. 69Proposition 8.41oeoa 7835
[TakeutiZaring] p. 70Proposition 8.42oeoe 7837
[TakeutiZaring] p. 73Theorem 9.1trcl 8772  tz9.1 8773
[TakeutiZaring] p. 76Definition 9.9df-r1 8795  r10 8799  r1lim 8803  r1limg 8802  r1suc 8801  r1sucg 8800
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 8811  r1ord2 8812  r1ordg 8809
[TakeutiZaring] p. 78Proposition 9.12tz9.12 8821
[TakeutiZaring] p. 78Proposition 9.13rankwflem 8846  tz9.13 8822  tz9.13g 8823
[TakeutiZaring] p. 79Definition 9.14df-rank 8796  rankval 8847  rankvalb 8828  rankvalg 8848
[TakeutiZaring] p. 79Proposition 9.16rankel 8870  rankelb 8855
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 8884  rankval3 8871  rankval3b 8857
[TakeutiZaring] p. 79Proposition 9.18rankonid 8860
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 8826
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 8865  rankr1c 8852  rankr1g 8863
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 8866
[TakeutiZaring] p. 80Exercise 1rankss 8880  rankssb 8879
[TakeutiZaring] p. 80Exercise 2unbndrank 8873
[TakeutiZaring] p. 80Proposition 9.19bndrank 8872
[TakeutiZaring] p. 83Axiom of Choiceac4 9503  dfac3 9148
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9057  numth 9500  numth2 9499
[TakeutiZaring] p. 85Definition 10.4cardval 9574
[TakeutiZaring] p. 85Proposition 10.5cardid 9575  cardid2 8983
[TakeutiZaring] p. 85Proposition 10.9oncard 8990
[TakeutiZaring] p. 85Proposition 10.10carden 9579
[TakeutiZaring] p. 85Proposition 10.11cardidm 8989
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 8974
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 8995
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 8987
[TakeutiZaring] p. 87Proposition 10.15pwen 8293
[TakeutiZaring] p. 88Exercise 1en0 8176
[TakeutiZaring] p. 88Exercise 7infensuc 8298
[TakeutiZaring] p. 89Exercise 10omxpen 8222
[TakeutiZaring] p. 90Corollary 10.23cardnn 8993
[TakeutiZaring] p. 90Definition 10.27alephiso 9125
[TakeutiZaring] p. 90Proposition 10.20nneneq 8303
[TakeutiZaring] p. 90Proposition 10.22onomeneq 8310
[TakeutiZaring] p. 90Proposition 10.26alephprc 9126
[TakeutiZaring] p. 90Corollary 10.21(1)php5 8308
[TakeutiZaring] p. 91Exercise 2alephle 9115
[TakeutiZaring] p. 91Exercise 3aleph0 9093
[TakeutiZaring] p. 91Exercise 4cardlim 9002
[TakeutiZaring] p. 91Exercise 7infpss 9245
[TakeutiZaring] p. 91Exercise 8infcntss 8394
[TakeutiZaring] p. 91Definition 10.29df-fin 8117  isfi 8137
[TakeutiZaring] p. 92Proposition 10.32onfin 8311
[TakeutiZaring] p. 92Proposition 10.34imadomg 9562
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 8215
[TakeutiZaring] p. 93Proposition 10.35fodomb 9554
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 9217  unxpdom 8327
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9004  cardsdomelir 9003
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 8329
[TakeutiZaring] p. 94Proposition 10.39infxpen 9041
[TakeutiZaring] p. 95Definition 10.42df-map 8015
[TakeutiZaring] p. 95Proposition 10.40infxpidm 9590  infxpidm2 9044
[TakeutiZaring] p. 95Proposition 10.41infcda 9236  infxp 9243
[TakeutiZaring] p. 96Proposition 10.44pw2en 8227  pw2f1o 8225
[TakeutiZaring] p. 96Proposition 10.45mapxpen 8286
[TakeutiZaring] p. 97Theorem 10.46ac6s3 9515
[TakeutiZaring] p. 98Theorem 10.46ac6c5 9510  ac6s5 9519
[TakeutiZaring] p. 98Theorem 10.47unidom 9571
[TakeutiZaring] p. 99Theorem 10.48uniimadom 9572  uniimadomf 9573
[TakeutiZaring] p. 100Definition 11.1cfcof 9302
[TakeutiZaring] p. 101Proposition 11.7cofsmo 9297
[TakeutiZaring] p. 102Exercise 1cfle 9282
[TakeutiZaring] p. 102Exercise 2cf0 9279
[TakeutiZaring] p. 102Exercise 3cfsuc 9285
[TakeutiZaring] p. 102Exercise 4cfom 9292
[TakeutiZaring] p. 102Proposition 11.9coftr 9301
[TakeutiZaring] p. 103Theorem 11.15alephreg 9610
[TakeutiZaring] p. 103Proposition 11.11cardcf 9280
[TakeutiZaring] p. 103Proposition 11.13alephsing 9304
[TakeutiZaring] p. 104Corollary 11.17cardinfima 9124
[TakeutiZaring] p. 104Proposition 11.16carduniima 9123
[TakeutiZaring] p. 104Proposition 11.18alephfp 9135  alephfp2 9136
[TakeutiZaring] p. 106Theorem 11.20gchina 9727
[TakeutiZaring] p. 106Theorem 11.21mappwen 9139
[TakeutiZaring] p. 107Theorem 11.26konigth 9597
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 9611
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 9612
[Tarski] p. 67Axiom B5ax-c5 34689
[Tarski] p. 67Scheme B5sp 2207
[Tarski] p. 68Lemma 6avril1 27661  equid 2097
[Tarski] p. 69Lemma 7equcomi 2102
[Tarski] p. 70Lemma 14spim 2416  spime 2418  spimeh 2083
[Tarski] p. 70Lemma 16ax-12 2203  ax-c15 34695  ax12i 2048
[Tarski] p. 70Lemmas 16 and 17sb6 2272
[Tarski] p. 75Axiom B7ax6v 2058
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1991  ax5ALT 34713
[Tarski], p. 75Scheme B8 of system S2ax-7 2093  ax-8 2147  ax-9 2154
[Tarski1999] p. 178Axiom 4axtgsegcon 25584
[Tarski1999] p. 178Axiom 5axtg5seg 25585
[Tarski1999] p. 179Axiom 7axtgpasch 25587
[Tarski1999] p. 180Axiom 7.1axtgpasch 25587
[Tarski1999] p. 185Axiom 11axtgcont1 25588
[Truss] p. 114Theorem 5.18ruc 15178
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 33780
[Viaclovsky8] p. 3Proposition 7ismblfin 33782
[Weierstrass] p. 272Definitiondf-mdet 20609  mdetuni 20646
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 889
[WhiteheadRussell] p. 96Axiom *1.3olc 857
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 858
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 905
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 952
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 180
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 132
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-pm2.04 33605
[WhiteheadRussell] p. 100Theorem *2.05frege5 38618  imim2 58  wl-imim2 33600
[WhiteheadRussell] p. 100Theorem *2.06imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 882
[WhiteheadRussell] p. 101Theorem *2.06barbara 2712  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 888
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-id 33603
[WhiteheadRussell] p. 101Theorem *2.11exmid 880
[WhiteheadRussell] p. 101Theorem *2.12notnot 138
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 883
[WhiteheadRussell] p. 102Theorem *2.14notnotr 128  notnotrALT2 39683  wl-notnotr 33604
[WhiteheadRussell] p. 102Theorem *2.15con1 145
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 38648  axfrege28 38647  con3 150
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 123
[WhiteheadRussell] p. 104Theorem *2.2orc 856
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 910
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 121  wl-pm2.21 33597
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 122
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 876
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 925
[WhiteheadRussell] p. 104Theorem *2.27conventions-label 27600  pm2.27 42  wl-pm2.27 33595
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 908
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 909
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 954
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 955
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 953
[WhiteheadRussell] p. 105Definition *2.33df-3or 1072
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 892
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 893
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 928
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 868
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 869
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 165
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 182
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 870
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 871
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 872
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 166
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 168
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 840
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 841
[WhiteheadRussell] p. 107Theorem *2.55orel1 875
[WhiteheadRussell] p. 107Theorem *2.56orel2 877
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 183
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 885
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 926
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 927
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 184
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 878  pm2.67 879
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 167
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 884
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 957
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 886
[WhiteheadRussell] p. 108Theorem *2.69looinv 194
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 958
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 959
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 919
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 917
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 956
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 960
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 918
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 976
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 455  pm3.2im 158
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 977
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 978
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 979
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 980
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 457
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 447
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 389
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 804
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 435
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 436
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 468  simplim 164
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 471  simprim 163
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 748
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 749
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 809
[WhiteheadRussell] p. 113Fact)pm3.45 608
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 811
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 480
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 481
[WhiteheadRussell] p. 113Theorem *3.44jao 945  pm3.44 944
[WhiteheadRussell] p. 113Theorem *3.47prth 810
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 459
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 948
[WhiteheadRussell] p. 116Theorem *4.1con34b 305
[WhiteheadRussell] p. 117Theorem *4.2biid 251
[WhiteheadRussell] p. 117Theorem *4.11notbi 308
[WhiteheadRussell] p. 117Theorem *4.12con2bi 342
[WhiteheadRussell] p. 117Theorem *4.13notnotb 304
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 808
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 828
[WhiteheadRussell] p. 117Theorem *4.21bicom 212
[WhiteheadRussell] p. 117Theorem *4.22biantr 807  bitr 806
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 553
[WhiteheadRussell] p. 117Theorem *4.25oridm 890  pm4.25 891
[WhiteheadRussell] p. 118Theorem *4.3ancom 448
[WhiteheadRussell] p. 118Theorem *4.4andi 992
[WhiteheadRussell] p. 118Theorem *4.31orcom 859
[WhiteheadRussell] p. 118Theorem *4.32anass 454
[WhiteheadRussell] p. 118Theorem *4.33orass 907
[WhiteheadRussell] p. 118Theorem *4.36anbi1 617
[WhiteheadRussell] p. 118Theorem *4.37orbi1 903
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 619
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 961
[WhiteheadRussell] p. 118Definition *4.34df-3an 1073
[WhiteheadRussell] p. 119Theorem *4.41ordi 990
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1040
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1008
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 981
[WhiteheadRussell] p. 119Theorem *4.45orabs 983  pm4.45 982  pm4.45im 825
[WhiteheadRussell] p. 120Theorem *4.5anor 967
[WhiteheadRussell] p. 120Theorem *4.6imor 842
[WhiteheadRussell] p. 120Theorem *4.7anclb 535
[WhiteheadRussell] p. 120Theorem *4.51ianor 966
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 969
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 970
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 971
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 972
[WhiteheadRussell] p. 120Theorem *4.56ioran 968  pm4.56 973
[WhiteheadRussell] p. 120Theorem *4.57oran 974  pm4.57 975
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 391
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 845
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 384
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 838
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 392
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 839
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 385
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 547  pm4.71d 551  pm4.71i 549  pm4.71r 548  pm4.71rd 552  pm4.71ri 550
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 934
[WhiteheadRussell] p. 121Theorem *4.73iba 517
[WhiteheadRussell] p. 121Theorem *4.74biorf 922
[WhiteheadRussell] p. 121Theorem *4.76jcab 507  pm4.76 508
[WhiteheadRussell] p. 121Theorem *4.77jaob 946  pm4.77 947
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 920
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 988
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 379
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 380
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1009
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1010
[WhiteheadRussell] p. 122Theorem *4.84imbi1 336
[WhiteheadRussell] p. 122Theorem *4.85imbi2 337
[WhiteheadRussell] p. 122Theorem *4.86bibi1 340
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 375  impexp 437  pm4.87 832
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 821
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 929
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 930
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 932
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 931
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 998
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 999
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 997
[WhiteheadRussell] p. 124Theorem *5.18nbbn 372  pm5.18 370
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 374
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 822
[WhiteheadRussell] p. 124Theorem *5.22xor 1000
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1034
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1036
[WhiteheadRussell] p. 124Theorem *5.25dfor2 887
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 562
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 376
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 350
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 986
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 938
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 827
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 563
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 831
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 823
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 829
[WhiteheadRussell] p. 125Theorem *5.41imdi 377  pm5.41 378
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 533
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 532
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 989
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1003
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 933
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 985
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1004
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1005
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1014
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 355
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 259
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1015
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 39081
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 39082
[WhiteheadRussell] p. 147Theorem *10.2219.26 1949
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 39083
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 39084
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 39085
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1972
[WhiteheadRussell] p. 151Theorem *10.301albitr 39086
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 39087
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 39088
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 39089
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 39090
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 39092
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 39093
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 39094
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 39091
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2595
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 39097
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 39098
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2500
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2194
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1904
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1905
[WhiteheadRussell] p. 161Theorem *11.319.21vv 39099
[WhiteheadRussell] p. 162Theorem *11.322alim 39100
[WhiteheadRussell] p. 162Theorem *11.332albi 39101
[WhiteheadRussell] p. 162Theorem *11.342exim 39102
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 39104
[WhiteheadRussell] p. 162Theorem *11.3412exbi 39103
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1966
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 39106
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 39107
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 39105
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1903
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 39108
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 39109
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1922
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 39110
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2341
[WhiteheadRussell] p. 164Theorem *11.5212exanali 39111
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 39116
[WhiteheadRussell] p. 165Theorem *11.56aaanv 39112
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 39113
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 39114
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 39115
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 39120
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 39117
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 39118
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 39119
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 39121
[WhiteheadRussell] p. 175Definition *14.02df-eu 2622
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 39132  pm13.13b 39133
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 39134
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3024
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3025
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3495
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 39140
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 39141
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 39135
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 39291  pm13.193 39136
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 39137
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 39138
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 39139
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 39146
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 39145
[WhiteheadRussell] p. 184Definition *14.01iotasbc 39144
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3640
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 39147  pm14.122b 39148  pm14.122c 39149
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 39150  pm14.123b 39151  pm14.123c 39152
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 39154
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 39153
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 39155
[WhiteheadRussell] p. 190Theorem *14.22iota4 6011
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 39156
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6012
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 39157
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 39159
[WhiteheadRussell] p. 192Theorem *14.26eupick 2685  eupickbi 2688  sbaniota 39160
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 39158
[WhiteheadRussell] p. 192Theorem *14.271eubi 39161
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 39162
[WhiteheadRussell] p. 235Definition *30.01conventions 27599  df-fv 6038
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9030  pm54.43lem 9029
[Young] p. 141Definition of operator orderingleop2 29323
[Young] p. 142Example 12.2(i)0leop 29329  idleop 29330
[vandenDries] p. 42Lemma 61irrapx1 37916
[vandenDries] p. 43Theorem 62pellex 37923  pellexlem1 37917

This page was last updated on 18-Aug-2022.
Copyright terms: Public domain