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 17723
[Adamek] p. 21Condition 3.1(b)df-cat 17723
[Adamek] p. 22Example 3.3(1)df-setc 18132
[Adamek] p. 24Example 3.3(4.c)0cat 17744  0funcg 49830  df-termc 50218
[Adamek] p. 24Example 3.3(4.d)df-prstc 50295  prsthinc 50209
[Adamek] p. 24Example 3.3(4.e)df-mndtc 50323  df-mndtc 50323
[Adamek] p. 24Example 3.3(4)(c)discsnterm 50319
[Adamek] p. 25Definition 3.5df-oppc 17767
[Adamek] p. 25Example 3.6(1)oduoppcciso 50311
[Adamek] p. 25Example 3.6(2)oppgoppcco 50336  oppgoppchom 50335  oppgoppcid 50337
[Adamek] p. 28Remark 3.9oppciso 17837
[Adamek] p. 28Remark 3.12invf1o 17825  invisoinvl 17846
[Adamek] p. 28Example 3.13idinv 17845  idiso 17844
[Adamek] p. 28Corollary 3.11inveq 17830
[Adamek] p. 28Definition 3.8df-inv 17804  df-iso 17805  dfiso2 17828
[Adamek] p. 28Proposition 3.10sectcan 17811
[Adamek] p. 29Remark 3.16cicer 17862  cicerALT 49791
[Adamek] p. 29Definition 3.15cic 17855  df-cic 17852
[Adamek] p. 29Definition 3.17df-func 17914
[Adamek] p. 29Proposition 3.14(1)invinv 17826
[Adamek] p. 29Proposition 3.14(2)invco 17827  isoco 17833
[Adamek] p. 30Remark 3.19df-func 17914
[Adamek] p. 30Example 3.20(1)idfucl 17937
[Adamek] p. 30Example 3.20(2)diag1 50049
[Adamek] p. 32Proposition 3.21funciso 17930
[Adamek] p. 33Example 3.26(1)discsnterm 50319  discthing 50206
[Adamek] p. 33Example 3.26(2)df-thinc 50163  prsthinc 50209  thincciso 50198  thincciso2 50200  thincciso3 50201  thinccisod 50199
[Adamek] p. 33Example 3.26(3)df-mndtc 50323
[Adamek] p. 33Proposition 3.23cofucl 17944  cofucla 49841
[Adamek] p. 34Remark 3.28(1)cofidfth 49907
[Adamek] p. 34Remark 3.28(2)catciso 18167  catcisoi 50145
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 18222
[Adamek] p. 34Definition 3.27(2)df-fth 17963
[Adamek] p. 34Definition 3.27(3)df-full 17962
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 18222
[Adamek] p. 35Corollary 3.32ffthiso 17987
[Adamek] p. 35Proposition 3.30(c)cofth 17993
[Adamek] p. 35Proposition 3.30(d)cofull 17992
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 18207
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 18207
[Adamek] p. 39Remark 3.422oppf 49877
[Adamek] p. 39Definition 3.41df-oppf 49868  funcoppc 17931
[Adamek] p. 39Definition 3.44.df-catc 18155  elcatchom 50142
[Adamek] p. 39Proposition 3.43(c)fthoppc 17981  fthoppf 49909
[Adamek] p. 39Proposition 3.43(d)fulloppc 17980  fulloppf 49908
[Adamek] p. 40Remark 3.48catccat 18164
[Adamek] p. 40Definition 3.470funcg 49830  df-catc 18155
[Adamek] p. 45Exercise 3Gincat 50346
[Adamek] p. 48Remark 4.2(2)cnelsubc 50349  nelsubc3 49816
[Adamek] p. 48Remark 4.2(3)imasubc 49896  imasubc2 49897  imasubc3 49901
[Adamek] p. 48Example 4.3(1.a)0subcat 17894
[Adamek] p. 48Example 4.3(1.b)catsubcat 17895
[Adamek] p. 48Definition 4.1(1)nelsubc3 49816
[Adamek] p. 48Definition 4.1(2)fullsubc 17906
[Adamek] p. 48Definition 4.1(a)df-subc 17868
[Adamek] p. 49Remark 4.4idsubc 49905
[Adamek] p. 49Remark 4.4(1)idemb 49904
[Adamek] p. 49Remark 4.4(2)idfullsubc 49906  ressffth 17996
[Adamek] p. 58Exercise 4Asetc1onsubc 50347
[Adamek] p. 83Definition 6.1df-nat 18002
[Adamek] p. 87Remark 6.14(a)fuccocl 18023
[Adamek] p. 87Remark 6.14(b)fucass 18027
[Adamek] p. 87Definition 6.15df-fuc 18003
[Adamek] p. 88Remark 6.16fuccat 18029
[Adamek] p. 101Definition 7.10funcg 49830  df-inito 18040
[Adamek] p. 101Example 7.2(3)0funcg 49830  df-termc 50218  initc 49836
[Adamek] p. 101Example 7.2 (6)irinitoringc 21608
[Adamek] p. 102Definition 7.4df-termo 18041  oppctermo 49981
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 18068
[Adamek] p. 102Proposition 7.3 (2)initoeu2 18072
[Adamek] p. 103Remark 7.8oppczeroo 49982
[Adamek] p. 103Definition 7.7df-zeroo 18042
[Adamek] p. 103Example 7.9 (3)nzerooringczr 21609
[Adamek] p. 103Proposition 7.6termoeu1w 18075
[Adamek] p. 106Definition 7.19df-sect 17803
[Adamek] p. 107Example 7.20(7)thincinv 50214
[Adamek] p. 108Example 7.25(4)thincsect2 50213
[Adamek] p. 110Example 7.33(9)thincmon 50178
[Adamek] p. 110Proposition 7.35sectmon 17838
[Adamek] p. 112Proposition 7.42sectepi 17840
[Adamek] p. 185Section 10.67updjud 9919
[Adamek] p. 193Definition 11.1(1)df-lmd 50390
[Adamek] p. 193Definition 11.3(1)df-lmd 50390
[Adamek] p. 194Definition 11.3(2)df-lmd 50390
[Adamek] p. 202Definition 11.27(1)df-cmd 50391
[Adamek] p. 202Definition 11.27(2)df-cmd 50391
[Adamek] p. 478Item Rngdf-ringc 20730
[AhoHopUll] p. 2Section 1.1df-bigo 49295
[AhoHopUll] p. 12Section 1.3df-blen 49317
[AhoHopUll] p. 318Section 9.1df-concat 14608  df-pfx 14709  df-substr 14679  df-word 14551  lencl 14570  wrd0 14576
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 24844  df-nmoo 31063
[AkhiezerGlazman] p. 64Theoremhmopidmch 32471  hmopidmchi 32469
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 32519  pjcmul2i 32520
[AkhiezerGlazman] p. 72Theoremcnvunop 32236  unoplin 32238
[AkhiezerGlazman] p. 72Equation 2unopadj 32237  unopadj2 32256
[AkhiezerGlazman] p. 73Theoremelunop2 32331  lnopunii 32330
[AkhiezerGlazman] p. 80Proposition 1adjlnop 32404
[Alling] p. 125Theorem 4.02(12)cofcutrtime 28096
[Alling] p. 184Axiom Bbdayfo 27817
[Alling] p. 184Axiom Oltsso 27816
[Alling] p. 184Axiom SDnodense 27832
[Alling] p. 185Lemma 0nocvxmin 27924
[Alling] p. 185Theoremconway 27948
[Alling] p. 185Axiom FEnoeta 27883
[Alling] p. 186Theorem 4lesrec 27968  lesrecd 27969
[Alling], p. 2Definitionrp-brsslt 44119
[Alling], p. 3Notenla0001 44122  nla0002 44120  nla0003 44121
[Apostol] p. 18Theorem I.1addcan 11393  addcan2d 11413  addcan2i 11403  addcand 11412  addcani 11402
[Apostol] p. 18Theorem I.2negeu 11446
[Apostol] p. 18Theorem I.3negsub 11505  negsubd 11574  negsubi 11535
[Apostol] p. 18Theorem I.4negneg 11507  negnegd 11559  negnegi 11527
[Apostol] p. 18Theorem I.5subdi 11646  subdid 11669  subdii 11662  subdir 11647  subdird 11670  subdiri 11663
[Apostol] p. 18Theorem I.6mul01 11388  mul01d 11408  mul01i 11399  mul02 11387  mul02d 11407  mul02i 11398
[Apostol] p. 18Theorem I.7mulcan 11850  mulcan2d 11847  mulcand 11846  mulcani 11852
[Apostol] p. 18Theorem I.8receu 11858  xreceu 33207
[Apostol] p. 18Theorem I.9divrec 11887  divrecd 11993  divreci 11959  divreczi 11952
[Apostol] p. 18Theorem I.10recrec 11911  recreci 11946
[Apostol] p. 18Theorem I.11mul0or 11853  mul0ord 11861  mul0ori 11860
[Apostol] p. 18Theorem I.12mul2neg 11652  mul2negd 11668  mul2negi 11661  mulneg1 11649  mulneg1d 11666  mulneg1i 11659
[Apostol] p. 18Theorem I.13divadddiv 11929  divadddivd 12034  divadddivi 11976
[Apostol] p. 18Theorem I.14divmuldiv 11914  divmuldivd 12031  divmuldivi 11974  rdivmuldivd 20494
[Apostol] p. 18Theorem I.15divdivdiv 11915  divdivdivd 12037  divdivdivi 11977
[Apostol] p. 20Axiom 7rpaddcl 13039  rpaddcld 13074  rpmulcl 13040  rpmulcld 13075
[Apostol] p. 20Axiom 8rpneg 13049
[Apostol] p. 20Axiom 90nrp 13052
[Apostol] p. 20Theorem I.17lttri 11335
[Apostol] p. 20Theorem I.18ltadd1d 11806  ltadd1dd 11824  ltadd1i 11767
[Apostol] p. 20Theorem I.19ltmul1 12064  ltmul1a 12063  ltmul1i 12132  ltmul1ii 12142  ltmul2 12065  ltmul2d 13101  ltmul2dd 13115  ltmul2i 12135
[Apostol] p. 20Theorem I.20msqgt0 11733  msqgt0d 11780  msqgt0i 11750
[Apostol] p. 20Theorem I.210lt1 11735
[Apostol] p. 20Theorem I.23lt0neg1 11719  lt0neg1d 11782  ltneg 11713  ltnegd 11791  ltnegi 11757
[Apostol] p. 20Theorem I.25lt2add 11698  lt2addd 11836  lt2addi 11775
[Apostol] p. 20Definition of positive numbersdf-rp 13016
[Apostol] p. 21Exercise 4recgt0 12060  recgt0d 12148  recgt0i 12119  recgt0ii 12120
[Apostol] p. 22Definition of integersdf-z 12591
[Apostol] p. 22Definition of positive integersdfnn3 12246
[Apostol] p. 22Definition of rationalsdf-q 12972
[Apostol] p. 24Theorem I.26supeu 9413
[Apostol] p. 26Theorem I.28nnunb 12499
[Apostol] p. 26Theorem I.29arch 12500  archd 45850
[Apostol] p. 28Exercise 2btwnz 12698
[Apostol] p. 28Exercise 3nnrecl 12501
[Apostol] p. 28Exercise 4rebtwnz 12970
[Apostol] p. 28Exercise 5zbtwnre 12969
[Apostol] p. 28Exercise 6qbtwnre 13224
[Apostol] p. 28Exercise 10(a)zeneo 16396  zneo 12678  zneoALTV 48401
[Apostol] p. 29Theorem I.35cxpsqrtth 26871  msqsqrtd 15494  resqrtth 15306  sqrtth 15416  sqrtthi 15422  sqsqrtd 15493
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 12235
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 12936
[Apostol] p. 361Remarkcrreczi 14264
[Apostol] p. 363Remarkabsgt0i 15451
[Apostol] p. 363Exampleabssubd 15507  abssubi 15455
[ApostolNT] p. 7Remarkfmtno0 48259  fmtno1 48260  fmtno2 48269  fmtno3 48270  fmtno4 48271  fmtno5fac 48301  fmtnofz04prm 48296
[ApostolNT] p. 7Definitiondf-fmtno 48247
[ApostolNT] p. 8Definitiondf-ppi 27240
[ApostolNT] p. 14Definitiondf-dvds 16310
[ApostolNT] p. 14Theorem 1.1(a)iddvds 16326
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 16351
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 16346
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 16339
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 16341
[ApostolNT] p. 14Theorem 1.1(f)1dvds 16327
[ApostolNT] p. 14Theorem 1.1(g)dvds0 16328
[ApostolNT] p. 14Theorem 1.1(h)0dvds 16333
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 16368
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 16370
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 16372
[ApostolNT] p. 15Definitiondf-gcd 16552  dfgcd2 16603
[ApostolNT] p. 16Definitionisprm2 16739
[ApostolNT] p. 16Theorem 1.5coprmdvds 16710
[ApostolNT] p. 16Theorem 1.7prminf 16974
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 16570
[ApostolNT] p. 16Theorem 1.4(b)gcdass 16604
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 16606
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 16585
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 16577
[ApostolNT] p. 17Theorem 1.8coprm 16769
[ApostolNT] p. 17Theorem 1.9euclemma 16771
[ApostolNT] p. 17Theorem 1.101arith2 16987
[ApostolNT] p. 18Theorem 1.13prmrec 16981
[ApostolNT] p. 19Theorem 1.14divalg 16460
[ApostolNT] p. 20Theorem 1.15eucalg 16644
[ApostolNT] p. 24Definitiondf-mu 27241
[ApostolNT] p. 25Definitiondf-phi 16824
[ApostolNT] p. 25Theorem 2.1musum 27331
[ApostolNT] p. 26Theorem 2.2phisum 16849
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 16834
[ApostolNT] p. 28Theorem 2.5(c)phimul 16838
[ApostolNT] p. 32Definitiondf-vma 27238
[ApostolNT] p. 32Theorem 2.9muinv 27333
[ApostolNT] p. 32Theorem 2.10vmasum 27356
[ApostolNT] p. 38Remarkdf-sgm 27242
[ApostolNT] p. 38Definitiondf-sgm 27242
[ApostolNT] p. 75Definitiondf-chp 27239  df-cht 27237
[ApostolNT] p. 104Definitioncongr 16721
[ApostolNT] p. 106Remarkdvdsval3 16313
[ApostolNT] p. 106Definitionmoddvds 16320
[ApostolNT] p. 107Example 2mod2eq0even 16403
[ApostolNT] p. 107Example 3mod2eq1n2dvds 16404
[ApostolNT] p. 107Example 4zmod1congr 13921
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 13961
[ApostolNT] p. 107Theorem 5.2(c)modexp 14274
[ApostolNT] p. 108Theorem 5.3modmulconst 16345
[ApostolNT] p. 109Theorem 5.4cncongr1 16724
[ApostolNT] p. 109Theorem 5.6gcdmodi 17133
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 16726
[ApostolNT] p. 113Theorem 5.17eulerth 16841
[ApostolNT] p. 113Theorem 5.18vfermltl 16860
[ApostolNT] p. 114Theorem 5.19fermltl 16842
[ApostolNT] p. 116Theorem 5.24wilthimp 27212
[ApostolNT] p. 179Definitiondf-lgs 27435  lgsprme0 27479
[ApostolNT] p. 180Example 11lgs 27480
[ApostolNT] p. 180Theorem 9.2lgsvalmod 27456
[ApostolNT] p. 180Theorem 9.3lgsdirprm 27471
[ApostolNT] p. 181Theorem 9.4m1lgs 27528
[ApostolNT] p. 181Theorem 9.52lgs 27547  2lgsoddprm 27556
[ApostolNT] p. 182Theorem 9.6gausslemma2d 27514
[ApostolNT] p. 185Theorem 9.8lgsquad 27523
[ApostolNT] p. 188Definitiondf-lgs 27435  lgs1 27481
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 27472
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 27474
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 27482
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 27483
[Baer] p. 40Property (b)mapdord 42380
[Baer] p. 40Property (c)mapd11 42381
[Baer] p. 40Property (e)mapdin 42404  mapdlsm 42406
[Baer] p. 40Property (f)mapd0 42407
[Baer] p. 40Definition of projectivitydf-mapd 42367  mapd1o 42390
[Baer] p. 41Property (g)mapdat 42409
[Baer] p. 44Part (1)mapdpg 42448
[Baer] p. 45Part (2)hdmap1eq 42543  mapdheq 42470  mapdheq2 42471  mapdheq2biN 42472
[Baer] p. 45Part (3)baerlem3 42455
[Baer] p. 46Part (4)mapdheq4 42474  mapdheq4lem 42473
[Baer] p. 46Part (5)baerlem5a 42456  baerlem5abmN 42460  baerlem5amN 42458  baerlem5b 42457  baerlem5bmN 42459
[Baer] p. 47Part (6)hdmap1l6 42563  hdmap1l6a 42551  hdmap1l6e 42556  hdmap1l6f 42557  hdmap1l6g 42558  hdmap1l6lem1 42549  hdmap1l6lem2 42550  mapdh6N 42489  mapdh6aN 42477  mapdh6eN 42482  mapdh6fN 42483  mapdh6gN 42484  mapdh6lem1N 42475  mapdh6lem2N 42476
[Baer] p. 48Part 9hdmapval 42570
[Baer] p. 48Part 10hdmap10 42582
[Baer] p. 48Part 11hdmapadd 42585
[Baer] p. 48Part (6)hdmap1l6h 42559  mapdh6hN 42485
[Baer] p. 48Part (7)mapdh75cN 42495  mapdh75d 42496  mapdh75e 42494  mapdh75fN 42497  mapdh7cN 42491  mapdh7dN 42492  mapdh7eN 42490  mapdh7fN 42493
[Baer] p. 48Part (8)mapdh8 42530  mapdh8a 42517  mapdh8aa 42518  mapdh8ab 42519  mapdh8ac 42520  mapdh8ad 42521  mapdh8b 42522  mapdh8c 42523  mapdh8d 42525  mapdh8d0N 42524  mapdh8e 42526  mapdh8g 42527  mapdh8i 42528  mapdh8j 42529
[Baer] p. 48Part (9)mapdh9a 42531
[Baer] p. 48Equation 10mapdhvmap 42511
[Baer] p. 49Part 12hdmap11 42590  hdmapeq0 42586  hdmapf1oN 42607  hdmapneg 42588  hdmaprnN 42606  hdmaprnlem1N 42591  hdmaprnlem3N 42592  hdmaprnlem3uN 42593  hdmaprnlem4N 42595  hdmaprnlem6N 42596  hdmaprnlem7N 42597  hdmaprnlem8N 42598  hdmaprnlem9N 42599  hdmapsub 42589
[Baer] p. 49Part 14hdmap14lem1 42610  hdmap14lem10 42619  hdmap14lem1a 42608  hdmap14lem2N 42611  hdmap14lem2a 42609  hdmap14lem3 42612  hdmap14lem8 42617  hdmap14lem9 42618
[Baer] p. 50Part 14hdmap14lem11 42620  hdmap14lem12 42621  hdmap14lem13 42622  hdmap14lem14 42623  hdmap14lem15 42624  hgmapval 42629
[Baer] p. 50Part 15hgmapadd 42636  hgmapmul 42637  hgmaprnlem2N 42639  hgmapvs 42633
[Baer] p. 50Part 16hgmaprnN 42643
[Baer] p. 110Lemma 1hdmapip0com 42659
[Baer] p. 110Line 27hdmapinvlem1 42660
[Baer] p. 110Line 28hdmapinvlem2 42661
[Baer] p. 110Line 30hdmapinvlem3 42662
[Baer] p. 110Part 1.2hdmapglem5 42664  hgmapvv 42668
[Baer] p. 110Proposition 1hdmapinvlem4 42663
[Baer] p. 111Line 10hgmapvvlem1 42665
[Baer] p. 111Line 15hdmapg 42672  hdmapglem7 42671
[Bauer], p. 483Theorem 1.22irrexpq 26872  2irrexpqALT 26941
[BellMachover] p. 36Lemma 10.3idALT 24
[BellMachover] p. 97Definition 10.1df-eu 2595
[BellMachover] p. 460Notationdf-mo 2565
[BellMachover] p. 460Definitionmo3 2590
[BellMachover] p. 461Axiom Extax-ext 2733
[BellMachover] p. 462Theorem 1.1axextmo 2737
[BellMachover] p. 463Axiom Repaxrep5 5245
[BellMachover] p. 463Scheme Sepax-sep 5256
[BellMachover] p. 463Theorem 1.3(ii)bj-bm1.3ii 37666  sepex 5262
[BellMachover] p. 466Problemaxpow2 5338
[BellMachover] p. 466Axiom Powaxpow3 5339
[BellMachover] p. 466Axiom Unionaxun2 7734
[BellMachover] p. 468Definitiondf-ord 6363
[BellMachover] p. 469Theorem 2.2(i)ordirr 6378
[BellMachover] p. 469Theorem 2.2(iii)onelon 6385
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 6380
[BellMachover] p. 471Definition of Ndf-om 7862
[BellMachover] p. 471Problem 2.5(ii)uniordint 7799
[BellMachover] p. 471Definition of Limdf-lim 6365
[BellMachover] p. 472Axiom Infzfinf2 9610
[BellMachover] p. 473Theorem 2.8limom 7877
[BellMachover] p. 477Equation 3.1df-r1 9735
[BellMachover] p. 478Definitionrankval2 9789  rankval2b 35458
[BellMachover] p. 478Theorem 3.3(i)r1ord3 9753  r1ord3g 9750
[BellMachover] p. 480Axiom Regzfreg 9557
[BellMachover] p. 488Axiom ACac5 10460  dfac4 10105
[BellMachover] p. 490Definition of alephalephval3 10093
[BeltramettiCassinelli] p. 98Remarkatlatmstc 40061
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 32671
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 32713  chirredi 32712
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 32701
[Beran] p. 3Definition of joinsshjval3 31672
[Beran] p. 39Theorem 2.3(i)cmcm2 31934  cmcm2i 31911  cmcm2ii 31916  cmt2N 39992
[Beran] p. 40Theorem 2.3(iii)lecm 31935  lecmi 31920  lecmii 31921
[Beran] p. 45Theorem 3.4cmcmlem 31909
[Beran] p. 49Theorem 4.2cm2j 31938  cm2ji 31943  cm2mi 31944
[Beran] p. 95Definitiondf-sh 31525  issh2 31527
[Beran] p. 95Lemma 3.1(S5)his5 31404
[Beran] p. 95Lemma 3.1(S6)his6 31417
[Beran] p. 95Lemma 3.1(S7)his7 31408
[Beran] p. 95Lemma 3.2(S8)ho01i 32146
[Beran] p. 95Lemma 3.2(S9)hoeq1 32148
[Beran] p. 95Lemma 3.2(S10)ho02i 32147
[Beran] p. 95Lemma 3.2(S11)hoeq2 32149
[Beran] p. 95Postulate (S1)ax-his1 31400  his1i 31418
[Beran] p. 95Postulate (S2)ax-his2 31401
[Beran] p. 95Postulate (S3)ax-his3 31402
[Beran] p. 95Postulate (S4)ax-his4 31403
[Beran] p. 96Definition of normdf-hnorm 31286  dfhnorm2 31440  normval 31442
[Beran] p. 96Definition for Cauchy sequencehcau 31502
[Beran] p. 96Definition of Cauchy sequencedf-hcau 31291
[Beran] p. 96Definition of complete subspaceisch3 31559
[Beran] p. 96Definition of convergedf-hlim 31290  hlimi 31506
[Beran] p. 97Theorem 3.3(i)norm-i-i 31451  norm-i 31447
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 31455  norm-ii 31456  normlem0 31427  normlem1 31428  normlem2 31429  normlem3 31430  normlem4 31431  normlem5 31432  normlem6 31433  normlem7 31434  normlem7tALT 31437
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 31457  norm-iii 31458
[Beran] p. 98Remark 3.4bcs 31499  bcsiALT 31497  bcsiHIL 31498
[Beran] p. 98Remark 3.4(B)normlem9at 31439  normpar 31473  normpari 31472
[Beran] p. 98Remark 3.4(C)normpyc 31464  normpyth 31463  normpythi 31460
[Beran] p. 99Remarklnfn0 32365  lnfn0i 32360  lnop0 32284  lnop0i 32288
[Beran] p. 99Theorem 3.5(i)nmcexi 32344  nmcfnex 32371  nmcfnexi 32369  nmcopex 32347  nmcopexi 32345
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 32372  nmcfnlbi 32370  nmcoplb 32348  nmcoplbi 32346
[Beran] p. 99Theorem 3.5(iii)lnfncon 32374  lnfnconi 32373  lnopcon 32353  lnopconi 32352
[Beran] p. 100Lemma 3.6normpar2i 31474
[Beran] p. 101Lemma 3.6norm3adifi 31471  norm3adifii 31466  norm3dif 31468  norm3difi 31465
[Beran] p. 102Theorem 3.7(i)chocunii 31619  pjhth 31711  pjhtheu 31712  pjpjhth 31743  pjpjhthi 31744  pjth 25577
[Beran] p. 102Theorem 3.7(ii)ococ 31724  ococi 31723
[Beran] p. 103Remark 3.8nlelchi 32379
[Beran] p. 104Theorem 3.9riesz3i 32380  riesz4 32382  riesz4i 32381
[Beran] p. 104Theorem 3.10cnlnadj 32397  cnlnadjeu 32396  cnlnadjeui 32395  cnlnadji 32394  cnlnadjlem1 32385  nmopadjlei 32406
[Beran] p. 106Theorem 3.11(i)adjeq0 32409
[Beran] p. 106Theorem 3.11(v)nmopadji 32408
[Beran] p. 106Theorem 3.11(ii)adjmul 32410
[Beran] p. 106Theorem 3.11(iv)adjadj 32254
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 32420  nmopcoadji 32419
[Beran] p. 106Theorem 3.11(iii)adjadd 32411
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 32421
[Beran] p. 106Theorem 3.11(viii)adjcoi 32418  pjadj2coi 32522  pjadjcoi 32479
[Beran] p. 107Definitiondf-ch 31539  isch2 31541
[Beran] p. 107Remark 3.12choccl 31624  isch3 31559  occl 31622  ocsh 31601  shoccl 31623  shocsh 31602
[Beran] p. 107Remark 3.12(B)ococin 31726
[Beran] p. 108Theorem 3.13chintcl 31650
[Beran] p. 109Property (i)pjadj2 32505  pjadj3 32506  pjadji 32003  pjadjii 31992
[Beran] p. 109Property (ii)pjidmco 32499  pjidmcoi 32495  pjidmi 31991
[Beran] p. 110Definition of projector orderingpjordi 32491
[Beran] p. 111Remarkho0val 32068  pjch1 31988
[Beran] p. 111Definitiondf-hfmul 32052  df-hfsum 32051  df-hodif 32050  df-homul 32049  df-hosum 32048
[Beran] p. 111Lemma 4.4(i)pjo 31989
[Beran] p. 111Lemma 4.4(ii)pjch 32012  pjchi 31750
[Beran] p. 111Lemma 4.4(iii)pjoc2 31757  pjoc2i 31756
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 31998
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 32483  pjssmii 31999
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 32482
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 32481
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 32486
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 32484  pjssge0ii 32000
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 32485  pjdifnormii 32001
[Bobzien] p. 116Statement T3stoic3 1804
[Bobzien] p. 117Statement T2stoic2a 1802
[Bobzien] p. 117Statement T4stoic4a 1805
[Bobzien] p. 117Conclusion the contradictorystoic1a 1800
[Bogachev] p. 16Definition 1.5df-oms 34648
[Bogachev] p. 17Lemma 1.5.4omssubadd 34656
[Bogachev] p. 17Example 1.5.2omsmon 34654
[Bogachev] p. 41Definition 1.11.2df-carsg 34658
[Bogachev] p. 42Theorem 1.11.4carsgsiga 34678
[Bogachev] p. 116Definition 2.3.1df-itgm 34709  df-sitm 34687
[Bogachev] p. 118Chapter 2.4.4df-itgm 34709
[Bogachev] p. 118Definition 2.4.1df-sitg 34686
[Bollobas] p. 1Section I.1df-edg 29364  isuhgrop 29386  isusgrop 29478  isuspgrop 29477
[Bollobas] p. 2Section I.1df-isubgr 48593  df-subgr 29584  uhgrspan1 29619  uhgrspansubgr 29607
[Bollobas] p. 3Definitiondf-gric 48613  gricuspgr 48650  isuspgrim 48628
[Bollobas] p. 3Section I.1cusgrsize 29770  df-clnbgr 48551  df-cusgr 29728  df-nbgr 29649  fusgrmaxsize 29780
[Bollobas] p. 4Definitiondf-upwlks 48866  df-wlks 29915
[Bollobas] p. 4Section I.1finsumvtxdg2size 29866  finsumvtxdgeven 29868  fusgr1th 29867  fusgrvtxdgonume 29870  vtxdgoddnumeven 29869
[Bollobas] p. 5Notationdf-pths 30029
[Bollobas] p. 5Definitiondf-crcts 30101  df-cycls 30102  df-trls 30006  df-wlkson 29916
[Bollobas] p. 7Section I.1df-ushgr 29375
[BourbakiAlg1] p. 1Definition 1df-clintop 48932  df-cllaw 48918  df-mgm 18697  df-mgm2 48951
[BourbakiAlg1] p. 4Definition 5df-assintop 48933  df-asslaw 48920  df-sgrp 18776  df-sgrp2 48953
[BourbakiAlg1] p. 7Definition 8df-cmgm2 48952  df-comlaw 48919
[BourbakiAlg1] p. 12Definition 2df-mnd 18792
[BourbakiAlg1] p. 17Chapter I.mndlactf1 33312  mndlactf1o 33316  mndractf1 33314  mndractf1o 33317
[BourbakiAlg1] p. 92Definition 1df-ring 20316
[BourbakiAlg1] p. 93Section I.8.1df-rng 20230
[BourbakiAlg1] p. 298Proposition 9lvecendof1f1o 33989
[BourbakiAlg2] p. 113Chapter 5.assafld 33993  assarrginv 33992
[BourbakiAlg2] p. 116Chapter 5,fldextrspundgle 34034  fldextrspunfld 34032  fldextrspunlem1 34031  fldextrspunlem2 34033  fldextrspunlsp 34030  fldextrspunlsplem 34029
[BourbakiCAlg2], p. 228Proposition 21arithidom 33793  dfufd2 33806
[BourbakiEns] p. Proposition 8fcof1 7285  fcofo 7286
[BourbakiTop1] p. Remarkxnegmnf 13235  xnegpnf 13234
[BourbakiTop1] p. Remark rexneg 13236
[BourbakiTop1] p. Remark 3ust0 24356  ustfilxp 24349
[BourbakiTop1] p. Axiom GT'tgpsubcn 24226
[BourbakiTop1] p. Criterionishmeo 23895
[BourbakiTop1] p. Example 1cstucnd 24419  iducn 24418  snfil 24000
[BourbakiTop1] p. Example 2neifil 24016
[BourbakiTop1] p. Theorem 1cnextcn 24203
[BourbakiTop1] p. Theorem 2ucnextcn 24439
[BourbakiTop1] p. Theorem 3df-hcmp 34313
[BourbakiTop1] p. Paragraph 3infil 23999
[BourbakiTop1] p. Definition 1df-ucn 24411  df-ust 24337  filintn0 23997  filn0 23998  istgp 24213  ucnprima 24417
[BourbakiTop1] p. Definition 2df-cfilu 24422
[BourbakiTop1] p. Definition 3df-cusp 24433  df-usp 24393  df-utop 24367  trust 24365
[BourbakiTop1] p. Definition 6df-pcmp 34212
[BourbakiTop1] p. Property V_issnei2 23252
[BourbakiTop1] p. Theorem 1(d)iscncl 23405
[BourbakiTop1] p. Condition F_Iustssel 24342
[BourbakiTop1] p. Condition U_Iustdiag 24345
[BourbakiTop1] p. Property V_iiinnei 23261
[BourbakiTop1] p. Property V_ivneiptopreu 23269  neissex 23263
[BourbakiTop1] p. Proposition 1neips 23249  neiss 23245  ucncn 24420  ustund 24358  ustuqtop 24382
[BourbakiTop1] p. Proposition 2cnpco 23403  neiptopreu 23269  utop2nei 24386  utop3cls 24387
[BourbakiTop1] p. Proposition 3fmucnd 24427  uspreg 24409  utopreg 24388
[BourbakiTop1] p. Proposition 4imasncld 23827  imasncls 23828  imasnopn 23826
[BourbakiTop1] p. Proposition 9cnpflf2 24136
[BourbakiTop1] p. Condition F_IIustincl 24344
[BourbakiTop1] p. Condition U_IIustinvel 24346
[BourbakiTop1] p. Property V_iiielnei 23247
[BourbakiTop1] p. Proposition 11cnextucn 24438
[BourbakiTop1] p. Condition F_IIbustbasel 24343
[BourbakiTop1] p. Condition U_IIIustexhalf 24347
[BourbakiTop1] p. Definition C'''df-cmp 23523
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 23982
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 23030
[BourbakiTop2] p. 195Definition 1df-ldlf 34209
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 46746
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 46748  stoweid 46747
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 46685  stoweidlem10 46694  stoweidlem14 46698  stoweidlem15 46699  stoweidlem35 46719  stoweidlem36 46720  stoweidlem37 46721  stoweidlem38 46722  stoweidlem40 46724  stoweidlem41 46725  stoweidlem43 46727  stoweidlem44 46728  stoweidlem46 46730  stoweidlem5 46689  stoweidlem50 46734  stoweidlem52 46736  stoweidlem53 46737  stoweidlem55 46739  stoweidlem56 46740
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 46707  stoweidlem24 46708  stoweidlem27 46711  stoweidlem28 46712  stoweidlem30 46714
[BrosowskiDeutsh] p. 91Proofstoweidlem34 46718  stoweidlem59 46743  stoweidlem60 46744
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 46729  stoweidlem49 46733  stoweidlem7 46691
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 46715  stoweidlem39 46723  stoweidlem42 46726  stoweidlem48 46732  stoweidlem51 46735  stoweidlem54 46738  stoweidlem57 46741  stoweidlem58 46742
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 46709
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 46701
[BrosowskiDeutsh] p. 92Proofstoweidlem11 46695  stoweidlem13 46697  stoweidlem26 46710  stoweidlem61 46745
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 46702
[Bruck] p. 1Section I.1df-clintop 48932  df-mgm 18697  df-mgm2 48951
[Bruck] p. 23Section II.1df-sgrp 18776  df-sgrp2 48953
[Bruck] p. 28Theorem 3.2dfgrp3 19104
[ChoquetDD] p. 2Definition of mappingdf-mpt 5192
[Church] p. 129Section II.24df-ifp 1077  dfifp2 1078
[Clemente] p. 10Definition ITnatded 30720
[Clemente] p. 10Definition I` `m,nnatded 30720
[Clemente] p. 11Definition E=>m,nnatded 30720
[Clemente] p. 11Definition I=>m,nnatded 30720
[Clemente] p. 11Definition E` `(1)natded 30720
[Clemente] p. 11Definition E` `(2)natded 30720
[Clemente] p. 12Definition E` `m,n,pnatded 30720
[Clemente] p. 12Definition I` `n(1)natded 30720
[Clemente] p. 12Definition I` `n(2)natded 30720
[Clemente] p. 13Definition I` `m,n,pnatded 30720
[Clemente] p. 14Proof 5.11natded 30720
[Clemente] p. 14Definition E` `nnatded 30720
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 30722  ex-natded5.2 30721
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 30725  ex-natded5.3 30724
[Clemente] p. 18Theorem 5.5ex-natded5.5 30727
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 30729  ex-natded5.7 30728
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 30731  ex-natded5.8 30730
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 30733  ex-natded5.13 30732
[Clemente] p. 32Definition I` `nnatded 30720
[Clemente] p. 32Definition E` `m,n,p,anatded 30720
[Clemente] p. 32Definition E` `n,tnatded 30720
[Clemente] p. 32Definition I` `n,tnatded 30720
[Clemente] p. 43Theorem 9.20ex-natded9.20 30734
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 30735
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 30737  ex-natded9.26 30736
[Cohen] p. 301Remarkrelogoprlem 26732
[Cohen] p. 301Property 2relogmul 26733  relogmuld 26766
[Cohen] p. 301Property 3relogdiv 26734  relogdivd 26767
[Cohen] p. 301Property 4relogexp 26737
[Cohen] p. 301Property 1alog1 26726
[Cohen] p. 301Property 1bloge 26727
[Cohen4] p. 348Observationrelogbcxpb 26928
[Cohen4] p. 349Propertyrelogbf 26932
[Cohen4] p. 352Definitionelogb 26911
[Cohen4] p. 361Property 2relogbmul 26918
[Cohen4] p. 361Property 3logbrec 26923  relogbdiv 26920
[Cohen4] p. 361Property 4relogbreexp 26916
[Cohen4] p. 361Property 6relogbexp 26921
[Cohen4] p. 361Property 1(a)logbid1 26909
[Cohen4] p. 361Property 1(b)logb1 26910
[Cohen4] p. 367Propertylogbchbase 26912
[Cohen4] p. 377Property 2logblt 26925
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 34641  sxbrsigalem4 34643
[Cohn] p. 81Section II.5acsdomd 18612  acsinfd 18611  acsinfdimd 18613  acsmap2d 18610  acsmapd 18609
[Cohn] p. 143Example 5.1.1sxbrsiga 34646
[Connell] p. 57Definitiondf-scmat 22627  df-scmatalt 49146
[Conway] p. 4Definitionlesrec 27968  lesrecd 27969
[Conway] p. 5Definitionaddsval 28131  addsval2 28132  df-adds 28129  df-muls 28276  df-negs 28190
[Conway] p. 7Theorem0lt1s 27981
[Conway] p. 12Theorem 12pw2cut2 28631
[Conway] p. 16Theorem 0(i)sltsright 28030
[Conway] p. 16Theorem 0(ii)sltsleft 28029
[Conway] p. 16Theorem 0(iii)lesid 27907
[Conway] p. 17Theorem 3addsass 28174  addsassd 28175  addscom 28135  addscomd 28136  addsrid 28133  addsridd 28134
[Conway] p. 17Definitiondf-0s 27976
[Conway] p. 17Theorem 4(ii)negnegs 28213
[Conway] p. 17Theorem 4(iii)negsid 28210  negsidd 28211
[Conway] p. 18Theorem 5leadds1 28158  leadds1d 28164
[Conway] p. 18Definitiondf-1s 27977
[Conway] p. 18Theorem 6(ii)negscl 28205  negscld 28206
[Conway] p. 18Theorem 6(iii)addscld 28149
[Conway] p. 19Notemulsunif2 28339
[Conway] p. 19Theorem 7addsdi 28324  addsdid 28325  addsdird 28326  mulnegs1d 28329  mulnegs2d 28330  mulsass 28335  mulsassd 28336  mulscom 28308  mulscomd 28309
[Conway] p. 19Theorem 8(i)mulscl 28303  mulscld 28304
[Conway] p. 19Theorem 8(iii)lemulsd 28307  ltmuls 28305  ltmulsd 28306
[Conway] p. 20Theorem 9mulsgt0 28313  mulsgt0d 28314
[Conway] p. 21Theorem 10(iv)precsex 28387
[Conway] p. 23Theorem 11eqcuts3 27973
[Conway] p. 24Definitiondf-reno 28659
[Conway] p. 24Theorem 13(ii)readdscl 28668  remulscl 28671  renegscl 28667
[Conway] p. 27Definitiondf-ons 28421  elons2 28427
[Conway] p. 27Theorem 14ltonsex 28431
[Conway] p. 28Theorem 15oncutlt 28433  onswe 28441
[Conway] p. 29Remarkmadebday 28069  newbday 28071  oldbday 28070
[Conway] p. 29Definitiondf-made 27996  df-new 27998  df-old 27997
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 13894
[Crawley] p. 1Definition of posetdf-poset 18368
[Crawley] p. 107Theorem 13.2hlsupr 40128
[Crawley] p. 110Theorem 13.3arglem1N 40932  dalaw 40628
[Crawley] p. 111Theorem 13.4hlathil 42703
[Crawley] p. 111Definition of set Wdf-watsN 40732
[Crawley] p. 111Definition of dilationdf-dilN 40848  df-ldil 40846  isldil 40852
[Crawley] p. 111Definition of translationdf-ltrn 40847  df-trnN 40849  isltrn 40861  ltrnu 40863
[Crawley] p. 112Lemma Acdlema1N 40533  cdlema2N 40534  exatleN 40146
[Crawley] p. 112Lemma B1cvrat 40218  cdlemb 40536  cdlemb2 40783  cdlemb3 41348  idltrn 40892  l1cvat 39797  lhpat 40785  lhpat2 40787  lshpat 39798  ltrnel 40881  ltrnmw 40893
[Crawley] p. 112Lemma Ccdlemc1 40933  cdlemc2 40934  ltrnnidn 40916  trlat 40911  trljat1 40908  trljat2 40909  trljat3 40910  trlne 40927  trlnidat 40915  trlnle 40928
[Crawley] p. 112Definition of automorphismdf-pautN 40733
[Crawley] p. 113Lemma Ccdlemc 40939  cdlemc3 40935  cdlemc4 40936
[Crawley] p. 113Lemma Dcdlemd 40949  cdlemd1 40940  cdlemd2 40941  cdlemd3 40942  cdlemd4 40943  cdlemd5 40944  cdlemd6 40945  cdlemd7 40946  cdlemd8 40947  cdlemd9 40948  cdleme31sde 41127  cdleme31se 41124  cdleme31se2 41125  cdleme31snd 41128  cdleme32a 41183  cdleme32b 41184  cdleme32c 41185  cdleme32d 41186  cdleme32e 41187  cdleme32f 41188  cdleme32fva 41179  cdleme32fva1 41180  cdleme32fvcl 41182  cdleme32le 41189  cdleme48fv 41241  cdleme4gfv 41249  cdleme50eq 41283  cdleme50f 41284  cdleme50f1 41285  cdleme50f1o 41288  cdleme50laut 41289  cdleme50ldil 41290  cdleme50lebi 41282  cdleme50rn 41287  cdleme50rnlem 41286  cdlemeg49le 41253  cdlemeg49lebilem 41281
[Crawley] p. 113Lemma Ecdleme 41302  cdleme00a 40951  cdleme01N 40963  cdleme02N 40964  cdleme0a 40953  cdleme0aa 40952  cdleme0b 40954  cdleme0c 40955  cdleme0cp 40956  cdleme0cq 40957  cdleme0dN 40958  cdleme0e 40959  cdleme0ex1N 40965  cdleme0ex2N 40966  cdleme0fN 40960  cdleme0gN 40961  cdleme0moN 40967  cdleme1 40969  cdleme10 40996  cdleme10tN 41000  cdleme11 41012  cdleme11a 41002  cdleme11c 41003  cdleme11dN 41004  cdleme11e 41005  cdleme11fN 41006  cdleme11g 41007  cdleme11h 41008  cdleme11j 41009  cdleme11k 41010  cdleme11l 41011  cdleme12 41013  cdleme13 41014  cdleme14 41015  cdleme15 41020  cdleme15a 41016  cdleme15b 41017  cdleme15c 41018  cdleme15d 41019  cdleme16 41027  cdleme16aN 41001  cdleme16b 41021  cdleme16c 41022  cdleme16d 41023  cdleme16e 41024  cdleme16f 41025  cdleme16g 41026  cdleme19a 41045  cdleme19b 41046  cdleme19c 41047  cdleme19d 41048  cdleme19e 41049  cdleme19f 41050  cdleme1b 40968  cdleme2 40970  cdleme20aN 41051  cdleme20bN 41052  cdleme20c 41053  cdleme20d 41054  cdleme20e 41055  cdleme20f 41056  cdleme20g 41057  cdleme20h 41058  cdleme20i 41059  cdleme20j 41060  cdleme20k 41061  cdleme20l 41064  cdleme20l1 41062  cdleme20l2 41063  cdleme20m 41065  cdleme20y 41044  cdleme20zN 41043  cdleme21 41079  cdleme21d 41072  cdleme21e 41073  cdleme22a 41082  cdleme22aa 41081  cdleme22b 41083  cdleme22cN 41084  cdleme22d 41085  cdleme22e 41086  cdleme22eALTN 41087  cdleme22f 41088  cdleme22f2 41089  cdleme22g 41090  cdleme23a 41091  cdleme23b 41092  cdleme23c 41093  cdleme26e 41101  cdleme26eALTN 41103  cdleme26ee 41102  cdleme26f 41105  cdleme26f2 41107  cdleme26f2ALTN 41106  cdleme26fALTN 41104  cdleme27N 41111  cdleme27a 41109  cdleme27cl 41108  cdleme28c 41114  cdleme3 40979  cdleme30a 41120  cdleme31fv 41132  cdleme31fv1 41133  cdleme31fv1s 41134  cdleme31fv2 41135  cdleme31id 41136  cdleme31sc 41126  cdleme31sdnN 41129  cdleme31sn 41122  cdleme31sn1 41123  cdleme31sn1c 41130  cdleme31sn2 41131  cdleme31so 41121  cdleme35a 41190  cdleme35b 41192  cdleme35c 41193  cdleme35d 41194  cdleme35e 41195  cdleme35f 41196  cdleme35fnpq 41191  cdleme35g 41197  cdleme35h 41198  cdleme35h2 41199  cdleme35sn2aw 41200  cdleme35sn3a 41201  cdleme36a 41202  cdleme36m 41203  cdleme37m 41204  cdleme38m 41205  cdleme38n 41206  cdleme39a 41207  cdleme39n 41208  cdleme3b 40971  cdleme3c 40972  cdleme3d 40973  cdleme3e 40974  cdleme3fN 40975  cdleme3fa 40978  cdleme3g 40976  cdleme3h 40977  cdleme4 40980  cdleme40m 41209  cdleme40n 41210  cdleme40v 41211  cdleme40w 41212  cdleme41fva11 41219  cdleme41sn3aw 41216  cdleme41sn4aw 41217  cdleme41snaw 41218  cdleme42a 41213  cdleme42b 41220  cdleme42c 41214  cdleme42d 41215  cdleme42e 41221  cdleme42f 41222  cdleme42g 41223  cdleme42h 41224  cdleme42i 41225  cdleme42k 41226  cdleme42ke 41227  cdleme42keg 41228  cdleme42mN 41229  cdleme42mgN 41230  cdleme43aN 41231  cdleme43bN 41232  cdleme43cN 41233  cdleme43dN 41234  cdleme5 40982  cdleme50ex 41301  cdleme50ltrn 41299  cdleme51finvN 41298  cdleme51finvfvN 41297  cdleme51finvtrN 41300  cdleme6 40983  cdleme7 40991  cdleme7a 40985  cdleme7aa 40984  cdleme7b 40986  cdleme7c 40987  cdleme7d 40988  cdleme7e 40989  cdleme7ga 40990  cdleme8 40992  cdleme8tN 40997  cdleme9 40995  cdleme9a 40993  cdleme9b 40994  cdleme9tN 40999  cdleme9taN 40998  cdlemeda 41040  cdlemedb 41039  cdlemednpq 41041  cdlemednuN 41042  cdlemefr27cl 41145  cdlemefr32fva1 41152  cdlemefr32fvaN 41151  cdlemefrs32fva 41142  cdlemefrs32fva1 41143  cdlemefs27cl 41155  cdlemefs32fva1 41165  cdlemefs32fvaN 41164  cdlemesner 41038  cdlemeulpq 40962
[Crawley] p. 114Lemma E4atex 40818  4atexlem7 40817  cdleme0nex 41032  cdleme17a 41028  cdleme17c 41030  cdleme17d 41240  cdleme17d1 41031  cdleme17d2 41237  cdleme18a 41033  cdleme18b 41034  cdleme18c 41035  cdleme18d 41037  cdleme4a 40981
[Crawley] p. 115Lemma Ecdleme21a 41067  cdleme21at 41070  cdleme21b 41068  cdleme21c 41069  cdleme21ct 41071  cdleme21f 41074  cdleme21g 41075  cdleme21h 41076  cdleme21i 41077  cdleme22gb 41036
[Crawley] p. 116Lemma Fcdlemf 41305  cdlemf1 41303  cdlemf2 41304
[Crawley] p. 116Lemma Gcdlemftr1 41309  cdlemg16 41399  cdlemg28 41446  cdlemg28a 41435  cdlemg28b 41445  cdlemg3a 41339  cdlemg42 41471  cdlemg43 41472  cdlemg44 41475  cdlemg44a 41473  cdlemg46 41477  cdlemg47 41478  cdlemg9 41376  ltrnco 41461  ltrncom 41480  tgrpabl 41493  trlco 41469
[Crawley] p. 116Definition of Gdf-tgrp 41485
[Crawley] p. 117Lemma Gcdlemg17 41419  cdlemg17b 41404
[Crawley] p. 117Definition of Edf-edring-rN 41498  df-edring 41499
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 41502
[Crawley] p. 118Remarktendopltp 41522
[Crawley] p. 118Lemma Hcdlemh 41559  cdlemh1 41557  cdlemh2 41558
[Crawley] p. 118Lemma Icdlemi 41562  cdlemi1 41560  cdlemi2 41561
[Crawley] p. 118Lemma Jcdlemj1 41563  cdlemj2 41564  cdlemj3 41565  tendocan 41566
[Crawley] p. 118Lemma Kcdlemk 41716  cdlemk1 41573  cdlemk10 41585  cdlemk11 41591  cdlemk11t 41688  cdlemk11ta 41671  cdlemk11tb 41673  cdlemk11tc 41687  cdlemk11u-2N 41631  cdlemk11u 41613  cdlemk12 41592  cdlemk12u-2N 41632  cdlemk12u 41614  cdlemk13-2N 41618  cdlemk13 41594  cdlemk14-2N 41620  cdlemk14 41596  cdlemk15-2N 41621  cdlemk15 41597  cdlemk16-2N 41622  cdlemk16 41599  cdlemk16a 41598  cdlemk17-2N 41623  cdlemk17 41600  cdlemk18-2N 41628  cdlemk18-3N 41642  cdlemk18 41610  cdlemk19-2N 41629  cdlemk19 41611  cdlemk19u 41712  cdlemk1u 41601  cdlemk2 41574  cdlemk20-2N 41634  cdlemk20 41616  cdlemk21-2N 41633  cdlemk21N 41615  cdlemk22-3 41643  cdlemk22 41635  cdlemk23-3 41644  cdlemk24-3 41645  cdlemk25-3 41646  cdlemk26-3 41648  cdlemk26b-3 41647  cdlemk27-3 41649  cdlemk28-3 41650  cdlemk29-3 41653  cdlemk3 41575  cdlemk30 41636  cdlemk31 41638  cdlemk32 41639  cdlemk33N 41651  cdlemk34 41652  cdlemk35 41654  cdlemk36 41655  cdlemk37 41656  cdlemk38 41657  cdlemk39 41658  cdlemk39u 41710  cdlemk4 41576  cdlemk41 41662  cdlemk42 41683  cdlemk42yN 41686  cdlemk43N 41705  cdlemk45 41689  cdlemk46 41690  cdlemk47 41691  cdlemk48 41692  cdlemk49 41693  cdlemk5 41578  cdlemk50 41694  cdlemk51 41695  cdlemk52 41696  cdlemk53 41699  cdlemk54 41700  cdlemk55 41703  cdlemk55u 41708  cdlemk56 41713  cdlemk5a 41577  cdlemk5auN 41602  cdlemk5u 41603  cdlemk6 41579  cdlemk6u 41604  cdlemk7 41590  cdlemk7u-2N 41630  cdlemk7u 41612  cdlemk8 41580  cdlemk9 41581  cdlemk9bN 41582  cdlemki 41583  cdlemkid 41678  cdlemkj-2N 41624  cdlemkj 41605  cdlemksat 41588  cdlemksel 41587  cdlemksv 41586  cdlemksv2 41589  cdlemkuat 41608  cdlemkuel-2N 41626  cdlemkuel-3 41640  cdlemkuel 41607  cdlemkuv-2N 41625  cdlemkuv2-2 41627  cdlemkuv2-3N 41641  cdlemkuv2 41609  cdlemkuvN 41606  cdlemkvcl 41584  cdlemky 41668  cdlemkyyN 41704  tendoex 41717
[Crawley] p. 120Remarkdva1dim 41727
[Crawley] p. 120Lemma Lcdleml1N 41718  cdleml2N 41719  cdleml3N 41720  cdleml4N 41721  cdleml5N 41722  cdleml6 41723  cdleml7 41724  cdleml8 41725  cdleml9 41726  dia1dim 41803
[Crawley] p. 120Lemma Mdia11N 41790  diaf11N 41791  dialss 41788  diaord 41789  dibf11N 41903  djajN 41879
[Crawley] p. 120Definition of isomorphism mapdiaval 41774
[Crawley] p. 121Lemma Mcdlemm10N 41860  dia2dimlem1 41806  dia2dimlem2 41807  dia2dimlem3 41808  dia2dimlem4 41809  dia2dimlem5 41810  diaf1oN 41872  diarnN 41871  dvheveccl 41854  dvhopN 41858
[Crawley] p. 121Lemma Ncdlemn 41954  cdlemn10 41948  cdlemn11 41953  cdlemn11a 41949  cdlemn11b 41950  cdlemn11c 41951  cdlemn11pre 41952  cdlemn2 41937  cdlemn2a 41938  cdlemn3 41939  cdlemn4 41940  cdlemn4a 41941  cdlemn5 41943  cdlemn5pre 41942  cdlemn6 41944  cdlemn7 41945  cdlemn8 41946  cdlemn9 41947  diclspsn 41936
[Crawley] p. 121Definition of phi(q)df-dic 41915
[Crawley] p. 122Lemma Ndih11 42007  dihf11 42009  dihjust 41959  dihjustlem 41958  dihord 42006  dihord1 41960  dihord10 41965  dihord11b 41964  dihord11c 41966  dihord2 41969  dihord2a 41961  dihord2b 41962  dihord2cN 41963  dihord2pre 41967  dihord2pre2 41968  dihordlem6 41955  dihordlem7 41956  dihordlem7b 41957
[Crawley] p. 122Definition of isomorphism mapdihffval 41972  dihfval 41973  dihval 41974
[Diestel] p. 3Definitiondf-gric 48613  df-grim 48610  isuspgrim 48628
[Diestel] p. 3Section 1.1df-cusgr 29728  df-nbgr 29649
[Diestel] p. 3Definition by df-grisom 48609
[Diestel] p. 4Section 1.1df-isubgr 48593  df-subgr 29584  uhgrspan1 29619  uhgrspansubgr 29607
[Diestel] p. 5Proposition 1.2.1fusgrvtxdgonume 29870  vtxdgoddnumeven 29869
[Diestel] p. 27Section 1.10df-ushgr 29375
[EGA] p. 80Notation 1.1.1rspecval 34220
[EGA] p. 80Proposition 1.1.2zartop 34232
[EGA] p. 80Proposition 1.1.2(i)zarcls0 34224  zarcls1 34225
[EGA] p. 81Corollary 1.1.8zart0 34235
[EGA], p. 82Proposition 1.1.10(ii)zarcmp 34238
[EGA], p. 83Corollary 1.2.3rhmpreimacn 34241
[Eisenberg] p. 67Definition 5.3df-dif 3907
[Eisenberg] p. 82Definition 6.3dfom3 9615
[Eisenberg] p. 125Definition 8.21df-map 8825
[Eisenberg] p. 216Example 13.2(4)omenps 9623
[Eisenberg] p. 310Theorem 19.8cardprc 9965
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 10538
[Enderton] p. 18Axiom of Empty Setaxnul 5267
[Enderton] p. 19Definitiondf-tp 4593
[Enderton] p. 26Exercise 5unissb 4905
[Enderton] p. 26Exercise 10pwel 5352
[Enderton] p. 28Exercise 7(b)pwun 5554
[Enderton] p. 30Theorem "Distributive laws"iinin1 5044  iinin2 5043  iinun2 5036  iunin1 5035  iunin1f 32868  iunin2 5034  uniin1 5038  uniin2 5039
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 5042  iundif2 5037
[Enderton] p. 32Exercise 20unineq 4240
[Enderton] p. 33Exercise 23iinuni 5063
[Enderton] p. 33Exercise 25iununi 5064
[Enderton] p. 33Exercise 24(a)iinpw 5071
[Enderton] p. 33Exercise 24(b)iunpw 7769  iunpwss 5072
[Enderton] p. 36Definitionopthwiener 5497
[Enderton] p. 38Exercise 6(a)unipw 5431
[Enderton] p. 38Exercise 6(b)pwuni 4910
[Enderton] p. 41Lemma 3Dopeluu 5452  rnex 7906  rnexg 7898
[Enderton] p. 41Exercise 8dmuni 5904  rnuni 6146
[Enderton] p. 42Definition of a functiondffun7 6563  dffun8 6564
[Enderton] p. 43Definition of function valuefunfv2 6969
[Enderton] p. 43Definition of single-rootedfuncnv 6605
[Enderton] p. 44Definition (d)dfima2 6064  dfima3 6065
[Enderton] p. 47Theorem 3Hfvco2 6978
[Enderton] p. 49Axiom of Choice (first form)ac7 10456  ac7g 10457  df-ac 10099  dfac2 10114  dfac2a 10112  dfac2b 10113  dfac3 10104  dfac7 10115
[Enderton] p. 50Theorem 3K(a)imauni 7244
[Enderton] p. 52Definitiondf-map 8825
[Enderton] p. 53Exercise 21coass 6267
[Enderton] p. 53Exercise 27dmco 6256
[Enderton] p. 53Exercise 14(a)funin 6612
[Enderton] p. 53Exercise 22(a)imass2 6104
[Enderton] p. 54Remarkixpf 8917  ixpssmap 8929
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 8895
[Enderton] p. 55Axiom of Choice (second form)ac9 10466  ac9s 10476
[Enderton] p. 56Theorem 3Meqvrelref 39311  erref 8714
[Enderton] p. 57Lemma 3Neqvrelthi 39314  erthi 8750
[Enderton] p. 57Definitiondf-ec 8695
[Enderton] p. 58Definitiondf-qs 8699
[Enderton] p. 61Exercise 35df-ec 8695
[Enderton] p. 65Exercise 56(a)dmun 5900
[Enderton] p. 68Definition of successordf-suc 6366
[Enderton] p. 71Definitiondf-tr 5218  dftr4 5223
[Enderton] p. 72Theorem 4Eunisuc 6442  unisucg 6441
[Enderton] p. 73Exercise 6unisuc 6442  unisucg 6441
[Enderton] p. 73Exercise 5(a)truni 5233
[Enderton] p. 73Exercise 5(b)trint 5235  trintALT 45559
[Enderton] p. 79Theorem 4I(A1)nna0 8589
[Enderton] p. 79Theorem 4I(A2)nnasuc 8591  onasuc 8512
[Enderton] p. 79Definition of operation valuedf-ov 7413
[Enderton] p. 80Theorem 4J(A1)nnm0 8590
[Enderton] p. 80Theorem 4J(A2)nnmsuc 8592  onmsuc 8513
[Enderton] p. 81Theorem 4K(1)nnaass 8607
[Enderton] p. 81Theorem 4K(2)nna0r 8594  nnacom 8602
[Enderton] p. 81Theorem 4K(3)nndi 8608
[Enderton] p. 81Theorem 4K(4)nnmass 8609
[Enderton] p. 81Theorem 4K(5)nnmcom 8611
[Enderton] p. 82Exercise 16nnm0r 8595  nnmsucr 8610
[Enderton] p. 88Exercise 23nnaordex 8623
[Enderton] p. 129Definitiondf-en 8943
[Enderton] p. 132Theorem 6B(b)canth 7364
[Enderton] p. 133Exercise 1xpomen 9998
[Enderton] p. 133Exercise 2qnnen 16268
[Enderton] p. 134Theorem (Pigeonhole Principle)php 9190
[Enderton] p. 135Corollary 6Cphp3 9192
[Enderton] p. 136Corollary 6Enneneq 9189
[Enderton] p. 136Corollary 6D(a)pssinf 9221
[Enderton] p. 136Corollary 6D(b)ominf 9223
[Enderton] p. 137Lemma 6Fpssnn 9152
[Enderton] p. 138Corollary 6Gssfi 9156
[Enderton] p. 139Theorem 6H(c)mapen 9128
[Enderton] p. 142Theorem 6I(3)xpdjuen 10162
[Enderton] p. 142Theorem 6I(4)mapdjuen 10163
[Enderton] p. 143Theorem 6Jdju0en 10158  dju1en 10154
[Enderton] p. 144Exercise 13iunfi 9299  unifi 9300  unifi2 9301
[Enderton] p. 144Corollary 6Kundif2 4437  unfi 9154  unfi2 9269
[Enderton] p. 145Figure 38ffoss 7942
[Enderton] p. 145Definitiondf-dom 8944
[Enderton] p. 146Example 1domen 8957  domeng 8958
[Enderton] p. 146Example 3nndomo 9201  nnsdom 9622  nnsdomg 9258
[Enderton] p. 149Theorem 6L(a)djudom2 10166
[Enderton] p. 149Theorem 6L(c)mapdom1 9129  xpdom1 9063  xpdom1g 9061  xpdom2g 9060
[Enderton] p. 149Theorem 6L(d)mapdom2 9135
[Enderton] p. 151Theorem 6Mzorn 10490  zorng 10487
[Enderton] p. 151Theorem 6M(4)ac8 10475  dfac5 10111
[Enderton] p. 159Theorem 6Qunictb 10559
[Enderton] p. 164Exampleinfdif 10190
[Enderton] p. 168Definitiondf-po 5569
[Enderton] p. 192Theorem 7M(a)oneli 6476
[Enderton] p. 192Theorem 7M(b)ontr1 6408
[Enderton] p. 192Theorem 7M(c)onirri 6475
[Enderton] p. 193Corollary 7N(b)0elon 6416
[Enderton] p. 193Corollary 7N(c)onsuci 7834
[Enderton] p. 193Corollary 7N(d)ssonunii 7779
[Enderton] p. 194Remarkonprc 7776
[Enderton] p. 194Exercise 16suc11 6470
[Enderton] p. 197Definitiondf-card 9924
[Enderton] p. 197Theorem 7Pcarden 10534
[Enderton] p. 200Exercise 25tfis 7850
[Enderton] p. 202Lemma 7Tr1tr 9747
[Enderton] p. 202Definitiondf-r1 9735
[Enderton] p. 202Theorem 7Qr1val1 9757
[Enderton] p. 204Theorem 7V(b)rankval4 9838  rankval4b 35459
[Enderton] p. 206Theorem 7X(b)en2lp 9574
[Enderton] p. 207Exercise 30rankpr 9828  rankprb 9822  rankpw 9814  rankpwi 9794  rankuniss 9837
[Enderton] p. 207Exercise 34opthreg 9586
[Enderton] p. 208Exercise 35suc11reg 9587
[Enderton] p. 212Definition of alephalephval3 10093
[Enderton] p. 213Theorem 8A(a)alephord2 10059
[Enderton] p. 213Theorem 8A(b)cardalephex 10073
[Enderton] p. 218Theorem Schema 8Eonfununi 8327
[Enderton] p. 222Definitiondf-kard 35529
[Enderton] p. 222Definition of kardkarden 9880  kardex 9879
[Enderton] p. 238Theorem 8Roeoa 8582
[Enderton] p. 238Theorem 8Soeoe 8584
[Enderton] p. 240Exercise 25oarec 8546
[Enderton] p. 257Definition of cofinalitycflm 10232
[FaureFrolicher] p. 57Definition 3.1.9mreexd 17697
[FaureFrolicher] p. 83Definition 4.1.1df-mri 17639
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 18608  mrieqv2d 17694  mrieqvd 17693
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 17698
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 17703  mreexexlem2d 17700
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 18614  mreexfidimd 17705
[Frege1879] p. 11Statementdf3or2 44464
[Frege1879] p. 12Statementdf3an2 44465  dfxor4 44462  dfxor5 44463
[Frege1879] p. 26Axiom 1ax-frege1 44486
[Frege1879] p. 26Axiom 2ax-frege2 44487
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 44491
[Frege1879] p. 31Proposition 4frege4 44495
[Frege1879] p. 32Proposition 5frege5 44496
[Frege1879] p. 33Proposition 6frege6 44502
[Frege1879] p. 34Proposition 7frege7 44504
[Frege1879] p. 35Axiom 8ax-frege8 44505  axfrege8 44503
[Frege1879] p. 35Proposition 8pm2.04 91  wl-luk-pm2.04 38057
[Frege1879] p. 35Proposition 9frege9 44508
[Frege1879] p. 36Proposition 10frege10 44516
[Frege1879] p. 36Proposition 11frege11 44510
[Frege1879] p. 37Proposition 12frege12 44509
[Frege1879] p. 37Proposition 13frege13 44518
[Frege1879] p. 37Proposition 14frege14 44519
[Frege1879] p. 38Proposition 15frege15 44522
[Frege1879] p. 38Proposition 16frege16 44512
[Frege1879] p. 39Proposition 17frege17 44517
[Frege1879] p. 39Proposition 18frege18 44514
[Frege1879] p. 39Proposition 19frege19 44520
[Frege1879] p. 40Proposition 20frege20 44524
[Frege1879] p. 40Proposition 21frege21 44523
[Frege1879] p. 41Proposition 22frege22 44515
[Frege1879] p. 42Proposition 23frege23 44521
[Frege1879] p. 42Proposition 24frege24 44511
[Frege1879] p. 42Proposition 25frege25 44513  rp-frege25 44501
[Frege1879] p. 42Proposition 26frege26 44506
[Frege1879] p. 43Axiom 28ax-frege28 44526
[Frege1879] p. 43Proposition 27frege27 44507
[Frege1879] p. 43Proposition 28con3 154
[Frege1879] p. 43Proposition 29frege29 44527
[Frege1879] p. 44Axiom 31ax-frege31 44530  axfrege31 44529
[Frege1879] p. 44Proposition 30frege30 44528
[Frege1879] p. 44Proposition 31notnotr 131
[Frege1879] p. 44Proposition 32frege32 44531
[Frege1879] p. 44Proposition 33frege33 44532
[Frege1879] p. 45Proposition 34frege34 44533
[Frege1879] p. 45Proposition 35frege35 44534
[Frege1879] p. 45Proposition 36frege36 44535
[Frege1879] p. 46Proposition 37frege37 44536
[Frege1879] p. 46Proposition 38frege38 44537
[Frege1879] p. 46Proposition 39frege39 44538
[Frege1879] p. 46Proposition 40frege40 44539
[Frege1879] p. 47Axiom 41ax-frege41 44541  axfrege41 44540
[Frege1879] p. 47Proposition 41notnot 143
[Frege1879] p. 47Proposition 42frege42 44542
[Frege1879] p. 47Proposition 43frege43 44543
[Frege1879] p. 47Proposition 44frege44 44544
[Frege1879] p. 47Proposition 45frege45 44545
[Frege1879] p. 48Proposition 46frege46 44546
[Frege1879] p. 48Proposition 47frege47 44547
[Frege1879] p. 49Proposition 48frege48 44548
[Frege1879] p. 49Proposition 49frege49 44549
[Frege1879] p. 49Proposition 50frege50 44550
[Frege1879] p. 50Axiom 52ax-frege52a 44553  ax-frege52c 44584  frege52aid 44554  frege52b 44585
[Frege1879] p. 50Axiom 54ax-frege54a 44558  ax-frege54c 44588  frege54b 44589
[Frege1879] p. 50Proposition 51frege51 44551
[Frege1879] p. 50Proposition 52dfsbcq 3745
[Frege1879] p. 50Proposition 53frege53a 44556  frege53aid 44555  frege53b 44586  frege53c 44610
[Frege1879] p. 50Proposition 54biid 264  eqid 2761
[Frege1879] p. 50Proposition 55frege55a 44564  frege55aid 44561  frege55b 44593  frege55c 44614  frege55cor1a 44565  frege55lem2a 44563  frege55lem2b 44592  frege55lem2c 44613
[Frege1879] p. 50Proposition 56frege56a 44567  frege56aid 44566  frege56b 44594  frege56c 44615
[Frege1879] p. 51Axiom 58ax-frege58a 44571  ax-frege58b 44597  frege58bid 44598  frege58c 44617
[Frege1879] p. 51Proposition 57frege57a 44569  frege57aid 44568  frege57b 44595  frege57c 44616
[Frege1879] p. 51Proposition 58spsbc 3756
[Frege1879] p. 51Proposition 59frege59a 44573  frege59b 44600  frege59c 44618
[Frege1879] p. 52Proposition 60frege60a 44574  frege60b 44601  frege60c 44619
[Frege1879] p. 52Proposition 61frege61a 44575  frege61b 44602  frege61c 44620
[Frege1879] p. 52Proposition 62frege62a 44576  frege62b 44603  frege62c 44621
[Frege1879] p. 52Proposition 63frege63a 44577  frege63b 44604  frege63c 44622
[Frege1879] p. 53Proposition 64frege64a 44578  frege64b 44605  frege64c 44623
[Frege1879] p. 53Proposition 65frege65a 44579  frege65b 44606  frege65c 44624
[Frege1879] p. 54Proposition 66frege66a 44580  frege66b 44607  frege66c 44625
[Frege1879] p. 54Proposition 67frege67a 44581  frege67b 44608  frege67c 44626
[Frege1879] p. 54Proposition 68frege68a 44582  frege68b 44609  frege68c 44627
[Frege1879] p. 55Definition 69dffrege69 44628
[Frege1879] p. 58Proposition 70frege70 44629
[Frege1879] p. 59Proposition 71frege71 44630
[Frege1879] p. 59Proposition 72frege72 44631
[Frege1879] p. 59Proposition 73frege73 44632
[Frege1879] p. 60Definition 76dffrege76 44635
[Frege1879] p. 60Proposition 74frege74 44633
[Frege1879] p. 60Proposition 75frege75 44634
[Frege1879] p. 62Proposition 77frege77 44636  frege77d 44442
[Frege1879] p. 63Proposition 78frege78 44637
[Frege1879] p. 63Proposition 79frege79 44638
[Frege1879] p. 63Proposition 80frege80 44639
[Frege1879] p. 63Proposition 81frege81 44640  frege81d 44443
[Frege1879] p. 64Proposition 82frege82 44641
[Frege1879] p. 65Proposition 83frege83 44642  frege83d 44444
[Frege1879] p. 65Proposition 84frege84 44643
[Frege1879] p. 66Proposition 85frege85 44644
[Frege1879] p. 66Proposition 86frege86 44645
[Frege1879] p. 66Proposition 87frege87 44646  frege87d 44446
[Frege1879] p. 67Proposition 88frege88 44647
[Frege1879] p. 68Proposition 89frege89 44648
[Frege1879] p. 68Proposition 90frege90 44649
[Frege1879] p. 68Proposition 91frege91 44650  frege91d 44447
[Frege1879] p. 69Proposition 92frege92 44651
[Frege1879] p. 70Proposition 93frege93 44652
[Frege1879] p. 70Proposition 94frege94 44653
[Frege1879] p. 70Proposition 95frege95 44654
[Frege1879] p. 71Definition 99dffrege99 44658
[Frege1879] p. 71Proposition 96frege96 44655  frege96d 44445
[Frege1879] p. 71Proposition 97frege97 44656  frege97d 44448
[Frege1879] p. 71Proposition 98frege98 44657  frege98d 44449
[Frege1879] p. 72Proposition 100frege100 44659
[Frege1879] p. 72Proposition 101frege101 44660
[Frege1879] p. 72Proposition 102frege102 44661  frege102d 44450
[Frege1879] p. 73Proposition 103frege103 44662
[Frege1879] p. 73Proposition 104frege104 44663
[Frege1879] p. 73Proposition 105frege105 44664
[Frege1879] p. 73Proposition 106frege106 44665  frege106d 44451
[Frege1879] p. 74Proposition 107frege107 44666
[Frege1879] p. 74Proposition 108frege108 44667  frege108d 44452
[Frege1879] p. 74Proposition 109frege109 44668  frege109d 44453
[Frege1879] p. 75Proposition 110frege110 44669
[Frege1879] p. 75Proposition 111frege111 44670  frege111d 44455
[Frege1879] p. 76Proposition 112frege112 44671
[Frege1879] p. 76Proposition 113frege113 44672
[Frege1879] p. 76Proposition 114frege114 44673  frege114d 44454
[Frege1879] p. 77Definition 115dffrege115 44674
[Frege1879] p. 77Proposition 116frege116 44675
[Frege1879] p. 78Proposition 117frege117 44676
[Frege1879] p. 78Proposition 118frege118 44677
[Frege1879] p. 78Proposition 119frege119 44678
[Frege1879] p. 78Proposition 120frege120 44679
[Frege1879] p. 79Proposition 121frege121 44680
[Frege1879] p. 79Proposition 122frege122 44681  frege122d 44456
[Frege1879] p. 79Proposition 123frege123 44682
[Frege1879] p. 80Proposition 124frege124 44683  frege124d 44457
[Frege1879] p. 81Proposition 125frege125 44684
[Frege1879] p. 81Proposition 126frege126 44685  frege126d 44458
[Frege1879] p. 82Proposition 127frege127 44686
[Frege1879] p. 83Proposition 128frege128 44687
[Frege1879] p. 83Proposition 129frege129 44688  frege129d 44459
[Frege1879] p. 84Proposition 130frege130 44689
[Frege1879] p. 85Proposition 131frege131 44690  frege131d 44460
[Frege1879] p. 86Proposition 132frege132 44691
[Frege1879] p. 86Proposition 133frege133 44692  frege133d 44461
[Fremlin1] p. 13Definition 111G (b)df-salgen 46997
[Fremlin1] p. 13Definition 111G (d)borelmbl 47320
[Fremlin1] p. 13Proposition 111G (b)salgenss 47020
[Fremlin1] p. 14Definition 112Aismea 47135
[Fremlin1] p. 15Remark 112B (d)psmeasure 47155
[Fremlin1] p. 15Property 112C (a)meadjun 47146  meadjunre 47160
[Fremlin1] p. 15Property 112C (b)meassle 47147
[Fremlin1] p. 15Property 112C (c)meaunle 47148
[Fremlin1] p. 16Property 112C (d)iundjiun 47144  meaiunle 47153  meaiunlelem 47152
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 47165  meaiuninc2 47166  meaiuninc3 47169  meaiuninc3v 47168  meaiunincf 47167  meaiuninclem 47164
[Fremlin1] p. 16Proposition 112C (f)meaiininc 47171  meaiininc2 47172  meaiininclem 47170
[Fremlin1] p. 19Theorem 113Ccaragen0 47190  caragendifcl 47198  caratheodory 47212  omelesplit 47202
[Fremlin1] p. 19Definition 113Aisome 47178  isomennd 47215  isomenndlem 47214
[Fremlin1] p. 19Remark 113B (c)omeunle 47200
[Fremlin1] p. 19Definition 112Dfcaragencmpl 47219  voncmpl 47305
[Fremlin1] p. 19Definition 113A (ii)omessle 47182
[Fremlin1] p. 20Theorem 113Ccarageniuncl 47207  carageniuncllem1 47205  carageniuncllem2 47206  caragenuncl 47197  caragenuncllem 47196  caragenunicl 47208
[Fremlin1] p. 21Remark 113Dcaragenel2d 47216
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 47210  caratheodorylem2 47211
[Fremlin1] p. 21Exercise 113Xacaragencmpl 47219
[Fremlin1] p. 23Lemma 114Bhoidmv1le 47278  hoidmv1lelem1 47275  hoidmv1lelem2 47276  hoidmv1lelem3 47277
[Fremlin1] p. 25Definition 114Eisvonmbl 47322
[Fremlin1] p. 29Lemma 115Bhoidmv1le 47278  hoidmvle 47284  hoidmvlelem1 47279  hoidmvlelem2 47280  hoidmvlelem3 47281  hoidmvlelem4 47282  hoidmvlelem5 47283  hsphoidmvle2 47269  hsphoif 47260  hsphoival 47263
[Fremlin1] p. 29Definition 1135 (b)hoicvr 47232
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 47240
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 47267  hoidmvn0val 47268  hoidmvval 47261  hoidmvval0 47271  hoidmvval0b 47274
[Fremlin1] p. 30Lemma 115Bhoiprodp1 47272  hsphoidmvle 47270
[Fremlin1] p. 30Definition 115Cdf-ovoln 47221  df-voln 47223
[Fremlin1] p. 30Proposition 115D (a)dmovn 47288  ovn0 47250  ovn0lem 47249  ovnf 47247  ovnome 47257  ovnssle 47245  ovnsslelem 47244  ovnsupge0 47241
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 47287  ovnhoilem1 47285  ovnhoilem2 47286  vonhoi 47351
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 47304  hoidifhspf 47302  hoidifhspval 47292  hoidifhspval2 47299  hoidifhspval3 47303  hspmbl 47313  hspmbllem1 47310  hspmbllem2 47311  hspmbllem3 47312
[Fremlin1] p. 31Definition 115Evoncmpl 47305  vonmea 47258
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 47256  ovnsubadd2 47330  ovnsubadd2lem 47329  ovnsubaddlem1 47254  ovnsubaddlem2 47255
[Fremlin1] p. 32Proposition 115G (a)hoimbl 47315  hoimbl2 47349  hoimbllem 47314  hspdifhsp 47300  opnvonmbl 47318  opnvonmbllem2 47317
[Fremlin1] p. 32Proposition 115G (b)borelmbl 47320
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 47363  iccvonmbllem 47362  ioovonmbl 47361
[Fremlin1] p. 32Proposition 115G (d)vonicc 47369  vonicclem2 47368  vonioo 47366  vonioolem2 47365  vonn0icc 47372  vonn0icc2 47376  vonn0ioo 47371  vonn0ioo2 47374
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 47373  snvonmbl 47370  vonct 47377  vonsn 47375
[Fremlin1] p. 35Lemma 121Asubsalsal 47043
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 47042  subsaliuncllem 47041
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 47409  salpreimalegt 47393  salpreimaltle 47410
[Fremlin1] p. 35Proposition 121B (i)issmf 47412  issmff 47418  issmflem 47411
[Fremlin1] p. 35Proposition 121B (ii)issmfle 47429  issmflelem 47428  smfpreimale 47438
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 47440  issmfgtlem 47439
[Fremlin1] p. 36Definition 121Cdf-smblfn 47380  issmf 47412  issmff 47418  issmfge 47454  issmfgelem 47453  issmfgt 47440  issmfgtlem 47439  issmfle 47429  issmflelem 47428  issmflem 47411
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 47391  salpreimagtlt 47414  salpreimalelt 47413
[Fremlin1] p. 36Proposition 121B (iv)issmfge 47454  issmfgelem 47453
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 47437
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 47435  cnfsmf 47424
[Fremlin1] p. 36Proposition 121D (c)decsmf 47451  decsmflem 47450  incsmf 47426  incsmflem 47425
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 47385  pimconstlt1 47386  smfconst 47433
[Fremlin1] p. 37Proposition 121E (b)smfadd 47449  smfaddlem1 47447  smfaddlem2 47448
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 47480
[Fremlin1] p. 37Proposition 121E (d)smfmul 47479  smfmullem1 47475  smfmullem2 47476  smfmullem3 47477  smfmullem4 47478
[Fremlin1] p. 37Proposition 121E (e)smfdiv 47481
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 47484  smfpimbor1lem2 47483
[Fremlin1] p. 37Proposition 121E (g)smfco 47486
[Fremlin1] p. 37Proposition 121E (h)smfres 47474
[Fremlin1] p. 38Proposition 121E (e)smfrec 47473
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 47482  smfresal 47472
[Fremlin1] p. 38Proposition 121F (a)smflim 47461  smflim2 47490  smflimlem1 47455  smflimlem2 47456  smflimlem3 47457  smflimlem4 47458  smflimlem5 47459  smflimlem6 47460  smflimmpt 47494
[Fremlin1] p. 38Proposition 121F (b)smfsup 47498  smfsuplem1 47495  smfsuplem2 47496  smfsuplem3 47497  smfsupmpt 47499  smfsupxr 47500
[Fremlin1] p. 38Proposition 121F (c)smfinf 47502  smfinflem 47501  smfinfmpt 47503
[Fremlin1] p. 39Remark 121Gsmflim 47461  smflim2 47490  smflimmpt 47494
[Fremlin1] p. 39Proposition 121Fsmfpimcc 47492
[Fremlin1] p. 39Proposition 121Hsmfdivdmmbl 47522  smfdivdmmbl2 47525  smfinfdmmbl 47533  smfinfdmmbllem 47532  smfsupdmmbl 47529  smfsupdmmbllem 47528
[Fremlin1] p. 39Proposition 121F (d)smflimsup 47512  smflimsuplem2 47505  smflimsuplem6 47509  smflimsuplem7 47510  smflimsuplem8 47511  smflimsupmpt 47513
[Fremlin1] p. 39Proposition 121F (e)smfliminf 47515  smfliminflem 47514  smfliminfmpt 47516
[Fremlin1] p. 80Definition 135E (b)df-smblfn 47380
[Fremlin1], p. 38Proposition 121F (b)fsupdm 47526  fsupdm2 47527
[Fremlin1], p. 39Proposition 121Hadddmmbl 47517  adddmmbl2 47518  finfdm 47530  finfdm2 47531  fsupdm 47526  fsupdm2 47527  muldmmbl 47519  muldmmbl2 47520
[Fremlin1], p. 39Proposition 121F (c)finfdm 47530  finfdm2 47531
[Fremlin5] p. 193Proposition 563Gbnulmbl2 25674
[Fremlin5] p. 213Lemma 565Cauniioovol 25717
[Fremlin5] p. 214Lemma 565Cauniioombl 25727
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 38315
[Fremlin5] p. 220Theorem 565Maftc1anc 38318
[FreydScedrov] p. 283Axiom of Infinityax-inf 9606  inf1 9590  inf2 9591
[Gleason] p. 117Proposition 9-2.1df-enq 10895  enqer 10905
[Gleason] p. 117Proposition 9-2.2df-1nq 10900  df-nq 10896
[Gleason] p. 117Proposition 9-2.3df-plpq 10892  df-plq 10898
[Gleason] p. 119Proposition 9-2.4caovmo 7647  df-mpq 10893  df-mq 10899
[Gleason] p. 119Proposition 9-2.5df-rq 10901
[Gleason] p. 119Proposition 9-2.6ltexnq 10959
[Gleason] p. 120Proposition 9-2.6(i)halfnq 10960  ltbtwnnq 10962
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 10955
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 10956
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 10963
[Gleason] p. 121Definition 9-3.1df-np 10965
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 10977
[Gleason] p. 121Definition 9-3.1(iii)prnmax 10979
[Gleason] p. 122Definitiondf-1p 10966
[Gleason] p. 122Remark (1)prub 10978
[Gleason] p. 122Lemma 9-3.4prlem934 11017
[Gleason] p. 122Proposition 9-3.2df-ltp 10969
[Gleason] p. 122Proposition 9-3.3ltsopr 11016  psslinpr 11015  supexpr 11038  suplem1pr 11036  suplem2pr 11037
[Gleason] p. 123Proposition 9-3.5addclpr 11002  addclprlem1 11000  addclprlem2 11001  df-plp 10967
[Gleason] p. 123Proposition 9-3.5(i)addasspr 11006
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 11005
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 11018
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 11027  ltexprlem1 11020  ltexprlem2 11021  ltexprlem3 11022  ltexprlem4 11023  ltexprlem5 11024  ltexprlem6 11025  ltexprlem7 11026
[Gleason] p. 123Proposition 9-3.5(v)ltapr 11029  ltaprlem 11028
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 11030
[Gleason] p. 124Lemma 9-3.6prlem936 11031
[Gleason] p. 124Proposition 9-3.7df-mp 10968  mulclpr 11004  mulclprlem 11003  reclem2pr 11032
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 11013
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 11008
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 11007
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 11012
[Gleason] p. 124Proposition 9-3.7(v)recexpr 11035  reclem3pr 11033  reclem4pr 11034
[Gleason] p. 126Proposition 9-4.1df-enr 11039  enrer 11047
[Gleason] p. 126Proposition 9-4.2df-0r 11044  df-1r 11045  df-nr 11040
[Gleason] p. 126Proposition 9-4.3df-mr 11042  df-plr 11041  negexsr 11086  recexsr 11091  recexsrlem 11087
[Gleason] p. 127Proposition 9-4.4df-ltr 11043
[Gleason] p. 130Proposition 10-1.3creui 12212  creur 12211  cru 12209
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 11172  axcnre 11148
[Gleason] p. 132Definition 10-3.1crim 15166  crimd 15283  crimi 15244  crre 15165  crred 15282  crrei 15243
[Gleason] p. 132Definition 10-3.2remim 15168  remimd 15249
[Gleason] p. 133Definition 10.36absval2 15335  absval2d 15499  absval2i 15449
[Gleason] p. 133Proposition 10-3.4(a)cjadd 15192  cjaddd 15271  cjaddi 15239
[Gleason] p. 133Proposition 10-3.4(c)cjmul 15193  cjmuld 15272  cjmuli 15240
[Gleason] p. 133Proposition 10-3.4(e)cjcj 15191  cjcjd 15250  cjcji 15222
[Gleason] p. 133Proposition 10-3.4(f)cjre 15190  cjreb 15174  cjrebd 15253  cjrebi 15225  cjred 15277  rere 15173  rereb 15171  rerebd 15252  rerebi 15224  rered 15275
[Gleason] p. 133Proposition 10-3.4(h)addcj 15199  addcjd 15263  addcji 15234
[Gleason] p. 133Proposition 10-3.7(a)absval 15289
[Gleason] p. 133Proposition 10-3.7(b)abscj 15330  abscjd 15504  abscji 15453
[Gleason] p. 133Proposition 10-3.7(c)abs00 15340  abs00d 15500  abs00i 15450  absne0d 15501
[Gleason] p. 133Proposition 10-3.7(d)releabs 15373  releabsd 15505  releabsi 15454
[Gleason] p. 133Proposition 10-3.7(f)absmul 15345  absmuld 15508  absmuli 15456
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 15333  sqabsaddi 15457
[Gleason] p. 133Proposition 10-3.7(h)abstri 15382  abstrid 15510  abstrii 15460
[Gleason] p. 134Definition 10-4.1df-exp 14098  exp0 14101  expp1 14104  expp1d 14183
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 26820  cxpaddd 26858  expadd 14140  expaddd 14184  expaddz 14142
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 26829  cxpmuld 26878  expmul 14143  expmuld 14185  expmulz 14144
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 26826  mulcxpd 26869  mulexp 14137  mulexpd 14197  mulexpz 14138
[Gleason] p. 140Exercise 1znnen 16267
[Gleason] p. 141Definition 11-2.1fzval 13536
[Gleason] p. 168Proposition 12-2.1(a)climadd 15683  rlimadd 15694  rlimdiv 15697
[Gleason] p. 168Proposition 12-2.1(b)climsub 15685  rlimsub 15695
[Gleason] p. 168Proposition 12-2.1(c)climmul 15684  rlimmul 15696
[Gleason] p. 171Corollary 12-2.2climmulc2 15688
[Gleason] p. 172Corollary 12-2.5climrecl 15634
[Gleason] p. 172Proposition 12-2.4(c)climabs 15655  climcj 15656  climim 15658  climre 15657  rlimabs 15660  rlimcj 15661  rlimim 15663  rlimre 15662
[Gleason] p. 173Definition 12-3.1df-ltxr 11247  df-xr 11246  ltxr 13139
[Gleason] p. 175Definition 12-4.1df-limsup 15522  limsupval 15525
[Gleason] p. 180Theorem 12-5.1climsup 15721
[Gleason] p. 180Theorem 12-5.3caucvg 15730  caucvgb 15731  caucvgbf 46173  caucvgr 15727  climcau 15722
[Gleason] p. 182Exercise 3cvgcmp 15868
[Gleason] p. 182Exercise 4cvgrat 15937
[Gleason] p. 195Theorem 13-2.12abs1m 15387
[Gleason] p. 217Lemma 13-4.1btwnzge0 13861
[Gleason] p. 223Definition 14-1.1df-met 21495
[Gleason] p. 223Definition 14-1.1(a)met0 24479  xmet0 24478
[Gleason] p. 223Definition 14-1.1(b)metgt0 24495
[Gleason] p. 223Definition 14-1.1(c)metsym 24486
[Gleason] p. 223Definition 14-1.1(d)mettri 24488  mstri 24605  xmettri 24487  xmstri 24604
[Gleason] p. 225Definition 14-1.5xpsmet 24518
[Gleason] p. 230Proposition 14-2.6txlm 23784
[Gleason] p. 240Theorem 14-4.3metcnp4 25448
[Gleason] p. 240Proposition 14-4.2metcnp3 24676
[Gleason] p. 243Proposition 14-4.16addcn 25002  addcn2 15645  mulcn 25004  mulcn2 15647  subcn 25003  subcn2 15646
[Gleason] p. 295Remarkbcval3 14342  bcval4 14343
[Gleason] p. 295Equation 2bcpasc 14357
[Gleason] p. 295Definition of binomial coefficientbcval 14340  df-bc 14339
[Gleason] p. 296Remarkbcn0 14346  bcnn 14348
[Gleason] p. 296Theorem 15-2.8binom 15884
[Gleason] p. 308Equation 2ef0 16144
[Gleason] p. 308Equation 3efcj 16145
[Gleason] p. 309Corollary 15-4.3efne0 16151
[Gleason] p. 309Corollary 15-4.4efexp 16156
[Gleason] p. 310Equation 14sinadd 16219
[Gleason] p. 310Equation 15cosadd 16220
[Gleason] p. 311Equation 17sincossq 16231
[Gleason] p. 311Equation 18cosbnd 16236  sinbnd 16235
[Gleason] p. 311Lemma 15-4.7sqeqor 14252  sqeqori 14250
[Gleason] p. 311Definition of ` `df-pi 16125
[Godowski] p. 730Equation SFgoeqi 32591
[GodowskiGreechie] p. 249Equation IV3oai 31986
[Golan] p. 1Remarksrgisid 20290
[Golan] p. 1Definitiondf-srg 20268
[Golan] p. 149Definitiondf-slmd 33487
[Gonshor] p. 7Definitiondf-cuts 27929
[Gonshor] p. 9Theorem 2.5lesrec 27968  lesrecd 27969
[Gonshor] p. 10Theorem 2.6cofcut1 28089  cofcut1d 28090
[Gonshor] p. 10Theorem 2.7cofcut2 28091  cofcut2d 28092
[Gonshor] p. 12Theorem 2.9cofcutr 28093  cofcutr1d 28094  cofcutr2d 28095
[Gonshor] p. 13Definitiondf-adds 28129
[Gonshor] p. 14Theorem 3.1addsprop 28145
[Gonshor] p. 15Theorem 3.2addsunif 28171
[Gonshor] p. 17Theorem 3.4mulsprop 28299
[Gonshor] p. 18Theorem 3.5mulsunif 28319
[Gonshor] p. 28Lemma 4.2halfcut 28627
[Gonshor] p. 28Theorem 4.2pw2cut 28629
[Gonshor] p. 30Theorem 4.2addhalfcut 28628
[Gonshor] p. 39Theorem 4.4(b)elreno2 28664
[Gonshor] p. 95Theorem 6.1addbday 28187
[GramKnuthPat], p. 47Definition 2.42df-fwddif 36617
[Gratzer] p. 23Section 0.6df-mre 17637
[Gratzer] p. 27Section 0.6df-mri 17639
[Hall] p. 1Section 1.1df-asslaw 48920  df-cllaw 48918  df-comlaw 48919
[Hall] p. 2Section 1.2df-clintop 48932
[Hall] p. 7Section 1.3df-sgrp2 48953
[Halmos] p. 28Partition ` `df-parts 39485  dfmembpart2 39490
[Halmos] p. 31Theorem 17.3riesz1 32383  riesz2 32384
[Halmos] p. 41Definition of Hermitianhmopadj2 32259
[Halmos] p. 42Definition of projector orderingpjordi 32491
[Halmos] p. 43Theorem 26.1elpjhmop 32503  elpjidm 32502  pjnmopi 32466
[Halmos] p. 44Remarkpjinormi 32005  pjinormii 31994
[Halmos] p. 44Theorem 26.2elpjch 32507  pjrn 32025  pjrni 32020  pjvec 32014
[Halmos] p. 44Theorem 26.3pjnorm2 32045
[Halmos] p. 44Theorem 26.4hmopidmpj 32472  hmopidmpji 32470
[Halmos] p. 45Theorem 27.1pjinvari 32509
[Halmos] p. 45Theorem 27.3pjoci 32498  pjocvec 32015
[Halmos] p. 45Theorem 27.4pjorthcoi 32487
[Halmos] p. 48Theorem 29.2pjssposi 32490
[Halmos] p. 48Theorem 29.3pjssdif1i 32493  pjssdif2i 32492
[Halmos] p. 50Definition of spectrumdf-spec 32173
[Hamilton] p. 28Definition 2.1ax-1 6
[Hamilton] p. 31Example 2.7(a)idALT 24
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1823
[Hatcher] p. 25Definitiondf-phtpc 25130  df-phtpy 25109
[Hatcher] p. 26Definitiondf-pco 25143  df-pi1 25146
[Hatcher] p. 26Proposition 1.2phtpcer 25133
[Hatcher] p. 26Proposition 1.3pi1grp 25188
[Hefferon] p. 240Definition 3.12df-dmat 22626  df-dmatalt 49145
[Helfgott] p. 2Theoremtgoldbach 48549
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 48534
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 48546  bgoldbtbnd 48541  bgoldbtbnd 48541  tgblthelfgott 48547
[Helfgott] p. 5Proposition 1.1circlevma 34995
[Helfgott] p. 69Statement 7.49circlemethhgt 34996
[Helfgott] p. 69Statement 7.50hgt750lema 35010  hgt750lemb 35009  hgt750leme 35011  hgt750lemf 35006  hgt750lemg 35007
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 48543  tgoldbachgt 35016  tgoldbachgtALTV 48544  tgoldbachgtd 35015
[Helfgott] p. 70Statement 7.49ax-hgt749 34997
[Herstein] p. 54Exercise 28df-grpo 30811
[Herstein] p. 55Lemma 2.2.1(a)grpideu 19010  grpoideu 30827  mndideu 18802
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 19040  grpoinveu 30837
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 19071  grpo2inv 30849
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 19083  grpoinvop 30851
[Herstein] p. 57Exercise 1dfgrp3e 19105
[Hitchcock] p. 5Rule A3mptnan 1796
[Hitchcock] p. 5Rule A4mptxor 1797
[Hitchcock] p. 5Rule A5mtpxor 1799
[Holland] p. 1519Theorem 2sumdmdi 32738
[Holland] p. 1520Lemma 5cdj1i 32751  cdj3i 32759  cdj3lem1 32752  cdjreui 32750
[Holland] p. 1524Lemma 7mddmdin0i 32749
[Holland95] p. 13Theorem 3.6hlathil 42703
[Holland95] p. 14Line 15hgmapvs 42633
[Holland95] p. 14Line 16hdmaplkr 42655
[Holland95] p. 14Line 17hdmapellkr 42656
[Holland95] p. 14Line 19hdmapglnm2 42653
[Holland95] p. 14Line 20hdmapip0com 42659
[Holland95] p. 14Theorem 3.6hdmapevec2 42578
[Holland95] p. 14Lines 24 and 25hdmapoc 42673
[Holland95] p. 204Definition of involutiondf-srng 20922
[Holland95] p. 212Definition of subspacedf-psubsp 40245
[Holland95] p. 214Lemma 3.3lclkrlem2v 42270
[Holland95] p. 214Definition 3.2df-lpolN 42223
[Holland95] p. 214Definition of nonsingularpnonsingN 40675
[Holland95] p. 215Lemma 3.3(1)dihoml4 42119  poml4N 40695
[Holland95] p. 215Lemma 3.3(2)dochexmid 42210  pexmidALTN 40720  pexmidN 40711
[Holland95] p. 218Theorem 3.6lclkr 42275
[Holland95] p. 218Definition of dual vector spacedf-ldual 39866  ldualset 39867
[Holland95] p. 222Item 1df-lines 40243  df-pointsN 40244
[Holland95] p. 222Item 2df-polarityN 40645
[Holland95] p. 223Remarkispsubcl2N 40689  omllaw4 39988  pol1N 40652  polcon3N 40659
[Holland95] p. 223Definitiondf-psubclN 40677
[Holland95] p. 223Equation for polaritypolval2N 40648
[Holmes] p. 40Definitiondf-xrn 38997
[Hughes] p. 44Equation 1.21bax-his3 31402
[Hughes] p. 47Definition of projection operatordfpjop 32500
[Hughes] p. 49Equation 1.30eighmre 32281  eigre 32153  eigrei 32152
[Hughes] p. 49Equation 1.31eighmorth 32282  eigorth 32156  eigorthi 32155
[Hughes] p. 137Remark (ii)eigposi 32154
[Huneke] p. 1Claim 1frgrncvvdeq 30626
[Huneke] p. 1Statement 1frgrncvvdeqlem7 30622
[Huneke] p. 1Statement 2frgrncvvdeqlem8 30623
[Huneke] p. 1Statement 3frgrncvvdeqlem9 30624
[Huneke] p. 2Claim 2frgrregorufr 30642  frgrregorufr0 30641  frgrregorufrg 30643
[Huneke] p. 2Claim 3frgrhash2wsp 30649  frrusgrord 30658  frrusgrord0 30657
[Huneke] p. 2Statementdf-clwwlknon 30405
[Huneke] p. 2Statement 4frgrwopreglem4 30632
[Huneke] p. 2Statement 5frgrwopreg1 30635  frgrwopreg2 30636  frgrwopregasn 30633  frgrwopregbsn 30634
[Huneke] p. 2Statement 6frgrwopreglem5 30638
[Huneke] p. 2Statement 7fusgreghash2wspv 30652
[Huneke] p. 2Statement 8fusgreghash2wsp 30655
[Huneke] p. 2Statement 9clwlksndivn 30403  numclwlk1 30688  numclwlk1lem1 30686  numclwlk1lem2 30687  numclwwlk1 30678  numclwwlk8 30709
[Huneke] p. 2Definition 3frgrwopreglem1 30629
[Huneke] p. 2Definition 4df-clwlks 30086
[Huneke] p. 2Definition 62clwwlk 30664
[Huneke] p. 2Definition 7numclwwlkovh 30690  numclwwlkovh0 30689
[Huneke] p. 2Statement 10numclwwlk2 30698
[Huneke] p. 2Statement 11rusgrnumwlkg 30295
[Huneke] p. 2Statement 12numclwwlk3 30702
[Huneke] p. 2Statement 13numclwwlk5 30705
[Huneke] p. 2Statement 14numclwwlk7 30708
[Indrzejczak] p. 33Definition ` `Enatded 30720  natded 30720
[Indrzejczak] p. 33Definition ` `Inatded 30720
[Indrzejczak] p. 34Definition ` `Enatded 30720  natded 30720
[Indrzejczak] p. 34Definition ` `Inatded 30720
[Jech] p. 4Definition of classcv 1567  cvjust 2755
[Jech] p. 42Lemma 6.1alephexp1 10563
[Jech] p. 42Equation 6.1alephadd 10561  alephmul 10562
[Jech] p. 43Lemma 6.2infmap 10560  infmap2 10199
[Jech] p. 71Lemma 9.3jech9.3 9785
[Jech] p. 72Equation 9.3scott0 9859  scottex 9858
[Jech] p. 72Exercise 9.1rankval4 9838  rankval4b 35459
[Jech] p. 72Scheme "Collection Principle"cp 9876
[Jech] p. 78Noteopthprc 5725
[JonesMatijasevic] p. 694Definition 2.3rmxyval 43612
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 43700
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 43701
[JonesMatijasevic] p. 695Equation 2.7rmxadd 43624
[JonesMatijasevic] p. 695Equation 2.8rmyadd 43628
[JonesMatijasevic] p. 695Equation 2.9rmxp1 43629  rmyp1 43630
[JonesMatijasevic] p. 695Equation 2.10rmxm1 43631  rmym1 43632
[JonesMatijasevic] p. 695Equation 2.11rmx0 43622  rmx1 43623  rmxluc 43633
[JonesMatijasevic] p. 695Equation 2.12rmy0 43626  rmy1 43627  rmyluc 43634
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 43636
[JonesMatijasevic] p. 695Equation 2.14rmydbl 43637
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 43657  jm2.17b 43658  jm2.17c 43659
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 43690
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 43694
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 43685
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 43660  jm2.24nn 43656
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 43699
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 43705  rmygeid 43661
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 43717
[Juillerat] p. 11Section *5etransc 46967  etransclem47 46965  etransclem48 46966
[Juillerat] p. 12Equation (7)etransclem44 46962
[Juillerat] p. 12Equation *(7)etransclem46 46964
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 46950
[Juillerat] p. 13Proofetransclem35 46953
[Juillerat] p. 13Part of case 2 proven inetransclem38 46956
[Juillerat] p. 13Part of case 2 provenetransclem24 46942
[Juillerat] p. 13Part of case 2: proven inetransclem41 46959
[Juillerat] p. 14Proofetransclem23 46941
[KalishMontague] p. 81Note 1ax-6 1995
[KalishMontague] p. 85Lemma 2equid 2040
[KalishMontague] p. 85Lemma 3equcomi 2045
[KalishMontague] p. 86Lemma 7cbvalivw 2035  cbvaliw 2034  wl-cbvmotv 38134  wl-motae 38136  wl-moteq 38135
[KalishMontague] p. 87Lemma 8spimvw 2014  spimw 1998
[KalishMontague] p. 87Lemma 9spfw 2061  spw 2062
[Kalmbach] p. 14Definition of latticechabs1 31834  chabs1i 31836  chabs2 31835  chabs2i 31837  chjass 31851  chjassi 31804  latabs1 18530  latabs2 18531
[Kalmbach] p. 15Definition of atomdf-at 32656  ela 32657
[Kalmbach] p. 15Definition of coverscvbr2 32601  cvrval2 40016
[Kalmbach] p. 16Definitiondf-ol 39920  df-oml 39921
[Kalmbach] p. 20Definition of commutescmbr 31902  cmbri 31908  cmtvalN 39953  df-cm 31901  df-cmtN 39919
[Kalmbach] p. 22Remarkomllaw5N 39989  pjoml5 31931  pjoml5i 31906
[Kalmbach] p. 22Definitionpjoml2 31929  pjoml2i 31903
[Kalmbach] p. 22Theorem 2(v)cmcm 31932  cmcmi 31910  cmcmii 31915  cmtcomN 39991
[Kalmbach] p. 22Theorem 2(ii)omllaw3 39987  omlsi 31722  pjoml 31754  pjomli 31753
[Kalmbach] p. 22Definition of OML lawomllaw2N 39986
[Kalmbach] p. 23Remarkcmbr2i 31914  cmcm3 31933  cmcm3i 31912  cmcm3ii 31917  cmcm4i 31913  cmt3N 39993  cmt4N 39994  cmtbr2N 39995
[Kalmbach] p. 23Lemma 3cmbr3 31926  cmbr3i 31918  cmtbr3N 39996
[Kalmbach] p. 25Theorem 5fh1 31936  fh1i 31939  fh2 31937  fh2i 31940  omlfh1N 40000
[Kalmbach] p. 65Remarkchjatom 32675  chslej 31816  chsleji 31776  shslej 31698  shsleji 31688
[Kalmbach] p. 65Proposition 1chocin 31813  chocini 31772  chsupcl 31658  chsupval2 31728  h0elch 31573  helch 31561  hsupval2 31727  ocin 31614  ococss 31611  shococss 31612
[Kalmbach] p. 65Definition of subspace sumshsval 31630
[Kalmbach] p. 66Remarkdf-pjh 31713  pjssmi 32483  pjssmii 31999
[Kalmbach] p. 67Lemma 3osum 31963  osumi 31960
[Kalmbach] p. 67Lemma 4pjci 32518
[Kalmbach] p. 103Exercise 6atmd2 32718
[Kalmbach] p. 103Exercise 12mdsl0 32628
[Kalmbach] p. 140Remarkhatomic 32678  hatomici 32677  hatomistici 32680
[Kalmbach] p. 140Proposition 1atlatmstc 40061
[Kalmbach] p. 140Proposition 1(i)atexch 32699  lsatexch 39785
[Kalmbach] p. 140Proposition 1(ii)chcv1 32673  cvlcvr1 40081  cvr1 40152
[Kalmbach] p. 140Proposition 1(iii)cvexch 32692  cvexchi 32687  cvrexch 40162
[Kalmbach] p. 149Remark 2chrelati 32682  hlrelat 40144  hlrelat5N 40143  lrelat 39756
[Kalmbach] p. 153Exercise 5lsmcv 21244  lsmsatcv 39752  spansncv 31971  spansncvi 31970
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 39771  spansncv2 32611
[Kalmbach] p. 266Definitiondf-st 32529
[Kalmbach2] p. 8Definition of adjointdf-adjh 32167
[KanamoriPincus] p. 415Theorem 1.1fpwwe 10630  fpwwe2 10627
[KanamoriPincus] p. 416Corollary 1.3canth4 10631
[KanamoriPincus] p. 417Corollary 1.6canthp1 10638
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 10633
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 10635
[KanamoriPincus] p. 418Proposition 1.7pwfseq 10648
[KanamoriPincus] p. 419Lemma 2.2gchdjuidm 10652  gchxpidm 10653
[KanamoriPincus] p. 419Theorem 2.1gchacg 10664  gchhar 10663
[KanamoriPincus] p. 420Lemma 2.3pwdjudom 10197  unxpwdom 9550
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 10654
[Kreyszig] p. 3Property M1metcl 24468  xmetcl 24467
[Kreyszig] p. 4Property M2meteq0 24475
[Kreyszig] p. 8Definition 1.1-8dscmet 24708
[Kreyszig] p. 12Equation 5conjmul 11931  muleqadd 11857
[Kreyszig] p. 18Definition 1.3-2mopnval 24574
[Kreyszig] p. 19Remarkmopntopon 24575
[Kreyszig] p. 19Theorem T1mopn0 24634  mopnm 24580
[Kreyszig] p. 19Theorem T2unimopn 24632
[Kreyszig] p. 19Definition of neighborhoodneibl 24637
[Kreyszig] p. 20Definition 1.3-3metcnp2 24678
[Kreyszig] p. 25Definition 1.4-1lmbr 23394  lmmbr 25396  lmmbr2 25397
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 23516
[Kreyszig] p. 28Theorem 1.4-5lmcau 25451
[Kreyszig] p. 28Definition 1.4-3iscau 25414  iscmet2 25432
[Kreyszig] p. 30Theorem 1.4-7cmetss 25454
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 23597  metelcls 25443
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 25444  metcld2 25445
[Kreyszig] p. 51Equation 2clmvneg1 25237  lmodvneg1 21005  nvinv 30957  vcm 30894
[Kreyszig] p. 51Equation 1aclm0vs 25233  lmod0vs 20995  slmd0vs 33510  vc0 30892
[Kreyszig] p. 51Equation 1blmodvs0 20996  slmdvs0 33511  vcz 30893
[Kreyszig] p. 58Definition 2.2-1imsmet 31009  ngpmet 24739  nrmmetd 24710
[Kreyszig] p. 59Equation 1imsdval 31004  imsdval2 31005  ncvspds 25299  ngpds 24740
[Kreyszig] p. 63Problem 1nmval 24725  nvnd 31006
[Kreyszig] p. 64Problem 2nmeq0 24754  nmge0 24753  nvge0 30991  nvz 30987
[Kreyszig] p. 64Problem 3nmrtri 24760  nvabs 30990
[Kreyszig] p. 91Definition 2.7-1isblo3i 31119
[Kreyszig] p. 92Equation 2df-nmoo 31063
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 31125  blocni 31123
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 31124
[Kreyszig] p. 129Definition 3.1-1cphipeq0 25342  ipeq0 21767  ipz 31037
[Kreyszig] p. 135Problem 2cphpyth 25354  pythi 31168
[Kreyszig] p. 137Lemma 3-2.1(a)sii 31172
[Kreyszig] p. 137Lemma 3.2-1(a)ipcau 25376
[Kreyszig] p. 144Equation 4supcvg 15910
[Kreyszig] p. 144Theorem 3.3-1minvec 25574  minveco 31202
[Kreyszig] p. 196Definition 3.9-1df-aj 31068
[Kreyszig] p. 247Theorem 4.7-2bcth 25467
[Kreyszig] p. 249Theorem 4.7-3ubth 31191
[Kreyszig] p. 470Definition of positive operator orderingleop 32441  leopg 32440
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 32459
[Kreyszig] p. 525Theorem 10.1-1htth 31236
[Kulpa] p. 547Theorempoimir 38270
[Kulpa] p. 547Equation (1)poimirlem32 38269
[Kulpa] p. 547Equation (2)poimirlem31 38268
[Kulpa] p. 548Theorembroucube 38271
[Kulpa] p. 548Equation (6)poimirlem26 38263
[Kulpa] p. 548Equation (7)poimirlem27 38264
[Kunen] p. 10Axiom 0ax6e 2413  axnul 5267
[Kunen] p. 11Axiom 3axnul 5267
[Kunen] p. 12Axiom 6zfrep6 5249
[Kunen] p. 24Definition 10.24mapval 8834  mapvalg 8832
[Kunen] p. 30Lemma 10.20fodomg 10505
[Kunen] p. 31Definition 10.24mapex 7936
[Kunen] p. 95Definition 2.1df-r1 9735
[Kunen] p. 97Lemma 2.10r1elss 9777  r1elssi 9776
[Kunen] p. 107Exercise 4rankop 9829  rankopb 9823  rankuni 9834  rankxplim 9850  rankxpsuc 9853
[Kunen2] p. 47Lemma I.9.9relpfr 45633
[Kunen2] p. 53Lemma I.9.21trfr 45641
[Kunen2] p. 53Lemma I.9.24(2)wffr 45640
[Kunen2] p. 53Definition I.9.20tcfr 45642
[Kunen2] p. 95Lemma I.16.2ralabso 45647  rexabso 45648
[Kunen2] p. 96Example I.16.3disjabso 45654  n0abso 45655  ssabso 45653
[Kunen2] p. 111Lemma II.2.4(1)traxext 45656
[Kunen2] p. 111Lemma II.2.4(2)sswfaxreg 45666
[Kunen2] p. 111Lemma II.2.4(3)ssclaxsep 45661
[Kunen2] p. 111Lemma II.2.4(4)prclaxpr 45664
[Kunen2] p. 111Lemma II.2.4(5)uniclaxun 45665
[Kunen2] p. 111Lemma II.2.4(6)modelaxrep 45660
[Kunen2] p. 112Corollary II.2.5wfaxext 45672  wfaxpr 45677  wfaxreg 45679  wfaxrep 45673  wfaxsep 45674  wfaxun 45678
[Kunen2] p. 113Lemma II.2.8pwclaxpow 45663
[Kunen2] p. 113Corollary II.2.9wfaxpow 45676
[Kunen2] p. 114Theorem II.2.13wfaxext 45672
[Kunen2] p. 114Lemma II.2.11(7)modelac8prim 45671  omelaxinf2 45668
[Kunen2] p. 114Corollary II.2.12wfac8prim 45681  wfaxinf2 45680
[Kunen2] p. 148Exercise II.9.2nregmodelf1o 45694  permaxext 45684  permaxinf2 45692  permaxnul 45687  permaxpow 45688  permaxpr 45689  permaxrep 45685  permaxsep 45686  permaxun 45690
[Kunen2] p. 148Definition II.9.1brpermmodel 45682
[Kunen2] p. 149Exercise II.9.3permac8prim 45693
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4968
[Lang] , p. 225Corollary 1.3finexttrb 34021
[Lang] p. Definitiondf-rn 5672
[Lang] p. 3Statementlidrideqd 18726  mndbn0 18807
[Lang] p. 3Definitiondf-mnd 18792
[Lang] p. 4Definition of a (finite) productgsumsplit1r 18744
[Lang] p. 4Property of composites. Second formulagsumccat 18899
[Lang] p. 5Equationgsumreidx 19986
[Lang] p. 5Definition of an (infinite) productgsumfsupp 48914
[Lang] p. 6Examplenn0mnd 48911
[Lang] p. 6Equationgsumxp2 20049
[Lang] p. 6Statementcycsubm 19272
[Lang] p. 6Definitionmulgnn0gsum 19145
[Lang] p. 6Observationmndlsmidm 19739
[Lang] p. 7Definitiondfgrp2e 19029
[Lang] p. 30Definitiondf-tocyc 33393
[Lang] p. 32Property (a)cyc3genpm 33438
[Lang] p. 32Property (b)cyc3conja 33443  cycpmconjv 33428
[Lang] p. 53Definitiondf-cat 17723
[Lang] p. 53Axiom CAT 1cat1 18153  cat1lem 18152
[Lang] p. 54Definitiondf-iso 17805
[Lang] p. 57Definitiondf-inito 18040  df-termo 18041
[Lang] p. 58Exampleirinitoringc 21608
[Lang] p. 58Statementinitoeu1 18067  termoeu1 18074
[Lang] p. 62Definitiondf-func 17914
[Lang] p. 65Definitiondf-nat 18002
[Lang] p. 91Notedf-ringc 20730
[Lang] p. 92Statementmxidlprm 33719
[Lang] p. 92Definitionisprmidlc 21451
[Lang] p. 128Remarkdsmmlmod 21874
[Lang] p. 129Prooflincscm 49177  lincscmcl 49179  lincsum 49176  lincsumcl 49178
[Lang] p. 129Statementlincolss 49181
[Lang] p. 129Observationdsmmfi 21867
[Lang] p. 141Theorem 5.3dimkerim 33983  qusdimsum 33984
[Lang] p. 141Corollary 5.4lssdimle 33964
[Lang] p. 147Definitionsnlindsntor 49218
[Lang] p. 504Statementmat1 22583  matring 22579
[Lang] p. 504Definitiondf-mamu 22527
[Lang] p. 505Statementmamuass 22538  mamutpos 22594  matassa 22580  mattposvs 22591  tposmap 22593
[Lang] p. 513Definitionmdet1 22737  mdetf 22731
[Lang] p. 513Theorem 4.4cramer 22827
[Lang] p. 514Proposition 4.6mdetleib 22723
[Lang] p. 514Proposition 4.8mdettpos 22747
[Lang] p. 515Definitiondf-minmar1 22771  smadiadetr 22811
[Lang] p. 515Corollary 4.9mdetero 22746  mdetralt 22744
[Lang] p. 517Proposition 4.15mdetmul 22759
[Lang] p. 518Definitiondf-madu 22770
[Lang] p. 518Proposition 4.16madulid 22781  madurid 22780  matinv 22813
[Lang] p. 561Theorem 3.1cayleyhamilton 23026
[Lang], p. 190Chapter 6vieta 33936
[Lang], p. 224Proposition 1.1extdgfialg 34050  finextalg 34054
[Lang], p. 224Proposition 1.2extdgmul 34019  fedgmul 33987
[Lang], p. 225Proposition 1.4algextdeg 34081
[Lang], p. 561Remarkchpmatply1 22968
[Lang], p. 561Definitiondf-chpmat 22963
[Lang2] p. 3Notationsdf-ind 12218
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 45014
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 45009
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 45015
[LeBlanc] p. 277Rule R2axnul 5267
[Levy] p. 12Axiom 4.3.1df-clab 2740  wl-df.clab 38119
[Levy] p. 59Definitiondf-ttrcl 9676
[Levy] p. 64Theorem 5.6(ii)frinsg 9722
[Levy] p. 338Axiomdf-clel 2836  df-cleq 2753  wl-df.cleq 38120
[Levy] p. 338Axiom. See also comments under ~ df-clab , ~ df-cleq , and ~ eqabb . Alternate characterizationswl-df.clel 38123
[Levy] p. 357Definition extends to class variables a relation already valid for set variables, and is therefore conservative. This only sketches the conservativity arguement; for details see Appendixwl-df.clel 38123
[Levy] p. 357Proof sketch of conservativity; for details see Appendixdf-clel 2836  df-cleq 2753  wl-df.cleq 38120
[Levy] p. 357Statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ~ ax-ext , see Appendixdf-clab 2740  wl-df.clab 38119
[Levy] p. 358Axiomdf-clab 2740  wl-df.clab 38119
[Levy58] p. 2Definition Iisfin1-3 10369
[Levy58] p. 2Definition IIdf-fin2 10269
[Levy58] p. 2Definition Iadf-fin1a 10268
[Levy58] p. 2Definition IIIdf-fin3 10271
[Levy58] p. 3Definition Vdf-fin5 10272
[Levy58] p. 3Definition IVdf-fin4 10270
[Levy58] p. 4Definition VIdf-fin6 10273
[Levy58] p. 4Definition VIIdf-fin7 10274
[Levy58], p. 3Theorem 1fin1a2 10398
[Lipparini] p. 3Lemma 2.1.1nosepssdm 27826
[Lipparini] p. 3Lemma 2.1.4noresle 27837
[Lipparini] p. 6Proposition 4.2noinfbnd1 27869  nosupbnd1 27854
[Lipparini] p. 6Proposition 4.3noinfbnd2 27871  nosupbnd2 27856
[Lipparini] p. 7Theorem 5.1noetasuplem3 27875  noetasuplem4 27876
[Lipparini] p. 7Corollary 4.4nosupinfsep 27872
[Lopez-Astorga] p. 12Rule 1mptnan 1796
[Lopez-Astorga] p. 12Rule 2mptxor 1797
[Lopez-Astorga] p. 12Rule 3mtpxor 1799
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 32726
[Maeda] p. 168Lemma 5mdsym 32730  mdsymi 32729
[Maeda] p. 168Lemma 4(i)mdsymlem4 32724  mdsymlem6 32726  mdsymlem7 32727
[Maeda] p. 168Lemma 4(ii)mdsymlem8 32728
[MaedaMaeda] p. 1Remarkssdmd1 32631  ssdmd2 32632  ssmd1 32629  ssmd2 32630
[MaedaMaeda] p. 1Lemma 1.2mddmd2 32627
[MaedaMaeda] p. 1Definition 1.1df-dmd 32599  df-md 32598  mdbr 32612
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 32649  mdslj1i 32637  mdslj2i 32638  mdslle1i 32635  mdslle2i 32636  mdslmd1i 32647  mdslmd2i 32648
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 32639  mdsl2bi 32641  mdsl2i 32640
[MaedaMaeda] p. 2Lemma 1.6mdexchi 32653
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 32650
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 32651
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 32628
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 32633  mdsl3 32634
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 32652
[MaedaMaeda] p. 4Theorem 1.14mdcompli 32747
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 40063  hlrelat1 40142
[MaedaMaeda] p. 31Lemma 7.5lcvexch 39781
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 32654  cvmdi 32642  cvnbtwn4 32607  cvrnbtwn4 40021
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 32655
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 40082  cvp 32693  cvrp 40158  lcvp 39782
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 32717
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 32716
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 40075  hlexch4N 40134
[MaedaMaeda] p. 34Exercise 7.1atabsi 32719
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 40185
[MaedaMaeda] p. 61Definition 15.10psubN 40491  atpsubN 40495  df-pointsN 40244  pointpsubN 40493
[MaedaMaeda] p. 62Theorem 15.5df-pmap 40246  pmap11 40504  pmaple 40503  pmapsub 40510  pmapval 40499
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 40507  pmap1N 40509
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 40512  pmapglb2N 40513  pmapglb2xN 40514  pmapglbx 40511
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 40594
[MaedaMaeda] p. 67Postulate PS1ps-1 40219
[MaedaMaeda] p. 68Lemma 16.2df-padd 40538  paddclN 40584  paddidm 40583
[MaedaMaeda] p. 68Condition PS2ps-2 40220
[MaedaMaeda] p. 68Equation 16.2.1paddass 40580
[MaedaMaeda] p. 69Lemma 16.4ps-1 40219
[MaedaMaeda] p. 69Theorem 16.4ps-2 40220
[MaedaMaeda] p. 70Theorem 16.9lsmmod 19744  lsmmod2 19745  lssats 39754  shatomici 32676  shatomistici 32679  shmodi 31708  shmodsi 31707
[MaedaMaeda] p. 130Remark 29.6dmdmd 32618  mdsymlem7 32727
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 31907
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 31811
[MaedaMaeda] p. 139Remarksumdmdii 32733
[Margaris] p. 40Rule Cexlimiv 1958
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 401  df-ex 1808  df-or 861  dfbi2 479
[Margaris] p. 51Theorem 1idALT 24
[Margaris] p. 56Theorem 3conventions 30717
[Margaris] p. 59Section 14notnotrALTVD 45593
[Margaris] p. 60Theorem 8jcn 163
[Margaris] p. 60Section 14con3ALTVD 45594
[Margaris] p. 79Rule Cexinst01 45304  exinst11 45305
[Margaris] p. 89Theorem 19.219.2 2004  19.2g 2222  r19.2z 4459
[Margaris] p. 89Theorem 19.319.3 2236  rr19.3v 3625
[Margaris] p. 89Theorem 19.5alcom 2192
[Margaris] p. 89Theorem 19.6alex 1854
[Margaris] p. 89Theorem 19.7alnex 1809
[Margaris] p. 89Theorem 19.819.8a 2215
[Margaris] p. 89Theorem 19.919.9 2239  19.9h 2319  exlimd 2252  exlimdh 2323
[Margaris] p. 89Theorem 19.11excom 2195  excomim 2196
[Margaris] p. 89Theorem 19.1219.12 2358
[Margaris] p. 90Section 19conventions-labels 30718  conventions-labels 30718  conventions-labels 30718  conventions-labels 30718
[Margaris] p. 90Theorem 19.14exnal 1855
[Margaris] p. 90Theorem 19.152albi 45058  albi 1846
[Margaris] p. 90Theorem 19.1619.16 2259
[Margaris] p. 90Theorem 19.1719.17 2260
[Margaris] p. 90Theorem 19.182exbi 45060  exbi 1875
[Margaris] p. 90Theorem 19.1919.19 2263
[Margaris] p. 90Theorem 19.202alim 45057  2alimdv 1946  alimd 2246  alimdh 1845  alimdv 1944  ax-4 1837  ralimdaa 3264  ralimdv 3177  ralimdva 3175  ralimdvva 3210  sbcimdv 3811
[Margaris] p. 90Theorem 19.2119.21 2241  19.21h 2320  19.21t 2240  19.21vv 45056  alrimd 2249  alrimdd 2248  alrimdh 1891  alrimdv 1957  alrimi 2247  alrimih 1852  alrimiv 1955  alrimivv 1956  bj-alrimdh 37183  hbralrimi 3153  r19.21be 3256  r19.21bi 3255  ralrimd 3268  ralrimdv 3161  ralrimdva 3163  ralrimdvv 3207  ralrimdvva 3218  ralrimi 3261  ralrimia 3262  ralrimiv 3154  ralrimiva 3155  ralrimivv 3204  ralrimivva 3206  ralrimivvva 3209  ralrimivw 3159
[Margaris] p. 90Theorem 19.222exim 45059  2eximdv 1947  bj-exim 37198  exim 1862  eximd 2250  eximdh 1892  eximdv 1945  rexim 3104  reximd2a 3273  reximdai 3265  reximdd 45836  reximddv 3179  reximddv2 3222  reximddv3 3180  reximdv 3178  reximdv2 3173  reximdva 3176  reximdvai 3174  reximdvva 3211  reximi2 3096
[Margaris] p. 90Theorem 19.2319.23 2245  19.23bi 2225  19.23h 2321  19.23t 2244  exlimdv 1961  exlimdvv 1962  exlimexi 45203  exlimiv 1958  exlimivv 1960  rexlimd3 45832  rexlimdv 3162  rexlimdv3a 3168  rexlimdva 3164  rexlimdva2 3166  rexlimdvaa 3165  rexlimdvv 3219  rexlimdvva 3220  rexlimdvvva 3221  rexlimdvw 3169  rexlimiv 3157  rexlimiva 3156  rexlimivv 3205
[Margaris] p. 90Theorem 19.2419.24 2019
[Margaris] p. 90Theorem 19.2519.25 1908
[Margaris] p. 90Theorem 19.2619.26 1898
[Margaris] p. 90Theorem 19.2719.27 2261  r19.27z 4470  r19.27zv 4471
[Margaris] p. 90Theorem 19.2819.28 2262  19.28vv 45066  r19.28z 4462  r19.28zf 45847  r19.28zv 4466  rr19.28v 3626
[Margaris] p. 90Theorem 19.2919.29 1901  r19.29d2r 3150  r19.29imd 3128
[Margaris] p. 90Theorem 19.3019.30 1909
[Margaris] p. 90Theorem 19.3119.31 2268  19.31vv 45064
[Margaris] p. 90Theorem 19.3219.32 2267  r19.32 47802
[Margaris] p. 90Theorem 19.3319.33-2 45062  19.33 1912
[Margaris] p. 90Theorem 19.3419.34 2020
[Margaris] p. 90Theorem 19.3519.35 1905
[Margaris] p. 90Theorem 19.3619.36 2264  19.36vv 45063  r19.36zv 4472
[Margaris] p. 90Theorem 19.3719.37 2266  19.37vv 45065  r19.37zv 4467
[Margaris] p. 90Theorem 19.3819.38 1867
[Margaris] p. 90Theorem 19.3919.39 2018
[Margaris] p. 90Theorem 19.4019.40-2 1915  19.40 1914  r19.40 3129
[Margaris] p. 90Theorem 19.4119.41 2269  19.41rg 45229
[Margaris] p. 90Theorem 19.4219.42 2270
[Margaris] p. 90Theorem 19.4319.43 1910
[Margaris] p. 90Theorem 19.4419.44 2271  r19.44zv 4469
[Margaris] p. 90Theorem 19.4519.45 2272  r19.45zv 4468
[Margaris] p. 110Exercise 2(b)eu1 2636
[Mayet] p. 370Remarkjpi 32588  largei 32585  stri 32575
[Mayet3] p. 9Definition of CH-statesdf-hst 32530  ishst 32532
[Mayet3] p. 10Theoremhstrbi 32584  hstri 32583
[Mayet3] p. 1223Theorem 4.1mayete3i 32046
[Mayet3] p. 1240Theorem 7.1mayetes3i 32047
[MegPav2000] p. 2344Theorem 3.3stcltrthi 32596
[MegPav2000] p. 2345Definition 3.4-1chintcl 31650  chsupcl 31658
[MegPav2000] p. 2345Definition 3.4-2hatomic 32678
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 32672
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 32699
[MegPav2000] p. 2366Figure 7pl42N 40725
[MegPav2002] p. 362Lemma 2.2latj31 18542  latj32 18540  latjass 18538
[Megill] p. 444Axiom C5ax-5 1938  ax5ALT 39649
[Megill] p. 444Section 7conventions 30717
[Megill] p. 445Lemma L12aecom-o 39643  ax-c11n 39630  axc11n 2456
[Megill] p. 446Lemma L17equtrr 2050
[Megill] p. 446Lemma L18ax6fromc10 39638
[Megill] p. 446Lemma L19hbnae-o 39670  hbnae 2462
[Megill] p. 447Remark 9.1dfsb1 2511  sbid 2289  sbidd-misc 50464  sbidd 50463
[Megill] p. 448Remark 9.6axc14 2493
[Megill] p. 448Scheme C4'ax-c4 39626
[Megill] p. 448Scheme C5'ax-c5 39625  sp 2217
[Megill] p. 448Scheme C6'ax-11 2190
[Megill] p. 448Scheme C7'ax-c7 39627
[Megill] p. 448Scheme C8'ax-7 2036
[Megill] p. 448Scheme C9'ax-c9 39632
[Megill] p. 448Scheme C10'ax-6 1995  ax-c10 39628
[Megill] p. 448Scheme C11'ax-c11 39629
[Megill] p. 448Scheme C12'ax-8 2143
[Megill] p. 448Scheme C13'ax-9 2151
[Megill] p. 448Scheme C14'ax-c14 39633
[Megill] p. 448Scheme C15'ax-c15 39631
[Megill] p. 448Scheme C16'ax-c16 39634
[Megill] p. 448Theorem 9.4dral1-o 39646  dral1 2469  dral2-o 39672  dral2 2468  drex1 2471  drex2 2472  drsb1 2525  drsb2 2300
[Megill] p. 449Theorem 9.7sbcom2 2205  sbequ 2115  sbid2v 2539
[Megill] p. 450Example in Appendixhba1-o 39639  hba1 2326
[Mendelson] p. 35Axiom A3hirstL-ax3 47596
[Mendelson] p. 36Lemma 1.8idALT 24
[Mendelson] p. 69Axiom 4rspsbc 3831  rspsbca 3832  stdpc4 2100
[Mendelson] p. 69Axiom 5ax-c4 39626  ra4 3838  stdpc5 2242
[Mendelson] p. 81Rule Cexlimiv 1958
[Mendelson] p. 95Axiom 6stdpc6 2056
[Mendelson] p. 95Axiom 7stdpc7 2284
[Mendelson] p. 225Axiom system NBGru 3742
[Mendelson] p. 230Exercise 4.8(b)opthwiener 5497
[Mendelson] p. 231Exercise 4.10(k)inv1 4354
[Mendelson] p. 231Exercise 4.10(l)unv 4355
[Mendelson] p. 231Exercise 4.10(n)dfin3 4229
[Mendelson] p. 231Exercise 4.10(o)df-nul 4286
[Mendelson] p. 231Exercise 4.10(q)dfin4 4230
[Mendelson] p. 231Exercise 4.10(s)ddif 4094
[Mendelson] p. 231Definition of uniondfun3 4228
[Mendelson] p. 235Exercise 4.12(c)univ 5432
[Mendelson] p. 235Exercise 4.12(d)pwv 4868
[Mendelson] p. 235Exercise 4.12(j)pwin 5552
[Mendelson] p. 235Exercise 4.12(k)pwunss 4579
[Mendelson] p. 235Exercise 4.12(l)pwssun 5553
[Mendelson] p. 235Exercise 4.12(n)uniin 4895
[Mendelson] p. 235Exercise 4.12(p)reli 5813
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 6270
[Mendelson] p. 244Proposition 4.8(g)epweon 7773
[Mendelson] p. 246Definition of successordf-suc 6366
[Mendelson] p. 250Exercise 4.36oelim2 8580
[Mendelson] p. 254Proposition 4.22(b)xpen 9127
[Mendelson] p. 254Proposition 4.22(c)xpsnen 9048  xpsneng 9049
[Mendelson] p. 254Proposition 4.22(d)xpcomen 9055  xpcomeng 9056
[Mendelson] p. 254Proposition 4.22(e)xpassen 9058
[Mendelson] p. 255Definitionbrsdom 8970
[Mendelson] p. 255Exercise 4.39endisj 9051
[Mendelson] p. 255Exercise 4.41mapprc 8827
[Mendelson] p. 255Exercise 4.43mapsnen 9033  mapsnend 9032
[Mendelson] p. 255Exercise 4.45mapunen 9133
[Mendelson] p. 255Exercise 4.47xpmapen 9132
[Mendelson] p. 255Exercise 4.42(a)map0e 8879
[Mendelson] p. 255Exercise 4.42(b)map1 9036
[Mendelson] p. 257Proposition 4.24(a)undom 9052
[Mendelson] p. 258Exercise 4.56(c)djuassen 10161  djucomen 10160
[Mendelson] p. 258Exercise 4.56(f)djudom1 10165
[Mendelson] p. 258Exercise 4.56(g)xp2dju 10159
[Mendelson] p. 266Proposition 4.34(a)oa1suc 8515
[Mendelson] p. 266Proposition 4.34(f)oaordex 8542
[Mendelson] p. 275Proposition 4.42(d)entri3 10542
[Mendelson] p. 281Definitiondf-r1 9735
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 9784
[Mendelson] p. 287Axiom system MKru 3742
[MertziosUnger] p. 152Definitiondf-frgr 30576
[MertziosUnger] p. 153Remark 1frgrconngr 30611
[MertziosUnger] p. 153Remark 2vdgn1frgrv2 30613  vdgn1frgrv3 30614
[MertziosUnger] p. 153Remark 3vdgfrgrgt2 30615
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 30608
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 30601  2pthfrgrrn 30599  2pthfrgrrn2 30600
[Mittelstaedt] p. 9Definitiondf-oc 31570
[Monk1] p. 22Remarkconventions 30717
[Monk1] p. 22Theorem 3.1conventions 30717
[Monk1] p. 26Theorem 2.8(vii)ssin 4190
[Monk1] p. 33Theorem 3.2(i)ssrel 5769  ssrelf 32926
[Monk1] p. 33Theorem 3.2(ii)eqrel 5770
[Monk1] p. 34Definition 3.3df-opab 5173
[Monk1] p. 36Theorem 3.7(i)coi1 6264  coi2 6265
[Monk1] p. 36Theorem 3.8(v)dm0 5910  rn0 5916
[Monk1] p. 36Theorem 3.7(ii)cnvi 5871
[Monk1] p. 37Theorem 3.13(i)relxp 5679
[Monk1] p. 37Theorem 3.13(x)dmxp 5919  rnxp 6168
[Monk1] p. 37Theorem 3.13(ii)0xp 5760  xp0 5761
[Monk1] p. 38Theorem 3.16(ii)ima0 6079
[Monk1] p. 38Theorem 3.16(viii)imai 6076
[Monk1] p. 39Theorem 3.17imaex 7910  imaexg 7909
[Monk1] p. 39Theorem 3.16(xi)imassrn 6073
[Monk1] p. 41Theorem 4.3(i)fnopfv 7070  funfvop 7045
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6935
[Monk1] p. 42Theorem 4.4(iii)fvelima 6946
[Monk1] p. 43Theorem 4.6funun 6582
[Monk1] p. 43Theorem 4.8(iv)dff13 7252  dff13f 7253
[Monk1] p. 46Theorem 4.15(v)funex 7217  funrnex 7950
[Monk1] p. 50Definition 5.4fniunfv 7245
[Monk1] p. 52Theorem 5.12(ii)op2ndb 6228
[Monk1] p. 52Theorem 5.11(viii)ssint 4928
[Monk1] p. 52Definition 5.13 (i)1stval2 8002  df-1st 7985
[Monk1] p. 52Definition 5.13 (ii)2ndval2 8003  df-2nd 7986
[Monk1] p. 112Theorem 15.17(v)ranksn 9825  ranksnb 9798
[Monk1] p. 112Theorem 15.17(iv)rankuni2 9826
[Monk1] p. 112Theorem 15.17(iii)rankun 9827  rankunb 9821
[Monk1] p. 113Theorem 15.18r1val3 9809
[Monk1] p. 113Definition 15.19df-r1 9735  r1val2 9808
[Monk1] p. 117Lemmazorn2 10489  zorn2g 10486
[Monk1] p. 133Theorem 18.11cardom 9971
[Monk1] p. 133Theorem 18.12canth3 10544
[Monk1] p. 133Theorem 18.14carduni 9966
[Monk2] p. 105Axiom C4ax-4 1837
[Monk2] p. 105Axiom C7ax-7 2036
[Monk2] p. 105Axiom C8ax-12 2211  ax-c15 39631  ax12v2 2213
[Monk2] p. 108Lemma 5ax-c4 39626
[Monk2] p. 109Lemma 12ax-11 2190
[Monk2] p. 109Lemma 15equvini 2485  equvinv 2057  eqvinop 5469
[Monk2] p. 113Axiom C5-1ax-5 1938  ax5ALT 39649
[Monk2] p. 113Axiom C5-2ax-10 2174
[Monk2] p. 113Axiom C5-3ax-11 2190
[Monk2] p. 114Lemma 21sp 2217
[Monk2] p. 114Lemma 22axc4 2352  hba1-o 39639  hba1 2326
[Monk2] p. 114Lemma 23nfia1 2186
[Monk2] p. 114Lemma 24nfa2 2208  nfra2 3363  nfra2w 3299
[Moore] p. 53Part Idf-mre 17637
[Munkres] p. 77Example 2distop 23131  indistop 23138  indistopon 23137
[Munkres] p. 77Example 3fctop 23140  fctop2 23141
[Munkres] p. 77Example 4cctop 23142
[Munkres] p. 78Definition of basisdf-bases 23082  isbasis3g 23085
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 17495  tgval2 23092
[Munkres] p. 79Remarktgcl 23105
[Munkres] p. 80Lemma 2.1tgval3 23099
[Munkres] p. 80Lemma 2.2tgss2 23123  tgss3 23122
[Munkres] p. 81Lemma 2.3basgen 23124  basgen2 23125
[Munkres] p. 83Exercise 3topdifinf 37961  topdifinfeq 37962  topdifinffin 37960  topdifinfindis 37958
[Munkres] p. 89Definition of subspace topologyresttop 23296
[Munkres] p. 93Theorem 6.1(1)0cld 23174  topcld 23171
[Munkres] p. 93Theorem 6.1(2)iincld 23175
[Munkres] p. 93Theorem 6.1(3)uncld 23177
[Munkres] p. 94Definition of closureclsval 23173
[Munkres] p. 94Definition of interiorntrval 23172
[Munkres] p. 95Theorem 6.5(a)clsndisj 23211  elcls 23209
[Munkres] p. 95Theorem 6.5(b)elcls3 23219
[Munkres] p. 97Theorem 6.6clslp 23284  neindisj 23253
[Munkres] p. 97Corollary 6.7cldlp 23286
[Munkres] p. 97Definition of limit pointislp2 23281  lpval 23275
[Munkres] p. 98Definition of Hausdorff spacedf-haus 23451
[Munkres] p. 102Definition of continuous functiondf-cn 23363  iscn 23371  iscn2 23374
[Munkres] p. 107Theorem 7.2(g)cncnp 23416  cncnp2 23417  cncnpi 23414  df-cnp 23364  iscnp 23373  iscnp2 23375
[Munkres] p. 127Theorem 10.1metcn 24679
[Munkres] p. 128Theorem 10.3metcn4 25449
[Nathanson] p. 123Remarkreprgt 34974  reprinfz1 34975  reprlt 34972
[Nathanson] p. 123Definitiondf-repr 34962
[Nathanson] p. 123Chapter 5.1circlemethnat 34994
[Nathanson] p. 123Propositionbreprexp 34986  breprexpnat 34987  itgexpif 34959
[NielsenChuang] p. 195Equation 4.73unierri 32422
[OeSilva] p. 2042Section 2ax-bgbltosilva 48542
[Pfenning] p. 17Definition XMnatded 30720
[Pfenning] p. 17Definition NNCnatded 30720  notnotrd 134
[Pfenning] p. 17Definition ` `Cnatded 30720
[Pfenning] p. 18Rule"natded 30720
[Pfenning] p. 18Definition /\Inatded 30720
[Pfenning] p. 18Definition ` `Enatded 30720  natded 30720  natded 30720  natded 30720  natded 30720
[Pfenning] p. 18Definition ` `Inatded 30720  natded 30720  natded 30720  natded 30720  natded 30720
[Pfenning] p. 18Definition ` `ELnatded 30720
[Pfenning] p. 18Definition ` `ERnatded 30720
[Pfenning] p. 18Definition ` `Ea,unatded 30720
[Pfenning] p. 18Definition ` `IRnatded 30720
[Pfenning] p. 18Definition ` `Ianatded 30720
[Pfenning] p. 127Definition =Enatded 30720
[Pfenning] p. 127Definition =Inatded 30720
[Ponnusamy] p. 361Theorem 6.44cphip0l 25340  df-dip 31019  dip0l 31036  ip0l 21765
[Ponnusamy] p. 361Equation 6.45cphipval 25381  ipval 31021
[Ponnusamy] p. 362Equation I1dipcj 31032  ipcj 21763
[Ponnusamy] p. 362Equation I3cphdir 25343  dipdir 31160  ipdir 21768  ipdiri 31148
[Ponnusamy] p. 362Equation I4ipidsq 31028  nmsq 25332
[Ponnusamy] p. 362Equation 6.46ip0i 31143
[Ponnusamy] p. 362Equation 6.47ip1i 31145
[Ponnusamy] p. 362Equation 6.48ip2i 31146
[Ponnusamy] p. 363Equation I2cphass 25349  dipass 31163  ipass 21774  ipassi 31159
[Prugovecki] p. 186Definition of brabraval 32262  df-bra 32168
[Prugovecki] p. 376Equation 8.1df-kb 32169  kbval 32272
[PtakPulmannova] p. 66Proposition 3.2.17atomli 32700
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 40630
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 32714  atcvat4i 32715  cvrat3 40184  cvrat4 40185  lsatcvat3 39794
[PtakPulmannova] p. 68Definition 3.2.18cvbr 32600  cvrval 40011  df-cv 32597  df-lcv 39761  lspsncv0 21249
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 40642
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 40643
[Quine] p. 16Definition 2.1df-clab 2740  rabid 3435  rabidd 45843  wl-df.clab 38119
[Quine] p. 17Definition 2.1''dfsb7 2312
[Quine] p. 18Definition 2.7df-cleq 2753  wl-df.cleq 38120
[Quine] p. 19Definition 2.9conventions 30717  df-v 3455
[Quine] p. 34Theorem 5.1eqabb 2900
[Quine] p. 35Theorem 5.2abid1 2897  abid2f 2953
[Quine] p. 40Theorem 6.1sb5 2309
[Quine] p. 40Theorem 6.2sb6 2117  sbalex 2276
[Quine] p. 41Theorem 6.3df-clel 2836  wl-df.clel 38123
[Quine] p. 41Theorem 6.4eqid 2761  eqid1 30784
[Quine] p. 41Theorem 6.5eqcom 2768
[Quine] p. 42Theorem 6.6df-sbc 3744
[Quine] p. 42Theorem 6.7dfsbcq 3745  dfsbcq2 3746
[Quine] p. 43Theorem 6.8vex 3457
[Quine] p. 43Theorem 6.9isset 3467
[Quine] p. 44Theorem 7.3spcgf 3549  spcgv 3554  spcimgf 3517
[Quine] p. 44Theorem 6.11spsbc 3756  spsbcd 3757
[Quine] p. 44Theorem 6.12elex 3474
[Quine] p. 44Theorem 6.13elab 3637  elabg 3634  elabgf 3632
[Quine] p. 44Theorem 6.14noel 4290
[Quine] p. 48Theorem 7.2snprc 4682
[Quine] p. 48Definition 7.1df-pr 4591  df-sn 4589
[Quine] p. 49Theorem 7.4snss 4749  snssg 4748
[Quine] p. 49Theorem 7.5prss 4785  prssg 4784
[Quine] p. 49Theorem 7.6prid1 4727  prid1g 4725  prid2 4728  prid2g 4726  snid 4627  snidg 4625
[Quine] p. 51Theorem 7.12snex 5410
[Quine] p. 51Theorem 7.13prex 5409
[Quine] p. 53Theorem 8.2unisn 4890  unisnALT 45604  unisng 4889
[Quine] p. 53Theorem 8.3uniun 4894
[Quine] p. 54Theorem 8.6elssuni 4903
[Quine] p. 54Theorem 8.7uni0 4900
[Quine] p. 56Theorem 8.17uniabio 6506
[Quine] p. 56Definition 8.18dfaiota2 47790  dfiota2 6493
[Quine] p. 57Theorem 8.19aiotaval 47799  iotaval 6510
[Quine] p. 57Theorem 8.22iotanul 6516
[Quine] p. 58Theorem 8.23iotaex 6512
[Quine] p. 58Definition 9.1df-op 4595
[Quine] p. 61Theorem 9.5opabid 5509  opabidw 5508  opelopab 5527  opelopaba 5520  opelopabaf 5529  opelopabf 5530  opelopabg 5523  opelopabga 5517  opelopabgf 5525  oprabid 7442  oprabidw 7441
[Quine] p. 64Definition 9.11df-xp 5667
[Quine] p. 64Definition 9.12df-cnv 5669
[Quine] p. 64Definition 9.15df-id 5556
[Quine] p. 65Theorem 10.3fun0 6601
[Quine] p. 65Theorem 10.4funi 6568
[Quine] p. 65Theorem 10.5funsn 6589  funsng 6587
[Quine] p. 65Definition 10.1df-fun 6538
[Quine] p. 65Definition 10.2args 6094  dffv4 6878
[Quine] p. 68Definition 10.11conventions 30717  df-fv 6544  fv2 6876
[Quine] p. 124Theorem 17.3nn0opth2 14308  nn0opth2i 14307  nn0opthi 14306  omopthi 8646
[Quine] p. 177Definition 25.2df-rdg 8396
[Quine] p. 232Equation icarddom 10537
[Quine] p. 284Axiom 39(vi)funimaex 6623  funimaexg 6622
[Quine] p. 331Axiom system NFru 3742
[ReedSimon] p. 36Definition (iii)ax-his3 31402
[ReedSimon] p. 63Exercise 4(a)df-dip 31019  polid 31477  polid2i 31475  polidi 31476
[ReedSimon] p. 63Exercise 4(b)df-ph 31131
[ReedSimon] p. 195Remarklnophm 32337  lnophmi 32336
[Retherford] p. 49Exercise 1(i)leopadd 32450
[Retherford] p. 49Exercise 1(ii)leopmul 32452  leopmuli 32451
[Retherford] p. 49Exercise 1(iv)leoptr 32455
[Retherford] p. 49Definition VI.1df-leop 32170  leoppos 32444
[Retherford] p. 49Exercise 1(iii)leoptri 32454
[Retherford] p. 49Definition of operator orderingleop3 32443
[Ribenboim] p. 181Remarknprmdvdsfacm1 48343
[Ribenboim], p. 181Statementppivalnn 48351
[Roman] p. 4Definitiondf-dmat 22626  df-dmatalt 49145
[Roman] p. 18Part Preliminariesdf-rng 20230
[Roman] p. 19Part Preliminariesdf-ring 20316
[Roman] p. 46Theorem 1.6isldepslvec2 49232
[Roman] p. 112Noteisldepslvec2 49232  ldepsnlinc 49255  zlmodzxznm 49244
[Roman] p. 112Examplezlmodzxzequa 49243  zlmodzxzequap 49246  zlmodzxzldep 49251
[Roman] p. 170Theorem 7.8cayleyhamilton 23026
[Rosenlicht] p. 80Theoremheicant 38272
[Rosser] p. 281Definitiondf-op 4595
[RosserSchoenfeld] p. 71Theorem 12.ax-ros335 34998
[RosserSchoenfeld] p. 71Theorem 13.ax-ros336 34999
[Rotman] p. 28Remarkpgrpgt2nabl 49113  pmtr3ncom 19544
[Rotman] p. 31Theorem 3.4symggen2 19540
[Rotman] p. 42Theorem 3.15cayley 19483  cayleyth 19484
[Rudin] p. 164Equation 27efcan 16149
[Rudin] p. 164Equation 30efzval 16157
[Rudin] p. 167Equation 48absefi 16251
[Sanford] p. 39Remarkax-mp 5  mto 200
[Sanford] p. 39Rule 3mtpxor 1799
[Sanford] p. 39Rule 4mptxor 1797
[Sanford] p. 40Rule 1mptnan 1796
[Schechter] p. 51Definition of antisymmetryintasym 6115
[Schechter] p. 51Definition of irreflexivityintirr 6118
[Schechter] p. 51Definition of symmetrycnvsym 6114
[Schechter] p. 51Definition of transitivitycotr 6112
[Schechter] p. 78Definition of Moore collection of setsdf-mre 17637
[Schechter] p. 79Definition of Moore closuredf-mrc 17638
[Schechter] p. 82Section 4.5df-mrc 17638
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 17640
[Schechter] p. 139Definition AC3dfac9 10119
[Schechter] p. 141Definition (MC)dfac11 43759
[Schechter] p. 149Axiom DC1ax-dc 10429  axdc3 10437
[Schechter] p. 187Definition of "ring with unit"isring 20318  isrngo 38514
[Schechter] p. 276Remark 11.6.espan0 31860
[Schechter] p. 276Definition of spandf-span 31627  spanval 31651
[Schechter] p. 428Definition 15.35bastop1 23129
[Schloeder] p. 1Lemma 1.3onelon 6385  onelord 43948  ordelon 6384  ordelord 6382
[Schloeder] p. 1Lemma 1.7onepsuc 43949  sucidg 6444
[Schloeder] p. 1Remark 1.50elon 6416  onsuc 7808  ord0 6415  ordsuci 7806
[Schloeder] p. 1Theorem 1.9epsoon 43950
[Schloeder] p. 1Definition 1.1dftr5 5221
[Schloeder] p. 1Definition 1.2dford3 43725  elon2 6371
[Schloeder] p. 1Definition 1.4df-suc 6366
[Schloeder] p. 1Definition 1.6epel 5564  epelg 5562
[Schloeder] p. 1Theorem 1.9(i)elirr 9561  epirron 43951  ordirr 6378
[Schloeder] p. 1Theorem 1.9(ii)oneltr 43953  oneptr 43952  ontr1 6408
[Schloeder] p. 1Theorem 1.9(iii)oneltri 6404  oneptri 43954  ordtri3or 6393
[Schloeder] p. 2Lemma 1.10ondif1 8485  ord0eln0 6417
[Schloeder] p. 2Lemma 1.13elsuci 6430  onsucss 43963  trsucss 6451
[Schloeder] p. 2Lemma 1.14ordsucss 7813
[Schloeder] p. 2Lemma 1.15onnbtwn 6457  ordnbtwn 6456
[Schloeder] p. 2Lemma 1.16orddif0suc 43965  ordnexbtwnsuc 43964
[Schloeder] p. 2Lemma 1.17fin1a2lem2 10384  onsucf1lem 43966  onsucf1o 43969  onsucf1olem 43967  onsucrn 43968
[Schloeder] p. 2Lemma 1.18dflim7 43970
[Schloeder] p. 2Remark 1.12ordzsl 7840
[Schloeder] p. 2Theorem 1.10ondif1i 43959  ordne0gt0 43958
[Schloeder] p. 2Definition 1.11dflim6 43961  limnsuc 43962  onsucelab 43960
[Schloeder] p. 3Remark 1.21omex 9611
[Schloeder] p. 3Theorem 1.19tfinds 7855
[Schloeder] p. 3Theorem 1.22omelon 9614  ordom 7871
[Schloeder] p. 3Definition 1.20dfom3 9615
[Schloeder] p. 4Lemma 2.21onn 8625
[Schloeder] p. 4Lemma 2.7ssonuni 7778  ssorduni 7777
[Schloeder] p. 4Remark 2.4oa1suc 8515
[Schloeder] p. 4Theorem 1.23dfom5 9618  limom 7877
[Schloeder] p. 4Definition 2.1df-1o 8452  df1o2 8459
[Schloeder] p. 4Definition 2.3oa0 8500  oa0suclim 43972  oalim 8516  oasuc 8508
[Schloeder] p. 4Definition 2.5om0 8501  om0suclim 43973  omlim 8517  omsuc 8510
[Schloeder] p. 4Definition 2.6oe0 8506  oe0m1 8505  oe0suclim 43974  oelim 8518  oesuc 8511
[Schloeder] p. 5Lemma 2.10onsupuni 43926
[Schloeder] p. 5Lemma 2.11onsupsucismax 43976
[Schloeder] p. 5Lemma 2.12onsssupeqcond 43977
[Schloeder] p. 5Lemma 2.13limexissup 43978  limexissupab 43980  limiun 43979  limuni 6423
[Schloeder] p. 5Lemma 2.14oa0r 8522
[Schloeder] p. 5Lemma 2.15om1 8526  om1om1r 43981  om1r 8527
[Schloeder] p. 5Remark 2.8oacl 8519  oaomoecl 43975  oecl 8521  omcl 8520
[Schloeder] p. 5Definition 2.9onsupintrab 43928
[Schloeder] p. 6Lemma 2.16oe1 8528
[Schloeder] p. 6Lemma 2.17oe1m 8529
[Schloeder] p. 6Lemma 2.18oe0rif 43982
[Schloeder] p. 6Theorem 2.19oasubex 43983
[Schloeder] p. 6Theorem 2.20nnacl 8596  nnamecl 43984  nnecl 8598  nnmcl 8597
[Schloeder] p. 7Lemma 3.1onsucwordi 43985
[Schloeder] p. 7Lemma 3.2oaword1 8536
[Schloeder] p. 7Lemma 3.3oaword2 8537
[Schloeder] p. 7Lemma 3.4oalimcl 8544
[Schloeder] p. 7Lemma 3.5oaltublim 43987
[Schloeder] p. 8Lemma 3.6oaordi3 43988
[Schloeder] p. 8Lemma 3.81oaomeqom 43990
[Schloeder] p. 8Lemma 3.10oa00 8543
[Schloeder] p. 8Lemma 3.11omge1 43994  omword1 8557
[Schloeder] p. 8Remark 3.9oaordnr 43993  oaordnrex 43992
[Schloeder] p. 8Theorem 3.7oaord3 43989
[Schloeder] p. 9Lemma 3.12omge2 43995  omword2 8558
[Schloeder] p. 9Lemma 3.13omlim2 43996
[Schloeder] p. 9Lemma 3.14omord2lim 43997
[Schloeder] p. 9Lemma 3.15omord2i 43998  omordi 8550
[Schloeder] p. 9Theorem 3.16omord 8552  omord2com 43999
[Schloeder] p. 10Lemma 3.172omomeqom 44000  df-2o 8453
[Schloeder] p. 10Lemma 3.19oege1 44003  oewordi 8576
[Schloeder] p. 10Lemma 3.20oege2 44004  oeworde 8578
[Schloeder] p. 10Lemma 3.21rp-oelim2 44005
[Schloeder] p. 10Lemma 3.22oeord2lim 44006
[Schloeder] p. 10Remark 3.18omnord1 44002  omnord1ex 44001
[Schloeder] p. 11Lemma 3.23oeord2i 44007
[Schloeder] p. 11Lemma 3.25nnoeomeqom 44009
[Schloeder] p. 11Remark 3.26oenord1 44013  oenord1ex 44012
[Schloeder] p. 11Theorem 4.1oaomoencom 44014
[Schloeder] p. 11Theorem 4.2oaass 8545
[Schloeder] p. 11Theorem 3.24oeord2com 44008
[Schloeder] p. 12Theorem 4.3odi 8563
[Schloeder] p. 13Theorem 4.4omass 8564
[Schloeder] p. 14Remark 4.6oenass 44016
[Schloeder] p. 14Theorem 4.7oeoa 8582
[Schloeder] p. 15Lemma 5.1cantnftermord 44017
[Schloeder] p. 15Lemma 5.2cantnfub 44018  cantnfub2 44019
[Schloeder] p. 16Theorem 5.3cantnf2 44022
[Schwabhauser] p. 10Axiom A1axcgrrflx 29230  axtgcgrrflx 28707
[Schwabhauser] p. 10Axiom A2axcgrtr 29231
[Schwabhauser] p. 10Axiom A3axcgrid 29232  axtgcgrid 28708
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 28693
[Schwabhauser] p. 11Axiom A4axsegcon 29243  axtgsegcon 28709  df-trkgcb 28695
[Schwabhauser] p. 11Axiom A5ax5seg 29254  axtg5seg 28710  df-trkgcb 28695
[Schwabhauser] p. 11Axiom A6axbtwnid 29255  axtgbtwnid 28711  df-trkgb 28694
[Schwabhauser] p. 12Axiom A7axpasch 29257  axtgpasch 28712  df-trkgb 28694
[Schwabhauser] p. 12Axiom A8axlowdim2 29276  df-trkg2d 35018
[Schwabhauser] p. 13Axiom A8axtglowdim2 28715
[Schwabhauser] p. 13Axiom A9axtgupdim2 28716  df-trkg2d 35018
[Schwabhauser] p. 13Axiom A10axeuclid 29279  axtgeucl 28717  df-trkge 28696
[Schwabhauser] p. 13Axiom A11axcont 29292  axtgcont 28714  axtgcont1 28713  df-trkgb 28694
[Schwabhauser] p. 24Theorem A10prlngmo 29177
[Schwabhauser] p. 27Theorem 2.1cgrrflx 36445
[Schwabhauser] p. 27Theorem 2.2cgrcomim 36447
[Schwabhauser] p. 27Theorem 2.3cgrtr 36450
[Schwabhauser] p. 27Theorem 2.4cgrcoml 36454
[Schwabhauser] p. 27Theorem 2.5cgrcomr 36455  tgcgrcomimp 28722  tgcgrcoml 28724  tgcgrcomr 28723
[Schwabhauser] p. 28Theorem 2.8cgrtriv 36460  tgcgrtriv 28729
[Schwabhauser] p. 28Theorem 2.105segofs 36464  tg5segofs 35029
[Schwabhauser] p. 28Definition 2.10df-afs 35026  df-ofs 36441
[Schwabhauser] p. 29Theorem 2.11cgrextend 36466  tgcgrextend 28730
[Schwabhauser] p. 29Theorem 2.12segconeq 36468  tgsegconeq 28731
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 36480  btwntriv2 36470  tgbtwntriv2 28732
[Schwabhauser] p. 30Theorem 3.2btwncomim 36471  tgbtwncom 28733
[Schwabhauser] p. 30Theorem 3.3btwntriv1 36474  tgbtwntriv1 28736
[Schwabhauser] p. 30Theorem 3.4btwnswapid 36475  tgbtwnswapid 28737
[Schwabhauser] p. 30Theorem 3.5btwnexch2 36481  btwnintr 36477  tgbtwnexch2 28741  tgbtwnintr 28738
[Schwabhauser] p. 30Theorem 3.6btwnexch 36483  btwnexch3 36478  tgbtwnexch 28743  tgbtwnexch3 28739
[Schwabhauser] p. 30Theorem 3.7btwnouttr 36482  tgbtwnouttr 28742  tgbtwnouttr2 28740
[Schwabhauser] p. 32Theorem 3.13axlowdim1 29275
[Schwabhauser] p. 32Theorem 3.14btwndiff 36485  tgbtwndiff 28751
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 28744  trisegint 36486
[Schwabhauser] p. 34Theorem 4.2ifscgr 36502  tgifscgr 28753
[Schwabhauser] p. 34Theorem 4.11colcom 28803  colrot1 28804  colrot2 28805  lncom 28871  lnrot1 28872  lnrot2 28873
[Schwabhauser] p. 34Definition 4.1df-ifs 36498
[Schwabhauser] p. 35Theorem 4.3cgrsub 36503  tgcgrsub 28754
[Schwabhauser] p. 35Theorem 4.5cgrxfr 36513  tgcgrxfr 28763
[Schwabhauser] p. 35Statement 4.4ercgrg 28762
[Schwabhauser] p. 35Definition 4.4df-cgr3 36499  df-cgrg 28756
[Schwabhauser] p. 35Definition instead (givendf-cgrg 28756
[Schwabhauser] p. 36Theorem 4.6btwnxfr 36514  tgbtwnxfr 28775
[Schwabhauser] p. 36Theorem 4.11colinearperm1 36520  colinearperm2 36522  colinearperm3 36521  colinearperm4 36523  colinearperm5 36524
[Schwabhauser] p. 36Definition 4.8df-ismt 28778
[Schwabhauser] p. 36Definition 4.10df-colinear 36497  tgellng 28798  tglng 28791
[Schwabhauser] p. 37Theorem 4.12colineartriv1 36525
[Schwabhauser] p. 37Theorem 4.13colinearxfr 36533  lnxfr 28811
[Schwabhauser] p. 37Theorem 4.14lineext 36534  lnext 28812
[Schwabhauser] p. 37Theorem 4.16fscgr 36538  tgfscgr 28813
[Schwabhauser] p. 37Theorem 4.17linecgr 36539  lncgr 28814
[Schwabhauser] p. 37Definition 4.15df-fs 36500
[Schwabhauser] p. 38Theorem 4.18lineid 36541  lnid 28815
[Schwabhauser] p. 38Theorem 4.19idinside 36542  tgidinside 28816
[Schwabhauser] p. 39Theorem 5.1btwnconn1 36559  tgbtwnconn1 28820
[Schwabhauser] p. 41Theorem 5.2btwnconn2 36560  tgbtwnconn2 28821
[Schwabhauser] p. 41Theorem 5.3btwnconn3 36561  tgbtwnconn3 28822
[Schwabhauser] p. 41Theorem 5.5brsegle2 36567
[Schwabhauser] p. 41Definition 5.4df-segle 36565  legov 28830
[Schwabhauser] p. 41Definition 5.5legov2 28831
[Schwabhauser] p. 42Remark 5.13legso 28844
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 36568
[Schwabhauser] p. 42Theorem 5.7seglerflx 36570
[Schwabhauser] p. 42Theorem 5.8segletr 36572
[Schwabhauser] p. 42Theorem 5.9segleantisym 36573
[Schwabhauser] p. 42Theorem 5.10seglelin 36574
[Schwabhauser] p. 42Theorem 5.11seglemin 36571
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 36576
[Schwabhauser] p. 42Proposition 5.7legid 28832
[Schwabhauser] p. 42Proposition 5.8legtrd 28834
[Schwabhauser] p. 42Proposition 5.9legtri3 28835
[Schwabhauser] p. 42Proposition 5.10legtrid 28836
[Schwabhauser] p. 42Proposition 5.11leg0 28837
[Schwabhauser] p. 43Theorem 6.2btwnoutside 36583
[Schwabhauser] p. 43Theorem 6.3broutsideof3 36584
[Schwabhauser] p. 43Theorem 6.4broutsideof 36579  df-outsideof 36578
[Schwabhauser] p. 43Definition 6.1broutsideof2 36580  ishlg 28850
[Schwabhauser] p. 44Theorem 6.4hlln 28855
[Schwabhauser] p. 44Theorem 6.5hlid 28857  outsideofrflx 36585
[Schwabhauser] p. 44Theorem 6.6hlcomb 28851  hlcomd 28852  outsideofcom 36586
[Schwabhauser] p. 44Theorem 6.7hltr 28858  outsideoftr 36587
[Schwabhauser] p. 44Theorem 6.11hlcgreq 28867  hlcgreu 28866  outsideofeu 36589
[Schwabhauser] p. 44Definition 6.8df-ray 36596
[Schwabhauser] p. 45Part 2df-lines2 36597
[Schwabhauser] p. 45Theorem 6.13outsidele 36590
[Schwabhauser] p. 45Theorem 6.15lineunray 36605
[Schwabhauser] p. 45Theorem 6.16lineelsb2 36606  tglineelsb2 28881
[Schwabhauser] p. 45Theorem 6.17linecom 36608  linerflx1 36607  linerflx2 36609  tglinecom 28884  tglinerflx1 28882  tglinerflx2 28883
[Schwabhauser] p. 45Theorem 6.18linethru 36611  tglinethru 28885
[Schwabhauser] p. 45Definition 6.14df-line2 36595  tglng 28791
[Schwabhauser] p. 45Proposition 6.13legbtwn 28839
[Schwabhauser] p. 46Theorem 6.19linethrueu 36614  tglinethrueu 28888
[Schwabhauser] p. 46Theorem 6.21lineintmo 36615  tglineineq 28892  tglineinsn 28893  tglineinteq 28895  tglineintmo 28891
[Schwabhauser] p. 46Theorem 6.23colline 28899
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 28900
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 28901
[Schwabhauser] p. 49Theorem 7.3mirinv 28919
[Schwabhauser] p. 49Theorem 7.7mirmir 28915
[Schwabhauser] p. 49Theorem 7.8mirreu3 28907
[Schwabhauser] p. 49Definition 7.5df-mir 28906  ismir 28912  mirbtwn 28911  mircgr 28910  mirfv 28909  mirval 28908
[Schwabhauser] p. 50Theorem 7.8mirreu 28917
[Schwabhauser] p. 50Theorem 7.9mireq 28918
[Schwabhauser] p. 50Theorem 7.10mirinv 28919
[Schwabhauser] p. 50Theorem 7.11mirf1o 28922
[Schwabhauser] p. 50Theorem 7.13miriso 28923
[Schwabhauser] p. 51Theorem 7.14mirmot 28928
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 28925  mirbtwni 28924
[Schwabhauser] p. 51Theorem 7.16mircgrs 28926
[Schwabhauser] p. 51Theorem 7.17miduniq 28938
[Schwabhauser] p. 52Lemma 7.21symquadlem 28942
[Schwabhauser] p. 52Theorem 7.18miduniq1 28939
[Schwabhauser] p. 52Theorem 7.19miduniq2 28940
[Schwabhauser] p. 52Theorem 7.20colmid 28941
[Schwabhauser] p. 53Lemma 7.22krippen 28944
[Schwabhauser] p. 55Lemma 7.25midexlem 28945
[Schwabhauser] p. 57Theorem 8.2ragcom 28953
[Schwabhauser] p. 57Definition 8.1df-rag 28949  israg 28952
[Schwabhauser] p. 58Theorem 8.3ragcol 28954
[Schwabhauser] p. 58Theorem 8.4ragmir 28955
[Schwabhauser] p. 58Theorem 8.5ragtrivb 28957
[Schwabhauser] p. 58Theorem 8.6ragflat2 28958
[Schwabhauser] p. 58Theorem 8.7ragflat 28959
[Schwabhauser] p. 58Theorem 8.8ragtriva 28960
[Schwabhauser] p. 58Theorem 8.9ragflat3 28961  ragncol 28964
[Schwabhauser] p. 58Theorem 8.10ragcgr 28962
[Schwabhauser] p. 59Theorem 8.12perpcom 28968
[Schwabhauser] p. 59Theorem 8.13ragperp 28972
[Schwabhauser] p. 59Theorem 8.14perpneq 28969
[Schwabhauser] p. 59Definition 8.11df-perpg 28951  isperp 28967
[Schwabhauser] p. 59Definition 8.13isperp2 28970
[Schwabhauser] p. 60Theorem 8.18foot 28977
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 28986  colperpexlem2 28987
[Schwabhauser] p. 63Theorem 8.21colperpex 28989  colperpexlem3 28988
[Schwabhauser] p. 64Theorem 8.22mideu 28994  midex 28993
[Schwabhauser] p. 66Lemma 8.24opphllem 28991
[Schwabhauser] p. 67Theorem 9.2oppcom 29000
[Schwabhauser] p. 67Definition 9.1islnopp 28995
[Schwabhauser] p. 68Lemma 9.3opphllem2 29004
[Schwabhauser] p. 68Lemma 9.4opphllem5 29007  opphllem6 29008
[Schwabhauser] p. 69Theorem 9.5opphl 29010
[Schwabhauser] p. 69Theorem 9.6axtgpasch 28712
[Schwabhauser] p. 70Theorem 9.6outpasch 29012
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 29020
[Schwabhauser] p. 71Definition 9.7df-hpg 29015  hpgbr 29017
[Schwabhauser] p. 72Lemma 9.10hpgerlem 29022
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 29021
[Schwabhauser] p. 72Theorem 9.11hpgid 29023
[Schwabhauser] p. 72Theorem 9.12hpgcom 29024
[Schwabhauser] p. 72Theorem 9.13hpgtr 29025
[Schwabhauser] p. 73Theorem 9.18colopp 29026
[Schwabhauser] p. 73Theorem 9.19colhp 29027
[Schwabhauser] p. 74Lemma 9.22lnincplng 29040
[Schwabhauser] p. 74Theorem 9.21plngcp 29042
[Schwabhauser] p. 74Theorem 9.24plngrot 29046
[Schwabhauser] p. 74Definition 9.20df-plng 29030  elplng 29036
[Schwabhauser] p. 75Theorem 9.25lnssplng 29048  lnssplng1 29049
[Schwabhauser] p. 76Theorem 9.26plng3p 29053
[Schwabhauser] p. 88Theorem 10.2lmieu 29067
[Schwabhauser] p. 88Definition 10.1df-mid 29057
[Schwabhauser] p. 89Theorem 10.4lmicom 29071
[Schwabhauser] p. 89Theorem 10.5lmilmi 29072
[Schwabhauser] p. 89Theorem 10.6lmireu 29073
[Schwabhauser] p. 89Theorem 10.7lmieq 29074
[Schwabhauser] p. 89Theorem 10.8lmiinv 29075
[Schwabhauser] p. 89Theorem 10.9lmif1o 29078
[Schwabhauser] p. 89Theorem 10.10lmiiso 29080
[Schwabhauser] p. 89Definition 10.3df-lmi 29058
[Schwabhauser] p. 90Theorem 10.11lmimot 29081
[Schwabhauser] p. 91Theorem 10.12hypcgr 29084
[Schwabhauser] p. 92Theorem 10.14lmiopp 29085
[Schwabhauser] p. 92Theorem 10.15lnperpex 29086  lnperpexs 29087
[Schwabhauser] p. 92Theorem 10.16trgcopy 29088  trgcopyeu 29090
[Schwabhauser] p. 95Definition 11.2dfcgra2 29114
[Schwabhauser] p. 95Definition 11.3iscgra 29093
[Schwabhauser] p. 95Proposition 11.4cgracgr 29102
[Schwabhauser] p. 95Proposition 11.10cgrahl1 29100  cgrahl2 29101
[Schwabhauser] p. 96Theorem 11.6cgraid 29103
[Schwabhauser] p. 96Theorem 11.9cgraswap 29104
[Schwabhauser] p. 97Theorem 11.7cgracom 29106
[Schwabhauser] p. 97Theorem 11.8cgratr 29107
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 29110  cgrahl 29111
[Schwabhauser] p. 98Theorem 11.13sacgr 29115
[Schwabhauser] p. 98Theorem 11.14oacgr 29116
[Schwabhauser] p. 98Theorem 11.15acopy 29117  acopyeu 29118
[Schwabhauser] p. 98Theorem 11.16ragcgra 29119
[Schwabhauser] p. 98Theorem 11.17cgrarag 29120
[Schwabhauser] p. 98Theorem 11.18ragsupplcgra 29121
[Schwabhauser] p. 99Theorem 11.19ragraghl 29122
[Schwabhauser] p. 99Theorem 11.20perpeq 29124
[Schwabhauser] p. 101Theorem 11.24inagswap 29131
[Schwabhauser] p. 101Theorem 11.25inaghl 29135
[Schwabhauser] p. 101Definition 11.23isinag 29128
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 29143
[Schwabhauser] p. 102Definition 11.27df-leag 29136  isleag 29137
[Schwabhauser] p. 107Theorem 11.49tgsas 29145  tgsas1 29144  tgsas2 29146  tgsas3 29147
[Schwabhauser] p. 108Theorem 11.50tgasa 29149  tgasa1 29148
[Schwabhauser] p. 109Theorem 11.51tgsss1 29150  tgsss2 29151  tgsss3 29152
[Schwabhauser] p. 121Definition 12.2df-prlng 29160
[Schwabhauser] p. 122Theorem 12.4prlngref 29163
[Schwabhauser] p. 122Theorem 12.5prlngsym 29164
[Schwabhauser] p. 122Theorem 12.6prlnghpg 29169
[Schwabhauser] p. 122Theorem 12.7dfprlng2 29170  dfprlng3 29171
[Schwabhauser] p. 122Theorem 12.9perpprlng 29173
[Schwabhauser] p. 122Theorem 12.10prlngex 29174
[Schwabhauser] p. 123Theorem 12.11prlngmo 29177  prlngmo2 29179
[Schwabhauser] p. 124Theorem 12.13prlngeu 29178
[Schwabhauser] p. 124Theorem 12.14prlngpln4 29180
[Schwabhauser] p. 124Theorem 12.15prlngplngtr 29181
[Schwabhauser] p. 125Theorem 12.16prlnginn0 29182
[Schwabhauser] p. 125Theorem 12.17prlngmid2 29183
[Shapiro] p. 230Theorem 6.5.1dchrhash 27411  dchrsum 27409  dchrsum2 27408  sumdchr 27412
[Shapiro] p. 232Theorem 6.5.2dchr2sum 27413  sum2dchr 27414
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 20137  ablfacrp2 20138
[Shapiro], p. 328Equation 9.2.4vmasum 27356
[Shapiro], p. 329Equation 9.2.7logfac2 27357
[Shapiro], p. 329Equation 9.2.9logfacrlim 27364
[Shapiro], p. 331Equation 9.2.13vmadivsum 27622
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 27625
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 27679  vmalogdivsum2 27678
[Shapiro], p. 375Theorem 9.4.1dirith 27669  dirith2 27668
[Shapiro], p. 375Equation 9.4.3rplogsum 27667  rpvmasum 27666  rpvmasum2 27652
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 27627
[Shapiro], p. 376Equation 9.4.8dchrvmasum 27665
[Shapiro], p. 377Lemma 9.4.1dchrisum 27632  dchrisumlem1 27629  dchrisumlem2 27630  dchrisumlem3 27631  dchrisumlema 27628
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 27635
[Shapiro], p. 379Equation 9.4.16dchrmusum 27664  dchrmusumlem 27662  dchrvmasumlem 27663
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 27634
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 27636
[Shapiro], p. 382Lemma 9.4.4dchrisum0 27660  dchrisum0re 27653  dchrisumn0 27661
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 27646
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 27650
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 27651
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 27706  pntrsumbnd2 27707  pntrsumo1 27705
[Shapiro], p. 405Equation 10.2.1mudivsum 27670
[Shapiro], p. 406Equation 10.2.6mulogsum 27672
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 27674
[Shapiro], p. 407Equation 10.2.8mulog2sum 27677
[Shapiro], p. 418Equation 10.4.6logsqvma 27682
[Shapiro], p. 418Equation 10.4.8logsqvma2 27683
[Shapiro], p. 419Equation 10.4.10selberg 27688
[Shapiro], p. 420Equation 10.4.12selberg2lem 27690
[Shapiro], p. 420Equation 10.4.14selberg2 27691
[Shapiro], p. 422Equation 10.6.7selberg3 27699
[Shapiro], p. 422Equation 10.4.20selberg4lem1 27700
[Shapiro], p. 422Equation 10.4.21selberg3lem1 27697  selberg3lem2 27698
[Shapiro], p. 422Equation 10.4.23selberg4 27701
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 27695
[Shapiro], p. 428Equation 10.6.2selbergr 27708
[Shapiro], p. 429Equation 10.6.8selberg3r 27709
[Shapiro], p. 430Equation 10.6.11selberg4r 27710
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 27724
[Shapiro], p. 434Equation 10.6.27pntlema 27736  pntlemb 27737  pntlemc 27735  pntlemd 27734  pntlemg 27738
[Shapiro], p. 435Equation 10.6.29pntlema 27736
[Shapiro], p. 436Lemma 10.6.1pntpbnd 27728
[Shapiro], p. 436Lemma 10.6.2pntibnd 27733
[Shapiro], p. 436Equation 10.6.34pntlema 27736
[Shapiro], p. 436Equation 10.6.35pntlem3 27749  pntleml 27751
[Stewart] p. 91Lemma 7.3constrss 34099
[Stewart] p. 92Definition 7.4.df-constr 34086
[Stewart] p. 96Theorem 7.10constraddcl 34118  constrinvcl 34129  constrmulcl 34127  constrnegcl 34119  constrsqrtcl 34135
[Stewart] p. 97Theorem 7.11constrextdg2 34105
[Stewart] p. 98Theorem 7.12constrext2chn 34115
[Stewart] p. 99Theorem 7.132sqr3nconstr 34137
[Stewart] p. 99Theorem 7.14cos9thpinconstr 34147
[Stoll] p. 13Definition corresponds to dfsymdif3 4258
[Stoll] p. 16Exercise 4.40dif 4362  dif0 4333
[Stoll] p. 16Exercise 4.8difdifdir 4451
[Stoll] p. 17Theorem 5.1(5)unvdif 4435
[Stoll] p. 19Theorem 5.2(13)undm 4249
[Stoll] p. 19Theorem 5.2(13')indm 4250
[Stoll] p. 20Remarkinvdif 4231
[Stoll] p. 25Definition of ordered tripledf-ot 4597
[Stoll] p. 43Definitionuniiun 5022
[Stoll] p. 44Definitionintiin 5023
[Stoll] p. 45Definitiondf-iin 4958
[Stoll] p. 45Definition indexed uniondf-iun 4957
[Stoll] p. 176Theorem 3.4(27)iman 406
[Stoll] p. 262Example 4.1dfsymdif3 4258
[Strang] p. 242Section 6.3expgrowth 45015
[Suppes] p. 22Theorem 2eq0 4303  eq0f 4300
[Suppes] p. 22Theorem 4eqss 3951  eqssd 3953  eqssi 3952
[Suppes] p. 23Theorem 5ss0 4358  ss0b 4357
[Suppes] p. 23Theorem 6sstr 3944  sstrALT2 45513
[Suppes] p. 23Theorem 7pssirr 4056
[Suppes] p. 23Theorem 8pssn2lp 4058
[Suppes] p. 23Theorem 9psstr 4061
[Suppes] p. 23Theorem 10pssss 4051
[Suppes] p. 25Theorem 12elin 3920  elun 4106
[Suppes] p. 26Theorem 15inidm 4178
[Suppes] p. 26Theorem 16in0 4351
[Suppes] p. 27Theorem 23unidm 4110
[Suppes] p. 27Theorem 24un0 4350
[Suppes] p. 27Theorem 25ssun1 4130
[Suppes] p. 27Theorem 26ssequn1 4138
[Suppes] p. 27Theorem 27unss 4142
[Suppes] p. 27Theorem 28indir 4238
[Suppes] p. 27Theorem 29undir 4239
[Suppes] p. 28Theorem 32difid 4331
[Suppes] p. 29Theorem 33difin 4224
[Suppes] p. 29Theorem 34indif 4232
[Suppes] p. 29Theorem 35undif1 4436
[Suppes] p. 29Theorem 36difun2 4441
[Suppes] p. 29Theorem 37difin0 4434
[Suppes] p. 29Theorem 38disjdif 4432
[Suppes] p. 29Theorem 39difundi 4242
[Suppes] p. 29Theorem 40difindi 4244
[Suppes] p. 30Theorem 41nalset 5276
[Suppes] p. 39Theorem 61uniss 4879
[Suppes] p. 39Theorem 65uniop 5498
[Suppes] p. 41Theorem 70intsn 4948
[Suppes] p. 42Theorem 71intpr 4946  intprg 4945
[Suppes] p. 42Theorem 73op1stb 5453
[Suppes] p. 42Theorem 78intun 4944
[Suppes] p. 44Definition 15(a)dfiun2 4995  dfiun2g 4993
[Suppes] p. 44Definition 15(b)dfiin2 4996
[Suppes] p. 47Theorem 86elpw 4565  elpw2 5304  elpw2g 5303  elpwg 4564  elpwgdedVD 45595
[Suppes] p. 47Theorem 87pwid 4584
[Suppes] p. 47Theorem 89pw0 4777
[Suppes] p. 48Theorem 90pwpw0 4778
[Suppes] p. 52Theorem 101xpss12 5676
[Suppes] p. 52Theorem 102xpindi 5819  xpindir 5820
[Suppes] p. 52Theorem 103xpundi 5730  xpundir 5731
[Suppes] p. 54Theorem 105elirrv 9558
[Suppes] p. 58Theorem 2relss 5768
[Suppes] p. 59Theorem 4eldm 5890  eldm2 5891  eldm2g 5889  eldmg 5888
[Suppes] p. 59Definition 3df-dm 5671
[Suppes] p. 60Theorem 6dmin 5901
[Suppes] p. 60Theorem 8rnun 6142
[Suppes] p. 60Theorem 9rnin 6143
[Suppes] p. 60Definition 4dfrn2 5878
[Suppes] p. 61Theorem 11brcnv 5868  brcnvg 5865
[Suppes] p. 62Equation 5elcnv 5862  elcnv2 5863
[Suppes] p. 62Theorem 12relcnv 6106
[Suppes] p. 62Theorem 15cnvin 6141
[Suppes] p. 62Theorem 16cnvun 6139
[Suppes] p. 63Definitiondftrrels2 39276
[Suppes] p. 63Theorem 20co02 6262
[Suppes] p. 63Theorem 21dmcoss 5965
[Suppes] p. 63Definition 7df-co 5670
[Suppes] p. 64Theorem 26cnvco 5875
[Suppes] p. 64Theorem 27coass 6267
[Suppes] p. 65Theorem 31resundi 5992
[Suppes] p. 65Theorem 34elima 6067  elima2 6068  elima3 6069  elimag 6066
[Suppes] p. 65Theorem 35imaundi 6147
[Suppes] p. 66Theorem 40dminss 6150
[Suppes] p. 66Theorem 41imainss 6151
[Suppes] p. 67Exercise 11cnvxp 6154
[Suppes] p. 81Definition 34dfec2 8696
[Suppes] p. 82Theorem 72elec 8740  elecALTV 38888  elecg 8738
[Suppes] p. 82Theorem 73eqvrelth 39312  erth 8748  erth2 8749
[Suppes] p. 83Theorem 74eqvreldisj 39315  erdisj 8751
[Suppes] p. 83Definition 35, df-parts 39485  dfmembpart2 39490
[Suppes] p. 89Theorem 96map0b 8880
[Suppes] p. 89Theorem 97map0 8884  map0g 8881
[Suppes] p. 89Theorem 98mapsn 8885  mapsnd 8883
[Suppes] p. 89Theorem 99mapss 8886
[Suppes] p. 91Definition 12(ii)alephsuc 10051
[Suppes] p. 91Definition 12(iii)alephlim 10050
[Suppes] p. 92Theorem 1enref 8981  enrefg 8980
[Suppes] p. 92Theorem 2ensym 8999  ensymb 8998  ensymi 9000
[Suppes] p. 92Theorem 3entr 9002
[Suppes] p. 92Theorem 4unen 9041
[Suppes] p. 94Theorem 15endom 8975
[Suppes] p. 94Theorem 16ssdomg 8996
[Suppes] p. 94Theorem 17domtr 9003
[Suppes] p. 95Theorem 18sbth 9084
[Suppes] p. 97Theorem 23canth2 9117  canth2g 9118
[Suppes] p. 97Definition 3brsdom2 9088  df-sdom 8945  dfsdom2 9087
[Suppes] p. 97Theorem 21(i)sdomirr 9101
[Suppes] p. 97Theorem 22(i)domnsym 9090
[Suppes] p. 97Theorem 21(ii)sdomnsym 9089
[Suppes] p. 97Theorem 22(ii)domsdomtr 9099
[Suppes] p. 97Theorem 22(iv)brdom2 8978
[Suppes] p. 97Theorem 21(iii)sdomtr 9102
[Suppes] p. 97Theorem 22(iii)sdomdomtr 9097
[Suppes] p. 98Exercise 4fundmen 9027  fundmeng 9028
[Suppes] p. 98Exercise 6xpdom3 9062
[Suppes] p. 98Exercise 11sdomentr 9098
[Suppes] p. 104Theorem 37fofi 9272
[Suppes] p. 104Theorem 38pwfi 9277
[Suppes] p. 105Theorem 40pwfi 9277
[Suppes] p. 111Axiom for cardinal numberscarden 10534
[Suppes] p. 130Definition 3df-tr 5218
[Suppes] p. 132Theorem 9ssonuni 7778
[Suppes] p. 134Definition 6df-suc 6366
[Suppes] p. 136Theorem Schema 22findes 7896  finds 7892  finds1 7895  finds2 7894
[Suppes] p. 151Theorem 42isfinite 9620  isfinite2 9257  isfiniteg 9259  unbnn 9255
[Suppes] p. 162Definition 5df-ltnq 10902  df-ltpq 10894
[Suppes] p. 197Theorem Schema 4tfindes 7858  tfinds 7855  tfinds2 7859
[Suppes] p. 209Theorem 18oaord1 8535
[Suppes] p. 209Theorem 21oaword2 8537
[Suppes] p. 211Theorem 25oaass 8545
[Suppes] p. 225Definition 8iscard2 9961
[Suppes] p. 227Theorem 56ondomon 10546
[Suppes] p. 228Theorem 59harcard 9963
[Suppes] p. 228Definition 12(i)aleph0 10049
[Suppes] p. 228Theorem Schema 61onintss 6413
[Suppes] p. 228Theorem Schema 62onminesb 7791  onminsb 7792
[Suppes] p. 229Theorem 64alephval2 10556
[Suppes] p. 229Theorem 65alephcard 10053
[Suppes] p. 229Theorem 66alephord2i 10060
[Suppes] p. 229Theorem 67alephnbtwn 10054
[Suppes] p. 229Definition 12df-aleph 9925
[Suppes] p. 242Theorem 6weth 10478
[Suppes] p. 242Theorem 8entric 10540
[Suppes] p. 242Theorem 9carden 10534
[Szendrei] p. 11Line 6df-cloneop 36154
[Szendrei] p. 11Paragraph 3df-suppos 36158
[TakeutiZaring] p. 8Axiom 1ax-ext 2733
[TakeutiZaring] p. 13Definition 4.5df-cleq 2753  wl-df.cleq 38120
[TakeutiZaring] p. 13Proposition 4.6df-clel 2836  wl-df.clel 38123
[TakeutiZaring] p. 13Proposition 4.9cvjust 2755
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2781
[TakeutiZaring] p. 14Definition 4.16df-oprab 7414
[TakeutiZaring] p. 14Proposition 4.14ru 3742
[TakeutiZaring] p. 15Axiom 2zfpair 5392
[TakeutiZaring] p. 15Exercise 1elpr 4613  elpr2 4615  elpr2g 4614  elprg 4611
[TakeutiZaring] p. 15Exercise 2elsn 4603  elsn2 4630  elsn2g 4629  elsng 4602  velsn 4604
[TakeutiZaring] p. 15Exercise 3elop 5449
[TakeutiZaring] p. 15Exercise 4sneq 4598  sneqr 4804
[TakeutiZaring] p. 15Definition 5.1dfpr2 4609  dfsn2 4601  dfsn2ALT 4610
[TakeutiZaring] p. 16Axiom 3uniex 7739
[TakeutiZaring] p. 16Exercise 6opth 5458
[TakeutiZaring] p. 16Exercise 7opex 5445
[TakeutiZaring] p. 16Exercise 8rext 5429
[TakeutiZaring] p. 16Corollary 5.8unex 7742  unexg 7741
[TakeutiZaring] p. 16Definition 5.3dftp2 4656
[TakeutiZaring] p. 16Definition 5.5df-uni 4872
[TakeutiZaring] p. 16Definition 5.6df-in 3911  df-un 3909
[TakeutiZaring] p. 16Proposition 5.7unipr 4888  uniprg 4887
[TakeutiZaring] p. 17Axiom 4vpwex 5348
[TakeutiZaring] p. 17Exercise 1eltp 4654
[TakeutiZaring] p. 17Exercise 5elsuc 6433  elsucg 6431  sstr2 3943
[TakeutiZaring] p. 17Exercise 6uncom 4111
[TakeutiZaring] p. 17Exercise 7incom 4161
[TakeutiZaring] p. 17Exercise 8unass 4124
[TakeutiZaring] p. 17Exercise 9inass 4179
[TakeutiZaring] p. 17Exercise 10indi 4236
[TakeutiZaring] p. 17Exercise 11undi 4237
[TakeutiZaring] p. 17Definition 5.9df-pss 3924  df-ss 3921
[TakeutiZaring] p. 17Definition 5.10df-pw 4563
[TakeutiZaring] p. 18Exercise 7unss2 4139
[TakeutiZaring] p. 18Exercise 9dfss2 3922  sseqin2 4175
[TakeutiZaring] p. 18Exercise 10ssid 3958
[TakeutiZaring] p. 18Exercise 12inss1 4188  inss2 4189
[TakeutiZaring] p. 18Exercise 13nss 4000
[TakeutiZaring] p. 18Exercise 15unieq 4882
[TakeutiZaring] p. 18Exercise 18sspwb 5430  sspwimp 45596  sspwimpALT 45603  sspwimpALT2 45606  sspwimpcf 45598
[TakeutiZaring] p. 18Exercise 19pweqb 5437
[TakeutiZaring] p. 19Axiom 5ax-rep 5237
[TakeutiZaring] p. 20Definitiondf-rab 3415
[TakeutiZaring] p. 20Corollary 5.160ex 5269
[TakeutiZaring] p. 20Definition 5.12df-dif 3907
[TakeutiZaring] p. 20Definition 5.14bj-dfnul2 37129  dfnul2 4288
[TakeutiZaring] p. 20Proposition 5.15difid 4331
[TakeutiZaring] p. 20Proposition 5.17(1)n0 4306  n0f 4302  neq0 4305  neq0f 4301
[TakeutiZaring] p. 21Axiom 6zfreg 9557
[TakeutiZaring] p. 21Axiom 6'zfregs 9700
[TakeutiZaring] p. 21Theorem 5.22setind 9715
[TakeutiZaring] p. 21Definition 5.20df-v 3455
[TakeutiZaring] p. 21Proposition 5.21vprc 5282
[TakeutiZaring] p. 22Exercise 10ss 4356
[TakeutiZaring] p. 22Exercise 3ssex 5290  ssexg 5289
[TakeutiZaring] p. 22Exercise 4inex1 5285
[TakeutiZaring] p. 22Exercise 5ruv 9569
[TakeutiZaring] p. 22Exercise 6elirr 9561
[TakeutiZaring] p. 22Exercise 7ssdif0 4320
[TakeutiZaring] p. 22Exercise 11difdif 4088
[TakeutiZaring] p. 22Exercise 13undif3 4252  undif3VD 45560
[TakeutiZaring] p. 22Exercise 14difss 4089
[TakeutiZaring] p. 22Exercise 15sscon 4096
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 3078
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 3088
[TakeutiZaring] p. 23Proposition 6.2xpex 7751  xpexg 7748
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 5668
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 6607
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 6785  fun11 6610
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 6549  svrelfun 6608
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5877
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5879
[TakeutiZaring] p. 24Definition 6.6(1)df-res 5673
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 5674
[TakeutiZaring] p. 24Definition 6.6(3)df-co 5670
[TakeutiZaring] p. 25Exercise 2cnvcnvss 6192  dfrel2 6187
[TakeutiZaring] p. 25Exercise 3xpss 5677
[TakeutiZaring] p. 25Exercise 5relun 5798
[TakeutiZaring] p. 25Exercise 6reluni 5805
[TakeutiZaring] p. 25Exercise 9inxp 5818
[TakeutiZaring] p. 25Exercise 12relres 6004
[TakeutiZaring] p. 25Exercise 13opelres 5984  opelresi 5986
[TakeutiZaring] p. 25Exercise 14dmres 6011
[TakeutiZaring] p. 25Exercise 15resss 6000
[TakeutiZaring] p. 25Exercise 17resabs1 6005
[TakeutiZaring] p. 25Exercise 18funres 6578
[TakeutiZaring] p. 25Exercise 24relco 6110
[TakeutiZaring] p. 25Exercise 29funco 6576
[TakeutiZaring] p. 25Exercise 30f1co 6787
[TakeutiZaring] p. 26Definition 6.10eu2 2635
[TakeutiZaring] p. 26Definition 6.11conventions 30717  df-fv 6544  fv3 6899
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 7921  cnvexg 7920
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 7905  dmexg 7897
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 7906  rnexg 7898
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 45132
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 7916
[TakeutiZaring] p. 27Corollary 6.13fvex 6894
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 47878  tz6.12-1-afv2 47945  tz6.12-1 6904  tz6.12-afv 47877  tz6.12-afv2 47944  tz6.12 6905  tz6.12c-afv2 47946  tz6.12c 6903
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2-afv2 47941  tz6.12-2 6868  tz6.12i-afv2 47947  tz6.12i 6907
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 6539
[TakeutiZaring] p. 27Definition 6.15(3)df-f 6540
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 6542  wfo 6534
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 6541  wf1 6533
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 6543  wf1o 6535
[TakeutiZaring] p. 28Exercise 4eqfnfv 7025  eqfnfv2 7026  eqfnfv2f 7029
[TakeutiZaring] p. 28Exercise 5fvco 6979
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 7215
[TakeutiZaring] p. 28Proposition 6.17resfunexg 7213
[TakeutiZaring] p. 29Exercise 9funimaex 6623  funimaexg 6622
[TakeutiZaring] p. 29Definition 6.18df-br 5109
[TakeutiZaring] p. 29Definition 6.19(1)df-so 5570
[TakeutiZaring] p. 30Definition 6.21dffr2 5622  dffr3 6101  eliniseg 6096  iniseg 6099
[TakeutiZaring] p. 30Definition 6.22df-eprel 5561
[TakeutiZaring] p. 30Proposition 6.23fr2nr 5638  fr3nr 7770  frirr 5637
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 5614
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 7772
[TakeutiZaring] p. 31Exercise 1frss 5625
[TakeutiZaring] p. 31Exercise 4wess 5647
[TakeutiZaring] p. 31Proposition 6.26tz6.26 6348  tz6.26i 6349  wefrc 5655  wereu2 5658
[TakeutiZaring] p. 32Theorem 6.27wfi 6350  wfii 6351
[TakeutiZaring] p. 32Definition 6.28df-isom 6545
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 7327
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 7328
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 7334
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 7335
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 7336
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 7340
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 7347
[TakeutiZaring] p. 34Proposition 6.33f1oiso 7349
[TakeutiZaring] p. 35Notationwtr 5217
[TakeutiZaring] p. 35Theorem 7.2trelpss 45133  tz7.2 5644
[TakeutiZaring] p. 35Definition 7.1dftr3 5222
[TakeutiZaring] p. 36Proposition 7.4ordwe 6373
[TakeutiZaring] p. 36Proposition 7.5tz7.5 6381
[TakeutiZaring] p. 36Proposition 7.6ordelord 6382  ordelordALT 45216  ordelordALTVD 45545
[TakeutiZaring] p. 37Corollary 7.8ordelpss 6388  ordelssne 6387
[TakeutiZaring] p. 37Proposition 7.7tz7.7 6386
[TakeutiZaring] p. 37Proposition 7.9ordin 6391
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 7780
[TakeutiZaring] p. 38Corollary 7.15ordsson 7781
[TakeutiZaring] p. 38Definition 7.11df-on 6364
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 6393
[TakeutiZaring] p. 38Proposition 7.12onfrALT 45228  ordon 7775
[TakeutiZaring] p. 38Proposition 7.13onprc 7776
[TakeutiZaring] p. 39Theorem 7.17tfi 7848
[TakeutiZaring] p. 40Exercise 3ontr2 6409
[TakeutiZaring] p. 40Exercise 7dftr2 5219
[TakeutiZaring] p. 40Exercise 9onssmin 7790
[TakeutiZaring] p. 40Exercise 11unon 7826
[TakeutiZaring] p. 40Exercise 12ordun 6467
[TakeutiZaring] p. 40Exercise 14ordequn 6466
[TakeutiZaring] p. 40Proposition 7.19ssorduni 7777
[TakeutiZaring] p. 40Proposition 7.20elssuni 4903
[TakeutiZaring] p. 41Definition 7.22df-suc 6366
[TakeutiZaring] p. 41Proposition 7.23sssucid 6443  sucidg 6444
[TakeutiZaring] p. 41Proposition 7.24onsuc 7808
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 6457  ordnbtwn 6456
[TakeutiZaring] p. 41Proposition 7.26onsucuni 7823
[TakeutiZaring] p. 42Exercise 1df-lim 6365
[TakeutiZaring] p. 42Exercise 4omssnlim 7876
[TakeutiZaring] p. 42Exercise 7ssnlim 7881
[TakeutiZaring] p. 42Exercise 8onsucssi 7836  ordelsuc 7815
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 7817
[TakeutiZaring] p. 42Definition 7.27nlimon 7846
[TakeutiZaring] p. 42Definition 7.28dfom2 7863
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 7884
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 7885
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 7886
[TakeutiZaring] p. 43Remarkomon 7873
[TakeutiZaring] p. 43Axiom 7inf3 9603  omex 9611
[TakeutiZaring] p. 43Theorem 7.32ordom 7871
[TakeutiZaring] p. 43Corollary 7.31find 7891
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 7888
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 7889
[TakeutiZaring] p. 44Exercise 1limomss 7866
[TakeutiZaring] p. 44Exercise 2int0 4926
[TakeutiZaring] p. 44Exercise 3trintss 5236
[TakeutiZaring] p. 44Exercise 4intss1 4927
[TakeutiZaring] p. 44Exercise 5intex 5314
[TakeutiZaring] p. 44Exercise 6oninton 7793
[TakeutiZaring] p. 44Exercise 11ordintdif 6412
[TakeutiZaring] p. 44Definition 7.35df-int 4912
[TakeutiZaring] p. 44Proposition 7.34noinfep 9628
[TakeutiZaring] p. 45Exercise 4onint 7788
[TakeutiZaring] p. 47Lemma 1tfrlem1 8361
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 8383
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 8384
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 8385
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 8392  tz7.44-2 8393  tz7.44-3 8394
[TakeutiZaring] p. 50Exercise 1smogt 8353
[TakeutiZaring] p. 50Exercise 3smoiso 8348
[TakeutiZaring] p. 50Definition 7.46df-smo 8332
[TakeutiZaring] p. 51Proposition 7.49tz7.49 8431  tz7.49c 8432
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 8429
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 8428
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 8430
[TakeutiZaring] p. 53Proposition 7.532eu5 2681
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 9994
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 9995
[TakeutiZaring] p. 56Definition 8.1oalim 8516  oasuc 8508
[TakeutiZaring] p. 57Remarktfindsg 7856
[TakeutiZaring] p. 57Proposition 8.2oacl 8519
[TakeutiZaring] p. 57Proposition 8.3oa0 8500  oa0r 8522
[TakeutiZaring] p. 57Proposition 8.16omcl 8520
[TakeutiZaring] p. 58Corollary 8.5oacan 8532
[TakeutiZaring] p. 58Proposition 8.4nnaord 8604  nnaordi 8603  oaord 8531  oaordi 8530
[TakeutiZaring] p. 59Proposition 8.6iunss2 5013  uniss2 4906
[TakeutiZaring] p. 59Proposition 8.7oawordri 8534
[TakeutiZaring] p. 59Proposition 8.8oawordeu 8539  oawordex 8541
[TakeutiZaring] p. 59Proposition 8.9nnacl 8596
[TakeutiZaring] p. 59Proposition 8.10oaabs 8633
[TakeutiZaring] p. 60Remarkoancom 9619
[TakeutiZaring] p. 60Proposition 8.11oalimcl 8544
[TakeutiZaring] p. 62Exercise 1nnarcl 8601
[TakeutiZaring] p. 62Exercise 5oaword1 8536
[TakeutiZaring] p. 62Definition 8.15om0x 8503  omlim 8517  omsuc 8510
[TakeutiZaring] p. 62Definition 8.15(a)om0 8501
[TakeutiZaring] p. 63Proposition 8.17nnecl 8598  nnmcl 8597
[TakeutiZaring] p. 63Proposition 8.19nnmord 8617  nnmordi 8616  omord 8552  omordi 8550
[TakeutiZaring] p. 63Proposition 8.20omcan 8553
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 8621  omwordri 8556
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 8523
[TakeutiZaring] p. 63Proposition 8.18(2)om1 8526  om1r 8527
[TakeutiZaring] p. 64Proposition 8.22om00 8559
[TakeutiZaring] p. 64Proposition 8.23omordlim 8561
[TakeutiZaring] p. 64Proposition 8.24omlimcl 8562
[TakeutiZaring] p. 64Proposition 8.25odi 8563
[TakeutiZaring] p. 65Theorem 8.26omass 8564
[TakeutiZaring] p. 67Definition 8.30nnesuc 8593  oe0 8506  oelim 8518  oesuc 8511  onesuc 8514
[TakeutiZaring] p. 67Proposition 8.31oe0m0 8504
[TakeutiZaring] p. 67Proposition 8.32oen0 8571
[TakeutiZaring] p. 67Proposition 8.33oeordi 8572
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 8505
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 8529
[TakeutiZaring] p. 68Corollary 8.34oeord 8573
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 8579
[TakeutiZaring] p. 68Proposition 8.35oewordri 8577
[TakeutiZaring] p. 68Proposition 8.37oeworde 8578
[TakeutiZaring] p. 69Proposition 8.41oeoa 8582
[TakeutiZaring] p. 70Proposition 8.42oeoe 8584
[TakeutiZaring] p. 73Theorem 9.1trcl 9696  tz9.1 9697
[TakeutiZaring] p. 76Definition 9.9df-r1 9735  r10 9739  r1lim 9743  r1limg 9742  r1suc 9741  r1sucg 9740
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 9751  r1ord2 9752  r1ordg 9749
[TakeutiZaring] p. 78Proposition 9.12tz9.12 9761
[TakeutiZaring] p. 78Proposition 9.13rankwflem 9786  tz9.13 9762  tz9.13g 9763
[TakeutiZaring] p. 79Definition 9.14df-rank 9736  rankval 9787  rankvalb 9768  rankvalg 9788
[TakeutiZaring] p. 79Proposition 9.16rankel 9810  rankelb 9795
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 9824  rankval3 9811  rankval3b 9797
[TakeutiZaring] p. 79Proposition 9.18rankonid 9800
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 9766
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 9805  rankr1c 9792  rankr1g 9803
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 9806
[TakeutiZaring] p. 80Exercise 1rankss 9820  rankssb 9819
[TakeutiZaring] p. 80Exercise 2unbndrank 9813
[TakeutiZaring] p. 80Proposition 9.19bndrank 9812
[TakeutiZaring] p. 83Axiom of Choiceac4 10458  dfac3 10104
[TakeutiZaring] p. 84Theorem 10.3dfac8a 10013  numth 10455  numth2 10454
[TakeutiZaring] p. 85Definition 10.4cardval 10529
[TakeutiZaring] p. 85Proposition 10.5cardid 10530  cardid2 9938
[TakeutiZaring] p. 85Proposition 10.9oncard 9945
[TakeutiZaring] p. 85Proposition 10.10carden 10534
[TakeutiZaring] p. 85Proposition 10.11cardidm 9944
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 9929
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 9950
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 9942
[TakeutiZaring] p. 87Proposition 10.15pwen 9137
[TakeutiZaring] p. 88Exercise 1en0 9014
[TakeutiZaring] p. 88Exercise 7infensuc 9142
[TakeutiZaring] p. 89Exercise 10omxpen 9066
[TakeutiZaring] p. 90Corollary 10.23cardnn 9948
[TakeutiZaring] p. 90Definition 10.27alephiso 10081
[TakeutiZaring] p. 90Proposition 10.20nneneq 9189
[TakeutiZaring] p. 90Proposition 10.22onomeneq 9197
[TakeutiZaring] p. 90Proposition 10.26alephprc 10082
[TakeutiZaring] p. 90Corollary 10.21(1)php5 9194
[TakeutiZaring] p. 91Exercise 2alephle 10071
[TakeutiZaring] p. 91Exercise 3aleph0 10049
[TakeutiZaring] p. 91Exercise 4cardlim 9957
[TakeutiZaring] p. 91Exercise 7infpss 10198
[TakeutiZaring] p. 91Exercise 8infcntss 9281
[TakeutiZaring] p. 91Definition 10.29df-fin 8946  isfi 8971
[TakeutiZaring] p. 92Proposition 10.32onfin 9198
[TakeutiZaring] p. 92Proposition 10.34imadomg 10517
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 9059
[TakeutiZaring] p. 93Proposition 10.35fodomb 10509
[TakeutiZaring] p. 93Proposition 10.36djuxpdom 10168  unxpdom 9218
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 9959  cardsdomelir 9958
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 9220
[TakeutiZaring] p. 94Proposition 10.39infxpen 9997
[TakeutiZaring] p. 95Definition 10.42df-map 8825
[TakeutiZaring] p. 95Proposition 10.40infxpidm 10545  infxpidm2 10000
[TakeutiZaring] p. 95Proposition 10.41infdju 10189  infxp 10196
[TakeutiZaring] p. 96Proposition 10.44pw2en 9071  pw2f1o 9069
[TakeutiZaring] p. 96Proposition 10.45mapxpen 9130
[TakeutiZaring] p. 97Theorem 10.46ac6s3 10470
[TakeutiZaring] p. 98Theorem 10.46ac6c5 10465  ac6s5 10474
[TakeutiZaring] p. 98Theorem 10.47unidom 10526
[TakeutiZaring] p. 99Theorem 10.48uniimadom 10527  uniimadomf 10528
[TakeutiZaring] p. 100Definition 11.1cfcof 10257
[TakeutiZaring] p. 101Proposition 11.7cofsmo 10252
[TakeutiZaring] p. 102Exercise 1cfle 10236
[TakeutiZaring] p. 102Exercise 2cf0 10233
[TakeutiZaring] p. 102Exercise 3cfsuc 10240
[TakeutiZaring] p. 102Exercise 4cfom 10247
[TakeutiZaring] p. 102Proposition 11.9coftr 10256
[TakeutiZaring] p. 103Theorem 11.15alephreg 10566
[TakeutiZaring] p. 103Proposition 11.11cardcf 10234
[TakeutiZaring] p. 103Proposition 11.13alephsing 10259
[TakeutiZaring] p. 104Corollary 11.17cardinfima 10080
[TakeutiZaring] p. 104Proposition 11.16carduniima 10079
[TakeutiZaring] p. 104Proposition 11.18alephfp 10091  alephfp2 10092
[TakeutiZaring] p. 106Theorem 11.20gchina 10683
[TakeutiZaring] p. 106Theorem 11.21mappwen 10095
[TakeutiZaring] p. 107Theorem 11.26konigth 10553
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 10567
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 10568
[Tarski] p. 67Axiom B5ax-c5 39625
[Tarski] p. 67Scheme B5sp 2217
[Tarski] p. 68Lemma 6avril1 30780  equid 2040
[Tarski] p. 69Lemma 7equcomi 2045
[Tarski] p. 70Lemma 14spim 2417  spime 2419  spimew 1999
[Tarski] p. 70Lemma 16ax-12 2211  ax-c15 39631  ax12i 1994
[Tarski] p. 70Lemmas 16 and 17sb6 2117
[Tarski] p. 75Axiom B7ax6v 1996
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1938  ax5ALT 39649
[Tarski], p. 75Scheme B8 of system S2ax-7 2036  ax-8 2143  ax-9 2151
[Tarski1999] p. 178Axiom 4axtgsegcon 28709
[Tarski1999] p. 178Axiom 5axtg5seg 28710
[Tarski1999] p. 179Axiom 7axtgpasch 28712
[Tarski1999] p. 180Axiom 7.1axtgpasch 28712
[Tarski1999] p. 185Axiom 11axtgcont1 28713
[Truss] p. 114Theorem 5.18ruc 16298
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 38276
[Viaclovsky8] p. 3Proposition 7ismblfin 38278
[Weierstrass] p. 272Definitiondf-mdet 22721  mdetuni 22758
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 916
[WhiteheadRussell] p. 96Axiom *1.3olc 881
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 882
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 932
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 983
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 190
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 136
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 91  wl-luk-pm2.04 38057
[WhiteheadRussell] p. 100Theorem *2.05frege5 44496  imim2 59  wl-luk-imim2 38052
[WhiteheadRussell] p. 100Theorem *2.06adh-minimp-imim1 47723  imim1 84
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 909
[WhiteheadRussell] p. 101Theorem *2.06barbara 2688  syl 18
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 915
[WhiteheadRussell] p. 101Theorem *2.08id 23  wl-luk-id 38055
[WhiteheadRussell] p. 101Theorem *2.11exmid 907
[WhiteheadRussell] p. 101Theorem *2.12notnot 143
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 910
[WhiteheadRussell] p. 102Theorem *2.14notnotr 131  notnotrALT2 45605  wl-luk-notnotr 38056
[WhiteheadRussell] p. 102Theorem *2.15con1 147
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 44526  axfrege28 44525  con3 154
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 129
[WhiteheadRussell] p. 104Theorem *2.2orc 880
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 937
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 124  wl-luk-pm2.21 38049
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 125
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 902
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 954
[WhiteheadRussell] p. 104Theorem *2.27conventions-labels 30718  pm2.27 43  wl-luk-pm2.27 38047
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 935
[WhiteheadRussell] p. 104Proof begins with references *2.21 ( ~ pm2.21 ) and *14.26 ( ~ eupickbi )mopickr 38988
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 936
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 985
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 986
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 984
[WhiteheadRussell] p. 105Definition *2.33df-3or 1102
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 919
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 920
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 957
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 57
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 894
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 895
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 170  pm2.5g 169
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 193
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 896
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 897
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 898
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 173
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 174
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 864
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 865
[WhiteheadRussell] p. 107Theorem *2.55orel1 901
[WhiteheadRussell] p. 107Theorem *2.56orel2 903
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 194
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 912
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 955
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 956
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 195
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 904  pm2.67 905
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 177  pm2.521g 175  pm2.521g2 176
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 911
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 988
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 913
[WhiteheadRussell] p. 108Theorem *2.69looinv 206
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 989
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 990
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 946
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 944
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 987
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 991
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 85
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 945
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 110
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 1007
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 474  pm3.2im 161
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 1008
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 1009
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 1010
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 1011
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 476
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 464
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 407
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 814
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 453
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 454
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 487  simplim 168
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 489  simprim 167
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 776
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 777
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 819
[WhiteheadRussell] p. 113Fact)pm3.45 633
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 821
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 497
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 498
[WhiteheadRussell] p. 113Theorem *3.44jao 975  pm3.44 974
[WhiteheadRussell] p. 113Theorem *3.47anim12 820
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 478
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 978
[WhiteheadRussell] p. 116Theorem *4.1con34b 319
[WhiteheadRussell] p. 117Theorem *4.2biid 264
[WhiteheadRussell] p. 117Theorem *4.11notbi 322
[WhiteheadRussell] p. 117Theorem *4.12con2bi 356
[WhiteheadRussell] p. 117Theorem *4.13notnotb 318
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 818
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 845
[WhiteheadRussell] p. 117Theorem *4.21bicom 225
[WhiteheadRussell] p. 117Theorem *4.22biantr 817  bitr 816
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 573
[WhiteheadRussell] p. 117Theorem *4.25oridm 917  pm4.25 918
[WhiteheadRussell] p. 118Theorem *4.3ancom 465
[WhiteheadRussell] p. 118Theorem *4.4andi 1023
[WhiteheadRussell] p. 118Theorem *4.31orcom 883
[WhiteheadRussell] p. 118Theorem *4.32anass 473
[WhiteheadRussell] p. 118Theorem *4.33orass 934
[WhiteheadRussell] p. 118Theorem *4.36anbi1 644
[WhiteheadRussell] p. 118Theorem *4.37orbi1 930
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 648
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 992
[WhiteheadRussell] p. 118Definition *4.34df-3an 1103
[WhiteheadRussell] p. 119Theorem *4.41ordi 1021
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 1067
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 1038
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 1012
[WhiteheadRussell] p. 119Theorem *4.45orabs 1014  pm4.45 1013  pm4.45im 840
[WhiteheadRussell] p. 120Theorem *4.5anor 998
[WhiteheadRussell] p. 120Theorem *4.6imor 866
[WhiteheadRussell] p. 120Theorem *4.7anclb 554
[WhiteheadRussell] p. 120Theorem *4.51ianor 997
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 1000
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 1001
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 1002
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 1003
[WhiteheadRussell] p. 120Theorem *4.56ioran 999  pm4.56 1004
[WhiteheadRussell] p. 120Theorem *4.57oran 1005  pm4.57 1006
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 409
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 869
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 402
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 862
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 410
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 863
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 403
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 566  pm4.71d 570  pm4.71i 568  pm4.71r 567  pm4.71rd 571  pm4.71ri 569
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 964
[WhiteheadRussell] p. 121Theorem *4.73iba 536
[WhiteheadRussell] p. 121Theorem *4.74biorf 949
[WhiteheadRussell] p. 121Theorem *4.76jcab 526  pm4.76 527
[WhiteheadRussell] p. 121Theorem *4.77jaob 976  pm4.77 977
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 947
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 1019
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 397
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 398
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 1039
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 1040
[WhiteheadRussell] p. 122Theorem *4.84imbi1 350
[WhiteheadRussell] p. 122Theorem *4.85imbi2 351
[WhiteheadRussell] p. 122Theorem *4.86bibi1 354
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 391  impexp 455  pm4.87 856
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 835
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 959  pm5.11g 958
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 960
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 962
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 961
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 1028
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 1029
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 1027
[WhiteheadRussell] p. 124Theorem *5.18nbbn 386  pm5.18 384
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 390
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 836
[WhiteheadRussell] p. 124Theorem *5.22xor 1030
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 1063
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 1064
[WhiteheadRussell] p. 124Theorem *5.25dfor2 914
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 582
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 392
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 364
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 1017
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 968
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 843
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 583
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 848
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 837
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 846
[WhiteheadRussell] p. 125Theorem *5.41imdi 393  pm5.41 394
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 552
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 551
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 1020
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 1033
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 963
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 1016
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 1034
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 1035
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 1043
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 369
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 273
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 1044
[WhiteheadRussell] p. 145Theorem *10.3bj-alsyl 37180
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 45038
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 45039
[WhiteheadRussell] p. 147Theorem *10.2219.26 1898
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 45040
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 45041
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 45042
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1921
[WhiteheadRussell] p. 151Theorem *10.301albitr 45043
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 45044
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 45045
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 45046
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 45047
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 45049
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 45050
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 45051
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 45048
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2122
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 45054
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 45055
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2102
[WhiteheadRussell] p. 160Theorem *11.21alrot3 2193
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1857
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1858
[WhiteheadRussell] p. 161Theorem *11.319.21vv 45056
[WhiteheadRussell] p. 162Theorem *11.322alim 45057
[WhiteheadRussell] p. 162Theorem *11.332albi 45058
[WhiteheadRussell] p. 162Theorem *11.342exim 45059
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 45061
[WhiteheadRussell] p. 162Theorem *11.3412exbi 45060
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1915
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 45063
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 45064
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 45062
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1856
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 45065
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 45066
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1874
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 45067
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2376
[WhiteheadRussell] p. 164Theorem *11.5212exanali 1888
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 45072
[WhiteheadRussell] p. 165Theorem *11.56aaanv 45068
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 45069
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 45070
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 45071
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 45076
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 45073
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 45074
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 45075
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 45077
[WhiteheadRussell] p. 175Definition *14.02df-eu 2595
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 45087  pm13.13b 45088
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 45089
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 3037
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 3038
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3624
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 45095
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 45096
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 45090
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 45231  pm13.193 45091
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 45092
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 45093
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 45094
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 45101
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 45100
[WhiteheadRussell] p. 184Definition *14.01iotasbc 45099
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3805
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 45102  pm14.122b 45103  pm14.122c 45104
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 45105  pm14.123b 45106  pm14.123c 45107
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 45109
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 45108
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 45110
[WhiteheadRussell] p. 190Theorem *14.22iota4 6517
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 45111
[WhiteheadRussell] p. 191Theorem *14.23iota4an 6518
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 45112
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 45114
[WhiteheadRussell] p. 192Theorem *14.26eupick 2659  eupickbi 2662  sbaniota 45115
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 45113
[WhiteheadRussell] p. 192Theorem *14.271eubi 2610
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 45116
[WhiteheadRussell] p. 235Definition *30.01conventions 30717  df-fv 6544
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 9986  pm54.43lem 9985
[Young] p. 141Definition of operator orderingleop2 32442
[Young] p. 142Example 12.2(i)0leop 32448  idleop 32449
[vandenDries] p. 42Lemma 61irrapx1 43525
[vandenDries] p. 43Theorem 62pellex 43532  pellexlem1 43526

This page was last updated on 27-Jul-2026.
Copyright terms: Public domain