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 17608
[Adamek] p. 21Condition 3.1(b)df-cat 17608
[Adamek] p. 22Example 3.3(1)df-setc 18022
[Adamek] p. 24Example 3.3(4.c)0cat 17629
[Adamek] p. 24Example 3.3(4.d)df-prstc 47585  prsthinc 47576
[Adamek] p. 24Example 3.3(4.e)df-mndtc 47606  df-mndtc 47606
[Adamek] p. 25Definition 3.5df-oppc 17652
[Adamek] p. 28Remark 3.9oppciso 17724
[Adamek] p. 28Remark 3.12invf1o 17712  invisoinvl 17733
[Adamek] p. 28Example 3.13idinv 17732  idiso 17731
[Adamek] p. 28Corollary 3.11inveq 17717
[Adamek] p. 28Definition 3.8df-inv 17691  df-iso 17692  dfiso2 17715
[Adamek] p. 28Proposition 3.10sectcan 17698
[Adamek] p. 29Remark 3.16cicer 17749
[Adamek] p. 29Definition 3.15cic 17742  df-cic 17739
[Adamek] p. 29Definition 3.17df-func 17804
[Adamek] p. 29Proposition 3.14(1)invinv 17713
[Adamek] p. 29Proposition 3.14(2)invco 17714  isoco 17720
[Adamek] p. 30Remark 3.19df-func 17804
[Adamek] p. 30Example 3.20(1)idfucl 17827
[Adamek] p. 32Proposition 3.21funciso 17820
[Adamek] p. 33Example 3.26(2)df-thinc 47542  prsthinc 47576  thincciso 47571
[Adamek] p. 33Example 3.26(3)df-mndtc 47606
[Adamek] p. 33Proposition 3.23cofucl 17834
[Adamek] p. 34Remark 3.28(2)catciso 18057
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18115
[Adamek] p. 34Definition 3.27(2)df-fth 17852
[Adamek] p. 34Definition 3.27(3)df-full 17851
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18115
[Adamek] p. 35Corollary 3.32ffthiso 17876
[Adamek] p. 35Proposition 3.30(c)cofth 17882
[Adamek] p. 35Proposition 3.30(d)cofull 17881
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18100
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18100
[Adamek] p. 39Definition 3.41funcoppc 17821
[Adamek] p. 39Definition 3.44.df-catc 18045
[Adamek] p. 39Proposition 3.43(c)fthoppc 17870
[Adamek] p. 39Proposition 3.43(d)fulloppc 17869
[Adamek] p. 40Remark 3.48catccat 18054
[Adamek] p. 40Definition 3.47df-catc 18045
[Adamek] p. 48Example 4.3(1.a)0subcat 17784
[Adamek] p. 48Example 4.3(1.b)catsubcat 17785
[Adamek] p. 48Definition 4.1(2)fullsubc 17796
[Adamek] p. 48Definition 4.1(a)df-subc 17755
[Adamek] p. 49Remark 4.4(2)ressffth 17885
[Adamek] p. 83Definition 6.1df-nat 17890
[Adamek] p. 87Remark 6.14(a)fuccocl 17913
[Adamek] p. 87Remark 6.14(b)fucass 17917
[Adamek] p. 87Definition 6.15df-fuc 17891
[Adamek] p. 88Remark 6.16fuccat 17919
[Adamek] p. 101Definition 7.1df-inito 17930
[Adamek] p. 101Example 7.2 (6)irinitoringc 46869
[Adamek] p. 102Definition 7.4df-termo 17931
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17958
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17962
[Adamek] p. 103Definition 7.7df-zeroo 17932
[Adamek] p. 103Example 7.9 (3)nzerooringczr 46872
[Adamek] p. 103Proposition 7.6termoeu1w 17965
[Adamek] p. 106Definition 7.19df-sect 17690
[Adamek] p. 185Section 10.67updjud 9925
[Adamek] p. 478Item Rngdf-ringc 46805
[AhoHopUll] p. 2Section 1.1df-bigo 47136
[AhoHopUll] p. 12Section 1.3df-blen 47158
[AhoHopUll] p. 318Section 9.1df-concat 14517  df-pfx 14617  df-substr 14587  df-word 14461  lencl 14479  wrd0 14485
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24207  df-nmoo 29976
[AkhiezerGlazman] p. 64Theoremhmopidmch 31384  hmopidmchi 31382
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 31432  pjcmul2i 31433
[AkhiezerGlazman] p. 72Theoremcnvunop 31149  unoplin 31151
[AkhiezerGlazman] p. 72Equation 2unopadj 31150  unopadj2 31169
[AkhiezerGlazman] p. 73Theoremelunop2 31244  lnopunii 31243
[AkhiezerGlazman] p. 80Proposition 1adjlnop 31317
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27394
[Alling] p. 184Axiom Bbdayfo 27160
[Alling] p. 184Axiom Osltso 27159
[Alling] p. 184Axiom SDnodense 27175
[Alling] p. 185Lemma 0nocvxmin 27260
[Alling] p. 185Theoremconway 27280
[Alling] p. 185Axiom FEnoeta 27226
[Alling] p. 186Theorem 4slerec 27300
[Alling], p. 2Definitionrp-brsslt 42107
[Alling], p. 3Notenla0001 42110  nla0002 42108  nla0003 42109
[Apostol] p. 18Theorem I.1addcan 11394  addcan2d 11414  addcan2i 11404  addcand 11413  addcani 11403
[Apostol] p. 18Theorem I.2negeu 11446
[Apostol] p. 18Theorem I.3negsub 11504  negsubd 11573  negsubi 11534
[Apostol] p. 18Theorem I.4negneg 11506  negnegd 11558  negnegi 11526
[Apostol] p. 18Theorem I.5subdi 11643  subdid 11666  subdii 11659  subdir 11644  subdird 11667  subdiri 11660
[Apostol] p. 18Theorem I.6mul01 11389  mul01d 11409  mul01i 11400  mul02 11388  mul02d 11408  mul02i 11399
[Apostol] p. 18Theorem I.7mulcan 11847  mulcan2d 11844  mulcand 11843  mulcani 11849
[Apostol] p. 18Theorem I.8receu 11855  xreceu 32066
[Apostol] p. 18Theorem I.9divrec 11884  divrecd 11989  divreci 11955  divreczi 11948
[Apostol] p. 18Theorem I.10recrec 11907  recreci 11942
[Apostol] p. 18Theorem I.11mul0or 11850  mul0ord 11860  mul0ori 11858
[Apostol] p. 18Theorem I.12mul2neg 11649  mul2negd 11665  mul2negi 11658  mulneg1 11646  mulneg1d 11663  mulneg1i 11656
[Apostol] p. 18Theorem I.13divadddiv 11925  divadddivd 12030  divadddivi 11972
[Apostol] p. 18Theorem I.14divmuldiv 11910  divmuldivd 12027  divmuldivi 11970  rdivmuldivd 20216
[Apostol] p. 18Theorem I.15divdivdiv 11911  divdivdivd 12033  divdivdivi 11973
[Apostol] p. 20Axiom 7rpaddcl 12992  rpaddcld 13027  rpmulcl 12993  rpmulcld 13028
[Apostol] p. 20Axiom 8rpneg 13002
[Apostol] p. 20Axiom 90nrp 13005
[Apostol] p. 20Theorem I.17lttri 11336
[Apostol] p. 20Theorem I.18ltadd1d 11803  ltadd1dd 11821  ltadd1i 11764
[Apostol] p. 20Theorem I.19ltmul1 12060  ltmul1a 12059  ltmul1i 12128  ltmul1ii 12138  ltmul2 12061  ltmul2d 13054  ltmul2dd 13068  ltmul2i 12131
[Apostol] p. 20Theorem I.20msqgt0 11730  msqgt0d 11777  msqgt0i 11747
[Apostol] p. 20Theorem I.210lt1 11732
[Apostol] p. 20Theorem I.23lt0neg1 11716  lt0neg1d 11779  ltneg 11710  ltnegd 11788  ltnegi 11754
[Apostol] p. 20Theorem I.25lt2add 11695  lt2addd 11833  lt2addi 11772
[Apostol] p. 20Definition of positive numbersdf-rp 12971
[Apostol] p. 21Exercise 4recgt0 12056  recgt0d 12144  recgt0i 12115  recgt0ii 12116
[Apostol] p. 22Definition of integersdf-z 12555
[Apostol] p. 22Definition of positive integersdfnn3 12222
[Apostol] p. 22Definition of rationalsdf-q 12929
[Apostol] p. 24Theorem I.26supeu 9445
[Apostol] p. 26Theorem I.28nnunb 12464
[Apostol] p. 26Theorem I.29arch 12465  archd 43789
[Apostol] p. 28Exercise 2btwnz 12661
[Apostol] p. 28Exercise 3nnrecl 12466
[Apostol] p. 28Exercise 4rebtwnz 12927
[Apostol] p. 28Exercise 5zbtwnre 12926
[Apostol] p. 28Exercise 6qbtwnre 13174
[Apostol] p. 28Exercise 10(a)zeneo 16278  zneo 12641  zneoALTV 46272
[Apostol] p. 29Theorem I.35cxpsqrtth 26219  msqsqrtd 15383  resqrtth 15198  sqrtth 15307  sqrtthi 15313  sqsqrtd 15382
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12211
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12893
[Apostol] p. 361Remarkcrreczi 14187
[Apostol] p. 363Remarkabsgt0i 15342
[Apostol] p. 363Exampleabssubd 15396  abssubi 15346
[ApostolNT] p. 7Remarkfmtno0 46143  fmtno1 46144  fmtno2 46153  fmtno3 46154  fmtno4 46155  fmtno5fac 46185  fmtnofz04prm 46180
[ApostolNT] p. 7Definitiondf-fmtno 46131
[ApostolNT] p. 8Definitiondf-ppi 26584
[ApostolNT] p. 14Definitiondf-dvds 16194
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16209
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16233
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16228
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16222
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16224
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16210
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16211
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16216
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16250
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16252
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16254
[ApostolNT] p. 15Definitiondf-gcd 16432  dfgcd2 16484
[ApostolNT] p. 16Definitionisprm2 16615
[ApostolNT] p. 16Theorem 1.5coprmdvds 16586
[ApostolNT] p. 16Theorem 1.7prminf 16844
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16450
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16485
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16487
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16465
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16457
[ApostolNT] p. 17Theorem 1.8coprm 16644
[ApostolNT] p. 17Theorem 1.9euclemma 16646
[ApostolNT] p. 17Theorem 1.101arith2 16857
[ApostolNT] p. 18Theorem 1.13prmrec 16851
[ApostolNT] p. 19Theorem 1.14divalg 16342
[ApostolNT] p. 20Theorem 1.15eucalg 16520
[ApostolNT] p. 24Definitiondf-mu 26585
[ApostolNT] p. 25Definitiondf-phi 16695
[ApostolNT] p. 25Theorem 2.1musum 26675
[ApostolNT] p. 26Theorem 2.2phisum 16719
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16705
[ApostolNT] p. 28Theorem 2.5(c)phimul 16709
[ApostolNT] p. 32Definitiondf-vma 26582
[ApostolNT] p. 32Theorem 2.9muinv 26677
[ApostolNT] p. 32Theorem 2.10vmasum 26699
[ApostolNT] p. 38Remarkdf-sgm 26586
[ApostolNT] p. 38Definitiondf-sgm 26586
[ApostolNT] p. 75Definitiondf-chp 26583  df-cht 26581
[ApostolNT] p. 104Definitioncongr 16597
[ApostolNT] p. 106Remarkdvdsval3 16197
[ApostolNT] p. 106Definitionmoddvds 16204
[ApostolNT] p. 107Example 2mod2eq0even 16285
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16286
[ApostolNT] p. 107Example 4zmod1congr 13849
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13886
[ApostolNT] p. 107Theorem 5.2(c)modexp 14197
[ApostolNT] p. 108Theorem 5.3modmulconst 16227
[ApostolNT] p. 109Theorem 5.4cncongr1 16600
[ApostolNT] p. 109Theorem 5.6gcdmodi 17003
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16602
[ApostolNT] p. 113Theorem 5.17eulerth 16712
[ApostolNT] p. 113Theorem 5.18vfermltl 16730
[ApostolNT] p. 114Theorem 5.19fermltl 16713
[ApostolNT] p. 116Theorem 5.24wilthimp 26556
[ApostolNT] p. 179Definitiondf-lgs 26778  lgsprme0 26822
[ApostolNT] p. 180Example 11lgs 26823
[ApostolNT] p. 180Theorem 9.2lgsvalmod 26799
[ApostolNT] p. 180Theorem 9.3lgsdirprm 26814
[ApostolNT] p. 181Theorem 9.4m1lgs 26871
[ApostolNT] p. 181Theorem 9.52lgs 26890  2lgsoddprm 26899
[ApostolNT] p. 182Theorem 9.6gausslemma2d 26857
[ApostolNT] p. 185Theorem 9.8lgsquad 26866
[ApostolNT] p. 188Definitiondf-lgs 26778  lgs1 26824
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 26815
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 26817
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 26825
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 26826
[Baer] p. 40Property (b)mapdord 40447
[Baer] p. 40Property (c)mapd11 40448
[Baer] p. 40Property (e)mapdin 40471  mapdlsm 40473
[Baer] p. 40Property (f)mapd0 40474
[Baer] p. 40Definition of projectivitydf-mapd 40434  mapd1o 40457
[Baer] p. 41Property (g)mapdat 40476
[Baer] p. 44Part (1)mapdpg 40515
[Baer] p. 45Part (2)hdmap1eq 40610  mapdheq 40537  mapdheq2 40538  mapdheq2biN 40539
[Baer] p. 45Part (3)baerlem3 40522
[Baer] p. 46Part (4)mapdheq4 40541  mapdheq4lem 40540
[Baer] p. 46Part (5)baerlem5a 40523  baerlem5abmN 40527  baerlem5amN 40525  baerlem5b 40524  baerlem5bmN 40526
[Baer] p. 47Part (6)hdmap1l6 40630  hdmap1l6a 40618  hdmap1l6e 40623  hdmap1l6f 40624  hdmap1l6g 40625  hdmap1l6lem1 40616  hdmap1l6lem2 40617  mapdh6N 40556  mapdh6aN 40544  mapdh6eN 40549  mapdh6fN 40550  mapdh6gN 40551  mapdh6lem1N 40542  mapdh6lem2N 40543
[Baer] p. 48Part 9hdmapval 40637
[Baer] p. 48Part 10hdmap10 40649
[Baer] p. 48Part 11hdmapadd 40652
[Baer] p. 48Part (6)hdmap1l6h 40626  mapdh6hN 40552
[Baer] p. 48Part (7)mapdh75cN 40562  mapdh75d 40563  mapdh75e 40561  mapdh75fN 40564  mapdh7cN 40558  mapdh7dN 40559  mapdh7eN 40557  mapdh7fN 40560
[Baer] p. 48Part (8)mapdh8 40597  mapdh8a 40584  mapdh8aa 40585  mapdh8ab 40586  mapdh8ac 40587  mapdh8ad 40588  mapdh8b 40589  mapdh8c 40590  mapdh8d 40592  mapdh8d0N 40591  mapdh8e 40593  mapdh8g 40594  mapdh8i 40595  mapdh8j 40596
[Baer] p. 48Part (9)mapdh9a 40598
[Baer] p. 48Equation 10mapdhvmap 40578
[Baer] p. 49Part 12hdmap11 40657  hdmapeq0 40653  hdmapf1oN 40674  hdmapneg 40655  hdmaprnN 40673  hdmaprnlem1N 40658  hdmaprnlem3N 40659  hdmaprnlem3uN 40660  hdmaprnlem4N 40662  hdmaprnlem6N 40663  hdmaprnlem7N 40664  hdmaprnlem8N 40665  hdmaprnlem9N 40666  hdmapsub 40656
[Baer] p. 49Part 14hdmap14lem1 40677  hdmap14lem10 40686  hdmap14lem1a 40675  hdmap14lem2N 40678  hdmap14lem2a 40676  hdmap14lem3 40679  hdmap14lem8 40684  hdmap14lem9 40685
[Baer] p. 50Part 14hdmap14lem11 40687  hdmap14lem12 40688  hdmap14lem13 40689  hdmap14lem14 40690  hdmap14lem15 40691  hgmapval 40696
[Baer] p. 50Part 15hgmapadd 40703  hgmapmul 40704  hgmaprnlem2N 40706  hgmapvs 40700
[Baer] p. 50Part 16hgmaprnN 40710
[Baer] p. 110Lemma 1hdmapip0com 40726
[Baer] p. 110Line 27hdmapinvlem1 40727
[Baer] p. 110Line 28hdmapinvlem2 40728
[Baer] p. 110Line 30hdmapinvlem3 40729
[Baer] p. 110Part 1.2hdmapglem5 40731  hgmapvv 40735
[Baer] p. 110Proposition 1hdmapinvlem4 40730
[Baer] p. 111Line 10hgmapvvlem1 40732
[Baer] p. 111Line 15hdmapg 40739  hdmapglem7 40738
[Bauer], p. 483Theorem 1.22irrexpq 26220  2irrexpqALT 26285
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2564
[BellMachover] p. 460Notationdf-mo 2535
[BellMachover] p. 460Definitionmo3 2559
[BellMachover] p. 461Axiom Extax-ext 2704
[BellMachover] p. 462Theorem 1.1axextmo 2708
[BellMachover] p. 463Axiom Repaxrep5 5290
[BellMachover] p. 463Scheme Sepax-sep 5298
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 35883  bm1.3ii 5301
[BellMachover] p. 466Problemaxpow2 5364
[BellMachover] p. 466Axiom Powaxpow3 5365
[BellMachover] p. 466Axiom Unionaxun2 7722
[BellMachover] p. 468Definitiondf-ord 6364
[BellMachover] p. 469Theorem 2.2(i)ordirr 6379
[BellMachover] p. 469Theorem 2.2(iii)onelon 6386
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6381
[BellMachover] p. 471Definition of Ndf-om 7851
[BellMachover] p. 471Problem 2.5(ii)uniordint 7784
[BellMachover] p. 471Definition of Limdf-lim 6366
[BellMachover] p. 472Axiom Infzfinf2 9633
[BellMachover] p. 473Theorem 2.8limom 7866
[BellMachover] p. 477Equation 3.1df-r1 9755
[BellMachover] p. 478Definitionrankval2 9809
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9773  r1ord3g 9770
[BellMachover] p. 480Axiom Regzfreg 9586
[BellMachover] p. 488Axiom ACac5 10468  dfac4 10113
[BellMachover] p. 490Definition of alephalephval3 10101
[BeltramettiCassinelli] p. 98Remarkatlatmstc 38127
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 31584
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 31626  chirredi 31625
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 31614
[Beran] p. 3Definition of joinsshjval3 30585
[Beran] p. 39Theorem 2.3(i)cmcm2 30847  cmcm2i 30824  cmcm2ii 30829  cmt2N 38058
[Beran] p. 40Theorem 2.3(iii)lecm 30848  lecmi 30833  lecmii 30834
[Beran] p. 45Theorem 3.4cmcmlem 30822
[Beran] p. 49Theorem 4.2cm2j 30851  cm2ji 30856  cm2mi 30857
[Beran] p. 95Definitiondf-sh 30438  issh2 30440
[Beran] p. 95Lemma 3.1(S5)his5 30317
[Beran] p. 95Lemma 3.1(S6)his6 30330
[Beran] p. 95Lemma 3.1(S7)his7 30321
[Beran] p. 95Lemma 3.2(S8)ho01i 31059
[Beran] p. 95Lemma 3.2(S9)hoeq1 31061
[Beran] p. 95Lemma 3.2(S10)ho02i 31060
[Beran] p. 95Lemma 3.2(S11)hoeq2 31062
[Beran] p. 95Postulate (S1)ax-his1 30313  his1i 30331
[Beran] p. 95Postulate (S2)ax-his2 30314
[Beran] p. 95Postulate (S3)ax-his3 30315
[Beran] p. 95Postulate (S4)ax-his4 30316
[Beran] p. 96Definition of normdf-hnorm 30199  dfhnorm2 30353  normval 30355
[Beran] p. 96Definition for Cauchy sequencehcau 30415
[Beran] p. 96Definition of Cauchy sequencedf-hcau 30204
[Beran] p. 96Definition of complete subspaceisch3 30472
[Beran] p. 96Definition of convergedf-hlim 30203  hlimi 30419
[Beran] p. 97Theorem 3.3(i)norm-i-i 30364  norm-i 30360
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 30368  norm-ii 30369  normlem0 30340  normlem1 30341  normlem2 30342  normlem3 30343  normlem4 30344  normlem5 30345  normlem6 30346  normlem7 30347  normlem7tALT 30350
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 30370  norm-iii 30371
[Beran] p. 98Remark 3.4bcs 30412  bcsiALT 30410  bcsiHIL 30411
[Beran] p. 98Remark 3.4(B)normlem9at 30352  normpar 30386  normpari 30385
[Beran] p. 98Remark 3.4(C)normpyc 30377  normpyth 30376  normpythi 30373
[Beran] p. 99Remarklnfn0 31278  lnfn0i 31273  lnop0 31197  lnop0i 31201
[Beran] p. 99Theorem 3.5(i)nmcexi 31257  nmcfnex 31284  nmcfnexi 31282  nmcopex 31260  nmcopexi 31258
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 31285  nmcfnlbi 31283  nmcoplb 31261  nmcoplbi 31259
[Beran] p. 99Theorem 3.5(iii)lnfncon 31287  lnfnconi 31286  lnopcon 31266  lnopconi 31265
[Beran] p. 100Lemma 3.6normpar2i 30387
[Beran] p. 101Lemma 3.6norm3adifi 30384  norm3adifii 30379  norm3dif 30381  norm3difi 30378
[Beran] p. 102Theorem 3.7(i)chocunii 30532  pjhth 30624  pjhtheu 30625  pjpjhth 30656  pjpjhthi 30657  pjth 24938
[Beran] p. 102Theorem 3.7(ii)ococ 30637  ococi 30636
[Beran] p. 103Remark 3.8nlelchi 31292
[Beran] p. 104Theorem 3.9riesz3i 31293  riesz4 31295  riesz4i 31294
[Beran] p. 104Theorem 3.10cnlnadj 31310  cnlnadjeu 31309  cnlnadjeui 31308  cnlnadji 31307  cnlnadjlem1 31298  nmopadjlei 31319
[Beran] p. 106Theorem 3.11(i)adjeq0 31322
[Beran] p. 106Theorem 3.11(v)nmopadji 31321
[Beran] p. 106Theorem 3.11(ii)adjmul 31323
[Beran] p. 106Theorem 3.11(iv)adjadj 31167
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 31333  nmopcoadji 31332
[Beran] p. 106Theorem 3.11(iii)adjadd 31324
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 31334
[Beran] p. 106Theorem 3.11(viii)adjcoi 31331  pjadj2coi 31435  pjadjcoi 31392
[Beran] p. 107Definitiondf-ch 30452  isch2 30454
[Beran] p. 107Remark 3.12choccl 30537  isch3 30472  occl 30535  ocsh 30514  shoccl 30536  shocsh 30515
[Beran] p. 107Remark 3.12(B)ococin 30639
[Beran] p. 108Theorem 3.13chintcl 30563
[Beran] p. 109Property (i)pjadj2 31418  pjadj3 31419  pjadji 30916  pjadjii 30905
[Beran] p. 109Property (ii)pjidmco 31412  pjidmcoi 31408  pjidmi 30904
[Beran] p. 110Definition of projector orderingpjordi 31404
[Beran] p. 111Remarkho0val 30981  pjch1 30901
[Beran] p. 111Definitiondf-hfmul 30965  df-hfsum 30964  df-hodif 30963  df-homul 30962  df-hosum 30961
[Beran] p. 111Lemma 4.4(i)pjo 30902
[Beran] p. 111Lemma 4.4(ii)pjch 30925  pjchi 30663
[Beran] p. 111Lemma 4.4(iii)pjoc2 30670  pjoc2i 30669
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 30911
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 31396  pjssmii 30912
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 31395
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 31394
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 31399
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 31397  pjssge0ii 30913
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 31398  pjdifnormii 30914
[Bobzien] p. 116Statement T3stoic3 1779
[Bobzien] p. 117Statement T2stoic2a 1777
[Bobzien] p. 117Statement T4stoic4a 1780
[Bobzien] p. 117Conclusion the contradictorystoic1a 1775
[Bogachev] p. 16Definition 1.5df-oms 33229
[Bogachev] p. 17Lemma 1.5.4omssubadd 33237
[Bogachev] p. 17Example 1.5.2omsmon 33235
[Bogachev] p. 41Definition 1.11.2df-carsg 33239
[Bogachev] p. 42Theorem 1.11.4carsgsiga 33259
[Bogachev] p. 116Definition 2.3.1df-itgm 33290  df-sitm 33268
[Bogachev] p. 118Chapter 2.4.4df-itgm 33290
[Bogachev] p. 118Definition 2.4.1df-sitg 33267
[Bollobas] p. 1Section I.1df-edg 28288  isuhgrop 28310  isusgrop 28402  isuspgrop 28401
[Bollobas] p. 2Section I.1df-subgr 28505  uhgrspan1 28540  uhgrspansubgr 28528
[Bollobas] p. 3Definitionisomuspgr 46437
[Bollobas] p. 3Section I.1cusgrsize 28691  df-cusgr 28649  df-nbgr 28570  fusgrmaxsize 28701
[Bollobas] p. 4Definitiondf-upwlks 46447  df-wlks 28836
[Bollobas] p. 4Section I.1finsumvtxdg2size 28787  finsumvtxdgeven 28789  fusgr1th 28788  fusgrvtxdgonume 28791  vtxdgoddnumeven 28790
[Bollobas] p. 5Notationdf-pths 28953
[Bollobas] p. 5Definitiondf-crcts 29023  df-cycls 29024  df-trls 28929  df-wlkson 28837
[Bollobas] p. 7Section I.1df-ushgr 28299
[BourbakiAlg1] p. 1Definition 1df-clintop 46545  df-cllaw 46531  df-mgm 18557  df-mgm2 46564
[BourbakiAlg1] p. 4Definition 5df-assintop 46546  df-asslaw 46533  df-sgrp 18606  df-sgrp2 46566
[BourbakiAlg1] p. 7Definition 8df-cmgm2 46565  df-comlaw 46532
[BourbakiAlg1] p. 12Definition 2df-mnd 18622
[BourbakiAlg1] p. 92Definition 1df-ring 20049
[BourbakiAlg1] p. 93Section I.8.1df-rng 46584
[BourbakiEns] p. Proposition 8fcof1 7280  fcofo 7281
[BourbakiTop1] p. Remarkxnegmnf 13185  xnegpnf 13184
[BourbakiTop1] p. Remark rexneg 13186
[BourbakiTop1] p. Remark 3ust0 23706  ustfilxp 23699
[BourbakiTop1] p. Axiom GT'tgpsubcn 23576
[BourbakiTop1] p. Criterionishmeo 23245
[BourbakiTop1] p. Example 1cstucnd 23771  iducn 23770  snfil 23350
[BourbakiTop1] p. Example 2neifil 23366
[BourbakiTop1] p. Theorem 1cnextcn 23553
[BourbakiTop1] p. Theorem 2ucnextcn 23791
[BourbakiTop1] p. Theorem 3df-hcmp 32875
[BourbakiTop1] p. Paragraph 3infil 23349
[BourbakiTop1] p. Definition 1df-ucn 23763  df-ust 23687  filintn0 23347  filn0 23348  istgp 23563  ucnprima 23769
[BourbakiTop1] p. Definition 2df-cfilu 23774
[BourbakiTop1] p. Definition 3df-cusp 23785  df-usp 23744  df-utop 23718  trust 23716
[BourbakiTop1] p. Definition 6df-pcmp 32774
[BourbakiTop1] p. Property V_issnei2 22602
[BourbakiTop1] p. Theorem 1(d)iscncl 22755
[BourbakiTop1] p. Condition F_Iustssel 23692
[BourbakiTop1] p. Condition U_Iustdiag 23695
[BourbakiTop1] p. Property V_iiinnei 22611
[BourbakiTop1] p. Property V_ivneiptopreu 22619  neissex 22613
[BourbakiTop1] p. Proposition 1neips 22599  neiss 22595  ucncn 23772  ustund 23708  ustuqtop 23733
[BourbakiTop1] p. Proposition 2cnpco 22753  neiptopreu 22619  utop2nei 23737  utop3cls 23738
[BourbakiTop1] p. Proposition 3fmucnd 23779  uspreg 23761  utopreg 23739
[BourbakiTop1] p. Proposition 4imasncld 23177  imasncls 23178  imasnopn 23176
[BourbakiTop1] p. Proposition 9cnpflf2 23486
[BourbakiTop1] p. Condition F_IIustincl 23694
[BourbakiTop1] p. Condition U_IIustinvel 23696
[BourbakiTop1] p. Property V_iiielnei 22597
[BourbakiTop1] p. Proposition 11cnextucn 23790
[BourbakiTop1] p. Condition F_IIbustbasel 23693
[BourbakiTop1] p. Condition U_IIIustexhalf 23697
[BourbakiTop1] p. Definition C'''df-cmp 22873
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23332
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22378
[BourbakiTop2] p. 195Definition 1df-ldlf 32771
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 44713
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 44715  stoweid 44714
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 44652  stoweidlem10 44661  stoweidlem14 44665  stoweidlem15 44666  stoweidlem35 44686  stoweidlem36 44687  stoweidlem37 44688  stoweidlem38 44689  stoweidlem40 44691  stoweidlem41 44692  stoweidlem43 44694  stoweidlem44 44695  stoweidlem46 44697  stoweidlem5 44656  stoweidlem50 44701  stoweidlem52 44703  stoweidlem53 44704  stoweidlem55 44706  stoweidlem56 44707
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 44674  stoweidlem24 44675  stoweidlem27 44678  stoweidlem28 44679  stoweidlem30 44681
[BrosowskiDeutsh] p. 91Proofstoweidlem34 44685  stoweidlem59 44710  stoweidlem60 44711
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 44696  stoweidlem49 44700  stoweidlem7 44658
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 44682  stoweidlem39 44690  stoweidlem42 44693  stoweidlem48 44699  stoweidlem51 44702  stoweidlem54 44705  stoweidlem57 44708  stoweidlem58 44709
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 44676
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 44668
[BrosowskiDeutsh] p. 92Proofstoweidlem11 44662  stoweidlem13 44664  stoweidlem26 44677  stoweidlem61 44712
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 44669
[Bruck] p. 1Section I.1df-clintop 46545  df-mgm 18557  df-mgm2 46564
[Bruck] p. 23Section II.1df-sgrp 18606  df-sgrp2 46566
[Bruck] p. 28Theorem 3.2dfgrp3 18918
[ChoquetDD] p. 2Definition of mappingdf-mpt 5231
[Church] p. 129Section II.24df-ifp 1063  dfifp2 1064
[Clemente] p. 10Definition ITnatded 29636
[Clemente] p. 10Definition I` `m,nnatded 29636
[Clemente] p. 11Definition E=>m,nnatded 29636
[Clemente] p. 11Definition I=>m,nnatded 29636
[Clemente] p. 11Definition E` `(1)natded 29636
[Clemente] p. 11Definition E` `(2)natded 29636
[Clemente] p. 12Definition E` `m,n,pnatded 29636
[Clemente] p. 12Definition I` `n(1)natded 29636
[Clemente] p. 12Definition I` `n(2)natded 29636
[Clemente] p. 13Definition I` `m,n,pnatded 29636
[Clemente] p. 14Proof 5.11natded 29636
[Clemente] p. 14Definition E` `nnatded 29636
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 29638  ex-natded5.2 29637
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 29641  ex-natded5.3 29640
[Clemente] p. 18Theorem 5.5ex-natded5.5 29643
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 29645  ex-natded5.7 29644
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 29647  ex-natded5.8 29646
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 29649  ex-natded5.13 29648
[Clemente] p. 32Definition I` `nnatded 29636
[Clemente] p. 32Definition E` `m,n,p,anatded 29636
[Clemente] p. 32Definition E` `n,tnatded 29636
[Clemente] p. 32Definition I` `n,tnatded 29636
[Clemente] p. 43Theorem 9.20ex-natded9.20 29650
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 29651
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 29653  ex-natded9.26 29652
[Cohen] p. 301Remarkrelogoprlem 26081
[Cohen] p. 301Property 2relogmul 26082  relogmuld 26115
[Cohen] p. 301Property 3relogdiv 26083  relogdivd 26116
[Cohen] p. 301Property 4relogexp 26086
[Cohen] p. 301Property 1alog1 26076
[Cohen] p. 301Property 1bloge 26077
[Cohen4] p. 348Observationrelogbcxpb 26272
[Cohen4] p. 349Propertyrelogbf 26276
[Cohen4] p. 352Definitionelogb 26255
[Cohen4] p. 361Property 2relogbmul 26262
[Cohen4] p. 361Property 3logbrec 26267  relogbdiv 26264
[Cohen4] p. 361Property 4relogbreexp 26260
[Cohen4] p. 361Property 6relogbexp 26265
[Cohen4] p. 361Property 1(a)logbid1 26253
[Cohen4] p. 361Property 1(b)logb1 26254
[Cohen4] p. 367Propertylogbchbase 26256
[Cohen4] p. 377Property 2logblt 26269
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 33222  sxbrsigalem4 33224
[Cohn] p. 81Section II.5acsdomd 18506  acsinfd 18505  acsinfdimd 18507  acsmap2d 18504  acsmapd 18503
[Cohn] p. 143Example 5.1.1sxbrsiga 33227
[Connell] p. 57Definitiondf-scmat 21975  df-scmatalt 46982
[Conway] p. 4Definitionslerec 27300
[Conway] p. 5Definitionaddsval 27426  addsval2 27427  df-adds 27424  df-muls 27543  df-negs 27476
[Conway] p. 7Theorem0slt1s 27310
[Conway] p. 16Theorem 0(i)ssltright 27346
[Conway] p. 16Theorem 0(ii)ssltleft 27345
[Conway] p. 16Theorem 0(iii)slerflex 27246
[Conway] p. 17Theorem 3addsass 27468  addsassd 27469  addscom 27430  addscomd 27431  addsrid 27428  addsridd 27429
[Conway] p. 17Definitiondf-0s 27305
[Conway] p. 17Theorem 4(ii)negnegs 27498
[Conway] p. 17Theorem 4(iii)negsid 27495  negsidd 27496
[Conway] p. 18Theorem 5sleadd1 27452  sleadd1d 27458
[Conway] p. 18Definitiondf-1s 27306
[Conway] p. 18Theorem 6(ii)negscl 27490  negscld 27491
[Conway] p. 18Theorem 6(iii)addscld 27444
[Conway] p. 19Theorem 7addsdi 27590  addsdid 27591  addsdird 27592  mulnegs1d 27595  mulnegs2d 27596  mulsass 27601  mulsassd 27602  mulscom 27575  mulscomd 27576
[Conway] p. 19Theorem 8(i)mulscl 27570  mulscld 27571
[Conway] p. 19Theorem 8(iii)slemuld 27574  sltmul 27572  sltmuld 27573
[Conway] p. 20Theorem 9mulsgt0 27580  mulsgt0d 27581
[Conway] p. 21Theorem 10(iv)precsex 27644
[Conway] p. 29Remarkmadebday 27374  newbday 27376  oldbday 27375
[Conway] p. 29Definitiondf-made 27322  df-new 27324  df-old 27323
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13822
[Crawley] p. 1Definition of posetdf-poset 18262
[Crawley] p. 107Theorem 13.2hlsupr 38195
[Crawley] p. 110Theorem 13.3arglem1N 38999  dalaw 38695
[Crawley] p. 111Theorem 13.4hlathil 40774
[Crawley] p. 111Definition of set Wdf-watsN 38799
[Crawley] p. 111Definition of dilationdf-dilN 38915  df-ldil 38913  isldil 38919
[Crawley] p. 111Definition of translationdf-ltrn 38914  df-trnN 38916  isltrn 38928  ltrnu 38930
[Crawley] p. 112Lemma Acdlema1N 38600  cdlema2N 38601  exatleN 38213
[Crawley] p. 112Lemma B1cvrat 38285  cdlemb 38603  cdlemb2 38850  cdlemb3 39415  idltrn 38959  l1cvat 37863  lhpat 38852  lhpat2 38854  lshpat 37864  ltrnel 38948  ltrnmw 38960
[Crawley] p. 112Lemma Ccdlemc1 39000  cdlemc2 39001  ltrnnidn 38983  trlat 38978  trljat1 38975  trljat2 38976  trljat3 38977  trlne 38994  trlnidat 38982  trlnle 38995
[Crawley] p. 112Definition of automorphismdf-pautN 38800
[Crawley] p. 113Lemma Ccdlemc 39006  cdlemc3 39002  cdlemc4 39003
[Crawley] p. 113Lemma Dcdlemd 39016  cdlemd1 39007  cdlemd2 39008  cdlemd3 39009  cdlemd4 39010  cdlemd5 39011  cdlemd6 39012  cdlemd7 39013  cdlemd8 39014  cdlemd9 39015  cdleme31sde 39194  cdleme31se 39191  cdleme31se2 39192  cdleme31snd 39195  cdleme32a 39250  cdleme32b 39251  cdleme32c 39252  cdleme32d 39253  cdleme32e 39254  cdleme32f 39255  cdleme32fva 39246  cdleme32fva1 39247  cdleme32fvcl 39249  cdleme32le 39256  cdleme48fv 39308  cdleme4gfv 39316  cdleme50eq 39350  cdleme50f 39351  cdleme50f1 39352  cdleme50f1o 39355  cdleme50laut 39356  cdleme50ldil 39357  cdleme50lebi 39349  cdleme50rn 39354  cdleme50rnlem 39353  cdlemeg49le 39320  cdlemeg49lebilem 39348
[Crawley] p. 113Lemma Ecdleme 39369  cdleme00a 39018  cdleme01N 39030  cdleme02N 39031  cdleme0a 39020  cdleme0aa 39019  cdleme0b 39021  cdleme0c 39022  cdleme0cp 39023  cdleme0cq 39024  cdleme0dN 39025  cdleme0e 39026  cdleme0ex1N 39032  cdleme0ex2N 39033  cdleme0fN 39027  cdleme0gN 39028  cdleme0moN 39034  cdleme1 39036  cdleme10 39063  cdleme10tN 39067  cdleme11 39079  cdleme11a 39069  cdleme11c 39070  cdleme11dN 39071  cdleme11e 39072  cdleme11fN 39073  cdleme11g 39074  cdleme11h 39075  cdleme11j 39076  cdleme11k 39077  cdleme11l 39078  cdleme12 39080  cdleme13 39081  cdleme14 39082  cdleme15 39087  cdleme15a 39083  cdleme15b 39084  cdleme15c 39085  cdleme15d 39086  cdleme16 39094  cdleme16aN 39068  cdleme16b 39088  cdleme16c 39089  cdleme16d 39090  cdleme16e 39091  cdleme16f 39092  cdleme16g 39093  cdleme19a 39112  cdleme19b 39113  cdleme19c 39114  cdleme19d 39115  cdleme19e 39116  cdleme19f 39117  cdleme1b 39035  cdleme2 39037  cdleme20aN 39118  cdleme20bN 39119  cdleme20c 39120  cdleme20d 39121  cdleme20e 39122  cdleme20f 39123  cdleme20g 39124  cdleme20h 39125  cdleme20i 39126  cdleme20j 39127  cdleme20k 39128  cdleme20l 39131  cdleme20l1 39129  cdleme20l2 39130  cdleme20m 39132  cdleme20y 39111  cdleme20zN 39110  cdleme21 39146  cdleme21d 39139  cdleme21e 39140  cdleme22a 39149  cdleme22aa 39148  cdleme22b 39150  cdleme22cN 39151  cdleme22d 39152  cdleme22e 39153  cdleme22eALTN 39154  cdleme22f 39155  cdleme22f2 39156  cdleme22g 39157  cdleme23a 39158  cdleme23b 39159  cdleme23c 39160  cdleme26e 39168  cdleme26eALTN 39170  cdleme26ee 39169  cdleme26f 39172  cdleme26f2 39174  cdleme26f2ALTN 39173  cdleme26fALTN 39171  cdleme27N 39178  cdleme27a 39176  cdleme27cl 39175  cdleme28c 39181  cdleme3 39046  cdleme30a 39187  cdleme31fv 39199  cdleme31fv1 39200  cdleme31fv1s 39201  cdleme31fv2 39202  cdleme31id 39203  cdleme31sc 39193  cdleme31sdnN 39196  cdleme31sn 39189  cdleme31sn1 39190  cdleme31sn1c 39197  cdleme31sn2 39198  cdleme31so 39188  cdleme35a 39257  cdleme35b 39259  cdleme35c 39260  cdleme35d 39261  cdleme35e 39262  cdleme35f 39263  cdleme35fnpq 39258  cdleme35g 39264  cdleme35h 39265  cdleme35h2 39266  cdleme35sn2aw 39267  cdleme35sn3a 39268  cdleme36a 39269  cdleme36m 39270  cdleme37m 39271  cdleme38m 39272  cdleme38n 39273  cdleme39a 39274  cdleme39n 39275  cdleme3b 39038  cdleme3c 39039  cdleme3d 39040  cdleme3e 39041  cdleme3fN 39042  cdleme3fa 39045  cdleme3g 39043  cdleme3h 39044  cdleme4 39047  cdleme40m 39276  cdleme40n 39277  cdleme40v 39278  cdleme40w 39279  cdleme41fva11 39286  cdleme41sn3aw 39283  cdleme41sn4aw 39284  cdleme41snaw 39285  cdleme42a 39280  cdleme42b 39287  cdleme42c 39281  cdleme42d 39282  cdleme42e 39288  cdleme42f 39289  cdleme42g 39290  cdleme42h 39291  cdleme42i 39292  cdleme42k 39293  cdleme42ke 39294  cdleme42keg 39295  cdleme42mN 39296  cdleme42mgN 39297  cdleme43aN 39298  cdleme43bN 39299  cdleme43cN 39300  cdleme43dN 39301  cdleme5 39049  cdleme50ex 39368  cdleme50ltrn 39366  cdleme51finvN 39365  cdleme51finvfvN 39364  cdleme51finvtrN 39367  cdleme6 39050  cdleme7 39058  cdleme7a 39052  cdleme7aa 39051  cdleme7b 39053  cdleme7c 39054  cdleme7d 39055  cdleme7e 39056  cdleme7ga 39057  cdleme8 39059  cdleme8tN 39064  cdleme9 39062  cdleme9a 39060  cdleme9b 39061  cdleme9tN 39066  cdleme9taN 39065  cdlemeda 39107  cdlemedb 39106  cdlemednpq 39108  cdlemednuN 39109  cdlemefr27cl 39212  cdlemefr32fva1 39219  cdlemefr32fvaN 39218  cdlemefrs32fva 39209  cdlemefrs32fva1 39210  cdlemefs27cl 39222  cdlemefs32fva1 39232  cdlemefs32fvaN 39231  cdlemesner 39105  cdlemeulpq 39029
[Crawley] p. 114Lemma E4atex 38885  4atexlem7 38884  cdleme0nex 39099  cdleme17a 39095  cdleme17c 39097  cdleme17d 39307  cdleme17d1 39098  cdleme17d2 39304  cdleme18a 39100  cdleme18b 39101  cdleme18c 39102  cdleme18d 39104  cdleme4a 39048
[Crawley] p. 115Lemma Ecdleme21a 39134  cdleme21at 39137  cdleme21b 39135  cdleme21c 39136  cdleme21ct 39138  cdleme21f 39141  cdleme21g 39142  cdleme21h 39143  cdleme21i 39144  cdleme22gb 39103
[Crawley] p. 116Lemma Fcdlemf 39372  cdlemf1 39370  cdlemf2 39371
[Crawley] p. 116Lemma Gcdlemftr1 39376  cdlemg16 39466  cdlemg28 39513  cdlemg28a 39502  cdlemg28b 39512  cdlemg3a 39406  cdlemg42 39538  cdlemg43 39539  cdlemg44 39542  cdlemg44a 39540  cdlemg46 39544  cdlemg47 39545  cdlemg9 39443  ltrnco 39528  ltrncom 39547  tgrpabl 39560  trlco 39536
[Crawley] p. 116Definition of Gdf-tgrp 39552
[Crawley] p. 117Lemma Gcdlemg17 39486  cdlemg17b 39471
[Crawley] p. 117Definition of Edf-edring-rN 39565  df-edring 39566
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 39569
[Crawley] p. 118Remarktendopltp 39589
[Crawley] p. 118Lemma Hcdlemh 39626  cdlemh1 39624  cdlemh2 39625
[Crawley] p. 118Lemma Icdlemi 39629  cdlemi1 39627  cdlemi2 39628
[Crawley] p. 118Lemma Jcdlemj1 39630  cdlemj2 39631  cdlemj3 39632  tendocan 39633
[Crawley] p. 118Lemma Kcdlemk 39783  cdlemk1 39640  cdlemk10 39652  cdlemk11 39658  cdlemk11t 39755  cdlemk11ta 39738  cdlemk11tb 39740  cdlemk11tc 39754  cdlemk11u-2N 39698  cdlemk11u 39680  cdlemk12 39659  cdlemk12u-2N 39699  cdlemk12u 39681  cdlemk13-2N 39685  cdlemk13 39661  cdlemk14-2N 39687  cdlemk14 39663  cdlemk15-2N 39688  cdlemk15 39664  cdlemk16-2N 39689  cdlemk16 39666  cdlemk16a 39665  cdlemk17-2N 39690  cdlemk17 39667  cdlemk18-2N 39695  cdlemk18-3N 39709  cdlemk18 39677  cdlemk19-2N 39696  cdlemk19 39678  cdlemk19u 39779  cdlemk1u 39668  cdlemk2 39641  cdlemk20-2N 39701  cdlemk20 39683  cdlemk21-2N 39700  cdlemk21N 39682  cdlemk22-3 39710  cdlemk22 39702  cdlemk23-3 39711  cdlemk24-3 39712  cdlemk25-3 39713  cdlemk26-3 39715  cdlemk26b-3 39714  cdlemk27-3 39716  cdlemk28-3 39717  cdlemk29-3 39720  cdlemk3 39642  cdlemk30 39703  cdlemk31 39705  cdlemk32 39706  cdlemk33N 39718  cdlemk34 39719  cdlemk35 39721  cdlemk36 39722  cdlemk37 39723  cdlemk38 39724  cdlemk39 39725  cdlemk39u 39777  cdlemk4 39643  cdlemk41 39729  cdlemk42 39750  cdlemk42yN 39753  cdlemk43N 39772  cdlemk45 39756  cdlemk46 39757  cdlemk47 39758  cdlemk48 39759  cdlemk49 39760  cdlemk5 39645  cdlemk50 39761  cdlemk51 39762  cdlemk52 39763  cdlemk53 39766  cdlemk54 39767  cdlemk55 39770  cdlemk55u 39775  cdlemk56 39780  cdlemk5a 39644  cdlemk5auN 39669  cdlemk5u 39670  cdlemk6 39646  cdlemk6u 39671  cdlemk7 39657  cdlemk7u-2N 39697  cdlemk7u 39679  cdlemk8 39647  cdlemk9 39648  cdlemk9bN 39649  cdlemki 39650  cdlemkid 39745  cdlemkj-2N 39691  cdlemkj 39672  cdlemksat 39655  cdlemksel 39654  cdlemksv 39653  cdlemksv2 39656  cdlemkuat 39675  cdlemkuel-2N 39693  cdlemkuel-3 39707  cdlemkuel 39674  cdlemkuv-2N 39692  cdlemkuv2-2 39694  cdlemkuv2-3N 39708  cdlemkuv2 39676  cdlemkuvN 39673  cdlemkvcl 39651  cdlemky 39735  cdlemkyyN 39771  tendoex 39784
[Crawley] p. 120Remarkdva1dim 39794
[Crawley] p. 120Lemma Lcdleml1N 39785  cdleml2N 39786  cdleml3N 39787  cdleml4N 39788  cdleml5N 39789  cdleml6 39790  cdleml7 39791  cdleml8 39792  cdleml9 39793  dia1dim 39870
[Crawley] p. 120Lemma Mdia11N 39857  diaf11N 39858  dialss 39855  diaord 39856  dibf11N 39970  djajN 39946
[Crawley] p. 120Definition of isomorphism mapdiaval 39841
[Crawley] p. 121Lemma Mcdlemm10N 39927  dia2dimlem1 39873  dia2dimlem2 39874  dia2dimlem3 39875  dia2dimlem4 39876  dia2dimlem5 39877  diaf1oN 39939  diarnN 39938  dvheveccl 39921  dvhopN 39925
[Crawley] p. 121Lemma Ncdlemn 40021  cdlemn10 40015  cdlemn11 40020  cdlemn11a 40016  cdlemn11b 40017  cdlemn11c 40018  cdlemn11pre 40019  cdlemn2 40004  cdlemn2a 40005  cdlemn3 40006  cdlemn4 40007  cdlemn4a 40008  cdlemn5 40010  cdlemn5pre 40009  cdlemn6 40011  cdlemn7 40012  cdlemn8 40013  cdlemn9 40014  diclspsn 40003
[Crawley] p. 121Definition of phi(q)df-dic 39982
[Crawley] p. 122Lemma Ndih11 40074  dihf11 40076  dihjust 40026  dihjustlem 40025  dihord 40073  dihord1 40027  dihord10 40032  dihord11b 40031  dihord11c 40033  dihord2 40036  dihord2a 40028  dihord2b 40029  dihord2cN 40030  dihord2pre 40034  dihord2pre2 40035  dihordlem6 40022  dihordlem7 40023  dihordlem7b 40024
[Crawley] p. 122Definition of isomorphism mapdihffval 40039  dihfval 40040  dihval 40041
[Diestel] p. 3Section 1.1df-cusgr 28649  df-nbgr 28570
[Diestel] p. 4Section 1.1df-subgr 28505  uhgrspan1 28540  uhgrspansubgr 28528
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 28791  vtxdgoddnumeven 28790
[Diestel] p. 27Section 1.10df-ushgr 28299
[EGA] p. 80Notation 1.1.1rspecval 32782
[EGA] p. 80Proposition 1.1.2zartop 32794
[EGA] p. 80Proposition 1.1.2(i)zarcls0 32786  zarcls1 32787
[EGA] p. 81Corollary 1.1.8zart0 32797
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 32800
[EGA], p. 83Corollary 1.2.3rhmpreimacn 32803
[Eisenberg] p. 67Definition 5.3df-dif 3950
[Eisenberg] p. 82Definition 6.3dfom3 9638
[Eisenberg] p. 125Definition 8.21df-map 8818
[Eisenberg] p. 216Example 13.2(4)omenps 9646
[Eisenberg] p. 310Theorem 19.8cardprc 9971
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10546
[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 31767  iunin2 5073  uniin1 31761  uniin2 31762
[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 7753  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 7898  rnexg 7890
[Enderton] p. 41Exercise 8dmuni 5912  rnuni 6145
[Enderton] p. 42Definition of a functiondffun7 6572  dffun8 6573
[Enderton] p. 43Definition of function valuefunfv2 6975
[Enderton] p. 43Definition of single-rootedfuncnv 6614
[Enderton] p. 44Definition (d)dfima2 6059  dfima3 6060
[Enderton] p. 47Theorem 3Hfvco2 6984
[Enderton] p. 49Axiom of Choice (first form)ac7 10464  ac7g 10465  df-ac 10107  dfac2 10122  dfac2a 10120  dfac2b 10121  dfac3 10112  dfac7 10123
[Enderton] p. 50Theorem 3K(a)imauni 7240
[Enderton] p. 52Definitiondf-map 8818
[Enderton] p. 53Exercise 21coass 6261
[Enderton] p. 53Exercise 27dmco 6250
[Enderton] p. 53Exercise 14(a)funin 6621
[Enderton] p. 53Exercise 22(a)imass2 6098
[Enderton] p. 54Remarkixpf 8910  ixpssmap 8922
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8888
[Enderton] p. 55Axiom of Choice (second form)ac9 10474  ac9s 10484
[Enderton] p. 56Theorem 3Meqvrelref 37418  erref 8719
[Enderton] p. 57Lemma 3Neqvrelthi 37421  erthi 8750
[Enderton] p. 57Definitiondf-ec 8701
[Enderton] p. 58Definitiondf-qs 8705
[Enderton] p. 61Exercise 35df-ec 8701
[Enderton] p. 65Exercise 56(a)dmun 5908
[Enderton] p. 68Definition of successordf-suc 6367
[Enderton] p. 71Definitiondf-tr 5265  dftr4 5271
[Enderton] p. 72Theorem 4Eunisuc 6440  unisucg 6439
[Enderton] p. 73Exercise 6unisuc 6440  unisucg 6439
[Enderton] p. 73Exercise 5(a)truni 5280
[Enderton] p. 73Exercise 5(b)trint 5282  trintALT 43575
[Enderton] p. 79Theorem 4I(A1)nna0 8600
[Enderton] p. 79Theorem 4I(A2)nnasuc 8602  onasuc 8523
[Enderton] p. 79Definition of operation valuedf-ov 7407
[Enderton] p. 80Theorem 4J(A1)nnm0 8601
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8603  onmsuc 8524
[Enderton] p. 81Theorem 4K(1)nnaass 8618
[Enderton] p. 81Theorem 4K(2)nna0r 8605  nnacom 8613
[Enderton] p. 81Theorem 4K(3)nndi 8619
[Enderton] p. 81Theorem 4K(4)nnmass 8620
[Enderton] p. 81Theorem 4K(5)nnmcom 8622
[Enderton] p. 82Exercise 16nnm0r 8606  nnmsucr 8621
[Enderton] p. 88Exercise 23nnaordex 8634
[Enderton] p. 129Definitiondf-en 8936
[Enderton] p. 132Theorem 6B(b)canth 7357
[Enderton] p. 133Exercise 1xpomen 10006
[Enderton] p. 133Exercise 2qnnen 16152
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9206
[Enderton] p. 135Corollary 6Cphp3 9208
[Enderton] p. 136Corollary 6Enneneq 9205
[Enderton] p. 136Corollary 6D(a)pssinf 9252
[Enderton] p. 136Corollary 6D(b)ominf 9254
[Enderton] p. 137Lemma 6Fpssnn 9164
[Enderton] p. 138Corollary 6Gssfi 9169
[Enderton] p. 139Theorem 6H(c)mapen 9137
[Enderton] p. 142Theorem 6I(3)xpdjuen 10170
[Enderton] p. 142Theorem 6I(4)mapdjuen 10171
[Enderton] p. 143Theorem 6Jdju0en 10166  dju1en 10162
[Enderton] p. 144Exercise 13iunfi 9336  unifi 9337  unifi2 9338
[Enderton] p. 144Corollary 6Kundif2 4475  unfi 9168  unfi2 9311
[Enderton] p. 145Figure 38ffoss 7927
[Enderton] p. 145Definitiondf-dom 8937
[Enderton] p. 146Example 1domen 8953  domeng 8954
[Enderton] p. 146Example 3nndomo 9229  nnsdom 9645  nnsdomg 9298
[Enderton] p. 149Theorem 6L(a)djudom2 10174
[Enderton] p. 149Theorem 6L(c)mapdom1 9138  xpdom1 9067  xpdom1g 9065  xpdom2g 9064
[Enderton] p. 149Theorem 6L(d)mapdom2 9144
[Enderton] p. 151Theorem 6Mzorn 10498  zorng 10495
[Enderton] p. 151Theorem 6M(4)ac8 10483  dfac5 10119
[Enderton] p. 159Theorem 6Qunictb 10566
[Enderton] p. 164Exampleinfdif 10200
[Enderton] p. 168Definitiondf-po 5587
[Enderton] p. 192Theorem 7M(a)oneli 6475
[Enderton] p. 192Theorem 7M(b)ontr1 6407
[Enderton] p. 192Theorem 7M(c)onirri 6474
[Enderton] p. 193Corollary 7N(b)0elon 6415
[Enderton] p. 193Corollary 7N(c)onsuci 7822
[Enderton] p. 193Corollary 7N(d)ssonunii 7763
[Enderton] p. 194Remarkonprc 7760
[Enderton] p. 194Exercise 16suc11 6468
[Enderton] p. 197Definitiondf-card 9930
[Enderton] p. 197Theorem 7Pcarden 10542
[Enderton] p. 200Exercise 25tfis 7839
[Enderton] p. 202Lemma 7Tr1tr 9767
[Enderton] p. 202Definitiondf-r1 9755
[Enderton] p. 202Theorem 7Qr1val1 9777
[Enderton] p. 204Theorem 7V(b)rankval4 9858
[Enderton] p. 206Theorem 7X(b)en2lp 9597
[Enderton] p. 207Exercise 30rankpr 9848  rankprb 9842  rankpw 9834  rankpwi 9814  rankuniss 9857
[Enderton] p. 207Exercise 34opthreg 9609
[Enderton] p. 208Exercise 35suc11reg 9610
[Enderton] p. 212Definition of alephalephval3 10101
[Enderton] p. 213Theorem 8A(a)alephord2 10067
[Enderton] p. 213Theorem 8A(b)cardalephex 10081
[Enderton] p. 218Theorem Schema 8Eonfununi 8336
[Enderton] p. 222Definition of kardkarden 9886  kardex 9885
[Enderton] p. 238Theorem 8Roeoa 8593
[Enderton] p. 238Theorem 8Soeoe 8595
[Enderton] p. 240Exercise 25oarec 8558
[Enderton] p. 257Definition of cofinalitycflm 10241
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17582
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17528
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18502  mrieqv2d 17579  mrieqvd 17578
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17583
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17588  mreexexlem2d 17585
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18508  mreexfidimd 17590
[Frege1879] p. 11Statementdf3or2 42452
[Frege1879] p. 12Statementdf3an2 42453  dfxor4 42450  dfxor5 42451
[Frege1879] p. 26Axiom 1ax-frege1 42474
[Frege1879] p. 26Axiom 2ax-frege2 42475
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 42479
[Frege1879] p. 31Proposition 4frege4 42483
[Frege1879] p. 32Proposition 5frege5 42484
[Frege1879] p. 33Proposition 6frege6 42490
[Frege1879] p. 34Proposition 7frege7 42492
[Frege1879] p. 35Axiom 8ax-frege8 42493  axfrege8 42491
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 36264
[Frege1879] p. 35Proposition 9frege9 42496
[Frege1879] p. 36Proposition 10frege10 42504
[Frege1879] p. 36Proposition 11frege11 42498
[Frege1879] p. 37Proposition 12frege12 42497
[Frege1879] p. 37Proposition 13frege13 42506
[Frege1879] p. 37Proposition 14frege14 42507
[Frege1879] p. 38Proposition 15frege15 42510
[Frege1879] p. 38Proposition 16frege16 42500
[Frege1879] p. 39Proposition 17frege17 42505
[Frege1879] p. 39Proposition 18frege18 42502
[Frege1879] p. 39Proposition 19frege19 42508
[Frege1879] p. 40Proposition 20frege20 42512
[Frege1879] p. 40Proposition 21frege21 42511
[Frege1879] p. 41Proposition 22frege22 42503
[Frege1879] p. 42Proposition 23frege23 42509
[Frege1879] p. 42Proposition 24frege24 42499
[Frege1879] p. 42Proposition 25frege25 42501  rp-frege25 42489
[Frege1879] p. 42Proposition 26frege26 42494
[Frege1879] p. 43Axiom 28ax-frege28 42514
[Frege1879] p. 43Proposition 27frege27 42495
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 42515
[Frege1879] p. 44Axiom 31ax-frege31 42518  axfrege31 42517
[Frege1879] p. 44Proposition 30frege30 42516
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 42519
[Frege1879] p. 44Proposition 33frege33 42520
[Frege1879] p. 45Proposition 34frege34 42521
[Frege1879] p. 45Proposition 35frege35 42522
[Frege1879] p. 45Proposition 36frege36 42523
[Frege1879] p. 46Proposition 37frege37 42524
[Frege1879] p. 46Proposition 38frege38 42525
[Frege1879] p. 46Proposition 39frege39 42526
[Frege1879] p. 46Proposition 40frege40 42527
[Frege1879] p. 47Axiom 41ax-frege41 42529  axfrege41 42528
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 42530
[Frege1879] p. 47Proposition 43frege43 42531
[Frege1879] p. 47Proposition 44frege44 42532
[Frege1879] p. 47Proposition 45frege45 42533
[Frege1879] p. 48Proposition 46frege46 42534
[Frege1879] p. 48Proposition 47frege47 42535
[Frege1879] p. 49Proposition 48frege48 42536
[Frege1879] p. 49Proposition 49frege49 42537
[Frege1879] p. 49Proposition 50frege50 42538
[Frege1879] p. 50Axiom 52ax-frege52a 42541  ax-frege52c 42572  frege52aid 42542  frege52b 42573
[Frege1879] p. 50Axiom 54ax-frege54a 42546  ax-frege54c 42576  frege54b 42577
[Frege1879] p. 50Proposition 51frege51 42539
[Frege1879] p. 50Proposition 52dfsbcq 3778
[Frege1879] p. 50Proposition 53frege53a 42544  frege53aid 42543  frege53b 42574  frege53c 42598
[Frege1879] p. 50Proposition 54biid 261  eqid 2733
[Frege1879] p. 50Proposition 55frege55a 42552  frege55aid 42549  frege55b 42581  frege55c 42602  frege55cor1a 42553  frege55lem2a 42551  frege55lem2b 42580  frege55lem2c 42601
[Frege1879] p. 50Proposition 56frege56a 42555  frege56aid 42554  frege56b 42582  frege56c 42603
[Frege1879] p. 51Axiom 58ax-frege58a 42559  ax-frege58b 42585  frege58bid 42586  frege58c 42605
[Frege1879] p. 51Proposition 57frege57a 42557  frege57aid 42556  frege57b 42583  frege57c 42604
[Frege1879] p. 51Proposition 58spsbc 3789
[Frege1879] p. 51Proposition 59frege59a 42561  frege59b 42588  frege59c 42606
[Frege1879] p. 52Proposition 60frege60a 42562  frege60b 42589  frege60c 42607
[Frege1879] p. 52Proposition 61frege61a 42563  frege61b 42590  frege61c 42608
[Frege1879] p. 52Proposition 62frege62a 42564  frege62b 42591  frege62c 42609
[Frege1879] p. 52Proposition 63frege63a 42565  frege63b 42592  frege63c 42610
[Frege1879] p. 53Proposition 64frege64a 42566  frege64b 42593  frege64c 42611
[Frege1879] p. 53Proposition 65frege65a 42567  frege65b 42594  frege65c 42612
[Frege1879] p. 54Proposition 66frege66a 42568  frege66b 42595  frege66c 42613
[Frege1879] p. 54Proposition 67frege67a 42569  frege67b 42596  frege67c 42614
[Frege1879] p. 54Proposition 68frege68a 42570  frege68b 42597  frege68c 42615
[Frege1879] p. 55Definition 69dffrege69 42616
[Frege1879] p. 58Proposition 70frege70 42617
[Frege1879] p. 59Proposition 71frege71 42618
[Frege1879] p. 59Proposition 72frege72 42619
[Frege1879] p. 59Proposition 73frege73 42620
[Frege1879] p. 60Definition 76dffrege76 42623
[Frege1879] p. 60Proposition 74frege74 42621
[Frege1879] p. 60Proposition 75frege75 42622
[Frege1879] p. 62Proposition 77frege77 42624  frege77d 42430
[Frege1879] p. 63Proposition 78frege78 42625
[Frege1879] p. 63Proposition 79frege79 42626
[Frege1879] p. 63Proposition 80frege80 42627
[Frege1879] p. 63Proposition 81frege81 42628  frege81d 42431
[Frege1879] p. 64Proposition 82frege82 42629
[Frege1879] p. 65Proposition 83frege83 42630  frege83d 42432
[Frege1879] p. 65Proposition 84frege84 42631
[Frege1879] p. 66Proposition 85frege85 42632
[Frege1879] p. 66Proposition 86frege86 42633
[Frege1879] p. 66Proposition 87frege87 42634  frege87d 42434
[Frege1879] p. 67Proposition 88frege88 42635
[Frege1879] p. 68Proposition 89frege89 42636
[Frege1879] p. 68Proposition 90frege90 42637
[Frege1879] p. 68Proposition 91frege91 42638  frege91d 42435
[Frege1879] p. 69Proposition 92frege92 42639
[Frege1879] p. 70Proposition 93frege93 42640
[Frege1879] p. 70Proposition 94frege94 42641
[Frege1879] p. 70Proposition 95frege95 42642
[Frege1879] p. 71Definition 99dffrege99 42646
[Frege1879] p. 71Proposition 96frege96 42643  frege96d 42433
[Frege1879] p. 71Proposition 97frege97 42644  frege97d 42436
[Frege1879] p. 71Proposition 98frege98 42645  frege98d 42437
[Frege1879] p. 72Proposition 100frege100 42647
[Frege1879] p. 72Proposition 101frege101 42648
[Frege1879] p. 72Proposition 102frege102 42649  frege102d 42438
[Frege1879] p. 73Proposition 103frege103 42650
[Frege1879] p. 73Proposition 104frege104 42651
[Frege1879] p. 73Proposition 105frege105 42652
[Frege1879] p. 73Proposition 106frege106 42653  frege106d 42439
[Frege1879] p. 74Proposition 107frege107 42654
[Frege1879] p. 74Proposition 108frege108 42655  frege108d 42440
[Frege1879] p. 74Proposition 109frege109 42656  frege109d 42441
[Frege1879] p. 75Proposition 110frege110 42657
[Frege1879] p. 75Proposition 111frege111 42658  frege111d 42443
[Frege1879] p. 76Proposition 112frege112 42659
[Frege1879] p. 76Proposition 113frege113 42660
[Frege1879] p. 76Proposition 114frege114 42661  frege114d 42442
[Frege1879] p. 77Definition 115dffrege115 42662
[Frege1879] p. 77Proposition 116frege116 42663
[Frege1879] p. 78Proposition 117frege117 42664
[Frege1879] p. 78Proposition 118frege118 42665
[Frege1879] p. 78Proposition 119frege119 42666
[Frege1879] p. 78Proposition 120frege120 42667
[Frege1879] p. 79Proposition 121frege121 42668
[Frege1879] p. 79Proposition 122frege122 42669  frege122d 42444
[Frege1879] p. 79Proposition 123frege123 42670
[Frege1879] p. 80Proposition 124frege124 42671  frege124d 42445
[Frege1879] p. 81Proposition 125frege125 42672
[Frege1879] p. 81Proposition 126frege126 42673  frege126d 42446
[Frege1879] p. 82Proposition 127frege127 42674
[Frege1879] p. 83Proposition 128frege128 42675
[Frege1879] p. 83Proposition 129frege129 42676  frege129d 42447
[Frege1879] p. 84Proposition 130frege130 42677
[Frege1879] p. 85Proposition 131frege131 42678  frege131d 42448
[Frege1879] p. 86Proposition 132frege132 42679
[Frege1879] p. 86Proposition 133frege133 42680  frege133d 42449
[Fremlin1] p. 13Definition 111G (b)df-salgen 44964
[Fremlin1] p. 13Definition 111G (d)borelmbl 45287
[Fremlin1] p. 13Proposition 111G (b)salgenss 44987
[Fremlin1] p. 14Definition 112Aismea 45102
[Fremlin1] p. 15Remark 112B (d)psmeasure 45122
[Fremlin1] p. 15Property 112C (a)meadjun 45113  meadjunre 45127
[Fremlin1] p. 15Property 112C (b)meassle 45114
[Fremlin1] p. 15Property 112C (c)meaunle 45115
[Fremlin1] p. 16Property 112C (d)iundjiun 45111  meaiunle 45120  meaiunlelem 45119
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 45132  meaiuninc2 45133  meaiuninc3 45136  meaiuninc3v 45135  meaiunincf 45134  meaiuninclem 45131
[Fremlin1] p. 16Proposition 112C (f)meaiininc 45138  meaiininc2 45139  meaiininclem 45137
[Fremlin1] p. 19Theorem 113Ccaragen0 45157  caragendifcl 45165  caratheodory 45179  omelesplit 45169
[Fremlin1] p. 19Definition 113Aisome 45145  isomennd 45182  isomenndlem 45181
[Fremlin1] p. 19Remark 113B (c)omeunle 45167
[Fremlin1] p. 19Definition 112Dfcaragencmpl 45186  voncmpl 45272
[Fremlin1] p. 19Definition 113A (ii)omessle 45149
[Fremlin1] p. 20Theorem 113Ccarageniuncl 45174  carageniuncllem1 45172  carageniuncllem2 45173  caragenuncl 45164  caragenuncllem 45163  caragenunicl 45175
[Fremlin1] p. 21Remark 113Dcaragenel2d 45183
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 45177  caratheodorylem2 45178
[Fremlin1] p. 21Exercise 113Xacaragencmpl 45186
[Fremlin1] p. 23Lemma 114Bhoidmv1le 45245  hoidmv1lelem1 45242  hoidmv1lelem2 45243  hoidmv1lelem3 45244
[Fremlin1] p. 25Definition 114Eisvonmbl 45289
[Fremlin1] p. 29Lemma 115Bhoidmv1le 45245  hoidmvle 45251  hoidmvlelem1 45246  hoidmvlelem2 45247  hoidmvlelem3 45248  hoidmvlelem4 45249  hoidmvlelem5 45250  hsphoidmvle2 45236  hsphoif 45227  hsphoival 45230
[Fremlin1] p. 29Definition 1135 (b)hoicvr 45199
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 45207
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 45234  hoidmvn0val 45235  hoidmvval 45228  hoidmvval0 45238  hoidmvval0b 45241
[Fremlin1] p. 30Lemma 115Bhoiprodp1 45239  hsphoidmvle 45237
[Fremlin1] p. 30Definition 115Cdf-ovoln 45188  df-voln 45190
[Fremlin1] p. 30Proposition 115D (a)dmovn 45255  ovn0 45217  ovn0lem 45216  ovnf 45214  ovnome 45224  ovnssle 45212  ovnsslelem 45211  ovnsupge0 45208
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 45254  ovnhoilem1 45252  ovnhoilem2 45253  vonhoi 45318
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 45271  hoidifhspf 45269  hoidifhspval 45259  hoidifhspval2 45266  hoidifhspval3 45270  hspmbl 45280  hspmbllem1 45277  hspmbllem2 45278  hspmbllem3 45279
[Fremlin1] p. 31Definition 115Evoncmpl 45272  vonmea 45225
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 45223  ovnsubadd2 45297  ovnsubadd2lem 45296  ovnsubaddlem1 45221  ovnsubaddlem2 45222
[Fremlin1] p. 32Proposition 115G (a)hoimbl 45282  hoimbl2 45316  hoimbllem 45281  hspdifhsp 45267  opnvonmbl 45285  opnvonmbllem2 45284
[Fremlin1] p. 32Proposition 115G (b)borelmbl 45287
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 45330  iccvonmbllem 45329  ioovonmbl 45328
[Fremlin1] p. 32Proposition 115G (d)vonicc 45336  vonicclem2 45335  vonioo 45333  vonioolem2 45332  vonn0icc 45339  vonn0icc2 45343  vonn0ioo 45338  vonn0ioo2 45341
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 45340  snvonmbl 45337  vonct 45344  vonsn 45342
[Fremlin1] p. 35Lemma 121Asubsalsal 45010
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 45009  subsaliuncllem 45008
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 45376  salpreimalegt 45360  salpreimaltle 45377
[Fremlin1] p. 35Proposition 121B (i)issmf 45379  issmff 45385  issmflem 45378
[Fremlin1] p. 35Proposition 121B (ii)issmfle 45396  issmflelem 45395  smfpreimale 45405
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 45407  issmfgtlem 45406
[Fremlin1] p. 36Definition 121Cdf-smblfn 45347  issmf 45379  issmff 45385  issmfge 45421  issmfgelem 45420  issmfgt 45407  issmfgtlem 45406  issmfle 45396  issmflelem 45395  issmflem 45378
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 45358  salpreimagtlt 45381  salpreimalelt 45380
[Fremlin1] p. 36Proposition 121B (iv)issmfge 45421  issmfgelem 45420
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 45404
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 45402  cnfsmf 45391
[Fremlin1] p. 36Proposition 121D (c)decsmf 45418  decsmflem 45417  incsmf 45393  incsmflem 45392
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 45352  pimconstlt1 45353  smfconst 45400
[Fremlin1] p. 37Proposition 121E (b)smfadd 45416  smfaddlem1 45414  smfaddlem2 45415
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 45447
[Fremlin1] p. 37Proposition 121E (d)smfmul 45446  smfmullem1 45442  smfmullem2 45443  smfmullem3 45444  smfmullem4 45445
[Fremlin1] p. 37Proposition 121E (e)smfdiv 45448
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 45451  smfpimbor1lem2 45450
[Fremlin1] p. 37Proposition 121E (g)smfco 45453
[Fremlin1] p. 37Proposition 121E (h)smfres 45441
[Fremlin1] p. 38Proposition 121E (e)smfrec 45440
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 45449  smfresal 45439
[Fremlin1] p. 38Proposition 121F (a)smflim 45428  smflim2 45457  smflimlem1 45422  smflimlem2 45423  smflimlem3 45424  smflimlem4 45425  smflimlem5 45426  smflimlem6 45427  smflimmpt 45461
[Fremlin1] p. 38Proposition 121F (b)smfsup 45465  smfsuplem1 45462  smfsuplem2 45463  smfsuplem3 45464  smfsupmpt 45466  smfsupxr 45467
[Fremlin1] p. 38Proposition 121F (c)smfinf 45469  smfinflem 45468  smfinfmpt 45470
[Fremlin1] p. 39Remark 121Gsmflim 45428  smflim2 45457  smflimmpt 45461
[Fremlin1] p. 39Proposition 121Fsmfpimcc 45459
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 45489  smfdivdmmbl2 45492  smfinfdmmbl 45500  smfinfdmmbllem 45499  smfsupdmmbl 45496  smfsupdmmbllem 45495
[Fremlin1] p. 39Proposition 121F (d)smflimsup 45479  smflimsuplem2 45472  smflimsuplem6 45476  smflimsuplem7 45477  smflimsuplem8 45478  smflimsupmpt 45480
[Fremlin1] p. 39Proposition 121F (e)smfliminf 45482  smfliminflem 45481  smfliminfmpt 45483
[Fremlin1] p. 80Definition 135E (b)df-smblfn 45347
[Fremlin1], p. 38Proposition 121F (b)fsupdm 45493  fsupdm2 45494
[Fremlin1], p. 39Proposition 121Hadddmmbl 45484  adddmmbl2 45485  finfdm 45497  finfdm2 45498  fsupdm 45493  fsupdm2 45494  muldmmbl 45486  muldmmbl2 45487
[Fremlin1], p. 39Proposition 121F (c)finfdm 45497  finfdm2 45498
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25035
[Fremlin5] p. 213Lemma 565Cauniioovol 25078
[Fremlin5] p. 214Lemma 565Cauniioombl 25088
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 36504
[Fremlin5] p. 220Theorem 565Maftc1anc 36507
[FreydScedrov] p. 283Axiom of Infinityax-inf 9629  inf1 9613  inf2 9614
[Gleason] p. 117Proposition 9-2.1df-enq 10902  enqer 10912
[Gleason] p. 117Proposition 9-2.2df-1nq 10907  df-nq 10903
[Gleason] p. 117Proposition 9-2.3df-plpq 10899  df-plq 10905
[Gleason] p. 119Proposition 9-2.4caovmo 7639  df-mpq 10900  df-mq 10906
[Gleason] p. 119Proposition 9-2.5df-rq 10908
[Gleason] p. 119Proposition 9-2.6ltexnq 10966
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10967  ltbtwnnq 10969
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10962
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10963
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10970
[Gleason] p. 121Definition 9-3.1df-np 10972
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10984
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10986
[Gleason] p. 122Definitiondf-1p 10973
[Gleason] p. 122Remark (1)prub 10985
[Gleason] p. 122Lemma 9-3.4prlem934 11024
[Gleason] p. 122Proposition 9-3.2df-ltp 10976
[Gleason] p. 122Proposition 9-3.3ltsopr 11023  psslinpr 11022  supexpr 11045  suplem1pr 11043  suplem2pr 11044
[Gleason] p. 123Proposition 9-3.5addclpr 11009  addclprlem1 11007  addclprlem2 11008  df-plp 10974
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11013
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11012
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11025
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11034  ltexprlem1 11027  ltexprlem2 11028  ltexprlem3 11029  ltexprlem4 11030  ltexprlem5 11031  ltexprlem6 11032  ltexprlem7 11033
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11036  ltaprlem 11035
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11037
[Gleason] p. 124Lemma 9-3.6prlem936 11038
[Gleason] p. 124Proposition 9-3.7df-mp 10975  mulclpr 11011  mulclprlem 11010  reclem2pr 11039
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11020
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11015
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11014
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11019
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11042  reclem3pr 11040  reclem4pr 11041
[Gleason] p. 126Proposition 9-4.1df-enr 11046  enrer 11054
[Gleason] p. 126Proposition 9-4.2df-0r 11051  df-1r 11052  df-nr 11047
[Gleason] p. 126Proposition 9-4.3df-mr 11049  df-plr 11048  negexsr 11093  recexsr 11098  recexsrlem 11094
[Gleason] p. 127Proposition 9-4.4df-ltr 11050
[Gleason] p. 130Proposition 10-1.3creui 12203  creur 12202  cru 12200
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11179  axcnre 11155
[Gleason] p. 132Definition 10-3.1crim 15058  crimd 15175  crimi 15136  crre 15057  crred 15174  crrei 15135
[Gleason] p. 132Definition 10-3.2remim 15060  remimd 15141
[Gleason] p. 133Definition 10.36absval2 15227  absval2d 15388  absval2i 15340
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15084  cjaddd 15163  cjaddi 15131
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15085  cjmuld 15164  cjmuli 15132
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15083  cjcjd 15142  cjcji 15114
[Gleason] p. 133Proposition 10-3.4(f)cjre 15082  cjreb 15066  cjrebd 15145  cjrebi 15117  cjred 15169  rere 15065  rereb 15063  rerebd 15144  rerebi 15116  rered 15167
[Gleason] p. 133Proposition 10-3.4(h)addcj 15091  addcjd 15155  addcji 15126
[Gleason] p. 133Proposition 10-3.7(a)absval 15181
[Gleason] p. 133Proposition 10-3.7(b)abscj 15222  abscjd 15393  abscji 15344
[Gleason] p. 133Proposition 10-3.7(c)abs00 15232  abs00d 15389  abs00i 15341  absne0d 15390
[Gleason] p. 133Proposition 10-3.7(d)releabs 15264  releabsd 15394  releabsi 15345
[Gleason] p. 133Proposition 10-3.7(f)absmul 15237  absmuld 15397  absmuli 15347
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15225  sqabsaddi 15348
[Gleason] p. 133Proposition 10-3.7(h)abstri 15273  abstrid 15399  abstrii 15351
[Gleason] p. 134Definition 10-4.1df-exp 14024  exp0 14027  expp1 14030  expp1d 14108
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26169  cxpaddd 26207  expadd 14066  expaddd 14109  expaddz 14068
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26178  cxpmuld 26226  expmul 14069  expmuld 14110  expmulz 14070
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26175  mulcxpd 26218  mulexp 14063  mulexpd 14122  mulexpz 14064
[Gleason] p. 140Exercise 1znnen 16151
[Gleason] p. 141Definition 11-2.1fzval 13482
[Gleason] p. 168Proposition 12-2.1(a)climadd 15572  rlimadd 15583  rlimdiv 15588
[Gleason] p. 168Proposition 12-2.1(b)climsub 15574  rlimsub 15585
[Gleason] p. 168Proposition 12-2.1(c)climmul 15573  rlimmul 15586
[Gleason] p. 171Corollary 12-2.2climmulc2 15577
[Gleason] p. 172Corollary 12-2.5climrecl 15523
[Gleason] p. 172Proposition 12-2.4(c)climabs 15544  climcj 15545  climim 15547  climre 15546  rlimabs 15549  rlimcj 15550  rlimim 15552  rlimre 15551
[Gleason] p. 173Definition 12-3.1df-ltxr 11249  df-xr 11248  ltxr 13091
[Gleason] p. 175Definition 12-4.1df-limsup 15411  limsupval 15414
[Gleason] p. 180Theorem 12-5.1climsup 15612
[Gleason] p. 180Theorem 12-5.3caucvg 15621  caucvgb 15622  caucvgbf 44135  caucvgr 15618  climcau 15613
[Gleason] p. 182Exercise 3cvgcmp 15758
[Gleason] p. 182Exercise 4cvgrat 15825
[Gleason] p. 195Theorem 13-2.12abs1m 15278
[Gleason] p. 217Lemma 13-4.1btwnzge0 13789
[Gleason] p. 223Definition 14-1.1df-met 20923
[Gleason] p. 223Definition 14-1.1(a)met0 23831  xmet0 23830
[Gleason] p. 223Definition 14-1.1(b)metgt0 23847
[Gleason] p. 223Definition 14-1.1(c)metsym 23838
[Gleason] p. 223Definition 14-1.1(d)mettri 23840  mstri 23957  xmettri 23839  xmstri 23956
[Gleason] p. 225Definition 14-1.5xpsmet 23870
[Gleason] p. 230Proposition 14-2.6txlm 23134
[Gleason] p. 240Theorem 14-4.3metcnp4 24809
[Gleason] p. 240Proposition 14-4.2metcnp3 24031
[Gleason] p. 243Proposition 14-4.16addcn 24363  addcn2 15534  mulcn 24365  mulcn2 15536  subcn 24364  subcn2 15535
[Gleason] p. 295Remarkbcval3 14262  bcval4 14263
[Gleason] p. 295Equation 2bcpasc 14277
[Gleason] p. 295Definition of binomial coefficientbcval 14260  df-bc 14259
[Gleason] p. 296Remarkbcn0 14266  bcnn 14268
[Gleason] p. 296Theorem 15-2.8binom 15772
[Gleason] p. 308Equation 2ef0 16030
[Gleason] p. 308Equation 3efcj 16031
[Gleason] p. 309Corollary 15-4.3efne0 16036
[Gleason] p. 309Corollary 15-4.4efexp 16040
[Gleason] p. 310Equation 14sinadd 16103
[Gleason] p. 310Equation 15cosadd 16104
[Gleason] p. 311Equation 17sincossq 16115
[Gleason] p. 311Equation 18cosbnd 16120  sinbnd 16119
[Gleason] p. 311Lemma 15-4.7sqeqor 14176  sqeqori 14174
[Gleason] p. 311Definition of ` `df-pi 16012
[Godowski] p. 730Equation SFgoeqi 31504
[GodowskiGreechie] p. 249Equation IV3oai 30899
[Golan] p. 1Remarksrgisid 20023
[Golan] p. 1Definitiondf-srg 20001
[Golan] p. 149Definitiondf-slmd 32324
[Gonshor] p. 7Definitiondf-scut 27265
[Gonshor] p. 9Theorem 2.5slerec 27300
[Gonshor] p. 10Theorem 2.6cofcut1 27387  cofcut1d 27388
[Gonshor] p. 10Theorem 2.7cofcut2 27389  cofcut2d 27390
[Gonshor] p. 12Theorem 2.9cofcutr 27391  cofcutr1d 27392  cofcutr2d 27393
[Gonshor] p. 13Definitiondf-adds 27424
[Gonshor] p. 14Theorem 3.1addsprop 27440
[Gonshor] p. 15Theorem 3.2addsunif 27465
[Gonshor] p. 17Theorem 3.4mulsprop 27566
[Gonshor] p. 18Theorem 3.5mulsunif 27585
[GramKnuthPat], p. 47Definition 2.42df-fwddif 35069
[Gratzer] p. 23Section 0.6df-mre 17526
[Gratzer] p. 27Section 0.6df-mri 17528
[Hall] p. 1Section 1.1df-asslaw 46533  df-cllaw 46531  df-comlaw 46532
[Hall] p. 2Section 1.2df-clintop 46545
[Hall] p. 7Section 1.3df-sgrp2 46566
[Halmos] p. 28Partition ` `df-parts 37573  dfmembpart2 37578
[Halmos] p. 31Theorem 17.3riesz1 31296  riesz2 31297
[Halmos] p. 41Definition of Hermitianhmopadj2 31172
[Halmos] p. 42Definition of projector orderingpjordi 31404
[Halmos] p. 43Theorem 26.1elpjhmop 31416  elpjidm 31415  pjnmopi 31379
[Halmos] p. 44Remarkpjinormi 30918  pjinormii 30907
[Halmos] p. 44Theorem 26.2elpjch 31420  pjrn 30938  pjrni 30933  pjvec 30927
[Halmos] p. 44Theorem 26.3pjnorm2 30958
[Halmos] p. 44Theorem 26.4hmopidmpj 31385  hmopidmpji 31383
[Halmos] p. 45Theorem 27.1pjinvari 31422
[Halmos] p. 45Theorem 27.3pjoci 31411  pjocvec 30928
[Halmos] p. 45Theorem 27.4pjorthcoi 31400
[Halmos] p. 48Theorem 29.2pjssposi 31403
[Halmos] p. 48Theorem 29.3pjssdif1i 31406  pjssdif2i 31405
[Halmos] p. 50Definition of spectrumdf-spec 31086
[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 1798
[Hatcher] p. 25Definitiondf-phtpc 24490  df-phtpy 24469
[Hatcher] p. 26Definitiondf-pco 24503  df-pi1 24506
[Hatcher] p. 26Proposition 1.2phtpcer 24493
[Hatcher] p. 26Proposition 1.3pi1grp 24548
[Hefferon] p. 240Definition 3.12df-dmat 21974  df-dmatalt 46981
[Helfgott] p. 2Theoremtgoldbach 46420
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 46405
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 46417  bgoldbtbnd 46412  bgoldbtbnd 46412  tgblthelfgott 46418
[Helfgott] p. 5Proposition 1.1circlevma 33592
[Helfgott] p. 69Statement 7.49circlemethhgt 33593
[Helfgott] p. 69Statement 7.50hgt750lema 33607  hgt750lemb 33606  hgt750leme 33608  hgt750lemf 33603  hgt750lemg 33604
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 46414  tgoldbachgt 33613  tgoldbachgtALTV 46415  tgoldbachgtd 33612
[Helfgott] p. 70Statement 7.49ax-hgt749 33594
[Herstein] p. 54Exercise 28df-grpo 29724
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18826  grpoideu 29740  mndideu 18632
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18855  grpoinveu 29750
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18886  grpo2inv 29762
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18897  grpoinvop 29764
[Herstein] p. 57Exercise 1dfgrp3e 18919
[Hitchcock] p. 5Rule A3mptnan 1771
[Hitchcock] p. 5Rule A4mptxor 1772
[Hitchcock] p. 5Rule A5mtpxor 1774
[Holland] p. 1519Theorem 2sumdmdi 31651
[Holland] p. 1520Lemma 5cdj1i 31664  cdj3i 31672  cdj3lem1 31665  cdjreui 31663
[Holland] p. 1524Lemma 7mddmdin0i 31662
[Holland95] p. 13Theorem 3.6hlathil 40774
[Holland95] p. 14Line 15hgmapvs 40700
[Holland95] p. 14Line 16hdmaplkr 40722
[Holland95] p. 14Line 17hdmapellkr 40723
[Holland95] p. 14Line 19hdmapglnm2 40720
[Holland95] p. 14Line 20hdmapip0com 40726
[Holland95] p. 14Theorem 3.6hdmapevec2 40645
[Holland95] p. 14Lines 24 and 25hdmapoc 40740
[Holland95] p. 204Definition of involutiondf-srng 20442
[Holland95] p. 212Definition of subspacedf-psubsp 38312
[Holland95] p. 214Lemma 3.3lclkrlem2v 40337
[Holland95] p. 214Definition 3.2df-lpolN 40290
[Holland95] p. 214Definition of nonsingularpnonsingN 38742
[Holland95] p. 215Lemma 3.3(1)dihoml4 40186  poml4N 38762
[Holland95] p. 215Lemma 3.3(2)dochexmid 40277  pexmidALTN 38787  pexmidN 38778
[Holland95] p. 218Theorem 3.6lclkr 40342
[Holland95] p. 218Definition of dual vector spacedf-ldual 37932  ldualset 37933
[Holland95] p. 222Item 1df-lines 38310  df-pointsN 38311
[Holland95] p. 222Item 2df-polarityN 38712
[Holland95] p. 223Remarkispsubcl2N 38756  omllaw4 38054  pol1N 38719  polcon3N 38726
[Holland95] p. 223Definitiondf-psubclN 38744
[Holland95] p. 223Equation for polaritypolval2N 38715
[Holmes] p. 40Definitiondf-xrn 37179
[Hughes] p. 44Equation 1.21bax-his3 30315
[Hughes] p. 47Definition of projection operatordfpjop 31413
[Hughes] p. 49Equation 1.30eighmre 31194  eigre 31066  eigrei 31065
[Hughes] p. 49Equation 1.31eighmorth 31195  eigorth 31069  eigorthi 31068
[Hughes] p. 137Remark (ii)eigposi 31067
[Huneke] p. 1Claim 1frgrncvvdeq 29542
[Huneke] p. 1Statement 1frgrncvvdeqlem7 29538
[Huneke] p. 1Statement 2frgrncvvdeqlem8 29539
[Huneke] p. 1Statement 3frgrncvvdeqlem9 29540
[Huneke] p. 2Claim 2frgrregorufr 29558  frgrregorufr0 29557  frgrregorufrg 29559
[Huneke] p. 2Claim 3frgrhash2wsp 29565  frrusgrord 29574  frrusgrord0 29573
[Huneke] p. 2Statementdf-clwwlknon 29321
[Huneke] p. 2Statement 4frgrwopreglem4 29548
[Huneke] p. 2Statement 5frgrwopreg1 29551  frgrwopreg2 29552  frgrwopregasn 29549  frgrwopregbsn 29550
[Huneke] p. 2Statement 6frgrwopreglem5 29554
[Huneke] p. 2Statement 7fusgreghash2wspv 29568
[Huneke] p. 2Statement 8fusgreghash2wsp 29571
[Huneke] p. 2Statement 9clwlksndivn 29319  numclwlk1 29604  numclwlk1lem1 29602  numclwlk1lem2 29603  numclwwlk1 29594  numclwwlk8 29625
[Huneke] p. 2Definition 3frgrwopreglem1 29545
[Huneke] p. 2Definition 4df-clwlks 29008
[Huneke] p. 2Definition 62clwwlk 29580
[Huneke] p. 2Definition 7numclwwlkovh 29606  numclwwlkovh0 29605
[Huneke] p. 2Statement 10numclwwlk2 29614
[Huneke] p. 2Statement 11rusgrnumwlkg 29211
[Huneke] p. 2Statement 12numclwwlk3 29618
[Huneke] p. 2Statement 13numclwwlk5 29621
[Huneke] p. 2Statement 14numclwwlk7 29624
[Indrzejczak] p. 33Definition ` `Enatded 29636  natded 29636
[Indrzejczak] p. 33Definition ` `Inatded 29636
[Indrzejczak] p. 34Definition ` `Enatded 29636  natded 29636
[Indrzejczak] p. 34Definition ` `Inatded 29636
[Jech] p. 4Definition of classcv 1541  cvjust 2727
[Jech] p. 42Lemma 6.1alephexp1 10570
[Jech] p. 42Equation 6.1alephadd 10568  alephmul 10569
[Jech] p. 43Lemma 6.2infmap 10567  infmap2 10209
[Jech] p. 71Lemma 9.3jech9.3 9805
[Jech] p. 72Equation 9.3scott0 9877  scottex 9876
[Jech] p. 72Exercise 9.1rankval4 9858
[Jech] p. 72Scheme "Collection Principle"cp 9882
[Jech] p. 78Noteopthprc 5738
[JonesMatijasevic] p. 694Definition 2.3rmxyval 41587
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 41675
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 41676
[JonesMatijasevic] p. 695Equation 2.7rmxadd 41599
[JonesMatijasevic] p. 695Equation 2.8rmyadd 41603
[JonesMatijasevic] p. 695Equation 2.9rmxp1 41604  rmyp1 41605
[JonesMatijasevic] p. 695Equation 2.10rmxm1 41606  rmym1 41607
[JonesMatijasevic] p. 695Equation 2.11rmx0 41597  rmx1 41598  rmxluc 41608
[JonesMatijasevic] p. 695Equation 2.12rmy0 41601  rmy1 41602  rmyluc 41609
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 41611
[JonesMatijasevic] p. 695Equation 2.14rmydbl 41612
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 41632  jm2.17b 41633  jm2.17c 41634
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 41665
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 41669
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 41660
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 41635  jm2.24nn 41631
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 41674
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 41680  rmygeid 41636
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 41692
[Juillerat] p. 11Section *5etransc 44934  etransclem47 44932  etransclem48 44933
[Juillerat] p. 12Equation (7)etransclem44 44929
[Juillerat] p. 12Equation *(7)etransclem46 44931
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 44917
[Juillerat] p. 13Proofetransclem35 44920
[Juillerat] p. 13Part of case 2 proven inetransclem38 44923
[Juillerat] p. 13Part of case 2 provenetransclem24 44909
[Juillerat] p. 13Part of case 2: proven inetransclem41 44926
[Juillerat] p. 14Proofetransclem23 44908
[KalishMontague] p. 81Note 1ax-6 1972
[KalishMontague] p. 85Lemma 2equid 2016
[KalishMontague] p. 85Lemma 3equcomi 2021
[KalishMontague] p. 86Lemma 7cbvalivw 2011  cbvaliw 2010  wl-cbvmotv 36320  wl-motae 36322  wl-moteq 36321
[KalishMontague] p. 87Lemma 8spimvw 2000  spimw 1975
[KalishMontague] p. 87Lemma 9spfw 2037  spw 2038
[Kalmbach] p. 14Definition of latticechabs1 30747  chabs1i 30749  chabs2 30748  chabs2i 30750  chjass 30764  chjassi 30717  latabs1 18424  latabs2 18425
[Kalmbach] p. 15Definition of atomdf-at 31569  ela 31570
[Kalmbach] p. 15Definition of coverscvbr2 31514  cvrval2 38082
[Kalmbach] p. 16Definitiondf-ol 37986  df-oml 37987
[Kalmbach] p. 20Definition of commutescmbr 30815  cmbri 30821  cmtvalN 38019  df-cm 30814  df-cmtN 37985
[Kalmbach] p. 22Remarkomllaw5N 38055  pjoml5 30844  pjoml5i 30819
[Kalmbach] p. 22Definitionpjoml2 30842  pjoml2i 30816
[Kalmbach] p. 22Theorem 2(v)cmcm 30845  cmcmi 30823  cmcmii 30828  cmtcomN 38057
[Kalmbach] p. 22Theorem 2(ii)omllaw3 38053  omlsi 30635  pjoml 30667  pjomli 30666
[Kalmbach] p. 22Definition of OML lawomllaw2N 38052
[Kalmbach] p. 23Remarkcmbr2i 30827  cmcm3 30846  cmcm3i 30825  cmcm3ii 30830  cmcm4i 30826  cmt3N 38059  cmt4N 38060  cmtbr2N 38061
[Kalmbach] p. 23Lemma 3cmbr3 30839  cmbr3i 30831  cmtbr3N 38062
[Kalmbach] p. 25Theorem 5fh1 30849  fh1i 30852  fh2 30850  fh2i 30853  omlfh1N 38066
[Kalmbach] p. 65Remarkchjatom 31588  chslej 30729  chsleji 30689  shslej 30611  shsleji 30601
[Kalmbach] p. 65Proposition 1chocin 30726  chocini 30685  chsupcl 30571  chsupval2 30641  h0elch 30486  helch 30474  hsupval2 30640  ocin 30527  ococss 30524  shococss 30525
[Kalmbach] p. 65Definition of subspace sumshsval 30543
[Kalmbach] p. 66Remarkdf-pjh 30626  pjssmi 31396  pjssmii 30912
[Kalmbach] p. 67Lemma 3osum 30876  osumi 30873
[Kalmbach] p. 67Lemma 4pjci 31431
[Kalmbach] p. 103Exercise 6atmd2 31631
[Kalmbach] p. 103Exercise 12mdsl0 31541
[Kalmbach] p. 140Remarkhatomic 31591  hatomici 31590  hatomistici 31593
[Kalmbach] p. 140Proposition 1atlatmstc 38127
[Kalmbach] p. 140Proposition 1(i)atexch 31612  lsatexch 37851
[Kalmbach] p. 140Proposition 1(ii)chcv1 31586  cvlcvr1 38147  cvr1 38219
[Kalmbach] p. 140Proposition 1(iii)cvexch 31605  cvexchi 31600  cvrexch 38229
[Kalmbach] p. 149Remark 2chrelati 31595  hlrelat 38211  hlrelat5N 38210  lrelat 37822
[Kalmbach] p. 153Exercise 5lsmcv 20742  lsmsatcv 37818  spansncv 30884  spansncvi 30883
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 37837  spansncv2 31524
[Kalmbach] p. 266Definitiondf-st 31442
[Kalmbach2] p. 8Definition of adjointdf-adjh 31080
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10637  fpwwe2 10634
[KanamoriPincus] p. 416Corollary 1.3canth4 10638
[KanamoriPincus] p. 417Corollary 1.6canthp1 10645
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10640
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10642
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10655
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10659  gchxpidm 10660
[KanamoriPincus] p. 419Theorem 2.1gchacg 10671  gchhar 10670
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10207  unxpwdom 9580
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10661
[Kreyszig] p. 3Property M1metcl 23820  xmetcl 23819
[Kreyszig] p. 4Property M2meteq0 23827
[Kreyszig] p. 8Definition 1.1-8dscmet 24063
[Kreyszig] p. 12Equation 5conjmul 11927  muleqadd 11854
[Kreyszig] p. 18Definition 1.3-2mopnval 23926
[Kreyszig] p. 19Remarkmopntopon 23927
[Kreyszig] p. 19Theorem T1mopn0 23989  mopnm 23932
[Kreyszig] p. 19Theorem T2unimopn 23987
[Kreyszig] p. 19Definition of neighborhoodneibl 23992
[Kreyszig] p. 20Definition 1.3-3metcnp2 24033
[Kreyszig] p. 25Definition 1.4-1lmbr 22744  lmmbr 24757  lmmbr2 24758
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 22866
[Kreyszig] p. 28Theorem 1.4-5lmcau 24812
[Kreyszig] p. 28Definition 1.4-3iscau 24775  iscmet2 24793
[Kreyszig] p. 30Theorem 1.4-7cmetss 24815
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 22947  metelcls 24804
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 24805  metcld2 24806
[Kreyszig] p. 51Equation 2clmvneg1 24597  lmodvneg1 20503  nvinv 29870  vcm 29807
[Kreyszig] p. 51Equation 1aclm0vs 24593  lmod0vs 20493  slmd0vs 32347  vc0 29805
[Kreyszig] p. 51Equation 1blmodvs0 20494  slmdvs0 32348  vcz 29806
[Kreyszig] p. 58Definition 2.2-1imsmet 29922  ngpmet 24094  nrmmetd 24065
[Kreyszig] p. 59Equation 1imsdval 29917  imsdval2 29918  ncvspds 24660  ngpds 24095
[Kreyszig] p. 63Problem 1nmval 24080  nvnd 29919
[Kreyszig] p. 64Problem 2nmeq0 24109  nmge0 24108  nvge0 29904  nvz 29900
[Kreyszig] p. 64Problem 3nmrtri 24115  nvabs 29903
[Kreyszig] p. 91Definition 2.7-1isblo3i 30032
[Kreyszig] p. 92Equation 2df-nmoo 29976
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30038  blocni 30036
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30037
[Kreyszig] p. 129Definition 3.1-1cphipeq0 24703  ipeq0 21175  ipz 29950
[Kreyszig] p. 135Problem 2cphpyth 24715  pythi 30081
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30085
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 24737
[Kreyszig] p. 144Equation 4supcvg 15798
[Kreyszig] p. 144Theorem 3.3-1minvec 24935  minveco 30115
[Kreyszig] p. 196Definition 3.9-1df-aj 29981
[Kreyszig] p. 247Theorem 4.7-2bcth 24828
[Kreyszig] p. 249Theorem 4.7-3ubth 30104
[Kreyszig] p. 470Definition of positive operator orderingleop 31354  leopg 31353
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 31372
[Kreyszig] p. 525Theorem 10.1-1htth 30149
[Kulpa] p. 547Theorempoimir 36459
[Kulpa] p. 547Equation (1)poimirlem32 36458
[Kulpa] p. 547Equation (2)poimirlem31 36457
[Kulpa] p. 548Theorembroucube 36460
[Kulpa] p. 548Equation (6)poimirlem26 36452
[Kulpa] p. 548Equation (7)poimirlem27 36453
[Kunen] p. 10Axiom 0ax6e 2383  axnul 5304
[Kunen] p. 11Axiom 3axnul 5304
[Kunen] p. 12Axiom 6zfrep6 7936
[Kunen] p. 24Definition 10.24mapval 8828  mapvalg 8826
[Kunen] p. 30Lemma 10.20fodomg 10513
[Kunen] p. 31Definition 10.24mapex 8822
[Kunen] p. 95Definition 2.1df-r1 9755
[Kunen] p. 97Lemma 2.10r1elss 9797  r1elssi 9796
[Kunen] p. 107Exercise 4rankop 9849  rankopb 9843  rankuni 9854  rankxplim 9870  rankxpsuc 9873
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 5008
[Lang] , p. 225Corollary 1.3finexttrb 32686
[Lang] p. Definitiondf-rn 5686
[Lang] p. 3Statementlidrideqd 18584  mndbn0 18637
[Lang] p. 3Definitiondf-mnd 18622
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18602
[Lang] p. 4Property of composites. Second formulagsumccat 18718
[Lang] p. 5Equationgsumreidx 19777
[Lang] p. 5Definition of an (infinite) productgsumfsupp 46527
[Lang] p. 6Examplenn0mnd 46524
[Lang] p. 6Equationgsumxp2 19840
[Lang] p. 6Statementcycsubm 19073
[Lang] p. 6Definitionmulgnn0gsum 18954
[Lang] p. 6Observationmndlsmidm 19531
[Lang] p. 7Definitiondfgrp2e 18844
[Lang] p. 30Definitiondf-tocyc 32244
[Lang] p. 32Property (a)cyc3genpm 32289
[Lang] p. 32Property (b)cyc3conja 32294  cycpmconjv 32279
[Lang] p. 53Definitiondf-cat 17608
[Lang] p. 53Axiom CAT 1cat1 18043  cat1lem 18042
[Lang] p. 54Definitiondf-iso 17692
[Lang] p. 57Definitiondf-inito 17930  df-termo 17931
[Lang] p. 58Exampleirinitoringc 46869
[Lang] p. 58Statementinitoeu1 17957  termoeu1 17964
[Lang] p. 62Definitiondf-func 17804
[Lang] p. 65Definitiondf-nat 17890
[Lang] p. 91Notedf-ringc 46805
[Lang] p. 92Statementmxidlprm 32544
[Lang] p. 92Definitionisprmidlc 32524
[Lang] p. 128Remarkdsmmlmod 21284
[Lang] p. 129Prooflincscm 47013  lincscmcl 47015  lincsum 47012  lincsumcl 47014
[Lang] p. 129Statementlincolss 47017
[Lang] p. 129Observationdsmmfi 21277
[Lang] p. 141Theorem 5.3dimkerim 32657  qusdimsum 32658
[Lang] p. 141Corollary 5.4lssdimle 32638
[Lang] p. 147Definitionsnlindsntor 47054
[Lang] p. 504Statementmat1 21931  matring 21927
[Lang] p. 504Definitiondf-mamu 21868
[Lang] p. 505Statementmamuass 21884  mamutpos 21942  matassa 21928  mattposvs 21939  tposmap 21941
[Lang] p. 513Definitionmdet1 22085  mdetf 22079
[Lang] p. 513Theorem 4.4cramer 22175
[Lang] p. 514Proposition 4.6mdetleib 22071
[Lang] p. 514Proposition 4.8mdettpos 22095
[Lang] p. 515Definitiondf-minmar1 22119  smadiadetr 22159
[Lang] p. 515Corollary 4.9mdetero 22094  mdetralt 22092
[Lang] p. 517Proposition 4.15mdetmul 22107
[Lang] p. 518Definitiondf-madu 22118
[Lang] p. 518Proposition 4.16madulid 22129  madurid 22128  matinv 22161
[Lang] p. 561Theorem 3.1cayleyhamilton 22374
[Lang], p. 224Proposition 1.2extdgmul 32685  fedgmul 32661
[Lang], p. 561Remarkchpmatply1 22316
[Lang], p. 561Definitiondf-chpmat 22311
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 43026
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 43021
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 43027
[LeBlanc] p. 277Rule R2axnul 5304
[Levy] p. 12Axiom 4.3.1df-clab 2711
[Levy] p. 59Definitiondf-ttrcl 9699
[Levy] p. 64Theorem 5.6(ii)frinsg 9742
[Levy] p. 338Axiomdf-clel 2811  df-cleq 2725
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2811  df-cleq 2725
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2711
[Levy] p. 358Axiomdf-clab 2711
[Levy58] p. 2Definition Iisfin1-3 10377
[Levy58] p. 2Definition IIdf-fin2 10277
[Levy58] p. 2Definition Iadf-fin1a 10276
[Levy58] p. 2Definition IIIdf-fin3 10279
[Levy58] p. 3Definition Vdf-fin5 10280
[Levy58] p. 3Definition IVdf-fin4 10278
[Levy58] p. 4Definition VIdf-fin6 10281
[Levy58] p. 4Definition VIIdf-fin7 10282
[Levy58], p. 3Theorem 1fin1a2 10406
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27169
[Lipparini] p. 3Lemma 2.1.4noresle 27180
[Lipparini] p. 6Proposition 4.2noinfbnd1 27212  nosupbnd1 27197
[Lipparini] p. 6Proposition 4.3noinfbnd2 27214  nosupbnd2 27199
[Lipparini] p. 7Theorem 5.1noetasuplem3 27218  noetasuplem4 27219
[Lipparini] p. 7Corollary 4.4nosupinfsep 27215
[Lopez-Astorga] p. 12Rule 1mptnan 1771
[Lopez-Astorga] p. 12Rule 2mptxor 1772
[Lopez-Astorga] p. 12Rule 3mtpxor 1774
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 31639
[Maeda] p. 168Lemma 5mdsym 31643  mdsymi 31642
[Maeda] p. 168Lemma 4(i)mdsymlem4 31637  mdsymlem6 31639  mdsymlem7 31640
[Maeda] p. 168Lemma 4(ii)mdsymlem8 31641
[MaedaMaeda] p. 1Remarkssdmd1 31544  ssdmd2 31545  ssmd1 31542  ssmd2 31543
[MaedaMaeda] p. 1Lemma 1.2mddmd2 31540
[MaedaMaeda] p. 1Definition 1.1df-dmd 31512  df-md 31511  mdbr 31525
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 31562  mdslj1i 31550  mdslj2i 31551  mdslle1i 31548  mdslle2i 31549  mdslmd1i 31560  mdslmd2i 31561
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 31552  mdsl2bi 31554  mdsl2i 31553
[MaedaMaeda] p. 2Lemma 1.6mdexchi 31566
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 31563
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 31564
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 31541
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 31546  mdsl3 31547
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 31565
[MaedaMaeda] p. 4Theorem 1.14mdcompli 31660
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 38129  hlrelat1 38209
[MaedaMaeda] p. 31Lemma 7.5lcvexch 37847
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 31567  cvmdi 31555  cvnbtwn4 31520  cvrnbtwn4 38087
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 31568
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 38148  cvp 31606  cvrp 38225  lcvp 37848
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 31630
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 31629
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 38141  hlexch4N 38201
[MaedaMaeda] p. 34Exercise 7.1atabsi 31632
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 38252
[MaedaMaeda] p. 61Definition 15.10psubN 38558  atpsubN 38562  df-pointsN 38311  pointpsubN 38560
[MaedaMaeda] p. 62Theorem 15.5df-pmap 38313  pmap11 38571  pmaple 38570  pmapsub 38577  pmapval 38566
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 38574  pmap1N 38576
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 38579  pmapglb2N 38580  pmapglb2xN 38581  pmapglbx 38578
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 38661
[MaedaMaeda] p. 67Postulate PS1ps-1 38286
[MaedaMaeda] p. 68Lemma 16.2df-padd 38605  paddclN 38651  paddidm 38650
[MaedaMaeda] p. 68Condition PS2ps-2 38287
[MaedaMaeda] p. 68Equation 16.2.1paddass 38647
[MaedaMaeda] p. 69Lemma 16.4ps-1 38286
[MaedaMaeda] p. 69Theorem 16.4ps-2 38287
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19536  lsmmod2 19537  lssats 37820  shatomici 31589  shatomistici 31592  shmodi 30621  shmodsi 30620
[MaedaMaeda] p. 130Remark 29.6dmdmd 31531  mdsymlem7 31640
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 30820
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 30724
[MaedaMaeda] p. 139Remarksumdmdii 31646
[Margaris] p. 40Rule Cexlimiv 1934
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 398  df-ex 1783  df-or 847  dfbi2 476
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 29633
[Margaris] p. 59Section 14notnotrALTVD 43609
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 43610
[Margaris] p. 79Rule Cexinst01 43319  exinst11 43320
[Margaris] p. 89Theorem 19.219.2 1981  19.2g 2182  r19.2z 4493
[Margaris] p. 89Theorem 19.319.3 2196  rr19.3v 3656
[Margaris] p. 89Theorem 19.5alcom 2157
[Margaris] p. 89Theorem 19.6alex 1829
[Margaris] p. 89Theorem 19.7alnex 1784
[Margaris] p. 89Theorem 19.819.8a 2175
[Margaris] p. 89Theorem 19.919.9 2199  19.9h 2283  exlimd 2212  exlimdh 2287
[Margaris] p. 89Theorem 19.11excom 2163  excomim 2164
[Margaris] p. 89Theorem 19.1219.12 2321
[Margaris] p. 90Section 19conventions-labels 29634  conventions-labels 29634  conventions-labels 29634  conventions-labels 29634
[Margaris] p. 90Theorem 19.14exnal 1830
[Margaris] p. 90Theorem 19.152albi 43070  albi 1821
[Margaris] p. 90Theorem 19.1619.16 2219
[Margaris] p. 90Theorem 19.1719.17 2220
[Margaris] p. 90Theorem 19.182exbi 43072  exbi 1850
[Margaris] p. 90Theorem 19.1919.19 2223
[Margaris] p. 90Theorem 19.202alim 43069  2alimdv 1922  alimd 2206  alimdh 1820  alimdv 1920  ax-4 1812  ralimdaa 3258  ralimdv 3170  ralimdva 3168  ralimdvva 3205  sbcimdv 3850
[Margaris] p. 90Theorem 19.2119.21 2201  19.21h 2284  19.21t 2200  19.21vv 43068  alrimd 2209  alrimdd 2208  alrimdh 1867  alrimdv 1933  alrimi 2207  alrimih 1827  alrimiv 1931  alrimivv 1932  hbralrimi 3145  r19.21be 3250  r19.21bi 3249  ralrimd 3262  ralrimdv 3153  ralrimdva 3155  ralrimdvv 3202  ralrimdvva 3210  ralrimi 3255  ralrimia 3256  ralrimiv 3146  ralrimiva 3147  ralrimivv 3199  ralrimivva 3201  ralrimivvva 3204  ralrimivw 3151
[Margaris] p. 90Theorem 19.222exim 43071  2eximdv 1923  exim 1837  eximd 2210  eximdh 1868  eximdv 1921  rexim 3088  reximd2a 3267  reximdai 3259  reximdd 43774  reximddv 3172  reximddv2 3213  reximddv3 43773  reximdv 3171  reximdv2 3165  reximdva 3169  reximdvai 3166  reximdvva 3206  reximi2 3080
[Margaris] p. 90Theorem 19.2319.23 2205  19.23bi 2185  19.23h 2285  19.23t 2204  exlimdv 1937  exlimdvv 1938  exlimexi 43218  exlimiv 1934  exlimivv 1936  rexlimd3 43766  rexlimdv 3154  rexlimdv3a 3160  rexlimdva 3156  rexlimdva2 3158  rexlimdvaa 3157  rexlimdvv 3211  rexlimdvva 3212  rexlimdvw 3161  rexlimiv 3149  rexlimiva 3148  rexlimivv 3200
[Margaris] p. 90Theorem 19.2419.24 1990
[Margaris] p. 90Theorem 19.2519.25 1884
[Margaris] p. 90Theorem 19.2619.26 1874
[Margaris] p. 90Theorem 19.2719.27 2221  r19.27z 4503  r19.27zv 4504
[Margaris] p. 90Theorem 19.2819.28 2222  19.28vv 43078  r19.28z 4496  r19.28zf 43786  r19.28zv 4499  rr19.28v 3657
[Margaris] p. 90Theorem 19.2919.29 1877  r19.29d2r 3141  r19.29imd 3119
[Margaris] p. 90Theorem 19.3019.30 1885
[Margaris] p. 90Theorem 19.3119.31 2228  19.31vv 43076
[Margaris] p. 90Theorem 19.3219.32 2227  r19.32 45741
[Margaris] p. 90Theorem 19.3319.33-2 43074  19.33 1888
[Margaris] p. 90Theorem 19.3419.34 1991
[Margaris] p. 90Theorem 19.3519.35 1881
[Margaris] p. 90Theorem 19.3619.36 2224  19.36vv 43075  r19.36zv 4505
[Margaris] p. 90Theorem 19.3719.37 2226  19.37vv 43077  r19.37zv 4500
[Margaris] p. 90Theorem 19.3819.38 1842
[Margaris] p. 90Theorem 19.3919.39 1989
[Margaris] p. 90Theorem 19.4019.40-2 1891  19.40 1890  r19.40 3120
[Margaris] p. 90Theorem 19.4119.41 2229  19.41rg 43244
[Margaris] p. 90Theorem 19.4219.42 2230
[Margaris] p. 90Theorem 19.4319.43 1886
[Margaris] p. 90Theorem 19.4419.44 2231  r19.44zv 4502
[Margaris] p. 90Theorem 19.4519.45 2232  r19.45zv 4501
[Margaris] p. 110Exercise 2(b)eu1 2607
[Mayet] p. 370Remarkjpi 31501  largei 31498  stri 31488
[Mayet3] p. 9Definition of CH-statesdf-hst 31443  ishst 31445
[Mayet3] p. 10Theoremhstrbi 31497  hstri 31496
[Mayet3] p. 1223Theorem 4.1mayete3i 30959
[Mayet3] p. 1240Theorem 7.1mayetes3i 30960
[MegPav2000] p. 2344Theorem 3.3stcltrthi 31509
[MegPav2000] p. 2345Definition 3.4-1chintcl 30563  chsupcl 30571
[MegPav2000] p. 2345Definition 3.4-2hatomic 31591
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 31585
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 31612
[MegPav2000] p. 2366Figure 7pl42N 38792
[MegPav2002] p. 362Lemma 2.2latj31 18436  latj32 18434  latjass 18432
[Megill] p. 444Axiom C5ax-5 1914  ax5ALT 37715
[Megill] p. 444Section 7conventions 29633
[Megill] p. 445Lemma L12aecom-o 37709  ax-c11n 37696  axc11n 2426
[Megill] p. 446Lemma L17equtrr 2026
[Megill] p. 446Lemma L18ax6fromc10 37704
[Megill] p. 446Lemma L19hbnae-o 37736  hbnae 2432
[Megill] p. 447Remark 9.1dfsb1 2481  sbid 2248  sbidd-misc 47666  sbidd 47665
[Megill] p. 448Remark 9.6axc14 2463
[Megill] p. 448Scheme C4'ax-c4 37692
[Megill] p. 448Scheme C5'ax-c5 37691  sp 2177
[Megill] p. 448Scheme C6'ax-11 2155
[Megill] p. 448Scheme C7'ax-c7 37693
[Megill] p. 448Scheme C8'ax-7 2012
[Megill] p. 448Scheme C9'ax-c9 37698
[Megill] p. 448Scheme C10'ax-6 1972  ax-c10 37694
[Megill] p. 448Scheme C11'ax-c11 37695
[Megill] p. 448Scheme C12'ax-8 2109
[Megill] p. 448Scheme C13'ax-9 2117
[Megill] p. 448Scheme C14'ax-c14 37699
[Megill] p. 448Scheme C15'ax-c15 37697
[Megill] p. 448Scheme C16'ax-c16 37700
[Megill] p. 448Theorem 9.4dral1-o 37712  dral1 2439  dral2-o 37738  dral2 2438  drex1 2441  drex2 2442  drsb1 2495  drsb2 2258
[Megill] p. 449Theorem 9.7sbcom2 2162  sbequ 2087  sbid2v 2509
[Megill] p. 450Example in Appendixhba1-o 37705  hba1 2290
[Mendelson] p. 35Axiom A3hirstL-ax3 45537
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3872  rspsbca 3873  stdpc4 2072
[Mendelson] p. 69Axiom 5ax-c4 37692  ra4 3879  stdpc5 2202
[Mendelson] p. 81Rule Cexlimiv 1934
[Mendelson] p. 95Axiom 6stdpc6 2032
[Mendelson] p. 95Axiom 7stdpc7 2243
[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 5824
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6264
[Mendelson] p. 244Proposition 4.8(g)epweon 7757
[Mendelson] p. 246Definition of successordf-suc 6367
[Mendelson] p. 250Exercise 4.36oelim2 8591
[Mendelson] p. 254Proposition 4.22(b)xpen 9136
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9051  xpsneng 9052
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9059  xpcomeng 9060
[Mendelson] p. 254Proposition 4.22(e)xpassen 9062
[Mendelson] p. 255Definitionbrsdom 8967
[Mendelson] p. 255Exercise 4.39endisj 9054
[Mendelson] p. 255Exercise 4.41mapprc 8820
[Mendelson] p. 255Exercise 4.43mapsnen 9033  mapsnend 9032
[Mendelson] p. 255Exercise 4.45mapunen 9142
[Mendelson] p. 255Exercise 4.47xpmapen 9141
[Mendelson] p. 255Exercise 4.42(a)map0e 8872
[Mendelson] p. 255Exercise 4.42(b)map1 9036
[Mendelson] p. 257Proposition 4.24(a)undom 9055
[Mendelson] p. 258Exercise 4.56(c)djuassen 10169  djucomen 10168
[Mendelson] p. 258Exercise 4.56(f)djudom1 10173
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10167
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8526
[Mendelson] p. 266Proposition 4.34(f)oaordex 8554
[Mendelson] p. 275Proposition 4.42(d)entri3 10550
[Mendelson] p. 281Definitiondf-r1 9755
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9804
[Mendelson] p. 287Axiom system MKru 3775
[MertziosUnger] p. 152Definitiondf-frgr 29492
[MertziosUnger] p. 153Remark 1frgrconngr 29527
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 29529  vdgn1frgrv3 29530
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 29531
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 29524
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 29517  2pthfrgrrn 29515  2pthfrgrrn2 29516
[Mittelstaedt] p. 9Definitiondf-oc 30483
[Monk1] p. 22Remarkconventions 29633
[Monk1] p. 22Theorem 3.1conventions 29633
[Monk1] p. 26Theorem 2.8(vii)ssin 4229
[Monk1] p. 33Theorem 3.2(i)ssrel 5780  ssrelf 31822
[Monk1] p. 33Theorem 3.2(ii)eqrel 5782
[Monk1] p. 34Definition 3.3df-opab 5210
[Monk1] p. 36Theorem 3.7(i)coi1 6258  coi2 6259
[Monk1] p. 36Theorem 3.8(v)dm0 5918  rn0 5923
[Monk1] p. 36Theorem 3.7(ii)cnvi 6138
[Monk1] p. 37Theorem 3.13(i)relxp 5693
[Monk1] p. 37Theorem 3.13(x)dmxp 5926  rnxp 6166
[Monk1] p. 37Theorem 3.13(ii)0xp 5772  xp0 6154
[Monk1] p. 38Theorem 3.16(ii)ima0 6073
[Monk1] p. 38Theorem 3.16(viii)imai 6070
[Monk1] p. 39Theorem 3.17imaex 7902  imaexALTV 37137  imaexg 7901
[Monk1] p. 39Theorem 3.16(xi)imassrn 6068
[Monk1] p. 41Theorem 4.3(i)fnopfv 7073  funfvop 7047
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6944
[Monk1] p. 42Theorem 4.4(iii)fvelima 6954
[Monk1] p. 43Theorem 4.6funun 6591
[Monk1] p. 43Theorem 4.8(iv)dff13 7249  dff13f 7250
[Monk1] p. 46Theorem 4.15(v)funex 7216  funrnex 7935
[Monk1] p. 50Definition 5.4fniunfv 7241
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6223
[Monk1] p. 52Theorem 5.11(viii)ssint 4967
[Monk1] p. 52Definition 5.13 (i)1stval2 7987  df-1st 7970
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7988  df-2nd 7971
[Monk1] p. 112Theorem 15.17(v)ranksn 9845  ranksnb 9818
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9846
[Monk1] p. 112Theorem 15.17(iii)rankun 9847  rankunb 9841
[Monk1] p. 113Theorem 15.18r1val3 9829
[Monk1] p. 113Definition 15.19df-r1 9755  r1val2 9828
[Monk1] p. 117Lemmazorn2 10497  zorn2g 10494
[Monk1] p. 133Theorem 18.11cardom 9977
[Monk1] p. 133Theorem 18.12canth3 10552
[Monk1] p. 133Theorem 18.14carduni 9972
[Monk2] p. 105Axiom C4ax-4 1812
[Monk2] p. 105Axiom C7ax-7 2012
[Monk2] p. 105Axiom C8ax-12 2172  ax-c15 37697  ax12v2 2174
[Monk2] p. 108Lemma 5ax-c4 37692
[Monk2] p. 109Lemma 12ax-11 2155
[Monk2] p. 109Lemma 15equvini 2455  equvinv 2033  eqvinop 5486
[Monk2] p. 113Axiom C5-1ax-5 1914  ax5ALT 37715
[Monk2] p. 113Axiom C5-2ax-10 2138
[Monk2] p. 113Axiom C5-3ax-11 2155
[Monk2] p. 114Lemma 21sp 2177
[Monk2] p. 114Lemma 22axc4 2315  hba1-o 37705  hba1 2290
[Monk2] p. 114Lemma 23nfia1 2151
[Monk2] p. 114Lemma 24nfa2 2171  nfra2 3373  nfra2w 3297
[Moore] p. 53Part Idf-mre 17526
[Munkres] p. 77Example 2distop 22480  indistop 22487  indistopon 22486
[Munkres] p. 77Example 3fctop 22489  fctop2 22490
[Munkres] p. 77Example 4cctop 22491
[Munkres] p. 78Definition of basisdf-bases 22431  isbasis3g 22434
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17385  tgval2 22441
[Munkres] p. 79Remarktgcl 22454
[Munkres] p. 80Lemma 2.1tgval3 22448
[Munkres] p. 80Lemma 2.2tgss2 22472  tgss3 22471
[Munkres] p. 81Lemma 2.3basgen 22473  basgen2 22474
[Munkres] p. 83Exercise 3topdifinf 36168  topdifinfeq 36169  topdifinffin 36167  topdifinfindis 36165
[Munkres] p. 89Definition of subspace topologyresttop 22646
[Munkres] p. 93Theorem 6.1(1)0cld 22524  topcld 22521
[Munkres] p. 93Theorem 6.1(2)iincld 22525
[Munkres] p. 93Theorem 6.1(3)uncld 22527
[Munkres] p. 94Definition of closureclsval 22523
[Munkres] p. 94Definition of interiorntrval 22522
[Munkres] p. 95Theorem 6.5(a)clsndisj 22561  elcls 22559
[Munkres] p. 95Theorem 6.5(b)elcls3 22569
[Munkres] p. 97Theorem 6.6clslp 22634  neindisj 22603
[Munkres] p. 97Corollary 6.7cldlp 22636
[Munkres] p. 97Definition of limit pointislp2 22631  lpval 22625
[Munkres] p. 98Definition of Hausdorff spacedf-haus 22801
[Munkres] p. 102Definition of continuous functiondf-cn 22713  iscn 22721  iscn2 22724
[Munkres] p. 107Theorem 7.2(g)cncnp 22766  cncnp2 22767  cncnpi 22764  df-cnp 22714  iscnp 22723  iscnp2 22725
[Munkres] p. 127Theorem 10.1metcn 24034
[Munkres] p. 128Theorem 10.3metcn4 24810
[Nathanson] p. 123Remarkreprgt 33571  reprinfz1 33572  reprlt 33569
[Nathanson] p. 123Definitiondf-repr 33559
[Nathanson] p. 123Chapter 5.1circlemethnat 33591
[Nathanson] p. 123Propositionbreprexp 33583  breprexpnat 33584  itgexpif 33556
[NielsenChuang] p. 195Equation 4.73unierri 31335
[OeSilva] p. 2042Section 2ax-bgbltosilva 46413
[Pfenning] p. 17Definition XMnatded 29636
[Pfenning] p. 17Definition NNCnatded 29636  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 29636
[Pfenning] p. 18Rule"natded 29636
[Pfenning] p. 18Definition /\Inatded 29636
[Pfenning] p. 18Definition ` `Enatded 29636  natded 29636  natded 29636  natded 29636  natded 29636
[Pfenning] p. 18Definition ` `Inatded 29636  natded 29636  natded 29636  natded 29636  natded 29636
[Pfenning] p. 18Definition ` `ELnatded 29636
[Pfenning] p. 18Definition ` `ERnatded 29636
[Pfenning] p. 18Definition ` `Ea,unatded 29636
[Pfenning] p. 18Definition ` `IRnatded 29636
[Pfenning] p. 18Definition ` `Ianatded 29636
[Pfenning] p. 127Definition =Enatded 29636
[Pfenning] p. 127Definition =Inatded 29636
[Ponnusamy] p. 361Theorem 6.44cphip0l 24701  df-dip 29932  dip0l 29949  ip0l 21173
[Ponnusamy] p. 361Equation 6.45cphipval 24742  ipval 29934
[Ponnusamy] p. 362Equation I1dipcj 29945  ipcj 21171
[Ponnusamy] p. 362Equation I3cphdir 24704  dipdir 30073  ipdir 21176  ipdiri 30061
[Ponnusamy] p. 362Equation I4ipidsq 29941  nmsq 24693
[Ponnusamy] p. 362Equation 6.46ip0i 30056
[Ponnusamy] p. 362Equation 6.47ip1i 30058
[Ponnusamy] p. 362Equation 6.48ip2i 30059
[Ponnusamy] p. 363Equation I2cphass 24710  dipass 30076  ipass 21182  ipassi 30072
[Prugovecki] p. 186Definition of brabraval 31175  df-bra 31081
[Prugovecki] p. 376Equation 8.1df-kb 31082  kbval 31185
[PtakPulmannova] p. 66Proposition 3.2.17atomli 31613
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 38697
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 31627  atcvat4i 31628  cvrat3 38251  cvrat4 38252  lsatcvat3 37860
[PtakPulmannova] p. 68Definition 3.2.18cvbr 31513  cvrval 38077  df-cv 31510  df-lcv 37827  lspsncv0 20747
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 38709
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 38710
[Quine] p. 16Definition 2.1df-clab 2711  rabid 3453  rabidd 43782
[Quine] p. 17Definition 2.1''dfsb7 2276
[Quine] p. 18Definition 2.7df-cleq 2725
[Quine] p. 19Definition 2.9conventions 29633  df-v 3477
[Quine] p. 34Theorem 5.1eqabb 2874
[Quine] p. 35Theorem 5.2abid1 2871  abid2f 2937
[Quine] p. 40Theorem 6.1sb5 2268
[Quine] p. 40Theorem 6.2sb6 2089  sbalex 2236
[Quine] p. 41Theorem 6.3df-clel 2811
[Quine] p. 41Theorem 6.4eqid 2733  eqid1 29700
[Quine] p. 41Theorem 6.5eqcom 2740
[Quine] p. 42Theorem 6.6df-sbc 3777
[Quine] p. 42Theorem 6.7dfsbcq 3778  dfsbcq2 3779
[Quine] p. 43Theorem 6.8vex 3479
[Quine] p. 43Theorem 6.9isset 3488
[Quine] p. 44Theorem 7.3spcgf 3581  spcgv 3586  spcimgf 3579
[Quine] p. 44Theorem 6.11spsbc 3789  spsbcd 3790
[Quine] p. 44Theorem 6.12elex 3493
[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 43620  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 6507
[Quine] p. 56Definition 8.18dfaiota2 45729  dfiota2 6493
[Quine] p. 57Theorem 8.19aiotaval 45738  iotaval 6511
[Quine] p. 57Theorem 8.22iotanul 6518
[Quine] p. 58Theorem 8.23iotaex 6513
[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 7436  oprabidw 7435
[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 6610
[Quine] p. 65Theorem 10.4funi 6577
[Quine] p. 65Theorem 10.5funsn 6598  funsng 6596
[Quine] p. 65Definition 10.1df-fun 6542
[Quine] p. 65Definition 10.2args 6088  dffv4 6885
[Quine] p. 68Definition 10.11conventions 29633  df-fv 6548  fv2 6883
[Quine] p. 124Theorem 17.3nn0opth2 14228  nn0opth2i 14227  nn0opthi 14226  omopthi 8656
[Quine] p. 177Definition 25.2df-rdg 8405
[Quine] p. 232Equation icarddom 10545
[Quine] p. 284Axiom 39(vi)funimaex 6633  funimaexg 6631
[Quine] p. 331Axiom system NFru 3775
[ReedSimon] p. 36Definition (iii)ax-his3 30315
[ReedSimon] p. 63Exercise 4(a)df-dip 29932  polid 30390  polid2i 30388  polidi 30389
[ReedSimon] p. 63Exercise 4(b)df-ph 30044
[ReedSimon] p. 195Remarklnophm 31250  lnophmi 31249
[Retherford] p. 49Exercise 1(i)leopadd 31363
[Retherford] p. 49Exercise 1(ii)leopmul 31365  leopmuli 31364
[Retherford] p. 49Exercise 1(iv)leoptr 31368
[Retherford] p. 49Definition VI.1df-leop 31083  leoppos 31357
[Retherford] p. 49Exercise 1(iii)leoptri 31367
[Retherford] p. 49Definition of operator orderingleop3 31356
[Roman] p. 4Definitiondf-dmat 21974  df-dmatalt 46981
[Roman] p. 18Part Preliminariesdf-rng 46584
[Roman] p. 19Part Preliminariesdf-ring 20049
[Roman] p. 46Theorem 1.6isldepslvec2 47068
[Roman] p. 112Noteisldepslvec2 47068  ldepsnlinc 47091  zlmodzxznm 47080
[Roman] p. 112Examplezlmodzxzequa 47079  zlmodzxzequap 47082  zlmodzxzldep 47087
[Roman] p. 170Theorem 7.8cayleyhamilton 22374
[Rosenlicht] p. 80Theoremheicant 36461
[Rosser] p. 281Definitiondf-op 4634
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 33595
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 33596
[Rotman] p. 28Remarkpgrpgt2nabl 46944  pmtr3ncom 19336
[Rotman] p. 31Theorem 3.4symggen2 19332
[Rotman] p. 42Theorem 3.15cayley 19275  cayleyth 19276
[Rudin] p. 164Equation 27efcan 16035
[Rudin] p. 164Equation 30efzval 16041
[Rudin] p. 167Equation 48absefi 16135
[Sanford] p. 39Remarkax-mp 5  mto 196
[Sanford] p. 39Rule 3mtpxor 1774
[Sanford] p. 39Rule 4mptxor 1772
[Sanford] p. 40Rule 1mptnan 1771
[Schechter] p. 51Definition of antisymmetryintasym 6113
[Schechter] p. 51Definition of irreflexivityintirr 6116
[Schechter] p. 51Definition of symmetrycnvsym 6110
[Schechter] p. 51Definition of transitivitycotr 6108
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17526
[Schechter] p. 79Definition of Moore closuredf-mrc 17527
[Schechter] p. 82Section 4.5df-mrc 17527
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17529
[Schechter] p. 139Definition AC3dfac9 10127
[Schechter] p. 141Definition (MC)dfac11 41737
[Schechter] p. 149Axiom DC1ax-dc 10437  axdc3 10445
[Schechter] p. 187Definition of "ring with unit"isring 20051  isrngo 36703
[Schechter] p. 276Remark 11.6.espan0 30773
[Schechter] p. 276Definition of spandf-span 30540  spanval 30564
[Schechter] p. 428Definition 15.35bastop1 22478
[Schloeder] p. 1Lemma 1.3onelon 6386  onelord 41933  ordelon 6385  ordelord 6383
[Schloeder] p. 1Lemma 1.7onepsuc 41934  sucidg 6442
[Schloeder] p. 1Remark 1.50elon 6415  onsuc 7794  ord0 6414  ordsuci 7791
[Schloeder] p. 1Theorem 1.9epsoon 41935
[Schloeder] p. 1Definition 1.1dftr5 5268
[Schloeder] p. 1Definition 1.2dford3 41700  elon2 6372
[Schloeder] p. 1Definition 1.4df-suc 6367
[Schloeder] p. 1Definition 1.6epel 5582  epelg 5580
[Schloeder] p. 1Theorem 1.9(i)elirr 9588  epirron 41936  ordirr 6379
[Schloeder] p. 1Theorem 1.9(ii)oneltr 41938  oneptr 41937  ontr1 6407
[Schloeder] p. 1Theorem 1.9(iii)oneltri 41940  oneptri 41939  ordtri3or 6393
[Schloeder] p. 2Lemma 1.10ondif1 8496  ord0eln0 6416
[Schloeder] p. 2Lemma 1.13elsuci 6428  onsucss 41949  trsucss 6449
[Schloeder] p. 2Lemma 1.14ordsucss 7801
[Schloeder] p. 2Lemma 1.15onnbtwn 6455  ordnbtwn 6454
[Schloeder] p. 2Lemma 1.16orddif0suc 41951  ordnexbtwnsuc 41950
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10392  onsucf1lem 41952  onsucf1o 41955  onsucf1olem 41953  onsucrn 41954
[Schloeder] p. 2Lemma 1.18dflim7 41956
[Schloeder] p. 2Remark 1.12ordzsl 7829
[Schloeder] p. 2Theorem 1.10ondif1i 41945  ordne0gt0 41944
[Schloeder] p. 2Definition 1.11dflim6 41947  limnsuc 41948  onsucelab 41946
[Schloeder] p. 3Remark 1.21omex 9634
[Schloeder] p. 3Theorem 1.19tfinds 7844
[Schloeder] p. 3Theorem 1.22omelon 9637  ordom 7860
[Schloeder] p. 3Definition 1.20dfom3 9638
[Schloeder] p. 4Lemma 2.21onn 8635
[Schloeder] p. 4Lemma 2.7ssonuni 7762  ssorduni 7761
[Schloeder] p. 4Remark 2.4oa1suc 8526
[Schloeder] p. 4Theorem 1.23dfom5 9641  limom 7866
[Schloeder] p. 4Definition 2.1df-1o 8461  df1o2 8468
[Schloeder] p. 4Definition 2.3oa0 8511  oa0suclim 41958  oalim 8527  oasuc 8519
[Schloeder] p. 4Definition 2.5om0 8512  om0suclim 41959  omlim 8528  omsuc 8521
[Schloeder] p. 4Definition 2.6oe0 8517  oe0m1 8516  oe0suclim 41960  oelim 8529  oesuc 8522
[Schloeder] p. 5Lemma 2.10onsupuni 41911
[Schloeder] p. 5Lemma 2.11onsupsucismax 41962
[Schloeder] p. 5Lemma 2.12onsssupeqcond 41963
[Schloeder] p. 5Lemma 2.13limexissup 41964  limexissupab 41966  limiun 41965  limuni 6422
[Schloeder] p. 5Lemma 2.14oa0r 8533
[Schloeder] p. 5Lemma 2.15om1 8538  om1om1r 41967  om1r 8539
[Schloeder] p. 5Remark 2.8oacl 8530  oaomoecl 41961  oecl 8532  omcl 8531
[Schloeder] p. 5Definition 2.9onsupintrab 41913
[Schloeder] p. 6Lemma 2.16oe1 8540
[Schloeder] p. 6Lemma 2.17oe1m 8541
[Schloeder] p. 6Lemma 2.18oe0rif 41968
[Schloeder] p. 6Theorem 2.19oasubex 41969
[Schloeder] p. 6Theorem 2.20nnacl 8607  nnamecl 41970  nnecl 8609  nnmcl 8608
[Schloeder] p. 7Lemma 3.1onsucwordi 41971
[Schloeder] p. 7Lemma 3.2oaword1 8548
[Schloeder] p. 7Lemma 3.3oaword2 8549
[Schloeder] p. 7Lemma 3.4oalimcl 8556
[Schloeder] p. 7Lemma 3.5oaltublim 41973
[Schloeder] p. 8Lemma 3.6oaordi3 41974
[Schloeder] p. 8Lemma 3.81oaomeqom 41976
[Schloeder] p. 8Lemma 3.10oa00 8555
[Schloeder] p. 8Lemma 3.11omge1 41980  omword1 8569
[Schloeder] p. 8Remark 3.9oaordnr 41979  oaordnrex 41978
[Schloeder] p. 8Theorem 3.7oaord3 41975
[Schloeder] p. 9Lemma 3.12omge2 41981  omword2 8570
[Schloeder] p. 9Lemma 3.13omlim2 41982
[Schloeder] p. 9Lemma 3.14omord2lim 41983
[Schloeder] p. 9Lemma 3.15omord2i 41984  omordi 8562
[Schloeder] p. 9Theorem 3.16omord 8564  omord2com 41985
[Schloeder] p. 10Lemma 3.172omomeqom 41986  df-2o 8462
[Schloeder] p. 10Lemma 3.19oege1 41989  oewordi 8587
[Schloeder] p. 10Lemma 3.20oege2 41990  oeworde 8589
[Schloeder] p. 10Lemma 3.21rp-oelim2 41991
[Schloeder] p. 10Lemma 3.22oeord2lim 41992
[Schloeder] p. 10Remark 3.18omnord1 41988  omnord1ex 41987
[Schloeder] p. 11Lemma 3.23oeord2i 41993
[Schloeder] p. 11Lemma 3.25nnoeomeqom 41995
[Schloeder] p. 11Remark 3.26oenord1 41999  oenord1ex 41998
[Schloeder] p. 11Theorem 4.1oaomoencom 42000
[Schloeder] p. 11Theorem 4.2oaass 8557
[Schloeder] p. 11Theorem 3.24oeord2com 41994
[Schloeder] p. 12Theorem 4.3odi 8575
[Schloeder] p. 13Theorem 4.4omass 8576
[Schloeder] p. 14Remark 4.6oenass 42002
[Schloeder] p. 14Theorem 4.7oeoa 8593
[Schloeder] p. 15Lemma 5.1cantnftermord 42003
[Schloeder] p. 15Lemma 5.2cantnfub 42004  cantnfub2 42005
[Schloeder] p. 16Theorem 5.3cantnf2 42008
[Schwabhauser] p. 10Axiom A1axcgrrflx 28152  axtgcgrrflx 27693
[Schwabhauser] p. 10Axiom A2axcgrtr 28153
[Schwabhauser] p. 10Axiom A3axcgrid 28154  axtgcgrid 27694
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 27679
[Schwabhauser] p. 11Axiom A4axsegcon 28165  axtgsegcon 27695  df-trkgcb 27681
[Schwabhauser] p. 11Axiom A5ax5seg 28176  axtg5seg 27696  df-trkgcb 27681
[Schwabhauser] p. 11Axiom A6axbtwnid 28177  axtgbtwnid 27697  df-trkgb 27680
[Schwabhauser] p. 12Axiom A7axpasch 28179  axtgpasch 27698  df-trkgb 27680
[Schwabhauser] p. 12Axiom A8axlowdim2 28198  df-trkg2d 33615
[Schwabhauser] p. 13Axiom A8axtglowdim2 27701
[Schwabhauser] p. 13Axiom A9axtgupdim2 27702  df-trkg2d 33615
[Schwabhauser] p. 13Axiom A10axeuclid 28201  axtgeucl 27703  df-trkge 27682
[Schwabhauser] p. 13Axiom A11axcont 28214  axtgcont 27700  axtgcont1 27699  df-trkgb 27680
[Schwabhauser] p. 27Theorem 2.1cgrrflx 34897
[Schwabhauser] p. 27Theorem 2.2cgrcomim 34899
[Schwabhauser] p. 27Theorem 2.3cgrtr 34902
[Schwabhauser] p. 27Theorem 2.4cgrcoml 34906
[Schwabhauser] p. 27Theorem 2.5cgrcomr 34907  tgcgrcomimp 27708  tgcgrcoml 27710  tgcgrcomr 27709
[Schwabhauser] p. 28Theorem 2.8cgrtriv 34912  tgcgrtriv 27715
[Schwabhauser] p. 28Theorem 2.105segofs 34916  tg5segofs 33623
[Schwabhauser] p. 28Definition 2.10df-afs 33620  df-ofs 34893
[Schwabhauser] p. 29Theorem 2.11cgrextend 34918  tgcgrextend 27716
[Schwabhauser] p. 29Theorem 2.12segconeq 34920  tgsegconeq 27717
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 34932  btwntriv2 34922  tgbtwntriv2 27718
[Schwabhauser] p. 30Theorem 3.2btwncomim 34923  tgbtwncom 27719
[Schwabhauser] p. 30Theorem 3.3btwntriv1 34926  tgbtwntriv1 27722
[Schwabhauser] p. 30Theorem 3.4btwnswapid 34927  tgbtwnswapid 27723
[Schwabhauser] p. 30Theorem 3.5btwnexch2 34933  btwnintr 34929  tgbtwnexch2 27727  tgbtwnintr 27724
[Schwabhauser] p. 30Theorem 3.6btwnexch 34935  btwnexch3 34930  tgbtwnexch 27729  tgbtwnexch3 27725
[Schwabhauser] p. 30Theorem 3.7btwnouttr 34934  tgbtwnouttr 27728  tgbtwnouttr2 27726
[Schwabhauser] p. 32Theorem 3.13axlowdim1 28197
[Schwabhauser] p. 32Theorem 3.14btwndiff 34937  tgbtwndiff 27737
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 27730  trisegint 34938
[Schwabhauser] p. 34Theorem 4.2ifscgr 34954  tgifscgr 27739
[Schwabhauser] p. 34Theorem 4.11colcom 27789  colrot1 27790  colrot2 27791  lncom 27853  lnrot1 27854  lnrot2 27855
[Schwabhauser] p. 34Definition 4.1df-ifs 34950
[Schwabhauser] p. 35Theorem 4.3cgrsub 34955  tgcgrsub 27740
[Schwabhauser] p. 35Theorem 4.5cgrxfr 34965  tgcgrxfr 27749
[Schwabhauser] p. 35Statement 4.4ercgrg 27748
[Schwabhauser] p. 35Definition 4.4df-cgr3 34951  df-cgrg 27742
[Schwabhauser] p. 35Definition instead (givendf-cgrg 27742
[Schwabhauser] p. 36Theorem 4.6btwnxfr 34966  tgbtwnxfr 27761
[Schwabhauser] p. 36Theorem 4.11colinearperm1 34972  colinearperm2 34974  colinearperm3 34973  colinearperm4 34975  colinearperm5 34976
[Schwabhauser] p. 36Definition 4.8df-ismt 27764
[Schwabhauser] p. 36Definition 4.10df-colinear 34949  tgellng 27784  tglng 27777
[Schwabhauser] p. 37Theorem 4.12colineartriv1 34977
[Schwabhauser] p. 37Theorem 4.13colinearxfr 34985  lnxfr 27797
[Schwabhauser] p. 37Theorem 4.14lineext 34986  lnext 27798
[Schwabhauser] p. 37Theorem 4.16fscgr 34990  tgfscgr 27799
[Schwabhauser] p. 37Theorem 4.17linecgr 34991  lncgr 27800
[Schwabhauser] p. 37Definition 4.15df-fs 34952
[Schwabhauser] p. 38Theorem 4.18lineid 34993  lnid 27801
[Schwabhauser] p. 38Theorem 4.19idinside 34994  tgidinside 27802
[Schwabhauser] p. 39Theorem 5.1btwnconn1 35011  tgbtwnconn1 27806
[Schwabhauser] p. 41Theorem 5.2btwnconn2 35012  tgbtwnconn2 27807
[Schwabhauser] p. 41Theorem 5.3btwnconn3 35013  tgbtwnconn3 27808
[Schwabhauser] p. 41Theorem 5.5brsegle2 35019
[Schwabhauser] p. 41Definition 5.4df-segle 35017  legov 27816
[Schwabhauser] p. 41Definition 5.5legov2 27817
[Schwabhauser] p. 42Remark 5.13legso 27830
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 35020
[Schwabhauser] p. 42Theorem 5.7seglerflx 35022
[Schwabhauser] p. 42Theorem 5.8segletr 35024
[Schwabhauser] p. 42Theorem 5.9segleantisym 35025
[Schwabhauser] p. 42Theorem 5.10seglelin 35026
[Schwabhauser] p. 42Theorem 5.11seglemin 35023
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 35028
[Schwabhauser] p. 42Proposition 5.7legid 27818
[Schwabhauser] p. 42Proposition 5.8legtrd 27820
[Schwabhauser] p. 42Proposition 5.9legtri3 27821
[Schwabhauser] p. 42Proposition 5.10legtrid 27822
[Schwabhauser] p. 42Proposition 5.11leg0 27823
[Schwabhauser] p. 43Theorem 6.2btwnoutside 35035
[Schwabhauser] p. 43Theorem 6.3broutsideof3 35036
[Schwabhauser] p. 43Theorem 6.4broutsideof 35031  df-outsideof 35030
[Schwabhauser] p. 43Definition 6.1broutsideof2 35032  ishlg 27833
[Schwabhauser] p. 44Theorem 6.4hlln 27838
[Schwabhauser] p. 44Theorem 6.5hlid 27840  outsideofrflx 35037
[Schwabhauser] p. 44Theorem 6.6hlcomb 27834  hlcomd 27835  outsideofcom 35038
[Schwabhauser] p. 44Theorem 6.7hltr 27841  outsideoftr 35039
[Schwabhauser] p. 44Theorem 6.11hlcgreu 27849  outsideofeu 35041
[Schwabhauser] p. 44Definition 6.8df-ray 35048
[Schwabhauser] p. 45Part 2df-lines2 35049
[Schwabhauser] p. 45Theorem 6.13outsidele 35042
[Schwabhauser] p. 45Theorem 6.15lineunray 35057
[Schwabhauser] p. 45Theorem 6.16lineelsb2 35058  tglineelsb2 27863
[Schwabhauser] p. 45Theorem 6.17linecom 35060  linerflx1 35059  linerflx2 35061  tglinecom 27866  tglinerflx1 27864  tglinerflx2 27865
[Schwabhauser] p. 45Theorem 6.18linethru 35063  tglinethru 27867
[Schwabhauser] p. 45Definition 6.14df-line2 35047  tglng 27777
[Schwabhauser] p. 45Proposition 6.13legbtwn 27825
[Schwabhauser] p. 46Theorem 6.19linethrueu 35066  tglinethrueu 27870
[Schwabhauser] p. 46Theorem 6.21lineintmo 35067  tglineineq 27874  tglineinteq 27876  tglineintmo 27873
[Schwabhauser] p. 46Theorem 6.23colline 27880
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 27881
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 27882
[Schwabhauser] p. 49Theorem 7.3mirinv 27897
[Schwabhauser] p. 49Theorem 7.7mirmir 27893
[Schwabhauser] p. 49Theorem 7.8mirreu3 27885
[Schwabhauser] p. 49Definition 7.5df-mir 27884  ismir 27890  mirbtwn 27889  mircgr 27888  mirfv 27887  mirval 27886
[Schwabhauser] p. 50Theorem 7.8mirreu 27895
[Schwabhauser] p. 50Theorem 7.9mireq 27896
[Schwabhauser] p. 50Theorem 7.10mirinv 27897
[Schwabhauser] p. 50Theorem 7.11mirf1o 27900
[Schwabhauser] p. 50Theorem 7.13miriso 27901
[Schwabhauser] p. 51Theorem 7.14mirmot 27906
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 27903  mirbtwni 27902
[Schwabhauser] p. 51Theorem 7.16mircgrs 27904
[Schwabhauser] p. 51Theorem 7.17miduniq 27916
[Schwabhauser] p. 52Lemma 7.21symquadlem 27920
[Schwabhauser] p. 52Theorem 7.18miduniq1 27917
[Schwabhauser] p. 52Theorem 7.19miduniq2 27918
[Schwabhauser] p. 52Theorem 7.20colmid 27919
[Schwabhauser] p. 53Lemma 7.22krippen 27922
[Schwabhauser] p. 55Lemma 7.25midexlem 27923
[Schwabhauser] p. 57Theorem 8.2ragcom 27929
[Schwabhauser] p. 57Definition 8.1df-rag 27925  israg 27928
[Schwabhauser] p. 58Theorem 8.3ragcol 27930
[Schwabhauser] p. 58Theorem 8.4ragmir 27931
[Schwabhauser] p. 58Theorem 8.5ragtrivb 27933
[Schwabhauser] p. 58Theorem 8.6ragflat2 27934
[Schwabhauser] p. 58Theorem 8.7ragflat 27935
[Schwabhauser] p. 58Theorem 8.8ragtriva 27936
[Schwabhauser] p. 58Theorem 8.9ragflat3 27937  ragncol 27940
[Schwabhauser] p. 58Theorem 8.10ragcgr 27938
[Schwabhauser] p. 59Theorem 8.12perpcom 27944
[Schwabhauser] p. 59Theorem 8.13ragperp 27948
[Schwabhauser] p. 59Theorem 8.14perpneq 27945
[Schwabhauser] p. 59Definition 8.11df-perpg 27927  isperp 27943
[Schwabhauser] p. 59Definition 8.13isperp2 27946
[Schwabhauser] p. 60Theorem 8.18foot 27953
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 27961  colperpexlem2 27962
[Schwabhauser] p. 63Theorem 8.21colperpex 27964  colperpexlem3 27963
[Schwabhauser] p. 64Theorem 8.22mideu 27969  midex 27968
[Schwabhauser] p. 66Lemma 8.24opphllem 27966
[Schwabhauser] p. 67Theorem 9.2oppcom 27975
[Schwabhauser] p. 67Definition 9.1islnopp 27970
[Schwabhauser] p. 68Lemma 9.3opphllem2 27979
[Schwabhauser] p. 68Lemma 9.4opphllem5 27982  opphllem6 27983
[Schwabhauser] p. 69Theorem 9.5opphl 27985
[Schwabhauser] p. 69Theorem 9.6axtgpasch 27698
[Schwabhauser] p. 70Theorem 9.6outpasch 27986
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 27994
[Schwabhauser] p. 71Definition 9.7df-hpg 27989  hpgbr 27991
[Schwabhauser] p. 72Lemma 9.10hpgerlem 27996
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 27995
[Schwabhauser] p. 72Theorem 9.11hpgid 27997
[Schwabhauser] p. 72Theorem 9.12hpgcom 27998
[Schwabhauser] p. 72Theorem 9.13hpgtr 27999
[Schwabhauser] p. 73Theorem 9.18colopp 28000
[Schwabhauser] p. 73Theorem 9.19colhp 28001
[Schwabhauser] p. 88Theorem 10.2lmieu 28015
[Schwabhauser] p. 88Definition 10.1df-mid 28005
[Schwabhauser] p. 89Theorem 10.4lmicom 28019
[Schwabhauser] p. 89Theorem 10.5lmilmi 28020
[Schwabhauser] p. 89Theorem 10.6lmireu 28021
[Schwabhauser] p. 89Theorem 10.7lmieq 28022
[Schwabhauser] p. 89Theorem 10.8lmiinv 28023
[Schwabhauser] p. 89Theorem 10.9lmif1o 28026
[Schwabhauser] p. 89Theorem 10.10lmiiso 28028
[Schwabhauser] p. 89Definition 10.3df-lmi 28006
[Schwabhauser] p. 90Theorem 10.11lmimot 28029
[Schwabhauser] p. 91Theorem 10.12hypcgr 28032
[Schwabhauser] p. 92Theorem 10.14lmiopp 28033
[Schwabhauser] p. 92Theorem 10.15lnperpex 28034
[Schwabhauser] p. 92Theorem 10.16trgcopy 28035  trgcopyeu 28037
[Schwabhauser] p. 95Definition 11.2dfcgra2 28061
[Schwabhauser] p. 95Definition 11.3iscgra 28040
[Schwabhauser] p. 95Proposition 11.4cgracgr 28049
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28047  cgrahl2 28048
[Schwabhauser] p. 96Theorem 11.6cgraid 28050
[Schwabhauser] p. 96Theorem 11.9cgraswap 28051
[Schwabhauser] p. 97Theorem 11.7cgracom 28053
[Schwabhauser] p. 97Theorem 11.8cgratr 28054
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28057  cgrahl 28058
[Schwabhauser] p. 98Theorem 11.13sacgr 28062
[Schwabhauser] p. 98Theorem 11.14oacgr 28063
[Schwabhauser] p. 98Theorem 11.15acopy 28064  acopyeu 28065
[Schwabhauser] p. 101Theorem 11.24inagswap 28072
[Schwabhauser] p. 101Theorem 11.25inaghl 28076
[Schwabhauser] p. 101Definition 11.23isinag 28069
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28084
[Schwabhauser] p. 102Definition 11.27df-leag 28077  isleag 28078
[Schwabhauser] p. 107Theorem 11.49tgsas 28086  tgsas1 28085  tgsas2 28087  tgsas3 28088
[Schwabhauser] p. 108Theorem 11.50tgasa 28090  tgasa1 28089
[Schwabhauser] p. 109Theorem 11.51tgsss1 28091  tgsss2 28092  tgsss3 28093
[Shapiro] p. 230Theorem 6.5.1dchrhash 26754  dchrsum 26752  dchrsum2 26751  sumdchr 26755
[Shapiro] p. 232Theorem 6.5.2dchr2sum 26756  sum2dchr 26757
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 19928  ablfacrp2 19929
[Shapiro], p. 328Equation 9.2.4vmasum 26699
[Shapiro], p. 329Equation 9.2.7logfac2 26700
[Shapiro], p. 329Equation 9.2.9logfacrlim 26707
[Shapiro], p. 331Equation 9.2.13vmadivsum 26965
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 26968
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27022  vmalogdivsum2 27021
[Shapiro], p. 375Theorem 9.4.1dirith 27012  dirith2 27011
[Shapiro], p. 375Equation 9.4.3rplogsum 27010  rpvmasum 27009  rpvmasum2 26995
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 26970
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27008
[Shapiro], p. 377Lemma 9.4.1dchrisum 26975  dchrisumlem1 26972  dchrisumlem2 26973  dchrisumlem3 26974  dchrisumlema 26971
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 26978
[Shapiro], p. 379Equation 9.4.16dchrmusum 27007  dchrmusumlem 27005  dchrvmasumlem 27006
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 26977
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 26979
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27003  dchrisum0re 26996  dchrisumn0 27004
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 26989
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 26993
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 26994
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27049  pntrsumbnd2 27050  pntrsumo1 27048
[Shapiro], p. 405Equation 10.2.1mudivsum 27013
[Shapiro], p. 406Equation 10.2.6mulogsum 27015
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27017
[Shapiro], p. 407Equation 10.2.8mulog2sum 27020
[Shapiro], p. 418Equation 10.4.6logsqvma 27025
[Shapiro], p. 418Equation 10.4.8logsqvma2 27026
[Shapiro], p. 419Equation 10.4.10selberg 27031
[Shapiro], p. 420Equation 10.4.12selberg2lem 27033
[Shapiro], p. 420Equation 10.4.14selberg2 27034
[Shapiro], p. 422Equation 10.6.7selberg3 27042
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27043
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27040  selberg3lem2 27041
[Shapiro], p. 422Equation 10.4.23selberg4 27044
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27038
[Shapiro], p. 428Equation 10.6.2selbergr 27051
[Shapiro], p. 429Equation 10.6.8selberg3r 27052
[Shapiro], p. 430Equation 10.6.11selberg4r 27053
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27067
[Shapiro], p. 434Equation 10.6.27pntlema 27079  pntlemb 27080  pntlemc 27078  pntlemd 27077  pntlemg 27081
[Shapiro], p. 435Equation 10.6.29pntlema 27079
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27071
[Shapiro], p. 436Lemma 10.6.2pntibnd 27076
[Shapiro], p. 436Equation 10.6.34pntlema 27079
[Shapiro], p. 436Equation 10.6.35pntlem3 27092  pntleml 27094
[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 403
[Stoll] p. 262Example 4.1dfsymdif3 4295
[Strang] p. 242Section 6.3expgrowth 43027
[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 43529
[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 43611
[Suppes] p. 47Theorem 87pwid 4623
[Suppes] p. 47Theorem 89pw0 4814
[Suppes] p. 48Theorem 90pwpw0 4815
[Suppes] p. 52Theorem 101xpss12 5690
[Suppes] p. 52Theorem 102xpindi 5831  xpindir 5832
[Suppes] p. 52Theorem 103xpundi 5742  xpundir 5743
[Suppes] p. 54Theorem 105elirrv 9587
[Suppes] p. 58Theorem 2relss 5779
[Suppes] p. 59Theorem 4eldm 5898  eldm2 5899  eldm2g 5897  eldmg 5896
[Suppes] p. 59Definition 3df-dm 5685
[Suppes] p. 60Theorem 6dmin 5909
[Suppes] p. 60Theorem 8rnun 6142
[Suppes] p. 60Theorem 9rnin 6143
[Suppes] p. 60Definition 4dfrn2 5886
[Suppes] p. 61Theorem 11brcnv 5880  brcnvg 5877
[Suppes] p. 62Equation 5elcnv 5874  elcnv2 5875
[Suppes] p. 62Theorem 12relcnv 6100
[Suppes] p. 62Theorem 15cnvin 6141
[Suppes] p. 62Theorem 16cnvun 6139
[Suppes] p. 63Definitiondftrrels2 37383
[Suppes] p. 63Theorem 20co02 6256
[Suppes] p. 63Theorem 21dmcoss 5968
[Suppes] p. 63Definition 7df-co 5684
[Suppes] p. 64Theorem 26cnvco 5883
[Suppes] p. 64Theorem 27coass 6261
[Suppes] p. 65Theorem 31resundi 5993
[Suppes] p. 65Theorem 34elima 6062  elima2 6063  elima3 6064  elimag 6061
[Suppes] p. 65Theorem 35imaundi 6146
[Suppes] p. 66Theorem 40dminss 6149
[Suppes] p. 66Theorem 41imainss 6150
[Suppes] p. 67Exercise 11cnvxp 6153
[Suppes] p. 81Definition 34dfec2 8702
[Suppes] p. 82Theorem 72elec 8743  elecALTV 37072  elecg 8742
[Suppes] p. 82Theorem 73eqvrelth 37419  erth 8748  erth2 8749
[Suppes] p. 83Theorem 74eqvreldisj 37422  erdisj 8751
[Suppes] p. 83Definition 35, df-parts 37573  dfmembpart2 37578
[Suppes] p. 89Theorem 96map0b 8873
[Suppes] p. 89Theorem 97map0 8877  map0g 8874
[Suppes] p. 89Theorem 98mapsn 8878  mapsnd 8876
[Suppes] p. 89Theorem 99mapss 8879
[Suppes] p. 91Definition 12(ii)alephsuc 10059
[Suppes] p. 91Definition 12(iii)alephlim 10058
[Suppes] p. 92Theorem 1enref 8977  enrefg 8976
[Suppes] p. 92Theorem 2ensym 8995  ensymb 8994  ensymi 8996
[Suppes] p. 92Theorem 3entr 8998
[Suppes] p. 92Theorem 4unen 9042
[Suppes] p. 94Theorem 15endom 8971
[Suppes] p. 94Theorem 16ssdomg 8992
[Suppes] p. 94Theorem 17domtr 8999
[Suppes] p. 95Theorem 18sbth 9089
[Suppes] p. 97Theorem 23canth2 9126  canth2g 9127
[Suppes] p. 97Definition 3brsdom2 9093  df-sdom 8938  dfsdom2 9092
[Suppes] p. 97Theorem 21(i)sdomirr 9110
[Suppes] p. 97Theorem 22(i)domnsym 9095
[Suppes] p. 97Theorem 21(ii)sdomnsym 9094
[Suppes] p. 97Theorem 22(ii)domsdomtr 9108
[Suppes] p. 97Theorem 22(iv)brdom2 8974
[Suppes] p. 97Theorem 21(iii)sdomtr 9111
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9106
[Suppes] p. 98Exercise 4fundmen 9027  fundmeng 9028
[Suppes] p. 98Exercise 6xpdom3 9066
[Suppes] p. 98Exercise 11sdomentr 9107
[Suppes] p. 104Theorem 37fofi 9334
[Suppes] p. 104Theorem 38pwfi 9174
[Suppes] p. 105Theorem 40pwfi 9174
[Suppes] p. 111Axiom for cardinal numberscarden 10542
[Suppes] p. 130Definition 3df-tr 5265
[Suppes] p. 132Theorem 9ssonuni 7762
[Suppes] p. 134Definition 6df-suc 6367
[Suppes] p. 136Theorem Schema 22findes 7888  finds 7884  finds1 7887  finds2 7886
[Suppes] p. 151Theorem 42isfinite 9643  isfinite2 9297  isfiniteg 9300  unbnn 9295
[Suppes] p. 162Definition 5df-ltnq 10909  df-ltpq 10901
[Suppes] p. 197Theorem Schema 4tfindes 7847  tfinds 7844  tfinds2 7848
[Suppes] p. 209Theorem 18oaord1 8547
[Suppes] p. 209Theorem 21oaword2 8549
[Suppes] p. 211Theorem 25oaass 8557
[Suppes] p. 225Definition 8iscard2 9967
[Suppes] p. 227Theorem 56ondomon 10554
[Suppes] p. 228Theorem 59harcard 9969
[Suppes] p. 228Definition 12(i)aleph0 10057
[Suppes] p. 228Theorem Schema 61onintss 6412
[Suppes] p. 228Theorem Schema 62onminesb 7776  onminsb 7777
[Suppes] p. 229Theorem 64alephval2 10563
[Suppes] p. 229Theorem 65alephcard 10061
[Suppes] p. 229Theorem 66alephord2i 10068
[Suppes] p. 229Theorem 67alephnbtwn 10062
[Suppes] p. 229Definition 12df-aleph 9931
[Suppes] p. 242Theorem 6weth 10486
[Suppes] p. 242Theorem 8entric 10548
[Suppes] p. 242Theorem 9carden 10542
[TakeutiZaring] p. 8Axiom 1ax-ext 2704
[TakeutiZaring] p. 13Definition 4.5df-cleq 2725
[TakeutiZaring] p. 13Proposition 4.6df-clel 2811
[TakeutiZaring] p. 13Proposition 4.9cvjust 2727
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2756
[TakeutiZaring] p. 14Definition 4.16df-oprab 7408
[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 7726
[TakeutiZaring] p. 16Exercise 6opth 5475
[TakeutiZaring] p. 16Exercise 7opex 5463
[TakeutiZaring] p. 16Exercise 8rext 5447
[TakeutiZaring] p. 16Corollary 5.8unex 7728  unexg 7731
[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 6431  elsucg 6429  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 43612  sspwimpALT 43619  sspwimpALT2 43622  sspwimpcf 43614
[TakeutiZaring] p. 18Exercise 19pweqb 5455
[TakeutiZaring] p. 19Axiom 5ax-rep 5284
[TakeutiZaring] p. 20Definitiondf-rab 3434
[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 9586
[TakeutiZaring] p. 21Axiom 6'zfregs 9723
[TakeutiZaring] p. 21Theorem 5.22setind 9725
[TakeutiZaring] p. 21Definition 5.20df-v 3477
[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 9593
[TakeutiZaring] p. 22Exercise 6elirr 9588
[TakeutiZaring] p. 22Exercise 7ssdif0 4362
[TakeutiZaring] p. 22Exercise 11difdif 4129
[TakeutiZaring] p. 22Exercise 13undif3 4289  undif3VD 43576
[TakeutiZaring] p. 22Exercise 14difss 4130
[TakeutiZaring] p. 22Exercise 15sscon 4137
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3063
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3072
[TakeutiZaring] p. 23Proposition 6.2xpex 7735  xpexg 7732
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5682
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6616
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6794  fun11 6619
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6556  svrelfun 6617
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5885
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5887
[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 6190  dfrel2 6185
[TakeutiZaring] p. 25Exercise 3xpss 5691
[TakeutiZaring] p. 25Exercise 5relun 5809
[TakeutiZaring] p. 25Exercise 6reluni 5816
[TakeutiZaring] p. 25Exercise 9inxp 5830
[TakeutiZaring] p. 25Exercise 12relres 6008
[TakeutiZaring] p. 25Exercise 13opelres 5985  opelresi 5987
[TakeutiZaring] p. 25Exercise 14dmres 6001
[TakeutiZaring] p. 25Exercise 15resss 6004
[TakeutiZaring] p. 25Exercise 17resabs1 6009
[TakeutiZaring] p. 25Exercise 18funres 6587
[TakeutiZaring] p. 25Exercise 24relco 6104
[TakeutiZaring] p. 25Exercise 29funco 6585
[TakeutiZaring] p. 25Exercise 30f1co 6796
[TakeutiZaring] p. 26Definition 6.10eu2 2606
[TakeutiZaring] p. 26Definition 6.11conventions 29633  df-fv 6548  fv3 6906
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7911  cnvexg 7910
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7897  dmexg 7889
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7898  rnexg 7890
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 43146
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7906
[TakeutiZaring] p. 27Corollary 6.13fvex 6901
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 45817  tz6.12-1-afv2 45884  tz6.12-1 6911  tz6.12-afv 45816  tz6.12-afv2 45883  tz6.12 6913  tz6.12c-afv2 45885  tz6.12c 6910
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 45880  tz6.12-2 6876  tz6.12i-afv2 45886  tz6.12i 6916
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6543
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6544
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6546  wfo 6538
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6545  wf1 6537
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6547  wf1o 6539
[TakeutiZaring] p. 28Exercise 4eqfnfv 7028  eqfnfv2 7029  eqfnfv2f 7032
[TakeutiZaring] p. 28Exercise 5fvco 6985
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7214
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7212
[TakeutiZaring] p. 29Exercise 9funimaex 6633  funimaexg 6631
[TakeutiZaring] p. 29Definition 6.18df-br 5148
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5588
[TakeutiZaring] p. 30Definition 6.21dffr2 5639  dffr3 6095  eliniseg 6090  iniseg 6093
[TakeutiZaring] p. 30Definition 6.22df-eprel 5579
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5653  fr3nr 7754  frirr 5652
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5630
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7756
[TakeutiZaring] p. 31Exercise 1frss 5642
[TakeutiZaring] p. 31Exercise 4wess 5662
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6345  tz6.26i 6347  wefrc 5669  wereu2 5672
[TakeutiZaring] p. 32Theorem 6.27wfi 6348  wfii 6350
[TakeutiZaring] p. 32Definition 6.28df-isom 6549
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7321
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7322
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7328
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7329
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7330
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7334
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7341
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7343
[TakeutiZaring] p. 35Notationwtr 5264
[TakeutiZaring] p. 35Theorem 7.2trelpss 43147  tz7.2 5659
[TakeutiZaring] p. 35Definition 7.1dftr3 5270
[TakeutiZaring] p. 36Proposition 7.4ordwe 6374
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6382
[TakeutiZaring] p. 36Proposition 7.6ordelord 6383  ordelordALT 43231  ordelordALTVD 43561
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6389  ordelssne 6388
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6387
[TakeutiZaring] p. 37Proposition 7.9ordin 6391
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7764
[TakeutiZaring] p. 38Corollary 7.15ordsson 7765
[TakeutiZaring] p. 38Definition 7.11df-on 6365
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6393
[TakeutiZaring] p. 38Proposition 7.12onfrALT 43243  ordon 7759
[TakeutiZaring] p. 38Proposition 7.13onprc 7760
[TakeutiZaring] p. 39Theorem 7.17tfi 7837
[TakeutiZaring] p. 40Exercise 3ontr2 6408
[TakeutiZaring] p. 40Exercise 7dftr2 5266
[TakeutiZaring] p. 40Exercise 9onssmin 7775
[TakeutiZaring] p. 40Exercise 11unon 7814
[TakeutiZaring] p. 40Exercise 12ordun 6465
[TakeutiZaring] p. 40Exercise 14ordequn 6464
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7761
[TakeutiZaring] p. 40Proposition 7.20elssuni 4940
[TakeutiZaring] p. 41Definition 7.22df-suc 6367
[TakeutiZaring] p. 41Proposition 7.23sssucid 6441  sucidg 6442
[TakeutiZaring] p. 41Proposition 7.24onsuc 7794
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6455  ordnbtwn 6454
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7811
[TakeutiZaring] p. 42Exercise 1df-lim 6366
[TakeutiZaring] p. 42Exercise 4omssnlim 7865
[TakeutiZaring] p. 42Exercise 7ssnlim 7870
[TakeutiZaring] p. 42Exercise 8onsucssi 7825  ordelsuc 7803
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7805
[TakeutiZaring] p. 42Definition 7.27nlimon 7835
[TakeutiZaring] p. 42Definition 7.28dfom2 7852
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7874
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7876
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7877
[TakeutiZaring] p. 43Remarkomon 7862
[TakeutiZaring] p. 43Axiom 7inf3 9626  omex 9634
[TakeutiZaring] p. 43Theorem 7.32ordom 7860
[TakeutiZaring] p. 43Corollary 7.31find 7882
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7878
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7879
[TakeutiZaring] p. 44Exercise 1limomss 7855
[TakeutiZaring] p. 44Exercise 2int0 4965
[TakeutiZaring] p. 44Exercise 3trintss 5283
[TakeutiZaring] p. 44Exercise 4intss1 4966
[TakeutiZaring] p. 44Exercise 5intex 5336
[TakeutiZaring] p. 44Exercise 6oninton 7778
[TakeutiZaring] p. 44Exercise 11ordintdif 6411
[TakeutiZaring] p. 44Definition 7.35df-int 4950
[TakeutiZaring] p. 44Proposition 7.34noinfep 9651
[TakeutiZaring] p. 45Exercise 4onint 7773
[TakeutiZaring] p. 47Lemma 1tfrlem1 8371
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8392
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8393
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8394
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8401  tz7.44-2 8402  tz7.44-3 8403
[TakeutiZaring] p. 50Exercise 1smogt 8362
[TakeutiZaring] p. 50Exercise 3smoiso 8357
[TakeutiZaring] p. 50Definition 7.46df-smo 8341
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8440  tz7.49c 8441
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8438
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8437
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8439
[TakeutiZaring] p. 53Proposition 7.532eu5 2652
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 10002
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 10003
[TakeutiZaring] p. 56Definition 8.1oalim 8527  oasuc 8519
[TakeutiZaring] p. 57Remarktfindsg 7845
[TakeutiZaring] p. 57Proposition 8.2oacl 8530
[TakeutiZaring] p. 57Proposition 8.3oa0 8511  oa0r 8533
[TakeutiZaring] p. 57Proposition 8.16omcl 8531
[TakeutiZaring] p. 58Corollary 8.5oacan 8544
[TakeutiZaring] p. 58Proposition 8.4nnaord 8615  nnaordi 8614  oaord 8543  oaordi 8542
[TakeutiZaring] p. 59Proposition 8.6iunss2 5051  uniss2 4944
[TakeutiZaring] p. 59Proposition 8.7oawordri 8546
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8551  oawordex 8553
[TakeutiZaring] p. 59Proposition 8.9nnacl 8607
[TakeutiZaring] p. 59Proposition 8.10oaabs 8643
[TakeutiZaring] p. 60Remarkoancom 9642
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8556
[TakeutiZaring] p. 62Exercise 1nnarcl 8612
[TakeutiZaring] p. 62Exercise 5oaword1 8548
[TakeutiZaring] p. 62Definition 8.15om0x 8514  omlim 8528  omsuc 8521
[TakeutiZaring] p. 62Definition 8.15(a)om0 8512
[TakeutiZaring] p. 63Proposition 8.17nnecl 8609  nnmcl 8608
[TakeutiZaring] p. 63Proposition 8.19nnmord 8628  nnmordi 8627  omord 8564  omordi 8562
[TakeutiZaring] p. 63Proposition 8.20omcan 8565
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8632  omwordri 8568
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8534
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8538  om1r 8539
[TakeutiZaring] p. 64Proposition 8.22om00 8571
[TakeutiZaring] p. 64Proposition 8.23omordlim 8573
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8574
[TakeutiZaring] p. 64Proposition 8.25odi 8575
[TakeutiZaring] p. 65Theorem 8.26omass 8576
[TakeutiZaring] p. 67Definition 8.30nnesuc 8604  oe0 8517  oelim 8529  oesuc 8522  onesuc 8525
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8515
[TakeutiZaring] p. 67Proposition 8.32oen0 8582
[TakeutiZaring] p. 67Proposition 8.33oeordi 8583
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8516
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8541
[TakeutiZaring] p. 68Corollary 8.34oeord 8584
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8590
[TakeutiZaring] p. 68Proposition 8.35oewordri 8588
[TakeutiZaring] p. 68Proposition 8.37oeworde 8589
[TakeutiZaring] p. 69Proposition 8.41oeoa 8593
[TakeutiZaring] p. 70Proposition 8.42oeoe 8595
[TakeutiZaring] p. 73Theorem 9.1trcl 9719  tz9.1 9720
[TakeutiZaring] p. 76Definition 9.9df-r1 9755  r10 9759  r1lim 9763  r1limg 9762  r1suc 9761  r1sucg 9760
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9771  r1ord2 9772  r1ordg 9769
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9781
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9806  tz9.13 9782  tz9.13g 9783
[TakeutiZaring] p. 79Definition 9.14df-rank 9756  rankval 9807  rankvalb 9788  rankvalg 9808
[TakeutiZaring] p. 79Proposition 9.16rankel 9830  rankelb 9815
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9844  rankval3 9831  rankval3b 9817
[TakeutiZaring] p. 79Proposition 9.18rankonid 9820
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9786
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9825  rankr1c 9812  rankr1g 9823
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9826
[TakeutiZaring] p. 80Exercise 1rankss 9840  rankssb 9839
[TakeutiZaring] p. 80Exercise 2unbndrank 9833
[TakeutiZaring] p. 80Proposition 9.19bndrank 9832
[TakeutiZaring] p. 83Axiom of Choiceac4 10466  dfac3 10112
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10021  numth 10463  numth2 10462
[TakeutiZaring] p. 85Definition 10.4cardval 10537
[TakeutiZaring] p. 85Proposition 10.5cardid 10538  cardid2 9944
[TakeutiZaring] p. 85Proposition 10.9oncard 9951
[TakeutiZaring] p. 85Proposition 10.10carden 10542
[TakeutiZaring] p. 85Proposition 10.11cardidm 9950
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9935
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9956
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9948
[TakeutiZaring] p. 87Proposition 10.15pwen 9146
[TakeutiZaring] p. 88Exercise 1en0 9009
[TakeutiZaring] p. 88Exercise 7infensuc 9151
[TakeutiZaring] p. 89Exercise 10omxpen 9070
[TakeutiZaring] p. 90Corollary 10.23cardnn 9954
[TakeutiZaring] p. 90Definition 10.27alephiso 10089
[TakeutiZaring] p. 90Proposition 10.20nneneq 9205
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9224
[TakeutiZaring] p. 90Proposition 10.26alephprc 10090
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9210
[TakeutiZaring] p. 91Exercise 2alephle 10079
[TakeutiZaring] p. 91Exercise 3aleph0 10057
[TakeutiZaring] p. 91Exercise 4cardlim 9963
[TakeutiZaring] p. 91Exercise 7infpss 10208
[TakeutiZaring] p. 91Exercise 8infcntss 9317
[TakeutiZaring] p. 91Definition 10.29df-fin 8939  isfi 8968
[TakeutiZaring] p. 92Proposition 10.32onfin 9226
[TakeutiZaring] p. 92Proposition 10.34imadomg 10525
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9063
[TakeutiZaring] p. 93Proposition 10.35fodomb 10517
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10176  unxpdom 9249
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9965  cardsdomelir 9964
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9251
[TakeutiZaring] p. 94Proposition 10.39infxpen 10005
[TakeutiZaring] p. 95Definition 10.42df-map 8818
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10553  infxpidm2 10008
[TakeutiZaring] p. 95Proposition 10.41infdju 10199  infxp 10206
[TakeutiZaring] p. 96Proposition 10.44pw2en 9075  pw2f1o 9073
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9139
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10478
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10473  ac6s5 10482
[TakeutiZaring] p. 98Theorem 10.47unidom 10534
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10535  uniimadomf 10536
[TakeutiZaring] p. 100Definition 11.1cfcof 10265
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10260
[TakeutiZaring] p. 102Exercise 1cfle 10245
[TakeutiZaring] p. 102Exercise 2cf0 10242
[TakeutiZaring] p. 102Exercise 3cfsuc 10248
[TakeutiZaring] p. 102Exercise 4cfom 10255
[TakeutiZaring] p. 102Proposition 11.9coftr 10264
[TakeutiZaring] p. 103Theorem 11.15alephreg 10573
[TakeutiZaring] p. 103Proposition 11.11cardcf 10243
[TakeutiZaring] p. 103Proposition 11.13alephsing 10267
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10088
[TakeutiZaring] p. 104Proposition 11.16carduniima 10087
[TakeutiZaring] p. 104Proposition 11.18alephfp 10099  alephfp2 10100
[TakeutiZaring] p. 106Theorem 11.20gchina 10690
[TakeutiZaring] p. 106Theorem 11.21mappwen 10103
[TakeutiZaring] p. 107Theorem 11.26konigth 10560
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10574
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10575
[Tarski] p. 67Axiom B5ax-c5 37691
[Tarski] p. 67Scheme B5sp 2177
[Tarski] p. 68Lemma 6avril1 29696  equid 2016
[Tarski] p. 69Lemma 7equcomi 2021
[Tarski] p. 70Lemma 14spim 2387  spime 2389  spimew 1976
[Tarski] p. 70Lemma 16ax-12 2172  ax-c15 37697  ax12i 1971
[Tarski] p. 70Lemmas 16 and 17sb6 2089
[Tarski] p. 75Axiom B7ax6v 1973
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1914  ax5ALT 37715
[Tarski], p. 75Scheme B8 of system S2ax-7 2012  ax-8 2109  ax-9 2117
[Tarski1999] p. 178Axiom 4axtgsegcon 27695
[Tarski1999] p. 178Axiom 5axtg5seg 27696
[Tarski1999] p. 179Axiom 7axtgpasch 27698
[Tarski1999] p. 180Axiom 7.1axtgpasch 27698
[Tarski1999] p. 185Axiom 11axtgcont1 27699
[Truss] p. 114Theorem 5.18ruc 16182
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 36465
[Viaclovsky8] p. 3Proposition 7ismblfin 36467
[Weierstrass] p. 272Definitiondf-mdet 22069  mdetuni 22106
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 903
[WhiteheadRussell] p. 96Axiom *1.3olc 867
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 868
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 919
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 967
[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 36264
[WhiteheadRussell] p. 100Theorem *2.05frege5 42484  imim2 58  wl-luk-imim2 36259
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 45664  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 896
[WhiteheadRussell] p. 101Theorem *2.06barbara 2659  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 902
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 36262
[WhiteheadRussell] p. 101Theorem *2.11exmid 894
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 897
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 43621  wl-luk-notnotr 36263
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 42514  axfrege28 42513  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 866
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 924
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 36256
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 889
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 939
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 29634  pm2.27 42  wl-luk-pm2.27 36254
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 922
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 37170
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 923
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 969
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 970
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 968
[WhiteheadRussell] p. 105Definition *2.33df-3or 1089
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 906
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 907
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 942
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 881
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 882
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 190
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 883
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 884
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 885
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 850
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 851
[WhiteheadRussell] p. 107Theorem *2.55orel1 888
[WhiteheadRussell] p. 107Theorem *2.56orel2 890
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 191
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 899
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 940
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 941
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 192
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 891  pm2.67 892
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 898
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 972
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 900
[WhiteheadRussell] p. 108Theorem *2.69looinv 202
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 973
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 974
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 933
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 931
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 971
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 975
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 932
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 991
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 471  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 992
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 993
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 994
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 995
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 473
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 461
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 404
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 802
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 450
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 451
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 484  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 486  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 764
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 765
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 807
[WhiteheadRussell] p. 113Fact)pm3.45 623
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 809
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 494
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 495
[WhiteheadRussell] p. 113Theorem *3.44jao 960  pm3.44 959
[WhiteheadRussell] p. 113Theorem *3.47anim12 808
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 475
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 963
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 261
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 354
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 806
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 832
[WhiteheadRussell] p. 117Theorem *4.21bicom 221
[WhiteheadRussell] p. 117Theorem *4.22biantr 805  bitr 804
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 565
[WhiteheadRussell] p. 117Theorem *4.25oridm 904  pm4.25 905
[WhiteheadRussell] p. 118Theorem *4.3ancom 462
[WhiteheadRussell] p. 118Theorem *4.4andi 1007
[WhiteheadRussell] p. 118Theorem *4.31orcom 869
[WhiteheadRussell] p. 118Theorem *4.32anass 470
[WhiteheadRussell] p. 118Theorem *4.33orass 921
[WhiteheadRussell] p. 118Theorem *4.36anbi1 633
[WhiteheadRussell] p. 118Theorem *4.37orbi1 917
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 637
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 976
[WhiteheadRussell] p. 118Definition *4.34df-3an 1090
[WhiteheadRussell] p. 119Theorem *4.41ordi 1005
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1053
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1022
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 996
[WhiteheadRussell] p. 119Theorem *4.45orabs 998  pm4.45 997  pm4.45im 827
[WhiteheadRussell] p. 120Theorem *4.5anor 982
[WhiteheadRussell] p. 120Theorem *4.6imor 852
[WhiteheadRussell] p. 120Theorem *4.7anclb 547
[WhiteheadRussell] p. 120Theorem *4.51ianor 981
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 984
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 985
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 986
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 987
[WhiteheadRussell] p. 120Theorem *4.56ioran 983  pm4.56 988
[WhiteheadRussell] p. 120Theorem *4.57oran 989  pm4.57 990
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 406
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 855
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 399
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 848
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 407
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 849
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 400
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 559  pm4.71d 563  pm4.71i 561  pm4.71r 560  pm4.71rd 564  pm4.71ri 562
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 949
[WhiteheadRussell] p. 121Theorem *4.73iba 529
[WhiteheadRussell] p. 121Theorem *4.74biorf 936
[WhiteheadRussell] p. 121Theorem *4.76jcab 519  pm4.76 520
[WhiteheadRussell] p. 121Theorem *4.77jaob 961  pm4.77 962
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 934
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1003
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 394
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 395
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1023
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1024
[WhiteheadRussell] p. 122Theorem *4.84imbi1 348
[WhiteheadRussell] p. 122Theorem *4.85imbi2 349
[WhiteheadRussell] p. 122Theorem *4.86bibi1 352
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 389  impexp 452  pm4.87 842
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 823
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 944  pm5.11g 943
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 945
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 947
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 946
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1012
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1013
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1011
[WhiteheadRussell] p. 124Theorem *5.18nbbn 385  pm5.18 383
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 388
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 824
[WhiteheadRussell] p. 124Theorem *5.22xor 1014
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1049
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1050
[WhiteheadRussell] p. 124Theorem *5.25dfor2 901
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 574
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 390
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 362
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1001
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 953
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 830
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 575
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 835
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 825
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 833
[WhiteheadRussell] p. 125Theorem *5.41imdi 391  pm5.41 392
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 545
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 544
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1004
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1017
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 948
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1000
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1018
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1019
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1027
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 367
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1028
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 43050
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 43051
[WhiteheadRussell] p. 147Theorem *10.2219.26 1874
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 43052
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 43053
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 43054
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1897
[WhiteheadRussell] p. 151Theorem *10.301albitr 43055
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 43056
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 43057
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 43058
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 43059
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 43061
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 43062
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 43063
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 43060
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2094
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 43066
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 43067
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2074
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2158
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1832
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1833
[WhiteheadRussell] p. 161Theorem *11.319.21vv 43068
[WhiteheadRussell] p. 162Theorem *11.322alim 43069
[WhiteheadRussell] p. 162Theorem *11.332albi 43070
[WhiteheadRussell] p. 162Theorem *11.342exim 43071
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 43073
[WhiteheadRussell] p. 162Theorem *11.3412exbi 43072
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1891
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 43075
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 43076
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 43074
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1831
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 43077
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 43078
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1849
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 43079
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2343
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1864
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 43084
[WhiteheadRussell] p. 165Theorem *11.56aaanv 43080
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 43081
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 43082
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 43083
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 43088
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 43085
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 43086
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 43087
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 43089
[WhiteheadRussell] p. 175Definition *14.02df-eu 2564
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 43099  pm13.13b 43100
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 43101
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3023
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3024
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3655
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 43107
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 43108
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 43102
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 43246  pm13.193 43103
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 43104
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 43105
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 43106
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 43113
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 43112
[WhiteheadRussell] p. 184Definition *14.01iotasbc 43111
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3844
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 43114  pm14.122b 43115  pm14.122c 43116
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 43117  pm14.123b 43118  pm14.123c 43119
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 43121
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 43120
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 43122
[WhiteheadRussell] p. 190Theorem *14.22iota4 6521
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 43123
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6522
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 43124
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 43126
[WhiteheadRussell] p. 192Theorem *14.26eupick 2630  eupickbi 2633  sbaniota 43127
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 43125
[WhiteheadRussell] p. 192Theorem *14.271eubi 2579
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 43129
[WhiteheadRussell] p. 235Definition *30.01conventions 29633  df-fv 6548
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9992  pm54.43lem 9991
[Young] p. 141Definition of operator orderingleop2 31355
[Young] p. 142Example 12.2(i)0leop 31361  idleop 31362
[vandenDries] p. 42Lemma 61irrapx1 41499
[vandenDries] p. 43Theorem 62pellex 41506  pellexlem1 41500

This page was last updated on 23-Mar-2025.
Copyright terms: Public domain