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 17616
[Adamek] p. 21Condition 3.1(b)df-cat 17616
[Adamek] p. 22Example 3.3(1)df-setc 18030
[Adamek] p. 24Example 3.3(4.c)0cat 17637
[Adamek] p. 24Example 3.3(4.d)df-prstc 47770  prsthinc 47761
[Adamek] p. 24Example 3.3(4.e)df-mndtc 47791  df-mndtc 47791
[Adamek] p. 25Definition 3.5df-oppc 17660
[Adamek] p. 28Remark 3.9oppciso 17732
[Adamek] p. 28Remark 3.12invf1o 17720  invisoinvl 17741
[Adamek] p. 28Example 3.13idinv 17740  idiso 17739
[Adamek] p. 28Corollary 3.11inveq 17725
[Adamek] p. 28Definition 3.8df-inv 17699  df-iso 17700  dfiso2 17723
[Adamek] p. 28Proposition 3.10sectcan 17706
[Adamek] p. 29Remark 3.16cicer 17757
[Adamek] p. 29Definition 3.15cic 17750  df-cic 17747
[Adamek] p. 29Definition 3.17df-func 17812
[Adamek] p. 29Proposition 3.14(1)invinv 17721
[Adamek] p. 29Proposition 3.14(2)invco 17722  isoco 17728
[Adamek] p. 30Remark 3.19df-func 17812
[Adamek] p. 30Example 3.20(1)idfucl 17835
[Adamek] p. 32Proposition 3.21funciso 17828
[Adamek] p. 33Example 3.26(2)df-thinc 47727  prsthinc 47761  thincciso 47756
[Adamek] p. 33Example 3.26(3)df-mndtc 47791
[Adamek] p. 33Proposition 3.23cofucl 17842
[Adamek] p. 34Remark 3.28(2)catciso 18065
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18123
[Adamek] p. 34Definition 3.27(2)df-fth 17860
[Adamek] p. 34Definition 3.27(3)df-full 17859
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18123
[Adamek] p. 35Corollary 3.32ffthiso 17884
[Adamek] p. 35Proposition 3.30(c)cofth 17890
[Adamek] p. 35Proposition 3.30(d)cofull 17889
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18108
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18108
[Adamek] p. 39Definition 3.41funcoppc 17829
[Adamek] p. 39Definition 3.44.df-catc 18053
[Adamek] p. 39Proposition 3.43(c)fthoppc 17878
[Adamek] p. 39Proposition 3.43(d)fulloppc 17877
[Adamek] p. 40Remark 3.48catccat 18062
[Adamek] p. 40Definition 3.47df-catc 18053
[Adamek] p. 48Example 4.3(1.a)0subcat 17792
[Adamek] p. 48Example 4.3(1.b)catsubcat 17793
[Adamek] p. 48Definition 4.1(2)fullsubc 17804
[Adamek] p. 48Definition 4.1(a)df-subc 17763
[Adamek] p. 49Remark 4.4(2)ressffth 17893
[Adamek] p. 83Definition 6.1df-nat 17898
[Adamek] p. 87Remark 6.14(a)fuccocl 17921
[Adamek] p. 87Remark 6.14(b)fucass 17925
[Adamek] p. 87Definition 6.15df-fuc 17899
[Adamek] p. 88Remark 6.16fuccat 17927
[Adamek] p. 101Definition 7.1df-inito 17938
[Adamek] p. 101Example 7.2 (6)irinitoringc 47055
[Adamek] p. 102Definition 7.4df-termo 17939
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17966
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17970
[Adamek] p. 103Definition 7.7df-zeroo 17940
[Adamek] p. 103Example 7.9 (3)nzerooringczr 47058
[Adamek] p. 103Proposition 7.6termoeu1w 17973
[Adamek] p. 106Definition 7.19df-sect 17698
[Adamek] p. 185Section 10.67updjud 9931
[Adamek] p. 478Item Rngdf-ringc 46991
[AhoHopUll] p. 2Section 1.1df-bigo 47321
[AhoHopUll] p. 12Section 1.3df-blen 47343
[AhoHopUll] p. 318Section 9.1df-concat 14525  df-pfx 14625  df-substr 14595  df-word 14469  lencl 14487  wrd0 14493
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24445  df-nmoo 30265
[AkhiezerGlazman] p. 64Theoremhmopidmch 31673  hmopidmchi 31671
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 31721  pjcmul2i 31722
[AkhiezerGlazman] p. 72Theoremcnvunop 31438  unoplin 31440
[AkhiezerGlazman] p. 72Equation 2unopadj 31439  unopadj2 31458
[AkhiezerGlazman] p. 73Theoremelunop2 31533  lnopunii 31532
[AkhiezerGlazman] p. 80Proposition 1adjlnop 31606
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27652
[Alling] p. 184Axiom Bbdayfo 27416
[Alling] p. 184Axiom Osltso 27415
[Alling] p. 184Axiom SDnodense 27431
[Alling] p. 185Lemma 0nocvxmin 27516
[Alling] p. 185Theoremconway 27537
[Alling] p. 185Axiom FEnoeta 27482
[Alling] p. 186Theorem 4slerec 27557
[Alling], p. 2Definitionrp-brsslt 42476
[Alling], p. 3Notenla0001 42479  nla0002 42477  nla0003 42478
[Apostol] p. 18Theorem I.1addcan 11402  addcan2d 11422  addcan2i 11412  addcand 11421  addcani 11411
[Apostol] p. 18Theorem I.2negeu 11454
[Apostol] p. 18Theorem I.3negsub 11512  negsubd 11581  negsubi 11542
[Apostol] p. 18Theorem I.4negneg 11514  negnegd 11566  negnegi 11534
[Apostol] p. 18Theorem I.5subdi 11651  subdid 11674  subdii 11667  subdir 11652  subdird 11675  subdiri 11668
[Apostol] p. 18Theorem I.6mul01 11397  mul01d 11417  mul01i 11408  mul02 11396  mul02d 11416  mul02i 11407
[Apostol] p. 18Theorem I.7mulcan 11855  mulcan2d 11852  mulcand 11851  mulcani 11857
[Apostol] p. 18Theorem I.8receu 11863  xreceu 32355
[Apostol] p. 18Theorem I.9divrec 11892  divrecd 11997  divreci 11963  divreczi 11956
[Apostol] p. 18Theorem I.10recrec 11915  recreci 11950
[Apostol] p. 18Theorem I.11mul0or 11858  mul0ord 11868  mul0ori 11866
[Apostol] p. 18Theorem I.12mul2neg 11657  mul2negd 11673  mul2negi 11666  mulneg1 11654  mulneg1d 11671  mulneg1i 11664
[Apostol] p. 18Theorem I.13divadddiv 11933  divadddivd 12038  divadddivi 11980
[Apostol] p. 18Theorem I.14divmuldiv 11918  divmuldivd 12035  divmuldivi 11978  rdivmuldivd 20304
[Apostol] p. 18Theorem I.15divdivdiv 11919  divdivdivd 12041  divdivdivi 11981
[Apostol] p. 20Axiom 7rpaddcl 13000  rpaddcld 13035  rpmulcl 13001  rpmulcld 13036
[Apostol] p. 20Axiom 8rpneg 13010
[Apostol] p. 20Axiom 90nrp 13013
[Apostol] p. 20Theorem I.17lttri 11344
[Apostol] p. 20Theorem I.18ltadd1d 11811  ltadd1dd 11829  ltadd1i 11772
[Apostol] p. 20Theorem I.19ltmul1 12068  ltmul1a 12067  ltmul1i 12136  ltmul1ii 12146  ltmul2 12069  ltmul2d 13062  ltmul2dd 13076  ltmul2i 12139
[Apostol] p. 20Theorem I.20msqgt0 11738  msqgt0d 11785  msqgt0i 11755
[Apostol] p. 20Theorem I.210lt1 11740
[Apostol] p. 20Theorem I.23lt0neg1 11724  lt0neg1d 11787  ltneg 11718  ltnegd 11796  ltnegi 11762
[Apostol] p. 20Theorem I.25lt2add 11703  lt2addd 11841  lt2addi 11780
[Apostol] p. 20Definition of positive numbersdf-rp 12979
[Apostol] p. 21Exercise 4recgt0 12064  recgt0d 12152  recgt0i 12123  recgt0ii 12124
[Apostol] p. 22Definition of integersdf-z 12563
[Apostol] p. 22Definition of positive integersdfnn3 12230
[Apostol] p. 22Definition of rationalsdf-q 12937
[Apostol] p. 24Theorem I.26supeu 9451
[Apostol] p. 26Theorem I.28nnunb 12472
[Apostol] p. 26Theorem I.29arch 12473  archd 44157
[Apostol] p. 28Exercise 2btwnz 12669
[Apostol] p. 28Exercise 3nnrecl 12474
[Apostol] p. 28Exercise 4rebtwnz 12935
[Apostol] p. 28Exercise 5zbtwnre 12934
[Apostol] p. 28Exercise 6qbtwnre 13182
[Apostol] p. 28Exercise 10(a)zeneo 16286  zneo 12649  zneoALTV 46635
[Apostol] p. 29Theorem I.35cxpsqrtth 26474  msqsqrtd 15391  resqrtth 15206  sqrtth 15315  sqrtthi 15321  sqsqrtd 15390
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12219
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12901
[Apostol] p. 361Remarkcrreczi 14195
[Apostol] p. 363Remarkabsgt0i 15350
[Apostol] p. 363Exampleabssubd 15404  abssubi 15354
[ApostolNT] p. 7Remarkfmtno0 46506  fmtno1 46507  fmtno2 46516  fmtno3 46517  fmtno4 46518  fmtno5fac 46548  fmtnofz04prm 46543
[ApostolNT] p. 7Definitiondf-fmtno 46494
[ApostolNT] p. 8Definitiondf-ppi 26840
[ApostolNT] p. 14Definitiondf-dvds 16202
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16217
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16241
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16236
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16230
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16232
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16218
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16219
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16224
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16258
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16260
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16262
[ApostolNT] p. 15Definitiondf-gcd 16440  dfgcd2 16492
[ApostolNT] p. 16Definitionisprm2 16623
[ApostolNT] p. 16Theorem 1.5coprmdvds 16594
[ApostolNT] p. 16Theorem 1.7prminf 16852
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16458
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16493
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16495
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16473
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16465
[ApostolNT] p. 17Theorem 1.8coprm 16652
[ApostolNT] p. 17Theorem 1.9euclemma 16654
[ApostolNT] p. 17Theorem 1.101arith2 16865
[ApostolNT] p. 18Theorem 1.13prmrec 16859
[ApostolNT] p. 19Theorem 1.14divalg 16350
[ApostolNT] p. 20Theorem 1.15eucalg 16528
[ApostolNT] p. 24Definitiondf-mu 26841
[ApostolNT] p. 25Definitiondf-phi 16703
[ApostolNT] p. 25Theorem 2.1musum 26931
[ApostolNT] p. 26Theorem 2.2phisum 16727
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16713
[ApostolNT] p. 28Theorem 2.5(c)phimul 16717
[ApostolNT] p. 32Definitiondf-vma 26838
[ApostolNT] p. 32Theorem 2.9muinv 26933
[ApostolNT] p. 32Theorem 2.10vmasum 26955
[ApostolNT] p. 38Remarkdf-sgm 26842
[ApostolNT] p. 38Definitiondf-sgm 26842
[ApostolNT] p. 75Definitiondf-chp 26839  df-cht 26837
[ApostolNT] p. 104Definitioncongr 16605
[ApostolNT] p. 106Remarkdvdsval3 16205
[ApostolNT] p. 106Definitionmoddvds 16212
[ApostolNT] p. 107Example 2mod2eq0even 16293
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16294
[ApostolNT] p. 107Example 4zmod1congr 13857
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13894
[ApostolNT] p. 107Theorem 5.2(c)modexp 14205
[ApostolNT] p. 108Theorem 5.3modmulconst 16235
[ApostolNT] p. 109Theorem 5.4cncongr1 16608
[ApostolNT] p. 109Theorem 5.6gcdmodi 17011
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16610
[ApostolNT] p. 113Theorem 5.17eulerth 16720
[ApostolNT] p. 113Theorem 5.18vfermltl 16738
[ApostolNT] p. 114Theorem 5.19fermltl 16721
[ApostolNT] p. 116Theorem 5.24wilthimp 26812
[ApostolNT] p. 179Definitiondf-lgs 27034  lgsprme0 27078
[ApostolNT] p. 180Example 11lgs 27079
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27055
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27070
[ApostolNT] p. 181Theorem 9.4m1lgs 27127
[ApostolNT] p. 181Theorem 9.52lgs 27146  2lgsoddprm 27155
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27113
[ApostolNT] p. 185Theorem 9.8lgsquad 27122
[ApostolNT] p. 188Definitiondf-lgs 27034  lgs1 27080
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27071
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27073
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27081
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27082
[Baer] p. 40Property (b)mapdord 40812
[Baer] p. 40Property (c)mapd11 40813
[Baer] p. 40Property (e)mapdin 40836  mapdlsm 40838
[Baer] p. 40Property (f)mapd0 40839
[Baer] p. 40Definition of projectivitydf-mapd 40799  mapd1o 40822
[Baer] p. 41Property (g)mapdat 40841
[Baer] p. 44Part (1)mapdpg 40880
[Baer] p. 45Part (2)hdmap1eq 40975  mapdheq 40902  mapdheq2 40903  mapdheq2biN 40904
[Baer] p. 45Part (3)baerlem3 40887
[Baer] p. 46Part (4)mapdheq4 40906  mapdheq4lem 40905
[Baer] p. 46Part (5)baerlem5a 40888  baerlem5abmN 40892  baerlem5amN 40890  baerlem5b 40889  baerlem5bmN 40891
[Baer] p. 47Part (6)hdmap1l6 40995  hdmap1l6a 40983  hdmap1l6e 40988  hdmap1l6f 40989  hdmap1l6g 40990  hdmap1l6lem1 40981  hdmap1l6lem2 40982  mapdh6N 40921  mapdh6aN 40909  mapdh6eN 40914  mapdh6fN 40915  mapdh6gN 40916  mapdh6lem1N 40907  mapdh6lem2N 40908
[Baer] p. 48Part 9hdmapval 41002
[Baer] p. 48Part 10hdmap10 41014
[Baer] p. 48Part 11hdmapadd 41017
[Baer] p. 48Part (6)hdmap1l6h 40991  mapdh6hN 40917
[Baer] p. 48Part (7)mapdh75cN 40927  mapdh75d 40928  mapdh75e 40926  mapdh75fN 40929  mapdh7cN 40923  mapdh7dN 40924  mapdh7eN 40922  mapdh7fN 40925
[Baer] p. 48Part (8)mapdh8 40962  mapdh8a 40949  mapdh8aa 40950  mapdh8ab 40951  mapdh8ac 40952  mapdh8ad 40953  mapdh8b 40954  mapdh8c 40955  mapdh8d 40957  mapdh8d0N 40956  mapdh8e 40958  mapdh8g 40959  mapdh8i 40960  mapdh8j 40961
[Baer] p. 48Part (9)mapdh9a 40963
[Baer] p. 48Equation 10mapdhvmap 40943
[Baer] p. 49Part 12hdmap11 41022  hdmapeq0 41018  hdmapf1oN 41039  hdmapneg 41020  hdmaprnN 41038  hdmaprnlem1N 41023  hdmaprnlem3N 41024  hdmaprnlem3uN 41025  hdmaprnlem4N 41027  hdmaprnlem6N 41028  hdmaprnlem7N 41029  hdmaprnlem8N 41030  hdmaprnlem9N 41031  hdmapsub 41021
[Baer] p. 49Part 14hdmap14lem1 41042  hdmap14lem10 41051  hdmap14lem1a 41040  hdmap14lem2N 41043  hdmap14lem2a 41041  hdmap14lem3 41044  hdmap14lem8 41049  hdmap14lem9 41050
[Baer] p. 50Part 14hdmap14lem11 41052  hdmap14lem12 41053  hdmap14lem13 41054  hdmap14lem14 41055  hdmap14lem15 41056  hgmapval 41061
[Baer] p. 50Part 15hgmapadd 41068  hgmapmul 41069  hgmaprnlem2N 41071  hgmapvs 41065
[Baer] p. 50Part 16hgmaprnN 41075
[Baer] p. 110Lemma 1hdmapip0com 41091
[Baer] p. 110Line 27hdmapinvlem1 41092
[Baer] p. 110Line 28hdmapinvlem2 41093
[Baer] p. 110Line 30hdmapinvlem3 41094
[Baer] p. 110Part 1.2hdmapglem5 41096  hgmapvv 41100
[Baer] p. 110Proposition 1hdmapinvlem4 41095
[Baer] p. 111Line 10hgmapvvlem1 41097
[Baer] p. 111Line 15hdmapg 41104  hdmapglem7 41103
[Bauer], p. 483Theorem 1.22irrexpq 26475  2irrexpqALT 26541
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2561
[BellMachover] p. 460Notationdf-mo 2532
[BellMachover] p. 460Definitionmo3 2556
[BellMachover] p. 461Axiom Extax-ext 2701
[BellMachover] p. 462Theorem 1.1axextmo 2705
[BellMachover] p. 463Axiom Repaxrep5 5290
[BellMachover] p. 463Scheme Sepax-sep 5298
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 36248  bm1.3ii 5301
[BellMachover] p. 466Problemaxpow2 5364
[BellMachover] p. 466Axiom Powaxpow3 5365
[BellMachover] p. 466Axiom Unionaxun2 7729
[BellMachover] p. 468Definitiondf-ord 6366
[BellMachover] p. 469Theorem 2.2(i)ordirr 6381
[BellMachover] p. 469Theorem 2.2(iii)onelon 6388
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6383
[BellMachover] p. 471Definition of Ndf-om 7858
[BellMachover] p. 471Problem 2.5(ii)uniordint 7791
[BellMachover] p. 471Definition of Limdf-lim 6368
[BellMachover] p. 472Axiom Infzfinf2 9639
[BellMachover] p. 473Theorem 2.8limom 7873
[BellMachover] p. 477Equation 3.1df-r1 9761
[BellMachover] p. 478Definitionrankval2 9815
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9779  r1ord3g 9776
[BellMachover] p. 480Axiom Regzfreg 9592
[BellMachover] p. 488Axiom ACac5 10474  dfac4 10119
[BellMachover] p. 490Definition of alephalephval3 10107
[BeltramettiCassinelli] p. 98Remarkatlatmstc 38492
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 31873
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 31915  chirredi 31914
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 31903
[Beran] p. 3Definition of joinsshjval3 30874
[Beran] p. 39Theorem 2.3(i)cmcm2 31136  cmcm2i 31113  cmcm2ii 31118  cmt2N 38423
[Beran] p. 40Theorem 2.3(iii)lecm 31137  lecmi 31122  lecmii 31123
[Beran] p. 45Theorem 3.4cmcmlem 31111
[Beran] p. 49Theorem 4.2cm2j 31140  cm2ji 31145  cm2mi 31146
[Beran] p. 95Definitiondf-sh 30727  issh2 30729
[Beran] p. 95Lemma 3.1(S5)his5 30606
[Beran] p. 95Lemma 3.1(S6)his6 30619
[Beran] p. 95Lemma 3.1(S7)his7 30610
[Beran] p. 95Lemma 3.2(S8)ho01i 31348
[Beran] p. 95Lemma 3.2(S9)hoeq1 31350
[Beran] p. 95Lemma 3.2(S10)ho02i 31349
[Beran] p. 95Lemma 3.2(S11)hoeq2 31351
[Beran] p. 95Postulate (S1)ax-his1 30602  his1i 30620
[Beran] p. 95Postulate (S2)ax-his2 30603
[Beran] p. 95Postulate (S3)ax-his3 30604
[Beran] p. 95Postulate (S4)ax-his4 30605
[Beran] p. 96Definition of normdf-hnorm 30488  dfhnorm2 30642  normval 30644
[Beran] p. 96Definition for Cauchy sequencehcau 30704
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30493
[Beran] p. 96Definition of complete subspaceisch3 30761
[Beran] p. 96Definition of convergedf-hlim 30492  hlimi 30708
[Beran] p. 97Theorem 3.3(i)norm-i-i 30653  norm-i 30649
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 30657  norm-ii 30658  normlem0 30629  normlem1 30630  normlem2 30631  normlem3 30632  normlem4 30633  normlem5 30634  normlem6 30635  normlem7 30636  normlem7tALT 30639
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 30659  norm-iii 30660
[Beran] p. 98Remark 3.4bcs 30701  bcsiALT 30699  bcsiHIL 30700
[Beran] p. 98Remark 3.4(B)normlem9at 30641  normpar 30675  normpari 30674
[Beran] p. 98Remark 3.4(C)normpyc 30666  normpyth 30665  normpythi 30662
[Beran] p. 99Remarklnfn0 31567  lnfn0i 31562  lnop0 31486  lnop0i 31490
[Beran] p. 99Theorem 3.5(i)nmcexi 31546  nmcfnex 31573  nmcfnexi 31571  nmcopex 31549  nmcopexi 31547
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 31574  nmcfnlbi 31572  nmcoplb 31550  nmcoplbi 31548
[Beran] p. 99Theorem 3.5(iii)lnfncon 31576  lnfnconi 31575  lnopcon 31555  lnopconi 31554
[Beran] p. 100Lemma 3.6normpar2i 30676
[Beran] p. 101Lemma 3.6norm3adifi 30673  norm3adifii 30668  norm3dif 30670  norm3difi 30667
[Beran] p. 102Theorem 3.7(i)chocunii 30821  pjhth 30913  pjhtheu 30914  pjpjhth 30945  pjpjhthi 30946  pjth 25187
[Beran] p. 102Theorem 3.7(ii)ococ 30926  ococi 30925
[Beran] p. 103Remark 3.8nlelchi 31581
[Beran] p. 104Theorem 3.9riesz3i 31582  riesz4 31584  riesz4i 31583
[Beran] p. 104Theorem 3.10cnlnadj 31599  cnlnadjeu 31598  cnlnadjeui 31597  cnlnadji 31596  cnlnadjlem1 31587  nmopadjlei 31608
[Beran] p. 106Theorem 3.11(i)adjeq0 31611
[Beran] p. 106Theorem 3.11(v)nmopadji 31610
[Beran] p. 106Theorem 3.11(ii)adjmul 31612
[Beran] p. 106Theorem 3.11(iv)adjadj 31456
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 31622  nmopcoadji 31621
[Beran] p. 106Theorem 3.11(iii)adjadd 31613
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 31623
[Beran] p. 106Theorem 3.11(viii)adjcoi 31620  pjadj2coi 31724  pjadjcoi 31681
[Beran] p. 107Definitiondf-ch 30741  isch2 30743
[Beran] p. 107Remark 3.12choccl 30826  isch3 30761  occl 30824  ocsh 30803  shoccl 30825  shocsh 30804
[Beran] p. 107Remark 3.12(B)ococin 30928
[Beran] p. 108Theorem 3.13chintcl 30852
[Beran] p. 109Property (i)pjadj2 31707  pjadj3 31708  pjadji 31205  pjadjii 31194
[Beran] p. 109Property (ii)pjidmco 31701  pjidmcoi 31697  pjidmi 31193
[Beran] p. 110Definition of projector orderingpjordi 31693
[Beran] p. 111Remarkho0val 31270  pjch1 31190
[Beran] p. 111Definitiondf-hfmul 31254  df-hfsum 31253  df-hodif 31252  df-homul 31251  df-hosum 31250
[Beran] p. 111Lemma 4.4(i)pjo 31191
[Beran] p. 111Lemma 4.4(ii)pjch 31214  pjchi 30952
[Beran] p. 111Lemma 4.4(iii)pjoc2 30959  pjoc2i 30958
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31200
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 31685  pjssmii 31201
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 31684
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 31683
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 31688
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 31686  pjssge0ii 31202
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 31687  pjdifnormii 31203
[Bobzien] p. 116Statement T3stoic3 1776
[Bobzien] p. 117Statement T2stoic2a 1774
[Bobzien] p. 117Statement T4stoic4a 1777
[Bobzien] p. 117Conclusion the contradictorystoic1a 1772
[Bogachev] p. 16Definition 1.5df-oms 33589
[Bogachev] p. 17Lemma 1.5.4omssubadd 33597
[Bogachev] p. 17Example 1.5.2omsmon 33595
[Bogachev] p. 41Definition 1.11.2df-carsg 33599
[Bogachev] p. 42Theorem 1.11.4carsgsiga 33619
[Bogachev] p. 116Definition 2.3.1df-itgm 33650  df-sitm 33628
[Bogachev] p. 118Chapter 2.4.4df-itgm 33650
[Bogachev] p. 118Definition 2.4.1df-sitg 33627
[Bollobas] p. 1Section I.1df-edg 28575  isuhgrop 28597  isusgrop 28689  isuspgrop 28688
[Bollobas] p. 2Section I.1df-subgr 28792  uhgrspan1 28827  uhgrspansubgr 28815
[Bollobas] p. 3Definitionisomuspgr 46800
[Bollobas] p. 3Section I.1cusgrsize 28978  df-cusgr 28936  df-nbgr 28857  fusgrmaxsize 28988
[Bollobas] p. 4Definitiondf-upwlks 46810  df-wlks 29123
[Bollobas] p. 4Section I.1finsumvtxdg2size 29074  finsumvtxdgeven 29076  fusgr1th 29075  fusgrvtxdgonume 29078  vtxdgoddnumeven 29077
[Bollobas] p. 5Notationdf-pths 29240
[Bollobas] p. 5Definitiondf-crcts 29310  df-cycls 29311  df-trls 29216  df-wlkson 29124
[Bollobas] p. 7Section I.1df-ushgr 28586
[BourbakiAlg1] p. 1Definition 1df-clintop 46876  df-cllaw 46862  df-mgm 18565  df-mgm2 46895
[BourbakiAlg1] p. 4Definition 5df-assintop 46877  df-asslaw 46864  df-sgrp 18644  df-sgrp2 46897
[BourbakiAlg1] p. 7Definition 8df-cmgm2 46896  df-comlaw 46863
[BourbakiAlg1] p. 12Definition 2df-mnd 18660
[BourbakiAlg1] p. 92Definition 1df-ring 20129
[BourbakiAlg1] p. 93Section I.8.1df-rng 20047
[BourbakiEns] p. Proposition 8fcof1 7287  fcofo 7288
[BourbakiTop1] p. Remarkxnegmnf 13193  xnegpnf 13192
[BourbakiTop1] p. Remark rexneg 13194
[BourbakiTop1] p. Remark 3ust0 23944  ustfilxp 23937
[BourbakiTop1] p. Axiom GT'tgpsubcn 23814
[BourbakiTop1] p. Criterionishmeo 23483
[BourbakiTop1] p. Example 1cstucnd 24009  iducn 24008  snfil 23588
[BourbakiTop1] p. Example 2neifil 23604
[BourbakiTop1] p. Theorem 1cnextcn 23791
[BourbakiTop1] p. Theorem 2ucnextcn 24029
[BourbakiTop1] p. Theorem 3df-hcmp 33235
[BourbakiTop1] p. Paragraph 3infil 23587
[BourbakiTop1] p. Definition 1df-ucn 24001  df-ust 23925  filintn0 23585  filn0 23586  istgp 23801  ucnprima 24007
[BourbakiTop1] p. Definition 2df-cfilu 24012
[BourbakiTop1] p. Definition 3df-cusp 24023  df-usp 23982  df-utop 23956  trust 23954
[BourbakiTop1] p. Definition 6df-pcmp 33134
[BourbakiTop1] p. Property V_issnei2 22840
[BourbakiTop1] p. Theorem 1(d)iscncl 22993
[BourbakiTop1] p. Condition F_Iustssel 23930
[BourbakiTop1] p. Condition U_Iustdiag 23933
[BourbakiTop1] p. Property V_iiinnei 22849
[BourbakiTop1] p. Property V_ivneiptopreu 22857  neissex 22851
[BourbakiTop1] p. Proposition 1neips 22837  neiss 22833  ucncn 24010  ustund 23946  ustuqtop 23971
[BourbakiTop1] p. Proposition 2cnpco 22991  neiptopreu 22857  utop2nei 23975  utop3cls 23976
[BourbakiTop1] p. Proposition 3fmucnd 24017  uspreg 23999  utopreg 23977
[BourbakiTop1] p. Proposition 4imasncld 23415  imasncls 23416  imasnopn 23414
[BourbakiTop1] p. Proposition 9cnpflf2 23724
[BourbakiTop1] p. Condition F_IIustincl 23932
[BourbakiTop1] p. Condition U_IIustinvel 23934
[BourbakiTop1] p. Property V_iiielnei 22835
[BourbakiTop1] p. Proposition 11cnextucn 24028
[BourbakiTop1] p. Condition F_IIbustbasel 23931
[BourbakiTop1] p. Condition U_IIIustexhalf 23935
[BourbakiTop1] p. Definition C'''df-cmp 23111
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23570
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22616
[BourbakiTop2] p. 195Definition 1df-ldlf 33131
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 45076
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 45078  stoweid 45077
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 45015  stoweidlem10 45024  stoweidlem14 45028  stoweidlem15 45029  stoweidlem35 45049  stoweidlem36 45050  stoweidlem37 45051  stoweidlem38 45052  stoweidlem40 45054  stoweidlem41 45055  stoweidlem43 45057  stoweidlem44 45058  stoweidlem46 45060  stoweidlem5 45019  stoweidlem50 45064  stoweidlem52 45066  stoweidlem53 45067  stoweidlem55 45069  stoweidlem56 45070
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 45037  stoweidlem24 45038  stoweidlem27 45041  stoweidlem28 45042  stoweidlem30 45044
[BrosowskiDeutsh] p. 91Proofstoweidlem34 45048  stoweidlem59 45073  stoweidlem60 45074
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 45059  stoweidlem49 45063  stoweidlem7 45021
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 45045  stoweidlem39 45053  stoweidlem42 45056  stoweidlem48 45062  stoweidlem51 45065  stoweidlem54 45068  stoweidlem57 45071  stoweidlem58 45072
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 45039
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 45031
[BrosowskiDeutsh] p. 92Proofstoweidlem11 45025  stoweidlem13 45027  stoweidlem26 45040  stoweidlem61 45075
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 45032
[Bruck] p. 1Section I.1df-clintop 46876  df-mgm 18565  df-mgm2 46895
[Bruck] p. 23Section II.1df-sgrp 18644  df-sgrp2 46897
[Bruck] p. 28Theorem 3.2dfgrp3 18958
[ChoquetDD] p. 2Definition of mappingdf-mpt 5231
[Church] p. 129Section II.24df-ifp 1060  dfifp2 1061
[Clemente] p. 10Definition ITnatded 29923
[Clemente] p. 10Definition I` `m,nnatded 29923
[Clemente] p. 11Definition E=>m,nnatded 29923
[Clemente] p. 11Definition I=>m,nnatded 29923
[Clemente] p. 11Definition E` `(1)natded 29923
[Clemente] p. 11Definition E` `(2)natded 29923
[Clemente] p. 12Definition E` `m,n,pnatded 29923
[Clemente] p. 12Definition I` `n(1)natded 29923
[Clemente] p. 12Definition I` `n(2)natded 29923
[Clemente] p. 13Definition I` `m,n,pnatded 29923
[Clemente] p. 14Proof 5.11natded 29923
[Clemente] p. 14Definition E` `nnatded 29923
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 29925  ex-natded5.2 29924
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 29928  ex-natded5.3 29927
[Clemente] p. 18Theorem 5.5ex-natded5.5 29930
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 29932  ex-natded5.7 29931
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 29934  ex-natded5.8 29933
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 29936  ex-natded5.13 29935
[Clemente] p. 32Definition I` `nnatded 29923
[Clemente] p. 32Definition E` `m,n,p,anatded 29923
[Clemente] p. 32Definition E` `n,tnatded 29923
[Clemente] p. 32Definition I` `n,tnatded 29923
[Clemente] p. 43Theorem 9.20ex-natded9.20 29937
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 29938
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 29940  ex-natded9.26 29939
[Cohen] p. 301Remarkrelogoprlem 26335
[Cohen] p. 301Property 2relogmul 26336  relogmuld 26369
[Cohen] p. 301Property 3relogdiv 26337  relogdivd 26370
[Cohen] p. 301Property 4relogexp 26340
[Cohen] p. 301Property 1alog1 26330
[Cohen] p. 301Property 1bloge 26331
[Cohen4] p. 348Observationrelogbcxpb 26528
[Cohen4] p. 349Propertyrelogbf 26532
[Cohen4] p. 352Definitionelogb 26511
[Cohen4] p. 361Property 2relogbmul 26518
[Cohen4] p. 361Property 3logbrec 26523  relogbdiv 26520
[Cohen4] p. 361Property 4relogbreexp 26516
[Cohen4] p. 361Property 6relogbexp 26521
[Cohen4] p. 361Property 1(a)logbid1 26509
[Cohen4] p. 361Property 1(b)logb1 26510
[Cohen4] p. 367Propertylogbchbase 26512
[Cohen4] p. 377Property 2logblt 26525
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 33582  sxbrsigalem4 33584
[Cohn] p. 81Section II.5acsdomd 18514  acsinfd 18513  acsinfdimd 18515  acsmap2d 18512  acsmapd 18511
[Cohn] p. 143Example 5.1.1sxbrsiga 33587
[Connell] p. 57Definitiondf-scmat 22213  df-scmatalt 47167
[Conway] p. 4Definitionslerec 27557
[Conway] p. 5Definitionaddsval 27684  addsval2 27685  df-adds 27682  df-muls 27802  df-negs 27735
[Conway] p. 7Theorem0slt1s 27567
[Conway] p. 16Theorem 0(i)ssltright 27603
[Conway] p. 16Theorem 0(ii)ssltleft 27602
[Conway] p. 16Theorem 0(iii)slerflex 27502
[Conway] p. 17Theorem 3addsass 27727  addsassd 27728  addscom 27688  addscomd 27689  addsrid 27686  addsridd 27687
[Conway] p. 17Definitiondf-0s 27562
[Conway] p. 17Theorem 4(ii)negnegs 27757
[Conway] p. 17Theorem 4(iii)negsid 27754  negsidd 27755
[Conway] p. 18Theorem 5sleadd1 27711  sleadd1d 27717
[Conway] p. 18Definitiondf-1s 27563
[Conway] p. 18Theorem 6(ii)negscl 27749  negscld 27750
[Conway] p. 18Theorem 6(iii)addscld 27702
[Conway] p. 19Theorem 7addsdi 27849  addsdid 27850  addsdird 27851  mulnegs1d 27854  mulnegs2d 27855  mulsass 27860  mulsassd 27861  mulscom 27834  mulscomd 27835
[Conway] p. 19Theorem 8(i)mulscl 27829  mulscld 27830
[Conway] p. 19Theorem 8(iii)slemuld 27833  sltmul 27831  sltmuld 27832
[Conway] p. 20Theorem 9mulsgt0 27839  mulsgt0d 27840
[Conway] p. 21Theorem 10(iv)precsex 27903
[Conway] p. 27Definitiondf-ons 27918  elons2 27924
[Conway] p. 27Theorem 14sltonex 27927
[Conway] p. 29Remarkmadebday 27631  newbday 27633  oldbday 27632
[Conway] p. 29Definitiondf-made 27579  df-new 27581  df-old 27580
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13830
[Crawley] p. 1Definition of posetdf-poset 18270
[Crawley] p. 107Theorem 13.2hlsupr 38560
[Crawley] p. 110Theorem 13.3arglem1N 39364  dalaw 39060
[Crawley] p. 111Theorem 13.4hlathil 41139
[Crawley] p. 111Definition of set Wdf-watsN 39164
[Crawley] p. 111Definition of dilationdf-dilN 39280  df-ldil 39278  isldil 39284
[Crawley] p. 111Definition of translationdf-ltrn 39279  df-trnN 39281  isltrn 39293  ltrnu 39295
[Crawley] p. 112Lemma Acdlema1N 38965  cdlema2N 38966  exatleN 38578
[Crawley] p. 112Lemma B1cvrat 38650  cdlemb 38968  cdlemb2 39215  cdlemb3 39780  idltrn 39324  l1cvat 38228  lhpat 39217  lhpat2 39219  lshpat 38229  ltrnel 39313  ltrnmw 39325
[Crawley] p. 112Lemma Ccdlemc1 39365  cdlemc2 39366  ltrnnidn 39348  trlat 39343  trljat1 39340  trljat2 39341  trljat3 39342  trlne 39359  trlnidat 39347  trlnle 39360
[Crawley] p. 112Definition of automorphismdf-pautN 39165
[Crawley] p. 113Lemma Ccdlemc 39371  cdlemc3 39367  cdlemc4 39368
[Crawley] p. 113Lemma Dcdlemd 39381  cdlemd1 39372  cdlemd2 39373  cdlemd3 39374  cdlemd4 39375  cdlemd5 39376  cdlemd6 39377  cdlemd7 39378  cdlemd8 39379  cdlemd9 39380  cdleme31sde 39559  cdleme31se 39556  cdleme31se2 39557  cdleme31snd 39560  cdleme32a 39615  cdleme32b 39616  cdleme32c 39617  cdleme32d 39618  cdleme32e 39619  cdleme32f 39620  cdleme32fva 39611  cdleme32fva1 39612  cdleme32fvcl 39614  cdleme32le 39621  cdleme48fv 39673  cdleme4gfv 39681  cdleme50eq 39715  cdleme50f 39716  cdleme50f1 39717  cdleme50f1o 39720  cdleme50laut 39721  cdleme50ldil 39722  cdleme50lebi 39714  cdleme50rn 39719  cdleme50rnlem 39718  cdlemeg49le 39685  cdlemeg49lebilem 39713
[Crawley] p. 113Lemma Ecdleme 39734  cdleme00a 39383  cdleme01N 39395  cdleme02N 39396  cdleme0a 39385  cdleme0aa 39384  cdleme0b 39386  cdleme0c 39387  cdleme0cp 39388  cdleme0cq 39389  cdleme0dN 39390  cdleme0e 39391  cdleme0ex1N 39397  cdleme0ex2N 39398  cdleme0fN 39392  cdleme0gN 39393  cdleme0moN 39399  cdleme1 39401  cdleme10 39428  cdleme10tN 39432  cdleme11 39444  cdleme11a 39434  cdleme11c 39435  cdleme11dN 39436  cdleme11e 39437  cdleme11fN 39438  cdleme11g 39439  cdleme11h 39440  cdleme11j 39441  cdleme11k 39442  cdleme11l 39443  cdleme12 39445  cdleme13 39446  cdleme14 39447  cdleme15 39452  cdleme15a 39448  cdleme15b 39449  cdleme15c 39450  cdleme15d 39451  cdleme16 39459  cdleme16aN 39433  cdleme16b 39453  cdleme16c 39454  cdleme16d 39455  cdleme16e 39456  cdleme16f 39457  cdleme16g 39458  cdleme19a 39477  cdleme19b 39478  cdleme19c 39479  cdleme19d 39480  cdleme19e 39481  cdleme19f 39482  cdleme1b 39400  cdleme2 39402  cdleme20aN 39483  cdleme20bN 39484  cdleme20c 39485  cdleme20d 39486  cdleme20e 39487  cdleme20f 39488  cdleme20g 39489  cdleme20h 39490  cdleme20i 39491  cdleme20j 39492  cdleme20k 39493  cdleme20l 39496  cdleme20l1 39494  cdleme20l2 39495  cdleme20m 39497  cdleme20y 39476  cdleme20zN 39475  cdleme21 39511  cdleme21d 39504  cdleme21e 39505  cdleme22a 39514  cdleme22aa 39513  cdleme22b 39515  cdleme22cN 39516  cdleme22d 39517  cdleme22e 39518  cdleme22eALTN 39519  cdleme22f 39520  cdleme22f2 39521  cdleme22g 39522  cdleme23a 39523  cdleme23b 39524  cdleme23c 39525  cdleme26e 39533  cdleme26eALTN 39535  cdleme26ee 39534  cdleme26f 39537  cdleme26f2 39539  cdleme26f2ALTN 39538  cdleme26fALTN 39536  cdleme27N 39543  cdleme27a 39541  cdleme27cl 39540  cdleme28c 39546  cdleme3 39411  cdleme30a 39552  cdleme31fv 39564  cdleme31fv1 39565  cdleme31fv1s 39566  cdleme31fv2 39567  cdleme31id 39568  cdleme31sc 39558  cdleme31sdnN 39561  cdleme31sn 39554  cdleme31sn1 39555  cdleme31sn1c 39562  cdleme31sn2 39563  cdleme31so 39553  cdleme35a 39622  cdleme35b 39624  cdleme35c 39625  cdleme35d 39626  cdleme35e 39627  cdleme35f 39628  cdleme35fnpq 39623  cdleme35g 39629  cdleme35h 39630  cdleme35h2 39631  cdleme35sn2aw 39632  cdleme35sn3a 39633  cdleme36a 39634  cdleme36m 39635  cdleme37m 39636  cdleme38m 39637  cdleme38n 39638  cdleme39a 39639  cdleme39n 39640  cdleme3b 39403  cdleme3c 39404  cdleme3d 39405  cdleme3e 39406  cdleme3fN 39407  cdleme3fa 39410  cdleme3g 39408  cdleme3h 39409  cdleme4 39412  cdleme40m 39641  cdleme40n 39642  cdleme40v 39643  cdleme40w 39644  cdleme41fva11 39651  cdleme41sn3aw 39648  cdleme41sn4aw 39649  cdleme41snaw 39650  cdleme42a 39645  cdleme42b 39652  cdleme42c 39646  cdleme42d 39647  cdleme42e 39653  cdleme42f 39654  cdleme42g 39655  cdleme42h 39656  cdleme42i 39657  cdleme42k 39658  cdleme42ke 39659  cdleme42keg 39660  cdleme42mN 39661  cdleme42mgN 39662  cdleme43aN 39663  cdleme43bN 39664  cdleme43cN 39665  cdleme43dN 39666  cdleme5 39414  cdleme50ex 39733  cdleme50ltrn 39731  cdleme51finvN 39730  cdleme51finvfvN 39729  cdleme51finvtrN 39732  cdleme6 39415  cdleme7 39423  cdleme7a 39417  cdleme7aa 39416  cdleme7b 39418  cdleme7c 39419  cdleme7d 39420  cdleme7e 39421  cdleme7ga 39422  cdleme8 39424  cdleme8tN 39429  cdleme9 39427  cdleme9a 39425  cdleme9b 39426  cdleme9tN 39431  cdleme9taN 39430  cdlemeda 39472  cdlemedb 39471  cdlemednpq 39473  cdlemednuN 39474  cdlemefr27cl 39577  cdlemefr32fva1 39584  cdlemefr32fvaN 39583  cdlemefrs32fva 39574  cdlemefrs32fva1 39575  cdlemefs27cl 39587  cdlemefs32fva1 39597  cdlemefs32fvaN 39596  cdlemesner 39470  cdlemeulpq 39394
[Crawley] p. 114Lemma E4atex 39250  4atexlem7 39249  cdleme0nex 39464  cdleme17a 39460  cdleme17c 39462  cdleme17d 39672  cdleme17d1 39463  cdleme17d2 39669  cdleme18a 39465  cdleme18b 39466  cdleme18c 39467  cdleme18d 39469  cdleme4a 39413
[Crawley] p. 115Lemma Ecdleme21a 39499  cdleme21at 39502  cdleme21b 39500  cdleme21c 39501  cdleme21ct 39503  cdleme21f 39506  cdleme21g 39507  cdleme21h 39508  cdleme21i 39509  cdleme22gb 39468
[Crawley] p. 116Lemma Fcdlemf 39737  cdlemf1 39735  cdlemf2 39736
[Crawley] p. 116Lemma Gcdlemftr1 39741  cdlemg16 39831  cdlemg28 39878  cdlemg28a 39867  cdlemg28b 39877  cdlemg3a 39771  cdlemg42 39903  cdlemg43 39904  cdlemg44 39907  cdlemg44a 39905  cdlemg46 39909  cdlemg47 39910  cdlemg9 39808  ltrnco 39893  ltrncom 39912  tgrpabl 39925  trlco 39901
[Crawley] p. 116Definition of Gdf-tgrp 39917
[Crawley] p. 117Lemma Gcdlemg17 39851  cdlemg17b 39836
[Crawley] p. 117Definition of Edf-edring-rN 39930  df-edring 39931
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 39934
[Crawley] p. 118Remarktendopltp 39954
[Crawley] p. 118Lemma Hcdlemh 39991  cdlemh1 39989  cdlemh2 39990
[Crawley] p. 118Lemma Icdlemi 39994  cdlemi1 39992  cdlemi2 39993
[Crawley] p. 118Lemma Jcdlemj1 39995  cdlemj2 39996  cdlemj3 39997  tendocan 39998
[Crawley] p. 118Lemma Kcdlemk 40148  cdlemk1 40005  cdlemk10 40017  cdlemk11 40023  cdlemk11t 40120  cdlemk11ta 40103  cdlemk11tb 40105  cdlemk11tc 40119  cdlemk11u-2N 40063  cdlemk11u 40045  cdlemk12 40024  cdlemk12u-2N 40064  cdlemk12u 40046  cdlemk13-2N 40050  cdlemk13 40026  cdlemk14-2N 40052  cdlemk14 40028  cdlemk15-2N 40053  cdlemk15 40029  cdlemk16-2N 40054  cdlemk16 40031  cdlemk16a 40030  cdlemk17-2N 40055  cdlemk17 40032  cdlemk18-2N 40060  cdlemk18-3N 40074  cdlemk18 40042  cdlemk19-2N 40061  cdlemk19 40043  cdlemk19u 40144  cdlemk1u 40033  cdlemk2 40006  cdlemk20-2N 40066  cdlemk20 40048  cdlemk21-2N 40065  cdlemk21N 40047  cdlemk22-3 40075  cdlemk22 40067  cdlemk23-3 40076  cdlemk24-3 40077  cdlemk25-3 40078  cdlemk26-3 40080  cdlemk26b-3 40079  cdlemk27-3 40081  cdlemk28-3 40082  cdlemk29-3 40085  cdlemk3 40007  cdlemk30 40068  cdlemk31 40070  cdlemk32 40071  cdlemk33N 40083  cdlemk34 40084  cdlemk35 40086  cdlemk36 40087  cdlemk37 40088  cdlemk38 40089  cdlemk39 40090  cdlemk39u 40142  cdlemk4 40008  cdlemk41 40094  cdlemk42 40115  cdlemk42yN 40118  cdlemk43N 40137  cdlemk45 40121  cdlemk46 40122  cdlemk47 40123  cdlemk48 40124  cdlemk49 40125  cdlemk5 40010  cdlemk50 40126  cdlemk51 40127  cdlemk52 40128  cdlemk53 40131  cdlemk54 40132  cdlemk55 40135  cdlemk55u 40140  cdlemk56 40145  cdlemk5a 40009  cdlemk5auN 40034  cdlemk5u 40035  cdlemk6 40011  cdlemk6u 40036  cdlemk7 40022  cdlemk7u-2N 40062  cdlemk7u 40044  cdlemk8 40012  cdlemk9 40013  cdlemk9bN 40014  cdlemki 40015  cdlemkid 40110  cdlemkj-2N 40056  cdlemkj 40037  cdlemksat 40020  cdlemksel 40019  cdlemksv 40018  cdlemksv2 40021  cdlemkuat 40040  cdlemkuel-2N 40058  cdlemkuel-3 40072  cdlemkuel 40039  cdlemkuv-2N 40057  cdlemkuv2-2 40059  cdlemkuv2-3N 40073  cdlemkuv2 40041  cdlemkuvN 40038  cdlemkvcl 40016  cdlemky 40100  cdlemkyyN 40136  tendoex 40149
[Crawley] p. 120Remarkdva1dim 40159
[Crawley] p. 120Lemma Lcdleml1N 40150  cdleml2N 40151  cdleml3N 40152  cdleml4N 40153  cdleml5N 40154  cdleml6 40155  cdleml7 40156  cdleml8 40157  cdleml9 40158  dia1dim 40235
[Crawley] p. 120Lemma Mdia11N 40222  diaf11N 40223  dialss 40220  diaord 40221  dibf11N 40335  djajN 40311
[Crawley] p. 120Definition of isomorphism mapdiaval 40206
[Crawley] p. 121Lemma Mcdlemm10N 40292  dia2dimlem1 40238  dia2dimlem2 40239  dia2dimlem3 40240  dia2dimlem4 40241  dia2dimlem5 40242  diaf1oN 40304  diarnN 40303  dvheveccl 40286  dvhopN 40290
[Crawley] p. 121Lemma Ncdlemn 40386  cdlemn10 40380  cdlemn11 40385  cdlemn11a 40381  cdlemn11b 40382  cdlemn11c 40383  cdlemn11pre 40384  cdlemn2 40369  cdlemn2a 40370  cdlemn3 40371  cdlemn4 40372  cdlemn4a 40373  cdlemn5 40375  cdlemn5pre 40374  cdlemn6 40376  cdlemn7 40377  cdlemn8 40378  cdlemn9 40379  diclspsn 40368
[Crawley] p. 121Definition of phi(q)df-dic 40347
[Crawley] p. 122Lemma Ndih11 40439  dihf11 40441  dihjust 40391  dihjustlem 40390  dihord 40438  dihord1 40392  dihord10 40397  dihord11b 40396  dihord11c 40398  dihord2 40401  dihord2a 40393  dihord2b 40394  dihord2cN 40395  dihord2pre 40399  dihord2pre2 40400  dihordlem6 40387  dihordlem7 40388  dihordlem7b 40389
[Crawley] p. 122Definition of isomorphism mapdihffval 40404  dihfval 40405  dihval 40406
[Diestel] p. 3Section 1.1df-cusgr 28936  df-nbgr 28857
[Diestel] p. 4Section 1.1df-subgr 28792  uhgrspan1 28827  uhgrspansubgr 28815
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29078  vtxdgoddnumeven 29077
[Diestel] p. 27Section 1.10df-ushgr 28586
[EGA] p. 80Notation 1.1.1rspecval 33142
[EGA] p. 80Proposition 1.1.2zartop 33154
[EGA] p. 80Proposition 1.1.2(i)zarcls0 33146  zarcls1 33147
[EGA] p. 81Corollary 1.1.8zart0 33157
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 33160
[EGA], p. 83Corollary 1.2.3rhmpreimacn 33163
[Eisenberg] p. 67Definition 5.3df-dif 3950
[Eisenberg] p. 82Definition 6.3dfom3 9644
[Eisenberg] p. 125Definition 8.21df-map 8824
[Eisenberg] p. 216Example 13.2(4)omenps 9652
[Eisenberg] p. 310Theorem 19.8cardprc 9977
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10552
[Enderton] p. 18Axiom of Empty Setaxnul 5304
[Enderton] p. 19Definitiondf-tp 4632
[Enderton] p. 26Exercise 5unissb 4942
[Enderton] p. 26Exercise 10pwel 5378
[Enderton] p. 28Exercise 7(b)pwun 5571
[Enderton] p. 30Theorem "Distributive laws"iinin1 5081  iinin2 5080  iinun2 5075  iunin1 5074  iunin1f 32056  iunin2 5073  uniin1 32050  uniin2 32051
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5079  iundif2 5076
[Enderton] p. 32Exercise 20unineq 4276
[Enderton] p. 33Exercise 23iinuni 5100
[Enderton] p. 33Exercise 25iununi 5101
[Enderton] p. 33Exercise 24(a)iinpw 5108
[Enderton] p. 33Exercise 24(b)iunpw 7760  iunpwss 5109
[Enderton] p. 36Definitionopthwiener 5513
[Enderton] p. 38Exercise 6(a)unipw 5449
[Enderton] p. 38Exercise 6(b)pwuni 4948
[Enderton] p. 41Lemma 3Dopeluu 5469  rnex 7905  rnexg 7897
[Enderton] p. 41Exercise 8dmuni 5913  rnuni 6147
[Enderton] p. 42Definition of a functiondffun7 6574  dffun8 6575
[Enderton] p. 43Definition of function valuefunfv2 6978
[Enderton] p. 43Definition of single-rootedfuncnv 6616
[Enderton] p. 44Definition (d)dfima2 6060  dfima3 6061
[Enderton] p. 47Theorem 3Hfvco2 6987
[Enderton] p. 49Axiom of Choice (first form)ac7 10470  ac7g 10471  df-ac 10113  dfac2 10128  dfac2a 10126  dfac2b 10127  dfac3 10118  dfac7 10129
[Enderton] p. 50Theorem 3K(a)imauni 7247
[Enderton] p. 52Definitiondf-map 8824
[Enderton] p. 53Exercise 21coass 6263
[Enderton] p. 53Exercise 27dmco 6252
[Enderton] p. 53Exercise 14(a)funin 6623
[Enderton] p. 53Exercise 22(a)imass2 6100
[Enderton] p. 54Remarkixpf 8916  ixpssmap 8928
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8894
[Enderton] p. 55Axiom of Choice (second form)ac9 10480  ac9s 10490
[Enderton] p. 56Theorem 3Meqvrelref 37783  erref 8725
[Enderton] p. 57Lemma 3Neqvrelthi 37786  erthi 8756
[Enderton] p. 57Definitiondf-ec 8707
[Enderton] p. 58Definitiondf-qs 8711
[Enderton] p. 61Exercise 35df-ec 8707
[Enderton] p. 65Exercise 56(a)dmun 5909
[Enderton] p. 68Definition of successordf-suc 6369
[Enderton] p. 71Definitiondf-tr 5265  dftr4 5271
[Enderton] p. 72Theorem 4Eunisuc 6442  unisucg 6441
[Enderton] p. 73Exercise 6unisuc 6442  unisucg 6441
[Enderton] p. 73Exercise 5(a)truni 5280
[Enderton] p. 73Exercise 5(b)trint 5282  trintALT 43944
[Enderton] p. 79Theorem 4I(A1)nna0 8606
[Enderton] p. 79Theorem 4I(A2)nnasuc 8608  onasuc 8530
[Enderton] p. 79Definition of operation valuedf-ov 7414
[Enderton] p. 80Theorem 4J(A1)nnm0 8607
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8609  onmsuc 8531
[Enderton] p. 81Theorem 4K(1)nnaass 8624
[Enderton] p. 81Theorem 4K(2)nna0r 8611  nnacom 8619
[Enderton] p. 81Theorem 4K(3)nndi 8625
[Enderton] p. 81Theorem 4K(4)nnmass 8626
[Enderton] p. 81Theorem 4K(5)nnmcom 8628
[Enderton] p. 82Exercise 16nnm0r 8612  nnmsucr 8627
[Enderton] p. 88Exercise 23nnaordex 8640
[Enderton] p. 129Definitiondf-en 8942
[Enderton] p. 132Theorem 6B(b)canth 7364
[Enderton] p. 133Exercise 1xpomen 10012
[Enderton] p. 133Exercise 2qnnen 16160
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9212
[Enderton] p. 135Corollary 6Cphp3 9214
[Enderton] p. 136Corollary 6Enneneq 9211
[Enderton] p. 136Corollary 6D(a)pssinf 9258
[Enderton] p. 136Corollary 6D(b)ominf 9260
[Enderton] p. 137Lemma 6Fpssnn 9170
[Enderton] p. 138Corollary 6Gssfi 9175
[Enderton] p. 139Theorem 6H(c)mapen 9143
[Enderton] p. 142Theorem 6I(3)xpdjuen 10176
[Enderton] p. 142Theorem 6I(4)mapdjuen 10177
[Enderton] p. 143Theorem 6Jdju0en 10172  dju1en 10168
[Enderton] p. 144Exercise 13iunfi 9342  unifi 9343  unifi2 9344
[Enderton] p. 144Corollary 6Kundif2 4475  unfi 9174  unfi2 9317
[Enderton] p. 145Figure 38ffoss 7934
[Enderton] p. 145Definitiondf-dom 8943
[Enderton] p. 146Example 1domen 8959  domeng 8960
[Enderton] p. 146Example 3nndomo 9235  nnsdom 9651  nnsdomg 9304
[Enderton] p. 149Theorem 6L(a)djudom2 10180
[Enderton] p. 149Theorem 6L(c)mapdom1 9144  xpdom1 9073  xpdom1g 9071  xpdom2g 9070
[Enderton] p. 149Theorem 6L(d)mapdom2 9150
[Enderton] p. 151Theorem 6Mzorn 10504  zorng 10501
[Enderton] p. 151Theorem 6M(4)ac8 10489  dfac5 10125
[Enderton] p. 159Theorem 6Qunictb 10572
[Enderton] p. 164Exampleinfdif 10206
[Enderton] p. 168Definitiondf-po 5587
[Enderton] p. 192Theorem 7M(a)oneli 6477
[Enderton] p. 192Theorem 7M(b)ontr1 6409
[Enderton] p. 192Theorem 7M(c)onirri 6476
[Enderton] p. 193Corollary 7N(b)0elon 6417
[Enderton] p. 193Corollary 7N(c)onsuci 7829
[Enderton] p. 193Corollary 7N(d)ssonunii 7770
[Enderton] p. 194Remarkonprc 7767
[Enderton] p. 194Exercise 16suc11 6470
[Enderton] p. 197Definitiondf-card 9936
[Enderton] p. 197Theorem 7Pcarden 10548
[Enderton] p. 200Exercise 25tfis 7846
[Enderton] p. 202Lemma 7Tr1tr 9773
[Enderton] p. 202Definitiondf-r1 9761
[Enderton] p. 202Theorem 7Qr1val1 9783
[Enderton] p. 204Theorem 7V(b)rankval4 9864
[Enderton] p. 206Theorem 7X(b)en2lp 9603
[Enderton] p. 207Exercise 30rankpr 9854  rankprb 9848  rankpw 9840  rankpwi 9820  rankuniss 9863
[Enderton] p. 207Exercise 34opthreg 9615
[Enderton] p. 208Exercise 35suc11reg 9616
[Enderton] p. 212Definition of alephalephval3 10107
[Enderton] p. 213Theorem 8A(a)alephord2 10073
[Enderton] p. 213Theorem 8A(b)cardalephex 10087
[Enderton] p. 218Theorem Schema 8Eonfununi 8343
[Enderton] p. 222Definition of kardkarden 9892  kardex 9891
[Enderton] p. 238Theorem 8Roeoa 8599
[Enderton] p. 238Theorem 8Soeoe 8601
[Enderton] p. 240Exercise 25oarec 8564
[Enderton] p. 257Definition of cofinalitycflm 10247
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17590
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17536
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18510  mrieqv2d 17587  mrieqvd 17586
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17591
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17596  mreexexlem2d 17593
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18516  mreexfidimd 17598
[Frege1879] p. 11Statementdf3or2 42821
[Frege1879] p. 12Statementdf3an2 42822  dfxor4 42819  dfxor5 42820
[Frege1879] p. 26Axiom 1ax-frege1 42843
[Frege1879] p. 26Axiom 2ax-frege2 42844
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 42848
[Frege1879] p. 31Proposition 4frege4 42852
[Frege1879] p. 32Proposition 5frege5 42853
[Frege1879] p. 33Proposition 6frege6 42859
[Frege1879] p. 34Proposition 7frege7 42861
[Frege1879] p. 35Axiom 8ax-frege8 42862  axfrege8 42860
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 36629
[Frege1879] p. 35Proposition 9frege9 42865
[Frege1879] p. 36Proposition 10frege10 42873
[Frege1879] p. 36Proposition 11frege11 42867
[Frege1879] p. 37Proposition 12frege12 42866
[Frege1879] p. 37Proposition 13frege13 42875
[Frege1879] p. 37Proposition 14frege14 42876
[Frege1879] p. 38Proposition 15frege15 42879
[Frege1879] p. 38Proposition 16frege16 42869
[Frege1879] p. 39Proposition 17frege17 42874
[Frege1879] p. 39Proposition 18frege18 42871
[Frege1879] p. 39Proposition 19frege19 42877
[Frege1879] p. 40Proposition 20frege20 42881
[Frege1879] p. 40Proposition 21frege21 42880
[Frege1879] p. 41Proposition 22frege22 42872
[Frege1879] p. 42Proposition 23frege23 42878
[Frege1879] p. 42Proposition 24frege24 42868
[Frege1879] p. 42Proposition 25frege25 42870  rp-frege25 42858
[Frege1879] p. 42Proposition 26frege26 42863
[Frege1879] p. 43Axiom 28ax-frege28 42883
[Frege1879] p. 43Proposition 27frege27 42864
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 42884
[Frege1879] p. 44Axiom 31ax-frege31 42887  axfrege31 42886
[Frege1879] p. 44Proposition 30frege30 42885
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 42888
[Frege1879] p. 44Proposition 33frege33 42889
[Frege1879] p. 45Proposition 34frege34 42890
[Frege1879] p. 45Proposition 35frege35 42891
[Frege1879] p. 45Proposition 36frege36 42892
[Frege1879] p. 46Proposition 37frege37 42893
[Frege1879] p. 46Proposition 38frege38 42894
[Frege1879] p. 46Proposition 39frege39 42895
[Frege1879] p. 46Proposition 40frege40 42896
[Frege1879] p. 47Axiom 41ax-frege41 42898  axfrege41 42897
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 42899
[Frege1879] p. 47Proposition 43frege43 42900
[Frege1879] p. 47Proposition 44frege44 42901
[Frege1879] p. 47Proposition 45frege45 42902
[Frege1879] p. 48Proposition 46frege46 42903
[Frege1879] p. 48Proposition 47frege47 42904
[Frege1879] p. 49Proposition 48frege48 42905
[Frege1879] p. 49Proposition 49frege49 42906
[Frege1879] p. 49Proposition 50frege50 42907
[Frege1879] p. 50Axiom 52ax-frege52a 42910  ax-frege52c 42941  frege52aid 42911  frege52b 42942
[Frege1879] p. 50Axiom 54ax-frege54a 42915  ax-frege54c 42945  frege54b 42946
[Frege1879] p. 50Proposition 51frege51 42908
[Frege1879] p. 50Proposition 52dfsbcq 3778
[Frege1879] p. 50Proposition 53frege53a 42913  frege53aid 42912  frege53b 42943  frege53c 42967
[Frege1879] p. 50Proposition 54biid 260  eqid 2730
[Frege1879] p. 50Proposition 55frege55a 42921  frege55aid 42918  frege55b 42950  frege55c 42971  frege55cor1a 42922  frege55lem2a 42920  frege55lem2b 42949  frege55lem2c 42970
[Frege1879] p. 50Proposition 56frege56a 42924  frege56aid 42923  frege56b 42951  frege56c 42972
[Frege1879] p. 51Axiom 58ax-frege58a 42928  ax-frege58b 42954  frege58bid 42955  frege58c 42974
[Frege1879] p. 51Proposition 57frege57a 42926  frege57aid 42925  frege57b 42952  frege57c 42973
[Frege1879] p. 51Proposition 58spsbc 3789
[Frege1879] p. 51Proposition 59frege59a 42930  frege59b 42957  frege59c 42975
[Frege1879] p. 52Proposition 60frege60a 42931  frege60b 42958  frege60c 42976
[Frege1879] p. 52Proposition 61frege61a 42932  frege61b 42959  frege61c 42977
[Frege1879] p. 52Proposition 62frege62a 42933  frege62b 42960  frege62c 42978
[Frege1879] p. 52Proposition 63frege63a 42934  frege63b 42961  frege63c 42979
[Frege1879] p. 53Proposition 64frege64a 42935  frege64b 42962  frege64c 42980
[Frege1879] p. 53Proposition 65frege65a 42936  frege65b 42963  frege65c 42981
[Frege1879] p. 54Proposition 66frege66a 42937  frege66b 42964  frege66c 42982
[Frege1879] p. 54Proposition 67frege67a 42938  frege67b 42965  frege67c 42983
[Frege1879] p. 54Proposition 68frege68a 42939  frege68b 42966  frege68c 42984
[Frege1879] p. 55Definition 69dffrege69 42985
[Frege1879] p. 58Proposition 70frege70 42986
[Frege1879] p. 59Proposition 71frege71 42987
[Frege1879] p. 59Proposition 72frege72 42988
[Frege1879] p. 59Proposition 73frege73 42989
[Frege1879] p. 60Definition 76dffrege76 42992
[Frege1879] p. 60Proposition 74frege74 42990
[Frege1879] p. 60Proposition 75frege75 42991
[Frege1879] p. 62Proposition 77frege77 42993  frege77d 42799
[Frege1879] p. 63Proposition 78frege78 42994
[Frege1879] p. 63Proposition 79frege79 42995
[Frege1879] p. 63Proposition 80frege80 42996
[Frege1879] p. 63Proposition 81frege81 42997  frege81d 42800
[Frege1879] p. 64Proposition 82frege82 42998
[Frege1879] p. 65Proposition 83frege83 42999  frege83d 42801
[Frege1879] p. 65Proposition 84frege84 43000
[Frege1879] p. 66Proposition 85frege85 43001
[Frege1879] p. 66Proposition 86frege86 43002
[Frege1879] p. 66Proposition 87frege87 43003  frege87d 42803
[Frege1879] p. 67Proposition 88frege88 43004
[Frege1879] p. 68Proposition 89frege89 43005
[Frege1879] p. 68Proposition 90frege90 43006
[Frege1879] p. 68Proposition 91frege91 43007  frege91d 42804
[Frege1879] p. 69Proposition 92frege92 43008
[Frege1879] p. 70Proposition 93frege93 43009
[Frege1879] p. 70Proposition 94frege94 43010
[Frege1879] p. 70Proposition 95frege95 43011
[Frege1879] p. 71Definition 99dffrege99 43015
[Frege1879] p. 71Proposition 96frege96 43012  frege96d 42802
[Frege1879] p. 71Proposition 97frege97 43013  frege97d 42805
[Frege1879] p. 71Proposition 98frege98 43014  frege98d 42806
[Frege1879] p. 72Proposition 100frege100 43016
[Frege1879] p. 72Proposition 101frege101 43017
[Frege1879] p. 72Proposition 102frege102 43018  frege102d 42807
[Frege1879] p. 73Proposition 103frege103 43019
[Frege1879] p. 73Proposition 104frege104 43020
[Frege1879] p. 73Proposition 105frege105 43021
[Frege1879] p. 73Proposition 106frege106 43022  frege106d 42808
[Frege1879] p. 74Proposition 107frege107 43023
[Frege1879] p. 74Proposition 108frege108 43024  frege108d 42809
[Frege1879] p. 74Proposition 109frege109 43025  frege109d 42810
[Frege1879] p. 75Proposition 110frege110 43026
[Frege1879] p. 75Proposition 111frege111 43027  frege111d 42812
[Frege1879] p. 76Proposition 112frege112 43028
[Frege1879] p. 76Proposition 113frege113 43029
[Frege1879] p. 76Proposition 114frege114 43030  frege114d 42811
[Frege1879] p. 77Definition 115dffrege115 43031
[Frege1879] p. 77Proposition 116frege116 43032
[Frege1879] p. 78Proposition 117frege117 43033
[Frege1879] p. 78Proposition 118frege118 43034
[Frege1879] p. 78Proposition 119frege119 43035
[Frege1879] p. 78Proposition 120frege120 43036
[Frege1879] p. 79Proposition 121frege121 43037
[Frege1879] p. 79Proposition 122frege122 43038  frege122d 42813
[Frege1879] p. 79Proposition 123frege123 43039
[Frege1879] p. 80Proposition 124frege124 43040  frege124d 42814
[Frege1879] p. 81Proposition 125frege125 43041
[Frege1879] p. 81Proposition 126frege126 43042  frege126d 42815
[Frege1879] p. 82Proposition 127frege127 43043
[Frege1879] p. 83Proposition 128frege128 43044
[Frege1879] p. 83Proposition 129frege129 43045  frege129d 42816
[Frege1879] p. 84Proposition 130frege130 43046
[Frege1879] p. 85Proposition 131frege131 43047  frege131d 42817
[Frege1879] p. 86Proposition 132frege132 43048
[Frege1879] p. 86Proposition 133frege133 43049  frege133d 42818
[Fremlin1] p. 13Definition 111G (b)df-salgen 45327
[Fremlin1] p. 13Definition 111G (d)borelmbl 45650
[Fremlin1] p. 13Proposition 111G (b)salgenss 45350
[Fremlin1] p. 14Definition 112Aismea 45465
[Fremlin1] p. 15Remark 112B (d)psmeasure 45485
[Fremlin1] p. 15Property 112C (a)meadjun 45476  meadjunre 45490
[Fremlin1] p. 15Property 112C (b)meassle 45477
[Fremlin1] p. 15Property 112C (c)meaunle 45478
[Fremlin1] p. 16Property 112C (d)iundjiun 45474  meaiunle 45483  meaiunlelem 45482
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 45495  meaiuninc2 45496  meaiuninc3 45499  meaiuninc3v 45498  meaiunincf 45497  meaiuninclem 45494
[Fremlin1] p. 16Proposition 112C (f)meaiininc 45501  meaiininc2 45502  meaiininclem 45500
[Fremlin1] p. 19Theorem 113Ccaragen0 45520  caragendifcl 45528  caratheodory 45542  omelesplit 45532
[Fremlin1] p. 19Definition 113Aisome 45508  isomennd 45545  isomenndlem 45544
[Fremlin1] p. 19Remark 113B (c)omeunle 45530
[Fremlin1] p. 19Definition 112Dfcaragencmpl 45549  voncmpl 45635
[Fremlin1] p. 19Definition 113A (ii)omessle 45512
[Fremlin1] p. 20Theorem 113Ccarageniuncl 45537  carageniuncllem1 45535  carageniuncllem2 45536  caragenuncl 45527  caragenuncllem 45526  caragenunicl 45538
[Fremlin1] p. 21Remark 113Dcaragenel2d 45546
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 45540  caratheodorylem2 45541
[Fremlin1] p. 21Exercise 113Xacaragencmpl 45549
[Fremlin1] p. 23Lemma 114Bhoidmv1le 45608  hoidmv1lelem1 45605  hoidmv1lelem2 45606  hoidmv1lelem3 45607
[Fremlin1] p. 25Definition 114Eisvonmbl 45652
[Fremlin1] p. 29Lemma 115Bhoidmv1le 45608  hoidmvle 45614  hoidmvlelem1 45609  hoidmvlelem2 45610  hoidmvlelem3 45611  hoidmvlelem4 45612  hoidmvlelem5 45613  hsphoidmvle2 45599  hsphoif 45590  hsphoival 45593
[Fremlin1] p. 29Definition 1135 (b)hoicvr 45562
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 45570
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 45597  hoidmvn0val 45598  hoidmvval 45591  hoidmvval0 45601  hoidmvval0b 45604
[Fremlin1] p. 30Lemma 115Bhoiprodp1 45602  hsphoidmvle 45600
[Fremlin1] p. 30Definition 115Cdf-ovoln 45551  df-voln 45553
[Fremlin1] p. 30Proposition 115D (a)dmovn 45618  ovn0 45580  ovn0lem 45579  ovnf 45577  ovnome 45587  ovnssle 45575  ovnsslelem 45574  ovnsupge0 45571
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 45617  ovnhoilem1 45615  ovnhoilem2 45616  vonhoi 45681
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 45634  hoidifhspf 45632  hoidifhspval 45622  hoidifhspval2 45629  hoidifhspval3 45633  hspmbl 45643  hspmbllem1 45640  hspmbllem2 45641  hspmbllem3 45642
[Fremlin1] p. 31Definition 115Evoncmpl 45635  vonmea 45588
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 45586  ovnsubadd2 45660  ovnsubadd2lem 45659  ovnsubaddlem1 45584  ovnsubaddlem2 45585
[Fremlin1] p. 32Proposition 115G (a)hoimbl 45645  hoimbl2 45679  hoimbllem 45644  hspdifhsp 45630  opnvonmbl 45648  opnvonmbllem2 45647
[Fremlin1] p. 32Proposition 115G (b)borelmbl 45650
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 45693  iccvonmbllem 45692  ioovonmbl 45691
[Fremlin1] p. 32Proposition 115G (d)vonicc 45699  vonicclem2 45698  vonioo 45696  vonioolem2 45695  vonn0icc 45702  vonn0icc2 45706  vonn0ioo 45701  vonn0ioo2 45704
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 45703  snvonmbl 45700  vonct 45707  vonsn 45705
[Fremlin1] p. 35Lemma 121Asubsalsal 45373
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 45372  subsaliuncllem 45371
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 45739  salpreimalegt 45723  salpreimaltle 45740
[Fremlin1] p. 35Proposition 121B (i)issmf 45742  issmff 45748  issmflem 45741
[Fremlin1] p. 35Proposition 121B (ii)issmfle 45759  issmflelem 45758  smfpreimale 45768
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 45770  issmfgtlem 45769
[Fremlin1] p. 36Definition 121Cdf-smblfn 45710  issmf 45742  issmff 45748  issmfge 45784  issmfgelem 45783  issmfgt 45770  issmfgtlem 45769  issmfle 45759  issmflelem 45758  issmflem 45741
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 45721  salpreimagtlt 45744  salpreimalelt 45743
[Fremlin1] p. 36Proposition 121B (iv)issmfge 45784  issmfgelem 45783
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 45767
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 45765  cnfsmf 45754
[Fremlin1] p. 36Proposition 121D (c)decsmf 45781  decsmflem 45780  incsmf 45756  incsmflem 45755
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 45715  pimconstlt1 45716  smfconst 45763
[Fremlin1] p. 37Proposition 121E (b)smfadd 45779  smfaddlem1 45777  smfaddlem2 45778
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 45810
[Fremlin1] p. 37Proposition 121E (d)smfmul 45809  smfmullem1 45805  smfmullem2 45806  smfmullem3 45807  smfmullem4 45808
[Fremlin1] p. 37Proposition 121E (e)smfdiv 45811
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 45814  smfpimbor1lem2 45813
[Fremlin1] p. 37Proposition 121E (g)smfco 45816
[Fremlin1] p. 37Proposition 121E (h)smfres 45804
[Fremlin1] p. 38Proposition 121E (e)smfrec 45803
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 45812  smfresal 45802
[Fremlin1] p. 38Proposition 121F (a)smflim 45791  smflim2 45820  smflimlem1 45785  smflimlem2 45786  smflimlem3 45787  smflimlem4 45788  smflimlem5 45789  smflimlem6 45790  smflimmpt 45824
[Fremlin1] p. 38Proposition 121F (b)smfsup 45828  smfsuplem1 45825  smfsuplem2 45826  smfsuplem3 45827  smfsupmpt 45829  smfsupxr 45830
[Fremlin1] p. 38Proposition 121F (c)smfinf 45832  smfinflem 45831  smfinfmpt 45833
[Fremlin1] p. 39Remark 121Gsmflim 45791  smflim2 45820  smflimmpt 45824
[Fremlin1] p. 39Proposition 121Fsmfpimcc 45822
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 45852  smfdivdmmbl2 45855  smfinfdmmbl 45863  smfinfdmmbllem 45862  smfsupdmmbl 45859  smfsupdmmbllem 45858
[Fremlin1] p. 39Proposition 121F (d)smflimsup 45842  smflimsuplem2 45835  smflimsuplem6 45839  smflimsuplem7 45840  smflimsuplem8 45841  smflimsupmpt 45843
[Fremlin1] p. 39Proposition 121F (e)smfliminf 45845  smfliminflem 45844  smfliminfmpt 45846
[Fremlin1] p. 80Definition 135E (b)df-smblfn 45710
[Fremlin1], p. 38Proposition 121F (b)fsupdm 45856  fsupdm2 45857
[Fremlin1], p. 39Proposition 121Hadddmmbl 45847  adddmmbl2 45848  finfdm 45860  finfdm2 45861  fsupdm 45856  fsupdm2 45857  muldmmbl 45849  muldmmbl2 45850
[Fremlin1], p. 39Proposition 121F (c)finfdm 45860  finfdm2 45861
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25285
[Fremlin5] p. 213Lemma 565Cauniioovol 25328
[Fremlin5] p. 214Lemma 565Cauniioombl 25338
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 36869
[Fremlin5] p. 220Theorem 565Maftc1anc 36872
[FreydScedrov] p. 283Axiom of Infinityax-inf 9635  inf1 9619  inf2 9620
[Gleason] p. 117Proposition 9-2.1df-enq 10908  enqer 10918
[Gleason] p. 117Proposition 9-2.2df-1nq 10913  df-nq 10909
[Gleason] p. 117Proposition 9-2.3df-plpq 10905  df-plq 10911
[Gleason] p. 119Proposition 9-2.4caovmo 7646  df-mpq 10906  df-mq 10912
[Gleason] p. 119Proposition 9-2.5df-rq 10914
[Gleason] p. 119Proposition 9-2.6ltexnq 10972
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10973  ltbtwnnq 10975
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10968
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10969
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10976
[Gleason] p. 121Definition 9-3.1df-np 10978
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10990
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10992
[Gleason] p. 122Definitiondf-1p 10979
[Gleason] p. 122Remark (1)prub 10991
[Gleason] p. 122Lemma 9-3.4prlem934 11030
[Gleason] p. 122Proposition 9-3.2df-ltp 10982
[Gleason] p. 122Proposition 9-3.3ltsopr 11029  psslinpr 11028  supexpr 11051  suplem1pr 11049  suplem2pr 11050
[Gleason] p. 123Proposition 9-3.5addclpr 11015  addclprlem1 11013  addclprlem2 11014  df-plp 10980
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11019
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11018
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11031
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11040  ltexprlem1 11033  ltexprlem2 11034  ltexprlem3 11035  ltexprlem4 11036  ltexprlem5 11037  ltexprlem6 11038  ltexprlem7 11039
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11042  ltaprlem 11041
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11043
[Gleason] p. 124Lemma 9-3.6prlem936 11044
[Gleason] p. 124Proposition 9-3.7df-mp 10981  mulclpr 11017  mulclprlem 11016  reclem2pr 11045
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11026
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11021
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11020
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11025
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11048  reclem3pr 11046  reclem4pr 11047
[Gleason] p. 126Proposition 9-4.1df-enr 11052  enrer 11060
[Gleason] p. 126Proposition 9-4.2df-0r 11057  df-1r 11058  df-nr 11053
[Gleason] p. 126Proposition 9-4.3df-mr 11055  df-plr 11054  negexsr 11099  recexsr 11104  recexsrlem 11100
[Gleason] p. 127Proposition 9-4.4df-ltr 11056
[Gleason] p. 130Proposition 10-1.3creui 12211  creur 12210  cru 12208
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11185  axcnre 11161
[Gleason] p. 132Definition 10-3.1crim 15066  crimd 15183  crimi 15144  crre 15065  crred 15182  crrei 15143
[Gleason] p. 132Definition 10-3.2remim 15068  remimd 15149
[Gleason] p. 133Definition 10.36absval2 15235  absval2d 15396  absval2i 15348
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15092  cjaddd 15171  cjaddi 15139
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15093  cjmuld 15172  cjmuli 15140
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15091  cjcjd 15150  cjcji 15122
[Gleason] p. 133Proposition 10-3.4(f)cjre 15090  cjreb 15074  cjrebd 15153  cjrebi 15125  cjred 15177  rere 15073  rereb 15071  rerebd 15152  rerebi 15124  rered 15175
[Gleason] p. 133Proposition 10-3.4(h)addcj 15099  addcjd 15163  addcji 15134
[Gleason] p. 133Proposition 10-3.7(a)absval 15189
[Gleason] p. 133Proposition 10-3.7(b)abscj 15230  abscjd 15401  abscji 15352
[Gleason] p. 133Proposition 10-3.7(c)abs00 15240  abs00d 15397  abs00i 15349  absne0d 15398
[Gleason] p. 133Proposition 10-3.7(d)releabs 15272  releabsd 15402  releabsi 15353
[Gleason] p. 133Proposition 10-3.7(f)absmul 15245  absmuld 15405  absmuli 15355
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15233  sqabsaddi 15356
[Gleason] p. 133Proposition 10-3.7(h)abstri 15281  abstrid 15407  abstrii 15359
[Gleason] p. 134Definition 10-4.1df-exp 14032  exp0 14035  expp1 14038  expp1d 14116
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26423  cxpaddd 26461  expadd 14074  expaddd 14117  expaddz 14076
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26432  cxpmuld 26481  expmul 14077  expmuld 14118  expmulz 14078
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26429  mulcxpd 26472  mulexp 14071  mulexpd 14130  mulexpz 14072
[Gleason] p. 140Exercise 1znnen 16159
[Gleason] p. 141Definition 11-2.1fzval 13490
[Gleason] p. 168Proposition 12-2.1(a)climadd 15580  rlimadd 15591  rlimdiv 15596
[Gleason] p. 168Proposition 12-2.1(b)climsub 15582  rlimsub 15593
[Gleason] p. 168Proposition 12-2.1(c)climmul 15581  rlimmul 15594
[Gleason] p. 171Corollary 12-2.2climmulc2 15585
[Gleason] p. 172Corollary 12-2.5climrecl 15531
[Gleason] p. 172Proposition 12-2.4(c)climabs 15552  climcj 15553  climim 15555  climre 15554  rlimabs 15557  rlimcj 15558  rlimim 15560  rlimre 15559
[Gleason] p. 173Definition 12-3.1df-ltxr 11257  df-xr 11256  ltxr 13099
[Gleason] p. 175Definition 12-4.1df-limsup 15419  limsupval 15422
[Gleason] p. 180Theorem 12-5.1climsup 15620
[Gleason] p. 180Theorem 12-5.3caucvg 15629  caucvgb 15630  caucvgbf 44498  caucvgr 15626  climcau 15621
[Gleason] p. 182Exercise 3cvgcmp 15766
[Gleason] p. 182Exercise 4cvgrat 15833
[Gleason] p. 195Theorem 13-2.12abs1m 15286
[Gleason] p. 217Lemma 13-4.1btwnzge0 13797
[Gleason] p. 223Definition 14-1.1df-met 21138
[Gleason] p. 223Definition 14-1.1(a)met0 24069  xmet0 24068
[Gleason] p. 223Definition 14-1.1(b)metgt0 24085
[Gleason] p. 223Definition 14-1.1(c)metsym 24076
[Gleason] p. 223Definition 14-1.1(d)mettri 24078  mstri 24195  xmettri 24077  xmstri 24194
[Gleason] p. 225Definition 14-1.5xpsmet 24108
[Gleason] p. 230Proposition 14-2.6txlm 23372
[Gleason] p. 240Theorem 14-4.3metcnp4 25058
[Gleason] p. 240Proposition 14-4.2metcnp3 24269
[Gleason] p. 243Proposition 14-4.16addcn 24601  addcn2 15542  mulcn 24603  mulcn2 15544  subcn 24602  subcn2 15543
[Gleason] p. 295Remarkbcval3 14270  bcval4 14271
[Gleason] p. 295Equation 2bcpasc 14285
[Gleason] p. 295Definition of binomial coefficientbcval 14268  df-bc 14267
[Gleason] p. 296Remarkbcn0 14274  bcnn 14276
[Gleason] p. 296Theorem 15-2.8binom 15780
[Gleason] p. 308Equation 2ef0 16038
[Gleason] p. 308Equation 3efcj 16039
[Gleason] p. 309Corollary 15-4.3efne0 16044
[Gleason] p. 309Corollary 15-4.4efexp 16048
[Gleason] p. 310Equation 14sinadd 16111
[Gleason] p. 310Equation 15cosadd 16112
[Gleason] p. 311Equation 17sincossq 16123
[Gleason] p. 311Equation 18cosbnd 16128  sinbnd 16127
[Gleason] p. 311Lemma 15-4.7sqeqor 14184  sqeqori 14182
[Gleason] p. 311Definition of ` `df-pi 16020
[Godowski] p. 730Equation SFgoeqi 31793
[GodowskiGreechie] p. 249Equation IV3oai 31188
[Golan] p. 1Remarksrgisid 20103
[Golan] p. 1Definitiondf-srg 20081
[Golan] p. 149Definitiondf-slmd 32616
[Gonshor] p. 7Definitiondf-scut 27521
[Gonshor] p. 9Theorem 2.5slerec 27557
[Gonshor] p. 10Theorem 2.6cofcut1 27645  cofcut1d 27646
[Gonshor] p. 10Theorem 2.7cofcut2 27647  cofcut2d 27648
[Gonshor] p. 12Theorem 2.9cofcutr 27649  cofcutr1d 27650  cofcutr2d 27651
[Gonshor] p. 13Definitiondf-adds 27682
[Gonshor] p. 14Theorem 3.1addsprop 27698
[Gonshor] p. 15Theorem 3.2addsunif 27724
[Gonshor] p. 17Theorem 3.4mulsprop 27825
[Gonshor] p. 18Theorem 3.5mulsunif 27844
[GramKnuthPat], p. 47Definition 2.42df-fwddif 35435
[Gratzer] p. 23Section 0.6df-mre 17534
[Gratzer] p. 27Section 0.6df-mri 17536
[Hall] p. 1Section 1.1df-asslaw 46864  df-cllaw 46862  df-comlaw 46863
[Hall] p. 2Section 1.2df-clintop 46876
[Hall] p. 7Section 1.3df-sgrp2 46897
[Halmos] p. 28Partition ` `df-parts 37938  dfmembpart2 37943
[Halmos] p. 31Theorem 17.3riesz1 31585  riesz2 31586
[Halmos] p. 41Definition of Hermitianhmopadj2 31461
[Halmos] p. 42Definition of projector orderingpjordi 31693
[Halmos] p. 43Theorem 26.1elpjhmop 31705  elpjidm 31704  pjnmopi 31668
[Halmos] p. 44Remarkpjinormi 31207  pjinormii 31196
[Halmos] p. 44Theorem 26.2elpjch 31709  pjrn 31227  pjrni 31222  pjvec 31216
[Halmos] p. 44Theorem 26.3pjnorm2 31247
[Halmos] p. 44Theorem 26.4hmopidmpj 31674  hmopidmpji 31672
[Halmos] p. 45Theorem 27.1pjinvari 31711
[Halmos] p. 45Theorem 27.3pjoci 31700  pjocvec 31217
[Halmos] p. 45Theorem 27.4pjorthcoi 31689
[Halmos] p. 48Theorem 29.2pjssposi 31692
[Halmos] p. 48Theorem 29.3pjssdif1i 31695  pjssdif2i 31694
[Halmos] p. 50Definition of spectrumdf-spec 31375
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 23
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1795
[Hatcher] p. 25Definitiondf-phtpc 24738  df-phtpy 24717
[Hatcher] p. 26Definitiondf-pco 24752  df-pi1 24755
[Hatcher] p. 26Proposition 1.2phtpcer 24741
[Hatcher] p. 26Proposition 1.3pi1grp 24797
[Hefferon] p. 240Definition 3.12df-dmat 22212  df-dmatalt 47166
[Helfgott] p. 2Theoremtgoldbach 46783
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 46768
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 46780  bgoldbtbnd 46775  bgoldbtbnd 46775  tgblthelfgott 46781
[Helfgott] p. 5Proposition 1.1circlevma 33952
[Helfgott] p. 69Statement 7.49circlemethhgt 33953
[Helfgott] p. 69Statement 7.50hgt750lema 33967  hgt750lemb 33966  hgt750leme 33968  hgt750lemf 33963  hgt750lemg 33964
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 46777  tgoldbachgt 33973  tgoldbachgtALTV 46778  tgoldbachgtd 33972
[Helfgott] p. 70Statement 7.49ax-hgt749 33954
[Herstein] p. 54Exercise 28df-grpo 30013
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18866  grpoideu 30029  mndideu 18670
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18895  grpoinveu 30039
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18926  grpo2inv 30051
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18937  grpoinvop 30053
[Herstein] p. 57Exercise 1dfgrp3e 18959
[Hitchcock] p. 5Rule A3mptnan 1768
[Hitchcock] p. 5Rule A4mptxor 1769
[Hitchcock] p. 5Rule A5mtpxor 1771
[Holland] p. 1519Theorem 2sumdmdi 31940
[Holland] p. 1520Lemma 5cdj1i 31953  cdj3i 31961  cdj3lem1 31954  cdjreui 31952
[Holland] p. 1524Lemma 7mddmdin0i 31951
[Holland95] p. 13Theorem 3.6hlathil 41139
[Holland95] p. 14Line 15hgmapvs 41065
[Holland95] p. 14Line 16hdmaplkr 41087
[Holland95] p. 14Line 17hdmapellkr 41088
[Holland95] p. 14Line 19hdmapglnm2 41085
[Holland95] p. 14Line 20hdmapip0com 41091
[Holland95] p. 14Theorem 3.6hdmapevec2 41010
[Holland95] p. 14Lines 24 and 25hdmapoc 41105
[Holland95] p. 204Definition of involutiondf-srng 20597
[Holland95] p. 212Definition of subspacedf-psubsp 38677
[Holland95] p. 214Lemma 3.3lclkrlem2v 40702
[Holland95] p. 214Definition 3.2df-lpolN 40655
[Holland95] p. 214Definition of nonsingularpnonsingN 39107
[Holland95] p. 215Lemma 3.3(1)dihoml4 40551  poml4N 39127
[Holland95] p. 215Lemma 3.3(2)dochexmid 40642  pexmidALTN 39152  pexmidN 39143
[Holland95] p. 218Theorem 3.6lclkr 40707
[Holland95] p. 218Definition of dual vector spacedf-ldual 38297  ldualset 38298
[Holland95] p. 222Item 1df-lines 38675  df-pointsN 38676
[Holland95] p. 222Item 2df-polarityN 39077
[Holland95] p. 223Remarkispsubcl2N 39121  omllaw4 38419  pol1N 39084  polcon3N 39091
[Holland95] p. 223Definitiondf-psubclN 39109
[Holland95] p. 223Equation for polaritypolval2N 39080
[Holmes] p. 40Definitiondf-xrn 37544
[Hughes] p. 44Equation 1.21bax-his3 30604
[Hughes] p. 47Definition of projection operatordfpjop 31702
[Hughes] p. 49Equation 1.30eighmre 31483  eigre 31355  eigrei 31354
[Hughes] p. 49Equation 1.31eighmorth 31484  eigorth 31358  eigorthi 31357
[Hughes] p. 137Remark (ii)eigposi 31356
[Huneke] p. 1Claim 1frgrncvvdeq 29829
[Huneke] p. 1Statement 1frgrncvvdeqlem7 29825
[Huneke] p. 1Statement 2frgrncvvdeqlem8 29826
[Huneke] p. 1Statement 3frgrncvvdeqlem9 29827
[Huneke] p. 2Claim 2frgrregorufr 29845  frgrregorufr0 29844  frgrregorufrg 29846
[Huneke] p. 2Claim 3frgrhash2wsp 29852  frrusgrord 29861  frrusgrord0 29860
[Huneke] p. 2Statementdf-clwwlknon 29608
[Huneke] p. 2Statement 4frgrwopreglem4 29835
[Huneke] p. 2Statement 5frgrwopreg1 29838  frgrwopreg2 29839  frgrwopregasn 29836  frgrwopregbsn 29837
[Huneke] p. 2Statement 6frgrwopreglem5 29841
[Huneke] p. 2Statement 7fusgreghash2wspv 29855
[Huneke] p. 2Statement 8fusgreghash2wsp 29858
[Huneke] p. 2Statement 9clwlksndivn 29606  numclwlk1 29891  numclwlk1lem1 29889  numclwlk1lem2 29890  numclwwlk1 29881  numclwwlk8 29912
[Huneke] p. 2Definition 3frgrwopreglem1 29832
[Huneke] p. 2Definition 4df-clwlks 29295
[Huneke] p. 2Definition 62clwwlk 29867
[Huneke] p. 2Definition 7numclwwlkovh 29893  numclwwlkovh0 29892
[Huneke] p. 2Statement 10numclwwlk2 29901
[Huneke] p. 2Statement 11rusgrnumwlkg 29498
[Huneke] p. 2Statement 12numclwwlk3 29905
[Huneke] p. 2Statement 13numclwwlk5 29908
[Huneke] p. 2Statement 14numclwwlk7 29911
[Indrzejczak] p. 33Definition ` `Enatded 29923  natded 29923
[Indrzejczak] p. 33Definition ` `Inatded 29923
[Indrzejczak] p. 34Definition ` `Enatded 29923  natded 29923
[Indrzejczak] p. 34Definition ` `Inatded 29923
[Jech] p. 4Definition of classcv 1538  cvjust 2724
[Jech] p. 42Lemma 6.1alephexp1 10576
[Jech] p. 42Equation 6.1alephadd 10574  alephmul 10575
[Jech] p. 43Lemma 6.2infmap 10573  infmap2 10215
[Jech] p. 71Lemma 9.3jech9.3 9811
[Jech] p. 72Equation 9.3scott0 9883  scottex 9882
[Jech] p. 72Exercise 9.1rankval4 9864
[Jech] p. 72Scheme "Collection Principle"cp 9888
[Jech] p. 78Noteopthprc 5739
[JonesMatijasevic] p. 694Definition 2.3rmxyval 41956
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 42044
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 42045
[JonesMatijasevic] p. 695Equation 2.7rmxadd 41968
[JonesMatijasevic] p. 695Equation 2.8rmyadd 41972
[JonesMatijasevic] p. 695Equation 2.9rmxp1 41973  rmyp1 41974
[JonesMatijasevic] p. 695Equation 2.10rmxm1 41975  rmym1 41976
[JonesMatijasevic] p. 695Equation 2.11rmx0 41966  rmx1 41967  rmxluc 41977
[JonesMatijasevic] p. 695Equation 2.12rmy0 41970  rmy1 41971  rmyluc 41978
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 41980
[JonesMatijasevic] p. 695Equation 2.14rmydbl 41981
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 42001  jm2.17b 42002  jm2.17c 42003
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 42034
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 42038
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 42029
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 42004  jm2.24nn 42000
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 42043
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 42049  rmygeid 42005
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 42061
[Juillerat] p. 11Section *5etransc 45297  etransclem47 45295  etransclem48 45296
[Juillerat] p. 12Equation (7)etransclem44 45292
[Juillerat] p. 12Equation *(7)etransclem46 45294
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 45280
[Juillerat] p. 13Proofetransclem35 45283
[Juillerat] p. 13Part of case 2 proven inetransclem38 45286
[Juillerat] p. 13Part of case 2 provenetransclem24 45272
[Juillerat] p. 13Part of case 2: proven inetransclem41 45289
[Juillerat] p. 14Proofetransclem23 45271
[KalishMontague] p. 81Note 1ax-6 1969
[KalishMontague] p. 85Lemma 2equid 2013
[KalishMontague] p. 85Lemma 3equcomi 2018
[KalishMontague] p. 86Lemma 7cbvalivw 2008  cbvaliw 2007  wl-cbvmotv 36685  wl-motae 36687  wl-moteq 36686
[KalishMontague] p. 87Lemma 8spimvw 1997  spimw 1972
[KalishMontague] p. 87Lemma 9spfw 2034  spw 2035
[Kalmbach] p. 14Definition of latticechabs1 31036  chabs1i 31038  chabs2 31037  chabs2i 31039  chjass 31053  chjassi 31006  latabs1 18432  latabs2 18433
[Kalmbach] p. 15Definition of atomdf-at 31858  ela 31859
[Kalmbach] p. 15Definition of coverscvbr2 31803  cvrval2 38447
[Kalmbach] p. 16Definitiondf-ol 38351  df-oml 38352
[Kalmbach] p. 20Definition of commutescmbr 31104  cmbri 31110  cmtvalN 38384  df-cm 31103  df-cmtN 38350
[Kalmbach] p. 22Remarkomllaw5N 38420  pjoml5 31133  pjoml5i 31108
[Kalmbach] p. 22Definitionpjoml2 31131  pjoml2i 31105
[Kalmbach] p. 22Theorem 2(v)cmcm 31134  cmcmi 31112  cmcmii 31117  cmtcomN 38422
[Kalmbach] p. 22Theorem 2(ii)omllaw3 38418  omlsi 30924  pjoml 30956  pjomli 30955
[Kalmbach] p. 22Definition of OML lawomllaw2N 38417
[Kalmbach] p. 23Remarkcmbr2i 31116  cmcm3 31135  cmcm3i 31114  cmcm3ii 31119  cmcm4i 31115  cmt3N 38424  cmt4N 38425  cmtbr2N 38426
[Kalmbach] p. 23Lemma 3cmbr3 31128  cmbr3i 31120  cmtbr3N 38427
[Kalmbach] p. 25Theorem 5fh1 31138  fh1i 31141  fh2 31139  fh2i 31142  omlfh1N 38431
[Kalmbach] p. 65Remarkchjatom 31877  chslej 31018  chsleji 30978  shslej 30900  shsleji 30890
[Kalmbach] p. 65Proposition 1chocin 31015  chocini 30974  chsupcl 30860  chsupval2 30930  h0elch 30775  helch 30763  hsupval2 30929  ocin 30816  ococss 30813  shococss 30814
[Kalmbach] p. 65Definition of subspace sumshsval 30832
[Kalmbach] p. 66Remarkdf-pjh 30915  pjssmi 31685  pjssmii 31201
[Kalmbach] p. 67Lemma 3osum 31165  osumi 31162
[Kalmbach] p. 67Lemma 4pjci 31720
[Kalmbach] p. 103Exercise 6atmd2 31920
[Kalmbach] p. 103Exercise 12mdsl0 31830
[Kalmbach] p. 140Remarkhatomic 31880  hatomici 31879  hatomistici 31882
[Kalmbach] p. 140Proposition 1atlatmstc 38492
[Kalmbach] p. 140Proposition 1(i)atexch 31901  lsatexch 38216
[Kalmbach] p. 140Proposition 1(ii)chcv1 31875  cvlcvr1 38512  cvr1 38584
[Kalmbach] p. 140Proposition 1(iii)cvexch 31894  cvexchi 31889  cvrexch 38594
[Kalmbach] p. 149Remark 2chrelati 31884  hlrelat 38576  hlrelat5N 38575  lrelat 38187
[Kalmbach] p. 153Exercise 5lsmcv 20899  lsmsatcv 38183  spansncv 31173  spansncvi 31172
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 38202  spansncv2 31813
[Kalmbach] p. 266Definitiondf-st 31731
[Kalmbach2] p. 8Definition of adjointdf-adjh 31369
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10643  fpwwe2 10640
[KanamoriPincus] p. 416Corollary 1.3canth4 10644
[KanamoriPincus] p. 417Corollary 1.6canthp1 10651
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10646
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10648
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10661
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10665  gchxpidm 10666
[KanamoriPincus] p. 419Theorem 2.1gchacg 10677  gchhar 10676
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10213  unxpwdom 9586
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10667
[Kreyszig] p. 3Property M1metcl 24058  xmetcl 24057
[Kreyszig] p. 4Property M2meteq0 24065
[Kreyszig] p. 8Definition 1.1-8dscmet 24301
[Kreyszig] p. 12Equation 5conjmul 11935  muleqadd 11862
[Kreyszig] p. 18Definition 1.3-2mopnval 24164
[Kreyszig] p. 19Remarkmopntopon 24165
[Kreyszig] p. 19Theorem T1mopn0 24227  mopnm 24170
[Kreyszig] p. 19Theorem T2unimopn 24225
[Kreyszig] p. 19Definition of neighborhoodneibl 24230
[Kreyszig] p. 20Definition 1.3-3metcnp2 24271
[Kreyszig] p. 25Definition 1.4-1lmbr 22982  lmmbr 25006  lmmbr2 25007
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23104
[Kreyszig] p. 28Theorem 1.4-5lmcau 25061
[Kreyszig] p. 28Definition 1.4-3iscau 25024  iscmet2 25042
[Kreyszig] p. 30Theorem 1.4-7cmetss 25064
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23185  metelcls 25053
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25054  metcld2 25055
[Kreyszig] p. 51Equation 2clmvneg1 24846  lmodvneg1 20659  nvinv 30159  vcm 30096
[Kreyszig] p. 51Equation 1aclm0vs 24842  lmod0vs 20649  slmd0vs 32639  vc0 30094
[Kreyszig] p. 51Equation 1blmodvs0 20650  slmdvs0 32640  vcz 30095
[Kreyszig] p. 58Definition 2.2-1imsmet 30211  ngpmet 24332  nrmmetd 24303
[Kreyszig] p. 59Equation 1imsdval 30206  imsdval2 30207  ncvspds 24909  ngpds 24333
[Kreyszig] p. 63Problem 1nmval 24318  nvnd 30208
[Kreyszig] p. 64Problem 2nmeq0 24347  nmge0 24346  nvge0 30193  nvz 30189
[Kreyszig] p. 64Problem 3nmrtri 24353  nvabs 30192
[Kreyszig] p. 91Definition 2.7-1isblo3i 30321
[Kreyszig] p. 92Equation 2df-nmoo 30265
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30327  blocni 30325
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30326
[Kreyszig] p. 129Definition 3.1-1cphipeq0 24952  ipeq0 21410  ipz 30239
[Kreyszig] p. 135Problem 2cphpyth 24964  pythi 30370
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30374
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 24986
[Kreyszig] p. 144Equation 4supcvg 15806
[Kreyszig] p. 144Theorem 3.3-1minvec 25184  minveco 30404
[Kreyszig] p. 196Definition 3.9-1df-aj 30270
[Kreyszig] p. 247Theorem 4.7-2bcth 25077
[Kreyszig] p. 249Theorem 4.7-3ubth 30393
[Kreyszig] p. 470Definition of positive operator orderingleop 31643  leopg 31642
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 31661
[Kreyszig] p. 525Theorem 10.1-1htth 30438
[Kulpa] p. 547Theorempoimir 36824
[Kulpa] p. 547Equation (1)poimirlem32 36823
[Kulpa] p. 547Equation (2)poimirlem31 36822
[Kulpa] p. 548Theorembroucube 36825
[Kulpa] p. 548Equation (6)poimirlem26 36817
[Kulpa] p. 548Equation (7)poimirlem27 36818
[Kunen] p. 10Axiom 0ax6e 2380  axnul 5304
[Kunen] p. 11Axiom 3axnul 5304
[Kunen] p. 12Axiom 6zfrep6 7943
[Kunen] p. 24Definition 10.24mapval 8834  mapvalg 8832
[Kunen] p. 30Lemma 10.20fodomg 10519
[Kunen] p. 31Definition 10.24mapex 8828
[Kunen] p. 95Definition 2.1df-r1 9761
[Kunen] p. 97Lemma 2.10r1elss 9803  r1elssi 9802
[Kunen] p. 107Exercise 4rankop 9855  rankopb 9849  rankuni 9860  rankxplim 9876  rankxpsuc 9879
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 5008
[Lang] , p. 225Corollary 1.3finexttrb 33029
[Lang] p. Definitiondf-rn 5686
[Lang] p. 3Statementlidrideqd 18594  mndbn0 18675
[Lang] p. 3Definitiondf-mnd 18660
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18612
[Lang] p. 4Property of composites. Second formulagsumccat 18758
[Lang] p. 5Equationgsumreidx 19826
[Lang] p. 5Definition of an (infinite) productgsumfsupp 46858
[Lang] p. 6Examplenn0mnd 46855
[Lang] p. 6Equationgsumxp2 19889
[Lang] p. 6Statementcycsubm 19117
[Lang] p. 6Definitionmulgnn0gsum 18996
[Lang] p. 6Observationmndlsmidm 19579
[Lang] p. 7Definitiondfgrp2e 18884
[Lang] p. 30Definitiondf-tocyc 32536
[Lang] p. 32Property (a)cyc3genpm 32581
[Lang] p. 32Property (b)cyc3conja 32586  cycpmconjv 32571
[Lang] p. 53Definitiondf-cat 17616
[Lang] p. 53Axiom CAT 1cat1 18051  cat1lem 18050
[Lang] p. 54Definitiondf-iso 17700
[Lang] p. 57Definitiondf-inito 17938  df-termo 17939
[Lang] p. 58Exampleirinitoringc 47055
[Lang] p. 58Statementinitoeu1 17965  termoeu1 17972
[Lang] p. 62Definitiondf-func 17812
[Lang] p. 65Definitiondf-nat 17898
[Lang] p. 91Notedf-ringc 46991
[Lang] p. 92Statementmxidlprm 32860
[Lang] p. 92Definitionisprmidlc 32840
[Lang] p. 128Remarkdsmmlmod 21519
[Lang] p. 129Prooflincscm 47198  lincscmcl 47200  lincsum 47197  lincsumcl 47199
[Lang] p. 129Statementlincolss 47202
[Lang] p. 129Observationdsmmfi 21512
[Lang] p. 141Theorem 5.3dimkerim 33000  qusdimsum 33001
[Lang] p. 141Corollary 5.4lssdimle 32980
[Lang] p. 147Definitionsnlindsntor 47239
[Lang] p. 504Statementmat1 22169  matring 22165
[Lang] p. 504Definitiondf-mamu 22106
[Lang] p. 505Statementmamuass 22122  mamutpos 22180  matassa 22166  mattposvs 22177  tposmap 22179
[Lang] p. 513Definitionmdet1 22323  mdetf 22317
[Lang] p. 513Theorem 4.4cramer 22413
[Lang] p. 514Proposition 4.6mdetleib 22309
[Lang] p. 514Proposition 4.8mdettpos 22333
[Lang] p. 515Definitiondf-minmar1 22357  smadiadetr 22397
[Lang] p. 515Corollary 4.9mdetero 22332  mdetralt 22330
[Lang] p. 517Proposition 4.15mdetmul 22345
[Lang] p. 518Definitiondf-madu 22356
[Lang] p. 518Proposition 4.16madulid 22367  madurid 22366  matinv 22399
[Lang] p. 561Theorem 3.1cayleyhamilton 22612
[Lang], p. 224Proposition 1.2extdgmul 33028  fedgmul 33004
[Lang], p. 561Remarkchpmatply1 22554
[Lang], p. 561Definitiondf-chpmat 22549
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 43395
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 43390
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 43396
[LeBlanc] p. 277Rule R2axnul 5304
[Levy] p. 12Axiom 4.3.1df-clab 2708
[Levy] p. 59Definitiondf-ttrcl 9705
[Levy] p. 64Theorem 5.6(ii)frinsg 9748
[Levy] p. 338Axiomdf-clel 2808  df-cleq 2722
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2808  df-cleq 2722
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2708
[Levy] p. 358Axiomdf-clab 2708
[Levy58] p. 2Definition Iisfin1-3 10383
[Levy58] p. 2Definition IIdf-fin2 10283
[Levy58] p. 2Definition Iadf-fin1a 10282
[Levy58] p. 2Definition IIIdf-fin3 10285
[Levy58] p. 3Definition Vdf-fin5 10286
[Levy58] p. 3Definition IVdf-fin4 10284
[Levy58] p. 4Definition VIdf-fin6 10287
[Levy58] p. 4Definition VIIdf-fin7 10288
[Levy58], p. 3Theorem 1fin1a2 10412
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27425
[Lipparini] p. 3Lemma 2.1.4noresle 27436
[Lipparini] p. 6Proposition 4.2noinfbnd1 27468  nosupbnd1 27453
[Lipparini] p. 6Proposition 4.3noinfbnd2 27470  nosupbnd2 27455
[Lipparini] p. 7Theorem 5.1noetasuplem3 27474  noetasuplem4 27475
[Lipparini] p. 7Corollary 4.4nosupinfsep 27471
[Lopez-Astorga] p. 12Rule 1mptnan 1768
[Lopez-Astorga] p. 12Rule 2mptxor 1769
[Lopez-Astorga] p. 12Rule 3mtpxor 1771
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 31928
[Maeda] p. 168Lemma 5mdsym 31932  mdsymi 31931
[Maeda] p. 168Lemma 4(i)mdsymlem4 31926  mdsymlem6 31928  mdsymlem7 31929
[Maeda] p. 168Lemma 4(ii)mdsymlem8 31930
[MaedaMaeda] p. 1Remarkssdmd1 31833  ssdmd2 31834  ssmd1 31831  ssmd2 31832
[MaedaMaeda] p. 1Lemma 1.2mddmd2 31829
[MaedaMaeda] p. 1Definition 1.1df-dmd 31801  df-md 31800  mdbr 31814
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 31851  mdslj1i 31839  mdslj2i 31840  mdslle1i 31837  mdslle2i 31838  mdslmd1i 31849  mdslmd2i 31850
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 31841  mdsl2bi 31843  mdsl2i 31842
[MaedaMaeda] p. 2Lemma 1.6mdexchi 31855
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 31852
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 31853
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 31830
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 31835  mdsl3 31836
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 31854
[MaedaMaeda] p. 4Theorem 1.14mdcompli 31949
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 38494  hlrelat1 38574
[MaedaMaeda] p. 31Lemma 7.5lcvexch 38212
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 31856  cvmdi 31844  cvnbtwn4 31809  cvrnbtwn4 38452
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 31857
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 38513  cvp 31895  cvrp 38590  lcvp 38213
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 31919
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 31918
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 38506  hlexch4N 38566
[MaedaMaeda] p. 34Exercise 7.1atabsi 31921
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 38617
[MaedaMaeda] p. 61Definition 15.10psubN 38923  atpsubN 38927  df-pointsN 38676  pointpsubN 38925
[MaedaMaeda] p. 62Theorem 15.5df-pmap 38678  pmap11 38936  pmaple 38935  pmapsub 38942  pmapval 38931
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 38939  pmap1N 38941
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 38944  pmapglb2N 38945  pmapglb2xN 38946  pmapglbx 38943
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 39026
[MaedaMaeda] p. 67Postulate PS1ps-1 38651
[MaedaMaeda] p. 68Lemma 16.2df-padd 38970  paddclN 39016  paddidm 39015
[MaedaMaeda] p. 68Condition PS2ps-2 38652
[MaedaMaeda] p. 68Equation 16.2.1paddass 39012
[MaedaMaeda] p. 69Lemma 16.4ps-1 38651
[MaedaMaeda] p. 69Theorem 16.4ps-2 38652
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19584  lsmmod2 19585  lssats 38185  shatomici 31878  shatomistici 31881  shmodi 30910  shmodsi 30909
[MaedaMaeda] p. 130Remark 29.6dmdmd 31820  mdsymlem7 31929
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31109
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31013
[MaedaMaeda] p. 139Remarksumdmdii 31935
[Margaris] p. 40Rule Cexlimiv 1931
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 395  df-ex 1780  df-or 844  dfbi2 473
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 29920
[Margaris] p. 59Section 14notnotrALTVD 43978
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 43979
[Margaris] p. 79Rule Cexinst01 43688  exinst11 43689
[Margaris] p. 89Theorem 19.219.2 1978  19.2g 2179  r19.2z 4493
[Margaris] p. 89Theorem 19.319.3 2193  rr19.3v 3656
[Margaris] p. 89Theorem 19.5alcom 2154
[Margaris] p. 89Theorem 19.6alex 1826
[Margaris] p. 89Theorem 19.7alnex 1781
[Margaris] p. 89Theorem 19.819.8a 2172
[Margaris] p. 89Theorem 19.919.9 2196  19.9h 2280  exlimd 2209  exlimdh 2284
[Margaris] p. 89Theorem 19.11excom 2160  excomim 2161
[Margaris] p. 89Theorem 19.1219.12 2318
[Margaris] p. 90Section 19conventions-labels 29921  conventions-labels 29921  conventions-labels 29921  conventions-labels 29921
[Margaris] p. 90Theorem 19.14exnal 1827
[Margaris] p. 90Theorem 19.152albi 43439  albi 1818
[Margaris] p. 90Theorem 19.1619.16 2216
[Margaris] p. 90Theorem 19.1719.17 2217
[Margaris] p. 90Theorem 19.182exbi 43441  exbi 1847
[Margaris] p. 90Theorem 19.1919.19 2220
[Margaris] p. 90Theorem 19.202alim 43438  2alimdv 1919  alimd 2203  alimdh 1817  alimdv 1917  ax-4 1809  ralimdaa 3255  ralimdv 3167  ralimdva 3165  ralimdvva 3202  sbcimdv 3850
[Margaris] p. 90Theorem 19.2119.21 2198  19.21h 2281  19.21t 2197  19.21vv 43437  alrimd 2206  alrimdd 2205  alrimdh 1864  alrimdv 1930  alrimi 2204  alrimih 1824  alrimiv 1928  alrimivv 1929  hbralrimi 3142  r19.21be 3247  r19.21bi 3246  ralrimd 3259  ralrimdv 3150  ralrimdva 3152  ralrimdvv 3199  ralrimdvva 3207  ralrimi 3252  ralrimia 3253  ralrimiv 3143  ralrimiva 3144  ralrimivv 3196  ralrimivva 3198  ralrimivvva 3201  ralrimivw 3148
[Margaris] p. 90Theorem 19.222exim 43440  2eximdv 1920  exim 1834  eximd 2207  eximdh 1865  eximdv 1918  rexim 3085  reximd2a 3264  reximdai 3256  reximdd 44142  reximddv 3169  reximddv2 3210  reximddv3 44141  reximdv 3168  reximdv2 3162  reximdva 3166  reximdvai 3163  reximdvva 3203  reximi2 3077
[Margaris] p. 90Theorem 19.2319.23 2202  19.23bi 2182  19.23h 2282  19.23t 2201  exlimdv 1934  exlimdvv 1935  exlimexi 43587  exlimiv 1931  exlimivv 1933  rexlimd3 44134  rexlimdv 3151  rexlimdv3a 3157  rexlimdva 3153  rexlimdva2 3155  rexlimdvaa 3154  rexlimdvv 3208  rexlimdvva 3209  rexlimdvw 3158  rexlimiv 3146  rexlimiva 3145  rexlimivv 3197
[Margaris] p. 90Theorem 19.2419.24 1987
[Margaris] p. 90Theorem 19.2519.25 1881
[Margaris] p. 90Theorem 19.2619.26 1871
[Margaris] p. 90Theorem 19.2719.27 2218  r19.27z 4503  r19.27zv 4504
[Margaris] p. 90Theorem 19.2819.28 2219  19.28vv 43447  r19.28z 4496  r19.28zf 44154  r19.28zv 4499  rr19.28v 3657
[Margaris] p. 90Theorem 19.2919.29 1874  r19.29d2r 3138  r19.29imd 3116
[Margaris] p. 90Theorem 19.3019.30 1882
[Margaris] p. 90Theorem 19.3119.31 2225  19.31vv 43445
[Margaris] p. 90Theorem 19.3219.32 2224  r19.32 46104
[Margaris] p. 90Theorem 19.3319.33-2 43443  19.33 1885
[Margaris] p. 90Theorem 19.3419.34 1988
[Margaris] p. 90Theorem 19.3519.35 1878
[Margaris] p. 90Theorem 19.3619.36 2221  19.36vv 43444  r19.36zv 4505
[Margaris] p. 90Theorem 19.3719.37 2223  19.37vv 43446  r19.37zv 4500
[Margaris] p. 90Theorem 19.3819.38 1839
[Margaris] p. 90Theorem 19.3919.39 1986
[Margaris] p. 90Theorem 19.4019.40-2 1888  19.40 1887  r19.40 3117
[Margaris] p. 90Theorem 19.4119.41 2226  19.41rg 43613
[Margaris] p. 90Theorem 19.4219.42 2227
[Margaris] p. 90Theorem 19.4319.43 1883
[Margaris] p. 90Theorem 19.4419.44 2228  r19.44zv 4502
[Margaris] p. 90Theorem 19.4519.45 2229  r19.45zv 4501
[Margaris] p. 110Exercise 2(b)eu1 2604
[Mayet] p. 370Remarkjpi 31790  largei 31787  stri 31777
[Mayet3] p. 9Definition of CH-statesdf-hst 31732  ishst 31734
[Mayet3] p. 10Theoremhstrbi 31786  hstri 31785
[Mayet3] p. 1223Theorem 4.1mayete3i 31248
[Mayet3] p. 1240Theorem 7.1mayetes3i 31249
[MegPav2000] p. 2344Theorem 3.3stcltrthi 31798
[MegPav2000] p. 2345Definition 3.4-1chintcl 30852  chsupcl 30860
[MegPav2000] p. 2345Definition 3.4-2hatomic 31880
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 31874
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 31901
[MegPav2000] p. 2366Figure 7pl42N 39157
[MegPav2002] p. 362Lemma 2.2latj31 18444  latj32 18442  latjass 18440
[Megill] p. 444Axiom C5ax-5 1911  ax5ALT 38080
[Megill] p. 444Section 7conventions 29920
[Megill] p. 445Lemma L12aecom-o 38074  ax-c11n 38061  axc11n 2423
[Megill] p. 446Lemma L17equtrr 2023
[Megill] p. 446Lemma L18ax6fromc10 38069
[Megill] p. 446Lemma L19hbnae-o 38101  hbnae 2429
[Megill] p. 447Remark 9.1dfsb1 2478  sbid 2245  sbidd-misc 47851  sbidd 47850
[Megill] p. 448Remark 9.6axc14 2460
[Megill] p. 448Scheme C4'ax-c4 38057
[Megill] p. 448Scheme C5'ax-c5 38056  sp 2174
[Megill] p. 448Scheme C6'ax-11 2152
[Megill] p. 448Scheme C7'ax-c7 38058
[Megill] p. 448Scheme C8'ax-7 2009
[Megill] p. 448Scheme C9'ax-c9 38063
[Megill] p. 448Scheme C10'ax-6 1969  ax-c10 38059
[Megill] p. 448Scheme C11'ax-c11 38060
[Megill] p. 448Scheme C12'ax-8 2106
[Megill] p. 448Scheme C13'ax-9 2114
[Megill] p. 448Scheme C14'ax-c14 38064
[Megill] p. 448Scheme C15'ax-c15 38062
[Megill] p. 448Scheme C16'ax-c16 38065
[Megill] p. 448Theorem 9.4dral1-o 38077  dral1 2436  dral2-o 38103  dral2 2435  drex1 2438  drex2 2439  drsb1 2492  drsb2 2255
[Megill] p. 449Theorem 9.7sbcom2 2159  sbequ 2084  sbid2v 2506
[Megill] p. 450Example in Appendixhba1-o 38070  hba1 2287
[Mendelson] p. 35Axiom A3hirstL-ax3 45900
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3872  rspsbca 3873  stdpc4 2069
[Mendelson] p. 69Axiom 5ax-c4 38057  ra4 3879  stdpc5 2199
[Mendelson] p. 81Rule Cexlimiv 1931
[Mendelson] p. 95Axiom 6stdpc6 2029
[Mendelson] p. 95Axiom 7stdpc7 2240
[Mendelson] p. 225Axiom system NBGru 3775
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5513
[Mendelson] p. 231Exercise 4.10(k)inv1 4393
[Mendelson] p. 231Exercise 4.10(l)unv 4394
[Mendelson] p. 231Exercise 4.10(n)dfin3 4265
[Mendelson] p. 231Exercise 4.10(o)df-nul 4322
[Mendelson] p. 231Exercise 4.10(q)dfin4 4266
[Mendelson] p. 231Exercise 4.10(s)ddif 4135
[Mendelson] p. 231Definition of uniondfun3 4264
[Mendelson] p. 235Exercise 4.12(c)univ 5450
[Mendelson] p. 235Exercise 4.12(d)pwv 4904
[Mendelson] p. 235Exercise 4.12(j)pwin 5569
[Mendelson] p. 235Exercise 4.12(k)pwunss 4619
[Mendelson] p. 235Exercise 4.12(l)pwssun 5570
[Mendelson] p. 235Exercise 4.12(n)uniin 4934
[Mendelson] p. 235Exercise 4.12(p)reli 5825
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6266
[Mendelson] p. 244Proposition 4.8(g)epweon 7764
[Mendelson] p. 246Definition of successordf-suc 6369
[Mendelson] p. 250Exercise 4.36oelim2 8597
[Mendelson] p. 254Proposition 4.22(b)xpen 9142
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9057  xpsneng 9058
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9065  xpcomeng 9066
[Mendelson] p. 254Proposition 4.22(e)xpassen 9068
[Mendelson] p. 255Definitionbrsdom 8973
[Mendelson] p. 255Exercise 4.39endisj 9060
[Mendelson] p. 255Exercise 4.41mapprc 8826
[Mendelson] p. 255Exercise 4.43mapsnen 9039  mapsnend 9038
[Mendelson] p. 255Exercise 4.45mapunen 9148
[Mendelson] p. 255Exercise 4.47xpmapen 9147
[Mendelson] p. 255Exercise 4.42(a)map0e 8878
[Mendelson] p. 255Exercise 4.42(b)map1 9042
[Mendelson] p. 257Proposition 4.24(a)undom 9061
[Mendelson] p. 258Exercise 4.56(c)djuassen 10175  djucomen 10174
[Mendelson] p. 258Exercise 4.56(f)djudom1 10179
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10173
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8533
[Mendelson] p. 266Proposition 4.34(f)oaordex 8560
[Mendelson] p. 275Proposition 4.42(d)entri3 10556
[Mendelson] p. 281Definitiondf-r1 9761
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9810
[Mendelson] p. 287Axiom system MKru 3775
[MertziosUnger] p. 152Definitiondf-frgr 29779
[MertziosUnger] p. 153Remark 1frgrconngr 29814
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 29816  vdgn1frgrv3 29817
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 29818
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 29811
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 29804  2pthfrgrrn 29802  2pthfrgrrn2 29803
[Mittelstaedt] p. 9Definitiondf-oc 30772
[Monk1] p. 22Remarkconventions 29920
[Monk1] p. 22Theorem 3.1conventions 29920
[Monk1] p. 26Theorem 2.8(vii)ssin 4229
[Monk1] p. 33Theorem 3.2(i)ssrel 5781  ssrelf 32111
[Monk1] p. 33Theorem 3.2(ii)eqrel 5783
[Monk1] p. 34Definition 3.3df-opab 5210
[Monk1] p. 36Theorem 3.7(i)coi1 6260  coi2 6261
[Monk1] p. 36Theorem 3.8(v)dm0 5919  rn0 5924
[Monk1] p. 36Theorem 3.7(ii)cnvi 6140
[Monk1] p. 37Theorem 3.13(i)relxp 5693
[Monk1] p. 37Theorem 3.13(x)dmxp 5927  rnxp 6168
[Monk1] p. 37Theorem 3.13(ii)0xp 5773  xp0 6156
[Monk1] p. 38Theorem 3.16(ii)ima0 6075
[Monk1] p. 38Theorem 3.16(viii)imai 6072
[Monk1] p. 39Theorem 3.17imaex 7909  imaexALTV 37502  imaexg 7908
[Monk1] p. 39Theorem 3.16(xi)imassrn 6069
[Monk1] p. 41Theorem 4.3(i)fnopfv 7076  funfvop 7050
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6946
[Monk1] p. 42Theorem 4.4(iii)fvelima 6956
[Monk1] p. 43Theorem 4.6funun 6593
[Monk1] p. 43Theorem 4.8(iv)dff13 7256  dff13f 7257
[Monk1] p. 46Theorem 4.15(v)funex 7222  funrnex 7942
[Monk1] p. 50Definition 5.4fniunfv 7248
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6225
[Monk1] p. 52Theorem 5.11(viii)ssint 4967
[Monk1] p. 52Definition 5.13 (i)1stval2 7994  df-1st 7977
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7995  df-2nd 7978
[Monk1] p. 112Theorem 15.17(v)ranksn 9851  ranksnb 9824
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9852
[Monk1] p. 112Theorem 15.17(iii)rankun 9853  rankunb 9847
[Monk1] p. 113Theorem 15.18r1val3 9835
[Monk1] p. 113Definition 15.19df-r1 9761  r1val2 9834
[Monk1] p. 117Lemmazorn2 10503  zorn2g 10500
[Monk1] p. 133Theorem 18.11cardom 9983
[Monk1] p. 133Theorem 18.12canth3 10558
[Monk1] p. 133Theorem 18.14carduni 9978
[Monk2] p. 105Axiom C4ax-4 1809
[Monk2] p. 105Axiom C7ax-7 2009
[Monk2] p. 105Axiom C8ax-12 2169  ax-c15 38062  ax12v2 2171
[Monk2] p. 108Lemma 5ax-c4 38057
[Monk2] p. 109Lemma 12ax-11 2152
[Monk2] p. 109Lemma 15equvini 2452  equvinv 2030  eqvinop 5486
[Monk2] p. 113Axiom C5-1ax-5 1911  ax5ALT 38080
[Monk2] p. 113Axiom C5-2ax-10 2135
[Monk2] p. 113Axiom C5-3ax-11 2152
[Monk2] p. 114Lemma 21sp 2174
[Monk2] p. 114Lemma 22axc4 2312  hba1-o 38070  hba1 2287
[Monk2] p. 114Lemma 23nfia1 2148
[Monk2] p. 114Lemma 24nfa2 2168  nfra2 3370  nfra2w 3294
[Moore] p. 53Part Idf-mre 17534
[Munkres] p. 77Example 2distop 22718  indistop 22725  indistopon 22724
[Munkres] p. 77Example 3fctop 22727  fctop2 22728
[Munkres] p. 77Example 4cctop 22729
[Munkres] p. 78Definition of basisdf-bases 22669  isbasis3g 22672
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17393  tgval2 22679
[Munkres] p. 79Remarktgcl 22692
[Munkres] p. 80Lemma 2.1tgval3 22686
[Munkres] p. 80Lemma 2.2tgss2 22710  tgss3 22709
[Munkres] p. 81Lemma 2.3basgen 22711  basgen2 22712
[Munkres] p. 83Exercise 3topdifinf 36533  topdifinfeq 36534  topdifinffin 36532  topdifinfindis 36530
[Munkres] p. 89Definition of subspace topologyresttop 22884
[Munkres] p. 93Theorem 6.1(1)0cld 22762  topcld 22759
[Munkres] p. 93Theorem 6.1(2)iincld 22763
[Munkres] p. 93Theorem 6.1(3)uncld 22765
[Munkres] p. 94Definition of closureclsval 22761
[Munkres] p. 94Definition of interiorntrval 22760
[Munkres] p. 95Theorem 6.5(a)clsndisj 22799  elcls 22797
[Munkres] p. 95Theorem 6.5(b)elcls3 22807
[Munkres] p. 97Theorem 6.6clslp 22872  neindisj 22841
[Munkres] p. 97Corollary 6.7cldlp 22874
[Munkres] p. 97Definition of limit pointislp2 22869  lpval 22863
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23039
[Munkres] p. 102Definition of continuous functiondf-cn 22951  iscn 22959  iscn2 22962
[Munkres] p. 107Theorem 7.2(g)cncnp 23004  cncnp2 23005  cncnpi 23002  df-cnp 22952  iscnp 22961  iscnp2 22963
[Munkres] p. 127Theorem 10.1metcn 24272
[Munkres] p. 128Theorem 10.3metcn4 25059
[Nathanson] p. 123Remarkreprgt 33931  reprinfz1 33932  reprlt 33929
[Nathanson] p. 123Definitiondf-repr 33919
[Nathanson] p. 123Chapter 5.1circlemethnat 33951
[Nathanson] p. 123Propositionbreprexp 33943  breprexpnat 33944  itgexpif 33916
[NielsenChuang] p. 195Equation 4.73unierri 31624
[OeSilva] p. 2042Section 2ax-bgbltosilva 46776
[Pfenning] p. 17Definition XMnatded 29923
[Pfenning] p. 17Definition NNCnatded 29923  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 29923
[Pfenning] p. 18Rule"natded 29923
[Pfenning] p. 18Definition /\Inatded 29923
[Pfenning] p. 18Definition ` `Enatded 29923  natded 29923  natded 29923  natded 29923  natded 29923
[Pfenning] p. 18Definition ` `Inatded 29923  natded 29923  natded 29923  natded 29923  natded 29923
[Pfenning] p. 18Definition ` `ELnatded 29923
[Pfenning] p. 18Definition ` `ERnatded 29923
[Pfenning] p. 18Definition ` `Ea,unatded 29923
[Pfenning] p. 18Definition ` `IRnatded 29923
[Pfenning] p. 18Definition ` `Ianatded 29923
[Pfenning] p. 127Definition =Enatded 29923
[Pfenning] p. 127Definition =Inatded 29923
[Ponnusamy] p. 361Theorem 6.44cphip0l 24950  df-dip 30221  dip0l 30238  ip0l 21408
[Ponnusamy] p. 361Equation 6.45cphipval 24991  ipval 30223
[Ponnusamy] p. 362Equation I1dipcj 30234  ipcj 21406
[Ponnusamy] p. 362Equation I3cphdir 24953  dipdir 30362  ipdir 21411  ipdiri 30350
[Ponnusamy] p. 362Equation I4ipidsq 30230  nmsq 24942
[Ponnusamy] p. 362Equation 6.46ip0i 30345
[Ponnusamy] p. 362Equation 6.47ip1i 30347
[Ponnusamy] p. 362Equation 6.48ip2i 30348
[Ponnusamy] p. 363Equation I2cphass 24959  dipass 30365  ipass 21417  ipassi 30361
[Prugovecki] p. 186Definition of brabraval 31464  df-bra 31370
[Prugovecki] p. 376Equation 8.1df-kb 31371  kbval 31474
[PtakPulmannova] p. 66Proposition 3.2.17atomli 31902
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 39062
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 31916  atcvat4i 31917  cvrat3 38616  cvrat4 38617  lsatcvat3 38225
[PtakPulmannova] p. 68Definition 3.2.18cvbr 31802  cvrval 38442  df-cv 31799  df-lcv 38192  lspsncv0 20904
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 39074
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 39075
[Quine] p. 16Definition 2.1df-clab 2708  rabid 3450  rabidd 44150
[Quine] p. 17Definition 2.1''dfsb7 2273
[Quine] p. 18Definition 2.7df-cleq 2722
[Quine] p. 19Definition 2.9conventions 29920  df-v 3474
[Quine] p. 34Theorem 5.1eqabb 2871
[Quine] p. 35Theorem 5.2abid1 2868  abid2f 2934
[Quine] p. 40Theorem 6.1sb5 2265
[Quine] p. 40Theorem 6.2sb6 2086  sbalex 2233
[Quine] p. 41Theorem 6.3df-clel 2808
[Quine] p. 41Theorem 6.4eqid 2730  eqid1 29987
[Quine] p. 41Theorem 6.5eqcom 2737
[Quine] p. 42Theorem 6.6df-sbc 3777
[Quine] p. 42Theorem 6.7dfsbcq 3778  dfsbcq2 3779
[Quine] p. 43Theorem 6.8vex 3476
[Quine] p. 43Theorem 6.9isset 3485
[Quine] p. 44Theorem 7.3spcgf 3580  spcgv 3585  spcimgf 3578
[Quine] p. 44Theorem 6.11spsbc 3789  spsbcd 3790
[Quine] p. 44Theorem 6.12elex 3491
[Quine] p. 44Theorem 6.13elab 3667  elabg 3665  elabgf 3663
[Quine] p. 44Theorem 6.14noel 4329
[Quine] p. 48Theorem 7.2snprc 4720
[Quine] p. 48Definition 7.1df-pr 4630  df-sn 4628
[Quine] p. 49Theorem 7.4snss 4788  snssg 4786
[Quine] p. 49Theorem 7.5prss 4822  prssg 4821
[Quine] p. 49Theorem 7.6prid1 4765  prid1g 4763  prid2 4766  prid2g 4764  snid 4663  snidg 4661
[Quine] p. 51Theorem 7.12snex 5430
[Quine] p. 51Theorem 7.13prex 5431
[Quine] p. 53Theorem 8.2unisn 4929  unisnALT 43989  unisng 4928
[Quine] p. 53Theorem 8.3uniun 4933
[Quine] p. 54Theorem 8.6elssuni 4940
[Quine] p. 54Theorem 8.7uni0 4938
[Quine] p. 56Theorem 8.17uniabio 6509
[Quine] p. 56Definition 8.18dfaiota2 46092  dfiota2 6495
[Quine] p. 57Theorem 8.19aiotaval 46101  iotaval 6513
[Quine] p. 57Theorem 8.22iotanul 6520
[Quine] p. 58Theorem 8.23iotaex 6515
[Quine] p. 58Definition 9.1df-op 4634
[Quine] p. 61Theorem 9.5opabid 5524  opabidw 5523  opelopab 5541  opelopaba 5535  opelopabaf 5543  opelopabf 5544  opelopabg 5537  opelopabga 5532  opelopabgf 5539  oprabid 7443  oprabidw 7442
[Quine] p. 64Definition 9.11df-xp 5681
[Quine] p. 64Definition 9.12df-cnv 5683
[Quine] p. 64Definition 9.15df-id 5573
[Quine] p. 65Theorem 10.3fun0 6612
[Quine] p. 65Theorem 10.4funi 6579
[Quine] p. 65Theorem 10.5funsn 6600  funsng 6598
[Quine] p. 65Definition 10.1df-fun 6544
[Quine] p. 65Definition 10.2args 6090  dffv4 6887
[Quine] p. 68Definition 10.11conventions 29920  df-fv 6550  fv2 6885
[Quine] p. 124Theorem 17.3nn0opth2 14236  nn0opth2i 14235  nn0opthi 14234  omopthi 8662
[Quine] p. 177Definition 25.2df-rdg 8412
[Quine] p. 232Equation icarddom 10551
[Quine] p. 284Axiom 39(vi)funimaex 6635  funimaexg 6633
[Quine] p. 331Axiom system NFru 3775
[ReedSimon] p. 36Definition (iii)ax-his3 30604
[ReedSimon] p. 63Exercise 4(a)df-dip 30221  polid 30679  polid2i 30677  polidi 30678
[ReedSimon] p. 63Exercise 4(b)df-ph 30333
[ReedSimon] p. 195Remarklnophm 31539  lnophmi 31538
[Retherford] p. 49Exercise 1(i)leopadd 31652
[Retherford] p. 49Exercise 1(ii)leopmul 31654  leopmuli 31653
[Retherford] p. 49Exercise 1(iv)leoptr 31657
[Retherford] p. 49Definition VI.1df-leop 31372  leoppos 31646
[Retherford] p. 49Exercise 1(iii)leoptri 31656
[Retherford] p. 49Definition of operator orderingleop3 31645
[Roman] p. 4Definitiondf-dmat 22212  df-dmatalt 47166
[Roman] p. 18Part Preliminariesdf-rng 20047
[Roman] p. 19Part Preliminariesdf-ring 20129
[Roman] p. 46Theorem 1.6isldepslvec2 47253
[Roman] p. 112Noteisldepslvec2 47253  ldepsnlinc 47276  zlmodzxznm 47265
[Roman] p. 112Examplezlmodzxzequa 47264  zlmodzxzequap 47267  zlmodzxzldep 47272
[Roman] p. 170Theorem 7.8cayleyhamilton 22612
[Rosenlicht] p. 80Theoremheicant 36826
[Rosser] p. 281Definitiondf-op 4634
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 33955
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 33956
[Rotman] p. 28Remarkpgrpgt2nabl 47130  pmtr3ncom 19384
[Rotman] p. 31Theorem 3.4symggen2 19380
[Rotman] p. 42Theorem 3.15cayley 19323  cayleyth 19324
[Rudin] p. 164Equation 27efcan 16043
[Rudin] p. 164Equation 30efzval 16049
[Rudin] p. 167Equation 48absefi 16143
[Sanford] p. 39Remarkax-mp 5  mto 196
[Sanford] p. 39Rule 3mtpxor 1771
[Sanford] p. 39Rule 4mptxor 1769
[Sanford] p. 40Rule 1mptnan 1768
[Schechter] p. 51Definition of antisymmetryintasym 6115
[Schechter] p. 51Definition of irreflexivityintirr 6118
[Schechter] p. 51Definition of symmetrycnvsym 6112
[Schechter] p. 51Definition of transitivitycotr 6110
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17534
[Schechter] p. 79Definition of Moore closuredf-mrc 17535
[Schechter] p. 82Section 4.5df-mrc 17535
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17537
[Schechter] p. 139Definition AC3dfac9 10133
[Schechter] p. 141Definition (MC)dfac11 42106
[Schechter] p. 149Axiom DC1ax-dc 10443  axdc3 10451
[Schechter] p. 187Definition of "ring with unit"isring 20131  isrngo 37068
[Schechter] p. 276Remark 11.6.espan0 31062
[Schechter] p. 276Definition of spandf-span 30829  spanval 30853
[Schechter] p. 428Definition 15.35bastop1 22716
[Schloeder] p. 1Lemma 1.3onelon 6388  onelord 42302  ordelon 6387  ordelord 6385
[Schloeder] p. 1Lemma 1.7onepsuc 42303  sucidg 6444
[Schloeder] p. 1Remark 1.50elon 6417  onsuc 7801  ord0 6416  ordsuci 7798
[Schloeder] p. 1Theorem 1.9epsoon 42304
[Schloeder] p. 1Definition 1.1dftr5 5268
[Schloeder] p. 1Definition 1.2dford3 42069  elon2 6374
[Schloeder] p. 1Definition 1.4df-suc 6369
[Schloeder] p. 1Definition 1.6epel 5582  epelg 5580
[Schloeder] p. 1Theorem 1.9(i)elirr 9594  epirron 42305  ordirr 6381
[Schloeder] p. 1Theorem 1.9(ii)oneltr 42307  oneptr 42306  ontr1 6409
[Schloeder] p. 1Theorem 1.9(iii)oneltri 42309  oneptri 42308  ordtri3or 6395
[Schloeder] p. 2Lemma 1.10ondif1 8503  ord0eln0 6418
[Schloeder] p. 2Lemma 1.13elsuci 6430  onsucss 42318  trsucss 6451
[Schloeder] p. 2Lemma 1.14ordsucss 7808
[Schloeder] p. 2Lemma 1.15onnbtwn 6457  ordnbtwn 6456
[Schloeder] p. 2Lemma 1.16orddif0suc 42320  ordnexbtwnsuc 42319
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10398  onsucf1lem 42321  onsucf1o 42324  onsucf1olem 42322  onsucrn 42323
[Schloeder] p. 2Lemma 1.18dflim7 42325
[Schloeder] p. 2Remark 1.12ordzsl 7836
[Schloeder] p. 2Theorem 1.10ondif1i 42314  ordne0gt0 42313
[Schloeder] p. 2Definition 1.11dflim6 42316  limnsuc 42317  onsucelab 42315
[Schloeder] p. 3Remark 1.21omex 9640
[Schloeder] p. 3Theorem 1.19tfinds 7851
[Schloeder] p. 3Theorem 1.22omelon 9643  ordom 7867
[Schloeder] p. 3Definition 1.20dfom3 9644
[Schloeder] p. 4Lemma 2.21onn 8641
[Schloeder] p. 4Lemma 2.7ssonuni 7769  ssorduni 7768
[Schloeder] p. 4Remark 2.4oa1suc 8533
[Schloeder] p. 4Theorem 1.23dfom5 9647  limom 7873
[Schloeder] p. 4Definition 2.1df-1o 8468  df1o2 8475
[Schloeder] p. 4Definition 2.3oa0 8518  oa0suclim 42327  oalim 8534  oasuc 8526
[Schloeder] p. 4Definition 2.5om0 8519  om0suclim 42328  omlim 8535  omsuc 8528
[Schloeder] p. 4Definition 2.6oe0 8524  oe0m1 8523  oe0suclim 42329  oelim 8536  oesuc 8529
[Schloeder] p. 5Lemma 2.10onsupuni 42280
[Schloeder] p. 5Lemma 2.11onsupsucismax 42331
[Schloeder] p. 5Lemma 2.12onsssupeqcond 42332
[Schloeder] p. 5Lemma 2.13limexissup 42333  limexissupab 42335  limiun 42334  limuni 6424
[Schloeder] p. 5Lemma 2.14oa0r 8540
[Schloeder] p. 5Lemma 2.15om1 8544  om1om1r 42336  om1r 8545
[Schloeder] p. 5Remark 2.8oacl 8537  oaomoecl 42330  oecl 8539  omcl 8538
[Schloeder] p. 5Definition 2.9onsupintrab 42282
[Schloeder] p. 6Lemma 2.16oe1 8546
[Schloeder] p. 6Lemma 2.17oe1m 8547
[Schloeder] p. 6Lemma 2.18oe0rif 42337
[Schloeder] p. 6Theorem 2.19oasubex 42338
[Schloeder] p. 6Theorem 2.20nnacl 8613  nnamecl 42339  nnecl 8615  nnmcl 8614
[Schloeder] p. 7Lemma 3.1onsucwordi 42340
[Schloeder] p. 7Lemma 3.2oaword1 8554
[Schloeder] p. 7Lemma 3.3oaword2 8555
[Schloeder] p. 7Lemma 3.4oalimcl 8562
[Schloeder] p. 7Lemma 3.5oaltublim 42342
[Schloeder] p. 8Lemma 3.6oaordi3 42343
[Schloeder] p. 8Lemma 3.81oaomeqom 42345
[Schloeder] p. 8Lemma 3.10oa00 8561
[Schloeder] p. 8Lemma 3.11omge1 42349  omword1 8575
[Schloeder] p. 8Remark 3.9oaordnr 42348  oaordnrex 42347
[Schloeder] p. 8Theorem 3.7oaord3 42344
[Schloeder] p. 9Lemma 3.12omge2 42350  omword2 8576
[Schloeder] p. 9Lemma 3.13omlim2 42351
[Schloeder] p. 9Lemma 3.14omord2lim 42352
[Schloeder] p. 9Lemma 3.15omord2i 42353  omordi 8568
[Schloeder] p. 9Theorem 3.16omord 8570  omord2com 42354
[Schloeder] p. 10Lemma 3.172omomeqom 42355  df-2o 8469
[Schloeder] p. 10Lemma 3.19oege1 42358  oewordi 8593
[Schloeder] p. 10Lemma 3.20oege2 42359  oeworde 8595
[Schloeder] p. 10Lemma 3.21rp-oelim2 42360
[Schloeder] p. 10Lemma 3.22oeord2lim 42361
[Schloeder] p. 10Remark 3.18omnord1 42357  omnord1ex 42356
[Schloeder] p. 11Lemma 3.23oeord2i 42362
[Schloeder] p. 11Lemma 3.25nnoeomeqom 42364
[Schloeder] p. 11Remark 3.26oenord1 42368  oenord1ex 42367
[Schloeder] p. 11Theorem 4.1oaomoencom 42369
[Schloeder] p. 11Theorem 4.2oaass 8563
[Schloeder] p. 11Theorem 3.24oeord2com 42363
[Schloeder] p. 12Theorem 4.3odi 8581
[Schloeder] p. 13Theorem 4.4omass 8582
[Schloeder] p. 14Remark 4.6oenass 42371
[Schloeder] p. 14Theorem 4.7oeoa 8599
[Schloeder] p. 15Lemma 5.1cantnftermord 42372
[Schloeder] p. 15Lemma 5.2cantnfub 42373  cantnfub2 42374
[Schloeder] p. 16Theorem 5.3cantnf2 42377
[Schwabhauser] p. 10Axiom A1axcgrrflx 28439  axtgcgrrflx 27980
[Schwabhauser] p. 10Axiom A2axcgrtr 28440
[Schwabhauser] p. 10Axiom A3axcgrid 28441  axtgcgrid 27981
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 27966
[Schwabhauser] p. 11Axiom A4axsegcon 28452  axtgsegcon 27982  df-trkgcb 27968
[Schwabhauser] p. 11Axiom A5ax5seg 28463  axtg5seg 27983  df-trkgcb 27968
[Schwabhauser] p. 11Axiom A6axbtwnid 28464  axtgbtwnid 27984  df-trkgb 27967
[Schwabhauser] p. 12Axiom A7axpasch 28466  axtgpasch 27985  df-trkgb 27967
[Schwabhauser] p. 12Axiom A8axlowdim2 28485  df-trkg2d 33975
[Schwabhauser] p. 13Axiom A8axtglowdim2 27988
[Schwabhauser] p. 13Axiom A9axtgupdim2 27989  df-trkg2d 33975
[Schwabhauser] p. 13Axiom A10axeuclid 28488  axtgeucl 27990  df-trkge 27969
[Schwabhauser] p. 13Axiom A11axcont 28501  axtgcont 27987  axtgcont1 27986  df-trkgb 27967
[Schwabhauser] p. 27Theorem 2.1cgrrflx 35263
[Schwabhauser] p. 27Theorem 2.2cgrcomim 35265
[Schwabhauser] p. 27Theorem 2.3cgrtr 35268
[Schwabhauser] p. 27Theorem 2.4cgrcoml 35272
[Schwabhauser] p. 27Theorem 2.5cgrcomr 35273  tgcgrcomimp 27995  tgcgrcoml 27997  tgcgrcomr 27996
[Schwabhauser] p. 28Theorem 2.8cgrtriv 35278  tgcgrtriv 28002
[Schwabhauser] p. 28Theorem 2.105segofs 35282  tg5segofs 33983
[Schwabhauser] p. 28Definition 2.10df-afs 33980  df-ofs 35259
[Schwabhauser] p. 29Theorem 2.11cgrextend 35284  tgcgrextend 28003
[Schwabhauser] p. 29Theorem 2.12segconeq 35286  tgsegconeq 28004
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 35298  btwntriv2 35288  tgbtwntriv2 28005
[Schwabhauser] p. 30Theorem 3.2btwncomim 35289  tgbtwncom 28006
[Schwabhauser] p. 30Theorem 3.3btwntriv1 35292  tgbtwntriv1 28009
[Schwabhauser] p. 30Theorem 3.4btwnswapid 35293  tgbtwnswapid 28010
[Schwabhauser] p. 30Theorem 3.5btwnexch2 35299  btwnintr 35295  tgbtwnexch2 28014  tgbtwnintr 28011
[Schwabhauser] p. 30Theorem 3.6btwnexch 35301  btwnexch3 35296  tgbtwnexch 28016  tgbtwnexch3 28012
[Schwabhauser] p. 30Theorem 3.7btwnouttr 35300  tgbtwnouttr 28015  tgbtwnouttr2 28013
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28484
[Schwabhauser] p. 32Theorem 3.14btwndiff 35303  tgbtwndiff 28024
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28017  trisegint 35304
[Schwabhauser] p. 34Theorem 4.2ifscgr 35320  tgifscgr 28026
[Schwabhauser] p. 34Theorem 4.11colcom 28076  colrot1 28077  colrot2 28078  lncom 28140  lnrot1 28141  lnrot2 28142
[Schwabhauser] p. 34Definition 4.1df-ifs 35316
[Schwabhauser] p. 35Theorem 4.3cgrsub 35321  tgcgrsub 28027
[Schwabhauser] p. 35Theorem 4.5cgrxfr 35331  tgcgrxfr 28036
[Schwabhauser] p. 35Statement 4.4ercgrg 28035
[Schwabhauser] p. 35Definition 4.4df-cgr3 35317  df-cgrg 28029
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28029
[Schwabhauser] p. 36Theorem 4.6btwnxfr 35332  tgbtwnxfr 28048
[Schwabhauser] p. 36Theorem 4.11colinearperm1 35338  colinearperm2 35340  colinearperm3 35339  colinearperm4 35341  colinearperm5 35342
[Schwabhauser] p. 36Definition 4.8df-ismt 28051
[Schwabhauser] p. 36Definition 4.10df-colinear 35315  tgellng 28071  tglng 28064
[Schwabhauser] p. 37Theorem 4.12colineartriv1 35343
[Schwabhauser] p. 37Theorem 4.13colinearxfr 35351  lnxfr 28084
[Schwabhauser] p. 37Theorem 4.14lineext 35352  lnext 28085
[Schwabhauser] p. 37Theorem 4.16fscgr 35356  tgfscgr 28086
[Schwabhauser] p. 37Theorem 4.17linecgr 35357  lncgr 28087
[Schwabhauser] p. 37Definition 4.15df-fs 35318
[Schwabhauser] p. 38Theorem 4.18lineid 35359  lnid 28088
[Schwabhauser] p. 38Theorem 4.19idinside 35360  tgidinside 28089
[Schwabhauser] p. 39Theorem 5.1btwnconn1 35377  tgbtwnconn1 28093
[Schwabhauser] p. 41Theorem 5.2btwnconn2 35378  tgbtwnconn2 28094
[Schwabhauser] p. 41Theorem 5.3btwnconn3 35379  tgbtwnconn3 28095
[Schwabhauser] p. 41Theorem 5.5brsegle2 35385
[Schwabhauser] p. 41Definition 5.4df-segle 35383  legov 28103
[Schwabhauser] p. 41Definition 5.5legov2 28104
[Schwabhauser] p. 42Remark 5.13legso 28117
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 35386
[Schwabhauser] p. 42Theorem 5.7seglerflx 35388
[Schwabhauser] p. 42Theorem 5.8segletr 35390
[Schwabhauser] p. 42Theorem 5.9segleantisym 35391
[Schwabhauser] p. 42Theorem 5.10seglelin 35392
[Schwabhauser] p. 42Theorem 5.11seglemin 35389
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 35394
[Schwabhauser] p. 42Proposition 5.7legid 28105
[Schwabhauser] p. 42Proposition 5.8legtrd 28107
[Schwabhauser] p. 42Proposition 5.9legtri3 28108
[Schwabhauser] p. 42Proposition 5.10legtrid 28109
[Schwabhauser] p. 42Proposition 5.11leg0 28110
[Schwabhauser] p. 43Theorem 6.2btwnoutside 35401
[Schwabhauser] p. 43Theorem 6.3broutsideof3 35402
[Schwabhauser] p. 43Theorem 6.4broutsideof 35397  df-outsideof 35396
[Schwabhauser] p. 43Definition 6.1broutsideof2 35398  ishlg 28120
[Schwabhauser] p. 44Theorem 6.4hlln 28125
[Schwabhauser] p. 44Theorem 6.5hlid 28127  outsideofrflx 35403
[Schwabhauser] p. 44Theorem 6.6hlcomb 28121  hlcomd 28122  outsideofcom 35404
[Schwabhauser] p. 44Theorem 6.7hltr 28128  outsideoftr 35405
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28136  outsideofeu 35407
[Schwabhauser] p. 44Definition 6.8df-ray 35414
[Schwabhauser] p. 45Part 2df-lines2 35415
[Schwabhauser] p. 45Theorem 6.13outsidele 35408
[Schwabhauser] p. 45Theorem 6.15lineunray 35423
[Schwabhauser] p. 45Theorem 6.16lineelsb2 35424  tglineelsb2 28150
[Schwabhauser] p. 45Theorem 6.17linecom 35426  linerflx1 35425  linerflx2 35427  tglinecom 28153  tglinerflx1 28151  tglinerflx2 28152
[Schwabhauser] p. 45Theorem 6.18linethru 35429  tglinethru 28154
[Schwabhauser] p. 45Definition 6.14df-line2 35413  tglng 28064
[Schwabhauser] p. 45Proposition 6.13legbtwn 28112
[Schwabhauser] p. 46Theorem 6.19linethrueu 35432  tglinethrueu 28157
[Schwabhauser] p. 46Theorem 6.21lineintmo 35433  tglineineq 28161  tglineinteq 28163  tglineintmo 28160
[Schwabhauser] p. 46Theorem 6.23colline 28167
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28168
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28169
[Schwabhauser] p. 49Theorem 7.3mirinv 28184
[Schwabhauser] p. 49Theorem 7.7mirmir 28180
[Schwabhauser] p. 49Theorem 7.8mirreu3 28172
[Schwabhauser] p. 49Definition 7.5df-mir 28171  ismir 28177  mirbtwn 28176  mircgr 28175  mirfv 28174  mirval 28173
[Schwabhauser] p. 50Theorem 7.8mirreu 28182
[Schwabhauser] p. 50Theorem 7.9mireq 28183
[Schwabhauser] p. 50Theorem 7.10mirinv 28184
[Schwabhauser] p. 50Theorem 7.11mirf1o 28187
[Schwabhauser] p. 50Theorem 7.13miriso 28188
[Schwabhauser] p. 51Theorem 7.14mirmot 28193
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28190  mirbtwni 28189
[Schwabhauser] p. 51Theorem 7.16mircgrs 28191
[Schwabhauser] p. 51Theorem 7.17miduniq 28203
[Schwabhauser] p. 52Lemma 7.21symquadlem 28207
[Schwabhauser] p. 52Theorem 7.18miduniq1 28204
[Schwabhauser] p. 52Theorem 7.19miduniq2 28205
[Schwabhauser] p. 52Theorem 7.20colmid 28206
[Schwabhauser] p. 53Lemma 7.22krippen 28209
[Schwabhauser] p. 55Lemma 7.25midexlem 28210
[Schwabhauser] p. 57Theorem 8.2ragcom 28216
[Schwabhauser] p. 57Definition 8.1df-rag 28212  israg 28215
[Schwabhauser] p. 58Theorem 8.3ragcol 28217
[Schwabhauser] p. 58Theorem 8.4ragmir 28218
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28220
[Schwabhauser] p. 58Theorem 8.6ragflat2 28221
[Schwabhauser] p. 58Theorem 8.7ragflat 28222
[Schwabhauser] p. 58Theorem 8.8ragtriva 28223
[Schwabhauser] p. 58Theorem 8.9ragflat3 28224  ragncol 28227
[Schwabhauser] p. 58Theorem 8.10ragcgr 28225
[Schwabhauser] p. 59Theorem 8.12perpcom 28231
[Schwabhauser] p. 59Theorem 8.13ragperp 28235
[Schwabhauser] p. 59Theorem 8.14perpneq 28232
[Schwabhauser] p. 59Definition 8.11df-perpg 28214  isperp 28230
[Schwabhauser] p. 59Definition 8.13isperp2 28233
[Schwabhauser] p. 60Theorem 8.18foot 28240
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28248  colperpexlem2 28249
[Schwabhauser] p. 63Theorem 8.21colperpex 28251  colperpexlem3 28250
[Schwabhauser] p. 64Theorem 8.22mideu 28256  midex 28255
[Schwabhauser] p. 66Lemma 8.24opphllem 28253
[Schwabhauser] p. 67Theorem 9.2oppcom 28262
[Schwabhauser] p. 67Definition 9.1islnopp 28257
[Schwabhauser] p. 68Lemma 9.3opphllem2 28266
[Schwabhauser] p. 68Lemma 9.4opphllem5 28269  opphllem6 28270
[Schwabhauser] p. 69Theorem 9.5opphl 28272
[Schwabhauser] p. 69Theorem 9.6axtgpasch 27985
[Schwabhauser] p. 70Theorem 9.6outpasch 28273
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28281
[Schwabhauser] p. 71Definition 9.7df-hpg 28276  hpgbr 28278
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28283
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28282
[Schwabhauser] p. 72Theorem 9.11hpgid 28284
[Schwabhauser] p. 72Theorem 9.12hpgcom 28285
[Schwabhauser] p. 72Theorem 9.13hpgtr 28286
[Schwabhauser] p. 73Theorem 9.18colopp 28287
[Schwabhauser] p. 73Theorem 9.19colhp 28288
[Schwabhauser] p. 88Theorem 10.2lmieu 28302
[Schwabhauser] p. 88Definition 10.1df-mid 28292
[Schwabhauser] p. 89Theorem 10.4lmicom 28306
[Schwabhauser] p. 89Theorem 10.5lmilmi 28307
[Schwabhauser] p. 89Theorem 10.6lmireu 28308
[Schwabhauser] p. 89Theorem 10.7lmieq 28309
[Schwabhauser] p. 89Theorem 10.8lmiinv 28310
[Schwabhauser] p. 89Theorem 10.9lmif1o 28313
[Schwabhauser] p. 89Theorem 10.10lmiiso 28315
[Schwabhauser] p. 89Definition 10.3df-lmi 28293
[Schwabhauser] p. 90Theorem 10.11lmimot 28316
[Schwabhauser] p. 91Theorem 10.12hypcgr 28319
[Schwabhauser] p. 92Theorem 10.14lmiopp 28320
[Schwabhauser] p. 92Theorem 10.15lnperpex 28321
[Schwabhauser] p. 92Theorem 10.16trgcopy 28322  trgcopyeu 28324
[Schwabhauser] p. 95Definition 11.2dfcgra2 28348
[Schwabhauser] p. 95Definition 11.3iscgra 28327
[Schwabhauser] p. 95Proposition 11.4cgracgr 28336
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28334  cgrahl2 28335
[Schwabhauser] p. 96Theorem 11.6cgraid 28337
[Schwabhauser] p. 96Theorem 11.9cgraswap 28338
[Schwabhauser] p. 97Theorem 11.7cgracom 28340
[Schwabhauser] p. 97Theorem 11.8cgratr 28341
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28344  cgrahl 28345
[Schwabhauser] p. 98Theorem 11.13sacgr 28349
[Schwabhauser] p. 98Theorem 11.14oacgr 28350
[Schwabhauser] p. 98Theorem 11.15acopy 28351  acopyeu 28352
[Schwabhauser] p. 101Theorem 11.24inagswap 28359
[Schwabhauser] p. 101Theorem 11.25inaghl 28363
[Schwabhauser] p. 101Definition 11.23isinag 28356
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28371
[Schwabhauser] p. 102Definition 11.27df-leag 28364  isleag 28365
[Schwabhauser] p. 107Theorem 11.49tgsas 28373  tgsas1 28372  tgsas2 28374  tgsas3 28375
[Schwabhauser] p. 108Theorem 11.50tgasa 28377  tgasa1 28376
[Schwabhauser] p. 109Theorem 11.51tgsss1 28378  tgsss2 28379  tgsss3 28380
[Shapiro] p. 230Theorem 6.5.1dchrhash 27010  dchrsum 27008  dchrsum2 27007  sumdchr 27011
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27012  sum2dchr 27013
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19977  ablfacrp2 19978
[Shapiro], p. 328Equation 9.2.4vmasum 26955
[Shapiro], p. 329Equation 9.2.7logfac2 26956
[Shapiro], p. 329Equation 9.2.9logfacrlim 26963
[Shapiro], p. 331Equation 9.2.13vmadivsum 27221
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27224
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27278  vmalogdivsum2 27277
[Shapiro], p. 375Theorem 9.4.1dirith 27268  dirith2 27267
[Shapiro], p. 375Equation 9.4.3rplogsum 27266  rpvmasum 27265  rpvmasum2 27251
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27226
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27264
[Shapiro], p. 377Lemma 9.4.1dchrisum 27231  dchrisumlem1 27228  dchrisumlem2 27229  dchrisumlem3 27230  dchrisumlema 27227
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27234
[Shapiro], p. 379Equation 9.4.16dchrmusum 27263  dchrmusumlem 27261  dchrvmasumlem 27262
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27233
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27235
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27259  dchrisum0re 27252  dchrisumn0 27260
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27245
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27249
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27250
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27305  pntrsumbnd2 27306  pntrsumo1 27304
[Shapiro], p. 405Equation 10.2.1mudivsum 27269
[Shapiro], p. 406Equation 10.2.6mulogsum 27271
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27273
[Shapiro], p. 407Equation 10.2.8mulog2sum 27276
[Shapiro], p. 418Equation 10.4.6logsqvma 27281
[Shapiro], p. 418Equation 10.4.8logsqvma2 27282
[Shapiro], p. 419Equation 10.4.10selberg 27287
[Shapiro], p. 420Equation 10.4.12selberg2lem 27289
[Shapiro], p. 420Equation 10.4.14selberg2 27290
[Shapiro], p. 422Equation 10.6.7selberg3 27298
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27299
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27296  selberg3lem2 27297
[Shapiro], p. 422Equation 10.4.23selberg4 27300
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27294
[Shapiro], p. 428Equation 10.6.2selbergr 27307
[Shapiro], p. 429Equation 10.6.8selberg3r 27308
[Shapiro], p. 430Equation 10.6.11selberg4r 27309
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27323
[Shapiro], p. 434Equation 10.6.27pntlema 27335  pntlemb 27336  pntlemc 27334  pntlemd 27333  pntlemg 27337
[Shapiro], p. 435Equation 10.6.29pntlema 27335
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27327
[Shapiro], p. 436Lemma 10.6.2pntibnd 27332
[Shapiro], p. 436Equation 10.6.34pntlema 27335
[Shapiro], p. 436Equation 10.6.35pntlem3 27348  pntleml 27350
[Stoll] p. 13Definition corresponds to dfsymdif3 4295
[Stoll] p. 16Exercise 4.40dif 4400  dif0 4371
[Stoll] p. 16Exercise 4.8difdifdir 4490
[Stoll] p. 17Theorem 5.1(5)unvdif 4473
[Stoll] p. 19Theorem 5.2(13)undm 4286
[Stoll] p. 19Theorem 5.2(13')indm 4287
[Stoll] p. 20Remarkinvdif 4267
[Stoll] p. 25Definition of ordered tripledf-ot 4636
[Stoll] p. 43Definitionuniiun 5060
[Stoll] p. 44Definitionintiin 5061
[Stoll] p. 45Definitiondf-iin 4999
[Stoll] p. 45Definition indexed uniondf-iun 4998
[Stoll] p. 176Theorem 3.4(27)iman 400
[Stoll] p. 262Example 4.1dfsymdif3 4295
[Strang] p. 242Section 6.3expgrowth 43396
[Suppes] p. 22Theorem 2eq0 4342  eq0f 4339
[Suppes] p. 22Theorem 4eqss 3996  eqssd 3998  eqssi 3997
[Suppes] p. 23Theorem 5ss0 4397  ss0b 4396
[Suppes] p. 23Theorem 6sstr 3989  sstrALT2 43898
[Suppes] p. 23Theorem 7pssirr 4099
[Suppes] p. 23Theorem 8pssn2lp 4100
[Suppes] p. 23Theorem 9psstr 4103
[Suppes] p. 23Theorem 10pssss 4094
[Suppes] p. 25Theorem 12elin 3963  elun 4147
[Suppes] p. 26Theorem 15inidm 4217
[Suppes] p. 26Theorem 16in0 4390
[Suppes] p. 27Theorem 23unidm 4151
[Suppes] p. 27Theorem 24un0 4389
[Suppes] p. 27Theorem 25ssun1 4171
[Suppes] p. 27Theorem 26ssequn1 4179
[Suppes] p. 27Theorem 27unss 4183
[Suppes] p. 27Theorem 28indir 4274
[Suppes] p. 27Theorem 29undir 4275
[Suppes] p. 28Theorem 32difid 4369
[Suppes] p. 29Theorem 33difin 4260
[Suppes] p. 29Theorem 34indif 4268
[Suppes] p. 29Theorem 35undif1 4474
[Suppes] p. 29Theorem 36difun2 4479
[Suppes] p. 29Theorem 37difin0 4472
[Suppes] p. 29Theorem 38disjdif 4470
[Suppes] p. 29Theorem 39difundi 4278
[Suppes] p. 29Theorem 40difindi 4280
[Suppes] p. 30Theorem 41nalset 5312
[Suppes] p. 39Theorem 61uniss 4915
[Suppes] p. 39Theorem 65uniop 5514
[Suppes] p. 41Theorem 70intsn 4989
[Suppes] p. 42Theorem 71intpr 4985  intprg 4984
[Suppes] p. 42Theorem 73op1stb 5470
[Suppes] p. 42Theorem 78intun 4983
[Suppes] p. 44Definition 15(a)dfiun2 5035  dfiun2g 5032
[Suppes] p. 44Definition 15(b)dfiin2 5036
[Suppes] p. 47Theorem 86elpw 4605  elpw2 5344  elpw2g 5343  elpwg 4604  elpwgdedVD 43980
[Suppes] p. 47Theorem 87pwid 4623
[Suppes] p. 47Theorem 89pw0 4814
[Suppes] p. 48Theorem 90pwpw0 4815
[Suppes] p. 52Theorem 101xpss12 5690
[Suppes] p. 52Theorem 102xpindi 5832  xpindir 5833
[Suppes] p. 52Theorem 103xpundi 5743  xpundir 5744
[Suppes] p. 54Theorem 105elirrv 9593
[Suppes] p. 58Theorem 2relss 5780
[Suppes] p. 59Theorem 4eldm 5899  eldm2 5900  eldm2g 5898  eldmg 5897
[Suppes] p. 59Definition 3df-dm 5685
[Suppes] p. 60Theorem 6dmin 5910
[Suppes] p. 60Theorem 8rnun 6144
[Suppes] p. 60Theorem 9rnin 6145
[Suppes] p. 60Definition 4dfrn2 5887
[Suppes] p. 61Theorem 11brcnv 5881  brcnvg 5878
[Suppes] p. 62Equation 5elcnv 5875  elcnv2 5876
[Suppes] p. 62Theorem 12relcnv 6102
[Suppes] p. 62Theorem 15cnvin 6143
[Suppes] p. 62Theorem 16cnvun 6141
[Suppes] p. 63Definitiondftrrels2 37748
[Suppes] p. 63Theorem 20co02 6258
[Suppes] p. 63Theorem 21dmcoss 5969
[Suppes] p. 63Definition 7df-co 5684
[Suppes] p. 64Theorem 26cnvco 5884
[Suppes] p. 64Theorem 27coass 6263
[Suppes] p. 65Theorem 31resundi 5994
[Suppes] p. 65Theorem 34elima 6063  elima2 6064  elima3 6065  elimag 6062
[Suppes] p. 65Theorem 35imaundi 6148
[Suppes] p. 66Theorem 40dminss 6151
[Suppes] p. 66Theorem 41imainss 6152
[Suppes] p. 67Exercise 11cnvxp 6155
[Suppes] p. 81Definition 34dfec2 8708
[Suppes] p. 82Theorem 72elec 8749  elecALTV 37437  elecg 8748
[Suppes] p. 82Theorem 73eqvrelth 37784  erth 8754  erth2 8755
[Suppes] p. 83Theorem 74eqvreldisj 37787  erdisj 8757
[Suppes] p. 83Definition 35, df-parts 37938  dfmembpart2 37943
[Suppes] p. 89Theorem 96map0b 8879
[Suppes] p. 89Theorem 97map0 8883  map0g 8880
[Suppes] p. 89Theorem 98mapsn 8884  mapsnd 8882
[Suppes] p. 89Theorem 99mapss 8885
[Suppes] p. 91Definition 12(ii)alephsuc 10065
[Suppes] p. 91Definition 12(iii)alephlim 10064
[Suppes] p. 92Theorem 1enref 8983  enrefg 8982
[Suppes] p. 92Theorem 2ensym 9001  ensymb 9000  ensymi 9002
[Suppes] p. 92Theorem 3entr 9004
[Suppes] p. 92Theorem 4unen 9048
[Suppes] p. 94Theorem 15endom 8977
[Suppes] p. 94Theorem 16ssdomg 8998
[Suppes] p. 94Theorem 17domtr 9005
[Suppes] p. 95Theorem 18sbth 9095
[Suppes] p. 97Theorem 23canth2 9132  canth2g 9133
[Suppes] p. 97Definition 3brsdom2 9099  df-sdom 8944  dfsdom2 9098
[Suppes] p. 97Theorem 21(i)sdomirr 9116
[Suppes] p. 97Theorem 22(i)domnsym 9101
[Suppes] p. 97Theorem 21(ii)sdomnsym 9100
[Suppes] p. 97Theorem 22(ii)domsdomtr 9114
[Suppes] p. 97Theorem 22(iv)brdom2 8980
[Suppes] p. 97Theorem 21(iii)sdomtr 9117
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9112
[Suppes] p. 98Exercise 4fundmen 9033  fundmeng 9034
[Suppes] p. 98Exercise 6xpdom3 9072
[Suppes] p. 98Exercise 11sdomentr 9113
[Suppes] p. 104Theorem 37fofi 9340
[Suppes] p. 104Theorem 38pwfi 9180
[Suppes] p. 105Theorem 40pwfi 9180
[Suppes] p. 111Axiom for cardinal numberscarden 10548
[Suppes] p. 130Definition 3df-tr 5265
[Suppes] p. 132Theorem 9ssonuni 7769
[Suppes] p. 134Definition 6df-suc 6369
[Suppes] p. 136Theorem Schema 22findes 7895  finds 7891  finds1 7894  finds2 7893
[Suppes] p. 151Theorem 42isfinite 9649  isfinite2 9303  isfiniteg 9306  unbnn 9301
[Suppes] p. 162Definition 5df-ltnq 10915  df-ltpq 10907
[Suppes] p. 197Theorem Schema 4tfindes 7854  tfinds 7851  tfinds2 7855
[Suppes] p. 209Theorem 18oaord1 8553
[Suppes] p. 209Theorem 21oaword2 8555
[Suppes] p. 211Theorem 25oaass 8563
[Suppes] p. 225Definition 8iscard2 9973
[Suppes] p. 227Theorem 56ondomon 10560
[Suppes] p. 228Theorem 59harcard 9975
[Suppes] p. 228Definition 12(i)aleph0 10063
[Suppes] p. 228Theorem Schema 61onintss 6414
[Suppes] p. 228Theorem Schema 62onminesb 7783  onminsb 7784
[Suppes] p. 229Theorem 64alephval2 10569
[Suppes] p. 229Theorem 65alephcard 10067
[Suppes] p. 229Theorem 66alephord2i 10074
[Suppes] p. 229Theorem 67alephnbtwn 10068
[Suppes] p. 229Definition 12df-aleph 9937
[Suppes] p. 242Theorem 6weth 10492
[Suppes] p. 242Theorem 8entric 10554
[Suppes] p. 242Theorem 9carden 10548
[Szendrei] p. 11Line 6df-cloneop 34969
[Szendrei] p. 11Paragraph 3df-suppos 34973
[TakeutiZaring] p. 8Axiom 1ax-ext 2701
[TakeutiZaring] p. 13Definition 4.5df-cleq 2722
[TakeutiZaring] p. 13Proposition 4.6df-clel 2808
[TakeutiZaring] p. 13Proposition 4.9cvjust 2724
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2753
[TakeutiZaring] p. 14Definition 4.16df-oprab 7415
[TakeutiZaring] p. 14Proposition 4.14ru 3775
[TakeutiZaring] p. 15Axiom 2zfpair 5418
[TakeutiZaring] p. 15Exercise 1elpr 4650  elpr2 4652  elpr2g 4651  elprg 4648
[TakeutiZaring] p. 15Exercise 2elsn 4642  elsn2 4666  elsn2g 4665  elsng 4641  velsn 4643
[TakeutiZaring] p. 15Exercise 3elop 5466
[TakeutiZaring] p. 15Exercise 4sneq 4637  sneqr 4840
[TakeutiZaring] p. 15Definition 5.1dfpr2 4646  dfsn2 4640  dfsn2ALT 4647
[TakeutiZaring] p. 16Axiom 3uniex 7733
[TakeutiZaring] p. 16Exercise 6opth 5475
[TakeutiZaring] p. 16Exercise 7opex 5463
[TakeutiZaring] p. 16Exercise 8rext 5447
[TakeutiZaring] p. 16Corollary 5.8unex 7735  unexg 7738
[TakeutiZaring] p. 16Definition 5.3dftp2 4692
[TakeutiZaring] p. 16Definition 5.5df-uni 4908
[TakeutiZaring] p. 16Definition 5.6df-in 3954  df-un 3952
[TakeutiZaring] p. 16Proposition 5.7unipr 4925  uniprg 4924
[TakeutiZaring] p. 17Axiom 4vpwex 5374
[TakeutiZaring] p. 17Exercise 1eltp 4691
[TakeutiZaring] p. 17Exercise 5elsuc 6433  elsucg 6431  sstr2 3988
[TakeutiZaring] p. 17Exercise 6uncom 4152
[TakeutiZaring] p. 17Exercise 7incom 4200
[TakeutiZaring] p. 17Exercise 8unass 4165
[TakeutiZaring] p. 17Exercise 9inass 4218
[TakeutiZaring] p. 17Exercise 10indi 4272
[TakeutiZaring] p. 17Exercise 11undi 4273
[TakeutiZaring] p. 17Definition 5.9df-pss 3966  dfss2 3967
[TakeutiZaring] p. 17Definition 5.10df-pw 4603
[TakeutiZaring] p. 18Exercise 7unss2 4180
[TakeutiZaring] p. 18Exercise 9df-ss 3964  sseqin2 4214
[TakeutiZaring] p. 18Exercise 10ssid 4003
[TakeutiZaring] p. 18Exercise 12inss1 4227  inss2 4228
[TakeutiZaring] p. 18Exercise 13nss 4045
[TakeutiZaring] p. 18Exercise 15unieq 4918
[TakeutiZaring] p. 18Exercise 18sspwb 5448  sspwimp 43981  sspwimpALT 43988  sspwimpALT2 43991  sspwimpcf 43983
[TakeutiZaring] p. 18Exercise 19pweqb 5455
[TakeutiZaring] p. 19Axiom 5ax-rep 5284
[TakeutiZaring] p. 20Definitiondf-rab 3431
[TakeutiZaring] p. 20Corollary 5.160ex 5306
[TakeutiZaring] p. 20Definition 5.12df-dif 3950
[TakeutiZaring] p. 20Definition 5.14dfnul2 4324
[TakeutiZaring] p. 20Proposition 5.15difid 4369
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4345  n0f 4341  neq0 4344  neq0f 4340
[TakeutiZaring] p. 21Axiom 6zfreg 9592
[TakeutiZaring] p. 21Axiom 6'zfregs 9729
[TakeutiZaring] p. 21Theorem 5.22setind 9731
[TakeutiZaring] p. 21Definition 5.20df-v 3474
[TakeutiZaring] p. 21Proposition 5.21vprc 5314
[TakeutiZaring] p. 22Exercise 10ss 4395
[TakeutiZaring] p. 22Exercise 3ssex 5320  ssexg 5322
[TakeutiZaring] p. 22Exercise 4inex1 5316
[TakeutiZaring] p. 22Exercise 5ruv 9599
[TakeutiZaring] p. 22Exercise 6elirr 9594
[TakeutiZaring] p. 22Exercise 7ssdif0 4362
[TakeutiZaring] p. 22Exercise 11difdif 4129
[TakeutiZaring] p. 22Exercise 13undif3 4289  undif3VD 43945
[TakeutiZaring] p. 22Exercise 14difss 4130
[TakeutiZaring] p. 22Exercise 15sscon 4137
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3060
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3069
[TakeutiZaring] p. 23Proposition 6.2xpex 7742  xpexg 7739
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5682
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6618
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6796  fun11 6621
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6558  svrelfun 6619
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5886
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5888
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5687
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5688
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5684
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6192  dfrel2 6187
[TakeutiZaring] p. 25Exercise 3xpss 5691
[TakeutiZaring] p. 25Exercise 5relun 5810
[TakeutiZaring] p. 25Exercise 6reluni 5817
[TakeutiZaring] p. 25Exercise 9inxp 5831
[TakeutiZaring] p. 25Exercise 12relres 6009
[TakeutiZaring] p. 25Exercise 13opelres 5986  opelresi 5988
[TakeutiZaring] p. 25Exercise 14dmres 6002
[TakeutiZaring] p. 25Exercise 15resss 6005
[TakeutiZaring] p. 25Exercise 17resabs1 6010
[TakeutiZaring] p. 25Exercise 18funres 6589
[TakeutiZaring] p. 25Exercise 24relco 6106
[TakeutiZaring] p. 25Exercise 29funco 6587
[TakeutiZaring] p. 25Exercise 30f1co 6798
[TakeutiZaring] p. 26Definition 6.10eu2 2603
[TakeutiZaring] p. 26Definition 6.11conventions 29920  df-fv 6550  fv3 6908
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7918  cnvexg 7917
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7904  dmexg 7896
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7905  rnexg 7897
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 43515
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7913
[TakeutiZaring] p. 27Corollary 6.13fvex 6903
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 46180  tz6.12-1-afv2 46247  tz6.12-1 6913  tz6.12-afv 46179  tz6.12-afv2 46246  tz6.12 6915  tz6.12c-afv2 46248  tz6.12c 6912
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 46243  tz6.12-2 6878  tz6.12i-afv2 46249  tz6.12i 6918
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6545
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6546
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6548  wfo 6540
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6547  wf1 6539
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6549  wf1o 6541
[TakeutiZaring] p. 28Exercise 4eqfnfv 7031  eqfnfv2 7032  eqfnfv2f 7035
[TakeutiZaring] p. 28Exercise 5fvco 6988
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7220
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7218
[TakeutiZaring] p. 29Exercise 9funimaex 6635  funimaexg 6633
[TakeutiZaring] p. 29Definition 6.18df-br 5148
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5588
[TakeutiZaring] p. 30Definition 6.21dffr2 5639  dffr3 6097  eliniseg 6092  iniseg 6095
[TakeutiZaring] p. 30Definition 6.22df-eprel 5579
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5653  fr3nr 7761  frirr 5652
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5630
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7763
[TakeutiZaring] p. 31Exercise 1frss 5642
[TakeutiZaring] p. 31Exercise 4wess 5662
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6347  tz6.26i 6349  wefrc 5669  wereu2 5672
[TakeutiZaring] p. 32Theorem 6.27wfi 6350  wfii 6352
[TakeutiZaring] p. 32Definition 6.28df-isom 6551
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7328
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7329
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7335
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7336
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7337
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7341
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7348
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7350
[TakeutiZaring] p. 35Notationwtr 5264
[TakeutiZaring] p. 35Theorem 7.2trelpss 43516  tz7.2 5659
[TakeutiZaring] p. 35Definition 7.1dftr3 5270
[TakeutiZaring] p. 36Proposition 7.4ordwe 6376
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6384
[TakeutiZaring] p. 36Proposition 7.6ordelord 6385  ordelordALT 43600  ordelordALTVD 43930
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6391  ordelssne 6390
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6389
[TakeutiZaring] p. 37Proposition 7.9ordin 6393
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7771
[TakeutiZaring] p. 38Corollary 7.15ordsson 7772
[TakeutiZaring] p. 38Definition 7.11df-on 6367
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6395
[TakeutiZaring] p. 38Proposition 7.12onfrALT 43612  ordon 7766
[TakeutiZaring] p. 38Proposition 7.13onprc 7767
[TakeutiZaring] p. 39Theorem 7.17tfi 7844
[TakeutiZaring] p. 40Exercise 3ontr2 6410
[TakeutiZaring] p. 40Exercise 7dftr2 5266
[TakeutiZaring] p. 40Exercise 9onssmin 7782
[TakeutiZaring] p. 40Exercise 11unon 7821
[TakeutiZaring] p. 40Exercise 12ordun 6467
[TakeutiZaring] p. 40Exercise 14ordequn 6466
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7768
[TakeutiZaring] p. 40Proposition 7.20elssuni 4940
[TakeutiZaring] p. 41Definition 7.22df-suc 6369
[TakeutiZaring] p. 41Proposition 7.23sssucid 6443  sucidg 6444
[TakeutiZaring] p. 41Proposition 7.24onsuc 7801
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6457  ordnbtwn 6456
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7818
[TakeutiZaring] p. 42Exercise 1df-lim 6368
[TakeutiZaring] p. 42Exercise 4omssnlim 7872
[TakeutiZaring] p. 42Exercise 7ssnlim 7877
[TakeutiZaring] p. 42Exercise 8onsucssi 7832  ordelsuc 7810
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7812
[TakeutiZaring] p. 42Definition 7.27nlimon 7842
[TakeutiZaring] p. 42Definition 7.28dfom2 7859
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7881
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7883
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7884
[TakeutiZaring] p. 43Remarkomon 7869
[TakeutiZaring] p. 43Axiom 7inf3 9632  omex 9640
[TakeutiZaring] p. 43Theorem 7.32ordom 7867
[TakeutiZaring] p. 43Corollary 7.31find 7889
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7885
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7886
[TakeutiZaring] p. 44Exercise 1limomss 7862
[TakeutiZaring] p. 44Exercise 2int0 4965
[TakeutiZaring] p. 44Exercise 3trintss 5283
[TakeutiZaring] p. 44Exercise 4intss1 4966
[TakeutiZaring] p. 44Exercise 5intex 5336
[TakeutiZaring] p. 44Exercise 6oninton 7785
[TakeutiZaring] p. 44Exercise 11ordintdif 6413
[TakeutiZaring] p. 44Definition 7.35df-int 4950
[TakeutiZaring] p. 44Proposition 7.34noinfep 9657
[TakeutiZaring] p. 45Exercise 4onint 7780
[TakeutiZaring] p. 47Lemma 1tfrlem1 8378
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8399
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8400
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8401
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8408  tz7.44-2 8409  tz7.44-3 8410
[TakeutiZaring] p. 50Exercise 1smogt 8369
[TakeutiZaring] p. 50Exercise 3smoiso 8364
[TakeutiZaring] p. 50Definition 7.46df-smo 8348
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8447  tz7.49c 8448
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8445
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8444
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8446
[TakeutiZaring] p. 53Proposition 7.532eu5 2649
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10008
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10009
[TakeutiZaring] p. 56Definition 8.1oalim 8534  oasuc 8526
[TakeutiZaring] p. 57Remarktfindsg 7852
[TakeutiZaring] p. 57Proposition 8.2oacl 8537
[TakeutiZaring] p. 57Proposition 8.3oa0 8518  oa0r 8540
[TakeutiZaring] p. 57Proposition 8.16omcl 8538
[TakeutiZaring] p. 58Corollary 8.5oacan 8550
[TakeutiZaring] p. 58Proposition 8.4nnaord 8621  nnaordi 8620  oaord 8549  oaordi 8548
[TakeutiZaring] p. 59Proposition 8.6iunss2 5051  uniss2 4944
[TakeutiZaring] p. 59Proposition 8.7oawordri 8552
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8557  oawordex 8559
[TakeutiZaring] p. 59Proposition 8.9nnacl 8613
[TakeutiZaring] p. 59Proposition 8.10oaabs 8649
[TakeutiZaring] p. 60Remarkoancom 9648
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8562
[TakeutiZaring] p. 62Exercise 1nnarcl 8618
[TakeutiZaring] p. 62Exercise 5oaword1 8554
[TakeutiZaring] p. 62Definition 8.15om0x 8521  omlim 8535  omsuc 8528
[TakeutiZaring] p. 62Definition 8.15(a)om0 8519
[TakeutiZaring] p. 63Proposition 8.17nnecl 8615  nnmcl 8614
[TakeutiZaring] p. 63Proposition 8.19nnmord 8634  nnmordi 8633  omord 8570  omordi 8568
[TakeutiZaring] p. 63Proposition 8.20omcan 8571
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8638  omwordri 8574
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8541
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8544  om1r 8545
[TakeutiZaring] p. 64Proposition 8.22om00 8577
[TakeutiZaring] p. 64Proposition 8.23omordlim 8579
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8580
[TakeutiZaring] p. 64Proposition 8.25odi 8581
[TakeutiZaring] p. 65Theorem 8.26omass 8582
[TakeutiZaring] p. 67Definition 8.30nnesuc 8610  oe0 8524  oelim 8536  oesuc 8529  onesuc 8532
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8522
[TakeutiZaring] p. 67Proposition 8.32oen0 8588
[TakeutiZaring] p. 67Proposition 8.33oeordi 8589
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8523
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8547
[TakeutiZaring] p. 68Corollary 8.34oeord 8590
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8596
[TakeutiZaring] p. 68Proposition 8.35oewordri 8594
[TakeutiZaring] p. 68Proposition 8.37oeworde 8595
[TakeutiZaring] p. 69Proposition 8.41oeoa 8599
[TakeutiZaring] p. 70Proposition 8.42oeoe 8601
[TakeutiZaring] p. 73Theorem 9.1trcl 9725  tz9.1 9726
[TakeutiZaring] p. 76Definition 9.9df-r1 9761  r10 9765  r1lim 9769  r1limg 9768  r1suc 9767  r1sucg 9766
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9777  r1ord2 9778  r1ordg 9775
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9787
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9812  tz9.13 9788  tz9.13g 9789
[TakeutiZaring] p. 79Definition 9.14df-rank 9762  rankval 9813  rankvalb 9794  rankvalg 9814
[TakeutiZaring] p. 79Proposition 9.16rankel 9836  rankelb 9821
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9850  rankval3 9837  rankval3b 9823
[TakeutiZaring] p. 79Proposition 9.18rankonid 9826
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9792
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9831  rankr1c 9818  rankr1g 9829
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9832
[TakeutiZaring] p. 80Exercise 1rankss 9846  rankssb 9845
[TakeutiZaring] p. 80Exercise 2unbndrank 9839
[TakeutiZaring] p. 80Proposition 9.19bndrank 9838
[TakeutiZaring] p. 83Axiom of Choiceac4 10472  dfac3 10118
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10027  numth 10469  numth2 10468
[TakeutiZaring] p. 85Definition 10.4cardval 10543
[TakeutiZaring] p. 85Proposition 10.5cardid 10544  cardid2 9950
[TakeutiZaring] p. 85Proposition 10.9oncard 9957
[TakeutiZaring] p. 85Proposition 10.10carden 10548
[TakeutiZaring] p. 85Proposition 10.11cardidm 9956
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9941
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9962
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9954
[TakeutiZaring] p. 87Proposition 10.15pwen 9152
[TakeutiZaring] p. 88Exercise 1en0 9015
[TakeutiZaring] p. 88Exercise 7infensuc 9157
[TakeutiZaring] p. 89Exercise 10omxpen 9076
[TakeutiZaring] p. 90Corollary 10.23cardnn 9960
[TakeutiZaring] p. 90Definition 10.27alephiso 10095
[TakeutiZaring] p. 90Proposition 10.20nneneq 9211
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9230
[TakeutiZaring] p. 90Proposition 10.26alephprc 10096
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9216
[TakeutiZaring] p. 91Exercise 2alephle 10085
[TakeutiZaring] p. 91Exercise 3aleph0 10063
[TakeutiZaring] p. 91Exercise 4cardlim 9969
[TakeutiZaring] p. 91Exercise 7infpss 10214
[TakeutiZaring] p. 91Exercise 8infcntss 9323
[TakeutiZaring] p. 91Definition 10.29df-fin 8945  isfi 8974
[TakeutiZaring] p. 92Proposition 10.32onfin 9232
[TakeutiZaring] p. 92Proposition 10.34imadomg 10531
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9069
[TakeutiZaring] p. 93Proposition 10.35fodomb 10523
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10182  unxpdom 9255
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9971  cardsdomelir 9970
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9257
[TakeutiZaring] p. 94Proposition 10.39infxpen 10011
[TakeutiZaring] p. 95Definition 10.42df-map 8824
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10559  infxpidm2 10014
[TakeutiZaring] p. 95Proposition 10.41infdju 10205  infxp 10212
[TakeutiZaring] p. 96Proposition 10.44pw2en 9081  pw2f1o 9079
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9145
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10484
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10479  ac6s5 10488
[TakeutiZaring] p. 98Theorem 10.47unidom 10540
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10541  uniimadomf 10542
[TakeutiZaring] p. 100Definition 11.1cfcof 10271
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10266
[TakeutiZaring] p. 102Exercise 1cfle 10251
[TakeutiZaring] p. 102Exercise 2cf0 10248
[TakeutiZaring] p. 102Exercise 3cfsuc 10254
[TakeutiZaring] p. 102Exercise 4cfom 10261
[TakeutiZaring] p. 102Proposition 11.9coftr 10270
[TakeutiZaring] p. 103Theorem 11.15alephreg 10579
[TakeutiZaring] p. 103Proposition 11.11cardcf 10249
[TakeutiZaring] p. 103Proposition 11.13alephsing 10273
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10094
[TakeutiZaring] p. 104Proposition 11.16carduniima 10093
[TakeutiZaring] p. 104Proposition 11.18alephfp 10105  alephfp2 10106
[TakeutiZaring] p. 106Theorem 11.20gchina 10696
[TakeutiZaring] p. 106Theorem 11.21mappwen 10109
[TakeutiZaring] p. 107Theorem 11.26konigth 10566
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10580
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10581
[Tarski] p. 67Axiom B5ax-c5 38056
[Tarski] p. 67Scheme B5sp 2174
[Tarski] p. 68Lemma 6avril1 29983  equid 2013
[Tarski] p. 69Lemma 7equcomi 2018
[Tarski] p. 70Lemma 14spim 2384  spime 2386  spimew 1973
[Tarski] p. 70Lemma 16ax-12 2169  ax-c15 38062  ax12i 1968
[Tarski] p. 70Lemmas 16 and 17sb6 2086
[Tarski] p. 75Axiom B7ax6v 1970
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1911  ax5ALT 38080
[Tarski], p. 75Scheme B8 of system S2ax-7 2009  ax-8 2106  ax-9 2114
[Tarski1999] p. 178Axiom 4axtgsegcon 27982
[Tarski1999] p. 178Axiom 5axtg5seg 27983
[Tarski1999] p. 179Axiom 7axtgpasch 27985
[Tarski1999] p. 180Axiom 7.1axtgpasch 27985
[Tarski1999] p. 185Axiom 11axtgcont1 27986
[Truss] p. 114Theorem 5.18ruc 16190
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 36830
[Viaclovsky8] p. 3Proposition 7ismblfin 36832
[Weierstrass] p. 272Definitiondf-mdet 22307  mdetuni 22344
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 900
[WhiteheadRussell] p. 96Axiom *1.3olc 864
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 865
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 916
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 964
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 188
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 135
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 90  wl-luk-pm2.04 36629
[WhiteheadRussell] p. 100Theorem *2.05frege5 42853  imim2 58  wl-luk-imim2 36624
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 46027  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 893
[WhiteheadRussell] p. 101Theorem *2.06barbara 2656  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 899
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 36627
[WhiteheadRussell] p. 101Theorem *2.11exmid 891
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 894
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 43990  wl-luk-notnotr 36628
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 42883  axfrege28 42882  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 863
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 921
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 36621
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 886
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 936
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 29921  pm2.27 42  wl-luk-pm2.27 36619
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 919
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 37535
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 920
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 966
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 967
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 965
[WhiteheadRussell] p. 105Definition *2.33df-3or 1086
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 903
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 904
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 939
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 878
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 879
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 190
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 880
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 881
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 882
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 847
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 848
[WhiteheadRussell] p. 107Theorem *2.55orel1 885
[WhiteheadRussell] p. 107Theorem *2.56orel2 887
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 191
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 896
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 937
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 938
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 192
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 888  pm2.67 889
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 895
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 969
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 897
[WhiteheadRussell] p. 108Theorem *2.69looinv 202
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 970
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 971
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 930
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 928
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 968
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 972
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 929
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 988
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 468  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 989
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 990
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 991
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 992
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 470
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 458
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 401
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 799
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 447
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 448
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 481  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 483  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 761
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 762
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 804
[WhiteheadRussell] p. 113Fact)pm3.45 620
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 806
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 491
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 492
[WhiteheadRussell] p. 113Theorem *3.44jao 957  pm3.44 956
[WhiteheadRussell] p. 113Theorem *3.47anim12 805
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 472
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 960
[WhiteheadRussell] p. 116Theorem *4.1con34b 315
[WhiteheadRussell] p. 117Theorem *4.2biid 260
[WhiteheadRussell] p. 117Theorem *4.11notbi 318
[WhiteheadRussell] p. 117Theorem *4.12con2bi 352
[WhiteheadRussell] p. 117Theorem *4.13notnotb 314
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 803
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 829
[WhiteheadRussell] p. 117Theorem *4.21bicom 221
[WhiteheadRussell] p. 117Theorem *4.22biantr 802  bitr 801
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 562
[WhiteheadRussell] p. 117Theorem *4.25oridm 901  pm4.25 902
[WhiteheadRussell] p. 118Theorem *4.3ancom 459
[WhiteheadRussell] p. 118Theorem *4.4andi 1004
[WhiteheadRussell] p. 118Theorem *4.31orcom 866
[WhiteheadRussell] p. 118Theorem *4.32anass 467
[WhiteheadRussell] p. 118Theorem *4.33orass 918
[WhiteheadRussell] p. 118Theorem *4.36anbi1 630
[WhiteheadRussell] p. 118Theorem *4.37orbi1 914
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 634
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 973
[WhiteheadRussell] p. 118Definition *4.34df-3an 1087
[WhiteheadRussell] p. 119Theorem *4.41ordi 1002
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1050
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1019
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 993
[WhiteheadRussell] p. 119Theorem *4.45orabs 995  pm4.45 994  pm4.45im 824
[WhiteheadRussell] p. 120Theorem *4.5anor 979
[WhiteheadRussell] p. 120Theorem *4.6imor 849
[WhiteheadRussell] p. 120Theorem *4.7anclb 544
[WhiteheadRussell] p. 120Theorem *4.51ianor 978
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 981
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 982
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 983
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 984
[WhiteheadRussell] p. 120Theorem *4.56ioran 980  pm4.56 985
[WhiteheadRussell] p. 120Theorem *4.57oran 986  pm4.57 987
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 403
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 852
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 396
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 845
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 404
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 846
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 397
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 556  pm4.71d 560  pm4.71i 558  pm4.71r 557  pm4.71rd 561  pm4.71ri 559
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 946
[WhiteheadRussell] p. 121Theorem *4.73iba 526
[WhiteheadRussell] p. 121Theorem *4.74biorf 933
[WhiteheadRussell] p. 121Theorem *4.76jcab 516  pm4.76 517
[WhiteheadRussell] p. 121Theorem *4.77jaob 958  pm4.77 959
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 931
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1000
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 391
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 392
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1020
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1021
[WhiteheadRussell] p. 122Theorem *4.84imbi1 346
[WhiteheadRussell] p. 122Theorem *4.85imbi2 347
[WhiteheadRussell] p. 122Theorem *4.86bibi1 350
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 386  impexp 449  pm4.87 839
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 820
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 941  pm5.11g 940
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 942
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 944
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 943
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1009
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1010
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1008
[WhiteheadRussell] p. 124Theorem *5.18nbbn 382  pm5.18 380
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 385
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 821
[WhiteheadRussell] p. 124Theorem *5.22xor 1011
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1046
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1047
[WhiteheadRussell] p. 124Theorem *5.25dfor2 898
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 571
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 387
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 360
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 998
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 950
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 827
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 572
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 832
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 822
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 830
[WhiteheadRussell] p. 125Theorem *5.41imdi 388  pm5.41 389
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 542
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 541
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1001
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1014
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 945
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 997
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1015
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1016
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1024
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 365
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 269
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1025
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 43419
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 43420
[WhiteheadRussell] p. 147Theorem *10.2219.26 1871
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 43421
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 43422
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 43423
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1894
[WhiteheadRussell] p. 151Theorem *10.301albitr 43424
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 43425
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 43426
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 43427
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 43428
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 43430
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 43431
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 43432
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 43429
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2091
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 43435
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 43436
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2071
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2155
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1829
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1830
[WhiteheadRussell] p. 161Theorem *11.319.21vv 43437
[WhiteheadRussell] p. 162Theorem *11.322alim 43438
[WhiteheadRussell] p. 162Theorem *11.332albi 43439
[WhiteheadRussell] p. 162Theorem *11.342exim 43440
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 43442
[WhiteheadRussell] p. 162Theorem *11.3412exbi 43441
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1888
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 43444
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 43445
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 43443
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1828
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 43446
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 43447
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1846
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 43448
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2340
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1861
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 43453
[WhiteheadRussell] p. 165Theorem *11.56aaanv 43449
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 43450
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 43451
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 43452
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 43457
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 43454
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 43455
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 43456
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 43458
[WhiteheadRussell] p. 175Definition *14.02df-eu 2561
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 43468  pm13.13b 43469
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 43470
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3020
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3021
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3655
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 43476
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 43477
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 43471
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 43615  pm13.193 43472
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 43473
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 43474
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 43475
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 43482
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 43481
[WhiteheadRussell] p. 184Definition *14.01iotasbc 43480
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3844
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 43483  pm14.122b 43484  pm14.122c 43485
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 43486  pm14.123b 43487  pm14.123c 43488
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 43490
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 43489
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 43491
[WhiteheadRussell] p. 190Theorem *14.22iota4 6523
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 43492
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6524
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 43493
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 43495
[WhiteheadRussell] p. 192Theorem *14.26eupick 2627  eupickbi 2630  sbaniota 43496
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 43494
[WhiteheadRussell] p. 192Theorem *14.271eubi 2576
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 43498
[WhiteheadRussell] p. 235Definition *30.01conventions 29920  df-fv 6550
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9998  pm54.43lem 9997
[Young] p. 141Definition of operator orderingleop2 31644
[Young] p. 142Example 12.2(i)0leop 31650  idleop 31651
[vandenDries] p. 42Lemma 61irrapx1 41868
[vandenDries] p. 43Theorem 62pellex 41875  pellexlem1 41869

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