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 17603
[Adamek] p. 21Condition 3.1(b)df-cat 17603
[Adamek] p. 22Example 3.3(1)df-setc 18012
[Adamek] p. 24Example 3.3(4.c)0cat 17624  0funcg 49433  df-termc 49821
[Adamek] p. 24Example 3.3(4.d)df-prstc 49898  prsthinc 49812
[Adamek] p. 24Example 3.3(4.e)df-mndtc 49926  df-mndtc 49926
[Adamek] p. 24Example 3.3(4)(c)discsnterm 49922
[Adamek] p. 25Definition 3.5df-oppc 17647
[Adamek] p. 25Example 3.6(1)oduoppcciso 49914
[Adamek] p. 25Example 3.6(2)oppgoppcco 49939  oppgoppchom 49938  oppgoppcid 49940
[Adamek] p. 28Remark 3.9oppciso 17717
[Adamek] p. 28Remark 3.12invf1o 17705  invisoinvl 17726
[Adamek] p. 28Example 3.13idinv 17725  idiso 17724
[Adamek] p. 28Corollary 3.11inveq 17710
[Adamek] p. 28Definition 3.8df-inv 17684  df-iso 17685  dfiso2 17708
[Adamek] p. 28Proposition 3.10sectcan 17691
[Adamek] p. 29Remark 3.16cicer 17742  cicerALT 49394
[Adamek] p. 29Definition 3.15cic 17735  df-cic 17732
[Adamek] p. 29Definition 3.17df-func 17794
[Adamek] p. 29Proposition 3.14(1)invinv 17706
[Adamek] p. 29Proposition 3.14(2)invco 17707  isoco 17713
[Adamek] p. 30Remark 3.19df-func 17794
[Adamek] p. 30Example 3.20(1)idfucl 17817
[Adamek] p. 30Example 3.20(2)diag1 49652
[Adamek] p. 32Proposition 3.21funciso 17810
[Adamek] p. 33Example 3.26(1)discsnterm 49922  discthing 49809
[Adamek] p. 33Example 3.26(2)df-thinc 49766  prsthinc 49812  thincciso 49801  thincciso2 49803  thincciso3 49804  thinccisod 49802
[Adamek] p. 33Example 3.26(3)df-mndtc 49926
[Adamek] p. 33Proposition 3.23cofucl 17824  cofucla 49444
[Adamek] p. 34Remark 3.28(1)cofidfth 49510
[Adamek] p. 34Remark 3.28(2)catciso 18047  catcisoi 49748
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18102
[Adamek] p. 34Definition 3.27(2)df-fth 17843
[Adamek] p. 34Definition 3.27(3)df-full 17842
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18102
[Adamek] p. 35Corollary 3.32ffthiso 17867
[Adamek] p. 35Proposition 3.30(c)cofth 17873
[Adamek] p. 35Proposition 3.30(d)cofull 17872
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18087
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18087
[Adamek] p. 39Remark 3.422oppf 49480
[Adamek] p. 39Definition 3.41df-oppf 49471  funcoppc 17811
[Adamek] p. 39Definition 3.44.df-catc 18035  elcatchom 49745
[Adamek] p. 39Proposition 3.43(c)fthoppc 17861  fthoppf 49512
[Adamek] p. 39Proposition 3.43(d)fulloppc 17860  fulloppf 49511
[Adamek] p. 40Remark 3.48catccat 18044
[Adamek] p. 40Definition 3.470funcg 49433  df-catc 18035
[Adamek] p. 45Exercise 3Gincat 49949
[Adamek] p. 48Remark 4.2(2)cnelsubc 49952  nelsubc3 49419
[Adamek] p. 48Remark 4.2(3)imasubc 49499  imasubc2 49500  imasubc3 49504
[Adamek] p. 48Example 4.3(1.a)0subcat 17774
[Adamek] p. 48Example 4.3(1.b)catsubcat 17775
[Adamek] p. 48Definition 4.1(1)nelsubc3 49419
[Adamek] p. 48Definition 4.1(2)fullsubc 17786
[Adamek] p. 48Definition 4.1(a)df-subc 17748
[Adamek] p. 49Remark 4.4idsubc 49508
[Adamek] p. 49Remark 4.4(1)idemb 49507
[Adamek] p. 49Remark 4.4(2)idfullsubc 49509  ressffth 17876
[Adamek] p. 58Exercise 4Asetc1onsubc 49950
[Adamek] p. 83Definition 6.1df-nat 17882
[Adamek] p. 87Remark 6.14(a)fuccocl 17903
[Adamek] p. 87Remark 6.14(b)fucass 17907
[Adamek] p. 87Definition 6.15df-fuc 17883
[Adamek] p. 88Remark 6.16fuccat 17909
[Adamek] p. 101Definition 7.10funcg 49433  df-inito 17920
[Adamek] p. 101Example 7.2(3)0funcg 49433  df-termc 49821  initc 49439
[Adamek] p. 101Example 7.2 (6)irinitoringc 21446
[Adamek] p. 102Definition 7.4df-termo 17921  oppctermo 49584
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17948
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17952
[Adamek] p. 103Remark 7.8oppczeroo 49585
[Adamek] p. 103Definition 7.7df-zeroo 17922
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21447
[Adamek] p. 103Proposition 7.6termoeu1w 17955
[Adamek] p. 106Definition 7.19df-sect 17683
[Adamek] p. 107Example 7.20(7)thincinv 49817
[Adamek] p. 108Example 7.25(4)thincsect2 49816
[Adamek] p. 110Example 7.33(9)thincmon 49781
[Adamek] p. 110Proposition 7.35sectmon 17718
[Adamek] p. 112Proposition 7.42sectepi 17720
[Adamek] p. 185Section 10.67updjud 9858
[Adamek] p. 193Definition 11.1(1)df-lmd 49993
[Adamek] p. 193Definition 11.3(1)df-lmd 49993
[Adamek] p. 194Definition 11.3(2)df-lmd 49993
[Adamek] p. 202Definition 11.27(1)df-cmd 49994
[Adamek] p. 202Definition 11.27(2)df-cmd 49994
[Adamek] p. 478Item Rngdf-ringc 20591
[AhoHopUll] p. 2Section 1.1df-bigo 48897
[AhoHopUll] p. 12Section 1.3df-blen 48919
[AhoHopUll] p. 318Section 9.1df-concat 14506  df-pfx 14607  df-substr 14577  df-word 14449  lencl 14468  wrd0 14474
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24664  df-nmoo 30832
[AkhiezerGlazman] p. 64Theoremhmopidmch 32240  hmopidmchi 32238
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32288  pjcmul2i 32289
[AkhiezerGlazman] p. 72Theoremcnvunop 32005  unoplin 32007
[AkhiezerGlazman] p. 72Equation 2unopadj 32006  unopadj2 32025
[AkhiezerGlazman] p. 73Theoremelunop2 32100  lnopunii 32099
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32173
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27935
[Alling] p. 184Axiom Bbdayfo 27657
[Alling] p. 184Axiom Oltsso 27656
[Alling] p. 184Axiom SDnodense 27672
[Alling] p. 185Lemma 0nocvxmin 27763
[Alling] p. 185Theoremconway 27787
[Alling] p. 185Axiom FEnoeta 27723
[Alling] p. 186Theorem 4lesrec 27807  lesrecd 27808
[Alling], p. 2Definitionrp-brsslt 43768
[Alling], p. 3Notenla0001 43771  nla0002 43769  nla0003 43770
[Apostol] p. 18Theorem I.1addcan 11329  addcan2d 11349  addcan2i 11339  addcand 11348  addcani 11338
[Apostol] p. 18Theorem I.2negeu 11382
[Apostol] p. 18Theorem I.3negsub 11441  negsubd 11510  negsubi 11471
[Apostol] p. 18Theorem I.4negneg 11443  negnegd 11495  negnegi 11463
[Apostol] p. 18Theorem I.5subdi 11582  subdid 11605  subdii 11598  subdir 11583  subdird 11606  subdiri 11599
[Apostol] p. 18Theorem I.6mul01 11324  mul01d 11344  mul01i 11335  mul02 11323  mul02d 11343  mul02i 11334
[Apostol] p. 18Theorem I.7mulcan 11786  mulcan2d 11783  mulcand 11782  mulcani 11788
[Apostol] p. 18Theorem I.8receu 11794  xreceu 33013
[Apostol] p. 18Theorem I.9divrec 11824  divrecd 11932  divreci 11898  divreczi 11891
[Apostol] p. 18Theorem I.10recrec 11850  recreci 11885
[Apostol] p. 18Theorem I.11mul0or 11789  mul0ord 11797  mul0ori 11796
[Apostol] p. 18Theorem I.12mul2neg 11588  mul2negd 11604  mul2negi 11597  mulneg1 11585  mulneg1d 11602  mulneg1i 11595
[Apostol] p. 18Theorem I.13divadddiv 11868  divadddivd 11973  divadddivi 11915
[Apostol] p. 18Theorem I.14divmuldiv 11853  divmuldivd 11970  divmuldivi 11913  rdivmuldivd 20361
[Apostol] p. 18Theorem I.15divdivdiv 11854  divdivdivd 11976  divdivdivi 11916
[Apostol] p. 20Axiom 7rpaddcl 12941  rpaddcld 12976  rpmulcl 12942  rpmulcld 12977
[Apostol] p. 20Axiom 8rpneg 12951
[Apostol] p. 20Axiom 90nrp 12954
[Apostol] p. 20Theorem I.17lttri 11271
[Apostol] p. 20Theorem I.18ltadd1d 11742  ltadd1dd 11760  ltadd1i 11703
[Apostol] p. 20Theorem I.19ltmul1 12003  ltmul1a 12002  ltmul1i 12072  ltmul1ii 12082  ltmul2 12004  ltmul2d 13003  ltmul2dd 13017  ltmul2i 12075
[Apostol] p. 20Theorem I.20msqgt0 11669  msqgt0d 11716  msqgt0i 11686
[Apostol] p. 20Theorem I.210lt1 11671
[Apostol] p. 20Theorem I.23lt0neg1 11655  lt0neg1d 11718  ltneg 11649  ltnegd 11727  ltnegi 11693
[Apostol] p. 20Theorem I.25lt2add 11634  lt2addd 11772  lt2addi 11711
[Apostol] p. 20Definition of positive numbersdf-rp 12918
[Apostol] p. 21Exercise 4recgt0 11999  recgt0d 12088  recgt0i 12059  recgt0ii 12060
[Apostol] p. 22Definition of integersdf-z 12501
[Apostol] p. 22Definition of positive integersdfnn3 12171
[Apostol] p. 22Definition of rationalsdf-q 12874
[Apostol] p. 24Theorem I.26supeu 9369
[Apostol] p. 26Theorem I.28nnunb 12409
[Apostol] p. 26Theorem I.29arch 12410  archd 45510
[Apostol] p. 28Exercise 2btwnz 12607
[Apostol] p. 28Exercise 3nnrecl 12411
[Apostol] p. 28Exercise 4rebtwnz 12872
[Apostol] p. 28Exercise 5zbtwnre 12871
[Apostol] p. 28Exercise 6qbtwnre 13126
[Apostol] p. 28Exercise 10(a)zeneo 16278  zneo 12587  zneoALTV 48018
[Apostol] p. 29Theorem I.35cxpsqrtth 26707  msqsqrtd 15378  resqrtth 15190  sqrtth 15300  sqrtthi 15306  sqsqrtd 15377
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12160
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12838
[Apostol] p. 361Remarkcrreczi 14163
[Apostol] p. 363Remarkabsgt0i 15335
[Apostol] p. 363Exampleabssubd 15391  abssubi 15339
[ApostolNT] p. 7Remarkfmtno0 47889  fmtno1 47890  fmtno2 47899  fmtno3 47900  fmtno4 47901  fmtno5fac 47931  fmtnofz04prm 47926
[ApostolNT] p. 7Definitiondf-fmtno 47877
[ApostolNT] p. 8Definitiondf-ppi 27078
[ApostolNT] p. 14Definitiondf-dvds 16192
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16208
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16233
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16228
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16221
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16223
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16209
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16210
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16215
[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 16434  dfgcd2 16485
[ApostolNT] p. 16Definitionisprm2 16621
[ApostolNT] p. 16Theorem 1.5coprmdvds 16592
[ApostolNT] p. 16Theorem 1.7prminf 16855
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16452
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16486
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16488
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16467
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16459
[ApostolNT] p. 17Theorem 1.8coprm 16650
[ApostolNT] p. 17Theorem 1.9euclemma 16652
[ApostolNT] p. 17Theorem 1.101arith2 16868
[ApostolNT] p. 18Theorem 1.13prmrec 16862
[ApostolNT] p. 19Theorem 1.14divalg 16342
[ApostolNT] p. 20Theorem 1.15eucalg 16526
[ApostolNT] p. 24Definitiondf-mu 27079
[ApostolNT] p. 25Definitiondf-phi 16705
[ApostolNT] p. 25Theorem 2.1musum 27169
[ApostolNT] p. 26Theorem 2.2phisum 16730
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16715
[ApostolNT] p. 28Theorem 2.5(c)phimul 16719
[ApostolNT] p. 32Definitiondf-vma 27076
[ApostolNT] p. 32Theorem 2.9muinv 27171
[ApostolNT] p. 32Theorem 2.10vmasum 27195
[ApostolNT] p. 38Remarkdf-sgm 27080
[ApostolNT] p. 38Definitiondf-sgm 27080
[ApostolNT] p. 75Definitiondf-chp 27077  df-cht 27075
[ApostolNT] p. 104Definitioncongr 16603
[ApostolNT] p. 106Remarkdvdsval3 16195
[ApostolNT] p. 106Definitionmoddvds 16202
[ApostolNT] p. 107Example 2mod2eq0even 16285
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16286
[ApostolNT] p. 107Example 4zmod1congr 13820
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13860
[ApostolNT] p. 107Theorem 5.2(c)modexp 14173
[ApostolNT] p. 108Theorem 5.3modmulconst 16227
[ApostolNT] p. 109Theorem 5.4cncongr1 16606
[ApostolNT] p. 109Theorem 5.6gcdmodi 17014
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16608
[ApostolNT] p. 113Theorem 5.17eulerth 16722
[ApostolNT] p. 113Theorem 5.18vfermltl 16741
[ApostolNT] p. 114Theorem 5.19fermltl 16723
[ApostolNT] p. 116Theorem 5.24wilthimp 27050
[ApostolNT] p. 179Definitiondf-lgs 27274  lgsprme0 27318
[ApostolNT] p. 180Example 11lgs 27319
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27295
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27310
[ApostolNT] p. 181Theorem 9.4m1lgs 27367
[ApostolNT] p. 181Theorem 9.52lgs 27386  2lgsoddprm 27395
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27353
[ApostolNT] p. 185Theorem 9.8lgsquad 27362
[ApostolNT] p. 188Definitiondf-lgs 27274  lgs1 27320
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27311
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27313
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27321
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27322
[Baer] p. 40Property (b)mapdord 42003
[Baer] p. 40Property (c)mapd11 42004
[Baer] p. 40Property (e)mapdin 42027  mapdlsm 42029
[Baer] p. 40Property (f)mapd0 42030
[Baer] p. 40Definition of projectivitydf-mapd 41990  mapd1o 42013
[Baer] p. 41Property (g)mapdat 42032
[Baer] p. 44Part (1)mapdpg 42071
[Baer] p. 45Part (2)hdmap1eq 42166  mapdheq 42093  mapdheq2 42094  mapdheq2biN 42095
[Baer] p. 45Part (3)baerlem3 42078
[Baer] p. 46Part (4)mapdheq4 42097  mapdheq4lem 42096
[Baer] p. 46Part (5)baerlem5a 42079  baerlem5abmN 42083  baerlem5amN 42081  baerlem5b 42080  baerlem5bmN 42082
[Baer] p. 47Part (6)hdmap1l6 42186  hdmap1l6a 42174  hdmap1l6e 42179  hdmap1l6f 42180  hdmap1l6g 42181  hdmap1l6lem1 42172  hdmap1l6lem2 42173  mapdh6N 42112  mapdh6aN 42100  mapdh6eN 42105  mapdh6fN 42106  mapdh6gN 42107  mapdh6lem1N 42098  mapdh6lem2N 42099
[Baer] p. 48Part 9hdmapval 42193
[Baer] p. 48Part 10hdmap10 42205
[Baer] p. 48Part 11hdmapadd 42208
[Baer] p. 48Part (6)hdmap1l6h 42182  mapdh6hN 42108
[Baer] p. 48Part (7)mapdh75cN 42118  mapdh75d 42119  mapdh75e 42117  mapdh75fN 42120  mapdh7cN 42114  mapdh7dN 42115  mapdh7eN 42113  mapdh7fN 42116
[Baer] p. 48Part (8)mapdh8 42153  mapdh8a 42140  mapdh8aa 42141  mapdh8ab 42142  mapdh8ac 42143  mapdh8ad 42144  mapdh8b 42145  mapdh8c 42146  mapdh8d 42148  mapdh8d0N 42147  mapdh8e 42149  mapdh8g 42150  mapdh8i 42151  mapdh8j 42152
[Baer] p. 48Part (9)mapdh9a 42154
[Baer] p. 48Equation 10mapdhvmap 42134
[Baer] p. 49Part 12hdmap11 42213  hdmapeq0 42209  hdmapf1oN 42230  hdmapneg 42211  hdmaprnN 42229  hdmaprnlem1N 42214  hdmaprnlem3N 42215  hdmaprnlem3uN 42216  hdmaprnlem4N 42218  hdmaprnlem6N 42219  hdmaprnlem7N 42220  hdmaprnlem8N 42221  hdmaprnlem9N 42222  hdmapsub 42212
[Baer] p. 49Part 14hdmap14lem1 42233  hdmap14lem10 42242  hdmap14lem1a 42231  hdmap14lem2N 42234  hdmap14lem2a 42232  hdmap14lem3 42235  hdmap14lem8 42240  hdmap14lem9 42241
[Baer] p. 50Part 14hdmap14lem11 42243  hdmap14lem12 42244  hdmap14lem13 42245  hdmap14lem14 42246  hdmap14lem15 42247  hgmapval 42252
[Baer] p. 50Part 15hgmapadd 42259  hgmapmul 42260  hgmaprnlem2N 42262  hgmapvs 42256
[Baer] p. 50Part 16hgmaprnN 42266
[Baer] p. 110Lemma 1hdmapip0com 42282
[Baer] p. 110Line 27hdmapinvlem1 42283
[Baer] p. 110Line 28hdmapinvlem2 42284
[Baer] p. 110Line 30hdmapinvlem3 42285
[Baer] p. 110Part 1.2hdmapglem5 42287  hgmapvv 42291
[Baer] p. 110Proposition 1hdmapinvlem4 42286
[Baer] p. 111Line 10hgmapvvlem1 42288
[Baer] p. 111Line 15hdmapg 42295  hdmapglem7 42294
[Bauer], p. 483Theorem 1.22irrexpq 26708  2irrexpqALT 26778
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2570
[BellMachover] p. 460Notationdf-mo 2540
[BellMachover] p. 460Definitionmo3 2565
[BellMachover] p. 461Axiom Extax-ext 2709
[BellMachover] p. 462Theorem 1.1axextmo 2713
[BellMachover] p. 463Axiom Repaxrep5 5234
[BellMachover] p. 463Scheme Sepax-sep 5243
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37303  sepex 5247
[BellMachover] p. 466Problemaxpow2 5314
[BellMachover] p. 466Axiom Powaxpow3 5315
[BellMachover] p. 466Axiom Unionaxun2 7692
[BellMachover] p. 468Definitiondf-ord 6328
[BellMachover] p. 469Theorem 2.2(i)ordirr 6343
[BellMachover] p. 469Theorem 2.2(iii)onelon 6350
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6345
[BellMachover] p. 471Definition of Ndf-om 7819
[BellMachover] p. 471Problem 2.5(ii)uniordint 7756
[BellMachover] p. 471Definition of Limdf-lim 6330
[BellMachover] p. 472Axiom Infzfinf2 9563
[BellMachover] p. 473Theorem 2.8limom 7834
[BellMachover] p. 477Equation 3.1df-r1 9688
[BellMachover] p. 478Definitionrankval2 9742  rankval2b 35274
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9706  r1ord3g 9703
[BellMachover] p. 480Axiom Regzfreg 9513
[BellMachover] p. 488Axiom ACac5 10399  dfac4 10044
[BellMachover] p. 490Definition of alephalephval3 10032
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39684
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32440
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32482  chirredi 32481
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32470
[Beran] p. 3Definition of joinsshjval3 31441
[Beran] p. 39Theorem 2.3(i)cmcm2 31703  cmcm2i 31680  cmcm2ii 31685  cmt2N 39615
[Beran] p. 40Theorem 2.3(iii)lecm 31704  lecmi 31689  lecmii 31690
[Beran] p. 45Theorem 3.4cmcmlem 31678
[Beran] p. 49Theorem 4.2cm2j 31707  cm2ji 31712  cm2mi 31713
[Beran] p. 95Definitiondf-sh 31294  issh2 31296
[Beran] p. 95Lemma 3.1(S5)his5 31173
[Beran] p. 95Lemma 3.1(S6)his6 31186
[Beran] p. 95Lemma 3.1(S7)his7 31177
[Beran] p. 95Lemma 3.2(S8)ho01i 31915
[Beran] p. 95Lemma 3.2(S9)hoeq1 31917
[Beran] p. 95Lemma 3.2(S10)ho02i 31916
[Beran] p. 95Lemma 3.2(S11)hoeq2 31918
[Beran] p. 95Postulate (S1)ax-his1 31169  his1i 31187
[Beran] p. 95Postulate (S2)ax-his2 31170
[Beran] p. 95Postulate (S3)ax-his3 31171
[Beran] p. 95Postulate (S4)ax-his4 31172
[Beran] p. 96Definition of normdf-hnorm 31055  dfhnorm2 31209  normval 31211
[Beran] p. 96Definition for Cauchy sequencehcau 31271
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31060
[Beran] p. 96Definition of complete subspaceisch3 31328
[Beran] p. 96Definition of convergedf-hlim 31059  hlimi 31275
[Beran] p. 97Theorem 3.3(i)norm-i-i 31220  norm-i 31216
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31224  norm-ii 31225  normlem0 31196  normlem1 31197  normlem2 31198  normlem3 31199  normlem4 31200  normlem5 31201  normlem6 31202  normlem7 31203  normlem7tALT 31206
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31226  norm-iii 31227
[Beran] p. 98Remark 3.4bcs 31268  bcsiALT 31266  bcsiHIL 31267
[Beran] p. 98Remark 3.4(B)normlem9at 31208  normpar 31242  normpari 31241
[Beran] p. 98Remark 3.4(C)normpyc 31233  normpyth 31232  normpythi 31229
[Beran] p. 99Remarklnfn0 32134  lnfn0i 32129  lnop0 32053  lnop0i 32057
[Beran] p. 99Theorem 3.5(i)nmcexi 32113  nmcfnex 32140  nmcfnexi 32138  nmcopex 32116  nmcopexi 32114
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32141  nmcfnlbi 32139  nmcoplb 32117  nmcoplbi 32115
[Beran] p. 99Theorem 3.5(iii)lnfncon 32143  lnfnconi 32142  lnopcon 32122  lnopconi 32121
[Beran] p. 100Lemma 3.6normpar2i 31243
[Beran] p. 101Lemma 3.6norm3adifi 31240  norm3adifii 31235  norm3dif 31237  norm3difi 31234
[Beran] p. 102Theorem 3.7(i)chocunii 31388  pjhth 31480  pjhtheu 31481  pjpjhth 31512  pjpjhthi 31513  pjth 25407
[Beran] p. 102Theorem 3.7(ii)ococ 31493  ococi 31492
[Beran] p. 103Remark 3.8nlelchi 32148
[Beran] p. 104Theorem 3.9riesz3i 32149  riesz4 32151  riesz4i 32150
[Beran] p. 104Theorem 3.10cnlnadj 32166  cnlnadjeu 32165  cnlnadjeui 32164  cnlnadji 32163  cnlnadjlem1 32154  nmopadjlei 32175
[Beran] p. 106Theorem 3.11(i)adjeq0 32178
[Beran] p. 106Theorem 3.11(v)nmopadji 32177
[Beran] p. 106Theorem 3.11(ii)adjmul 32179
[Beran] p. 106Theorem 3.11(iv)adjadj 32023
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32189  nmopcoadji 32188
[Beran] p. 106Theorem 3.11(iii)adjadd 32180
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32190
[Beran] p. 106Theorem 3.11(viii)adjcoi 32187  pjadj2coi 32291  pjadjcoi 32248
[Beran] p. 107Definitiondf-ch 31308  isch2 31310
[Beran] p. 107Remark 3.12choccl 31393  isch3 31328  occl 31391  ocsh 31370  shoccl 31392  shocsh 31371
[Beran] p. 107Remark 3.12(B)ococin 31495
[Beran] p. 108Theorem 3.13chintcl 31419
[Beran] p. 109Property (i)pjadj2 32274  pjadj3 32275  pjadji 31772  pjadjii 31761
[Beran] p. 109Property (ii)pjidmco 32268  pjidmcoi 32264  pjidmi 31760
[Beran] p. 110Definition of projector orderingpjordi 32260
[Beran] p. 111Remarkho0val 31837  pjch1 31757
[Beran] p. 111Definitiondf-hfmul 31821  df-hfsum 31820  df-hodif 31819  df-homul 31818  df-hosum 31817
[Beran] p. 111Lemma 4.4(i)pjo 31758
[Beran] p. 111Lemma 4.4(ii)pjch 31781  pjchi 31519
[Beran] p. 111Lemma 4.4(iii)pjoc2 31526  pjoc2i 31525
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31767
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32252  pjssmii 31768
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32251
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32250
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32255
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32253  pjssge0ii 31769
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32254  pjdifnormii 31770
[Bobzien] p. 116Statement T3stoic3 1778
[Bobzien] p. 117Statement T2stoic2a 1776
[Bobzien] p. 117Statement T4stoic4a 1779
[Bobzien] p. 117Conclusion the contradictorystoic1a 1774
[Bogachev] p. 16Definition 1.5df-oms 34469
[Bogachev] p. 17Lemma 1.5.4omssubadd 34477
[Bogachev] p. 17Example 1.5.2omsmon 34475
[Bogachev] p. 41Definition 1.11.2df-carsg 34479
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34499
[Bogachev] p. 116Definition 2.3.1df-itgm 34530  df-sitm 34508
[Bogachev] p. 118Chapter 2.4.4df-itgm 34530
[Bogachev] p. 118Definition 2.4.1df-sitg 34507
[Bollobas] p. 1Section I.1df-edg 29133  isuhgrop 29155  isusgrop 29247  isuspgrop 29246
[Bollobas] p. 2Section I.1df-isubgr 48210  df-subgr 29353  uhgrspan1 29388  uhgrspansubgr 29376
[Bollobas] p. 3Definitiondf-gric 48230  gricuspgr 48267  isuspgrim 48245
[Bollobas] p. 3Section I.1cusgrsize 29540  df-clnbgr 48168  df-cusgr 29497  df-nbgr 29418  fusgrmaxsize 29550
[Bollobas] p. 4Definitiondf-upwlks 48483  df-wlks 29685
[Bollobas] p. 4Section I.1finsumvtxdg2size 29636  finsumvtxdgeven 29638  fusgr1th 29637  fusgrvtxdgonume 29640  vtxdgoddnumeven 29639
[Bollobas] p. 5Notationdf-pths 29799
[Bollobas] p. 5Definitiondf-crcts 29871  df-cycls 29872  df-trls 29776  df-wlkson 29686
[Bollobas] p. 7Section I.1df-ushgr 29144
[BourbakiAlg1] p. 1Definition 1df-clintop 48549  df-cllaw 48535  df-mgm 18577  df-mgm2 48568
[BourbakiAlg1] p. 4Definition 5df-assintop 48550  df-asslaw 48537  df-sgrp 18656  df-sgrp2 48570
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48569  df-comlaw 48536
[BourbakiAlg1] p. 12Definition 2df-mnd 18672
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33118  mndlactf1o 33122  mndractf1 33120  mndractf1o 33123
[BourbakiAlg1] p. 92Definition 1df-ring 20182
[BourbakiAlg1] p. 93Section I.8.1df-rng 20100
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33810
[BourbakiAlg2] p. 113Chapter 5.assafld 33814  assarrginv 33813
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33855  fldextrspunfld 33853  fldextrspunlem1 33852  fldextrspunlem2 33854  fldextrspunlsp 33851  fldextrspunlsplem 33850
[BourbakiCAlg2], p. 228Proposition 21arithidom 33629  dfufd2 33642
[BourbakiEns] p. Proposition 8fcof1 7243  fcofo 7244
[BourbakiTop1] p. Remarkxnegmnf 13137  xnegpnf 13136
[BourbakiTop1] p. Remark rexneg 13138
[BourbakiTop1] p. Remark 3ust0 24176  ustfilxp 24169
[BourbakiTop1] p. Axiom GT'tgpsubcn 24046
[BourbakiTop1] p. Criterionishmeo 23715
[BourbakiTop1] p. Example 1cstucnd 24239  iducn 24238  snfil 23820
[BourbakiTop1] p. Example 2neifil 23836
[BourbakiTop1] p. Theorem 1cnextcn 24023
[BourbakiTop1] p. Theorem 2ucnextcn 24259
[BourbakiTop1] p. Theorem 3df-hcmp 34134
[BourbakiTop1] p. Paragraph 3infil 23819
[BourbakiTop1] p. Definition 1df-ucn 24231  df-ust 24157  filintn0 23817  filn0 23818  istgp 24033  ucnprima 24237
[BourbakiTop1] p. Definition 2df-cfilu 24242
[BourbakiTop1] p. Definition 3df-cusp 24253  df-usp 24213  df-utop 24187  trust 24185
[BourbakiTop1] p. Definition 6df-pcmp 34033
[BourbakiTop1] p. Property V_issnei2 23072
[BourbakiTop1] p. Theorem 1(d)iscncl 23225
[BourbakiTop1] p. Condition F_Iustssel 24162
[BourbakiTop1] p. Condition U_Iustdiag 24165
[BourbakiTop1] p. Property V_iiinnei 23081
[BourbakiTop1] p. Property V_ivneiptopreu 23089  neissex 23083
[BourbakiTop1] p. Proposition 1neips 23069  neiss 23065  ucncn 24240  ustund 24178  ustuqtop 24202
[BourbakiTop1] p. Proposition 2cnpco 23223  neiptopreu 23089  utop2nei 24206  utop3cls 24207
[BourbakiTop1] p. Proposition 3fmucnd 24247  uspreg 24229  utopreg 24208
[BourbakiTop1] p. Proposition 4imasncld 23647  imasncls 23648  imasnopn 23646
[BourbakiTop1] p. Proposition 9cnpflf2 23956
[BourbakiTop1] p. Condition F_IIustincl 24164
[BourbakiTop1] p. Condition U_IIustinvel 24166
[BourbakiTop1] p. Property V_iiielnei 23067
[BourbakiTop1] p. Proposition 11cnextucn 24258
[BourbakiTop1] p. Condition F_IIbustbasel 24163
[BourbakiTop1] p. Condition U_IIIustexhalf 24167
[BourbakiTop1] p. Definition C'''df-cmp 23343
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23802
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22850
[BourbakiTop2] p. 195Definition 1df-ldlf 34030
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46409
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46411  stoweid 46410
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46348  stoweidlem10 46357  stoweidlem14 46361  stoweidlem15 46362  stoweidlem35 46382  stoweidlem36 46383  stoweidlem37 46384  stoweidlem38 46385  stoweidlem40 46387  stoweidlem41 46388  stoweidlem43 46390  stoweidlem44 46391  stoweidlem46 46393  stoweidlem5 46352  stoweidlem50 46397  stoweidlem52 46399  stoweidlem53 46400  stoweidlem55 46402  stoweidlem56 46403
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46370  stoweidlem24 46371  stoweidlem27 46374  stoweidlem28 46375  stoweidlem30 46377
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46381  stoweidlem59 46406  stoweidlem60 46407
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46392  stoweidlem49 46396  stoweidlem7 46354
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46378  stoweidlem39 46386  stoweidlem42 46389  stoweidlem48 46395  stoweidlem51 46398  stoweidlem54 46401  stoweidlem57 46404  stoweidlem58 46405
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46372
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46364
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46358  stoweidlem13 46360  stoweidlem26 46373  stoweidlem61 46408
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46365
[Bruck] p. 1Section I.1df-clintop 48549  df-mgm 18577  df-mgm2 48568
[Bruck] p. 23Section II.1df-sgrp 18656  df-sgrp2 48570
[Bruck] p. 28Theorem 3.2dfgrp3 18981
[ChoquetDD] p. 2Definition of mappingdf-mpt 5182
[Church] p. 129Section II.24df-ifp 1064  dfifp2 1065
[Clemente] p. 10Definition ITnatded 30490
[Clemente] p. 10Definition I` `m,nnatded 30490
[Clemente] p. 11Definition E=>m,nnatded 30490
[Clemente] p. 11Definition I=>m,nnatded 30490
[Clemente] p. 11Definition E` `(1)natded 30490
[Clemente] p. 11Definition E` `(2)natded 30490
[Clemente] p. 12Definition E` `m,n,pnatded 30490
[Clemente] p. 12Definition I` `n(1)natded 30490
[Clemente] p. 12Definition I` `n(2)natded 30490
[Clemente] p. 13Definition I` `m,n,pnatded 30490
[Clemente] p. 14Proof 5.11natded 30490
[Clemente] p. 14Definition E` `nnatded 30490
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30492  ex-natded5.2 30491
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30495  ex-natded5.3 30494
[Clemente] p. 18Theorem 5.5ex-natded5.5 30497
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30499  ex-natded5.7 30498
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30501  ex-natded5.8 30500
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30503  ex-natded5.13 30502
[Clemente] p. 32Definition I` `nnatded 30490
[Clemente] p. 32Definition E` `m,n,p,anatded 30490
[Clemente] p. 32Definition E` `n,tnatded 30490
[Clemente] p. 32Definition I` `n,tnatded 30490
[Clemente] p. 43Theorem 9.20ex-natded9.20 30504
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30505
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30507  ex-natded9.26 30506
[Cohen] p. 301Remarkrelogoprlem 26568
[Cohen] p. 301Property 2relogmul 26569  relogmuld 26602
[Cohen] p. 301Property 3relogdiv 26570  relogdivd 26603
[Cohen] p. 301Property 4relogexp 26573
[Cohen] p. 301Property 1alog1 26562
[Cohen] p. 301Property 1bloge 26563
[Cohen4] p. 348Observationrelogbcxpb 26765
[Cohen4] p. 349Propertyrelogbf 26769
[Cohen4] p. 352Definitionelogb 26748
[Cohen4] p. 361Property 2relogbmul 26755
[Cohen4] p. 361Property 3logbrec 26760  relogbdiv 26757
[Cohen4] p. 361Property 4relogbreexp 26753
[Cohen4] p. 361Property 6relogbexp 26758
[Cohen4] p. 361Property 1(a)logbid1 26746
[Cohen4] p. 361Property 1(b)logb1 26747
[Cohen4] p. 367Propertylogbchbase 26749
[Cohen4] p. 377Property 2logblt 26762
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34462  sxbrsigalem4 34464
[Cohn] p. 81Section II.5acsdomd 18492  acsinfd 18491  acsinfdimd 18493  acsmap2d 18490  acsmapd 18489
[Cohn] p. 143Example 5.1.1sxbrsiga 34467
[Connell] p. 57Definitiondf-scmat 22447  df-scmatalt 48748
[Conway] p. 4Definitionlesrec 27807  lesrecd 27808
[Conway] p. 5Definitionaddsval 27970  addsval2 27971  df-adds 27968  df-muls 28115  df-negs 28029
[Conway] p. 7Theorem0lt1s 27820
[Conway] p. 12Theorem 12pw2cut2 28470
[Conway] p. 16Theorem 0(i)sltsright 27869
[Conway] p. 16Theorem 0(ii)sltsleft 27868
[Conway] p. 16Theorem 0(iii)lesid 27747
[Conway] p. 17Theorem 3addsass 28013  addsassd 28014  addscom 27974  addscomd 27975  addsrid 27972  addsridd 27973
[Conway] p. 17Definitiondf-0s 27815
[Conway] p. 17Theorem 4(ii)negnegs 28052
[Conway] p. 17Theorem 4(iii)negsid 28049  negsidd 28050
[Conway] p. 18Theorem 5leadds1 27997  leadds1d 28003
[Conway] p. 18Definitiondf-1s 27816
[Conway] p. 18Theorem 6(ii)negscl 28044  negscld 28045
[Conway] p. 18Theorem 6(iii)addscld 27988
[Conway] p. 19Notemulsunif2 28178
[Conway] p. 19Theorem 7addsdi 28163  addsdid 28164  addsdird 28165  mulnegs1d 28168  mulnegs2d 28169  mulsass 28174  mulsassd 28175  mulscom 28147  mulscomd 28148
[Conway] p. 19Theorem 8(i)mulscl 28142  mulscld 28143
[Conway] p. 19Theorem 8(iii)lemulsd 28146  ltmuls 28144  ltmulsd 28145
[Conway] p. 20Theorem 9mulsgt0 28152  mulsgt0d 28153
[Conway] p. 21Theorem 10(iv)precsex 28226
[Conway] p. 23Theorem 11eqcuts3 27812
[Conway] p. 24Definitiondf-reno 28498
[Conway] p. 24Theorem 13(ii)readdscl 28507  remulscl 28510  renegscl 28506
[Conway] p. 27Definitiondf-ons 28260  elons2 28266
[Conway] p. 27Theorem 14ltonsex 28270
[Conway] p. 28Theorem 15oncutlt 28272  onswe 28280
[Conway] p. 29Remarkmadebday 27908  newbday 27910  oldbday 27909
[Conway] p. 29Definitiondf-made 27835  df-new 27837  df-old 27836
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13793
[Crawley] p. 1Definition of posetdf-poset 18248
[Crawley] p. 107Theorem 13.2hlsupr 39751
[Crawley] p. 110Theorem 13.3arglem1N 40555  dalaw 40251
[Crawley] p. 111Theorem 13.4hlathil 42326
[Crawley] p. 111Definition of set Wdf-watsN 40355
[Crawley] p. 111Definition of dilationdf-dilN 40471  df-ldil 40469  isldil 40475
[Crawley] p. 111Definition of translationdf-ltrn 40470  df-trnN 40472  isltrn 40484  ltrnu 40486
[Crawley] p. 112Lemma Acdlema1N 40156  cdlema2N 40157  exatleN 39769
[Crawley] p. 112Lemma B1cvrat 39841  cdlemb 40159  cdlemb2 40406  cdlemb3 40971  idltrn 40515  l1cvat 39420  lhpat 40408  lhpat2 40410  lshpat 39421  ltrnel 40504  ltrnmw 40516
[Crawley] p. 112Lemma Ccdlemc1 40556  cdlemc2 40557  ltrnnidn 40539  trlat 40534  trljat1 40531  trljat2 40532  trljat3 40533  trlne 40550  trlnidat 40538  trlnle 40551
[Crawley] p. 112Definition of automorphismdf-pautN 40356
[Crawley] p. 113Lemma Ccdlemc 40562  cdlemc3 40558  cdlemc4 40559
[Crawley] p. 113Lemma Dcdlemd 40572  cdlemd1 40563  cdlemd2 40564  cdlemd3 40565  cdlemd4 40566  cdlemd5 40567  cdlemd6 40568  cdlemd7 40569  cdlemd8 40570  cdlemd9 40571  cdleme31sde 40750  cdleme31se 40747  cdleme31se2 40748  cdleme31snd 40751  cdleme32a 40806  cdleme32b 40807  cdleme32c 40808  cdleme32d 40809  cdleme32e 40810  cdleme32f 40811  cdleme32fva 40802  cdleme32fva1 40803  cdleme32fvcl 40805  cdleme32le 40812  cdleme48fv 40864  cdleme4gfv 40872  cdleme50eq 40906  cdleme50f 40907  cdleme50f1 40908  cdleme50f1o 40911  cdleme50laut 40912  cdleme50ldil 40913  cdleme50lebi 40905  cdleme50rn 40910  cdleme50rnlem 40909  cdlemeg49le 40876  cdlemeg49lebilem 40904
[Crawley] p. 113Lemma Ecdleme 40925  cdleme00a 40574  cdleme01N 40586  cdleme02N 40587  cdleme0a 40576  cdleme0aa 40575  cdleme0b 40577  cdleme0c 40578  cdleme0cp 40579  cdleme0cq 40580  cdleme0dN 40581  cdleme0e 40582  cdleme0ex1N 40588  cdleme0ex2N 40589  cdleme0fN 40583  cdleme0gN 40584  cdleme0moN 40590  cdleme1 40592  cdleme10 40619  cdleme10tN 40623  cdleme11 40635  cdleme11a 40625  cdleme11c 40626  cdleme11dN 40627  cdleme11e 40628  cdleme11fN 40629  cdleme11g 40630  cdleme11h 40631  cdleme11j 40632  cdleme11k 40633  cdleme11l 40634  cdleme12 40636  cdleme13 40637  cdleme14 40638  cdleme15 40643  cdleme15a 40639  cdleme15b 40640  cdleme15c 40641  cdleme15d 40642  cdleme16 40650  cdleme16aN 40624  cdleme16b 40644  cdleme16c 40645  cdleme16d 40646  cdleme16e 40647  cdleme16f 40648  cdleme16g 40649  cdleme19a 40668  cdleme19b 40669  cdleme19c 40670  cdleme19d 40671  cdleme19e 40672  cdleme19f 40673  cdleme1b 40591  cdleme2 40593  cdleme20aN 40674  cdleme20bN 40675  cdleme20c 40676  cdleme20d 40677  cdleme20e 40678  cdleme20f 40679  cdleme20g 40680  cdleme20h 40681  cdleme20i 40682  cdleme20j 40683  cdleme20k 40684  cdleme20l 40687  cdleme20l1 40685  cdleme20l2 40686  cdleme20m 40688  cdleme20y 40667  cdleme20zN 40666  cdleme21 40702  cdleme21d 40695  cdleme21e 40696  cdleme22a 40705  cdleme22aa 40704  cdleme22b 40706  cdleme22cN 40707  cdleme22d 40708  cdleme22e 40709  cdleme22eALTN 40710  cdleme22f 40711  cdleme22f2 40712  cdleme22g 40713  cdleme23a 40714  cdleme23b 40715  cdleme23c 40716  cdleme26e 40724  cdleme26eALTN 40726  cdleme26ee 40725  cdleme26f 40728  cdleme26f2 40730  cdleme26f2ALTN 40729  cdleme26fALTN 40727  cdleme27N 40734  cdleme27a 40732  cdleme27cl 40731  cdleme28c 40737  cdleme3 40602  cdleme30a 40743  cdleme31fv 40755  cdleme31fv1 40756  cdleme31fv1s 40757  cdleme31fv2 40758  cdleme31id 40759  cdleme31sc 40749  cdleme31sdnN 40752  cdleme31sn 40745  cdleme31sn1 40746  cdleme31sn1c 40753  cdleme31sn2 40754  cdleme31so 40744  cdleme35a 40813  cdleme35b 40815  cdleme35c 40816  cdleme35d 40817  cdleme35e 40818  cdleme35f 40819  cdleme35fnpq 40814  cdleme35g 40820  cdleme35h 40821  cdleme35h2 40822  cdleme35sn2aw 40823  cdleme35sn3a 40824  cdleme36a 40825  cdleme36m 40826  cdleme37m 40827  cdleme38m 40828  cdleme38n 40829  cdleme39a 40830  cdleme39n 40831  cdleme3b 40594  cdleme3c 40595  cdleme3d 40596  cdleme3e 40597  cdleme3fN 40598  cdleme3fa 40601  cdleme3g 40599  cdleme3h 40600  cdleme4 40603  cdleme40m 40832  cdleme40n 40833  cdleme40v 40834  cdleme40w 40835  cdleme41fva11 40842  cdleme41sn3aw 40839  cdleme41sn4aw 40840  cdleme41snaw 40841  cdleme42a 40836  cdleme42b 40843  cdleme42c 40837  cdleme42d 40838  cdleme42e 40844  cdleme42f 40845  cdleme42g 40846  cdleme42h 40847  cdleme42i 40848  cdleme42k 40849  cdleme42ke 40850  cdleme42keg 40851  cdleme42mN 40852  cdleme42mgN 40853  cdleme43aN 40854  cdleme43bN 40855  cdleme43cN 40856  cdleme43dN 40857  cdleme5 40605  cdleme50ex 40924  cdleme50ltrn 40922  cdleme51finvN 40921  cdleme51finvfvN 40920  cdleme51finvtrN 40923  cdleme6 40606  cdleme7 40614  cdleme7a 40608  cdleme7aa 40607  cdleme7b 40609  cdleme7c 40610  cdleme7d 40611  cdleme7e 40612  cdleme7ga 40613  cdleme8 40615  cdleme8tN 40620  cdleme9 40618  cdleme9a 40616  cdleme9b 40617  cdleme9tN 40622  cdleme9taN 40621  cdlemeda 40663  cdlemedb 40662  cdlemednpq 40664  cdlemednuN 40665  cdlemefr27cl 40768  cdlemefr32fva1 40775  cdlemefr32fvaN 40774  cdlemefrs32fva 40765  cdlemefrs32fva1 40766  cdlemefs27cl 40778  cdlemefs32fva1 40788  cdlemefs32fvaN 40787  cdlemesner 40661  cdlemeulpq 40585
[Crawley] p. 114Lemma E4atex 40441  4atexlem7 40440  cdleme0nex 40655  cdleme17a 40651  cdleme17c 40653  cdleme17d 40863  cdleme17d1 40654  cdleme17d2 40860  cdleme18a 40656  cdleme18b 40657  cdleme18c 40658  cdleme18d 40660  cdleme4a 40604
[Crawley] p. 115Lemma Ecdleme21a 40690  cdleme21at 40693  cdleme21b 40691  cdleme21c 40692  cdleme21ct 40694  cdleme21f 40697  cdleme21g 40698  cdleme21h 40699  cdleme21i 40700  cdleme22gb 40659
[Crawley] p. 116Lemma Fcdlemf 40928  cdlemf1 40926  cdlemf2 40927
[Crawley] p. 116Lemma Gcdlemftr1 40932  cdlemg16 41022  cdlemg28 41069  cdlemg28a 41058  cdlemg28b 41068  cdlemg3a 40962  cdlemg42 41094  cdlemg43 41095  cdlemg44 41098  cdlemg44a 41096  cdlemg46 41100  cdlemg47 41101  cdlemg9 40999  ltrnco 41084  ltrncom 41103  tgrpabl 41116  trlco 41092
[Crawley] p. 116Definition of Gdf-tgrp 41108
[Crawley] p. 117Lemma Gcdlemg17 41042  cdlemg17b 41027
[Crawley] p. 117Definition of Edf-edring-rN 41121  df-edring 41122
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41125
[Crawley] p. 118Remarktendopltp 41145
[Crawley] p. 118Lemma Hcdlemh 41182  cdlemh1 41180  cdlemh2 41181
[Crawley] p. 118Lemma Icdlemi 41185  cdlemi1 41183  cdlemi2 41184
[Crawley] p. 118Lemma Jcdlemj1 41186  cdlemj2 41187  cdlemj3 41188  tendocan 41189
[Crawley] p. 118Lemma Kcdlemk 41339  cdlemk1 41196  cdlemk10 41208  cdlemk11 41214  cdlemk11t 41311  cdlemk11ta 41294  cdlemk11tb 41296  cdlemk11tc 41310  cdlemk11u-2N 41254  cdlemk11u 41236  cdlemk12 41215  cdlemk12u-2N 41255  cdlemk12u 41237  cdlemk13-2N 41241  cdlemk13 41217  cdlemk14-2N 41243  cdlemk14 41219  cdlemk15-2N 41244  cdlemk15 41220  cdlemk16-2N 41245  cdlemk16 41222  cdlemk16a 41221  cdlemk17-2N 41246  cdlemk17 41223  cdlemk18-2N 41251  cdlemk18-3N 41265  cdlemk18 41233  cdlemk19-2N 41252  cdlemk19 41234  cdlemk19u 41335  cdlemk1u 41224  cdlemk2 41197  cdlemk20-2N 41257  cdlemk20 41239  cdlemk21-2N 41256  cdlemk21N 41238  cdlemk22-3 41266  cdlemk22 41258  cdlemk23-3 41267  cdlemk24-3 41268  cdlemk25-3 41269  cdlemk26-3 41271  cdlemk26b-3 41270  cdlemk27-3 41272  cdlemk28-3 41273  cdlemk29-3 41276  cdlemk3 41198  cdlemk30 41259  cdlemk31 41261  cdlemk32 41262  cdlemk33N 41274  cdlemk34 41275  cdlemk35 41277  cdlemk36 41278  cdlemk37 41279  cdlemk38 41280  cdlemk39 41281  cdlemk39u 41333  cdlemk4 41199  cdlemk41 41285  cdlemk42 41306  cdlemk42yN 41309  cdlemk43N 41328  cdlemk45 41312  cdlemk46 41313  cdlemk47 41314  cdlemk48 41315  cdlemk49 41316  cdlemk5 41201  cdlemk50 41317  cdlemk51 41318  cdlemk52 41319  cdlemk53 41322  cdlemk54 41323  cdlemk55 41326  cdlemk55u 41331  cdlemk56 41336  cdlemk5a 41200  cdlemk5auN 41225  cdlemk5u 41226  cdlemk6 41202  cdlemk6u 41227  cdlemk7 41213  cdlemk7u-2N 41253  cdlemk7u 41235  cdlemk8 41203  cdlemk9 41204  cdlemk9bN 41205  cdlemki 41206  cdlemkid 41301  cdlemkj-2N 41247  cdlemkj 41228  cdlemksat 41211  cdlemksel 41210  cdlemksv 41209  cdlemksv2 41212  cdlemkuat 41231  cdlemkuel-2N 41249  cdlemkuel-3 41263  cdlemkuel 41230  cdlemkuv-2N 41248  cdlemkuv2-2 41250  cdlemkuv2-3N 41264  cdlemkuv2 41232  cdlemkuvN 41229  cdlemkvcl 41207  cdlemky 41291  cdlemkyyN 41327  tendoex 41340
[Crawley] p. 120Remarkdva1dim 41350
[Crawley] p. 120Lemma Lcdleml1N 41341  cdleml2N 41342  cdleml3N 41343  cdleml4N 41344  cdleml5N 41345  cdleml6 41346  cdleml7 41347  cdleml8 41348  cdleml9 41349  dia1dim 41426
[Crawley] p. 120Lemma Mdia11N 41413  diaf11N 41414  dialss 41411  diaord 41412  dibf11N 41526  djajN 41502
[Crawley] p. 120Definition of isomorphism mapdiaval 41397
[Crawley] p. 121Lemma Mcdlemm10N 41483  dia2dimlem1 41429  dia2dimlem2 41430  dia2dimlem3 41431  dia2dimlem4 41432  dia2dimlem5 41433  diaf1oN 41495  diarnN 41494  dvheveccl 41477  dvhopN 41481
[Crawley] p. 121Lemma Ncdlemn 41577  cdlemn10 41571  cdlemn11 41576  cdlemn11a 41572  cdlemn11b 41573  cdlemn11c 41574  cdlemn11pre 41575  cdlemn2 41560  cdlemn2a 41561  cdlemn3 41562  cdlemn4 41563  cdlemn4a 41564  cdlemn5 41566  cdlemn5pre 41565  cdlemn6 41567  cdlemn7 41568  cdlemn8 41569  cdlemn9 41570  diclspsn 41559
[Crawley] p. 121Definition of phi(q)df-dic 41538
[Crawley] p. 122Lemma Ndih11 41630  dihf11 41632  dihjust 41582  dihjustlem 41581  dihord 41629  dihord1 41583  dihord10 41588  dihord11b 41587  dihord11c 41589  dihord2 41592  dihord2a 41584  dihord2b 41585  dihord2cN 41586  dihord2pre 41590  dihord2pre2 41591  dihordlem6 41578  dihordlem7 41579  dihordlem7b 41580
[Crawley] p. 122Definition of isomorphism mapdihffval 41595  dihfval 41596  dihval 41597
[Diestel] p. 3Definitiondf-gric 48230  df-grim 48227  isuspgrim 48245
[Diestel] p. 3Section 1.1df-cusgr 29497  df-nbgr 29418
[Diestel] p. 3Definition by df-grisom 48226
[Diestel] p. 4Section 1.1df-isubgr 48210  df-subgr 29353  uhgrspan1 29388  uhgrspansubgr 29376
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29640  vtxdgoddnumeven 29639
[Diestel] p. 27Section 1.10df-ushgr 29144
[EGA] p. 80Notation 1.1.1rspecval 34041
[EGA] p. 80Proposition 1.1.2zartop 34053
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34045  zarcls1 34046
[EGA] p. 81Corollary 1.1.8zart0 34056
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34059
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34062
[Eisenberg] p. 67Definition 5.3df-dif 3906
[Eisenberg] p. 82Definition 6.3dfom3 9568
[Eisenberg] p. 125Definition 8.21df-map 8777
[Eisenberg] p. 216Example 13.2(4)omenps 9576
[Eisenberg] p. 310Theorem 19.8cardprc 9904
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10477
[Enderton] p. 18Axiom of Empty Setaxnul 5252
[Enderton] p. 19Definitiondf-tp 4587
[Enderton] p. 26Exercise 5unissb 4898
[Enderton] p. 26Exercise 10pwel 5328
[Enderton] p. 28Exercise 7(b)pwun 5525
[Enderton] p. 30Theorem "Distributive laws"iinin1 5036  iinin2 5035  iinun2 5030  iunin1 5029  iunin1f 32643  iunin2 5028  uniin1 32637  uniin2 32638
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5034  iundif2 5031
[Enderton] p. 32Exercise 20unineq 4242
[Enderton] p. 33Exercise 23iinuni 5055
[Enderton] p. 33Exercise 25iununi 5056
[Enderton] p. 33Exercise 24(a)iinpw 5063
[Enderton] p. 33Exercise 24(b)iunpw 7726  iunpwss 5064
[Enderton] p. 36Definitionopthwiener 5470
[Enderton] p. 38Exercise 6(a)unipw 5405
[Enderton] p. 38Exercise 6(b)pwuni 4903
[Enderton] p. 41Lemma 3Dopeluu 5426  rnex 7862  rnexg 7854
[Enderton] p. 41Exercise 8dmuni 5871  rnuni 6114
[Enderton] p. 42Definition of a functiondffun7 6527  dffun8 6528
[Enderton] p. 43Definition of function valuefunfv2 6930
[Enderton] p. 43Definition of single-rootedfuncnv 6569
[Enderton] p. 44Definition (d)dfima2 6029  dfima3 6030
[Enderton] p. 47Theorem 3Hfvco2 6939
[Enderton] p. 49Axiom of Choice (first form)ac7 10395  ac7g 10396  df-ac 10038  dfac2 10054  dfac2a 10052  dfac2b 10053  dfac3 10043  dfac7 10055
[Enderton] p. 50Theorem 3K(a)imauni 7202
[Enderton] p. 52Definitiondf-map 8777
[Enderton] p. 53Exercise 21coass 6232
[Enderton] p. 53Exercise 27dmco 6221
[Enderton] p. 53Exercise 14(a)funin 6576
[Enderton] p. 53Exercise 22(a)imass2 6069
[Enderton] p. 54Remarkixpf 8870  ixpssmap 8882
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8848
[Enderton] p. 55Axiom of Choice (second form)ac9 10405  ac9s 10415
[Enderton] p. 56Theorem 3Meqvrelref 38934  erref 8666
[Enderton] p. 57Lemma 3Neqvrelthi 38937  erthi 8702
[Enderton] p. 57Definitiondf-ec 8647
[Enderton] p. 58Definitiondf-qs 8651
[Enderton] p. 61Exercise 35df-ec 8647
[Enderton] p. 65Exercise 56(a)dmun 5867
[Enderton] p. 68Definition of successordf-suc 6331
[Enderton] p. 71Definitiondf-tr 5208  dftr4 5213
[Enderton] p. 72Theorem 4Eunisuc 6406  unisucg 6405
[Enderton] p. 73Exercise 6unisuc 6406  unisucg 6405
[Enderton] p. 73Exercise 5(a)truni 5222
[Enderton] p. 73Exercise 5(b)trint 5224  trintALT 45225
[Enderton] p. 79Theorem 4I(A1)nna0 8542
[Enderton] p. 79Theorem 4I(A2)nnasuc 8544  onasuc 8465
[Enderton] p. 79Definition of operation valuedf-ov 7371
[Enderton] p. 80Theorem 4J(A1)nnm0 8543
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8545  onmsuc 8466
[Enderton] p. 81Theorem 4K(1)nnaass 8560
[Enderton] p. 81Theorem 4K(2)nna0r 8547  nnacom 8555
[Enderton] p. 81Theorem 4K(3)nndi 8561
[Enderton] p. 81Theorem 4K(4)nnmass 8562
[Enderton] p. 81Theorem 4K(5)nnmcom 8564
[Enderton] p. 82Exercise 16nnm0r 8548  nnmsucr 8563
[Enderton] p. 88Exercise 23nnaordex 8576
[Enderton] p. 129Definitiondf-en 8896
[Enderton] p. 132Theorem 6B(b)canth 7322
[Enderton] p. 133Exercise 1xpomen 9937
[Enderton] p. 133Exercise 2qnnen 16150
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9143
[Enderton] p. 135Corollary 6Cphp3 9145
[Enderton] p. 136Corollary 6Enneneq 9142
[Enderton] p. 136Corollary 6D(a)pssinf 9174
[Enderton] p. 136Corollary 6D(b)ominf 9176
[Enderton] p. 137Lemma 6Fpssnn 9105
[Enderton] p. 138Corollary 6Gssfi 9109
[Enderton] p. 139Theorem 6H(c)mapen 9081
[Enderton] p. 142Theorem 6I(3)xpdjuen 10102
[Enderton] p. 142Theorem 6I(4)mapdjuen 10103
[Enderton] p. 143Theorem 6Jdju0en 10098  dju1en 10094
[Enderton] p. 144Exercise 13iunfi 9255  unifi 9256  unifi2 9257
[Enderton] p. 144Corollary 6Kundif2 4431  unfi 9107  unfi2 9222
[Enderton] p. 145Figure 38ffoss 7900
[Enderton] p. 145Definitiondf-dom 8897
[Enderton] p. 146Example 1domen 8910  domeng 8911
[Enderton] p. 146Example 3nndomo 9154  nnsdom 9575  nnsdomg 9211
[Enderton] p. 149Theorem 6L(a)djudom2 10106
[Enderton] p. 149Theorem 6L(c)mapdom1 9082  xpdom1 9016  xpdom1g 9014  xpdom2g 9013
[Enderton] p. 149Theorem 6L(d)mapdom2 9088
[Enderton] p. 151Theorem 6Mzorn 10429  zorng 10426
[Enderton] p. 151Theorem 6M(4)ac8 10414  dfac5 10051
[Enderton] p. 159Theorem 6Qunictb 10498
[Enderton] p. 164Exampleinfdif 10130
[Enderton] p. 168Definitiondf-po 5540
[Enderton] p. 192Theorem 7M(a)oneli 6440
[Enderton] p. 192Theorem 7M(b)ontr1 6372
[Enderton] p. 192Theorem 7M(c)onirri 6439
[Enderton] p. 193Corollary 7N(b)0elon 6380
[Enderton] p. 193Corollary 7N(c)onsuci 7791
[Enderton] p. 193Corollary 7N(d)ssonunii 7736
[Enderton] p. 194Remarkonprc 7733
[Enderton] p. 194Exercise 16suc11 6434
[Enderton] p. 197Definitiondf-card 9863
[Enderton] p. 197Theorem 7Pcarden 10473
[Enderton] p. 200Exercise 25tfis 7807
[Enderton] p. 202Lemma 7Tr1tr 9700
[Enderton] p. 202Definitiondf-r1 9688
[Enderton] p. 202Theorem 7Qr1val1 9710
[Enderton] p. 204Theorem 7V(b)rankval4 9791  rankval4b 35275
[Enderton] p. 206Theorem 7X(b)en2lp 9527
[Enderton] p. 207Exercise 30rankpr 9781  rankprb 9775  rankpw 9767  rankpwi 9747  rankuniss 9790
[Enderton] p. 207Exercise 34opthreg 9539
[Enderton] p. 208Exercise 35suc11reg 9540
[Enderton] p. 212Definition of alephalephval3 10032
[Enderton] p. 213Theorem 8A(a)alephord2 9998
[Enderton] p. 213Theorem 8A(b)cardalephex 10012
[Enderton] p. 218Theorem Schema 8Eonfununi 8283
[Enderton] p. 222Definition of kardkarden 9819  kardex 9818
[Enderton] p. 238Theorem 8Roeoa 8535
[Enderton] p. 238Theorem 8Soeoe 8537
[Enderton] p. 240Exercise 25oarec 8499
[Enderton] p. 257Definition of cofinalitycflm 10172
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17577
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17519
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18488  mrieqv2d 17574  mrieqvd 17573
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17578
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17583  mreexexlem2d 17580
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18494  mreexfidimd 17585
[Frege1879] p. 11Statementdf3or2 44113
[Frege1879] p. 12Statementdf3an2 44114  dfxor4 44111  dfxor5 44112
[Frege1879] p. 26Axiom 1ax-frege1 44135
[Frege1879] p. 26Axiom 2ax-frege2 44136
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44140
[Frege1879] p. 31Proposition 4frege4 44144
[Frege1879] p. 32Proposition 5frege5 44145
[Frege1879] p. 33Proposition 6frege6 44151
[Frege1879] p. 34Proposition 7frege7 44153
[Frege1879] p. 35Axiom 8ax-frege8 44154  axfrege8 44152
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37689
[Frege1879] p. 35Proposition 9frege9 44157
[Frege1879] p. 36Proposition 10frege10 44165
[Frege1879] p. 36Proposition 11frege11 44159
[Frege1879] p. 37Proposition 12frege12 44158
[Frege1879] p. 37Proposition 13frege13 44167
[Frege1879] p. 37Proposition 14frege14 44168
[Frege1879] p. 38Proposition 15frege15 44171
[Frege1879] p. 38Proposition 16frege16 44161
[Frege1879] p. 39Proposition 17frege17 44166
[Frege1879] p. 39Proposition 18frege18 44163
[Frege1879] p. 39Proposition 19frege19 44169
[Frege1879] p. 40Proposition 20frege20 44173
[Frege1879] p. 40Proposition 21frege21 44172
[Frege1879] p. 41Proposition 22frege22 44164
[Frege1879] p. 42Proposition 23frege23 44170
[Frege1879] p. 42Proposition 24frege24 44160
[Frege1879] p. 42Proposition 25frege25 44162  rp-frege25 44150
[Frege1879] p. 42Proposition 26frege26 44155
[Frege1879] p. 43Axiom 28ax-frege28 44175
[Frege1879] p. 43Proposition 27frege27 44156
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 44176
[Frege1879] p. 44Axiom 31ax-frege31 44179  axfrege31 44178
[Frege1879] p. 44Proposition 30frege30 44177
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 44180
[Frege1879] p. 44Proposition 33frege33 44181
[Frege1879] p. 45Proposition 34frege34 44182
[Frege1879] p. 45Proposition 35frege35 44183
[Frege1879] p. 45Proposition 36frege36 44184
[Frege1879] p. 46Proposition 37frege37 44185
[Frege1879] p. 46Proposition 38frege38 44186
[Frege1879] p. 46Proposition 39frege39 44187
[Frege1879] p. 46Proposition 40frege40 44188
[Frege1879] p. 47Axiom 41ax-frege41 44190  axfrege41 44189
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 44191
[Frege1879] p. 47Proposition 43frege43 44192
[Frege1879] p. 47Proposition 44frege44 44193
[Frege1879] p. 47Proposition 45frege45 44194
[Frege1879] p. 48Proposition 46frege46 44195
[Frege1879] p. 48Proposition 47frege47 44196
[Frege1879] p. 49Proposition 48frege48 44197
[Frege1879] p. 49Proposition 49frege49 44198
[Frege1879] p. 49Proposition 50frege50 44199
[Frege1879] p. 50Axiom 52ax-frege52a 44202  ax-frege52c 44233  frege52aid 44203  frege52b 44234
[Frege1879] p. 50Axiom 54ax-frege54a 44207  ax-frege54c 44237  frege54b 44238
[Frege1879] p. 50Proposition 51frege51 44200
[Frege1879] p. 50Proposition 52dfsbcq 3744
[Frege1879] p. 50Proposition 53frege53a 44205  frege53aid 44204  frege53b 44235  frege53c 44259
[Frege1879] p. 50Proposition 54biid 261  eqid 2737
[Frege1879] p. 50Proposition 55frege55a 44213  frege55aid 44210  frege55b 44242  frege55c 44263  frege55cor1a 44214  frege55lem2a 44212  frege55lem2b 44241  frege55lem2c 44262
[Frege1879] p. 50Proposition 56frege56a 44216  frege56aid 44215  frege56b 44243  frege56c 44264
[Frege1879] p. 51Axiom 58ax-frege58a 44220  ax-frege58b 44246  frege58bid 44247  frege58c 44266
[Frege1879] p. 51Proposition 57frege57a 44218  frege57aid 44217  frege57b 44244  frege57c 44265
[Frege1879] p. 51Proposition 58spsbc 3755
[Frege1879] p. 51Proposition 59frege59a 44222  frege59b 44249  frege59c 44267
[Frege1879] p. 52Proposition 60frege60a 44223  frege60b 44250  frege60c 44268
[Frege1879] p. 52Proposition 61frege61a 44224  frege61b 44251  frege61c 44269
[Frege1879] p. 52Proposition 62frege62a 44225  frege62b 44252  frege62c 44270
[Frege1879] p. 52Proposition 63frege63a 44226  frege63b 44253  frege63c 44271
[Frege1879] p. 53Proposition 64frege64a 44227  frege64b 44254  frege64c 44272
[Frege1879] p. 53Proposition 65frege65a 44228  frege65b 44255  frege65c 44273
[Frege1879] p. 54Proposition 66frege66a 44229  frege66b 44256  frege66c 44274
[Frege1879] p. 54Proposition 67frege67a 44230  frege67b 44257  frege67c 44275
[Frege1879] p. 54Proposition 68frege68a 44231  frege68b 44258  frege68c 44276
[Frege1879] p. 55Definition 69dffrege69 44277
[Frege1879] p. 58Proposition 70frege70 44278
[Frege1879] p. 59Proposition 71frege71 44279
[Frege1879] p. 59Proposition 72frege72 44280
[Frege1879] p. 59Proposition 73frege73 44281
[Frege1879] p. 60Definition 76dffrege76 44284
[Frege1879] p. 60Proposition 74frege74 44282
[Frege1879] p. 60Proposition 75frege75 44283
[Frege1879] p. 62Proposition 77frege77 44285  frege77d 44091
[Frege1879] p. 63Proposition 78frege78 44286
[Frege1879] p. 63Proposition 79frege79 44287
[Frege1879] p. 63Proposition 80frege80 44288
[Frege1879] p. 63Proposition 81frege81 44289  frege81d 44092
[Frege1879] p. 64Proposition 82frege82 44290
[Frege1879] p. 65Proposition 83frege83 44291  frege83d 44093
[Frege1879] p. 65Proposition 84frege84 44292
[Frege1879] p. 66Proposition 85frege85 44293
[Frege1879] p. 66Proposition 86frege86 44294
[Frege1879] p. 66Proposition 87frege87 44295  frege87d 44095
[Frege1879] p. 67Proposition 88frege88 44296
[Frege1879] p. 68Proposition 89frege89 44297
[Frege1879] p. 68Proposition 90frege90 44298
[Frege1879] p. 68Proposition 91frege91 44299  frege91d 44096
[Frege1879] p. 69Proposition 92frege92 44300
[Frege1879] p. 70Proposition 93frege93 44301
[Frege1879] p. 70Proposition 94frege94 44302
[Frege1879] p. 70Proposition 95frege95 44303
[Frege1879] p. 71Definition 99dffrege99 44307
[Frege1879] p. 71Proposition 96frege96 44304  frege96d 44094
[Frege1879] p. 71Proposition 97frege97 44305  frege97d 44097
[Frege1879] p. 71Proposition 98frege98 44306  frege98d 44098
[Frege1879] p. 72Proposition 100frege100 44308
[Frege1879] p. 72Proposition 101frege101 44309
[Frege1879] p. 72Proposition 102frege102 44310  frege102d 44099
[Frege1879] p. 73Proposition 103frege103 44311
[Frege1879] p. 73Proposition 104frege104 44312
[Frege1879] p. 73Proposition 105frege105 44313
[Frege1879] p. 73Proposition 106frege106 44314  frege106d 44100
[Frege1879] p. 74Proposition 107frege107 44315
[Frege1879] p. 74Proposition 108frege108 44316  frege108d 44101
[Frege1879] p. 74Proposition 109frege109 44317  frege109d 44102
[Frege1879] p. 75Proposition 110frege110 44318
[Frege1879] p. 75Proposition 111frege111 44319  frege111d 44104
[Frege1879] p. 76Proposition 112frege112 44320
[Frege1879] p. 76Proposition 113frege113 44321
[Frege1879] p. 76Proposition 114frege114 44322  frege114d 44103
[Frege1879] p. 77Definition 115dffrege115 44323
[Frege1879] p. 77Proposition 116frege116 44324
[Frege1879] p. 78Proposition 117frege117 44325
[Frege1879] p. 78Proposition 118frege118 44326
[Frege1879] p. 78Proposition 119frege119 44327
[Frege1879] p. 78Proposition 120frege120 44328
[Frege1879] p. 79Proposition 121frege121 44329
[Frege1879] p. 79Proposition 122frege122 44330  frege122d 44105
[Frege1879] p. 79Proposition 123frege123 44331
[Frege1879] p. 80Proposition 124frege124 44332  frege124d 44106
[Frege1879] p. 81Proposition 125frege125 44333
[Frege1879] p. 81Proposition 126frege126 44334  frege126d 44107
[Frege1879] p. 82Proposition 127frege127 44335
[Frege1879] p. 83Proposition 128frege128 44336
[Frege1879] p. 83Proposition 129frege129 44337  frege129d 44108
[Frege1879] p. 84Proposition 130frege130 44338
[Frege1879] p. 85Proposition 131frege131 44339  frege131d 44109
[Frege1879] p. 86Proposition 132frege132 44340
[Frege1879] p. 86Proposition 133frege133 44341  frege133d 44110
[Fremlin1] p. 13Definition 111G (b)df-salgen 46660
[Fremlin1] p. 13Definition 111G (d)borelmbl 46983
[Fremlin1] p. 13Proposition 111G (b)salgenss 46683
[Fremlin1] p. 14Definition 112Aismea 46798
[Fremlin1] p. 15Remark 112B (d)psmeasure 46818
[Fremlin1] p. 15Property 112C (a)meadjun 46809  meadjunre 46823
[Fremlin1] p. 15Property 112C (b)meassle 46810
[Fremlin1] p. 15Property 112C (c)meaunle 46811
[Fremlin1] p. 16Property 112C (d)iundjiun 46807  meaiunle 46816  meaiunlelem 46815
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46828  meaiuninc2 46829  meaiuninc3 46832  meaiuninc3v 46831  meaiunincf 46830  meaiuninclem 46827
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46834  meaiininc2 46835  meaiininclem 46833
[Fremlin1] p. 19Theorem 113Ccaragen0 46853  caragendifcl 46861  caratheodory 46875  omelesplit 46865
[Fremlin1] p. 19Definition 113Aisome 46841  isomennd 46878  isomenndlem 46877
[Fremlin1] p. 19Remark 113B (c)omeunle 46863
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46882  voncmpl 46968
[Fremlin1] p. 19Definition 113A (ii)omessle 46845
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46870  carageniuncllem1 46868  carageniuncllem2 46869  caragenuncl 46860  caragenuncllem 46859  caragenunicl 46871
[Fremlin1] p. 21Remark 113Dcaragenel2d 46879
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46873  caratheodorylem2 46874
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46882
[Fremlin1] p. 23Lemma 114Bhoidmv1le 46941  hoidmv1lelem1 46938  hoidmv1lelem2 46939  hoidmv1lelem3 46940
[Fremlin1] p. 25Definition 114Eisvonmbl 46985
[Fremlin1] p. 29Lemma 115Bhoidmv1le 46941  hoidmvle 46947  hoidmvlelem1 46942  hoidmvlelem2 46943  hoidmvlelem3 46944  hoidmvlelem4 46945  hoidmvlelem5 46946  hsphoidmvle2 46932  hsphoif 46923  hsphoival 46926
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46895
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46903
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 46930  hoidmvn0val 46931  hoidmvval 46924  hoidmvval0 46934  hoidmvval0b 46937
[Fremlin1] p. 30Lemma 115Bhoiprodp1 46935  hsphoidmvle 46933
[Fremlin1] p. 30Definition 115Cdf-ovoln 46884  df-voln 46886
[Fremlin1] p. 30Proposition 115D (a)dmovn 46951  ovn0 46913  ovn0lem 46912  ovnf 46910  ovnome 46920  ovnssle 46908  ovnsslelem 46907  ovnsupge0 46904
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 46950  ovnhoilem1 46948  ovnhoilem2 46949  vonhoi 47014
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 46967  hoidifhspf 46965  hoidifhspval 46955  hoidifhspval2 46962  hoidifhspval3 46966  hspmbl 46976  hspmbllem1 46973  hspmbllem2 46974  hspmbllem3 46975
[Fremlin1] p. 31Definition 115Evoncmpl 46968  vonmea 46921
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 46919  ovnsubadd2 46993  ovnsubadd2lem 46992  ovnsubaddlem1 46917  ovnsubaddlem2 46918
[Fremlin1] p. 32Proposition 115G (a)hoimbl 46978  hoimbl2 47012  hoimbllem 46977  hspdifhsp 46963  opnvonmbl 46981  opnvonmbllem2 46980
[Fremlin1] p. 32Proposition 115G (b)borelmbl 46983
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47026  iccvonmbllem 47025  ioovonmbl 47024
[Fremlin1] p. 32Proposition 115G (d)vonicc 47032  vonicclem2 47031  vonioo 47029  vonioolem2 47028  vonn0icc 47035  vonn0icc2 47039  vonn0ioo 47034  vonn0ioo2 47037
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47036  snvonmbl 47033  vonct 47040  vonsn 47038
[Fremlin1] p. 35Lemma 121Asubsalsal 46706
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46705  subsaliuncllem 46704
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47072  salpreimalegt 47056  salpreimaltle 47073
[Fremlin1] p. 35Proposition 121B (i)issmf 47075  issmff 47081  issmflem 47074
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47092  issmflelem 47091  smfpreimale 47101
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47103  issmfgtlem 47102
[Fremlin1] p. 36Definition 121Cdf-smblfn 47043  issmf 47075  issmff 47081  issmfge 47117  issmfgelem 47116  issmfgt 47103  issmfgtlem 47102  issmfle 47092  issmflelem 47091  issmflem 47074
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47054  salpreimagtlt 47077  salpreimalelt 47076
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47117  issmfgelem 47116
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47100
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47098  cnfsmf 47087
[Fremlin1] p. 36Proposition 121D (c)decsmf 47114  decsmflem 47113  incsmf 47089  incsmflem 47088
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47048  pimconstlt1 47049  smfconst 47096
[Fremlin1] p. 37Proposition 121E (b)smfadd 47112  smfaddlem1 47110  smfaddlem2 47111
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47143
[Fremlin1] p. 37Proposition 121E (d)smfmul 47142  smfmullem1 47138  smfmullem2 47139  smfmullem3 47140  smfmullem4 47141
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47144
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47147  smfpimbor1lem2 47146
[Fremlin1] p. 37Proposition 121E (g)smfco 47149
[Fremlin1] p. 37Proposition 121E (h)smfres 47137
[Fremlin1] p. 38Proposition 121E (e)smfrec 47136
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47145  smfresal 47135
[Fremlin1] p. 38Proposition 121F (a)smflim 47124  smflim2 47153  smflimlem1 47118  smflimlem2 47119  smflimlem3 47120  smflimlem4 47121  smflimlem5 47122  smflimlem6 47123  smflimmpt 47157
[Fremlin1] p. 38Proposition 121F (b)smfsup 47161  smfsuplem1 47158  smfsuplem2 47159  smfsuplem3 47160  smfsupmpt 47162  smfsupxr 47163
[Fremlin1] p. 38Proposition 121F (c)smfinf 47165  smfinflem 47164  smfinfmpt 47166
[Fremlin1] p. 39Remark 121Gsmflim 47124  smflim2 47153  smflimmpt 47157
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47155
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47185  smfdivdmmbl2 47188  smfinfdmmbl 47196  smfinfdmmbllem 47195  smfsupdmmbl 47192  smfsupdmmbllem 47191
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47175  smflimsuplem2 47168  smflimsuplem6 47172  smflimsuplem7 47173  smflimsuplem8 47174  smflimsupmpt 47176
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47178  smfliminflem 47177  smfliminfmpt 47179
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47043
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47189  fsupdm2 47190
[Fremlin1], p. 39Proposition 121Hadddmmbl 47180  adddmmbl2 47181  finfdm 47193  finfdm2 47194  fsupdm 47189  fsupdm2 47190  muldmmbl 47182  muldmmbl2 47183
[Fremlin1], p. 39Proposition 121F (c)finfdm 47193  finfdm2 47194
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25505
[Fremlin5] p. 213Lemma 565Cauniioovol 25548
[Fremlin5] p. 214Lemma 565Cauniioombl 25558
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 37938
[Fremlin5] p. 220Theorem 565Maftc1anc 37941
[FreydScedrov] p. 283Axiom of Infinityax-inf 9559  inf1 9543  inf2 9544
[Gleason] p. 117Proposition 9-2.1df-enq 10834  enqer 10844
[Gleason] p. 117Proposition 9-2.2df-1nq 10839  df-nq 10835
[Gleason] p. 117Proposition 9-2.3df-plpq 10831  df-plq 10837
[Gleason] p. 119Proposition 9-2.4caovmo 7605  df-mpq 10832  df-mq 10838
[Gleason] p. 119Proposition 9-2.5df-rq 10840
[Gleason] p. 119Proposition 9-2.6ltexnq 10898
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10899  ltbtwnnq 10901
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10894
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10895
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10902
[Gleason] p. 121Definition 9-3.1df-np 10904
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10916
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10918
[Gleason] p. 122Definitiondf-1p 10905
[Gleason] p. 122Remark (1)prub 10917
[Gleason] p. 122Lemma 9-3.4prlem934 10956
[Gleason] p. 122Proposition 9-3.2df-ltp 10908
[Gleason] p. 122Proposition 9-3.3ltsopr 10955  psslinpr 10954  supexpr 10977  suplem1pr 10975  suplem2pr 10976
[Gleason] p. 123Proposition 9-3.5addclpr 10941  addclprlem1 10939  addclprlem2 10940  df-plp 10906
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10945
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10944
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10957
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10966  ltexprlem1 10959  ltexprlem2 10960  ltexprlem3 10961  ltexprlem4 10962  ltexprlem5 10963  ltexprlem6 10964  ltexprlem7 10965
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10968  ltaprlem 10967
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10969
[Gleason] p. 124Lemma 9-3.6prlem936 10970
[Gleason] p. 124Proposition 9-3.7df-mp 10907  mulclpr 10943  mulclprlem 10942  reclem2pr 10971
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10952
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10947
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10946
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10951
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10974  reclem3pr 10972  reclem4pr 10973
[Gleason] p. 126Proposition 9-4.1df-enr 10978  enrer 10986
[Gleason] p. 126Proposition 9-4.2df-0r 10983  df-1r 10984  df-nr 10979
[Gleason] p. 126Proposition 9-4.3df-mr 10981  df-plr 10980  negexsr 11025  recexsr 11030  recexsrlem 11026
[Gleason] p. 127Proposition 9-4.4df-ltr 10982
[Gleason] p. 130Proposition 10-1.3creui 12152  creur 12151  cru 12149
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11111  axcnre 11087
[Gleason] p. 132Definition 10-3.1crim 15050  crimd 15167  crimi 15128  crre 15049  crred 15166  crrei 15127
[Gleason] p. 132Definition 10-3.2remim 15052  remimd 15133
[Gleason] p. 133Definition 10.36absval2 15219  absval2d 15383  absval2i 15333
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15076  cjaddd 15155  cjaddi 15123
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15077  cjmuld 15156  cjmuli 15124
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15075  cjcjd 15134  cjcji 15106
[Gleason] p. 133Proposition 10-3.4(f)cjre 15074  cjreb 15058  cjrebd 15137  cjrebi 15109  cjred 15161  rere 15057  rereb 15055  rerebd 15136  rerebi 15108  rered 15159
[Gleason] p. 133Proposition 10-3.4(h)addcj 15083  addcjd 15147  addcji 15118
[Gleason] p. 133Proposition 10-3.7(a)absval 15173
[Gleason] p. 133Proposition 10-3.7(b)abscj 15214  abscjd 15388  abscji 15337
[Gleason] p. 133Proposition 10-3.7(c)abs00 15224  abs00d 15384  abs00i 15334  absne0d 15385
[Gleason] p. 133Proposition 10-3.7(d)releabs 15257  releabsd 15389  releabsi 15338
[Gleason] p. 133Proposition 10-3.7(f)absmul 15229  absmuld 15392  absmuli 15340
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15217  sqabsaddi 15341
[Gleason] p. 133Proposition 10-3.7(h)abstri 15266  abstrid 15394  abstrii 15344
[Gleason] p. 134Definition 10-4.1df-exp 13997  exp0 14000  expp1 14003  expp1d 14082
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26656  cxpaddd 26694  expadd 14039  expaddd 14083  expaddz 14041
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26665  cxpmuld 26714  expmul 14042  expmuld 14084  expmulz 14043
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26662  mulcxpd 26705  mulexp 14036  mulexpd 14096  mulexpz 14037
[Gleason] p. 140Exercise 1znnen 16149
[Gleason] p. 141Definition 11-2.1fzval 13437
[Gleason] p. 168Proposition 12-2.1(a)climadd 15567  rlimadd 15578  rlimdiv 15581
[Gleason] p. 168Proposition 12-2.1(b)climsub 15569  rlimsub 15579
[Gleason] p. 168Proposition 12-2.1(c)climmul 15568  rlimmul 15580
[Gleason] p. 171Corollary 12-2.2climmulc2 15572
[Gleason] p. 172Corollary 12-2.5climrecl 15518
[Gleason] p. 172Proposition 12-2.4(c)climabs 15539  climcj 15540  climim 15542  climre 15541  rlimabs 15544  rlimcj 15545  rlimim 15547  rlimre 15546
[Gleason] p. 173Definition 12-3.1df-ltxr 11183  df-xr 11182  ltxr 13041
[Gleason] p. 175Definition 12-4.1df-limsup 15406  limsupval 15409
[Gleason] p. 180Theorem 12-5.1climsup 15605
[Gleason] p. 180Theorem 12-5.3caucvg 15614  caucvgb 15615  caucvgbf 45836  caucvgr 15611  climcau 15606
[Gleason] p. 182Exercise 3cvgcmp 15751
[Gleason] p. 182Exercise 4cvgrat 15818
[Gleason] p. 195Theorem 13-2.12abs1m 15271
[Gleason] p. 217Lemma 13-4.1btwnzge0 13760
[Gleason] p. 223Definition 14-1.1df-met 21315
[Gleason] p. 223Definition 14-1.1(a)met0 24299  xmet0 24298
[Gleason] p. 223Definition 14-1.1(b)metgt0 24315
[Gleason] p. 223Definition 14-1.1(c)metsym 24306
[Gleason] p. 223Definition 14-1.1(d)mettri 24308  mstri 24425  xmettri 24307  xmstri 24424
[Gleason] p. 225Definition 14-1.5xpsmet 24338
[Gleason] p. 230Proposition 14-2.6txlm 23604
[Gleason] p. 240Theorem 14-4.3metcnp4 25278
[Gleason] p. 240Proposition 14-4.2metcnp3 24496
[Gleason] p. 243Proposition 14-4.16addcn 24822  addcn2 15529  mulcn 24824  mulcn2 15531  subcn 24823  subcn2 15530
[Gleason] p. 295Remarkbcval3 14241  bcval4 14242
[Gleason] p. 295Equation 2bcpasc 14256
[Gleason] p. 295Definition of binomial coefficientbcval 14239  df-bc 14238
[Gleason] p. 296Remarkbcn0 14245  bcnn 14247
[Gleason] p. 296Theorem 15-2.8binom 15765
[Gleason] p. 308Equation 2ef0 16026
[Gleason] p. 308Equation 3efcj 16027
[Gleason] p. 309Corollary 15-4.3efne0 16033
[Gleason] p. 309Corollary 15-4.4efexp 16038
[Gleason] p. 310Equation 14sinadd 16101
[Gleason] p. 310Equation 15cosadd 16102
[Gleason] p. 311Equation 17sincossq 16113
[Gleason] p. 311Equation 18cosbnd 16118  sinbnd 16117
[Gleason] p. 311Lemma 15-4.7sqeqor 14151  sqeqori 14149
[Gleason] p. 311Definition of ` `df-pi 16007
[Godowski] p. 730Equation SFgoeqi 32360
[GodowskiGreechie] p. 249Equation IV3oai 31755
[Golan] p. 1Remarksrgisid 20156
[Golan] p. 1Definitiondf-srg 20134
[Golan] p. 149Definitiondf-slmd 33294
[Gonshor] p. 7Definitiondf-cuts 27768
[Gonshor] p. 9Theorem 2.5lesrec 27807  lesrecd 27808
[Gonshor] p. 10Theorem 2.6cofcut1 27928  cofcut1d 27929
[Gonshor] p. 10Theorem 2.7cofcut2 27930  cofcut2d 27931
[Gonshor] p. 12Theorem 2.9cofcutr 27932  cofcutr1d 27933  cofcutr2d 27934
[Gonshor] p. 13Definitiondf-adds 27968
[Gonshor] p. 14Theorem 3.1addsprop 27984
[Gonshor] p. 15Theorem 3.2addsunif 28010
[Gonshor] p. 17Theorem 3.4mulsprop 28138
[Gonshor] p. 18Theorem 3.5mulsunif 28158
[Gonshor] p. 28Lemma 4.2halfcut 28466
[Gonshor] p. 28Theorem 4.2pw2cut 28468
[Gonshor] p. 30Theorem 4.2addhalfcut 28467
[Gonshor] p. 39Theorem 4.4(b)elreno2 28503
[Gonshor] p. 95Theorem 6.1addbday 28026
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36372
[Gratzer] p. 23Section 0.6df-mre 17517
[Gratzer] p. 27Section 0.6df-mri 17519
[Hall] p. 1Section 1.1df-asslaw 48537  df-cllaw 48535  df-comlaw 48536
[Hall] p. 2Section 1.2df-clintop 48549
[Hall] p. 7Section 1.3df-sgrp2 48570
[Halmos] p. 28Partition ` `df-parts 39108  dfmembpart2 39113
[Halmos] p. 31Theorem 17.3riesz1 32152  riesz2 32153
[Halmos] p. 41Definition of Hermitianhmopadj2 32028
[Halmos] p. 42Definition of projector orderingpjordi 32260
[Halmos] p. 43Theorem 26.1elpjhmop 32272  elpjidm 32271  pjnmopi 32235
[Halmos] p. 44Remarkpjinormi 31774  pjinormii 31763
[Halmos] p. 44Theorem 26.2elpjch 32276  pjrn 31794  pjrni 31789  pjvec 31783
[Halmos] p. 44Theorem 26.3pjnorm2 31814
[Halmos] p. 44Theorem 26.4hmopidmpj 32241  hmopidmpji 32239
[Halmos] p. 45Theorem 27.1pjinvari 32278
[Halmos] p. 45Theorem 27.3pjoci 32267  pjocvec 31784
[Halmos] p. 45Theorem 27.4pjorthcoi 32256
[Halmos] p. 48Theorem 29.2pjssposi 32259
[Halmos] p. 48Theorem 29.3pjssdif1i 32262  pjssdif2i 32261
[Halmos] p. 50Definition of spectrumdf-spec 31942
[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 1797
[Hatcher] p. 25Definitiondf-phtpc 24959  df-phtpy 24938
[Hatcher] p. 26Definitiondf-pco 24973  df-pi1 24976
[Hatcher] p. 26Proposition 1.2phtpcer 24962
[Hatcher] p. 26Proposition 1.3pi1grp 25018
[Hefferon] p. 240Definition 3.12df-dmat 22446  df-dmatalt 48747
[Helfgott] p. 2Theoremtgoldbach 48166
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48151
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48163  bgoldbtbnd 48158  bgoldbtbnd 48158  tgblthelfgott 48164
[Helfgott] p. 5Proposition 1.1circlevma 34819
[Helfgott] p. 69Statement 7.49circlemethhgt 34820
[Helfgott] p. 69Statement 7.50hgt750lema 34834  hgt750lemb 34833  hgt750leme 34835  hgt750lemf 34830  hgt750lemg 34831
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48160  tgoldbachgt 34840  tgoldbachgtALTV 48161  tgoldbachgtd 34839
[Helfgott] p. 70Statement 7.49ax-hgt749 34821
[Herstein] p. 54Exercise 28df-grpo 30580
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18886  grpoideu 30596  mndideu 18682
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18916  grpoinveu 30606
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18947  grpo2inv 30618
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18960  grpoinvop 30620
[Herstein] p. 57Exercise 1dfgrp3e 18982
[Hitchcock] p. 5Rule A3mptnan 1770
[Hitchcock] p. 5Rule A4mptxor 1771
[Hitchcock] p. 5Rule A5mtpxor 1773
[Holland] p. 1519Theorem 2sumdmdi 32507
[Holland] p. 1520Lemma 5cdj1i 32520  cdj3i 32528  cdj3lem1 32521  cdjreui 32519
[Holland] p. 1524Lemma 7mddmdin0i 32518
[Holland95] p. 13Theorem 3.6hlathil 42326
[Holland95] p. 14Line 15hgmapvs 42256
[Holland95] p. 14Line 16hdmaplkr 42278
[Holland95] p. 14Line 17hdmapellkr 42279
[Holland95] p. 14Line 19hdmapglnm2 42276
[Holland95] p. 14Line 20hdmapip0com 42282
[Holland95] p. 14Theorem 3.6hdmapevec2 42201
[Holland95] p. 14Lines 24 and 25hdmapoc 42296
[Holland95] p. 204Definition of involutiondf-srng 20785
[Holland95] p. 212Definition of subspacedf-psubsp 39868
[Holland95] p. 214Lemma 3.3lclkrlem2v 41893
[Holland95] p. 214Definition 3.2df-lpolN 41846
[Holland95] p. 214Definition of nonsingularpnonsingN 40298
[Holland95] p. 215Lemma 3.3(1)dihoml4 41742  poml4N 40318
[Holland95] p. 215Lemma 3.3(2)dochexmid 41833  pexmidALTN 40343  pexmidN 40334
[Holland95] p. 218Theorem 3.6lclkr 41898
[Holland95] p. 218Definition of dual vector spacedf-ldual 39489  ldualset 39490
[Holland95] p. 222Item 1df-lines 39866  df-pointsN 39867
[Holland95] p. 222Item 2df-polarityN 40268
[Holland95] p. 223Remarkispsubcl2N 40312  omllaw4 39611  pol1N 40275  polcon3N 40282
[Holland95] p. 223Definitiondf-psubclN 40300
[Holland95] p. 223Equation for polaritypolval2N 40271
[Holmes] p. 40Definitiondf-xrn 38620
[Hughes] p. 44Equation 1.21bax-his3 31171
[Hughes] p. 47Definition of projection operatordfpjop 32269
[Hughes] p. 49Equation 1.30eighmre 32050  eigre 31922  eigrei 31921
[Hughes] p. 49Equation 1.31eighmorth 32051  eigorth 31925  eigorthi 31924
[Hughes] p. 137Remark (ii)eigposi 31923
[Huneke] p. 1Claim 1frgrncvvdeq 30396
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30392
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30393
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30394
[Huneke] p. 2Claim 2frgrregorufr 30412  frgrregorufr0 30411  frgrregorufrg 30413
[Huneke] p. 2Claim 3frgrhash2wsp 30419  frrusgrord 30428  frrusgrord0 30427
[Huneke] p. 2Statementdf-clwwlknon 30175
[Huneke] p. 2Statement 4frgrwopreglem4 30402
[Huneke] p. 2Statement 5frgrwopreg1 30405  frgrwopreg2 30406  frgrwopregasn 30403  frgrwopregbsn 30404
[Huneke] p. 2Statement 6frgrwopreglem5 30408
[Huneke] p. 2Statement 7fusgreghash2wspv 30422
[Huneke] p. 2Statement 8fusgreghash2wsp 30425
[Huneke] p. 2Statement 9clwlksndivn 30173  numclwlk1 30458  numclwlk1lem1 30456  numclwlk1lem2 30457  numclwwlk1 30448  numclwwlk8 30479
[Huneke] p. 2Definition 3frgrwopreglem1 30399
[Huneke] p. 2Definition 4df-clwlks 29856
[Huneke] p. 2Definition 62clwwlk 30434
[Huneke] p. 2Definition 7numclwwlkovh 30460  numclwwlkovh0 30459
[Huneke] p. 2Statement 10numclwwlk2 30468
[Huneke] p. 2Statement 11rusgrnumwlkg 30065
[Huneke] p. 2Statement 12numclwwlk3 30472
[Huneke] p. 2Statement 13numclwwlk5 30475
[Huneke] p. 2Statement 14numclwwlk7 30478
[Indrzejczak] p. 33Definition ` `Enatded 30490  natded 30490
[Indrzejczak] p. 33Definition ` `Inatded 30490
[Indrzejczak] p. 34Definition ` `Enatded 30490  natded 30490
[Indrzejczak] p. 34Definition ` `Inatded 30490
[Jech] p. 4Definition of classcv 1541  cvjust 2731
[Jech] p. 42Lemma 6.1alephexp1 10502
[Jech] p. 42Equation 6.1alephadd 10500  alephmul 10501
[Jech] p. 43Lemma 6.2infmap 10499  infmap2 10139
[Jech] p. 71Lemma 9.3jech9.3 9738
[Jech] p. 72Equation 9.3scott0 9810  scottex 9809
[Jech] p. 72Exercise 9.1rankval4 9791  rankval4b 35275
[Jech] p. 72Scheme "Collection Principle"cp 9815
[Jech] p. 78Noteopthprc 5696
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43261
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43349
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43350
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43273
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43277
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43278  rmyp1 43279
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43280  rmym1 43281
[JonesMatijasevic] p. 695Equation 2.11rmx0 43271  rmx1 43272  rmxluc 43282
[JonesMatijasevic] p. 695Equation 2.12rmy0 43275  rmy1 43276  rmyluc 43283
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43285
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43286
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43306  jm2.17b 43307  jm2.17c 43308
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43339
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43343
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43334
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43309  jm2.24nn 43305
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43348
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43354  rmygeid 43310
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43366
[Juillerat] p. 11Section *5etransc 46630  etransclem47 46628  etransclem48 46629
[Juillerat] p. 12Equation (7)etransclem44 46625
[Juillerat] p. 12Equation *(7)etransclem46 46627
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46613
[Juillerat] p. 13Proofetransclem35 46616
[Juillerat] p. 13Part of case 2 proven inetransclem38 46619
[Juillerat] p. 13Part of case 2 provenetransclem24 46605
[Juillerat] p. 13Part of case 2: proven inetransclem41 46622
[Juillerat] p. 14Proofetransclem23 46604
[KalishMontague] p. 81Note 1ax-6 1969
[KalishMontague] p. 85Lemma 2equid 2014
[KalishMontague] p. 85Lemma 3equcomi 2019
[KalishMontague] p. 86Lemma 7cbvalivw 2009  cbvaliw 2008  wl-cbvmotv 37757  wl-motae 37759  wl-moteq 37758
[KalishMontague] p. 87Lemma 8spimvw 1988  spimw 1972
[KalishMontague] p. 87Lemma 9spfw 2035  spw 2036
[Kalmbach] p. 14Definition of latticechabs1 31603  chabs1i 31605  chabs2 31604  chabs2i 31606  chjass 31620  chjassi 31573  latabs1 18410  latabs2 18411
[Kalmbach] p. 15Definition of atomdf-at 32425  ela 32426
[Kalmbach] p. 15Definition of coverscvbr2 32370  cvrval2 39639
[Kalmbach] p. 16Definitiondf-ol 39543  df-oml 39544
[Kalmbach] p. 20Definition of commutescmbr 31671  cmbri 31677  cmtvalN 39576  df-cm 31670  df-cmtN 39542
[Kalmbach] p. 22Remarkomllaw5N 39612  pjoml5 31700  pjoml5i 31675
[Kalmbach] p. 22Definitionpjoml2 31698  pjoml2i 31672
[Kalmbach] p. 22Theorem 2(v)cmcm 31701  cmcmi 31679  cmcmii 31684  cmtcomN 39614
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39610  omlsi 31491  pjoml 31523  pjomli 31522
[Kalmbach] p. 22Definition of OML lawomllaw2N 39609
[Kalmbach] p. 23Remarkcmbr2i 31683  cmcm3 31702  cmcm3i 31681  cmcm3ii 31686  cmcm4i 31682  cmt3N 39616  cmt4N 39617  cmtbr2N 39618
[Kalmbach] p. 23Lemma 3cmbr3 31695  cmbr3i 31687  cmtbr3N 39619
[Kalmbach] p. 25Theorem 5fh1 31705  fh1i 31708  fh2 31706  fh2i 31709  omlfh1N 39623
[Kalmbach] p. 65Remarkchjatom 32444  chslej 31585  chsleji 31545  shslej 31467  shsleji 31457
[Kalmbach] p. 65Proposition 1chocin 31582  chocini 31541  chsupcl 31427  chsupval2 31497  h0elch 31342  helch 31330  hsupval2 31496  ocin 31383  ococss 31380  shococss 31381
[Kalmbach] p. 65Definition of subspace sumshsval 31399
[Kalmbach] p. 66Remarkdf-pjh 31482  pjssmi 32252  pjssmii 31768
[Kalmbach] p. 67Lemma 3osum 31732  osumi 31729
[Kalmbach] p. 67Lemma 4pjci 32287
[Kalmbach] p. 103Exercise 6atmd2 32487
[Kalmbach] p. 103Exercise 12mdsl0 32397
[Kalmbach] p. 140Remarkhatomic 32447  hatomici 32446  hatomistici 32449
[Kalmbach] p. 140Proposition 1atlatmstc 39684
[Kalmbach] p. 140Proposition 1(i)atexch 32468  lsatexch 39408
[Kalmbach] p. 140Proposition 1(ii)chcv1 32442  cvlcvr1 39704  cvr1 39775
[Kalmbach] p. 140Proposition 1(iii)cvexch 32461  cvexchi 32456  cvrexch 39785
[Kalmbach] p. 149Remark 2chrelati 32451  hlrelat 39767  hlrelat5N 39766  lrelat 39379
[Kalmbach] p. 153Exercise 5lsmcv 21108  lsmsatcv 39375  spansncv 31740  spansncvi 31739
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39394  spansncv2 32380
[Kalmbach] p. 266Definitiondf-st 32298
[Kalmbach2] p. 8Definition of adjointdf-adjh 31936
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10569  fpwwe2 10566
[KanamoriPincus] p. 416Corollary 1.3canth4 10570
[KanamoriPincus] p. 417Corollary 1.6canthp1 10577
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10572
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10574
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10587
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10591  gchxpidm 10592
[KanamoriPincus] p. 419Theorem 2.1gchacg 10603  gchhar 10602
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10137  unxpwdom 9506
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10593
[Kreyszig] p. 3Property M1metcl 24288  xmetcl 24287
[Kreyszig] p. 4Property M2meteq0 24295
[Kreyszig] p. 8Definition 1.1-8dscmet 24528
[Kreyszig] p. 12Equation 5conjmul 11870  muleqadd 11793
[Kreyszig] p. 18Definition 1.3-2mopnval 24394
[Kreyszig] p. 19Remarkmopntopon 24395
[Kreyszig] p. 19Theorem T1mopn0 24454  mopnm 24400
[Kreyszig] p. 19Theorem T2unimopn 24452
[Kreyszig] p. 19Definition of neighborhoodneibl 24457
[Kreyszig] p. 20Definition 1.3-3metcnp2 24498
[Kreyszig] p. 25Definition 1.4-1lmbr 23214  lmmbr 25226  lmmbr2 25227
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23336
[Kreyszig] p. 28Theorem 1.4-5lmcau 25281
[Kreyszig] p. 28Definition 1.4-3iscau 25244  iscmet2 25262
[Kreyszig] p. 30Theorem 1.4-7cmetss 25284
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23417  metelcls 25273
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25274  metcld2 25275
[Kreyszig] p. 51Equation 2clmvneg1 25067  lmodvneg1 20868  nvinv 30726  vcm 30663
[Kreyszig] p. 51Equation 1aclm0vs 25063  lmod0vs 20858  slmd0vs 33317  vc0 30661
[Kreyszig] p. 51Equation 1blmodvs0 20859  slmdvs0 33318  vcz 30662
[Kreyszig] p. 58Definition 2.2-1imsmet 30778  ngpmet 24559  nrmmetd 24530
[Kreyszig] p. 59Equation 1imsdval 30773  imsdval2 30774  ncvspds 25129  ngpds 24560
[Kreyszig] p. 63Problem 1nmval 24545  nvnd 30775
[Kreyszig] p. 64Problem 2nmeq0 24574  nmge0 24573  nvge0 30760  nvz 30756
[Kreyszig] p. 64Problem 3nmrtri 24580  nvabs 30759
[Kreyszig] p. 91Definition 2.7-1isblo3i 30888
[Kreyszig] p. 92Equation 2df-nmoo 30832
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30894  blocni 30892
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30893
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25172  ipeq0 21605  ipz 30806
[Kreyszig] p. 135Problem 2cphpyth 25184  pythi 30937
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30941
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25206
[Kreyszig] p. 144Equation 4supcvg 15791
[Kreyszig] p. 144Theorem 3.3-1minvec 25404  minveco 30971
[Kreyszig] p. 196Definition 3.9-1df-aj 30837
[Kreyszig] p. 247Theorem 4.7-2bcth 25297
[Kreyszig] p. 249Theorem 4.7-3ubth 30960
[Kreyszig] p. 470Definition of positive operator orderingleop 32210  leopg 32209
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32228
[Kreyszig] p. 525Theorem 10.1-1htth 31005
[Kulpa] p. 547Theorempoimir 37893
[Kulpa] p. 547Equation (1)poimirlem32 37892
[Kulpa] p. 547Equation (2)poimirlem31 37891
[Kulpa] p. 548Theorembroucube 37894
[Kulpa] p. 548Equation (6)poimirlem26 37886
[Kulpa] p. 548Equation (7)poimirlem27 37887
[Kunen] p. 10Axiom 0ax6e 2388  axnul 5252
[Kunen] p. 11Axiom 3axnul 5252
[Kunen] p. 12Axiom 6zfrep6 7909
[Kunen] p. 24Definition 10.24mapval 8787  mapvalg 8785
[Kunen] p. 30Lemma 10.20fodomg 10444
[Kunen] p. 31Definition 10.24mapex 7893
[Kunen] p. 95Definition 2.1df-r1 9688
[Kunen] p. 97Lemma 2.10r1elss 9730  r1elssi 9729
[Kunen] p. 107Exercise 4rankop 9782  rankopb 9776  rankuni 9787  rankxplim 9803  rankxpsuc 9806
[Kunen2] p. 47Lemma I.9.9relpfr 45299
[Kunen2] p. 53Lemma I.9.21trfr 45307
[Kunen2] p. 53Lemma I.9.24(2)wffr 45306
[Kunen2] p. 53Definition I.9.20tcfr 45308
[Kunen2] p. 95Lemma I.16.2ralabso 45313  rexabso 45314
[Kunen2] p. 96Example I.16.3disjabso 45320  n0abso 45321  ssabso 45319
[Kunen2] p. 111Lemma II.2.4(1)traxext 45322
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45332
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45327
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45330
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45331
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45326
[Kunen2] p. 112Corollary II.2.5wfaxext 45338  wfaxpr 45343  wfaxreg 45345  wfaxrep 45339  wfaxsep 45340  wfaxun 45344
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45329
[Kunen2] p. 113Corollary II.2.9wfaxpow 45342
[Kunen2] p. 114Theorem II.2.13wfaxext 45338
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45337  omelaxinf2 45334
[Kunen2] p. 114Corollary II.2.12wfac8prim 45347  wfaxinf2 45346
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45360  permaxext 45350  permaxinf2 45358  permaxnul 45353  permaxpow 45354  permaxpr 45355  permaxrep 45351  permaxsep 45352  permaxun 45356
[Kunen2] p. 148Definition II.9.1brpermmodel 45348
[Kunen2] p. 149Exercise II.9.3permac8prim 45359
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4961
[Lang] , p. 225Corollary 1.3finexttrb 33842
[Lang] p. Definitiondf-rn 5643
[Lang] p. 3Statementlidrideqd 18606  mndbn0 18687
[Lang] p. 3Definitiondf-mnd 18672
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18624
[Lang] p. 4Property of composites. Second formulagsumccat 18778
[Lang] p. 5Equationgsumreidx 19858
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48531
[Lang] p. 6Examplenn0mnd 48528
[Lang] p. 6Equationgsumxp2 19921
[Lang] p. 6Statementcycsubm 19143
[Lang] p. 6Definitionmulgnn0gsum 19022
[Lang] p. 6Observationmndlsmidm 19611
[Lang] p. 7Definitiondfgrp2e 18905
[Lang] p. 30Definitiondf-tocyc 33200
[Lang] p. 32Property (a)cyc3genpm 33245
[Lang] p. 32Property (b)cyc3conja 33250  cycpmconjv 33235
[Lang] p. 53Definitiondf-cat 17603
[Lang] p. 53Axiom CAT 1cat1 18033  cat1lem 18032
[Lang] p. 54Definitiondf-iso 17685
[Lang] p. 57Definitiondf-inito 17920  df-termo 17921
[Lang] p. 58Exampleirinitoringc 21446
[Lang] p. 58Statementinitoeu1 17947  termoeu1 17954
[Lang] p. 62Definitiondf-func 17794
[Lang] p. 65Definitiondf-nat 17882
[Lang] p. 91Notedf-ringc 20591
[Lang] p. 92Statementmxidlprm 33562
[Lang] p. 92Definitionisprmidlc 33539
[Lang] p. 128Remarkdsmmlmod 21712
[Lang] p. 129Prooflincscm 48779  lincscmcl 48781  lincsum 48778  lincsumcl 48780
[Lang] p. 129Statementlincolss 48783
[Lang] p. 129Observationdsmmfi 21705
[Lang] p. 141Theorem 5.3dimkerim 33804  qusdimsum 33805
[Lang] p. 141Corollary 5.4lssdimle 33784
[Lang] p. 147Definitionsnlindsntor 48820
[Lang] p. 504Statementmat1 22403  matring 22399
[Lang] p. 504Definitiondf-mamu 22347
[Lang] p. 505Statementmamuass 22358  mamutpos 22414  matassa 22400  mattposvs 22411  tposmap 22413
[Lang] p. 513Definitionmdet1 22557  mdetf 22551
[Lang] p. 513Theorem 4.4cramer 22647
[Lang] p. 514Proposition 4.6mdetleib 22543
[Lang] p. 514Proposition 4.8mdettpos 22567
[Lang] p. 515Definitiondf-minmar1 22591  smadiadetr 22631
[Lang] p. 515Corollary 4.9mdetero 22566  mdetralt 22564
[Lang] p. 517Proposition 4.15mdetmul 22579
[Lang] p. 518Definitiondf-madu 22590
[Lang] p. 518Proposition 4.16madulid 22601  madurid 22600  matinv 22633
[Lang] p. 561Theorem 3.1cayleyhamilton 22846
[Lang], p. 190Chapter 6vieta 33756
[Lang], p. 224Proposition 1.1extdgfialg 33871  finextalg 33875
[Lang], p. 224Proposition 1.2extdgmul 33840  fedgmul 33808
[Lang], p. 225Proposition 1.4algextdeg 33902
[Lang], p. 561Remarkchpmatply1 22788
[Lang], p. 561Definitiondf-chpmat 22783
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44679
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44674
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44680
[LeBlanc] p. 277Rule R2axnul 5252
[Levy] p. 12Axiom 4.3.1df-clab 2716
[Levy] p. 59Definitiondf-ttrcl 9629
[Levy] p. 64Theorem 5.6(ii)frinsg 9675
[Levy] p. 338Axiomdf-clel 2812  df-cleq 2729
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2812  df-cleq 2729
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2716
[Levy] p. 358Axiomdf-clab 2716
[Levy58] p. 2Definition Iisfin1-3 10308
[Levy58] p. 2Definition IIdf-fin2 10208
[Levy58] p. 2Definition Iadf-fin1a 10207
[Levy58] p. 2Definition IIIdf-fin3 10210
[Levy58] p. 3Definition Vdf-fin5 10211
[Levy58] p. 3Definition IVdf-fin4 10209
[Levy58] p. 4Definition VIdf-fin6 10212
[Levy58] p. 4Definition VIIdf-fin7 10213
[Levy58], p. 3Theorem 1fin1a2 10337
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27666
[Lipparini] p. 3Lemma 2.1.4noresle 27677
[Lipparini] p. 6Proposition 4.2noinfbnd1 27709  nosupbnd1 27694
[Lipparini] p. 6Proposition 4.3noinfbnd2 27711  nosupbnd2 27696
[Lipparini] p. 7Theorem 5.1noetasuplem3 27715  noetasuplem4 27716
[Lipparini] p. 7Corollary 4.4nosupinfsep 27712
[Lopez-Astorga] p. 12Rule 1mptnan 1770
[Lopez-Astorga] p. 12Rule 2mptxor 1771
[Lopez-Astorga] p. 12Rule 3mtpxor 1773
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32495
[Maeda] p. 168Lemma 5mdsym 32499  mdsymi 32498
[Maeda] p. 168Lemma 4(i)mdsymlem4 32493  mdsymlem6 32495  mdsymlem7 32496
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32497
[MaedaMaeda] p. 1Remarkssdmd1 32400  ssdmd2 32401  ssmd1 32398  ssmd2 32399
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32396
[MaedaMaeda] p. 1Definition 1.1df-dmd 32368  df-md 32367  mdbr 32381
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32418  mdslj1i 32406  mdslj2i 32407  mdslle1i 32404  mdslle2i 32405  mdslmd1i 32416  mdslmd2i 32417
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32408  mdsl2bi 32410  mdsl2i 32409
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32422
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32419
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32420
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32397
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32402  mdsl3 32403
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32421
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32516
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39686  hlrelat1 39765
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39404
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32423  cvmdi 32411  cvnbtwn4 32376  cvrnbtwn4 39644
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32424
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39705  cvp 32462  cvrp 39781  lcvp 39405
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32486
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32485
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39698  hlexch4N 39757
[MaedaMaeda] p. 34Exercise 7.1atabsi 32488
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39808
[MaedaMaeda] p. 61Definition 15.10psubN 40114  atpsubN 40118  df-pointsN 39867  pointpsubN 40116
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39869  pmap11 40127  pmaple 40126  pmapsub 40133  pmapval 40122
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40130  pmap1N 40132
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40135  pmapglb2N 40136  pmapglb2xN 40137  pmapglbx 40134
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40217
[MaedaMaeda] p. 67Postulate PS1ps-1 39842
[MaedaMaeda] p. 68Lemma 16.2df-padd 40161  paddclN 40207  paddidm 40206
[MaedaMaeda] p. 68Condition PS2ps-2 39843
[MaedaMaeda] p. 68Equation 16.2.1paddass 40203
[MaedaMaeda] p. 69Lemma 16.4ps-1 39842
[MaedaMaeda] p. 69Theorem 16.4ps-2 39843
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19616  lsmmod2 19617  lssats 39377  shatomici 32445  shatomistici 32448  shmodi 31477  shmodsi 31476
[MaedaMaeda] p. 130Remark 29.6dmdmd 32387  mdsymlem7 32496
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31676
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31580
[MaedaMaeda] p. 139Remarksumdmdii 32502
[Margaris] p. 40Rule Cexlimiv 1932
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 396  df-ex 1782  df-or 849  dfbi2 474
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 30487
[Margaris] p. 59Section 14notnotrALTVD 45259
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 45260
[Margaris] p. 79Rule Cexinst01 44970  exinst11 44971
[Margaris] p. 89Theorem 19.219.2 1978  19.2g 2196  r19.2z 4454
[Margaris] p. 89Theorem 19.319.3 2210  rr19.3v 3623
[Margaris] p. 89Theorem 19.5alcom 2165
[Margaris] p. 89Theorem 19.6alex 1828
[Margaris] p. 89Theorem 19.7alnex 1783
[Margaris] p. 89Theorem 19.819.8a 2189
[Margaris] p. 89Theorem 19.919.9 2213  19.9h 2293  exlimd 2226  exlimdh 2297
[Margaris] p. 89Theorem 19.11excom 2168  excomim 2169
[Margaris] p. 89Theorem 19.1219.12 2333
[Margaris] p. 90Section 19conventions-labels 30488  conventions-labels 30488  conventions-labels 30488  conventions-labels 30488
[Margaris] p. 90Theorem 19.14exnal 1829
[Margaris] p. 90Theorem 19.152albi 44723  albi 1820
[Margaris] p. 90Theorem 19.1619.16 2233
[Margaris] p. 90Theorem 19.1719.17 2234
[Margaris] p. 90Theorem 19.182exbi 44725  exbi 1849
[Margaris] p. 90Theorem 19.1919.19 2237
[Margaris] p. 90Theorem 19.202alim 44722  2alimdv 1920  alimd 2220  alimdh 1819  alimdv 1918  ax-4 1811  ralimdaa 3239  ralimdv 3152  ralimdva 3150  ralimdvva 3185  sbcimdv 3811
[Margaris] p. 90Theorem 19.2119.21 2215  19.21h 2294  19.21t 2214  19.21vv 44721  alrimd 2223  alrimdd 2222  alrimdh 1865  alrimdv 1931  alrimi 2221  alrimih 1826  alrimiv 1929  alrimivv 1930  hbralrimi 3128  r19.21be 3231  r19.21bi 3230  ralrimd 3243  ralrimdv 3136  ralrimdva 3138  ralrimdvv 3182  ralrimdvva 3193  ralrimi 3236  ralrimia 3237  ralrimiv 3129  ralrimiva 3130  ralrimivv 3179  ralrimivva 3181  ralrimivvva 3184  ralrimivw 3134
[Margaris] p. 90Theorem 19.222exim 44724  2eximdv 1921  bj-exim 36853  exim 1836  eximd 2224  eximdh 1866  eximdv 1919  rexim 3079  reximd2a 3248  reximdai 3240  reximdd 45496  reximddv 3154  reximddv2 3197  reximddv3 3155  reximdv 3153  reximdv2 3148  reximdva 3151  reximdvai 3149  reximdvva 3186  reximi2 3071
[Margaris] p. 90Theorem 19.2319.23 2219  19.23bi 2199  19.23h 2295  19.23t 2218  exlimdv 1935  exlimdvv 1936  exlimexi 44869  exlimiv 1932  exlimivv 1934  rexlimd3 45492  rexlimdv 3137  rexlimdv3a 3143  rexlimdva 3139  rexlimdva2 3141  rexlimdvaa 3140  rexlimdvv 3194  rexlimdvva 3195  rexlimdvvva 3196  rexlimdvw 3144  rexlimiv 3132  rexlimiva 3131  rexlimivv 3180
[Margaris] p. 90Theorem 19.2419.24 1993
[Margaris] p. 90Theorem 19.2519.25 1882
[Margaris] p. 90Theorem 19.2619.26 1872
[Margaris] p. 90Theorem 19.2719.27 2235  r19.27z 4465  r19.27zv 4466
[Margaris] p. 90Theorem 19.2819.28 2236  19.28vv 44731  r19.28z 4457  r19.28zf 45507  r19.28zv 4461  rr19.28v 3624
[Margaris] p. 90Theorem 19.2919.29 1875  r19.29d2r 3125  r19.29imd 3103
[Margaris] p. 90Theorem 19.3019.30 1883
[Margaris] p. 90Theorem 19.3119.31 2242  19.31vv 44729
[Margaris] p. 90Theorem 19.3219.32 2241  r19.32 47447
[Margaris] p. 90Theorem 19.3319.33-2 44727  19.33 1886
[Margaris] p. 90Theorem 19.3419.34 1994
[Margaris] p. 90Theorem 19.3519.35 1879
[Margaris] p. 90Theorem 19.3619.36 2238  19.36vv 44728  r19.36zv 4467
[Margaris] p. 90Theorem 19.3719.37 2240  19.37vv 44730  r19.37zv 4462
[Margaris] p. 90Theorem 19.3819.38 1841
[Margaris] p. 90Theorem 19.3919.39 1992
[Margaris] p. 90Theorem 19.4019.40-2 1889  19.40 1888  r19.40 3104
[Margaris] p. 90Theorem 19.4119.41 2243  19.41rg 44895
[Margaris] p. 90Theorem 19.4219.42 2244
[Margaris] p. 90Theorem 19.4319.43 1884
[Margaris] p. 90Theorem 19.4419.44 2245  r19.44zv 4464
[Margaris] p. 90Theorem 19.4519.45 2246  r19.45zv 4463
[Margaris] p. 110Exercise 2(b)eu1 2611
[Mayet] p. 370Remarkjpi 32357  largei 32354  stri 32344
[Mayet3] p. 9Definition of CH-statesdf-hst 32299  ishst 32301
[Mayet3] p. 10Theoremhstrbi 32353  hstri 32352
[Mayet3] p. 1223Theorem 4.1mayete3i 31815
[Mayet3] p. 1240Theorem 7.1mayetes3i 31816
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32365
[MegPav2000] p. 2345Definition 3.4-1chintcl 31419  chsupcl 31427
[MegPav2000] p. 2345Definition 3.4-2hatomic 32447
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32441
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32468
[MegPav2000] p. 2366Figure 7pl42N 40348
[MegPav2002] p. 362Lemma 2.2latj31 18422  latj32 18420  latjass 18418
[Megill] p. 444Axiom C5ax-5 1912  ax5ALT 39272
[Megill] p. 444Section 7conventions 30487
[Megill] p. 445Lemma L12aecom-o 39266  ax-c11n 39253  axc11n 2431
[Megill] p. 446Lemma L17equtrr 2024
[Megill] p. 446Lemma L18ax6fromc10 39261
[Megill] p. 446Lemma L19hbnae-o 39293  hbnae 2437
[Megill] p. 447Remark 9.1dfsb1 2486  sbid 2263  sbidd-misc 50067  sbidd 50066
[Megill] p. 448Remark 9.6axc14 2468
[Megill] p. 448Scheme C4'ax-c4 39249
[Megill] p. 448Scheme C5'ax-c5 39248  sp 2191
[Megill] p. 448Scheme C6'ax-11 2163
[Megill] p. 448Scheme C7'ax-c7 39250
[Megill] p. 448Scheme C8'ax-7 2010
[Megill] p. 448Scheme C9'ax-c9 39255
[Megill] p. 448Scheme C10'ax-6 1969  ax-c10 39251
[Megill] p. 448Scheme C11'ax-c11 39252
[Megill] p. 448Scheme C12'ax-8 2116
[Megill] p. 448Scheme C13'ax-9 2124
[Megill] p. 448Scheme C14'ax-c14 39256
[Megill] p. 448Scheme C15'ax-c15 39254
[Megill] p. 448Scheme C16'ax-c16 39257
[Megill] p. 448Theorem 9.4dral1-o 39269  dral1 2444  dral2-o 39295  dral2 2443  drex1 2446  drex2 2447  drsb1 2500  drsb2 2274
[Megill] p. 449Theorem 9.7sbcom2 2179  sbequ 2089  sbid2v 2514
[Megill] p. 450Example in Appendixhba1-o 39262  hba1 2300
[Mendelson] p. 35Axiom A3hirstL-ax3 47241
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3831  rspsbca 3832  stdpc4 2074
[Mendelson] p. 69Axiom 5ax-c4 39249  ra4 3838  stdpc5 2216
[Mendelson] p. 81Rule Cexlimiv 1932
[Mendelson] p. 95Axiom 6stdpc6 2030
[Mendelson] p. 95Axiom 7stdpc7 2258
[Mendelson] p. 225Axiom system NBGru 3740
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5470
[Mendelson] p. 231Exercise 4.10(k)inv1 4352
[Mendelson] p. 231Exercise 4.10(l)unv 4353
[Mendelson] p. 231Exercise 4.10(n)dfin3 4231
[Mendelson] p. 231Exercise 4.10(o)df-nul 4288
[Mendelson] p. 231Exercise 4.10(q)dfin4 4232
[Mendelson] p. 231Exercise 4.10(s)ddif 4095
[Mendelson] p. 231Definition of uniondfun3 4230
[Mendelson] p. 235Exercise 4.12(c)univ 5406
[Mendelson] p. 235Exercise 4.12(d)pwv 4862
[Mendelson] p. 235Exercise 4.12(j)pwin 5523
[Mendelson] p. 235Exercise 4.12(k)pwunss 4574
[Mendelson] p. 235Exercise 4.12(l)pwssun 5524
[Mendelson] p. 235Exercise 4.12(n)uniin 4889
[Mendelson] p. 235Exercise 4.12(p)reli 5783
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6235
[Mendelson] p. 244Proposition 4.8(g)epweon 7730
[Mendelson] p. 246Definition of successordf-suc 6331
[Mendelson] p. 250Exercise 4.36oelim2 8533
[Mendelson] p. 254Proposition 4.22(b)xpen 9080
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9001  xpsneng 9002
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9008  xpcomeng 9009
[Mendelson] p. 254Proposition 4.22(e)xpassen 9011
[Mendelson] p. 255Definitionbrsdom 8923
[Mendelson] p. 255Exercise 4.39endisj 9004
[Mendelson] p. 255Exercise 4.41mapprc 8779
[Mendelson] p. 255Exercise 4.43mapsnen 8986  mapsnend 8985
[Mendelson] p. 255Exercise 4.45mapunen 9086
[Mendelson] p. 255Exercise 4.47xpmapen 9085
[Mendelson] p. 255Exercise 4.42(a)map0e 8832
[Mendelson] p. 255Exercise 4.42(b)map1 8989
[Mendelson] p. 257Proposition 4.24(a)undom 9005
[Mendelson] p. 258Exercise 4.56(c)djuassen 10101  djucomen 10100
[Mendelson] p. 258Exercise 4.56(f)djudom1 10105
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10099
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8468
[Mendelson] p. 266Proposition 4.34(f)oaordex 8495
[Mendelson] p. 275Proposition 4.42(d)entri3 10481
[Mendelson] p. 281Definitiondf-r1 9688
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9737
[Mendelson] p. 287Axiom system MKru 3740
[MertziosUnger] p. 152Definitiondf-frgr 30346
[MertziosUnger] p. 153Remark 1frgrconngr 30381
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30383  vdgn1frgrv3 30384
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30385
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30378
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30371  2pthfrgrrn 30369  2pthfrgrrn2 30370
[Mittelstaedt] p. 9Definitiondf-oc 31339
[Monk1] p. 22Remarkconventions 30487
[Monk1] p. 22Theorem 3.1conventions 30487
[Monk1] p. 26Theorem 2.8(vii)ssin 4193
[Monk1] p. 33Theorem 3.2(i)ssrel 5740  ssrelf 32704
[Monk1] p. 33Theorem 3.2(ii)eqrel 5741
[Monk1] p. 34Definition 3.3df-opab 5163
[Monk1] p. 36Theorem 3.7(i)coi1 6229  coi2 6230
[Monk1] p. 36Theorem 3.8(v)dm0 5877  rn0 5883
[Monk1] p. 36Theorem 3.7(ii)cnvi 6107
[Monk1] p. 37Theorem 3.13(i)relxp 5650
[Monk1] p. 37Theorem 3.13(x)dmxp 5886  rnxp 6136
[Monk1] p. 37Theorem 3.13(ii)0xp 5731  xp0 5732
[Monk1] p. 38Theorem 3.16(ii)ima0 6044
[Monk1] p. 38Theorem 3.16(viii)imai 6041
[Monk1] p. 39Theorem 3.17imaex 7866  imaexg 7865
[Monk1] p. 39Theorem 3.16(xi)imassrn 6038
[Monk1] p. 41Theorem 4.3(i)fnopfv 7029  funfvop 7004
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6896
[Monk1] p. 42Theorem 4.4(iii)fvelima 6907
[Monk1] p. 43Theorem 4.6funun 6546
[Monk1] p. 43Theorem 4.8(iv)dff13 7210  dff13f 7211
[Monk1] p. 46Theorem 4.15(v)funex 7175  funrnex 7908
[Monk1] p. 50Definition 5.4fniunfv 7203
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6193
[Monk1] p. 52Theorem 5.11(viii)ssint 4921
[Monk1] p. 52Definition 5.13 (i)1stval2 7960  df-1st 7943
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7961  df-2nd 7944
[Monk1] p. 112Theorem 15.17(v)ranksn 9778  ranksnb 9751
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9779
[Monk1] p. 112Theorem 15.17(iii)rankun 9780  rankunb 9774
[Monk1] p. 113Theorem 15.18r1val3 9762
[Monk1] p. 113Definition 15.19df-r1 9688  r1val2 9761
[Monk1] p. 117Lemmazorn2 10428  zorn2g 10425
[Monk1] p. 133Theorem 18.11cardom 9910
[Monk1] p. 133Theorem 18.12canth3 10483
[Monk1] p. 133Theorem 18.14carduni 9905
[Monk2] p. 105Axiom C4ax-4 1811
[Monk2] p. 105Axiom C7ax-7 2010
[Monk2] p. 105Axiom C8ax-12 2185  ax-c15 39254  ax12v2 2187
[Monk2] p. 108Lemma 5ax-c4 39249
[Monk2] p. 109Lemma 12ax-11 2163
[Monk2] p. 109Lemma 15equvini 2460  equvinv 2031  eqvinop 5443
[Monk2] p. 113Axiom C5-1ax-5 1912  ax5ALT 39272
[Monk2] p. 113Axiom C5-2ax-10 2147
[Monk2] p. 113Axiom C5-3ax-11 2163
[Monk2] p. 114Lemma 21sp 2191
[Monk2] p. 114Lemma 22axc4 2327  hba1-o 39262  hba1 2300
[Monk2] p. 114Lemma 23nfia1 2159
[Monk2] p. 114Lemma 24nfa2 2182  nfra2 3348  nfra2w 3274
[Moore] p. 53Part Idf-mre 17517
[Munkres] p. 77Example 2distop 22951  indistop 22958  indistopon 22957
[Munkres] p. 77Example 3fctop 22960  fctop2 22961
[Munkres] p. 77Example 4cctop 22962
[Munkres] p. 78Definition of basisdf-bases 22902  isbasis3g 22905
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17375  tgval2 22912
[Munkres] p. 79Remarktgcl 22925
[Munkres] p. 80Lemma 2.1tgval3 22919
[Munkres] p. 80Lemma 2.2tgss2 22943  tgss3 22942
[Munkres] p. 81Lemma 2.3basgen 22944  basgen2 22945
[Munkres] p. 83Exercise 3topdifinf 37593  topdifinfeq 37594  topdifinffin 37592  topdifinfindis 37590
[Munkres] p. 89Definition of subspace topologyresttop 23116
[Munkres] p. 93Theorem 6.1(1)0cld 22994  topcld 22991
[Munkres] p. 93Theorem 6.1(2)iincld 22995
[Munkres] p. 93Theorem 6.1(3)uncld 22997
[Munkres] p. 94Definition of closureclsval 22993
[Munkres] p. 94Definition of interiorntrval 22992
[Munkres] p. 95Theorem 6.5(a)clsndisj 23031  elcls 23029
[Munkres] p. 95Theorem 6.5(b)elcls3 23039
[Munkres] p. 97Theorem 6.6clslp 23104  neindisj 23073
[Munkres] p. 97Corollary 6.7cldlp 23106
[Munkres] p. 97Definition of limit pointislp2 23101  lpval 23095
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23271
[Munkres] p. 102Definition of continuous functiondf-cn 23183  iscn 23191  iscn2 23194
[Munkres] p. 107Theorem 7.2(g)cncnp 23236  cncnp2 23237  cncnpi 23234  df-cnp 23184  iscnp 23193  iscnp2 23195
[Munkres] p. 127Theorem 10.1metcn 24499
[Munkres] p. 128Theorem 10.3metcn4 25279
[Nathanson] p. 123Remarkreprgt 34798  reprinfz1 34799  reprlt 34796
[Nathanson] p. 123Definitiondf-repr 34786
[Nathanson] p. 123Chapter 5.1circlemethnat 34818
[Nathanson] p. 123Propositionbreprexp 34810  breprexpnat 34811  itgexpif 34783
[NielsenChuang] p. 195Equation 4.73unierri 32191
[OeSilva] p. 2042Section 2ax-bgbltosilva 48159
[Pfenning] p. 17Definition XMnatded 30490
[Pfenning] p. 17Definition NNCnatded 30490  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30490
[Pfenning] p. 18Rule"natded 30490
[Pfenning] p. 18Definition /\Inatded 30490
[Pfenning] p. 18Definition ` `Enatded 30490  natded 30490  natded 30490  natded 30490  natded 30490
[Pfenning] p. 18Definition ` `Inatded 30490  natded 30490  natded 30490  natded 30490  natded 30490
[Pfenning] p. 18Definition ` `ELnatded 30490
[Pfenning] p. 18Definition ` `ERnatded 30490
[Pfenning] p. 18Definition ` `Ea,unatded 30490
[Pfenning] p. 18Definition ` `IRnatded 30490
[Pfenning] p. 18Definition ` `Ianatded 30490
[Pfenning] p. 127Definition =Enatded 30490
[Pfenning] p. 127Definition =Inatded 30490
[Ponnusamy] p. 361Theorem 6.44cphip0l 25170  df-dip 30788  dip0l 30805  ip0l 21603
[Ponnusamy] p. 361Equation 6.45cphipval 25211  ipval 30790
[Ponnusamy] p. 362Equation I1dipcj 30801  ipcj 21601
[Ponnusamy] p. 362Equation I3cphdir 25173  dipdir 30929  ipdir 21606  ipdiri 30917
[Ponnusamy] p. 362Equation I4ipidsq 30797  nmsq 25162
[Ponnusamy] p. 362Equation 6.46ip0i 30912
[Ponnusamy] p. 362Equation 6.47ip1i 30914
[Ponnusamy] p. 362Equation 6.48ip2i 30915
[Ponnusamy] p. 363Equation I2cphass 25179  dipass 30932  ipass 21612  ipassi 30928
[Prugovecki] p. 186Definition of brabraval 32031  df-bra 31937
[Prugovecki] p. 376Equation 8.1df-kb 31938  kbval 32041
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32469
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40253
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32483  atcvat4i 32484  cvrat3 39807  cvrat4 39808  lsatcvat3 39417
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32369  cvrval 39634  df-cv 32366  df-lcv 39384  lspsncv0 21113
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40265
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40266
[Quine] p. 16Definition 2.1df-clab 2716  rabid 3422  rabidd 45503
[Quine] p. 17Definition 2.1''dfsb7 2286
[Quine] p. 18Definition 2.7df-cleq 2729
[Quine] p. 19Definition 2.9conventions 30487  df-v 3444
[Quine] p. 34Theorem 5.1eqabb 2876
[Quine] p. 35Theorem 5.2abid1 2873  abid2f 2930
[Quine] p. 40Theorem 6.1sb5 2283
[Quine] p. 40Theorem 6.2sb6 2091  sbalex 2250
[Quine] p. 41Theorem 6.3df-clel 2812
[Quine] p. 41Theorem 6.4eqid 2737  eqid1 30554
[Quine] p. 41Theorem 6.5eqcom 2744
[Quine] p. 42Theorem 6.6df-sbc 3743
[Quine] p. 42Theorem 6.7dfsbcq 3744  dfsbcq2 3745
[Quine] p. 43Theorem 6.8vex 3446
[Quine] p. 43Theorem 6.9isset 3456
[Quine] p. 44Theorem 7.3spcgf 3547  spcgv 3552  spcimgf 3509
[Quine] p. 44Theorem 6.11spsbc 3755  spsbcd 3756
[Quine] p. 44Theorem 6.12elex 3463
[Quine] p. 44Theorem 6.13elab 3636  elabg 3633  elabgf 3631
[Quine] p. 44Theorem 6.14noel 4292
[Quine] p. 48Theorem 7.2snprc 4676
[Quine] p. 48Definition 7.1df-pr 4585  df-sn 4583
[Quine] p. 49Theorem 7.4snss 4743  snssg 4742
[Quine] p. 49Theorem 7.5prss 4778  prssg 4777
[Quine] p. 49Theorem 7.6prid1 4721  prid1g 4719  prid2 4722  prid2g 4720  snid 4621  snidg 4619
[Quine] p. 51Theorem 7.12snex 5385
[Quine] p. 51Theorem 7.13prex 5384
[Quine] p. 53Theorem 8.2unisn 4884  unisnALT 45270  unisng 4883
[Quine] p. 53Theorem 8.3uniun 4888
[Quine] p. 54Theorem 8.6elssuni 4896
[Quine] p. 54Theorem 8.7uni0 4893
[Quine] p. 56Theorem 8.17uniabio 6470
[Quine] p. 56Definition 8.18dfaiota2 47435  dfiota2 6457
[Quine] p. 57Theorem 8.19aiotaval 47444  iotaval 6474
[Quine] p. 57Theorem 8.22iotanul 6480
[Quine] p. 58Theorem 8.23iotaex 6476
[Quine] p. 58Definition 9.1df-op 4589
[Quine] p. 61Theorem 9.5opabid 5481  opabidw 5480  opelopab 5498  opelopaba 5492  opelopabaf 5500  opelopabf 5501  opelopabg 5494  opelopabga 5489  opelopabgf 5496  oprabid 7400  oprabidw 7399
[Quine] p. 64Definition 9.11df-xp 5638
[Quine] p. 64Definition 9.12df-cnv 5640
[Quine] p. 64Definition 9.15df-id 5527
[Quine] p. 65Theorem 10.3fun0 6565
[Quine] p. 65Theorem 10.4funi 6532
[Quine] p. 65Theorem 10.5funsn 6553  funsng 6551
[Quine] p. 65Definition 10.1df-fun 6502
[Quine] p. 65Definition 10.2args 6059  dffv4 6839
[Quine] p. 68Definition 10.11conventions 30487  df-fv 6508  fv2 6837
[Quine] p. 124Theorem 17.3nn0opth2 14207  nn0opth2i 14206  nn0opthi 14205  omopthi 8599
[Quine] p. 177Definition 25.2df-rdg 8351
[Quine] p. 232Equation icarddom 10476
[Quine] p. 284Axiom 39(vi)funimaex 6588  funimaexg 6587
[Quine] p. 331Axiom system NFru 3740
[ReedSimon] p. 36Definition (iii)ax-his3 31171
[ReedSimon] p. 63Exercise 4(a)df-dip 30788  polid 31246  polid2i 31244  polidi 31245
[ReedSimon] p. 63Exercise 4(b)df-ph 30900
[ReedSimon] p. 195Remarklnophm 32106  lnophmi 32105
[Retherford] p. 49Exercise 1(i)leopadd 32219
[Retherford] p. 49Exercise 1(ii)leopmul 32221  leopmuli 32220
[Retherford] p. 49Exercise 1(iv)leoptr 32224
[Retherford] p. 49Definition VI.1df-leop 31939  leoppos 32213
[Retherford] p. 49Exercise 1(iii)leoptri 32223
[Retherford] p. 49Definition of operator orderingleop3 32212
[Roman] p. 4Definitiondf-dmat 22446  df-dmatalt 48747
[Roman] p. 18Part Preliminariesdf-rng 20100
[Roman] p. 19Part Preliminariesdf-ring 20182
[Roman] p. 46Theorem 1.6isldepslvec2 48834
[Roman] p. 112Noteisldepslvec2 48834  ldepsnlinc 48857  zlmodzxznm 48846
[Roman] p. 112Examplezlmodzxzequa 48845  zlmodzxzequap 48848  zlmodzxzldep 48853
[Roman] p. 170Theorem 7.8cayleyhamilton 22846
[Rosenlicht] p. 80Theoremheicant 37895
[Rosser] p. 281Definitiondf-op 4589
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34822
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34823
[Rotman] p. 28Remarkpgrpgt2nabl 48715  pmtr3ncom 19416
[Rotman] p. 31Theorem 3.4symggen2 19412
[Rotman] p. 42Theorem 3.15cayley 19355  cayleyth 19356
[Rudin] p. 164Equation 27efcan 16031
[Rudin] p. 164Equation 30efzval 16039
[Rudin] p. 167Equation 48absefi 16133
[Sanford] p. 39Remarkax-mp 5  mto 197
[Sanford] p. 39Rule 3mtpxor 1773
[Sanford] p. 39Rule 4mptxor 1771
[Sanford] p. 40Rule 1mptnan 1770
[Schechter] p. 51Definition of antisymmetryintasym 6080
[Schechter] p. 51Definition of irreflexivityintirr 6083
[Schechter] p. 51Definition of symmetrycnvsym 6079
[Schechter] p. 51Definition of transitivitycotr 6077
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17517
[Schechter] p. 79Definition of Moore closuredf-mrc 17518
[Schechter] p. 82Section 4.5df-mrc 17518
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17520
[Schechter] p. 139Definition AC3dfac9 10059
[Schechter] p. 141Definition (MC)dfac11 43408
[Schechter] p. 149Axiom DC1ax-dc 10368  axdc3 10376
[Schechter] p. 187Definition of "ring with unit"isring 20184  isrngo 38137
[Schechter] p. 276Remark 11.6.espan0 31629
[Schechter] p. 276Definition of spandf-span 31396  spanval 31420
[Schechter] p. 428Definition 15.35bastop1 22949
[Schloeder] p. 1Lemma 1.3onelon 6350  onelord 43597  ordelon 6349  ordelord 6347
[Schloeder] p. 1Lemma 1.7onepsuc 43598  sucidg 6408
[Schloeder] p. 1Remark 1.50elon 6380  onsuc 7765  ord0 6379  ordsuci 7763
[Schloeder] p. 1Theorem 1.9epsoon 43599
[Schloeder] p. 1Definition 1.1dftr5 5211
[Schloeder] p. 1Definition 1.2dford3 43374  elon2 6336
[Schloeder] p. 1Definition 1.4df-suc 6331
[Schloeder] p. 1Definition 1.6epel 5535  epelg 5533
[Schloeder] p. 1Theorem 1.9(i)elirr 9516  epirron 43600  ordirr 6343
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43602  oneptr 43601  ontr1 6372
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6368  oneptri 43603  ordtri3or 6357
[Schloeder] p. 2Lemma 1.10ondif1 8438  ord0eln0 6381
[Schloeder] p. 2Lemma 1.13elsuci 6394  onsucss 43612  trsucss 6415
[Schloeder] p. 2Lemma 1.14ordsucss 7770
[Schloeder] p. 2Lemma 1.15onnbtwn 6421  ordnbtwn 6420
[Schloeder] p. 2Lemma 1.16orddif0suc 43614  ordnexbtwnsuc 43613
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10323  onsucf1lem 43615  onsucf1o 43618  onsucf1olem 43616  onsucrn 43617
[Schloeder] p. 2Lemma 1.18dflim7 43619
[Schloeder] p. 2Remark 1.12ordzsl 7797
[Schloeder] p. 2Theorem 1.10ondif1i 43608  ordne0gt0 43607
[Schloeder] p. 2Definition 1.11dflim6 43610  limnsuc 43611  onsucelab 43609
[Schloeder] p. 3Remark 1.21omex 9564
[Schloeder] p. 3Theorem 1.19tfinds 7812
[Schloeder] p. 3Theorem 1.22omelon 9567  ordom 7828
[Schloeder] p. 3Definition 1.20dfom3 9568
[Schloeder] p. 4Lemma 2.21onn 8578
[Schloeder] p. 4Lemma 2.7ssonuni 7735  ssorduni 7734
[Schloeder] p. 4Remark 2.4oa1suc 8468
[Schloeder] p. 4Theorem 1.23dfom5 9571  limom 7834
[Schloeder] p. 4Definition 2.1df-1o 8407  df1o2 8414
[Schloeder] p. 4Definition 2.3oa0 8453  oa0suclim 43621  oalim 8469  oasuc 8461
[Schloeder] p. 4Definition 2.5om0 8454  om0suclim 43622  omlim 8470  omsuc 8463
[Schloeder] p. 4Definition 2.6oe0 8459  oe0m1 8458  oe0suclim 43623  oelim 8471  oesuc 8464
[Schloeder] p. 5Lemma 2.10onsupuni 43575
[Schloeder] p. 5Lemma 2.11onsupsucismax 43625
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43626
[Schloeder] p. 5Lemma 2.13limexissup 43627  limexissupab 43629  limiun 43628  limuni 6387
[Schloeder] p. 5Lemma 2.14oa0r 8475
[Schloeder] p. 5Lemma 2.15om1 8479  om1om1r 43630  om1r 8480
[Schloeder] p. 5Remark 2.8oacl 8472  oaomoecl 43624  oecl 8474  omcl 8473
[Schloeder] p. 5Definition 2.9onsupintrab 43577
[Schloeder] p. 6Lemma 2.16oe1 8481
[Schloeder] p. 6Lemma 2.17oe1m 8482
[Schloeder] p. 6Lemma 2.18oe0rif 43631
[Schloeder] p. 6Theorem 2.19oasubex 43632
[Schloeder] p. 6Theorem 2.20nnacl 8549  nnamecl 43633  nnecl 8551  nnmcl 8550
[Schloeder] p. 7Lemma 3.1onsucwordi 43634
[Schloeder] p. 7Lemma 3.2oaword1 8489
[Schloeder] p. 7Lemma 3.3oaword2 8490
[Schloeder] p. 7Lemma 3.4oalimcl 8497
[Schloeder] p. 7Lemma 3.5oaltublim 43636
[Schloeder] p. 8Lemma 3.6oaordi3 43637
[Schloeder] p. 8Lemma 3.81oaomeqom 43639
[Schloeder] p. 8Lemma 3.10oa00 8496
[Schloeder] p. 8Lemma 3.11omge1 43643  omword1 8510
[Schloeder] p. 8Remark 3.9oaordnr 43642  oaordnrex 43641
[Schloeder] p. 8Theorem 3.7oaord3 43638
[Schloeder] p. 9Lemma 3.12omge2 43644  omword2 8511
[Schloeder] p. 9Lemma 3.13omlim2 43645
[Schloeder] p. 9Lemma 3.14omord2lim 43646
[Schloeder] p. 9Lemma 3.15omord2i 43647  omordi 8503
[Schloeder] p. 9Theorem 3.16omord 8505  omord2com 43648
[Schloeder] p. 10Lemma 3.172omomeqom 43649  df-2o 8408
[Schloeder] p. 10Lemma 3.19oege1 43652  oewordi 8529
[Schloeder] p. 10Lemma 3.20oege2 43653  oeworde 8531
[Schloeder] p. 10Lemma 3.21rp-oelim2 43654
[Schloeder] p. 10Lemma 3.22oeord2lim 43655
[Schloeder] p. 10Remark 3.18omnord1 43651  omnord1ex 43650
[Schloeder] p. 11Lemma 3.23oeord2i 43656
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43658
[Schloeder] p. 11Remark 3.26oenord1 43662  oenord1ex 43661
[Schloeder] p. 11Theorem 4.1oaomoencom 43663
[Schloeder] p. 11Theorem 4.2oaass 8498
[Schloeder] p. 11Theorem 3.24oeord2com 43657
[Schloeder] p. 12Theorem 4.3odi 8516
[Schloeder] p. 13Theorem 4.4omass 8517
[Schloeder] p. 14Remark 4.6oenass 43665
[Schloeder] p. 14Theorem 4.7oeoa 8535
[Schloeder] p. 15Lemma 5.1cantnftermord 43666
[Schloeder] p. 15Lemma 5.2cantnfub 43667  cantnfub2 43668
[Schloeder] p. 16Theorem 5.3cantnf2 43671
[Schwabhauser] p. 10Axiom A1axcgrrflx 28999  axtgcgrrflx 28546
[Schwabhauser] p. 10Axiom A2axcgrtr 29000
[Schwabhauser] p. 10Axiom A3axcgrid 29001  axtgcgrid 28547
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28532
[Schwabhauser] p. 11Axiom A4axsegcon 29012  axtgsegcon 28548  df-trkgcb 28534
[Schwabhauser] p. 11Axiom A5ax5seg 29023  axtg5seg 28549  df-trkgcb 28534
[Schwabhauser] p. 11Axiom A6axbtwnid 29024  axtgbtwnid 28550  df-trkgb 28533
[Schwabhauser] p. 12Axiom A7axpasch 29026  axtgpasch 28551  df-trkgb 28533
[Schwabhauser] p. 12Axiom A8axlowdim2 29045  df-trkg2d 34842
[Schwabhauser] p. 13Axiom A8axtglowdim2 28554
[Schwabhauser] p. 13Axiom A9axtgupdim2 28555  df-trkg2d 34842
[Schwabhauser] p. 13Axiom A10axeuclid 29048  axtgeucl 28556  df-trkge 28535
[Schwabhauser] p. 13Axiom A11axcont 29061  axtgcont 28553  axtgcont1 28552  df-trkgb 28533
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36200
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36202
[Schwabhauser] p. 27Theorem 2.3cgrtr 36205
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36209
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36210  tgcgrcomimp 28561  tgcgrcoml 28563  tgcgrcomr 28562
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36215  tgcgrtriv 28568
[Schwabhauser] p. 28Theorem 2.105segofs 36219  tg5segofs 34850
[Schwabhauser] p. 28Definition 2.10df-afs 34847  df-ofs 36196
[Schwabhauser] p. 29Theorem 2.11cgrextend 36221  tgcgrextend 28569
[Schwabhauser] p. 29Theorem 2.12segconeq 36223  tgsegconeq 28570
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36235  btwntriv2 36225  tgbtwntriv2 28571
[Schwabhauser] p. 30Theorem 3.2btwncomim 36226  tgbtwncom 28572
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36229  tgbtwntriv1 28575
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36230  tgbtwnswapid 28576
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36236  btwnintr 36232  tgbtwnexch2 28580  tgbtwnintr 28577
[Schwabhauser] p. 30Theorem 3.6btwnexch 36238  btwnexch3 36233  tgbtwnexch 28582  tgbtwnexch3 28578
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36237  tgbtwnouttr 28581  tgbtwnouttr2 28579
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29044
[Schwabhauser] p. 32Theorem 3.14btwndiff 36240  tgbtwndiff 28590
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28583  trisegint 36241
[Schwabhauser] p. 34Theorem 4.2ifscgr 36257  tgifscgr 28592
[Schwabhauser] p. 34Theorem 4.11colcom 28642  colrot1 28643  colrot2 28644  lncom 28706  lnrot1 28707  lnrot2 28708
[Schwabhauser] p. 34Definition 4.1df-ifs 36253
[Schwabhauser] p. 35Theorem 4.3cgrsub 36258  tgcgrsub 28593
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36268  tgcgrxfr 28602
[Schwabhauser] p. 35Statement 4.4ercgrg 28601
[Schwabhauser] p. 35Definition 4.4df-cgr3 36254  df-cgrg 28595
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28595
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36269  tgbtwnxfr 28614
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36275  colinearperm2 36277  colinearperm3 36276  colinearperm4 36278  colinearperm5 36279
[Schwabhauser] p. 36Definition 4.8df-ismt 28617
[Schwabhauser] p. 36Definition 4.10df-colinear 36252  tgellng 28637  tglng 28630
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36280
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36288  lnxfr 28650
[Schwabhauser] p. 37Theorem 4.14lineext 36289  lnext 28651
[Schwabhauser] p. 37Theorem 4.16fscgr 36293  tgfscgr 28652
[Schwabhauser] p. 37Theorem 4.17linecgr 36294  lncgr 28653
[Schwabhauser] p. 37Definition 4.15df-fs 36255
[Schwabhauser] p. 38Theorem 4.18lineid 36296  lnid 28654
[Schwabhauser] p. 38Theorem 4.19idinside 36297  tgidinside 28655
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36314  tgbtwnconn1 28659
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36315  tgbtwnconn2 28660
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36316  tgbtwnconn3 28661
[Schwabhauser] p. 41Theorem 5.5brsegle2 36322
[Schwabhauser] p. 41Definition 5.4df-segle 36320  legov 28669
[Schwabhauser] p. 41Definition 5.5legov2 28670
[Schwabhauser] p. 42Remark 5.13legso 28683
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36323
[Schwabhauser] p. 42Theorem 5.7seglerflx 36325
[Schwabhauser] p. 42Theorem 5.8segletr 36327
[Schwabhauser] p. 42Theorem 5.9segleantisym 36328
[Schwabhauser] p. 42Theorem 5.10seglelin 36329
[Schwabhauser] p. 42Theorem 5.11seglemin 36326
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36331
[Schwabhauser] p. 42Proposition 5.7legid 28671
[Schwabhauser] p. 42Proposition 5.8legtrd 28673
[Schwabhauser] p. 42Proposition 5.9legtri3 28674
[Schwabhauser] p. 42Proposition 5.10legtrid 28675
[Schwabhauser] p. 42Proposition 5.11leg0 28676
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36338
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36339
[Schwabhauser] p. 43Theorem 6.4broutsideof 36334  df-outsideof 36333
[Schwabhauser] p. 43Definition 6.1broutsideof2 36335  ishlg 28686
[Schwabhauser] p. 44Theorem 6.4hlln 28691
[Schwabhauser] p. 44Theorem 6.5hlid 28693  outsideofrflx 36340
[Schwabhauser] p. 44Theorem 6.6hlcomb 28687  hlcomd 28688  outsideofcom 36341
[Schwabhauser] p. 44Theorem 6.7hltr 28694  outsideoftr 36342
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28702  outsideofeu 36344
[Schwabhauser] p. 44Definition 6.8df-ray 36351
[Schwabhauser] p. 45Part 2df-lines2 36352
[Schwabhauser] p. 45Theorem 6.13outsidele 36345
[Schwabhauser] p. 45Theorem 6.15lineunray 36360
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36361  tglineelsb2 28716
[Schwabhauser] p. 45Theorem 6.17linecom 36363  linerflx1 36362  linerflx2 36364  tglinecom 28719  tglinerflx1 28717  tglinerflx2 28718
[Schwabhauser] p. 45Theorem 6.18linethru 36366  tglinethru 28720
[Schwabhauser] p. 45Definition 6.14df-line2 36350  tglng 28630
[Schwabhauser] p. 45Proposition 6.13legbtwn 28678
[Schwabhauser] p. 46Theorem 6.19linethrueu 36369  tglinethrueu 28723
[Schwabhauser] p. 46Theorem 6.21lineintmo 36370  tglineineq 28727  tglineinteq 28729  tglineintmo 28726
[Schwabhauser] p. 46Theorem 6.23colline 28733
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28734
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28735
[Schwabhauser] p. 49Theorem 7.3mirinv 28750
[Schwabhauser] p. 49Theorem 7.7mirmir 28746
[Schwabhauser] p. 49Theorem 7.8mirreu3 28738
[Schwabhauser] p. 49Definition 7.5df-mir 28737  ismir 28743  mirbtwn 28742  mircgr 28741  mirfv 28740  mirval 28739
[Schwabhauser] p. 50Theorem 7.8mirreu 28748
[Schwabhauser] p. 50Theorem 7.9mireq 28749
[Schwabhauser] p. 50Theorem 7.10mirinv 28750
[Schwabhauser] p. 50Theorem 7.11mirf1o 28753
[Schwabhauser] p. 50Theorem 7.13miriso 28754
[Schwabhauser] p. 51Theorem 7.14mirmot 28759
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28756  mirbtwni 28755
[Schwabhauser] p. 51Theorem 7.16mircgrs 28757
[Schwabhauser] p. 51Theorem 7.17miduniq 28769
[Schwabhauser] p. 52Lemma 7.21symquadlem 28773
[Schwabhauser] p. 52Theorem 7.18miduniq1 28770
[Schwabhauser] p. 52Theorem 7.19miduniq2 28771
[Schwabhauser] p. 52Theorem 7.20colmid 28772
[Schwabhauser] p. 53Lemma 7.22krippen 28775
[Schwabhauser] p. 55Lemma 7.25midexlem 28776
[Schwabhauser] p. 57Theorem 8.2ragcom 28782
[Schwabhauser] p. 57Definition 8.1df-rag 28778  israg 28781
[Schwabhauser] p. 58Theorem 8.3ragcol 28783
[Schwabhauser] p. 58Theorem 8.4ragmir 28784
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28786
[Schwabhauser] p. 58Theorem 8.6ragflat2 28787
[Schwabhauser] p. 58Theorem 8.7ragflat 28788
[Schwabhauser] p. 58Theorem 8.8ragtriva 28789
[Schwabhauser] p. 58Theorem 8.9ragflat3 28790  ragncol 28793
[Schwabhauser] p. 58Theorem 8.10ragcgr 28791
[Schwabhauser] p. 59Theorem 8.12perpcom 28797
[Schwabhauser] p. 59Theorem 8.13ragperp 28801
[Schwabhauser] p. 59Theorem 8.14perpneq 28798
[Schwabhauser] p. 59Definition 8.11df-perpg 28780  isperp 28796
[Schwabhauser] p. 59Definition 8.13isperp2 28799
[Schwabhauser] p. 60Theorem 8.18foot 28806
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28814  colperpexlem2 28815
[Schwabhauser] p. 63Theorem 8.21colperpex 28817  colperpexlem3 28816
[Schwabhauser] p. 64Theorem 8.22mideu 28822  midex 28821
[Schwabhauser] p. 66Lemma 8.24opphllem 28819
[Schwabhauser] p. 67Theorem 9.2oppcom 28828
[Schwabhauser] p. 67Definition 9.1islnopp 28823
[Schwabhauser] p. 68Lemma 9.3opphllem2 28832
[Schwabhauser] p. 68Lemma 9.4opphllem5 28835  opphllem6 28836
[Schwabhauser] p. 69Theorem 9.5opphl 28838
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28551
[Schwabhauser] p. 70Theorem 9.6outpasch 28839
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28847
[Schwabhauser] p. 71Definition 9.7df-hpg 28842  hpgbr 28844
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28849
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28848
[Schwabhauser] p. 72Theorem 9.11hpgid 28850
[Schwabhauser] p. 72Theorem 9.12hpgcom 28851
[Schwabhauser] p. 72Theorem 9.13hpgtr 28852
[Schwabhauser] p. 73Theorem 9.18colopp 28853
[Schwabhauser] p. 73Theorem 9.19colhp 28854
[Schwabhauser] p. 88Theorem 10.2lmieu 28868
[Schwabhauser] p. 88Definition 10.1df-mid 28858
[Schwabhauser] p. 89Theorem 10.4lmicom 28872
[Schwabhauser] p. 89Theorem 10.5lmilmi 28873
[Schwabhauser] p. 89Theorem 10.6lmireu 28874
[Schwabhauser] p. 89Theorem 10.7lmieq 28875
[Schwabhauser] p. 89Theorem 10.8lmiinv 28876
[Schwabhauser] p. 89Theorem 10.9lmif1o 28879
[Schwabhauser] p. 89Theorem 10.10lmiiso 28881
[Schwabhauser] p. 89Definition 10.3df-lmi 28859
[Schwabhauser] p. 90Theorem 10.11lmimot 28882
[Schwabhauser] p. 91Theorem 10.12hypcgr 28885
[Schwabhauser] p. 92Theorem 10.14lmiopp 28886
[Schwabhauser] p. 92Theorem 10.15lnperpex 28887
[Schwabhauser] p. 92Theorem 10.16trgcopy 28888  trgcopyeu 28890
[Schwabhauser] p. 95Definition 11.2dfcgra2 28914
[Schwabhauser] p. 95Definition 11.3iscgra 28893
[Schwabhauser] p. 95Proposition 11.4cgracgr 28902
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28900  cgrahl2 28901
[Schwabhauser] p. 96Theorem 11.6cgraid 28903
[Schwabhauser] p. 96Theorem 11.9cgraswap 28904
[Schwabhauser] p. 97Theorem 11.7cgracom 28906
[Schwabhauser] p. 97Theorem 11.8cgratr 28907
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28910  cgrahl 28911
[Schwabhauser] p. 98Theorem 11.13sacgr 28915
[Schwabhauser] p. 98Theorem 11.14oacgr 28916
[Schwabhauser] p. 98Theorem 11.15acopy 28917  acopyeu 28918
[Schwabhauser] p. 101Theorem 11.24inagswap 28925
[Schwabhauser] p. 101Theorem 11.25inaghl 28929
[Schwabhauser] p. 101Definition 11.23isinag 28922
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28937
[Schwabhauser] p. 102Definition 11.27df-leag 28930  isleag 28931
[Schwabhauser] p. 107Theorem 11.49tgsas 28939  tgsas1 28938  tgsas2 28940  tgsas3 28941
[Schwabhauser] p. 108Theorem 11.50tgasa 28943  tgasa1 28942
[Schwabhauser] p. 109Theorem 11.51tgsss1 28944  tgsss2 28945  tgsss3 28946
[Shapiro] p. 230Theorem 6.5.1dchrhash 27250  dchrsum 27248  dchrsum2 27247  sumdchr 27251
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27252  sum2dchr 27253
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20009  ablfacrp2 20010
[Shapiro], p. 328Equation 9.2.4vmasum 27195
[Shapiro], p. 329Equation 9.2.7logfac2 27196
[Shapiro], p. 329Equation 9.2.9logfacrlim 27203
[Shapiro], p. 331Equation 9.2.13vmadivsum 27461
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27464
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27518  vmalogdivsum2 27517
[Shapiro], p. 375Theorem 9.4.1dirith 27508  dirith2 27507
[Shapiro], p. 375Equation 9.4.3rplogsum 27506  rpvmasum 27505  rpvmasum2 27491
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27466
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27504
[Shapiro], p. 377Lemma 9.4.1dchrisum 27471  dchrisumlem1 27468  dchrisumlem2 27469  dchrisumlem3 27470  dchrisumlema 27467
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27474
[Shapiro], p. 379Equation 9.4.16dchrmusum 27503  dchrmusumlem 27501  dchrvmasumlem 27502
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27473
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27475
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27499  dchrisum0re 27492  dchrisumn0 27500
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27485
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27489
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27490
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27545  pntrsumbnd2 27546  pntrsumo1 27544
[Shapiro], p. 405Equation 10.2.1mudivsum 27509
[Shapiro], p. 406Equation 10.2.6mulogsum 27511
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27513
[Shapiro], p. 407Equation 10.2.8mulog2sum 27516
[Shapiro], p. 418Equation 10.4.6logsqvma 27521
[Shapiro], p. 418Equation 10.4.8logsqvma2 27522
[Shapiro], p. 419Equation 10.4.10selberg 27527
[Shapiro], p. 420Equation 10.4.12selberg2lem 27529
[Shapiro], p. 420Equation 10.4.14selberg2 27530
[Shapiro], p. 422Equation 10.6.7selberg3 27538
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27539
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27536  selberg3lem2 27537
[Shapiro], p. 422Equation 10.4.23selberg4 27540
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27534
[Shapiro], p. 428Equation 10.6.2selbergr 27547
[Shapiro], p. 429Equation 10.6.8selberg3r 27548
[Shapiro], p. 430Equation 10.6.11selberg4r 27549
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27563
[Shapiro], p. 434Equation 10.6.27pntlema 27575  pntlemb 27576  pntlemc 27574  pntlemd 27573  pntlemg 27577
[Shapiro], p. 435Equation 10.6.29pntlema 27575
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27567
[Shapiro], p. 436Lemma 10.6.2pntibnd 27572
[Shapiro], p. 436Equation 10.6.34pntlema 27575
[Shapiro], p. 436Equation 10.6.35pntlem3 27588  pntleml 27590
[Stewart] p. 91Lemma 7.3constrss 33920
[Stewart] p. 92Definition 7.4.df-constr 33907
[Stewart] p. 96Theorem 7.10constraddcl 33939  constrinvcl 33950  constrmulcl 33948  constrnegcl 33940  constrsqrtcl 33956
[Stewart] p. 97Theorem 7.11constrextdg2 33926
[Stewart] p. 98Theorem 7.12constrext2chn 33936
[Stewart] p. 99Theorem 7.132sqr3nconstr 33958
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33968
[Stoll] p. 13Definition corresponds to dfsymdif3 4260
[Stoll] p. 16Exercise 4.40dif 4359  dif0 4332
[Stoll] p. 16Exercise 4.8difdifdir 4446
[Stoll] p. 17Theorem 5.1(5)unvdif 4429
[Stoll] p. 19Theorem 5.2(13)undm 4251
[Stoll] p. 19Theorem 5.2(13')indm 4252
[Stoll] p. 20Remarkinvdif 4233
[Stoll] p. 25Definition of ordered tripledf-ot 4591
[Stoll] p. 43Definitionuniiun 5016
[Stoll] p. 44Definitionintiin 5017
[Stoll] p. 45Definitiondf-iin 4951
[Stoll] p. 45Definition indexed uniondf-iun 4950
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4260
[Strang] p. 242Section 6.3expgrowth 44680
[Suppes] p. 22Theorem 2eq0 4304  eq0f 4301
[Suppes] p. 22Theorem 4eqss 3951  eqssd 3953  eqssi 3952
[Suppes] p. 23Theorem 5ss0 4356  ss0b 4355
[Suppes] p. 23Theorem 6sstr 3944  sstrALT2 45179
[Suppes] p. 23Theorem 7pssirr 4057
[Suppes] p. 23Theorem 8pssn2lp 4058
[Suppes] p. 23Theorem 9psstr 4061
[Suppes] p. 23Theorem 10pssss 4052
[Suppes] p. 25Theorem 12elin 3919  elun 4107
[Suppes] p. 26Theorem 15inidm 4181
[Suppes] p. 26Theorem 16in0 4349
[Suppes] p. 27Theorem 23unidm 4111
[Suppes] p. 27Theorem 24un0 4348
[Suppes] p. 27Theorem 25ssun1 4132
[Suppes] p. 27Theorem 26ssequn1 4140
[Suppes] p. 27Theorem 27unss 4144
[Suppes] p. 27Theorem 28indir 4240
[Suppes] p. 27Theorem 29undir 4241
[Suppes] p. 28Theorem 32difid 4330
[Suppes] p. 29Theorem 33difin 4226
[Suppes] p. 29Theorem 34indif 4234
[Suppes] p. 29Theorem 35undif1 4430
[Suppes] p. 29Theorem 36difun2 4435
[Suppes] p. 29Theorem 37difin0 4428
[Suppes] p. 29Theorem 38disjdif 4426
[Suppes] p. 29Theorem 39difundi 4244
[Suppes] p. 29Theorem 40difindi 4246
[Suppes] p. 30Theorem 41nalset 5260
[Suppes] p. 39Theorem 61uniss 4873
[Suppes] p. 39Theorem 65uniop 5471
[Suppes] p. 41Theorem 70intsn 4941
[Suppes] p. 42Theorem 71intpr 4939  intprg 4938
[Suppes] p. 42Theorem 73op1stb 5427
[Suppes] p. 42Theorem 78intun 4937
[Suppes] p. 44Definition 15(a)dfiun2 4989  dfiun2g 4987
[Suppes] p. 44Definition 15(b)dfiin2 4990
[Suppes] p. 47Theorem 86elpw 4560  elpw2 5281  elpw2g 5280  elpwg 4559  elpwgdedVD 45261
[Suppes] p. 47Theorem 87pwid 4578
[Suppes] p. 47Theorem 89pw0 4770
[Suppes] p. 48Theorem 90pwpw0 4771
[Suppes] p. 52Theorem 101xpss12 5647
[Suppes] p. 52Theorem 102xpindi 5790  xpindir 5791
[Suppes] p. 52Theorem 103xpundi 5701  xpundir 5702
[Suppes] p. 54Theorem 105elirrv 9514
[Suppes] p. 58Theorem 2relss 5739
[Suppes] p. 59Theorem 4eldm 5857  eldm2 5858  eldm2g 5856  eldmg 5855
[Suppes] p. 59Definition 3df-dm 5642
[Suppes] p. 60Theorem 6dmin 5868
[Suppes] p. 60Theorem 8rnun 6111
[Suppes] p. 60Theorem 9rnin 6112
[Suppes] p. 60Definition 4dfrn2 5845
[Suppes] p. 61Theorem 11brcnv 5839  brcnvg 5836
[Suppes] p. 62Equation 5elcnv 5833  elcnv2 5834
[Suppes] p. 62Theorem 12relcnv 6071
[Suppes] p. 62Theorem 15cnvin 6110
[Suppes] p. 62Theorem 16cnvun 6108
[Suppes] p. 63Definitiondftrrels2 38899
[Suppes] p. 63Theorem 20co02 6227
[Suppes] p. 63Theorem 21dmcoss 5932
[Suppes] p. 63Definition 7df-co 5641
[Suppes] p. 64Theorem 26cnvco 5842
[Suppes] p. 64Theorem 27coass 6232
[Suppes] p. 65Theorem 31resundi 5960
[Suppes] p. 65Theorem 34elima 6032  elima2 6033  elima3 6034  elimag 6031
[Suppes] p. 65Theorem 35imaundi 6115
[Suppes] p. 66Theorem 40dminss 6119
[Suppes] p. 66Theorem 41imainss 6120
[Suppes] p. 67Exercise 11cnvxp 6123
[Suppes] p. 81Definition 34dfec2 8648
[Suppes] p. 82Theorem 72elec 8692  elecALTV 38511  elecg 8690
[Suppes] p. 82Theorem 73eqvrelth 38935  erth 8700  erth2 8701
[Suppes] p. 83Theorem 74eqvreldisj 38938  erdisj 8703
[Suppes] p. 83Definition 35, df-parts 39108  dfmembpart2 39113
[Suppes] p. 89Theorem 96map0b 8833
[Suppes] p. 89Theorem 97map0 8837  map0g 8834
[Suppes] p. 89Theorem 98mapsn 8838  mapsnd 8836
[Suppes] p. 89Theorem 99mapss 8839
[Suppes] p. 91Definition 12(ii)alephsuc 9990
[Suppes] p. 91Definition 12(iii)alephlim 9989
[Suppes] p. 92Theorem 1enref 8934  enrefg 8933
[Suppes] p. 92Theorem 2ensym 8952  ensymb 8951  ensymi 8953
[Suppes] p. 92Theorem 3entr 8955
[Suppes] p. 92Theorem 4unen 8994
[Suppes] p. 94Theorem 15endom 8928
[Suppes] p. 94Theorem 16ssdomg 8949
[Suppes] p. 94Theorem 17domtr 8956
[Suppes] p. 95Theorem 18sbth 9037
[Suppes] p. 97Theorem 23canth2 9070  canth2g 9071
[Suppes] p. 97Definition 3brsdom2 9041  df-sdom 8898  dfsdom2 9040
[Suppes] p. 97Theorem 21(i)sdomirr 9054
[Suppes] p. 97Theorem 22(i)domnsym 9043
[Suppes] p. 97Theorem 21(ii)sdomnsym 9042
[Suppes] p. 97Theorem 22(ii)domsdomtr 9052
[Suppes] p. 97Theorem 22(iv)brdom2 8931
[Suppes] p. 97Theorem 21(iii)sdomtr 9055
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9050
[Suppes] p. 98Exercise 4fundmen 8980  fundmeng 8981
[Suppes] p. 98Exercise 6xpdom3 9015
[Suppes] p. 98Exercise 11sdomentr 9051
[Suppes] p. 104Theorem 37fofi 9225
[Suppes] p. 104Theorem 38pwfi 9231
[Suppes] p. 105Theorem 40pwfi 9231
[Suppes] p. 111Axiom for cardinal numberscarden 10473
[Suppes] p. 130Definition 3df-tr 5208
[Suppes] p. 132Theorem 9ssonuni 7735
[Suppes] p. 134Definition 6df-suc 6331
[Suppes] p. 136Theorem Schema 22findes 7852  finds 7848  finds1 7851  finds2 7850
[Suppes] p. 151Theorem 42isfinite 9573  isfinite2 9210  isfiniteg 9212  unbnn 9208
[Suppes] p. 162Definition 5df-ltnq 10841  df-ltpq 10833
[Suppes] p. 197Theorem Schema 4tfindes 7815  tfinds 7812  tfinds2 7816
[Suppes] p. 209Theorem 18oaord1 8488
[Suppes] p. 209Theorem 21oaword2 8490
[Suppes] p. 211Theorem 25oaass 8498
[Suppes] p. 225Definition 8iscard2 9900
[Suppes] p. 227Theorem 56ondomon 10485
[Suppes] p. 228Theorem 59harcard 9902
[Suppes] p. 228Definition 12(i)aleph0 9988
[Suppes] p. 228Theorem Schema 61onintss 6377
[Suppes] p. 228Theorem Schema 62onminesb 7748  onminsb 7749
[Suppes] p. 229Theorem 64alephval2 10495
[Suppes] p. 229Theorem 65alephcard 9992
[Suppes] p. 229Theorem 66alephord2i 9999
[Suppes] p. 229Theorem 67alephnbtwn 9993
[Suppes] p. 229Definition 12df-aleph 9864
[Suppes] p. 242Theorem 6weth 10417
[Suppes] p. 242Theorem 8entric 10479
[Suppes] p. 242Theorem 9carden 10473
[Szendrei] p. 11Line 6df-cloneop 35909
[Szendrei] p. 11Paragraph 3df-suppos 35913
[TakeutiZaring] p. 8Axiom 1ax-ext 2709
[TakeutiZaring] p. 13Definition 4.5df-cleq 2729
[TakeutiZaring] p. 13Proposition 4.6df-clel 2812
[TakeutiZaring] p. 13Proposition 4.9cvjust 2731
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2757
[TakeutiZaring] p. 14Definition 4.16df-oprab 7372
[TakeutiZaring] p. 14Proposition 4.14ru 3740
[TakeutiZaring] p. 15Axiom 2zfpair 5368
[TakeutiZaring] p. 15Exercise 1elpr 4607  elpr2 4609  elpr2g 4608  elprg 4605
[TakeutiZaring] p. 15Exercise 2elsn 4597  elsn2 4624  elsn2g 4623  elsng 4596  velsn 4598
[TakeutiZaring] p. 15Exercise 3elop 5423
[TakeutiZaring] p. 15Exercise 4sneq 4592  sneqr 4798
[TakeutiZaring] p. 15Definition 5.1dfpr2 4603  dfsn2 4595  dfsn2ALT 4604
[TakeutiZaring] p. 16Axiom 3uniex 7696
[TakeutiZaring] p. 16Exercise 6opth 5432
[TakeutiZaring] p. 16Exercise 7opex 5419
[TakeutiZaring] p. 16Exercise 8rext 5403
[TakeutiZaring] p. 16Corollary 5.8unex 7699  unexg 7698
[TakeutiZaring] p. 16Definition 5.3dftp2 4650
[TakeutiZaring] p. 16Definition 5.5df-uni 4866
[TakeutiZaring] p. 16Definition 5.6df-in 3910  df-un 3908
[TakeutiZaring] p. 16Proposition 5.7unipr 4882  uniprg 4881
[TakeutiZaring] p. 17Axiom 4vpwex 5324
[TakeutiZaring] p. 17Exercise 1eltp 4648
[TakeutiZaring] p. 17Exercise 5elsuc 6397  elsucg 6395  sstr2 3942
[TakeutiZaring] p. 17Exercise 6uncom 4112
[TakeutiZaring] p. 17Exercise 7incom 4163
[TakeutiZaring] p. 17Exercise 8unass 4126
[TakeutiZaring] p. 17Exercise 9inass 4182
[TakeutiZaring] p. 17Exercise 10indi 4238
[TakeutiZaring] p. 17Exercise 11undi 4239
[TakeutiZaring] p. 17Definition 5.9df-pss 3923  df-ss 3920
[TakeutiZaring] p. 17Definition 5.10df-pw 4558
[TakeutiZaring] p. 18Exercise 7unss2 4141
[TakeutiZaring] p. 18Exercise 9dfss2 3921  sseqin2 4177
[TakeutiZaring] p. 18Exercise 10ssid 3958
[TakeutiZaring] p. 18Exercise 12inss1 4191  inss2 4192
[TakeutiZaring] p. 18Exercise 13nss 4000
[TakeutiZaring] p. 18Exercise 15unieq 4876
[TakeutiZaring] p. 18Exercise 18sspwb 5404  sspwimp 45262  sspwimpALT 45269  sspwimpALT2 45272  sspwimpcf 45264
[TakeutiZaring] p. 18Exercise 19pweqb 5411
[TakeutiZaring] p. 19Axiom 5ax-rep 5226
[TakeutiZaring] p. 20Definitiondf-rab 3402
[TakeutiZaring] p. 20Corollary 5.160ex 5254
[TakeutiZaring] p. 20Definition 5.12df-dif 3906
[TakeutiZaring] p. 20Definition 5.14dfnul2 4290
[TakeutiZaring] p. 20Proposition 5.15difid 4330
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4307  n0f 4303  neq0 4306  neq0f 4302
[TakeutiZaring] p. 21Axiom 6zfreg 9513
[TakeutiZaring] p. 21Axiom 6'zfregs 9653
[TakeutiZaring] p. 21Theorem 5.22setind 9668
[TakeutiZaring] p. 21Definition 5.20df-v 3444
[TakeutiZaring] p. 21Proposition 5.21vprc 5262
[TakeutiZaring] p. 22Exercise 10ss 4354
[TakeutiZaring] p. 22Exercise 3ssex 5268  ssexg 5270
[TakeutiZaring] p. 22Exercise 4inex1 5264
[TakeutiZaring] p. 22Exercise 5ruv 9522
[TakeutiZaring] p. 22Exercise 6elirr 9516
[TakeutiZaring] p. 22Exercise 7ssdif0 4320
[TakeutiZaring] p. 22Exercise 11difdif 4089
[TakeutiZaring] p. 22Exercise 13undif3 4254  undif3VD 45226
[TakeutiZaring] p. 22Exercise 14difss 4090
[TakeutiZaring] p. 22Exercise 15sscon 4097
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3053
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3063
[TakeutiZaring] p. 23Proposition 6.2xpex 7708  xpexg 7705
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5639
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6571
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6747  fun11 6574
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6513  svrelfun 6572
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5844
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5846
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5644
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5645
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5641
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6160  dfrel2 6155
[TakeutiZaring] p. 25Exercise 3xpss 5648
[TakeutiZaring] p. 25Exercise 5relun 5768
[TakeutiZaring] p. 25Exercise 6reluni 5775
[TakeutiZaring] p. 25Exercise 9inxp 5788
[TakeutiZaring] p. 25Exercise 12relres 5972
[TakeutiZaring] p. 25Exercise 13opelres 5952  opelresi 5954
[TakeutiZaring] p. 25Exercise 14dmres 5979
[TakeutiZaring] p. 25Exercise 15resss 5968
[TakeutiZaring] p. 25Exercise 17resabs1 5973
[TakeutiZaring] p. 25Exercise 18funres 6542
[TakeutiZaring] p. 25Exercise 24relco 6075
[TakeutiZaring] p. 25Exercise 29funco 6540
[TakeutiZaring] p. 25Exercise 30f1co 6749
[TakeutiZaring] p. 26Definition 6.10eu2 2610
[TakeutiZaring] p. 26Definition 6.11conventions 30487  df-fv 6508  fv3 6860
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7877  cnvexg 7876
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7861  dmexg 7853
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7862  rnexg 7854
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44798
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7872
[TakeutiZaring] p. 27Corollary 6.13fvex 6855
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47523  tz6.12-1-afv2 47590  tz6.12-1 6865  tz6.12-afv 47522  tz6.12-afv2 47589  tz6.12 6866  tz6.12c-afv2 47591  tz6.12c 6864
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47586  tz6.12-2 6829  tz6.12i-afv2 47592  tz6.12i 6868
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6503
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6504
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6506  wfo 6498
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6505  wf1 6497
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6507  wf1o 6499
[TakeutiZaring] p. 28Exercise 4eqfnfv 6985  eqfnfv2 6986  eqfnfv2f 6989
[TakeutiZaring] p. 28Exercise 5fvco 6940
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7173
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7171
[TakeutiZaring] p. 29Exercise 9funimaex 6588  funimaexg 6587
[TakeutiZaring] p. 29Definition 6.18df-br 5101
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5541
[TakeutiZaring] p. 30Definition 6.21dffr2 5593  dffr3 6066  eliniseg 6061  iniseg 6064
[TakeutiZaring] p. 30Definition 6.22df-eprel 5532
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5609  fr3nr 7727  frirr 5608
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5585
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7729
[TakeutiZaring] p. 31Exercise 1frss 5596
[TakeutiZaring] p. 31Exercise 4wess 5618
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6313  tz6.26i 6314  wefrc 5626  wereu2 5629
[TakeutiZaring] p. 32Theorem 6.27wfi 6315  wfii 6316
[TakeutiZaring] p. 32Definition 6.28df-isom 6509
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7285
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7286
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7292
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7293
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7294
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7298
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7305
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7307
[TakeutiZaring] p. 35Notationwtr 5207
[TakeutiZaring] p. 35Theorem 7.2trelpss 44799  tz7.2 5615
[TakeutiZaring] p. 35Definition 7.1dftr3 5212
[TakeutiZaring] p. 36Proposition 7.4ordwe 6338
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6346
[TakeutiZaring] p. 36Proposition 7.6ordelord 6347  ordelordALT 44882  ordelordALTVD 45211
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6353  ordelssne 6352
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6351
[TakeutiZaring] p. 37Proposition 7.9ordin 6355
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7737
[TakeutiZaring] p. 38Corollary 7.15ordsson 7738
[TakeutiZaring] p. 38Definition 7.11df-on 6329
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6357
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44894  ordon 7732
[TakeutiZaring] p. 38Proposition 7.13onprc 7733
[TakeutiZaring] p. 39Theorem 7.17tfi 7805
[TakeutiZaring] p. 40Exercise 3ontr2 6373
[TakeutiZaring] p. 40Exercise 7dftr2 5209
[TakeutiZaring] p. 40Exercise 9onssmin 7747
[TakeutiZaring] p. 40Exercise 11unon 7783
[TakeutiZaring] p. 40Exercise 12ordun 6431
[TakeutiZaring] p. 40Exercise 14ordequn 6430
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7734
[TakeutiZaring] p. 40Proposition 7.20elssuni 4896
[TakeutiZaring] p. 41Definition 7.22df-suc 6331
[TakeutiZaring] p. 41Proposition 7.23sssucid 6407  sucidg 6408
[TakeutiZaring] p. 41Proposition 7.24onsuc 7765
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6421  ordnbtwn 6420
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7780
[TakeutiZaring] p. 42Exercise 1df-lim 6330
[TakeutiZaring] p. 42Exercise 4omssnlim 7833
[TakeutiZaring] p. 42Exercise 7ssnlim 7838
[TakeutiZaring] p. 42Exercise 8onsucssi 7793  ordelsuc 7772
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7774
[TakeutiZaring] p. 42Definition 7.27nlimon 7803
[TakeutiZaring] p. 42Definition 7.28dfom2 7820
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7841
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7842
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7843
[TakeutiZaring] p. 43Remarkomon 7830
[TakeutiZaring] p. 43Axiom 7inf3 9556  omex 9564
[TakeutiZaring] p. 43Theorem 7.32ordom 7828
[TakeutiZaring] p. 43Corollary 7.31find 7847
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7844
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7845
[TakeutiZaring] p. 44Exercise 1limomss 7823
[TakeutiZaring] p. 44Exercise 2int0 4919
[TakeutiZaring] p. 44Exercise 3trintss 5225
[TakeutiZaring] p. 44Exercise 4intss1 4920
[TakeutiZaring] p. 44Exercise 5intex 5291
[TakeutiZaring] p. 44Exercise 6oninton 7750
[TakeutiZaring] p. 44Exercise 11ordintdif 6376
[TakeutiZaring] p. 44Definition 7.35df-int 4905
[TakeutiZaring] p. 44Proposition 7.34noinfep 9581
[TakeutiZaring] p. 45Exercise 4onint 7745
[TakeutiZaring] p. 47Lemma 1tfrlem1 8317
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8338
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8339
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8340
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8347  tz7.44-2 8348  tz7.44-3 8349
[TakeutiZaring] p. 50Exercise 1smogt 8309
[TakeutiZaring] p. 50Exercise 3smoiso 8304
[TakeutiZaring] p. 50Definition 7.46df-smo 8288
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8386  tz7.49c 8387
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8384
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8383
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8385
[TakeutiZaring] p. 53Proposition 7.532eu5 2657
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9933
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9934
[TakeutiZaring] p. 56Definition 8.1oalim 8469  oasuc 8461
[TakeutiZaring] p. 57Remarktfindsg 7813
[TakeutiZaring] p. 57Proposition 8.2oacl 8472
[TakeutiZaring] p. 57Proposition 8.3oa0 8453  oa0r 8475
[TakeutiZaring] p. 57Proposition 8.16omcl 8473
[TakeutiZaring] p. 58Corollary 8.5oacan 8485
[TakeutiZaring] p. 58Proposition 8.4nnaord 8557  nnaordi 8556  oaord 8484  oaordi 8483
[TakeutiZaring] p. 59Proposition 8.6iunss2 5007  uniss2 4899
[TakeutiZaring] p. 59Proposition 8.7oawordri 8487
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8492  oawordex 8494
[TakeutiZaring] p. 59Proposition 8.9nnacl 8549
[TakeutiZaring] p. 59Proposition 8.10oaabs 8586
[TakeutiZaring] p. 60Remarkoancom 9572
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8497
[TakeutiZaring] p. 62Exercise 1nnarcl 8554
[TakeutiZaring] p. 62Exercise 5oaword1 8489
[TakeutiZaring] p. 62Definition 8.15om0x 8456  omlim 8470  omsuc 8463
[TakeutiZaring] p. 62Definition 8.15(a)om0 8454
[TakeutiZaring] p. 63Proposition 8.17nnecl 8551  nnmcl 8550
[TakeutiZaring] p. 63Proposition 8.19nnmord 8570  nnmordi 8569  omord 8505  omordi 8503
[TakeutiZaring] p. 63Proposition 8.20omcan 8506
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8574  omwordri 8509
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8476
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8479  om1r 8480
[TakeutiZaring] p. 64Proposition 8.22om00 8512
[TakeutiZaring] p. 64Proposition 8.23omordlim 8514
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8515
[TakeutiZaring] p. 64Proposition 8.25odi 8516
[TakeutiZaring] p. 65Theorem 8.26omass 8517
[TakeutiZaring] p. 67Definition 8.30nnesuc 8546  oe0 8459  oelim 8471  oesuc 8464  onesuc 8467
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8457
[TakeutiZaring] p. 67Proposition 8.32oen0 8524
[TakeutiZaring] p. 67Proposition 8.33oeordi 8525
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8458
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8482
[TakeutiZaring] p. 68Corollary 8.34oeord 8526
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8532
[TakeutiZaring] p. 68Proposition 8.35oewordri 8530
[TakeutiZaring] p. 68Proposition 8.37oeworde 8531
[TakeutiZaring] p. 69Proposition 8.41oeoa 8535
[TakeutiZaring] p. 70Proposition 8.42oeoe 8537
[TakeutiZaring] p. 73Theorem 9.1trcl 9649  tz9.1 9650
[TakeutiZaring] p. 76Definition 9.9df-r1 9688  r10 9692  r1lim 9696  r1limg 9695  r1suc 9694  r1sucg 9693
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9704  r1ord2 9705  r1ordg 9702
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9714
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9739  tz9.13 9715  tz9.13g 9716
[TakeutiZaring] p. 79Definition 9.14df-rank 9689  rankval 9740  rankvalb 9721  rankvalg 9741
[TakeutiZaring] p. 79Proposition 9.16rankel 9763  rankelb 9748
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9777  rankval3 9764  rankval3b 9750
[TakeutiZaring] p. 79Proposition 9.18rankonid 9753
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9719
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9758  rankr1c 9745  rankr1g 9756
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9759
[TakeutiZaring] p. 80Exercise 1rankss 9773  rankssb 9772
[TakeutiZaring] p. 80Exercise 2unbndrank 9766
[TakeutiZaring] p. 80Proposition 9.19bndrank 9765
[TakeutiZaring] p. 83Axiom of Choiceac4 10397  dfac3 10043
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9952  numth 10394  numth2 10393
[TakeutiZaring] p. 85Definition 10.4cardval 10468
[TakeutiZaring] p. 85Proposition 10.5cardid 10469  cardid2 9877
[TakeutiZaring] p. 85Proposition 10.9oncard 9884
[TakeutiZaring] p. 85Proposition 10.10carden 10473
[TakeutiZaring] p. 85Proposition 10.11cardidm 9883
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9868
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9889
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9881
[TakeutiZaring] p. 87Proposition 10.15pwen 9090
[TakeutiZaring] p. 88Exercise 1en0 8967
[TakeutiZaring] p. 88Exercise 7infensuc 9095
[TakeutiZaring] p. 89Exercise 10omxpen 9019
[TakeutiZaring] p. 90Corollary 10.23cardnn 9887
[TakeutiZaring] p. 90Definition 10.27alephiso 10020
[TakeutiZaring] p. 90Proposition 10.20nneneq 9142
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9150
[TakeutiZaring] p. 90Proposition 10.26alephprc 10021
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9147
[TakeutiZaring] p. 91Exercise 2alephle 10010
[TakeutiZaring] p. 91Exercise 3aleph0 9988
[TakeutiZaring] p. 91Exercise 4cardlim 9896
[TakeutiZaring] p. 91Exercise 7infpss 10138
[TakeutiZaring] p. 91Exercise 8infcntss 9235
[TakeutiZaring] p. 91Definition 10.29df-fin 8899  isfi 8924
[TakeutiZaring] p. 92Proposition 10.32onfin 9151
[TakeutiZaring] p. 92Proposition 10.34imadomg 10456
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9012
[TakeutiZaring] p. 93Proposition 10.35fodomb 10448
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10108  unxpdom 9171
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9898  cardsdomelir 9897
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9173
[TakeutiZaring] p. 94Proposition 10.39infxpen 9936
[TakeutiZaring] p. 95Definition 10.42df-map 8777
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10484  infxpidm2 9939
[TakeutiZaring] p. 95Proposition 10.41infdju 10129  infxp 10136
[TakeutiZaring] p. 96Proposition 10.44pw2en 9024  pw2f1o 9022
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9083
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10409
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10404  ac6s5 10413
[TakeutiZaring] p. 98Theorem 10.47unidom 10465
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10466  uniimadomf 10467
[TakeutiZaring] p. 100Definition 11.1cfcof 10196
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10191
[TakeutiZaring] p. 102Exercise 1cfle 10176
[TakeutiZaring] p. 102Exercise 2cf0 10173
[TakeutiZaring] p. 102Exercise 3cfsuc 10179
[TakeutiZaring] p. 102Exercise 4cfom 10186
[TakeutiZaring] p. 102Proposition 11.9coftr 10195
[TakeutiZaring] p. 103Theorem 11.15alephreg 10505
[TakeutiZaring] p. 103Proposition 11.11cardcf 10174
[TakeutiZaring] p. 103Proposition 11.13alephsing 10198
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10019
[TakeutiZaring] p. 104Proposition 11.16carduniima 10018
[TakeutiZaring] p. 104Proposition 11.18alephfp 10030  alephfp2 10031
[TakeutiZaring] p. 106Theorem 11.20gchina 10622
[TakeutiZaring] p. 106Theorem 11.21mappwen 10034
[TakeutiZaring] p. 107Theorem 11.26konigth 10492
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10506
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10507
[Tarski] p. 67Axiom B5ax-c5 39248
[Tarski] p. 67Scheme B5sp 2191
[Tarski] p. 68Lemma 6avril1 30550  equid 2014
[Tarski] p. 69Lemma 7equcomi 2019
[Tarski] p. 70Lemma 14spim 2392  spime 2394  spimew 1973
[Tarski] p. 70Lemma 16ax-12 2185  ax-c15 39254  ax12i 1968
[Tarski] p. 70Lemmas 16 and 17sb6 2091
[Tarski] p. 75Axiom B7ax6v 1970
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1912  ax5ALT 39272
[Tarski], p. 75Scheme B8 of system S2ax-7 2010  ax-8 2116  ax-9 2124
[Tarski1999] p. 178Axiom 4axtgsegcon 28548
[Tarski1999] p. 178Axiom 5axtg5seg 28549
[Tarski1999] p. 179Axiom 7axtgpasch 28551
[Tarski1999] p. 180Axiom 7.1axtgpasch 28551
[Tarski1999] p. 185Axiom 11axtgcont1 28552
[Truss] p. 114Theorem 5.18ruc 16180
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37899
[Viaclovsky8] p. 3Proposition 7ismblfin 37901
[Weierstrass] p. 272Definitiondf-mdet 22541  mdetuni 22578
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 904
[WhiteheadRussell] p. 96Axiom *1.3olc 869
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 870
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 920
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 970
[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 37689
[WhiteheadRussell] p. 100Theorem *2.05frege5 44145  imim2 58  wl-luk-imim2 37684
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47368  imim1 83
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 897
[WhiteheadRussell] p. 101Theorem *2.06barbara 2664  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 903
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-luk-id 37687
[WhiteheadRussell] p. 101Theorem *2.11exmid 895
[WhiteheadRussell] p. 101Theorem *2.12notnot 142
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 898
[WhiteheadRussell] p. 102Theorem *2.14notnotr 130  notnotrALT2 45271  wl-luk-notnotr 37688
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44175  axfrege28 44174  con3 153
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 128
[WhiteheadRussell] p. 104Theorem *2.2orc 868
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 925
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 123  wl-luk-pm2.21 37681
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 124
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 890
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 942
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30488  pm2.27 42  wl-luk-pm2.27 37679
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 923
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38611
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 924
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 972
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 973
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 971
[WhiteheadRussell] p. 105Definition *2.33df-3or 1088
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 907
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 908
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 945
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 56
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 882
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 883
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 169  pm2.5g 168
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 191
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 884
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 885
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 886
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 172
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 173
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 852
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 853
[WhiteheadRussell] p. 107Theorem *2.55orel1 889
[WhiteheadRussell] p. 107Theorem *2.56orel2 891
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 192
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 900
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 943
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 944
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 193
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 892  pm2.67 893
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 176  pm2.521g 174  pm2.521g2 175
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 899
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 975
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 901
[WhiteheadRussell] p. 108Theorem *2.69looinv 203
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 976
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 977
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 934
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 932
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 974
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 978
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 84
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 933
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 109
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 994
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 469  pm3.2im 160
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 995
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 996
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 997
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 998
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 471
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 459
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 402
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 803
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 448
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 449
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 482  simplim 167
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 484  simprim 166
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 765
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 766
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 808
[WhiteheadRussell] p. 113Fact)pm3.45 623
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 810
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 492
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 493
[WhiteheadRussell] p. 113Theorem *3.44jao 963  pm3.44 962
[WhiteheadRussell] p. 113Theorem *3.47anim12 809
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 473
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 966
[WhiteheadRussell] p. 116Theorem *4.1con34b 316
[WhiteheadRussell] p. 117Theorem *4.2biid 261
[WhiteheadRussell] p. 117Theorem *4.11notbi 319
[WhiteheadRussell] p. 117Theorem *4.12con2bi 353
[WhiteheadRussell] p. 117Theorem *4.13notnotb 315
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 807
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 833
[WhiteheadRussell] p. 117Theorem *4.21bicom 222
[WhiteheadRussell] p. 117Theorem *4.22biantr 806  bitr 805
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 563
[WhiteheadRussell] p. 117Theorem *4.25oridm 905  pm4.25 906
[WhiteheadRussell] p. 118Theorem *4.3ancom 460
[WhiteheadRussell] p. 118Theorem *4.4andi 1010
[WhiteheadRussell] p. 118Theorem *4.31orcom 871
[WhiteheadRussell] p. 118Theorem *4.32anass 468
[WhiteheadRussell] p. 118Theorem *4.33orass 922
[WhiteheadRussell] p. 118Theorem *4.36anbi1 634
[WhiteheadRussell] p. 118Theorem *4.37orbi1 918
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 638
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 979
[WhiteheadRussell] p. 118Definition *4.34df-3an 1089
[WhiteheadRussell] p. 119Theorem *4.41ordi 1008
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1054
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1025
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 999
[WhiteheadRussell] p. 119Theorem *4.45orabs 1001  pm4.45 1000  pm4.45im 828
[WhiteheadRussell] p. 120Theorem *4.5anor 985
[WhiteheadRussell] p. 120Theorem *4.6imor 854
[WhiteheadRussell] p. 120Theorem *4.7anclb 545
[WhiteheadRussell] p. 120Theorem *4.51ianor 984
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 987
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 988
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 989
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 990
[WhiteheadRussell] p. 120Theorem *4.56ioran 986  pm4.56 991
[WhiteheadRussell] p. 120Theorem *4.57oran 992  pm4.57 993
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 404
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 857
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 397
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 850
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 405
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 851
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 398
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 557  pm4.71d 561  pm4.71i 559  pm4.71r 558  pm4.71rd 562  pm4.71ri 560
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 952
[WhiteheadRussell] p. 121Theorem *4.73iba 527
[WhiteheadRussell] p. 121Theorem *4.74biorf 937
[WhiteheadRussell] p. 121Theorem *4.76jcab 517  pm4.76 518
[WhiteheadRussell] p. 121Theorem *4.77jaob 964  pm4.77 965
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 935
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1006
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 392
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 393
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1026
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1027
[WhiteheadRussell] p. 122Theorem *4.84imbi1 347
[WhiteheadRussell] p. 122Theorem *4.85imbi2 348
[WhiteheadRussell] p. 122Theorem *4.86bibi1 351
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 387  impexp 450  pm4.87 844
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 824
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 947  pm5.11g 946
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 948
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 950
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 949
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1015
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1016
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1014
[WhiteheadRussell] p. 124Theorem *5.18nbbn 383  pm5.18 381
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 386
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 825
[WhiteheadRussell] p. 124Theorem *5.22xor 1017
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1050
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1051
[WhiteheadRussell] p. 124Theorem *5.25dfor2 902
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 572
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 388
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 361
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1004
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 956
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 831
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 573
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 836
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 826
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 834
[WhiteheadRussell] p. 125Theorem *5.41imdi 389  pm5.41 390
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 543
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 542
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1007
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1020
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 951
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1003
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1021
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1022
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1030
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 366
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 270
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1031
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44703
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44704
[WhiteheadRussell] p. 147Theorem *10.2219.26 1872
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44705
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44706
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44707
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1895
[WhiteheadRussell] p. 151Theorem *10.301albitr 44708
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44709
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44710
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44711
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44712
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44714
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44715
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44716
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44713
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2096
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44719
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44720
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2076
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2166
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1831
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1832
[WhiteheadRussell] p. 161Theorem *11.319.21vv 44721
[WhiteheadRussell] p. 162Theorem *11.322alim 44722
[WhiteheadRussell] p. 162Theorem *11.332albi 44723
[WhiteheadRussell] p. 162Theorem *11.342exim 44724
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44726
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44725
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1889
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44728
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44729
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44727
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1830
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44730
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44731
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1848
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44732
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2351
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1862
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44737
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44733
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44734
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44735
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44736
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44741
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44738
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44739
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44740
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44742
[WhiteheadRussell] p. 175Definition *14.02df-eu 2570
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44752  pm13.13b 44753
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44754
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3014
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3015
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3622
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44760
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44761
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44755
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44897  pm13.193 44756
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44757
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44758
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44759
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44766
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44765
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44764
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3805
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44767  pm14.122b 44768  pm14.122c 44769
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44770  pm14.123b 44771  pm14.123c 44772
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44774
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44773
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44775
[WhiteheadRussell] p. 190Theorem *14.22iota4 6481
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44776
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6482
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44777
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44779
[WhiteheadRussell] p. 192Theorem *14.26eupick 2634  eupickbi 2637  sbaniota 44780
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44778
[WhiteheadRussell] p. 192Theorem *14.271eubi 2585
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44781
[WhiteheadRussell] p. 235Definition *30.01conventions 30487  df-fv 6508
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9925  pm54.43lem 9924
[Young] p. 141Definition of operator orderingleop2 32211
[Young] p. 142Example 12.2(i)0leop 32217  idleop 32218
[vandenDries] p. 42Lemma 61irrapx1 43174
[vandenDries] p. 43Theorem 62pellex 43181  pellexlem1 43175

This page was last updated on 26-Mar-2026.
Copyright terms: Public domain