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 17623
[Adamek] p. 21Condition 3.1(b)df-cat 17623
[Adamek] p. 22Example 3.3(1)df-setc 18032
[Adamek] p. 24Example 3.3(4.c)0cat 17644  0funcg 49557  df-termc 49945
[Adamek] p. 24Example 3.3(4.d)df-prstc 50022  prsthinc 49936
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50050  df-mndtc 50050
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50046
[Adamek] p. 25Definition 3.5df-oppc 17667
[Adamek] p. 25Example 3.6(1)oduoppcciso 50038
[Adamek] p. 25Example 3.6(2)oppgoppcco 50063  oppgoppchom 50062  oppgoppcid 50064
[Adamek] p. 28Remark 3.9oppciso 17737
[Adamek] p. 28Remark 3.12invf1o 17725  invisoinvl 17746
[Adamek] p. 28Example 3.13idinv 17745  idiso 17744
[Adamek] p. 28Corollary 3.11inveq 17730
[Adamek] p. 28Definition 3.8df-inv 17704  df-iso 17705  dfiso2 17728
[Adamek] p. 28Proposition 3.10sectcan 17711
[Adamek] p. 29Remark 3.16cicer 17762  cicerALT 49518
[Adamek] p. 29Definition 3.15cic 17755  df-cic 17752
[Adamek] p. 29Definition 3.17df-func 17814
[Adamek] p. 29Proposition 3.14(1)invinv 17726
[Adamek] p. 29Proposition 3.14(2)invco 17727  isoco 17733
[Adamek] p. 30Remark 3.19df-func 17814
[Adamek] p. 30Example 3.20(1)idfucl 17837
[Adamek] p. 30Example 3.20(2)diag1 49776
[Adamek] p. 32Proposition 3.21funciso 17830
[Adamek] p. 33Example 3.26(1)discsnterm 50046  discthing 49933
[Adamek] p. 33Example 3.26(2)df-thinc 49890  prsthinc 49936  thincciso 49925  thincciso2 49927  thincciso3 49928  thinccisod 49926
[Adamek] p. 33Example 3.26(3)df-mndtc 50050
[Adamek] p. 33Proposition 3.23cofucl 17844  cofucla 49568
[Adamek] p. 34Remark 3.28(1)cofidfth 49634
[Adamek] p. 34Remark 3.28(2)catciso 18067  catcisoi 49872
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18122
[Adamek] p. 34Definition 3.27(2)df-fth 17863
[Adamek] p. 34Definition 3.27(3)df-full 17862
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18122
[Adamek] p. 35Corollary 3.32ffthiso 17887
[Adamek] p. 35Proposition 3.30(c)cofth 17893
[Adamek] p. 35Proposition 3.30(d)cofull 17892
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18107
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18107
[Adamek] p. 39Remark 3.422oppf 49604
[Adamek] p. 39Definition 3.41df-oppf 49595  funcoppc 17831
[Adamek] p. 39Definition 3.44.df-catc 18055  elcatchom 49869
[Adamek] p. 39Proposition 3.43(c)fthoppc 17881  fthoppf 49636
[Adamek] p. 39Proposition 3.43(d)fulloppc 17880  fulloppf 49635
[Adamek] p. 40Remark 3.48catccat 18064
[Adamek] p. 40Definition 3.470funcg 49557  df-catc 18055
[Adamek] p. 45Exercise 3Gincat 50073
[Adamek] p. 48Remark 4.2(2)cnelsubc 50076  nelsubc3 49543
[Adamek] p. 48Remark 4.2(3)imasubc 49623  imasubc2 49624  imasubc3 49628
[Adamek] p. 48Example 4.3(1.a)0subcat 17794
[Adamek] p. 48Example 4.3(1.b)catsubcat 17795
[Adamek] p. 48Definition 4.1(1)nelsubc3 49543
[Adamek] p. 48Definition 4.1(2)fullsubc 17806
[Adamek] p. 48Definition 4.1(a)df-subc 17768
[Adamek] p. 49Remark 4.4idsubc 49632
[Adamek] p. 49Remark 4.4(1)idemb 49631
[Adamek] p. 49Remark 4.4(2)idfullsubc 49633  ressffth 17896
[Adamek] p. 58Exercise 4Asetc1onsubc 50074
[Adamek] p. 83Definition 6.1df-nat 17902
[Adamek] p. 87Remark 6.14(a)fuccocl 17923
[Adamek] p. 87Remark 6.14(b)fucass 17927
[Adamek] p. 87Definition 6.15df-fuc 17903
[Adamek] p. 88Remark 6.16fuccat 17929
[Adamek] p. 101Definition 7.10funcg 49557  df-inito 17940
[Adamek] p. 101Example 7.2(3)0funcg 49557  df-termc 49945  initc 49563
[Adamek] p. 101Example 7.2 (6)irinitoringc 21467
[Adamek] p. 102Definition 7.4df-termo 17941  oppctermo 49708
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 17968
[Adamek] p. 102Proposition 7.3 (2)initoeu2 17972
[Adamek] p. 103Remark 7.8oppczeroo 49709
[Adamek] p. 103Definition 7.7df-zeroo 17942
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21468
[Adamek] p. 103Proposition 7.6termoeu1w 17975
[Adamek] p. 106Definition 7.19df-sect 17703
[Adamek] p. 107Example 7.20(7)thincinv 49941
[Adamek] p. 108Example 7.25(4)thincsect2 49940
[Adamek] p. 110Example 7.33(9)thincmon 49905
[Adamek] p. 110Proposition 7.35sectmon 17738
[Adamek] p. 112Proposition 7.42sectepi 17740
[Adamek] p. 185Section 10.67updjud 9847
[Adamek] p. 193Definition 11.1(1)df-lmd 50117
[Adamek] p. 193Definition 11.3(1)df-lmd 50117
[Adamek] p. 194Definition 11.3(2)df-lmd 50117
[Adamek] p. 202Definition 11.27(1)df-cmd 50118
[Adamek] p. 202Definition 11.27(2)df-cmd 50118
[Adamek] p. 478Item Rngdf-ringc 20612
[AhoHopUll] p. 2Section 1.1df-bigo 49021
[AhoHopUll] p. 12Section 1.3df-blen 49043
[AhoHopUll] p. 318Section 9.1df-concat 14522  df-pfx 14623  df-substr 14593  df-word 14465  lencl 14484  wrd0 14490
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24682  df-nmoo 30836
[AkhiezerGlazman] p. 64Theoremhmopidmch 32244  hmopidmchi 32242
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32292  pjcmul2i 32293
[AkhiezerGlazman] p. 72Theoremcnvunop 32009  unoplin 32011
[AkhiezerGlazman] p. 72Equation 2unopadj 32010  unopadj2 32029
[AkhiezerGlazman] p. 73Theoremelunop2 32104  lnopunii 32103
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32177
[Alling] p. 125Theorem 4.02(12)cofcutrtime 27938
[Alling] p. 184Axiom Bbdayfo 27660
[Alling] p. 184Axiom Oltsso 27659
[Alling] p. 184Axiom SDnodense 27675
[Alling] p. 185Lemma 0nocvxmin 27766
[Alling] p. 185Theoremconway 27790
[Alling] p. 185Axiom FEnoeta 27726
[Alling] p. 186Theorem 4lesrec 27810  lesrecd 27811
[Alling], p. 2Definitionrp-brsslt 43865
[Alling], p. 3Notenla0001 43868  nla0002 43866  nla0003 43867
[Apostol] p. 18Theorem I.1addcan 11319  addcan2d 11339  addcan2i 11329  addcand 11338  addcani 11328
[Apostol] p. 18Theorem I.2negeu 11372
[Apostol] p. 18Theorem I.3negsub 11431  negsubd 11500  negsubi 11461
[Apostol] p. 18Theorem I.4negneg 11433  negnegd 11485  negnegi 11453
[Apostol] p. 18Theorem I.5subdi 11572  subdid 11595  subdii 11588  subdir 11573  subdird 11596  subdiri 11589
[Apostol] p. 18Theorem I.6mul01 11314  mul01d 11334  mul01i 11325  mul02 11313  mul02d 11333  mul02i 11324
[Apostol] p. 18Theorem I.7mulcan 11776  mulcan2d 11773  mulcand 11772  mulcani 11778
[Apostol] p. 18Theorem I.8receu 11784  xreceu 33001
[Apostol] p. 18Theorem I.9divrec 11814  divrecd 11923  divreci 11889  divreczi 11882
[Apostol] p. 18Theorem I.10recrec 11841  recreci 11876
[Apostol] p. 18Theorem I.11mul0or 11779  mul0ord 11787  mul0ori 11786
[Apostol] p. 18Theorem I.12mul2neg 11578  mul2negd 11594  mul2negi 11587  mulneg1 11575  mulneg1d 11592  mulneg1i 11585
[Apostol] p. 18Theorem I.13divadddiv 11859  divadddivd 11964  divadddivi 11906
[Apostol] p. 18Theorem I.14divmuldiv 11844  divmuldivd 11961  divmuldivi 11904  rdivmuldivd 20382
[Apostol] p. 18Theorem I.15divdivdiv 11845  divdivdivd 11967  divdivdivi 11907
[Apostol] p. 20Axiom 7rpaddcl 12955  rpaddcld 12990  rpmulcl 12956  rpmulcld 12991
[Apostol] p. 20Axiom 8rpneg 12965
[Apostol] p. 20Axiom 90nrp 12968
[Apostol] p. 20Theorem I.17lttri 11261
[Apostol] p. 20Theorem I.18ltadd1d 11732  ltadd1dd 11750  ltadd1i 11693
[Apostol] p. 20Theorem I.19ltmul1 11994  ltmul1a 11993  ltmul1i 12063  ltmul1ii 12073  ltmul2 11995  ltmul2d 13017  ltmul2dd 13031  ltmul2i 12066
[Apostol] p. 20Theorem I.20msqgt0 11659  msqgt0d 11706  msqgt0i 11676
[Apostol] p. 20Theorem I.210lt1 11661
[Apostol] p. 20Theorem I.23lt0neg1 11645  lt0neg1d 11708  ltneg 11639  ltnegd 11717  ltnegi 11683
[Apostol] p. 20Theorem I.25lt2add 11624  lt2addd 11762  lt2addi 11701
[Apostol] p. 20Definition of positive numbersdf-rp 12932
[Apostol] p. 21Exercise 4recgt0 11990  recgt0d 12079  recgt0i 12050  recgt0ii 12051
[Apostol] p. 22Definition of integersdf-z 12514
[Apostol] p. 22Definition of positive integersdfnn3 12177
[Apostol] p. 22Definition of rationalsdf-q 12888
[Apostol] p. 24Theorem I.26supeu 9358
[Apostol] p. 26Theorem I.28nnunb 12422
[Apostol] p. 26Theorem I.29arch 12423  archd 45607
[Apostol] p. 28Exercise 2btwnz 12621
[Apostol] p. 28Exercise 3nnrecl 12424
[Apostol] p. 28Exercise 4rebtwnz 12886
[Apostol] p. 28Exercise 5zbtwnre 12885
[Apostol] p. 28Exercise 6qbtwnre 13140
[Apostol] p. 28Exercise 10(a)zeneo 16297  zneo 12601  zneoALTV 48142
[Apostol] p. 29Theorem I.35cxpsqrtth 26710  msqsqrtd 15394  resqrtth 15206  sqrtth 15316  sqrtthi 15322  sqsqrtd 15393
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12166
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12852
[Apostol] p. 361Remarkcrreczi 14179
[Apostol] p. 363Remarkabsgt0i 15351
[Apostol] p. 363Exampleabssubd 15407  abssubi 15355
[ApostolNT] p. 7Remarkfmtno0 48000  fmtno1 48001  fmtno2 48010  fmtno3 48011  fmtno4 48012  fmtno5fac 48042  fmtnofz04prm 48037
[ApostolNT] p. 7Definitiondf-fmtno 47988
[ApostolNT] p. 8Definitiondf-ppi 27081
[ApostolNT] p. 14Definitiondf-dvds 16211
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16227
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16252
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16247
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16240
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16242
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16228
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16229
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16234
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16269
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16271
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16273
[ApostolNT] p. 15Definitiondf-gcd 16453  dfgcd2 16504
[ApostolNT] p. 16Definitionisprm2 16640
[ApostolNT] p. 16Theorem 1.5coprmdvds 16611
[ApostolNT] p. 16Theorem 1.7prminf 16875
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16471
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16505
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16507
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16486
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16478
[ApostolNT] p. 17Theorem 1.8coprm 16670
[ApostolNT] p. 17Theorem 1.9euclemma 16672
[ApostolNT] p. 17Theorem 1.101arith2 16888
[ApostolNT] p. 18Theorem 1.13prmrec 16882
[ApostolNT] p. 19Theorem 1.14divalg 16361
[ApostolNT] p. 20Theorem 1.15eucalg 16545
[ApostolNT] p. 24Definitiondf-mu 27082
[ApostolNT] p. 25Definitiondf-phi 16725
[ApostolNT] p. 25Theorem 2.1musum 27172
[ApostolNT] p. 26Theorem 2.2phisum 16750
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16735
[ApostolNT] p. 28Theorem 2.5(c)phimul 16739
[ApostolNT] p. 32Definitiondf-vma 27079
[ApostolNT] p. 32Theorem 2.9muinv 27174
[ApostolNT] p. 32Theorem 2.10vmasum 27198
[ApostolNT] p. 38Remarkdf-sgm 27083
[ApostolNT] p. 38Definitiondf-sgm 27083
[ApostolNT] p. 75Definitiondf-chp 27080  df-cht 27078
[ApostolNT] p. 104Definitioncongr 16622
[ApostolNT] p. 106Remarkdvdsval3 16214
[ApostolNT] p. 106Definitionmoddvds 16221
[ApostolNT] p. 107Example 2mod2eq0even 16304
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16305
[ApostolNT] p. 107Example 4zmod1congr 13836
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13876
[ApostolNT] p. 107Theorem 5.2(c)modexp 14189
[ApostolNT] p. 108Theorem 5.3modmulconst 16246
[ApostolNT] p. 109Theorem 5.4cncongr1 16625
[ApostolNT] p. 109Theorem 5.6gcdmodi 17034
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16627
[ApostolNT] p. 113Theorem 5.17eulerth 16742
[ApostolNT] p. 113Theorem 5.18vfermltl 16761
[ApostolNT] p. 114Theorem 5.19fermltl 16743
[ApostolNT] p. 116Theorem 5.24wilthimp 27053
[ApostolNT] p. 179Definitiondf-lgs 27277  lgsprme0 27321
[ApostolNT] p. 180Example 11lgs 27322
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27298
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27313
[ApostolNT] p. 181Theorem 9.4m1lgs 27370
[ApostolNT] p. 181Theorem 9.52lgs 27389  2lgsoddprm 27398
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27356
[ApostolNT] p. 185Theorem 9.8lgsquad 27365
[ApostolNT] p. 188Definitiondf-lgs 27277  lgs1 27323
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27314
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27316
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27324
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27325
[Baer] p. 40Property (b)mapdord 42095
[Baer] p. 40Property (c)mapd11 42096
[Baer] p. 40Property (e)mapdin 42119  mapdlsm 42121
[Baer] p. 40Property (f)mapd0 42122
[Baer] p. 40Definition of projectivitydf-mapd 42082  mapd1o 42105
[Baer] p. 41Property (g)mapdat 42124
[Baer] p. 44Part (1)mapdpg 42163
[Baer] p. 45Part (2)hdmap1eq 42258  mapdheq 42185  mapdheq2 42186  mapdheq2biN 42187
[Baer] p. 45Part (3)baerlem3 42170
[Baer] p. 46Part (4)mapdheq4 42189  mapdheq4lem 42188
[Baer] p. 46Part (5)baerlem5a 42171  baerlem5abmN 42175  baerlem5amN 42173  baerlem5b 42172  baerlem5bmN 42174
[Baer] p. 47Part (6)hdmap1l6 42278  hdmap1l6a 42266  hdmap1l6e 42271  hdmap1l6f 42272  hdmap1l6g 42273  hdmap1l6lem1 42264  hdmap1l6lem2 42265  mapdh6N 42204  mapdh6aN 42192  mapdh6eN 42197  mapdh6fN 42198  mapdh6gN 42199  mapdh6lem1N 42190  mapdh6lem2N 42191
[Baer] p. 48Part 9hdmapval 42285
[Baer] p. 48Part 10hdmap10 42297
[Baer] p. 48Part 11hdmapadd 42300
[Baer] p. 48Part (6)hdmap1l6h 42274  mapdh6hN 42200
[Baer] p. 48Part (7)mapdh75cN 42210  mapdh75d 42211  mapdh75e 42209  mapdh75fN 42212  mapdh7cN 42206  mapdh7dN 42207  mapdh7eN 42205  mapdh7fN 42208
[Baer] p. 48Part (8)mapdh8 42245  mapdh8a 42232  mapdh8aa 42233  mapdh8ab 42234  mapdh8ac 42235  mapdh8ad 42236  mapdh8b 42237  mapdh8c 42238  mapdh8d 42240  mapdh8d0N 42239  mapdh8e 42241  mapdh8g 42242  mapdh8i 42243  mapdh8j 42244
[Baer] p. 48Part (9)mapdh9a 42246
[Baer] p. 48Equation 10mapdhvmap 42226
[Baer] p. 49Part 12hdmap11 42305  hdmapeq0 42301  hdmapf1oN 42322  hdmapneg 42303  hdmaprnN 42321  hdmaprnlem1N 42306  hdmaprnlem3N 42307  hdmaprnlem3uN 42308  hdmaprnlem4N 42310  hdmaprnlem6N 42311  hdmaprnlem7N 42312  hdmaprnlem8N 42313  hdmaprnlem9N 42314  hdmapsub 42304
[Baer] p. 49Part 14hdmap14lem1 42325  hdmap14lem10 42334  hdmap14lem1a 42323  hdmap14lem2N 42326  hdmap14lem2a 42324  hdmap14lem3 42327  hdmap14lem8 42332  hdmap14lem9 42333
[Baer] p. 50Part 14hdmap14lem11 42335  hdmap14lem12 42336  hdmap14lem13 42337  hdmap14lem14 42338  hdmap14lem15 42339  hgmapval 42344
[Baer] p. 50Part 15hgmapadd 42351  hgmapmul 42352  hgmaprnlem2N 42354  hgmapvs 42348
[Baer] p. 50Part 16hgmaprnN 42358
[Baer] p. 110Lemma 1hdmapip0com 42374
[Baer] p. 110Line 27hdmapinvlem1 42375
[Baer] p. 110Line 28hdmapinvlem2 42376
[Baer] p. 110Line 30hdmapinvlem3 42377
[Baer] p. 110Part 1.2hdmapglem5 42379  hgmapvv 42383
[Baer] p. 110Proposition 1hdmapinvlem4 42378
[Baer] p. 111Line 10hgmapvvlem1 42380
[Baer] p. 111Line 15hdmapg 42387  hdmapglem7 42386
[Bauer], p. 483Theorem 1.22irrexpq 26711  2irrexpqALT 26781
[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 5220
[BellMachover] p. 463Scheme Sepax-sep 5231
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37384  sepex 5235
[BellMachover] p. 466Problemaxpow2 5302
[BellMachover] p. 466Axiom Powaxpow3 5303
[BellMachover] p. 466Axiom Unionaxun2 7682
[BellMachover] p. 468Definitiondf-ord 6318
[BellMachover] p. 469Theorem 2.2(i)ordirr 6333
[BellMachover] p. 469Theorem 2.2(iii)onelon 6340
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6335
[BellMachover] p. 471Definition of Ndf-om 7809
[BellMachover] p. 471Problem 2.5(ii)uniordint 7746
[BellMachover] p. 471Definition of Limdf-lim 6320
[BellMachover] p. 472Axiom Infzfinf2 9552
[BellMachover] p. 473Theorem 2.8limom 7824
[BellMachover] p. 477Equation 3.1df-r1 9677
[BellMachover] p. 478Definitionrankval2 9731  rankval2b 35263
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9695  r1ord3g 9692
[BellMachover] p. 480Axiom Regzfreg 9502
[BellMachover] p. 488Axiom ACac5 10388  dfac4 10033
[BellMachover] p. 490Definition of alephalephval3 10021
[BeltramettiCassinelli] p. 98Remarkatlatmstc 39776
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32444
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32486  chirredi 32485
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32474
[Beran] p. 3Definition of joinsshjval3 31445
[Beran] p. 39Theorem 2.3(i)cmcm2 31707  cmcm2i 31684  cmcm2ii 31689  cmt2N 39707
[Beran] p. 40Theorem 2.3(iii)lecm 31708  lecmi 31693  lecmii 31694
[Beran] p. 45Theorem 3.4cmcmlem 31682
[Beran] p. 49Theorem 4.2cm2j 31711  cm2ji 31716  cm2mi 31717
[Beran] p. 95Definitiondf-sh 31298  issh2 31300
[Beran] p. 95Lemma 3.1(S5)his5 31177
[Beran] p. 95Lemma 3.1(S6)his6 31190
[Beran] p. 95Lemma 3.1(S7)his7 31181
[Beran] p. 95Lemma 3.2(S8)ho01i 31919
[Beran] p. 95Lemma 3.2(S9)hoeq1 31921
[Beran] p. 95Lemma 3.2(S10)ho02i 31920
[Beran] p. 95Lemma 3.2(S11)hoeq2 31922
[Beran] p. 95Postulate (S1)ax-his1 31173  his1i 31191
[Beran] p. 95Postulate (S2)ax-his2 31174
[Beran] p. 95Postulate (S3)ax-his3 31175
[Beran] p. 95Postulate (S4)ax-his4 31176
[Beran] p. 96Definition of normdf-hnorm 31059  dfhnorm2 31213  normval 31215
[Beran] p. 96Definition for Cauchy sequencehcau 31275
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31064
[Beran] p. 96Definition of complete subspaceisch3 31332
[Beran] p. 96Definition of convergedf-hlim 31063  hlimi 31279
[Beran] p. 97Theorem 3.3(i)norm-i-i 31224  norm-i 31220
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31228  norm-ii 31229  normlem0 31200  normlem1 31201  normlem2 31202  normlem3 31203  normlem4 31204  normlem5 31205  normlem6 31206  normlem7 31207  normlem7tALT 31210
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31230  norm-iii 31231
[Beran] p. 98Remark 3.4bcs 31272  bcsiALT 31270  bcsiHIL 31271
[Beran] p. 98Remark 3.4(B)normlem9at 31212  normpar 31246  normpari 31245
[Beran] p. 98Remark 3.4(C)normpyc 31237  normpyth 31236  normpythi 31233
[Beran] p. 99Remarklnfn0 32138  lnfn0i 32133  lnop0 32057  lnop0i 32061
[Beran] p. 99Theorem 3.5(i)nmcexi 32117  nmcfnex 32144  nmcfnexi 32142  nmcopex 32120  nmcopexi 32118
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32145  nmcfnlbi 32143  nmcoplb 32121  nmcoplbi 32119
[Beran] p. 99Theorem 3.5(iii)lnfncon 32147  lnfnconi 32146  lnopcon 32126  lnopconi 32125
[Beran] p. 100Lemma 3.6normpar2i 31247
[Beran] p. 101Lemma 3.6norm3adifi 31244  norm3adifii 31239  norm3dif 31241  norm3difi 31238
[Beran] p. 102Theorem 3.7(i)chocunii 31392  pjhth 31484  pjhtheu 31485  pjpjhth 31516  pjpjhthi 31517  pjth 25415
[Beran] p. 102Theorem 3.7(ii)ococ 31497  ococi 31496
[Beran] p. 103Remark 3.8nlelchi 32152
[Beran] p. 104Theorem 3.9riesz3i 32153  riesz4 32155  riesz4i 32154
[Beran] p. 104Theorem 3.10cnlnadj 32170  cnlnadjeu 32169  cnlnadjeui 32168  cnlnadji 32167  cnlnadjlem1 32158  nmopadjlei 32179
[Beran] p. 106Theorem 3.11(i)adjeq0 32182
[Beran] p. 106Theorem 3.11(v)nmopadji 32181
[Beran] p. 106Theorem 3.11(ii)adjmul 32183
[Beran] p. 106Theorem 3.11(iv)adjadj 32027
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32193  nmopcoadji 32192
[Beran] p. 106Theorem 3.11(iii)adjadd 32184
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32194
[Beran] p. 106Theorem 3.11(viii)adjcoi 32191  pjadj2coi 32295  pjadjcoi 32252
[Beran] p. 107Definitiondf-ch 31312  isch2 31314
[Beran] p. 107Remark 3.12choccl 31397  isch3 31332  occl 31395  ocsh 31374  shoccl 31396  shocsh 31375
[Beran] p. 107Remark 3.12(B)ococin 31499
[Beran] p. 108Theorem 3.13chintcl 31423
[Beran] p. 109Property (i)pjadj2 32278  pjadj3 32279  pjadji 31776  pjadjii 31765
[Beran] p. 109Property (ii)pjidmco 32272  pjidmcoi 32268  pjidmi 31764
[Beran] p. 110Definition of projector orderingpjordi 32264
[Beran] p. 111Remarkho0val 31841  pjch1 31761
[Beran] p. 111Definitiondf-hfmul 31825  df-hfsum 31824  df-hodif 31823  df-homul 31822  df-hosum 31821
[Beran] p. 111Lemma 4.4(i)pjo 31762
[Beran] p. 111Lemma 4.4(ii)pjch 31785  pjchi 31523
[Beran] p. 111Lemma 4.4(iii)pjoc2 31530  pjoc2i 31529
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31771
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32256  pjssmii 31772
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32255
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32254
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32259
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32257  pjssge0ii 31773
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32258  pjdifnormii 31774
[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 34457
[Bogachev] p. 17Lemma 1.5.4omssubadd 34465
[Bogachev] p. 17Example 1.5.2omsmon 34463
[Bogachev] p. 41Definition 1.11.2df-carsg 34467
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34487
[Bogachev] p. 116Definition 2.3.1df-itgm 34518  df-sitm 34496
[Bogachev] p. 118Chapter 2.4.4df-itgm 34518
[Bogachev] p. 118Definition 2.4.1df-sitg 34495
[Bollobas] p. 1Section I.1df-edg 29136  isuhgrop 29158  isusgrop 29250  isuspgrop 29249
[Bollobas] p. 2Section I.1df-isubgr 48334  df-subgr 29356  uhgrspan1 29391  uhgrspansubgr 29379
[Bollobas] p. 3Definitiondf-gric 48354  gricuspgr 48391  isuspgrim 48369
[Bollobas] p. 3Section I.1cusgrsize 29543  df-clnbgr 48292  df-cusgr 29500  df-nbgr 29421  fusgrmaxsize 29553
[Bollobas] p. 4Definitiondf-upwlks 48607  df-wlks 29688
[Bollobas] p. 4Section I.1finsumvtxdg2size 29639  finsumvtxdgeven 29641  fusgr1th 29640  fusgrvtxdgonume 29643  vtxdgoddnumeven 29642
[Bollobas] p. 5Notationdf-pths 29802
[Bollobas] p. 5Definitiondf-crcts 29874  df-cycls 29875  df-trls 29779  df-wlkson 29689
[Bollobas] p. 7Section I.1df-ushgr 29147
[BourbakiAlg1] p. 1Definition 1df-clintop 48673  df-cllaw 48659  df-mgm 18597  df-mgm2 48692
[BourbakiAlg1] p. 4Definition 5df-assintop 48674  df-asslaw 48661  df-sgrp 18676  df-sgrp2 48694
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48693  df-comlaw 48660
[BourbakiAlg1] p. 12Definition 2df-mnd 18692
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33106  mndlactf1o 33110  mndractf1 33108  mndractf1o 33111
[BourbakiAlg1] p. 92Definition 1df-ring 20205
[BourbakiAlg1] p. 93Section I.8.1df-rng 20123
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33798
[BourbakiAlg2] p. 113Chapter 5.assafld 33802  assarrginv 33801
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 33843  fldextrspunfld 33841  fldextrspunlem1 33840  fldextrspunlem2 33842  fldextrspunlsp 33839  fldextrspunlsplem 33838
[BourbakiCAlg2], p. 228Proposition 21arithidom 33617  dfufd2 33630
[BourbakiEns] p. Proposition 8fcof1 7233  fcofo 7234
[BourbakiTop1] p. Remarkxnegmnf 13151  xnegpnf 13150
[BourbakiTop1] p. Remark rexneg 13152
[BourbakiTop1] p. Remark 3ust0 24194  ustfilxp 24187
[BourbakiTop1] p. Axiom GT'tgpsubcn 24064
[BourbakiTop1] p. Criterionishmeo 23733
[BourbakiTop1] p. Example 1cstucnd 24257  iducn 24256  snfil 23838
[BourbakiTop1] p. Example 2neifil 23854
[BourbakiTop1] p. Theorem 1cnextcn 24041
[BourbakiTop1] p. Theorem 2ucnextcn 24277
[BourbakiTop1] p. Theorem 3df-hcmp 34122
[BourbakiTop1] p. Paragraph 3infil 23837
[BourbakiTop1] p. Definition 1df-ucn 24249  df-ust 24175  filintn0 23835  filn0 23836  istgp 24051  ucnprima 24255
[BourbakiTop1] p. Definition 2df-cfilu 24260
[BourbakiTop1] p. Definition 3df-cusp 24271  df-usp 24231  df-utop 24205  trust 24203
[BourbakiTop1] p. Definition 6df-pcmp 34021
[BourbakiTop1] p. Property V_issnei2 23090
[BourbakiTop1] p. Theorem 1(d)iscncl 23243
[BourbakiTop1] p. Condition F_Iustssel 24180
[BourbakiTop1] p. Condition U_Iustdiag 24183
[BourbakiTop1] p. Property V_iiinnei 23099
[BourbakiTop1] p. Property V_ivneiptopreu 23107  neissex 23101
[BourbakiTop1] p. Proposition 1neips 23087  neiss 23083  ucncn 24258  ustund 24196  ustuqtop 24220
[BourbakiTop1] p. Proposition 2cnpco 23241  neiptopreu 23107  utop2nei 24224  utop3cls 24225
[BourbakiTop1] p. Proposition 3fmucnd 24265  uspreg 24247  utopreg 24226
[BourbakiTop1] p. Proposition 4imasncld 23665  imasncls 23666  imasnopn 23664
[BourbakiTop1] p. Proposition 9cnpflf2 23974
[BourbakiTop1] p. Condition F_IIustincl 24182
[BourbakiTop1] p. Condition U_IIustinvel 24184
[BourbakiTop1] p. Property V_iiielnei 23085
[BourbakiTop1] p. Proposition 11cnextucn 24276
[BourbakiTop1] p. Condition F_IIbustbasel 24181
[BourbakiTop1] p. Condition U_IIIustexhalf 24185
[BourbakiTop1] p. Definition C'''df-cmp 23361
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23820
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 22868
[BourbakiTop2] p. 195Definition 1df-ldlf 34018
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46505
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46507  stoweid 46506
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46444  stoweidlem10 46453  stoweidlem14 46457  stoweidlem15 46458  stoweidlem35 46478  stoweidlem36 46479  stoweidlem37 46480  stoweidlem38 46481  stoweidlem40 46483  stoweidlem41 46484  stoweidlem43 46486  stoweidlem44 46487  stoweidlem46 46489  stoweidlem5 46448  stoweidlem50 46493  stoweidlem52 46495  stoweidlem53 46496  stoweidlem55 46498  stoweidlem56 46499
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46466  stoweidlem24 46467  stoweidlem27 46470  stoweidlem28 46471  stoweidlem30 46473
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46477  stoweidlem59 46502  stoweidlem60 46503
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46488  stoweidlem49 46492  stoweidlem7 46450
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46474  stoweidlem39 46482  stoweidlem42 46485  stoweidlem48 46491  stoweidlem51 46494  stoweidlem54 46497  stoweidlem57 46500  stoweidlem58 46501
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46468
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46460
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46454  stoweidlem13 46456  stoweidlem26 46469  stoweidlem61 46504
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46461
[Bruck] p. 1Section I.1df-clintop 48673  df-mgm 18597  df-mgm2 48692
[Bruck] p. 23Section II.1df-sgrp 18676  df-sgrp2 48694
[Bruck] p. 28Theorem 3.2dfgrp3 19004
[ChoquetDD] p. 2Definition of mappingdf-mpt 5168
[Church] p. 129Section II.24df-ifp 1064  dfifp2 1065
[Clemente] p. 10Definition ITnatded 30493
[Clemente] p. 10Definition I` `m,nnatded 30493
[Clemente] p. 11Definition E=>m,nnatded 30493
[Clemente] p. 11Definition I=>m,nnatded 30493
[Clemente] p. 11Definition E` `(1)natded 30493
[Clemente] p. 11Definition E` `(2)natded 30493
[Clemente] p. 12Definition E` `m,n,pnatded 30493
[Clemente] p. 12Definition I` `n(1)natded 30493
[Clemente] p. 12Definition I` `n(2)natded 30493
[Clemente] p. 13Definition I` `m,n,pnatded 30493
[Clemente] p. 14Proof 5.11natded 30493
[Clemente] p. 14Definition E` `nnatded 30493
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30495  ex-natded5.2 30494
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30498  ex-natded5.3 30497
[Clemente] p. 18Theorem 5.5ex-natded5.5 30500
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30502  ex-natded5.7 30501
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30504  ex-natded5.8 30503
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30506  ex-natded5.13 30505
[Clemente] p. 32Definition I` `nnatded 30493
[Clemente] p. 32Definition E` `m,n,p,anatded 30493
[Clemente] p. 32Definition E` `n,tnatded 30493
[Clemente] p. 32Definition I` `n,tnatded 30493
[Clemente] p. 43Theorem 9.20ex-natded9.20 30507
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30508
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30510  ex-natded9.26 30509
[Cohen] p. 301Remarkrelogoprlem 26571
[Cohen] p. 301Property 2relogmul 26572  relogmuld 26605
[Cohen] p. 301Property 3relogdiv 26573  relogdivd 26606
[Cohen] p. 301Property 4relogexp 26576
[Cohen] p. 301Property 1alog1 26565
[Cohen] p. 301Property 1bloge 26566
[Cohen4] p. 348Observationrelogbcxpb 26768
[Cohen4] p. 349Propertyrelogbf 26772
[Cohen4] p. 352Definitionelogb 26751
[Cohen4] p. 361Property 2relogbmul 26758
[Cohen4] p. 361Property 3logbrec 26763  relogbdiv 26760
[Cohen4] p. 361Property 4relogbreexp 26756
[Cohen4] p. 361Property 6relogbexp 26761
[Cohen4] p. 361Property 1(a)logbid1 26749
[Cohen4] p. 361Property 1(b)logb1 26750
[Cohen4] p. 367Propertylogbchbase 26752
[Cohen4] p. 377Property 2logblt 26765
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34450  sxbrsigalem4 34452
[Cohn] p. 81Section II.5acsdomd 18512  acsinfd 18511  acsinfdimd 18513  acsmap2d 18510  acsmapd 18509
[Cohn] p. 143Example 5.1.1sxbrsiga 34455
[Connell] p. 57Definitiondf-scmat 22465  df-scmatalt 48872
[Conway] p. 4Definitionlesrec 27810  lesrecd 27811
[Conway] p. 5Definitionaddsval 27973  addsval2 27974  df-adds 27971  df-muls 28118  df-negs 28032
[Conway] p. 7Theorem0lt1s 27823
[Conway] p. 12Theorem 12pw2cut2 28473
[Conway] p. 16Theorem 0(i)sltsright 27872
[Conway] p. 16Theorem 0(ii)sltsleft 27871
[Conway] p. 16Theorem 0(iii)lesid 27750
[Conway] p. 17Theorem 3addsass 28016  addsassd 28017  addscom 27977  addscomd 27978  addsrid 27975  addsridd 27976
[Conway] p. 17Definitiondf-0s 27818
[Conway] p. 17Theorem 4(ii)negnegs 28055
[Conway] p. 17Theorem 4(iii)negsid 28052  negsidd 28053
[Conway] p. 18Theorem 5leadds1 28000  leadds1d 28006
[Conway] p. 18Definitiondf-1s 27819
[Conway] p. 18Theorem 6(ii)negscl 28047  negscld 28048
[Conway] p. 18Theorem 6(iii)addscld 27991
[Conway] p. 19Notemulsunif2 28181
[Conway] p. 19Theorem 7addsdi 28166  addsdid 28167  addsdird 28168  mulnegs1d 28171  mulnegs2d 28172  mulsass 28177  mulsassd 28178  mulscom 28150  mulscomd 28151
[Conway] p. 19Theorem 8(i)mulscl 28145  mulscld 28146
[Conway] p. 19Theorem 8(iii)lemulsd 28149  ltmuls 28147  ltmulsd 28148
[Conway] p. 20Theorem 9mulsgt0 28155  mulsgt0d 28156
[Conway] p. 21Theorem 10(iv)precsex 28229
[Conway] p. 23Theorem 11eqcuts3 27815
[Conway] p. 24Definitiondf-reno 28501
[Conway] p. 24Theorem 13(ii)readdscl 28510  remulscl 28513  renegscl 28509
[Conway] p. 27Definitiondf-ons 28263  elons2 28269
[Conway] p. 27Theorem 14ltonsex 28273
[Conway] p. 28Theorem 15oncutlt 28275  onswe 28283
[Conway] p. 29Remarkmadebday 27911  newbday 27913  oldbday 27912
[Conway] p. 29Definitiondf-made 27838  df-new 27840  df-old 27839
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13809
[Crawley] p. 1Definition of posetdf-poset 18268
[Crawley] p. 107Theorem 13.2hlsupr 39843
[Crawley] p. 110Theorem 13.3arglem1N 40647  dalaw 40343
[Crawley] p. 111Theorem 13.4hlathil 42418
[Crawley] p. 111Definition of set Wdf-watsN 40447
[Crawley] p. 111Definition of dilationdf-dilN 40563  df-ldil 40561  isldil 40567
[Crawley] p. 111Definition of translationdf-ltrn 40562  df-trnN 40564  isltrn 40576  ltrnu 40578
[Crawley] p. 112Lemma Acdlema1N 40248  cdlema2N 40249  exatleN 39861
[Crawley] p. 112Lemma B1cvrat 39933  cdlemb 40251  cdlemb2 40498  cdlemb3 41063  idltrn 40607  l1cvat 39512  lhpat 40500  lhpat2 40502  lshpat 39513  ltrnel 40596  ltrnmw 40608
[Crawley] p. 112Lemma Ccdlemc1 40648  cdlemc2 40649  ltrnnidn 40631  trlat 40626  trljat1 40623  trljat2 40624  trljat3 40625  trlne 40642  trlnidat 40630  trlnle 40643
[Crawley] p. 112Definition of automorphismdf-pautN 40448
[Crawley] p. 113Lemma Ccdlemc 40654  cdlemc3 40650  cdlemc4 40651
[Crawley] p. 113Lemma Dcdlemd 40664  cdlemd1 40655  cdlemd2 40656  cdlemd3 40657  cdlemd4 40658  cdlemd5 40659  cdlemd6 40660  cdlemd7 40661  cdlemd8 40662  cdlemd9 40663  cdleme31sde 40842  cdleme31se 40839  cdleme31se2 40840  cdleme31snd 40843  cdleme32a 40898  cdleme32b 40899  cdleme32c 40900  cdleme32d 40901  cdleme32e 40902  cdleme32f 40903  cdleme32fva 40894  cdleme32fva1 40895  cdleme32fvcl 40897  cdleme32le 40904  cdleme48fv 40956  cdleme4gfv 40964  cdleme50eq 40998  cdleme50f 40999  cdleme50f1 41000  cdleme50f1o 41003  cdleme50laut 41004  cdleme50ldil 41005  cdleme50lebi 40997  cdleme50rn 41002  cdleme50rnlem 41001  cdlemeg49le 40968  cdlemeg49lebilem 40996
[Crawley] p. 113Lemma Ecdleme 41017  cdleme00a 40666  cdleme01N 40678  cdleme02N 40679  cdleme0a 40668  cdleme0aa 40667  cdleme0b 40669  cdleme0c 40670  cdleme0cp 40671  cdleme0cq 40672  cdleme0dN 40673  cdleme0e 40674  cdleme0ex1N 40680  cdleme0ex2N 40681  cdleme0fN 40675  cdleme0gN 40676  cdleme0moN 40682  cdleme1 40684  cdleme10 40711  cdleme10tN 40715  cdleme11 40727  cdleme11a 40717  cdleme11c 40718  cdleme11dN 40719  cdleme11e 40720  cdleme11fN 40721  cdleme11g 40722  cdleme11h 40723  cdleme11j 40724  cdleme11k 40725  cdleme11l 40726  cdleme12 40728  cdleme13 40729  cdleme14 40730  cdleme15 40735  cdleme15a 40731  cdleme15b 40732  cdleme15c 40733  cdleme15d 40734  cdleme16 40742  cdleme16aN 40716  cdleme16b 40736  cdleme16c 40737  cdleme16d 40738  cdleme16e 40739  cdleme16f 40740  cdleme16g 40741  cdleme19a 40760  cdleme19b 40761  cdleme19c 40762  cdleme19d 40763  cdleme19e 40764  cdleme19f 40765  cdleme1b 40683  cdleme2 40685  cdleme20aN 40766  cdleme20bN 40767  cdleme20c 40768  cdleme20d 40769  cdleme20e 40770  cdleme20f 40771  cdleme20g 40772  cdleme20h 40773  cdleme20i 40774  cdleme20j 40775  cdleme20k 40776  cdleme20l 40779  cdleme20l1 40777  cdleme20l2 40778  cdleme20m 40780  cdleme20y 40759  cdleme20zN 40758  cdleme21 40794  cdleme21d 40787  cdleme21e 40788  cdleme22a 40797  cdleme22aa 40796  cdleme22b 40798  cdleme22cN 40799  cdleme22d 40800  cdleme22e 40801  cdleme22eALTN 40802  cdleme22f 40803  cdleme22f2 40804  cdleme22g 40805  cdleme23a 40806  cdleme23b 40807  cdleme23c 40808  cdleme26e 40816  cdleme26eALTN 40818  cdleme26ee 40817  cdleme26f 40820  cdleme26f2 40822  cdleme26f2ALTN 40821  cdleme26fALTN 40819  cdleme27N 40826  cdleme27a 40824  cdleme27cl 40823  cdleme28c 40829  cdleme3 40694  cdleme30a 40835  cdleme31fv 40847  cdleme31fv1 40848  cdleme31fv1s 40849  cdleme31fv2 40850  cdleme31id 40851  cdleme31sc 40841  cdleme31sdnN 40844  cdleme31sn 40837  cdleme31sn1 40838  cdleme31sn1c 40845  cdleme31sn2 40846  cdleme31so 40836  cdleme35a 40905  cdleme35b 40907  cdleme35c 40908  cdleme35d 40909  cdleme35e 40910  cdleme35f 40911  cdleme35fnpq 40906  cdleme35g 40912  cdleme35h 40913  cdleme35h2 40914  cdleme35sn2aw 40915  cdleme35sn3a 40916  cdleme36a 40917  cdleme36m 40918  cdleme37m 40919  cdleme38m 40920  cdleme38n 40921  cdleme39a 40922  cdleme39n 40923  cdleme3b 40686  cdleme3c 40687  cdleme3d 40688  cdleme3e 40689  cdleme3fN 40690  cdleme3fa 40693  cdleme3g 40691  cdleme3h 40692  cdleme4 40695  cdleme40m 40924  cdleme40n 40925  cdleme40v 40926  cdleme40w 40927  cdleme41fva11 40934  cdleme41sn3aw 40931  cdleme41sn4aw 40932  cdleme41snaw 40933  cdleme42a 40928  cdleme42b 40935  cdleme42c 40929  cdleme42d 40930  cdleme42e 40936  cdleme42f 40937  cdleme42g 40938  cdleme42h 40939  cdleme42i 40940  cdleme42k 40941  cdleme42ke 40942  cdleme42keg 40943  cdleme42mN 40944  cdleme42mgN 40945  cdleme43aN 40946  cdleme43bN 40947  cdleme43cN 40948  cdleme43dN 40949  cdleme5 40697  cdleme50ex 41016  cdleme50ltrn 41014  cdleme51finvN 41013  cdleme51finvfvN 41012  cdleme51finvtrN 41015  cdleme6 40698  cdleme7 40706  cdleme7a 40700  cdleme7aa 40699  cdleme7b 40701  cdleme7c 40702  cdleme7d 40703  cdleme7e 40704  cdleme7ga 40705  cdleme8 40707  cdleme8tN 40712  cdleme9 40710  cdleme9a 40708  cdleme9b 40709  cdleme9tN 40714  cdleme9taN 40713  cdlemeda 40755  cdlemedb 40754  cdlemednpq 40756  cdlemednuN 40757  cdlemefr27cl 40860  cdlemefr32fva1 40867  cdlemefr32fvaN 40866  cdlemefrs32fva 40857  cdlemefrs32fva1 40858  cdlemefs27cl 40870  cdlemefs32fva1 40880  cdlemefs32fvaN 40879  cdlemesner 40753  cdlemeulpq 40677
[Crawley] p. 114Lemma E4atex 40533  4atexlem7 40532  cdleme0nex 40747  cdleme17a 40743  cdleme17c 40745  cdleme17d 40955  cdleme17d1 40746  cdleme17d2 40952  cdleme18a 40748  cdleme18b 40749  cdleme18c 40750  cdleme18d 40752  cdleme4a 40696
[Crawley] p. 115Lemma Ecdleme21a 40782  cdleme21at 40785  cdleme21b 40783  cdleme21c 40784  cdleme21ct 40786  cdleme21f 40789  cdleme21g 40790  cdleme21h 40791  cdleme21i 40792  cdleme22gb 40751
[Crawley] p. 116Lemma Fcdlemf 41020  cdlemf1 41018  cdlemf2 41019
[Crawley] p. 116Lemma Gcdlemftr1 41024  cdlemg16 41114  cdlemg28 41161  cdlemg28a 41150  cdlemg28b 41160  cdlemg3a 41054  cdlemg42 41186  cdlemg43 41187  cdlemg44 41190  cdlemg44a 41188  cdlemg46 41192  cdlemg47 41193  cdlemg9 41091  ltrnco 41176  ltrncom 41195  tgrpabl 41208  trlco 41184
[Crawley] p. 116Definition of Gdf-tgrp 41200
[Crawley] p. 117Lemma Gcdlemg17 41134  cdlemg17b 41119
[Crawley] p. 117Definition of Edf-edring-rN 41213  df-edring 41214
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41217
[Crawley] p. 118Remarktendopltp 41237
[Crawley] p. 118Lemma Hcdlemh 41274  cdlemh1 41272  cdlemh2 41273
[Crawley] p. 118Lemma Icdlemi 41277  cdlemi1 41275  cdlemi2 41276
[Crawley] p. 118Lemma Jcdlemj1 41278  cdlemj2 41279  cdlemj3 41280  tendocan 41281
[Crawley] p. 118Lemma Kcdlemk 41431  cdlemk1 41288  cdlemk10 41300  cdlemk11 41306  cdlemk11t 41403  cdlemk11ta 41386  cdlemk11tb 41388  cdlemk11tc 41402  cdlemk11u-2N 41346  cdlemk11u 41328  cdlemk12 41307  cdlemk12u-2N 41347  cdlemk12u 41329  cdlemk13-2N 41333  cdlemk13 41309  cdlemk14-2N 41335  cdlemk14 41311  cdlemk15-2N 41336  cdlemk15 41312  cdlemk16-2N 41337  cdlemk16 41314  cdlemk16a 41313  cdlemk17-2N 41338  cdlemk17 41315  cdlemk18-2N 41343  cdlemk18-3N 41357  cdlemk18 41325  cdlemk19-2N 41344  cdlemk19 41326  cdlemk19u 41427  cdlemk1u 41316  cdlemk2 41289  cdlemk20-2N 41349  cdlemk20 41331  cdlemk21-2N 41348  cdlemk21N 41330  cdlemk22-3 41358  cdlemk22 41350  cdlemk23-3 41359  cdlemk24-3 41360  cdlemk25-3 41361  cdlemk26-3 41363  cdlemk26b-3 41362  cdlemk27-3 41364  cdlemk28-3 41365  cdlemk29-3 41368  cdlemk3 41290  cdlemk30 41351  cdlemk31 41353  cdlemk32 41354  cdlemk33N 41366  cdlemk34 41367  cdlemk35 41369  cdlemk36 41370  cdlemk37 41371  cdlemk38 41372  cdlemk39 41373  cdlemk39u 41425  cdlemk4 41291  cdlemk41 41377  cdlemk42 41398  cdlemk42yN 41401  cdlemk43N 41420  cdlemk45 41404  cdlemk46 41405  cdlemk47 41406  cdlemk48 41407  cdlemk49 41408  cdlemk5 41293  cdlemk50 41409  cdlemk51 41410  cdlemk52 41411  cdlemk53 41414  cdlemk54 41415  cdlemk55 41418  cdlemk55u 41423  cdlemk56 41428  cdlemk5a 41292  cdlemk5auN 41317  cdlemk5u 41318  cdlemk6 41294  cdlemk6u 41319  cdlemk7 41305  cdlemk7u-2N 41345  cdlemk7u 41327  cdlemk8 41295  cdlemk9 41296  cdlemk9bN 41297  cdlemki 41298  cdlemkid 41393  cdlemkj-2N 41339  cdlemkj 41320  cdlemksat 41303  cdlemksel 41302  cdlemksv 41301  cdlemksv2 41304  cdlemkuat 41323  cdlemkuel-2N 41341  cdlemkuel-3 41355  cdlemkuel 41322  cdlemkuv-2N 41340  cdlemkuv2-2 41342  cdlemkuv2-3N 41356  cdlemkuv2 41324  cdlemkuvN 41321  cdlemkvcl 41299  cdlemky 41383  cdlemkyyN 41419  tendoex 41432
[Crawley] p. 120Remarkdva1dim 41442
[Crawley] p. 120Lemma Lcdleml1N 41433  cdleml2N 41434  cdleml3N 41435  cdleml4N 41436  cdleml5N 41437  cdleml6 41438  cdleml7 41439  cdleml8 41440  cdleml9 41441  dia1dim 41518
[Crawley] p. 120Lemma Mdia11N 41505  diaf11N 41506  dialss 41503  diaord 41504  dibf11N 41618  djajN 41594
[Crawley] p. 120Definition of isomorphism mapdiaval 41489
[Crawley] p. 121Lemma Mcdlemm10N 41575  dia2dimlem1 41521  dia2dimlem2 41522  dia2dimlem3 41523  dia2dimlem4 41524  dia2dimlem5 41525  diaf1oN 41587  diarnN 41586  dvheveccl 41569  dvhopN 41573
[Crawley] p. 121Lemma Ncdlemn 41669  cdlemn10 41663  cdlemn11 41668  cdlemn11a 41664  cdlemn11b 41665  cdlemn11c 41666  cdlemn11pre 41667  cdlemn2 41652  cdlemn2a 41653  cdlemn3 41654  cdlemn4 41655  cdlemn4a 41656  cdlemn5 41658  cdlemn5pre 41657  cdlemn6 41659  cdlemn7 41660  cdlemn8 41661  cdlemn9 41662  diclspsn 41651
[Crawley] p. 121Definition of phi(q)df-dic 41630
[Crawley] p. 122Lemma Ndih11 41722  dihf11 41724  dihjust 41674  dihjustlem 41673  dihord 41721  dihord1 41675  dihord10 41680  dihord11b 41679  dihord11c 41681  dihord2 41684  dihord2a 41676  dihord2b 41677  dihord2cN 41678  dihord2pre 41682  dihord2pre2 41683  dihordlem6 41670  dihordlem7 41671  dihordlem7b 41672
[Crawley] p. 122Definition of isomorphism mapdihffval 41687  dihfval 41688  dihval 41689
[Diestel] p. 3Definitiondf-gric 48354  df-grim 48351  isuspgrim 48369
[Diestel] p. 3Section 1.1df-cusgr 29500  df-nbgr 29421
[Diestel] p. 3Definition by df-grisom 48350
[Diestel] p. 4Section 1.1df-isubgr 48334  df-subgr 29356  uhgrspan1 29391  uhgrspansubgr 29379
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29643  vtxdgoddnumeven 29642
[Diestel] p. 27Section 1.10df-ushgr 29147
[EGA] p. 80Notation 1.1.1rspecval 34029
[EGA] p. 80Proposition 1.1.2zartop 34041
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34033  zarcls1 34034
[EGA] p. 81Corollary 1.1.8zart0 34044
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34047
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34050
[Eisenberg] p. 67Definition 5.3df-dif 3893
[Eisenberg] p. 82Definition 6.3dfom3 9557
[Eisenberg] p. 125Definition 8.21df-map 8766
[Eisenberg] p. 216Example 13.2(4)omenps 9565
[Eisenberg] p. 310Theorem 19.8cardprc 9893
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10466
[Enderton] p. 18Axiom of Empty Setaxnul 5240
[Enderton] p. 19Definitiondf-tp 4573
[Enderton] p. 26Exercise 5unissb 4884
[Enderton] p. 26Exercise 10pwel 5316
[Enderton] p. 28Exercise 7(b)pwun 5515
[Enderton] p. 30Theorem "Distributive laws"iinin1 5022  iinin2 5021  iinun2 5016  iunin1 5015  iunin1f 32647  iunin2 5014  uniin1 32641  uniin2 32642
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5020  iundif2 5017
[Enderton] p. 32Exercise 20unineq 4229
[Enderton] p. 33Exercise 23iinuni 5041
[Enderton] p. 33Exercise 25iununi 5042
[Enderton] p. 33Exercise 24(a)iinpw 5049
[Enderton] p. 33Exercise 24(b)iunpw 7716  iunpwss 5050
[Enderton] p. 36Definitionopthwiener 5460
[Enderton] p. 38Exercise 6(a)unipw 5395
[Enderton] p. 38Exercise 6(b)pwuni 4889
[Enderton] p. 41Lemma 3Dopeluu 5416  rnex 7852  rnexg 7844
[Enderton] p. 41Exercise 8dmuni 5861  rnuni 6104
[Enderton] p. 42Definition of a functiondffun7 6517  dffun8 6518
[Enderton] p. 43Definition of function valuefunfv2 6920
[Enderton] p. 43Definition of single-rootedfuncnv 6559
[Enderton] p. 44Definition (d)dfima2 6019  dfima3 6020
[Enderton] p. 47Theorem 3Hfvco2 6929
[Enderton] p. 49Axiom of Choice (first form)ac7 10384  ac7g 10385  df-ac 10027  dfac2 10043  dfac2a 10041  dfac2b 10042  dfac3 10032  dfac7 10044
[Enderton] p. 50Theorem 3K(a)imauni 7192
[Enderton] p. 52Definitiondf-map 8766
[Enderton] p. 53Exercise 21coass 6222
[Enderton] p. 53Exercise 27dmco 6211
[Enderton] p. 53Exercise 14(a)funin 6566
[Enderton] p. 53Exercise 22(a)imass2 6059
[Enderton] p. 54Remarkixpf 8859  ixpssmap 8871
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8837
[Enderton] p. 55Axiom of Choice (second form)ac9 10394  ac9s 10404
[Enderton] p. 56Theorem 3Meqvrelref 39026  erref 8655
[Enderton] p. 57Lemma 3Neqvrelthi 39029  erthi 8691
[Enderton] p. 57Definitiondf-ec 8636
[Enderton] p. 58Definitiondf-qs 8640
[Enderton] p. 61Exercise 35df-ec 8636
[Enderton] p. 65Exercise 56(a)dmun 5857
[Enderton] p. 68Definition of successordf-suc 6321
[Enderton] p. 71Definitiondf-tr 5194  dftr4 5199
[Enderton] p. 72Theorem 4Eunisuc 6396  unisucg 6395
[Enderton] p. 73Exercise 6unisuc 6396  unisucg 6395
[Enderton] p. 73Exercise 5(a)truni 5208
[Enderton] p. 73Exercise 5(b)trint 5210  trintALT 45322
[Enderton] p. 79Theorem 4I(A1)nna0 8531
[Enderton] p. 79Theorem 4I(A2)nnasuc 8533  onasuc 8454
[Enderton] p. 79Definition of operation valuedf-ov 7361
[Enderton] p. 80Theorem 4J(A1)nnm0 8532
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8534  onmsuc 8455
[Enderton] p. 81Theorem 4K(1)nnaass 8549
[Enderton] p. 81Theorem 4K(2)nna0r 8536  nnacom 8544
[Enderton] p. 81Theorem 4K(3)nndi 8550
[Enderton] p. 81Theorem 4K(4)nnmass 8551
[Enderton] p. 81Theorem 4K(5)nnmcom 8553
[Enderton] p. 82Exercise 16nnm0r 8537  nnmsucr 8552
[Enderton] p. 88Exercise 23nnaordex 8565
[Enderton] p. 129Definitiondf-en 8885
[Enderton] p. 132Theorem 6B(b)canth 7312
[Enderton] p. 133Exercise 1xpomen 9926
[Enderton] p. 133Exercise 2qnnen 16169
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9132
[Enderton] p. 135Corollary 6Cphp3 9134
[Enderton] p. 136Corollary 6Enneneq 9131
[Enderton] p. 136Corollary 6D(a)pssinf 9163
[Enderton] p. 136Corollary 6D(b)ominf 9165
[Enderton] p. 137Lemma 6Fpssnn 9094
[Enderton] p. 138Corollary 6Gssfi 9098
[Enderton] p. 139Theorem 6H(c)mapen 9070
[Enderton] p. 142Theorem 6I(3)xpdjuen 10091
[Enderton] p. 142Theorem 6I(4)mapdjuen 10092
[Enderton] p. 143Theorem 6Jdju0en 10087  dju1en 10083
[Enderton] p. 144Exercise 13iunfi 9244  unifi 9245  unifi2 9246
[Enderton] p. 144Corollary 6Kundif2 4418  unfi 9096  unfi2 9211
[Enderton] p. 145Figure 38ffoss 7890
[Enderton] p. 145Definitiondf-dom 8886
[Enderton] p. 146Example 1domen 8899  domeng 8900
[Enderton] p. 146Example 3nndomo 9143  nnsdom 9564  nnsdomg 9200
[Enderton] p. 149Theorem 6L(a)djudom2 10095
[Enderton] p. 149Theorem 6L(c)mapdom1 9071  xpdom1 9005  xpdom1g 9003  xpdom2g 9002
[Enderton] p. 149Theorem 6L(d)mapdom2 9077
[Enderton] p. 151Theorem 6Mzorn 10418  zorng 10415
[Enderton] p. 151Theorem 6M(4)ac8 10403  dfac5 10040
[Enderton] p. 159Theorem 6Qunictb 10487
[Enderton] p. 164Exampleinfdif 10119
[Enderton] p. 168Definitiondf-po 5530
[Enderton] p. 192Theorem 7M(a)oneli 6430
[Enderton] p. 192Theorem 7M(b)ontr1 6362
[Enderton] p. 192Theorem 7M(c)onirri 6429
[Enderton] p. 193Corollary 7N(b)0elon 6370
[Enderton] p. 193Corollary 7N(c)onsuci 7781
[Enderton] p. 193Corollary 7N(d)ssonunii 7726
[Enderton] p. 194Remarkonprc 7723
[Enderton] p. 194Exercise 16suc11 6424
[Enderton] p. 197Definitiondf-card 9852
[Enderton] p. 197Theorem 7Pcarden 10462
[Enderton] p. 200Exercise 25tfis 7797
[Enderton] p. 202Lemma 7Tr1tr 9689
[Enderton] p. 202Definitiondf-r1 9677
[Enderton] p. 202Theorem 7Qr1val1 9699
[Enderton] p. 204Theorem 7V(b)rankval4 9780  rankval4b 35264
[Enderton] p. 206Theorem 7X(b)en2lp 9516
[Enderton] p. 207Exercise 30rankpr 9770  rankprb 9764  rankpw 9756  rankpwi 9736  rankuniss 9779
[Enderton] p. 207Exercise 34opthreg 9528
[Enderton] p. 208Exercise 35suc11reg 9529
[Enderton] p. 212Definition of alephalephval3 10021
[Enderton] p. 213Theorem 8A(a)alephord2 9987
[Enderton] p. 213Theorem 8A(b)cardalephex 10001
[Enderton] p. 218Theorem Schema 8Eonfununi 8272
[Enderton] p. 222Definition of kardkarden 9808  kardex 9807
[Enderton] p. 238Theorem 8Roeoa 8524
[Enderton] p. 238Theorem 8Soeoe 8526
[Enderton] p. 240Exercise 25oarec 8488
[Enderton] p. 257Definition of cofinalitycflm 10161
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17597
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17539
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18508  mrieqv2d 17594  mrieqvd 17593
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17598
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17603  mreexexlem2d 17600
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18514  mreexfidimd 17605
[Frege1879] p. 11Statementdf3or2 44210
[Frege1879] p. 12Statementdf3an2 44211  dfxor4 44208  dfxor5 44209
[Frege1879] p. 26Axiom 1ax-frege1 44232
[Frege1879] p. 26Axiom 2ax-frege2 44233
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44237
[Frege1879] p. 31Proposition 4frege4 44241
[Frege1879] p. 32Proposition 5frege5 44242
[Frege1879] p. 33Proposition 6frege6 44248
[Frege1879] p. 34Proposition 7frege7 44250
[Frege1879] p. 35Axiom 8ax-frege8 44251  axfrege8 44249
[Frege1879] p. 35Proposition 8pm2.04 90  wl-luk-pm2.04 37772
[Frege1879] p. 35Proposition 9frege9 44254
[Frege1879] p. 36Proposition 10frege10 44262
[Frege1879] p. 36Proposition 11frege11 44256
[Frege1879] p. 37Proposition 12frege12 44255
[Frege1879] p. 37Proposition 13frege13 44264
[Frege1879] p. 37Proposition 14frege14 44265
[Frege1879] p. 38Proposition 15frege15 44268
[Frege1879] p. 38Proposition 16frege16 44258
[Frege1879] p. 39Proposition 17frege17 44263
[Frege1879] p. 39Proposition 18frege18 44260
[Frege1879] p. 39Proposition 19frege19 44266
[Frege1879] p. 40Proposition 20frege20 44270
[Frege1879] p. 40Proposition 21frege21 44269
[Frege1879] p. 41Proposition 22frege22 44261
[Frege1879] p. 42Proposition 23frege23 44267
[Frege1879] p. 42Proposition 24frege24 44257
[Frege1879] p. 42Proposition 25frege25 44259  rp-frege25 44247
[Frege1879] p. 42Proposition 26frege26 44252
[Frege1879] p. 43Axiom 28ax-frege28 44272
[Frege1879] p. 43Proposition 27frege27 44253
[Frege1879] p. 43Proposition 28con3 153
[Frege1879] p. 43Proposition 29frege29 44273
[Frege1879] p. 44Axiom 31ax-frege31 44276  axfrege31 44275
[Frege1879] p. 44Proposition 30frege30 44274
[Frege1879] p. 44Proposition 31notnotr 130
[Frege1879] p. 44Proposition 32frege32 44277
[Frege1879] p. 44Proposition 33frege33 44278
[Frege1879] p. 45Proposition 34frege34 44279
[Frege1879] p. 45Proposition 35frege35 44280
[Frege1879] p. 45Proposition 36frege36 44281
[Frege1879] p. 46Proposition 37frege37 44282
[Frege1879] p. 46Proposition 38frege38 44283
[Frege1879] p. 46Proposition 39frege39 44284
[Frege1879] p. 46Proposition 40frege40 44285
[Frege1879] p. 47Axiom 41ax-frege41 44287  axfrege41 44286
[Frege1879] p. 47Proposition 41notnot 142
[Frege1879] p. 47Proposition 42frege42 44288
[Frege1879] p. 47Proposition 43frege43 44289
[Frege1879] p. 47Proposition 44frege44 44290
[Frege1879] p. 47Proposition 45frege45 44291
[Frege1879] p. 48Proposition 46frege46 44292
[Frege1879] p. 48Proposition 47frege47 44293
[Frege1879] p. 49Proposition 48frege48 44294
[Frege1879] p. 49Proposition 49frege49 44295
[Frege1879] p. 49Proposition 50frege50 44296
[Frege1879] p. 50Axiom 52ax-frege52a 44299  ax-frege52c 44330  frege52aid 44300  frege52b 44331
[Frege1879] p. 50Axiom 54ax-frege54a 44304  ax-frege54c 44334  frege54b 44335
[Frege1879] p. 50Proposition 51frege51 44297
[Frege1879] p. 50Proposition 52dfsbcq 3731
[Frege1879] p. 50Proposition 53frege53a 44302  frege53aid 44301  frege53b 44332  frege53c 44356
[Frege1879] p. 50Proposition 54biid 261  eqid 2737
[Frege1879] p. 50Proposition 55frege55a 44310  frege55aid 44307  frege55b 44339  frege55c 44360  frege55cor1a 44311  frege55lem2a 44309  frege55lem2b 44338  frege55lem2c 44359
[Frege1879] p. 50Proposition 56frege56a 44313  frege56aid 44312  frege56b 44340  frege56c 44361
[Frege1879] p. 51Axiom 58ax-frege58a 44317  ax-frege58b 44343  frege58bid 44344  frege58c 44363
[Frege1879] p. 51Proposition 57frege57a 44315  frege57aid 44314  frege57b 44341  frege57c 44362
[Frege1879] p. 51Proposition 58spsbc 3742
[Frege1879] p. 51Proposition 59frege59a 44319  frege59b 44346  frege59c 44364
[Frege1879] p. 52Proposition 60frege60a 44320  frege60b 44347  frege60c 44365
[Frege1879] p. 52Proposition 61frege61a 44321  frege61b 44348  frege61c 44366
[Frege1879] p. 52Proposition 62frege62a 44322  frege62b 44349  frege62c 44367
[Frege1879] p. 52Proposition 63frege63a 44323  frege63b 44350  frege63c 44368
[Frege1879] p. 53Proposition 64frege64a 44324  frege64b 44351  frege64c 44369
[Frege1879] p. 53Proposition 65frege65a 44325  frege65b 44352  frege65c 44370
[Frege1879] p. 54Proposition 66frege66a 44326  frege66b 44353  frege66c 44371
[Frege1879] p. 54Proposition 67frege67a 44327  frege67b 44354  frege67c 44372
[Frege1879] p. 54Proposition 68frege68a 44328  frege68b 44355  frege68c 44373
[Frege1879] p. 55Definition 69dffrege69 44374
[Frege1879] p. 58Proposition 70frege70 44375
[Frege1879] p. 59Proposition 71frege71 44376
[Frege1879] p. 59Proposition 72frege72 44377
[Frege1879] p. 59Proposition 73frege73 44378
[Frege1879] p. 60Definition 76dffrege76 44381
[Frege1879] p. 60Proposition 74frege74 44379
[Frege1879] p. 60Proposition 75frege75 44380
[Frege1879] p. 62Proposition 77frege77 44382  frege77d 44188
[Frege1879] p. 63Proposition 78frege78 44383
[Frege1879] p. 63Proposition 79frege79 44384
[Frege1879] p. 63Proposition 80frege80 44385
[Frege1879] p. 63Proposition 81frege81 44386  frege81d 44189
[Frege1879] p. 64Proposition 82frege82 44387
[Frege1879] p. 65Proposition 83frege83 44388  frege83d 44190
[Frege1879] p. 65Proposition 84frege84 44389
[Frege1879] p. 66Proposition 85frege85 44390
[Frege1879] p. 66Proposition 86frege86 44391
[Frege1879] p. 66Proposition 87frege87 44392  frege87d 44192
[Frege1879] p. 67Proposition 88frege88 44393
[Frege1879] p. 68Proposition 89frege89 44394
[Frege1879] p. 68Proposition 90frege90 44395
[Frege1879] p. 68Proposition 91frege91 44396  frege91d 44193
[Frege1879] p. 69Proposition 92frege92 44397
[Frege1879] p. 70Proposition 93frege93 44398
[Frege1879] p. 70Proposition 94frege94 44399
[Frege1879] p. 70Proposition 95frege95 44400
[Frege1879] p. 71Definition 99dffrege99 44404
[Frege1879] p. 71Proposition 96frege96 44401  frege96d 44191
[Frege1879] p. 71Proposition 97frege97 44402  frege97d 44194
[Frege1879] p. 71Proposition 98frege98 44403  frege98d 44195
[Frege1879] p. 72Proposition 100frege100 44405
[Frege1879] p. 72Proposition 101frege101 44406
[Frege1879] p. 72Proposition 102frege102 44407  frege102d 44196
[Frege1879] p. 73Proposition 103frege103 44408
[Frege1879] p. 73Proposition 104frege104 44409
[Frege1879] p. 73Proposition 105frege105 44410
[Frege1879] p. 73Proposition 106frege106 44411  frege106d 44197
[Frege1879] p. 74Proposition 107frege107 44412
[Frege1879] p. 74Proposition 108frege108 44413  frege108d 44198
[Frege1879] p. 74Proposition 109frege109 44414  frege109d 44199
[Frege1879] p. 75Proposition 110frege110 44415
[Frege1879] p. 75Proposition 111frege111 44416  frege111d 44201
[Frege1879] p. 76Proposition 112frege112 44417
[Frege1879] p. 76Proposition 113frege113 44418
[Frege1879] p. 76Proposition 114frege114 44419  frege114d 44200
[Frege1879] p. 77Definition 115dffrege115 44420
[Frege1879] p. 77Proposition 116frege116 44421
[Frege1879] p. 78Proposition 117frege117 44422
[Frege1879] p. 78Proposition 118frege118 44423
[Frege1879] p. 78Proposition 119frege119 44424
[Frege1879] p. 78Proposition 120frege120 44425
[Frege1879] p. 79Proposition 121frege121 44426
[Frege1879] p. 79Proposition 122frege122 44427  frege122d 44202
[Frege1879] p. 79Proposition 123frege123 44428
[Frege1879] p. 80Proposition 124frege124 44429  frege124d 44203
[Frege1879] p. 81Proposition 125frege125 44430
[Frege1879] p. 81Proposition 126frege126 44431  frege126d 44204
[Frege1879] p. 82Proposition 127frege127 44432
[Frege1879] p. 83Proposition 128frege128 44433
[Frege1879] p. 83Proposition 129frege129 44434  frege129d 44205
[Frege1879] p. 84Proposition 130frege130 44435
[Frege1879] p. 85Proposition 131frege131 44436  frege131d 44206
[Frege1879] p. 86Proposition 132frege132 44437
[Frege1879] p. 86Proposition 133frege133 44438  frege133d 44207
[Fremlin1] p. 13Definition 111G (b)df-salgen 46756
[Fremlin1] p. 13Definition 111G (d)borelmbl 47079
[Fremlin1] p. 13Proposition 111G (b)salgenss 46779
[Fremlin1] p. 14Definition 112Aismea 46894
[Fremlin1] p. 15Remark 112B (d)psmeasure 46914
[Fremlin1] p. 15Property 112C (a)meadjun 46905  meadjunre 46919
[Fremlin1] p. 15Property 112C (b)meassle 46906
[Fremlin1] p. 15Property 112C (c)meaunle 46907
[Fremlin1] p. 16Property 112C (d)iundjiun 46903  meaiunle 46912  meaiunlelem 46911
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 46924  meaiuninc2 46925  meaiuninc3 46928  meaiuninc3v 46927  meaiunincf 46926  meaiuninclem 46923
[Fremlin1] p. 16Proposition 112C (f)meaiininc 46930  meaiininc2 46931  meaiininclem 46929
[Fremlin1] p. 19Theorem 113Ccaragen0 46949  caragendifcl 46957  caratheodory 46971  omelesplit 46961
[Fremlin1] p. 19Definition 113Aisome 46937  isomennd 46974  isomenndlem 46973
[Fremlin1] p. 19Remark 113B (c)omeunle 46959
[Fremlin1] p. 19Definition 112Dfcaragencmpl 46978  voncmpl 47064
[Fremlin1] p. 19Definition 113A (ii)omessle 46941
[Fremlin1] p. 20Theorem 113Ccarageniuncl 46966  carageniuncllem1 46964  carageniuncllem2 46965  caragenuncl 46956  caragenuncllem 46955  caragenunicl 46967
[Fremlin1] p. 21Remark 113Dcaragenel2d 46975
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 46969  caratheodorylem2 46970
[Fremlin1] p. 21Exercise 113Xacaragencmpl 46978
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47037  hoidmv1lelem1 47034  hoidmv1lelem2 47035  hoidmv1lelem3 47036
[Fremlin1] p. 25Definition 114Eisvonmbl 47081
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47037  hoidmvle 47043  hoidmvlelem1 47038  hoidmvlelem2 47039  hoidmvlelem3 47040  hoidmvlelem4 47041  hoidmvlelem5 47042  hsphoidmvle2 47028  hsphoif 47019  hsphoival 47022
[Fremlin1] p. 29Definition 1135 (b)hoicvr 46991
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 46999
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47026  hoidmvn0val 47027  hoidmvval 47020  hoidmvval0 47030  hoidmvval0b 47033
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47031  hsphoidmvle 47029
[Fremlin1] p. 30Definition 115Cdf-ovoln 46980  df-voln 46982
[Fremlin1] p. 30Proposition 115D (a)dmovn 47047  ovn0 47009  ovn0lem 47008  ovnf 47006  ovnome 47016  ovnssle 47004  ovnsslelem 47003  ovnsupge0 47000
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47046  ovnhoilem1 47044  ovnhoilem2 47045  vonhoi 47110
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47063  hoidifhspf 47061  hoidifhspval 47051  hoidifhspval2 47058  hoidifhspval3 47062  hspmbl 47072  hspmbllem1 47069  hspmbllem2 47070  hspmbllem3 47071
[Fremlin1] p. 31Definition 115Evoncmpl 47064  vonmea 47017
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47015  ovnsubadd2 47089  ovnsubadd2lem 47088  ovnsubaddlem1 47013  ovnsubaddlem2 47014
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47074  hoimbl2 47108  hoimbllem 47073  hspdifhsp 47059  opnvonmbl 47077  opnvonmbllem2 47076
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47079
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47122  iccvonmbllem 47121  ioovonmbl 47120
[Fremlin1] p. 32Proposition 115G (d)vonicc 47128  vonicclem2 47127  vonioo 47125  vonioolem2 47124  vonn0icc 47131  vonn0icc2 47135  vonn0ioo 47130  vonn0ioo2 47133
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47132  snvonmbl 47129  vonct 47136  vonsn 47134
[Fremlin1] p. 35Lemma 121Asubsalsal 46802
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 46801  subsaliuncllem 46800
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47168  salpreimalegt 47152  salpreimaltle 47169
[Fremlin1] p. 35Proposition 121B (i)issmf 47171  issmff 47177  issmflem 47170
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47188  issmflelem 47187  smfpreimale 47197
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47199  issmfgtlem 47198
[Fremlin1] p. 36Definition 121Cdf-smblfn 47139  issmf 47171  issmff 47177  issmfge 47213  issmfgelem 47212  issmfgt 47199  issmfgtlem 47198  issmfle 47188  issmflelem 47187  issmflem 47170
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47150  salpreimagtlt 47173  salpreimalelt 47172
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47213  issmfgelem 47212
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47196
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47194  cnfsmf 47183
[Fremlin1] p. 36Proposition 121D (c)decsmf 47210  decsmflem 47209  incsmf 47185  incsmflem 47184
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47144  pimconstlt1 47145  smfconst 47192
[Fremlin1] p. 37Proposition 121E (b)smfadd 47208  smfaddlem1 47206  smfaddlem2 47207
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47239
[Fremlin1] p. 37Proposition 121E (d)smfmul 47238  smfmullem1 47234  smfmullem2 47235  smfmullem3 47236  smfmullem4 47237
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47240
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47243  smfpimbor1lem2 47242
[Fremlin1] p. 37Proposition 121E (g)smfco 47245
[Fremlin1] p. 37Proposition 121E (h)smfres 47233
[Fremlin1] p. 38Proposition 121E (e)smfrec 47232
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47241  smfresal 47231
[Fremlin1] p. 38Proposition 121F (a)smflim 47220  smflim2 47249  smflimlem1 47214  smflimlem2 47215  smflimlem3 47216  smflimlem4 47217  smflimlem5 47218  smflimlem6 47219  smflimmpt 47253
[Fremlin1] p. 38Proposition 121F (b)smfsup 47257  smfsuplem1 47254  smfsuplem2 47255  smfsuplem3 47256  smfsupmpt 47258  smfsupxr 47259
[Fremlin1] p. 38Proposition 121F (c)smfinf 47261  smfinflem 47260  smfinfmpt 47262
[Fremlin1] p. 39Remark 121Gsmflim 47220  smflim2 47249  smflimmpt 47253
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47251
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47281  smfdivdmmbl2 47284  smfinfdmmbl 47292  smfinfdmmbllem 47291  smfsupdmmbl 47288  smfsupdmmbllem 47287
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47271  smflimsuplem2 47264  smflimsuplem6 47268  smflimsuplem7 47269  smflimsuplem8 47270  smflimsupmpt 47272
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47274  smfliminflem 47273  smfliminfmpt 47275
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47139
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47285  fsupdm2 47286
[Fremlin1], p. 39Proposition 121Hadddmmbl 47276  adddmmbl2 47277  finfdm 47289  finfdm2 47290  fsupdm 47285  fsupdm2 47286  muldmmbl 47278  muldmmbl2 47279
[Fremlin1], p. 39Proposition 121F (c)finfdm 47289  finfdm2 47290
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25512
[Fremlin5] p. 213Lemma 565Cauniioovol 25555
[Fremlin5] p. 214Lemma 565Cauniioombl 25565
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38030
[Fremlin5] p. 220Theorem 565Maftc1anc 38033
[FreydScedrov] p. 283Axiom of Infinityax-inf 9548  inf1 9532  inf2 9533
[Gleason] p. 117Proposition 9-2.1df-enq 10823  enqer 10833
[Gleason] p. 117Proposition 9-2.2df-1nq 10828  df-nq 10824
[Gleason] p. 117Proposition 9-2.3df-plpq 10820  df-plq 10826
[Gleason] p. 119Proposition 9-2.4caovmo 7595  df-mpq 10821  df-mq 10827
[Gleason] p. 119Proposition 9-2.5df-rq 10829
[Gleason] p. 119Proposition 9-2.6ltexnq 10887
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10888  ltbtwnnq 10890
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10883
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10884
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10891
[Gleason] p. 121Definition 9-3.1df-np 10893
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10905
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10907
[Gleason] p. 122Definitiondf-1p 10894
[Gleason] p. 122Remark (1)prub 10906
[Gleason] p. 122Lemma 9-3.4prlem934 10945
[Gleason] p. 122Proposition 9-3.2df-ltp 10897
[Gleason] p. 122Proposition 9-3.3ltsopr 10944  psslinpr 10943  supexpr 10966  suplem1pr 10964  suplem2pr 10965
[Gleason] p. 123Proposition 9-3.5addclpr 10930  addclprlem1 10928  addclprlem2 10929  df-plp 10895
[Gleason] p. 123Proposition 9-3.5(i)addasspr 10934
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 10933
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 10946
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 10955  ltexprlem1 10948  ltexprlem2 10949  ltexprlem3 10950  ltexprlem4 10951  ltexprlem5 10952  ltexprlem6 10953  ltexprlem7 10954
[Gleason] p. 123Proposition 9-3.5(v)ltapr 10957  ltaprlem 10956
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 10958
[Gleason] p. 124Lemma 9-3.6prlem936 10959
[Gleason] p. 124Proposition 9-3.7df-mp 10896  mulclpr 10932  mulclprlem 10931  reclem2pr 10960
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 10941
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 10936
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 10935
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 10940
[Gleason] p. 124Proposition 9-3.7(v)recexpr 10963  reclem3pr 10961  reclem4pr 10962
[Gleason] p. 126Proposition 9-4.1df-enr 10967  enrer 10975
[Gleason] p. 126Proposition 9-4.2df-0r 10972  df-1r 10973  df-nr 10968
[Gleason] p. 126Proposition 9-4.3df-mr 10970  df-plr 10969  negexsr 11014  recexsr 11019  recexsrlem 11015
[Gleason] p. 127Proposition 9-4.4df-ltr 10971
[Gleason] p. 130Proposition 10-1.3creui 12143  creur 12142  cru 12140
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11100  axcnre 11076
[Gleason] p. 132Definition 10-3.1crim 15066  crimd 15183  crimi 15144  crre 15065  crred 15182  crrei 15143
[Gleason] p. 132Definition 10-3.2remim 15068  remimd 15149
[Gleason] p. 133Definition 10.36absval2 15235  absval2d 15399  absval2i 15349
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15092  cjaddd 15171  cjaddi 15139
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15093  cjmuld 15172  cjmuli 15140
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15091  cjcjd 15150  cjcji 15122
[Gleason] p. 133Proposition 10-3.4(f)cjre 15090  cjreb 15074  cjrebd 15153  cjrebi 15125  cjred 15177  rere 15073  rereb 15071  rerebd 15152  rerebi 15124  rered 15175
[Gleason] p. 133Proposition 10-3.4(h)addcj 15099  addcjd 15163  addcji 15134
[Gleason] p. 133Proposition 10-3.7(a)absval 15189
[Gleason] p. 133Proposition 10-3.7(b)abscj 15230  abscjd 15404  abscji 15353
[Gleason] p. 133Proposition 10-3.7(c)abs00 15240  abs00d 15400  abs00i 15350  absne0d 15401
[Gleason] p. 133Proposition 10-3.7(d)releabs 15273  releabsd 15405  releabsi 15354
[Gleason] p. 133Proposition 10-3.7(f)absmul 15245  absmuld 15408  absmuli 15356
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15233  sqabsaddi 15357
[Gleason] p. 133Proposition 10-3.7(h)abstri 15282  abstrid 15410  abstrii 15360
[Gleason] p. 134Definition 10-4.1df-exp 14013  exp0 14016  expp1 14019  expp1d 14098
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26659  cxpaddd 26697  expadd 14055  expaddd 14099  expaddz 14057
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26668  cxpmuld 26717  expmul 14058  expmuld 14100  expmulz 14059
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26665  mulcxpd 26708  mulexp 14052  mulexpd 14112  mulexpz 14053
[Gleason] p. 140Exercise 1znnen 16168
[Gleason] p. 141Definition 11-2.1fzval 13452
[Gleason] p. 168Proposition 12-2.1(a)climadd 15583  rlimadd 15594  rlimdiv 15597
[Gleason] p. 168Proposition 12-2.1(b)climsub 15585  rlimsub 15595
[Gleason] p. 168Proposition 12-2.1(c)climmul 15584  rlimmul 15596
[Gleason] p. 171Corollary 12-2.2climmulc2 15588
[Gleason] p. 172Corollary 12-2.5climrecl 15534
[Gleason] p. 172Proposition 12-2.4(c)climabs 15555  climcj 15556  climim 15558  climre 15557  rlimabs 15560  rlimcj 15561  rlimim 15563  rlimre 15562
[Gleason] p. 173Definition 12-3.1df-ltxr 11173  df-xr 11172  ltxr 13055
[Gleason] p. 175Definition 12-4.1df-limsup 15422  limsupval 15425
[Gleason] p. 180Theorem 12-5.1climsup 15621
[Gleason] p. 180Theorem 12-5.3caucvg 15630  caucvgb 15631  caucvgbf 45932  caucvgr 15627  climcau 15622
[Gleason] p. 182Exercise 3cvgcmp 15768
[Gleason] p. 182Exercise 4cvgrat 15837
[Gleason] p. 195Theorem 13-2.12abs1m 15287
[Gleason] p. 217Lemma 13-4.1btwnzge0 13776
[Gleason] p. 223Definition 14-1.1df-met 21336
[Gleason] p. 223Definition 14-1.1(a)met0 24317  xmet0 24316
[Gleason] p. 223Definition 14-1.1(b)metgt0 24333
[Gleason] p. 223Definition 14-1.1(c)metsym 24324
[Gleason] p. 223Definition 14-1.1(d)mettri 24326  mstri 24443  xmettri 24325  xmstri 24442
[Gleason] p. 225Definition 14-1.5xpsmet 24356
[Gleason] p. 230Proposition 14-2.6txlm 23622
[Gleason] p. 240Theorem 14-4.3metcnp4 25286
[Gleason] p. 240Proposition 14-4.2metcnp3 24514
[Gleason] p. 243Proposition 14-4.16addcn 24840  addcn2 15545  mulcn 24842  mulcn2 15547  subcn 24841  subcn2 15546
[Gleason] p. 295Remarkbcval3 14257  bcval4 14258
[Gleason] p. 295Equation 2bcpasc 14272
[Gleason] p. 295Definition of binomial coefficientbcval 14255  df-bc 14254
[Gleason] p. 296Remarkbcn0 14261  bcnn 14263
[Gleason] p. 296Theorem 15-2.8binom 15784
[Gleason] p. 308Equation 2ef0 16045
[Gleason] p. 308Equation 3efcj 16046
[Gleason] p. 309Corollary 15-4.3efne0 16052
[Gleason] p. 309Corollary 15-4.4efexp 16057
[Gleason] p. 310Equation 14sinadd 16120
[Gleason] p. 310Equation 15cosadd 16121
[Gleason] p. 311Equation 17sincossq 16132
[Gleason] p. 311Equation 18cosbnd 16137  sinbnd 16136
[Gleason] p. 311Lemma 15-4.7sqeqor 14167  sqeqori 14165
[Gleason] p. 311Definition of ` `df-pi 16026
[Godowski] p. 730Equation SFgoeqi 32364
[GodowskiGreechie] p. 249Equation IV3oai 31759
[Golan] p. 1Remarksrgisid 20179
[Golan] p. 1Definitiondf-srg 20157
[Golan] p. 149Definitiondf-slmd 33282
[Gonshor] p. 7Definitiondf-cuts 27771
[Gonshor] p. 9Theorem 2.5lesrec 27810  lesrecd 27811
[Gonshor] p. 10Theorem 2.6cofcut1 27931  cofcut1d 27932
[Gonshor] p. 10Theorem 2.7cofcut2 27933  cofcut2d 27934
[Gonshor] p. 12Theorem 2.9cofcutr 27935  cofcutr1d 27936  cofcutr2d 27937
[Gonshor] p. 13Definitiondf-adds 27971
[Gonshor] p. 14Theorem 3.1addsprop 27987
[Gonshor] p. 15Theorem 3.2addsunif 28013
[Gonshor] p. 17Theorem 3.4mulsprop 28141
[Gonshor] p. 18Theorem 3.5mulsunif 28161
[Gonshor] p. 28Lemma 4.2halfcut 28469
[Gonshor] p. 28Theorem 4.2pw2cut 28471
[Gonshor] p. 30Theorem 4.2addhalfcut 28470
[Gonshor] p. 39Theorem 4.4(b)elreno2 28506
[Gonshor] p. 95Theorem 6.1addbday 28029
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36362
[Gratzer] p. 23Section 0.6df-mre 17537
[Gratzer] p. 27Section 0.6df-mri 17539
[Hall] p. 1Section 1.1df-asslaw 48661  df-cllaw 48659  df-comlaw 48660
[Hall] p. 2Section 1.2df-clintop 48673
[Hall] p. 7Section 1.3df-sgrp2 48694
[Halmos] p. 28Partition ` `df-parts 39200  dfmembpart2 39205
[Halmos] p. 31Theorem 17.3riesz1 32156  riesz2 32157
[Halmos] p. 41Definition of Hermitianhmopadj2 32032
[Halmos] p. 42Definition of projector orderingpjordi 32264
[Halmos] p. 43Theorem 26.1elpjhmop 32276  elpjidm 32275  pjnmopi 32239
[Halmos] p. 44Remarkpjinormi 31778  pjinormii 31767
[Halmos] p. 44Theorem 26.2elpjch 32280  pjrn 31798  pjrni 31793  pjvec 31787
[Halmos] p. 44Theorem 26.3pjnorm2 31818
[Halmos] p. 44Theorem 26.4hmopidmpj 32245  hmopidmpji 32243
[Halmos] p. 45Theorem 27.1pjinvari 32282
[Halmos] p. 45Theorem 27.3pjoci 32271  pjocvec 31788
[Halmos] p. 45Theorem 27.4pjorthcoi 32260
[Halmos] p. 48Theorem 29.2pjssposi 32263
[Halmos] p. 48Theorem 29.3pjssdif1i 32266  pjssdif2i 32265
[Halmos] p. 50Definition of spectrumdf-spec 31946
[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 24968  df-phtpy 24947
[Hatcher] p. 26Definitiondf-pco 24981  df-pi1 24984
[Hatcher] p. 26Proposition 1.2phtpcer 24971
[Hatcher] p. 26Proposition 1.3pi1grp 25026
[Hefferon] p. 240Definition 3.12df-dmat 22464  df-dmatalt 48871
[Helfgott] p. 2Theoremtgoldbach 48290
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48275
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48287  bgoldbtbnd 48282  bgoldbtbnd 48282  tgblthelfgott 48288
[Helfgott] p. 5Proposition 1.1circlevma 34807
[Helfgott] p. 69Statement 7.49circlemethhgt 34808
[Helfgott] p. 69Statement 7.50hgt750lema 34822  hgt750lemb 34821  hgt750leme 34823  hgt750lemf 34818  hgt750lemg 34819
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48284  tgoldbachgt 34828  tgoldbachgtALTV 48285  tgoldbachgtd 34827
[Helfgott] p. 70Statement 7.49ax-hgt749 34809
[Herstein] p. 54Exercise 28df-grpo 30584
[Herstein] p. 55Lemma 2.2.1(a)grpideu 18909  grpoideu 30600  mndideu 18702
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 18939  grpoinveu 30610
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 18970  grpo2inv 30622
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 18983  grpoinvop 30624
[Herstein] p. 57Exercise 1dfgrp3e 19005
[Hitchcock] p. 5Rule A3mptnan 1770
[Hitchcock] p. 5Rule A4mptxor 1771
[Hitchcock] p. 5Rule A5mtpxor 1773
[Holland] p. 1519Theorem 2sumdmdi 32511
[Holland] p. 1520Lemma 5cdj1i 32524  cdj3i 32532  cdj3lem1 32525  cdjreui 32523
[Holland] p. 1524Lemma 7mddmdin0i 32522
[Holland95] p. 13Theorem 3.6hlathil 42418
[Holland95] p. 14Line 15hgmapvs 42348
[Holland95] p. 14Line 16hdmaplkr 42370
[Holland95] p. 14Line 17hdmapellkr 42371
[Holland95] p. 14Line 19hdmapglnm2 42368
[Holland95] p. 14Line 20hdmapip0com 42374
[Holland95] p. 14Theorem 3.6hdmapevec2 42293
[Holland95] p. 14Lines 24 and 25hdmapoc 42388
[Holland95] p. 204Definition of involutiondf-srng 20806
[Holland95] p. 212Definition of subspacedf-psubsp 39960
[Holland95] p. 214Lemma 3.3lclkrlem2v 41985
[Holland95] p. 214Definition 3.2df-lpolN 41938
[Holland95] p. 214Definition of nonsingularpnonsingN 40390
[Holland95] p. 215Lemma 3.3(1)dihoml4 41834  poml4N 40410
[Holland95] p. 215Lemma 3.3(2)dochexmid 41925  pexmidALTN 40435  pexmidN 40426
[Holland95] p. 218Theorem 3.6lclkr 41990
[Holland95] p. 218Definition of dual vector spacedf-ldual 39581  ldualset 39582
[Holland95] p. 222Item 1df-lines 39958  df-pointsN 39959
[Holland95] p. 222Item 2df-polarityN 40360
[Holland95] p. 223Remarkispsubcl2N 40404  omllaw4 39703  pol1N 40367  polcon3N 40374
[Holland95] p. 223Definitiondf-psubclN 40392
[Holland95] p. 223Equation for polaritypolval2N 40363
[Holmes] p. 40Definitiondf-xrn 38712
[Hughes] p. 44Equation 1.21bax-his3 31175
[Hughes] p. 47Definition of projection operatordfpjop 32273
[Hughes] p. 49Equation 1.30eighmre 32054  eigre 31926  eigrei 31925
[Hughes] p. 49Equation 1.31eighmorth 32055  eigorth 31929  eigorthi 31928
[Hughes] p. 137Remark (ii)eigposi 31927
[Huneke] p. 1Claim 1frgrncvvdeq 30399
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30395
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30396
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30397
[Huneke] p. 2Claim 2frgrregorufr 30415  frgrregorufr0 30414  frgrregorufrg 30416
[Huneke] p. 2Claim 3frgrhash2wsp 30422  frrusgrord 30431  frrusgrord0 30430
[Huneke] p. 2Statementdf-clwwlknon 30178
[Huneke] p. 2Statement 4frgrwopreglem4 30405
[Huneke] p. 2Statement 5frgrwopreg1 30408  frgrwopreg2 30409  frgrwopregasn 30406  frgrwopregbsn 30407
[Huneke] p. 2Statement 6frgrwopreglem5 30411
[Huneke] p. 2Statement 7fusgreghash2wspv 30425
[Huneke] p. 2Statement 8fusgreghash2wsp 30428
[Huneke] p. 2Statement 9clwlksndivn 30176  numclwlk1 30461  numclwlk1lem1 30459  numclwlk1lem2 30460  numclwwlk1 30451  numclwwlk8 30482
[Huneke] p. 2Definition 3frgrwopreglem1 30402
[Huneke] p. 2Definition 4df-clwlks 29859
[Huneke] p. 2Definition 62clwwlk 30437
[Huneke] p. 2Definition 7numclwwlkovh 30463  numclwwlkovh0 30462
[Huneke] p. 2Statement 10numclwwlk2 30471
[Huneke] p. 2Statement 11rusgrnumwlkg 30068
[Huneke] p. 2Statement 12numclwwlk3 30475
[Huneke] p. 2Statement 13numclwwlk5 30478
[Huneke] p. 2Statement 14numclwwlk7 30481
[Indrzejczak] p. 33Definition ` `Enatded 30493  natded 30493
[Indrzejczak] p. 33Definition ` `Inatded 30493
[Indrzejczak] p. 34Definition ` `Enatded 30493  natded 30493
[Indrzejczak] p. 34Definition ` `Inatded 30493
[Jech] p. 4Definition of classcv 1541  cvjust 2731
[Jech] p. 42Lemma 6.1alephexp1 10491
[Jech] p. 42Equation 6.1alephadd 10489  alephmul 10490
[Jech] p. 43Lemma 6.2infmap 10488  infmap2 10128
[Jech] p. 71Lemma 9.3jech9.3 9727
[Jech] p. 72Equation 9.3scott0 9799  scottex 9798
[Jech] p. 72Exercise 9.1rankval4 9780  rankval4b 35264
[Jech] p. 72Scheme "Collection Principle"cp 9804
[Jech] p. 78Noteopthprc 5686
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43358
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43446
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43447
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43370
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43374
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43375  rmyp1 43376
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43377  rmym1 43378
[JonesMatijasevic] p. 695Equation 2.11rmx0 43368  rmx1 43369  rmxluc 43379
[JonesMatijasevic] p. 695Equation 2.12rmy0 43372  rmy1 43373  rmyluc 43380
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43382
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43383
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43403  jm2.17b 43404  jm2.17c 43405
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43436
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43440
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43431
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43406  jm2.24nn 43402
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43445
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43451  rmygeid 43407
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43463
[Juillerat] p. 11Section *5etransc 46726  etransclem47 46724  etransclem48 46725
[Juillerat] p. 12Equation (7)etransclem44 46721
[Juillerat] p. 12Equation *(7)etransclem46 46723
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46709
[Juillerat] p. 13Proofetransclem35 46712
[Juillerat] p. 13Part of case 2 proven inetransclem38 46715
[Juillerat] p. 13Part of case 2 provenetransclem24 46701
[Juillerat] p. 13Part of case 2: proven inetransclem41 46718
[Juillerat] p. 14Proofetransclem23 46700
[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 37849  wl-motae 37851  wl-moteq 37850
[KalishMontague] p. 87Lemma 8spimvw 1988  spimw 1972
[KalishMontague] p. 87Lemma 9spfw 2035  spw 2036
[Kalmbach] p. 14Definition of latticechabs1 31607  chabs1i 31609  chabs2 31608  chabs2i 31610  chjass 31624  chjassi 31577  latabs1 18430  latabs2 18431
[Kalmbach] p. 15Definition of atomdf-at 32429  ela 32430
[Kalmbach] p. 15Definition of coverscvbr2 32374  cvrval2 39731
[Kalmbach] p. 16Definitiondf-ol 39635  df-oml 39636
[Kalmbach] p. 20Definition of commutescmbr 31675  cmbri 31681  cmtvalN 39668  df-cm 31674  df-cmtN 39634
[Kalmbach] p. 22Remarkomllaw5N 39704  pjoml5 31704  pjoml5i 31679
[Kalmbach] p. 22Definitionpjoml2 31702  pjoml2i 31676
[Kalmbach] p. 22Theorem 2(v)cmcm 31705  cmcmi 31683  cmcmii 31688  cmtcomN 39706
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39702  omlsi 31495  pjoml 31527  pjomli 31526
[Kalmbach] p. 22Definition of OML lawomllaw2N 39701
[Kalmbach] p. 23Remarkcmbr2i 31687  cmcm3 31706  cmcm3i 31685  cmcm3ii 31690  cmcm4i 31686  cmt3N 39708  cmt4N 39709  cmtbr2N 39710
[Kalmbach] p. 23Lemma 3cmbr3 31699  cmbr3i 31691  cmtbr3N 39711
[Kalmbach] p. 25Theorem 5fh1 31709  fh1i 31712  fh2 31710  fh2i 31713  omlfh1N 39715
[Kalmbach] p. 65Remarkchjatom 32448  chslej 31589  chsleji 31549  shslej 31471  shsleji 31461
[Kalmbach] p. 65Proposition 1chocin 31586  chocini 31545  chsupcl 31431  chsupval2 31501  h0elch 31346  helch 31334  hsupval2 31500  ocin 31387  ococss 31384  shococss 31385
[Kalmbach] p. 65Definition of subspace sumshsval 31403
[Kalmbach] p. 66Remarkdf-pjh 31486  pjssmi 32256  pjssmii 31772
[Kalmbach] p. 67Lemma 3osum 31736  osumi 31733
[Kalmbach] p. 67Lemma 4pjci 32291
[Kalmbach] p. 103Exercise 6atmd2 32491
[Kalmbach] p. 103Exercise 12mdsl0 32401
[Kalmbach] p. 140Remarkhatomic 32451  hatomici 32450  hatomistici 32453
[Kalmbach] p. 140Proposition 1atlatmstc 39776
[Kalmbach] p. 140Proposition 1(i)atexch 32472  lsatexch 39500
[Kalmbach] p. 140Proposition 1(ii)chcv1 32446  cvlcvr1 39796  cvr1 39867
[Kalmbach] p. 140Proposition 1(iii)cvexch 32465  cvexchi 32460  cvrexch 39877
[Kalmbach] p. 149Remark 2chrelati 32455  hlrelat 39859  hlrelat5N 39858  lrelat 39471
[Kalmbach] p. 153Exercise 5lsmcv 21129  lsmsatcv 39467  spansncv 31744  spansncvi 31743
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39486  spansncv2 32384
[Kalmbach] p. 266Definitiondf-st 32302
[Kalmbach2] p. 8Definition of adjointdf-adjh 31940
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10558  fpwwe2 10555
[KanamoriPincus] p. 416Corollary 1.3canth4 10559
[KanamoriPincus] p. 417Corollary 1.6canthp1 10566
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10561
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10563
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10576
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10580  gchxpidm 10581
[KanamoriPincus] p. 419Theorem 2.1gchacg 10592  gchhar 10591
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10126  unxpwdom 9495
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10582
[Kreyszig] p. 3Property M1metcl 24306  xmetcl 24305
[Kreyszig] p. 4Property M2meteq0 24313
[Kreyszig] p. 8Definition 1.1-8dscmet 24546
[Kreyszig] p. 12Equation 5conjmul 11861  muleqadd 11783
[Kreyszig] p. 18Definition 1.3-2mopnval 24412
[Kreyszig] p. 19Remarkmopntopon 24413
[Kreyszig] p. 19Theorem T1mopn0 24472  mopnm 24418
[Kreyszig] p. 19Theorem T2unimopn 24470
[Kreyszig] p. 19Definition of neighborhoodneibl 24475
[Kreyszig] p. 20Definition 1.3-3metcnp2 24516
[Kreyszig] p. 25Definition 1.4-1lmbr 23232  lmmbr 25234  lmmbr2 25235
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23354
[Kreyszig] p. 28Theorem 1.4-5lmcau 25289
[Kreyszig] p. 28Definition 1.4-3iscau 25252  iscmet2 25270
[Kreyszig] p. 30Theorem 1.4-7cmetss 25292
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23435  metelcls 25281
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25282  metcld2 25283
[Kreyszig] p. 51Equation 2clmvneg1 25075  lmodvneg1 20889  nvinv 30730  vcm 30667
[Kreyszig] p. 51Equation 1aclm0vs 25071  lmod0vs 20879  slmd0vs 33305  vc0 30665
[Kreyszig] p. 51Equation 1blmodvs0 20880  slmdvs0 33306  vcz 30666
[Kreyszig] p. 58Definition 2.2-1imsmet 30782  ngpmet 24577  nrmmetd 24548
[Kreyszig] p. 59Equation 1imsdval 30777  imsdval2 30778  ncvspds 25137  ngpds 24578
[Kreyszig] p. 63Problem 1nmval 24563  nvnd 30779
[Kreyszig] p. 64Problem 2nmeq0 24592  nmge0 24591  nvge0 30764  nvz 30760
[Kreyszig] p. 64Problem 3nmrtri 24598  nvabs 30763
[Kreyszig] p. 91Definition 2.7-1isblo3i 30892
[Kreyszig] p. 92Equation 2df-nmoo 30836
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 30898  blocni 30896
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 30897
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25180  ipeq0 21626  ipz 30810
[Kreyszig] p. 135Problem 2cphpyth 25192  pythi 30941
[Kreyszig] p. 137Lemma 3-2.1(a)sii 30945
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25214
[Kreyszig] p. 144Equation 4supcvg 15810
[Kreyszig] p. 144Theorem 3.3-1minvec 25412  minveco 30975
[Kreyszig] p. 196Definition 3.9-1df-aj 30841
[Kreyszig] p. 247Theorem 4.7-2bcth 25305
[Kreyszig] p. 249Theorem 4.7-3ubth 30964
[Kreyszig] p. 470Definition of positive operator orderingleop 32214  leopg 32213
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32232
[Kreyszig] p. 525Theorem 10.1-1htth 31009
[Kulpa] p. 547Theorempoimir 37985
[Kulpa] p. 547Equation (1)poimirlem32 37984
[Kulpa] p. 547Equation (2)poimirlem31 37983
[Kulpa] p. 548Theorembroucube 37986
[Kulpa] p. 548Equation (6)poimirlem26 37978
[Kulpa] p. 548Equation (7)poimirlem27 37979
[Kunen] p. 10Axiom 0ax6e 2388  axnul 5240
[Kunen] p. 11Axiom 3axnul 5240
[Kunen] p. 12Axiom 6zfrep6 5224
[Kunen] p. 24Definition 10.24mapval 8776  mapvalg 8774
[Kunen] p. 30Lemma 10.20fodomg 10433
[Kunen] p. 31Definition 10.24mapex 7883
[Kunen] p. 95Definition 2.1df-r1 9677
[Kunen] p. 97Lemma 2.10r1elss 9719  r1elssi 9718
[Kunen] p. 107Exercise 4rankop 9771  rankopb 9765  rankuni 9776  rankxplim 9792  rankxpsuc 9795
[Kunen2] p. 47Lemma I.9.9relpfr 45396
[Kunen2] p. 53Lemma I.9.21trfr 45404
[Kunen2] p. 53Lemma I.9.24(2)wffr 45403
[Kunen2] p. 53Definition I.9.20tcfr 45405
[Kunen2] p. 95Lemma I.16.2ralabso 45410  rexabso 45411
[Kunen2] p. 96Example I.16.3disjabso 45417  n0abso 45418  ssabso 45416
[Kunen2] p. 111Lemma II.2.4(1)traxext 45419
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45429
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45424
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45427
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45428
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45423
[Kunen2] p. 112Corollary II.2.5wfaxext 45435  wfaxpr 45440  wfaxreg 45442  wfaxrep 45436  wfaxsep 45437  wfaxun 45441
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45426
[Kunen2] p. 113Corollary II.2.9wfaxpow 45439
[Kunen2] p. 114Theorem II.2.13wfaxext 45435
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45434  omelaxinf2 45431
[Kunen2] p. 114Corollary II.2.12wfac8prim 45444  wfaxinf2 45443
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45457  permaxext 45447  permaxinf2 45455  permaxnul 45450  permaxpow 45451  permaxpr 45452  permaxrep 45448  permaxsep 45449  permaxun 45453
[Kunen2] p. 148Definition II.9.1brpermmodel 45445
[Kunen2] p. 149Exercise II.9.3permac8prim 45456
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4947
[Lang] , p. 225Corollary 1.3finexttrb 33830
[Lang] p. Definitiondf-rn 5633
[Lang] p. 3Statementlidrideqd 18626  mndbn0 18707
[Lang] p. 3Definitiondf-mnd 18692
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18644
[Lang] p. 4Property of composites. Second formulagsumccat 18798
[Lang] p. 5Equationgsumreidx 19881
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48655
[Lang] p. 6Examplenn0mnd 48652
[Lang] p. 6Equationgsumxp2 19944
[Lang] p. 6Statementcycsubm 19166
[Lang] p. 6Definitionmulgnn0gsum 19045
[Lang] p. 6Observationmndlsmidm 19634
[Lang] p. 7Definitiondfgrp2e 18928
[Lang] p. 30Definitiondf-tocyc 33188
[Lang] p. 32Property (a)cyc3genpm 33233
[Lang] p. 32Property (b)cyc3conja 33238  cycpmconjv 33223
[Lang] p. 53Definitiondf-cat 17623
[Lang] p. 53Axiom CAT 1cat1 18053  cat1lem 18052
[Lang] p. 54Definitiondf-iso 17705
[Lang] p. 57Definitiondf-inito 17940  df-termo 17941
[Lang] p. 58Exampleirinitoringc 21467
[Lang] p. 58Statementinitoeu1 17967  termoeu1 17974
[Lang] p. 62Definitiondf-func 17814
[Lang] p. 65Definitiondf-nat 17902
[Lang] p. 91Notedf-ringc 20612
[Lang] p. 92Statementmxidlprm 33550
[Lang] p. 92Definitionisprmidlc 33527
[Lang] p. 128Remarkdsmmlmod 21733
[Lang] p. 129Prooflincscm 48903  lincscmcl 48905  lincsum 48902  lincsumcl 48904
[Lang] p. 129Statementlincolss 48907
[Lang] p. 129Observationdsmmfi 21726
[Lang] p. 141Theorem 5.3dimkerim 33792  qusdimsum 33793
[Lang] p. 141Corollary 5.4lssdimle 33772
[Lang] p. 147Definitionsnlindsntor 48944
[Lang] p. 504Statementmat1 22421  matring 22417
[Lang] p. 504Definitiondf-mamu 22365
[Lang] p. 505Statementmamuass 22376  mamutpos 22432  matassa 22418  mattposvs 22429  tposmap 22431
[Lang] p. 513Definitionmdet1 22575  mdetf 22569
[Lang] p. 513Theorem 4.4cramer 22665
[Lang] p. 514Proposition 4.6mdetleib 22561
[Lang] p. 514Proposition 4.8mdettpos 22585
[Lang] p. 515Definitiondf-minmar1 22609  smadiadetr 22649
[Lang] p. 515Corollary 4.9mdetero 22584  mdetralt 22582
[Lang] p. 517Proposition 4.15mdetmul 22597
[Lang] p. 518Definitiondf-madu 22608
[Lang] p. 518Proposition 4.16madulid 22619  madurid 22618  matinv 22651
[Lang] p. 561Theorem 3.1cayleyhamilton 22864
[Lang], p. 190Chapter 6vieta 33744
[Lang], p. 224Proposition 1.1extdgfialg 33859  finextalg 33863
[Lang], p. 224Proposition 1.2extdgmul 33828  fedgmul 33796
[Lang], p. 225Proposition 1.4algextdeg 33890
[Lang], p. 561Remarkchpmatply1 22806
[Lang], p. 561Definitiondf-chpmat 22801
[Lang2] p. 3Notationsdf-ind 12149
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 44776
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 44771
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 44777
[LeBlanc] p. 277Rule R2axnul 5240
[Levy] p. 12Axiom 4.3.1df-clab 2716  wl-df.clab 37834
[Levy] p. 59Definitiondf-ttrcl 9618
[Levy] p. 64Theorem 5.6(ii)frinsg 9664
[Levy] p. 338Axiomdf-clel 2812  df-cleq 2729  wl-df.clel 37838  wl-df.cleq 37835
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2812  df-cleq 2729  wl-df.clel 37838  wl-df.cleq 37835
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2716  wl-df.clab 37834
[Levy] p. 358Axiomdf-clab 2716  wl-df.clab 37834
[Levy58] p. 2Definition Iisfin1-3 10297
[Levy58] p. 2Definition IIdf-fin2 10197
[Levy58] p. 2Definition Iadf-fin1a 10196
[Levy58] p. 2Definition IIIdf-fin3 10199
[Levy58] p. 3Definition Vdf-fin5 10200
[Levy58] p. 3Definition IVdf-fin4 10198
[Levy58] p. 4Definition VIdf-fin6 10201
[Levy58] p. 4Definition VIIdf-fin7 10202
[Levy58], p. 3Theorem 1fin1a2 10326
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27669
[Lipparini] p. 3Lemma 2.1.4noresle 27680
[Lipparini] p. 6Proposition 4.2noinfbnd1 27712  nosupbnd1 27697
[Lipparini] p. 6Proposition 4.3noinfbnd2 27714  nosupbnd2 27699
[Lipparini] p. 7Theorem 5.1noetasuplem3 27718  noetasuplem4 27719
[Lipparini] p. 7Corollary 4.4nosupinfsep 27715
[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 32499
[Maeda] p. 168Lemma 5mdsym 32503  mdsymi 32502
[Maeda] p. 168Lemma 4(i)mdsymlem4 32497  mdsymlem6 32499  mdsymlem7 32500
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32501
[MaedaMaeda] p. 1Remarkssdmd1 32404  ssdmd2 32405  ssmd1 32402  ssmd2 32403
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32400
[MaedaMaeda] p. 1Definition 1.1df-dmd 32372  df-md 32371  mdbr 32385
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32422  mdslj1i 32410  mdslj2i 32411  mdslle1i 32408  mdslle2i 32409  mdslmd1i 32420  mdslmd2i 32421
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32412  mdsl2bi 32414  mdsl2i 32413
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32426
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32423
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32424
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32401
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32406  mdsl3 32407
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32425
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32520
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 39778  hlrelat1 39857
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39496
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32427  cvmdi 32415  cvnbtwn4 32380  cvrnbtwn4 39736
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32428
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 39797  cvp 32466  cvrp 39873  lcvp 39497
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32490
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32489
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 39790  hlexch4N 39849
[MaedaMaeda] p. 34Exercise 7.1atabsi 32492
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 39900
[MaedaMaeda] p. 61Definition 15.10psubN 40206  atpsubN 40210  df-pointsN 39959  pointpsubN 40208
[MaedaMaeda] p. 62Theorem 15.5df-pmap 39961  pmap11 40219  pmaple 40218  pmapsub 40225  pmapval 40214
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40222  pmap1N 40224
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40227  pmapglb2N 40228  pmapglb2xN 40229  pmapglbx 40226
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40309
[MaedaMaeda] p. 67Postulate PS1ps-1 39934
[MaedaMaeda] p. 68Lemma 16.2df-padd 40253  paddclN 40299  paddidm 40298
[MaedaMaeda] p. 68Condition PS2ps-2 39935
[MaedaMaeda] p. 68Equation 16.2.1paddass 40295
[MaedaMaeda] p. 69Lemma 16.4ps-1 39934
[MaedaMaeda] p. 69Theorem 16.4ps-2 39935
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19639  lsmmod2 19640  lssats 39469  shatomici 32449  shatomistici 32452  shmodi 31481  shmodsi 31480
[MaedaMaeda] p. 130Remark 29.6dmdmd 32391  mdsymlem7 32500
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31680
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31584
[MaedaMaeda] p. 139Remarksumdmdii 32506
[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 30490
[Margaris] p. 59Section 14notnotrALTVD 45356
[Margaris] p. 60Theorem 8jcn 162
[Margaris] p. 60Section 14con3ALTVD 45357
[Margaris] p. 79Rule Cexinst01 45067  exinst11 45068
[Margaris] p. 89Theorem 19.219.2 1978  19.2g 2196  r19.2z 4440
[Margaris] p. 89Theorem 19.319.3 2210  rr19.3v 3610
[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 30491  conventions-labels 30491  conventions-labels 30491  conventions-labels 30491
[Margaris] p. 90Theorem 19.14exnal 1829
[Margaris] p. 90Theorem 19.152albi 44820  albi 1820
[Margaris] p. 90Theorem 19.1619.16 2233
[Margaris] p. 90Theorem 19.1719.17 2234
[Margaris] p. 90Theorem 19.182exbi 44822  exbi 1849
[Margaris] p. 90Theorem 19.1919.19 2237
[Margaris] p. 90Theorem 19.202alim 44819  2alimdv 1920  alimd 2220  alimdh 1819  alimdv 1918  ax-4 1811  ralimdaa 3239  ralimdv 3152  ralimdva 3150  ralimdvva 3185  sbcimdv 3798
[Margaris] p. 90Theorem 19.2119.21 2215  19.21h 2294  19.21t 2214  19.21vv 44818  alrimd 2223  alrimdd 2222  alrimdh 1865  alrimdv 1931  alrimi 2221  alrimih 1826  alrimiv 1929  alrimivv 1930  bj-alrimdh 36902  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 44821  2eximdv 1921  bj-exim 36917  exim 1836  eximd 2224  eximdh 1866  eximdv 1919  rexim 3079  reximd2a 3248  reximdai 3240  reximdd 45593  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 44966  exlimiv 1932  exlimivv 1934  rexlimd3 45589  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 4451  r19.27zv 4452
[Margaris] p. 90Theorem 19.2819.28 2236  19.28vv 44828  r19.28z 4443  r19.28zf 45604  r19.28zv 4447  rr19.28v 3611
[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 44826
[Margaris] p. 90Theorem 19.3219.32 2241  r19.32 47543
[Margaris] p. 90Theorem 19.3319.33-2 44824  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 44825  r19.36zv 4453
[Margaris] p. 90Theorem 19.3719.37 2240  19.37vv 44827  r19.37zv 4448
[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 44992
[Margaris] p. 90Theorem 19.4219.42 2244
[Margaris] p. 90Theorem 19.4319.43 1884
[Margaris] p. 90Theorem 19.4419.44 2245  r19.44zv 4450
[Margaris] p. 90Theorem 19.4519.45 2246  r19.45zv 4449
[Margaris] p. 110Exercise 2(b)eu1 2611
[Mayet] p. 370Remarkjpi 32361  largei 32358  stri 32348
[Mayet3] p. 9Definition of CH-statesdf-hst 32303  ishst 32305
[Mayet3] p. 10Theoremhstrbi 32357  hstri 32356
[Mayet3] p. 1223Theorem 4.1mayete3i 31819
[Mayet3] p. 1240Theorem 7.1mayetes3i 31820
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32369
[MegPav2000] p. 2345Definition 3.4-1chintcl 31423  chsupcl 31431
[MegPav2000] p. 2345Definition 3.4-2hatomic 32451
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32445
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32472
[MegPav2000] p. 2366Figure 7pl42N 40440
[MegPav2002] p. 362Lemma 2.2latj31 18442  latj32 18440  latjass 18438
[Megill] p. 444Axiom C5ax-5 1912  ax5ALT 39364
[Megill] p. 444Section 7conventions 30490
[Megill] p. 445Lemma L12aecom-o 39358  ax-c11n 39345  axc11n 2431
[Megill] p. 446Lemma L17equtrr 2024
[Megill] p. 446Lemma L18ax6fromc10 39353
[Megill] p. 446Lemma L19hbnae-o 39385  hbnae 2437
[Megill] p. 447Remark 9.1dfsb1 2486  sbid 2263  sbidd-misc 50191  sbidd 50190
[Megill] p. 448Remark 9.6axc14 2468
[Megill] p. 448Scheme C4'ax-c4 39341
[Megill] p. 448Scheme C5'ax-c5 39340  sp 2191
[Megill] p. 448Scheme C6'ax-11 2163
[Megill] p. 448Scheme C7'ax-c7 39342
[Megill] p. 448Scheme C8'ax-7 2010
[Megill] p. 448Scheme C9'ax-c9 39347
[Megill] p. 448Scheme C10'ax-6 1969  ax-c10 39343
[Megill] p. 448Scheme C11'ax-c11 39344
[Megill] p. 448Scheme C12'ax-8 2116
[Megill] p. 448Scheme C13'ax-9 2124
[Megill] p. 448Scheme C14'ax-c14 39348
[Megill] p. 448Scheme C15'ax-c15 39346
[Megill] p. 448Scheme C16'ax-c16 39349
[Megill] p. 448Theorem 9.4dral1-o 39361  dral1 2444  dral2-o 39387  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 39354  hba1 2300
[Mendelson] p. 35Axiom A3hirstL-ax3 47337
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3818  rspsbca 3819  stdpc4 2074
[Mendelson] p. 69Axiom 5ax-c4 39341  ra4 3825  stdpc5 2216
[Mendelson] p. 81Rule Cexlimiv 1932
[Mendelson] p. 95Axiom 6stdpc6 2030
[Mendelson] p. 95Axiom 7stdpc7 2258
[Mendelson] p. 225Axiom system NBGru 3727
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5460
[Mendelson] p. 231Exercise 4.10(k)inv1 4339
[Mendelson] p. 231Exercise 4.10(l)unv 4340
[Mendelson] p. 231Exercise 4.10(n)dfin3 4218
[Mendelson] p. 231Exercise 4.10(o)df-nul 4275
[Mendelson] p. 231Exercise 4.10(q)dfin4 4219
[Mendelson] p. 231Exercise 4.10(s)ddif 4082
[Mendelson] p. 231Definition of uniondfun3 4217
[Mendelson] p. 235Exercise 4.12(c)univ 5396
[Mendelson] p. 235Exercise 4.12(d)pwv 4848
[Mendelson] p. 235Exercise 4.12(j)pwin 5513
[Mendelson] p. 235Exercise 4.12(k)pwunss 4560
[Mendelson] p. 235Exercise 4.12(l)pwssun 5514
[Mendelson] p. 235Exercise 4.12(n)uniin 4875
[Mendelson] p. 235Exercise 4.12(p)reli 5773
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6225
[Mendelson] p. 244Proposition 4.8(g)epweon 7720
[Mendelson] p. 246Definition of successordf-suc 6321
[Mendelson] p. 250Exercise 4.36oelim2 8522
[Mendelson] p. 254Proposition 4.22(b)xpen 9069
[Mendelson] p. 254Proposition 4.22(c)xpsnen 8990  xpsneng 8991
[Mendelson] p. 254Proposition 4.22(d)xpcomen 8997  xpcomeng 8998
[Mendelson] p. 254Proposition 4.22(e)xpassen 9000
[Mendelson] p. 255Definitionbrsdom 8912
[Mendelson] p. 255Exercise 4.39endisj 8993
[Mendelson] p. 255Exercise 4.41mapprc 8768
[Mendelson] p. 255Exercise 4.43mapsnen 8975  mapsnend 8974
[Mendelson] p. 255Exercise 4.45mapunen 9075
[Mendelson] p. 255Exercise 4.47xpmapen 9074
[Mendelson] p. 255Exercise 4.42(a)map0e 8821
[Mendelson] p. 255Exercise 4.42(b)map1 8978
[Mendelson] p. 257Proposition 4.24(a)undom 8994
[Mendelson] p. 258Exercise 4.56(c)djuassen 10090  djucomen 10089
[Mendelson] p. 258Exercise 4.56(f)djudom1 10094
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10088
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8457
[Mendelson] p. 266Proposition 4.34(f)oaordex 8484
[Mendelson] p. 275Proposition 4.42(d)entri3 10470
[Mendelson] p. 281Definitiondf-r1 9677
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9726
[Mendelson] p. 287Axiom system MKru 3727
[MertziosUnger] p. 152Definitiondf-frgr 30349
[MertziosUnger] p. 153Remark 1frgrconngr 30384
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30386  vdgn1frgrv3 30387
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30388
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30381
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30374  2pthfrgrrn 30372  2pthfrgrrn2 30373
[Mittelstaedt] p. 9Definitiondf-oc 31343
[Monk1] p. 22Remarkconventions 30490
[Monk1] p. 22Theorem 3.1conventions 30490
[Monk1] p. 26Theorem 2.8(vii)ssin 4180
[Monk1] p. 33Theorem 3.2(i)ssrel 5730  ssrelf 32708
[Monk1] p. 33Theorem 3.2(ii)eqrel 5731
[Monk1] p. 34Definition 3.3df-opab 5149
[Monk1] p. 36Theorem 3.7(i)coi1 6219  coi2 6220
[Monk1] p. 36Theorem 3.8(v)dm0 5867  rn0 5873
[Monk1] p. 36Theorem 3.7(ii)cnvi 6097
[Monk1] p. 37Theorem 3.13(i)relxp 5640
[Monk1] p. 37Theorem 3.13(x)dmxp 5876  rnxp 6126
[Monk1] p. 37Theorem 3.13(ii)0xp 5721  xp0 5722
[Monk1] p. 38Theorem 3.16(ii)ima0 6034
[Monk1] p. 38Theorem 3.16(viii)imai 6031
[Monk1] p. 39Theorem 3.17imaex 7856  imaexg 7855
[Monk1] p. 39Theorem 3.16(xi)imassrn 6028
[Monk1] p. 41Theorem 4.3(i)fnopfv 7019  funfvop 6994
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6886
[Monk1] p. 42Theorem 4.4(iii)fvelima 6897
[Monk1] p. 43Theorem 4.6funun 6536
[Monk1] p. 43Theorem 4.8(iv)dff13 7200  dff13f 7201
[Monk1] p. 46Theorem 4.15(v)funex 7165  funrnex 7898
[Monk1] p. 50Definition 5.4fniunfv 7193
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6183
[Monk1] p. 52Theorem 5.11(viii)ssint 4907
[Monk1] p. 52Definition 5.13 (i)1stval2 7950  df-1st 7933
[Monk1] p. 52Definition 5.13 (ii)2ndval2 7951  df-2nd 7934
[Monk1] p. 112Theorem 15.17(v)ranksn 9767  ranksnb 9740
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9768
[Monk1] p. 112Theorem 15.17(iii)rankun 9769  rankunb 9763
[Monk1] p. 113Theorem 15.18r1val3 9751
[Monk1] p. 113Definition 15.19df-r1 9677  r1val2 9750
[Monk1] p. 117Lemmazorn2 10417  zorn2g 10414
[Monk1] p. 133Theorem 18.11cardom 9899
[Monk1] p. 133Theorem 18.12canth3 10472
[Monk1] p. 133Theorem 18.14carduni 9894
[Monk2] p. 105Axiom C4ax-4 1811
[Monk2] p. 105Axiom C7ax-7 2010
[Monk2] p. 105Axiom C8ax-12 2185  ax-c15 39346  ax12v2 2187
[Monk2] p. 108Lemma 5ax-c4 39341
[Monk2] p. 109Lemma 12ax-11 2163
[Monk2] p. 109Lemma 15equvini 2460  equvinv 2031  eqvinop 5433
[Monk2] p. 113Axiom C5-1ax-5 1912  ax5ALT 39364
[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 39354  hba1 2300
[Monk2] p. 114Lemma 23nfia1 2159
[Monk2] p. 114Lemma 24nfa2 2182  nfra2 3339  nfra2w 3274
[Moore] p. 53Part Idf-mre 17537
[Munkres] p. 77Example 2distop 22969  indistop 22976  indistopon 22975
[Munkres] p. 77Example 3fctop 22978  fctop2 22979
[Munkres] p. 77Example 4cctop 22980
[Munkres] p. 78Definition of basisdf-bases 22920  isbasis3g 22923
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17395  tgval2 22930
[Munkres] p. 79Remarktgcl 22943
[Munkres] p. 80Lemma 2.1tgval3 22937
[Munkres] p. 80Lemma 2.2tgss2 22961  tgss3 22960
[Munkres] p. 81Lemma 2.3basgen 22962  basgen2 22963
[Munkres] p. 83Exercise 3topdifinf 37676  topdifinfeq 37677  topdifinffin 37675  topdifinfindis 37673
[Munkres] p. 89Definition of subspace topologyresttop 23134
[Munkres] p. 93Theorem 6.1(1)0cld 23012  topcld 23009
[Munkres] p. 93Theorem 6.1(2)iincld 23013
[Munkres] p. 93Theorem 6.1(3)uncld 23015
[Munkres] p. 94Definition of closureclsval 23011
[Munkres] p. 94Definition of interiorntrval 23010
[Munkres] p. 95Theorem 6.5(a)clsndisj 23049  elcls 23047
[Munkres] p. 95Theorem 6.5(b)elcls3 23057
[Munkres] p. 97Theorem 6.6clslp 23122  neindisj 23091
[Munkres] p. 97Corollary 6.7cldlp 23124
[Munkres] p. 97Definition of limit pointislp2 23119  lpval 23113
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23289
[Munkres] p. 102Definition of continuous functiondf-cn 23201  iscn 23209  iscn2 23212
[Munkres] p. 107Theorem 7.2(g)cncnp 23254  cncnp2 23255  cncnpi 23252  df-cnp 23202  iscnp 23211  iscnp2 23213
[Munkres] p. 127Theorem 10.1metcn 24517
[Munkres] p. 128Theorem 10.3metcn4 25287
[Nathanson] p. 123Remarkreprgt 34786  reprinfz1 34787  reprlt 34784
[Nathanson] p. 123Definitiondf-repr 34774
[Nathanson] p. 123Chapter 5.1circlemethnat 34806
[Nathanson] p. 123Propositionbreprexp 34798  breprexpnat 34799  itgexpif 34771
[NielsenChuang] p. 195Equation 4.73unierri 32195
[OeSilva] p. 2042Section 2ax-bgbltosilva 48283
[Pfenning] p. 17Definition XMnatded 30493
[Pfenning] p. 17Definition NNCnatded 30493  notnotrd 133
[Pfenning] p. 17Definition ` `Cnatded 30493
[Pfenning] p. 18Rule"natded 30493
[Pfenning] p. 18Definition /\Inatded 30493
[Pfenning] p. 18Definition ` `Enatded 30493  natded 30493  natded 30493  natded 30493  natded 30493
[Pfenning] p. 18Definition ` `Inatded 30493  natded 30493  natded 30493  natded 30493  natded 30493
[Pfenning] p. 18Definition ` `ELnatded 30493
[Pfenning] p. 18Definition ` `ERnatded 30493
[Pfenning] p. 18Definition ` `Ea,unatded 30493
[Pfenning] p. 18Definition ` `IRnatded 30493
[Pfenning] p. 18Definition ` `Ianatded 30493
[Pfenning] p. 127Definition =Enatded 30493
[Pfenning] p. 127Definition =Inatded 30493
[Ponnusamy] p. 361Theorem 6.44cphip0l 25178  df-dip 30792  dip0l 30809  ip0l 21624
[Ponnusamy] p. 361Equation 6.45cphipval 25219  ipval 30794
[Ponnusamy] p. 362Equation I1dipcj 30805  ipcj 21622
[Ponnusamy] p. 362Equation I3cphdir 25181  dipdir 30933  ipdir 21627  ipdiri 30921
[Ponnusamy] p. 362Equation I4ipidsq 30801  nmsq 25170
[Ponnusamy] p. 362Equation 6.46ip0i 30916
[Ponnusamy] p. 362Equation 6.47ip1i 30918
[Ponnusamy] p. 362Equation 6.48ip2i 30919
[Ponnusamy] p. 363Equation I2cphass 25187  dipass 30936  ipass 21633  ipassi 30932
[Prugovecki] p. 186Definition of brabraval 32035  df-bra 31941
[Prugovecki] p. 376Equation 8.1df-kb 31942  kbval 32045
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32473
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40345
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32487  atcvat4i 32488  cvrat3 39899  cvrat4 39900  lsatcvat3 39509
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32373  cvrval 39726  df-cv 32370  df-lcv 39476  lspsncv0 21134
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40357
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40358
[Quine] p. 16Definition 2.1df-clab 2716  rabid 3411  rabidd 45600  wl-df.clab 37834
[Quine] p. 17Definition 2.1''dfsb7 2286
[Quine] p. 18Definition 2.7df-cleq 2729  wl-df.cleq 37835
[Quine] p. 19Definition 2.9conventions 30490  df-v 3432
[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  wl-df.clel 37838
[Quine] p. 41Theorem 6.4eqid 2737  eqid1 30557
[Quine] p. 41Theorem 6.5eqcom 2744
[Quine] p. 42Theorem 6.6df-sbc 3730
[Quine] p. 42Theorem 6.7dfsbcq 3731  dfsbcq2 3732
[Quine] p. 43Theorem 6.8vex 3434
[Quine] p. 43Theorem 6.9isset 3444
[Quine] p. 44Theorem 7.3spcgf 3534  spcgv 3539  spcimgf 3496
[Quine] p. 44Theorem 6.11spsbc 3742  spsbcd 3743
[Quine] p. 44Theorem 6.12elex 3451
[Quine] p. 44Theorem 6.13elab 3623  elabg 3620  elabgf 3618
[Quine] p. 44Theorem 6.14noel 4279
[Quine] p. 48Theorem 7.2snprc 4662
[Quine] p. 48Definition 7.1df-pr 4571  df-sn 4569
[Quine] p. 49Theorem 7.4snss 4729  snssg 4728
[Quine] p. 49Theorem 7.5prss 4764  prssg 4763
[Quine] p. 49Theorem 7.6prid1 4707  prid1g 4705  prid2 4708  prid2g 4706  snid 4607  snidg 4605
[Quine] p. 51Theorem 7.12snex 5374
[Quine] p. 51Theorem 7.13prex 5373
[Quine] p. 53Theorem 8.2unisn 4870  unisnALT 45367  unisng 4869
[Quine] p. 53Theorem 8.3uniun 4874
[Quine] p. 54Theorem 8.6elssuni 4882
[Quine] p. 54Theorem 8.7uni0 4879
[Quine] p. 56Theorem 8.17uniabio 6460
[Quine] p. 56Definition 8.18dfaiota2 47531  dfiota2 6447
[Quine] p. 57Theorem 8.19aiotaval 47540  iotaval 6464
[Quine] p. 57Theorem 8.22iotanul 6470
[Quine] p. 58Theorem 8.23iotaex 6466
[Quine] p. 58Definition 9.1df-op 4575
[Quine] p. 61Theorem 9.5opabid 5471  opabidw 5470  opelopab 5488  opelopaba 5482  opelopabaf 5490  opelopabf 5491  opelopabg 5484  opelopabga 5479  opelopabgf 5486  oprabid 7390  oprabidw 7389
[Quine] p. 64Definition 9.11df-xp 5628
[Quine] p. 64Definition 9.12df-cnv 5630
[Quine] p. 64Definition 9.15df-id 5517
[Quine] p. 65Theorem 10.3fun0 6555
[Quine] p. 65Theorem 10.4funi 6522
[Quine] p. 65Theorem 10.5funsn 6543  funsng 6541
[Quine] p. 65Definition 10.1df-fun 6492
[Quine] p. 65Definition 10.2args 6049  dffv4 6829
[Quine] p. 68Definition 10.11conventions 30490  df-fv 6498  fv2 6827
[Quine] p. 124Theorem 17.3nn0opth2 14223  nn0opth2i 14222  nn0opthi 14221  omopthi 8588
[Quine] p. 177Definition 25.2df-rdg 8340
[Quine] p. 232Equation icarddom 10465
[Quine] p. 284Axiom 39(vi)funimaex 6578  funimaexg 6577
[Quine] p. 331Axiom system NFru 3727
[ReedSimon] p. 36Definition (iii)ax-his3 31175
[ReedSimon] p. 63Exercise 4(a)df-dip 30792  polid 31250  polid2i 31248  polidi 31249
[ReedSimon] p. 63Exercise 4(b)df-ph 30904
[ReedSimon] p. 195Remarklnophm 32110  lnophmi 32109
[Retherford] p. 49Exercise 1(i)leopadd 32223
[Retherford] p. 49Exercise 1(ii)leopmul 32225  leopmuli 32224
[Retherford] p. 49Exercise 1(iv)leoptr 32228
[Retherford] p. 49Definition VI.1df-leop 31943  leoppos 32217
[Retherford] p. 49Exercise 1(iii)leoptri 32227
[Retherford] p. 49Definition of operator orderingleop3 32216
[Ribenboim] p. 181Remarknprmdvdsfacm1 48084
[Ribenboim], p. 181Statementppivalnn 48092
[Roman] p. 4Definitiondf-dmat 22464  df-dmatalt 48871
[Roman] p. 18Part Preliminariesdf-rng 20123
[Roman] p. 19Part Preliminariesdf-ring 20205
[Roman] p. 46Theorem 1.6isldepslvec2 48958
[Roman] p. 112Noteisldepslvec2 48958  ldepsnlinc 48981  zlmodzxznm 48970
[Roman] p. 112Examplezlmodzxzequa 48969  zlmodzxzequap 48972  zlmodzxzldep 48977
[Roman] p. 170Theorem 7.8cayleyhamilton 22864
[Rosenlicht] p. 80Theoremheicant 37987
[Rosser] p. 281Definitiondf-op 4575
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34810
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34811
[Rotman] p. 28Remarkpgrpgt2nabl 48839  pmtr3ncom 19439
[Rotman] p. 31Theorem 3.4symggen2 19435
[Rotman] p. 42Theorem 3.15cayley 19378  cayleyth 19379
[Rudin] p. 164Equation 27efcan 16050
[Rudin] p. 164Equation 30efzval 16058
[Rudin] p. 167Equation 48absefi 16152
[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 6070
[Schechter] p. 51Definition of irreflexivityintirr 6073
[Schechter] p. 51Definition of symmetrycnvsym 6069
[Schechter] p. 51Definition of transitivitycotr 6067
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17537
[Schechter] p. 79Definition of Moore closuredf-mrc 17538
[Schechter] p. 82Section 4.5df-mrc 17538
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17540
[Schechter] p. 139Definition AC3dfac9 10048
[Schechter] p. 141Definition (MC)dfac11 43505
[Schechter] p. 149Axiom DC1ax-dc 10357  axdc3 10365
[Schechter] p. 187Definition of "ring with unit"isring 20207  isrngo 38229
[Schechter] p. 276Remark 11.6.espan0 31633
[Schechter] p. 276Definition of spandf-span 31400  spanval 31424
[Schechter] p. 428Definition 15.35bastop1 22967
[Schloeder] p. 1Lemma 1.3onelon 6340  onelord 43694  ordelon 6339  ordelord 6337
[Schloeder] p. 1Lemma 1.7onepsuc 43695  sucidg 6398
[Schloeder] p. 1Remark 1.50elon 6370  onsuc 7755  ord0 6369  ordsuci 7753
[Schloeder] p. 1Theorem 1.9epsoon 43696
[Schloeder] p. 1Definition 1.1dftr5 5197
[Schloeder] p. 1Definition 1.2dford3 43471  elon2 6326
[Schloeder] p. 1Definition 1.4df-suc 6321
[Schloeder] p. 1Definition 1.6epel 5525  epelg 5523
[Schloeder] p. 1Theorem 1.9(i)elirr 9505  epirron 43697  ordirr 6333
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43699  oneptr 43698  ontr1 6362
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6358  oneptri 43700  ordtri3or 6347
[Schloeder] p. 2Lemma 1.10ondif1 8427  ord0eln0 6371
[Schloeder] p. 2Lemma 1.13elsuci 6384  onsucss 43709  trsucss 6405
[Schloeder] p. 2Lemma 1.14ordsucss 7760
[Schloeder] p. 2Lemma 1.15onnbtwn 6411  ordnbtwn 6410
[Schloeder] p. 2Lemma 1.16orddif0suc 43711  ordnexbtwnsuc 43710
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10312  onsucf1lem 43712  onsucf1o 43715  onsucf1olem 43713  onsucrn 43714
[Schloeder] p. 2Lemma 1.18dflim7 43716
[Schloeder] p. 2Remark 1.12ordzsl 7787
[Schloeder] p. 2Theorem 1.10ondif1i 43705  ordne0gt0 43704
[Schloeder] p. 2Definition 1.11dflim6 43707  limnsuc 43708  onsucelab 43706
[Schloeder] p. 3Remark 1.21omex 9553
[Schloeder] p. 3Theorem 1.19tfinds 7802
[Schloeder] p. 3Theorem 1.22omelon 9556  ordom 7818
[Schloeder] p. 3Definition 1.20dfom3 9557
[Schloeder] p. 4Lemma 2.21onn 8567
[Schloeder] p. 4Lemma 2.7ssonuni 7725  ssorduni 7724
[Schloeder] p. 4Remark 2.4oa1suc 8457
[Schloeder] p. 4Theorem 1.23dfom5 9560  limom 7824
[Schloeder] p. 4Definition 2.1df-1o 8396  df1o2 8403
[Schloeder] p. 4Definition 2.3oa0 8442  oa0suclim 43718  oalim 8458  oasuc 8450
[Schloeder] p. 4Definition 2.5om0 8443  om0suclim 43719  omlim 8459  omsuc 8452
[Schloeder] p. 4Definition 2.6oe0 8448  oe0m1 8447  oe0suclim 43720  oelim 8460  oesuc 8453
[Schloeder] p. 5Lemma 2.10onsupuni 43672
[Schloeder] p. 5Lemma 2.11onsupsucismax 43722
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43723
[Schloeder] p. 5Lemma 2.13limexissup 43724  limexissupab 43726  limiun 43725  limuni 6377
[Schloeder] p. 5Lemma 2.14oa0r 8464
[Schloeder] p. 5Lemma 2.15om1 8468  om1om1r 43727  om1r 8469
[Schloeder] p. 5Remark 2.8oacl 8461  oaomoecl 43721  oecl 8463  omcl 8462
[Schloeder] p. 5Definition 2.9onsupintrab 43674
[Schloeder] p. 6Lemma 2.16oe1 8470
[Schloeder] p. 6Lemma 2.17oe1m 8471
[Schloeder] p. 6Lemma 2.18oe0rif 43728
[Schloeder] p. 6Theorem 2.19oasubex 43729
[Schloeder] p. 6Theorem 2.20nnacl 8538  nnamecl 43730  nnecl 8540  nnmcl 8539
[Schloeder] p. 7Lemma 3.1onsucwordi 43731
[Schloeder] p. 7Lemma 3.2oaword1 8478
[Schloeder] p. 7Lemma 3.3oaword2 8479
[Schloeder] p. 7Lemma 3.4oalimcl 8486
[Schloeder] p. 7Lemma 3.5oaltublim 43733
[Schloeder] p. 8Lemma 3.6oaordi3 43734
[Schloeder] p. 8Lemma 3.81oaomeqom 43736
[Schloeder] p. 8Lemma 3.10oa00 8485
[Schloeder] p. 8Lemma 3.11omge1 43740  omword1 8499
[Schloeder] p. 8Remark 3.9oaordnr 43739  oaordnrex 43738
[Schloeder] p. 8Theorem 3.7oaord3 43735
[Schloeder] p. 9Lemma 3.12omge2 43741  omword2 8500
[Schloeder] p. 9Lemma 3.13omlim2 43742
[Schloeder] p. 9Lemma 3.14omord2lim 43743
[Schloeder] p. 9Lemma 3.15omord2i 43744  omordi 8492
[Schloeder] p. 9Theorem 3.16omord 8494  omord2com 43745
[Schloeder] p. 10Lemma 3.172omomeqom 43746  df-2o 8397
[Schloeder] p. 10Lemma 3.19oege1 43749  oewordi 8518
[Schloeder] p. 10Lemma 3.20oege2 43750  oeworde 8520
[Schloeder] p. 10Lemma 3.21rp-oelim2 43751
[Schloeder] p. 10Lemma 3.22oeord2lim 43752
[Schloeder] p. 10Remark 3.18omnord1 43748  omnord1ex 43747
[Schloeder] p. 11Lemma 3.23oeord2i 43753
[Schloeder] p. 11Lemma 3.25nnoeomeqom 43755
[Schloeder] p. 11Remark 3.26oenord1 43759  oenord1ex 43758
[Schloeder] p. 11Theorem 4.1oaomoencom 43760
[Schloeder] p. 11Theorem 4.2oaass 8487
[Schloeder] p. 11Theorem 3.24oeord2com 43754
[Schloeder] p. 12Theorem 4.3odi 8505
[Schloeder] p. 13Theorem 4.4omass 8506
[Schloeder] p. 14Remark 4.6oenass 43762
[Schloeder] p. 14Theorem 4.7oeoa 8524
[Schloeder] p. 15Lemma 5.1cantnftermord 43763
[Schloeder] p. 15Lemma 5.2cantnfub 43764  cantnfub2 43765
[Schloeder] p. 16Theorem 5.3cantnf2 43768
[Schwabhauser] p. 10Axiom A1axcgrrflx 29002  axtgcgrrflx 28549
[Schwabhauser] p. 10Axiom A2axcgrtr 29003
[Schwabhauser] p. 10Axiom A3axcgrid 29004  axtgcgrid 28550
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28535
[Schwabhauser] p. 11Axiom A4axsegcon 29015  axtgsegcon 28551  df-trkgcb 28537
[Schwabhauser] p. 11Axiom A5ax5seg 29026  axtg5seg 28552  df-trkgcb 28537
[Schwabhauser] p. 11Axiom A6axbtwnid 29027  axtgbtwnid 28553  df-trkgb 28536
[Schwabhauser] p. 12Axiom A7axpasch 29029  axtgpasch 28554  df-trkgb 28536
[Schwabhauser] p. 12Axiom A8axlowdim2 29048  df-trkg2d 34830
[Schwabhauser] p. 13Axiom A8axtglowdim2 28557
[Schwabhauser] p. 13Axiom A9axtgupdim2 28558  df-trkg2d 34830
[Schwabhauser] p. 13Axiom A10axeuclid 29051  axtgeucl 28559  df-trkge 28538
[Schwabhauser] p. 13Axiom A11axcont 29064  axtgcont 28556  axtgcont1 28555  df-trkgb 28536
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36190
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36192
[Schwabhauser] p. 27Theorem 2.3cgrtr 36195
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36199
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36200  tgcgrcomimp 28564  tgcgrcoml 28566  tgcgrcomr 28565
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36205  tgcgrtriv 28571
[Schwabhauser] p. 28Theorem 2.105segofs 36209  tg5segofs 34838
[Schwabhauser] p. 28Definition 2.10df-afs 34835  df-ofs 36186
[Schwabhauser] p. 29Theorem 2.11cgrextend 36211  tgcgrextend 28572
[Schwabhauser] p. 29Theorem 2.12segconeq 36213  tgsegconeq 28573
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36225  btwntriv2 36215  tgbtwntriv2 28574
[Schwabhauser] p. 30Theorem 3.2btwncomim 36216  tgbtwncom 28575
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36219  tgbtwntriv1 28578
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36220  tgbtwnswapid 28579
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36226  btwnintr 36222  tgbtwnexch2 28583  tgbtwnintr 28580
[Schwabhauser] p. 30Theorem 3.6btwnexch 36228  btwnexch3 36223  tgbtwnexch 28585  tgbtwnexch3 28581
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36227  tgbtwnouttr 28584  tgbtwnouttr2 28582
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29047
[Schwabhauser] p. 32Theorem 3.14btwndiff 36230  tgbtwndiff 28593
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28586  trisegint 36231
[Schwabhauser] p. 34Theorem 4.2ifscgr 36247  tgifscgr 28595
[Schwabhauser] p. 34Theorem 4.11colcom 28645  colrot1 28646  colrot2 28647  lncom 28709  lnrot1 28710  lnrot2 28711
[Schwabhauser] p. 34Definition 4.1df-ifs 36243
[Schwabhauser] p. 35Theorem 4.3cgrsub 36248  tgcgrsub 28596
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36258  tgcgrxfr 28605
[Schwabhauser] p. 35Statement 4.4ercgrg 28604
[Schwabhauser] p. 35Definition 4.4df-cgr3 36244  df-cgrg 28598
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28598
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36259  tgbtwnxfr 28617
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36265  colinearperm2 36267  colinearperm3 36266  colinearperm4 36268  colinearperm5 36269
[Schwabhauser] p. 36Definition 4.8df-ismt 28620
[Schwabhauser] p. 36Definition 4.10df-colinear 36242  tgellng 28640  tglng 28633
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36270
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36278  lnxfr 28653
[Schwabhauser] p. 37Theorem 4.14lineext 36279  lnext 28654
[Schwabhauser] p. 37Theorem 4.16fscgr 36283  tgfscgr 28655
[Schwabhauser] p. 37Theorem 4.17linecgr 36284  lncgr 28656
[Schwabhauser] p. 37Definition 4.15df-fs 36245
[Schwabhauser] p. 38Theorem 4.18lineid 36286  lnid 28657
[Schwabhauser] p. 38Theorem 4.19idinside 36287  tgidinside 28658
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36304  tgbtwnconn1 28662
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36305  tgbtwnconn2 28663
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36306  tgbtwnconn3 28664
[Schwabhauser] p. 41Theorem 5.5brsegle2 36312
[Schwabhauser] p. 41Definition 5.4df-segle 36310  legov 28672
[Schwabhauser] p. 41Definition 5.5legov2 28673
[Schwabhauser] p. 42Remark 5.13legso 28686
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36313
[Schwabhauser] p. 42Theorem 5.7seglerflx 36315
[Schwabhauser] p. 42Theorem 5.8segletr 36317
[Schwabhauser] p. 42Theorem 5.9segleantisym 36318
[Schwabhauser] p. 42Theorem 5.10seglelin 36319
[Schwabhauser] p. 42Theorem 5.11seglemin 36316
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36321
[Schwabhauser] p. 42Proposition 5.7legid 28674
[Schwabhauser] p. 42Proposition 5.8legtrd 28676
[Schwabhauser] p. 42Proposition 5.9legtri3 28677
[Schwabhauser] p. 42Proposition 5.10legtrid 28678
[Schwabhauser] p. 42Proposition 5.11leg0 28679
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36328
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36329
[Schwabhauser] p. 43Theorem 6.4broutsideof 36324  df-outsideof 36323
[Schwabhauser] p. 43Definition 6.1broutsideof2 36325  ishlg 28689
[Schwabhauser] p. 44Theorem 6.4hlln 28694
[Schwabhauser] p. 44Theorem 6.5hlid 28696  outsideofrflx 36330
[Schwabhauser] p. 44Theorem 6.6hlcomb 28690  hlcomd 28691  outsideofcom 36331
[Schwabhauser] p. 44Theorem 6.7hltr 28697  outsideoftr 36332
[Schwabhauser] p. 44Theorem 6.11hlcgreu 28705  outsideofeu 36334
[Schwabhauser] p. 44Definition 6.8df-ray 36341
[Schwabhauser] p. 45Part 2df-lines2 36342
[Schwabhauser] p. 45Theorem 6.13outsidele 36335
[Schwabhauser] p. 45Theorem 6.15lineunray 36350
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36351  tglineelsb2 28719
[Schwabhauser] p. 45Theorem 6.17linecom 36353  linerflx1 36352  linerflx2 36354  tglinecom 28722  tglinerflx1 28720  tglinerflx2 28721
[Schwabhauser] p. 45Theorem 6.18linethru 36356  tglinethru 28723
[Schwabhauser] p. 45Definition 6.14df-line2 36340  tglng 28633
[Schwabhauser] p. 45Proposition 6.13legbtwn 28681
[Schwabhauser] p. 46Theorem 6.19linethrueu 36359  tglinethrueu 28726
[Schwabhauser] p. 46Theorem 6.21lineintmo 36360  tglineineq 28730  tglineinteq 28732  tglineintmo 28729
[Schwabhauser] p. 46Theorem 6.23colline 28736
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28737
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28738
[Schwabhauser] p. 49Theorem 7.3mirinv 28753
[Schwabhauser] p. 49Theorem 7.7mirmir 28749
[Schwabhauser] p. 49Theorem 7.8mirreu3 28741
[Schwabhauser] p. 49Definition 7.5df-mir 28740  ismir 28746  mirbtwn 28745  mircgr 28744  mirfv 28743  mirval 28742
[Schwabhauser] p. 50Theorem 7.8mirreu 28751
[Schwabhauser] p. 50Theorem 7.9mireq 28752
[Schwabhauser] p. 50Theorem 7.10mirinv 28753
[Schwabhauser] p. 50Theorem 7.11mirf1o 28756
[Schwabhauser] p. 50Theorem 7.13miriso 28757
[Schwabhauser] p. 51Theorem 7.14mirmot 28762
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28759  mirbtwni 28758
[Schwabhauser] p. 51Theorem 7.16mircgrs 28760
[Schwabhauser] p. 51Theorem 7.17miduniq 28772
[Schwabhauser] p. 52Lemma 7.21symquadlem 28776
[Schwabhauser] p. 52Theorem 7.18miduniq1 28773
[Schwabhauser] p. 52Theorem 7.19miduniq2 28774
[Schwabhauser] p. 52Theorem 7.20colmid 28775
[Schwabhauser] p. 53Lemma 7.22krippen 28778
[Schwabhauser] p. 55Lemma 7.25midexlem 28779
[Schwabhauser] p. 57Theorem 8.2ragcom 28785
[Schwabhauser] p. 57Definition 8.1df-rag 28781  israg 28784
[Schwabhauser] p. 58Theorem 8.3ragcol 28786
[Schwabhauser] p. 58Theorem 8.4ragmir 28787
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28789
[Schwabhauser] p. 58Theorem 8.6ragflat2 28790
[Schwabhauser] p. 58Theorem 8.7ragflat 28791
[Schwabhauser] p. 58Theorem 8.8ragtriva 28792
[Schwabhauser] p. 58Theorem 8.9ragflat3 28793  ragncol 28796
[Schwabhauser] p. 58Theorem 8.10ragcgr 28794
[Schwabhauser] p. 59Theorem 8.12perpcom 28800
[Schwabhauser] p. 59Theorem 8.13ragperp 28804
[Schwabhauser] p. 59Theorem 8.14perpneq 28801
[Schwabhauser] p. 59Definition 8.11df-perpg 28783  isperp 28799
[Schwabhauser] p. 59Definition 8.13isperp2 28802
[Schwabhauser] p. 60Theorem 8.18foot 28809
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28817  colperpexlem2 28818
[Schwabhauser] p. 63Theorem 8.21colperpex 28820  colperpexlem3 28819
[Schwabhauser] p. 64Theorem 8.22mideu 28825  midex 28824
[Schwabhauser] p. 66Lemma 8.24opphllem 28822
[Schwabhauser] p. 67Theorem 9.2oppcom 28831
[Schwabhauser] p. 67Definition 9.1islnopp 28826
[Schwabhauser] p. 68Lemma 9.3opphllem2 28835
[Schwabhauser] p. 68Lemma 9.4opphllem5 28838  opphllem6 28839
[Schwabhauser] p. 69Theorem 9.5opphl 28841
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28554
[Schwabhauser] p. 70Theorem 9.6outpasch 28842
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 28850
[Schwabhauser] p. 71Definition 9.7df-hpg 28845  hpgbr 28847
[Schwabhauser] p. 72Lemma 9.10hpgerlem 28852
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 28851
[Schwabhauser] p. 72Theorem 9.11hpgid 28853
[Schwabhauser] p. 72Theorem 9.12hpgcom 28854
[Schwabhauser] p. 72Theorem 9.13hpgtr 28855
[Schwabhauser] p. 73Theorem 9.18colopp 28856
[Schwabhauser] p. 73Theorem 9.19colhp 28857
[Schwabhauser] p. 88Theorem 10.2lmieu 28871
[Schwabhauser] p. 88Definition 10.1df-mid 28861
[Schwabhauser] p. 89Theorem 10.4lmicom 28875
[Schwabhauser] p. 89Theorem 10.5lmilmi 28876
[Schwabhauser] p. 89Theorem 10.6lmireu 28877
[Schwabhauser] p. 89Theorem 10.7lmieq 28878
[Schwabhauser] p. 89Theorem 10.8lmiinv 28879
[Schwabhauser] p. 89Theorem 10.9lmif1o 28882
[Schwabhauser] p. 89Theorem 10.10lmiiso 28884
[Schwabhauser] p. 89Definition 10.3df-lmi 28862
[Schwabhauser] p. 90Theorem 10.11lmimot 28885
[Schwabhauser] p. 91Theorem 10.12hypcgr 28888
[Schwabhauser] p. 92Theorem 10.14lmiopp 28889
[Schwabhauser] p. 92Theorem 10.15lnperpex 28890
[Schwabhauser] p. 92Theorem 10.16trgcopy 28891  trgcopyeu 28893
[Schwabhauser] p. 95Definition 11.2dfcgra2 28917
[Schwabhauser] p. 95Definition 11.3iscgra 28896
[Schwabhauser] p. 95Proposition 11.4cgracgr 28905
[Schwabhauser] p. 95Proposition 11.10cgrahl1 28903  cgrahl2 28904
[Schwabhauser] p. 96Theorem 11.6cgraid 28906
[Schwabhauser] p. 96Theorem 11.9cgraswap 28907
[Schwabhauser] p. 97Theorem 11.7cgracom 28909
[Schwabhauser] p. 97Theorem 11.8cgratr 28910
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 28913  cgrahl 28914
[Schwabhauser] p. 98Theorem 11.13sacgr 28918
[Schwabhauser] p. 98Theorem 11.14oacgr 28919
[Schwabhauser] p. 98Theorem 11.15acopy 28920  acopyeu 28921
[Schwabhauser] p. 101Theorem 11.24inagswap 28928
[Schwabhauser] p. 101Theorem 11.25inaghl 28932
[Schwabhauser] p. 101Definition 11.23isinag 28925
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 28940
[Schwabhauser] p. 102Definition 11.27df-leag 28933  isleag 28934
[Schwabhauser] p. 107Theorem 11.49tgsas 28942  tgsas1 28941  tgsas2 28943  tgsas3 28944
[Schwabhauser] p. 108Theorem 11.50tgasa 28946  tgasa1 28945
[Schwabhauser] p. 109Theorem 11.51tgsss1 28947  tgsss2 28948  tgsss3 28949
[Shapiro] p. 230Theorem 6.5.1dchrhash 27253  dchrsum 27251  dchrsum2 27250  sumdchr 27254
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27255  sum2dchr 27256
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20032  ablfacrp2 20033
[Shapiro], p. 328Equation 9.2.4vmasum 27198
[Shapiro], p. 329Equation 9.2.7logfac2 27199
[Shapiro], p. 329Equation 9.2.9logfacrlim 27206
[Shapiro], p. 331Equation 9.2.13vmadivsum 27464
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27467
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27521  vmalogdivsum2 27520
[Shapiro], p. 375Theorem 9.4.1dirith 27511  dirith2 27510
[Shapiro], p. 375Equation 9.4.3rplogsum 27509  rpvmasum 27508  rpvmasum2 27494
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27469
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27507
[Shapiro], p. 377Lemma 9.4.1dchrisum 27474  dchrisumlem1 27471  dchrisumlem2 27472  dchrisumlem3 27473  dchrisumlema 27470
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27477
[Shapiro], p. 379Equation 9.4.16dchrmusum 27506  dchrmusumlem 27504  dchrvmasumlem 27505
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27476
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27478
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27502  dchrisum0re 27495  dchrisumn0 27503
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27488
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27492
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27493
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27548  pntrsumbnd2 27549  pntrsumo1 27547
[Shapiro], p. 405Equation 10.2.1mudivsum 27512
[Shapiro], p. 406Equation 10.2.6mulogsum 27514
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27516
[Shapiro], p. 407Equation 10.2.8mulog2sum 27519
[Shapiro], p. 418Equation 10.4.6logsqvma 27524
[Shapiro], p. 418Equation 10.4.8logsqvma2 27525
[Shapiro], p. 419Equation 10.4.10selberg 27530
[Shapiro], p. 420Equation 10.4.12selberg2lem 27532
[Shapiro], p. 420Equation 10.4.14selberg2 27533
[Shapiro], p. 422Equation 10.6.7selberg3 27541
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27542
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27539  selberg3lem2 27540
[Shapiro], p. 422Equation 10.4.23selberg4 27543
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27537
[Shapiro], p. 428Equation 10.6.2selbergr 27550
[Shapiro], p. 429Equation 10.6.8selberg3r 27551
[Shapiro], p. 430Equation 10.6.11selberg4r 27552
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27566
[Shapiro], p. 434Equation 10.6.27pntlema 27578  pntlemb 27579  pntlemc 27577  pntlemd 27576  pntlemg 27580
[Shapiro], p. 435Equation 10.6.29pntlema 27578
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27570
[Shapiro], p. 436Lemma 10.6.2pntibnd 27575
[Shapiro], p. 436Equation 10.6.34pntlema 27578
[Shapiro], p. 436Equation 10.6.35pntlem3 27591  pntleml 27593
[Stewart] p. 91Lemma 7.3constrss 33908
[Stewart] p. 92Definition 7.4.df-constr 33895
[Stewart] p. 96Theorem 7.10constraddcl 33927  constrinvcl 33938  constrmulcl 33936  constrnegcl 33928  constrsqrtcl 33944
[Stewart] p. 97Theorem 7.11constrextdg2 33914
[Stewart] p. 98Theorem 7.12constrext2chn 33924
[Stewart] p. 99Theorem 7.132sqr3nconstr 33946
[Stewart] p. 99Theorem 7.14cos9thpinconstr 33956
[Stoll] p. 13Definition corresponds to dfsymdif3 4247
[Stoll] p. 16Exercise 4.40dif 4346  dif0 4319
[Stoll] p. 16Exercise 4.8difdifdir 4432
[Stoll] p. 17Theorem 5.1(5)unvdif 4416
[Stoll] p. 19Theorem 5.2(13)undm 4238
[Stoll] p. 19Theorem 5.2(13')indm 4239
[Stoll] p. 20Remarkinvdif 4220
[Stoll] p. 25Definition of ordered tripledf-ot 4577
[Stoll] p. 43Definitionuniiun 5002
[Stoll] p. 44Definitionintiin 5003
[Stoll] p. 45Definitiondf-iin 4937
[Stoll] p. 45Definition indexed uniondf-iun 4936
[Stoll] p. 176Theorem 3.4(27)iman 401
[Stoll] p. 262Example 4.1dfsymdif3 4247
[Strang] p. 242Section 6.3expgrowth 44777
[Suppes] p. 22Theorem 2eq0 4291  eq0f 4288
[Suppes] p. 22Theorem 4eqss 3938  eqssd 3940  eqssi 3939
[Suppes] p. 23Theorem 5ss0 4343  ss0b 4342
[Suppes] p. 23Theorem 6sstr 3931  sstrALT2 45276
[Suppes] p. 23Theorem 7pssirr 4044
[Suppes] p. 23Theorem 8pssn2lp 4045
[Suppes] p. 23Theorem 9psstr 4048
[Suppes] p. 23Theorem 10pssss 4039
[Suppes] p. 25Theorem 12elin 3906  elun 4094
[Suppes] p. 26Theorem 15inidm 4168
[Suppes] p. 26Theorem 16in0 4336
[Suppes] p. 27Theorem 23unidm 4098
[Suppes] p. 27Theorem 24un0 4335
[Suppes] p. 27Theorem 25ssun1 4119
[Suppes] p. 27Theorem 26ssequn1 4127
[Suppes] p. 27Theorem 27unss 4131
[Suppes] p. 27Theorem 28indir 4227
[Suppes] p. 27Theorem 29undir 4228
[Suppes] p. 28Theorem 32difid 4317
[Suppes] p. 29Theorem 33difin 4213
[Suppes] p. 29Theorem 34indif 4221
[Suppes] p. 29Theorem 35undif1 4417
[Suppes] p. 29Theorem 36difun2 4422
[Suppes] p. 29Theorem 37difin0 4415
[Suppes] p. 29Theorem 38disjdif 4413
[Suppes] p. 29Theorem 39difundi 4231
[Suppes] p. 29Theorem 40difindi 4233
[Suppes] p. 30Theorem 41nalset 5248
[Suppes] p. 39Theorem 61uniss 4859
[Suppes] p. 39Theorem 65uniop 5461
[Suppes] p. 41Theorem 70intsn 4927
[Suppes] p. 42Theorem 71intpr 4925  intprg 4924
[Suppes] p. 42Theorem 73op1stb 5417
[Suppes] p. 42Theorem 78intun 4923
[Suppes] p. 44Definition 15(a)dfiun2 4975  dfiun2g 4973
[Suppes] p. 44Definition 15(b)dfiin2 4976
[Suppes] p. 47Theorem 86elpw 4546  elpw2 5269  elpw2g 5268  elpwg 4545  elpwgdedVD 45358
[Suppes] p. 47Theorem 87pwid 4564
[Suppes] p. 47Theorem 89pw0 4756
[Suppes] p. 48Theorem 90pwpw0 4757
[Suppes] p. 52Theorem 101xpss12 5637
[Suppes] p. 52Theorem 102xpindi 5780  xpindir 5781
[Suppes] p. 52Theorem 103xpundi 5691  xpundir 5692
[Suppes] p. 54Theorem 105elirrv 9503
[Suppes] p. 58Theorem 2relss 5729
[Suppes] p. 59Theorem 4eldm 5847  eldm2 5848  eldm2g 5846  eldmg 5845
[Suppes] p. 59Definition 3df-dm 5632
[Suppes] p. 60Theorem 6dmin 5858
[Suppes] p. 60Theorem 8rnun 6101
[Suppes] p. 60Theorem 9rnin 6102
[Suppes] p. 60Definition 4dfrn2 5835
[Suppes] p. 61Theorem 11brcnv 5829  brcnvg 5826
[Suppes] p. 62Equation 5elcnv 5823  elcnv2 5824
[Suppes] p. 62Theorem 12relcnv 6061
[Suppes] p. 62Theorem 15cnvin 6100
[Suppes] p. 62Theorem 16cnvun 6098
[Suppes] p. 63Definitiondftrrels2 38991
[Suppes] p. 63Theorem 20co02 6217
[Suppes] p. 63Theorem 21dmcoss 5922
[Suppes] p. 63Definition 7df-co 5631
[Suppes] p. 64Theorem 26cnvco 5832
[Suppes] p. 64Theorem 27coass 6222
[Suppes] p. 65Theorem 31resundi 5950
[Suppes] p. 65Theorem 34elima 6022  elima2 6023  elima3 6024  elimag 6021
[Suppes] p. 65Theorem 35imaundi 6105
[Suppes] p. 66Theorem 40dminss 6109
[Suppes] p. 66Theorem 41imainss 6110
[Suppes] p. 67Exercise 11cnvxp 6113
[Suppes] p. 81Definition 34dfec2 8637
[Suppes] p. 82Theorem 72elec 8681  elecALTV 38603  elecg 8679
[Suppes] p. 82Theorem 73eqvrelth 39027  erth 8689  erth2 8690
[Suppes] p. 83Theorem 74eqvreldisj 39030  erdisj 8692
[Suppes] p. 83Definition 35, df-parts 39200  dfmembpart2 39205
[Suppes] p. 89Theorem 96map0b 8822
[Suppes] p. 89Theorem 97map0 8826  map0g 8823
[Suppes] p. 89Theorem 98mapsn 8827  mapsnd 8825
[Suppes] p. 89Theorem 99mapss 8828
[Suppes] p. 91Definition 12(ii)alephsuc 9979
[Suppes] p. 91Definition 12(iii)alephlim 9978
[Suppes] p. 92Theorem 1enref 8923  enrefg 8922
[Suppes] p. 92Theorem 2ensym 8941  ensymb 8940  ensymi 8942
[Suppes] p. 92Theorem 3entr 8944
[Suppes] p. 92Theorem 4unen 8983
[Suppes] p. 94Theorem 15endom 8917
[Suppes] p. 94Theorem 16ssdomg 8938
[Suppes] p. 94Theorem 17domtr 8945
[Suppes] p. 95Theorem 18sbth 9026
[Suppes] p. 97Theorem 23canth2 9059  canth2g 9060
[Suppes] p. 97Definition 3brsdom2 9030  df-sdom 8887  dfsdom2 9029
[Suppes] p. 97Theorem 21(i)sdomirr 9043
[Suppes] p. 97Theorem 22(i)domnsym 9032
[Suppes] p. 97Theorem 21(ii)sdomnsym 9031
[Suppes] p. 97Theorem 22(ii)domsdomtr 9041
[Suppes] p. 97Theorem 22(iv)brdom2 8920
[Suppes] p. 97Theorem 21(iii)sdomtr 9044
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9039
[Suppes] p. 98Exercise 4fundmen 8969  fundmeng 8970
[Suppes] p. 98Exercise 6xpdom3 9004
[Suppes] p. 98Exercise 11sdomentr 9040
[Suppes] p. 104Theorem 37fofi 9214
[Suppes] p. 104Theorem 38pwfi 9220
[Suppes] p. 105Theorem 40pwfi 9220
[Suppes] p. 111Axiom for cardinal numberscarden 10462
[Suppes] p. 130Definition 3df-tr 5194
[Suppes] p. 132Theorem 9ssonuni 7725
[Suppes] p. 134Definition 6df-suc 6321
[Suppes] p. 136Theorem Schema 22findes 7842  finds 7838  finds1 7841  finds2 7840
[Suppes] p. 151Theorem 42isfinite 9562  isfinite2 9199  isfiniteg 9201  unbnn 9197
[Suppes] p. 162Definition 5df-ltnq 10830  df-ltpq 10822
[Suppes] p. 197Theorem Schema 4tfindes 7805  tfinds 7802  tfinds2 7806
[Suppes] p. 209Theorem 18oaord1 8477
[Suppes] p. 209Theorem 21oaword2 8479
[Suppes] p. 211Theorem 25oaass 8487
[Suppes] p. 225Definition 8iscard2 9889
[Suppes] p. 227Theorem 56ondomon 10474
[Suppes] p. 228Theorem 59harcard 9891
[Suppes] p. 228Definition 12(i)aleph0 9977
[Suppes] p. 228Theorem Schema 61onintss 6367
[Suppes] p. 228Theorem Schema 62onminesb 7738  onminsb 7739
[Suppes] p. 229Theorem 64alephval2 10484
[Suppes] p. 229Theorem 65alephcard 9981
[Suppes] p. 229Theorem 66alephord2i 9988
[Suppes] p. 229Theorem 67alephnbtwn 9982
[Suppes] p. 229Definition 12df-aleph 9853
[Suppes] p. 242Theorem 6weth 10406
[Suppes] p. 242Theorem 8entric 10468
[Suppes] p. 242Theorem 9carden 10462
[Szendrei] p. 11Line 6df-cloneop 35899
[Szendrei] p. 11Paragraph 3df-suppos 35903
[TakeutiZaring] p. 8Axiom 1ax-ext 2709
[TakeutiZaring] p. 13Definition 4.5df-cleq 2729  wl-df.cleq 37835
[TakeutiZaring] p. 13Proposition 4.6df-clel 2812  wl-df.clel 37838
[TakeutiZaring] p. 13Proposition 4.9cvjust 2731
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2757
[TakeutiZaring] p. 14Definition 4.16df-oprab 7362
[TakeutiZaring] p. 14Proposition 4.14ru 3727
[TakeutiZaring] p. 15Axiom 2zfpair 5356
[TakeutiZaring] p. 15Exercise 1elpr 4593  elpr2 4595  elpr2g 4594  elprg 4591
[TakeutiZaring] p. 15Exercise 2elsn 4583  elsn2 4610  elsn2g 4609  elsng 4582  velsn 4584
[TakeutiZaring] p. 15Exercise 3elop 5413
[TakeutiZaring] p. 15Exercise 4sneq 4578  sneqr 4784
[TakeutiZaring] p. 15Definition 5.1dfpr2 4589  dfsn2 4581  dfsn2ALT 4590
[TakeutiZaring] p. 16Axiom 3uniex 7686
[TakeutiZaring] p. 16Exercise 6opth 5422
[TakeutiZaring] p. 16Exercise 7opex 5409
[TakeutiZaring] p. 16Exercise 8rext 5393
[TakeutiZaring] p. 16Corollary 5.8unex 7689  unexg 7688
[TakeutiZaring] p. 16Definition 5.3dftp2 4636
[TakeutiZaring] p. 16Definition 5.5df-uni 4852
[TakeutiZaring] p. 16Definition 5.6df-in 3897  df-un 3895
[TakeutiZaring] p. 16Proposition 5.7unipr 4868  uniprg 4867
[TakeutiZaring] p. 17Axiom 4vpwex 5312
[TakeutiZaring] p. 17Exercise 1eltp 4634
[TakeutiZaring] p. 17Exercise 5elsuc 6387  elsucg 6385  sstr2 3929
[TakeutiZaring] p. 17Exercise 6uncom 4099
[TakeutiZaring] p. 17Exercise 7incom 4150
[TakeutiZaring] p. 17Exercise 8unass 4113
[TakeutiZaring] p. 17Exercise 9inass 4169
[TakeutiZaring] p. 17Exercise 10indi 4225
[TakeutiZaring] p. 17Exercise 11undi 4226
[TakeutiZaring] p. 17Definition 5.9df-pss 3910  df-ss 3907
[TakeutiZaring] p. 17Definition 5.10df-pw 4544
[TakeutiZaring] p. 18Exercise 7unss2 4128
[TakeutiZaring] p. 18Exercise 9dfss2 3908  sseqin2 4164
[TakeutiZaring] p. 18Exercise 10ssid 3945
[TakeutiZaring] p. 18Exercise 12inss1 4178  inss2 4179
[TakeutiZaring] p. 18Exercise 13nss 3987
[TakeutiZaring] p. 18Exercise 15unieq 4862
[TakeutiZaring] p. 18Exercise 18sspwb 5394  sspwimp 45359  sspwimpALT 45366  sspwimpALT2 45369  sspwimpcf 45361
[TakeutiZaring] p. 18Exercise 19pweqb 5401
[TakeutiZaring] p. 19Axiom 5ax-rep 5212
[TakeutiZaring] p. 20Definitiondf-rab 3391
[TakeutiZaring] p. 20Corollary 5.160ex 5242
[TakeutiZaring] p. 20Definition 5.12df-dif 3893
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 36848  dfnul2 4277
[TakeutiZaring] p. 20Proposition 5.15difid 4317
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4294  n0f 4290  neq0 4293  neq0f 4289
[TakeutiZaring] p. 21Axiom 6zfreg 9502
[TakeutiZaring] p. 21Axiom 6'zfregs 9642
[TakeutiZaring] p. 21Theorem 5.22setind 9657
[TakeutiZaring] p. 21Definition 5.20df-v 3432
[TakeutiZaring] p. 21Proposition 5.21vprc 5250
[TakeutiZaring] p. 22Exercise 10ss 4341
[TakeutiZaring] p. 22Exercise 3ssex 5256  ssexg 5258
[TakeutiZaring] p. 22Exercise 4inex1 5252
[TakeutiZaring] p. 22Exercise 5ruv 9511
[TakeutiZaring] p. 22Exercise 6elirr 9505
[TakeutiZaring] p. 22Exercise 7ssdif0 4307
[TakeutiZaring] p. 22Exercise 11difdif 4076
[TakeutiZaring] p. 22Exercise 13undif3 4241  undif3VD 45323
[TakeutiZaring] p. 22Exercise 14difss 4077
[TakeutiZaring] p. 22Exercise 15sscon 4084
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3053
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3063
[TakeutiZaring] p. 23Proposition 6.2xpex 7698  xpexg 7695
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5629
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6561
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6737  fun11 6564
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6503  svrelfun 6562
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5834
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5836
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5634
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5635
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5631
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6150  dfrel2 6145
[TakeutiZaring] p. 25Exercise 3xpss 5638
[TakeutiZaring] p. 25Exercise 5relun 5758
[TakeutiZaring] p. 25Exercise 6reluni 5765
[TakeutiZaring] p. 25Exercise 9inxp 5778
[TakeutiZaring] p. 25Exercise 12relres 5962
[TakeutiZaring] p. 25Exercise 13opelres 5942  opelresi 5944
[TakeutiZaring] p. 25Exercise 14dmres 5969
[TakeutiZaring] p. 25Exercise 15resss 5958
[TakeutiZaring] p. 25Exercise 17resabs1 5963
[TakeutiZaring] p. 25Exercise 18funres 6532
[TakeutiZaring] p. 25Exercise 24relco 6065
[TakeutiZaring] p. 25Exercise 29funco 6530
[TakeutiZaring] p. 25Exercise 30f1co 6739
[TakeutiZaring] p. 26Definition 6.10eu2 2610
[TakeutiZaring] p. 26Definition 6.11conventions 30490  df-fv 6498  fv3 6850
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7867  cnvexg 7866
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7851  dmexg 7843
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7852  rnexg 7844
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 44895
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7862
[TakeutiZaring] p. 27Corollary 6.13fvex 6845
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47619  tz6.12-1-afv2 47686  tz6.12-1 6855  tz6.12-afv 47618  tz6.12-afv2 47685  tz6.12 6856  tz6.12c-afv2 47687  tz6.12c 6854
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47682  tz6.12-2 6819  tz6.12i-afv2 47688  tz6.12i 6858
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6493
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6494
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6496  wfo 6488
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6495  wf1 6487
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6497  wf1o 6489
[TakeutiZaring] p. 28Exercise 4eqfnfv 6975  eqfnfv2 6976  eqfnfv2f 6979
[TakeutiZaring] p. 28Exercise 5fvco 6930
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7163
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7161
[TakeutiZaring] p. 29Exercise 9funimaex 6578  funimaexg 6577
[TakeutiZaring] p. 29Definition 6.18df-br 5087
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5531
[TakeutiZaring] p. 30Definition 6.21dffr2 5583  dffr3 6056  eliniseg 6051  iniseg 6054
[TakeutiZaring] p. 30Definition 6.22df-eprel 5522
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5599  fr3nr 7717  frirr 5598
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5575
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7719
[TakeutiZaring] p. 31Exercise 1frss 5586
[TakeutiZaring] p. 31Exercise 4wess 5608
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6303  tz6.26i 6304  wefrc 5616  wereu2 5619
[TakeutiZaring] p. 32Theorem 6.27wfi 6305  wfii 6306
[TakeutiZaring] p. 32Definition 6.28df-isom 6499
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7275
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7276
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7282
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7283
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7284
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7288
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7295
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7297
[TakeutiZaring] p. 35Notationwtr 5193
[TakeutiZaring] p. 35Theorem 7.2trelpss 44896  tz7.2 5605
[TakeutiZaring] p. 35Definition 7.1dftr3 5198
[TakeutiZaring] p. 36Proposition 7.4ordwe 6328
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6336
[TakeutiZaring] p. 36Proposition 7.6ordelord 6337  ordelordALT 44979  ordelordALTVD 45308
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6343  ordelssne 6342
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6341
[TakeutiZaring] p. 37Proposition 7.9ordin 6345
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7727
[TakeutiZaring] p. 38Corollary 7.15ordsson 7728
[TakeutiZaring] p. 38Definition 7.11df-on 6319
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6347
[TakeutiZaring] p. 38Proposition 7.12onfrALT 44991  ordon 7722
[TakeutiZaring] p. 38Proposition 7.13onprc 7723
[TakeutiZaring] p. 39Theorem 7.17tfi 7795
[TakeutiZaring] p. 40Exercise 3ontr2 6363
[TakeutiZaring] p. 40Exercise 7dftr2 5195
[TakeutiZaring] p. 40Exercise 9onssmin 7737
[TakeutiZaring] p. 40Exercise 11unon 7773
[TakeutiZaring] p. 40Exercise 12ordun 6421
[TakeutiZaring] p. 40Exercise 14ordequn 6420
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7724
[TakeutiZaring] p. 40Proposition 7.20elssuni 4882
[TakeutiZaring] p. 41Definition 7.22df-suc 6321
[TakeutiZaring] p. 41Proposition 7.23sssucid 6397  sucidg 6398
[TakeutiZaring] p. 41Proposition 7.24onsuc 7755
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6411  ordnbtwn 6410
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7770
[TakeutiZaring] p. 42Exercise 1df-lim 6320
[TakeutiZaring] p. 42Exercise 4omssnlim 7823
[TakeutiZaring] p. 42Exercise 7ssnlim 7828
[TakeutiZaring] p. 42Exercise 8onsucssi 7783  ordelsuc 7762
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7764
[TakeutiZaring] p. 42Definition 7.27nlimon 7793
[TakeutiZaring] p. 42Definition 7.28dfom2 7810
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7831
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7832
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7833
[TakeutiZaring] p. 43Remarkomon 7820
[TakeutiZaring] p. 43Axiom 7inf3 9545  omex 9553
[TakeutiZaring] p. 43Theorem 7.32ordom 7818
[TakeutiZaring] p. 43Corollary 7.31find 7837
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7834
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7835
[TakeutiZaring] p. 44Exercise 1limomss 7813
[TakeutiZaring] p. 44Exercise 2int0 4905
[TakeutiZaring] p. 44Exercise 3trintss 5211
[TakeutiZaring] p. 44Exercise 4intss1 4906
[TakeutiZaring] p. 44Exercise 5intex 5279
[TakeutiZaring] p. 44Exercise 6oninton 7740
[TakeutiZaring] p. 44Exercise 11ordintdif 6366
[TakeutiZaring] p. 44Definition 7.35df-int 4891
[TakeutiZaring] p. 44Proposition 7.34noinfep 9570
[TakeutiZaring] p. 45Exercise 4onint 7735
[TakeutiZaring] p. 47Lemma 1tfrlem1 8306
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8327
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8328
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8329
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8336  tz7.44-2 8337  tz7.44-3 8338
[TakeutiZaring] p. 50Exercise 1smogt 8298
[TakeutiZaring] p. 50Exercise 3smoiso 8293
[TakeutiZaring] p. 50Definition 7.46df-smo 8277
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8375  tz7.49c 8376
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8373
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8372
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8374
[TakeutiZaring] p. 53Proposition 7.532eu5 2657
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9922
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9923
[TakeutiZaring] p. 56Definition 8.1oalim 8458  oasuc 8450
[TakeutiZaring] p. 57Remarktfindsg 7803
[TakeutiZaring] p. 57Proposition 8.2oacl 8461
[TakeutiZaring] p. 57Proposition 8.3oa0 8442  oa0r 8464
[TakeutiZaring] p. 57Proposition 8.16omcl 8462
[TakeutiZaring] p. 58Corollary 8.5oacan 8474
[TakeutiZaring] p. 58Proposition 8.4nnaord 8546  nnaordi 8545  oaord 8473  oaordi 8472
[TakeutiZaring] p. 59Proposition 8.6iunss2 4993  uniss2 4885
[TakeutiZaring] p. 59Proposition 8.7oawordri 8476
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8481  oawordex 8483
[TakeutiZaring] p. 59Proposition 8.9nnacl 8538
[TakeutiZaring] p. 59Proposition 8.10oaabs 8575
[TakeutiZaring] p. 60Remarkoancom 9561
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8486
[TakeutiZaring] p. 62Exercise 1nnarcl 8543
[TakeutiZaring] p. 62Exercise 5oaword1 8478
[TakeutiZaring] p. 62Definition 8.15om0x 8445  omlim 8459  omsuc 8452
[TakeutiZaring] p. 62Definition 8.15(a)om0 8443
[TakeutiZaring] p. 63Proposition 8.17nnecl 8540  nnmcl 8539
[TakeutiZaring] p. 63Proposition 8.19nnmord 8559  nnmordi 8558  omord 8494  omordi 8492
[TakeutiZaring] p. 63Proposition 8.20omcan 8495
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8563  omwordri 8498
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8465
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8468  om1r 8469
[TakeutiZaring] p. 64Proposition 8.22om00 8501
[TakeutiZaring] p. 64Proposition 8.23omordlim 8503
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8504
[TakeutiZaring] p. 64Proposition 8.25odi 8505
[TakeutiZaring] p. 65Theorem 8.26omass 8506
[TakeutiZaring] p. 67Definition 8.30nnesuc 8535  oe0 8448  oelim 8460  oesuc 8453  onesuc 8456
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8446
[TakeutiZaring] p. 67Proposition 8.32oen0 8513
[TakeutiZaring] p. 67Proposition 8.33oeordi 8514
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8447
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8471
[TakeutiZaring] p. 68Corollary 8.34oeord 8515
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8521
[TakeutiZaring] p. 68Proposition 8.35oewordri 8519
[TakeutiZaring] p. 68Proposition 8.37oeworde 8520
[TakeutiZaring] p. 69Proposition 8.41oeoa 8524
[TakeutiZaring] p. 70Proposition 8.42oeoe 8526
[TakeutiZaring] p. 73Theorem 9.1trcl 9638  tz9.1 9639
[TakeutiZaring] p. 76Definition 9.9df-r1 9677  r10 9681  r1lim 9685  r1limg 9684  r1suc 9683  r1sucg 9682
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9693  r1ord2 9694  r1ordg 9691
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9703
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9728  tz9.13 9704  tz9.13g 9705
[TakeutiZaring] p. 79Definition 9.14df-rank 9678  rankval 9729  rankvalb 9710  rankvalg 9730
[TakeutiZaring] p. 79Proposition 9.16rankel 9752  rankelb 9737
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9766  rankval3 9753  rankval3b 9739
[TakeutiZaring] p. 79Proposition 9.18rankonid 9742
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9708
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9747  rankr1c 9734  rankr1g 9745
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9748
[TakeutiZaring] p. 80Exercise 1rankss 9762  rankssb 9761
[TakeutiZaring] p. 80Exercise 2unbndrank 9755
[TakeutiZaring] p. 80Proposition 9.19bndrank 9754
[TakeutiZaring] p. 83Axiom of Choiceac4 10386  dfac3 10032
[TakeutiZaring] p. 84Theorem 10.3dfac8a 9941  numth 10383  numth2 10382
[TakeutiZaring] p. 85Definition 10.4cardval 10457
[TakeutiZaring] p. 85Proposition 10.5cardid 10458  cardid2 9866
[TakeutiZaring] p. 85Proposition 10.9oncard 9873
[TakeutiZaring] p. 85Proposition 10.10carden 10462
[TakeutiZaring] p. 85Proposition 10.11cardidm 9872
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9857
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9878
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9870
[TakeutiZaring] p. 87Proposition 10.15pwen 9079
[TakeutiZaring] p. 88Exercise 1en0 8956
[TakeutiZaring] p. 88Exercise 7infensuc 9084
[TakeutiZaring] p. 89Exercise 10omxpen 9008
[TakeutiZaring] p. 90Corollary 10.23cardnn 9876
[TakeutiZaring] p. 90Definition 10.27alephiso 10009
[TakeutiZaring] p. 90Proposition 10.20nneneq 9131
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9139
[TakeutiZaring] p. 90Proposition 10.26alephprc 10010
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9136
[TakeutiZaring] p. 91Exercise 2alephle 9999
[TakeutiZaring] p. 91Exercise 3aleph0 9977
[TakeutiZaring] p. 91Exercise 4cardlim 9885
[TakeutiZaring] p. 91Exercise 7infpss 10127
[TakeutiZaring] p. 91Exercise 8infcntss 9224
[TakeutiZaring] p. 91Definition 10.29df-fin 8888  isfi 8913
[TakeutiZaring] p. 92Proposition 10.32onfin 9140
[TakeutiZaring] p. 92Proposition 10.34imadomg 10445
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9001
[TakeutiZaring] p. 93Proposition 10.35fodomb 10437
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10097  unxpdom 9160
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9887  cardsdomelir 9886
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9162
[TakeutiZaring] p. 94Proposition 10.39infxpen 9925
[TakeutiZaring] p. 95Definition 10.42df-map 8766
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10473  infxpidm2 9928
[TakeutiZaring] p. 95Proposition 10.41infdju 10118  infxp 10125
[TakeutiZaring] p. 96Proposition 10.44pw2en 9013  pw2f1o 9011
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9072
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10398
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10393  ac6s5 10402
[TakeutiZaring] p. 98Theorem 10.47unidom 10454
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10455  uniimadomf 10456
[TakeutiZaring] p. 100Definition 11.1cfcof 10185
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10180
[TakeutiZaring] p. 102Exercise 1cfle 10165
[TakeutiZaring] p. 102Exercise 2cf0 10162
[TakeutiZaring] p. 102Exercise 3cfsuc 10168
[TakeutiZaring] p. 102Exercise 4cfom 10175
[TakeutiZaring] p. 102Proposition 11.9coftr 10184
[TakeutiZaring] p. 103Theorem 11.15alephreg 10494
[TakeutiZaring] p. 103Proposition 11.11cardcf 10163
[TakeutiZaring] p. 103Proposition 11.13alephsing 10187
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10008
[TakeutiZaring] p. 104Proposition 11.16carduniima 10007
[TakeutiZaring] p. 104Proposition 11.18alephfp 10019  alephfp2 10020
[TakeutiZaring] p. 106Theorem 11.20gchina 10611
[TakeutiZaring] p. 106Theorem 11.21mappwen 10023
[TakeutiZaring] p. 107Theorem 11.26konigth 10481
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10495
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10496
[Tarski] p. 67Axiom B5ax-c5 39340
[Tarski] p. 67Scheme B5sp 2191
[Tarski] p. 68Lemma 6avril1 30553  equid 2014
[Tarski] p. 69Lemma 7equcomi 2019
[Tarski] p. 70Lemma 14spim 2392  spime 2394  spimew 1973
[Tarski] p. 70Lemma 16ax-12 2185  ax-c15 39346  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 39364
[Tarski], p. 75Scheme B8 of system S2ax-7 2010  ax-8 2116  ax-9 2124
[Tarski1999] p. 178Axiom 4axtgsegcon 28551
[Tarski1999] p. 178Axiom 5axtg5seg 28552
[Tarski1999] p. 179Axiom 7axtgpasch 28554
[Tarski1999] p. 180Axiom 7.1axtgpasch 28554
[Tarski1999] p. 185Axiom 11axtgcont1 28555
[Truss] p. 114Theorem 5.18ruc 16199
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 37991
[Viaclovsky8] p. 3Proposition 7ismblfin 37993
[Weierstrass] p. 272Definitiondf-mdet 22559  mdetuni 22596
[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 37772
[WhiteheadRussell] p. 100Theorem *2.05frege5 44242  imim2 58  wl-luk-imim2 37767
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47464  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 37770
[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 45368  wl-luk-notnotr 37771
[WhiteheadRussell] p. 102Theorem *2.15con1 146
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44272  axfrege28 44271  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 37764
[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 30491  pm2.27 42  wl-luk-pm2.27 37762
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 923
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38703
[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. 145Theorem *10.3bj-alsyl 36899
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 44800
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 44801
[WhiteheadRussell] p. 147Theorem *10.2219.26 1872
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 44802
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 44803
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 44804
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1895
[WhiteheadRussell] p. 151Theorem *10.301albitr 44805
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 44806
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 44807
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 44808
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 44809
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 44811
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 44812
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 44813
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 44810
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2096
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 44816
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 44817
[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 44818
[WhiteheadRussell] p. 162Theorem *11.322alim 44819
[WhiteheadRussell] p. 162Theorem *11.332albi 44820
[WhiteheadRussell] p. 162Theorem *11.342exim 44821
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 44823
[WhiteheadRussell] p. 162Theorem *11.3412exbi 44822
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1889
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 44825
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 44826
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 44824
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1830
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 44827
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 44828
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1848
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 44829
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2351
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1862
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 44834
[WhiteheadRussell] p. 165Theorem *11.56aaanv 44830
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 44831
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 44832
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 44833
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 44838
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 44835
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 44836
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 44837
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 44839
[WhiteheadRussell] p. 175Definition *14.02df-eu 2570
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 44849  pm13.13b 44850
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 44851
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3014
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3015
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3609
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 44857
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 44858
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 44852
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 44994  pm13.193 44853
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 44854
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 44855
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 44856
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 44863
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 44862
[WhiteheadRussell] p. 184Definition *14.01iotasbc 44861
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3792
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 44864  pm14.122b 44865  pm14.122c 44866
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 44867  pm14.123b 44868  pm14.123c 44869
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 44871
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 44870
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 44872
[WhiteheadRussell] p. 190Theorem *14.22iota4 6471
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 44873
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6472
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 44874
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 44876
[WhiteheadRussell] p. 192Theorem *14.26eupick 2634  eupickbi 2637  sbaniota 44877
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 44875
[WhiteheadRussell] p. 192Theorem *14.271eubi 2585
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 44878
[WhiteheadRussell] p. 235Definition *30.01conventions 30490  df-fv 6498
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9914  pm54.43lem 9913
[Young] p. 141Definition of operator orderingleop2 32215
[Young] p. 142Example 12.2(i)0leop 32221  idleop 32222
[vandenDries] p. 42Lemma 61irrapx1 43271
[vandenDries] p. 43Theorem 62pellex 43278  pellexlem1 43272

This page was last updated on 16-Apr-2026.
Copyright terms: Public domain